%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR023+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 : n001.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:36 PM UTC 2026
% Result : Theorem 0.14s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR023+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.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 14:30:00 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.40 fof(f9,axiom,(
% 0.14/0.40 (! [Event,Time,Fluent] :( ( happens(Event,Time)& initiates(Event,Fluent,Time) )=> holdsAt(Fluent,plus(Time,n1)) ) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f13,axiom,(
% 0.14/0.40 (! [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/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f16,axiom,(
% 0.14/0.40 (! [Event,Time] :( happens(Event,Time)<=> ( ( Event = push& Time = n0 )| ( Event = pull& Time = n1 )| ( Event = pull& Time = n2 )| ( Event = push& Time = n2 ) ) ) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f26,axiom,(
% 0.14/0.40 plus(n1,n2) = n3 ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f31,axiom,(
% 0.14/0.40 (! [X,Y] : plus(X,Y) = plus(Y,X) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f48,conjecture,(
% 0.14/0.40 holdsAt(spinning,n3) ),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f49,negated_conjecture,(
% 0.14/0.40 ~(holdsAt(spinning,n3) )),
% 0.14/0.40 inference(negated_conjecture,[status(cth)],[f48])).
% 0.14/0.40 fof(f88,plain,(
% 0.14/0.40 ![Event,Time,Fluent]: ((~happens(Event,Time)|~initiates(Event,Fluent,Time))|holdsAt(Fluent,plus(Time,n1)))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.14/0.40 fof(f89,plain,(
% 0.14/0.40 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~initiates(Event,Fluent,Time)))|holdsAt(Fluent,plus(Time,n1)))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f88])).
% 0.14/0.40 fof(f90,plain,(
% 0.14/0.40 ![X0,X1,X2]: (~happens(X0,X1)|~initiates(X0,X2,X1)|holdsAt(X2,plus(X1,n1)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f89])).
% 0.14/0.40 fof(f101,definition,(
% 0.14/0.40 ![Event,Fluent,Time]: (sP0_prd(Time,Fluent,Event)<=>(((Event=push&Fluent=forwards)&~happens(pull,Time))|((Event=pull&Fluent=backwards)&~happens(push,Time))))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.14/0.40 fof(f102,plain,(
% 0.14/0.40 ![Event,Fluent,Time]: (initiates(Event,Fluent,Time)<=>(sP0_prd(Time,Fluent,Event)|((Event=pull&Fluent=spinning)&happens(push,Time))))),
% 0.14/0.40 inference(formula_renaming,[status(thm)],[f13,f101])).
% 0.14/0.40 fof(f103,plain,(
% 0.14/0.40 ![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/0.40 inference(NNF_transformation,[status(thm)],[f102])).
% 0.14/0.40 fof(f104,plain,(
% 0.14/0.40 (![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/0.40 inference(miniscoping,[status(thm)],[f103])).
% 0.14/0.40 fof(f109,plain,(
% 0.14/0.40 ![X0,X1,X2]: (initiates(X0,X1,X2)|~X0=pull|~X1=spinning|~happens(push,X2))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f104])).
% 0.14/0.40 fof(f120,definition,(
% 0.14/0.40 ![Event,Time]: (sP2_prd(Time,Event)<=>(((Event=push&Time=n0)|(Event=pull&Time=n1))|(Event=pull&Time=n2)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.14/0.40 fof(f121,plain,(
% 0.14/0.40 ![Event,Time]: (happens(Event,Time)<=>(sP2_prd(Time,Event)|(Event=push&Time=n2)))),
% 0.14/0.40 inference(formula_renaming,[status(thm)],[f16,f120])).
% 0.14/0.40 fof(f122,plain,(
% 0.14/0.40 ![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/0.40 inference(NNF_transformation,[status(thm)],[f121])).
% 0.14/0.40 fof(f123,plain,(
% 0.14/0.40 (![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/0.40 inference(miniscoping,[status(thm)],[f122])).
% 0.14/0.40 fof(f126,plain,(
% 0.14/0.40 ![X0,X1]: (happens(X0,X1)|~sP2_prd(X1,X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f123])).
% 0.14/0.40 fof(f127,plain,(
% 0.14/0.40 ![X0,X1]: (happens(X0,X1)|~X0=push|~X1=n2)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f123])).
% 0.14/0.40 fof(f137,plain,(
% 0.14/0.40 plus(n1,n2)=n3),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f26])).
% 0.14/0.40 fof(f142,plain,(
% 0.14/0.40 ![X0,X1]: (plus(X0,X1)=plus(X1,X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f31])).
% 0.14/0.40 fof(f195,plain,(
% 0.14/0.40 ~holdsAt(spinning,n3)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f49])).
% 0.14/0.40 fof(f214,definition,(
% 0.14/0.40 ![Event,Time]: (sP5_prd(Time,Event)<=>((Event=push&Time=n0)|(Event=pull&Time=n1)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.14/0.40 fof(f215,plain,(
% 0.14/0.40 ![Event,Time]: (sP2_prd(Time,Event)<=>(sP5_prd(Time,Event)|(Event=pull&Time=n2)))),
% 0.14/0.40 inference(formula_renaming,[status(thm)],[f120,f214])).
% 0.14/0.40 fof(f216,plain,(
% 0.14/0.40 ![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/0.40 inference(NNF_transformation,[status(thm)],[f215])).
% 0.14/0.40 fof(f217,plain,(
% 0.14/0.40 (![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/0.40 inference(miniscoping,[status(thm)],[f216])).
% 0.14/0.40 fof(f221,plain,(
% 0.14/0.40 ![X0,X1]: (sP2_prd(X0,X1)|~X1=pull|~X0=n2)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f217])).
% 0.14/0.40 fof(f269,plain,(
% 0.14/0.40 ![X0]: (initiates(pull,spinning,X0)|~happens(push,X0))),
% 0.14/0.40 inference(destructive_equality_resolution,[status(thm)],[f109])).
% 0.14/0.40 fof(f271,plain,(
% 0.14/0.40 happens(push,n2)),
% 0.14/0.40 inference(destructive_equality_resolution,[status(thm)],[f127])).
% 0.14/0.40 fof(f276,plain,(
% 0.14/0.40 sP2_prd(n2,pull)),
% 0.14/0.40 inference(destructive_equality_resolution,[status(thm)],[f221])).
% 0.14/0.40 fof(f294,plain,(
% 0.14/0.40 initiates(pull,spinning,n2)),
% 0.14/0.40 inference(resolution,[status(thm)],[f271,f269])).
% 0.14/0.40 fof(f295,plain,(
% 0.14/0.40 ~happens(pull,n2)|holdsAt(spinning,plus(n2,n1))),
% 0.14/0.40 inference(resolution,[status(thm)],[f294,f90])).
% 0.14/0.40 fof(f314,plain,(
% 0.14/0.40 happens(pull,n2)),
% 0.14/0.40 inference(resolution,[status(thm)],[f126,f276])).
% 0.14/0.40 fof(f316,plain,(
% 0.14/0.40 holdsAt(spinning,plus(n2,n1))),
% 0.14/0.40 inference(backward_subsumption_resolution,[status(thm)],[f295,f314])).
% 0.14/0.40 fof(f349,plain,(
% 0.14/0.40 holdsAt(spinning,plus(n1,n2))),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f142,f316])).
% 0.14/0.40 fof(f365,plain,(
% 0.14/0.40 holdsAt(spinning,n3)),
% 0.14/0.40 inference(forward_demodulation,[status(thm)],[f137,f349])).
% 0.14/0.40 fof(f366,plain,(
% 0.14/0.40 $false),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f365,f195])).
% 0.14/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.43 % Elapsed time: 0.061498 seconds
% 0.14/0.43 % CPU time: 0.174161 seconds
% 0.14/0.43 % Total memory used: 106.167 MB
% 0.14/0.43 % Net memory used: 106.027 MB
%------------------------------------------------------------------------------