%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR008+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 : n005.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 11.12s 1.85s
% Output : CNFRefutation 11.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 34
% Syntax : Number of formulae : 242 ( 62 unt; 3 def)
% Number of atoms : 769 ( 212 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 824 ( 297 ~; 368 |; 135 &)
% ( 16 <=>; 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 : 395 ( 370 !; 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/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(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/sandbox/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/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(f9,axiom,
! [Event,Time,Fluent] :
( ( initiates(Event,Fluent,Time)
& happens(Event,Time) )
=> holdsAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [Event,Time,Fluent] :
( ( terminates(Event,Fluent,Time)
& happens(Event,Time) )
=> ~ holdsAt(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(f14,axiom,
! [Event,Fluent,Time] :
( terminates(Event,Fluent,Time)
<=> ( ( Fluent = filling
& Event = overflow )
| ( Fluent = filling
& Event = tapOff ) ) ),
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(f18,axiom,
! [Time,Height1,Height2] :
( ( holdsAt(waterLevel(Height2),Time)
& holdsAt(waterLevel(Height1),Time) )
=> Height1 = Height2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
tapOff != tapOn,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
tapOff != overflow,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
overflow != tapOn,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X] : filling != waterLevel(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
plus(n0,n2) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
plus(n1,n1) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X,Y] : plus(X,Y) = plus(Y,X),
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(f40,axiom,
! [X] :
( less(X,n2)
<=> less_or_equal(X,n1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [X] :
( less(X,n3)
<=> less_or_equal(X,n2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [X,Y] :
( less(X,Y)
<=> ( Y != X
& ~ less(Y,X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
holdsAt(waterLevel(n0),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,hypothesis,
~ holdsAt(filling,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,hypothesis,
~ releasedAt(filling,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,conjecture,
holdsAt(waterLevel(n2),n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,negated_conjecture,
~ holdsAt(waterLevel(n2),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(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(f82,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| terminates(sK4_skl(X1,X0),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(f98,plain,
! [Event,Time,Fluent] :
( ~ holdsAt(Fluent,plus(Time,n1))
| ~ terminates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f99,plain,
! [Time,Fluent] :
( ~ holdsAt(Fluent,plus(Time,n1))
| ! [Event] :
( ~ terminates(Event,Fluent,Time)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f98]) ).
fof(f100,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ terminates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
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(f148,plain,
tapOff != overflow,
inference(cnf_transformation,[status(thm)],[f20]) ).
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(f161,plain,
plus(n1,n1) = n2,
inference(cnf_transformation,[status(thm)],[f30]) ).
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(n2),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,
less(n1,n2),
inference(resolution,[status(thm)],[f253,f182]) ).
fof(f272,plain,
happens(tapOn,n0),
inference(resolution,[status(thm)],[f139,f256]) ).
fof(f278,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(f280,plain,
! [X0] :
( ~ holdsAt(X0,n1)
| happens(sK5_skl(n0,X0),n0)
| releasedAt(X0,n1)
| holdsAt(X0,n0) ),
inference(forward_demodulation,[status(thm)],[f158,f278]) ).
fof(f285,plain,
plus(n2,n0) = n2,
inference(backward_demodulation,[status(thm)],[f167,f159]) ).
fof(f292,plain,
! [X0] :
( less(X0,n3)
| ~ less(X0,n2) ),
inference(resolution,[status(thm)],[f171,f186]) ).
fof(f293,plain,
! [X0] :
( less(X0,n2)
| ~ less(X0,n1) ),
inference(resolution,[status(thm)],[f171,f182]) ).
fof(f310,plain,
less(n1,n3),
inference(resolution,[status(thm)],[f292,f260]) ).
fof(f319,plain,
! [X0,X1,X2] :
( ~ sP0_prd(X1,X2,X0)
| holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f97,f116]) ).
fof(f323,plain,
! [X0,X1,X2] :
( ~ stoppedIn(X2,X1,X0)
| ~ holdsAt(X1,plus(sK1_skl(X0,X1,X2),n1))
| ~ happens(sK0_skl(X0,X1,X2),sK1_skl(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f100,f63]) ).
fof(f324,plain,
! [X0,X1,X2] :
( ~ stoppedIn(X2,X0,X1)
| ~ holdsAt(X0,plus(sK1_skl(X1,X0,X2),n1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f323,f60]) ).
fof(f335,plain,
less(n0,n1),
inference(resolution,[status(thm)],[f178,f253]) ).
fof(f337,plain,
less(n0,n2),
inference(resolution,[status(thm)],[f335,f293]) ).
fof(f374,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(f380,plain,
! [X0,X1] :
( X0 = tapOn
| holdsAt(waterLevel(n3),X1)
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f136,f235]) ).
fof(f387,plain,
! [X0,X1] :
( X0 = tapOn
| holdsAt(filling,X1)
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f137,f235]) ).
fof(f390,plain,
! [X0,X1] :
( X0 = tapOn
| X0 = overflow
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f138,f235]) ).
fof(f406,plain,
! [X0] :
( less_or_equal(X0,n0)
| X0 = n1
| less(n1,X0) ),
inference(resolution,[status(thm)],[f215,f177]) ).
fof(f436,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(n0,X0)),X0),
inference(resolution,[status(thm)],[f252,f216]) ).
fof(f882,plain,
! [X0] :
( ~ sP0_prd(n0,X0,tapOn)
| holdsAt(X0,plus(n0,n1)) ),
inference(resolution,[status(thm)],[f319,f272]) ).
fof(f884,plain,
! [X0] :
( ~ sP0_prd(n0,X0,tapOn)
| holdsAt(X0,n1) ),
inference(forward_demodulation,[status(thm)],[f158,f882]) ).
fof(f1177,plain,
( ~ releasedAt(filling,plus(n0,n1))
| filling = waterLevel(sK9_skl(filling,sK7_skl(n0,filling))) ),
inference(resolution,[status(thm)],[f374,f220]) ).
fof(f1184,plain,
( ~ releasedAt(filling,n1)
| filling = waterLevel(sK9_skl(filling,sK7_skl(n0,filling))) ),
inference(forward_demodulation,[status(thm)],[f158,f1177]) ).
fof(f1185,plain,
~ releasedAt(filling,n1),
inference(forward_subsumption_resolution,[status(thm)],[f1184,f150]) ).
fof(f1232,plain,
( ~ releasedAt(filling,plus(n1,n1))
| filling = waterLevel(sK9_skl(filling,sK7_skl(n1,filling))) ),
inference(resolution,[status(thm)],[f1185,f374]) ).
fof(f1234,plain,
( ~ releasedAt(filling,n2)
| filling = waterLevel(sK9_skl(filling,sK7_skl(n1,filling))) ),
inference(forward_demodulation,[status(thm)],[f161,f1232]) ).
fof(f1235,plain,
~ releasedAt(filling,n2),
inference(forward_subsumption_resolution,[status(thm)],[f1234,f150]) ).
fof(f1468,plain,
! [X0] :
( X0 = n0
| less(X0,n0)
| X0 = n1
| less(n1,X0) ),
inference(resolution,[status(thm)],[f406,f170]) ).
fof(f1469,plain,
! [X0] :
( X0 = n0
| X0 = n1
| less(n1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1468,f174]) ).
fof(f1471,plain,
trajectory(filling,n0,waterLevel(n1),n1),
inference(paramodulation,[status(thm)],[f158,f436]) ).
fof(f1473,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(X0,n0)),X0),
inference(paramodulation,[status(thm)],[f167,f436]) ).
fof(f1679,plain,
! [X0] :
( ~ less(X0,n1)
| X0 = n0
| X0 = n1 ),
inference(resolution,[status(thm)],[f1469,f213]) ).
fof(f1700,plain,
! [X0] :
( ~ sP2_prd(X0,tapOn)
| holdsAt(X0,n1) ),
inference(resolution,[status(thm)],[f884,f231]) ).
fof(f1702,plain,
holdsAt(filling,n1),
inference(resolution,[status(thm)],[f1700,f257]) ).
fof(f1707,plain,
( happens(sK5_skl(n0,filling),n0)
| releasedAt(filling,n1)
| holdsAt(filling,n0) ),
inference(resolution,[status(thm)],[f1702,f280]) ).
fof(f1708,plain,
( holdsAt(filling,plus(n1,n1))
| terminates(sK4_skl(n1,filling),filling,n1)
| releasedAt(filling,plus(n1,n1)) ),
inference(resolution,[status(thm)],[f1702,f82]) ).
fof(f1709,plain,
( holdsAt(filling,plus(n1,n1))
| happens(sK4_skl(n1,filling),n1)
| releasedAt(filling,plus(n1,n1)) ),
inference(resolution,[status(thm)],[f1702,f81]) ).
fof(f1710,plain,
( happens(sK5_skl(n0,filling),n0)
| releasedAt(filling,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1707,f217]) ).
fof(f1711,plain,
( holdsAt(filling,plus(n1,n1))
| terminates(sK4_skl(n1,filling),filling,n1)
| releasedAt(filling,n2) ),
inference(forward_demodulation,[status(thm)],[f161,f1708]) ).
fof(f1712,plain,
( holdsAt(filling,n2)
| terminates(sK4_skl(n1,filling),filling,n1)
| releasedAt(filling,n2) ),
inference(forward_demodulation,[status(thm)],[f161,f1711]) ).
fof(f1713,plain,
( holdsAt(filling,n2)
| terminates(sK4_skl(n1,filling),filling,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1712,f1235]) ).
fof(f1714,plain,
( holdsAt(filling,plus(n1,n1))
| happens(sK4_skl(n1,filling),n1)
| releasedAt(filling,n2) ),
inference(forward_demodulation,[status(thm)],[f161,f1709]) ).
fof(f1715,plain,
( holdsAt(filling,n2)
| happens(sK4_skl(n1,filling),n1)
| releasedAt(filling,n2) ),
inference(forward_demodulation,[status(thm)],[f161,f1714]) ).
fof(f1716,plain,
( holdsAt(filling,n2)
| happens(sK4_skl(n1,filling),n1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1715,f1235]) ).
fof(f1821,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)],[f1471,f75]) ).
fof(f1822,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,f1821]) ).
fof(f1823,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,f1822]) ).
fof(f1824,plain,
! [X0] :
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1823,f335]) ).
fof(f2301,plain,
trajectory(filling,n0,waterLevel(n2),n2),
inference(paramodulation,[status(thm)],[f285,f1473]) ).
fof(f2311,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)],[f2301,f75]) ).
fof(f2312,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,f2311]) ).
fof(f2313,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)],[f285,f2312]) ).
fof(f2314,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,f2313]) ).
fof(f2315,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)],[f285,f2314]) ).
fof(f2316,plain,
! [X0] :
( holdsAt(waterLevel(n2),n2)
| stoppedIn(n0,filling,n2)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2315,f337]) ).
fof(f2888,plain,
happens(sK5_skl(n0,filling),n0),
inference(forward_subsumption_resolution,[status(thm)],[f1710,f1185]) ).
fof(f2889,plain,
( sK5_skl(n0,filling) = tapOn
| holdsAt(filling,n0) ),
inference(resolution,[status(thm)],[f2888,f387]) ).
fof(f2899,plain,
sK5_skl(n0,filling) = tapOn,
inference(forward_subsumption_resolution,[status(thm)],[f2889,f217]) ).
fof(f2909,plain,
( ~ holdsAt(filling,plus(n0,n1))
| initiates(tapOn,filling,n0)
| releasedAt(filling,plus(n0,n1))
| holdsAt(filling,n0) ),
inference(paramodulation,[status(thm)],[f2899,f86]) ).
fof(f2926,plain,
( ~ holdsAt(filling,plus(n0,n1))
| initiates(tapOn,filling,n0)
| releasedAt(filling,n1)
| holdsAt(filling,n0) ),
inference(forward_demodulation,[status(thm)],[f158,f2909]) ).
fof(f2927,plain,
( ~ holdsAt(filling,n1)
| initiates(tapOn,filling,n0)
| releasedAt(filling,n1)
| holdsAt(filling,n0) ),
inference(forward_demodulation,[status(thm)],[f158,f2926]) ).
fof(f2928,plain,
( ~ holdsAt(filling,n1)
| initiates(tapOn,filling,n0)
| releasedAt(filling,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[f2927,f217]) ).
fof(f3774,plain,
( sK4_skl(n1,filling) = overflow
| sK4_skl(n1,filling) = tapOff
| holdsAt(filling,n2) ),
inference(resolution,[status(thm)],[f1713,f120]) ).
fof(f5033,plain,
! [X0] :
( stoppedIn(n0,filling,n2)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2316,f222]) ).
fof(f5035,plain,
! [X0] :
( ~ sP0_prd(n0,filling,X0)
| stoppedIn(n0,filling,n2)
| ~ happens(X0,n0) ),
inference(resolution,[status(thm)],[f5033,f116]) ).
fof(f5338,plain,
( ~ sP0_prd(n0,filling,tapOn)
| stoppedIn(n0,filling,n2) ),
inference(resolution,[status(thm)],[f5035,f272]) ).
fof(f5348,plain,
( ~ sP2_prd(filling,tapOn)
| stoppedIn(n0,filling,n2) ),
inference(resolution,[status(thm)],[f5338,f231]) ).
fof(f5351,plain,
stoppedIn(n0,filling,n2),
inference(forward_subsumption_resolution,[status(thm)],[f5348,f257]) ).
fof(f5365,plain,
~ holdsAt(filling,plus(sK1_skl(n2,filling,n0),n1)),
inference(resolution,[status(thm)],[f5351,f324]) ).
fof(f5370,plain,
less(sK1_skl(n2,filling,n0),n2),
inference(resolution,[status(thm)],[f5351,f62]) ).
fof(f5375,plain,
less_or_equal(sK1_skl(n2,filling,n0),n1),
inference(resolution,[status(thm)],[f5370,f181]) ).
fof(f5398,plain,
( sK1_skl(n2,filling,n0) = n1
| less(sK1_skl(n2,filling,n0),n1) ),
inference(resolution,[status(thm)],[f5375,f170]) ).
fof(f5602,plain,
( ~ holdsAt(filling,n1)
| initiates(tapOn,filling,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2928,f1185]) ).
fof(f5603,plain,
initiates(tapOn,filling,n0),
inference(resolution,[status(thm)],[f5602,f1702]) ).
fof(f5684,plain,
( sK1_skl(n2,filling,n0) = n0
| sK1_skl(n2,filling,n0) = n1
| sK1_skl(n2,filling,n0) = n1 ),
inference(resolution,[status(thm)],[f5398,f1679]) ).
fof(f5692,plain,
( sK1_skl(n2,filling,n0) = n0
| sK1_skl(n2,filling,n0) = n1 ),
inference(duplicate_literals_removal,[status(thm)],[f5684]) ).
fof(f5699,plain,
( sK1_skl(n2,filling,n0) = n1
| ~ holdsAt(filling,plus(n0,n1)) ),
inference(paramodulation,[status(thm)],[f5692,f5365]) ).
fof(f5720,plain,
( sK1_skl(n2,filling,n0) = n1
| ~ holdsAt(filling,n1) ),
inference(forward_demodulation,[status(thm)],[f158,f5699]) ).
fof(f5721,plain,
sK1_skl(n2,filling,n0) = n1,
inference(forward_subsumption_resolution,[status(thm)],[f5720,f1702]) ).
fof(f5732,plain,
~ holdsAt(filling,plus(n1,n1)),
inference(backward_demodulation,[status(thm)],[f5721,f5365]) ).
fof(f5752,plain,
~ holdsAt(filling,n2),
inference(forward_demodulation,[status(thm)],[f161,f5732]) ).
fof(f5761,plain,
( sK4_skl(n1,filling) = overflow
| sK4_skl(n1,filling) = tapOff ),
inference(backward_subsumption_resolution,[status(thm)],[f3774,f5752]) ).
fof(f5763,plain,
happens(sK4_skl(n1,filling),n1),
inference(backward_subsumption_resolution,[status(thm)],[f1716,f5752]) ).
fof(f5959,plain,
( sK4_skl(n1,filling) = overflow
| happens(tapOff,n1) ),
inference(paramodulation,[status(thm)],[f5761,f5763]) ).
fof(f5969,plain,
( tapOff = tapOn
| tapOff = overflow
| sK4_skl(n1,filling) = overflow ),
inference(resolution,[status(thm)],[f5959,f390]) ).
fof(f5978,plain,
( tapOff = tapOn
| sK4_skl(n1,filling) = overflow ),
inference(forward_subsumption_resolution,[status(thm)],[f5969,f148]) ).
fof(f6000,plain,
happens(overflow,n1),
inference(backward_demodulation,[status(thm)],[f6001,f5763]) ).
fof(f6001,plain,
sK4_skl(n1,filling) = overflow,
inference(forward_subsumption_resolution,[status(thm)],[f5978,f147]) ).
fof(f6006,plain,
( overflow = tapOn
| holdsAt(waterLevel(n3),n1) ),
inference(resolution,[status(thm)],[f6000,f380]) ).
fof(f6016,plain,
holdsAt(waterLevel(n3),n1),
inference(forward_subsumption_resolution,[status(thm)],[f6006,f149]) ).
fof(f6025,plain,
! [X0] :
( X0 = n3
| ~ holdsAt(waterLevel(X0),n1) ),
inference(resolution,[status(thm)],[f6016,f146]) ).
fof(f6595,plain,
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1)
| ~ happens(tapOn,n0) ),
inference(resolution,[status(thm)],[f1824,f5603]) ).
fof(f6598,plain,
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[f6595,f272]) ).
fof(f6647,plain,
( n1 = n3
| stoppedIn(n0,filling,n1) ),
inference(resolution,[status(thm)],[f6598,f6025]) ).
fof(f6675,plain,
( less(sK1_skl(n1,filling,n0),n1)
| n1 = n3 ),
inference(resolution,[status(thm)],[f6647,f62]) ).
fof(f6681,plain,
( less_or_equal(sK1_skl(n1,filling,n0),n0)
| n1 = n3 ),
inference(resolution,[status(thm)],[f6675,f177]) ).
fof(f6685,plain,
( sK1_skl(n1,filling,n0) = n0
| less(sK1_skl(n1,filling,n0),n0)
| n1 = n3 ),
inference(resolution,[status(thm)],[f6681,f170]) ).
fof(f6686,plain,
( sK1_skl(n1,filling,n0) = n0
| n1 = n3 ),
inference(forward_subsumption_resolution,[status(thm)],[f6685,f174]) ).
fof(f6690,plain,
( n1 = n3
| less(n0,n0)
| ~ stoppedIn(n0,filling,n1) ),
inference(paramodulation,[status(thm)],[f6686,f61]) ).
fof(f6695,plain,
( n1 = n3
| less(n0,n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6690,f6647]) ).
fof(f6922,plain,
less(n3,n3),
inference(backward_demodulation,[status(thm)],[f6939,f310]) ).
fof(f6939,plain,
n1 = n3,
inference(forward_subsumption_resolution,[status(thm)],[f6695,f174]) ).
fof(f7194,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f6922,f254]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR008+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n005.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 14:24:04 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 11.12/1.85 % Refutation found
% 11.12/1.85 % SZS status Theorem for theBenchmark: Theorem is valid
% 11.12/1.85 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.12/1.89 % Elapsed time: 1.523575 seconds
% 11.12/1.89 % CPU time: 11.609776 seconds
% 11.12/1.89 % Total memory used: 198.399 MB
% 11.12/1.89 % Net memory used: 189.171 MB
%------------------------------------------------------------------------------