----- 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 thm5.in". The process ID is 16997. % Reading file thm5.in. op(400,xfx,*). set(para_from). set(para_into). set(para_from_vars). set(para_into_vars). set(order_eq). assign(pick_given_ratio,4). clear(print_kept). clear(print_new_demod). clear(print_back_demod). assign(max_mem,30000). assign(max_weight,17). assign(max_weight,1). set(hyper_res). set(para_from_units_only). set(para_into_units_only). list(usable). 1 [] x=x. 2 [] g(x1,x2,x3,x4,x5)!=f(x1,x2,x3,x4,x5)|g(x2,x3,x4,x5,x1)=f(x2,x3,x4,x5,x1). end_of_list. list(sos). 3 [] f(e,e,e,e,e)=e. 4 [] f(u,v,w,x,f(u,v,w,x,y))=y. 5 [] g(e,e,e,e,e)=e. 6 [] g(u,v,w,x,g(u,v,w,x,y))=y. 7 [] f(x,y,z,u,g(v,w,v6,u,v7))=f(x,y,z,v8,g(v,w,v6,v8,v7)). end_of_list. list(passive). 8 [] g(A,B,C,D,E)!=f(A,B,C,D,E). end_of_list. weight_list(pick_given). weight(e,10). weight(x,9). weight(f($(1),$(1),$(1),$(1),$(1)),10). weight(g($(1),$(1),$(1),$(1),$(1)),10). weight($(1)=$(1),10). end_of_list. weight_list(purge_gen). weight(x,0). weight(e,0). weight(g($(1),$(1),$(1),$(1),$(1))=f($(1),$(1),$(1),$(1),$(1)),1). weight(f($(1),$(1),$(1),$(1),g($(1),$(1),$(1),$(1),$(1)))=$(1),1). end_of_list. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=80) 3 [] f(e,e,e,e,e)=e. given clause #2: (wt=80) 5 [] g(e,e,e,e,e)=e. given clause #3: (wt=120) 4 [] f(u,v,w,x,f(u,v,w,x,y))=y. given clause #4: (wt=120) 6 [] g(u,v,w,x,g(u,v,w,x,y))=y. given clause #5: (wt=130) 9 [para_into,5.1.2,3.1.2] g(e,e,e,e,e)=f(e,e,e,e,e). given clause #6: (wt=212) 7 [] f(x,y,z,u,g(v,w,v6,u,v7))=f(x,y,z,v8,g(v,w,v6,v8,v7)). given clause #7: (wt=130) 10 [para_from,5.1.2,3.1.1.5] f(e,e,e,e,g(e,e,e,e,e))=e. 11 back subsumes 10. given clause #8: (wt=128) 11 [para_into,10.1.1,7.1.2] f(e,e,e,x,g(e,e,e,x,e))=e. 12 back subsumes 9. given clause #9: (wt=128) 12 [para_from,11.1.1,4.1.1.5,flip.1] g(e,e,e,x,e)=f(e,e,e,x,e). given clause #10: (wt=128) 13 [hyper,12,2] g(e,e,x,e,e)=f(e,e,x,e,e). given clause #11: (wt=128) 14 [hyper,13,2] g(e,x,e,e,e)=f(e,x,e,e,e). given clause #12: (wt=128) 15 [para_from,13.1.2,4.1.1.5] f(e,e,x,e,g(e,e,x,e,e))=e. 18 back subsumes 15. 18 back subsumes 11. given clause #13: (wt=126) 18 [para_into,15.1.1,7.1.2] f(e,e,x,y,g(e,e,x,y,e))=e. 19 back subsumes 13. 19 back subsumes 12. given clause #14: (wt=126) 19 [para_from,18.1.1,4.1.1.5,flip.1] g(e,e,x,y,e)=f(e,e,x,y,e). 20 back subsumes 14. given clause #15: (wt=126) 20 [hyper,19,2] g(e,x,y,e,e)=f(e,x,y,e,e). 21 back subsumes 16. 22 back subsumes 17. given clause #16: (wt=126) 21 [hyper,20,2] g(x,y,e,e,e)=f(x,y,e,e,e). given clause #17: (wt=126) 22 [para_from,20.1.2,4.1.1.5] f(e,x,y,e,g(e,x,y,e,e))=e. 25 back subsumes 22. 25 back subsumes 18. given clause #18: (wt=124) 25 [para_into,22.1.1,7.1.2] f(e,x,y,z,g(e,x,y,z,e))=e. 26 back subsumes 20. 26 back subsumes 19. given clause #19: (wt=124) 26 [para_from,25.1.1,4.1.1.5,flip.1] g(e,x,y,z,e)=f(e,x,y,z,e). 27 back subsumes 21. given clause #20: (wt=124) 27 [hyper,26,2] g(x,y,z,e,e)=f(x,y,z,e,e). 28 back subsumes 23. 29 back subsumes 24. given clause #21: (wt=124) 28 [hyper,27,2] g(x,y,e,e,z)=f(x,y,e,e,z). given clause #22: (wt=124) 29 [para_from,27.1.2,4.1.1.5] f(x,y,z,e,g(x,y,z,e,e))=e. 32 back subsumes 29. 32 back subsumes 25. given clause #23: (wt=122) 32 [para_into,29.1.1,7.1.2] f(x,y,z,u,g(x,y,z,u,e))=e. 33 back subsumes 27. 33 back subsumes 26. given clause #24: (wt=122) 33 [para_from,32.1.1,4.1.1.5,flip.1] g(x,y,z,u,e)=f(x,y,z,u,e). 34 back subsumes 28. given clause #25: (wt=122) 34 [hyper,33,2] g(x,y,z,e,u)=f(x,y,z,e,u). 35 back subsumes 30. 36 back subsumes 31. given clause #26: (wt=122) 35 [hyper,34,2] g(x,y,e,z,u)=f(x,y,e,z,u). given clause #27: (wt=122) 36 [para_into,34.1.1,6.1.1,flip.1] f(x,y,z,e,g(x,y,z,e,u))=u. 39 back subsumes 38. 39 back subsumes 36. 39 back subsumes 32. given clause #28: (wt=120) 39 [para_into,36.1.1,7.1.2] f(x,y,z,u,g(x,y,z,u,v))=v. ----> UNIT CONFLICT at 0.03 sec ----> 41 [binary,40.1,8.1] $F. Length of proof is 19. Level of proof is 19. ---------------- PROOF ---------------- 2 [] g(x1,x2,x3,x4,x5)!=f(x1,x2,x3,x4,x5)|g(x2,x3,x4,x5,x1)=f(x2,x3,x4,x5,x1). 3 [] f(e,e,e,e,e)=e. 4 [] f(u,v,w,x,f(u,v,w,x,y))=y. 5 [] g(e,e,e,e,e)=e. 6 [] g(u,v,w,x,g(u,v,w,x,y))=y. 7 [] f(x,y,z,u,g(v,w,v6,u,v7))=f(x,y,z,v8,g(v,w,v6,v8,v7)). 8 [] g(A,B,C,D,E)!=f(A,B,C,D,E). 10 [para_from,5.1.2,3.1.1.5] f(e,e,e,e,g(e,e,e,e,e))=e. 11 [para_into,10.1.1,7.1.2] f(e,e,e,x,g(e,e,e,x,e))=e. 12 [para_from,11.1.1,4.1.1.5,flip.1] g(e,e,e,x,e)=f(e,e,e,x,e). 13 [hyper,12,2] g(e,e,x,e,e)=f(e,e,x,e,e). 15 [para_from,13.1.2,4.1.1.5] f(e,e,x,e,g(e,e,x,e,e))=e. 18 [para_into,15.1.1,7.1.2] f(e,e,x,y,g(e,e,x,y,e))=e. 19 [para_from,18.1.1,4.1.1.5,flip.1] g(e,e,x,y,e)=f(e,e,x,y,e). 20 [hyper,19,2] g(e,x,y,e,e)=f(e,x,y,e,e). 22 [para_from,20.1.2,4.1.1.5] f(e,x,y,e,g(e,x,y,e,e))=e. 25 [para_into,22.1.1,7.1.2] f(e,x,y,z,g(e,x,y,z,e))=e. 26 [para_from,25.1.1,4.1.1.5,flip.1] g(e,x,y,z,e)=f(e,x,y,z,e). 27 [hyper,26,2] g(x,y,z,e,e)=f(x,y,z,e,e). 29 [para_from,27.1.2,4.1.1.5] f(x,y,z,e,g(x,y,z,e,e))=e. 32 [para_into,29.1.1,7.1.2] f(x,y,z,u,g(x,y,z,u,e))=e. 33 [para_from,32.1.1,4.1.1.5,flip.1] g(x,y,z,u,e)=f(x,y,z,u,e). 34 [hyper,33,2] g(x,y,z,e,u)=f(x,y,z,e,u). 36 [para_into,34.1.1,6.1.1,flip.1] f(x,y,z,e,g(x,y,z,e,u))=u. 39 [para_into,36.1.1,7.1.2] f(x,y,z,u,g(x,y,z,u,v))=v. 40 [para_into,39.1.1.5,6.1.1,flip.1] g(x,y,z,u,v)=f(x,y,z,u,v). 41 [binary,40.1,8.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 28 clauses generated 5388 hyper_res generated 13 para_from generated 2230 para_into generated 3145 demod & eval rewrites 0 clauses wt,lit,sk delete 5296 tautologies deleted 0 clauses forward subsumed 60 (subsumed by sos) 13 unit deletions 0 factor simplifications 0 clauses kept 32 new demodulators 0 empty clauses 1 clauses back demodulated 0 clauses back subsumed 26 usable size 11 sos size 2 demodulators size 0 passive size 1 hot size 0 Kbytes malloced 976 ----------- times (seconds) ----------- user CPU time 0.03 (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 16997 finished Mon Nov 14 15:26:22 2005