============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11418 was started by mccune on cleo.thornwood, Sat Aug 12 21:01:01 2006 The command was "/home/mccune/bin/prover9 -f olsax2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file olsax2.in 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). [goal]. 2 f(f(x,x),f(x,y)) = x # answer(absorb). [goal]. 3 f(x,f(x,x)) = f(y,f(y,y)) # answer(one). [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). [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). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 11 f(x,x) = x'. [copy(10),flip(a)]. 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)]. 20 f(x,y)' = x ^ y. [back_rewrite(9),rewrite(11(3))]. 21 f(x',y') = x v y. [back_rewrite(7),rewrite(11(1),11(2))]. 22 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(x',x)),z))) = y. [back_rewrite(5),rewrite(11(5))]. 23 f(c9,c8 ^ c10) != f(c8,c9 ^ c10) | f(c8',f(c8,c9)) != c8 | f(c9,c9') != f(c8,c8') # answer(combined). [back_rewrite(19),rewrite(20(5),20(10))]. 24 f(c2,c1 ^ c3) != f(c1,c2 ^ c3) # answer(assoc). [back_rewrite(13),rewrite(20(5),20(10))]. 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=0): 15 f(c4',f(c4,c5)) != c4 # answer(absorb). [copy(14),rewrite(11(3))]. given #3 (I,wt=0): 17 f(c7,c7') != f(c6,c6') # answer(one). [copy(16),rewrite(11(4),11(8)),flip(a)]. given #4 (I,wt=8): 20 f(x,y)' = x ^ y. [back_rewrite(9),rewrite(11(3))]. given #5 (I,wt=9): 21 f(x',y') = x v y. [back_rewrite(7),rewrite(11(1),11(2))]. given #6 (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 #7 (I,wt=0): 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))]. given #8 (I,wt=0): 24 f(c2,c1 ^ c3) != f(c1,c2 ^ c3) # answer(assoc). [back_rewrite(13),rewrite(20(5),20(10))]. given #9 (T,wt=7): 25 x ^ x = x''. [para(11(a,1),20(a,1,1)),flip(a)]. given #10 (T,wt=7): 26 x v x = x''. [para(21(a,1),11(a,1))]. given #11 (A,wt=10): 27 (x v y)' = x' ^ y'. [para(21(a,1),20(a,1,1))]. given #12 (F,wt=12): 28 f(x ^ y,z') = f(x,y) v z. [para(20(a,1),21(a,1,1))]. given #13 (F,wt=12): 29 f(x',y ^ z) = x v f(y,z). [para(20(a,1),21(a,1,2))]. given #14 (T,wt=14): 43 f(x',y' ^ z') = x v (y v z). [para(27(a,1),21(a,1,2))]. given #15 (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 #16 (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 #17 (F,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 #18 (F,wt=17): 48 f(x ^ y,z' ^ u') = f(x,y) v (z v u). [para(27(a,1),28(a,1,2))]. given #19 (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 #20 (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 #21 (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 #22 (F,wt=17): 55 f(x',y' ^ (z ^ u)) = x v (y v f(z,u)). [para(29(a,1),29(a,2,2))]. given #23 (F,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 #24 (T,wt=18): 32 f(f(x'',y),f(x,f(f(x,f(x',x)),x))) = x. [para(11(a,1),22(a,1,1,1)),rewrite(11(1))]. given #25 (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 #26 (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 #27 (F,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 #28 (F,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 #29 (T,wt=12): 236 f(x',f(x'',x)) = x''. [para(32(a,1),190(a,1,2,2))]. given #30 (T,wt=13): 238 x' ^ f(x'',x) = x'''. [para(236(a,1),20(a,1,1)),flip(a)]. given #31 (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 #32 (F,wt=14): 240 f(x'',x'' v x) = x'''. [para(21(a,1),236(a,1,2))]. given #33 (F,wt=15): 229 f(x,f(x',x' ^ (x' v x))) = x'. [para(11(a,1),190(a,1,2,2)),rewrite(20(6))]. given #34 (T,wt=14): 275 f(x,x v f(x',x' v x)) = x'. [para(29(a,1),229(a,1,2))]. given #35 (T,wt=15): 253 x'' ^ (x'' v x) = x''''. [para(21(a,1),238(a,1,2))]. given #36 (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 #37 (F,wt=15): 281 x ^ (x v f(x',x' v x)) = x''. [para(275(a,1),20(a,1,1)),flip(a)]. given #38 (F,wt=16): 271 x ^ f(x',x' ^ (x' v x)) = x''. [para(229(a,1),20(a,1,1)),flip(a)]. given #39 (T,wt=17): 239 f(x ^ y,f((x ^ y)',f(x,y))) = (x ^ y)'. [para(20(a,1),236(a,1,1)),rewrite(20(3),20(8))]. given #40 (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 #41 (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 #42 (F,wt=18): 223 (x' v y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(184(a,1),20(a,1,1)),flip(a)]. given #43 (F,wt=18): 230 x ^ f(x',f(f(x',x' v x),y)) = x''. [para(190(a,1),20(a,1,1)),flip(a)]. given #44 (T,wt=18): 252 (x ^ y) ^ f((x ^ y)',f(x,y)) = (x ^ y)''. [para(20(a,1),238(a,1,1)),rewrite(20(3),20(8))]. given #45 (T,wt=18): 307 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 #46 (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 #47 (F,wt=12): 411 f(x,f(x',x' v x)) = x'. [para(307(a,1),190(a,1,2))]. given #48 (F,wt=13): 414 x ^ f(x',x' v x) = x''. [para(307(a,1),230(a,1,2))]. given #49 (T,wt=18): 308 f(x,f(x',x' ^ f(y ^ x,f(y,x)))) = x'. [para(31(a,1),35(a,1,1)),rewrite(20(4))]. given #50 (T,wt=17): 464 f(x,x v f(x',f(y ^ x,f(y,x)))) = x'. [para(29(a,1),308(a,1,2))]. given #51 (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 #52 (F,wt=18): 384 x ^ f(f(x,y),f(x,y) ^ (x' v x)) = x ^ y. [para(307(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. given #53 (F,wt=18): 475 x ^ (x v f(x',f(y ^ x,f(y,x)))) = x''. [para(464(a,1),20(a,1,1)),flip(a)]. given #54 (T,wt=19): 59 f(x',(y' ^ z') ^ u') = x v ((y v z) v u). [para(27(a,1),43(a,1,2,1))]. given #55 (T,wt=19): 60 f(x',y' ^ (z' ^ u')) = x v (y v (z v u)). [para(27(a,1),43(a,1,2,2))]. given #56 (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 #57 (F,wt=19): 63 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 #58 (F,wt=19): 73 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 #59 (T,wt=19): 129 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 #60 (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 #61 (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 #62 (F,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 #63 (F,wt=19): 244 f((x ^ y)',(x ^ y)' v f(x,y)) = (x ^ y)''. [para(29(a,1),236(a,1,2))]. given #64 (T,wt=19): 434 f(f(x,y),f(x ^ y,(x ^ y) v f(x,y))) = x ^ y. [para(20(a,1),411(a,1,2,1)),rewrite(20(4),20(9))]. given #65 (T,wt=19): 457 x ^ f(x',x' ^ f(y ^ x,f(y,x))) = x''. [para(308(a,1),20(a,1,1)),flip(a)]. given #66 (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 #67 (F,wt=8): 759 f(x,x'') = x'. [para(41(a,1),190(a,1,2,2)),rewrite(11(3))]. given #68 (F,wt=9): 764 x ^ x'' = x''. [para(41(a,1),230(a,1,2,2)),rewrite(11(3))]. given #69 (T,wt=9): 775 x v x'' = x''. [para(759(a,1),21(a,1)),flip(a)]. given #70 (T,wt=12): 774 f(f(x,y),(x ^ y)') = x ^ y. [para(20(a,1),759(a,1,2,1)),rewrite(20(6))]. given #71 (A,wt=23): 42 f(x,f(f(x,y),f(f(f(x,y),f(z ^ x,f(z,x))),u))) = f(x,y). [para(22(a,1),22(a,1,1)),rewrite(20(4))]. given #72 (F,wt=9): 882 f(x,x ^ y) = f(x,y). [para(41(a,1),42(a,1,2,2)),rewrite(11(3),20(2))]. given #73 (F,wt=7): 1010 x'' v x = x. [para(181(a,1),882(a,2)),rewrite(192(12),21(5))]. given #74 (T,wt=7): 1145 x'''' = x. [back_rewrite(752),rewrite(1078(1),1078(6),1078(10),1078(14),1078(18),1078(22),1143(22))]. given #75 (T,wt=7): 1166 x'' ^ x = x. [back_rewrite(1063),rewrite(1145(7))]. given #76 (A,wt=9): 995 x ^ (x ^ y) = x ^ y. [para(882(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. given #77 (F,wt=0): 1158 (c2 ^ (c1 ^ c3))''' != (c1 ^ (c2 ^ c3))''' # answer(assoc). [back_rewrite(24),rewrite(1078(5),1078(13))]. given #78 (F,wt=0): 1159 (c9 ^ (c8 ^ c10))''' != (c8 ^ (c9 ^ c10))''' | (c8' ^ (c8 ^ c9)''')''' != c8 | (c9 ^ c9')''' != (c8 ^ c8')''' # answer(combined). [back_rewrite(23),rewrite(1078(5),1078(13),1078(22),1078(26),1078(35),1078(42))]. given #79 (T,wt=10): 1078 f(x,y) = (x ^ y)'''. [para(1010(a,1),29(a,2)),rewrite(20(2),1019(5)),flip(a)]. given #80 (T,wt=12): 1079 x v y = (x' ^ y')'''. [para(1010(a,1),43(a,2,2)),rewrite(1063(6),1076(6),1078(3)),flip(a)]. given #81 (A,wt=14): 1088 ((x ^ y)''' ^ x')''' = x. [back_rewrite(1040),rewrite(1078(1),1078(6))]. ============================== PROOF ================================= % Proof 1 at 0.26 (+ 0.01) seconds: absorb. % Length of proof is 44. % Level of proof is 14. % Maximum clause weight is 36. % Given clauses 81. 2 f(f(x,x),f(x,y)) = x # answer(absorb). [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)]. 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))]. 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))]. 42 f(x,f(f(x,y),f(f(f(x,y),f(z ^ x,f(z,x))),u))) = f(x,y). [para(22(a,1),22(a,1,1)),rewrite(20(4))]. 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)]. 236 f(x',f(x'',x)) = x''. [para(32(a,1),190(a,1,2,2))]. 240 f(x'',x'' v x) = x'''. [para(21(a,1),236(a,1,2))]. 337 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))]. 752 f(f(x,y),f(y,f(f(y,f(x',x)),z))) = y. [para(41(a,1),22(a,1,1))]. 763 f(x,y) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(41(a,1),36(a,1,1))]. 857 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),42(a,1,2,2))]. 882 f(x,x ^ y) = f(x,y). [para(41(a,1),42(a,1,2,2)),rewrite(11(3),20(2))]. 1010 x'' v x = x. [para(181(a,1),882(a,2)),rewrite(192(12),21(5))]. 1019 f(x'',x) = x'''. [para(240(a,1),882(a,2)),rewrite(1010(7),882(6))]. 1040 f(f(x,y),x') = x. [para(41(a,1),882(a,2)),rewrite(337(17))]. 1078 f(x,y) = (x ^ y)'''. [para(1010(a,1),29(a,2)),rewrite(20(2),1019(5)),flip(a)]. 1088 ((x ^ y)''' ^ x')''' = x. [back_rewrite(1040),rewrite(1078(1),1078(6))]. 1124 (x' ^ ((x' ^ (x ^ y)''')''' ^ x)''')''' = (x' ^ (x ^ y)''')'''. [back_rewrite(857),rewrite(1078(3),1078(7),1078(11),1078(15),1078(20),1078(24))]. 1143 (x ^ y)''' ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(763),rewrite(1078(1),1078(6),1078(10),1078(14),1078(18))]. 1145 x'''' = x. [back_rewrite(752),rewrite(1078(1),1078(6),1078(10),1078(14),1078(18),1078(22),1143(22))]. 1161 (c4' ^ (c4 ^ c5)''')''' != c4 # answer(absorb). [back_rewrite(15),rewrite(1078(5),1078(9))]. 1167 x'' = x. [para(25(a,1),1088(a,1,1,1,1,1,1,1,1)),rewrite(1145(4),25(3),1145(4))]. 1171 ((x' ^ y)' ^ x)' = x'. [para(1145(a,1),1088(a,1,1,1,1,2)),rewrite(1167(2),1167(4),1167(6),1167(7))]. 1174 (c4' ^ (c4 ^ c5)')' != c4 # answer(absorb). [back_rewrite(1161),rewrite(1167(7),1167(9))]. 1188 (x' ^ (x ^ y)')' = x. [back_rewrite(1124),rewrite(1167(5),1167(7),1171(8),1167(3),25(3),1167(2),1167(2),1167(2),1167(4),1167(6)),flip(a)]. 1189 $F # answer(absorb). [resolve(1188,a,1174,a)]. ============================== end of proof ========================== % Redundant proof: 1208 $F # answer(absorb). [back_rewrite(1174),rewrite(1188(8)),xx(a)]. % Disable descendants: 14x 15x 1161x 1174x given #82 (F,wt=0): 1175 (c7 ^ c7')' != (c6 ^ c6')' # answer(one). [back_rewrite(1160),rewrite(1167(6),1167(11))]. given #83 (F,wt=0): 1177 (c2 ^ (c1 ^ c3))' != (c1 ^ (c2 ^ c3))' # answer(assoc). [back_rewrite(1158),rewrite(1167(7),1167(13))]. given #84 (T,wt=5): 1167 x'' = x. [para(25(a,1),1088(a,1,1,1,1,1,1,1,1)),rewrite(1145(4),25(3),1145(4))]. given #85 (T,wt=5): 1206 x ^ x = x. [back_rewrite(25),rewrite(1167(3))]. given #86 (A,wt=10): 1170 (x ^ y)' ^ x' = x'. [para(1088(a,1),764(a,2,1)),rewrite(1167(3),1167(6),1167(7),1167(10),1167(10),25(9),1167(6))]. given #87 (F,wt=0): 1207 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' | (c9 ^ c9')' != (c8 ^ c8')' # answer(combined). [back_rewrite(1176),rewrite(1188(21)),xx(b)]. given #88 (F,wt=8): 1205 f(x,y) = (x ^ y)'. [back_rewrite(1078),rewrite(1167(4))]. given #89 (T,wt=9): 1209 (x' ^ y)' ^ x = x. [para(1167(a,1),1170(a,1,2)),rewrite(1167(6))]. given #90 (T,wt=10): 1188 (x' ^ (x ^ y)')' = x. [back_rewrite(1124),rewrite(1167(5),1167(7),1171(8),1167(3),25(3),1167(2),1167(2),1167(2),1167(4),1167(6)),flip(a)]. given #91 (A,wt=27): 1180 ((x ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1155),rewrite(1167(3),1167(5),1167(9),1167(11),1167(13),1167(15))]. given #92 (F,wt=10): 1204 x v y = (x' ^ y')'. [back_rewrite(1079),rewrite(1167(6))]. given #93 (F,wt=10): 1210 x' ^ (x ^ y)' = x'. [para(1188(a,1),1167(a,1,1)),flip(a)]. given #94 (T,wt=9): 1225 x ^ (x' ^ y)' = x. [para(1167(a,1),1210(a,1,1)),rewrite(1167(6))]. given #95 (T,wt=9): 1226 (x ^ y) ^ x = x ^ y. [para(1170(a,1),1210(a,1,2,1)),rewrite(1167(3),1167(3),1167(5))]. given #96 (A,wt=26): 1182 x ^ ((x ^ y)' ^ (((x ^ y)' ^ (x ^ x')')' ^ z)')' = x ^ y. [back_rewrite(1152),rewrite(1167(3),1167(5),1167(6),1167(8),1167(10),1167(12),1167(14))]. given #97 (F,wt=13): 1203 (((x ^ y)' ^ y') ^ y')' = y. [back_rewrite(1089),rewrite(1167(3),1167(8))]. given #98 (F,wt=13): 1239 ((x ^ y)' ^ y') ^ y' = y'. [para(1203(a,1),1167(a,1,1)),flip(a)]. given #99 (T,wt=11): 1244 ((x ^ y')' ^ y) ^ y = y. [para(1167(a,1),1239(a,1,1,2)),rewrite(1167(6),1167(7))]. given #100 (T,wt=11): 1248 x ^ ((y ^ x')' ^ x) = x. [para(1244(a,1),1226(a,1,1)),rewrite(1244(10))]. given #101 (A,wt=25): 1185 ((x ^ y)' ^ y') ^ (y ^ ((y ^ (x' ^ x)')' ^ y)')' = y'. [back_rewrite(1147),rewrite(1167(3),1167(8),1167(10),1167(12),1167(14))]. given #102 (F,wt=13): 1245 x' ^ ((y ^ x)' ^ x') = x'. [para(1239(a,1),1226(a,1,1)),rewrite(1239(12))]. given #103 (F,wt=15): 1213 ((x ^ y)' ^ (y ^ z)') ^ y' = y'. [para(1180(a,1),995(a,1,2)),rewrite(1180(22))]. given #104 (T,wt=15): 1235 x' ^ ((y ^ x)' ^ (x ^ z)') = x'. [para(1180(a,1),1226(a,1,1)),rewrite(1180(22))]. given #105 (T,wt=15): 1255 ((x ^ y')' ^ (y' ^ z)') ^ y = y. [para(1167(a,1),1213(a,1,2)),rewrite(1167(10))]. given #106 (A,wt=22): 1187 (x ^ y)' ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1143),rewrite(1167(3),1167(6),1167(8),1167(10),1167(12))]. given #107 (F,wt=9): 1280 x ^ (y ^ x) = y ^ x. [para(1187(a,1),1170(a,1,1,1)),rewrite(1167(2),1167(3),1167(5))]. given #108 (F,wt=9): 1282 (x ^ y')' ^ y = y. [para(1209(a,1),1187(a,1,2,1,2,1)),rewrite(1206(6),1167(5),1167(6))]. given #109 (T,wt=9): 1283 (x ^ y) ^ y = x ^ y. [para(1187(a,1),1210(a,1,2,1)),rewrite(1167(3),1167(3),1167(5))]. given #110 (T,wt=9): 1290 x ^ (y ^ x')' = x. [para(1280(a,1),1225(a,1,2,1))]. given #111 (A,wt=23): 1191 (x ^ ((x ^ y)' ^ ((z ^ x) ^ (z ^ x)')')')' = (x ^ y)'. [back_rewrite(1122),rewrite(1167(3),1167(6),1167(8),1167(10),1167(12),1167(14))]. given #112 (F,wt=10): 1277 (x ^ y)' ^ y' = y'. [para(1187(a,1),995(a,1,2)),rewrite(1187(16))]. given #113 (F,wt=10): 1284 x' ^ (y ^ x)' = x'. [para(1187(a,1),1226(a,1,1)),rewrite(1187(16))]. given #114 (T,wt=15): 1259 ((x ^ y)' ^ (x ^ z)') ^ x' = x'. [para(1226(a,1),1213(a,1,1,1,1))]. given #115 (T,wt=15): 1264 x ^ ((y ^ x')' ^ (x' ^ z)') = x. [para(1167(a,1),1235(a,1,1)),rewrite(1167(10))]. given #116 (A,wt=20): 1194 (x ^ y)' ^ (x ^ ((x ^ y)' ^ (x ^ y))')' = x'. [back_rewrite(1115),rewrite(1167(3),1167(8),1167(10))]. given #117 (F,wt=15): 1269 x' ^ ((x ^ y)' ^ (x ^ z)') = x'. [para(1226(a,1),1235(a,1,2,1,1))]. given #118 (F,wt=15): 1276 ((x' ^ y)' ^ (x' ^ z)') ^ x = x. [para(1226(a,1),1255(a,1,1,1,1))]. given #119 (T,wt=15): 1293 ((x ^ y)' ^ (z ^ y)') ^ y' = y'. [para(1280(a,1),1213(a,1,1,2,1))]. given #120 (T,wt=15): 1294 x' ^ ((y ^ x)' ^ (z ^ x)') = x'. [para(1280(a,1),1235(a,1,2,2,1))]. given #121 (A,wt=19): 1198 ((((x ^ y)' ^ (y ^ z)')' ^ u)' ^ y')' = y. [back_rewrite(1103),rewrite(1167(3),1167(5),1167(7),1167(9),1167(12))]. given #122 (F,wt=12): 1373 (((x ^ y) ^ z)' ^ x')' = x. [para(1170(a,1),1198(a,1,1,1,1,1,1)),rewrite(1167(3))]. given #123 (F,wt=12): 1383 (((x ^ y) ^ z)' ^ y')' = y. [para(1290(a,1),1198(a,1,1,1,1,1,1)),rewrite(1167(3))]. given #124 (T,wt=12): 1390 ((x ^ y) ^ z)' ^ x' = x'. [para(1373(a,1),1167(a,1,1)),flip(a)]. given #125 (T,wt=11): 1425 ((x' ^ y) ^ z)' ^ x = x. [para(1167(a,1),1390(a,1,2)),rewrite(1167(7))]. given #126 (A,wt=29): 1214 ((x ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x' ^ x)')' ^ (y ^ z))')' = y'. [para(995(a,1),1180(a,1,1,2,1))]. given #127 (F,wt=11): 1439 x ^ ((x' ^ y) ^ z)' = x. [para(1425(a,1),1226(a,1,1)),rewrite(1425(10))]. given #128 (F,wt=11): 1440 ((x ^ y') ^ z)' ^ y = y. [para(1280(a,1),1425(a,1,1,1,1))]. given #129 (T,wt=11): 1441 (x ^ (y' ^ z))' ^ y = y. [para(1280(a,1),1425(a,1,1,1))]. given #130 (T,wt=11): 1455 x ^ ((y ^ x') ^ z)' = x. [para(1280(a,1),1439(a,1,2,1,1))]. given #131 (A,wt=36): 1215 ((x ^ y)' ^ (y ^ ((y ^ (x' ^ x)')' ^ z))') ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [para(995(a,1),1180(a,1,2,1,2,1))]. given #132 (F,wt=11): 1456 x ^ (y ^ (x' ^ z))' = x. [para(1280(a,1),1439(a,1,2,1))]. given #133 (F,wt=11): 1464 (x ^ (y ^ z'))' ^ z = z. [para(1280(a,1),1440(a,1,1,1))]. given #134 (T,wt=11): 1492 x ^ (y ^ (z ^ x'))' = x. [para(1280(a,1),1455(a,1,2,1))]. given #135 (T,wt=12): 1412 ((x ^ y) ^ z)' ^ y' = y'. [para(1383(a,1),1167(a,1,1)),flip(a)]. given #136 (A,wt=28): 1216 ((x' ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x ^ x')')' ^ z)')' = y'. [para(1167(a,1),1180(a,1,2,1,2,1,1,1,2,1,1))]. given #137 (F,wt=12): 1430 x' ^ ((x ^ y) ^ z)' = x'. [para(1390(a,1),1226(a,1,1)),rewrite(1390(10))]. given #138 (F,wt=12): 1433 (x ^ (y ^ z))' ^ y' = y'. [para(1280(a,1),1390(a,1,1,1))]. given #139 (T,wt=12): 1489 x' ^ ((y ^ x) ^ z)' = x'. [para(1167(a,1),1455(a,1,2,1,1,2))]. given #140 (T,wt=12): 1497 x' ^ (y ^ (x ^ z))' = x'. [para(1167(a,1),1456(a,1,2,1,2,1))]. given #141 (A,wt=28): 1218 ((x ^ y)' ^ (y ^ (y ^ (x' ^ x)')')') ^ (y ^ (x' ^ x)')' = y'. [para(1206(a,1),1180(a,1,2,1,2,1)),rewrite(1167(16),995(15))]. given #142 (F,wt=11): 1587 (x' ^ x) ^ y = x' ^ x. [para(1170(a,1),1218(a,1,1,2,1,2,1)),rewrite(1439(5),1167(9),1525(10),1170(9),1167(5),995(4),1167(7)),flip(a)]. given #143 (F,wt=9): 1598 (x' ^ x)' ^ y = y. [para(1587(a,1),1282(a,1,1,1))]. given #144 (T,wt=9): 1599 x ^ (y' ^ y)' = x. [para(1587(a,1),1290(a,1,2,1))]. NOTE: New constant: (x' ^ x)' = c_0. [new_symbol(1604)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c_0, ', ^, v, f ]). given #145 (T,wt=5): 1606 x ^ c_0 = x. [back_rewrite(1599),rewrite(1605(3))]. given #146 (A,wt=23): 1219 x ^ ((y ^ x)' ^ (x ^ z)')' = ((y ^ x)' ^ (x ^ z)')'. [para(1180(a,1),1170(a,1,1,1)),rewrite(1167(2))]. given #147 (F,wt=5): 1607 c_0 ^ x = x. [back_rewrite(1598),rewrite(1605(3))]. given #148 (F,wt=7): 1618 c_0' ^ x = c_0'. [para(1606(a,1),1587(a,1,1)),rewrite(1606(7))]. given #149 (T,wt=7): 1663 x' ^ x = c_0'. [para(1219(a,1),1587(a,1)),rewrite(1589(3),1605(3),1587(4),1605(4),1206(3)),flip(a)]. ============================== PROOF ================================= % Proof 2 at 0.37 (+ 0.01) seconds: one. % Length of proof is 83. % Level of proof is 26. % Maximum clause weight is 39. % Given clauses 149. 3 f(x,f(x,x)) = f(y,f(y,y)) # answer(one). [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)]. 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))]. 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))]. 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))]. 42 f(x,f(f(x,y),f(f(f(x,y),f(z ^ x,f(z,x))),u))) = f(x,y). [para(22(a,1),22(a,1,1)),rewrite(20(4))]. 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)]. 199 (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)]. 230 x ^ f(x',f(f(x',x' v x),y)) = x''. [para(190(a,1),20(a,1,1)),flip(a)]. 236 f(x',f(x'',x)) = x''. [para(32(a,1),190(a,1,2,2))]. 240 f(x'',x'' v x) = x'''. [para(21(a,1),236(a,1,2))]. 337 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))]. 752 f(f(x,y),f(y,f(f(y,f(x',x)),z))) = y. [para(41(a,1),22(a,1,1))]. 763 f(x,y) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(41(a,1),36(a,1,1))]. 764 x ^ x'' = x''. [para(41(a,1),230(a,1,2,2)),rewrite(11(3))]. 857 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),42(a,1,2,2))]. 882 f(x,x ^ y) = f(x,y). [para(41(a,1),42(a,1,2,2)),rewrite(11(3),20(2))]. 995 x ^ (x ^ y) = x ^ y. [para(882(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. 999 f(f(f(f(x,y),f(y,z)),u),y') = y. [para(22(a,1),882(a,2)),rewrite(36(14))]. 1010 x'' v x = x. [para(181(a,1),882(a,2)),rewrite(192(12),21(5))]. 1019 f(x'',x) = x'''. [para(240(a,1),882(a,2)),rewrite(1010(7),882(6))]. 1040 f(f(x,y),x') = x. [para(41(a,1),882(a,2)),rewrite(337(17))]. 1078 f(x,y) = (x ^ y)'''. [para(1010(a,1),29(a,2)),rewrite(20(2),1019(5)),flip(a)]. 1088 ((x ^ y)''' ^ x')''' = x. [back_rewrite(1040),rewrite(1078(1),1078(6))]. 1103 ((((x ^ y)''' ^ (y ^ z)''')''' ^ u)''' ^ y')''' = y. [back_rewrite(999),rewrite(1078(1),1078(5),1078(9),1078(13),1078(18))]. 1124 (x' ^ ((x' ^ (x ^ y)''')''' ^ x)''')''' = (x' ^ (x ^ y)''')'''. [back_rewrite(857),rewrite(1078(3),1078(7),1078(11),1078(15),1078(20),1078(24))]. 1143 (x ^ y)''' ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(763),rewrite(1078(1),1078(6),1078(10),1078(14),1078(18))]. 1145 x'''' = x. [back_rewrite(752),rewrite(1078(1),1078(6),1078(10),1078(14),1078(18),1078(22),1143(22))]. 1155 ((x ^ y)''' ^ (y ^ z)''') ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(199),rewrite(1078(1),1078(5),1078(11),1078(15),1078(19),1078(23))]. 1160 (c7 ^ c7')''' != (c6 ^ c6')''' # answer(one). [back_rewrite(17),rewrite(1078(4),1078(11))]. 1167 x'' = x. [para(25(a,1),1088(a,1,1,1,1,1,1,1,1)),rewrite(1145(4),25(3),1145(4))]. 1170 (x ^ y)' ^ x' = x'. [para(1088(a,1),764(a,2,1)),rewrite(1167(3),1167(6),1167(7),1167(10),1167(10),25(9),1167(6))]. 1171 ((x' ^ y)' ^ x)' = x'. [para(1145(a,1),1088(a,1,1,1,1,2)),rewrite(1167(2),1167(4),1167(6),1167(7))]. 1175 (c7 ^ c7')' != (c6 ^ c6')' # answer(one). [back_rewrite(1160),rewrite(1167(6),1167(11))]. 1180 ((x ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1155),rewrite(1167(3),1167(5),1167(9),1167(11),1167(13),1167(15))]. 1187 (x ^ y)' ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1143),rewrite(1167(3),1167(6),1167(8),1167(10),1167(12))]. 1188 (x' ^ (x ^ y)')' = x. [back_rewrite(1124),rewrite(1167(5),1167(7),1171(8),1167(3),25(3),1167(2),1167(2),1167(2),1167(4),1167(6)),flip(a)]. 1198 ((((x ^ y)' ^ (y ^ z)')' ^ u)' ^ y')' = y. [back_rewrite(1103),rewrite(1167(3),1167(5),1167(7),1167(9),1167(12))]. 1206 x ^ x = x. [back_rewrite(25),rewrite(1167(3))]. 1209 (x' ^ y)' ^ x = x. [para(1167(a,1),1170(a,1,2)),rewrite(1167(6))]. 1210 x' ^ (x ^ y)' = x'. [para(1188(a,1),1167(a,1,1)),flip(a)]. 1218 ((x ^ y)' ^ (y ^ (y ^ (x' ^ x)')')') ^ (y ^ (x' ^ x)')' = y'. [para(1206(a,1),1180(a,1,2,1,2,1)),rewrite(1167(16),995(15))]. 1219 x ^ ((y ^ x)' ^ (x ^ z)')' = ((y ^ x)' ^ (x ^ z)')'. [para(1180(a,1),1170(a,1,1,1)),rewrite(1167(2))]. 1225 x ^ (x' ^ y)' = x. [para(1167(a,1),1210(a,1,1)),rewrite(1167(6))]. 1226 (x ^ y) ^ x = x ^ y. [para(1170(a,1),1210(a,1,2,1)),rewrite(1167(3),1167(3),1167(5))]. 1277 (x ^ y)' ^ y' = y'. [para(1187(a,1),995(a,1,2)),rewrite(1187(16))]. 1280 x ^ (y ^ x) = y ^ x. [para(1187(a,1),1170(a,1,1,1)),rewrite(1167(2),1167(3),1167(5))]. 1282 (x ^ y')' ^ y = y. [para(1209(a,1),1187(a,1,2,1,2,1)),rewrite(1206(6),1167(5),1167(6))]. 1290 x ^ (y ^ x')' = x. [para(1280(a,1),1225(a,1,2,1))]. 1373 (((x ^ y) ^ z)' ^ x')' = x. [para(1170(a,1),1198(a,1,1,1,1,1,1)),rewrite(1167(3))]. 1390 ((x ^ y) ^ z)' ^ x' = x'. [para(1373(a,1),1167(a,1,1)),flip(a)]. 1425 ((x' ^ y) ^ z)' ^ x = x. [para(1167(a,1),1390(a,1,2)),rewrite(1167(7))]. 1439 x ^ ((x' ^ y) ^ z)' = x. [para(1425(a,1),1226(a,1,1)),rewrite(1425(10))]. 1455 x ^ ((y ^ x') ^ z)' = x. [para(1280(a,1),1439(a,1,2,1,1))]. 1456 x ^ (y ^ (x' ^ z))' = x. [para(1280(a,1),1439(a,1,2,1))]. 1492 x ^ (y ^ (z ^ x'))' = x. [para(1280(a,1),1455(a,1,2,1))]. 1525 x' ^ (y ^ (z ^ x))' = x'. [para(1167(a,1),1492(a,1,2,1,2,2))]. 1587 (x' ^ x) ^ y = x' ^ x. [para(1170(a,1),1218(a,1,1,2,1,2,1)),rewrite(1439(5),1167(9),1525(10),1170(9),1167(5),995(4),1167(7)),flip(a)]. 1589 x ^ (y' ^ y) = y' ^ y. [para(1282(a,1),1218(a,1,1,2,1,2,1)),rewrite(1167(4),1456(5),1167(5),1167(9),1525(10),1167(5),1277(9),1167(5),995(4),1167(6),1167(7)),flip(a)]. 1598 (x' ^ x)' ^ y = y. [para(1587(a,1),1282(a,1,1,1))]. 1599 x ^ (y' ^ y)' = x. [para(1587(a,1),1290(a,1,2,1))]. 1604 (x' ^ x)' = (y' ^ y)'. [para(1599(a,1),1598(a,1))]. 1605 (x' ^ x)' = c_0. [new_symbol(1604)]. 1663 x' ^ x = c_0'. [para(1219(a,1),1587(a,1)),rewrite(1589(3),1605(3),1587(4),1605(4),1206(3)),flip(a)]. 1668 x ^ x' = c_0'. [para(1167(a,1),1663(a,1,1))]. 1670 $F # answer(one). [back_rewrite(1175),rewrite(1668(4),1167(3),1668(5),1167(4)),xx(a)]. ============================== end of proof ========================== % Disable descendants: 16x 17x 1160x 1175x given #150 (T,wt=7): 1666 x ^ c_0' = c_0'. [back_rewrite(1589),rewrite(1663(2),1663(5))]. given #151 (A,wt=23): 1230 ((x ^ y)' ^ (y ^ z)')' ^ y = ((x ^ y)' ^ (y ^ z)')'. [para(1180(a,1),1210(a,1,2,1)),rewrite(1167(8))]. given #152 (F,wt=0): 1669 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' # answer(combined). [back_rewrite(1207),rewrite(1668(17),1167(16),1668(18),1167(17)),xx(b)]. given #153 (F,wt=7): 1668 x ^ x' = c_0'. [para(1167(a,1),1663(a,1,1))]. given #154 (T,wt=12): 1510 (x ^ (y ^ z))' ^ z' = z'. [para(1167(a,1),1464(a,1,1,1,2,2))]. given #155 (T,wt=12): 1525 x' ^ (y ^ (z ^ x))' = x'. [para(1167(a,1),1492(a,1,2,1,2,2))]. given #156 (A,wt=17): 1256 ((x ^ (y ^ z)')' ^ y) ^ (y ^ z) = y ^ z. [para(1170(a,1),1213(a,1,1,2,1)),rewrite(1167(6),1167(8),1167(10))]. given #157 (F,wt=11): 1717 (x ^ y) ^ (y ^ x) = y ^ x. [para(1284(a,1),1256(a,1,1,1,1)),rewrite(1167(2))]. % Operation ^ is commutative; C redundancy checks enabled. % back CAC tautology: 1744 (x ^ y)' = (y ^ x)'. [para(1717(a,1),1210(a,1,2,1)),rewrite(1743(5))]. given #158 (F,wt=7): 1745 x ^ y = y ^ x. [para(1717(a,1),1226(a,1,1)),rewrite(1717(3),1717(4))]. given #159 (T,wt=13): 1392 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(1373(a,1),1170(a,1,1)),rewrite(1167(4),1167(7))]. given #160 (T,wt=13): 1414 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z. [para(1383(a,1),1170(a,1,1)),rewrite(1167(4),1167(7))]. given #161 (A,wt=17): 1268 (x ^ y) ^ (x ^ ((x ^ y)' ^ z)') = x ^ y. [para(1210(a,1),1235(a,1,2,1,1)),rewrite(1167(3),1167(3),1167(10))]. given #162 (F,wt=13): 1426 (x' ^ y)' ^ (x ^ z) = x ^ z. [para(1170(a,1),1390(a,1,1,1,1)),rewrite(1167(6),1167(8))]. given #163 (F,wt=13): 1432 (x' ^ y)' ^ (z ^ x) = z ^ x. [para(1187(a,1),1390(a,1,1,1,1)),rewrite(1167(6),1167(8))]. given #164 (T,wt=13): 1450 (x ^ y) ^ (x' ^ z)' = x ^ y. [para(1170(a,1),1439(a,1,2,1,1))]. given #165 (T,wt=13): 1454 (x ^ y) ^ (y' ^ z)' = x ^ y. [para(1187(a,1),1439(a,1,2,1,1))]. given #166 (A,wt=36): 1275 ((x ^ y)' ^ (y ^ z)')' ^ (y ^ (((x ^ y)' ^ (y ^ z)') ^ u)') = ((x ^ y)' ^ (y ^ z)')'. [para(1235(a,1),1235(a,1,2,1,1)),rewrite(1167(8))]. given #167 (F,wt=13): 1470 (x ^ y')' ^ (y ^ z) = y ^ z. [para(1170(a,1),1441(a,1,1,1,2))]. given #168 (F,wt=13): 1476 (x ^ y')' ^ (z ^ y) = z ^ y. [para(1187(a,1),1441(a,1,1,1,2))]. given #169 (T,wt=13): 1498 (x ^ y) ^ (z ^ x')' = x ^ y. [para(1170(a,1),1456(a,1,2,1,2))]. given #170 (T,wt=13): 1502 (x ^ y) ^ (z ^ y')' = x ^ y. [para(1187(a,1),1456(a,1,2,1,2))]. given #171 (A,wt=17): 1319 (x ^ y) ^ (y ^ ((x ^ y)' ^ z)') = x ^ y. [para(1284(a,1),1235(a,1,2,1,1)),rewrite(1167(3),1167(3),1167(10))]. given #172 (F,wt=13): 1558 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(1433(a,1),1170(a,1,1,1)),rewrite(1167(2),1167(4),1167(7))]. given #173 (F,wt=13): 1696 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(1510(a,1),1170(a,1,1,1)),rewrite(1167(2),1167(4),1167(7))]. given #174 (T,wt=13): 1794 x ^ (((x' ^ y) ^ z) ^ u)' = x. [para(1392(a,1),1439(a,1,2,1,1))]. given #175 (T,wt=13): 1795 x ^ (((y ^ x') ^ z) ^ u)' = x. [para(1392(a,1),1455(a,1,2,1))]. given #176 (A,wt=23): 1320 x ^ ((x ^ y)' ^ (x ^ z)')' = ((x ^ y)' ^ (x ^ z)')'. [para(1259(a,1),1170(a,1,1,1)),rewrite(1167(2))]. given #177 (F,wt=13): 1796 x ^ (y ^ ((x' ^ z) ^ u))' = x. [para(1392(a,1),1456(a,1,2,1,2))]. given #178 (F,wt=13): 1810 x ^ ((y ^ (x' ^ z)) ^ u)' = x. [para(1414(a,1),1439(a,1,2,1))]. given #179 (T,wt=13): 1812 x ^ ((y ^ (z ^ x')) ^ u)' = x. [para(1414(a,1),1455(a,1,2,1))]. given #180 (T,wt=13): 1814 x ^ (y ^ ((z ^ x') ^ u))' = x. [para(1414(a,1),1456(a,1,2,1,2))]. given #181 (A,wt=15): 1332 x ^ ((x' ^ y)' ^ (x' ^ z)') = x. [para(1226(a,1),1264(a,1,2,1,1))]. given #182 (F,wt=13): 1901 x ^ (y ^ (z ^ (x' ^ u)))' = x. [para(1456(a,1),1476(a,1,2)),rewrite(1167(5),1745(6),1456(11))]. given #183 (F,wt=13): 1903 x ^ (y ^ (z ^ (u ^ x')))' = x. [para(1492(a,1),1476(a,1,2)),rewrite(1167(5),1745(6),1492(11))]. given #184 (T,wt=14): 1427 (x ^ y)' ^ (x' ^ z) = x' ^ z. [para(1209(a,1),1390(a,1,1,1,1)),rewrite(1167(6),1167(9))]. given #185 (T,wt=14): 1434 (x ^ y)' ^ (z ^ x') = z ^ x'. [para(1282(a,1),1390(a,1,1,1,1)),rewrite(1167(6),1167(9))]. given #186 (A,wt=15): 1333 x ^ ((y ^ x')' ^ (z ^ x')') = x. [para(1280(a,1),1264(a,1,2,2,1))]. given #187 (F,wt=14): 1451 (x' ^ y) ^ (x ^ z)' = x' ^ y. [para(1209(a,1),1439(a,1,2,1,1))]. given #188 (F,wt=14): 1457 (x ^ y') ^ (y ^ z)' = x ^ y'. [para(1282(a,1),1439(a,1,2,1,1))]. given #189 (T,wt=14): 1471 (x ^ y)' ^ (y' ^ z) = y' ^ z. [para(1209(a,1),1441(a,1,1,1,2))]. given #190 (T,wt=14): 1477 (x ^ y)' ^ (z ^ y') = z ^ y'. [para(1282(a,1),1441(a,1,1,1,2))]. given #191 (A,wt=36): 1342 ((x ^ y)' ^ (x ^ z)')' ^ (x ^ (((x ^ y)' ^ (x ^ z)') ^ u)') = ((x ^ y)' ^ (x ^ z)')'. [para(1269(a,1),1235(a,1,2,1,1)),rewrite(1167(8))]. given #192 (F,wt=14): 1499 (x' ^ y) ^ (z ^ x)' = x' ^ y. [para(1209(a,1),1456(a,1,2,1,2))]. given #193 (F,wt=14): 1503 (x ^ y') ^ (z ^ y)' = x ^ y'. [para(1282(a,1),1456(a,1,2,1,2))]. given #194 (T,wt=14): 1743 (x ^ y)' ^ (y ^ x)' = (y ^ x)'. [para(1717(a,1),1170(a,1,1,1))]. given #195 (T,wt=14): 1797 x' ^ (((x ^ y) ^ z) ^ u)' = x'. [para(1392(a,1),1430(a,1,2,1,1))]. given #196 (A,wt=15): 1344 x' ^ ((x ^ y)' ^ (z ^ x)') = x'. [para(1280(a,1),1269(a,1,2,2,1))]. given #197 (F,wt=14): 1798 x' ^ (((y ^ x) ^ z) ^ u)' = x'. [para(1392(a,1),1489(a,1,2,1))]. given #198 (F,wt=14): 1799 x' ^ (y ^ ((x ^ z) ^ u))' = x'. [para(1392(a,1),1497(a,1,2,1,2))]. given #199 (T,wt=14): 1817 x' ^ ((y ^ (x ^ z)) ^ u)' = x'. [para(1414(a,1),1430(a,1,2,1))]. given #200 (T,wt=14): 1819 x' ^ ((y ^ (z ^ x)) ^ u)' = x'. [para(1414(a,1),1489(a,1,2,1))]. given #201 (A,wt=23): 1348 x ^ ((y ^ x)' ^ (z ^ x)')' = ((y ^ x)' ^ (z ^ x)')'. [para(1293(a,1),1170(a,1,1,1)),rewrite(1167(2))]. given #202 (F,wt=14): 1821 x' ^ (y ^ ((z ^ x) ^ u))' = x'. [para(1414(a,1),1497(a,1,2,1,2))]. given #203 (F,wt=14): 1907 x' ^ (y ^ (z ^ (x ^ u)))' = x'. [para(1497(a,1),1476(a,1,2)),rewrite(1167(4),1745(6),1497(11))]. given #204 (T,wt=14): 1910 x' ^ (y ^ (z ^ (u ^ x)))' = x'. [para(1525(a,1),1476(a,1,2)),rewrite(1167(4),1745(6),1525(11))]. given #205 (T,wt=15): 1738 (x ^ y) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(1497(a,1),1256(a,1,1,1,1)),rewrite(1167(2))]. given #206 (A,wt=36): 1359 ((x ^ y)' ^ (z ^ y)')' ^ (y ^ (((x ^ y)' ^ (z ^ y)') ^ u)') = ((x ^ y)' ^ (z ^ y)')'. [para(1293(a,1),1269(a,1,2,1,1)),rewrite(1167(8))]. given #207 (F,wt=9): 2557 x' ^ (x ^ y) = c_0'. [para(1668(a,1),1738(a,1,1)),rewrite(1618(6)),flip(a)]. given #208 (F,wt=9): 2612 x ^ (x' ^ y) = c_0'. [para(1167(a,1),2557(a,1,1))]. given #209 (T,wt=9): 2613 x' ^ (y ^ x) = c_0'. [para(1280(a,1),2557(a,1,2))]. given #210 (T,wt=9): 2621 x ^ (y ^ x') = c_0'. [para(2557(a,1),1476(a,1)),rewrite(1745(5)),flip(a)]. given #211 (A,wt=17): 1362 (x ^ y) ^ (x ^ (z ^ (x ^ y)')') = x ^ y. [para(1210(a,1),1294(a,1,2,1,1)),rewrite(1167(3),1167(3),1167(10))]. given #212 (F,wt=11): 2615 (x ^ y)' ^ (y ^ x) = c_0'. [para(1717(a,1),2557(a,1,2))]. given #213 (F,wt=11): 2616 x' ^ ((x ^ y) ^ z) = c_0'. [para(1392(a,1),2557(a,1,2))]. given #214 (T,wt=11): 2617 x' ^ ((y ^ x) ^ z) = c_0'. [para(1414(a,1),2557(a,1,2))]. given #215 (T,wt=11): 2618 (x' ^ y) ^ (x ^ z) = c_0'. [para(1426(a,1),2557(a,1,2)),rewrite(1167(4))]. given #216 (A,wt=36): 1363 ((x ^ y)' ^ (y ^ z)')' ^ (y ^ (u ^ ((x ^ y)' ^ (y ^ z)'))') = ((x ^ y)' ^ (y ^ z)')'. [para(1235(a,1),1294(a,1,2,1,1)),rewrite(1167(8))]. given #217 (F,wt=11): 2619 (x' ^ y) ^ (z ^ x) = c_0'. [para(1432(a,1),2557(a,1,2)),rewrite(1167(4))]. given #218 (F,wt=11): 2620 (x ^ y') ^ (y ^ z) = c_0'. [para(1470(a,1),2557(a,1,2)),rewrite(1167(4))]. given #219 (T,wt=11): 2622 (x ^ y') ^ (z ^ y) = c_0'. [para(1476(a,1),2557(a,1,2)),rewrite(1167(4))]. given #220 (T,wt=11): 2623 x' ^ (y ^ (x ^ z)) = c_0'. [para(1558(a,1),2557(a,1,2))]. given #221 (A,wt=17): 1365 (x ^ y) ^ (y ^ (z ^ (x ^ y)')') = x ^ y. [para(1284(a,1),1294(a,1,2,1,1)),rewrite(1167(3),1167(3),1167(10))]. given #222 (F,wt=11): 2624 x' ^ (y ^ (z ^ x)) = c_0'. [para(1696(a,1),2557(a,1,2))]. given #223 (F,wt=11): 2626 (x ^ y) ^ (x' ^ z) = c_0'. [para(1427(a,1),2557(a,1,2)),rewrite(1167(3))]. given #224 (T,wt=11): 2627 (x ^ y) ^ (z ^ x') = c_0'. [para(1434(a,1),2557(a,1,2)),rewrite(1167(3))]. given #225 (T,wt=11): 2628 (x ^ y) ^ (y' ^ z) = c_0'. [para(1471(a,1),2557(a,1,2)),rewrite(1167(3))]. given #226 (A,wt=36): 1366 ((x ^ y)' ^ (x ^ z)')' ^ (x ^ (u ^ ((x ^ y)' ^ (x ^ z)'))') = ((x ^ y)' ^ (x ^ z)')'. [para(1269(a,1),1294(a,1,2,1,1)),rewrite(1167(8))]. given #227 (F,wt=11): 2629 (x ^ y) ^ (z ^ y') = c_0'. [para(1477(a,1),2557(a,1,2)),rewrite(1167(3))]. given #228 (F,wt=11): 2630 (x ^ y) ^ (y ^ x)' = c_0'. [para(1743(a,1),2557(a,1,2)),rewrite(1167(3))]. given #229 (T,wt=11): 2634 x ^ ((x' ^ y) ^ z) = c_0'. [para(1392(a,1),2612(a,1,2))]. given #230 (T,wt=11): 2635 x ^ ((y ^ x') ^ z) = c_0'. [para(1414(a,1),2612(a,1,2))]. given #231 (A,wt=36): 1368 ((x ^ y)' ^ (z ^ y)')' ^ (y ^ (u ^ ((x ^ y)' ^ (z ^ y)'))') = ((x ^ y)' ^ (z ^ y)')'. [para(1294(a,1),1294(a,1,2,1,1)),rewrite(1167(8))]. given #232 (F,wt=11): 2636 x ^ (y ^ (x' ^ z)) = c_0'. [para(1558(a,1),2612(a,1,2))]. given #233 (F,wt=11): 2637 x ^ (y ^ (z ^ x')) = c_0'. [para(1696(a,1),2612(a,1,2))]. given #234 (T,wt=11): 2967 x ^ (y ^ (y ^ x)') = c_0'. [para(2637(a,1),1738(a,1)),flip(a)]. given #235 (T,wt=11): 2968 x ^ (y ^ (x ^ y)') = c_0'. [para(1745(a,1),2967(a,1,2,2,1))]. given #236 (A,wt=27): 1371 x ^ (((y ^ x)' ^ (x ^ z)')' ^ u) = ((y ^ x)' ^ (x ^ z)')' ^ u. [para(1198(a,1),1170(a,1,1)),rewrite(1167(9),1167(17))]. given #237 (F,wt=13): 2632 (x ^ y)' ^ (y ^ (x ^ z)) = c_0'. [para(1738(a,1),2557(a,1,2))]. given #238 (F,wt=13): 2643 x ^ (((x' ^ y) ^ z) ^ u) = c_0'. [para(1794(a,1),2613(a,1,2)),rewrite(1167(6),1745(5))]. given #239 (T,wt=13): 2644 x ^ (((y ^ x') ^ z) ^ u) = c_0'. [para(1795(a,1),2613(a,1,2)),rewrite(1167(6),1745(5))]. given #240 (T,wt=13): 2645 x ^ (y ^ ((x' ^ z) ^ u)) = c_0'. [para(1796(a,1),2613(a,1,2)),rewrite(1167(6),1745(5))]. given #241 (A,wt=23): 1408 ((x ^ y) ^ z) ^ (x ^ (((x ^ y) ^ z)' ^ u)') = (x ^ y) ^ z. [para(1373(a,1),1269(a,1,2,1)),rewrite(1167(4),1167(13))]. given #242 (F,wt=13): 2646 x ^ ((y ^ (x' ^ z)) ^ u) = c_0'. [para(1810(a,1),2613(a,1,2)),rewrite(1167(6),1745(5))]. given #243 (F,wt=13): 2647 x ^ ((y ^ (z ^ x')) ^ u) = c_0'. [para(1812(a,1),2613(a,1,2)),rewrite(1167(6),1745(5))]. given #244 (T,wt=13): 2648 x ^ (y ^ ((z ^ x') ^ u)) = c_0'. [para(1814(a,1),2613(a,1,2)),rewrite(1167(6),1745(5))]. given #245 (T,wt=13): 2649 x ^ (y ^ (z ^ (x' ^ u))) = c_0'. [para(1901(a,1),2613(a,1,2)),rewrite(1167(6),1745(5))]. given #246 (A,wt=23): 1423 ((x ^ y) ^ z) ^ (y ^ (((x ^ y) ^ z)' ^ u)') = (x ^ y) ^ z. [para(1383(a,1),1269(a,1,2,1)),rewrite(1167(4),1167(13))]. given #247 (F,wt=13): 2650 x ^ (y ^ (z ^ (u ^ x'))) = c_0'. [para(1903(a,1),2613(a,1,2)),rewrite(1167(6),1745(5))]. given #248 (F,wt=13): 2652 x' ^ (((x ^ y) ^ z) ^ u) = c_0'. [para(1797(a,1),2613(a,1,2)),rewrite(1167(5),1745(5))]. given #249 (T,wt=13): 2654 x' ^ (((y ^ x) ^ z) ^ u) = c_0'. [para(1798(a,1),2613(a,1,2)),rewrite(1167(5),1745(5))]. given #250 (T,wt=13): 2655 x' ^ (y ^ ((x ^ z) ^ u)) = c_0'. [para(1799(a,1),2613(a,1,2)),rewrite(1167(5),1745(5))]. given #251 (A,wt=27): 1429 (x' ^ y)' ^ ((z ^ x)' ^ (x ^ u)')' = ((z ^ x)' ^ (x ^ u)')'. [para(1180(a,1),1390(a,1,1,1,1))]. given #252 (F,wt=13): 2656 x' ^ ((y ^ (x ^ z)) ^ u) = c_0'. [para(1817(a,1),2613(a,1,2)),rewrite(1167(5),1745(5))]. given #253 (F,wt=13): 2657 x' ^ ((y ^ (z ^ x)) ^ u) = c_0'. [para(1819(a,1),2613(a,1,2)),rewrite(1167(5),1745(5))]. given #254 (T,wt=13): 2658 x' ^ (y ^ ((z ^ x) ^ u)) = c_0'. [para(1821(a,1),2613(a,1,2)),rewrite(1167(5),1745(5))]. given #255 (T,wt=13): 2659 x' ^ (y ^ (z ^ (x ^ u))) = c_0'. [para(1907(a,1),2613(a,1,2)),rewrite(1167(5),1745(5))]. given #256 (A,wt=30): 1431 (x ^ y)' ^ ((z ^ x')' ^ (x' ^ u)')' = ((z ^ x')' ^ (x' ^ u)')'. [para(1255(a,1),1390(a,1,1,1,1))]. given #257 (F,wt=13): 2660 x' ^ (y ^ (z ^ (u ^ x))) = c_0'. [para(1910(a,1),2613(a,1,2)),rewrite(1167(5),1745(5))]. given #258 (F,wt=13): 2685 (x ^ y) ^ ((y ^ x)' ^ z) = c_0'. [para(2615(a,1),1738(a,1,1)),rewrite(1618(8)),flip(a)]. given #259 (T,wt=13): 2688 (x ^ y)' ^ ((y ^ x) ^ z) = c_0'. [para(1717(a,1),2616(a,1,2,1))]. given #260 (T,wt=13): 2689 (x' ^ y) ^ ((x ^ z) ^ u) = c_0'. [para(1426(a,1),2616(a,1,2,1)),rewrite(1167(4))]. given #261 (A,wt=27): 1435 (x' ^ y)' ^ ((x ^ z)' ^ (x ^ u)')' = ((x ^ z)' ^ (x ^ u)')'. [para(1259(a,1),1390(a,1,1,1,1))]. given #262 (F,wt=13): 2690 (x' ^ y) ^ ((z ^ x) ^ u) = c_0'. [para(1432(a,1),2616(a,1,2,1)),rewrite(1167(4))]. given #263 (F,wt=13): 2691 (x ^ y') ^ ((y ^ z) ^ u) = c_0'. [para(1470(a,1),2616(a,1,2,1)),rewrite(1167(4))]. given #264 (T,wt=13): 2692 (x ^ y') ^ ((z ^ y) ^ u) = c_0'. [para(1476(a,1),2616(a,1,2,1)),rewrite(1167(4))]. given #265 (T,wt=13): 2695 (x ^ y) ^ ((x' ^ z) ^ u) = c_0'. [para(1427(a,1),2616(a,1,2,1)),rewrite(1167(3))]. given #266 (A,wt=30): 1436 (x ^ y)' ^ ((x' ^ z)' ^ (x' ^ u)')' = ((x' ^ z)' ^ (x' ^ u)')'. [para(1276(a,1),1390(a,1,1,1,1))]. given #267 (F,wt=13): 2696 (x ^ y) ^ ((z ^ x') ^ u) = c_0'. [para(1434(a,1),2616(a,1,2,1)),rewrite(1167(3))]. given #268 (F,wt=13): 2697 (x ^ y) ^ ((y' ^ z) ^ u) = c_0'. [para(1471(a,1),2616(a,1,2,1)),rewrite(1167(3))]. given #269 (T,wt=13): 2698 (x ^ y) ^ ((z ^ y') ^ u) = c_0'. [para(1477(a,1),2616(a,1,2,1)),rewrite(1167(3))]. given #270 (T,wt=13): 2701 ((x ^ y) ^ z) ^ (x' ^ u) = c_0'. [para(2616(a,1),1738(a,1,1)),rewrite(1618(8)),flip(a)]. given #271 (A,wt=27): 1437 (x' ^ y)' ^ ((z ^ x)' ^ (u ^ x)')' = ((z ^ x)' ^ (u ^ x)')'. [para(1293(a,1),1390(a,1,1,1,1))]. given #272 (F,wt=13): 2707 ((x' ^ y) ^ z) ^ (x ^ u) = c_0'. [para(1439(a,1),2617(a,1,2,1)),rewrite(1167(5))]. given #273 (F,wt=13): 2708 ((x ^ y') ^ z) ^ (y ^ u) = c_0'. [para(1455(a,1),2617(a,1,2,1)),rewrite(1167(5))]. given #274 (T,wt=13): 2709 (x ^ (y' ^ z)) ^ (y ^ u) = c_0'. [para(1456(a,1),2617(a,1,2,1)),rewrite(1167(5))]. given #275 (T,wt=13): 2710 (x ^ (y ^ z')) ^ (z ^ u) = c_0'. [para(1492(a,1),2617(a,1,2,1)),rewrite(1167(5))]. given #276 (A,wt=17): 1438 (x' ^ y)' ^ ((x ^ z) ^ u) = (x ^ z) ^ u. [para(1390(a,1),1390(a,1,1,1,1)),rewrite(1167(7),1167(10))]. given #277 (F,wt=13): 2711 ((x ^ y) ^ z) ^ (y' ^ u) = c_0'. [para(1489(a,1),2617(a,1,2,1)),rewrite(1167(4))]. given #278 (F,wt=13): 2712 (x ^ (y ^ z)) ^ (y' ^ u) = c_0'. [para(1497(a,1),2617(a,1,2,1)),rewrite(1167(4))]. given #279 (T,wt=13): 2714 (x ^ (y ^ z)) ^ (z' ^ u) = c_0'. [para(1525(a,1),2617(a,1,2,1)),rewrite(1167(4))]. given #280 (T,wt=13): 2743 ((x' ^ y) ^ z) ^ (u ^ x) = c_0'. [para(1432(a,1),2618(a,1,2)),rewrite(1167(4))]. given #281 (A,wt=18): 1443 (x ^ y)' ^ ((x' ^ z) ^ u) = (x' ^ z) ^ u. [para(1425(a,1),1390(a,1,1,1,1)),rewrite(1167(7),1167(11))]. given #282 (F,wt=13): 2744 ((x ^ y') ^ z) ^ (u ^ y) = c_0'. [para(1476(a,1),2618(a,1,2)),rewrite(1167(4))]. given #283 (F,wt=13): 2745 (x' ^ y) ^ (z ^ (x ^ u)) = c_0'. [para(1558(a,1),2618(a,1,2))]. given #284 (T,wt=13): 2746 (x' ^ y) ^ (z ^ (u ^ x)) = c_0'. [para(1696(a,1),2618(a,1,2))]. given #285 (T,wt=13): 2748 ((x ^ y) ^ z) ^ (u ^ x') = c_0'. [para(1434(a,1),2618(a,1,2)),rewrite(1167(3))]. given #286 (A,wt=17): 1460 ((x ^ y) ^ z) ^ (x' ^ u)' = (x ^ y) ^ z. [para(1390(a,1),1439(a,1,2,1,1))]. given #287 (F,wt=13): 2749 ((x ^ y) ^ z) ^ (u ^ y') = c_0'. [para(1477(a,1),2618(a,1,2)),rewrite(1167(3))]. given #288 (F,wt=13): 2767 (x ^ y) ^ (z ^ (x' ^ u)) = c_0'. [para(1426(a,1),2619(a,1,1))]. given #289 (T,wt=13): 2768 (x ^ y) ^ (z ^ (y' ^ u)) = c_0'. [para(1432(a,1),2619(a,1,1))]. given #290 (T,wt=13): 2770 (x ^ y) ^ (z ^ (u ^ x')) = c_0'. [para(1470(a,1),2619(a,1,1))]. given #291 (A,wt=18): 1461 ((x' ^ y) ^ z) ^ (x ^ u)' = (x' ^ y) ^ z. [para(1425(a,1),1439(a,1,2,1,1))]. given #292 (F,wt=13): 2771 (x ^ y) ^ (z ^ (u ^ y')) = c_0'. [para(1476(a,1),2619(a,1,1))]. given #293 (F,wt=13): 2773 (x ^ (y' ^ z)) ^ (u ^ y) = c_0'. [para(1558(a,1),2619(a,1,1))]. given #294 (T,wt=13): 2774 (x ^ (y ^ z')) ^ (u ^ z) = c_0'. [para(1696(a,1),2619(a,1,1))]. given #295 (T,wt=13): 2785 (x ^ y') ^ (z ^ (y ^ u)) = c_0'. [para(1434(a,1),2619(a,1,1))]. given #296 (A,wt=18): 1466 (x ^ y)' ^ ((z ^ x') ^ u) = (z ^ x') ^ u. [para(1440(a,1),1390(a,1,1,1,1)),rewrite(1167(7),1167(11))]. given #297 (F,wt=13): 2787 (x ^ y') ^ (z ^ (u ^ y)) = c_0'. [para(1477(a,1),2619(a,1,1))]. given #298 (F,wt=13): 2789 (x ^ y)' ^ (z ^ (y ^ x)) = c_0'. [para(1743(a,1),2619(a,1,1))]. given #299 (T,wt=13): 2804 (x ^ (y ^ z)') ^ (z ^ y) = c_0'. [para(1717(a,1),2620(a,1,2))]. given #300 (T,wt=13): 2806 (x ^ (y ^ z)) ^ (u ^ y') = c_0'. [para(1434(a,1),2620(a,1,2)),rewrite(1167(3))]. given #301 (A,wt=18): 1468 ((x ^ y') ^ z) ^ (y ^ u)' = (x ^ y') ^ z. [para(1440(a,1),1439(a,1,2,1,1))]. given #302 (F,wt=13): 2807 (x ^ (y ^ z)) ^ (u ^ z') = c_0'. [para(1477(a,1),2620(a,1,2)),rewrite(1167(3))]. given #303 (F,wt=13): 2808 (x ^ (y ^ z)) ^ (z ^ y)' = c_0'. [para(1743(a,1),2620(a,1,2)),rewrite(1167(3))]. given #304 (T,wt=13): 2841 (x ^ y) ^ (z ^ (y ^ x)') = c_0'. [para(1743(a,1),2623(a,1,2,2)),rewrite(1167(3))]. given #305 (T,wt=13): 2969 (x ^ (x ^ y)') ^ (y ^ z) = c_0'. [para(2967(a,1),1738(a,1,1)),rewrite(1618(8)),flip(a)]. given #306 (A,wt=18): 1483 (x ^ y)' ^ (z ^ (x' ^ u)) = z ^ (x' ^ u). [para(1441(a,1),1390(a,1,1,1,1)),rewrite(1167(7),1167(11))]. given #307 (F,wt=13): 2970 (x ^ (y ^ x)') ^ (y ^ z) = c_0'. [para(2968(a,1),1738(a,1,1)),rewrite(1618(8)),flip(a)]. given #308 (F,wt=13): 3071 (x ^ y)' ^ (y ^ (z ^ x)) = c_0'. [para(1280(a,1),2632(a,1,2,2))]. given #309 (T,wt=13): 3073 (x ^ (y ^ z)) ^ (y ^ x)' = c_0'. [para(2632(a,1),1717(a,1,1)),rewrite(1618(8)),flip(a)]. given #310 (T,wt=13): 3075 (x ^ y)' ^ (x ^ (y ^ z)) = c_0'. [para(1745(a,1),2632(a,1,1,1))]. given #311 (A,wt=17): 1484 (x ^ y')' ^ ((y ^ z) ^ u) = (y ^ z) ^ u. [para(1390(a,1),1441(a,1,1,1,2))]. given #312 (F,wt=13): 3076 (x ^ y)' ^ ((x ^ z) ^ y) = c_0'. [para(1745(a,1),2632(a,1,2))]. given #313 (F,wt=13): 3087 (x ^ y)' ^ (x ^ (z ^ y)) = c_0'. [para(1696(a,1),2632(a,1,2))]. given #314 (T,wt=13): 3300 x ^ (y ^ ((y ^ x)' ^ z)) = c_0'. [para(2649(a,1),1738(a,1)),flip(a)]. given #315 (T,wt=13): 3399 x ^ (y ^ (z ^ (y ^ x)')) = c_0'. [para(2650(a,1),1738(a,1)),flip(a)]. given #316 (A,wt=18): 1485 (x ^ y)' ^ ((y' ^ z) ^ u) = (y' ^ z) ^ u. [para(1425(a,1),1441(a,1,1,1,2))]. given #317 (F,wt=13): 4671 (x ^ (x ^ y)') ^ (z ^ y) = c_0'. [para(1280(a,1),2969(a,1,2))]. given #318 (F,wt=13): 4673 (x ^ y) ^ (z ^ (z ^ x)') = c_0'. [para(2969(a,1),1717(a,1,1)),rewrite(1618(8)),flip(a)]. given #319 (T,wt=13): 4681 x ^ ((y ^ (y ^ x)') ^ z) = c_0'. [para(2969(a,1),1558(a,1)),flip(a)]. given #320 (T,wt=13): 4683 x ^ (y ^ (z ^ (z ^ x)')) = c_0'. [para(2969(a,1),1696(a,1)),flip(a)]. given #321 (A,wt=18): 1486 (x ^ (y' ^ z)) ^ (y ^ u)' = x ^ (y' ^ z). [para(1441(a,1),1439(a,1,2,1,1))]. given #322 (F,wt=13): 4694 x ^ ((y ^ (x ^ y)') ^ z) = c_0'. [para(2968(a,1),2969(a,1,1,2,1)),rewrite(1167(3),1606(2))]. given #323 (F,wt=13): 4771 (x ^ (y ^ x)') ^ (z ^ y) = c_0'. [para(1280(a,1),2970(a,1,2))]. given #324 (T,wt=13): 4773 (x ^ y) ^ (z ^ (x ^ z)') = c_0'. [para(2970(a,1),1717(a,1,1)),rewrite(1618(8)),flip(a)]. given #325 (T,wt=13): 4782 x ^ (y ^ (z ^ (x ^ z)')) = c_0'. [para(2970(a,1),1696(a,1)),flip(a)]. given #326 (A,wt=18): 1487 (x ^ y)' ^ ((z ^ y') ^ u) = (z ^ y') ^ u. [para(1440(a,1),1441(a,1,1,1,2))]. given #327 (F,wt=13): 4819 (x ^ (y ^ z)) ^ (z ^ x)' = c_0'. [para(3071(a,1),1717(a,1,1)),rewrite(1618(8)),flip(a)]. given #328 (F,wt=13): 4820 (x ^ y)' ^ ((z ^ x) ^ y) = c_0'. [para(1745(a,1),3071(a,1,2))]. given #329 (T,wt=13): 4821 (x ^ y)' ^ ((y ^ z) ^ x) = c_0'. [para(1392(a,1),3071(a,1,2))]. given #330 (T,wt=13): 4822 (x ^ y)' ^ ((z ^ y) ^ x) = c_0'. [para(1414(a,1),3071(a,1,2))]. given #331 (A,wt=18): 1488 (x ^ y)' ^ (z ^ (y' ^ u)) = z ^ (y' ^ u). [para(1441(a,1),1441(a,1,1,1,2))]. given #332 (F,wt=13): 5106 x ^ (y ^ ((x ^ y)' ^ z)) = c_0'. [para(1745(a,1),3300(a,1,2,2,1,1))]. given #333 (F,wt=13): 5112 x ^ ((y ^ x)' ^ (y ^ z)) = c_0'. [para(1558(a,1),3300(a,1,2))]. given #334 (T,wt=13): 5114 x ^ ((y ^ x)' ^ (z ^ y)) = c_0'. [para(1696(a,1),3300(a,1,2))]. given #335 (T,wt=13): 5126 x ^ (y ^ (z ^ (x ^ y)')) = c_0'. [para(1745(a,1),3399(a,1,2,2,2,1))]. given #336 (A,wt=17): 1506 ((x ^ y) ^ z) ^ (u ^ x')' = (x ^ y) ^ z. [para(1390(a,1),1456(a,1,2,1,2))]. given #337 (F,wt=13): 5127 x ^ ((y ^ z) ^ (y ^ x)') = c_0'. [para(1392(a,1),3399(a,1,2))]. given #338 (F,wt=13): 5128 x ^ ((y ^ z) ^ (z ^ x)') = c_0'. [para(1414(a,1),3399(a,1,2))]. given #339 (T,wt=13): 5214 (x ^ y) ^ (z ^ (z ^ y)') = c_0'. [para(4671(a,1),1717(a,1,1)),rewrite(1618(8)),flip(a)]. given #340 (T,wt=13): 5320 x ^ ((x ^ y)' ^ (y ^ z)) = c_0'. [para(1738(a,1),4694(a,1,2))]. given #341 (A,wt=18): 1507 ((x' ^ y) ^ z) ^ (u ^ x)' = (x' ^ y) ^ z. [para(1425(a,1),1456(a,1,2,1,2))]. given #342 (F,wt=13): 5335 (x ^ y) ^ (z ^ (y ^ z)') = c_0'. [para(4771(a,1),1717(a,1,1)),rewrite(1618(8)),flip(a)]. given #343 (F,wt=13): 5503 ((x ^ y) ^ z) ^ (z ^ x)' = c_0'. [para(1392(a,1),4819(a,1,1))]. given #344 (T,wt=13): 5504 ((x ^ y) ^ z) ^ (z ^ y)' = c_0'. [para(1414(a,1),4819(a,1,1))]. given #345 (T,wt=13): 5810 x ^ ((x ^ y)' ^ (z ^ y)) = c_0'. [para(1696(a,1),5106(a,1,2))]. given #346 (A,wt=18): 1508 ((x ^ y') ^ z) ^ (u ^ y)' = (x ^ y') ^ z. [para(1440(a,1),1456(a,1,2,1,2))]. given #347 (F,wt=13): 5907 x ^ ((y ^ z) ^ (x ^ y)') = c_0'. [para(1392(a,1),5126(a,1,2))]. given #348 (F,wt=13): 5908 x ^ ((y ^ z) ^ (x ^ z)') = c_0'. [para(1414(a,1),5126(a,1,2))]. given #349 (T,wt=15): 1741 (x ^ y) ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(1525(a,1),1256(a,1,1,1,1)),rewrite(1167(2))]. given #350 (T,wt=13): 6263 (x ^ y) ^ (x ^ z) = z ^ (x ^ y). [para(1738(a,1),1741(a,1,2)),rewrite(6213(6),1738(7))]. ============================== PROOF ================================= % Proof 3 at 3.67 (+ 0.04) seconds: combined. % Length of proof is 117. % Level of proof is 27. % Maximum clause weight is 39. % Given clauses 350. 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). [goal]. 5 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z))) = y # label(OL_Sh). [assumption]. 6 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 7 f(f(x,x),f(y,y)) = x v y. [copy(6),flip(a)]. 8 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. 9 f(f(x,y),f(x,y)) = x ^ y. [copy(8),flip(a)]. 10 x' = f(x,x) # label(definition_complementation). [assumption]. 11 f(x,x) = x'. [copy(10),flip(a)]. 18 f(c8,f(f(c9,c10),f(c9,c10))) != f(c9,f(f(c8,c10),f(c8,c10))) | f(f(c8,c8),f(c8,c9)) != c8 | f(c8,f(c8,c8)) != f(c9,f(c9,c9)) # answer(combined). [deny(4)]. 19 f(c9,f(c8,c10)') != f(c8,f(c9,c10)') | f(c8',f(c8,c9)) != c8 | f(c9,c9') != f(c8,c8') # answer(combined). [copy(18),rewrite(11(8),11(14),11(16),11(25),11(29)),flip(a),flip(c)]. 20 f(x,y)' = x ^ y. [back_rewrite(9),rewrite(11(3))]. 21 f(x',y') = x v y. [back_rewrite(7),rewrite(11(1),11(2))]. 22 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(x',x)),z))) = y. [back_rewrite(5),rewrite(11(5))]. 23 f(c9,c8 ^ c10) != f(c8,c9 ^ c10) | f(c8',f(c8,c9)) != c8 | f(c9,c9') != f(c8,c8') # answer(combined). [back_rewrite(19),rewrite(20(5),20(10))]. 25 x ^ x = x''. [para(11(a,1),20(a,1,1)),flip(a)]. 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))]. 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))]. 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))]. 42 f(x,f(f(x,y),f(f(f(x,y),f(z ^ x,f(z,x))),u))) = f(x,y). [para(22(a,1),22(a,1,1)),rewrite(20(4))]. 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)]. 199 (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)]. 230 x ^ f(x',f(f(x',x' v x),y)) = x''. [para(190(a,1),20(a,1,1)),flip(a)]. 236 f(x',f(x'',x)) = x''. [para(32(a,1),190(a,1,2,2))]. 240 f(x'',x'' v x) = x'''. [para(21(a,1),236(a,1,2))]. 337 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))]. 752 f(f(x,y),f(y,f(f(y,f(x',x)),z))) = y. [para(41(a,1),22(a,1,1))]. 763 f(x,y) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(41(a,1),36(a,1,1))]. 764 x ^ x'' = x''. [para(41(a,1),230(a,1,2,2)),rewrite(11(3))]. 857 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),42(a,1,2,2))]. 882 f(x,x ^ y) = f(x,y). [para(41(a,1),42(a,1,2,2)),rewrite(11(3),20(2))]. 995 x ^ (x ^ y) = x ^ y. [para(882(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. 999 f(f(f(f(x,y),f(y,z)),u),y') = y. [para(22(a,1),882(a,2)),rewrite(36(14))]. 1010 x'' v x = x. [para(181(a,1),882(a,2)),rewrite(192(12),21(5))]. 1019 f(x'',x) = x'''. [para(240(a,1),882(a,2)),rewrite(1010(7),882(6))]. 1040 f(f(x,y),x') = x. [para(41(a,1),882(a,2)),rewrite(337(17))]. 1078 f(x,y) = (x ^ y)'''. [para(1010(a,1),29(a,2)),rewrite(20(2),1019(5)),flip(a)]. 1088 ((x ^ y)''' ^ x')''' = x. [back_rewrite(1040),rewrite(1078(1),1078(6))]. 1103 ((((x ^ y)''' ^ (y ^ z)''')''' ^ u)''' ^ y')''' = y. [back_rewrite(999),rewrite(1078(1),1078(5),1078(9),1078(13),1078(18))]. 1124 (x' ^ ((x' ^ (x ^ y)''')''' ^ x)''')''' = (x' ^ (x ^ y)''')'''. [back_rewrite(857),rewrite(1078(3),1078(7),1078(11),1078(15),1078(20),1078(24))]. 1143 (x ^ y)''' ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(763),rewrite(1078(1),1078(6),1078(10),1078(14),1078(18))]. 1145 x'''' = x. [back_rewrite(752),rewrite(1078(1),1078(6),1078(10),1078(14),1078(18),1078(22),1143(22))]. 1155 ((x ^ y)''' ^ (y ^ z)''') ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(199),rewrite(1078(1),1078(5),1078(11),1078(15),1078(19),1078(23))]. 1159 (c9 ^ (c8 ^ c10))''' != (c8 ^ (c9 ^ c10))''' | (c8' ^ (c8 ^ c9)''')''' != c8 | (c9 ^ c9')''' != (c8 ^ c8')''' # answer(combined). [back_rewrite(23),rewrite(1078(5),1078(13),1078(22),1078(26),1078(35),1078(42))]. 1167 x'' = x. [para(25(a,1),1088(a,1,1,1,1,1,1,1,1)),rewrite(1145(4),25(3),1145(4))]. 1170 (x ^ y)' ^ x' = x'. [para(1088(a,1),764(a,2,1)),rewrite(1167(3),1167(6),1167(7),1167(10),1167(10),25(9),1167(6))]. 1171 ((x' ^ y)' ^ x)' = x'. [para(1145(a,1),1088(a,1,1,1,1,2)),rewrite(1167(2),1167(4),1167(6),1167(7))]. 1176 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' | (c8' ^ (c8 ^ c9)')' != c8 | (c9 ^ c9')' != (c8 ^ c8')' # answer(combined). [back_rewrite(1159),rewrite(1167(7),1167(13),1167(20),1167(22),1167(29),1167(34))]. 1180 ((x ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1155),rewrite(1167(3),1167(5),1167(9),1167(11),1167(13),1167(15))]. 1187 (x ^ y)' ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1143),rewrite(1167(3),1167(6),1167(8),1167(10),1167(12))]. 1188 (x' ^ (x ^ y)')' = x. [back_rewrite(1124),rewrite(1167(5),1167(7),1171(8),1167(3),25(3),1167(2),1167(2),1167(2),1167(4),1167(6)),flip(a)]. 1198 ((((x ^ y)' ^ (y ^ z)')' ^ u)' ^ y')' = y. [back_rewrite(1103),rewrite(1167(3),1167(5),1167(7),1167(9),1167(12))]. 1206 x ^ x = x. [back_rewrite(25),rewrite(1167(3))]. 1207 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' | (c9 ^ c9')' != (c8 ^ c8')' # answer(combined). [back_rewrite(1176),rewrite(1188(21)),xx(b)]. 1209 (x' ^ y)' ^ x = x. [para(1167(a,1),1170(a,1,2)),rewrite(1167(6))]. 1210 x' ^ (x ^ y)' = x'. [para(1188(a,1),1167(a,1,1)),flip(a)]. 1213 ((x ^ y)' ^ (y ^ z)') ^ y' = y'. [para(1180(a,1),995(a,1,2)),rewrite(1180(22))]. 1218 ((x ^ y)' ^ (y ^ (y ^ (x' ^ x)')')') ^ (y ^ (x' ^ x)')' = y'. [para(1206(a,1),1180(a,1,2,1,2,1)),rewrite(1167(16),995(15))]. 1219 x ^ ((y ^ x)' ^ (x ^ z)')' = ((y ^ x)' ^ (x ^ z)')'. [para(1180(a,1),1170(a,1,1,1)),rewrite(1167(2))]. 1225 x ^ (x' ^ y)' = x. [para(1167(a,1),1210(a,1,1)),rewrite(1167(6))]. 1226 (x ^ y) ^ x = x ^ y. [para(1170(a,1),1210(a,1,2,1)),rewrite(1167(3),1167(3),1167(5))]. 1235 x' ^ ((y ^ x)' ^ (x ^ z)') = x'. [para(1180(a,1),1226(a,1,1)),rewrite(1180(22))]. 1256 ((x ^ (y ^ z)')' ^ y) ^ (y ^ z) = y ^ z. [para(1170(a,1),1213(a,1,1,2,1)),rewrite(1167(6),1167(8),1167(10))]. 1269 x' ^ ((x ^ y)' ^ (x ^ z)') = x'. [para(1226(a,1),1235(a,1,2,1,1))]. 1277 (x ^ y)' ^ y' = y'. [para(1187(a,1),995(a,1,2)),rewrite(1187(16))]. 1280 x ^ (y ^ x) = y ^ x. [para(1187(a,1),1170(a,1,1,1)),rewrite(1167(2),1167(3),1167(5))]. 1282 (x ^ y')' ^ y = y. [para(1209(a,1),1187(a,1,2,1,2,1)),rewrite(1206(6),1167(5),1167(6))]. 1284 x' ^ (y ^ x)' = x'. [para(1187(a,1),1226(a,1,1)),rewrite(1187(16))]. 1290 x ^ (y ^ x')' = x. [para(1280(a,1),1225(a,1,2,1))]. 1373 (((x ^ y) ^ z)' ^ x')' = x. [para(1170(a,1),1198(a,1,1,1,1,1,1)),rewrite(1167(3))]. 1383 (((x ^ y) ^ z)' ^ y')' = y. [para(1290(a,1),1198(a,1,1,1,1,1,1)),rewrite(1167(3))]. 1390 ((x ^ y) ^ z)' ^ x' = x'. [para(1373(a,1),1167(a,1,1)),flip(a)]. 1408 ((x ^ y) ^ z) ^ (x ^ (((x ^ y) ^ z)' ^ u)') = (x ^ y) ^ z. [para(1373(a,1),1269(a,1,2,1)),rewrite(1167(4),1167(13))]. 1423 ((x ^ y) ^ z) ^ (y ^ (((x ^ y) ^ z)' ^ u)') = (x ^ y) ^ z. [para(1383(a,1),1269(a,1,2,1)),rewrite(1167(4),1167(13))]. 1425 ((x' ^ y) ^ z)' ^ x = x. [para(1167(a,1),1390(a,1,2)),rewrite(1167(7))]. 1433 (x ^ (y ^ z))' ^ y' = y'. [para(1280(a,1),1390(a,1,1,1))]. 1439 x ^ ((x' ^ y) ^ z)' = x. [para(1425(a,1),1226(a,1,1)),rewrite(1425(10))]. 1440 ((x ^ y') ^ z)' ^ y = y. [para(1280(a,1),1425(a,1,1,1,1))]. 1441 (x ^ (y' ^ z))' ^ y = y. [para(1280(a,1),1425(a,1,1,1))]. 1455 x ^ ((y ^ x') ^ z)' = x. [para(1280(a,1),1439(a,1,2,1,1))]. 1456 x ^ (y ^ (x' ^ z))' = x. [para(1280(a,1),1439(a,1,2,1))]. 1464 (x ^ (y ^ z'))' ^ z = z. [para(1280(a,1),1440(a,1,1,1))]. 1485 (x ^ y)' ^ ((y' ^ z) ^ u) = (y' ^ z) ^ u. [para(1425(a,1),1441(a,1,1,1,2))]. 1488 (x ^ y)' ^ (z ^ (y' ^ u)) = z ^ (y' ^ u). [para(1441(a,1),1441(a,1,1,1,2))]. 1492 x ^ (y ^ (z ^ x'))' = x. [para(1280(a,1),1455(a,1,2,1))]. 1497 x' ^ (y ^ (x ^ z))' = x'. [para(1167(a,1),1456(a,1,2,1,2,1))]. 1510 (x ^ (y ^ z))' ^ z' = z'. [para(1167(a,1),1464(a,1,1,1,2,2))]. 1525 x' ^ (y ^ (z ^ x))' = x'. [para(1167(a,1),1492(a,1,2,1,2,2))]. 1558 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(1433(a,1),1170(a,1,1,1)),rewrite(1167(2),1167(4),1167(7))]. 1587 (x' ^ x) ^ y = x' ^ x. [para(1170(a,1),1218(a,1,1,2,1,2,1)),rewrite(1439(5),1167(9),1525(10),1170(9),1167(5),995(4),1167(7)),flip(a)]. 1589 x ^ (y' ^ y) = y' ^ y. [para(1282(a,1),1218(a,1,1,2,1,2,1)),rewrite(1167(4),1456(5),1167(5),1167(9),1525(10),1167(5),1277(9),1167(5),995(4),1167(6),1167(7)),flip(a)]. 1598 (x' ^ x)' ^ y = y. [para(1587(a,1),1282(a,1,1,1))]. 1599 x ^ (y' ^ y)' = x. [para(1587(a,1),1290(a,1,2,1))]. 1604 (x' ^ x)' = (y' ^ y)'. [para(1599(a,1),1598(a,1))]. 1605 (x' ^ x)' = c_0. [new_symbol(1604)]. 1663 x' ^ x = c_0'. [para(1219(a,1),1587(a,1)),rewrite(1589(3),1605(3),1587(4),1605(4),1206(3)),flip(a)]. 1668 x ^ x' = c_0'. [para(1167(a,1),1663(a,1,1))]. 1669 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' # answer(combined). [back_rewrite(1207),rewrite(1668(17),1167(16),1668(18),1167(17)),xx(b)]. 1696 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(1510(a,1),1170(a,1,1,1)),rewrite(1167(2),1167(4),1167(7))]. 1717 (x ^ y) ^ (y ^ x) = y ^ x. [para(1284(a,1),1256(a,1,1,1,1)),rewrite(1167(2))]. 1738 (x ^ y) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(1497(a,1),1256(a,1,1,1,1)),rewrite(1167(2))]. 1741 (x ^ y) ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(1525(a,1),1256(a,1,1,1,1)),rewrite(1167(2))]. 1745 x ^ y = y ^ x. [para(1717(a,1),1226(a,1,1)),rewrite(1717(3),1717(4))]. 2578 (x ^ y) ^ (x ^ (z ^ y)) = x ^ (z ^ y). [para(1696(a,1),1738(a,1,2)),rewrite(1696(7))]. 5169 ((x ^ y) ^ z) ^ (y ^ ((z' ^ u) ^ v)') = (x ^ y) ^ z. [para(1485(a,1),1423(a,1,2,2,1))]. 5756 ((x ^ y) ^ z) ^ (x ^ (u ^ (z' ^ v))') = (x ^ y) ^ z. [para(1488(a,1),1408(a,1,2,2,1))]. 6213 (x ^ (y ^ z)) ^ (z ^ x) = x ^ (y ^ z). [para(1741(a,1),1717(a,1,2)),rewrite(1745(7),995(7),1741(8))]. 6263 (x ^ y) ^ (x ^ z) = z ^ (x ^ y). [para(1738(a,1),1741(a,1,2)),rewrite(6213(6),1738(7))]. 6338 (x ^ y) ^ (x ^ z) = (x ^ y) ^ z. [para(6263(a,2),1717(a,1,1)),rewrite(1745(6),2578(6))]. 6340 (x ^ y) ^ z = y ^ (x ^ z). [para(6263(a,1),1745(a,1)),rewrite(6338(5)),flip(a)]. 6655 x ^ (y ^ (z ^ (u ^ (x' ^ v))')) = y ^ (z ^ x). [back_rewrite(5756),rewrite(6340(2),6340(8),6340(8),1558(7),6340(9))]. 6765 x ^ (y ^ z) = y ^ (x ^ z). [back_rewrite(5169),rewrite(6340(2),6340(5),6340(8),995(7),6340(7),6655(7),6340(4))]. 7288 $F # answer(combined). [back_rewrite(1669),rewrite(6765(5)),xx(a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 4 at 3.67 (+ 0.04) seconds: assoc. % Length of proof is 101. % Level of proof is 27. % Maximum clause weight is 39. % Given clauses 350. 1 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(assoc). [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)]. 12 f(c1,f(f(c2,c3),f(c2,c3))) != f(c2,f(f(c1,c3),f(c1,c3))) # answer(assoc). [deny(1)]. 13 f(c2,f(c1,c3)') != f(c1,f(c2,c3)') # answer(assoc). [copy(12),rewrite(11(8),11(14)),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))]. 24 f(c2,c1 ^ c3) != f(c1,c2 ^ c3) # answer(assoc). [back_rewrite(13),rewrite(20(5),20(10))]. 25 x ^ x = x''. [para(11(a,1),20(a,1,1)),flip(a)]. 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))]. 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))]. 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))]. 42 f(x,f(f(x,y),f(f(f(x,y),f(z ^ x,f(z,x))),u))) = f(x,y). [para(22(a,1),22(a,1,1)),rewrite(20(4))]. 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)]. 199 (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)]. 230 x ^ f(x',f(f(x',x' v x),y)) = x''. [para(190(a,1),20(a,1,1)),flip(a)]. 236 f(x',f(x'',x)) = x''. [para(32(a,1),190(a,1,2,2))]. 240 f(x'',x'' v x) = x'''. [para(21(a,1),236(a,1,2))]. 337 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))]. 752 f(f(x,y),f(y,f(f(y,f(x',x)),z))) = y. [para(41(a,1),22(a,1,1))]. 763 f(x,y) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(41(a,1),36(a,1,1))]. 764 x ^ x'' = x''. [para(41(a,1),230(a,1,2,2)),rewrite(11(3))]. 857 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),42(a,1,2,2))]. 882 f(x,x ^ y) = f(x,y). [para(41(a,1),42(a,1,2,2)),rewrite(11(3),20(2))]. 995 x ^ (x ^ y) = x ^ y. [para(882(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. 999 f(f(f(f(x,y),f(y,z)),u),y') = y. [para(22(a,1),882(a,2)),rewrite(36(14))]. 1010 x'' v x = x. [para(181(a,1),882(a,2)),rewrite(192(12),21(5))]. 1019 f(x'',x) = x'''. [para(240(a,1),882(a,2)),rewrite(1010(7),882(6))]. 1040 f(f(x,y),x') = x. [para(41(a,1),882(a,2)),rewrite(337(17))]. 1078 f(x,y) = (x ^ y)'''. [para(1010(a,1),29(a,2)),rewrite(20(2),1019(5)),flip(a)]. 1088 ((x ^ y)''' ^ x')''' = x. [back_rewrite(1040),rewrite(1078(1),1078(6))]. 1103 ((((x ^ y)''' ^ (y ^ z)''')''' ^ u)''' ^ y')''' = y. [back_rewrite(999),rewrite(1078(1),1078(5),1078(9),1078(13),1078(18))]. 1124 (x' ^ ((x' ^ (x ^ y)''')''' ^ x)''')''' = (x' ^ (x ^ y)''')'''. [back_rewrite(857),rewrite(1078(3),1078(7),1078(11),1078(15),1078(20),1078(24))]. 1143 (x ^ y)''' ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(763),rewrite(1078(1),1078(6),1078(10),1078(14),1078(18))]. 1145 x'''' = x. [back_rewrite(752),rewrite(1078(1),1078(6),1078(10),1078(14),1078(18),1078(22),1143(22))]. 1155 ((x ^ y)''' ^ (y ^ z)''') ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(199),rewrite(1078(1),1078(5),1078(11),1078(15),1078(19),1078(23))]. 1158 (c2 ^ (c1 ^ c3))''' != (c1 ^ (c2 ^ c3))''' # answer(assoc). [back_rewrite(24),rewrite(1078(5),1078(13))]. 1167 x'' = x. [para(25(a,1),1088(a,1,1,1,1,1,1,1,1)),rewrite(1145(4),25(3),1145(4))]. 1170 (x ^ y)' ^ x' = x'. [para(1088(a,1),764(a,2,1)),rewrite(1167(3),1167(6),1167(7),1167(10),1167(10),25(9),1167(6))]. 1171 ((x' ^ y)' ^ x)' = x'. [para(1145(a,1),1088(a,1,1,1,1,2)),rewrite(1167(2),1167(4),1167(6),1167(7))]. 1177 (c2 ^ (c1 ^ c3))' != (c1 ^ (c2 ^ c3))' # answer(assoc). [back_rewrite(1158),rewrite(1167(7),1167(13))]. 1180 ((x ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1155),rewrite(1167(3),1167(5),1167(9),1167(11),1167(13),1167(15))]. 1187 (x ^ y)' ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1143),rewrite(1167(3),1167(6),1167(8),1167(10),1167(12))]. 1188 (x' ^ (x ^ y)')' = x. [back_rewrite(1124),rewrite(1167(5),1167(7),1171(8),1167(3),25(3),1167(2),1167(2),1167(2),1167(4),1167(6)),flip(a)]. 1198 ((((x ^ y)' ^ (y ^ z)')' ^ u)' ^ y')' = y. [back_rewrite(1103),rewrite(1167(3),1167(5),1167(7),1167(9),1167(12))]. 1210 x' ^ (x ^ y)' = x'. [para(1188(a,1),1167(a,1,1)),flip(a)]. 1213 ((x ^ y)' ^ (y ^ z)') ^ y' = y'. [para(1180(a,1),995(a,1,2)),rewrite(1180(22))]. 1225 x ^ (x' ^ y)' = x. [para(1167(a,1),1210(a,1,1)),rewrite(1167(6))]. 1226 (x ^ y) ^ x = x ^ y. [para(1170(a,1),1210(a,1,2,1)),rewrite(1167(3),1167(3),1167(5))]. 1235 x' ^ ((y ^ x)' ^ (x ^ z)') = x'. [para(1180(a,1),1226(a,1,1)),rewrite(1180(22))]. 1256 ((x ^ (y ^ z)')' ^ y) ^ (y ^ z) = y ^ z. [para(1170(a,1),1213(a,1,1,2,1)),rewrite(1167(6),1167(8),1167(10))]. 1269 x' ^ ((x ^ y)' ^ (x ^ z)') = x'. [para(1226(a,1),1235(a,1,2,1,1))]. 1280 x ^ (y ^ x) = y ^ x. [para(1187(a,1),1170(a,1,1,1)),rewrite(1167(2),1167(3),1167(5))]. 1284 x' ^ (y ^ x)' = x'. [para(1187(a,1),1226(a,1,1)),rewrite(1187(16))]. 1290 x ^ (y ^ x')' = x. [para(1280(a,1),1225(a,1,2,1))]. 1373 (((x ^ y) ^ z)' ^ x')' = x. [para(1170(a,1),1198(a,1,1,1,1,1,1)),rewrite(1167(3))]. 1383 (((x ^ y) ^ z)' ^ y')' = y. [para(1290(a,1),1198(a,1,1,1,1,1,1)),rewrite(1167(3))]. 1390 ((x ^ y) ^ z)' ^ x' = x'. [para(1373(a,1),1167(a,1,1)),flip(a)]. 1408 ((x ^ y) ^ z) ^ (x ^ (((x ^ y) ^ z)' ^ u)') = (x ^ y) ^ z. [para(1373(a,1),1269(a,1,2,1)),rewrite(1167(4),1167(13))]. 1423 ((x ^ y) ^ z) ^ (y ^ (((x ^ y) ^ z)' ^ u)') = (x ^ y) ^ z. [para(1383(a,1),1269(a,1,2,1)),rewrite(1167(4),1167(13))]. 1425 ((x' ^ y) ^ z)' ^ x = x. [para(1167(a,1),1390(a,1,2)),rewrite(1167(7))]. 1433 (x ^ (y ^ z))' ^ y' = y'. [para(1280(a,1),1390(a,1,1,1))]. 1439 x ^ ((x' ^ y) ^ z)' = x. [para(1425(a,1),1226(a,1,1)),rewrite(1425(10))]. 1440 ((x ^ y') ^ z)' ^ y = y. [para(1280(a,1),1425(a,1,1,1,1))]. 1441 (x ^ (y' ^ z))' ^ y = y. [para(1280(a,1),1425(a,1,1,1))]. 1455 x ^ ((y ^ x') ^ z)' = x. [para(1280(a,1),1439(a,1,2,1,1))]. 1456 x ^ (y ^ (x' ^ z))' = x. [para(1280(a,1),1439(a,1,2,1))]. 1464 (x ^ (y ^ z'))' ^ z = z. [para(1280(a,1),1440(a,1,1,1))]. 1485 (x ^ y)' ^ ((y' ^ z) ^ u) = (y' ^ z) ^ u. [para(1425(a,1),1441(a,1,1,1,2))]. 1488 (x ^ y)' ^ (z ^ (y' ^ u)) = z ^ (y' ^ u). [para(1441(a,1),1441(a,1,1,1,2))]. 1492 x ^ (y ^ (z ^ x'))' = x. [para(1280(a,1),1455(a,1,2,1))]. 1497 x' ^ (y ^ (x ^ z))' = x'. [para(1167(a,1),1456(a,1,2,1,2,1))]. 1510 (x ^ (y ^ z))' ^ z' = z'. [para(1167(a,1),1464(a,1,1,1,2,2))]. 1525 x' ^ (y ^ (z ^ x))' = x'. [para(1167(a,1),1492(a,1,2,1,2,2))]. 1558 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(1433(a,1),1170(a,1,1,1)),rewrite(1167(2),1167(4),1167(7))]. 1696 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(1510(a,1),1170(a,1,1,1)),rewrite(1167(2),1167(4),1167(7))]. 1717 (x ^ y) ^ (y ^ x) = y ^ x. [para(1284(a,1),1256(a,1,1,1,1)),rewrite(1167(2))]. 1738 (x ^ y) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(1497(a,1),1256(a,1,1,1,1)),rewrite(1167(2))]. 1741 (x ^ y) ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(1525(a,1),1256(a,1,1,1,1)),rewrite(1167(2))]. 1745 x ^ y = y ^ x. [para(1717(a,1),1226(a,1,1)),rewrite(1717(3),1717(4))]. 2578 (x ^ y) ^ (x ^ (z ^ y)) = x ^ (z ^ y). [para(1696(a,1),1738(a,1,2)),rewrite(1696(7))]. 5169 ((x ^ y) ^ z) ^ (y ^ ((z' ^ u) ^ v)') = (x ^ y) ^ z. [para(1485(a,1),1423(a,1,2,2,1))]. 5756 ((x ^ y) ^ z) ^ (x ^ (u ^ (z' ^ v))') = (x ^ y) ^ z. [para(1488(a,1),1408(a,1,2,2,1))]. 6213 (x ^ (y ^ z)) ^ (z ^ x) = x ^ (y ^ z). [para(1741(a,1),1717(a,1,2)),rewrite(1745(7),995(7),1741(8))]. 6263 (x ^ y) ^ (x ^ z) = z ^ (x ^ y). [para(1738(a,1),1741(a,1,2)),rewrite(6213(6),1738(7))]. 6338 (x ^ y) ^ (x ^ z) = (x ^ y) ^ z. [para(6263(a,2),1717(a,1,1)),rewrite(1745(6),2578(6))]. 6340 (x ^ y) ^ z = y ^ (x ^ z). [para(6263(a,1),1745(a,1)),rewrite(6338(5)),flip(a)]. 6655 x ^ (y ^ (z ^ (u ^ (x' ^ v))')) = y ^ (z ^ x). [back_rewrite(5756),rewrite(6340(2),6340(8),6340(8),1558(7),6340(9))]. 6765 x ^ (y ^ z) = y ^ (x ^ z). [back_rewrite(5169),rewrite(6340(2),6340(5),6340(8),995(7),6340(7),6655(7),6340(4))]. 7289 $F # answer(assoc). [back_rewrite(1177),rewrite(6765(5)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=350. Generated=134551. Kept=7273. proofs=4. Usable=57. Sos=938. Demods=1390. Limbo=523, Disabled=5763. Hints=0. Weight_deleted=4733. Literals_deleted=0. Forward_subsumed=122541. Back_subsumed=186. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=6958 (5 lex), Back_demodulated=5568. Back_unit_deleted=0. Demod_attempts=2569516. Demod_rewrites=442117. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=5. Megabytes=6.14. User_CPU=3.67, System_CPU=0.04, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 4 proofs. Process 11418 exit (max_proofs) Sat Aug 12 21:01:05 2006