LEO-II: read-problem-file /CW/home-0/sutcliff/CASC/23/Problems/TNE/TNE083.p LEO-II: prove-with-fo-atp e LEO II: timeout set (60 seconds). ...... LEO-II tries to prove the following (sub)problems. (0) Problem: % Problem related to split clause no. 14 thf(epso,type,(epso: (($o>$o)>$o))). thf(epsoo,type,(epsoo: ((($o>$o)>$o)>($o>$o)))). thf(q,type,(q: (($o>$o)>$o))). thf(a9,axiom,(q@(^[X:$o]: $false))). thf(a15,axiom,(![P:($o>$o)]: ((![X:$o]: (~ (P@X))) | (P@(epso@P))))). thf(a16,axiom,(![P:(($o>$o)>$o)]: ((![X:($o>$o)]: (~ (P@X))) | (P@(epsoo@P))))). thf(a12,axiom,(q@(^[X:$o]: X))). thf(a13,axiom,(q@(^[X:$o]: $true))). thf(c14,negated_conjecture,(~ (q@(epsoo@epso)))). *** Trying Problem: 0 . [Unidepth=8] WATCH: 0.00 CPU 0.01 WC . [E:50s]..... WATCH: 2.99 CPU 3.02 WC . WATCH: 6.00 CPU 6.03 WC . WATCH: 9.00 CPU 9.04 WC . WATCH: 12.00 CPU 12.05 WC WATCH: 15.01 CPU 15.06 WC . WATCH: 18.01 CPU 18.07 WC WATCH: 21.01 CPU 21.08 WC . WATCH: 24.02 CPU 24.09 WC WATCH: 27.03 CPU 27.10 WC WATCH: 30.03 CPU 30.11 WC . WATCH: 33.04 CPU 33.12 WC WATCH: 36.04 CPU 36.13 WC WATCH: 39.04 CPU 39.14 WC WATCH: 42.05 CPU 42.15 WC . WATCH: 45.06 CPU 45.16 WC WATCH: 48.06 CPU 48.17 WC WATCH: 51.07 CPU 51.18 WC WATCH: 54.07 CPU 54.19 WC WATCH: 57.08 CPU 57.20 WC LEO II: timeout after 60 seconds. % SZS status Timeout (60sec) for /CW/home-0/sutcliff/CASC/23/Problems/TNE/TNE083.p LEO-II: flag-relevance-filter -1 Flag RELEVANCE_FILTER set to: -1 Prim_subst level set to 0 LEO-II: flag-max-uni-depth 5 Flag MAX_UNI_DEPTH set to: 5 LEO-II: read-problem-file /CW/home-0/sutcliff/CASC/23/Problems/TNE/TNE083.p .. LEO-II: prove-with-fo-atp e LEO II: timeout set (60 seconds). ...... LEO-II tries to prove the following (sub)problems. (0) Problem: % Problem related to split clause no. 14 thf(epso,type,(epso: (($o>$o)>$o))). thf(epsoo,type,(epsoo: ((($o>$o)>$o)>($o>$o)))). thf(q,type,(q: (($o>$o)>$o))). thf(a9,axiom,(q@(^[X:$o]: $false))). thf(a15,axiom,(![P:($o>$o)]: ((![X:$o]: (~ (P@X))) | (P@(epso@P))))). thf(a16,axiom,(![P:(($o>$o)>$o)]: ((![X:($o>$o)]: (~ (P@X))) | (P@(epsoo@P))))). thf(a12,axiom,(q@(^[X:$o]: X))). thf(a13,axiom,(q@(^[X:$o]: $true))). thf(c14,negated_conjecture,(~ (q@(epsoo@epso)))). *** Trying Problem: 0 [Unidepth=5].. [E:50s]... WATCH: 60.07 CPU 60.21 WC .... WATCH: 63.08 CPU 63.22 WC . WATCH: 66.09 CPU 66.23 WC . WATCH: 69.09 CPU 69.24 WC WATCH: 72.09 CPU 72.25 WC . WATCH: 75.10 CPU 75.26 WC WATCH: 78.10 CPU 78.27 WC . WATCH: 81.11 CPU 81.28 WC WATCH: 84.11 CPU 84.29 WC . WATCH: 87.12 CPU 87.30 WC WATCH: 90.12 CPU 90.31 WC WATCH: 93.13 CPU 93.32 WC WATCH: 96.13 CPU 96.33 WC WATCH: 99.14 CPU 99.34 WC . WATCH: 102.14 CPU 102.35 WC WATCH: 105.15 CPU 105.36 WC WATCH: 108.16 CPU 108.37 WC WATCH: 111.16 CPU 111.38 WC . WATCH: 114.17 CPU 114.39 WC WATCH: 117.17 CPU 117.40 WC .LEO II: timeout after 60 seconds. % SZS status Timeout (60sec) for /CW/home-0/sutcliff/CASC/23/Problems/TNE/TNE083.p LEO-II: flag-relevance-filter 1 Flag RELEVANCE_FILTER set to: 1 LEO-II: flag-prim-subst 3 Prim_subst level set to 3 LEO-II: flag-max-uni-depth 3 Flag MAX_UNI_DEPTH set to: 3 LEO-II: read-problem-file /CW/home-0/sutcliff/CASC/23/Problems/TNE/TNE083.p . LEO-II: prove-with-fo-atp e LEO II: timeout set (60 seconds). ...... LEO-II tries to prove the following (sub)problems. (0) Problem: % Problem related to split clause no. 14 thf(epso,type,(epso: (($o>$o)>$o))). thf(epsoo,type,(epsoo: ((($o>$o)>$o)>($o>$o)))). thf(q,type,(q: (($o>$o)>$o))). thf(a9,axiom,(q@(^[X:$o]: $false))). thf(a15,axiom,(![P:($o>$o)]: ((![X:$o]: (~ (P@X))) | (P@(epso@P))))). thf(a16,axiom,(![P:(($o>$o)>$o)]: ((![X:($o>$o)]: (~ (P@X))) | (P@(epsoo@P))))). thf(a12,axiom,(q@(^[X:$o]: X))). thf(a13,axiom,(q@(^[X:$o]: $true))). thf(c14,negated_conjecture,(~ (q@(epsoo@epso)))). *** Trying Problem: 0 . [Unidepth=3]. [E:50s]...... WATCH: 120.17 CPU 120.41 WC ................................. [E:50s]....... [E:50s].... [E:50s] Running out of time, I should stop! ... [E:50s][Unidepth=4]..... [E:50s]............ WATCH: 122.89 CPU 123.42 WC .................... WATCH: 125.89 CPU 126.43 WC .................... WATCH: 128.90 CPU 129.44 WC ............. WATCH: 131.90 CPU 132.45 WC ............... WATCH: 134.91 CPU 135.46 WC ............ WATCH: 137.92 CPU 138.48 WC ................. WATCH: 140.93 CPU 141.49 WC ........... WATCH: 143.93 CPU 144.50 WC ...................... WATCH: 146.94 CPU 147.52 WC ............. WATCH: 149.95 CPU 150.53 WC ......... WATCH: 152.96 CPU 153.55 WC WATCH: 155.97 CPU 156.56 WC ............................................................................................................................. WATCH: 158.97 CPU 159.58 WC ... WATCH: 161.98 CPU 162.59 WC .. WATCH: 164.98 CPU 165.60 WC .. WATCH: 167.99 CPU 168.61 WC .. WATCH: 171.00 CPU 171.62 WC . WATCH: 174.00 CPU 174.63 WC .. WATCH: 177.01 CPU 177.65 WC .LEO II: timeout after 60 seconds. % SZS status Timeout (60sec) for /CW/home-0/sutcliff/CASC/23/Problems/TNE/TNE083.p LEO-II: flag-relevance-filter 0 Flag RELEVANCE_FILTER set to: 0 LEO-II: flag-sos Flag SOS set to: false LEO-II: flag-prim-subst 3 Prim_subst level set to 3 LEO-II: flag-max-uni-depth 8 Flag MAX_UNI_DEPTH set to: 8 LEO-II: flag-unfold-defs-early Flag UNFOLD_DEFS_EARLY set to: false LEO-II: read-problem-file /CW/home-0/sutcliff/CASC/23/Problems/TNE/TNE083.p LEO-II: prove-with-fo-atp e LEO II: timeout set (60 seconds). ...... LEO-II tries to prove the following (sub)problems. (0) Problem: % Problem related to split clause no. 8 thf(epso,type,(epso: (($o>$o)>$o))). thf(epsoo,type,(epsoo: ((($o>$o)>$o)>($o>$o)))). thf(q,type,(q: (($o>$o)>$o))). thf(a1,axiom,(q@(^[X:$o]: $false))). thf(a9,axiom,(![P:($o>$o)]: ((![X:$o]: (~ (P@X))) | (P@(epso@P))))). thf(a10,axiom,(![P:(($o>$o)>$o)]: ((![X:($o>$o)]: (~ (P@X))) | (P@(epsoo@P))))). thf(a4,axiom,(q@(^[X:$o]: X))). thf(a5,axiom,(q@(^[X:$o]: $true))). thf(c8,negated_conjecture,(~ (q@(epsoo@epso)))). *** Trying Problem: 0 [Unidepth=8].. [E:50s]..... WATCH: 180.03 CPU 180.66 WC WATCH: 183.04 CPU 183.67 WC . WATCH: 186.05 CPU 186.69 WC . WATCH: 189.06 CPU 189.70 WC WATCH: 192.07 CPU 192.71 WC . WATCH: 195.07 CPU 195.72 WC WATCH: 198.08 CPU 198.74 WC . WATCH: 201.09 CPU 201.75 WC WATCH: 204.10 CPU 204.76 WC WATCH: 207.10 CPU 207.78 WC . WATCH: 210.11 CPU 210.79 WC WATCH: 213.12 CPU 213.81 WC WATCH: 216.13 CPU 216.82 WC WATCH: 219.13 CPU 219.83 WC . WATCH: 222.14 CPU 222.85 WC WATCH: 225.15 CPU 225.86 WC WATCH: 228.16 CPU 228.87 WC . WATCH: 231.16 CPU 231.89 WC WATCH: 234.17 CPU 234.90 WC WATCH: 237.18 CPU 237.91 WC LEO II: timeout after 60 seconds. % SZS status Timeout (60sec) for /CW/home-0/sutcliff/CASC/23/Problems/TNE/TNE083.p WATCH: 239.73 CPU 240.46 WC FINAL WATCH: 239.73 CPU 240.46 WC