%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR020+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 : n013.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.13s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR020+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.08/0.35 % Computer : n013.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:06 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.48 % Refutation found
% 0.13/0.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.48 fof(f10,axiom,(
% 0.13/0.48 (! [Event,Time,Fluent] :( ( happens(Event,Time)& terminates(Event,Fluent,Time) )=> ~ holdsAt(Fluent,plus(Time,n1)) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f13,axiom,(
% 0.13/0.48 (! [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.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f14,axiom,(
% 0.13/0.48 (! [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.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f16,axiom,(
% 0.13/0.48 (! [Event,Time] :( happens(Event,Time)<=> ( ( Event = push& Time = n0 )| ( Event = pull& Time = n1 )| ( Event = pull& Time = n2 )| ( Event = push& Time = n2 ) ) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f17,axiom,(
% 0.13/0.48 push != pull ),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f19,axiom,(
% 0.13/0.48 forwards != spinning ),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f20,axiom,(
% 0.13/0.48 spinning != backwards ),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f25,axiom,(
% 0.13/0.48 plus(n1,n1) = n2 ),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f32,axiom,(
% 0.13/0.48 (! [X,Y] :( less_or_equal(X,Y)<=> ( less(X,Y)| X = Y ) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f34,axiom,(
% 0.13/0.48 (! [X] :( less(X,n1)<=> less_or_equal(X,n0) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f35,axiom,(
% 0.13/0.48 (! [X] :( less(X,n2)<=> less_or_equal(X,n1) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f36,axiom,(
% 0.13/0.48 (! [X] :( less(X,n3)<=> less_or_equal(X,n2) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f37,axiom,(
% 0.13/0.48 (! [X] :( less(X,n4)<=> less_or_equal(X,n3) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f38,axiom,(
% 0.13/0.48 (! [X] :( less(X,n5)<=> less_or_equal(X,n4) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f39,axiom,(
% 0.13/0.48 (! [X] :( less(X,n6)<=> less_or_equal(X,n5) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f40,axiom,(
% 0.13/0.48 (! [X] :( less(X,n7)<=> less_or_equal(X,n6) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f41,axiom,(
% 0.13/0.48 (! [X] :( less(X,n8)<=> less_or_equal(X,n7) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f42,axiom,(
% 0.13/0.48 (! [X] :( less(X,n9)<=> less_or_equal(X,n8) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f43,axiom,(
% 0.13/0.48 (! [X,Y] :( less(X,Y)<=> ( ~ less(Y,X)& Y != X ) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f48,conjecture,(
% 0.13/0.48 ~ holdsAt(spinning,n2) ),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f49,negated_conjecture,(
% 0.13/0.48 ~(~ holdsAt(spinning,n2) )),
% 0.13/0.48 inference(negated_conjecture,[status(cth)],[f48])).
% 0.13/0.48 fof(f91,plain,(
% 0.13/0.48 ![Event,Time,Fluent]: ((~happens(Event,Time)|~terminates(Event,Fluent,Time))|~holdsAt(Fluent,plus(Time,n1)))),
% 0.13/0.48 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.13/0.48 fof(f92,plain,(
% 0.13/0.48 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~terminates(Event,Fluent,Time)))|~holdsAt(Fluent,plus(Time,n1)))),
% 0.13/0.48 inference(miniscoping,[status(thm)],[f91])).
% 0.13/0.48 fof(f93,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~happens(X0,X1)|~terminates(X0,X2,X1)|~holdsAt(X2,plus(X1,n1)))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f92])).
% 0.13/0.48 fof(f101,definition,(
% 0.13/0.48 ![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)<=>(((Event=push&Fluent=forwards)&~happens(pull,Time))|((Event=pull&Fluent=backwards)&~happens(push,Time))))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.13/0.48 fof(f110,definition,(
% 0.13/0.48 ![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.13/0.48 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.13/0.48 fof(f111,plain,(
% 0.13/0.48 ![Event,Fluent,Time]: (terminates(Event,Fluent,Time)<=>(sP1_prd(Time,Fluent,Event)|((Event=pull&Fluent=spinning)&~happens(push,Time))))),
% 0.13/0.48 inference(formula_renaming,[status(thm)],[f14,f110])).
% 0.13/0.48 fof(f112,plain,(
% 0.13/0.48 ![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.13/0.48 inference(NNF_transformation,[status(thm)],[f111])).
% 0.13/0.48 fof(f113,plain,(
% 0.13/0.48 (![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.13/0.48 inference(miniscoping,[status(thm)],[f112])).
% 0.13/0.48 fof(f118,plain,(
% 0.13/0.48 ![X0,X1,X2]: (terminates(X0,X1,X2)|~X0=pull|~X1=spinning|happens(push,X2))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f113])).
% 0.13/0.48 fof(f120,definition,(
% 0.13/0.48 ![Event,Time]: (sP2_prd(Time,Event)<=>(((Event=push&Time=n0)|(Event=pull&Time=n1))|(Event=pull&Time=n2)))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.13/0.48 fof(f121,plain,(
% 0.13/0.48 ![Event,Time]: (happens(Event,Time)<=>(sP2_prd(Time,Event)|(Event=push&Time=n2)))),
% 0.13/0.48 inference(formula_renaming,[status(thm)],[f16,f120])).
% 0.13/0.48 fof(f122,plain,(
% 0.13/0.48 ![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.13/0.48 inference(NNF_transformation,[status(thm)],[f121])).
% 0.13/0.48 fof(f123,plain,(
% 0.13/0.48 (![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.13/0.48 inference(miniscoping,[status(thm)],[f122])).
% 0.13/0.48 fof(f125,plain,(
% 0.13/0.48 ![X0,X1]: (~happens(X0,X1)|sP2_prd(X1,X0)|X1=n2)),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f123])).
% 0.13/0.48 fof(f126,plain,(
% 0.13/0.48 ![X0,X1]: (happens(X0,X1)|~sP2_prd(X1,X0))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f123])).
% 0.13/0.48 fof(f128,plain,(
% 0.13/0.48 ~push=pull),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.48 fof(f130,plain,(
% 0.13/0.48 ~forwards=spinning),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f19])).
% 0.13/0.48 fof(f131,plain,(
% 0.13/0.48 ~spinning=backwards),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f20])).
% 0.13/0.48 fof(f136,plain,(
% 0.13/0.48 plus(n1,n1)=n2),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f25])).
% 0.13/0.48 fof(f143,plain,(
% 0.13/0.48 ![X,Y]: ((~less_or_equal(X,Y)|(less(X,Y)|X=Y))&(less_or_equal(X,Y)|(~less(X,Y)&~X=Y)))),
% 0.13/0.48 inference(NNF_transformation,[status(thm)],[f32])).
% 0.13/0.48 fof(f144,plain,(
% 0.13/0.48 (![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.13/0.48 inference(miniscoping,[status(thm)],[f143])).
% 0.13/0.48 fof(f146,plain,(
% 0.13/0.48 ![X0,X1]: (less_or_equal(X0,X1)|~less(X0,X1))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f144])).
% 0.13/0.48 fof(f147,plain,(
% 0.13/0.48 ![X0,X1]: (less_or_equal(X0,X1)|~X0=X1)),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f144])).
% 0.13/0.48 fof(f150,plain,(
% 0.13/0.48 ![X]: ((~less(X,n1)|less_or_equal(X,n0))&(less(X,n1)|~less_or_equal(X,n0)))),
% 0.13/0.48 inference(NNF_transformation,[status(thm)],[f34])).
% 0.13/0.48 fof(f151,plain,(
% 0.13/0.48 (![X]: (~less(X,n1)|less_or_equal(X,n0)))&(![X]: (less(X,n1)|~less_or_equal(X,n0)))),
% 0.13/0.48 inference(miniscoping,[status(thm)],[f150])).
% 0.13/0.48 fof(f153,plain,(
% 0.13/0.48 ![X0]: (less(X0,n1)|~less_or_equal(X0,n0))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f151])).
% 0.13/0.48 fof(f154,plain,(
% 0.13/0.48 ![X]: ((~less(X,n2)|less_or_equal(X,n1))&(less(X,n2)|~less_or_equal(X,n1)))),
% 0.13/0.48 inference(NNF_transformation,[status(thm)],[f35])).
% 0.13/0.48 fof(f155,plain,(
% 0.13/0.48 (![X]: (~less(X,n2)|less_or_equal(X,n1)))&(![X]: (less(X,n2)|~less_or_equal(X,n1)))),
% 0.13/0.48 inference(miniscoping,[status(thm)],[f154])).
% 0.13/0.48 fof(f157,plain,(
% 0.13/0.48 ![X0]: (less(X0,n2)|~less_or_equal(X0,n1))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f155])).
% 0.13/0.48 fof(f158,plain,(
% 0.13/0.48 ![X]: ((~less(X,n3)|less_or_equal(X,n2))&(less(X,n3)|~less_or_equal(X,n2)))),
% 0.13/0.48 inference(NNF_transformation,[status(thm)],[f36])).
% 0.13/0.48 fof(f159,plain,(
% 0.13/0.48 (![X]: (~less(X,n3)|less_or_equal(X,n2)))&(![X]: (less(X,n3)|~less_or_equal(X,n2)))),
% 0.13/0.48 inference(miniscoping,[status(thm)],[f158])).
% 0.13/0.48 fof(f161,plain,(
% 0.13/0.48 ![X0]: (less(X0,n3)|~less_or_equal(X0,n2))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f159])).
% 0.13/0.48 fof(f162,plain,(
% 0.13/0.48 ![X]: ((~less(X,n4)|less_or_equal(X,n3))&(less(X,n4)|~less_or_equal(X,n3)))),
% 0.13/0.48 inference(NNF_transformation,[status(thm)],[f37])).
% 0.13/0.48 fof(f163,plain,(
% 0.13/0.48 (![X]: (~less(X,n4)|less_or_equal(X,n3)))&(![X]: (less(X,n4)|~less_or_equal(X,n3)))),
% 0.13/0.48 inference(miniscoping,[status(thm)],[f162])).
% 0.13/0.48 fof(f165,plain,(
% 0.13/0.48 ![X0]: (less(X0,n4)|~less_or_equal(X0,n3))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f163])).
% 0.13/0.48 fof(f166,plain,(
% 0.13/0.48 ![X]: ((~less(X,n5)|less_or_equal(X,n4))&(less(X,n5)|~less_or_equal(X,n4)))),
% 0.13/0.48 inference(NNF_transformation,[status(thm)],[f38])).
% 0.13/0.48 fof(f167,plain,(
% 0.13/0.48 (![X]: (~less(X,n5)|less_or_equal(X,n4)))&(![X]: (less(X,n5)|~less_or_equal(X,n4)))),
% 0.13/0.48 inference(miniscoping,[status(thm)],[f166])).
% 0.13/0.48 fof(f169,plain,(
% 0.13/0.48 ![X0]: (less(X0,n5)|~less_or_equal(X0,n4))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f167])).
% 0.13/0.48 fof(f170,plain,(
% 0.13/0.48 ![X]: ((~less(X,n6)|less_or_equal(X,n5))&(less(X,n6)|~less_or_equal(X,n5)))),
% 0.13/0.48 inference(NNF_transformation,[status(thm)],[f39])).
% 0.13/0.48 fof(f171,plain,(
% 0.13/0.48 (![X]: (~less(X,n6)|less_or_equal(X,n5)))&(![X]: (less(X,n6)|~less_or_equal(X,n5)))),
% 0.13/0.48 inference(miniscoping,[status(thm)],[f170])).
% 0.13/0.48 fof(f173,plain,(
% 0.13/0.48 ![X0]: (less(X0,n6)|~less_or_equal(X0,n5))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f171])).
% 0.13/0.48 fof(f174,plain,(
% 0.13/0.48 ![X]: ((~less(X,n7)|less_or_equal(X,n6))&(less(X,n7)|~less_or_equal(X,n6)))),
% 0.13/0.48 inference(NNF_transformation,[status(thm)],[f40])).
% 0.13/0.48 fof(f175,plain,(
% 0.13/0.48 (![X]: (~less(X,n7)|less_or_equal(X,n6)))&(![X]: (less(X,n7)|~less_or_equal(X,n6)))),
% 0.13/0.48 inference(miniscoping,[status(thm)],[f174])).
% 0.13/0.48 fof(f177,plain,(
% 0.13/0.48 ![X0]: (less(X0,n7)|~less_or_equal(X0,n6))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f175])).
% 0.13/0.48 fof(f178,plain,(
% 0.13/0.48 ![X]: ((~less(X,n8)|less_or_equal(X,n7))&(less(X,n8)|~less_or_equal(X,n7)))),
% 0.13/0.48 inference(NNF_transformation,[status(thm)],[f41])).
% 0.13/0.48 fof(f179,plain,(
% 0.13/0.48 (![X]: (~less(X,n8)|less_or_equal(X,n7)))&(![X]: (less(X,n8)|~less_or_equal(X,n7)))),
% 0.13/0.48 inference(miniscoping,[status(thm)],[f178])).
% 0.13/0.48 fof(f181,plain,(
% 0.13/0.48 ![X0]: (less(X0,n8)|~less_or_equal(X0,n7))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f179])).
% 0.13/0.48 fof(f182,plain,(
% 0.13/0.48 ![X]: ((~less(X,n9)|less_or_equal(X,n8))&(less(X,n9)|~less_or_equal(X,n8)))),
% 0.13/0.48 inference(NNF_transformation,[status(thm)],[f42])).
% 0.13/0.48 fof(f183,plain,(
% 0.13/0.48 (![X]: (~less(X,n9)|less_or_equal(X,n8)))&(![X]: (less(X,n9)|~less_or_equal(X,n8)))),
% 0.13/0.48 inference(miniscoping,[status(thm)],[f182])).
% 0.13/0.48 fof(f185,plain,(
% 0.13/0.48 ![X0]: (less(X0,n9)|~less_or_equal(X0,n8))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f183])).
% 0.13/0.48 fof(f186,plain,(
% 0.13/0.48 ![X,Y]: ((~less(X,Y)|(~less(Y,X)&~Y=X))&(less(X,Y)|(less(Y,X)|Y=X)))),
% 0.13/0.48 inference(NNF_transformation,[status(thm)],[f43])).
% 0.13/0.48 fof(f187,plain,(
% 0.13/0.48 (![X,Y]: (~less(X,Y)|(~less(Y,X)&~Y=X)))&(![X,Y]: (less(X,Y)|(less(Y,X)|Y=X)))),
% 0.13/0.48 inference(miniscoping,[status(thm)],[f186])).
% 0.13/0.48 fof(f188,plain,(
% 0.13/0.48 ![X0,X1]: (~less(X0,X1)|~less(X1,X0))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f187])).
% 0.13/0.48 fof(f189,plain,(
% 0.13/0.48 ![X0,X1]: (~less(X0,X1)|~X1=X0)),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f187])).
% 0.13/0.48 fof(f195,plain,(
% 0.13/0.48 holdsAt(spinning,n2)),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f49])).
% 0.13/0.48 fof(f196,definition,(
% 0.13/0.48 ![Event,Fluent,Time]: (sP3_prd(Time,Fluent,Event)<=>((Event=push&Fluent=forwards)&~happens(pull,Time)))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.13/0.48 fof(f214,definition,(
% 0.13/0.48 ![Event,Time]: (sP5_prd(Time,Event)<=>((Event=push&Time=n0)|(Event=pull&Time=n1)))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.13/0.48 fof(f215,plain,(
% 0.13/0.48 ![Event,Time]: (sP2_prd(Time,Event)<=>(sP5_prd(Time,Event)|(Event=pull&Time=n2)))),
% 0.13/0.48 inference(formula_renaming,[status(thm)],[f120,f214])).
% 0.13/0.48 fof(f216,plain,(
% 0.13/0.48 ![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.13/0.48 inference(NNF_transformation,[status(thm)],[f215])).
% 0.13/0.48 fof(f217,plain,(
% 0.13/0.48 (![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.13/0.48 inference(miniscoping,[status(thm)],[f216])).
% 0.13/0.48 fof(f218,plain,(
% 0.13/0.48 ![X0,X1]: (~sP2_prd(X0,X1)|sP5_prd(X0,X1)|X1=pull)),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f217])).
% 0.13/0.48 fof(f220,plain,(
% 0.13/0.48 ![X0,X1]: (sP2_prd(X0,X1)|~sP5_prd(X0,X1))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f217])).
% 0.13/0.48 fof(f222,plain,(
% 0.13/0.48 ![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.13/0.48 inference(NNF_transformation,[status(thm)],[f196])).
% 0.13/0.48 fof(f223,plain,(
% 0.13/0.48 (![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.13/0.48 inference(miniscoping,[status(thm)],[f222])).
% 0.13/0.48 fof(f225,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|X1=forwards)),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f223])).
% 0.13/0.48 fof(f237,plain,(
% 0.13/0.48 ![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.13/0.48 inference(NNF_transformation,[status(thm)],[f214])).
% 0.13/0.48 fof(f238,plain,(
% 0.13/0.48 (![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.13/0.48 inference(miniscoping,[status(thm)],[f237])).
% 0.13/0.48 fof(f241,plain,(
% 0.13/0.48 ![X0,X1]: (~sP5_prd(X0,X1)|X0=n0|X1=pull)),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f238])).
% 0.13/0.48 fof(f244,plain,(
% 0.13/0.48 ![X0,X1]: (sP5_prd(X0,X1)|~X1=pull|~X0=n1)),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f238])).
% 0.13/0.48 fof(f270,plain,(
% 0.13/0.48 ![X0]: (terminates(pull,spinning,X0)|happens(push,X0))),
% 0.13/0.48 inference(destructive_equality_resolution,[status(thm)],[f118])).
% 0.13/0.48 fof(f272,plain,(
% 0.13/0.48 ![X0]: (less_or_equal(X0,X0))),
% 0.13/0.48 inference(destructive_equality_resolution,[status(thm)],[f147])).
% 0.13/0.48 fof(f273,plain,(
% 0.13/0.48 ![X0]: (~less(X0,X0))),
% 0.13/0.48 inference(destructive_equality_resolution,[status(thm)],[f189])).
% 0.13/0.48 fof(f280,plain,(
% 0.13/0.48 sP5_prd(n1,pull)),
% 0.13/0.48 inference(destructive_equality_resolution,[status(thm)],[f244])).
% 0.13/0.48 fof(f285,plain,(
% 0.13/0.48 less(n1,n2)),
% 0.13/0.48 inference(resolution,[status(thm)],[f272,f157])).
% 0.13/0.48 fof(f325,plain,(
% 0.13/0.48 less_or_equal(n1,n2)),
% 0.13/0.48 inference(resolution,[status(thm)],[f146,f285])).
% 0.13/0.48 fof(f327,plain,(
% 0.13/0.48 sP2_prd(n1,pull)),
% 0.13/0.48 inference(resolution,[status(thm)],[f220,f280])).
% 0.13/0.48 fof(f329,plain,(
% 0.13/0.48 happens(pull,n1)),
% 0.13/0.48 inference(resolution,[status(thm)],[f327,f126])).
% 0.13/0.48 fof(f335,definition,(
% 0.13/0.48 sQ3_spl <=> (happens(push,n1))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f336,plain,(
% 0.13/0.48 happens(push,n1)|~sQ3_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f335])).
% 0.13/0.48 fof(f371,definition,(
% 0.13/0.48 sQ11_spl <=> (n1=n2)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f372,plain,(
% 0.13/0.48 n1=n2|~sQ11_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f371])).
% 0.13/0.48 fof(f375,plain,(
% 0.13/0.48 less(n0,n1)),
% 0.13/0.48 inference(resolution,[status(thm)],[f153,f272])).
% 0.13/0.48 fof(f379,plain,(
% 0.13/0.48 less_or_equal(n0,n1)),
% 0.13/0.48 inference(resolution,[status(thm)],[f375,f146])).
% 0.13/0.48 fof(f380,plain,(
% 0.13/0.48 less(n0,n2)),
% 0.13/0.48 inference(resolution,[status(thm)],[f379,f157])).
% 0.13/0.48 fof(f385,definition,(
% 0.13/0.48 sQ13_spl <=> (n0=n1)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f386,plain,(
% 0.13/0.48 n0=n1|~sQ13_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f385])).
% 0.13/0.48 fof(f391,plain,(
% 0.13/0.48 less_or_equal(n0,n2)),
% 0.13/0.48 inference(resolution,[status(thm)],[f380,f146])).
% 0.13/0.48 fof(f404,plain,(
% 0.13/0.48 less(n0,n3)),
% 0.13/0.48 inference(resolution,[status(thm)],[f161,f391])).
% 0.13/0.48 fof(f405,plain,(
% 0.13/0.48 less(n1,n3)),
% 0.13/0.48 inference(resolution,[status(thm)],[f161,f325])).
% 0.13/0.48 fof(f489,plain,(
% 0.13/0.48 less_or_equal(n0,n3)),
% 0.13/0.48 inference(resolution,[status(thm)],[f404,f146])).
% 0.13/0.48 fof(f493,plain,(
% 0.13/0.48 less_or_equal(n1,n3)),
% 0.13/0.48 inference(resolution,[status(thm)],[f405,f146])).
% 0.13/0.48 fof(f628,plain,(
% 0.13/0.48 less(n2,n2)|~sQ11_spl),
% 0.13/0.48 inference(forward_demodulation,[status(thm)],[f372,f285])).
% 0.13/0.48 fof(f629,plain,(
% 0.13/0.48 $false|~sQ11_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f628,f273])).
% 0.13/0.48 fof(f630,plain,(
% 0.13/0.48 ~sQ11_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f629])).
% 0.13/0.48 fof(f701,plain,(
% 0.13/0.48 ![X0,X1]: (~happens(X0,n1)|~terminates(X0,X1,n1)|~holdsAt(X1,n2))),
% 0.13/0.48 inference(paramodulation,[status(thm)],[f136,f93])).
% 0.13/0.48 fof(f737,plain,(
% 0.13/0.48 less(n1,n1)|~sQ13_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f386,f375])).
% 0.13/0.48 fof(f752,plain,(
% 0.13/0.48 $false|~sQ13_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f737,f273])).
% 0.13/0.48 fof(f753,plain,(
% 0.13/0.48 ~sQ13_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f752])).
% 0.13/0.48 fof(f911,definition,(
% 0.13/0.48 sQ58_spl <=> (happens(pull,n1))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f913,plain,(
% 0.13/0.48 ~happens(pull,n1)|sQ58_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f911])).
% 0.13/0.48 fof(f922,plain,(
% 0.13/0.48 $false|sQ58_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f913,f329])).
% 0.13/0.48 fof(f923,plain,(
% 0.13/0.48 sQ58_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f922])).
% 0.13/0.48 fof(f930,plain,(
% 0.13/0.48 ~happens(pull,n1)|~holdsAt(spinning,n2)|happens(push,n1)),
% 0.13/0.48 inference(resolution,[status(thm)],[f701,f270])).
% 0.13/0.48 fof(f931,definition,(
% 0.13/0.48 sQ62_spl <=> (holdsAt(spinning,n2))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f933,plain,(
% 0.13/0.48 ~holdsAt(spinning,n2)|sQ62_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f931])).
% 0.13/0.48 fof(f934,plain,(
% 0.13/0.48 ~sQ58_spl|~sQ62_spl|sQ3_spl),
% 0.13/0.48 inference(split_clause,[status(thm)],[f930,f911,f931,f335])).
% 0.13/0.48 fof(f935,plain,(
% 0.13/0.48 $false|sQ62_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f933,f195])).
% 0.13/0.48 fof(f936,plain,(
% 0.13/0.48 sQ62_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f935])).
% 0.13/0.48 fof(f969,definition,(
% 0.13/0.48 sQ65_spl <=> (sP2_prd(n1,push))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f970,plain,(
% 0.13/0.48 sP2_prd(n1,push)|~sQ65_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f969])).
% 0.13/0.48 fof(f991,definition,(
% 0.13/0.48 sQ71_spl <=> (pull=push)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f992,plain,(
% 0.13/0.48 pull=push|~sQ71_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f991])).
% 0.13/0.48 fof(f999,plain,(
% 0.13/0.48 $false|~sQ71_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f992,f128])).
% 0.13/0.48 fof(f1000,plain,(
% 0.13/0.48 ~sQ71_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f999])).
% 0.13/0.48 fof(f1001,plain,(
% 0.13/0.48 sP2_prd(n1,push)|n1=n2|~sQ3_spl),
% 0.13/0.48 inference(resolution,[status(thm)],[f125,f336])).
% 0.13/0.48 fof(f1006,plain,(
% 0.13/0.48 sQ65_spl|sQ11_spl|~sQ3_spl),
% 0.13/0.48 inference(split_clause,[status(thm)],[f1001,f969,f371,f335])).
% 0.13/0.48 fof(f1070,definition,(
% 0.13/0.48 sQ77_spl <=> (n1=n4)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1071,plain,(
% 0.13/0.48 n1=n4|~sQ77_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1070])).
% 0.13/0.48 fof(f1074,definition,(
% 0.13/0.48 sQ78_spl <=> (n0=n4)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1075,plain,(
% 0.13/0.48 n0=n4|~sQ78_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1074])).
% 0.13/0.48 fof(f1157,plain,(
% 0.13/0.48 less(n3,n4)),
% 0.13/0.48 inference(resolution,[status(thm)],[f165,f272])).
% 0.13/0.48 fof(f1158,plain,(
% 0.13/0.48 less(n4,n5)),
% 0.13/0.48 inference(resolution,[status(thm)],[f169,f272])).
% 0.13/0.48 fof(f1178,plain,(
% 0.13/0.48 less(n1,n4)),
% 0.13/0.48 inference(resolution,[status(thm)],[f493,f165])).
% 0.13/0.48 fof(f1202,plain,(
% 0.13/0.48 less(n0,n4)),
% 0.13/0.48 inference(resolution,[status(thm)],[f489,f165])).
% 0.13/0.48 fof(f1209,plain,(
% 0.13/0.48 less(n5,n6)),
% 0.13/0.48 inference(resolution,[status(thm)],[f173,f272])).
% 0.13/0.48 fof(f1219,plain,(
% 0.13/0.48 ~less(n4,n1)),
% 0.13/0.48 inference(resolution,[status(thm)],[f1178,f188])).
% 0.13/0.48 fof(f1220,plain,(
% 0.13/0.48 less_or_equal(n1,n4)),
% 0.13/0.48 inference(resolution,[status(thm)],[f1178,f146])).
% 0.13/0.48 fof(f1223,plain,(
% 0.13/0.48 less_or_equal(n0,n4)),
% 0.13/0.48 inference(resolution,[status(thm)],[f1202,f146])).
% 0.13/0.48 fof(f1224,plain,(
% 0.13/0.48 less(n1,n5)),
% 0.13/0.48 inference(resolution,[status(thm)],[f1220,f169])).
% 0.13/0.48 fof(f1230,plain,(
% 0.13/0.48 less(n0,n5)),
% 0.13/0.48 inference(resolution,[status(thm)],[f1223,f169])).
% 0.13/0.48 fof(f1237,plain,(
% 0.13/0.48 less(n4,n4)|~sQ78_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f1075,f1202])).
% 0.13/0.48 fof(f1256,plain,(
% 0.13/0.48 $false|~sQ78_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1237,f273])).
% 0.13/0.48 fof(f1257,plain,(
% 0.13/0.48 ~sQ78_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f1256])).
% 0.13/0.48 fof(f1260,plain,(
% 0.13/0.48 less(n4,n4)|~sQ77_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f1071,f1178])).
% 0.13/0.48 fof(f1278,plain,(
% 0.13/0.48 $false|~sQ77_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1260,f273])).
% 0.13/0.48 fof(f1279,plain,(
% 0.13/0.48 ~sQ77_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f1278])).
% 0.13/0.48 fof(f1286,plain,(
% 0.13/0.48 ~less(n4,n3)),
% 0.13/0.48 inference(resolution,[status(thm)],[f1157,f188])).
% 0.13/0.48 fof(f1287,plain,(
% 0.13/0.48 less_or_equal(n3,n4)),
% 0.13/0.48 inference(resolution,[status(thm)],[f1157,f146])).
% 0.13/0.48 fof(f1291,plain,(
% 0.13/0.48 ~less(n5,n4)),
% 0.13/0.48 inference(resolution,[status(thm)],[f1158,f188])).
% 0.13/0.48 fof(f1298,plain,(
% 0.13/0.48 less(n6,n7)),
% 0.13/0.48 inference(resolution,[status(thm)],[f177,f272])).
% 0.13/0.48 fof(f1299,plain,(
% 0.13/0.48 less(n7,n8)),
% 0.13/0.48 inference(resolution,[status(thm)],[f181,f272])).
% 0.13/0.48 fof(f1324,plain,(
% 0.13/0.48 ~less(n5,n1)),
% 0.13/0.48 inference(resolution,[status(thm)],[f1224,f188])).
% 0.13/0.48 fof(f1355,plain,(
% 0.13/0.48 ~less(n6,n5)),
% 0.13/0.48 inference(resolution,[status(thm)],[f1209,f188])).
% 0.13/0.48 fof(f1366,plain,(
% 0.13/0.48 less(n8,n9)),
% 0.13/0.48 inference(resolution,[status(thm)],[f185,f272])).
% 0.13/0.48 fof(f1436,definition,(
% 0.13/0.48 sQ92_spl <=> (less_or_equal(n9,n8))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1437,plain,(
% 0.13/0.48 less_or_equal(n9,n8)|~sQ92_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1436])).
% 0.13/0.48 fof(f1440,definition,(
% 0.13/0.48 sQ93_spl <=> (less_or_equal(n2,n1))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1441,plain,(
% 0.13/0.48 less_or_equal(n2,n1)|~sQ93_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1440])).
% 0.13/0.48 fof(f1447,definition,(
% 0.13/0.48 sQ95_spl <=> (less_or_equal(n8,n7))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1448,plain,(
% 0.13/0.48 less_or_equal(n8,n7)|~sQ95_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1447])).
% 0.13/0.48 fof(f1454,definition,(
% 0.13/0.48 sQ97_spl <=> (less_or_equal(n7,n6))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1455,plain,(
% 0.13/0.48 less_or_equal(n7,n6)|~sQ97_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1454])).
% 0.13/0.48 fof(f1535,definition,(
% 0.13/0.48 sQ107_spl <=> (n5=n1)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1536,plain,(
% 0.13/0.48 n5=n1|~sQ107_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1535])).
% 0.13/0.48 fof(f1554,plain,(
% 0.13/0.48 ~less(n4,n5)|~sQ107_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f1536,f1219])).
% 0.13/0.48 fof(f1569,plain,(
% 0.13/0.48 $false|~sQ107_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1554,f1158])).
% 0.13/0.48 fof(f1570,plain,(
% 0.13/0.48 ~sQ107_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f1569])).
% 0.13/0.48 fof(f1577,definition,(
% 0.13/0.48 sQ109_spl <=> (n4=n3)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1578,plain,(
% 0.13/0.48 n4=n3|~sQ109_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1577])).
% 0.13/0.48 fof(f1587,plain,(
% 0.13/0.48 less(n4,n4)|~sQ109_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f1578,f1157])).
% 0.13/0.48 fof(f1599,plain,(
% 0.13/0.48 $false|~sQ109_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1587,f273])).
% 0.13/0.48 fof(f1600,plain,(
% 0.13/0.48 ~sQ109_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f1599])).
% 0.13/0.48 fof(f1601,plain,(
% 0.13/0.48 less(n3,n5)),
% 0.13/0.48 inference(resolution,[status(thm)],[f1287,f169])).
% 0.13/0.48 fof(f1609,definition,(
% 0.13/0.48 sQ111_spl <=> (n5=n4)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1610,plain,(
% 0.13/0.48 n5=n4|~sQ111_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1609])).
% 0.13/0.48 fof(f1615,definition,(
% 0.13/0.48 sQ112_spl <=> (sP3_prd(n4,spinning,pull))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1616,plain,(
% 0.13/0.48 sP3_prd(n4,spinning,pull)|~sQ112_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1615])).
% 0.13/0.48 fof(f1620,definition,(
% 0.13/0.48 sQ113_spl <=> (spinning=backwards)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1621,plain,(
% 0.13/0.48 spinning=backwards|~sQ113_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1620])).
% 0.13/0.48 fof(f1624,plain,(
% 0.13/0.48 $false|~sQ113_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1621,f131])).
% 0.13/0.48 fof(f1625,plain,(
% 0.13/0.48 ~sQ113_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f1624])).
% 0.13/0.48 fof(f1643,definition,(
% 0.13/0.48 sQ117_spl <=> (n0=n5)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1644,plain,(
% 0.13/0.48 n0=n5|~sQ117_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1643])).
% 0.13/0.48 fof(f1658,plain,(
% 0.13/0.48 less(n5,n4)|~sQ117_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f1644,f1202])).
% 0.13/0.48 fof(f1666,plain,(
% 0.13/0.48 $false|~sQ117_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1658,f1291])).
% 0.13/0.48 fof(f1667,plain,(
% 0.13/0.48 ~sQ117_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f1666])).
% 0.13/0.48 fof(f1689,plain,(
% 0.13/0.48 less(n5,n5)|~sQ111_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f1610,f1158])).
% 0.13/0.48 fof(f1696,plain,(
% 0.13/0.48 $false|~sQ111_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1689,f273])).
% 0.13/0.48 fof(f1697,plain,(
% 0.13/0.48 ~sQ111_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f1696])).
% 0.13/0.48 fof(f1776,plain,(
% 0.13/0.48 less(n2,n2)|~sQ93_spl),
% 0.13/0.48 inference(resolution,[status(thm)],[f1441,f157])).
% 0.13/0.48 fof(f1778,plain,(
% 0.13/0.48 $false|~sQ93_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1776,f273])).
% 0.13/0.48 fof(f1779,plain,(
% 0.13/0.48 ~sQ93_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f1778])).
% 0.13/0.48 fof(f1807,definition,(
% 0.13/0.48 sQ125_spl <=> (n6=n5)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1808,plain,(
% 0.13/0.48 n6=n5|~sQ125_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1807])).
% 0.13/0.48 fof(f1819,plain,(
% 0.13/0.48 less(n6,n6)|~sQ125_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f1808,f1209])).
% 0.13/0.48 fof(f1822,plain,(
% 0.13/0.48 $false|~sQ125_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1819,f273])).
% 0.13/0.48 fof(f1823,plain,(
% 0.13/0.48 ~sQ125_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f1822])).
% 0.13/0.48 fof(f1831,definition,(
% 0.13/0.48 sQ126_spl <=> (less(n4,n3))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1832,plain,(
% 0.13/0.48 less(n4,n3)|~sQ126_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1831])).
% 0.13/0.48 fof(f1836,definition,(
% 0.13/0.48 sQ127_spl <=> (less(n5,n4))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1837,plain,(
% 0.13/0.48 less(n5,n4)|~sQ127_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1836])).
% 0.13/0.48 fof(f1841,definition,(
% 0.13/0.48 sQ128_spl <=> (less(n6,n5))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1842,plain,(
% 0.13/0.48 less(n6,n5)|~sQ128_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1841])).
% 0.13/0.48 fof(f1845,plain,(
% 0.13/0.48 less(n7,n7)|~sQ97_spl),
% 0.13/0.48 inference(resolution,[status(thm)],[f1455,f177])).
% 0.13/0.48 fof(f1847,plain,(
% 0.13/0.48 $false|~sQ97_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1845,f273])).
% 0.13/0.48 fof(f1848,plain,(
% 0.13/0.48 ~sQ97_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f1847])).
% 0.13/0.48 fof(f1849,plain,(
% 0.13/0.48 less(n8,n8)|~sQ95_spl),
% 0.13/0.48 inference(resolution,[status(thm)],[f1448,f181])).
% 0.13/0.48 fof(f1851,plain,(
% 0.13/0.48 $false|~sQ95_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1849,f273])).
% 0.13/0.48 fof(f1852,plain,(
% 0.13/0.48 ~sQ95_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f1851])).
% 0.13/0.48 fof(f1853,plain,(
% 0.13/0.48 less(n9,n9)|~sQ92_spl),
% 0.13/0.48 inference(resolution,[status(thm)],[f1437,f185])).
% 0.13/0.48 fof(f1855,plain,(
% 0.13/0.48 $false|~sQ92_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1853,f273])).
% 0.13/0.48 fof(f1856,plain,(
% 0.13/0.48 ~sQ92_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f1855])).
% 0.13/0.48 fof(f1865,plain,(
% 0.13/0.48 spinning=forwards|~sQ112_spl),
% 0.13/0.48 inference(resolution,[status(thm)],[f1616,f225])).
% 0.13/0.48 fof(f1867,plain,(
% 0.13/0.48 $false|~sQ112_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1865,f130])).
% 0.13/0.48 fof(f1868,plain,(
% 0.13/0.48 ~sQ112_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f1867])).
% 0.13/0.48 fof(f1936,plain,(
% 0.13/0.48 sP5_prd(n1,push)|push=pull|~sQ65_spl),
% 0.13/0.48 inference(resolution,[status(thm)],[f218,f970])).
% 0.13/0.48 fof(f1943,definition,(
% 0.13/0.48 sQ133_spl <=> (sP5_prd(n1,push))),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f1944,plain,(
% 0.13/0.48 sP5_prd(n1,push)|~sQ133_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f1943])).
% 0.13/0.48 fof(f1946,plain,(
% 0.13/0.48 sQ133_spl|sQ71_spl|~sQ65_spl),
% 0.13/0.48 inference(split_clause,[status(thm)],[f1936,f1943,f991,f969])).
% 0.13/0.48 fof(f2027,definition,(
% 0.13/0.48 sQ138_spl <=> (n7=n6)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f2028,plain,(
% 0.13/0.48 n7=n6|~sQ138_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f2027])).
% 0.13/0.48 fof(f2038,plain,(
% 0.13/0.48 less(n7,n7)|~sQ138_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f2028,f1298])).
% 0.13/0.48 fof(f2041,plain,(
% 0.13/0.48 $false|~sQ138_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f2038,f273])).
% 0.13/0.48 fof(f2042,plain,(
% 0.13/0.48 ~sQ138_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f2041])).
% 0.13/0.48 fof(f2051,definition,(
% 0.13/0.48 sQ140_spl <=> (n8=n7)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f2052,plain,(
% 0.13/0.48 n8=n7|~sQ140_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f2051])).
% 0.13/0.48 fof(f2091,definition,(
% 0.13/0.48 sQ146_spl <=> (n6=n1)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f2092,plain,(
% 0.13/0.48 n6=n1|~sQ146_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f2091])).
% 0.13/0.48 fof(f2100,plain,(
% 0.13/0.48 ~less(n5,n6)|~sQ146_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f2092,f1324])).
% 0.13/0.48 fof(f2146,plain,(
% 0.13/0.48 less(n8,n8)|~sQ140_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f2052,f1299])).
% 0.13/0.48 fof(f2149,plain,(
% 0.13/0.48 $false|~sQ140_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f2146,f273])).
% 0.13/0.48 fof(f2150,plain,(
% 0.13/0.48 ~sQ140_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f2149])).
% 0.13/0.48 fof(f2179,definition,(
% 0.13/0.48 sQ149_spl <=> (n9=n8)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f2180,plain,(
% 0.13/0.48 n9=n8|~sQ149_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f2179])).
% 0.13/0.48 fof(f2207,definition,(
% 0.13/0.48 sQ153_spl <=> (n0=n6)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f2208,plain,(
% 0.13/0.48 n0=n6|~sQ153_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f2207])).
% 0.13/0.48 fof(f2215,plain,(
% 0.13/0.48 less(n6,n5)|~sQ153_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f2208,f1230])).
% 0.13/0.48 fof(f2233,plain,(
% 0.13/0.48 $false|~sQ153_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f2215,f1355])).
% 0.13/0.48 fof(f2234,plain,(
% 0.13/0.48 ~sQ153_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f2233])).
% 0.13/0.48 fof(f2245,plain,(
% 0.13/0.48 less(n9,n9)|~sQ149_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f2180,f1366])).
% 0.13/0.48 fof(f2248,plain,(
% 0.13/0.48 $false|~sQ149_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f2245,f273])).
% 0.13/0.48 fof(f2249,plain,(
% 0.13/0.48 ~sQ149_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f2248])).
% 0.13/0.48 fof(f2256,plain,(
% 0.13/0.48 $false|~sQ126_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1832,f1286])).
% 0.13/0.48 fof(f2257,plain,(
% 0.13/0.48 ~sQ126_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f2256])).
% 0.13/0.48 fof(f2258,plain,(
% 0.13/0.48 $false|~sQ127_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1837,f1291])).
% 0.13/0.48 fof(f2259,plain,(
% 0.13/0.48 ~sQ127_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f2258])).
% 0.13/0.48 fof(f2260,plain,(
% 0.13/0.48 $false|~sQ128_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1842,f1355])).
% 0.13/0.48 fof(f2261,plain,(
% 0.13/0.48 ~sQ128_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f2260])).
% 0.13/0.48 fof(f2269,definition,(
% 0.13/0.48 sQ155_spl <=> (n5=n3)),
% 0.13/0.48 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 0.13/0.48 fof(f2270,plain,(
% 0.13/0.48 n5=n3|~sQ155_spl),
% 0.13/0.48 inference(component_clause,[status(thm)],[f2269])).
% 0.13/0.48 fof(f2344,plain,(
% 0.13/0.48 less(n5,n5)|~sQ155_spl),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f2270,f1601])).
% 0.13/0.48 fof(f2352,plain,(
% 0.13/0.48 $false|~sQ155_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f2344,f273])).
% 0.13/0.48 fof(f2353,plain,(
% 0.13/0.48 ~sQ155_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f2352])).
% 0.13/0.48 fof(f2363,plain,(
% 0.13/0.48 $false|~sQ146_spl),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f2100,f1209])).
% 0.13/0.48 fof(f2364,plain,(
% 0.13/0.48 ~sQ146_spl),
% 0.13/0.48 inference(contradiction_clause,[status(thm)],[f2363])).
% 0.13/0.48 fof(f2368,plain,(
% 0.13/0.48 n1=n0|push=pull|~sQ133_spl),
% 0.13/0.48 inference(resolution,[status(thm)],[f241,f1944])).
% 0.13/0.48 fof(f2369,plain,(
% 0.13/0.48 sQ13_spl|sQ71_spl|~sQ133_spl),
% 0.13/0.48 inference(split_clause,[status(thm)],[f2368,f385,f991,f1943])).
% 0.13/0.48 fof(f2370,plain,(
% 0.13/0.48 $false),
% 0.13/0.48 inference(sat_refutation,[status(thm)],[f630,f753,f923,f934,f936,f1000,f1006,f1257,f1279,f1570,f1600,f1625,f1667,f1697,f1779,f1823,f1848,f1852,f1856,f1868,f1946,f2042,f2150,f2234,f2249,f2257,f2259,f2261,f2353,f2364,f2369])).
% 0.13/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.49 % Elapsed time: 0.124151 seconds
% 0.13/0.49 % CPU time: 0.714606 seconds
% 0.13/0.49 % Total memory used: 117.299 MB
% 0.13/0.49 % Net memory used: 116.253 MB
%------------------------------------------------------------------------------