E-Darwin 1.4 2011/07/07 (based on Darwin 1.3)


Defaulting to tptp format.
Parsing /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE056.p ...

WATCH: 0.00 CPU 0.01 WC
Calling eprover for clausification ...



Proving  ...


WATCH: 2.99 CPU 3.02 WC

WATCH: 5.99 CPU 6.03 WC

WATCH: 9.00 CPU 9.05 WC

WATCH: 12.00 CPU 12.06 WC

WATCH: 15.01 CPU 15.07 WC

WATCH: 18.03 CPU 18.09 WC

WATCH: 21.03 CPU 21.10 WC

WATCH: 24.04 CPU 24.11 WC

WATCH: 27.05 CPU 27.13 WC

WATCH: 30.06 CPU 30.14 WC

WATCH: 33.06 CPU 33.15 WC

WATCH: 36.07 CPU 36.17 WC

WATCH: 39.08 CPU 39.18 WC

WATCH: 42.09 CPU 42.19 WC
% SZS status Theorem for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE056.p

WATCH: 42.22 CPU 42.35 WC

FINAL WATCH: 42.22 CPU 42.35 WC