%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR009+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 12.43s 7.14s
% Output : CNFRefutation 12.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 28
% Syntax : Number of formulae : 186 ( 41 unt; 3 def)
% Number of atoms : 638 ( 163 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 702 ( 250 ~; 302 |; 127 &)
% ( 15 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-4 aty)
% Number of functors : 19 ( 19 usr; 9 con; 0-3 aty)
% Number of variables : 355 ( 330 !; 25 ?)
% 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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [Fluent,Time] :
( ( ~ ? [Event] :
( terminates(Event,Fluent,Time)
& happens(Event,Time) )
& ~ releasedAt(Fluent,plus(Time,n1))
& holdsAt(Fluent,Time) )
=> holdsAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [Fluent,Time] :
( ( ~ ? [Event] :
( initiates(Event,Fluent,Time)
& happens(Event,Time) )
& ~ releasedAt(Fluent,plus(Time,n1))
& ~ holdsAt(Fluent,Time) )
=> ~ holdsAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [Event,Time,Fluent] :
( ( initiates(Event,Fluent,Time)
& happens(Event,Time) )
=> holdsAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [Event,Time,Fluent] :
( ( ( terminates(Event,Fluent,Time)
| initiates(Event,Fluent,Time) )
& happens(Event,Time) )
=> ~ releasedAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [Event,Fluent,Time] :
( releases(Event,Fluent,Time)
<=> ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOn ) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [Time,Height1,Height2] :
( ( holdsAt(waterLevel(Height2),Time)
& holdsAt(waterLevel(Height1),Time) )
=> Height1 = Height2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
overflow != tapOn,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X] : filling != waterLevel(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
plus(n1,n1) = n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [X,Y] :
( less_or_equal(X,Y)
<=> ( X = Y
| less(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
~ ? [X] : less(X,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X] :
( less(X,n1)
<=> less_or_equal(X,n0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [X] :
( less(X,n2)
<=> less_or_equal(X,n1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [X] :
( less(X,n3)
<=> less_or_equal(X,n2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [X,Y] :
( less(X,Y)
<=> ( Y != X
& ~ less(Y,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
holdsAt(waterLevel(n0),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,hypothesis,
~ holdsAt(filling,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,conjecture,
holdsAt(filling,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,negated_conjecture,
~ holdsAt(filling,n2),
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(f79,plain,
! [Fluent,Time] :
( holdsAt(Fluent,plus(Time,n1))
| ? [Event] :
( terminates(Event,Fluent,Time)
& happens(Event,Time) )
| releasedAt(Fluent,plus(Time,n1))
| ~ holdsAt(Fluent,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f80,plain,
! [Fluent,Time] :
( holdsAt(Fluent,plus(Time,n1))
| ( terminates(sK4_skl(Time,Fluent),Fluent,Time)
& happens(sK4_skl(Time,Fluent),Time) )
| releasedAt(Fluent,plus(Time,n1))
| ~ holdsAt(Fluent,Time) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(Event,sK4_skl(Time,Fluent))],[f79]) ).
fof(f81,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| happens(sK4_skl(X1,X0),X1)
| releasedAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f83,plain,
! [Fluent,Time] :
( ~ holdsAt(Fluent,plus(Time,n1))
| ? [Event] :
( initiates(Event,Fluent,Time)
& happens(Event,Time) )
| releasedAt(Fluent,plus(Time,n1))
| holdsAt(Fluent,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f84,plain,
! [Fluent,Time] :
( ~ holdsAt(Fluent,plus(Time,n1))
| ( initiates(sK5_skl(Time,Fluent),Fluent,Time)
& happens(sK5_skl(Time,Fluent),Time) )
| releasedAt(Fluent,plus(Time,n1))
| holdsAt(Fluent,Time) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(Event,sK5_skl(Time,Fluent))],[f83]) ).
fof(f85,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| happens(sK5_skl(X1,X0),X1)
| releasedAt(X0,plus(X1,n1))
| holdsAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f86,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| initiates(sK5_skl(X1,X0),X0,X1)
| releasedAt(X0,plus(X1,n1))
| holdsAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
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(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(f95,plain,
! [Event,Time,Fluent] :
( holdsAt(Fluent,plus(Time,n1))
| ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f96,plain,
! [Time,Fluent] :
( holdsAt(Fluent,plus(Time,n1))
| ! [Event] :
( ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f95]) ).
fof(f97,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f104,plain,
! [Event,Time,Fluent] :
( ~ releasedAt(Fluent,plus(Time,n1))
| ( ~ terminates(Event,Fluent,Time)
& ~ initiates(Event,Fluent,Time) )
| ~ happens(Event,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f105,plain,
! [Time,Fluent] :
( ~ releasedAt(Fluent,plus(Time,n1))
| ! [Event] :
( ( ~ terminates(Event,Fluent,Time)
& ~ initiates(Event,Fluent,Time) )
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f104]) ).
fof(f106,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
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(f130,plain,
! [X0,X1,X2] :
( X1 = waterLevel(sK9_skl(X1,X0))
| ~ 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(f136,plain,
! [X0,X1] :
( holdsAt(waterLevel(n3),X1)
| sP1_prd(X1,X0)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f137,plain,
! [X0,X1] :
( holdsAt(filling,X1)
| sP1_prd(X1,X0)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f138,plain,
! [X0,X1] :
( X0 = overflow
| sP1_prd(X1,X0)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
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(f144,plain,
! [Time,Height1,Height2] :
( Height1 = Height2
| ~ holdsAt(waterLevel(Height2),Time)
| ~ holdsAt(waterLevel(Height1),Time) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f145,plain,
! [Height1,Height2] :
( Height1 = Height2
| ! [Time] :
( ~ holdsAt(waterLevel(Height2),Time)
| ~ holdsAt(waterLevel(Height1),Time) ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f146,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ holdsAt(waterLevel(X2),X1)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f149,plain,
overflow != tapOn,
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f150,plain,
! [X0] : filling != waterLevel(X0),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f158,plain,
plus(n0,n1) = n1,
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f161,plain,
plus(n1,n1) = n2,
inference(cnf_transformation,[status(thm)],[f30]) ).
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(f171,plain,
! [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(f179,plain,
! [X] :
( ( ~ less_or_equal(X,n1)
| less(X,n2) )
& ( less_or_equal(X,n1)
| ~ less(X,n2) ) ),
inference(NNF_transformation,[status(thm)],[f40]) ).
fof(f180,plain,
( ! [X] :
( ~ less_or_equal(X,n1)
| less(X,n2) )
& ! [X] :
( less_or_equal(X,n1)
| ~ less(X,n2) ) ),
inference(miniscoping,[status(thm)],[f179]) ).
fof(f182,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f183,plain,
! [X] :
( ( ~ less_or_equal(X,n2)
| less(X,n3) )
& ( less_or_equal(X,n2)
| ~ less(X,n3) ) ),
inference(NNF_transformation,[status(thm)],[f41]) ).
fof(f184,plain,
( ! [X] :
( ~ less_or_equal(X,n2)
| less(X,n3) )
& ! [X] :
( less_or_equal(X,n2)
| ~ less(X,n3) ) ),
inference(miniscoping,[status(thm)],[f183]) ).
fof(f186,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f211,plain,
! [X,Y] :
( ( Y = X
| less(Y,X)
| less(X,Y) )
& ( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f48]) ).
fof(f212,plain,
( ! [X,Y] :
( Y = X
| less(Y,X)
| less(X,Y) )
& ! [X,Y] :
( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(miniscoping,[status(thm)],[f211]) ).
fof(f214,plain,
! [X0,X1] :
( X1 != X0
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f216,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f217,plain,
~ holdsAt(filling,n0),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f222,plain,
~ holdsAt(filling,n2),
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(f235,plain,
! [X0,X1] :
( X1 = tapOn
| ~ sP1_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f234]) ).
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(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(f254,plain,
! [X0] : ~ less(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f214]) ).
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(f259,plain,
less(n1,n2),
inference(resolution,[status(thm)],[f253,f182]) ).
fof(f271,plain,
happens(tapOn,n0),
inference(resolution,[status(thm)],[f139,f256]) ).
fof(f293,plain,
! [X0] :
( less(X0,n3)
| ~ less(X0,n2) ),
inference(resolution,[status(thm)],[f171,f186]) ).
fof(f305,plain,
less(n1,n3),
inference(resolution,[status(thm)],[f293,f259]) ).
fof(f318,plain,
less(n0,n1),
inference(resolution,[status(thm)],[f178,f253]) ).
fof(f321,plain,
! [X0,X1,X2] :
( ~ sP0_prd(X1,X2,X0)
| holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f97,f116]) ).
fof(f345,plain,
! [X0,X1,X2] :
( ~ sP0_prd(X1,X2,X0)
| ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f106,f116]) ).
fof(f373,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| X0 = waterLevel(sK9_skl(X0,sK7_skl(X1,X0))) ),
inference(resolution,[status(thm)],[f130,f94]) ).
fof(f377,plain,
! [X0,X1] :
( X0 = tapOn
| holdsAt(waterLevel(n3),X1)
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f136,f235]) ).
fof(f382,plain,
! [X0,X1] :
( X0 = tapOn
| holdsAt(filling,X1)
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f137,f235]) ).
fof(f445,plain,
! [X0,X1] :
( X0 = tapOn
| X0 = overflow
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f138,f235]) ).
fof(f446,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(n0,X0)),X0),
inference(resolution,[status(thm)],[f252,f216]) ).
fof(f922,plain,
! [X0,X1,X2] :
( ~ sP2_prd(X2,X0)
| holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f321,f231]) ).
fof(f1044,plain,
! [X0,X1,X2] :
( ~ sP2_prd(X2,X0)
| ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f345,f231]) ).
fof(f1085,plain,
! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1)
| X0 = waterLevel(sK9_skl(X0,sK7_skl(n1,X0))) ),
inference(paramodulation,[status(thm)],[f161,f373]) ).
fof(f1214,plain,
! [X0,X1] :
( ~ holdsAt(X1,plus(X0,n1))
| releasedAt(X1,plus(X0,n1))
| holdsAt(X1,X0)
| sK5_skl(X0,X1) = tapOn
| holdsAt(filling,X0) ),
inference(resolution,[status(thm)],[f382,f85]) ).
fof(f1404,plain,
trajectory(filling,n0,waterLevel(n1),n1),
inference(paramodulation,[status(thm)],[f158,f446]) ).
fof(f1906,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)],[f1404,f75]) ).
fof(f1907,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,f1906]) ).
fof(f1908,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,f1907]) ).
fof(f1909,plain,
! [X0] :
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1908,f318]) ).
fof(f2491,plain,
! [X0] :
( holdsAt(filling,plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(resolution,[status(thm)],[f922,f257]) ).
fof(f2683,plain,
! [X0] :
( ~ releasedAt(filling,plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(resolution,[status(thm)],[f1044,f257]) ).
fof(f3891,plain,
holdsAt(filling,plus(n0,n1)),
inference(resolution,[status(thm)],[f2491,f271]) ).
fof(f3892,plain,
holdsAt(filling,n1),
inference(forward_demodulation,[status(thm)],[f158,f3891]) ).
fof(f3895,plain,
( holdsAt(filling,plus(n1,n1))
| happens(sK4_skl(n1,filling),n1)
| releasedAt(filling,plus(n1,n1)) ),
inference(resolution,[status(thm)],[f3892,f81]) ).
fof(f3900,plain,
( holdsAt(filling,plus(n1,n1))
| happens(sK4_skl(n1,filling),n1)
| releasedAt(filling,n2) ),
inference(forward_demodulation,[status(thm)],[f161,f3895]) ).
fof(f3901,plain,
( holdsAt(filling,n2)
| happens(sK4_skl(n1,filling),n1)
| releasedAt(filling,n2) ),
inference(forward_demodulation,[status(thm)],[f161,f3900]) ).
fof(f3902,plain,
( happens(sK4_skl(n1,filling),n1)
| releasedAt(filling,n2) ),
inference(forward_subsumption_resolution,[status(thm)],[f3901,f222]) ).
fof(f3910,plain,
! [X0] :
( ~ holdsAt(X0,n1)
| releasedAt(X0,plus(n0,n1))
| holdsAt(X0,n0)
| sK5_skl(n0,X0) = tapOn
| holdsAt(filling,n0) ),
inference(paramodulation,[status(thm)],[f158,f1214]) ).
fof(f3917,plain,
! [X0] :
( ~ holdsAt(X0,n1)
| releasedAt(X0,n1)
| holdsAt(X0,n0)
| sK5_skl(n0,X0) = tapOn
| holdsAt(filling,n0) ),
inference(forward_demodulation,[status(thm)],[f158,f3910]) ).
fof(f3918,plain,
! [X0] :
( ~ holdsAt(X0,n1)
| releasedAt(X0,n1)
| holdsAt(X0,n0)
| sK5_skl(n0,X0) = tapOn ),
inference(forward_subsumption_resolution,[status(thm)],[f3917,f217]) ).
fof(f4089,plain,
~ releasedAt(filling,plus(n0,n1)),
inference(resolution,[status(thm)],[f2683,f271]) ).
fof(f4090,plain,
~ releasedAt(filling,n1),
inference(forward_demodulation,[status(thm)],[f158,f4089]) ).
fof(f4094,plain,
( ~ releasedAt(filling,n2)
| filling = waterLevel(sK9_skl(filling,sK7_skl(n1,filling))) ),
inference(resolution,[status(thm)],[f4090,f1085]) ).
fof(f4097,plain,
~ releasedAt(filling,n2),
inference(forward_subsumption_resolution,[status(thm)],[f4094,f150]) ).
fof(f4099,plain,
happens(sK4_skl(n1,filling),n1),
inference(backward_subsumption_resolution,[status(thm)],[f3902,f4097]) ).
fof(f4107,plain,
( sK4_skl(n1,filling) = tapOn
| holdsAt(waterLevel(n3),n1) ),
inference(resolution,[status(thm)],[f4099,f377]) ).
fof(f4109,plain,
( sK4_skl(n1,filling) = tapOn
| sK4_skl(n1,filling) = overflow ),
inference(resolution,[status(thm)],[f4099,f445]) ).
fof(f4441,plain,
( releasedAt(filling,n1)
| holdsAt(filling,n0)
| sK5_skl(n0,filling) = tapOn ),
inference(resolution,[status(thm)],[f3918,f3892]) ).
fof(f4444,plain,
( releasedAt(filling,n1)
| sK5_skl(n0,filling) = tapOn ),
inference(forward_subsumption_resolution,[status(thm)],[f4441,f217]) ).
fof(f4445,plain,
sK5_skl(n0,filling) = tapOn,
inference(forward_subsumption_resolution,[status(thm)],[f4444,f4090]) ).
fof(f4452,plain,
( ~ holdsAt(filling,plus(n0,n1))
| initiates(tapOn,filling,n0)
| releasedAt(filling,plus(n0,n1))
| holdsAt(filling,n0) ),
inference(paramodulation,[status(thm)],[f4445,f86]) ).
fof(f4469,plain,
( ~ holdsAt(filling,plus(n0,n1))
| initiates(tapOn,filling,n0)
| releasedAt(filling,n1)
| holdsAt(filling,n0) ),
inference(forward_demodulation,[status(thm)],[f158,f4452]) ).
fof(f4470,plain,
( ~ holdsAt(filling,n1)
| initiates(tapOn,filling,n0)
| releasedAt(filling,n1)
| holdsAt(filling,n0) ),
inference(forward_demodulation,[status(thm)],[f158,f4469]) ).
fof(f4471,plain,
( ~ holdsAt(filling,n1)
| initiates(tapOn,filling,n0)
| releasedAt(filling,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[f4470,f217]) ).
fof(f5085,plain,
( sK4_skl(n1,filling) = overflow
| happens(tapOn,n1) ),
inference(paramodulation,[status(thm)],[f4109,f4099]) ).
fof(f5088,plain,
( holdsAt(filling,plus(n1,n1))
| sK4_skl(n1,filling) = overflow ),
inference(resolution,[status(thm)],[f5085,f2491]) ).
fof(f5099,plain,
( holdsAt(filling,n2)
| sK4_skl(n1,filling) = overflow ),
inference(forward_demodulation,[status(thm)],[f161,f5088]) ).
fof(f5100,plain,
sK4_skl(n1,filling) = overflow,
inference(forward_subsumption_resolution,[status(thm)],[f5099,f222]) ).
fof(f5107,plain,
( overflow = tapOn
| holdsAt(waterLevel(n3),n1) ),
inference(backward_demodulation,[status(thm)],[f5100,f4107]) ).
fof(f5113,plain,
holdsAt(waterLevel(n3),n1),
inference(forward_subsumption_resolution,[status(thm)],[f5107,f149]) ).
fof(f5165,plain,
! [X0] :
( X0 = n3
| ~ holdsAt(waterLevel(X0),n1) ),
inference(resolution,[status(thm)],[f5113,f146]) ).
fof(f7984,plain,
( ~ holdsAt(filling,n1)
| initiates(tapOn,filling,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4471,f4090]) ).
fof(f7985,plain,
initiates(tapOn,filling,n0),
inference(resolution,[status(thm)],[f7984,f3892]) ).
fof(f8000,plain,
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1)
| ~ happens(tapOn,n0) ),
inference(resolution,[status(thm)],[f7985,f1909]) ).
fof(f8024,plain,
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[f8000,f271]) ).
fof(f8074,plain,
( n1 = n3
| stoppedIn(n0,filling,n1) ),
inference(resolution,[status(thm)],[f8024,f5165]) ).
fof(f8101,plain,
( less(sK1_skl(n1,filling,n0),n1)
| n1 = n3 ),
inference(resolution,[status(thm)],[f8074,f62]) ).
fof(f8125,plain,
( less_or_equal(sK1_skl(n1,filling,n0),n0)
| n1 = n3 ),
inference(resolution,[status(thm)],[f8101,f177]) ).
fof(f8129,plain,
( sK1_skl(n1,filling,n0) = n0
| less(sK1_skl(n1,filling,n0),n0)
| n1 = n3 ),
inference(resolution,[status(thm)],[f8125,f170]) ).
fof(f8130,plain,
( sK1_skl(n1,filling,n0) = n0
| n1 = n3 ),
inference(forward_subsumption_resolution,[status(thm)],[f8129,f174]) ).
fof(f8136,plain,
( n1 = n3
| less(n0,n0)
| ~ stoppedIn(n0,filling,n1) ),
inference(paramodulation,[status(thm)],[f8130,f61]) ).
fof(f8141,plain,
( n1 = n3
| less(n0,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f8136,f8074]) ).
fof(f8463,plain,
less(n3,n3),
inference(backward_demodulation,[status(thm)],[f8478,f305]) ).
fof(f8478,plain,
n1 = n3,
inference(forward_subsumption_resolution,[status(thm)],[f8141,f174]) ).
fof(f8982,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f8463,f254]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR009+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n014.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Mon Sep 21 14:24:11 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.15/5.41 % Drodi V4.1.1
% 12.43/7.14 % Refutation found
% 12.43/7.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.43/7.14 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.43/7.18 % Elapsed time: 1.779927 seconds
% 12.43/7.18 % CPU time: 13.740796 seconds
% 12.43/7.18 % Total memory used: 225.594 MB
% 12.43/7.18 % Net memory used: 214.432 MB
%------------------------------------------------------------------------------