%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR007+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 : n017.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 32.71s 4.67s
% Output : CNFRefutation 32.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 30
% Syntax : Number of formulae : 220 ( 47 unt; 3 def)
% Number of atoms : 739 ( 246 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 785 ( 266 ~; 368 |; 129 &)
% ( 16 <=>; 6 =>; 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 : 18 ( 18 usr; 9 con; 0-3 aty)
% Number of variables : 370 ( 347 !; 23 ?)
% 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(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(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(f14,axiom,
! [Event,Fluent,Time] :
( terminates(Event,Fluent,Time)
<=> ( ( Fluent = filling
& Event = overflow )
| ( Fluent = filling
& Event = tapOff ) ) ),
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(f19,axiom,
tapOff != tapOn,
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(f28,axiom,
plus(n0,n2) = n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X,Y] : plus(X,Y) = plus(Y,X),
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(f53,hypothesis,
~ releasedAt(filling,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,conjecture,
~ holdsAt(waterLevel(n3),n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,negated_conjecture,
~ ~ holdsAt(waterLevel(n3),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(f60,plain,
! [X0,X1,X2] :
( happens(sK0_skl(X2,X1,X0),sK1_skl(X2,X1,X0))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
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(f63,plain,
! [X0,X1,X2] :
( terminates(sK0_skl(X2,X1,X0),X1,sK1_skl(X2,X1,X0))
| ~ 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(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(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(f118,plain,
! [Event,Fluent,Time] :
( ( ( ( Fluent != filling
| Event != overflow )
& ( Fluent != filling
| Event != tapOff ) )
| terminates(Event,Fluent,Time) )
& ( ( Fluent = filling
& Event = overflow )
| ( Fluent = filling
& Event = tapOff )
| ~ terminates(Event,Fluent,Time) ) ),
inference(NNF_transformation,[status(thm)],[f14]) ).
fof(f119,plain,
( ! [Event,Fluent] :
( ( ( Fluent != filling
| Event != overflow )
& ( Fluent != filling
| Event != tapOff ) )
| ! [Time] : terminates(Event,Fluent,Time) )
& ! [Event,Fluent] :
( ( Fluent = filling
& Event = overflow )
| ( Fluent = filling
& Event = tapOff )
| ! [Time] : ~ terminates(Event,Fluent,Time) ) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f120,plain,
! [X0,X1,X2] :
( X0 = overflow
| X0 = tapOff
| ~ terminates(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
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(f147,plain,
tapOff != tapOn,
inference(cnf_transformation,[status(thm)],[f19]) ).
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(f159,plain,
plus(n0,n2) = n2,
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f167,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[status(thm)],[f36]) ).
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(f181,plain,
! [X0] :
( less_or_equal(X0,n1)
| ~ less(X0,n2) ),
inference(cnf_transformation,[status(thm)],[f180]) ).
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(f213,plain,
! [X0,X1] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f214,plain,
! [X0,X1] :
( X1 != X0
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f215,plain,
! [X0,X1] :
( X1 = X0
| less(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(f220,plain,
~ releasedAt(filling,n0),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f222,plain,
holdsAt(waterLevel(n3),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(f260,plain,
! [X0] :
( X0 = n3
| ~ holdsAt(waterLevel(X0),n2) ),
inference(resolution,[status(thm)],[f146,f222]) ).
fof(f261,plain,
less(n1,n2),
inference(resolution,[status(thm)],[f253,f182]) ).
fof(f264,plain,
less(n2,n3),
inference(resolution,[status(thm)],[f186,f253]) ).
fof(f274,plain,
happens(tapOn,n0),
inference(resolution,[status(thm)],[f139,f256]) ).
fof(f283,plain,
! [X0] :
( ~ holdsAt(X0,n1)
| happens(sK5_skl(n0,X0),n0)
| releasedAt(X0,plus(n0,n1))
| holdsAt(X0,n0) ),
inference(paramodulation,[status(thm)],[f158,f85]) ).
fof(f286,plain,
! [X0] :
( ~ holdsAt(X0,n1)
| happens(sK5_skl(n0,X0),n0)
| releasedAt(X0,n1)
| holdsAt(X0,n0) ),
inference(forward_demodulation,[status(thm)],[f158,f283]) ).
fof(f294,plain,
plus(n2,n0) = n2,
inference(backward_demodulation,[status(thm)],[f167,f159]) ).
fof(f305,plain,
! [X0] :
( less(X0,n3)
| ~ less(X0,n2) ),
inference(resolution,[status(thm)],[f171,f186]) ).
fof(f306,plain,
! [X0] :
( less(X0,n2)
| ~ less(X0,n1) ),
inference(resolution,[status(thm)],[f171,f182]) ).
fof(f320,plain,
less(n1,n3),
inference(resolution,[status(thm)],[f305,f261]) ).
fof(f343,plain,
! [X0,X1,X2] :
( holdsAt(X1,plus(X0,n1))
| ~ happens(X2,X0)
| ~ sP0_prd(X0,X1,X2) ),
inference(resolution,[status(thm)],[f116,f97]) ).
fof(f348,plain,
less(n0,n1),
inference(resolution,[status(thm)],[f178,f253]) ).
fof(f359,plain,
less(n0,n2),
inference(resolution,[status(thm)],[f348,f306]) ).
fof(f381,plain,
! [X0,X1,X2] :
( ~ stoppedIn(X2,X1,X0)
| sK0_skl(X0,X1,X2) = overflow
| sK0_skl(X0,X1,X2) = tapOff ),
inference(resolution,[status(thm)],[f120,f63]) ).
fof(f386,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(f390,plain,
! [X0,X1] :
( X0 = tapOn
| holdsAt(waterLevel(n3),X1)
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f136,f235]) ).
fof(f397,plain,
! [X0,X1] :
( X0 = tapOn
| holdsAt(filling,X1)
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f137,f235]) ).
fof(f404,plain,
! [X0,X1] :
( X0 = tapOn
| X0 = overflow
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f138,f235]) ).
fof(f424,plain,
! [X0] :
( less_or_equal(X0,n0)
| X0 = n1
| less(n1,X0) ),
inference(resolution,[status(thm)],[f215,f177]) ).
fof(f432,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(n0,X0)),X0),
inference(resolution,[status(thm)],[f252,f216]) ).
fof(f698,plain,
! [X0,X1,X2] :
( ~ stoppedIn(X2,X1,X0)
| sK0_skl(X0,X1,X2) = tapOn
| sK0_skl(X0,X1,X2) = overflow ),
inference(resolution,[status(thm)],[f404,f60]) ).
fof(f1025,plain,
! [X0] :
( holdsAt(X0,plus(n0,n1))
| ~ sP0_prd(n0,X0,tapOn) ),
inference(resolution,[status(thm)],[f343,f274]) ).
fof(f1027,plain,
! [X0] :
( holdsAt(X0,n1)
| ~ sP0_prd(n0,X0,tapOn) ),
inference(forward_demodulation,[status(thm)],[f158,f1025]) ).
fof(f1232,plain,
( ~ releasedAt(filling,plus(n0,n1))
| filling = waterLevel(sK9_skl(filling,sK7_skl(n0,filling))) ),
inference(resolution,[status(thm)],[f386,f220]) ).
fof(f1237,plain,
( ~ releasedAt(filling,n1)
| filling = waterLevel(sK9_skl(filling,sK7_skl(n0,filling))) ),
inference(forward_demodulation,[status(thm)],[f158,f1232]) ).
fof(f1238,plain,
~ releasedAt(filling,n1),
inference(forward_subsumption_resolution,[status(thm)],[f1237,f150]) ).
fof(f1598,plain,
! [X0] :
( X0 = n0
| less(X0,n0)
| X0 = n1
| less(n1,X0) ),
inference(resolution,[status(thm)],[f424,f170]) ).
fof(f1599,plain,
! [X0] :
( X0 = n0
| X0 = n1
| less(n1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1598,f174]) ).
fof(f1681,plain,
! [X0] :
( ~ less(X0,n1)
| X0 = n0
| X0 = n1 ),
inference(resolution,[status(thm)],[f1599,f213]) ).
fof(f1703,plain,
! [X0] :
( ~ sP2_prd(X0,tapOn)
| holdsAt(X0,n1) ),
inference(resolution,[status(thm)],[f1027,f231]) ).
fof(f1705,plain,
holdsAt(filling,n1),
inference(resolution,[status(thm)],[f1703,f257]) ).
fof(f1711,plain,
( happens(sK5_skl(n0,filling),n0)
| releasedAt(filling,n1)
| holdsAt(filling,n0) ),
inference(resolution,[status(thm)],[f1705,f286]) ).
fof(f1714,plain,
( happens(sK5_skl(n0,filling),n0)
| releasedAt(filling,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1711,f217]) ).
fof(f1718,plain,
trajectory(filling,n0,waterLevel(n1),n1),
inference(paramodulation,[status(thm)],[f158,f432]) ).
fof(f1720,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(X0,n0)),X0),
inference(paramodulation,[status(thm)],[f167,f432]) ).
fof(f1828,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)],[f1718,f75]) ).
fof(f1829,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,f1828]) ).
fof(f1830,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,f1829]) ).
fof(f1831,plain,
! [X0] :
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1830,f348]) ).
fof(f2225,plain,
trajectory(filling,n0,waterLevel(n2),n2),
inference(paramodulation,[status(thm)],[f294,f1720]) ).
fof(f2235,plain,
! [X0] :
( holdsAt(waterLevel(n2),plus(n0,n2))
| stoppedIn(n0,filling,plus(n0,n2))
| ~ less(n0,n2)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(resolution,[status(thm)],[f2225,f75]) ).
fof(f2236,plain,
! [X0] :
( holdsAt(waterLevel(n2),plus(n0,n2))
| stoppedIn(n0,filling,plus(n2,n0))
| ~ less(n0,n2)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_demodulation,[status(thm)],[f167,f2235]) ).
fof(f2237,plain,
! [X0] :
( holdsAt(waterLevel(n2),plus(n0,n2))
| stoppedIn(n0,filling,n2)
| ~ less(n0,n2)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_demodulation,[status(thm)],[f294,f2236]) ).
fof(f2238,plain,
! [X0] :
( holdsAt(waterLevel(n2),plus(n2,n0))
| stoppedIn(n0,filling,n2)
| ~ less(n0,n2)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_demodulation,[status(thm)],[f167,f2237]) ).
fof(f2239,plain,
! [X0] :
( holdsAt(waterLevel(n2),n2)
| stoppedIn(n0,filling,n2)
| ~ less(n0,n2)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_demodulation,[status(thm)],[f294,f2238]) ).
fof(f2240,plain,
! [X0] :
( holdsAt(waterLevel(n2),n2)
| stoppedIn(n0,filling,n2)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2239,f359]) ).
fof(f2970,plain,
happens(sK5_skl(n0,filling),n0),
inference(forward_subsumption_resolution,[status(thm)],[f1714,f1238]) ).
fof(f2971,plain,
( sK5_skl(n0,filling) = tapOn
| holdsAt(filling,n0) ),
inference(resolution,[status(thm)],[f2970,f397]) ).
fof(f2981,plain,
sK5_skl(n0,filling) = tapOn,
inference(forward_subsumption_resolution,[status(thm)],[f2971,f217]) ).
fof(f2985,plain,
( ~ holdsAt(filling,plus(n0,n1))
| initiates(tapOn,filling,n0)
| releasedAt(filling,plus(n0,n1))
| holdsAt(filling,n0) ),
inference(paramodulation,[status(thm)],[f2981,f86]) ).
fof(f2986,plain,
( ~ holdsAt(filling,plus(n0,n1))
| initiates(tapOn,filling,n0)
| releasedAt(filling,n1)
| holdsAt(filling,n0) ),
inference(forward_demodulation,[status(thm)],[f158,f2985]) ).
fof(f2987,plain,
( ~ holdsAt(filling,n1)
| initiates(tapOn,filling,n0)
| releasedAt(filling,n1)
| holdsAt(filling,n0) ),
inference(forward_demodulation,[status(thm)],[f158,f2986]) ).
fof(f2988,plain,
( ~ holdsAt(filling,n1)
| initiates(tapOn,filling,n0)
| releasedAt(filling,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[f2987,f217]) ).
fof(f4501,plain,
( holdsAt(waterLevel(n2),n2)
| stoppedIn(n0,filling,n2)
| ~ initiates(tapOn,filling,n0) ),
inference(resolution,[status(thm)],[f2240,f274]) ).
fof(f5403,plain,
( ~ holdsAt(filling,n1)
| initiates(tapOn,filling,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2988,f1238]) ).
fof(f5404,plain,
initiates(tapOn,filling,n0),
inference(resolution,[status(thm)],[f5403,f1705]) ).
fof(f6051,plain,
( holdsAt(waterLevel(n2),n2)
| stoppedIn(n0,filling,n2) ),
inference(forward_subsumption_resolution,[status(thm)],[f4501,f5404]) ).
fof(f6054,plain,
( n2 = n3
| stoppedIn(n0,filling,n2) ),
inference(resolution,[status(thm)],[f6051,f260]) ).
fof(f6064,plain,
( sK0_skl(n2,filling,n0) = tapOn
| sK0_skl(n2,filling,n0) = overflow
| n2 = n3 ),
inference(resolution,[status(thm)],[f6054,f698]) ).
fof(f6066,plain,
( sK0_skl(n2,filling,n0) = overflow
| sK0_skl(n2,filling,n0) = tapOff
| n2 = n3 ),
inference(resolution,[status(thm)],[f6054,f381]) ).
fof(f6074,plain,
( less(sK1_skl(n2,filling,n0),n2)
| n2 = n3 ),
inference(resolution,[status(thm)],[f6054,f62]) ).
fof(f6080,plain,
( less_or_equal(sK1_skl(n2,filling,n0),n1)
| n2 = n3 ),
inference(resolution,[status(thm)],[f6074,f181]) ).
fof(f6092,plain,
( sK1_skl(n2,filling,n0) = n1
| less(sK1_skl(n2,filling,n0),n1)
| n2 = n3 ),
inference(resolution,[status(thm)],[f6080,f170]) ).
fof(f6152,plain,
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1)
| ~ initiates(tapOn,filling,n0) ),
inference(resolution,[status(thm)],[f1831,f274]) ).
fof(f6155,plain,
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[f6152,f5404]) ).
fof(f6213,plain,
! [X0] :
( X0 = n1
| ~ holdsAt(waterLevel(X0),n1)
| stoppedIn(n0,filling,n1) ),
inference(resolution,[status(thm)],[f6155,f146]) ).
fof(f7664,plain,
( sK0_skl(n2,filling,n0) = overflow
| n2 = n3
| sK0_skl(n2,filling,n0) = overflow
| tapOn = tapOff
| n2 = n3 ),
inference(paramodulation,[status(thm)],[f6064,f6066]) ).
fof(f7671,plain,
( sK0_skl(n2,filling,n0) = overflow
| tapOn = tapOff
| n2 = n3 ),
inference(duplicate_literals_removal,[status(thm)],[f7664]) ).
fof(f7672,plain,
( sK0_skl(n2,filling,n0) = overflow
| n2 = n3 ),
inference(forward_subsumption_resolution,[status(thm)],[f7671,f147]) ).
fof(f7678,plain,
( n2 = n3
| happens(overflow,sK1_skl(n2,filling,n0))
| ~ stoppedIn(n0,filling,n2) ),
inference(paramodulation,[status(thm)],[f7672,f60]) ).
fof(f7679,plain,
( n2 = n3
| happens(overflow,sK1_skl(n2,filling,n0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7678,f6054]) ).
fof(f7683,plain,
( overflow = tapOn
| holdsAt(filling,sK1_skl(n2,filling,n0))
| n2 = n3 ),
inference(resolution,[status(thm)],[f7679,f397]) ).
fof(f7685,plain,
( overflow = tapOn
| holdsAt(waterLevel(n3),sK1_skl(n2,filling,n0))
| n2 = n3 ),
inference(resolution,[status(thm)],[f7679,f390]) ).
fof(f7693,plain,
( holdsAt(filling,sK1_skl(n2,filling,n0))
| n2 = n3 ),
inference(forward_subsumption_resolution,[status(thm)],[f7683,f149]) ).
fof(f7694,plain,
( holdsAt(waterLevel(n3),sK1_skl(n2,filling,n0))
| n2 = n3 ),
inference(forward_subsumption_resolution,[status(thm)],[f7685,f149]) ).
fof(f10603,plain,
( sK1_skl(n2,filling,n0) = n0
| sK1_skl(n2,filling,n0) = n1
| sK1_skl(n2,filling,n0) = n1
| n2 = n3 ),
inference(resolution,[status(thm)],[f6092,f1681]) ).
fof(f10612,plain,
( sK1_skl(n2,filling,n0) = n0
| sK1_skl(n2,filling,n0) = n1
| n2 = n3 ),
inference(duplicate_literals_removal,[status(thm)],[f10603]) ).
fof(f10707,plain,
( sK1_skl(n2,filling,n0) = n1
| n2 = n3
| holdsAt(filling,n0)
| n2 = n3 ),
inference(paramodulation,[status(thm)],[f10612,f7693]) ).
fof(f10742,plain,
( sK1_skl(n2,filling,n0) = n1
| holdsAt(filling,n0)
| n2 = n3 ),
inference(duplicate_literals_removal,[status(thm)],[f10707]) ).
fof(f10743,plain,
( sK1_skl(n2,filling,n0) = n1
| n2 = n3 ),
inference(forward_subsumption_resolution,[status(thm)],[f10742,f217]) ).
fof(f10820,plain,
( n2 = n3
| holdsAt(waterLevel(n3),n1)
| n2 = n3 ),
inference(paramodulation,[status(thm)],[f10743,f7694]) ).
fof(f10854,plain,
( holdsAt(waterLevel(n3),n1)
| n2 = n3 ),
inference(duplicate_literals_removal,[status(thm)],[f10820]) ).
fof(f10917,plain,
( n3 = n1
| stoppedIn(n0,filling,n1)
| n2 = n3 ),
inference(resolution,[status(thm)],[f10854,f6213]) ).
fof(f11239,plain,
( less(sK1_skl(n1,filling,n0),n1)
| n3 = n1
| n2 = n3 ),
inference(resolution,[status(thm)],[f10917,f62]) ).
fof(f12180,plain,
( less_or_equal(sK1_skl(n1,filling,n0),n0)
| n3 = n1
| n2 = n3 ),
inference(resolution,[status(thm)],[f11239,f177]) ).
fof(f12577,plain,
( sK1_skl(n1,filling,n0) = n0
| less(sK1_skl(n1,filling,n0),n0)
| n3 = n1
| n2 = n3 ),
inference(resolution,[status(thm)],[f12180,f170]) ).
fof(f12578,plain,
( sK1_skl(n1,filling,n0) = n0
| n3 = n1
| n2 = n3 ),
inference(forward_subsumption_resolution,[status(thm)],[f12577,f174]) ).
fof(f12584,plain,
( n3 = n1
| n2 = n3
| less(n0,n0)
| ~ stoppedIn(n0,filling,n1) ),
inference(paramodulation,[status(thm)],[f12578,f61]) ).
fof(f12591,plain,
( n3 = n1
| n2 = n3
| less(n0,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f12584,f10917]) ).
fof(f12631,plain,
( n3 = n1
| n2 = n3 ),
inference(forward_subsumption_resolution,[status(thm)],[f12591,f174]) ).
fof(f12912,plain,
( n2 = n3
| less(n3,n3) ),
inference(paramodulation,[status(thm)],[f12631,f320]) ).
fof(f12978,plain,
n2 = n3,
inference(forward_subsumption_resolution,[status(thm)],[f12912,f254]) ).
fof(f13442,plain,
less(n2,n2),
inference(backward_demodulation,[status(thm)],[f12978,f264]) ).
fof(f13722,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f13442,f254]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR007+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n017.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 14:18:57 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 32.71/4.67 % Refutation found
% 32.71/4.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 32.71/4.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.33/4.72 % Elapsed time: 4.278188 seconds
% 1.33/4.72 % CPU time: 33.438499 seconds
% 1.33/4.72 % Total memory used: 266.497 MB
% 1.33/4.72 % Net memory used: 249.692 MB
%------------------------------------------------------------------------------