----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Wed Aug 6 14:26:48 2003 The command was "../../bin/otter". The process ID is 6390. op(400,xfx,*). set(para_into). set(para_from). set(order_eq). set(dynamic_demod). set(process_input). set(demod_out_in). set(lrpo). lex([$T,A,B,C,D,E,1,_*_,rs(_,_),ls(_,_),_=_]). assign(max_weight,20). assign(pick_given_ratio,3). assign(max_proofs,2). assign(max_mem,20000). clear(print_kept). clear(print_new_demod). list(usable). 0 [] x=x. 0 [] x*rs(x,y)=y. 0 [] rs(x,x*y)=y. 0 [] ls(x,y)*y=x. 0 [] ls(x*y,y)=x. 0 [] 1*x=x. 0 [] x*1=x. end_of_list. list(sos). 0 [] (x*y)* (z*x)= (x* (y*z))*x. 0 [] A* (B* (A*C))!= ((A*B)*A)*C|$ANS(Moufang_3). end_of_list. list(demodulators). 1 [] EQ(((x*y)*z)*y=x* (y* (z*y)),$T). 2 [] EQ(x* (y* (z*y))= ((x*y)*z)*y,$T). end_of_list. list(hot). 3 [] (x*y)* (z*x)= (x* (y*z))*x. 4 [] x*rs(x,y)=y. 5 [] rs(x,x*y)=y. 6 [] ls(x,y)*y=x. 7 [] ls(x*y,y)=x. 8 [] 1*x=x. 9 [] x*1=x. end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 10 [] x=x. ** KEPT (pick-wt=7): 11 [] x*rs(x,y)=y. ---> New Demodulator: 12 [new_demod,11] x*rs(x,y)=y. ** KEPT (pick-wt=7): 13 [] rs(x,x*y)=y. ---> New Demodulator: 14 [new_demod,13] rs(x,x*y)=y. ** KEPT (pick-wt=7): 15 [] ls(x,y)*y=x. ---> New Demodulator: 16 [new_demod,15] ls(x,y)*y=x. ** KEPT (pick-wt=7): 17 [] ls(x*y,y)=x. ---> New Demodulator: 18 [new_demod,17] ls(x*y,y)=x. ** KEPT (pick-wt=5): 19 [] 1*x=x. ---> New Demodulator: 20 [new_demod,19] 1*x=x. ** KEPT (pick-wt=5): 21 [] x*1=x. ---> New Demodulator: 22 [new_demod,21] x*1=x. ------------> process sos: ** KEPT (pick-wt=15): 24 [copy,23,flip.1] (x* (y*z))*x= (x*y)* (z*x). ---> New Demodulator: 25 [new_demod,24] (x* (y*z))*x= (x*y)* (z*x). ** KEPT (pick-wt=15): 27 [copy,26,flip.1] ((A*B)*A)*C!=A* (B* (A*C))|$ANS(Moufang_3). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=15) 24 [copy,23,flip.1] (x* (y*z))*x= (x*y)* (z*x). 73 back subsumes 52. 83 back subsumes 45. given clause #2: (wt=7) 128 (heat=1) [para_into,116.1.1.2.1,9.1.1,demod,72,20] rs(x,x)*y=y. 138 back subsumes 126. given clause #3: (wt=5) 138 [para_into,128.1.1,21.1.1] rs(x,x)=1. given clause #4: (wt=5) 140 [para_into,128.1.1,11.1.1,demod,139,flip.1] rs(1,x)=x. given clause #5: (wt=15) 27 [copy,26,flip.1] ((A*B)*A)*C!=A* (B* (A*C))|$ANS(Moufang_3). given clause #6: (wt=5) 142 [para_from,128.1.1,17.1.1.1,demod,139] ls(x,x)=1. given clause #7: (wt=9) 81 (heat=1) [para_into,36.1.1.2,9.1.1,demod,20,22] rs(1,x)*y=x*y. given clause #8: (wt=9) 90 (heat=1) [para_into,38.1.1.2,9.1.1,demod,20,20] x*ls(y,1)=x*y. 145 back subsumes 118. given clause #9: (wt=11) 28 [para_into,24.1.1.1.2,19.1.1,demod,22] (x*y)*x=x* (y*x). given clause #10: (wt=5) 145 [para_into,90.1.1,128.1.1,demod,129] ls(x,1)=x. given clause #11: (wt=11) 42 (heat=1) [para_into,28.1.1.1,4.1.1,flip.1] x* (rs(x,y)*x)=y*x. 178 back subsumes 166. 188 back subsumes 178. given clause #12: (wt=7) 202 (heat=1) [para_into,176.1.1.2,8.1.1,demod,139,flip.1] rs(x,1)*x=1. given clause #13: (wt=15) 30 [para_into,24.1.1.1.2,15.1.1,demod,29,flip.1] (x*ls(y,z))* (z*x)=x* (y*x). given clause #14: (wt=7) 213 [para_from,202.1.1,17.1.1.1] ls(1,x)=rs(x,1). given clause #15: (wt=7) 215 [para_from,202.1.1,13.1.1.2] rs(rs(x,1),1)=x. given clause #16: (wt=7) 248 (heat=1) [para_into,246.1.1,9.1.1,demod,22] rs(ls(x,y),x)=y. given clause #17: (wt=15) 32 [para_into,24.1.1.1.2,11.1.1,demod,29,flip.1] (x*y)* (rs(y,z)*x)=x* (z*x). given clause #18: (wt=9) 194 (heat=1) [para_into,174.1.1.1,8.1.1] ls(x,rs(x,1)*x)=x. given clause #19: (wt=9) 221 (heat=1) [para_from,207.1.1,5.1.1.2,demod,14,flip.1] (x*rs(y,1))*y=x. 304 back subsumes 237. 304 back subsumes 235. given clause #20: (wt=9) 244 (heat=1) [para_from,211.1.2,7.1.1.1,demod,47] rs(x,1)* (x*y)=y. given clause #21: (wt=19) 34 [para_into,24.1.2.1,15.1.1,demod,29] ls(x,y)* ((y*z)*ls(x,y))=x* (z*ls(x,y)). given clause #22: (wt=9) 255 (heat=1) [para_from,250.1.1,7.1.1.1,demod,47] rs(x,1)*y=rs(x,y). 444 back subsumes 421. given clause #23: (wt=9) 262 [para_into,221.1.1.1.2,248.1.1,demod,214] (x*y)*rs(y,1)=x. given clause #24: (wt=9) 266 [para_into,221.1.1.1,15.1.1,flip.1] ls(x,rs(y,1))=x*y. given clause #25: (wt=15) 36 [para_into,24.1.2.1,11.1.1,demod,29] x* ((rs(x,y)*z)*x)=y* (z*x). given clause #26: (wt=9) 270 (heat=1) [para_into,262.1.1.1,6.1.1,flip.1] ls(x,y)=x*rs(y,1). given clause #27: (wt=9) 272 (heat=1) [para_into,262.1.1.1,4.1.1] x*rs(rs(y,x),1)=y. given clause #28: (wt=9) 278 (heat=1) [para_from,262.1.1,5.1.1.2] rs(x*y,x)=rs(y,1). given clause #29: (wt=15) 38 [para_into,24.1.2.2,15.1.1,demod,29] x* ((y*ls(z,x))*x)= (x*y)*z. -------- PROOF -------- 586 [binary,584.1,144.1] $ANS(Moufang_3). ----> UNIT CONFLICT at 0.10 sec ----> 586 [binary,584.1,144.1] $ANS(Moufang_3). Length of proof is 34. Level of proof is 14. ---------------- PROOF ---------------- 4 [] x*rs(x,y)=y. 5 [] rs(x,x*y)=y. 6 [] ls(x,y)*y=x. 7 [] ls(x*y,y)=x. 8 [] 1*x=x. 9 [] x*1=x. 11 [] x*rs(x,y)=y. 14,13 [] rs(x,x*y)=y. 15 [] ls(x,y)*y=x. 17 [] ls(x*y,y)=x. 20,19 [] 1*x=x. 22,21 [] x*1=x. 23 [] (x*y)* (z*x)= (x* (y*z))*x. 24 [copy,23,flip.1] (x* (y*z))*x= (x*y)* (z*x). 26 [] A* (B* (A*C))!= ((A*B)*A)*C|$ANS(Moufang_3). 27 [copy,26,flip.1] ((A*B)*A)*C!=A* (B* (A*C))|$ANS(Moufang_3). 29,28 [para_into,24.1.1.1.2,19.1.1,demod,22] (x*y)*x=x* (y*x). 30 [para_into,24.1.1.1.2,15.1.1,demod,29,flip.1] (x*ls(y,z))* (z*x)=x* (y*x). 32 [para_into,24.1.1.1.2,11.1.1,demod,29,flip.1] (x*y)* (rs(y,z)*x)=x* (z*x). 36 [para_into,24.1.2.1,11.1.1,demod,29] x* ((rs(x,y)*z)*x)=y* (z*x). 38 [para_into,24.1.2.2,15.1.1,demod,29] x* ((y*ls(z,x))*x)= (x*y)*z. 42 (heat=1) [para_into,28.1.1.1,4.1.1,flip.1] x* (rs(x,y)*x)=y*x. 47,46 (heat=1) [para_from,28.1.1,7.1.1.1] ls(x* (y*x),x)=x*y. 72,71 (heat=1) [para_from,32.1.1,5.1.1.2] rs(x*y,x* (z*x))=rs(y,z)*x. 82,81 (heat=1) [para_into,36.1.1.2,9.1.1,demod,20,22] rs(1,x)*y=x*y. 116 [para_from,24.1.1,13.1.1.2] rs(x* (y*z),(x*y)* (z*x))=x. 129,128 (heat=1) [para_into,116.1.1.2.1,9.1.1,demod,72,20] rs(x,x)*y=y. 139,138 [para_into,128.1.1,21.1.1] rs(x,x)=1. 144 [para_from,81.1.2,27.1.2.2.2,demod,29,82] (A* (B*A))*C!=A* (B* (A*C))|$ANS(Moufang_3). 176 [para_from,42.1.1,13.1.1.2] rs(x,y*x)=rs(x,y)*x. 202 (heat=1) [para_into,176.1.1.2,8.1.1,demod,139,flip.1] rs(x,1)*x=1. 207 [para_from,202.1.1,24.1.2.2,demod,29,22] x* ((y*rs(x,1))*x)=x*y. 211 [para_from,202.1.1,24.1.2.1,demod,29,20] rs(x,1)* ((x*y)*rs(x,1))=y*rs(x,1). 214,213 [para_from,202.1.1,17.1.1.1] ls(1,x)=rs(x,1). 221 (heat=1) [para_from,207.1.1,5.1.1.2,demod,14,flip.1] (x*rs(y,1))*y=x. 244 (heat=1) [para_from,211.1.2,7.1.1.1,demod,47] rs(x,1)* (x*y)=y. 246 [para_from,30.1.1,13.1.1.2,demod,72] rs(ls(x,y),x)*z=y*z. 248 (heat=1) [para_into,246.1.1,9.1.1,demod,22] rs(ls(x,y),x)=y. 262 [para_into,221.1.1.1.2,248.1.1,demod,214] (x*y)*rs(y,1)=x. 271,270 (heat=1) [para_into,262.1.1.1,6.1.1,flip.1] ls(x,y)=x*rs(y,1). 272 (heat=1) [para_into,262.1.1.1,4.1.1] x*rs(rs(y,x),1)=y. 316 [para_into,244.1.1.1,248.1.1,demod,271,20] x* (rs(x,1)*y)=y. 331,330 (heat=1) [para_into,316.1.1.2,4.1.1,flip.1] rs(rs(x,1),y)=x*y. 380 [para_from,244.1.1,17.1.1.1,demod,271] x*rs(y*x,1)=rs(y,1). 396,395 (heat=1) [para_from,380.1.1,5.1.1.2,flip.1] rs(x*y,1)=rs(y,rs(x,1)). 526,525 [para_from,272.1.1,244.1.1.2,flip.1] rs(rs(x,y),1)=rs(y,1)*x. 573 [para_from,38.1.2,221.1.1.1,demod,271] (x* ((y* (rs(z,1)*rs(x,1)))*x))*z=x*y. 584 (heat=1) [para_into,573.1.1.1.2.1,6.1.1,demod,271,396,331,526,129] (x* (y*x))*z=x* (y* (x*z)). 586 [binary,584.1,144.1] $ANS(Moufang_3). ------------ end of proof ------------- given clause #30: (wt=9) 316 [para_into,244.1.1.1,248.1.1,demod,271,20] x* (rs(x,1)*y)=y. given clause #31: (wt=9) 330 (heat=1) [para_into,316.1.1.2,4.1.1,flip.1] rs(rs(x,1),y)=x*y. -------- PROOF -------- 615 [binary,614.1,10.1] $ANS(Moufang_3). ----> UNIT CONFLICT at 0.11 sec ----> 615 [binary,614.1,10.1] $ANS(Moufang_3). Length of proof is 32. Level of proof is 15. ---------------- PROOF ---------------- 4 [] x*rs(x,y)=y. 5 [] rs(x,x*y)=y. 6 [] ls(x,y)*y=x. 7 [] ls(x*y,y)=x. 8 [] 1*x=x. 9 [] x*1=x. 10 [] x=x. 11 [] x*rs(x,y)=y. 14,13 [] rs(x,x*y)=y. 15 [] ls(x,y)*y=x. 17 [] ls(x*y,y)=x. 20,19 [] 1*x=x. 22,21 [] x*1=x. 23 [] (x*y)* (z*x)= (x* (y*z))*x. 24 [copy,23,flip.1] (x* (y*z))*x= (x*y)* (z*x). 26 [] A* (B* (A*C))!= ((A*B)*A)*C|$ANS(Moufang_3). 27 [copy,26,flip.1] ((A*B)*A)*C!=A* (B* (A*C))|$ANS(Moufang_3). 29,28 [para_into,24.1.1.1.2,19.1.1,demod,22] (x*y)*x=x* (y*x). 30 [para_into,24.1.1.1.2,15.1.1,demod,29,flip.1] (x*ls(y,z))* (z*x)=x* (y*x). 32 [para_into,24.1.1.1.2,11.1.1,demod,29,flip.1] (x*y)* (rs(y,z)*x)=x* (z*x). 38 [para_into,24.1.2.2,15.1.1,demod,29] x* ((y*ls(z,x))*x)= (x*y)*z. 42 (heat=1) [para_into,28.1.1.1,4.1.1,flip.1] x* (rs(x,y)*x)=y*x. 47,46 (heat=1) [para_from,28.1.1,7.1.1.1] ls(x* (y*x),x)=x*y. 72,71 (heat=1) [para_from,32.1.1,5.1.1.2] rs(x*y,x* (z*x))=rs(y,z)*x. 116 [para_from,24.1.1,13.1.1.2] rs(x* (y*z),(x*y)* (z*x))=x. 129,128 (heat=1) [para_into,116.1.1.2.1,9.1.1,demod,72,20] rs(x,x)*y=y. 139,138 [para_into,128.1.1,21.1.1] rs(x,x)=1. 176 [para_from,42.1.1,13.1.1.2] rs(x,y*x)=rs(x,y)*x. 202 (heat=1) [para_into,176.1.1.2,8.1.1,demod,139,flip.1] rs(x,1)*x=1. 207 [para_from,202.1.1,24.1.2.2,demod,29,22] x* ((y*rs(x,1))*x)=x*y. 211 [para_from,202.1.1,24.1.2.1,demod,29,20] rs(x,1)* ((x*y)*rs(x,1))=y*rs(x,1). 214,213 [para_from,202.1.1,17.1.1.1] ls(1,x)=rs(x,1). 221 (heat=1) [para_from,207.1.1,5.1.1.2,demod,14,flip.1] (x*rs(y,1))*y=x. 244 (heat=1) [para_from,211.1.2,7.1.1.1,demod,47] rs(x,1)* (x*y)=y. 246 [para_from,30.1.1,13.1.1.2,demod,72] rs(ls(x,y),x)*z=y*z. 248 (heat=1) [para_into,246.1.1,9.1.1,demod,22] rs(ls(x,y),x)=y. 262 [para_into,221.1.1.1.2,248.1.1,demod,214] (x*y)*rs(y,1)=x. 271,270 (heat=1) [para_into,262.1.1.1,6.1.1,flip.1] ls(x,y)=x*rs(y,1). 272 (heat=1) [para_into,262.1.1.1,4.1.1] x*rs(rs(y,x),1)=y. 316 [para_into,244.1.1.1,248.1.1,demod,271,20] x* (rs(x,1)*y)=y. 331,330 (heat=1) [para_into,316.1.1.2,4.1.1,flip.1] rs(rs(x,1),y)=x*y. 380 [para_from,244.1.1,17.1.1.1,demod,271] x*rs(y*x,1)=rs(y,1). 396,395 (heat=1) [para_from,380.1.1,5.1.1.2,flip.1] rs(x*y,1)=rs(y,rs(x,1)). 526,525 [para_from,272.1.1,244.1.1.2,flip.1] rs(rs(x,y),1)=rs(y,1)*x. 573 [para_from,38.1.2,221.1.1.1,demod,271] (x* ((y* (rs(z,1)*rs(x,1)))*x))*z=x*y. 585,584 (heat=1) [para_into,573.1.1.1.2.1,6.1.1,demod,271,396,331,526,129] (x* (y*x))*z=x* (y* (x*z)). 614 [para_from,330.1.2,27.1.2.2.2,demod,29,585,331] A* (B* (A*C))!=A* (B* (A*C))|$ANS(Moufang_3). 615 [binary,614.1,10.1] $ANS(Moufang_3). ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 31 clauses generated 3887 (hot clauses generated) 1918 para_from generated 1809 para_into generated 2078 demod & eval rewrites 8511 clauses wt,lit,sk delete 885 tautologies deleted 0 clauses forward subsumed 2676 (subsumed by sos) 348 unit deletions 0 factor simplifications 0 clauses kept 335 (hot clauses kept) 247 new demodulators 267 empty clauses 2 clauses back demodulated 0 clauses back subsumed 9 usable size 38 sos size 288 demodulators size 269 passive size 0 hot size 7 Kbytes malloced 638 ----------- times (seconds) ----------- user CPU time 0.11 (0 hr, 0 min, 0 sec) system CPU time 0.04 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) input time 0.00 clausify time 0.00 process input 0.00 pick given time 0.00 para_into time 0.01 para_from time 0.01 pre_process time 0.07 renumber time 0.01 demod time 0.00 order equalities 0.01 unit deleletion 0.00 factor simplify 0.00 weigh cl time 0.00 hints keep time 0.00 sort lits time 0.00 forward subsume 0.01 delete cl time 0.00 keep cl time 0.01 hints time 0.00 print_cl time 0.00 conflict time 0.00 new demod time 0.01 post_process time 0.00 back demod time 0.00 back subsume 0.00 factor time 0.00 hot list time 0.06 unindex time 0.00 That finishes the proof of the theorem. Process 6390 finished Wed Aug 6 14:26:48 2003