%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR014+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 : n005.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 4.04s 0.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR014+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.06/0.34 % Computer : n005.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Mon Sep 21 14:23:47 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.06/0.36 % Drodi V4.1.1
% 4.04/0.97 % Refutation found
% 4.04/0.97 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.04/0.97 % SZS output start CNFRefutation for theBenchmark
% 4.04/0.97 fof(f8,axiom,(
% 4.04/0.97 (! [Fluent,Time] :( ( ~ releasedAt(Fluent,Time)& ~ (? [Event] :( happens(Event,Time)& releases(Event,Fluent,Time) ) ))=> ~ releasedAt(Fluent,plus(Time,n1)) ) )),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f15,axiom,(
% 4.04/0.97 (! [Event,Fluent,Time] :( releases(Event,Fluent,Time)<=> (? [Height] :( Event = tapOn& Fluent = waterLevel(Height) ) )) )),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f16,axiom,(
% 4.04/0.97 (! [Event,Time] :( happens(Event,Time)<=> ( ( Event = tapOn& Time = n0 )| ( holdsAt(waterLevel(n3),Time)& holdsAt(filling,Time)& Event = overflow ) ) ) )),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f21,axiom,(
% 4.04/0.97 overflow != tapOn ),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f22,axiom,(
% 4.04/0.97 (! [X] : filling != waterLevel(X) )),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f27,axiom,(
% 4.04/0.97 plus(n0,n1) = n1 ),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f30,axiom,(
% 4.04/0.97 plus(n1,n1) = n2 ),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f31,axiom,(
% 4.04/0.97 plus(n1,n2) = n3 ),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f36,axiom,(
% 4.04/0.97 (! [X,Y] : plus(X,Y) = plus(Y,X) )),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f37,axiom,(
% 4.04/0.97 (! [X,Y] :( less_or_equal(X,Y)<=> ( less(X,Y)| X = Y ) ) )),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f38,axiom,(
% 4.04/0.97 ~ (? [X] : less(X,n0) )),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f39,axiom,(
% 4.04/0.97 (! [X] :( less(X,n1)<=> less_or_equal(X,n0) ) )),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f53,hypothesis,(
% 4.04/0.97 ~ releasedAt(filling,n0) ),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f55,conjecture,(
% 4.04/0.97 ~ releasedAt(filling,n3) ),
% 4.04/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.04/0.97 fof(f56,negated_conjecture,(
% 4.04/0.97 ~(~ releasedAt(filling,n3) )),
% 4.04/0.97 inference(negated_conjecture,[status(cth)],[f55])).
% 4.04/0.97 fof(f91,plain,(
% 4.04/0.97 ![Fluent,Time]: ((releasedAt(Fluent,Time)|(?[Event]: (happens(Event,Time)&releases(Event,Fluent,Time))))|~releasedAt(Fluent,plus(Time,n1)))),
% 4.04/0.97 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 4.04/0.97 fof(f92,plain,(
% 4.04/0.97 ![Fluent,Time]: ((releasedAt(Fluent,Time)|(happens(sK7_skl(Time,Fluent),Time)&releases(sK7_skl(Time,Fluent),Fluent,Time)))|~releasedAt(Fluent,plus(Time,n1)))),
% 4.04/0.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Event,sK7_skl(Time,Fluent))],[f91])).
% 4.04/0.97 fof(f93,plain,(
% 4.04/0.97 ![X0,X1]: (releasedAt(X0,X1)|happens(sK7_skl(X1,X0),X1)|~releasedAt(X0,plus(X1,n1)))),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f92])).
% 4.04/0.97 fof(f94,plain,(
% 4.04/0.97 ![X0,X1]: (releasedAt(X0,X1)|releases(sK7_skl(X1,X0),X0,X1)|~releasedAt(X0,plus(X1,n1)))),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f92])).
% 4.04/0.97 fof(f126,plain,(
% 4.04/0.97 ![Event,Fluent,Time]: ((~releases(Event,Fluent,Time)|(?[Height]: (Event=tapOn&Fluent=waterLevel(Height))))&(releases(Event,Fluent,Time)|(![Height]: (~Event=tapOn|~Fluent=waterLevel(Height)))))),
% 4.04/0.97 inference(NNF_transformation,[status(thm)],[f15])).
% 4.04/0.97 fof(f127,plain,(
% 4.04/0.97 (![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)))))),
% 4.04/0.97 inference(miniscoping,[status(thm)],[f126])).
% 4.04/0.97 fof(f128,plain,(
% 4.04/0.97 (![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)))))),
% 4.04/0.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(Height,sK9_skl(Fluent,Event))],[f127])).
% 4.04/0.97 fof(f129,plain,(
% 4.04/0.97 ![X0,X1,X2]: (~releases(X0,X1,X2)|X0=tapOn)),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f128])).
% 4.04/0.97 fof(f130,plain,(
% 4.04/0.97 ![X0,X1,X2]: (~releases(X0,X1,X2)|X1=waterLevel(sK9_skl(X1,X0)))),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f128])).
% 4.04/0.97 fof(f132,definition,(
% 4.04/0.97 ![Event,Time]: (sP1_prd(Time,Event)<=>(Event=tapOn&Time=n0))),
% 4.04/0.97 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 4.04/0.97 fof(f133,plain,(
% 4.04/0.97 ![Event,Time]: (happens(Event,Time)<=>(sP1_prd(Time,Event)|((holdsAt(waterLevel(n3),Time)&holdsAt(filling,Time))&Event=overflow)))),
% 4.04/0.97 inference(formula_renaming,[status(thm)],[f16,f132])).
% 4.04/0.97 fof(f134,plain,(
% 4.04/0.97 ![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))))),
% 4.04/0.97 inference(NNF_transformation,[status(thm)],[f133])).
% 4.04/0.97 fof(f135,plain,(
% 4.04/0.97 (![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))))),
% 4.04/0.97 inference(miniscoping,[status(thm)],[f134])).
% 4.04/0.97 fof(f138,plain,(
% 4.04/0.97 ![X0,X1]: (~happens(X0,X1)|sP1_prd(X1,X0)|X0=overflow)),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f135])).
% 4.04/0.97 fof(f149,plain,(
% 4.04/0.97 ~overflow=tapOn),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f21])).
% 4.04/0.97 fof(f150,plain,(
% 4.04/0.97 ![X0]: (~filling=waterLevel(X0))),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f22])).
% 4.04/0.97 fof(f158,plain,(
% 4.04/0.97 plus(n0,n1)=n1),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f27])).
% 4.04/0.97 fof(f161,plain,(
% 4.04/0.97 plus(n1,n1)=n2),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f30])).
% 4.04/0.97 fof(f162,plain,(
% 4.04/0.97 plus(n1,n2)=n3),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f31])).
% 4.04/0.97 fof(f167,plain,(
% 4.04/0.97 ![X0,X1]: (plus(X0,X1)=plus(X1,X0))),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f36])).
% 4.04/0.97 fof(f168,plain,(
% 4.04/0.97 ![X,Y]: ((~less_or_equal(X,Y)|(less(X,Y)|X=Y))&(less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 4.04/0.97 inference(NNF_transformation,[status(thm)],[f37])).
% 4.04/0.97 fof(f169,plain,(
% 4.04/0.97 (![X,Y]: (~less_or_equal(X,Y)|(less(X,Y)|X=Y)))&(![X,Y]: (less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 4.04/0.97 inference(miniscoping,[status(thm)],[f168])).
% 4.04/0.97 fof(f172,plain,(
% 4.04/0.97 ![X0,X1]: (less_or_equal(X0,X1)|~X0=X1)),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f169])).
% 4.04/0.97 fof(f173,plain,(
% 4.04/0.97 (![X]: ~less(X,n0))),
% 4.04/0.97 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 4.04/0.97 fof(f174,plain,(
% 4.04/0.97 ![X0]: (~less(X0,n0))),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f173])).
% 4.04/0.97 fof(f175,plain,(
% 4.04/0.97 ![X]: ((~less(X,n1)|less_or_equal(X,n0))&(less(X,n1)|~less_or_equal(X,n0)))),
% 4.04/0.97 inference(NNF_transformation,[status(thm)],[f39])).
% 4.04/0.97 fof(f176,plain,(
% 4.04/0.97 (![X]: (~less(X,n1)|less_or_equal(X,n0)))&(![X]: (less(X,n1)|~less_or_equal(X,n0)))),
% 4.04/0.97 inference(miniscoping,[status(thm)],[f175])).
% 4.04/0.97 fof(f178,plain,(
% 4.04/0.97 ![X0]: (less(X0,n1)|~less_or_equal(X0,n0))),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f176])).
% 4.04/0.97 fof(f220,plain,(
% 4.04/0.97 ~releasedAt(filling,n0)),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f53])).
% 4.04/0.97 fof(f222,plain,(
% 4.04/0.97 releasedAt(filling,n3)),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f56])).
% 4.04/0.97 fof(f233,plain,(
% 4.04/0.97 ![Event,Time]: ((~sP1_prd(Time,Event)|(Event=tapOn&Time=n0))&(sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 4.04/0.97 inference(NNF_transformation,[status(thm)],[f132])).
% 4.04/0.97 fof(f234,plain,(
% 4.04/0.97 (![Event,Time]: (~sP1_prd(Time,Event)|(Event=tapOn&Time=n0)))&(![Event,Time]: (sP1_prd(Time,Event)|(~Event=tapOn|~Time=n0)))),
% 4.04/0.97 inference(miniscoping,[status(thm)],[f233])).
% 4.04/0.97 fof(f236,plain,(
% 4.04/0.97 ![X0,X1]: (~sP1_prd(X0,X1)|X0=n0)),
% 4.04/0.97 inference(cnf_transformation,[status(thm)],[f234])).
% 4.04/0.97 fof(f247,plain,(
% 4.04/0.97 ![X0]: (less_or_equal(X0,X0))),
% 4.04/0.97 inference(destructive_equality_resolution,[status(thm)],[f172])).
% 4.04/0.97 fof(f405,plain,(
% 4.04/0.97 ![X0,X1]: (sK7_skl(X0,X1)=tapOn|releasedAt(X1,X0)|~releasedAt(X1,plus(X0,n1)))),
% 4.04/0.97 inference(resolution,[status(thm)],[f129,f94])).
% 4.04/0.97 fof(f790,plain,(
% 4.04/0.97 ![X0,X1]: (sK7_skl(X0,X1)=tapOn|releasedAt(X1,X0)|~releasedAt(X1,plus(n1,X0)))),
% 4.04/0.97 inference(paramodulation,[status(thm)],[f167,f405])).
% 4.04/0.97 fof(f1012,plain,(
% 4.04/0.97 ![X0,X1]: (X0=waterLevel(sK9_skl(X0,sK7_skl(X1,X0)))|releasedAt(X0,X1)|~releasedAt(X0,plus(X1,n1)))),
% 4.04/0.97 inference(resolution,[status(thm)],[f130,f94])).
% 4.04/0.97 fof(f1720,plain,(
% 4.04/0.97 ![X0]: (X0=waterLevel(sK9_skl(X0,sK7_skl(n0,X0)))|releasedAt(X0,n0)|~releasedAt(X0,n1))),
% 4.04/0.97 inference(paramodulation,[status(thm)],[f158,f1012])).
% 4.04/0.97 fof(f1788,plain,(
% 4.04/0.97 ![X0]: (sK7_skl(n1,X0)=tapOn|releasedAt(X0,n1)|~releasedAt(X0,n2))),
% 4.04/0.97 inference(paramodulation,[status(thm)],[f161,f790])).
% 4.04/0.97 fof(f1820,plain,(
% 4.04/0.97 plus(n2,n1)=n3),
% 4.04/0.97 inference(forward_demodulation,[status(thm)],[f167,f162])).
% 4.04/0.97 fof(f1829,plain,(
% 4.04/0.97 ![X0]: (sK7_skl(n2,X0)=tapOn|releasedAt(X0,n2)|~releasedAt(X0,n3))),
% 4.04/0.97 inference(paramodulation,[status(thm)],[f1820,f405])).
% 4.04/0.97 fof(f2340,plain,(
% 4.04/0.97 sK7_skl(n2,filling)=tapOn|releasedAt(filling,n2)),
% 4.04/0.97 inference(resolution,[status(thm)],[f1829,f222])).
% 4.04/0.97 fof(f2341,plain,(
% 4.04/0.97 sK7_skl(n2,filling)=tapOn|sK7_skl(n1,filling)=tapOn|releasedAt(filling,n1)),
% 4.04/0.97 inference(resolution,[status(thm)],[f2340,f1788])).
% 4.04/0.97 fof(f2403,plain,(
% 4.04/0.97 less(n0,n1)),
% 4.04/0.97 inference(resolution,[status(thm)],[f178,f247])).
% 4.04/0.97 fof(f2483,plain,(
% 4.04/0.97 sK7_skl(n2,filling)=tapOn|sK7_skl(n1,filling)=tapOn|filling=waterLevel(sK9_skl(filling,sK7_skl(n0,filling)))|releasedAt(filling,n0)),
% 4.04/0.98 inference(resolution,[status(thm)],[f2341,f1720])).
% 4.04/0.98 fof(f2487,plain,(
% 4.04/0.98 sK7_skl(n2,filling)=tapOn|sK7_skl(n1,filling)=tapOn|releasedAt(filling,n0)),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2483,f150])).
% 4.04/0.98 fof(f2491,plain,(
% 4.04/0.98 sK7_skl(n2,filling)=tapOn|sK7_skl(n1,filling)=tapOn),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2487,f220])).
% 4.04/0.98 fof(f2495,plain,(
% 4.04/0.98 releasedAt(filling,n1)|happens(tapOn,n1)|~releasedAt(filling,plus(n1,n1))|sK7_skl(n2,filling)=tapOn),
% 4.04/0.98 inference(paramodulation,[status(thm)],[f2491,f93])).
% 4.04/0.98 fof(f2502,plain,(
% 4.04/0.98 releasedAt(filling,n1)|happens(tapOn,n1)|~releasedAt(filling,n2)|sK7_skl(n2,filling)=tapOn),
% 4.04/0.98 inference(forward_demodulation,[status(thm)],[f161,f2495])).
% 4.04/0.98 fof(f2503,plain,(
% 4.04/0.98 releasedAt(filling,n1)|happens(tapOn,n1)|sK7_skl(n2,filling)=tapOn),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2502,f2340])).
% 4.04/0.98 fof(f2512,plain,(
% 4.04/0.98 releasedAt(filling,n1)|sK7_skl(n2,filling)=tapOn|sP1_prd(n1,tapOn)|tapOn=overflow),
% 4.04/0.98 inference(resolution,[status(thm)],[f2503,f138])).
% 4.04/0.98 fof(f2516,plain,(
% 4.04/0.98 releasedAt(filling,n1)|sK7_skl(n2,filling)=tapOn|sP1_prd(n1,tapOn)),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2512,f149])).
% 4.04/0.98 fof(f2517,plain,(
% 4.04/0.98 sK7_skl(n2,filling)=tapOn|sP1_prd(n1,tapOn)|filling=waterLevel(sK9_skl(filling,sK7_skl(n0,filling)))|releasedAt(filling,n0)),
% 4.04/0.98 inference(resolution,[status(thm)],[f2516,f1720])).
% 4.04/0.98 fof(f2521,plain,(
% 4.04/0.98 sK7_skl(n2,filling)=tapOn|sP1_prd(n1,tapOn)|releasedAt(filling,n0)),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2517,f150])).
% 4.04/0.98 fof(f2525,plain,(
% 4.04/0.98 sK7_skl(n2,filling)=tapOn|sP1_prd(n1,tapOn)),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2521,f220])).
% 4.04/0.98 fof(f2526,plain,(
% 4.04/0.98 sK7_skl(n2,filling)=tapOn|n1=n0),
% 4.04/0.98 inference(resolution,[status(thm)],[f2525,f236])).
% 4.04/0.98 fof(f2530,plain,(
% 4.04/0.98 releasedAt(filling,n2)|releases(tapOn,filling,n2)|~releasedAt(filling,plus(n2,n1))|n1=n0),
% 4.04/0.98 inference(paramodulation,[status(thm)],[f2526,f94])).
% 4.04/0.98 fof(f2536,plain,(
% 4.04/0.98 releasedAt(filling,n2)|releases(tapOn,filling,n2)|~releasedAt(filling,n3)|n1=n0),
% 4.04/0.98 inference(forward_demodulation,[status(thm)],[f1820,f2530])).
% 4.04/0.98 fof(f2537,plain,(
% 4.04/0.98 releasedAt(filling,n2)|releases(tapOn,filling,n2)|n1=n0),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2536,f222])).
% 4.04/0.98 fof(f2607,plain,(
% 4.04/0.98 releasedAt(filling,n2)|n1=n0|filling=waterLevel(sK9_skl(filling,tapOn))),
% 4.04/0.98 inference(resolution,[status(thm)],[f2537,f130])).
% 4.04/0.98 fof(f2610,plain,(
% 4.04/0.98 releasedAt(filling,n2)|n1=n0),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2607,f150])).
% 4.04/0.98 fof(f2612,plain,(
% 4.04/0.98 n1=n0|sK7_skl(n1,filling)=tapOn|releasedAt(filling,n1)),
% 4.04/0.98 inference(resolution,[status(thm)],[f2610,f1788])).
% 4.04/0.98 fof(f2642,plain,(
% 4.04/0.98 n1=n0|sK7_skl(n1,filling)=tapOn|filling=waterLevel(sK9_skl(filling,sK7_skl(n0,filling)))|releasedAt(filling,n0)),
% 4.04/0.98 inference(resolution,[status(thm)],[f2612,f1720])).
% 4.04/0.98 fof(f2646,plain,(
% 4.04/0.98 n1=n0|sK7_skl(n1,filling)=tapOn|releasedAt(filling,n0)),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2642,f150])).
% 4.04/0.98 fof(f2650,plain,(
% 4.04/0.98 n1=n0|sK7_skl(n1,filling)=tapOn),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2646,f220])).
% 4.04/0.98 fof(f2656,plain,(
% 4.04/0.98 releasedAt(filling,n1)|happens(tapOn,n1)|~releasedAt(filling,plus(n1,n1))|n1=n0),
% 4.04/0.98 inference(paramodulation,[status(thm)],[f2650,f93])).
% 4.04/0.98 fof(f2662,plain,(
% 4.04/0.98 releasedAt(filling,n1)|happens(tapOn,n1)|~releasedAt(filling,n2)|n1=n0),
% 4.04/0.98 inference(forward_demodulation,[status(thm)],[f161,f2656])).
% 4.04/0.98 fof(f2663,plain,(
% 4.04/0.98 releasedAt(filling,n1)|happens(tapOn,n1)|n1=n0),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2662,f2610])).
% 4.04/0.98 fof(f2672,plain,(
% 4.04/0.98 releasedAt(filling,n1)|n1=n0|sP1_prd(n1,tapOn)|tapOn=overflow),
% 4.04/0.98 inference(resolution,[status(thm)],[f2663,f138])).
% 4.04/0.98 fof(f2680,plain,(
% 4.04/0.98 releasedAt(filling,n1)|n1=n0|tapOn=overflow),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2672,f236])).
% 4.04/0.98 fof(f2681,plain,(
% 4.04/0.98 releasedAt(filling,n1)|n1=n0),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2680,f149])).
% 4.04/0.98 fof(f2682,plain,(
% 4.04/0.98 n1=n0|filling=waterLevel(sK9_skl(filling,sK7_skl(n0,filling)))|releasedAt(filling,n0)),
% 4.04/0.98 inference(resolution,[status(thm)],[f2681,f1720])).
% 4.04/0.98 fof(f2686,plain,(
% 4.04/0.98 n1=n0|releasedAt(filling,n0)),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2682,f150])).
% 4.04/0.98 fof(f2704,plain,(
% 4.04/0.98 less(n0,n0)),
% 4.04/0.98 inference(backward_demodulation,[status(thm)],[f2778,f2403])).
% 4.04/0.98 fof(f2778,plain,(
% 4.04/0.98 n1=n0),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2686,f220])).
% 4.04/0.98 fof(f2782,plain,(
% 4.04/0.98 $false),
% 4.04/0.98 inference(forward_subsumption_resolution,[status(thm)],[f2704,f174])).
% 4.04/0.98 % SZS output end CNFRefutation for theBenchmark.p
% 0.43/1.01 % Elapsed time: 0.655043 seconds
% 0.43/1.01 % CPU time: 4.827385 seconds
% 0.43/1.01 % Total memory used: 170.525 MB
% 0.43/1.01 % Net memory used: 165.157 MB
%------------------------------------------------------------------------------