WATCH: 0.00 CPU 0.01 WC

WATCH: 2.90 CPU 3.02 WC

WATCH: 5.91 CPU 6.03 WC

WATCH: 8.91 CPU 9.04 WC

WATCH: 11.92 CPU 12.05 WC

WATCH: 14.92 CPU 15.06 WC

WATCH: 17.93 CPU 18.07 WC

WATCH: 20.93 CPU 21.08 WC

WATCH: 23.94 CPU 24.09 WC

WATCH: 26.94 CPU 27.09 WC

WATCH: 29.95 CPU 30.10 WC

WATCH: 32.95 CPU 33.11 WC

WATCH: 35.96 CPU 36.12 WC

WATCH: 38.96 CPU 39.13 WC

WATCH: 41.97 CPU 42.14 WC

WATCH: 44.97 CPU 45.15 WC

WATCH: 47.98 CPU 48.16 WC

WATCH: 50.98 CPU 51.17 WC

WATCH: 53.98 CPU 54.18 WC

WATCH: 56.99 CPU 57.19 WC

WATCH: 59.99 CPU 60.20 WC

WATCH: 63.00 CPU 63.21 WC

WATCH: 66.00 CPU 66.22 WC

WATCH: 69.01 CPU 69.23 WC

WATCH: 72.01 CPU 72.24 WC

WATCH: 75.02 CPU 75.25 WC

WATCH: 78.02 CPU 78.26 WC

WATCH: 81.03 CPU 81.27 WC

WATCH: 84.03 CPU 84.28 WC

WATCH: 87.04 CPU 87.29 WC

WATCH: 90.04 CPU 90.30 WC

WATCH: 93.05 CPU 93.31 WC

WATCH: 96.05 CPU 96.32 WC

Search stopped in tp_alloc by max_mem option.
----- Otter 3.3f, August 2004 -----
The process was started by sutcliff on cl5-011,
Wed Aug  3 14:43:27 2011
The command was "/CW/home-0/sutcliff/Systems/Otter---3.3/otter".  The process ID is 9715.

set(prolog_style_variables).
set(tptp_eq).
set(auto).
   dependent: set(auto1).
   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).
clear(print_given).

