%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR024+1.009 : 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 : n002.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.16s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR024+1.009 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n002.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 21 14:27:03 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 0.16/0.59 % Refutation found
% 0.16/0.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.59 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.59 fof(f9,axiom,(
% 0.16/0.59 (! [Event,Time,Fluent] :( ( happens(Event,Time)& initiates(Event,Fluent,Time) )=> holdsAt(Fluent,plus(Time,n1)) ) )),
% 0.16/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.59 fof(f13,axiom,(
% 0.16/0.59 (! [Event,Fluent,Time] :( initiates(Event,Fluent,Time)<=> (? [Agent,Trolley] :( ( Event = push(Agent,Trolley)& Fluent = forwards(Trolley)& ~ happens(pull(Agent,Trolley),Time) )| ( Event = pull(Agent,Trolley)& Fluent = backwards(Trolley)& ~ happens(push(Agent,Trolley),Time) )| ( Event = pull(Agent,Trolley)& Fluent = spinning(Trolley)& happens(push(Agent,Trolley),Time) ) ) )) )),
% 0.16/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.59 fof(f23,axiom,(
% 0.16/0.59 plus(n0,n1) = n1 ),
% 0.16/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.59 fof(f48,axiom,(
% 0.16/0.59 (! [Event,Time] :( happens(Event,Time)<=> ( ( Event = pull(agent1,trolley1)& Time = n0 )| ( Event = push(agent1,trolley1)& Time = n0 )| ( Event = pull(agent2,trolley2)& Time = n0 )| ( Event = push(agent2,trolley2)& Time = n0 )| ( Event = pull(agent3,trolley3)& Time = n0 )| ( Event = push(agent3,trolley3)& Time = n0 )| ( Event = pull(agent4,trolley4)& Time = n0 )| ( Event = push(agent4,trolley4)& Time = n0 )| ( Event = pull(agent5,trolley5)& Time = n0 )| ( Event = push(agent5,trolley5)& Time = n0 )| ( Event = pull(agent6,trolley6)& Time = n0 )| ( Event = push(agent6,trolley6)& Time = n0 )| ( Event = pull(agent7,trolley7)& Time = n0 )| ( Event = push(agent7,trolley7)& Time = n0 )| ( Event = pull(agent8,trolley8)& Time = n0 )| ( Event = push(agent8,trolley8)& Time = n0 )| ( Event = pull(agent9,trolley9)& Time = n0 )| ( Event = push(agent9,trolley9)& Time = n0 ) ) ) )),
% 0.16/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.59 fof(f58,conjecture,(
% 0.16/0.59 ( holdsAt(spinning(trolley1),n1)& holdsAt(spinning(trolley2),n1)& holdsAt(spinning(trolley3),n1)& holdsAt(spinning(trolley4),n1)& holdsAt(spinning(trolley5),n1)& holdsAt(spinning(trolley6),n1)& holdsAt(spinning(trolley7),n1)& holdsAt(spinning(trolley8),n1)& holdsAt(spinning(trolley9),n1) ) ),
% 0.16/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.59 fof(f59,negated_conjecture,(
% 0.16/0.59 ~(( holdsAt(spinning(trolley1),n1)& holdsAt(spinning(trolley2),n1)& holdsAt(spinning(trolley3),n1)& holdsAt(spinning(trolley4),n1)& holdsAt(spinning(trolley5),n1)& holdsAt(spinning(trolley6),n1)& holdsAt(spinning(trolley7),n1)& holdsAt(spinning(trolley8),n1)& holdsAt(spinning(trolley9),n1) ) )),
% 0.16/0.59 inference(negated_conjecture,[status(cth)],[f58])).
% 0.16/0.59 fof(f98,plain,(
% 0.16/0.59 ![Event,Time,Fluent]: ((~happens(Event,Time)|~initiates(Event,Fluent,Time))|holdsAt(Fluent,plus(Time,n1)))),
% 0.16/0.59 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.16/0.59 fof(f99,plain,(
% 0.16/0.59 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~initiates(Event,Fluent,Time)))|holdsAt(Fluent,plus(Time,n1)))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f98])).
% 0.16/0.59 fof(f100,plain,(
% 0.16/0.59 ![X0,X1,X2]: (~happens(X0,X1)|~initiates(X0,X2,X1)|holdsAt(X2,plus(X1,n1)))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f99])).
% 0.16/0.59 fof(f111,definition,(
% 0.16/0.59 ![Event,Fluent,Time,Agent,Trolley]: (sP0_prd(Trolley,Agent,Time,Fluent,Event)<=>(((Event=push(Agent,Trolley)&Fluent=forwards(Trolley))&~happens(pull(Agent,Trolley),Time))|((Event=pull(Agent,Trolley)&Fluent=backwards(Trolley))&~happens(push(Agent,Trolley),Time))))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.16/0.59 fof(f112,plain,(
% 0.16/0.59 ![Event,Fluent,Time]: (initiates(Event,Fluent,Time)<=>(?[Agent,Trolley]: (sP0_prd(Trolley,Agent,Time,Fluent,Event)|((Event=pull(Agent,Trolley)&Fluent=spinning(Trolley))&happens(push(Agent,Trolley),Time)))))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f13,f111])).
% 0.16/0.59 fof(f113,plain,(
% 0.16/0.59 ![Event,Fluent,Time]: ((~initiates(Event,Fluent,Time)|(?[Agent,Trolley]: (sP0_prd(Trolley,Agent,Time,Fluent,Event)|((Event=pull(Agent,Trolley)&Fluent=spinning(Trolley))&happens(push(Agent,Trolley),Time)))))&(initiates(Event,Fluent,Time)|(![Agent,Trolley]: (~sP0_prd(Trolley,Agent,Time,Fluent,Event)&((~Event=pull(Agent,Trolley)|~Fluent=spinning(Trolley))|~happens(push(Agent,Trolley),Time))))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f112])).
% 0.16/0.59 fof(f114,plain,(
% 0.16/0.59 (![Event,Fluent,Time]: (~initiates(Event,Fluent,Time)|((?[Agent,Trolley]: sP0_prd(Trolley,Agent,Time,Fluent,Event))|(?[Agent,Trolley]: ((Event=pull(Agent,Trolley)&Fluent=spinning(Trolley))&happens(push(Agent,Trolley),Time))))))&(![Event,Fluent,Time]: (initiates(Event,Fluent,Time)|((![Agent,Trolley]: ~sP0_prd(Trolley,Agent,Time,Fluent,Event))&(![Agent,Trolley]: ((~Event=pull(Agent,Trolley)|~Fluent=spinning(Trolley))|~happens(push(Agent,Trolley),Time))))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f113])).
% 0.16/0.59 fof(f115,plain,(
% 0.16/0.59 (![Event,Fluent,Time]: (~initiates(Event,Fluent,Time)|(sP0_prd(sK9_skl(Time,Fluent,Event),sK8_skl(Time,Fluent,Event),Time,Fluent,Event)|((Event=pull(sK10_skl(Time,Fluent,Event),sK11_skl(Time,Fluent,Event))&Fluent=spinning(sK11_skl(Time,Fluent,Event)))&happens(push(sK10_skl(Time,Fluent,Event),sK11_skl(Time,Fluent,Event)),Time)))))&(![Event,Fluent,Time]: (initiates(Event,Fluent,Time)|((![Agent,Trolley]: ~sP0_prd(Trolley,Agent,Time,Fluent,Event))&(![Agent,Trolley]: ((~Event=pull(Agent,Trolley)|~Fluent=spinning(Trolley))|~happens(push(Agent,Trolley),Time))))))),
% 0.16/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl,sK10_skl,sK11_skl]),skolemize(Agent,sK8_skl(Time,Fluent,Event)),skolemize(Trolley,sK9_skl(Time,Fluent,Event)),skolemize(Agent,sK10_skl(Time,Fluent,Event)),skolemize(Trolley,sK11_skl(Time,Fluent,Event))],[f114])).
% 0.16/0.59 fof(f120,plain,(
% 0.16/0.59 ![X0,X1,X2,X3,X4]: (initiates(X0,X1,X2)|~X0=pull(X3,X4)|~X1=spinning(X4)|~happens(push(X3,X4),X2))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f115])).
% 0.16/0.59 fof(f141,plain,(
% 0.16/0.59 plus(n0,n1)=n1),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f23])).
% 0.16/0.59 fof(f220,definition,(
% 0.16/0.59 ![Event,Time]: (sP4_prd(Time,Event)<=>(((((((((((((((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0))|(Event=pull(agent3,trolley3)&Time=n0))|(Event=push(agent3,trolley3)&Time=n0))|(Event=pull(agent4,trolley4)&Time=n0))|(Event=push(agent4,trolley4)&Time=n0))|(Event=pull(agent5,trolley5)&Time=n0))|(Event=push(agent5,trolley5)&Time=n0))|(Event=pull(agent6,trolley6)&Time=n0))|(Event=push(agent6,trolley6)&Time=n0))|(Event=pull(agent7,trolley7)&Time=n0))|(Event=push(agent7,trolley7)&Time=n0))|(Event=pull(agent8,trolley8)&Time=n0))|(Event=push(agent8,trolley8)&Time=n0))|(Event=pull(agent9,trolley9)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.16/0.59 fof(f221,plain,(
% 0.16/0.59 ![Event,Time]: (happens(Event,Time)<=>(sP4_prd(Time,Event)|(Event=push(agent9,trolley9)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f48,f220])).
% 0.16/0.59 fof(f222,plain,(
% 0.16/0.59 ![Event,Time]: ((~happens(Event,Time)|(sP4_prd(Time,Event)|(Event=push(agent9,trolley9)&Time=n0)))&(happens(Event,Time)|(~sP4_prd(Time,Event)&(~Event=push(agent9,trolley9)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f221])).
% 0.16/0.59 fof(f223,plain,(
% 0.16/0.59 (![Event,Time]: (~happens(Event,Time)|(sP4_prd(Time,Event)|(Event=push(agent9,trolley9)&Time=n0))))&(![Event,Time]: (happens(Event,Time)|(~sP4_prd(Time,Event)&(~Event=push(agent9,trolley9)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f222])).
% 0.16/0.59 fof(f226,plain,(
% 0.16/0.59 ![X0,X1]: (happens(X0,X1)|~sP4_prd(X1,X0))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f223])).
% 0.16/0.59 fof(f227,plain,(
% 0.16/0.59 ![X0,X1]: (happens(X0,X1)|~X0=push(agent9,trolley9)|~X1=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f223])).
% 0.16/0.59 fof(f336,plain,(
% 0.16/0.59 ((((((((~holdsAt(spinning(trolley1),n1)|~holdsAt(spinning(trolley2),n1))|~holdsAt(spinning(trolley3),n1))|~holdsAt(spinning(trolley4),n1))|~holdsAt(spinning(trolley5),n1))|~holdsAt(spinning(trolley6),n1))|~holdsAt(spinning(trolley7),n1))|~holdsAt(spinning(trolley8),n1))|~holdsAt(spinning(trolley9),n1))),
% 0.16/0.59 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 0.16/0.59 fof(f337,plain,(
% 0.16/0.59 ~holdsAt(spinning(trolley1),n1)|~holdsAt(spinning(trolley2),n1)|~holdsAt(spinning(trolley3),n1)|~holdsAt(spinning(trolley4),n1)|~holdsAt(spinning(trolley5),n1)|~holdsAt(spinning(trolley6),n1)|~holdsAt(spinning(trolley7),n1)|~holdsAt(spinning(trolley8),n1)|~holdsAt(spinning(trolley9),n1)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f336])).
% 0.16/0.59 fof(f374,definition,(
% 0.16/0.59 ![Event,Time]: (sP9_prd(Time,Event)<=>((((((((((((((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0))|(Event=pull(agent3,trolley3)&Time=n0))|(Event=push(agent3,trolley3)&Time=n0))|(Event=pull(agent4,trolley4)&Time=n0))|(Event=push(agent4,trolley4)&Time=n0))|(Event=pull(agent5,trolley5)&Time=n0))|(Event=push(agent5,trolley5)&Time=n0))|(Event=pull(agent6,trolley6)&Time=n0))|(Event=push(agent6,trolley6)&Time=n0))|(Event=pull(agent7,trolley7)&Time=n0))|(Event=push(agent7,trolley7)&Time=n0))|(Event=pull(agent8,trolley8)&Time=n0))|(Event=push(agent8,trolley8)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.16/0.59 fof(f375,plain,(
% 0.16/0.59 ![Event,Time]: (sP4_prd(Time,Event)<=>(sP9_prd(Time,Event)|(Event=pull(agent9,trolley9)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f220,f374])).
% 0.16/0.59 fof(f376,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP4_prd(Time,Event)|(sP9_prd(Time,Event)|(Event=pull(agent9,trolley9)&Time=n0)))&(sP4_prd(Time,Event)|(~sP9_prd(Time,Event)&(~Event=pull(agent9,trolley9)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f375])).
% 0.16/0.59 fof(f377,plain,(
% 0.16/0.59 (![Event,Time]: (~sP4_prd(Time,Event)|(sP9_prd(Time,Event)|(Event=pull(agent9,trolley9)&Time=n0))))&(![Event,Time]: (sP4_prd(Time,Event)|(~sP9_prd(Time,Event)&(~Event=pull(agent9,trolley9)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f376])).
% 0.16/0.59 fof(f380,plain,(
% 0.16/0.59 ![X0,X1]: (sP4_prd(X0,X1)|~sP9_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f377])).
% 0.16/0.59 fof(f381,plain,(
% 0.16/0.59 ![X0,X1]: (sP4_prd(X0,X1)|~X1=pull(agent9,trolley9)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f377])).
% 0.16/0.59 fof(f412,definition,(
% 0.16/0.59 ![Event,Time]: (sP12_prd(Time,Event)<=>(((((((((((((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0))|(Event=pull(agent3,trolley3)&Time=n0))|(Event=push(agent3,trolley3)&Time=n0))|(Event=pull(agent4,trolley4)&Time=n0))|(Event=push(agent4,trolley4)&Time=n0))|(Event=pull(agent5,trolley5)&Time=n0))|(Event=push(agent5,trolley5)&Time=n0))|(Event=pull(agent6,trolley6)&Time=n0))|(Event=push(agent6,trolley6)&Time=n0))|(Event=pull(agent7,trolley7)&Time=n0))|(Event=push(agent7,trolley7)&Time=n0))|(Event=pull(agent8,trolley8)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 0.16/0.59 fof(f413,plain,(
% 0.16/0.59 ![Event,Time]: (sP9_prd(Time,Event)<=>(sP12_prd(Time,Event)|(Event=push(agent8,trolley8)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f374,f412])).
% 0.16/0.59 fof(f414,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP9_prd(Time,Event)|(sP12_prd(Time,Event)|(Event=push(agent8,trolley8)&Time=n0)))&(sP9_prd(Time,Event)|(~sP12_prd(Time,Event)&(~Event=push(agent8,trolley8)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f413])).
% 0.16/0.59 fof(f415,plain,(
% 0.16/0.59 (![Event,Time]: (~sP9_prd(Time,Event)|(sP12_prd(Time,Event)|(Event=push(agent8,trolley8)&Time=n0))))&(![Event,Time]: (sP9_prd(Time,Event)|(~sP12_prd(Time,Event)&(~Event=push(agent8,trolley8)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f414])).
% 0.16/0.59 fof(f418,plain,(
% 0.16/0.59 ![X0,X1]: (sP9_prd(X0,X1)|~sP12_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f415])).
% 0.16/0.59 fof(f419,plain,(
% 0.16/0.59 ![X0,X1]: (sP9_prd(X0,X1)|~X1=push(agent8,trolley8)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f415])).
% 0.16/0.59 fof(f438,definition,(
% 0.16/0.59 ![Event,Time]: (sP15_prd(Time,Event)<=>((((((((((((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0))|(Event=pull(agent3,trolley3)&Time=n0))|(Event=push(agent3,trolley3)&Time=n0))|(Event=pull(agent4,trolley4)&Time=n0))|(Event=push(agent4,trolley4)&Time=n0))|(Event=pull(agent5,trolley5)&Time=n0))|(Event=push(agent5,trolley5)&Time=n0))|(Event=pull(agent6,trolley6)&Time=n0))|(Event=push(agent6,trolley6)&Time=n0))|(Event=pull(agent7,trolley7)&Time=n0))|(Event=push(agent7,trolley7)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP15_prd])],[])).
% 0.16/0.59 fof(f439,plain,(
% 0.16/0.59 ![Event,Time]: (sP12_prd(Time,Event)<=>(sP15_prd(Time,Event)|(Event=pull(agent8,trolley8)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f412,f438])).
% 0.16/0.59 fof(f440,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP12_prd(Time,Event)|(sP15_prd(Time,Event)|(Event=pull(agent8,trolley8)&Time=n0)))&(sP12_prd(Time,Event)|(~sP15_prd(Time,Event)&(~Event=pull(agent8,trolley8)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f439])).
% 0.16/0.59 fof(f441,plain,(
% 0.16/0.59 (![Event,Time]: (~sP12_prd(Time,Event)|(sP15_prd(Time,Event)|(Event=pull(agent8,trolley8)&Time=n0))))&(![Event,Time]: (sP12_prd(Time,Event)|(~sP15_prd(Time,Event)&(~Event=pull(agent8,trolley8)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f440])).
% 0.16/0.59 fof(f444,plain,(
% 0.16/0.59 ![X0,X1]: (sP12_prd(X0,X1)|~sP15_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f441])).
% 0.16/0.59 fof(f445,plain,(
% 0.16/0.59 ![X0,X1]: (sP12_prd(X0,X1)|~X1=pull(agent8,trolley8)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f441])).
% 0.16/0.59 fof(f464,definition,(
% 0.16/0.59 ![Event,Time]: (sP18_prd(Time,Event)<=>(((((((((((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0))|(Event=pull(agent3,trolley3)&Time=n0))|(Event=push(agent3,trolley3)&Time=n0))|(Event=pull(agent4,trolley4)&Time=n0))|(Event=push(agent4,trolley4)&Time=n0))|(Event=pull(agent5,trolley5)&Time=n0))|(Event=push(agent5,trolley5)&Time=n0))|(Event=pull(agent6,trolley6)&Time=n0))|(Event=push(agent6,trolley6)&Time=n0))|(Event=pull(agent7,trolley7)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP18_prd])],[])).
% 0.16/0.59 fof(f465,plain,(
% 0.16/0.59 ![Event,Time]: (sP15_prd(Time,Event)<=>(sP18_prd(Time,Event)|(Event=push(agent7,trolley7)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f438,f464])).
% 0.16/0.59 fof(f466,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP15_prd(Time,Event)|(sP18_prd(Time,Event)|(Event=push(agent7,trolley7)&Time=n0)))&(sP15_prd(Time,Event)|(~sP18_prd(Time,Event)&(~Event=push(agent7,trolley7)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f465])).
% 0.16/0.59 fof(f467,plain,(
% 0.16/0.59 (![Event,Time]: (~sP15_prd(Time,Event)|(sP18_prd(Time,Event)|(Event=push(agent7,trolley7)&Time=n0))))&(![Event,Time]: (sP15_prd(Time,Event)|(~sP18_prd(Time,Event)&(~Event=push(agent7,trolley7)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f466])).
% 0.16/0.59 fof(f470,plain,(
% 0.16/0.59 ![X0,X1]: (sP15_prd(X0,X1)|~sP18_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f467])).
% 0.16/0.59 fof(f471,plain,(
% 0.16/0.59 ![X0,X1]: (sP15_prd(X0,X1)|~X1=push(agent7,trolley7)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f467])).
% 0.16/0.59 fof(f484,definition,(
% 0.16/0.59 ![Event,Time]: (sP19_prd(Time,Event)<=>((((((((((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0))|(Event=pull(agent3,trolley3)&Time=n0))|(Event=push(agent3,trolley3)&Time=n0))|(Event=pull(agent4,trolley4)&Time=n0))|(Event=push(agent4,trolley4)&Time=n0))|(Event=pull(agent5,trolley5)&Time=n0))|(Event=push(agent5,trolley5)&Time=n0))|(Event=pull(agent6,trolley6)&Time=n0))|(Event=push(agent6,trolley6)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP19_prd])],[])).
% 0.16/0.59 fof(f485,plain,(
% 0.16/0.59 ![Event,Time]: (sP18_prd(Time,Event)<=>(sP19_prd(Time,Event)|(Event=pull(agent7,trolley7)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f464,f484])).
% 0.16/0.59 fof(f486,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP18_prd(Time,Event)|(sP19_prd(Time,Event)|(Event=pull(agent7,trolley7)&Time=n0)))&(sP18_prd(Time,Event)|(~sP19_prd(Time,Event)&(~Event=pull(agent7,trolley7)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f485])).
% 0.16/0.59 fof(f487,plain,(
% 0.16/0.59 (![Event,Time]: (~sP18_prd(Time,Event)|(sP19_prd(Time,Event)|(Event=pull(agent7,trolley7)&Time=n0))))&(![Event,Time]: (sP18_prd(Time,Event)|(~sP19_prd(Time,Event)&(~Event=pull(agent7,trolley7)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f486])).
% 0.16/0.59 fof(f490,plain,(
% 0.16/0.59 ![X0,X1]: (sP18_prd(X0,X1)|~sP19_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f487])).
% 0.16/0.59 fof(f491,plain,(
% 0.16/0.59 ![X0,X1]: (sP18_prd(X0,X1)|~X1=pull(agent7,trolley7)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f487])).
% 0.16/0.59 fof(f492,definition,(
% 0.16/0.59 ![Event,Time]: (sP20_prd(Time,Event)<=>(((((((((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0))|(Event=pull(agent3,trolley3)&Time=n0))|(Event=push(agent3,trolley3)&Time=n0))|(Event=pull(agent4,trolley4)&Time=n0))|(Event=push(agent4,trolley4)&Time=n0))|(Event=pull(agent5,trolley5)&Time=n0))|(Event=push(agent5,trolley5)&Time=n0))|(Event=pull(agent6,trolley6)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP20_prd])],[])).
% 0.16/0.59 fof(f493,plain,(
% 0.16/0.59 ![Event,Time]: (sP19_prd(Time,Event)<=>(sP20_prd(Time,Event)|(Event=push(agent6,trolley6)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f484,f492])).
% 0.16/0.59 fof(f494,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP19_prd(Time,Event)|(sP20_prd(Time,Event)|(Event=push(agent6,trolley6)&Time=n0)))&(sP19_prd(Time,Event)|(~sP20_prd(Time,Event)&(~Event=push(agent6,trolley6)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f493])).
% 0.16/0.59 fof(f495,plain,(
% 0.16/0.59 (![Event,Time]: (~sP19_prd(Time,Event)|(sP20_prd(Time,Event)|(Event=push(agent6,trolley6)&Time=n0))))&(![Event,Time]: (sP19_prd(Time,Event)|(~sP20_prd(Time,Event)&(~Event=push(agent6,trolley6)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f494])).
% 0.16/0.59 fof(f498,plain,(
% 0.16/0.59 ![X0,X1]: (sP19_prd(X0,X1)|~sP20_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f495])).
% 0.16/0.59 fof(f499,plain,(
% 0.16/0.59 ![X0,X1]: (sP19_prd(X0,X1)|~X1=push(agent6,trolley6)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f495])).
% 0.16/0.59 fof(f500,definition,(
% 0.16/0.59 ![Event,Time]: (sP21_prd(Time,Event)<=>((((((((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0))|(Event=pull(agent3,trolley3)&Time=n0))|(Event=push(agent3,trolley3)&Time=n0))|(Event=pull(agent4,trolley4)&Time=n0))|(Event=push(agent4,trolley4)&Time=n0))|(Event=pull(agent5,trolley5)&Time=n0))|(Event=push(agent5,trolley5)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP21_prd])],[])).
% 0.16/0.59 fof(f501,plain,(
% 0.16/0.59 ![Event,Time]: (sP20_prd(Time,Event)<=>(sP21_prd(Time,Event)|(Event=pull(agent6,trolley6)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f492,f500])).
% 0.16/0.59 fof(f502,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP20_prd(Time,Event)|(sP21_prd(Time,Event)|(Event=pull(agent6,trolley6)&Time=n0)))&(sP20_prd(Time,Event)|(~sP21_prd(Time,Event)&(~Event=pull(agent6,trolley6)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f501])).
% 0.16/0.59 fof(f503,plain,(
% 0.16/0.59 (![Event,Time]: (~sP20_prd(Time,Event)|(sP21_prd(Time,Event)|(Event=pull(agent6,trolley6)&Time=n0))))&(![Event,Time]: (sP20_prd(Time,Event)|(~sP21_prd(Time,Event)&(~Event=pull(agent6,trolley6)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f502])).
% 0.16/0.59 fof(f506,plain,(
% 0.16/0.59 ![X0,X1]: (sP20_prd(X0,X1)|~sP21_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f503])).
% 0.16/0.59 fof(f507,plain,(
% 0.16/0.59 ![X0,X1]: (sP20_prd(X0,X1)|~X1=pull(agent6,trolley6)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f503])).
% 0.16/0.59 fof(f508,definition,(
% 0.16/0.59 ![Event,Time]: (sP22_prd(Time,Event)<=>(((((((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0))|(Event=pull(agent3,trolley3)&Time=n0))|(Event=push(agent3,trolley3)&Time=n0))|(Event=pull(agent4,trolley4)&Time=n0))|(Event=push(agent4,trolley4)&Time=n0))|(Event=pull(agent5,trolley5)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP22_prd])],[])).
% 0.16/0.59 fof(f509,plain,(
% 0.16/0.59 ![Event,Time]: (sP21_prd(Time,Event)<=>(sP22_prd(Time,Event)|(Event=push(agent5,trolley5)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f500,f508])).
% 0.16/0.59 fof(f510,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP21_prd(Time,Event)|(sP22_prd(Time,Event)|(Event=push(agent5,trolley5)&Time=n0)))&(sP21_prd(Time,Event)|(~sP22_prd(Time,Event)&(~Event=push(agent5,trolley5)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f509])).
% 0.16/0.59 fof(f511,plain,(
% 0.16/0.59 (![Event,Time]: (~sP21_prd(Time,Event)|(sP22_prd(Time,Event)|(Event=push(agent5,trolley5)&Time=n0))))&(![Event,Time]: (sP21_prd(Time,Event)|(~sP22_prd(Time,Event)&(~Event=push(agent5,trolley5)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f510])).
% 0.16/0.59 fof(f514,plain,(
% 0.16/0.59 ![X0,X1]: (sP21_prd(X0,X1)|~sP22_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f511])).
% 0.16/0.59 fof(f515,plain,(
% 0.16/0.59 ![X0,X1]: (sP21_prd(X0,X1)|~X1=push(agent5,trolley5)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f511])).
% 0.16/0.59 fof(f516,definition,(
% 0.16/0.59 ![Event,Time]: (sP23_prd(Time,Event)<=>((((((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0))|(Event=pull(agent3,trolley3)&Time=n0))|(Event=push(agent3,trolley3)&Time=n0))|(Event=pull(agent4,trolley4)&Time=n0))|(Event=push(agent4,trolley4)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP23_prd])],[])).
% 0.16/0.59 fof(f517,plain,(
% 0.16/0.59 ![Event,Time]: (sP22_prd(Time,Event)<=>(sP23_prd(Time,Event)|(Event=pull(agent5,trolley5)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f508,f516])).
% 0.16/0.59 fof(f518,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP22_prd(Time,Event)|(sP23_prd(Time,Event)|(Event=pull(agent5,trolley5)&Time=n0)))&(sP22_prd(Time,Event)|(~sP23_prd(Time,Event)&(~Event=pull(agent5,trolley5)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f517])).
% 0.16/0.59 fof(f519,plain,(
% 0.16/0.59 (![Event,Time]: (~sP22_prd(Time,Event)|(sP23_prd(Time,Event)|(Event=pull(agent5,trolley5)&Time=n0))))&(![Event,Time]: (sP22_prd(Time,Event)|(~sP23_prd(Time,Event)&(~Event=pull(agent5,trolley5)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f518])).
% 0.16/0.59 fof(f522,plain,(
% 0.16/0.59 ![X0,X1]: (sP22_prd(X0,X1)|~sP23_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f519])).
% 0.16/0.59 fof(f523,plain,(
% 0.16/0.59 ![X0,X1]: (sP22_prd(X0,X1)|~X1=pull(agent5,trolley5)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f519])).
% 0.16/0.59 fof(f524,definition,(
% 0.16/0.59 ![Event,Time]: (sP24_prd(Time,Event)<=>(((((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0))|(Event=pull(agent3,trolley3)&Time=n0))|(Event=push(agent3,trolley3)&Time=n0))|(Event=pull(agent4,trolley4)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP24_prd])],[])).
% 0.16/0.59 fof(f525,plain,(
% 0.16/0.59 ![Event,Time]: (sP23_prd(Time,Event)<=>(sP24_prd(Time,Event)|(Event=push(agent4,trolley4)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f516,f524])).
% 0.16/0.59 fof(f526,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP23_prd(Time,Event)|(sP24_prd(Time,Event)|(Event=push(agent4,trolley4)&Time=n0)))&(sP23_prd(Time,Event)|(~sP24_prd(Time,Event)&(~Event=push(agent4,trolley4)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f525])).
% 0.16/0.59 fof(f527,plain,(
% 0.16/0.59 (![Event,Time]: (~sP23_prd(Time,Event)|(sP24_prd(Time,Event)|(Event=push(agent4,trolley4)&Time=n0))))&(![Event,Time]: (sP23_prd(Time,Event)|(~sP24_prd(Time,Event)&(~Event=push(agent4,trolley4)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f526])).
% 0.16/0.59 fof(f530,plain,(
% 0.16/0.59 ![X0,X1]: (sP23_prd(X0,X1)|~sP24_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f527])).
% 0.16/0.59 fof(f531,plain,(
% 0.16/0.59 ![X0,X1]: (sP23_prd(X0,X1)|~X1=push(agent4,trolley4)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f527])).
% 0.16/0.59 fof(f532,definition,(
% 0.16/0.59 ![Event,Time]: (sP25_prd(Time,Event)<=>((((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0))|(Event=pull(agent3,trolley3)&Time=n0))|(Event=push(agent3,trolley3)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP25_prd])],[])).
% 0.16/0.59 fof(f533,plain,(
% 0.16/0.59 ![Event,Time]: (sP24_prd(Time,Event)<=>(sP25_prd(Time,Event)|(Event=pull(agent4,trolley4)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f524,f532])).
% 0.16/0.59 fof(f534,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP24_prd(Time,Event)|(sP25_prd(Time,Event)|(Event=pull(agent4,trolley4)&Time=n0)))&(sP24_prd(Time,Event)|(~sP25_prd(Time,Event)&(~Event=pull(agent4,trolley4)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f533])).
% 0.16/0.59 fof(f535,plain,(
% 0.16/0.59 (![Event,Time]: (~sP24_prd(Time,Event)|(sP25_prd(Time,Event)|(Event=pull(agent4,trolley4)&Time=n0))))&(![Event,Time]: (sP24_prd(Time,Event)|(~sP25_prd(Time,Event)&(~Event=pull(agent4,trolley4)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f534])).
% 0.16/0.59 fof(f538,plain,(
% 0.16/0.59 ![X0,X1]: (sP24_prd(X0,X1)|~sP25_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f535])).
% 0.16/0.59 fof(f539,plain,(
% 0.16/0.59 ![X0,X1]: (sP24_prd(X0,X1)|~X1=pull(agent4,trolley4)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f535])).
% 0.16/0.59 fof(f540,definition,(
% 0.16/0.59 ![Event,Time]: (sP26_prd(Time,Event)<=>(((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0))|(Event=pull(agent3,trolley3)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP26_prd])],[])).
% 0.16/0.59 fof(f541,plain,(
% 0.16/0.59 ![Event,Time]: (sP25_prd(Time,Event)<=>(sP26_prd(Time,Event)|(Event=push(agent3,trolley3)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f532,f540])).
% 0.16/0.59 fof(f542,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP25_prd(Time,Event)|(sP26_prd(Time,Event)|(Event=push(agent3,trolley3)&Time=n0)))&(sP25_prd(Time,Event)|(~sP26_prd(Time,Event)&(~Event=push(agent3,trolley3)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f541])).
% 0.16/0.59 fof(f543,plain,(
% 0.16/0.59 (![Event,Time]: (~sP25_prd(Time,Event)|(sP26_prd(Time,Event)|(Event=push(agent3,trolley3)&Time=n0))))&(![Event,Time]: (sP25_prd(Time,Event)|(~sP26_prd(Time,Event)&(~Event=push(agent3,trolley3)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f542])).
% 0.16/0.59 fof(f546,plain,(
% 0.16/0.59 ![X0,X1]: (sP25_prd(X0,X1)|~sP26_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f543])).
% 0.16/0.59 fof(f547,plain,(
% 0.16/0.59 ![X0,X1]: (sP25_prd(X0,X1)|~X1=push(agent3,trolley3)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f543])).
% 0.16/0.59 fof(f548,definition,(
% 0.16/0.59 ![Event,Time]: (sP27_prd(Time,Event)<=>((((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0))|(Event=push(agent2,trolley2)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP27_prd])],[])).
% 0.16/0.59 fof(f549,plain,(
% 0.16/0.59 ![Event,Time]: (sP26_prd(Time,Event)<=>(sP27_prd(Time,Event)|(Event=pull(agent3,trolley3)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f540,f548])).
% 0.16/0.59 fof(f550,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP26_prd(Time,Event)|(sP27_prd(Time,Event)|(Event=pull(agent3,trolley3)&Time=n0)))&(sP26_prd(Time,Event)|(~sP27_prd(Time,Event)&(~Event=pull(agent3,trolley3)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f549])).
% 0.16/0.59 fof(f551,plain,(
% 0.16/0.59 (![Event,Time]: (~sP26_prd(Time,Event)|(sP27_prd(Time,Event)|(Event=pull(agent3,trolley3)&Time=n0))))&(![Event,Time]: (sP26_prd(Time,Event)|(~sP27_prd(Time,Event)&(~Event=pull(agent3,trolley3)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f550])).
% 0.16/0.59 fof(f554,plain,(
% 0.16/0.59 ![X0,X1]: (sP26_prd(X0,X1)|~sP27_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f551])).
% 0.16/0.59 fof(f555,plain,(
% 0.16/0.59 ![X0,X1]: (sP26_prd(X0,X1)|~X1=pull(agent3,trolley3)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f551])).
% 0.16/0.59 fof(f556,definition,(
% 0.16/0.59 ![Event,Time]: (sP28_prd(Time,Event)<=>(((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP28_prd])],[])).
% 0.16/0.59 fof(f557,plain,(
% 0.16/0.59 ![Event,Time]: (sP27_prd(Time,Event)<=>(sP28_prd(Time,Event)|(Event=push(agent2,trolley2)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f548,f556])).
% 0.16/0.59 fof(f558,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP27_prd(Time,Event)|(sP28_prd(Time,Event)|(Event=push(agent2,trolley2)&Time=n0)))&(sP27_prd(Time,Event)|(~sP28_prd(Time,Event)&(~Event=push(agent2,trolley2)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f557])).
% 0.16/0.59 fof(f559,plain,(
% 0.16/0.59 (![Event,Time]: (~sP27_prd(Time,Event)|(sP28_prd(Time,Event)|(Event=push(agent2,trolley2)&Time=n0))))&(![Event,Time]: (sP27_prd(Time,Event)|(~sP28_prd(Time,Event)&(~Event=push(agent2,trolley2)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f558])).
% 0.16/0.59 fof(f562,plain,(
% 0.16/0.59 ![X0,X1]: (sP27_prd(X0,X1)|~sP28_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f559])).
% 0.16/0.59 fof(f563,plain,(
% 0.16/0.59 ![X0,X1]: (sP27_prd(X0,X1)|~X1=push(agent2,trolley2)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f559])).
% 0.16/0.59 fof(f564,definition,(
% 0.16/0.59 ![Event,Time]: (sP29_prd(Time,Event)<=>((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0)))),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sP29_prd])],[])).
% 0.16/0.59 fof(f565,plain,(
% 0.16/0.59 ![Event,Time]: (sP28_prd(Time,Event)<=>(sP29_prd(Time,Event)|(Event=pull(agent2,trolley2)&Time=n0)))),
% 0.16/0.59 inference(formula_renaming,[status(thm)],[f556,f564])).
% 0.16/0.59 fof(f566,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP28_prd(Time,Event)|(sP29_prd(Time,Event)|(Event=pull(agent2,trolley2)&Time=n0)))&(sP28_prd(Time,Event)|(~sP29_prd(Time,Event)&(~Event=pull(agent2,trolley2)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f565])).
% 0.16/0.59 fof(f567,plain,(
% 0.16/0.59 (![Event,Time]: (~sP28_prd(Time,Event)|(sP29_prd(Time,Event)|(Event=pull(agent2,trolley2)&Time=n0))))&(![Event,Time]: (sP28_prd(Time,Event)|(~sP29_prd(Time,Event)&(~Event=pull(agent2,trolley2)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f566])).
% 0.16/0.59 fof(f570,plain,(
% 0.16/0.59 ![X0,X1]: (sP28_prd(X0,X1)|~sP29_prd(X0,X1))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f567])).
% 0.16/0.59 fof(f571,plain,(
% 0.16/0.59 ![X0,X1]: (sP28_prd(X0,X1)|~X1=pull(agent2,trolley2)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f567])).
% 0.16/0.59 fof(f572,plain,(
% 0.16/0.59 ![Event,Time]: ((~sP29_prd(Time,Event)|((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0)))&(sP29_prd(Time,Event)|((~Event=pull(agent1,trolley1)|~Time=n0)&(~Event=push(agent1,trolley1)|~Time=n0))))),
% 0.16/0.59 inference(NNF_transformation,[status(thm)],[f564])).
% 0.16/0.59 fof(f573,plain,(
% 0.16/0.59 (![Event,Time]: (~sP29_prd(Time,Event)|((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))))&(![Event,Time]: (sP29_prd(Time,Event)|((~Event=pull(agent1,trolley1)|~Time=n0)&(~Event=push(agent1,trolley1)|~Time=n0))))),
% 0.16/0.59 inference(miniscoping,[status(thm)],[f572])).
% 0.16/0.59 fof(f578,plain,(
% 0.16/0.59 ![X0,X1]: (sP29_prd(X0,X1)|~X1=pull(agent1,trolley1)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f573])).
% 0.16/0.59 fof(f579,plain,(
% 0.16/0.59 ![X0,X1]: (sP29_prd(X0,X1)|~X1=push(agent1,trolley1)|~X0=n0)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f573])).
% 0.16/0.59 fof(f580,plain,(
% 0.16/0.59 ![X0,X1,X2]: (initiates(pull(X0,X1),spinning(X1),X2)|~happens(push(X0,X1),X2))),
% 0.16/0.59 inference(destructive_equality_resolution,[status(thm)],[f120])).
% 0.16/0.59 fof(f587,plain,(
% 0.16/0.59 happens(push(agent9,trolley9),n0)),
% 0.16/0.59 inference(destructive_equality_resolution,[status(thm)],[f227])).
% 0.16/0.59 fof(f596,plain,(
% 0.16/0.59 sP4_prd(n0,pull(agent9,trolley9))),
% 0.16/0.59 inference(destructive_equality_resolution,[status(thm)],[f381])).
% 0.16/0.59 fof(f601,plain,(
% 0.16/0.59 sP9_prd(n0,push(agent8,trolley8))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f419])).
% 0.16/0.60 fof(f604,plain,(
% 0.16/0.60 sP12_prd(n0,pull(agent8,trolley8))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f445])).
% 0.16/0.60 fof(f607,plain,(
% 0.16/0.60 sP15_prd(n0,push(agent7,trolley7))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f471])).
% 0.16/0.60 fof(f610,plain,(
% 0.16/0.60 sP18_prd(n0,pull(agent7,trolley7))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f491])).
% 0.16/0.60 fof(f611,plain,(
% 0.16/0.60 sP19_prd(n0,push(agent6,trolley6))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f499])).
% 0.16/0.60 fof(f612,plain,(
% 0.16/0.60 sP20_prd(n0,pull(agent6,trolley6))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f507])).
% 0.16/0.60 fof(f613,plain,(
% 0.16/0.60 sP21_prd(n0,push(agent5,trolley5))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f515])).
% 0.16/0.60 fof(f614,plain,(
% 0.16/0.60 sP22_prd(n0,pull(agent5,trolley5))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f523])).
% 0.16/0.60 fof(f615,plain,(
% 0.16/0.60 sP23_prd(n0,push(agent4,trolley4))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f531])).
% 0.16/0.60 fof(f616,plain,(
% 0.16/0.60 sP24_prd(n0,pull(agent4,trolley4))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f539])).
% 0.16/0.60 fof(f617,plain,(
% 0.16/0.60 sP25_prd(n0,push(agent3,trolley3))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f547])).
% 0.16/0.60 fof(f618,plain,(
% 0.16/0.60 sP26_prd(n0,pull(agent3,trolley3))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f555])).
% 0.16/0.60 fof(f619,plain,(
% 0.16/0.60 sP27_prd(n0,push(agent2,trolley2))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f563])).
% 0.16/0.60 fof(f620,plain,(
% 0.16/0.60 sP28_prd(n0,pull(agent2,trolley2))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f571])).
% 0.16/0.60 fof(f623,plain,(
% 0.16/0.60 sP29_prd(n0,pull(agent1,trolley1))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f578])).
% 0.16/0.60 fof(f624,plain,(
% 0.16/0.60 sP29_prd(n0,push(agent1,trolley1))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f579])).
% 0.16/0.60 fof(f655,plain,(
% 0.16/0.60 ![X0,X1]: (~happens(X0,n0)|~initiates(X0,X1,n0)|holdsAt(X1,n1))),
% 0.16/0.60 inference(paramodulation,[status(thm)],[f141,f100])).
% 0.16/0.60 fof(f779,plain,(
% 0.16/0.60 happens(pull(agent9,trolley9),n0)),
% 0.16/0.60 inference(resolution,[status(thm)],[f596,f226])).
% 0.16/0.60 fof(f781,plain,(
% 0.16/0.60 sP4_prd(n0,push(agent8,trolley8))),
% 0.16/0.60 inference(resolution,[status(thm)],[f601,f380])).
% 0.16/0.60 fof(f783,plain,(
% 0.16/0.60 sP9_prd(n0,pull(agent8,trolley8))),
% 0.16/0.60 inference(resolution,[status(thm)],[f604,f418])).
% 0.16/0.60 fof(f785,plain,(
% 0.16/0.60 sP12_prd(n0,push(agent7,trolley7))),
% 0.16/0.60 inference(resolution,[status(thm)],[f607,f444])).
% 0.16/0.60 fof(f787,plain,(
% 0.16/0.60 sP15_prd(n0,pull(agent7,trolley7))),
% 0.16/0.60 inference(resolution,[status(thm)],[f610,f470])).
% 0.16/0.60 fof(f789,plain,(
% 0.16/0.60 sP18_prd(n0,push(agent6,trolley6))),
% 0.16/0.60 inference(resolution,[status(thm)],[f611,f490])).
% 0.16/0.60 fof(f794,plain,(
% 0.16/0.60 sP19_prd(n0,pull(agent6,trolley6))),
% 0.16/0.60 inference(resolution,[status(thm)],[f612,f498])).
% 0.16/0.60 fof(f796,plain,(
% 0.16/0.60 sP20_prd(n0,push(agent5,trolley5))),
% 0.16/0.60 inference(resolution,[status(thm)],[f613,f506])).
% 0.16/0.60 fof(f798,plain,(
% 0.16/0.60 sP21_prd(n0,pull(agent5,trolley5))),
% 0.16/0.60 inference(resolution,[status(thm)],[f614,f514])).
% 0.16/0.60 fof(f800,plain,(
% 0.16/0.60 sP22_prd(n0,push(agent4,trolley4))),
% 0.16/0.60 inference(resolution,[status(thm)],[f615,f522])).
% 0.16/0.60 fof(f802,plain,(
% 0.16/0.60 sP23_prd(n0,pull(agent4,trolley4))),
% 0.16/0.60 inference(resolution,[status(thm)],[f616,f530])).
% 0.16/0.60 fof(f804,plain,(
% 0.16/0.60 sP24_prd(n0,push(agent3,trolley3))),
% 0.16/0.60 inference(resolution,[status(thm)],[f617,f538])).
% 0.16/0.60 fof(f808,plain,(
% 0.16/0.60 sP25_prd(n0,pull(agent3,trolley3))),
% 0.16/0.60 inference(resolution,[status(thm)],[f618,f546])).
% 0.16/0.60 fof(f810,plain,(
% 0.16/0.60 sP26_prd(n0,push(agent2,trolley2))),
% 0.16/0.60 inference(resolution,[status(thm)],[f619,f554])).
% 0.16/0.60 fof(f812,plain,(
% 0.16/0.60 sP27_prd(n0,pull(agent2,trolley2))),
% 0.16/0.60 inference(resolution,[status(thm)],[f620,f562])).
% 0.16/0.60 fof(f814,plain,(
% 0.16/0.60 sP28_prd(n0,pull(agent1,trolley1))),
% 0.16/0.60 inference(resolution,[status(thm)],[f623,f570])).
% 0.16/0.60 fof(f816,plain,(
% 0.16/0.60 sP28_prd(n0,push(agent1,trolley1))),
% 0.16/0.60 inference(resolution,[status(thm)],[f624,f570])).
% 0.16/0.60 fof(f937,plain,(
% 0.16/0.60 happens(push(agent8,trolley8),n0)),
% 0.16/0.60 inference(resolution,[status(thm)],[f781,f226])).
% 0.16/0.60 fof(f939,plain,(
% 0.16/0.60 sP4_prd(n0,pull(agent8,trolley8))),
% 0.16/0.60 inference(resolution,[status(thm)],[f783,f380])).
% 0.16/0.60 fof(f943,plain,(
% 0.16/0.60 sP9_prd(n0,push(agent7,trolley7))),
% 0.16/0.60 inference(resolution,[status(thm)],[f785,f418])).
% 0.16/0.60 fof(f945,plain,(
% 0.16/0.60 sP12_prd(n0,pull(agent7,trolley7))),
% 0.16/0.60 inference(resolution,[status(thm)],[f787,f444])).
% 0.16/0.60 fof(f947,plain,(
% 0.16/0.60 sP15_prd(n0,push(agent6,trolley6))),
% 0.16/0.60 inference(resolution,[status(thm)],[f789,f470])).
% 0.16/0.60 fof(f949,plain,(
% 0.16/0.60 sP18_prd(n0,pull(agent6,trolley6))),
% 0.16/0.60 inference(resolution,[status(thm)],[f794,f490])).
% 0.16/0.60 fof(f957,plain,(
% 0.16/0.60 sP19_prd(n0,push(agent5,trolley5))),
% 0.16/0.60 inference(resolution,[status(thm)],[f796,f498])).
% 0.16/0.60 fof(f959,plain,(
% 0.16/0.60 sP20_prd(n0,pull(agent5,trolley5))),
% 0.16/0.60 inference(resolution,[status(thm)],[f798,f506])).
% 0.16/0.60 fof(f961,plain,(
% 0.16/0.60 sP21_prd(n0,push(agent4,trolley4))),
% 0.16/0.60 inference(resolution,[status(thm)],[f800,f514])).
% 0.16/0.60 fof(f963,plain,(
% 0.16/0.60 sP22_prd(n0,pull(agent4,trolley4))),
% 0.16/0.60 inference(resolution,[status(thm)],[f802,f522])).
% 0.16/0.60 fof(f965,plain,(
% 0.16/0.60 sP23_prd(n0,push(agent3,trolley3))),
% 0.16/0.60 inference(resolution,[status(thm)],[f804,f530])).
% 0.16/0.61 fof(f967,plain,(
% 0.16/0.61 sP24_prd(n0,pull(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f808,f538])).
% 0.16/0.61 fof(f973,plain,(
% 0.16/0.61 sP25_prd(n0,push(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f810,f546])).
% 0.16/0.61 fof(f975,plain,(
% 0.16/0.61 sP26_prd(n0,pull(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f812,f554])).
% 0.16/0.61 fof(f977,plain,(
% 0.16/0.61 sP27_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f814,f562])).
% 0.16/0.61 fof(f979,plain,(
% 0.16/0.61 sP27_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f816,f562])).
% 0.16/0.61 fof(f1129,plain,(
% 0.16/0.61 happens(pull(agent8,trolley8),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f939,f226])).
% 0.16/0.61 fof(f1131,plain,(
% 0.16/0.61 sP4_prd(n0,push(agent7,trolley7))),
% 0.16/0.61 inference(resolution,[status(thm)],[f943,f380])).
% 0.16/0.61 fof(f1133,plain,(
% 0.16/0.61 sP9_prd(n0,pull(agent7,trolley7))),
% 0.16/0.61 inference(resolution,[status(thm)],[f945,f418])).
% 0.16/0.61 fof(f1135,plain,(
% 0.16/0.61 sP12_prd(n0,push(agent6,trolley6))),
% 0.16/0.61 inference(resolution,[status(thm)],[f947,f444])).
% 0.16/0.61 fof(f1137,plain,(
% 0.16/0.61 sP15_prd(n0,pull(agent6,trolley6))),
% 0.16/0.61 inference(resolution,[status(thm)],[f949,f470])).
% 0.16/0.61 fof(f1139,plain,(
% 0.16/0.61 sP18_prd(n0,push(agent5,trolley5))),
% 0.16/0.61 inference(resolution,[status(thm)],[f957,f490])).
% 0.16/0.61 fof(f1141,plain,(
% 0.16/0.61 sP19_prd(n0,pull(agent5,trolley5))),
% 0.16/0.61 inference(resolution,[status(thm)],[f959,f498])).
% 0.16/0.61 fof(f1147,plain,(
% 0.16/0.61 sP20_prd(n0,push(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f961,f506])).
% 0.16/0.61 fof(f1149,plain,(
% 0.16/0.61 sP21_prd(n0,pull(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f963,f514])).
% 0.16/0.61 fof(f1153,plain,(
% 0.16/0.61 sP22_prd(n0,push(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f965,f522])).
% 0.16/0.61 fof(f1155,plain,(
% 0.16/0.61 sP23_prd(n0,pull(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f967,f530])).
% 0.16/0.61 fof(f1162,plain,(
% 0.16/0.61 sP24_prd(n0,push(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f973,f538])).
% 0.16/0.61 fof(f1164,plain,(
% 0.16/0.61 sP25_prd(n0,pull(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f975,f546])).
% 0.16/0.61 fof(f1166,plain,(
% 0.16/0.61 sP26_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f977,f554])).
% 0.16/0.61 fof(f1168,plain,(
% 0.16/0.61 sP26_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f979,f554])).
% 0.16/0.61 fof(f1247,plain,(
% 0.16/0.61 happens(push(agent7,trolley7),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1131,f226])).
% 0.16/0.61 fof(f1249,plain,(
% 0.16/0.61 sP4_prd(n0,pull(agent7,trolley7))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1133,f380])).
% 0.16/0.61 fof(f1251,plain,(
% 0.16/0.61 sP9_prd(n0,push(agent6,trolley6))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1135,f418])).
% 0.16/0.61 fof(f1253,plain,(
% 0.16/0.61 sP12_prd(n0,pull(agent6,trolley6))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1137,f444])).
% 0.16/0.61 fof(f1255,plain,(
% 0.16/0.61 sP15_prd(n0,push(agent5,trolley5))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1139,f470])).
% 0.16/0.61 fof(f1257,plain,(
% 0.16/0.61 sP18_prd(n0,pull(agent5,trolley5))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1141,f490])).
% 0.16/0.61 fof(f1259,plain,(
% 0.16/0.61 sP19_prd(n0,push(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1147,f498])).
% 0.16/0.61 fof(f1268,plain,(
% 0.16/0.61 sP20_prd(n0,pull(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1149,f506])).
% 0.16/0.61 fof(f1270,plain,(
% 0.16/0.61 sP21_prd(n0,push(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1153,f514])).
% 0.16/0.61 fof(f1275,plain,(
% 0.16/0.61 sP22_prd(n0,pull(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1155,f522])).
% 0.16/0.61 fof(f1278,plain,(
% 0.16/0.61 sP23_prd(n0,push(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1162,f530])).
% 0.16/0.61 fof(f1280,plain,(
% 0.16/0.61 sP24_prd(n0,pull(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1164,f538])).
% 0.16/0.61 fof(f1287,plain,(
% 0.16/0.61 sP25_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1166,f546])).
% 0.16/0.61 fof(f1289,plain,(
% 0.16/0.61 sP25_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1168,f546])).
% 0.16/0.61 fof(f1366,plain,(
% 0.16/0.61 happens(pull(agent7,trolley7),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1249,f226])).
% 0.16/0.61 fof(f1373,plain,(
% 0.16/0.61 sP4_prd(n0,push(agent6,trolley6))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1251,f380])).
% 0.16/0.61 fof(f1375,plain,(
% 0.16/0.61 sP9_prd(n0,pull(agent6,trolley6))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1253,f418])).
% 0.16/0.61 fof(f1377,plain,(
% 0.16/0.61 sP12_prd(n0,push(agent5,trolley5))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1255,f444])).
% 0.16/0.61 fof(f1379,plain,(
% 0.16/0.61 sP15_prd(n0,pull(agent5,trolley5))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1257,f470])).
% 0.16/0.61 fof(f1381,plain,(
% 0.16/0.61 sP18_prd(n0,push(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1259,f490])).
% 0.16/0.61 fof(f1383,plain,(
% 0.16/0.61 sP19_prd(n0,pull(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1268,f498])).
% 0.16/0.61 fof(f1391,plain,(
% 0.16/0.61 sP20_prd(n0,push(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1270,f506])).
% 0.16/0.61 fof(f1393,plain,(
% 0.16/0.61 sP21_prd(n0,pull(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1275,f514])).
% 0.16/0.61 fof(f1397,plain,(
% 0.16/0.61 sP22_prd(n0,push(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1278,f522])).
% 0.16/0.61 fof(f1399,plain,(
% 0.16/0.61 sP23_prd(n0,pull(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1280,f530])).
% 0.16/0.61 fof(f1415,plain,(
% 0.16/0.61 sP24_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1287,f538])).
% 0.16/0.61 fof(f1417,plain,(
% 0.16/0.61 sP24_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1289,f538])).
% 0.16/0.61 fof(f1483,plain,(
% 0.16/0.61 happens(push(agent6,trolley6),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1373,f226])).
% 0.16/0.61 fof(f1488,plain,(
% 0.16/0.61 sP4_prd(n0,pull(agent6,trolley6))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1375,f380])).
% 0.16/0.61 fof(f1490,plain,(
% 0.16/0.61 sP9_prd(n0,push(agent5,trolley5))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1377,f418])).
% 0.16/0.61 fof(f1492,plain,(
% 0.16/0.61 sP12_prd(n0,pull(agent5,trolley5))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1379,f444])).
% 0.16/0.61 fof(f1494,plain,(
% 0.16/0.61 sP15_prd(n0,push(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1381,f470])).
% 0.16/0.61 fof(f1496,plain,(
% 0.16/0.61 sP18_prd(n0,pull(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1383,f490])).
% 0.16/0.61 fof(f1498,plain,(
% 0.16/0.61 sP19_prd(n0,push(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1391,f498])).
% 0.16/0.61 fof(f1502,plain,(
% 0.16/0.61 sP20_prd(n0,pull(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1393,f506])).
% 0.16/0.61 fof(f1504,plain,(
% 0.16/0.61 sP21_prd(n0,push(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1397,f514])).
% 0.16/0.61 fof(f1510,plain,(
% 0.16/0.61 sP22_prd(n0,pull(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1399,f522])).
% 0.16/0.61 fof(f1520,plain,(
% 0.16/0.61 sP23_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1415,f530])).
% 0.16/0.61 fof(f1523,plain,(
% 0.16/0.61 ![X0,X1]: (~happens(pull(X0,X1),n0)|holdsAt(spinning(X1),n1)|~happens(push(X0,X1),n0))),
% 0.16/0.61 inference(resolution,[status(thm)],[f655,f580])).
% 0.16/0.61 fof(f1524,plain,(
% 0.16/0.61 sP23_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1417,f530])).
% 0.16/0.61 fof(f1587,plain,(
% 0.16/0.61 happens(pull(agent6,trolley6),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1488,f226])).
% 0.16/0.61 fof(f1591,plain,(
% 0.16/0.61 sP4_prd(n0,push(agent5,trolley5))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1490,f380])).
% 0.16/0.61 fof(f1593,plain,(
% 0.16/0.61 sP9_prd(n0,pull(agent5,trolley5))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1492,f418])).
% 0.16/0.61 fof(f1595,plain,(
% 0.16/0.61 sP12_prd(n0,push(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1494,f444])).
% 0.16/0.61 fof(f1597,plain,(
% 0.16/0.61 sP15_prd(n0,pull(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1496,f470])).
% 0.16/0.61 fof(f1599,plain,(
% 0.16/0.61 sP18_prd(n0,push(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1498,f490])).
% 0.16/0.61 fof(f1601,plain,(
% 0.16/0.61 sP19_prd(n0,pull(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1502,f498])).
% 0.16/0.61 fof(f1603,plain,(
% 0.16/0.61 sP20_prd(n0,push(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1504,f506])).
% 0.16/0.61 fof(f1605,plain,(
% 0.16/0.61 sP21_prd(n0,pull(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1510,f514])).
% 0.16/0.61 fof(f1607,plain,(
% 0.16/0.61 sP22_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1520,f522])).
% 0.16/0.61 fof(f1609,plain,(
% 0.16/0.61 sP22_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1524,f522])).
% 0.16/0.61 fof(f1649,plain,(
% 0.16/0.61 happens(push(agent5,trolley5),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1591,f226])).
% 0.16/0.61 fof(f1658,plain,(
% 0.16/0.61 sP4_prd(n0,pull(agent5,trolley5))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1593,f380])).
% 0.16/0.61 fof(f1660,plain,(
% 0.16/0.61 sP9_prd(n0,push(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1595,f418])).
% 0.16/0.61 fof(f1663,plain,(
% 0.16/0.61 sP12_prd(n0,pull(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1597,f444])).
% 0.16/0.61 fof(f1665,plain,(
% 0.16/0.61 sP15_prd(n0,push(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1599,f470])).
% 0.16/0.61 fof(f1667,plain,(
% 0.16/0.61 sP18_prd(n0,pull(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1601,f490])).
% 0.16/0.61 fof(f1669,plain,(
% 0.16/0.61 sP19_prd(n0,push(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1603,f498])).
% 0.16/0.61 fof(f1674,plain,(
% 0.16/0.61 sP20_prd(n0,pull(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1605,f506])).
% 0.16/0.61 fof(f1676,plain,(
% 0.16/0.61 sP21_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1607,f514])).
% 0.16/0.61 fof(f1678,plain,(
% 0.16/0.61 sP21_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1609,f514])).
% 0.16/0.61 fof(f1730,plain,(
% 0.16/0.61 happens(pull(agent5,trolley5),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1658,f226])).
% 0.16/0.61 fof(f1732,plain,(
% 0.16/0.61 sP4_prd(n0,push(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1660,f380])).
% 0.16/0.61 fof(f1734,plain,(
% 0.16/0.61 sP9_prd(n0,pull(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1663,f418])).
% 0.16/0.61 fof(f1759,plain,(
% 0.16/0.61 sP12_prd(n0,push(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1665,f444])).
% 0.16/0.61 fof(f1761,plain,(
% 0.16/0.61 sP15_prd(n0,pull(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1667,f470])).
% 0.16/0.61 fof(f1763,plain,(
% 0.16/0.61 sP18_prd(n0,push(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1669,f490])).
% 0.16/0.61 fof(f1765,plain,(
% 0.16/0.61 sP19_prd(n0,pull(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1674,f498])).
% 0.16/0.61 fof(f1767,plain,(
% 0.16/0.61 sP20_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1676,f506])).
% 0.16/0.61 fof(f1769,plain,(
% 0.16/0.61 sP20_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1678,f506])).
% 0.16/0.61 fof(f1845,plain,(
% 0.16/0.61 happens(push(agent4,trolley4),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1732,f226])).
% 0.16/0.61 fof(f1851,plain,(
% 0.16/0.61 sP4_prd(n0,pull(agent4,trolley4))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1734,f380])).
% 0.16/0.61 fof(f1853,plain,(
% 0.16/0.61 sP9_prd(n0,push(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1759,f418])).
% 0.16/0.61 fof(f1855,plain,(
% 0.16/0.61 sP12_prd(n0,pull(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1761,f444])).
% 0.16/0.61 fof(f1857,plain,(
% 0.16/0.61 sP15_prd(n0,push(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1763,f470])).
% 0.16/0.61 fof(f1859,plain,(
% 0.16/0.61 sP18_prd(n0,pull(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1765,f490])).
% 0.16/0.61 fof(f1861,plain,(
% 0.16/0.61 sP19_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1767,f498])).
% 0.16/0.61 fof(f1875,plain,(
% 0.16/0.61 sP19_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1769,f498])).
% 0.16/0.61 fof(f1912,plain,(
% 0.16/0.61 happens(pull(agent4,trolley4),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1851,f226])).
% 0.16/0.61 fof(f1914,plain,(
% 0.16/0.61 sP4_prd(n0,push(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1853,f380])).
% 0.16/0.61 fof(f1916,plain,(
% 0.16/0.61 sP9_prd(n0,pull(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1855,f418])).
% 0.16/0.61 fof(f1918,plain,(
% 0.16/0.61 sP12_prd(n0,push(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1857,f444])).
% 0.16/0.61 fof(f1920,plain,(
% 0.16/0.61 sP15_prd(n0,pull(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1859,f470])).
% 0.16/0.61 fof(f1922,plain,(
% 0.16/0.61 sP18_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1861,f490])).
% 0.16/0.61 fof(f1940,plain,(
% 0.16/0.61 sP18_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1875,f490])).
% 0.16/0.61 fof(f1971,plain,(
% 0.16/0.61 happens(push(agent3,trolley3),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1914,f226])).
% 0.16/0.61 fof(f1973,plain,(
% 0.16/0.61 sP4_prd(n0,pull(agent3,trolley3))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1916,f380])).
% 0.16/0.61 fof(f1975,plain,(
% 0.16/0.61 sP9_prd(n0,push(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1918,f418])).
% 0.16/0.61 fof(f1977,plain,(
% 0.16/0.61 sP12_prd(n0,pull(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1920,f444])).
% 0.16/0.61 fof(f1979,plain,(
% 0.16/0.61 sP15_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1922,f470])).
% 0.16/0.61 fof(f1981,plain,(
% 0.16/0.61 sP15_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1940,f470])).
% 0.16/0.61 fof(f2027,plain,(
% 0.16/0.61 happens(pull(agent3,trolley3),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1973,f226])).
% 0.16/0.61 fof(f2031,plain,(
% 0.16/0.61 sP4_prd(n0,push(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1975,f380])).
% 0.16/0.61 fof(f2033,plain,(
% 0.16/0.61 sP9_prd(n0,pull(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1977,f418])).
% 0.16/0.61 fof(f2035,plain,(
% 0.16/0.61 sP12_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1979,f444])).
% 0.16/0.61 fof(f2037,plain,(
% 0.16/0.61 sP12_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f1981,f444])).
% 0.16/0.61 fof(f2074,plain,(
% 0.16/0.61 happens(push(agent2,trolley2),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f2031,f226])).
% 0.16/0.61 fof(f2076,plain,(
% 0.16/0.61 sP4_prd(n0,pull(agent2,trolley2))),
% 0.16/0.61 inference(resolution,[status(thm)],[f2033,f380])).
% 0.16/0.61 fof(f2078,plain,(
% 0.16/0.61 sP9_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f2035,f418])).
% 0.16/0.61 fof(f2090,plain,(
% 0.16/0.61 sP9_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f2037,f418])).
% 0.16/0.61 fof(f2138,plain,(
% 0.16/0.61 happens(pull(agent2,trolley2),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f2076,f226])).
% 0.16/0.61 fof(f2140,plain,(
% 0.16/0.61 sP4_prd(n0,pull(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f2078,f380])).
% 0.16/0.61 fof(f2148,plain,(
% 0.16/0.61 sP4_prd(n0,push(agent1,trolley1))),
% 0.16/0.61 inference(resolution,[status(thm)],[f2090,f380])).
% 0.16/0.61 fof(f2179,plain,(
% 0.16/0.61 happens(pull(agent1,trolley1),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f2140,f226])).
% 0.16/0.61 fof(f2181,plain,(
% 0.16/0.61 happens(push(agent1,trolley1),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f2148,f226])).
% 0.16/0.61 fof(f2352,plain,(
% 0.16/0.61 holdsAt(spinning(trolley1),n1)|~happens(push(agent1,trolley1),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1523,f2179])).
% 0.16/0.61 fof(f2353,plain,(
% 0.16/0.61 holdsAt(spinning(trolley2),n1)|~happens(push(agent2,trolley2),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1523,f2138])).
% 0.16/0.61 fof(f2354,plain,(
% 0.16/0.61 holdsAt(spinning(trolley3),n1)|~happens(push(agent3,trolley3),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1523,f2027])).
% 0.16/0.61 fof(f2355,plain,(
% 0.16/0.61 holdsAt(spinning(trolley4),n1)|~happens(push(agent4,trolley4),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1523,f1912])).
% 0.16/0.61 fof(f2356,plain,(
% 0.16/0.61 holdsAt(spinning(trolley5),n1)|~happens(push(agent5,trolley5),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1523,f1730])).
% 0.16/0.61 fof(f2357,plain,(
% 0.16/0.61 holdsAt(spinning(trolley6),n1)|~happens(push(agent6,trolley6),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1523,f1587])).
% 0.16/0.61 fof(f2358,plain,(
% 0.16/0.61 holdsAt(spinning(trolley7),n1)|~happens(push(agent7,trolley7),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1523,f1366])).
% 0.16/0.61 fof(f2359,plain,(
% 0.16/0.61 holdsAt(spinning(trolley8),n1)|~happens(push(agent8,trolley8),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1523,f1129])).
% 0.16/0.61 fof(f2360,plain,(
% 0.16/0.61 holdsAt(spinning(trolley9),n1)|~happens(push(agent9,trolley9),n0)),
% 0.16/0.61 inference(resolution,[status(thm)],[f1523,f779])).
% 0.16/0.61 fof(f2361,plain,(
% 0.16/0.61 ~holdsAt(spinning(trolley2),n1)|~holdsAt(spinning(trolley3),n1)|~holdsAt(spinning(trolley4),n1)|~holdsAt(spinning(trolley5),n1)|~holdsAt(spinning(trolley6),n1)|~holdsAt(spinning(trolley7),n1)|~holdsAt(spinning(trolley8),n1)|~holdsAt(spinning(trolley9),n1)),
% 0.16/0.61 inference(backward_subsumption_resolution,[status(thm)],[f337,f2362])).
% 0.16/0.61 fof(f2362,plain,(
% 0.16/0.61 holdsAt(spinning(trolley1),n1)),
% 0.16/0.61 inference(forward_subsumption_resolution,[status(thm)],[f2352,f2181])).
% 0.16/0.61 fof(f2363,plain,(
% 0.16/0.61 holdsAt(spinning(trolley2),n1)),
% 0.16/0.61 inference(forward_subsumption_resolution,[status(thm)],[f2353,f2074])).
% 0.16/0.61 fof(f2364,plain,(
% 0.16/0.61 holdsAt(spinning(trolley3),n1)),
% 0.16/0.61 inference(forward_subsumption_resolution,[status(thm)],[f2354,f1971])).
% 0.16/0.61 fof(f2365,plain,(
% 0.16/0.61 holdsAt(spinning(trolley4),n1)),
% 0.16/0.61 inference(forward_subsumption_resolution,[status(thm)],[f2355,f1845])).
% 0.16/0.61 fof(f2366,plain,(
% 0.16/0.61 holdsAt(spinning(trolley5),n1)),
% 0.16/0.61 inference(forward_subsumption_resolution,[status(thm)],[f2356,f1649])).
% 0.16/0.61 fof(f2367,plain,(
% 0.16/0.61 holdsAt(spinning(trolley6),n1)),
% 0.16/0.61 inference(forward_subsumption_resolution,[status(thm)],[f2357,f1483])).
% 0.16/0.61 fof(f2368,plain,(
% 0.16/0.61 holdsAt(spinning(trolley7),n1)),
% 0.16/0.61 inference(forward_subsumption_resolution,[status(thm)],[f2358,f1247])).
% 0.16/0.61 fof(f2369,plain,(
% 0.16/0.61 holdsAt(spinning(trolley8),n1)),
% 0.16/0.61 inference(forward_subsumption_resolution,[status(thm)],[f2359,f937])).
% 0.16/0.61 fof(f2370,plain,(
% 0.16/0.62 holdsAt(spinning(trolley9),n1)),
% 0.16/0.62 inference(forward_subsumption_resolution,[status(thm)],[f2360,f587])).
% 0.16/0.62 fof(f2371,plain,(
% 0.16/0.62 ~holdsAt(spinning(trolley3),n1)|~holdsAt(spinning(trolley4),n1)|~holdsAt(spinning(trolley5),n1)|~holdsAt(spinning(trolley6),n1)|~holdsAt(spinning(trolley7),n1)|~holdsAt(spinning(trolley8),n1)|~holdsAt(spinning(trolley9),n1)),
% 0.16/0.62 inference(forward_subsumption_resolution,[status(thm)],[f2361,f2363])).
% 0.16/0.62 fof(f2381,plain,(
% 0.16/0.62 ~holdsAt(spinning(trolley3),n1)|~holdsAt(spinning(trolley5),n1)|~holdsAt(spinning(trolley6),n1)|~holdsAt(spinning(trolley7),n1)|~holdsAt(spinning(trolley8),n1)|~holdsAt(spinning(trolley9),n1)),
% 0.16/0.62 inference(resolution,[status(thm)],[f2365,f2371])).
% 0.16/0.62 fof(f2384,plain,(
% 0.16/0.62 ~holdsAt(spinning(trolley5),n1)|~holdsAt(spinning(trolley6),n1)|~holdsAt(spinning(trolley7),n1)|~holdsAt(spinning(trolley8),n1)|~holdsAt(spinning(trolley9),n1)),
% 0.16/0.62 inference(forward_subsumption_resolution,[status(thm)],[f2381,f2364])).
% 0.16/0.62 fof(f2407,plain,(
% 0.16/0.62 ~holdsAt(spinning(trolley5),n1)|~holdsAt(spinning(trolley6),n1)|~holdsAt(spinning(trolley7),n1)|~holdsAt(spinning(trolley9),n1)),
% 0.16/0.62 inference(resolution,[status(thm)],[f2369,f2384])).
% 0.16/0.62 fof(f2410,plain,(
% 0.16/0.62 ~holdsAt(spinning(trolley6),n1)|~holdsAt(spinning(trolley7),n1)|~holdsAt(spinning(trolley9),n1)),
% 0.16/0.62 inference(forward_subsumption_resolution,[status(thm)],[f2407,f2366])).
% 0.16/0.62 fof(f2412,plain,(
% 0.16/0.62 ~holdsAt(spinning(trolley6),n1)|~holdsAt(spinning(trolley7),n1)),
% 0.16/0.62 inference(resolution,[status(thm)],[f2370,f2410])).
% 0.16/0.62 fof(f2416,plain,(
% 0.16/0.62 ~holdsAt(spinning(trolley7),n1)),
% 0.16/0.62 inference(forward_subsumption_resolution,[status(thm)],[f2412,f2367])).
% 0.16/0.62 fof(f2417,plain,(
% 0.16/0.62 $false),
% 0.16/0.62 inference(backward_subsumption_resolution,[status(thm)],[f2368,f2416])).
% 0.16/0.62 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.64 % Elapsed time: 0.226530 seconds
% 0.16/0.64 % CPU time: 1.204497 seconds
% 0.16/0.64 % Total memory used: 129.445 MB
% 0.16/0.64 % Net memory used: 128.703 MB
%------------------------------------------------------------------------------