%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR008+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:14:34 PM UTC 2026
% Result : Theorem 12.43s 2.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR008+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/1.00 % Computer : n013.cluster.edu
% 0.10/1.00 % Model : x86_64 x86_64
% 0.10/1.00 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/1.00 % Memory : 8046.5625MB
% 0.10/1.00 % OS : Linux 6.8.0-71-generic
% 0.10/1.00 % CPULimit : 300
% 0.10/1.01 % WCLimit : 300
% 0.10/1.01 % DateTime : Mon Sep 21 14:23:38 UTC 2026
% 0.10/1.01 % CPUTime :
% 0.10/1.03 % Drodi V4.1.1
% 12.43/2.69 % Refutation found
% 12.43/2.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.43/2.69 % SZS output start CNFRefutation for theBenchmark
% 12.43/2.69 fof(f1,axiom,(
% 12.43/2.69 (! [Time1,Fluent,Time2] :( stoppedIn(Time1,Fluent,Time2)<=> (? [Event,Time] :( happens(Event,Time)& less(Time1,Time)& less(Time,Time2)& terminates(Event,Fluent,Time) ) )) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f3,axiom,(
% 12.43/2.69 (! [Event,Time,Fluent,Fluent2,Offset] :( ( happens(Event,Time)& initiates(Event,Fluent,Time)& less(n0,Offset)& trajectory(Fluent,Time,Fluent2,Offset)& ~ stoppedIn(Time,Fluent,plus(Time,Offset)) )=> holdsAt(Fluent2,plus(Time,Offset)) ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f8,axiom,(
% 12.43/2.69 (! [Fluent,Time] :( ( ~ releasedAt(Fluent,Time)& ~ (? [Event] :( happens(Event,Time)& releases(Event,Fluent,Time) ) ))=> ~ releasedAt(Fluent,plus(Time,n1)) ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f9,axiom,(
% 12.43/2.69 (! [Event,Time,Fluent] :( ( happens(Event,Time)& initiates(Event,Fluent,Time) )=> holdsAt(Fluent,plus(Time,n1)) ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f10,axiom,(
% 12.43/2.69 (! [Event,Time,Fluent] :( ( happens(Event,Time)& terminates(Event,Fluent,Time) )=> ~ holdsAt(Fluent,plus(Time,n1)) ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f11,axiom,(
% 12.43/2.69 (! [Event,Time,Fluent] :( ( happens(Event,Time)& releases(Event,Fluent,Time) )=> releasedAt(Fluent,plus(Time,n1)) ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f13,axiom,(
% 12.43/2.69 (! [Event,Fluent,Time] :( initiates(Event,Fluent,Time)<=> ( ( Event = tapOn& Fluent = filling )| ( Event = overflow& Fluent = spilling )| (? [Height] :( holdsAt(waterLevel(Height),Time)& Event = tapOff& Fluent = waterLevel(Height) ))| (? [Height] :( holdsAt(waterLevel(Height),Time)& Event = overflow& Fluent = waterLevel(Height) ) )) ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f15,axiom,(
% 12.43/2.69 (! [Event,Fluent,Time] :( releases(Event,Fluent,Time)<=> (? [Height] :( Event = tapOn& Fluent = waterLevel(Height) ) )) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f16,axiom,(
% 12.43/2.69 (! [Event,Time] :( happens(Event,Time)<=> ( ( Event = tapOn& Time = n0 )| ( holdsAt(waterLevel(n3),Time)& holdsAt(filling,Time)& Event = overflow ) ) ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f17,axiom,(
% 12.43/2.69 (! [Height1,Time,Height2,Offset] :( ( holdsAt(waterLevel(Height1),Time)& Height2 = plus(Height1,Offset) )=> trajectory(filling,Time,waterLevel(Height2),Offset) ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f18,axiom,(
% 12.43/2.69 (! [Time,Height1,Height2] :( ( holdsAt(waterLevel(Height1),Time)& holdsAt(waterLevel(Height2),Time) )=> Height1 = Height2 ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f27,axiom,(
% 12.43/2.69 plus(n0,n1) = n1 ),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f28,axiom,(
% 12.43/2.69 plus(n0,n2) = n2 ),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f37,axiom,(
% 12.43/2.69 (! [X,Y] :( less_or_equal(X,Y)<=> ( less(X,Y)| X = Y ) ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f38,axiom,(
% 12.43/2.69 ~ (? [X] : less(X,n0) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f39,axiom,(
% 12.43/2.69 (! [X] :( less(X,n1)<=> less_or_equal(X,n0) ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f40,axiom,(
% 12.43/2.69 (! [X] :( less(X,n2)<=> less_or_equal(X,n1) ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f41,axiom,(
% 12.43/2.69 (! [X] :( less(X,n3)<=> less_or_equal(X,n2) ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f48,axiom,(
% 12.43/2.69 (! [X,Y] :( less(X,Y)<=> ( ~ less(Y,X)& Y != X ) ) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f49,hypothesis,(
% 12.43/2.69 holdsAt(waterLevel(n0),n0) ),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f50,hypothesis,(
% 12.43/2.69 ~ holdsAt(filling,n0) ),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f52,hypothesis,(
% 12.43/2.69 (! [Height] : ~ releasedAt(waterLevel(Height),n0) )),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f55,conjecture,(
% 12.43/2.69 holdsAt(waterLevel(n2),n2) ),
% 12.43/2.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.43/2.69 fof(f56,negated_conjecture,(
% 12.43/2.69 ~(holdsAt(waterLevel(n2),n2) )),
% 12.43/2.69 inference(negated_conjecture,[status(cth)],[f55])).
% 12.43/2.69 fof(f57,plain,(
% 12.43/2.69 ![Time1,Fluent,Time2]: ((~stoppedIn(Time1,Fluent,Time2)|(?[Event,Time]: (((happens(Event,Time)&less(Time1,Time))&less(Time,Time2))&terminates(Event,Fluent,Time))))&(stoppedIn(Time1,Fluent,Time2)|(![Event,Time]: (((~happens(Event,Time)|~less(Time1,Time))|~less(Time,Time2))|~terminates(Event,Fluent,Time)))))),
% 12.43/2.69 inference(NNF_transformation,[status(thm)],[f1])).
% 12.43/2.69 fof(f58,plain,(
% 12.43/2.69 (![Time1,Fluent,Time2]: (~stoppedIn(Time1,Fluent,Time2)|(?[Event,Time]: (((happens(Event,Time)&less(Time1,Time))&less(Time,Time2))&terminates(Event,Fluent,Time)))))&(![Time1,Fluent,Time2]: (stoppedIn(Time1,Fluent,Time2)|(![Event,Time]: (((~happens(Event,Time)|~less(Time1,Time))|~less(Time,Time2))|~terminates(Event,Fluent,Time)))))),
% 12.43/2.69 inference(miniscoping,[status(thm)],[f57])).
% 12.43/2.69 fof(f59,plain,(
% 12.43/2.69 (![Time1,Fluent,Time2]: (~stoppedIn(Time1,Fluent,Time2)|(((happens(sK0_skl(Time2,Fluent,Time1),sK1_skl(Time2,Fluent,Time1))&less(Time1,sK1_skl(Time2,Fluent,Time1)))&less(sK1_skl(Time2,Fluent,Time1),Time2))&terminates(sK0_skl(Time2,Fluent,Time1),Fluent,sK1_skl(Time2,Fluent,Time1)))))&(![Time1,Fluent,Time2]: (stoppedIn(Time1,Fluent,Time2)|(![Event,Time]: (((~happens(Event,Time)|~less(Time1,Time))|~less(Time,Time2))|~terminates(Event,Fluent,Time)))))),
% 12.43/2.69 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])).
% 12.43/2.69 fof(f60,plain,(
% 12.43/2.69 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|happens(sK0_skl(X2,X1,X0),sK1_skl(X2,X1,X0)))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f59])).
% 12.43/2.69 fof(f61,plain,(
% 12.43/2.69 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|less(X0,sK1_skl(X2,X1,X0)))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f59])).
% 12.43/2.69 fof(f62,plain,(
% 12.43/2.69 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|less(sK1_skl(X2,X1,X0),X2))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f59])).
% 12.43/2.69 fof(f63,plain,(
% 12.43/2.69 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|terminates(sK0_skl(X2,X1,X0),X1,sK1_skl(X2,X1,X0)))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f59])).
% 12.43/2.69 fof(f73,plain,(
% 12.43/2.69 ![Event,Time,Fluent,Fluent2,Offset]: (((((~happens(Event,Time)|~initiates(Event,Fluent,Time))|~less(n0,Offset))|~trajectory(Fluent,Time,Fluent2,Offset))|stoppedIn(Time,Fluent,plus(Time,Offset)))|holdsAt(Fluent2,plus(Time,Offset)))),
% 12.43/2.69 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 12.43/2.69 fof(f74,plain,(
% 12.43/2.69 ![Time,Fluent2,Offset]: ((![Fluent]: ((((![Event]: (~happens(Event,Time)|~initiates(Event,Fluent,Time)))|~less(n0,Offset))|~trajectory(Fluent,Time,Fluent2,Offset))|stoppedIn(Time,Fluent,plus(Time,Offset))))|holdsAt(Fluent2,plus(Time,Offset)))),
% 12.43/2.69 inference(miniscoping,[status(thm)],[f73])).
% 12.43/2.69 fof(f75,plain,(
% 12.43/2.69 ![X0,X1,X2,X3,X4]: (~happens(X0,X1)|~initiates(X0,X2,X1)|~less(n0,X3)|~trajectory(X2,X1,X4,X3)|stoppedIn(X1,X2,plus(X1,X3))|holdsAt(X4,plus(X1,X3)))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f74])).
% 12.43/2.69 fof(f91,plain,(
% 12.43/2.69 ![Fluent,Time]: ((releasedAt(Fluent,Time)|(?[Event]: (happens(Event,Time)&releases(Event,Fluent,Time))))|~releasedAt(Fluent,plus(Time,n1)))),
% 12.43/2.69 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 12.43/2.69 fof(f92,plain,(
% 12.43/2.69 ![Fluent,Time]: ((releasedAt(Fluent,Time)|(happens(sK7_skl(Time,Fluent),Time)&releases(sK7_skl(Time,Fluent),Fluent,Time)))|~releasedAt(Fluent,plus(Time,n1)))),
% 12.43/2.69 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Event,sK7_skl(Time,Fluent))],[f91])).
% 12.43/2.69 fof(f93,plain,(
% 12.43/2.69 ![X0,X1]: (releasedAt(X0,X1)|happens(sK7_skl(X1,X0),X1)|~releasedAt(X0,plus(X1,n1)))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f92])).
% 12.43/2.69 fof(f95,plain,(
% 12.43/2.69 ![Event,Time,Fluent]: ((~happens(Event,Time)|~initiates(Event,Fluent,Time))|holdsAt(Fluent,plus(Time,n1)))),
% 12.43/2.69 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 12.43/2.69 fof(f96,plain,(
% 12.43/2.69 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~initiates(Event,Fluent,Time)))|holdsAt(Fluent,plus(Time,n1)))),
% 12.43/2.69 inference(miniscoping,[status(thm)],[f95])).
% 12.43/2.69 fof(f97,plain,(
% 12.43/2.69 ![X0,X1,X2]: (~happens(X0,X1)|~initiates(X0,X2,X1)|holdsAt(X2,plus(X1,n1)))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f96])).
% 12.43/2.69 fof(f98,plain,(
% 12.43/2.69 ![Event,Time,Fluent]: ((~happens(Event,Time)|~terminates(Event,Fluent,Time))|~holdsAt(Fluent,plus(Time,n1)))),
% 12.43/2.69 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 12.43/2.69 fof(f99,plain,(
% 12.43/2.69 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~terminates(Event,Fluent,Time)))|~holdsAt(Fluent,plus(Time,n1)))),
% 12.43/2.69 inference(miniscoping,[status(thm)],[f98])).
% 12.43/2.69 fof(f100,plain,(
% 12.43/2.69 ![X0,X1,X2]: (~happens(X0,X1)|~terminates(X0,X2,X1)|~holdsAt(X2,plus(X1,n1)))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f99])).
% 12.43/2.69 fof(f101,plain,(
% 12.43/2.69 ![Event,Time,Fluent]: ((~happens(Event,Time)|~releases(Event,Fluent,Time))|releasedAt(Fluent,plus(Time,n1)))),
% 12.43/2.69 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 12.43/2.69 fof(f102,plain,(
% 12.43/2.69 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~releases(Event,Fluent,Time)))|releasedAt(Fluent,plus(Time,n1)))),
% 12.43/2.69 inference(miniscoping,[status(thm)],[f101])).
% 12.43/2.69 fof(f103,plain,(
% 12.43/2.69 ![X0,X1,X2]: (~happens(X0,X1)|~releases(X0,X2,X1)|releasedAt(X2,plus(X1,n1)))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f102])).
% 12.43/2.69 fof(f108,definition,(
% 12.43/2.69 ![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)<=>(((Event=tapOn&Fluent=filling)|(Event=overflow&Fluent=spilling))|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=tapOff)&Fluent=waterLevel(Height)))))),
% 12.43/2.69 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 12.43/2.69 fof(f109,plain,(
% 12.43/2.69 ![Event,Fluent,Time]: (initiates(Event,Fluent,Time)<=>(sP0_prd(Time,Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=overflow)&Fluent=waterLevel(Height)))))),
% 12.43/2.69 inference(formula_renaming,[status(thm)],[f13,f108])).
% 12.43/2.69 fof(f110,plain,(
% 12.43/2.69 ![Event,Fluent,Time]: ((~initiates(Event,Fluent,Time)|(sP0_prd(Time,Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=overflow)&Fluent=waterLevel(Height)))))&(initiates(Event,Fluent,Time)|(~sP0_prd(Time,Fluent,Event)&(![Height]: ((~holdsAt(waterLevel(Height),Time)|~Event=overflow)|~Fluent=waterLevel(Height))))))),
% 12.43/2.69 inference(NNF_transformation,[status(thm)],[f109])).
% 12.43/2.69 fof(f111,plain,(
% 12.43/2.69 (![Event,Fluent,Time]: (~initiates(Event,Fluent,Time)|(sP0_prd(Time,Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=overflow)&Fluent=waterLevel(Height))))))&(![Event,Fluent,Time]: (initiates(Event,Fluent,Time)|(~sP0_prd(Time,Fluent,Event)&(![Height]: ((~holdsAt(waterLevel(Height),Time)|~Event=overflow)|~Fluent=waterLevel(Height))))))),
% 12.43/2.69 inference(miniscoping,[status(thm)],[f110])).
% 12.43/2.69 fof(f112,plain,(
% 12.43/2.69 (![Event,Fluent,Time]: (~initiates(Event,Fluent,Time)|(sP0_prd(Time,Fluent,Event)|((holdsAt(waterLevel(sK8_skl(Time,Fluent,Event)),Time)&Event=overflow)&Fluent=waterLevel(sK8_skl(Time,Fluent,Event))))))&(![Event,Fluent,Time]: (initiates(Event,Fluent,Time)|(~sP0_prd(Time,Fluent,Event)&(![Height]: ((~holdsAt(waterLevel(Height),Time)|~Event=overflow)|~Fluent=waterLevel(Height))))))),
% 12.43/2.69 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(Height,sK8_skl(Time,Fluent,Event))],[f111])).
% 12.43/2.69 fof(f116,plain,(
% 12.43/2.69 ![X0,X1,X2]: (initiates(X0,X1,X2)|~sP0_prd(X2,X1,X0))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f112])).
% 12.43/2.69 fof(f126,plain,(
% 12.43/2.69 ![Event,Fluent,Time]: ((~releases(Event,Fluent,Time)|(?[Height]: (Event=tapOn&Fluent=waterLevel(Height))))&(releases(Event,Fluent,Time)|(![Height]: (~Event=tapOn|~Fluent=waterLevel(Height)))))),
% 12.43/2.69 inference(NNF_transformation,[status(thm)],[f15])).
% 12.43/2.69 fof(f127,plain,(
% 12.43/2.69 (![Event,Fluent]: ((![Time]: ~releases(Event,Fluent,Time))|(Event=tapOn&(?[Height]: Fluent=waterLevel(Height)))))&(![Event,Fluent]: ((![Time]: releases(Event,Fluent,Time))|(~Event=tapOn|(![Height]: ~Fluent=waterLevel(Height)))))),
% 12.43/2.69 inference(miniscoping,[status(thm)],[f126])).
% 12.43/2.69 fof(f128,plain,(
% 12.43/2.69 (![Event,Fluent]: ((![Time]: ~releases(Event,Fluent,Time))|(Event=tapOn&Fluent=waterLevel(sK9_skl(Fluent,Event)))))&(![Event,Fluent]: ((![Time]: releases(Event,Fluent,Time))|(~Event=tapOn|(![Height]: ~Fluent=waterLevel(Height)))))),
% 12.43/2.69 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(Height,sK9_skl(Fluent,Event))],[f127])).
% 12.43/2.69 fof(f131,plain,(
% 12.43/2.69 ![X0,X1,X2,X3]: (releases(X0,X1,X2)|~X0=tapOn|~X1=waterLevel(X3))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f128])).
% 12.43/2.69 fof(f132,definition,(
% 12.43/2.69 ![Event,Time]: (sP1_prd(Time,Event)<=>(Event=tapOn&Time=n0))),
% 12.43/2.69 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 12.43/2.69 fof(f133,plain,(
% 12.43/2.69 ![Event,Time]: (happens(Event,Time)<=>(sP1_prd(Time,Event)|((holdsAt(waterLevel(n3),Time)&holdsAt(filling,Time))&Event=overflow)))),
% 12.43/2.69 inference(formula_renaming,[status(thm)],[f16,f132])).
% 12.43/2.69 fof(f134,plain,(
% 12.43/2.69 ![Event,Time]: ((~happens(Event,Time)|(sP1_prd(Time,Event)|((holdsAt(waterLevel(n3),Time)&holdsAt(filling,Time))&Event=overflow)))&(happens(Event,Time)|(~sP1_prd(Time,Event)&((~holdsAt(waterLevel(n3),Time)|~holdsAt(filling,Time))|~Event=overflow))))),
% 12.43/2.69 inference(NNF_transformation,[status(thm)],[f133])).
% 12.43/2.69 fof(f135,plain,(
% 12.43/2.69 (![Event,Time]: (~happens(Event,Time)|(sP1_prd(Time,Event)|((holdsAt(waterLevel(n3),Time)&holdsAt(filling,Time))&Event=overflow))))&(![Event,Time]: (happens(Event,Time)|(~sP1_prd(Time,Event)&((~holdsAt(waterLevel(n3),Time)|~holdsAt(filling,Time))|~Event=overflow))))),
% 12.43/2.69 inference(miniscoping,[status(thm)],[f134])).
% 12.43/2.69 fof(f136,plain,(
% 12.43/2.69 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|holdsAt(waterLevel(n3),X1))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f135])).
% 12.43/2.69 fof(f137,plain,(
% 12.43/2.69 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|holdsAt(filling,X1))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f135])).
% 12.43/2.69 fof(f138,plain,(
% 12.43/2.69 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|X0=overflow)),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f135])).
% 12.43/2.69 fof(f139,plain,(
% 12.43/2.69 ![X0,X1]: (happens(X0,X1)|~sP1_prd(X1,X0))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f135])).
% 12.43/2.69 fof(f141,plain,(
% 12.43/2.69 ![Height1,Time,Height2,Offset]: ((~holdsAt(waterLevel(Height1),Time)|~Height2=plus(Height1,Offset))|trajectory(filling,Time,waterLevel(Height2),Offset))),
% 12.43/2.69 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 12.43/2.69 fof(f142,plain,(
% 12.43/2.69 ![Time,Height2,Offset]: ((![Height1]: (~holdsAt(waterLevel(Height1),Time)|~Height2=plus(Height1,Offset)))|trajectory(filling,Time,waterLevel(Height2),Offset))),
% 12.43/2.69 inference(miniscoping,[status(thm)],[f141])).
% 12.43/2.69 fof(f143,plain,(
% 12.43/2.69 ![X0,X1,X2,X3]: (~holdsAt(waterLevel(X0),X1)|~X2=plus(X0,X3)|trajectory(filling,X1,waterLevel(X2),X3))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f142])).
% 12.43/2.69 fof(f144,plain,(
% 12.43/2.69 ![Time,Height1,Height2]: ((~holdsAt(waterLevel(Height1),Time)|~holdsAt(waterLevel(Height2),Time))|Height1=Height2)),
% 12.43/2.69 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 12.43/2.69 fof(f145,plain,(
% 12.43/2.69 ![Height1,Height2]: ((![Time]: (~holdsAt(waterLevel(Height1),Time)|~holdsAt(waterLevel(Height2),Time)))|Height1=Height2)),
% 12.43/2.69 inference(miniscoping,[status(thm)],[f144])).
% 12.43/2.69 fof(f146,plain,(
% 12.43/2.69 ![X0,X1,X2]: (~holdsAt(waterLevel(X0),X1)|~holdsAt(waterLevel(X2),X1)|X0=X2)),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f145])).
% 12.43/2.69 fof(f158,plain,(
% 12.43/2.69 plus(n0,n1)=n1),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f27])).
% 12.43/2.69 fof(f159,plain,(
% 12.43/2.69 plus(n0,n2)=n2),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f28])).
% 12.43/2.69 fof(f168,plain,(
% 12.43/2.69 ![X,Y]: ((~less_or_equal(X,Y)|(less(X,Y)|X=Y))&(less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 12.43/2.69 inference(NNF_transformation,[status(thm)],[f37])).
% 12.43/2.69 fof(f169,plain,(
% 12.43/2.69 (![X,Y]: (~less_or_equal(X,Y)|(less(X,Y)|X=Y)))&(![X,Y]: (less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 12.43/2.69 inference(miniscoping,[status(thm)],[f168])).
% 12.43/2.69 fof(f170,plain,(
% 12.43/2.69 ![X0,X1]: (~less_or_equal(X0,X1)|less(X0,X1)|X0=X1)),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f169])).
% 12.43/2.69 fof(f171,plain,(
% 12.43/2.69 ![X0,X1]: (less_or_equal(X0,X1)|~less(X0,X1))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f169])).
% 12.43/2.69 fof(f172,plain,(
% 12.43/2.69 ![X0,X1]: (less_or_equal(X0,X1)|~X0=X1)),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f169])).
% 12.43/2.69 fof(f173,plain,(
% 12.43/2.69 (![X]: ~less(X,n0))),
% 12.43/2.69 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 12.43/2.69 fof(f174,plain,(
% 12.43/2.69 ![X0]: (~less(X0,n0))),
% 12.43/2.69 inference(cnf_transformation,[status(thm)],[f173])).
% 12.43/2.70 fof(f175,plain,(
% 12.43/2.70 ![X]: ((~less(X,n1)|less_or_equal(X,n0))&(less(X,n1)|~less_or_equal(X,n0)))),
% 12.43/2.70 inference(NNF_transformation,[status(thm)],[f39])).
% 12.43/2.70 fof(f176,plain,(
% 12.43/2.70 (![X]: (~less(X,n1)|less_or_equal(X,n0)))&(![X]: (less(X,n1)|~less_or_equal(X,n0)))),
% 12.43/2.70 inference(miniscoping,[status(thm)],[f175])).
% 12.43/2.70 fof(f177,plain,(
% 12.43/2.70 ![X0]: (~less(X0,n1)|less_or_equal(X0,n0))),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f176])).
% 12.43/2.70 fof(f178,plain,(
% 12.43/2.70 ![X0]: (less(X0,n1)|~less_or_equal(X0,n0))),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f176])).
% 12.43/2.70 fof(f179,plain,(
% 12.43/2.70 ![X]: ((~less(X,n2)|less_or_equal(X,n1))&(less(X,n2)|~less_or_equal(X,n1)))),
% 12.43/2.70 inference(NNF_transformation,[status(thm)],[f40])).
% 12.43/2.70 fof(f180,plain,(
% 12.43/2.70 (![X]: (~less(X,n2)|less_or_equal(X,n1)))&(![X]: (less(X,n2)|~less_or_equal(X,n1)))),
% 12.43/2.70 inference(miniscoping,[status(thm)],[f179])).
% 12.43/2.70 fof(f181,plain,(
% 12.43/2.70 ![X0]: (~less(X0,n2)|less_or_equal(X0,n1))),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f180])).
% 12.43/2.70 fof(f182,plain,(
% 12.43/2.70 ![X0]: (less(X0,n2)|~less_or_equal(X0,n1))),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f180])).
% 12.43/2.70 fof(f183,plain,(
% 12.43/2.70 ![X]: ((~less(X,n3)|less_or_equal(X,n2))&(less(X,n3)|~less_or_equal(X,n2)))),
% 12.43/2.70 inference(NNF_transformation,[status(thm)],[f41])).
% 12.43/2.70 fof(f184,plain,(
% 12.43/2.70 (![X]: (~less(X,n3)|less_or_equal(X,n2)))&(![X]: (less(X,n3)|~less_or_equal(X,n2)))),
% 12.43/2.70 inference(miniscoping,[status(thm)],[f183])).
% 12.43/2.70 fof(f186,plain,(
% 12.43/2.70 ![X0]: (less(X0,n3)|~less_or_equal(X0,n2))),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f184])).
% 12.43/2.70 fof(f211,plain,(
% 12.43/2.70 ![X,Y]: ((~less(X,Y)|(~less(Y,X)&~Y=X))&(less(X,Y)|(less(Y,X)|Y=X)))),
% 12.43/2.70 inference(NNF_transformation,[status(thm)],[f48])).
% 12.43/2.70 fof(f212,plain,(
% 12.43/2.70 (![X,Y]: (~less(X,Y)|(~less(Y,X)&~Y=X)))&(![X,Y]: (less(X,Y)|(less(Y,X)|Y=X)))),
% 12.43/2.70 inference(miniscoping,[status(thm)],[f211])).
% 12.43/2.70 fof(f213,plain,(
% 12.43/2.70 ![X0,X1]: (~less(X0,X1)|~less(X1,X0))),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f212])).
% 12.43/2.70 fof(f214,plain,(
% 12.43/2.70 ![X0,X1]: (~less(X0,X1)|~X1=X0)),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f212])).
% 12.43/2.70 fof(f215,plain,(
% 12.43/2.70 ![X0,X1]: (less(X0,X1)|less(X1,X0)|X1=X0)),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f212])).
% 12.43/2.70 fof(f216,plain,(
% 12.43/2.70 holdsAt(waterLevel(n0),n0)),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f49])).
% 12.43/2.70 fof(f217,plain,(
% 12.43/2.70 ~holdsAt(filling,n0)),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f50])).
% 12.43/2.70 fof(f219,plain,(
% 12.43/2.70 ![X0]: (~releasedAt(waterLevel(X0),n0))),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f52])).
% 12.43/2.70 fof(f222,plain,(
% 12.43/2.70 ~holdsAt(waterLevel(n2),n2)),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f56])).
% 12.43/2.70 fof(f223,definition,(
% 12.43/2.70 ![Event,Fluent]: (sP2_prd(Fluent,Event)<=>((Event=tapOn&Fluent=filling)|(Event=overflow&Fluent=spilling)))),
% 12.43/2.70 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 12.43/2.70 fof(f224,plain,(
% 12.43/2.70 ![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)<=>(sP2_prd(Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=tapOff)&Fluent=waterLevel(Height)))))),
% 12.43/2.70 inference(formula_renaming,[status(thm)],[f108,f223])).
% 12.43/2.70 fof(f225,plain,(
% 12.43/2.70 ![Event,Fluent,Time]: ((~sP0_prd(Time,Fluent,Event)|(sP2_prd(Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=tapOff)&Fluent=waterLevel(Height)))))&(sP0_prd(Time,Fluent,Event)|(~sP2_prd(Fluent,Event)&(![Height]: ((~holdsAt(waterLevel(Height),Time)|~Event=tapOff)|~Fluent=waterLevel(Height))))))),
% 12.43/2.70 inference(NNF_transformation,[status(thm)],[f224])).
% 12.43/2.70 fof(f226,plain,(
% 12.43/2.70 (![Event,Fluent,Time]: (~sP0_prd(Time,Fluent,Event)|(sP2_prd(Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=tapOff)&Fluent=waterLevel(Height))))))&(![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)|(~sP2_prd(Fluent,Event)&(![Height]: ((~holdsAt(waterLevel(Height),Time)|~Event=tapOff)|~Fluent=waterLevel(Height))))))),
% 12.43/2.70 inference(miniscoping,[status(thm)],[f225])).
% 12.43/2.70 fof(f227,plain,(
% 12.43/2.70 (![Event,Fluent,Time]: (~sP0_prd(Time,Fluent,Event)|(sP2_prd(Fluent,Event)|((holdsAt(waterLevel(sK10_skl(Time,Fluent,Event)),Time)&Event=tapOff)&Fluent=waterLevel(sK10_skl(Time,Fluent,Event))))))&(![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)|(~sP2_prd(Fluent,Event)&(![Height]: ((~holdsAt(waterLevel(Height),Time)|~Event=tapOff)|~Fluent=waterLevel(Height))))))),
% 12.43/2.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(Height,sK10_skl(Time,Fluent,Event))],[f226])).
% 12.43/2.70 fof(f231,plain,(
% 12.43/2.70 ![X0,X1,X2]: (sP0_prd(X0,X1,X2)|~sP2_prd(X1,X2))),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f227])).
% 12.43/2.70 fof(f233,plain,(
% 12.43/2.70 ![Event,Time]: ((~sP1_prd(Time,Event)|(Event=tapOn&Time=n0))&(sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 12.43/2.70 inference(NNF_transformation,[status(thm)],[f132])).
% 12.43/2.70 fof(f234,plain,(
% 12.43/2.70 (![Event,Time]: (~sP1_prd(Time,Event)|(Event=tapOn&Time=n0)))&(![Event,Time]: (sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 12.43/2.70 inference(miniscoping,[status(thm)],[f233])).
% 12.43/2.70 fof(f235,plain,(
% 12.43/2.70 ![X0,X1]: (~sP1_prd(X0,X1)|X1=tapOn)),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f234])).
% 12.43/2.70 fof(f236,plain,(
% 12.43/2.70 ![X0,X1]: (~sP1_prd(X0,X1)|X0=n0)),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f234])).
% 12.43/2.70 fof(f237,plain,(
% 12.43/2.70 ![X0,X1]: (sP1_prd(X0,X1)|~X1=tapOn|~X0=n0)),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f234])).
% 12.43/2.70 fof(f238,plain,(
% 12.43/2.70 ![Event,Fluent]: ((~sP2_prd(Fluent,Event)|((Event=tapOn&Fluent=filling)|(Event=overflow&Fluent=spilling)))&(sP2_prd(Fluent,Event)|((~Event=tapOn|~Fluent=filling)&(~Event=overflow|~Fluent=spilling))))),
% 12.43/2.70 inference(NNF_transformation,[status(thm)],[f223])).
% 12.43/2.70 fof(f239,plain,(
% 12.43/2.70 (![Event,Fluent]: (~sP2_prd(Fluent,Event)|((Event=tapOn&Fluent=filling)|(Event=overflow&Fluent=spilling))))&(![Event,Fluent]: (sP2_prd(Fluent,Event)|((~Event=tapOn|~Fluent=filling)&(~Event=overflow|~Fluent=spilling))))),
% 12.43/2.70 inference(miniscoping,[status(thm)],[f238])).
% 12.43/2.70 fof(f244,plain,(
% 12.43/2.70 ![X0,X1]: (sP2_prd(X0,X1)|~X1=tapOn|~X0=filling)),
% 12.43/2.70 inference(cnf_transformation,[status(thm)],[f239])).
% 12.43/2.70 fof(f250,plain,(
% 12.43/2.70 ![X0,X1]: (releases(tapOn,waterLevel(X0),X1))),
% 12.43/2.70 inference(destructive_equality_resolution,[status(thm)],[f131])).
% 12.43/2.70 fof(f252,plain,(
% 12.43/2.70 ![X0,X1,X2]: (~holdsAt(waterLevel(X0),X1)|trajectory(filling,X1,waterLevel(plus(X0,X2)),X2))),
% 12.43/2.70 inference(destructive_equality_resolution,[status(thm)],[f143])).
% 12.43/2.70 fof(f253,plain,(
% 12.43/2.70 ![X0]: (less_or_equal(X0,X0))),
% 12.43/2.70 inference(destructive_equality_resolution,[status(thm)],[f172])).
% 12.43/2.70 fof(f254,plain,(
% 12.43/2.70 ![X0]: (~less(X0,X0))),
% 12.43/2.70 inference(destructive_equality_resolution,[status(thm)],[f214])).
% 12.43/2.70 fof(f256,plain,(
% 12.43/2.70 sP1_prd(n0,tapOn)),
% 12.43/2.70 inference(destructive_equality_resolution,[status(thm)],[f237])).
% 12.43/2.70 fof(f257,plain,(
% 12.43/2.70 sP2_prd(filling,tapOn)),
% 12.43/2.70 inference(destructive_equality_resolution,[status(thm)],[f244])).
% 12.43/2.70 fof(f262,plain,(
% 12.43/2.70 less(n1,n2)),
% 12.43/2.70 inference(resolution,[status(thm)],[f253,f182])).
% 12.43/2.70 fof(f272,plain,(
% 12.43/2.70 ![X0]: (~less(X0,n2)|less(X0,n3))),
% 12.43/2.70 inference(resolution,[status(thm)],[f171,f186])).
% 12.43/2.70 fof(f273,plain,(
% 12.43/2.70 ![X0]: (~less(X0,n1)|less(X0,n2))),
% 12.43/2.70 inference(resolution,[status(thm)],[f171,f182])).
% 12.43/2.70 fof(f279,plain,(
% 12.43/2.70 less(n1,n3)),
% 12.43/2.70 inference(resolution,[status(thm)],[f272,f262])).
% 12.43/2.70 fof(f289,plain,(
% 12.43/2.70 less(n0,n1)),
% 12.43/2.70 inference(resolution,[status(thm)],[f178,f253])).
% 12.43/2.70 fof(f291,plain,(
% 12.43/2.70 less(n0,n2)),
% 12.43/2.70 inference(resolution,[status(thm)],[f289,f273])).
% 12.43/2.70 fof(f306,plain,(
% 12.43/2.70 ![X0]: (less(n1,X0)|n1=X0|less_or_equal(X0,n0))),
% 12.43/2.70 inference(resolution,[status(thm)],[f215,f177])).
% 12.43/2.70 fof(f339,plain,(
% 12.43/2.70 ![X0,X1,X2]: (sP1_prd(sK1_skl(X0,X1,X2),sK0_skl(X0,X1,X2))|sK0_skl(X0,X1,X2)=overflow|~stoppedIn(X2,X1,X0))),
% 12.43/2.70 inference(resolution,[status(thm)],[f138,f60])).
% 12.43/2.70 fof(f341,plain,(
% 12.43/2.70 ![X0,X1,X2,X3]: (~terminates(sK0_skl(X0,X1,X2),X3,sK1_skl(X0,X1,X2))|~holdsAt(X3,plus(sK1_skl(X0,X1,X2),n1))|~stoppedIn(X2,X1,X0))),
% 12.43/2.70 inference(resolution,[status(thm)],[f100,f60])).
% 12.43/2.70 fof(f345,plain,(
% 12.43/2.70 ![X0]: (~happens(X0,n0)|sP1_prd(n0,X0))),
% 12.43/2.70 inference(resolution,[status(thm)],[f217,f137])).
% 12.43/2.70 fof(f883,plain,(
% 12.43/2.70 ![X0]: (releasedAt(X0,n0)|happens(sK7_skl(n0,X0),n0)|~releasedAt(X0,n1))),
% 12.43/2.70 inference(paramodulation,[status(thm)],[f158,f93])).
% 12.43/2.70 fof(f989,plain,(
% 12.43/2.70 ![X0,X1,X2]: (~initiates(X0,X1,X2)|holdsAt(X1,plus(X2,n1))|~sP1_prd(X2,X0))),
% 12.43/2.70 inference(resolution,[status(thm)],[f97,f139])).
% 12.43/2.70 fof(f991,plain,(
% 12.43/2.70 ![X0,X1,X2]: (~releases(X0,X1,X2)|releasedAt(X1,plus(X2,n1))|~sP1_prd(X2,X0))),
% 12.43/2.70 inference(resolution,[status(thm)],[f103,f139])).
% 12.43/2.70 fof(f1278,plain,(
% 12.43/2.70 ![X0]: (less(n1,X0)|n1=X0|less(X0,n0)|X0=n0)),
% 12.43/2.70 inference(resolution,[status(thm)],[f306,f170])).
% 12.43/2.70 fof(f1279,plain,(
% 12.43/2.70 ![X0]: (less(n1,X0)|n1=X0|X0=n0)),
% 12.43/2.70 inference(forward_subsumption_resolution,[status(thm)],[f1278,f174])).
% 12.43/2.70 fof(f1294,plain,(
% 12.43/2.70 ![X0]: (n1=X0|X0=n0|~less(X0,n1))),
% 12.43/2.70 inference(resolution,[status(thm)],[f1279,f213])).
% 12.43/2.70 fof(f1457,plain,(
% 12.43/2.70 ![X0]: (trajectory(filling,n0,waterLevel(plus(n0,X0)),X0))),
% 12.43/2.70 inference(resolution,[status(thm)],[f252,f216])).
% 12.43/2.70 fof(f1462,plain,(
% 12.43/2.70 trajectory(filling,n0,waterLevel(n1),n1)),
% 12.43/2.70 inference(paramodulation,[status(thm)],[f158,f1457])).
% 12.43/2.70 fof(f1464,plain,(
% 12.43/2.70 trajectory(filling,n0,waterLevel(n2),n2)),
% 12.43/2.70 inference(paramodulation,[status(thm)],[f159,f1457])).
% 12.43/2.70 fof(f1467,plain,(
% 12.43/2.70 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n2)|stoppedIn(n0,filling,plus(n0,n2))|holdsAt(waterLevel(n2),plus(n0,n2)))),
% 12.43/2.70 inference(resolution,[status(thm)],[f1464,f75])).
% 12.43/2.70 fof(f1468,plain,(
% 12.43/2.70 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n2)|stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),plus(n0,n2)))),
% 12.43/2.70 inference(forward_demodulation,[status(thm)],[f159,f1467])).
% 12.43/2.70 fof(f1469,plain,(
% 12.43/2.70 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n2)|stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2))),
% 12.43/2.70 inference(forward_demodulation,[status(thm)],[f159,f1468])).
% 12.43/2.70 fof(f1470,plain,(
% 12.43/2.70 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2))),
% 12.43/2.70 inference(forward_subsumption_resolution,[status(thm)],[f1469,f291])).
% 12.43/2.70 fof(f1471,plain,(
% 12.43/2.70 ![X0]: (~initiates(X0,filling,n0)|stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2)|~sP1_prd(n0,X0))),
% 12.43/2.70 inference(resolution,[status(thm)],[f1470,f139])).
% 12.43/2.70 fof(f1472,plain,(
% 12.43/2.70 ![X0]: (~initiates(X0,filling,n0)|stoppedIn(n0,filling,n2)|~sP1_prd(n0,X0))),
% 12.43/2.70 inference(forward_subsumption_resolution,[status(thm)],[f1471,f222])).
% 12.43/2.70 fof(f1473,plain,(
% 12.43/2.70 ~initiates(tapOn,filling,n0)|stoppedIn(n0,filling,n2)),
% 12.43/2.70 inference(resolution,[status(thm)],[f1472,f256])).
% 12.43/2.70 fof(f1474,plain,(
% 12.43/2.70 stoppedIn(n0,filling,n2)|~sP0_prd(n0,filling,tapOn)),
% 12.43/2.70 inference(resolution,[status(thm)],[f1473,f116])).
% 12.43/2.70 fof(f1475,plain,(
% 12.43/2.70 stoppedIn(n0,filling,n2)|~sP2_prd(filling,tapOn)),
% 12.43/2.70 inference(resolution,[status(thm)],[f1474,f231])).
% 12.43/2.70 fof(f1476,plain,(
% 12.43/2.70 stoppedIn(n0,filling,n2)),
% 12.43/2.70 inference(forward_subsumption_resolution,[status(thm)],[f1475,f257])).
% 12.43/2.70 fof(f1480,plain,(
% 12.43/2.70 sP1_prd(sK1_skl(n2,filling,n0),sK0_skl(n2,filling,n0))|sK0_skl(n2,filling,n0)=overflow),
% 12.43/2.70 inference(resolution,[status(thm)],[f1476,f339])).
% 12.43/2.70 fof(f1481,plain,(
% 12.43/2.70 terminates(sK0_skl(n2,filling,n0),filling,sK1_skl(n2,filling,n0))),
% 12.43/2.70 inference(resolution,[status(thm)],[f1476,f63])).
% 12.43/2.70 fof(f1482,plain,(
% 12.43/2.70 less(sK1_skl(n2,filling,n0),n2)),
% 12.43/2.70 inference(resolution,[status(thm)],[f1476,f62])).
% 12.43/2.70 fof(f1486,plain,(
% 12.43/2.70 less_or_equal(sK1_skl(n2,filling,n0),n1)),
% 12.43/2.70 inference(resolution,[status(thm)],[f1482,f181])).
% 12.43/2.70 fof(f1493,plain,(
% 12.43/2.70 less(sK1_skl(n2,filling,n0),n1)|sK1_skl(n2,filling,n0)=n1),
% 12.43/2.70 inference(resolution,[status(thm)],[f1486,f170])).
% 12.43/2.70 fof(f1500,plain,(
% 12.43/2.70 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n1)|stoppedIn(n0,filling,plus(n0,n1))|holdsAt(waterLevel(n1),plus(n0,n1)))),
% 12.43/2.70 inference(resolution,[status(thm)],[f1462,f75])).
% 12.43/2.70 fof(f1501,plain,(
% 12.43/2.70 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n1)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),plus(n0,n1)))),
% 12.43/2.70 inference(forward_demodulation,[status(thm)],[f158,f1500])).
% 12.43/2.70 fof(f1502,plain,(
% 12.43/2.70 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n1)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1))),
% 12.43/2.70 inference(forward_demodulation,[status(thm)],[f158,f1501])).
% 12.43/2.70 fof(f1503,plain,(
% 12.43/2.70 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1))),
% 12.43/2.70 inference(forward_subsumption_resolution,[status(thm)],[f1502,f289])).
% 12.43/2.70 fof(f1864,plain,(
% 12.43/2.70 ~holdsAt(filling,plus(sK1_skl(n2,filling,n0),n1))|~stoppedIn(n0,filling,n2)),
% 12.43/2.70 inference(resolution,[status(thm)],[f1481,f341])).
% 12.43/2.70 fof(f1869,plain,(
% 12.43/2.70 ~holdsAt(filling,plus(sK1_skl(n2,filling,n0),n1))),
% 12.43/2.70 inference(forward_subsumption_resolution,[status(thm)],[f1864,f1476])).
% 12.43/2.70 fof(f1891,plain,(
% 12.43/2.70 sK0_skl(n2,filling,n0)=overflow|sK1_skl(n2,filling,n0)=n0),
% 12.43/2.70 inference(resolution,[status(thm)],[f1480,f236])).
% 12.43/2.70 fof(f2150,plain,(
% 12.43/2.70 ~stoppedIn(n0,filling,n2)|less(n0,n0)|sK0_skl(n2,filling,n0)=overflow),
% 12.43/2.70 inference(paramodulation,[status(thm)],[f1891,f61])).
% 12.43/2.70 fof(f2159,plain,(
% 12.43/2.70 less(n0,n0)|sK0_skl(n2,filling,n0)=overflow),
% 12.43/2.70 inference(forward_subsumption_resolution,[status(thm)],[f2150,f1476])).
% 12.43/2.70 fof(f2162,plain,(
% 12.43/2.70 sK0_skl(n2,filling,n0)=overflow),
% 12.43/2.70 inference(resolution,[status(thm)],[f2159,f174])).
% 12.43/2.70 fof(f2202,plain,(
% 12.43/2.70 ~stoppedIn(n0,filling,n2)|happens(overflow,sK1_skl(n2,filling,n0))),
% 12.43/2.70 inference(paramodulation,[status(thm)],[f2162,f60])).
% 12.43/2.70 fof(f2207,plain,(
% 12.43/2.70 happens(overflow,sK1_skl(n2,filling,n0))),
% 12.43/2.70 inference(forward_subsumption_resolution,[status(thm)],[f2202,f1476])).
% 12.43/2.70 fof(f2210,plain,(
% 12.43/2.70 sP1_prd(sK1_skl(n2,filling,n0),overflow)|holdsAt(waterLevel(n3),sK1_skl(n2,filling,n0))),
% 12.43/2.70 inference(resolution,[status(thm)],[f2207,f136])).
% 12.43/2.70 fof(f2597,plain,(
% 12.43/2.70 ![X0]: (~initiates(tapOn,X0,n0)|holdsAt(X0,plus(n0,n1)))),
% 12.43/2.70 inference(resolution,[status(thm)],[f989,f256])).
% 12.43/2.70 fof(f2598,plain,(
% 12.43/2.70 ![X0]: (~initiates(tapOn,X0,n0)|holdsAt(X0,n1))),
% 12.43/2.70 inference(forward_demodulation,[status(thm)],[f158,f2597])).
% 12.43/2.70 fof(f2599,plain,(
% 12.43/2.70 ![X0]: (holdsAt(X0,n1)|~sP0_prd(n0,X0,tapOn))),
% 12.43/2.70 inference(resolution,[status(thm)],[f2598,f116])).
% 12.43/2.70 fof(f2600,plain,(
% 12.43/2.70 ![X0]: (holdsAt(X0,n1)|~sP2_prd(X0,tapOn))),
% 12.43/2.70 inference(resolution,[status(thm)],[f2599,f231])).
% 12.43/2.70 fof(f2601,plain,(
% 12.43/2.70 holdsAt(filling,n1)),
% 12.43/2.70 inference(resolution,[status(thm)],[f2600,f257])).
% 12.43/2.70 fof(f2605,plain,(
% 12.43/2.70 ![X0]: (~releases(tapOn,X0,n0)|releasedAt(X0,plus(n0,n1)))),
% 12.43/2.70 inference(resolution,[status(thm)],[f991,f256])).
% 12.43/2.70 fof(f2606,plain,(
% 12.43/2.70 ![X0]: (~releases(tapOn,X0,n0)|releasedAt(X0,n1))),
% 12.43/2.70 inference(forward_demodulation,[status(thm)],[f158,f2605])).
% 12.43/2.70 fof(f2607,plain,(
% 12.43/2.70 ![X0]: (releasedAt(waterLevel(X0),n1))),
% 12.43/2.70 inference(resolution,[status(thm)],[f2606,f250])).
% 12.43/2.70 fof(f2608,plain,(
% 12.43/2.70 ![X0]: (releasedAt(waterLevel(X0),n0)|happens(sK7_skl(n0,waterLevel(X0)),n0))),
% 12.43/2.70 inference(resolution,[status(thm)],[f2607,f883])).
% 12.43/2.70 fof(f2611,plain,(
% 12.43/2.70 ![X0]: (happens(sK7_skl(n0,waterLevel(X0)),n0))),
% 12.43/2.70 inference(forward_subsumption_resolution,[status(thm)],[f2608,f219])).
% 12.43/2.70 fof(f2618,plain,(
% 12.43/2.70 sK1_skl(n2,filling,n0)=n1|n1=sK1_skl(n2,filling,n0)|sK1_skl(n2,filling,n0)=n0),
% 12.43/2.70 inference(resolution,[status(thm)],[f1493,f1294])).
% 12.43/2.70 fof(f2623,plain,(
% 12.43/2.70 sK1_skl(n2,filling,n0)=n1|sK1_skl(n2,filling,n0)=n0),
% 12.43/2.70 inference(duplicate_literals_removal,[status(thm)],[f2618])).
% 12.43/2.70 fof(f2993,plain,(
% 12.43/2.70 ![X0]: (sP1_prd(n0,sK7_skl(n0,waterLevel(X0))))),
% 12.43/2.70 inference(resolution,[status(thm)],[f2611,f345])).
% 12.43/2.70 fof(f3015,plain,(
% 12.43/2.70 ![X0]: (sK7_skl(n0,waterLevel(X0))=tapOn)),
% 12.43/2.70 inference(resolution,[status(thm)],[f2993,f235])).
% 12.43/2.70 fof(f3020,plain,(
% 12.43/2.70 happens(tapOn,n0)),
% 12.43/2.70 inference(backward_demodulation,[status(thm)],[f3015,f2611])).
% 12.43/2.70 fof(f4672,plain,(
% 12.43/2.70 sP1_prd(sK1_skl(n2,filling,n0),overflow)|holdsAt(waterLevel(n3),n1)|sK1_skl(n2,filling,n0)=n0),
% 12.43/2.70 inference(paramodulation,[status(thm)],[f2623,f2210])).
% 12.43/2.70 fof(f4674,plain,(
% 12.43/2.70 holdsAt(waterLevel(n3),n1)|sK1_skl(n2,filling,n0)=n0),
% 12.43/2.70 inference(forward_subsumption_resolution,[status(thm)],[f4672,f236])).
% 12.43/2.70 fof(f4679,plain,(
% 12.43/2.70 ![X0]: (sK1_skl(n2,filling,n0)=n0|~holdsAt(waterLevel(X0),n1)|X0=n3)),
% 12.43/2.70 inference(resolution,[status(thm)],[f4674,f146])).
% 12.43/2.70 fof(f8334,plain,(
% 12.43/2.70 ~initiates(tapOn,filling,n0)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)),
% 12.43/2.70 inference(resolution,[status(thm)],[f1503,f3020])).
% 12.43/2.70 fof(f8337,plain,(
% 12.43/2.70 stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)|~sP0_prd(n0,filling,tapOn)),
% 12.43/2.70 inference(resolution,[status(thm)],[f8334,f116])).
% 12.43/2.70 fof(f8355,plain,(
% 12.43/2.70 stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)|~sP2_prd(filling,tapOn)),
% 12.43/2.70 inference(resolution,[status(thm)],[f8337,f231])).
% 12.43/2.70 fof(f8356,plain,(
% 12.43/2.70 stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)),
% 12.43/2.70 inference(forward_subsumption_resolution,[status(thm)],[f8355,f257])).
% 12.43/2.71 fof(f8357,plain,(
% 12.43/2.71 stoppedIn(n0,filling,n1)|sK1_skl(n2,filling,n0)=n0|n1=n3),
% 12.43/2.71 inference(resolution,[status(thm)],[f8356,f4679])).
% 12.43/2.71 fof(f8389,plain,(
% 12.43/2.71 sK1_skl(n2,filling,n0)=n0|n1=n3|less(sK1_skl(n1,filling,n0),n1)),
% 12.43/2.71 inference(resolution,[status(thm)],[f8357,f62])).
% 12.43/2.71 fof(f8421,plain,(
% 12.43/2.71 sK1_skl(n2,filling,n0)=n0|n1=n3|less_or_equal(sK1_skl(n1,filling,n0),n0)),
% 12.43/2.71 inference(resolution,[status(thm)],[f8389,f177])).
% 12.43/2.71 fof(f8425,plain,(
% 12.43/2.71 sK1_skl(n2,filling,n0)=n0|n1=n3|less(sK1_skl(n1,filling,n0),n0)|sK1_skl(n1,filling,n0)=n0),
% 12.43/2.71 inference(resolution,[status(thm)],[f8421,f170])).
% 12.43/2.71 fof(f8426,plain,(
% 12.43/2.71 sK1_skl(n2,filling,n0)=n0|n1=n3|sK1_skl(n1,filling,n0)=n0),
% 12.43/2.71 inference(forward_subsumption_resolution,[status(thm)],[f8425,f174])).
% 12.43/2.71 fof(f8451,plain,(
% 12.43/2.71 ~holdsAt(filling,plus(n0,n1))|n1=n3|sK1_skl(n1,filling,n0)=n0),
% 12.43/2.71 inference(paramodulation,[status(thm)],[f8426,f1869])).
% 12.43/2.71 fof(f8467,plain,(
% 12.43/2.71 ~holdsAt(filling,n1)|n1=n3|sK1_skl(n1,filling,n0)=n0),
% 12.43/2.71 inference(forward_demodulation,[status(thm)],[f158,f8451])).
% 12.43/2.71 fof(f8468,plain,(
% 12.43/2.71 n1=n3|sK1_skl(n1,filling,n0)=n0),
% 12.43/2.71 inference(forward_subsumption_resolution,[status(thm)],[f8467,f2601])).
% 12.43/2.71 fof(f8481,plain,(
% 12.43/2.71 ~stoppedIn(n0,filling,n1)|less(n0,n0)|n1=n3),
% 12.43/2.71 inference(paramodulation,[status(thm)],[f8468,f61])).
% 12.43/2.71 fof(f8485,plain,(
% 12.43/2.71 sK1_skl(n2,filling,n0)=n0|n1=n3),
% 12.43/2.71 inference(backward_subsumption_resolution,[status(thm)],[f8357,f8486])).
% 12.43/2.71 fof(f8486,plain,(
% 12.43/2.71 ~stoppedIn(n0,filling,n1)|n1=n3),
% 12.43/2.71 inference(forward_subsumption_resolution,[status(thm)],[f8481,f174])).
% 12.43/2.71 fof(f8516,plain,(
% 12.43/2.71 ~holdsAt(filling,plus(n0,n1))|n1=n3),
% 12.43/2.71 inference(paramodulation,[status(thm)],[f8485,f1869])).
% 12.43/2.71 fof(f8532,plain,(
% 12.43/2.71 ~holdsAt(filling,n1)|n1=n3),
% 12.43/2.71 inference(forward_demodulation,[status(thm)],[f158,f8516])).
% 12.43/2.71 fof(f8678,plain,(
% 12.43/2.71 less(n1,n1)),
% 12.43/2.71 inference(backward_demodulation,[status(thm)],[f8799,f279])).
% 12.43/2.71 fof(f8799,plain,(
% 12.43/2.71 n1=n3),
% 12.43/2.71 inference(forward_subsumption_resolution,[status(thm)],[f8532,f2601])).
% 12.43/2.71 fof(f9085,plain,(
% 12.43/2.71 $false),
% 12.43/2.71 inference(forward_subsumption_resolution,[status(thm)],[f8678,f254])).
% 12.43/2.71 % SZS output end CNFRefutation for theBenchmark.p
% 3.45/2.73 % Elapsed time: 1.705960 seconds
% 3.45/2.73 % CPU time: 13.241765 seconds
% 3.45/2.73 % Total memory used: 191.977 MB
% 3.45/2.73 % Net memory used: 183.241 MB
%------------------------------------------------------------------------------