----- Otter 3.0.3d, Feb 1995 ----- The job was started by mccune on altair.mcs.anl.gov, Mon Mar 6 15:05:34 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_weight,119). assign(change_limit_after,2). assign(new_max_weight,90). assign(max_mem,12000). assign(max_proofs,7). weight_list(pick_given). weight($(1)=$(2),1). end_of_list. list(usable). 0 [] x=x. 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). 7 [] g(A)!=A|$Ans("g(x)=x"). end_of_list. list(sos). 0 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v x1)^ (x2 v y))^y)^u) v ((((y^x1) v (x2^y)) v y)^ ((((y v x1)^ (x2 v y))^y) v u)))) v (v^ (y v (((((y v x1)^ (x2 v y))^y)^u) v ((((y^x1) v (x2^y)) v y)^ ((((y v x1)^ (x2 v y))^y) v u))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. end_of_list. ------------> process usable: ** KEPT (wt=4): 8 [] x=x. Following clause subsumed by 8 during input processing: 0 [copy,8,flip.1] x=x. ------------> process sos: ** KEPT (wt=110): 9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. ---> New Demodulator: 10 [new_demod,9] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. >>>> Starting back demodulation with 10. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=110) 9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. given clause #2: (wt=118) 11 [para_into,9.1.1.2.1.2.1,9.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^g((y^z) v (z^ (y v z)))) v (z^ (x v g((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 90. given clause #3: (wt=120) 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. given clause #4: (wt=60) 15 [para_into,13.1.1.2.1,9.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=12) 19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. given clause #6: (wt=22) 23 [para_into,19.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. given clause #7: (wt=38) 21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. given clause #8: (wt=14) 37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. given clause #9: (wt=27) 55 [para_from,37.1.1,19.1.1.2.2] ((x^g(y))^ (y^ (x v g(y)))) v ((x^g(y))^y)=x^g(y). given clause #10: (wt=28) 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. given clause #11: (wt=46) 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). given clause #12: (wt=12) 71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. given clause #13: (wt=22) 85 [para_from,71.1.1,19.1.1.2.2] ((x^y)^ (y^ (x v y))) v ((x^y)^y)=x^y. given clause #14: (wt=28) 73 [para_into,71.1.1.2.2,71.1.1] ((x^y)^ (y^ (x v y))) v ((y^ (x v y))^y)=y^ (x v y). given clause #15: (wt=28) 81 [para_into,71.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^ (x v y))^x)=x^ (x v y). given clause #16: (wt=33) 77 [para_into,71.1.1.2.2,37.1.1] ((x^g(y))^ (y^ (x v g(y)))) v ((y^ (x v g(y)))^y)=y^ (x v g(y)). given clause #17: (wt=36) 79 [para_into,71.1.1.2.2,23.1.1] (((x^y)^ (x^ (x v y)))^ ((x^y)^x)) v (((x^y)^x)^ (x^y))= (x^y)^x. given clause #18: (wt=36) 101 [para_from,85.1.1,71.1.1.2.2] (((x^y)^ (y^ (x v y)))^ ((x^y)^y)) v (((x^y)^y)^ (x^y))= (x^y)^y. given clause #19: (wt=43) 75 [para_into,71.1.1.2.2,55.1.1] (((x^g(y))^ (y^ (x v g(y))))^ ((x^g(y))^y)) v (((x^g(y))^y)^ (x^g(y)))= (x^g(y))^y. given clause #20: (wt=46) 107 [para_into,73.1.1.1.2.2,71.1.1,demod,72,72] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((y^ (x v y))^y)^ (y^ (x v y)))= (y^ (x v y))^y. given clause #21: (wt=46) 115 [para_into,73.1.1.1.2.2,19.1.1,demod,20,20] (((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x)) v (((x^ (x v y))^x)^ (x^ (x v y)))= (x^ (x v y))^x. given clause #22: (wt=48) 33 [para_into,23.1.1.1.2.2,19.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 #23: (wt=48) 83 [para_from,71.1.1,23.1.1.1.2.2] (((x^y)^ (y^ (x v y)))^ ((x^y)^y)) v (((x^y)^ (y^ (x v y)))^ (x^y))= (x^y)^ (y^ (x v y)). given clause #24: (wt=52) 89 [para_into,85.1.1.1.2.2,71.1.1] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((x^y)^ (y^ (x v y)))^ (y^ (x v y)))= (x^y)^ (y^ (x v y)). given clause #25: (wt=52) 97 [para_into,85.1.1.1.2.2,19.1.1] (((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x)) v (((x^y)^ (x^ (x v y)))^ (x^ (x v y)))= (x^y)^ (x^ (x v y)). given clause #26: (wt=53) 111 [para_into,73.1.1.1.2.2,37.1.1,demod,38,38] (((x^g(y))^ (y^ (x v g(y))))^ ((y^ (x v g(y)))^y)) v (((y^ (x v g(y)))^y)^ (y^ (x v g(y))))= (y^ (x v g(y)))^y. given clause #27: (wt=58) 53 [para_from,37.1.1,23.1.1.1.2.2] (((x^g(y))^ (y^ (x v g(y))))^ ((x^g(y))^y)) v (((x^g(y))^ (y^ (x v g(y))))^ (x^g(y)))= (x^g(y))^ (y^ (x v g(y))). given clause #28: (wt=60) 103 [para_into,73.1.1.1.2.2,85.1.1,demod,86,86] ((((x^y)^ (y^ (x v y)))^ ((x^y)^y))^ (((x^y)^y)^ (x^y))) v ((((x^y)^y)^ (x^y))^ ((x^y)^y))= ((x^y)^y)^ (x^y). given clause #29: (wt=60) 113 [para_into,73.1.1.1.2.2,23.1.1,demod,24,24] ((((x^y)^ (x^ (x v y)))^ ((x^y)^x))^ (((x^y)^x)^ (x^y))) v ((((x^y)^x)^ (x^y))^ ((x^y)^x))= ((x^y)^x)^ (x^y). given clause #30: (wt=62) 93 [para_into,85.1.1.1.2.2,37.1.1] (((x^g(y))^ (y^ (x v g(y))))^ ((y^ (x v g(y)))^y)) v (((x^g(y))^ (y^ (x v g(y))))^ (y^ (x v g(y))))= (x^g(y))^ (y^ (x v g(y))). given clause #31: (wt=72) 109 [para_into,73.1.1.1.2.2,55.1.1,demod,56,56] ((((x^g(y))^ (y^ (x v g(y))))^ ((x^g(y))^y))^ (((x^g(y))^y)^ (x^g(y)))) v ((((x^g(y))^y)^ (x^g(y)))^ ((x^g(y))^y))= ((x^g(y))^y)^ (x^g(y)). given clause #32: (wt=78) 87 [para_into,85.1.1.1.2.2,85.1.1] ((((x^y)^ (y^ (x v y)))^ ((x^y)^y))^ (((x^y)^y)^ (x^y))) v ((((x^y)^ (y^ (x v y)))^ ((x^y)^y))^ ((x^y)^y))= ((x^y)^ (y^ (x v y)))^ ((x^y)^y). given clause #33: (wt=78) 95 [para_into,85.1.1.1.2.2,23.1.1] ((((x^y)^ (x^ (x v y)))^ ((x^y)^x))^ (((x^y)^x)^ (x^y))) v ((((x^y)^ (x^ (x v y)))^ ((x^y)^x))^ ((x^y)^x))= ((x^y)^ (x^ (x v y)))^ ((x^y)^x). given clause #34: (wt=80) 105 [para_into,73.1.1.1.2.2,73.1.1,demod,74,74] ((((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y))^ (((y^ (x v y))^y)^ (y^ (x v y)))) v ((((y^ (x v y))^y)^ (y^ (x v y)))^ ((y^ (x v y))^y))= ((y^ (x v y))^y)^ (y^ (x v y)). given clause #35: (wt=80) 121 [para_into,81.1.1.1.2.2,85.1.1,demod,86,86] ((((x^y)^ (y^ (x v y)))^ ((x^y)^y))^ (((x^y)^ (y^ (x v y)))^ (x^y))) v ((((x^y)^ (y^ (x v y)))^ (x^y))^ ((x^y)^ (y^ (x v y))))= ((x^y)^ (y^ (x v y)))^ (x^y). given clause #36: (wt=80) 129 [para_into,81.1.1.1.2.2,23.1.1,demod,24,24] ((((x^y)^ (x^ (x v y)))^ ((x^y)^x))^ (((x^y)^ (x^ (x v y)))^ (x^y))) v ((((x^y)^ (x^ (x v y)))^ (x^y))^ ((x^y)^ (x^ (x v y))))= ((x^y)^ (x^ (x v y)))^ (x^y). given clause #37: (wt=80) 133 [para_from,81.1.1,73.1.1.2.1.2,demod,82,82] ((((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x))^ (((x^ (x v y))^x)^ (x^ (x v y)))) v ((((x^ (x v y))^x)^ (x^ (x v y)))^ ((x^ (x v y))^x))= ((x^ (x v y))^x)^ (x^ (x v y)). given clause #38: (wt=86) 31 [para_into,23.1.1.1.2.2,23.1.1] ((((x^y)^ (x^ (x v y)))^ ((x^y)^x))^ (((x^y)^ (x^ (x v y)))^ (x^y))) v ((((x^y)^ (x^ (x v y)))^ ((x^y)^x))^ ((x^y)^ (x^ (x v y))))= ((x^y)^ (x^ (x v y)))^ ((x^y)^x). given clause #39: (wt=86) 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. given clause #40: (wt=38) 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. given clause #41: (wt=22) 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. given clause #42: (wt=12) 159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. given clause #43: (wt=12) 161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. ----> UNIT CONFLICT at 51.15 sec ----> 209 [binary,207.1,7.1] $Ans("g(x)=x"). Length of proof is 17. Level of proof is 12. ---------------- PROOF ---------------- 7 [] g(A)!=A|$Ans("g(x)=x"). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.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^g((y^z) v (z^ (y v z)))) v (z^ (x v g((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)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.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. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 209 [binary,207.1,7.1] $Ans("g(x)=x"). ------------ end of proof ------------- given clause #44: (wt=5) 207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. given clause #45: (wt=16) 205 [para_from,159.1.1,71.1.1.2.2] (((x^y) v (z^x))^x) v (x^x)=x. given clause #46: (wt=22) 228 [para_from,161.1.1,19.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((x^x)^x)=x^x. given clause #47: (wt=26) 197 [para_from,159.1.1,73.1.1.2.1.2,demod,160,160] ((((x^y) v (z^x))^x)^ (x^x)) v ((x^x)^x)=x^x. given clause #48: (wt=28) 242 [para_from,161.1.1,71.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((y^ (x v x))^x)=y^ (x v x). given clause #49: (wt=34) 189 [para_from,159.1.1,19.1.1.2.2] (((x^y) v (z^x))^x) v (((x^y) v (z^x))^x)= (x^y) v (z^x). given clause #50: (wt=36) 212 [back_demod,165,demod,208,208] (x^y) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v y))=y. given clause #51: (wt=20) 292 [para_into,212.1.1.2.1,161.1.1] (x^y) v ((((y v z)^ (u v y))^y)^ (x v y))=y. given clause #52: (wt=12) 396 [para_into,292.1.1,19.1.1] ((x v y)^ (z v x))^x=x. given clause #53: (wt=10) 460 [para_into,396.1.1.1.2,159.1.1] ((x v y)^x)^x=x. given clause #54: (wt=10) 510 [para_from,396.1.1,161.1.1.2] (x^x) v (x v x)=x. given clause #55: (wt=10) 518 [para_from,396.1.1,159.1.1.1.2] ((x^y) v x) v x=x. given clause #56: (wt=14) 512 [para_from,396.1.1,205.1.1.1.1.2] (((x^y) v x)^x) v (x^x)=x. given clause #57: (wt=14) 646 [para_from,460.1.1,71.1.1.1] x v (x^ (((x v y)^x) v x))=x. given clause #58: (wt=8) 778 [para_from,646.1.1,460.1.1.1.1] (x^x)^x=x. given clause #59: (wt=10) 780 [para_from,646.1.1,396.1.1.1.1] (x^ (y v x))^x=x. ----> UNIT CONFLICT at 63.22 sec ----> 1098 [binary,1096.1,1.1] $Ans(idem_meet). Length of proof is 32. Level of proof is 21. ---------------- PROOF ---------------- 1 [] A^A!=A|$Ans(idem_meet). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.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^g((y^z) v (z^ (y v z)))) v (z^ (x v g((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)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.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. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 85 [para_from,71.1.1,19.1.1.2.2] ((x^y)^ (y^ (x v y))) v ((x^y)^y)=x^y. 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 151 [para_into,43.1.1.2.1,71.1.1] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 165 [back_demod,151,demod,160] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 208,207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 212 [back_demod,165,demod,208,208] (x^y) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v y))=y. 292 [para_into,212.1.1.2.1,161.1.1] (x^y) v ((((y v z)^ (u v y))^y)^ (x v y))=y. 396 [para_into,292.1.1,19.1.1] ((x v y)^ (z v x))^x=x. 460 [para_into,396.1.1.1.2,159.1.1] ((x v y)^x)^x=x. 605,604 [para_into,460.1.1.1.1,19.1.1] (x^ (x^y))^ (x^y)=x^y. 647,646 [para_from,460.1.1,71.1.1.1] x v (x^ (((x v y)^x) v x))=x. 781,780 [para_from,646.1.1,396.1.1.1.1] (x^ (y v x))^x=x. 800 [para_from,646.1.1,85.1.1.1.2.2,demod,781,605] ((x^ (x^ (((x v y)^x) v x)))^x) v (x^ (((x v y)^x) v x))=x^ (x^ (((x v y)^x) v x)). 966 [para_into,780.1.1.1.2,646.1.1,demod,781] x^ (x^ (((x v y)^x) v x))=x^ (((x v y)^x) v x). 1007,1006 [para_into,780.1.1.1.2,71.1.1,demod,781] x^ (x^ (y v x))=x^ (y v x). 1021,1020 [back_demod,800,demod,1007,781,647,1007,flip.1] x^ (((x v y)^x) v x)=x. 1096 [back_demod,966,demod,1021,1021] x^x=x. 1098 [binary,1096.1,1.1] $Ans(idem_meet). ------------ end of proof ------------- ----> UNIT CONFLICT at 64.02 sec ----> 1167 [binary,1165.1,4.1] $Ans(idem_join). Length of proof is 49. Level of proof is 24. ---------------- PROOF ---------------- 4 [] A v A!=A|$Ans(idem_join). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.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^g((y^z) v (z^ (y v z)))) v (z^ (x v g((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)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.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. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 23 [para_into,19.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 33 [para_into,23.1.1.1.2.2,19.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)). 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 73 [para_into,71.1.1.2.2,71.1.1] ((x^y)^ (y^ (x v y))) v ((y^ (x v y))^y)=y^ (x v y). 82,81 [para_into,71.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^ (x v y))^x)=x^ (x v y). 85 [para_from,71.1.1,19.1.1.2.2] ((x^y)^ (y^ (x v y))) v ((x^y)^y)=x^y. 115 [para_into,73.1.1.1.2.2,19.1.1,demod,20,20] (((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x)) v (((x^ (x v y))^x)^ (x^ (x v y)))= (x^ (x v y))^x. 133 [para_from,81.1.1,73.1.1.2.1.2,demod,82,82] ((((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x))^ (((x^ (x v y))^x)^ (x^ (x v y)))) v ((((x^ (x v y))^x)^ (x^ (x v y)))^ ((x^ (x v y))^x))= ((x^ (x v y))^x)^ (x^ (x v y)). 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 151 [para_into,43.1.1.2.1,71.1.1] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 165 [back_demod,151,demod,160] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 205 [para_from,159.1.1,71.1.1.2.2] (((x^y) v (z^x))^x) v (x^x)=x. 208,207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 212 [back_demod,165,demod,208,208] (x^y) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v y))=y. 292 [para_into,212.1.1.2.1,161.1.1] (x^y) v ((((y v z)^ (u v y))^y)^ (x v y))=y. 396 [para_into,292.1.1,19.1.1] ((x v y)^ (z v x))^x=x. 460 [para_into,396.1.1.1.2,159.1.1] ((x v y)^x)^x=x. 512 [para_from,396.1.1,205.1.1.1.1.2] (((x^y) v x)^x) v (x^x)=x. 605,604 [para_into,460.1.1.1.1,19.1.1] (x^ (x^y))^ (x^y)=x^y. 647,646 [para_from,460.1.1,71.1.1.1] x v (x^ (((x v y)^x) v x))=x. 779,778 [para_from,646.1.1,460.1.1.1.1] (x^x)^x=x. 781,780 [para_from,646.1.1,396.1.1.1.1] (x^ (y v x))^x=x. 782 [para_from,646.1.1,133.1.1.2.1.2.2,demod,647,647,779,647,779,647,647,779,647,779,647,779,647] ((((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x)^ (x^ (x^x))) v ((x^ (x^x))^x)=x^ (x^x). 784 [para_from,646.1.1,115.1.1.2.2.2,demod,647,647,779,647,779,647,779] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x) v (x^ (x^x))=x. 790 [para_from,646.1.1,33.1.1.2.1.2.2,demod,647,647] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ ((x^ (x^ (((x v y)^x) v x)))^x)) v (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ (x^ (x^ (((x v y)^x) v x))))= (x^ (x^ (((x v y)^x) v x)))^ (x^x). 800 [para_from,646.1.1,85.1.1.1.2.2,demod,781,605] ((x^ (x^ (((x v y)^x) v x)))^x) v (x^ (((x v y)^x) v x))=x^ (x^ (((x v y)^x) v x)). 966 [para_into,780.1.1.1.2,646.1.1,demod,781] x^ (x^ (((x v y)^x) v x))=x^ (((x v y)^x) v x). 969,968 [para_into,780.1.1.1.2,512.1.1,demod,779] x^ (x^x)=x^x. 1007,1006 [para_into,780.1.1.1.2,71.1.1,demod,781] x^ (x^ (y v x))=x^ (y v x). 1021,1020 [back_demod,800,demod,1007,781,647,1007,flip.1] x^ (((x v y)^x) v x)=x. 1029,1028 [back_demod,790,demod,1021,1021,779,1021,1021,779,1021] (((x^x)^ (x^x))^x) v (x^x)= (x^x)^ (x^x). 1033,1032 [back_demod,784,demod,1021,969,1029] (x^x)^ (x^x)=x. 1034 [back_demod,782,demod,1021,1033,969,1033,969,779,969] x v x=x^x. 1097,1096 [back_demod,966,demod,1021,1021] x^x=x. 1165 [back_demod,1034,demod,1097] x v x=x. 1167 [binary,1165.1,4.1] $Ans(idem_join). ------------ end of proof ------------- given clause #60: (wt=6) 1096 [back_demod,966,demod,1021,1021] x^x=x. given clause #61: (wt=6) 1165 [back_demod,1034,demod,1097] x v x=x. given clause #62: (wt=8) 1127 [back_demod,904,demod,1035,1097,1097] (x v y)^x=x. given clause #63: (wt=8) 1135 [back_demod,624,demod,1128,1128,1128,1128,1128,1128,1035,1097,1128,flip.1] x v (y^x)=x. given clause #64: (wt=8) 1222 [back_demod,1133,demod,1191] (x^y) v y=y. given clause #65: (wt=10) 1188 [back_demod,906,demod,1128] x^ ((x v y) v x)=x. given clause #66: (wt=12) 1190 [back_demod,1153,demod,1162,1097,1162,1179,1162,1179,1166] x^ (y^x)=y^x. ----> UNIT CONFLICT at 65.88 sec ----> 1288 [binary,1286.1,6.1] $Ans(a3_join). Length of proof is 72. Level of proof is 29. ---------------- PROOF ---------------- 6 [] ((A^C) v (B^C)) v C!=C|$Ans(a3_join). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.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^g((y^z) v (z^ (y v z)))) v (z^ (x v g((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)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.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. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 23 [para_into,19.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 33 [para_into,23.1.1.1.2.2,19.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)). 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 73 [para_into,71.1.1.2.2,71.1.1] ((x^y)^ (y^ (x v y))) v ((y^ (x v y))^y)=y^ (x v y). 82,81 [para_into,71.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^ (x v y))^x)=x^ (x v y). 85 [para_from,71.1.1,19.1.1.2.2] ((x^y)^ (y^ (x v y))) v ((x^y)^y)=x^y. 101 [para_from,85.1.1,71.1.1.2.2] (((x^y)^ (y^ (x v y)))^ ((x^y)^y)) v (((x^y)^y)^ (x^y))= (x^y)^y. 107 [para_into,73.1.1.1.2.2,71.1.1,demod,72,72] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((y^ (x v y))^y)^ (y^ (x v y)))= (y^ (x v y))^y. 115 [para_into,73.1.1.1.2.2,19.1.1,demod,20,20] (((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x)) v (((x^ (x v y))^x)^ (x^ (x v y)))= (x^ (x v y))^x. 133 [para_from,81.1.1,73.1.1.2.1.2,demod,82,82] ((((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x))^ (((x^ (x v y))^x)^ (x^ (x v y)))) v ((((x^ (x v y))^x)^ (x^ (x v y)))^ ((x^ (x v y))^x))= ((x^ (x v y))^x)^ (x^ (x v y)). 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 151 [para_into,43.1.1.2.1,71.1.1] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 162,161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 165 [back_demod,151,demod,160] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 205 [para_from,159.1.1,71.1.1.2.2] (((x^y) v (z^x))^x) v (x^x)=x. 208,207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 212 [back_demod,165,demod,208,208] (x^y) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v y))=y. 230 [para_from,161.1.1,107.1.1.2.2.2,demod,162,162,162,162] ((((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))^ (((y^ (x v x))^x)^ (y^ (x v x)))) v ((((y^ (x v x))^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))= ((y^ (x v x))^x)^ (y^ (x v x)). 234 [para_from,161.1.1,73.1.1.2.1.2,demod,162,162] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((y^ (x v x))^x)^ (y^ (x v x)))= (y^ (x v x))^x. 236 [para_from,161.1.1,85.1.1.1.2.2] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((x^x)^ (y^ (x v x)))^ (y^ (x v x)))= (x^x)^ (y^ (x v x)). 242 [para_from,161.1.1,71.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((y^ (x v x))^x)=y^ (x v x). 292 [para_into,212.1.1.2.1,161.1.1] (x^y) v ((((y v z)^ (u v y))^y)^ (x v y))=y. 396 [para_into,292.1.1,19.1.1] ((x v y)^ (z v x))^x=x. 460 [para_into,396.1.1.1.2,159.1.1] ((x v y)^x)^x=x. 512 [para_from,396.1.1,205.1.1.1.1.2] (((x^y) v x)^x) v (x^x)=x. 599,598 [para_into,460.1.1.1.1,71.1.1] (x^ (y^x))^ (y^x)=y^x. 605,604 [para_into,460.1.1.1.1,19.1.1] (x^ (x^y))^ (x^y)=x^y. 647,646 [para_from,460.1.1,71.1.1.1] x v (x^ (((x v y)^x) v x))=x. 779,778 [para_from,646.1.1,460.1.1.1.1] (x^x)^x=x. 781,780 [para_from,646.1.1,396.1.1.1.1] (x^ (y v x))^x=x. 782 [para_from,646.1.1,133.1.1.2.1.2.2,demod,647,647,779,647,779,647,647,779,647,779,647,779,647] ((((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x)^ (x^ (x^x))) v ((x^ (x^x))^x)=x^ (x^x). 784 [para_from,646.1.1,115.1.1.2.2.2,demod,647,647,779,647,779,647,779] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x) v (x^ (x^x))=x. 790 [para_from,646.1.1,33.1.1.2.1.2.2,demod,647,647] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ ((x^ (x^ (((x v y)^x) v x)))^x)) v (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ (x^ (x^ (((x v y)^x) v x))))= (x^ (x^ (((x v y)^x) v x)))^ (x^x). 800 [para_from,646.1.1,85.1.1.1.2.2,demod,781,605] ((x^ (x^ (((x v y)^x) v x)))^x) v (x^ (((x v y)^x) v x))=x^ (x^ (((x v y)^x) v x)). 966 [para_into,780.1.1.1.2,646.1.1,demod,781] x^ (x^ (((x v y)^x) v x))=x^ (((x v y)^x) v x). 969,968 [para_into,780.1.1.1.2,512.1.1,demod,779] x^ (x^x)=x^x. 972 [para_into,780.1.1.1.2,242.1.1] (((x^ (y v y))^y)^ (x^ (y v y)))^ ((x^ (y v y))^y)= (x^ (y v y))^y. 976 [para_into,780.1.1.1.2,161.1.1] ((x^ (y v y))^y)^ (x^ (y v y))=x^ (y v y). 990 [para_into,780.1.1.1.2,101.1.1] ((((x^y)^y)^ (x^y))^ ((x^y)^y))^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 999,998 [para_into,780.1.1.1.2,85.1.1] (((x^y)^y)^ (x^y))^ ((x^y)^y)= (x^y)^y. 1007,1006 [para_into,780.1.1.1.2,71.1.1,demod,781] x^ (x^ (y v x))=x^ (y v x). 1021,1020 [back_demod,800,demod,1007,781,647,1007,flip.1] x^ (((x v y)^x) v x)=x. 1029,1028 [back_demod,790,demod,1021,1021,779,1021,1021,779,1021] (((x^x)^ (x^x))^x) v (x^x)= (x^x)^ (x^x). 1033,1032 [back_demod,784,demod,1021,969,1029] (x^x)^ (x^x)=x. 1035,1034 [back_demod,782,demod,1021,1033,969,1033,969,779,969] x v x=x^x. 1064 [back_demod,230,demod,1035,1035,1035,1035,1035,1035,1035,1035,1035] ((((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))^ (((y^ (x^x))^x)^ (y^ (x^x)))) v ((((y^ (x^x))^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))= ((y^ (x^x))^x)^ (y^ (x^x)). 1066 [back_demod,972,demod,1035,1035,1035,1035] (((x^ (y^y))^y)^ (x^ (y^y)))^ ((x^ (y^y))^y)= (x^ (y^y))^y. 1068 [back_demod,234,demod,1035,1035,1035,1035,1035] (((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x)) v (((y^ (x^x))^x)^ (y^ (x^x)))= (y^ (x^x))^x. 1078 [back_demod,990,demod,999] ((x^y)^y)^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 1097,1096 [back_demod,966,demod,1021,1021] x^x=x. 1124,1123 [back_demod,976,demod,1035,1097,1035,1097,1035,1097] ((x^y)^y)^ (x^y)=x^y. 1150,1149 [back_demod,236,demod,1097,1035,1097,1035,1097,1097,1035,1097,1035,1097,599,1097,1035,1097] ((x^ (y^x))^ ((y^x)^x)) v (y^x)=x^ (y^x). 1153 [back_demod,1064,demod,1097,1097,1097,1097,1097,1124,1097,1097,1124,1097,1097,1097,1124] (((x^ (y^x))^ ((y^x)^x))^ (y^x)) v ((y^x)^ ((y^x)^x))=y^x. 1162,1161 [back_demod,1068,demod,1097,1097,1097,1097,1097,1124,1150,1097,flip.1] (x^y)^y=y^ (x^y). 1164,1163 [back_demod,1066,demod,1097,1162,1097,1162,1097,1162,1162,1097,1162] (x^ (y^x))^ ((y^x)^ (x^ (y^x)))=x^ (y^x). 1166,1165 [back_demod,1034,demod,1097] x v x=x. 1179,1178 [back_demod,1078,demod,1162,1162,1162,1164,1162,1162,flip.1] (x^y)^ (y^ (x^y))=y^ (x^y). 1190 [back_demod,1153,demod,1162,1097,1162,1179,1162,1179,1166] x^ (y^x)=y^x. 1286 [para_from,1190.1.1,159.1.1.1.1] ((x^y) v (z^y)) v y=y. 1288 [binary,1286.1,6.1] $Ans(a3_join). ------------ end of proof ------------- given clause #67: (wt=10) 1284 [para_into,1190.1.1.2,1188.1.1,demod,1189] ((x v y) v x)^x=x. given clause #68: (wt=12) 1204 [back_demod,604,demod,1162,1191] x^ (x^y)=x^y. given clause #69: (wt=12) 1220 [back_demod,1161,demod,1191] (x^y)^y=x^y. given clause #70: (wt=12) 1238 [para_from,780.1.1,71.1.1.1,demod,1203] x v ((x^ (y v x)) v x)=x. given clause #71: (wt=12) 1286 [para_from,1190.1.1,159.1.1.1.1] ((x^y) v (z^y)) v y=y. given clause #72: (wt=14) 1107 [back_demod,884,demod,1007,781,547,1007,flip.1] x^ (((x v y)^ (z v x)) v x)=x. given clause #73: (wt=8) 1379 [back_demod,1248,demod,1352,781,1166,flip.1] x^ (y v x)=x. given clause #74: (wt=8) 1387 [back_demod,1202,demod,1380,flip.1] (x^y) v x=x. given clause #75: (wt=8) 1399 [para_from,1379.1.1,1190.1.1.2,demod,1380] (x v y)^y=y. given clause #76: (wt=8) 1413 [back_demod,1262,demod,1412,1166] x^ (x v y)=x. given clause #77: (wt=12) 1401 [para_from,1379.1.1,1135.1.1.2] (x v y) v y=x v y. given clause #78: (wt=12) 1405 [para_from,1379.1.1,1222.1.1.1] x v (y v x)=y v x. ----> UNIT CONFLICT at 67.73 sec ----> 1427 [binary,1425.1,3.1] $Ans(a3_meet). Length of proof is 90. Level of proof is 34. ---------------- PROOF ---------------- 3 [] ((A v C)^ (B v C))^C!=C|$Ans(a3_meet). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.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^g((y^z) v (z^ (y v z)))) v (z^ (x v g((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)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.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. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 23 [para_into,19.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 33 [para_into,23.1.1.1.2.2,19.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)). 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 73 [para_into,71.1.1.2.2,71.1.1] ((x^y)^ (y^ (x v y))) v ((y^ (x v y))^y)=y^ (x v y). 82,81 [para_into,71.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^ (x v y))^x)=x^ (x v y). 85 [para_from,71.1.1,19.1.1.2.2] ((x^y)^ (y^ (x v y))) v ((x^y)^y)=x^y. 89 [para_into,85.1.1.1.2.2,71.1.1] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((x^y)^ (y^ (x v y)))^ (y^ (x v y)))= (x^y)^ (y^ (x v y)). 101 [para_from,85.1.1,71.1.1.2.2] (((x^y)^ (y^ (x v y)))^ ((x^y)^y)) v (((x^y)^y)^ (x^y))= (x^y)^y. 107 [para_into,73.1.1.1.2.2,71.1.1,demod,72,72] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((y^ (x v y))^y)^ (y^ (x v y)))= (y^ (x v y))^y. 115 [para_into,73.1.1.1.2.2,19.1.1,demod,20,20] (((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x)) v (((x^ (x v y))^x)^ (x^ (x v y)))= (x^ (x v y))^x. 133 [para_from,81.1.1,73.1.1.2.1.2,demod,82,82] ((((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x))^ (((x^ (x v y))^x)^ (x^ (x v y)))) v ((((x^ (x v y))^x)^ (x^ (x v y)))^ ((x^ (x v y))^x))= ((x^ (x v y))^x)^ (x^ (x v y)). 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 151 [para_into,43.1.1.2.1,71.1.1] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 162,161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 165 [back_demod,151,demod,160] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 205 [para_from,159.1.1,71.1.1.2.2] (((x^y) v (z^x))^x) v (x^x)=x. 208,207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 212 [back_demod,165,demod,208,208] (x^y) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v y))=y. 228 [para_from,161.1.1,19.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((x^x)^x)=x^x. 230 [para_from,161.1.1,107.1.1.2.2.2,demod,162,162,162,162] ((((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))^ (((y^ (x v x))^x)^ (y^ (x v x)))) v ((((y^ (x v x))^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))= ((y^ (x v x))^x)^ (y^ (x v x)). 234 [para_from,161.1.1,73.1.1.2.1.2,demod,162,162] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((y^ (x v x))^x)^ (y^ (x v x)))= (y^ (x v x))^x. 236 [para_from,161.1.1,85.1.1.1.2.2] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((x^x)^ (y^ (x v x)))^ (y^ (x v x)))= (x^x)^ (y^ (x v x)). 242 [para_from,161.1.1,71.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((y^ (x v x))^x)=y^ (x v x). 292 [para_into,212.1.1.2.1,161.1.1] (x^y) v ((((y v z)^ (u v y))^y)^ (x v y))=y. 397,396 [para_into,292.1.1,19.1.1] ((x v y)^ (z v x))^x=x. 460 [para_into,396.1.1.1.2,159.1.1] ((x v y)^x)^x=x. 512 [para_from,396.1.1,205.1.1.1.1.2] (((x^y) v x)^x) v (x^x)=x. 518 [para_from,396.1.1,159.1.1.1.2] ((x^y) v x) v x=x. 540 [para_from,396.1.1,89.1.1.2.1.1,demod,397,397] ((x^ (x^ (((x v y)^ (z v x)) v x)))^ ((x^ (((x v y)^ (z v x)) v x))^x)) v ((x^ (x^ (((x v y)^ (z v x)) v x)))^ (x^ (((x v y)^ (z v x)) v x)))=x^ (x^ (((x v y)^ (z v x)) v x)). 547,546 [para_from,396.1.1,71.1.1.1] x v (x^ (((x v y)^ (z v x)) v x))=x. 599,598 [para_into,460.1.1.1.1,71.1.1] (x^ (y^x))^ (y^x)=y^x. 605,604 [para_into,460.1.1.1.1,19.1.1] (x^ (x^y))^ (x^y)=x^y. 606 [back_demod,540,demod,605] ((x^ (x^ (((x v y)^ (z v x)) v x)))^ ((x^ (((x v y)^ (z v x)) v x))^x)) v (x^ (((x v y)^ (z v x)) v x))=x^ (x^ (((x v y)^ (z v x)) v x)). 647,646 [para_from,460.1.1,71.1.1.1] x v (x^ (((x v y)^x) v x))=x. 702 [para_from,518.1.1,460.1.1.1.1] (x^ ((x^y) v x))^ ((x^y) v x)= (x^y) v x. 779,778 [para_from,646.1.1,460.1.1.1.1] (x^x)^x=x. 781,780 [para_from,646.1.1,396.1.1.1.1] (x^ (y v x))^x=x. 782 [para_from,646.1.1,133.1.1.2.1.2.2,demod,647,647,779,647,779,647,647,779,647,779,647,779,647] ((((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x)^ (x^ (x^x))) v ((x^ (x^x))^x)=x^ (x^x). 784 [para_from,646.1.1,115.1.1.2.2.2,demod,647,647,779,647,779,647,779] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x) v (x^ (x^x))=x. 790 [para_from,646.1.1,33.1.1.2.1.2.2,demod,647,647] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ ((x^ (x^ (((x v y)^x) v x)))^x)) v (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ (x^ (x^ (((x v y)^x) v x))))= (x^ (x^ (((x v y)^x) v x)))^ (x^x). 800 [para_from,646.1.1,85.1.1.1.2.2,demod,781,605] ((x^ (x^ (((x v y)^x) v x)))^x) v (x^ (((x v y)^x) v x))=x^ (x^ (((x v y)^x) v x)). 860 [back_demod,228,demod,779] ((x^x)^ (y^ (x v x))) v x=x^x. 884 [back_demod,606,demod,781] ((x^ (x^ (((x v y)^ (z v x)) v x)))^x) v (x^ (((x v y)^ (z v x)) v x))=x^ (x^ (((x v y)^ (z v x)) v x)). 966 [para_into,780.1.1.1.2,646.1.1,demod,781] x^ (x^ (((x v y)^x) v x))=x^ (((x v y)^x) v x). 969,968 [para_into,780.1.1.1.2,512.1.1,demod,779] x^ (x^x)=x^x. 972 [para_into,780.1.1.1.2,242.1.1] (((x^ (y v y))^y)^ (x^ (y v y)))^ ((x^ (y v y))^y)= (x^ (y v y))^y. 976 [para_into,780.1.1.1.2,161.1.1] ((x^ (y v y))^y)^ (x^ (y v y))=x^ (y v y). 990 [para_into,780.1.1.1.2,101.1.1] ((((x^y)^y)^ (x^y))^ ((x^y)^y))^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 999,998 [para_into,780.1.1.1.2,85.1.1] (((x^y)^y)^ (x^y))^ ((x^y)^y)= (x^y)^y. 1007,1006 [para_into,780.1.1.1.2,71.1.1,demod,781] x^ (x^ (y v x))=x^ (y v x). 1021,1020 [back_demod,800,demod,1007,781,647,1007,flip.1] x^ (((x v y)^x) v x)=x. 1029,1028 [back_demod,790,demod,1021,1021,779,1021,1021,779,1021] (((x^x)^ (x^x))^x) v (x^x)= (x^x)^ (x^x). 1033,1032 [back_demod,784,demod,1021,969,1029] (x^x)^ (x^x)=x. 1035,1034 [back_demod,782,demod,1021,1033,969,1033,969,779,969] x v x=x^x. 1064 [back_demod,230,demod,1035,1035,1035,1035,1035,1035,1035,1035,1035] ((((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))^ (((y^ (x^x))^x)^ (y^ (x^x)))) v ((((y^ (x^x))^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))= ((y^ (x^x))^x)^ (y^ (x^x)). 1066 [back_demod,972,demod,1035,1035,1035,1035] (((x^ (y^y))^y)^ (x^ (y^y)))^ ((x^ (y^y))^y)= (x^ (y^y))^y. 1068 [back_demod,234,demod,1035,1035,1035,1035,1035] (((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x)) v (((y^ (x^x))^x)^ (y^ (x^x)))= (y^ (x^x))^x. 1078 [back_demod,990,demod,999] ((x^y)^y)^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 1097,1096 [back_demod,966,demod,1021,1021] x^x=x. 1107 [back_demod,884,demod,1007,781,547,1007,flip.1] x^ (((x v y)^ (z v x)) v x)=x. 1124,1123 [back_demod,976,demod,1035,1097,1035,1097,1035,1097] ((x^y)^y)^ (x^y)=x^y. 1133 [back_demod,860,demod,1097,1035,1097,1097] (x^ (y^x)) v x=x. 1150,1149 [back_demod,236,demod,1097,1035,1097,1035,1097,1097,1035,1097,1035,1097,599,1097,1035,1097] ((x^ (y^x))^ ((y^x)^x)) v (y^x)=x^ (y^x). 1153 [back_demod,1064,demod,1097,1097,1097,1097,1097,1124,1097,1097,1124,1097,1097,1097,1124] (((x^ (y^x))^ ((y^x)^x))^ (y^x)) v ((y^x)^ ((y^x)^x))=y^x. 1162,1161 [back_demod,1068,demod,1097,1097,1097,1097,1097,1124,1150,1097,flip.1] (x^y)^y=y^ (x^y). 1164,1163 [back_demod,1066,demod,1097,1162,1097,1162,1097,1162,1162,1097,1162] (x^ (y^x))^ ((y^x)^ (x^ (y^x)))=x^ (y^x). 1166,1165 [back_demod,1034,demod,1097] x v x=x. 1179,1178 [back_demod,1078,demod,1162,1162,1162,1164,1162,1162,flip.1] (x^y)^ (y^ (x^y))=y^ (x^y). 1191,1190 [back_demod,1153,demod,1162,1097,1162,1179,1162,1179,1166] x^ (y^x)=y^x. 1203,1202 [back_demod,702,demod,1162,1191] x^ ((x^y) v x)= (x^y) v x. 1222 [back_demod,1133,demod,1191] (x^y) v y=y. 1238 [para_from,780.1.1,71.1.1.1,demod,1203] x v ((x^ (y v x)) v x)=x. 1248 [para_from,780.1.1,19.1.1.1] x v ((x^ (y v x))^ ((x^ (y v x)) v x))=x^ (y v x). 1352,1351 [para_into,1107.1.1.2.1.1,1238.1.1,demod,1203] (x^ (y v x)) v x=x. 1379 [back_demod,1248,demod,1352,781,1166,flip.1] x^ (y v x)=x. 1405 [para_from,1379.1.1,1222.1.1.1] x v (y v x)=y v x. 1425 [para_from,1405.1.1,396.1.1.1.1] ((x v y)^ (z v y))^y=y. 1427 [binary,1425.1,3.1] $Ans(a3_meet). ------------ end of proof ------------- given clause #79: (wt=12) 1407 [back_demod,1250,demod,1402] x v (x v y)=x v y. given clause #80: (wt=12) 1415 [back_demod,1309,demod,1414,1166] (x^y)^x=x^y. given clause #81: (wt=8) 1432 [para_from,1415.1.1,1135.1.1.2] x v (x^y)=x. given clause #82: (wt=12) 1417 [back_demod,554,demod,1414,1166] x^ ((x v y)^ (z v x))=x. given clause #83: (wt=12) 1423 [para_from,1413.1.1,1135.1.1.2] (x v y) v x=x v y. given clause #84: (wt=12) 1425 [para_from,1405.1.1,396.1.1.1.1] ((x v y)^ (z v y))^y=y. given clause #85: (wt=12) 1428 [para_from,1415.1.1,1286.1.1.1.2] ((x^y) v (y^z)) v y=y. given clause #86: (wt=12) 1430 [para_from,1415.1.1,159.1.1.1.2] ((x^y) v (x^z)) v x=x. given clause #87: (wt=12) 1438 [para_into,1417.1.1.2.1,1405.1.1] x^ ((y v x)^ (z v x))=x. given clause #88: (wt=12) 1456 [para_into,1423.1.1.1,1286.1.1,demod,1287] x v ((y^x) v (z^x))=x. given clause #89: (wt=12) 1458 [para_into,1423.1.1.1,159.1.1,demod,160] x v ((x^y) v (z^x))=x. given clause #90: (wt=12) 1460 [para_from,1423.1.1,1417.1.1.2.2] x^ ((x v y)^ (x v z))=x. given clause #91: (wt=12) 1462 [para_from,1423.1.1,396.1.1.1.2] ((x v y)^ (x v z))^x=x. given clause #92: (wt=12) 1466 [para_into,1425.1.1.1.2,1423.1.1] ((x v y)^ (y v z))^y=y. given clause #93: (wt=12) 1484 [para_from,1428.1.1,1423.1.1.1,demod,1429] x v ((y^x) v (x^z))=x. given clause #94: (wt=12) 1498 [para_from,1430.1.1,1423.1.1.1,demod,1431] x v ((x^y) v (x^z))=x. given clause #95: (wt=12) 1510 [para_into,1438.1.1.2.2,1423.1.1] x^ ((y v x)^ (x v z))=x. given clause #96: (wt=18) 442 [para_into,396.1.1.1.1,71.1.1] (x^ (y v (z^x)))^ (z^x)=z^x. given clause #97: (wt=14) 1650 [para_into,442.1.1.1.2,1432.1.1] (x^y)^ (y^x)=y^x. ----> UNIT CONFLICT at 69.54 sec ----> 1687 [binary,1686.1,2.1] $Ans(comm_meet). Length of proof is 106. Level of proof is 40. ---------------- PROOF ---------------- 2 [] A^B!=B^A|$Ans(comm_meet). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.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^g((y^z) v (z^ (y v z)))) v (z^ (x v g((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)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.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. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 23 [para_into,19.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 33 [para_into,23.1.1.1.2.2,19.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)). 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 73 [para_into,71.1.1.2.2,71.1.1] ((x^y)^ (y^ (x v y))) v ((y^ (x v y))^y)=y^ (x v y). 82,81 [para_into,71.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^ (x v y))^x)=x^ (x v y). 85 [para_from,71.1.1,19.1.1.2.2] ((x^y)^ (y^ (x v y))) v ((x^y)^y)=x^y. 89 [para_into,85.1.1.1.2.2,71.1.1] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((x^y)^ (y^ (x v y)))^ (y^ (x v y)))= (x^y)^ (y^ (x v y)). 101 [para_from,85.1.1,71.1.1.2.2] (((x^y)^ (y^ (x v y)))^ ((x^y)^y)) v (((x^y)^y)^ (x^y))= (x^y)^y. 107 [para_into,73.1.1.1.2.2,71.1.1,demod,72,72] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((y^ (x v y))^y)^ (y^ (x v y)))= (y^ (x v y))^y. 115 [para_into,73.1.1.1.2.2,19.1.1,demod,20,20] (((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x)) v (((x^ (x v y))^x)^ (x^ (x v y)))= (x^ (x v y))^x. 133 [para_from,81.1.1,73.1.1.2.1.2,demod,82,82] ((((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x))^ (((x^ (x v y))^x)^ (x^ (x v y)))) v ((((x^ (x v y))^x)^ (x^ (x v y)))^ ((x^ (x v y))^x))= ((x^ (x v y))^x)^ (x^ (x v y)). 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 151 [para_into,43.1.1.2.1,71.1.1] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 162,161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 165 [back_demod,151,demod,160] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 189 [para_from,159.1.1,19.1.1.2.2] (((x^y) v (z^x))^x) v (((x^y) v (z^x))^x)= (x^y) v (z^x). 205 [para_from,159.1.1,71.1.1.2.2] (((x^y) v (z^x))^x) v (x^x)=x. 208,207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 212 [back_demod,165,demod,208,208] (x^y) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v y))=y. 228 [para_from,161.1.1,19.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((x^x)^x)=x^x. 230 [para_from,161.1.1,107.1.1.2.2.2,demod,162,162,162,162] ((((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))^ (((y^ (x v x))^x)^ (y^ (x v x)))) v ((((y^ (x v x))^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))= ((y^ (x v x))^x)^ (y^ (x v x)). 234 [para_from,161.1.1,73.1.1.2.1.2,demod,162,162] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((y^ (x v x))^x)^ (y^ (x v x)))= (y^ (x v x))^x. 236 [para_from,161.1.1,85.1.1.1.2.2] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((x^x)^ (y^ (x v x)))^ (y^ (x v x)))= (x^x)^ (y^ (x v x)). 242 [para_from,161.1.1,71.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((y^ (x v x))^x)=y^ (x v x). 292 [para_into,212.1.1.2.1,161.1.1] (x^y) v ((((y v z)^ (u v y))^y)^ (x v y))=y. 397,396 [para_into,292.1.1,19.1.1] ((x v y)^ (z v x))^x=x. 442 [para_into,396.1.1.1.1,71.1.1] (x^ (y v (z^x)))^ (z^x)=z^x. 461,460 [para_into,396.1.1.1.2,159.1.1] ((x v y)^x)^x=x. 504 [para_from,396.1.1,242.1.1.2] ((x^x)^ ((x v y)^ (x v x))) v x= (x v y)^ (x v x). 512 [para_from,396.1.1,205.1.1.1.1.2] (((x^y) v x)^x) v (x^x)=x. 518 [para_from,396.1.1,159.1.1.1.2] ((x^y) v x) v x=x. 540 [para_from,396.1.1,89.1.1.2.1.1,demod,397,397] ((x^ (x^ (((x v y)^ (z v x)) v x)))^ ((x^ (((x v y)^ (z v x)) v x))^x)) v ((x^ (x^ (((x v y)^ (z v x)) v x)))^ (x^ (((x v y)^ (z v x)) v x)))=x^ (x^ (((x v y)^ (z v x)) v x)). 547,546 [para_from,396.1.1,71.1.1.1] x v (x^ (((x v y)^ (z v x)) v x))=x. 599,598 [para_into,460.1.1.1.1,71.1.1] (x^ (y^x))^ (y^x)=y^x. 605,604 [para_into,460.1.1.1.1,19.1.1] (x^ (x^y))^ (x^y)=x^y. 606 [back_demod,540,demod,605] ((x^ (x^ (((x v y)^ (z v x)) v x)))^ ((x^ (((x v y)^ (z v x)) v x))^x)) v (x^ (((x v y)^ (z v x)) v x))=x^ (x^ (((x v y)^ (z v x)) v x)). 624 [para_from,460.1.1,189.1.1.2.1.1,demod,461,461] ((x v (y^ ((x v z)^x)))^ ((x v z)^x)) v ((x v (y^ ((x v z)^x)))^ ((x v z)^x))=x v (y^ ((x v z)^x)). 647,646 [para_from,460.1.1,71.1.1.1] x v (x^ (((x v y)^x) v x))=x. 700 [para_into,518.1.1.1.1,396.1.1] (x v ((x v y)^ (z v x))) v ((x v y)^ (z v x))= (x v y)^ (z v x). 702 [para_from,518.1.1,460.1.1.1.1] (x^ ((x^y) v x))^ ((x^y) v x)= (x^y) v x. 779,778 [para_from,646.1.1,460.1.1.1.1] (x^x)^x=x. 781,780 [para_from,646.1.1,396.1.1.1.1] (x^ (y v x))^x=x. 782 [para_from,646.1.1,133.1.1.2.1.2.2,demod,647,647,779,647,779,647,647,779,647,779,647,779,647] ((((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x)^ (x^ (x^x))) v ((x^ (x^x))^x)=x^ (x^x). 784 [para_from,646.1.1,115.1.1.2.2.2,demod,647,647,779,647,779,647,779] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x) v (x^ (x^x))=x. 790 [para_from,646.1.1,33.1.1.2.1.2.2,demod,647,647] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ ((x^ (x^ (((x v y)^x) v x)))^x)) v (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ (x^ (x^ (((x v y)^x) v x))))= (x^ (x^ (((x v y)^x) v x)))^ (x^x). 800 [para_from,646.1.1,85.1.1.1.2.2,demod,781,605] ((x^ (x^ (((x v y)^x) v x)))^x) v (x^ (((x v y)^x) v x))=x^ (x^ (((x v y)^x) v x)). 861,860 [back_demod,228,demod,779] ((x^x)^ (y^ (x v x))) v x=x^x. 884 [back_demod,606,demod,781] ((x^ (x^ (((x v y)^ (z v x)) v x)))^x) v (x^ (((x v y)^ (z v x)) v x))=x^ (x^ (((x v y)^ (z v x)) v x)). 904 [back_demod,504,demod,861,flip.1] (x v y)^ (x v x)=x^x. 966 [para_into,780.1.1.1.2,646.1.1,demod,781] x^ (x^ (((x v y)^x) v x))=x^ (((x v y)^x) v x). 969,968 [para_into,780.1.1.1.2,512.1.1,demod,779] x^ (x^x)=x^x. 972 [para_into,780.1.1.1.2,242.1.1] (((x^ (y v y))^y)^ (x^ (y v y)))^ ((x^ (y v y))^y)= (x^ (y v y))^y. 976 [para_into,780.1.1.1.2,161.1.1] ((x^ (y v y))^y)^ (x^ (y v y))=x^ (y v y). 990 [para_into,780.1.1.1.2,101.1.1] ((((x^y)^y)^ (x^y))^ ((x^y)^y))^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 999,998 [para_into,780.1.1.1.2,85.1.1] (((x^y)^y)^ (x^y))^ ((x^y)^y)= (x^y)^y. 1007,1006 [para_into,780.1.1.1.2,71.1.1,demod,781] x^ (x^ (y v x))=x^ (y v x). 1021,1020 [back_demod,800,demod,1007,781,647,1007,flip.1] x^ (((x v y)^x) v x)=x. 1029,1028 [back_demod,790,demod,1021,1021,779,1021,1021,779,1021] (((x^x)^ (x^x))^x) v (x^x)= (x^x)^ (x^x). 1033,1032 [back_demod,784,demod,1021,969,1029] (x^x)^ (x^x)=x. 1035,1034 [back_demod,782,demod,1021,1033,969,1033,969,779,969] x v x=x^x. 1064 [back_demod,230,demod,1035,1035,1035,1035,1035,1035,1035,1035,1035] ((((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))^ (((y^ (x^x))^x)^ (y^ (x^x)))) v ((((y^ (x^x))^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))= ((y^ (x^x))^x)^ (y^ (x^x)). 1066 [back_demod,972,demod,1035,1035,1035,1035] (((x^ (y^y))^y)^ (x^ (y^y)))^ ((x^ (y^y))^y)= (x^ (y^y))^y. 1068 [back_demod,234,demod,1035,1035,1035,1035,1035] (((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x)) v (((y^ (x^x))^x)^ (y^ (x^x)))= (y^ (x^x))^x. 1078 [back_demod,990,demod,999] ((x^y)^y)^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 1097,1096 [back_demod,966,demod,1021,1021] x^x=x. 1107 [back_demod,884,demod,1007,781,547,1007,flip.1] x^ (((x v y)^ (z v x)) v x)=x. 1124,1123 [back_demod,976,demod,1035,1097,1035,1097,1035,1097] ((x^y)^y)^ (x^y)=x^y. 1128,1127 [back_demod,904,demod,1035,1097,1097] (x v y)^x=x. 1135 [back_demod,624,demod,1128,1128,1128,1128,1128,1128,1035,1097,1128,flip.1] x v (y^x)=x. 1150,1149 [back_demod,236,demod,1097,1035,1097,1035,1097,1097,1035,1097,1035,1097,599,1097,1035,1097] ((x^ (y^x))^ ((y^x)^x)) v (y^x)=x^ (y^x). 1153 [back_demod,1064,demod,1097,1097,1097,1097,1097,1124,1097,1097,1124,1097,1097,1097,1124] (((x^ (y^x))^ ((y^x)^x))^ (y^x)) v ((y^x)^ ((y^x)^x))=y^x. 1162,1161 [back_demod,1068,demod,1097,1097,1097,1097,1097,1124,1150,1097,flip.1] (x^y)^y=y^ (x^y). 1164,1163 [back_demod,1066,demod,1097,1162,1097,1162,1097,1162,1162,1097,1162] (x^ (y^x))^ ((y^x)^ (x^ (y^x)))=x^ (y^x). 1166,1165 [back_demod,1034,demod,1097] x v x=x. 1179,1178 [back_demod,1078,demod,1162,1162,1162,1164,1162,1162,flip.1] (x^y)^ (y^ (x^y))=y^ (x^y). 1191,1190 [back_demod,1153,demod,1162,1097,1162,1179,1162,1179,1166] x^ (y^x)=y^x. 1203,1202 [back_demod,702,demod,1162,1191] x^ ((x^y) v x)= (x^y) v x. 1205,1204 [back_demod,604,demod,1162,1191] x^ (x^y)=x^y. 1238 [para_from,780.1.1,71.1.1.1,demod,1203] x v ((x^ (y v x)) v x)=x. 1248 [para_from,780.1.1,19.1.1.1] x v ((x^ (y v x))^ ((x^ (y v x)) v x))=x^ (y v x). 1262 [para_from,1127.1.1,23.1.1.2.1,demod,1128,1128] (x^ ((x v y)^ ((x v y) v x))) v (x^ (x v y))=x. 1266 [para_from,1127.1.1,19.1.1.1] x v ((x v y)^ ((x v y) v x))=x v y. 1309 [para_from,1204.1.1,23.1.1.2.1,demod,1205,1205] ((x^y)^ (x^ (x v (x^y)))) v ((x^y)^x)=x^y. 1352,1351 [para_into,1107.1.1.2.1.1,1238.1.1,demod,1203] (x^ (y v x)) v x=x. 1379 [back_demod,1248,demod,1352,781,1166,flip.1] x^ (y v x)=x. 1402,1401 [para_from,1379.1.1,1135.1.1.2] (x v y) v y=x v y. 1410,1409 [back_demod,700,demod,1402] x v ((x v y)^ (z v x))= (x v y)^ (z v x). 1412,1411 [back_demod,1266,demod,1410] (x v y)^ ((x v y) v x)=x v y. 1414,1413 [back_demod,1262,demod,1412,1166] x^ (x v y)=x. 1415 [back_demod,1309,demod,1414,1166] (x^y)^x=x^y. 1432 [para_from,1415.1.1,1135.1.1.2] x v (x^y)=x. 1651,1650 [para_into,442.1.1.1.2,1432.1.1] (x^y)^ (y^x)=y^x. 1686 [para_from,1650.1.1,1415.1.1.1,demod,1651,1651] x^y=y^x. 1687 [binary,1686.1,2.1] $Ans(comm_meet). ------------ end of proof ------------- given clause #98: (wt=10) 1686 [para_from,1650.1.1,1415.1.1.1,demod,1651,1651] x^y=y^x. given clause #99: (wt=14) 1680 [para_from,1650.1.1,1432.1.1.2] (x^y) v (y^x)=x^y. given clause #100: (wt=16) 1642 [para_into,442.1.1.1.2.2,1510.1.1,demod,1511,1511] (((x v y)^ (y v z))^ (u v y))^y=y. given clause #101: (wt=16) 1644 [para_into,442.1.1.1.2.2,1460.1.1,demod,1461,1461] (((x v y)^ (x v z))^ (u v x))^x=x. given clause #102: (wt=16) 1646 [para_into,442.1.1.1.2.2,1438.1.1,demod,1439,1439] (((x v y)^ (z v y))^ (u v y))^y=y. given clause #103: (wt=16) 1648 [para_into,442.1.1.1.2.2,1417.1.1,demod,1418,1418] (((x v y)^ (z v x))^ (u v x))^x=x. given clause #104: (wt=16) 1750 [para_into,1642.1.1.1.2,1423.1.1] (((x v y)^ (y v z))^ (y v u))^y=y. given clause #105: (wt=16) 1754 [para_into,1642.1.1.1,1686.1.1] ((x v y)^ ((z v y)^ (y v u)))^y=y. given clause #106: (wt=16) 1756 [para_into,1642.1.1,1686.1.1] x^ (((y v x)^ (x v z))^ (u v x))=x. given clause #107: (wt=16) 1802 [para_into,1644.1.1.1.2,1423.1.1] (((x v y)^ (x v z))^ (x v u))^x=x. given clause #108: (wt=16) 1806 [para_into,1644.1.1.1,1686.1.1] ((x v y)^ ((y v z)^ (y v u)))^y=y. given clause #109: (wt=16) 1808 [para_into,1644.1.1,1686.1.1] x^ (((x v y)^ (x v z))^ (u v x))=x. given clause #110: (wt=16) 1858 [para_into,1646.1.1.1.2,1423.1.1] (((x v y)^ (z v y))^ (y v u))^y=y. given clause #111: (wt=16) 1862 [para_into,1646.1.1.1,1686.1.1] ((x v y)^ ((z v y)^ (u v y)))^y=y. given clause #112: (wt=16) 1864 [para_into,1646.1.1,1686.1.1] x^ (((y v x)^ (z v x))^ (u v x))=x. given clause #113: (wt=16) 1900 [para_into,1648.1.1.1.2,1423.1.1] (((x v y)^ (z v x))^ (x v u))^x=x. given clause #114: (wt=16) 1904 [para_into,1648.1.1.1,1686.1.1] ((x v y)^ ((y v z)^ (u v y)))^y=y. given clause #115: (wt=16) 1906 [para_into,1648.1.1,1686.1.1] x^ (((x v y)^ (z v x))^ (u v x))=x. given clause #116: (wt=16) 1954 [para_into,1750.1.1.1,1686.1.1] ((x v y)^ ((z v x)^ (x v u)))^x=x. given clause #117: (wt=16) 1956 [para_into,1750.1.1,1686.1.1] x^ (((y v x)^ (x v z))^ (x v u))=x. given clause #118: (wt=16) 2018 [para_into,1754.1.1,1686.1.1] x^ ((y v x)^ ((z v x)^ (x v u)))=x. given clause #119: (wt=16) 2094 [para_into,1802.1.1.1,1686.1.1] ((x v y)^ ((x v z)^ (x v u)))^x=x. given clause #120: (wt=16) 2096 [para_into,1802.1.1,1686.1.1] x^ (((x v y)^ (x v z))^ (x v u))=x. given clause #121: (wt=16) 2144 [para_into,1806.1.1,1686.1.1] x^ ((y v x)^ ((x v z)^ (x v u)))=x. given clause #122: (wt=16) 2210 [para_into,1858.1.1.1,1686.1.1] ((x v y)^ ((z v x)^ (u v x)))^x=x. given clause #123: (wt=16) 2212 [para_into,1858.1.1,1686.1.1] x^ (((y v x)^ (z v x))^ (x v u))=x. given clause #124: (wt=16) 2264 [para_into,1862.1.1,1686.1.1] x^ ((y v x)^ ((z v x)^ (u v x)))=x. given clause #125: (wt=16) 2320 [para_into,1900.1.1.1,1686.1.1] ((x v y)^ ((x v z)^ (u v x)))^x=x. given clause #126: (wt=16) 2322 [para_into,1900.1.1,1686.1.1] x^ (((x v y)^ (z v x))^ (x v u))=x. given clause #127: (wt=16) 2360 [para_into,1904.1.1,1686.1.1] x^ ((y v x)^ ((x v z)^ (u v x)))=x. given clause #128: (wt=16) 2426 [para_into,1954.1.1,1686.1.1] x^ ((x v y)^ ((z v x)^ (x v u)))=x. given clause #129: (wt=16) 2530 [para_into,2094.1.1,1686.1.1] x^ ((x v y)^ ((x v z)^ (x v u)))=x. given clause #130: (wt=16) 2610 [para_into,2210.1.1,1686.1.1] x^ ((x v y)^ ((z v x)^ (u v x)))=x. given clause #131: (wt=16) 2684 [para_into,2320.1.1,1686.1.1] x^ ((x v y)^ ((x v z)^ (u v x)))=x. given clause #132: (wt=18) 448 [para_into,396.1.1.1.1,19.1.1] (x^ (y v (x^z)))^ (x^z)=x^z. given clause #133: (wt=18) 1141 [back_demod,458,demod,1035,1097,1035,1097,1035,1097] (((x^y) v z)^y)^ (x^y)=x^y. given clause #134: (wt=18) 1252 [para_from,1127.1.1,159.1.1.1.1] (x v (y^ (x v z))) v (x v z)=x v z. given clause #135: (wt=16) 2868 [para_into,1252.1.1.1.2.2,1430.1.1,demod,1431,1431] (((x^y) v (x^z)) v (u^x)) v x=x. given clause #136: (wt=16) 2870 [para_into,1252.1.1.1.2.2,1428.1.1,demod,1429,1429] (((x^y) v (y^z)) v (u^y)) v y=y. given clause #137: (wt=16) 2872 [para_into,1252.1.1.1.2.2,1286.1.1,demod,1287,1287] (((x^y) v (z^y)) v (u^y)) v y=y. given clause #138: (wt=16) 2876 [para_into,1252.1.1.1.2.2,159.1.1,demod,160,160] (((x^y) v (z^x)) v (u^x)) v x=x. given clause #139: (wt=16) 3130 [para_into,2868.1.1.1.2,1686.1.1] (((x^y) v (x^z)) v (x^u)) v x=x. given clause #140: (wt=16) 3246 [para_from,2868.1.1,1423.1.1.1,demod,2869] x v (((x^y) v (x^z)) v (u^x))=x. given clause #141: (wt=16) 3348 [para_into,2870.1.1.1.2,1686.1.1] (((x^y) v (y^z)) v (y^u)) v y=y. given clause #142: (wt=16) 3464 [para_from,2870.1.1,1423.1.1.1,demod,2871] x v (((y^x) v (x^z)) v (u^x))=x. given clause #143: (wt=16) 3556 [para_into,2872.1.1.1.2,1686.1.1] (((x^y) v (z^y)) v (y^u)) v y=y. given clause #144: (wt=16) 3672 [para_from,2872.1.1,1423.1.1.1,demod,2873] x v (((y^x) v (z^x)) v (u^x))=x. given clause #145: (wt=16) 3730 [para_into,2876.1.1.1.2,1686.1.1] (((x^y) v (z^x)) v (x^u)) v x=x. given clause #146: (wt=16) 3846 [para_from,2876.1.1,1423.1.1.1,demod,2877] x v (((x^y) v (z^x)) v (u^x))=x. given clause #147: (wt=16) 4078 [para_from,3130.1.1,1423.1.1.1,demod,3131] x v (((x^y) v (x^z)) v (x^u))=x. given clause #148: (wt=16) 4406 [para_from,3348.1.1,1423.1.1.1,demod,3349] x v (((y^x) v (x^z)) v (x^u))=x. given clause #149: (wt=16) 4674 [para_from,3556.1.1,1423.1.1.1,demod,3557] x v (((y^x) v (z^x)) v (x^u))=x. given clause #150: (wt=16) 4898 [para_from,3730.1.1,1423.1.1.1,demod,3731] x v (((x^y) v (z^x)) v (x^u))=x. given clause #151: (wt=18) 1395 [para_from,1379.1.1,1286.1.1.1.2] ((x^ (y v z)) v z) v (y v z)=y v z. given clause #152: (wt=16) 5224 [para_into,1395.1.1.1.1.2,1498.1.1,demod,1499,1499] ((x^y) v ((y^z) v (y^u))) v y=y. given clause #153: (wt=16) 5226 [para_into,1395.1.1.1.1.2,1484.1.1,demod,1485,1485] ((x^y) v ((z^y) v (y^u))) v y=y. given clause #154: (wt=16) 5228 [para_into,1395.1.1.1.1.2,1458.1.1,demod,1459,1459] ((x^y) v ((y^z) v (u^y))) v y=y. given clause #155: (wt=16) 5230 [para_into,1395.1.1.1.1.2,1456.1.1,demod,1457,1457] ((x^y) v ((z^y) v (u^y))) v y=y. given clause #156: (wt=16) 5380 [para_into,5224.1.1.1.1,1686.1.1] ((x^y) v ((x^z) v (x^u))) v x=x. given clause #157: (wt=16) 5600 [para_from,5224.1.1,1423.1.1.1,demod,5225] x v ((y^x) v ((x^z) v (x^u)))=x. given clause #158: (wt=16) 5650 [para_into,5226.1.1.1.1,1686.1.1] ((x^y) v ((z^x) v (x^u))) v x=x. given clause #159: (wt=16) 5818 [para_from,5226.1.1,1423.1.1.1,demod,5227] x v ((y^x) v ((z^x) v (x^u)))=x. given clause #160: (wt=16) 5868 [para_into,5228.1.1.1.1,1686.1.1] ((x^y) v ((x^z) v (u^x))) v x=x. given clause #161: (wt=16) 6036 [para_from,5228.1.1,1423.1.1.1,demod,5229] x v ((y^x) v ((x^z) v (u^x)))=x. given clause #162: (wt=16) 6086 [para_into,5230.1.1.1.1,1686.1.1] ((x^y) v ((z^x) v (u^x))) v x=x. given clause #163: (wt=16) 6202 [para_from,5230.1.1,1423.1.1.1,demod,5231] x v ((y^x) v ((z^x) v (u^x)))=x. given clause #164: (wt=16) 6434 [para_from,5380.1.1,1423.1.1.1,demod,5381] x v ((x^y) v ((x^z) v (x^u)))=x. given clause #165: (wt=16) 6764 [para_from,5650.1.1,1423.1.1.1,demod,5651] x v ((x^y) v ((z^x) v (x^u)))=x. given clause #166: (wt=16) 7042 [para_from,5868.1.1,1423.1.1.1,demod,5869] x v ((x^y) v ((x^z) v (u^x)))=x. given clause #167: (wt=16) 7268 [para_from,6086.1.1,1423.1.1.1,demod,6087] x v ((x^y) v ((z^x) v (u^x)))=x. given clause #168: (wt=18) 1397 [para_from,1379.1.1,159.1.1.1.2] (((x v y)^z) v y) v (x v y)=x v y. given clause #169: (wt=18) 1403 [para_from,1379.1.1,1286.1.1.1.1] (x v (y^ (z v x))) v (z v x)=z v x. given clause #170: (wt=14) 7728 [para_into,1403.1.1.1.2,1413.1.1] (x v y) v (y v x)=y v x. ----> UNIT CONFLICT at 126.31 sec ----> 7949 [binary,7948.1,5.1] $Ans(comm_join). Length of proof is 104. Level of proof is 38. ---------------- PROOF ---------------- 5 [] A v B!=B v A|$Ans(comm_join). 10,9 [] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((y^ (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w)))) v (v6^ (y v (((((y v u)^ (v v y))^y)^w) v ((((y^u) v (v^y)) v y)^ ((((y v u)^ (v v y))^y) v w))))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 12,11 [para_into,9.1.1.2.1.2.1,9.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^g((y^z) v (z^ (y v z)))) v (z^ (x v g((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)). 13 [para_into,11.1.1.1.1.1.2,9.1.1,demod,10,10,10,10,10,10,10,10] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (((y^ (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6)))) v (v7^ (y v (((((y v v)^ (w v y))^y)^v6) v ((((y^v) v (w^y)) v y)^ ((((y v v)^ (w v y))^y) v v6))))))^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 16,15 [para_into,13.1.1.2.1,9.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. 20,19 [para_into,15.1.1.1.1,15.1.1,demod,16] (x^y) v (x^ (x v y))=x. 22,21 [para_from,15.1.1,11.1.1.2.1.2.2.2.1,demod,16,16,16,16,16,16,16,16] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (y^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 23 [para_into,19.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^y)^x)=x^y. 25 [para_from,19.1.1,13.1.1.2.1.2.1.2.1] (((x^y) v (y^ (x v y)))^z) v (((x^g(y)) v (((u^g(y)) v (y^ (u v g(y))))^ (x v g(y))))^ (((x^y) v (y^ (x v y))) v z))=y. 33 [para_into,23.1.1.1.2.2,19.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)). 38,37 [para_into,21.1.1.1.1,21.1.1,demod,22,22,20,flip.1] (x^g(y)) v (y^ (x v g(y)))=y. 41 [para_into,21.1.1.2.1,11.1.1,demod,12,12,20,flip.1] (x^g((y^z) v (z^ (y v z)))) v (z^ (x v g((y^z) v (z^ (y v z)))))= (y^z) v (z^ (y v z)). 43 [para_into,21.1.1.2.1,9.1.1,demod,10,10,20,flip.1] (x^g(y)) v (((y^ (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))) v (w^ (y v (((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v))))))^ (x v g(y)))=y. 51 [back_demod,25,demod,38,38] (((x^y) v (y^ (x v y)))^z) v (y^ (((x^y) v (y^ (x v y))) v z))=y. 72,71 [para_into,41.1.1,51.1.1,flip.1] (x^y) v (y^ (x v y))=y. 73 [para_into,71.1.1.2.2,71.1.1] ((x^y)^ (y^ (x v y))) v ((y^ (x v y))^y)=y^ (x v y). 82,81 [para_into,71.1.1.2.2,19.1.1] ((x^y)^ (x^ (x v y))) v ((x^ (x v y))^x)=x^ (x v y). 85 [para_from,71.1.1,19.1.1.2.2] ((x^y)^ (y^ (x v y))) v ((x^y)^y)=x^y. 89 [para_into,85.1.1.1.2.2,71.1.1] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((x^y)^ (y^ (x v y)))^ (y^ (x v y)))= (x^y)^ (y^ (x v y)). 101 [para_from,85.1.1,71.1.1.2.2] (((x^y)^ (y^ (x v y)))^ ((x^y)^y)) v (((x^y)^y)^ (x^y))= (x^y)^y. 107 [para_into,73.1.1.1.2.2,71.1.1,demod,72,72] (((x^y)^ (y^ (x v y)))^ ((y^ (x v y))^y)) v (((y^ (x v y))^y)^ (y^ (x v y)))= (y^ (x v y))^y. 115 [para_into,73.1.1.1.2.2,19.1.1,demod,20,20] (((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x)) v (((x^ (x v y))^x)^ (x^ (x v y)))= (x^ (x v y))^x. 133 [para_from,81.1.1,73.1.1.2.1.2,demod,82,82] ((((x^y)^ (x^ (x v y)))^ ((x^ (x v y))^x))^ (((x^ (x v y))^x)^ (x^ (x v y)))) v ((((x^ (x v y))^x)^ (x^ (x v y)))^ ((x^ (x v y))^x))= ((x^ (x v y))^x)^ (x^ (x v y)). 149 [para_into,43.1.1.2.1.1.2,71.1.1,demod,72] (x^g(y)) v (((y^ (((y^z) v (u^y)) v y)) v (v^ (y v (((y^z) v (u^y)) v y))))^ (x v g(y)))=y. 151 [para_into,43.1.1.2.1,71.1.1] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v ((((y^z) v (u^y)) v y)^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 155 [para_into,149.1.1.2.1,71.1.1] (x^g(y)) v ((((y^z) v (u^y)) v y)^ (x v g(y)))=y. 157 [para_into,149.1.1,19.1.1] (x^ (((x^y) v (z^x)) v x)) v (u^ (x v (((x^y) v (z^x)) v x)))=x. 160,159 [para_into,155.1.1,19.1.1] ((x^y) v (z^x)) v x=x. 162,161 [back_demod,157,demod,160,160] (x^x) v (y^ (x v x))=x. 165 [back_demod,151,demod,160] (x^g(y)) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v g(y)))=y. 189 [para_from,159.1.1,19.1.1.2.2] (((x^y) v (z^x))^x) v (((x^y) v (z^x))^x)= (x^y) v (z^x). 205 [para_from,159.1.1,71.1.1.2.2] (((x^y) v (z^x))^x) v (x^x)=x. 208,207 [para_into,161.1.1,37.1.1,flip.1] g(x)=x. 212 [back_demod,165,demod,208,208] (x^y) v ((((((y v z)^ (u v y))^y)^v) v (y^ ((((y v z)^ (u v y))^y) v v)))^ (x v y))=y. 228 [para_from,161.1.1,19.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((x^x)^x)=x^x. 230 [para_from,161.1.1,107.1.1.2.2.2,demod,162,162,162,162] ((((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))^ (((y^ (x v x))^x)^ (y^ (x v x)))) v ((((y^ (x v x))^x)^ (y^ (x v x)))^ ((y^ (x v x))^x))= ((y^ (x v x))^x)^ (y^ (x v x)). 234 [para_from,161.1.1,73.1.1.2.1.2,demod,162,162] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((y^ (x v x))^x)^ (y^ (x v x)))= (y^ (x v x))^x. 236 [para_from,161.1.1,85.1.1.1.2.2] (((x^x)^ (y^ (x v x)))^ ((y^ (x v x))^x)) v (((x^x)^ (y^ (x v x)))^ (y^ (x v x)))= (x^x)^ (y^ (x v x)). 242 [para_from,161.1.1,71.1.1.2.2] ((x^x)^ (y^ (x v x))) v ((y^ (x v x))^x)=y^ (x v x). 292 [para_into,212.1.1.2.1,161.1.1] (x^y) v ((((y v z)^ (u v y))^y)^ (x v y))=y. 397,396 [para_into,292.1.1,19.1.1] ((x v y)^ (z v x))^x=x. 461,460 [para_into,396.1.1.1.2,159.1.1] ((x v y)^x)^x=x. 504 [para_from,396.1.1,242.1.1.2] ((x^x)^ ((x v y)^ (x v x))) v x= (x v y)^ (x v x). 512 [para_from,396.1.1,205.1.1.1.1.2] (((x^y) v x)^x) v (x^x)=x. 518 [para_from,396.1.1,159.1.1.1.2] ((x^y) v x) v x=x. 540 [para_from,396.1.1,89.1.1.2.1.1,demod,397,397] ((x^ (x^ (((x v y)^ (z v x)) v x)))^ ((x^ (((x v y)^ (z v x)) v x))^x)) v ((x^ (x^ (((x v y)^ (z v x)) v x)))^ (x^ (((x v y)^ (z v x)) v x)))=x^ (x^ (((x v y)^ (z v x)) v x)). 547,546 [para_from,396.1.1,71.1.1.1] x v (x^ (((x v y)^ (z v x)) v x))=x. 599,598 [para_into,460.1.1.1.1,71.1.1] (x^ (y^x))^ (y^x)=y^x. 605,604 [para_into,460.1.1.1.1,19.1.1] (x^ (x^y))^ (x^y)=x^y. 606 [back_demod,540,demod,605] ((x^ (x^ (((x v y)^ (z v x)) v x)))^ ((x^ (((x v y)^ (z v x)) v x))^x)) v (x^ (((x v y)^ (z v x)) v x))=x^ (x^ (((x v y)^ (z v x)) v x)). 624 [para_from,460.1.1,189.1.1.2.1.1,demod,461,461] ((x v (y^ ((x v z)^x)))^ ((x v z)^x)) v ((x v (y^ ((x v z)^x)))^ ((x v z)^x))=x v (y^ ((x v z)^x)). 647,646 [para_from,460.1.1,71.1.1.1] x v (x^ (((x v y)^x) v x))=x. 700 [para_into,518.1.1.1.1,396.1.1] (x v ((x v y)^ (z v x))) v ((x v y)^ (z v x))= (x v y)^ (z v x). 702 [para_from,518.1.1,460.1.1.1.1] (x^ ((x^y) v x))^ ((x^y) v x)= (x^y) v x. 779,778 [para_from,646.1.1,460.1.1.1.1] (x^x)^x=x. 781,780 [para_from,646.1.1,396.1.1.1.1] (x^ (y v x))^x=x. 782 [para_from,646.1.1,133.1.1.2.1.2.2,demod,647,647,779,647,779,647,647,779,647,779,647,779,647] ((((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x)^ (x^ (x^x))) v ((x^ (x^x))^x)=x^ (x^x). 784 [para_from,646.1.1,115.1.1.2.2.2,demod,647,647,779,647,779,647,779] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^x) v (x^ (x^x))=x. 790 [para_from,646.1.1,33.1.1.2.1.2.2,demod,647,647] (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ ((x^ (x^ (((x v y)^x) v x)))^x)) v (((x^ (x^ (((x v y)^x) v x)))^ (x^x))^ (x^ (x^ (((x v y)^x) v x))))= (x^ (x^ (((x v y)^x) v x)))^ (x^x). 800 [para_from,646.1.1,85.1.1.1.2.2,demod,781,605] ((x^ (x^ (((x v y)^x) v x)))^x) v (x^ (((x v y)^x) v x))=x^ (x^ (((x v y)^x) v x)). 861,860 [back_demod,228,demod,779] ((x^x)^ (y^ (x v x))) v x=x^x. 884 [back_demod,606,demod,781] ((x^ (x^ (((x v y)^ (z v x)) v x)))^x) v (x^ (((x v y)^ (z v x)) v x))=x^ (x^ (((x v y)^ (z v x)) v x)). 904 [back_demod,504,demod,861,flip.1] (x v y)^ (x v x)=x^x. 966 [para_into,780.1.1.1.2,646.1.1,demod,781] x^ (x^ (((x v y)^x) v x))=x^ (((x v y)^x) v x). 969,968 [para_into,780.1.1.1.2,512.1.1,demod,779] x^ (x^x)=x^x. 972 [para_into,780.1.1.1.2,242.1.1] (((x^ (y v y))^y)^ (x^ (y v y)))^ ((x^ (y v y))^y)= (x^ (y v y))^y. 976 [para_into,780.1.1.1.2,161.1.1] ((x^ (y v y))^y)^ (x^ (y v y))=x^ (y v y). 990 [para_into,780.1.1.1.2,101.1.1] ((((x^y)^y)^ (x^y))^ ((x^y)^y))^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 999,998 [para_into,780.1.1.1.2,85.1.1] (((x^y)^y)^ (x^y))^ ((x^y)^y)= (x^y)^y. 1007,1006 [para_into,780.1.1.1.2,71.1.1,demod,781] x^ (x^ (y v x))=x^ (y v x). 1021,1020 [back_demod,800,demod,1007,781,647,1007,flip.1] x^ (((x v y)^x) v x)=x. 1029,1028 [back_demod,790,demod,1021,1021,779,1021,1021,779,1021] (((x^x)^ (x^x))^x) v (x^x)= (x^x)^ (x^x). 1033,1032 [back_demod,784,demod,1021,969,1029] (x^x)^ (x^x)=x. 1035,1034 [back_demod,782,demod,1021,1033,969,1033,969,779,969] x v x=x^x. 1064 [back_demod,230,demod,1035,1035,1035,1035,1035,1035,1035,1035,1035] ((((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))^ (((y^ (x^x))^x)^ (y^ (x^x)))) v ((((y^ (x^x))^x)^ (y^ (x^x)))^ ((y^ (x^x))^x))= ((y^ (x^x))^x)^ (y^ (x^x)). 1066 [back_demod,972,demod,1035,1035,1035,1035] (((x^ (y^y))^y)^ (x^ (y^y)))^ ((x^ (y^y))^y)= (x^ (y^y))^y. 1068 [back_demod,234,demod,1035,1035,1035,1035,1035] (((x^x)^ (y^ (x^x)))^ ((y^ (x^x))^x)) v (((y^ (x^x))^x)^ (y^ (x^x)))= (y^ (x^x))^x. 1078 [back_demod,990,demod,999] ((x^y)^y)^ (((x^y)^y)^ (x^y))= ((x^y)^y)^ (x^y). 1097,1096 [back_demod,966,demod,1021,1021] x^x=x. 1107 [back_demod,884,demod,1007,781,547,1007,flip.1] x^ (((x v y)^ (z v x)) v x)=x. 1124,1123 [back_demod,976,demod,1035,1097,1035,1097,1035,1097] ((x^y)^y)^ (x^y)=x^y. 1128,1127 [back_demod,904,demod,1035,1097,1097] (x v y)^x=x. 1135 [back_demod,624,demod,1128,1128,1128,1128,1128,1128,1035,1097,1128,flip.1] x v (y^x)=x. 1150,1149 [back_demod,236,demod,1097,1035,1097,1035,1097,1097,1035,1097,1035,1097,599,1097,1035,1097] ((x^ (y^x))^ ((y^x)^x)) v (y^x)=x^ (y^x). 1153 [back_demod,1064,demod,1097,1097,1097,1097,1097,1124,1097,1097,1124,1097,1097,1097,1124] (((x^ (y^x))^ ((y^x)^x))^ (y^x)) v ((y^x)^ ((y^x)^x))=y^x. 1162,1161 [back_demod,1068,demod,1097,1097,1097,1097,1097,1124,1150,1097,flip.1] (x^y)^y=y^ (x^y). 1164,1163 [back_demod,1066,demod,1097,1162,1097,1162,1097,1162,1162,1097,1162] (x^ (y^x))^ ((y^x)^ (x^ (y^x)))=x^ (y^x). 1166,1165 [back_demod,1034,demod,1097] x v x=x. 1179,1178 [back_demod,1078,demod,1162,1162,1162,1164,1162,1162,flip.1] (x^y)^ (y^ (x^y))=y^ (x^y). 1191,1190 [back_demod,1153,demod,1162,1097,1162,1179,1162,1179,1166] x^ (y^x)=y^x. 1203,1202 [back_demod,702,demod,1162,1191] x^ ((x^y) v x)= (x^y) v x. 1238 [para_from,780.1.1,71.1.1.1,demod,1203] x v ((x^ (y v x)) v x)=x. 1248 [para_from,780.1.1,19.1.1.1] x v ((x^ (y v x))^ ((x^ (y v x)) v x))=x^ (y v x). 1262 [para_from,1127.1.1,23.1.1.2.1,demod,1128,1128] (x^ ((x v y)^ ((x v y) v x))) v (x^ (x v y))=x. 1266 [para_from,1127.1.1,19.1.1.1] x v ((x v y)^ ((x v y) v x))=x v y. 1286 [para_from,1190.1.1,159.1.1.1.1] ((x^y) v (z^y)) v y=y. 1352,1351 [para_into,1107.1.1.2.1.1,1238.1.1,demod,1203] (x^ (y v x)) v x=x. 1379 [back_demod,1248,demod,1352,781,1166,flip.1] x^ (y v x)=x. 1402,1401 [para_from,1379.1.1,1135.1.1.2] (x v y) v y=x v y. 1403 [para_from,1379.1.1,1286.1.1.1.1] (x v (y^ (z v x))) v (z v x)=z v x. 1410,1409 [back_demod,700,demod,1402] x v ((x v y)^ (z v x))= (x v y)^ (z v x). 1412,1411 [back_demod,1266,demod,1410] (x v y)^ ((x v y) v x)=x v y. 1413 [back_demod,1262,demod,1412,1166] x^ (x v y)=x. 1423 [para_from,1413.1.1,1135.1.1.2] (x v y) v x=x v y. 7729,7728 [para_into,1403.1.1.1.2,1413.1.1] (x v y) v (y v x)=y v x. 7948 [para_from,7728.1.1,1423.1.1.1,demod,7729,7729] x v y=y v x. 7949 [binary,7948.1,5.1] $Ans(comm_join). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 170 clauses generated 20626 para_from generated 8972 para_into generated 11654 demod & eval rewrites 50029 clauses wt,lit,sk delete 2958 tautologies deleted 0 clauses forward subsumed 14369 (subsumed by sos) 2 unit deletions 0 factor simplifications 0 clauses kept 3969 new demodulators 3966 empty clauses 7 clauses back demodulated 666 clauses back subsumed 0 usable size 111 sos size 3192 demodulators size 3300 passive size 7 hot size 0 Kbytes malloced 9580 ----------- times (seconds) ----------- user CPU time 126.50 (0 hr, 2 min, 6 sec) system CPU time 12.20 (0 hr, 0 min, 12 sec) wall-clock time 144 (0 hr, 2 min, 24 sec) input time 0.11 clausify time 0.00 process input 0.04 para_into time 10.56 para_from time 7.87 pre_process time 91.96 renumber time 6.57 demod time 36.26 order equalities 7.61 unit deleletion 0.00 factor simplify 0.00 weigh cl time 6.56 sort lits time 0.00 forward subsume 2.41 delete cl time 5.70 keep cl time 15.24 print_cl time 0.00 conflict time 1.52 new demod time 8.48 post_process time 14.31 back demod time 9.60 back subsume 4.48 factor time 0.00 unindex time 1.42 The job finished Mon Mar 6 15:07:58 1995