----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Fri Sep 12 16:34:53 2003 The command was "otter". The process ID is 26010. include("ortholattice-header"). ------- start included file ortholattice-header------- op(400,infix,^). op(400,infix,v). lex([A,B,C,D,0,1,x v x,c(x),x^x,f(x,x)]). 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(process_input). dependent: set(lrpo). assign(pick_given_ratio,3). assign(max_weight,25). clear(detailed_history). assign(max_seconds,60). assign(max_mem,100000). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). clear(print_kept). assign(stats_level,1). list(usable). 0 [] x=x. end_of_list. ------- end included file ortholattice-header------- list(sos). 0 [] x v (y v z)=y v (x v z). 0 [] x v (x^y)=x. 0 [] x^y=c(c(x) v c(y)). 0 [] c(c(x))=x. 0 [] x v c(x)=y v c(y). 0 [] f(x,y)=c(x) v c(y). end_of_list. lex([A,B,C,D,0,1,f(x,x),x v x,c(x),x^x]). assign(max_proofs,6). list(passive). 1 [] f(A,f(f(B,C),f(B,C)))!=f(B,f(f(A,C),f(A,C)))|$Ans(SS). 2 [] f(f(A,A),f(A,B))!=A|$Ans(SS). 3 [] f(A,f(A,A))!=f(B,f(B,B))|$Ans(SS). 4 [] A v B!=f(f(A,A),f(B,B))|$Ans(J). 5 [] A^B!=f(f(A,B),f(A,B))|$Ans(M). 6 [] c(A)!=f(A,A)|$Ans(C). end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 7 [] x=x. Following clause subsumed by 7 during input processing: 0 [copy,7,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=11): 8 [] x v (y v z)=y v (x v z). ** KEPT (pick-wt=7): 9 [] x v (x^y)=x. ---> New Demodulator: 10 [new_demod,9] x v (x^y)=x. ** KEPT (pick-wt=10): 11 [] x^y=c(c(x) v c(y)). ---> New Demodulator: 12 [new_demod,11] x^y=c(c(x) v c(y)). ** KEPT (pick-wt=5): 13 [] c(c(x))=x. ---> New Demodulator: 14 [new_demod,13] c(c(x))=x. ** KEPT (pick-wt=9): 15 [] x v c(x)=y v c(y). ** KEPT (pick-wt=9): 17 [copy,16,flip.1] c(x) v c(y)=f(x,y). ---> New Demodulator: 18 [new_demod,17] c(x) v c(y)=f(x,y). Following clause subsumed by 8 during input processing: 0 [copy,8,flip.1] x v (y v z)=y v (x v z). >>>> Starting back demodulation with 10. >>>> Starting back demodulation with 12. >> back demodulating 9 with 12. >>>> Starting back demodulation with 14. Following clause subsumed by 15 during input processing: 0 [copy,15,flip.1] x v c(x)=y v c(y). >>>> Starting back demodulation with 18. >> back demodulating 11 with 18. >>>> Starting back demodulation with 20. >>>> Starting back demodulation with 22. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=11) 8 [] x v (y v z)=y v (x v z). given clause #2: (wt=5) 13 [] c(c(x))=x. given clause #3: (wt=8) 19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. given clause #4: (wt=8) 21 [back_demod,11,demod,18] x^y=c(f(x,y)). given clause #5: (wt=9) 15 [] x v c(x)=y v c(y). given clause #6: (wt=9) 17 [copy,16,flip.1] c(x) v c(y)=f(x,y). given clause #7: (wt=9) 27 [para_into,15,13] c(x) v x=y v c(y). given clause #8: (wt=9) 28 [copy,27,flip.1] x v c(x)=c(y) v y. given clause #9: (wt=15) 23 [para_into,8,8] x v (y v (z v u))=z v (x v (y v u)). given clause #10: (wt=9) 31 [para_into,17,13] x v c(y)=f(c(x),y). given clause #11: (wt=8) 77 [para_into,31,19,flip.1] f(c(x),f(x,y))=x. ----> UNIT CONFLICT at 0.01 sec ----> 87 [binary,85,6] $Ans(C). Length of proof is 5. Level of proof is 4. ---------------- PROOF ---------------- 6 [] c(A)!=f(A,A)|$Ans(C). 9 [] x v (x^y)=x. 12,11 [] x^y=c(c(x) v c(y)). 14,13 [] c(c(x))=x. 16 [] f(x,y)=c(x) v c(y). 18,17 [copy,16,flip.1] c(x) v c(y)=f(x,y). 19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. 31 [para_into,17,13] x v c(y)=f(c(x),y). 77 [para_into,31,19,flip.1] f(c(x),f(x,y))=x. 85 [para_into,77,77,demod,14,flip.1] c(x)=f(x,x). 87 [binary,85,6] $Ans(C). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.01 sec ----> 95 [binary,93,4] $Ans(J). Length of proof is 8. Level of proof is 5. ---------------- PROOF ---------------- 4 [] A v B!=f(f(A,A),f(B,B))|$Ans(J). 9 [] x v (x^y)=x. 12,11 [] x^y=c(c(x) v c(y)). 14,13 [] c(c(x))=x. 16 [] f(x,y)=c(x) v c(y). 18,17 [copy,16,flip.1] c(x) v c(y)=f(x,y). 19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. 31 [para_into,17,13] x v c(y)=f(c(x),y). 75 [para_into,31,13] x v y=f(c(x),c(y)). 77 [para_into,31,19,flip.1] f(c(x),f(x,y))=x. 79 [copy,75,flip.1] f(c(x),c(y))=x v y. 86,85 [para_into,77,77,demod,14,flip.1] c(x)=f(x,x). 93 [back_demod,79,demod,86,86,flip.1] x v y=f(f(x,x),f(y,y)). 95 [binary,93,4] $Ans(J). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.01 sec ----> 98 [binary,96,2] $Ans(SS). Length of proof is 6. Level of proof is 5. ---------------- PROOF ---------------- 2 [] f(f(A,A),f(A,B))!=A|$Ans(SS). 9 [] x v (x^y)=x. 12,11 [] x^y=c(c(x) v c(y)). 14,13 [] c(c(x))=x. 16 [] f(x,y)=c(x) v c(y). 18,17 [copy,16,flip.1] c(x) v c(y)=f(x,y). 19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. 31 [para_into,17,13] x v c(y)=f(c(x),y). 77 [para_into,31,19,flip.1] f(c(x),f(x,y))=x. 86,85 [para_into,77,77,demod,14,flip.1] c(x)=f(x,x). 96 [back_demod,77,demod,86] f(f(x,x),f(x,y))=x. 98 [binary,96,2] $Ans(SS). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.01 sec ----> 101 [binary,100,3] $Ans(SS). Length of proof is 14. Level of proof is 6. ---------------- PROOF ---------------- 3 [] f(A,f(A,A))!=f(B,f(B,B))|$Ans(SS). 9 [] x v (x^y)=x. 12,11 [] x^y=c(c(x) v c(y)). 14,13 [] c(c(x))=x. 15 [] x v c(x)=y v c(y). 16 [] f(x,y)=c(x) v c(y). 18,17 [copy,16,flip.1] c(x) v c(y)=f(x,y). 19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. 27 [para_into,15,13] c(x) v x=y v c(y). 28 [copy,27,flip.1] x v c(x)=c(y) v y. 31 [para_into,17,13] x v c(y)=f(c(x),y). 48 [para_into,28,17] f(x,c(x))=c(y) v y. 49 [copy,48,flip.1] c(x) v x=f(y,c(y)). 75 [para_into,31,13] x v y=f(c(x),c(y)). 77 [para_into,31,19,flip.1] f(c(x),f(x,y))=x. 79 [copy,75,flip.1] f(c(x),c(y))=x v y. 86,85 [para_into,77,77,demod,14,flip.1] c(x)=f(x,x). 94,93 [back_demod,79,demod,86,86,flip.1] x v y=f(f(x,x),f(y,y)). 97,96 [back_demod,77,demod,86] f(f(x,x),f(x,y))=x. 100 [back_demod,49,demod,86,94,97,86] f(x,f(x,x))=f(y,f(y,y)). 101 [binary,100,3] $Ans(SS). ------------ end of proof ------------- ----> UNIT CONFLICT at 0.01 sec ----> 110 [binary,108,5] $Ans(M). Length of proof is 7. Level of proof is 5. ---------------- PROOF ---------------- 5 [] A^B!=f(f(A,B),f(A,B))|$Ans(M). 9 [] x v (x^y)=x. 12,11 [] x^y=c(c(x) v c(y)). 14,13 [] c(c(x))=x. 16 [] f(x,y)=c(x) v c(y). 18,17 [copy,16,flip.1] c(x) v c(y)=f(x,y). 19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. 21 [back_demod,11,demod,18] x^y=c(f(x,y)). 31 [para_into,17,13] x v c(y)=f(c(x),y). 77 [para_into,31,19,flip.1] f(c(x),f(x,y))=x. 86,85 [para_into,77,77,demod,14,flip.1] c(x)=f(x,x). 108 [back_demod,21,demod,86] x^y=f(f(x,y),f(x,y)). 110 [binary,108,5] $Ans(M). ------------ end of proof ------------- given clause #12: (wt=6) 85 [para_into,77,77,demod,14,flip.1] c(x)=f(x,x). given clause #13: (wt=11) 93 [back_demod,79,demod,86,86,flip.1] x v y=f(f(x,x),f(y,y)). given clause #14: (wt=9) 96 [back_demod,77,demod,86] f(f(x,x),f(x,y))=x. given clause #15: (wt=11) 99 [back_demod,76,demod,86,94,97,86] f(x,f(x,x))=f(f(y,y),y). given clause #16: (wt=11) 100 [back_demod,49,demod,86,94,97,86] f(x,f(x,x))=f(y,f(y,y)). given clause #17: (wt=11) 102 [back_demod,43,demod,86,94,97,86] f(f(x,x),x)=f(f(y,y),y). given clause #18: (wt=11) 105 [back_demod,35,demod,86,94,97,86] f(f(x,x),x)=f(y,f(y,y)). given clause #19: (wt=11) 106 [back_demod,33,demod,86,86] f(x,f(f(x,x),y))=f(x,x). given clause #20: (wt=11) 108 [back_demod,21,demod,86] x^y=f(f(x,y),f(x,y)). given clause #21: (wt=25) 103 [back_demod,40,demod,86,86,94,97,94,97,94] f(x,f(f(f(y,y),z),f(f(y,y),z)))=f(f(y,y),f(f(x,z),f(x,z))). ----> UNIT CONFLICT at 0.02 sec ----> 120 [binary,119,1] $Ans(SS). Length of proof is 13. Level of proof is 7. ---------------- PROOF ---------------- 1 [] f(A,f(f(B,C),f(B,C)))!=f(B,f(f(A,C),f(A,C)))|$Ans(SS). 8 [] x v (y v z)=y v (x v z). 9 [] x v (x^y)=x. 12,11 [] x^y=c(c(x) v c(y)). 14,13 [] c(c(x))=x. 16 [] f(x,y)=c(x) v c(y). 18,17 [copy,16,flip.1] c(x) v c(y)=f(x,y). 19 [back_demod,9,demod,12,18] x v c(f(x,y))=x. 31 [para_into,17,13] x v c(y)=f(c(x),y). 39 [para_from,17,8] x v f(y,z)=c(y) v (x v c(z)). 40 [copy,39,flip.1] c(x) v (y v c(z))=y v f(x,z). 75 [para_into,31,13] x v y=f(c(x),c(y)). 77 [para_into,31,19,flip.1] f(c(x),f(x,y))=x. 79 [copy,75,flip.1] f(c(x),c(y))=x v y. 86,85 [para_into,77,77,demod,14,flip.1] c(x)=f(x,x). 94,93 [back_demod,79,demod,86,86,flip.1] x v y=f(f(x,x),f(y,y)). 97,96 [back_demod,77,demod,86] f(f(x,x),f(x,y))=x. 103 [back_demod,40,demod,86,86,94,97,94,97,94] f(x,f(f(f(y,y),z),f(f(y,y),z)))=f(f(y,y),f(f(x,z),f(x,z))). 119 [para_into,103,96,demod,97,97] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 120 [binary,119,1] $Ans(SS). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 21 clauses generated 124 clauses kept 90 clauses forward subsumed 141 clauses back subsumed 0 Kbytes malloced 287 ----------- times (seconds) ----------- user CPU time 0.02 (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) para_into time 0.00 para_from time 0.01 for_sub time 0.00 back_sub time 0.00 conflict time 0.00 demod time 0.00 That finishes the proof of the theorem. Process 26010 finished Fri Sep 12 16:34:53 2003