%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR017+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:35 PM UTC 2026
% Result : Theorem 0.14s 5.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR017+1 : 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.09/5.36 % Computer : n016.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 14:28:58 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 0.14/5.52 % Refutation found
% 0.14/5.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.52 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.52 fof(f6,axiom,(
% 0.14/5.52 (! [Fluent,Time] :( ( ~ holdsAt(Fluent,Time)& ~ releasedAt(Fluent,plus(Time,n1))& ~ (? [Event] :( happens(Event,Time)& initiates(Event,Fluent,Time) ) ))=> ~ holdsAt(Fluent,plus(Time,n1)) ) )),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f13,axiom,(
% 0.14/5.52 (! [Event,Fluent,Time] :( initiates(Event,Fluent,Time)<=> ( ( Event = push& Fluent = forwards& ~ happens(pull,Time) )| ( Event = pull& Fluent = backwards& ~ happens(push,Time) )| ( Event = pull& Fluent = spinning& happens(push,Time) ) ) ) )),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f16,axiom,(
% 0.14/5.52 (! [Event,Time] :( happens(Event,Time)<=> ( ( Event = push& Time = n0 )| ( Event = pull& Time = n1 )| ( Event = pull& Time = n2 )| ( Event = push& Time = n2 ) ) ) )),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f17,axiom,(
% 0.14/5.52 push != pull ),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f19,axiom,(
% 0.14/5.52 forwards != spinning ),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f21,axiom,(
% 0.14/5.52 plus(n0,n0) = n0 ),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f22,axiom,(
% 0.14/5.52 plus(n0,n1) = n1 ),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f32,axiom,(
% 0.14/5.52 (! [X,Y] :( less_or_equal(X,Y)<=> ( less(X,Y)| X = Y ) ) )),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f33,axiom,(
% 0.14/5.52 ~ (? [X] : less(X,n0) )),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f34,axiom,(
% 0.14/5.52 (! [X] :( less(X,n1)<=> less_or_equal(X,n0) ) )),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f35,axiom,(
% 0.14/5.52 (! [X] :( less(X,n2)<=> less_or_equal(X,n1) ) )),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f43,axiom,(
% 0.14/5.52 (! [X,Y] :( less(X,Y)<=> ( ~ less(Y,X)& Y != X ) ) )),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f46,hypothesis,(
% 0.14/5.52 ~ holdsAt(spinning,n0) ),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f47,hypothesis,(
% 0.14/5.52 (! [Fluent,Time] : ~ releasedAt(Fluent,Time) )),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f48,conjecture,(
% 0.14/5.52 ~ holdsAt(spinning,n1) ),
% 0.14/5.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.52 fof(f49,negated_conjecture,(
% 0.14/5.52 ~(~ holdsAt(spinning,n1) )),
% 0.14/5.52 inference(negated_conjecture,[status(cth)],[f48])).
% 0.14/5.52 fof(f76,plain,(
% 0.14/5.52 ![Fluent,Time]: (((holdsAt(Fluent,Time)|releasedAt(Fluent,plus(Time,n1)))|(?[Event]: (happens(Event,Time)&initiates(Event,Fluent,Time))))|~holdsAt(Fluent,plus(Time,n1)))),
% 0.14/5.52 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.14/5.52 fof(f77,plain,(
% 0.14/5.52 ![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)))),
% 0.14/5.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(Event,sK5_skl(Time,Fluent))],[f76])).
% 0.14/5.52 fof(f78,plain,(
% 0.14/5.52 ![X0,X1]: (holdsAt(X0,X1)|releasedAt(X0,plus(X1,n1))|happens(sK5_skl(X1,X0),X1)|~holdsAt(X0,plus(X1,n1)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f77])).
% 0.14/5.52 fof(f79,plain,(
% 0.14/5.52 ![X0,X1]: (holdsAt(X0,X1)|releasedAt(X0,plus(X1,n1))|initiates(sK5_skl(X1,X0),X0,X1)|~holdsAt(X0,plus(X1,n1)))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f77])).
% 0.14/5.52 fof(f101,definition,(
% 0.14/5.52 ![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)<=>(((Event=push&Fluent=forwards)&~happens(pull,Time))|((Event=pull&Fluent=backwards)&~happens(push,Time))))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.14/5.52 fof(f102,plain,(
% 0.14/5.52 ![Event,Fluent,Time]: (initiates(Event,Fluent,Time)<=>(sP0_prd(Time,Fluent,Event)|((Event=pull&Fluent=spinning)&happens(push,Time))))),
% 0.14/5.52 inference(formula_renaming,[status(thm)],[f13,f101])).
% 0.14/5.52 fof(f103,plain,(
% 0.14/5.52 ![Event,Fluent,Time]: ((~initiates(Event,Fluent,Time)|(sP0_prd(Time,Fluent,Event)|((Event=pull&Fluent=spinning)&happens(push,Time))))&(initiates(Event,Fluent,Time)|(~sP0_prd(Time,Fluent,Event)&((~Event=pull|~Fluent=spinning)|~happens(push,Time)))))),
% 0.14/5.52 inference(NNF_transformation,[status(thm)],[f102])).
% 0.14/5.52 fof(f104,plain,(
% 0.14/5.52 (![Event,Fluent,Time]: (~initiates(Event,Fluent,Time)|(sP0_prd(Time,Fluent,Event)|((Event=pull&Fluent=spinning)&happens(push,Time)))))&(![Event,Fluent,Time]: (initiates(Event,Fluent,Time)|(~sP0_prd(Time,Fluent,Event)&((~Event=pull|~Fluent=spinning)|~happens(push,Time)))))),
% 0.14/5.52 inference(miniscoping,[status(thm)],[f103])).
% 0.14/5.52 fof(f105,plain,(
% 0.14/5.52 ![X0,X1,X2]: (~initiates(X0,X1,X2)|sP0_prd(X2,X1,X0)|X0=pull)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f104])).
% 0.14/5.52 fof(f120,definition,(
% 0.14/5.52 ![Event,Time]: (sP2_prd(Time,Event)<=>(((Event=push&Time=n0)|(Event=pull&Time=n1))|(Event=pull&Time=n2)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.14/5.52 fof(f121,plain,(
% 0.14/5.52 ![Event,Time]: (happens(Event,Time)<=>(sP2_prd(Time,Event)|(Event=push&Time=n2)))),
% 0.14/5.52 inference(formula_renaming,[status(thm)],[f16,f120])).
% 0.14/5.52 fof(f122,plain,(
% 0.14/5.52 ![Event,Time]: ((~happens(Event,Time)|(sP2_prd(Time,Event)|(Event=push&Time=n2)))&(happens(Event,Time)|(~sP2_prd(Time,Event)&(~Event=push|~Time=n2))))),
% 0.14/5.52 inference(NNF_transformation,[status(thm)],[f121])).
% 0.14/5.52 fof(f123,plain,(
% 0.14/5.52 (![Event,Time]: (~happens(Event,Time)|(sP2_prd(Time,Event)|(Event=push&Time=n2))))&(![Event,Time]: (happens(Event,Time)|(~sP2_prd(Time,Event)&(~Event=push|~Time=n2))))),
% 0.14/5.52 inference(miniscoping,[status(thm)],[f122])).
% 0.14/5.52 fof(f125,plain,(
% 0.14/5.52 ![X0,X1]: (~happens(X0,X1)|sP2_prd(X1,X0)|X1=n2)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f123])).
% 0.14/5.52 fof(f126,plain,(
% 0.14/5.52 ![X0,X1]: (happens(X0,X1)|~sP2_prd(X1,X0))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f123])).
% 0.14/5.52 fof(f128,plain,(
% 0.14/5.52 ~push=pull),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f17])).
% 0.14/5.52 fof(f130,plain,(
% 0.14/5.52 ~forwards=spinning),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f19])).
% 0.14/5.52 fof(f132,plain,(
% 0.14/5.52 plus(n0,n0)=n0),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f21])).
% 0.14/5.52 fof(f133,plain,(
% 0.14/5.52 plus(n0,n1)=n1),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f22])).
% 0.14/5.52 fof(f143,plain,(
% 0.14/5.52 ![X,Y]: ((~less_or_equal(X,Y)|(less(X,Y)|X=Y))&(less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 0.14/5.52 inference(NNF_transformation,[status(thm)],[f32])).
% 0.14/5.52 fof(f144,plain,(
% 0.14/5.52 (![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.14/5.52 inference(miniscoping,[status(thm)],[f143])).
% 0.14/5.52 fof(f147,plain,(
% 0.14/5.52 ![X0,X1]: (less_or_equal(X0,X1)|~X0=X1)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f144])).
% 0.14/5.52 fof(f148,plain,(
% 0.14/5.52 (![X]: ~less(X,n0))),
% 0.14/5.52 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.14/5.52 fof(f149,plain,(
% 0.14/5.52 ![X0]: (~less(X0,n0))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f148])).
% 0.14/5.52 fof(f150,plain,(
% 0.14/5.52 ![X]: ((~less(X,n1)|less_or_equal(X,n0))&(less(X,n1)|~less_or_equal(X,n0)))),
% 0.14/5.52 inference(NNF_transformation,[status(thm)],[f34])).
% 0.14/5.52 fof(f151,plain,(
% 0.14/5.52 (![X]: (~less(X,n1)|less_or_equal(X,n0)))&(![X]: (less(X,n1)|~less_or_equal(X,n0)))),
% 0.14/5.52 inference(miniscoping,[status(thm)],[f150])).
% 0.14/5.52 fof(f153,plain,(
% 0.14/5.52 ![X0]: (less(X0,n1)|~less_or_equal(X0,n0))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f151])).
% 0.14/5.52 fof(f154,plain,(
% 0.14/5.52 ![X]: ((~less(X,n2)|less_or_equal(X,n1))&(less(X,n2)|~less_or_equal(X,n1)))),
% 0.14/5.52 inference(NNF_transformation,[status(thm)],[f35])).
% 0.14/5.52 fof(f155,plain,(
% 0.14/5.52 (![X]: (~less(X,n2)|less_or_equal(X,n1)))&(![X]: (less(X,n2)|~less_or_equal(X,n1)))),
% 0.14/5.52 inference(miniscoping,[status(thm)],[f154])).
% 0.14/5.52 fof(f157,plain,(
% 0.14/5.52 ![X0]: (less(X0,n2)|~less_or_equal(X0,n1))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f155])).
% 0.14/5.52 fof(f186,plain,(
% 0.14/5.52 ![X,Y]: ((~less(X,Y)|(~less(Y,X)&~Y=X))&(less(X,Y)|(less(Y,X)|Y=X)))),
% 0.14/5.52 inference(NNF_transformation,[status(thm)],[f43])).
% 0.14/5.52 fof(f187,plain,(
% 0.14/5.52 (![X,Y]: (~less(X,Y)|(~less(Y,X)&~Y=X)))&(![X,Y]: (less(X,Y)|(less(Y,X)|Y=X)))),
% 0.14/5.52 inference(miniscoping,[status(thm)],[f186])).
% 0.14/5.52 fof(f188,plain,(
% 0.14/5.52 ![X0,X1]: (~less(X0,X1)|~less(X1,X0))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f187])).
% 0.14/5.52 fof(f193,plain,(
% 0.14/5.52 ~holdsAt(spinning,n0)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f46])).
% 0.14/5.52 fof(f194,plain,(
% 0.14/5.52 ![X0,X1]: (~releasedAt(X0,X1))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f47])).
% 0.14/5.52 fof(f195,plain,(
% 0.14/5.52 holdsAt(spinning,n1)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f49])).
% 0.14/5.52 fof(f196,definition,(
% 0.14/5.52 ![Event,Fluent,Time]: (sP3_prd(Time,Fluent,Event)<=>((Event=push&Fluent=forwards)&~happens(pull,Time)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.14/5.52 fof(f197,plain,(
% 0.14/5.52 ![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)<=>(sP3_prd(Time,Fluent,Event)|((Event=pull&Fluent=backwards)&~happens(push,Time))))),
% 0.14/5.52 inference(formula_renaming,[status(thm)],[f101,f196])).
% 0.14/5.52 fof(f198,plain,(
% 0.14/5.52 ![Event,Fluent,Time]: ((~sP0_prd(Time,Fluent,Event)|(sP3_prd(Time,Fluent,Event)|((Event=pull&Fluent=backwards)&~happens(push,Time))))&(sP0_prd(Time,Fluent,Event)|(~sP3_prd(Time,Fluent,Event)&((~Event=pull|~Fluent=backwards)|happens(push,Time)))))),
% 0.14/5.52 inference(NNF_transformation,[status(thm)],[f197])).
% 0.14/5.52 fof(f199,plain,(
% 0.14/5.52 (![Event,Fluent,Time]: (~sP0_prd(Time,Fluent,Event)|(sP3_prd(Time,Fluent,Event)|((Event=pull&Fluent=backwards)&~happens(push,Time)))))&(![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)|(~sP3_prd(Time,Fluent,Event)&((~Event=pull|~Fluent=backwards)|happens(push,Time)))))),
% 0.14/5.52 inference(miniscoping,[status(thm)],[f198])).
% 0.14/5.52 fof(f202,plain,(
% 0.14/5.52 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|sP3_prd(X0,X1,X2)|~happens(push,X0))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f199])).
% 0.14/5.52 fof(f214,definition,(
% 0.14/5.52 ![Event,Time]: (sP5_prd(Time,Event)<=>((Event=push&Time=n0)|(Event=pull&Time=n1)))),
% 0.14/5.52 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.14/5.52 fof(f215,plain,(
% 0.14/5.52 ![Event,Time]: (sP2_prd(Time,Event)<=>(sP5_prd(Time,Event)|(Event=pull&Time=n2)))),
% 0.14/5.52 inference(formula_renaming,[status(thm)],[f120,f214])).
% 0.14/5.52 fof(f216,plain,(
% 0.14/5.52 ![Event,Time]: ((~sP2_prd(Time,Event)|(sP5_prd(Time,Event)|(Event=pull&Time=n2)))&(sP2_prd(Time,Event)|(~sP5_prd(Time,Event)&(~Event=pull|~Time=n2))))),
% 0.14/5.52 inference(NNF_transformation,[status(thm)],[f215])).
% 0.14/5.52 fof(f217,plain,(
% 0.14/5.52 (![Event,Time]: (~sP2_prd(Time,Event)|(sP5_prd(Time,Event)|(Event=pull&Time=n2))))&(![Event,Time]: (sP2_prd(Time,Event)|(~sP5_prd(Time,Event)&(~Event=pull|~Time=n2))))),
% 0.14/5.52 inference(miniscoping,[status(thm)],[f216])).
% 0.14/5.52 fof(f219,plain,(
% 0.14/5.52 ![X0,X1]: (~sP2_prd(X0,X1)|sP5_prd(X0,X1)|X0=n2)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f217])).
% 0.14/5.52 fof(f220,plain,(
% 0.14/5.52 ![X0,X1]: (sP2_prd(X0,X1)|~sP5_prd(X0,X1))),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f217])).
% 0.14/5.52 fof(f222,plain,(
% 0.14/5.52 ![Event,Fluent,Time]: ((~sP3_prd(Time,Fluent,Event)|((Event=push&Fluent=forwards)&~happens(pull,Time)))&(sP3_prd(Time,Fluent,Event)|((~Event=push|~Fluent=forwards)|happens(pull,Time))))),
% 0.14/5.52 inference(NNF_transformation,[status(thm)],[f196])).
% 0.14/5.52 fof(f223,plain,(
% 0.14/5.52 (![Event,Fluent,Time]: (~sP3_prd(Time,Fluent,Event)|((Event=push&Fluent=forwards)&~happens(pull,Time))))&(![Event,Fluent,Time]: (sP3_prd(Time,Fluent,Event)|((~Event=push|~Fluent=forwards)|happens(pull,Time))))),
% 0.14/5.52 inference(miniscoping,[status(thm)],[f222])).
% 0.14/5.52 fof(f225,plain,(
% 0.14/5.52 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|X1=forwards)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f223])).
% 0.14/5.52 fof(f237,plain,(
% 0.14/5.52 ![Event,Time]: ((~sP5_prd(Time,Event)|((Event=push&Time=n0)|(Event=pull&Time=n1)))&(sP5_prd(Time,Event)|((~Event=push|~Time=n0)&(~Event=pull|~Time=n1))))),
% 0.14/5.52 inference(NNF_transformation,[status(thm)],[f214])).
% 0.14/5.52 fof(f238,plain,(
% 0.14/5.52 (![Event,Time]: (~sP5_prd(Time,Event)|((Event=push&Time=n0)|(Event=pull&Time=n1))))&(![Event,Time]: (sP5_prd(Time,Event)|((~Event=push|~Time=n0)&(~Event=pull|~Time=n1))))),
% 0.14/5.52 inference(miniscoping,[status(thm)],[f237])).
% 0.14/5.52 fof(f240,plain,(
% 0.14/5.52 ![X0,X1]: (~sP5_prd(X0,X1)|X1=push|X0=n1)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f238])).
% 0.14/5.52 fof(f243,plain,(
% 0.14/5.52 ![X0,X1]: (sP5_prd(X0,X1)|~X1=push|~X0=n0)),
% 0.14/5.52 inference(cnf_transformation,[status(thm)],[f238])).
% 0.14/5.52 fof(f269,plain,(
% 0.14/5.52 ![X0]: (less_or_equal(X0,X0))),
% 0.14/5.52 inference(destructive_equality_resolution,[status(thm)],[f147])).
% 0.14/5.52 fof(f287,plain,(
% 0.14/5.52 less(n0,n1)),
% 0.14/5.52 inference(resolution,[status(thm)],[f153,f269])).
% 0.14/5.52 fof(f294,plain,(
% 0.14/5.52 less(n1,n2)),
% 0.14/5.52 inference(resolution,[status(thm)],[f157,f269])).
% 0.14/5.52 fof(f301,plain,(
% 0.14/5.52 ~less(n2,n1)),
% 0.14/5.52 inference(resolution,[status(thm)],[f294,f188])).
% 0.14/5.53 fof(f437,plain,(
% 0.14/5.53 ![X0,X1]: (holdsAt(X0,X1)|happens(sK5_skl(X1,X0),X1)|~holdsAt(X0,plus(X1,n1)))),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f78,f194])).
% 0.14/5.53 fof(f439,plain,(
% 0.14/5.53 ![X0]: (holdsAt(X0,n0)|happens(sK5_skl(n0,X0),n0)|~holdsAt(X0,n1))),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f133,f437])).
% 0.14/5.53 fof(f442,plain,(
% 0.14/5.53 ![X0,X1]: (holdsAt(X0,X1)|initiates(sK5_skl(X1,X0),X0,X1)|~holdsAt(X0,plus(X1,n1)))),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f79,f194])).
% 0.14/5.53 fof(f444,plain,(
% 0.14/5.53 ![X0]: (holdsAt(X0,n0)|initiates(sK5_skl(n0,X0),X0,n0)|~holdsAt(X0,n1))),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f133,f442])).
% 0.14/5.53 fof(f819,plain,(
% 0.14/5.53 ![X0]: (sP5_prd(X0,push)|~X0=n0)),
% 0.14/5.53 inference(equality_resolution,[status(thm)],[f243])).
% 0.14/5.53 fof(f820,plain,(
% 0.14/5.53 sP5_prd(plus(n0,n0),push)),
% 0.14/5.53 inference(resolution,[status(thm)],[f819,f132])).
% 0.14/5.53 fof(f822,plain,(
% 0.14/5.53 sP5_prd(n0,push)),
% 0.14/5.53 inference(forward_demodulation,[status(thm)],[f132,f820])).
% 0.14/5.53 fof(f827,plain,(
% 0.14/5.53 sP2_prd(n0,push)),
% 0.14/5.53 inference(resolution,[status(thm)],[f822,f220])).
% 0.14/5.53 fof(f828,plain,(
% 0.14/5.53 happens(push,n0)),
% 0.14/5.53 inference(resolution,[status(thm)],[f827,f126])).
% 0.14/5.53 fof(f1759,plain,(
% 0.14/5.53 holdsAt(spinning,n0)|happens(sK5_skl(n0,spinning),n0)),
% 0.14/5.53 inference(resolution,[status(thm)],[f439,f195])).
% 0.14/5.53 fof(f1760,plain,(
% 0.14/5.53 happens(sK5_skl(n0,spinning),n0)),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1759,f193])).
% 0.14/5.53 fof(f1761,plain,(
% 0.14/5.53 sP2_prd(n0,sK5_skl(n0,spinning))|n0=n2),
% 0.14/5.53 inference(resolution,[status(thm)],[f1760,f125])).
% 0.14/5.53 fof(f1763,plain,(
% 0.14/5.53 n0=n2|sP5_prd(n0,sK5_skl(n0,spinning))|n0=n2),
% 0.14/5.53 inference(resolution,[status(thm)],[f1761,f219])).
% 0.14/5.53 fof(f1766,plain,(
% 0.14/5.53 n0=n2|sP5_prd(n0,sK5_skl(n0,spinning))),
% 0.14/5.53 inference(duplicate_literals_removal,[status(thm)],[f1763])).
% 0.14/5.53 fof(f1769,plain,(
% 0.14/5.53 n0=n2|sK5_skl(n0,spinning)=push|n0=n1),
% 0.14/5.53 inference(resolution,[status(thm)],[f1766,f240])).
% 0.14/5.53 fof(f2785,plain,(
% 0.14/5.53 holdsAt(spinning,n0)|initiates(sK5_skl(n0,spinning),spinning,n0)),
% 0.14/5.53 inference(resolution,[status(thm)],[f444,f195])).
% 0.14/5.53 fof(f2786,plain,(
% 0.14/5.53 initiates(sK5_skl(n0,spinning),spinning,n0)),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2785,f193])).
% 0.14/5.53 fof(f2798,plain,(
% 0.14/5.53 initiates(push,spinning,n0)|n0=n2|n0=n1),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f1769,f2786])).
% 0.14/5.53 fof(f2803,plain,(
% 0.14/5.53 n0=n2|n0=n1|sP0_prd(n0,spinning,push)|push=pull),
% 0.14/5.53 inference(resolution,[status(thm)],[f2798,f105])).
% 0.14/5.53 fof(f2806,plain,(
% 0.14/5.53 n0=n2|n0=n1|sP0_prd(n0,spinning,push)),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2803,f128])).
% 0.14/5.53 fof(f2809,plain,(
% 0.14/5.53 n0=n2|n0=n1|sP3_prd(n0,spinning,push)|~happens(push,n0)),
% 0.14/5.53 inference(resolution,[status(thm)],[f2806,f202])).
% 0.14/5.53 fof(f2813,plain,(
% 0.14/5.53 n0=n2|n0=n1|sP3_prd(n0,spinning,push)),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2809,f828])).
% 0.14/5.53 fof(f2818,plain,(
% 0.14/5.53 n0=n2|n0=n1|spinning=forwards),
% 0.14/5.53 inference(resolution,[status(thm)],[f2813,f225])).
% 0.14/5.53 fof(f2820,plain,(
% 0.14/5.53 n0=n2|n0=n1),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2818,f130])).
% 0.14/5.53 fof(f2891,plain,(
% 0.14/5.53 ~less(n0,n1)|n0=n1),
% 0.14/5.53 inference(paramodulation,[status(thm)],[f2820,f301])).
% 0.14/5.53 fof(f2914,plain,(
% 0.14/5.53 n0=n1),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2891,f287])).
% 0.14/5.53 fof(f3053,plain,(
% 0.14/5.53 less(n0,n0)),
% 0.14/5.53 inference(backward_demodulation,[status(thm)],[f2914,f287])).
% 0.14/5.53 fof(f3137,plain,(
% 0.14/5.53 $false),
% 0.14/5.53 inference(forward_subsumption_resolution,[status(thm)],[f3053,f149])).
% 0.14/5.53 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.55 % Elapsed time: 0.169711 seconds
% 0.14/5.55 % CPU time: 1.116498 seconds
% 0.14/5.55 % Total memory used: 125.257 MB
% 0.14/5.55 % Net memory used: 123.462 MB
%------------------------------------------------------------------------------