----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Fri Sep 12 16:35:27 2003 The command was "otter". The process ID is 26068. include("ortholattice-header"). ------- start included file ortholattice-header------- op(400,infix,^). op(400,infix,v). lex([A,B,C,D,0,1,x v x,c(x),x^x,f(x,x)]). set(anl_eq). 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). assign(pick_given_ratio,3). assign(max_weight,25). clear(detailed_history). assign(max_seconds,60). assign(max_mem,100000). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). clear(print_kept). assign(stats_level,1). list(usable). 0 [] x=x. end_of_list. ------- end included file ortholattice-header------- list(sos). 0 [] x v (y v z)=y v (x v z). 0 [] x^ (y^z)=y^ (x^z). 0 [] x v (x^y)=x. 0 [] x^ (x v y)=x. 0 [] x v (y^ (x v z))=x v (z^ (x v y)). 0 [] A v (B^ (A v C))!= (A v B)^ (A v C)|$Ans(MOD2). end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 1 [] x=x. Following clause subsumed by 1 during input processing: 0 [copy,1,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=11): 2 [] x v (y v z)=y v (x v z). ** KEPT (pick-wt=11): 3 [] x^ (y^z)=y^ (x^z). ** KEPT (pick-wt=7): 4 [] x v (x^y)=x. ---> New Demodulator: 5 [new_demod,4] x v (x^y)=x. ** KEPT (pick-wt=7): 6 [] x^ (x v y)=x. ---> New Demodulator: 7 [new_demod,6] x^ (x v y)=x. ** KEPT (pick-wt=15): 8 [] x v (y^ (x v z))=x v (z^ (x v y)). ** KEPT (pick-wt=15): 10 [copy,9,flip.1] (A v B)^ (A v C)!=A v (B^ (A v C))|$Ans(MOD2). Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] x v (y v z)=y v (x v z). Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] x^ (y^z)=y^ (x^z). >>>> Starting back demodulation with 5. >>>> Starting back demodulation with 7. Following clause subsumed by 8 during input processing: 0 [copy,8,flip.1] x v (y^ (x v z))=x v (z^ (x v y)). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=11) 2 [] x v (y v z)=y v (x v z). given clause #2: (wt=7) 4 [] x v (x^y)=x. given clause #3: (wt=7) 6 [] x^ (x v y)=x. given clause #4: (wt=5) 15 [para_into,6,4] x^x=x. given clause #5: (wt=11) 3 [] x^ (y^z)=y^ (x^z). given clause #6: (wt=5) 19 [para_from,6,4] x v x=x. given clause #7: (wt=9) 17 [para_into,6,2] x^ (y v (x v z))=x. given clause #8: (wt=7) 35 [para_into,17,19] x^ (y v x)=x. given clause #9: (wt=15) 8 [] x v (y^ (x v z))=x v (z^ (x v y)). given clause #10: (wt=7) 47 [para_into,8,19,demod,7,20] x v (y^x)=x. given clause #11: (wt=9) 21 [para_into,3,15,flip.1] x^ (y^x)=y^x. given clause #12: (wt=7) 81 [para_into,21,35,demod,36] (x v y)^y=y. given clause #13: (wt=15) 10 [copy,9,flip.1] (A v B)^ (A v C)!=A v (B^ (A v C))|$Ans(MOD2). given clause #14: (wt=7) 85 [para_into,21,6,demod,7] (x v y)^x=x. given clause #15: (wt=9) 29 [para_from,3,4] x v (y^ (x^z))=x. given clause #16: (wt=9) 33 [para_from,19,2,flip.1] x v (y v x)=y v x. given clause #17: (wt=15) 11 [para_into,2,2] x v (y v (z v u))=z v (x v (y v u)). given clause #18: (wt=7) 123 [para_into,33,47,demod,48] (x^y) v y=y. given clause #19: (wt=7) 129 [para_into,33,4,demod,5] (x^y) v x=x. given clause #20: (wt=9) 41 [para_into,35,4] (x^y)^x=x^y. given clause #21: (wt=15) 12 [copy,11,flip.1] x v (y v (z v u))=y v (z v (x v u)). given clause #22: (wt=9) 63 [para_into,47,35] (x v y) v y=x v y. given clause #23: (wt=9) 67 [para_into,47,6] (x v y) v x=x v y. given clause #24: (wt=9) 71 [back_demod,31,demod,64] x v (x v y)=x v y. given clause #25: (wt=11) 13 [para_from,4,2,flip.1] x v (y v (x^z))=y v x. given clause #26: (wt=7) 301 [para_into,13,47] x v y=y v x. given clause #27: (wt=9) 73 [para_from,47,35] (x^y)^y=x^y. given clause #28: (wt=9) 79 [back_demod,26,demod,74] x^ (x^y)=x^y. given clause #29: (wt=11) 23 [para_into,3,6,flip.1] x^ (y^ (x v z))=y^x. given clause #30: (wt=7) 356 [para_into,23,35] x^y=y^x. given clause #31: (wt=9) 83 [para_into,21,17,demod,18] (x v (y v z))^y=y. given clause #32: (wt=9) 111 [para_into,29,21] x v (y^ (z^x))=x. given clause #33: (wt=15) 25 [para_into,3,3] x^ (y^ (z^u))=z^ (x^ (y^u)). given clause #34: (wt=9) 125 [para_into,33,29,demod,30] (x^ (y^z)) v y=y. given clause #35: (wt=9) 133 [para_from,33,17] x^ (y v (z v x))=x. given clause #36: (wt=9) 204 [para_from,41,29] x v ((x^y)^z)=x. given clause #37: (wt=15) 28 [copy,25,flip.1] x^ (y^ (z^u))=y^ (z^ (x^u)). given clause #38: (wt=9) 279 [para_from,67,17] x^ ((x v y) v z)=x. given clause #39: (wt=9) 295 [para_into,13,129,demod,5,flip.1] ((x^y)^z) v x=x. given clause #40: (wt=9) 350 [para_into,23,85,demod,7,flip.1] ((x v y) v z)^x=x. given clause #41: (wt=11) 37 [para_into,17,2] x^ (y v (z v (x v u)))=x. given clause #42: (wt=9) 378 [para_into,83,301] (x v (y v z))^z=z. given clause #43: (wt=9) 400 [para_into,111,356] x v ((y^x)^z)=x. given clause #44: (wt=9) 402 [para_into,111,301] (x^ (y^z)) v z=z. given clause #45: (wt=13) 39 [para_from,17,3,flip.1] x^ (y^ (z v (x v u)))=y^x. given clause #46: (wt=9) 525 [para_into,133,301] x^ ((y v x) v z)=x. given clause #47: (wt=9) 658 [para_into,295,356] ((x^y)^z) v y=y. given clause #48: (wt=9) 697 [para_into,350,301] ((x v y) v z)^y=y. given clause #49: (wt=13) 43 [para_into,35,2] (x v y)^ (x v (z v y))=x v y. given clause #50: (wt=11) 45 [para_from,35,3,flip.1] x^ (y^ (z v x))=y^x. given clause #51: (wt=11) 77 [para_from,47,2,flip.1] x v (y v (z^x))=y v x. given clause #52: (wt=11) 99 [para_from,81,3,flip.1] (x v y)^ (z^y)=z^y. given clause #53: (wt=23) 49 [para_into,8,8] x v (y^ (x v (z^ (x v u))))=x v ((u^ (x v z))^ (x v y)). given clause #54: (wt=11) 105 [para_from,85,3,flip.1] (x v y)^ (z^x)=z^x. given clause #55: (wt=11) 107 [para_into,29,85] (x v y) v (z^x)=x v y. given clause #56: (wt=11) 109 [para_into,29,81] (x v y) v (z^y)=x v y. given clause #57: (wt=19) 52 [para_into,8,2] x v (y^ (z v (x v u)))=x v ((z v u)^ (x v y)). given clause #58: (wt=11) 113 [para_into,29,3] x v (y^ (z^ (x^u)))=x. given clause #59: (wt=11) 182 [para_from,123,17] (x^y)^ (z v y)=x^y. given clause #60: (wt=11) 185 [para_from,123,2,flip.1] (x^y) v (z v y)=z v y. given clause #61: (wt=13) 53 [para_into,8,17,flip.1] x v ((y v z)^ (x v y))=x v y. given clause #62: (wt=11) 196 [para_from,129,17] (x^y)^ (z v x)=x^y. given clause #63: (wt=11) 199 [para_from,129,2,flip.1] (x^y) v (z v x)=z v x. given clause #64: (wt=11) 235 [para_from,12,85] (x v (y v (z v u)))^z=z. given clause #65: (wt=23) 57 [copy,49,flip.1] x v ((y^ (x v z))^ (x v u))=x v (u^ (x v (z^ (x v y)))). given clause #66: (wt=11) 299 [para_into,13,63,demod,14,flip.1] (x v (y^z)) v y=x v y. given clause #67: (wt=11) 319 [para_into,301,2] x v (y v z)= (x v z) v y. given clause #68: (wt=11) 324 [para_from,301,13] x v ((x^y) v z)=z v x. given clause #69: (wt=19) 58 [copy,52,flip.1] x v ((y v z)^ (x v u))=x v (u^ (y v (x v z))). given clause #70: (wt=11) 332 [para_from,301,2] x v (y v z)=z v (x v y). given clause #71: (wt=11) 333 [copy,324,flip.1] x v y=y v ((y^z) v x). given clause #72: (wt=11) 339 [copy,332,flip.1] x v (y v z)=y v (z v x). given clause #73: (wt=19) 59 [para_from,8,35] (x^ (y v z))^ (y v (z^ (y v x)))=x^ (y v z). given clause #74: (wt=11) 352 [para_into,23,73,demod,24,flip.1] (x^ (y v z))^y=x^y. given clause #75: (wt=11) 367 [para_into,356,3] x^ (y^z)= (x^z)^y. given clause #76: (wt=11) 370 [para_from,356,23] x^ ((x v y)^z)=z^x. given clause #77: (wt=19) 61 [para_from,8,2] x v (y v (z^ (y v u)))=y v (x v (u^ (y v z))). given clause #78: (wt=11) 373 [para_from,356,3] x^ (y^z)=z^ (x^y). given clause #79: (wt=11) 374 [copy,370,flip.1] x^y=y^ ((y v z)^x). given clause #80: (wt=11) 377 [copy,373,flip.1] x^ (y^z)=y^ (z^x). given clause #81: (wt=19) 62 [copy,61,flip.1] x v (y v (z^ (x v u)))=y v (x v (u^ (x v z))). given clause #82: (wt=11) 380 [para_into,83,129] (x v y)^ (y^z)=y^z. given clause #83: (wt=11) 480 [para_into,125,85] (x^y) v (y v z)=y v z. given clause #84: (wt=11) 486 [para_into,125,3] (x^ (y^ (z^u))) v z=z. given clause #85: (wt=13) 69 [para_into,47,3] (x^y) v (x^ (z^y))=x^y. given clause #86: (wt=11) 660 [para_into,295,85] (x^y) v (x v z)=x v z. given clause #87: (wt=11) 701 [para_into,350,129] (x v y)^ (x^z)=x^z. given clause #88: (wt=11) 740 [para_into,37,301] x^ (y v (z v (u v x)))=x. given clause #89: (wt=13) 89 [para_from,21,3,flip.1] x^ (y^ (z^x))=y^ (z^x). given clause #90: (wt=11) 1076 [para_into,45,378,demod,36,flip.1] (x v (y v (z v u)))^u=u. given clause #91: (wt=11) 1117 [para_into,77,402,demod,48,flip.1] (x^ (y^ (z^u))) v u=u. given clause #92: (wt=11) 1234 [para_into,107,402,demod,403] x v (y^ (z^ (u^x)))=x. given clause #93: (wt=13) 93 [para_into,81,2] (x v (y v z))^ (x v z)=x v z. given clause #94: (wt=11) 1730 [para_into,319,301,flip.1] (x v y) v z=x v (y v z). given clause #95: (wt=11) 1741 [para_into,319,301,demod,1731,1731] x v (y v z)=z v (y v x). given clause #96: (wt=11) 1780 [back_demod,1401,demod,1731,1731,412] x v (y v z)=x v (z v y). given clause #97: (wt=13) 95 [para_into,81,3] x^ ((y v (x^z))^z)=x^z. given clause #98: (wt=11) 1884 [para_from,324,43] (x v y)^ (y v x)=x v y. given clause #99: (wt=11) 2023 [para_into,333,301,flip.1] x v ((x^y) v z)=x v z. given clause #100: (wt=11) 2221 [para_into,367,356,flip.1] (x^y)^z=x^ (y^z). given clause #101: (wt=13) 101 [para_into,85,3] x^ (((x^y) v z)^y)=x^y. given clause #102: (wt=11) 2228 [para_into,367,356,demod,2222,2222] x^ (y^z)=z^ (y^x). given clause #103: (wt=11) 2299 [back_demod,1991,demod,2222,1009] x^ (y v z)=x^ (z v y). given clause #104: (wt=11) 2375 [back_demod,955,demod,2222,2222,2222,538,2222] x^ (y^z)=x^ (z^y). given clause #105: (wt=13) 117 [para_from,29,81] x^ (y^ (x^z))=y^ (x^z). given clause #106: (wt=11) 2541 [para_into,374,356,flip.1] x^ ((x v y)^z)=x^z. given clause #107: (wt=11) 2651 [para_into,380,3] x^ ((y v x)^z)=x^z. given clause #108: (wt=11) 2673 [para_into,480,2] x v ((y^x) v z)=x v z. given clause #109: (wt=13) 121 [para_from,29,2,flip.1] x v (y v (z^ (x^u)))=y v x. given clause #110: (wt=11) 3350 [para_into,2228,1884,demod,3258] x^ (y v z)= (z v y)^x. given clause #111: (wt=11) 3362 [copy,3350,flip.1] (x v y)^z=z^ (y v x). given clause #112: (wt=11) 3661 [para_into,3350,356] (x v y)^z= (y v x)^z. given clause #113: (wt=21) 127 [para_into,33,8] (x^ (y v z)) v (y v (z^ (y v x)))=y v (x^ (y v z)). given clause #114: (wt=13) 136 [para_from,33,2,flip.1] x v (y v (z v x))=y v (z v x). given clause #115: (wt=13) 150 [para_into,11,19,demod,64,flip.1] x v (y v (x v z))=y v (x v z). given clause #116: (wt=13) 172 [para_into,123,3] (x^ (y^z)) v (x^z)=x^z. given clause #117: (wt=15) 139 [para_into,11,47,flip.1] x v (y v (z v (u^x)))=y v (z v x). given clause #118: (wt=13) 176 [para_into,123,2] x v ((y^ (x v z)) v z)=x v z. given clause #119: (wt=13) 190 [para_into,129,2] x v (((x v y)^z) v y)=x v y. given clause #120: (wt=13) 239 [para_from,12,17] x^ (y v (z v (u v (x v v))))=x. given clause #121: (wt=17) 141 [para_into,11,33,flip.1] x v (y v (z v (u v x)))=y v (z v (u v x)). given clause #122: (wt=13) 302 [para_into,13,8] x v (y v (z^ (y v x)))=y v x. ----> UNIT CONFLICT at 0.64 sec ----> 4219 [binary,4218,369] $Ans(MOD2). Length of proof is 23. Level of proof is 7. ---------------- PROOF ---------------- 2 [] x v (y v z)=y v (x v z). 3 [] x^ (y^z)=y^ (x^z). 4 [] x v (x^y)=x. 7,6 [] x^ (x v y)=x. 8 [] x v (y^ (x v z))=x v (z^ (x v y)). 9 [] A v (B^ (A v C))!= (A v B)^ (A v C)|$Ans(MOD2). 10 [copy,9,flip.1] (A v B)^ (A v C)!=A v (B^ (A v C))|$Ans(MOD2). 13 [para_from,4,2,flip.1] x v (y v (x^z))=y v x. 15 [para_into,6,4] x^x=x. 17 [para_into,6,2] x^ (y v (x v z))=x. 20,19 [para_from,6,4] x v x=x. 21 [para_into,3,15,flip.1] x^ (y^x)=y^x. 23 [para_into,3,6,flip.1] x^ (y^ (x v z))=y^x. 31 [para_into,19,2] x v ((x v y) v y)=x v y. 36,35 [para_into,17,19] x^ (y v x)=x. 47 [para_into,8,19,demod,7,20] x v (y^x)=x. 59 [para_from,8,35] (x^ (y v z))^ (y v (z^ (y v x)))=x^ (y v z). 64,63 [para_into,47,35] (x v y) v y=x v y. 71 [back_demod,31,demod,64] x v (x v y)=x v y. 81 [para_into,21,35,demod,36] (x v y)^y=y. 302 [para_into,13,8] x v (y v (z^ (y v x)))=y v x. 311,310 [para_from,13,81] (x v y)^ (x v (y^z))=x v (y^z). 356 [para_into,23,35] x^y=y^x. 367 [para_into,356,3] x^ (y^z)= (x^z)^y. 369 [para_from,356,10] (A v C)^ (A v B)!=A v (B^ (A v C))|$Ans(MOD2). 2164 [para_into,59,71] ((x v y)^ (x v z))^ (x v (z^ (x v y)))= (x v y)^ (x v z). 2222,2221 [para_into,367,356,flip.1] (x^y)^z=x^ (y^z). 2260,2259 [back_demod,2164,demod,2222,311] (x v y)^ (x v (z^ (x v y)))= (x v y)^ (x v z). 4218 [para_from,302,81,demod,2260] (x v y)^ (x v z)=x v (z^ (x v y)). 4219 [binary,4218,369] $Ans(MOD2). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 122 clauses generated 12003 clauses kept 2712 clauses forward subsumed 10868 clauses back subsumed 5 Kbytes malloced 2937 ----------- times (seconds) ----------- user CPU time 0.64 (0 hr, 0 min, 0 sec) system CPU time 0.14 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) para_into time 0.02 para_from time 0.05 for_sub time 0.03 back_sub time 0.05 conflict time 0.02 demod time 0.09 That finishes the proof of the theorem. Process 26068 finished Fri Sep 12 16:35:28 2003