%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR012+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 : n015.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:35 PM UTC 2026
% Result : Theorem 0.12s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR012+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.07/0.35 % Computer : n015.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 14:27:06 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 0.12/0.49 % Refutation found
% 0.12/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.49 fof(f1,axiom,(
% 0.12/0.49 (! [Time1,Fluent,Time2] :( stoppedIn(Time1,Fluent,Time2)<=> (? [Event,Time] :( happens(Event,Time)& less(Time1,Time)& less(Time,Time2)& terminates(Event,Fluent,Time) ) )) )),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f3,axiom,(
% 0.12/0.49 (! [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)) ) )),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f13,axiom,(
% 0.12/0.49 (! [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) ) )) ) )),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f14,axiom,(
% 0.12/0.49 (! [Event,Fluent,Time] :( terminates(Event,Fluent,Time)<=> ( ( Event = tapOff& Fluent = filling )| ( Event = overflow& Fluent = filling ) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f16,axiom,(
% 0.12/0.49 (! [Event,Time] :( happens(Event,Time)<=> ( ( Event = tapOn& Time = n0 )| ( holdsAt(waterLevel(n3),Time)& holdsAt(filling,Time)& Event = overflow ) ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f17,axiom,(
% 0.12/0.49 (! [Height1,Time,Height2,Offset] :( ( holdsAt(waterLevel(Height1),Time)& Height2 = plus(Height1,Offset) )=> trajectory(filling,Time,waterLevel(Height2),Offset) ) )),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f19,axiom,(
% 0.12/0.49 tapOff != tapOn ),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f21,axiom,(
% 0.12/0.49 overflow != tapOn ),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f27,axiom,(
% 0.12/0.49 plus(n0,n1) = n1 ),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f37,axiom,(
% 0.12/0.49 (! [X,Y] :( less_or_equal(X,Y)<=> ( less(X,Y)| X = Y ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f38,axiom,(
% 0.12/0.49 ~ (? [X] : less(X,n0) )),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f39,axiom,(
% 0.12/0.49 (! [X] :( less(X,n1)<=> less_or_equal(X,n0) ) )),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f48,axiom,(
% 0.12/0.49 (! [X,Y] :( less(X,Y)<=> ( ~ less(Y,X)& Y != X ) ) )),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f49,hypothesis,(
% 0.12/0.49 holdsAt(waterLevel(n0),n0) ),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f50,hypothesis,(
% 0.12/0.49 ~ holdsAt(filling,n0) ),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f55,conjecture,(
% 0.12/0.49 holdsAt(waterLevel(n1),n1) ),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f56,negated_conjecture,(
% 0.12/0.49 ~(holdsAt(waterLevel(n1),n1) )),
% 0.12/0.49 inference(negated_conjecture,[status(cth)],[f55])).
% 0.12/0.49 fof(f57,plain,(
% 0.12/0.49 ![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)))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f1])).
% 0.12/0.49 fof(f58,plain,(
% 0.12/0.49 (![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)))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f57])).
% 0.12/0.49 fof(f59,plain,(
% 0.12/0.49 (![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)))))),
% 0.12/0.49 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])).
% 0.12/0.49 fof(f60,plain,(
% 0.12/0.49 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|happens(sK0_skl(X2,X1,X0),sK1_skl(X2,X1,X0)))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f59])).
% 0.12/0.49 fof(f62,plain,(
% 0.12/0.49 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|less(sK1_skl(X2,X1,X0),X2))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f59])).
% 0.12/0.49 fof(f63,plain,(
% 0.12/0.49 ![X0,X1,X2]: (~stoppedIn(X0,X1,X2)|terminates(sK0_skl(X2,X1,X0),X1,sK1_skl(X2,X1,X0)))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f59])).
% 0.12/0.49 fof(f73,plain,(
% 0.12/0.49 ![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)))),
% 0.12/0.49 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.12/0.49 fof(f74,plain,(
% 0.12/0.49 ![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)))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f73])).
% 0.12/0.49 fof(f75,plain,(
% 0.12/0.49 ![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)))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f74])).
% 0.12/0.49 fof(f108,definition,(
% 0.12/0.49 ![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)))))),
% 0.12/0.49 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.12/0.49 fof(f109,plain,(
% 0.12/0.49 ![Event,Fluent,Time]: (initiates(Event,Fluent,Time)<=>(sP0_prd(Time,Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=overflow)&Fluent=waterLevel(Height)))))),
% 0.12/0.49 inference(formula_renaming,[status(thm)],[f13,f108])).
% 0.12/0.49 fof(f110,plain,(
% 0.12/0.49 ![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))))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f109])).
% 0.12/0.49 fof(f111,plain,(
% 0.12/0.49 (![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))))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f110])).
% 0.12/0.49 fof(f112,plain,(
% 0.12/0.49 (![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))))))),
% 0.12/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(Height,sK8_skl(Time,Fluent,Event))],[f111])).
% 0.12/0.49 fof(f116,plain,(
% 0.12/0.49 ![X0,X1,X2]: (initiates(X0,X1,X2)|~sP0_prd(X2,X1,X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f112])).
% 0.12/0.49 fof(f118,plain,(
% 0.12/0.49 ![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))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f14])).
% 0.12/0.49 fof(f119,plain,(
% 0.12/0.49 (![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))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f118])).
% 0.12/0.49 fof(f120,plain,(
% 0.12/0.49 ![X0,X1,X2]: (~terminates(X0,X1,X2)|X0=tapOff|X0=overflow)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f119])).
% 0.12/0.49 fof(f132,definition,(
% 0.12/0.49 ![Event,Time]: (sP1_prd(Time,Event)<=>(Event=tapOn&Time=n0))),
% 0.12/0.49 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.12/0.49 fof(f133,plain,(
% 0.12/0.49 ![Event,Time]: (happens(Event,Time)<=>(sP1_prd(Time,Event)|((holdsAt(waterLevel(n3),Time)&holdsAt(filling,Time))&Event=overflow)))),
% 0.12/0.49 inference(formula_renaming,[status(thm)],[f16,f132])).
% 0.12/0.49 fof(f134,plain,(
% 0.12/0.49 ![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))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f133])).
% 0.12/0.49 fof(f135,plain,(
% 0.12/0.49 (![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))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f134])).
% 0.12/0.49 fof(f137,plain,(
% 0.12/0.49 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|holdsAt(filling,X1))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f135])).
% 0.12/0.49 fof(f139,plain,(
% 0.12/0.49 ![X0,X1]: (happens(X0,X1)|~sP1_prd(X1,X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f135])).
% 0.12/0.49 fof(f141,plain,(
% 0.12/0.49 ![Height1,Time,Height2,Offset]: ((~holdsAt(waterLevel(Height1),Time)|~Height2=plus(Height1,Offset))|trajectory(filling,Time,waterLevel(Height2),Offset))),
% 0.12/0.49 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.12/0.49 fof(f142,plain,(
% 0.12/0.49 ![Time,Height2,Offset]: ((![Height1]: (~holdsAt(waterLevel(Height1),Time)|~Height2=plus(Height1,Offset)))|trajectory(filling,Time,waterLevel(Height2),Offset))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f141])).
% 0.12/0.49 fof(f143,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (~holdsAt(waterLevel(X0),X1)|~X2=plus(X0,X3)|trajectory(filling,X1,waterLevel(X2),X3))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f142])).
% 0.12/0.49 fof(f147,plain,(
% 0.12/0.49 ~tapOff=tapOn),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f19])).
% 0.12/0.49 fof(f149,plain,(
% 0.12/0.49 ~overflow=tapOn),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f21])).
% 0.12/0.49 fof(f158,plain,(
% 0.12/0.49 plus(n0,n1)=n1),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f27])).
% 0.12/0.49 fof(f168,plain,(
% 0.12/0.49 ![X,Y]: ((~less_or_equal(X,Y)|(less(X,Y)|X=Y))&(less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f37])).
% 0.12/0.49 fof(f169,plain,(
% 0.12/0.49 (![X,Y]: (~less_or_equal(X,Y)|(less(X,Y)|X=Y)))&(![X,Y]: (less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f168])).
% 0.12/0.49 fof(f170,plain,(
% 0.12/0.49 ![X0,X1]: (~less_or_equal(X0,X1)|less(X0,X1)|X0=X1)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f169])).
% 0.12/0.49 fof(f172,plain,(
% 0.12/0.49 ![X0,X1]: (less_or_equal(X0,X1)|~X0=X1)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f169])).
% 0.12/0.49 fof(f173,plain,(
% 0.12/0.49 (![X]: ~less(X,n0))),
% 0.12/0.49 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.12/0.49 fof(f174,plain,(
% 0.12/0.49 ![X0]: (~less(X0,n0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f173])).
% 0.12/0.49 fof(f175,plain,(
% 0.12/0.49 ![X]: ((~less(X,n1)|less_or_equal(X,n0))&(less(X,n1)|~less_or_equal(X,n0)))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f39])).
% 0.12/0.49 fof(f176,plain,(
% 0.12/0.49 (![X]: (~less(X,n1)|less_or_equal(X,n0)))&(![X]: (less(X,n1)|~less_or_equal(X,n0)))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f175])).
% 0.12/0.49 fof(f177,plain,(
% 0.12/0.49 ![X0]: (~less(X0,n1)|less_or_equal(X0,n0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f176])).
% 0.12/0.49 fof(f178,plain,(
% 0.12/0.49 ![X0]: (less(X0,n1)|~less_or_equal(X0,n0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f176])).
% 0.12/0.49 fof(f211,plain,(
% 0.12/0.49 ![X,Y]: ((~less(X,Y)|(~less(Y,X)&~Y=X))&(less(X,Y)|(less(Y,X)|Y=X)))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f48])).
% 0.12/0.49 fof(f212,plain,(
% 0.12/0.49 (![X,Y]: (~less(X,Y)|(~less(Y,X)&~Y=X)))&(![X,Y]: (less(X,Y)|(less(Y,X)|Y=X)))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f211])).
% 0.12/0.49 fof(f213,plain,(
% 0.12/0.49 ![X0,X1]: (~less(X0,X1)|~less(X1,X0))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f212])).
% 0.12/0.49 fof(f215,plain,(
% 0.12/0.49 ![X0,X1]: (less(X0,X1)|less(X1,X0)|X1=X0)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f212])).
% 0.12/0.49 fof(f216,plain,(
% 0.12/0.49 holdsAt(waterLevel(n0),n0)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f49])).
% 0.12/0.49 fof(f217,plain,(
% 0.12/0.49 ~holdsAt(filling,n0)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f50])).
% 0.12/0.49 fof(f222,plain,(
% 0.12/0.49 ~holdsAt(waterLevel(n1),n1)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f56])).
% 0.12/0.49 fof(f223,definition,(
% 0.12/0.49 ![Event,Fluent]: (sP2_prd(Fluent,Event)<=>((Event=tapOn&Fluent=filling)|(Event=overflow&Fluent=spilling)))),
% 0.12/0.49 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.12/0.49 fof(f224,plain,(
% 0.12/0.49 ![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)<=>(sP2_prd(Fluent,Event)|(?[Height]: ((holdsAt(waterLevel(Height),Time)&Event=tapOff)&Fluent=waterLevel(Height)))))),
% 0.12/0.49 inference(formula_renaming,[status(thm)],[f108,f223])).
% 0.12/0.49 fof(f225,plain,(
% 0.12/0.49 ![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))))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f224])).
% 0.12/0.49 fof(f226,plain,(
% 0.12/0.49 (![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))))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f225])).
% 0.12/0.49 fof(f227,plain,(
% 0.12/0.49 (![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))))))),
% 0.12/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(Height,sK10_skl(Time,Fluent,Event))],[f226])).
% 0.12/0.49 fof(f231,plain,(
% 0.12/0.49 ![X0,X1,X2]: (sP0_prd(X0,X1,X2)|~sP2_prd(X1,X2))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f227])).
% 0.12/0.49 fof(f233,plain,(
% 0.12/0.49 ![Event,Time]: ((~sP1_prd(Time,Event)|(Event=tapOn&Time=n0))&(sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f132])).
% 0.12/0.49 fof(f234,plain,(
% 0.12/0.49 (![Event,Time]: (~sP1_prd(Time,Event)|(Event=tapOn&Time=n0)))&(![Event,Time]: (sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f233])).
% 0.12/0.49 fof(f235,plain,(
% 0.12/0.49 ![X0,X1]: (~sP1_prd(X0,X1)|X1=tapOn)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f234])).
% 0.12/0.49 fof(f237,plain,(
% 0.12/0.49 ![X0,X1]: (sP1_prd(X0,X1)|~X1=tapOn|~X0=n0)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f234])).
% 0.12/0.49 fof(f238,plain,(
% 0.12/0.49 ![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))))),
% 0.12/0.49 inference(NNF_transformation,[status(thm)],[f223])).
% 0.12/0.49 fof(f239,plain,(
% 0.12/0.49 (![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))))),
% 0.12/0.49 inference(miniscoping,[status(thm)],[f238])).
% 0.12/0.49 fof(f244,plain,(
% 0.12/0.49 ![X0,X1]: (sP2_prd(X0,X1)|~X1=tapOn|~X0=filling)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f239])).
% 0.12/0.49 fof(f252,plain,(
% 0.12/0.49 ![X0,X1,X2]: (~holdsAt(waterLevel(X0),X1)|trajectory(filling,X1,waterLevel(plus(X0,X2)),X2))),
% 0.12/0.49 inference(destructive_equality_resolution,[status(thm)],[f143])).
% 0.12/0.49 fof(f253,plain,(
% 0.12/0.49 ![X0]: (less_or_equal(X0,X0))),
% 0.12/0.49 inference(destructive_equality_resolution,[status(thm)],[f172])).
% 0.12/0.49 fof(f256,plain,(
% 0.12/0.49 sP1_prd(n0,tapOn)),
% 0.12/0.49 inference(destructive_equality_resolution,[status(thm)],[f237])).
% 0.12/0.49 fof(f257,plain,(
% 0.12/0.49 sP2_prd(filling,tapOn)),
% 0.12/0.49 inference(destructive_equality_resolution,[status(thm)],[f244])).
% 0.12/0.49 fof(f273,plain,(
% 0.12/0.49 ![X0,X1]: (less_or_equal(sK1_skl(n1,X0,X1),n0)|~stoppedIn(X1,X0,n1))),
% 0.12/0.49 inference(resolution,[status(thm)],[f177,f62])).
% 0.12/0.49 fof(f275,plain,(
% 0.12/0.49 less(n0,n1)),
% 0.12/0.49 inference(resolution,[status(thm)],[f178,f253])).
% 0.12/0.49 fof(f284,plain,(
% 0.12/0.49 ![X0,X1]: (~less(X0,X1)|~less_or_equal(X1,X0)|X1=X0)),
% 0.12/0.49 inference(resolution,[status(thm)],[f213,f170])).
% 0.12/0.49 fof(f301,plain,(
% 0.12/0.49 ![X0]: (trajectory(filling,n0,waterLevel(plus(n0,X0)),X0))),
% 0.12/0.49 inference(resolution,[status(thm)],[f216,f252])).
% 0.12/0.49 fof(f310,plain,(
% 0.12/0.49 ![X0,X1]: (X0=tapOn|~happens(X0,X1)|holdsAt(filling,X1))),
% 0.12/0.49 inference(resolution,[status(thm)],[f235,f137])).
% 0.12/0.49 fof(f315,plain,(
% 0.12/0.49 happens(tapOn,n0)),
% 0.12/0.49 inference(resolution,[status(thm)],[f256,f139])).
% 0.12/0.49 fof(f316,plain,(
% 0.12/0.49 ![X0]: (sP0_prd(X0,filling,tapOn))),
% 0.12/0.49 inference(resolution,[status(thm)],[f257,f231])).
% 0.12/0.49 fof(f336,plain,(
% 0.12/0.49 ![X0,X1]: (~less(n0,sK1_skl(n1,X0,X1))|sK1_skl(n1,X0,X1)=n0|~stoppedIn(X1,X0,n1))),
% 0.12/0.49 inference(resolution,[status(thm)],[f284,f273])).
% 0.12/0.49 fof(f352,plain,(
% 0.12/0.49 trajectory(filling,n0,waterLevel(n1),n1)),
% 0.12/0.49 inference(paramodulation,[status(thm)],[f158,f301])).
% 0.12/0.49 fof(f357,plain,(
% 0.12/0.49 ![X0,X1,X2]: (sK0_skl(X0,X1,X2)=tapOn|holdsAt(filling,sK1_skl(X0,X1,X2))|~stoppedIn(X2,X1,X0))),
% 0.12/0.49 inference(resolution,[status(thm)],[f310,f60])).
% 0.12/0.49 fof(f364,plain,(
% 0.12/0.49 ![X0]: (initiates(tapOn,filling,X0))),
% 0.12/0.49 inference(resolution,[status(thm)],[f316,f116])).
% 0.12/0.49 fof(f403,plain,(
% 0.12/0.49 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n1)|stoppedIn(n0,filling,plus(n0,n1))|holdsAt(waterLevel(n1),plus(n0,n1)))),
% 0.12/0.49 inference(resolution,[status(thm)],[f352,f75])).
% 0.12/0.49 fof(f404,plain,(
% 0.12/0.49 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n1)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),plus(n0,n1)))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f158,f403])).
% 0.12/0.49 fof(f405,plain,(
% 0.12/0.49 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|~less(n0,n1)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f158,f404])).
% 0.12/0.49 fof(f406,plain,(
% 0.12/0.49 ![X0]: (~happens(X0,n0)|~initiates(X0,filling,n0)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1))),
% 0.12/0.49 inference(forward_subsumption_resolution,[status(thm)],[f405,f275])).
% 0.12/0.49 fof(f507,plain,(
% 0.12/0.49 ![X0]: (less(n0,X0)|X0=n0)),
% 0.12/0.49 inference(resolution,[status(thm)],[f174,f215])).
% 0.12/0.49 fof(f512,plain,(
% 0.12/0.49 ![X0,X1]: (sK1_skl(n1,X0,X1)=n0|~stoppedIn(X1,X0,n1))),
% 0.12/0.49 inference(backward_subsumption_resolution,[status(thm)],[f336,f507])).
% 0.12/0.49 fof(f746,plain,(
% 0.12/0.49 ~happens(tapOn,n0)|stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)),
% 0.12/0.49 inference(resolution,[status(thm)],[f406,f364])).
% 0.12/0.49 fof(f748,plain,(
% 0.12/0.49 stoppedIn(n0,filling,n1)|holdsAt(waterLevel(n1),n1)),
% 0.12/0.49 inference(forward_subsumption_resolution,[status(thm)],[f746,f315])).
% 0.12/0.49 fof(f751,plain,(
% 0.12/0.49 stoppedIn(n0,filling,n1)),
% 0.12/0.49 inference(resolution,[status(thm)],[f748,f222])).
% 0.12/0.49 fof(f764,plain,(
% 0.12/0.49 sK1_skl(n1,filling,n0)=n0),
% 0.12/0.49 inference(resolution,[status(thm)],[f751,f512])).
% 0.12/0.49 fof(f769,plain,(
% 0.12/0.49 sK0_skl(n1,filling,n0)=tapOn|holdsAt(filling,sK1_skl(n1,filling,n0))),
% 0.12/0.49 inference(resolution,[status(thm)],[f751,f357])).
% 0.12/0.49 fof(f776,plain,(
% 0.12/0.49 sK0_skl(n1,filling,n0)=tapOn|holdsAt(filling,n0)),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f764,f769])).
% 0.12/0.49 fof(f777,plain,(
% 0.12/0.49 sK0_skl(n1,filling,n0)=tapOn),
% 0.12/0.49 inference(forward_subsumption_resolution,[status(thm)],[f776,f217])).
% 0.12/0.49 fof(f781,plain,(
% 0.12/0.49 ~stoppedIn(n0,filling,n1)|terminates(sK0_skl(n1,filling,n0),filling,n0)),
% 0.12/0.49 inference(paramodulation,[status(thm)],[f764,f63])).
% 0.12/0.49 fof(f785,plain,(
% 0.12/0.49 ~stoppedIn(n0,filling,n1)|terminates(tapOn,filling,n0)),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f777,f781])).
% 0.12/0.49 fof(f786,plain,(
% 0.12/0.49 terminates(tapOn,filling,n0)),
% 0.12/0.49 inference(forward_subsumption_resolution,[status(thm)],[f785,f751])).
% 0.12/0.49 fof(f789,plain,(
% 0.12/0.49 tapOn=tapOff|tapOn=overflow),
% 0.12/0.49 inference(resolution,[status(thm)],[f786,f120])).
% 0.12/0.49 fof(f805,plain,(
% 0.12/0.49 ~tapOn=tapOn),
% 0.12/0.49 inference(backward_demodulation,[status(thm)],[f825,f149])).
% 0.12/0.50 fof(f825,plain,(
% 0.12/0.50 tapOn=overflow),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f789,f147])).
% 0.12/0.50 fof(f828,plain,(
% 0.12/0.50 $false),
% 0.12/0.50 inference(trivial_equality_resolution,[status(thm)],[f805])).
% 0.12/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.38/0.51 % Elapsed time: 0.155465 seconds
% 0.38/0.51 % CPU time: 0.966432 seconds
% 0.38/0.51 % Total memory used: 122.688 MB
% 0.38/0.51 % Net memory used: 121.134 MB
%------------------------------------------------------------------------------