%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR024+1.010 : 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 : n004.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.09s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR024+1.010 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n004.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 14:24:20 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.57 % Refutation found
% 0.09/0.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.57 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.57 fof(f9,axiom,(
% 0.09/0.57 (! [Event,Time,Fluent] :( ( happens(Event,Time)& initiates(Event,Fluent,Time) )=> holdsAt(Fluent,plus(Time,n1)) ) )),
% 0.09/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f13,axiom,(
% 0.09/0.57 (! [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.09/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f23,axiom,(
% 0.09/0.57 plus(n0,n1) = n1 ),
% 0.09/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f45,axiom,(
% 0.09/0.57 (! [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 )| ( Event = pull(agent10,trolley10)& Time = n0 )| ( Event = push(agent10,trolley10)& Time = n0 ) ) ) )),
% 0.09/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f49,conjecture,(
% 0.09/0.57 ( 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)& holdsAt(spinning(trolley10),n1) ) ),
% 0.09/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.57 fof(f50,negated_conjecture,(
% 0.09/0.57 ~(( 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)& holdsAt(spinning(trolley10),n1) ) )),
% 0.09/0.57 inference(negated_conjecture,[status(cth)],[f49])).
% 0.09/0.57 fof(f89,plain,(
% 0.09/0.57 ![Event,Time,Fluent]: ((~happens(Event,Time)|~initiates(Event,Fluent,Time))|holdsAt(Fluent,plus(Time,n1)))),
% 0.09/0.57 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.09/0.57 fof(f90,plain,(
% 0.09/0.57 ![Time,Fluent]: ((![Event]: (~happens(Event,Time)|~initiates(Event,Fluent,Time)))|holdsAt(Fluent,plus(Time,n1)))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f89])).
% 0.09/0.57 fof(f91,plain,(
% 0.09/0.57 ![X0,X1,X2]: (~happens(X0,X1)|~initiates(X0,X2,X1)|holdsAt(X2,plus(X1,n1)))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f90])).
% 0.09/0.57 fof(f102,definition,(
% 0.09/0.57 ![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.09/0.57 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.09/0.57 fof(f103,plain,(
% 0.09/0.57 ![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.09/0.57 inference(formula_renaming,[status(thm)],[f13,f102])).
% 0.09/0.57 fof(f104,plain,(
% 0.09/0.57 ![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.09/0.57 inference(NNF_transformation,[status(thm)],[f103])).
% 0.09/0.57 fof(f105,plain,(
% 0.09/0.57 (![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.09/0.57 inference(miniscoping,[status(thm)],[f104])).
% 0.09/0.57 fof(f106,plain,(
% 0.09/0.57 (![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.09/0.57 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))],[f105])).
% 0.09/0.57 fof(f111,plain,(
% 0.09/0.57 ![X0,X1,X2,X3,X4]: (initiates(X0,X1,X2)|~X0=pull(X3,X4)|~X1=spinning(X4)|~happens(push(X3,X4),X2))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f106])).
% 0.09/0.57 fof(f132,plain,(
% 0.09/0.57 plus(n0,n1)=n1),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f23])).
% 0.09/0.57 fof(f190,definition,(
% 0.09/0.57 ![Event,Time]: (sP2_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))|(Event=push(agent9,trolley9)&Time=n0))|(Event=pull(agent10,trolley10)&Time=n0)))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.09/0.57 fof(f191,plain,(
% 0.09/0.57 ![Event,Time]: (happens(Event,Time)<=>(sP2_prd(Time,Event)|(Event=push(agent10,trolley10)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f45,f190])).
% 0.09/0.57 fof(f192,plain,(
% 0.09/0.57 ![Event,Time]: ((~happens(Event,Time)|(sP2_prd(Time,Event)|(Event=push(agent10,trolley10)&Time=n0)))&(happens(Event,Time)|(~sP2_prd(Time,Event)&(~Event=push(agent10,trolley10)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f191])).
% 0.09/0.57 fof(f193,plain,(
% 0.09/0.57 (![Event,Time]: (~happens(Event,Time)|(sP2_prd(Time,Event)|(Event=push(agent10,trolley10)&Time=n0))))&(![Event,Time]: (happens(Event,Time)|(~sP2_prd(Time,Event)&(~Event=push(agent10,trolley10)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f192])).
% 0.09/0.57 fof(f196,plain,(
% 0.09/0.57 ![X0,X1]: (happens(X0,X1)|~sP2_prd(X1,X0))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f193])).
% 0.09/0.57 fof(f197,plain,(
% 0.09/0.57 ![X0,X1]: (happens(X0,X1)|~X0=push(agent10,trolley10)|~X1=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f193])).
% 0.09/0.57 fof(f319,plain,(
% 0.09/0.57 (((((((((~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))|~holdsAt(spinning(trolley10),n1))),
% 0.09/0.57 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.09/0.57 fof(f320,plain,(
% 0.09/0.57 ~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)|~holdsAt(spinning(trolley10),n1)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f319])).
% 0.09/0.57 fof(f339,definition,(
% 0.09/0.57 ![Event,Time]: (sP5_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))|(Event=push(agent9,trolley9)&Time=n0)))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.09/0.57 fof(f340,plain,(
% 0.09/0.57 ![Event,Time]: (sP2_prd(Time,Event)<=>(sP5_prd(Time,Event)|(Event=pull(agent10,trolley10)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f190,f339])).
% 0.09/0.57 fof(f341,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP2_prd(Time,Event)|(sP5_prd(Time,Event)|(Event=pull(agent10,trolley10)&Time=n0)))&(sP2_prd(Time,Event)|(~sP5_prd(Time,Event)&(~Event=pull(agent10,trolley10)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f340])).
% 0.09/0.57 fof(f342,plain,(
% 0.09/0.57 (![Event,Time]: (~sP2_prd(Time,Event)|(sP5_prd(Time,Event)|(Event=pull(agent10,trolley10)&Time=n0))))&(![Event,Time]: (sP2_prd(Time,Event)|(~sP5_prd(Time,Event)&(~Event=pull(agent10,trolley10)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f341])).
% 0.09/0.57 fof(f345,plain,(
% 0.09/0.57 ![X0,X1]: (sP2_prd(X0,X1)|~sP5_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f342])).
% 0.09/0.57 fof(f346,plain,(
% 0.09/0.57 ![X0,X1]: (sP2_prd(X0,X1)|~X1=pull(agent10,trolley10)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f342])).
% 0.09/0.57 fof(f362,definition,(
% 0.09/0.57 ![Event,Time]: (sP7_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.09/0.57 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.09/0.57 fof(f363,plain,(
% 0.09/0.57 ![Event,Time]: (sP5_prd(Time,Event)<=>(sP7_prd(Time,Event)|(Event=push(agent9,trolley9)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f339,f362])).
% 0.09/0.57 fof(f364,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP5_prd(Time,Event)|(sP7_prd(Time,Event)|(Event=push(agent9,trolley9)&Time=n0)))&(sP5_prd(Time,Event)|(~sP7_prd(Time,Event)&(~Event=push(agent9,trolley9)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f363])).
% 0.09/0.57 fof(f365,plain,(
% 0.09/0.57 (![Event,Time]: (~sP5_prd(Time,Event)|(sP7_prd(Time,Event)|(Event=push(agent9,trolley9)&Time=n0))))&(![Event,Time]: (sP5_prd(Time,Event)|(~sP7_prd(Time,Event)&(~Event=push(agent9,trolley9)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f364])).
% 0.09/0.57 fof(f368,plain,(
% 0.09/0.57 ![X0,X1]: (sP5_prd(X0,X1)|~sP7_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f365])).
% 0.09/0.57 fof(f369,plain,(
% 0.09/0.57 ![X0,X1]: (sP5_prd(X0,X1)|~X1=push(agent9,trolley9)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f365])).
% 0.09/0.57 fof(f379,definition,(
% 0.09/0.57 ![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.09/0.57 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.09/0.57 fof(f380,plain,(
% 0.09/0.57 ![Event,Time]: (sP7_prd(Time,Event)<=>(sP9_prd(Time,Event)|(Event=pull(agent9,trolley9)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f362,f379])).
% 0.09/0.57 fof(f381,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP7_prd(Time,Event)|(sP9_prd(Time,Event)|(Event=pull(agent9,trolley9)&Time=n0)))&(sP7_prd(Time,Event)|(~sP9_prd(Time,Event)&(~Event=pull(agent9,trolley9)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f380])).
% 0.09/0.57 fof(f382,plain,(
% 0.09/0.57 (![Event,Time]: (~sP7_prd(Time,Event)|(sP9_prd(Time,Event)|(Event=pull(agent9,trolley9)&Time=n0))))&(![Event,Time]: (sP7_prd(Time,Event)|(~sP9_prd(Time,Event)&(~Event=pull(agent9,trolley9)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f381])).
% 0.09/0.57 fof(f385,plain,(
% 0.09/0.57 ![X0,X1]: (sP7_prd(X0,X1)|~sP9_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f382])).
% 0.09/0.57 fof(f386,plain,(
% 0.09/0.57 ![X0,X1]: (sP7_prd(X0,X1)|~X1=pull(agent9,trolley9)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f382])).
% 0.09/0.57 fof(f396,definition,(
% 0.09/0.57 ![Event,Time]: (sP11_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.09/0.57 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.09/0.57 fof(f397,plain,(
% 0.09/0.57 ![Event,Time]: (sP9_prd(Time,Event)<=>(sP11_prd(Time,Event)|(Event=push(agent8,trolley8)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f379,f396])).
% 0.09/0.57 fof(f398,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP9_prd(Time,Event)|(sP11_prd(Time,Event)|(Event=push(agent8,trolley8)&Time=n0)))&(sP9_prd(Time,Event)|(~sP11_prd(Time,Event)&(~Event=push(agent8,trolley8)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f397])).
% 0.09/0.57 fof(f399,plain,(
% 0.09/0.57 (![Event,Time]: (~sP9_prd(Time,Event)|(sP11_prd(Time,Event)|(Event=push(agent8,trolley8)&Time=n0))))&(![Event,Time]: (sP9_prd(Time,Event)|(~sP11_prd(Time,Event)&(~Event=push(agent8,trolley8)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f398])).
% 0.09/0.57 fof(f402,plain,(
% 0.09/0.57 ![X0,X1]: (sP9_prd(X0,X1)|~sP11_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f399])).
% 0.09/0.57 fof(f403,plain,(
% 0.09/0.57 ![X0,X1]: (sP9_prd(X0,X1)|~X1=push(agent8,trolley8)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f399])).
% 0.09/0.57 fof(f410,definition,(
% 0.09/0.57 ![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)))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 0.09/0.57 fof(f411,plain,(
% 0.09/0.57 ![Event,Time]: (sP11_prd(Time,Event)<=>(sP12_prd(Time,Event)|(Event=pull(agent8,trolley8)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f396,f410])).
% 0.09/0.57 fof(f412,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP11_prd(Time,Event)|(sP12_prd(Time,Event)|(Event=pull(agent8,trolley8)&Time=n0)))&(sP11_prd(Time,Event)|(~sP12_prd(Time,Event)&(~Event=pull(agent8,trolley8)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f411])).
% 0.09/0.57 fof(f413,plain,(
% 0.09/0.57 (![Event,Time]: (~sP11_prd(Time,Event)|(sP12_prd(Time,Event)|(Event=pull(agent8,trolley8)&Time=n0))))&(![Event,Time]: (sP11_prd(Time,Event)|(~sP12_prd(Time,Event)&(~Event=pull(agent8,trolley8)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f412])).
% 0.09/0.57 fof(f416,plain,(
% 0.09/0.57 ![X0,X1]: (sP11_prd(X0,X1)|~sP12_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f413])).
% 0.09/0.57 fof(f417,plain,(
% 0.09/0.57 ![X0,X1]: (sP11_prd(X0,X1)|~X1=pull(agent8,trolley8)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f413])).
% 0.09/0.57 fof(f418,definition,(
% 0.09/0.57 ![Event,Time]: (sP13_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.09/0.57 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 0.09/0.57 fof(f419,plain,(
% 0.09/0.57 ![Event,Time]: (sP12_prd(Time,Event)<=>(sP13_prd(Time,Event)|(Event=push(agent7,trolley7)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f410,f418])).
% 0.09/0.57 fof(f420,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP12_prd(Time,Event)|(sP13_prd(Time,Event)|(Event=push(agent7,trolley7)&Time=n0)))&(sP12_prd(Time,Event)|(~sP13_prd(Time,Event)&(~Event=push(agent7,trolley7)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f419])).
% 0.09/0.57 fof(f421,plain,(
% 0.09/0.57 (![Event,Time]: (~sP12_prd(Time,Event)|(sP13_prd(Time,Event)|(Event=push(agent7,trolley7)&Time=n0))))&(![Event,Time]: (sP12_prd(Time,Event)|(~sP13_prd(Time,Event)&(~Event=push(agent7,trolley7)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f420])).
% 0.09/0.57 fof(f424,plain,(
% 0.09/0.57 ![X0,X1]: (sP12_prd(X0,X1)|~sP13_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f421])).
% 0.09/0.57 fof(f425,plain,(
% 0.09/0.57 ![X0,X1]: (sP12_prd(X0,X1)|~X1=push(agent7,trolley7)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f421])).
% 0.09/0.57 fof(f426,definition,(
% 0.09/0.57 ![Event,Time]: (sP14_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.09/0.57 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 0.09/0.57 fof(f427,plain,(
% 0.09/0.57 ![Event,Time]: (sP13_prd(Time,Event)<=>(sP14_prd(Time,Event)|(Event=pull(agent7,trolley7)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f418,f426])).
% 0.09/0.57 fof(f428,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP13_prd(Time,Event)|(sP14_prd(Time,Event)|(Event=pull(agent7,trolley7)&Time=n0)))&(sP13_prd(Time,Event)|(~sP14_prd(Time,Event)&(~Event=pull(agent7,trolley7)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f427])).
% 0.09/0.57 fof(f429,plain,(
% 0.09/0.57 (![Event,Time]: (~sP13_prd(Time,Event)|(sP14_prd(Time,Event)|(Event=pull(agent7,trolley7)&Time=n0))))&(![Event,Time]: (sP13_prd(Time,Event)|(~sP14_prd(Time,Event)&(~Event=pull(agent7,trolley7)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f428])).
% 0.09/0.57 fof(f432,plain,(
% 0.09/0.57 ![X0,X1]: (sP13_prd(X0,X1)|~sP14_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f429])).
% 0.09/0.57 fof(f433,plain,(
% 0.09/0.57 ![X0,X1]: (sP13_prd(X0,X1)|~X1=pull(agent7,trolley7)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f429])).
% 0.09/0.57 fof(f434,definition,(
% 0.09/0.57 ![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)))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sP15_prd])],[])).
% 0.09/0.57 fof(f435,plain,(
% 0.09/0.57 ![Event,Time]: (sP14_prd(Time,Event)<=>(sP15_prd(Time,Event)|(Event=push(agent6,trolley6)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f426,f434])).
% 0.09/0.57 fof(f436,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP14_prd(Time,Event)|(sP15_prd(Time,Event)|(Event=push(agent6,trolley6)&Time=n0)))&(sP14_prd(Time,Event)|(~sP15_prd(Time,Event)&(~Event=push(agent6,trolley6)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f435])).
% 0.09/0.57 fof(f437,plain,(
% 0.09/0.57 (![Event,Time]: (~sP14_prd(Time,Event)|(sP15_prd(Time,Event)|(Event=push(agent6,trolley6)&Time=n0))))&(![Event,Time]: (sP14_prd(Time,Event)|(~sP15_prd(Time,Event)&(~Event=push(agent6,trolley6)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f436])).
% 0.09/0.57 fof(f440,plain,(
% 0.09/0.57 ![X0,X1]: (sP14_prd(X0,X1)|~sP15_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f437])).
% 0.09/0.57 fof(f441,plain,(
% 0.09/0.57 ![X0,X1]: (sP14_prd(X0,X1)|~X1=push(agent6,trolley6)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f437])).
% 0.09/0.57 fof(f442,definition,(
% 0.09/0.57 ![Event,Time]: (sP16_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.09/0.57 introduced(definition,[new_symbols(definition,[sP16_prd])],[])).
% 0.09/0.57 fof(f443,plain,(
% 0.09/0.57 ![Event,Time]: (sP15_prd(Time,Event)<=>(sP16_prd(Time,Event)|(Event=pull(agent6,trolley6)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f434,f442])).
% 0.09/0.57 fof(f444,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP15_prd(Time,Event)|(sP16_prd(Time,Event)|(Event=pull(agent6,trolley6)&Time=n0)))&(sP15_prd(Time,Event)|(~sP16_prd(Time,Event)&(~Event=pull(agent6,trolley6)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f443])).
% 0.09/0.57 fof(f445,plain,(
% 0.09/0.57 (![Event,Time]: (~sP15_prd(Time,Event)|(sP16_prd(Time,Event)|(Event=pull(agent6,trolley6)&Time=n0))))&(![Event,Time]: (sP15_prd(Time,Event)|(~sP16_prd(Time,Event)&(~Event=pull(agent6,trolley6)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f444])).
% 0.09/0.57 fof(f448,plain,(
% 0.09/0.57 ![X0,X1]: (sP15_prd(X0,X1)|~sP16_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f445])).
% 0.09/0.57 fof(f449,plain,(
% 0.09/0.57 ![X0,X1]: (sP15_prd(X0,X1)|~X1=pull(agent6,trolley6)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f445])).
% 0.09/0.57 fof(f450,definition,(
% 0.09/0.57 ![Event,Time]: (sP17_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.09/0.57 introduced(definition,[new_symbols(definition,[sP17_prd])],[])).
% 0.09/0.57 fof(f451,plain,(
% 0.09/0.57 ![Event,Time]: (sP16_prd(Time,Event)<=>(sP17_prd(Time,Event)|(Event=push(agent5,trolley5)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f442,f450])).
% 0.09/0.57 fof(f452,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP16_prd(Time,Event)|(sP17_prd(Time,Event)|(Event=push(agent5,trolley5)&Time=n0)))&(sP16_prd(Time,Event)|(~sP17_prd(Time,Event)&(~Event=push(agent5,trolley5)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f451])).
% 0.09/0.57 fof(f453,plain,(
% 0.09/0.57 (![Event,Time]: (~sP16_prd(Time,Event)|(sP17_prd(Time,Event)|(Event=push(agent5,trolley5)&Time=n0))))&(![Event,Time]: (sP16_prd(Time,Event)|(~sP17_prd(Time,Event)&(~Event=push(agent5,trolley5)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f452])).
% 0.09/0.57 fof(f456,plain,(
% 0.09/0.57 ![X0,X1]: (sP16_prd(X0,X1)|~sP17_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f453])).
% 0.09/0.57 fof(f457,plain,(
% 0.09/0.57 ![X0,X1]: (sP16_prd(X0,X1)|~X1=push(agent5,trolley5)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f453])).
% 0.09/0.57 fof(f458,definition,(
% 0.09/0.57 ![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)))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sP18_prd])],[])).
% 0.09/0.57 fof(f459,plain,(
% 0.09/0.57 ![Event,Time]: (sP17_prd(Time,Event)<=>(sP18_prd(Time,Event)|(Event=pull(agent5,trolley5)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f450,f458])).
% 0.09/0.57 fof(f460,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP17_prd(Time,Event)|(sP18_prd(Time,Event)|(Event=pull(agent5,trolley5)&Time=n0)))&(sP17_prd(Time,Event)|(~sP18_prd(Time,Event)&(~Event=pull(agent5,trolley5)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f459])).
% 0.09/0.57 fof(f461,plain,(
% 0.09/0.57 (![Event,Time]: (~sP17_prd(Time,Event)|(sP18_prd(Time,Event)|(Event=pull(agent5,trolley5)&Time=n0))))&(![Event,Time]: (sP17_prd(Time,Event)|(~sP18_prd(Time,Event)&(~Event=pull(agent5,trolley5)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f460])).
% 0.09/0.57 fof(f464,plain,(
% 0.09/0.57 ![X0,X1]: (sP17_prd(X0,X1)|~sP18_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f461])).
% 0.09/0.57 fof(f465,plain,(
% 0.09/0.57 ![X0,X1]: (sP17_prd(X0,X1)|~X1=pull(agent5,trolley5)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f461])).
% 0.09/0.57 fof(f466,definition,(
% 0.09/0.57 ![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)))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sP19_prd])],[])).
% 0.09/0.57 fof(f467,plain,(
% 0.09/0.57 ![Event,Time]: (sP18_prd(Time,Event)<=>(sP19_prd(Time,Event)|(Event=push(agent4,trolley4)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f458,f466])).
% 0.09/0.57 fof(f468,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP18_prd(Time,Event)|(sP19_prd(Time,Event)|(Event=push(agent4,trolley4)&Time=n0)))&(sP18_prd(Time,Event)|(~sP19_prd(Time,Event)&(~Event=push(agent4,trolley4)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f467])).
% 0.09/0.57 fof(f469,plain,(
% 0.09/0.57 (![Event,Time]: (~sP18_prd(Time,Event)|(sP19_prd(Time,Event)|(Event=push(agent4,trolley4)&Time=n0))))&(![Event,Time]: (sP18_prd(Time,Event)|(~sP19_prd(Time,Event)&(~Event=push(agent4,trolley4)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f468])).
% 0.09/0.57 fof(f472,plain,(
% 0.09/0.57 ![X0,X1]: (sP18_prd(X0,X1)|~sP19_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f469])).
% 0.09/0.57 fof(f473,plain,(
% 0.09/0.57 ![X0,X1]: (sP18_prd(X0,X1)|~X1=push(agent4,trolley4)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f469])).
% 0.09/0.57 fof(f474,definition,(
% 0.09/0.57 ![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)))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sP20_prd])],[])).
% 0.09/0.57 fof(f475,plain,(
% 0.09/0.57 ![Event,Time]: (sP19_prd(Time,Event)<=>(sP20_prd(Time,Event)|(Event=pull(agent4,trolley4)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f466,f474])).
% 0.09/0.57 fof(f476,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP19_prd(Time,Event)|(sP20_prd(Time,Event)|(Event=pull(agent4,trolley4)&Time=n0)))&(sP19_prd(Time,Event)|(~sP20_prd(Time,Event)&(~Event=pull(agent4,trolley4)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f475])).
% 0.09/0.57 fof(f477,plain,(
% 0.09/0.57 (![Event,Time]: (~sP19_prd(Time,Event)|(sP20_prd(Time,Event)|(Event=pull(agent4,trolley4)&Time=n0))))&(![Event,Time]: (sP19_prd(Time,Event)|(~sP20_prd(Time,Event)&(~Event=pull(agent4,trolley4)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f476])).
% 0.09/0.57 fof(f480,plain,(
% 0.09/0.57 ![X0,X1]: (sP19_prd(X0,X1)|~sP20_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f477])).
% 0.09/0.57 fof(f481,plain,(
% 0.09/0.57 ![X0,X1]: (sP19_prd(X0,X1)|~X1=pull(agent4,trolley4)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f477])).
% 0.09/0.57 fof(f482,definition,(
% 0.09/0.57 ![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)))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sP21_prd])],[])).
% 0.09/0.57 fof(f483,plain,(
% 0.09/0.57 ![Event,Time]: (sP20_prd(Time,Event)<=>(sP21_prd(Time,Event)|(Event=push(agent3,trolley3)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f474,f482])).
% 0.09/0.57 fof(f484,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP20_prd(Time,Event)|(sP21_prd(Time,Event)|(Event=push(agent3,trolley3)&Time=n0)))&(sP20_prd(Time,Event)|(~sP21_prd(Time,Event)&(~Event=push(agent3,trolley3)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f483])).
% 0.09/0.57 fof(f485,plain,(
% 0.09/0.57 (![Event,Time]: (~sP20_prd(Time,Event)|(sP21_prd(Time,Event)|(Event=push(agent3,trolley3)&Time=n0))))&(![Event,Time]: (sP20_prd(Time,Event)|(~sP21_prd(Time,Event)&(~Event=push(agent3,trolley3)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f484])).
% 0.09/0.57 fof(f488,plain,(
% 0.09/0.57 ![X0,X1]: (sP20_prd(X0,X1)|~sP21_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f485])).
% 0.09/0.57 fof(f489,plain,(
% 0.09/0.57 ![X0,X1]: (sP20_prd(X0,X1)|~X1=push(agent3,trolley3)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f485])).
% 0.09/0.57 fof(f490,definition,(
% 0.09/0.57 ![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)))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sP22_prd])],[])).
% 0.09/0.57 fof(f491,plain,(
% 0.09/0.57 ![Event,Time]: (sP21_prd(Time,Event)<=>(sP22_prd(Time,Event)|(Event=pull(agent3,trolley3)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f482,f490])).
% 0.09/0.57 fof(f492,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP21_prd(Time,Event)|(sP22_prd(Time,Event)|(Event=pull(agent3,trolley3)&Time=n0)))&(sP21_prd(Time,Event)|(~sP22_prd(Time,Event)&(~Event=pull(agent3,trolley3)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f491])).
% 0.09/0.57 fof(f493,plain,(
% 0.09/0.57 (![Event,Time]: (~sP21_prd(Time,Event)|(sP22_prd(Time,Event)|(Event=pull(agent3,trolley3)&Time=n0))))&(![Event,Time]: (sP21_prd(Time,Event)|(~sP22_prd(Time,Event)&(~Event=pull(agent3,trolley3)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f492])).
% 0.09/0.57 fof(f496,plain,(
% 0.09/0.57 ![X0,X1]: (sP21_prd(X0,X1)|~sP22_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f493])).
% 0.09/0.57 fof(f497,plain,(
% 0.09/0.57 ![X0,X1]: (sP21_prd(X0,X1)|~X1=pull(agent3,trolley3)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f493])).
% 0.09/0.57 fof(f498,definition,(
% 0.09/0.57 ![Event,Time]: (sP23_prd(Time,Event)<=>(((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))|(Event=pull(agent2,trolley2)&Time=n0)))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sP23_prd])],[])).
% 0.09/0.57 fof(f499,plain,(
% 0.09/0.57 ![Event,Time]: (sP22_prd(Time,Event)<=>(sP23_prd(Time,Event)|(Event=push(agent2,trolley2)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f490,f498])).
% 0.09/0.57 fof(f500,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP22_prd(Time,Event)|(sP23_prd(Time,Event)|(Event=push(agent2,trolley2)&Time=n0)))&(sP22_prd(Time,Event)|(~sP23_prd(Time,Event)&(~Event=push(agent2,trolley2)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f499])).
% 0.09/0.57 fof(f501,plain,(
% 0.09/0.57 (![Event,Time]: (~sP22_prd(Time,Event)|(sP23_prd(Time,Event)|(Event=push(agent2,trolley2)&Time=n0))))&(![Event,Time]: (sP22_prd(Time,Event)|(~sP23_prd(Time,Event)&(~Event=push(agent2,trolley2)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f500])).
% 0.09/0.57 fof(f504,plain,(
% 0.09/0.57 ![X0,X1]: (sP22_prd(X0,X1)|~sP23_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f501])).
% 0.09/0.57 fof(f505,plain,(
% 0.09/0.57 ![X0,X1]: (sP22_prd(X0,X1)|~X1=push(agent2,trolley2)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f501])).
% 0.09/0.57 fof(f506,definition,(
% 0.09/0.57 ![Event,Time]: (sP24_prd(Time,Event)<=>((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0)))),
% 0.09/0.57 introduced(definition,[new_symbols(definition,[sP24_prd])],[])).
% 0.09/0.57 fof(f507,plain,(
% 0.09/0.57 ![Event,Time]: (sP23_prd(Time,Event)<=>(sP24_prd(Time,Event)|(Event=pull(agent2,trolley2)&Time=n0)))),
% 0.09/0.57 inference(formula_renaming,[status(thm)],[f498,f506])).
% 0.09/0.57 fof(f508,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP23_prd(Time,Event)|(sP24_prd(Time,Event)|(Event=pull(agent2,trolley2)&Time=n0)))&(sP23_prd(Time,Event)|(~sP24_prd(Time,Event)&(~Event=pull(agent2,trolley2)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f507])).
% 0.09/0.57 fof(f509,plain,(
% 0.09/0.57 (![Event,Time]: (~sP23_prd(Time,Event)|(sP24_prd(Time,Event)|(Event=pull(agent2,trolley2)&Time=n0))))&(![Event,Time]: (sP23_prd(Time,Event)|(~sP24_prd(Time,Event)&(~Event=pull(agent2,trolley2)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f508])).
% 0.09/0.57 fof(f512,plain,(
% 0.09/0.57 ![X0,X1]: (sP23_prd(X0,X1)|~sP24_prd(X0,X1))),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f509])).
% 0.09/0.57 fof(f513,plain,(
% 0.09/0.57 ![X0,X1]: (sP23_prd(X0,X1)|~X1=pull(agent2,trolley2)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f509])).
% 0.09/0.57 fof(f514,plain,(
% 0.09/0.57 ![Event,Time]: ((~sP24_prd(Time,Event)|((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0)))&(sP24_prd(Time,Event)|((~Event=pull(agent1,trolley1)|~Time=n0)&(~Event=push(agent1,trolley1)|~Time=n0))))),
% 0.09/0.57 inference(NNF_transformation,[status(thm)],[f506])).
% 0.09/0.57 fof(f515,plain,(
% 0.09/0.57 (![Event,Time]: (~sP24_prd(Time,Event)|((Event=pull(agent1,trolley1)&Time=n0)|(Event=push(agent1,trolley1)&Time=n0))))&(![Event,Time]: (sP24_prd(Time,Event)|((~Event=pull(agent1,trolley1)|~Time=n0)&(~Event=push(agent1,trolley1)|~Time=n0))))),
% 0.09/0.57 inference(miniscoping,[status(thm)],[f514])).
% 0.09/0.57 fof(f520,plain,(
% 0.09/0.57 ![X0,X1]: (sP24_prd(X0,X1)|~X1=pull(agent1,trolley1)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f515])).
% 0.09/0.57 fof(f521,plain,(
% 0.09/0.57 ![X0,X1]: (sP24_prd(X0,X1)|~X1=push(agent1,trolley1)|~X0=n0)),
% 0.09/0.57 inference(cnf_transformation,[status(thm)],[f515])).
% 0.09/0.57 fof(f522,plain,(
% 0.09/0.57 ![X0,X1,X2]: (initiates(pull(X0,X1),spinning(X1),X2)|~happens(push(X0,X1),X2))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f111])).
% 0.09/0.57 fof(f527,plain,(
% 0.09/0.57 happens(push(agent10,trolley10),n0)),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f197])).
% 0.09/0.57 fof(f534,plain,(
% 0.09/0.57 sP2_prd(n0,pull(agent10,trolley10))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f346])).
% 0.09/0.57 fof(f537,plain,(
% 0.09/0.57 sP5_prd(n0,push(agent9,trolley9))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f369])).
% 0.09/0.57 fof(f539,plain,(
% 0.09/0.57 sP7_prd(n0,pull(agent9,trolley9))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f386])).
% 0.09/0.57 fof(f541,plain,(
% 0.09/0.57 sP9_prd(n0,push(agent8,trolley8))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f403])).
% 0.09/0.57 fof(f543,plain,(
% 0.09/0.57 sP11_prd(n0,pull(agent8,trolley8))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f417])).
% 0.09/0.57 fof(f544,plain,(
% 0.09/0.57 sP12_prd(n0,push(agent7,trolley7))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f425])).
% 0.09/0.57 fof(f545,plain,(
% 0.09/0.57 sP13_prd(n0,pull(agent7,trolley7))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f433])).
% 0.09/0.57 fof(f546,plain,(
% 0.09/0.57 sP14_prd(n0,push(agent6,trolley6))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f441])).
% 0.09/0.57 fof(f547,plain,(
% 0.09/0.57 sP15_prd(n0,pull(agent6,trolley6))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f449])).
% 0.09/0.57 fof(f548,plain,(
% 0.09/0.57 sP16_prd(n0,push(agent5,trolley5))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f457])).
% 0.09/0.57 fof(f549,plain,(
% 0.09/0.57 sP17_prd(n0,pull(agent5,trolley5))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f465])).
% 0.09/0.57 fof(f550,plain,(
% 0.09/0.57 sP18_prd(n0,push(agent4,trolley4))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f473])).
% 0.09/0.57 fof(f551,plain,(
% 0.09/0.57 sP19_prd(n0,pull(agent4,trolley4))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f481])).
% 0.09/0.57 fof(f552,plain,(
% 0.09/0.57 sP20_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f489])).
% 0.09/0.57 fof(f553,plain,(
% 0.09/0.57 sP21_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f497])).
% 0.09/0.57 fof(f554,plain,(
% 0.09/0.57 sP22_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f505])).
% 0.09/0.57 fof(f555,plain,(
% 0.09/0.57 sP23_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f513])).
% 0.09/0.57 fof(f558,plain,(
% 0.09/0.57 sP24_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f520])).
% 0.09/0.57 fof(f559,plain,(
% 0.09/0.57 sP24_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(destructive_equality_resolution,[status(thm)],[f521])).
% 0.09/0.57 fof(f579,plain,(
% 0.09/0.57 ![X0,X1]: (~happens(X0,n0)|~initiates(X0,X1,n0)|holdsAt(X1,n1))),
% 0.09/0.57 inference(paramodulation,[status(thm)],[f132,f91])).
% 0.09/0.57 fof(f628,plain,(
% 0.09/0.57 happens(pull(agent10,trolley10),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f534,f196])).
% 0.09/0.57 fof(f629,plain,(
% 0.09/0.57 sP2_prd(n0,push(agent9,trolley9))),
% 0.09/0.57 inference(resolution,[status(thm)],[f537,f345])).
% 0.09/0.57 fof(f630,plain,(
% 0.09/0.57 sP5_prd(n0,pull(agent9,trolley9))),
% 0.09/0.57 inference(resolution,[status(thm)],[f539,f368])).
% 0.09/0.57 fof(f631,plain,(
% 0.09/0.57 sP7_prd(n0,push(agent8,trolley8))),
% 0.09/0.57 inference(resolution,[status(thm)],[f541,f385])).
% 0.09/0.57 fof(f632,plain,(
% 0.09/0.57 sP9_prd(n0,pull(agent8,trolley8))),
% 0.09/0.57 inference(resolution,[status(thm)],[f543,f402])).
% 0.09/0.57 fof(f635,plain,(
% 0.09/0.57 sP11_prd(n0,push(agent7,trolley7))),
% 0.09/0.57 inference(resolution,[status(thm)],[f544,f416])).
% 0.09/0.57 fof(f636,plain,(
% 0.09/0.57 sP12_prd(n0,pull(agent7,trolley7))),
% 0.09/0.57 inference(resolution,[status(thm)],[f545,f424])).
% 0.09/0.57 fof(f637,plain,(
% 0.09/0.57 sP13_prd(n0,push(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f546,f432])).
% 0.09/0.57 fof(f638,plain,(
% 0.09/0.57 sP14_prd(n0,pull(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f547,f440])).
% 0.09/0.57 fof(f639,plain,(
% 0.09/0.57 sP15_prd(n0,push(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f548,f448])).
% 0.09/0.57 fof(f640,plain,(
% 0.09/0.57 sP16_prd(n0,pull(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f549,f456])).
% 0.09/0.57 fof(f641,plain,(
% 0.09/0.57 sP17_prd(n0,push(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f550,f464])).
% 0.09/0.57 fof(f642,plain,(
% 0.09/0.57 sP18_prd(n0,pull(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f551,f472])).
% 0.09/0.57 fof(f643,plain,(
% 0.09/0.57 sP19_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f552,f480])).
% 0.09/0.57 fof(f644,plain,(
% 0.09/0.57 sP20_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f553,f488])).
% 0.09/0.57 fof(f645,plain,(
% 0.09/0.57 sP21_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f554,f496])).
% 0.09/0.57 fof(f646,plain,(
% 0.09/0.57 sP22_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f555,f504])).
% 0.09/0.57 fof(f675,plain,(
% 0.09/0.57 sP23_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f558,f512])).
% 0.09/0.57 fof(f676,plain,(
% 0.09/0.57 sP23_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f559,f512])).
% 0.09/0.57 fof(f741,plain,(
% 0.09/0.57 happens(push(agent9,trolley9),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f629,f196])).
% 0.09/0.57 fof(f742,plain,(
% 0.09/0.57 sP2_prd(n0,pull(agent9,trolley9))),
% 0.09/0.57 inference(resolution,[status(thm)],[f630,f345])).
% 0.09/0.57 fof(f743,plain,(
% 0.09/0.57 sP5_prd(n0,push(agent8,trolley8))),
% 0.09/0.57 inference(resolution,[status(thm)],[f631,f368])).
% 0.09/0.57 fof(f744,plain,(
% 0.09/0.57 sP7_prd(n0,pull(agent8,trolley8))),
% 0.09/0.57 inference(resolution,[status(thm)],[f632,f385])).
% 0.09/0.57 fof(f745,plain,(
% 0.09/0.57 sP9_prd(n0,push(agent7,trolley7))),
% 0.09/0.57 inference(resolution,[status(thm)],[f635,f402])).
% 0.09/0.57 fof(f758,plain,(
% 0.09/0.57 sP11_prd(n0,pull(agent7,trolley7))),
% 0.09/0.57 inference(resolution,[status(thm)],[f636,f416])).
% 0.09/0.57 fof(f759,plain,(
% 0.09/0.57 sP12_prd(n0,push(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f637,f424])).
% 0.09/0.57 fof(f760,plain,(
% 0.09/0.57 sP13_prd(n0,pull(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f638,f432])).
% 0.09/0.57 fof(f761,plain,(
% 0.09/0.57 sP14_prd(n0,push(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f639,f440])).
% 0.09/0.57 fof(f772,plain,(
% 0.09/0.57 sP15_prd(n0,pull(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f640,f448])).
% 0.09/0.57 fof(f773,plain,(
% 0.09/0.57 sP16_prd(n0,push(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f641,f456])).
% 0.09/0.57 fof(f774,plain,(
% 0.09/0.57 sP17_prd(n0,pull(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f642,f464])).
% 0.09/0.57 fof(f775,plain,(
% 0.09/0.57 sP18_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f643,f472])).
% 0.09/0.57 fof(f776,plain,(
% 0.09/0.57 sP19_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f644,f480])).
% 0.09/0.57 fof(f777,plain,(
% 0.09/0.57 sP20_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f645,f488])).
% 0.09/0.57 fof(f778,plain,(
% 0.09/0.57 sP21_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f646,f496])).
% 0.09/0.57 fof(f793,plain,(
% 0.09/0.57 sP22_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f675,f504])).
% 0.09/0.57 fof(f794,plain,(
% 0.09/0.57 sP22_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f676,f504])).
% 0.09/0.57 fof(f870,plain,(
% 0.09/0.57 happens(pull(agent9,trolley9),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f742,f196])).
% 0.09/0.57 fof(f871,plain,(
% 0.09/0.57 sP2_prd(n0,push(agent8,trolley8))),
% 0.09/0.57 inference(resolution,[status(thm)],[f743,f345])).
% 0.09/0.57 fof(f872,plain,(
% 0.09/0.57 sP5_prd(n0,pull(agent8,trolley8))),
% 0.09/0.57 inference(resolution,[status(thm)],[f744,f368])).
% 0.09/0.57 fof(f873,plain,(
% 0.09/0.57 sP7_prd(n0,push(agent7,trolley7))),
% 0.09/0.57 inference(resolution,[status(thm)],[f745,f385])).
% 0.09/0.57 fof(f890,plain,(
% 0.09/0.57 sP9_prd(n0,pull(agent7,trolley7))),
% 0.09/0.57 inference(resolution,[status(thm)],[f758,f402])).
% 0.09/0.57 fof(f891,plain,(
% 0.09/0.57 sP11_prd(n0,push(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f759,f416])).
% 0.09/0.57 fof(f892,plain,(
% 0.09/0.57 sP12_prd(n0,pull(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f760,f424])).
% 0.09/0.57 fof(f893,plain,(
% 0.09/0.57 sP13_prd(n0,push(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f761,f432])).
% 0.09/0.57 fof(f894,plain,(
% 0.09/0.57 sP14_prd(n0,pull(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f772,f440])).
% 0.09/0.57 fof(f895,plain,(
% 0.09/0.57 sP15_prd(n0,push(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f773,f448])).
% 0.09/0.57 fof(f901,plain,(
% 0.09/0.57 sP16_prd(n0,pull(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f774,f456])).
% 0.09/0.57 fof(f902,plain,(
% 0.09/0.57 sP17_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f775,f464])).
% 0.09/0.57 fof(f903,plain,(
% 0.09/0.57 sP18_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f776,f472])).
% 0.09/0.57 fof(f904,plain,(
% 0.09/0.57 sP19_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f777,f480])).
% 0.09/0.57 fof(f905,plain,(
% 0.09/0.57 sP20_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f778,f488])).
% 0.09/0.57 fof(f909,plain,(
% 0.09/0.57 sP21_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f793,f496])).
% 0.09/0.57 fof(f910,plain,(
% 0.09/0.57 sP21_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f794,f496])).
% 0.09/0.57 fof(f922,plain,(
% 0.09/0.57 happens(push(agent8,trolley8),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f871,f196])).
% 0.09/0.57 fof(f923,plain,(
% 0.09/0.57 sP2_prd(n0,pull(agent8,trolley8))),
% 0.09/0.57 inference(resolution,[status(thm)],[f872,f345])).
% 0.09/0.57 fof(f924,plain,(
% 0.09/0.57 sP5_prd(n0,push(agent7,trolley7))),
% 0.09/0.57 inference(resolution,[status(thm)],[f873,f368])).
% 0.09/0.57 fof(f932,plain,(
% 0.09/0.57 sP7_prd(n0,pull(agent7,trolley7))),
% 0.09/0.57 inference(resolution,[status(thm)],[f890,f385])).
% 0.09/0.57 fof(f933,plain,(
% 0.09/0.57 sP9_prd(n0,push(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f891,f402])).
% 0.09/0.57 fof(f934,plain,(
% 0.09/0.57 sP11_prd(n0,pull(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f892,f416])).
% 0.09/0.57 fof(f935,plain,(
% 0.09/0.57 sP12_prd(n0,push(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f893,f424])).
% 0.09/0.57 fof(f936,plain,(
% 0.09/0.57 sP13_prd(n0,pull(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f894,f432])).
% 0.09/0.57 fof(f937,plain,(
% 0.09/0.57 sP14_prd(n0,push(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f895,f440])).
% 0.09/0.57 fof(f938,plain,(
% 0.09/0.57 sP15_prd(n0,pull(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f901,f448])).
% 0.09/0.57 fof(f941,plain,(
% 0.09/0.57 sP16_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f902,f456])).
% 0.09/0.57 fof(f942,plain,(
% 0.09/0.57 sP17_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f903,f464])).
% 0.09/0.57 fof(f943,plain,(
% 0.09/0.57 sP18_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f904,f472])).
% 0.09/0.57 fof(f944,plain,(
% 0.09/0.57 sP19_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f905,f480])).
% 0.09/0.57 fof(f946,plain,(
% 0.09/0.57 sP20_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f909,f488])).
% 0.09/0.57 fof(f947,plain,(
% 0.09/0.57 sP20_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f910,f488])).
% 0.09/0.57 fof(f956,plain,(
% 0.09/0.57 happens(pull(agent8,trolley8),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f923,f196])).
% 0.09/0.57 fof(f960,plain,(
% 0.09/0.57 sP2_prd(n0,push(agent7,trolley7))),
% 0.09/0.57 inference(resolution,[status(thm)],[f924,f345])).
% 0.09/0.57 fof(f967,plain,(
% 0.09/0.57 sP5_prd(n0,pull(agent7,trolley7))),
% 0.09/0.57 inference(resolution,[status(thm)],[f932,f368])).
% 0.09/0.57 fof(f968,plain,(
% 0.09/0.57 sP7_prd(n0,push(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f933,f385])).
% 0.09/0.57 fof(f969,plain,(
% 0.09/0.57 sP9_prd(n0,pull(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f934,f402])).
% 0.09/0.57 fof(f970,plain,(
% 0.09/0.57 sP11_prd(n0,push(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f935,f416])).
% 0.09/0.57 fof(f971,plain,(
% 0.09/0.57 sP12_prd(n0,pull(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f936,f424])).
% 0.09/0.57 fof(f972,plain,(
% 0.09/0.57 sP13_prd(n0,push(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f937,f432])).
% 0.09/0.57 fof(f973,plain,(
% 0.09/0.57 sP14_prd(n0,pull(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f938,f440])).
% 0.09/0.57 fof(f974,plain,(
% 0.09/0.57 sP15_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f941,f448])).
% 0.09/0.57 fof(f975,plain,(
% 0.09/0.57 sP16_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f942,f456])).
% 0.09/0.57 fof(f980,plain,(
% 0.09/0.57 sP17_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f943,f464])).
% 0.09/0.57 fof(f981,plain,(
% 0.09/0.57 sP18_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f944,f472])).
% 0.09/0.57 fof(f982,plain,(
% 0.09/0.57 sP19_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f946,f480])).
% 0.09/0.57 fof(f983,plain,(
% 0.09/0.57 sP19_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f947,f480])).
% 0.09/0.57 fof(f992,plain,(
% 0.09/0.57 happens(push(agent7,trolley7),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f960,f196])).
% 0.09/0.57 fof(f996,plain,(
% 0.09/0.57 sP2_prd(n0,pull(agent7,trolley7))),
% 0.09/0.57 inference(resolution,[status(thm)],[f967,f345])).
% 0.09/0.57 fof(f997,plain,(
% 0.09/0.57 sP5_prd(n0,push(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f968,f368])).
% 0.09/0.57 fof(f998,plain,(
% 0.09/0.57 sP7_prd(n0,pull(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f969,f385])).
% 0.09/0.57 fof(f999,plain,(
% 0.09/0.57 sP9_prd(n0,push(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f970,f402])).
% 0.09/0.57 fof(f1000,plain,(
% 0.09/0.57 sP11_prd(n0,pull(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f971,f416])).
% 0.09/0.57 fof(f1005,plain,(
% 0.09/0.57 sP12_prd(n0,push(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f972,f424])).
% 0.09/0.57 fof(f1006,plain,(
% 0.09/0.57 sP13_prd(n0,pull(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f973,f432])).
% 0.09/0.57 fof(f1007,plain,(
% 0.09/0.57 sP14_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f974,f440])).
% 0.09/0.57 fof(f1008,plain,(
% 0.09/0.57 sP15_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f975,f448])).
% 0.09/0.57 fof(f1009,plain,(
% 0.09/0.57 sP16_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f980,f456])).
% 0.09/0.57 fof(f1010,plain,(
% 0.09/0.57 sP17_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f981,f464])).
% 0.09/0.57 fof(f1011,plain,(
% 0.09/0.57 sP18_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f982,f472])).
% 0.09/0.57 fof(f1012,plain,(
% 0.09/0.57 sP18_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f983,f472])).
% 0.09/0.57 fof(f1024,plain,(
% 0.09/0.57 happens(pull(agent7,trolley7),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f996,f196])).
% 0.09/0.57 fof(f1025,plain,(
% 0.09/0.57 sP2_prd(n0,push(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f997,f345])).
% 0.09/0.57 fof(f1026,plain,(
% 0.09/0.57 sP5_prd(n0,pull(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f998,f368])).
% 0.09/0.57 fof(f1027,plain,(
% 0.09/0.57 sP7_prd(n0,push(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f999,f385])).
% 0.09/0.57 fof(f1028,plain,(
% 0.09/0.57 sP9_prd(n0,pull(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1000,f402])).
% 0.09/0.57 fof(f1029,plain,(
% 0.09/0.57 sP11_prd(n0,push(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1005,f416])).
% 0.09/0.57 fof(f1030,plain,(
% 0.09/0.57 sP12_prd(n0,pull(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1006,f424])).
% 0.09/0.57 fof(f1035,plain,(
% 0.09/0.57 sP13_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1007,f432])).
% 0.09/0.57 fof(f1036,plain,(
% 0.09/0.57 sP14_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1008,f440])).
% 0.09/0.57 fof(f1037,plain,(
% 0.09/0.57 sP15_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1009,f448])).
% 0.09/0.57 fof(f1038,plain,(
% 0.09/0.57 sP16_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1010,f456])).
% 0.09/0.57 fof(f1040,plain,(
% 0.09/0.57 sP17_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1011,f464])).
% 0.09/0.57 fof(f1041,plain,(
% 0.09/0.57 sP17_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1012,f464])).
% 0.09/0.57 fof(f1051,plain,(
% 0.09/0.57 happens(push(agent6,trolley6),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1025,f196])).
% 0.09/0.57 fof(f1052,plain,(
% 0.09/0.57 sP2_prd(n0,pull(agent6,trolley6))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1026,f345])).
% 0.09/0.57 fof(f1053,plain,(
% 0.09/0.57 sP5_prd(n0,push(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1027,f368])).
% 0.09/0.57 fof(f1054,plain,(
% 0.09/0.57 sP7_prd(n0,pull(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1028,f385])).
% 0.09/0.57 fof(f1055,plain,(
% 0.09/0.57 sP9_prd(n0,push(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1029,f402])).
% 0.09/0.57 fof(f1056,plain,(
% 0.09/0.57 sP11_prd(n0,pull(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1030,f416])).
% 0.09/0.57 fof(f1057,plain,(
% 0.09/0.57 sP12_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1035,f424])).
% 0.09/0.57 fof(f1058,plain,(
% 0.09/0.57 sP13_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1036,f432])).
% 0.09/0.57 fof(f1059,plain,(
% 0.09/0.57 sP14_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1037,f440])).
% 0.09/0.57 fof(f1060,plain,(
% 0.09/0.57 sP15_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1038,f448])).
% 0.09/0.57 fof(f1061,plain,(
% 0.09/0.57 sP16_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1040,f456])).
% 0.09/0.57 fof(f1062,plain,(
% 0.09/0.57 sP16_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1041,f456])).
% 0.09/0.57 fof(f1075,plain,(
% 0.09/0.57 happens(pull(agent6,trolley6),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1052,f196])).
% 0.09/0.57 fof(f1077,plain,(
% 0.09/0.57 sP2_prd(n0,push(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1053,f345])).
% 0.09/0.57 fof(f1078,plain,(
% 0.09/0.57 sP5_prd(n0,pull(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1054,f368])).
% 0.09/0.57 fof(f1079,plain,(
% 0.09/0.57 sP7_prd(n0,push(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1055,f385])).
% 0.09/0.57 fof(f1080,plain,(
% 0.09/0.57 sP9_prd(n0,pull(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1056,f402])).
% 0.09/0.57 fof(f1081,plain,(
% 0.09/0.57 sP11_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1057,f416])).
% 0.09/0.57 fof(f1082,plain,(
% 0.09/0.57 sP12_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1058,f424])).
% 0.09/0.57 fof(f1083,plain,(
% 0.09/0.57 sP13_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1059,f432])).
% 0.09/0.57 fof(f1084,plain,(
% 0.09/0.57 sP14_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1060,f440])).
% 0.09/0.57 fof(f1093,plain,(
% 0.09/0.57 sP15_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1061,f448])).
% 0.09/0.57 fof(f1094,plain,(
% 0.09/0.57 sP15_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1062,f448])).
% 0.09/0.57 fof(f1102,plain,(
% 0.09/0.57 happens(push(agent5,trolley5),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1077,f196])).
% 0.09/0.57 fof(f1103,plain,(
% 0.09/0.57 sP2_prd(n0,pull(agent5,trolley5))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1078,f345])).
% 0.09/0.57 fof(f1104,plain,(
% 0.09/0.57 sP5_prd(n0,push(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1079,f368])).
% 0.09/0.57 fof(f1105,plain,(
% 0.09/0.57 sP7_prd(n0,pull(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1080,f385])).
% 0.09/0.57 fof(f1106,plain,(
% 0.09/0.57 sP9_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1081,f402])).
% 0.09/0.57 fof(f1107,plain,(
% 0.09/0.57 sP11_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1082,f416])).
% 0.09/0.57 fof(f1116,plain,(
% 0.09/0.57 sP12_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1083,f424])).
% 0.09/0.57 fof(f1117,plain,(
% 0.09/0.57 sP13_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1084,f432])).
% 0.09/0.57 fof(f1118,plain,(
% 0.09/0.57 sP14_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1093,f440])).
% 0.09/0.57 fof(f1119,plain,(
% 0.09/0.57 sP14_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1094,f440])).
% 0.09/0.57 fof(f1125,plain,(
% 0.09/0.57 happens(pull(agent5,trolley5),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1103,f196])).
% 0.09/0.57 fof(f1126,plain,(
% 0.09/0.57 sP2_prd(n0,push(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1104,f345])).
% 0.09/0.57 fof(f1127,plain,(
% 0.09/0.57 sP5_prd(n0,pull(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1105,f368])).
% 0.09/0.57 fof(f1128,plain,(
% 0.09/0.57 sP7_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1106,f385])).
% 0.09/0.57 fof(f1129,plain,(
% 0.09/0.57 sP9_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1107,f402])).
% 0.09/0.57 fof(f1131,plain,(
% 0.09/0.57 sP11_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1116,f416])).
% 0.09/0.57 fof(f1132,plain,(
% 0.09/0.57 sP12_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1117,f424])).
% 0.09/0.57 fof(f1133,plain,(
% 0.09/0.57 sP13_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1118,f432])).
% 0.09/0.57 fof(f1134,plain,(
% 0.09/0.57 sP13_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1119,f432])).
% 0.09/0.57 fof(f1138,plain,(
% 0.09/0.57 happens(push(agent4,trolley4),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1126,f196])).
% 0.09/0.57 fof(f1139,plain,(
% 0.09/0.57 sP2_prd(n0,pull(agent4,trolley4))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1127,f345])).
% 0.09/0.57 fof(f1140,plain,(
% 0.09/0.57 sP5_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1128,f368])).
% 0.09/0.57 fof(f1141,plain,(
% 0.09/0.57 sP7_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1129,f385])).
% 0.09/0.57 fof(f1148,plain,(
% 0.09/0.57 sP9_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1131,f402])).
% 0.09/0.57 fof(f1149,plain,(
% 0.09/0.57 sP11_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1132,f416])).
% 0.09/0.57 fof(f1150,plain,(
% 0.09/0.57 sP12_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1133,f424])).
% 0.09/0.57 fof(f1151,plain,(
% 0.09/0.57 sP12_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1134,f424])).
% 0.09/0.57 fof(f1155,plain,(
% 0.09/0.57 happens(pull(agent4,trolley4),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1139,f196])).
% 0.09/0.57 fof(f1156,plain,(
% 0.09/0.57 sP2_prd(n0,push(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1140,f345])).
% 0.09/0.57 fof(f1157,plain,(
% 0.09/0.57 sP5_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1141,f368])).
% 0.09/0.57 fof(f1159,plain,(
% 0.09/0.57 sP7_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1148,f385])).
% 0.09/0.57 fof(f1160,plain,(
% 0.09/0.57 sP9_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1149,f402])).
% 0.09/0.57 fof(f1163,plain,(
% 0.09/0.57 sP11_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1150,f416])).
% 0.09/0.57 fof(f1164,plain,(
% 0.09/0.57 sP11_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1151,f416])).
% 0.09/0.57 fof(f1165,plain,(
% 0.09/0.57 happens(push(agent3,trolley3),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1156,f196])).
% 0.09/0.57 fof(f1166,plain,(
% 0.09/0.57 sP2_prd(n0,pull(agent3,trolley3))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1157,f345])).
% 0.09/0.57 fof(f1168,plain,(
% 0.09/0.57 sP5_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1159,f368])).
% 0.09/0.57 fof(f1169,plain,(
% 0.09/0.57 sP7_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1160,f385])).
% 0.09/0.57 fof(f1170,plain,(
% 0.09/0.57 sP9_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1163,f402])).
% 0.09/0.57 fof(f1171,plain,(
% 0.09/0.57 sP9_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1164,f402])).
% 0.09/0.57 fof(f1173,plain,(
% 0.09/0.57 happens(pull(agent3,trolley3),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1166,f196])).
% 0.09/0.57 fof(f1177,plain,(
% 0.09/0.57 sP2_prd(n0,push(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1168,f345])).
% 0.09/0.57 fof(f1178,plain,(
% 0.09/0.57 sP5_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1169,f368])).
% 0.09/0.57 fof(f1179,plain,(
% 0.09/0.57 sP7_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1170,f385])).
% 0.09/0.57 fof(f1180,plain,(
% 0.09/0.57 sP7_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1171,f385])).
% 0.09/0.57 fof(f1182,plain,(
% 0.09/0.57 happens(push(agent2,trolley2),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1177,f196])).
% 0.09/0.57 fof(f1183,plain,(
% 0.09/0.57 sP2_prd(n0,pull(agent2,trolley2))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1178,f345])).
% 0.09/0.57 fof(f1184,plain,(
% 0.09/0.57 sP5_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1179,f368])).
% 0.09/0.57 fof(f1185,plain,(
% 0.09/0.57 sP5_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1180,f368])).
% 0.09/0.57 fof(f1187,plain,(
% 0.09/0.57 happens(pull(agent2,trolley2),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1183,f196])).
% 0.09/0.57 fof(f1188,plain,(
% 0.09/0.57 sP2_prd(n0,pull(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1184,f345])).
% 0.09/0.57 fof(f1191,plain,(
% 0.09/0.57 sP2_prd(n0,push(agent1,trolley1))),
% 0.09/0.57 inference(resolution,[status(thm)],[f1185,f345])).
% 0.09/0.57 fof(f1192,plain,(
% 0.09/0.57 happens(pull(agent1,trolley1),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1188,f196])).
% 0.09/0.57 fof(f1193,plain,(
% 0.09/0.57 happens(push(agent1,trolley1),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1191,f196])).
% 0.09/0.57 fof(f1439,plain,(
% 0.09/0.57 ![X0,X1]: (~happens(pull(X0,X1),n0)|holdsAt(spinning(X1),n1)|~happens(push(X0,X1),n0))),
% 0.09/0.57 inference(resolution,[status(thm)],[f579,f522])).
% 0.09/0.57 fof(f2284,plain,(
% 0.09/0.57 holdsAt(spinning(trolley1),n1)|~happens(push(agent1,trolley1),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1439,f1192])).
% 0.09/0.57 fof(f2285,plain,(
% 0.09/0.57 holdsAt(spinning(trolley2),n1)|~happens(push(agent2,trolley2),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1439,f1187])).
% 0.09/0.57 fof(f2286,plain,(
% 0.09/0.57 holdsAt(spinning(trolley3),n1)|~happens(push(agent3,trolley3),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1439,f1173])).
% 0.09/0.57 fof(f2287,plain,(
% 0.09/0.57 holdsAt(spinning(trolley4),n1)|~happens(push(agent4,trolley4),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1439,f1155])).
% 0.09/0.57 fof(f2288,plain,(
% 0.09/0.57 holdsAt(spinning(trolley5),n1)|~happens(push(agent5,trolley5),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1439,f1125])).
% 0.09/0.57 fof(f2289,plain,(
% 0.09/0.57 holdsAt(spinning(trolley6),n1)|~happens(push(agent6,trolley6),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1439,f1075])).
% 0.09/0.57 fof(f2290,plain,(
% 0.09/0.57 holdsAt(spinning(trolley7),n1)|~happens(push(agent7,trolley7),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1439,f1024])).
% 0.09/0.57 fof(f2291,plain,(
% 0.09/0.57 holdsAt(spinning(trolley8),n1)|~happens(push(agent8,trolley8),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1439,f956])).
% 0.09/0.57 fof(f2292,plain,(
% 0.09/0.57 holdsAt(spinning(trolley9),n1)|~happens(push(agent9,trolley9),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1439,f870])).
% 0.09/0.57 fof(f2293,plain,(
% 0.09/0.57 holdsAt(spinning(trolley10),n1)|~happens(push(agent10,trolley10),n0)),
% 0.09/0.57 inference(resolution,[status(thm)],[f1439,f628])).
% 0.09/0.57 fof(f2294,plain,(
% 0.09/0.57 ~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)|~holdsAt(spinning(trolley10),n1)),
% 0.09/0.57 inference(backward_subsumption_resolution,[status(thm)],[f320,f2295])).
% 0.09/0.57 fof(f2295,plain,(
% 0.09/0.57 holdsAt(spinning(trolley1),n1)),
% 0.09/0.57 inference(forward_subsumption_resolution,[status(thm)],[f2284,f1193])).
% 0.09/0.57 fof(f2296,plain,(
% 0.09/0.57 holdsAt(spinning(trolley2),n1)),
% 0.09/0.57 inference(forward_subsumption_resolution,[status(thm)],[f2285,f1182])).
% 0.09/0.57 fof(f2297,plain,(
% 0.09/0.57 holdsAt(spinning(trolley3),n1)),
% 0.09/0.57 inference(forward_subsumption_resolution,[status(thm)],[f2286,f1165])).
% 0.09/0.57 fof(f2298,plain,(
% 0.09/0.57 holdsAt(spinning(trolley4),n1)),
% 0.09/0.57 inference(forward_subsumption_resolution,[status(thm)],[f2287,f1138])).
% 0.09/0.57 fof(f2299,plain,(
% 0.09/0.57 holdsAt(spinning(trolley5),n1)),
% 0.09/0.57 inference(forward_subsumption_resolution,[status(thm)],[f2288,f1102])).
% 0.09/0.57 fof(f2300,plain,(
% 0.09/0.57 holdsAt(spinning(trolley6),n1)),
% 0.09/0.57 inference(forward_subsumption_resolution,[status(thm)],[f2289,f1051])).
% 0.09/0.57 fof(f2301,plain,(
% 0.09/0.57 holdsAt(spinning(trolley7),n1)),
% 0.09/0.57 inference(forward_subsumption_resolution,[status(thm)],[f2290,f992])).
% 0.09/0.57 fof(f2302,plain,(
% 0.09/0.57 holdsAt(spinning(trolley8),n1)),
% 1.17/0.59 inference(forward_subsumption_resolution,[status(thm)],[f2291,f922])).
% 1.17/0.59 fof(f2303,plain,(
% 1.17/0.59 holdsAt(spinning(trolley9),n1)),
% 1.17/0.59 inference(forward_subsumption_resolution,[status(thm)],[f2292,f741])).
% 1.17/0.59 fof(f2304,plain,(
% 1.17/0.59 holdsAt(spinning(trolley10),n1)),
% 1.17/0.59 inference(forward_subsumption_resolution,[status(thm)],[f2293,f527])).
% 1.17/0.59 fof(f2305,plain,(
% 1.17/0.59 ~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)|~holdsAt(spinning(trolley10),n1)),
% 1.17/0.59 inference(forward_subsumption_resolution,[status(thm)],[f2294,f2296])).
% 1.17/0.59 fof(f2327,plain,(
% 1.17/0.59 ~holdsAt(spinning(trolley3),n1)|~holdsAt(spinning(trolley5),n1)|~holdsAt(spinning(trolley6),n1)|~holdsAt(spinning(trolley7),n1)|~holdsAt(spinning(trolley8),n1)|~holdsAt(spinning(trolley9),n1)|~holdsAt(spinning(trolley10),n1)),
% 1.17/0.59 inference(resolution,[status(thm)],[f2298,f2305])).
% 1.17/0.59 fof(f2331,plain,(
% 1.17/0.59 ~holdsAt(spinning(trolley5),n1)|~holdsAt(spinning(trolley6),n1)|~holdsAt(spinning(trolley7),n1)|~holdsAt(spinning(trolley8),n1)|~holdsAt(spinning(trolley9),n1)|~holdsAt(spinning(trolley10),n1)),
% 1.17/0.59 inference(forward_subsumption_resolution,[status(thm)],[f2327,f2297])).
% 1.17/0.59 fof(f2418,plain,(
% 1.17/0.59 ~holdsAt(spinning(trolley5),n1)|~holdsAt(spinning(trolley7),n1)|~holdsAt(spinning(trolley8),n1)|~holdsAt(spinning(trolley9),n1)|~holdsAt(spinning(trolley10),n1)),
% 1.17/0.59 inference(resolution,[status(thm)],[f2331,f2300])).
% 1.17/0.59 fof(f2423,plain,(
% 1.17/0.59 ~holdsAt(spinning(trolley7),n1)|~holdsAt(spinning(trolley8),n1)|~holdsAt(spinning(trolley9),n1)|~holdsAt(spinning(trolley10),n1)),
% 1.17/0.59 inference(forward_subsumption_resolution,[status(thm)],[f2418,f2299])).
% 1.17/0.59 fof(f2428,plain,(
% 1.17/0.59 ~holdsAt(spinning(trolley7),n1)|~holdsAt(spinning(trolley9),n1)|~holdsAt(spinning(trolley10),n1)),
% 1.17/0.59 inference(resolution,[status(thm)],[f2423,f2302])).
% 1.17/0.59 fof(f2431,plain,(
% 1.17/0.59 ~holdsAt(spinning(trolley9),n1)|~holdsAt(spinning(trolley10),n1)),
% 1.17/0.59 inference(forward_subsumption_resolution,[status(thm)],[f2428,f2301])).
% 1.17/0.59 fof(f2434,plain,(
% 1.17/0.59 ~holdsAt(spinning(trolley9),n1)),
% 1.17/0.59 inference(resolution,[status(thm)],[f2431,f2304])).
% 1.17/0.59 fof(f2435,plain,(
% 1.17/0.59 $false),
% 1.17/0.59 inference(forward_subsumption_resolution,[status(thm)],[f2434,f2303])).
% 1.17/0.59 % SZS output end CNFRefutation for theBenchmark.p
% 1.17/0.60 % Elapsed time: 0.223379 seconds
% 1.17/0.60 % CPU time: 1.451631 seconds
% 1.17/0.60 % Total memory used: 136.352 MB
% 1.17/0.60 % Net memory used: 134.978 MB
%------------------------------------------------------------------------------