----- 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 lem2.in". The process ID is 16993. % Reading file lem2.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,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(x,y,z,u,v)=f(x,y,z,v,u). 4 [] f(u,v,w,x,f(u,v,w,x,y))=y. 5 [] g(x,y,z,u,v)=g(x,y,z,v,u). 6 [] g(e,e,e,e,e)=e. 7 [] g(u,v,w,x,g(u,v,w,x,y))=y. end_of_list. list(passive). 8 [] f(A,B,C,X,g(H,I,J,X,N))!=f(A,B,C,Y,g(H,I,J,Y,N)). 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(f($(1),$(1),$(1),$(1),g($(1),$(1),$(1),$(1),g($(1),$(1),$(1),$(1),$(1))))=f($(1),$(1),$(1),$(1),g($(1),$(1),$(1),$(1),$(1))),1). weight(f($(1),$(1),$(1),$(1),g($(1),$(1),$(1),$(1),$(1)))=f($(1),$(1),$(1),$(1),g($(1),$(1),$(1),$(1),$(1))),1). weight(f($(1),$(1),$(1),$(1),g($(1),$(1),$(1),$(1),$(1)))=f($(1),$(1),$(1),$(1),$(1)),1). 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=120) 3 [] f(x,y,z,u,v)=f(x,y,z,v,u). given clause #2: (wt=80) 6 [] 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) 5 [] g(x,y,z,u,v)=g(x,y,z,v,u). given clause #5: (wt=120) 7 [] g(u,v,w,x,g(u,v,w,x,y))=y. given clause #6: (wt=172) 9 [para_from,6.1.1,3.1.2.4] f(x,y,z,u,g(e,e,e,e,e))=f(x,y,z,e,u). given clause #7: (wt=172) 11 [para_into,9.1.2,3.1.2] f(x,y,z,u,g(e,e,e,e,e))=f(x,y,z,u,e). given clause #8: (wt=264) 10 [para_into,9.1.1.4,7.1.1,flip.1] f(x,y,z,e,g(u,v,w,v6,g(u,v,w,v6,v7)))=f(x,y,z,v7,g(e,e,e,e,e)). given clause #9: (wt=264) 14 [gL,10] f(x,y,z,e,g(u,v,w,v6,g(e,v,w,v6,v7)))=f(x,y,z,v7,g(u,e,e,e,e)). given clause #10: (wt=264) 12 [para_into,11.1.2.5,7.1.2,flip.1] f(x,y,z,u,g(v,w,v6,v7,g(v,w,v6,v7,e)))=f(x,y,z,u,g(e,e,e,e,e)). given clause #11: (wt=264) 13 [para_into,10.1.1.5.5,5.1.2] f(x,y,z,e,g(u,v,w,v6,g(u,v,w,v7,v6)))=f(x,y,z,v7,g(e,e,e,e,e)). given clause #12: (wt=264) 15 [gL,10] f(x,y,z,e,g(u,v,w,v6,g(u,e,w,v6,v7)))=f(x,y,z,v7,g(e,v,e,e,e)). given clause #13: (wt=264) 16 [gL,10] f(x,y,z,e,g(u,v,w,v6,g(u,v,e,v6,v7)))=f(x,y,z,v7,g(e,e,w,e,e)). given clause #14: (wt=264) 17 [gL,10] f(x,y,z,e,g(u,v,w,v6,g(u,v,w,e,v7)))=f(x,y,z,v7,g(e,e,e,v6,e)). given clause #15: (wt=214) 33 [para_into,17.1.1,13.1.1,gL-id,gL-id,gL-id,gL-id] f(x,y,z,e,g(u,v,w,e,v6))=f(x,y,z,v7,g(u,v,w,v7,v6)). ----> UNIT CONFLICT at 0.08 sec ----> 41 [binary,40.1,8.1] $F. Length of proof is 6. Level of proof is 5. ---------------- PROOF ---------------- 3 [] f(x,y,z,u,v)=f(x,y,z,v,u). 5 [] g(x,y,z,u,v)=g(x,y,z,v,u). 6 [] g(e,e,e,e,e)=e. 7 [] g(u,v,w,x,g(u,v,w,x,y))=y. 8 [] f(A,B,C,X,g(H,I,J,X,N))!=f(A,B,C,Y,g(H,I,J,Y,N)). 9 [para_from,6.1.1,3.1.2.4] f(x,y,z,u,g(e,e,e,e,e))=f(x,y,z,e,u). 10 [para_into,9.1.1.4,7.1.1,flip.1] f(x,y,z,e,g(u,v,w,v6,g(u,v,w,v6,v7)))=f(x,y,z,v7,g(e,e,e,e,e)). 13 [para_into,10.1.1.5.5,5.1.2] f(x,y,z,e,g(u,v,w,v6,g(u,v,w,v7,v6)))=f(x,y,z,v7,g(e,e,e,e,e)). 17 [gL,10] f(x,y,z,e,g(u,v,w,v6,g(u,v,w,e,v7)))=f(x,y,z,v7,g(e,e,e,v6,e)). 33 [para_into,17.1.1,13.1.1,gL-id,gL-id,gL-id,gL-id] f(x,y,z,e,g(u,v,w,e,v6))=f(x,y,z,v7,g(u,v,w,v7,v6)). 40 [para_into,33.1.1,33.1.1] f(x,y,z,u,g(v,w,v6,u,v7))=f(x,y,z,v8,g(v,w,v6,v8,v7)). 41 [binary,40.1,8.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 15 clauses generated 6027 hyper_res generated 0 para_from generated 2307 para_into generated 3643 gL rule generated 77 demod & eval rewrites 0 clauses wt,lit,sk delete 5791 tautologies deleted 0 clauses forward subsumed 204 (subsumed by sos) 32 unit deletions 0 factor simplifications 0 clauses kept 32 new demodulators 0 empty clauses 1 clauses back demodulated 0 clauses back subsumed 0 usable size 17 sos size 22 demodulators size 0 passive size 1 hot size 0 Kbytes malloced 976 ----------- times (seconds) ----------- user CPU time 0.08 (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 16993 finished Mon Nov 14 15:26:22 2005