----- Otter 3.0.3c, Jan 1995 ----- The job was started by mccune on gyro, Tue Feb 14 09:22:20 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(pick_given_ratio,4). assign(max_weight,21). assign(max_mem,12000). list(usable). 0 [] x=x. end_of_list. list(sos). 0 [] x^x=x. 0 [] x^y=y^x. 0 [] ((x v z)^ (y v z))^z=z. 0 [] x v x=x. 0 [] x v y=y v x. 0 [] ((x^z) v (y^z)) v z=z. end_of_list. list(sos). 0 [] x^ (y v (x v z))=x. 0 [] (A v B) v C!=A v (B v C)|$Ans(assoc_join). end_of_list. ------------> process usable: ** KEPT (wt=3): 1 [] x=x. Following clause subsumed by 1 during input processing: 0 [copy,1,flip.1] x=x. ------------> process sos: ** KEPT (wt=5): 2 [] x^x=x. ---> New Demodulator: 3 [new_demod,2] x^x=x. ** KEPT (wt=7): 4 [] x^y=y^x. ** KEPT (wt=11): 5 [] ((x v y)^ (z v y))^y=y. ---> New Demodulator: 6 [new_demod,5] ((x v y)^ (z v y))^y=y. ** KEPT (wt=5): 7 [] x v x=x. ---> New Demodulator: 8 [new_demod,7] x v x=x. ** KEPT (wt=7): 9 [] x v y=y v x. ** KEPT (wt=11): 10 [] ((x^y) v (z^y)) v y=y. ---> New Demodulator: 11 [new_demod,10] ((x^y) v (z^y)) v y=y. ** KEPT (wt=9): 12 [] x^ (y v (x v z))=x. ---> New Demodulator: 13 [new_demod,12] x^ (y v (x v z))=x. ** KEPT (wt=11): 14 [] (A v B) v C!=A v (B v C)|$Ans(assoc_join). >>>> Starting back demodulation with 3. Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] x^y=y^x. >>>> Starting back demodulation with 6. >>>> Starting back demodulation with 8. Following clause subsumed by 9 during input processing: 0 [copy,9,flip.1] x v y=y v x. >>>> Starting back demodulation with 11. >>>> Starting back demodulation with 13. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=5) 2 [] x^x=x. given clause #2: (wt=5) 7 [] x v x=x. given clause #3: (wt=7) 4 [] x^y=y^x. given clause #4: (wt=7) 9 [] x v y=y v x. given clause #5: (wt=9) 12 [] x^ (y v (x v z))=x. given clause #6: (wt=11) 5 [] ((x v y)^ (z v y))^y=y. given clause #7: (wt=7) 17 [para_into,12.1.1.2.2,7.1.1] x^ (y v x)=x. given clause #8: (wt=7) 21 [para_into,12.1.1.2,7.1.1] x^ (x v y)=x. given clause #9: (wt=7) 31 [para_into,5.1.1.1,2.1.1] (x v y)^y=y. given clause #10: (wt=7) 35 [para_into,21.1.1,4.1.1] (x v y)^x=x. given clause #11: (wt=11) 10 [] ((x^y) v (z^y)) v y=y. given clause #12: (wt=7) 57 [para_into,10.1.1.1,7.1.1] (x^y) v y=y. given clause #13: (wt=7) 73 [para_into,57.1.1.1,4.1.1] (x^y) v x=x. given clause #14: (wt=7) 75 [para_into,57.1.1,9.1.1] x v (y^x)=x. given clause #15: (wt=7) 85 [para_into,73.1.1,9.1.1] x v (x^y)=x. given clause #16: (wt=11) 14 [] (A v B) v C!=A v (B v C)|$Ans(assoc_join). given clause #17: (wt=9) 15 [para_into,12.1.1.2.2,9.1.1] x^ (y v (z v x))=x. given clause #18: (wt=9) 19 [para_into,12.1.1.2,9.1.1] x^ ((x v y) v z)=x. given clause #19: (wt=9) 23 [para_into,12.1.1,4.1.1] (x v (y v z))^y=y. given clause #20: (wt=9) 67 [para_into,57.1.1.1,21.1.1] x v (x v y)=x v y. given clause #21: (wt=11) 25 [para_into,5.1.1.1.1,9.1.1] ((x v y)^ (z v x))^x=x. given clause #22: (wt=9) 69 [para_into,57.1.1.1,17.1.1] x v (y v x)=y v x. given clause #23: (wt=9) 79 [para_from,57.1.1,35.1.1.1] x^ (y^x)=y^x. given clause #24: (wt=9) 81 [para_from,57.1.1,21.1.1.2] (x^y)^y=x^y. given clause #25: (wt=9) 89 [para_from,73.1.1,35.1.1.1] x^ (x^y)=x^y. given clause #26: (wt=11) 27 [para_into,5.1.1.1.2,9.1.1] ((x v y)^ (y v z))^y=y. given clause #27: (wt=9) 91 [para_from,73.1.1,21.1.1.2] (x^y)^x=x^y. given clause #28: (wt=9) 93 [para_into,75.1.1.2,21.1.1] (x v y) v x=x v y. given clause #29: (wt=9) 95 [para_into,75.1.1.2,17.1.1] (x v y) v y=x v y. given clause #30: (wt=9) 111 [para_into,15.1.1.2,9.1.1] x^ ((y v x) v z)=x. given clause #31: (wt=11) 33 [para_into,5.1.1,4.1.1] x^ ((y v x)^ (z v x))=x. given clause #32: (wt=9) 113 [para_into,15.1.1,4.1.1] (x v (y v z))^z=z. given clause #33: (wt=9) 129 [para_into,19.1.1,4.1.1] ((x v y) v z)^x=x. given clause #34: (wt=9) 167 [para_into,111.1.1,4.1.1] ((x v y) v z)^y=y. given clause #35: (wt=11) 45 [para_into,10.1.1.1.1,4.1.1] ((x^y) v (z^x)) v x=x. given clause #36: (wt=15) 39 [para_into,10.1.1.1.1,21.1.1] (x v (y^ (x v z))) v (x v z)=x v z. given clause #37: (wt=11) 55 [para_into,10.1.1.1.2,4.1.1] ((x^y) v (y^z)) v y=y. given clause #38: (wt=11) 59 [para_into,10.1.1,9.1.1] x v ((y^x) v (z^x))=x. given clause #39: (wt=11) 77 [para_from,57.1.1,12.1.1.2.2] (x^y)^ (z v y)=x^y. given clause #40: (wt=11) 87 [para_from,73.1.1,12.1.1.2.2] (x^y)^ (z v x)=x^y. given clause #41: (wt=15) 41 [para_into,10.1.1.1.1,17.1.1] (x v (y^ (z v x))) v (z v x)=z v x. given clause #42: (wt=11) 109 [para_into,14.1.1.1,9.1.1] (B v A) v C!=A v (B v C)|$Ans(assoc_join). given clause #43: (wt=11) 110 [para_into,14.1.1,9.1.1] C v (A v B)!=A v (B v C)|$Ans(assoc_join). given clause #44: (wt=11) 123 [para_into,19.1.1.2.1,73.1.1] (x^y)^ (x v z)=x^y. given clause #45: (wt=11) 125 [para_into,19.1.1.2.1,57.1.1] (x^y)^ (y v z)=x^y. given clause #46: (wt=21) 43 [para_into,10.1.1.1.1,12.1.1] (x v (y^ (z v (x v u)))) v (z v (x v u))=z v (x v u). given clause #47: (wt=11) 139 [para_into,23.1.1.1.2,73.1.1] (x v y)^ (y^z)=y^z. given clause #48: (wt=11) 141 [para_into,23.1.1.1.2,57.1.1] (x v y)^ (z^y)=z^y. given clause #49: (wt=11) 149 [para_into,25.1.1.1.2,9.1.1] ((x v y)^ (x v z))^x=x. given clause #50: (wt=11) 151 [para_into,25.1.1,4.1.1] x^ ((x v y)^ (z v x))=x. given clause #51: (wt=15) 49 [para_into,10.1.1.1.2,21.1.1] ((x^ (y v z)) v y) v (y v z)=y v z. given clause #52: (wt=11) 161 [para_into,27.1.1,4.1.1] x^ ((y v x)^ (x v z))=x. given clause #53: (wt=11) 185 [para_into,129.1.1.1.1,73.1.1] (x v y)^ (x^z)=x^z. given clause #54: (wt=11) 187 [para_into,129.1.1.1.1,57.1.1] (x v y)^ (z^x)=z^x. given clause #55: (wt=11) 193 [para_into,45.1.1.1.2,91.1.1] ((x^y) v (x^z)) v x=x. given clause #56: (wt=15) 51 [para_into,10.1.1.1.2,17.1.1] ((x^ (y v z)) v z) v (y v z)=y v z. given clause #57: (wt=11) 205 [para_into,45.1.1,9.1.1] x v ((x^y) v (z^x))=x. given clause #58: (wt=11) 259 [para_into,55.1.1,9.1.1] x v ((y^x) v (x^z))=x. given clause #59: (wt=11) 297 [para_into,77.1.1.1,111.1.1,demod,112] x^ (y v ((z v x) v u))=x. given clause #60: (wt=11) 303 [para_into,77.1.1.1,19.1.1,demod,20] x^ (y v ((x v z) v u))=x. given clause #61: (wt=21) 53 [para_into,10.1.1.1.2,12.1.1] ((x^ (y v (z v u))) v z) v (y v (z v u))=y v (z v u). given clause #62: (wt=11) 305 [para_into,77.1.1.1,15.1.1,demod,16] x^ (y v (z v (u v x)))=x. given clause #63: (wt=11) 307 [para_into,77.1.1.1,12.1.1,demod,13] x^ (y v (z v (x v u)))=x. given clause #64: (wt=11) 321 [para_from,77.1.1,75.1.1.2] (x v y) v (z^y)=x v y. given clause #65: (wt=9) 820 [para_into,321.1.1.1,85.1.1,demod,86] x v (y^ (x^z))=x. given clause #66: (wt=19) 61 [para_from,10.1.1,12.1.1.2.2] ((x^y) v (z^y))^ (u v y)= (x^y) v (z^y). given clause #67: (wt=9) 822 [para_into,321.1.1.1,75.1.1,demod,76] x v (y^ (z^x))=x. given clause #68: (wt=9) 894 [para_into,820.1.1.2,91.1.1] x v ((x^y)^z)=x. given clause #69: (wt=9) 896 [para_into,820.1.1,9.1.1] (x^ (y^z)) v y=y. given clause #70: (wt=9) 982 [para_into,822.1.1.2,91.1.1] x v ((y^x)^z)=x. given clause #71: (wt=17) 63 [para_from,10.1.1,35.1.1.1] x^ ((y^x) v (z^x))= (y^x) v (z^x). given clause #72: (wt=9) 984 [para_into,822.1.1,9.1.1] (x^ (y^z)) v z=z. given clause #73: (wt=9) 1044 [para_into,894.1.1,9.1.1] ((x^y)^z) v x=x. given clause #74: (wt=9) 1126 [para_into,982.1.1,9.1.1] ((x^y)^z) v y=y. given clause #75: (wt=11) 327 [para_from,77.1.1,57.1.1.1] (x^y) v (z v y)=z v y. given clause #76: (wt=17) 65 [para_from,10.1.1,21.1.1.2] ((x^y) v (z^y))^y= (x^y) v (z^y). given clause #77: (wt=11) 349 [para_from,87.1.1,75.1.1.2] (x v y) v (y^z)=x v y. given clause #78: (wt=11) 357 [para_from,87.1.1,57.1.1.1] (x^y) v (z v x)=z v x. given clause #79: (wt=11) 365 [para_into,41.1.1.1.2,21.1.1] (x v y) v (y v x)=y v x. given clause #80: (wt=11) 383 [para_into,109.1.1,9.1.1] C v (B v A)!=A v (B v C)|$Ans(assoc_join). given clause #81: (wt=13) 71 [para_into,57.1.1.1,12.1.1] x v (y v (x v z))=y v (x v z). given clause #82: (wt=11) 384 [para_into,123.1.1.1,167.1.1,demod,168] x^ (((y v x) v z) v u)=x. given clause #83: (wt=11) 386 [para_into,123.1.1.1,129.1.1,demod,130] x^ (((x v y) v z) v u)=x. given clause #84: (wt=11) 388 [para_into,123.1.1.1,113.1.1,demod,114] x^ ((y v (z v x)) v u)=x. given clause #85: (wt=11) 394 [para_into,123.1.1.1,23.1.1,demod,24] x^ ((y v (x v z)) v u)=x. given clause #86: (wt=17) 83 [para_into,73.1.1.1,5.1.1] x v ((y v x)^ (z v x))= (y v x)^ (z v x). given clause #87: (wt=11) 408 [para_from,123.1.1,75.1.1.2] (x v y) v (x^z)=x v y. given clause #88: (wt=11) 416 [para_from,123.1.1,57.1.1.1] (x^y) v (x v z)=x v z. given clause #89: (wt=11) 440 [para_from,125.1.1,75.1.1.2] (x v y) v (z^x)=x v y. given clause #90: (wt=11) 448 [para_from,125.1.1,57.1.1.1] (x^y) v (y v z)=y v z. given clause #91: (wt=13) 97 [para_into,75.1.1.2,12.1.1] (x v (y v z)) v y=x v (y v z). given clause #92: (wt=11) 488 [para_into,139.1.1.2,167.1.1,demod,168] (x v ((y v z) v u))^z=z. given clause #93: (wt=11) 492 [para_into,139.1.1.2,129.1.1,demod,130] (x v ((y v z) v u))^y=y. given clause #94: (wt=11) 494 [para_into,139.1.1.2,113.1.1,demod,114] (x v (y v (z v u)))^u=u. given clause #95: (wt=11) 500 [para_into,139.1.1.2,23.1.1,demod,24] (x v (y v (z v u)))^z=z. given clause #96: (wt=15) 99 [para_from,75.1.1,5.1.1.1.2] ((x v (y^z))^z)^ (y^z)=y^z. given clause #97: (wt=11) 516 [para_into,149.1.1,4.1.1] x^ ((x v y)^ (x v z))=x. given clause #98: (wt=11) 578 [para_into,185.1.1.2,167.1.1,demod,168] (((x v y) v z) v u)^y=y. given clause #99: (wt=11) 586 [para_into,185.1.1.2,129.1.1,demod,130] (((x v y) v z) v u)^x=x. given clause #100: (wt=11) 588 [para_into,185.1.1.2,113.1.1,demod,114] ((x v (y v z)) v u)^z=z. given clause #101: (wt=15) 101 [para_from,75.1.1,5.1.1.1.1] (x^ (y v (z^x)))^ (z^x)=z^x. given clause #102: (wt=11) 594 [para_into,185.1.1.2,23.1.1,demod,24] ((x v (y v z)) v u)^y=y. given clause #103: (wt=11) 604 [para_into,193.1.1,9.1.1] x v ((x^y) v (x^z))=x. given clause #104: (wt=11) 928 [para_from,820.1.1,321.1.1.1,demod,821] x v (y^ (z^ (x^u)))=x. given clause #105: (wt=11) 1012 [para_from,822.1.1,321.1.1.1,demod,823] x v (y^ (z^ (u^x)))=x. given clause #106: (wt=17) 103 [para_into,85.1.1.2,5.1.1] ((x v y)^ (z v y)) v y= (x v y)^ (z v y). given clause #107: (wt=11) 1076 [para_from,894.1.1,321.1.1.1,demod,895] x v (y^ ((x^z)^u))=x. given clause #108: (wt=11) 1154 [para_from,982.1.1,321.1.1.1,demod,983] x v (y^ ((z^x)^u))=x. given clause #109: (wt=11) 1260 [para_into,327.1.1.2,982.1.1,demod,983] (x^ ((y^z)^u)) v z=z. given clause #110: (wt=11) 1262 [para_into,327.1.1.2,894.1.1,demod,895] (x^ ((y^z)^u)) v y=y. given clause #111: (wt=15) 105 [para_from,85.1.1,5.1.1.1.2] ((x v (y^z))^y)^ (y^z)=y^z. given clause #112: (wt=11) 1264 [para_into,327.1.1.2,822.1.1,demod,823] (x^ (y^ (z^u))) v u=u. given clause #113: (wt=11) 1266 [para_into,327.1.1.2,820.1.1,demod,821] (x^ (y^ (z^u))) v z=z. given clause #114: (wt=11) 1284 [para_into,349.1.1.1,982.1.1,demod,983] x v (((y^x)^z)^u)=x. given clause #115: (wt=11) 1286 [para_into,349.1.1.1,894.1.1,demod,895] x v (((x^y)^z)^u)=x. given clause #116: (wt=15) 107 [para_from,85.1.1,5.1.1.1.1] (x^ (y v (x^z)))^ (x^z)=x^z. given clause #117: (wt=11) 1288 [para_into,349.1.1.1,822.1.1,demod,823] x v ((y^ (z^x))^u)=x. given clause #118: (wt=11) 1290 [para_into,349.1.1.1,820.1.1,demod,821] x v ((y^ (x^z))^u)=x. given clause #119: (wt=11) 1320 [para_into,357.1.1.2,982.1.1,demod,983] (((x^y)^z)^u) v y=y. given clause #120: (wt=11) 1322 [para_into,357.1.1.2,894.1.1,demod,895] (((x^y)^z)^u) v x=x. given clause #121: (wt=13) 115 [para_from,15.1.1,75.1.1.2] (x v (y v z)) v z=x v (y v z). given clause #122: (wt=11) 1324 [para_into,357.1.1.2,822.1.1,demod,823] ((x^ (y^z))^u) v z=z. given clause #123: (wt=11) 1326 [para_into,357.1.1.2,820.1.1,demod,821] ((x^ (y^z))^u) v y=y. given clause #124: (wt=11) 1356 [para_from,365.1.1,35.1.1.1] (x v y)^ (y v x)=y v x. given clause #125: (wt=11) 1368 [para_into,71.1.1.2.2,9.1.1,demod,120] x v (y v z)=x v (z v y). given clause #126: (wt=21) 117 [para_from,15.1.1,10.1.1.1.2] ((x^ (y v (z v u))) v u) v (y v (z v u))=y v (z v u). given clause #127: (wt=11) 1995 [para_into,101.1.1.1.2,85.1.1] (x^y)^ (y^x)=y^x. given clause #128: (wt=11) 2986 [para_into,1368.1.1,9.1.1] (x v y) v z=z v (y v x). given clause #129: (wt=11) 2988 [copy,2986,flip.1] x v (y v z)= (z v y) v x. given clause #130: (wt=11) 3100 [para_from,1995.1.1,55.1.1.1.2,demod,3097] (x^y) v (y^x)=y^x. 3265 back subsumes 943. 3265 back subsumes 941. given clause #131: (wt=13) 119 [para_from,15.1.1,57.1.1.1] x v (y v (z v x))=y v (z v x). given clause #132: (wt=11) 3191 [para_into,2988.1.1,9.1.1] (x v y) v z= (y v x) v z. 3288 back subsumes 942. 3288 back subsumes 940. given clause #133: (wt=11) 3264 [para_from,3100.1.1,2988.1.1.2,demod,3101] x v (y^z)= (z^y) v x. given clause #134: (wt=11) 3265 [para_from,3100.1.1,1368.1.1.2,demod,3101] x v (y^z)=x v (z^y). given clause #135: (wt=11) 3278 [para_from,3100.1.1,2986.1.1.1,demod,3101] (x^y) v z=z v (y^x). given clause #136: (wt=21) 121 [para_from,15.1.1,10.1.1.1.1] (x v (y^ (z v (u v x)))) v (z v (u v x))=z v (u v x). given clause #137: (wt=11) 3288 [para_into,3191.1.1.1,3100.1.1,demod,3101] (x^y) v z= (y^x) v z. given clause #138: (wt=13) 131 [para_from,19.1.1,75.1.1.2] ((x v y) v z) v x= (x v y) v z. given clause #139: (wt=13) 135 [para_from,19.1.1,57.1.1.1] x v ((x v y) v z)= (x v y) v z. given clause #140: (wt=13) 169 [para_from,111.1.1,75.1.1.2] ((x v y) v z) v y= (x v y) v z. given clause #141: (wt=19) 127 [para_into,19.1.1.2.1,10.1.1] ((x^y) v (z^y))^ (y v u)= (x^y) v (z^y). given clause #142: (wt=13) 173 [para_from,111.1.1,57.1.1.1] x v ((y v x) v z)= (y v x) v z. given clause #143: (wt=13) 299 [para_into,77.1.1.1,77.1.1,demod,78] (x^y)^ (z v (u v y))=x^y. given clause #144: (wt=13) 301 [para_into,77.1.1.1,33.1.1,demod,34] x^ (y v ((z v x)^ (u v x)))=x. given clause #145: (wt=13) 309 [para_into,77.1.1.2,85.1.1] (x^ (y^z))^y=x^ (y^z). given clause #146: (wt=21) 133 [para_from,19.1.1,10.1.1.1.2] ((x^ ((y v z) v u)) v y) v ((y v z) v u)= (y v z) v u. given clause #147: (wt=11) 3862 [para_into,309.1.1.1.2,4.1.1,demod,312] x^ (y^z)=x^ (z^y). 3942 back subsumes 1546. 3942 back subsumes 1544. given clause #148: (wt=11) 3942 [para_into,3862.1.1.2,1356.1.1,demod,1357] x^ (y v z)=x^ (z v y). 3993 back subsumes 3523. 3995 back subsumes 3515. 3996 back subsumes 3555. 3997 back subsumes 3144. 3998 back subsumes 3299. 4000 back subsumes 3137. given clause #149: (wt=11) 3953 [para_into,3862.1.1,4.1.1] (x^y)^z=z^ (y^x). given clause #150: (wt=11) 3955 [copy,3953,flip.1] x^ (y^z)= (z^y)^x. given clause #151: (wt=21) 137 [para_from,19.1.1,10.1.1.1.1] (x v (y^ ((x v z) v u))) v ((x v z) v u)= (x v z) v u. given clause #152: (wt=11) 4011 [para_into,3942.1.1,4.1.1] (x v y)^z=z^ (y v x). given clause #153: (wt=11) 4012 [copy,4011,flip.1] x^ (y v z)= (z v y)^x. 4236 back subsumes 1545. 4236 back subsumes 1539. given clause #154: (wt=11) 4103 [para_into,3955.1.1,4.1.1] (x^y)^z= (y^x)^z. given clause #155: (wt=11) 4236 [para_into,4012.1.1,4.1.1] (x v y)^z= (y v x)^z. 4300 back subsumes 3522. 4302 back subsumes 3514. 4303 back subsumes 3552. 4304 back subsumes 3143. 4305 back subsumes 3296. 4307 back subsumes 3132. given clause #156: (wt=19) 143 [para_into,23.1.1.1.2,10.1.1] (x v y)^ ((z^y) v (u^y))= (z^y) v (u^y). given clause #157: (wt=13) 311 [para_into,77.1.1.2,75.1.1] (x^ (y^z))^z=x^ (y^z). given clause #158: (wt=13) 319 [para_from,77.1.1,39.1.1.1.2] (x v (y^z)) v (x v z)=x v z. given clause #159: (wt=13) 333 [para_into,87.1.1.1,27.1.1,demod,28] x^ (y v ((z v x)^ (x v u)))=x. given clause #160: (wt=13) 335 [para_into,87.1.1.1,25.1.1,demod,26] x^ (y v ((x v z)^ (u v x)))=x. given clause #161: (wt=15) 145 [para_into,25.1.1.1.2,85.1.1] (((x^y) v z)^x)^ (x^y)=x^y. given clause #162: (wt=13) 337 [para_into,87.1.1.2,85.1.1] ((x^y)^z)^x= (x^y)^z. given clause #163: (wt=13) 339 [para_into,87.1.1.2,75.1.1] ((x^y)^z)^y= (x^y)^z. given clause #164: (wt=13) 347 [para_from,87.1.1,39.1.1.1.2] (x v (y^z)) v (x v y)=x v y. given clause #165: (wt=13) 355 [para_from,87.1.1,77.1.1.1,demod,88] (x^y)^ (z v (u v x))=x^y. given clause #166: (wt=15) 147 [para_into,25.1.1.1.2,75.1.1] (((x^y) v z)^y)^ (x^y)=x^y. given clause #167: (wt=13) 390 [para_into,123.1.1.1,27.1.1,demod,28] x^ (((y v x)^ (x v z)) v u)=x. given clause #168: (wt=13) 392 [para_into,123.1.1.1,25.1.1,demod,26] x^ (((x v y)^ (z v x)) v u)=x. given clause #169: (wt=13) 396 [para_into,123.1.1.1,5.1.1,demod,6] x^ (((y v x)^ (z v x)) v u)=x. given clause #170: (wt=13) 406 [para_from,123.1.1,41.1.1.1.2] (x v (y^z)) v (y v x)=y v x. given clause #171: (wt=17) 153 [para_from,25.1.1,85.1.1.2] ((x v y)^ (z v x)) v x= (x v y)^ (z v x). given clause #172: (wt=13) 414 [para_from,123.1.1,77.1.1.1,demod,124] (x^y)^ (z v (x v u))=x^y. given clause #173: (wt=13) 422 [para_into,125.1.1.1,125.1.1,demod,126] (x^y)^ ((y v z) v u)=x^y. given clause #174: (wt=13) 424 [para_into,125.1.1.1,123.1.1,demod,124] (x^y)^ ((x v z) v u)=x^y. given clause #175: (wt=13) 426 [para_into,125.1.1.1,87.1.1,demod,88] (x^y)^ ((z v x) v u)=x^y. given clause #176: (wt=17) 155 [para_from,25.1.1,73.1.1.1] x v ((x v y)^ (z v x))= (x v y)^ (z v x). given clause #177: (wt=13) 428 [para_into,125.1.1.1,77.1.1,demod,78] (x^y)^ ((z v y) v u)=x^y. given clause #178: (wt=13) 438 [para_from,125.1.1,41.1.1.1.2] (x v (y^z)) v (z v x)=z v x. given clause #179: (wt=13) 446 [para_from,125.1.1,77.1.1.1,demod,126] (x^y)^ (z v (y v u))=x^y. given clause #180: (wt=13) 482 [para_into,139.1.1.1,85.1.1] x^ ((x^y)^z)= (x^y)^z. given clause #181: (wt=15) 157 [para_into,27.1.1.1.1,85.1.1] (x^ ((x^y) v z))^ (x^y)=x^y. given clause #182: (wt=13) 484 [para_into,139.1.1.1,75.1.1] x^ ((y^x)^z)= (y^x)^z. given clause #183: (wt=13) 490 [para_into,139.1.1.2,139.1.1,demod,140] (x v (y v z))^ (z^u)=z^u. given clause #184: (wt=13) 496 [para_into,139.1.1.2,27.1.1,demod,28] (x v ((y v z)^ (z v u)))^z=z. given clause #185: (wt=13) 498 [para_into,139.1.1.2,25.1.1,demod,26] (x v ((y v z)^ (u v y)))^y=y. given clause #186: (wt=15) 159 [para_into,27.1.1.1.1,75.1.1] (x^ ((y^x) v z))^ (y^x)=y^x. given clause #187: (wt=13) 502 [para_into,139.1.1.2,5.1.1,demod,6] (x v ((y v z)^ (u v z)))^z=z. given clause #188: (wt=13) 504 [para_into,141.1.1.1,85.1.1] x^ (y^ (x^z))=y^ (x^z). given clause #189: (wt=13) 506 [para_into,141.1.1.1,75.1.1] x^ (y^ (z^x))=y^ (z^x). given clause #190: (wt=13) 510 [para_into,141.1.1.2,125.1.1,demod,126] (x v (y v z))^ (u^y)=u^y. given clause #191: (wt=17) 163 [para_from,27.1.1,85.1.1.2] ((x v y)^ (y v z)) v y= (x v y)^ (y v z). given clause #192: (wt=13) 512 [para_into,141.1.1.2,123.1.1,demod,124] (x v (y v z))^ (y^u)=y^u. given clause #193: (wt=13) 514 [para_into,141.1.1.2,77.1.1,demod,78] (x v (y v z))^ (u^z)=u^z. given clause #194: (wt=13) 518 [para_from,149.1.1,139.1.1.2,demod,150] (x v ((y v z)^ (y v u)))^y=y. given clause #195: (wt=13) 520 [para_from,149.1.1,123.1.1.1,demod,150] x^ (((x v y)^ (x v z)) v u)=x. given clause #196: (wt=17) 165 [para_from,27.1.1,73.1.1.1] x v ((y v x)^ (x v z))= (y v x)^ (x v z). given clause #197: (wt=13) 522 [para_from,149.1.1,87.1.1.1,demod,150] x^ (y v ((x v z)^ (x v u)))=x. given clause #198: (wt=13) 546 [para_into,49.1.1.1.1,87.1.1] ((x^y) v z) v (z v x)=z v x. given clause #199: (wt=13) 548 [para_into,49.1.1.1.1,77.1.1] ((x^y) v z) v (z v y)=z v y. given clause #200: (wt=13) 576 [para_into,185.1.1.2,185.1.1,demod,186] ((x v y) v z)^ (x^u)=x^u. given clause #201: (wt=21) 171 [para_from,111.1.1,10.1.1.1.2] ((x^ ((y v z) v u)) v z) v ((y v z) v u)= (y v z) v u. given clause #202: (wt=13) 580 [para_into,185.1.1.2,149.1.1,demod,150] (((x v y)^ (x v z)) v u)^x=x. given clause #203: (wt=13) 582 [para_into,185.1.1.2,141.1.1,demod,142] ((x v y) v z)^ (u^y)=u^y. given clause #204: (wt=13) 584 [para_into,185.1.1.2,139.1.1,demod,140] ((x v y) v z)^ (y^u)=y^u. given clause #205: (wt=13) 590 [para_into,185.1.1.2,27.1.1,demod,28] (((x v y)^ (y v z)) v u)^y=y. given clause #206: (wt=21) 175 [para_from,111.1.1,10.1.1.1.1] (x v (y^ ((z v x) v u))) v ((z v x) v u)= (z v x) v u. given clause #207: (wt=13) 592 [para_into,185.1.1.2,25.1.1,demod,26] (((x v y)^ (z v x)) v u)^x=x. given clause #208: (wt=13) 596 [para_into,185.1.1.2,5.1.1,demod,6] (((x v y)^ (z v y)) v u)^y=y. given clause #209: (wt=13) 602 [para_into,187.1.1.2,125.1.1,demod,126] ((x v y) v z)^ (u^x)=u^x. given clause #210: (wt=13) 632 [para_into,51.1.1.1.1,125.1.1] ((x^y) v z) v (y v z)=y v z. given clause #211: (wt=15) 177 [para_into,33.1.1.2.1,85.1.1] (x^y)^ (x^ (z v (x^y)))=x^y. given clause #212: (wt=13) 634 [para_into,51.1.1.1.1,123.1.1] ((x^y) v z) v (x v z)=x v z. given clause #213: (wt=13) 704 [para_from,297.1.1,187.1.1.2,demod,298] ((x v ((y v z) v u)) v v)^z=z. given clause #214: (wt=13) 710 [para_from,297.1.1,141.1.1.2,demod,298] (x v (y v ((z v u) v v)))^u=u. given clause #215: (wt=13) 712 [para_from,297.1.1,125.1.1.1,demod,298] x^ ((y v ((z v x) v u)) v v)=x. given clause #216: (wt=15) 179 [para_into,33.1.1.2.1,75.1.1] (x^y)^ (y^ (z v (x^y)))=x^y. given clause #217: (wt=13) 714 [para_from,297.1.1,77.1.1.1,demod,298] x^ (y v (z v ((u v x) v v)))=x. given clause #218: (wt=13) 722 [para_from,303.1.1,187.1.1.2,demod,304] ((x v ((y v z) v u)) v v)^y=y. given clause #219: (wt=13) 728 [para_from,303.1.1,141.1.1.2,demod,304] (x v (y v ((z v u) v v)))^z=z. given clause #220: (wt=13) 730 [para_from,303.1.1,125.1.1.1,demod,304] x^ ((y v ((x v z) v u)) v v)=x. given clause #221: (wt=15) 181 [para_into,33.1.1.2.2,85.1.1] (x^y)^ ((z v (x^y))^x)=x^y. given clause #222: (wt=13) 732 [para_from,303.1.1,77.1.1.1,demod,304] x^ (y v (z v ((x v u) v v)))=x. given clause #223: (wt=13) 776 [para_from,305.1.1,187.1.1.2,demod,306] ((x v (y v (z v u))) v v)^u=u. given clause #224: (wt=13) 784 [para_from,305.1.1,141.1.1.2,demod,306] (x v (y v (z v (u v v))))^v=v. given clause #225: (wt=13) 786 [para_from,305.1.1,125.1.1.1,demod,306] x^ ((y v (z v (u v x))) v v)=x. given clause #226: (wt=15) 183 [para_into,33.1.1.2.2,75.1.1] (x^y)^ ((z v (x^y))^y)=x^y. given clause #227: (wt=13) 788 [para_from,305.1.1,77.1.1.1,demod,306] x^ (y v (z v (u v (v v x))))=x. given clause #228: (wt=13) 798 [para_from,307.1.1,187.1.1.2,demod,308] ((x v (y v (z v u))) v v)^z=z. given clause #229: (wt=13) 806 [para_from,307.1.1,141.1.1.2,demod,308] (x v (y v (z v (u v v))))^u=u. given clause #230: (wt=13) 808 [para_from,307.1.1,125.1.1.1,demod,308] x^ ((y v (z v (x v u))) v v)=x. given clause #231: (wt=19) 189 [para_into,129.1.1.1.1,10.1.1] (x v y)^ ((z^x) v (u^x))= (z^x) v (u^x). given clause #232: (wt=13) 810 [para_from,307.1.1,77.1.1.1,demod,308] x^ (y v (z v (u v (x v v))))=x. given clause #233: (wt=13) 814 [para_into,321.1.1.1,321.1.1,demod,322] (x v y) v (z^ (u^y))=x v y. given clause #234: (wt=13) 816 [para_into,321.1.1.1,259.1.1,demod,260] x v (y^ ((z^x) v (x^u)))=x. given clause #235: (wt=13) 818 [para_into,321.1.1.1,205.1.1,demod,206] x v (y^ ((x^z) v (u^x)))=x. given clause #236: (wt=21) 191 [para_into,45.1.1.1.2,111.1.1] ((((x v y) v z)^u) v y) v ((x v y) v z)= (x v y) v z. given clause #237: (wt=13) 824 [para_into,321.1.1.1,59.1.1,demod,60] x v (y^ ((z^x) v (u^x)))=x. given clause #238: (wt=13) 876 [para_into,820.1.1.2.2,187.1.1] (x v y) v (z^ (u^x))=x v y. given clause #239: (wt=13) 878 [para_into,820.1.1.2.2,185.1.1] (x v y) v (z^ (x^u))=x v y. given clause #240: (wt=13) 884 [para_into,820.1.1.2.2,139.1.1] (x v y) v (z^ (y^u))=x v y. given clause #241: (wt=15) 195 [para_into,45.1.1.1.2,21.1.1] (((x v y)^z) v x) v (x v y)=x v y. given clause #242: (wt=13) 900 [para_from,820.1.1,51.1.1.2,demod,821,821] ((x^y) v (z^ (y^u))) v y=y. given clause #243: (wt=13) 914 [para_from,820.1.1,41.1.1.2,demod,821,821] ((x^ (y^z)) v (u^y)) v y=y. given clause #244: (wt=13) 988 [para_from,822.1.1,51.1.1.2,demod,823,823] ((x^y) v (z^ (u^y))) v y=y. given clause #245: (wt=13) 1000 [para_from,822.1.1,41.1.1.2,demod,823,823] ((x^ (y^z)) v (u^z)) v z=z. given clause #246: (wt=21) 197 [para_into,45.1.1.1.2,19.1.1] ((((x v y) v z)^u) v x) v ((x v y) v z)= (x v y) v z. given clause #247: (wt=13) 1024 [para_into,894.1.1.2.1,187.1.1] (x v y) v ((z^x)^u)=x v y. given clause #248: (wt=13) 1026 [para_into,894.1.1.2.1,185.1.1] (x v y) v ((x^z)^u)=x v y. given clause #249: (wt=13) 1032 [para_into,894.1.1.2.1,141.1.1] (x v y) v ((z^y)^u)=x v y. given clause #250: (wt=13) 1034 [para_into,894.1.1.2.1,139.1.1] (x v y) v ((y^z)^u)=x v y. given clause #251: (wt=15) 199 [para_into,45.1.1.1.2,17.1.1] (((x v y)^z) v y) v (x v y)=x v y. given clause #252: (wt=13) 1048 [para_from,894.1.1,51.1.1.2,demod,895,895] ((x^y) v ((y^z)^u)) v y=y. given clause #253: (wt=13) 1062 [para_from,894.1.1,41.1.1.2,demod,895,895] (((x^y)^z) v (u^x)) v x=x. given clause #254: (wt=13) 1088 [para_into,896.1.1.1.2,187.1.1] (x^ (y^z)) v (z v u)=z v u. given clause #255: (wt=13) 1090 [para_into,896.1.1.1.2,185.1.1] (x^ (y^z)) v (y v u)=y v u. given clause #256: (wt=21) 201 [para_into,45.1.1.1.2,15.1.1] (((x v (y v z))^u) v z) v (x v (y v z))=x v (y v z). given clause #257: (wt=13) 1096 [para_into,896.1.1.1.2,141.1.1] (x^ (y^z)) v (u v z)=u v z. given clause #258: (wt=13) 1098 [para_into,896.1.1.1.2,139.1.1] (x^ (y^z)) v (u v y)=u v y. given clause #259: (wt=13) 1130 [para_from,982.1.1,51.1.1.2,demod,983,983] ((x^y) v ((z^y)^u)) v y=y. given clause #260: (wt=13) 1142 [para_from,982.1.1,41.1.1.2,demod,983,983] (((x^y)^z) v (u^y)) v y=y. given clause #261: (wt=21) 203 [para_into,45.1.1.1.2,12.1.1] (((x v (y v z))^u) v y) v (x v (y v z))=x v (y v z). given clause #262: (wt=13) 1174 [para_from,63.1.1,896.1.1.1.2] (x^ ((y^z) v (u^z))) v z=z. given clause #263: (wt=13) 1176 [para_from,63.1.1,894.1.1.2.1] x v (((y^x) v (z^x))^u)=x. given clause #264: (wt=13) 1196 [para_into,1044.1.1.1.1,187.1.1] ((x^y)^z) v (y v u)=y v u. given clause #265: (wt=13) 1198 [para_into,1044.1.1.1.1,185.1.1] ((x^y)^z) v (x v u)=x v u. given clause #266: (wt=19) 207 [para_from,45.1.1,23.1.1.1.2] (x v y)^ ((y^z) v (u^y))= (y^z) v (u^y). given clause #267: (wt=13) 1204 [para_into,1044.1.1.1.1,141.1.1] ((x^y)^z) v (u v y)=u v y. given clause #268: (wt=13) 1206 [para_into,1044.1.1.1.1,139.1.1] ((x^y)^z) v (u v x)=u v x. given clause #269: (wt=13) 1212 [para_into,1044.1.1.1.1,63.1.1] (((x^y) v (z^y))^u) v y=y. given clause #270: (wt=13) 1268 [para_into,327.1.1.2,259.1.1,demod,260] (x^ ((y^z) v (z^u))) v z=z. given clause #271: (wt=19) 209 [para_from,45.1.1,12.1.1.2.2] ((x^y) v (z^x))^ (u v x)= (x^y) v (z^x). given clause #272: (wt=13) 1270 [para_into,327.1.1.2,205.1.1,demod,206] (x^ ((y^z) v (u^y))) v y=y. given clause #273: (wt=13) 1292 [para_into,349.1.1.1,259.1.1,demod,260] x v (((y^x) v (x^z))^u)=x. given clause #274: (wt=13) 1294 [para_into,349.1.1.1,205.1.1,demod,206] x v (((x^y) v (z^x))^u)=x. given clause #275: (wt=13) 1328 [para_into,357.1.1.2,259.1.1,demod,260] (((x^y) v (y^z))^u) v y=y. given clause #276: (wt=17) 211 [para_from,45.1.1,35.1.1.1] x^ ((x^y) v (z^x))= (x^y) v (z^x). given clause #277: (wt=13) 1330 [para_into,357.1.1.2,205.1.1,demod,206] (((x^y) v (z^x))^u) v x=x. given clause #278: (wt=13) 1338 [para_from,365.1.1,27.1.1.1.2,demod,1335] (x v (y v z))^ (z v y)=y v z. given clause #279: (wt=13) 1340 [para_from,365.1.1,149.1.1.1.2,demod,1335] ((x v y) v z)^ (y v x)=x v y. given clause #280: (wt=13) 1348 [para_from,365.1.1,12.1.1.2.2] (x v y)^ (z v (y v x))=x v y. given clause #281: (wt=17) 213 [para_from,45.1.1,21.1.1.2] ((x^y) v (z^x))^x= (x^y) v (z^x). given clause #282: (wt=13) 1354 [para_from,365.1.1,149.1.1.1.1,demod,1345] (x v y)^ ((y v x) v z)=y v x. given clause #283: (wt=13) 1369 [para_from,71.1.1,27.1.1.1.2] ((x v y)^ (z v (y v u)))^y=y. given clause #284: (wt=13) 1371 [para_from,71.1.1,161.1.1.2.2] x^ ((y v x)^ (z v (x v u)))=x. given clause #285: (wt=13) 1373 [para_from,71.1.1,149.1.1.1.2] ((x v y)^ (z v (x v u)))^x=x. given clause #286: (wt=19) 215 [para_from,45.1.1,129.1.1.1.1] (x v y)^ ((x^z) v (u^x))= (x^z) v (u^x). given clause #287: (wt=13) 1375 [para_from,71.1.1,303.1.1.2.2.1] x^ (y v ((z v (x v u)) v v))=x. given clause #288: (wt=13) 1377 [para_from,71.1.1,149.1.1.1.1] ((x v (y v z))^ (y v u))^y=y. given clause #289: (wt=13) 1379 [para_from,71.1.1,151.1.1.2.1] x^ ((y v (x v z))^ (u v x))=x. given clause #290: (wt=13) 1381 [para_from,71.1.1,25.1.1.1.1] ((x v (y v z))^ (u v y))^y=y. given clause #291: (wt=19) 217 [para_from,45.1.1,19.1.1.2.1] ((x^y) v (z^x))^ (x v u)= (x^y) v (z^x). given clause #292: (wt=13) 1401 [para_into,384.1.1.2,71.1.1] x^ (y v (((z v x) v u) v v))=x. given clause #293: (wt=13) 1409 [para_from,384.1.1,187.1.1.2,demod,385] ((((x v y) v z) v u) v v)^y=y. given clause #294: (wt=13) 1419 [para_from,384.1.1,141.1.1.2,demod,385] (x v (((y v z) v u) v v))^z=z. given clause #295: (wt=13) 1425 [para_from,384.1.1,125.1.1.1,demod,385] x^ ((((y v x) v z) v u) v v)=x. given clause #296: (wt=15) 219 [para_into,39.1.1.1.2.2,45.1.1,demod,46,46] (((x^y) v (z^x)) v (u^x)) v x=x. given clause #297: (wt=13) 1433 [para_into,386.1.1.2.1.1,71.1.1] x^ (((y v (x v z)) v u) v v)=x. given clause #298: (wt=13) 1435 [para_into,386.1.1.2,71.1.1] x^ (y v (((x v z) v u) v v))=x. given clause #299: (wt=13) 1443 [para_from,386.1.1,187.1.1.2,demod,387] ((((x v y) v z) v u) v v)^x=x. given clause #300: (wt=13) 1453 [para_from,386.1.1,141.1.1.2,demod,387] (x v (((y v z) v u) v v))^y=y. given clause #301: (wt=21) 221 [para_into,39.1.1.1.2.2,39.1.1,demod,40,40] ((x v (y^ (x v z))) v (u^ (x v z))) v (x v z)=x v z. given clause #302: (wt=13) 1459 [para_from,386.1.1,125.1.1.1,demod,387] x^ ((((x v y) v z) v u) v v)=x. given clause #303: (wt=13) 1479 [para_into,388.1.1.2,71.1.1] x^ (y v ((z v (u v x)) v v))=x. given clause #304: (wt=13) 1487 [para_from,388.1.1,187.1.1.2,demod,389] (((x v (y v z)) v u) v v)^z=z. given clause #305: (wt=13) 1497 [para_from,388.1.1,141.1.1.2,demod,389] (x v ((y v (z v u)) v v))^u=u. given clause #306: (wt=15) 223 [para_into,39.1.1.1.2.2,10.1.1,demod,11,11] (((x^y) v (z^y)) v (u^y)) v y=y. given clause #307: (wt=13) 1503 [para_from,388.1.1,125.1.1.1,demod,389] x^ (((y v (z v x)) v u) v v)=x. given clause #308: (wt=13) 1517 [para_from,394.1.1,187.1.1.2,demod,395] (((x v (y v z)) v u) v v)^y=y. given clause #309: (wt=13) 1527 [para_from,394.1.1,141.1.1.2,demod,395] (x v ((y v (z v u)) v v))^z=z. given clause #310: (wt=13) 1599 [para_into,408.1.1.1,365.1.1,demod,366] (x v y) v ((y v x)^z)=x v y. given clause #311: (wt=15) 225 [para_into,39.1.1.1.2.2,9.1.1] (x v (y^ (z v x))) v (x v z)=x v z. given clause #312: (wt=13) 1601 [para_into,408.1.1.1,193.1.1,demod,194] x v (((x^y) v (x^z))^u)=x. given clause #313: (wt=13) 1655 [para_into,416.1.1.2,365.1.1,demod,366] ((x v y)^z) v (y v x)=y v x. given clause #314: (wt=13) 1657 [para_into,416.1.1.2,193.1.1,demod,194] (((x^y) v (x^z))^u) v x=x. given clause #315: (wt=13) 1667 [para_into,440.1.1.1,365.1.1,demod,366] (x v y) v (z^ (y v x))=x v y. given clause #316: (wt=15) 227 [para_into,39.1.1.1.2,91.1.1] (x v ((x v y)^z)) v (x v y)=x v y. given clause #317: (wt=13) 1669 [para_into,440.1.1.1,193.1.1,demod,194] x v (y^ ((x^z) v (x^u)))=x. given clause #318: (wt=13) 1739 [para_into,448.1.1.2,365.1.1,demod,366] (x^ (y v z)) v (z v y)=z v y. given clause #319: (wt=13) 1741 [para_into,448.1.1.2,193.1.1,demod,194] (x^ ((y^z) v (y^u))) v y=y. given clause #320: (wt=13) 1767 [para_from,97.1.1,161.1.1.2.1] x^ ((y v (x v z))^ (x v u))=x. given clause #321: (wt=15) 229 [para_into,39.1.1.1.2,15.1.1] (x v y) v (x v (z v y))=x v (z v y). given clause #322: (wt=13) 1773 [para_from,97.1.1,151.1.1.2.2] x^ ((x v y)^ (z v (x v u)))=x. given clause #323: (wt=13) 1853 [para_into,99.1.1.1.1.2,111.1.1,demod,112,112] ((x v y)^ ((z v y) v u))^y=y. given clause #324: (wt=13) 1855 [para_into,99.1.1.1.1.2,19.1.1,demod,20,20] ((x v y)^ ((y v z) v u))^y=y. given clause #325: (wt=13) 1857 [para_into,99.1.1.1.1.2,15.1.1,demod,16,16] ((x v y)^ (z v (u v y)))^y=y. given clause #326: (wt=15) 231 [para_into,39.1.1.1.2,12.1.1] (x v y) v (x v (y v z))=x v (y v z). given clause #327: (wt=11) 12971 [para_into,231.1.1.2,634.1.1,demod,12428,635] x v ((x^y) v z)=x v z. ----> UNIT CONFLICT at 168.88 sec ----> 13311 [binary,13309.1,14.1] $Ans(assoc_join). Length of proof is 30. Level of proof is 9. ---------------- PROOF ---------------- 2 [] x^x=x. 4 [] x^y=y^x. 5 [] ((x v y)^ (z v y))^y=y. 7 [] x v x=x. 9 [] x v y=y v x. 10 [] ((x^y) v (z^y)) v y=y. 12 [] x^ (y v (x v z))=x. 14 [] (A v B) v C!=A v (B v C)|$Ans(assoc_join). 15 [para_into,12.1.1.2.2,9.1.1] x^ (y v (z v x))=x. 17 [para_into,12.1.1.2.2,7.1.1] x^ (y v x)=x. 19 [para_into,12.1.1.2,9.1.1] x^ ((x v y) v z)=x. 21 [para_into,12.1.1.2,7.1.1] x^ (x v y)=x. 31 [para_into,5.1.1.1,2.1.1] (x v y)^y=y. 39 [para_into,10.1.1.1.1,21.1.1] (x v (y^ (x v z))) v (x v z)=x v z. 51 [para_into,10.1.1.1.2,17.1.1] ((x^ (y v z)) v z) v (y v z)=y v z. 57 [para_into,10.1.1.1,7.1.1] (x^y) v y=y. 71 [para_into,57.1.1.1,12.1.1] x v (y v (x v z))=y v (x v z). 73 [para_into,57.1.1.1,4.1.1] (x^y) v x=x. 75 [para_into,57.1.1,9.1.1] x v (y^x)=x. 96,95 [para_into,75.1.1.2,17.1.1] (x v y) v y=x v y. 111 [para_into,15.1.1.2,9.1.1] x^ ((y v x) v z)=x. 120,119 [para_from,15.1.1,57.1.1.1] x v (y v (z v x))=y v (z v x). 123 [para_into,19.1.1.2.1,73.1.1] (x^y)^ (x v z)=x^y. 129 [para_into,19.1.1,4.1.1] ((x v y) v z)^x=x. 167 [para_into,111.1.1,4.1.1] ((x v y) v z)^y=y. 229 [para_into,39.1.1.1.2,15.1.1] (x v y) v (x v (z v y))=x v (z v y). 232,231 [para_into,39.1.1.1.2,12.1.1] (x v y) v (x v (y v z))=x v (y v z). 635,634 [para_into,51.1.1.1.1,123.1.1] ((x^y) v z) v (x v z)=x v z. 1368 [para_into,71.1.1.2.2,9.1.1,demod,120] x v (y v z)=x v (z v y). 2986 [para_into,1368.1.1,9.1.1] (x v y) v z=z v (y v x). 2988 [copy,2986,flip.1] x v (y v z)= (z v y) v x. 12428,12427 [para_into,229.1.1,2988.1.1] ((x v y) v z) v (z v y)=z v (x v y). 12971 [para_into,231.1.1.2,634.1.1,demod,12428,635] x v ((x^y) v z)=x v z. 13003 [para_from,231.1.1,229.1.1.2,demod,232] ((x v y) v (y v z)) v (x v (y v z))=x v (y v z). 13256,13255 [para_into,12971.1.1.2.1,167.1.1] ((x v y) v z) v (y v u)= ((x v y) v z) v u. 13266,13265 [para_into,12971.1.1.2.1,129.1.1] ((x v y) v z) v (x v u)= ((x v y) v z) v u. 13274,13273 [para_into,12971.1.1.2.1,31.1.1] (x v y) v (y v z)= (x v y) v z. 13309 [back_demod,13003,demod,13274,13266,13256,96] (x v y) v z=x v (y v z). 13311 [binary,13309.1,14.1] $Ans(assoc_join). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 327 clauses generated 133794 para_from generated 60064 para_into generated 73730 demod & eval rewrites 178746 clauses wt,lit,sk delete 20284 tautologies deleted 0 clauses forward subsumed 107359 (subsumed by sos) 636 unit deletions 0 factor simplifications 0 clauses kept 6783 new demodulators 6527 empty clauses 1 clauses back demodulated 371 clauses back subsumed 20 usable size 319 sos size 6073 demodulators size 6225 passive size 0 hot size 0 Kbytes malloced 8685 ----------- times (seconds) ----------- user CPU time 168.90 (0 hr, 2 min, 48 sec) system CPU time 38.70 (0 hr, 0 min, 38 sec) wall-clock time 213 (0 hr, 3 min, 33 sec) input time 0.04 clausify time 0.00 process input 0.02 para_into time 14.40 para_from time 13.51 pre_process time 117.91 renumber time 7.01 demod time 69.67 order equalities 3.73 unit deleletion 0.00 factor simplify 0.00 weigh cl time 5.51 sort lits time 0.00 forward subsume 9.57 delete cl time 6.79 keep cl time 6.23 print_cl time 0.01 conflict time 0.62 new demod time 3.57 post_process time 17.95 back demod time 12.88 back subsume 4.67 factor time 0.00 unindex time 3.82 The job finished Tue Feb 14 09:25:53 1995