----- Otter 3.0.4, August 1995 -----
The job was started by brings on hopfield.phil.rpi.edu, Thu May 27 15:53:25 1999
The command was "otter".

set(auto).
   dependent: set(process_input).
   dependent: clear(print_kept).
   dependent: clear(print_new_demod).
   dependent: clear(print_back_demod).
   dependent: clear(print_back_sub).
   dependent: set(control_memory).
   dependent: assign(max_mem, 12000).
   dependent: assign(pick_given_ratio, 4).
   dependent: assign(stats_level, 1).
   dependent: assign(max_seconds, 10800).

formula_list(usable).
all x y z (American(x)&Weapon(y)&Nation(z)&Hostile(z)&Sells(x,z,y)->Criminal(x)).
exists x (Owns(anono,x)&Missile(x)).
all x (Owns(anono,x)&Missile(x)->Sells(awest,anono,x)).
all x (Missile(x)->Weapon(x)).
all x (Enemy(x,aamerica)->Hostile(x)).
American(awest).
Nation(anono).
Enemy(anono,aamerica).
Nation(aamerica).
-Criminal(awest).
end_of_list.

-------> usable clausifies to:

list(usable).
0 [] -American(x)| -Weapon(y)| -Nation(z)| -Hostile(z)| -Sells(x,z,y)|Criminal(x).
0 [] Owns(anono,$c1).
0 [] Missile($c1).
0 [] -Owns(anono,x)| -Missile(x)|Sells(awest,anono,x).
0 [] -Missile(x)|Weapon(x).
0 [] -Enemy(x,aamerica)|Hostile(x).
0 [] American(awest).
0 [] Nation(anono).
0 [] Enemy(anono,aamerica).
0 [] Nation(aamerica).
0 [] -Criminal(awest).
end_of_list.

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

This is a Horn set without equality.  The strategy will
be hyperresolution, with satellites in sos and nuclei
in usable.

   dependent: set(hyper_res).
   dependent: clear(order_hyper).

------------> process usable:
** KEPT (pick-wt=14): 1 [] -American(x)| -Weapon(y)| -Nation(z)| -Hostile(z)| -Sells(x,z,y)|Criminal(x).
** KEPT (pick-wt=9): 2 [] -Owns(anono,x)| -Missile(x)|Sells(awest,anono,x).
** KEPT (pick-wt=4): 3 [] -Missile(x)|Weapon(x).
** KEPT (pick-wt=5): 4 [] -Enemy(x,aamerica)|Hostile(x).
** KEPT (pick-wt=2): 5 [] -Criminal(awest).

------------> process sos:
** KEPT (pick-wt=3): 6 [] Owns(anono,$c1).
** KEPT (pick-wt=2): 7 [] Missile($c1).
** KEPT (pick-wt=2): 8 [] American(awest).
** KEPT (pick-wt=2): 9 [] Nation(anono).
** KEPT (pick-wt=3): 10 [] Enemy(anono,aamerica).
** KEPT (pick-wt=2): 11 [] Nation(aamerica).

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

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

given clause #1: (wt=3) 6 [] Owns(anono,$c1).

given clause #2: (wt=2) 7 [] Missile($c1).

given clause #3: (wt=2) 8 [] American(awest).

given clause #4: (wt=2) 9 [] Nation(anono).

given clause #5: (wt=2) 11 [] Nation(aamerica).

given clause #6: (wt=3) 10 [] Enemy(anono,aamerica).

given clause #7: (wt=2) 12 [hyper,7,3] Weapon($c1).

given clause #8: (wt=2) 14 [hyper,10,4] Hostile(anono).

given clause #9: (wt=4) 13 [hyper,7,2,6] Sells(awest,anono,$c1).

----> UNIT CONFLICT at   0.04 sec ----> 16 [binary,15.1,5.1] $F.

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

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

1 [] -American(x)| -Weapon(y)| -Nation(z)| -Hostile(z)| -Sells(x,z,y)|Criminal(x).
2 [] -Owns(anono,x)| -Missile(x)|Sells(awest,anono,x).
3 [] -Missile(x)|Weapon(x).
4 [] -Enemy(x,aamerica)|Hostile(x).
5 [] -Criminal(awest).
6 [] Owns(anono,$c1).
7 [] Missile($c1).
8 [] American(awest).
9 [] Nation(anono).
10 [] Enemy(anono,aamerica).
12 [hyper,7,3] Weapon($c1).
13 [hyper,7,2,6] Sells(awest,anono,$c1).
14 [hyper,10,4] Hostile(anono).
15 [hyper,13,1,8,12,9,14] Criminal(awest).
16 [binary,15.1,5.1] $F.

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


Search stopped by max_proofs option.

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

-------------- statistics -------------
clauses given                  9
clauses generated              4
clauses kept                  15
clauses forward subsumed       0
clauses back subsumed          0
Kbytes malloced               95

----------- times (seconds) -----------
user CPU time          0.05          (0 hr, 0 min, 0 sec)
system CPU time        0.15          (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.01
demod time             0.00

The job finished        Thu May 27 15:53:25 1999