%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR013+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 : n018.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 21.42s 3.12s
% Output : CNFRefutation 21.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 113
% Syntax : Number of formulae : 555 ( 92 unt; 75 def)
% Number of atoms : 1441 ( 273 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 1548 ( 662 ~; 638 |; 146 &)
% ( 95 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 87 ( 85 usr; 73 prp; 0-4 aty)
% Number of functors : 26 ( 26 usr; 16 con; 0-3 aty)
% Number of variables : 505 ( 482 !; 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/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(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(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(f12,axiom,
! [Event,Time,Fluent] :
( ( ( terminates(Event,Fluent,Time)
| initiates(Event,Fluent,Time) )
& happens(Event,Time) )
=> ~ releasedAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [Event,Fluent,Time] :
( initiates(Event,Fluent,Time)
<=> ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = overflow
& holdsAt(waterLevel(Height),Time) )
| ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOff
& holdsAt(waterLevel(Height),Time) )
| ( Fluent = spilling
& Event = overflow )
| ( Fluent = filling
& Event = tapOn ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(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(f22,axiom,
! [X] : filling != waterLevel(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X] : spilling != waterLevel(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X,Y] :
( waterLevel(X) = waterLevel(Y)
<=> X = Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
plus(n0,n0) = n0,
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(f31,axiom,
plus(n1,n2) = n3,
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(f42,axiom,
! [X] :
( less(X,n4)
<=> less_or_equal(X,n3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [X] :
( less(X,n5)
<=> less_or_equal(X,n4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [X] :
( less(X,n6)
<=> less_or_equal(X,n5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [X] :
( less(X,n7)
<=> less_or_equal(X,n6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [X] :
( less(X,n8)
<=> less_or_equal(X,n7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [X] :
( less(X,n9)
<=> less_or_equal(X,n8) ),
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(f55,conjecture,
~ ? [Event] :
( terminates(Event,filling,n2)
& happens(Event,n2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,negated_conjecture,
~ ~ ? [Event] :
( terminates(Event,filling,n2)
& happens(Event,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(f64,plain,
! [X0,X1,X2,X3,X4] :
( ~ terminates(X3,X1,X4)
| ~ less(X4,X2)
| ~ less(X0,X4)
| ~ happens(X3,X4)
| 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(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(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(f117,plain,
! [X0,X1,X2,X3] :
( X1 != waterLevel(X3)
| X0 != overflow
| ~ holdsAt(waterLevel(X3),X2)
| 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(f123,plain,
! [X0,X1,X2] :
( X1 = filling
| X1 = filling
| ~ terminates(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f125,plain,
! [X0,X1,X2] :
( X1 != filling
| X0 != overflow
| 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(f131,plain,
! [X0,X1,X2,X3] :
( X1 != waterLevel(X3)
| X0 != tapOn
| releases(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f132,definition,
! [Event,Time] :
( sP1_prd(Time,Event)
<=> ( Time = n0
& Event = tapOn ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f133,plain,
! [Event,Time] :
( happens(Event,Time)
<=> ( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| sP1_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f16,f132]) ).
fof(f134,plain,
! [Event,Time] :
( ( ( ( Event != overflow
| ~ holdsAt(filling,Time)
| ~ holdsAt(waterLevel(n3),Time) )
& ~ sP1_prd(Time,Event) )
| happens(Event,Time) )
& ( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| sP1_prd(Time,Event)
| ~ happens(Event,Time) ) ),
inference(NNF_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
( ! [Event,Time] :
( ( ( Event != overflow
| ~ holdsAt(filling,Time)
| ~ holdsAt(waterLevel(n3),Time) )
& ~ sP1_prd(Time,Event) )
| happens(Event,Time) )
& ! [Event,Time] :
( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| sP1_prd(Time,Event)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f134]) ).
fof(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(f140,plain,
! [X0,X1] :
( X0 != overflow
| ~ holdsAt(filling,X1)
| ~ holdsAt(waterLevel(n3),X1)
| 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(f150,plain,
! [X0] : filling != waterLevel(X0),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f151,plain,
! [X0] : spilling != waterLevel(X0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f153,plain,
! [X,Y] :
( ( X != Y
| waterLevel(X) = waterLevel(Y) )
& ( X = Y
| waterLevel(X) != waterLevel(Y) ) ),
inference(NNF_transformation,[status(thm)],[f25]) ).
fof(f154,plain,
( ! [X,Y] :
( X != Y
| waterLevel(X) = waterLevel(Y) )
& ! [X,Y] :
( X = Y
| waterLevel(X) != waterLevel(Y) ) ),
inference(miniscoping,[status(thm)],[f153]) ).
fof(f155,plain,
! [X0,X1] :
( X0 = X1
| waterLevel(X0) != waterLevel(X1) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f157,plain,
plus(n0,n0) = n0,
inference(cnf_transformation,[status(thm)],[f26]) ).
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(f162,plain,
plus(n1,n2) = n3,
inference(cnf_transformation,[status(thm)],[f31]) ).
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(f185,plain,
! [X0] :
( less_or_equal(X0,n2)
| ~ less(X0,n3) ),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f186,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f187,plain,
! [X] :
( ( ~ less_or_equal(X,n3)
| less(X,n4) )
& ( less_or_equal(X,n3)
| ~ less(X,n4) ) ),
inference(NNF_transformation,[status(thm)],[f42]) ).
fof(f188,plain,
( ! [X] :
( ~ less_or_equal(X,n3)
| less(X,n4) )
& ! [X] :
( less_or_equal(X,n3)
| ~ less(X,n4) ) ),
inference(miniscoping,[status(thm)],[f187]) ).
fof(f190,plain,
! [X0] :
( ~ less_or_equal(X0,n3)
| less(X0,n4) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f191,plain,
! [X] :
( ( ~ less_or_equal(X,n4)
| less(X,n5) )
& ( less_or_equal(X,n4)
| ~ less(X,n5) ) ),
inference(NNF_transformation,[status(thm)],[f43]) ).
fof(f192,plain,
( ! [X] :
( ~ less_or_equal(X,n4)
| less(X,n5) )
& ! [X] :
( less_or_equal(X,n4)
| ~ less(X,n5) ) ),
inference(miniscoping,[status(thm)],[f191]) ).
fof(f194,plain,
! [X0] :
( ~ less_or_equal(X0,n4)
| less(X0,n5) ),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f195,plain,
! [X] :
( ( ~ less_or_equal(X,n5)
| less(X,n6) )
& ( less_or_equal(X,n5)
| ~ less(X,n6) ) ),
inference(NNF_transformation,[status(thm)],[f44]) ).
fof(f196,plain,
( ! [X] :
( ~ less_or_equal(X,n5)
| less(X,n6) )
& ! [X] :
( less_or_equal(X,n5)
| ~ less(X,n6) ) ),
inference(miniscoping,[status(thm)],[f195]) ).
fof(f198,plain,
! [X0] :
( ~ less_or_equal(X0,n5)
| less(X0,n6) ),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f199,plain,
! [X] :
( ( ~ less_or_equal(X,n6)
| less(X,n7) )
& ( less_or_equal(X,n6)
| ~ less(X,n7) ) ),
inference(NNF_transformation,[status(thm)],[f45]) ).
fof(f200,plain,
( ! [X] :
( ~ less_or_equal(X,n6)
| less(X,n7) )
& ! [X] :
( less_or_equal(X,n6)
| ~ less(X,n7) ) ),
inference(miniscoping,[status(thm)],[f199]) ).
fof(f202,plain,
! [X0] :
( ~ less_or_equal(X0,n6)
| less(X0,n7) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f203,plain,
! [X] :
( ( ~ less_or_equal(X,n7)
| less(X,n8) )
& ( less_or_equal(X,n7)
| ~ less(X,n8) ) ),
inference(NNF_transformation,[status(thm)],[f46]) ).
fof(f204,plain,
( ! [X] :
( ~ less_or_equal(X,n7)
| less(X,n8) )
& ! [X] :
( less_or_equal(X,n7)
| ~ less(X,n8) ) ),
inference(miniscoping,[status(thm)],[f203]) ).
fof(f206,plain,
! [X0] :
( ~ less_or_equal(X0,n7)
| less(X0,n8) ),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f207,plain,
! [X] :
( ( ~ less_or_equal(X,n8)
| less(X,n9) )
& ( less_or_equal(X,n8)
| ~ less(X,n9) ) ),
inference(NNF_transformation,[status(thm)],[f47]) ).
fof(f208,plain,
( ! [X] :
( ~ less_or_equal(X,n8)
| less(X,n9) )
& ! [X] :
( less_or_equal(X,n8)
| ~ less(X,n9) ) ),
inference(miniscoping,[status(thm)],[f207]) ).
fof(f210,plain,
! [X0] :
( ~ less_or_equal(X0,n8)
| less(X0,n9) ),
inference(cnf_transformation,[status(thm)],[f208]) ).
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(f222,plain,
( terminates(sK10_skl,filling,n2)
& happens(sK10_skl,n2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(Event,sK10_skl)],[f56]) ).
fof(f223,plain,
happens(sK10_skl,n2),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f224,plain,
terminates(sK10_skl,filling,n2),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f225,definition,
! [Event,Fluent] :
( sP2_prd(Fluent,Event)
<=> ( ( Fluent = spilling
& Event = overflow )
| ( Fluent = filling
& Event = tapOn ) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f226,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,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) )
& ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOff
& holdsAt(waterLevel(Height),Time) )
| sP2_prd(Fluent,Event)
| ~ sP0_prd(Time,Fluent,Event) ) ),
inference(NNF_transformation,[status(thm)],[f226]) ).
fof(f228,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)],[f227]) ).
fof(f229,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(sK11_skl(Time,Fluent,Event))
& Event = tapOff
& holdsAt(waterLevel(sK11_skl(Time,Fluent,Event)),Time) )
| sP2_prd(Fluent,Event)
| ~ sP0_prd(Time,Fluent,Event) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(Height,sK11_skl(Time,Fluent,Event))],[f228]) ).
fof(f233,plain,
! [X0,X1,X2] :
( ~ sP2_prd(X1,X2)
| sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f234,plain,
! [X0,X1,X2,X3] :
( X1 != waterLevel(X3)
| X2 != tapOff
| ~ holdsAt(waterLevel(X3),X0)
| sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f235,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(f236,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)],[f235]) ).
fof(f237,plain,
! [X0,X1] :
( X1 = tapOn
| ~ sP1_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f238,plain,
! [X0,X1] :
( X0 = n0
| ~ sP1_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f239,plain,
! [X0,X1] :
( X0 != n0
| X1 != tapOn
| sP1_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f240,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)],[f225]) ).
fof(f241,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)],[f240]) ).
fof(f246,plain,
! [X0,X1] :
( X0 != filling
| X1 != tapOn
| sP2_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f248,plain,
! [X0,X1] :
( ~ holdsAt(waterLevel(X0),X1)
| initiates(overflow,waterLevel(X0),X1) ),
inference(destructive_equality_resolution,[status(thm)],[f117]) ).
fof(f249,plain,
! [X0,X1,X2] :
( X1 = filling
| ~ terminates(X0,X1,X2) ),
inference(duplicate_literals_removal,[status(thm)],[f123]) ).
fof(f251,plain,
! [X0] : terminates(overflow,filling,X0),
inference(destructive_equality_resolution,[status(thm)],[f125]) ).
fof(f252,plain,
! [X0,X1] : releases(tapOn,waterLevel(X0),X1),
inference(destructive_equality_resolution,[status(thm)],[f131]) ).
fof(f253,plain,
! [X0] :
( ~ holdsAt(filling,X0)
| ~ holdsAt(waterLevel(n3),X0)
| happens(overflow,X0) ),
inference(destructive_equality_resolution,[status(thm)],[f140]) ).
fof(f254,plain,
! [X0,X1,X2] :
( trajectory(filling,X1,waterLevel(plus(X0,X2)),X2)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(destructive_equality_resolution,[status(thm)],[f143]) ).
fof(f255,plain,
! [X0] : less_or_equal(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f172]) ).
fof(f256,plain,
! [X0] : ~ less(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f214]) ).
fof(f257,plain,
! [X0,X1] :
( ~ holdsAt(waterLevel(X1),X0)
| sP0_prd(X0,waterLevel(X1),tapOff) ),
inference(destructive_equality_resolution,[status(thm)],[f234]) ).
fof(f258,plain,
sP1_prd(n0,tapOn),
inference(destructive_equality_resolution,[status(thm)],[f239]) ).
fof(f259,plain,
sP2_prd(filling,tapOn),
inference(destructive_equality_resolution,[status(thm)],[f246]) ).
fof(f262,plain,
! [X0,X1] :
( ~ holdsAt(X1,n2)
| ~ terminates(X0,X1,n1)
| ~ happens(X0,n1) ),
inference(paramodulation,[status(thm)],[f161,f100]) ).
fof(f264,plain,
~ less_or_equal(n2,n1),
inference(resolution,[status(thm)],[f182,f256]) ).
fof(f266,plain,
~ less_or_equal(n3,n2),
inference(resolution,[status(thm)],[f186,f256]) ).
fof(f268,plain,
! [X0,X1] :
( ~ less(n2,X1)
| ~ less(X0,n2)
| ~ happens(sK10_skl,n2)
| stoppedIn(X0,filling,X1) ),
inference(resolution,[status(thm)],[f64,f224]) ).
fof(f269,definition,
! [X0,X1] :
( sQ0_spl
<=> ( ~ less(n2,X1)
| ~ less(X0,n2)
| stoppedIn(X0,filling,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f270,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ less(n2,X1)
| ~ less(X0,n2)
| stoppedIn(X0,filling,X1) ),
inference(component_clause,[status(thm)],[f269]) ).
fof(f272,definition,
( sQ1_spl
<=> happens(sK10_skl,n2) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f274,plain,
( sQ1_spl
| ~ happens(sK10_skl,n2) ),
inference(component_clause,[status(thm)],[f272]) ).
fof(f275,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f268,f269,f272]) ).
fof(f283,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ less_or_equal(X0,n1)
| ~ less(n2,X1)
| stoppedIn(X0,filling,X1) ),
inference(resolution,[status(thm)],[f270,f182]) ).
fof(f285,plain,
! [X0] :
( ~ sQ0_spl
| ~ less(n2,X0)
| stoppedIn(n1,filling,X0) ),
inference(resolution,[status(thm)],[f283,f255]) ).
fof(f287,plain,
! [X0] :
( ~ sQ0_spl
| less(sK1_skl(X0,filling,n1),X0)
| ~ less(n2,X0) ),
inference(resolution,[status(thm)],[f285,f62]) ).
fof(f297,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f274,f223]) ).
fof(f298,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f297]) ).
fof(f333,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(n1,X1))
| ~ terminates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(paramodulation,[status(thm)],[f167,f100]) ).
fof(f360,plain,
~ less(n3,n2),
inference(resolution,[status(thm)],[f171,f266]) ).
fof(f361,plain,
~ less(n2,n1),
inference(resolution,[status(thm)],[f171,f264]) ).
fof(f363,plain,
~ less_or_equal(n3,n1),
inference(resolution,[status(thm)],[f360,f182]) ).
fof(f470,plain,
! [X0,X1,X2] :
( ~ sP2_prd(X1,X0)
| initiates(X0,X1,X2) ),
inference(resolution,[status(thm)],[f116,f233]) ).
fof(f487,definition,
( sQ26_spl
<=> less_or_equal(n2,n2) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f489,plain,
( sQ26_spl
| ~ less_or_equal(n2,n2) ),
inference(component_clause,[status(thm)],[f487]) ).
fof(f526,plain,
! [X0] :
( ~ less(X0,n3)
| X0 = n2
| less(X0,n2) ),
inference(resolution,[status(thm)],[f170,f185]) ).
fof(f527,plain,
! [X0] :
( ~ less(X0,n2)
| X0 = n1
| less(X0,n1) ),
inference(resolution,[status(thm)],[f170,f181]) ).
fof(f530,plain,
! [X0] :
( X0 = n0
| less(X0,n0)
| ~ less(X0,n1) ),
inference(resolution,[status(thm)],[f177,f170]) ).
fof(f531,plain,
! [X0] :
( X0 = n0
| ~ less(X0,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[f530,f174]) ).
fof(f539,plain,
less(n0,n1),
inference(resolution,[status(thm)],[f178,f255]) ).
fof(f547,plain,
! [X0] :
( ~ less(X0,n3)
| less(X0,n4) ),
inference(resolution,[status(thm)],[f190,f171]) ).
fof(f566,definition,
( sQ35_spl
<=> less(sK1_skl(n2,filling,n0),n2) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f567,plain,
( ~ sQ35_spl
| less(sK1_skl(n2,filling,n0),n2) ),
inference(component_clause,[status(thm)],[f566]) ).
fof(f570,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f489,f255]) ).
fof(f571,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f570]) ).
fof(f584,plain,
( ~ sQ0_spl
| ~ less(n2,n3)
| sK1_skl(n3,filling,n1) = n2
| less(sK1_skl(n3,filling,n1),n2) ),
inference(resolution,[status(thm)],[f526,f287]) ).
fof(f593,definition,
( sQ38_spl
<=> less(sK1_skl(n3,filling,n1),n2) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f594,plain,
( ~ sQ38_spl
| less(sK1_skl(n3,filling,n1),n2) ),
inference(component_clause,[status(thm)],[f593]) ).
fof(f596,definition,
( sQ39_spl
<=> sK1_skl(n3,filling,n1) = n2 ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f597,plain,
( ~ sQ39_spl
| sK1_skl(n3,filling,n1) = n2 ),
inference(component_clause,[status(thm)],[f596]) ).
fof(f599,definition,
( sQ40_spl
<=> less(n2,n3) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f601,plain,
( sQ40_spl
| ~ less(n2,n3) ),
inference(component_clause,[status(thm)],[f599]) ).
fof(f602,plain,
( ~ sQ0_spl
| ~ sQ40_spl
| sQ39_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f584,f593,f596,f599,f269]) ).
fof(f612,plain,
( sQ40_spl
| ~ less_or_equal(n2,n2) ),
inference(resolution,[status(thm)],[f601,f186]) ).
fof(f613,plain,
( sQ40_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f612,f487,f599]) ).
fof(f626,plain,
! [X0] :
( ~ less(X0,n4)
| less(X0,n5) ),
inference(resolution,[status(thm)],[f194,f171]) ).
fof(f631,plain,
! [X0] :
( ~ less(X0,n5)
| less(X0,n6) ),
inference(resolution,[status(thm)],[f198,f171]) ).
fof(f680,definition,
( sQ50_spl
<=> less(n0,n2) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f690,plain,
( ~ sQ38_spl
| sK1_skl(n3,filling,n1) = n1
| less(sK1_skl(n3,filling,n1),n1) ),
inference(resolution,[status(thm)],[f594,f527]) ).
fof(f694,definition,
( sQ52_spl
<=> less(sK1_skl(n3,filling,n1),n1) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f695,plain,
( ~ sQ52_spl
| less(sK1_skl(n3,filling,n1),n1) ),
inference(component_clause,[status(thm)],[f694]) ).
fof(f697,definition,
( sQ53_spl
<=> sK1_skl(n3,filling,n1) = n1 ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f698,plain,
( ~ sQ53_spl
| sK1_skl(n3,filling,n1) = n1 ),
inference(component_clause,[status(thm)],[f697]) ).
fof(f700,plain,
( ~ sQ38_spl
| sQ53_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f690,f694,f697,f593]) ).
fof(f711,plain,
( ~ sQ39_spl
| happens(sK0_skl(n3,filling,n1),n2)
| ~ stoppedIn(n1,filling,n3) ),
inference(paramodulation,[status(thm)],[f597,f60]) ).
fof(f732,definition,
( sQ59_spl
<=> stoppedIn(n1,filling,n3) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f734,plain,
( sQ59_spl
| ~ stoppedIn(n1,filling,n3) ),
inference(component_clause,[status(thm)],[f732]) ).
fof(f744,definition,
( sQ62_spl
<=> happens(sK0_skl(n3,filling,n1),n2) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f745,plain,
( ~ sQ62_spl
| happens(sK0_skl(n3,filling,n1),n2) ),
inference(component_clause,[status(thm)],[f744]) ).
fof(f747,plain,
( ~ sQ39_spl
| sQ62_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f711,f732,f744,f596]) ).
fof(f758,definition,
( sQ63_spl
<=> less(n1,n1) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f759,plain,
( ~ sQ63_spl
| less(n1,n1) ),
inference(component_clause,[status(thm)],[f758]) ).
fof(f765,plain,
( ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f759,f256]) ).
fof(f766,plain,
~ sQ63_spl,
inference(contradiction_clause,[status(thm)],[f765]) ).
fof(f768,plain,
( ~ sQ0_spl
| sQ59_spl
| ~ less(n2,n3) ),
inference(resolution,[status(thm)],[f734,f285]) ).
fof(f769,plain,
( ~ sQ0_spl
| sQ59_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f768,f599,f732,f269]) ).
fof(f780,plain,
! [X0] :
( ~ less(X0,n7)
| less(X0,n8) ),
inference(resolution,[status(thm)],[f206,f171]) ).
fof(f781,plain,
less(n7,n8),
inference(resolution,[status(thm)],[f206,f255]) ).
fof(f810,definition,
( sQ68_spl
<=> less(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f811,plain,
( ~ sQ68_spl
| less(n0,n0) ),
inference(component_clause,[status(thm)],[f810]) ).
fof(f820,plain,
( ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f811,f174]) ).
fof(f821,plain,
~ sQ68_spl,
inference(contradiction_clause,[status(thm)],[f820]) ).
fof(f873,plain,
! [X0] :
( ~ less(X0,n8)
| less(X0,n9) ),
inference(resolution,[status(thm)],[f210,f171]) ).
fof(f874,plain,
less(n8,n9),
inference(resolution,[status(thm)],[f210,f255]) ).
fof(f899,plain,
! [X0] :
( X0 = n0
| less(n0,X0) ),
inference(resolution,[status(thm)],[f215,f174]) ).
fof(f954,definition,
( sQ91_spl
<=> n4 = n3 ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f955,plain,
( ~ sQ91_spl
| n4 = n3 ),
inference(component_clause,[status(thm)],[f954]) ).
fof(f966,definition,
( sQ94_spl
<=> n3 = n2 ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f967,plain,
( ~ sQ94_spl
| n3 = n2 ),
inference(component_clause,[status(thm)],[f966]) ).
fof(f1033,plain,
initiates(overflow,waterLevel(n0),n0),
inference(resolution,[status(thm)],[f248,f216]) ).
fof(f1036,definition,
( sQ95_spl
<=> overflow = tapOff ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1037,plain,
( ~ sQ95_spl
| overflow = tapOff ),
inference(component_clause,[status(thm)],[f1036]) ).
fof(f1047,plain,
( ~ sQ95_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1037,f148]) ).
fof(f1048,plain,
~ sQ95_spl,
inference(contradiction_clause,[status(thm)],[f1047]) ).
fof(f1051,plain,
! [X0] :
( ~ holdsAt(X0,plus(n1,n2))
| ~ terminates(sK10_skl,X0,n2) ),
inference(resolution,[status(thm)],[f223,f333]) ).
fof(f1053,plain,
( sK10_skl = overflow
| sK10_skl = tapOff ),
inference(resolution,[status(thm)],[f224,f120]) ).
fof(f1056,definition,
( sQ98_spl
<=> sK10_skl = tapOff ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1057,plain,
( ~ sQ98_spl
| sK10_skl = tapOff ),
inference(component_clause,[status(thm)],[f1056]) ).
fof(f1059,definition,
( sQ99_spl
<=> sK10_skl = overflow ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1060,plain,
( ~ sQ99_spl
| sK10_skl = overflow ),
inference(component_clause,[status(thm)],[f1059]) ).
fof(f1062,plain,
( sQ99_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f1053,f1056,f1059]) ).
fof(f1086,plain,
! [X0] : waterLevel(X0) = waterLevel(sK9_skl(waterLevel(X0),tapOn)),
inference(resolution,[status(thm)],[f130,f252]) ).
fof(f1089,plain,
! [X0,X1] :
( X1 = n0
| holdsAt(waterLevel(n3),X1)
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f136,f238]) ).
fof(f1101,plain,
! [X0] :
( ~ less(X0,n1)
| less(X0,n2) ),
inference(resolution,[status(thm)],[f182,f171]) ).
fof(f1105,plain,
( less_or_equal(n0,n1)
| n2 = n0 ),
inference(resolution,[status(thm)],[f899,f181]) ).
fof(f1114,definition,
( sQ100_spl
<=> n2 = n0 ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1115,plain,
( ~ sQ100_spl
| n2 = n0 ),
inference(component_clause,[status(thm)],[f1114]) ).
fof(f1117,definition,
( sQ101_spl
<=> less_or_equal(n0,n1) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1118,plain,
( ~ sQ101_spl
| less_or_equal(n0,n1) ),
inference(component_clause,[status(thm)],[f1117]) ).
fof(f1120,plain,
( sQ101_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f1105,f1114,f1117]) ).
fof(f1129,definition,
( sQ104_spl
<=> n1 = n0 ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1130,plain,
( ~ sQ104_spl
| n1 = n0 ),
inference(component_clause,[status(thm)],[f1129]) ).
fof(f1158,plain,
( ~ sQ100_spl
| ~ less(n0,n1) ),
inference(backward_demodulation,[status(thm)],[f1115,f361]) ).
fof(f1170,plain,
( ~ sQ100_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1158,f539]) ).
fof(f1171,plain,
~ sQ100_spl,
inference(contradiction_clause,[status(thm)],[f1170]) ).
fof(f1193,plain,
( ~ sQ104_spl
| less(n0,n0) ),
inference(backward_demodulation,[status(thm)],[f1130,f539]) ).
fof(f1223,plain,
( ~ sQ104_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f1193,f810,f1129]) ).
fof(f1255,plain,
! [X0] :
( sP1_prd(n0,X0)
| ~ happens(X0,n0) ),
inference(resolution,[status(thm)],[f137,f217]) ).
fof(f1256,plain,
! [X0,X1] :
( X1 = n0
| X0 = overflow
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f138,f238]) ).
fof(f1257,plain,
! [X0,X1] :
( X0 = tapOn
| X0 = overflow
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f138,f237]) ).
fof(f1287,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(n0,X0)),X0),
inference(resolution,[status(thm)],[f254,f216]) ).
fof(f1406,plain,
( ~ sQ53_spl
| less(n1,n1)
| ~ stoppedIn(n1,filling,n3) ),
inference(paramodulation,[status(thm)],[f698,f61]) ).
fof(f1408,plain,
( ~ sQ53_spl
| sQ63_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f1406,f732,f758,f697]) ).
fof(f1428,definition,
! [X0] :
( sQ115_spl
<=> ( sP1_prd(n3,X0)
| ~ happens(X0,n3) ) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1429,plain,
! [X0] :
( ~ sQ115_spl
| sP1_prd(n3,X0)
| ~ happens(X0,n3) ),
inference(component_clause,[status(thm)],[f1428]) ).
fof(f1478,definition,
( sQ116_spl
<=> less(n1,n0) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1479,plain,
( ~ sQ116_spl
| less(n1,n0) ),
inference(component_clause,[status(thm)],[f1478]) ).
fof(f1486,plain,
( ~ sQ116_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1479,f174]) ).
fof(f1487,plain,
~ sQ116_spl,
inference(contradiction_clause,[status(thm)],[f1486]) ).
fof(f1498,plain,
( n1 = n0
| less(n0,n2) ),
inference(resolution,[status(thm)],[f1101,f899]) ).
fof(f1500,plain,
( sQ104_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f1498,f680,f1129]) ).
fof(f1521,definition,
( sQ118_spl
<=> n3 = n0 ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1522,plain,
( ~ sQ118_spl
| n3 = n0 ),
inference(component_clause,[status(thm)],[f1521]) ).
fof(f1541,plain,
( ~ sQ118_spl
| ~ less_or_equal(n0,n1) ),
inference(backward_demodulation,[status(thm)],[f1522,f363]) ).
fof(f1621,plain,
! [X0] :
( X0 = tapOn
| ~ happens(X0,n0) ),
inference(resolution,[status(thm)],[f1255,f237]) ).
fof(f1632,plain,
! [X0,X1] :
( sP1_prd(n2,X1)
| ~ happens(X1,n2)
| ~ terminates(X0,filling,n1)
| ~ happens(X0,n1) ),
inference(resolution,[status(thm)],[f262,f137]) ).
fof(f1633,definition,
! [X0] :
( sQ121_spl
<=> ( ~ terminates(X0,filling,n1)
| ~ happens(X0,n1) ) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1634,plain,
! [X0] :
( ~ sQ121_spl
| ~ terminates(X0,filling,n1)
| ~ happens(X0,n1) ),
inference(component_clause,[status(thm)],[f1633]) ).
fof(f1636,definition,
! [X1] :
( sQ122_spl
<=> ( sP1_prd(n2,X1)
| ~ happens(X1,n2) ) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1637,plain,
! [X0] :
( ~ sQ122_spl
| sP1_prd(n2,X0)
| ~ happens(X0,n2) ),
inference(component_clause,[status(thm)],[f1636]) ).
fof(f1639,plain,
( sQ122_spl
| sQ121_spl ),
inference(split_clause,[status(thm)],[f1632,f1633,f1636]) ).
fof(f1660,plain,
! [X0] :
( ~ sQ115_spl
| n3 = n0
| ~ happens(X0,n3) ),
inference(resolution,[status(thm)],[f1429,f238]) ).
fof(f1662,definition,
! [X0] :
( sQ123_spl
<=> ~ happens(X0,n3) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1663,plain,
! [X0] :
( ~ sQ123_spl
| ~ happens(X0,n3) ),
inference(component_clause,[status(thm)],[f1662]) ).
fof(f1665,plain,
( ~ sQ115_spl
| sQ118_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f1660,f1662,f1521,f1428]) ).
fof(f1666,plain,
! [X0] :
( ~ holdsAt(X0,n3)
| ~ terminates(sK10_skl,X0,n2) ),
inference(forward_demodulation,[status(thm)],[f162,f1051]) ).
fof(f1675,plain,
! [X0] :
( ~ holdsAt(X0,plus(n0,n1))
| releasedAt(X0,plus(n0,n1))
| holdsAt(X0,n0)
| sK5_skl(n0,X0) = tapOn ),
inference(resolution,[status(thm)],[f1621,f85]) ).
fof(f1679,plain,
! [X0] :
( ~ holdsAt(X0,plus(n0,n1))
| releasedAt(X0,n1)
| holdsAt(X0,n0)
| sK5_skl(n0,X0) = tapOn ),
inference(forward_demodulation,[status(thm)],[f158,f1675]) ).
fof(f1680,plain,
! [X0] :
( ~ holdsAt(X0,n1)
| releasedAt(X0,n1)
| holdsAt(X0,n0)
| sK5_skl(n0,X0) = tapOn ),
inference(forward_demodulation,[status(thm)],[f158,f1679]) ).
fof(f1684,plain,
! [X0] :
( ~ less(n4,X0)
| ~ less(X0,n3) ),
inference(resolution,[status(thm)],[f547,f213]) ).
fof(f1713,plain,
! [X0,X1] :
( X1 = n0
| holdsAt(waterLevel(n3),X1)
| ~ happens(X0,X1) ),
inference(resolution,[status(thm)],[f136,f238]) ).
fof(f1722,plain,
( ~ sQ52_spl
| sK1_skl(n3,filling,n1) = n0 ),
inference(resolution,[status(thm)],[f695,f531]) ).
fof(f1729,plain,
( ~ sQ52_spl
| less(n1,n0)
| ~ stoppedIn(n1,filling,n3) ),
inference(paramodulation,[status(thm)],[f1722,f61]) ).
fof(f1731,plain,
( ~ sQ52_spl
| sQ116_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f1729,f732,f1478,f694]) ).
fof(f1836,plain,
! [X0] :
( ~ sQ122_spl
| n2 = n0
| ~ happens(X0,n2) ),
inference(resolution,[status(thm)],[f1637,f238]) ).
fof(f1838,definition,
! [X0] :
( sQ133_spl
<=> ~ happens(X0,n2) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f1839,plain,
! [X0] :
( ~ sQ133_spl
| ~ happens(X0,n2) ),
inference(component_clause,[status(thm)],[f1838]) ).
fof(f1841,plain,
( ~ sQ122_spl
| sQ100_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f1836,f1838,f1114,f1636]) ).
fof(f1850,plain,
( ~ sQ133_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f223,f1839]) ).
fof(f1851,plain,
~ sQ133_spl,
inference(contradiction_clause,[status(thm)],[f1850]) ).
fof(f1953,plain,
( ~ sQ118_spl
| ~ sQ101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1541,f1118]) ).
fof(f1954,plain,
( ~ sQ118_spl
| ~ sQ101_spl ),
inference(contradiction_clause,[status(thm)],[f1953]) ).
fof(f1981,definition,
! [X0] :
( sQ144_spl
<=> ~ happens(X0,n1) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f1982,plain,
! [X0] :
( ~ sQ144_spl
| ~ happens(X0,n1) ),
inference(component_clause,[status(thm)],[f1981]) ).
fof(f2047,plain,
! [X0] :
( ~ sQ99_spl
| ~ holdsAt(X0,n3)
| ~ terminates(overflow,X0,n2) ),
inference(forward_demodulation,[status(thm)],[f1060,f1666]) ).
fof(f2048,plain,
! [X0] :
( ~ sQ99_spl
| sP1_prd(n3,X0)
| ~ happens(X0,n3)
| ~ terminates(overflow,filling,n2) ),
inference(resolution,[status(thm)],[f2047,f137]) ).
fof(f2049,definition,
( sQ148_spl
<=> terminates(overflow,filling,n2) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f2051,plain,
( sQ148_spl
| ~ terminates(overflow,filling,n2) ),
inference(component_clause,[status(thm)],[f2049]) ).
fof(f2052,plain,
( ~ sQ99_spl
| sQ115_spl
| ~ sQ148_spl ),
inference(split_clause,[status(thm)],[f2048,f2049,f1428,f1059]) ).
fof(f2053,plain,
( sQ148_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2051,f251]) ).
fof(f2054,plain,
sQ148_spl,
inference(contradiction_clause,[status(thm)],[f2053]) ).
fof(f2074,plain,
~ less(n8,n7),
inference(resolution,[status(thm)],[f781,f213]) ).
fof(f2107,plain,
( ~ sQ35_spl
| sK1_skl(n2,filling,n0) = n1
| less(sK1_skl(n2,filling,n0),n1) ),
inference(resolution,[status(thm)],[f567,f527]) ).
fof(f2109,definition,
( sQ150_spl
<=> less(sK1_skl(n2,filling,n0),n1) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f2110,plain,
( ~ sQ150_spl
| less(sK1_skl(n2,filling,n0),n1) ),
inference(component_clause,[status(thm)],[f2109]) ).
fof(f2112,definition,
( sQ151_spl
<=> sK1_skl(n2,filling,n0) = n1 ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f2113,plain,
( ~ sQ151_spl
| sK1_skl(n2,filling,n0) = n1 ),
inference(component_clause,[status(thm)],[f2112]) ).
fof(f2115,plain,
( ~ sQ35_spl
| sQ151_spl
| sQ150_spl ),
inference(split_clause,[status(thm)],[f2107,f2109,f2112,f566]) ).
fof(f2117,plain,
( ~ sQ151_spl
| happens(sK0_skl(n2,filling,n0),n1)
| ~ stoppedIn(n0,filling,n2) ),
inference(paramodulation,[status(thm)],[f2113,f60]) ).
fof(f2118,definition,
( sQ152_spl
<=> stoppedIn(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f2120,plain,
( sQ152_spl
| ~ stoppedIn(n0,filling,n2) ),
inference(component_clause,[status(thm)],[f2118]) ).
fof(f2122,definition,
( sQ153_spl
<=> happens(sK0_skl(n2,filling,n0),n1) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f2123,plain,
( ~ sQ153_spl
| happens(sK0_skl(n2,filling,n0),n1) ),
inference(component_clause,[status(thm)],[f2122]) ).
fof(f2125,plain,
( ~ sQ151_spl
| sQ153_spl
| ~ sQ152_spl ),
inference(split_clause,[status(thm)],[f2117,f2118,f2122,f2112]) ).
fof(f2126,plain,
( ~ sQ153_spl
| ~ sQ144_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2123,f1982]) ).
fof(f2127,plain,
( ~ sQ153_spl
| ~ sQ144_spl ),
inference(contradiction_clause,[status(thm)],[f2126]) ).
fof(f2213,plain,
~ less_or_equal(n8,n6),
inference(resolution,[status(thm)],[f2074,f202]) ).
fof(f2249,plain,
~ less(n8,n6),
inference(resolution,[status(thm)],[f2213,f171]) ).
fof(f2250,plain,
~ less(n8,n5),
inference(resolution,[status(thm)],[f2249,f631]) ).
fof(f2297,plain,
~ less(n8,n4),
inference(resolution,[status(thm)],[f2250,f626]) ).
fof(f2404,plain,
~ less(n8,n3),
inference(resolution,[status(thm)],[f2297,f547]) ).
fof(f2469,definition,
( sQ185_spl
<=> holdsAt(filling,n0) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f2470,plain,
( ~ sQ185_spl
| holdsAt(filling,n0) ),
inference(component_clause,[status(thm)],[f2469]) ).
fof(f2479,definition,
( sQ188_spl
<=> holdsAt(waterLevel(n3),plus(n0,n1)) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f2480,plain,
( ~ sQ188_spl
| holdsAt(waterLevel(n3),plus(n0,n1)) ),
inference(component_clause,[status(thm)],[f2479]) ).
fof(f2481,plain,
( sQ188_spl
| ~ holdsAt(waterLevel(n3),plus(n0,n1)) ),
inference(component_clause,[status(thm)],[f2479]) ).
fof(f2483,plain,
( ~ sQ188_spl
| holdsAt(waterLevel(n3),n1) ),
inference(forward_demodulation,[status(thm)],[f158,f2480]) ).
fof(f2485,plain,
( ~ sQ188_spl
| ~ holdsAt(filling,n1)
| happens(overflow,n1) ),
inference(resolution,[status(thm)],[f2483,f253]) ).
fof(f2491,definition,
( sQ189_spl
<=> happens(overflow,n1) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f2494,definition,
( sQ190_spl
<=> holdsAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f2495,plain,
( ~ sQ190_spl
| holdsAt(filling,n1) ),
inference(component_clause,[status(thm)],[f2494]) ).
fof(f2497,plain,
( ~ sQ188_spl
| ~ sQ190_spl
| sQ189_spl ),
inference(split_clause,[status(thm)],[f2485,f2491,f2494,f2479]) ).
fof(f2512,plain,
( sQ188_spl
| ~ holdsAt(waterLevel(n3),n1) ),
inference(forward_demodulation,[status(thm)],[f158,f2481]) ).
fof(f2599,plain,
! [X0] :
( ~ less(X0,n8)
| less(X0,n9) ),
inference(resolution,[status(thm)],[f210,f171]) ).
fof(f2654,plain,
less(n4,n5),
inference(resolution,[status(thm)],[f194,f255]) ).
fof(f2771,plain,
~ less_or_equal(n4,n3),
inference(resolution,[status(thm)],[f190,f256]) ).
fof(f2834,definition,
( sQ218_spl
<=> releasedAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition]) ).
fof(f2837,definition,
( sQ219_spl
<=> releases(sK7_skl(n1,filling),filling,n1) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f2838,plain,
( ~ sQ219_spl
| releases(sK7_skl(n1,filling),filling,n1) ),
inference(component_clause,[status(thm)],[f2837]) ).
fof(f2859,plain,
( ~ sQ99_spl
| happens(overflow,n2) ),
inference(forward_demodulation,[status(thm)],[f1060,f223]) ).
fof(f3274,plain,
( ~ sQ99_spl
| ~ sQ94_spl
| happens(overflow,n3) ),
inference(backward_demodulation,[status(thm)],[f967,f2859]) ).
fof(f3443,plain,
~ less_or_equal(n8,n2),
inference(resolution,[status(thm)],[f2404,f186]) ).
fof(f3624,plain,
~ less(n8,n3),
inference(resolution,[status(thm)],[f3443,f185]) ).
fof(f3625,plain,
~ less(n8,n2),
inference(resolution,[status(thm)],[f3443,f171]) ).
fof(f3823,definition,
( sQ254_spl
<=> happens(overflow,n2) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f3824,plain,
( ~ sQ254_spl
| happens(overflow,n2) ),
inference(component_clause,[status(thm)],[f3823]) ).
fof(f3965,definition,
( sQ277_spl
<=> terminates(sK6_skl(n2,waterLevel(n0)),waterLevel(n0),n2) ),
introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition]) ).
fof(f3966,plain,
( ~ sQ277_spl
| terminates(sK6_skl(n2,waterLevel(n0)),waterLevel(n0),n2) ),
inference(component_clause,[status(thm)],[f3965]) ).
fof(f4324,definition,
( sQ299_spl
<=> holdsAt(waterLevel(n3),n2) ),
introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition]) ).
fof(f4325,plain,
( ~ sQ299_spl
| holdsAt(waterLevel(n3),n2) ),
inference(component_clause,[status(thm)],[f4324]) ).
fof(f4357,plain,
( ~ sQ98_spl
| happens(tapOff,n2) ),
inference(forward_demodulation,[status(thm)],[f1057,f223]) ).
fof(f4376,definition,
( sQ302_spl
<=> less(n8,n7) ),
introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).
fof(f4391,definition,
( sQ305_spl
<=> happens(tapOff,n2) ),
introduced(definition,[new_symbols(definition,[sQ305_spl])],[split_symbol_definition]) ).
fof(f4392,plain,
( ~ sQ305_spl
| happens(tapOff,n2) ),
inference(component_clause,[status(thm)],[f4391]) ).
fof(f4393,plain,
( sQ305_spl
| ~ happens(tapOff,n2) ),
inference(component_clause,[status(thm)],[f4391]) ).
fof(f4396,plain,
( sQ305_spl
| ~ sQ98_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4393,f4357]) ).
fof(f4397,plain,
( sQ305_spl
| ~ sQ98_spl ),
inference(contradiction_clause,[status(thm)],[f4396]) ).
fof(f4495,definition,
( sQ308_spl
<=> releasedAt(filling,plus(n0,n1)) ),
introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition]) ).
fof(f4497,plain,
( sQ308_spl
| ~ releasedAt(filling,plus(n0,n1)) ),
inference(component_clause,[status(thm)],[f4495]) ).
fof(f4503,plain,
( sQ308_spl
| ~ releasedAt(filling,n1) ),
inference(forward_demodulation,[status(thm)],[f158,f4497]) ).
fof(f4610,definition,
( sQ314_spl
<=> holdsAt(filling,plus(n0,n1)) ),
introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition]) ).
fof(f4611,plain,
( ~ sQ314_spl
| holdsAt(filling,plus(n0,n1)) ),
inference(component_clause,[status(thm)],[f4610]) ).
fof(f4621,plain,
( ~ sQ314_spl
| holdsAt(filling,n1) ),
inference(forward_demodulation,[status(thm)],[f158,f4611]) ).
fof(f4695,plain,
( ~ sQ121_spl
| ~ happens(overflow,n1) ),
inference(resolution,[status(thm)],[f1634,f251]) ).
fof(f4714,plain,
! [X0] :
( ~ less(n8,X0)
| ~ less(X0,n7) ),
inference(resolution,[status(thm)],[f780,f213]) ).
fof(f4757,plain,
! [X0] :
( ~ less(n9,X0)
| ~ less(X0,n8) ),
inference(resolution,[status(thm)],[f873,f213]) ).
fof(f4769,plain,
! [X0] :
( ~ sQ299_spl
| X0 = n3
| ~ holdsAt(waterLevel(X0),n2) ),
inference(resolution,[status(thm)],[f4325,f146]) ).
fof(f4857,plain,
! [X0] : X0 = sK9_skl(waterLevel(X0),tapOn),
inference(resolution,[status(thm)],[f1086,f155]) ).
fof(f5024,plain,
trajectory(filling,n0,waterLevel(n2),n2),
inference(paramodulation,[status(thm)],[f159,f1287]) ).
fof(f5029,definition,
! [X0] :
( sQ332_spl
<=> ( ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ) ),
introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition]) ).
fof(f5030,plain,
! [X0] :
( ~ sQ332_spl
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(component_clause,[status(thm)],[f5029]) ).
fof(f5105,definition,
( sQ337_spl
<=> tapOff = tapOn ),
introduced(definition,[new_symbols(definition,[sQ337_spl])],[split_symbol_definition]) ).
fof(f5106,plain,
( ~ sQ337_spl
| tapOff = tapOn ),
inference(component_clause,[status(thm)],[f5105]) ).
fof(f5113,plain,
( ~ sQ337_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5106,f147]) ).
fof(f5114,plain,
~ sQ337_spl,
inference(contradiction_clause,[status(thm)],[f5113]) ).
fof(f5138,plain,
! [X0] :
( ~ sQ299_spl
| sK9_skl(waterLevel(X0),tapOn) = n3
| ~ holdsAt(waterLevel(X0),n2) ),
inference(paramodulation,[status(thm)],[f1086,f4769]) ).
fof(f5167,plain,
! [X0] :
( sQ188_spl
| n1 = n0
| ~ happens(X0,n1) ),
inference(resolution,[status(thm)],[f2512,f1089]) ).
fof(f5168,plain,
( sQ188_spl
| sQ104_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f5167,f1981,f1129,f2479]) ).
fof(f5256,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)],[f5024,f75]) ).
fof(f5257,definition,
( sQ352_spl
<=> stoppedIn(n0,filling,plus(n0,n2)) ),
introduced(definition,[new_symbols(definition,[sQ352_spl])],[split_symbol_definition]) ).
fof(f5258,plain,
( ~ sQ352_spl
| stoppedIn(n0,filling,plus(n0,n2)) ),
inference(component_clause,[status(thm)],[f5257]) ).
fof(f5260,definition,
( sQ353_spl
<=> holdsAt(waterLevel(n2),plus(n0,n2)) ),
introduced(definition,[new_symbols(definition,[sQ353_spl])],[split_symbol_definition]) ).
fof(f5261,plain,
( ~ sQ353_spl
| holdsAt(waterLevel(n2),plus(n0,n2)) ),
inference(component_clause,[status(thm)],[f5260]) ).
fof(f5263,plain,
( sQ353_spl
| sQ352_spl
| ~ sQ50_spl
| sQ332_spl ),
inference(split_clause,[status(thm)],[f5256,f5029,f680,f5257,f5260]) ).
fof(f5264,plain,
( ~ sQ353_spl
| holdsAt(waterLevel(n2),n2) ),
inference(forward_demodulation,[status(thm)],[f159,f5261]) ).
fof(f5265,plain,
( ~ sQ352_spl
| stoppedIn(n0,filling,n2) ),
inference(forward_demodulation,[status(thm)],[f159,f5258]) ).
fof(f5266,plain,
( ~ sQ352_spl
| sQ152_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5265,f2120]) ).
fof(f5267,plain,
( ~ sQ352_spl
| sQ152_spl ),
inference(contradiction_clause,[status(thm)],[f5266]) ).
fof(f5323,plain,
( ~ sQ150_spl
| sK1_skl(n2,filling,n0) = n0 ),
inference(resolution,[status(thm)],[f2110,f531]) ).
fof(f5368,plain,
( ~ sQ150_spl
| less(n0,n0)
| ~ stoppedIn(n0,filling,n2) ),
inference(paramodulation,[status(thm)],[f5323,f61]) ).
fof(f5382,plain,
( ~ sQ150_spl
| sQ68_spl
| ~ sQ152_spl ),
inference(split_clause,[status(thm)],[f5368,f2118,f810,f2109]) ).
fof(f5739,plain,
sP0_prd(n0,waterLevel(n0),tapOff),
inference(resolution,[status(thm)],[f216,f257]) ).
fof(f5836,plain,
( ~ sQ62_spl
| n2 = n0
| sK0_skl(n3,filling,n1) = overflow ),
inference(resolution,[status(thm)],[f745,f1256]) ).
fof(f5841,definition,
( sQ406_spl
<=> sK0_skl(n3,filling,n1) = overflow ),
introduced(definition,[new_symbols(definition,[sQ406_spl])],[split_symbol_definition]) ).
fof(f5842,plain,
( ~ sQ406_spl
| sK0_skl(n3,filling,n1) = overflow ),
inference(component_clause,[status(thm)],[f5841]) ).
fof(f5848,plain,
( ~ sQ62_spl
| sQ100_spl
| sQ406_spl ),
inference(split_clause,[status(thm)],[f5836,f5841,f1114,f744]) ).
fof(f5872,plain,
( ~ sQ406_spl
| happens(overflow,sK1_skl(n3,filling,n1))
| ~ stoppedIn(n1,filling,n3) ),
inference(paramodulation,[status(thm)],[f5842,f60]) ).
fof(f5885,definition,
( sQ411_spl
<=> happens(overflow,sK1_skl(n3,filling,n1)) ),
introduced(definition,[new_symbols(definition,[sQ411_spl])],[split_symbol_definition]) ).
fof(f5886,plain,
( ~ sQ411_spl
| happens(overflow,sK1_skl(n3,filling,n1)) ),
inference(component_clause,[status(thm)],[f5885]) ).
fof(f5888,plain,
( ~ sQ406_spl
| sQ411_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f5872,f732,f5885,f5841]) ).
fof(f5895,plain,
( ~ sQ411_spl
| ~ sQ39_spl
| happens(overflow,n2) ),
inference(forward_demodulation,[status(thm)],[f597,f5886]) ).
fof(f6285,plain,
( ~ sQ190_spl
| releasedAt(filling,n1)
| holdsAt(filling,n0)
| sK5_skl(n0,filling) = tapOn ),
inference(resolution,[status(thm)],[f1680,f2495]) ).
fof(f6287,definition,
( sQ460_spl
<=> sK5_skl(n0,filling) = tapOn ),
introduced(definition,[new_symbols(definition,[sQ460_spl])],[split_symbol_definition]) ).
fof(f6288,plain,
( ~ sQ460_spl
| sK5_skl(n0,filling) = tapOn ),
inference(component_clause,[status(thm)],[f6287]) ).
fof(f6290,plain,
( ~ sQ190_spl
| sQ218_spl
| sQ185_spl
| sQ460_spl ),
inference(split_clause,[status(thm)],[f6285,f6287,f2469,f2834,f2494]) ).
fof(f6313,definition,
( sQ463_spl
<=> happens(tapOn,n0) ),
introduced(definition,[new_symbols(definition,[sQ463_spl])],[split_symbol_definition]) ).
fof(f6314,plain,
( ~ sQ463_spl
| happens(tapOn,n0) ),
inference(component_clause,[status(thm)],[f6313]) ).
fof(f6315,plain,
( sQ463_spl
| ~ happens(tapOn,n0) ),
inference(component_clause,[status(thm)],[f6313]) ).
fof(f6317,definition,
( sQ464_spl
<=> initiates(tapOn,filling,n0) ),
introduced(definition,[new_symbols(definition,[sQ464_spl])],[split_symbol_definition]) ).
fof(f6318,plain,
( ~ sQ464_spl
| initiates(tapOn,filling,n0) ),
inference(component_clause,[status(thm)],[f6317]) ).
fof(f6319,plain,
( sQ464_spl
| ~ initiates(tapOn,filling,n0) ),
inference(component_clause,[status(thm)],[f6317]) ).
fof(f6349,plain,
( sQ463_spl
| ~ sP1_prd(n0,tapOn) ),
inference(resolution,[status(thm)],[f6315,f139]) ).
fof(f6350,plain,
( sQ463_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6349,f258]) ).
fof(f6351,plain,
sQ463_spl,
inference(contradiction_clause,[status(thm)],[f6350]) ).
fof(f6406,plain,
( sQ308_spl
| ~ sQ218_spl ),
inference(split_clause,[status(thm)],[f4503,f2834,f4495]) ).
fof(f6447,plain,
( ~ sQ411_spl
| ~ sQ39_spl
| sQ254_spl ),
inference(split_clause,[status(thm)],[f5895,f3823,f596,f5885]) ).
fof(f6451,plain,
! [X0] :
( ~ sQ299_spl
| X0 = n3
| ~ holdsAt(waterLevel(X0),n2) ),
inference(forward_demodulation,[status(thm)],[f4857,f5138]) ).
fof(f6480,plain,
( ~ sQ464_spl
| holdsAt(filling,plus(n0,n1))
| ~ happens(tapOn,n0) ),
inference(resolution,[status(thm)],[f6318,f97]) ).
fof(f6481,plain,
( ~ sQ464_spl
| ~ releasedAt(filling,plus(n0,n1))
| ~ happens(tapOn,n0) ),
inference(resolution,[status(thm)],[f6318,f106]) ).
fof(f6490,plain,
( ~ sQ464_spl
| sQ314_spl
| ~ sQ463_spl ),
inference(split_clause,[status(thm)],[f6480,f6313,f4610,f6317]) ).
fof(f6491,plain,
( ~ sQ464_spl
| ~ sQ308_spl
| ~ sQ463_spl ),
inference(split_clause,[status(thm)],[f6481,f6313,f4495,f6317]) ).
fof(f6496,plain,
( ~ sQ314_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f4621,f2494,f4610]) ).
fof(f6578,plain,
( sQ464_spl
| ~ sP2_prd(filling,tapOn) ),
inference(resolution,[status(thm)],[f6319,f470]) ).
fof(f6579,plain,
( sQ464_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6578,f259]) ).
fof(f6580,plain,
sQ464_spl,
inference(contradiction_clause,[status(thm)],[f6579]) ).
fof(f6581,plain,
( ~ sQ121_spl
| ~ sQ189_spl ),
inference(split_clause,[status(thm)],[f4695,f2491,f1633]) ).
fof(f6582,plain,
( ~ sQ185_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2470,f217]) ).
fof(f6583,plain,
~ sQ185_spl,
inference(contradiction_clause,[status(thm)],[f6582]) ).
fof(f6782,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| ~ less(n4,X0) ),
inference(resolution,[status(thm)],[f1684,f186]) ).
fof(f6794,definition,
( sQ491_spl
<=> less(n4,n3) ),
introduced(definition,[new_symbols(definition,[sQ491_spl])],[split_symbol_definition]) ).
fof(f6931,plain,
( ~ sQ91_spl
| ~ less_or_equal(n3,n3) ),
inference(backward_demodulation,[status(thm)],[f955,f2771]) ).
fof(f6951,plain,
( ~ sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6931,f255]) ).
fof(f6952,plain,
~ sQ91_spl,
inference(contradiction_clause,[status(thm)],[f6951]) ).
fof(f7049,plain,
( ~ sQ254_spl
| n2 = n0
| holdsAt(waterLevel(n3),n2) ),
inference(resolution,[status(thm)],[f1713,f3824]) ).
fof(f7058,plain,
( ~ sQ254_spl
| sQ100_spl
| sQ299_spl ),
inference(split_clause,[status(thm)],[f7049,f4324,f1114,f3823]) ).
fof(f7188,definition,
( sQ516_spl
<=> holdsAt(waterLevel(n0),n0) ),
introduced(definition,[new_symbols(definition,[sQ516_spl])],[split_symbol_definition]) ).
fof(f7190,plain,
( sQ516_spl
| ~ holdsAt(waterLevel(n0),n0) ),
inference(component_clause,[status(thm)],[f7188]) ).
fof(f7253,definition,
( sQ523_spl
<=> n9 = n3 ),
introduced(definition,[new_symbols(definition,[sQ523_spl])],[split_symbol_definition]) ).
fof(f7254,plain,
( ~ sQ523_spl
| n9 = n3 ),
inference(component_clause,[status(thm)],[f7253]) ).
fof(f7256,definition,
( sQ524_spl
<=> n9 = n2 ),
introduced(definition,[new_symbols(definition,[sQ524_spl])],[split_symbol_definition]) ).
fof(f7257,plain,
( ~ sQ524_spl
| n9 = n2 ),
inference(component_clause,[status(thm)],[f7256]) ).
fof(f7265,plain,
( ~ sQ524_spl
| less(n8,n2) ),
inference(backward_demodulation,[status(thm)],[f7257,f874]) ).
fof(f7282,plain,
( ~ sQ524_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7265,f3625]) ).
fof(f7283,plain,
~ sQ524_spl,
inference(contradiction_clause,[status(thm)],[f7282]) ).
fof(f7286,plain,
! [X0] :
( ~ sQ523_spl
| ~ less_or_equal(X0,n8)
| less(X0,n3) ),
inference(forward_demodulation,[status(thm)],[f7254,f210]) ).
fof(f7289,plain,
( ~ sQ523_spl
| less(n8,n3) ),
inference(resolution,[status(thm)],[f7286,f255]) ).
fof(f7290,plain,
( ~ sQ523_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7289,f3624]) ).
fof(f7291,plain,
~ sQ523_spl,
inference(contradiction_clause,[status(thm)],[f7290]) ).
fof(f7641,definition,
( sQ535_spl
<=> less(n9,n8) ),
introduced(definition,[new_symbols(definition,[sQ535_spl])],[split_symbol_definition]) ).
fof(f7789,plain,
! [X0] :
( ~ less(X0,n3)
| ~ less(n4,X0) ),
inference(resolution,[status(thm)],[f6782,f185]) ).
fof(f7825,definition,
( sQ550_spl
<=> n5 = n0 ),
introduced(definition,[new_symbols(definition,[sQ550_spl])],[split_symbol_definition]) ).
fof(f7826,plain,
( ~ sQ550_spl
| n5 = n0 ),
inference(component_clause,[status(thm)],[f7825]) ).
fof(f7856,plain,
( ~ sQ550_spl
| less(n4,n0) ),
inference(backward_demodulation,[status(thm)],[f7826,f2654]) ).
fof(f7891,plain,
( ~ sQ550_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7856,f174]) ).
fof(f7892,plain,
~ sQ550_spl,
inference(contradiction_clause,[status(thm)],[f7891]) ).
fof(f7995,plain,
( ~ sQ277_spl
| waterLevel(n0) = filling ),
inference(resolution,[status(thm)],[f3966,f249]) ).
fof(f8016,plain,
( ~ sQ277_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7995,f150]) ).
fof(f8017,plain,
~ sQ277_spl,
inference(contradiction_clause,[status(thm)],[f8016]) ).
fof(f8414,plain,
( ~ less(n4,n3)
| ~ less(n4,n3) ),
inference(resolution,[status(thm)],[f547,f7789]) ).
fof(f8422,plain,
~ sQ491_spl,
inference(split_clause,[status(thm)],[f8414,f6794]) ).
fof(f8479,definition,
( sQ581_spl
<=> waterLevel(n0) = filling ),
introduced(definition,[new_symbols(definition,[sQ581_spl])],[split_symbol_definition]) ).
fof(f8480,plain,
( ~ sQ581_spl
| waterLevel(n0) = filling ),
inference(component_clause,[status(thm)],[f8479]) ).
fof(f8482,definition,
( sQ582_spl
<=> waterLevel(n0) = spilling ),
introduced(definition,[new_symbols(definition,[sQ582_spl])],[split_symbol_definition]) ).
fof(f8483,plain,
( ~ sQ582_spl
| waterLevel(n0) = spilling ),
inference(component_clause,[status(thm)],[f8482]) ).
fof(f8504,plain,
( ~ sQ582_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8483,f151]) ).
fof(f8505,plain,
~ sQ582_spl,
inference(contradiction_clause,[status(thm)],[f8504]) ).
fof(f8506,plain,
( ~ sQ581_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8480,f150]) ).
fof(f8507,plain,
~ sQ581_spl,
inference(contradiction_clause,[status(thm)],[f8506]) ).
fof(f8558,definition,
! [X0] :
( sQ588_spl
<=> ~ initiates(tapOff,waterLevel(n0),X0) ),
introduced(definition,[new_symbols(definition,[sQ588_spl])],[split_symbol_definition]) ).
fof(f8559,plain,
! [X0] :
( ~ sQ588_spl
| ~ initiates(tapOff,waterLevel(n0),X0) ),
inference(component_clause,[status(thm)],[f8558]) ).
fof(f9498,plain,
( ~ sQ305_spl
| tapOff = tapOn
| tapOff = overflow ),
inference(resolution,[status(thm)],[f4392,f1257]) ).
fof(f9508,plain,
( ~ sQ305_spl
| sQ337_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f9498,f1036,f5105,f4391]) ).
fof(f9592,plain,
( ~ less(n8,n7)
| ~ less(n8,n7) ),
inference(resolution,[status(thm)],[f4714,f780]) ).
fof(f9613,plain,
~ sQ302_spl,
inference(split_clause,[status(thm)],[f9592,f4376]) ).
fof(f9627,plain,
( ~ less(n9,n8)
| ~ less(n9,n8) ),
inference(resolution,[status(thm)],[f4757,f2599]) ).
fof(f9645,plain,
~ sQ535_spl,
inference(split_clause,[status(thm)],[f9627,f7641]) ).
fof(f9883,plain,
( sQ516_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7190,f216]) ).
fof(f9884,plain,
sQ516_spl,
inference(contradiction_clause,[status(thm)],[f9883]) ).
fof(f9932,definition,
! [X0] :
( sQ704_spl
<=> ~ initiates(overflow,waterLevel(n0),X0) ),
introduced(definition,[new_symbols(definition,[sQ704_spl])],[split_symbol_definition]) ).
fof(f9933,plain,
! [X0] :
( ~ sQ704_spl
| ~ initiates(overflow,waterLevel(n0),X0) ),
inference(component_clause,[status(thm)],[f9932]) ).
fof(f9936,plain,
( ~ sQ704_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1033,f9933]) ).
fof(f9938,plain,
~ sQ704_spl,
inference(contradiction_clause,[status(thm)],[f9936]) ).
fof(f9949,plain,
initiates(tapOff,waterLevel(n0),n0),
inference(resolution,[status(thm)],[f5739,f116]) ).
fof(f9966,plain,
( ~ sQ588_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9949,f8559]) ).
fof(f9967,plain,
~ sQ588_spl,
inference(contradiction_clause,[status(thm)],[f9966]) ).
fof(f10095,plain,
( ~ sQ219_spl
| filling = waterLevel(sK9_skl(filling,sK7_skl(n1,filling))) ),
inference(resolution,[status(thm)],[f2838,f130]) ).
fof(f10101,plain,
( ~ sQ219_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10095,f150]) ).
fof(f10102,plain,
~ sQ219_spl,
inference(contradiction_clause,[status(thm)],[f10101]) ).
fof(f10226,definition,
( sQ726_spl
<=> happens(overflow,n3) ),
introduced(definition,[new_symbols(definition,[sQ726_spl])],[split_symbol_definition]) ).
fof(f10227,plain,
( ~ sQ726_spl
| happens(overflow,n3) ),
inference(component_clause,[status(thm)],[f10226]) ).
fof(f10243,plain,
( ~ sQ726_spl
| ~ sQ123_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10227,f1663]) ).
fof(f10244,plain,
( ~ sQ726_spl
| ~ sQ123_spl ),
inference(contradiction_clause,[status(thm)],[f10243]) ).
fof(f12299,definition,
( sQ894_spl
<=> waterLevel(n1) = spilling ),
introduced(definition,[new_symbols(definition,[sQ894_spl])],[split_symbol_definition]) ).
fof(f12300,plain,
( ~ sQ894_spl
| waterLevel(n1) = spilling ),
inference(component_clause,[status(thm)],[f12299]) ).
fof(f12303,definition,
( sQ895_spl
<=> waterLevel(n1) = filling ),
introduced(definition,[new_symbols(definition,[sQ895_spl])],[split_symbol_definition]) ).
fof(f12304,plain,
( ~ sQ895_spl
| waterLevel(n1) = filling ),
inference(component_clause,[status(thm)],[f12303]) ).
fof(f12324,plain,
( ~ sQ894_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12300,f151]) ).
fof(f12325,plain,
~ sQ894_spl,
inference(contradiction_clause,[status(thm)],[f12324]) ).
fof(f12326,plain,
( ~ sQ895_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12304,f150]) ).
fof(f12327,plain,
~ sQ895_spl,
inference(contradiction_clause,[status(thm)],[f12326]) ).
fof(f12927,definition,
( sQ966_spl
<=> stoppedIn(n0,filling,plus(n0,n0)) ),
introduced(definition,[new_symbols(definition,[sQ966_spl])],[split_symbol_definition]) ).
fof(f12928,plain,
( ~ sQ966_spl
| stoppedIn(n0,filling,plus(n0,n0)) ),
inference(component_clause,[status(thm)],[f12927]) ).
fof(f12935,plain,
( ~ sQ966_spl
| stoppedIn(n0,filling,n0) ),
inference(forward_demodulation,[status(thm)],[f157,f12928]) ).
fof(f12939,plain,
( ~ sQ966_spl
| less(sK1_skl(n0,filling,n0),n0) ),
inference(resolution,[status(thm)],[f12935,f62]) ).
fof(f12947,plain,
( ~ sQ966_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12939,f174]) ).
fof(f12948,plain,
~ sQ966_spl,
inference(contradiction_clause,[status(thm)],[f12947]) ).
fof(f12960,plain,
( ~ sQ332_spl
| ~ holdsAt(filling,plus(n0,n1))
| releasedAt(filling,plus(n0,n1))
| holdsAt(filling,n0)
| ~ happens(sK5_skl(n0,filling),n0) ),
inference(resolution,[status(thm)],[f5030,f86]) ).
fof(f12963,definition,
( sQ970_spl
<=> happens(sK5_skl(n0,filling),n0) ),
introduced(definition,[new_symbols(definition,[sQ970_spl])],[split_symbol_definition]) ).
fof(f12965,plain,
( sQ970_spl
| ~ happens(sK5_skl(n0,filling),n0) ),
inference(component_clause,[status(thm)],[f12963]) ).
fof(f12966,plain,
( ~ sQ332_spl
| ~ sQ314_spl
| sQ308_spl
| sQ185_spl
| ~ sQ970_spl ),
inference(split_clause,[status(thm)],[f12960,f12963,f2469,f4495,f4610,f5029]) ).
fof(f12967,plain,
( sQ970_spl
| ~ sQ460_spl
| ~ happens(tapOn,n0) ),
inference(forward_demodulation,[status(thm)],[f6288,f12965]) ).
fof(f12968,plain,
( sQ970_spl
| ~ sQ460_spl
| ~ sQ463_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12967,f6314]) ).
fof(f12969,plain,
( sQ970_spl
| ~ sQ460_spl
| ~ sQ463_spl ),
inference(contradiction_clause,[status(thm)],[f12968]) ).
fof(f12975,plain,
( ~ sQ352_spl
| less(sK1_skl(n2,filling,n0),n2) ),
inference(resolution,[status(thm)],[f5265,f62]) ).
fof(f12980,plain,
( ~ sQ352_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f12975,f566,f5257]) ).
fof(f13002,plain,
( ~ sQ299_spl
| ~ sQ353_spl
| n2 = n3 ),
inference(resolution,[status(thm)],[f5264,f6451]) ).
fof(f13012,plain,
( ~ sQ299_spl
| ~ sQ353_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f13002,f966,f5260,f4324]) ).
fof(f13026,plain,
( ~ sQ99_spl
| ~ sQ94_spl
| sQ726_spl ),
inference(split_clause,[status(thm)],[f3274,f10226,f966,f1059]) ).
fof(f13033,plain,
$false,
inference(sat_refutation,[status(thm)],[f275,f298,f571,f602,f613,f700,f747,f766,f769,f821,f1048,f1062,f1120,f1171,f1223,f1408,f1487,f1500,f1639,f1665,f1731,f1841,f1851,f1954,f2052,f2054,f2115,f2125,f2127,f2497,f4397,f5114,f5168,f5263,f5267,f5382,f5848,f5888,f6290,f6351,f6406,f6447,f6490,f6491,f6496,f6580,f6581,f6583,f6952,f7058,f7283,f7291,f7892,f8017,f8422,f8505,f8507,f9508,f9613,f9645,f9884,f9938,f9967,f10102,f10244,f12325,f12327,f12948,f12966,f12969,f12980,f13012,f13026]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR013+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n018.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 14:25:58 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 21.42/3.12 % Refutation found
% 21.42/3.12 % SZS status Theorem for theBenchmark: Theorem is valid
% 21.42/3.12 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 21.42/3.16 % Elapsed time: 2.788362 seconds
% 21.42/3.16 % CPU time: 21.839442 seconds
% 21.42/3.16 % Total memory used: 268.997 MB
% 21.42/3.16 % Net memory used: 252.197 MB
%------------------------------------------------------------------------------