----- Otter 3.0.6, April 2000 ----- The process was started by ??? on ???, Thu Sep 20 15:40:14 2001 The command was "otter". set(auto). dependent: set(auto1). dependent: set(process_input). dependent: clear(print_kept). dependent: clear(print_new_demod). dependent: clear(print_back_demod). dependent: clear(print_back_sub). dependent: set(control_memory). dependent: assign(max_mem, 12000). dependent: assign(pick_given_ratio, 4). dependent: assign(stats_level, 1). dependent: assign(max_seconds, 10800). set(ur_res). assign(max_distinct_vars,1). list(usable). 0 [] x=x. 0 [] m(1,x)=x. 0 [] m(x,1)=x. 0 [] m(x,m(y,z))=m(m(x,y),z). 0 [] m(x,y)=m(y,x). 0 [] m(x,y)!=m(x,z)|y=z. 0 [] -d(x,y)|m(x,f(x,y))=y. 0 [] m(x,z)!=y|d(x,y). 0 [] -d(2,m(x,y))|d(2,x)|d(2,y). 0 [] m(a,a)=m(2,m(b,b)). 0 [] -d(x,a)| -d(x,b)|x=1. 0 [] 2!=1. end_of_list. set(build_proof_object_2). dependent: set(build_proof_object). dependent: set(order_history). SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=3. This ia a non-Horn set with equality. The strategy will be Knuth-Bendix, ordered hyper_res, factoring, and unit deletion, with positive clauses in sos and nonpositive clauses in usable. dependent: 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(lrpo). dependent: set(hyper_res). dependent: set(unit_deletion). dependent: set(factor). ------------> process usable: ** KEPT (pick-wt=10): 1 [] m(x,y)!=m(x,z)|y=z. ** KEPT (pick-wt=10): 2 [] -d(x,y)|m(x,f(x,y))=y. ** KEPT (pick-wt=8): 3 [] m(x,y)!=z|d(x,z). ** KEPT (pick-wt=11): 4 [] -d(2,m(x,y))|d(2,x)|d(2,y). ** KEPT (pick-wt=9): 5 [] -d(x,a)| -d(x,b)|x=1. ** KEPT (pick-wt=3): 6 [] 2!=1. ------------> process sos: ** KEPT (pick-wt=3): 8 [] x=x. ** KEPT (pick-wt=5): 9 [] m(1,x)=x. ---> New Demodulator: 10 [new_demod,9] m(1,x)=x. ** KEPT (pick-wt=5): 11 [] m(x,1)=x. ---> New Demodulator: 12 [new_demod,11] m(x,1)=x. ** KEPT (pick-wt=11): 14 [copy,13,flip.1] m(m(x,y),z)=m(x,m(y,z)). ---> New Demodulator: 15 [new_demod,14] m(m(x,y),z)=m(x,m(y,z)). ** KEPT (pick-wt=7): 16 [] m(x,y)=m(y,x). ** KEPT (pick-wt=9): 18 [copy,17,flip.1] m(2,m(b,b))=m(a,a). ---> New Demodulator: 19 [new_demod,18] m(2,m(b,b))=m(a,a). Following clause subsumed by 8 during input processing: 0 [copy,8,flip.1] x=x. >>>> Starting back demodulation with 10. >>>> Starting back demodulation with 12. >>>> Starting back demodulation with 15. Following clause subsumed by 16 during input processing: 0 [copy,16,flip.1] m(x,y)=m(y,x). >>>> Starting back demodulation with 19. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=3) 8 [] x=x. given clause #2: (wt=5) 9 [] m(1,x)=x. given clause #3: (wt=3) 20 [hyper,3,9.1] d(1,x). given clause #4: (wt=5) 11 [] m(x,1)=x. given clause #5: (wt=3) 24 [hyper,3,11.1] d(x,x). given clause #6: (wt=11) 14 [copy,13,flip.1] m(m(x,y),z)=m(x,m(y,z)). given clause #7: (wt=5) 22 [para_into,9.1.1,2.2.1,unit_del,20,flip.1] f(1,x)=x. given clause #8: (wt=7) 16 [] m(x,y)=m(y,x). given clause #9: (wt=7) 25 [hyper,2,24.1] m(x,f(x,x))=x. given clause #10: (wt=7) 27 [para_into,25.1.1,16.1.1] m(f(x,x),x)=x. given clause #11: (wt=9) 18 [copy,17,flip.1] m(2,m(b,b))=m(a,a). given clause #12: (wt=5) 29 [hyper,3,27.1] d(f(x,x),x). given clause #13: (wt=5) 30 [hyper,3,18.1] d(2,m(a,a)). given clause #14: (wt=3) 42 [hyper,7,30.1] d(2,a). given clause #15: (wt=3) 48 [ur,5.2,42,6] -d(2,b). given clause #16: (wt=9) 21 [para_into,9.1.1,5.3.1,demod,10,10] 1=x| -d(x,a)| -d(x,b). given clause #17: (wt=5) 50 [ur,7.1,48] -d(2,m(b,b)). given clause #18: (wt=5) 51 [ur,3.1,48] m(2,x)!=b. given clause #19: (wt=3) 62 [para_into,51.1.1,25.1.1,flip.1] b!=2. given clause #20: (wt=5) 63 [para_into,51.1.1,18.1.1] m(a,a)!=b. given clause #21: (wt=10) 32 [para_into,18.1.1.2.1,5.3.1,demod,10,unit_del,24,flip.1] m(a,a)=m(2,b)| -d(b,a). given clause #22: (wt=5) 64 [para_into,51.1.1,16.1.1] m(x,2)!=b. given clause #23: (wt=6) 49 [para_into,42.1.2,5.3.1,unit_del,24] d(2,1)| -d(a,b). given clause #24: (wt=6) 52 [para_into,48.1.2,5.3.1,unit_del,24] -d(2,1)| -d(b,a). given clause #25: (wt=6) 66 [para_into,51.1.1,2.2.1] x!=b| -d(2,x). given clause #26: (wt=15) 33 [para_into,18.1.1.2,5.3.1,demod,12,flip.1] m(a,a)=2| -d(m(b,b),a)| -d(m(b,b),b). given clause #27: (wt=3) 83 [ur,66.1,42,flip.1] b!=a. given clause #28: (wt=6) 94 [para_into,83.1.1,5.3.1,unit_del,24,flip.1] a!=1| -d(b,a). given clause #29: (wt=6) 95 [para_into,94.1.1,5.3.1,unit_del,8,24] -d(b,a)| -d(a,b). given clause #30: (wt=6) 97 [para_into,95.1.2,5.3.1,unit_del,24,factor_simp] -d(b,1)| -d(a,b). given clause #31: (wt=9) 34 [para_into,18.1.1,16.1.1,demod,15] m(b,m(b,2))=m(a,a). given clause #32: (wt=5) 100 [hyper,3,34.1] d(b,m(a,a)). given clause #33: (wt=5) 107 [para_from,34.1.1,4.1.2,unit_del,30,48] d(2,m(b,2)). given clause #34: (wt=5) 118 [para_into,107.1.2,16.1.1] d(2,m(2,b)). given clause #35: (wt=6) 98 [para_into,95.2.2,5.3.1,unit_del,24,factor_simp] -d(b,a)| -d(a,1). given clause #36: (wt=13) 36 [para_from,18.1.1,14.1.1.1,demod,15,15,flip.1] m(2,m(b,m(b,x)))=m(a,m(a,x)). given clause #37: (wt=6) 112 [para_into,100.1.2.1,5.3.1,demod,10,unit_del,24] d(b,a)| -d(a,b). given clause #38: (wt=6) 138 [para_into,112.1.2,5.3.1,unit_del,24,factor_simp] d(b,1)| -d(a,b). given clause #39: (wt=7) 46 [hyper,2,42.1] m(2,f(2,a))=a. given clause #40: (wt=6) 144 [para_into,46.1.1,5.3.1,demod,47,47,unit_del,24,flip.1] a=1| -d(a,b). given clause #41: (wt=8) 38 [para_from,18.1.1,3.1.1] m(a,a)!=x|d(2,x). given clause #42: (wt=6) 147 [para_from,46.1.1,3.1.1] a!=x|d(2,x). given clause #43: (wt=5) 153 [ur,147.1,50,flip.1] m(b,b)!=a. given clause #44: (wt=7) 58 [ur,4.1,48,50] -d(2,m(b,m(b,b))). given clause #45: (wt=7) 59 [ur,3.1,50] m(2,x)!=m(b,b). given clause #46: (wt=12) 39 [para_from,18.1.1,1.1.1] m(a,a)!=m(2,x)|m(b,b)=x. given clause #47: (wt=5) 165 [para_into,59.1.1,25.1.1,flip.1] m(b,b)!=2. given clause #48: (wt=7) 60 [copy,59,flip.1] m(b,b)!=m(2,x). given clause #49: (wt=7) 67 [ur,1.1,62] m(x,b)!=m(x,2). given clause #50: (wt=7) 93 [ur,1.1,83] m(x,b)!=m(x,a). given clause #51: (wt=11) 40 [hyper,2,29.1] m(f(x,x),f(f(x,x),x))=x. given clause #52: (wt=7) 123 [hyper,3,36.1] d(2,m(a,m(a,x))). given clause #53: (wt=7) 137 [para_from,36.1.1,51.1.1] m(a,m(a,x))!=b. given clause #54: (wt=7) 142 [para_into,46.1.1,16.1.1] m(f(2,a),2)=a. given clause #55: (wt=5) 223 [hyper,3,142.1] d(f(2,a),a). given clause #56: (wt=11) 43 [hyper,2,30.1] m(2,f(2,m(a,a)))=m(a,a). given clause #57: (wt=7) 150 [ur,38.1,50,flip.1] m(b,b)!=m(a,a). given clause #58: (wt=7) 157 [ur,147.1,58,flip.1] m(b,m(b,b))!=a. given clause #59: (wt=7) 166 [para_into,59.1.1,16.1.1] m(x,2)!=m(b,b). given clause #60: (wt=7) 170 [copy,166,flip.1] m(b,b)!=m(x,2). given clause #61: (wt=13) 45 [para_into,30.1.2,5.3.1] d(2,1)| -d(m(a,a),a)| -d(m(a,a),b). given clause #62: (wt=7) 171 [ur,39.1,153] m(a,a)!=m(2,a). given clause #63: (wt=7) 186 [ur,39.1,165] m(a,a)!=m(2,2). given clause #64: (wt=7) 195 [para_into,67.1.1,16.1.1] m(b,x)!=m(x,2). given clause #65: (wt=7) 197 [copy,195,flip.1] m(x,2)!=m(b,x). given clause #66: (wt=12) 53 [para_into,21.2.2,5.3.1,unit_del,24] 1=x| -d(x,1)| -d(x,b)| -d(a,b). given clause #67: (wt=7) 201 [para_into,93.1.1,27.1.1,flip.1] m(f(b,b),a)!=b. given clause #68: (wt=7) 202 [para_into,93.1.1,16.1.1] m(b,x)!=m(x,a). given clause #69: (wt=7) 204 [copy,202,flip.1] m(x,a)!=m(b,x). given clause #70: (wt=7) 215 [para_into,123.1.2.2,16.1.1] d(2,m(a,m(x,a))). given clause #71: (wt=12) 54 [para_into,21.3.2,5.3.1,unit_del,24] 1=x| -d(x,a)| -d(x,1)| -d(b,a). given clause #72: (wt=7) 220 [para_into,137.1.1.2,16.1.1] m(a,m(x,a))!=b. given clause #73: (wt=7) 269 [para_into,197.1.1,142.1.1,flip.1] m(b,f(2,a))!=a. given clause #74: (wt=7) 270 [para_into,197.1.1,27.1.1,flip.1] m(b,f(2,2))!=2. given clause #75: (wt=7) 271 [para_into,197.1.1,16.1.1,flip.1] m(b,x)!=m(2,x). given clause #76: (wt=9) 56 [factor,54,2,4,flip.1] b=1| -d(b,a)| -d(b,1). given clause #77: (wt=6) 316 [para_into,56.3.1,5.3.1,unit_del,24,24,factor_simp] b=1| -d(b,a). given clause #78: (wt=7) 279 [para_into,201.1.1,16.1.1] m(a,f(b,b))!=b. given clause #79: (wt=7) 287 [para_into,204.1.1,27.1.1,flip.1] m(b,f(a,a))!=a. given clause #80: (wt=7) 288 [para_into,204.1.1,16.1.1,flip.1] m(b,x)!=m(a,x). given clause #81: (wt=9) 57 [ur,7.1,50,demod,15] -d(2,m(b,m(b,m(b,b)))). given clause #82: (wt=7) 293 [para_into,215.1.2,16.1.1,demod,15] d(2,m(x,m(a,a))). given clause #83: (wt=7) 300 [para_into,220.1.1,16.1.1,demod,15] m(x,m(a,a))!=b. given clause #84: (wt=7) 305 [para_into,269.1.1,16.1.1] m(f(2,a),b)!=a. given clause #85: (wt=7) 309 [para_into,270.1.1,16.1.1] m(f(2,2),b)!=2. given clause #86: (wt=13) 61 [para_into,50.1.2,5.3.1] -d(2,1)| -d(m(b,b),a)| -d(m(b,b),b). given clause #87: (wt=7) 312 [para_into,271.1.1,16.1.1] m(x,b)!=m(2,x). given clause #88: (wt=7) 315 [copy,312,flip.1] m(2,x)!=m(x,b). given clause #89: (wt=7) 325 [para_into,287.1.1,16.1.1] m(f(a,a),b)!=a. given clause #90: (wt=7) 331 [para_into,288.1.1,16.1.1] m(x,b)!=m(a,x). given clause #91: (wt=13) 65 [para_into,51.1.1,5.3.1,flip.1] b!=1| -d(m(2,x),a)| -d(m(2,x),b). given clause #92: (wt=6) 373 [para_into,65.2.1,46.1.1,demod,47,unit_del,24] b!=1| -d(a,b). given clause #93: (wt=7) 334 [copy,331,flip.1] m(a,x)!=m(x,b). given clause #94: (wt=8) 108 [para_from,34.1.1,3.1.1] m(a,a)!=x|d(b,x). given clause #95: (wt=8) 114 [para_into,100.1.2,32.1.1] d(b,m(2,b))| -d(b,a). given clause #96: (wt=9) 68 [ur,1.1,63] m(x,m(a,a))!=m(x,b). given clause #97: (wt=6) 388 [para_into,114.1.2.2,316.1.1,demod,12,factor_simp] d(b,2)| -d(b,a). given clause #98: (wt=8) 168 [para_into,59.1.1,2.2.1] x!=m(b,b)| -d(2,x). given clause #99: (wt=8) 193 [para_into,67.1.1.2,5.3.1,demod,12,unit_del,24,flip.1] m(x,2)!=x| -d(b,a). given clause #100: (wt=8) 199 [para_into,93.1.1.2,5.3.1,demod,12,unit_del,24,flip.1] m(x,a)!=x| -d(b,a). given clause #101: (wt=13) 70 [para_into,63.1.1,5.3.1,flip.1] b!=1| -d(m(a,a),a)| -d(m(a,a),b). given clause #102: (wt=8) 212 [para_into,123.1.2.1,144.1.1,demod,10] d(2,m(a,x))| -d(a,b). given clause #103: (wt=6) 409 [para_into,212.1.2.1,144.1.1,demod,10,factor_simp] d(2,x)| -d(a,b). given clause #104: (wt=3) 410 [ur,409.2,58] -d(a,b). given clause #105: (wt=5) 411 [ur,3.1,410] m(a,x)!=b. given clause #106: (wt=14) 75 [para_from,32.1.1,14.1.1.1,demod,15] m(2,m(b,x))=m(a,m(a,x))| -d(b,a). given clause #107: (wt=5) 412 [para_into,411.1.1,16.1.1] m(x,a)!=b. given clause #108: (wt=6) 414 [para_into,411.1.1,2.2.1] x!=b| -d(a,x). given clause #109: (wt=8) 216 [para_into,123.1.2.2,2.2.1] d(2,m(a,x))| -d(a,x). given clause #110: (wt=8) 225 [para_into,142.1.1.1,5.3.1,demod,10,unit_del,223,flip.1] a=2| -d(f(2,a),b). given clause #111: (wt=11) 76 [para_from,32.1.1,3.1.1] m(2,b)!=x|d(a,x)| -d(b,a). given clause #112: (wt=5) 464 [para_from,225.1.1,171.1.1.2,unit_del,16] -d(f(2,a),b). given clause #113: (wt=7) 467 [ur,3.1,464] m(f(2,a),x)!=b. given clause #114: (wt=5) 469 [para_into,467.1.1,25.1.1] f(2,a)!=b. given clause #115: (wt=7) 470 [para_into,467.1.1,16.1.1] m(x,f(2,a))!=b. given clause #116: (wt=13) 77 [para_from,32.1.1,1.1.1,flip.1] m(a,x)!=m(2,b)|a=x| -d(b,a). given clause #117: (wt=8) 228 [para_from,142.1.1,3.1.1] a!=x|d(f(2,a),x). given clause #118: (wt=8) 303 [para_into,269.1.1.1,5.3.1,demod,10,unit_del,24] f(2,a)!=a| -d(b,a). given clause #119: (wt=8) 308 [para_into,270.1.1.1,5.3.1,demod,10,unit_del,24] f(2,2)!=2| -d(b,a). given clause #120: (wt=8) 310 [para_into,271.1.1.1,5.3.1,demod,10,unit_del,24,flip.1] m(2,x)!=x| -d(b,a). given clause #121: (wt=13) 78 [para_into,64.1.1,5.3.1,flip.1] b!=1| -d(m(x,2),a)| -d(m(x,2),b). given clause #122: (wt=8) 323 [para_into,287.1.1.1,316.1.1,demod,10] f(a,a)!=a| -d(b,a). given clause #123: (wt=8) 328 [para_into,288.1.1.1,316.1.1,demod,10,flip.1] m(a,x)!=x| -d(b,a). given clause #124: (wt=8) 389 [para_into,114.1.2,16.1.1] d(b,m(b,2))| -d(b,a). given clause #125: (wt=8) 402 [para_into,199.1.1,32.1.1,factor_simp] m(2,b)!=a| -d(b,a). given clause #126: (wt=12) 81 [para_into,52.1.2,21.1.1] -d(2,x)| -d(b,a)| -d(x,a)| -d(x,b). given clause #127: (wt=6) 518 [para_into,402.1.1.2,316.1.1,demod,12,factor_simp] a!=2| -d(b,a). given clause #128: (wt=8) 429 [para_into,216.1.2,16.1.1] d(2,m(x,a))| -d(a,x). given clause #129: (wt=8) 468 [para_into,464.1.2,316.1.1] -d(f(2,a),1)| -d(b,a). given clause #130: (wt=8) 472 [para_into,467.1.1,2.2.1] x!=b| -d(f(2,a),x). given clause #131: (wt=18) 85 [para_into,33.1.1,32.1.1] m(2,b)=2| -d(m(b,b),a)| -d(m(b,b),b)| -d(b,a). given clause #132: (wt=8) 519 [para_into,402.1.1,16.1.1] m(b,2)!=a| -d(b,a). given clause #133: (wt=9) 102 [para_into,34.1.1.2,16.1.1] m(b,m(2,b))=m(a,a). given clause #134: (wt=9) 155 [ur,1.1,153] m(x,m(b,b))!=m(x,a). given clause #135: (wt=9) 158 [ur,38.1,58,flip.1] m(b,m(b,b))!=m(a,a). given clause #136: (wt=20) 86 [para_into,33.1.1,5.3.1,unit_del,6] -d(m(b,b),a)| -d(m(b,b),b)| -d(m(a,a),a)| -d(m(a,a),b). given clause #137: (wt=9) 161 [ur,3.1,58] m(2,x)!=m(b,m(b,b)). given clause #138: (wt=7) 558 [para_into,161.1.1,25.1.1,flip.1] m(b,m(b,b))!=2. given clause #139: (wt=9) 162 [copy,161,flip.1] m(b,m(b,b))!=m(2,x). given clause #140: (wt=9) 164 [para_into,59.1.1,36.1.1] m(a,m(a,x))!=m(b,b). given clause #141: (wt=13) 87 [para_into,33.2.1.1,5.3.1,demod,10,unit_del,24,factor_simp] m(a,a)=2| -d(b,a)| -d(m(b,b),b). given clause #142: (wt=8) 572 [para_into,87.3.1.1,316.1.1,demod,10,unit_del,24,factor_simp] m(a,a)=2| -d(b,a). given clause #143: (wt=8) 575 [para_into,572.1.1,32.1.1,factor_simp] m(2,b)=2| -d(b,a). given clause #144: (wt=8) 577 [para_from,572.1.1,204.1.1,flip.1] m(b,a)!=2| -d(b,a). given clause #145: (wt=8) 578 [para_from,572.1.1,334.1.1,flip.1] m(a,b)!=2| -d(b,a). given clause #146: (wt=19) 90 [para_from,33.1.1,14.1.1.1,flip.1] m(a,m(a,x))=m(2,x)| -d(m(b,b),a)| -d(m(b,b),b). given clause #147: (wt=8) 580 [para_from,572.1.1,293.1.2.2] d(2,m(x,2))| -d(b,a). given clause #148: (wt=8) 584 [para_into,575.1.1,16.1.1] m(b,2)=2| -d(b,a). given clause #149: (wt=8) 604 [para_into,580.1.2,16.1.1] d(2,m(2,x))| -d(b,a). given clause #150: (wt=9) 169 [copy,164,flip.1] m(b,b)!=m(a,m(a,x)). given clause #151: (wt=16) 91 [para_from,33.1.1,3.1.1] 2!=x|d(a,x)| -d(m(b,b),a)| -d(m(b,b),b). given clause #152: (wt=9) 187 [ur,1.1,165] m(x,m(b,b))!=m(x,2). given clause #153: (wt=9) 189 [ur,39.1,60] m(a,a)!=m(2,m(2,x)). given clause #154: (wt=9) 190 [copy,189,flip.1] m(2,m(2,x))!=m(a,a). given clause #155: (wt=9) 198 [ur,39.1,93,flip.1] m(2,m(b,a))!=m(a,a). given clause #156: (wt=18) 92 [para_from,33.1.1,1.1.1,flip.1] m(a,x)!=2|a=x| -d(m(b,b),a)| -d(m(b,b),b). given clause #157: (wt=9) 242 [ur,39.1,150,flip.1] m(2,m(a,a))!=m(a,a). given clause #158: (wt=9) 250 [ur,39.1,170] m(a,a)!=m(2,m(x,2)). given clause #159: (wt=9) 251 [copy,250,flip.1] m(2,m(x,2))!=m(a,a). given clause #160: (wt=9) 281 [para_into,202.1.1,34.1.1,demod,15,flip.1] m(b,m(2,a))!=m(a,a). given clause #161: (wt=10) 101 [para_into,34.1.1.1,5.3.1,demod,10,unit_del,24] m(b,2)=m(a,a)| -d(b,a). given clause #162: (wt=9) 327 [ur,39.1,288,flip.1] m(2,m(a,b))!=m(a,a). given clause #163: (wt=9) 330 [para_into,288.1.1,34.1.1,flip.1] m(a,m(b,2))!=m(a,a). given clause #164: (wt=9) 335 [ur,147.1,57,flip.1] m(b,m(b,m(b,b)))!=a. given clause #165: (wt=9) 393 [para_into,68.1.1,16.1.1,demod,15] m(a,m(a,x))!=m(x,b). given clause #166: (wt=10) 104 [para_into,34.1.1.2,5.3.1,demod,12,unit_del,63] -d(m(b,2),a)| -d(m(b,2),b). given clause #167: (wt=8) 731 [para_into,104.1.1.1,316.1.1,demod,10,unit_del,42] -d(m(b,2),b)| -d(b,a). given clause #168: (wt=8) 737 [para_into,731.1.1,101.1.1,factor_simp] -d(m(a,a),b)| -d(b,a). given clause #169: (wt=8) 738 [para_into,731.1.1,16.1.1] -d(m(2,b),b)| -d(b,a). given clause #170: (wt=8) 739 [para_into,731.1.2,316.1.1,factor_simp] -d(m(b,2),1)| -d(b,a). given clause #171: (wt=13) 105 [para_from,34.1.1,14.1.1.1,demod,15,15,flip.1] m(b,m(b,m(2,x)))=m(a,m(a,x)). given clause #172: (wt=7) 751 [hyper,3,105.1] d(b,m(a,m(a,x))). given clause #173: (wt=7) 786 [para_from,105.1.1,4.1.2,unit_del,123,48] d(2,m(b,m(2,x))). given clause #174: (wt=5) 798 [hyper,4,786.1,unit_del,48] d(2,m(2,x)). given clause #175: (wt=5) 804 [para_into,786.1.2.2,46.1.1] d(2,m(b,a)). given clause #176: (wt=12) 109 [para_from,34.1.1,1.1.1,flip.1] m(b,x)!=m(a,a)|m(b,2)=x. given clause #177: (wt=5) 810 [para_into,798.1.2,16.1.1] d(2,m(x,2)). given clause #178: (wt=5) 815 [para_into,804.1.2,16.1.1] d(2,m(a,b)). given clause #179: (wt=7) 793 [para_into,751.1.2.2,16.1.1] d(b,m(a,m(x,a))). given clause #180: (wt=7) 802 [ur,66.1,786] m(b,m(2,x))!=b. given clause #181: (wt=11) 110 [hyper,2,100.1] m(b,f(b,m(a,a)))=m(a,a). given clause #182: (wt=7) 806 [para_into,786.1.2.2,16.1.1] d(2,m(b,m(x,2))). given clause #183: (wt=7) 857 [para_into,793.1.2,16.1.1,demod,15] d(b,m(x,m(a,a))). given clause #184: (wt=7) 861 [para_into,802.1.1.2,16.1.1] m(b,m(x,2))!=b. given clause #185: (wt=7) 917 [para_from,110.1.1,4.1.2,unit_del,30,48] d(2,f(b,m(a,a))). given clause #186: (wt=13) 113 [para_into,100.1.2,33.1.1] d(b,2)| -d(m(b,b),a)| -d(m(b,b),b). given clause #187: (wt=7) 922 [para_into,806.1.2,16.1.1,demod,15] d(2,m(x,m(2,b))). given clause #188: (wt=7) 931 [para_into,861.1.1.2,27.1.1,demod,864] f(b,m(a,a))!=b. given clause #189: (wt=7) 932 [para_into,861.1.1,16.1.1,demod,15] m(x,m(2,b))!=b. given clause #190: (wt=8) 745 [para_into,737.1.2,316.1.1,factor_simp] -d(m(a,a),1)| -d(b,a). given clause #191: (wt=12) 122 [para_into,98.2.2,21.1.1] -d(b,a)| -d(a,x)| -d(x,a)| -d(x,b). given clause #192: (wt=8) 746 [para_into,738.1.2,316.1.1,factor_simp] -d(m(2,b),1)| -d(b,a). given clause #193: (wt=8) 795 [para_into,751.1.2.2,2.2.1] d(b,m(a,x))| -d(a,x). given clause #194: (wt=6) 974 [para_into,795.1.2,11.1.1] d(b,a)| -d(a,1). given clause #195: (wt=8) 807 [para_into,786.1.2.2,2.2.1] d(2,m(b,x))| -d(2,x). given clause #196: (wt=11) 126 [para_into,36.1.1.2.2,25.1.1,demod,19,flip.1] m(a,m(a,f(b,b)))=m(a,a). given clause #197: (wt=3) 986 [para_into,807.1.2,11.1.1,unit_del,48] -d(2,1). given clause #198: (wt=3) 992 [ur,147.1,986] a!=1. given clause #199: (wt=5) 984 [para_into,807.1.2,25.1.1,unit_del,48] -d(2,f(b,b)). given clause #200: (wt=5) 989 [hyper,3,126.1] d(a,m(a,a)). given clause #201: (wt=13) 128 [para_into,36.1.1.2.2,16.1.1] m(2,m(b,m(x,b)))=m(a,m(a,x)). given clause #202: (wt=5) 993 [ur,38.1,986] m(a,a)!=1. given clause #203: (wt=5) 994 [ur,3.1,986] m(2,x)!=1. given clause #204: (wt=5) 996 [ur,1.1,992,demod,12] m(x,a)!=x. given clause #205: (wt=5) 998 [ur,147.1,984,flip.1] f(b,b)!=a. given clause #206: (wt=19) 130 [para_into,36.1.1.2.2,5.3.1,demod,12,flip.1] m(a,m(a,x))=m(2,b)| -d(m(b,x),a)| -d(m(b,x),b). given clause #207: (wt=5) 1035 [para_into,994.1.1,16.1.1] m(x,2)!=1. given clause #208: (wt=5) 1038 [para_into,996.1.1,27.1.1,flip.1] f(a,a)!=a. given clause #209: (wt=5) 1039 [para_into,996.1.1,16.1.1] m(a,x)!=x. given clause #210: (wt=6) 1014 [para_into,989.1.2,572.1.1] d(a,2)| -d(b,a). given clause #211: (wt=16) 131 [para_into,36.1.1.2.2,2.2.1] m(2,m(b,x))=m(a,m(a,f(b,x)))| -d(b,x). given clause #212: (wt=6) 1036 [para_into,994.1.1,2.2.1] x!=1| -d(2,x). given clause #213: (wt=5) 1115 [ur,1036.1,815] m(a,b)!=1. given clause #214: (wt=5) 1117 [ur,1036.1,804] m(b,a)!=1. given clause #215: (wt=7) 981 [hyper,807,815.1] d(2,m(b,m(a,b))). given clause #216: (wt=11) 132 [para_into,36.1.1.2,34.1.1,flip.1] m(a,m(a,2))=m(2,m(a,a)). given clause #217: (wt=7) 990 [hyper,1,126.1] m(a,f(b,b))=a. given clause #218: (wt=6) 1166 [para_from,990.1.1,3.1.1] a!=x|d(a,x). given clause #219: (wt=7) 999 [ur,38.1,984] m(a,a)!=f(b,b). given clause #220: (wt=7) 1004 [ur,3.1,984] m(2,x)!=f(b,b). given clause #221: (wt=21) 134 [para_into,36.1.1.2,5.3.1,demod,12,flip.1] m(a,m(a,x))=2| -d(m(b,m(b,x)),a)| -d(m(b,m(b,x)),b). given clause #222: (wt=5) 1177 [para_into,1004.1.1,25.1.1,flip.1] f(b,b)!=2. given clause #223: (wt=7) 1028 [ur,1.1,993,demod,12] m(x,m(a,a))!=x. given clause #224: (wt=7) 1034 [para_into,994.1.1,128.1.1] m(a,m(a,x))!=1. given clause #225: (wt=7) 1113 [ur,1036.1,922] m(x,m(2,b))!=1. given clause #226: (wt=13) 135 [para_into,36.1.1,16.1.1,demod,15,15] m(b,m(b,m(x,2)))=m(a,m(a,x)). given clause #227: (wt=7) 1114 [ur,1036.1,917] f(b,m(a,a))!=1. given clause #228: (wt=7) 1116 [ur,1036.1,806] m(b,m(x,2))!=1. given clause #229: (wt=7) 1118 [ur,1036.1,786] m(b,m(2,x))!=1. given clause #230: (wt=7) 1119 [ur,1036.1,293] m(x,m(a,a))!=1. given clause #231: (wt=11) 145 [para_from,46.1.1,14.1.1.1,flip.1] m(2,m(f(2,a),x))=m(a,x). ----> UNIT CONFLICT at 8760.80 sec ----> 1273 [binary,1272.1,1261.1] $F. Length of proof is 16. Level of proof is 10. ---------------- PROOF ---------------- 1 [] m(x,y)!=m(x,z)|y=z. 2 [] -d(x,y)|m(x,f(x,y))=y. 3 [] m(x,y)!=z|d(x,z). 4 [] -d(2,m(x,y))|d(2,x)|d(2,y). 5 [] -d(x,a)| -d(x,b)|x=1. 6 [] 2!=1. 7 [factor,4,2,3] -d(2,m(x,x))|d(2,x). 13 [] m(x,m(y,z))=m(m(x,y),z). 14 [copy,13,flip.1] m(m(x,y),z)=m(x,m(y,z)). 16 [] m(x,y)=m(y,x). 17 [] m(a,a)=m(2,m(b,b)). 18 [copy,17,flip.1] m(2,m(b,b))=m(a,a). 30 [hyper,3,18.1] d(2,m(a,a)). 39 [para_from,18.1.1,1.1.1] m(a,a)!=m(2,x)|m(b,b)=x. 42 [hyper,7,30.1] d(2,a). 46 [hyper,2,42.1] m(2,f(2,a))=a. 48 [ur,5.2,42,6] -d(2,b). 50 [ur,7.1,48] -d(2,m(b,b)). 59 [ur,3.1,50] m(2,x)!=m(b,b). 60 [copy,59,flip.1] m(b,b)!=m(2,x). 145 [para_from,46.1.1,14.1.1.1,flip.1] m(2,m(f(2,a),x))=m(a,x). 189 [ur,39.1,60] m(a,a)!=m(2,m(2,x)). 190 [copy,189,flip.1] m(2,m(2,x))!=m(a,a). 1261 [para_into,145.1.1.2,16.1.1] m(2,m(x,f(2,a)))=m(a,x). 1272 [para_from,145.1.1,190.1.1.2] m(2,m(a,x))!=m(a,a). 1273 [binary,1272.1,1261.1] $F. ------------ end of proof ------------- translate_ur: sat_map for box=2, orig= 48 [ur,5.2,42,6] -d(2,b). 42 0 6 0 [] -d(x,a)| -d(x,b)|x=1. translate_ur: sat_map for box=1, orig= 50 [ur,7.1,48] -d(2,m(b,b)). 0 48 0 [] -d(2,m(x,x))|d(2,x). translate_ur: sat_map for box=1, orig= 59 [ur,3.1,50] m(2,x)!=m(b,b). 0 50 0 [] m(x,y)!=z|d(x,z). translate_ur: sat_map for box=1, orig= 189 [ur,39.1,60] m(a,a)!=m(2,m(2,x)). 0 60 0 [] m(a,a)!=m(2,x)|m(b,b)=x. ;; BEGINNING OF PROOF OBJECT ( (1 (input) (or (not (= (m v0 v1) (m v0 v2))) (= v1 v2)) (1)) (2 (input) (or (not (d v0 v1)) (= (m v0 (f v0 v1)) v1)) (2)) (3 (input) (or (not (= (m v0 v1) v2)) (d v0 v2)) (3)) (4 (input) (or (not (d (2) (m v0 v1))) (or (d (2) v0) (d (2) v1))) (4)) (5 (input) (or (not (d v0 (a))) (or (not (d v0 (b))) (= v0 (1)))) (5)) (6 (input) (not (= (2) (1))) (6)) (7 (instantiate 4 ((v0 . v1))) (or (not (d (2) (m v1 v1))) (or (d (2) v1) (d (2) v1))) NIL) (8 (propositional 7) (or (not (d (2) (m v1 v1))) (d (2) v1)) NIL) (9 (instantiate 8 ((v1 . v0))) (or (not (d (2) (m v0 v0))) (d (2) v0)) (7)) (10 (input) (= (m v0 (m v1 v2)) (m (m v0 v1) v2)) (13)) (11 (flip 10 ()) (= (m (m v0 v1) v2) (m v0 (m v1 v2))) (14)) (12 (input) (= (m v0 v1) (m v1 v0)) (16)) (13 (input) (= (m (a) (a)) (m (2) (m (b) (b)))) (17)) (14 (flip 13 ()) (= (m (2) (m (b) (b))) (m (a) (a))) (18)) (15 (instantiate 3 ((v0 . (2))(v1 . (m (b) (b)))(v2 . (m (a) (a))))) (or (not (= (m (2) (m (b) (b))) (m (a) (a)))) (d (2) (m (a) (a)))) NIL) (16 (resolve 15 (1) 14 ()) (d (2) (m (a) (a))) (30)) (17 (instantiate 1 ((v0 . (2))(v1 . (m (b) (b)))(v2 . v66))) (or (not (= (m (2) (m (b) (b))) (m (2) v66))) (= (m (b) (b)) v66)) NIL) (18 (paramod 14 (1) 17 (1 1 1)) (or (not (= (m (a) (a)) (m (2) v66))) (= (m (b) (b)) v66)) NIL) (19 (instantiate 18 ((v66 . v0))) (or (not (= (m (a) (a)) (m (2) v0))) (= (m (b) (b)) v0)) (39)) (20 (instantiate 9 ((v0 . (a)))) (or (not (d (2) (m (a) (a)))) (d (2) (a))) NIL) (21 (resolve 20 (1) 16 ()) (d (2) (a)) (42)) (22 (instantiate 2 ((v0 . (2))(v1 . (a)))) (or (not (d (2) (a))) (= (m (2) (f (2) (a))) (a))) NIL) (23 (resolve 22 (1) 21 ()) (= (m (2) (f (2) (a))) (a)) (46)) (24 (instantiate 5 ((v0 . (2)))) (or (not (d (2) (a))) (or (not (d (2) (b))) (= (2) (1)))) NIL) (25 (resolve 24 (1) 21 ()) (or (not (d (2) (b))) (= (2) (1))) NIL) (26 (resolve 25 (2) 6 ()) (not (d (2) (b))) (48)) (27 (instantiate 9 ((v0 . (b)))) (or (not (d (2) (m (b) (b)))) (d (2) (b))) NIL) (28 (resolve 27 (2) 26 ()) (not (d (2) (m (b) (b)))) (50)) (29 (instantiate 3 ((v0 . (2))(v2 . (m (b) (b))))) (or (not (= (m (2) v1) (m (b) (b)))) (d (2) (m (b) (b)))) NIL) (30 (resolve 29 (2) 28 ()) (not (= (m (2) v1) (m (b) (b)))) NIL) (31 (instantiate 30 ((v1 . v0))) (not (= (m (2) v0) (m (b) (b)))) (59)) (32 (flip 31 ()) (not (= (m (b) (b)) (m (2) v0))) (60)) (33 (instantiate 11 ((v0 . (2))(v1 . (f (2) (a)))(v2 . v66))) (= (m (m (2) (f (2) (a))) v66) (m (2) (m (f (2) (a)) v66))) NIL) (34 (paramod 23 (1) 33 (1 1)) (= (m (a) v66) (m (2) (m (f (2) (a)) v66))) NIL) (35 (flip 34 ()) (= (m (2) (m (f (2) (a)) v66)) (m (a) v66)) NIL) (36 (instantiate 35 ((v66 . v0))) (= (m (2) (m (f (2) (a)) v0)) (m (a) v0)) (145)) (37 (instantiate 19 ((v0 . (m (2) v64)))) (or (not (= (m (a) (a)) (m (2) (m (2) v64)))) (= (m (b) (b)) (m (2) v64))) NIL) (38 (instantiate 32 ((v0 . v64))) (not (= (m (b) (b)) (m (2) v64))) NIL) (39 (resolve 37 (2) 38 ()) (not (= (m (a) (a)) (m (2) (m (2) v64)))) NIL) (40 (instantiate 39 ((v64 . v0))) (not (= (m (a) (a)) (m (2) (m (2) v0)))) (189)) (41 (flip 40 ()) (not (= (m (2) (m (2) v0)) (m (a) (a)))) (190)) (42 (instantiate 12 ((v0 . (f (2) (a)))(v1 . v64))) (= (m (f (2) (a)) v64) (m v64 (f (2) (a)))) NIL) (43 (instantiate 36 ((v0 . v64))) (= (m (2) (m (f (2) (a)) v64)) (m (a) v64)) NIL) (44 (paramod 42 (1) 43 (1 2)) (= (m (2) (m v64 (f (2) (a)))) (m (a) v64)) NIL) (45 (instantiate 44 ((v64 . v0))) (= (m (2) (m v0 (f (2) (a)))) (m (a) v0)) (1261)) (46 (instantiate 41 ((v0 . (m (f (2) (a)) v0)))) (not (= (m (2) (m (2) (m (f (2) (a)) v0))) (m (a) (a)))) NIL) (47 (paramod 36 (1) 46 (1 1 2)) (not (= (m (2) (m (a) v0)) (m (a) (a)))) (1272)) (48 (instantiate 47 ((v0 . (f (2) (a))))) (not (= (m (2) (m (a) (f (2) (a)))) (m (a) (a)))) NIL) (49 (instantiate 45 ((v0 . (a)))) (= (m (2) (m (a) (f (2) (a)))) (m (a) (a))) NIL) (50 (resolve 48 () 49 ()) false (1273)) ) ;; END OF PROOF OBJECT Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 231 clauses generated 5020 clauses kept 1192 clauses forward subsumed 2515 clauses back subsumed 299 Kbytes malloced 798 ----------- times (seconds) ----------- user CPU time 8760.83 (2 hr, 26 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 2 (0 hr, 0 min, 2 sec) hyper_res time 0.00 UR_res time 0.00 para_into time 0.00 para_from time 0.00 for_sub time 0.00 back_sub time 0.00 conflict time 0.00 demod time 0.00 That finishes the proof of the theorem. Process 0 finished Thu Sep 20 15:40:16 2001