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


Defaulting to tptp format.
Parsing /CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ061.p ...
Parsing /CW/home-0/sutcliff/TPTP/Axioms/KLE001+6.ax ...
Parsing /CW/home-0/sutcliff/TPTP/Axioms/KLE001+4.ax ...
Parsing /CW/home-0/sutcliff/TPTP/Axioms/KLE001+0.ax ...
Calling eprover for clausification ...



Proving  ...


WATCH: 2.94 CPU 3.02 WC

WATCH: 5.95 CPU 6.03 WC

WATCH: 8.95 CPU 9.04 WC

WATCH: 11.95 CPU 12.05 WC

WATCH: 14.96 CPU 15.06 WC

WATCH: 17.97 CPU 18.07 WC

WATCH: 20.97 CPU 21.08 WC

WATCH: 23.97 CPU 24.09 WC

WATCH: 26.98 CPU 27.10 WC

WATCH: 29.98 CPU 30.11 WC

WATCH: 32.99 CPU 33.12 WC

WATCH: 35.99 CPU 36.13 WC

WATCH: 39.00 CPU 39.14 WC

WATCH: 42.00 CPU 42.15 WC

WATCH: 45.01 CPU 45.16 WC

WATCH: 48.01 CPU 48.17 WC

WATCH: 51.02 CPU 51.18 WC

WATCH: 54.01 CPU 54.19 WC

WATCH: 57.03 CPU 57.20 WC

WATCH: 60.03 CPU 60.21 WC

WATCH: 63.03 CPU 63.22 WC

WATCH: 66.04 CPU 66.23 WC

WATCH: 69.04 CPU 69.24 WC

WATCH: 72.05 CPU 72.25 WC

WATCH: 75.05 CPU 75.26 WC

WATCH: 78.06 CPU 78.27 WC

WATCH: 81.06 CPU 81.28 WC

WATCH: 84.06 CPU 84.29 WC

WATCH: 87.07 CPU 87.30 WC

WATCH: 90.07 CPU 90.30 WC

WATCH: 93.08 CPU 93.32 WC

WATCH: 96.10 CPU 96.34 WC

WATCH: 99.12 CPU 99.36 WC

WATCH: 102.12 CPU 102.37 WC

WATCH: 105.12 CPU 105.38 WC

WATCH: 108.13 CPU 108.39 WC

WATCH: 111.13 CPU 111.40 WC

WATCH: 114.14 CPU 114.41 WC

WATCH: 117.14 CPU 117.42 WC

WATCH: 120.15 CPU 120.43 WC

WATCH: 123.15 CPU 123.45 WC

WATCH: 126.16 CPU 126.46 WC

WATCH: 129.17 CPU 129.47 WC

WATCH: 132.19 CPU 132.49 WC

WATCH: 135.19 CPU 135.50 WC

WATCH: 138.21 CPU 138.52 WC

WATCH: 141.22 CPU 141.53 WC

WATCH: 144.22 CPU 144.54 WC

WATCH: 147.23 CPU 147.56 WC

WATCH: 150.23 CPU 150.57 WC

WATCH: 153.24 CPU 153.58 WC

WATCH: 156.24 CPU 156.59 WC

WATCH: 159.25 CPU 159.61 WC

WATCH: 162.26 CPU 162.62 WC

WATCH: 165.27 CPU 165.64 WC

WATCH: 168.27 CPU 168.65 WC

WATCH: 171.28 CPU 171.67 WC

WATCH: 174.29 CPU 174.68 WC

WATCH: 177.30 CPU 177.70 WC

WATCH: 180.32 CPU 180.72 WC

WATCH: 183.33 CPU 183.73 WC

WATCH: 186.33 CPU 186.75 WC

WATCH: 189.35 CPU 189.76 WC

WATCH: 192.36 CPU 192.78 WC

WATCH: 195.36 CPU 195.79 WC

WATCH: 198.37 CPU 198.80 WC

WATCH: 201.38 CPU 201.82 WC

WATCH: 204.39 CPU 204.84 WC

WATCH: 207.40 CPU 207.85 WC

WATCH: 210.41 CPU 210.86 WC

WATCH: 213.42 CPU 213.88 WC

WATCH: 216.43 CPU 216.89 WC

WATCH: 219.44 CPU 219.91 WC

WATCH: 222.45 CPU 222.92 WC

WATCH: 225.45 CPU 225.93 WC

WATCH: 228.46 CPU 228.94 WC

WATCH: 231.46 CPU 231.95 WC

WATCH: 234.47 CPU 234.96 WC

WATCH: 237.47 CPU 237.97 WC

WATCH: 240.47 CPU 240.98 WC

WATCH: 243.48 CPU 243.99 WC

WATCH: 246.49 CPU 247.00 WC

WATCH: 249.50 CPU 250.02 WC

WATCH: 252.50 CPU 253.03 WC

WATCH: 255.51 CPU 256.04 WC

WATCH: 258.52 CPU 259.05 WC

WATCH: 261.51 CPU 262.06 WC

WATCH: 264.52 CPU 265.07 WC

WATCH: 267.53 CPU 268.08 WC

WATCH: 270.53 CPU 271.09 WC

WATCH: 273.54 CPU 274.10 WC

WATCH: 276.55 CPU 277.11 WC

WATCH: 279.55 CPU 280.12 WC

WATCH: 282.56 CPU 283.14 WC

WATCH: 285.57 CPU 286.15 WC

WATCH: 288.58 CPU 289.16 WC

WATCH: 291.58 CPU 292.17 WC

WATCH: 294.58 CPU 295.18 WC

WATCH: 297.59 CPU 298.19 WC

WATCH: 300.59 CPU 301.20 WC

FINAL WATCH: 300.59 CPU 301.36 WC