----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Fri Sep 12 16:35:26 2003 The command was "otter". The process ID is 26052. 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------- assign(max_proofs,2). list(sos). 0 [] x v (y v z)=y v (x v z). 0 [] x^ (y^z)=y^ (x^z). 0 [] x v (x^y)=x. 0 [] x^ (x v y)=x. end_of_list. list(passive). 1 [] A v B!=B v A|$Ans(CJ). 2 [] A v A!=A|$Ans(IJ). end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 3 [] x=x. Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=11): 4 [] x v (y v z)=y v (x v z). ** KEPT (pick-wt=11): 5 [] x^ (y^z)=y^ (x^z). ** KEPT (pick-wt=7): 6 [] x v (x^y)=x. ---> New Demodulator: 7 [new_demod,6] x v (x^y)=x. ** KEPT (pick-wt=7): 8 [] x^ (x v y)=x. ---> New Demodulator: 9 [new_demod,8] x^ (x v y)=x. Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] x v (y v z)=y v (x v z). Following clause subsumed by 5 during input processing: 0 [copy,5,flip.1] x^ (y^z)=y^ (x^z). >>>> Starting back demodulation with 7. >>>> Starting back demodulation with 9. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=11) 4 [] x v (y v z)=y v (x v z). given clause #2: (wt=7) 6 [] x v (x^y)=x. given clause #3: (wt=7) 8 [] x^ (x v y)=x. ----> UNIT CONFLICT at 0.00 sec ----> 20 [binary,18,2] $Ans(IJ). Length of proof is 1. Level of proof is 1. ---------------- PROOF ---------------- 2 [] A v A!=A|$Ans(IJ). 6 [] x v (x^y)=x. 8 [] x^ (x v y)=x. 18 [para_from,8,6] x v x=x. 20 [binary,18,2] $Ans(IJ). ------------ end of proof ------------- given clause #4: (wt=5) 14 [para_into,8,6] x^x=x. given clause #5: (wt=11) 5 [] x^ (y^z)=y^ (x^z). given clause #6: (wt=5) 18 [para_from,8,6] x v x=x. given clause #7: (wt=9) 16 [para_into,8,4] x^ (y v (x v z))=x. given clause #8: (wt=7) 35 [para_into,16,18] x^ (y v x)=x. given clause #9: (wt=15) 10 [para_into,4,4] x v (y v (z v u))=z v (x v (y v u)). given clause #10: (wt=9) 21 [para_into,5,14,flip.1] x^ (y^x)=y^x. given clause #11: (wt=7) 66 [para_into,21,35,demod,36] (x v y)^y=y. given clause #12: (wt=7) 70 [para_into,21,8,demod,9] (x v y)^x=x. given clause #13: (wt=15) 11 [copy,10,flip.1] x v (y v (z v u))=y v (z v (x v u)). given clause #14: (wt=7) 74 [para_from,21,6] x v (y^x)=x. given clause #15: (wt=9) 29 [para_from,5,6] x v (y^ (x^z))=x. given clause #16: (wt=9) 33 [para_from,18,4,flip.1] x v (y v x)=y v x. given clause #17: (wt=11) 12 [para_from,6,4,flip.1] x v (y v (x^z))=y v x. ----> UNIT CONFLICT at 0.01 sec ----> 170 [binary,169,1] $Ans(CJ). Length of proof is 5. Level of proof is 4. ---------------- PROOF ---------------- 1 [] A v B!=B v A|$Ans(CJ). 4 [] x v (y v z)=y v (x v z). 5 [] x^ (y^z)=y^ (x^z). 6 [] x v (x^y)=x. 8 [] x^ (x v y)=x. 12 [para_from,6,4,flip.1] x v (y v (x^z))=y v x. 14 [para_into,8,6] x^x=x. 21 [para_into,5,14,flip.1] x^ (y^x)=y^x. 74 [para_from,21,6] x v (y^x)=x. 169 [para_into,12,74] x v y=y v x. 170 [binary,169,1] $Ans(CJ). ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 17 clauses generated 217 clauses kept 104 clauses forward subsumed 162 clauses back subsumed 0 Kbytes malloced 319 ----------- times (seconds) ----------- user CPU time 0.01 (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 26052 finished Fri Sep 12 16:35:26 2003