%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR024+1.009 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:12:51 PM UTC 2026
% Result : Theorem 0.14s 0.78s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 22
% Syntax : Number of formulae : 334 ( 192 unt; 17 def)
% Number of atoms : 1152 ( 580 equ)
% Maximal formula atoms : 37 ( 3 avg)
% Number of connectives : 1110 ( 292 ~; 450 |; 331 &)
% ( 36 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 1 prp; 0-5 aty)
% Number of functors : 30 ( 30 usr; 20 con; 0-3 aty)
% Number of variables : 302 ( 292 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [Event,Time,Fluent] :
( ( initiates(Event,Fluent,Time)
& happens(Event,Time) )
=> holdsAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [Event,Fluent,Time] :
( initiates(Event,Fluent,Time)
<=> ? [Agent,Trolley] :
( ( happens(push(Agent,Trolley),Time)
& Fluent = spinning(Trolley)
& Event = pull(Agent,Trolley) )
| ( ~ happens(push(Agent,Trolley),Time)
& Fluent = backwards(Trolley)
& Event = pull(Agent,Trolley) )
| ( ~ happens(pull(Agent,Trolley),Time)
& Fluent = forwards(Trolley)
& Event = push(Agent,Trolley) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [Event,Time] :
( happens(Event,Time)
<=> ( ( Time = n0
& Event = push(agent9,trolley9) )
| ( Time = n0
& Event = pull(agent9,trolley9) )
| ( Time = n0
& Event = push(agent8,trolley8) )
| ( Time = n0
& Event = pull(agent8,trolley8) )
| ( Time = n0
& Event = push(agent7,trolley7) )
| ( Time = n0
& Event = pull(agent7,trolley7) )
| ( Time = n0
& Event = push(agent6,trolley6) )
| ( Time = n0
& Event = pull(agent6,trolley6) )
| ( Time = n0
& Event = push(agent5,trolley5) )
| ( Time = n0
& Event = pull(agent5,trolley5) )
| ( Time = n0
& Event = push(agent4,trolley4) )
| ( Time = n0
& Event = pull(agent4,trolley4) )
| ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,conjecture,
( holdsAt(spinning(trolley9),n1)
& holdsAt(spinning(trolley8),n1)
& holdsAt(spinning(trolley7),n1)
& holdsAt(spinning(trolley6),n1)
& holdsAt(spinning(trolley5),n1)
& holdsAt(spinning(trolley4),n1)
& holdsAt(spinning(trolley3),n1)
& holdsAt(spinning(trolley2),n1)
& holdsAt(spinning(trolley1),n1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,negated_conjecture,
~ ( holdsAt(spinning(trolley9),n1)
& holdsAt(spinning(trolley8),n1)
& holdsAt(spinning(trolley7),n1)
& holdsAt(spinning(trolley6),n1)
& holdsAt(spinning(trolley5),n1)
& holdsAt(spinning(trolley4),n1)
& holdsAt(spinning(trolley3),n1)
& holdsAt(spinning(trolley2),n1)
& holdsAt(spinning(trolley1),n1) ),
inference(negated_conjecture,[status(cth)],[f58]) ).
fof(f98,plain,
! [Event,Time,Fluent] :
( holdsAt(Fluent,plus(Time,n1))
| ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f99,plain,
! [Time,Fluent] :
( holdsAt(Fluent,plus(Time,n1))
| ! [Event] :
( ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f98]) ).
fof(f100,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f111,definition,
! [Event,Fluent,Time,Agent,Trolley] :
( sP0_prd(Trolley,Agent,Time,Fluent,Event)
<=> ( ( ~ happens(push(Agent,Trolley),Time)
& Fluent = backwards(Trolley)
& Event = pull(Agent,Trolley) )
| ( ~ happens(pull(Agent,Trolley),Time)
& Fluent = forwards(Trolley)
& Event = push(Agent,Trolley) ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f112,plain,
! [Event,Fluent,Time] :
( initiates(Event,Fluent,Time)
<=> ? [Agent,Trolley] :
( ( happens(push(Agent,Trolley),Time)
& Fluent = spinning(Trolley)
& Event = pull(Agent,Trolley) )
| sP0_prd(Trolley,Agent,Time,Fluent,Event) ) ),
inference(formula_renaming,[status(thm)],[f13,f111]) ).
fof(f113,plain,
! [Event,Fluent,Time] :
( ( ! [Agent,Trolley] :
( ( ~ happens(push(Agent,Trolley),Time)
| Fluent != spinning(Trolley)
| Event != pull(Agent,Trolley) )
& ~ sP0_prd(Trolley,Agent,Time,Fluent,Event) )
| initiates(Event,Fluent,Time) )
& ( ? [Agent,Trolley] :
( ( happens(push(Agent,Trolley),Time)
& Fluent = spinning(Trolley)
& Event = pull(Agent,Trolley) )
| sP0_prd(Trolley,Agent,Time,Fluent,Event) )
| ~ initiates(Event,Fluent,Time) ) ),
inference(NNF_transformation,[status(thm)],[f112]) ).
fof(f114,plain,
( ! [Event,Fluent,Time] :
( ( ! [Agent,Trolley] :
( ~ happens(push(Agent,Trolley),Time)
| Fluent != spinning(Trolley)
| Event != pull(Agent,Trolley) )
& ! [Agent,Trolley] : ~ sP0_prd(Trolley,Agent,Time,Fluent,Event) )
| initiates(Event,Fluent,Time) )
& ! [Event,Fluent,Time] :
( ? [Agent,Trolley] :
( happens(push(Agent,Trolley),Time)
& Fluent = spinning(Trolley)
& Event = pull(Agent,Trolley) )
| ? [Agent,Trolley] : sP0_prd(Trolley,Agent,Time,Fluent,Event)
| ~ initiates(Event,Fluent,Time) ) ),
inference(miniscoping,[status(thm)],[f113]) ).
fof(f115,plain,
( ! [Event,Fluent,Time] :
( ( ! [Agent,Trolley] :
( ~ happens(push(Agent,Trolley),Time)
| Fluent != spinning(Trolley)
| Event != pull(Agent,Trolley) )
& ! [Agent,Trolley] : ~ sP0_prd(Trolley,Agent,Time,Fluent,Event) )
| initiates(Event,Fluent,Time) )
& ! [Event,Fluent,Time] :
( ( happens(push(sK10_skl(Time,Fluent,Event),sK11_skl(Time,Fluent,Event)),Time)
& Fluent = spinning(sK11_skl(Time,Fluent,Event))
& Event = pull(sK10_skl(Time,Fluent,Event),sK11_skl(Time,Fluent,Event)) )
| sP0_prd(sK9_skl(Time,Fluent,Event),sK8_skl(Time,Fluent,Event),Time,Fluent,Event)
| ~ initiates(Event,Fluent,Time) ) ),
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]) ).
fof(f120,plain,
! [X0,X1,X2,X3,X4] :
( ~ happens(push(X3,X4),X2)
| X1 != spinning(X4)
| X0 != pull(X3,X4)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f141,plain,
plus(n0,n1) = n1,
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f220,definition,
! [Event,Time] :
( sP4_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent9,trolley9) )
| ( Time = n0
& Event = push(agent8,trolley8) )
| ( Time = n0
& Event = pull(agent8,trolley8) )
| ( Time = n0
& Event = push(agent7,trolley7) )
| ( Time = n0
& Event = pull(agent7,trolley7) )
| ( Time = n0
& Event = push(agent6,trolley6) )
| ( Time = n0
& Event = pull(agent6,trolley6) )
| ( Time = n0
& Event = push(agent5,trolley5) )
| ( Time = n0
& Event = pull(agent5,trolley5) )
| ( Time = n0
& Event = push(agent4,trolley4) )
| ( Time = n0
& Event = pull(agent4,trolley4) )
| ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f221,plain,
! [Event,Time] :
( happens(Event,Time)
<=> ( ( Time = n0
& Event = push(agent9,trolley9) )
| sP4_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f48,f220]) ).
fof(f222,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent9,trolley9) )
& ~ sP4_prd(Time,Event) )
| happens(Event,Time) )
& ( ( Time = n0
& Event = push(agent9,trolley9) )
| sP4_prd(Time,Event)
| ~ happens(Event,Time) ) ),
inference(NNF_transformation,[status(thm)],[f221]) ).
fof(f223,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent9,trolley9) )
& ~ sP4_prd(Time,Event) )
| happens(Event,Time) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent9,trolley9) )
| sP4_prd(Time,Event)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f222]) ).
fof(f226,plain,
! [X0,X1] :
( ~ sP4_prd(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f227,plain,
! [X0,X1] :
( X1 != n0
| X0 != push(agent9,trolley9)
| happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f336,plain,
( ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(pre_NNF_transformation,[status(thm)],[f59]) ).
fof(f337,plain,
( ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f374,definition,
! [Event,Time] :
( sP9_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent8,trolley8) )
| ( Time = n0
& Event = pull(agent8,trolley8) )
| ( Time = n0
& Event = push(agent7,trolley7) )
| ( Time = n0
& Event = pull(agent7,trolley7) )
| ( Time = n0
& Event = push(agent6,trolley6) )
| ( Time = n0
& Event = pull(agent6,trolley6) )
| ( Time = n0
& Event = push(agent5,trolley5) )
| ( Time = n0
& Event = pull(agent5,trolley5) )
| ( Time = n0
& Event = push(agent4,trolley4) )
| ( Time = n0
& Event = pull(agent4,trolley4) )
| ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP9_prd])],[]) ).
fof(f375,plain,
! [Event,Time] :
( sP4_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent9,trolley9) )
| sP9_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f220,f374]) ).
fof(f376,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent9,trolley9) )
& ~ sP9_prd(Time,Event) )
| sP4_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent9,trolley9) )
| sP9_prd(Time,Event)
| ~ sP4_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f375]) ).
fof(f377,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent9,trolley9) )
& ~ sP9_prd(Time,Event) )
| sP4_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent9,trolley9) )
| sP9_prd(Time,Event)
| ~ sP4_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f376]) ).
fof(f380,plain,
! [X0,X1] :
( ~ sP9_prd(X0,X1)
| sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f377]) ).
fof(f381,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent9,trolley9)
| sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f377]) ).
fof(f412,definition,
! [Event,Time] :
( sP12_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent8,trolley8) )
| ( Time = n0
& Event = push(agent7,trolley7) )
| ( Time = n0
& Event = pull(agent7,trolley7) )
| ( Time = n0
& Event = push(agent6,trolley6) )
| ( Time = n0
& Event = pull(agent6,trolley6) )
| ( Time = n0
& Event = push(agent5,trolley5) )
| ( Time = n0
& Event = pull(agent5,trolley5) )
| ( Time = n0
& Event = push(agent4,trolley4) )
| ( Time = n0
& Event = pull(agent4,trolley4) )
| ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP12_prd])],[]) ).
fof(f413,plain,
! [Event,Time] :
( sP9_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent8,trolley8) )
| sP12_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f374,f412]) ).
fof(f414,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent8,trolley8) )
& ~ sP12_prd(Time,Event) )
| sP9_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent8,trolley8) )
| sP12_prd(Time,Event)
| ~ sP9_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f413]) ).
fof(f415,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent8,trolley8) )
& ~ sP12_prd(Time,Event) )
| sP9_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent8,trolley8) )
| sP12_prd(Time,Event)
| ~ sP9_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f414]) ).
fof(f418,plain,
! [X0,X1] :
( ~ sP12_prd(X0,X1)
| sP9_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f419,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent8,trolley8)
| sP9_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f438,definition,
! [Event,Time] :
( sP15_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent7,trolley7) )
| ( Time = n0
& Event = pull(agent7,trolley7) )
| ( Time = n0
& Event = push(agent6,trolley6) )
| ( Time = n0
& Event = pull(agent6,trolley6) )
| ( Time = n0
& Event = push(agent5,trolley5) )
| ( Time = n0
& Event = pull(agent5,trolley5) )
| ( Time = n0
& Event = push(agent4,trolley4) )
| ( Time = n0
& Event = pull(agent4,trolley4) )
| ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP15_prd])],[]) ).
fof(f439,plain,
! [Event,Time] :
( sP12_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent8,trolley8) )
| sP15_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f412,f438]) ).
fof(f440,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent8,trolley8) )
& ~ sP15_prd(Time,Event) )
| sP12_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent8,trolley8) )
| sP15_prd(Time,Event)
| ~ sP12_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f439]) ).
fof(f441,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent8,trolley8) )
& ~ sP15_prd(Time,Event) )
| sP12_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent8,trolley8) )
| sP15_prd(Time,Event)
| ~ sP12_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f440]) ).
fof(f444,plain,
! [X0,X1] :
( ~ sP15_prd(X0,X1)
| sP12_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f441]) ).
fof(f445,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent8,trolley8)
| sP12_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f441]) ).
fof(f464,definition,
! [Event,Time] :
( sP18_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent7,trolley7) )
| ( Time = n0
& Event = push(agent6,trolley6) )
| ( Time = n0
& Event = pull(agent6,trolley6) )
| ( Time = n0
& Event = push(agent5,trolley5) )
| ( Time = n0
& Event = pull(agent5,trolley5) )
| ( Time = n0
& Event = push(agent4,trolley4) )
| ( Time = n0
& Event = pull(agent4,trolley4) )
| ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP18_prd])],[]) ).
fof(f465,plain,
! [Event,Time] :
( sP15_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent7,trolley7) )
| sP18_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f438,f464]) ).
fof(f466,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent7,trolley7) )
& ~ sP18_prd(Time,Event) )
| sP15_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent7,trolley7) )
| sP18_prd(Time,Event)
| ~ sP15_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f465]) ).
fof(f467,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent7,trolley7) )
& ~ sP18_prd(Time,Event) )
| sP15_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent7,trolley7) )
| sP18_prd(Time,Event)
| ~ sP15_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f466]) ).
fof(f470,plain,
! [X0,X1] :
( ~ sP18_prd(X0,X1)
| sP15_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f467]) ).
fof(f471,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent7,trolley7)
| sP15_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f467]) ).
fof(f484,definition,
! [Event,Time] :
( sP19_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent6,trolley6) )
| ( Time = n0
& Event = pull(agent6,trolley6) )
| ( Time = n0
& Event = push(agent5,trolley5) )
| ( Time = n0
& Event = pull(agent5,trolley5) )
| ( Time = n0
& Event = push(agent4,trolley4) )
| ( Time = n0
& Event = pull(agent4,trolley4) )
| ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP19_prd])],[]) ).
fof(f485,plain,
! [Event,Time] :
( sP18_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent7,trolley7) )
| sP19_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f464,f484]) ).
fof(f486,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent7,trolley7) )
& ~ sP19_prd(Time,Event) )
| sP18_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent7,trolley7) )
| sP19_prd(Time,Event)
| ~ sP18_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f485]) ).
fof(f487,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent7,trolley7) )
& ~ sP19_prd(Time,Event) )
| sP18_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent7,trolley7) )
| sP19_prd(Time,Event)
| ~ sP18_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f486]) ).
fof(f490,plain,
! [X0,X1] :
( ~ sP19_prd(X0,X1)
| sP18_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f487]) ).
fof(f491,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent7,trolley7)
| sP18_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f487]) ).
fof(f492,definition,
! [Event,Time] :
( sP20_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent6,trolley6) )
| ( Time = n0
& Event = push(agent5,trolley5) )
| ( Time = n0
& Event = pull(agent5,trolley5) )
| ( Time = n0
& Event = push(agent4,trolley4) )
| ( Time = n0
& Event = pull(agent4,trolley4) )
| ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP20_prd])],[]) ).
fof(f493,plain,
! [Event,Time] :
( sP19_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent6,trolley6) )
| sP20_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f484,f492]) ).
fof(f494,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent6,trolley6) )
& ~ sP20_prd(Time,Event) )
| sP19_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent6,trolley6) )
| sP20_prd(Time,Event)
| ~ sP19_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f493]) ).
fof(f495,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent6,trolley6) )
& ~ sP20_prd(Time,Event) )
| sP19_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent6,trolley6) )
| sP20_prd(Time,Event)
| ~ sP19_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f494]) ).
fof(f498,plain,
! [X0,X1] :
( ~ sP20_prd(X0,X1)
| sP19_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f495]) ).
fof(f499,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent6,trolley6)
| sP19_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f495]) ).
fof(f500,definition,
! [Event,Time] :
( sP21_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent5,trolley5) )
| ( Time = n0
& Event = pull(agent5,trolley5) )
| ( Time = n0
& Event = push(agent4,trolley4) )
| ( Time = n0
& Event = pull(agent4,trolley4) )
| ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP21_prd])],[]) ).
fof(f501,plain,
! [Event,Time] :
( sP20_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent6,trolley6) )
| sP21_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f492,f500]) ).
fof(f502,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent6,trolley6) )
& ~ sP21_prd(Time,Event) )
| sP20_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent6,trolley6) )
| sP21_prd(Time,Event)
| ~ sP20_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f501]) ).
fof(f503,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent6,trolley6) )
& ~ sP21_prd(Time,Event) )
| sP20_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent6,trolley6) )
| sP21_prd(Time,Event)
| ~ sP20_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f502]) ).
fof(f506,plain,
! [X0,X1] :
( ~ sP21_prd(X0,X1)
| sP20_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f503]) ).
fof(f507,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent6,trolley6)
| sP20_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f503]) ).
fof(f508,definition,
! [Event,Time] :
( sP22_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent5,trolley5) )
| ( Time = n0
& Event = push(agent4,trolley4) )
| ( Time = n0
& Event = pull(agent4,trolley4) )
| ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP22_prd])],[]) ).
fof(f509,plain,
! [Event,Time] :
( sP21_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent5,trolley5) )
| sP22_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f500,f508]) ).
fof(f510,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent5,trolley5) )
& ~ sP22_prd(Time,Event) )
| sP21_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent5,trolley5) )
| sP22_prd(Time,Event)
| ~ sP21_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f509]) ).
fof(f511,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent5,trolley5) )
& ~ sP22_prd(Time,Event) )
| sP21_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent5,trolley5) )
| sP22_prd(Time,Event)
| ~ sP21_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f510]) ).
fof(f514,plain,
! [X0,X1] :
( ~ sP22_prd(X0,X1)
| sP21_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f511]) ).
fof(f515,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent5,trolley5)
| sP21_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f511]) ).
fof(f516,definition,
! [Event,Time] :
( sP23_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent4,trolley4) )
| ( Time = n0
& Event = pull(agent4,trolley4) )
| ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP23_prd])],[]) ).
fof(f517,plain,
! [Event,Time] :
( sP22_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent5,trolley5) )
| sP23_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f508,f516]) ).
fof(f518,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent5,trolley5) )
& ~ sP23_prd(Time,Event) )
| sP22_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent5,trolley5) )
| sP23_prd(Time,Event)
| ~ sP22_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f517]) ).
fof(f519,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent5,trolley5) )
& ~ sP23_prd(Time,Event) )
| sP22_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent5,trolley5) )
| sP23_prd(Time,Event)
| ~ sP22_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f518]) ).
fof(f522,plain,
! [X0,X1] :
( ~ sP23_prd(X0,X1)
| sP22_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f519]) ).
fof(f523,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent5,trolley5)
| sP22_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f519]) ).
fof(f524,definition,
! [Event,Time] :
( sP24_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent4,trolley4) )
| ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP24_prd])],[]) ).
fof(f525,plain,
! [Event,Time] :
( sP23_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent4,trolley4) )
| sP24_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f516,f524]) ).
fof(f526,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent4,trolley4) )
& ~ sP24_prd(Time,Event) )
| sP23_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent4,trolley4) )
| sP24_prd(Time,Event)
| ~ sP23_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f525]) ).
fof(f527,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent4,trolley4) )
& ~ sP24_prd(Time,Event) )
| sP23_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent4,trolley4) )
| sP24_prd(Time,Event)
| ~ sP23_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f526]) ).
fof(f530,plain,
! [X0,X1] :
( ~ sP24_prd(X0,X1)
| sP23_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f527]) ).
fof(f531,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent4,trolley4)
| sP23_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f527]) ).
fof(f532,definition,
! [Event,Time] :
( sP25_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP25_prd])],[]) ).
fof(f533,plain,
! [Event,Time] :
( sP24_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent4,trolley4) )
| sP25_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f524,f532]) ).
fof(f534,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent4,trolley4) )
& ~ sP25_prd(Time,Event) )
| sP24_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent4,trolley4) )
| sP25_prd(Time,Event)
| ~ sP24_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f533]) ).
fof(f535,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent4,trolley4) )
& ~ sP25_prd(Time,Event) )
| sP24_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent4,trolley4) )
| sP25_prd(Time,Event)
| ~ sP24_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f534]) ).
fof(f538,plain,
! [X0,X1] :
( ~ sP25_prd(X0,X1)
| sP24_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f535]) ).
fof(f539,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent4,trolley4)
| sP24_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f535]) ).
fof(f540,definition,
! [Event,Time] :
( sP26_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP26_prd])],[]) ).
fof(f541,plain,
! [Event,Time] :
( sP25_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent3,trolley3) )
| sP26_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f532,f540]) ).
fof(f542,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent3,trolley3) )
& ~ sP26_prd(Time,Event) )
| sP25_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent3,trolley3) )
| sP26_prd(Time,Event)
| ~ sP25_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f541]) ).
fof(f543,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent3,trolley3) )
& ~ sP26_prd(Time,Event) )
| sP25_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent3,trolley3) )
| sP26_prd(Time,Event)
| ~ sP25_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f542]) ).
fof(f546,plain,
! [X0,X1] :
( ~ sP26_prd(X0,X1)
| sP25_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f543]) ).
fof(f547,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent3,trolley3)
| sP25_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f543]) ).
fof(f548,definition,
! [Event,Time] :
( sP27_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP27_prd])],[]) ).
fof(f549,plain,
! [Event,Time] :
( sP26_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent3,trolley3) )
| sP27_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f540,f548]) ).
fof(f550,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent3,trolley3) )
& ~ sP27_prd(Time,Event) )
| sP26_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent3,trolley3) )
| sP27_prd(Time,Event)
| ~ sP26_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f549]) ).
fof(f551,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent3,trolley3) )
& ~ sP27_prd(Time,Event) )
| sP26_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent3,trolley3) )
| sP27_prd(Time,Event)
| ~ sP26_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f550]) ).
fof(f554,plain,
! [X0,X1] :
( ~ sP27_prd(X0,X1)
| sP26_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f551]) ).
fof(f555,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent3,trolley3)
| sP26_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f551]) ).
fof(f556,definition,
! [Event,Time] :
( sP28_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP28_prd])],[]) ).
fof(f557,plain,
! [Event,Time] :
( sP27_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent2,trolley2) )
| sP28_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f548,f556]) ).
fof(f558,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent2,trolley2) )
& ~ sP28_prd(Time,Event) )
| sP27_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent2,trolley2) )
| sP28_prd(Time,Event)
| ~ sP27_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f557]) ).
fof(f559,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent2,trolley2) )
& ~ sP28_prd(Time,Event) )
| sP27_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent2,trolley2) )
| sP28_prd(Time,Event)
| ~ sP27_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f558]) ).
fof(f562,plain,
! [X0,X1] :
( ~ sP28_prd(X0,X1)
| sP27_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f559]) ).
fof(f563,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent2,trolley2)
| sP27_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f559]) ).
fof(f564,definition,
! [Event,Time] :
( sP29_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP29_prd])],[]) ).
fof(f565,plain,
! [Event,Time] :
( sP28_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent2,trolley2) )
| sP29_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f556,f564]) ).
fof(f566,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent2,trolley2) )
& ~ sP29_prd(Time,Event) )
| sP28_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent2,trolley2) )
| sP29_prd(Time,Event)
| ~ sP28_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f565]) ).
fof(f567,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent2,trolley2) )
& ~ sP29_prd(Time,Event) )
| sP28_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent2,trolley2) )
| sP29_prd(Time,Event)
| ~ sP28_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f566]) ).
fof(f570,plain,
! [X0,X1] :
( ~ sP29_prd(X0,X1)
| sP28_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f567]) ).
fof(f571,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent2,trolley2)
| sP28_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f567]) ).
fof(f572,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent1,trolley1) )
& ( Time != n0
| Event != pull(agent1,trolley1) ) )
| sP29_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) )
| ~ sP29_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f564]) ).
fof(f573,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent1,trolley1) )
& ( Time != n0
| Event != pull(agent1,trolley1) ) )
| sP29_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) )
| ~ sP29_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f572]) ).
fof(f578,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent1,trolley1)
| sP29_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f573]) ).
fof(f579,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent1,trolley1)
| sP29_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f573]) ).
fof(f580,plain,
! [X0,X1,X2] :
( ~ happens(push(X0,X1),X2)
| initiates(pull(X0,X1),spinning(X1),X2) ),
inference(destructive_equality_resolution,[status(thm)],[f120]) ).
fof(f587,plain,
happens(push(agent9,trolley9),n0),
inference(destructive_equality_resolution,[status(thm)],[f227]) ).
fof(f596,plain,
sP4_prd(n0,pull(agent9,trolley9)),
inference(destructive_equality_resolution,[status(thm)],[f381]) ).
fof(f601,plain,
sP9_prd(n0,push(agent8,trolley8)),
inference(destructive_equality_resolution,[status(thm)],[f419]) ).
fof(f604,plain,
sP12_prd(n0,pull(agent8,trolley8)),
inference(destructive_equality_resolution,[status(thm)],[f445]) ).
fof(f607,plain,
sP15_prd(n0,push(agent7,trolley7)),
inference(destructive_equality_resolution,[status(thm)],[f471]) ).
fof(f610,plain,
sP18_prd(n0,pull(agent7,trolley7)),
inference(destructive_equality_resolution,[status(thm)],[f491]) ).
fof(f611,plain,
sP19_prd(n0,push(agent6,trolley6)),
inference(destructive_equality_resolution,[status(thm)],[f499]) ).
fof(f612,plain,
sP20_prd(n0,pull(agent6,trolley6)),
inference(destructive_equality_resolution,[status(thm)],[f507]) ).
fof(f613,plain,
sP21_prd(n0,push(agent5,trolley5)),
inference(destructive_equality_resolution,[status(thm)],[f515]) ).
fof(f614,plain,
sP22_prd(n0,pull(agent5,trolley5)),
inference(destructive_equality_resolution,[status(thm)],[f523]) ).
fof(f615,plain,
sP23_prd(n0,push(agent4,trolley4)),
inference(destructive_equality_resolution,[status(thm)],[f531]) ).
fof(f616,plain,
sP24_prd(n0,pull(agent4,trolley4)),
inference(destructive_equality_resolution,[status(thm)],[f539]) ).
fof(f617,plain,
sP25_prd(n0,push(agent3,trolley3)),
inference(destructive_equality_resolution,[status(thm)],[f547]) ).
fof(f618,plain,
sP26_prd(n0,pull(agent3,trolley3)),
inference(destructive_equality_resolution,[status(thm)],[f555]) ).
fof(f619,plain,
sP27_prd(n0,push(agent2,trolley2)),
inference(destructive_equality_resolution,[status(thm)],[f563]) ).
fof(f620,plain,
sP28_prd(n0,pull(agent2,trolley2)),
inference(destructive_equality_resolution,[status(thm)],[f571]) ).
fof(f623,plain,
sP29_prd(n0,pull(agent1,trolley1)),
inference(destructive_equality_resolution,[status(thm)],[f578]) ).
fof(f624,plain,
sP29_prd(n0,push(agent1,trolley1)),
inference(destructive_equality_resolution,[status(thm)],[f579]) ).
fof(f741,plain,
initiates(pull(agent9,trolley9),spinning(trolley9),n0),
inference(resolution,[status(thm)],[f587,f580]) ).
fof(f743,plain,
happens(pull(agent9,trolley9),n0),
inference(resolution,[status(thm)],[f596,f226]) ).
fof(f745,plain,
sP4_prd(n0,push(agent8,trolley8)),
inference(resolution,[status(thm)],[f601,f380]) ).
fof(f747,plain,
sP9_prd(n0,pull(agent8,trolley8)),
inference(resolution,[status(thm)],[f604,f418]) ).
fof(f749,plain,
sP12_prd(n0,push(agent7,trolley7)),
inference(resolution,[status(thm)],[f607,f444]) ).
fof(f751,plain,
sP15_prd(n0,pull(agent7,trolley7)),
inference(resolution,[status(thm)],[f610,f470]) ).
fof(f753,plain,
sP18_prd(n0,push(agent6,trolley6)),
inference(resolution,[status(thm)],[f611,f490]) ).
fof(f755,plain,
sP19_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f612,f498]) ).
fof(f757,plain,
sP20_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f613,f506]) ).
fof(f759,plain,
sP21_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f614,f514]) ).
fof(f761,plain,
sP22_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f615,f522]) ).
fof(f763,plain,
sP23_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f616,f530]) ).
fof(f768,plain,
sP24_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f617,f538]) ).
fof(f770,plain,
sP25_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f618,f546]) ).
fof(f772,plain,
sP26_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f619,f554]) ).
fof(f774,plain,
sP27_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f620,f562]) ).
fof(f776,plain,
sP28_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f623,f570]) ).
fof(f778,plain,
sP28_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f624,f570]) ).
fof(f886,plain,
happens(push(agent8,trolley8),n0),
inference(resolution,[status(thm)],[f745,f226]) ).
fof(f888,plain,
sP4_prd(n0,pull(agent8,trolley8)),
inference(resolution,[status(thm)],[f747,f380]) ).
fof(f890,plain,
sP9_prd(n0,push(agent7,trolley7)),
inference(resolution,[status(thm)],[f749,f418]) ).
fof(f892,plain,
sP12_prd(n0,pull(agent7,trolley7)),
inference(resolution,[status(thm)],[f751,f444]) ).
fof(f894,plain,
sP15_prd(n0,push(agent6,trolley6)),
inference(resolution,[status(thm)],[f753,f470]) ).
fof(f896,plain,
sP18_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f755,f490]) ).
fof(f898,plain,
sP19_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f757,f498]) ).
fof(f900,plain,
sP20_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f759,f506]) ).
fof(f902,plain,
sP21_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f761,f514]) ).
fof(f904,plain,
sP22_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f763,f522]) ).
fof(f906,plain,
sP23_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f768,f530]) ).
fof(f908,plain,
sP24_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f770,f538]) ).
fof(f910,plain,
sP25_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f772,f546]) ).
fof(f912,plain,
sP26_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f774,f554]) ).
fof(f914,plain,
sP27_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f776,f562]) ).
fof(f916,plain,
sP27_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f778,f562]) ).
fof(f1040,plain,
initiates(pull(agent8,trolley8),spinning(trolley8),n0),
inference(resolution,[status(thm)],[f886,f580]) ).
fof(f1044,plain,
happens(pull(agent8,trolley8),n0),
inference(resolution,[status(thm)],[f888,f226]) ).
fof(f1046,plain,
sP4_prd(n0,push(agent7,trolley7)),
inference(resolution,[status(thm)],[f890,f380]) ).
fof(f1048,plain,
sP9_prd(n0,pull(agent7,trolley7)),
inference(resolution,[status(thm)],[f892,f418]) ).
fof(f1050,plain,
sP12_prd(n0,push(agent6,trolley6)),
inference(resolution,[status(thm)],[f894,f444]) ).
fof(f1052,plain,
sP15_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f896,f470]) ).
fof(f1054,plain,
sP18_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f898,f490]) ).
fof(f1056,plain,
sP19_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f900,f498]) ).
fof(f1058,plain,
sP20_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f902,f506]) ).
fof(f1060,plain,
sP21_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f904,f514]) ).
fof(f1062,plain,
sP22_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f906,f522]) ).
fof(f1064,plain,
sP23_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f908,f530]) ).
fof(f1066,plain,
sP24_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f910,f538]) ).
fof(f1068,plain,
sP25_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f912,f546]) ).
fof(f1070,plain,
sP26_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f914,f554]) ).
fof(f1072,plain,
sP26_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f916,f554]) ).
fof(f1133,plain,
happens(push(agent7,trolley7),n0),
inference(resolution,[status(thm)],[f1046,f226]) ).
fof(f1135,plain,
sP4_prd(n0,pull(agent7,trolley7)),
inference(resolution,[status(thm)],[f1048,f380]) ).
fof(f1137,plain,
sP9_prd(n0,push(agent6,trolley6)),
inference(resolution,[status(thm)],[f1050,f418]) ).
fof(f1139,plain,
sP12_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f1052,f444]) ).
fof(f1141,plain,
sP15_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f1054,f470]) ).
fof(f1143,plain,
sP18_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f1056,f490]) ).
fof(f1145,plain,
sP19_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1058,f498]) ).
fof(f1147,plain,
sP20_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1060,f506]) ).
fof(f1153,plain,
sP21_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1062,f514]) ).
fof(f1155,plain,
sP22_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1064,f522]) ).
fof(f1157,plain,
sP23_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1066,f530]) ).
fof(f1159,plain,
sP24_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1068,f538]) ).
fof(f1161,plain,
sP25_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f1070,f546]) ).
fof(f1163,plain,
sP25_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f1072,f546]) ).
fof(f1210,plain,
initiates(pull(agent7,trolley7),spinning(trolley7),n0),
inference(resolution,[status(thm)],[f1133,f580]) ).
fof(f1213,plain,
happens(pull(agent7,trolley7),n0),
inference(resolution,[status(thm)],[f1135,f226]) ).
fof(f1215,plain,
sP4_prd(n0,push(agent6,trolley6)),
inference(resolution,[status(thm)],[f1137,f380]) ).
fof(f1217,plain,
sP9_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f1139,f418]) ).
fof(f1219,plain,
sP12_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f1141,f444]) ).
fof(f1221,plain,
sP15_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f1143,f470]) ).
fof(f1223,plain,
sP18_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1145,f490]) ).
fof(f1225,plain,
sP19_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1147,f498]) ).
fof(f1227,plain,
sP20_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1153,f506]) ).
fof(f1229,plain,
sP21_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1155,f514]) ).
fof(f1231,plain,
sP22_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1157,f522]) ).
fof(f1233,plain,
sP23_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1159,f530]) ).
fof(f1235,plain,
sP24_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f1161,f538]) ).
fof(f1237,plain,
sP24_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f1163,f538]) ).
fof(f1275,plain,
happens(push(agent6,trolley6),n0),
inference(resolution,[status(thm)],[f1215,f226]) ).
fof(f1277,plain,
sP4_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f1217,f380]) ).
fof(f1279,plain,
sP9_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f1219,f418]) ).
fof(f1281,plain,
sP12_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f1221,f444]) ).
fof(f1283,plain,
sP15_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1223,f470]) ).
fof(f1285,plain,
sP18_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1225,f490]) ).
fof(f1291,plain,
sP19_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1227,f498]) ).
fof(f1293,plain,
sP20_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1229,f506]) ).
fof(f1295,plain,
sP21_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1231,f514]) ).
fof(f1297,plain,
sP22_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1233,f522]) ).
fof(f1299,plain,
sP23_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f1235,f530]) ).
fof(f1301,plain,
sP23_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f1237,f530]) ).
fof(f1327,plain,
initiates(pull(agent6,trolley6),spinning(trolley6),n0),
inference(resolution,[status(thm)],[f1275,f580]) ).
fof(f1330,plain,
happens(pull(agent6,trolley6),n0),
inference(resolution,[status(thm)],[f1277,f226]) ).
fof(f1332,plain,
sP4_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f1279,f380]) ).
fof(f1334,plain,
sP9_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f1281,f418]) ).
fof(f1336,plain,
sP12_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1283,f444]) ).
fof(f1338,plain,
sP15_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1285,f470]) ).
fof(f1340,plain,
sP18_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1291,f490]) ).
fof(f1342,plain,
sP19_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1293,f498]) ).
fof(f1344,plain,
sP20_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1295,f506]) ).
fof(f1349,plain,
sP21_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1297,f514]) ).
fof(f1351,plain,
sP22_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f1299,f522]) ).
fof(f1353,plain,
sP22_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f1301,f522]) ).
fof(f1372,plain,
happens(push(agent5,trolley5),n0),
inference(resolution,[status(thm)],[f1332,f226]) ).
fof(f1374,plain,
sP4_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f1334,f380]) ).
fof(f1376,plain,
sP9_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1336,f418]) ).
fof(f1378,plain,
sP12_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1338,f444]) ).
fof(f1380,plain,
sP15_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1340,f470]) ).
fof(f1382,plain,
sP18_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1342,f490]) ).
fof(f1384,plain,
sP19_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1344,f498]) ).
fof(f1386,plain,
sP20_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1349,f506]) ).
fof(f1388,plain,
sP21_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f1351,f514]) ).
fof(f1390,plain,
sP21_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f1353,f514]) ).
fof(f1399,plain,
initiates(pull(agent5,trolley5),spinning(trolley5),n0),
inference(resolution,[status(thm)],[f1372,f580]) ).
fof(f1408,plain,
happens(pull(agent5,trolley5),n0),
inference(resolution,[status(thm)],[f1374,f226]) ).
fof(f1410,plain,
sP4_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1376,f380]) ).
fof(f1412,plain,
sP9_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1378,f418]) ).
fof(f1414,plain,
sP12_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1380,f444]) ).
fof(f1416,plain,
sP15_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1382,f470]) ).
fof(f1418,plain,
sP18_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1384,f490]) ).
fof(f1423,plain,
sP19_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1386,f498]) ).
fof(f1425,plain,
sP20_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f1388,f506]) ).
fof(f1427,plain,
sP20_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f1390,f506]) ).
fof(f1431,plain,
happens(push(agent4,trolley4),n0),
inference(resolution,[status(thm)],[f1410,f226]) ).
fof(f1433,plain,
sP4_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1412,f380]) ).
fof(f1435,plain,
sP9_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1414,f418]) ).
fof(f1437,plain,
sP12_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1416,f444]) ).
fof(f1439,plain,
sP15_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1418,f470]) ).
fof(f1441,plain,
sP18_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1423,f490]) ).
fof(f1443,plain,
sP19_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f1425,f498]) ).
fof(f1445,plain,
sP19_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f1427,f498]) ).
fof(f1454,plain,
initiates(pull(agent4,trolley4),spinning(trolley4),n0),
inference(resolution,[status(thm)],[f1431,f580]) ).
fof(f1457,plain,
happens(pull(agent4,trolley4),n0),
inference(resolution,[status(thm)],[f1433,f226]) ).
fof(f1459,plain,
sP4_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1435,f380]) ).
fof(f1461,plain,
sP9_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1437,f418]) ).
fof(f1463,plain,
sP12_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1439,f444]) ).
fof(f1465,plain,
sP15_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1441,f470]) ).
fof(f1467,plain,
sP18_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f1443,f490]) ).
fof(f1469,plain,
sP18_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f1445,f490]) ).
fof(f1473,plain,
happens(push(agent3,trolley3),n0),
inference(resolution,[status(thm)],[f1459,f226]) ).
fof(f1475,plain,
sP4_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1461,f380]) ).
fof(f1477,plain,
sP9_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1463,f418]) ).
fof(f1479,plain,
sP12_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1465,f444]) ).
fof(f1481,plain,
sP15_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f1467,f470]) ).
fof(f1483,plain,
sP15_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f1469,f470]) ).
fof(f1485,plain,
initiates(pull(agent3,trolley3),spinning(trolley3),n0),
inference(resolution,[status(thm)],[f1473,f580]) ).
fof(f1488,plain,
happens(pull(agent3,trolley3),n0),
inference(resolution,[status(thm)],[f1475,f226]) ).
fof(f1490,plain,
sP4_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1477,f380]) ).
fof(f1492,plain,
sP9_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1479,f418]) ).
fof(f1494,plain,
sP12_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f1481,f444]) ).
fof(f1496,plain,
sP12_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f1483,f444]) ).
fof(f1500,plain,
happens(push(agent2,trolley2),n0),
inference(resolution,[status(thm)],[f1490,f226]) ).
fof(f1502,plain,
sP4_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1492,f380]) ).
fof(f1507,plain,
sP9_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f1494,f418]) ).
fof(f1509,plain,
sP9_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f1496,f418]) ).
fof(f1511,plain,
initiates(pull(agent2,trolley2),spinning(trolley2),n0),
inference(resolution,[status(thm)],[f1500,f580]) ).
fof(f1514,plain,
happens(pull(agent2,trolley2),n0),
inference(resolution,[status(thm)],[f1502,f226]) ).
fof(f1516,plain,
sP4_prd(n0,pull(agent1,trolley1)),
inference(resolution,[status(thm)],[f1507,f380]) ).
fof(f1518,plain,
sP4_prd(n0,push(agent1,trolley1)),
inference(resolution,[status(thm)],[f1509,f380]) ).
fof(f1522,plain,
happens(pull(agent1,trolley1),n0),
inference(resolution,[status(thm)],[f1516,f226]) ).
fof(f1524,plain,
happens(push(agent1,trolley1),n0),
inference(resolution,[status(thm)],[f1518,f226]) ).
fof(f1528,plain,
initiates(pull(agent1,trolley1),spinning(trolley1),n0),
inference(resolution,[status(thm)],[f1524,f580]) ).
fof(f2161,plain,
( holdsAt(spinning(trolley9),plus(n0,n1))
| ~ happens(pull(agent9,trolley9),n0) ),
inference(resolution,[status(thm)],[f741,f100]) ).
fof(f2162,plain,
( holdsAt(spinning(trolley9),n1)
| ~ happens(pull(agent9,trolley9),n0) ),
inference(forward_demodulation,[status(thm)],[f141,f2161]) ).
fof(f2163,plain,
( ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(backward_subsumption_resolution,[status(thm)],[f337,f2164]) ).
fof(f2164,plain,
holdsAt(spinning(trolley9),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2162,f743]) ).
fof(f2169,plain,
( holdsAt(spinning(trolley8),plus(n0,n1))
| ~ happens(pull(agent8,trolley8),n0) ),
inference(resolution,[status(thm)],[f1040,f100]) ).
fof(f2170,plain,
( holdsAt(spinning(trolley8),n1)
| ~ happens(pull(agent8,trolley8),n0) ),
inference(forward_demodulation,[status(thm)],[f141,f2169]) ).
fof(f2171,plain,
( ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2163,f2172]) ).
fof(f2172,plain,
holdsAt(spinning(trolley8),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2170,f1044]) ).
fof(f2173,plain,
( holdsAt(spinning(trolley7),plus(n0,n1))
| ~ happens(pull(agent7,trolley7),n0) ),
inference(resolution,[status(thm)],[f1210,f100]) ).
fof(f2174,plain,
( holdsAt(spinning(trolley7),n1)
| ~ happens(pull(agent7,trolley7),n0) ),
inference(forward_demodulation,[status(thm)],[f141,f2173]) ).
fof(f2175,plain,
( ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2171,f2176]) ).
fof(f2176,plain,
holdsAt(spinning(trolley7),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2174,f1213]) ).
fof(f2178,plain,
( holdsAt(spinning(trolley6),plus(n0,n1))
| ~ happens(pull(agent6,trolley6),n0) ),
inference(resolution,[status(thm)],[f1327,f100]) ).
fof(f2179,plain,
( holdsAt(spinning(trolley6),n1)
| ~ happens(pull(agent6,trolley6),n0) ),
inference(forward_demodulation,[status(thm)],[f141,f2178]) ).
fof(f2180,plain,
( ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2175,f2181]) ).
fof(f2181,plain,
holdsAt(spinning(trolley6),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2179,f1330]) ).
fof(f2182,plain,
( holdsAt(spinning(trolley5),plus(n0,n1))
| ~ happens(pull(agent5,trolley5),n0) ),
inference(resolution,[status(thm)],[f1399,f100]) ).
fof(f2183,plain,
( holdsAt(spinning(trolley5),n1)
| ~ happens(pull(agent5,trolley5),n0) ),
inference(forward_demodulation,[status(thm)],[f141,f2182]) ).
fof(f2184,plain,
( ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2180,f2185]) ).
fof(f2185,plain,
holdsAt(spinning(trolley5),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2183,f1408]) ).
fof(f2186,plain,
( holdsAt(spinning(trolley4),plus(n0,n1))
| ~ happens(pull(agent4,trolley4),n0) ),
inference(resolution,[status(thm)],[f1454,f100]) ).
fof(f2187,plain,
( holdsAt(spinning(trolley4),n1)
| ~ happens(pull(agent4,trolley4),n0) ),
inference(forward_demodulation,[status(thm)],[f141,f2186]) ).
fof(f2188,plain,
( ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2184,f2189]) ).
fof(f2189,plain,
holdsAt(spinning(trolley4),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2187,f1457]) ).
fof(f2190,plain,
( holdsAt(spinning(trolley3),plus(n0,n1))
| ~ happens(pull(agent3,trolley3),n0) ),
inference(resolution,[status(thm)],[f1485,f100]) ).
fof(f2191,plain,
( holdsAt(spinning(trolley3),n1)
| ~ happens(pull(agent3,trolley3),n0) ),
inference(forward_demodulation,[status(thm)],[f141,f2190]) ).
fof(f2192,plain,
( ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2188,f2193]) ).
fof(f2193,plain,
holdsAt(spinning(trolley3),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2191,f1488]) ).
fof(f2196,plain,
( holdsAt(spinning(trolley2),plus(n0,n1))
| ~ happens(pull(agent2,trolley2),n0) ),
inference(resolution,[status(thm)],[f1511,f100]) ).
fof(f2197,plain,
( holdsAt(spinning(trolley2),n1)
| ~ happens(pull(agent2,trolley2),n0) ),
inference(forward_demodulation,[status(thm)],[f141,f2196]) ).
fof(f2198,plain,
~ holdsAt(spinning(trolley1),n1),
inference(backward_subsumption_resolution,[status(thm)],[f2192,f2199]) ).
fof(f2199,plain,
holdsAt(spinning(trolley2),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2197,f1514]) ).
fof(f2200,plain,
( holdsAt(spinning(trolley1),plus(n0,n1))
| ~ happens(pull(agent1,trolley1),n0) ),
inference(resolution,[status(thm)],[f1528,f100]) ).
fof(f2201,plain,
( holdsAt(spinning(trolley1),n1)
| ~ happens(pull(agent1,trolley1),n0) ),
inference(forward_demodulation,[status(thm)],[f141,f2200]) ).
fof(f2203,plain,
holdsAt(spinning(trolley1),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2201,f1522]) ).
fof(f2204,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f2198,f2203]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR024+1.009 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.57 % Computer : n008.cluster.edu
% 0.09/0.57 % Model : x86_64 x86_64
% 0.09/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.57 % Memory : 8046.5625MB
% 0.09/0.57 % OS : Linux 6.8.0-71-generic
% 0.09/0.57 % CPULimit : 300
% 0.09/0.57 % WCLimit : 300
% 0.09/0.57 % DateTime : Mon Sep 21 14:25:11 UTC 2026
% 0.09/0.57 % CPUTime :
% 0.09/0.59 % Drodi V4.1.1
% 0.14/0.78 % Refutation found
% 0.14/0.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.81 % Elapsed time: 0.224356 seconds
% 0.14/0.81 % CPU time: 1.532215 seconds
% 0.14/0.81 % Total memory used: 144.851 MB
% 0.14/0.81 % Net memory used: 143.717 MB
%------------------------------------------------------------------------------