%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR012+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:05:11 PM UTC 2026
% Result : Theorem 49.75s 6.85s
% Output : Proof 49.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 11
% Syntax : Number of formulae : 73 ( 24 unt; 0 def)
% Number of atoms : 271 ( 91 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 313 ( 115 ~; 124 |; 66 &)
% ( 6 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-4 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-3 aty)
% Number of variables : 136 ( 4 sgn 75 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f15,axiom,
! [Event,Time] :
( happens(Event,Time)
<=> ( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| ( Time = n0
& Event = tapOn ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_all_defn) ).
fof(f15_nnf,plain,
! [Event,Time] :
( ( ( ( Event != overflow
| ~ holdsAt(filling,Time)
| ~ holdsAt(waterLevel(n3),Time) )
& ( Time != n0
| Event != tapOn ) )
| happens(Event,Time) )
& ( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| ( Time = n0
& Event = tapOn )
| ~ happens(Event,Time) ) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [Event,Time] :
( ( ( ( Event != overflow
| ~ holdsAt(filling,Time)
| ~ holdsAt(waterLevel(n3),Time) )
& ( Time != n0
| Event != tapOn ) )
| happens(Event,Time) )
& ( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| ( Time = n0
& Event = tapOn )
| ~ happens(Event,Time) ) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c80,plain,
( X1 != n0
| X0 != tapOn
| happens(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p473,plain,
( X0 != n0
| happens(tapOn,X0) ),
inference(equality_resolution,[status(thm)],[c80]) ).
cnf(p475,plain,
happens(tapOn,n0),
inference(equality_resolution,[status(thm)],[p473]) ).
fof(f2,axiom,
! [Event,Time,Fluent,Fluent2,Offset] :
( ( ~ stoppedIn(Time,Fluent,plus(Time,Offset))
& trajectory(Fluent,Time,Fluent2,Offset)
& less(n0,Offset)
& initiates(Event,Fluent,Time)
& happens(Event,Time) )
=> holdsAt(Fluent2,plus(Time,Offset)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',change_holding) ).
fof(f2_nnf,plain,
! [Event,Time,Fluent,Fluent2,Offset] :
( holdsAt(Fluent2,plus(Time,Offset))
| stoppedIn(Time,Fluent,plus(Time,Offset))
| ~ trajectory(Fluent,Time,Fluent2,Offset)
| ~ less(n0,Offset)
| ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [Event,Time,Fluent,Offset,Fluent2] :
( holdsAt(Fluent2,plus(Time,Offset))
| stoppedIn(Time,Fluent,plus(Time,Offset))
| ~ trajectory(Fluent,Time,Fluent2,Offset)
| ~ less(n0,Offset)
| ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c10,plain,
( holdsAt(X3,plus(X1,X4))
| stoppedIn(X1,X2,plus(X1,X4))
| ~ trajectory(X2,X1,X3,X4)
| ~ less(n0,X4)
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p476,plain,
( holdsAt(X2,plus(n0,X1))
| stoppedIn(n0,X0,plus(n0,X1))
| ~ trajectory(X0,n0,X2,X1)
| ~ less(n0,X1)
| ~ initiates(tapOn,X0,n0) ),
inference(resolution,[status(thm)],[p475,c10]) ).
fof(f12,axiom,
! [Event,Fluent,Time] :
( initiates(Event,Fluent,Time)
<=> ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = overflow
& holdsAt(waterLevel(Height),Time) )
| ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOff
& holdsAt(waterLevel(Height),Time) )
| ( Fluent = spilling
& Event = overflow )
| ( Fluent = filling
& Event = tapOn ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',initiates_all_defn) ).
fof(f12_nnf,plain,
! [Event,Fluent,Time] :
( ( ( ! [Height] :
( Fluent != waterLevel(Height)
| Event != overflow
| ~ holdsAt(waterLevel(Height),Time) )
& ! [Height] :
( Fluent != waterLevel(Height)
| Event != tapOff
| ~ holdsAt(waterLevel(Height),Time) )
& ( Fluent != spilling
| Event != overflow )
& ( Fluent != filling
| Event != tapOn ) )
| initiates(Event,Fluent,Time) )
& ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = overflow
& holdsAt(waterLevel(Height),Time) )
| ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOff
& holdsAt(waterLevel(Height),Time) )
| ( Fluent = spilling
& Event = overflow )
| ( Fluent = filling
& Event = tapOn )
| ~ initiates(Event,Fluent,Time) ) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [Event,Fluent,Time,Height] :
( ( ( ( Fluent != waterLevel(Height)
| Event != overflow
| ~ holdsAt(waterLevel(Height),Time) )
& ( Fluent != waterLevel(Height)
| Event != tapOff
| ~ holdsAt(waterLevel(Height),Time) )
& ( Fluent != spilling
| Event != overflow )
& ( Fluent != filling
| Event != tapOn ) )
| initiates(Event,Fluent,Time) )
& ( ( Fluent = waterLevel(sk9(Event,Fluent,Time))
& Event = overflow
& holdsAt(waterLevel(sk9(Event,Fluent,Time)),Time) )
| ( Fluent = waterLevel(sk8(Event,Fluent,Time))
& Event = tapOff
& holdsAt(waterLevel(sk8(Event,Fluent,Time)),Time) )
| ( Fluent = spilling
& Event = overflow )
| ( Fluent = filling
& Event = tapOn )
| ~ initiates(Event,Fluent,Time) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk8,sk9])],[f12_nnf]) ).
cnf(c61,plain,
( X1 != filling
| X0 != tapOn
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p419,plain,
( X0 != filling
| initiates(tapOn,X0,X1) ),
inference(equality_resolution,[status(thm)],[c61]) ).
cnf(p434,plain,
initiates(tapOn,filling,X0),
inference(equality_resolution,[status(thm)],[p419]) ).
cnf(p1665,plain,
( holdsAt(X1,plus(n0,X0))
| stoppedIn(n0,filling,plus(n0,X0))
| ~ trajectory(filling,n0,X1,X0)
| ~ less(n0,X0) ),
inference(resolution,[status(thm)],[p476,p434]) ).
fof(f38,axiom,
! [X] :
( less(X,n1)
<=> less_or_equal(X,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less1) ).
fof(f38_nnf,plain,
! [X] :
( ( ~ less_or_equal(X,n0)
| less(X,n1) )
& ( less_or_equal(X,n0)
| ~ less(X,n1) ) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [X] :
( ( ~ less_or_equal(X,n0)
| less(X,n1) )
& ( less_or_equal(X,n0)
| ~ less(X,n1) ) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c108,plain,
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
fof(f36,axiom,
! [X,Y] :
( less_or_equal(X,Y)
<=> ( X = Y
| less(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_or_equal) ).
fof(f36_nnf,plain,
! [X,Y] :
( ( ( X != Y
& ~ less(X,Y) )
| less_or_equal(X,Y) )
& ( X = Y
| less(X,Y)
| ~ less_or_equal(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [X,Y] :
( ( ( X != Y
& ~ less(X,Y) )
| less_or_equal(X,Y) )
& ( X = Y
| less(X,Y)
| ~ less_or_equal(X,Y) ) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c105,plain,
( X0 != X1
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p138,plain,
less_or_equal(X0,X0),
inference(equality_resolution,[status(thm)],[c105]) ).
cnf(p140,plain,
less(n0,n1),
inference(resolution,[status(thm)],[c108,p138]) ).
cnf(p17852,plain,
( holdsAt(X0,n1)
| stoppedIn(n0,filling,n1)
| ~ trajectory(filling,n0,X0,n1) ),
inference(resolution,[status(thm)],[p1665,p140]) ).
fof(f16,axiom,
! [Height1,Time,Height2,Offset] :
( ( Height2 = plus(Height1,Offset)
& holdsAt(waterLevel(Height1),Time) )
=> trajectory(filling,Time,waterLevel(Height2),Offset) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',change_of_waterLevel) ).
fof(f16_nnf,plain,
! [Height1,Time,Height2,Offset] :
( trajectory(filling,Time,waterLevel(Height2),Offset)
| Height2 != plus(Height1,Offset)
| ~ holdsAt(waterLevel(Height1),Time) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [Height1,Time,Height2,Offset] :
( trajectory(filling,Time,waterLevel(Height2),Offset)
| Height2 != plus(Height1,Offset)
| ~ holdsAt(waterLevel(Height1),Time) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c82,plain,
( trajectory(filling,X1,waterLevel(X2),X3)
| X2 != plus(X0,X3)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p488,plain,
( trajectory(filling,X1,waterLevel(plus(X0,X2)),X2)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(equality_resolution,[status(thm)],[c82]) ).
fof(f48,hypothesis,
holdsAt(waterLevel(n0),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',waterLevel_0) ).
fof(f48_nnf,plain,
holdsAt(waterLevel(n0),n0),
inference(nnf_transformation,[status(thm)],[f48]) ).
cnf(c128,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[status(esa)],[f48_nnf]) ).
cnf(p1714,plain,
trajectory(filling,n0,waterLevel(plus(n0,X0)),X0),
inference(resolution,[status(thm)],[p488,c128]) ).
cnf(p17865,plain,
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1) ),
inference(resolution,[status(thm)],[p17852,p1714]) ).
fof(f54,conjecture,
holdsAt(waterLevel(n1),n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',waterLevel_1) ).
fof(f54_neg,negated_conjecture,
~ holdsAt(waterLevel(n1),n1),
inference(negated_conjecture,[status(cth)],[f54]) ).
fof(f54_nnf,plain,
~ holdsAt(waterLevel(n1),n1),
inference(nnf_transformation,[status(thm)],[f54_neg]) ).
fof(f54_sk,plain,
~ holdsAt(waterLevel(n1),n1),
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c134,plain,
~ holdsAt(waterLevel(n1),n1),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(p17867,plain,
stoppedIn(n0,filling,n1),
inference(resolution,[status(thm)],[p17865,c134]) ).
fof(f0,axiom,
! [Time1,Fluent,Time2] :
( stoppedIn(Time1,Fluent,Time2)
<=> ? [Event,Time] :
( terminates(Event,Fluent,Time)
& less(Time,Time2)
& less(Time1,Time)
& happens(Event,Time) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',stoppedin_defn) ).
fof(f0_nnf,plain,
! [Time1,Fluent,Time2] :
( ( ! [Event,Time] :
( ~ terminates(Event,Fluent,Time)
| ~ less(Time,Time2)
| ~ less(Time1,Time)
| ~ happens(Event,Time) )
| stoppedIn(Time1,Fluent,Time2) )
& ( ? [Event,Time] :
( terminates(Event,Fluent,Time)
& less(Time,Time2)
& less(Time1,Time)
& happens(Event,Time) )
| ~ stoppedIn(Time1,Fluent,Time2) ) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [Time1,Fluent,Time2,Event,Time] :
( ( ~ terminates(Event,Fluent,Time)
| ~ less(Time,Time2)
| ~ less(Time1,Time)
| ~ happens(Event,Time)
| stoppedIn(Time1,Fluent,Time2) )
& ( ( terminates(sk0(Time1,Fluent,Time2),Fluent,sk1(Time1,Fluent,Time2))
& less(sk1(Time1,Fluent,Time2),Time2)
& less(Time1,sk1(Time1,Fluent,Time2))
& happens(sk0(Time1,Fluent,Time2),sk1(Time1,Fluent,Time2)) )
| ~ stoppedIn(Time1,Fluent,Time2) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f0_nnf]) ).
cnf(c2,plain,
( less(sk1(X0,X1,X2),X2)
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p17870,plain,
less(sk1(n0,filling,n1),n1),
inference(resolution,[status(thm)],[p17867,c2]) ).
fof(f47,axiom,
! [X,Y] :
( less(X,Y)
<=> ( Y != X
& ~ less(Y,X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_property) ).
fof(f47_nnf,plain,
! [X,Y] :
( ( Y = X
| less(Y,X)
| less(X,Y) )
& ( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
! [X,Y] :
( ( Y = X
| less(Y,X)
| less(X,Y) )
& ( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c127,plain,
( X1 = X0
| less(X1,X0)
| less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(c107,plain,
( less_or_equal(X0,n0)
| ~ less(X0,n1) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p504,plain,
( less_or_equal(X0,n0)
| n1 = X0
| less(n1,X0) ),
inference(resolution,[status(thm)],[c127,c107]) ).
cnf(c103,plain,
( X0 = X1
| less(X0,X1)
| ~ less_or_equal(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p603,plain,
( X0 = n0
| less(X0,n0)
| n1 = X0
| less(n1,X0) ),
inference(resolution,[status(thm)],[p504,c103]) ).
fof(f37,axiom,
~ ? [X] : less(X,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less0) ).
fof(f37_nnf,plain,
! [X] : ~ less(X,n0),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [X] : ~ less(X,n0),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c106,plain,
~ less(X0,n0),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p1981,plain,
( X0 = n0
| n1 = X0
| less(n1,X0) ),
inference(resolution,[status(thm)],[p603,c106]) ).
cnf(c125,plain,
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p1984,plain,
( ~ less(X0,n1)
| X0 = n0
| n1 = X0 ),
inference(resolution,[status(thm)],[p1981,c125]) ).
cnf(p17905,plain,
( sk1(n0,filling,n1) = n0
| n1 = sk1(n0,filling,n1) ),
inference(resolution,[status(thm)],[p17870,p1984]) ).
cnf(c1,plain,
( less(X0,sk1(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p17869,plain,
less(n0,sk1(n0,filling,n1)),
inference(resolution,[status(thm)],[p17867,c1]) ).
cnf(c126,plain,
( X1 != X0
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p17873,plain,
sk1(n0,filling,n1) != n0,
inference(resolution,[status(thm)],[p17869,c126]) ).
cnf(p20312,plain,
n1 = sk1(n0,filling,n1),
inference(resolution,[status(thm)],[p17905,p17873]) ).
cnf(p17886,plain,
n1 != sk1(n0,filling,n1),
inference(resolution,[status(thm)],[p17870,c126]) ).
cnf(p20321,plain,
$false,
inference(resolution,[status(thm)],[p20312,p17886]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR012+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 08:10:11 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 49.75/6.85 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 49.75/6.85 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------