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/FEQ005.p ...

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



Proving  ...


WATCH: 2.87 CPU 3.02 WC

WATCH: 5.88 CPU 6.03 WC

WATCH: 8.88 CPU 9.04 WC

WATCH: 11.88 CPU 12.05 WC

WATCH: 14.89 CPU 15.06 WC

WATCH: 17.89 CPU 18.07 WC

WATCH: 20.90 CPU 21.08 WC

WATCH: 23.90 CPU 24.09 WC

WATCH: 26.91 CPU 27.10 WC

WATCH: 29.92 CPU 30.11 WC

WATCH: 32.92 CPU 33.12 WC

WATCH: 35.93 CPU 36.13 WC

WATCH: 38.93 CPU 39.13 WC

WATCH: 41.94 CPU 42.14 WC

WATCH: 44.94 CPU 45.15 WC

WATCH: 47.95 CPU 48.16 WC

WATCH: 50.95 CPU 51.17 WC

WATCH: 53.95 CPU 54.18 WC

WATCH: 56.96 CPU 57.19 WC

WATCH: 59.96 CPU 60.20 WC

WATCH: 62.96 CPU 63.21 WC

WATCH: 65.97 CPU 66.22 WC

WATCH: 68.97 CPU 69.23 WC

WATCH: 71.97 CPU 72.24 WC

WATCH: 74.98 CPU 75.25 WC

WATCH: 77.98 CPU 78.26 WC

WATCH: 80.99 CPU 81.27 WC

WATCH: 83.99 CPU 84.28 WC

WATCH: 87.00 CPU 87.29 WC

WATCH: 90.00 CPU 90.30 WC

WATCH: 93.01 CPU 93.31 WC

WATCH: 96.01 CPU 96.32 WC

WATCH: 99.02 CPU 99.33 WC

WATCH: 102.02 CPU 102.34 WC

WATCH: 105.02 CPU 105.35 WC

WATCH: 108.03 CPU 108.36 WC

WATCH: 111.03 CPU 111.37 WC

WATCH: 114.04 CPU 114.38 WC

WATCH: 117.04 CPU 117.39 WC

WATCH: 120.05 CPU 120.40 WC

WATCH: 123.05 CPU 123.41 WC

WATCH: 126.06 CPU 126.42 WC

WATCH: 129.06 CPU 129.43 WC

WATCH: 132.07 CPU 132.44 WC

WATCH: 135.07 CPU 135.45 WC

WATCH: 138.07 CPU 138.46 WC

WATCH: 141.08 CPU 141.47 WC

WATCH: 144.08 CPU 144.48 WC

WATCH: 147.09 CPU 147.49 WC

WATCH: 150.10 CPU 150.50 WC

WATCH: 153.10 CPU 153.52 WC

WATCH: 156.11 CPU 156.53 WC

WATCH: 159.11 CPU 159.54 WC

WATCH: 162.12 CPU 162.56 WC

WATCH: 165.13 CPU 165.57 WC

WATCH: 168.14 CPU 168.58 WC

WATCH: 171.15 CPU 171.60 WC

WATCH: 174.16 CPU 174.61 WC

WATCH: 177.16 CPU 177.62 WC

WATCH: 180.16 CPU 180.63 WC

WATCH: 183.18 CPU 183.65 WC

WATCH: 186.18 CPU 186.66 WC

WATCH: 189.19 CPU 189.67 WC

WATCH: 192.19 CPU 192.69 WC

WATCH: 195.20 CPU 195.70 WC

WATCH: 198.21 CPU 198.71 WC

WATCH: 201.22 CPU 201.73 WC

WATCH: 204.23 CPU 204.74 WC

WATCH: 207.22 CPU 207.75 WC

WATCH: 210.23 CPU 210.76 WC

WATCH: 213.24 CPU 213.77 WC

WATCH: 216.25 CPU 216.78 WC

WATCH: 219.26 CPU 219.80 WC

WATCH: 222.26 CPU 222.81 WC

WATCH: 225.27 CPU 225.82 WC

WATCH: 228.28 CPU 228.84 WC

WATCH: 231.29 CPU 231.85 WC

WATCH: 234.30 CPU 234.86 WC

WATCH: 237.30 CPU 237.88 WC

WATCH: 240.31 CPU 240.89 WC

WATCH: 243.32 CPU 243.90 WC

WATCH: 246.33 CPU 246.92 WC

WATCH: 249.34 CPU 249.93 WC

WATCH: 252.34 CPU 252.94 WC

WATCH: 255.35 CPU 255.95 WC

WATCH: 258.36 CPU 258.97 WC

WATCH: 261.36 CPU 261.98 WC

WATCH: 264.37 CPU 264.99 WC

WATCH: 267.38 CPU 268.01 WC

WATCH: 270.39 CPU 271.02 WC

WATCH: 273.40 CPU 274.03 WC

WATCH: 276.40 CPU 277.05 WC

WATCH: 279.41 CPU 280.06 WC

WATCH: 282.42 CPU 283.07 WC

WATCH: 285.43 CPU 286.08 WC

WATCH: 288.44 CPU 289.10 WC

WATCH: 291.45 CPU 292.11 WC

WATCH: 294.45 CPU 295.12 WC

WATCH: 297.46 CPU 298.14 WC

WATCH: 300.47 CPU 301.15 WC

FINAL WATCH: 300.47 CPU 301.27 WC