============================== Prover9 =============================== Prover9 (32) version June-2007, June 2007. Process 18409 was started by mccune on cleo, Mon Jun 18 15:23:24 2007 The command was "prover9 -f olsax-fold.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file olsax-fold.in assign(max_seconds,300). assign(order,kbo). assign(new_constants,1). set(restrict_denials). assign(eq_defs,fold). formulas(assumptions). f(f(f(f(y,x),f(x,z)),u),f(x,f(f(x,f(f(y,y),y)),z))) = x # label(OL_Sh). x v y = f(f(x,x),f(y,y)) # label(definition_join). x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). x' = f(x,x) # label(definition_complementation). end_of_list. formulas(goals). f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(assoc). f(f(x,x),f(x,y)) = x # answer(absorb). f(x,f(x,x)) = f(y,f(y,y)) # answer(one). f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) & f(f(x,x),f(x,y)) = x & f(x,f(x,x)) = f(y,f(y,y)) # answer(combined). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(assoc) # label(non_clause) # label(goal). [goal]. 2 f(f(x,x),f(x,y)) = x # answer(absorb) # label(non_clause) # label(goal). [goal]. 3 f(x,f(x,x)) = f(y,f(y,y)) # answer(one) # label(non_clause) # label(goal). [goal]. 4 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) & f(f(x,x),f(x,y)) = x & f(x,f(x,x)) = f(y,f(y,y)) # answer(combined) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z))) = y # label(OL_Sh). [assumption]. x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. x' = f(x,x) # label(definition_complementation). [assumption]. f(c1,f(f(c2,c3),f(c2,c3))) != f(c2,f(f(c1,c3),f(c1,c3))) # answer(assoc). [deny(1)]. f(f(c4,c4),f(c4,c5)) != c4 # answer(absorb). [deny(2)]. f(c6,f(c6,c6)) != f(c7,f(c7,c7)) # answer(one). [deny(3)]. f(c8,f(f(c9,c10),f(c9,c10))) != f(c9,f(f(c8,c10),f(c8,c10))) | f(f(c8,c8),f(c8,c9)) != c8 | f(c8,f(c8,c8)) != f(c9,f(c9,c9)) # answer(combined). [deny(4)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 4). % (Horn set with more than one neg. clause) Term ordering decisions: % Assigning unary symbol ' kb_weight 0 and highest precedence (15). Function symbol KB weights: c1=1. c2=1. c3=1. c4=1. c5=1. c6=1. c7=1. c8=1. c9=1. c10=1. f=1. ^=1. v=1. '=0. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, f, ^, v, ' ]). Skipping inverse_order, because term ordering is KBO. Folding symbols: ^/2 v/2. After fold_eq: Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, ^, v, f, ' ]). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: % set(back_unit_deletion). % (Horn set with negative nonunits) % set(back_unit_deletion) -> set(unit_deletion). restricted denial: (wt=13): 13 f(c2,f(c1,c3)') != f(c1,f(c2,c3)') # answer(assoc). [copy(12),rewrite([11(8),11(14)]),flip(a)]. restricted denial: (wt=8): 15 f(c4',f(c4,c5)) != c4 # answer(absorb). [copy(14),rewrite([11(3)])]. restricted denial: (wt=9): 17 f(c7,c7') != f(c6,c6') # answer(one). [copy(16),rewrite([11(4),11(8)]),flip(a)]. restricted denial: (wt=30): 19 f(c9,f(c8,c10)') != f(c8,f(c9,c10)') | f(c8',f(c8,c9)) != c8 | f(c9,c9') != f(c8,c8') # answer(combined). [copy(18),rewrite([11(8),11(14),11(16),11(25),11(29)]),flip(a),flip(c)]. restricted denial: (wt=28): 23 f(c9,c8 ^ c10) != f(c8,c9 ^ c10) | f(c8',f(c8,c9)) != c8 | f(c9,c9') != f(c8,c8') # answer(combined). [back_rewrite(19),rewrite([20(5),20(10)])]. restricted denial: (wt=11): 24 f(c2,c1 ^ c3) != f(c1,c2 ^ c3) # answer(assoc). [back_rewrite(13),rewrite([20(5),20(10)])]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 15 f(c4',f(c4,c5)) != c4 # answer(absorb). [copy(14),rewrite([11(3)])]. 17 f(c7,c7') != f(c6,c6') # answer(one). [copy(16),rewrite([11(4),11(8)]),flip(a)]. 23 f(c9,c8 ^ c10) != f(c8,c9 ^ c10) | f(c8',f(c8,c9)) != c8 | f(c9,c9') != f(c8,c8') # answer(combined). [back_rewrite(19),rewrite([20(5),20(10)])]. 24 f(c2,c1 ^ c3) != f(c1,c2 ^ c3) # answer(assoc). [back_rewrite(13),rewrite([20(5),20(10)])]. end_of_list. formulas(sos). 11 f(x,x) = x'. [copy(10),flip(a)]. 20 f(x,y)' = x ^ y. [back_rewrite(9),rewrite([11(3)])]. 21 f(x',y') = x v y. [back_rewrite(7),rewrite([11(1),11(2)])]. 22 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(x',x)),z))) = y. [back_rewrite(5),rewrite([11(5)])]. end_of_list. formulas(demodulators). 11 f(x,x) = x'. [copy(10),flip(a)]. 20 f(x,y)' = x ^ y. [back_rewrite(9),rewrite([11(3)])]. 21 f(x',y') = x v y. [back_rewrite(7),rewrite([11(1),11(2)])]. 22 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(x',x)),z))) = y. [back_rewrite(5),rewrite([11(5)])]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=6): 11 f(x,x) = x'. [copy(10),flip(a)]. given #2 (I,wt=8): 20 f(x,y)' = x ^ y. [back_rewrite(9),rewrite([11(3)])]. given #3 (I,wt=9): 21 f(x',y') = x v y. [back_rewrite(7),rewrite([11(1),11(2)])]. given #4 (I,wt=22): 22 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(x',x)),z))) = y. [back_rewrite(5),rewrite([11(5)])]. given #5 (A,wt=7): 25 x ^ x = x''. [para(11(a,1),20(a,1,1)),flip(a)]. given #6 (T,wt=7): 26 x v x = x''. [para(21(a,1),11(a,1))]. given #7 (T,wt=10): 27 (x v y)' = x' ^ y'. [para(21(a,1),20(a,1,1))]. given #8 (T,wt=12): 28 f(x ^ y,z') = f(x,y) v z. [para(20(a,1),21(a,1,1))]. given #9 (T,wt=12): 29 f(x',y ^ z) = x v f(y,z). [para(20(a,1),21(a,1,2))]. given #10 (A,wt=21): 30 f(f(f(x',f(x,y)),z),f(x,f(f(x,f(x',x)),y))) = x. [para(11(a,1),22(a,1,1,1,1))]. given #11 (T,wt=15): 47 f(x ^ y,z ^ u) = f(x,y) v f(z,u). [para(20(a,1),28(a,1,2))]. given #12 (T,wt=18): 32 f(f(x'',y),f(x,f(f(x,f(x',x)),x))) = x. [para(11(a,1),22(a,1,1,1)),rewrite([11(1)])]. given #13 (T,wt=17): 75 f(x''',f(x,f(f(x,f(x',x)),x))) = x. [para(11(a,1),32(a,1,1))]. given #14 (T,wt=17): 78 f(x' v y,f(x,f(f(x,f(x',x)),x))) = x. [para(21(a,1),32(a,1,1))]. given #15 (A,wt=21): 31 f(f(f(f(x,y),y'),z),f(y,f(f(y,f(x',x)),y))) = y. [para(11(a,1),22(a,1,1,1,2))]. given #16 (T,wt=17): 87 f(x,f(x',f(f(x',x' v x),y))) = x'. [para(32(a,1),30(a,1,1)),rewrite([21(6)])]. given #17 (T,wt=12): 140 f(x',f(x'',x)) = x''. [para(32(a,1),87(a,1,2,2))]. given #18 (T,wt=13): 142 x' ^ f(x'',x) = x'''. [para(140(a,1),20(a,1,1)),flip(a)]. given #19 (T,wt=14): 131 f(x,x v f(x',x' v x)) = x'. [para(11(a,1),87(a,1,2,2)),rewrite([20(6),29(6)])]. given #20 (A,wt=20): 33 f(f(x,y) ^ f(y,z),f(y,f(f(y,f(x',x)),z))) = y. [para(11(a,1),22(a,1,1)),rewrite([20(4)])]. given #21 (T,wt=14): 144 f(x'',x'' v x) = x'''. [para(21(a,1),140(a,1,2))]. given #22 (T,wt=15): 152 x'' ^ (x'' v x) = x''''. [para(21(a,1),142(a,1,2))]. given #23 (T,wt=15): 155 x ^ (x v f(x',x' v x)) = x''. [para(131(a,1),20(a,1,1)),flip(a)]. given #24 (T,wt=17): 143 f(x ^ y,f((x ^ y)',f(x,y))) = (x ^ y)'. [para(20(a,1),140(a,1,1)),rewrite([20(3),20(8)])]. given #25 (A,wt=32): 34 f(f(f(f(x,f(x',x)),f(f(x',x),y)),z),f(f(x',x),f(x' ^ x,y))) = f(x',x). [para(11(a,1),22(a,1,2,2,1)),rewrite([20(13)])]. given #26 (T,wt=18): 89 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(75(a,1),20(a,1,1)),flip(a)]. given #27 (T,wt=18): 97 (x' v y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(78(a,1),20(a,1,1)),flip(a)]. given #28 (T,wt=18): 132 x ^ f(x',f(f(x',x' v x),y)) = x''. [para(87(a,1),20(a,1,1)),flip(a)]. given #29 (T,wt=18): 151 (x ^ y) ^ f((x ^ y)',f(x,y)) = (x ^ y)''. [para(20(a,1),142(a,1,1)),rewrite([20(3),20(8)])]. given #30 (A,wt=25): 35 f(f(f(f(x,y),f(y,f(y,f(x',x)))),z),f(y,y ^ f(x',x))) = y. [para(11(a,1),22(a,1,2,2)),rewrite([20(11)])]. given #31 (T,wt=17): 289 f(x,x v f(x',f(y ^ x,f(y,x)))) = x'. [para(31(a,1),35(a,1,1)),rewrite([20(4),29(7)])]. given #32 (T,wt=18): 281 f(x,f(f(x,y),f(x,y) ^ (x' v x))) = f(x,y). [para(30(a,1),35(a,1,1)),rewrite([21(6)])]. given #33 (T,wt=12): 346 f(x,f(x',x' v x)) = x'. [para(281(a,1),87(a,1,2))]. given #34 (T,wt=13): 354 x ^ f(x',x' v x) = x''. [para(281(a,1),132(a,1,2))]. given #35 (A,wt=23): 36 f(f(f(x,y),f(y,z)),u) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(22(a,1),20(a,1,1)),flip(a)]. given #36 (T,wt=18): 299 x ^ (x v f(x',f(y ^ x,f(y,x)))) = x''. [para(289(a,1),20(a,1,1)),flip(a)]. given #37 (T,wt=18): 327 x ^ f(f(x,y),f(x,y) ^ (x' v x)) = x ^ y. [para(281(a,1),20(a,1,1)),rewrite([20(2)]),flip(a)]. given #38 (T,wt=19): 53 f(x' ^ f(x,y),f(x,f(f(x,f(x',x)),y))) = x. [para(11(a,1),30(a,1,1)),rewrite([20(4)])]. given #39 (T,wt=19): 76 f(x'',y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(32(a,1),20(a,1,1)),flip(a)]. given #40 (A,wt=27): 37 f(f(f(f(f(x,y),z),f(z,u)),w),f(z,f(f(z,f(x ^ y,f(x,y))),u))) = z. [para(20(a,1),22(a,1,2,2,1,2,1))]. given #41 (T,wt=19): 105 f(f(x,y) ^ y',f(y,f(f(y,f(x',x)),y))) = y. [para(11(a,1),31(a,1,1)),rewrite([20(4)])]. given #42 (T,wt=19): 148 f((x ^ y)',(x ^ y)' v f(x,y)) = (x ^ y)''. [para(29(a,1),140(a,1,2))]. given #43 (T,wt=19): 357 f(f(x,y),f(x ^ y,(x ^ y) v f(x,y))) = x ^ y. [para(20(a,1),346(a,1,2,1)),rewrite([20(4),20(9)])]. given #44 (T,wt=20): 62 f(x,f(f(x,y),f(f(f(x,y),x' v x),z))) = f(x,y). [para(30(a,1),22(a,1,1)),rewrite([21(6)])]. given #45 (A,wt=26): 38 f(f(f(x v y,f(y',z)),u),f(y',f(f(y',x' v x),z))) = y'. [para(21(a,1),22(a,1,1,1,1)),rewrite([21(11)])]. given #46 (T,wt=14): 689 f(x,f(f(x,y),x' v x)) = f(x,y). [para(281(a,1),62(a,1,2))]. given #47 (T,wt=14): 755 x ^ f(f(x,y),x' v x) = x ^ y. [para(689(a,1),20(a,1,1)),rewrite([20(2)]),flip(a)]. given #48 (T,wt=17): 757 f(x',f(x v y,x'' v x')) = x v y. [para(21(a,1),689(a,1,2,1)),rewrite([21(11)])]. given #49 (T,wt=18): 673 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),62(a,1,2,2))]. given #50 (A,wt=27): 39 f(f(f(f(x,y'),y v z),u),f(y',f(f(y',f(x',x)),z'))) = y'. [para(21(a,1),22(a,1,1,1,2))]. given #51 (T,wt=18): 790 f(x' ^ f(x,x' v x),f(x,f(x',x))) = x. [para(689(a,1),53(a,1,2))]. given #52 (T,wt=18): 832 x' ^ f(f(x',f(x,y)),x) = x' ^ f(x,y). [para(673(a,1),20(a,1,1)),rewrite([20(4)]),flip(a)]. given #53 (T,wt=19): 679 f(f(x,y),f(f(f(x,y),y'),y)) = f(f(x,y),y'). [para(31(a,1),62(a,1,2,2))]. given #54 (T,wt=19): 770 f(x''',f(x,x'''' v x''')) = x. [para(75(a,1),689(a,1,2,1)),rewrite([75(22)])]. given #55 (A,wt=23): 40 f(f(f(f(x',y),f(y,z)),u),f(y,f(f(y,x' v x),z))) = y. [para(21(a,1),22(a,1,2,2,1,2))]. given #56 (T,wt=19): 777 f(f(x,y) ^ f(y,y' v y),f(y,f(x',x))) = y. [para(689(a,1),33(a,1,2))]. given #57 (T,wt=19): 803 x' ^ f(x v y,x'' v x') = x' ^ y'. [para(21(a,1),755(a,1,2,1))]. given #58 (T,wt=19): 900 (x' ^ f(x,x' v x)) ^ f(x,f(x',x)) = x'. [para(790(a,1),20(a,1,1)),flip(a)]. given #59 (T,wt=19): 934 f(x,y) ^ f(f(f(x,y),y'),y) = f(x,y) ^ y'. [para(679(a,1),20(a,1,1)),rewrite([20(4)]),flip(a)]. given #60 (A,wt=71): 41 f(f(f(x,f(f(x,f(f(x,f(y',y)),z)),u)),w),f(f(x,f(f(x,f(y',y)),z)),f(f(f(x,f(f(x,f(y',y)),z)),f(f(f(y,x),f(x,z)) ^ v5,f(f(f(y,x),f(x,z)),v5))),u))) = f(x,f(f(x,f(y',y)),z)). [para(22(a,1),22(a,1,1,1,1)),rewrite([20(23)])]. given #61 (T,wt=20): 115 f(x,f(x',f(f(x',f(y ^ x,f(y,x))),z))) = x'. [para(31(a,1),22(a,1,1)),rewrite([20(4)])]. given #62 (T,wt=15): 1228 f(x,f(x',f(y ^ x,f(y,x)))) = x'. [para(281(a,1),115(a,1,2))]. given #63 (T,wt=16): 1262 x ^ f(x',f(y ^ x,f(y,x))) = x''. [para(1228(a,1),20(a,1,1)),flip(a)]. given #64 (T,wt=20): 154 (x ^ y)' ^ ((x ^ y)' v f(x,y)) = (x ^ y)'''. [para(29(a,1),142(a,1,2))]. given #65 (A,wt=61): 42 f(f(f(f(x,f(f(f(y,z),f(z,u)),w)),z),v5),f(f(f(f(y,z),f(z,u)),w),f(f(f(f(f(y,z),f(z,u)),w),f(x',x)),f(z,f(f(z,f(y',y)),u))))) = f(f(f(y,z),f(z,u)),w). [para(22(a,1),22(a,1,1,1,2))]. given #66 (T,wt=20): 372 f(x,y) ^ f(x ^ y,(x ^ y) v f(x,y)) = (x ^ y)'. [para(20(a,1),354(a,1,2,1)),rewrite([20(4),20(9)])]. given #67 (T,wt=20): 392 x ^ f(f(x,y),f(f(f(x,y),x' v x),z)) = x ^ y. [para(30(a,1),36(a,1,1)),rewrite([21(6),20(10)])]. given #68 (T,wt=20): 471 (x' ^ f(x,y)) ^ f(x,f(f(x,f(x',x)),y)) = x'. [para(53(a,1),20(a,1,1)),flip(a)]. given #69 (T,wt=20): 581 (f(x,y) ^ y') ^ f(y,f(f(y,f(x',x)),y)) = y'. [para(105(a,1),20(a,1,1)),flip(a)]. given #70 (A,wt=34): 43 f(f(x,y),f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z',z)),u)))) = x. [para(22(a,1),22(a,1,1,1)),rewrite([20(5)])]. given #71 (T,wt=8): 1606 f(x,x'') = x'. [para(43(a,1),87(a,1,2,2)),rewrite([11(3)])]. given #72 (T,wt=9): 1625 x ^ x'' = x''. [para(43(a,1),132(a,1,2,2)),rewrite([11(3)])]. given #73 (T,wt=9): 1658 f(x,x ^ y) = f(x,y). [para(43(a,1),62(a,1,2,2)),rewrite([11(3),20(2)])]. given #74 (T,wt=7): 2014 x'' v x = x. [para(75(a,1),1658(a,2)),rewrite([89(12),21(5)])]. given #75 (A,wt=23): 44 f(x,f(f(x,y),f(f(f(x,y),f(z ^ x,f(z,x))),u))) = f(x,y). [para(22(a,1),22(a,1,1)),rewrite([20(4)])]. given #76 (T,wt=8): 2063 f(f(x,y),x') = x. [para(43(a,1),1658(a,2)),rewrite([380(17)])]. ============================== PROOF ================================= % Proof 1 at 0.77 (+ 0.00) seconds: absorb. % Length of proof is 58. % Level of proof is 12. % Maximum clause weight is 77. % Given clauses 76. 2 f(f(x,x),f(x,y)) = x # answer(absorb) # label(non_clause) # label(goal). [goal]. 5 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z))) = y # label(OL_Sh). [assumption]. 6 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 7 f(f(x,x),f(y,y)) = x v y. [copy(6),flip(a)]. 8 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. 9 f(f(x,y),f(x,y)) = x ^ y. [copy(8),flip(a)]. 10 x' = f(x,x) # label(definition_complementation). [assumption]. 11 f(x,x) = x'. [copy(10),flip(a)]. 14 f(f(c4,c4),f(c4,c5)) != c4 # answer(absorb). [deny(2)]. 15 f(c4',f(c4,c5)) != c4 # answer(absorb). [copy(14),rewrite([11(3)])]. 20 f(x,y)' = x ^ y. [back_rewrite(9),rewrite([11(3)])]. 21 f(x',y') = x v y. [back_rewrite(7),rewrite([11(1),11(2)])]. 22 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(x',x)),z))) = y. [back_rewrite(5),rewrite([11(5)])]. 25 x ^ x = x''. [para(11(a,1),20(a,1,1)),flip(a)]. 27 (x v y)' = x' ^ y'. [para(21(a,1),20(a,1,1))]. 30 f(f(f(x',f(x,y)),z),f(x,f(f(x,f(x',x)),y))) = x. [para(11(a,1),22(a,1,1,1,1))]. 31 f(f(f(f(x,y),y'),z),f(y,f(f(y,f(x',x)),y))) = y. [para(11(a,1),22(a,1,1,1,2))]. 32 f(f(x'',y),f(x,f(f(x,f(x',x)),x))) = x. [para(11(a,1),22(a,1,1,1)),rewrite([11(1)])]. 35 f(f(f(f(x,y),f(y,f(y,f(x',x)))),z),f(y,y ^ f(x',x))) = y. [para(11(a,1),22(a,1,2,2)),rewrite([20(11)])]. 36 f(f(f(x,y),f(y,z)),u) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(22(a,1),20(a,1,1)),flip(a)]. 43 f(f(x,y),f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z',z)),u)))) = x. [para(22(a,1),22(a,1,1,1)),rewrite([20(5)])]. 53 f(x' ^ f(x,y),f(x,f(f(x,f(x',x)),y))) = x. [para(11(a,1),30(a,1,1)),rewrite([20(4)])]. 62 f(x,f(f(x,y),f(f(f(x,y),x' v x),z))) = f(x,y). [para(30(a,1),22(a,1,1)),rewrite([21(6)])]. 75 f(x''',f(x,f(f(x,f(x',x)),x))) = x. [para(11(a,1),32(a,1,1))]. 76 f(x'',y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(32(a,1),20(a,1,1)),flip(a)]. 78 f(x' v y,f(x,f(f(x,f(x',x)),x))) = x. [para(21(a,1),32(a,1,1))]. 87 f(x,f(x',f(f(x',x' v x),y))) = x'. [para(32(a,1),30(a,1,1)),rewrite([21(6)])]. 89 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(75(a,1),20(a,1,1)),flip(a)]. 140 f(x',f(x'',x)) = x''. [para(32(a,1),87(a,1,2,2))]. 144 f(x'',x'' v x) = x'''. [para(21(a,1),140(a,1,2))]. 281 f(x,f(f(x,y),f(x,y) ^ (x' v x))) = f(x,y). [para(30(a,1),35(a,1,1)),rewrite([21(6)])]. 346 f(x,f(x',x' v x)) = x'. [para(281(a,1),87(a,1,2))]. 357 f(f(x,y),f(x ^ y,(x ^ y) v f(x,y))) = x ^ y. [para(20(a,1),346(a,1,2,1)),rewrite([20(4),20(9)])]. 380 f(x,y) ^ f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z',z)),u))) = x'. [para(22(a,1),36(a,1,1,1)),rewrite([20(5)])]. 521 f(x''',y) ^ f(x',f(f(x',x' v x),x')) = x''. [para(21(a,1),76(a,1,2,2,1,2))]. 673 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),62(a,1,2,2))]. 689 f(x,f(f(x,y),x' v x)) = f(x,y). [para(281(a,1),62(a,1,2))]. 770 f(x''',f(x,x'''' v x''')) = x. [para(75(a,1),689(a,1,2,1)),rewrite([75(22)])]. 832 x' ^ f(f(x',f(x,y)),x) = x' ^ f(x,y). [para(673(a,1),20(a,1,1)),rewrite([20(4)]),flip(a)]. 834 f(x'',f(f(x'',x v y),x')) = f(x'',x v y). [para(21(a,1),673(a,1,2,1,2)),rewrite([21(14)])]. 930 (x' ^ f(x,y))' ^ f(f((x' ^ f(x,y))',x),x' ^ f(x,y)) = (x' ^ f(x,y))' ^ x. [para(53(a,1),832(a,1,2,1,2)),rewrite([53(27)])]. 988 f(f(f(x,x ^ (x'''' v x''')),y),f(f(x,x'''' v x'''),f(f(f(x,x'''' v x'''),x''' v x''),f(x,x'''' v x''')))) = f(x,x'''' v x'''). [para(770(a,1),31(a,1,1,1,1)),rewrite([20(10),21(37)])]. 1658 f(x,x ^ y) = f(x,y). [para(43(a,1),62(a,1,2,2)),rewrite([11(3),20(2)])]. 1758 f(f(f(x,x'''' v x'''),y),f(f(x,x'''' v x'''),f(f(f(x,x'''' v x'''),x''' v x''),f(x,x'''' v x''')))) = f(x,x'''' v x'''). [back_rewrite(988),rewrite([1658(10)])]. 2013 f(f(x'',y),x') = x. [para(32(a,1),1658(a,2)),rewrite([76(12)])]. 2014 x'' v x = x. [para(75(a,1),1658(a,2)),rewrite([89(12),21(5)])]. 2022 f(x'',x) = x'''. [para(144(a,1),1658(a,2)),rewrite([2014(7),1658(6)])]. 2063 f(f(x,y),x') = x. [para(43(a,1),1658(a,2)),rewrite([380(17)])]. 2085 f(x'',x v y) = x'''. [back_rewrite(834),rewrite([2013(8),2022(3)]),flip(a)]. 2291 x'' = x. [para(11(a,1),2063(a,1,1)),rewrite([11(3)])]. 2302 f(x,y') = x' v y. [para(78(a,1),2063(a,1,1)),rewrite([27(3),2291(2),1658(3)])]. 2325 (x ^ y)' = f(x,y). [para(357(a,1),2063(a,1,1)),rewrite([20(3),11(3)])]. 2426 f(x,x v y) = x'. [back_rewrite(2085),rewrite([2291(2),2291(4)])]. 2451 f(f(x',y),x) = x'. [back_rewrite(1758),rewrite([2291(2),2291(2),2291(2),2426(3),2291(4),2291(4),2291(4),2426(5),2291(5),2291(5),2291(5),2426(6),2291(6),2291(7),2426(7),2291(5),2291(5),2291(5),2291(5),2426(6),2302(5),2426(6),2291(4),2291(5),2291(5),2291(5),2426(6)])]. 2564 f(x',y) ^ x = x. [back_rewrite(521),rewrite([2291(2),2426(7),2291(5),2302(5),2426(6),2291(4),2291(5)])]. 2602 x ^ x = x. [back_rewrite(25),rewrite([2291(3)])]. 2842 f(x',f(x,y)) = x. [back_rewrite(930),rewrite([2325(4),2325(7),2451(7),1658(8),2602(7),2325(7),2564(7)])]. 2843 $F # answer(absorb). [resolve(2842,a,15,a)]. ============================== end of proof ========================== restricted denial: (wt=28): 2793 f(c9,c8 ^ c10) != f(c8,c9 ^ c10) | f(c8',f(c8,c9)) != c8 | c9' v c9 != c8' v c8 # answer(combined). [back_rewrite(23),rewrite([2302(23),2302(27)])]. restricted denial: (wt=9): 2794 c7' v c7 != c6' v c6 # answer(one). [back_rewrite(17),rewrite([2302(4),2302(8)])]. % Redundant proof: 2967 $F # answer(absorb). [back_rewrite(15),rewrite([2842(6)]),xx(a)]. restricted denial: (wt=20): 2938 f(c9,c8 ^ c10) != f(c8,c9 ^ c10) | c9' v c9 != c8' v c8 # answer(combined). [back_rewrite(2793),rewrite([2842(17)]),xx(b)]. % Disable descendants (x means already disabled): 14x 15x given #77 (T,wt=5): 2291 x'' = x. [para(11(a,1),2063(a,1,1)),rewrite([11(3)])]. restricted denial: (wt=22): 3029 c9' v f(c8,c10) != c8' v f(c9,c10) | c9' v c9 != c8' v c8 # answer(combined). [back_rewrite(2938),rewrite([3018(5),3018(11)])]. restricted denial: (wt=13): 3119 c2' v f(c1,c3) != c1' v f(c2,c3) # answer(assoc). [back_rewrite(24),rewrite([3018(5),3018(11)])]. given #78 (T,wt=5): 2601 x v x = x. [back_rewrite(26),rewrite([2291(3)])]. given #79 (T,wt=5): 2602 x ^ x = x. [back_rewrite(25),rewrite([2291(3)])]. given #80 (A,wt=29): 46 f(f(f(f(x v y,z),f(z,u)),w),f(z,f(f(z,f(x' ^ y',x v y)),u))) = z. [para(27(a,1),22(a,1,2,2,1,2,1))]. given #81 (T,wt=7): 2329 (x ^ y) v x = x. [para(62(a,1),2063(a,1,1)),rewrite([2302(3),20(2)])]. given #82 (T,wt=7): 2427 x ^ (x v y) = x. [back_rewrite(2083),rewrite([2291(2),2291(4),2291(4)])]. given #83 (T,wt=7): 2579 (x v y) ^ x = x. [back_rewrite(256),rewrite([2291(2),2426(6),2291(4),2302(4),2426(5),2291(3),2291(4)])]. given #84 (T,wt=8): 2294 f(x v y,x) = x'. [para(21(a,1),2063(a,1,1)),rewrite([2291(3)])]. given #85 (A,wt=31): 48 f(f(f(f(x,y) v z,f(z',u)),w),f(z',f(f(z',(x ^ y) v f(x,y)),u))) = z'. [para(28(a,1),22(a,1,1,1,1)),rewrite([29(12)])]. given #86 (T,wt=8): 2325 (x ^ y)' = f(x,y). [para(357(a,1),2063(a,1,1)),rewrite([20(3),11(3)])]. given #87 (T,wt=8): 2426 f(x,x v y) = x'. [back_rewrite(2085),rewrite([2291(2),2291(4)])]. given #88 (T,wt=8): 2564 f(x',y) ^ x = x. [back_rewrite(521),rewrite([2291(2),2426(7),2291(5),2302(5),2426(6),2291(4),2291(5)])]. given #89 (T,wt=8): 2842 f(x',f(x,y)) = x. [back_rewrite(930),rewrite([2325(4),2325(7),2451(7),1658(8),2602(7),2325(7),2564(7)])]. given #90 (A,wt=32): 50 f(f(f(x v f(y,z),f(y ^ z,u)),w),f(y ^ z,f(f(y ^ z,x' v x),u))) = y ^ z. [para(29(a,1),22(a,1,1,1,1)),rewrite([21(12)])]. given #91 (T,wt=8): 2939 x ^ f(x',y) = x. [back_rewrite(2478),rewrite([2842(6),2928(4)])]. given #92 (T,wt=9): 1704 x ^ (x ^ y) = x ^ y. [para(43(a,1),392(a,1,2,2)),rewrite([11(3),20(2)])]. given #93 (T,wt=9): 2292 f(x,y) ^ x' = x'. [para(2063(a,1),20(a,1,1)),flip(a)]. given #94 (T,wt=9): 2302 f(x,y') = x' v y. [para(78(a,1),2063(a,1,1)),rewrite([27(3),2291(2),1658(3)])]. restricted denial: (wt=17): 3738 c2' v (c1' v c3') != c1' v (c2' v c3') # answer(assoc). [back_rewrite(3119),rewrite([3465(5),3465(13)])]. restricted denial: (wt=26): 3806 c9' v (c8' v c10') != c8' v (c9' v c10') | c9' v c9 != c8' v c8 # answer(combined). [back_rewrite(3029),rewrite([3465(5),3465(13)])]. given #95 (A,wt=17): 2508 (x v y) ^ (((x v y) ^ y) v y) = (x v y) ^ y. [back_rewrite(1135),rewrite([2291(4),2302(5),20(4),2291(8)])]. given #96 (T,wt=7): 3847 x v (x ^ y) = x. [back_rewrite(2842),rewrite([3465(2),3465(5),2291(2),27(4),2291(2),2291(2)])]. given #97 (T,wt=9): 2616 ((x ^ y) v y) v y = y. [back_rewrite(2038),rewrite([2302(3),20(2)])]. given #98 (T,wt=9): 2928 (x ^ y) ^ x = x ^ y. [back_rewrite(1677),rewrite([2789(5),2602(3)]),flip(a)]. given #99 (T,wt=9): 3192 x v (x v y) = x v y. [para(2579(a,1),2329(a,1,1))]. given #100 (A,wt=11): 2617 (((x ^ y) v y) ^ z) v y = y. [back_rewrite(2017),rewrite([2302(3),20(2),2302(5),20(4)])]. given #101 (T,wt=7): 4263 (x ^ y) v y = y. [para(2579(a,1),2617(a,1,1))]. given #102 (T,wt=9): 3325 (x v y) v x = x v y. [para(2294(a,1),2842(a,1,2)),rewrite([27(2),2302(5),2325(4),2302(3),2291(2)])]. given #103 (T,wt=7): 4358 x v (y ^ x) = x. [para(4263(a,1),3325(a,1,1)),rewrite([4263(4)])]. given #104 (T,wt=9): 3465 f(x,y) = x' v y'. [para(2291(a,1),2302(a,1,2))]. given #105 (A,wt=24): 2658 (x' v y) ^ (((x' v y) ^ (y v z)) v y) = (x' v y) ^ (y v z). [back_rewrite(1452),rewrite([2302(2),2302(4),2302(8),20(7),2302(10)])]. given #106 (T,wt=9): 4356 (x ^ y) ^ y = x ^ y. [para(4263(a,1),2427(a,1,2))]. given #107 (T,wt=9): 4357 x ^ (y ^ x) = y ^ x. [para(4263(a,1),2579(a,1,1))]. given #108 (T,wt=10): 3999 (x ^ y)' = x' v y'. [back_rewrite(2325),rewrite([3465(3)])]. given #109 (T,wt=11): 4034 ((x ^ y) v (y ^ z)) v y = y. [back_rewrite(2021),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3)])]. given #110 (A,wt=14): 3338 (x' ^ y) v (x' v x) = x' v x. [back_rewrite(2581),rewrite([3322(9),3322(9),2302(8),2325(7),2302(6),2426(8),27(5),2291(4),3018(5),20(3),2302(4)])]. given #111 (T,wt=11): 4302 (x' v y') ^ y' = y'. [back_rewrite(3801),rewrite([4263(7)]),flip(a)]. given #112 (T,wt=8): 4394 (x' v y) ^ y = y. [para(2291(a,1),4302(a,1,1,2)),rewrite([2291(4),2291(5)])]. given #113 (T,wt=7): 4409 (x v y) ^ y = y. [para(2291(a,1),4394(a,1,1,1))]. given #114 (T,wt=7): 4427 x ^ (y v x) = x. [para(4409(a,1),2928(a,1,1)),rewrite([4409(4)])]. given #115 (A,wt=30): 3467 ((((x v y) ^ z) v (z ^ u')) ^ w) v (z ^ ((z ^ ((x v y) v (x' ^ y'))) v u)) = z. [para(2302(a,1),46(a,1,1,1,2)),rewrite([3465(2),27(2),3465(8),27(6),2325(4),3465(3),2291(2),2291(2),2291(3),27(5),2291(4),3465(6),27(6),2325(3),3465(2),27(2),2325(8),3465(7),2291(8),3465(15),2325(14),3465(13),2291(12),2291(12),27(13),3465(16),27(17),27(13),2325(18),3465(17),2291(16),2291(16),3465(19),27(18),2291(12),2325(16),3465(15),2325(14),3465(13),2291(12),2291(12),27(13),2291(18),3465(18),27(19),2325(18),3465(17),27(18),27(14),2325(19),3465(18),2291(17),2291(17),3465(22),27(11),2325(9),3465(8),27(6),2325(4),3465(3),2291(2),2291(2),2291(3),27(5),2291(4),2291(7),27(18),2291(8),2325(16),3465(15),27(14),2291(8),2325(12),3465(11),2325(10),3465(9),2291(8),2291(8),27(9),2291(14)])]. given #116 (T,wt=9): 4425 x v (y v x) = y v x. [para(4409(a,1),2329(a,1,1))]. given #117 (T,wt=9): 4426 (x v y) v y = x v y. [para(4409(a,1),3847(a,1,2))]. given #118 (T,wt=11): 4381 ((x ^ y) v (x ^ z)) v x = x. [para(2928(a,1),4034(a,1,1,1))]. given #119 (T,wt=11): 4382 x v ((y ^ x) v (x ^ z)) = x. [para(4034(a,1),3325(a,1,1)),rewrite([4034(8)])]. given #120 (A,wt=36): 3469 ((((x ^ y') ^ z') v (z' ^ u)) ^ w) v (z' ^ ((z' ^ ((x ^ y') v (x' v y))) v u')) = z'. [para(2302(a,1),48(a,1,1,1,1,1)),rewrite([3465(5),2291(5),3465(6),27(4),27(3),2291(2),27(7),2291(7),3465(8),27(8),2325(5),3465(4),2325(3),3465(2),2291(3),2291(4),2325(6),3465(5),2291(5),3465(14),2291(15),3465(16),2291(11),27(15),2325(12),3465(11),2291(12),27(14),2291(13),3465(16),27(16),2325(16),3465(15),27(13),2291(12),2325(15),3465(14),2291(15),3465(19),2291(10),27(18),2325(16),3465(15),2291(10),27(14),2325(11),3465(10),2291(11),27(13),2291(12),2291(16),3465(17),27(9),2325(7),3465(6),27(4),27(3),2291(2),27(7),2291(7),2291(9),27(17),2325(17),3465(16),27(16),2325(16),3465(15),27(13),2291(12),2325(15),3465(14),2291(15)])]. given #121 (T,wt=11): 4383 ((x ^ y) v (z ^ y)) v y = y. [para(4357(a,1),4034(a,1,1,2))]. given #122 (T,wt=11): 4476 x v ((x ^ y) v (x ^ z)) = x. [para(4381(a,1),3325(a,1,1)),rewrite([4381(8)])]. given #123 (T,wt=11): 4477 ((x ^ y) v (z ^ x)) v x = x. [para(4357(a,1),4381(a,1,1,2))]. given #124 (T,wt=11): 4508 x v ((y ^ x) v (z ^ x)) = x. [para(4357(a,1),4382(a,1,2,2))]. given #125 (A,wt=35): 3470 ((((x ^ y) ^ z') v (z' ^ u')) ^ w) v (z' ^ ((z' ^ ((x ^ y) v (x' v y'))) v u)) = z'. [para(2302(a,1),48(a,1,1,1,2)),rewrite([3465(1),2291(6),3465(6),27(5),27(4),2291(2),2291(2),27(5),3465(8),27(8),2325(4),3465(3),2325(2),3465(1),2291(5),2325(8),3465(7),2291(6),2291(6),3465(12),3465(16),2291(11),27(15),2325(11),3465(10),27(16),2291(14),2291(14),3465(17),27(16),2325(16),3465(15),27(14),2291(12),2291(12),2325(13),3465(12),2291(18),3465(18),2291(10),27(17),2325(16),3465(15),2291(10),27(14),2325(10),3465(9),27(15),2291(13),2291(13),3465(18),27(9),2325(7),3465(6),27(5),27(4),2291(2),2291(2),27(5),2291(9),27(18),2325(18),3465(17),27(16),2325(16),3465(15),27(14),2291(12),2291(12),2325(13),3465(12),2291(18)])]. given #126 (T,wt=11): 4543 x v ((x ^ y) v (z ^ x)) = x. [para(4357(a,1),4476(a,1,2,2))]. given #127 (T,wt=12): 4068 (x ^ y) v (y ^ (x v x')) = y. [back_rewrite(1717),rewrite([3465(1),3465(5),2291(5),3465(6),27(7),2291(7),3465(8),27(4),2291(2),2291(2),27(6),2291(3),3999(4),2291(3)])]. given #128 (T,wt=11): 4586 (x v x') v y = x v x'. [para(2579(a,1),4068(a,1,2)),rewrite([3553(7)]),flip(a)]. given #129 (T,wt=8): 4603 (x v x') ^ y = y. [para(4586(a,1),4409(a,1,1))]. given #130 (A,wt=32): 3476 x' v ((x' v y') ^ (((x' v y') ^ ((z' v x') v (z ^ x))) v u)) = x' v y'. [back_rewrite(3464),rewrite([3465(1),3465(4),3465(8),3465(11),2325(8),3465(7),27(13),2291(11),2291(11),3465(14),27(4),2291(2),2291(2),27(12),2325(11),3465(10),27(5),2291(3),2291(3),27(8),27(6),2291(4),2291(4),2325(5),3465(4),3465(12),27(13),2325(3),3465(2),2325(14),3465(13),27(12),2325(6),3465(5),2325(13),3465(12),2325(9),3465(8),27(14),2291(12),2291(12),2291(15),3465(17)])]. given #131 (T,wt=8): 4604 x ^ (y v y') = x. [para(4586(a,1),4427(a,1,2))]. NOTE: New constant: x v x' = c_0. [new_symbol(4729)]. NOTE: New Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c_0, ^, v, f, ' ]). given #132 (T,wt=5): 4783 x ^ c_0 = x. [back_rewrite(4604),rewrite([4781(2)])]. given #133 (T,wt=5): 4784 c_0 ^ x = x. [back_rewrite(4603),rewrite([4781(2)])]. given #134 (T,wt=5): 4785 x v c_0 = c_0. [back_rewrite(4589),rewrite([4781(2),4781(4)])]. given #135 (A,wt=77): 3486 ((x v ((x v ((x v (y' ^ y)) ^ z)) ^ u)) ^ w) v ((x v ((x v (y' ^ y)) ^ z)) ^ (((x v ((x v (y' ^ y)) ^ z)) ^ ((((y' v x) ^ (x v z')) v v5') v (((y ^ x') v (x' ^ z)) ^ v5))) v u')) = x v ((x v (y' ^ y)) ^ z). [back_rewrite(3454),rewrite([3465(5),2291(5),3465(6),2291(4),27(5),2291(5),3465(6),27(6),2325(6),3465(5),2291(5),3465(9),2291(3),27(8),2325(6),3465(5),2291(3),27(4),2291(4),2291(6),3465(7),27(7),2325(7),3465(6),27(6),2325(6),3465(5),2291(5),3465(12),2291(2),27(11),2325(9),3465(8),2291(2),27(7),2325(5),3465(4),2291(2),27(3),2291(3),2291(5),2291(7),3465(8),27(8),2325(8),3465(7),27(7),2325(7),3465(6),27(6),2325(6),3465(5),2291(5),3465(18),2291(18),3465(19),2291(17),27(18),2291(18),3465(19),27(19),2325(19),3465(18),2291(18),3465(22),2291(16),27(21),2325(19),3465(18),2291(16),27(17),2291(17),2291(19),3465(23),2291(23),3465(24),2291(22),27(23),2291(23),3465(24),27(24),2325(24),3465(23),2291(23),3465(27),2291(21),27(26),2325(24),3465(23),2291(21),27(22),2291(22),2291(24),3465(28),2291(28),3465(29),27(27),2291(26),27(29),2291(29),3465(34),2291(34),3465(35),27(33),2291(32),27(35),2291(35),3465(36),27(36),2325(33),3465(32),2291(33),2325(35),3465(34),2291(34),3465(38),2325(31),3465(30),27(30),2325(27),3465(26),2291(27),2325(29),3465(28),2291(28),27(39),2325(37),3465(36),27(34),2291(33),27(36),2291(36),2291(38),3465(39),27(25),2325(25),3465(24),27(24),2325(24),3465(23),2291(23),27(42),27(35),2325(33),3465(32),27(30),2291(29),27(32),2291(32),2291(34),2325(40),3465(39),27(39),2325(36),3465(35),2291(36),2325(38),3465(37),2291(37),3465(43),27(43),2325(28),3465(27),2291(21),27(26),2325(24),3465(23),2291(21),27(22),2291(22),2291(24),2325(39),3465(38),2325(31),3465(30),27(30),2325(27),3465(26),2291(27),2325(29),3465(28),2291(28),27(39),2325(37),3465(36),27(34),2291(33),27(36),2291(36),2291(38),3465(42),27(20),2325(20),3465(19),27(19),2325(19),3465(18),2291(18),27(45),2325(43),3465(42),27(28),2325(28),3465(27),27(27),2325(27),3465(26),2291(26),27(45),27(38),2325(36),3465(35),27(33),2291(32),27(35),2291(35),2291(37),2325(43),3465(42),27(42),2325(39),3465(38),2291(39),2325(41),3465(40),2291(40),2291(47),3465(48),27(15),2325(13),3465(12),2291(2),27(11),2325(9),3465(8),2291(2),27(7),2325(5),3465(4),2291(2),27(3),2291(3),2291(5),2291(7),2291(9),27(42),2325(17),3465(16),2291(10),27(15),2325(13),3465(12),2291(10),27(11),2291(11),2291(13),2325(38),3465(37),27(37),2325(22),3465(21),2291(15),27(20),2325(18),3465(17),2291(15),27(16),2291(16),2291(18),2325(33),3465(32),2325(25),3465(24),27(24),2325(21),3465(20),2291(21),2325(23),3465(22),2291(22),27(33),2325(31),3465(30),27(28),2291(27),27(30),2291(30),2291(32),3465(41),2291(41),3465(42),2291(40),27(41),2291(41),3465(42),27(42),2325(42),3465(41),2291(41),3465(45),2291(39),27(44),2325(42),3465(41),2291(39),27(40),2291(40),2291(42)])]. given #136 (T,wt=5): 4786 c_0 v x = c_0. [back_rewrite(4586),rewrite([4781(2),4781(4)])]. given #137 (T,wt=6): 4781 x v x' = c_0. [new_symbol(4729)]. ============================== PROOF ================================= % Proof 2 at 1.78 (+ 0.01) seconds: one. % Length of proof is 100. % Level of proof is 20. % Maximum clause weight is 77. % Given clauses 137. 3 f(x,f(x,x)) = f(y,f(y,y)) # answer(one) # label(non_clause) # label(goal). [goal]. 5 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z))) = y # label(OL_Sh). [assumption]. 6 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 7 f(f(x,x),f(y,y)) = x v y. [copy(6),flip(a)]. 8 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. 9 f(f(x,y),f(x,y)) = x ^ y. [copy(8),flip(a)]. 10 x' = f(x,x) # label(definition_complementation). [assumption]. 11 f(x,x) = x'. [copy(10),flip(a)]. 16 f(c6,f(c6,c6)) != f(c7,f(c7,c7)) # answer(one). [deny(3)]. 17 f(c7,c7') != f(c6,c6') # answer(one). [copy(16),rewrite([11(4),11(8)]),flip(a)]. 20 f(x,y)' = x ^ y. [back_rewrite(9),rewrite([11(3)])]. 21 f(x',y') = x v y. [back_rewrite(7),rewrite([11(1),11(2)])]. 22 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(x',x)),z))) = y. [back_rewrite(5),rewrite([11(5)])]. 25 x ^ x = x''. [para(11(a,1),20(a,1,1)),flip(a)]. 27 (x v y)' = x' ^ y'. [para(21(a,1),20(a,1,1))]. 28 f(x ^ y,z') = f(x,y) v z. [para(20(a,1),21(a,1,1))]. 29 f(x',y ^ z) = x v f(y,z). [para(20(a,1),21(a,1,2))]. 30 f(f(f(x',f(x,y)),z),f(x,f(f(x,f(x',x)),y))) = x. [para(11(a,1),22(a,1,1,1,1))]. 31 f(f(f(f(x,y),y'),z),f(y,f(f(y,f(x',x)),y))) = y. [para(11(a,1),22(a,1,1,1,2))]. 32 f(f(x'',y),f(x,f(f(x,f(x',x)),x))) = x. [para(11(a,1),22(a,1,1,1)),rewrite([11(1)])]. 34 f(f(f(f(x,f(x',x)),f(f(x',x),y)),z),f(f(x',x),f(x' ^ x,y))) = f(x',x). [para(11(a,1),22(a,1,2,2,1)),rewrite([20(13)])]. 35 f(f(f(f(x,y),f(y,f(y,f(x',x)))),z),f(y,y ^ f(x',x))) = y. [para(11(a,1),22(a,1,2,2)),rewrite([20(11)])]. 36 f(f(f(x,y),f(y,z)),u) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(22(a,1),20(a,1,1)),flip(a)]. 43 f(f(x,y),f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z',z)),u)))) = x. [para(22(a,1),22(a,1,1,1)),rewrite([20(5)])]. 53 f(x' ^ f(x,y),f(x,f(f(x,f(x',x)),y))) = x. [para(11(a,1),30(a,1,1)),rewrite([20(4)])]. 62 f(x,f(f(x,y),f(f(f(x,y),x' v x),z))) = f(x,y). [para(30(a,1),22(a,1,1)),rewrite([21(6)])]. 67 f(f(f((x ^ y)',f(x,y) v z),u),f(x ^ y,f(f(x ^ y,(x ^ y) v f(x,y)),z'))) = x ^ y. [para(28(a,1),30(a,1,1,1,2)),rewrite([29(12)])]. 75 f(x''',f(x,f(f(x,f(x',x)),x))) = x. [para(11(a,1),32(a,1,1))]. 76 f(x'',y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(32(a,1),20(a,1,1)),flip(a)]. 78 f(x' v y,f(x,f(f(x,f(x',x)),x))) = x. [para(21(a,1),32(a,1,1))]. 87 f(x,f(x',f(f(x',x' v x),y))) = x'. [para(32(a,1),30(a,1,1)),rewrite([21(6)])]. 89 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(75(a,1),20(a,1,1)),flip(a)]. 97 (x' v y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(78(a,1),20(a,1,1)),flip(a)]. 105 f(f(x,y) ^ y',f(y,f(f(y,f(x',x)),y))) = y. [para(11(a,1),31(a,1,1)),rewrite([20(4)])]. 107 f(f(f(x,y),y'),z) ^ f(y,f(f(y,f(x',x)),y)) = y'. [para(31(a,1),20(a,1,1)),flip(a)]. 140 f(x',f(x'',x)) = x''. [para(32(a,1),87(a,1,2,2))]. 144 f(x'',x'' v x) = x'''. [para(21(a,1),140(a,1,2))]. 256 (x'' v y) ^ f(x',f(f(x',x' v x),x')) = x''. [para(21(a,1),97(a,1,2,2,1,2))]. 281 f(x,f(f(x,y),f(x,y) ^ (x' v x))) = f(x,y). [para(30(a,1),35(a,1,1)),rewrite([21(6)])]. 346 f(x,f(x',x' v x)) = x'. [para(281(a,1),87(a,1,2))]. 357 f(f(x,y),f(x ^ y,(x ^ y) v f(x,y))) = x ^ y. [para(20(a,1),346(a,1,2,1)),rewrite([20(4),20(9)])]. 380 f(x,y) ^ f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z',z)),u))) = x'. [para(22(a,1),36(a,1,1,1)),rewrite([20(5)])]. 521 f(x''',y) ^ f(x',f(f(x',x' v x),x')) = x''. [para(21(a,1),76(a,1,2,2,1,2))]. 673 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),62(a,1,2,2))]. 689 f(x,f(f(x,y),x' v x)) = f(x,y). [para(281(a,1),62(a,1,2))]. 770 f(x''',f(x,x'''' v x''')) = x. [para(75(a,1),689(a,1,2,1)),rewrite([75(22)])]. 832 x' ^ f(f(x',f(x,y)),x) = x' ^ f(x,y). [para(673(a,1),20(a,1,1)),rewrite([20(4)]),flip(a)]. 834 f(x'',f(f(x'',x v y),x')) = f(x'',x v y). [para(21(a,1),673(a,1,2,1,2)),rewrite([21(14)])]. 863 f((f(x,y) ^ y')',f(f((f(x,y) ^ y')',y),f(x,y) ^ y')) = f((f(x,y) ^ y')',y). [para(105(a,1),673(a,1,2,1,2)),rewrite([105(27)])]. 930 (x' ^ f(x,y))' ^ f(f((x' ^ f(x,y))',x),x' ^ f(x,y)) = (x' ^ f(x,y))' ^ x. [para(53(a,1),832(a,1,2,1,2)),rewrite([53(27)])]. 988 f(f(f(x,x ^ (x'''' v x''')),y),f(f(x,x'''' v x'''),f(f(f(x,x'''' v x'''),x''' v x''),f(x,x'''' v x''')))) = f(x,x'''' v x'''). [para(770(a,1),31(a,1,1,1,1)),rewrite([20(10),21(37)])]. 1626 f(f(x,y),f(y,y ^ f(x',x))) = y. [para(43(a,1),35(a,1,1))]. 1658 f(x,x ^ y) = f(x,y). [para(43(a,1),62(a,1,2,2)),rewrite([11(3),20(2)])]. 1677 (x ^ y) ^ f(f(x ^ y,x),f(x,y)) = (x ^ y) ^ x. [para(43(a,1),832(a,1,2,1,2)),rewrite([20(2),20(3),20(8),43(23)])]. 1717 f(f(x,y),f(y,f(x',x))) = y. [back_rewrite(1626),rewrite([1658(5)])]. 1758 f(f(f(x,x'''' v x'''),y),f(f(x,x'''' v x'''),f(f(f(x,x'''' v x'''),x''' v x''),f(x,x'''' v x''')))) = f(x,x'''' v x'''). [back_rewrite(988),rewrite([1658(10)])]. 2013 f(f(x'',y),x') = x. [para(32(a,1),1658(a,2)),rewrite([76(12)])]. 2014 x'' v x = x. [para(75(a,1),1658(a,2)),rewrite([89(12),21(5)])]. 2017 f(f(f(f(x,y),y'),z),y') = y. [para(31(a,1),1658(a,2)),rewrite([107(14)])]. 2022 f(x'',x) = x'''. [para(144(a,1),1658(a,2)),rewrite([2014(7),1658(6)])]. 2063 f(f(x,y),x') = x. [para(43(a,1),1658(a,2)),rewrite([380(17)])]. 2085 f(x'',x v y) = x'''. [back_rewrite(834),rewrite([2013(8),2022(3)]),flip(a)]. 2291 x'' = x. [para(11(a,1),2063(a,1,1)),rewrite([11(3)])]. 2302 f(x,y') = x' v y. [para(78(a,1),2063(a,1,1)),rewrite([27(3),2291(2),1658(3)])]. 2310 f(f((x ^ f(x',x)) v x,y),f(f(x',x),f(x' ^ x,x))) = f(x',x). [para(2063(a,1),34(a,1,1,1,2)),rewrite([2302(5),20(4),2291(11)])]. 2325 (x ^ y)' = f(x,y). [para(357(a,1),2063(a,1,1)),rewrite([20(3),11(3)])]. 2329 (x ^ y) v x = x. [para(62(a,1),2063(a,1,1)),rewrite([2302(3),20(2)])]. 2426 f(x,x v y) = x'. [back_rewrite(2085),rewrite([2291(2),2291(4)])]. 2451 f(f(x',y),x) = x'. [back_rewrite(1758),rewrite([2291(2),2291(2),2291(2),2426(3),2291(4),2291(4),2291(4),2426(5),2291(5),2291(5),2291(5),2426(6),2291(6),2291(7),2426(7),2291(5),2291(5),2291(5),2291(5),2426(6),2302(5),2426(6),2291(4),2291(5),2291(5),2291(5),2426(6)])]. 2564 f(x',y) ^ x = x. [back_rewrite(521),rewrite([2291(2),2426(7),2291(5),2302(5),2426(6),2291(4),2291(5)])]. 2579 (x v y) ^ x = x. [back_rewrite(256),rewrite([2291(2),2426(6),2291(4),2302(4),2426(5),2291(3),2291(4)])]. 2602 x ^ x = x. [back_rewrite(25),rewrite([2291(3)])]. 2617 (((x ^ y) v y) ^ z) v y = y. [back_rewrite(2017),rewrite([2302(3),20(2),2302(5),20(4)])]. 2789 f(f(x ^ y,z),f(x,y)) = x ^ y. [back_rewrite(67),rewrite([2325(2),2426(4),20(2),2426(8),2325(5),2302(6),20(5),2426(6),2325(4)])]. 2794 c7' v c7 != c6' v c6 # answer(one). [back_rewrite(17),rewrite([2302(4),2302(8)])]. 2842 f(x',f(x,y)) = x. [back_rewrite(930),rewrite([2325(4),2325(7),2451(7),1658(8),2602(7),2325(7),2564(7)])]. 2848 f((x ^ y) v y,f(f((x ^ y) v y,y),f(x,y) ^ y')) = f((x ^ y) v y,y). [back_rewrite(863),rewrite([2325(4),2302(3),20(2),2325(6),2302(5),20(4),2325(14),2302(13),20(12)])]. 2885 f(f(x,y),f(f(x',x),f(x' ^ x,x))) = f(x',x). [back_rewrite(2310),rewrite([2329(4)])]. 2928 (x ^ y) ^ x = x ^ y. [back_rewrite(1677),rewrite([2789(5),2602(3)]),flip(a)]. 3018 f(x,y ^ z) = x' v f(y,z). [para(2291(a,1),29(a,1,1))]. 3035 f((x ^ y) v y,y) = f(x,y) ^ y'. [back_rewrite(2848),rewrite([3018(9),20(6),2302(8),20(7),2329(8),11(5),27(3),2325(2)]),flip(a)]. 3327 f(f(x,y),f(x ^ y,z)) = x ^ y. [para(2325(a,1),2842(a,1,1))]. 3376 (x ^ y) v f(x',x) = f(x',x). [back_rewrite(2885),rewrite([3327(7),3018(4),20(2)])]. 3465 f(x,y) = x' v y'. [para(2291(a,1),2302(a,1,2))]. 3553 (x ^ y) v (x v x') = x v x'. [back_rewrite(3376),rewrite([3465(3),2291(3),3465(6),2291(6)])]. 3801 ((x' v y') ^ y') v y' = (x' v y') ^ y'. [back_rewrite(3035),rewrite([3465(3),27(3),2325(2),3465(1),3465(8)])]. 3999 (x ^ y)' = x' v y'. [back_rewrite(2325),rewrite([3465(3)])]. 4068 (x ^ y) v (y ^ (x v x')) = y. [back_rewrite(1717),rewrite([3465(1),3465(5),2291(5),3465(6),27(7),2291(7),3465(8),27(4),2291(2),2291(2),27(6),2291(3),3999(4),2291(3)])]. 4263 (x ^ y) v y = y. [para(2579(a,1),2617(a,1,1))]. 4302 (x' v y') ^ y' = y'. [back_rewrite(3801),rewrite([4263(7)]),flip(a)]. 4394 (x' v y) ^ y = y. [para(2291(a,1),4302(a,1,1,2)),rewrite([2291(4),2291(5)])]. 4409 (x v y) ^ y = y. [para(2291(a,1),4394(a,1,1,1))]. 4427 x ^ (y v x) = x. [para(4409(a,1),2928(a,1,1)),rewrite([4409(4)])]. 4586 (x v x') v y = x v x'. [para(2579(a,1),4068(a,1,2)),rewrite([3553(7)]),flip(a)]. 4603 (x v x') ^ y = y. [para(4586(a,1),4409(a,1,1))]. 4604 x ^ (y v y') = x. [para(4586(a,1),4427(a,1,2))]. 4729 x v x' = y v y'. [para(4604(a,1),4603(a,1))]. 4781 x v x' = c_0. [new_symbol(4729)]. 4855 x' v x = c_0. [para(2291(a,1),4781(a,1,2))]. 4942 $F # answer(one). [back_rewrite(2794),rewrite([4855(4),4855(5)]),xx(a)]. ============================== end of proof ========================== restricted denial: (wt=17): 4941 c9' v (c8' v c10') != c8' v (c9' v c10') # answer(combined). [back_rewrite(3806),rewrite([4855(21),4855(22)]),xx(b)]. % Disable descendants (x means already disabled): 16x 17x 2794x given #138 (T,wt=6): 4855 x' v x = c_0. [para(2291(a,1),4781(a,1,2))]. given #139 (T,wt=7): 4853 x' ^ x = c_0'. [para(4781(a,1),27(a,1,1)),rewrite([2291(5)]),flip(a)]. given #140 (A,wt=58): 3507 (((x' v y') ^ (y' v z')) v u') ^ (((w ^ (((x' v y') ^ (y' v z')) v u')) v y') ^ v5) = ((w ^ (((x' v y') ^ (y' v z')) v u')) v y') ^ v5. [back_rewrite(3432),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(4),27(4),2325(2),3465(1),2325(5),3465(4),3465(10),3465(13),3465(16),27(13),2291(11),2291(11),27(14),2291(12),2291(12),3465(13),27(13),2325(11),3465(10),2325(14),3465(13),3465(19),27(20),2325(18),3465(17),27(14),2291(12),2291(12),27(15),2291(13),2291(13),2291(15),3465(16),27(16),2291(11),2325(14),3465(13),27(13),2325(11),3465(10),2325(14),3465(13),3465(24),3465(27),3465(30),27(27),2291(25),2291(25),27(28),2291(26),2291(26),3465(27),27(27),2325(25),3465(24),2325(28),3465(27),3465(33),27(34),2325(32),3465(31),27(28),2291(26),2291(26),27(29),2291(27),2291(27),2291(29),3465(30),27(30),2291(25),2325(28),3465(27),27(27),2325(25),3465(24),2325(28),3465(27)])]. given #141 (T,wt=6): 4993 c_0' v x = x. [para(4853(a,1),4263(a,1,1))]. given #142 (T,wt=6): 4994 x v c_0' = x. [para(4853(a,1),4358(a,1,2))]. given #143 (T,wt=7): 4943 x ^ x' = c_0'. [para(4855(a,1),27(a,1,1)),rewrite([2291(4)]),flip(a)]. given #144 (T,wt=7): 4995 c_0' ^ x = c_0'. [para(4853(a,1),4356(a,1,1)),rewrite([4853(5)])]. given #145 (A,wt=17): 3510 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [back_rewrite(3428),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(5),3465(8),3465(11),27(8),2291(6),2291(6),27(9),2291(7),2291(7)])]. given #146 (T,wt=7): 4996 x ^ c_0' = c_0'. [para(4853(a,1),4357(a,1,2)),rewrite([4853(5)])]. given #147 (T,wt=11): 4854 (x v y) v (x' ^ y') = c_0. [para(27(a,1),4781(a,1,2))]. given #148 (T,wt=11): 4856 (x ^ y) v (x' v y') = c_0. [para(3999(a,1),4781(a,1,2))]. given #149 (T,wt=11): 4944 (x' ^ y') v (x v y) = c_0. [para(27(a,1),4855(a,1,1))]. given #150 (A,wt=21): 3511 x ^ (((y ^ x) v (x ^ z)) ^ u) = ((y ^ x) v (x ^ z)) ^ u. [back_rewrite(3426),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(6),3465(9),3465(12),27(9),2291(7),2291(7),27(10),2291(8),2291(8)])]. given #151 (T,wt=11): 4945 (x' v y') v (x ^ y) = c_0. [para(3999(a,1),4855(a,1,1))]. given #152 (T,wt=11): 5087 (x' v y) v (x ^ y') = c_0. [para(2291(a,1),4854(a,1,2,1))]. given #153 (T,wt=11): 5088 (x v y') v (x' ^ y) = c_0. [para(2291(a,1),4854(a,1,2,2))]. given #154 (T,wt=11): 5094 (x' ^ y) v (x v y') = c_0. [para(2291(a,1),4856(a,1,2,1))]. given #155 (A,wt=69): 3527 (((x' ^ (y ^ z)) v ((y ^ z) ^ u)) ^ w) v ((y ^ z) ^ (((y ^ z) ^ ((v5' v (((x' ^ (y ^ z)) v ((y ^ z) ^ u)) ^ w)) v (v5 ^ (((x v (y' v z')) ^ ((y' v z') v u')) v w')))) v v6')) = y ^ z. [back_rewrite(3408),rewrite([3465(1),3465(6),2325(6),3465(5),3465(10),27(5),27(5),2291(3),2291(3),27(9),27(7),2291(5),2291(5),2291(6),3465(7),27(7),2325(4),3465(3),2291(2),2325(2),3465(1),2325(7),3465(6),2325(6),3465(5),3465(15),3465(20),2325(20),3465(19),3465(24),27(19),27(19),2291(17),2291(17),27(23),27(21),2291(19),2291(19),2291(20),3465(21),27(21),2325(18),3465(17),2291(16),2325(16),3465(15),2325(21),3465(20),2325(20),3465(19),3465(28),3465(33),2325(33),3465(32),3465(37),27(32),27(32),2291(30),2291(30),27(36),27(34),2291(32),2291(32),2291(33),3465(34),27(34),2325(31),3465(30),2291(29),2325(29),3465(28),2325(34),3465(33),2325(33),3465(32),3465(40),27(41),2325(39),3465(38),27(33),27(33),2291(31),2291(31),27(37),27(35),2291(33),2291(33),2291(34),2291(36),3465(37),2325(28),3465(27),27(28),2325(26),3465(25),27(20),27(20),2291(18),2291(18),27(24),27(22),2291(20),2291(20),2291(21),2291(23),27(33),2291(25),2325(31),3465(30),27(30),2325(27),3465(26),2291(25),2325(25),3465(24),2325(30),3465(29),2325(29),3465(28),3465(38),2325(15),3465(14),27(40),27(26),2291(18),2325(24),3465(23),27(23),2325(20),3465(19),2291(18),2325(18),3465(17),2325(23),3465(22),2325(22),3465(21),2325(43),3465(42),27(43),2325(41),3465(40),27(35),27(35),2291(33),2291(33),27(39),27(37),2291(35),2291(35),2291(36),2291(38),3465(41),27(41),27(17),2291(15),2291(15),2325(38),3465(37),2325(28),3465(27),27(28),2325(26),3465(25),27(20),27(20),2291(18),2291(18),27(24),27(22),2291(20),2291(20),2291(21),2291(23),27(33),2291(25),2325(31),3465(30),27(30),2325(27),3465(26),2291(25),2325(25),3465(24),2325(30),3465(29),2325(29),3465(28),3465(41),2325(14),3465(13),27(43),2325(41),3465(40),2325(17),3465(16),27(42),27(28),2291(20),2325(26),3465(25),27(25),2325(22),3465(21),2291(20),2325(20),3465(19),2325(25),3465(24),2325(24),3465(23),2325(45),3465(44),27(45),2325(43),3465(42),27(37),27(37),2291(35),2291(35),27(41),27(39),2291(37),2291(37),2291(38),2291(40),2291(44),3465(45),27(13),2325(11),3465(10),27(5),27(5),2291(3),2291(3),27(9),27(7),2291(5),2291(5),2291(6),2291(8),27(40),27(11),2291(9),2291(9),2325(37),3465(36),27(36),27(12),2291(10),2291(10),2325(33),3465(32),2325(23),3465(22),27(23),2325(21),3465(20),27(15),27(15),2291(13),2291(13),27(19),27(17),2291(15),2291(15),2291(16),2291(18),27(28),2291(20),2325(26),3465(25),27(25),2325(22),3465(21),2291(20),2325(20),3465(19),2325(25),3465(24),2325(24),3465(23)])]. given #156 (T,wt=11): 5095 (x ^ y') v (x' v y) = c_0. [para(2291(a,1),4856(a,1,2,2))]. given #157 (T,wt=12): 4992 (x' ^ y') ^ (x v y) = c_0'. [para(27(a,1),4853(a,1,1))]. given #158 (T,wt=12): 4997 (x' v y') ^ (x ^ y) = c_0'. [para(3999(a,1),4853(a,1,1))]. given #159 (T,wt=12): 5066 (x v y) ^ (x' ^ y') = c_0'. [para(27(a,1),4943(a,1,2))]. given #160 (A,wt=74): 3529 (((x v (y' v z')) ^ ((y' v z') v u')) v w') ^ ((y' v z') v (((y' v z') v ((((x v (y' v z')) ^ ((y' v z') v u')) v w') ^ (((x' ^ (y ^ z)) v ((y ^ z) ^ u)) ^ w))) ^ v5)) = y' v z'. [back_rewrite(3406),rewrite([3465(1),3465(6),2325(6),3465(5),3465(10),27(5),27(5),2291(3),2291(3),27(9),27(7),2291(5),2291(5),2291(6),3465(7),27(7),2325(4),3465(3),2291(2),2325(2),3465(1),2325(7),3465(6),2325(6),3465(5),3465(15),3465(20),2325(20),3465(19),3465(24),27(19),27(19),2291(17),2291(17),27(23),27(21),2291(19),2291(19),2291(20),3465(22),3465(27),2325(27),3465(26),3465(31),27(26),27(26),2291(24),2291(24),27(30),27(28),2291(26),2291(26),2291(27),3465(28),27(28),2325(25),3465(24),2291(23),2325(23),3465(22),2325(28),3465(27),2325(27),3465(26),3465(35),2325(15),3465(14),27(37),2325(24),3465(23),27(23),2325(20),3465(19),2291(18),2325(18),3465(17),2325(23),3465(22),2325(22),3465(21),27(41),2325(39),3465(38),27(33),27(33),2291(31),2291(31),27(37),27(35),2291(33),2291(33),2291(34),2291(36),3465(38),27(38),27(17),2291(15),2291(15),2325(35),3465(34),27(27),2325(25),3465(24),27(19),27(19),2291(17),2291(17),27(23),27(21),2291(19),2291(19),2291(20),2291(22),2325(29),3465(28),27(28),2325(25),3465(24),2291(23),2325(23),3465(22),2325(28),3465(27),2325(27),3465(26),3465(38),2325(14),3465(13),27(40),2325(38),3465(37),2325(17),3465(16),27(39),2325(26),3465(25),27(25),2325(22),3465(21),2291(20),2325(20),3465(19),2325(25),3465(24),2325(24),3465(23),27(43),2325(41),3465(40),27(35),27(35),2291(33),2291(33),27(39),27(37),2291(35),2291(35),2291(36),2291(38),2291(41),3465(43)])]. given #161 (T,wt=12): 5067 (x ^ y) ^ (x' v y') = c_0'. [para(3999(a,1),4943(a,1,2))]. given #162 (T,wt=12): 5100 ((x' ^ y) ^ z) v x' = x'. [back_rewrite(3683),rewrite([5094(10),4783(7),2427(8)])]. given #163 (T,wt=9): 5292 ((x ^ y) ^ z) v x = x. [para(2291(a,1),5100(a,1,1,1,1)),rewrite([2291(4),2291(5)])]. given #164 (T,wt=9): 5302 x v ((x ^ y) ^ z) = x. [para(5292(a,1),3325(a,1,1)),rewrite([5292(6)])]. given #165 (A,wt=66): 3531 (((x v (y' v z')) ^ ((y' v z') v u')) v w') ^ ((y' v z') v ((((x v (y' v z')) ^ ((y' v z') v u')) v w') ^ (((x' ^ (y ^ z)) v ((y ^ z) ^ u)) ^ w))) = y' v z'. [back_rewrite(3403),rewrite([3465(1),3465(6),2325(6),3465(5),3465(10),27(5),27(5),2291(3),2291(3),27(9),27(7),2291(5),2291(5),2291(6),3465(7),27(7),2325(4),3465(3),2291(2),2325(2),3465(1),2325(7),3465(6),2325(6),3465(5),3465(14),3465(19),2325(19),3465(18),3465(23),27(18),27(18),2291(16),2291(16),27(22),27(20),2291(18),2291(18),2291(19),3465(21),3465(26),2325(26),3465(25),3465(30),27(25),27(25),2291(23),2291(23),27(29),27(27),2291(25),2291(25),2291(26),3465(27),27(27),2325(24),3465(23),2291(22),2325(22),3465(21),2325(27),3465(26),2325(26),3465(25),3465(34),2325(14),3465(13),27(36),2325(23),3465(22),27(22),2325(19),3465(18),2291(17),2325(17),3465(16),2325(22),3465(21),2325(21),3465(20),27(40),2325(38),3465(37),27(32),27(32),2291(30),2291(30),27(36),27(34),2291(32),2291(32),2291(33),2291(35),3465(38)])]. given #166 (T,wt=9): 5303 ((x ^ y) ^ z) v y = y. [para(4357(a,1),5292(a,1,1,1))]. given #167 (T,wt=9): 5304 (x ^ (y ^ z)) v y = y. [para(4357(a,1),5292(a,1,1))]. given #168 (T,wt=9): 5312 x v ((y ^ x) ^ z) = x. [para(4357(a,1),5302(a,1,2,1))]. given #169 (T,wt=9): 5313 x v (y ^ (x ^ z)) = x. [para(4357(a,1),5302(a,1,2))]. given #170 (A,wt=57): 3535 (((x' ^ (y ^ z)) v ((y ^ z) ^ u)) ^ w) v ((y ^ z) ^ ((((x' ^ (y ^ z)) v ((y ^ z) ^ u)) ^ w) v (((x v (y' v z')) ^ ((y' v z') v u')) v w'))) = y ^ z. [back_rewrite(3399),rewrite([3465(1),3465(6),2325(6),3465(5),3465(10),27(5),27(5),2291(3),2291(3),27(9),27(7),2291(5),2291(5),2291(6),3465(7),27(7),2325(4),3465(3),2291(2),2325(2),3465(1),2325(7),3465(6),2325(6),3465(5),3465(14),3465(19),2325(19),3465(18),3465(23),27(18),27(18),2291(16),2291(16),27(22),27(20),2291(18),2291(18),2291(19),3465(21),3465(26),2325(26),3465(25),3465(30),27(25),27(25),2291(23),2291(23),27(29),27(27),2291(25),2291(25),2291(26),3465(27),27(27),2325(24),3465(23),2291(22),2325(22),3465(21),2325(27),3465(26),2325(26),3465(25),3465(34),2325(14),3465(13),27(36),2325(23),3465(22),27(22),2325(19),3465(18),2291(17),2325(17),3465(16),2325(22),3465(21),2325(21),3465(20),27(40),2325(38),3465(37),27(32),27(32),2291(30),2291(30),27(36),27(34),2291(32),2291(32),2291(33),2291(35),3465(37),27(13),2325(11),3465(10),27(5),27(5),2291(3),2291(3),27(9),27(7),2291(5),2291(5),2291(6),2291(8),27(32),27(11),2291(9),2291(9),2325(29),3465(28),27(21),2325(19),3465(18),27(13),27(13),2291(11),2291(11),27(17),27(15),2291(13),2291(13),2291(14),2291(16),2325(23),3465(22),27(22),2325(19),3465(18),2291(17),2325(17),3465(16),2325(22),3465(21),2325(21),3465(20)])]. given #171 (T,wt=9): 5357 (x ^ (y ^ z)) v z = z. [para(4357(a,1),5303(a,1,1))]. given #172 (T,wt=9): 5377 x v (y ^ (z ^ x)) = x. [para(4357(a,1),5312(a,1,2))]. given #173 (T,wt=11): 5291 ((x v y') v z') ^ x = x. [para(5100(a,1),27(a,1,1)),rewrite([2291(2),3999(4),3999(3),2291(2),2291(6)]),flip(a)]. given #174 (T,wt=10): 5448 ((x v y) v z') ^ x = x. [para(2291(a,1),5291(a,1,1,1,2))]. given #175 (A,wt=64): 3540 (((x' ^ (y ^ z)) v ((y ^ z) ^ u)) ^ w) v ((y ^ z) ^ (((y ^ z) ^ ((((x' ^ (y ^ z)) v ((y ^ z) ^ u)) ^ w) v (((x v (y' v z')) ^ ((y' v z') v u')) v w'))) v v5')) = y ^ z. [back_rewrite(3394),rewrite([3465(1),3465(6),2325(6),3465(5),3465(10),27(5),27(5),2291(3),2291(3),27(9),27(7),2291(5),2291(5),2291(6),3465(7),27(7),2325(4),3465(3),2291(2),2325(2),3465(1),2325(7),3465(6),2325(6),3465(5),3465(15),3465(20),2325(20),3465(19),3465(24),27(19),27(19),2291(17),2291(17),27(23),27(21),2291(19),2291(19),2291(20),3465(22),3465(27),2325(27),3465(26),3465(31),27(26),27(26),2291(24),2291(24),27(30),27(28),2291(26),2291(26),2291(27),3465(28),27(28),2325(25),3465(24),2291(23),2325(23),3465(22),2325(28),3465(27),2325(27),3465(26),3465(35),2325(15),3465(14),27(37),2325(24),3465(23),27(23),2325(20),3465(19),2291(18),2325(18),3465(17),2325(23),3465(22),2325(22),3465(21),27(41),2325(39),3465(38),27(33),27(33),2291(31),2291(31),27(37),27(35),2291(33),2291(33),2291(34),2291(36),3465(38),27(38),27(17),2291(15),2291(15),2325(35),3465(34),27(27),2325(25),3465(24),27(19),27(19),2291(17),2291(17),27(23),27(21),2291(19),2291(19),2291(20),2291(22),2325(29),3465(28),27(28),2325(25),3465(24),2291(23),2325(23),3465(22),2325(28),3465(27),2325(27),3465(26),3465(38),2325(14),3465(13),27(40),2325(38),3465(37),2325(17),3465(16),27(39),2325(26),3465(25),27(25),2325(22),3465(21),2291(20),2325(20),3465(19),2325(25),3465(24),2325(24),3465(23),27(43),2325(41),3465(40),27(35),27(35),2291(33),2291(33),27(39),27(37),2291(35),2291(35),2291(36),2291(38),2291(41),3465(42),27(13),2325(11),3465(10),27(5),27(5),2291(3),2291(3),27(9),27(7),2291(5),2291(5),2291(6),2291(8),27(37),27(11),2291(9),2291(9),2325(34),3465(33),27(33),27(12),2291(10),2291(10),2325(30),3465(29),27(22),2325(20),3465(19),27(14),27(14),2291(12),2291(12),27(18),27(16),2291(14),2291(14),2291(15),2291(17),2325(24),3465(23),27(23),2325(20),3465(19),2291(18),2325(18),3465(17),2325(23),3465(22),2325(22),3465(21)])]. given #176 (T,wt=9): 5477 ((x v y) v z) ^ x = x. [para(2291(a,1),5448(a,1,1,2))]. given #177 (T,wt=9): 5550 x ^ ((x v y) v z) = x. [para(5477(a,1),2928(a,1,1)),rewrite([5477(6)])]. given #178 (T,wt=9): 5554 ((x v y) v z) ^ y = y. [para(4425(a,1),5477(a,1,1,1))]. given #179 (T,wt=9): 5555 (x v (y v z)) ^ y = y. [para(4425(a,1),5477(a,1,1))]. given #180 (A,wt=38): 3542 (x ^ y) ^ (((x ^ y) ^ z) v ((((x ^ y) ^ z) v ((u' ^ (x ^ y)) ^ (u v (x' v y')))) ^ w)) = (x ^ y) ^ z. [back_rewrite(3391),rewrite([3465(3),2325(3),3465(2),3465(8),2325(8),3465(7),3465(15),3465(19),2325(15),3465(14),2291(13),2325(13),3465(12),27(20),27(20),2291(18),2291(18),3465(20),27(12),27(10),2291(8),2291(8),2291(9),27(17),27(13),27(13),2291(11),2291(11),2325(15),3465(14),2291(13),2325(13),3465(12),3465(18),27(18),2325(9),3465(8),2325(8),3465(7),2325(20),3465(19),2325(15),3465(14),2291(13),2325(13),3465(12),27(20),27(20),2291(18),2291(18),3465(23),27(7),27(5),2291(3),2291(3),2291(4),27(20),2325(18),3465(17),27(9),27(7),2291(5),2291(5),2291(6),27(14),27(10),27(10),2291(8),2291(8),2325(12),3465(11),2291(10),2325(10),3465(9),2291(16)])]. given #181 (T,wt=9): 5581 x ^ ((y v x) v z) = x. [para(4425(a,1),5550(a,1,2,1))]. given #182 (T,wt=9): 5582 x ^ (y v (x v z)) = x. [para(4425(a,1),5550(a,1,2))]. given #183 (T,wt=9): 5597 (x v (y v z)) ^ z = z. [para(4425(a,1),5554(a,1,1))]. given #184 (T,wt=9): 5663 x ^ (y v (z v x)) = x. [para(4425(a,1),5581(a,1,2))]. given #185 (A,wt=34): 3665 x' ^ ((x' ^ y) v (((x' ^ y) v (((z ^ u) ^ x') ^ ((z' v u') v x))) ^ w)) = x' ^ y. [back_rewrite(3227),rewrite([3465(3),2291(3),3465(5),2291(5),3465(9),3465(13),2325(9),3465(8),2325(7),3465(6),2291(10),27(14),27(13),2291(11),2291(11),3465(14),27(6),2291(6),27(14),27(10),27(9),2291(7),2291(7),2325(12),3465(11),2325(10),3465(9),2291(13),3465(15),27(15),2325(6),3465(5),2291(5),2325(14),3465(13),2325(9),3465(8),2325(7),3465(6),2291(10),27(14),27(13),2291(11),2291(11),3465(17),27(4),2291(4),27(17),2325(15),3465(14),27(6),2291(6),27(14),27(10),27(9),2291(7),2291(7),2325(12),3465(11),2325(10),3465(9),2291(13),2291(16)])]. given #186 (T,wt=11): 5301 (x ^ y) v (x v z) = x v z. [para(2579(a,1),5292(a,1,1,1))]. given #187 (T,wt=11): 5305 (x ^ y) v (z v x) = z v x. [para(4409(a,1),5292(a,1,1,1))]. given #188 (T,wt=11): 5311 (x v y) v (x ^ z) = x v y. [para(2579(a,1),5302(a,1,2,1))]. given #189 (T,wt=11): 5314 (x v y) v (y ^ z) = x v y. [para(4409(a,1),5302(a,1,2,1))]. given #190 (A,wt=41): 3785 ((x ^ y) v (y ^ z)) v (y ^ ((y ^ ((u' v ((x ^ y) v (y ^ z))) v (u ^ ((x' v y') ^ (y' v z'))))) v w')) = y. [back_rewrite(3059),rewrite([3465(1),3465(4),3465(8),3465(11),3465(17),3465(20),3465(23),27(20),2291(18),2291(18),27(21),2291(19),2291(19),3465(21),2325(16),3465(15),2325(16),3465(15),27(12),2291(10),2291(10),27(13),2291(11),2291(11),27(18),2291(14),27(16),2325(14),3465(13),2325(17),3465(16),3465(22),27(23),27(14),2291(10),27(12),2325(10),3465(9),2325(13),3465(12),2325(25),3465(24),2325(25),3465(24),27(21),2291(19),2291(19),27(22),2291(20),2291(20),3465(24),27(24),2291(9),2325(22),3465(21),2325(16),3465(15),2325(16),3465(15),27(12),2291(10),2291(10),27(13),2291(11),2291(11),27(18),2291(14),27(16),2325(14),3465(13),2325(17),3465(16),3465(25),27(26),2325(24),3465(23),27(24),27(15),2291(11),27(13),2325(11),3465(10),2325(14),3465(13),2325(26),3465(25),2325(26),3465(25),27(22),2291(20),2291(20),27(23),2291(21),2291(21),2291(26),3465(27),2325(8),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),27(23),2291(5),2325(21),3465(20),27(20),2291(5),2325(18),3465(17),2325(12),3465(11),2325(12),3465(11),27(8),2291(6),2291(6),27(9),2291(7),2291(7),27(14),2291(10),27(12),2325(10),3465(9),2325(13),3465(12)])]. given #191 (T,wt=11): 5367 (x ^ y) v (y v z) = y v z. [para(2579(a,1),5304(a,1,1,2))]. given #192 (T,wt=11): 5368 (x ^ y) v (z v y) = z v y. [para(4409(a,1),5304(a,1,1,2))]. given #193 (T,wt=11): 5383 (x v y) v (z ^ x) = x v y. [para(2579(a,1),5313(a,1,2,2))]. given #194 (T,wt=11): 5384 (x v y) v (z ^ y) = x v y. [para(4409(a,1),5313(a,1,2,2))]. given #195 (A,wt=45): 3790 (((x ^ y) v (y ^ z)) ^ u) v (((w' v (((x ^ y) v (y ^ z)) ^ u)) ^ y) v v5') = ((w' v (((x ^ y) v (y ^ z)) ^ u)) ^ y) v v5'. [back_rewrite(3053),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(5),3465(8),3465(11),27(8),2291(6),2291(6),27(9),2291(7),2291(7),3465(8),27(8),2325(6),3465(5),2325(9),3465(8),3465(14),27(15),2325(13),3465(12),27(9),2291(7),2291(7),27(10),2291(8),2291(8),2291(10),3465(11),27(11),2291(6),2325(9),3465(8),27(8),2325(6),3465(5),2325(9),3465(8),3465(17),27(17),2325(15),3465(14),27(15),2325(13),3465(12),27(9),2291(7),2291(7),27(10),2291(8),2291(8),2291(10),2291(12),3465(15),3465(18),3465(21),27(18),2291(16),2291(16),27(19),2291(17),2291(17),3465(18),27(18),2325(16),3465(15),2325(19),3465(18),3465(24),27(25),2325(23),3465(22),27(19),2291(17),2291(17),27(20),2291(18),2291(18),2291(20),3465(21),27(21),2291(16),2325(19),3465(18),27(18),2325(16),3465(15),2325(19),3465(18),3465(27),27(27),2325(25),3465(24),27(25),2325(23),3465(22),27(19),2291(17),2291(17),27(20),2291(18),2291(18),2291(20),2291(22)])]. given #196 (T,wt=11): 5548 (x v y) ^ (x ^ z) = x ^ z. [para(2329(a,1),5477(a,1,1,1))]. given #197 (T,wt=11): 5551 (x v y) ^ (z ^ x) = z ^ x. [para(4263(a,1),5477(a,1,1,1))]. given #198 (T,wt=11): 5578 (x ^ y) ^ (x v z) = x ^ y. [para(2329(a,1),5550(a,1,2,1))]. given #199 (T,wt=11): 5579 (x ^ y) ^ (y v z) = x ^ y. [para(4263(a,1),5550(a,1,2,1))]. given #200 (A,wt=26): 3818 x' v ((y' v x') ^ (x' v z')) = (y' v x') ^ (x' v z'). [back_rewrite(2991),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(4),27(5),2325(3),3465(2),2325(6),3465(5),3465(10),3465(13)])]. given #201 (T,wt=11): 5612 (x v y) ^ (y ^ z) = y ^ z. [para(2329(a,1),5555(a,1,1,2))]. given #202 (T,wt=11): 5614 (x v y) ^ (z ^ y) = z ^ y. [para(4263(a,1),5555(a,1,1,2))]. given #203 (T,wt=11): 5668 (x ^ y) ^ (z v x) = x ^ y. [para(2329(a,1),5582(a,1,2,2))]. given #204 (T,wt=11): 5669 (x ^ y) ^ (z v y) = x ^ y. [para(4263(a,1),5582(a,1,2,2))]. given #205 (A,wt=21): 3825 (((x ^ y) v (y ^ z)) ^ u) ^ y = ((x ^ y) v (y ^ z)) ^ u. [back_rewrite(2934),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(6),3465(9),3465(12),27(9),2291(7),2291(7),27(10),2291(8),2291(8)])]. given #206 (T,wt=11): 5730 (((x ^ y) ^ z) ^ u) v x = x. [para(5292(a,1),5301(a,1,2)),rewrite([5292(7)])]. given #207 (T,wt=11): 5731 (((x ^ y) ^ z) ^ u) v y = y. [para(5303(a,1),5301(a,1,2)),rewrite([5303(7)])]. given #208 (T,wt=11): 5732 ((x ^ (y ^ z)) ^ u) v y = y. [para(5304(a,1),5301(a,1,2)),rewrite([5304(7)])]. given #209 (T,wt=11): 5733 ((x ^ (y ^ z)) ^ u) v z = z. [para(5357(a,1),5301(a,1,2)),rewrite([5357(7)])]. given #210 (A,wt=45): 3828 (((x' v (((y ^ z) v (z ^ u)) ^ w)) ^ z) v v5') v (((y ^ z) v (z ^ u)) ^ w) = ((x' v (((y ^ z) v (z ^ u)) ^ w)) ^ z) v v5'. [back_rewrite(2931),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(4),27(4),2325(2),3465(1),2325(5),3465(4),3465(10),27(11),2325(9),3465(8),27(5),2291(3),2291(3),27(6),2291(4),2291(4),2291(6),3465(7),27(7),2291(2),2325(5),3465(4),27(4),2325(2),3465(1),2325(5),3465(4),3465(14),3465(17),3465(20),27(17),2291(15),2291(15),27(18),2291(16),2291(16),3465(17),27(17),2325(15),3465(14),2325(18),3465(17),3465(23),2325(14),3465(13),27(13),2325(11),3465(10),27(11),2325(9),3465(8),27(5),2291(3),2291(3),27(6),2291(4),2291(4),2291(6),2291(8),27(19),2325(17),3465(16),27(13),2291(11),2291(11),27(14),2291(12),2291(12),2291(14),3465(15),3465(18),3465(21),27(18),2291(16),2291(16),27(19),2291(17),2291(17),3465(18),27(18),2325(16),3465(15),2325(19),3465(18),3465(24),27(25),2325(23),3465(22),27(19),2291(17),2291(17),27(20),2291(18),2291(18),2291(20),3465(21),27(21),2291(16),2325(19),3465(18),27(18),2325(16),3465(15),2325(19),3465(18),3465(27),27(27),2325(25),3465(24),27(25),2325(23),3465(22),27(19),2291(17),2291(17),27(20),2291(18),2291(18),2291(20),2291(22)])]. given #211 (T,wt=11): 5761 x v (((x ^ y) ^ z) ^ u) = x. [para(5292(a,1),5311(a,1,1)),rewrite([5292(7)])]. given #212 (T,wt=11): 5762 x v (((y ^ x) ^ z) ^ u) = x. [para(5303(a,1),5311(a,1,1)),rewrite([5303(7)])]. given #213 (T,wt=11): 5763 x v ((y ^ (x ^ z)) ^ u) = x. [para(5304(a,1),5311(a,1,1)),rewrite([5304(7)])]. given #214 (T,wt=11): 5764 x v ((y ^ (z ^ x)) ^ u) = x. [para(5357(a,1),5311(a,1,1)),rewrite([5357(7)])]. given #215 (A,wt=58): 3829 (((x ^ (((y' v z') ^ (z' v u')) v w')) v z') ^ v5) ^ (((y' v z') ^ (z' v u')) v w') = ((x ^ (((y' v z') ^ (z' v u')) v w')) v z') ^ v5. [back_rewrite(2930),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(4),27(4),2325(2),3465(1),2325(5),3465(4),3465(10),27(11),2325(9),3465(8),27(5),2291(3),2291(3),27(6),2291(4),2291(4),2291(6),3465(7),27(7),2291(2),2325(5),3465(4),27(4),2325(2),3465(1),2325(5),3465(4),3465(14),3465(17),3465(20),27(17),2291(15),2291(15),27(18),2291(16),2291(16),3465(17),27(17),2325(15),3465(14),2325(18),3465(17),3465(24),3465(27),3465(30),27(27),2291(25),2291(25),27(28),2291(26),2291(26),3465(27),27(27),2325(25),3465(24),2325(28),3465(27),3465(33),27(34),2325(32),3465(31),27(28),2291(26),2291(26),27(29),2291(27),2291(27),2291(29),3465(30),27(30),2291(25),2325(28),3465(27),27(27),2325(25),3465(24),2325(28),3465(27)])]. given #216 (T,wt=11): 5823 (x ^ ((y ^ z) ^ u)) v y = y. [para(5292(a,1),5367(a,1,2)),rewrite([5292(7)])]. given #217 (T,wt=11): 5824 (x ^ ((y ^ z) ^ u)) v z = z. [para(5303(a,1),5367(a,1,2)),rewrite([5303(7)])]. given #218 (T,wt=11): 5825 (x ^ (y ^ (z ^ u))) v z = z. [para(5304(a,1),5367(a,1,2)),rewrite([5304(7)])]. given #219 (T,wt=11): 5826 (x ^ (y ^ (z ^ u))) v u = u. [para(5357(a,1),5367(a,1,2)),rewrite([5357(7)])]. given #220 (A,wt=26): 3845 ((x' v y') ^ (y' v z')) v y' = (x' v y') ^ (y' v z'). [back_rewrite(2849),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(4),27(4),2325(2),3465(1),2325(5),3465(4),3465(10),3465(13)])]. given #221 (T,wt=11): 5846 x v (y ^ ((x ^ z) ^ u)) = x. [para(5292(a,1),5383(a,1,1)),rewrite([5292(7)])]. given #222 (T,wt=11): 5847 x v (y ^ ((z ^ x) ^ u)) = x. [para(5303(a,1),5383(a,1,1)),rewrite([5303(7)])]. given #223 (T,wt=11): 5848 x v (y ^ (z ^ (x ^ u))) = x. [para(5304(a,1),5383(a,1,1)),rewrite([5304(7)])]. given #224 (T,wt=11): 5849 x v (y ^ (z ^ (u ^ x))) = x. [para(5357(a,1),5383(a,1,1)),rewrite([5357(7)])]. given #225 (A,wt=17): 3846 ((x ^ y) v (y ^ z)) ^ y = (x ^ y) v (y ^ z). [back_rewrite(2844),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(5),3465(8),3465(11),27(8),2291(6),2291(6),27(9),2291(7),2291(7)])]. given #226 (T,wt=11): 5918 (((x v y) v z) v u) ^ x = x. [para(5477(a,1),5548(a,1,2)),rewrite([5477(7)])]. given #227 (T,wt=11): 5919 (((x v y) v z) v u) ^ y = y. [para(5554(a,1),5548(a,1,2)),rewrite([5554(7)])]. given #228 (T,wt=11): 5920 ((x v (y v z)) v u) ^ y = y. [para(5555(a,1),5548(a,1,2)),rewrite([5555(7)])]. given #229 (T,wt=11): 5921 ((x v (y v z)) v u) ^ z = z. [para(5597(a,1),5548(a,1,2)),rewrite([5597(7)])]. given #230 (A,wt=49): 3887 (((x ^ y') v (y' ^ z')) ^ u) v (y' ^ ((y' ^ ((((x ^ y') v (y' ^ z')) ^ u) v (((x' v y) ^ (y v z)) v u'))) v w')) = y'. [back_rewrite(2717),rewrite([3465(4),27(3),2291(2),27(4),3465(7),27(7),2325(3),3465(2),2291(3),2325(6),3465(5),2291(4),2291(4),3465(12),27(11),2291(10),27(12),3465(19),27(18),2291(17),27(19),3465(22),27(22),2325(18),3465(17),2291(18),2325(21),3465(20),2291(19),2291(19),3465(23),2291(9),27(22),2325(15),3465(14),27(14),2325(10),3465(9),2291(10),2325(13),3465(12),2291(11),2291(11),27(20),2325(18),3465(17),27(16),2291(15),27(17),2291(21),3465(23),27(23),2325(23),3465(22),27(15),2325(13),3465(12),27(11),2291(10),27(12),2291(16),2325(23),3465(22),27(22),2325(18),3465(17),2291(18),2325(21),3465(20),2291(19),2291(19),3465(26),2291(8),27(25),2325(23),3465(22),2291(8),27(21),2325(14),3465(13),27(13),2325(9),3465(8),2291(9),2325(12),3465(11),2291(10),2291(10),27(19),2325(17),3465(16),27(15),2291(14),27(16),2291(20),2291(23),3465(24),27(7),2325(5),3465(4),27(3),2291(2),27(4),2291(8),27(25),2325(25),3465(24),27(24),2325(24),3465(23),27(16),2325(14),3465(13),27(12),2291(11),27(13),2291(17),2325(24),3465(23),27(23),2325(19),3465(18),2291(19),2325(22),3465(21),2291(20),2291(20)])]. given #231 (T,wt=11): 5957 x ^ (((x v y) v z) v u) = x. [para(5477(a,1),5578(a,1,1)),rewrite([5477(7)])]. given #232 (T,wt=11): 5958 x ^ (((y v x) v z) v u) = x. [para(5554(a,1),5578(a,1,1)),rewrite([5554(7)])]. given #233 (T,wt=11): 5959 x ^ ((y v (x v z)) v u) = x. [para(5555(a,1),5578(a,1,1)),rewrite([5555(7)])]. given #234 (T,wt=11): 5960 x ^ ((y v (z v x)) v u) = x. [para(5597(a,1),5578(a,1,1)),rewrite([5597(7)])]. given #235 (A,wt=43): 3888 (((x ^ y') v (y' ^ z')) ^ u) v (y' ^ ((((x ^ y') v (y' ^ z')) ^ u) v (((x' v y) ^ (y v z)) v u'))) = y'. [back_rewrite(2715),rewrite([3465(4),27(3),2291(2),27(4),3465(7),27(7),2325(3),3465(2),2291(3),2325(6),3465(5),2291(4),2291(4),3465(11),27(10),2291(9),27(11),3465(18),27(17),2291(16),27(18),3465(21),27(21),2325(17),3465(16),2291(17),2325(20),3465(19),2291(18),2291(18),3465(22),2291(8),27(21),2325(14),3465(13),27(13),2325(9),3465(8),2291(9),2325(12),3465(11),2291(10),2291(10),27(19),2325(17),3465(16),27(15),2291(14),27(16),2291(20),3465(22),27(7),2325(5),3465(4),27(3),2291(2),27(4),2291(8),27(23),2325(23),3465(22),27(15),2325(13),3465(12),27(11),2291(10),27(12),2291(16),2325(23),3465(22),27(22),2325(18),3465(17),2291(18),2325(21),3465(20),2291(19),2291(19)])]. given #236 (T,wt=11): 6007 (x v ((y v z) v u)) ^ y = y. [para(5477(a,1),5612(a,1,2)),rewrite([5477(7)])]. given #237 (T,wt=11): 6008 (x v ((y v z) v u)) ^ z = z. [para(5554(a,1),5612(a,1,2)),rewrite([5554(7)])]. given #238 (T,wt=11): 6009 (x v (y v (z v u))) ^ z = z. [para(5555(a,1),5612(a,1,2)),rewrite([5555(7)])]. given #239 (T,wt=11): 6010 (x v (y v (z v u))) ^ u = u. [para(5597(a,1),5612(a,1,2)),rewrite([5597(7)])]. given #240 (A,wt=13): 3922 (((x ^ y) v (y ^ z)) ^ u) v y = y. [back_rewrite(2619),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3)])]. given #241 (T,wt=11): 6031 x ^ (y v ((x v z) v u)) = x. [para(5477(a,1),5668(a,1,1)),rewrite([5477(7)])]. given #242 (T,wt=11): 6032 x ^ (y v ((z v x) v u)) = x. [para(5554(a,1),5668(a,1,1)),rewrite([5554(7)])]. given #243 (T,wt=11): 6033 x ^ (y v (z v (x v u))) = x. [para(5555(a,1),5668(a,1,1)),rewrite([5555(7)])]. given #244 (T,wt=11): 6034 x ^ (y v (z v (u v x))) = x. [para(5597(a,1),5668(a,1,1)),rewrite([5597(7)])]. given #245 (A,wt=54): 3927 (((x ^ y') v (y' ^ z')) ^ u) v (y' ^ ((y' ^ ((w' v (((x ^ y') v (y' ^ z')) ^ u)) v (w ^ (((x' v y) ^ (y v z)) v u')))) v v5')) = y'. [back_rewrite(2610),rewrite([3465(4),27(3),2291(2),27(4),3465(7),27(7),2325(3),3465(2),2291(3),2325(6),3465(5),2291(4),2291(4),3465(12),27(11),2291(10),27(12),3465(15),27(15),2325(11),3465(10),2291(11),2325(14),3465(13),2291(12),2291(12),3465(19),27(18),2291(17),27(19),3465(22),27(22),2325(18),3465(17),2291(18),2325(21),3465(20),2291(19),2291(19),3465(22),27(23),2325(21),3465(20),27(19),2291(18),27(20),2291(24),3465(25),2325(16),3465(15),27(16),2325(14),3465(13),27(12),2291(11),27(13),2291(17),27(27),2291(19),2325(25),3465(24),27(24),2325(20),3465(19),2291(20),2325(23),3465(22),2291(21),2291(21),3465(26),2291(9),27(25),27(17),2291(9),2325(15),3465(14),27(14),2325(10),3465(9),2291(10),2325(13),3465(12),2291(11),2291(11),2325(22),3465(21),27(22),2325(20),3465(19),27(18),2291(17),27(19),2291(23),3465(26),27(26),2325(26),3465(25),2325(16),3465(15),27(16),2325(14),3465(13),27(12),2291(11),27(13),2291(17),27(27),2291(19),2325(25),3465(24),27(24),2325(20),3465(19),2291(20),2325(23),3465(22),2291(21),2291(21),3465(29),2291(8),27(28),2325(26),3465(25),2291(8),27(24),27(16),2291(8),2325(14),3465(13),27(13),2325(9),3465(8),2291(9),2325(12),3465(11),2291(10),2291(10),2325(21),3465(20),27(21),2325(19),3465(18),27(17),2291(16),27(18),2291(22),2291(26),3465(27),27(7),2325(5),3465(4),27(3),2291(2),27(4),2291(8),27(28),2325(28),3465(27),27(27),2325(27),3465(26),2325(17),3465(16),27(17),2325(15),3465(14),27(13),2291(12),27(14),2291(18),27(28),2291(20),2325(26),3465(25),27(25),2325(21),3465(20),2291(21),2325(24),3465(23),2291(22),2291(22)])]. given #246 (T,wt=12): 5139 (x ^ y') ^ (x' v y) = c_0'. [para(5087(a,1),27(a,1,1)),rewrite([27(5),2291(4),3999(7),2291(7)]),flip(a)]. given #247 (T,wt=12): 5148 (x' ^ y) ^ (x v y') = c_0'. [para(5088(a,1),27(a,1,1)),rewrite([27(5),2291(5),3999(7),2291(6)]),flip(a)]. given #248 (T,wt=12): 5159 (x v y') ^ (x' ^ y) = c_0'. [para(5094(a,1),27(a,1,1)),rewrite([3999(5),2291(4),27(7),2291(7)]),flip(a)]. given #249 (T,wt=12): 5217 (x' v y) ^ (x ^ y') = c_0'. [para(5095(a,1),27(a,1,1)),rewrite([3999(5),2291(5),27(7),2291(6)]),flip(a)]. given #250 (A,wt=25): 3928 (((x v y) ^ (y v z')) v u') v y = ((x v y) ^ (y v z')) v u'. [back_rewrite(2606),rewrite([3465(3),2291(3),3465(4),27(2),27(6),2291(6),3465(7),27(7),2325(4),3465(3),2291(2),2291(2),2325(4),3465(3),2291(3),3465(10),2291(10),3465(11),27(9),27(13),2291(13),3465(14),27(14),2325(11),3465(10),2291(9),2291(9),2325(11),3465(10),2291(10)])]. given #251 (T,wt=13): 5107 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(2329(a,1),3511(a,1,2,1)),rewrite([2928(5),2601(6)])]. given #252 (T,wt=13): 5110 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(3511(a,1),3847(a,1,2))]. given #253 (T,wt=13): 5112 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z. [para(4358(a,1),3511(a,1,2,1)),rewrite([4357(6),2601(6)])]. given #254 (T,wt=13): 5300 ((x ^ y) ^ z) ^ x = (x ^ y) ^ z. [para(5292(a,1),2427(a,1,2))]. given #255 (A,wt=40): 3958 (((x' v y) ^ (y v z)) v u') ^ (y v ((((x' v y) ^ (y v z)) v u') ^ (((x ^ y') v (y' ^ z')) ^ u))) = y. [back_rewrite(2528),rewrite([3465(4),27(3),2291(2),27(4),3465(7),27(7),2325(3),3465(2),2291(3),2325(6),3465(5),2291(4),2291(4),3465(11),27(10),2291(9),27(11),3465(18),27(17),2291(16),27(18),3465(21),27(21),2325(17),3465(16),2291(17),2325(20),3465(19),2291(18),2291(18),3465(22),2291(8),27(21),2325(14),3465(13),27(13),2325(9),3465(8),2291(9),2325(12),3465(11),2291(10),2291(10),27(19),2325(17),3465(16),27(15),2291(14),27(16),2291(20)])]. given #256 (T,wt=13): 5356 ((x ^ y) ^ z) ^ y = (x ^ y) ^ z. [para(5303(a,1),2427(a,1,2))]. given #257 (T,wt=13): 5365 (x ^ (y ^ z)) ^ y = x ^ (y ^ z). [para(5304(a,1),2427(a,1,2))]. given #258 (T,wt=13): 5366 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(5304(a,1),2579(a,1,1))]. given #259 (T,wt=13): 5369 (x ^ ((y ^ z) v (z ^ u))) v z = z. [para(3510(a,1),5304(a,1,1,2))]. given #260 (A,wt=44): 3971 (((x' v y) ^ (y v z)) v u') ^ (y v ((y v ((((x' v y) ^ (y v z)) v u') ^ (((x ^ y') v (y' ^ z')) ^ u))) ^ w)) = y. [back_rewrite(2479),rewrite([3465(4),27(3),2291(2),27(4),3465(7),27(7),2325(3),3465(2),2291(3),2325(6),3465(5),2291(4),2291(4),3465(12),27(11),2291(10),27(12),3465(19),27(18),2291(17),27(19),3465(22),27(22),2325(18),3465(17),2291(18),2325(21),3465(20),2291(19),2291(19),3465(23),2291(9),27(22),2325(15),3465(14),27(14),2325(10),3465(9),2291(10),2325(13),3465(12),2291(11),2291(11),27(20),2325(18),3465(17),27(16),2291(15),27(17),2291(21),3465(23),27(23),2325(23),3465(22),27(15),2325(13),3465(12),27(11),2291(10),27(12),2291(16),2325(23),3465(22),27(22),2325(18),3465(17),2291(18),2325(21),3465(20),2291(19),2291(19),3465(26),2291(8),27(25),2325(23),3465(22),2291(8),27(21),2325(14),3465(13),27(13),2325(9),3465(8),2291(9),2325(12),3465(11),2291(10),2291(10),27(19),2325(17),3465(16),27(15),2291(14),27(16),2291(20),2291(23)])]. given #261 (T,wt=13): 5385 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(3510(a,1),5313(a,1,2,2))]. given #262 (T,wt=13): 5432 (x ^ (y ^ z)) ^ z = x ^ (y ^ z). [para(5357(a,1),2427(a,1,2))]. given #263 (T,wt=13): 5433 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(5357(a,1),2579(a,1,1))]. given #264 (T,wt=13): 5547 x v ((x v y) v z) = (x v y) v z. [para(5477(a,1),2329(a,1,1))]. given #265 (A,wt=25): 3996 x v (((y' v x) ^ (x v z)) v u') = ((y' v x) ^ (x v z)) v u'. [back_rewrite(2336),rewrite([3465(4),27(3),2291(2),27(4),3465(7),27(7),2325(3),3465(2),2291(3),2325(6),3465(5),2291(4),2291(4),3465(11),27(10),2291(9),27(11),3465(14),27(14),2325(10),3465(9),2291(10),2325(13),3465(12),2291(11),2291(11)])]. given #266 (T,wt=13): 5549 ((x v y) v z) v x = (x v y) v z. [para(5477(a,1),3847(a,1,2))]. given #267 (T,wt=13): 5594 x v ((y v x) v z) = (y v x) v z. [para(5554(a,1),2329(a,1,1))]. given #268 (T,wt=13): 5595 ((x v y) v z) v y = (x v y) v z. [para(5554(a,1),3847(a,1,2))]. given #269 (T,wt=13): 5611 x v (y v (x v z)) = y v (x v z). [para(5555(a,1),2329(a,1,1))]. given #270 (A,wt=54): 4008 (((x' ^ y') v (y' ^ z)) ^ u) v (y' ^ ((y' ^ ((w' v (((x' ^ y') v (y' ^ z)) ^ u)) v (w ^ (((x v y) ^ (y v z')) v u')))) v v5')) = y'. [back_rewrite(2257),rewrite([3465(3),2291(3),3465(4),27(2),27(6),2291(6),3465(7),27(7),3999(4),2291(2),2291(2),3999(4),2291(3),3465(11),2291(11),3465(12),27(10),27(14),2291(14),3465(15),27(15),3999(12),2291(10),2291(10),3999(12),2291(11),3465(18),2291(18),3465(19),27(17),27(21),2291(21),3465(22),27(22),3999(19),2291(17),2291(17),3999(19),2291(18),3465(22),27(23),3999(21),27(18),27(22),2291(22),2291(24),3465(25),3999(16),27(16),3999(14),27(11),27(15),2291(15),2291(17),27(27),2291(19),3999(25),27(24),3999(21),2291(19),2291(19),3999(21),2291(20),3465(26),2291(9),27(25),27(17),2291(9),3999(15),27(14),3999(11),2291(9),2291(9),3999(11),2291(10),3999(22),27(22),3999(20),27(17),27(21),2291(21),2291(23),3465(26),27(26),3999(26),3999(16),27(16),3999(14),27(11),27(15),2291(15),2291(17),27(27),2291(19),3999(25),27(24),3999(21),2291(19),2291(19),3999(21),2291(20),3465(29),2291(8),27(28),3999(26),2291(8),27(24),27(16),2291(8),3999(14),27(13),3999(10),2291(8),2291(8),3999(10),2291(9),3999(21),27(21),3999(19),27(16),27(20),2291(20),2291(22),2291(26),3465(27),27(7),3999(5),27(2),27(6),2291(6),2291(8),27(28),3999(28),27(27),3999(27),3999(17),27(17),3999(15),27(12),27(16),2291(16),2291(18),27(28),2291(20),3999(26),27(25),3999(22),2291(20),2291(20),3999(22),2291(21)])]. given #271 (T,wt=13): 5613 (x v (y v z)) v y = x v (y v z). [para(5555(a,1),3847(a,1,2))]. given #272 (T,wt=13): 5681 x v (y v (z v x)) = y v (z v x). [para(5597(a,1),2329(a,1,1))]. given #273 (T,wt=13): 5682 (x v (y v z)) v z = x v (y v z). [para(5597(a,1),3847(a,1,2))]. given #274 (T,wt=13): 5724 (((x ^ y) v (x ^ z)) ^ u) v x = x. [para(4381(a,1),5301(a,1,2)),rewrite([4381(9)])]. given #275 (A,wt=28): 4020 (x ^ y') v (x ^ ((x ^ ((z' v (x ^ y')) v (z ^ (x' v y)))) v u')) = x. [back_rewrite(2225),rewrite([3465(8),27(9),2291(8),3465(10),3999(6),27(6),2291(5),27(11),2291(8),3999(9),2291(9),3465(11),27(12),27(8),2291(5),3999(6),2291(6),3999(10),27(10),2291(9),3465(13),27(13),2291(4),3999(11),3999(6),27(6),2291(5),27(11),2291(8),3999(9),2291(9),3465(14),27(15),3999(13),27(13),27(9),2291(6),3999(7),2291(7),3999(11),27(11),2291(10),2291(15),3465(16),27(3),2291(2),27(16),2291(4),3999(14),27(13),2291(4),3999(11),3999(6),27(6),2291(5),27(11),2291(8),3999(9),2291(9)])]. given #276 (T,wt=13): 5725 (((x ^ y) v (z ^ y)) ^ u) v y = y. [para(4383(a,1),5301(a,1,2)),rewrite([4383(9)])]. given #277 (T,wt=13): 5726 (((x ^ y) v (z ^ x)) ^ u) v x = x. [para(4477(a,1),5301(a,1,2)),rewrite([4477(9)])]. given #278 (T,wt=13): 5734 ((x v y) v z) ^ (x ^ u) = x ^ u. [para(5301(a,1),5477(a,1,1,1))]. given #279 (T,wt=13): 5736 (x ^ y) ^ ((x v z) v u) = x ^ y. [para(5301(a,1),5550(a,1,2,1))]. given #280 (A,wt=55): 4021 (x' v y') v (((x' v y') v z') ^ ((((x' v y') v z') ^ (((u' v w') v (x' v y')) v ((u ^ w) ^ (x ^ y)))) v v5')) = (x' v y') v z'. [back_rewrite(2222),rewrite([3465(3),3999(3),3465(8),3999(8),3465(15),3465(18),3465(22),3999(15),3999(13),3999(16),27(26),27(22),2291(20),2291(20),27(23),2291(21),2291(21),3465(23),27(12),27(10),2291(8),2291(8),2291(9),27(20),27(16),27(12),2291(10),2291(10),27(13),2291(11),2291(11),3999(15),3999(13),3999(16),3465(21),27(21),3999(9),3999(8),3999(23),3999(15),3999(13),3999(16),27(26),27(22),2291(20),2291(20),27(23),2291(21),2291(21),3465(26),27(7),27(5),2291(3),2291(3),2291(4),27(23),3999(21),27(9),27(7),2291(5),2291(5),2291(6),27(17),27(13),27(9),2291(7),2291(7),27(10),2291(8),2291(8),3999(12),3999(10),3999(13),2291(19),3465(20),3999(2),27(22),3999(6),3999(5),3999(24),27(23),3999(11),3999(10),3999(25),3999(17),3999(15),3999(18),27(28),27(24),2291(22),2291(22),27(25),2291(23),2291(23),3465(31),3999(31)])]. given #281 (T,wt=13): 5738 (x v (y v z)) ^ (y ^ u) = y ^ u. [para(5301(a,1),5555(a,1,1,2))]. given #282 (T,wt=10): 8392 x' ^ (x ^ y') = c_0'. [para(5738(a,1),5066(a,1)),rewrite([27(4),2291(3)])]. given #283 (T,wt=8): 8442 x v (x' v y) = c_0. [para(8392(a,1),3999(a,1,1)),rewrite([2291(3),2291(3),3999(4),2291(4)]),flip(a)]. given #284 (T,wt=8): 8462 x' v (x v y) = c_0. [para(2291(a,1),8442(a,1,2,1))]. given #285 (A,wt=43): 4067 (((x ^ y) v (y ^ z)) ^ u) v (y ^ ((w' v (((x ^ y) v (y ^ z)) ^ u)) v (w ^ (((x' v y') ^ (y' v z')) v u')))) = y. [back_rewrite(1729),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(4),27(4),3999(2),3999(5),3465(10),3465(13),3465(16),27(13),2291(11),2291(11),27(14),2291(12),2291(12),3465(13),27(13),3999(11),3999(14),3465(20),3465(23),3465(26),27(23),2291(21),2291(21),27(24),2291(22),2291(22),3465(23),27(23),3999(21),3999(24),3465(29),27(30),3999(28),27(24),2291(22),2291(22),27(25),2291(23),2291(23),2291(25),3465(26),3999(20),27(20),3999(18),27(14),2291(12),2291(12),27(15),2291(13),2291(13),2291(15),27(22),2291(17),3999(20),27(19),3999(17),3999(20),3465(27),27(28),27(17),2291(12),3999(15),27(14),3999(12),3999(15),3999(31),27(31),3999(29),27(25),2291(23),2291(23),27(26),2291(24),2291(24),2291(26),3465(29),27(10),3999(8),27(4),2291(2),2291(2),27(5),2291(3),2291(3),2291(5),27(24),2291(6),3999(22),3999(15),27(15),3999(13),27(9),2291(7),2291(7),27(10),2291(8),2291(8),2291(10),27(17),2291(12),3999(15),27(14),3999(12),3999(15)])]. given #286 (T,wt=8): 8464 x v (y v x') = c_0. [para(4425(a,1),8442(a,1,2))]. given #287 (T,wt=8): 8470 x' v (y v x) = c_0. [para(8442(a,1),5681(a,1)),flip(a)]. given #288 (T,wt=8): 8631 (x v y) v x' = c_0. [para(8464(a,1),5547(a,1)),flip(a)]. given #289 (T,wt=8): 8632 (x v y) v y' = c_0. [para(8464(a,1),5594(a,1)),flip(a)]. given #290 (A,wt=55): 4112 (((x' v y') ^ (y' v z')) v u') ^ (y' v ((y' v ((w ^ (((x' v y') ^ (y' v z')) v u')) ^ (w' v (((x ^ y) v (y ^ z)) ^ u)))) ^ v5)) = y'. [back_rewrite(1401),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(4),27(4),3999(2),3999(5),3465(10),3465(13),3465(16),27(13),2291(11),2291(11),27(14),2291(12),2291(12),3465(13),27(13),3999(11),3999(14),3465(20),3465(23),3465(26),27(23),2291(21),2291(21),27(24),2291(22),2291(22),3465(23),27(23),3999(21),3999(24),3465(29),27(30),3999(28),27(24),2291(22),2291(22),27(25),2291(23),2291(23),2291(25),3465(26),3999(20),27(20),3999(18),27(14),2291(12),2291(12),27(15),2291(13),2291(13),2291(15),27(22),2291(17),3999(20),27(19),3999(17),3999(20),3465(27),27(28),27(17),2291(12),3999(15),27(14),3999(12),3999(15),3999(31),27(31),3999(29),27(25),2291(23),2291(23),27(26),2291(24),2291(24),2291(26),3465(29),27(29),2291(11),3999(27),3999(20),27(20),3999(18),27(14),2291(12),2291(12),27(15),2291(13),2291(13),2291(15),27(22),2291(17),3999(20),27(19),3999(17),3999(20),3465(30),27(31),3999(29),27(29),27(18),2291(13),3999(16),27(15),3999(13),3999(16),3999(32),27(32),3999(30),27(26),2291(24),2291(24),27(27),2291(25),2291(25),2291(27),2291(31)])]. given #291 (T,wt=8): 8636 (x' v y) v x = c_0. [para(8470(a,1),5547(a,1)),flip(a)]. given #292 (T,wt=8): 8637 (x v y') v y = c_0. [para(8470(a,1),5594(a,1)),flip(a)]. given #293 (T,wt=9): 8440 x' ^ (x ^ y) = c_0'. [para(2291(a,1),8392(a,1,2,2))]. given #294 (T,wt=9): 8827 x ^ (x' ^ y) = c_0'. [para(2291(a,1),8440(a,1,1))]. given #295 (A,wt=48): 4118 (((x ^ y) v (y ^ z)) ^ u) v (y ^ ((y ^ ((w' v (((x ^ y) v (y ^ z)) ^ u)) v (w ^ (((x' v y') ^ (y' v z')) v u')))) v v5')) = y. [back_rewrite(1365),rewrite([3465(1),3465(4),3465(7),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(4),27(4),3999(2),3999(5),3465(10),3465(13),3465(16),27(13),2291(11),2291(11),27(14),2291(12),2291(12),3465(13),27(13),3999(11),3999(14),3465(20),3465(23),3465(26),27(23),2291(21),2291(21),27(24),2291(22),2291(22),3465(23),27(23),3999(21),3999(24),3465(29),27(30),3999(28),27(24),2291(22),2291(22),27(25),2291(23),2291(23),2291(25),3465(26),3999(20),27(20),3999(18),27(14),2291(12),2291(12),27(15),2291(13),2291(13),2291(15),27(22),2291(17),3999(20),27(19),3999(17),3999(20),3465(27),27(28),27(17),2291(12),3999(15),27(14),3999(12),3999(15),3999(31),27(31),3999(29),27(25),2291(23),2291(23),27(26),2291(24),2291(24),2291(26),3465(29),27(29),2291(11),3999(27),3999(20),27(20),3999(18),27(14),2291(12),2291(12),27(15),2291(13),2291(13),2291(15),27(22),2291(17),3999(20),27(19),3999(17),3999(20),3465(30),27(31),3999(29),27(29),27(18),2291(13),3999(16),27(15),3999(13),3999(16),3999(32),27(32),3999(30),27(26),2291(24),2291(24),27(27),2291(25),2291(25),2291(27),2291(31),3465(32),27(10),3999(8),27(4),2291(2),2291(2),27(5),2291(3),2291(3),2291(5),27(27),2291(6),3999(25),27(24),2291(6),3999(22),3999(15),27(15),3999(13),27(9),2291(7),2291(7),27(10),2291(8),2291(8),2291(10),27(17),2291(12),3999(15),27(14),3999(12),3999(15)])]. given #296 (T,wt=9): 8828 x' ^ (y ^ x) = c_0'. [para(4357(a,1),8440(a,1,2))]. given #297 (T,wt=9): 8852 x ^ (y ^ x') = c_0'. [para(8440(a,1),5433(a,1)),flip(a)]. given #298 (T,wt=9): 8969 (x' ^ y) ^ x = c_0'. [para(8828(a,1),5107(a,1)),flip(a)]. given #299 (T,wt=9): 8970 (x ^ y') ^ y = c_0'. [para(8828(a,1),5112(a,1)),flip(a)]. given #300 (A,wt=48): 4234 (((((x' v y') v (z' v u')) ^ w) v (w ^ v5)) ^ v6) v (w ^ ((w ^ (((x' v y') v (z' v u')) v ((x ^ y) ^ (z ^ u)))) v v5')) = w. [back_rewrite(538),rewrite([3465(1),3465(4),3465(8),27(8),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3465(6),3465(9),27(6),3999(4),3999(2),3999(5),2291(9),27(12),2291(10),2291(10),3465(11),27(11),3999(9),27(8),27(4),2291(2),2291(2),27(5),2291(3),2291(3),3999(7),3465(15),3465(18),3465(22),3999(15),3999(13),3999(16),27(26),27(22),2291(20),2291(20),27(23),2291(21),2291(21),3465(23),27(24),27(20),27(16),2291(14),2291(14),27(17),2291(15),2291(15),3999(19),3999(17),3999(20),3465(25),27(25),2291(13),3999(23),3999(15),3999(13),3999(16),27(26),27(22),2291(20),2291(20),27(23),2291(21),2291(21),3465(26),27(27),3999(25),27(25),27(21),27(17),2291(15),2291(15),27(18),2291(16),2291(16),3999(20),3999(18),3999(21),2291(27),3465(28),27(12),3999(10),27(6),3999(4),3999(2),3999(5),2291(9),27(12),2291(10),2291(10),2291(12),27(28),2291(13),3999(26),27(25),2291(13),3999(23),3999(15),3999(13),3999(16),27(26),27(22),2291(20),2291(20),27(23),2291(21),2291(21)])]. given #301 (T,wt=9): 8978 (x ^ y) ^ x' = c_0'. [para(8852(a,1),5107(a,1)),flip(a)]. given #302 (T,wt=9): 8979 (x ^ y) ^ y' = c_0'. [para(8852(a,1),5112(a,1)),flip(a)]. given #303 (T,wt=10): 8467 x v ((x' v y) v z) = c_0. [para(5547(a,1),8442(a,1,2))]. given #304 (T,wt=10): 8468 x v ((y v x') v z) = c_0. [para(5594(a,1),8442(a,1,2))]. given #305 (A,wt=21): 4371 (x v y) ^ (((x v y) ^ (y v z)) v y) = (x v y) ^ (y v z). [para(2291(a,1),2658(a,1,1,1)),rewrite([2291(3),2291(8)])]. given #306 (T,wt=10): 8469 x v (y v (x' v z)) = c_0. [para(5611(a,1),8442(a,1,2))]. given #307 (T,wt=10): 8471 x v (y v (z v x')) = c_0. [para(5681(a,1),8442(a,1,2))]. given #308 (T,wt=10): 8498 x' v ((x v y) v z) = c_0. [para(5547(a,1),8462(a,1,2))]. given #309 (T,wt=10): 8499 x' v ((y v x) v z) = c_0. [para(5594(a,1),8462(a,1,2))]. given #310 (A,wt=17): 4378 ((x' v y') ^ (y' v z')) ^ y' = y'. [para(4034(a,1),27(a,1,1)),rewrite([27(5),3999(3),3999(6)]),flip(a)]. given #311 (T,wt=10): 8500 x' v (y v (x v z)) = c_0. [para(5611(a,1),8462(a,1,2))]. given #312 (T,wt=10): 8501 x' v (y v (z v x)) = c_0. [para(5681(a,1),8462(a,1,2))]. given #313 (T,wt=10): 8663 ((x v y) v z) v x' = c_0. [para(5547(a,1),8631(a,1,1))]. given #314 (T,wt=10): 8664 ((x v y) v z) v y' = c_0. [para(5594(a,1),8631(a,1,1))]. given #315 (A,wt=15): 4379 (x v ((x v y) ^ z)) v (x v y) = x v y. [para(2427(a,1),4034(a,1,1,1))]. given #316 (T,wt=10): 8665 (x v (y v z)) v y' = c_0. [para(5611(a,1),8631(a,1,1))]. given #317 (T,wt=10): 8666 (x v (y v z)) v z' = c_0. [para(5681(a,1),8631(a,1,1))]. given #318 (T,wt=10): 8814 ((x' v y) v z) v x = c_0. [para(5547(a,1),8636(a,1,1))]. given #319 (T,wt=10): 8815 ((x v y') v z) v y = c_0. [para(5594(a,1),8636(a,1,1))]. given #320 (A,wt=15): 4380 ((x ^ (y v z)) v y) v (y v z) = y v z. [para(2579(a,1),4034(a,1,1,2))]. given #321 (T,wt=10): 8816 (x v (y' v z)) v y = c_0. [para(5611(a,1),8636(a,1,1))]. given #322 (T,wt=10): 8817 (x v (y v z')) v z = c_0. [para(5681(a,1),8636(a,1,1))]. given #323 (T,wt=10): 9115 (x' v y) v (x v z) = c_0. [para(8467(a,1),5611(a,1)),flip(a)]. given #324 (T,wt=10): 9117 (x' v y) v (z v x) = c_0. [para(8467(a,1),5681(a,1)),flip(a)]. given #325 (A,wt=15): 4428 ((x ^ (y v z)) v z) v (y v z) = y v z. [para(4409(a,1),4034(a,1,1,2))]. given #326 (T,wt=10): 9122 (x v y') v (y v z) = c_0. [para(8468(a,1),5611(a,1)),flip(a)]. given #327 (T,wt=10): 9124 (x v y') v (z v y) = c_0. [para(8468(a,1),5681(a,1)),flip(a)]. given #328 (T,wt=10): 9204 (x v y) v (x' v z) = c_0. [para(8469(a,1),5547(a,1)),flip(a)]. given #329 (T,wt=10): 9205 (x v y) v (y' v z) = c_0. [para(8469(a,1),5594(a,1)),flip(a)]. given #330 (A,wt=15): 4431 (x v ((y v x) ^ z)) v (y v x) = y v x. [para(4427(a,1),4034(a,1,1,1))]. given #331 (T,wt=10): 9208 (x v y) v (z v x') = c_0. [para(8471(a,1),5547(a,1)),flip(a)]. given #332 (T,wt=10): 9209 (x v y) v (z v y') = c_0. [para(8471(a,1),5594(a,1)),flip(a)]. given #333 (T,wt=11): 8849 x' ^ ((x ^ y) ^ z) = c_0'. [para(5107(a,1),8440(a,1,2))]. given #334 (T,wt=11): 8850 x' ^ ((y ^ x) ^ z) = c_0'. [para(5112(a,1),8440(a,1,2))]. given #335 (A,wt=17): 4472 ((x' v y') ^ (x' v z')) ^ x' = x'. [para(4381(a,1),27(a,1,1)),rewrite([27(5),3999(3),3999(6)]),flip(a)]. given #336 (T,wt=11): 8851 x' ^ (y ^ (x ^ z)) = c_0'. [para(5366(a,1),8440(a,1,2))]. given #337 (T,wt=11): 8853 x' ^ (y ^ (z ^ x)) = c_0'. [para(5433(a,1),8440(a,1,2))]. given #338 (T,wt=11): 8864 x ^ ((x' ^ y) ^ z) = c_0'. [para(5107(a,1),8827(a,1,2))]. given #339 (T,wt=11): 8865 x ^ ((y ^ x') ^ z) = c_0'. [para(5112(a,1),8827(a,1,2))]. given #340 (A,wt=17): 4473 ((x ^ y) v (x ^ z)) ^ x = (x ^ y) v (x ^ z). [para(4381(a,1),2427(a,1,2))]. given #341 (T,wt=11): 8866 x ^ (y ^ (x' ^ z)) = c_0'. [para(5366(a,1),8827(a,1,2))]. given #342 (T,wt=11): 8867 x ^ (y ^ (z ^ x')) = c_0'. [para(5433(a,1),8827(a,1,2))]. given #343 (T,wt=11): 8986 ((x' ^ y) ^ z) ^ x = c_0'. [para(5107(a,1),8969(a,1,1))]. given #344 (T,wt=11): 8987 ((x ^ y') ^ z) ^ y = c_0'. [para(5112(a,1),8969(a,1,1))]. given #345 (A,wt=17): 4474 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(4381(a,1),2579(a,1,1))]. given #346 (T,wt=11): 8988 (x ^ (y' ^ z)) ^ y = c_0'. [para(5366(a,1),8969(a,1,1))]. given #347 (T,wt=11): 8989 (x ^ (y ^ z')) ^ z = c_0'. [para(5433(a,1),8969(a,1,1))]. given #348 (T,wt=11): 9102 ((x ^ y) ^ z) ^ x' = c_0'. [para(5107(a,1),8978(a,1,1))]. given #349 (T,wt=11): 9103 ((x ^ y) ^ z) ^ y' = c_0'. [para(5112(a,1),8978(a,1,1))]. given #350 (A,wt=15): 4475 (((x v y) ^ z) v x) v (x v y) = x v y. [para(2579(a,1),4381(a,1,1,2))]. given #351 (T,wt=11): 9104 (x ^ (y ^ z)) ^ y' = c_0'. [para(5366(a,1),8978(a,1,1))]. given #352 (T,wt=11): 9105 (x ^ (y ^ z)) ^ z' = c_0'. [para(5433(a,1),8978(a,1,1))]. given #353 (T,wt=11): 9482 (x v y) v (y v x) = y v x. [para(4427(a,1),4380(a,1,1,1))]. % Operation v is commutative; C redundancy checks enabled. given #354 (T,wt=7): 10434 x v y = y v x. [para(9482(a,1),2579(a,1,1)),rewrite([10433(3)])]. given #355 (A,wt=19): 4503 ((x ^ ((x ^ y) v z')) v u') ^ (x ^ y) = x ^ y. [back_rewrite(3604),rewrite([4486(11),3847(10)])]. given #356 (T,wt=11): 9838 (x ^ y) ^ (x' ^ z) = c_0'. [para(8849(a,1),5366(a,1)),flip(a)]. given #357 (T,wt=11): 9840 (x ^ y) ^ (z ^ x') = c_0'. [para(8849(a,1),5433(a,1)),flip(a)]. given #358 (T,wt=11): 9854 (x ^ y) ^ (y' ^ z) = c_0'. [para(8850(a,1),5366(a,1)),flip(a)]. given #359 (T,wt=11): 9856 (x ^ y) ^ (z ^ y') = c_0'. [para(8850(a,1),5433(a,1)),flip(a)]. given #360 (A,wt=17): 4505 x' ^ ((y' v x') ^ (x' v z')) = x'. [para(4382(a,1),27(a,1,1)),rewrite([27(6),3999(4),3999(7)]),flip(a)]. given #361 (T,wt=11): 9948 (x' ^ y) ^ (x ^ z) = c_0'. [para(8851(a,1),5107(a,1)),flip(a)]. given #362 (T,wt=11): 9949 (x ^ y') ^ (y ^ z) = c_0'. [para(8851(a,1),5112(a,1)),flip(a)]. given #363 (T,wt=11): 9962 (x' ^ y) ^ (z ^ x) = c_0'. [para(8853(a,1),5107(a,1)),flip(a)]. given #364 (T,wt=11): 9963 (x ^ y') ^ (z ^ y) = c_0'. [para(8853(a,1),5112(a,1)),flip(a)]. given #365 (A,wt=15): 4506 (x v y) v (x v ((x v y) ^ z)) = x v y. [para(2427(a,1),4382(a,1,2,1))]. given #366 (T,wt=11): 10433 (x v y) ^ (y v x) = x v y. [para(9482(a,1),2427(a,1,2))]. given #367 (T,wt=11): 10459 (x' ^ y') v (y v x) = c_0. [para(9482(a,1),8462(a,1,2)),rewrite([27(2)])]. given #368 (T,wt=11): 11737 x' ^ y' = y' ^ x'. [para(10434(a,1),27(a,1,1)),rewrite([27(2)])]. given #369 (T,wt=9): 12003 x' ^ y = y ^ x'. [para(2291(a,1),11737(a,1,1)),rewrite([2291(5)]),flip(a)]. % Operation ^ is commutative; C redundancy checks enabled. % back CAC tautology: 12012 (x' ^ y) v (z' ^ x') = (x' ^ y) v (x' ^ z'). [para(11737(a,1),4473(a,1,1,2)),rewrite([12003(8,R),4547(8)])]. % back CAC tautology: 12009 x ^ (y' ^ z') = x ^ (z' ^ y'). [para(11737(a,1),5365(a,1,1,2)),rewrite([12003(6,R),5433(6)])]. % back CAC tautology: 12008 (x' ^ y') ^ z = (y' ^ x') ^ z. [para(11737(a,1),5107(a,1,2,1)),rewrite([5112(6)])]. % back CAC tautology: 12007 ((x ^ y') v (z' ^ y')) ^ u = ((x ^ y') v (y' ^ z')) ^ u. [para(11737(a,1),3511(a,1,2,1,2)),rewrite([5113(9)])]. % back CAC tautology: 12006 ((x' ^ y') v (y' ^ z)) ^ u = ((y' ^ x') v (y' ^ z)) ^ u. [para(11737(a,1),3511(a,1,2,1,1)),rewrite([5111(9)]),flip(a)]. % back CAC tautology: 12005 (x ^ y') v (z' ^ y') = (x ^ y') v (y' ^ z'). [para(11737(a,1),3510(a,1,2,2)),rewrite([4539(8)])]. % back CAC tautology: 12004 (x' ^ y') v (y' ^ z) = (y' ^ x') v (y' ^ z). [para(11737(a,1),3510(a,1,2,1)),rewrite([4474(8)]),flip(a)]. given #370 (A,wt=15): 4510 (x v y) v (y v ((x v y) ^ z)) = x v y. [para(4427(a,1),4382(a,1,2,1))]. given #371 (T,wt=7): 12121 x ^ y = y ^ x. [para(2291(a,1),12003(a,1,1)),rewrite([2291(3)])]. given #372 (T,wt=11): 11738 (x ^ y) v (y' v x') = c_0. [para(10434(a,1),4856(a,1,2))]. given #373 (T,wt=11): 11739 (x' ^ y) v (y' v x) = c_0. [para(10434(a,1),5094(a,1,2))]. given #374 (T,wt=11): 11740 (x ^ y') v (y v x') = c_0. [para(10434(a,1),5095(a,1,2))]. given #375 (A,wt=17): 4539 x ^ ((y ^ x) v (z ^ x)) = (y ^ x) v (z ^ x). [para(4383(a,1),2579(a,1,1))]. given #376 (T,wt=12): 9112 x v (((x' v y) v z) v u) = c_0. [para(5547(a,1),8467(a,1,2,1))]. given #377 (T,wt=12): 9113 x v (((y v x') v z) v u) = c_0. [para(5594(a,1),8467(a,1,2,1))]. given #378 (T,wt=12): 9114 x v ((y v (x' v z)) v u) = c_0. [para(5594(a,1),8467(a,1,2))]. given #379 (T,wt=12): 9116 x v (y v ((x' v z) v u)) = c_0. [para(5611(a,1),8467(a,1,2))]. given #380 (A,wt=17): 4547 x ^ ((x ^ y) v (z ^ x)) = (x ^ y) v (z ^ x). [para(4477(a,1),2579(a,1,1))]. given #381 (T,wt=12): 9118 x v ((y v (z v x')) v u) = c_0. [para(5681(a,1),8467(a,1,2,1))]. given #382 (T,wt=12): 9119 x v (y v (z v (x' v u))) = c_0. [para(5681(a,1),8467(a,1,2))]. given #383 (T,wt=12): 9123 x v (y v ((z v x') v u)) = c_0. [para(5611(a,1),8468(a,1,2))]. given #384 (T,wt=12): 9125 x v (y v (z v (u v x'))) = c_0. [para(5681(a,1),8468(a,1,2))]. given #385 (A,wt=17): 4549 x' ^ ((y' v x') ^ (z' v x')) = x'. [para(4508(a,1),27(a,1,1)),rewrite([27(6),3999(4),3999(7)]),flip(a)]. given #386 (T,wt=12): 9235 x' v (((x v y) v z) v u) = c_0. [para(5547(a,1),8498(a,1,2,1))]. given #387 (T,wt=12): 9237 x' v (((y v x) v z) v u) = c_0. [para(5594(a,1),8498(a,1,2,1))]. given #388 (T,wt=12): 9238 x' v ((y v (x v z)) v u) = c_0. [para(5594(a,1),8498(a,1,2))]. given #389 (T,wt=12): 9239 x' v (y v ((x v z) v u)) = c_0. [para(5611(a,1),8498(a,1,2))]. given #390 (A,wt=15): 4550 (x v y) v (x v (z ^ (x v y))) = x v y. [para(2427(a,1),4508(a,1,2,1))]. given #391 (T,wt=12): 9241 x' v ((y v (z v x)) v u) = c_0. [para(5681(a,1),8498(a,1,2,1))]. given #392 (T,wt=12): 9242 x' v (y v (z v (x v u))) = c_0. [para(5681(a,1),8498(a,1,2))]. given #393 (T,wt=12): 9249 x' v (y v ((z v x) v u)) = c_0. [para(5611(a,1),8499(a,1,2))]. given #394 (T,wt=12): 9250 x' v (y v (z v (u v x))) = c_0. [para(5681(a,1),8499(a,1,2))]. given #395 (A,wt=15): 4551 (x v y) v (y v (z ^ (x v y))) = x v y. [para(4427(a,1),4508(a,1,2,1))]. given #396 (T,wt=12): 9577 ((x' v y) v z) v (x v u) = c_0. [para(5547(a,1),9115(a,1,1))]. given #397 (T,wt=12): 9578 (x' v y) v ((x v z) v u) = c_0. [para(5547(a,1),9115(a,1,2))]. given #398 (T,wt=12): 9580 ((x v y') v z) v (y v u) = c_0. [para(5594(a,1),9115(a,1,1))]. given #399 (T,wt=12): 9581 (x' v y) v ((z v x) v u) = c_0. [para(5594(a,1),9115(a,1,2))]. given #400 (A,wt=17): 4582 x' ^ ((x' v y') ^ (z' v x')) = x'. [para(4543(a,1),27(a,1,1)),rewrite([27(6),3999(4),3999(7)]),flip(a)]. given #401 (T,wt=12): 9582 (x v (y' v z)) v (y v u) = c_0. [para(5611(a,1),9115(a,1,1))]. given #402 (T,wt=12): 9583 (x' v y) v (z v (x v u)) = c_0. [para(5611(a,1),9115(a,1,2))]. given #403 (T,wt=12): 9585 (x v (y v z')) v (z v u) = c_0. [para(5681(a,1),9115(a,1,1))]. given #404 (T,wt=12): 9586 (x' v y) v (z v (u v x)) = c_0. [para(5681(a,1),9115(a,1,2))]. given #405 (A,wt=30): 5051 (((x' v y') ^ (y' v z')) v u') ^ ((u' v y') ^ w) = (u' v y') ^ w. [para(4427(a,1),3507(a,1,2,1,1)),rewrite([4427(25)])]. given #406 (T,wt=12): 9594 ((x' v y) v z) v (u v x) = c_0. [para(5547(a,1),9117(a,1,1))]. given #407 (T,wt=12): 9595 ((x v y') v z) v (u v y) = c_0. [para(5594(a,1),9117(a,1,1))]. given #408 (T,wt=12): 9596 (x v (y' v z)) v (u v y) = c_0. [para(5611(a,1),9117(a,1,1))]. given #409 (T,wt=12): 9597 (x v (y v z')) v (u v z) = c_0. [para(5681(a,1),9117(a,1,1))]. given #410 (A,wt=19): 5069 (x v y) ^ (x v ((x v y) ^ z)) = x v ((x v y) ^ z). [para(2427(a,1),3510(a,1,2,1)),rewrite([2427(7)])]. given #411 (T,wt=12): 9665 (x v y') v ((y v z) v u) = c_0. [para(5547(a,1),9122(a,1,2))]. given #412 (T,wt=12): 9667 (x v y') v ((z v y) v u) = c_0. [para(5594(a,1),9122(a,1,2))]. given #413 (T,wt=12): 9668 (x v y') v (z v (y v u)) = c_0. [para(5611(a,1),9122(a,1,2))]. given #414 (T,wt=12): 9670 (x v y') v (z v (u v y)) = c_0. [para(5681(a,1),9122(a,1,2))]. given #415 (A,wt=19): 5073 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z). [para(4427(a,1),3510(a,1,2,1)),rewrite([4427(7)])]. given #416 (T,wt=12): 9700 ((x v y) v z) v (x' v u) = c_0. [para(5547(a,1),9204(a,1,1))]. given #417 (T,wt=12): 9701 (x v y) v ((x' v z) v u) = c_0. [para(5547(a,1),9204(a,1,2))]. given #418 (T,wt=12): 9703 ((x v y) v z) v (y' v u) = c_0. [para(5594(a,1),9204(a,1,1))]. given #419 (T,wt=12): 9704 (x v y) v ((z v x') v u) = c_0. [para(5594(a,1),9204(a,1,2))]. given #420 (A,wt=15): 5076 x v ((y ^ x) v ((z ^ x) v (x ^ u))) = x. [para(3510(a,1),4382(a,1,2,2))]. given #421 (T,wt=12): 9705 (x v (y v z)) v (y' v u) = c_0. [para(5611(a,1),9204(a,1,1))]. given #422 (T,wt=12): 9706 (x v y) v (z v (x' v u)) = c_0. [para(5611(a,1),9204(a,1,2))]. given #423 (T,wt=12): 9708 (x v (y v z)) v (z' v u) = c_0. [para(5681(a,1),9204(a,1,1))]. given #424 (T,wt=12): 9709 (x v y) v (z v (u v x')) = c_0. [para(5681(a,1),9204(a,1,2))]. given #425 (A,wt=15): 5077 x v (((y ^ x) v (x ^ z)) v (x ^ u)) = x. [para(3510(a,1),4476(a,1,2,1))]. given #426 (T,wt=12): 9718 (x v y) v ((y' v z) v u) = c_0. [para(5547(a,1),9205(a,1,2))]. given #427 (T,wt=12): 9719 (x v y) v ((z v y') v u) = c_0. [para(5594(a,1),9205(a,1,2))]. given #428 (T,wt=12): 9720 (x v y) v (z v (y' v u)) = c_0. [para(5611(a,1),9205(a,1,2))]. given #429 (T,wt=12): 9721 (x v y) v (z v (u v y')) = c_0. [para(5681(a,1),9205(a,1,2))]. given #430 (A,wt=15): 5078 x v ((x ^ y) v ((z ^ x) v (x ^ u))) = x. [para(3510(a,1),4476(a,1,2,2))]. given #431 (T,wt=12): 9793 ((x v y) v z) v (u v x') = c_0. [para(5547(a,1),9208(a,1,1))]. given #432 (T,wt=12): 9795 ((x v y) v z) v (u v y') = c_0. [para(5594(a,1),9208(a,1,1))]. given #433 (T,wt=12): 9796 (x v (y v z)) v (u v y') = c_0. [para(5611(a,1),9208(a,1,1))]. given #434 (T,wt=12): 9798 (x v (y v z)) v (u v z') = c_0. [para(5681(a,1),9208(a,1,1))]. given #435 (A,wt=15): 5080 x v (((y ^ x) v (x ^ z)) v (u ^ x)) = x. [para(3510(a,1),4543(a,1,2,1))]. given #436 (T,wt=12): 11741 (x' ^ y') ^ (y v x) = c_0'. [para(10434(a,1),4992(a,1,2))]. given #437 (T,wt=12): 11744 (x ^ y) ^ (y' v x') = c_0'. [para(10434(a,1),5067(a,1,2))]. given #438 (T,wt=12): 11745 (x ^ y') ^ (y v x') = c_0'. [para(10434(a,1),5139(a,1,2))]. given #439 (T,wt=12): 11746 (x' ^ y) ^ (y' v x) = c_0'. [para(10434(a,1),5148(a,1,2))]. given #440 (A,wt=25): 5081 x ^ ((y ^ x) v ((z ^ x) v (x ^ u))) = (y ^ x) v ((z ^ x) v (x ^ u)). [para(3510(a,1),3510(a,1,2,2)),rewrite([3510(11)])]. given #441 (T,wt=12): 12359 x ^ ((y' v x) ^ (x v z)) = x. [back_rewrite(10277),rewrite([12121(5)])]. given #442 (T,wt=11): 14130 x ^ ((y v x) ^ (x v z)) = x. [para(2291(a,1),12359(a,1,2,1,1))]. given #443 (T,wt=11): 14195 x ^ ((y v x) ^ (z v x)) = x. [para(4425(a,1),14130(a,1,2,2))]. given #444 (T,wt=11): 14245 x ^ ((x v y) ^ (x v z)) = x. [para(10434(a,1),14130(a,1,2,1))]. given #445 (A,wt=16): 5092 ((x v y) ^ z) v ((x' ^ y') v z') = c_0. [para(27(a,1),4856(a,1,2,1))]. given #446 (T,wt=11): 14248 x ^ ((x v y) ^ (z v x)) = x. [para(12121(a,1),14130(a,1,2))]. given #447 (T,wt=13): 5740 (x ^ y) ^ (z v (x v u)) = x ^ y. [para(5301(a,1),5582(a,1,2,2))]. given #448 (T,wt=13): 5742 ((x ^ y) ^ z) v (x v u) = x v u. [para(5301(a,1),5301(a,1,2)),rewrite([5301(7)])]. given #449 (T,wt=13): 5746 ((x v y) v z) ^ (y ^ u) = y ^ u. [para(5305(a,1),5477(a,1,1,1))]. given #450 (A,wt=16): 5093 (x ^ (y v z)) v (x' v (y' ^ z')) = c_0. [para(27(a,1),4856(a,1,2,2))]. given #451 (T,wt=13): 5748 (x ^ y) ^ ((z v x) v u) = x ^ y. [para(5305(a,1),5550(a,1,2,1))]. given #452 (T,wt=13): 5750 (x v (y v z)) ^ (z ^ u) = z ^ u. [para(5305(a,1),5555(a,1,1,2))]. given #453 (T,wt=13): 5752 (x ^ y) ^ (z v (u v x)) = x ^ y. [para(5305(a,1),5582(a,1,2,2))]. given #454 (T,wt=13): 5754 ((x ^ y) ^ z) v (u v x) = u v x. [para(5305(a,1),5301(a,1,2)),rewrite([5305(7)])]. given #455 (A,wt=16): 5096 ((x ^ y) ^ z) v ((x' v y') v z') = c_0. [para(3999(a,1),4856(a,1,2,1))]. given #456 (T,wt=13): 5755 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(4381(a,1),5311(a,1,1)),rewrite([4381(9)])]. given #457 (T,wt=13): 5756 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(4383(a,1),5311(a,1,1)),rewrite([4383(9)])]. given #458 (T,wt=13): 5757 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(4477(a,1),5311(a,1,1)),rewrite([4477(9)])]. given #459 (T,wt=13): 5769 (x v y) v ((x ^ z) ^ u) = x v y. [para(5301(a,1),5311(a,1,1)),rewrite([5301(7)])]. given #460 (A,wt=16): 5097 (x ^ (y ^ z)) v (x' v (y' v z')) = c_0. [para(3999(a,1),4856(a,1,2,2))]. given #461 (T,wt=13): 5770 (x v y) v ((y ^ z) ^ u) = x v y. [para(5305(a,1),5311(a,1,1)),rewrite([5305(7)])]. given #462 (T,wt=13): 5827 ((x v y) v z) ^ (u ^ x) = u ^ x. [para(5367(a,1),5477(a,1,1,1))]. given #463 (T,wt=13): 5828 (x ^ y) ^ ((y v z) v u) = x ^ y. [para(5367(a,1),5550(a,1,2,1))]. given #464 (T,wt=13): 5829 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(5367(a,1),5555(a,1,1,2))]. given #465 (A,wt=16): 5103 ((x' ^ y') ^ z') v ((x v y) v z) = c_0. [para(27(a,1),4944(a,1,1,1))]. given #466 (T,wt=13): 5830 (x ^ y) ^ (z v (y v u)) = x ^ y. [para(5367(a,1),5582(a,1,2,2))]. given #467 (T,wt=13): 5831 ((x ^ y) ^ z) v (y v u) = y v u. [para(5367(a,1),5301(a,1,2)),rewrite([5367(7)])]. given #468 (T,wt=13): 5832 (x ^ (y ^ z)) v (y v u) = y v u. [para(5301(a,1),5367(a,1,2)),rewrite([5301(7)])]. given #469 (T,wt=13): 5833 (x ^ (y ^ z)) v (u v y) = u v y. [para(5305(a,1),5367(a,1,2)),rewrite([5305(7)])]. given #470 (A,wt=16): 5104 (x' ^ (y' ^ z')) v (x v (y v z)) = c_0. [para(27(a,1),4944(a,1,1,2))]. given #471 (T,wt=13): 5834 (x v y) v ((z ^ x) ^ u) = x v y. [para(5367(a,1),5311(a,1,1)),rewrite([5367(7)])]. given #472 (T,wt=13): 5835 (x ^ (y ^ z)) v (z v u) = z v u. [para(5367(a,1),5367(a,1,2)),rewrite([5367(7)])]. given #473 (T,wt=13): 5836 ((x v y) v z) ^ (u ^ y) = u ^ y. [para(5368(a,1),5477(a,1,1,1))]. given #474 (T,wt=13): 5837 (x ^ y) ^ ((z v y) v u) = x ^ y. [para(5368(a,1),5550(a,1,2,1))]. given #475 (A,wt=16): 5105 ((x' v y') ^ z') v ((x ^ y) v z) = c_0. [para(3999(a,1),4944(a,1,1,1))]. given #476 (T,wt=13): 5838 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(5368(a,1),5555(a,1,1,2))]. given #477 (T,wt=13): 5839 (x ^ y) ^ (z v (u v y)) = x ^ y. [para(5368(a,1),5582(a,1,2,2))]. given #478 (T,wt=13): 5840 ((x ^ y) ^ z) v (u v y) = u v y. [para(5368(a,1),5301(a,1,2)),rewrite([5368(7)])]. given #479 (T,wt=13): 5841 (x v y) v ((z ^ y) ^ u) = x v y. [para(5368(a,1),5311(a,1,1)),rewrite([5368(7)])]. given #480 (A,wt=16): 5106 (x' ^ (y' v z')) v (x v (y ^ z)) = c_0. [para(3999(a,1),4944(a,1,1,2))]. given #481 (T,wt=13): 5842 (x ^ (y ^ z)) v (u v z) = u v z. [para(5368(a,1),5367(a,1,2)),rewrite([5368(7)])]. given #482 (T,wt=13): 5843 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(4381(a,1),5383(a,1,1)),rewrite([4381(9)])]. given #483 (T,wt=13): 5844 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(4383(a,1),5383(a,1,1)),rewrite([4383(9)])]. given #484 (T,wt=13): 5845 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(4477(a,1),5383(a,1,1)),rewrite([4477(9)])]. given #485 (A,wt=23): 5108 (x v y) ^ ((x v ((x v y) ^ z)) ^ u) = (x v ((x v y) ^ z)) ^ u. [para(2427(a,1),3511(a,1,2,1,1)),rewrite([2427(8)])]. given #486 (T,wt=13): 5850 (x v y) v (z ^ (x ^ u)) = x v y. [para(5301(a,1),5383(a,1,1)),rewrite([5301(7)])]. given #487 (T,wt=13): 5851 (x v y) v (z ^ (y ^ u)) = x v y. [para(5305(a,1),5383(a,1,1)),rewrite([5305(7)])]. given #488 (T,wt=13): 5852 (x v y) v (z ^ (u ^ x)) = x v y. [para(5367(a,1),5383(a,1,1)),rewrite([5367(7)])]. given #489 (T,wt=13): 5853 (x v y) v (z ^ (u ^ y)) = x v y. [para(5368(a,1),5383(a,1,1)),rewrite([5368(7)])]. given #490 (A,wt=21): 5111 x ^ (((x ^ y) v (x ^ z)) ^ u) = ((x ^ y) v (x ^ z)) ^ u. [para(2928(a,1),3511(a,1,2,1,1)),rewrite([2928(7)])]. given #491 (T,wt=13): 6083 x v ((((x ^ y) ^ z) ^ u) ^ w) = x. [para(5730(a,1),5311(a,1,1)),rewrite([5730(9)])]. given #492 (T,wt=13): 6085 x v (y ^ (((x ^ z) ^ u) ^ w)) = x. [para(5730(a,1),5383(a,1,1)),rewrite([5730(9)])]. given #493 (T,wt=13): 6102 x v ((((y ^ x) ^ z) ^ u) ^ w) = x. [para(5731(a,1),5311(a,1,1)),rewrite([5731(9)])]. given #494 (T,wt=13): 6104 x v (y ^ (((z ^ x) ^ u) ^ w)) = x. [para(5731(a,1),5383(a,1,1)),rewrite([5731(9)])]. given #495 (A,wt=21): 5113 x ^ (((y ^ x) v (z ^ x)) ^ u) = ((y ^ x) v (z ^ x)) ^ u. [para(4357(a,1),3511(a,1,2,1,2)),rewrite([4357(8)])]. given #496 (T,wt=13): 6123 x v (((y ^ (x ^ z)) ^ u) ^ w) = x. [para(5732(a,1),5311(a,1,1)),rewrite([5732(9)])]. given #497 (T,wt=13): 6125 x v (y ^ ((z ^ (x ^ u)) ^ w)) = x. [para(5732(a,1),5383(a,1,1)),rewrite([5732(9)])]. given #498 (T,wt=13): 6141 x v (((y ^ (z ^ x)) ^ u) ^ w) = x. [para(5733(a,1),5311(a,1,1)),rewrite([5733(9)])]. given #499 (T,wt=13): 6143 x v (y ^ ((z ^ (u ^ x)) ^ w)) = x. [para(5733(a,1),5383(a,1,1)),rewrite([5733(9)])]. given #500 (A,wt=21): 5114 x ^ (y ^ ((z ^ x) v (x ^ u))) = y ^ ((z ^ x) v (x ^ u)). [para(4357(a,1),3511(a,1,2)),rewrite([4357(13)])]. given #501 (T,wt=13): 6282 x v ((y ^ ((x ^ z) ^ u)) ^ w) = x. [para(5823(a,1),5311(a,1,1)),rewrite([5823(9)])]. given #502 (T,wt=13): 6284 x v (y ^ (z ^ ((x ^ u) ^ w))) = x. [para(5823(a,1),5383(a,1,1)),rewrite([5823(9)])]. given #503 (T,wt=13): 6300 x v ((y ^ ((z ^ x) ^ u)) ^ w) = x. [para(5824(a,1),5311(a,1,1)),rewrite([5824(9)])]. given #504 (T,wt=13): 6302 x v (y ^ (z ^ ((u ^ x) ^ w))) = x. [para(5824(a,1),5383(a,1,1)),rewrite([5824(9)])]. given #505 (A,wt=23): 5117 (x v y) ^ ((y v ((x v y) ^ z)) ^ u) = (y v ((x v y) ^ z)) ^ u. [para(4427(a,1),3511(a,1,2,1,1)),rewrite([4427(8)])]. given #506 (T,wt=13): 6319 x v ((y ^ (z ^ (x ^ u))) ^ w) = x. [para(5825(a,1),5311(a,1,1)),rewrite([5825(9)])]. given #507 (T,wt=13): 6321 x v (y ^ (z ^ (u ^ (x ^ w)))) = x. [para(5825(a,1),5383(a,1,1)),rewrite([5825(9)])]. given #508 (T,wt=13): 6335 x v ((y ^ (z ^ (u ^ x))) ^ w) = x. [para(5826(a,1),5311(a,1,1)),rewrite([5826(9)])]. given #509 (T,wt=13): 6337 x v (y ^ (z ^ (u ^ (w ^ x)))) = x. [para(5826(a,1),5383(a,1,1)),rewrite([5826(9)])]. given #510 (A,wt=17): 5120 x v ((y ^ x) v (((z ^ x) v (x ^ u)) ^ w)) = x. [para(3511(a,1),4382(a,1,2,2))]. given #511 (T,wt=13): 6437 x ^ ((((x v y) v z) v u) v w) = x. [para(5918(a,1),5578(a,1,1)),rewrite([5918(9)])]. given #512 (T,wt=13): 6439 x ^ (y v (((x v z) v u) v w)) = x. [para(5918(a,1),5668(a,1,1)),rewrite([5918(9)])]. given #513 (T,wt=13): 6477 x ^ ((((y v x) v z) v u) v w) = x. [para(5919(a,1),5578(a,1,1)),rewrite([5919(9)])]. given #514 (T,wt=13): 6479 x ^ (y v (((z v x) v u) v w)) = x. [para(5919(a,1),5668(a,1,1)),rewrite([5919(9)])]. given #515 (A,wt=17): 5121 x v ((((y ^ x) v (x ^ z)) ^ u) v (x ^ w)) = x. [para(3511(a,1),4476(a,1,2,1))]. given #516 (T,wt=13): 6522 x ^ (((y v (x v z)) v u) v w) = x. [para(5920(a,1),5578(a,1,1)),rewrite([5920(9)])]. given #517 (T,wt=13): 6524 x ^ (y v ((z v (x v u)) v w)) = x. [para(5920(a,1),5668(a,1,1)),rewrite([5920(9)])]. given #518 (T,wt=13): 6562 x ^ (((y v (z v x)) v u) v w) = x. [para(5921(a,1),5578(a,1,1)),rewrite([5921(9)])]. given #519 (T,wt=13): 6564 x ^ (y v ((z v (u v x)) v w)) = x. [para(5921(a,1),5668(a,1,1)),rewrite([5921(9)])]. given #520 (A,wt=17): 5122 x v ((x ^ y) v (((z ^ x) v (x ^ u)) ^ w)) = x. [para(3511(a,1),4476(a,1,2,2))]. given #521 (T,wt=13): 6817 x ^ ((y v ((x v z) v u)) v w) = x. [para(6007(a,1),5578(a,1,1)),rewrite([6007(9)])]. given #522 (T,wt=13): 6819 x ^ (y v (z v ((x v u) v w))) = x. [para(6007(a,1),5668(a,1,1)),rewrite([6007(9)])]. given #523 (T,wt=13): 6858 x ^ ((y v ((z v x) v u)) v w) = x. [para(6008(a,1),5578(a,1,1)),rewrite([6008(9)])]. given #524 (T,wt=13): 6860 x ^ (y v (z v ((u v x) v w))) = x. [para(6008(a,1),5668(a,1,1)),rewrite([6008(9)])]. given #525 (A,wt=17): 5124 x v ((((y ^ x) v (x ^ z)) ^ u) v (w ^ x)) = x. [para(3511(a,1),4543(a,1,2,1))]. given #526 (T,wt=13): 6903 x ^ ((y v (z v (x v u))) v w) = x. [para(6009(a,1),5578(a,1,1)),rewrite([6009(9)])]. given #527 (T,wt=13): 6905 x ^ (y v (z v (u v (x v w)))) = x. [para(6009(a,1),5668(a,1,1)),rewrite([6009(9)])]. given #528 (T,wt=13): 6944 x ^ ((y v (z v (u v x))) v w) = x. [para(6010(a,1),5578(a,1,1)),rewrite([6010(9)])]. given #529 (T,wt=13): 6946 x ^ (y v (z v (u v (w v x)))) = x. [para(6010(a,1),5668(a,1,1)),rewrite([6010(9)])]. given #530 (A,wt=29): 5126 x ^ ((y ^ x) v (((z ^ x) v (x ^ u)) ^ w)) = (y ^ x) v (((z ^ x) v (x ^ u)) ^ w). [para(3511(a,1),3510(a,1,2,2)),rewrite([3511(13)])]. given #531 (T,wt=13): 7308 x v ((y ^ x) v ((x ^ z) ^ u)) = x. [para(5107(a,1),4382(a,1,2,2))]. given #532 (T,wt=13): 7309 x v (((x ^ y) ^ z) v (x ^ u)) = x. [para(5107(a,1),4476(a,1,2,1))]. given #533 (T,wt=13): 7310 x v ((x ^ y) v ((x ^ z) ^ u)) = x. [para(5107(a,1),4476(a,1,2,2))]. given #534 (T,wt=13): 7312 x v (((x ^ y) ^ z) v (u ^ x)) = x. [para(5107(a,1),4543(a,1,2,1))]. given #535 (A,wt=29): 5127 x ^ (((y ^ x) v ((z ^ x) v (x ^ u))) ^ w) = ((y ^ x) v ((z ^ x) v (x ^ u))) ^ w. [para(3510(a,1),3511(a,1,2,1,2)),rewrite([3510(12)])]. Low Water (keep, True_semantics): wt=95 Low Water (keep, True_semantics): wt=92 Low Water (keep, True_semantics): wt=85 given #536 (T,wt=13): 7383 x v ((y ^ x) v ((z ^ x) ^ u)) = x. [para(5112(a,1),4382(a,1,2,2))]. given #537 (T,wt=13): 7384 x v (((y ^ x) ^ z) v (x ^ u)) = x. [para(5112(a,1),4476(a,1,2,1))]. given #538 (T,wt=13): 7385 x v ((x ^ y) v ((z ^ x) ^ u)) = x. [para(5112(a,1),4476(a,1,2,2))]. given #539 (T,wt=13): 7387 x v (((y ^ x) ^ z) v (u ^ x)) = x. [para(5112(a,1),4543(a,1,2,1))]. given #540 (A,wt=41): 5128 x ^ ((y ^ ((z ^ x) v (x ^ u))) v (((z ^ x) v (x ^ u)) ^ w)) = (y ^ ((z ^ x) v (x ^ u))) v (((z ^ x) v (x ^ u)) ^ w). [para(3510(a,1),3511(a,1,2)),rewrite([3510(23)])]. Low Water (keep, True_semantics): wt=65 given #541 (T,wt=13): 7551 x v ((y ^ (x ^ z)) v (x ^ u)) = x. [para(5365(a,1),4382(a,1,2,1))]. given #542 (T,wt=13): 7555 x v ((y ^ (x ^ z)) v (u ^ x)) = x. [para(5365(a,1),4508(a,1,2,1))]. given #543 (T,wt=13): 7556 x v ((y ^ x) v (z ^ (x ^ u))) = x. [para(5365(a,1),4508(a,1,2,2))]. given #544 (T,wt=13): 7557 x v ((x ^ y) v (z ^ (x ^ u))) = x. [para(5365(a,1),4543(a,1,2,2))]. given #545 (A,wt=26): 5129 (((x ^ y) v (y ^ z)) ^ u) v (((x' v y') ^ (y' v z')) v u') = c_0. [para(3511(a,1),4856(a,1,1)),rewrite([3999(10),27(9),3999(7),3999(10),3998(15)])]. Low Water (keep, True_semantics): wt=56 given #546 (T,wt=13): 7798 x v ((y ^ (z ^ x)) v (x ^ u)) = x. [para(5432(a,1),4382(a,1,2,1))]. given #547 (T,wt=13): 7802 x v ((y ^ (z ^ x)) v (u ^ x)) = x. [para(5432(a,1),4508(a,1,2,1))]. given #548 (T,wt=13): 7803 x v ((y ^ x) v (z ^ (u ^ x))) = x. [para(5432(a,1),4508(a,1,2,2))]. given #549 (T,wt=13): 7804 x v ((x ^ y) v (z ^ (u ^ x))) = x. [para(5432(a,1),4543(a,1,2,2))]. given #550 (A,wt=33): 5130 x ^ (((y ^ x) v (((z ^ x) v (x ^ u)) ^ w)) ^ v5) = ((y ^ x) v (((z ^ x) v (x ^ u)) ^ w)) ^ v5. [para(3511(a,1),3511(a,1,2,1,2)),rewrite([3511(14)])]. Low Water (keep, True_semantics): wt=49 given #551 (T,wt=13): 8461 (x v y) v ((x' ^ y') v z) = c_0. [para(27(a,1),8442(a,1,2,1))]. given #552 (T,wt=13): 8463 (x ^ y) v ((x' v y') v z) = c_0. [para(3999(a,1),8442(a,1,2,1))]. given #553 (T,wt=13): 8473 (x' ^ y') v ((x v y) v z) = c_0. [para(27(a,1),8462(a,1,1))]. given #554 (T,wt=13): 8474 (x' v y') v ((x ^ y) v z) = c_0. [para(3999(a,1),8462(a,1,1))]. given #555 (A,wt=45): 5131 x ^ (((y ^ ((z ^ x) v (x ^ u))) v (((z ^ x) v (x ^ u)) ^ w)) ^ v5) = ((y ^ ((z ^ x) v (x ^ u))) v (((z ^ x) v (x ^ u)) ^ w)) ^ v5. [para(3511(a,1),3511(a,1,2)),rewrite([3511(25)])]. Low Water (keep, True_semantics): wt=47 given #556 (T,wt=13): 8625 (x v y) v (z v (x' ^ y')) = c_0. [para(27(a,1),8464(a,1,2,2))]. given #557 (T,wt=13): 8626 (x ^ y) v (z v (x' v y')) = c_0. [para(3999(a,1),8464(a,1,2,2))]. given #558 (T,wt=13): 8633 (x' ^ y') v (z v (x v y)) = c_0. [para(27(a,1),8470(a,1,1))]. given #559 (T,wt=13): 8634 (x' v y') v (z v (x ^ y)) = c_0. [para(3999(a,1),8470(a,1,1))]. given #560 (A,wt=16): 5160 ((x' ^ y') ^ z) v ((x v y) v z') = c_0. [para(27(a,1),5094(a,1,1,1))]. given #561 (T,wt=13): 8830 x' ^ ((y ^ x) v (x ^ z)) = c_0'. [para(3510(a,1),8440(a,1,2))]. given #562 (T,wt=13): 9833 x' ^ (((x ^ y) ^ z) ^ u) = c_0'. [para(5107(a,1),8849(a,1,2,1))]. given #563 (T,wt=13): 9834 x' ^ (((y ^ x) ^ z) ^ u) = c_0'. [para(5112(a,1),8849(a,1,2,1))]. Low Water (keep, True_semantics): wt=46 given #564 (T,wt=13): 9835 x' ^ ((y ^ (x ^ z)) ^ u) = c_0'. [para(5112(a,1),8849(a,1,2))]. Low Water (keep, True_semantics): wt=43 given #565 (A,wt=16): 5161 (x' ^ (y v z)) v (x v (y' ^ z')) = c_0. [para(27(a,1),5094(a,1,2,2))]. given #566 (T,wt=13): 9839 x' ^ (y ^ ((x ^ z) ^ u)) = c_0'. [para(5366(a,1),8849(a,1,2))]. given #567 (T,wt=13): 9841 x' ^ ((y ^ (z ^ x)) ^ u) = c_0'. [para(5433(a,1),8849(a,1,2,1))]. given #568 (T,wt=13): 9842 x' ^ (y ^ (z ^ (x ^ u))) = c_0'. [para(5433(a,1),8849(a,1,2))]. Low Water (keep, True_semantics): wt=41 given #569 (T,wt=13): 9855 x' ^ (y ^ ((z ^ x) ^ u)) = c_0'. [para(5366(a,1),8850(a,1,2))]. given #570 (A,wt=16): 5162 ((x' v y') ^ z) v ((x ^ y) v z') = c_0. [para(3999(a,1),5094(a,1,1,1))]. given #571 (T,wt=13): 9857 x' ^ (y ^ (z ^ (u ^ x))) = c_0'. [para(5433(a,1),8850(a,1,2))]. given #572 (T,wt=13): 9919 x' ^ ((x ^ y) v (x ^ z)) = c_0'. [para(4472(a,1),8978(a,1,1)),rewrite([3999(9),27(5),2291(3),2291(3),27(6),2291(4),2291(4)])]. given #573 (T,wt=13): 9973 x ^ (((x' ^ y) ^ z) ^ u) = c_0'. [para(5107(a,1),8864(a,1,2,1))]. Low Water (keep, True_semantics): wt=40 given #574 (T,wt=13): 9974 x ^ (((y ^ x') ^ z) ^ u) = c_0'. [para(5112(a,1),8864(a,1,2,1))]. given #575 (A,wt=16): 5163 (x' ^ (y ^ z)) v (x v (y' v z')) = c_0. [para(3999(a,1),5094(a,1,2,2))]. given #576 (T,wt=13): 9975 x ^ ((y ^ (x' ^ z)) ^ u) = c_0'. [para(5112(a,1),8864(a,1,2))]. given #577 (T,wt=13): 9976 x ^ (y ^ ((x' ^ z) ^ u)) = c_0'. [para(5366(a,1),8864(a,1,2))]. given #578 (T,wt=13): 9977 x ^ ((y ^ (z ^ x')) ^ u) = c_0'. [para(5433(a,1),8864(a,1,2,1))]. given #579 (T,wt=13): 9978 x ^ (y ^ (z ^ (x' ^ u))) = c_0'. [para(5433(a,1),8864(a,1,2))]. given #580 (A,wt=26): 5169 (((x ^ y') v (y' ^ z)) ^ u) v (((x' v y) ^ (y v z')) v u') = c_0. [para(3511(a,1),5094(a,1,1)),rewrite([3999(13),27(12),3999(9),2291(9),3999(11),2291(10),3998(14)])]. given #581 (T,wt=13): 9989 x ^ (y ^ ((z ^ x') ^ u)) = c_0'. [para(5366(a,1),8865(a,1,2))]. Low Water (keep, True_semantics): wt=38 given #582 (T,wt=13): 9990 x ^ (y ^ (z ^ (u ^ x'))) = c_0'. [para(5433(a,1),8865(a,1,2))]. given #583 (T,wt=13): 10437 (x v y) ^ ((y v x) v z) = x v y. [para(9482(a,1),5550(a,1,2,1))]. given #584 (T,wt=13): 10439 (x v y) ^ (z v (y v x)) = x v y. [para(9482(a,1),5582(a,1,2,2))]. given #585 (A,wt=79): 5170 (((x v (y' v z')) ^ ((y' v z') v u')) v w') ^ ((y' v z') v (((y' v z') v ((v5 ^ (((x v (y' v z')) ^ ((y' v z') v u')) v w')) ^ (v5' v (((x' ^ (y ^ z)) v ((y ^ z) ^ u)) ^ w)))) ^ v6)) = y' v z'. [para(3527(a,1),27(a,1,1)),rewrite([3999(2),3999(11),27(10),3999(7),2291(5),3999(5),3999(10),3999(9),3999(45),3999(17),27(46),3999(44),3999(20),27(45),27(31),2291(23),3999(29),27(28),3999(25),2291(23),3999(23),3999(28),3999(27),3999(48),27(48),3999(46),27(40),27(40),2291(38),2291(38),27(44),27(42),2291(40),2291(40),2291(41),2291(43),2291(47)]),flip(a)]. Low Water (keep, True_semantics): wt=37 given #586 (T,wt=13): 10440 (x v y) v ((y v x) ^ z) = x v y. [para(9482(a,1),5301(a,1,2)),rewrite([10434(4),9482(7)])]. given #587 (T,wt=13): 10441 (x v y) v (z ^ (y v x)) = x v y. [para(9482(a,1),5367(a,1,2)),rewrite([10434(4),9482(7)])]. given #588 (T,wt=13): 10461 (x' ^ y') v ((y v x) v z) = c_0. [para(9482(a,1),8498(a,1,2,1)),rewrite([27(2)])]. given #589 (T,wt=13): 10462 (x' ^ y') v (z v (y v x)) = c_0. [para(9482(a,1),8500(a,1,2,2)),rewrite([27(2)])]. given #590 (A,wt=16): 5218 (x ^ (y' ^ z')) v (x' v (y v z)) = c_0. [para(27(a,1),5095(a,1,1,2))]. given #591 (T,wt=13): 10463 (x v y) v ((y' ^ x') v z) = c_0. [para(9482(a,1),9115(a,1,2)),rewrite([27(2),10434(6)])]. given #592 (T,wt=13): 10464 (x v y) v (z v (y' ^ x')) = c_0. [para(9482(a,1),9122(a,1,2)),rewrite([27(2),10434(6)])]. given #593 (T,wt=13): 10584 (x v y) v (y v (z ^ x)) = x v y. [back_rewrite(9737),rewrite([10434(4)])]. given #594 (T,wt=13): 10585 (x v y) v (y v (x ^ z)) = x v y. [back_rewrite(9735),rewrite([10434(4)])]. given #595 (A,wt=16): 5219 ((x v y) ^ z') v ((x' ^ y') v z) = c_0. [para(27(a,1),5095(a,1,2,1))]. Low Water (keep, True_semantics): wt=35 given #596 (T,wt=13): 10606 (x v y) v ((z ^ x) v y) = x v y. [back_rewrite(9611),rewrite([10434(4)])]. given #597 (T,wt=13): 10608 (x v y) v ((x ^ z) v y) = x v y. [back_rewrite(9609),rewrite([10434(4)])]. given #598 (T,wt=13): 10650 (x v y) v ((z ^ y) v x) = x v y. [back_rewrite(9498),rewrite([10434(4)])]. given #599 (T,wt=13): 10651 (x v y) v ((y ^ z) v x) = x v y. [back_rewrite(9497),rewrite([10434(4)])]. given #600 (A,wt=16): 5220 (x ^ (y' v z')) v (x' v (y ^ z)) = c_0. [para(3999(a,1),5095(a,1,1,2))]. given #601 (T,wt=13): 10673 (x v y) v (x v (z ^ y)) = x v y. [back_rewrite(9385),rewrite([10434(4)])]. given #602 (T,wt=13): 10674 (x v y) v (x v (y ^ z)) = x v y. [back_rewrite(9384),rewrite([10434(4)])]. given #603 (T,wt=13): 11845 ((x ^ y) ^ z) ^ (x' ^ u) = c_0'. [para(5107(a,1),9838(a,1,1))]. Low Water (keep, True_semantics): wt=34 given #604 (T,wt=13): 11846 (x ^ y) ^ ((x' ^ z) ^ u) = c_0'. [para(5107(a,1),9838(a,1,2))]. given #605 (A,wt=16): 5221 ((x ^ y) ^ z') v ((x' v y') v z) = c_0. [para(3999(a,1),5095(a,1,2,1))]. given #606 (T,wt=13): 11847 ((x ^ y) ^ z) ^ (y' ^ u) = c_0'. [para(5112(a,1),9838(a,1,1))]. given #607 (T,wt=13): 11848 (x ^ y) ^ ((z ^ x') ^ u) = c_0'. [para(5112(a,1),9838(a,1,2))]. given #608 (T,wt=13): 11851 (x ^ (y ^ z)) ^ (y' ^ u) = c_0'. [para(5366(a,1),9838(a,1,1))]. given #609 (T,wt=13): 11852 (x ^ y) ^ (z ^ (x' ^ u)) = c_0'. [para(5366(a,1),9838(a,1,2))]. Low Water (keep, True_semantics): wt=32 given #610 (A,wt=17): 5226 ((x' ^ y') ^ z') ^ ((x v y) v z) = c_0'. [para(27(a,1),4992(a,1,1,1))]. given #611 (T,wt=13): 11853 (x ^ (y ^ z)) ^ (z' ^ u) = c_0'. [para(5433(a,1),9838(a,1,1))]. Low Water (keep, True_semantics): wt=31 given #612 (T,wt=13): 11854 (x ^ y) ^ (z ^ (u ^ x')) = c_0'. [para(5433(a,1),9838(a,1,2))]. given #613 (T,wt=13): 11872 ((x ^ y) ^ z) ^ (u ^ x') = c_0'. [para(5107(a,1),9840(a,1,1))]. given #614 (T,wt=13): 11873 ((x ^ y) ^ z) ^ (u ^ y') = c_0'. [para(5112(a,1),9840(a,1,1))]. given #615 (A,wt=17): 5227 (x' ^ (y' ^ z')) ^ (x v (y v z)) = c_0'. [para(27(a,1),4992(a,1,1,2))]. given #616 (T,wt=13): 11876 (x ^ (y ^ z)) ^ (u ^ y') = c_0'. [para(5366(a,1),9840(a,1,1))]. given #617 (T,wt=13): 11877 (x ^ (y ^ z)) ^ (u ^ z') = c_0'. [para(5433(a,1),9840(a,1,1))]. given #618 (T,wt=13): 11886 (x ^ y) ^ ((y' ^ z) ^ u) = c_0'. [para(5107(a,1),9854(a,1,2))]. given #619 (T,wt=13): 11887 (x ^ y) ^ ((z ^ y') ^ u) = c_0'. [para(5112(a,1),9854(a,1,2))]. given #620 (A,wt=17): 5228 ((x' v y') ^ z') ^ ((x ^ y) v z) = c_0'. [para(3999(a,1),4992(a,1,1,1))]. given #621 (T,wt=13): 11888 (x ^ y) ^ (z ^ (y' ^ u)) = c_0'. [para(5366(a,1),9854(a,1,2))]. given #622 (T,wt=13): 11889 (x ^ y) ^ (z ^ (u ^ y')) = c_0'. [para(5433(a,1),9854(a,1,2))]. given #623 (T,wt=13): 11927 ((x' ^ y) ^ z) ^ (x ^ u) = c_0'. [para(5107(a,1),9948(a,1,1))]. given #624 (T,wt=13): 11928 (x' ^ y) ^ ((x ^ z) ^ u) = c_0'. [para(5107(a,1),9948(a,1,2))]. given #625 (A,wt=17): 5229 (x' ^ (y' v z')) ^ (x v (y ^ z)) = c_0'. [para(3999(a,1),4992(a,1,1,2))]. given #626 (T,wt=13): 11929 ((x ^ y') ^ z) ^ (y ^ u) = c_0'. [para(5112(a,1),9948(a,1,1))]. given #627 (T,wt=13): 11930 (x' ^ y) ^ ((z ^ x) ^ u) = c_0'. [para(5112(a,1),9948(a,1,2))]. given #628 (T,wt=13): 11933 (x ^ (y' ^ z)) ^ (y ^ u) = c_0'. [para(5366(a,1),9948(a,1,1))]. given #629 (T,wt=13): 11934 (x' ^ y) ^ (z ^ (x ^ u)) = c_0'. [para(5366(a,1),9948(a,1,2))]. given #630 (A,wt=67): 5273 (((x v (y' v z')) ^ ((y' v z') v u')) v w') v ((y' v z') v ((((x v (y' v z')) ^ ((y' v z') v u')) v w') ^ v5)) = ((x v (y' v z')) ^ ((y' v z') v u')) v w'. [para(3529(a,1),4476(a,1,2,1))]. given #631 (T,wt=13): 11935 (x ^ (y ^ z')) ^ (z ^ u) = c_0'. [para(5433(a,1),9948(a,1,1))]. given #632 (T,wt=13): 11936 (x' ^ y) ^ (z ^ (u ^ x)) = c_0'. [para(5433(a,1),9948(a,1,2))]. given #633 (T,wt=13): 11956 (x ^ y') ^ ((y ^ z) ^ u) = c_0'. [para(5107(a,1),9949(a,1,2))]. Low Water (keep, True_semantics): wt=29 given #634 (T,wt=13): 11957 (x ^ y') ^ ((z ^ y) ^ u) = c_0'. [para(5112(a,1),9949(a,1,2))]. given #635 (A,wt=17): 5286 ((x v y) ^ z) ^ ((x' ^ y') v z') = c_0'. [para(27(a,1),5067(a,1,2,1))]. given #636 (T,wt=13): 11960 (x ^ y') ^ (z ^ (y ^ u)) = c_0'. [para(5366(a,1),9949(a,1,2))]. given #637 (T,wt=13): 11961 (x ^ y') ^ (z ^ (u ^ y)) = c_0'. [para(5433(a,1),9949(a,1,2))]. given #638 (T,wt=13): 11969 ((x' ^ y) ^ z) ^ (u ^ x) = c_0'. [para(5107(a,1),9962(a,1,1))]. given #639 (T,wt=13): 11970 ((x ^ y') ^ z) ^ (u ^ y) = c_0'. [para(5112(a,1),9962(a,1,1))]. given #640 (A,wt=17): 5287 (x ^ (y v z)) ^ (x' v (y' ^ z')) = c_0'. [para(27(a,1),5067(a,1,2,2))]. given #641 (T,wt=13): 11971 (x ^ (y' ^ z)) ^ (u ^ y) = c_0'. [para(5366(a,1),9962(a,1,1))]. given #642 (T,wt=13): 11972 (x ^ (y ^ z')) ^ (u ^ z) = c_0'. [para(5433(a,1),9962(a,1,1))]. given #643 (T,wt=13): 12702 x' ^ ((y ^ x) v (z ^ x)) = c_0'. [para(4539(a,1),8440(a,1,2))]. given #644 (T,wt=13): 12786 x' ^ ((x ^ y) v (z ^ x)) = c_0'. [para(4547(a,1),8440(a,1,2))]. given #645 (A,wt=17): 5288 ((x ^ y) ^ z) ^ ((x' v y') v z') = c_0'. [para(3999(a,1),5067(a,1,2,1))]. given #646 (T,wt=13): 13361 x v (y v ((y v x) ^ z)) = y v x. [para(5069(a,1),4510(a,1,2,2)),rewrite([9493(6)])]. given #647 (T,wt=11): 25998 x v (y v (x ^ z)) = y v x. [para(5612(a,1),13361(a,1,2,2))]. given #648 (T,wt=11): 25999 x v (y v (z ^ x)) = y v x. [para(5614(a,1),13361(a,1,2,2))]. % Operation v is associative-commutative; CAC redundancy checks enabled. ============================== PROOF ================================= % Proof 3 at 16.42 (+ 0.09) seconds: combined. % Length of proof is 189. % Level of proof is 36. % Maximum clause weight is 77. % Given clauses 648. 4 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) & f(f(x,x),f(x,y)) = x & f(x,f(x,x)) = f(y,f(y,y)) # answer(combined) # label(non_clause) # label(goal). [goal]. 5 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z))) = y # label(OL_Sh). [assumption]. 6 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 7 f(f(x,x),f(y,y)) = x v y. [copy(6),flip(a)]. 8 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. 9 f(f(x,y),f(x,y)) = x ^ y. [copy(8),flip(a)]. 10 x' = f(x,x) # label(definition_complementation). [assumption]. 11 f(x,x) = x'. [copy(10),flip(a)]. 18 f(c8,f(f(c9,c10),f(c9,c10))) != f(c9,f(f(c8,c10),f(c8,c10))) | f(f(c8,c8),f(c8,c9)) != c8 | f(c8,f(c8,c8)) != f(c9,f(c9,c9)) # answer(combined). [deny(4)]. 19 f(c9,f(c8,c10)') != f(c8,f(c9,c10)') | f(c8',f(c8,c9)) != c8 | f(c9,c9') != f(c8,c8') # answer(combined). [copy(18),rewrite([11(8),11(14),11(16),11(25),11(29)]),flip(a),flip(c)]. 20 f(x,y)' = x ^ y. [back_rewrite(9),rewrite([11(3)])]. 21 f(x',y') = x v y. [back_rewrite(7),rewrite([11(1),11(2)])]. 22 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(x',x)),z))) = y. [back_rewrite(5),rewrite([11(5)])]. 23 f(c9,c8 ^ c10) != f(c8,c9 ^ c10) | f(c8',f(c8,c9)) != c8 | f(c9,c9') != f(c8,c8') # answer(combined). [back_rewrite(19),rewrite([20(5),20(10)])]. 25 x ^ x = x''. [para(11(a,1),20(a,1,1)),flip(a)]. 27 (x v y)' = x' ^ y'. [para(21(a,1),20(a,1,1))]. 28 f(x ^ y,z') = f(x,y) v z. [para(20(a,1),21(a,1,1))]. 29 f(x',y ^ z) = x v f(y,z). [para(20(a,1),21(a,1,2))]. 30 f(f(f(x',f(x,y)),z),f(x,f(f(x,f(x',x)),y))) = x. [para(11(a,1),22(a,1,1,1,1))]. 31 f(f(f(f(x,y),y'),z),f(y,f(f(y,f(x',x)),y))) = y. [para(11(a,1),22(a,1,1,1,2))]. 32 f(f(x'',y),f(x,f(f(x,f(x',x)),x))) = x. [para(11(a,1),22(a,1,1,1)),rewrite([11(1)])]. 33 f(f(x,y) ^ f(y,z),f(y,f(f(y,f(x',x)),z))) = y. [para(11(a,1),22(a,1,1)),rewrite([20(4)])]. 34 f(f(f(f(x,f(x',x)),f(f(x',x),y)),z),f(f(x',x),f(x' ^ x,y))) = f(x',x). [para(11(a,1),22(a,1,2,2,1)),rewrite([20(13)])]. 35 f(f(f(f(x,y),f(y,f(y,f(x',x)))),z),f(y,y ^ f(x',x))) = y. [para(11(a,1),22(a,1,2,2)),rewrite([20(11)])]. 36 f(f(f(x,y),f(y,z)),u) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(22(a,1),20(a,1,1)),flip(a)]. 38 f(f(f(x v y,f(y',z)),u),f(y',f(f(y',x' v x),z))) = y'. [para(21(a,1),22(a,1,1,1,1)),rewrite([21(11)])]. 43 f(f(x,y),f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z',z)),u)))) = x. [para(22(a,1),22(a,1,1,1)),rewrite([20(5)])]. 53 f(x' ^ f(x,y),f(x,f(f(x,f(x',x)),y))) = x. [para(11(a,1),30(a,1,1)),rewrite([20(4)])]. 62 f(x,f(f(x,y),f(f(f(x,y),x' v x),z))) = f(x,y). [para(30(a,1),22(a,1,1)),rewrite([21(6)])]. 67 f(f(f((x ^ y)',f(x,y) v z),u),f(x ^ y,f(f(x ^ y,(x ^ y) v f(x,y)),z'))) = x ^ y. [para(28(a,1),30(a,1,1,1,2)),rewrite([29(12)])]. 75 f(x''',f(x,f(f(x,f(x',x)),x))) = x. [para(11(a,1),32(a,1,1))]. 76 f(x'',y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(32(a,1),20(a,1,1)),flip(a)]. 78 f(x' v y,f(x,f(f(x,f(x',x)),x))) = x. [para(21(a,1),32(a,1,1))]. 87 f(x,f(x',f(f(x',x' v x),y))) = x'. [para(32(a,1),30(a,1,1)),rewrite([21(6)])]. 89 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(75(a,1),20(a,1,1)),flip(a)]. 97 (x' v y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(78(a,1),20(a,1,1)),flip(a)]. 105 f(f(x,y) ^ y',f(y,f(f(y,f(x',x)),y))) = y. [para(11(a,1),31(a,1,1)),rewrite([20(4)])]. 107 f(f(f(x,y),y'),z) ^ f(y,f(f(y,f(x',x)),y)) = y'. [para(31(a,1),20(a,1,1)),flip(a)]. 132 x ^ f(x',f(f(x',x' v x),y)) = x''. [para(87(a,1),20(a,1,1)),flip(a)]. 140 f(x',f(x'',x)) = x''. [para(32(a,1),87(a,1,2,2))]. 144 f(x'',x'' v x) = x'''. [para(21(a,1),140(a,1,2))]. 166 (f(x,y) ^ f(y,z)) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(33(a,1),20(a,1,1)),flip(a)]. 256 (x'' v y) ^ f(x',f(f(x',x' v x),x')) = x''. [para(21(a,1),97(a,1,2,2,1,2))]. 281 f(x,f(f(x,y),f(x,y) ^ (x' v x))) = f(x,y). [para(30(a,1),35(a,1,1)),rewrite([21(6)])]. 346 f(x,f(x',x' v x)) = x'. [para(281(a,1),87(a,1,2))]. 357 f(f(x,y),f(x ^ y,(x ^ y) v f(x,y))) = x ^ y. [para(20(a,1),346(a,1,2,1)),rewrite([20(4),20(9)])]. 380 f(x,y) ^ f(x,f(f(x,f(f(z,x) ^ f(x,u),f(f(z,x),f(x,u)))),f(f(x,f(z',z)),u))) = x'. [para(22(a,1),36(a,1,1,1)),rewrite([20(5)])]. 392 x ^ f(f(x,y),f(f(f(x,y),x' v x),z)) = x ^ y. [para(30(a,1),36(a,1,1)),rewrite([21(6),20(10)])]. 521 f(x''',y) ^ f(x',f(f(x',x' v x),x')) = x''. [para(21(a,1),76(a,1,2,2,1,2))]. 673 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),62(a,1,2,2))]. 679 f(f(x,y),f(f(f(x,y),y'),y)) = f(f(x,y),y'). [para(31(a,1),62(a,1,2,2))]. 689 f(x,f(f(x,y),x' v x)) = f(x,y). [para(281(a,1),62(a,1,2))]. 770 f(x''',f(x,x'''' v x''')) = x. [para(75(a,1),689(a,1,2,1)),rewrite([75(22)])]. 832 x' ^ f(f(x',f(x,y)),x) = x' ^ f(x,y). [para(673(a,1),20(a,1,1)),rewrite([20(4)]),flip(a)]. 834 f(x'',f(f(x'',x v y),x')) = f(x'',x v y). [para(21(a,1),673(a,1,2,1,2)),rewrite([21(14)])]. 863 f((f(x,y) ^ y')',f(f((f(x,y) ^ y')',y),f(x,y) ^ y')) = f((f(x,y) ^ y')',y). [para(105(a,1),673(a,1,2,1,2)),rewrite([105(27)])]. 920 x'' ^ f(f(x'',x v y),x') = x'' ^ (x v y). [para(21(a,1),832(a,1,2,1,2)),rewrite([21(14)])]. 930 (x' ^ f(x,y))' ^ f(f((x' ^ f(x,y))',x),x' ^ f(x,y)) = (x' ^ f(x,y))' ^ x. [para(53(a,1),832(a,1,2,1,2)),rewrite([53(27)])]. 934 f(x,y) ^ f(f(f(x,y),y'),y) = f(x,y) ^ y'. [para(679(a,1),20(a,1,1)),rewrite([20(4)]),flip(a)]. 988 f(f(f(x,x ^ (x'''' v x''')),y),f(f(x,x'''' v x'''),f(f(f(x,x'''' v x'''),x''' v x''),f(x,x'''' v x''')))) = f(x,x'''' v x'''). [para(770(a,1),31(a,1,1,1,1)),rewrite([20(10),21(37)])]. 1140 x'' ^ f(x' v f(x'',x),f(x'',x)) = x'' ^ (x'' ^ x). [para(140(a,1),934(a,1,1)),rewrite([140(7),20(8),29(8),140(17),20(18)])]. 1606 f(x,x'') = x'. [para(43(a,1),87(a,1,2,2)),rewrite([11(3)])]. 1625 x ^ x'' = x''. [para(43(a,1),132(a,1,2,2)),rewrite([11(3)])]. 1626 f(f(x,y),f(y,y ^ f(x',x))) = y. [para(43(a,1),35(a,1,1))]. 1658 f(x,x ^ y) = f(x,y). [para(43(a,1),62(a,1,2,2)),rewrite([11(3),20(2)])]. 1677 (x ^ y) ^ f(f(x ^ y,x),f(x,y)) = (x ^ y) ^ x. [para(43(a,1),832(a,1,2,1,2)),rewrite([20(2),20(3),20(8),43(23)])]. 1704 x ^ (x ^ y) = x ^ y. [para(43(a,1),392(a,1,2,2)),rewrite([11(3),20(2)])]. 1717 f(f(x,y),f(y,f(x',x))) = y. [back_rewrite(1626),rewrite([1658(5)])]. 1758 f(f(f(x,x'''' v x'''),y),f(f(x,x'''' v x'''),f(f(f(x,x'''' v x'''),x''' v x''),f(x,x'''' v x''')))) = f(x,x'''' v x'''). [back_rewrite(988),rewrite([1658(10)])]. 1903 x'' ^ f(x' v f(x'',x),f(x'',x)) = x'' ^ x. [back_rewrite(1140),rewrite([1704(18)])]. 1943 x v x'' = x''. [para(1606(a,1),21(a,1)),flip(a)]. 2013 f(f(x'',y),x') = x. [para(32(a,1),1658(a,2)),rewrite([76(12)])]. 2014 x'' v x = x. [para(75(a,1),1658(a,2)),rewrite([89(12),21(5)])]. 2017 f(f(f(f(x,y),y'),z),y') = y. [para(31(a,1),1658(a,2)),rewrite([107(14)])]. 2021 f(f(x,y),f(y,z)) v y = y. [para(33(a,1),1658(a,2)),rewrite([166(12),28(5)])]. 2022 f(x'',x) = x'''. [para(144(a,1),1658(a,2)),rewrite([2014(7),1658(6)])]. 2063 f(f(x,y),x') = x. [para(43(a,1),1658(a,2)),rewrite([380(17)])]. 2064 x'' ^ x = x''''. [back_rewrite(1903),rewrite([2022(6),1943(7),2022(8),11(9),1625(7)]),flip(a)]. 2083 x'' ^ (x v y) = x''''. [back_rewrite(920),rewrite([2013(8),2064(3)]),flip(a)]. 2085 f(x'',x v y) = x'''. [back_rewrite(834),rewrite([2013(8),2022(3)]),flip(a)]. 2291 x'' = x. [para(11(a,1),2063(a,1,1)),rewrite([11(3)])]. 2292 f(x,y) ^ x' = x'. [para(2063(a,1),20(a,1,1)),flip(a)]. 2294 f(x v y,x) = x'. [para(21(a,1),2063(a,1,1)),rewrite([2291(3)])]. 2302 f(x,y') = x' v y. [para(78(a,1),2063(a,1,1)),rewrite([27(3),2291(2),1658(3)])]. 2310 f(f((x ^ f(x',x)) v x,y),f(f(x',x),f(x' ^ x,x))) = f(x',x). [para(2063(a,1),34(a,1,1,1,2)),rewrite([2302(5),20(4),2291(11)])]. 2325 (x ^ y)' = f(x,y). [para(357(a,1),2063(a,1,1)),rewrite(