%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR009+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 : n010.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 10.10s 1.76s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR009+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.10/0.37 % Computer : n010.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 14:24:26 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 10.10/1.76 % Refutation found
% 10.10/1.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.10/1.76 % SZS output start CNFRefutation for theBenchmark
% 10.10/1.76 fof(f1,axiom,(
% 10.10/1.76 (! [Time1,Fluent,Time2] :( stoppedIn(Time1,Fluent,Time2)<=> (? [Event,Time] :( happens(Event,Time)& less(Time1,Time)& less(Time,Time2)& terminates(Event,Fluent,Time) ) )) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f3,axiom,(
% 10.10/1.76 (! [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)) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f5,axiom,(
% 10.10/1.76 (! [Fluent,Time] :( ( holdsAt(Fluent,Time)& ~ releasedAt(Fluent,plus(Time,n1))& ~ (? [Event] :( happens(Event,Time)& terminates(Event,Fluent,Time) ) ))=> holdsAt(Fluent,plus(Time,n1)) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f8,axiom,(
% 10.10/1.76 (! [Fluent,Time] :( ( ~ releasedAt(Fluent,Time)& ~ (? [Event] :( happens(Event,Time)& releases(Event,Fluent,Time) ) ))=> ~ releasedAt(Fluent,plus(Time,n1)) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f9,axiom,(
% 10.10/1.76 (! [Event,Time,Fluent] :( ( happens(Event,Time)& initiates(Event,Fluent,Time) )=> holdsAt(Fluent,plus(Time,n1)) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f11,axiom,(
% 10.10/1.76 (! [Event,Time,Fluent] :( ( happens(Event,Time)& releases(Event,Fluent,Time) )=> releasedAt(Fluent,plus(Time,n1)) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f12,axiom,(
% 10.10/1.76 (! [Event,Time,Fluent] :( ( happens(Event,Time)& ( initiates(Event,Fluent,Time)| terminates(Event,Fluent,Time) ) )=> ~ releasedAt(Fluent,plus(Time,n1)) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f13,axiom,(
% 10.10/1.76 (! [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) ) )) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f15,axiom,(
% 10.10/1.76 (! [Event,Fluent,Time] :( releases(Event,Fluent,Time)<=> (? [Height] :( Event = tapOn& Fluent = waterLevel(Height) ) )) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f16,axiom,(
% 10.10/1.76 (! [Event,Time] :( happens(Event,Time)<=> ( ( Event = tapOn& Time = n0 )| ( holdsAt(waterLevel(n3),Time)& holdsAt(filling,Time)& Event = overflow ) ) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f17,axiom,(
% 10.10/1.76 (! [Height1,Time,Height2,Offset] :( ( holdsAt(waterLevel(Height1),Time)& Height2 = plus(Height1,Offset) )=> trajectory(filling,Time,waterLevel(Height2),Offset) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f18,axiom,(
% 10.10/1.76 (! [Time,Height1,Height2] :( ( holdsAt(waterLevel(Height1),Time)& holdsAt(waterLevel(Height2),Time) )=> Height1 = Height2 ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f22,axiom,(
% 10.10/1.76 (! [X] : filling != waterLevel(X) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f27,axiom,(
% 10.10/1.76 plus(n0,n1) = n1 ),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f30,axiom,(
% 10.10/1.76 plus(n1,n1) = n2 ),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f36,axiom,(
% 10.10/1.76 (! [X,Y] : plus(X,Y) = plus(Y,X) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f37,axiom,(
% 10.10/1.76 (! [X,Y] :( less_or_equal(X,Y)<=> ( less(X,Y)| X = Y ) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f38,axiom,(
% 10.10/1.76 ~ (? [X] : less(X,n0) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f39,axiom,(
% 10.10/1.76 (! [X] :( less(X,n1)<=> less_or_equal(X,n0) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f40,axiom,(
% 10.10/1.76 (! [X] :( less(X,n2)<=> less_or_equal(X,n1) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f41,axiom,(
% 10.10/1.76 (! [X] :( less(X,n3)<=> less_or_equal(X,n2) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f48,axiom,(
% 10.10/1.76 (! [X,Y] :( less(X,Y)<=> ( ~ less(Y,X)& Y != X ) ) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f49,hypothesis,(
% 10.10/1.76 holdsAt(waterLevel(n0),n0) ),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f50,hypothesis,(
% 10.10/1.76 ~ holdsAt(filling,n0) ),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f52,hypothesis,(
% 10.10/1.76 (! [Height] : ~ releasedAt(waterLevel(Height),n0) )),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f55,conjecture,(
% 10.10/1.76 holdsAt(filling,n2) ),
% 10.10/1.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.76 fof(f56,negated_conjecture,(
% 10.10/1.76 ~(holdsAt(filling,n2) )),
% 10.10/1.76 inference(negated_conjecture,[status(cth)],[f55])).
% 10.10/1.76 fof(f57,plain,(
% 10.10/1.76 ![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)))))),
% 10.10/1.76 inference(NNF_transformation,[status(thm)],[f1])).
% 10.10/1.76 fof(f58,plain,(
% 10.10/1.76 (![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)))))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f57])).
% 10.10/1.76 fof(f59,plain,(
% 10.10/1.76 (![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)))))),
% 10.10/1.76 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])).
% 10.10/1.76 fof(f61,plain,(
% 10.10/1.76 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|less(X0,sK1_skl(X2,X1,X0)))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f59])).
% 10.10/1.76 fof(f62,plain,(
% 10.10/1.76 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|less(sK1_skl(X2,X1,X0),X2))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f59])).
% 10.10/1.76 fof(f73,plain,(
% 10.10/1.76 ![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)))),
% 10.10/1.76 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 10.10/1.76 fof(f74,plain,(
% 10.10/1.76 ![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)))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f73])).
% 10.10/1.76 fof(f75,plain,(
% 10.10/1.76 ![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)))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f74])).
% 10.10/1.76 fof(f79,plain,(
% 10.10/1.76 ![Fluent,Time]: (((~holdsAt(Fluent,Time)|releasedAt(Fluent,plus(Time,n1)))|(?[Event]: (happens(Event,Time)&terminates(Event,Fluent,Time))))|holdsAt(Fluent,plus(Time,n1)))),
% 10.10/1.76 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 10.10/1.76 fof(f80,plain,(
% 10.10/1.76 ![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)))),
% 10.10/1.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(Event,sK4_skl(Time,Fluent))],[f79])).
% 10.10/1.76 fof(f81,plain,(
% 10.10/1.76 ![X0,X1]: (~holdsAt(X0,X1)|releasedAt(X0,plus(X1,n1))|happens(sK4_skl(X1,X0),X1)|holdsAt(X0,plus(X1,n1)))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f80])).
% 10.10/1.76 fof(f91,plain,(
% 10.10/1.76 ![Fluent,Time]: ((releasedAt(Fluent,Time)|(?[Event]: (happens(Event,Time)&releases(Event,Fluent,Time))))|~releasedAt(Fluent,plus(Time,n1)))),
% 10.10/1.76 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 10.10/1.76 fof(f92,plain,(
% 10.10/1.76 ![Fluent,Time]: ((releasedAt(Fluent,Time)|(happens(sK7_skl(Time,Fluent),Time)&releases(sK7_skl(Time,Fluent),Fluent,Time)))|~releasedAt(Fluent,plus(Time,n1)))),
% 10.10/1.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Event,sK7_skl(Time,Fluent))],[f91])).
% 10.10/1.76 fof(f93,plain,(
% 10.10/1.76 ![X0,X1]: (releasedAt(X0,X1)|happens(sK7_skl(X1,X0),X1)|~releasedAt(X0,plus(X1,n1)))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f92])).
% 10.10/1.76 fof(f94,plain,(
% 10.10/1.76 ![X0,X1]: (releasedAt(X0,X1)|releases(sK7_skl(X1,X0),X0,X1)|~releasedAt(X0,plus(X1,n1)))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f92])).
% 10.10/1.76 fof(f95,plain,(
% 10.10/1.76 ![Event,Time,Fluent]: ((~happens(Event,Time)|~initiates(Event,Fluent,Time))|holdsAt(Fluent,plus(Time,n1)))),
% 10.10/1.76 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 10.10/1.76 fof(f96,plain,(
% 10.10/1.76 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~initiates(Event,Fluent,Time)))|holdsAt(Fluent,plus(Time,n1)))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f95])).
% 10.10/1.76 fof(f97,plain,(
% 10.10/1.76 ![X0,X1,X2]: (~happens(X0,X1)|~initiates(X0,X2,X1)|holdsAt(X2,plus(X1,n1)))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f96])).
% 10.10/1.76 fof(f101,plain,(
% 10.10/1.76 ![Event,Time,Fluent]: ((~happens(Event,Time)|~releases(Event,Fluent,Time))|releasedAt(Fluent,plus(Time,n1)))),
% 10.10/1.76 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 10.10/1.76 fof(f102,plain,(
% 10.10/1.76 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~releases(Event,Fluent,Time)))|releasedAt(Fluent,plus(Time,n1)))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f101])).
% 10.10/1.76 fof(f103,plain,(
% 10.10/1.76 ![X0,X1,X2]: (~happens(X0,X1)|~releases(X0,X2,X1)|releasedAt(X2,plus(X1,n1)))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f102])).
% 10.10/1.76 fof(f104,plain,(
% 10.10/1.76 ![Event,Time,Fluent]: ((~happens(Event,Time)|(~initiates(Event,Fluent,Time)&~terminates(Event,Fluent,Time)))|~releasedAt(Fluent,plus(Time,n1)))),
% 10.10/1.76 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 10.10/1.76 fof(f105,plain,(
% 10.10/1.76 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|(~initiates(Event,Fluent,Time)&~terminates(Event,Fluent,Time))))|~releasedAt(Fluent,plus(Time,n1)))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f104])).
% 10.10/1.76 fof(f106,plain,(
% 10.10/1.76 ![X0,X1,X2]: (~happens(X0,X1)|~initiates(X0,X2,X1)|~releasedAt(X2,plus(X1,n1)))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f105])).
% 10.10/1.76 fof(f108,definition,(
% 10.10/1.76 ![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)))))),
% 10.10/1.76 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 10.10/1.76 fof(f109,plain,(
% 10.10/1.76 ![Event,Fluent,Time]: (initiates(Event,Fluent,Time)<=>(sP0_prd(Time,Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=overflow)&Fluent=waterLevel(Height)))))),
% 10.10/1.76 inference(formula_renaming,[status(thm)],[f13,f108])).
% 10.10/1.76 fof(f110,plain,(
% 10.10/1.76 ![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))))))),
% 10.10/1.76 inference(NNF_transformation,[status(thm)],[f109])).
% 10.10/1.76 fof(f111,plain,(
% 10.10/1.76 (![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))))))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f110])).
% 10.10/1.76 fof(f112,plain,(
% 10.10/1.76 (![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))))))),
% 10.10/1.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(Height,sK8_skl(Time,Fluent,Event))],[f111])).
% 10.10/1.76 fof(f116,plain,(
% 10.10/1.76 ![X0,X1,X2]: (initiates(X0,X1,X2)|~sP0_prd(X2,X1,X0))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f112])).
% 10.10/1.76 fof(f126,plain,(
% 10.10/1.76 ![Event,Fluent,Time]: ((~releases(Event,Fluent,Time)|(?[Height]: (Event=tapOn&Fluent=waterLevel(Height))))&(releases(Event,Fluent,Time)|(![Height]: (~Event=tapOn|~Fluent=waterLevel(Height)))))),
% 10.10/1.76 inference(NNF_transformation,[status(thm)],[f15])).
% 10.10/1.76 fof(f127,plain,(
% 10.10/1.76 (![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)))))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f126])).
% 10.10/1.76 fof(f128,plain,(
% 10.10/1.76 (![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)))))),
% 10.10/1.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(Height,sK9_skl(Fluent,Event))],[f127])).
% 10.10/1.76 fof(f129,plain,(
% 10.10/1.76 ![X0,X1,X2]: (~releases(X0,X1,X2)|X0=tapOn)),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f128])).
% 10.10/1.76 fof(f130,plain,(
% 10.10/1.76 ![X0,X1,X2]: (~releases(X0,X1,X2)|X1=waterLevel(sK9_skl(X1,X0)))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f128])).
% 10.10/1.76 fof(f131,plain,(
% 10.10/1.76 ![X0,X1,X2,X3]: (releases(X0,X1,X2)|~X0=tapOn|~X1=waterLevel(X3))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f128])).
% 10.10/1.76 fof(f132,definition,(
% 10.10/1.76 ![Event,Time]: (sP1_prd(Time,Event)<=>(Event=tapOn&Time=n0))),
% 10.10/1.76 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 10.10/1.76 fof(f133,plain,(
% 10.10/1.76 ![Event,Time]: (happens(Event,Time)<=>(sP1_prd(Time,Event)|((holdsAt(waterLevel(n3),Time)&holdsAt(filling,Time))&Event=overflow)))),
% 10.10/1.76 inference(formula_renaming,[status(thm)],[f16,f132])).
% 10.10/1.76 fof(f134,plain,(
% 10.10/1.76 ![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))))),
% 10.10/1.76 inference(NNF_transformation,[status(thm)],[f133])).
% 10.10/1.76 fof(f135,plain,(
% 10.10/1.76 (![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))))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f134])).
% 10.10/1.76 fof(f136,plain,(
% 10.10/1.76 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|holdsAt(waterLevel(n3),X1))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f135])).
% 10.10/1.76 fof(f138,plain,(
% 10.10/1.76 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|X0=overflow)),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f135])).
% 10.10/1.76 fof(f139,plain,(
% 10.10/1.76 ![X0,X1]: (happens(X0,X1)|~sP1_prd(X1,X0))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f135])).
% 10.10/1.76 fof(f141,plain,(
% 10.10/1.76 ![Height1,Time,Height2,Offset]: ((~holdsAt(waterLevel(Height1),Time)|~Height2=plus(Height1,Offset))|trajectory(filling,Time,waterLevel(Height2),Offset))),
% 10.10/1.76 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 10.10/1.76 fof(f142,plain,(
% 10.10/1.76 ![Time,Height2,Offset]: ((![Height1]: (~holdsAt(waterLevel(Height1),Time)|~Height2=plus(Height1,Offset)))|trajectory(filling,Time,waterLevel(Height2),Offset))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f141])).
% 10.10/1.76 fof(f143,plain,(
% 10.10/1.76 ![X0,X1,X2,X3]: (~holdsAt(waterLevel(X0),X1)|~X2=plus(X0,X3)|trajectory(filling,X1,waterLevel(X2),X3))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f142])).
% 10.10/1.76 fof(f144,plain,(
% 10.10/1.76 ![Time,Height1,Height2]: ((~holdsAt(waterLevel(Height1),Time)|~holdsAt(waterLevel(Height2),Time))|Height1=Height2)),
% 10.10/1.76 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 10.10/1.76 fof(f145,plain,(
% 10.10/1.76 ![Height1,Height2]: ((![Time]: (~holdsAt(waterLevel(Height1),Time)|~holdsAt(waterLevel(Height2),Time)))|Height1=Height2)),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f144])).
% 10.10/1.76 fof(f146,plain,(
% 10.10/1.76 ![X0,X1,X2]: (~holdsAt(waterLevel(X0),X1)|~holdsAt(waterLevel(X2),X1)|X0=X2)),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f145])).
% 10.10/1.76 fof(f150,plain,(
% 10.10/1.76 ![X0]: (~filling=waterLevel(X0))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f22])).
% 10.10/1.76 fof(f158,plain,(
% 10.10/1.76 plus(n0,n1)=n1),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f27])).
% 10.10/1.76 fof(f161,plain,(
% 10.10/1.76 plus(n1,n1)=n2),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f30])).
% 10.10/1.76 fof(f167,plain,(
% 10.10/1.76 ![X0,X1]: (plus(X0,X1)=plus(X1,X0))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f36])).
% 10.10/1.76 fof(f168,plain,(
% 10.10/1.76 ![X,Y]: ((~less_or_equal(X,Y)|(less(X,Y)|X=Y))&(less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 10.10/1.76 inference(NNF_transformation,[status(thm)],[f37])).
% 10.10/1.76 fof(f169,plain,(
% 10.10/1.76 (![X,Y]: (~less_or_equal(X,Y)|(less(X,Y)|X=Y)))&(![X,Y]: (less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f168])).
% 10.10/1.76 fof(f170,plain,(
% 10.10/1.76 ![X0,X1]: (~less_or_equal(X0,X1)|less(X0,X1)|X0=X1)),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f169])).
% 10.10/1.76 fof(f172,plain,(
% 10.10/1.76 ![X0,X1]: (less_or_equal(X0,X1)|~X0=X1)),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f169])).
% 10.10/1.76 fof(f173,plain,(
% 10.10/1.76 (![X]: ~less(X,n0))),
% 10.10/1.76 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 10.10/1.76 fof(f174,plain,(
% 10.10/1.76 ![X0]: (~less(X0,n0))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f173])).
% 10.10/1.76 fof(f175,plain,(
% 10.10/1.76 ![X]: ((~less(X,n1)|less_or_equal(X,n0))&(less(X,n1)|~less_or_equal(X,n0)))),
% 10.10/1.76 inference(NNF_transformation,[status(thm)],[f39])).
% 10.10/1.76 fof(f176,plain,(
% 10.10/1.76 (![X]: (~less(X,n1)|less_or_equal(X,n0)))&(![X]: (less(X,n1)|~less_or_equal(X,n0)))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f175])).
% 10.10/1.76 fof(f177,plain,(
% 10.10/1.76 ![X0]: (~less(X0,n1)|less_or_equal(X0,n0))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f176])).
% 10.10/1.76 fof(f178,plain,(
% 10.10/1.76 ![X0]: (less(X0,n1)|~less_or_equal(X0,n0))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f176])).
% 10.10/1.76 fof(f179,plain,(
% 10.10/1.76 ![X]: ((~less(X,n2)|less_or_equal(X,n1))&(less(X,n2)|~less_or_equal(X,n1)))),
% 10.10/1.76 inference(NNF_transformation,[status(thm)],[f40])).
% 10.10/1.76 fof(f180,plain,(
% 10.10/1.76 (![X]: (~less(X,n2)|less_or_equal(X,n1)))&(![X]: (less(X,n2)|~less_or_equal(X,n1)))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f179])).
% 10.10/1.76 fof(f182,plain,(
% 10.10/1.76 ![X0]: (less(X0,n2)|~less_or_equal(X0,n1))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f180])).
% 10.10/1.76 fof(f183,plain,(
% 10.10/1.76 ![X]: ((~less(X,n3)|less_or_equal(X,n2))&(less(X,n3)|~less_or_equal(X,n2)))),
% 10.10/1.76 inference(NNF_transformation,[status(thm)],[f41])).
% 10.10/1.76 fof(f184,plain,(
% 10.10/1.76 (![X]: (~less(X,n3)|less_or_equal(X,n2)))&(![X]: (less(X,n3)|~less_or_equal(X,n2)))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f183])).
% 10.10/1.76 fof(f186,plain,(
% 10.10/1.76 ![X0]: (less(X0,n3)|~less_or_equal(X0,n2))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f184])).
% 10.10/1.76 fof(f211,plain,(
% 10.10/1.76 ![X,Y]: ((~less(X,Y)|(~less(Y,X)&~Y=X))&(less(X,Y)|(less(Y,X)|Y=X)))),
% 10.10/1.76 inference(NNF_transformation,[status(thm)],[f48])).
% 10.10/1.76 fof(f212,plain,(
% 10.10/1.76 (![X,Y]: (~less(X,Y)|(~less(Y,X)&~Y=X)))&(![X,Y]: (less(X,Y)|(less(Y,X)|Y=X)))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f211])).
% 10.10/1.76 fof(f213,plain,(
% 10.10/1.76 ![X0,X1]: (~less(X0,X1)|~less(X1,X0))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f212])).
% 10.10/1.76 fof(f216,plain,(
% 10.10/1.76 holdsAt(waterLevel(n0),n0)),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f49])).
% 10.10/1.76 fof(f217,plain,(
% 10.10/1.76 ~holdsAt(filling,n0)),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f50])).
% 10.10/1.76 fof(f219,plain,(
% 10.10/1.76 ![X0]: (~releasedAt(waterLevel(X0),n0))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f52])).
% 10.10/1.76 fof(f222,plain,(
% 10.10/1.76 ~holdsAt(filling,n2)),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f56])).
% 10.10/1.76 fof(f223,definition,(
% 10.10/1.76 ![Event,Fluent]: (sP2_prd(Fluent,Event)<=>((Event=tapOn&Fluent=filling)|(Event=overflow&Fluent=spilling)))),
% 10.10/1.76 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 10.10/1.76 fof(f224,plain,(
% 10.10/1.76 ![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)<=>(sP2_prd(Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=tapOff)&Fluent=waterLevel(Height)))))),
% 10.10/1.76 inference(formula_renaming,[status(thm)],[f108,f223])).
% 10.10/1.76 fof(f225,plain,(
% 10.10/1.76 ![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))))))),
% 10.10/1.76 inference(NNF_transformation,[status(thm)],[f224])).
% 10.10/1.76 fof(f226,plain,(
% 10.10/1.76 (![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))))))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f225])).
% 10.10/1.76 fof(f227,plain,(
% 10.10/1.76 (![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))))))),
% 10.10/1.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(Height,sK10_skl(Time,Fluent,Event))],[f226])).
% 10.10/1.76 fof(f231,plain,(
% 10.10/1.76 ![X0,X1,X2]: (sP0_prd(X0,X1,X2)|~sP2_prd(X1,X2))),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f227])).
% 10.10/1.76 fof(f233,plain,(
% 10.10/1.76 ![Event,Time]: ((~sP1_prd(Time,Event)|(Event=tapOn&Time=n0))&(sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 10.10/1.76 inference(NNF_transformation,[status(thm)],[f132])).
% 10.10/1.76 fof(f234,plain,(
% 10.10/1.76 (![Event,Time]: (~sP1_prd(Time,Event)|(Event=tapOn&Time=n0)))&(![Event,Time]: (sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f233])).
% 10.10/1.76 fof(f236,plain,(
% 10.10/1.76 ![X0,X1]: (~sP1_prd(X0,X1)|X0=n0)),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f234])).
% 10.10/1.76 fof(f237,plain,(
% 10.10/1.76 ![X0,X1]: (sP1_prd(X0,X1)|~X1=tapOn|~X0=n0)),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f234])).
% 10.10/1.76 fof(f238,plain,(
% 10.10/1.76 ![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))))),
% 10.10/1.76 inference(NNF_transformation,[status(thm)],[f223])).
% 10.10/1.76 fof(f239,plain,(
% 10.10/1.76 (![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))))),
% 10.10/1.76 inference(miniscoping,[status(thm)],[f238])).
% 10.10/1.76 fof(f244,plain,(
% 10.10/1.76 ![X0,X1]: (sP2_prd(X0,X1)|~X1=tapOn|~X0=filling)),
% 10.10/1.76 inference(cnf_transformation,[status(thm)],[f239])).
% 10.10/1.76 fof(f250,plain,(
% 10.10/1.76 ![X0,X1]: (releases(tapOn,waterLevel(X0),X1))),
% 10.10/1.76 inference(destructive_equality_resolution,[status(thm)],[f131])).
% 10.10/1.76 fof(f252,plain,(
% 10.10/1.76 ![X0,X1,X2]: (~holdsAt(waterLevel(X0),X1)|trajectory(filling,X1,waterLevel(plus(X0,X2)),X2))),
% 10.10/1.76 inference(destructive_equality_resolution,[status(thm)],[f143])).
% 10.10/1.76 fof(f253,plain,(
% 10.10/1.76 ![X0]: (less_or_equal(X0,X0))),
% 10.10/1.76 inference(destructive_equality_resolution,[status(thm)],[f172])).
% 10.10/1.76 fof(f256,plain,(
% 10.10/1.76 sP1_prd(n0,tapOn)),
% 10.10/1.76 inference(destructive_equality_resolution,[status(thm)],[f237])).
% 10.10/1.76 fof(f257,plain,(
% 10.10/1.76 sP2_prd(filling,tapOn)),
% 10.10/1.76 inference(destructive_equality_resolution,[status(thm)],[f244])).
% 10.10/1.76 fof(f261,plain,(
% 10.10/1.76 less(n2,n3)),
% 10.10/1.76 inference(resolution,[status(thm)],[f253,f186])).
% 10.10/1.76 fof(f262,plain,(
% 10.10/1.76 less(n1,n2)),
% 10.10/1.76 inference(resolution,[status(thm)],[f253,f182])).
% 10.10/1.76 fof(f294,plain,(
% 10.10/1.76 ![X0,X1]: (sK7_skl(X0,X1)=tapOn|releasedAt(X1,X0)|~releasedAt(X1,plus(X0,n1)))),
% 10.10/1.76 inference(resolution,[status(thm)],[f129,f94])).
% 10.10/1.76 fof(f295,plain,(
% 10.10/1.76 ![X0,X1]: (X0=waterLevel(sK9_skl(X0,sK7_skl(X1,X0)))|releasedAt(X0,X1)|~releasedAt(X0,plus(X1,n1)))),
% 10.10/1.76 inference(resolution,[status(thm)],[f130,f94])).
% 10.10/1.76 fof(f298,plain,(
% 10.10/1.76 ![X0,X1]: (~happens(tapOn,X0)|releasedAt(waterLevel(X1),plus(X0,n1)))),
% 10.10/1.76 inference(resolution,[status(thm)],[f250,f103])).
% 10.10/1.76 fof(f330,plain,(
% 10.10/1.76 ![X0,X1,X2]: (~happens(X0,X1)|~initiates(X0,X2,X1)|~releasedAt(X2,plus(n1,X1)))),
% 10.10/1.76 inference(paramodulation,[status(thm)],[f167,f106])).
% 10.10/1.76 fof(f349,plain,(
% 10.10/1.76 ~less(n3,n2)),
% 10.10/1.76 inference(resolution,[status(thm)],[f213,f261])).
% 10.10/1.76 fof(f359,plain,(
% 10.10/1.76 ![X0]: (~less(X0,n1)|less(X0,n0)|X0=n0)),
% 10.10/1.76 inference(resolution,[status(thm)],[f177,f170])).
% 10.10/1.76 fof(f360,plain,(
% 10.10/1.76 ![X0]: (~less(X0,n1)|X0=n0)),
% 10.10/1.76 inference(forward_subsumption_resolution,[status(thm)],[f359,f174])).
% 10.10/1.76 fof(f363,plain,(
% 10.10/1.76 less(n0,n1)),
% 10.10/1.76 inference(resolution,[status(thm)],[f178,f253])).
% 10.10/1.76 fof(f486,plain,(
% 10.10/1.76 ![X0]: (trajectory(filling,n0,waterLevel(plus(n0,X0)),X0))),
% 10.10/1.76 inference(resolution,[status(thm)],[f216,f252])).
% 10.10/1.76 fof(f548,plain,(
% 10.10/1.76 ![X0]: (sP0_prd(X0,filling,tapOn))),
% 10.10/1.76 inference(resolution,[status(thm)],[f231,f257])).
% 10.10/1.76 fof(f686,plain,(
% 10.10/1.76 ![X0]: (initiates(tapOn,filling,X0))),
% 10.10/1.76 inference(resolution,[status(thm)],[f548,f116])).
% 10.10/1.76 fof(f735,plain,(
% 10.10/1.76 ![X0]: (~happens(tapOn,X0)|holdsAt(filling,plus(X0,n1)))),
% 10.10/1.76 inference(resolution,[status(thm)],[f686,f97])).
% 10.10/1.76 fof(f738,plain,(
% 10.10/1.76 ![X0]: (sK7_skl(n0,X0)=tapOn|releasedAt(X0,n0)|~releasedAt(X0,n1))),
% 10.10/1.76 inference(paramodulation,[status(thm)],[f158,f294])).
% 10.10/1.76 fof(f741,plain,(
% 10.10/1.76 ![X0]: (X0=waterLevel(sK9_skl(X0,sK7_skl(n1,X0)))|releasedAt(X0,n1)|~releasedAt(X0,n2))),
% 10.10/1.76 inference(paramodulation,[status(thm)],[f161,f295])).
% 10.10/1.76 fof(f760,plain,(
% 10.10/1.76 ![X0,X1]: (releasedAt(waterLevel(X0),plus(X1,n1))|~sP1_prd(X1,tapOn))),
% 10.10/1.76 inference(resolution,[status(thm)],[f298,f139])).
% 10.10/1.76 fof(f857,plain,(
% 10.10/1.76 ![X0,X1]: (sK1_skl(n1,X0,X1)=n0|~stoppedIn(X1,X0,n1))),
% 10.10/1.76 inference(resolution,[status(thm)],[f360,f62])).
% 10.10/1.76 fof(f984,plain,(
% 10.10/1.76 ![X0]: (~happens(tapOn,X0)|~releasedAt(filling,plus(n1,X0)))),
% 10.10/1.76 inference(resolution,[status(thm)],[f330,f686])).
% 10.10/1.76 fof(f1394,plain,(
% 10.10/1.76 trajectory(filling,n0,waterLevel(n1),n1)),
% 10.10/1.76 inference(paramodulation,[status(thm)],[f158,f486])).
% 10.10/1.76 fof(f1748,plain,(
% 10.10/1.76 ![X0]: (releasedAt(waterLevel(X0),plus(n0,n1)))),
% 10.10/1.76 inference(resolution,[status(thm)],[f760,f256])).
% 10.10/1.76 fof(f1749,plain,(
% 10.10/1.76 ![X0]: (releasedAt(waterLevel(X0),n1))),
% 10.10/1.76 inference(forward_demodulation,[status(thm)],[f158,f1748])).
% 10.10/1.76 fof(f1775,plain,(
% 10.10/1.76 ![X0]: (sK7_skl(n0,waterLevel(X0))=tapOn|releasedAt(waterLevel(X0),n0))),
% 10.10/1.76 inference(resolution,[status(thm)],[f1749,f738])).
% 10.10/1.76 fof(f1781,plain,(
% 10.10/1.76 ![X0]: (sK7_skl(n0,waterLevel(X0))=tapOn)),
% 10.10/1.76 inference(forward_subsumption_resolution,[status(thm)],[f1775,f219])).
% 10.10/1.76 fof(f1790,plain,(
% 10.10/1.76 ![X0]: (releasedAt(waterLevel(X0),n0)|happens(tapOn,n0)|~releasedAt(waterLevel(X0),plus(n0,n1)))),
% 10.10/1.76 inference(paramodulation,[status(thm)],[f1781,f93])).
% 10.10/1.76 fof(f1796,plain,(
% 10.10/1.76 ![X0]: (releasedAt(waterLevel(X0),n0)|happens(tapOn,n0)|~releasedAt(waterLevel(X0),n1))),
% 10.10/1.76 inference(forward_demodulation,[status(thm)],[f158,f1790])).
% 10.10/1.76 fof(f1797,plain,(
% 10.10/1.76 ![X0]: (happens(tapOn,n0)|~releasedAt(waterLevel(X0),n1))),
% 10.10/1.76 inference(forward_subsumption_resolution,[status(thm)],[f1796,f219])).
% 10.10/1.76 fof(f2571,plain,(
% 10.10/1.76 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n1)|stoppedIn(n0,filling,plus(n0,n1))|holdsAt(waterLevel(n1),plus(n0,n1)))),
% 10.10/1.76 inference(resolution,[status(thm)],[f1394,f75])).
% 10.10/1.76 fof(f2572,plain,(
% 10.10/1.76 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n1)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),plus(n0,n1)))),
% 10.10/1.76 inference(forward_demodulation,[status(thm)],[f158,f2571])).
% 10.10/1.76 fof(f2573,plain,(
% 10.10/1.76 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n1)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1))),
% 10.10/1.76 inference(forward_demodulation,[status(thm)],[f158,f2572])).
% 10.10/1.76 fof(f2574,plain,(
% 10.10/1.76 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1))),
% 10.10/1.76 inference(forward_subsumption_resolution,[status(thm)],[f2573,f363])).
% 10.10/1.76 fof(f2750,plain,(
% 10.10/1.76 happens(tapOn,n0)),
% 10.10/1.76 inference(forward_subsumption_resolution,[status(thm)],[f1797,f1749])).
% 10.10/1.76 fof(f2752,plain,(
% 10.10/1.76 ~releasedAt(filling,plus(n1,n0))),
% 10.10/1.76 inference(resolution,[status(thm)],[f2750,f984])).
% 10.10/1.76 fof(f2753,plain,(
% 10.10/1.76 holdsAt(filling,plus(n0,n1))),
% 10.10/1.76 inference(resolution,[status(thm)],[f2750,f735])).
% 10.10/1.76 fof(f2766,plain,(
% 10.10/1.76 holdsAt(filling,n1)),
% 10.10/1.76 inference(forward_demodulation,[status(thm)],[f158,f2753])).
% 10.10/1.76 fof(f2777,plain,(
% 10.10/1.78 releasedAt(filling,plus(n1,n1))|happens(sK4_skl(n1,filling),n1)|holdsAt(filling,plus(n1,n1))),
% 10.10/1.78 inference(resolution,[status(thm)],[f2766,f81])).
% 10.10/1.78 fof(f2785,plain,(
% 10.10/1.78 releasedAt(filling,n2)|happens(sK4_skl(n1,filling),n1)|holdsAt(filling,plus(n1,n1))),
% 10.10/1.78 inference(forward_demodulation,[status(thm)],[f161,f2777])).
% 10.10/1.78 fof(f2786,plain,(
% 10.10/1.78 releasedAt(filling,n2)|happens(sK4_skl(n1,filling),n1)|holdsAt(filling,n2)),
% 10.10/1.78 inference(forward_demodulation,[status(thm)],[f161,f2785])).
% 10.10/1.78 fof(f2787,plain,(
% 10.10/1.78 releasedAt(filling,n2)|happens(sK4_skl(n1,filling),n1)),
% 10.10/1.78 inference(forward_subsumption_resolution,[status(thm)],[f2786,f222])).
% 10.10/1.78 fof(f2802,plain,(
% 10.10/1.78 releasedAt(filling,n2)|sP1_prd(n1,sK4_skl(n1,filling))|sK4_skl(n1,filling)=overflow),
% 10.10/1.78 inference(resolution,[status(thm)],[f2787,f138])).
% 10.10/1.78 fof(f2934,plain,(
% 10.10/1.78 ~releasedAt(filling,plus(n0,n1))),
% 10.10/1.78 inference(paramodulation,[status(thm)],[f167,f2752])).
% 10.10/1.78 fof(f2936,plain,(
% 10.10/1.78 ~releasedAt(filling,n1)),
% 10.10/1.78 inference(forward_demodulation,[status(thm)],[f158,f2934])).
% 10.10/1.78 fof(f3056,plain,(
% 10.10/1.78 releasedAt(filling,n2)|sK4_skl(n1,filling)=overflow|n1=n0),
% 10.10/1.78 inference(resolution,[status(thm)],[f2802,f236])).
% 10.10/1.78 fof(f3097,plain,(
% 10.10/1.78 sK4_skl(n1,filling)=overflow|n1=n0|filling=waterLevel(sK9_skl(filling,sK7_skl(n1,filling)))|releasedAt(filling,n1)),
% 10.10/1.78 inference(resolution,[status(thm)],[f3056,f741])).
% 10.10/1.78 fof(f3107,plain,(
% 10.10/1.78 sK4_skl(n1,filling)=overflow|n1=n0|releasedAt(filling,n1)),
% 10.10/1.78 inference(forward_subsumption_resolution,[status(thm)],[f3097,f150])).
% 10.10/1.78 fof(f3243,plain,(
% 10.10/1.78 sK4_skl(n1,filling)=overflow|n1=n0),
% 10.10/1.78 inference(forward_subsumption_resolution,[status(thm)],[f3107,f2936])).
% 10.10/1.78 fof(f3252,plain,(
% 10.10/1.78 releasedAt(filling,n2)|happens(overflow,n1)|n1=n0),
% 10.10/1.78 inference(paramodulation,[status(thm)],[f3243,f2787])).
% 10.10/1.78 fof(f3279,plain,(
% 10.10/1.78 happens(overflow,n1)|n1=n0|filling=waterLevel(sK9_skl(filling,sK7_skl(n1,filling)))|releasedAt(filling,n1)),
% 10.10/1.78 inference(resolution,[status(thm)],[f3252,f741])).
% 10.10/1.78 fof(f3289,plain,(
% 10.10/1.78 happens(overflow,n1)|n1=n0|releasedAt(filling,n1)),
% 10.10/1.78 inference(forward_subsumption_resolution,[status(thm)],[f3279,f150])).
% 10.10/1.78 fof(f3291,plain,(
% 10.10/1.78 happens(overflow,n1)|n1=n0),
% 10.10/1.78 inference(forward_subsumption_resolution,[status(thm)],[f3289,f2936])).
% 10.10/1.78 fof(f3305,plain,(
% 10.10/1.78 n1=n0|sP1_prd(n1,overflow)|holdsAt(waterLevel(n3),n1)),
% 10.10/1.78 inference(resolution,[status(thm)],[f3291,f136])).
% 10.10/1.78 fof(f3311,plain,(
% 10.10/1.78 n1=n0|holdsAt(waterLevel(n3),n1)),
% 10.10/1.78 inference(forward_subsumption_resolution,[status(thm)],[f3305,f236])).
% 10.10/1.78 fof(f3375,plain,(
% 10.10/1.78 ![X0]: (n1=n0|~holdsAt(waterLevel(X0),n1)|X0=n3)),
% 10.10/1.78 inference(resolution,[status(thm)],[f3311,f146])).
% 10.10/1.78 fof(f4838,plain,(
% 10.10/1.78 ~happens(tapOn,n0)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)),
% 10.10/1.78 inference(resolution,[status(thm)],[f2574,f686])).
% 10.10/1.78 fof(f4840,plain,(
% 10.10/1.78 stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)),
% 10.10/1.78 inference(forward_subsumption_resolution,[status(thm)],[f4838,f2750])).
% 10.10/1.78 fof(f4875,plain,(
% 10.10/1.78 stoppedIn(n0,filling,n1)|n1=n0|n1=n3),
% 10.10/1.78 inference(resolution,[status(thm)],[f4840,f3375])).
% 10.10/1.78 fof(f4891,plain,(
% 10.10/1.78 n1=n0|n1=n3|sK1_skl(n1,filling,n0)=n0),
% 10.10/1.78 inference(resolution,[status(thm)],[f4875,f857])).
% 10.10/1.78 fof(f5295,plain,(
% 10.10/1.78 ~stoppedIn(n0,filling,n1)|less(n0,n0)|n1=n0|n1=n3),
% 10.10/1.78 inference(paramodulation,[status(thm)],[f4891,f61])).
% 10.10/1.78 fof(f5302,plain,(
% 10.10/1.78 less(n0,n0)|n1=n0|n1=n3),
% 10.10/1.78 inference(forward_subsumption_resolution,[status(thm)],[f5295,f4875])).
% 10.10/1.78 fof(f5304,plain,(
% 10.10/1.78 n1=n0|n1=n3),
% 10.10/1.78 inference(forward_subsumption_resolution,[status(thm)],[f5302,f174])).
% 10.10/1.78 fof(f5404,plain,(
% 10.10/1.78 ~less(n1,n2)|n1=n0),
% 10.10/1.78 inference(paramodulation,[status(thm)],[f5304,f349])).
% 10.10/1.78 fof(f5446,plain,(
% 10.10/1.78 n1=n0),
% 10.10/1.78 inference(forward_subsumption_resolution,[status(thm)],[f5404,f262])).
% 10.10/1.78 fof(f5622,plain,(
% 10.10/1.78 holdsAt(filling,n0)),
% 10.10/1.78 inference(backward_demodulation,[status(thm)],[f5446,f2766])).
% 10.10/1.78 fof(f5976,plain,(
% 10.10/1.78 $false),
% 10.10/1.78 inference(forward_subsumption_resolution,[status(thm)],[f5622,f217])).
% 10.10/1.78 % SZS output end CNFRefutation for theBenchmark.p
% 10.10/1.79 % Elapsed time: 1.409361 seconds
% 10.10/1.79 % CPU time: 10.796416 seconds
% 10.10/1.79 % Total memory used: 203.465 MB
% 10.10/1.79 % Net memory used: 193.024 MB
%------------------------------------------------------------------------------