----- Otter 3.0.3d, Feb 1995 ----- The job was started by mccune on altair.mcs.anl.gov, Mon Mar 6 14:51:43 1995 The command was "otter3". op(400,xfx,^). op(400,xfx,v). set(knuth_bendix). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(process_input). dependent: set(lrpo). clear(print_kept). clear(print_new_demod). clear(print_back_demod). assign(max_mem,16000). assign(max_proofs,6). assign(max_weight,155). assign(change_limit_after,2). assign(new_max_weight,60). list(usable). 0 [] x=x. end_of_list. list(sos). 0 [] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^x1) v (x2^y)) v y)) v (((y^ (((y v x1)^ (x2 v y))^y)) v (u^ (y v (((y v x1)^ (x2 v y))^y))))^ (x v (((y^x1) v (x2^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. end_of_list. list(passive). 1 [] A^A!=A|$Ans(idem_meet). 2 [] A^B!=B^A|$Ans(comm_meet). 3 [] ((A v C)^ (B v C))^C!=C|$Ans(a3_meet). 4 [] A v A!=A|$Ans(idem_join). 5 [] A v B!=B v A|$Ans(comm_join). 6 [] ((A^C) v (B^C)) v C!=C|$Ans(a3_join). end_of_list. ------------> process usable: ** KEPT (wt=3): 7 [] x=x. Following clause subsumed by 7 during input processing: 0 [copy,7,flip.1] x=x. ------------> process sos: ** KEPT (wt=75): 8 [] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((y^ (((y v u)^ (v v y))^y)) v (w^ (y v (((y v u)^ (v v y))^y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. ---> New Demodulator: 9 [new_demod,8] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((y^ (((y v u)^ (v v y))^y)) v (w^ (y v (((y v u)^ (v v y))^y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. >>>> Starting back demodulation with 9. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=75) 8 [] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((y^ (((y v u)^ (v v y))^y)) v (w^ (y v (((y v u)^ (v v y))^y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. given clause #2: (wt=155) 10 [para_into,8.1.1.2.1.2.1,8.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^ (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z))))) v (z^ (x v (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z)))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). reducing weight limit to 60. given clause #3: (wt=99) 12 [para_into,10.1.1.1.1.1.2,8.1.1,demod,9,9,9,9,9,9,9,9,9,9,9,9] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((w^ (((y^v6) v (v7^y)) v y)) v (((y^ (((y v v6)^ (v7 v y))^y)) v (v8^ (y v (((y v v6)^ (v7 v y))^y))))^ (w v (((y^v6) v (v7^y)) v y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. given clause #4: (wt=59) 14 [para_into,12.1.1.2.1,8.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. given clause #5: (wt=11) 18 [para_into,14.1.1.1.1,14.1.1,demod,15] (x^y) v (x^ (x v y))=x. given clause #6: (wt=19) 22 [para_into,18.1.1.2.2,18.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. given clause #7: (wt=39) 26 [para_into,22.1.1.1.2.2,18.1.1] (((x^y)^ (x^ (x v y)))^ ((x^y)^x)) v (((x^y)^ (x^ (x v y)))^ (x^y))= (x^y)^ (x^ (x v y)). given clause #8: (wt=51) 20 [para_from,14.1.1,10.1.1.2.1.2.2.2.2,demod,15,15,15,15,15,15,15,15,15,15,15,15] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (y^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. given clause #9: (wt=27) 28 [para_into,20.1.1.1.1,20.1.1,demod,21,21,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (y^ (x v (((y^z) v (u^y)) v y)))=y. given clause #10: (wt=27) 36 [back_demod,20,demod,29] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. given clause #11: (wt=51) 30 [para_into,20.1.1.2.1,8.1.1,demod,9,9,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (((y^ (((y v z)^ (u v y))^y)) v (v^ (y v (((y v z)^ (u v y))^y))))^ (x v (((y^z) v (u^y)) v y)))=y. given clause #12: (wt=27) 42 [para_into,30.1.1,36.1.1] (x^ (((x v y)^ (z v x))^x)) v (u^ (x v (((x v y)^ (z v x))^x)))=x. given clause #13: (wt=11) 50 [para_into,42.1.1,36.1.1,flip.1] (x^y) v (y^ (x v y))=y. given clause #14: (wt=11) 64 [para_into,50.1.1,42.1.1,flip.1] ((x v y)^ (z v x))^x=x. given clause #15: (wt=11) 70 [back_demod,42,demod,65,65] (x^x) v (y^ (x v x))=x. given clause #16: (wt=9) 108 [para_into,70.1.1.2,64.1.1] (x^x) v (x v x)=x. given clause #17: (wt=11) 110 [para_into,70.1.1,28.1.1,flip.1] ((x^y) v (z^x)) v x=x. given clause #18: (wt=9) 126 [para_into,110.1.1.1.2,64.1.1] ((x^y) v x) v x=x. given clause #19: (wt=9) 128 [para_from,110.1.1,64.1.1.1.2] ((x v y)^x)^x=x. given clause #20: (wt=13) 146 [para_from,126.1.1,50.1.1.2.2] (((x^y) v x)^x) v (x^x)=x. given clause #21: (wt=13) 154 [para_into,128.1.1.1.1,50.1.1] (x^ (y^x))^ (y^x)=y^x. given clause #22: (wt=7) 188 [para_into,154.1.1.1.2,128.1.1,demod,129,129] (x^x)^x=x. given clause #23: (wt=11) 218 [para_from,188.1.1,50.1.1.1] x v (x^ ((x^x) v x))=x. given clause #24: (wt=9) 226 [para_from,218.1.1,64.1.1.1.1] (x^ (y v x))^x=x. given clause #25: (wt=9) 238 [para_into,226.1.1.1.2,146.1.1,demod,189] x^ (x^x)=x^x. given clause #26: (wt=11) 280 [para_from,238.1.1,154.1.1.1] (x^x)^ (x^x)=x^x. given clause #27: (wt=13) 160 [para_into,128.1.1.1.1,18.1.1] (x^ (x^y))^ (x^y)=x^y. ----> UNIT CONFLICT at 23.66 sec ----> 312 [binary,310.1,1.1] $Ans(idem_meet). Length of proof is 20. Level of proof is 17. ---------------- PROOF ---------------- 1 [] A^A!=A|$Ans(idem_meet). 9,8 [] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((y^ (((y v u)^ (v v y))^y)) v (w^ (y v (((y v u)^ (v v y))^y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 10 [para_into,8.1.1.2.1.2.1,8.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^ (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z))))) v (z^ (x v (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z)))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). 12 [para_into,10.1.1.1.1.1.2,8.1.1,demod,9,9,9,9,9,9,9,9,9,9,9,9] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((w^ (((y^v6) v (v7^y)) v y)) v (((y^ (((y v v6)^ (v7 v y))^y)) v (v8^ (y v (((y v v6)^ (v7 v y))^y))))^ (w v (((y^v6) v (v7^y)) v y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 15,14 [para_into,12.1.1.2.1,8.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. 19,18 [para_into,14.1.1.1.1,14.1.1,demod,15] (x^y) v (x^ (x v y))=x. 21,20 [para_from,14.1.1,10.1.1.2.1.2.2.2.2,demod,15,15,15,15,15,15,15,15,15,15,15,15] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (y^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 29,28 [para_into,20.1.1.1.1,20.1.1,demod,21,21,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (y^ (x v (((y^z) v (u^y)) v y)))=y. 30 [para_into,20.1.1.2.1,8.1.1,demod,9,9,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (((y^ (((y v z)^ (u v y))^y)) v (v^ (y v (((y v z)^ (u v y))^y))))^ (x v (((y^z) v (u^y)) v y)))=y. 36 [back_demod,20,demod,29] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 42 [para_into,30.1.1,36.1.1] (x^ (((x v y)^ (z v x))^x)) v (u^ (x v (((x v y)^ (z v x))^x)))=x. 50 [para_into,42.1.1,36.1.1,flip.1] (x^y) v (y^ (x v y))=y. 65,64 [para_into,50.1.1,42.1.1,flip.1] ((x v y)^ (z v x))^x=x. 70 [back_demod,42,demod,65,65] (x^x) v (y^ (x v x))=x. 110 [para_into,70.1.1,28.1.1,flip.1] ((x^y) v (z^x)) v x=x. 129,128 [para_from,110.1.1,64.1.1.1.2] ((x v y)^x)^x=x. 154 [para_into,128.1.1.1.1,50.1.1] (x^ (y^x))^ (y^x)=y^x. 160 [para_into,128.1.1.1.1,18.1.1] (x^ (x^y))^ (x^y)=x^y. 188 [para_into,154.1.1.1.2,128.1.1,demod,129,129] (x^x)^x=x. 218 [para_from,188.1.1,50.1.1.1] x v (x^ ((x^x) v x))=x. 227,226 [para_from,218.1.1,64.1.1.1.1] (x^ (y v x))^x=x. 310 [para_into,160.1.1.1.2,226.1.1,demod,227,227,227] x^x=x. 312 [binary,310.1,1.1] $Ans(idem_meet). ------------ end of proof ------------- ----> UNIT CONFLICT at 23.80 sec ----> 333 [binary,331.1,4.1] $Ans(idem_join). Length of proof is 34. Level of proof is 21. ---------------- PROOF ---------------- 4 [] A v A!=A|$Ans(idem_join). 9,8 [] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((y^ (((y v u)^ (v v y))^y)) v (w^ (y v (((y v u)^ (v v y))^y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 10 [para_into,8.1.1.2.1.2.1,8.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^ (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z))))) v (z^ (x v (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z)))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). 12 [para_into,10.1.1.1.1.1.2,8.1.1,demod,9,9,9,9,9,9,9,9,9,9,9,9] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((w^ (((y^v6) v (v7^y)) v y)) v (((y^ (((y v v6)^ (v7 v y))^y)) v (v8^ (y v (((y v v6)^ (v7 v y))^y))))^ (w v (((y^v6) v (v7^y)) v y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 15,14 [para_into,12.1.1.2.1,8.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. 19,18 [para_into,14.1.1.1.1,14.1.1,demod,15] (x^y) v (x^ (x v y))=x. 21,20 [para_from,14.1.1,10.1.1.2.1.2.2.2.2,demod,15,15,15,15,15,15,15,15,15,15,15,15] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (y^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 22 [para_into,18.1.1.2.2,18.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 26 [para_into,22.1.1.1.2.2,18.1.1] (((x^y)^ (x^ (x v y)))^ ((x^y)^x)) v (((x^y)^ (x^ (x v y)))^ (x^y))= (x^y)^ (x^ (x v y)). 29,28 [para_into,20.1.1.1.1,20.1.1,demod,21,21,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (y^ (x v (((y^z) v (u^y)) v y)))=y. 30 [para_into,20.1.1.2.1,8.1.1,demod,9,9,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (((y^ (((y v z)^ (u v y))^y)) v (v^ (y v (((y v z)^ (u v y))^y))))^ (x v (((y^z) v (u^y)) v y)))=y. 36 [back_demod,20,demod,29] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 42 [para_into,30.1.1,36.1.1] (x^ (((x v y)^ (z v x))^x)) v (u^ (x v (((x v y)^ (z v x))^x)))=x. 50 [para_into,42.1.1,36.1.1,flip.1] (x^y) v (y^ (x v y))=y. 65,64 [para_into,50.1.1,42.1.1,flip.1] ((x v y)^ (z v x))^x=x. 70 [back_demod,42,demod,65,65] (x^x) v (y^ (x v x))=x. 110 [para_into,70.1.1,28.1.1,flip.1] ((x^y) v (z^x)) v x=x. 126 [para_into,110.1.1.1.2,64.1.1] ((x^y) v x) v x=x. 129,128 [para_from,110.1.1,64.1.1.1.2] ((x v y)^x)^x=x. 146 [para_from,126.1.1,50.1.1.2.2] (((x^y) v x)^x) v (x^x)=x. 154 [para_into,128.1.1.1.1,50.1.1] (x^ (y^x))^ (y^x)=y^x. 160 [para_into,128.1.1.1.1,18.1.1] (x^ (x^y))^ (x^y)=x^y. 189,188 [para_into,154.1.1.1.2,128.1.1,demod,129,129] (x^x)^x=x. 218 [para_from,188.1.1,50.1.1.1] x v (x^ ((x^x) v x))=x. 227,226 [para_from,218.1.1,64.1.1.1.1] (x^ (y v x))^x=x. 228 [para_from,218.1.1,22.1.1.1.2.2] ((x^ (x^ ((x^x) v x)))^ (x^x)) v ((x^ (x^ ((x^x) v x)))^x)=x^ (x^ ((x^x) v x)). 238 [para_into,226.1.1.1.2,146.1.1,demod,189] x^ (x^x)=x^x. 245,244 [para_into,226.1.1.1.2,50.1.1,demod,227] x^ (x^ (y v x))=x^ (y v x). 256 [back_demod,228,demod,245,245,227,245] ((x^ ((x^x) v x))^ (x^x)) v x=x^ ((x^x) v x). 281,280 [para_from,238.1.1,154.1.1.1] (x^x)^ (x^x)=x^x. 300 [para_from,280.1.1,146.1.1.1.1.1,demod,281] (((x^x) v (x^x))^ (x^x)) v (x^x)=x^x. 306 [para_from,280.1.1,26.1.1.2.2,demod,281,245,281,281,227,281,245,227,281,245,flip.1] (x^x)^ ((x^x) v (x^x))= (x^x) v (x^x). 311,310 [para_into,160.1.1.1.2,226.1.1,demod,227,227,227] x^x=x. 316,315 [back_demod,306,demod,311,311,311,311,311] x^ (x v x)=x v x. 322,321 [back_demod,300,demod,311,311,311,311,311] ((x v x)^x) v x=x. 331 [back_demod,256,demod,311,316,311,322,311,316,flip.1] x v x=x. 333 [binary,331.1,4.1] $Ans(idem_join). ------------ end of proof ------------- given clause #28: (wt=5) 310 [para_into,160.1.1.1.2,226.1.1,demod,227,227,227] x^x=x. given clause #29: (wt=5) 331 [back_demod,256,demod,311,316,311,322,311,316,flip.1] x v x=x. given clause #30: (wt=7) 354 [back_demod,70,demod,311,332] x v (y^x)=x. given clause #31: (wt=7) 372 [back_demod,162,demod,355,355,flip.1] (x v y)^x=x. given clause #32: (wt=7) 378 [back_demod,336,demod,371] (x^y) v y=y. given clause #33: (wt=9) 370 [back_demod,202,demod,355,355,flip.1] x^ (y^x)=y^x. ----> UNIT CONFLICT at 24.27 sec ----> 406 [binary,404.1,6.1] $Ans(a3_join). Length of proof is 38. Level of proof is 24. ---------------- PROOF ---------------- 6 [] ((A^C) v (B^C)) v C!=C|$Ans(a3_join). 9,8 [] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((y^ (((y v u)^ (v v y))^y)) v (w^ (y v (((y v u)^ (v v y))^y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 10 [para_into,8.1.1.2.1.2.1,8.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^ (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z))))) v (z^ (x v (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z)))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). 12 [para_into,10.1.1.1.1.1.2,8.1.1,demod,9,9,9,9,9,9,9,9,9,9,9,9] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((w^ (((y^v6) v (v7^y)) v y)) v (((y^ (((y v v6)^ (v7 v y))^y)) v (v8^ (y v (((y v v6)^ (v7 v y))^y))))^ (w v (((y^v6) v (v7^y)) v y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 15,14 [para_into,12.1.1.2.1,8.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. 19,18 [para_into,14.1.1.1.1,14.1.1,demod,15] (x^y) v (x^ (x v y))=x. 21,20 [para_from,14.1.1,10.1.1.2.1.2.2.2.2,demod,15,15,15,15,15,15,15,15,15,15,15,15] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (y^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 22 [para_into,18.1.1.2.2,18.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 26 [para_into,22.1.1.1.2.2,18.1.1] (((x^y)^ (x^ (x v y)))^ ((x^y)^x)) v (((x^y)^ (x^ (x v y)))^ (x^y))= (x^y)^ (x^ (x v y)). 29,28 [para_into,20.1.1.1.1,20.1.1,demod,21,21,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (y^ (x v (((y^z) v (u^y)) v y)))=y. 30 [para_into,20.1.1.2.1,8.1.1,demod,9,9,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (((y^ (((y v z)^ (u v y))^y)) v (v^ (y v (((y v z)^ (u v y))^y))))^ (x v (((y^z) v (u^y)) v y)))=y. 36 [back_demod,20,demod,29] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 42 [para_into,30.1.1,36.1.1] (x^ (((x v y)^ (z v x))^x)) v (u^ (x v (((x v y)^ (z v x))^x)))=x. 50 [para_into,42.1.1,36.1.1,flip.1] (x^y) v (y^ (x v y))=y. 65,64 [para_into,50.1.1,42.1.1,flip.1] ((x v y)^ (z v x))^x=x. 70 [back_demod,42,demod,65,65] (x^x) v (y^ (x v x))=x. 110 [para_into,70.1.1,28.1.1,flip.1] ((x^y) v (z^x)) v x=x. 126 [para_into,110.1.1.1.2,64.1.1] ((x^y) v x) v x=x. 129,128 [para_from,110.1.1,64.1.1.1.2] ((x v y)^x)^x=x. 146 [para_from,126.1.1,50.1.1.2.2] (((x^y) v x)^x) v (x^x)=x. 154 [para_into,128.1.1.1.1,50.1.1] (x^ (y^x))^ (y^x)=y^x. 160 [para_into,128.1.1.1.1,18.1.1] (x^ (x^y))^ (x^y)=x^y. 189,188 [para_into,154.1.1.1.2,128.1.1,demod,129,129] (x^x)^x=x. 202 [para_from,154.1.1,126.1.1.1.1] ((x^y) v (y^ (x^y))) v (y^ (x^y))=y^ (x^y). 218 [para_from,188.1.1,50.1.1.1] x v (x^ ((x^x) v x))=x. 227,226 [para_from,218.1.1,64.1.1.1.1] (x^ (y v x))^x=x. 228 [para_from,218.1.1,22.1.1.1.2.2] ((x^ (x^ ((x^x) v x)))^ (x^x)) v ((x^ (x^ ((x^x) v x)))^x)=x^ (x^ ((x^x) v x)). 238 [para_into,226.1.1.1.2,146.1.1,demod,189] x^ (x^x)=x^x. 245,244 [para_into,226.1.1.1.2,50.1.1,demod,227] x^ (x^ (y v x))=x^ (y v x). 256 [back_demod,228,demod,245,245,227,245] ((x^ ((x^x) v x))^ (x^x)) v x=x^ ((x^x) v x). 281,280 [para_from,238.1.1,154.1.1.1] (x^x)^ (x^x)=x^x. 300 [para_from,280.1.1,146.1.1.1.1.1,demod,281] (((x^x) v (x^x))^ (x^x)) v (x^x)=x^x. 306 [para_from,280.1.1,26.1.1.2.2,demod,281,245,281,281,227,281,245,227,281,245,flip.1] (x^x)^ ((x^x) v (x^x))= (x^x) v (x^x). 311,310 [para_into,160.1.1.1.2,226.1.1,demod,227,227,227] x^x=x. 316,315 [back_demod,306,demod,311,311,311,311,311] x^ (x v x)=x v x. 322,321 [back_demod,300,demod,311,311,311,311,311] ((x v x)^x) v x=x. 332,331 [back_demod,256,demod,311,316,311,322,311,316,flip.1] x v x=x. 355,354 [back_demod,70,demod,311,332] x v (y^x)=x. 370 [back_demod,202,demod,355,355,flip.1] x^ (y^x)=y^x. 404 [para_from,370.1.1,110.1.1.1.1] ((x^y) v (z^y)) v y=y. 406 [binary,404.1,6.1] $Ans(a3_join). ------------ end of proof ------------- given clause #34: (wt=9) 376 [back_demod,338,demod,371,371] (x^y)^y=x^y. given clause #35: (wt=9) 380 [back_demod,160,demod,377] x^ (x^y)=x^y. given clause #36: (wt=11) 390 [back_demod,272,demod,385] x v ((x^ (y v x)) v x)=x. given clause #37: (wt=11) 396 [para_from,372.1.1,50.1.1.1] x v (x^ ((x v y) v x))=x. given clause #38: (wt=9) 429 [para_from,396.1.1,22.1.1.1.2.2,demod,381,311,227,381,227,332,381,flip.1] x^ ((x v y) v x)=x. given clause #39: (wt=9) 441 [para_from,429.1.1,370.1.1.2,demod,430] ((x v y) v x)^x=x. given clause #40: (wt=11) 404 [para_from,370.1.1,110.1.1.1.1] ((x^y) v (z^y)) v y=y. given clause #41: (wt=13) 360 [back_demod,144,demod,332] ((x^y) v x)^x= (x^y) v x. given clause #42: (wt=9) 487 [para_from,360.1.1,354.1.1.2] x v ((x^y) v x)=x. given clause #43: (wt=13) 384 [back_demod,148,demod,377] x^ ((x^y) v x)= (x^y) v x. given clause #44: (wt=7) 503 [para_from,384.1.1,226.1.1.1,demod,361] (x^y) v x=x. given clause #45: (wt=7) 505 [back_demod,278,demod,504,227,332,flip.1] x^ (y v x)=x. given clause #46: (wt=7) 515 [back_demod,400,demod,514,332] x^ (x v y)=x. given clause #47: (wt=7) 523 [para_from,505.1.1,370.1.1.2,demod,506] (x v y)^y=y. given clause #48: (wt=9) 509 [back_demod,499,demod,506,flip.1] x v (x v y)=x v y. given clause #49: (wt=9) 517 [back_demod,411,demod,516,332] (x^y)^x=x^y. given clause #50: (wt=7) 541 [para_from,517.1.1,354.1.1.2] x v (x^y)=x. given clause #51: (wt=9) 525 [para_from,505.1.1,354.1.1.2] (x v y) v y=x v y. given clause #52: (wt=9) 531 [para_from,505.1.1,378.1.1.1] x v (y v x)=y v x. ----> UNIT CONFLICT at 25.35 sec ----> 551 [binary,549.1,3.1] $Ans(a3_meet). Length of proof is 55. Level of proof is 29. ---------------- PROOF ---------------- 3 [] ((A v C)^ (B v C))^C!=C|$Ans(a3_meet). 9,8 [] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((y^ (((y v u)^ (v v y))^y)) v (w^ (y v (((y v u)^ (v v y))^y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 10 [para_into,8.1.1.2.1.2.1,8.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^ (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z))))) v (z^ (x v (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z)))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). 12 [para_into,10.1.1.1.1.1.2,8.1.1,demod,9,9,9,9,9,9,9,9,9,9,9,9] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((w^ (((y^v6) v (v7^y)) v y)) v (((y^ (((y v v6)^ (v7 v y))^y)) v (v8^ (y v (((y v v6)^ (v7 v y))^y))))^ (w v (((y^v6) v (v7^y)) v y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 15,14 [para_into,12.1.1.2.1,8.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. 19,18 [para_into,14.1.1.1.1,14.1.1,demod,15] (x^y) v (x^ (x v y))=x. 21,20 [para_from,14.1.1,10.1.1.2.1.2.2.2.2,demod,15,15,15,15,15,15,15,15,15,15,15,15] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (y^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 22 [para_into,18.1.1.2.2,18.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 26 [para_into,22.1.1.1.2.2,18.1.1] (((x^y)^ (x^ (x v y)))^ ((x^y)^x)) v (((x^y)^ (x^ (x v y)))^ (x^y))= (x^y)^ (x^ (x v y)). 29,28 [para_into,20.1.1.1.1,20.1.1,demod,21,21,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (y^ (x v (((y^z) v (u^y)) v y)))=y. 30 [para_into,20.1.1.2.1,8.1.1,demod,9,9,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (((y^ (((y v z)^ (u v y))^y)) v (v^ (y v (((y v z)^ (u v y))^y))))^ (x v (((y^z) v (u^y)) v y)))=y. 36 [back_demod,20,demod,29] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 42 [para_into,30.1.1,36.1.1] (x^ (((x v y)^ (z v x))^x)) v (u^ (x v (((x v y)^ (z v x))^x)))=x. 50 [para_into,42.1.1,36.1.1,flip.1] (x^y) v (y^ (x v y))=y. 52 [para_from,42.1.1,18.1.1.2.2] ((x^ (((x v y)^ (z v x))^x))^ (u^ (x v (((x v y)^ (z v x))^x)))) v ((x^ (((x v y)^ (z v x))^x))^x)=x^ (((x v y)^ (z v x))^x). 65,64 [para_into,50.1.1,42.1.1,flip.1] ((x v y)^ (z v x))^x=x. 68 [back_demod,52,demod,65,65,65,65] ((x^x)^ (y^ (x v x))) v ((x^x)^x)=x^x. 70 [back_demod,42,demod,65,65] (x^x) v (y^ (x v x))=x. 110 [para_into,70.1.1,28.1.1,flip.1] ((x^y) v (z^x)) v x=x. 114 [para_from,70.1.1,22.1.1.1.2.2] (((x^x)^ (y^ (x v x)))^ ((x^x)^x)) v (((x^x)^ (y^ (x v x)))^ (x^x))= (x^x)^ (y^ (x v x)). 126 [para_into,110.1.1.1.2,64.1.1] ((x^y) v x) v x=x. 129,128 [para_from,110.1.1,64.1.1.1.2] ((x v y)^x)^x=x. 144 [para_from,126.1.1,18.1.1.2.2] (((x^y) v x)^x) v (((x^y) v x)^x)= (x^y) v x. 146 [para_from,126.1.1,50.1.1.2.2] (((x^y) v x)^x) v (x^x)=x. 148 [para_into,128.1.1.1.1,126.1.1] (x^ ((x^y) v x))^ ((x^y) v x)= (x^y) v x. 154 [para_into,128.1.1.1.1,50.1.1] (x^ (y^x))^ (y^x)=y^x. 160 [para_into,128.1.1.1.1,18.1.1] (x^ (x^y))^ (x^y)=x^y. 189,188 [para_into,154.1.1.1.2,128.1.1,demod,129,129] (x^x)^x=x. 196 [back_demod,114,demod,189] (((x^x)^ (y^ (x v x)))^x) v (((x^x)^ (y^ (x v x)))^ (x^x))= (x^x)^ (y^ (x v x)). 198 [back_demod,68,demod,189] ((x^x)^ (y^ (x v x))) v x=x^x. 202 [para_from,154.1.1,126.1.1.1.1] ((x^y) v (y^ (x^y))) v (y^ (x^y))=y^ (x^y). 218 [para_from,188.1.1,50.1.1.1] x v (x^ ((x^x) v x))=x. 227,226 [para_from,218.1.1,64.1.1.1.1] (x^ (y v x))^x=x. 228 [para_from,218.1.1,22.1.1.1.2.2] ((x^ (x^ ((x^x) v x)))^ (x^x)) v ((x^ (x^ ((x^x) v x)))^x)=x^ (x^ ((x^x) v x)). 238 [para_into,226.1.1.1.2,146.1.1,demod,189] x^ (x^x)=x^x. 245,244 [para_into,226.1.1.1.2,50.1.1,demod,227] x^ (x^ (y v x))=x^ (y v x). 256 [back_demod,228,demod,245,245,227,245] ((x^ ((x^x) v x))^ (x^x)) v x=x^ ((x^x) v x). 278 [para_from,226.1.1,18.1.1.1] x v ((x^ (y v x))^ ((x^ (y v x)) v x))=x^ (y v x). 281,280 [para_from,238.1.1,154.1.1.1] (x^x)^ (x^x)=x^x. 300 [para_from,280.1.1,146.1.1.1.1.1,demod,281] (((x^x) v (x^x))^ (x^x)) v (x^x)=x^x. 306 [para_from,280.1.1,26.1.1.2.2,demod,281,245,281,281,227,281,245,227,281,245,flip.1] (x^x)^ ((x^x) v (x^x))= (x^x) v (x^x). 311,310 [para_into,160.1.1.1.2,226.1.1,demod,227,227,227] x^x=x. 316,315 [back_demod,306,demod,311,311,311,311,311] x^ (x v x)=x v x. 322,321 [back_demod,300,demod,311,311,311,311,311] ((x v x)^x) v x=x. 332,331 [back_demod,256,demod,311,316,311,322,311,316,flip.1] x v x=x. 336 [back_demod,198,demod,311,332,311] (x^ (y^x)) v x=x. 338 [back_demod,196,demod,311,332,311,332,311,332,311,332] (x^ (y^x))^x=x^ (y^x). 355,354 [back_demod,70,demod,311,332] x v (y^x)=x. 361,360 [back_demod,144,demod,332] ((x^y) v x)^x= (x^y) v x. 371,370 [back_demod,202,demod,355,355,flip.1] x^ (y^x)=y^x. 377,376 [back_demod,338,demod,371,371] (x^y)^y=x^y. 378 [back_demod,336,demod,371] (x^y) v y=y. 384 [back_demod,148,demod,377] x^ ((x^y) v x)= (x^y) v x. 504,503 [para_from,384.1.1,226.1.1.1,demod,361] (x^y) v x=x. 505 [back_demod,278,demod,504,227,332,flip.1] x^ (y v x)=x. 531 [para_from,505.1.1,378.1.1.1] x v (y v x)=y v x. 549 [para_from,531.1.1,64.1.1.1.1] ((x v y)^ (z v y))^y=y. 551 [binary,549.1,3.1] $Ans(a3_meet). ------------ end of proof ------------- given clause #53: (wt=9) 535 [para_from,515.1.1,354.1.1.2] (x v y) v x=x v y. given clause #54: (wt=11) 519 [back_demod,104,demod,516,332] x^ ((x v y)^ (z v x))=x. given clause #55: (wt=11) 539 [para_from,517.1.1,404.1.1.1.2] ((x^y) v (y^z)) v y=y. given clause #56: (wt=11) 543 [para_from,517.1.1,110.1.1.1.2] ((x^y) v (x^z)) v x=x. given clause #57: (wt=11) 549 [para_from,531.1.1,64.1.1.1.1] ((x v y)^ (z v y))^y=y. given clause #58: (wt=11) 552 [para_into,535.1.1.1,404.1.1,demod,405] x v ((y^x) v (z^x))=x. given clause #59: (wt=11) 554 [para_into,535.1.1.1,110.1.1,demod,111] x v ((x^y) v (z^x))=x. given clause #60: (wt=11) 556 [para_from,535.1.1,64.1.1.1.2] ((x v y)^ (x v z))^x=x. given clause #61: (wt=11) 558 [para_into,519.1.1.2.1,531.1.1] x^ ((y v x)^ (z v x))=x. given clause #62: (wt=11) 570 [para_into,519.1.1.2.2,535.1.1] x^ ((x v y)^ (x v z))=x. given clause #63: (wt=11) 584 [para_from,539.1.1,535.1.1.1,demod,540] x v ((y^x) v (x^z))=x. given clause #64: (wt=11) 594 [para_from,543.1.1,535.1.1.1,demod,544] x v ((x^y) v (x^z))=x. given clause #65: (wt=11) 606 [para_into,549.1.1.1.2,535.1.1] ((x v y)^ (y v z))^y=y. given clause #66: (wt=11) 690 [para_into,558.1.1.2.2,535.1.1] x^ ((y v x)^ (x v z))=x. given clause #67: (wt=15) 76 [para_into,64.1.1.1.1,50.1.1] (x^ (y v (z^x)))^ (z^x)=z^x. given clause #68: (wt=11) 764 [para_into,76.1.1.1.2,541.1.1] (x^y)^ (y^x)=y^x. ----> UNIT CONFLICT at 26.79 sec ----> 801 [binary,800.1,2.1] $Ans(comm_meet). Length of proof is 63. Level of proof is 34. ---------------- PROOF ---------------- 2 [] A^B!=B^A|$Ans(comm_meet). 9,8 [] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((y^ (((y v u)^ (v v y))^y)) v (w^ (y v (((y v u)^ (v v y))^y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 10 [para_into,8.1.1.2.1.2.1,8.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^ (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z))))) v (z^ (x v (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z)))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). 12 [para_into,10.1.1.1.1.1.2,8.1.1,demod,9,9,9,9,9,9,9,9,9,9,9,9] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((w^ (((y^v6) v (v7^y)) v y)) v (((y^ (((y v v6)^ (v7 v y))^y)) v (v8^ (y v (((y v v6)^ (v7 v y))^y))))^ (w v (((y^v6) v (v7^y)) v y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 15,14 [para_into,12.1.1.2.1,8.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. 19,18 [para_into,14.1.1.1.1,14.1.1,demod,15] (x^y) v (x^ (x v y))=x. 21,20 [para_from,14.1.1,10.1.1.2.1.2.2.2.2,demod,15,15,15,15,15,15,15,15,15,15,15,15] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (y^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 22 [para_into,18.1.1.2.2,18.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 26 [para_into,22.1.1.1.2.2,18.1.1] (((x^y)^ (x^ (x v y)))^ ((x^y)^x)) v (((x^y)^ (x^ (x v y)))^ (x^y))= (x^y)^ (x^ (x v y)). 29,28 [para_into,20.1.1.1.1,20.1.1,demod,21,21,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (y^ (x v (((y^z) v (u^y)) v y)))=y. 30 [para_into,20.1.1.2.1,8.1.1,demod,9,9,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (((y^ (((y v z)^ (u v y))^y)) v (v^ (y v (((y v z)^ (u v y))^y))))^ (x v (((y^z) v (u^y)) v y)))=y. 36 [back_demod,20,demod,29] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 42 [para_into,30.1.1,36.1.1] (x^ (((x v y)^ (z v x))^x)) v (u^ (x v (((x v y)^ (z v x))^x)))=x. 50 [para_into,42.1.1,36.1.1,flip.1] (x^y) v (y^ (x v y))=y. 65,64 [para_into,50.1.1,42.1.1,flip.1] ((x v y)^ (z v x))^x=x. 70 [back_demod,42,demod,65,65] (x^x) v (y^ (x v x))=x. 76 [para_into,64.1.1.1.1,50.1.1] (x^ (y v (z^x)))^ (z^x)=z^x. 110 [para_into,70.1.1,28.1.1,flip.1] ((x^y) v (z^x)) v x=x. 114 [para_from,70.1.1,22.1.1.1.2.2] (((x^x)^ (y^ (x v x)))^ ((x^x)^x)) v (((x^x)^ (y^ (x v x)))^ (x^x))= (x^x)^ (y^ (x v x)). 126 [para_into,110.1.1.1.2,64.1.1] ((x^y) v x) v x=x. 129,128 [para_from,110.1.1,64.1.1.1.2] ((x v y)^x)^x=x. 144 [para_from,126.1.1,18.1.1.2.2] (((x^y) v x)^x) v (((x^y) v x)^x)= (x^y) v x. 146 [para_from,126.1.1,50.1.1.2.2] (((x^y) v x)^x) v (x^x)=x. 148 [para_into,128.1.1.1.1,126.1.1] (x^ ((x^y) v x))^ ((x^y) v x)= (x^y) v x. 154 [para_into,128.1.1.1.1,50.1.1] (x^ (y^x))^ (y^x)=y^x. 160 [para_into,128.1.1.1.1,18.1.1] (x^ (x^y))^ (x^y)=x^y. 162 [para_from,128.1.1,126.1.1.1.1] (x v ((x v y)^x)) v ((x v y)^x)= (x v y)^x. 189,188 [para_into,154.1.1.1.2,128.1.1,demod,129,129] (x^x)^x=x. 196 [back_demod,114,demod,189] (((x^x)^ (y^ (x v x)))^x) v (((x^x)^ (y^ (x v x)))^ (x^x))= (x^x)^ (y^ (x v x)). 202 [para_from,154.1.1,126.1.1.1.1] ((x^y) v (y^ (x^y))) v (y^ (x^y))=y^ (x^y). 218 [para_from,188.1.1,50.1.1.1] x v (x^ ((x^x) v x))=x. 227,226 [para_from,218.1.1,64.1.1.1.1] (x^ (y v x))^x=x. 228 [para_from,218.1.1,22.1.1.1.2.2] ((x^ (x^ ((x^x) v x)))^ (x^x)) v ((x^ (x^ ((x^x) v x)))^x)=x^ (x^ ((x^x) v x)). 238 [para_into,226.1.1.1.2,146.1.1,demod,189] x^ (x^x)=x^x. 245,244 [para_into,226.1.1.1.2,50.1.1,demod,227] x^ (x^ (y v x))=x^ (y v x). 256 [back_demod,228,demod,245,245,227,245] ((x^ ((x^x) v x))^ (x^x)) v x=x^ ((x^x) v x). 278 [para_from,226.1.1,18.1.1.1] x v ((x^ (y v x))^ ((x^ (y v x)) v x))=x^ (y v x). 281,280 [para_from,238.1.1,154.1.1.1] (x^x)^ (x^x)=x^x. 300 [para_from,280.1.1,146.1.1.1.1.1,demod,281] (((x^x) v (x^x))^ (x^x)) v (x^x)=x^x. 306 [para_from,280.1.1,26.1.1.2.2,demod,281,245,281,281,227,281,245,227,281,245,flip.1] (x^x)^ ((x^x) v (x^x))= (x^x) v (x^x). 311,310 [para_into,160.1.1.1.2,226.1.1,demod,227,227,227] x^x=x. 316,315 [back_demod,306,demod,311,311,311,311,311] x^ (x v x)=x v x. 322,321 [back_demod,300,demod,311,311,311,311,311] ((x v x)^x) v x=x. 332,331 [back_demod,256,demod,311,316,311,322,311,316,flip.1] x v x=x. 338 [back_demod,196,demod,311,332,311,332,311,332,311,332] (x^ (y^x))^x=x^ (y^x). 355,354 [back_demod,70,demod,311,332] x v (y^x)=x. 361,360 [back_demod,144,demod,332] ((x^y) v x)^x= (x^y) v x. 371,370 [back_demod,202,demod,355,355,flip.1] x^ (y^x)=y^x. 373,372 [back_demod,162,demod,355,355,flip.1] (x v y)^x=x. 377,376 [back_demod,338,demod,371,371] (x^y)^y=x^y. 381,380 [back_demod,160,demod,377] x^ (x^y)=x^y. 384 [back_demod,148,demod,377] x^ ((x^y) v x)= (x^y) v x. 400 [para_from,372.1.1,22.1.1.2.1,demod,373,373] (x^ ((x v y)^ ((x v y) v x))) v (x^ (x v y))=x. 402 [para_from,372.1.1,18.1.1.1] x v ((x v y)^ ((x v y) v x))=x v y. 411 [para_from,380.1.1,22.1.1.2.1,demod,381,381] ((x^y)^ (x^ (x v (x^y)))) v ((x^y)^x)=x^y. 501 [para_into,384.1.1.2.1,64.1.1,demod,65] ((x v y)^ (z v x))^ (x v ((x v y)^ (z v x)))=x v ((x v y)^ (z v x)). 504,503 [para_from,384.1.1,226.1.1.1,demod,361] (x^y) v x=x. 506,505 [back_demod,278,demod,504,227,332,flip.1] x^ (y v x)=x. 508,507 [back_demod,501,demod,506,flip.1] x v ((x v y)^ (z v x))= (x v y)^ (z v x). 514,513 [back_demod,402,demod,508] (x v y)^ ((x v y) v x)=x v y. 516,515 [back_demod,400,demod,514,332] x^ (x v y)=x. 517 [back_demod,411,demod,516,332] (x^y)^x=x^y. 541 [para_from,517.1.1,354.1.1.2] x v (x^y)=x. 765,764 [para_into,76.1.1.1.2,541.1.1] (x^y)^ (y^x)=y^x. 800 [para_from,764.1.1,517.1.1.1,demod,765,765] x^y=y^x. 801 [binary,800.1,2.1] $Ans(comm_meet). ------------ end of proof ------------- given clause #69: (wt=7) 800 [para_from,764.1.1,517.1.1.1,demod,765,765] x^y=y^x. given clause #70: (wt=11) 798 [para_from,764.1.1,541.1.1.2] (x^y) v (y^x)=x^y. given clause #71: (wt=15) 84 [para_into,64.1.1.1.1,18.1.1] (x^ (y v (x^z)))^ (x^z)=x^z. given clause #72: (wt=15) 364 [back_demod,112,demod,332,332,332] (((x^y) v z)^y)^ (x^y)=x^y. given clause #73: (wt=15) 394 [para_from,372.1.1,110.1.1.1.1] (x v (y^ (x v z))) v (x v z)=x v z. given clause #74: (wt=15) 521 [para_from,505.1.1,404.1.1.1.2] ((x^ (y v z)) v z) v (y v z)=y v z. given clause #75: (wt=15) 527 [para_from,505.1.1,110.1.1.1.2] (((x v y)^z) v y) v (x v y)=x v y. given clause #76: (wt=15) 529 [para_from,505.1.1,404.1.1.1.1] (x v (y^ (z v x))) v (z v x)=z v x. given clause #77: (wt=11) 974 [para_into,529.1.1.1.2,515.1.1] (x v y) v (y v x)=y v x. ----> UNIT CONFLICT at 28.24 sec ----> 1013 [binary,1012.1,5.1] $Ans(comm_join). Length of proof is 61. Level of proof is 32. ---------------- PROOF ---------------- 5 [] A v B!=B v A|$Ans(comm_join). 9,8 [] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((y^ (((y v u)^ (v v y))^y)) v (w^ (y v (((y v u)^ (v v y))^y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 10 [para_into,8.1.1.2.1.2.1,8.1.1] (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z))))))^u) v (((x^ (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z))))) v (z^ (x v (((((y^z) v (z^ (y v z)))^v) v (w^ ((y^z) v (z^ (y v z))))) v ((y^z) v (z^ (y v z)))))))^ (((x^ ((y^z) v (z^ (y v z)))) v (((y^z) v (z^ (y v z)))^ (x v ((y^z) v (z^ (y v z)))))) v u))= (y^z) v (z^ (y v z)). 12 [para_into,10.1.1.1.1.1.2,8.1.1,demod,9,9,9,9,9,9,9,9,9,9,9,9] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (((w^ (((y^v6) v (v7^y)) v y)) v (((y^ (((y v v6)^ (v7 v y))^y)) v (v8^ (y v (((y v v6)^ (v7 v y))^y))))^ (w v (((y^v6) v (v7^y)) v y))))^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 15,14 [para_into,12.1.1.2.1,8.1.1] (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y)))^z) v (y^ (((((x^y) v (y^ (x v y)))^y) v (y^ (((x^y) v (y^ (x v y))) v y))) v z))=y. 19,18 [para_into,14.1.1.1.1,14.1.1,demod,15] (x^y) v (x^ (x v y))=x. 21,20 [para_from,14.1.1,10.1.1.2.1.2.2.2.2,demod,15,15,15,15,15,15,15,15,15,15,15,15] (((x^y) v (y^ (x v y)))^z) v (((x^ (((y^u) v (v^y)) v y)) v (y^ (x v (((y^u) v (v^y)) v y))))^ (((x^y) v (y^ (x v y))) v z))=y. 22 [para_into,18.1.1.2.2,18.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 26 [para_into,22.1.1.1.2.2,18.1.1] (((x^y)^ (x^ (x v y)))^ ((x^y)^x)) v (((x^y)^ (x^ (x v y)))^ (x^y))= (x^y)^ (x^ (x v y)). 29,28 [para_into,20.1.1.1.1,20.1.1,demod,21,21,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (y^ (x v (((y^z) v (u^y)) v y)))=y. 30 [para_into,20.1.1.2.1,8.1.1,demod,9,9,19,flip.1] (x^ (((y^z) v (u^y)) v y)) v (((y^ (((y v z)^ (u v y))^y)) v (v^ (y v (((y v z)^ (u v y))^y))))^ (x v (((y^z) v (u^y)) v y)))=y. 36 [back_demod,20,demod,29] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 42 [para_into,30.1.1,36.1.1] (x^ (((x v y)^ (z v x))^x)) v (u^ (x v (((x v y)^ (z v x))^x)))=x. 50 [para_into,42.1.1,36.1.1,flip.1] (x^y) v (y^ (x v y))=y. 65,64 [para_into,50.1.1,42.1.1,flip.1] ((x v y)^ (z v x))^x=x. 70 [back_demod,42,demod,65,65] (x^x) v (y^ (x v x))=x. 110 [para_into,70.1.1,28.1.1,flip.1] ((x^y) v (z^x)) v x=x. 114 [para_from,70.1.1,22.1.1.1.2.2] (((x^x)^ (y^ (x v x)))^ ((x^x)^x)) v (((x^x)^ (y^ (x v x)))^ (x^x))= (x^x)^ (y^ (x v x)). 126 [para_into,110.1.1.1.2,64.1.1] ((x^y) v x) v x=x. 129,128 [para_from,110.1.1,64.1.1.1.2] ((x v y)^x)^x=x. 144 [para_from,126.1.1,18.1.1.2.2] (((x^y) v x)^x) v (((x^y) v x)^x)= (x^y) v x. 146 [para_from,126.1.1,50.1.1.2.2] (((x^y) v x)^x) v (x^x)=x. 148 [para_into,128.1.1.1.1,126.1.1] (x^ ((x^y) v x))^ ((x^y) v x)= (x^y) v x. 154 [para_into,128.1.1.1.1,50.1.1] (x^ (y^x))^ (y^x)=y^x. 160 [para_into,128.1.1.1.1,18.1.1] (x^ (x^y))^ (x^y)=x^y. 162 [para_from,128.1.1,126.1.1.1.1] (x v ((x v y)^x)) v ((x v y)^x)= (x v y)^x. 189,188 [para_into,154.1.1.1.2,128.1.1,demod,129,129] (x^x)^x=x. 196 [back_demod,114,demod,189] (((x^x)^ (y^ (x v x)))^x) v (((x^x)^ (y^ (x v x)))^ (x^x))= (x^x)^ (y^ (x v x)). 202 [para_from,154.1.1,126.1.1.1.1] ((x^y) v (y^ (x^y))) v (y^ (x^y))=y^ (x^y). 218 [para_from,188.1.1,50.1.1.1] x v (x^ ((x^x) v x))=x. 227,226 [para_from,218.1.1,64.1.1.1.1] (x^ (y v x))^x=x. 228 [para_from,218.1.1,22.1.1.1.2.2] ((x^ (x^ ((x^x) v x)))^ (x^x)) v ((x^ (x^ ((x^x) v x)))^x)=x^ (x^ ((x^x) v x)). 238 [para_into,226.1.1.1.2,146.1.1,demod,189] x^ (x^x)=x^x. 245,244 [para_into,226.1.1.1.2,50.1.1,demod,227] x^ (x^ (y v x))=x^ (y v x). 256 [back_demod,228,demod,245,245,227,245] ((x^ ((x^x) v x))^ (x^x)) v x=x^ ((x^x) v x). 278 [para_from,226.1.1,18.1.1.1] x v ((x^ (y v x))^ ((x^ (y v x)) v x))=x^ (y v x). 281,280 [para_from,238.1.1,154.1.1.1] (x^x)^ (x^x)=x^x. 300 [para_from,280.1.1,146.1.1.1.1.1,demod,281] (((x^x) v (x^x))^ (x^x)) v (x^x)=x^x. 306 [para_from,280.1.1,26.1.1.2.2,demod,281,245,281,281,227,281,245,227,281,245,flip.1] (x^x)^ ((x^x) v (x^x))= (x^x) v (x^x). 311,310 [para_into,160.1.1.1.2,226.1.1,demod,227,227,227] x^x=x. 316,315 [back_demod,306,demod,311,311,311,311,311] x^ (x v x)=x v x. 322,321 [back_demod,300,demod,311,311,311,311,311] ((x v x)^x) v x=x. 332,331 [back_demod,256,demod,311,316,311,322,311,316,flip.1] x v x=x. 338 [back_demod,196,demod,311,332,311,332,311,332,311,332] (x^ (y^x))^x=x^ (y^x). 355,354 [back_demod,70,demod,311,332] x v (y^x)=x. 361,360 [back_demod,144,demod,332] ((x^y) v x)^x= (x^y) v x. 371,370 [back_demod,202,demod,355,355,flip.1] x^ (y^x)=y^x. 373,372 [back_demod,162,demod,355,355,flip.1] (x v y)^x=x. 377,376 [back_demod,338,demod,371,371] (x^y)^y=x^y. 384 [back_demod,148,demod,377] x^ ((x^y) v x)= (x^y) v x. 400 [para_from,372.1.1,22.1.1.2.1,demod,373,373] (x^ ((x v y)^ ((x v y) v x))) v (x^ (x v y))=x. 402 [para_from,372.1.1,18.1.1.1] x v ((x v y)^ ((x v y) v x))=x v y. 404 [para_from,370.1.1,110.1.1.1.1] ((x^y) v (z^y)) v y=y. 501 [para_into,384.1.1.2.1,64.1.1,demod,65] ((x v y)^ (z v x))^ (x v ((x v y)^ (z v x)))=x v ((x v y)^ (z v x)). 504,503 [para_from,384.1.1,226.1.1.1,demod,361] (x^y) v x=x. 506,505 [back_demod,278,demod,504,227,332,flip.1] x^ (y v x)=x. 508,507 [back_demod,501,demod,506,flip.1] x v ((x v y)^ (z v x))= (x v y)^ (z v x). 514,513 [back_demod,402,demod,508] (x v y)^ ((x v y) v x)=x v y. 515 [back_demod,400,demod,514,332] x^ (x v y)=x. 529 [para_from,505.1.1,404.1.1.1.1] (x v (y^ (z v x))) v (z v x)=z v x. 535 [para_from,515.1.1,354.1.1.2] (x v y) v x=x v y. 975,974 [para_into,529.1.1.1.2,515.1.1] (x v y) v (y v x)=y v x. 1012 [para_from,974.1.1,535.1.1.1,demod,975,975] x v y=y v x. 1013 [binary,1012.1,5.1] $Ans(comm_join). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 77 clauses generated 3071 para_from generated 1491 para_into generated 1580 demod & eval rewrites 8923 clauses wt,lit,sk delete 491 tautologies deleted 0 clauses forward subsumed 2308 (subsumed by sos) 2 unit deletions 0 factor simplifications 0 clauses kept 502 new demodulators 499 empty clauses 6 clauses back demodulated 226 clauses back subsumed 0 usable size 46 sos size 230 demodulators size 273 passive size 6 hot size 0 Kbytes malloced 1085 ----------- times (seconds) ----------- user CPU time 28.33 (0 hr, 0 min, 28 sec) system CPU time 1.96 (0 hr, 0 min, 1 sec) wall-clock time 31 (0 hr, 0 min, 31 sec) input time 0.07 clausify time 0.00 process input 0.04 para_into time 3.01 para_from time 3.46 pre_process time 20.56 renumber time 2.68 demod time 10.28 order equalities 1.14 unit deleletion 0.00 factor simplify 0.00 weigh cl time 1.89 sort lits time 0.00 forward subsume 0.23 delete cl time 2.04 keep cl time 0.88 print_cl time 0.01 conflict time 0.51 new demod time 0.58 post_process time 0.87 back demod time 0.70 back subsume 0.14 factor time 0.00 unindex time 0.27 The job finished Mon Mar 6 14:52:14 1995