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

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



Proving  ...


WATCH: 2.98 CPU 3.02 WC

WATCH: 6.00 CPU 6.04 WC

WATCH: 9.01 CPU 9.05 WC

WATCH: 12.01 CPU 12.06 WC

WATCH: 15.02 CPU 15.07 WC

WATCH: 18.02 CPU 18.08 WC

WATCH: 21.03 CPU 21.09 WC

WATCH: 24.03 CPU 24.10 WC

WATCH: 27.04 CPU 27.11 WC

WATCH: 30.04 CPU 30.12 WC

WATCH: 33.04 CPU 33.13 WC

WATCH: 36.05 CPU 36.14 WC

WATCH: 39.05 CPU 39.15 WC

WATCH: 42.06 CPU 42.16 WC

WATCH: 45.07 CPU 45.17 WC

WATCH: 48.07 CPU 48.18 WC

WATCH: 51.07 CPU 51.19 WC

WATCH: 54.08 CPU 54.20 WC

WATCH: 57.08 CPU 57.21 WC

WATCH: 60.08 CPU 60.22 WC

WATCH: 63.09 CPU 63.23 WC

WATCH: 66.10 CPU 66.24 WC

WATCH: 69.10 CPU 69.25 WC

WATCH: 72.10 CPU 72.26 WC

WATCH: 75.11 CPU 75.27 WC

WATCH: 78.12 CPU 78.28 WC

WATCH: 81.12 CPU 81.29 WC

WATCH: 84.12 CPU 84.30 WC

WATCH: 87.13 CPU 87.31 WC

WATCH: 90.14 CPU 90.32 WC

WATCH: 93.14 CPU 93.33 WC

WATCH: 96.15 CPU 96.34 WC

WATCH: 99.15 CPU 99.35 WC

WATCH: 102.16 CPU 102.36 WC

WATCH: 105.16 CPU 105.37 WC

WATCH: 108.16 CPU 108.38 WC

WATCH: 111.16 CPU 111.39 WC

WATCH: 114.17 CPU 114.40 WC

WATCH: 117.17 CPU 117.41 WC

WATCH: 120.17 CPU 120.42 WC

WATCH: 123.18 CPU 123.43 WC

WATCH: 126.19 CPU 126.44 WC

WATCH: 129.19 CPU 129.45 WC

WATCH: 132.20 CPU 132.46 WC

WATCH: 135.20 CPU 135.46 WC

WATCH: 138.21 CPU 138.47 WC

WATCH: 141.21 CPU 141.48 WC

WATCH: 144.21 CPU 144.49 WC

WATCH: 147.22 CPU 147.50 WC

WATCH: 150.23 CPU 150.51 WC

WATCH: 153.23 CPU 153.52 WC

WATCH: 156.23 CPU 156.53 WC

WATCH: 159.24 CPU 159.54 WC

WATCH: 162.24 CPU 162.55 WC

WATCH: 165.25 CPU 165.56 WC

WATCH: 168.25 CPU 168.57 WC

WATCH: 171.26 CPU 171.58 WC

WATCH: 174.26 CPU 174.59 WC

WATCH: 177.27 CPU 177.60 WC

WATCH: 180.27 CPU 180.61 WC

WATCH: 183.28 CPU 183.62 WC

WATCH: 186.28 CPU 186.63 WC

WATCH: 189.29 CPU 189.64 WC

WATCH: 192.29 CPU 192.65 WC

WATCH: 195.30 CPU 195.66 WC

WATCH: 198.30 CPU 198.67 WC

WATCH: 201.30 CPU 201.68 WC

WATCH: 204.31 CPU 204.70 WC

WATCH: 207.32 CPU 207.71 WC

WATCH: 210.32 CPU 210.72 WC

WATCH: 213.33 CPU 213.74 WC

WATCH: 216.34 CPU 216.75 WC

WATCH: 219.35 CPU 219.76 WC

WATCH: 222.36 CPU 222.78 WC

WATCH: 225.37 CPU 225.79 WC

WATCH: 228.37 CPU 228.80 WC

WATCH: 231.38 CPU 231.82 WC

WATCH: 234.39 CPU 234.83 WC

WATCH: 237.40 CPU 237.84 WC

WATCH: 240.41 CPU 240.85 WC

WATCH: 243.41 CPU 243.87 WC

WATCH: 246.42 CPU 246.88 WC

WATCH: 249.43 CPU 249.89 WC

WATCH: 252.44 CPU 252.91 WC

WATCH: 255.45 CPU 255.92 WC

WATCH: 258.45 CPU 258.93 WC

WATCH: 261.46 CPU 261.95 WC

WATCH: 264.47 CPU 264.96 WC

WATCH: 267.48 CPU 267.97 WC

WATCH: 270.48 CPU 270.99 WC

WATCH: 273.49 CPU 273.99 WC

WATCH: 276.50 CPU 277.00 WC

WATCH: 279.50 CPU 280.01 WC

WATCH: 282.50 CPU 283.02 WC

WATCH: 285.51 CPU 286.03 WC

WATCH: 288.51 CPU 289.04 WC

WATCH: 291.52 CPU 292.06 WC

WATCH: 294.53 CPU 295.07 WC

WATCH: 297.53 CPU 298.08 WC

WATCH: 300.54 CPU 301.09 WC

FINAL WATCH: 300.54 CPU 301.24 WC