%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR012+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 : Thu Sep 24 12:12:49 PM UTC 2026
% Result : Theorem 3.74s 0.96s
% Output : CNFRefutation 3.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 18
% Syntax : Number of formulae : 112 ( 29 unt; 3 def)
% Number of atoms : 421 ( 120 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 482 ( 173 ~; 189 |; 104 &)
% ( 12 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 8 con; 0-3 aty)
% Number of variables : 273 ( 252 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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') ).
fof(f3,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') ).
fof(f8,axiom,
! [Fluent,Time] :
( ( ~ ? [Event] :
( releases(Event,Fluent,Time)
& happens(Event,Time) )
& ~ releasedAt(Fluent,Time) )
=> ~ releasedAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [Event,Time,Fluent] :
( ( releases(Event,Fluent,Time)
& happens(Event,Time) )
=> releasedAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,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') ).
fof(f15,axiom,
! [Event,Fluent,Time] :
( releases(Event,Fluent,Time)
<=> ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOn ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,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') ).
fof(f17,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') ).
fof(f27,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [X,Y] :
( less_or_equal(X,Y)
<=> ( X = Y
| less(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
~ ? [X] : less(X,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X] :
( less(X,n1)
<=> less_or_equal(X,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
holdsAt(waterLevel(n0),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,hypothesis,
! [Height] : ~ releasedAt(waterLevel(Height),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,conjecture,
holdsAt(waterLevel(n1),n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,negated_conjecture,
~ holdsAt(waterLevel(n1),n1),
inference(negated_conjecture,[status(cth)],[f55]) ).
fof(f57,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)],[f1]) ).
fof(f58,plain,
( ! [Time1,Fluent,Time2] :
( ! [Event,Time] :
( ~ terminates(Event,Fluent,Time)
| ~ less(Time,Time2)
| ~ less(Time1,Time)
| ~ happens(Event,Time) )
| stoppedIn(Time1,Fluent,Time2) )
& ! [Time1,Fluent,Time2] :
( ? [Event,Time] :
( terminates(Event,Fluent,Time)
& less(Time,Time2)
& less(Time1,Time)
& happens(Event,Time) )
| ~ stoppedIn(Time1,Fluent,Time2) ) ),
inference(miniscoping,[status(thm)],[f57]) ).
fof(f59,plain,
( ! [Time1,Fluent,Time2] :
( ! [Event,Time] :
( ~ terminates(Event,Fluent,Time)
| ~ less(Time,Time2)
| ~ less(Time1,Time)
| ~ happens(Event,Time) )
| stoppedIn(Time1,Fluent,Time2) )
& ! [Time1,Fluent,Time2] :
( ( terminates(sK0_skl(Time2,Fluent,Time1),Fluent,sK1_skl(Time2,Fluent,Time1))
& less(sK1_skl(Time2,Fluent,Time1),Time2)
& less(Time1,sK1_skl(Time2,Fluent,Time1))
& happens(sK0_skl(Time2,Fluent,Time1),sK1_skl(Time2,Fluent,Time1)) )
| ~ stoppedIn(Time1,Fluent,Time2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Event,sK0_skl(Time2,Fluent,Time1)),skolemize(Time,sK1_skl(Time2,Fluent,Time1))],[f58]) ).
fof(f61,plain,
! [X0,X1,X2] :
( less(X0,sK1_skl(X2,X1,X0))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f62,plain,
! [X0,X1,X2] :
( less(sK1_skl(X2,X1,X0),X2)
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f73,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(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f74,plain,
! [Time,Fluent2,Offset] :
( holdsAt(Fluent2,plus(Time,Offset))
| ! [Fluent] :
( stoppedIn(Time,Fluent,plus(Time,Offset))
| ~ trajectory(Fluent,Time,Fluent2,Offset)
| ~ less(n0,Offset)
| ! [Event] :
( ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ) ) ),
inference(miniscoping,[status(thm)],[f73]) ).
fof(f75,plain,
! [X0,X1,X2,X3,X4] :
( holdsAt(X4,plus(X1,X3))
| stoppedIn(X1,X2,plus(X1,X3))
| ~ trajectory(X2,X1,X4,X3)
| ~ less(n0,X3)
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f91,plain,
! [Fluent,Time] :
( ~ releasedAt(Fluent,plus(Time,n1))
| ? [Event] :
( releases(Event,Fluent,Time)
& happens(Event,Time) )
| releasedAt(Fluent,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f92,plain,
! [Fluent,Time] :
( ~ releasedAt(Fluent,plus(Time,n1))
| ( releases(sK7_skl(Time,Fluent),Fluent,Time)
& happens(sK7_skl(Time,Fluent),Time) )
| releasedAt(Fluent,Time) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Event,sK7_skl(Time,Fluent))],[f91]) ).
fof(f93,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| happens(sK7_skl(X1,X0),X1)
| releasedAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f94,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releases(sK7_skl(X1,X0),X0,X1)
| releasedAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f101,plain,
! [Event,Time,Fluent] :
( releasedAt(Fluent,plus(Time,n1))
| ~ releases(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f102,plain,
! [Time,Fluent] :
( releasedAt(Fluent,plus(Time,n1))
| ! [Event] :
( ~ releases(Event,Fluent,Time)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f101]) ).
fof(f103,plain,
! [X0,X1,X2] :
( releasedAt(X2,plus(X1,n1))
| ~ releases(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f108,definition,
! [Event,Fluent,Time] :
( sP0_prd(Time,Fluent,Event)
<=> ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOff
& holdsAt(waterLevel(Height),Time) )
| ( Fluent = spilling
& Event = overflow )
| ( Fluent = filling
& Event = tapOn ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f109,plain,
! [Event,Fluent,Time] :
( initiates(Event,Fluent,Time)
<=> ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = overflow
& holdsAt(waterLevel(Height),Time) )
| sP0_prd(Time,Fluent,Event) ) ),
inference(formula_renaming,[status(thm)],[f13,f108]) ).
fof(f110,plain,
! [Event,Fluent,Time] :
( ( ( ! [Height] :
( Fluent != waterLevel(Height)
| Event != overflow
| ~ holdsAt(waterLevel(Height),Time) )
& ~ sP0_prd(Time,Fluent,Event) )
| initiates(Event,Fluent,Time) )
& ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = overflow
& holdsAt(waterLevel(Height),Time) )
| sP0_prd(Time,Fluent,Event)
| ~ initiates(Event,Fluent,Time) ) ),
inference(NNF_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
( ! [Event,Fluent,Time] :
( ( ! [Height] :
( Fluent != waterLevel(Height)
| Event != overflow
| ~ holdsAt(waterLevel(Height),Time) )
& ~ sP0_prd(Time,Fluent,Event) )
| initiates(Event,Fluent,Time) )
& ! [Event,Fluent,Time] :
( ? [Height] :
( Fluent = waterLevel(Height)
& Event = overflow
& holdsAt(waterLevel(Height),Time) )
| sP0_prd(Time,Fluent,Event)
| ~ initiates(Event,Fluent,Time) ) ),
inference(miniscoping,[status(thm)],[f110]) ).
fof(f112,plain,
( ! [Event,Fluent,Time] :
( ( ! [Height] :
( Fluent != waterLevel(Height)
| Event != overflow
| ~ holdsAt(waterLevel(Height),Time) )
& ~ sP0_prd(Time,Fluent,Event) )
| initiates(Event,Fluent,Time) )
& ! [Event,Fluent,Time] :
( ( Fluent = waterLevel(sK8_skl(Time,Fluent,Event))
& Event = overflow
& holdsAt(waterLevel(sK8_skl(Time,Fluent,Event)),Time) )
| sP0_prd(Time,Fluent,Event)
| ~ initiates(Event,Fluent,Time) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(Height,sK8_skl(Time,Fluent,Event))],[f111]) ).
fof(f116,plain,
! [X0,X1,X2] :
( ~ sP0_prd(X2,X1,X0)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f126,plain,
! [Event,Fluent,Time] :
( ( ! [Height] :
( Fluent != waterLevel(Height)
| Event != tapOn )
| releases(Event,Fluent,Time) )
& ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOn )
| ~ releases(Event,Fluent,Time) ) ),
inference(NNF_transformation,[status(thm)],[f15]) ).
fof(f127,plain,
( ! [Event,Fluent] :
( ! [Height] : Fluent != waterLevel(Height)
| Event != tapOn
| ! [Time] : releases(Event,Fluent,Time) )
& ! [Event,Fluent] :
( ( ? [Height] : Fluent = waterLevel(Height)
& Event = tapOn )
| ! [Time] : ~ releases(Event,Fluent,Time) ) ),
inference(miniscoping,[status(thm)],[f126]) ).
fof(f128,plain,
( ! [Event,Fluent] :
( ! [Height] : Fluent != waterLevel(Height)
| Event != tapOn
| ! [Time] : releases(Event,Fluent,Time) )
& ! [Event,Fluent] :
( ( Fluent = waterLevel(sK9_skl(Fluent,Event))
& Event = tapOn )
| ! [Time] : ~ releases(Event,Fluent,Time) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(Height,sK9_skl(Fluent,Event))],[f127]) ).
fof(f129,plain,
! [X0,X1,X2] :
( X0 = tapOn
| ~ releases(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f131,plain,
! [X0,X1,X2,X3] :
( X1 != waterLevel(X3)
| X0 != tapOn
| releases(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f132,definition,
! [Event,Time] :
( sP1_prd(Time,Event)
<=> ( Time = n0
& Event = tapOn ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f133,plain,
! [Event,Time] :
( happens(Event,Time)
<=> ( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| sP1_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f16,f132]) ).
fof(f134,plain,
! [Event,Time] :
( ( ( ( Event != overflow
| ~ holdsAt(filling,Time)
| ~ holdsAt(waterLevel(n3),Time) )
& ~ sP1_prd(Time,Event) )
| happens(Event,Time) )
& ( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| sP1_prd(Time,Event)
| ~ happens(Event,Time) ) ),
inference(NNF_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
( ! [Event,Time] :
( ( ( Event != overflow
| ~ holdsAt(filling,Time)
| ~ holdsAt(waterLevel(n3),Time) )
& ~ sP1_prd(Time,Event) )
| happens(Event,Time) )
& ! [Event,Time] :
( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| sP1_prd(Time,Event)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f134]) ).
fof(f139,plain,
! [X0,X1] :
( ~ sP1_prd(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f141,plain,
! [Height1,Time,Height2,Offset] :
( trajectory(filling,Time,waterLevel(Height2),Offset)
| Height2 != plus(Height1,Offset)
| ~ holdsAt(waterLevel(Height1),Time) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f142,plain,
! [Time,Height2,Offset] :
( trajectory(filling,Time,waterLevel(Height2),Offset)
| ! [Height1] :
( Height2 != plus(Height1,Offset)
| ~ holdsAt(waterLevel(Height1),Time) ) ),
inference(miniscoping,[status(thm)],[f141]) ).
fof(f143,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| X2 != plus(X0,X3)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f158,plain,
plus(n0,n1) = n1,
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f168,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)],[f37]) ).
fof(f169,plain,
( ! [X,Y] :
( ( X != Y
& ~ less(X,Y) )
| less_or_equal(X,Y) )
& ! [X,Y] :
( X = Y
| less(X,Y)
| ~ less_or_equal(X,Y) ) ),
inference(miniscoping,[status(thm)],[f168]) ).
fof(f170,plain,
! [X0,X1] :
( X0 = X1
| less(X0,X1)
| ~ less_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f172,plain,
! [X0,X1] :
( X0 != X1
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f173,plain,
! [X] : ~ less(X,n0),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f174,plain,
! [X0] : ~ less(X0,n0),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f175,plain,
! [X] :
( ( ~ less_or_equal(X,n0)
| less(X,n1) )
& ( less_or_equal(X,n0)
| ~ less(X,n1) ) ),
inference(NNF_transformation,[status(thm)],[f39]) ).
fof(f176,plain,
( ! [X] :
( ~ less_or_equal(X,n0)
| less(X,n1) )
& ! [X] :
( less_or_equal(X,n0)
| ~ less(X,n1) ) ),
inference(miniscoping,[status(thm)],[f175]) ).
fof(f177,plain,
! [X0] :
( less_or_equal(X0,n0)
| ~ less(X0,n1) ),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f178,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f216,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f219,plain,
! [X0] : ~ releasedAt(waterLevel(X0),n0),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f222,plain,
~ holdsAt(waterLevel(n1),n1),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f223,definition,
! [Event,Fluent] :
( sP2_prd(Fluent,Event)
<=> ( ( Fluent = spilling
& Event = overflow )
| ( Fluent = filling
& Event = tapOn ) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f224,plain,
! [Event,Fluent,Time] :
( sP0_prd(Time,Fluent,Event)
<=> ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOff
& holdsAt(waterLevel(Height),Time) )
| sP2_prd(Fluent,Event) ) ),
inference(formula_renaming,[status(thm)],[f108,f223]) ).
fof(f225,plain,
! [Event,Fluent,Time] :
( ( ( ! [Height] :
( Fluent != waterLevel(Height)
| Event != tapOff
| ~ holdsAt(waterLevel(Height),Time) )
& ~ sP2_prd(Fluent,Event) )
| sP0_prd(Time,Fluent,Event) )
& ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOff
& holdsAt(waterLevel(Height),Time) )
| sP2_prd(Fluent,Event)
| ~ sP0_prd(Time,Fluent,Event) ) ),
inference(NNF_transformation,[status(thm)],[f224]) ).
fof(f226,plain,
( ! [Event,Fluent,Time] :
( ( ! [Height] :
( Fluent != waterLevel(Height)
| Event != tapOff
| ~ holdsAt(waterLevel(Height),Time) )
& ~ sP2_prd(Fluent,Event) )
| sP0_prd(Time,Fluent,Event) )
& ! [Event,Fluent,Time] :
( ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOff
& holdsAt(waterLevel(Height),Time) )
| sP2_prd(Fluent,Event)
| ~ sP0_prd(Time,Fluent,Event) ) ),
inference(miniscoping,[status(thm)],[f225]) ).
fof(f227,plain,
( ! [Event,Fluent,Time] :
( ( ! [Height] :
( Fluent != waterLevel(Height)
| Event != tapOff
| ~ holdsAt(waterLevel(Height),Time) )
& ~ sP2_prd(Fluent,Event) )
| sP0_prd(Time,Fluent,Event) )
& ! [Event,Fluent,Time] :
( ( Fluent = waterLevel(sK10_skl(Time,Fluent,Event))
& Event = tapOff
& holdsAt(waterLevel(sK10_skl(Time,Fluent,Event)),Time) )
| sP2_prd(Fluent,Event)
| ~ sP0_prd(Time,Fluent,Event) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(Height,sK10_skl(Time,Fluent,Event))],[f226]) ).
fof(f231,plain,
! [X0,X1,X2] :
( ~ sP2_prd(X1,X2)
| sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f233,plain,
! [Event,Time] :
( ( Time != n0
| Event != tapOn
| sP1_prd(Time,Event) )
& ( ( Time = n0
& Event = tapOn )
| ~ sP1_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f132]) ).
fof(f234,plain,
( ! [Event,Time] :
( Time != n0
| Event != tapOn
| sP1_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = tapOn )
| ~ sP1_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f233]) ).
fof(f237,plain,
! [X0,X1] :
( X0 != n0
| X1 != tapOn
| sP1_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f238,plain,
! [Event,Fluent] :
( ( ( ( Fluent != spilling
| Event != overflow )
& ( Fluent != filling
| Event != tapOn ) )
| sP2_prd(Fluent,Event) )
& ( ( Fluent = spilling
& Event = overflow )
| ( Fluent = filling
& Event = tapOn )
| ~ sP2_prd(Fluent,Event) ) ),
inference(NNF_transformation,[status(thm)],[f223]) ).
fof(f239,plain,
( ! [Event,Fluent] :
( ( ( Fluent != spilling
| Event != overflow )
& ( Fluent != filling
| Event != tapOn ) )
| sP2_prd(Fluent,Event) )
& ! [Event,Fluent] :
( ( Fluent = spilling
& Event = overflow )
| ( Fluent = filling
& Event = tapOn )
| ~ sP2_prd(Fluent,Event) ) ),
inference(miniscoping,[status(thm)],[f238]) ).
fof(f244,plain,
! [X0,X1] :
( X0 != filling
| X1 != tapOn
| sP2_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f250,plain,
! [X0,X1] : releases(tapOn,waterLevel(X0),X1),
inference(destructive_equality_resolution,[status(thm)],[f131]) ).
fof(f252,plain,
! [X0,X1,X2] :
( trajectory(filling,X1,waterLevel(plus(X0,X2)),X2)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(destructive_equality_resolution,[status(thm)],[f143]) ).
fof(f253,plain,
! [X0] : less_or_equal(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f172]) ).
fof(f256,plain,
sP1_prd(n0,tapOn),
inference(destructive_equality_resolution,[status(thm)],[f237]) ).
fof(f257,plain,
sP2_prd(filling,tapOn),
inference(destructive_equality_resolution,[status(thm)],[f244]) ).
fof(f283,plain,
! [X0,X1] :
( sK7_skl(X1,X0) = tapOn
| ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1) ),
inference(resolution,[status(thm)],[f94,f129]) ).
fof(f292,plain,
! [X0,X1] :
( releasedAt(waterLevel(X1),plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(resolution,[status(thm)],[f103,f250]) ).
fof(f301,plain,
less(n0,n1),
inference(resolution,[status(thm)],[f178,f253]) ).
fof(f365,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(n0,X0)),X0),
inference(resolution,[status(thm)],[f252,f216]) ).
fof(f487,plain,
! [X0] :
( sK7_skl(n0,waterLevel(X0)) = tapOn
| ~ releasedAt(waterLevel(X0),plus(n0,n1)) ),
inference(resolution,[status(thm)],[f283,f219]) ).
fof(f491,plain,
! [X0] :
( sK7_skl(n0,waterLevel(X0)) = tapOn
| ~ releasedAt(waterLevel(X0),n1) ),
inference(forward_demodulation,[status(thm)],[f158,f487]) ).
fof(f520,plain,
! [X0,X1] :
( ~ sP1_prd(X1,tapOn)
| releasedAt(waterLevel(X0),plus(X1,n1)) ),
inference(resolution,[status(thm)],[f292,f139]) ).
fof(f699,plain,
trajectory(filling,n0,waterLevel(n1),n1),
inference(paramodulation,[status(thm)],[f158,f365]) ).
fof(f1155,plain,
! [X0] :
( holdsAt(waterLevel(n1),plus(n0,n1))
| stoppedIn(n0,filling,plus(n0,n1))
| ~ less(n0,n1)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(resolution,[status(thm)],[f699,f75]) ).
fof(f1156,plain,
! [X0] :
( holdsAt(waterLevel(n1),plus(n0,n1))
| stoppedIn(n0,filling,n1)
| ~ less(n0,n1)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_demodulation,[status(thm)],[f158,f1155]) ).
fof(f1157,plain,
! [X0] :
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1)
| ~ less(n0,n1)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_demodulation,[status(thm)],[f158,f1156]) ).
fof(f1158,plain,
! [X0] :
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1157,f301]) ).
fof(f1464,plain,
! [X0] : releasedAt(waterLevel(X0),plus(n0,n1)),
inference(resolution,[status(thm)],[f520,f256]) ).
fof(f1469,plain,
! [X0] : releasedAt(waterLevel(X0),n1),
inference(forward_demodulation,[status(thm)],[f158,f1464]) ).
fof(f1473,plain,
! [X0] : sK7_skl(n0,waterLevel(X0)) = tapOn,
inference(backward_subsumption_resolution,[status(thm)],[f491,f1469]) ).
fof(f1489,plain,
! [X0] :
( ~ releasedAt(waterLevel(X0),plus(n0,n1))
| happens(tapOn,n0)
| releasedAt(waterLevel(X0),n0) ),
inference(paramodulation,[status(thm)],[f1473,f93]) ).
fof(f1491,plain,
! [X0] :
( ~ releasedAt(waterLevel(X0),n1)
| happens(tapOn,n0)
| releasedAt(waterLevel(X0),n0) ),
inference(forward_demodulation,[status(thm)],[f158,f1489]) ).
fof(f1492,plain,
! [X0] :
( ~ releasedAt(waterLevel(X0),n1)
| happens(tapOn,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1491,f219]) ).
fof(f1921,plain,
happens(tapOn,n0),
inference(forward_subsumption_resolution,[status(thm)],[f1492,f1469]) ).
fof(f5270,plain,
! [X0] :
( stoppedIn(n0,filling,n1)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1158,f222]) ).
fof(f5272,plain,
! [X0] :
( ~ sP0_prd(n0,filling,X0)
| stoppedIn(n0,filling,n1)
| ~ happens(X0,n0) ),
inference(resolution,[status(thm)],[f5270,f116]) ).
fof(f5302,plain,
! [X0] :
( ~ sP2_prd(filling,X0)
| stoppedIn(n0,filling,n1)
| ~ happens(X0,n0) ),
inference(resolution,[status(thm)],[f5272,f231]) ).
fof(f5303,plain,
( stoppedIn(n0,filling,n1)
| ~ happens(tapOn,n0) ),
inference(resolution,[status(thm)],[f5302,f257]) ).
fof(f5307,plain,
stoppedIn(n0,filling,n1),
inference(forward_subsumption_resolution,[status(thm)],[f5303,f1921]) ).
fof(f5326,plain,
less(sK1_skl(n1,filling,n0),n1),
inference(resolution,[status(thm)],[f5307,f62]) ).
fof(f5337,plain,
less_or_equal(sK1_skl(n1,filling,n0),n0),
inference(resolution,[status(thm)],[f5326,f177]) ).
fof(f5355,plain,
( sK1_skl(n1,filling,n0) = n0
| less(sK1_skl(n1,filling,n0),n0) ),
inference(resolution,[status(thm)],[f5337,f170]) ).
fof(f5356,plain,
sK1_skl(n1,filling,n0) = n0,
inference(forward_subsumption_resolution,[status(thm)],[f5355,f174]) ).
fof(f5361,plain,
( less(n0,n0)
| ~ stoppedIn(n0,filling,n1) ),
inference(paramodulation,[status(thm)],[f5356,f61]) ).
fof(f5364,plain,
less(n0,n0),
inference(forward_subsumption_resolution,[status(thm)],[f5361,f5307]) ).
fof(f5366,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f5364,f174]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR012+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 14:24:47 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 3.74/0.96 % Refutation found
% 3.74/0.96 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.74/0.96 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.01/1.01 % Elapsed time: 0.627542 seconds
% 1.01/1.01 % CPU time: 4.280657 seconds
% 1.01/1.01 % Total memory used: 148.385 MB
% 1.01/1.01 % Net memory used: 144.488 MB
%------------------------------------------------------------------------------