----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Fri Sep 12 16:35:27 2003 The command was "otter". The process ID is 26067. 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 [] x v (y^ (x v z))=x v (z^ (x v y)). 0 [] A v (c(A)^ (A v B))!=A v B|$Ans(OM). end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 1 [] x=x. Following clause subsumed by 1 during input processing: 0 [copy,1,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=11): 2 [] x v (y v z)=y v (x v z). ** KEPT (pick-wt=7): 3 [] x v (x^y)=x. ---> New Demodulator: 4 [new_demod,3] x v (x^y)=x. ** KEPT (pick-wt=10): 5 [] x^y=c(c(x) v c(y)). ---> New Demodulator: 6 [new_demod,5] x^y=c(c(x) v c(y)). ** KEPT (pick-wt=5): 7 [] c(c(x))=x. ---> New Demodulator: 8 [new_demod,7] c(c(x))=x. ** KEPT (pick-wt=9): 9 [] x v c(x)=y v c(y). ** KEPT (pick-wt=21): 11 [copy,10,demod,6,6] x v c(c(y) v c(x v z))=x v c(c(z) v c(x v y)). ** KEPT (pick-wt=13): 13 [copy,12,demod,6,8] A v c(A v c(A v B))!=A v B|$Ans(OM). Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] x v (y v z)=y v (x v z). >>>> Starting back demodulation with 4. >>>> Starting back demodulation with 6. >> back demodulating 3 with 6. >>>> Starting back demodulation with 8. Following clause subsumed by 9 during input processing: 0 [copy,9,flip.1] x v c(x)=y v c(y). Following clause subsumed by 11 during input processing: 0 [copy,11,flip.1] x v c(c(y) v c(x v z))=x v c(c(z) v c(x v y)). >>>> Starting back demodulation with 15. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=11) 2 [] x v (y v z)=y v (x v z). given clause #2: (wt=5) 7 [] c(c(x))=x. given clause #3: (wt=9) 9 [] x v c(x)=y v c(y). given clause #4: (wt=9) 18 [para_into,9,7] c(x) v x=y v c(y). given clause #5: (wt=10) 5 [] x^y=c(c(x) v c(y)). given clause #6: (wt=9) 19 [copy,18,flip.1] x v c(x)=c(y) v y. given clause #7: (wt=9) 26 [para_into,19,7] c(x) v x=c(y) v y. given clause #8: (wt=10) 14 [back_demod,3,demod,6] x v c(c(x) v c(y))=x. given clause #9: (wt=21) 11 [copy,10,demod,6,6] x v c(c(y) v c(x v z))=x v c(c(z) v c(x v y)). ----> UNIT CONFLICT at 0.00 sec ----> 52 [binary,50,13] $Ans(OM). Length of proof is 7. Level of proof is 4. ---------------- PROOF ---------------- 3 [] x v (x^y)=x. 6,5 [] x^y=c(c(x) v c(y)). 8,7 [] c(c(x))=x. 9 [] x v c(x)=y v c(y). 10 [] x v (y^ (x v z))=x v (z^ (x v y)). 11 [copy,10,demod,6,6] x v c(c(y) v c(x v z))=x v c(c(z) v c(x v y)). 12 [] A v (c(A)^ (A v B))!=A v B|$Ans(OM). 13 [copy,12,demod,6,8] A v c(A v c(A v B))!=A v B|$Ans(OM). 14 [back_demod,3,demod,6] x v c(c(x) v c(y))=x. 18 [para_into,9,7] c(x) v x=y v c(y). 19 [copy,18,flip.1] x v c(x)=c(y) v y. 40,39 [para_into,14,19] x v c(c(y) v y)=x. 50 [para_into,11,19,demod,40,8,8,flip.1] x v c(x v c(x v y))=x v y. 52 [binary,50,13] $Ans(OM). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 9 clauses generated 45 clauses kept 36 clauses forward subsumed 42 clauses back subsumed 0 Kbytes malloced 223 ----------- times (seconds) ----------- user CPU time 0.00 (0 hr, 0 min, 0 sec) system CPU time 0.01 (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.00 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 26067 finished Fri Sep 12 16:35:27 2003