----- Otter 3.3, August 2003 -----
The process was started by mccune on gyro.thornwood,
Wed Aug  6 14:25:57 2003
The command was "../../bin/otter".  The process ID is 5912.

set(hyper_res).
set(print_lists_at_end).
assign(stats_level,1).

list(usable).
1 [] P(A).
2 [] P(B).
3 [] P(C).
4 [] P(D).
end_of_list.

list(sos).
5 [] -P(x)| -P(y)|NE(x,y).
end_of_list.

list(passive).
6 [] NE(x,x).
end_of_list.

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

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

given clause #1: (wt=7) 5 [] -P(x)| -P(y)|NE(x,y).
** KEPT (pick-wt=3): 7 [hyper,5,4,3] NE(D,C).
** KEPT (pick-wt=3): 8 [hyper,5,4,2] NE(D,B).
** KEPT (pick-wt=3): 9 [hyper,5,4,1] NE(D,A).
** KEPT (pick-wt=3): 10 [hyper,5,3,4] NE(C,D).
** KEPT (pick-wt=3): 11 [hyper,5,3,2] NE(C,B).
** KEPT (pick-wt=3): 12 [hyper,5,3,1] NE(C,A).
** KEPT (pick-wt=3): 13 [hyper,5,2,4] NE(B,D).
** KEPT (pick-wt=3): 14 [hyper,5,2,3] NE(B,C).
** KEPT (pick-wt=3): 15 [hyper,5,2,1] NE(B,A).
** KEPT (pick-wt=3): 16 [hyper,5,1,4] NE(A,D).
** KEPT (pick-wt=3): 17 [hyper,5,1,3] NE(A,C).
** KEPT (pick-wt=3): 18 [hyper,5,1,2] NE(A,B).

given clause #2: (wt=3) 7 [hyper,5,4,3] NE(D,C).

given clause #3: (wt=3) 8 [hyper,5,4,2] NE(D,B).

given clause #4: (wt=3) 9 [hyper,5,4,1] NE(D,A).

given clause #5: (wt=3) 10 [hyper,5,3,4] NE(C,D).

given clause #6: (wt=3) 11 [hyper,5,3,2] NE(C,B).

given clause #7: (wt=3) 12 [hyper,5,3,1] NE(C,A).

given clause #8: (wt=3) 13 [hyper,5,2,4] NE(B,D).

given clause #9: (wt=3) 14 [hyper,5,2,3] NE(B,C).

given clause #10: (wt=3) 15 [hyper,5,2,1] NE(B,A).

given clause #11: (wt=3) 16 [hyper,5,1,4] NE(A,D).

given clause #12: (wt=3) 17 [hyper,5,1,3] NE(A,C).

given clause #13: (wt=3) 18 [hyper,5,1,2] NE(A,B).

Search stopped because sos empty.


Search stopped because sos empty.

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

list(usable).
1 [] P(A).
2 [] P(B).
3 [] P(C).
4 [] P(D).
5 [] -P(x)| -P(y)|NE(x,y).
7 [hyper,5,4,3] NE(D,C).
8 [hyper,5,4,2] NE(D,B).
9 [hyper,5,4,1] NE(D,A).
10 [hyper,5,3,4] NE(C,D).
11 [hyper,5,3,2] NE(C,B).
12 [hyper,5,3,1] NE(C,A).
13 [hyper,5,2,4] NE(B,D).
14 [hyper,5,2,3] NE(B,C).
15 [hyper,5,2,1] NE(B,A).
16 [hyper,5,1,4] NE(A,D).
17 [hyper,5,1,3] NE(A,C).
18 [hyper,5,1,2] NE(A,B).
end_of_list.

list(sos).
end_of_list.

list(demodulators).
end_of_list.


-------------- statistics -------------
clauses given                 13
clauses generated             16
clauses kept                  12
clauses forward subsumed       4
clauses back subsumed          0
Kbytes malloced              191

----------- 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)
hyper_res time         0.00
for_sub time           0.00
back_sub time          0.00
conflict time          0.00

Process 5912 finished Wed Aug  6 14:25:57 2003