----- Otter 3.3f, August 2004 ----- The process was started by mccune on cleo.thornwood, Mon Nov 14 15:26:22 2005 The command was "otter33f -f lem1.in". The process ID is 16992. % Reading file lem1.in. op(400,xfx,*). set(para_from). set(para_into). set(para_from_vars). set(para_into_vars). set(order_eq). set(geometric_rule). set(geometric_rewrite_before). assign(pick_given_ratio,4). clear(print_kept). clear(print_new_demod). clear(print_back_demod). assign(max_mem,16000). set(back_demod). dependent: set(dynamic_demod). set(process_input). clear(para_into_vars). list(usable). 0 [] x=x. end_of_list. list(sos). 0 [] f(x,y,z,u,v)=f(x,y,z,v,u). 0 [] f(e,e,e,e,e)=e. 0 [] f(e,e,e,x,f(e,e,e,x,y))=y. end_of_list. list(passive). 1 [] f(A1,A2,A3,A4,f(A1,A2,A3,A4,A5))!=A5. end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 2 [] x=x. ------------> process sos: ** KEPT (pick-wt=13): 3 [] f(x,y,z,u,v)=f(x,y,z,v,u). ** KEPT (pick-wt=8): 4 [] f(e,e,e,e,e)=e. ---> New Demodulator: 5 [new_demod,4] f(e,e,e,e,e)=e. ** KEPT (pick-wt=13): 6 [] f(e,e,e,x,f(e,e,e,x,y))=y. ---> New Demodulator: 7 [new_demod,6] f(e,e,e,x,f(e,e,e,x,y))=y. >>>> Starting back demodulation with 5. >>>> Starting back demodulation with 7. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=13) 3 [] f(x,y,z,u,v)=f(x,y,z,v,u). given clause #2: (wt=8) 4 [] f(e,e,e,e,e)=e. given clause #3: (wt=13) 6 [] f(e,e,e,x,f(e,e,e,x,y))=y. given clause #4: (wt=13) 8 [para_into,6.1.1.5,3.1.2] f(e,e,e,x,f(e,e,e,y,x))=y. given clause #5: (wt=18) 12 [para_from,6.1.2,4.1.2,gL-id,gL-id,gL-id,flip.1] f(x,y,z,u,f(e,e,e,u,e))=f(x,y,z,e,e). 20 back subsumes 19. given clause #6: (wt=13) 10 [para_into,6.1.1,3.1.2] f(e,e,e,f(e,e,e,x,y),x)=y. given clause #7: (wt=18) 15 [para_from,8.1.2,4.1.2,gL-id,gL-id,gL-id,flip.1] f(x,y,z,u,f(e,e,e,e,u))=f(x,y,z,e,e). 29 back subsumes 28. given clause #8: (wt=13) 13 [para_into,8.1.1.5,6.1.1] f(e,e,e,f(e,e,e,x,y),y)=x. given clause #9: (wt=23) 20 [para_into,12.1.2,12.1.2,gL-id,gL-id,gL-id,gL-id] f(x,y,z,u,f(v,w,v6,u,v7))=f(x,y,z,v8,f(v,w,v6,v8,v7)). 43 back subsumes 30. 44 back subsumes 38. 48 back subsumes 33. 49 back subsumes 46. given clause #10: (wt=18) 16 [para_into,12.1.1,3.1.2] f(x,y,z,f(e,e,e,u,e),u)=f(x,y,z,e,e). 62 back subsumes 61. given clause #11: (wt=28) 17 [para_into,12.1.2.5,8.1.2,gL-id,gL-id,gL-id,flip.1] f(x,y,z,e,f(u,v,w,v6,f(e,e,e,e,v6)))=f(x,y,z,v7,f(u,v,w,v7,e)). given clause #12: (wt=18) 23 [para_from,10.1.1,12.1.1.5] f(x,y,z,f(e,e,e,e,u),u)=f(x,y,z,e,e). 109 back subsumes 108. given clause #13: (wt=23) 29 [para_into,15.1.2,15.1.2,gL-id,gL-id,gL-id,gL-id] f(x,y,z,u,f(v,w,v6,v7,u))=f(x,y,z,v8,f(v,w,v6,v7,v8)). 128 back subsumes 63. 129 back subsumes 111. 130 back subsumes 129. 131 back subsumes 67. 132 back subsumes 117. 133 back subsumes 132. 135 back subsumes 76. given clause #14: (wt=23) 40 [para_into,20.1.1.5,10.1.1] f(x,y,z,f(e,e,e,u,v),v)=f(x,y,z,w,f(e,e,e,w,u)). 152 back subsumes 110. 158 back subsumes 157. 168 back subsumes 116. given clause #15: (wt=23) 62 [para_into,16.1.2,16.1.2,gL-id,gL-id,gL-id,gL-id] f(x,y,z,f(u,v,w,v6,v7),v6)=f(x,y,z,f(u,v,w,v8,v7),v8). given clause #16: (wt=28) 18 [para_into,12.1.2.5,6.1.2,gL-id,gL-id,gL-id,flip.1] f(x,y,z,e,f(u,v,w,v6,f(e,e,e,v6,e)))=f(x,y,z,v7,f(u,v,w,v7,e)). given clause #17: (wt=23) 109 [para_into,23.1.2,23.1.2,gL-id,gL-id,gL-id,gL-id] f(x,y,z,f(u,v,w,v6,v7),v7)=f(x,y,z,f(u,v,w,v6,v8),v8). given clause #18: (wt=23) 41 [para_into,20.1.1.5,8.1.1,flip.1] f(x,y,z,u,f(e,e,e,u,f(e,e,e,v,w)))=f(x,y,z,w,v). given clause #19: (wt=23) 152 [para_into,40.1.2.5,40.1.1,gL-id,gL-id,gL-id,demod,7] f(x,y,z,f(u,v,w,v6,v7),v7)=f(x,y,z,f(u,v,w,v8,v6),v8). 315 back subsumes 170. 330 back subsumes 131. 331 back subsumes 244. 346 back subsumes 40. 366 back subsumes 128. 367 back subsumes 321. 385 back subsumes 47. given clause #20: (wt=23) 42 [para_into,20.1.1.5,6.1.1,flip.1] f(x,y,z,u,f(e,e,e,u,f(e,e,e,v,w)))=f(x,y,z,v,w). given clause #21: (wt=28) 21 [para_into,12.1.2,8.1.2,gL-id,gL-id,gL-id,flip.1] f(e,e,e,x,f(y,z,u,f(v,w,v6,e,e),x))=f(v,w,v6,v7,f(y,z,u,v7,e)). given clause #22: (wt=18) 485 [gL,21,flip.1] f(x,y,z,f(x,y,z,e,e),u)=f(e,e,e,e,u). 510 back subsumes 509. given clause #23: (wt=13) 514 [para_into,485.1.2,23.1.2,gL-id,demod,14] f(x,y,z,f(x,y,z,u,e),e)=u. 561 back subsumes 491. 561 back subsumes 361. 562 back subsumes 490. 562 back subsumes 271. given clause #24: (wt=13) 533 [para_from,485.1.1,21.1.1.5,demod,9,flip.1] f(x,y,z,u,f(x,y,z,u,e))=e. ----> UNIT CONFLICT at 0.04 sec ----> 615 [binary,613.1,1.1] $F. Length of proof is 6. Level of proof is 5. ---------------- PROOF ---------------- 1 [] f(A1,A2,A3,A4,f(A1,A2,A3,A4,A5))!=A5. 3 [] f(x,y,z,u,v)=f(x,y,z,v,u). 4 [] f(e,e,e,e,e)=e. 7,6 [] f(e,e,e,x,f(e,e,e,x,y))=y. 9,8 [para_into,6.1.1.5,3.1.2] f(e,e,e,x,f(e,e,e,y,x))=y. 12 [para_from,6.1.2,4.1.2,gL-id,gL-id,gL-id,flip.1] f(x,y,z,u,f(e,e,e,u,e))=f(x,y,z,e,e). 21 [para_into,12.1.2,8.1.2,gL-id,gL-id,gL-id,flip.1] f(e,e,e,x,f(y,z,u,f(v,w,v6,e,e),x))=f(v,w,v6,v7,f(y,z,u,v7,e)). 485 [gL,21,flip.1] f(x,y,z,f(x,y,z,e,e),u)=f(e,e,e,e,u). 533 [para_from,485.1.1,21.1.1.5,demod,9,flip.1] f(x,y,z,u,f(x,y,z,u,e))=e. 613 [para_into,533.1.2,6.1.2,gL-id,demod,7] f(x,y,z,u,f(x,y,z,u,v))=v. 615 [binary,613.1,1.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 24 clauses generated 2934 para_from generated 1034 para_into generated 1780 gL rule generated 120 demod & eval rewrites 1745 clauses wt,lit,sk delete 0 tautologies deleted 0 clauses forward subsumed 2402 (subsumed by sos) 666 unit deletions 0 factor simplifications 0 clauses kept 546 new demodulators 67 empty clauses 1 clauses back demodulated 10 clauses back subsumed 30 usable size 21 sos size 485 demodulators size 61 passive size 1 hot size 0 Kbytes malloced 1953 ----------- times (seconds) ----------- user CPU time 0.04 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) That finishes the proof of the theorem. Process 16992 finished Mon Nov 14 15:26:22 2005