Otter proof of mushrooms example:


otter < mushrooms.in

----- Otter 3.0.4, August 1995 -----
The job was started by keller on turing, Tue Feb 18 12:59:30 1997
The command was "otter".

set(auto).

list(usable).
0 [] -fungus(x)|mushroom(x)|toadstool(x).
0 [] -boletus(x)|fungus(x).
0 [] -toadstool(x)|poisonous(x).
0 [] -boletus(x)| -mushroom(x).
0 [] boletus(this).
0 [] -poisonous(this).
end_of_list.

SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=3.

This is a non-Horn set without equality.  The strategy will
be ordered hyper_res, unit deletion, and factoring, with
satellites in sos with and nuclei in usable.

   dependent: set(hyper_res).
   dependent: set(factor).
   dependent: set(unit_deletion).

------------> process usable:
** KEPT (pick-wt=6): 1 [] -fungus(x)|mushroom(x)|toadstool(x).
** KEPT (pick-wt=4): 2 [] -boletus(x)|fungus(x).
** KEPT (pick-wt=4): 3 [] -toadstool(x)|poisonous(x).
** KEPT (pick-wt=4): 4 [] -boletus(x)| -mushroom(x).
** KEPT (pick-wt=2): 5 [] -poisonous(this).

------------> process sos:
** KEPT (pick-wt=2): 6 [] boletus(this).

======= end of input processing =======

=========== start of search ===========

given clause #1: (wt=2) 6 [] boletus(this).

given clause #2: (wt=2) 7 [hyper,6,2] fungus(this).

given clause #3: (wt=4) 8 [hyper,7,1] mushroom(this)|toadstool(this).

given clause #4: (wt=2) 9 [hyper,8,3,unit_del,5] mushroom(this).

-----> EMPTY CLAUSE at   0.02 sec ----> 10 [hyper,9,4,6] $F.


-------- PROOF -------- 
Length of proof is 3.  Level of proof is 3.

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

1 [] -fungus(x)|mushroom(x)|toadstool(x).
2 [] -boletus(x)|fungus(x).
3 [] -toadstool(x)|poisonous(x).
4 [] -boletus(x)| -mushroom(x).
5 [] -poisonous(this).
6 [] boletus(this).
7 [hyper,6,2] fungus(this).
8 [hyper,7,1] mushroom(this)|toadstool(this).
9 [hyper,8,3,unit_del,5] mushroom(this).
10 [hyper,9,4,6] $F.

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

Search stopped by max_proofs option.

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

-------------- statistics -------------
clauses given                  4
clauses generated              4
clauses kept                   9
clauses forward subsumed       0
clauses back subsumed          1
Kbytes malloced               63

----------- times (seconds) -----------
user CPU time          0.03          (0 hr, 0 min, 0 sec)
system CPU time        0.03          (0 hr, 0 min, 0 sec)
wall-clock time        0             (0 hr, 0 min, 0 sec)
hyper_res time         0.00
for_sub time           0.00
back_sub time          0.00
conflict time          0.00
demod time             0.00

The job finished        Tue Feb 18 12:59:30 1997