%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR015+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 : n014.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.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR015+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.34 % Computer : n014.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 14:23:49 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.36 % Drodi V4.1.1
% 0.12/0.43 % Refutation found
% 0.12/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.43 fof(f6,axiom,(
% 0.12/0.43 (! [Fluent,Time] :( ( ~ holdsAt(Fluent,Time)& ~ releasedAt(Fluent,plus(Time,n1))& ~ (? [Event] :( happens(Event,Time)& initiates(Event,Fluent,Time) ) ))=> ~ holdsAt(Fluent,plus(Time,n1)) ) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f10,axiom,(
% 0.12/0.43 (! [Event,Time,Fluent] :( ( happens(Event,Time)& terminates(Event,Fluent,Time) )=> ~ holdsAt(Fluent,plus(Time,n1)) ) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f13,axiom,(
% 0.12/0.43 (! [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.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f14,axiom,(
% 0.12/0.43 (! [Event,Fluent,Time] :( terminates(Event,Fluent,Time)<=> ( ( Event = push& Fluent = backwards& ~ happens(pull,Time) )| ( Event = pull& Fluent = forwards& ~ happens(push,Time) )| ( Event = pull& Fluent = forwards& happens(push,Time) )| ( Event = pull& Fluent = backwards& happens(push,Time) )| ( Event = push& Fluent = spinning& ~ happens(pull,Time) )| ( Event = pull& Fluent = spinning& ~ happens(push,Time) ) ) ) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f16,axiom,(
% 0.12/0.43 (! [Event,Time] :( happens(Event,Time)<=> ( ( Event = push& Time = n0 )| ( Event = pull& Time = n1 )| ( Event = pull& Time = n2 )| ( Event = push& Time = n2 ) ) ) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f20,axiom,(
% 0.12/0.43 spinning != backwards ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f22,axiom,(
% 0.12/0.43 plus(n0,n1) = n1 ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f45,hypothesis,(
% 0.12/0.43 ~ holdsAt(backwards,n0) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f47,hypothesis,(
% 0.12/0.43 (! [Fluent,Time] : ~ releasedAt(Fluent,Time) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f48,conjecture,(
% 0.12/0.43 ~ holdsAt(backwards,n1) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f49,negated_conjecture,(
% 0.12/0.43 ~(~ holdsAt(backwards,n1) )),
% 0.12/0.43 inference(negated_conjecture,[status(cth)],[f48])).
% 0.12/0.43 fof(f76,plain,(
% 0.12/0.43 ![Fluent,Time]: (((holdsAt(Fluent,Time)|releasedAt(Fluent,plus(Time,n1)))|(?[Event]: (happens(Event,Time)&initiates(Event,Fluent,Time))))|~holdsAt(Fluent,plus(Time,n1)))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.12/0.43 fof(f77,plain,(
% 0.12/0.43 ![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.12/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(Event,sK5_skl(Time,Fluent))],[f76])).
% 0.12/0.43 fof(f79,plain,(
% 0.12/0.43 ![X0,X1]: (holdsAt(X0,X1)|releasedAt(X0,plus(X1,n1))|initiates(sK5_skl(X1,X0),X0,X1)|~holdsAt(X0,plus(X1,n1)))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f77])).
% 0.12/0.43 fof(f91,plain,(
% 0.12/0.43 ![Event,Time,Fluent]: ((~happens(Event,Time)|~terminates(Event,Fluent,Time))|~holdsAt(Fluent,plus(Time,n1)))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.12/0.43 fof(f92,plain,(
% 0.12/0.43 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~terminates(Event,Fluent,Time)))|~holdsAt(Fluent,plus(Time,n1)))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f91])).
% 0.12/0.43 fof(f93,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~happens(X0,X1)|~terminates(X0,X2,X1)|~holdsAt(X2,plus(X1,n1)))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f92])).
% 0.12/0.43 fof(f101,definition,(
% 0.12/0.43 ![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)<=>(((Event=push&Fluent=forwards)&~happens(pull,Time))|((Event=pull&Fluent=backwards)&~happens(push,Time))))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.12/0.43 fof(f102,plain,(
% 0.12/0.43 ![Event,Fluent,Time]: (initiates(Event,Fluent,Time)<=>(sP0_prd(Time,Fluent,Event)|((Event=pull&Fluent=spinning)&happens(push,Time))))),
% 0.12/0.43 inference(formula_renaming,[status(thm)],[f13,f101])).
% 0.12/0.43 fof(f103,plain,(
% 0.12/0.43 ![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.12/0.43 inference(NNF_transformation,[status(thm)],[f102])).
% 0.12/0.43 fof(f104,plain,(
% 0.12/0.43 (![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.12/0.43 inference(miniscoping,[status(thm)],[f103])).
% 0.12/0.43 fof(f106,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~initiates(X0,X1,X2)|sP0_prd(X2,X1,X0)|X1=spinning)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f104])).
% 0.12/0.43 fof(f110,definition,(
% 0.12/0.43 ![Event,Fluent,Time]: (sP1_prd(Time,Fluent,Event)<=>((((((Event=push&Fluent=backwards)&~happens(pull,Time))|((Event=pull&Fluent=forwards)&~happens(push,Time)))|((Event=pull&Fluent=forwards)&happens(push,Time)))|((Event=pull&Fluent=backwards)&happens(push,Time)))|((Event=push&Fluent=spinning)&~happens(pull,Time))))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.12/0.43 fof(f111,plain,(
% 0.12/0.43 ![Event,Fluent,Time]: (terminates(Event,Fluent,Time)<=>(sP1_prd(Time,Fluent,Event)|((Event=pull&Fluent=spinning)&~happens(push,Time))))),
% 0.12/0.43 inference(formula_renaming,[status(thm)],[f14,f110])).
% 0.12/0.43 fof(f112,plain,(
% 0.12/0.43 ![Event,Fluent,Time]: ((~terminates(Event,Fluent,Time)|(sP1_prd(Time,Fluent,Event)|((Event=pull&Fluent=spinning)&~happens(push,Time))))&(terminates(Event,Fluent,Time)|(~sP1_prd(Time,Fluent,Event)&((~Event=pull|~Fluent=spinning)|happens(push,Time)))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f111])).
% 0.12/0.43 fof(f113,plain,(
% 0.12/0.43 (![Event,Fluent,Time]: (~terminates(Event,Fluent,Time)|(sP1_prd(Time,Fluent,Event)|((Event=pull&Fluent=spinning)&~happens(push,Time)))))&(![Event,Fluent,Time]: (terminates(Event,Fluent,Time)|(~sP1_prd(Time,Fluent,Event)&((~Event=pull|~Fluent=spinning)|happens(push,Time)))))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f112])).
% 0.12/0.43 fof(f117,plain,(
% 0.12/0.43 ![X0,X1,X2]: (terminates(X0,X1,X2)|~sP1_prd(X2,X1,X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f113])).
% 0.12/0.43 fof(f120,definition,(
% 0.12/0.43 ![Event,Time]: (sP2_prd(Time,Event)<=>(((Event=push&Time=n0)|(Event=pull&Time=n1))|(Event=pull&Time=n2)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.12/0.43 fof(f121,plain,(
% 0.12/0.43 ![Event,Time]: (happens(Event,Time)<=>(sP2_prd(Time,Event)|(Event=push&Time=n2)))),
% 0.12/0.43 inference(formula_renaming,[status(thm)],[f16,f120])).
% 0.12/0.43 fof(f122,plain,(
% 0.12/0.43 ![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.12/0.43 inference(NNF_transformation,[status(thm)],[f121])).
% 0.12/0.43 fof(f123,plain,(
% 0.12/0.43 (![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.12/0.43 inference(miniscoping,[status(thm)],[f122])).
% 0.12/0.43 fof(f126,plain,(
% 0.12/0.43 ![X0,X1]: (happens(X0,X1)|~sP2_prd(X1,X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f123])).
% 0.12/0.43 fof(f131,plain,(
% 0.12/0.43 ~spinning=backwards),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f20])).
% 0.12/0.43 fof(f133,plain,(
% 0.12/0.43 plus(n0,n1)=n1),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f22])).
% 0.12/0.43 fof(f192,plain,(
% 0.12/0.43 ~holdsAt(backwards,n0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f45])).
% 0.12/0.43 fof(f194,plain,(
% 0.12/0.43 ![X0,X1]: (~releasedAt(X0,X1))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f47])).
% 0.12/0.43 fof(f195,plain,(
% 0.12/0.43 holdsAt(backwards,n1)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f49])).
% 0.12/0.43 fof(f196,definition,(
% 0.12/0.43 ![Event,Fluent,Time]: (sP3_prd(Time,Fluent,Event)<=>((Event=push&Fluent=forwards)&~happens(pull,Time)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.12/0.43 fof(f197,plain,(
% 0.12/0.43 ![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)<=>(sP3_prd(Time,Fluent,Event)|((Event=pull&Fluent=backwards)&~happens(push,Time))))),
% 0.12/0.43 inference(formula_renaming,[status(thm)],[f101,f196])).
% 0.12/0.43 fof(f198,plain,(
% 0.12/0.43 ![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.12/0.43 inference(NNF_transformation,[status(thm)],[f197])).
% 0.12/0.43 fof(f199,plain,(
% 0.12/0.43 (![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.12/0.43 inference(miniscoping,[status(thm)],[f198])).
% 0.12/0.43 fof(f202,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|sP3_prd(X0,X1,X2)|~happens(push,X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f199])).
% 0.12/0.43 fof(f205,definition,(
% 0.12/0.43 ![Event,Fluent,Time]: (sP4_prd(Time,Fluent,Event)<=>(((((Event=push&Fluent=backwards)&~happens(pull,Time))|((Event=pull&Fluent=forwards)&~happens(push,Time)))|((Event=pull&Fluent=forwards)&happens(push,Time)))|((Event=pull&Fluent=backwards)&happens(push,Time))))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.12/0.43 fof(f206,plain,(
% 0.12/0.43 ![Event,Fluent,Time]: (sP1_prd(Time,Fluent,Event)<=>(sP4_prd(Time,Fluent,Event)|((Event=push&Fluent=spinning)&~happens(pull,Time))))),
% 0.12/0.43 inference(formula_renaming,[status(thm)],[f110,f205])).
% 0.12/0.43 fof(f207,plain,(
% 0.12/0.43 ![Event,Fluent,Time]: ((~sP1_prd(Time,Fluent,Event)|(sP4_prd(Time,Fluent,Event)|((Event=push&Fluent=spinning)&~happens(pull,Time))))&(sP1_prd(Time,Fluent,Event)|(~sP4_prd(Time,Fluent,Event)&((~Event=push|~Fluent=spinning)|happens(pull,Time)))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f206])).
% 0.12/0.43 fof(f208,plain,(
% 0.12/0.43 (![Event,Fluent,Time]: (~sP1_prd(Time,Fluent,Event)|(sP4_prd(Time,Fluent,Event)|((Event=push&Fluent=spinning)&~happens(pull,Time)))))&(![Event,Fluent,Time]: (sP1_prd(Time,Fluent,Event)|(~sP4_prd(Time,Fluent,Event)&((~Event=push|~Fluent=spinning)|happens(pull,Time)))))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f207])).
% 0.12/0.43 fof(f212,plain,(
% 0.12/0.43 ![X0,X1,X2]: (sP1_prd(X0,X1,X2)|~sP4_prd(X0,X1,X2))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f208])).
% 0.12/0.43 fof(f214,definition,(
% 0.12/0.43 ![Event,Time]: (sP5_prd(Time,Event)<=>((Event=push&Time=n0)|(Event=pull&Time=n1)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.12/0.43 fof(f215,plain,(
% 0.12/0.43 ![Event,Time]: (sP2_prd(Time,Event)<=>(sP5_prd(Time,Event)|(Event=pull&Time=n2)))),
% 0.12/0.43 inference(formula_renaming,[status(thm)],[f120,f214])).
% 0.12/0.43 fof(f216,plain,(
% 0.12/0.43 ![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.12/0.43 inference(NNF_transformation,[status(thm)],[f215])).
% 0.12/0.43 fof(f217,plain,(
% 0.12/0.43 (![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.12/0.43 inference(miniscoping,[status(thm)],[f216])).
% 0.12/0.43 fof(f220,plain,(
% 0.12/0.43 ![X0,X1]: (sP2_prd(X0,X1)|~sP5_prd(X0,X1))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f217])).
% 0.12/0.43 fof(f222,plain,(
% 0.12/0.43 ![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.12/0.43 inference(NNF_transformation,[status(thm)],[f196])).
% 0.12/0.43 fof(f223,plain,(
% 0.12/0.43 (![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.12/0.43 inference(miniscoping,[status(thm)],[f222])).
% 0.12/0.43 fof(f226,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|~happens(pull,X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f223])).
% 0.12/0.43 fof(f228,definition,(
% 0.12/0.43 ![Event,Fluent,Time]: (sP6_prd(Time,Fluent,Event)<=>((((Event=push&Fluent=backwards)&~happens(pull,Time))|((Event=pull&Fluent=forwards)&~happens(push,Time)))|((Event=pull&Fluent=forwards)&happens(push,Time))))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.12/0.43 fof(f229,plain,(
% 0.12/0.43 ![Event,Fluent,Time]: (sP4_prd(Time,Fluent,Event)<=>(sP6_prd(Time,Fluent,Event)|((Event=pull&Fluent=backwards)&happens(push,Time))))),
% 0.12/0.43 inference(formula_renaming,[status(thm)],[f205,f228])).
% 0.12/0.43 fof(f230,plain,(
% 0.12/0.43 ![Event,Fluent,Time]: ((~sP4_prd(Time,Fluent,Event)|(sP6_prd(Time,Fluent,Event)|((Event=pull&Fluent=backwards)&happens(push,Time))))&(sP4_prd(Time,Fluent,Event)|(~sP6_prd(Time,Fluent,Event)&((~Event=pull|~Fluent=backwards)|~happens(push,Time)))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f229])).
% 0.12/0.43 fof(f231,plain,(
% 0.12/0.43 (![Event,Fluent,Time]: (~sP4_prd(Time,Fluent,Event)|(sP6_prd(Time,Fluent,Event)|((Event=pull&Fluent=backwards)&happens(push,Time)))))&(![Event,Fluent,Time]: (sP4_prd(Time,Fluent,Event)|(~sP6_prd(Time,Fluent,Event)&((~Event=pull|~Fluent=backwards)|~happens(push,Time)))))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f230])).
% 0.12/0.43 fof(f235,plain,(
% 0.12/0.43 ![X0,X1,X2]: (sP4_prd(X0,X1,X2)|~sP6_prd(X0,X1,X2))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f231])).
% 0.12/0.43 fof(f237,plain,(
% 0.12/0.43 ![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.12/0.43 inference(NNF_transformation,[status(thm)],[f214])).
% 0.12/0.43 fof(f238,plain,(
% 0.12/0.43 (![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.12/0.43 inference(miniscoping,[status(thm)],[f237])).
% 0.12/0.43 fof(f243,plain,(
% 0.12/0.43 ![X0,X1]: (sP5_prd(X0,X1)|~X1=push|~X0=n0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f238])).
% 0.12/0.43 fof(f245,definition,(
% 0.12/0.43 ![Event,Fluent,Time]: (sP7_prd(Time,Fluent,Event)<=>(((Event=push&Fluent=backwards)&~happens(pull,Time))|((Event=pull&Fluent=forwards)&~happens(push,Time))))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.12/0.43 fof(f246,plain,(
% 0.12/0.43 ![Event,Fluent,Time]: (sP6_prd(Time,Fluent,Event)<=>(sP7_prd(Time,Fluent,Event)|((Event=pull&Fluent=forwards)&happens(push,Time))))),
% 0.12/0.43 inference(formula_renaming,[status(thm)],[f228,f245])).
% 0.12/0.43 fof(f247,plain,(
% 0.12/0.43 ![Event,Fluent,Time]: ((~sP6_prd(Time,Fluent,Event)|(sP7_prd(Time,Fluent,Event)|((Event=pull&Fluent=forwards)&happens(push,Time))))&(sP6_prd(Time,Fluent,Event)|(~sP7_prd(Time,Fluent,Event)&((~Event=pull|~Fluent=forwards)|~happens(push,Time)))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f246])).
% 0.12/0.43 fof(f248,plain,(
% 0.12/0.43 (![Event,Fluent,Time]: (~sP6_prd(Time,Fluent,Event)|(sP7_prd(Time,Fluent,Event)|((Event=pull&Fluent=forwards)&happens(push,Time)))))&(![Event,Fluent,Time]: (sP6_prd(Time,Fluent,Event)|(~sP7_prd(Time,Fluent,Event)&((~Event=pull|~Fluent=forwards)|~happens(push,Time)))))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f247])).
% 0.12/0.43 fof(f252,plain,(
% 0.12/0.43 ![X0,X1,X2]: (sP6_prd(X0,X1,X2)|~sP7_prd(X0,X1,X2))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f248])).
% 0.12/0.43 fof(f254,definition,(
% 0.12/0.43 ![Event,Fluent,Time]: (sP8_prd(Time,Fluent,Event)<=>((Event=push&Fluent=backwards)&~happens(pull,Time)))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.12/0.43 fof(f255,plain,(
% 0.12/0.43 ![Event,Fluent,Time]: (sP7_prd(Time,Fluent,Event)<=>(sP8_prd(Time,Fluent,Event)|((Event=pull&Fluent=forwards)&~happens(push,Time))))),
% 0.12/0.43 inference(formula_renaming,[status(thm)],[f245,f254])).
% 0.12/0.43 fof(f256,plain,(
% 0.12/0.43 ![Event,Fluent,Time]: ((~sP7_prd(Time,Fluent,Event)|(sP8_prd(Time,Fluent,Event)|((Event=pull&Fluent=forwards)&~happens(push,Time))))&(sP7_prd(Time,Fluent,Event)|(~sP8_prd(Time,Fluent,Event)&((~Event=pull|~Fluent=forwards)|happens(push,Time)))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f255])).
% 0.12/0.43 fof(f257,plain,(
% 0.12/0.43 (![Event,Fluent,Time]: (~sP7_prd(Time,Fluent,Event)|(sP8_prd(Time,Fluent,Event)|((Event=pull&Fluent=forwards)&~happens(push,Time)))))&(![Event,Fluent,Time]: (sP7_prd(Time,Fluent,Event)|(~sP8_prd(Time,Fluent,Event)&((~Event=pull|~Fluent=forwards)|happens(push,Time)))))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f256])).
% 0.12/0.43 fof(f261,plain,(
% 0.12/0.43 ![X0,X1,X2]: (sP7_prd(X0,X1,X2)|~sP8_prd(X0,X1,X2))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f257])).
% 0.12/0.43 fof(f263,plain,(
% 0.12/0.43 ![Event,Fluent,Time]: ((~sP8_prd(Time,Fluent,Event)|((Event=push&Fluent=backwards)&~happens(pull,Time)))&(sP8_prd(Time,Fluent,Event)|((~Event=push|~Fluent=backwards)|happens(pull,Time))))),
% 0.12/0.44 inference(NNF_transformation,[status(thm)],[f254])).
% 0.12/0.44 fof(f264,plain,(
% 0.12/0.44 (![Event,Fluent,Time]: (~sP8_prd(Time,Fluent,Event)|((Event=push&Fluent=backwards)&~happens(pull,Time))))&(![Event,Fluent,Time]: (sP8_prd(Time,Fluent,Event)|((~Event=push|~Fluent=backwards)|happens(pull,Time))))),
% 0.12/0.44 inference(miniscoping,[status(thm)],[f263])).
% 0.12/0.44 fof(f268,plain,(
% 0.12/0.44 ![X0,X1,X2]: (sP8_prd(X0,X1,X2)|~X2=push|~X1=backwards|happens(pull,X0))),
% 0.12/0.44 inference(cnf_transformation,[status(thm)],[f264])).
% 0.12/0.44 fof(f275,plain,(
% 0.12/0.44 ![X0,X1]: (holdsAt(X0,X1)|initiates(sK5_skl(X1,X0),X0,X1)|~holdsAt(X0,plus(X1,n1)))),
% 0.12/0.44 inference(backward_subsumption_resolution,[status(thm)],[f79,f194])).
% 0.12/0.44 fof(f284,plain,(
% 0.12/0.44 sP5_prd(n0,push)),
% 0.12/0.44 inference(destructive_equality_resolution,[status(thm)],[f243])).
% 0.12/0.44 fof(f288,plain,(
% 0.12/0.44 ![X0]: (sP8_prd(X0,backwards,push)|happens(pull,X0))),
% 0.12/0.44 inference(destructive_equality_resolution,[status(thm)],[f268])).
% 0.12/0.44 fof(f313,plain,(
% 0.12/0.44 sP2_prd(n0,push)),
% 0.12/0.44 inference(resolution,[status(thm)],[f284,f220])).
% 0.12/0.44 fof(f318,plain,(
% 0.12/0.44 ![X0]: (happens(pull,X0)|sP7_prd(X0,backwards,push))),
% 0.12/0.44 inference(resolution,[status(thm)],[f288,f261])).
% 0.12/0.44 fof(f332,plain,(
% 0.12/0.44 happens(push,n0)),
% 0.12/0.44 inference(resolution,[status(thm)],[f313,f126])).
% 0.12/0.44 fof(f335,plain,(
% 0.12/0.44 ![X0]: (happens(pull,X0)|sP6_prd(X0,backwards,push))),
% 0.12/0.44 inference(resolution,[status(thm)],[f318,f252])).
% 0.12/0.44 fof(f345,plain,(
% 0.12/0.44 ![X0]: (happens(pull,X0)|sP4_prd(X0,backwards,push))),
% 0.12/0.44 inference(resolution,[status(thm)],[f335,f235])).
% 0.12/0.44 fof(f346,plain,(
% 0.12/0.44 ![X0]: (happens(pull,X0)|sP1_prd(X0,backwards,push))),
% 0.12/0.44 inference(resolution,[status(thm)],[f345,f212])).
% 0.12/0.44 fof(f347,plain,(
% 0.12/0.44 ![X0]: (happens(pull,X0)|terminates(push,backwards,X0))),
% 0.12/0.44 inference(resolution,[status(thm)],[f346,f117])).
% 0.12/0.44 fof(f350,plain,(
% 0.12/0.44 ![X0]: (happens(pull,X0)|~happens(push,X0)|~holdsAt(backwards,plus(X0,n1)))),
% 0.12/0.44 inference(resolution,[status(thm)],[f347,f93])).
% 0.12/0.44 fof(f514,plain,(
% 0.12/0.44 ![X0]: (holdsAt(X0,n0)|initiates(sK5_skl(n0,X0),X0,n0)|~holdsAt(X0,n1))),
% 0.12/0.44 inference(paramodulation,[status(thm)],[f133,f275])).
% 0.12/0.44 fof(f551,plain,(
% 0.12/0.44 happens(pull,n0)|~holdsAt(backwards,plus(n0,n1))),
% 0.12/0.44 inference(resolution,[status(thm)],[f350,f332])).
% 0.12/0.44 fof(f553,plain,(
% 0.12/0.44 happens(pull,n0)|~holdsAt(backwards,n1)),
% 0.12/0.44 inference(forward_demodulation,[status(thm)],[f133,f551])).
% 0.12/0.44 fof(f556,plain,(
% 0.12/0.44 happens(pull,n0)),
% 0.12/0.44 inference(forward_subsumption_resolution,[status(thm)],[f553,f195])).
% 0.12/0.44 fof(f915,plain,(
% 0.12/0.44 holdsAt(backwards,n0)|initiates(sK5_skl(n0,backwards),backwards,n0)),
% 0.12/0.44 inference(resolution,[status(thm)],[f514,f195])).
% 0.12/0.44 fof(f917,plain,(
% 0.12/0.44 initiates(sK5_skl(n0,backwards),backwards,n0)),
% 0.12/0.44 inference(forward_subsumption_resolution,[status(thm)],[f915,f192])).
% 0.12/0.44 fof(f928,plain,(
% 0.12/0.44 sP0_prd(n0,backwards,sK5_skl(n0,backwards))|backwards=spinning),
% 0.12/0.44 inference(resolution,[status(thm)],[f917,f106])).
% 0.12/0.44 fof(f932,plain,(
% 0.12/0.44 sP0_prd(n0,backwards,sK5_skl(n0,backwards))),
% 0.12/0.44 inference(forward_subsumption_resolution,[status(thm)],[f928,f131])).
% 0.12/0.44 fof(f939,plain,(
% 0.12/0.44 sP3_prd(n0,backwards,sK5_skl(n0,backwards))|~happens(push,n0)),
% 0.12/0.44 inference(resolution,[status(thm)],[f932,f202])).
% 0.12/0.44 fof(f943,plain,(
% 0.12/0.44 sP3_prd(n0,backwards,sK5_skl(n0,backwards))),
% 0.12/0.44 inference(forward_subsumption_resolution,[status(thm)],[f939,f332])).
% 0.12/0.44 fof(f948,plain,(
% 0.12/0.44 ~happens(pull,n0)),
% 0.12/0.44 inference(resolution,[status(thm)],[f943,f226])).
% 0.12/0.44 fof(f952,plain,(
% 0.12/0.44 $false),
% 0.12/0.44 inference(forward_subsumption_resolution,[status(thm)],[f948,f556])).
% 0.12/0.44 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.45 % Elapsed time: 0.101910 seconds
% 0.12/0.45 % CPU time: 0.559708 seconds
% 0.12/0.45 % Total memory used: 115.505 MB
% 0.12/0.45 % Net memory used: 114.835 MB
%------------------------------------------------------------------------------