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/FEQ073.p ...
Parsing /CW/home-0/sutcliff/TPTP/Axioms/KLE002+0.ax ...

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



Proving  ...


WATCH: 2.96 CPU 3.02 WC

WATCH: 5.97 CPU 6.03 WC

WATCH: 8.98 CPU 9.05 WC

WATCH: 11.99 CPU 12.06 WC

WATCH: 14.99 CPU 15.07 WC

WATCH: 17.99 CPU 18.08 WC

WATCH: 21.00 CPU 21.09 WC

WATCH: 24.01 CPU 24.10 WC

WATCH: 27.01 CPU 27.11 WC

WATCH: 30.02 CPU 30.12 WC

WATCH: 33.02 CPU 33.13 WC

WATCH: 36.03 CPU 36.14 WC

WATCH: 39.03 CPU 39.15 WC

WATCH: 42.04 CPU 42.16 WC

WATCH: 45.04 CPU 45.17 WC

WATCH: 48.05 CPU 48.18 WC

WATCH: 51.05 CPU 51.19 WC

WATCH: 54.05 CPU 54.20 WC

WATCH: 57.06 CPU 57.21 WC

WATCH: 60.07 CPU 60.22 WC

WATCH: 63.07 CPU 63.23 WC

WATCH: 66.07 CPU 66.24 WC

WATCH: 69.08 CPU 69.25 WC

WATCH: 72.09 CPU 72.27 WC

WATCH: 75.09 CPU 75.27 WC

WATCH: 78.10 CPU 78.28 WC

WATCH: 81.10 CPU 81.30 WC

WATCH: 84.11 CPU 84.31 WC

WATCH: 87.12 CPU 87.32 WC

WATCH: 90.13 CPU 90.33 WC

WATCH: 93.13 CPU 93.34 WC

WATCH: 96.13 CPU 96.35 WC

WATCH: 99.14 CPU 99.36 WC

WATCH: 102.14 CPU 102.37 WC

WATCH: 105.15 CPU 105.38 WC

WATCH: 108.15 CPU 108.39 WC

WATCH: 111.16 CPU 111.40 WC

WATCH: 114.16 CPU 114.41 WC

WATCH: 117.16 CPU 117.42 WC

WATCH: 120.17 CPU 120.43 WC

WATCH: 123.17 CPU 123.44 WC

WATCH: 126.18 CPU 126.45 WC

WATCH: 129.18 CPU 129.46 WC

WATCH: 132.19 CPU 132.47 WC

WATCH: 135.19 CPU 135.48 WC

WATCH: 138.20 CPU 138.49 WC

WATCH: 141.20 CPU 141.50 WC

WATCH: 144.21 CPU 144.51 WC

WATCH: 147.21 CPU 147.52 WC

WATCH: 150.22 CPU 150.53 WC

WATCH: 153.22 CPU 153.54 WC

WATCH: 156.22 CPU 156.55 WC

WATCH: 159.23 CPU 159.56 WC

WATCH: 162.24 CPU 162.58 WC

WATCH: 165.25 CPU 165.59 WC

WATCH: 168.26 CPU 168.61 WC

WATCH: 171.28 CPU 171.63 WC

WATCH: 174.29 CPU 174.64 WC

WATCH: 177.30 CPU 177.66 WC

WATCH: 180.30 CPU 180.67 WC

WATCH: 183.31 CPU 183.68 WC

WATCH: 186.32 CPU 186.69 WC

WATCH: 189.32 CPU 189.70 WC

WATCH: 192.33 CPU 192.71 WC

WATCH: 195.33 CPU 195.72 WC

WATCH: 198.34 CPU 198.73 WC

WATCH: 201.35 CPU 201.75 WC

WATCH: 204.35 CPU 204.76 WC

WATCH: 207.35 CPU 207.76 WC

WATCH: 210.36 CPU 210.78 WC

WATCH: 213.37 CPU 213.79 WC

WATCH: 216.37 CPU 216.80 WC

WATCH: 219.38 CPU 219.82 WC

WATCH: 222.40 CPU 222.83 WC

WATCH: 225.41 CPU 225.85 WC

WATCH: 228.42 CPU 228.86 WC

WATCH: 231.42 CPU 231.87 WC

WATCH: 234.44 CPU 234.89 WC

WATCH: 237.45 CPU 237.91 WC

WATCH: 240.46 CPU 240.92 WC

WATCH: 243.47 CPU 243.94 WC

WATCH: 246.48 CPU 246.96 WC

WATCH: 249.49 CPU 249.97 WC

WATCH: 252.50 CPU 252.99 WC

WATCH: 255.51 CPU 256.00 WC

WATCH: 258.51 CPU 259.02 WC

WATCH: 261.53 CPU 262.03 WC

WATCH: 264.53 CPU 265.05 WC

WATCH: 267.55 CPU 268.06 WC

WATCH: 270.55 CPU 271.07 WC

WATCH: 273.55 CPU 274.08 WC

WATCH: 276.56 CPU 277.09 WC

WATCH: 279.57 CPU 280.10 WC

WATCH: 282.57 CPU 283.11 WC

WATCH: 285.57 CPU 286.12 WC

WATCH: 288.58 CPU 289.13 WC

WATCH: 291.58 CPU 292.14 WC

WATCH: 294.59 CPU 295.15 WC

WATCH: 297.59 CPU 298.16 WC

WATCH: 300.60 CPU 301.17 WC

FINAL WATCH: 300.60 CPU 301.32 WC