%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR024+1.010 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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.46s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 24
% Syntax : Number of formulae : 355 ( 189 unt; 19 def)
% Number of atoms : 1316 ( 682 equ)
% Maximal formula atoms : 41 ( 3 avg)
% Number of connectives : 1299 ( 338 ~; 534 |; 386 &)
% ( 40 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 1 prp; 0-5 aty)
% Number of functors : 32 ( 32 usr; 22 con; 0-3 aty)
% Number of variables : 368 ( 358 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [Event,Time,Fluent] :
( ( initiates(Event,Fluent,Time)
& happens(Event,Time) )
=> holdsAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [Event,Time] :
( happens(Event,Time)
<=> ( ( Time = n0
& Event = push(agent10,trolley10) )
| ( Time = n0
& Event = pull(agent10,trolley10) )
| ( 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/sandbox/benchmark/theBenchmark.p') ).
fof(f49,conjecture,
( holdsAt(spinning(trolley10),n1)
& 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/sandbox/benchmark/theBenchmark.p') ).
fof(f50,negated_conjecture,
~ ( holdsAt(spinning(trolley10),n1)
& 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)],[f49]) ).
fof(f89,plain,
! [Event,Time,Fluent] :
( holdsAt(Fluent,plus(Time,n1))
| ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f90,plain,
! [Time,Fluent] :
( holdsAt(Fluent,plus(Time,n1))
| ! [Event] :
( ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f89]) ).
fof(f91,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f102,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(f103,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,f102]) ).
fof(f104,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)],[f103]) ).
fof(f105,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)],[f104]) ).
fof(f106,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))],[f105]) ).
fof(f111,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)],[f106]) ).
fof(f132,plain,
plus(n0,n1) = n1,
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f190,definition,
! [Event,Time] :
( sP2_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent10,trolley10) )
| ( 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) ) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f191,plain,
! [Event,Time] :
( happens(Event,Time)
<=> ( ( Time = n0
& Event = push(agent10,trolley10) )
| sP2_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f45,f190]) ).
fof(f192,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent10,trolley10) )
& ~ sP2_prd(Time,Event) )
| happens(Event,Time) )
& ( ( Time = n0
& Event = push(agent10,trolley10) )
| sP2_prd(Time,Event)
| ~ happens(Event,Time) ) ),
inference(NNF_transformation,[status(thm)],[f191]) ).
fof(f193,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent10,trolley10) )
& ~ sP2_prd(Time,Event) )
| happens(Event,Time) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent10,trolley10) )
| sP2_prd(Time,Event)
| ~ happens(Event,Time) ) ),
inference(miniscoping,[status(thm)],[f192]) ).
fof(f196,plain,
! [X0,X1] :
( ~ sP2_prd(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f197,plain,
! [X0,X1] :
( X1 != n0
| X0 != push(agent10,trolley10)
| happens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f319,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ 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)],[f50]) ).
fof(f320,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ 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)],[f319]) ).
fof(f339,definition,
! [Event,Time] :
( sP5_prd(Time,Event)
<=> ( ( 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) ) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f340,plain,
! [Event,Time] :
( sP2_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent10,trolley10) )
| sP5_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f190,f339]) ).
fof(f341,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent10,trolley10) )
& ~ sP5_prd(Time,Event) )
| sP2_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent10,trolley10) )
| sP5_prd(Time,Event)
| ~ sP2_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f340]) ).
fof(f342,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent10,trolley10) )
& ~ sP5_prd(Time,Event) )
| sP2_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent10,trolley10) )
| sP5_prd(Time,Event)
| ~ sP2_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f341]) ).
fof(f345,plain,
! [X0,X1] :
( ~ sP5_prd(X0,X1)
| sP2_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f346,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent10,trolley10)
| sP2_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f362,definition,
! [Event,Time] :
( sP7_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,[sP7_prd])],[]) ).
fof(f363,plain,
! [Event,Time] :
( sP5_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent9,trolley9) )
| sP7_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f339,f362]) ).
fof(f364,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent9,trolley9) )
& ~ sP7_prd(Time,Event) )
| sP5_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent9,trolley9) )
| sP7_prd(Time,Event)
| ~ sP5_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f363]) ).
fof(f365,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent9,trolley9) )
& ~ sP7_prd(Time,Event) )
| sP5_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent9,trolley9) )
| sP7_prd(Time,Event)
| ~ sP5_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f364]) ).
fof(f368,plain,
! [X0,X1] :
( ~ sP7_prd(X0,X1)
| sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f365]) ).
fof(f369,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent9,trolley9)
| sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f365]) ).
fof(f379,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(f380,plain,
! [Event,Time] :
( sP7_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent9,trolley9) )
| sP9_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f362,f379]) ).
fof(f381,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent9,trolley9) )
& ~ sP9_prd(Time,Event) )
| sP7_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent9,trolley9) )
| sP9_prd(Time,Event)
| ~ sP7_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f380]) ).
fof(f382,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent9,trolley9) )
& ~ sP9_prd(Time,Event) )
| sP7_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent9,trolley9) )
| sP9_prd(Time,Event)
| ~ sP7_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f381]) ).
fof(f385,plain,
! [X0,X1] :
( ~ sP9_prd(X0,X1)
| sP7_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f386,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent9,trolley9)
| sP7_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f396,definition,
! [Event,Time] :
( sP11_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,[sP11_prd])],[]) ).
fof(f397,plain,
! [Event,Time] :
( sP9_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent8,trolley8) )
| sP11_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f379,f396]) ).
fof(f398,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent8,trolley8) )
& ~ sP11_prd(Time,Event) )
| sP9_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent8,trolley8) )
| sP11_prd(Time,Event)
| ~ sP9_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f397]) ).
fof(f399,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent8,trolley8) )
& ~ sP11_prd(Time,Event) )
| sP9_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent8,trolley8) )
| sP11_prd(Time,Event)
| ~ sP9_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f398]) ).
fof(f402,plain,
! [X0,X1] :
( ~ sP11_prd(X0,X1)
| sP9_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f399]) ).
fof(f403,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent8,trolley8)
| sP9_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f399]) ).
fof(f410,definition,
! [Event,Time] :
( sP12_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,[sP12_prd])],[]) ).
fof(f411,plain,
! [Event,Time] :
( sP11_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent8,trolley8) )
| sP12_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f396,f410]) ).
fof(f412,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent8,trolley8) )
& ~ sP12_prd(Time,Event) )
| sP11_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent8,trolley8) )
| sP12_prd(Time,Event)
| ~ sP11_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f411]) ).
fof(f413,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent8,trolley8) )
& ~ sP12_prd(Time,Event) )
| sP11_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent8,trolley8) )
| sP12_prd(Time,Event)
| ~ sP11_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f412]) ).
fof(f416,plain,
! [X0,X1] :
( ~ sP12_prd(X0,X1)
| sP11_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f413]) ).
fof(f417,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent8,trolley8)
| sP11_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f413]) ).
fof(f418,definition,
! [Event,Time] :
( sP13_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,[sP13_prd])],[]) ).
fof(f419,plain,
! [Event,Time] :
( sP12_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent7,trolley7) )
| sP13_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f410,f418]) ).
fof(f420,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent7,trolley7) )
& ~ sP13_prd(Time,Event) )
| sP12_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent7,trolley7) )
| sP13_prd(Time,Event)
| ~ sP12_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f419]) ).
fof(f421,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent7,trolley7) )
& ~ sP13_prd(Time,Event) )
| sP12_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent7,trolley7) )
| sP13_prd(Time,Event)
| ~ sP12_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f420]) ).
fof(f424,plain,
! [X0,X1] :
( ~ sP13_prd(X0,X1)
| sP12_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f421]) ).
fof(f425,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent7,trolley7)
| sP12_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f421]) ).
fof(f426,definition,
! [Event,Time] :
( sP14_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,[sP14_prd])],[]) ).
fof(f427,plain,
! [Event,Time] :
( sP13_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent7,trolley7) )
| sP14_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f418,f426]) ).
fof(f428,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent7,trolley7) )
& ~ sP14_prd(Time,Event) )
| sP13_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent7,trolley7) )
| sP14_prd(Time,Event)
| ~ sP13_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f427]) ).
fof(f429,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent7,trolley7) )
& ~ sP14_prd(Time,Event) )
| sP13_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent7,trolley7) )
| sP14_prd(Time,Event)
| ~ sP13_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f428]) ).
fof(f432,plain,
! [X0,X1] :
( ~ sP14_prd(X0,X1)
| sP13_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f429]) ).
fof(f433,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent7,trolley7)
| sP13_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f429]) ).
fof(f434,definition,
! [Event,Time] :
( sP15_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,[sP15_prd])],[]) ).
fof(f435,plain,
! [Event,Time] :
( sP14_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent6,trolley6) )
| sP15_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f426,f434]) ).
fof(f436,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent6,trolley6) )
& ~ sP15_prd(Time,Event) )
| sP14_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent6,trolley6) )
| sP15_prd(Time,Event)
| ~ sP14_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f435]) ).
fof(f437,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent6,trolley6) )
& ~ sP15_prd(Time,Event) )
| sP14_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent6,trolley6) )
| sP15_prd(Time,Event)
| ~ sP14_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f436]) ).
fof(f440,plain,
! [X0,X1] :
( ~ sP15_prd(X0,X1)
| sP14_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f437]) ).
fof(f441,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent6,trolley6)
| sP14_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f437]) ).
fof(f442,definition,
! [Event,Time] :
( sP16_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,[sP16_prd])],[]) ).
fof(f443,plain,
! [Event,Time] :
( sP15_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent6,trolley6) )
| sP16_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f434,f442]) ).
fof(f444,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent6,trolley6) )
& ~ sP16_prd(Time,Event) )
| sP15_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent6,trolley6) )
| sP16_prd(Time,Event)
| ~ sP15_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f443]) ).
fof(f445,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent6,trolley6) )
& ~ sP16_prd(Time,Event) )
| sP15_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent6,trolley6) )
| sP16_prd(Time,Event)
| ~ sP15_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f444]) ).
fof(f448,plain,
! [X0,X1] :
( ~ sP16_prd(X0,X1)
| sP15_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f445]) ).
fof(f449,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent6,trolley6)
| sP15_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f445]) ).
fof(f450,definition,
! [Event,Time] :
( sP17_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,[sP17_prd])],[]) ).
fof(f451,plain,
! [Event,Time] :
( sP16_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent5,trolley5) )
| sP17_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f442,f450]) ).
fof(f452,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent5,trolley5) )
& ~ sP17_prd(Time,Event) )
| sP16_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent5,trolley5) )
| sP17_prd(Time,Event)
| ~ sP16_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f451]) ).
fof(f453,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent5,trolley5) )
& ~ sP17_prd(Time,Event) )
| sP16_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent5,trolley5) )
| sP17_prd(Time,Event)
| ~ sP16_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f452]) ).
fof(f456,plain,
! [X0,X1] :
( ~ sP17_prd(X0,X1)
| sP16_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f453]) ).
fof(f457,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent5,trolley5)
| sP16_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f453]) ).
fof(f458,definition,
! [Event,Time] :
( sP18_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,[sP18_prd])],[]) ).
fof(f459,plain,
! [Event,Time] :
( sP17_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent5,trolley5) )
| sP18_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f450,f458]) ).
fof(f460,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent5,trolley5) )
& ~ sP18_prd(Time,Event) )
| sP17_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent5,trolley5) )
| sP18_prd(Time,Event)
| ~ sP17_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f459]) ).
fof(f461,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent5,trolley5) )
& ~ sP18_prd(Time,Event) )
| sP17_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent5,trolley5) )
| sP18_prd(Time,Event)
| ~ sP17_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f460]) ).
fof(f464,plain,
! [X0,X1] :
( ~ sP18_prd(X0,X1)
| sP17_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f461]) ).
fof(f465,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent5,trolley5)
| sP17_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f461]) ).
fof(f466,definition,
! [Event,Time] :
( sP19_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,[sP19_prd])],[]) ).
fof(f467,plain,
! [Event,Time] :
( sP18_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent4,trolley4) )
| sP19_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f458,f466]) ).
fof(f468,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent4,trolley4) )
& ~ sP19_prd(Time,Event) )
| sP18_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent4,trolley4) )
| sP19_prd(Time,Event)
| ~ sP18_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f467]) ).
fof(f469,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent4,trolley4) )
& ~ sP19_prd(Time,Event) )
| sP18_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent4,trolley4) )
| sP19_prd(Time,Event)
| ~ sP18_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f468]) ).
fof(f472,plain,
! [X0,X1] :
( ~ sP19_prd(X0,X1)
| sP18_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f469]) ).
fof(f473,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent4,trolley4)
| sP18_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f469]) ).
fof(f474,definition,
! [Event,Time] :
( sP20_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,[sP20_prd])],[]) ).
fof(f475,plain,
! [Event,Time] :
( sP19_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent4,trolley4) )
| sP20_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f466,f474]) ).
fof(f476,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent4,trolley4) )
& ~ sP20_prd(Time,Event) )
| sP19_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent4,trolley4) )
| sP20_prd(Time,Event)
| ~ sP19_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f475]) ).
fof(f477,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent4,trolley4) )
& ~ sP20_prd(Time,Event) )
| sP19_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent4,trolley4) )
| sP20_prd(Time,Event)
| ~ sP19_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f476]) ).
fof(f480,plain,
! [X0,X1] :
( ~ sP20_prd(X0,X1)
| sP19_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f477]) ).
fof(f481,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent4,trolley4)
| sP19_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f477]) ).
fof(f482,definition,
! [Event,Time] :
( sP21_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,[sP21_prd])],[]) ).
fof(f483,plain,
! [Event,Time] :
( sP20_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent3,trolley3) )
| sP21_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f474,f482]) ).
fof(f484,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent3,trolley3) )
& ~ sP21_prd(Time,Event) )
| sP20_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent3,trolley3) )
| sP21_prd(Time,Event)
| ~ sP20_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f483]) ).
fof(f485,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent3,trolley3) )
& ~ sP21_prd(Time,Event) )
| sP20_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent3,trolley3) )
| sP21_prd(Time,Event)
| ~ sP20_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f484]) ).
fof(f488,plain,
! [X0,X1] :
( ~ sP21_prd(X0,X1)
| sP20_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f485]) ).
fof(f489,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent3,trolley3)
| sP20_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f485]) ).
fof(f490,definition,
! [Event,Time] :
( sP22_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,[sP22_prd])],[]) ).
fof(f491,plain,
! [Event,Time] :
( sP21_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent3,trolley3) )
| sP22_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f482,f490]) ).
fof(f492,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent3,trolley3) )
& ~ sP22_prd(Time,Event) )
| sP21_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent3,trolley3) )
| sP22_prd(Time,Event)
| ~ sP21_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f491]) ).
fof(f493,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent3,trolley3) )
& ~ sP22_prd(Time,Event) )
| sP21_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent3,trolley3) )
| sP22_prd(Time,Event)
| ~ sP21_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f492]) ).
fof(f496,plain,
! [X0,X1] :
( ~ sP22_prd(X0,X1)
| sP21_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f493]) ).
fof(f497,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent3,trolley3)
| sP21_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f493]) ).
fof(f498,definition,
! [Event,Time] :
( sP23_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,[sP23_prd])],[]) ).
fof(f499,plain,
! [Event,Time] :
( sP22_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent2,trolley2) )
| sP23_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f490,f498]) ).
fof(f500,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent2,trolley2) )
& ~ sP23_prd(Time,Event) )
| sP22_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent2,trolley2) )
| sP23_prd(Time,Event)
| ~ sP22_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f499]) ).
fof(f501,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent2,trolley2) )
& ~ sP23_prd(Time,Event) )
| sP22_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent2,trolley2) )
| sP23_prd(Time,Event)
| ~ sP22_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f500]) ).
fof(f504,plain,
! [X0,X1] :
( ~ sP23_prd(X0,X1)
| sP22_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f501]) ).
fof(f505,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent2,trolley2)
| sP22_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f501]) ).
fof(f506,definition,
! [Event,Time] :
( sP24_prd(Time,Event)
<=> ( ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP24_prd])],[]) ).
fof(f507,plain,
! [Event,Time] :
( sP23_prd(Time,Event)
<=> ( ( Time = n0
& Event = pull(agent2,trolley2) )
| sP24_prd(Time,Event) ) ),
inference(formula_renaming,[status(thm)],[f498,f506]) ).
fof(f508,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != pull(agent2,trolley2) )
& ~ sP24_prd(Time,Event) )
| sP23_prd(Time,Event) )
& ( ( Time = n0
& Event = pull(agent2,trolley2) )
| sP24_prd(Time,Event)
| ~ sP23_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f507]) ).
fof(f509,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != pull(agent2,trolley2) )
& ~ sP24_prd(Time,Event) )
| sP23_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = pull(agent2,trolley2) )
| sP24_prd(Time,Event)
| ~ sP23_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f508]) ).
fof(f512,plain,
! [X0,X1] :
( ~ sP24_prd(X0,X1)
| sP23_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f509]) ).
fof(f513,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent2,trolley2)
| sP23_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f509]) ).
fof(f514,plain,
! [Event,Time] :
( ( ( ( Time != n0
| Event != push(agent1,trolley1) )
& ( Time != n0
| Event != pull(agent1,trolley1) ) )
| sP24_prd(Time,Event) )
& ( ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) )
| ~ sP24_prd(Time,Event) ) ),
inference(NNF_transformation,[status(thm)],[f506]) ).
fof(f515,plain,
( ! [Event,Time] :
( ( ( Time != n0
| Event != push(agent1,trolley1) )
& ( Time != n0
| Event != pull(agent1,trolley1) ) )
| sP24_prd(Time,Event) )
& ! [Event,Time] :
( ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) )
| ~ sP24_prd(Time,Event) ) ),
inference(miniscoping,[status(thm)],[f514]) ).
fof(f520,plain,
! [X0,X1] :
( X0 != n0
| X1 != pull(agent1,trolley1)
| sP24_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f515]) ).
fof(f521,plain,
! [X0,X1] :
( X0 != n0
| X1 != push(agent1,trolley1)
| sP24_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f515]) ).
fof(f522,plain,
! [X0,X1,X2] :
( ~ happens(push(X0,X1),X2)
| initiates(pull(X0,X1),spinning(X1),X2) ),
inference(destructive_equality_resolution,[status(thm)],[f111]) ).
fof(f526,plain,
happens(push(agent10,trolley10),n0),
inference(destructive_equality_resolution,[status(thm)],[f197]) ).
fof(f529,plain,
sP2_prd(n0,pull(agent10,trolley10)),
inference(destructive_equality_resolution,[status(thm)],[f346]) ).
fof(f532,plain,
sP5_prd(n0,push(agent9,trolley9)),
inference(destructive_equality_resolution,[status(thm)],[f369]) ).
fof(f534,plain,
sP7_prd(n0,pull(agent9,trolley9)),
inference(destructive_equality_resolution,[status(thm)],[f386]) ).
fof(f536,plain,
sP9_prd(n0,push(agent8,trolley8)),
inference(destructive_equality_resolution,[status(thm)],[f403]) ).
fof(f538,plain,
sP11_prd(n0,pull(agent8,trolley8)),
inference(destructive_equality_resolution,[status(thm)],[f417]) ).
fof(f539,plain,
sP12_prd(n0,push(agent7,trolley7)),
inference(destructive_equality_resolution,[status(thm)],[f425]) ).
fof(f540,plain,
sP13_prd(n0,pull(agent7,trolley7)),
inference(destructive_equality_resolution,[status(thm)],[f433]) ).
fof(f541,plain,
sP14_prd(n0,push(agent6,trolley6)),
inference(destructive_equality_resolution,[status(thm)],[f441]) ).
fof(f542,plain,
sP15_prd(n0,pull(agent6,trolley6)),
inference(destructive_equality_resolution,[status(thm)],[f449]) ).
fof(f543,plain,
sP16_prd(n0,push(agent5,trolley5)),
inference(destructive_equality_resolution,[status(thm)],[f457]) ).
fof(f544,plain,
sP17_prd(n0,pull(agent5,trolley5)),
inference(destructive_equality_resolution,[status(thm)],[f465]) ).
fof(f545,plain,
sP18_prd(n0,push(agent4,trolley4)),
inference(destructive_equality_resolution,[status(thm)],[f473]) ).
fof(f546,plain,
sP19_prd(n0,pull(agent4,trolley4)),
inference(destructive_equality_resolution,[status(thm)],[f481]) ).
fof(f547,plain,
sP20_prd(n0,push(agent3,trolley3)),
inference(destructive_equality_resolution,[status(thm)],[f489]) ).
fof(f548,plain,
sP21_prd(n0,pull(agent3,trolley3)),
inference(destructive_equality_resolution,[status(thm)],[f497]) ).
fof(f549,plain,
sP22_prd(n0,push(agent2,trolley2)),
inference(destructive_equality_resolution,[status(thm)],[f505]) ).
fof(f550,plain,
sP23_prd(n0,pull(agent2,trolley2)),
inference(destructive_equality_resolution,[status(thm)],[f513]) ).
fof(f552,plain,
sP24_prd(n0,pull(agent1,trolley1)),
inference(destructive_equality_resolution,[status(thm)],[f520]) ).
fof(f553,plain,
sP24_prd(n0,push(agent1,trolley1)),
inference(destructive_equality_resolution,[status(thm)],[f521]) ).
fof(f578,plain,
! [X0,X1] :
( holdsAt(X1,n1)
| ~ initiates(X0,X1,n0)
| ~ happens(X0,n0) ),
inference(paramodulation,[status(thm)],[f132,f91]) ).
fof(f626,plain,
! [X0,X1] :
( sP22_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f512,f504]) ).
fof(f627,plain,
! [X0,X1] :
( sP21_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f626,f496]) ).
fof(f628,plain,
! [X0,X1] :
( sP20_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f627,f488]) ).
fof(f629,plain,
! [X0,X1] :
( sP19_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f628,f480]) ).
fof(f630,plain,
! [X0,X1] :
( sP18_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f629,f472]) ).
fof(f631,plain,
! [X0,X1] :
( sP17_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f630,f464]) ).
fof(f632,plain,
! [X0,X1] :
( sP16_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f631,f456]) ).
fof(f633,plain,
! [X0,X1] :
( sP15_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f632,f448]) ).
fof(f634,plain,
! [X0,X1] :
( sP14_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f633,f440]) ).
fof(f635,plain,
! [X0,X1] :
( sP13_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f634,f432]) ).
fof(f636,plain,
! [X0,X1] :
( sP12_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f635,f424]) ).
fof(f637,plain,
! [X0,X1] :
( sP11_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f636,f416]) ).
fof(f638,plain,
! [X0,X1] :
( sP9_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f637,f402]) ).
fof(f639,plain,
! [X0,X1] :
( sP7_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f638,f385]) ).
fof(f640,plain,
! [X0,X1] :
( sP5_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f639,f368]) ).
fof(f641,plain,
! [X0,X1] :
( sP2_prd(X0,X1)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f640,f345]) ).
fof(f642,plain,
! [X0,X1] :
( happens(X1,X0)
| ~ sP24_prd(X0,X1) ),
inference(resolution,[status(thm)],[f641,f196]) ).
fof(f715,plain,
happens(pull(agent10,trolley10),n0),
inference(resolution,[status(thm)],[f529,f196]) ).
fof(f716,plain,
sP2_prd(n0,push(agent9,trolley9)),
inference(resolution,[status(thm)],[f532,f345]) ).
fof(f717,plain,
sP5_prd(n0,pull(agent9,trolley9)),
inference(resolution,[status(thm)],[f534,f368]) ).
fof(f722,plain,
sP7_prd(n0,push(agent8,trolley8)),
inference(resolution,[status(thm)],[f536,f385]) ).
fof(f723,plain,
sP9_prd(n0,pull(agent8,trolley8)),
inference(resolution,[status(thm)],[f538,f402]) ).
fof(f724,plain,
sP11_prd(n0,push(agent7,trolley7)),
inference(resolution,[status(thm)],[f539,f416]) ).
fof(f725,plain,
sP12_prd(n0,pull(agent7,trolley7)),
inference(resolution,[status(thm)],[f540,f424]) ).
fof(f726,plain,
sP13_prd(n0,push(agent6,trolley6)),
inference(resolution,[status(thm)],[f541,f432]) ).
fof(f727,plain,
sP14_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f542,f440]) ).
fof(f728,plain,
sP15_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f543,f448]) ).
fof(f729,plain,
sP16_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f544,f456]) ).
fof(f730,plain,
sP17_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f545,f464]) ).
fof(f734,plain,
sP18_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f546,f472]) ).
fof(f735,plain,
sP19_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f547,f480]) ).
fof(f736,plain,
sP20_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f548,f488]) ).
fof(f737,plain,
sP21_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f549,f496]) ).
fof(f738,plain,
sP22_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f550,f504]) ).
fof(f739,plain,
happens(pull(agent1,trolley1),n0),
inference(resolution,[status(thm)],[f552,f642]) ).
fof(f741,plain,
happens(push(agent1,trolley1),n0),
inference(resolution,[status(thm)],[f553,f642]) ).
fof(f837,plain,
happens(push(agent9,trolley9),n0),
inference(resolution,[status(thm)],[f716,f196]) ).
fof(f838,plain,
sP2_prd(n0,pull(agent9,trolley9)),
inference(resolution,[status(thm)],[f717,f345]) ).
fof(f839,plain,
sP5_prd(n0,push(agent8,trolley8)),
inference(resolution,[status(thm)],[f722,f368]) ).
fof(f840,plain,
sP7_prd(n0,pull(agent8,trolley8)),
inference(resolution,[status(thm)],[f723,f385]) ).
fof(f844,plain,
sP9_prd(n0,push(agent7,trolley7)),
inference(resolution,[status(thm)],[f724,f402]) ).
fof(f845,plain,
sP11_prd(n0,pull(agent7,trolley7)),
inference(resolution,[status(thm)],[f725,f416]) ).
fof(f846,plain,
sP12_prd(n0,push(agent6,trolley6)),
inference(resolution,[status(thm)],[f726,f424]) ).
fof(f847,plain,
sP13_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f727,f432]) ).
fof(f848,plain,
sP14_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f728,f440]) ).
fof(f849,plain,
sP15_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f729,f448]) ).
fof(f854,plain,
sP16_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f730,f456]) ).
fof(f855,plain,
sP17_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f734,f464]) ).
fof(f856,plain,
sP18_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f735,f472]) ).
fof(f857,plain,
sP19_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f736,f480]) ).
fof(f858,plain,
sP20_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f737,f488]) ).
fof(f859,plain,
sP21_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f738,f496]) ).
fof(f1030,plain,
happens(pull(agent9,trolley9),n0),
inference(resolution,[status(thm)],[f838,f196]) ).
fof(f1031,plain,
sP2_prd(n0,push(agent8,trolley8)),
inference(resolution,[status(thm)],[f839,f345]) ).
fof(f1032,plain,
sP5_prd(n0,pull(agent8,trolley8)),
inference(resolution,[status(thm)],[f840,f368]) ).
fof(f1036,plain,
sP7_prd(n0,push(agent7,trolley7)),
inference(resolution,[status(thm)],[f844,f385]) ).
fof(f1037,plain,
sP9_prd(n0,pull(agent7,trolley7)),
inference(resolution,[status(thm)],[f845,f402]) ).
fof(f1038,plain,
sP11_prd(n0,push(agent6,trolley6)),
inference(resolution,[status(thm)],[f846,f416]) ).
fof(f1039,plain,
sP12_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f847,f424]) ).
fof(f1040,plain,
sP13_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f848,f432]) ).
fof(f1041,plain,
sP14_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f849,f440]) ).
fof(f1048,plain,
sP15_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f854,f448]) ).
fof(f1049,plain,
sP16_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f855,f456]) ).
fof(f1050,plain,
sP17_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f856,f464]) ).
fof(f1051,plain,
sP18_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f857,f472]) ).
fof(f1052,plain,
sP19_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f858,f480]) ).
fof(f1053,plain,
sP20_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f859,f488]) ).
fof(f1054,plain,
happens(push(agent8,trolley8),n0),
inference(resolution,[status(thm)],[f1031,f196]) ).
fof(f1055,plain,
sP2_prd(n0,pull(agent8,trolley8)),
inference(resolution,[status(thm)],[f1032,f345]) ).
fof(f1064,plain,
sP5_prd(n0,push(agent7,trolley7)),
inference(resolution,[status(thm)],[f1036,f368]) ).
fof(f1065,plain,
sP7_prd(n0,pull(agent7,trolley7)),
inference(resolution,[status(thm)],[f1037,f385]) ).
fof(f1066,plain,
sP9_prd(n0,push(agent6,trolley6)),
inference(resolution,[status(thm)],[f1038,f402]) ).
fof(f1070,plain,
sP11_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f1039,f416]) ).
fof(f1071,plain,
sP12_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f1040,f424]) ).
fof(f1072,plain,
sP13_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f1041,f432]) ).
fof(f1073,plain,
sP14_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1048,f440]) ).
fof(f1074,plain,
sP15_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1049,f448]) ).
fof(f1075,plain,
sP16_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1050,f456]) ).
fof(f1080,plain,
sP17_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1051,f464]) ).
fof(f1081,plain,
sP18_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1052,f472]) ).
fof(f1082,plain,
sP19_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1053,f480]) ).
fof(f1083,plain,
happens(pull(agent8,trolley8),n0),
inference(resolution,[status(thm)],[f1055,f196]) ).
fof(f1084,plain,
sP2_prd(n0,push(agent7,trolley7)),
inference(resolution,[status(thm)],[f1064,f345]) ).
fof(f1085,plain,
sP5_prd(n0,pull(agent7,trolley7)),
inference(resolution,[status(thm)],[f1065,f368]) ).
fof(f1086,plain,
sP7_prd(n0,push(agent6,trolley6)),
inference(resolution,[status(thm)],[f1066,f385]) ).
fof(f1087,plain,
sP9_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f1070,f402]) ).
fof(f1093,plain,
sP11_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f1071,f416]) ).
fof(f1094,plain,
sP12_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f1072,f424]) ).
fof(f1095,plain,
sP13_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1073,f432]) ).
fof(f1099,plain,
sP14_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1074,f440]) ).
fof(f1100,plain,
sP15_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1075,f448]) ).
fof(f1101,plain,
sP16_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1080,f456]) ).
fof(f1102,plain,
sP17_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1081,f464]) ).
fof(f1103,plain,
sP18_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1082,f472]) ).
fof(f1108,plain,
happens(push(agent7,trolley7),n0),
inference(resolution,[status(thm)],[f1084,f196]) ).
fof(f1109,plain,
sP2_prd(n0,pull(agent7,trolley7)),
inference(resolution,[status(thm)],[f1085,f345]) ).
fof(f1110,plain,
sP5_prd(n0,push(agent6,trolley6)),
inference(resolution,[status(thm)],[f1086,f368]) ).
fof(f1111,plain,
sP7_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f1087,f385]) ).
fof(f1112,plain,
sP9_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f1093,f402]) ).
fof(f1113,plain,
sP11_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f1094,f416]) ).
fof(f1114,plain,
sP12_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1095,f424]) ).
fof(f1115,plain,
sP13_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1099,f432]) ).
fof(f1116,plain,
sP14_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1100,f440]) ).
fof(f1122,plain,
sP15_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1101,f448]) ).
fof(f1123,plain,
sP16_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1102,f456]) ).
fof(f1124,plain,
sP17_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1103,f464]) ).
fof(f1128,plain,
happens(pull(agent7,trolley7),n0),
inference(resolution,[status(thm)],[f1109,f196]) ).
fof(f1129,plain,
sP2_prd(n0,push(agent6,trolley6)),
inference(resolution,[status(thm)],[f1110,f345]) ).
fof(f1130,plain,
sP5_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f1111,f368]) ).
fof(f1131,plain,
sP7_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f1112,f385]) ).
fof(f1132,plain,
sP9_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f1113,f402]) ).
fof(f1137,plain,
sP11_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1114,f416]) ).
fof(f1138,plain,
sP12_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1115,f424]) ).
fof(f1139,plain,
sP13_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1116,f432]) ).
fof(f1140,plain,
sP14_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1122,f440]) ).
fof(f1141,plain,
sP15_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1123,f448]) ).
fof(f1142,plain,
sP16_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1124,f456]) ).
fof(f1143,plain,
happens(push(agent6,trolley6),n0),
inference(resolution,[status(thm)],[f1129,f196]) ).
fof(f1144,plain,
sP2_prd(n0,pull(agent6,trolley6)),
inference(resolution,[status(thm)],[f1130,f345]) ).
fof(f1150,plain,
sP5_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f1131,f368]) ).
fof(f1151,plain,
sP7_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f1132,f385]) ).
fof(f1152,plain,
sP9_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1137,f402]) ).
fof(f1156,plain,
sP11_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1138,f416]) ).
fof(f1157,plain,
sP12_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1139,f424]) ).
fof(f1158,plain,
sP13_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1140,f432]) ).
fof(f1159,plain,
sP14_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1141,f440]) ).
fof(f1160,plain,
sP15_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1142,f448]) ).
fof(f1165,plain,
happens(pull(agent6,trolley6),n0),
inference(resolution,[status(thm)],[f1144,f196]) ).
fof(f1166,plain,
sP2_prd(n0,push(agent5,trolley5)),
inference(resolution,[status(thm)],[f1150,f345]) ).
fof(f1167,plain,
sP5_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f1151,f368]) ).
fof(f1168,plain,
sP7_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1152,f385]) ).
fof(f1169,plain,
sP9_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1156,f402]) ).
fof(f1170,plain,
sP11_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1157,f416]) ).
fof(f1171,plain,
sP12_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1158,f424]) ).
fof(f1172,plain,
sP13_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1159,f432]) ).
fof(f1173,plain,
sP14_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1160,f440]) ).
fof(f1353,plain,
happens(push(agent5,trolley5),n0),
inference(resolution,[status(thm)],[f1166,f196]) ).
fof(f1355,plain,
sP2_prd(n0,pull(agent5,trolley5)),
inference(resolution,[status(thm)],[f1167,f345]) ).
fof(f1357,plain,
sP5_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1168,f368]) ).
fof(f1359,plain,
sP7_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1169,f385]) ).
fof(f1361,plain,
sP9_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1170,f402]) ).
fof(f1363,plain,
sP11_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1171,f416]) ).
fof(f1365,plain,
sP12_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1172,f424]) ).
fof(f1367,plain,
sP13_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1173,f432]) ).
fof(f1370,plain,
happens(pull(agent5,trolley5),n0),
inference(resolution,[status(thm)],[f1355,f196]) ).
fof(f1372,plain,
sP2_prd(n0,push(agent4,trolley4)),
inference(resolution,[status(thm)],[f1357,f345]) ).
fof(f1374,plain,
sP5_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1359,f368]) ).
fof(f1376,plain,
sP7_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1361,f385]) ).
fof(f1378,plain,
sP9_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1363,f402]) ).
fof(f1380,plain,
sP11_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1365,f416]) ).
fof(f1382,plain,
sP12_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1367,f424]) ).
fof(f1385,plain,
happens(push(agent4,trolley4),n0),
inference(resolution,[status(thm)],[f1372,f196]) ).
fof(f1386,plain,
! [X0,X1] :
( ~ happens(push(X0,X1),n0)
| holdsAt(spinning(X1),n1)
| ~ happens(pull(X0,X1),n0) ),
inference(resolution,[status(thm)],[f578,f522]) ).
fof(f1392,plain,
sP2_prd(n0,pull(agent4,trolley4)),
inference(resolution,[status(thm)],[f1374,f345]) ).
fof(f1394,plain,
sP5_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1376,f368]) ).
fof(f1396,plain,
sP7_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1378,f385]) ).
fof(f1399,plain,
sP9_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1380,f402]) ).
fof(f1401,plain,
sP11_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1382,f416]) ).
fof(f1404,plain,
happens(pull(agent4,trolley4),n0),
inference(resolution,[status(thm)],[f1392,f196]) ).
fof(f1406,plain,
sP2_prd(n0,push(agent3,trolley3)),
inference(resolution,[status(thm)],[f1394,f345]) ).
fof(f1408,plain,
sP5_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1396,f368]) ).
fof(f1410,plain,
sP7_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1399,f385]) ).
fof(f1412,plain,
sP9_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1401,f402]) ).
fof(f1415,plain,
happens(push(agent3,trolley3),n0),
inference(resolution,[status(thm)],[f1406,f196]) ).
fof(f1417,plain,
sP2_prd(n0,pull(agent3,trolley3)),
inference(resolution,[status(thm)],[f1408,f345]) ).
fof(f1419,plain,
sP5_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1410,f368]) ).
fof(f1421,plain,
sP7_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1412,f385]) ).
fof(f1424,plain,
happens(pull(agent3,trolley3),n0),
inference(resolution,[status(thm)],[f1417,f196]) ).
fof(f1426,plain,
sP2_prd(n0,push(agent2,trolley2)),
inference(resolution,[status(thm)],[f1419,f345]) ).
fof(f1428,plain,
sP5_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1421,f368]) ).
fof(f1431,plain,
happens(push(agent2,trolley2),n0),
inference(resolution,[status(thm)],[f1426,f196]) ).
fof(f1433,plain,
sP2_prd(n0,pull(agent2,trolley2)),
inference(resolution,[status(thm)],[f1428,f345]) ).
fof(f1436,plain,
happens(pull(agent2,trolley2),n0),
inference(resolution,[status(thm)],[f1433,f196]) ).
fof(f2570,plain,
( ~ happens(push(agent2,trolley2),n0)
| holdsAt(spinning(trolley2),n1) ),
inference(resolution,[status(thm)],[f1386,f1436]) ).
fof(f2571,plain,
( ~ happens(push(agent3,trolley3),n0)
| holdsAt(spinning(trolley3),n1) ),
inference(resolution,[status(thm)],[f1386,f1424]) ).
fof(f2572,plain,
( ~ happens(push(agent4,trolley4),n0)
| holdsAt(spinning(trolley4),n1) ),
inference(resolution,[status(thm)],[f1386,f1404]) ).
fof(f2573,plain,
( ~ happens(push(agent5,trolley5),n0)
| holdsAt(spinning(trolley5),n1) ),
inference(resolution,[status(thm)],[f1386,f1370]) ).
fof(f2574,plain,
( ~ happens(push(agent6,trolley6),n0)
| holdsAt(spinning(trolley6),n1) ),
inference(resolution,[status(thm)],[f1386,f1165]) ).
fof(f2575,plain,
( ~ happens(push(agent7,trolley7),n0)
| holdsAt(spinning(trolley7),n1) ),
inference(resolution,[status(thm)],[f1386,f1128]) ).
fof(f2576,plain,
( ~ happens(push(agent8,trolley8),n0)
| holdsAt(spinning(trolley8),n1) ),
inference(resolution,[status(thm)],[f1386,f1083]) ).
fof(f2577,plain,
( ~ happens(push(agent9,trolley9),n0)
| holdsAt(spinning(trolley9),n1) ),
inference(resolution,[status(thm)],[f1386,f1030]) ).
fof(f2578,plain,
( ~ happens(push(agent1,trolley1),n0)
| holdsAt(spinning(trolley1),n1) ),
inference(resolution,[status(thm)],[f1386,f739]) ).
fof(f2579,plain,
( ~ happens(push(agent10,trolley10),n0)
| holdsAt(spinning(trolley10),n1) ),
inference(resolution,[status(thm)],[f1386,f715]) ).
fof(f2580,plain,
holdsAt(spinning(trolley2),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2570,f1431]) ).
fof(f2581,plain,
holdsAt(spinning(trolley3),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2571,f1415]) ).
fof(f2582,plain,
holdsAt(spinning(trolley4),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2572,f1385]) ).
fof(f2583,plain,
holdsAt(spinning(trolley5),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2573,f1353]) ).
fof(f2584,plain,
holdsAt(spinning(trolley6),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2574,f1143]) ).
fof(f2585,plain,
holdsAt(spinning(trolley7),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2575,f1108]) ).
fof(f2586,plain,
holdsAt(spinning(trolley8),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2576,f1054]) ).
fof(f2587,plain,
holdsAt(spinning(trolley9),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2577,f837]) ).
fof(f2588,plain,
holdsAt(spinning(trolley1),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2578,f741]) ).
fof(f2589,plain,
holdsAt(spinning(trolley10),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2579,f526]) ).
fof(f2590,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ 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(trolley1),n1) ),
inference(backward_subsumption_resolution,[status(thm)],[f320,f2580]) ).
fof(f2591,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ 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(trolley1),n1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2590,f2581]) ).
fof(f2592,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2591,f2582]) ).
fof(f2593,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2592,f2583]) ).
fof(f2594,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2593,f2584]) ).
fof(f2595,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2594,f2585]) ).
fof(f2628,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1) ),
inference(forward_subsumption_resolution,[status(thm)],[f2595,f2588]) ).
fof(f2629,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ holdsAt(spinning(trolley8),n1) ),
inference(resolution,[status(thm)],[f2628,f2587]) ).
fof(f2631,plain,
~ holdsAt(spinning(trolley10),n1),
inference(forward_subsumption_resolution,[status(thm)],[f2629,f2586]) ).
fof(f2633,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2631,f2589]) ).
%------------------------------------------------------------------------------
%----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 -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n011.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:26 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 0.14/0.46 % Refutation found
% 0.14/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.50 % Elapsed time: 0.120474 seconds
% 0.14/0.50 % CPU time: 0.604148 seconds
% 0.14/0.50 % Total memory used: 125.835 MB
% 0.14/0.50 % Net memory used: 125.207 MB
%------------------------------------------------------------------------------