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

set(binary_res).
   dependent: set(factor).
   dependent: set(unit_deletion).
set(lex_order_vars).
assign(max_given,1).

lex([a,b,c,d,e,f(x),add(x,x)]).

special_unary([neg(x)]).

list(usable).
1 [] -dum|P1(add(c,add(add(a,b),add(e,d)))).
2 [] -dum|P2(add(neg(c),add(add(neg(a),neg(b)),add(neg(e),neg(d))))).
3 [] -dum|P3(add(c,add(add(a,neg(b)),add(e,neg(d))))).
4 [] -dum|P4(add(add(neg(a),b),add(neg(b),add(add(b,neg(b)),add(a,b))))).
5 [] -dum|P5(add(x,add(add(c,add(add(a,neg(y)),neg(b))),add(f(y),b)))).
end_of_list.

list(sos).
6 [] dum.
end_of_list.

list(demodulators).
7 [] EQ(add(x,y),add(y,x)).
8 [] EQ(add(x,add(y,z)),add(y,add(x,z))).
9 [] EQ(add(add(x,y),z),add(x,add(y,z))).
end_of_list.
lex dependent demodulator: 7 [] EQ(add(x,y),add(y,x)).
lex dependent demodulator: 8 [] EQ(add(x,add(y,z)),add(y,add(x,z))).

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

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

given clause #1: (wt=1) 6 [] dum.

Search stopped by max_given option.

** KEPT (pick-wt=17): 10 [binary,6.1,5.1,demod,7,7,8,7,8,8,7,7,8,7,8,8,8,7,8,8] P5(add(x,add(neg(y),add(a,add(b,add(neg(b),add(c,f(y)))))))).
** KEPT (pick-wt=17): 11 [binary,6.1,4.1,demod,7,8,7,8,7,8,8,8,8,7,8,7,8,8] P4(add(a,add(neg(a),add(b,add(b,add(b,add(neg(b),neg(b)))))))).
** KEPT (pick-wt=12): 12 [binary,6.1,3.1,demod,7,8,7,8,7,8,8,8,8] P3(add(a,add(neg(b),add(c,add(neg(d),e))))).
** KEPT (pick-wt=15): 13 [binary,6.1,2.1,demod,7,8,7,8,7,8,8,8,8] P2(add(neg(a),add(neg(b),add(neg(c),add(neg(d),neg(e)))))).
** KEPT (pick-wt=10): 14 [binary,6.1,1.1,demod,7,8,7,8,7,8,8,8,8] P1(add(a,add(b,add(c,add(d,e))))).

Search stopped by max_given option.

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

-------------- statistics -------------
clauses given                  1
clauses generated              5
  binary_res generated         5
  factors generated            0
demod & eval rewrites         57
clauses wt,lit,sk delete       0
tautologies deleted            0
clauses forward subsumed       0
  (subsumed by sos)            0
unit deletions                 0
factor simplifications         0
clauses kept                   5
new demodulators               0
empty clauses                  0
clauses back demodulated       0
clauses back subsumed          0
usable size                    6
sos size                       5
demodulators size              3
passive size                   0
hot size                       0
Kbytes malloced              976

----------- times (seconds) -----------
user CPU time          0.00          (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)

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