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

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



Proving  ...


WATCH: 2.97 CPU 3.02 WC

WATCH: 5.97 CPU 6.03 WC

WATCH: 8.98 CPU 9.04 WC

WATCH: 11.98 CPU 12.05 WC

WATCH: 14.98 CPU 15.06 WC

WATCH: 17.99 CPU 18.07 WC

WATCH: 20.99 CPU 21.08 WC

WATCH: 24.00 CPU 24.09 WC

WATCH: 27.01 CPU 27.11 WC

WATCH: 30.02 CPU 30.12 WC

WATCH: 33.03 CPU 33.13 WC

WATCH: 36.03 CPU 36.14 WC

WATCH: 39.04 CPU 39.15 WC

WATCH: 42.04 CPU 42.16 WC

WATCH: 45.05 CPU 45.17 WC

WATCH: 48.05 CPU 48.18 WC

WATCH: 51.05 CPU 51.19 WC

WATCH: 54.06 CPU 54.20 WC

WATCH: 57.06 CPU 57.21 WC

WATCH: 60.06 CPU 60.22 WC

WATCH: 63.07 CPU 63.23 WC

WATCH: 66.08 CPU 66.24 WC

WATCH: 69.08 CPU 69.25 WC

WATCH: 72.09 CPU 72.26 WC

WATCH: 75.09 CPU 75.26 WC

WATCH: 78.10 CPU 78.27 WC

WATCH: 81.10 CPU 81.28 WC

WATCH: 84.11 CPU 84.29 WC

WATCH: 87.11 CPU 87.30 WC

WATCH: 90.12 CPU 90.31 WC

WATCH: 93.12 CPU 93.32 WC

WATCH: 96.13 CPU 96.33 WC

WATCH: 99.13 CPU 99.34 WC

WATCH: 102.13 CPU 102.35 WC

WATCH: 105.14 CPU 105.36 WC

WATCH: 108.14 CPU 108.37 WC

WATCH: 111.15 CPU 111.38 WC

WATCH: 114.15 CPU 114.39 WC

WATCH: 117.15 CPU 117.40 WC

WATCH: 120.16 CPU 120.41 WC

WATCH: 123.16 CPU 123.42 WC

WATCH: 126.17 CPU 126.43 WC

WATCH: 129.17 CPU 129.44 WC

WATCH: 132.18 CPU 132.45 WC

WATCH: 135.18 CPU 135.46 WC

WATCH: 138.19 CPU 138.47 WC

WATCH: 141.20 CPU 141.49 WC

WATCH: 144.20 CPU 144.50 WC

WATCH: 147.21 CPU 147.51 WC

WATCH: 150.22 CPU 150.53 WC

WATCH: 153.23 CPU 153.54 WC

WATCH: 156.23 CPU 156.55 WC

WATCH: 159.24 CPU 159.57 WC

WATCH: 162.25 CPU 162.58 WC

WATCH: 165.26 CPU 165.59 WC

WATCH: 168.27 CPU 168.60 WC

WATCH: 171.27 CPU 171.62 WC

WATCH: 174.28 CPU 174.63 WC

WATCH: 177.29 CPU 177.65 WC

WATCH: 180.30 CPU 180.66 WC

WATCH: 183.31 CPU 183.67 WC

WATCH: 186.32 CPU 186.69 WC

WATCH: 189.32 CPU 189.70 WC

WATCH: 192.33 CPU 192.71 WC

WATCH: 195.34 CPU 195.73 WC

WATCH: 198.35 CPU 198.74 WC

WATCH: 201.35 CPU 201.75 WC

WATCH: 204.36 CPU 204.76 WC

WATCH: 207.37 CPU 207.78 WC

WATCH: 210.37 CPU 210.79 WC

WATCH: 213.38 CPU 213.80 WC

WATCH: 216.38 CPU 216.82 WC

WATCH: 219.39 CPU 219.83 WC

WATCH: 222.40 CPU 222.84 WC

WATCH: 225.40 CPU 225.86 WC

WATCH: 228.41 CPU 228.87 WC

WATCH: 231.42 CPU 231.88 WC

WATCH: 234.42 CPU 234.90 WC

WATCH: 237.43 CPU 237.91 WC

WATCH: 240.44 CPU 240.92 WC

WATCH: 243.44 CPU 243.94 WC

WATCH: 246.45 CPU 246.95 WC

WATCH: 249.46 CPU 249.96 WC

WATCH: 252.47 CPU 252.98 WC

WATCH: 255.47 CPU 255.99 WC

WATCH: 258.48 CPU 259.00 WC

WATCH: 261.48 CPU 262.01 WC

WATCH: 264.50 CPU 265.03 WC

WATCH: 267.50 CPU 268.04 WC

WATCH: 270.51 CPU 271.06 WC

WATCH: 273.52 CPU 274.07 WC

WATCH: 276.53 CPU 277.08 WC

WATCH: 279.54 CPU 280.09 WC

WATCH: 282.54 CPU 283.11 WC

WATCH: 285.55 CPU 286.12 WC

WATCH: 288.56 CPU 289.13 WC

WATCH: 291.57 CPU 292.15 WC

WATCH: 294.58 CPU 295.16 WC

WATCH: 297.58 CPU 298.17 WC

WATCH: 300.59 CPU 301.19 WC

FINAL WATCH: 300.59 CPU 301.32 WC