%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR007+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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 103.05s 13.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR007+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n016.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 14:28:23 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.46 % Drodi V4.1.1
% 103.05/13.57 % Refutation found
% 103.05/13.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 103.05/13.57 % SZS output start CNFRefutation for theBenchmark
% 103.05/13.57 fof(f1,axiom,(
% 103.05/13.57 (! [Time1,Fluent,Time2] :( stoppedIn(Time1,Fluent,Time2)<=> (? [Event,Time] :( happens(Event,Time)& less(Time1,Time)& less(Time,Time2)& terminates(Event,Fluent,Time) ) )) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f3,axiom,(
% 103.05/13.57 (! [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)) ) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f9,axiom,(
% 103.05/13.57 (! [Event,Time,Fluent] :( ( happens(Event,Time)& initiates(Event,Fluent,Time) )=> holdsAt(Fluent,plus(Time,n1)) ) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f10,axiom,(
% 103.05/13.57 (! [Event,Time,Fluent] :( ( happens(Event,Time)& terminates(Event,Fluent,Time) )=> ~ holdsAt(Fluent,plus(Time,n1)) ) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f13,axiom,(
% 103.05/13.57 (! [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) ) )) ) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f16,axiom,(
% 103.05/13.57 (! [Event,Time] :( happens(Event,Time)<=> ( ( Event = tapOn& Time = n0 )| ( holdsAt(waterLevel(n3),Time)& holdsAt(filling,Time)& Event = overflow ) ) ) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f17,axiom,(
% 103.05/13.57 (! [Height1,Time,Height2,Offset] :( ( holdsAt(waterLevel(Height1),Time)& Height2 = plus(Height1,Offset) )=> trajectory(filling,Time,waterLevel(Height2),Offset) ) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f18,axiom,(
% 103.05/13.57 (! [Time,Height1,Height2] :( ( holdsAt(waterLevel(Height1),Time)& holdsAt(waterLevel(Height2),Time) )=> Height1 = Height2 ) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f21,axiom,(
% 103.05/13.57 overflow != tapOn ),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f27,axiom,(
% 103.05/13.57 plus(n0,n1) = n1 ),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f28,axiom,(
% 103.05/13.57 plus(n0,n2) = n2 ),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f37,axiom,(
% 103.05/13.57 (! [X,Y] :( less_or_equal(X,Y)<=> ( less(X,Y)| X = Y ) ) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f38,axiom,(
% 103.05/13.57 ~ (? [X] : less(X,n0) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f39,axiom,(
% 103.05/13.57 (! [X] :( less(X,n1)<=> less_or_equal(X,n0) ) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f40,axiom,(
% 103.05/13.57 (! [X] :( less(X,n2)<=> less_or_equal(X,n1) ) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f41,axiom,(
% 103.05/13.57 (! [X] :( less(X,n3)<=> less_or_equal(X,n2) ) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f48,axiom,(
% 103.05/13.57 (! [X,Y] :( less(X,Y)<=> ( ~ less(Y,X)& Y != X ) ) )),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f49,hypothesis,(
% 103.05/13.57 holdsAt(waterLevel(n0),n0) ),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f50,hypothesis,(
% 103.05/13.57 ~ holdsAt(filling,n0) ),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f55,conjecture,(
% 103.05/13.57 ~ holdsAt(waterLevel(n3),n2) ),
% 103.05/13.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 103.05/13.57 fof(f56,negated_conjecture,(
% 103.05/13.57 ~(~ holdsAt(waterLevel(n3),n2) )),
% 103.05/13.57 inference(negated_conjecture,[status(cth)],[f55])).
% 103.05/13.57 fof(f57,plain,(
% 103.05/13.57 ![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)))))),
% 103.05/13.57 inference(NNF_transformation,[status(thm)],[f1])).
% 103.05/13.57 fof(f58,plain,(
% 103.05/13.57 (![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)))))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f57])).
% 103.05/13.57 fof(f59,plain,(
% 103.05/13.57 (![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)))))),
% 103.05/13.57 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])).
% 103.05/13.57 fof(f60,plain,(
% 103.05/13.57 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|happens(sK0_skl(X2,X1,X0),sK1_skl(X2,X1,X0)))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f59])).
% 103.05/13.57 fof(f61,plain,(
% 103.05/13.57 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|less(X0,sK1_skl(X2,X1,X0)))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f59])).
% 103.05/13.57 fof(f62,plain,(
% 103.05/13.57 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|less(sK1_skl(X2,X1,X0),X2))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f59])).
% 103.05/13.57 fof(f63,plain,(
% 103.05/13.57 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|terminates(sK0_skl(X2,X1,X0),X1,sK1_skl(X2,X1,X0)))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f59])).
% 103.05/13.57 fof(f73,plain,(
% 103.05/13.57 ![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)))),
% 103.05/13.57 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 103.05/13.57 fof(f74,plain,(
% 103.05/13.57 ![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)))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f73])).
% 103.05/13.57 fof(f75,plain,(
% 103.05/13.57 ![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)))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f74])).
% 103.05/13.57 fof(f95,plain,(
% 103.05/13.57 ![Event,Time,Fluent]: ((~happens(Event,Time)|~initiates(Event,Fluent,Time))|holdsAt(Fluent,plus(Time,n1)))),
% 103.05/13.57 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 103.05/13.57 fof(f96,plain,(
% 103.05/13.57 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~initiates(Event,Fluent,Time)))|holdsAt(Fluent,plus(Time,n1)))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f95])).
% 103.05/13.57 fof(f97,plain,(
% 103.05/13.57 ![X0,X1,X2]: (~happens(X0,X1)|~initiates(X0,X2,X1)|holdsAt(X2,plus(X1,n1)))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f96])).
% 103.05/13.57 fof(f98,plain,(
% 103.05/13.57 ![Event,Time,Fluent]: ((~happens(Event,Time)|~terminates(Event,Fluent,Time))|~holdsAt(Fluent,plus(Time,n1)))),
% 103.05/13.57 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 103.05/13.57 fof(f99,plain,(
% 103.05/13.57 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~terminates(Event,Fluent,Time)))|~holdsAt(Fluent,plus(Time,n1)))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f98])).
% 103.05/13.57 fof(f100,plain,(
% 103.05/13.57 ![X0,X1,X2]: (~happens(X0,X1)|~terminates(X0,X2,X1)|~holdsAt(X2,plus(X1,n1)))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f99])).
% 103.05/13.57 fof(f108,definition,(
% 103.05/13.57 ![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)))))),
% 103.05/13.57 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 103.05/13.57 fof(f109,plain,(
% 103.05/13.57 ![Event,Fluent,Time]: (initiates(Event,Fluent,Time)<=>(sP0_prd(Time,Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=overflow)&Fluent=waterLevel(Height)))))),
% 103.05/13.57 inference(formula_renaming,[status(thm)],[f13,f108])).
% 103.05/13.57 fof(f110,plain,(
% 103.05/13.57 ![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))))))),
% 103.05/13.57 inference(NNF_transformation,[status(thm)],[f109])).
% 103.05/13.57 fof(f111,plain,(
% 103.05/13.57 (![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))))))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f110])).
% 103.05/13.57 fof(f112,plain,(
% 103.05/13.57 (![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))))))),
% 103.05/13.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(Height,sK8_skl(Time,Fluent,Event))],[f111])).
% 103.05/13.57 fof(f116,plain,(
% 103.05/13.57 ![X0,X1,X2]: (initiates(X0,X1,X2)|~sP0_prd(X2,X1,X0))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f112])).
% 103.05/13.57 fof(f132,definition,(
% 103.05/13.57 ![Event,Time]: (sP1_prd(Time,Event)<=>(Event=tapOn&Time=n0))),
% 103.05/13.57 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 103.05/13.57 fof(f133,plain,(
% 103.05/13.57 ![Event,Time]: (happens(Event,Time)<=>(sP1_prd(Time,Event)|((holdsAt(waterLevel(n3),Time)&holdsAt(filling,Time))&Event=overflow)))),
% 103.05/13.57 inference(formula_renaming,[status(thm)],[f16,f132])).
% 103.05/13.57 fof(f134,plain,(
% 103.05/13.57 ![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))))),
% 103.05/13.57 inference(NNF_transformation,[status(thm)],[f133])).
% 103.05/13.57 fof(f135,plain,(
% 103.05/13.57 (![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))))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f134])).
% 103.05/13.57 fof(f136,plain,(
% 103.05/13.57 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|holdsAt(waterLevel(n3),X1))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f135])).
% 103.05/13.57 fof(f137,plain,(
% 103.05/13.57 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|holdsAt(filling,X1))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f135])).
% 103.05/13.57 fof(f138,plain,(
% 103.05/13.57 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|X0=overflow)),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f135])).
% 103.05/13.57 fof(f139,plain,(
% 103.05/13.57 ![X0,X1]: (happens(X0,X1)|~sP1_prd(X1,X0))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f135])).
% 103.05/13.57 fof(f141,plain,(
% 103.05/13.57 ![Height1,Time,Height2,Offset]: ((~holdsAt(waterLevel(Height1),Time)|~Height2=plus(Height1,Offset))|trajectory(filling,Time,waterLevel(Height2),Offset))),
% 103.05/13.57 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 103.05/13.57 fof(f142,plain,(
% 103.05/13.57 ![Time,Height2,Offset]: ((![Height1]: (~holdsAt(waterLevel(Height1),Time)|~Height2=plus(Height1,Offset)))|trajectory(filling,Time,waterLevel(Height2),Offset))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f141])).
% 103.05/13.57 fof(f143,plain,(
% 103.05/13.57 ![X0,X1,X2,X3]: (~holdsAt(waterLevel(X0),X1)|~X2=plus(X0,X3)|trajectory(filling,X1,waterLevel(X2),X3))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f142])).
% 103.05/13.57 fof(f144,plain,(
% 103.05/13.57 ![Time,Height1,Height2]: ((~holdsAt(waterLevel(Height1),Time)|~holdsAt(waterLevel(Height2),Time))|Height1=Height2)),
% 103.05/13.57 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 103.05/13.57 fof(f145,plain,(
% 103.05/13.57 ![Height1,Height2]: ((![Time]: (~holdsAt(waterLevel(Height1),Time)|~holdsAt(waterLevel(Height2),Time)))|Height1=Height2)),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f144])).
% 103.05/13.57 fof(f146,plain,(
% 103.05/13.57 ![X0,X1,X2]: (~holdsAt(waterLevel(X0),X1)|~holdsAt(waterLevel(X2),X1)|X0=X2)),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f145])).
% 103.05/13.57 fof(f149,plain,(
% 103.05/13.57 ~overflow=tapOn),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f21])).
% 103.05/13.57 fof(f158,plain,(
% 103.05/13.57 plus(n0,n1)=n1),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f27])).
% 103.05/13.57 fof(f159,plain,(
% 103.05/13.57 plus(n0,n2)=n2),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f28])).
% 103.05/13.57 fof(f168,plain,(
% 103.05/13.57 ![X,Y]: ((~less_or_equal(X,Y)|(less(X,Y)|X=Y))&(less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 103.05/13.57 inference(NNF_transformation,[status(thm)],[f37])).
% 103.05/13.57 fof(f169,plain,(
% 103.05/13.57 (![X,Y]: (~less_or_equal(X,Y)|(less(X,Y)|X=Y)))&(![X,Y]: (less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f168])).
% 103.05/13.57 fof(f170,plain,(
% 103.05/13.57 ![X0,X1]: (~less_or_equal(X0,X1)|less(X0,X1)|X0=X1)),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f169])).
% 103.05/13.57 fof(f171,plain,(
% 103.05/13.57 ![X0,X1]: (less_or_equal(X0,X1)|~less(X0,X1))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f169])).
% 103.05/13.57 fof(f172,plain,(
% 103.05/13.57 ![X0,X1]: (less_or_equal(X0,X1)|~X0=X1)),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f169])).
% 103.05/13.57 fof(f173,plain,(
% 103.05/13.57 (![X]: ~less(X,n0))),
% 103.05/13.57 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 103.05/13.57 fof(f174,plain,(
% 103.05/13.57 ![X0]: (~less(X0,n0))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f173])).
% 103.05/13.57 fof(f175,plain,(
% 103.05/13.57 ![X]: ((~less(X,n1)|less_or_equal(X,n0))&(less(X,n1)|~less_or_equal(X,n0)))),
% 103.05/13.57 inference(NNF_transformation,[status(thm)],[f39])).
% 103.05/13.57 fof(f176,plain,(
% 103.05/13.57 (![X]: (~less(X,n1)|less_or_equal(X,n0)))&(![X]: (less(X,n1)|~less_or_equal(X,n0)))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f175])).
% 103.05/13.57 fof(f177,plain,(
% 103.05/13.57 ![X0]: (~less(X0,n1)|less_or_equal(X0,n0))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f176])).
% 103.05/13.57 fof(f178,plain,(
% 103.05/13.57 ![X0]: (less(X0,n1)|~less_or_equal(X0,n0))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f176])).
% 103.05/13.57 fof(f179,plain,(
% 103.05/13.57 ![X]: ((~less(X,n2)|less_or_equal(X,n1))&(less(X,n2)|~less_or_equal(X,n1)))),
% 103.05/13.57 inference(NNF_transformation,[status(thm)],[f40])).
% 103.05/13.57 fof(f180,plain,(
% 103.05/13.57 (![X]: (~less(X,n2)|less_or_equal(X,n1)))&(![X]: (less(X,n2)|~less_or_equal(X,n1)))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f179])).
% 103.05/13.57 fof(f181,plain,(
% 103.05/13.57 ![X0]: (~less(X0,n2)|less_or_equal(X0,n1))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f180])).
% 103.05/13.57 fof(f182,plain,(
% 103.05/13.57 ![X0]: (less(X0,n2)|~less_or_equal(X0,n1))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f180])).
% 103.05/13.57 fof(f183,plain,(
% 103.05/13.57 ![X]: ((~less(X,n3)|less_or_equal(X,n2))&(less(X,n3)|~less_or_equal(X,n2)))),
% 103.05/13.57 inference(NNF_transformation,[status(thm)],[f41])).
% 103.05/13.57 fof(f184,plain,(
% 103.05/13.57 (![X]: (~less(X,n3)|less_or_equal(X,n2)))&(![X]: (less(X,n3)|~less_or_equal(X,n2)))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f183])).
% 103.05/13.57 fof(f186,plain,(
% 103.05/13.57 ![X0]: (less(X0,n3)|~less_or_equal(X0,n2))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f184])).
% 103.05/13.57 fof(f211,plain,(
% 103.05/13.57 ![X,Y]: ((~less(X,Y)|(~less(Y,X)&~Y=X))&(less(X,Y)|(less(Y,X)|Y=X)))),
% 103.05/13.57 inference(NNF_transformation,[status(thm)],[f48])).
% 103.05/13.57 fof(f212,plain,(
% 103.05/13.57 (![X,Y]: (~less(X,Y)|(~less(Y,X)&~Y=X)))&(![X,Y]: (less(X,Y)|(less(Y,X)|Y=X)))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f211])).
% 103.05/13.57 fof(f214,plain,(
% 103.05/13.57 ![X0,X1]: (~less(X0,X1)|~X1=X0)),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f212])).
% 103.05/13.57 fof(f216,plain,(
% 103.05/13.57 holdsAt(waterLevel(n0),n0)),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f49])).
% 103.05/13.57 fof(f217,plain,(
% 103.05/13.57 ~holdsAt(filling,n0)),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f50])).
% 103.05/13.57 fof(f222,plain,(
% 103.05/13.57 holdsAt(waterLevel(n3),n2)),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f56])).
% 103.05/13.57 fof(f223,definition,(
% 103.05/13.57 ![Event,Fluent]: (sP2_prd(Fluent,Event)<=>((Event=tapOn&Fluent=filling)|(Event=overflow&Fluent=spilling)))),
% 103.05/13.57 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 103.05/13.57 fof(f224,plain,(
% 103.05/13.57 ![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)<=>(sP2_prd(Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=tapOff)&Fluent=waterLevel(Height)))))),
% 103.05/13.57 inference(formula_renaming,[status(thm)],[f108,f223])).
% 103.05/13.57 fof(f225,plain,(
% 103.05/13.57 ![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))))))),
% 103.05/13.57 inference(NNF_transformation,[status(thm)],[f224])).
% 103.05/13.57 fof(f226,plain,(
% 103.05/13.57 (![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))))))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f225])).
% 103.05/13.57 fof(f227,plain,(
% 103.05/13.57 (![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))))))),
% 103.05/13.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(Height,sK10_skl(Time,Fluent,Event))],[f226])).
% 103.05/13.57 fof(f231,plain,(
% 103.05/13.57 ![X0,X1,X2]: (sP0_prd(X0,X1,X2)|~sP2_prd(X1,X2))),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f227])).
% 103.05/13.57 fof(f233,plain,(
% 103.05/13.57 ![Event,Time]: ((~sP1_prd(Time,Event)|(Event=tapOn&Time=n0))&(sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 103.05/13.57 inference(NNF_transformation,[status(thm)],[f132])).
% 103.05/13.57 fof(f234,plain,(
% 103.05/13.57 (![Event,Time]: (~sP1_prd(Time,Event)|(Event=tapOn&Time=n0)))&(![Event,Time]: (sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f233])).
% 103.05/13.57 fof(f235,plain,(
% 103.05/13.57 ![X0,X1]: (~sP1_prd(X0,X1)|X1=tapOn)),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f234])).
% 103.05/13.57 fof(f236,plain,(
% 103.05/13.57 ![X0,X1]: (~sP1_prd(X0,X1)|X0=n0)),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f234])).
% 103.05/13.57 fof(f237,plain,(
% 103.05/13.57 ![X0,X1]: (sP1_prd(X0,X1)|~X1=tapOn|~X0=n0)),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f234])).
% 103.05/13.57 fof(f238,plain,(
% 103.05/13.57 ![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))))),
% 103.05/13.57 inference(NNF_transformation,[status(thm)],[f223])).
% 103.05/13.57 fof(f239,plain,(
% 103.05/13.57 (![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))))),
% 103.05/13.57 inference(miniscoping,[status(thm)],[f238])).
% 103.05/13.57 fof(f244,plain,(
% 103.05/13.57 ![X0,X1]: (sP2_prd(X0,X1)|~X1=tapOn|~X0=filling)),
% 103.05/13.57 inference(cnf_transformation,[status(thm)],[f239])).
% 103.05/13.57 fof(f252,plain,(
% 103.05/13.57 ![X0,X1,X2]: (~holdsAt(waterLevel(X0),X1)|trajectory(filling,X1,waterLevel(plus(X0,X2)),X2))),
% 103.05/13.57 inference(destructive_equality_resolution,[status(thm)],[f143])).
% 103.05/13.57 fof(f253,plain,(
% 103.05/13.57 ![X0]: (less_or_equal(X0,X0))),
% 103.05/13.57 inference(destructive_equality_resolution,[status(thm)],[f172])).
% 103.05/13.57 fof(f254,plain,(
% 103.05/13.57 ![X0]: (~less(X0,X0))),
% 103.05/13.57 inference(destructive_equality_resolution,[status(thm)],[f214])).
% 103.05/13.57 fof(f256,plain,(
% 103.05/13.57 sP1_prd(n0,tapOn)),
% 103.05/13.57 inference(destructive_equality_resolution,[status(thm)],[f237])).
% 103.05/13.57 fof(f257,plain,(
% 103.05/13.57 sP2_prd(filling,tapOn)),
% 103.05/13.57 inference(destructive_equality_resolution,[status(thm)],[f244])).
% 103.05/13.57 fof(f260,plain,(
% 103.05/13.57 ![X0]: (~holdsAt(waterLevel(X0),n2)|X0=n3)),
% 103.05/13.57 inference(resolution,[status(thm)],[f146,f222])).
% 103.05/13.57 fof(f262,plain,(
% 103.05/13.57 less(n1,n2)),
% 103.05/13.57 inference(resolution,[status(thm)],[f253,f182])).
% 103.05/13.57 fof(f265,plain,(
% 103.05/13.57 less(n2,n3)),
% 103.05/13.57 inference(resolution,[status(thm)],[f186,f253])).
% 103.05/13.57 fof(f276,plain,(
% 103.05/13.57 happens(tapOn,n0)),
% 103.05/13.57 inference(resolution,[status(thm)],[f139,f256])).
% 103.05/13.57 fof(f299,plain,(
% 103.05/13.57 ![X0]: (~less(X0,n2)|less(X0,n3))),
% 103.05/13.57 inference(resolution,[status(thm)],[f171,f186])).
% 103.05/13.57 fof(f300,plain,(
% 103.05/13.57 ![X0]: (~less(X0,n1)|less(X0,n2))),
% 103.05/13.57 inference(resolution,[status(thm)],[f171,f182])).
% 103.05/13.57 fof(f328,plain,(
% 103.05/13.57 less(n1,n3)),
% 103.05/13.57 inference(resolution,[status(thm)],[f299,f262])).
% 103.05/13.57 fof(f341,plain,(
% 103.05/13.57 ![X0,X1,X2]: (initiates(X0,X1,X2)|~sP2_prd(X1,X0))),
% 103.05/13.57 inference(resolution,[status(thm)],[f116,f231])).
% 103.05/13.57 fof(f380,plain,(
% 103.05/13.57 ![X0]: (initiates(tapOn,filling,X0))),
% 103.05/13.57 inference(resolution,[status(thm)],[f341,f257])).
% 103.05/13.57 fof(f383,plain,(
% 103.05/13.57 ![X0]: (~happens(tapOn,X0)|holdsAt(filling,plus(X0,n1)))),
% 103.05/13.57 inference(resolution,[status(thm)],[f380,f97])).
% 103.05/13.57 fof(f386,plain,(
% 103.05/13.57 ![X0]: (less(X0,n1)|X0=n1|~less(X0,n2))),
% 103.05/13.57 inference(resolution,[status(thm)],[f170,f181])).
% 103.05/13.57 fof(f389,plain,(
% 103.05/13.57 ![X0]: (~less(X0,n1)|less(X0,n0)|X0=n0)),
% 103.05/13.57 inference(resolution,[status(thm)],[f177,f170])).
% 103.05/13.57 fof(f390,plain,(
% 103.05/13.57 ![X0]: (~less(X0,n1)|X0=n0)),
% 103.05/13.57 inference(forward_subsumption_resolution,[status(thm)],[f389,f174])).
% 103.05/13.57 fof(f391,plain,(
% 103.05/13.57 ![X0,X1]: (sK1_skl(n1,X0,X1)=n0|~stoppedIn(X1,X0,n1))),
% 103.05/13.57 inference(resolution,[status(thm)],[f390,f62])).
% 103.05/13.57 fof(f394,plain,(
% 103.05/13.57 ![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))),
% 103.05/13.57 inference(resolution,[status(thm)],[f100,f63])).
% 103.05/13.57 fof(f395,plain,(
% 103.05/13.57 ![X0,X1,X2]: (~holdsAt(X0,plus(sK1_skl(X1,X0,X2),n1))|~stoppedIn(X2,X0,X1))),
% 103.05/13.57 inference(forward_subsumption_resolution,[status(thm)],[f394,f60])).
% 103.05/13.57 fof(f424,plain,(
% 103.05/13.57 ![X0,X1]: (less(sK1_skl(n2,X0,X1),n1)|sK1_skl(n2,X0,X1)=n1|~stoppedIn(X1,X0,n2))),
% 103.05/13.57 inference(resolution,[status(thm)],[f386,f62])).
% 103.05/13.57 fof(f437,plain,(
% 103.05/13.57 less(n0,n1)),
% 103.05/13.57 inference(resolution,[status(thm)],[f178,f253])).
% 103.05/13.57 fof(f440,plain,(
% 103.05/13.57 less(n0,n2)),
% 103.05/13.57 inference(resolution,[status(thm)],[f437,f300])).
% 103.05/13.57 fof(f563,plain,(
% 103.05/13.57 ![X0,X1]: (~happens(X0,X1)|holdsAt(filling,X1)|X0=tapOn)),
% 103.05/13.57 inference(resolution,[status(thm)],[f137,f235])).
% 103.05/13.57 fof(f591,plain,(
% 103.05/13.57 ![X0,X1]: (~happens(X0,X1)|X0=overflow|X1=n0)),
% 103.05/13.57 inference(resolution,[status(thm)],[f138,f236])).
% 103.05/13.57 fof(f594,plain,(
% 103.05/13.57 ![X0]: (trajectory(filling,n0,waterLevel(plus(n0,X0)),X0))),
% 103.05/13.57 inference(resolution,[status(thm)],[f252,f216])).
% 103.05/13.57 fof(f1165,plain,(
% 103.05/13.57 ![X0,X1,X2]: (sK0_skl(X0,X1,X2)=overflow|sK1_skl(X0,X1,X2)=n0|~stoppedIn(X2,X1,X0))),
% 103.05/13.57 inference(resolution,[status(thm)],[f591,f60])).
% 103.05/13.57 fof(f2210,plain,(
% 103.05/13.57 trajectory(filling,n0,waterLevel(n1),n1)),
% 103.05/13.57 inference(paramodulation,[status(thm)],[f158,f594])).
% 103.05/13.57 fof(f2213,plain,(
% 103.05/13.57 trajectory(filling,n0,waterLevel(n2),n2)),
% 103.05/13.57 inference(paramodulation,[status(thm)],[f159,f594])).
% 103.05/13.57 fof(f2249,plain,(
% 103.05/13.57 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n2)|stoppedIn(n0,filling,plus(n0,n2))|holdsAt(waterLevel(n2),plus(n0,n2)))),
% 103.05/13.57 inference(resolution,[status(thm)],[f2213,f75])).
% 103.05/13.57 fof(f2250,plain,(
% 103.05/13.57 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n2)|stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),plus(n0,n2)))),
% 103.05/13.57 inference(forward_demodulation,[status(thm)],[f159,f2249])).
% 103.05/13.57 fof(f2251,plain,(
% 103.05/13.57 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n2)|stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2))),
% 103.05/13.57 inference(forward_demodulation,[status(thm)],[f159,f2250])).
% 103.05/13.57 fof(f2252,plain,(
% 103.05/13.57 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2))),
% 103.05/13.57 inference(forward_subsumption_resolution,[status(thm)],[f2251,f440])).
% 103.05/13.57 fof(f2306,plain,(
% 103.05/13.57 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n1)|stoppedIn(n0,filling,plus(n0,n1))|holdsAt(waterLevel(n1),plus(n0,n1)))),
% 103.05/13.57 inference(resolution,[status(thm)],[f2210,f75])).
% 103.05/13.57 fof(f2307,plain,(
% 103.05/13.57 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n1)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),plus(n0,n1)))),
% 103.05/13.57 inference(forward_demodulation,[status(thm)],[f158,f2306])).
% 103.05/13.57 fof(f2308,plain,(
% 103.05/13.57 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n1)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1))),
% 103.05/13.57 inference(forward_demodulation,[status(thm)],[f158,f2307])).
% 103.05/13.57 fof(f2309,plain,(
% 103.05/13.57 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1))),
% 103.05/13.57 inference(forward_subsumption_resolution,[status(thm)],[f2308,f437])).
% 103.05/13.57 fof(f2545,plain,(
% 103.05/13.57 ~happens(tapOn,n0)|stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2)),
% 103.05/13.57 inference(resolution,[status(thm)],[f2252,f380])).
% 103.05/13.57 fof(f2547,plain,(
% 103.05/13.57 stoppedIn(n0,filling,n2)|holdsAt(waterLevel(n2),n2)),
% 103.05/13.57 inference(forward_subsumption_resolution,[status(thm)],[f2545,f276])).
% 103.05/13.57 fof(f2573,plain,(
% 103.05/13.57 holdsAt(filling,plus(n0,n1))),
% 103.05/13.57 inference(resolution,[status(thm)],[f383,f276])).
% 103.05/13.57 fof(f2574,plain,(
% 103.05/13.57 holdsAt(filling,n1)),
% 103.05/13.57 inference(forward_demodulation,[status(thm)],[f158,f2573])).
% 103.05/13.57 fof(f3117,plain,(
% 103.05/13.57 stoppedIn(n0,filling,n2)|n2=n3),
% 103.05/13.57 inference(resolution,[status(thm)],[f2547,f260])).
% 103.05/13.57 fof(f3131,plain,(
% 103.05/13.57 n2=n3|less(sK1_skl(n2,filling,n0),n1)|sK1_skl(n2,filling,n0)=n1),
% 103.05/13.57 inference(resolution,[status(thm)],[f3117,f424])).
% 103.05/13.57 fof(f3135,plain,(
% 103.05/13.57 n2=n3|~holdsAt(filling,plus(sK1_skl(n2,filling,n0),n1))),
% 103.05/13.57 inference(resolution,[status(thm)],[f3117,f395])).
% 103.05/13.57 fof(f3940,plain,(
% 103.05/13.57 sK0_skl(n2,filling,n0)=overflow|sK1_skl(n2,filling,n0)=n0|n2=n3),
% 103.05/13.57 inference(resolution,[status(thm)],[f1165,f3117])).
% 103.05/13.57 fof(f5609,plain,(
% 103.05/13.57 n2=n3|~holdsAt(filling,plus(n0,n1))|sK0_skl(n2,filling,n0)=overflow|n2=n3),
% 103.05/13.57 inference(paramodulation,[status(thm)],[f3940,f3135])).
% 103.05/13.57 fof(f5624,plain,(
% 103.05/13.57 n2=n3|~holdsAt(filling,n1)|sK0_skl(n2,filling,n0)=overflow|n2=n3),
% 103.05/13.57 inference(forward_demodulation,[status(thm)],[f158,f5609])).
% 103.05/13.57 fof(f5625,plain,(
% 103.05/13.57 n2=n3|~holdsAt(filling,n1)|sK0_skl(n2,filling,n0)=overflow),
% 103.05/13.57 inference(duplicate_literals_removal,[status(thm)],[f5624])).
% 103.05/13.57 fof(f5626,plain,(
% 103.05/13.57 n2=n3|sK0_skl(n2,filling,n0)=overflow),
% 103.05/13.57 inference(forward_subsumption_resolution,[status(thm)],[f5625,f2574])).
% 103.05/13.57 fof(f5635,plain,(
% 103.05/13.57 ~stoppedIn(n0,filling,n2)|happens(overflow,sK1_skl(n2,filling,n0))|n2=n3),
% 103.05/13.57 inference(paramodulation,[status(thm)],[f5626,f60])).
% 103.05/13.57 fof(f5636,plain,(
% 103.05/13.57 happens(overflow,sK1_skl(n2,filling,n0))|n2=n3),
% 103.05/13.57 inference(forward_subsumption_resolution,[status(thm)],[f5635,f3117])).
% 103.05/13.57 fof(f5640,plain,(
% 103.05/13.57 n2=n3|holdsAt(filling,sK1_skl(n2,filling,n0))|overflow=tapOn),
% 103.05/13.57 inference(resolution,[status(thm)],[f5636,f563])).
% 103.05/13.57 fof(f5644,plain,(
% 103.05/13.57 n2=n3|sP1_prd(sK1_skl(n2,filling,n0),overflow)|holdsAt(waterLevel(n3),sK1_skl(n2,filling,n0))),
% 103.05/13.57 inference(resolution,[status(thm)],[f5636,f136])).
% 103.05/13.57 fof(f5645,plain,(
% 103.05/13.57 n2=n3|holdsAt(filling,sK1_skl(n2,filling,n0))),
% 103.05/13.57 inference(forward_subsumption_resolution,[status(thm)],[f5640,f149])).
% 103.05/13.57 fof(f6277,plain,(
% 103.05/13.57 n2=n3|sK1_skl(n2,filling,n0)=n1|sK1_skl(n2,filling,n0)=n0),
% 103.05/13.57 inference(resolution,[status(thm)],[f3131,f390])).
% 103.05/13.57 fof(f11487,plain,(
% 103.05/13.57 ~happens(tapOn,n0)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)),
% 103.05/13.57 inference(resolution,[status(thm)],[f2309,f380])).
% 103.05/13.57 fof(f11489,plain,(
% 103.05/13.57 stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)),
% 103.05/13.57 inference(forward_subsumption_resolution,[status(thm)],[f11487,f276])).
% 103.05/13.57 fof(f11645,plain,(
% 103.05/13.57 ![X0]: (stoppedIn(n0,filling,n1)|~holdsAt(waterLevel(X0),n1)|X0=n1)),
% 103.05/13.57 inference(resolution,[status(thm)],[f11489,f146])).
% 103.05/13.57 fof(f13190,plain,(
% 103.05/13.57 n2=n3|sP1_prd(sK1_skl(n2,filling,n0),overflow)|holdsAt(waterLevel(n3),n1)|n2=n3|sK1_skl(n2,filling,n0)=n0),
% 103.05/13.57 inference(paramodulation,[status(thm)],[f6277,f5644])).
% 103.05/13.57 fof(f13192,plain,(
% 103.05/13.57 n2=n3|sP1_prd(sK1_skl(n2,filling,n0),overflow)|holdsAt(waterLevel(n3),n1)|sK1_skl(n2,filling,n0)=n0),
% 103.05/13.57 inference(duplicate_literals_removal,[status(thm)],[f13190])).
% 103.05/13.57 fof(f13193,plain,(
% 103.05/13.57 n2=n3|holdsAt(waterLevel(n3),n1)|sK1_skl(n2,filling,n0)=n0),
% 103.05/13.59 inference(forward_subsumption_resolution,[status(thm)],[f13192,f236])).
% 103.05/13.59 fof(f13195,plain,(
% 103.05/13.59 n2=n3|sK1_skl(n2,filling,n0)=n0|stoppedIn(n0,filling,n1)|n3=n1),
% 103.05/13.59 inference(resolution,[status(thm)],[f13193,f11645])).
% 103.05/13.59 fof(f13561,plain,(
% 103.05/13.59 n2=n3|sK1_skl(n2,filling,n0)=n0|n3=n1|sK1_skl(n1,filling,n0)=n0),
% 103.05/13.59 inference(resolution,[status(thm)],[f13195,f391])).
% 103.05/13.59 fof(f17955,plain,(
% 103.05/13.59 n2=n3|holdsAt(filling,n0)|n2=n3|n3=n1|sK1_skl(n1,filling,n0)=n0),
% 103.05/13.59 inference(paramodulation,[status(thm)],[f13561,f5645])).
% 103.05/13.59 fof(f17993,plain,(
% 103.05/13.59 n2=n3|holdsAt(filling,n0)|n3=n1|sK1_skl(n1,filling,n0)=n0),
% 103.05/13.59 inference(duplicate_literals_removal,[status(thm)],[f17955])).
% 103.05/13.59 fof(f17994,plain,(
% 103.05/13.59 n2=n3|n3=n1|sK1_skl(n1,filling,n0)=n0),
% 103.05/13.59 inference(forward_subsumption_resolution,[status(thm)],[f17993,f217])).
% 103.05/13.59 fof(f18016,plain,(
% 103.05/13.59 ~stoppedIn(n0,filling,n1)|less(n0,n0)|n2=n3|n3=n1),
% 103.05/13.59 inference(paramodulation,[status(thm)],[f17994,f61])).
% 103.05/13.59 fof(f18022,plain,(
% 103.05/13.59 n2=n3|sK1_skl(n2,filling,n0)=n0|n3=n1),
% 103.05/13.59 inference(backward_subsumption_resolution,[status(thm)],[f13195,f18023])).
% 81.29/13.67 fof(f18023,plain,(
% 81.29/13.67 ~stoppedIn(n0,filling,n1)|n2=n3|n3=n1),
% 81.29/13.67 inference(forward_subsumption_resolution,[status(thm)],[f18016,f174])).
% 81.29/13.67 fof(f18068,plain,(
% 81.29/13.67 n2=n3|holdsAt(filling,n0)|n2=n3|n3=n1),
% 81.29/13.67 inference(paramodulation,[status(thm)],[f18022,f5645])).
% 81.29/13.67 fof(f18106,plain,(
% 81.29/13.67 n2=n3|holdsAt(filling,n0)|n3=n1),
% 81.29/13.67 inference(duplicate_literals_removal,[status(thm)],[f18068])).
% 81.29/13.67 fof(f18107,plain,(
% 81.29/13.67 n2=n3|n3=n1),
% 81.29/13.67 inference(forward_subsumption_resolution,[status(thm)],[f18106,f217])).
% 81.29/13.67 fof(f18392,plain,(
% 81.29/13.67 less(n3,n3)|n3=n1),
% 81.29/13.67 inference(paramodulation,[status(thm)],[f18107,f265])).
% 81.29/13.67 fof(f18772,plain,(
% 81.29/13.67 less(n1,n1)),
% 81.29/13.67 inference(backward_demodulation,[status(thm)],[f19927,f328])).
% 81.29/13.67 fof(f19927,plain,(
% 81.29/13.67 n3=n1),
% 81.29/13.67 inference(forward_subsumption_resolution,[status(thm)],[f18392,f254])).
% 81.29/13.67 fof(f20625,plain,(
% 81.29/13.67 $false),
% 81.29/13.67 inference(forward_subsumption_resolution,[status(thm)],[f18772,f254])).
% 81.29/13.67 % SZS output end CNFRefutation for theBenchmark.p
% 81.29/13.68 % Elapsed time: 13.226856 seconds
% 81.29/13.68 % CPU time: 104.109184 seconds
% 81.29/13.68 % Total memory used: 457.845 MB
% 81.29/13.68 % Net memory used: 427.596 MB
%------------------------------------------------------------------------------