----- Otter 3.3f, August 2004 -----
The process was started by mccune on gyro.thornwood,
Mon Aug  2 15:31:14 2004
The command was "../../bin/otter".  The process ID is 8907.

set(para_from).
set(para_into).
set(para_from_vars).
set(order_eq).
set(geometric_rule).
set(geometric_rewrite_before).
set(lrpo).

lex([a,b,f(x,x,x)]).
assign(max_mem,1500).
clear(print_kept).
clear(print_back_sub).

list(usable).
1 [] x=x.
end_of_list.

list(sos).
2 [] f(x,x,y)=x.
3 [] f(x,y,x)=x.
4 [] f(y,x,x)=x.
end_of_list.

list(passive).
5 [] a!=b.
end_of_list.

======= end of input processing =======

=========== start of search ===========

given clause #1: (wt=6) 2 [] f(x,x,y)=x.

given clause #2: (wt=6) 3 [] f(x,y,x)=x.

given clause #3: (wt=6) 4 [] f(y,x,x)=x.

given clause #4: (wt=12) 6 [para_into,2.1.1,2.1.2] f(f(x,x,y),f(x,x,y),z)=x.

given clause #5: (wt=18) 16 [para_into,6.1.1.1,6.1.1,gL-id] f(x,f(f(y,y,z),f(y,y,z),u),v)=f(x,y,z).

given clause #6: (wt=6) 65 [para_into,16.1.1,3.1.1,flip.1] f(x,y,z)=x.

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

----> UNIT CONFLICT at   0.01 sec ----> 83 [binary,82.1,5.1] $F.

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

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

2 [] f(x,x,y)=x.
3 [] f(x,y,x)=x.
4 [] f(y,x,x)=x.
5 [] a!=b.
6 [para_into,2.1.1,2.1.2] f(f(x,x,y),f(x,x,y),z)=x.
16 [para_into,6.1.1.1,6.1.1,gL-id] f(x,f(f(y,y,z),f(y,y,z),u),v)=f(x,y,z).
65 [para_into,16.1.1,3.1.1,flip.1] f(x,y,z)=x.
82 [para_into,65.1.1,4.1.1] x=y.
83 [binary,82.1,5.1] $F.

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


Search stopped by max_proofs option.


Search stopped by max_proofs option.

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

-------------- statistics -------------
clauses given                  6
clauses generated            138
  para_from generated         42
  para_into generated         94
  gL rule generated            2
demod & eval rewrites          0
clauses wt,lit,sk delete       0
tautologies deleted            0
clauses forward subsumed      61
  (subsumed by sos)           34
unit deletions                 0
factor simplifications         0
clauses kept                  77
new demodulators               0
empty clauses                  1
clauses back demodulated       0
clauses back subsumed          7
usable size                    5
sos size                      69
demodulators size              0
passive size                   1
hot size                       0
Kbytes malloced              976

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

That finishes the proof of the theorem.

Process 8907 finished Mon Aug  2 15:31:14 2004