----- Otter 3.3, August 2003 ----- The process was started by freek on oneblin, Wed Mar 2 15:38:41 2005 The command was "otter". The process ID is 14745. 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. 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(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(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,9,3] d(1,x). given clause #4: (wt=5) 11 [] m(x,1)=x. given clause #5: (wt=3) 24 [hyper,11,3] 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,24,2] 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,27,3] d(f(x,x),x). given clause #13: (wt=5) 30 [hyper,18,3] d(2,m(a,a)). given clause #14: (wt=3) 42 [hyper,30,7] d(2,a). given clause #15: (wt=3) 48 [ur,42,5,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,48,7] -d(2,m(b,b)). given clause #18: (wt=5) 51 [ur,48,3] 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,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,34,3] 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,42,2] 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,50,flip.1] m(b,b)!=a. given clause #44: (wt=7) 58 [ur,50,4,48] -d(2,m(b,m(b,b))). given clause #45: (wt=7) 59 [ur,50,3] 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,62,1] m(x,b)!=m(x,2). given clause #50: (wt=7) 93 [ur,83,1] m(x,b)!=m(x,a). given clause #51: (wt=11) 40 [hyper,29,2] m(f(x,x),f(f(x,x),x))=x. given clause #52: (wt=7) 123 [hyper,36,3] 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,142,3] d(f(2,a),a). given clause #56: (wt=11) 43 [hyper,30,2] m(2,f(2,m(a,a)))=m(a,a). given clause #57: (wt=7) 150 [ur,38,50,flip.1] m(b,b)!=m(a,a). given clause #58: (wt=7) 157 [ur,58,147,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,153] m(a,a)!=m(2,a). given clause #63: (wt=7) 186 [ur,165,39] 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,50,7,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,63,1] 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,58] -d(a,b). given clause #105: (wt=5) 411 [ur,410,3] 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,464,3] 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,153,1] m(x,m(b,b))!=m(x,a). given clause #135: (wt=9) 158 [ur,58,38,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,58,3] 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,165,1] m(x,m(b,b))!=m(x,2). given clause #153: (wt=9) 189 [ur,60,39] 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,93,39,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,150,39,flip.1] m(2,m(a,a))!=m(a,a). given clause #158: (wt=9) 250 [ur,170,39] 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,288,39,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,57,147,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,105,3] 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,786,4,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,786,66] m(b,m(2,x))!=b. given clause #181: (wt=11) 110 [hyper,100,2] 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,986,147] 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,126,3] 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,986,38] m(a,a)!=1. given clause #203: (wt=5) 994 [ur,986,3] m(2,x)!=1. given clause #204: (wt=5) 996 [ur,992,1,demod,12] m(x,a)!=x. given clause #205: (wt=5) 998 [ur,984,147,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,815] m(a,b)!=1. given clause #214: (wt=5) 1117 [ur,1036,804] m(b,a)!=1. given clause #215: (wt=7) 981 [hyper,807,815] 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,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,984,38] m(a,a)!=f(b,b). given clause #220: (wt=7) 1004 [ur,984,3] 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,993,1,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,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,917] f(b,m(a,a))!=1. given clause #228: (wt=7) 1116 [ur,1036,806] m(b,m(x,2))!=1. given clause #229: (wt=7) 1118 [ur,1036,786] m(b,m(2,x))!=1. given clause #230: (wt=7) 1119 [ur,1036,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 0.25 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,18,3] 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,30,7] d(2,a). 46 [hyper,42,2] m(2,f(2,a))=a. 48 [ur,42,5,6] -d(2,b). 50 [ur,48,7] -d(2,m(b,b)). 59 [ur,50,3] 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,60,39] 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 ------------- 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 830 ----------- times (seconds) ----------- user CPU time 0.25 (0 hr, 0 min, 0 sec) system CPU time 0.06 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) hyper_res time 0.00 UR_res time 0.01 para_into time 0.02 para_from time 0.00 for_sub time 0.05 back_sub time 0.01 conflict time 0.01 demod time 0.01 That finishes the proof of the theorem. Process 14745 finished Wed Mar 2 15:38:41 2005