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


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

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



Proving  ...


WATCH: 2.98 CPU 3.02 WC

WATCH: 5.98 CPU 6.04 WC

WATCH: 8.99 CPU 9.05 WC

WATCH: 12.00 CPU 12.06 WC

WATCH: 15.01 CPU 15.08 WC

WATCH: 18.02 CPU 18.09 WC

WATCH: 21.02 CPU 21.10 WC

WATCH: 24.03 CPU 24.12 WC

WATCH: 27.04 CPU 27.13 WC

WATCH: 30.05 CPU 30.14 WC

WATCH: 33.05 CPU 33.15 WC

WATCH: 36.06 CPU 36.17 WC

WATCH: 39.07 CPU 39.18 WC

WATCH: 42.08 CPU 42.19 WC

WATCH: 45.08 CPU 45.20 WC

WATCH: 48.09 CPU 48.21 WC

WATCH: 51.09 CPU 51.22 WC

WATCH: 54.09 CPU 54.23 WC

WATCH: 57.10 CPU 57.24 WC

WATCH: 60.10 CPU 60.25 WC

WATCH: 63.11 CPU 63.27 WC

WATCH: 66.12 CPU 66.28 WC

WATCH: 69.13 CPU 69.29 WC

WATCH: 72.13 CPU 72.31 WC

WATCH: 75.14 CPU 75.32 WC

WATCH: 78.15 CPU 78.33 WC

WATCH: 81.16 CPU 81.34 WC

WATCH: 84.17 CPU 84.36 WC

WATCH: 87.17 CPU 87.37 WC

WATCH: 90.18 CPU 90.38 WC

WATCH: 93.19 CPU 93.40 WC

WATCH: 96.20 CPU 96.41 WC

WATCH: 99.21 CPU 99.42 WC

WATCH: 102.21 CPU 102.44 WC

WATCH: 105.22 CPU 105.45 WC

WATCH: 108.23 CPU 108.46 WC

WATCH: 111.23 CPU 111.48 WC

WATCH: 114.24 CPU 114.49 WC

WATCH: 117.25 CPU 117.50 WC

WATCH: 120.26 CPU 120.52 WC

WATCH: 123.27 CPU 123.53 WC

WATCH: 126.27 CPU 126.54 WC

WATCH: 129.28 CPU 129.55 WC

WATCH: 132.29 CPU 132.57 WC

WATCH: 135.30 CPU 135.58 WC

WATCH: 138.31 CPU 138.59 WC

WATCH: 141.31 CPU 141.61 WC

WATCH: 144.32 CPU 144.62 WC

WATCH: 147.33 CPU 147.63 WC

WATCH: 150.34 CPU 150.65 WC

WATCH: 153.35 CPU 153.66 WC

WATCH: 156.35 CPU 156.67 WC

WATCH: 159.36 CPU 159.69 WC

WATCH: 162.37 CPU 162.70 WC

WATCH: 165.37 CPU 165.71 WC

WATCH: 168.38 CPU 168.73 WC

WATCH: 171.39 CPU 171.74 WC

WATCH: 174.40 CPU 174.75 WC

WATCH: 177.41 CPU 177.76 WC

WATCH: 180.41 CPU 180.78 WC

WATCH: 183.42 CPU 183.79 WC

WATCH: 186.43 CPU 186.80 WC

WATCH: 189.45 CPU 189.82 WC

WATCH: 192.45 CPU 192.83 WC

WATCH: 195.46 CPU 195.84 WC

WATCH: 198.47 CPU 198.86 WC

WATCH: 201.48 CPU 201.87 WC

WATCH: 204.49 CPU 204.88 WC

WATCH: 207.49 CPU 207.89 WC

WATCH: 210.50 CPU 210.91 WC

WATCH: 213.51 CPU 213.92 WC

WATCH: 216.51 CPU 216.94 WC

WATCH: 219.52 CPU 219.95 WC

WATCH: 222.53 CPU 222.96 WC

WATCH: 225.54 CPU 225.97 WC

WATCH: 228.55 CPU 228.99 WC

WATCH: 231.56 CPU 232.00 WC

WATCH: 234.56 CPU 235.01 WC

WATCH: 237.57 CPU 238.03 WC

WATCH: 240.58 CPU 241.04 WC

WATCH: 243.58 CPU 244.05 WC

WATCH: 246.59 CPU 247.07 WC

WATCH: 249.60 CPU 250.08 WC

WATCH: 252.61 CPU 253.09 WC

WATCH: 255.62 CPU 256.11 WC

WATCH: 258.62 CPU 259.12 WC

WATCH: 261.63 CPU 262.13 WC

WATCH: 264.64 CPU 265.14 WC

WATCH: 267.64 CPU 268.16 WC

WATCH: 270.65 CPU 271.17 WC

WATCH: 273.66 CPU 274.18 WC

WATCH: 276.67 CPU 277.20 WC

WATCH: 279.68 CPU 280.21 WC

WATCH: 282.68 CPU 283.22 WC

WATCH: 285.69 CPU 286.24 WC

WATCH: 288.70 CPU 289.25 WC

WATCH: 291.71 CPU 292.26 WC

WATCH: 294.72 CPU 295.28 WC

WATCH: 297.73 CPU 298.29 WC

WATCH: 300.73 CPU 301.30 WC

FINAL WATCH: 300.73 CPU 301.42 WC