%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR002+2 : 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 : n003.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 2.87s 0.82s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR002+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n003.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 14:24:47 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 2.87/0.82 % Refutation found
% 2.87/0.82 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.87/0.82 % SZS output start CNFRefutation for theBenchmark
% 2.87/0.82 fof(f6,axiom,(
% 2.87/0.82 (! [Fluent,Time] :( ( ~ holdsAt(Fluent,Time)& ~ releasedAt(Fluent,plus(Time,n1))& ~ (? [Event] :( happens(Event,Time)& initiates(Event,Fluent,Time) ) ))=> ~ holdsAt(Fluent,plus(Time,n1)) ) )),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f8,axiom,(
% 2.87/0.82 (! [Fluent,Time] :( ( ~ releasedAt(Fluent,Time)& ~ (? [Event] :( happens(Event,Time)& releases(Event,Fluent,Time) ) ))=> ~ releasedAt(Fluent,plus(Time,n1)) ) )),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f10,axiom,(
% 2.87/0.82 (! [Event,Time,Fluent] :( ( happens(Event,Time)& terminates(Event,Fluent,Time) )=> ~ holdsAt(Fluent,plus(Time,n1)) ) )),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f14,axiom,(
% 2.87/0.82 (! [Event,Fluent,Time] :( terminates(Event,Fluent,Time)<=> ( ( Event = tapOff& Fluent = filling )| ( Event = overflow& Fluent = filling ) ) ) )),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f15,axiom,(
% 2.87/0.82 (! [Event,Fluent,Time] :( releases(Event,Fluent,Time)<=> (? [Height] :( Event = tapOn& Fluent = waterLevel(Height) ) )) )),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f16,axiom,(
% 2.87/0.82 (! [Event,Time] :( happens(Event,Time)<=> ( ( Event = tapOn& Time = n0 )| ( holdsAt(waterLevel(n3),Time)& holdsAt(filling,Time)& Event = overflow ) ) ) )),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f21,axiom,(
% 2.87/0.82 overflow != tapOn ),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f22,axiom,(
% 2.87/0.82 (! [X] : filling != waterLevel(X) )),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f27,axiom,(
% 2.87/0.82 plus(n0,n1) = n1 ),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f30,axiom,(
% 2.87/0.82 plus(n1,n1) = n2 ),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f31,axiom,(
% 2.87/0.82 plus(n1,n2) = n3 ),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f32,axiom,(
% 2.87/0.82 plus(n1,n3) = n4 ),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f36,axiom,(
% 2.87/0.82 (! [X,Y] : plus(X,Y) = plus(Y,X) )),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f37,axiom,(
% 2.87/0.82 (! [X,Y] :( less_or_equal(X,Y)<=> ( less(X,Y)| X = Y ) ) )),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f39,axiom,(
% 2.87/0.82 (! [X] :( less(X,n1)<=> less_or_equal(X,n0) ) )),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f40,axiom,(
% 2.87/0.82 (! [X] :( less(X,n2)<=> less_or_equal(X,n1) ) )),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f41,axiom,(
% 2.87/0.82 (! [X] :( less(X,n3)<=> less_or_equal(X,n2) ) )),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f48,axiom,(
% 2.87/0.82 (! [X,Y] :( less(X,Y)<=> ( ~ less(Y,X)& Y != X ) ) )),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f53,hypothesis,(
% 2.87/0.82 ~ releasedAt(filling,n0) ),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f55,lemma,(
% 2.87/0.82 holdsAt(waterLevel(n3),n3) ),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f56,conjecture,(
% 2.87/0.82 ~ holdsAt(filling,n4) ),
% 2.87/0.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.87/0.82 fof(f57,negated_conjecture,(
% 2.87/0.82 ~(~ holdsAt(filling,n4) )),
% 2.87/0.82 inference(negated_conjecture,[status(cth)],[f56])).
% 2.87/0.82 fof(f84,plain,(
% 2.87/0.82 ![Fluent,Time]: (((holdsAt(Fluent,Time)|releasedAt(Fluent,plus(Time,n1)))|(?[Event]: (happens(Event,Time)&initiates(Event,Fluent,Time))))|~holdsAt(Fluent,plus(Time,n1)))),
% 2.87/0.82 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 2.87/0.82 fof(f85,plain,(
% 2.87/0.82 ![Fluent,Time]: (((holdsAt(Fluent,Time)|releasedAt(Fluent,plus(Time,n1)))|(happens(sK5_skl(Time,Fluent),Time)&initiates(sK5_skl(Time,Fluent),Fluent,Time)))|~holdsAt(Fluent,plus(Time,n1)))),
% 2.87/0.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(Event,sK5_skl(Time,Fluent))],[f84])).
% 2.87/0.82 fof(f86,plain,(
% 2.87/0.82 ![X0,X1]: (holdsAt(X0,X1)|releasedAt(X0,plus(X1,n1))|happens(sK5_skl(X1,X0),X1)|~holdsAt(X0,plus(X1,n1)))),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f85])).
% 2.87/0.82 fof(f92,plain,(
% 2.87/0.82 ![Fluent,Time]: ((releasedAt(Fluent,Time)|(?[Event]: (happens(Event,Time)&releases(Event,Fluent,Time))))|~releasedAt(Fluent,plus(Time,n1)))),
% 2.87/0.82 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 2.87/0.82 fof(f93,plain,(
% 2.87/0.82 ![Fluent,Time]: ((releasedAt(Fluent,Time)|(happens(sK7_skl(Time,Fluent),Time)&releases(sK7_skl(Time,Fluent),Fluent,Time)))|~releasedAt(Fluent,plus(Time,n1)))),
% 2.87/0.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Event,sK7_skl(Time,Fluent))],[f92])).
% 2.87/0.82 fof(f95,plain,(
% 2.87/0.82 ![X0,X1]: (releasedAt(X0,X1)|releases(sK7_skl(X1,X0),X0,X1)|~releasedAt(X0,plus(X1,n1)))),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f93])).
% 2.87/0.82 fof(f99,plain,(
% 2.87/0.82 ![Event,Time,Fluent]: ((~happens(Event,Time)|~terminates(Event,Fluent,Time))|~holdsAt(Fluent,plus(Time,n1)))),
% 2.87/0.82 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 2.87/0.82 fof(f100,plain,(
% 2.87/0.82 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~terminates(Event,Fluent,Time)))|~holdsAt(Fluent,plus(Time,n1)))),
% 2.87/0.82 inference(miniscoping,[status(thm)],[f99])).
% 2.87/0.82 fof(f101,plain,(
% 2.87/0.82 ![X0,X1,X2]: (~happens(X0,X1)|~terminates(X0,X2,X1)|~holdsAt(X2,plus(X1,n1)))),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f100])).
% 2.87/0.82 fof(f119,plain,(
% 2.87/0.82 ![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))))),
% 2.87/0.82 inference(NNF_transformation,[status(thm)],[f14])).
% 2.87/0.82 fof(f120,plain,(
% 2.87/0.82 (![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))))),
% 2.87/0.82 inference(miniscoping,[status(thm)],[f119])).
% 2.87/0.82 fof(f126,plain,(
% 2.87/0.82 ![X0,X1,X2]: (terminates(X0,X1,X2)|~X0=overflow|~X1=filling)),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f120])).
% 2.87/0.82 fof(f127,plain,(
% 2.87/0.82 ![Event,Fluent,Time]: ((~releases(Event,Fluent,Time)|(?[Height]: (Event=tapOn&Fluent=waterLevel(Height))))&(releases(Event,Fluent,Time)|(![Height]: (~Event=tapOn|~Fluent=waterLevel(Height)))))),
% 2.87/0.82 inference(NNF_transformation,[status(thm)],[f15])).
% 2.87/0.82 fof(f128,plain,(
% 2.87/0.82 (![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)))))),
% 2.87/0.82 inference(miniscoping,[status(thm)],[f127])).
% 2.87/0.82 fof(f129,plain,(
% 2.87/0.82 (![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)))))),
% 2.87/0.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(Height,sK9_skl(Fluent,Event))],[f128])).
% 2.87/0.82 fof(f131,plain,(
% 2.87/0.82 ![X0,X1,X2]: (~releases(X0,X1,X2)|X1=waterLevel(sK9_skl(X1,X0)))),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f129])).
% 2.87/0.82 fof(f133,definition,(
% 2.87/0.82 ![Event,Time]: (sP1_prd(Time,Event)<=>(Event=tapOn&Time=n0))),
% 2.87/0.82 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 2.87/0.82 fof(f134,plain,(
% 2.87/0.82 ![Event,Time]: (happens(Event,Time)<=>(sP1_prd(Time,Event)|((holdsAt(waterLevel(n3),Time)&holdsAt(filling,Time))&Event=overflow)))),
% 2.87/0.82 inference(formula_renaming,[status(thm)],[f16,f133])).
% 2.87/0.82 fof(f135,plain,(
% 2.87/0.82 ![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))))),
% 2.87/0.82 inference(NNF_transformation,[status(thm)],[f134])).
% 2.87/0.82 fof(f136,plain,(
% 2.87/0.82 (![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))))),
% 2.87/0.82 inference(miniscoping,[status(thm)],[f135])).
% 2.87/0.82 fof(f138,plain,(
% 2.87/0.82 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|holdsAt(filling,X1))),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f136])).
% 2.87/0.82 fof(f139,plain,(
% 2.87/0.82 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|X0=overflow)),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f136])).
% 2.87/0.82 fof(f141,plain,(
% 2.87/0.82 ![X0,X1]: (happens(X0,X1)|~holdsAt(waterLevel(n3),X1)|~holdsAt(filling,X1)|~X0=overflow)),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f136])).
% 2.87/0.82 fof(f150,plain,(
% 2.87/0.82 ~overflow=tapOn),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f21])).
% 2.87/0.82 fof(f151,plain,(
% 2.87/0.82 ![X0]: (~filling=waterLevel(X0))),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f22])).
% 2.87/0.82 fof(f159,plain,(
% 2.87/0.82 plus(n0,n1)=n1),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f27])).
% 2.87/0.82 fof(f162,plain,(
% 2.87/0.82 plus(n1,n1)=n2),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f30])).
% 2.87/0.82 fof(f163,plain,(
% 2.87/0.82 plus(n1,n2)=n3),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f31])).
% 2.87/0.82 fof(f164,plain,(
% 2.87/0.82 plus(n1,n3)=n4),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f32])).
% 2.87/0.82 fof(f168,plain,(
% 2.87/0.82 ![X0,X1]: (plus(X0,X1)=plus(X1,X0))),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f36])).
% 2.87/0.82 fof(f169,plain,(
% 2.87/0.82 ![X,Y]: ((~less_or_equal(X,Y)|(less(X,Y)|X=Y))&(less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 2.87/0.82 inference(NNF_transformation,[status(thm)],[f37])).
% 2.87/0.82 fof(f170,plain,(
% 2.87/0.82 (![X,Y]: (~less_or_equal(X,Y)|(less(X,Y)|X=Y)))&(![X,Y]: (less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 2.87/0.82 inference(miniscoping,[status(thm)],[f169])).
% 2.87/0.82 fof(f172,plain,(
% 2.87/0.82 ![X0,X1]: (less_or_equal(X0,X1)|~less(X0,X1))),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f170])).
% 2.87/0.82 fof(f173,plain,(
% 2.87/0.82 ![X0,X1]: (less_or_equal(X0,X1)|~X0=X1)),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f170])).
% 2.87/0.82 fof(f176,plain,(
% 2.87/0.82 ![X]: ((~less(X,n1)|less_or_equal(X,n0))&(less(X,n1)|~less_or_equal(X,n0)))),
% 2.87/0.82 inference(NNF_transformation,[status(thm)],[f39])).
% 2.87/0.82 fof(f177,plain,(
% 2.87/0.82 (![X]: (~less(X,n1)|less_or_equal(X,n0)))&(![X]: (less(X,n1)|~less_or_equal(X,n0)))),
% 2.87/0.82 inference(miniscoping,[status(thm)],[f176])).
% 2.87/0.82 fof(f179,plain,(
% 2.87/0.82 ![X0]: (less(X0,n1)|~less_or_equal(X0,n0))),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f177])).
% 2.87/0.82 fof(f180,plain,(
% 2.87/0.82 ![X]: ((~less(X,n2)|less_or_equal(X,n1))&(less(X,n2)|~less_or_equal(X,n1)))),
% 2.87/0.82 inference(NNF_transformation,[status(thm)],[f40])).
% 2.87/0.82 fof(f181,plain,(
% 2.87/0.82 (![X]: (~less(X,n2)|less_or_equal(X,n1)))&(![X]: (less(X,n2)|~less_or_equal(X,n1)))),
% 2.87/0.82 inference(miniscoping,[status(thm)],[f180])).
% 2.87/0.82 fof(f183,plain,(
% 2.87/0.82 ![X0]: (less(X0,n2)|~less_or_equal(X0,n1))),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f181])).
% 2.87/0.82 fof(f184,plain,(
% 2.87/0.82 ![X]: ((~less(X,n3)|less_or_equal(X,n2))&(less(X,n3)|~less_or_equal(X,n2)))),
% 2.87/0.82 inference(NNF_transformation,[status(thm)],[f41])).
% 2.87/0.82 fof(f185,plain,(
% 2.87/0.82 (![X]: (~less(X,n3)|less_or_equal(X,n2)))&(![X]: (less(X,n3)|~less_or_equal(X,n2)))),
% 2.87/0.82 inference(miniscoping,[status(thm)],[f184])).
% 2.87/0.82 fof(f187,plain,(
% 2.87/0.82 ![X0]: (less(X0,n3)|~less_or_equal(X0,n2))),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f185])).
% 2.87/0.82 fof(f212,plain,(
% 2.87/0.82 ![X,Y]: ((~less(X,Y)|(~less(Y,X)&~Y=X))&(less(X,Y)|(less(Y,X)|Y=X)))),
% 2.87/0.82 inference(NNF_transformation,[status(thm)],[f48])).
% 2.87/0.82 fof(f213,plain,(
% 2.87/0.82 (![X,Y]: (~less(X,Y)|(~less(Y,X)&~Y=X)))&(![X,Y]: (less(X,Y)|(less(Y,X)|Y=X)))),
% 2.87/0.82 inference(miniscoping,[status(thm)],[f212])).
% 2.87/0.82 fof(f214,plain,(
% 2.87/0.82 ![X0,X1]: (~less(X0,X1)|~less(X1,X0))),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f213])).
% 2.87/0.82 fof(f221,plain,(
% 2.87/0.82 ~releasedAt(filling,n0)),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f53])).
% 2.87/0.82 fof(f223,plain,(
% 2.87/0.82 holdsAt(waterLevel(n3),n3)),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f55])).
% 2.87/0.82 fof(f224,plain,(
% 2.87/0.82 holdsAt(filling,n4)),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f57])).
% 2.87/0.82 fof(f235,plain,(
% 2.87/0.82 ![Event,Time]: ((~sP1_prd(Time,Event)|(Event=tapOn&Time=n0))&(sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 2.87/0.82 inference(NNF_transformation,[status(thm)],[f133])).
% 2.87/0.82 fof(f236,plain,(
% 2.87/0.82 (![Event,Time]: (~sP1_prd(Time,Event)|(Event=tapOn&Time=n0)))&(![Event,Time]: (sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 2.87/0.82 inference(miniscoping,[status(thm)],[f235])).
% 2.87/0.82 fof(f237,plain,(
% 2.87/0.82 ![X0,X1]: (~sP1_prd(X0,X1)|X1=tapOn)),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f236])).
% 2.87/0.82 fof(f238,plain,(
% 2.87/0.82 ![X0,X1]: (~sP1_prd(X0,X1)|X0=n0)),
% 2.87/0.82 inference(cnf_transformation,[status(thm)],[f236])).
% 2.87/0.82 fof(f251,plain,(
% 2.87/0.82 ![X0]: (terminates(overflow,filling,X0))),
% 2.87/0.82 inference(destructive_equality_resolution,[status(thm)],[f126])).
% 2.87/0.82 fof(f253,plain,(
% 2.87/0.82 ![X0]: (happens(overflow,X0)|~holdsAt(waterLevel(n3),X0)|~holdsAt(filling,X0))),
% 2.87/0.82 inference(destructive_equality_resolution,[status(thm)],[f141])).
% 2.87/0.82 fof(f255,plain,(
% 2.87/0.82 ![X0]: (less_or_equal(X0,X0))),
% 2.87/0.82 inference(destructive_equality_resolution,[status(thm)],[f173])).
% 2.87/0.82 fof(f288,plain,(
% 2.87/0.82 ![X0,X1]: (holdsAt(X0,X1)|releasedAt(X0,plus(X1,n1))|happens(sK5_skl(X1,X0),X1)|~holdsAt(X0,plus(n1,X1)))),
% 2.87/0.82 inference(paramodulation,[status(thm)],[f168,f86])).
% 2.87/0.82 fof(f307,plain,(
% 2.87/0.82 less(n0,n1)),
% 2.87/0.82 inference(resolution,[status(thm)],[f179,f255])).
% 2.87/0.82 fof(f311,plain,(
% 2.87/0.82 less(n1,n2)),
% 2.87/0.82 inference(resolution,[status(thm)],[f183,f255])).
% 2.87/0.82 fof(f330,plain,(
% 2.87/0.82 ![X0]: (less(X0,n3)|~less(X0,n2))),
% 2.87/0.82 inference(resolution,[status(thm)],[f187,f172])).
% 2.87/0.82 fof(f346,plain,(
% 2.87/0.82 ![X0,X1,X2]: (~happens(X0,X1)|~terminates(X0,X2,X1)|~holdsAt(X2,plus(n1,X1)))),
% 2.87/0.82 inference(paramodulation,[status(thm)],[f168,f101])).
% 2.87/0.82 fof(f364,plain,(
% 2.87/0.82 less(n1,n3)),
% 2.87/0.82 inference(resolution,[status(thm)],[f330,f311])).
% 2.87/0.82 fof(f367,plain,(
% 2.87/0.82 ~less(n3,n1)),
% 2.87/0.82 inference(resolution,[status(thm)],[f364,f214])).
% 2.87/0.82 fof(f372,plain,(
% 2.87/0.82 ![X0,X1]: (X0=waterLevel(sK9_skl(X0,sK7_skl(X1,X0)))|releasedAt(X0,X1)|~releasedAt(X0,plus(X1,n1)))),
% 2.87/0.82 inference(resolution,[status(thm)],[f131,f95])).
% 2.87/0.82 fof(f385,plain,(
% 2.87/0.82 ![X0,X1]: (~happens(X0,X1)|holdsAt(filling,X1)|X0=tapOn)),
% 2.87/0.82 inference(resolution,[status(thm)],[f138,f237])).
% 2.87/0.82 fof(f403,plain,(
% 2.87/0.82 happens(overflow,n3)|~holdsAt(filling,n3)),
% 2.87/0.82 inference(resolution,[status(thm)],[f253,f223])).
% 2.87/0.82 fof(f404,plain,(
% 2.87/0.82 ![X0]: (happens(overflow,n3)|~happens(X0,n3)|X0=tapOn)),
% 2.87/0.82 inference(resolution,[status(thm)],[f403,f385])).
% 2.87/0.82 fof(f453,plain,(
% 2.87/0.82 ![X0]: (~happens(overflow,X0)|~holdsAt(filling,plus(n1,X0)))),
% 2.87/0.82 inference(resolution,[status(thm)],[f346,f251])).
% 2.87/0.82 fof(f517,plain,(
% 2.87/0.82 ![X0]: (X0=waterLevel(sK9_skl(X0,sK7_skl(n0,X0)))|releasedAt(X0,n0)|~releasedAt(X0,n1))),
% 2.87/0.82 inference(paramodulation,[status(thm)],[f159,f372])).
% 2.87/0.82 fof(f518,plain,(
% 2.87/0.82 ![X0]: (X0=waterLevel(sK9_skl(X0,sK7_skl(n1,X0)))|releasedAt(X0,n1)|~releasedAt(X0,n2))),
% 2.87/0.82 inference(paramodulation,[status(thm)],[f162,f372])).
% 2.87/0.82 fof(f519,plain,(
% 2.87/0.82 ![X0,X1]: (X0=waterLevel(sK9_skl(X0,sK7_skl(X1,X0)))|releasedAt(X0,X1)|~releasedAt(X0,plus(n1,X1)))),
% 2.87/0.82 inference(paramodulation,[status(thm)],[f168,f372])).
% 2.87/0.82 fof(f528,plain,(
% 2.87/0.82 ![X0]: (X0=waterLevel(sK9_skl(X0,sK7_skl(n2,X0)))|releasedAt(X0,n2)|~releasedAt(X0,n3))),
% 2.87/0.82 inference(paramodulation,[status(thm)],[f163,f519])).
% 2.87/0.82 fof(f530,plain,(
% 2.87/0.82 ![X0]: (X0=waterLevel(sK9_skl(X0,sK7_skl(n3,X0)))|releasedAt(X0,n3)|~releasedAt(X0,n4))),
% 2.87/0.82 inference(paramodulation,[status(thm)],[f164,f519])).
% 2.87/0.82 fof(f563,plain,(
% 2.87/0.82 ![X0]: (holdsAt(X0,n3)|releasedAt(X0,plus(n3,n1))|happens(sK5_skl(n3,X0),n3)|~holdsAt(X0,n4))),
% 2.87/0.82 inference(paramodulation,[status(thm)],[f164,f288])).
% 2.87/0.82 fof(f576,plain,(
% 2.87/0.82 ![X0,X1]: (X0=n0|~happens(X1,X0)|X1=overflow)),
% 2.87/0.82 inference(resolution,[status(thm)],[f238,f139])).
% 2.87/0.82 fof(f608,plain,(
% 2.87/0.82 holdsAt(filling,n3)|releasedAt(filling,plus(n3,n1))|happens(sK5_skl(n3,filling),n3)),
% 2.87/0.82 inference(resolution,[status(thm)],[f563,f224])).
% 2.87/0.82 fof(f610,plain,(
% 2.87/0.82 holdsAt(filling,n3)|happens(sK5_skl(n3,filling),n3)|filling=waterLevel(sK9_skl(filling,sK7_skl(n3,filling)))|releasedAt(filling,n3)),
% 2.87/0.82 inference(resolution,[status(thm)],[f608,f372])).
% 2.87/0.82 fof(f613,plain,(
% 2.87/0.82 holdsAt(filling,n3)|releasedAt(filling,plus(n1,n3))|happens(sK5_skl(n3,filling),n3)),
% 2.87/0.82 inference(paramodulation,[status(thm)],[f168,f608])).
% 2.87/0.82 fof(f615,plain,(
% 2.87/0.82 holdsAt(filling,n3)|happens(sK5_skl(n3,filling),n3)|releasedAt(filling,n3)),
% 2.87/0.82 inference(forward_subsumption_resolution,[status(thm)],[f610,f151])).
% 2.87/0.82 fof(f616,plain,(
% 2.87/0.82 holdsAt(filling,n3)|releasedAt(filling,n4)|happens(sK5_skl(n3,filling),n3)),
% 2.87/0.82 inference(forward_demodulation,[status(thm)],[f164,f613])).
% 2.87/0.82 fof(f618,plain,(
% 2.87/0.82 holdsAt(filling,n3)|releasedAt(filling,n4)|happens(overflow,n3)|sK5_skl(n3,filling)=tapOn),
% 2.87/0.82 inference(resolution,[status(thm)],[f616,f404])).
% 2.87/0.82 fof(f621,plain,(
% 2.87/0.82 releasedAt(filling,n4)|happens(overflow,n3)|sK5_skl(n3,filling)=tapOn),
% 2.87/0.82 inference(forward_subsumption_resolution,[status(thm)],[f618,f403])).
% 2.87/0.82 fof(f623,plain,(
% 2.87/0.82 happens(overflow,n3)|sK5_skl(n3,filling)=tapOn|filling=waterLevel(sK9_skl(filling,sK7_skl(n3,filling)))|releasedAt(filling,n3)),
% 2.87/0.82 inference(resolution,[status(thm)],[f621,f530])).
% 2.87/0.82 fof(f625,plain,(
% 2.87/0.82 happens(overflow,n3)|sK5_skl(n3,filling)=tapOn|releasedAt(filling,n3)),
% 2.87/0.82 inference(forward_subsumption_resolution,[status(thm)],[f623,f151])).
% 2.87/0.82 fof(f641,plain,(
% 2.87/0.82 happens(overflow,n3)|sK5_skl(n3,filling)=tapOn|filling=waterLevel(sK9_skl(filling,sK7_skl(n2,filling)))|releasedAt(filling,n2)),
% 2.87/0.82 inference(resolution,[status(thm)],[f625,f528])).
% 2.87/0.82 fof(f643,plain,(
% 2.87/0.82 happens(overflow,n3)|sK5_skl(n3,filling)=tapOn|releasedAt(filling,n2)),
% 2.87/0.82 inference(forward_subsumption_resolution,[status(thm)],[f641,f151])).
% 2.87/0.82 fof(f644,plain,(
% 2.87/0.82 happens(overflow,n3)|sK5_skl(n3,filling)=tapOn|filling=waterLevel(sK9_skl(filling,sK7_skl(n1,filling)))|releasedAt(filling,n1)),
% 2.87/0.82 inference(resolution,[status(thm)],[f643,f518])).
% 2.87/0.82 fof(f646,plain,(
% 2.87/0.82 happens(overflow,n3)|sK5_skl(n3,filling)=tapOn|releasedAt(filling,n1)),
% 2.87/0.82 inference(forward_subsumption_resolution,[status(thm)],[f644,f151])).
% 2.87/0.82 fof(f651,plain,(
% 2.87/0.82 happens(overflow,n3)|sK5_skl(n3,filling)=tapOn|filling=waterLevel(sK9_skl(filling,sK7_skl(n0,filling)))|releasedAt(filling,n0)),
% 2.87/0.82 inference(resolution,[status(thm)],[f646,f517])).
% 2.87/0.82 fof(f654,plain,(
% 2.87/0.82 happens(overflow,n3)|sK5_skl(n3,filling)=tapOn|releasedAt(filling,n0)),
% 2.87/0.82 inference(forward_subsumption_resolution,[status(thm)],[f651,f151])).
% 2.87/0.82 fof(f656,plain,(
% 2.87/0.82 happens(overflow,n3)|sK5_skl(n3,filling)=tapOn),
% 2.87/0.82 inference(resolution,[status(thm)],[f654,f221])).
% 2.87/0.82 fof(f659,plain,(
% 2.87/0.82 sK5_skl(n3,filling)=tapOn|~holdsAt(filling,plus(n1,n3))),
% 2.87/0.82 inference(resolution,[status(thm)],[f656,f453])).
% 2.87/0.82 fof(f663,plain,(
% 2.87/0.82 sK5_skl(n3,filling)=tapOn|~holdsAt(filling,n4)),
% 2.87/0.82 inference(forward_demodulation,[status(thm)],[f164,f659])).
% 2.87/0.82 fof(f669,plain,(
% 2.87/0.82 holdsAt(filling,n3)|happens(tapOn,n3)|releasedAt(filling,n3)),
% 2.87/0.82 inference(backward_demodulation,[status(thm)],[f670,f615])).
% 2.87/0.82 fof(f670,plain,(
% 2.87/0.82 sK5_skl(n3,filling)=tapOn),
% 2.87/0.82 inference(forward_subsumption_resolution,[status(thm)],[f663,f224])).
% 2.87/0.82 fof(f685,plain,(
% 2.87/0.82 holdsAt(filling,n3)|happens(tapOn,n3)|filling=waterLevel(sK9_skl(filling,sK7_skl(n2,filling)))|releasedAt(filling,n2)),
% 2.87/0.82 inference(resolution,[status(thm)],[f669,f528])).
% 2.87/0.82 fof(f687,plain,(
% 2.87/0.82 holdsAt(filling,n3)|happens(tapOn,n3)|releasedAt(filling,n2)),
% 2.87/0.82 inference(forward_subsumption_resolution,[status(thm)],[f685,f151])).
% 2.87/0.82 fof(f688,plain,(
% 2.87/0.82 holdsAt(filling,n3)|happens(tapOn,n3)|filling=waterLevel(sK9_skl(filling,sK7_skl(n1,filling)))|releasedAt(filling,n1)),
% 2.87/0.82 inference(resolution,[status(thm)],[f687,f518])).
% 2.87/0.82 fof(f690,plain,(
% 2.87/0.82 holdsAt(filling,n3)|happens(tapOn,n3)|releasedAt(filling,n1)),
% 2.87/0.82 inference(forward_subsumption_resolution,[status(thm)],[f688,f151])).
% 2.87/0.82 fof(f691,plain,(
% 2.87/0.82 holdsAt(filling,n3)|happens(tapOn,n3)|filling=waterLevel(sK9_skl(filling,sK7_skl(n0,filling)))|releasedAt(filling,n0)),
% 2.87/0.82 inference(resolution,[status(thm)],[f690,f517])).
% 2.87/0.82 fof(f694,plain,(
% 2.87/0.82 holdsAt(filling,n3)|happens(tapOn,n3)|releasedAt(filling,n0)),
% 2.87/0.82 inference(forward_subsumption_resolution,[status(thm)],[f691,f151])).
% 2.87/0.82 fof(f696,plain,(
% 2.87/0.82 holdsAt(filling,n3)|happens(tapOn,n3)),
% 2.87/0.82 inference(resolution,[status(thm)],[f694,f221])).
% 2.87/0.82 fof(f699,plain,(
% 2.87/0.82 happens(tapOn,n3)|happens(overflow,n3)),
% 2.87/0.82 inference(resolution,[status(thm)],[f696,f403])).
% 2.87/0.82 fof(f701,plain,(
% 2.87/0.82 happens(tapOn,n3)|~holdsAt(filling,plus(n1,n3))),
% 2.87/0.82 inference(resolution,[status(thm)],[f699,f453])).
% 2.87/0.82 fof(f705,plain,(
% 2.87/0.82 happens(tapOn,n3)|~holdsAt(filling,n4)),
% 2.87/0.82 inference(forward_demodulation,[status(thm)],[f164,f701])).
% 2.87/0.82 fof(f706,plain,(
% 2.87/0.82 happens(tapOn,n3)),
% 2.87/0.82 inference(forward_subsumption_resolution,[status(thm)],[f705,f224])).
% 2.87/0.82 fof(f1004,plain,(
% 2.87/0.82 n3=n0|tapOn=overflow),
% 2.87/0.82 inference(resolution,[status(thm)],[f576,f706])).
% 2.87/0.82 fof(f1069,plain,(
% 2.87/0.82 ~less(n0,n1)),
% 2.87/0.82 inference(backward_demodulation,[status(thm)],[f1163,f367])).
% 2.87/0.84 fof(f1163,plain,(
% 2.87/0.84 n3=n0),
% 2.87/0.84 inference(forward_subsumption_resolution,[status(thm)],[f1004,f150])).
% 2.87/0.84 fof(f1259,plain,(
% 2.87/0.84 $false),
% 2.87/0.84 inference(forward_subsumption_resolution,[status(thm)],[f1069,f307])).
% 2.87/0.84 % SZS output end CNFRefutation for theBenchmark.p
% 0.27/0.85 % Elapsed time: 0.481208 seconds
% 0.27/0.85 % CPU time: 3.495478 seconds
% 0.27/0.85 % Total memory used: 155.499 MB
% 0.27/0.85 % Net memory used: 151.657 MB
%------------------------------------------------------------------------------