----- 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 26056.

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).
end_of_list.

list(sos).
0 [] A^ (A v B)!=A|$Ans(B2).
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=10): 11 [copy,10,demod,6] c(c(A) v c(A v B))!=A|$Ans(B2).
  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).
>>>> Starting back demodulation with 13.

======= 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) 16 [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) 17 [copy,16,flip.1] x v c(x)=c(y) v y.

given clause #7: (wt=9) 24 [para_into,17,7] c(x) v x=c(y) v y.

given clause #8: (wt=10) 11 [copy,10,demod,6] c(c(A) v c(A v B))!=A|$Ans(B2).

given clause #9: (wt=10) 12 [back_demod,3,demod,6] x v c(c(x) v c(y))=x.

given clause #10: (wt=5) 41 [para_into,12,12,demod,8] x v x=x.

given clause #11: (wt=9) 33 [para_into,12,7] x v c(c(x) v y)=x.

----> UNIT CONFLICT at   0.01 sec ----> 54 [binary,53,1] $Ans(B2).

Length of proof is 5.  Level of proof is 4.

---------------- PROOF ----------------

1 [] x=x.
3 [] x v (x^y)=x.
6,5 [] x^y=c(c(x) v c(y)).
8,7 [] c(c(x))=x.
10 [] A^ (A v B)!=A|$Ans(B2).
11 [copy,10,demod,6] c(c(A) v c(A v B))!=A|$Ans(B2).
12 [back_demod,3,demod,6] x v c(c(x) v c(y))=x.
33 [para_into,12,7] x v c(c(x) v y)=x.
50,49 [para_into,33,7] c(x) v c(x v y)=c(x).
53 [back_demod,11,demod,50,8] A!=A|$Ans(B2).
54 [binary,53,1] $Ans(B2).

------------ end of proof -------------


Search stopped by max_proofs option.

============ end of search ============

-------------- statistics -------------
clauses given                 11
clauses generated             56
clauses kept                  37
clauses forward subsumed      52
clauses back subsumed          0
Kbytes malloced              223

----------- times (seconds) -----------
user CPU time          0.01          (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.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 26056 finished Fri Sep 12 16:35:26 2003