formula_list(usable).
-((all B C ((all Z q1(f(Z)))-> (exists X Y (q1(X)& (p1(f(Y))->p1(X)& (r1(Y)->r1(B)&r1(C)))))))& (all A B C (r(B,C)& (all X (s1(X)->p1(X)))& (all X Y (r(X,Y)->q(X,Y)))&s1(B)&s1(A)-> (exists X Y (q(X,Y)&p1(X)))))& ((all X exists Y (p1(X)&q1(Y)))-> (exists Z all Y (r1(Z)|p1(Y))))& ((all X exists Y (a(Y,Y)&a(X,Y)))-> (exists Z a(Z,Z)))& (all A B C (s1(A)& (all X (s1(X)->p1(X)))& (all X Y (r(X,Y)->q(X,Y)))&r(B,C)&s1(B)-> (exists X Y (q(X,Y)&p1(X)))))& (all A B ((all Y (q1(Y)->p1(Y)))-> (exists X ((p1(X)->p1(A))& (q1(X)->p1(B))))))& (all A B ((all Z (q1(Z)->p1(Z)))-> (exists X ((q1(X)->p1(B))& (p1(X)->p1(A))))))& ((exists X (a1(X)->b(X)))-> ((all X a1(X))-> (exists X b(X))))& ((exists X b(X))-> (exists X (b(X)|a1(X))))& ((exists Y X a(X,Y))<-> (exists X Y a(X,Y)))& ((exists Y p1(Y))<-> (exists X p1(X)))& (exists Z all X exists Y ((p(Z,Y)&p(Y,Z)->p(Y,X))& (p(Y,X)-> (exists W p(W,Y)))))& (exists X all Y (p1(X)->p1(Y)))& (all A B exists X Y ((p1(X)->r1(Y))-> (p1(A)->r1(B))))& ((exists X p1(X))-> (exists Y p1(Y)))& ((all X Y p(X,Y))-> (all X p(X,X)))& (a0|b0| (b0<->a0))& ((all X (p1(X)->q1(X)))& (exists Y (q1(Y)->r1(Y)))-> (exists Z (p1(Z)->r1(Z))))& (all B ((all Y ((r1(B)->r1(Y))->p(f(Y),Y)))-> (exists X Y (p(X,Y)& (q(f(B),B)->q(X,Y))))))& (all A B exists X Y ((q1(X)->p(X,A))&q1(A)&q1(B)&r1(A)&r1(B)&s1(A)& (s1(A)->p(X,Y))& (r1(Y)->p(B,Y))->p(A,B)))& (a0&b0-> (b0<->a0))& (all A ((g0|f0)& (all X (p1(X)&q1(X)))->q1(A)))& (p1(z)->p1(z))& ((exists X all Y p(X,Y))-> (all Y exists X p(X,Y)))& (exists Y ((exists X p1(X))->p1(Y)))& (all B (r1(B)& (all X (p1(X)->q1(X)))-> ((all Y (r1(Y)->p1(Y)))->q1(B))))& (all A B ((all Y (q1(Y)->p1(Y)))-> (exists X ((q1(X)->p1(B))& (p1(X)->p1(A))))))& ((all X Y ((all Z (a_member_of(Z,Y)<->a_member_of(Z,X)))<->eq(X,Y)))-> (all A B (eq(A,B)->eq(B,A))))& ((exists X p1(X))-> (exists Z p1(Z)))& ((all X p1(X))-> (all Y p1(Y))& (all X p1(X)))& (all A B ((all X p1(X))->p1(B)&p1(A)))& ((exists X a1(X))& (all X b(X))-> (exists X (b(X)&a1(X))))& -(exists Y all X (a(X,Y)<-> -a(X,X)))& ((all X (a1(X)->b(X)))-> ((exists X a1(X))-> (exists X b(X))))& ((all X (p1(X)->q1(X)))-> ((all X p1(X))-> (all X q1(X))))& ((all X p1(X))-> (exists Y p1(Y)))& ((exists X p1(X))-> (a0-> (b0| -b0)& (q0->q0))& (exists X p1(X)))& ((exists Y q1(Y))& (all X p1(X))-> (exists Z all Y (r1(Z)|p1(Y))))& ((all X p1(X))-> (all A B (p1(A)&p1(B))))& (all A exists X X2 X3 X4 Y (p1(A)&e(A)& (e(X)->s(X,f(X))|g(X))& (e(X2)->c(f(X2))|g(X2))& (s(A,Y)->p1(Y))->p1(X3)&g(X3)|p1(X4)&c(X4)))& (-(all X (a1(X)->b(X)))& (all X (a1(X)->b(X)|c(X)))-> (exists X (c(X)&a1(X))))& (all B C (q1(f(B))-> (exists X Y ((p1(f(Y))-> (r1(Y)->r1(B)&r1(C))&p1(X))&q1(X)))))& (all C B ((all Z q1(f(Z)))-> (exists X Y ((p1(f(Y))->p1(X))& (r1(Y)->r1(B)&r1(C))&q1(X)))))).
end_of_list.

Search stopped in tp_alloc by max_mem option.

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

-------------- statistics -------------
clauses given                  0
clauses generated              0
clauses kept                   0
clauses forward subsumed       0
clauses back subsumed          0
Kbytes malloced            11718

----------- times (seconds) -----------
user CPU time         98.25          (0 hr, 1 min, 38 sec)
system CPU time        0.00          (0 hr, 0 min, 0 sec)
wall-clock time       99             (0 hr, 1 min, 39 sec)

Process 9715 finished Wed Aug  3 14:45:06 2011
Otter interrupted
PROOF NOT FOUND

WATCH: 98.45 CPU 98.75 WC

FINAL WATCH: 98.45 CPU 98.75 WC