============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3924 was started by mccune on cleo.thornwood, Wed Nov 22 11:25:05 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) # 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.01 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 (T,wt=7): 25 x ^ x = x''. [para(11(a,1),20(a,1,1)),flip(a)]. given #6 (A,wt=7): 26 x v x = x''. [para(21(a,1),11(a,1))]. given #7 (F,wt=10): 27 (x v y)' = x' ^ y'. [para(21(a,1),20(a,1,1))]. given #8 (F,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 (T,wt=14): 43 f(x',y' ^ z') = x v (y v z). [para(27(a,1),21(a,1,2))]. given #11 (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 #12 (F,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 (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 #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 (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 #16 (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 #17 (F,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 (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 #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 (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 #21 (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 #22 (F,wt=17): 181 f(x''',f(x,f(f(x,f(x',x)),x))) = x. [para(11(a,1),32(a,1,1))]. given #23 (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 #24 (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 #25 (T,wt=12): 236 f(x',f(x'',x)) = x''. [para(32(a,1),190(a,1,2,2))]. given #26 (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 #27 (F,wt=13): 238 x' ^ f(x'',x) = x'''. [para(236(a,1),20(a,1,1)),flip(a)]. given #28 (F,wt=14): 240 f(x'',x'' v x) = x'''. [para(21(a,1),236(a,1,2))]. given #29 (T,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 #30 (T,wt=14): 275 f(x,x v f(x',x' v x)) = x'. [para(29(a,1),229(a,1,2))]. given #31 (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 #32 (F,wt=15): 261 x'' ^ (x'' v x) = x''''. [para(21(a,1),238(a,1,2))]. given #33 (F,wt=15): 281 x ^ (x v f(x',x' v x)) = x''. [para(275(a,1),20(a,1,1)),flip(a)]. given #34 (T,wt=16): 271 x ^ f(x',x' ^ (x' v x)) = x''. [para(229(a,1),20(a,1,1)),flip(a)]. given #35 (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 #36 (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 #37 (F,wt=18): 217 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(181(a,1),20(a,1,1)),flip(a)]. given #38 (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 #39 (T,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 #40 (T,wt=18): 260 (x ^ y) ^ f((x ^ y)',f(x,y)) = (x ^ y)''. [para(20(a,1),238(a,1,1)),rewrite(20(3),20(8))]. given #41 (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 #42 (F,wt=18): 306 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 #43 (F,wt=12): 428 f(x,f(x',x' v x)) = x'. [para(306(a,1),190(a,1,2))]. given #44 (T,wt=13): 431 x ^ f(x',x' v x) = x''. [para(306(a,1),230(a,1,2))]. given #45 (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 #46 (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 #47 (F,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 #48 (F,wt=18): 401 x ^ f(f(x,y),f(x,y) ^ (x' v x)) = x ^ y. [para(306(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. given #49 (T,wt=18): 499 x ^ (x v f(x',f(y ^ x,f(y,x)))) = x''. [para(464(a,1),20(a,1,1)),flip(a)]. given #50 (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 #51 (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 #52 (F,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 #53 (F,wt=19): 61 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 #54 (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 #55 (T,wt=19): 114 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 #56 (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 #57 (F,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 #58 (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 #59 (T,wt=19): 244 f((x ^ y)',(x ^ y)' v f(x,y)) = (x ^ y)''. [para(29(a,1),236(a,1,2))]. given #60 (T,wt=19): 434 f(f(x,y),f(x ^ y,(x ^ y) v f(x,y))) = x ^ y. [para(20(a,1),428(a,1,2,1)),rewrite(20(4),20(9))]. given #61 (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 #62 (F,wt=8): 751 f(x,x'') = x'. [para(41(a,1),190(a,1,2,2)),rewrite(11(3))]. given #63 (F,wt=9): 756 x ^ x'' = x''. [para(41(a,1),230(a,1,2,2)),rewrite(11(3))]. given #64 (T,wt=9): 766 x v x'' = x''. [para(751(a,1),21(a,1)),flip(a)]. given #65 (T,wt=12): 765 f(f(x,y),(x ^ y)') = x ^ y. [para(20(a,1),751(a,1,2,1)),rewrite(20(6))]. given #66 (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 #67 (F,wt=9): 871 f(x,x ^ y) = f(x,y). [para(41(a,1),42(a,1,2,2)),rewrite(11(3),20(2))]. given #68 (F,wt=7): 992 x'' v x = x. [para(181(a,1),871(a,2)),rewrite(217(12),21(5))]. restricted denial: (wt=17): 1143 (c2 ^ (c1 ^ c3))''' != (c1 ^ (c2 ^ c3))''' # answer(assoc). [back_rewrite(24),rewrite(1062(5),1062(13))]. restricted denial: (wt=46): 1144 (c9 ^ (c8 ^ c10))''' != (c8 ^ (c9 ^ c10))''' | (c8' ^ (c8 ^ c9)''')''' != c8 | (c9 ^ c9')''' != (c8 ^ c8')''' # answer(combined). [back_rewrite(23),rewrite(1062(5),1062(13),1062(22),1062(26),1062(35),1062(42))]. restricted denial: (wt=15): 1145 (c7 ^ c7')''' != (c6 ^ c6')''' # answer(one). [back_rewrite(17),rewrite(1062(4),1062(11))]. restricted denial: (wt=14): 1146 (c4' ^ (c4 ^ c5)''')''' != c4 # answer(absorb). [back_rewrite(15),rewrite(1062(5),1062(9))]. given #69 (T,wt=7): 1130 x'''' = x. [back_rewrite(744),rewrite(1062(1),1062(6),1062(10),1062(14),1062(18),1062(22),1128(22))]. given #70 (T,wt=7): 1151 x'' ^ x = x. [back_rewrite(1048),rewrite(1130(7))]. given #71 (A,wt=9): 973 x ^ (x ^ y) = x ^ y. [para(871(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. given #72 (F,wt=10): 1062 f(x,y) = (x ^ y)'''. [para(992(a,1),29(a,2)),rewrite(20(2),997(5)),flip(a)]. given #73 (F,wt=12): 1063 x v y = (x' ^ y')'''. [para(992(a,1),43(a,2,2)),rewrite(1048(6),1060(6),1062(3)),flip(a)]. given #74 (T,wt=14): 1077 ((x ^ y)''' ^ x')''' = x. [back_rewrite(1018),rewrite(1062(1),1062(6))]. ============================== PROOF ================================= % Proof 1 at 0.27 (+ 0.00) seconds: absorb. % Length of proof is 44. % Level of proof is 14. % Maximum clause weight is 36. % Given clauses 74. 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)]. 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))]. 217 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))]. 333 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))]. 744 f(f(x,y),f(y,f(f(y,f(x',x)),z))) = y. [para(41(a,1),22(a,1,1))]. 755 f(x,y) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(41(a,1),36(a,1,1))]. 845 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),42(a,1,2,2))]. 871 f(x,x ^ y) = f(x,y). [para(41(a,1),42(a,1,2,2)),rewrite(11(3),20(2))]. 992 x'' v x = x. [para(181(a,1),871(a,2)),rewrite(217(12),21(5))]. 997 f(x'',x) = x'''. [para(240(a,1),871(a,2)),rewrite(992(7),871(6))]. 1018 f(f(x,y),x') = x. [para(41(a,1),871(a,2)),rewrite(333(17))]. 1062 f(x,y) = (x ^ y)'''. [para(992(a,1),29(a,2)),rewrite(20(2),997(5)),flip(a)]. 1077 ((x ^ y)''' ^ x')''' = x. [back_rewrite(1018),rewrite(1062(1),1062(6))]. 1109 (x' ^ ((x' ^ (x ^ y)''')''' ^ x)''')''' = (x' ^ (x ^ y)''')'''. [back_rewrite(845),rewrite(1062(3),1062(7),1062(11),1062(15),1062(20),1062(24))]. 1128 (x ^ y)''' ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(755),rewrite(1062(1),1062(6),1062(10),1062(14),1062(18))]. 1130 x'''' = x. [back_rewrite(744),rewrite(1062(1),1062(6),1062(10),1062(14),1062(18),1062(22),1128(22))]. 1146 (c4' ^ (c4 ^ c5)''')''' != c4 # answer(absorb). [back_rewrite(15),rewrite(1062(5),1062(9))]. 1152 x'' = x. [para(25(a,1),1077(a,1,1,1,1,1,1,1,1)),rewrite(1130(4),25(3),1130(4))]. 1156 ((x' ^ y)' ^ x)' = x'. [para(1130(a,1),1077(a,1,1,1,1,2)),rewrite(1152(2),1152(4),1152(6),1152(7))]. 1159 (c4' ^ (c4 ^ c5)')' != c4 # answer(absorb). [back_rewrite(1146),rewrite(1152(7),1152(9))]. 1173 (x' ^ (x ^ y)')' = x. [back_rewrite(1109),rewrite(1152(5),1152(7),1156(8),1152(3),25(3),1152(2),1152(2),1152(2),1152(4),1152(6)),flip(a)]. 1174 $F # answer(absorb). [resolve(1173,a,1159,a)]. ============================== end of proof ========================== restricted denial: (wt=10): 1159 (c4' ^ (c4 ^ c5)')' != c4 # answer(absorb). [back_rewrite(1146),rewrite(1152(7),1152(9))]. restricted denial: (wt=11): 1160 (c7 ^ c7')' != (c6 ^ c6')' # answer(one). [back_rewrite(1145),rewrite(1152(6),1152(11))]. restricted denial: (wt=34): 1161 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' | (c8' ^ (c8 ^ c9)')' != c8 | (c9 ^ c9')' != (c8 ^ c8')' # answer(combined). [back_rewrite(1144),rewrite(1152(7),1152(13),1152(20),1152(22),1152(29),1152(34))]. restricted denial: (wt=13): 1162 (c2 ^ (c1 ^ c3))' != (c1 ^ (c2 ^ c3))' # answer(assoc). [back_rewrite(1143),rewrite(1152(7),1152(13))]. % Redundant proof: 1193 $F # answer(absorb). [back_rewrite(1159),rewrite(1173(8)),xx(a)]. restricted denial: (wt=24): 1192 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' | (c9 ^ c9')' != (c8 ^ c8')' # answer(combined). [back_rewrite(1161),rewrite(1173(21)),xx(b)]. % Disable descendants (x means already disabled): 14x 15x 1146x 1159x given #75 (T,wt=5): 1152 x'' = x. [para(25(a,1),1077(a,1,1,1,1,1,1,1,1)),rewrite(1130(4),25(3),1130(4))]. given #76 (A,wt=10): 1155 (x ^ y)' ^ x' = x'. [para(1077(a,1),756(a,2,1)),rewrite(1152(3),1152(6),1152(7),1152(10),1152(10),25(9),1152(6))]. given #77 (F,wt=5): 1191 x ^ x = x. [back_rewrite(25),rewrite(1152(3))]. given #78 (F,wt=8): 1190 f(x,y) = (x ^ y)'. [back_rewrite(1062),rewrite(1152(4))]. given #79 (T,wt=9): 1194 (x' ^ y)' ^ x = x. [para(1152(a,1),1155(a,1,2)),rewrite(1152(6))]. given #80 (T,wt=10): 1173 (x' ^ (x ^ y)')' = x. [back_rewrite(1109),rewrite(1152(5),1152(7),1156(8),1152(3),25(3),1152(2),1152(2),1152(2),1152(4),1152(6)),flip(a)]. given #81 (A,wt=27): 1164 ((x ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1141),rewrite(1152(3),1152(5),1152(9),1152(11),1152(13),1152(15))]. given #82 (F,wt=10): 1189 x v y = (x' ^ y')'. [back_rewrite(1063),rewrite(1152(6))]. given #83 (F,wt=10): 1195 x' ^ (x ^ y)' = x'. [para(1173(a,1),1152(a,1,1)),flip(a)]. given #84 (T,wt=9): 1210 x ^ (x' ^ y)' = x. [para(1152(a,1),1195(a,1,1)),rewrite(1152(6))]. given #85 (T,wt=9): 1211 (x ^ y) ^ x = x ^ y. [para(1155(a,1),1195(a,1,2,1)),rewrite(1152(3),1152(3),1152(5))]. given #86 (A,wt=26): 1167 x ^ ((x ^ y)' ^ (((x ^ y)' ^ (x ^ x')')' ^ z)')' = x ^ y. [back_rewrite(1137),rewrite(1152(3),1152(5),1152(6),1152(8),1152(10),1152(12),1152(14))]. given #87 (F,wt=13): 1188 (((x ^ y)' ^ y') ^ y')' = y. [back_rewrite(1078),rewrite(1152(3),1152(8))]. given #88 (F,wt=13): 1224 ((x ^ y)' ^ y') ^ y' = y'. [para(1188(a,1),1152(a,1,1)),flip(a)]. given #89 (T,wt=11): 1229 ((x ^ y')' ^ y) ^ y = y. [para(1152(a,1),1224(a,1,1,2)),rewrite(1152(6),1152(7))]. given #90 (T,wt=11): 1233 x ^ ((y ^ x')' ^ x) = x. [para(1229(a,1),1211(a,1,1)),rewrite(1229(10))]. given #91 (A,wt=25): 1170 ((x ^ y)' ^ y') ^ (y ^ ((y ^ (x' ^ x)')' ^ y)')' = y'. [back_rewrite(1132),rewrite(1152(3),1152(8),1152(10),1152(12),1152(14))]. given #92 (F,wt=13): 1230 x' ^ ((y ^ x)' ^ x') = x'. [para(1224(a,1),1211(a,1,1)),rewrite(1224(12))]. given #93 (F,wt=15): 1198 ((x ^ y)' ^ (y ^ z)') ^ y' = y'. [para(1164(a,1),973(a,1,2)),rewrite(1164(22))]. given #94 (T,wt=15): 1220 x' ^ ((y ^ x)' ^ (x ^ z)') = x'. [para(1164(a,1),1211(a,1,1)),rewrite(1164(22))]. given #95 (T,wt=15): 1240 ((x ^ y')' ^ (y' ^ z)') ^ y = y. [para(1152(a,1),1198(a,1,2)),rewrite(1152(10))]. given #96 (A,wt=22): 1172 (x ^ y)' ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1128),rewrite(1152(3),1152(6),1152(8),1152(10),1152(12))]. given #97 (F,wt=9): 1264 x ^ (y ^ x) = y ^ x. [para(1172(a,1),1155(a,1,1,1)),rewrite(1152(2),1152(3),1152(5))]. given #98 (F,wt=9): 1267 (x ^ y')' ^ y = y. [para(1194(a,1),1172(a,1,2,1,2,1)),rewrite(1191(6),1152(5),1152(6))]. given #99 (T,wt=9): 1268 (x ^ y) ^ y = x ^ y. [para(1172(a,1),1195(a,1,2,1)),rewrite(1152(3),1152(3),1152(5))]. given #100 (T,wt=9): 1275 x ^ (y ^ x')' = x. [para(1264(a,1),1210(a,1,2,1))]. given #101 (A,wt=23): 1176 (x ^ ((x ^ y)' ^ ((z ^ x) ^ (z ^ x)')')')' = (x ^ y)'. [back_rewrite(1107),rewrite(1152(3),1152(6),1152(8),1152(10),1152(12),1152(14))]. given #102 (F,wt=10): 1262 (x ^ y)' ^ y' = y'. [para(1172(a,1),973(a,1,2)),rewrite(1172(16))]. given #103 (F,wt=10): 1269 x' ^ (y ^ x)' = x'. [para(1172(a,1),1211(a,1,1)),rewrite(1172(16))]. given #104 (T,wt=15): 1244 ((x ^ y)' ^ (x ^ z)') ^ x' = x'. [para(1211(a,1),1198(a,1,1,1,1))]. given #105 (T,wt=15): 1249 x ^ ((y ^ x')' ^ (x' ^ z)') = x. [para(1152(a,1),1220(a,1,1)),rewrite(1152(10))]. given #106 (A,wt=20): 1179 (x ^ y)' ^ (x ^ ((x ^ y)' ^ (x ^ y))')' = x'. [back_rewrite(1104),rewrite(1152(3),1152(8),1152(10))]. given #107 (F,wt=15): 1254 x' ^ ((x ^ y)' ^ (x ^ z)') = x'. [para(1211(a,1),1220(a,1,2,1,1))]. given #108 (F,wt=15): 1261 ((x' ^ y)' ^ (x' ^ z)') ^ x = x. [para(1211(a,1),1240(a,1,1,1,1))]. given #109 (T,wt=15): 1278 ((x ^ y)' ^ (z ^ y)') ^ y' = y'. [para(1264(a,1),1198(a,1,1,2,1))]. given #110 (T,wt=15): 1279 x' ^ ((y ^ x)' ^ (z ^ x)') = x'. [para(1264(a,1),1220(a,1,2,2,1))]. given #111 (A,wt=19): 1183 ((((x ^ y)' ^ (y ^ z)')' ^ u)' ^ y')' = y. [back_rewrite(1092),rewrite(1152(3),1152(5),1152(7),1152(9),1152(12))]. given #112 (F,wt=12): 1358 (((x ^ y) ^ z)' ^ x')' = x. [para(1155(a,1),1183(a,1,1,1,1,1,1)),rewrite(1152(3))]. given #113 (F,wt=12): 1368 (((x ^ y) ^ z)' ^ y')' = y. [para(1275(a,1),1183(a,1,1,1,1,1,1)),rewrite(1152(3))]. given #114 (T,wt=12): 1375 ((x ^ y) ^ z)' ^ x' = x'. [para(1358(a,1),1152(a,1,1)),flip(a)]. given #115 (T,wt=11): 1410 ((x' ^ y) ^ z)' ^ x = x. [para(1152(a,1),1375(a,1,2)),rewrite(1152(7))]. given #116 (A,wt=29): 1199 ((x ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x' ^ x)')' ^ (y ^ z))')' = y'. [para(973(a,1),1164(a,1,1,2,1))]. given #117 (F,wt=11): 1424 x ^ ((x' ^ y) ^ z)' = x. [para(1410(a,1),1211(a,1,1)),rewrite(1410(10))]. given #118 (F,wt=11): 1425 ((x ^ y') ^ z)' ^ y = y. [para(1264(a,1),1410(a,1,1,1,1))]. given #119 (T,wt=11): 1426 (x ^ (y' ^ z))' ^ y = y. [para(1264(a,1),1410(a,1,1,1))]. given #120 (T,wt=11): 1440 x ^ ((y ^ x') ^ z)' = x. [para(1264(a,1),1424(a,1,2,1,1))]. given #121 (A,wt=36): 1200 ((x ^ y)' ^ (y ^ ((y ^ (x' ^ x)')' ^ z))') ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [para(973(a,1),1164(a,1,2,1,2,1))]. given #122 (F,wt=11): 1441 x ^ (y ^ (x' ^ z))' = x. [para(1264(a,1),1424(a,1,2,1))]. given #123 (F,wt=11): 1449 (x ^ (y ^ z'))' ^ z = z. [para(1264(a,1),1425(a,1,1,1))]. given #124 (T,wt=11): 1477 x ^ (y ^ (z ^ x'))' = x. [para(1264(a,1),1440(a,1,2,1))]. given #125 (T,wt=12): 1397 ((x ^ y) ^ z)' ^ y' = y'. [para(1368(a,1),1152(a,1,1)),flip(a)]. given #126 (A,wt=28): 1201 ((x' ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x ^ x')')' ^ z)')' = y'. [para(1152(a,1),1164(a,1,2,1,2,1,1,1,2,1,1))]. given #127 (F,wt=12): 1415 x' ^ ((x ^ y) ^ z)' = x'. [para(1375(a,1),1211(a,1,1)),rewrite(1375(10))]. given #128 (F,wt=12): 1418 (x ^ (y ^ z))' ^ y' = y'. [para(1264(a,1),1375(a,1,1,1))]. given #129 (T,wt=12): 1474 x' ^ ((y ^ x) ^ z)' = x'. [para(1152(a,1),1440(a,1,2,1,1,2))]. given #130 (T,wt=12): 1482 x' ^ (y ^ (x ^ z))' = x'. [para(1152(a,1),1441(a,1,2,1,2,1))]. given #131 (A,wt=23): 1202 x ^ ((y ^ x)' ^ (x ^ z)')' = ((y ^ x)' ^ (x ^ z)')'. [para(1164(a,1),1155(a,1,1,1)),rewrite(1152(2))]. given #132 (F,wt=12): 1495 (x ^ (y ^ z))' ^ z' = z'. [para(1152(a,1),1449(a,1,1,1,2,2))]. given #133 (F,wt=12): 1510 x' ^ (y ^ (z ^ x))' = x'. [para(1152(a,1),1477(a,1,2,1,2,2))]. given #134 (T,wt=13): 1377 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(1358(a,1),1155(a,1,1)),rewrite(1152(4),1152(7))]. given #135 (T,wt=13): 1381 ((x ^ y) ^ z) ^ x = (x ^ y) ^ z. [para(1358(a,1),1195(a,1,2)),rewrite(1152(4),1152(7))]. given #136 (A,wt=35): 1204 ((x ^ (y ^ z)')' ^ y) ^ ((y ^ z)' ^ (((y ^ z)' ^ (x' ^ x)')' ^ y')')' = y ^ z. [para(1155(a,1),1164(a,1,1,2,1)),rewrite(1152(6),1152(23))]. given #137 (F,wt=11): 1708 (x' ^ x) ^ y = x' ^ x. [para(1155(a,1),1204(a,1,2,1,2,1,1,1)),rewrite(1424(5),973(4),1152(10),1439(12),1155(10),1152(6),1191(5)),flip(a)]. given #138 (F,wt=9): 1750 (x' ^ x)' ^ y = y. [para(1708(a,1),1267(a,1,1,1))]. given #139 (T,wt=9): 1751 x ^ (y' ^ y)' = x. [para(1708(a,1),1275(a,1,2,1))]. NOTE: New constant: (x' ^ x)' = c_0. [new_symbol(1761)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c_0, ', ^, v, f ]). given #140 (T,wt=5): 1765 x ^ c_0 = x. [back_rewrite(1751),rewrite(1764(3))]. given #141 (A,wt=23): 1215 ((x ^ y)' ^ (y ^ z)')' ^ y = ((x ^ y)' ^ (y ^ z)')'. [para(1164(a,1),1195(a,1,2,1)),rewrite(1152(8))]. given #142 (F,wt=5): 1766 c_0 ^ x = x. [back_rewrite(1750),rewrite(1764(3))]. given #143 (F,wt=7): 1777 c_0' ^ x = c_0'. [para(1765(a,1),1708(a,1,1)),rewrite(1765(7))]. given #144 (T,wt=7): 1805 x' ^ x = c_0'. [para(1708(a,1),1215(a,1,1,1,2,1)),rewrite(1742(3),1764(3),1764(4),1191(3),1742(5),1742(5),1764(5),1708(6),1764(6),1191(5))]. ============================== PROOF ================================= % Proof 2 at 0.41 (+ 0.02) seconds: one. % Length of proof is 87. % Level of proof is 24. % Maximum clause weight is 39. % Given clauses 144. 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)]. 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))]. 194 (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)]. 217 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(181(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))]. 333 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))]. 744 f(f(x,y),f(y,f(f(y,f(x',x)),z))) = y. [para(41(a,1),22(a,1,1))]. 755 f(x,y) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(41(a,1),36(a,1,1))]. 756 x ^ x'' = x''. [para(41(a,1),230(a,1,2,2)),rewrite(11(3))]. 845 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),42(a,1,2,2))]. 871 f(x,x ^ y) = f(x,y). [para(41(a,1),42(a,1,2,2)),rewrite(11(3),20(2))]. 973 x ^ (x ^ y) = x ^ y. [para(871(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. 977 f(f(f(f(x,y),f(y,z)),u),y') = y. [para(22(a,1),871(a,2)),rewrite(36(14))]. 992 x'' v x = x. [para(181(a,1),871(a,2)),rewrite(217(12),21(5))]. 997 f(x'',x) = x'''. [para(240(a,1),871(a,2)),rewrite(992(7),871(6))]. 1018 f(f(x,y),x') = x. [para(41(a,1),871(a,2)),rewrite(333(17))]. 1062 f(x,y) = (x ^ y)'''. [para(992(a,1),29(a,2)),rewrite(20(2),997(5)),flip(a)]. 1077 ((x ^ y)''' ^ x')''' = x. [back_rewrite(1018),rewrite(1062(1),1062(6))]. 1092 ((((x ^ y)''' ^ (y ^ z)''')''' ^ u)''' ^ y')''' = y. [back_rewrite(977),rewrite(1062(1),1062(5),1062(9),1062(13),1062(18))]. 1109 (x' ^ ((x' ^ (x ^ y)''')''' ^ x)''')''' = (x' ^ (x ^ y)''')'''. [back_rewrite(845),rewrite(1062(3),1062(7),1062(11),1062(15),1062(20),1062(24))]. 1128 (x ^ y)''' ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(755),rewrite(1062(1),1062(6),1062(10),1062(14),1062(18))]. 1130 x'''' = x. [back_rewrite(744),rewrite(1062(1),1062(6),1062(10),1062(14),1062(18),1062(22),1128(22))]. 1141 ((x ^ y)''' ^ (y ^ z)''') ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(194),rewrite(1062(1),1062(5),1062(11),1062(15),1062(19),1062(23))]. 1145 (c7 ^ c7')''' != (c6 ^ c6')''' # answer(one). [back_rewrite(17),rewrite(1062(4),1062(11))]. 1152 x'' = x. [para(25(a,1),1077(a,1,1,1,1,1,1,1,1)),rewrite(1130(4),25(3),1130(4))]. 1155 (x ^ y)' ^ x' = x'. [para(1077(a,1),756(a,2,1)),rewrite(1152(3),1152(6),1152(7),1152(10),1152(10),25(9),1152(6))]. 1156 ((x' ^ y)' ^ x)' = x'. [para(1130(a,1),1077(a,1,1,1,1,2)),rewrite(1152(2),1152(4),1152(6),1152(7))]. 1160 (c7 ^ c7')' != (c6 ^ c6')' # answer(one). [back_rewrite(1145),rewrite(1152(6),1152(11))]. 1164 ((x ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1141),rewrite(1152(3),1152(5),1152(9),1152(11),1152(13),1152(15))]. 1172 (x ^ y)' ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1128),rewrite(1152(3),1152(6),1152(8),1152(10),1152(12))]. 1173 (x' ^ (x ^ y)')' = x. [back_rewrite(1109),rewrite(1152(5),1152(7),1156(8),1152(3),25(3),1152(2),1152(2),1152(2),1152(4),1152(6)),flip(a)]. 1183 ((((x ^ y)' ^ (y ^ z)')' ^ u)' ^ y')' = y. [back_rewrite(1092),rewrite(1152(3),1152(5),1152(7),1152(9),1152(12))]. 1191 x ^ x = x. [back_rewrite(25),rewrite(1152(3))]. 1194 (x' ^ y)' ^ x = x. [para(1152(a,1),1155(a,1,2)),rewrite(1152(6))]. 1195 x' ^ (x ^ y)' = x'. [para(1173(a,1),1152(a,1,1)),flip(a)]. 1202 x ^ ((y ^ x)' ^ (x ^ z)')' = ((y ^ x)' ^ (x ^ z)')'. [para(1164(a,1),1155(a,1,1,1)),rewrite(1152(2))]. 1204 ((x ^ (y ^ z)')' ^ y) ^ ((y ^ z)' ^ (((y ^ z)' ^ (x' ^ x)')' ^ y')')' = y ^ z. [para(1155(a,1),1164(a,1,1,2,1)),rewrite(1152(6),1152(23))]. 1210 x ^ (x' ^ y)' = x. [para(1152(a,1),1195(a,1,1)),rewrite(1152(6))]. 1211 (x ^ y) ^ x = x ^ y. [para(1155(a,1),1195(a,1,2,1)),rewrite(1152(3),1152(3),1152(5))]. 1215 ((x ^ y)' ^ (y ^ z)')' ^ y = ((x ^ y)' ^ (y ^ z)')'. [para(1164(a,1),1195(a,1,2,1)),rewrite(1152(8))]. 1262 (x ^ y)' ^ y' = y'. [para(1172(a,1),973(a,1,2)),rewrite(1172(16))]. 1264 x ^ (y ^ x) = y ^ x. [para(1172(a,1),1155(a,1,1,1)),rewrite(1152(2),1152(3),1152(5))]. 1267 (x ^ y')' ^ y = y. [para(1194(a,1),1172(a,1,2,1,2,1)),rewrite(1191(6),1152(5),1152(6))]. 1275 x ^ (y ^ x')' = x. [para(1264(a,1),1210(a,1,2,1))]. 1284 (x ^ (y ^ (x' ^ x))')' ^ ((y ^ (x' ^ x))' ^ ((x' ^ x) ^ z)')' = y ^ (x' ^ x). [para(1267(a,1),1172(a,1,2,1,2,1,1,1)),rewrite(1152(4),1152(10),1152(14),1152(21),1152(22))]. 1358 (((x ^ y) ^ z)' ^ x')' = x. [para(1155(a,1),1183(a,1,1,1,1,1,1)),rewrite(1152(3))]. 1375 ((x ^ y) ^ z)' ^ x' = x'. [para(1358(a,1),1152(a,1,1)),flip(a)]. 1377 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(1358(a,1),1155(a,1,1)),rewrite(1152(4),1152(7))]. 1410 ((x' ^ y) ^ z)' ^ x = x. [para(1152(a,1),1375(a,1,2)),rewrite(1152(7))]. 1424 x ^ ((x' ^ y) ^ z)' = x. [para(1410(a,1),1211(a,1,1)),rewrite(1410(10))]. 1439 (x ^ y) ^ (y' ^ z)' = x ^ y. [para(1172(a,1),1424(a,1,2,1,1))]. 1441 x ^ (y ^ (x' ^ z))' = x. [para(1264(a,1),1424(a,1,2,1))]. 1447 x' ^ ((y ^ (x' ^ x))' ^ ((x' ^ x) ^ z)')' = y ^ (x' ^ x). [back_rewrite(1284),rewrite(1441(5))]. 1678 x ^ ((y ^ (x ^ z))' ^ ((x ^ z) ^ u)')' = ((y ^ (x ^ z))' ^ ((x ^ z) ^ u)')'. [para(1202(a,1),1377(a,1,2)),rewrite(1202(19))]. 1683 ((x ^ (y' ^ y))' ^ ((y' ^ y) ^ z)')' = x ^ (y' ^ y). [back_rewrite(1447),rewrite(1678(12))]. 1708 (x' ^ x) ^ y = x' ^ x. [para(1155(a,1),1204(a,1,2,1,2,1,1,1)),rewrite(1424(5),973(4),1152(10),1439(12),1155(10),1152(6),1191(5)),flip(a)]. 1742 x ^ (y' ^ y) = y' ^ y. [back_rewrite(1683),rewrite(1708(7),1262(8),1152(4)),flip(a)]. 1750 (x' ^ x)' ^ y = y. [para(1708(a,1),1267(a,1,1,1))]. 1751 x ^ (y' ^ y)' = x. [para(1708(a,1),1275(a,1,2,1))]. 1761 (x' ^ x)' = (y' ^ y)'. [para(1751(a,1),1750(a,1))]. 1764 (x' ^ x)' = c_0. [new_symbol(1761)]. 1805 x' ^ x = c_0'. [para(1708(a,1),1215(a,1,1,1,2,1)),rewrite(1742(3),1764(3),1764(4),1191(3),1742(5),1742(5),1764(5),1708(6),1764(6),1191(5))]. 1810 x ^ x' = c_0'. [para(1152(a,1),1805(a,1,1))]. 1812 $F # answer(one). [back_rewrite(1160),rewrite(1810(4),1152(3),1810(5),1152(4)),xx(a)]. ============================== end of proof ========================== restricted denial: (wt=13): 1811 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' # answer(combined). [back_rewrite(1192),rewrite(1810(17),1152(16),1810(18),1152(17)),xx(b)]. % Disable descendants (x means already disabled): 16x 17x 1145x 1160x given #145 (T,wt=7): 1808 x ^ c_0' = c_0'. [back_rewrite(1742),rewrite(1805(2),1805(5))]. given #146 (A,wt=17): 1241 ((x ^ (y ^ z)')' ^ y) ^ (y ^ z) = y ^ z. [para(1155(a,1),1198(a,1,1,2,1)),rewrite(1152(6),1152(8),1152(10))]. given #147 (F,wt=7): 1810 x ^ x' = c_0'. [para(1152(a,1),1805(a,1,1))]. given #148 (F,wt=11): 1714 (x ^ y) ^ (y ^ x) = y ^ x. [para(1269(a,1),1204(a,1,1,1,1)),rewrite(1152(2),1152(7),1321(10),1195(8),1152(4))]. % Operation ^ is commutative; C redundancy checks enabled. % back CAC tautology: 1823 (x ^ y)' = (y ^ x)'. [para(1714(a,1),1195(a,1,2,1)),rewrite(1822(5))]. given #149 (T,wt=7): 1824 x ^ y = y ^ x. [para(1714(a,1),1211(a,1,1)),rewrite(1714(3),1714(4))]. given #150 (T,wt=13): 1399 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z. [para(1368(a,1),1155(a,1,1)),rewrite(1152(4),1152(7))]. given #151 (A,wt=17): 1253 (x ^ y) ^ (x ^ ((x ^ y)' ^ z)') = x ^ y. [para(1195(a,1),1220(a,1,2,1,1)),rewrite(1152(3),1152(3),1152(10))]. given #152 (F,wt=13): 1411 (x' ^ y)' ^ (x ^ z) = x ^ z. [para(1155(a,1),1375(a,1,1,1,1)),rewrite(1152(6),1152(8))]. given #153 (F,wt=13): 1417 (x' ^ y)' ^ (z ^ x) = z ^ x. [para(1172(a,1),1375(a,1,1,1,1)),rewrite(1152(6),1152(8))]. given #154 (T,wt=13): 1435 (x ^ y) ^ (x' ^ z)' = x ^ y. [para(1155(a,1),1424(a,1,2,1,1))]. given #155 (T,wt=13): 1439 (x ^ y) ^ (y' ^ z)' = x ^ y. [para(1172(a,1),1424(a,1,2,1,1))]. given #156 (A,wt=36): 1260 ((x ^ y)' ^ (y ^ z)')' ^ (y ^ (((x ^ y)' ^ (y ^ z)') ^ u)') = ((x ^ y)' ^ (y ^ z)')'. [para(1220(a,1),1220(a,1,2,1,1)),rewrite(1152(8))]. given #157 (F,wt=13): 1455 (x ^ y')' ^ (y ^ z) = y ^ z. [para(1155(a,1),1426(a,1,1,1,2))]. given #158 (F,wt=13): 1461 (x ^ y')' ^ (z ^ y) = z ^ y. [para(1172(a,1),1426(a,1,1,1,2))]. given #159 (T,wt=13): 1483 (x ^ y) ^ (z ^ x')' = x ^ y. [para(1155(a,1),1441(a,1,2,1,2))]. given #160 (T,wt=13): 1487 (x ^ y) ^ (z ^ y')' = x ^ y. [para(1172(a,1),1441(a,1,2,1,2))]. given #161 (A,wt=17): 1304 (x ^ y) ^ (y ^ ((x ^ y)' ^ z)') = x ^ y. [para(1269(a,1),1220(a,1,2,1,1)),rewrite(1152(3),1152(3),1152(10))]. given #162 (F,wt=13): 1543 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(1418(a,1),1155(a,1,1,1)),rewrite(1152(2),1152(4),1152(7))]. given #163 (F,wt=13): 1622 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(1495(a,1),1155(a,1,1,1)),rewrite(1152(2),1152(4),1152(7))]. given #164 (T,wt=13): 1661 x ^ (((x' ^ y) ^ z) ^ u)' = x. [para(1377(a,1),1424(a,1,2,1,1))]. given #165 (T,wt=13): 1666 x ^ (((y ^ x') ^ z) ^ u)' = x. [para(1377(a,1),1440(a,1,2,1))]. given #166 (A,wt=23): 1305 x ^ ((x ^ y)' ^ (x ^ z)')' = ((x ^ y)' ^ (x ^ z)')'. [para(1244(a,1),1155(a,1,1,1)),rewrite(1152(2))]. given #167 (F,wt=13): 1667 x ^ (y ^ ((x' ^ z) ^ u))' = x. [para(1377(a,1),1441(a,1,2,1,2))]. given #168 (F,wt=13): 1876 x ^ ((y ^ (x' ^ z)) ^ u)' = x. [para(1399(a,1),1424(a,1,2,1))]. given #169 (T,wt=13): 1877 x ^ ((y ^ (z ^ x')) ^ u)' = x. [para(1399(a,1),1440(a,1,2,1))]. given #170 (T,wt=13): 1878 x ^ (y ^ ((z ^ x') ^ u))' = x. [para(1399(a,1),1441(a,1,2,1,2))]. given #171 (A,wt=15): 1317 x ^ ((x' ^ y)' ^ (x' ^ z)') = x. [para(1211(a,1),1249(a,1,2,1,1))]. given #172 (F,wt=13): 1951 x ^ (y ^ (z ^ (x' ^ u)))' = x. [para(1441(a,1),1461(a,1,2)),rewrite(1152(5),1824(6),1441(11))]. given #173 (F,wt=13): 1953 x ^ (y ^ (z ^ (u ^ x')))' = x. [para(1477(a,1),1461(a,1,2)),rewrite(1152(5),1824(6),1477(11))]. given #174 (T,wt=14): 1412 (x ^ y)' ^ (x' ^ z) = x' ^ z. [para(1194(a,1),1375(a,1,1,1,1)),rewrite(1152(6),1152(9))]. given #175 (T,wt=14): 1419 (x ^ y)' ^ (z ^ x') = z ^ x'. [para(1267(a,1),1375(a,1,1,1,1)),rewrite(1152(6),1152(9))]. given #176 (A,wt=15): 1318 x ^ ((y ^ x')' ^ (z ^ x')') = x. [para(1264(a,1),1249(a,1,2,2,1))]. given #177 (F,wt=14): 1436 (x' ^ y) ^ (x ^ z)' = x' ^ y. [para(1194(a,1),1424(a,1,2,1,1))]. given #178 (F,wt=14): 1442 (x ^ y') ^ (y ^ z)' = x ^ y'. [para(1267(a,1),1424(a,1,2,1,1))]. given #179 (T,wt=14): 1456 (x ^ y)' ^ (y' ^ z) = y' ^ z. [para(1194(a,1),1426(a,1,1,1,2))]. given #180 (T,wt=14): 1462 (x ^ y)' ^ (z ^ y') = z ^ y'. [para(1267(a,1),1426(a,1,1,1,2))]. given #181 (A,wt=36): 1327 ((x ^ y)' ^ (x ^ z)')' ^ (x ^ (((x ^ y)' ^ (x ^ z)') ^ u)') = ((x ^ y)' ^ (x ^ z)')'. [para(1254(a,1),1220(a,1,2,1,1)),rewrite(1152(8))]. given #182 (F,wt=14): 1484 (x' ^ y) ^ (z ^ x)' = x' ^ y. [para(1194(a,1),1441(a,1,2,1,2))]. given #183 (F,wt=14): 1488 (x ^ y') ^ (z ^ y)' = x ^ y'. [para(1267(a,1),1441(a,1,2,1,2))]. given #184 (T,wt=14): 1672 x' ^ (((x ^ y) ^ z) ^ u)' = x'. [para(1377(a,1),1415(a,1,2,1,1))]. given #185 (T,wt=14): 1675 x' ^ (((y ^ x) ^ z) ^ u)' = x'. [para(1377(a,1),1474(a,1,2,1))]. given #186 (A,wt=15): 1329 x' ^ ((x ^ y)' ^ (z ^ x)') = x'. [para(1264(a,1),1254(a,1,2,2,1))]. given #187 (F,wt=14): 1676 x' ^ (y ^ ((x ^ z) ^ u))' = x'. [para(1377(a,1),1482(a,1,2,1,2))]. given #188 (F,wt=14): 1822 (x ^ y)' ^ (y ^ x)' = (y ^ x)'. [para(1714(a,1),1155(a,1,1,1))]. given #189 (T,wt=14): 1879 x' ^ ((y ^ (x ^ z)) ^ u)' = x'. [para(1399(a,1),1415(a,1,2,1))]. given #190 (T,wt=14): 1880 x' ^ ((y ^ (z ^ x)) ^ u)' = x'. [para(1399(a,1),1474(a,1,2,1))]. given #191 (A,wt=23): 1333 x ^ ((y ^ x)' ^ (z ^ x)')' = ((y ^ x)' ^ (z ^ x)')'. [para(1278(a,1),1155(a,1,1,1)),rewrite(1152(2))]. given #192 (F,wt=14): 1881 x' ^ (y ^ ((z ^ x) ^ u))' = x'. [para(1399(a,1),1482(a,1,2,1,2))]. given #193 (F,wt=14): 1957 x' ^ (y ^ (z ^ (x ^ u)))' = x'. [para(1482(a,1),1461(a,1,2)),rewrite(1152(4),1824(6),1482(11))]. given #194 (T,wt=14): 1960 x' ^ (y ^ (z ^ (u ^ x)))' = x'. [para(1510(a,1),1461(a,1,2)),rewrite(1152(4),1824(6),1510(11))]. given #195 (T,wt=15): 1660 ((x' ^ y) ^ z)' ^ (x ^ u) = x ^ u. [para(1410(a,1),1377(a,1,2,1)),rewrite(1410(11))]. given #196 (A,wt=36): 1344 ((x ^ y)' ^ (z ^ y)')' ^ (y ^ (((x ^ y)' ^ (z ^ y)') ^ u)') = ((x ^ y)' ^ (z ^ y)')'. [para(1278(a,1),1254(a,1,2,1,1)),rewrite(1152(8))]. given #197 (F,wt=15): 1663 ((x ^ y') ^ z)' ^ (y ^ u) = y ^ u. [para(1425(a,1),1377(a,1,2,1)),rewrite(1425(11))]. given #198 (F,wt=15): 1665 (x ^ (y' ^ z))' ^ (y ^ u) = y ^ u. [para(1426(a,1),1377(a,1,2,1)),rewrite(1426(11))]. given #199 (T,wt=15): 1668 (x ^ (y ^ z'))' ^ (z ^ u) = z ^ u. [para(1449(a,1),1377(a,1,2,1)),rewrite(1449(11))]. given #200 (T,wt=15): 1695 (x ^ y) ^ ((x' ^ z) ^ u)' = x ^ y. [para(1410(a,1),1381(a,1,1,1)),rewrite(1410(11))]. given #201 (A,wt=17): 1347 (x ^ y) ^ (x ^ (z ^ (x ^ y)')') = x ^ y. [para(1195(a,1),1279(a,1,2,1,1)),rewrite(1152(3),1152(3),1152(10))]. given #202 (F,wt=15): 1697 (x ^ y) ^ ((z ^ x') ^ u)' = x ^ y. [para(1425(a,1),1381(a,1,1,1)),rewrite(1425(11))]. given #203 (F,wt=15): 1698 (x ^ y) ^ (z ^ (x' ^ u))' = x ^ y. [para(1426(a,1),1381(a,1,1,1)),rewrite(1426(11))]. given #204 (T,wt=9): 2831 x ^ (x' ^ y) = c_0'. [para(1698(a,1),1810(a,1))]. given #205 (T,wt=9): 2839 x' ^ (x ^ y) = c_0'. [para(1152(a,1),2831(a,1,2,1))]. given #206 (A,wt=36): 1348 ((x ^ y)' ^ (y ^ z)')' ^ (y ^ (u ^ ((x ^ y)' ^ (y ^ z)'))') = ((x ^ y)' ^ (y ^ z)')'. [para(1220(a,1),1279(a,1,2,1,1)),rewrite(1152(8))]. given #207 (F,wt=9): 2840 x ^ (y ^ x') = c_0'. [para(1264(a,1),2831(a,1,2))]. given #208 (F,wt=9): 2849 x' ^ (y ^ x) = c_0'. [para(2831(a,1),1622(a,1)),flip(a)]. given #209 (T,wt=11): 2842 x ^ ((x' ^ y) ^ z) = c_0'. [para(1377(a,1),2831(a,1,2))]. given #210 (T,wt=11): 2843 x ^ ((y ^ x') ^ z) = c_0'. [para(1399(a,1),2831(a,1,2))]. given #211 (A,wt=17): 1350 (x ^ y) ^ (y ^ (z ^ (x ^ y)')') = x ^ y. [para(1269(a,1),1279(a,1,2,1,1)),rewrite(1152(3),1152(3),1152(10))]. given #212 (F,wt=11): 2844 (x' ^ y) ^ (x ^ z) = c_0'. [para(1411(a,1),2831(a,1,2))]. given #213 (F,wt=11): 2845 (x' ^ y) ^ (z ^ x) = c_0'. [para(1417(a,1),2831(a,1,2))]. given #214 (T,wt=11): 2846 (x ^ y') ^ (y ^ z) = c_0'. [para(1455(a,1),2831(a,1,2))]. given #215 (T,wt=11): 2847 (x ^ y') ^ (z ^ y) = c_0'. [para(1461(a,1),2831(a,1,2))]. given #216 (A,wt=36): 1351 ((x ^ y)' ^ (x ^ z)')' ^ (x ^ (u ^ ((x ^ y)' ^ (x ^ z)'))') = ((x ^ y)' ^ (x ^ z)')'. [para(1254(a,1),1279(a,1,2,1,1)),rewrite(1152(8))]. given #217 (F,wt=11): 2848 x ^ (y ^ (x' ^ z)) = c_0'. [para(1543(a,1),2831(a,1,2))]. given #218 (F,wt=11): 2850 x ^ (y ^ (z ^ x')) = c_0'. [para(1622(a,1),2831(a,1,2))]. given #219 (T,wt=11): 2852 (x ^ y) ^ (x' ^ z) = c_0'. [para(1412(a,1),2831(a,1,2))]. given #220 (T,wt=11): 2853 (x ^ y) ^ (z ^ x') = c_0'. [para(1419(a,1),2831(a,1,2))]. given #221 (A,wt=36): 1353 ((x ^ y)' ^ (z ^ y)')' ^ (y ^ (u ^ ((x ^ y)' ^ (z ^ y)'))') = ((x ^ y)' ^ (z ^ y)')'. [para(1279(a,1),1279(a,1,2,1,1)),rewrite(1152(8))]. given #222 (F,wt=11): 2854 (x ^ y) ^ (y' ^ z) = c_0'. [para(1456(a,1),2831(a,1,2))]. given #223 (F,wt=11): 2855 (x ^ y) ^ (z ^ y') = c_0'. [para(1462(a,1),2831(a,1,2))]. given #224 (T,wt=11): 2856 (x ^ y) ^ (y ^ x)' = c_0'. [para(1822(a,1),2831(a,1,2))]. given #225 (T,wt=11): 2863 x' ^ ((x ^ y) ^ z) = c_0'. [para(1377(a,1),2839(a,1,2))]. given #226 (A,wt=27): 1356 x ^ (((y ^ x)' ^ (x ^ z)')' ^ u) = ((y ^ x)' ^ (x ^ z)')' ^ u. [para(1183(a,1),1155(a,1,1)),rewrite(1152(9),1152(17))]. given #227 (F,wt=11): 2864 (x ^ y)' ^ (y ^ x) = c_0'. [para(1714(a,1),2839(a,1,2))]. given #228 (F,wt=11): 2865 x' ^ ((y ^ x) ^ z) = c_0'. [para(1399(a,1),2839(a,1,2))]. given #229 (T,wt=11): 2866 x' ^ (y ^ (x ^ z)) = c_0'. [para(1543(a,1),2839(a,1,2))]. given #230 (T,wt=11): 2867 x' ^ (y ^ (z ^ x)) = c_0'. [para(1622(a,1),2839(a,1,2))]. given #231 (A,wt=23): 1393 ((x ^ y) ^ z) ^ (x ^ (((x ^ y) ^ z)' ^ u)') = (x ^ y) ^ z. [para(1358(a,1),1254(a,1,2,1)),rewrite(1152(4),1152(13))]. given #232 (F,wt=13): 2858 ((x' ^ y) ^ z) ^ (x ^ u) = c_0'. [para(1660(a,1),2831(a,1,2))]. given #233 (F,wt=13): 2859 ((x ^ y') ^ z) ^ (y ^ u) = c_0'. [para(1663(a,1),2831(a,1,2))]. given #234 (T,wt=13): 2860 (x ^ (y' ^ z)) ^ (y ^ u) = c_0'. [para(1665(a,1),2831(a,1,2))]. given #235 (T,wt=13): 2861 (x ^ (y ^ z')) ^ (z ^ u) = c_0'. [para(1668(a,1),2831(a,1,2))]. given #236 (A,wt=23): 1408 ((x ^ y) ^ z) ^ (y ^ (((x ^ y) ^ z)' ^ u)') = (x ^ y) ^ z. [para(1368(a,1),1254(a,1,2,1)),rewrite(1152(4),1152(13))]. given #237 (F,wt=13): 2880 x ^ (((x' ^ y) ^ z) ^ u) = c_0'. [para(1661(a,1),2840(a,1,2)),rewrite(1824(5))]. given #238 (F,wt=13): 2881 x ^ (((y ^ x') ^ z) ^ u) = c_0'. [para(1666(a,1),2840(a,1,2)),rewrite(1824(5))]. given #239 (T,wt=13): 2882 x ^ (y ^ ((x' ^ z) ^ u)) = c_0'. [para(1667(a,1),2840(a,1,2)),rewrite(1824(5))]. given #240 (T,wt=13): 2883 x ^ ((y ^ (x' ^ z)) ^ u) = c_0'. [para(1876(a,1),2840(a,1,2)),rewrite(1824(5))]. given #241 (A,wt=27): 1414 (x' ^ y)' ^ ((z ^ x)' ^ (x ^ u)')' = ((z ^ x)' ^ (x ^ u)')'. [para(1164(a,1),1375(a,1,1,1,1))]. given #242 (F,wt=13): 2884 x ^ ((y ^ (z ^ x')) ^ u) = c_0'. [para(1877(a,1),2840(a,1,2)),rewrite(1824(5))]. given #243 (F,wt=13): 2885 x ^ (y ^ ((z ^ x') ^ u)) = c_0'. [para(1878(a,1),2840(a,1,2)),rewrite(1824(5))]. given #244 (T,wt=13): 2886 x ^ (y ^ (z ^ (x' ^ u))) = c_0'. [para(1951(a,1),2840(a,1,2)),rewrite(1824(5))]. given #245 (T,wt=13): 2887 x ^ (y ^ (z ^ (u ^ x'))) = c_0'. [para(1953(a,1),2840(a,1,2)),rewrite(1824(5))]. given #246 (A,wt=30): 1416 (x ^ y)' ^ ((z ^ x')' ^ (x' ^ u)')' = ((z ^ x')' ^ (x' ^ u)')'. [para(1240(a,1),1375(a,1,1,1,1))]. given #247 (F,wt=13): 2888 x' ^ (((x ^ y) ^ z) ^ u) = c_0'. [para(1672(a,1),2840(a,1,2)),rewrite(1824(5))]. given #248 (F,wt=13): 2889 x' ^ (((y ^ x) ^ z) ^ u) = c_0'. [para(1675(a,1),2840(a,1,2)),rewrite(1824(5))]. given #249 (T,wt=13): 2890 x' ^ (y ^ ((x ^ z) ^ u)) = c_0'. [para(1676(a,1),2840(a,1,2)),rewrite(1824(5))]. given #250 (T,wt=13): 2891 x' ^ ((y ^ (x ^ z)) ^ u) = c_0'. [para(1879(a,1),2840(a,1,2)),rewrite(1824(5))]. given #251 (A,wt=27): 1420 (x' ^ y)' ^ ((x ^ z)' ^ (x ^ u)')' = ((x ^ z)' ^ (x ^ u)')'. [para(1244(a,1),1375(a,1,1,1,1))]. given #252 (F,wt=13): 2892 x' ^ ((y ^ (z ^ x)) ^ u) = c_0'. [para(1880(a,1),2840(a,1,2)),rewrite(1824(5))]. given #253 (F,wt=13): 2893 x' ^ (y ^ ((z ^ x) ^ u)) = c_0'. [para(1881(a,1),2840(a,1,2)),rewrite(1824(5))]. given #254 (T,wt=13): 2894 x' ^ (y ^ (z ^ (x ^ u))) = c_0'. [para(1957(a,1),2840(a,1,2)),rewrite(1824(5))]. given #255 (T,wt=13): 2895 x' ^ (y ^ (z ^ (u ^ x))) = c_0'. [para(1960(a,1),2840(a,1,2)),rewrite(1824(5))]. given #256 (A,wt=30): 1421 (x ^ y)' ^ ((x' ^ z)' ^ (x' ^ u)')' = ((x' ^ z)' ^ (x' ^ u)')'. [para(1261(a,1),1375(a,1,1,1,1))]. given #257 (F,wt=13): 2906 (x' ^ y) ^ ((x ^ z) ^ u) = c_0'. [para(1411(a,1),2842(a,1,2,1))]. given #258 (F,wt=13): 2907 (x' ^ y) ^ ((z ^ x) ^ u) = c_0'. [para(1417(a,1),2842(a,1,2,1))]. given #259 (T,wt=13): 2908 (x ^ y') ^ ((y ^ z) ^ u) = c_0'. [para(1455(a,1),2842(a,1,2,1))]. given #260 (T,wt=13): 2909 (x ^ y') ^ ((z ^ y) ^ u) = c_0'. [para(1461(a,1),2842(a,1,2,1))]. given #261 (A,wt=27): 1422 (x' ^ y)' ^ ((z ^ x)' ^ (u ^ x)')' = ((z ^ x)' ^ (u ^ x)')'. [para(1278(a,1),1375(a,1,1,1,1))]. given #262 (F,wt=13): 2912 (x ^ y) ^ ((x' ^ z) ^ u) = c_0'. [para(1412(a,1),2842(a,1,2,1))]. given #263 (F,wt=13): 2913 (x ^ y) ^ ((z ^ x') ^ u) = c_0'. [para(1419(a,1),2842(a,1,2,1))]. given #264 (T,wt=13): 2914 (x ^ y) ^ ((y' ^ z) ^ u) = c_0'. [para(1456(a,1),2842(a,1,2,1))]. given #265 (T,wt=13): 2915 (x ^ y) ^ ((z ^ y') ^ u) = c_0'. [para(1462(a,1),2842(a,1,2,1))]. given #266 (A,wt=17): 1423 (x' ^ y)' ^ ((x ^ z) ^ u) = (x ^ z) ^ u. [para(1375(a,1),1375(a,1,1,1,1)),rewrite(1152(7),1152(10))]. given #267 (F,wt=13): 2916 (x ^ y) ^ ((y ^ x)' ^ z) = c_0'. [para(1822(a,1),2842(a,1,2,1))]. given #268 (F,wt=13): 2923 ((x ^ y) ^ z) ^ (x' ^ u) = c_0'. [para(1415(a,1),2843(a,1,2,1))]. given #269 (T,wt=13): 2924 ((x ^ y) ^ z) ^ (y' ^ u) = c_0'. [para(1474(a,1),2843(a,1,2,1))]. given #270 (T,wt=13): 2925 (x ^ (y ^ z)) ^ (y' ^ u) = c_0'. [para(1482(a,1),2843(a,1,2,1))]. given #271 (A,wt=18): 1428 (x ^ y)' ^ ((x' ^ z) ^ u) = (x' ^ z) ^ u. [para(1410(a,1),1375(a,1,1,1,1)),rewrite(1152(7),1152(11))]. given #272 (F,wt=13): 2927 (x ^ (y ^ z)) ^ (z' ^ u) = c_0'. [para(1510(a,1),2843(a,1,2,1))]. given #273 (F,wt=13): 3003 ((x' ^ y) ^ z) ^ (u ^ x) = c_0'. [para(1417(a,1),2844(a,1,2)),rewrite(1152(4))]. given #274 (T,wt=13): 3004 ((x ^ y') ^ z) ^ (u ^ y) = c_0'. [para(1461(a,1),2844(a,1,2)),rewrite(1152(4))]. given #275 (T,wt=13): 3005 (x' ^ y) ^ (z ^ (x ^ u)) = c_0'. [para(1543(a,1),2844(a,1,2))]. given #276 (A,wt=17): 1445 ((x ^ y) ^ z) ^ (x' ^ u)' = (x ^ y) ^ z. [para(1375(a,1),1424(a,1,2,1,1))]. given #277 (F,wt=13): 3006 (x' ^ y) ^ (z ^ (u ^ x)) = c_0'. [para(1622(a,1),2844(a,1,2))]. given #278 (F,wt=13): 3009 ((x ^ y) ^ z) ^ (u ^ x') = c_0'. [para(1419(a,1),2844(a,1,2)),rewrite(1152(3))]. given #279 (T,wt=13): 3010 ((x ^ y) ^ z) ^ (u ^ y') = c_0'. [para(1462(a,1),2844(a,1,2)),rewrite(1152(3))]. given #280 (T,wt=13): 3011 (x ^ y)' ^ ((y ^ x) ^ z) = c_0'. [para(1822(a,1),2844(a,1,1))]. given #281 (A,wt=18): 1446 ((x' ^ y) ^ z) ^ (x ^ u)' = (x' ^ y) ^ z. [para(1410(a,1),1424(a,1,2,1,1))]. given #282 (F,wt=13): 3023 (x ^ y) ^ (z ^ (x' ^ u)) = c_0'. [para(1411(a,1),2845(a,1,1))]. given #283 (F,wt=13): 3024 (x ^ y) ^ (z ^ (y' ^ u)) = c_0'. [para(1417(a,1),2845(a,1,1))]. given #284 (T,wt=13): 3026 (x ^ y) ^ (z ^ (u ^ x')) = c_0'. [para(1455(a,1),2845(a,1,1))]. given #285 (T,wt=13): 3027 (x ^ y) ^ (z ^ (u ^ y')) = c_0'. [para(1461(a,1),2845(a,1,1))]. given #286 (A,wt=18): 1451 (x ^ y)' ^ ((z ^ x') ^ u) = (z ^ x') ^ u. [para(1425(a,1),1375(a,1,1,1,1)),rewrite(1152(7),1152(11))]. given #287 (F,wt=13): 3029 (x ^ (y' ^ z)) ^ (u ^ y) = c_0'. [para(1543(a,1),2845(a,1,1))]. given #288 (F,wt=13): 3030 (x ^ (y ^ z')) ^ (u ^ z) = c_0'. [para(1622(a,1),2845(a,1,1))]. given #289 (T,wt=13): 3040 (x ^ y') ^ (z ^ (y ^ u)) = c_0'. [para(1419(a,1),2845(a,1,1))]. given #290 (T,wt=13): 3041 (x ^ y') ^ (z ^ (u ^ y)) = c_0'. [para(1462(a,1),2845(a,1,1))]. given #291 (A,wt=18): 1453 ((x ^ y') ^ z) ^ (y ^ u)' = (x ^ y') ^ z. [para(1425(a,1),1424(a,1,2,1,1))]. given #292 (F,wt=13): 3047 (x ^ y)' ^ (z ^ (y ^ x)) = c_0'. [para(1822(a,1),2845(a,1,1))]. given #293 (F,wt=13): 3063 (x ^ (y ^ z)') ^ (z ^ y) = c_0'. [para(1714(a,1),2846(a,1,2))]. given #294 (T,wt=13): 3065 (x ^ (y ^ z)) ^ (u ^ y') = c_0'. [para(1419(a,1),2846(a,1,2)),rewrite(1152(3))]. given #295 (T,wt=13): 3066 (x ^ (y ^ z)) ^ (u ^ z') = c_0'. [para(1462(a,1),2846(a,1,2)),rewrite(1152(3))]. given #296 (A,wt=18): 1468 (x ^ y)' ^ (z ^ (x' ^ u)) = z ^ (x' ^ u). [para(1426(a,1),1375(a,1,1,1,1)),rewrite(1152(7),1152(11))]. given #297 (F,wt=13): 3067 (x ^ (y ^ z)) ^ (z ^ y)' = c_0'. [para(1822(a,1),2846(a,1,2)),rewrite(1152(3))]. given #298 (F,wt=13): 3110 (x ^ y) ^ (z ^ (y ^ x)') = c_0'. [para(1822(a,1),2848(a,1,2,2))]. given #299 (T,wt=15): 1699 (x ^ y) ^ (z ^ (u ^ x'))' = x ^ y. [para(1449(a,1),1381(a,1,1,1)),rewrite(1449(11))]. given #300 (T,wt=15): 1762 (x ^ y) ^ (y ^ (z ^ x)) = y ^ (z ^ x). [back_rewrite(1739),rewrite(1760(11),1152(8),1195(10),1152(5))]. given #301 (A,wt=17): 1469 (x ^ y')' ^ ((y ^ z) ^ u) = (y ^ z) ^ u. [para(1375(a,1),1426(a,1,1,1,2))]. given #302 (F,wt=11): 4990 x ^ (y ^ (y ^ x)') = c_0'. [para(1762(a,1),2848(a,1)),rewrite(1824(3))]. given #303 (F,wt=11): 5094 x ^ (y ^ (x ^ y)') = c_0'. [para(1824(a,1),4990(a,1,2,2,1))]. given #304 (T,wt=13): 4986 (x ^ y)' ^ (y ^ (z ^ x)) = c_0'. [para(1762(a,1),2839(a,1,2))]. given #305 (T,wt=13): 5004 x ^ (y ^ ((y ^ x)' ^ z)) = c_0'. [para(1762(a,1),2882(a,1)),rewrite(1824(4))]. given #306 (A,wt=18): 1470 (x ^ y)' ^ ((y' ^ z) ^ u) = (y' ^ z) ^ u. [para(1410(a,1),1426(a,1,1,1,2))]. given #307 (F,wt=13): 5006 x ^ (y ^ (z ^ (y ^ x)')) = c_0'. [para(1762(a,1),2885(a,1)),rewrite(1824(4))]. given #308 (F,wt=13): 5029 (x ^ y)' ^ (x ^ (z ^ y)) = c_0'. [para(1762(a,1),3011(a,1,2))]. given #309 (T,wt=13): 5043 (x ^ y) ^ (y ^ z) = z ^ (x ^ y). [para(1762(a,1),1762(a,1,2)),rewrite(4914(6),1762(7))]. given #310 (T,wt=11): 5490 x ^ (y ^ z) = z ^ (x ^ y). [back_rewrite(5388),rewrite(5489(3))]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. ============================== PROOF ================================= % Proof 3 at 2.86 (+ 0.07) seconds: combined. % Length of proof is 130. % Level of proof is 28. % Maximum clause weight is 46. % Given clauses 310. 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]. 5 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(f(x,x),x)),z))) = y # label(OL_Sh). [assumption]. 6 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 7 f(f(x,x),f(y,y)) = x v y. [copy(6),flip(a)]. 8 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. 9 f(f(x,y),f(x,y)) = x ^ y. [copy(8),flip(a)]. 10 x' = f(x,x) # label(definition_complementation). [assumption]. 11 f(x,x) = x'. [copy(10),flip(a)]. 18 f(c8,f(f(c9,c10),f(c9,c10))) != f(c9,f(f(c8,c10),f(c8,c10))) | f(f(c8,c8),f(c8,c9)) != c8 | f(c8,f(c8,c8)) != f(c9,f(c9,c9)) # answer(combined). [deny(4)]. 19 f(c9,f(c8,c10)') != f(c8,f(c9,c10)') | f(c8',f(c8,c9)) != c8 | f(c9,c9') != f(c8,c8') # answer(combined). [copy(18),rewrite(11(8),11(14),11(16),11(25),11(29)),flip(a),flip(c)]. 20 f(x,y)' = x ^ y. [back_rewrite(9),rewrite(11(3))]. 21 f(x',y') = x v y. [back_rewrite(7),rewrite(11(1),11(2))]. 22 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(y,f(x',x)),z))) = y. [back_rewrite(5),rewrite(11(5))]. 23 f(c9,c8 ^ c10) != f(c8,c9 ^ c10) | f(c8',f(c8,c9)) != c8 | f(c9,c9') != f(c8,c8') # answer(combined). [back_rewrite(19),rewrite(20(5),20(10))]. 25 x ^ x = x''. [para(11(a,1),20(a,1,1)),flip(a)]. 27 (x v y)' = x' ^ y'. [para(21(a,1),20(a,1,1))]. 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))]. 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))]. 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))]. 43 f(x',y' ^ z') = x v (y v z). [para(27(a,1),21(a,1,2))]. 52 f(x' ^ y',z ^ u) = (x v y) v f(z,u). [para(27(a,1),29(a,1,1))]. 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))]. 194 (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)]. 217 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(181(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))]. 238 x' ^ f(x'',x) = x'''. [para(236(a,1),20(a,1,1)),flip(a)]. 240 f(x'',x'' v x) = x'''. [para(21(a,1),236(a,1,2))]. 261 x'' ^ (x'' v x) = x''''. [para(21(a,1),238(a,1,2))]. 306 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))]. 333 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))]. 401 x ^ f(f(x,y),f(x,y) ^ (x' v x)) = x ^ y. [para(306(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. 744 f(f(x,y),f(y,f(f(y,f(x',x)),z))) = y. [para(41(a,1),22(a,1,1))]. 755 f(x,y) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(41(a,1),36(a,1,1))]. 756 x ^ x'' = x''. [para(41(a,1),230(a,1,2,2)),rewrite(11(3))]. 762 f(x,y) ^ f(x,x ^ ((x ^ y) v f(x,y))) = x'. [para(41(a,1),401(a,1,2,1)),rewrite(41(17),20(3),333(23))]. 845 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),42(a,1,2,2))]. 871 f(x,x ^ y) = f(x,y). [para(41(a,1),42(a,1,2,2)),rewrite(11(3),20(2))]. 886 f(x,y) ^ f(x,(x ^ y) v f(x,y)) = x'. [back_rewrite(762),rewrite(871(6))]. 973 x ^ (x ^ y) = x ^ y. [para(871(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. 977 f(f(f(f(x,y),f(y,z)),u),y') = y. [para(22(a,1),871(a,2)),rewrite(36(14))]. 992 x'' v x = x. [para(181(a,1),871(a,2)),rewrite(217(12),21(5))]. 997 f(x'',x) = x'''. [para(240(a,1),871(a,2)),rewrite(992(7),871(6))]. 1018 f(f(x,y),x') = x. [para(41(a,1),871(a,2)),rewrite(333(17))]. 1048 x'' ^ x = x''''. [back_rewrite(261),rewrite(992(5))]. 1060 x''''' = x'. [para(992(a,1),27(a,1,1)),rewrite(1048(6)),flip(a)]. 1062 f(x,y) = (x ^ y)'''. [para(992(a,1),29(a,2)),rewrite(20(2),997(5)),flip(a)]. 1063 x v y = (x' ^ y')'''. [para(992(a,1),43(a,2,2)),rewrite(1048(6),1060(6),1062(3)),flip(a)]. 1065 (x' ^ (y ^ z)'''')''' = (x' ^ (y ^ z))'''. [para(992(a,1),52(a,2,1)),rewrite(1048(5),1060(5),1062(3),1062(7),1063(11)),flip(a)]. 1077 ((x ^ y)''' ^ x')''' = x. [back_rewrite(1018),rewrite(1062(1),1062(6))]. 1092 ((((x ^ y)''' ^ (y ^ z)''')''' ^ u)''' ^ y')''' = y. [back_rewrite(977),rewrite(1062(1),1062(5),1062(9),1062(13),1062(18))]. 1104 (x ^ y)''' ^ (x ^ ((x ^ y)' ^ (x ^ y))''')''' = x'. [back_rewrite(886),rewrite(1062(1),1062(6),1063(10),1065(15),1062(12))]. 1109 (x' ^ ((x' ^ (x ^ y)''')''' ^ x)''')''' = (x' ^ (x ^ y)''')'''. [back_rewrite(845),rewrite(1062(3),1062(7),1062(11),1062(15),1062(20),1062(24))]. 1128 (x ^ y)''' ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(755),rewrite(1062(1),1062(6),1062(10),1062(14),1062(18))]. 1130 x'''' = x. [back_rewrite(744),rewrite(1062(1),1062(6),1062(10),1062(14),1062(18),1062(22),1128(22))]. 1141 ((x ^ y)''' ^ (y ^ z)''') ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(194),rewrite(1062(1),1062(5),1062(11),1062(15),1062(19),1062(23))]. 1144 (c9 ^ (c8 ^ c10))''' != (c8 ^ (c9 ^ c10))''' | (c8' ^ (c8 ^ c9)''')''' != c8 | (c9 ^ c9')''' != (c8 ^ c8')''' # answer(combined). [back_rewrite(23),rewrite(1062(5),1062(13),1062(22),1062(26),1062(35),1062(42))]. 1152 x'' = x. [para(25(a,1),1077(a,1,1,1,1,1,1,1,1)),rewrite(1130(4),25(3),1130(4))]. 1155 (x ^ y)' ^ x' = x'. [para(1077(a,1),756(a,2,1)),rewrite(1152(3),1152(6),1152(7),1152(10),1152(10),25(9),1152(6))]. 1156 ((x' ^ y)' ^ x)' = x'. [para(1130(a,1),1077(a,1,1,1,1,2)),rewrite(1152(2),1152(4),1152(6),1152(7))]. 1161 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' | (c8' ^ (c8 ^ c9)')' != c8 | (c9 ^ c9')' != (c8 ^ c8')' # answer(combined). [back_rewrite(1144),rewrite(1152(7),1152(13),1152(20),1152(22),1152(29),1152(34))]. 1164 ((x ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1141),rewrite(1152(3),1152(5),1152(9),1152(11),1152(13),1152(15))]. 1172 (x ^ y)' ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1128),rewrite(1152(3),1152(6),1152(8),1152(10),1152(12))]. 1173 (x' ^ (x ^ y)')' = x. [back_rewrite(1109),rewrite(1152(5),1152(7),1156(8),1152(3),25(3),1152(2),1152(2),1152(2),1152(4),1152(6)),flip(a)]. 1179 (x ^ y)' ^ (x ^ ((x ^ y)' ^ (x ^ y))')' = x'. [back_rewrite(1104),rewrite(1152(3),1152(8),1152(10))]. 1183 ((((x ^ y)' ^ (y ^ z)')' ^ u)' ^ y')' = y. [back_rewrite(1092),rewrite(1152(3),1152(5),1152(7),1152(9),1152(12))]. 1191 x ^ x = x. [back_rewrite(25),rewrite(1152(3))]. 1192 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' | (c9 ^ c9')' != (c8 ^ c8')' # answer(combined). [back_rewrite(1161),rewrite(1173(21)),xx(b)]. 1194 (x' ^ y)' ^ x = x. [para(1152(a,1),1155(a,1,2)),rewrite(1152(6))]. 1195 x' ^ (x ^ y)' = x'. [para(1173(a,1),1152(a,1,1)),flip(a)]. 1202 x ^ ((y ^ x)' ^ (x ^ z)')' = ((y ^ x)' ^ (x ^ z)')'. [para(1164(a,1),1155(a,1,1,1)),rewrite(1152(2))]. 1204 ((x ^ (y ^ z)')' ^ y) ^ ((y ^ z)' ^ (((y ^ z)' ^ (x' ^ x)')' ^ y')')' = y ^ z. [para(1155(a,1),1164(a,1,1,2,1)),rewrite(1152(6),1152(23))]. 1210 x ^ (x' ^ y)' = x. [para(1152(a,1),1195(a,1,1)),rewrite(1152(6))]. 1211 (x ^ y) ^ x = x ^ y. [para(1155(a,1),1195(a,1,2,1)),rewrite(1152(3),1152(3),1152(5))]. 1215 ((x ^ y)' ^ (y ^ z)')' ^ y = ((x ^ y)' ^ (y ^ z)')'. [para(1164(a,1),1195(a,1,2,1)),rewrite(1152(8))]. 1220 x' ^ ((y ^ x)' ^ (x ^ z)') = x'. [para(1164(a,1),1211(a,1,1)),rewrite(1164(22))]. 1262 (x ^ y)' ^ y' = y'. [para(1172(a,1),973(a,1,2)),rewrite(1172(16))]. 1264 x ^ (y ^ x) = y ^ x. [para(1172(a,1),1155(a,1,1,1)),rewrite(1152(2),1152(3),1152(5))]. 1267 (x ^ y')' ^ y = y. [para(1194(a,1),1172(a,1,2,1,2,1)),rewrite(1191(6),1152(5),1152(6))]. 1269 x' ^ (y ^ x)' = x'. [para(1172(a,1),1211(a,1,1)),rewrite(1172(16))]. 1275 x ^ (y ^ x')' = x. [para(1264(a,1),1210(a,1,2,1))]. 1279 x' ^ ((y ^ x)' ^ (z ^ x)') = x'. [para(1264(a,1),1220(a,1,2,2,1))]. 1284 (x ^ (y ^ (x' ^ x))')' ^ ((y ^ (x' ^ x))' ^ ((x' ^ x) ^ z)')' = y ^ (x' ^ x). [para(1267(a,1),1172(a,1,2,1,2,1,1,1)),rewrite(1152(4),1152(10),1152(14),1152(21),1152(22))]. 1321 ((x ^ y)' ^ (y ^ y')')' = x ^ y. [para(1172(a,1),1179(a,1,1,1)),rewrite(1152(2),1172(14),1152(4),1172(14),1202(8),1152(10))]. 1347 (x ^ y) ^ (x ^ (z ^ (x ^ y)')') = x ^ y. [para(1195(a,1),1279(a,1,2,1,1)),rewrite(1152(3),1152(3),1152(10))]. 1358 (((x ^ y) ^ z)' ^ x')' = x. [para(1155(a,1),1183(a,1,1,1,1,1,1)),rewrite(1152(3))]. 1375 ((x ^ y) ^ z)' ^ x' = x'. [para(1358(a,1),1152(a,1,1)),flip(a)]. 1377 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(1358(a,1),1155(a,1,1)),rewrite(1152(4),1152(7))]. 1410 ((x' ^ y) ^ z)' ^ x = x. [para(1152(a,1),1375(a,1,2)),rewrite(1152(7))]. 1424 x ^ ((x' ^ y) ^ z)' = x. [para(1410(a,1),1211(a,1,1)),rewrite(1410(10))]. 1439 (x ^ y) ^ (y' ^ z)' = x ^ y. [para(1172(a,1),1424(a,1,2,1,1))]. 1440 x ^ ((y ^ x') ^ z)' = x. [para(1264(a,1),1424(a,1,2,1,1))]. 1441 x ^ (y ^ (x' ^ z))' = x. [para(1264(a,1),1424(a,1,2,1))]. 1447 x' ^ ((y ^ (x' ^ x))' ^ ((x' ^ x) ^ z)')' = y ^ (x' ^ x). [back_rewrite(1284),rewrite(1441(5))]. 1477 x ^ (y ^ (z ^ x'))' = x. [para(1264(a,1),1440(a,1,2,1))]. 1482 x' ^ (y ^ (x ^ z))' = x'. [para(1152(a,1),1441(a,1,2,1,2,1))]. 1510 x' ^ (y ^ (z ^ x))' = x'. [para(1152(a,1),1477(a,1,2,1,2,2))]. 1678 x ^ ((y ^ (x ^ z))' ^ ((x ^ z) ^ u)')' = ((y ^ (x ^ z))' ^ ((x ^ z) ^ u)')'. [para(1202(a,1),1377(a,1,2)),rewrite(1202(19))]. 1683 ((x ^ (y' ^ y))' ^ ((y' ^ y) ^ z)')' = x ^ (y' ^ y). [back_rewrite(1447),rewrite(1678(12))]. 1708 (x' ^ x) ^ y = x' ^ x. [para(1155(a,1),1204(a,1,2,1,2,1,1,1)),rewrite(1424(5),973(4),1152(10),1439(12),1155(10),1152(6),1191(5)),flip(a)]. 1714 (x ^ y) ^ (y ^ x) = y ^ x. [para(1269(a,1),1204(a,1,1,1,1)),rewrite(1152(2),1152(7),1321(10),1195(8),1152(4))]. 1737 (x ^ y) ^ ((y ^ (x ^ z))' ^ (((y ^ (x ^ z))' ^ (x ^ x')')' ^ y')')' = y ^ (x ^ z). [para(1482(a,1),1204(a,1,1,1,1)),rewrite(1152(2),1152(9))]. 1739 (x ^ y) ^ ((y ^ (z ^ x))' ^ (((y ^ (z ^ x))' ^ (x ^ x')')' ^ y')')' = y ^ (z ^ x). [para(1510(a,1),1204(a,1,1,1,1)),rewrite(1152(2),1152(9))]. 1742 x ^ (y' ^ y) = y' ^ y. [back_rewrite(1683),rewrite(1708(7),1262(8),1152(4)),flip(a)]. 1750 (x' ^ x)' ^ y = y. [para(1708(a,1),1267(a,1,1,1))]. 1751 x ^ (y' ^ y)' = x. [para(1708(a,1),1275(a,1,2,1))]. 1760 x ^ (y ^ y')' = x. [para(1152(a,1),1751(a,1,2,1,1))]. 1761 (x' ^ x)' = (y' ^ y)'. [para(1751(a,1),1750(a,1))]. 1762 (x ^ y) ^ (y ^ (z ^ x)) = y ^ (z ^ x). [back_rewrite(1739),rewrite(1760(11),1152(8),1195(10),1152(5))]. 1763 (x ^ y) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [back_rewrite(1737),rewrite(1760(11),1152(8),1195(10),1152(5))]. 1764 (x' ^ x)' = c_0. [new_symbol(1761)]. 1805 x' ^ x = c_0'. [para(1708(a,1),1215(a,1,1,1,2,1)),rewrite(1742(3),1764(3),1764(4),1191(3),1742(5),1742(5),1764(5),1708(6),1764(6),1191(5))]. 1810 x ^ x' = c_0'. [para(1152(a,1),1805(a,1,1))]. 1811 (c9 ^ (c8 ^ c10))' != (c8 ^ (c9 ^ c10))' # answer(combined). [back_rewrite(1192),rewrite(1810(17),1152(16),1810(18),1152(17)),xx(b)]. 1824 x ^ y = y ^ x. [para(1714(a,1),1211(a,1,1)),rewrite(1714(3),1714(4))]. 2782 (x ^ y) ^ (x ^ (z ^ y)) = x ^ (z ^ y). [para(1510(a,1),1347(a,1,2,2,1)),rewrite(1152(4),1824(4))]. 4914 (x ^ (y ^ z)) ^ (z ^ x) = x ^ (y ^ z). [para(1762(a,1),1714(a,1,2)),rewrite(1824(7),973(7),1762(8))]. 5043 (x ^ y) ^ (y ^ z) = z ^ (x ^ y). [para(1762(a,1),1762(a,1,2)),rewrite(4914(6),1762(7))]. 5386 (x ^ y) ^ (y ^ z) = (x ^ y) ^ z. [para(5043(a,2),1714(a,1,1)),rewrite(1824(6),2782(6))]. 5388 (x ^ y) ^ (x ^ z) = z ^ (y ^ x). [para(1824(a,1),5043(a,1,1))]. 5489 (x ^ y) ^ (x ^ z) = y ^ (x ^ z). [back_rewrite(1763),rewrite(5386(4))]. 5490 x ^ (y ^ z) = z ^ (x ^ y). [back_rewrite(5388),rewrite(5489(3))]. 5606 x ^ (y ^ z) = y ^ (x ^ z). [para(1824(a,1),5490(a,1,2))]. 6359 $F # answer(combined). [back_rewrite(1811),rewrite(5606(5)),xx(a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 4 at 2.86 (+ 0.07) seconds: assoc. % Length of proof is 113. % Level of proof is 28. % Maximum clause weight is 39. % Given clauses 310. 1 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(assoc) # 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)]. 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)]. 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))]. 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))]. 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))]. 43 f(x',y' ^ z') = x v (y v z). [para(27(a,1),21(a,1,2))]. 52 f(x' ^ y',z ^ u) = (x v y) v f(z,u). [para(27(a,1),29(a,1,1))]. 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))]. 194 (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)]. 217 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(181(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))]. 238 x' ^ f(x'',x) = x'''. [para(236(a,1),20(a,1,1)),flip(a)]. 240 f(x'',x'' v x) = x'''. [para(21(a,1),236(a,1,2))]. 261 x'' ^ (x'' v x) = x''''. [para(21(a,1),238(a,1,2))]. 306 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))]. 333 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))]. 401 x ^ f(f(x,y),f(x,y) ^ (x' v x)) = x ^ y. [para(306(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. 744 f(f(x,y),f(y,f(f(y,f(x',x)),z))) = y. [para(41(a,1),22(a,1,1))]. 755 f(x,y) ^ f(y,f(f(y,f(x',x)),z)) = y'. [para(41(a,1),36(a,1,1))]. 756 x ^ x'' = x''. [para(41(a,1),230(a,1,2,2)),rewrite(11(3))]. 762 f(x,y) ^ f(x,x ^ ((x ^ y) v f(x,y))) = x'. [para(41(a,1),401(a,1,2,1)),rewrite(41(17),20(3),333(23))]. 845 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [para(30(a,1),42(a,1,2,2))]. 871 f(x,x ^ y) = f(x,y). [para(41(a,1),42(a,1,2,2)),rewrite(11(3),20(2))]. 886 f(x,y) ^ f(x,(x ^ y) v f(x,y)) = x'. [back_rewrite(762),rewrite(871(6))]. 973 x ^ (x ^ y) = x ^ y. [para(871(a,1),20(a,1,1)),rewrite(20(2)),flip(a)]. 977 f(f(f(f(x,y),f(y,z)),u),y') = y. [para(22(a,1),871(a,2)),rewrite(36(14))]. 992 x'' v x = x. [para(181(a,1),871(a,2)),rewrite(217(12),21(5))]. 997 f(x'',x) = x'''. [para(240(a,1),871(a,2)),rewrite(992(7),871(6))]. 1018 f(f(x,y),x') = x. [para(41(a,1),871(a,2)),rewrite(333(17))]. 1048 x'' ^ x = x''''. [back_rewrite(261),rewrite(992(5))]. 1060 x''''' = x'. [para(992(a,1),27(a,1,1)),rewrite(1048(6)),flip(a)]. 1062 f(x,y) = (x ^ y)'''. [para(992(a,1),29(a,2)),rewrite(20(2),997(5)),flip(a)]. 1063 x v y = (x' ^ y')'''. [para(992(a,1),43(a,2,2)),rewrite(1048(6),1060(6),1062(3)),flip(a)]. 1065 (x' ^ (y ^ z)'''')''' = (x' ^ (y ^ z))'''. [para(992(a,1),52(a,2,1)),rewrite(1048(5),1060(5),1062(3),1062(7),1063(11)),flip(a)]. 1077 ((x ^ y)''' ^ x')''' = x. [back_rewrite(1018),rewrite(1062(1),1062(6))]. 1092 ((((x ^ y)''' ^ (y ^ z)''')''' ^ u)''' ^ y')''' = y. [back_rewrite(977),rewrite(1062(1),1062(5),1062(9),1062(13),1062(18))]. 1104 (x ^ y)''' ^ (x ^ ((x ^ y)' ^ (x ^ y))''')''' = x'. [back_rewrite(886),rewrite(1062(1),1062(6),1063(10),1065(15),1062(12))]. 1109 (x' ^ ((x' ^ (x ^ y)''')''' ^ x)''')''' = (x' ^ (x ^ y)''')'''. [back_rewrite(845),rewrite(1062(3),1062(7),1062(11),1062(15),1062(20),1062(24))]. 1128 (x ^ y)''' ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(755),rewrite(1062(1),1062(6),1062(10),1062(14),1062(18))]. 1130 x'''' = x. [back_rewrite(744),rewrite(1062(1),1062(6),1062(10),1062(14),1062(18),1062(22),1128(22))]. 1141 ((x ^ y)''' ^ (y ^ z)''') ^ (y ^ ((y ^ (x' ^ x)''')''' ^ z)''')''' = y'. [back_rewrite(194),rewrite(1062(1),1062(5),1062(11),1062(15),1062(19),1062(23))]. 1143 (c2 ^ (c1 ^ c3))''' != (c1 ^ (c2 ^ c3))''' # answer(assoc). [back_rewrite(24),rewrite(1062(5),1062(13))]. 1152 x'' = x. [para(25(a,1),1077(a,1,1,1,1,1,1,1,1)),rewrite(1130(4),25(3),1130(4))]. 1155 (x ^ y)' ^ x' = x'. [para(1077(a,1),756(a,2,1)),rewrite(1152(3),1152(6),1152(7),1152(10),1152(10),25(9),1152(6))]. 1156 ((x' ^ y)' ^ x)' = x'. [para(1130(a,1),1077(a,1,1,1,1,2)),rewrite(1152(2),1152(4),1152(6),1152(7))]. 1162 (c2 ^ (c1 ^ c3))' != (c1 ^ (c2 ^ c3))' # answer(assoc). [back_rewrite(1143),rewrite(1152(7),1152(13))]. 1164 ((x ^ y)' ^ (y ^ z)') ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1141),rewrite(1152(3),1152(5),1152(9),1152(11),1152(13),1152(15))]. 1172 (x ^ y)' ^ (y ^ ((y ^ (x' ^ x)')' ^ z)')' = y'. [back_rewrite(1128),rewrite(1152(3),1152(6),1152(8),1152(10),1152(12))]. 1173 (x' ^ (x ^ y)')' = x. [back_rewrite(1109),rewrite(1152(5),1152(7),1156(8),1152(3),25(3),1152(2),1152(2),1152(2),1152(4),1152(6)),flip(a)]. 1179 (x ^ y)' ^ (x ^ ((x ^ y)' ^ (x ^ y))')' = x'. [back_rewrite(1104),rewrite(1152(3),1152(8),1152(10))]. 1183 ((((x ^ y)' ^ (y ^ z)')' ^ u)' ^ y')' = y. [back_rewrite(1092),rewrite(1152(3),1152(5),1152(7),1152(9),1152(12))]. 1191 x ^ x = x. [back_rewrite(25),rewrite(1152(3))]. 1195 x' ^ (x ^ y)' = x'. [para(1173(a,1),1152(a,1,1)),flip(a)]. 1202 x ^ ((y ^ x)' ^ (x ^ z)')' = ((y ^ x)' ^ (x ^ z)')'. [para(1164(a,1),1155(a,1,1,1)),rewrite(1152(2))]. 1204 ((x ^ (y ^ z)')' ^ y) ^ ((y ^ z)' ^ (((y ^ z)' ^ (x' ^ x)')' ^ y')')' = y ^ z. [para(1155(a,1),1164(a,1,1,2,1)),rewrite(1152(6),1152(23))]. 1210 x ^ (x' ^ y)' = x. [para(1152(a,1),1195(a,1,1)),rewrite(1152(6))]. 1211 (x ^ y) ^ x = x ^ y. [para(1155(a,1),1195(a,1,2,1)),rewrite(1152(3),1152(3),1152(5))]. 1220 x' ^ ((y ^ x)' ^ (x ^ z)') = x'. [para(1164(a,1),1211(a,1,1)),rewrite(1164(22))]. 1264 x ^ (y ^ x) = y ^ x. [para(1172(a,1),1155(a,1,1,1)),rewrite(1152(2),1152(3),1152(5))]. 1269 x' ^ (y ^ x)' = x'. [para(1172(a,1),1211(a,1,1)),rewrite(1172(16))]. 1275 x ^ (y ^ x')' = x. [para(1264(a,1),1210(a,1,2,1))]. 1279 x' ^ ((y ^ x)' ^ (z ^ x)') = x'. [para(1264(a,1),1220(a,1,2,2,1))]. 1321 ((x ^ y)' ^ (y ^ y')')' = x ^ y. [para(1172(a,1),1179(a,1,1,1)),rewrite(1152(2),1172(14),1152(4),1172(14),1202(8),1152(10))]. 1347 (x ^ y) ^ (x ^ (z ^ (x ^ y)')') = x ^ y. [para(1195(a,1),1279(a,1,2,1,1)),rewrite(1152(3),1152(3),1152(10))]. 1358 (((x ^ y) ^ z)' ^ x')' = x. [para(1155(a,1),1183(a,1,1,1,1,1,1)),rewrite(1152(3))]. 1375 ((x ^ y) ^ z)' ^ x' = x'. [para(1358(a,1),1152(a,1,1)),flip(a)]. 1410 ((x' ^ y) ^ z)' ^ x = x. [para(1152(a,1),1375(a,1,2)),rewrite(1152(7))]. 1424 x ^ ((x' ^ y) ^ z)' = x. [para(1410(a,1),1211(a,1,1)),rewrite(1410(10))]. 1439 (x ^ y) ^ (y' ^ z)' = x ^ y. [para(1172(a,1),1424(a,1,2,1,1))]. 1440 x ^ ((y ^ x') ^ z)' = x. [para(1264(a,1),1424(a,1,2,1,1))]. 1441 x ^ (y ^ (x' ^ z))' = x. [para(1264(a,1),1424(a,1,2,1))]. 1477 x ^ (y ^ (z ^ x'))' = x. [para(1264(a,1),1440(a,1,2,1))]. 1482 x' ^ (y ^ (x ^ z))' = x'. [para(1152(a,1),1441(a,1,2,1,2,1))]. 1510 x' ^ (y ^ (z ^ x))' = x'. [para(1152(a,1),1477(a,1,2,1,2,2))]. 1708 (x' ^ x) ^ y = x' ^ x. [para(1155(a,1),1204(a,1,2,1,2,1,1,1)),rewrite(1424(5),973(4),1152(10),1439(12),1155(10),1152(6),1191(5)),flip(a)]. 1714 (x ^ y) ^ (y ^ x) = y ^ x. [para(1269(a,1),1204(a,1,1,1,1)),rewrite(1152(2),1152(7),1321(10),1195(8),1152(4))]. 1737 (x ^ y) ^ ((y ^ (x ^ z))' ^ (((y ^ (x ^ z))' ^ (x ^ x')')' ^ y')')' = y ^ (x ^ z). [para(1482(a,1),1204(a,1,1,1,1)),rewrite(1152(2),1152(9))]. 1739 (x ^ y) ^ ((y ^ (z ^ x))' ^ (((y ^ (z ^ x))' ^ (x ^ x')')' ^ y')')' = y ^ (z ^ x). [para(1510(a,1),1204(a,1,1,1,1)),rewrite(1152(2),1152(9))]. 1751 x ^ (y' ^ y)' = x. [para(1708(a,1),1275(a,1,2,1))]. 1760 x ^ (y ^ y')' = x. [para(1152(a,1),1751(a,1,2,1,1))]. 1762 (x ^ y) ^ (y ^ (z ^ x)) = y ^ (z ^ x). [back_rewrite(1739),rewrite(1760(11),1152(8),1195(10),1152(5))]. 1763 (x ^ y) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [back_rewrite(1737),rewrite(1760(11),1152(8),1195(10),1152(5))]. 1824 x ^ y = y ^ x. [para(1714(a,1),1211(a,1,1)),rewrite(1714(3),1714(4))]. 2782 (x ^ y) ^ (x ^ (z ^ y)) = x ^ (z ^ y). [para(1510(a,1),1347(a,1,2,2,1)),rewrite(1152(4),1824(4))]. 4914 (x ^ (y ^ z)) ^ (z ^ x) = x ^ (y ^ z). [para(1762(a,1),1714(a,1,2)),rewrite(1824(7),973(7),1762(8))]. 5043 (x ^ y) ^ (y ^ z) = z ^ (x ^ y). [para(1762(a,1),1762(a,1,2)),rewrite(4914(6),1762(7))]. 5386 (x ^ y) ^ (y ^ z) = (x ^ y) ^ z. [para(5043(a,2),1714(a,1,1)),rewrite(1824(6),2782(6))]. 5388 (x ^ y) ^ (x ^ z) = z ^ (y ^ x). [para(1824(a,1),5043(a,1,1))]. 5489 (x ^ y) ^ (x ^ z) = y ^ (x ^ z). [back_rewrite(1763),rewrite(5386(4))]. 5490 x ^ (y ^ z) = z ^ (x ^ y). [back_rewrite(5388),rewrite(5489(3))]. 5606 x ^ (y ^ z) = y ^ (x ^ z). [para(1824(a,1),5490(a,1,2))]. 6364 $F # answer(assoc). [back_rewrite(1162),rewrite(5606(5)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=310. Generated=105036. Kept=6348. proofs=4. Usable=53. Sos=539. Demods=1234. Limbo=757, Disabled=5007. Hints=0. Weight_deleted=4856. Literals_deleted=0. Forward_subsumed=93828. Back_subsumed=159. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=5987 (5 lex), Back_demodulated=4839. Back_unit_deleted=0. Demod_attempts=2049260. Demod_rewrites=339459. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=5. Megabytes=6.17. User_CPU=2.87, System_CPU=0.07, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 4 proofs. Process 3924 exit (max_proofs) Wed Nov 22 11:25:09 2006