%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR006+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 : n006.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 32.21s 4.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR006+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n006.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 14:23:27 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.14/0.39 % Drodi V4.1.1
% 32.21/4.67 % Refutation found
% 32.21/4.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 32.21/4.67 % SZS output start CNFRefutation for theBenchmark
% 32.21/4.67 fof(f1,axiom,(
% 32.21/4.67 (! [Time1,Fluent,Time2] :( stoppedIn(Time1,Fluent,Time2)<=> (? [Event,Time] :( happens(Event,Time)& less(Time1,Time)& less(Time,Time2)& terminates(Event,Fluent,Time) ) )) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f3,axiom,(
% 32.21/4.67 (! [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)) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f5,axiom,(
% 32.21/4.67 (! [Fluent,Time] :( ( holdsAt(Fluent,Time)& ~ releasedAt(Fluent,plus(Time,n1))& ~ (? [Event] :( happens(Event,Time)& terminates(Event,Fluent,Time) ) ))=> holdsAt(Fluent,plus(Time,n1)) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f8,axiom,(
% 32.21/4.67 (! [Fluent,Time] :( ( ~ releasedAt(Fluent,Time)& ~ (? [Event] :( happens(Event,Time)& releases(Event,Fluent,Time) ) ))=> ~ releasedAt(Fluent,plus(Time,n1)) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f9,axiom,(
% 32.21/4.67 (! [Event,Time,Fluent] :( ( happens(Event,Time)& initiates(Event,Fluent,Time) )=> holdsAt(Fluent,plus(Time,n1)) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f10,axiom,(
% 32.21/4.67 (! [Event,Time,Fluent] :( ( happens(Event,Time)& terminates(Event,Fluent,Time) )=> ~ holdsAt(Fluent,plus(Time,n1)) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f11,axiom,(
% 32.21/4.67 (! [Event,Time,Fluent] :( ( happens(Event,Time)& releases(Event,Fluent,Time) )=> releasedAt(Fluent,plus(Time,n1)) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f12,axiom,(
% 32.21/4.67 (! [Event,Time,Fluent] :( ( happens(Event,Time)& ( initiates(Event,Fluent,Time)| terminates(Event,Fluent,Time) ) )=> ~ releasedAt(Fluent,plus(Time,n1)) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f13,axiom,(
% 32.21/4.67 (! [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) ) )) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f14,axiom,(
% 32.21/4.67 (! [Event,Fluent,Time] :( terminates(Event,Fluent,Time)<=> ( ( Event = tapOff& Fluent = filling )| ( Event = overflow& Fluent = filling ) ) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f15,axiom,(
% 32.21/4.67 (! [Event,Fluent,Time] :( releases(Event,Fluent,Time)<=> (? [Height] :( Event = tapOn& Fluent = waterLevel(Height) ) )) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f16,axiom,(
% 32.21/4.67 (! [Event,Time] :( happens(Event,Time)<=> ( ( Event = tapOn& Time = n0 )| ( holdsAt(waterLevel(n3),Time)& holdsAt(filling,Time)& Event = overflow ) ) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f17,axiom,(
% 32.21/4.67 (! [Height1,Time,Height2,Offset] :( ( holdsAt(waterLevel(Height1),Time)& Height2 = plus(Height1,Offset) )=> trajectory(filling,Time,waterLevel(Height2),Offset) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f19,axiom,(
% 32.21/4.67 tapOff != tapOn ),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f20,axiom,(
% 32.21/4.67 tapOff != overflow ),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f21,axiom,(
% 32.21/4.67 overflow != tapOn ),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f22,axiom,(
% 32.21/4.67 (! [X] : filling != waterLevel(X) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f27,axiom,(
% 32.21/4.67 plus(n0,n1) = n1 ),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f29,axiom,(
% 32.21/4.67 plus(n0,n3) = n3 ),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f30,axiom,(
% 32.21/4.67 plus(n1,n1) = n2 ),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f31,axiom,(
% 32.21/4.67 plus(n1,n2) = n3 ),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f36,axiom,(
% 32.21/4.67 (! [X,Y] : plus(X,Y) = plus(Y,X) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f37,axiom,(
% 32.21/4.67 (! [X,Y] :( less_or_equal(X,Y)<=> ( less(X,Y)| X = Y ) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f38,axiom,(
% 32.21/4.67 ~ (? [X] : less(X,n0) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f39,axiom,(
% 32.21/4.67 (! [X] :( less(X,n1)<=> less_or_equal(X,n0) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f40,axiom,(
% 32.21/4.67 (! [X] :( less(X,n2)<=> less_or_equal(X,n1) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f41,axiom,(
% 32.21/4.67 (! [X] :( less(X,n3)<=> less_or_equal(X,n2) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f48,axiom,(
% 32.21/4.67 (! [X,Y] :( less(X,Y)<=> ( ~ less(Y,X)& Y != X ) ) )),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f49,hypothesis,(
% 32.21/4.67 holdsAt(waterLevel(n0),n0) ),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f55,conjecture,(
% 32.21/4.67 holdsAt(waterLevel(n3),n3) ),
% 32.21/4.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.21/4.67 fof(f56,negated_conjecture,(
% 32.21/4.67 ~(holdsAt(waterLevel(n3),n3) )),
% 32.21/4.67 inference(negated_conjecture,[status(cth)],[f55])).
% 32.21/4.67 fof(f57,plain,(
% 32.21/4.67 ![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)))))),
% 32.21/4.67 inference(NNF_transformation,[status(thm)],[f1])).
% 32.21/4.67 fof(f58,plain,(
% 32.21/4.67 (![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)))))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f57])).
% 32.21/4.67 fof(f59,plain,(
% 32.21/4.67 (![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)))))),
% 32.21/4.67 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])).
% 32.21/4.67 fof(f60,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|happens(sK0_skl(X2,X1,X0),sK1_skl(X2,X1,X0)))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f59])).
% 32.21/4.67 fof(f62,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|less(sK1_skl(X2,X1,X0),X2))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f59])).
% 32.21/4.67 fof(f63,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|terminates(sK0_skl(X2,X1,X0),X1,sK1_skl(X2,X1,X0)))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f59])).
% 32.21/4.67 fof(f73,plain,(
% 32.21/4.67 ![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)))),
% 32.21/4.67 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 32.21/4.67 fof(f74,plain,(
% 32.21/4.67 ![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)))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f73])).
% 32.21/4.67 fof(f75,plain,(
% 32.21/4.67 ![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)))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f74])).
% 32.21/4.67 fof(f79,plain,(
% 32.21/4.67 ![Fluent,Time]: (((~holdsAt(Fluent,Time)|releasedAt(Fluent,plus(Time,n1)))|(?[Event]: (happens(Event,Time)&terminates(Event,Fluent,Time))))|holdsAt(Fluent,plus(Time,n1)))),
% 32.21/4.67 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 32.21/4.67 fof(f80,plain,(
% 32.21/4.67 ![Fluent,Time]: (((~holdsAt(Fluent,Time)|releasedAt(Fluent,plus(Time,n1)))|(happens(sK4_skl(Time,Fluent),Time)&terminates(sK4_skl(Time,Fluent),Fluent,Time)))|holdsAt(Fluent,plus(Time,n1)))),
% 32.21/4.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(Event,sK4_skl(Time,Fluent))],[f79])).
% 32.21/4.67 fof(f82,plain,(
% 32.21/4.67 ![X0,X1]: (~holdsAt(X0,X1)|releasedAt(X0,plus(X1,n1))|terminates(sK4_skl(X1,X0),X0,X1)|holdsAt(X0,plus(X1,n1)))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f80])).
% 32.21/4.67 fof(f91,plain,(
% 32.21/4.67 ![Fluent,Time]: ((releasedAt(Fluent,Time)|(?[Event]: (happens(Event,Time)&releases(Event,Fluent,Time))))|~releasedAt(Fluent,plus(Time,n1)))),
% 32.21/4.67 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 32.21/4.67 fof(f92,plain,(
% 32.21/4.67 ![Fluent,Time]: ((releasedAt(Fluent,Time)|(happens(sK7_skl(Time,Fluent),Time)&releases(sK7_skl(Time,Fluent),Fluent,Time)))|~releasedAt(Fluent,plus(Time,n1)))),
% 32.21/4.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Event,sK7_skl(Time,Fluent))],[f91])).
% 32.21/4.67 fof(f93,plain,(
% 32.21/4.67 ![X0,X1]: (releasedAt(X0,X1)|happens(sK7_skl(X1,X0),X1)|~releasedAt(X0,plus(X1,n1)))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f92])).
% 32.21/4.67 fof(f94,plain,(
% 32.21/4.67 ![X0,X1]: (releasedAt(X0,X1)|releases(sK7_skl(X1,X0),X0,X1)|~releasedAt(X0,plus(X1,n1)))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f92])).
% 32.21/4.67 fof(f95,plain,(
% 32.21/4.67 ![Event,Time,Fluent]: ((~happens(Event,Time)|~initiates(Event,Fluent,Time))|holdsAt(Fluent,plus(Time,n1)))),
% 32.21/4.67 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 32.21/4.67 fof(f96,plain,(
% 32.21/4.67 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~initiates(Event,Fluent,Time)))|holdsAt(Fluent,plus(Time,n1)))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f95])).
% 32.21/4.67 fof(f97,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~happens(X0,X1)|~initiates(X0,X2,X1)|holdsAt(X2,plus(X1,n1)))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f96])).
% 32.21/4.67 fof(f98,plain,(
% 32.21/4.67 ![Event,Time,Fluent]: ((~happens(Event,Time)|~terminates(Event,Fluent,Time))|~holdsAt(Fluent,plus(Time,n1)))),
% 32.21/4.67 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 32.21/4.67 fof(f99,plain,(
% 32.21/4.67 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~terminates(Event,Fluent,Time)))|~holdsAt(Fluent,plus(Time,n1)))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f98])).
% 32.21/4.67 fof(f100,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~happens(X0,X1)|~terminates(X0,X2,X1)|~holdsAt(X2,plus(X1,n1)))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f99])).
% 32.21/4.67 fof(f101,plain,(
% 32.21/4.67 ![Event,Time,Fluent]: ((~happens(Event,Time)|~releases(Event,Fluent,Time))|releasedAt(Fluent,plus(Time,n1)))),
% 32.21/4.67 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 32.21/4.67 fof(f102,plain,(
% 32.21/4.67 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~releases(Event,Fluent,Time)))|releasedAt(Fluent,plus(Time,n1)))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f101])).
% 32.21/4.67 fof(f103,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~happens(X0,X1)|~releases(X0,X2,X1)|releasedAt(X2,plus(X1,n1)))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f102])).
% 32.21/4.67 fof(f104,plain,(
% 32.21/4.67 ![Event,Time,Fluent]: ((~happens(Event,Time)|(~initiates(Event,Fluent,Time)&~terminates(Event,Fluent,Time)))|~releasedAt(Fluent,plus(Time,n1)))),
% 32.21/4.67 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 32.21/4.67 fof(f105,plain,(
% 32.21/4.67 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|(~initiates(Event,Fluent,Time)&~terminates(Event,Fluent,Time))))|~releasedAt(Fluent,plus(Time,n1)))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f104])).
% 32.21/4.67 fof(f106,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~happens(X0,X1)|~initiates(X0,X2,X1)|~releasedAt(X2,plus(X1,n1)))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f105])).
% 32.21/4.67 fof(f108,definition,(
% 32.21/4.67 ![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)))))),
% 32.21/4.67 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 32.21/4.67 fof(f109,plain,(
% 32.21/4.67 ![Event,Fluent,Time]: (initiates(Event,Fluent,Time)<=>(sP0_prd(Time,Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=overflow)&Fluent=waterLevel(Height)))))),
% 32.21/4.67 inference(formula_renaming,[status(thm)],[f13,f108])).
% 32.21/4.67 fof(f110,plain,(
% 32.21/4.67 ![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))))))),
% 32.21/4.67 inference(NNF_transformation,[status(thm)],[f109])).
% 32.21/4.67 fof(f111,plain,(
% 32.21/4.67 (![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))))))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f110])).
% 32.21/4.67 fof(f112,plain,(
% 32.21/4.67 (![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))))))),
% 32.21/4.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(Height,sK8_skl(Time,Fluent,Event))],[f111])).
% 32.21/4.67 fof(f116,plain,(
% 32.21/4.67 ![X0,X1,X2]: (initiates(X0,X1,X2)|~sP0_prd(X2,X1,X0))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f112])).
% 32.21/4.67 fof(f117,plain,(
% 32.21/4.67 ![X0,X1,X2,X3]: (initiates(X0,X1,X2)|~holdsAt(waterLevel(X3),X2)|~X0=overflow|~X1=waterLevel(X3))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f112])).
% 32.21/4.67 fof(f118,plain,(
% 32.21/4.67 ![Event,Fluent,Time]: ((~terminates(Event,Fluent,Time)|((Event=tapOff&Fluent=filling)|(Event=overflow&Fluent=filling)))&(terminates(Event,Fluent,Time)|((~Event=tapOff|~Fluent=filling)&(~Event=overflow|~Fluent=filling))))),
% 32.21/4.67 inference(NNF_transformation,[status(thm)],[f14])).
% 32.21/4.67 fof(f119,plain,(
% 32.21/4.67 (![Event,Fluent]: ((![Time]: ~terminates(Event,Fluent,Time))|((Event=tapOff&Fluent=filling)|(Event=overflow&Fluent=filling))))&(![Event,Fluent]: ((![Time]: terminates(Event,Fluent,Time))|((~Event=tapOff|~Fluent=filling)&(~Event=overflow|~Fluent=filling))))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f118])).
% 32.21/4.67 fof(f120,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~terminates(X0,X1,X2)|X0=tapOff|X0=overflow)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f119])).
% 32.21/4.67 fof(f123,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~terminates(X0,X1,X2)|X1=filling|X1=filling)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f119])).
% 32.21/4.67 fof(f126,plain,(
% 32.21/4.67 ![Event,Fluent,Time]: ((~releases(Event,Fluent,Time)|(?[Height]: (Event=tapOn&Fluent=waterLevel(Height))))&(releases(Event,Fluent,Time)|(![Height]: (~Event=tapOn|~Fluent=waterLevel(Height)))))),
% 32.21/4.67 inference(NNF_transformation,[status(thm)],[f15])).
% 32.21/4.67 fof(f127,plain,(
% 32.21/4.67 (![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)))))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f126])).
% 32.21/4.67 fof(f128,plain,(
% 32.21/4.67 (![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)))))),
% 32.21/4.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(Height,sK9_skl(Fluent,Event))],[f127])).
% 32.21/4.67 fof(f129,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~releases(X0,X1,X2)|X0=tapOn)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f128])).
% 32.21/4.67 fof(f131,plain,(
% 32.21/4.67 ![X0,X1,X2,X3]: (releases(X0,X1,X2)|~X0=tapOn|~X1=waterLevel(X3))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f128])).
% 32.21/4.67 fof(f132,definition,(
% 32.21/4.67 ![Event,Time]: (sP1_prd(Time,Event)<=>(Event=tapOn&Time=n0))),
% 32.21/4.67 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 32.21/4.67 fof(f133,plain,(
% 32.21/4.67 ![Event,Time]: (happens(Event,Time)<=>(sP1_prd(Time,Event)|((holdsAt(waterLevel(n3),Time)&holdsAt(filling,Time))&Event=overflow)))),
% 32.21/4.67 inference(formula_renaming,[status(thm)],[f16,f132])).
% 32.21/4.67 fof(f134,plain,(
% 32.21/4.67 ![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))))),
% 32.21/4.67 inference(NNF_transformation,[status(thm)],[f133])).
% 32.21/4.67 fof(f135,plain,(
% 32.21/4.67 (![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))))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f134])).
% 32.21/4.67 fof(f136,plain,(
% 32.21/4.67 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|holdsAt(waterLevel(n3),X1))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f135])).
% 32.21/4.67 fof(f138,plain,(
% 32.21/4.67 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|X0=overflow)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f135])).
% 32.21/4.67 fof(f139,plain,(
% 32.21/4.67 ![X0,X1]: (happens(X0,X1)|~sP1_prd(X1,X0))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f135])).
% 32.21/4.67 fof(f141,plain,(
% 32.21/4.67 ![Height1,Time,Height2,Offset]: ((~holdsAt(waterLevel(Height1),Time)|~Height2=plus(Height1,Offset))|trajectory(filling,Time,waterLevel(Height2),Offset))),
% 32.21/4.67 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 32.21/4.67 fof(f142,plain,(
% 32.21/4.67 ![Time,Height2,Offset]: ((![Height1]: (~holdsAt(waterLevel(Height1),Time)|~Height2=plus(Height1,Offset)))|trajectory(filling,Time,waterLevel(Height2),Offset))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f141])).
% 32.21/4.67 fof(f143,plain,(
% 32.21/4.67 ![X0,X1,X2,X3]: (~holdsAt(waterLevel(X0),X1)|~X2=plus(X0,X3)|trajectory(filling,X1,waterLevel(X2),X3))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f142])).
% 32.21/4.67 fof(f147,plain,(
% 32.21/4.67 ~tapOff=tapOn),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f19])).
% 32.21/4.67 fof(f148,plain,(
% 32.21/4.67 ~tapOff=overflow),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f20])).
% 32.21/4.67 fof(f149,plain,(
% 32.21/4.67 ~overflow=tapOn),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f21])).
% 32.21/4.67 fof(f150,plain,(
% 32.21/4.67 ![X0]: (~filling=waterLevel(X0))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f22])).
% 32.21/4.67 fof(f158,plain,(
% 32.21/4.67 plus(n0,n1)=n1),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f27])).
% 32.21/4.67 fof(f160,plain,(
% 32.21/4.67 plus(n0,n3)=n3),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f29])).
% 32.21/4.67 fof(f161,plain,(
% 32.21/4.67 plus(n1,n1)=n2),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f30])).
% 32.21/4.67 fof(f162,plain,(
% 32.21/4.67 plus(n1,n2)=n3),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f31])).
% 32.21/4.67 fof(f167,plain,(
% 32.21/4.67 ![X0,X1]: (plus(X0,X1)=plus(X1,X0))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f36])).
% 32.21/4.67 fof(f168,plain,(
% 32.21/4.67 ![X,Y]: ((~less_or_equal(X,Y)|(less(X,Y)|X=Y))&(less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 32.21/4.67 inference(NNF_transformation,[status(thm)],[f37])).
% 32.21/4.67 fof(f169,plain,(
% 32.21/4.67 (![X,Y]: (~less_or_equal(X,Y)|(less(X,Y)|X=Y)))&(![X,Y]: (less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f168])).
% 32.21/4.67 fof(f170,plain,(
% 32.21/4.67 ![X0,X1]: (~less_or_equal(X0,X1)|less(X0,X1)|X0=X1)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f169])).
% 32.21/4.67 fof(f171,plain,(
% 32.21/4.67 ![X0,X1]: (less_or_equal(X0,X1)|~less(X0,X1))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f169])).
% 32.21/4.67 fof(f172,plain,(
% 32.21/4.67 ![X0,X1]: (less_or_equal(X0,X1)|~X0=X1)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f169])).
% 32.21/4.67 fof(f173,plain,(
% 32.21/4.67 (![X]: ~less(X,n0))),
% 32.21/4.67 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 32.21/4.67 fof(f174,plain,(
% 32.21/4.67 ![X0]: (~less(X0,n0))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f173])).
% 32.21/4.67 fof(f175,plain,(
% 32.21/4.67 ![X]: ((~less(X,n1)|less_or_equal(X,n0))&(less(X,n1)|~less_or_equal(X,n0)))),
% 32.21/4.67 inference(NNF_transformation,[status(thm)],[f39])).
% 32.21/4.67 fof(f176,plain,(
% 32.21/4.67 (![X]: (~less(X,n1)|less_or_equal(X,n0)))&(![X]: (less(X,n1)|~less_or_equal(X,n0)))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f175])).
% 32.21/4.67 fof(f177,plain,(
% 32.21/4.67 ![X0]: (~less(X0,n1)|less_or_equal(X0,n0))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f176])).
% 32.21/4.67 fof(f178,plain,(
% 32.21/4.67 ![X0]: (less(X0,n1)|~less_or_equal(X0,n0))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f176])).
% 32.21/4.67 fof(f179,plain,(
% 32.21/4.67 ![X]: ((~less(X,n2)|less_or_equal(X,n1))&(less(X,n2)|~less_or_equal(X,n1)))),
% 32.21/4.67 inference(NNF_transformation,[status(thm)],[f40])).
% 32.21/4.67 fof(f180,plain,(
% 32.21/4.67 (![X]: (~less(X,n2)|less_or_equal(X,n1)))&(![X]: (less(X,n2)|~less_or_equal(X,n1)))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f179])).
% 32.21/4.67 fof(f181,plain,(
% 32.21/4.67 ![X0]: (~less(X0,n2)|less_or_equal(X0,n1))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f180])).
% 32.21/4.67 fof(f182,plain,(
% 32.21/4.67 ![X0]: (less(X0,n2)|~less_or_equal(X0,n1))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f180])).
% 32.21/4.67 fof(f183,plain,(
% 32.21/4.67 ![X]: ((~less(X,n3)|less_or_equal(X,n2))&(less(X,n3)|~less_or_equal(X,n2)))),
% 32.21/4.67 inference(NNF_transformation,[status(thm)],[f41])).
% 32.21/4.67 fof(f184,plain,(
% 32.21/4.67 (![X]: (~less(X,n3)|less_or_equal(X,n2)))&(![X]: (less(X,n3)|~less_or_equal(X,n2)))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f183])).
% 32.21/4.67 fof(f185,plain,(
% 32.21/4.67 ![X0]: (~less(X0,n3)|less_or_equal(X0,n2))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f184])).
% 32.21/4.67 fof(f186,plain,(
% 32.21/4.67 ![X0]: (less(X0,n3)|~less_or_equal(X0,n2))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f184])).
% 32.21/4.67 fof(f211,plain,(
% 32.21/4.67 ![X,Y]: ((~less(X,Y)|(~less(Y,X)&~Y=X))&(less(X,Y)|(less(Y,X)|Y=X)))),
% 32.21/4.67 inference(NNF_transformation,[status(thm)],[f48])).
% 32.21/4.67 fof(f212,plain,(
% 32.21/4.67 (![X,Y]: (~less(X,Y)|(~less(Y,X)&~Y=X)))&(![X,Y]: (less(X,Y)|(less(Y,X)|Y=X)))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f211])).
% 32.21/4.67 fof(f213,plain,(
% 32.21/4.67 ![X0,X1]: (~less(X0,X1)|~less(X1,X0))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f212])).
% 32.21/4.67 fof(f214,plain,(
% 32.21/4.67 ![X0,X1]: (~less(X0,X1)|~X1=X0)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f212])).
% 32.21/4.67 fof(f215,plain,(
% 32.21/4.67 ![X0,X1]: (less(X0,X1)|less(X1,X0)|X1=X0)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f212])).
% 32.21/4.67 fof(f216,plain,(
% 32.21/4.67 holdsAt(waterLevel(n0),n0)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f49])).
% 32.21/4.67 fof(f222,plain,(
% 32.21/4.67 ~holdsAt(waterLevel(n3),n3)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f56])).
% 32.21/4.67 fof(f223,definition,(
% 32.21/4.67 ![Event,Fluent]: (sP2_prd(Fluent,Event)<=>((Event=tapOn&Fluent=filling)|(Event=overflow&Fluent=spilling)))),
% 32.21/4.67 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 32.21/4.67 fof(f224,plain,(
% 32.21/4.67 ![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)<=>(sP2_prd(Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=tapOff)&Fluent=waterLevel(Height)))))),
% 32.21/4.67 inference(formula_renaming,[status(thm)],[f108,f223])).
% 32.21/4.67 fof(f225,plain,(
% 32.21/4.67 ![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))))))),
% 32.21/4.67 inference(NNF_transformation,[status(thm)],[f224])).
% 32.21/4.67 fof(f226,plain,(
% 32.21/4.67 (![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))))))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f225])).
% 32.21/4.67 fof(f227,plain,(
% 32.21/4.67 (![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))))))),
% 32.21/4.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(Height,sK10_skl(Time,Fluent,Event))],[f226])).
% 32.21/4.67 fof(f231,plain,(
% 32.21/4.67 ![X0,X1,X2]: (sP0_prd(X0,X1,X2)|~sP2_prd(X1,X2))),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f227])).
% 32.21/4.67 fof(f233,plain,(
% 32.21/4.67 ![Event,Time]: ((~sP1_prd(Time,Event)|(Event=tapOn&Time=n0))&(sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 32.21/4.67 inference(NNF_transformation,[status(thm)],[f132])).
% 32.21/4.67 fof(f234,plain,(
% 32.21/4.67 (![Event,Time]: (~sP1_prd(Time,Event)|(Event=tapOn&Time=n0)))&(![Event,Time]: (sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f233])).
% 32.21/4.67 fof(f235,plain,(
% 32.21/4.67 ![X0,X1]: (~sP1_prd(X0,X1)|X1=tapOn)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f234])).
% 32.21/4.67 fof(f236,plain,(
% 32.21/4.67 ![X0,X1]: (~sP1_prd(X0,X1)|X0=n0)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f234])).
% 32.21/4.67 fof(f237,plain,(
% 32.21/4.67 ![X0,X1]: (sP1_prd(X0,X1)|~X1=tapOn|~X0=n0)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f234])).
% 32.21/4.67 fof(f238,plain,(
% 32.21/4.67 ![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))))),
% 32.21/4.67 inference(NNF_transformation,[status(thm)],[f223])).
% 32.21/4.67 fof(f239,plain,(
% 32.21/4.67 (![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))))),
% 32.21/4.67 inference(miniscoping,[status(thm)],[f238])).
% 32.21/4.67 fof(f244,plain,(
% 32.21/4.67 ![X0,X1]: (sP2_prd(X0,X1)|~X1=tapOn|~X0=filling)),
% 32.21/4.67 inference(cnf_transformation,[status(thm)],[f239])).
% 32.21/4.67 fof(f246,plain,(
% 32.21/4.67 ![X0,X1]: (initiates(overflow,waterLevel(X0),X1)|~holdsAt(waterLevel(X0),X1))),
% 32.21/4.67 inference(destructive_equality_resolution,[status(thm)],[f117])).
% 32.21/4.67 fof(f247,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~terminates(X0,X1,X2)|X1=filling)),
% 32.21/4.67 inference(duplicate_literals_removal,[status(thm)],[f123])).
% 32.21/4.67 fof(f250,plain,(
% 32.21/4.67 ![X0,X1]: (releases(tapOn,waterLevel(X0),X1))),
% 32.21/4.67 inference(destructive_equality_resolution,[status(thm)],[f131])).
% 32.21/4.67 fof(f252,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~holdsAt(waterLevel(X0),X1)|trajectory(filling,X1,waterLevel(plus(X0,X2)),X2))),
% 32.21/4.67 inference(destructive_equality_resolution,[status(thm)],[f143])).
% 32.21/4.67 fof(f253,plain,(
% 32.21/4.67 ![X0]: (less_or_equal(X0,X0))),
% 32.21/4.67 inference(destructive_equality_resolution,[status(thm)],[f172])).
% 32.21/4.67 fof(f254,plain,(
% 32.21/4.67 ![X0]: (~less(X0,X0))),
% 32.21/4.67 inference(destructive_equality_resolution,[status(thm)],[f214])).
% 32.21/4.67 fof(f256,plain,(
% 32.21/4.67 sP1_prd(n0,tapOn)),
% 32.21/4.67 inference(destructive_equality_resolution,[status(thm)],[f237])).
% 32.21/4.67 fof(f257,plain,(
% 32.21/4.67 sP2_prd(filling,tapOn)),
% 32.21/4.67 inference(destructive_equality_resolution,[status(thm)],[f244])).
% 32.21/4.67 fof(f270,plain,(
% 32.21/4.67 n3=plus(n2,n1)),
% 32.21/4.67 inference(paramodulation,[status(thm)],[f162,f167])).
% 32.21/4.67 fof(f307,plain,(
% 32.21/4.67 less(n0,n1)),
% 32.21/4.67 inference(resolution,[status(thm)],[f178,f253])).
% 32.21/4.67 fof(f310,plain,(
% 32.21/4.67 less_or_equal(n0,n1)),
% 32.21/4.67 inference(resolution,[status(thm)],[f307,f171])).
% 32.21/4.67 fof(f313,plain,(
% 32.21/4.67 less(n0,n2)),
% 32.21/4.67 inference(resolution,[status(thm)],[f182,f310])).
% 32.21/4.67 fof(f317,plain,(
% 32.21/4.67 less_or_equal(n0,n2)),
% 32.21/4.67 inference(resolution,[status(thm)],[f313,f171])).
% 32.21/4.67 fof(f318,plain,(
% 32.21/4.67 ![X0,X1]: (~holdsAt(X0,X1)|releasedAt(X0,plus(X1,n1))|holdsAt(X0,plus(X1,n1))|X0=filling)),
% 32.21/4.67 inference(resolution,[status(thm)],[f82,f247])).
% 32.21/4.67 fof(f325,plain,(
% 32.21/4.67 ![X0,X1]: (less_or_equal(sK1_skl(n3,X0,X1),n2)|~stoppedIn(X1,X0,n3))),
% 32.21/4.67 inference(resolution,[status(thm)],[f185,f62])).
% 32.21/4.67 fof(f327,plain,(
% 32.21/4.67 less(n0,n3)),
% 32.21/4.67 inference(resolution,[status(thm)],[f186,f317])).
% 32.21/4.67 fof(f357,plain,(
% 32.21/4.67 ![X0,X1]: (releasedAt(X0,X1)|~releasedAt(X0,plus(X1,n1))|sK7_skl(X1,X0)=tapOn)),
% 32.21/4.67 inference(resolution,[status(thm)],[f94,f129])).
% 32.21/4.67 fof(f360,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~happens(X0,X1)|holdsAt(X2,plus(X1,n1))|~sP0_prd(X1,X2,X0))),
% 32.21/4.67 inference(resolution,[status(thm)],[f97,f116])).
% 32.21/4.67 fof(f384,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~happens(sK0_skl(X0,X1,X2),sK1_skl(X0,X1,X2))|~holdsAt(X1,plus(sK1_skl(X0,X1,X2),n1))|~stoppedIn(X2,X1,X0))),
% 32.21/4.67 inference(resolution,[status(thm)],[f100,f63])).
% 32.21/4.67 fof(f387,plain,(
% 32.21/4.67 ![X0,X1,X2]: (~holdsAt(X0,plus(sK1_skl(X1,X0,X2),n1))|~stoppedIn(X2,X0,X1))),
% 32.21/4.67 inference(forward_subsumption_resolution,[status(thm)],[f384,f60])).
% 32.21/4.67 fof(f389,plain,(
% 32.21/4.67 ![X0,X1]: (~happens(tapOn,X0)|releasedAt(waterLevel(X1),plus(X0,n1)))),
% 32.21/4.67 inference(resolution,[status(thm)],[f103,f250])).
% 32.21/4.67 fof(f455,plain,(
% 32.21/4.67 ![X0,X1]: (less(X0,X1)|X0=X1|less_or_equal(X1,X0))),
% 32.21/4.67 inference(resolution,[status(thm)],[f215,f171])).
% 32.21/4.67 fof(f518,plain,(
% 32.21/4.67 initiates(overflow,waterLevel(n0),n0)),
% 32.21/4.67 inference(resolution,[status(thm)],[f246,f216])).
% 32.21/4.67 fof(f549,plain,(
% 32.21/4.67 ![X0,X1,X2]: (sK0_skl(X0,X1,X2)=tapOff|sK0_skl(X0,X1,X2)=overflow|~stoppedIn(X2,X1,X0))),
% 32.21/4.67 inference(resolution,[status(thm)],[f120,f63])).
% 32.21/4.67 fof(f584,plain,(
% 32.21/4.67 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|initiates(overflow,waterLevel(n3),X1))),
% 32.21/4.67 inference(resolution,[status(thm)],[f136,f246])).
% 32.21/4.67 fof(f592,plain,(
% 32.21/4.67 ![X0,X1]: (sP1_prd(X0,sK7_skl(X0,X1))|sK7_skl(X0,X1)=overflow|releasedAt(X1,X0)|~releasedAt(X1,plus(X0,n1)))),
% 32.21/4.67 inference(resolution,[status(thm)],[f138,f93])).
% 32.21/4.67 fof(f595,plain,(
% 32.21/4.67 ![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))),
% 32.21/4.67 inference(resolution,[status(thm)],[f138,f60])).
% 32.21/4.67 fof(f676,plain,(
% 32.21/4.67 ![X0]: (trajectory(filling,n0,waterLevel(plus(n0,X0)),X0))),
% 32.21/4.67 inference(resolution,[status(thm)],[f252,f216])).
% 32.21/4.67 fof(f1074,plain,(
% 32.21/4.67 ![X0]: (X0=n2|less_or_equal(n2,X0)|less_or_equal(X0,n1))),
% 32.21/4.67 inference(resolution,[status(thm)],[f455,f181])).
% 32.21/4.67 fof(f1075,plain,(
% 32.21/4.67 ![X0]: (X0=n1|less_or_equal(n1,X0)|less_or_equal(X0,n0))),
% 32.21/4.67 inference(resolution,[status(thm)],[f455,f177])).
% 32.21/4.67 fof(f1086,plain,(
% 32.21/4.67 ~happens(overflow,n0)|~releasedAt(waterLevel(n0),plus(n0,n1))),
% 32.21/4.67 inference(resolution,[status(thm)],[f518,f106])).
% 32.21/4.67 fof(f1091,plain,(
% 32.21/4.67 ~happens(overflow,n0)|~releasedAt(waterLevel(n0),n1)),
% 32.21/4.67 inference(forward_demodulation,[status(thm)],[f158,f1086])).
% 32.21/4.67 fof(f1770,plain,(
% 32.21/4.67 ![X0]: (X0=n2|less_or_equal(n2,X0)|less(X0,n1)|X0=n1)),
% 32.21/4.67 inference(resolution,[status(thm)],[f1074,f170])).
% 32.21/4.67 fof(f1848,plain,(
% 32.21/4.67 ![X0]: (X0=n1|less_or_equal(n1,X0)|less(X0,n0)|X0=n0)),
% 32.21/4.67 inference(resolution,[status(thm)],[f1075,f170])).
% 32.21/4.67 fof(f1850,plain,(
% 32.21/4.67 ![X0]: (X0=n1|less_or_equal(n1,X0)|X0=n0)),
% 32.21/4.67 inference(forward_subsumption_resolution,[status(thm)],[f1848,f174])).
% 32.21/4.67 fof(f1861,plain,(
% 32.21/4.67 ![X0]: (X0=n1|X0=n0|less(n1,X0)|n1=X0)),
% 32.21/4.67 inference(resolution,[status(thm)],[f1850,f170])).
% 32.21/4.67 fof(f1862,plain,(
% 32.21/4.67 ![X0]: (X0=n1|X0=n0|less(n1,X0))),
% 32.21/4.67 inference(duplicate_literals_removal,[status(thm)],[f1861])).
% 32.21/4.67 fof(f1873,plain,(
% 32.21/4.67 ![X0]: (X0=n1|X0=n0|~less(X0,n1))),
% 32.21/4.67 inference(resolution,[status(thm)],[f1862,f213])).
% 32.21/4.68 fof(f2257,plain,(
% 32.21/4.68 ![X0]: (releasedAt(X0,n2)|~releasedAt(X0,n3)|sK7_skl(n2,X0)=tapOn)),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f270,f357])).
% 32.21/4.68 fof(f2268,plain,(
% 32.21/4.68 ![X0,X1,X2]: (holdsAt(X0,plus(X1,n1))|~sP0_prd(X1,X0,X2)|~sP1_prd(X1,X2))),
% 32.21/4.68 inference(resolution,[status(thm)],[f360,f139])).
% 32.21/4.68 fof(f2964,plain,(
% 32.21/4.68 ![X0,X1]: (releasedAt(waterLevel(X0),plus(X1,n1))|~sP1_prd(X1,tapOn))),
% 32.21/4.68 inference(resolution,[status(thm)],[f389,f139])).
% 32.21/4.68 fof(f8586,plain,(
% 32.21/4.68 trajectory(filling,n0,waterLevel(n3),n3)),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f160,f676])).
% 32.21/4.68 fof(f8634,plain,(
% 32.21/4.68 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n3)|stoppedIn(n0,filling,plus(n0,n3))|holdsAt(waterLevel(n3),plus(n0,n3)))),
% 32.21/4.68 inference(resolution,[status(thm)],[f8586,f75])).
% 32.21/4.68 fof(f8635,plain,(
% 32.21/4.68 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n3)|stoppedIn(n0,filling,n3)|holdsAt(waterLevel(n3),plus(n0,n3)))),
% 32.21/4.68 inference(forward_demodulation,[status(thm)],[f160,f8634])).
% 32.21/4.68 fof(f8636,plain,(
% 32.21/4.68 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n3)|stoppedIn(n0,filling,n3)|holdsAt(waterLevel(n3),n3))),
% 32.21/4.68 inference(forward_demodulation,[status(thm)],[f160,f8635])).
% 32.21/4.68 fof(f8637,plain,(
% 32.21/4.68 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|stoppedIn(n0,filling,n3)|holdsAt(waterLevel(n3),n3))),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f8636,f327])).
% 32.21/4.68 fof(f8639,plain,(
% 32.21/4.68 ![X0]: (~happens(X0,n0)|stoppedIn(n0,filling,n3)|holdsAt(waterLevel(n3),n3)|~sP0_prd(n0,filling,X0))),
% 32.21/4.68 inference(resolution,[status(thm)],[f8637,f116])).
% 32.21/4.68 fof(f8643,plain,(
% 32.21/4.68 ![X0]: (~happens(X0,n0)|stoppedIn(n0,filling,n3)|~sP0_prd(n0,filling,X0))),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f8639,f222])).
% 32.21/4.68 fof(f8647,plain,(
% 32.21/4.68 ![X0]: (stoppedIn(n0,filling,n3)|~sP0_prd(n0,filling,X0)|~sP1_prd(n0,X0))),
% 32.21/4.68 inference(resolution,[status(thm)],[f8643,f139])).
% 32.21/4.68 fof(f8658,plain,(
% 32.21/4.68 ![X0]: (stoppedIn(n0,filling,n3)|~sP1_prd(n0,X0)|~sP2_prd(filling,X0))),
% 32.21/4.68 inference(resolution,[status(thm)],[f8647,f231])).
% 32.21/4.68 fof(f8669,plain,(
% 32.21/4.68 stoppedIn(n0,filling,n3)|~sP1_prd(n0,tapOn)),
% 32.21/4.68 inference(resolution,[status(thm)],[f8658,f257])).
% 32.21/4.68 fof(f8674,plain,(
% 32.21/4.68 stoppedIn(n0,filling,n3)),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f8669,f256])).
% 32.21/4.68 fof(f8675,plain,(
% 32.21/4.68 less_or_equal(sK1_skl(n3,filling,n0),n2)),
% 32.21/4.68 inference(resolution,[status(thm)],[f8674,f325])).
% 32.21/4.68 fof(f8676,plain,(
% 32.21/4.68 sP1_prd(sK1_skl(n3,filling,n0),sK0_skl(n3,filling,n0))|sK0_skl(n3,filling,n0)=overflow),
% 32.21/4.68 inference(resolution,[status(thm)],[f8674,f595])).
% 32.21/4.68 fof(f8678,plain,(
% 32.21/4.68 sK0_skl(n3,filling,n0)=tapOff|sK0_skl(n3,filling,n0)=overflow),
% 32.21/4.68 inference(resolution,[status(thm)],[f8674,f549])).
% 32.21/4.68 fof(f8681,plain,(
% 32.21/4.68 ~holdsAt(filling,plus(sK1_skl(n3,filling,n0),n1))),
% 32.21/4.68 inference(resolution,[status(thm)],[f8674,f387])).
% 32.21/4.68 fof(f8688,plain,(
% 32.21/4.68 less(sK1_skl(n3,filling,n0),n2)|sK1_skl(n3,filling,n0)=n2),
% 32.21/4.68 inference(resolution,[status(thm)],[f8675,f170])).
% 32.21/4.68 fof(f9629,plain,(
% 32.21/4.68 ~stoppedIn(n0,filling,n3)|happens(overflow,sK1_skl(n3,filling,n0))|sK0_skl(n3,filling,n0)=tapOff),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f8678,f60])).
% 32.21/4.68 fof(f9631,plain,(
% 32.21/4.68 happens(overflow,sK1_skl(n3,filling,n0))|sK0_skl(n3,filling,n0)=tapOff),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f9629,f8674])).
% 32.21/4.68 fof(f9640,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|~less(n2,sK1_skl(n3,filling,n0))),
% 32.21/4.68 inference(resolution,[status(thm)],[f8688,f213])).
% 32.21/4.68 fof(f9721,plain,(
% 32.21/4.68 sK0_skl(n3,filling,n0)=overflow|sK1_skl(n3,filling,n0)=n0),
% 32.21/4.68 inference(resolution,[status(thm)],[f8676,f236])).
% 32.21/4.68 fof(f9722,plain,(
% 32.21/4.68 sK0_skl(n3,filling,n0)=overflow|sK0_skl(n3,filling,n0)=tapOn),
% 32.21/4.68 inference(resolution,[status(thm)],[f8676,f235])).
% 32.21/4.68 fof(f9729,plain,(
% 32.21/4.68 ~stoppedIn(n0,filling,n3)|happens(overflow,sK1_skl(n3,filling,n0))|sK1_skl(n3,filling,n0)=n0),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f9721,f60])).
% 32.21/4.68 fof(f9730,plain,(
% 32.21/4.68 happens(overflow,sK1_skl(n3,filling,n0))|sK1_skl(n3,filling,n0)=n0),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f9729,f8674])).
% 32.21/4.68 fof(f9734,plain,(
% 32.21/4.68 sP1_prd(sK1_skl(n3,filling,n0),tapOn)|sK0_skl(n3,filling,n0)=overflow|sK0_skl(n3,filling,n0)=overflow),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f9722,f8676])).
% 32.21/4.68 fof(f9737,plain,(
% 32.21/4.68 ~stoppedIn(n0,filling,n3)|terminates(tapOn,filling,sK1_skl(n3,filling,n0))|sK0_skl(n3,filling,n0)=overflow),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f9722,f63])).
% 32.21/4.68 fof(f9740,plain,(
% 32.21/4.68 sP1_prd(sK1_skl(n3,filling,n0),tapOn)|sK0_skl(n3,filling,n0)=overflow),
% 32.21/4.68 inference(duplicate_literals_removal,[status(thm)],[f9734])).
% 32.21/4.68 fof(f9741,plain,(
% 32.21/4.68 terminates(tapOn,filling,sK1_skl(n3,filling,n0))|sK0_skl(n3,filling,n0)=overflow),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f9737,f8674])).
% 32.21/4.68 fof(f9748,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n0|sP1_prd(sK1_skl(n3,filling,n0),overflow)|initiates(overflow,waterLevel(n3),sK1_skl(n3,filling,n0))),
% 32.21/4.68 inference(resolution,[status(thm)],[f9730,f584])).
% 32.21/4.68 fof(f9761,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n0|initiates(overflow,waterLevel(n3),sK1_skl(n3,filling,n0))),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f9748,f236])).
% 32.21/4.68 fof(f10190,plain,(
% 32.21/4.68 sK0_skl(n3,filling,n0)=overflow|tapOn=tapOff|tapOn=overflow),
% 32.21/4.68 inference(resolution,[status(thm)],[f9741,f120])).
% 32.21/4.68 fof(f10197,plain,(
% 32.21/4.68 sK0_skl(n3,filling,n0)=overflow|tapOn=overflow),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f10190,f147])).
% 32.21/4.68 fof(f10209,plain,(
% 32.21/4.68 ~stoppedIn(n0,filling,n3)|happens(overflow,sK1_skl(n3,filling,n0))|tapOn=overflow),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f10197,f60])).
% 32.21/4.68 fof(f10213,plain,(
% 32.21/4.68 happens(overflow,sK1_skl(n3,filling,n0))|tapOn=overflow),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f10209,f8674])).
% 32.21/4.68 fof(f10219,plain,(
% 32.21/4.68 tapOn=overflow|sP1_prd(sK1_skl(n3,filling,n0),overflow)|initiates(overflow,waterLevel(n3),sK1_skl(n3,filling,n0))),
% 32.21/4.68 inference(resolution,[status(thm)],[f10213,f584])).
% 32.21/4.68 fof(f10233,plain,(
% 32.21/4.68 sP1_prd(sK1_skl(n3,filling,n0),overflow)|initiates(overflow,waterLevel(n3),sK1_skl(n3,filling,n0))),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f10219,f149])).
% 32.21/4.68 fof(f10259,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n0|~happens(overflow,sK1_skl(n3,filling,n0))|holdsAt(waterLevel(n3),plus(sK1_skl(n3,filling,n0),n1))),
% 32.21/4.68 inference(resolution,[status(thm)],[f9761,f97])).
% 32.21/4.68 fof(f10263,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n0|holdsAt(waterLevel(n3),plus(sK1_skl(n3,filling,n0),n1))),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f10259,f9730])).
% 32.21/4.68 fof(f10294,plain,(
% 32.21/4.68 ![X0]: (releasedAt(waterLevel(X0),plus(n0,n1)))),
% 32.21/4.68 inference(resolution,[status(thm)],[f2964,f256])).
% 32.21/4.68 fof(f10296,plain,(
% 32.21/4.68 ~happens(overflow,n0)),
% 32.21/4.68 inference(backward_subsumption_resolution,[status(thm)],[f1091,f10299])).
% 32.21/4.68 fof(f10299,plain,(
% 32.21/4.68 ![X0]: (releasedAt(waterLevel(X0),n1))),
% 32.21/4.68 inference(forward_demodulation,[status(thm)],[f158,f10294])).
% 32.21/4.68 fof(f10868,plain,(
% 32.21/4.68 ![X0]: (X0=n2|less_or_equal(n2,X0)|X0=n1|X0=n1|X0=n0)),
% 32.21/4.68 inference(resolution,[status(thm)],[f1770,f1873])).
% 32.21/4.68 fof(f10882,plain,(
% 32.21/4.68 ![X0]: (X0=n2|less_or_equal(n2,X0)|X0=n1|X0=n0)),
% 32.21/4.68 inference(duplicate_literals_removal,[status(thm)],[f10868])).
% 32.21/4.68 fof(f10899,plain,(
% 32.21/4.68 ![X0]: (X0=n2|X0=n1|X0=n0|less(n2,X0)|n2=X0)),
% 32.21/4.68 inference(resolution,[status(thm)],[f10882,f170])).
% 32.21/4.68 fof(f10900,plain,(
% 32.21/4.68 ![X0]: (X0=n2|X0=n1|X0=n0|less(n2,X0))),
% 32.21/4.68 inference(duplicate_literals_removal,[status(thm)],[f10899])).
% 32.21/4.68 fof(f10901,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|sK1_skl(n3,filling,n0)=n1|sK1_skl(n3,filling,n0)=n0|sK1_skl(n3,filling,n0)=n2),
% 32.21/4.68 inference(resolution,[status(thm)],[f10900,f9640])).
% 32.21/4.68 fof(f10954,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|sK1_skl(n3,filling,n0)=n1|sK1_skl(n3,filling,n0)=n0),
% 32.21/4.68 inference(duplicate_literals_removal,[status(thm)],[f10901])).
% 32.21/4.68 fof(f12011,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n0|holdsAt(waterLevel(n3),plus(n1,sK1_skl(n3,filling,n0)))),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f167,f10263])).
% 32.21/4.68 fof(f12084,plain,(
% 32.21/4.68 happens(overflow,n0)|tapOn=overflow|sK1_skl(n3,filling,n0)=n2|sK1_skl(n3,filling,n0)=n1),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f10954,f10213])).
% 32.21/4.68 fof(f12141,plain,(
% 32.21/4.68 tapOn=overflow|sK1_skl(n3,filling,n0)=n2|sK1_skl(n3,filling,n0)=n1),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f12084,f10296])).
% 32.21/4.68 fof(f12167,plain,(
% 32.21/4.68 sP1_prd(sK1_skl(n3,filling,n0),overflow)|initiates(overflow,waterLevel(n3),n1)|tapOn=overflow|sK1_skl(n3,filling,n0)=n2),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f12141,f10233])).
% 32.21/4.68 fof(f12173,plain,(
% 32.21/4.68 happens(overflow,n1)|tapOn=overflow|tapOn=overflow|sK1_skl(n3,filling,n0)=n2),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f12141,f10213])).
% 32.21/4.68 fof(f12235,plain,(
% 32.21/4.68 initiates(overflow,waterLevel(n3),n1)|tapOn=overflow|sK1_skl(n3,filling,n0)=n2),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f12167,f235])).
% 32.21/4.68 fof(f12239,plain,(
% 32.21/4.68 happens(overflow,n1)|tapOn=overflow|sK1_skl(n3,filling,n0)=n2),
% 32.21/4.68 inference(duplicate_literals_removal,[status(thm)],[f12173])).
% 32.21/4.68 fof(f12240,plain,(
% 32.21/4.68 happens(overflow,n1)|sK1_skl(n3,filling,n0)=n2),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f12239,f149])).
% 32.21/4.68 fof(f14302,plain,(
% 32.21/4.68 tapOn=overflow|sK1_skl(n3,filling,n0)=n2|~happens(overflow,n1)|~releasedAt(waterLevel(n3),plus(n1,n1))),
% 32.21/4.68 inference(resolution,[status(thm)],[f12235,f106])).
% 32.21/4.68 fof(f14303,plain,(
% 32.21/4.68 tapOn=overflow|sK1_skl(n3,filling,n0)=n2|~happens(overflow,n1)|holdsAt(waterLevel(n3),plus(n1,n1))),
% 32.21/4.68 inference(resolution,[status(thm)],[f12235,f97])).
% 32.21/4.68 fof(f14315,plain,(
% 32.21/4.68 tapOn=overflow|sK1_skl(n3,filling,n0)=n2|~happens(overflow,n1)|~releasedAt(waterLevel(n3),n2)),
% 32.21/4.68 inference(forward_demodulation,[status(thm)],[f161,f14302])).
% 32.21/4.68 fof(f14316,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|~happens(overflow,n1)|~releasedAt(waterLevel(n3),n2)),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f14315,f149])).
% 32.21/4.68 fof(f14317,plain,(
% 32.21/4.68 tapOn=overflow|sK1_skl(n3,filling,n0)=n2|~happens(overflow,n1)|holdsAt(waterLevel(n3),n2)),
% 32.21/4.68 inference(forward_demodulation,[status(thm)],[f161,f14303])).
% 32.21/4.68 fof(f14318,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|~happens(overflow,n1)|holdsAt(waterLevel(n3),n2)),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f14317,f149])).
% 32.21/4.68 fof(f14320,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|holdsAt(waterLevel(n3),n2)|sK1_skl(n3,filling,n0)=n2),
% 32.21/4.68 inference(resolution,[status(thm)],[f14318,f12240])).
% 32.21/4.68 fof(f14322,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|holdsAt(waterLevel(n3),n2)),
% 32.21/4.68 inference(duplicate_literals_removal,[status(thm)],[f14320])).
% 32.21/4.68 fof(f14337,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|releasedAt(waterLevel(n3),plus(n2,n1))|holdsAt(waterLevel(n3),plus(n2,n1))|waterLevel(n3)=filling),
% 32.21/4.68 inference(resolution,[status(thm)],[f14322,f318])).
% 32.21/4.68 fof(f14354,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|releasedAt(waterLevel(n3),n3)|holdsAt(waterLevel(n3),plus(n2,n1))|waterLevel(n3)=filling),
% 32.21/4.68 inference(forward_demodulation,[status(thm)],[f270,f14337])).
% 32.21/4.68 fof(f14355,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|releasedAt(waterLevel(n3),n3)|holdsAt(waterLevel(n3),n3)|waterLevel(n3)=filling),
% 32.21/4.68 inference(forward_demodulation,[status(thm)],[f270,f14354])).
% 32.21/4.68 fof(f14356,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|releasedAt(waterLevel(n3),n3)|waterLevel(n3)=filling),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f14355,f222])).
% 32.21/4.68 fof(f15538,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|waterLevel(n3)=filling|releasedAt(waterLevel(n3),n2)|sK7_skl(n2,waterLevel(n3))=tapOn),
% 32.21/4.68 inference(resolution,[status(thm)],[f14356,f2257])).
% 32.21/4.68 fof(f15541,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|releasedAt(waterLevel(n3),n2)|sK7_skl(n2,waterLevel(n3))=tapOn),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f15538,f150])).
% 32.21/4.68 fof(f16263,plain,(
% 32.21/4.68 ![X0,X1,X2]: (holdsAt(X0,plus(X1,n1))|~sP1_prd(X1,X2)|~sP2_prd(X0,X2))),
% 32.21/4.68 inference(resolution,[status(thm)],[f2268,f231])).
% 32.21/4.68 fof(f16272,plain,(
% 32.21/4.68 ![X0]: (holdsAt(filling,plus(X0,n1))|~sP1_prd(X0,tapOn))),
% 32.21/4.68 inference(resolution,[status(thm)],[f16263,f257])).
% 32.21/4.68 fof(f16277,plain,(
% 32.21/4.68 holdsAt(filling,plus(sK1_skl(n3,filling,n0),n1))|sK0_skl(n3,filling,n0)=overflow),
% 32.21/4.68 inference(resolution,[status(thm)],[f16272,f9740])).
% 32.21/4.68 fof(f16295,plain,(
% 32.21/4.68 happens(overflow,sK1_skl(n3,filling,n0))|overflow=tapOff),
% 32.21/4.68 inference(backward_demodulation,[status(thm)],[f16338,f9631])).
% 32.21/4.68 fof(f16338,plain,(
% 32.21/4.68 sK0_skl(n3,filling,n0)=overflow),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f16277,f8681])).
% 32.21/4.68 fof(f16344,plain,(
% 32.21/4.68 happens(overflow,sK1_skl(n3,filling,n0))),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f16295,f148])).
% 32.21/4.68 fof(f16445,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|sK7_skl(n2,waterLevel(n3))=tapOn|sK1_skl(n3,filling,n0)=n2|~happens(overflow,n1)),
% 32.21/4.68 inference(resolution,[status(thm)],[f15541,f14316])).
% 32.21/4.68 fof(f16453,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|sK7_skl(n2,waterLevel(n3))=tapOn|~happens(overflow,n1)),
% 32.21/4.68 inference(duplicate_literals_removal,[status(thm)],[f16445])).
% 32.21/4.68 fof(f16454,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n2|sK7_skl(n2,waterLevel(n3))=tapOn),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f16453,f12240])).
% 32.21/4.68 fof(f16471,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n0|holdsAt(waterLevel(n3),plus(n1,n2))|sK7_skl(n2,waterLevel(n3))=tapOn),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f16454,f12011])).
% 32.21/4.68 fof(f16519,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n0|holdsAt(waterLevel(n3),n3)|sK7_skl(n2,waterLevel(n3))=tapOn),
% 32.21/4.68 inference(forward_demodulation,[status(thm)],[f162,f16471])).
% 32.21/4.68 fof(f16520,plain,(
% 32.21/4.68 sK1_skl(n3,filling,n0)=n0|sK7_skl(n2,waterLevel(n3))=tapOn),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f16519,f222])).
% 32.21/4.68 fof(f16631,plain,(
% 32.21/4.68 happens(overflow,n0)|sK7_skl(n2,waterLevel(n3))=tapOn),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f16520,f16344])).
% 32.21/4.68 fof(f16725,plain,(
% 32.21/4.68 sK7_skl(n2,waterLevel(n3))=tapOn),
% 32.21/4.68 inference(forward_subsumption_resolution,[status(thm)],[f16631,f10296])).
% 32.21/4.68 fof(f16743,plain,(
% 32.21/4.68 sP1_prd(n2,tapOn)|sK7_skl(n2,waterLevel(n3))=overflow|releasedAt(waterLevel(n3),n2)|~releasedAt(waterLevel(n3),plus(n2,n1))),
% 32.21/4.68 inference(paramodulation,[status(thm)],[f16725,f592])).
% 32.21/4.68 fof(f16751,plain,(
% 32.21/4.68 sP1_prd(n2,tapOn)|tapOn=overflow|releasedAt(waterLevel(n3),n2)|~releasedAt(waterLevel(n3),plus(n2,n1))),
% 32.21/4.68 inference(forward_demodulation,[status(thm)],[f16725,f16743])).
% 32.21/4.68 fof(f16752,plain,(
% 32.21/4.68 sP1_prd(n2,tapOn)|tapOn=overflow|releasedAt(waterLevel(n3),n2)|~releasedAt(waterLevel(n3),n3)),
% 32.21/4.68 inference(forward_demodulation,[status(thm)],[f270,f16751])).
% 32.21/4.68 fof(f16753,plain,(
% 32.21/4.68 sP1_prd(n2,tapOn)|releasedAt(waterLevel(n3),n2)|~releasedAt(waterLevel(n3),n3)),
% 32.21/4.73 inference(forward_subsumption_resolution,[status(thm)],[f16752,f149])).
% 32.21/4.73 fof(f17244,plain,(
% 32.21/4.73 sP1_prd(n2,tapOn)|releasedAt(waterLevel(n3),n2)|sK1_skl(n3,filling,n0)=n2|waterLevel(n3)=filling),
% 32.21/4.73 inference(resolution,[status(thm)],[f16753,f14356])).
% 32.21/4.73 fof(f17248,plain,(
% 32.21/4.73 sP1_prd(n2,tapOn)|releasedAt(waterLevel(n3),n2)|sK1_skl(n3,filling,n0)=n2),
% 32.21/4.73 inference(forward_subsumption_resolution,[status(thm)],[f17244,f150])).
% 32.21/4.73 fof(f17255,plain,(
% 32.21/4.73 sP1_prd(n2,tapOn)|sK1_skl(n3,filling,n0)=n2|sK1_skl(n3,filling,n0)=n2|~happens(overflow,n1)),
% 32.21/4.73 inference(resolution,[status(thm)],[f17248,f14316])).
% 32.21/4.73 fof(f17263,plain,(
% 32.21/4.73 sP1_prd(n2,tapOn)|sK1_skl(n3,filling,n0)=n2|~happens(overflow,n1)),
% 32.21/4.73 inference(duplicate_literals_removal,[status(thm)],[f17255])).
% 32.21/4.73 fof(f17264,plain,(
% 32.21/4.73 sP1_prd(n2,tapOn)|sK1_skl(n3,filling,n0)=n2),
% 32.21/4.73 inference(forward_subsumption_resolution,[status(thm)],[f17263,f12240])).
% 32.21/4.73 fof(f17272,plain,(
% 32.21/4.73 sK1_skl(n3,filling,n0)=n2|n2=n0),
% 32.21/4.73 inference(resolution,[status(thm)],[f17264,f236])).
% 32.21/4.73 fof(f17284,plain,(
% 32.21/4.73 sK1_skl(n3,filling,n0)=n0|holdsAt(waterLevel(n3),plus(n1,n2))|n2=n0),
% 32.21/4.73 inference(paramodulation,[status(thm)],[f17272,f12011])).
% 32.21/4.73 fof(f17332,plain,(
% 32.21/4.73 sK1_skl(n3,filling,n0)=n0|holdsAt(waterLevel(n3),n3)|n2=n0),
% 32.21/4.73 inference(forward_demodulation,[status(thm)],[f162,f17284])).
% 32.21/4.73 fof(f17333,plain,(
% 32.21/4.73 sK1_skl(n3,filling,n0)=n0|n2=n0),
% 32.21/4.73 inference(forward_subsumption_resolution,[status(thm)],[f17332,f222])).
% 32.21/4.73 fof(f17448,plain,(
% 32.21/4.73 n2=n0|n2=n0|n2=n0),
% 32.21/4.73 inference(paramodulation,[status(thm)],[f17272,f17333])).
% 32.21/4.73 fof(f17705,plain,(
% 32.21/4.73 less(n2,n2)),
% 32.21/4.73 inference(backward_demodulation,[status(thm)],[f17941,f313])).
% 32.21/4.73 fof(f17941,plain,(
% 32.21/4.73 n2=n0),
% 32.21/4.73 inference(duplicate_literals_removal,[status(thm)],[f17448])).
% 32.21/4.73 fof(f18227,plain,(
% 32.21/4.73 $false),
% 32.21/4.73 inference(forward_subsumption_resolution,[status(thm)],[f17705,f254])).
% 32.21/4.73 % SZS output end CNFRefutation for theBenchmark.p
% 32.21/4.74 % Elapsed time: 4.350354 seconds
% 32.21/4.74 % CPU time: 33.815523 seconds
% 32.21/4.74 % Total memory used: 280.951 MB
% 32.21/4.74 % Net memory used: 266.645 MB
%------------------------------------------------------------------------------