============================== Prover9 ===============================
Prover9 (32) version November-2006, November 2006.
Process 3830 was started by mccune on cleo.thornwood,
Wed Nov 22 11:23:58 2006
The command was "/home/mccune/bin/prover9 -f a2.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file a2.in


formulas(sos).
(((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (((w v x) ^ (v6 v x)) v v7) = x # label(A2).
end_of_list.

formulas(goals).
y v (x ^ (y ^ z)) = y & y ^ (x v (y v z)) = y & ((x ^ y) v (y ^ z)) v y = y & ((x v y) ^ (y v z)) ^ y = y # answer(McKenzie).
end_of_list.

============================== end of input ==========================

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:
1 y v (x ^ (y ^ z)) = y & y ^ (x v (y v z)) = y & ((x ^ y) v (y ^ z)) v y = y & ((x v y) ^ (y v z)) ^ y = y # answer(McKenzie) # label(goal).  [goal].

============================== end of process non-clausal formulas ===

============================== PROCESS INITIAL CLAUSES ===============

% Clauses before input processing:

formulas(usable).
end_of_list.

formulas(sos).
(((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (((w v y) ^ (v6 v y)) v v7) = y # label(A2).  [assumption].
c1 v (c2 ^ (c1 ^ c3)) != c1 | c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 | ((c2 v c1) ^ (c1 v c3)) ^ c1 != c1 # answer(McKenzie).  [deny(1)].
end_of_list.

formulas(demodulators).
end_of_list.

============================== PREDICATE ELIMINATION =================

No predicates eliminated.

============================== end predicate elimination =============

Auto_denials:  (no changes).

Term ordering decisions:
Relation symbol precedence:  lex([ = ]).
Function symbol precedence:  lex([ c1, c2, c3, v, ^ ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)
    % set(paramodulation) -> set(back_demod).
  % set(hyper_resolution).  % (nonunit Horn with equality)
  % set(neg_ur_resolution).  % (nonunit Horn with equality)
  % assign(para_lit_limit, 4).  % (nonunit Horn with equality)

Auto_process settings:
  % set(back_unit_deletion).  % (Horn set with negative nonunits)
    % set(back_unit_deletion) -> set(unit_deletion).

============================== end of process initial clauses ========

============================== CLAUSES FOR SEARCH ====================

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
2 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (((w v y) ^ (v6 v y)) v v7) = y # label(A2).  [assumption].
3 c1 v (c2 ^ (c1 ^ c3)) != c1 | c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 | ((c2 v c1) ^ (c1 v c3)) ^ c1 != c1 # answer(McKenzie).  [deny(1)].
end_of_list.

formulas(demodulators).
2 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (((w v y) ^ (v6 v y)) v v7) = y # label(A2).  [assumption].
end_of_list.

============================== end of clauses for search =============

============================== SEARCH ================================

% Starting search at 0.00 seconds.

given #1 (I,wt=29): 2 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (((w v y) ^ (v6 v y)) v v7) = y # label(A2).  [assumption].

given #2 (I,wt=40): 3 c1 v (c2 ^ (c1 ^ c3)) != c1 | c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 | ((c2 v c1) ^ (c1 v c3)) ^ c1 != c1 # answer(McKenzie).  [deny(1)].

given #3 (F,wt=21): 6 (((x v y) ^ y) v (y v y)) ^ (((z v y) ^ (u v y)) v v) = y.  [para(2(a,1),2(a,1,1,2))].

given #4 (T,wt=25): 10 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (y v z) = y v y.  [para(6(a,1),6(a,1,2,1))].

given #5 (T,wt=27): 11 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (((v v y) ^ (w v y)) v v6) = y.  [para(10(a,1),2(a,1,1,2,1,1))].

given #6 (A,wt=61): 4 (((x v ((y v z) ^ (u v z))) ^ ((y v z) ^ (u v z))) v ((z v (v ^ ((y v z) ^ (u v z)))) ^ w)) ^ (((v6 v ((y v z) ^ (u v z))) ^ (v7 v ((y v z) ^ (u v z)))) v v8) = (y v z) ^ (u v z).  [para(2(a,1),2(a,1,1,2,1,1))].

given #7 (F,wt=33): 17 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (z ^ (y v y))) ^ u)) ^ (y v v) = y v y.  [para(6(a,1),11(a,1,2,1))].

given #8 (F,wt=31): 29 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (y v y)) ^ z)) ^ (y v u) = y v y.  [para(10(a,1),17(a,1,1,2,1,2))].

given #9 (T,wt=33): 25 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) ^ (((v6 v y) ^ (v7 v y)) v v8) = y.  [para(11(a,1),4(a,1,1,1,1,2)),rewrite(11(17),11(22),11(26),11(27),11(31))].

given #10 (T,wt=21): 37 (((x v y) ^ y) v (z ^ y)) ^ (((u v y) ^ (v v y)) v w) = y.  [para(2(a,1),25(a,1,1,2))].

given #11 (A,wt=83): 5 (((x v (((y v z) ^ (u v z)) v v)) ^ (((y v z) ^ (u v z)) v v)) v (((w ^ ((((y v z) ^ (u v z)) v v) v (((y v z) ^ (u v z)) v v))) v z) ^ v6)) ^ (((v7 v (((y v z) ^ (u v z)) v v)) ^ (v8 v (((y v z) ^ (u v z)) v v))) v v9) = ((y v z) ^ (u v z)) v v.  [para(2(a,1),2(a,1,1,2,1,2))].

given #12 (F,wt=23): 50 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (y v u) = y v y.  [para(6(a,1),37(a,1,2,1))].

given #13 (F,wt=21): 70 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (y v z) = y v y.  [para(10(a,1),50(a,1,1,2))].

given #14 (T,wt=15): 87 ((x v x) v (x v x)) ^ (x v y) = x v x.  [para(70(a,1),70(a,1,1,1))].

given #15 (T,wt=17): 86 ((x v x) v (y ^ (x v x))) ^ (x v z) = x v x.  [para(70(a,1),50(a,1,1,1))].

given #16 (A,wt=83): 7 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v (((w ^ ((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v))) v (v6 ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v7)) ^ (z v v8) = ((y ^ (z v z)) v (u ^ z)) ^ v.  [para(2(a,1),2(a,1,2,1))].

given #17 (F,wt=19): 75 ((x v x) v ((x v x) v (x v x))) ^ (x v y) = x v x.  [para(70(a,1),10(a,1,1,1))].

given #18 (F,wt=23): 60 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (z v v) = y ^ z.  [para(37(a,1),37(a,1,2,1))].

given #19 (T,wt=15): 107 ((x v x) v (y ^ x)) ^ (x v z) = x v x.  [para(60(a,1),86(a,1,1,2))].

given #20 (T,wt=21): 106 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (y v u) = y v y.  [para(60(a,1),50(a,1,1,2))].

given #21 (A,wt=35): 8 (((x v (y v y)) ^ (y v y)) v (((z ^ ((y v y) v (y v y))) v (u ^ (y v y))) ^ v)) ^ (y v w) = y v y.  [para(6(a,1),2(a,1,2,1))].

given #22 (F,wt=23): 96 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (x v v) = x v x.  [para(7(a,1),86(a,1,1,2))].

given #23 (F,wt=21): 137 ((x v x) v (((x v x) v (y ^ x)) ^ z)) ^ (x v u) = x v x.  [para(10(a,1),96(a,1,1,2,1,1))].

given #24 (T,wt=21): 147 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (x v v) = x v x.  [para(60(a,1),96(a,1,1,2,1,1))].

given #25 (T,wt=13): 164 ((x v x) v x) ^ (x v y) = x v x.  [para(2(a,1),147(a,1,1,2))].

given #26 (A,wt=65): 9 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v ((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ (z v w) = ((y ^ (z v z)) v (u ^ z)) ^ v.  [para(2(a,1),6(a,1,2,1))].

given #27 (F,wt=17): 179 (((x v y) ^ y) v (y v y)) ^ ((y v y) v z) = y.  [para(164(a,1),6(a,1,2,1))].

given #28 (F,wt=17): 184 (((x v y) ^ y) v (z ^ y)) ^ ((y v y) v u) = y.  [para(164(a,1),37(a,1,2,1))].

given #29 (T,wt=19): 201 (((x v y) ^ y) v (z ^ y)) ^ (((y v y) v u) v v) = y.  [para(179(a,1),60(a,1,1,1,1,2)),rewrite(179(8),179(9),179(15))].

given #30 (T,wt=21): 231 (((x v y) ^ y) v (z ^ y)) ^ ((((y v y) v u) v v) v w) = y.  [para(201(a,1),60(a,1,1,1,1,2)),rewrite(201(9),201(10),201(17))].

given #31 (A,wt=43): 12 (((x v (y v z)) ^ (y v z)) v (((u ^ ((y v z) v (y v z))) v (y v y)) ^ v)) ^ (((w v (y v z)) ^ (v6 v (y v z))) v v7) = y v z.  [para(10(a,1),2(a,1,1,2,1,2))].

given #32 (F,wt=23): 98 (((x v y) ^ y) v (z ^ y)) ^ ((((u v y) ^ (v v y)) v w) v v6) = y.  [para(2(a,1),60(a,1,1,1,1,2)),rewrite(2(14),2(15),2(23))].

given #33 (F,wt=23): 180 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ ((y v y) v v) = y.  [para(164(a,1),11(a,1,2,1))].

given #34 (T,wt=23): 199 (((x v x) v (x v x)) v x) ^ ((x v x) v y) = (x v x) v (x v x).  [para(179(a,1),86(a,1,1,2))].

given #35 (T,wt=21): 331 (((x v y) ^ y) v (y v y)) ^ (((y v y) v (y v y)) v z) = y.  [para(199(a,1),6(a,1,2,1))].

given #36 (A,wt=71): 13 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v (((v ^ ((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u))) v (w ^ (((y v y) v (z ^ y)) ^ u))) ^ v6)) ^ (y v v7) = ((y v y) v (z ^ y)) ^ u.  [para(11(a,1),2(a,1,2,1))].

given #37 (F,wt=23): 215 ((x v x) v (y ^ (x v x))) ^ (((x v x) v (x v x)) v z) = x v x.  [para(70(a,1),184(a,1,1,1))].

given #38 (F,wt=21): 362 ((x v x) v (x v x)) ^ (((x v x) v (x v x)) v y) = x v x.  [para(10(a,1),215(a,1,1,2))].

given #39 (T,wt=21): 364 ((x v x) v (y ^ x)) ^ (((x v x) v (x v x)) v z) = x v x.  [para(60(a,1),215(a,1,1,2))].

given #40 (T,wt=23): 256 (((x v y) ^ y) v (z ^ y)) ^ (((((y v y) v u) v v) v w) v v6) = y.  [para(231(a,1),60(a,1,1,1,1,2)),rewrite(231(10),231(11),231(19))].

given #41 (A,wt=81): 14 (((x v (((y v z) ^ (u v z)) v v)) ^ (((y v z) ^ (u v z)) v v)) v ((((((y v z) ^ (u v z)) v v) v (((y v z) ^ (u v z)) v v)) v z) ^ w)) ^ (((v6 v (((y v z) ^ (u v z)) v v)) ^ (v7 v (((y v z) ^ (u v z)) v v))) v v8) = ((y v z) ^ (u v z)) v v.  [para(2(a,1),11(a,1,1,2,1,2))].

given #42 (F,wt=25): 49 (((x v (y ^ z)) ^ (y ^ z)) v ((y ^ z) v (y ^ z))) ^ (z v u) = y ^ z.  [para(37(a,1),6(a,1,2,1))].

given #43 (F,wt=19): 421 (((x v y) ^ y) v (y v y)) ^ (((y v y) v z) v u) = y.  [para(179(a,1),49(a,1,1,1,1,2)),rewrite(179(8),179(9),179(9),179(15))].

given #44 (T,wt=21): 422 (((x v y) ^ y) v (y v y)) ^ ((((y v y) v z) v u) v v) = y.  [para(201(a,1),49(a,1,1,1,1,2)),rewrite(201(9),201(10),201(10),201(17))].

given #45 (T,wt=23): 417 (((x v y) ^ y) v (y v y)) ^ ((((z v y) ^ (u v y)) v v) v w) = y.  [para(2(a,1),49(a,1,1,1,1,2)),rewrite(2(14),2(15),2(15),2(23))].

given #46 (A,wt=81): 15 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v ((((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v)) v (w ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v6)) ^ (z v v7) = ((y ^ (z v z)) v (u ^ z)) ^ v.  [para(2(a,1),11(a,1,2,1))].

given #47 (F,wt=23): 423 (((x v y) ^ y) v (y v y)) ^ (((((y v y) v z) v u) v v) v w) = y.  [para(231(a,1),49(a,1,1,1,1,2)),rewrite(231(10),231(11),231(11),231(19))].

given #48 (F,wt=25): 80 ((x v x) v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (x v z) = x v x.  [para(70(a,1),29(a,1,1,1))].

given #49 (T,wt=25): 99 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ ((y v u) v v) = y v y.  [para(10(a,1),60(a,1,1,1,1,2)),rewrite(10(12),10(14),10(20))].

given #50 (T,wt=19): 454 ((x v x) v (y ^ (x v x))) ^ ((x v z) v u) = x v x.  [para(70(a,1),99(a,1,1,1))].

given #51 (A,wt=55): 16 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v ((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u))) ^ (y v v) = ((y v y) v (z ^ y)) ^ u.  [para(11(a,1),6(a,1,2,1))].

given #52 (F,wt=17): 486 ((x v x) v (x v x)) ^ ((x v y) v z) = x v x.  [para(10(a,1),454(a,1,1,2))].

given #53 (F,wt=17): 488 ((x v x) v (y ^ x)) ^ ((x v z) v u) = x v x.  [para(60(a,1),454(a,1,1,2))].

given #54 (T,wt=23): 447 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ ((y v z) v u) = y v y.  [para(10(a,1),99(a,1,1,2))].

given #55 (T,wt=23): 458 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ ((y v u) v v) = y v y.  [para(60(a,1),99(a,1,1,2))].

given #56 (A,wt=41): 18 (((x v (y v z)) ^ (y v z)) v ((((y v z) v (y v z)) v (y v y)) ^ u)) ^ (((v v (y v z)) ^ (w v (y v z))) v v6) = y v z.  [para(10(a,1),11(a,1,1,2,1,2))].

given #57 (F,wt=23): 493 ((x v x) v (((x v x) v (y ^ x)) ^ z)) ^ ((x v u) v v) = x v x.  [para(13(a,1),454(a,1,1,2))].

given #58 (F,wt=25): 111 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ ((z v v) v w) = y ^ z.  [para(60(a,1),60(a,1,1,1,1,2)),rewrite(60(11),60(13),60(19))].

given #59 (T,wt=25): 115 (((x v y) v (x v y)) v (x v x)) ^ ((x v y) v z) = (x v y) v (x v y).  [para(10(a,1),107(a,1,1,2))].

given #60 (T,wt=25): 122 (((x v y) v (x v y)) v (z ^ x)) ^ ((x v y) v u) = (x v y) v (x v y).  [para(60(a,1),107(a,1,1,2))].

given #61 (A,wt=69): 19 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v ((((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u)) v (v ^ (((y v y) v (z ^ y)) ^ u))) ^ w)) ^ (y v v6) = ((y v y) v (z ^ y)) ^ u.  [para(11(a,1),11(a,1,2,1))].

given #62 (F,wt=25): 178 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ ((y v y) v w) = y.  [para(164(a,1),2(a,1,2,1))].

given #63 (F,wt=23): 599 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ ((y v y) v w) = y.  [para(60(a,1),178(a,1,1,2,1,1))].

given #64 (T,wt=15): 617 (((x v y) ^ y) v y) ^ ((y v y) v z) = y.  [para(2(a,1),599(a,1,1,2))].

given #65 (T,wt=15): 645 (((x v y) ^ y) v (y v y)) ^ (y v z) = y.  [para(617(a,1),6(a,1,2,1))].

given #66 (A,wt=35): 20 (((x v y) ^ y) v (((((z ^ (y v y)) v (u ^ y)) ^ v) v (w ^ y)) ^ v6)) ^ (((v7 v y) ^ (v8 v y)) v v9) = y.  [para(2(a,1),4(a,1,1,1,1,2)),rewrite(2(19),2(25),2(29),2(30),2(34))].

given #67 (F,wt=11): 676 (x v x) v (x v x) = x v x.  [para(70(a,1),645(a,1,1,1)),rewrite(675(8))].

given #68 (F,wt=11): 785 (x v x) ^ (x v y) = x v x.  [back_rewrite(87),rewrite(676(3))].

given #69 (T,wt=13): 675 (x v (x v x)) ^ (x v y) = x v x.  [para(645(a,1),70(a,1,1,1))].

given #70 (T,wt=13): 682 (x v (y ^ x)) ^ (x v z) = x v x.  [para(645(a,1),106(a,1,1,1))].

given #71 (A,wt=89): 21 (((x v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) ^ ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) v u) ^ (((w v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) ^ (v6 v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u))))) v v7) = (y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)).  [para(2(a,1),4(a,1,1,2))].

given #72 (F,wt=13): 757 (x v x) ^ ((x v y) v z) = x v x.  [back_rewrite(486),rewrite(676(3))].

given #73 (F,wt=13): 878 (((x v y) ^ y) v y) ^ (y v y) = y.  [para(676(a,1),617(a,1,2))].

given #74 (T,wt=15): 650 (((x v y) ^ y) v (z ^ y)) ^ (y v u) = y.  [para(617(a,1),37(a,1,2,1))].

given #75 (T,wt=15): 673 (x v (y ^ (x v x))) ^ (x v z) = x v x.  [para(645(a,1),50(a,1,1,1))].

given #76 (A,wt=77): 22 (((x v (((y ^ (z v z)) v (u ^ z)) ^ (v v (u ^ z)))) ^ (((y ^ (z v z)) v (u ^ z)) ^ (v v (u ^ z)))) v (((u ^ z) v (w ^ (((y ^ (z v z)) v (u ^ z)) ^ (v v (u ^ z))))) ^ v6)) ^ (z v v7) = ((y ^ (z v z)) v (u ^ z)) ^ (v v (u ^ z)).  [para(2(a,1),4(a,1,2,1))].

given #77 (F,wt=15): 720 ((x v x) v x) ^ ((x v y) v z) = x v x.  [para(645(a,1),454(a,1,1,2))].

given #78 (F,wt=15): 723 (x v (x v x)) ^ ((x v y) v z) = x v x.  [para(645(a,1),447(a,1,1,1))].

given #79 (T,wt=15): 724 (x v (y ^ x)) ^ ((x v z) v u) = x v x.  [para(645(a,1),458(a,1,1,1))].

given #80 (T,wt=15): 739 (x v ((x v x) ^ y)) ^ (x v z) = x v x.  [back_rewrite(665),rewrite(676(3),676(3))].

given #81 (A,wt=81): 23 (((x v ((y v (z ^ ((u v y) ^ (v v y)))) ^ w)) ^ ((y v (z ^ ((u v y) ^ (v v y)))) ^ w)) v (((y v (z ^ ((u v y) ^ (v v y)))) ^ w) v ((y v (z ^ ((u v y) ^ (v v y)))) ^ w))) ^ (((u v y) ^ (v v y)) v v6) = (y v (z ^ ((u v y) ^ (v v y)))) ^ w.  [para(4(a,1),6(a,1,2,1))].

given #82 (F,wt=15): 766 (x v x) ^ (((x v x) v y) v z) = x v x.  [back_rewrite(427),rewrite(676(4),676(3),676(4))].

given #83 (F,wt=17): 654 (((x v y) ^ y) v (z ^ y)) ^ ((y v u) v v) = y.  [para(617(a,1),98(a,1,2,1,1))].

given #84 (T,wt=17): 657 (((x v y) ^ y) v (y v y)) ^ ((y v z) v u) = y.  [para(617(a,1),417(a,1,2,1,1))].

given #85 (T,wt=17): 712 (x v (x v x)) ^ (((x v x) v y) v z) = x v x.  [para(645(a,1),421(a,1,1,1)),rewrite(676(3),676(5))].

given #86 (A,wt=99): 24 (((x v ((y v (z ^ ((u v y) ^ (v v y)))) ^ w)) ^ ((y v (z ^ ((u v y) ^ (v v y)))) ^ w)) v (((((y v (z ^ ((u v y) ^ (v v y)))) ^ w) v ((y v (z ^ ((u v y) ^ (v v y)))) ^ w)) v (v6 ^ ((y v (z ^ ((u v y) ^ (v v y)))) ^ w))) ^ v7)) ^ (((u v y) ^ (v v y)) v v8) = (y v (z ^ ((u v y) ^ (v v y)))) ^ w.  [para(4(a,1),11(a,1,2,1))].

given #87 (F,wt=17): 718 (x v (y ^ (x v x))) ^ ((x v z) v u) = x v x.  [para(645(a,1),99(a,1,1,1))].

given #88 (F,wt=17): 765 (x v x) ^ ((((x v x) v y) v z) v u) = x v x.  [back_rewrite(428),rewrite(676(4),676(3),676(4))].

given #89 (T,wt=17): 787 ((x v x) v ((x v x) ^ y)) ^ (x v z) = x v x.  [back_rewrite(80),rewrite(676(4),676(4))].

given #90 (T,wt=19): 674 (((x v (y v y)) ^ (y v y)) v y) ^ (y v z) = y v y.  [para(645(a,1),50(a,1,1,2))].

given #91 (A,wt=69): 26 (((x v (((y v y) v (z ^ y)) ^ (u v (z ^ y)))) ^ (((y v y) v (z ^ y)) ^ (u v (z ^ y)))) v (((z ^ y) v (v ^ (((y v y) v (z ^ y)) ^ (u v (z ^ y))))) ^ w)) ^ (y v v6) = ((y v y) v (z ^ y)) ^ (u v (z ^ y)).  [para(11(a,1),4(a,1,2,1))].

given #92 (F,wt=19): 686 ((x v x) v ((x v (y ^ x)) ^ z)) ^ (x v u) = x v x.  [para(645(a,1),96(a,1,1,2,1,1))].

given #93 (F,wt=19): 693 (x v (y ^ (x v x))) ^ (((x v x) v z) v u) = x v x.  [para(645(a,1),201(a,1,1,1)),rewrite(676(6))].

given #94 (T,wt=17): 1217 (x v (y ^ x)) ^ (((x v x) v z) v u) = x v x.  [para(60(a,1),693(a,1,1,2))].

given #95 (T,wt=19): 713 (x v (x v x)) ^ ((((x v x) v y) v z) v u) = x v x.  [para(645(a,1),422(a,1,1,1)),rewrite(676(3),676(5))].

given #96 (A,wt=73): 27 (((x v ((y v z) ^ (u v z))) ^ ((y v z) ^ (u v z))) v ((((z v (v ^ ((y v z) ^ (u v z)))) ^ w) v (v6 ^ ((y v z) ^ (u v z)))) ^ v7)) ^ (((v8 v ((y v z) ^ (u v z))) ^ (v9 v ((y v z) ^ (u v z)))) v v10) = (y v z) ^ (u v z).  [para(4(a,1),4(a,1,1,1,1,2)),rewrite(4(36),4(46),4(53),4(57),4(64))].

given #97 (F,wt=19): 729 (((x v y) ^ y) v (z ^ y)) ^ (((y v u) v v) v w) = y.  [para(645(a,1),111(a,1,1,1,1,2)),rewrite(645(7),645(8),645(14))].

given #98 (F,wt=19): 763 (x v x) ^ (((((x v x) v y) v z) v u) v v) = x v x.  [back_rewrite(443),rewrite(676(4),676(3),676(4))].

given #99 (T,wt=19): 882 ((x v x) v ((y ^ x) v (y ^ x))) ^ (x v z) = x v x.  [para(785(a,1),147(a,1,1,2))].

given #100 (T,wt=19): 902 ((x v y) v x) ^ ((x v y) v z) = (x v y) v (x v y).  [para(645(a,1),682(a,1,1,2))].

given #101 (A,wt=95): 35 (((x v (((y v z) ^ (u v z)) v v)) ^ (((y v z) ^ (u v z)) v v)) v ((((((((y v z) ^ (u v z)) v v) v (((y v z) ^ (u v z)) v v)) v z) ^ w) v (v6 ^ (((y v z) ^ (u v z)) v v))) ^ v7)) ^ (((v8 v (((y v z) ^ (u v z)) v v)) ^ (v9 v (((y v z) ^ (u v z)) v v))) v v10) = ((y v z) ^ (u v z)) v v.  [para(2(a,1),25(a,1,1,2,1,1,1,2))].

given #102 (F,wt=19): 912 (((x v y) ^ y) v y) ^ (((z v y) ^ (u v y)) v v) = y.  [para(37(a,1),21(a,1,1,1,1,2)),rewrite(37(13),37(15),37(16),37(20))].

given #103 (F,wt=13): 1422 (((x v y) ^ y) v y) ^ (y v z) = y.  [para(617(a,1),912(a,1,2,1))].

given #104 (T,wt=19): 964 (x v (((x v x) v (y ^ x)) ^ z)) ^ (x v u) = x v x.  [para(13(a,1),673(a,1,1,2))].

given #105 (T,wt=19): 1011 ((x v x) v ((x v x) ^ y)) ^ ((x v x) v z) = x v x.  [para(676(a,1),739(a,1,1,2,1)),rewrite(676(10))].

given #106 (A,wt=95): 36 (((x v (((y v z) ^ (u v z)) v v)) ^ (((y v z) ^ (u v z)) v v)) v ((((((((y v z) ^ (u v z)) v v) v (((y v z) ^ (u v z)) v v)) v (w ^ (((y v z) ^ (u v z)) v v))) ^ v6) v z) ^ v7)) ^ (((v8 v (((y v z) ^ (u v z)) v v)) ^ (v9 v (((y v z) ^ (u v z)) v v))) v v10) = ((y v z) ^ (u v z)) v v.  [para(2(a,1),25(a,1,1,2,1,2))].

given #107 (F,wt=19): 1114 (((x v y) ^ y) v (y v y)) ^ (((y v z) v u) v v) = y.  [para(654(a,1),49(a,1,1,1,1,2)),rewrite(654(8),654(9),654(9),654(15))].

given #108 (F,wt=19): 1427 (((x v y) ^ y) v y) ^ (((y v z) v (y v z)) v u) = y.  [para(902(a,1),912(a,1,2,1))].

given #109 (T,wt=17): 1472 (((x v y) ^ y) v y) ^ ((y v z) v (y v z)) = y.  [para(676(a,1),1427(a,1,2))].

given #110 (T,wt=21): 646 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (y v v) = y.  [para(617(a,1),11(a,1,2,1))].

given #111 (A,wt=97): 38 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v ((((((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v)) v (w ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v6) v (v7 ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v8)) ^ (z v v9) = ((y ^ (z v z)) v (u ^ z)) ^ v.  [para(2(a,1),25(a,1,2,1))].

given #112 (F,wt=21): 695 (x v (y ^ (x v x))) ^ ((((x v x) v z) v u) v v) = x v x.  [para(645(a,1),231(a,1,1,1)),rewrite(676(6))].

given #113 (F,wt=19): 1513 (x v (y ^ x)) ^ ((((x v x) v z) v u) v v) = x v x.  [para(60(a,1),695(a,1,1,2))].

given #114 (T,wt=19): 1515 ((x v x) v x) ^ ((((x v x) v y) v z) v u) = x v x.  [para(180(a,1),695(a,1,1,2)),rewrite(676(5),676(10))].

given #115 (T,wt=21): 717 (x v (x v x)) ^ (((((x v x) v y) v z) v u) v v) = x v x.  [para(645(a,1),423(a,1,1,1)),rewrite(676(3),676(5))].

given #116 (A,wt=85): 39 (((x v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) ^ (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) v ((((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w) v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w))) ^ (y v v6) = ((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w.  [para(25(a,1),6(a,1,2,1))].

given #117 (F,wt=21): 719 (((x v (y v y)) ^ (y v y)) v y) ^ ((y v z) v u) = y v y.  [para(645(a,1),99(a,1,1,2))].

given #118 (F,wt=21): 733 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ ((y v y) v v) = y.  [para(645(a,1),178(a,1,1,2,1,1))].

given #119 (T,wt=19): 1598 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ (y v y) = y.  [para(676(a,1),733(a,1,2))].

given #120 (T,wt=21): 741 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (x v u) = x v x.  [back_rewrite(663),rewrite(676(3))].

given #121 (A,wt=49): 41 (((x v (y v z)) ^ (y v z)) v ((((((y v z) v (y v z)) v (y v y)) ^ u) v (v ^ (y v z))) ^ w)) ^ (((v6 v (y v z)) ^ (v7 v (y v z))) v v8) = y v z.  [para(10(a,1),25(a,1,1,2,1,1,1,2))].

given #122 (F,wt=17): 1641 (x v (((x v x) v x) ^ y)) ^ (x v z) = x v x.  [para(645(a,1),741(a,1,1,2,1,2))].

given #123 (F,wt=21): 790 (x v x) ^ (((y v (x v x)) ^ (z v (x v x))) v u) = x v x.  [back_rewrite(73),rewrite(676(4),676(3))].

given #124 (T,wt=17): 1696 (x v x) ^ (((x v y) v (x v y)) v z) = x v x.  [para(115(a,1),790(a,1,2,1))].

given #125 (T,wt=19): 1697 (x v x) ^ (((x v x) ^ (y v (x v x))) v z) = x v x.  [para(676(a,1),790(a,1,2,1,1))].

given #126 (A,wt=7): 1749 x ^ (x v y) = x.  [para(98(a,1),1697(a,1,2,1)),rewrite(1737(5),1737(7))].

given #127 (F,wt=5): 1786 x v x = x.  [back_rewrite(1446),rewrite(1737(5),1737(6),785(3),1737(6))].

given #128 (F,wt=5): 2299 x ^ x = x.  [back_rewrite(1784),rewrite(1814(2),1814(3),1814(2),1786(1),1814(3))].

given #129 (T,wt=7): 1814 (x v y) ^ y = y.  [back_rewrite(1737),rewrite(1786(5))].

given #130 (T,wt=9): 1834 x ^ ((x v y) v z) = x.  [back_rewrite(1696),rewrite(1786(1),1786(3),1786(4))].

given #131 (A,wt=29): 1789 ((x ^ (y v x)) v (((x ^ (y v x)) v x) ^ z)) ^ ((x ^ (y v x)) v u) = x ^ (y v x).  [back_rewrite(1783),rewrite(1786(1),1786(1),1786(3),1786(3),1786(5),1786(5),1786(7),1786(5),1786(8),1786(8),1786(12),1786(12),1786(14),1786(14),1786(16))].

given #132 (F,wt=9): 2156 (x ^ y) ^ y = x ^ y.  [back_rewrite(865),rewrite(1786(1),1786(3),1814(4),1786(2),1786(3),1786(4),1786(3),1786(2),1786(3))].

given #133 (F,wt=11): 1831 (x ^ y) ^ (y v z) = x ^ y.  [back_rewrite(1700),rewrite(1786(3),1786(2),1786(6))].

given #134 (T,wt=11): 1833 x ^ ((x ^ (y v x)) v z) = x.  [back_rewrite(1697),rewrite(1786(1),1786(1),1786(1),1786(5))].

given #135 (T,wt=9): 2327 x ^ (x ^ (y v x)) = x.  [para(1786(a,1),1833(a,1,2))].

given #136 (A,wt=31): 1792 (((x ^ (y v x)) v z) v x) ^ (((((x ^ (y v x)) v z) v u) v v) v w) = (x ^ (y v x)) v z.  [back_rewrite(1780),rewrite(1786(1),1786(1),1786(4),1786(5),1786(5),1786(8),1786(8),1786(11),1786(12),1786(12),1786(15),1786(15),1786(18))].

given #137 (F,wt=11): 1836 (x ^ y) ^ (x v z) = x ^ y.  [back_rewrite(1694),rewrite(1786(1),1786(1),1786(3),1786(3),1814(4),1786(2),1786(2),1786(3),1786(2),1786(4),1786(4))].

given #138 (F,wt=9): 2330 (x ^ y) ^ x = x ^ y.  [para(1786(a,1),1836(a,1,2))].

given #139 (T,wt=7): 2332 x ^ (y v x) = x.  [para(1814(a,1),2330(a,1,1)),rewrite(1814(4))].

given #140 (T,wt=7): 2335 x v (x ^ y) = x.  [back_rewrite(2326),rewrite(2332(2),2332(2),1786(1),2332(4))].

given #141 (A,wt=27): 1817 (((x v y) v z) v ((((x v y) v z) v x) ^ u)) ^ ((x v y) v z) = (x v y) v z.  [back_rewrite(1734),rewrite(1786(3),1786(6),1814(6),1786(5),1786(5),1786(10),1786(12),1786(12),1786(13))].

given #142 (F,wt=9): 2331 x ^ ((y v x) v z) = x.  [para(1814(a,1),1836(a,1,1)),rewrite(1814(5))].

given #143 (F,wt=9): 2334 (x v y) v x = x v y.  [back_rewrite(2328),rewrite(2332(2),2332(4))].

given #144 (T,wt=7): 2357 (x v y) ^ x = x.  [para(2334(a,1),1814(a,1,1))].

given #145 (T,wt=9): 2352 x ^ (x ^ y) = x ^ y.  [para(2335(a,1),1814(a,1,1))].

given #146 (A,wt=29): 1818 (((x v y) v z) v ((((x v y) v z) v x) ^ u)) ^ (((x v y) v z) v v) = (x v y) v z.  [back_rewrite(1733),rewrite(1786(3),1786(6),1814(6),1786(5),1786(5),1786(10),1786(12),1786(12),1786(14))].

given #147 (F,wt=9): 2353 (x v y) v y = x v y.  [para(1814(a,1),2335(a,1,2))].

given #148 (F,wt=11): 1943 x ^ (((x v y) v z) v u) = x.  [back_rewrite(1515),rewrite(1786(1),1786(1),1786(1),1786(5))].

given #149 (T,wt=11): 2195 (x v (y ^ x)) ^ (x v z) = x.  [back_rewrite(682),rewrite(1786(5))].

given #150 (T,wt=7): 2360 x v (y ^ x) = x.  [para(2195(a,1),2299(a,1)),flip(a)].

given #151 (A,wt=51): 1821 (((x v y) v z) v (((((u ^ ((x v y) v z)) v (v ^ ((x v y) v z))) ^ w) v x) ^ v6)) ^ (((v7 v ((x v y) v z)) ^ (v8 v ((x v y) v z))) v v9) = (x v y) v z.  [back_rewrite(1721),rewrite(1786(3),1786(6),1814(6),1786(5),1786(7),1786(7),1786(8),1786(11),1786(16),1786(19),1786(25))].

given #152 (F,wt=9): 2427 x ^ (y ^ x) = y ^ x.  [para(2360(a,1),1814(a,1,1))].

given #153 (F,wt=9): 2463 ((x v y) v z) ^ x = x.  [para(1834(a,1),2427(a,1,2)),rewrite(1834(6))].

given #154 (T,wt=9): 2466 ((x v y) v z) ^ y = y.  [para(2331(a,1),2427(a,1,2)),rewrite(2331(6))].

given #155 (T,wt=11): 2356 x ^ (((y v x) v z) v u) = x.  [para(2331(a,1),1831(a,1,1)),rewrite(2331(7))].

given #156 (A,wt=51): 1822 (((x v y) v z) v (((((u ^ ((x v y) v z)) v x) ^ v) v (w ^ ((x v y) v z))) ^ v6)) ^ (((v7 v ((x v y) v z)) ^ (v8 v ((x v y) v z))) v v9) = (x v y) v z.  [back_rewrite(1720),rewrite(1786(3),1786(6),1814(6),1786(5),1786(7),1786(7),1786(6),1786(10),1786(16),1786(19),1786(25))].

given #157 (F,wt=11): 2429 (x v y) v (z ^ x) = x v y.  [para(1831(a,1),2360(a,1,2))].

given #158 (F,wt=11): 2430 (x v y) v (x ^ z) = x v y.  [para(1836(a,1),2360(a,1,2))].

given #159 (T,wt=11): 2464 (x v y) ^ (z ^ x) = z ^ x.  [para(1831(a,1),2427(a,1,2)),rewrite(1831(6))].

given #160 (T,wt=11): 2465 (x v y) ^ (x ^ z) = x ^ z.  [para(1836(a,1),2427(a,1,2)),rewrite(1836(6))].

given #161 (A,wt=31): 1823 (((x v y) v z) v (((u ^ ((x v y) v z)) v x) ^ v)) ^ (((x v y) v z) v w) = (x v y) v z.  [back_rewrite(1719),rewrite(1786(3),1786(6),1814(6),1786(5),1786(6),1786(11),1786(13),1786(13),1786(15))].

given #162 (F,wt=11): 2467 (((x v y) v z) v u) ^ x = x.  [para(1943(a,1),2427(a,1,2)),rewrite(1943(8))].

given #163 (F,wt=11): 2470 (((x v y) v z) v u) ^ y = y.  [para(2356(a,1),2427(a,1,2)),rewrite(2356(8))].

given #164 (T,wt=13): 1832 x ^ (((y v x) ^ (z v x)) v u) = x.  [back_rewrite(1699),rewrite(1786(1),1786(1),1786(2),1814(2),1786(2),1786(3),1814(3),1786(6))].

given #165 (T,wt=11): 2522 x ^ ((y v x) ^ (z v x)) = x.  [para(1786(a,1),1832(a,1,2))].

given #166 (A,wt=31): 1824 (((x v y) v z) v ((x v (u ^ ((x v y) v z))) ^ v)) ^ (((x v y) v z) v w) = (x v y) v z.  [back_rewrite(1718),rewrite(1786(3),1786(6),1814(6),1786(3),1786(5),1786(11),1786(13),1786(13),1786(15))].

given #167 (F,wt=11): 2540 x ^ ((x v y) ^ (z v x)) = x.  [para(2334(a,1),2522(a,1,2,1))].

given #168 (F,wt=11): 2541 x ^ ((y v x) ^ (x v z)) = x.  [para(2334(a,1),2522(a,1,2,2))].

given #169 (T,wt=11): 2545 ((x v y) ^ (z v y)) ^ y = y.  [para(2522(a,1),2427(a,1,2)),rewrite(2522(8))].

given #170 (T,wt=11): 2562 x ^ ((x v y) ^ (x v z)) = x.  [para(2334(a,1),2540(a,1,2,2))].

given #171 (A,wt=23): 1825 ((x v y) v ((x v (z ^ (x v y))) ^ u)) ^ ((x v y) v v) = x v y.  [back_rewrite(1716),rewrite(1786(3),1786(5),1814(4),1786(2),1786(4),1786(9),1786(12))].

given #172 (F,wt=29): 2578 c1 v (c2 ^ (c1 ^ c3)) != c1 | c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 # answer(McKenzie).  [back_rewrite(3),rewrite(2573(38)),xx(d)].

given #173 (F,wt=11): 2565 ((x v y) ^ (z v x)) ^ x = x.  [para(2540(a,1),2427(a,1,2)),rewrite(2540(8))].

given #174 (T,wt=11): 2573 ((x v y) ^ (y v z)) ^ y = y.  [para(2541(a,1),2427(a,1,2)),rewrite(2541(8))].

given #175 (T,wt=11): 2589 ((x v y) ^ (x v z)) ^ x = x.  [para(2562(a,1),2427(a,1,2)),rewrite(2562(8))].

given #176 (A,wt=29): 1829 ((x v y) v ((x v (x v y)) ^ z)) ^ (((u v (x v y)) ^ (v v (x v y))) v w) = x v y.  [back_rewrite(1708),rewrite(1786(3),1786(5),1814(4),1786(2),1786(4),1786(8),1786(10),1786(15))].

given #177 (F,wt=13): 1842 (x ^ y) ^ ((x v z) v u) = x ^ y.  [back_rewrite(1687),rewrite(1786(1),1786(1),1786(3),1786(3),1814(4),1786(2),1786(2),1786(3),1786(3),1786(4),1786(3),1786(2),1786(5),1786(5))].

given #178 (F,wt=13): 1981 (x ^ y) ^ ((y v z) v u) = x ^ y.  [back_rewrite(1420),rewrite(1814(4),1786(3),1786(4))].

given #179 (T,wt=13): 2045 x ^ ((((x v y) v z) v u) v v) = x.  [back_rewrite(1292),rewrite(1814(2),1786(1),1786(1))].

given #180 (T,wt=13): 2428 ((x v y) v z) v x = (x v y) v z.  [para(1834(a,1),2360(a,1,2))].

given #181 (A,wt=29): 1839 (x v (((((x ^ y) v (z ^ x)) ^ u) v (v ^ x)) ^ w)) ^ (((v6 v x) ^ (v7 v x)) v v8) = x.  [back_rewrite(1691),rewrite(1786(1),1786(2),1814(2),1786(1),1786(1),1786(2),1786(5),1786(9),1786(10),1786(14))].

given #182 (F,wt=13): 2431 ((x v y) v z) v y = (x v y) v z.  [para(2331(a,1),2360(a,1,2))].

given #183 (F,wt=13): 2468 x ^ ((((y v x) v z) v u) v v) = x.  [para(2356(a,1),1831(a,1,1)),rewrite(2356(9))].

given #184 (T,wt=13): 2503 ((x v y) v z) ^ (u ^ x) = u ^ x.  [para(2429(a,1),2466(a,1,1,1))].

given #185 (T,wt=13): 2505 ((x v y) v z) ^ (x ^ u) = x ^ u.  [para(2430(a,1),2466(a,1,1,1))].

given #186 (A,wt=33): 1841 ((x ^ y) v (((((z ^ (x ^ y)) v (u ^ (x ^ y))) ^ v) v (w ^ (x ^ y))) ^ v6)) ^ (x v v7) = x ^ y.  [back_rewrite(1688),rewrite(1786(1),1786(1),1786(3),1786(3),1814(4),1786(2),1786(2),1786(3),1786(3),1786(4),1786(4),1786(4),1786(8),1786(8),1786(13),1786(15),1786(15))].

given #187 (F,wt=13): 2506 ((((x v y) v z) v u) v v) ^ x = x.  [para(1943(a,1),2464(a,1,2)),rewrite(1943(9))].

given #188 (F,wt=13): 2507 ((((x v y) v z) v u) v v) ^ y = y.  [para(2356(a,1),2464(a,1,2)),rewrite(2356(9))].

given #189 (T,wt=13): 2525 x ^ (((x v y) ^ (z v x)) v u) = x.  [para(2334(a,1),1832(a,1,2,1,1))].

given #190 (T,wt=13): 2526 x ^ (((y v x) ^ (x v z)) v u) = x.  [para(2334(a,1),1832(a,1,2,1,2))].

given #191 (A,wt=33): 1845 ((x v y) v (((z ^ (x v y)) v (x ^ u)) ^ v)) ^ (((w v (x v y)) ^ (v6 v (x v y))) v v7) = x v y.  [back_rewrite(1684),rewrite(1786(1),1786(3),1814(4),1786(2),1786(3),1786(4),1786(4),1786(4),1786(8),1786(10),1786(15))].

given #192 (F,wt=13): 2530 (((x v y) ^ (z v y)) v u) ^ y = y.  [para(1832(a,1),2427(a,1,2)),rewrite(1832(10))].

given #193 (F,wt=13): 2569 (((x v y) ^ (z v x)) v u) ^ x = x.  [para(2540(a,1),2464(a,1,2)),rewrite(2540(9))].

given #194 (T,wt=13): 2577 (((x v y) ^ (y v z)) v u) ^ y = y.  [para(2541(a,1),2464(a,1,2)),rewrite(2541(9))].

given #195 (T,wt=13): 2587 x ^ (((x v y) ^ (x v z)) v u) = x.  [para(2562(a,1),1831(a,1,1)),rewrite(2562(9))].

given #196 (A,wt=21): 1848 (x v (((x ^ y) v x) ^ z)) ^ (((u v x) ^ (v v x)) v w) = x.  [back_rewrite(1681),rewrite(1786(1),1786(2),1814(2),1786(1),1786(5),1786(6),1786(10))].

given #197 (F,wt=11): 2834 x v (((x ^ y) v x) ^ z) = x.  [para(1848(a,1),2332(a,1)),flip(a)].

given #198 (F,wt=20): 2903 c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 # answer(McKenzie).  [back_rewrite(2578),rewrite(2867(7)),xx(a)].

given #199 (T,wt=9): 2859 x v ((x ^ y) v x) = x.  [para(1749(a,1),2834(a,1,2))].

given #200 (T,wt=7): 2904 (x ^ y) v x = x.  [para(2859(a,1),1814(a,1,1)),rewrite(2332(3)),flip(a)].

given #201 (A,wt=31): 1850 ((x v y) v ((((x v y) ^ z) v x) ^ u)) ^ (((v v (x v y)) ^ (w v (x v y))) v v6) = x v y.  [back_rewrite(1679),rewrite(1786(3),1786(5),1814(4),1786(4),1786(9),1786(11),1786(16))].

given #202 (F,wt=7): 2929 (x ^ y) v y = y.  [para(2427(a,1),2904(a,1,1))].

given #203 (F,wt=9): 2867 x v (y ^ (x ^ z)) = x.  [para(2464(a,1),2834(a,1,2))].

given #204 (T,wt=9): 2869 x v ((x ^ y) ^ z) = x.  [para(2465(a,1),2834(a,1,2))].

given #205 (T,wt=9): 2925 x v (y v x) = y v x.  [para(1814(a,1),2904(a,1,1))].

given #206 (A,wt=25): 1856 ((x ^ y) v ((((x ^ y) ^ z) v (u ^ (x ^ y))) ^ v)) ^ (y v w) = x ^ y.  [back_rewrite(1672),rewrite(1786(3),1786(5),1814(4),1786(4),1786(6),1786(9),1786(13))].

given #207 (F,wt=11): 3095 ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 # answer(McKenzie).  [back_rewrite(2903),rewrite(3048(7)),xx(a)].

given #208 (F,wt=9): 2928 x v (x v y) = x v y.  [para(2357(a,1),2904(a,1,1))].

given #209 (T,wt=9): 2967 x v (y ^ (z ^ x)) = x.  [para(2929(a,1),2429(a,1,1)),rewrite(2929(5))].

given #210 (T,wt=9): 2968 x v ((y ^ x) ^ z) = x.  [para(2929(a,1),2430(a,1,1)),rewrite(2929(5))].

given #211 (A,wt=17): 1861 (x v (((x ^ y) v (z ^ x)) ^ u)) ^ (x v v) = x.  [back_rewrite(1664),rewrite(1786(1),1786(2),1814(2),1786(1),1786(2),1786(6),1786(7),1814(7),1786(8))].

given #212 (F,wt=9): 3048 x ^ (y v (x v z)) = x.  [para(2925(a,1),1834(a,1,2))].

given #213 (F,wt=9): 3051 x ^ (y v (z v x)) = x.  [para(2925(a,1),2331(a,1,2))].

given #214 (T,wt=9): 3054 (x v (y v z)) ^ y = y.  [para(2925(a,1),2463(a,1,1))].

given #215 (T,wt=9): 3055 (x v (y v z)) ^ z = z.  [para(2925(a,1),2466(a,1,1))].

given #216 (A,wt=49): 1875 (((x v y) ^ (z v y)) v ((((x v y) ^ (z v y)) v ((y v (u ^ ((x v y) ^ (z v y)))) ^ v)) ^ w)) ^ (((x v y) ^ (z v y)) v v6) = (x v y) ^ (z v y).  [back_rewrite(1642),rewrite(1786(10),1786(27))].

given #217 (F,wt=9): 3093 (x ^ (y ^ z)) v y = y.  [para(2867(a,1),2925(a,1,2)),rewrite(2867(6))].

given #218 (F,wt=9): 3094 ((x ^ y) ^ z) v x = x.  [para(2869(a,1),2925(a,1,2)),rewrite(2869(6))].

given #219 (T,wt=9): 3145 (x ^ (y ^ z)) v z = z.  [para(2967(a,1),2925(a,1,2)),rewrite(2967(6))].

given #220 (T,wt=9): 3167 ((x ^ y) ^ z) v y = y.  [para(2968(a,1),2925(a,1,2)),rewrite(2968(6))].

given #221 (A,wt=21): 1879 (x v ((x v (((y ^ x) v (z ^ x)) ^ u)) ^ v)) ^ (x v w) = x.  [back_rewrite(1638),rewrite(1786(1),1786(1),1786(10))].

given #222 (F,wt=11): 2933 (x ^ y) v (y v z) = y v z.  [para(2464(a,1),2904(a,1,1))].

given #223 (F,wt=11): 2935 (x ^ y) v (x v z) = x v z.  [para(2465(a,1),2904(a,1,1))].

given #224 (T,wt=11): 2976 (x v y) v (z ^ y) = x v y.  [para(1814(a,1),2867(a,1,2,2))].

given #225 (T,wt=11): 3012 (x v y) v (y ^ z) = x v y.  [para(1814(a,1),2869(a,1,2,1))].

given #226 (A,wt=23): 1883 (((x ^ y) v (z ^ x)) ^ u) ^ (x v v) = ((x ^ y) v (z ^ x)) ^ u.  [back_rewrite(1634),rewrite(1786(1),1786(1),1786(2),1786(6),1786(6),1786(7),1814(10),1786(5),1786(5),1786(6),1786(9),1786(9),1786(10),1786(13),1786(9),1786(5),1786(7),1786(7),1786(8))].

given #227 (F,wt=11): 3049 (x ^ y) ^ (z v y) = x ^ y.  [para(2925(a,1),1831(a,1,2))].

given #228 (F,wt=11): 3050 (x ^ y) ^ (z v x) = x ^ y.  [para(2925(a,1),1836(a,1,2))].

given #229 (T,wt=11): 3052 x ^ ((y v (x v z)) v u) = x.  [para(2925(a,1),1943(a,1,2,1))].

given #230 (T,wt=11): 3053 x ^ (y v ((x v z) v u)) = x.  [para(2925(a,1),1943(a,1,2))].

given #231 (A,wt=57): 1900 ((((x v y) ^ (z v y)) v u) v (((((x v y) ^ (z v y)) v u) v ((y v (v ^ ((x v y) ^ (z v y)))) ^ w)) ^ v6)) ^ ((((x v y) ^ (z v y)) v u) v v7) = ((x v y) ^ (z v y)) v u.  [back_rewrite(1601),rewrite(1814(10),1786(26))].

given #232 (F,wt=11): 3056 x ^ ((y v (z v x)) v u) = x.  [para(2925(a,1),2356(a,1,2,1))].

given #233 (F,wt=11): 3057 x ^ (y v ((z v x) v u)) = x.  [para(2925(a,1),2356(a,1,2))].

given #234 (T,wt=11): 3058 (x v y) ^ (z ^ y) = z ^ y.  [para(2925(a,1),2464(a,1,1))].

given #235 (T,wt=11): 3059 (x v y) ^ (y ^ z) = y ^ z.  [para(2925(a,1),2465(a,1,1))].

given #236 (A,wt=29): 1911 ((x v y) v (((x v y) v (((z ^ x) v (u ^ x)) ^ v)) ^ w)) ^ ((x v y) v v6) = x v y.  [back_rewrite(1585),rewrite(1814(4),1786(3),1786(12))].

given #237 (F,wt=11): 3060 ((x v (y v z)) v u) ^ y = y.  [para(2925(a,1),2467(a,1,1,1))].

given #238 (F,wt=11): 3061 (x v ((y v z) v u)) ^ y = y.  [para(2925(a,1),2467(a,1,1))].

given #239 (T,wt=11): 3062 ((x v (y v z)) v u) ^ z = z.  [para(2925(a,1),2470(a,1,1,1))].

given #240 (T,wt=11): 3063 (x v ((y v z) v u)) ^ z = z.  [para(2925(a,1),2470(a,1,1))].

given #241 (A,wt=49): 1935 ((((x v y) ^ (z v y)) v u) v ((y v (v ^ ((x v y) ^ (z v y)))) ^ w)) ^ ((((((x v y) ^ (z v y)) v u) v v6) v v7) v v8) = ((x v y) ^ (z v y)) v u.  [back_rewrite(1533),rewrite(1786(20),1786(28))].

given #242 (F,wt=11): 3262 (x ^ y) v (z v y) = z v y.  [para(1814(a,1),3093(a,1,1,2))].

given #243 (F,wt=11): 3266 x v (y ^ (z ^ (x ^ u))) = x.  [para(3093(a,1),2429(a,1,1)),rewrite(3093(7))].

given #244 (T,wt=11): 3267 x v ((y ^ (x ^ z)) ^ u) = x.  [para(3093(a,1),2430(a,1,1)),rewrite(3093(7))].

given #245 (T,wt=11): 3291 (x ^ y) v (z v x) = z v x.  [para(1814(a,1),3094(a,1,1,1))].

given #246 (A,wt=27): 1939 ((x v y) v (((z ^ x) v (u ^ x)) ^ v)) ^ ((((x v y) v w) v v6) v v7) = x v y.  [back_rewrite(1527),rewrite(1786(2),1786(9),1786(14))].

given #247 (F,wt=11): 3295 x v (y ^ ((x ^ z) ^ u)) = x.  [para(3094(a,1),2429(a,1,1)),rewrite(3094(7))].

given #248 (F,wt=11): 3296 x v (((x ^ y) ^ z) ^ u) = x.  [para(3094(a,1),2430(a,1,1)),rewrite(3094(7))].

given #249 (T,wt=11): 3322 x v (y ^ (z ^ (u ^ x))) = x.  [para(3145(a,1),2429(a,1,1)),rewrite(3145(7))].

given #250 (T,wt=11): 3323 x v ((y ^ (z ^ x)) ^ u) = x.  [para(3145(a,1),2430(a,1,1)),rewrite(3145(7))].

given #251 (A,wt=43): 1940 (((x v y) ^ (z v y)) v ((y v (u ^ ((x v y) ^ (z v y)))) ^ v)) ^ (((((x v y) ^ (z v y)) v w) v v6) v v7) = (x v y) ^ (z v y).  [back_rewrite(1520),rewrite(1786(17),1786(24))].

given #252 (F,wt=11): 3333 x v (y ^ ((z ^ x) ^ u)) = x.  [para(3167(a,1),2429(a,1,1)),rewrite(3167(7))].

given #253 (F,wt=11): 3334 x v (((y ^ x) ^ z) ^ u) = x.  [para(3167(a,1),2430(a,1,1)),rewrite(3167(7))].

given #254 (T,wt=11): 3395 (x ^ (y ^ (z ^ u))) v z = z.  [para(3093(a,1),2933(a,1,2)),rewrite(3093(7))].

given #255 (T,wt=11): 3396 (x ^ ((y ^ z) ^ u)) v y = y.  [para(3094(a,1),2933(a,1,2)),rewrite(3094(7))].

given #256 (A,wt=21): 1946 (x v (((y ^ x) v (z ^ x)) ^ u)) ^ (((x v v) v w) v v6) = x.  [back_rewrite(1512),rewrite(1786(1),1786(6),1786(10))].

given #257 (F,wt=11): 3397 (x ^ (y ^ (z ^ u))) v u = u.  [para(3145(a,1),2933(a,1,2)),rewrite(3145(7))].

given #258 (F,wt=11): 3398 (x ^ ((y ^ z) ^ u)) v z = z.  [para(3167(a,1),2933(a,1,2)),rewrite(3167(7))].

given #259 (T,wt=11): 3399 ((x ^ (y ^ z)) ^ u) v y = y.  [para(3093(a,1),2935(a,1,2)),rewrite(3093(7))].

given #260 (T,wt=11): 3400 (((x ^ y) ^ z) ^ u) v x = x.  [para(3094(a,1),2935(a,1,2)),rewrite(3094(7))].

given #261 (A,wt=39): 1954 ((x v y) v (((((z ^ (x v y)) v (u ^ (x v y))) ^ v) v x) ^ w)) ^ (((v6 v (x v y)) ^ (v7 v (x v y))) v v8) = x v y.  [back_rewrite(1487),rewrite(1786(3),1786(5),1814(4),1786(4),1786(6),1786(13),1786(15),1786(20))].

given #262 (F,wt=11): 3401 ((x ^ (y ^ z)) ^ u) v z = z.  [para(3145(a,1),2935(a,1,2)),rewrite(3145(7))].

given #263 (F,wt=11): 3402 (((x ^ y) ^ z) ^ u) v y = y.  [para(3167(a,1),2935(a,1,2)),rewrite(3167(7))].

given #264 (T,wt=11): 3538 x ^ (y v (z v (x v u))) = x.  [para(3048(a,1),3049(a,1,1)),rewrite(3048(7))].

given #265 (T,wt=11): 3539 x ^ (y v (z v (u v x))) = x.  [para(3051(a,1),3049(a,1,1)),rewrite(3051(7))].

given #266 (A,wt=39): 1955 ((x v y) v (((((z ^ (x v y)) v x) ^ u) v (v ^ (x v y))) ^ w)) ^ (((v6 v (x v y)) ^ (v7 v (x v y))) v v8) = x v y.  [back_rewrite(1486),rewrite(1786(3),1786(5),1814(4),1786(4),1786(8),1786(13),1786(15),1786(20))].

given #267 (F,wt=11): 3668 (x v (y v (z v u))) ^ z = z.  [para(3048(a,1),3058(a,1,2)),rewrite(3048(7))].

given #268 (F,wt=11): 3669 (x v (y v (z v u))) ^ u = u.  [para(3051(a,1),3058(a,1,2)),rewrite(3051(7))].

given #269 (T,wt=13): 2591 (((x v y) ^ (x v z)) v u) ^ x = x.  [para(2562(a,1),2464(a,1,2)),rewrite(2562(9))].

given #270 (T,wt=13): 2627 x ^ (((x v y) v z) ^ (u v x)) = x.  [para(2428(a,1),2522(a,1,2,1))].

given #271 (A,wt=23): 1956 ((x v y) v (((z ^ (x v y)) v x) ^ u)) ^ ((x v y) v v) = x v y.  [back_rewrite(1485),rewrite(1786(3),1786(5),1814(4),1786(4),1786(9),1786(12))].

given #272 (F,wt=13): 2628 x ^ ((y v x) ^ ((x v z) v u)) = x.  [para(2428(a,1),2522(a,1,2,2))].

given #273 (F,wt=13): 2629 x ^ ((x v y) ^ ((x v z) v u)) = x.  [para(2428(a,1),2540(a,1,2,2))].

given #274 (T,wt=13): 2630 x ^ (((x v y) v z) ^ (x v u)) = x.  [para(2428(a,1),2541(a,1,2,1))].

given #275 (T,wt=13): 2631 (((x v y) v z) ^ (u v x)) ^ x = x.  [para(2428(a,1),2545(a,1,1,1))].

given #276 (A,wt=25): 1962 (((x ^ (y v z)) v y) ^ u) ^ ((y v z) v v) = ((x ^ (y v z)) v y) ^ u.  [back_rewrite(1478),rewrite(1786(3),1786(8),1814(10),1786(7),1786(11),1786(13),1786(9),1786(7),1786(10))].

given #277 (F,wt=13): 2632 ((x v y) ^ ((y v z) v u)) ^ y = y.  [para(2428(a,1),2545(a,1,1,2))].

given #278 (F,wt=13): 2633 ((x v y) ^ ((x v z) v u)) ^ x = x.  [para(2428(a,1),2565(a,1,1,2))].

given #279 (T,wt=13): 2634 (((x v y) v z) ^ (x v u)) ^ x = x.  [para(2428(a,1),2573(a,1,1,1))].

given #280 (T,wt=13): 2692 x ^ (((y v x) v z) ^ (u v x)) = x.  [para(2431(a,1),2522(a,1,2,1))].

given #281 (A,wt=35): 1980 (((((x ^ y) v (z ^ y)) ^ u) v (v ^ y)) ^ w) ^ (y v v6) = ((((x ^ y) v (z ^ y)) ^ u) v (v ^ y)) ^ w.  [back_rewrite(1423),rewrite(1786(1),1786(9),1814(16),1786(8),1786(15),1786(10))].

given #282 (F,wt=13): 2693 x ^ ((y v x) ^ ((z v x) v u)) = x.  [para(2431(a,1),2522(a,1,2,2))].

given #283 (F,wt=13): 2694 x ^ ((x v y) ^ ((z v x) v u)) = x.  [para(2431(a,1),2540(a,1,2,2))].

given #284 (T,wt=13): 2695 x ^ (((y v x) v z) ^ (x v u)) = x.  [para(2431(a,1),2541(a,1,2,1))].

given #285 (T,wt=13): 2696 (((x v y) v z) ^ (u v y)) ^ y = y.  [para(2431(a,1),2545(a,1,1,1))].

given #286 (A,wt=23): 1982 (((x ^ y) v (z ^ y)) ^ u) ^ (y v v) = ((x ^ y) v (z ^ y)) ^ u.  [back_rewrite(1417),rewrite(1814(10),1786(9),1786(5))].

given #287 (F,wt=13): 2697 ((x v y) ^ ((z v y) v u)) ^ y = y.  [para(2431(a,1),2545(a,1,1,2))].

given #288 (F,wt=13): 2698 ((x v y) ^ ((z v x) v u)) ^ x = x.  [para(2431(a,1),2565(a,1,1,2))].

given #289 (T,wt=13): 2699 (((x v y) v z) ^ (y v u)) ^ y = y.  [para(2431(a,1),2573(a,1,1,1))].

given #290 (T,wt=13): 2926 (x ^ (y ^ z)) ^ y = x ^ (y ^ z).  [para(2904(a,1),1831(a,1,2))].

given #291 (A,wt=53): 1999 (((x v y) ^ (z v y)) v ((((y v (u ^ ((x v y) ^ (z v y)))) ^ v) v (w ^ ((x v y) ^ (z v y)))) ^ v6)) ^ ((((x v y) ^ (z v y)) v v7) v v8) = (x v y) ^ (z v y).  [back_rewrite(1385),rewrite(1814(8),1786(25))].

given #292 (F,wt=13): 2927 ((x ^ y) ^ z) ^ x = (x ^ y) ^ z.  [para(2904(a,1),1836(a,1,2))].

given #293 (F,wt=13): 2930 x v ((x v y) v z) = (x v y) v z.  [para(2463(a,1),2904(a,1,1))].

given #294 (T,wt=13): 2931 x v ((y v x) v z) = (y v x) v z.  [para(2466(a,1),2904(a,1,1))].

given #295 (T,wt=13): 2932 x ^ (y ^ (x ^ z)) = y ^ (x ^ z).  [para(2904(a,1),2464(a,1,1))].

given #296 (A,wt=25): 2001 (x v (((((y ^ x) v (z ^ x)) ^ u) v (v ^ x)) ^ w)) ^ ((x v v6) v v7) = x.  [back_rewrite(1382),rewrite(1814(2),1786(1),1786(11))].

given #297 (F,wt=13): 2934 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z.  [para(2904(a,1),2465(a,1,1))].

given #298 (F,wt=13): 2965 (x ^ (y ^ z)) ^ z = x ^ (y ^ z).  [para(2929(a,1),1831(a,1,2))].

given #299 (T,wt=13): 2966 ((x ^ y) ^ z) ^ y = (x ^ y) ^ z.  [para(2929(a,1),1836(a,1,2))].

given #300 (T,wt=13): 2969 x ^ (y ^ (z ^ x)) = y ^ (z ^ x).  [para(2929(a,1),2464(a,1,1))].

given #301 (A,wt=49): 2004 ((((x v y) ^ (z v y)) v u) v (((v ^ (((x v y) ^ (z v y)) v u)) v y) ^ w)) ^ (((((x v y) ^ (z v y)) v u) v v6) v v7) = ((x v y) ^ (z v y)) v u.  [back_rewrite(1378),rewrite(1814(10),1786(13),1786(23))].

given #302 (F,wt=13): 2970 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z.  [para(2929(a,1),2465(a,1,1))].

given #303 (F,wt=13): 2979 (x v y) v (z ^ (u ^ x)) = x v y.  [para(2464(a,1),2867(a,1,2,2))].

given #304 (T,wt=13): 2980 (x v y) v (z ^ (x ^ u)) = x v y.  [para(2465(a,1),2867(a,1,2,2))].

given #305 (T,wt=13): 3015 (x v y) v ((z ^ x) ^ u) = x v y.  [para(2464(a,1),2869(a,1,2,1))].

given #306 (A,wt=35): 2016 (((x v y) ^ (z v y)) v (((u ^ ((x v y) ^ (z v y))) v y) ^ v)) ^ ((z v y) v w) = (x v y) ^ (z v y).  [back_rewrite(1357),rewrite(1786(7),1786(11),1814(8),1786(10),1786(13),1786(20))].

given #307 (F,wt=13): 3016 (x v y) v ((x ^ z) ^ u) = x v y.  [para(2465(a,1),2869(a,1,2,1))].

given #308 (F,wt=13): 3064 x ^ (y v ((z v x) ^ (u v x))) = x.  [para(2925(a,1),1832(a,1,2))].

given #309 (T,wt=13): 3065 (x ^ y) ^ ((z v x) v u) = x ^ y.  [para(2925(a,1),1842(a,1,2,1))].

given #310 (T,wt=13): 3066 (x ^ y) ^ (z v (x v u)) = x ^ y.  [para(2925(a,1),1842(a,1,2))].

given #311 (A,wt=33): 2017 ((x v y) v (((z ^ (x v y)) v (u ^ x)) ^ v)) ^ (((w v (x v y)) ^ (v6 v (x v y))) v v7) = x v y.  [back_rewrite(1356),rewrite(1786(1),1786(3),1814(4),1786(2),1786(3),1786(4),1786(6),1786(8),1786(10),1786(15))].

given #312 (F,wt=13): 3067 (x ^ y) ^ ((z v y) v u) = x ^ y.  [para(2925(a,1),1981(a,1,2,1))].

given #313 (F,wt=13): 3068 (x ^ y) ^ (z v (y v u)) = x ^ y.  [para(2925(a,1),1981(a,1,2))].

given #314 (T,wt=13): 3069 x ^ (((y v (x v z)) v u) v v) = x.  [para(2925(a,1),2045(a,1,2,1,1))].

given #315 (T,wt=13): 3070 x ^ ((y v ((x v z) v u)) v v) = x.  [para(2925(a,1),2045(a,1,2,1))].

given #316 (A,wt=63): 2024 ((((x v y) v z) v u) v ((((x v (v ^ (((x v y) v z) v u))) ^ w) v (v6 ^ (((x v y) v z) v u))) ^ v7)) ^ (((v8 v (((x v y) v z) v u)) ^ (v9 v (((x v y) v z) v u))) v v10) = ((x v y) v z) v u.  [back_rewrite(1341),rewrite(1786(1),1786(5),1814(8),1786(4),1786(4),1786(10),1786(17),1786(21),1786(28))].

given #317 (F,wt=13): 3071 x ^ (y v (((x v z) v u) v v)) = x.  [para(2925(a,1),2045(a,1,2))].

given #318 (F,wt=13): 3072 (x v (y v z)) v y = x v (y v z).  [para(2925(a,1),2428(a,1,1)),rewrite(2925(7))].

given #319 (T,wt=13): 3073 (x v (y v z)) v z = x v (y v z).  [para(2925(a,1),2431(a,1,1)),rewrite(2925(7))].

given #320 (T,wt=13): 3074 x ^ (((y v (z v x)) v u) v v) = x.  [para(2925(a,1),2468(a,1,2,1,1))].

given #321 (A,wt=47): 2025 (((((x v y) v z) v u) v v) v (((w ^ ((((x v y) v z) v u) v v)) v x) ^ v6)) ^ (((((x v y) v z) v u) v v) v v7) = (((x v y) v z) v u) v v.  [back_rewrite(1340),rewrite(1786(1),1786(6),1814(10),1786(5),1786(10),1786(13),1786(17),1786(21),1786(19))].

given #322 (F,wt=13): 3075 x ^ ((y v ((z v x) v u)) v v) = x.  [para(2925(a,1),2468(a,1,2,1))].

given #323 (F,wt=13): 3076 x ^ (y v (((z v x) v u) v v)) = x.  [para(2925(a,1),2468(a,1,2))].

given #324 (T,wt=13): 3077 ((x v y) v z) ^ (u ^ y) = u ^ y.  [para(2925(a,1),2503(a,1,1,1))].

given #325 (T,wt=13): 3078 (x v (y v z)) ^ (u ^ y) = u ^ y.  [para(2925(a,1),2503(a,1,1))].

given #326 (A,wt=47): 2026 (((((x v y) v z) v u) v v) v ((x v (w ^ ((((x v y) v z) v u) v v))) ^ v6)) ^ (((((x v y) v z) v u) v v) v v7) = (((x v y) v z) v u) v v.  [back_rewrite(1339),rewrite(1786(1),1786(6),1814(10),1786(5),1786(5),1786(13),1786(17),1786(21),1786(19))].

given #327 (F,wt=13): 3079 ((x v y) v z) ^ (y ^ u) = y ^ u.  [para(2925(a,1),2505(a,1,1,1))].

given #328 (F,wt=13): 3080 (x v (y v z)) ^ (y ^ u) = y ^ u.  [para(2925(a,1),2505(a,1,1))].

given #329 (T,wt=13): 3081 (((x v (y v z)) v u) v v) ^ y = y.  [para(2925(a,1),2506(a,1,1,1,1))].

given #330 (T,wt=13): 3082 ((x v ((y v z) v u)) v v) ^ y = y.  [para(2925(a,1),2506(a,1,1,1))].

given #331 (A,wt=15): 2030 x ^ (((((x v y) v z) v u) v v) v w) = x.  [back_rewrite(1332),rewrite(1786(1),1786(2),1814(2),1786(1),1786(1),1786(1),1786(7))].

given #332 (F,wt=13): 3083 (x v (((y v z) v u) v v)) ^ y = y.  [para(2925(a,1),2506(a,1,1))].

given #333 (F,wt=13): 3084 (((x v (y v z)) v u) v v) ^ z = z.  [para(2925(a,1),2507(a,1,1,1,1))].

given #334 (T,wt=13): 3085 ((x v ((y v z) v u)) v v) ^ z = z.  [para(2925(a,1),2507(a,1,1,1))].

given #335 (T,wt=13): 3086 (x v (((y v z) v u) v v)) ^ z = z.  [para(2925(a,1),2507(a,1,1))].

given #336 (A,wt=51): 2036 ((((x v y) v z) v u) v ((x v (v ^ (((x v y) v z) v u))) ^ w)) ^ (((v6 v (((x v y) v z) v u)) ^ (v7 v (((x v y) v z) v u))) v v8) = ((x v y) v z) v u.  [back_rewrite(1320),rewrite(1786(1),1786(5),1814(8),1786(4),1786(4),1786(11),1786(15),1786(22))].

given #337 (F,wt=13): 3087 x ^ (y v ((x v z) ^ (u v x))) = x.  [para(2925(a,1),2525(a,1,2))].

given #338 (F,wt=13): 3088 x ^ (y v ((z v x) ^ (x v u))) = x.  [para(2925(a,1),2526(a,1,2))].

given #339 (T,wt=13): 3089 (x v ((y v z) ^ (u v z))) ^ z = z.  [para(2925(a,1),2530(a,1,1))].

given #340 (T,wt=13): 3090 (x v ((y v z) ^ (u v y))) ^ y = y.  [para(2925(a,1),2569(a,1,1))].

given #341 (A,wt=63): 2039 ((((x v y) v z) v u) v (((((v ^ (((x v y) v z) v u)) v (w ^ (((x v y) v z) v u))) ^ v6) v x) ^ v7)) ^ (((v8 v (((x v y) v z) v u)) ^ (v9 v (((x v y) v z) v u))) v v10) = ((x v y) v z) v u.  [back_rewrite(1308),rewrite(1814(8),1786(10))].

given #342 (F,wt=13): 3091 (x v ((y v z) ^ (z v u))) ^ z = z.  [para(2925(a,1),2577(a,1,1))].

given #343 (F,wt=13): 3092 x ^ (y v ((x v z) ^ (x v u))) = x.  [para(2925(a,1),2587(a,1,2))].

given #344 (T,wt=13): 3169 x v (((x ^ y) v (z ^ x)) ^ u) = x.  [para(1861(a,1),2299(a,1)),flip(a)].

given #345 (T,wt=11): 7861 x v ((x ^ y) v (z ^ x)) = x.  [para(1749(a,1),3169(a,1,2))].

given #346 (A,wt=63): 2040 ((((x v y) v z) v u) v (((((v ^ (((x v y) v z) v u)) v x) ^ w) v (v6 ^ (((x v y) v z) v u))) ^ v7)) ^ (((v8 v (((x v y) v z) v u)) ^ (v9 v (((x v y) v z) v u))) v v10) = ((x v y) v z) v u.  [back_rewrite(1307),rewrite(1814(8),1786(10))].

given #347 (F,wt=11): 8038 x v ((x ^ y) v (x ^ z)) = x.  [para(2330(a,1),7861(a,1,2,2))].

given #348 (F,wt=11): 8044 x v ((y ^ x) v (z ^ x)) = x.  [para(2427(a,1),7861(a,1,2,1))].

given #349 (T,wt=11): 8097 ((x ^ y) v (z ^ x)) v x = x.  [para(7861(a,1),2925(a,1,2)),rewrite(7861(8))].

given #350 (T,wt=11): 8354 x v ((y ^ x) v (x ^ z)) = x.  [para(2427(a,1),8038(a,1,2,1))].

============================== PROOF =================================

% Proof 1 at 4.26 (+ 0.05) seconds: McKenzie.
% Length of proof is 101.
% Level of proof is 32.
% Maximum clause weight is 89.
% Given clauses 350.

1 y v (x ^ (y ^ z)) = y & y ^ (x v (y v z)) = y & ((x ^ y) v (y ^ z)) v y = y & ((x v y) ^ (y v z)) ^ y = y # answer(McKenzie) # label(goal).  [goal].
2 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (((w v y) ^ (v6 v y)) v v7) = y # label(A2).  [assumption].
3 c1 v (c2 ^ (c1 ^ c3)) != c1 | c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 | ((c2 v c1) ^ (c1 v c3)) ^ c1 != c1 # answer(McKenzie).  [deny(1)].
4 (((x v ((y v z) ^ (u v z))) ^ ((y v z) ^ (u v z))) v ((z v (v ^ ((y v z) ^ (u v z)))) ^ w)) ^ (((v6 v ((y v z) ^ (u v z))) ^ (v7 v ((y v z) ^ (u v z)))) v v8) = (y v z) ^ (u v z).  [para(2(a,1),2(a,1,1,2,1,1))].
6 (((x v y) ^ y) v (y v y)) ^ (((z v y) ^ (u v y)) v v) = y.  [para(2(a,1),2(a,1,1,2))].
7 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v (((w ^ ((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v))) v (v6 ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v7)) ^ (z v v8) = ((y ^ (z v z)) v (u ^ z)) ^ v.  [para(2(a,1),2(a,1,2,1))].
10 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (y v z) = y v y.  [para(6(a,1),6(a,1,2,1))].
11 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (((v v y) ^ (w v y)) v v6) = y.  [para(10(a,1),2(a,1,1,2,1,1))].
17 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (z ^ (y v y))) ^ u)) ^ (y v v) = y v y.  [para(6(a,1),11(a,1,2,1))].
21 (((x v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) ^ ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) v u) ^ (((w v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) ^ (v6 v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u))))) v v7) = (y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)).  [para(2(a,1),4(a,1,1,2))].
25 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) ^ (((v6 v y) ^ (v7 v y)) v v8) = y.  [para(11(a,1),4(a,1,1,1,1,2)),rewrite(11(17),11(22),11(26),11(27),11(31))].
29 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (y v y)) ^ z)) ^ (y v u) = y v y.  [para(10(a,1),17(a,1,1,2,1,2))].
37 (((x v y) ^ y) v (z ^ y)) ^ (((u v y) ^ (v v y)) v w) = y.  [para(2(a,1),25(a,1,1,2))].
41 (((x v (y v z)) ^ (y v z)) v ((((((y v z) v (y v z)) v (y v y)) ^ u) v (v ^ (y v z))) ^ w)) ^ (((v6 v (y v z)) ^ (v7 v (y v z))) v v8) = y v z.  [para(10(a,1),25(a,1,1,2,1,1,1,2))].
50 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (y v u) = y v y.  [para(6(a,1),37(a,1,2,1))].
60 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (z v v) = y ^ z.  [para(37(a,1),37(a,1,2,1))].
70 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (y v z) = y v y.  [para(10(a,1),50(a,1,1,2))].
73 ((x v x) v ((x v x) v (x v x))) ^ (((y v (x v x)) ^ (z v (x v x))) v u) = x v x.  [para(70(a,1),6(a,1,1,1))].
86 ((x v x) v (y ^ (x v x))) ^ (x v z) = x v x.  [para(70(a,1),50(a,1,1,1))].
87 ((x v x) v (x v x)) ^ (x v y) = x v x.  [para(70(a,1),70(a,1,1,1))].
96 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (x v v) = x v x.  [para(7(a,1),86(a,1,1,2))].
98 (((x v y) ^ y) v (z ^ y)) ^ ((((u v y) ^ (v v y)) v w) v v6) = y.  [para(2(a,1),60(a,1,1,1,1,2)),rewrite(2(14),2(15),2(23))].
106 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (y v u) = y v y.  [para(60(a,1),50(a,1,1,2))].
107 ((x v x) v (y ^ x)) ^ (x v z) = x v x.  [para(60(a,1),86(a,1,1,2))].
115 (((x v y) v (x v y)) v (x v x)) ^ ((x v y) v z) = (x v y) v (x v y).  [para(10(a,1),107(a,1,1,2))].
147 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (x v v) = x v x.  [para(60(a,1),96(a,1,1,2,1,1))].
164 ((x v x) v x) ^ (x v y) = x v x.  [para(2(a,1),147(a,1,1,2))].
178 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ ((y v y) v w) = y.  [para(164(a,1),2(a,1,2,1))].
179 (((x v y) ^ y) v (y v y)) ^ ((y v y) v z) = y.  [para(164(a,1),6(a,1,2,1))].
201 (((x v y) ^ y) v (z ^ y)) ^ (((y v y) v u) v v) = y.  [para(179(a,1),60(a,1,1,1,1,2)),rewrite(179(8),179(9),179(15))].
231 (((x v y) ^ y) v (z ^ y)) ^ ((((y v y) v u) v v) v w) = y.  [para(201(a,1),60(a,1,1,1,1,2)),rewrite(201(9),201(10),201(17))].
599 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ ((y v y) v w) = y.  [para(60(a,1),178(a,1,1,2,1,1))].
617 (((x v y) ^ y) v y) ^ ((y v y) v z) = y.  [para(2(a,1),599(a,1,1,2))].
645 (((x v y) ^ y) v (y v y)) ^ (y v z) = y.  [para(617(a,1),6(a,1,2,1))].
650 (((x v y) ^ y) v (z ^ y)) ^ (y v u) = y.  [para(617(a,1),37(a,1,2,1))].
663 (x v ((((x v x) v (x v x)) v (y ^ (x v x))) ^ z)) ^ (x v u) = x v x.  [para(645(a,1),17(a,1,1,1))].
665 (x v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (x v z) = x v x.  [para(645(a,1),29(a,1,1,1))].
675 (x v (x v x)) ^ (x v y) = x v x.  [para(645(a,1),70(a,1,1,1))].
676 (x v x) v (x v x) = x v x.  [para(70(a,1),645(a,1,1,1)),rewrite(675(8))].
682 (x v (y ^ x)) ^ (x v z) = x v x.  [para(645(a,1),106(a,1,1,1))].
695 (x v (y ^ (x v x))) ^ ((((x v x) v z) v u) v v) = x v x.  [para(645(a,1),231(a,1,1,1)),rewrite(676(6))].
733 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ ((y v y) v v) = y.  [para(645(a,1),178(a,1,1,2,1,1))].
739 (x v ((x v x) ^ y)) ^ (x v z) = x v x.  [back_rewrite(665),rewrite(676(3),676(3))].
741 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (x v u) = x v x.  [back_rewrite(663),rewrite(676(3))].
785 (x v x) ^ (x v y) = x v x.  [back_rewrite(87),rewrite(676(3))].
790 (x v x) ^ (((y v (x v x)) ^ (z v (x v x))) v u) = x v x.  [back_rewrite(73),rewrite(676(4),676(3))].
882 ((x v x) v ((y ^ x) v (y ^ x))) ^ (x v z) = x v x.  [para(785(a,1),147(a,1,1,2))].
912 (((x v y) ^ y) v y) ^ (((z v y) ^ (u v y)) v v) = y.  [para(37(a,1),21(a,1,1,1,1,2)),rewrite(37(13),37(15),37(16),37(20))].
1011 ((x v x) v ((x v x) ^ y)) ^ ((x v x) v z) = x v x.  [para(676(a,1),739(a,1,1,2,1)),rewrite(676(10))].
1446 ((((x v y) ^ y) v ((x v y) ^ y)) v y) ^ ((((x v y) ^ y) v ((x v y) ^ y)) v z) = ((x v y) ^ y) v ((x v y) ^ y).  [para(37(a,1),1011(a,1,1,2))].
1513 (x v (y ^ x)) ^ ((((x v x) v z) v u) v v) = x v x.  [para(60(a,1),695(a,1,1,2))].
1598 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ (y v y) = y.  [para(676(a,1),733(a,1,2))].
1615 (((x v ((y v z) ^ z)) ^ ((y v z) ^ z)) v z) ^ (((y v z) ^ z) v ((y v z) ^ z)) = (y v z) ^ z.  [para(2(a,1),1598(a,1,1,2))].
1641 (x v (((x v x) v x) ^ y)) ^ (x v z) = x v x.  [para(645(a,1),741(a,1,1,2,1,2))].
1664 (((x v (y v y)) ^ (y v y)) v ((((y v y) ^ z) v (u ^ (y v y))) ^ v)) ^ (((w v (y v y)) ^ (y v y)) v v6) = y v y.  [para(676(a,1),41(a,1,2,1,2)),rewrite(676(7),676(7))].
1681 (((x v (y v y)) ^ (y v y)) v ((((y v y) ^ z) v y) ^ u)) ^ (((v v (y v y)) ^ (w v (y v y))) v v6) = y v y.  [para(1598(a,1),41(a,1,1,2,1,2)),rewrite(676(7),676(7))].
1694 (((x v (((y v y) v y) ^ z)) ^ (((y v y) v y) ^ z)) v (((y v y) v y) ^ z)) ^ ((y v y) v u) = ((y v y) v y) ^ z.  [para(1641(a,1),912(a,1,2,1))].
1696 (x v x) ^ (((x v y) v (x v y)) v z) = x v x.  [para(115(a,1),790(a,1,2,1))].
1697 (x v x) ^ (((x v x) ^ (y v (x v x))) v z) = x v x.  [para(676(a,1),790(a,1,2,1,1))].
1699 (x v x) ^ (((y v ((z v (x v x)) ^ (x v x))) ^ (u v ((z v (x v x)) ^ (x v x)))) v v) = x v x.  [para(21(a,1),790(a,1,2,1))].
1700 ((x ^ y) v (x ^ y)) ^ ((y v y) v z) = (x ^ y) v (x ^ y).  [para(882(a,1),790(a,1,2,1))].
1737 ((x v y) ^ y) v ((x v y) ^ y) = y.  [para(37(a,1),1697(a,1,2,1)),rewrite(650(7)),flip(a)].
1749 x ^ (x v y) = x.  [para(98(a,1),1697(a,1,2,1)),rewrite(1737(5),1737(7))].
1780 ((((x v x) ^ (y v (x v x))) v z) v (x v x)) ^ (((((((x v x) ^ (y v (x v x))) v z) v (((x v x) ^ (y v (x v x))) v z)) v u) v v) v w) = (((x v x) ^ (y v (x v x))) v z) v (((x v x) ^ (y v (x v x))) v z).  [para(1697(a,1),1513(a,1,1,2))].
1784 (((x v ((y v z) ^ z)) ^ ((y v z) ^ z)) v z) ^ z = (y v z) ^ z.  [back_rewrite(1615),rewrite(1737(12))].
1786 x v x = x.  [back_rewrite(1446),rewrite(1737(5),1737(6),785(3),1737(6))].
1792 (((x ^ (y v x)) v z) v x) ^ (((((x ^ (y v x)) v z) v u) v v) v w) = (x ^ (y v x)) v z.  [back_rewrite(1780),rewrite(1786(1),1786(1),1786(4),1786(5),1786(5),1786(8),1786(8),1786(11),1786(12),1786(12),1786(15),1786(15),1786(18))].
1814 (x v y) ^ y = y.  [back_rewrite(1737),rewrite(1786(5))].
1831 (x ^ y) ^ (y v z) = x ^ y.  [back_rewrite(1700),rewrite(1786(3),1786(2),1786(6))].
1832 x ^ (((y v x) ^ (z v x)) v u) = x.  [back_rewrite(1699),rewrite(1786(1),1786(1),1786(2),1814(2),1786(2),1786(3),1814(3),1786(6))].
1834 x ^ ((x v y) v z) = x.  [back_rewrite(1696),rewrite(1786(1),1786(3),1786(4))].
1836 (x ^ y) ^ (x v z) = x ^ y.  [back_rewrite(1694),rewrite(1786(1),1786(1),1786(3),1786(3),1814(4),1786(2),1786(2),1786(3),1786(2),1786(4),1786(4))].
1848 (x v (((x ^ y) v x) ^ z)) ^ (((u v x) ^ (v v x)) v w) = x.  [back_rewrite(1681),rewrite(1786(1),1786(2),1814(2),1786(1),1786(5),1786(6),1786(10))].
1861 (x v (((x ^ y) v (z ^ x)) ^ u)) ^ (x v v) = x.  [back_rewrite(1664),rewrite(1786(1),1786(2),1814(2),1786(1),1786(2),1786(6),1786(7),1814(7),1786(8))].
2195 (x v (y ^ x)) ^ (x v z) = x.  [back_rewrite(682),rewrite(1786(5))].
2299 x ^ x = x.  [back_rewrite(1784),rewrite(1814(2),1814(3),1814(2),1786(1),1814(3))].
2328 ((x ^ (y v x)) v z) v x = (x ^ (y v x)) v z.  [para(1792(a,1),1834(a,1)),flip(a)].
2330 (x ^ y) ^ x = x ^ y.  [para(1786(a,1),1836(a,1,2))].
2332 x ^ (y v x) = x.  [para(1814(a,1),2330(a,1,1)),rewrite(1814(4))].
2334 (x v y) v x = x v y.  [back_rewrite(2328),rewrite(2332(2),2332(4))].
2360 x v (y ^ x) = x.  [para(2195(a,1),2299(a,1)),flip(a)].
2427 x ^ (y ^ x) = y ^ x.  [para(2360(a,1),1814(a,1,1))].
2464 (x v y) ^ (z ^ x) = z ^ x.  [para(1831(a,1),2427(a,1,2)),rewrite(1831(6))].
2522 x ^ ((y v x) ^ (z v x)) = x.  [para(1786(a,1),1832(a,1,2))].
2541 x ^ ((y v x) ^ (x v z)) = x.  [para(2334(a,1),2522(a,1,2,2))].
2573 ((x v y) ^ (y v z)) ^ y = y.  [para(2541(a,1),2427(a,1,2)),rewrite(2541(8))].
2578 c1 v (c2 ^ (c1 ^ c3)) != c1 | c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 # answer(McKenzie).  [back_rewrite(3),rewrite(2573(38)),xx(d)].
2834 x v (((x ^ y) v x) ^ z) = x.  [para(1848(a,1),2332(a,1)),flip(a)].
2859 x v ((x ^ y) v x) = x.  [para(1749(a,1),2834(a,1,2))].
2867 x v (y ^ (x ^ z)) = x.  [para(2464(a,1),2834(a,1,2))].
2903 c1 ^ (c2 v (c1 v c3)) != c1 | ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 # answer(McKenzie).  [back_rewrite(2578),rewrite(2867(7)),xx(a)].
2904 (x ^ y) v x = x.  [para(2859(a,1),1814(a,1,1)),rewrite(2332(3)),flip(a)].
2925 x v (y v x) = y v x.  [para(1814(a,1),2904(a,1,1))].
3048 x ^ (y v (x v z)) = x.  [para(2925(a,1),1834(a,1,2))].
3095 ((c2 ^ c1) v (c1 ^ c3)) v c1 != c1 # answer(McKenzie).  [back_rewrite(2903),rewrite(3048(7)),xx(a)].
3169 x v (((x ^ y) v (z ^ x)) ^ u) = x.  [para(1861(a,1),2299(a,1)),flip(a)].
7861 x v ((x ^ y) v (z ^ x)) = x.  [para(1749(a,1),3169(a,1,2))].
8038 x v ((x ^ y) v (x ^ z)) = x.  [para(2330(a,1),7861(a,1,2,2))].
8354 x v ((y ^ x) v (x ^ z)) = x.  [para(2427(a,1),8038(a,1,2,1))].
8768 ((x ^ y) v (y ^ z)) v y = y.  [para(8354(a,1),2925(a,1,2)),rewrite(8354(8))].
8769 $F # answer(McKenzie).  [resolve(8768,a,3095,a)].

============================== end of proof ==========================

============================== STATISTICS ============================

Given=350. Generated=93657. Kept=8767. proofs=1.
Usable=179. Sos=5850. Demods=6053. Limbo=25, Disabled=2714. Hints=0.
Weight_deleted=7832. Literals_deleted=0.
Forward_subsumed=77058. Back_subsumed=289.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=8762 (0 lex), Back_demodulated=2423. Back_unit_deleted=0.
Demod_attempts=4166215. Demod_rewrites=278387.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=3.
Megabytes=12.80.
User_CPU=4.26, System_CPU=0.06, Wall_clock=4.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 3830 exit (max_proofs) Wed Nov 22 11:24:02 2006