%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR001+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:47 PM UTC 2026
% Result : Theorem 18.66s 2.87s
% Output : CNFRefutation 18.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 24
% Syntax : Number of formulae : 175 ( 41 unt; 3 def)
% Number of atoms : 596 ( 181 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 645 ( 224 ~; 302 |; 101 &)
% ( 14 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 10 con; 0-3 aty)
% Number of variables : 277 ( 261 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
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(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(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(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(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(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(f32,axiom,
plus(n1,n3) = n4,
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(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(f53,hypothesis,
~ releasedAt(filling,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,lemma,
holdsAt(waterLevel(n3),n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,conjecture,
holdsAt(waterLevel(n3),n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,negated_conjecture,
~ holdsAt(waterLevel(n3),n4),
inference(negated_conjecture,[status(cth)],[f56]) ).
fof(f80,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(f81,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))],[f80]) ).
fof(f82,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)],[f81]) ).
fof(f92,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(f93,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))],[f92]) ).
fof(f94,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| happens(sK7_skl(X1,X0),X1)
| releasedAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f95,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releases(sK7_skl(X1,X0),X0,X1)
| releasedAt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f96,plain,
! [Event,Time,Fluent] :
( holdsAt(Fluent,plus(Time,n1))
| ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f97,plain,
! [Time,Fluent] :
( holdsAt(Fluent,plus(Time,n1))
| ! [Event] :
( ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f96]) ).
fof(f98,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f105,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(f106,plain,
! [Time,Fluent] :
( ~ releasedAt(Fluent,plus(Time,n1))
| ! [Event] :
( ( ~ terminates(Event,Fluent,Time)
& ~ initiates(Event,Fluent,Time) )
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f105]) ).
fof(f107,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f109,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(f110,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,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) )
& ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = overflow
& holdsAt(waterLevel(Height),Time) )
| sP0_prd(Time,Fluent,Event)
| ~ initiates(Event,Fluent,Time) ) ),
inference(NNF_transformation,[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] :
( ? [Height] :
( Fluent = waterLevel(Height)
& Event = overflow
& holdsAt(waterLevel(Height),Time) )
| sP0_prd(Time,Fluent,Event)
| ~ initiates(Event,Fluent,Time) ) ),
inference(miniscoping,[status(thm)],[f111]) ).
fof(f113,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))],[f112]) ).
fof(f117,plain,
! [X0,X1,X2] :
( ~ sP0_prd(X2,X1,X0)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f118,plain,
! [X0,X1,X2,X3] :
( X1 != waterLevel(X3)
| X0 != overflow
| ~ holdsAt(waterLevel(X3),X2)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f127,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(f128,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)],[f127]) ).
fof(f129,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))],[f128]) ).
fof(f131,plain,
! [X0,X1,X2] :
( X1 = waterLevel(sK9_skl(X1,X0))
| ~ releases(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f133,definition,
! [Event,Time] :
( sP1_prd(Time,Event)
<=> ( Time = n0
& Event = tapOn ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f134,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,f133]) ).
fof(f135,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)],[f134]) ).
fof(f136,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)],[f135]) ).
fof(f137,plain,
! [X0,X1] :
( holdsAt(waterLevel(n3),X1)
| sP1_prd(X1,X0)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f138,plain,
! [X0,X1] :
( holdsAt(filling,X1)
| sP1_prd(X1,X0)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f140,plain,
! [X0,X1] :
( ~ sP1_prd(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f141,plain,
! [X0,X1] :
( X0 != overflow
| ~ holdsAt(filling,X1)
| ~ holdsAt(waterLevel(n3),X1)
| happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f151,plain,
! [X0] : filling != waterLevel(X0),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f159,plain,
plus(n0,n1) = n1,
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f162,plain,
plus(n1,n1) = n2,
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f163,plain,
plus(n1,n2) = n3,
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f164,plain,
plus(n1,n3) = n4,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f168,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f169,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(f170,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)],[f169]) ).
fof(f172,plain,
! [X0,X1] :
( ~ less(X0,X1)
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f173,plain,
! [X0,X1] :
( X0 != X1
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f176,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(f177,plain,
( ! [X] :
( ~ less_or_equal(X,n0)
| less(X,n1) )
& ! [X] :
( less_or_equal(X,n0)
| ~ less(X,n1) ) ),
inference(miniscoping,[status(thm)],[f176]) ).
fof(f179,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f180,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(f181,plain,
( ! [X] :
( ~ less_or_equal(X,n1)
| less(X,n2) )
& ! [X] :
( less_or_equal(X,n1)
| ~ less(X,n2) ) ),
inference(miniscoping,[status(thm)],[f180]) ).
fof(f183,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f184,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(f185,plain,
( ! [X] :
( ~ less_or_equal(X,n2)
| less(X,n3) )
& ! [X] :
( less_or_equal(X,n2)
| ~ less(X,n3) ) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f187,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f212,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(f213,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)],[f212]) ).
fof(f215,plain,
! [X0,X1] :
( X1 != X0
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f221,plain,
~ releasedAt(filling,n0),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f223,plain,
holdsAt(waterLevel(n3),n3),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f224,plain,
~ holdsAt(waterLevel(n3),n4),
inference(cnf_transformation,[status(thm)],[f57]) ).
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)],[f109,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(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))],[f228]) ).
fof(f233,plain,
! [X0,X1,X2] :
( ~ sP2_prd(X1,X2)
| 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)],[f133]) ).
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(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)],[f118]) ).
fof(f253,plain,
! [X0] :
( ~ holdsAt(filling,X0)
| ~ holdsAt(waterLevel(n3),X0)
| happens(overflow,X0) ),
inference(destructive_equality_resolution,[status(thm)],[f141]) ).
fof(f255,plain,
! [X0] : less_or_equal(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f173]) ).
fof(f256,plain,
! [X0] : ~ less(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f215]) ).
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(f281,plain,
happens(tapOn,n0),
inference(resolution,[status(thm)],[f140,f258]) ).
fof(f282,plain,
n3 = plus(n2,n1),
inference(paramodulation,[status(thm)],[f163,f168]) ).
fof(f283,plain,
n4 = plus(n3,n1),
inference(paramodulation,[status(thm)],[f164,f168]) ).
fof(f386,plain,
! [X0] :
( holdsAt(X0,n4)
| happens(sK4_skl(n3,X0),n3)
| releasedAt(X0,plus(n3,n1))
| ~ holdsAt(X0,n3) ),
inference(paramodulation,[status(thm)],[f283,f82]) ).
fof(f387,plain,
! [X0] :
( holdsAt(X0,n3)
| happens(sK4_skl(n2,X0),n2)
| releasedAt(X0,plus(n2,n1))
| ~ holdsAt(X0,n2) ),
inference(paramodulation,[status(thm)],[f282,f82]) ).
fof(f388,plain,
! [X0] :
( holdsAt(X0,n2)
| happens(sK4_skl(n1,X0),n1)
| releasedAt(X0,plus(n1,n1))
| ~ holdsAt(X0,n1) ),
inference(paramodulation,[status(thm)],[f162,f82]) ).
fof(f392,plain,
! [X0] :
( holdsAt(X0,n4)
| happens(sK4_skl(n3,X0),n3)
| releasedAt(X0,n4)
| ~ holdsAt(X0,n3) ),
inference(forward_demodulation,[status(thm)],[f283,f386]) ).
fof(f393,plain,
! [X0] :
( holdsAt(X0,n3)
| happens(sK4_skl(n2,X0),n2)
| releasedAt(X0,n3)
| ~ holdsAt(X0,n2) ),
inference(forward_demodulation,[status(thm)],[f282,f387]) ).
fof(f394,plain,
! [X0] :
( holdsAt(X0,n2)
| happens(sK4_skl(n1,X0),n1)
| releasedAt(X0,n2)
| ~ holdsAt(X0,n1) ),
inference(forward_demodulation,[status(thm)],[f162,f388]) ).
fof(f437,plain,
! [X0,X1,X2] :
( ~ sP2_prd(X1,X0)
| initiates(X0,X1,X2) ),
inference(resolution,[status(thm)],[f117,f233]) ).
fof(f445,plain,
less(n0,n1),
inference(resolution,[status(thm)],[f179,f255]) ).
fof(f450,plain,
less_or_equal(n0,n1),
inference(resolution,[status(thm)],[f445,f172]) ).
fof(f455,plain,
! [X0] :
( ~ releasedAt(X0,n4)
| happens(sK7_skl(n3,X0),n3)
| releasedAt(X0,n3) ),
inference(paramodulation,[status(thm)],[f283,f94]) ).
fof(f456,plain,
! [X0] :
( ~ releasedAt(X0,n3)
| happens(sK7_skl(n2,X0),n2)
| releasedAt(X0,n2) ),
inference(paramodulation,[status(thm)],[f282,f94]) ).
fof(f471,plain,
less(n0,n2),
inference(resolution,[status(thm)],[f183,f450]) ).
fof(f477,plain,
less_or_equal(n0,n2),
inference(resolution,[status(thm)],[f471,f172]) ).
fof(f489,plain,
less(n0,n3),
inference(resolution,[status(thm)],[f187,f477]) ).
fof(f512,plain,
! [X0,X1] :
( holdsAt(X1,n4)
| ~ initiates(X0,X1,n3)
| ~ happens(X0,n3) ),
inference(paramodulation,[status(thm)],[f283,f98]) ).
fof(f515,plain,
! [X0,X1] :
( holdsAt(X1,n1)
| ~ initiates(X0,X1,n0)
| ~ happens(X0,n0) ),
inference(paramodulation,[status(thm)],[f159,f98]) ).
fof(f583,plain,
! [X0,X1] :
( ~ releasedAt(X1,n3)
| ~ initiates(X0,X1,n2)
| ~ happens(X0,n2) ),
inference(paramodulation,[status(thm)],[f282,f107]) ).
fof(f584,plain,
! [X0,X1] :
( ~ releasedAt(X1,n2)
| ~ initiates(X0,X1,n1)
| ~ happens(X0,n1) ),
inference(paramodulation,[status(thm)],[f162,f107]) ).
fof(f657,plain,
! [X0] :
( holdsAt(waterLevel(X0),n4)
| ~ happens(overflow,n3)
| ~ holdsAt(waterLevel(X0),n3) ),
inference(resolution,[status(thm)],[f248,f512]) ).
fof(f730,plain,
( holdsAt(waterLevel(n3),n4)
| ~ happens(overflow,n3) ),
inference(resolution,[status(thm)],[f657,f223]) ).
fof(f731,plain,
~ happens(overflow,n3),
inference(forward_subsumption_resolution,[status(thm)],[f730,f224]) ).
fof(f777,plain,
! [X0,X1] : ~ releases(X0,filling,X1),
inference(resolution,[status(thm)],[f131,f151]) ).
fof(f841,plain,
! [X0] :
( ~ releasedAt(filling,plus(X0,n1))
| releasedAt(filling,X0) ),
inference(resolution,[status(thm)],[f777,f95]) ).
fof(f856,plain,
( ~ holdsAt(filling,n3)
| happens(overflow,n3) ),
inference(resolution,[status(thm)],[f253,f223]) ).
fof(f857,plain,
! [X0,X1] :
( sP1_prd(X0,X1)
| ~ happens(X1,X0)
| ~ holdsAt(filling,X0)
| happens(overflow,X0) ),
inference(resolution,[status(thm)],[f253,f137]) ).
fof(f860,plain,
~ holdsAt(filling,n3),
inference(forward_subsumption_resolution,[status(thm)],[f856,f731]) ).
fof(f861,plain,
! [X0,X1] :
( sP1_prd(X0,X1)
| ~ happens(X1,X0)
| happens(overflow,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f857,f138]) ).
fof(f1373,plain,
! [X0] :
( ~ releasedAt(X0,n4)
| releasedAt(X0,n3)
| sP1_prd(n3,sK7_skl(n3,X0))
| happens(overflow,n3) ),
inference(resolution,[status(thm)],[f861,f455]) ).
fof(f1380,plain,
! [X0] :
( holdsAt(X0,n4)
| releasedAt(X0,n4)
| ~ holdsAt(X0,n3)
| sP1_prd(n3,sK4_skl(n3,X0))
| happens(overflow,n3) ),
inference(resolution,[status(thm)],[f861,f392]) ).
fof(f1386,plain,
! [X0] :
( ~ releasedAt(X0,n4)
| releasedAt(X0,n3)
| sP1_prd(n3,sK7_skl(n3,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1373,f731]) ).
fof(f1389,plain,
! [X0] :
( holdsAt(X0,n4)
| releasedAt(X0,n4)
| ~ holdsAt(X0,n3)
| sP1_prd(n3,sK4_skl(n3,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1380,f731]) ).
fof(f1459,plain,
! [X0] :
( n3 = n0
| ~ releasedAt(X0,n4)
| releasedAt(X0,n3) ),
inference(resolution,[status(thm)],[f1386,f238]) ).
fof(f1901,plain,
! [X0] :
( n3 = n0
| holdsAt(X0,n4)
| releasedAt(X0,n4)
| ~ holdsAt(X0,n3) ),
inference(resolution,[status(thm)],[f1389,f238]) ).
fof(f1905,plain,
( n3 = n0
| holdsAt(waterLevel(n3),n4)
| releasedAt(waterLevel(n3),n4) ),
inference(resolution,[status(thm)],[f1901,f223]) ).
fof(f1907,plain,
( n3 = n0
| releasedAt(waterLevel(n3),n4) ),
inference(forward_subsumption_resolution,[status(thm)],[f1905,f224]) ).
fof(f1912,plain,
( n3 = n0
| releasedAt(waterLevel(n3),n3)
| n3 = n0 ),
inference(resolution,[status(thm)],[f1907,f1459]) ).
fof(f1913,plain,
( releasedAt(waterLevel(n3),n3)
| n3 = n0 ),
inference(duplicate_literals_removal,[status(thm)],[f1912]) ).
fof(f2936,plain,
( ~ releasedAt(filling,n3)
| releasedAt(filling,n2) ),
inference(paramodulation,[status(thm)],[f282,f841]) ).
fof(f2937,plain,
( ~ releasedAt(filling,n2)
| releasedAt(filling,n1) ),
inference(paramodulation,[status(thm)],[f162,f841]) ).
fof(f2938,plain,
( ~ releasedAt(filling,n1)
| releasedAt(filling,n0) ),
inference(paramodulation,[status(thm)],[f159,f841]) ).
fof(f2941,plain,
~ releasedAt(filling,n1),
inference(forward_subsumption_resolution,[status(thm)],[f2938,f221]) ).
fof(f2942,plain,
~ releasedAt(filling,n3),
inference(backward_subsumption_resolution,[status(thm)],[f2936,f2944]) ).
fof(f2944,plain,
~ releasedAt(filling,n2),
inference(forward_subsumption_resolution,[status(thm)],[f2937,f2941]) ).
fof(f3261,plain,
! [X0,X1] :
( ~ sP2_prd(X1,X0)
| holdsAt(X1,n1)
| ~ happens(X0,n0) ),
inference(resolution,[status(thm)],[f515,f437]) ).
fof(f3264,plain,
( holdsAt(filling,n1)
| ~ happens(tapOn,n0) ),
inference(resolution,[status(thm)],[f3261,f259]) ).
fof(f3265,plain,
holdsAt(filling,n1),
inference(forward_subsumption_resolution,[status(thm)],[f3264,f281]) ).
fof(f3671,plain,
! [X0] :
( ~ holdsAt(waterLevel(X0),n2)
| ~ releasedAt(waterLevel(X0),n3)
| ~ happens(overflow,n2) ),
inference(resolution,[status(thm)],[f583,f248]) ).
fof(f3679,plain,
! [X0] :
( ~ holdsAt(waterLevel(X0),n1)
| ~ releasedAt(waterLevel(X0),n2)
| ~ happens(overflow,n1) ),
inference(resolution,[status(thm)],[f584,f248]) ).
fof(f9081,plain,
! [X0] :
( sP1_prd(n2,X0)
| ~ happens(X0,n2)
| ~ releasedAt(waterLevel(n3),n3)
| ~ happens(overflow,n2) ),
inference(resolution,[status(thm)],[f3671,f137]) ).
fof(f9082,plain,
! [X0] :
( sP1_prd(n2,X0)
| ~ happens(X0,n2)
| ~ releasedAt(waterLevel(n3),n3) ),
inference(forward_subsumption_resolution,[status(thm)],[f9081,f861]) ).
fof(f9083,plain,
! [X0] :
( n3 = n0
| sP1_prd(n2,X0)
| ~ happens(X0,n2) ),
inference(resolution,[status(thm)],[f9082,f1913]) ).
fof(f9086,plain,
! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2)
| n3 = n0
| sP1_prd(n2,sK7_skl(n2,X0)) ),
inference(resolution,[status(thm)],[f9083,f456]) ).
fof(f9096,plain,
! [X0] :
( holdsAt(X0,n3)
| releasedAt(X0,n3)
| ~ holdsAt(X0,n2)
| n3 = n0
| sP1_prd(n2,sK4_skl(n2,X0)) ),
inference(resolution,[status(thm)],[f9083,f393]) ).
fof(f9129,plain,
! [X0] :
( n2 = n0
| ~ releasedAt(X0,n3)
| releasedAt(X0,n2)
| n3 = n0 ),
inference(resolution,[status(thm)],[f9086,f238]) ).
fof(f9139,plain,
( n3 = n0
| n2 = n0
| releasedAt(waterLevel(n3),n2)
| n3 = n0 ),
inference(resolution,[status(thm)],[f9129,f1913]) ).
fof(f9150,plain,
( n2 = n0
| releasedAt(waterLevel(n3),n2)
| n3 = n0 ),
inference(duplicate_literals_removal,[status(thm)],[f9139]) ).
fof(f9322,plain,
! [X0] :
( sP1_prd(n1,X0)
| ~ happens(X0,n1)
| ~ releasedAt(waterLevel(n3),n2)
| ~ happens(overflow,n1) ),
inference(resolution,[status(thm)],[f3679,f137]) ).
fof(f9323,plain,
! [X0] :
( sP1_prd(n1,X0)
| ~ happens(X0,n1)
| ~ releasedAt(waterLevel(n3),n2) ),
inference(forward_subsumption_resolution,[status(thm)],[f9322,f861]) ).
fof(f9324,plain,
! [X0] :
( n2 = n0
| n3 = n0
| sP1_prd(n1,X0)
| ~ happens(X0,n1) ),
inference(resolution,[status(thm)],[f9323,f9150]) ).
fof(f9337,plain,
! [X0] :
( holdsAt(X0,n2)
| releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| n2 = n0
| n3 = n0
| sP1_prd(n1,sK4_skl(n1,X0)) ),
inference(resolution,[status(thm)],[f9324,f394]) ).
fof(f11199,plain,
! [X0] :
( n2 = n0
| holdsAt(X0,n3)
| releasedAt(X0,n3)
| ~ holdsAt(X0,n2)
| n3 = n0 ),
inference(resolution,[status(thm)],[f9096,f238]) ).
fof(f13013,plain,
! [X0] :
( n1 = n0
| holdsAt(X0,n2)
| releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| n2 = n0
| n3 = n0 ),
inference(resolution,[status(thm)],[f9337,f238]) ).
fof(f13015,plain,
( n1 = n0
| holdsAt(filling,n2)
| releasedAt(filling,n2)
| n2 = n0
| n3 = n0 ),
inference(resolution,[status(thm)],[f13013,f3265]) ).
fof(f13020,plain,
( n1 = n0
| holdsAt(filling,n2)
| n2 = n0
| n3 = n0 ),
inference(forward_subsumption_resolution,[status(thm)],[f13015,f2944]) ).
fof(f13022,plain,
( n2 = n0
| holdsAt(filling,n3)
| releasedAt(filling,n3)
| n3 = n0
| n1 = n0
| n2 = n0
| n3 = n0 ),
inference(resolution,[status(thm)],[f13020,f11199]) ).
fof(f13025,plain,
( holdsAt(filling,n3)
| releasedAt(filling,n3)
| n1 = n0
| n2 = n0
| n3 = n0 ),
inference(duplicate_literals_removal,[status(thm)],[f13022]) ).
fof(f13026,plain,
( holdsAt(filling,n3)
| n1 = n0
| n2 = n0
| n3 = n0 ),
inference(forward_subsumption_resolution,[status(thm)],[f13025,f2942]) ).
fof(f13027,plain,
( n1 = n0
| n2 = n0
| n3 = n0 ),
inference(forward_subsumption_resolution,[status(thm)],[f13026,f860]) ).
fof(f13092,plain,
( n2 = n0
| n3 = n0
| less(n1,n1) ),
inference(paramodulation,[status(thm)],[f13027,f445]) ).
fof(f13121,plain,
( n2 = n0
| n3 = n0 ),
inference(forward_subsumption_resolution,[status(thm)],[f13092,f256]) ).
fof(f13192,plain,
( n2 = n0
| less(n3,n3) ),
inference(paramodulation,[status(thm)],[f13121,f489]) ).
fof(f13220,plain,
n2 = n0,
inference(forward_subsumption_resolution,[status(thm)],[f13192,f256]) ).
fof(f13495,plain,
less(n2,n2),
inference(backward_demodulation,[status(thm)],[f13220,f471]) ).
fof(f13662,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f13495,f256]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR001+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.42 % Computer : n026.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Mon Sep 21 14:25:53 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.44 % Drodi V4.1.1
% 18.66/2.87 % Refutation found
% 18.66/2.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 18.66/2.87 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.11/2.93 % Elapsed time: 2.488846 seconds
% 3.11/2.93 % CPU time: 19.273334 seconds
% 3.11/2.93 % Total memory used: 227.415 MB
% 3.11/2.93 % Net memory used: 215.362 MB
%------------------------------------------------------------------------------