============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 26987 was started by mccune on cleo, Fri Apr 13 09:17:30 2007 The command was "/home/mccune/bin/prover9 -f olsax2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file olsax2.in assign(max_seconds,300). assign(new_constants,1). lex([',^,v,f]). set(restrict_denials). assign(max_weight,40). formulas(sos). 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(goal). [goal]. 2 f(f(x,x),f(x,y)) = x # answer(absorb) # label(goal). [goal]. 3 f(x,f(x,x)) = f(y,f(y,y)) # answer(one) # 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(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: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, ', ^, v, f ]). Skipping inverse_order, because there is a lex command. Skipping unfold_eq, becaure there is a lex command. Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 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=14): 43 f(x',y' ^ z') = x v (y v z). [para(27(a,1),21(a,1,2))]. given #12 (T,wt=15): 45 f(x ^ y,z ^ u) = f(x,y) v f(z,u). [para(20(a,1),28(a,1,2))]. given #13 (T,wt=16): 53 f(x',y ^ z) v u = (x v f(y,z)) v u. [para(29(a,1),28(a,2,1)),rewrite(28(5))]. given #14 (T,wt=17): 48 f(x ^ y,z' ^ u') = f(x,y) v (z v u). [para(27(a,1),28(a,1,2))]. 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): 52 f(x' ^ y',z ^ u) = (x v y) v f(z,u). [para(27(a,1),29(a,1,1))]. given #17 (T,wt=17): 54 f(x',(y ^ z) ^ u') = x v (f(y,z) v u). [para(28(a,1),29(a,2,2))]. given #18 (T,wt=17): 55 f(x',y' ^ (z ^ u)) = x v (y v f(z,u)). [para(29(a,1),29(a,2,2))]. given #19 (T,wt=16): 149 x v f(y',z ^ u) = x v (y v f(z,u)). [para(55(a,1),29(a,1)),flip(a)]. given #20 (A,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 #21 (T,wt=17): 181 f(x''',f(x,f(f(x,f(x',x)),x))) = x. [para(11(a,1),32(a,1,1))]. given #22 (T,wt=17): 184 f(x' v y,f(x,f(f(x,f(x',x)),x))) = x. [para(21(a,1),32(a,1,1))]. given #23 (T,wt=17): 190 f(x,f(x',f(f(x',x' v x),y))) = x'. [para(32(a,1),30(a,1,1)),rewrite(21(6))]. given #24 (T,wt=12): 209 f(x',f(x'',x)) = x''. [para(32(a,1),190(a,1,2,2))]. given #25 (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 #26 (T,wt=13): 210 x' ^ f(x'',x) = x'''. [para(209(a,1),20(a,1,1)),flip(a)]. given #27 (T,wt=14): 212 f(x'',x'' v x) = x'''. [para(21(a,1),209(a,1,2))]. given #28 (T,wt=15): 202 f(x,f(x',x' ^ (x' v x))) = x'. [para(11(a,1),190(a,1,2,2)),rewrite(20(6))]. given #29 (T,wt=14): 267 f(x,x v f(x',x' v x)) = x'. [para(29(a,1),202(a,1,2))]. given #30 (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 #31 (T,wt=15): 253 x'' ^ (x'' v x) = x''''. [para(21(a,1),210(a,1,2))]. given #32 (T,wt=15): 273 x ^ (x v f(x',x' v x)) = x''. [para(267(a,1),20(a,1,1)),flip(a)]. given #33 (T,wt=16): 263 x ^ f(x',x' ^ (x' v x)) = x''. [para(202(a,1),20(a,1,1)),flip(a)]. given #34 (T,wt=17): 211 f(x ^ y,f((x ^ y)',f(x,y))) = (x ^ y)'. [para(20(a,1),209(a,1,1)),rewrite(20(3),20(8))]. given #35 (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 #36 (T,wt=18): 192 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(181(a,1),20(a,1,1)),flip(a)]. given #37 (T,wt=18): 197 (x' v y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(184(a,1),20(a,1,1)),flip(a)]. given #38 (T,wt=18): 203 x ^ f(x',f(f(x',x' v x),y)) = x''. [para(190(a,1),20(a,1,1)),flip(a)]. given #39 (T,wt=18): 252 (x ^ y) ^ f((x ^ y)',f(x,y)) = (x ^ y)''. [para(20(a,1),210(a,1,1)),rewrite(20(3),20(8))]. given #40 (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 #41 (T,wt=18): 325 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 #42 (T,wt=12): 408 f(x,f(x',x' v x)) = x'. [para(325(a,1),190(a,1,2))]. given #43 (T,wt=13): 412 x ^ f(x',x' v x) = x''. [para(325(a,1),203(a,1,2))]. given #44 (T,wt=18): 328 f(x,f(x',x' ^ f(y ^ x,f(y,x)))) = x'. [para(31(a,1),35(a,1,1)),rewrite(20(4))]. given #45 (A,wt=27): 37 f(f(f(f(f(x,y),z),f(z,u)),v),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 #46 (T,wt=17): 444 f(x,x v f(x',f(y ^ x,f(y,x)))) = x'. [para(29(a,1),328(a,1,2))]. given #47 (T,wt=18): 384 x ^ f(f(x,y),f(x,y) ^ (x' v x)) = x ^ y. [para(325(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. given #48 (T,wt=18): 475 x ^ (x v f(x',f(y ^ x,f(y,x)))) = x''. [para(444(a,1),20(a,1,1)),flip(a)]. given #49 (T,wt=19): 56 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 #50 (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 #51 (T,wt=19): 71 f(x',(y' ^ z') ^ u') = x v ((y v z) v u). [para(27(a,1),43(a,1,2,1))]. given #52 (T,wt=19): 72 f(x',y' ^ (z' ^ u')) = x v (y v (z v u)). [para(27(a,1),43(a,1,2,2))]. given #53 (T,wt=19): 76 f(x ^ y,z ^ u) v v = (f(x,y) v f(z,u)) v v. [para(45(a,1),28(a,2,1)),rewrite(28(5))]. given #54 (T,wt=19): 102 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 #55 (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 #56 (T,wt=19): 167 x v f(y ^ z,u ^ v) = x v (f(y,z) v f(u,v)). [para(20(a,1),149(a,1,2,1))]. given #57 (T,wt=19): 182 f(x'',y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(32(a,1),20(a,1,1)),flip(a)]. given #58 (T,wt=19): 216 f((x ^ y)',(x ^ y)' v f(x,y)) = (x ^ y)''. [para(29(a,1),209(a,1,2))]. given #59 (T,wt=19): 415 f(f(x,y),f(x ^ y,(x ^ y) v f(x,y))) = x ^ y. [para(20(a,1),408(a,1,2,1)),rewrite(20(4),20(9))]. given #60 (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 #61 (T,wt=19): 437 x ^ f(x',x' ^ f(y ^ x,f(y,x))) = x''. [para(328(a,1),20(a,1,1)),flip(a)]. given #62 (T,wt=20): 63 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 #63 (T,wt=14): 782 f(x,f(f(x,y),x' v x)) = f(x,y). [para(325(a,1),63(a,1,2))]. given #64 (T,wt=14): 794 x ^ f(f(x,y),x' v x) = x ^ y. [para(782(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. given #65 (A,wt=34): 41 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 #66 (T,wt=8): 861 f(x,x'') = x'. [para(41(a,1),190(a,1,2,2)),rewrite(11(3))]. given #67 (T,wt=9): 866 x ^ x'' = x''. [para(41(a,1),203(a,1,2,2)),rewrite(11(3))]. given #68 (T,wt=9): 878 f(x,x ^ y) = f(x,y). [para(41(a,1),63(a,1,2,2)),rewrite(11(3),20(2))]. given #69 (T,wt=7): 993 x'' v x = x. [para(181(a,1),878(a,2)),rewrite(192(12),21(5))]. restricted denial: (wt=17): 1130 (c2 ^ (c1 ^ c3))''' != (c1 ^ (c2 ^ c3))''' # answer(assoc). [back_rewrite(24),rewrite(1061(5),1061(13))]. restricted denial: (wt=46): 1131 (c9 ^ (c8 ^ c10))''' != (c8 ^ (c9 ^ c10))''' | (c8' ^ (c8 ^ c9)''')''' != c8 | (c9 ^ c9')''' != (c8 ^ c8')''' # answer(combined). [back_rewrite(23),rewrite(1061(5),1061(13),1061(22),1061(26),1061(35),1061(42))]. restricted denial: (wt=15): 1132 (c7 ^ c7')''' != (c6 ^ c6')''' # answer(one). [back_rewrite(17),rewrite(1061(4),1061(11))]. restricted denial: (wt=14): 1133 (c4' ^ (c4 ^ c5)''')''' != c4 # answer(absorb). [back_rewrite(15),rewrite(1061(5),1061(9))]. given #70 (A,wt=9): 978 x ^ (x ^ y) = x ^ y. [para(878(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. given #71 (T,wt=7): 1103 x'''' = x. [back_rewrite(879),rewrite(1061(1),1061(6),1062(10),1096(11),1061(12),1061(16),1102(16))]. given #72 (T,wt=7): 1136 x'' ^ x = x. [back_rewrite(1046),rewrite(1103(7))]. given #73 (T,wt=10): 1061 f(x,y) = (x ^ y)'''. [para(993(a,1),29(a,2)),rewrite(20(2),999(5)),flip(a)]. given #74 (T,wt=12): 1062 x v y = (x' ^ y')'''. [para(993(a,1),43(a,2,2)),rewrite(1046(6),1059(6),1061(3)),flip(a)]. given #75 (A,wt=14): 1073 ((x ^ y)''' ^ x')''' = x. [back_rewrite(1023),rewrite(1061(1),1061(6))]. ============================== PROOF ================================= % Proof 1 at 0.24 (+ 0.00) seconds: absorb. % Length of proof is 58. % Level of proof is 16. % Maximum clause weight is 36. % Given clauses 75. 2 f(f(x,x),f(x,y)) = x # answer(absorb) # 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))]. 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))]. 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)]. 41 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))]. 43 f(x',y' ^ z') = x v (y v z). [para(27(a,1),21(a,1,2))]. 63 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))]. 181 f(x''',f(x,f(f(x,f(x',x)),x))) = x. [para(11(a,1),32(a,1,1))]. 190 f(x,f(x',f(f(x',x' v x),y))) = x'. [para(32(a,1),30(a,1,1)),rewrite(21(6))]. 192 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(181(a,1),20(a,1,1)),flip(a)]. 209 f(x',f(x'',x)) = x''. [para(32(a,1),190(a,1,2,2))]. 210 x' ^ f(x'',x) = x'''. [para(209(a,1),20(a,1,1)),flip(a)]. 212 f(x'',x'' v x) = x'''. [para(21(a,1),209(a,1,2))]. 253 x'' ^ (x'' v x) = x''''. [para(21(a,1),210(a,1,2))]. 325 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))]. 352 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))]. 765 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),63(a,1,2,2))]. 782 f(x,f(f(x,y),x' v x)) = f(x,y). [para(325(a,1),63(a,1,2))]. 794 x ^ f(f(x,y),x' v x) = x ^ y. [para(782(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. 861 f(x,x'') = x'. [para(41(a,1),190(a,1,2,2)),rewrite(11(3))]. 878 f(x,x ^ y) = f(x,y). [para(41(a,1),63(a,1,2,2)),rewrite(11(3),20(2))]. 879 f(f(x,y),f(x,(x ^ y) v f(x,y))) = x. [para(41(a,1),782(a,1,2,1)),rewrite(20(3),41(22))]. 880 f(x,y) ^ f(x,(x ^ y) v f(x,y)) = x'. [para(41(a,1),794(a,1,2,1)),rewrite(20(3),352(22))]. 939 f(f(x,y),(x ^ y)') = x ^ y. [para(20(a,1),861(a,1,2,1)),rewrite(20(6))]. 993 x'' v x = x. [para(181(a,1),878(a,2)),rewrite(192(12),21(5))]. 999 f(x'',x) = x'''. [para(212(a,1),878(a,2)),rewrite(993(7),878(6))]. 1023 f(f(x,y),x') = x. [para(41(a,1),878(a,2)),rewrite(352(17))]. 1046 x'' ^ x = x''''. [back_rewrite(253),rewrite(993(5))]. 1059 x''''' = x'. [para(993(a,1),27(a,1,1)),rewrite(1046(6)),flip(a)]. 1061 f(x,y) = (x ^ y)'''. [para(993(a,1),29(a,2)),rewrite(20(2),999(5)),flip(a)]. 1062 x v y = (x' ^ y')'''. [para(993(a,1),43(a,2,2)),rewrite(1046(6),1059(6),1061(3)),flip(a)]. 1073 ((x ^ y)''' ^ x')''' = x. [back_rewrite(1023),rewrite(1061(1),1061(6))]. 1096 (x ^ y)'''' = x ^ y. [back_rewrite(939),rewrite(1061(1),1061(7),1046(7),1059(6))]. 1102 (x ^ y)''' ^ (x ^ ((x ^ y)' ^ (x ^ y))''')''' = x'. [back_rewrite(880),rewrite(1061(1),1061(6),1062(10),1096(11),1061(12))]. 1103 x'''' = x. [back_rewrite(879),rewrite(1061(1),1061(6),1062(10),1096(11),1061(12),1061(16),1102(16))]. 1118 (x' ^ ((x' ^ (x ^ y)''')''' ^ x)''')''' = (x' ^ (x ^ y)''')'''. [back_rewrite(765),rewrite(1061(3),1061(7),1061(11),1061(15),1061(20),1061(24))]. 1133 (c4' ^ (c4 ^ c5)''')''' != c4 # answer(absorb). [back_rewrite(15),rewrite(1061(5),1061(9))]. 1137 x'' = x. [para(25(a,1),1073(a,1,1,1,1,1,1,1,1)),rewrite(1103(4),25(3),1103(4))]. 1141 ((x' ^ y)' ^ x)' = x'. [para(1103(a,1),1073(a,1,1,1,1,2)),rewrite(1137(2),1137(4),1137(6),1137(7))]. 1143 (c4' ^ (c4 ^ c5)')' != c4 # answer(absorb). [back_rewrite(1133),rewrite(1137(7),1137(9))]. 1155 (x' ^ (x ^ y)')' = x. [back_rewrite(1118),rewrite(1137(5),1137(7),1141(8),1137(3),25(3),1137(2),1137(2),1137(2),1137(4),1137(6)),flip(a)]. 1156 $F # answer(absorb). [resolve(1155,a,1143,a)]. ============================== end of proof ========================== restricted denial: (wt=10): 1143 (c4' ^ (c4 ^ c5)')' != c4 # answer(absorb). [back_rewrite(1133),rewrite(1137(7),1137(9))]. restricted denial: (wt=11): 1144 (c7 ^ c7')' != (c6 ^ c6')' # answer(one). [back_rewrite(1132),rewrite(1137(6),1137(11))]. restricted denial: (wt=34): 1145 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' | (c8' ^ (c8 ^ c9)')' != c8 | (c9 ^ c9')' != (c8 ^ c8')' # answer(combined). [back_rewrite(1131),rewrite(1137(7),1137(13),1137(20),1137(22),1137(29),1137(34))]. restricted denial: (wt=13): 1146 (c2 ^ (c1 ^ c3))' != (c1 ^ (c2 ^ c3))' # answer(assoc). [back_rewrite(1130),rewrite(1137(7),1137(13))]. % Redundant proof: 1180 $F # answer(absorb). [back_rewrite(1143),rewrite(1155(8)),xx(a)]. restricted denial: (wt=24): 1179 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' | (c9 ^ c9')' != (c8 ^ c8')' # answer(combined). [back_rewrite(1145),rewrite(1155(21)),xx(b)]. % Disable descendants (x means already disabled): 14x 15x 1133x 1143x given #76 (T,wt=5): 1137 x'' = x. [para(25(a,1),1073(a,1,1,1,1,1,1,1,1)),rewrite(1103(4),25(3),1103(4))]. given #77 (T,wt=5): 1178 x ^ x = x. [back_rewrite(25),rewrite(1137(3))]. given #78 (T,wt=8): 1177 f(x,y) = (x ^ y)'. [back_rewrite(1061),rewrite(1137(4))]. given #79 (T,wt=10): 1140 (x ^ y)' ^ x' = x'. [para(1073(a,1),866(a,2,1)),rewrite(1137(3),1137(6),1137(7),1137(10),1137(10),25(9),1137(6))]. given #80 (A,wt=22): 1147 (x ^ y)' ^ (x ^ ((x ^ (x' ^ x)')' ^ x)')' = x'. [back_rewrite(1129),rewrite(1137(2),1137(3),1137(6),1137(8),1137(10),1137(12))]. given #81 (T,wt=9): 1181 (x' ^ y)' ^ x = x. [para(1137(a,1),1140(a,1,2)),rewrite(1137(6))]. given #82 (T,wt=10): 1155 (x' ^ (x ^ y)')' = x. [back_rewrite(1118),rewrite(1137(5),1137(7),1141(8),1137(3),25(3),1137(2),1137(2),1137(2),1137(4),1137(6)),flip(a)]. given #83 (T,wt=10): 1176 x v y = (x' ^ y')'. [back_rewrite(1062),rewrite(1137(6))]. given #84 (T,wt=10): 1183 x' ^ (x ^ y)' = x'. [para(1155(a,1),1137(a,1,1)),flip(a)]. given #85 (A,wt=27): 1150 ((x ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1125),rewrite(1137(3),1137(5),1137(9),1137(11),1137(13),1137(15))]. given #86 (T,wt=9): 1186 x ^ (x' ^ y)' = x. [para(1137(a,1),1183(a,1,1)),rewrite(1137(6))]. given #87 (T,wt=9): 1187 (x ^ y) ^ x = x ^ y. [para(1140(a,1),1183(a,1,2,1)),rewrite(1137(3),1137(3),1137(5))]. given #88 (T,wt=13): 1175 (((x ^ y)' ^ y') ^ y')' = y. [back_rewrite(1075),rewrite(1137(3),1137(8))]. given #89 (T,wt=13): 1208 ((x ^ y)' ^ y') ^ y' = y'. [para(1175(a,1),1137(a,1,1)),flip(a)]. given #90 (A,wt=26): 1151 x ^ ((x ^ y)' ^ (((x ^ y)' ^ (x ^ x')')' ^ z)')' = x ^ y. [back_rewrite(1124),rewrite(1137(3),1137(5),1137(6),1137(8),1137(10),1137(12),1137(14))]. given #91 (T,wt=11): 1212 ((x ^ y')' ^ y) ^ y = y. [para(1137(a,1),1208(a,1,1,2)),rewrite(1137(6),1137(7))]. given #92 (T,wt=11): 1220 x ^ ((y ^ x')' ^ x) = x. [para(1212(a,1),1187(a,1,1)),rewrite(1212(10))]. given #93 (T,wt=13): 1213 x' ^ ((y ^ x)' ^ x') = x'. [para(1208(a,1),1187(a,1,1)),rewrite(1208(12))]. given #94 (T,wt=15): 1188 ((x ^ y)' ^ (y ^ z)') ^ y' = y'. [para(1150(a,1),978(a,1,2)),rewrite(1150(22))]. given #95 (A,wt=25): 1154 ((x ^ y)' ^ y') ^ (y ^ ((y ^ (x' ^ x)')' ^ y)')' = y'. [back_rewrite(1120),rewrite(1137(3),1137(8),1137(10),1137(12),1137(14))]. given #96 (T,wt=15): 1207 x' ^ ((y ^ x)' ^ (x ^ z)') = x'. [para(1150(a,1),1187(a,1,1)),rewrite(1150(22))]. given #97 (T,wt=15): 1225 ((x ^ y')' ^ (y' ^ z)') ^ y = y. [para(1137(a,1),1188(a,1,2)),rewrite(1137(10))]. given #98 (T,wt=15): 1229 ((x ^ y)' ^ (x ^ z)') ^ x' = x'. [para(1187(a,1),1188(a,1,1,1,1))]. given #99 (T,wt=15): 1236 x ^ ((y ^ x')' ^ (x' ^ z)') = x. [para(1137(a,1),1207(a,1,1)),rewrite(1137(10))]. given #100 (A,wt=25): 1159 (((x ^ y)' ^ (y ^ (y ^ y')')') ^ (y ^ (x' ^ x)')')' = y. [back_rewrite(1114),rewrite(1137(3),1137(4),1137(6),1137(8),1137(12),1137(14),1137(16))]. given #101 (T,wt=15): 1241 x' ^ ((x ^ y)' ^ (x ^ z)') = x'. [para(1187(a,1),1207(a,1,2,1,1))]. given #102 (T,wt=15): 1248 ((x' ^ y)' ^ (x' ^ z)') ^ x = x. [para(1187(a,1),1225(a,1,1,1,1))]. given #103 (T,wt=15): 1259 ((x ^ y)' ^ (x ^ x')')' = x ^ y. [back_rewrite(1158),rewrite(1249(8))]. given #104 (T,wt=15): 1261 x ^ ((x' ^ y)' ^ (x' ^ z)') = x. [para(1187(a,1),1236(a,1,2,1,1))]. given #105 (A,wt=22): 1163 (x ^ y)' ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1106),rewrite(1137(3),1137(6),1137(8),1137(10),1137(12))]. given #106 (T,wt=9): 1289 x ^ (y ^ x) = y ^ x. [para(1163(a,1),1140(a,1,1,1)),rewrite(1137(2),1137(3),1137(5))]. given #107 (T,wt=9): 1291 (x ^ y')' ^ y = y. [para(1181(a,1),1163(a,1,2,1,2,1)),rewrite(1178(6),1137(5),1137(6))]. given #108 (T,wt=9): 1292 (x ^ y) ^ y = x ^ y. [para(1163(a,1),1183(a,1,2,1)),rewrite(1137(3),1137(3),1137(5))]. given #109 (T,wt=9): 1303 x ^ (y ^ x')' = x. [para(1289(a,1),1186(a,1,2,1))]. given #110 (A,wt=23): 1168 (x ^ ((x ^ y)' ^ ((z ^ x) ^ (z ^ x)')')')' = (x ^ y)'. [back_rewrite(1097),rewrite(1137(3),1137(6),1137(8),1137(10),1137(12),1137(14))]. given #111 (T,wt=10): 1286 (x ^ y)' ^ y' = y'. [para(1163(a,1),978(a,1,2)),rewrite(1163(16))]. given #112 (T,wt=10): 1293 x' ^ (y ^ x)' = x'. [para(1163(a,1),1187(a,1,1)),rewrite(1163(16))]. given #113 (T,wt=13): 1300 (x ^ y) ^ (x ^ x') = x ^ x'. [back_rewrite(1281),rewrite(1289(7))]. given #114 (T,wt=13): 1338 (x ^ x') ^ (x ^ y) = x ^ x'. [para(1300(a,1),1187(a,1,1)),rewrite(1300(8))]. given #115 (A,wt=19): 1170 ((((x ^ y)' ^ (y ^ z)')' ^ u)' ^ y')' = y. [back_rewrite(1088),rewrite(1137(3),1137(5),1137(7),1137(9),1137(12))]. given #116 (T,wt=12): 1361 (((x ^ y) ^ z)' ^ x')' = x. [para(1140(a,1),1170(a,1,1,1,1,1,1)),rewrite(1137(3))]. given #117 (T,wt=12): 1373 (((x ^ y) ^ z)' ^ y')' = y. [para(1303(a,1),1170(a,1,1,1,1,1,1)),rewrite(1137(3))]. given #118 (T,wt=11): 1411 ((x ^ x')' ^ y')' = y. [para(1300(a,1),1373(a,1,1,1,1))]. given #119 (T,wt=11): 1412 (x ^ x')' ^ y' = y'. [para(1411(a,1),1137(a,1,1)),flip(a)]. given #120 (A,wt=29): 1189 ((x ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x' ^ x)')' ^ (y ^ z))')' = y'. [para(978(a,1),1150(a,1,1,2,1))]. given #121 (T,wt=9): 1430 (x ^ x')' ^ y = y. [para(1137(a,1),1412(a,1,2)),rewrite(1137(6))]. given #122 (T,wt=9): 1435 (x' ^ x)' ^ y = y. [para(1137(a,1),1430(a,1,1,1,2))]. NOTE: New constant: x' ^ x = c_0. [new_symbol(1450)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c_0, ', ^, v, f ]). ============================== PROOF ================================= % Proof 2 at 0.30 (+ 0.01) seconds: one. % Length of proof is 110. % Level of proof is 31. % Maximum clause weight is 39. % Given clauses 122. 3 f(x,f(x,x)) = f(y,f(y,y)) # answer(one) # 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))]. 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))]. 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)]. 41 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))]. 43 f(x',y' ^ z') = x v (y v z). [para(27(a,1),21(a,1,2))]. 48 f(x ^ y,z' ^ u') = f(x,y) v (z v u). [para(27(a,1),28(a,1,2))]. 63 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))]. 102 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))]. 181 f(x''',f(x,f(f(x,f(x',x)),x))) = x. [para(11(a,1),32(a,1,1))]. 190 f(x,f(x',f(f(x',x' v x),y))) = x'. [para(32(a,1),30(a,1,1)),rewrite(21(6))]. 192 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(181(a,1),20(a,1,1)),flip(a)]. 203 x ^ f(x',f(f(x',x' v x),y)) = x''. [para(190(a,1),20(a,1,1)),flip(a)]. 209 f(x',f(x'',x)) = x''. [para(32(a,1),190(a,1,2,2))]. 210 x' ^ f(x'',x) = x'''. [para(209(a,1),20(a,1,1)),flip(a)]. 212 f(x'',x'' v x) = x'''. [para(21(a,1),209(a,1,2))]. 224 (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)]. 253 x'' ^ (x'' v x) = x''''. [para(21(a,1),210(a,1,2))]. 325 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))]. 352 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))]. 650 (f(x,y) ^ y') ^ f(y,f(f(y,f(x',x)),y)) = y'. [para(102(a,1),20(a,1,1)),flip(a)]. 765 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),63(a,1,2,2))]. 782 f(x,f(f(x,y),x' v x)) = f(x,y). [para(325(a,1),63(a,1,2))]. 794 x ^ f(f(x,y),x' v x) = x ^ y. [para(782(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. 861 f(x,x'') = x'. [para(41(a,1),190(a,1,2,2)),rewrite(11(3))]. 866 x ^ x'' = x''. [para(41(a,1),203(a,1,2,2)),rewrite(11(3))]. 867 f(x,y) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(41(a,1),36(a,1,1))]. 878 f(x,x ^ y) = f(x,y). [para(41(a,1),63(a,1,2,2)),rewrite(11(3),20(2))]. 879 f(f(x,y),f(x,(x ^ y) v f(x,y))) = x. [para(41(a,1),782(a,1,2,1)),rewrite(20(3),41(22))]. 880 f(x,y) ^ f(x,(x ^ y) v f(x,y)) = x'. [para(41(a,1),794(a,1,2,1)),rewrite(20(3),352(22))]. 939 f(f(x,y),(x ^ y)') = x ^ y. [para(20(a,1),861(a,1,2,1)),rewrite(20(6))]. 978 x ^ (x ^ y) = x ^ y. [para(878(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. 982 f(f(f(f(x,y),f(y,z)),u),y') = y. [para(22(a,1),878(a,2)),rewrite(36(14))]. 993 x'' v x = x. [para(181(a,1),878(a,2)),rewrite(192(12),21(5))]. 999 f(x'',x) = x'''. [para(212(a,1),878(a,2)),rewrite(993(7),878(6))]. 1017 f(f(x,y),y') v y = y. [para(102(a,1),878(a,2)),rewrite(650(12),28(5))]. 1023 f(f(x,y),x') = x. [para(41(a,1),878(a,2)),rewrite(352(17))]. 1046 x'' ^ x = x''''. [back_rewrite(253),rewrite(993(5))]. 1059 x''''' = x'. [para(993(a,1),27(a,1,1)),rewrite(1046(6)),flip(a)]. 1061 f(x,y) = (x ^ y)'''. [para(993(a,1),29(a,2)),rewrite(20(2),999(5)),flip(a)]. 1062 x v y = (x' ^ y')'''. [para(993(a,1),43(a,2,2)),rewrite(1046(6),1059(6),1061(3)),flip(a)]. 1063 ((x ^ y)'''' ^ z')''' = ((x ^ y) ^ z')'''. [para(993(a,1),48(a,2,2)),rewrite(1046(6),1059(6),1061(3),1061(7),1062(11)),flip(a)]. 1073 ((x ^ y)''' ^ x')''' = x. [back_rewrite(1023),rewrite(1061(1),1061(6))]. 1075 (((x ^ y)''' ^ y') ^ y')''' = y. [back_rewrite(1017),rewrite(1061(1),1061(6),1062(10),1063(15))]. 1088 ((((x ^ y)''' ^ (y ^ z)''')''' ^ u)''' ^ y')''' = y. [back_rewrite(982),rewrite(1061(1),1061(5),1061(9),1061(13),1061(18))]. 1096 (x ^ y)'''' = x ^ y. [back_rewrite(939),rewrite(1061(1),1061(7),1046(7),1059(6))]. 1102 (x ^ y)''' ^ (x ^ ((x ^ y)' ^ (x ^ y))''')''' = x'. [back_rewrite(880),rewrite(1061(1),1061(6),1062(10),1096(11),1061(12))]. 1103 x'''' = x. [back_rewrite(879),rewrite(1061(1),1061(6),1062(10),1096(11),1061(12),1061(16),1102(16))]. 1106 (x ^ y)''' ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(867),rewrite(1061(1),1061(6),1061(10),1061(14),1061(18))]. 1115 x ^ ((x ^ y)''' ^ (x'' ^ x')''')''' = x ^ y. [back_rewrite(794),rewrite(1061(1),1062(6),1061(12))]. 1118 (x' ^ ((x' ^ (x ^ y)''')''' ^ x)''')''' = (x' ^ (x ^ y)''')'''. [back_rewrite(765),rewrite(1061(3),1061(7),1061(11),1061(15),1061(20),1061(24))]. 1125 ((x ^ y)''' ^ (y ^ z)''') ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(224),rewrite(1061(1),1061(5),1061(11),1061(15),1061(19),1061(23))]. 1132 (c7 ^ c7')''' != (c6 ^ c6')''' # answer(one). [back_rewrite(17),rewrite(1061(4),1061(11))]. 1137 x'' = x. [para(25(a,1),1073(a,1,1,1,1,1,1,1,1)),rewrite(1103(4),25(3),1103(4))]. 1140 (x ^ y)' ^ x' = x'. [para(1073(a,1),866(a,2,1)),rewrite(1137(3),1137(6),1137(7),1137(10),1137(10),25(9),1137(6))]. 1141 ((x' ^ y)' ^ x)' = x'. [para(1103(a,1),1073(a,1,1,1,1,2)),rewrite(1137(2),1137(4),1137(6),1137(7))]. 1144 (c7 ^ c7')' != (c6 ^ c6')' # answer(one). [back_rewrite(1132),rewrite(1137(6),1137(11))]. 1150 ((x ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1125),rewrite(1137(3),1137(5),1137(9),1137(11),1137(13),1137(15))]. 1155 (x' ^ (x ^ y)')' = x. [back_rewrite(1118),rewrite(1137(5),1137(7),1141(8),1137(3),25(3),1137(2),1137(2),1137(2),1137(4),1137(6)),flip(a)]. 1158 x ^ ((x ^ y)' ^ (x ^ x')')' = x ^ y. [back_rewrite(1115),rewrite(1137(3),1137(4),1137(6),1137(8))]. 1163 (x ^ y)' ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1106),rewrite(1137(3),1137(6),1137(8),1137(10),1137(12))]. 1170 ((((x ^ y)' ^ (y ^ z)')' ^ u)' ^ y')' = y. [back_rewrite(1088),rewrite(1137(3),1137(5),1137(7),1137(9),1137(12))]. 1175 (((x ^ y)' ^ y') ^ y')' = y. [back_rewrite(1075),rewrite(1137(3),1137(8))]. 1183 x' ^ (x ^ y)' = x'. [para(1155(a,1),1137(a,1,1)),flip(a)]. 1186 x ^ (x' ^ y)' = x. [para(1137(a,1),1183(a,1,1)),rewrite(1137(6))]. 1187 (x ^ y) ^ x = x ^ y. [para(1140(a,1),1183(a,1,2,1)),rewrite(1137(3),1137(3),1137(5))]. 1188 ((x ^ y)' ^ (y ^ z)') ^ y' = y'. [para(1150(a,1),978(a,1,2)),rewrite(1150(22))]. 1208 ((x ^ y)' ^ y') ^ y' = y'. [para(1175(a,1),1137(a,1,1)),flip(a)]. 1212 ((x ^ y')' ^ y) ^ y = y. [para(1137(a,1),1208(a,1,1,2)),rewrite(1137(6),1137(7))]. 1220 x ^ ((y ^ x')' ^ x) = x. [para(1212(a,1),1187(a,1,1)),rewrite(1212(10))]. 1229 ((x ^ y)' ^ (x ^ z)') ^ x' = x'. [para(1187(a,1),1188(a,1,1,1,1))]. 1249 x ^ ((x ^ y)' ^ (x ^ z)')' = ((x ^ y)' ^ (x ^ z)')'. [para(1229(a,1),1140(a,1,1,1)),rewrite(1137(2))]. 1259 ((x ^ y)' ^ (x ^ x')')' = x ^ y. [back_rewrite(1158),rewrite(1249(8))]. 1281 (x ^ x') ^ ((x ^ y) ^ (x ^ x')) = x ^ x'. [para(1259(a,1),1220(a,1,2,1))]. 1289 x ^ (y ^ x) = y ^ x. [para(1163(a,1),1140(a,1,1,1)),rewrite(1137(2),1137(3),1137(5))]. 1300 (x ^ y) ^ (x ^ x') = x ^ x'. [back_rewrite(1281),rewrite(1289(7))]. 1303 x ^ (y ^ x')' = x. [para(1289(a,1),1186(a,1,2,1))]. 1333 (x' ^ y) ^ (x' ^ x) = x' ^ x. [para(1137(a,1),1300(a,1,2,2)),rewrite(1137(8))]. 1373 (((x ^ y) ^ z)' ^ y')' = y. [para(1303(a,1),1170(a,1,1,1,1,1,1)),rewrite(1137(3))]. 1411 ((x ^ x')' ^ y')' = y. [para(1300(a,1),1373(a,1,1,1,1))]. 1412 (x ^ x')' ^ y' = y'. [para(1411(a,1),1137(a,1,1)),flip(a)]. 1417 ((x ^ (y ^ y')')' ^ z) ^ ((x' ^ x) ^ z') = y ^ y'. [para(1411(a,1),1150(a,1,1,2)),rewrite(1412(16),1137(13),1412(15),1137(12),1137(15))]. 1430 (x ^ x')' ^ y = y. [para(1137(a,1),1412(a,1,2)),rewrite(1137(6))]. 1435 (x' ^ x)' ^ y = y. [para(1137(a,1),1430(a,1,1,1,2))]. 1437 x ^ (y ^ y')' = x. [para(1430(a,1),1187(a,1,1)),rewrite(1430(8))]. 1440 (x' ^ y) ^ ((x' ^ x) ^ y') = z ^ z'. [back_rewrite(1417),rewrite(1437(4))]. 1442 (x' ^ x) ^ y' = x' ^ x. [para(1435(a,1),1183(a,1,2,1)),rewrite(1137(4),1137(8))]. 1450 x' ^ x = y ^ y'. [back_rewrite(1440),rewrite(1442(6),1333(5))]. 1454 x' ^ x = c_0. [new_symbol(1450)]. 1461 x ^ x' = c_0. [back_rewrite(1450),rewrite(1454(2)),flip(a)]. 1465 $F # answer(one). [back_rewrite(1144),rewrite(1461(4),1461(6)),xx(a)]. ============================== end of proof ========================== restricted denial: (wt=13): 1464 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' # answer(combined). [back_rewrite(1179),rewrite(1461(17),1461(19)),xx(b)]. % Disable descendants (x means already disabled): 16x 17x 1132x 1144x given #123 (T,wt=5): 1459 c_0 ^ x = c_0. [back_rewrite(1452),rewrite(1454(2),1454(4))]. given #124 (T,wt=5): 1460 x ^ c_0 = c_0. [back_rewrite(1451),rewrite(1454(2),1454(4))]. given #125 (A,wt=23): 1194 x ^ ((y ^ x)' ^ (x ^ z)')' = ((y ^ x)' ^ (x ^ z)')'. [para(1150(a,1),1140(a,1,1,1)),rewrite(1137(2))]. given #126 (T,wt=6): 1454 x' ^ x = c_0. [new_symbol(1450)]. given #127 (T,wt=6): 1461 x ^ x' = c_0. [back_rewrite(1450),rewrite(1454(2)),flip(a)]. given #128 (T,wt=6): 1462 x ^ c_0' = x. [back_rewrite(1446),rewrite(1454(2))]. given #129 (T,wt=6): 1463 c_0' ^ x = x. [back_rewrite(1435),rewrite(1454(2))]. given #130 (A,wt=23): 1199 ((x ^ y)' ^ (y ^ z)')' ^ y = ((x ^ y)' ^ (y ^ z)')'. [para(1150(a,1),1183(a,1,2,1)),rewrite(1137(8))]. given #131 (T,wt=12): 1377 ((x ^ y) ^ z)' ^ x' = x'. [para(1361(a,1),1137(a,1,1)),flip(a)]. given #132 (T,wt=11): 1496 ((x' ^ y) ^ z)' ^ x = x. [para(1137(a,1),1377(a,1,2)),rewrite(1137(7))]. given #133 (T,wt=11): 1511 x ^ ((x' ^ y) ^ z)' = x. [para(1496(a,1),1187(a,1,1)),rewrite(1496(10))]. given #134 (T,wt=11): 1512 ((x ^ y') ^ z)' ^ y = y. [para(1289(a,1),1496(a,1,1,1,1))]. given #135 (A,wt=17): 1226 ((x ^ (y ^ z)')' ^ y) ^ (y ^ z) = y ^ z. [para(1140(a,1),1188(a,1,1,2,1)),rewrite(1137(6),1137(8),1137(10))]. given #136 (T,wt=11): 1513 (x ^ (y' ^ z))' ^ y = y. [para(1289(a,1),1496(a,1,1,1))]. given #137 (T,wt=11): 1519 x ^ ((y ^ x') ^ z)' = x. [para(1289(a,1),1511(a,1,2,1,1))]. given #138 (T,wt=11): 1520 x ^ (y ^ (x' ^ z))' = x. [para(1289(a,1),1511(a,1,2,1))]. given #139 (T,wt=11): 1529 (x ^ (y ^ z'))' ^ z = z. [para(1289(a,1),1512(a,1,1,1))]. given #140 (A,wt=17): 1227 (x ^ ((x ^ y)' ^ z)') ^ (x ^ y) = x ^ y. [para(1183(a,1),1188(a,1,1,1,1)),rewrite(1137(2),1137(8),1137(10))]. given #141 (T,wt=11): 1544 (x ^ y) ^ (y ^ x) = y ^ x. [para(1293(a,1),1226(a,1,1,1,1)),rewrite(1137(2))]. % Operation ^ is commutative; C redundancy checks enabled. % back CAC tautology: 1629 (x ^ y)' = (y ^ x)'. [para(1544(a,1),1183(a,1,2,1)),rewrite(1628(5))]. given #142 (T,wt=7): 1630 x ^ y = y ^ x. [para(1544(a,1),1187(a,1,1)),rewrite(1544(3),1544(4))]. given #143 (T,wt=11): 1574 x ^ (y ^ (z ^ x'))' = x. [para(1289(a,1),1519(a,1,2,1))]. given #144 (T,wt=12): 1499 x' ^ ((x ^ y) ^ z)' = x'. [para(1377(a,1),1187(a,1,1)),rewrite(1377(10))]. given #145 (A,wt=17): 1238 (x ^ y) ^ (x ^ ((x ^ y)' ^ z)') = x ^ y. [para(1183(a,1),1207(a,1,2,1,1)),rewrite(1137(3),1137(3),1137(10))]. given #146 (T,wt=12): 1573 x' ^ ((y ^ x) ^ z)' = x'. [para(1137(a,1),1519(a,1,2,1,1,2))]. given #147 (T,wt=12): 1578 x' ^ (y ^ (x ^ z))' = x'. [para(1137(a,1),1520(a,1,2,1,2,1))]. given #148 (T,wt=12): 1672 x' ^ (y ^ (z ^ x))' = x'. [back_rewrite(1591),rewrite(1630(5))]. given #149 (T,wt=13): 1379 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(1361(a,1),1140(a,1,1)),rewrite(1137(4),1137(7))]. given #150 (A,wt=36): 1247 ((x ^ y)' ^ (y ^ z)')' ^ (y ^ (((x ^ y)' ^ (y ^ z)') ^ u)') = ((x ^ y)' ^ (y ^ z)')'. [para(1207(a,1),1207(a,1,2,1,1)),rewrite(1137(8))]. given #151 (T,wt=13): 1401 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z. [para(1373(a,1),1140(a,1,1)),rewrite(1137(4),1137(7))]. given #152 (T,wt=13): 1497 (x' ^ y)' ^ (x ^ z) = x ^ z. [para(1140(a,1),1377(a,1,1,1,1)),rewrite(1137(6),1137(8))]. given #153 (T,wt=13): 1506 (x' ^ y)' ^ (z ^ x) = z ^ x. [para(1286(a,1),1377(a,1,1,1,1)),rewrite(1137(6),1137(8))]. given #154 (T,wt=13): 1517 (x ^ y) ^ (x' ^ z)' = x ^ y. [para(1140(a,1),1511(a,1,2,1,1))]. given #155 (A,wt=23): 1249 x ^ ((x ^ y)' ^ (x ^ z)')' = ((x ^ y)' ^ (x ^ z)')'. [para(1229(a,1),1140(a,1,1,1)),rewrite(1137(2))]. given #156 (T,wt=13): 1522 (x ^ y) ^ (y' ^ z)' = x ^ y. [para(1286(a,1),1511(a,1,2,1,1))]. given #157 (T,wt=13): 1552 (x ^ y')' ^ (y ^ z) = y ^ z. [para(1140(a,1),1513(a,1,1,1,2))]. given #158 (T,wt=13): 1562 (x ^ y')' ^ (z ^ y) = z ^ y. [para(1286(a,1),1513(a,1,1,1,2))]. given #159 (T,wt=13): 1579 (x ^ y) ^ (z ^ x')' = x ^ y. [para(1140(a,1),1520(a,1,2,1,2))]. given #160 (A,wt=36): 1271 ((x ^ y)' ^ (x ^ z)')' ^ (x ^ (((x ^ y)' ^ (x ^ z)') ^ u)') = ((x ^ y)' ^ (x ^ z)')'. [para(1241(a,1),1207(a,1,2,1,1)),rewrite(1137(8))]. given #161 (T,wt=13): 1582 (x ^ y) ^ (z ^ y')' = x ^ y. [para(1286(a,1),1520(a,1,2,1,2))]. given #162 (T,wt=13): 1703 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(1578(a,1),1303(a,1,2,1)),rewrite(1137(4),1630(3))]. given #163 (T,wt=13): 1714 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(1672(a,1),1303(a,1,2,1)),rewrite(1137(4),1630(3))]. given #164 (T,wt=13): 1723 x ^ (((x' ^ y) ^ z) ^ u)' = x. [para(1379(a,1),1511(a,1,2,1,1))]. given #165 (A,wt=17): 1298 (x ^ y) ^ (y ^ ((x ^ y)' ^ z)') = x ^ y. [para(1163(a,1),1241(a,1,2,1,1)),rewrite(1137(3),1137(3),1137(10))]. given #166 (T,wt=13): 1724 x ^ (((y ^ x') ^ z) ^ u)' = x. [para(1379(a,1),1519(a,1,2,1))]. given #167 (T,wt=13): 1725 x ^ (y ^ ((x' ^ z) ^ u))' = x. [para(1379(a,1),1520(a,1,2,1,2))]. given #168 (T,wt=13): 1753 x ^ ((y ^ (x' ^ z)) ^ u)' = x. [para(1401(a,1),1511(a,1,2,1))]. given #169 (T,wt=13): 1755 x ^ ((y ^ (z ^ x')) ^ u)' = x. [para(1401(a,1),1519(a,1,2,1))]. given #170 (A,wt=15): 1305 x' ^ ((y ^ x)' ^ (z ^ x)') = x'. [para(1289(a,1),1207(a,1,2,2,1))]. given #171 (T,wt=13): 1757 x ^ (y ^ ((z ^ x') ^ u))' = x. [para(1401(a,1),1520(a,1,2,1,2))]. given #172 (T,wt=13): 1854 x ^ (y ^ (z ^ (x' ^ u)))' = x. [para(1520(a,1),1562(a,1,2)),rewrite(1137(5),1630(6),1520(11))]. given #173 (T,wt=13): 1856 x ^ (y ^ (z ^ (u ^ x')))' = x. [para(1574(a,1),1562(a,1,2)),rewrite(1137(5),1630(6),1574(11))]. given #174 (T,wt=14): 1498 (x ^ y)' ^ (x' ^ z) = x' ^ z. [para(1181(a,1),1377(a,1,1,1,1)),rewrite(1137(6),1137(9))]. given #175 (A,wt=15): 1308 x ^ ((y ^ x')' ^ (z ^ x')') = x. [para(1289(a,1),1236(a,1,2,2,1))]. given #176 (T,wt=14): 1505 (x ^ y)' ^ (z ^ x') = z ^ x'. [para(1291(a,1),1377(a,1,1,1,1)),rewrite(1137(6),1137(9))]. given #177 (T,wt=14): 1518 (x' ^ y) ^ (x ^ z)' = x' ^ y. [para(1181(a,1),1511(a,1,2,1,1))]. given #178 (T,wt=14): 1521 (x ^ y') ^ (y ^ z)' = x ^ y'. [para(1291(a,1),1511(a,1,2,1,1))]. given #179 (T,wt=14): 1553 (x ^ y)' ^ (y' ^ z) = y' ^ z. [para(1181(a,1),1513(a,1,1,1,2))]. given #180 (A,wt=15): 1309 x' ^ ((x ^ y)' ^ (z ^ x)') = x'. [para(1289(a,1),1241(a,1,2,2,1))]. given #181 (T,wt=14): 1561 (x ^ y)' ^ (z ^ y') = z ^ y'. [para(1291(a,1),1513(a,1,1,1,2))]. given #182 (T,wt=14): 1580 (x' ^ y) ^ (z ^ x)' = x' ^ y. [para(1181(a,1),1520(a,1,2,1,2))]. given #183 (T,wt=14): 1581 (x ^ y') ^ (z ^ y)' = x ^ y'. [para(1291(a,1),1520(a,1,2,1,2))]. given #184 (T,wt=14): 1628 (x ^ y)' ^ (y ^ x)' = (y ^ x)'. [para(1544(a,1),1140(a,1,1,1))]. given #185 (A,wt=15): 1311 x ^ ((x' ^ y)' ^ (z ^ x')') = x. [para(1289(a,1),1261(a,1,2,2,1))]. given #186 (T,wt=14): 1727 x' ^ (((x ^ y) ^ z) ^ u)' = x'. [para(1379(a,1),1499(a,1,2,1,1))]. given #187 (T,wt=14): 1729 x' ^ (((y ^ x) ^ z) ^ u)' = x'. [para(1379(a,1),1573(a,1,2,1))]. given #188 (T,wt=14): 1730 x' ^ (y ^ ((x ^ z) ^ u))' = x'. [para(1379(a,1),1578(a,1,2,1,2))]. given #189 (T,wt=14): 1760 x' ^ ((y ^ (x ^ z)) ^ u)' = x'. [para(1401(a,1),1499(a,1,2,1))]. given #190 (A,wt=27): 1359 x ^ (((y ^ x)' ^ (x ^ z)')' ^ u) = ((y ^ x)' ^ (x ^ z)')' ^ u. [para(1170(a,1),1140(a,1,1)),rewrite(1137(9),1137(17))]. given #191 (T,wt=14): 1764 x' ^ ((y ^ (z ^ x)) ^ u)' = x'. [para(1401(a,1),1573(a,1,2,1))]. given #192 (T,wt=14): 1766 x' ^ (y ^ ((z ^ x) ^ u))' = x'. [para(1401(a,1),1578(a,1,2,1,2))]. given #193 (T,wt=14): 1863 x' ^ (y ^ (z ^ (x ^ u)))' = x'. [para(1578(a,1),1562(a,1,2)),rewrite(1137(4),1630(6),1578(11))]. given #194 (T,wt=14): 1865 x' ^ (y ^ (z ^ (u ^ x)))' = x'. [para(1672(a,1),1562(a,1,2)),rewrite(1137(4),1630(6),1672(11))]. given #195 (A,wt=23): 1390 ((x ^ y) ^ z) ^ (x ^ (((x ^ y) ^ z)' ^ u)') = (x ^ y) ^ z. [para(1361(a,1),1241(a,1,2,1)),rewrite(1137(4),1137(13))]. given #196 (T,wt=15): 1726 (x ^ y) ^ ((y ^ x) ^ z) = (y ^ x) ^ z. [para(1544(a,1),1379(a,1,2,1)),rewrite(1544(7))]. given #197 (T,wt=15): 1732 (x ^ y) ^ ((y ^ x)' ^ z)' = y ^ x. [back_rewrite(1637),rewrite(1726(8))]. given #198 (T,wt=15): 1754 ((x' ^ y) ^ z)' ^ (x ^ u) = x ^ u. [para(1511(a,1),1401(a,1,2,1)),rewrite(1511(11))]. given #199 (T,wt=15): 1756 ((x ^ y') ^ z)' ^ (y ^ u) = y ^ u. [para(1519(a,1),1401(a,1,2,1)),rewrite(1519(11))]. given #200 (A,wt=23): 1407 ((x ^ y) ^ z) ^ (y ^ (((x ^ y) ^ z)' ^ u)') = (x ^ y) ^ z. [para(1373(a,1),1241(a,1,2,1)),rewrite(1137(4),1137(13))]. given #201 (T,wt=15): 1758 (x ^ (y' ^ z))' ^ (y ^ u) = y ^ u. [para(1520(a,1),1401(a,1,2,1)),rewrite(1520(11))]. given #202 (T,wt=15): 1759 (x ^ (y ^ z'))' ^ (z ^ u) = z ^ u. [para(1574(a,1),1401(a,1,2,1)),rewrite(1574(11))]. given #203 (T,wt=15): 1793 ((x' ^ y) ^ z)' ^ (u ^ x) = u ^ x. [para(1379(a,1),1506(a,1,1,1))]. given #204 (T,wt=15): 1795 ((x ^ y') ^ z)' ^ (u ^ y) = u ^ y. [para(1401(a,1),1506(a,1,1,1))]. given #205 (A,wt=26): 1467 (x ^ y)' ^ (x ^ ((x ^ y)' ^ z)')' = (x ^ ((x ^ y)' ^ z)')'. [para(1183(a,1),1194(a,1,2,1,1,1)),rewrite(1137(4),1183(13),1137(11))]. given #206 (T,wt=15): 1798 (x ^ y) ^ ((x' ^ z) ^ u)' = x ^ y. [para(1379(a,1),1517(a,1,2,1))]. given #207 (T,wt=15): 1799 (x ^ y) ^ ((z ^ x') ^ u)' = x ^ y. [para(1401(a,1),1517(a,1,2,1))]. given #208 (T,wt=15): 1800 (x ^ y) ^ ((y' ^ z) ^ u)' = x ^ y. [para(1506(a,1),1517(a,1,1)),rewrite(1137(5),1506(11))]. given #209 (T,wt=8): 3026 x ^ (x' ^ y) = c_0. [para(1800(a,1),1461(a,1)),rewrite(1630(3))]. given #210 (A,wt=20): 1469 x' ^ ((y ^ x)' ^ ((z ^ x)' ^ (x ^ u)')) = x'. [para(1194(a,1),1207(a,1,2,2,1)),rewrite(1137(10))]. given #211 (T,wt=8): 3033 x' ^ (x ^ y) = c_0. [para(1137(a,1),3026(a,1,2,1))]. given #212 (T,wt=8): 3034 x ^ (y ^ x') = c_0. [para(1289(a,1),3026(a,1,2))]. given #213 (T,wt=8): 3044 x' ^ (y ^ x) = c_0. [para(3026(a,1),1714(a,1)),flip(a)]. given #214 (T,wt=10): 3036 x ^ ((x' ^ y) ^ z) = c_0. [para(1379(a,1),3026(a,1,2))]. given #215 (A,wt=21): 1473 x ^ ((y ^ x')' ^ ((z ^ x')' ^ (x' ^ u)')) = x. [para(1194(a,1),1236(a,1,2,2,1)),rewrite(1137(12))]. given #216 (T,wt=10): 3037 x ^ ((y ^ x') ^ z) = c_0. [para(1401(a,1),3026(a,1,2))]. given #217 (T,wt=10): 3038 (x' ^ y) ^ (x ^ z) = c_0. [para(1497(a,1),3026(a,1,2))]. given #218 (T,wt=10): 3039 (x' ^ y) ^ (z ^ x) = c_0. [para(1506(a,1),3026(a,1,2))]. given #219 (T,wt=10): 3041 (x ^ y') ^ (y ^ z) = c_0. [para(1552(a,1),3026(a,1,2))]. given #220 (A,wt=20): 1474 x' ^ (((y ^ x)' ^ (x ^ z)') ^ (x ^ u)') = x'. [para(1194(a,1),1241(a,1,2,1,1)),rewrite(1137(8))]. given #221 (T,wt=10): 3042 (x ^ y') ^ (z ^ y) = c_0. [para(1562(a,1),3026(a,1,2))]. given #222 (T,wt=10): 3043 x ^ (y ^ (x' ^ z)) = c_0. [para(1703(a,1),3026(a,1,2))]. given #223 (T,wt=10): 3045 x ^ (y ^ (z ^ x')) = c_0. [para(1714(a,1),3026(a,1,2))]. given #224 (T,wt=10): 3046 (x ^ y) ^ (x' ^ z) = c_0. [para(1498(a,1),3026(a,1,2))]. given #225 (A,wt=20): 1475 x' ^ ((x ^ y)' ^ ((z ^ x)' ^ (x ^ u)')) = x'. [para(1194(a,1),1241(a,1,2,2,1)),rewrite(1137(10))]. given #226 (T,wt=10): 3047 (x ^ y) ^ (z ^ x') = c_0. [para(1505(a,1),3026(a,1,2))]. given #227 (T,wt=10): 3048 (x ^ y) ^ (y' ^ z) = c_0. [para(1553(a,1),3026(a,1,2))]. given #228 (T,wt=10): 3049 (x ^ y) ^ (z ^ y') = c_0. [para(1561(a,1),3026(a,1,2))]. given #229 (T,wt=10): 3050 (x ^ y) ^ (y ^ x)' = c_0. [para(1628(a,1),3026(a,1,2))]. given #230 (A,wt=21): 1478 x ^ (((y ^ x')' ^ (x' ^ z)') ^ (x' ^ u)') = x. [para(1194(a,1),1261(a,1,2,1,1)),rewrite(1137(9))]. given #231 (T,wt=10): 3136 (x ^ y)' ^ (y ^ x) = c_0. [para(1544(a,1),3033(a,1,2))]. given #232 (T,wt=10): 3137 x' ^ ((x ^ y) ^ z) = c_0. [para(1379(a,1),3033(a,1,2))]. given #233 (T,wt=10): 3138 x' ^ ((y ^ x) ^ z) = c_0. [para(1401(a,1),3033(a,1,2))]. given #234 (T,wt=10): 3140 x' ^ (y ^ (x ^ z)) = c_0. [para(1703(a,1),3033(a,1,2))]. given #235 (A,wt=21): 1479 x ^ ((x' ^ y)' ^ ((z ^ x')' ^ (x' ^ u)')) = x. [para(1194(a,1),1261(a,1,2,2,1)),rewrite(1137(12))]. given #236 (T,wt=10): 3141 x' ^ (y ^ (z ^ x)) = c_0. [para(1714(a,1),3033(a,1,2))]. given #237 (T,wt=12): 3052 ((x' ^ y) ^ z) ^ (x ^ u) = c_0. [para(1754(a,1),3026(a,1,2))]. given #238 (T,wt=12): 3053 ((x ^ y') ^ z) ^ (y ^ u) = c_0. [para(1756(a,1),3026(a,1,2))]. given #239 (T,wt=12): 3054 (x ^ (y' ^ z)) ^ (y ^ u) = c_0. [para(1758(a,1),3026(a,1,2))]. given #240 (A,wt=23): 1480 x ^ ((y ^ x)' ^ (z ^ x)')' = ((y ^ x)' ^ (z ^ x)')'. [para(1289(a,1),1194(a,1,2,1,2,1)),rewrite(1289(11))]. given #241 (T,wt=12): 3055 (x ^ (y ^ z')) ^ (z ^ u) = c_0. [para(1759(a,1),3026(a,1,2))]. given #242 (T,wt=12): 3056 ((x' ^ y) ^ z) ^ (u ^ x) = c_0. [para(1793(a,1),3026(a,1,2))]. given #243 (T,wt=12): 3057 ((x ^ y') ^ z) ^ (u ^ y) = c_0. [para(1795(a,1),3026(a,1,2))]. given #244 (T,wt=12): 3143 (x ^ y)' ^ ((y ^ x) ^ z) = c_0. [para(1726(a,1),3033(a,1,2))]. given #245 (A,wt=26): 1484 (x ^ y)' ^ (y ^ ((x ^ y)' ^ z)')' = (y ^ ((x ^ y)' ^ z)')'. [para(1293(a,1),1194(a,1,2,1,1,1)),rewrite(1137(4),1293(13),1137(11))]. given #246 (T,wt=12): 3144 x ^ (((x' ^ y) ^ z) ^ u) = c_0. [para(1723(a,1),3034(a,1,2)),rewrite(1630(5))]. given #247 (T,wt=12): 3145 x ^ (((y ^ x') ^ z) ^ u) = c_0. [para(1724(a,1),3034(a,1,2)),rewrite(1630(5))]. given #248 (T,wt=12): 3146 x ^ (y ^ ((x' ^ z) ^ u)) = c_0. [para(1725(a,1),3034(a,1,2)),rewrite(1630(5))]. given #249 (T,wt=12): 3147 x ^ ((y ^ (x' ^ z)) ^ u) = c_0. [para(1753(a,1),3034(a,1,2)),rewrite(1630(5))]. given #250 (A,wt=33): 1485 x ^ ((y ^ x)' ^ ((z ^ x)' ^ (x ^ u)'))' = ((y ^ x)' ^ ((z ^ x)' ^ (x ^ u)'))'. [para(1194(a,1),1194(a,1,2,1,2,1)),rewrite(1137(9),1194(19),1137(19))]. given #251 (T,wt=12): 3148 x ^ ((y ^ (z ^ x')) ^ u) = c_0. [para(1755(a,1),3034(a,1,2)),rewrite(1630(5))]. given #252 (T,wt=12): 3149 x ^ (y ^ ((z ^ x') ^ u)) = c_0. [para(1757(a,1),3034(a,1,2)),rewrite(1630(5))]. given #253 (T,wt=12): 3150 x ^ (y ^ (z ^ (x' ^ u))) = c_0. [para(1854(a,1),3034(a,1,2)),rewrite(1630(5))]. given #254 (T,wt=12): 3151 x ^ (y ^ (z ^ (u ^ x'))) = c_0. [para(1856(a,1),3034(a,1,2)),rewrite(1630(5))]. given #255 (A,wt=33): 1493 x ^ (((y ^ x)' ^ (x ^ z)') ^ (x ^ u)')' = (((y ^ x)' ^ (x ^ z)') ^ (x ^ u)')'. [para(1199(a,1),1194(a,1,2,1,1,1)),rewrite(1137(7),1199(17),1137(17))]. given #256 (T,wt=12): 3152 x' ^ (((x ^ y) ^ z) ^ u) = c_0. [para(1727(a,1),3034(a,1,2)),rewrite(1630(5))]. given #257 (T,wt=12): 3153 x' ^ (((y ^ x) ^ z) ^ u) = c_0. [para(1729(a,1),3034(a,1,2)),rewrite(1630(5))]. given #258 (T,wt=12): 3154 x' ^ (y ^ ((x ^ z) ^ u)) = c_0. [para(1730(a,1),3034(a,1,2)),rewrite(1630(5))]. given #259 (T,wt=12): 3155 x' ^ ((y ^ (x ^ z)) ^ u) = c_0. [para(1760(a,1),3034(a,1,2)),rewrite(1630(5))]. given #260 (A,wt=27): 1500 (x' ^ y)' ^ ((z ^ x)' ^ (x ^ u)')' = ((z ^ x)' ^ (x ^ u)')'. [para(1188(a,1),1377(a,1,1,1,1))]. given #261 (T,wt=12): 3156 x' ^ ((y ^ (z ^ x)) ^ u) = c_0. [para(1764(a,1),3034(a,1,2)),rewrite(1630(5))]. given #262 (T,wt=12): 3157 x' ^ (y ^ ((z ^ x) ^ u)) = c_0. [para(1766(a,1),3034(a,1,2)),rewrite(1630(5))]. given #263 (T,wt=12): 3158 x' ^ (y ^ (z ^ (x ^ u))) = c_0. [para(1863(a,1),3034(a,1,2)),rewrite(1630(5))]. given #264 (T,wt=12): 3159 x' ^ (y ^ (z ^ (u ^ x))) = c_0. [para(1865(a,1),3034(a,1,2)),rewrite(1630(5))]. given #265 (A,wt=30): 1501 (x ^ y)' ^ ((z ^ x')' ^ (x' ^ u)')' = ((z ^ x')' ^ (x' ^ u)')'. [para(1225(a,1),1377(a,1,1,1,1))]. given #266 (T,wt=12): 3171 (x' ^ y) ^ ((x ^ z) ^ u) = c_0. [para(1497(a,1),3036(a,1,2,1))]. given #267 (T,wt=12): 3172 (x' ^ y) ^ ((z ^ x) ^ u) = c_0. [para(1506(a,1),3036(a,1,2,1))]. given #268 (T,wt=12): 3175 (x ^ y') ^ ((y ^ z) ^ u) = c_0. [para(1552(a,1),3036(a,1,2,1))]. given #269 (T,wt=12): 3176 (x ^ y') ^ ((z ^ y) ^ u) = c_0. [para(1562(a,1),3036(a,1,2,1))]. given #270 (A,wt=27): 1502 (x' ^ y)' ^ ((x ^ z)' ^ (x ^ u)')' = ((x ^ z)' ^ (x ^ u)')'. [para(1229(a,1),1377(a,1,1,1,1))]. given #271 (T,wt=12): 3177 (x ^ y) ^ ((x' ^ z) ^ u) = c_0. [para(1498(a,1),3036(a,1,2,1))]. given #272 (T,wt=12): 3178 (x ^ y) ^ ((z ^ x') ^ u) = c_0. [para(1505(a,1),3036(a,1,2,1))]. given #273 (T,wt=12): 3179 (x ^ y) ^ ((y' ^ z) ^ u) = c_0. [para(1553(a,1),3036(a,1,2,1))]. given #274 (T,wt=12): 3180 (x ^ y) ^ ((z ^ y') ^ u) = c_0. [para(1561(a,1),3036(a,1,2,1))]. given #275 (A,wt=30): 1503 (x ^ y)' ^ ((x' ^ z)' ^ (x' ^ u)')' = ((x' ^ z)' ^ (x' ^ u)')'. [para(1248(a,1),1377(a,1,1,1,1))]. given #276 (T,wt=12): 3181 (x ^ y) ^ ((y ^ x)' ^ z) = c_0. [para(1628(a,1),3036(a,1,2,1))]. given #277 (T,wt=12): 3210 ((x ^ y) ^ z) ^ (x' ^ u) = c_0. [para(1499(a,1),3037(a,1,2,1))]. given #278 (T,wt=12): 3211 ((x ^ y) ^ z) ^ (y' ^ u) = c_0. [para(1573(a,1),3037(a,1,2,1))]. given #279 (T,wt=12): 3212 (x ^ (y ^ z)) ^ (y' ^ u) = c_0. [para(1578(a,1),3037(a,1,2,1))]. given #280 (A,wt=17): 1510 (x' ^ y)' ^ ((x ^ z) ^ u) = (x ^ z) ^ u. [para(1377(a,1),1377(a,1,1,1,1)),rewrite(1137(7),1137(10))]. given #281 (T,wt=12): 3213 (x ^ (y ^ z)) ^ (z' ^ u) = c_0. [para(1672(a,1),3037(a,1,2,1))]. given #282 (T,wt=12): 3236 (x' ^ y) ^ (z ^ (x ^ u)) = c_0. [para(1703(a,1),3038(a,1,2))]. given #283 (T,wt=12): 3237 (x' ^ y) ^ (z ^ (u ^ x)) = c_0. [para(1714(a,1),3038(a,1,2))]. given #284 (T,wt=12): 3238 ((x ^ y) ^ z) ^ (u ^ x') = c_0. [para(1505(a,1),3038(a,1,2)),rewrite(1137(3))]. given #285 (A,wt=18): 1516 (x ^ y)' ^ ((x' ^ z) ^ u) = (x' ^ z) ^ u. [para(1496(a,1),1377(a,1,1,1,1)),rewrite(1137(7),1137(11))]. given #286 (T,wt=12): 3239 ((x ^ y) ^ z) ^ (u ^ y') = c_0. [para(1561(a,1),3038(a,1,2)),rewrite(1137(3))]. given #287 (T,wt=12): 3256 (x ^ y) ^ (z ^ (x' ^ u)) = c_0. [para(1497(a,1),3039(a,1,1))]. given #288 (T,wt=12): 3257 (x ^ y) ^ (z ^ (y' ^ u)) = c_0. [para(1506(a,1),3039(a,1,1))]. given #289 (T,wt=12): 3259 (x ^ y) ^ (z ^ (u ^ x')) = c_0. [para(1552(a,1),3039(a,1,1))]. given #290 (A,wt=19): 1524 x ^ (((y ^ x')' ^ (x' ^ z)')' ^ u)' = x. [para(1194(a,1),1511(a,1,2,1,1))]. given #291 (T,wt=12): 3260 (x ^ y) ^ (z ^ (u ^ y')) = c_0. [para(1562(a,1),3039(a,1,1))]. given #292 (T,wt=12): 3262 (x ^ (y' ^ z)) ^ (u ^ y) = c_0. [para(1703(a,1),3039(a,1,1))]. given #293 (T,wt=12): 3263 (x ^ (y ^ z')) ^ (u ^ z) = c_0. [para(1714(a,1),3039(a,1,1))]. given #294 (T,wt=12): 3275 (x ^ y') ^ (z ^ (y ^ u)) = c_0. [para(1505(a,1),3039(a,1,1))]. given #295 (A,wt=19): 1525 x ^ ((y ^ (x' ^ z))' ^ ((x' ^ z) ^ u)') = x. [para(1194(a,1),1511(a,1,2,1)),rewrite(1137(11))]. given #296 (T,wt=12): 3277 (x ^ y') ^ (z ^ (u ^ y)) = c_0. [para(1561(a,1),3039(a,1,1))]. given #297 (T,wt=12): 3278 (x ^ y)' ^ (z ^ (y ^ x)) = c_0. [para(1628(a,1),3039(a,1,1))]. given #298 (T,wt=12): 3301 (x ^ (y ^ z)') ^ (z ^ y) = c_0. [para(1544(a,1),3041(a,1,2))]. given #299 (T,wt=12): 3303 (x ^ (y ^ z)) ^ (u ^ y') = c_0. [para(1505(a,1),3041(a,1,2)),rewrite(1137(3))]. given #300 (A,wt=17): 1527 ((x ^ y) ^ z) ^ (x' ^ u)' = (x ^ y) ^ z. [para(1377(a,1),1511(a,1,2,1,1))]. given #301 (T,wt=12): 3304 (x ^ (y ^ z)) ^ (u ^ z') = c_0. [para(1561(a,1),3041(a,1,2)),rewrite(1137(3))]. given #302 (T,wt=12): 3305 (x ^ (y ^ z)) ^ (z ^ y)' = c_0. [para(1628(a,1),3041(a,1,2)),rewrite(1137(3))]. given #303 (T,wt=12): 3423 (x ^ y) ^ (z ^ (y ^ x)') = c_0. [para(1628(a,1),3043(a,1,2,2))]. given #304 (T,wt=14): 3184 ((x' ^ y) ^ z) ^ ((x ^ u) ^ v) = c_0. [para(1754(a,1),3036(a,1,2,1))]. given #305 (A,wt=18): 1528 ((x' ^ y) ^ z) ^ (x ^ u)' = (x' ^ y) ^ z. [para(1496(a,1),1511(a,1,2,1,1))]. given #306 (T,wt=14): 3185 ((x ^ y') ^ z) ^ ((y ^ u) ^ v) = c_0. [para(1756(a,1),3036(a,1,2,1))]. given #307 (T,wt=14): 3186 (x ^ (y' ^ z)) ^ ((y ^ u) ^ v) = c_0. [para(1758(a,1),3036(a,1,2,1))]. given #308 (T,wt=14): 3187 (x ^ (y ^ z')) ^ ((z ^ u) ^ v) = c_0. [para(1759(a,1),3036(a,1,2,1))]. given #309 (T,wt=14): 3188 ((x' ^ y) ^ z) ^ ((u ^ x) ^ v) = c_0. [para(1793(a,1),3036(a,1,2,1))]. given #310 (A,wt=18): 1533 (x ^ y)' ^ ((z ^ x') ^ u) = (z ^ x') ^ u. [para(1512(a,1),1377(a,1,1,1,1)),rewrite(1137(7),1137(11))]. given #311 (T,wt=14): 3189 ((x ^ y') ^ z) ^ ((u ^ y) ^ v) = c_0. [para(1795(a,1),3036(a,1,2,1))]. given #312 (T,wt=14): 3215 (((x' ^ y) ^ z) ^ u) ^ (x ^ v) = c_0. [para(1723(a,1),3037(a,1,2,1))]. given #313 (T,wt=14): 3216 (((x ^ y') ^ z) ^ u) ^ (y ^ v) = c_0. [para(1724(a,1),3037(a,1,2,1))]. given #314 (T,wt=14): 3217 (x ^ ((y' ^ z) ^ u)) ^ (y ^ v) = c_0. [para(1725(a,1),3037(a,1,2,1))]. given #315 (A,wt=18): 1534 ((x ^ y') ^ z) ^ (y ^ u)' = (x ^ y') ^ z. [para(1512(a,1),1511(a,1,2,1,1))]. given #316 (T,wt=14): 3218 ((x ^ (y' ^ z)) ^ u) ^ (y ^ v) = c_0. [para(1753(a,1),3037(a,1,2,1))]. given #317 (T,wt=14): 3219 ((x ^ (y ^ z')) ^ u) ^ (z ^ v) = c_0. [para(1755(a,1),3037(a,1,2,1))]. given #318 (T,wt=14): 3220 (x ^ ((y ^ z') ^ u)) ^ (z ^ v) = c_0. [para(1757(a,1),3037(a,1,2,1))]. given #319 (T,wt=14): 3221 (x ^ (y ^ (z' ^ u))) ^ (z ^ v) = c_0. [para(1854(a,1),3037(a,1,2,1))]. given #320 (A,wt=18): 1566 (x ^ y)' ^ (z ^ (x' ^ u)) = z ^ (x' ^ u). [para(1513(a,1),1377(a,1,1,1,1)),rewrite(1137(7),1137(11))]. given #321 (T,wt=14): 3222 (x ^ (y ^ (z ^ u'))) ^ (u ^ v) = c_0. [para(1856(a,1),3037(a,1,2,1))]. given #322 (T,wt=14): 3223 (((x ^ y) ^ z) ^ u) ^ (x' ^ v) = c_0. [para(1727(a,1),3037(a,1,2,1))]. given #323 (T,wt=14): 3224 (((x ^ y) ^ z) ^ u) ^ (y' ^ v) = c_0. [para(1729(a,1),3037(a,1,2,1))]. given #324 (T,wt=14): 3225 (x ^ ((y ^ z) ^ u)) ^ (y' ^ v) = c_0. [para(1730(a,1),3037(a,1,2,1))]. given #325 (A,wt=17): 1567 (x ^ y')' ^ ((y ^ z) ^ u) = (y ^ z) ^ u. [para(1377(a,1),1513(a,1,1,1,2))]. given #326 (T,wt=14): 3226 ((x ^ (y ^ z)) ^ u) ^ (y' ^ v) = c_0. [para(1760(a,1),3037(a,1,2,1))]. given #327 (T,wt=14): 3228 ((x ^ (y ^ z)) ^ u) ^ (z' ^ v) = c_0. [para(1764(a,1),3037(a,1,2,1))]. given #328 (T,wt=14): 3229 (x ^ ((y ^ z) ^ u)) ^ (z' ^ v) = c_0. [para(1766(a,1),3037(a,1,2,1))]. given #329 (T,wt=14): 3230 (x ^ (y ^ (z ^ u))) ^ (z' ^ v) = c_0. [para(1863(a,1),3037(a,1,2,1))]. given #330 (A,wt=18): 1568 (x ^ y)' ^ ((y' ^ z) ^ u) = (y' ^ z) ^ u. [para(1496(a,1),1513(a,1,1,1,2))]. given #331 (T,wt=14): 3231 (x ^ (y ^ (z ^ u))) ^ (u' ^ v) = c_0. [para(1865(a,1),3037(a,1,2,1))]. given #332 (T,wt=14): 3242 ((x ^ y)' ^ z) ^ ((y ^ x) ^ u) = c_0. [para(1726(a,1),3038(a,1,2))]. given #333 (T,wt=14): 3243 (x ^ y) ^ (((x' ^ z) ^ u) ^ v) = c_0. [para(1754(a,1),3038(a,1,1))]. given #334 (T,wt=14): 3244 (x ^ y) ^ (((z ^ x') ^ u) ^ v) = c_0. [para(1756(a,1),3038(a,1,1))]. given #335 (A,wt=18): 1569 (x ^ (y' ^ z)) ^ (y ^ u)' = x ^ (y' ^ z). [para(1513(a,1),1511(a,1,2,1,1))]. given #336 (T,wt=14): 3245 (x ^ y) ^ ((z ^ (x' ^ u)) ^ v) = c_0. [para(1758(a,1),3038(a,1,1))]. given #337 (T,wt=14): 3246 (x ^ y) ^ ((z ^ (u ^ x')) ^ v) = c_0. [para(1759(a,1),3038(a,1,1))]. given #338 (T,wt=14): 3247 (x ^ y) ^ (((y' ^ z) ^ u) ^ v) = c_0. [para(1793(a,1),3038(a,1,1))]. given #339 (T,wt=14): 3248 (((x' ^ y) ^ z) ^ u) ^ (v ^ x) = c_0. [para(1793(a,1),3038(a,1,2)),rewrite(1137(5))]. given #340 (A,wt=18): 1570 (x ^ y)' ^ ((z ^ y') ^ u) = (z ^ y') ^ u. [para(1512(a,1),1513(a,1,1,1,2))]. given #341 (T,wt=14): 3249 (x ^ y) ^ (((z ^ y') ^ u) ^ v) = c_0. [para(1795(a,1),3038(a,1,1))]. given #342 (T,wt=14): 3250 (((x ^ y') ^ z) ^ u) ^ (v ^ y) = c_0. [para(1795(a,1),3038(a,1,2)),rewrite(1137(5))]. given #343 (T,wt=14): 3264 x ^ ((((x' ^ y) ^ z) ^ u) ^ v) = c_0. [para(1723(a,1),3039(a,1,2)),rewrite(1137(6),1630(6))]. given #344 (T,wt=14): 3266 x ^ ((((y ^ x') ^ z) ^ u) ^ v) = c_0. [para(1724(a,1),3039(a,1,2)),rewrite(1137(6),1630(6))]. given #345 (A,wt=18): 1572 (x ^ y)' ^ (z ^ (y' ^ u)) = z ^ (y' ^ u). [para(1513(a,1),1513(a,1,1,1,2))]. given #346 (T,wt=14): 3267 x ^ ((y ^ ((x' ^ z) ^ u)) ^ v) = c_0. [para(1725(a,1),3039(a,1,2)),rewrite(1137(6),1630(6))]. given #347 (T,wt=14): 3268 x ^ (((y ^ (x' ^ z)) ^ u) ^ v) = c_0. [para(1753(a,1),3039(a,1,2)),rewrite(1137(6),1630(6))]. given #348 (T,wt=14): 3269 x ^ (((y ^ (z ^ x')) ^ u) ^ v) = c_0. [para(1755(a,1),3039(a,1,2)),rewrite(1137(6),1630(6))]. given #349 (T,wt=14): 3271 x ^ ((y ^ ((z ^ x') ^ u)) ^ v) = c_0. [para(1757(a,1),3039(a,1,2)),rewrite(1137(6),1630(6))]. given #350 (A,wt=19): 1576 x ^ ((y ^ (z ^ x'))' ^ ((z ^ x') ^ u)') = x. [para(1194(a,1),1519(a,1,2,1)),rewrite(1137(11))]. given #351 (T,wt=14): 3272 x ^ ((y ^ (z ^ (x' ^ u))) ^ v) = c_0. [para(1854(a,1),3039(a,1,2)),rewrite(1137(6),1630(6))]. given #352 (T,wt=14): 3273 x ^ ((y ^ (z ^ (u ^ x'))) ^ v) = c_0. [para(1856(a,1),3039(a,1,2)),rewrite(1137(6),1630(6))]. given #353 (T,wt=14): 3280 x' ^ ((((x ^ y) ^ z) ^ u) ^ v) = c_0. [para(1727(a,1),3039(a,1,2)),rewrite(1137(5),1630(6))]. given #354 (T,wt=14): 3281 x' ^ ((((y ^ x) ^ z) ^ u) ^ v) = c_0. [para(1729(a,1),3039(a,1,2)),rewrite(1137(5),1630(6))]. given #355 (A,wt=19): 1584 x ^ (y ^ ((z ^ x')' ^ (x' ^ u)')')' = x. [para(1194(a,1),1520(a,1,2,1,2))]. given #356 (T,wt=14): 3282 x' ^ ((y ^ ((x ^ z) ^ u)) ^ v) = c_0. [para(1730(a,1),3039(a,1,2)),rewrite(1137(5),1630(6))]. given #357 (T,wt=14): 3283 x' ^ (((y ^ (x ^ z)) ^ u) ^ v) = c_0. [para(1760(a,1),3039(a,1,2)),rewrite(1137(5),1630(6))]. given #358 (T,wt=14): 3285 x' ^ (((y ^ (z ^ x)) ^ u) ^ v) = c_0. [para(1764(a,1),3039(a,1,2)),rewrite(1137(5),1630(6))]. given #359 (T,wt=14): 3286 x' ^ ((y ^ ((z ^ x) ^ u)) ^ v) = c_0. [para(1766(a,1),3039(a,1,2)),rewrite(1137(5),1630(6))]. given #360 (A,wt=17): 1586 ((x ^ y) ^ z) ^ (u ^ x')' = (x ^ y) ^ z. [para(1377(a,1),1520(a,1,2,1,2))]. given #361 (T,wt=14): 3287 x' ^ ((y ^ (z ^ (x ^ u))) ^ v) = c_0. [para(1863(a,1),3039(a,1,2)),rewrite(1137(5),1630(6))]. given #362 (T,wt=14): 3288 x' ^ ((y ^ (z ^ (u ^ x))) ^ v) = c_0. [para(1865(a,1),3039(a,1,2)),rewrite(1137(5),1630(6))]. given #363 (T,wt=14): 3290 (x ^ y) ^ (z ^ ((x' ^ u) ^ v)) = c_0. [para(1754(a,1),3039(a,1,1))]. given #364 (T,wt=14): 3291 (x ^ y) ^ (z ^ ((u ^ x') ^ v)) = c_0. [para(1756(a,1),3039(a,1,1))]. given #365 (A,wt=18): 1587 ((x' ^ y) ^ z) ^ (u ^ x)' = (x' ^ y) ^ z. [para(1496(a,1),1520(a,1,2,1,2))]. given #366 (T,wt=14): 3293 (x ^ y) ^ (z ^ (u ^ (x' ^ v))) = c_0. [para(1758(a,1),3039(a,1,1))]. given #367 (T,wt=14): 3294 (x ^ y) ^ (z ^ (u ^ (v ^ x'))) = c_0. [para(1759(a,1),3039(a,1,1))]. given #368 (T,wt=14): 3295 (x ^ y) ^ (z ^ ((y' ^ u) ^ v)) = c_0. [para(1793(a,1),3039(a,1,1))]. given #369 (T,wt=14): 3296 (x ^ y) ^ (z ^ ((u ^ y') ^ v)) = c_0. [para(1795(a,1),3039(a,1,1))]. given #370 (A,wt=18): 1588 ((x ^ y') ^ z) ^ (u ^ y)' = (x ^ y') ^ z. [para(1512(a,1),1520(a,1,2,1,2))]. given #371 (T,wt=14): 3307 (x ^ (y ^ z)') ^ ((z ^ y) ^ u) = c_0. [para(1726(a,1),3041(a,1,2))]. given #372 (T,wt=14): 3308 (x ^ ((y' ^ z) ^ u)) ^ (v ^ y) = c_0. [para(1793(a,1),3041(a,1,2)),rewrite(1137(5))]. given #373 (T,wt=14): 3309 (x ^ ((y ^ z') ^ u)) ^ (v ^ z) = c_0. [para(1795(a,1),3041(a,1,2)),rewrite(1137(5))]. given #374 (T,wt=14): 3397 x ^ (y ^ (((x' ^ z) ^ u) ^ v)) = c_0. [para(1723(a,1),3042(a,1,1))]. given #375 (A,wt=18): 1589 (x' ^ y) ^ (y ^ (x' ^ z)) = y ^ (x' ^ z). [para(1520(a,1),1226(a,1,1,1,1))]. given #376 (T,wt=12): 7998 x ^ (y' ^ (y' ^ x)') = c_0. [para(1589(a,1),3045(a,1))]. given #377 (T,wt=10): 8086 x ^ (y ^ (y ^ x)') = c_0. [para(1137(a,1),7998(a,1,2,1)),rewrite(1137(2))]. given #378 (T,wt=10): 8088 x ^ (y ^ (x ^ y)') = c_0. [para(1630(a,1),8086(a,1,2,2,1))]. given #379 (T,wt=14): 3399 x ^ (y ^ (((z ^ x') ^ u) ^ v)) = c_0. [para(1724(a,1),3042(a,1,1))]. given #380 (A,wt=18): 1590 (x ^ (y' ^ z)) ^ (u ^ y)' = x ^ (y' ^ z). [para(1513(a,1),1520(a,1,2,1,2))]. given #381 (T,wt=14): 3400 x ^ (y ^ (z ^ ((x' ^ u) ^ v))) = c_0. [para(1725(a,1),3042(a,1,1))]. given #382 (T,wt=14): 3401 x ^ (y ^ ((z ^ (x' ^ u)) ^ v)) = c_0. [para(1753(a,1),3042(a,1,1))]. given #383 (T,wt=14): 3402 x ^ (y ^ ((z ^ (u ^ x')) ^ v)) = c_0. [para(1755(a,1),3042(a,1,1))]. given #384 (T,wt=14): 3404 x ^ (y ^ (z ^ ((u ^ x') ^ v))) = c_0. [para(1757(a,1),3042(a,1,1))]. given #385 (A,wt=18): 1602 (x ^ y)' ^ (z ^ (u ^ x')) = z ^ (u ^ x'). [para(1529(a,1),1377(a,1,1,1,1)),rewrite(1137(7),1137(11))]. given #386 (T,wt=14): 3405 x ^ (y ^ (z ^ (u ^ (x' ^ v)))) = c_0. [para(1854(a,1),3042(a,1,1))]. given #387 (T,wt=14): 3406 x ^ (y ^ (z ^ (u ^ (v ^ x')))) = c_0. [para(1856(a,1),3042(a,1,1))]. given #388 (T,wt=14): 3410 x' ^ (y ^ (((x ^ z) ^ u) ^ v)) = c_0. [para(1727(a,1),3042(a,1,1))]. given #389 (T,wt=14): 3411 x' ^ (y ^ (((z ^ x) ^ u) ^ v)) = c_0. [para(1729(a,1),3042(a,1,1))]. given #390 (A,wt=18): 1603 (x ^ (y ^ z')) ^ (z ^ u)' = x ^ (y ^ z'). [para(1529(a,1),1511(a,1,2,1,1))]. given #391 (T,wt=14): 3412 x' ^ (y ^ (z ^ ((x ^ u) ^ v))) = c_0. [para(1730(a,1),3042(a,1,1))]. given #392 (T,wt=14): 3413 x' ^ (y ^ ((z ^ (x ^ u)) ^ v)) = c_0. [para(1760(a,1),3042(a,1,1))]. given #393 (T,wt=14): 3414 x' ^ (y ^ ((z ^ (u ^ x)) ^ v)) = c_0. [para(1764(a,1),3042(a,1,1))]. given #394 (T,wt=14): 3415 x' ^ (y ^ (z ^ ((u ^ x) ^ v))) = c_0. [para(1766(a,1),3042(a,1,1))]. given #395 (A,wt=18): 1605 (x ^ y)' ^ (z ^ (u ^ y')) = z ^ (u ^ y'). [para(1529(a,1),1513(a,1,1,1,2))]. given #396 (T,wt=14): 3416 x' ^ (y ^ (z ^ (u ^ (x ^ v)))) = c_0. [para(1863(a,1),3042(a,1,1))]. given #397 (T,wt=14): 3417 x' ^ (y ^ (z ^ (u ^ (v ^ x)))) = c_0. [para(1865(a,1),3042(a,1,1))]. given #398 (T,wt=14): 3426 ((x' ^ y) ^ z) ^ (u ^ (x ^ v)) = c_0. [para(1754(a,1),3043(a,1,2,2))]. given #399 (T,wt=14): 3427 ((x ^ y') ^ z) ^ (u ^ (y ^ v)) = c_0. [para(1756(a,1),3043(a,1,2,2))]. given #400 (A,wt=18): 1606 (x ^ (y ^ z')) ^ (u ^ z)' = x ^ (y ^ z'). [para(1529(a,1),1520(a,1,2,1,2))]. given #401 (T,wt=14): 3428 (x ^ (y' ^ z)) ^ (u ^ (y ^ v)) = c_0. [para(1758(a,1),3043(a,1,2,2))]. given #402 (T,wt=14): 3429 (x ^ (y ^ z')) ^ (u ^ (z ^ v)) = c_0. [para(1759(a,1),3043(a,1,2,2))]. given #403 (T,wt=14): 3430 ((x' ^ y) ^ z) ^ (u ^ (v ^ x)) = c_0. [para(1793(a,1),3043(a,1,2,2))]. given #404 (T,wt=14): 3431 ((x ^ y') ^ z) ^ (u ^ (v ^ y)) = c_0. [para(1795(a,1),3043(a,1,2,2))]. given #405 (A,wt=39): 1612 (x ^ ((x ^ y)' ^ z)')' ^ ((x ^ y)' ^ ((x ^ ((x ^ y)' ^ z)') ^ u)') = (x ^ ((x ^ y)' ^ z)')'. [para(1227(a,1),1241(a,1,2,1,1))]. given #406 (T,wt=14): 3432 ((x ^ (y' ^ z)) ^ u) ^ (v ^ y) = c_0. [para(1753(a,1),3045(a,1,2,2))]. given #407 (T,wt=14): 3433 ((x ^ (y ^ z')) ^ u) ^ (v ^ z) = c_0. [para(1755(a,1),3045(a,1,2,2))]. given #408 (T,wt=14): 3434 (x ^ (y ^ (z' ^ u))) ^ (v ^ z) = c_0. [para(1854(a,1),3045(a,1,2,2))]. given #409 (T,wt=14): 3435 (x ^ (y ^ (z ^ u'))) ^ (v ^ u) = c_0. [para(1856(a,1),3045(a,1,2,2))]. given #410 (A,wt=28): 1617 ((x ^ y) ^ z)' ^ (x ^ ((x ^ y)' ^ u)')' = (x ^ ((x ^ y)' ^ u)')'. [para(1227(a,1),1377(a,1,1,1,1))]. given #411 (T,wt=14): 3436 (((x ^ y) ^ z) ^ u) ^ (v ^ x') = c_0. [para(1727(a,1),3045(a,1,2,2))]. given #412 (T,wt=14): 3437 (((x ^ y) ^ z) ^ u) ^ (v ^ y') = c_0. [para(1729(a,1),3045(a,1,2,2))]. given #413 (T,wt=14): 3438 (x ^ ((y ^ z) ^ u)) ^ (v ^ y') = c_0. [para(1730(a,1),3045(a,1,2,2))]. given #414 (T,wt=14): 3439 ((x ^ (y ^ z)) ^ u) ^ (v ^ y') = c_0. [para(1760(a,1),3045(a,1,2,2))]. given #415 (A,wt=18): 1624 (x ^ y') ^ (x ^ (y' ^ z)) = x ^ (y' ^ z). [para(1513(a,1),1227(a,1,1,2,1))]. given #416 (T,wt=14): 3441 ((x ^ (y ^ z)) ^ u) ^ (v ^ z') = c_0. [para(1764(a,1),3045(a,1,2,2))]. given #417 (T,wt=14): 3442 (x ^ ((y ^ z) ^ u)) ^ (v ^ z') = c_0. [para(1766(a,1),3045(a,1,2,2))]. given #418 (T,wt=14): 3443 (x ^ (y ^ (z ^ u))) ^ (v ^ z') = c_0. [para(1863(a,1),3045(a,1,2,2))]. given #419 (T,wt=14): 3444 (x ^ (y ^ (z ^ u))) ^ (v ^ u') = c_0. [para(1865(a,1),3045(a,1,2,2))]. given #420 (A,wt=18): 1626 (x ^ y') ^ (x ^ (z ^ y')) = x ^ (z ^ y'). [para(1529(a,1),1227(a,1,1,2,1))]. given #421 (T,wt=14): 3450 ((x ^ y) ^ z) ^ ((y ^ x)' ^ u) = c_0. [para(1726(a,1),3046(a,1,1))]. given #422 (T,wt=14): 3530 ((x ^ y) ^ z) ^ (u ^ (y ^ x)') = c_0. [para(1726(a,1),3047(a,1,1))]. given #423 (T,wt=14): 3562 (x ^ y)' ^ (((y ^ x) ^ z) ^ u) = c_0. [para(1726(a,1),3137(a,1,2,1))]. given #424 (T,wt=14): 3580 (x ^ y)' ^ (z ^ ((y ^ x) ^ u)) = c_0. [para(1726(a,1),3140(a,1,2,2))]. given #425 (A,wt=16): 1634 (x ^ y)' ^ ((y ^ x) ^ z)' = (x ^ y)'. [para(1544(a,1),1377(a,1,1,1,1)),rewrite(1630(6))]. given #426 (T,wt=14): 3625 (x ^ y) ^ (((y ^ x)' ^ z) ^ u) = c_0. [para(1544(a,1),3052(a,1,2)),rewrite(1630(6))]. given #427 (T,wt=14): 3626 ((x ^ y) ^ z) ^ ((x' ^ u) ^ v) = c_0. [para(1497(a,1),3052(a,1,1,1))]. given #428 (T,wt=14): 3627 ((x ^ y) ^ z) ^ ((y' ^ u) ^ v) = c_0. [para(1506(a,1),3052(a,1,1,1))]. given #429 (T,wt=14): 3631 ((x ^ y) ^ z) ^ ((u ^ x') ^ v) = c_0. [para(1552(a,1),3052(a,1,1,1))]. given #430 (A,wt=17): 1636 (x ^ y) ^ (x ^ (z ^ (x ^ y)')') = x ^ y. [para(1226(a,1),1544(a,2)),rewrite(1630(6),1630(12),1630(14),1178(15))]. given #431 (T,wt=14): 3632 ((x ^ y) ^ z) ^ ((u ^ y') ^ v) = c_0. [para(1562(a,1),3052(a,1,1,1))]. given #432 (T,wt=14): 3653 (x ^ y) ^ ((z ^ (y ^ x)') ^ u) = c_0. [para(1544(a,1),3053(a,1,2)),rewrite(1630(6))]. given #433 (T,wt=14): 3654 (x' ^ y) ^ (((x ^ z) ^ u) ^ v) = c_0. [para(1499(a,1),3053(a,1,1,1))]. given #434 (T,wt=14): 3655 (x' ^ y) ^ (((z ^ x) ^ u) ^ v) = c_0. [para(1573(a,1),3053(a,1,1,1))]. given #435 (A,wt=28): 1640 ((x ^ y) ^ z)' ^ (x ^ (u ^ (x ^ y)')')' = (x ^ (u ^ (x ^ y)')')'. [back_rewrite(1546),rewrite(1630(8),1630(15))]. given #436 (T,wt=14): 3656 (x' ^ y) ^ ((z ^ (x ^ u)) ^ v) = c_0. [para(1578(a,1),3053(a,1,1,1))]. given #437 (T,wt=14): 3657 (x' ^ y) ^ ((z ^ (u ^ x)) ^ v) = c_0. [para(1672(a,1),3053(a,1,1,1))]. given #438 (T,wt=14): 3668 (x ^ y)' ^ ((z ^ (y ^ x)) ^ u) = c_0. [para(1628(a,1),3053(a,1,2)),rewrite(1137(3),1630(6))]. given #439 (T,wt=14): 3689 (x ^ y) ^ (z ^ ((y ^ x)' ^ u)) = c_0. [para(1544(a,1),3054(a,1,2)),rewrite(1630(6))]. given #440 (A,wt=39): 1641 (x ^ (y ^ (x ^ z)')')' ^ ((x ^ z)' ^ ((x ^ (y ^ (x ^ z)')') ^ u)') = (x ^ (y ^ (x ^ z)')')'. [back_rewrite(1541),rewrite(1630(5),1630(11),1630(16),1630(22))]. given #441 (T,wt=14): 3690 (x ^ (y' ^ z)) ^ ((u ^ y) ^ v) = c_0. [para(1401(a,1),3054(a,1,2))]. given #442 (T,wt=14): 3691 (x ^ (y ^ z)) ^ ((y' ^ u) ^ v) = c_0. [para(1497(a,1),3054(a,1,1,2))]. given #443 (T,wt=14): 3692 (x ^ (y ^ z)) ^ ((z' ^ u) ^ v) = c_0. [para(1506(a,1),3054(a,1,1,2))]. given #444 (T,wt=14): 3695 (x ^ (y ^ z)) ^ ((u ^ y') ^ v) = c_0. [para(1552(a,1),3054(a,1,1,2))]. given #445 (A,wt=39): 1642 (x ^ (y ^ (x ^ z)')')' ^ ((x ^ z)' ^ (u ^ (x ^ (y ^ (x ^ z)')'))') = (x ^ (y ^ (x ^ z)')')'. [back_rewrite(1536),rewrite(1630(5),1630(11),1630(16),1630(22))]. given #446 (T,wt=14): 3696 (x ^ (y ^ z)) ^ ((u ^ z') ^ v) = c_0. [para(1562(a,1),3054(a,1,1,2))]. given #447 (T,wt=14): 3697 (x ^ (y' ^ z)) ^ (u ^ (v ^ y)) = c_0. [para(1714(a,1),3054(a,1,2))]. given #448 (T,wt=14): 3698 (x ^ (y ^ z')) ^ ((u ^ z) ^ v) = c_0. [para(1561(a,1),3054(a,1,1,2))]. given #449 (T,wt=14): 3823 (x ^ y) ^ ((z ^ (y' ^ u)) ^ v) = c_0. [para(1520(a,1),3055(a,1,1,2))]. given #450 (A,wt=32): 1644 ((x ^ y) ^ z)' ^ (x ^ (u ^ ((x ^ y) ^ z)')')' = (x ^ (u ^ ((x ^ y) ^ z)')')'. [back_rewrite(1509),rewrite(1630(6),1630(11),1630(17))]. given #451 (T,wt=14): 3824 (x ^ (y ^ (z ^ u)')) ^ (u ^ z) = c_0. [para(1544(a,1),3055(a,1,2))]. given #452 (T,wt=14): 3825 (x ^ y) ^ ((z ^ (u ^ y')) ^ v) = c_0. [para(1574(a,1),3055(a,1,1,2))]. given #453 (T,wt=14): 3826 (x ^ y') ^ (((y ^ z) ^ u) ^ v) = c_0. [para(1499(a,1),3055(a,1,1,2))]. given #454 (T,wt=14): 3827 (x ^ y') ^ (((z ^ y) ^ u) ^ v) = c_0. [para(1573(a,1),3055(a,1,1,2))]. given #455 (A,wt=26): 1645 (x ^ y)' ^ (y ^ (z ^ (x ^ y)')')' = (y ^ (z ^ (x ^ y)')')'. [back_rewrite(1491),rewrite(1630(5),1630(9),1630(14))]. given #456 (T,wt=14): 3828 (x ^ y') ^ ((z ^ (y ^ u)) ^ v) = c_0. [para(1578(a,1),3055(a,1,1,2))]. given #457 (T,wt=14): 3829 (x ^ y') ^ ((z ^ (u ^ y)) ^ v) = c_0. [para(1672(a,1),3055(a,1,1,2))]. given #458 (T,wt=14): 3831 (x ^ (y ^ z')) ^ (u ^ (v ^ z)) = c_0. [para(1714(a,1),3055(a,1,2))]. given #459 (T,wt=14): 3840 (x ^ (y ^ (z ^ u))) ^ (u ^ z)' = c_0. [para(1628(a,1),3055(a,1,2)),rewrite(1137(3))]. given #460 (A,wt=26): 1646 (x ^ y)' ^ (x ^ (z ^ (x ^ y)')')' = (x ^ (z ^ (x ^ y)')')'. [back_rewrite(1486),rewrite(1630(5),1630(9),1630(14))]. given #461 (T,wt=14): 3864 ((x ^ y) ^ z) ^ (u ^ (x' ^ v)) = c_0. [para(1497(a,1),3056(a,1,1,1))]. given #462 (T,wt=14): 3865 ((x ^ y) ^ z) ^ (u ^ (y' ^ v)) = c_0. [para(1506(a,1),3056(a,1,1,1))]. given #463 (T,wt=14): 3868 ((x ^ y) ^ z) ^ (u ^ (v ^ x')) = c_0. [para(1552(a,1),3056(a,1,1,1))]. given #464 (T,wt=14): 3869 ((x ^ y) ^ z) ^ (u ^ (v ^ y')) = c_0. [para(1562(a,1),3056(a,1,1,1))]. given #465 (A,wt=40): 1652 (((x ^ y)' ^ (x ^ z)')' ^ ((x ^ (u ^ ((x ^ y)' ^ (x ^ z)'))')' ^ v)')' = (x ^ y)' ^ (x ^ z)'. [back_rewrite(1367),rewrite(1630(8),1630(18))]. given #466 (T,wt=14): 3883 ((x ^ y)' ^ z) ^ (u ^ (y ^ x)) = c_0. [para(1628(a,1),3056(a,1,1,1))]. given #467 (T,wt=14): 3918 (x' ^ y) ^ (z ^ ((x ^ u) ^ v)) = c_0. [para(1499(a,1),3057(a,1,1,1))]. given #468 (T,wt=14): 3920 (x' ^ y) ^ (z ^ ((u ^ x) ^ v)) = c_0. [para(1573(a,1),3057(a,1,1,1))]. given #469 (T,wt=14): 3921 (x' ^ y) ^ (z ^ (u ^ (x ^ v))) = c_0. [para(1578(a,1),3057(a,1,1,1))]. given #470 (A,wt=40): 1655 (((x ^ y)' ^ (y ^ z)')' ^ ((y ^ (u ^ ((x ^ y)' ^ (y ^ z)'))')' ^ v)')' = (x ^ y)' ^ (y ^ z)'. [back_rewrite(1364),rewrite(1630(8),1630(18))]. given #471 (T,wt=14): 3922 (x' ^ y) ^ (z ^ (u ^ (v ^ x))) = c_0. [para(1672(a,1),3057(a,1,1,1))]. given #472 (T,wt=14): 3976 (x ^ y)' ^ (z ^ (u ^ (y ^ x))) = c_0. [para(1714(a,1),3143(a,1,2))]. given #473 (T,wt=14): 4080 (x ^ y') ^ (z ^ ((y ^ u) ^ v)) = c_0. [para(1552(a,1),3146(a,1,2,2,1))]. given #474 (T,wt=14): 4081 (x ^ y') ^ (z ^ ((u ^ y) ^ v)) = c_0. [para(1562(a,1),3146(a,1,2,2,1))]. given #475 (A,wt=25): 1658 (x ^ y) ^ ((x ^ ((x ^ y)' ^ z)') ^ ((x ^ y)' ^ u)') = x ^ y. [back_rewrite(1627),rewrite(1630(12))]. given #476 (T,wt=14): 4222 (x ^ (y ^ z)) ^ (u ^ (y' ^ v)) = c_0. [para(1578(a,1),3149(a,1,2,2,1))]. given #477 (T,wt=14): 4223 (x ^ (y ^ z)) ^ (u ^ (z' ^ v)) = c_0. [para(1672(a,1),3149(a,1,2,2,1))]. given #478 (T,wt=14): 4247 (x ^ y') ^ (z ^ (u ^ (y ^ v))) = c_0. [para(1552(a,1),3150(a,1,2,2,2))]. given #479 (T,wt=14): 4248 (x ^ y') ^ (z ^ (u ^ (v ^ y))) = c_0. [para(1562(a,1),3150(a,1,2,2,2))]. given #480 (A,wt=17): 1659 x ^ ((y ^ (z ^ x'))' ^ (x' ^ u)') = x. [back_rewrite(1625),rewrite(1630(9))]. given #481 (T,wt=14): 4249 (x ^ y) ^ (z ^ (u ^ (y' ^ v))) = c_0. [para(1553(a,1),3150(a,1,2,2,2))]. given #482 (T,wt=14): 4250 (x ^ y) ^ (z ^ (u ^ (v ^ y'))) = c_0. [para(1561(a,1),3150(a,1,2,2,2))]. given #483 (T,wt=14): 4251 (x ^ y) ^ (z ^ (u ^ (y ^ x)')) = c_0. [para(1628(a,1),3150(a,1,2,2,2))]. given #484 (T,wt=14): 4264 (x ^ (y ^ z)) ^ (u ^ (v ^ y')) = c_0. [para(1578(a,1),3151(a,1,2,2,2))]. given #485 (A,wt=17): 1660 x ^ ((y ^ (x' ^ z))' ^ (x' ^ u)') = x. [back_rewrite(1623),rewrite(1630(9))]. given #486 (T,wt=14): 4265 (x ^ (y ^ z)) ^ (u ^ (v ^ z')) = c_0. [para(1672(a,1),3151(a,1,2,2,2))]. given #487 (T,wt=14): 4737 (x ^ (y ^ z)) ^ ((z ^ y)' ^ u) = c_0. [para(1628(a,1),3175(a,1,2,1)),rewrite(1137(3))]. given #488 (T,wt=14): 5208 (x ^ (y ^ z)) ^ (u ^ (z ^ y)') = c_0. [para(1628(a,1),3257(a,1,2,2))]. given #489 (T,wt=14): 5348 (x ^ (y ^ z)') ^ (u ^ (z ^ y)) = c_0. [para(1628(a,1),3262(a,1,1,2))]. given #490 (A,wt=25): 1661 (x ^ y) ^ ((x ^ (z ^ (x ^ y)')') ^ ((x ^ y)' ^ u)') = x ^ y. [back_rewrite(1622),rewrite(1630(5),1630(12))]. given #491 (T,wt=14): 7993 (x' ^ y)' ^ (y ^ (x' ^ z)) = c_0. [para(1589(a,1),3033(a,1,2))]. given #492 (T,wt=12): 11740 (x ^ y)' ^ (y ^ (x ^ z)) = c_0. [para(1137(a,1),7993(a,1,1,1,1)),rewrite(1137(4))]. given #493 (T,wt=12): 11803 (x ^ y)' ^ (y ^ (z ^ x)) = c_0. [para(1289(a,1),11740(a,1,2,2))]. given #494 (T,wt=12): 11805 (x ^ (y ^ z)) ^ (y ^ x)' = c_0. [para(11740(a,1),1544(a,1,1)),rewrite(1459(7)),flip(a)]. given #495 (A,wt=25): 1662 (x ^ y) ^ ((z ^ (x ^ y)')' ^ (x ^ ((x ^ y)' ^ u)')) = x ^ y. [back_rewrite(1621),rewrite(1630(12))]. given #496 (T,wt=12): 11807 (x ^ y)' ^ (x ^ (y ^ z)) = c_0. [para(1630(a,1),11740(a,1,1,1))]. given #497 (T,wt=12): 11808 (x ^ y)' ^ ((x ^ z) ^ y) = c_0. [para(1630(a,1),11740(a,1,2))]. given #498 (T,wt=12): 11816 (x ^ y)' ^ (x ^ (z ^ y)) = c_0. [para(1714(a,1),11740(a,1,2))]. given #499 (T,wt=12): 11828 (x ^ (x ^ y)') ^ (y ^ z) = c_0. [para(8086(a,1),11740(a,1,1,1)),rewrite(1463(8))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 39 (0.00 of 8.82 sec). given #500 (A,wt=17): 1663 x ^ (((y ^ x') ^ z)' ^ (x' ^ u)') = x. [back_rewrite(1620),rewrite(1630(9))]. Low Water (keep, True_semantics): wt=40 given #501 (T,wt=12): 11829 (x ^ (y ^ x)') ^ (y ^ z) = c_0. [para(8088(a,1),11740(a,1,1,1)),rewrite(1463(8))]. given #502 (T,wt=12): 11844 (x ^ (y ^ z)) ^ (z ^ x)' = c_0. [para(11803(a,1),1544(a,1,1)),rewrite(1459(7)),flip(a)]. given #503 (T,wt=12): 11845 (x ^ y)' ^ ((z ^ x) ^ y) = c_0. [para(1630(a,1),11803(a,1,2))]. given #504 (T,wt=12): 11852 (x ^ y)' ^ ((y ^ z) ^ x) = c_0. [para(1379(a,1),11803(a,1,2))]. given #505 (A,wt=17): 1664 x ^ (((x' ^ y) ^ z)' ^ (x' ^ u)') = x. [back_rewrite(1619),rewrite(1630(9))]. given #506 (T,wt=12): 11854 (x ^ y)' ^ ((z ^ y) ^ x) = c_0. [para(1401(a,1),11803(a,1,2))]. given #507 (T,wt=12): 11903 (x ^ (x ^ y)') ^ (z ^ y) = c_0. [para(8086(a,1),11803(a,1,1,1)),rewrite(1463(8))]. given #508 (T,wt=12): 11904 (x ^ (y ^ x)') ^ (z ^ y) = c_0. [para(8088(a,1),11803(a,1,1,1)),rewrite(1463(8))]. given #509 (T,wt=12): 12140 x ^ ((y ^ (y ^ x)') ^ z) = c_0. [para(8086(a,1),11807(a,1,1,1)),rewrite(1463(8))]. given #510 (A,wt=17): 1665 x' ^ (((x ^ y) ^ z)' ^ (x ^ u)') = x'. [back_rewrite(1618),rewrite(1630(8))]. Low Water (keep, True_semantics): wt=37 given #511 (T,wt=12): 12141 x ^ ((y ^ (x ^ y)') ^ z) = c_0. [para(8088(a,1),11807(a,1,1,1)),rewrite(1463(8))]. given #512 (T,wt=12): 12217 (x ^ y) ^ (z ^ (z ^ x)') = c_0. [para(8086(a,1),11808(a,1,1,1)),rewrite(1463(8))]. given #513 (T,wt=12): 12218 (x ^ y) ^ (z ^ (x ^ z)') = c_0. [para(8088(a,1),11808(a,1,1,1)),rewrite(1463(8))]. given #514 (T,wt=12): 12287 x ^ (y ^ (z ^ (z ^ x)')) = c_0. [para(8086(a,1),11816(a,1,1,1)),rewrite(1463(8))]. given #515 (A,wt=25): 1666 (x ^ y) ^ (x ^ ((z ^ (x ^ y)')' ^ ((x ^ y)' ^ u)')) = x ^ y. [back_rewrite(1616),rewrite(1630(12))]. given #516 (T,wt=12): 12288 x ^ (y ^ (z ^ (x ^ z)')) = c_0. [para(8088(a,1),11816(a,1,1,1)),rewrite(1463(8))]. given #517 (T,wt=12): 12592 ((x ^ y) ^ z) ^ (z ^ x)' = c_0. [para(1379(a,1),11844(a,1,1))]. given #518 (T,wt=12): 12594 ((x ^ y) ^ z) ^ (z ^ y)' = c_0. [para(1401(a,1),11844(a,1,1))]. given #519 (T,wt=12): 12719 (x ^ y) ^ (z ^ (z ^ y)') = c_0. [para(8086(a,1),11845(a,1,1,1)),rewrite(1463(8))]. given #520 (A,wt=21): 1667 x ^ (((x' ^ y)' ^ (x' ^ z)') ^ (x' ^ u)') = x. [back_rewrite(1614),rewrite(1630(12))]. given #521 (T,wt=12): 12720 (x ^ y) ^ (z ^ (y ^ z)') = c_0. [para(8088(a,1),11845(a,1,1,1)),rewrite(1463(8))]. given #522 (T,wt=14): 8012 x ^ (y' ^ ((y' ^ x)' ^ z)) = c_0. [para(1589(a,1),3150(a,1))]. given #523 (T,wt=12): 13831 x ^ (y ^ ((y ^ x)' ^ z)) = c_0. [para(1137(a,1),8012(a,1,2,1)),rewrite(1137(2))]. given #524 (T,wt=12): 13866 x ^ (y ^ (z ^ (y ^ x)')) = c_0. [para(1289(a,1),13831(a,1,2,2))]. given #525 (A,wt=20): 1668 x' ^ (((x ^ y)' ^ (x ^ z)') ^ (x ^ u)') = x'. [back_rewrite(1611),rewrite(1630(10))]. given #526 (T,wt=12): 13868 x ^ (y ^ ((x ^ y)' ^ z)) = c_0. [para(1630(a,1),13831(a,1,2,2,1,1))]. given #527 (T,wt=12): 13873 x ^ ((y ^ x)' ^ (y ^ z)) = c_0. [para(1703(a,1),13831(a,1,2))]. given #528 (T,wt=12): 13875 x ^ ((y ^ x)' ^ (z ^ y)) = c_0. [para(1714(a,1),13831(a,1,2))]. Low Water (keep, True_semantics): wt=35 given #529 (T,wt=12): 13893 x ^ (y ^ (z ^ (x ^ y)')) = c_0. [para(1630(a,1),13866(a,1,2,2,2,1))]. given #530 (A,wt=39): 1669 (x ^ ((x ^ y)' ^ z)')' ^ ((x ^ y)' ^ (u ^ (x ^ ((x ^ y)' ^ z)'))') = (x ^ ((x ^ y)' ^ z)')'. [back_rewrite(1608),rewrite(1630(16))]. given #531 (T,wt=12): 13894 x ^ ((y ^ z) ^ (y ^ x)') = c_0. [para(1379(a,1),13866(a,1,2))]. given #532 (T,wt=12): 13895 x ^ ((y ^ z) ^ (z ^ x)') = c_0. [para(1401(a,1),13866(a,1,2))]. given #533 (T,wt=12): 14038 x ^ ((x ^ y)' ^ (y ^ z)) = c_0. [para(1703(a,1),13868(a,1,2))]. given #534 (T,wt=12): 14040 x ^ ((x ^ y)' ^ (z ^ y)) = c_0. [para(1714(a,1),13868(a,1,2))]. given #535 (A,wt=17): 1670 x ^ ((y ^ x')' ^ (z ^ (u ^ x'))') = x. [back_rewrite(1604),rewrite(1630(9))]. Low Water (keep, True_semantics): wt=34 given #536 (T,wt=12): 14172 x ^ ((y ^ z) ^ (x ^ y)') = c_0. [para(1379(a,1),13893(a,1,2))]. given #537 (T,wt=12): 14173 x ^ ((y ^ z) ^ (x ^ z)') = c_0. [para(1401(a,1),13893(a,1,2))]. given #538 (T,wt=14): 11806 ((x ^ y) ^ z)' ^ (z ^ (y ^ x)) = c_0. [para(1544(a,1),11740(a,1,2,2))]. given #539 (T,wt=14): 11809 (x ^ y)' ^ (y ^ ((x ^ z) ^ u)) = c_0. [para(1379(a,1),11740(a,1,2,2))]. given #540 (A,wt=17): 1673 x ^ ((y ^ x')' ^ (z ^ (x' ^ u))') = x. [back_rewrite(1571),rewrite(1630(9))]. given #541 (T,wt=14): 11810 (x ^ y)' ^ (y ^ ((z ^ x) ^ u)) = c_0. [para(1401(a,1),11740(a,1,2,2))]. given #542 (T,wt=14): 11811 (x ^ y) ^ (x ^ (y' ^ z)')' = c_0. [para(1506(a,1),11740(a,1,2)),rewrite(1630(7))]. Low Water (keep, True_semantics): wt=32 given #543 (T,wt=14): 11813 (x ^ y) ^ (x ^ (z ^ y')')' = c_0. [para(1562(a,1),11740(a,1,2)),rewrite(1630(7))]. given #544 (T,wt=14): 11814 (x ^ y)' ^ (y ^ (z ^ (x ^ u))) = c_0. [para(1703(a,1),11740(a,1,2,2))]. given #545 (A,wt=25): 1675 (x ^ y) ^ ((z ^ (x ^ y)')' ^ (x ^ (u ^ (x ^ y)')')) = x ^ y. [back_rewrite(1550),rewrite(1630(9),1630(12))]. given #546 (T,wt=14): 11815 (x ^ y)' ^ (y ^ (z ^ (u ^ x))) = c_0. [para(1714(a,1),11740(a,1,2,2))]. given #547 (T,wt=14): 11817 (x ^ y') ^ (x ^ (y ^ z)')' = c_0. [para(1505(a,1),11740(a,1,2)),rewrite(1630(7))]. given #548 (T,wt=14): 11818 (x ^ y') ^ (x ^ (z ^ y)')' = c_0. [para(1561(a,1),11740(a,1,2)),rewrite(1630(7))]. given #549 (T,wt=14): 11832 (x ^ (y ^ z)) ^ ((y ^ x)' ^ u) = c_0. [para(11740(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #550 (A,wt=17): 1676 x ^ ((y ^ x')' ^ ((z ^ x') ^ u)') = x. [back_rewrite(1549),rewrite(1630(9))]. Low Water (keep, True_semantics): wt=31 given #551 (T,wt=14): 11833 ((x ^ y)' ^ z)' ^ (z ^ x') = c_0. [para(1183(a,1),11803(a,1,2,2))]. given #552 (T,wt=14): 11834 ((x' ^ y)' ^ z)' ^ (z ^ x) = c_0. [para(1186(a,1),11803(a,1,2,2))]. given #553 (T,wt=14): 11839 ((x ^ y')' ^ z)' ^ (z ^ y) = c_0. [para(1303(a,1),11803(a,1,2,2))]. given #554 (T,wt=14): 11840 ((x ^ y)' ^ z)' ^ (z ^ y') = c_0. [para(1293(a,1),11803(a,1,2,2))]. Low Water (keep, True_semantics): wt=30 given #555 (A,wt=17): 1677 x ^ ((y ^ x')' ^ ((x' ^ z) ^ u)') = x. [back_rewrite(1548),rewrite(1630(9))]. given #556 (T,wt=14): 11855 (x ^ (y' ^ z)')' ^ (y ^ x) = c_0. [para(1497(a,1),11803(a,1,2))]. given #557 (T,wt=14): 11856 (x ^ (y ^ z')')' ^ (z ^ x) = c_0. [para(1552(a,1),11803(a,1,2))]. given #558 (T,wt=14): 11868 (x ^ (y ^ z)')' ^ (y' ^ x) = c_0. [para(1498(a,1),11803(a,1,2))]. given #559 (T,wt=14): 11870 (x ^ (y ^ z)')' ^ (z' ^ x) = c_0. [para(1553(a,1),11803(a,1,2))]. given #560 (A,wt=17): 1678 x' ^ ((y ^ x)' ^ ((x ^ z) ^ u)') = x'. [back_rewrite(1547),rewrite(1630(8))]. given #561 (T,wt=14): 11883 (x ^ (y ^ z))' ^ ((z ^ y) ^ x) = c_0. [para(1726(a,1),11803(a,1,2))]. given #562 (T,wt=14): 11914 (x ^ (y ^ z)) ^ ((z ^ x)' ^ u) = c_0. [para(11803(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #563 (T,wt=14): 11915 (x ^ (y ^ z)) ^ (u ^ (y ^ x)') = c_0. [para(11740(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #564 (T,wt=14): 11916 (x ^ (y ^ z)) ^ (u ^ (z ^ x)') = c_0. [para(11803(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #565 (A,wt=21): 1679 x ^ ((y ^ x')' ^ ((x' ^ z)' ^ (x' ^ u)')) = x. [back_rewrite(1542),rewrite(1630(12))]. Low Water (keep, True_semantics): wt=29 given #566 (T,wt=14): 11918 (x ^ (y ^ z)) ^ ((z ^ y) ^ x)' = c_0. [para(1544(a,1),11805(a,1,1,2))]. given #567 (T,wt=14): 11919 (x ^ ((y ^ z) ^ u)) ^ (y ^ x)' = c_0. [para(1379(a,1),11805(a,1,1,2))]. Low Water (keep, True_semantics): wt=28 given #568 (T,wt=14): 11920 (x ^ ((y ^ z) ^ u)) ^ (z ^ x)' = c_0. [para(1401(a,1),11805(a,1,1,2))]. given #569 (T,wt=14): 11926 (x ^ (y ^ (z ^ u))) ^ (z ^ x)' = c_0. [para(1703(a,1),11805(a,1,1,2))]. given #570 (A,wt=20): 1680 x' ^ ((y ^ x)' ^ ((x ^ z)' ^ (x ^ u)')) = x'. [back_rewrite(1539),rewrite(1630(10))]. given #571 (T,wt=14): 11927 (x ^ (y ^ (z ^ u))) ^ (u ^ x)' = c_0. [para(1714(a,1),11805(a,1,1,2))]. given #572 (T,wt=14): 11969 (x ^ y)' ^ ((y ^ (x ^ z)) ^ u) = c_0. [para(11805(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #573 (T,wt=14): 11970 (x ^ y)' ^ (z ^ (y ^ (x ^ u))) = c_0. [para(11805(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #574 (T,wt=14): 12104 (x ^ (y ^ z))' ^ (x ^ (z ^ y)) = c_0. [para(1544(a,1),11807(a,1,2,2))]. given #575 (A,wt=19): 1681 x' ^ ((y ^ (x ^ z))' ^ ((x ^ z) ^ u)') = x'. [back_rewrite(1508),rewrite(1630(9))]. given #576 (T,wt=14): 12105 (x ^ y)' ^ (x ^ ((y ^ z) ^ u)) = c_0. [para(1379(a,1),11807(a,1,2,2))]. given #577 (T,wt=14): 12106 (x ^ y)' ^ (x ^ ((z ^ y) ^ u)) = c_0. [para(1401(a,1),11807(a,1,2,2))]. given #578 (T,wt=14): 12112 (x ^ y)' ^ (x ^ (z ^ (y ^ u))) = c_0. [para(1703(a,1),11807(a,1,2,2))]. given #579 (T,wt=14): 12113 (x ^ y)' ^ (x ^ (z ^ (u ^ y))) = c_0. [para(1714(a,1),11807(a,1,2,2))]. given #580 (A,wt=23): 1682 ((x ^ y) ^ z) ^ (y ^ (u ^ ((x ^ y) ^ z)')') = (x ^ y) ^ z. [back_rewrite(1404),rewrite(1630(8))]. Low Water (keep, True_semantics): wt=27 given #581 (T,wt=14): 12149 (x ^ (y ^ z)) ^ ((x ^ y)' ^ u) = c_0. [para(11807(a,1),11740(a,1,1,1)),rewrite(1463(9))]. Low Water (keep, True_semantics): wt=26 given #582 (T,wt=14): 12150 (x ^ (y ^ z)) ^ (u ^ (x ^ y)') = c_0. [para(11807(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #583 (T,wt=14): 12151 (x ^ y)' ^ ((y ^ (z ^ x)) ^ u) = c_0. [para(11803(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #584 (T,wt=14): 12152 (x ^ y)' ^ ((x ^ (y ^ z)) ^ u) = c_0. [para(11807(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #585 (A,wt=23): 1683 ((x ^ y) ^ z) ^ (x ^ (u ^ ((x ^ y) ^ z)')') = (x ^ y) ^ z. [back_rewrite(1385),rewrite(1630(8))]. given #586 (T,wt=14): 12159 ((x ^ y) ^ z)' ^ ((y ^ x) ^ z) = c_0. [para(1544(a,1),11808(a,1,2,1))]. given #587 (T,wt=14): 12161 (x ^ y)' ^ (((x ^ z) ^ u) ^ y) = c_0. [para(1379(a,1),11808(a,1,2,1))]. given #588 (T,wt=14): 12162 (x ^ y)' ^ (((z ^ x) ^ u) ^ y) = c_0. [para(1401(a,1),11808(a,1,2,1))]. given #589 (T,wt=14): 12168 (x ^ y)' ^ ((z ^ (x ^ u)) ^ y) = c_0. [para(1703(a,1),11808(a,1,2,1))]. given #590 (A,wt=19): 1684 x' ^ (((y ^ x)' ^ (x ^ z)')' ^ u)' = x'. [back_rewrite(1357),rewrite(1630(10))]. given #591 (T,wt=14): 12169 (x ^ y)' ^ ((z ^ (u ^ x)) ^ y) = c_0. [para(1714(a,1),11808(a,1,2,1))]. given #592 (T,wt=14): 12228 ((x ^ y) ^ z) ^ ((x ^ z)' ^ u) = c_0. [para(11808(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #593 (T,wt=14): 12229 ((x ^ y)' ^ z) ^ (y ^ (x ^ u)) = c_0. [para(11740(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #594 (T,wt=14): 12230 ((x ^ y) ^ z) ^ (u ^ (x ^ z)') = c_0. [para(11808(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #595 (A,wt=17): 1685 (x ^ y) ^ (y ^ (z ^ (x ^ y)')') = x ^ y. [back_rewrite(1295),rewrite(1630(6))]. Low Water (keep, True_semantics): wt=25 given #596 (T,wt=14): 12231 ((x ^ y)' ^ z) ^ (y ^ (u ^ x)) = c_0. [para(11803(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #597 (T,wt=14): 12232 (x ^ y)' ^ (((x ^ z) ^ y) ^ u) = c_0. [para(11808(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #598 (T,wt=14): 12233 ((x ^ y)' ^ z) ^ (x ^ (y ^ u)) = c_0. [para(11807(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #599 (T,wt=14): 12234 ((x ^ y)' ^ z) ^ ((x ^ u) ^ y) = c_0. [para(11808(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #600 (A,wt=36): 1686 ((x ^ y)' ^ (x ^ z)')' ^ (x ^ (u ^ ((x ^ y)' ^ (x ^ z)'))') = ((x ^ y)' ^ (x ^ z)')'. [back_rewrite(1256),rewrite(1630(14))]. given #601 (T,wt=14): 12247 (x ^ y) ^ ((x' ^ z)' ^ y)' = c_0. [para(1497(a,1),11816(a,1,2)),rewrite(1630(7))]. given #602 (T,wt=14): 12248 (x ^ y) ^ ((z ^ x')' ^ y)' = c_0. [para(1552(a,1),11816(a,1,2)),rewrite(1630(7))]. given #603 (T,wt=14): 12260 (x' ^ y) ^ ((x ^ z)' ^ y)' = c_0. [para(1498(a,1),11816(a,1,2)),rewrite(1630(7))]. given #604 (T,wt=14): 12262 (x' ^ y) ^ ((z ^ x)' ^ y)' = c_0. [para(1553(a,1),11816(a,1,2)),rewrite(1630(7))]. given #605 (A,wt=36): 1687 ((x ^ y)' ^ (y ^ z)')' ^ (y ^ (u ^ ((x ^ y)' ^ (y ^ z)'))') = ((x ^ y)' ^ (y ^ z)')'. [back_rewrite(1240),rewrite(1630(14))]. given #606 (T,wt=14): 12298 (x ^ (y ^ z)) ^ ((x ^ z)' ^ u) = c_0. [para(11816(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #607 (T,wt=14): 12299 (x ^ (y ^ z)) ^ (u ^ (x ^ z)') = c_0. [para(11816(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #608 (T,wt=14): 12300 (x ^ y)' ^ (z ^ (y ^ (u ^ x))) = c_0. [para(11803(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #609 (T,wt=14): 12302 (x ^ y)' ^ ((x ^ (z ^ y)) ^ u) = c_0. [para(11816(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #610 (A,wt=32): 1690 ((x ^ y) ^ z)' ^ (x ^ (((x ^ y) ^ z)' ^ u)')' = (x ^ (((x ^ y) ^ z)' ^ u)')'. [para(1499(a,1),1194(a,1,2,1,1,1)),rewrite(1137(5),1499(16),1137(13))]. given #611 (T,wt=14): 12303 (x ^ y)' ^ (z ^ (x ^ (y ^ u))) = c_0. [para(11807(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #612 (T,wt=14): 12304 ((x ^ y)' ^ z) ^ (x ^ (u ^ y)) = c_0. [para(11816(a,1),11808(a,1,1,1)),rewrite(1463(9))]. Low Water (keep, True_semantics): wt=24 given #613 (T,wt=14): 12305 (x ^ y)' ^ (z ^ ((x ^ u) ^ y)) = c_0. [para(11808(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #614 (T,wt=14): 12306 (x ^ y)' ^ (z ^ (x ^ (u ^ y))) = c_0. [para(11816(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #615 (A,wt=17): 1691 (x ^ y) ^ (y ^ ((y ^ x)' ^ z)') = y ^ x. [para(1630(a,1),1238(a,1,1))]. given #616 (T,wt=14): 12308 (x ^ (x ^ (y ^ z))') ^ (z ^ y) = c_0. [para(1544(a,1),11828(a,1,2))]. given #617 (T,wt=14): 12309 (x ^ (x ^ y)') ^ ((y ^ z) ^ u) = c_0. [para(1379(a,1),11828(a,1,2))]. given #618 (T,wt=14): 12310 (x ^ (x ^ y)') ^ ((z ^ y) ^ u) = c_0. [para(1401(a,1),11828(a,1,2))]. given #619 (T,wt=14): 12316 (x ^ (x ^ y)') ^ (z ^ (y ^ u)) = c_0. [para(1703(a,1),11828(a,1,2))]. given #620 (A,wt=17): 1692 (x ^ y) ^ (x ^ ((y ^ x)' ^ z)') = x ^ y. [para(1630(a,1),1238(a,1,2,2,1,1,1))]. given #621 (T,wt=14): 12317 (x ^ (x ^ y)') ^ (z ^ (u ^ y)) = c_0. [para(1714(a,1),11828(a,1,2))]. given #622 (T,wt=14): 12355 (x ^ y) ^ ((z ^ (z ^ x)') ^ u) = c_0. [para(11828(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #623 (T,wt=14): 12356 (x ^ y) ^ (z ^ (u ^ (u ^ x)')) = c_0. [para(11828(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #624 (T,wt=14): 12357 ((x ^ (x ^ y)') ^ z) ^ (y ^ u) = c_0. [para(11828(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #625 (A,wt=27): 1693 ((x ^ y)' ^ (y ^ z)')' ^ (y' ^ u)' = ((x ^ y)' ^ (y ^ z)')'. [para(1207(a,1),1573(a,1,2,1,1))]. given #626 (T,wt=14): 12525 (x ^ y) ^ (z ^ ((y ^ x) ^ z)') = c_0. [para(1544(a,1),11829(a,1,2)),rewrite(1630(6))]. given #627 (T,wt=14): 12526 (x ^ (y ^ x)') ^ ((y ^ z) ^ u) = c_0. [para(1379(a,1),11829(a,1,2))]. given #628 (T,wt=14): 12527 (x ^ (y ^ x)') ^ ((z ^ y) ^ u) = c_0. [para(1401(a,1),11829(a,1,2))]. given #629 (T,wt=14): 12533 (x ^ (y ^ x)') ^ (z ^ (y ^ u)) = c_0. [para(1703(a,1),11829(a,1,2))]. given #630 (A,wt=30): 1694 ((x ^ y')' ^ (y' ^ z)')' ^ (y ^ u)' = ((x ^ y')' ^ (y' ^ z)')'. [para(1236(a,1),1573(a,1,2,1,1))]. given #631 (T,wt=14): 12534 (x ^ (y ^ x)') ^ (z ^ (u ^ y)) = c_0. [para(1714(a,1),11829(a,1,2))]. given #632 (T,wt=14): 12572 (x ^ y) ^ ((z ^ (x ^ z)') ^ u) = c_0. [para(11829(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #633 (T,wt=14): 12573 (x ^ y) ^ (z ^ (u ^ (x ^ u)')) = c_0. [para(11829(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #634 (T,wt=14): 12574 ((x ^ (y ^ x)') ^ z) ^ (y ^ u) = c_0. [para(11829(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #635 (A,wt=27): 1695 ((x ^ y)' ^ (x ^ z)')' ^ (x' ^ u)' = ((x ^ y)' ^ (x ^ z)')'. [para(1241(a,1),1573(a,1,2,1,1))]. given #636 (T,wt=14): 12575 (x ^ y') ^ ((y ^ z)' ^ x)' = c_0. [para(1183(a,1),11844(a,1,1,2))]. given #637 (T,wt=14): 12576 (x ^ y) ^ ((y' ^ z)' ^ x)' = c_0. [para(1186(a,1),11844(a,1,1,2))]. given #638 (T,wt=14): 12581 (x ^ y) ^ ((z ^ y')' ^ x)' = c_0. [para(1303(a,1),11844(a,1,1,2))]. given #639 (T,wt=14): 12582 (x ^ y') ^ ((z ^ y)' ^ x)' = c_0. [para(1293(a,1),11844(a,1,1,2))]. given #640 (A,wt=30): 1696 ((x' ^ y)' ^ (x' ^ z)')' ^ (x ^ u)' = ((x' ^ y)' ^ (x' ^ z)')'. [para(1261(a,1),1573(a,1,2,1,1))]. given #641 (T,wt=14): 12595 (x ^ y) ^ (y ^ (x' ^ z)')' = c_0. [para(1497(a,1),11844(a,1,1))]. given #642 (T,wt=14): 12596 (x ^ y) ^ (y ^ (z ^ x')')' = c_0. [para(1552(a,1),11844(a,1,1))]. given #643 (T,wt=14): 12608 (x' ^ y) ^ (y ^ (x ^ z)')' = c_0. [para(1498(a,1),11844(a,1,1))]. given #644 (T,wt=14): 12610 (x' ^ y) ^ (y ^ (z ^ x)')' = c_0. [para(1553(a,1),11844(a,1,1))]. given #645 (A,wt=32): 1697 ((x ^ y) ^ z)' ^ (y ^ (((x ^ y) ^ z)' ^ u)')' = (y ^ (((x ^ y) ^ z)' ^ u)')'. [para(1573(a,1),1194(a,1,2,1,1,1)),rewrite(1137(5),1573(16),1137(13))]. given #646 (T,wt=14): 12623 ((x ^ y) ^ z) ^ (z ^ (y ^ x))' = c_0. [para(1726(a,1),11844(a,1,1))]. given #647 (T,wt=14): 12734 ((x ^ y) ^ z) ^ ((y ^ z)' ^ u) = c_0. [para(11845(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #648 (T,wt=14): 12735 (x ^ (y ^ z)') ^ (z ^ (y ^ u)) = c_0. [para(11740(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #649 (T,wt=14): 12736 ((x ^ y) ^ z) ^ (u ^ (y ^ z)') = c_0. [para(11845(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #650 (A,wt=19): 1698 x' ^ ((y ^ (z ^ x))' ^ ((z ^ x) ^ u)') = x'. [para(1194(a,1),1573(a,1,2,1)),rewrite(1137(10))]. given #651 (T,wt=14): 12737 (x ^ (y ^ z)') ^ (z ^ (u ^ y)) = c_0. [para(11803(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #652 (T,wt=14): 12738 (x ^ (y ^ (z ^ u))) ^ (z ^ y)' = c_0. [para(11805(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #653 (T,wt=14): 12741 (x ^ y)' ^ (((z ^ x) ^ y) ^ u) = c_0. [para(11845(a,1),11807(a,1,1,1)),rewrite(1463(9))]. Low Water (keep, True_semantics): wt=23 given #654 (T,wt=14): 12742 (x ^ (y ^ z)') ^ (y ^ (z ^ u)) = c_0. [para(11807(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #655 (A,wt=17): 1699 ((x ^ y) ^ z) ^ (y' ^ u)' = (x ^ y) ^ z. [para(1573(a,1),1519(a,1,2,1,1))]. given #656 (T,wt=14): 12743 ((x ^ y)' ^ z) ^ ((u ^ x) ^ y) = c_0. [para(11845(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #657 (T,wt=14): 12744 (x ^ (y ^ z)') ^ ((y ^ u) ^ z) = c_0. [para(11808(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #658 (T,wt=14): 12745 (x ^ y)' ^ (z ^ ((u ^ x) ^ y)) = c_0. [para(11845(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #659 (T,wt=14): 12746 (x ^ (y ^ z)') ^ (y ^ (u ^ z)) = c_0. [para(11816(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #660 (A,wt=17): 1700 ((x ^ y) ^ z) ^ (u ^ y')' = (x ^ y) ^ z. [para(1573(a,1),1574(a,1,2,1,2))]. given #661 (T,wt=14): 12747 (x ^ (y ^ (y ^ z)')) ^ (z ^ u) = c_0. [para(11828(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #662 (T,wt=14): 12750 (x ^ (y ^ (z ^ y)')) ^ (z ^ u) = c_0. [para(11829(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #663 (T,wt=14): 12751 (x ^ (y ^ (z ^ u))) ^ (u ^ y)' = c_0. [para(11844(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #664 (T,wt=14): 12752 (x ^ (y ^ z)') ^ ((u ^ y) ^ z) = c_0. [para(11845(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #665 (A,wt=28): 1701 (x ^ ((x ^ y)' ^ z)')' ^ ((x ^ y) ^ u)' = (x ^ ((x ^ y)' ^ z)')'. [para(1238(a,1),1573(a,1,2,1,1))]. given #666 (T,wt=14): 12753 (x ^ y)' ^ (((y ^ z) ^ u) ^ x) = c_0. [para(1379(a,1),11852(a,1,2,1))]. given #667 (T,wt=14): 12754 (x ^ y)' ^ (((z ^ y) ^ u) ^ x) = c_0. [para(1401(a,1),11852(a,1,2,1))]. given #668 (T,wt=14): 12758 (x ^ y)' ^ ((z ^ (y ^ u)) ^ x) = c_0. [para(1703(a,1),11852(a,1,2,1))]. given #669 (T,wt=14): 12759 (x ^ y)' ^ ((z ^ (u ^ y)) ^ x) = c_0. [para(1714(a,1),11852(a,1,2,1))]. given #670 (A,wt=23): 1702 (x ^ (y ^ z)) ^ (y ^ ((x ^ (y ^ z))' ^ u)') = x ^ (y ^ z). [para(1578(a,1),1207(a,1,2,1,1)),rewrite(1137(4),1137(4),1137(13))]. given #671 (T,wt=14): 12793 ((x ^ y) ^ z) ^ ((z ^ x)' ^ u) = c_0. [para(11852(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #672 (T,wt=14): 12794 ((x ^ y) ^ z) ^ (u ^ (z ^ x)') = c_0. [para(11852(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #673 (T,wt=14): 12795 (x ^ y)' ^ (((y ^ z) ^ x) ^ u) = c_0. [para(11852(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #674 (T,wt=14): 12796 ((x ^ y)' ^ z) ^ ((y ^ u) ^ x) = c_0. [para(11852(a,1),11808(a,1,1,1)),rewrite(1463(9))]. Low Water (keep, True_semantics): wt=22 given #675 (A,wt=32): 1704 (x ^ (y ^ z))' ^ (y ^ ((x ^ (y ^ z))' ^ u)')' = (y ^ ((x ^ (y ^ z))' ^ u)')'. [para(1578(a,1),1194(a,1,2,1,1,1)),rewrite(1137(5),1578(16),1137(13))]. given #676 (T,wt=14): 12797 (x ^ y)' ^ (z ^ ((y ^ u) ^ x)) = c_0. [para(11852(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #677 (T,wt=14): 12798 ((x ^ y) ^ z) ^ (u ^ (u ^ x)') = c_0. [para(11828(a,1),11852(a,1,1,1)),rewrite(1463(9))]. given #678 (T,wt=14): 12799 ((x ^ y) ^ z) ^ (u ^ (x ^ u)') = c_0. [para(11829(a,1),11852(a,1,1,1)),rewrite(1463(9))]. given #679 (T,wt=14): 12800 (x ^ (y ^ z)') ^ ((z ^ u) ^ y) = c_0. [para(11852(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #680 (A,wt=19): 1705 x' ^ (y ^ ((z ^ x)' ^ (x ^ u)')')' = x'. [para(1194(a,1),1578(a,1,2,1,2))]. given #681 (T,wt=14): 13017 ((x ^ y) ^ z) ^ ((z ^ y)' ^ u) = c_0. [para(11854(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #682 (T,wt=14): 13018 ((x ^ y) ^ z) ^ (u ^ (z ^ y)') = c_0. [para(11854(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #683 (T,wt=14): 13020 (x ^ y)' ^ (((z ^ y) ^ x) ^ u) = c_0. [para(11854(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #684 (T,wt=14): 13021 ((x ^ y)' ^ z) ^ ((u ^ y) ^ x) = c_0. [para(11854(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #685 (A,wt=17): 1706 (x ^ (y ^ z)) ^ (y' ^ u)' = x ^ (y ^ z). [para(1578(a,1),1519(a,1,2,1,1))]. given #686 (T,wt=14): 13022 (x ^ y)' ^ (z ^ ((u ^ y) ^ x)) = c_0. [para(11854(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #687 (T,wt=14): 13023 (x ^ (y ^ z)) ^ (u ^ (u ^ y)') = c_0. [para(11828(a,1),11854(a,1,1,1)),rewrite(1463(9))]. given #688 (T,wt=14): 13025 (x ^ (y ^ z)) ^ (u ^ (y ^ u)') = c_0. [para(11829(a,1),11854(a,1,1,1)),rewrite(1463(9))]. given #689 (T,wt=14): 13026 (x ^ (y ^ z)') ^ ((u ^ z) ^ y) = c_0. [para(11854(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #690 (A,wt=16): 1707 (x ^ y)' ^ (z ^ (y ^ x))' = (x ^ y)'. [para(1544(a,1),1578(a,1,2,1,2))]. given #691 (T,wt=14): 13027 (x ^ ((y ^ z) ^ u)) ^ (u ^ y)' = c_0. [para(11852(a,1),11854(a,1,1,1)),rewrite(1463(9))]. given #692 (T,wt=14): 13029 (x ^ ((y ^ z) ^ u)) ^ (u ^ z)' = c_0. [para(11854(a,1),11854(a,1,1,1)),rewrite(1463(9))]. given #693 (T,wt=14): 13030 x' ^ (y ^ (y ^ (x ^ z)')') = c_0. [para(1183(a,1),11903(a,1,2)),rewrite(1630(7))]. given #694 (T,wt=14): 13031 x ^ (y ^ (y ^ (x' ^ z)')') = c_0. [para(1186(a,1),11903(a,1,2)),rewrite(1630(7))]. given #695 (A,wt=17): 1708 (x ^ (y ^ z)) ^ (u ^ y')' = x ^ (y ^ z). [para(1578(a,1),1574(a,1,2,1,2))]. given #696 (T,wt=14): 13036 x ^ (y ^ (y ^ (z ^ x')')') = c_0. [para(1303(a,1),11903(a,1,2)),rewrite(1630(7))]. given #697 (T,wt=14): 13037 x' ^ (y ^ (y ^ (z ^ x)')') = c_0. [para(1293(a,1),11903(a,1,2)),rewrite(1630(7))]. given #698 (T,wt=14): 13090 (x ^ y) ^ ((z ^ (z ^ y)') ^ u) = c_0. [para(11903(a,1),11740(a,1,1,1)),rewrite(1463(9))]. Low Water (displace, True_semantics): id=12939, wt=37 Low Water (displace, True_semantics): id=12832, wt=36 Low Water (displace, True_semantics): id=13733, wt=35 given #699 (T,wt=14): 13091 (x ^ y) ^ (z ^ (u ^ (u ^ y)')) = c_0. [para(11903(a,1),11803(a,1,1,1)),rewrite(1463(9))]. Low Water (displace, True_semantics): id=13755, wt=34 Low Water (displace, True_semantics): id=14399, wt=33 Low Water (displace, True_semantics): id=14786, wt=32 Low Water (displace, True_semantics): id=15297, wt=31 given #700 (A,wt=23): 1709 (x ^ (y ^ z)) ^ (z ^ ((x ^ (y ^ z))' ^ u)') = x ^ (y ^ z). [para(1672(a,1),1207(a,1,2,1,1)),rewrite(1137(4),1137(4),1137(13))]. given #701 (T,wt=14): 13093 ((x ^ (x ^ y)') ^ z) ^ (u ^ y) = c_0. [para(11903(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #702 (T,wt=14): 13095 (x ^ (y ^ (y ^ z)')) ^ (u ^ z) = c_0. [para(11903(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #703 (T,wt=14): 13096 ((x ^ y) ^ z) ^ (u ^ (u ^ y)') = c_0. [para(11903(a,1),11852(a,1,1,1)),rewrite(1463(9))]. given #704 (T,wt=14): 13098 (x ^ (y ^ z)) ^ (u ^ (u ^ z)') = c_0. [para(11903(a,1),11854(a,1,1,1)),rewrite(1463(9))]. Low Water (displace, True_semantics): id=15569, wt=30 given #705 (A,wt=27): 1710 ((x ^ y)' ^ (y ^ z)')' ^ (u ^ y')' = ((x ^ y)' ^ (y ^ z)')'. [para(1207(a,1),1672(a,1,2,1,2))]. given #706 (T,wt=14): 13099 x' ^ (y ^ ((x ^ z)' ^ y)') = c_0. [para(1183(a,1),11904(a,1,2)),rewrite(1630(7))]. given #707 (T,wt=14): 13100 x ^ (y ^ ((x' ^ z)' ^ y)') = c_0. [para(1186(a,1),11904(a,1,2)),rewrite(1630(7))]. given #708 (T,wt=14): 13105 x ^ (y ^ ((z ^ x')' ^ y)') = c_0. [para(1303(a,1),11904(a,1,2)),rewrite(1630(7))]. given #709 (T,wt=14): 13106 x' ^ (y ^ ((z ^ x)' ^ y)') = c_0. [para(1293(a,1),11904(a,1,2)),rewrite(1630(7))]. given #710 (A,wt=30): 1711 ((x ^ y')' ^ (y' ^ z)')' ^ (u ^ y)' = ((x ^ y')' ^ (y' ^ z)')'. [para(1236(a,1),1672(a,1,2,1,2))]. given #711 (T,wt=14): 13159 (x ^ y) ^ ((z ^ (y ^ z)') ^ u) = c_0. [para(11904(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #712 (T,wt=14): 13160 (x ^ y) ^ (z ^ (u ^ (y ^ u)')) = c_0. [para(11904(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #713 (T,wt=14): 13162 ((x ^ (y ^ x)') ^ z) ^ (u ^ y) = c_0. [para(11904(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #714 (T,wt=14): 13164 (x ^ (y ^ (z ^ y)')) ^ (u ^ z) = c_0. [para(11904(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #715 (A,wt=27): 1712 ((x ^ y)' ^ (x ^ z)')' ^ (u ^ x')' = ((x ^ y)' ^ (x ^ z)')'. [para(1241(a,1),1672(a,1,2,1,2))]. given #716 (T,wt=14): 13165 ((x ^ y) ^ z) ^ (u ^ (y ^ u)') = c_0. [para(11904(a,1),11852(a,1,1,1)),rewrite(1463(9))]. Low Water (displace, True_semantics): id=16308, wt=29 given #717 (T,wt=14): 13167 (x ^ (y ^ z)) ^ (u ^ (z ^ u)') = c_0. [para(11904(a,1),11854(a,1,1,1)),rewrite(1463(9))]. given #718 (T,wt=14): 13168 x ^ (((y ^ (y ^ x)') ^ z) ^ u) = c_0. [para(1379(a,1),12140(a,1,2))]. given #719 (T,wt=14): 13169 x ^ ((y ^ (z ^ (z ^ x)')) ^ u) = c_0. [para(1401(a,1),12140(a,1,2))]. given #720 (A,wt=30): 1713 ((x' ^ y)' ^ (x' ^ z)')' ^ (u ^ x)' = ((x' ^ y)' ^ (x' ^ z)')'. [para(1261(a,1),1672(a,1,2,1,2))]. given #721 (T,wt=14): 13171 x ^ (y ^ ((z ^ (z ^ x)') ^ u)) = c_0. [para(1703(a,1),12140(a,1,2))]. given #722 (T,wt=14): 13172 x ^ (y ^ (z ^ (u ^ (u ^ x)'))) = c_0. [para(1714(a,1),12140(a,1,2))]. given #723 (T,wt=14): 13301 x ^ (((y ^ (x ^ y)') ^ z) ^ u) = c_0. [para(1379(a,1),12141(a,1,2))]. Low Water (displace, True_semantics): id=16759, wt=28 given #724 (T,wt=14): 13302 x ^ ((y ^ (z ^ (x ^ z)')) ^ u) = c_0. [para(1401(a,1),12141(a,1,2))]. given #725 (A,wt=32): 1715 (x ^ (y ^ z))' ^ (z ^ ((x ^ (y ^ z))' ^ u)')' = (z ^ ((x ^ (y ^ z))' ^ u)')'. [para(1672(a,1),1194(a,1,2,1,1,1)),rewrite(1137(5),1672(16),1137(13))]. given #726 (T,wt=14): 13304 x ^ (y ^ ((z ^ (x ^ z)') ^ u)) = c_0. [para(1703(a,1),12141(a,1,2))]. given #727 (T,wt=14): 13305 x ^ (y ^ (z ^ (u ^ (x ^ u)'))) = c_0. [para(1714(a,1),12141(a,1,2))]. given #728 (T,wt=14): 13311 (x ^ y) ^ (z ^ (z ^ (y ^ x))') = c_0. [para(1544(a,1),12217(a,1,1))]. given #729 (T,wt=14): 13562 (((x ^ y) ^ z) ^ u) ^ (u ^ x)' = c_0. [para(1379(a,1),12592(a,1,1,1))]. given #730 (A,wt=17): 1716 (x ^ (y ^ z)) ^ (z' ^ u)' = x ^ (y ^ z). [para(1672(a,1),1519(a,1,2,1,1))]. given #731 (T,wt=14): 13563 (((x ^ y) ^ z) ^ u) ^ (u ^ y)' = c_0. [para(1401(a,1),12592(a,1,1,1))]. Low Water (keep, True_semantics): wt=21 given #732 (T,wt=14): 13567 ((x ^ (y ^ z)) ^ u) ^ (u ^ y)' = c_0. [para(1703(a,1),12592(a,1,1,1))]. given #733 (T,wt=14): 13568 ((x ^ (y ^ z)) ^ u) ^ (u ^ z)' = c_0. [para(1714(a,1),12592(a,1,1,1))]. given #734 (T,wt=14): 13835 x ^ (y ^ ((y' ^ z)' ^ x)') = c_0. [para(1506(a,1),8012(a,1,2)),rewrite(1630(6))]. Low Water (displace, True_semantics): id=17281, wt=27 given #735 (A,wt=17): 1717 (x ^ (y ^ z)) ^ (u ^ z')' = x ^ (y ^ z). [para(1672(a,1),1574(a,1,2,1,2))]. Low Water (displace, True_semantics): id=17927, wt=26 given #736 (T,wt=14): 13837 x ^ (y ^ ((z ^ y')' ^ x)') = c_0. [para(1562(a,1),8012(a,1,2)),rewrite(1630(6))]. given #737 (T,wt=14): 13842 x ^ (y' ^ ((y ^ z)' ^ x)') = c_0. [para(1505(a,1),8012(a,1,2)),rewrite(1630(6))]. given #738 (T,wt=14): 13843 x ^ (y' ^ ((z ^ y)' ^ x)') = c_0. [para(1561(a,1),8012(a,1,2)),rewrite(1630(6))]. given #739 (T,wt=14): 13869 x ^ (y ^ (((y ^ x)' ^ z) ^ u)) = c_0. [para(1379(a,1),13831(a,1,2,2))]. given #740 (A,wt=28): 1718 (x ^ ((x ^ y)' ^ z)')' ^ (u ^ (x ^ y))' = (x ^ ((x ^ y)' ^ z)')'. [para(1238(a,1),1672(a,1,2,1,2))]. given #741 (T,wt=14): 13870 x ^ (y ^ ((z ^ (y ^ x)') ^ u)) = c_0. [para(1401(a,1),13831(a,1,2,2))]. given #742 (T,wt=14): 13872 x ^ (y ^ (z ^ ((y ^ x)' ^ u))) = c_0. [para(1703(a,1),13831(a,1,2,2))]. given #743 (T,wt=14): 13874 x ^ (y ^ (z ^ (u ^ (y ^ x)'))) = c_0. [para(1714(a,1),13831(a,1,2,2))]. given #744 (T,wt=14): 13882 x ^ (y' ^ (x ^ (y ^ z)')') = c_0. [para(13831(a,1),1602(a,1)),rewrite(1630(7)),flip(a)]. given #745 (A,wt=17): 1719 x' ^ ((x ^ y)' ^ ((x ^ z) ^ u)') = x'. [para(1379(a,1),1241(a,1,2,2,1))]. given #746 (T,wt=14): 13883 x ^ (y' ^ (x ^ (z ^ y)')') = c_0. [para(13831(a,1),1605(a,1)),rewrite(1630(7)),flip(a)]. given #747 (T,wt=14): 13887 (x ^ ((x ^ y)' ^ z)) ^ (y ^ u) = c_0. [para(13831(a,1),11740(a,1,1,1)),rewrite(1463(9))]. Low Water (displace, True_semantics): id=18913, wt=25 given #748 (T,wt=14): 13888 (x ^ ((x ^ y)' ^ z)) ^ (u ^ y) = c_0. [para(13831(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #749 (T,wt=14): 13889 x ^ ((y ^ ((y ^ x)' ^ z)) ^ u) = c_0. [para(13831(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #750 (A,wt=17): 1720 x ^ ((x' ^ y)' ^ ((x' ^ z) ^ u)') = x. [para(1379(a,1),1261(a,1,2,2,1))]. given #751 (T,wt=14): 13890 (x ^ y) ^ (z ^ ((z ^ x)' ^ u)) = c_0. [para(13831(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #752 (T,wt=14): 13891 x ^ (y ^ (z ^ ((z ^ x)' ^ u))) = c_0. [para(13831(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #753 (T,wt=14): 13892 (x ^ y) ^ (z ^ ((z ^ y)' ^ u)) = c_0. [para(13831(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #754 (T,wt=14): 13897 x ^ ((y ^ z) ^ ((z ^ y) ^ x)') = c_0. [para(1726(a,1),13866(a,1,2))]. given #755 (A,wt=27): 1721 x ^ ((y ^ x)' ^ ((x ^ z) ^ u)')' = ((y ^ x)' ^ ((x ^ z) ^ u)')'. [para(1379(a,1),1194(a,1,2,1,2,1)),rewrite(1379(13))]. given #756 (T,wt=14): 13906 (x ^ (y ^ (x ^ z)')) ^ (z ^ u) = c_0. [para(13866(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #757 (T,wt=14): 13907 (x ^ (y ^ (x ^ z)')) ^ (u ^ z) = c_0. [para(13866(a,1),11803(a,1,1,1)),rewrite(1463(9))]. Low Water (displace, True_semantics): id=19683, wt=24 given #758 (T,wt=14): 13908 x ^ ((y ^ (z ^ (y ^ x)')) ^ u) = c_0. [para(13866(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #759 (T,wt=14): 13909 (x ^ y) ^ (z ^ (u ^ (z ^ x)')) = c_0. [para(13866(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #760 (A,wt=31): 1722 x ^ ((y ^ (x ^ z))' ^ ((x ^ z) ^ u)')' = ((y ^ (x ^ z))' ^ ((x ^ z) ^ u)')'. [para(1194(a,1),1379(a,1,2)),rewrite(1194(19))]. given #761 (T,wt=14): 13910 x ^ (y ^ (z ^ (u ^ (z ^ x)'))) = c_0. [para(13866(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #762 (T,wt=14): 13911 (x ^ y) ^ (z ^ (u ^ (z ^ y)')) = c_0. [para(13866(a,1),11845(a,1,1,1)),rewrite(1463(9))]. Low Water (keep, True_semantics): wt=20 given #763 (T,wt=14): 14032 x ^ (y ^ (((x ^ y)' ^ z) ^ u)) = c_0. [para(1379(a,1),13868(a,1,2,2))]. given #764 (T,wt=14): 14033 x ^ (y ^ ((z ^ (x ^ y)') ^ u)) = c_0. [para(1401(a,1),13868(a,1,2,2))]. given #765 (A,wt=19): 1728 (x ^ y) ^ (x ^ (((x ^ y)' ^ z) ^ u)') = x ^ y. [para(1379(a,1),1238(a,1,2,2,1))]. given #766 (T,wt=14): 14034 x ^ (y ^ (x ^ (y' ^ z)')') = c_0. [para(1506(a,1),13868(a,1,2)),rewrite(1630(6))]. given #767 (T,wt=14): 14036 x ^ (y ^ (x ^ (z ^ y')')') = c_0. [para(1562(a,1),13868(a,1,2)),rewrite(1630(6))]. given #768 (T,wt=14): 14037 x ^ (y ^ (z ^ ((x ^ y)' ^ u))) = c_0. [para(1703(a,1),13868(a,1,2,2))]. given #769 (T,wt=14): 14039 x ^ (y ^ (z ^ (u ^ (x ^ y)'))) = c_0. [para(1714(a,1),13868(a,1,2,2))]. given #770 (A,wt=17): 1731 x ^ (((x ^ y) ^ z) ^ u) = ((x ^ y) ^ z) ^ u. [para(1379(a,1),1379(a,1,2,1)),rewrite(1379(7))]. given #771 (T,wt=14): 14056 (x ^ ((y ^ x)' ^ z)) ^ (y ^ u) = c_0. [para(13868(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #772 (T,wt=14): 14057 (x ^ ((y ^ x)' ^ z)) ^ (u ^ y) = c_0. [para(13868(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #773 (T,wt=14): 14058 x ^ ((y ^ ((x ^ y)' ^ z)) ^ u) = c_0. [para(13868(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #774 (T,wt=14): 14059 (x ^ y) ^ (z ^ ((x ^ z)' ^ u)) = c_0. [para(13868(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #775 (A,wt=36): 1733 ((x ^ y)' ^ (z ^ y)')' ^ (y ^ (((x ^ y)' ^ (z ^ y)') ^ u)') = ((x ^ y)' ^ (z ^ y)')'. [para(1289(a,1),1247(a,1,1,1,2,1)),rewrite(1289(10),1289(19))]. given #776 (T,wt=14): 14060 x ^ (y ^ (z ^ ((x ^ z)' ^ u))) = c_0. [para(13868(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #777 (T,wt=14): 14061 (x ^ y) ^ (z ^ ((y ^ z)' ^ u)) = c_0. [para(13868(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #778 (T,wt=14): 14063 x ^ ((y ^ x)' ^ ((y ^ z) ^ u)) = c_0. [para(1379(a,1),13873(a,1,2,2))]. given #779 (T,wt=14): 14064 x ^ ((y ^ x)' ^ ((z ^ y) ^ u)) = c_0. [para(1401(a,1),13873(a,1,2,2))]. given #780 (A,wt=39): 1734 (x ^ ((y ^ x)' ^ z)')' ^ ((y ^ x)' ^ ((x ^ ((y ^ x)' ^ z)') ^ u)') = (x ^ ((y ^ x)' ^ z)')'. [para(1293(a,1),1247(a,1,1,1,1,1)),rewrite(1137(2),1293(12),1137(10),1293(21),1137(19))]. given #781 (T,wt=14): 14070 x ^ ((y ^ x)' ^ (z ^ (y ^ u))) = c_0. [para(1703(a,1),13873(a,1,2,2))]. given #782 (T,wt=14): 14071 x ^ ((y ^ x)' ^ (z ^ (u ^ y))) = c_0. [para(1714(a,1),13873(a,1,2,2))]. given #783 (T,wt=14): 14105 ((x ^ y)' ^ (x ^ z)) ^ (y ^ u) = c_0. [para(13873(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #784 (T,wt=14): 14106 ((x ^ y)' ^ (x ^ z)) ^ (u ^ y) = c_0. [para(13873(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #785 (A,wt=36): 1736 ((x ^ y)' ^ (x ^ z)')' ^ (x ^ (((y ^ x)' ^ (x ^ z)') ^ u)') = ((y ^ x)' ^ (x ^ z)')'. [para(1630(a,1),1247(a,1,1,1,1,1))]. given #786 (T,wt=14): 14107 x ^ (((y ^ x)' ^ (y ^ z)) ^ u) = c_0. [para(13873(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #787 (T,wt=14): 14108 (x ^ y) ^ ((z ^ x)' ^ (z ^ u)) = c_0. [para(13873(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #788 (T,wt=14): 14109 x ^ (y ^ ((z ^ x)' ^ (z ^ u))) = c_0. [para(13873(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #789 (T,wt=14): 14110 (x ^ y) ^ ((z ^ y)' ^ (z ^ u)) = c_0. [para(13873(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #790 (A,wt=36): 1737 ((x ^ y)' ^ (z ^ y)')' ^ (y ^ (((x ^ y)' ^ (y ^ z)') ^ u)') = ((x ^ y)' ^ (y ^ z)')'. [para(1630(a,1),1247(a,1,1,1,2,1))]. given #791 (T,wt=14): 14159 ((x ^ y)' ^ (z ^ x)) ^ (y ^ u) = c_0. [para(13875(a,1),11740(a,1,1,1)),rewrite(1463(9))]. Low Water (displace, True_semantics): id=21113, wt=23 given #792 (T,wt=14): 14160 ((x ^ y)' ^ (z ^ x)) ^ (u ^ y) = c_0. [para(13875(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #793 (T,wt=14): 14162 x ^ (((y ^ x)' ^ (z ^ y)) ^ u) = c_0. [para(13875(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #794 (T,wt=14): 14163 (x ^ y) ^ ((z ^ x)' ^ (u ^ z)) = c_0. [para(13875(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #795 (A,wt=36): 1738 ((x ^ y)' ^ (z ^ x)')' ^ (x ^ (((z ^ x)' ^ (x ^ y)') ^ u)') = ((z ^ x)' ^ (x ^ y)')'. [para(1630(a,1),1247(a,1,1,1))]. given #796 (T,wt=14): 14164 x ^ (y ^ ((z ^ x)' ^ (u ^ z))) = c_0. [para(13875(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #797 (T,wt=14): 14166 (x ^ y) ^ ((z ^ y)' ^ (u ^ z)) = c_0. [para(13875(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #798 (T,wt=14): 14175 x ^ ((y ^ z) ^ (x ^ (z ^ y))') = c_0. [para(1726(a,1),13893(a,1,2))]. given #799 (T,wt=14): 14184 (x ^ (y ^ (z ^ x)')) ^ (z ^ u) = c_0. [para(13893(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #800 (A,wt=36): 1739 ((x ^ y)' ^ (y ^ z)')' ^ (y ^ (((y ^ x)' ^ (y ^ z)') ^ u)') = ((x ^ y)' ^ (y ^ z)')'. [para(1630(a,1),1247(a,1,2,2,1,1,1,1))]. given #801 (T,wt=14): 14185 (x ^ (y ^ (z ^ x)')) ^ (u ^ z) = c_0. [para(13893(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #802 (T,wt=14): 14186 x ^ ((y ^ (z ^ (x ^ y)')) ^ u) = c_0. [para(13893(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #803 (T,wt=14): 14187 (x ^ y) ^ (z ^ (u ^ (x ^ z)')) = c_0. [para(13893(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #804 (T,wt=14): 14188 x ^ (y ^ (z ^ (u ^ (x ^ z)'))) = c_0. [para(13893(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #805 (A,wt=36): 1740 ((x ^ y)' ^ (y ^ z)')' ^ (y ^ (((x ^ y)' ^ (z ^ y)') ^ u)') = ((x ^ y)' ^ (y ^ z)')'. [para(1630(a,1),1247(a,1,2,2,1,1,2,1))]. given #806 (T,wt=14): 14189 (x ^ y) ^ (z ^ (u ^ (y ^ z)')) = c_0. [para(13893(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #807 (T,wt=14): 14198 x ^ (((y ^ z) ^ u) ^ (y ^ x)') = c_0. [para(1379(a,1),13894(a,1,2,1))]. given #808 (T,wt=14): 14199 x ^ (((y ^ z) ^ u) ^ (z ^ x)') = c_0. [para(1401(a,1),13894(a,1,2,1))]. given #809 (T,wt=14): 14203 x ^ ((y ^ (z ^ u)) ^ (z ^ x)') = c_0. [para(1703(a,1),13894(a,1,2,1))]. given #810 (A,wt=36): 1741 ((x ^ y)' ^ (y ^ z)')' ^ (y ^ (((y ^ z)' ^ (x ^ y)') ^ u)') = ((x ^ y)' ^ (y ^ z)')'. [para(1630(a,1),1247(a,1,2,2,1,1))]. given #811 (T,wt=14): 14204 x ^ ((y ^ (z ^ u)) ^ (u ^ x)') = c_0. [para(1714(a,1),13894(a,1,2,1))]. given #812 (T,wt=14): 14237 ((x ^ y) ^ (x ^ z)') ^ (z ^ u) = c_0. [para(13894(a,1),11740(a,1,1,1)),rewrite(1463(9))]. Low Water (displace, True_semantics): id=21959, wt=22 given #813 (T,wt=14): 14238 ((x ^ y) ^ (x ^ z)') ^ (u ^ z) = c_0. [para(13894(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #814 (T,wt=14): 14239 x ^ (((y ^ z) ^ (y ^ x)') ^ u) = c_0. [para(13894(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #815 (A,wt=38): 1742 ((x ^ y)' ^ (y ^ z)')' ^ (y ^ ((((x ^ y)' ^ (y ^ z)') ^ u) ^ v)') = ((x ^ y)' ^ (y ^ z)')'. [para(1379(a,1),1247(a,1,2,2,1))]. given #816 (T,wt=14): 14240 (x ^ y) ^ ((z ^ u) ^ (z ^ x)') = c_0. [para(13894(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #817 (T,wt=14): 14241 x ^ (y ^ ((z ^ u) ^ (z ^ x)')) = c_0. [para(13894(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #818 (T,wt=14): 14242 (x ^ y) ^ ((z ^ u) ^ (z ^ y)') = c_0. [para(13894(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #819 (T,wt=14): 14243 ((x ^ y) ^ (y ^ z)') ^ (z ^ u) = c_0. [para(13895(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #820 (A,wt=17): 1743 x' ^ ((y ^ x)' ^ ((z ^ x) ^ u)') = x'. [para(1401(a,1),1207(a,1,2,2,1))]. given #821 (T,wt=14): 14244 ((x ^ y) ^ (y ^ z)') ^ (u ^ z) = c_0. [para(13895(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #822 (T,wt=14): 14245 x ^ (((y ^ z) ^ (z ^ x)') ^ u) = c_0. [para(13895(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #823 (T,wt=14): 14246 (x ^ y) ^ ((z ^ u) ^ (u ^ x)') = c_0. [para(13895(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #824 (T,wt=14): 14247 x ^ (y ^ ((z ^ u) ^ (u ^ x)')) = c_0. [para(13895(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #825 (A,wt=19): 1744 ((x ^ y)' ^ (y ^ z)') ^ (y' ^ u) = y' ^ u. [para(1207(a,1),1401(a,1,2,1)),rewrite(1207(15))]. given #826 (T,wt=14): 14248 (x ^ y) ^ ((z ^ u) ^ (u ^ y)') = c_0. [para(13895(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #827 (T,wt=14): 14250 x ^ ((x ^ (y ^ z))' ^ (z ^ y)) = c_0. [para(1544(a,1),14038(a,1,2,2))]. given #828 (T,wt=14): 14251 x ^ ((x ^ y)' ^ ((y ^ z) ^ u)) = c_0. [para(1379(a,1),14038(a,1,2,2))]. given #829 (T,wt=14): 14252 x ^ ((x ^ y)' ^ ((z ^ y) ^ u)) = c_0. [para(1401(a,1),14038(a,1,2,2))]. given #830 (A,wt=19): 1745 ((x ^ y')' ^ (y' ^ z)') ^ (y ^ u) = y ^ u. [para(1236(a,1),1401(a,1,2,1)),rewrite(1236(17))]. given #831 (T,wt=14): 14258 x ^ ((x ^ y)' ^ (z ^ (y ^ u))) = c_0. [para(1703(a,1),14038(a,1,2,2))]. given #832 (T,wt=14): 14259 x ^ ((x ^ y)' ^ (z ^ (u ^ y))) = c_0. [para(1714(a,1),14038(a,1,2,2))]. given #833 (T,wt=14): 14293 ((x ^ y)' ^ (y ^ z)) ^ (x ^ u) = c_0. [para(14038(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #834 (T,wt=14): 14294 ((x ^ y)' ^ (y ^ z)) ^ (u ^ x) = c_0. [para(14038(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #835 (A,wt=17): 1746 x' ^ (((y ^ x) ^ z)' ^ (x ^ u)') = x'. [para(1401(a,1),1241(a,1,2,1,1))]. given #836 (T,wt=14): 14295 x ^ (((x ^ y)' ^ (y ^ z)) ^ u) = c_0. [para(14038(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #837 (T,wt=14): 14296 (x ^ y) ^ ((x ^ z)' ^ (z ^ u)) = c_0. [para(14038(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #838 (T,wt=14): 14297 x ^ (y ^ ((x ^ z)' ^ (z ^ u))) = c_0. [para(14038(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #839 (T,wt=14): 14298 (x ^ y) ^ ((y ^ z)' ^ (z ^ u)) = c_0. [para(14038(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #840 (A,wt=17): 1747 x' ^ ((x ^ y)' ^ ((z ^ x) ^ u)') = x'. [para(1401(a,1),1241(a,1,2,2,1))]. given #841 (T,wt=14): 14347 ((x ^ y)' ^ (z ^ y)) ^ (x ^ u) = c_0. [para(14040(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #842 (T,wt=14): 14348 ((x ^ y)' ^ (z ^ y)) ^ (u ^ x) = c_0. [para(14040(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #843 (T,wt=14): 14350 x ^ (((x ^ y)' ^ (z ^ y)) ^ u) = c_0. [para(14040(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #844 (T,wt=14): 14351 (x ^ y) ^ ((x ^ z)' ^ (u ^ z)) = c_0. [para(14040(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #845 (A,wt=19): 1748 ((x ^ y)' ^ (x ^ z)') ^ (x' ^ u) = x' ^ u. [para(1241(a,1),1401(a,1,2,1)),rewrite(1241(15))]. given #846 (T,wt=14): 14352 x ^ (y ^ ((x ^ z)' ^ (u ^ z))) = c_0. [para(14040(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #847 (T,wt=14): 14354 (x ^ y) ^ ((y ^ z)' ^ (u ^ z)) = c_0. [para(14040(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #848 (T,wt=14): 14518 x ^ (((y ^ z) ^ u) ^ (x ^ y)') = c_0. [para(1379(a,1),14172(a,1,2,1))]. given #849 (T,wt=14): 14519 x ^ (((y ^ z) ^ u) ^ (x ^ z)') = c_0. [para(1401(a,1),14172(a,1,2,1))]. given #850 (A,wt=17): 1749 x ^ ((x' ^ y)' ^ ((z ^ x') ^ u)') = x. [para(1401(a,1),1261(a,1,2,2,1))]. given #851 (T,wt=14): 14523 x ^ ((y ^ (z ^ u)) ^ (x ^ z)') = c_0. [para(1703(a,1),14172(a,1,2,1))]. given #852 (T,wt=14): 14524 x ^ ((y ^ (z ^ u)) ^ (x ^ u)') = c_0. [para(1714(a,1),14172(a,1,2,1))]. given #853 (T,wt=14): 14558 ((x ^ y) ^ (z ^ x)') ^ (z ^ u) = c_0. [para(14172(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #854 (T,wt=14): 14559 ((x ^ y) ^ (z ^ x)') ^ (u ^ z) = c_0. [para(14172(a,1),11803(a,1,1,1)),rewrite(1463(9))]. Low Water (displace, True_semantics): id=23159, wt=21 given #855 (A,wt=19): 1750 ((x' ^ y)' ^ (x' ^ z)') ^ (x ^ u) = x ^ u. [para(1261(a,1),1401(a,1,2,1)),rewrite(1261(17))]. given #856 (T,wt=14): 14560 x ^ (((y ^ z) ^ (x ^ y)') ^ u) = c_0. [para(14172(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #857 (T,wt=14): 14561 (x ^ y) ^ ((z ^ u) ^ (x ^ z)') = c_0. [para(14172(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #858 (T,wt=14): 14562 x ^ (y ^ ((z ^ u) ^ (x ^ z)')) = c_0. [para(14172(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #859 (T,wt=14): 14563 (x ^ y) ^ ((z ^ u) ^ (y ^ z)') = c_0. [para(14172(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #860 (A,wt=27): 1751 x ^ ((y ^ x)' ^ ((z ^ x) ^ u)')' = ((y ^ x)' ^ ((z ^ x) ^ u)')'. [para(1401(a,1),1194(a,1,2,1,2,1)),rewrite(1401(13))]. given #861 (T,wt=14): 14564 ((x ^ y) ^ (z ^ y)') ^ (z ^ u) = c_0. [para(14173(a,1),11740(a,1,1,1)),rewrite(1463(9))]. given #862 (T,wt=14): 14565 ((x ^ y) ^ (z ^ y)') ^ (u ^ z) = c_0. [para(14173(a,1),11803(a,1,1,1)),rewrite(1463(9))]. given #863 (T,wt=14): 14566 x ^ (((y ^ z) ^ (x ^ z)') ^ u) = c_0. [para(14173(a,1),11807(a,1,1,1)),rewrite(1463(9))]. given #864 (T,wt=14): 14567 (x ^ y) ^ ((z ^ u) ^ (x ^ u)') = c_0. [para(14173(a,1),11808(a,1,1,1)),rewrite(1463(9))]. given #865 (A,wt=31): 1752 x ^ ((y ^ (z ^ x))' ^ ((z ^ x) ^ u)')' = ((y ^ (z ^ x))' ^ ((z ^ x) ^ u)')'. [para(1194(a,1),1401(a,1,2)),rewrite(1194(19))]. given #866 (T,wt=14): 14568 x ^ (y ^ ((z ^ u) ^ (x ^ u)')) = c_0. [para(14173(a,1),11816(a,1,1,1)),rewrite(1463(9))]. given #867 (T,wt=14): 14569 (x ^ y) ^ ((z ^ u) ^ (y ^ u)') = c_0. [para(14173(a,1),11845(a,1,1,1)),rewrite(1463(9))]. given #868 (T,wt=14): 14620 (x ^ y)' ^ ((x ^ z) ^ (y ^ u)) = c_0. [para(1703(a,1),11809(a,1,2))]. given #869 (T,wt=14): 14623 (x ^ y)' ^ ((x ^ z) ^ (u ^ y)) = c_0. [para(1714(a,1),11809(a,1,2))]. given #870 (A,wt=16): 1761 ((x ^ y) ^ z)' ^ (x' ^ u) = x' ^ u. [para(1499(a,1),1401(a,1,2,1)),rewrite(1499(11))]. given #871 (T,wt=14): 14889 (x ^ y)' ^ ((z ^ x) ^ (y ^ u)) = c_0. [para(1703(a,1),11810(a,1,2))]. given #872 (T,wt=14): 14891 (x ^ y)' ^ ((z ^ x) ^ (u ^ y)) = c_0. [para(1714(a,1),11810(a,1,2))]. given #873 (T,wt=14): 15030 (x ^ (y ^ z)) ^ (x ^ (z ^ y))' = c_0. [para(1628(a,1),11811(a,1,2,1,2,1)),rewrite(1137(5))]. given #874 (T,wt=14): 15143 (x ^ y)' ^ ((y ^ z) ^ (x ^ u)) = c_0. [para(1379(a,1),11814(a,1,2))]. given #875 (A,wt=19): 1762 (x ^ y) ^ (x ^ ((z ^ (x ^ y)') ^ u)') = x ^ y. [para(1401(a,1),1238(a,1,2,2,1))]. given #876 (T,wt=14): 15144 (x ^ y)' ^ ((z ^ y) ^ (x ^ u)) = c_0. [para(1401(a,1),11814(a,1,2))]. given #877 (T,wt=14): 15401 (x ^ y)' ^ ((y ^ z) ^ (u ^ x)) = c_0. [para(1379(a,1),11815(a,1,2))]. given #878 (T,wt=14): 15402 (x ^ y)' ^ ((z ^ y) ^ (u ^ x)) = c_0. [para(1401(a,1),11815(a,1,2))]. given #879 (T,wt=14): 16412 ((x ^ y) ^ z) ^ ((y ^ x) ^ z)' = c_0. [para(11806(a,1),11883(a,1,1,1)),rewrite(1463(9))]. given #880 (A,wt=21): 1763 (x ^ ((x ^ y)' ^ z)') ^ ((x ^ y) ^ u) = (x ^ y) ^ u. [para(1238(a,1),1401(a,1,2,1)),rewrite(1238(15))]. given #881 (T,wt=14): 16903 ((x ^ y) ^ (z ^ u)) ^ (z ^ x)' = c_0. [para(1379(a,1),11926(a,1,1))]. given #882 (T,wt=14): 16904 ((x ^ y) ^ (z ^ u)) ^ (z ^ y)' = c_0. [para(1401(a,1),11926(a,1,1))]. given #883 (T,wt=14): 17086 ((x ^ y) ^ (z ^ u)) ^ (u ^ x)' = c_0. [para(1379(a,1),11927(a,1,1))]. Low Water (displace, True_semantics): id=24292, wt=20 given #884 (T,wt=14): 17087 ((x ^ y) ^ (z ^ u)) ^ (u ^ y)' = c_0. [para(1401(a,1),11927(a,1,1))]. given #885 (A,wt=16): 1765 ((x ^ y) ^ z)' ^ (y' ^ u) = y' ^ u. [para(1573(a,1),1401(a,1,2,1)),rewrite(1573(11))]. given #886 (T,wt=14): 23577 x ^ (((y ^ x)' ^ z) ^ (y ^ u)) = c_0. [para(1703(a,1),13869(a,1,2))]. given #887 (T,wt=14): 23580 x ^ (((y ^ x)' ^ z) ^ (u ^ y)) = c_0. [para(1714(a,1),13869(a,1,2))]. given #888 (T,wt=14): 23629 x ^ ((y ^ (z ^ x)') ^ (z ^ u)) = c_0. [para(1703(a,1),13870(a,1,2))]. given #889 (T,wt=14): 23631 x ^ ((y ^ (z ^ x)') ^ (u ^ z)) = c_0. [para(1714(a,1),13870(a,1,2))]. given #890 (A,wt=16): 1767 (x ^ (y ^ z))' ^ (y' ^ u) = y' ^ u. [para(1578(a,1),1401(a,1,2,1)),rewrite(1578(11))]. given #891 (T,wt=14): 23673 x ^ ((y ^ z) ^ ((y ^ x)' ^ u)) = c_0. [para(1379(a,1),13872(a,1,2))]. given #892 (T,wt=14): 23674 x ^ ((y ^ z) ^ ((z ^ x)' ^ u)) = c_0. [para(1401(a,1),13872(a,1,2))]. given #893 (T,wt=14): 23719 x ^ ((y ^ z) ^ (u ^ (y ^ x)')) = c_0. [para(1379(a,1),13874(a,1,2))]. given #894 (T,wt=14): 23720 x ^ ((y ^ z) ^ (u ^ (z ^ x)')) = c_0. [para(1401(a,1),13874(a,1,2))]. given #895 (A,wt=16): 1768 (x ^ (y ^ z))' ^ (z' ^ u) = z' ^ u. [para(1672(a,1),1401(a,1,2,1)),rewrite(1672(11))]. Low Water (keep, True_semantics): wt=19 given #896 (T,wt=14): 24325 x ^ (((x ^ y)' ^ z) ^ (y ^ u)) = c_0. [para(1703(a,1),14032(a,1,2))]. given #897 (T,wt=14): 24328 x ^ (((x ^ y)' ^ z) ^ (u ^ y)) = c_0. [para(1714(a,1),14032(a,1,2))]. given #898 (T,wt=14): 24373 x ^ ((y ^ (x ^ z)') ^ (z ^ u)) = c_0. [para(1703(a,1),14033(a,1,2))]. given #899 (T,wt=14): 24375 x ^ ((y ^ (x ^ z)') ^ (u ^ z)) = c_0. [para(1714(a,1),14033(a,1,2))]. given #900 (A,wt=17): 1769 x ^ (((y ^ x) ^ z) ^ u) = ((y ^ x) ^ z) ^ u. [para(1401(a,1),1379(a,1,2,1)),rewrite(1401(7))]. given #901 (T,wt=14): 24475 x ^ ((y ^ z) ^ ((x ^ y)' ^ u)) = c_0. [para(1379(a,1),14037(a,1,2))]. given #902 (T,wt=14): 24476 x ^ ((y ^ z) ^ ((x ^ z)' ^ u)) = c_0. [para(1401(a,1),14037(a,1,2))]. given #903 (T,wt=14): 24521 x ^ ((y ^ z) ^ (u ^ (x ^ y)')) = c_0. [para(1379(a,1),14039(a,1,2))]. given #904 (T,wt=14): 24522 x ^ ((y ^ z) ^ (u ^ (x ^ z)')) = c_0. [para(1401(a,1),14039(a,1,2))]. given #905 (A,wt=17): 1770 x ^ ((y ^ (x ^ z)) ^ u) = (y ^ (x ^ z)) ^ u. [para(1401(a,1),1379(a,1,2)),rewrite(1401(9))]. given #906 (T,wt=15): 1828 (x ^ y) ^ ((z ^ y') ^ u)' = x ^ y. [para(1401(a,1),1522(a,1,2,1))]. given #907 (T,wt=15): 1837 (x ^ (y ^ z)')' ^ (z ^ y) = z ^ y. [para(1544(a,1),1552(a,1,2)),rewrite(1544(9))]. Low Water (keep, True_semantics): wt=18 given #908 (T,wt=15): 1841 (x ^ (y' ^ z))' ^ (u ^ y) = u ^ y. [para(1506(a,1),1552(a,1,2)),rewrite(1137(4),1506(11))]. given #909 (T,wt=15): 1869 (x ^ (y ^ z'))' ^ (u ^ z) = u ^ z. [para(1562(a,1),1552(a,1,2)),rewrite(1137(4),1562(11))]. given #910 (A,wt=38): 1771 ((x ^ y)' ^ (y ^ z)')' ^ (y ^ ((u ^ ((x ^ y)' ^ (y ^ z)')) ^ v)') = ((x ^ y)' ^ (y ^ z)')'. [para(1401(a,1),1247(a,1,2,2,1))]. given #911 (T,wt=15): 1870 (x ^ y) ^ (z ^ (y ^ x)')' = x ^ y. [para(1544(a,1),1579(a,1,1)),rewrite(1544(9))]. given #912 (T,wt=15): 1871 (x ^ y) ^ (z ^ (x' ^ u))' = x ^ y. [para(1497(a,1),1579(a,1,1)),rewrite(1137(5),1497(11))]. given #913 (T,wt=15): 1872 (x ^ y) ^ (z ^ (y' ^ u))' = x ^ y. [para(1506(a,1),1579(a,1,1)),rewrite(1137(5),1506(11))]. given #914 (T,wt=15): 1873 (x ^ y) ^ (z ^ (u ^ x'))' = x ^ y. [para(1552(a,1),1579(a,1,1)),rewrite(1137(5),1552(11))]. given #915 (A,wt=40): 1772 (x ^ (((y ^ x)' ^ (x ^ z)') ^ u)') ^ (((y ^ x)' ^ (x ^ z)')' ^ v) = ((y ^ x)' ^ (x ^ z)')' ^ v. [para(1247(a,1),1401(a,1,2,1)),rewrite(1247(31))]. given #916 (T,wt=15): 1874 (x ^ y) ^ (z ^ (u ^ y'))' = x ^ y. [para(1562(a,1),1579(a,1,1)),rewrite(1137(5),1562(11))]. given #917 (T,wt=15): 1891 (x ^ y) ^ (z ^ (y ^ x)) = z ^ (y ^ x). [para(1544(a,1),1703(a,1,2,2)),rewrite(1544(7))]. given #918 (T,wt=15): 1927 x ^ ((((x' ^ y) ^ z) ^ u) ^ v)' = x. [para(1379(a,1),1723(a,1,2,1,1,1))]. given #919 (T,wt=15): 1929 x ^ ((((y ^ x') ^ z) ^ u) ^ v)' = x. [para(1401(a,1),1723(a,1,2,1,1,1))]. given #920 (A,wt=17): 1773 x ^ ((y ^ (z ^ x)) ^ u) = (y ^ (z ^ x)) ^ u. [para(1401(a,1),1401(a,1,2)),rewrite(1401(9))]. given #921 (T,wt=15): 1930 x ^ (((y ^ (x' ^ z)) ^ u) ^ v)' = x. [para(1401(a,1),1723(a,1,2,1,1))]. given #922 (T,wt=15): 1931 x ^ ((y ^ ((x' ^ z) ^ u)) ^ v)' = x. [para(1401(a,1),1723(a,1,2,1))]. given #923 (T,wt=15): 1940 x ^ (y ^ (((x' ^ z) ^ u) ^ v))' = x. [para(1723(a,1),1562(a,1,2)),rewrite(1137(6),1630(7),1723(13))]. given #924 (T,wt=15): 1943 x ^ (((y ^ (z ^ x')) ^ u) ^ v)' = x. [para(1714(a,1),1723(a,1,2,1,1,1))]. given #925 (A,wt=23): 1774 (x' ^ y) ^ ((z ^ (x' ^ y)')' ^ (x ^ u)') = x' ^ y. [para(1497(a,1),1207(a,1,2,2,1)),rewrite(1137(4),1137(15))]. given #926 (T,wt=15): 1944 x ^ ((y ^ (z ^ (x' ^ u))) ^ v)' = x. [para(1714(a,1),1723(a,1,2,1,1))]. given #927 (T,wt=15): 1945 x ^ (y ^ (z ^ ((x' ^ u) ^ v)))' = x. [para(1714(a,1),1723(a,1,2,1))]. given #928 (T,wt=15): 1976 x ^ ((y ^ ((z ^ x') ^ u)) ^ v)' = x. [para(1401(a,1),1724(a,1,2,1))]. given #929 (T,wt=15): 1981 x ^ (y ^ (((z ^ x') ^ u) ^ v))' = x. [para(1724(a,1),1562(a,1,2)),rewrite(1137(6),1630(7),1724(13))]. given #930 (A,wt=23): 1775 (x' ^ y) ^ ((x ^ z)' ^ ((x' ^ y)' ^ u)') = x' ^ y. [para(1497(a,1),1241(a,1,2,1,1)),rewrite(1137(4),1137(15))]. given #931 (T,wt=15): 1983 x ^ ((y ^ (z ^ (u ^ x'))) ^ v)' = x. [para(1714(a,1),1724(a,1,2,1,1))]. given #932 (T,wt=15): 1984 x ^ (y ^ (z ^ ((u ^ x') ^ v)))' = x. [para(1714(a,1),1724(a,1,2,1))]. given #933 (T,wt=15): 1994 x ^ (y ^ ((z ^ (x' ^ u)) ^ v))' = x. [para(1401(a,1),1725(a,1,2,1,2))]. given #934 (T,wt=15): 2004 x ^ (y ^ ((z ^ (u ^ x')) ^ v))' = x. [para(1714(a,1),1725(a,1,2,1,2,1))]. given #935 (A,wt=23): 1776 (x' ^ y) ^ (((x' ^ y)' ^ z)' ^ (x ^ u)') = x' ^ y. [para(1497(a,1),1241(a,1,2,2,1)),rewrite(1137(4),1137(15))]. given #936 (T,wt=15): 2005 x ^ (y ^ (z ^ (u ^ (x' ^ v))))' = x. [para(1714(a,1),1725(a,1,2,1,2))]. given #937 (T,wt=15): 2042 x ^ (y ^ (z ^ (u ^ (v ^ x'))))' = x. [para(1714(a,1),1755(a,1,2,1))]. given #938 (T,wt=15): 2150 (x ^ y) ^ (y ^ (x' ^ z)') = x ^ y. [para(1498(a,1),1298(a,1,2,2,1))]. given #939 (T,wt=15): 2168 (x ^ y) ^ (y ^ (z ^ x')') = x ^ y. [para(1505(a,1),1298(a,1,2,2,1))]. given #940 (A,wt=35): 1777 (x' ^ y)' ^ ((z ^ (x' ^ y)')' ^ (x ^ u)')' = ((z ^ (x' ^ y)')' ^ (x ^ u)')'. [para(1497(a,1),1194(a,1,2,1,2,1)),rewrite(1497(23))]. given #941 (T,wt=15): 2184 (x ^ y) ^ (x ^ (y' ^ z)') = x ^ y. [para(1553(a,1),1238(a,1,2,2,1))]. given #942 (T,wt=15): 2214 (x ^ y) ^ (x ^ (z ^ y')') = x ^ y. [para(1561(a,1),1238(a,1,2,2,1))]. given #943 (T,wt=15): 2226 (x ^ (y ^ z)) ^ (z ^ y) = x ^ (y ^ z). [para(1628(a,1),1522(a,1,2,1)),rewrite(1137(5))]. given #944 (T,wt=15): 3135 x' ^ ((y ^ x)' ^ (x ^ z)')' = c_0. [para(1194(a,1),3033(a,1,2))]. given #945 (A,wt=16): 1778 (x' ^ y) ^ ((x ^ z) ^ u)' = x' ^ y. [para(1497(a,1),1511(a,1,2,1,1))]. given #946 (T,wt=15): 3139 x' ^ ((x ^ y)' ^ (x ^ z)')' = c_0. [para(1249(a,1),3033(a,1,2))]. given #947 (T,wt=15): 3163 x' ^ ((y ^ x)' ^ (z ^ x)')' = c_0. [para(1305(a,1),3044(a,1,2)),rewrite(1630(8))]. given #948 (T,wt=15): 3165 x' ^ ((x ^ y)' ^ (z ^ x)')' = c_0. [para(1309(a,1),3044(a,1,2)),rewrite(1630(8))]. given #949 (T,wt=15): 7929 (x ^ y) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(1137(a,1),1589(a,1,1,1)),rewrite(1137(3),1137(6))]. given #950 (A,wt=16): 1779 (x' ^ y) ^ (z ^ (x ^ u))' = x' ^ y. [para(1497(a,1),1520(a,1,2,1,2))]. given #951 (T,wt=14): 27882 (x ^ (y ^ z))' ^ (z ^ (y ^ x)) = c_0. [para(7929(a,1),11815(a,1,2))]. given #952 (T,wt=14): 27883 (x ^ (y ^ z)) ^ (z ^ (y ^ x))' = c_0. [para(7929(a,1),11927(a,1,1))]. given #953 (T,wt=14): 27884 (x ^ (y ^ z)) ^ ((y ^ x) ^ z)' = c_0. [para(7929(a,1),12113(a,1,2)),rewrite(1630(6))]. given #954 (T,wt=14): 27885 x ^ (y ^ (z ^ (z ^ (y ^ x))')) = c_0. [para(7929(a,1),13172(a,1))]. given #955 (A,wt=21): 1780 (x ^ y) ^ ((x' ^ z)' ^ ((x ^ y)' ^ u)') = x ^ y. [para(1497(a,1),1238(a,1,1)),rewrite(1497(9),1497(15))]. given #956 (T,wt=14): 27886 x ^ (y ^ (z ^ ((y ^ x) ^ z)')) = c_0. [para(7929(a,1),13305(a,1))]. given #957 (T,wt=14): 27887 x ^ (y ^ (z ^ ((z ^ y) ^ x)')) = c_0. [para(7929(a,1),13874(a,1,2))]. given #958 (T,wt=14): 27888 x ^ (y ^ (z ^ (x ^ (z ^ y))')) = c_0. [para(7929(a,1),14039(a,1,2))]. given #959 (T,wt=14): 27890 (x ^ (y ^ z))' ^ (y ^ (z ^ x)) = c_0. [para(1630(a,1),27882(a,1,1,1,2))]. given #960 (A,wt=17): 1781 (x' ^ y)' ^ ((z ^ x) ^ u) = (z ^ x) ^ u. [para(1401(a,1),1497(a,1,2)),rewrite(1401(9))]. given #961 (T,wt=14): 27891 (x ^ (y ^ z))' ^ (z ^ (x ^ y)) = c_0. [para(1630(a,1),27882(a,1,2,2))]. given #962 (T,wt=14): 27892 (x ^ (y ^ z))' ^ ((y ^ x) ^ z) = c_0. [para(1630(a,1),27882(a,1,2))]. given #963 (T,wt=14): 27903 x ^ (y ^ (z ^ (z ^ (x ^ y))')) = c_0. [para(12308(a,1),27882(a,1,1,1)),rewrite(1463(9))]. given #964 (T,wt=14): 27904 (x ^ y) ^ (z ^ (y ^ (x ^ z))') = c_0. [para(27882(a,1),27882(a,1,1,1)),rewrite(1463(9))]. given #965 (A,wt=23): 1782 (x' ^ y) ^ ((z ^ (x' ^ y)')' ^ (u ^ x)') = x' ^ y. [para(1506(a,1),1207(a,1,2,2,1)),rewrite(1137(4),1137(15))]. given #966 (T,wt=14): 27906 (x ^ (y ^ z)) ^ (y ^ (z ^ x))' = c_0. [para(1630(a,1),27883(a,1,1,2))]. given #967 (T,wt=14): 27907 (x ^ (y ^ z)) ^ (z ^ (x ^ y))' = c_0. [para(1630(a,1),27883(a,1,2,1,2))]. given #968 (T,wt=14): 27911 (x ^ (y ^ z)) ^ ((z ^ x) ^ y)' = c_0. [para(1630(a,1),27884(a,1,1,2))]. given #969 (T,wt=14): 27912 ((x ^ y) ^ z) ^ ((x ^ z) ^ y)' = c_0. [para(1630(a,1),27884(a,1,1))]. given #970 (A,wt=23): 1783 (x' ^ y) ^ ((z ^ x)' ^ ((x' ^ y)' ^ u)') = x' ^ y. [para(1506(a,1),1241(a,1,2,1,1)),rewrite(1137(4),1137(15))]. given #971 (T,wt=14): 27913 (x ^ (y ^ z)) ^ ((x