%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : CSR024+1.010 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n005.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 : Fri Sep 25 01:09:55 PM UTC 2026
% Result : Theorem 2.81s 1.75s
% Output : CNFRefutation 2.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 35
% Syntax : Number of formulae : 361 ( 101 unt; 30 def)
% Number of atoms : 1222 ( 426 equ)
% Maximal formula atoms : 48 ( 3 avg)
% Number of connectives : 1274 ( 505 ~; 534 |; 210 &)
% ( 24 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 35 ( 33 usr; 11 prp; 0-5 aty)
% Number of functors : 30 ( 30 usr; 22 con; 0-3 aty)
% Number of variables : 493 ( 0 sgn 485 !; 8 ?; 200 :)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [X0,X1,X2] :
( ( initiates(X0,X2,X1)
& happens(X0,X1) )
=> holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_holds) ).
fof(f13,axiom,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ? [X3,X4] :
( ( happens(push(X3,X4),X2)
& X1 = spinning(X4)
& X0 = pull(X3,X4) )
| ( ~ happens(push(X3,X4),X2)
& X1 = backwards(X4)
& X0 = pull(X3,X4) )
| ( ~ happens(pull(X3,X4),X2)
& X1 = forwards(X4)
& X0 = push(X3,X4) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+3.ax',initiates_all_defn) ).
fof(f23,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_1) ).
fof(f45,axiom,
! [X0,X1] :
( happens(X0,X1)
<=> ( ( X1 = n0
& X0 = push(agent10,trolley10) )
| ( X1 = n0
& X0 = pull(agent10,trolley10) )
| ( X1 = n0
& X0 = push(agent9,trolley9) )
| ( X1 = n0
& X0 = pull(agent9,trolley9) )
| ( X1 = n0
& X0 = push(agent8,trolley8) )
| ( X1 = n0
& X0 = pull(agent8,trolley8) )
| ( X1 = n0
& X0 = push(agent7,trolley7) )
| ( X1 = n0
& X0 = pull(agent7,trolley7) )
| ( X1 = n0
& X0 = push(agent6,trolley6) )
| ( X1 = n0
& X0 = pull(agent6,trolley6) )
| ( X1 = n0
& X0 = push(agent5,trolley5) )
| ( X1 = n0
& X0 = pull(agent5,trolley5) )
| ( X1 = n0
& X0 = push(agent4,trolley4) )
| ( X1 = n0
& X0 = pull(agent4,trolley4) )
| ( X1 = n0
& X0 = push(agent3,trolley3) )
| ( X1 = n0
& X0 = pull(agent3,trolley3) )
| ( X1 = n0
& X0 = push(agent2,trolley2) )
| ( X1 = n0
& X0 = pull(agent2,trolley2) )
| ( X1 = n0
& X0 = push(agent1,trolley1) )
| ( X1 = n0
& X0 = pull(agent1,trolley1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_all_defn) ).
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',spinning_3) ).
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(f65,plain,
! [X0,X1,X2] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(ennf_transformation,[],[f9]) ).
fof(f66,plain,
! [X0,X1,X2] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(flattening,[],[f65]) ).
fof(f78,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(ennf_transformation,[],[f50]) ).
fof(f118,plain,
! [X0,X1,X2] :
( ( ~ initiates(X0,X1,X2)
| ? [X3,X4] :
( sP0(X0,X4,X3,X1,X2)
| sP1(X0,X4,X3,X1,X2)
| ( ~ happens(pull(X3,X4),X2)
& X1 = forwards(X4)
& X0 = push(X3,X4) ) ) )
& ( ! [X3,X4] :
( ~ sP0(X0,X4,X3,X1,X2)
& ~ sP1(X0,X4,X3,X1,X2)
& ( happens(pull(X3,X4),X2)
| forwards(X4) != X1
| push(X3,X4) != X0 ) )
| initiates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f81]) ).
fof(f119,plain,
! [X0,X1,X2] :
( ( ~ initiates(X0,X1,X2)
| ? [X5,X6] :
( sP0(X0,X6,X5,X1,X2)
| sP1(X0,X6,X5,X1,X2)
| ( ~ happens(pull(X5,X6),X2)
& forwards(X6) = X1
& push(X5,X6) = X0 ) ) )
& ( ! [X3,X4] :
( ~ sP0(X0,X4,X3,X1,X2)
& ~ sP1(X0,X4,X3,X1,X2)
& ( happens(pull(X3,X4),X2)
| forwards(X4) != X1
| push(X3,X4) != X0 ) )
| initiates(X0,X1,X2) ) ),
inference(rectify,[],[f118]) ).
fof(f120,plain,
! [X0,X1,X2] :
( ( ~ initiates(X0,X1,X2)
| sP0(X0,sK31(X0,X1,X2),sK30(X0,X1,X2),X1,X2)
| sP1(X0,sK31(X0,X1,X2),sK30(X0,X1,X2),X1,X2)
| ( ~ happens(pull(sK30(X0,X1,X2),sK31(X0,X1,X2)),X2)
& forwards(sK31(X0,X1,X2)) = X1
& push(sK30(X0,X1,X2),sK31(X0,X1,X2)) = X0 ) )
& ( ! [X3,X4] :
( ~ sP0(X0,X4,X3,X1,X2)
& ~ sP1(X0,X4,X3,X1,X2)
& ( happens(pull(X3,X4),X2)
| forwards(X4) != X1
| push(X3,X4) != X0 ) )
| initiates(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30,sK31]),skolemize(X5,sK30(X0,X1,X2)),skolemize(X6,sK31(X0,X1,X2))],[f119]) ).
fof(f153,plain,
! [X0,X1] :
( ( ~ sP25(X0,X1)
| sP8(X0,X1)
| sP9(X0,X1)
| sP10(X0,X1)
| sP11(X0,X1)
| sP12(X0,X1)
| sP13(X0,X1)
| sP14(X0,X1)
| sP15(X0,X1)
| sP16(X0,X1)
| sP17(X0,X1)
| sP18(X0,X1)
| sP19(X0,X1)
| sP20(X0,X1)
| sP21(X0,X1)
| sP22(X0,X1)
| sP23(X0,X1)
| sP24(X0,X1)
| ( X1 = n0
& X0 = pull(agent2,trolley2) )
| ( X1 = n0
& X0 = push(agent1,trolley1) )
| ( X1 = n0
& X0 = pull(agent1,trolley1) ) )
& ( ( ~ sP8(X0,X1)
& ~ sP9(X0,X1)
& ~ sP10(X0,X1)
& ~ sP11(X0,X1)
& ~ sP12(X0,X1)
& ~ sP13(X0,X1)
& ~ sP14(X0,X1)
& ~ sP15(X0,X1)
& ~ sP16(X0,X1)
& ~ sP17(X0,X1)
& ~ sP18(X0,X1)
& ~ sP19(X0,X1)
& ~ sP20(X0,X1)
& ~ sP21(X0,X1)
& ~ sP22(X0,X1)
& ~ sP23(X0,X1)
& ~ sP24(X0,X1)
& ( n0 != X1
| pull(agent2,trolley2) != X0 )
& ( n0 != X1
| push(agent1,trolley1) != X0 )
& ( n0 != X1
| pull(agent1,trolley1) != X0 ) )
| sP25(X0,X1) ) ),
inference(nnf_transformation,[],[f106]) ).
fof(f154,plain,
! [X0,X1] :
( ( ~ sP25(X0,X1)
| sP8(X0,X1)
| sP9(X0,X1)
| sP10(X0,X1)
| sP11(X0,X1)
| sP12(X0,X1)
| sP13(X0,X1)
| sP14(X0,X1)
| sP15(X0,X1)
| sP16(X0,X1)
| sP17(X0,X1)
| sP18(X0,X1)
| sP19(X0,X1)
| sP20(X0,X1)
| sP21(X0,X1)
| sP22(X0,X1)
| sP23(X0,X1)
| sP24(X0,X1)
| ( X1 = n0
& X0 = pull(agent2,trolley2) )
| ( X1 = n0
& X0 = push(agent1,trolley1) )
| ( X1 = n0
& X0 = pull(agent1,trolley1) ) )
& ( ( ~ sP8(X0,X1)
& ~ sP9(X0,X1)
& ~ sP10(X0,X1)
& ~ sP11(X0,X1)
& ~ sP12(X0,X1)
& ~ sP13(X0,X1)
& ~ sP14(X0,X1)
& ~ sP15(X0,X1)
& ~ sP16(X0,X1)
& ~ sP17(X0,X1)
& ~ sP18(X0,X1)
& ~ sP19(X0,X1)
& ~ sP20(X0,X1)
& ~ sP21(X0,X1)
& ~ sP22(X0,X1)
& ~ sP23(X0,X1)
& ~ sP24(X0,X1)
& ( n0 != X1
| pull(agent2,trolley2) != X0 )
& ( n0 != X1
| push(agent1,trolley1) != X0 )
& ( n0 != X1
| pull(agent1,trolley1) != X0 ) )
| sP25(X0,X1) ) ),
inference(flattening,[],[f153]) ).
fof(f155,plain,
! [X0,X1] :
( ( ~ sP24(X0,X1)
| ( X1 = n0
& X0 = push(agent2,trolley2) ) )
& ( n0 != X1
| push(agent2,trolley2) != X0
| sP24(X0,X1) ) ),
inference(nnf_transformation,[],[f105]) ).
fof(f156,plain,
! [X0,X1] :
( ( ~ sP24(X0,X1)
| ( X1 = n0
& X0 = push(agent2,trolley2) ) )
& ( n0 != X1
| push(agent2,trolley2) != X0
| sP24(X0,X1) ) ),
inference(flattening,[],[f155]) ).
fof(f157,plain,
! [X0,X1] :
( ( ~ sP23(X0,X1)
| ( X1 = n0
& X0 = pull(agent3,trolley3) ) )
& ( n0 != X1
| pull(agent3,trolley3) != X0
| sP23(X0,X1) ) ),
inference(nnf_transformation,[],[f104]) ).
fof(f158,plain,
! [X0,X1] :
( ( ~ sP23(X0,X1)
| ( X1 = n0
& X0 = pull(agent3,trolley3) ) )
& ( n0 != X1
| pull(agent3,trolley3) != X0
| sP23(X0,X1) ) ),
inference(flattening,[],[f157]) ).
fof(f159,plain,
! [X0,X1] :
( ( ~ sP22(X0,X1)
| ( X1 = n0
& X0 = push(agent3,trolley3) ) )
& ( n0 != X1
| push(agent3,trolley3) != X0
| sP22(X0,X1) ) ),
inference(nnf_transformation,[],[f103]) ).
fof(f160,plain,
! [X0,X1] :
( ( ~ sP22(X0,X1)
| ( X1 = n0
& X0 = push(agent3,trolley3) ) )
& ( n0 != X1
| push(agent3,trolley3) != X0
| sP22(X0,X1) ) ),
inference(flattening,[],[f159]) ).
fof(f161,plain,
! [X0,X1] :
( ( ~ sP21(X0,X1)
| ( X1 = n0
& X0 = pull(agent4,trolley4) ) )
& ( n0 != X1
| pull(agent4,trolley4) != X0
| sP21(X0,X1) ) ),
inference(nnf_transformation,[],[f102]) ).
fof(f162,plain,
! [X0,X1] :
( ( ~ sP21(X0,X1)
| ( X1 = n0
& X0 = pull(agent4,trolley4) ) )
& ( n0 != X1
| pull(agent4,trolley4) != X0
| sP21(X0,X1) ) ),
inference(flattening,[],[f161]) ).
fof(f163,plain,
! [X0,X1] :
( ( ~ sP20(X0,X1)
| ( X1 = n0
& X0 = push(agent4,trolley4) ) )
& ( n0 != X1
| push(agent4,trolley4) != X0
| sP20(X0,X1) ) ),
inference(nnf_transformation,[],[f101]) ).
fof(f164,plain,
! [X0,X1] :
( ( ~ sP20(X0,X1)
| ( X1 = n0
& X0 = push(agent4,trolley4) ) )
& ( n0 != X1
| push(agent4,trolley4) != X0
| sP20(X0,X1) ) ),
inference(flattening,[],[f163]) ).
fof(f165,plain,
! [X0,X1] :
( ( ~ sP19(X0,X1)
| ( X1 = n0
& X0 = pull(agent5,trolley5) ) )
& ( n0 != X1
| pull(agent5,trolley5) != X0
| sP19(X0,X1) ) ),
inference(nnf_transformation,[],[f100]) ).
fof(f166,plain,
! [X0,X1] :
( ( ~ sP19(X0,X1)
| ( X1 = n0
& X0 = pull(agent5,trolley5) ) )
& ( n0 != X1
| pull(agent5,trolley5) != X0
| sP19(X0,X1) ) ),
inference(flattening,[],[f165]) ).
fof(f167,plain,
! [X0,X1] :
( ( ~ sP18(X0,X1)
| ( X1 = n0
& X0 = push(agent5,trolley5) ) )
& ( n0 != X1
| push(agent5,trolley5) != X0
| sP18(X0,X1) ) ),
inference(nnf_transformation,[],[f99]) ).
fof(f168,plain,
! [X0,X1] :
( ( ~ sP18(X0,X1)
| ( X1 = n0
& X0 = push(agent5,trolley5) ) )
& ( n0 != X1
| push(agent5,trolley5) != X0
| sP18(X0,X1) ) ),
inference(flattening,[],[f167]) ).
fof(f169,plain,
! [X0,X1] :
( ( ~ sP17(X0,X1)
| ( X1 = n0
& X0 = pull(agent6,trolley6) ) )
& ( n0 != X1
| pull(agent6,trolley6) != X0
| sP17(X0,X1) ) ),
inference(nnf_transformation,[],[f98]) ).
fof(f170,plain,
! [X0,X1] :
( ( ~ sP17(X0,X1)
| ( X1 = n0
& X0 = pull(agent6,trolley6) ) )
& ( n0 != X1
| pull(agent6,trolley6) != X0
| sP17(X0,X1) ) ),
inference(flattening,[],[f169]) ).
fof(f171,plain,
! [X0,X1] :
( ( ~ sP16(X0,X1)
| ( X1 = n0
& X0 = push(agent6,trolley6) ) )
& ( n0 != X1
| push(agent6,trolley6) != X0
| sP16(X0,X1) ) ),
inference(nnf_transformation,[],[f97]) ).
fof(f172,plain,
! [X0,X1] :
( ( ~ sP16(X0,X1)
| ( X1 = n0
& X0 = push(agent6,trolley6) ) )
& ( n0 != X1
| push(agent6,trolley6) != X0
| sP16(X0,X1) ) ),
inference(flattening,[],[f171]) ).
fof(f173,plain,
! [X0,X1] :
( ( ~ sP15(X0,X1)
| ( X1 = n0
& X0 = pull(agent7,trolley7) ) )
& ( n0 != X1
| pull(agent7,trolley7) != X0
| sP15(X0,X1) ) ),
inference(nnf_transformation,[],[f96]) ).
fof(f174,plain,
! [X0,X1] :
( ( ~ sP15(X0,X1)
| ( X1 = n0
& X0 = pull(agent7,trolley7) ) )
& ( n0 != X1
| pull(agent7,trolley7) != X0
| sP15(X0,X1) ) ),
inference(flattening,[],[f173]) ).
fof(f175,plain,
! [X0,X1] :
( ( ~ sP14(X0,X1)
| ( X1 = n0
& X0 = push(agent7,trolley7) ) )
& ( n0 != X1
| push(agent7,trolley7) != X0
| sP14(X0,X1) ) ),
inference(nnf_transformation,[],[f95]) ).
fof(f176,plain,
! [X0,X1] :
( ( ~ sP14(X0,X1)
| ( X1 = n0
& X0 = push(agent7,trolley7) ) )
& ( n0 != X1
| push(agent7,trolley7) != X0
| sP14(X0,X1) ) ),
inference(flattening,[],[f175]) ).
fof(f177,plain,
! [X0,X1] :
( ( ~ sP13(X0,X1)
| ( X1 = n0
& X0 = pull(agent8,trolley8) ) )
& ( n0 != X1
| pull(agent8,trolley8) != X0
| sP13(X0,X1) ) ),
inference(nnf_transformation,[],[f94]) ).
fof(f178,plain,
! [X0,X1] :
( ( ~ sP13(X0,X1)
| ( X1 = n0
& X0 = pull(agent8,trolley8) ) )
& ( n0 != X1
| pull(agent8,trolley8) != X0
| sP13(X0,X1) ) ),
inference(flattening,[],[f177]) ).
fof(f179,plain,
! [X0,X1] :
( ( ~ sP12(X0,X1)
| ( X1 = n0
& X0 = push(agent8,trolley8) ) )
& ( n0 != X1
| push(agent8,trolley8) != X0
| sP12(X0,X1) ) ),
inference(nnf_transformation,[],[f93]) ).
fof(f180,plain,
! [X0,X1] :
( ( ~ sP12(X0,X1)
| ( X1 = n0
& X0 = push(agent8,trolley8) ) )
& ( n0 != X1
| push(agent8,trolley8) != X0
| sP12(X0,X1) ) ),
inference(flattening,[],[f179]) ).
fof(f181,plain,
! [X0,X1] :
( ( ~ sP11(X0,X1)
| ( X1 = n0
& X0 = pull(agent9,trolley9) ) )
& ( n0 != X1
| pull(agent9,trolley9) != X0
| sP11(X0,X1) ) ),
inference(nnf_transformation,[],[f92]) ).
fof(f182,plain,
! [X0,X1] :
( ( ~ sP11(X0,X1)
| ( X1 = n0
& X0 = pull(agent9,trolley9) ) )
& ( n0 != X1
| pull(agent9,trolley9) != X0
| sP11(X0,X1) ) ),
inference(flattening,[],[f181]) ).
fof(f183,plain,
! [X0,X1] :
( ( ~ sP10(X0,X1)
| ( X1 = n0
& X0 = push(agent9,trolley9) ) )
& ( n0 != X1
| push(agent9,trolley9) != X0
| sP10(X0,X1) ) ),
inference(nnf_transformation,[],[f91]) ).
fof(f184,plain,
! [X0,X1] :
( ( ~ sP10(X0,X1)
| ( X1 = n0
& X0 = push(agent9,trolley9) ) )
& ( n0 != X1
| push(agent9,trolley9) != X0
| sP10(X0,X1) ) ),
inference(flattening,[],[f183]) ).
fof(f185,plain,
! [X0,X1] :
( ( ~ sP9(X0,X1)
| ( X1 = n0
& X0 = pull(agent10,trolley10) ) )
& ( n0 != X1
| pull(agent10,trolley10) != X0
| sP9(X0,X1) ) ),
inference(nnf_transformation,[],[f90]) ).
fof(f186,plain,
! [X0,X1] :
( ( ~ sP9(X0,X1)
| ( X1 = n0
& X0 = pull(agent10,trolley10) ) )
& ( n0 != X1
| pull(agent10,trolley10) != X0
| sP9(X0,X1) ) ),
inference(flattening,[],[f185]) ).
fof(f189,plain,
! [X0,X1] :
( ( ~ happens(X0,X1)
| sP25(X0,X1) )
& ( ~ sP25(X0,X1)
| happens(X0,X1) ) ),
inference(nnf_transformation,[],[f107]) ).
fof(f198,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f66]) ).
fof(f214,plain,
! [X2,X3,X0,X1,X4] :
( ~ sP0(X0,X4,X3,X1,X2)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f120]) ).
fof(f256,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f23]) ).
fof(f299,plain,
! [X0,X1] :
( ~ sP8(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f300,plain,
! [X0,X1] :
( ~ sP9(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f301,plain,
! [X0,X1] :
( ~ sP10(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f302,plain,
! [X0,X1] :
( ~ sP11(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f303,plain,
! [X0,X1] :
( ~ sP12(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f304,plain,
! [X0,X1] :
( ~ sP13(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f305,plain,
! [X0,X1] :
( ~ sP14(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f306,plain,
! [X0,X1] :
( ~ sP15(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f307,plain,
! [X0,X1] :
( ~ sP16(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f308,plain,
! [X0,X1] :
( ~ sP17(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f309,plain,
! [X0,X1] :
( ~ sP18(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f310,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f311,plain,
! [X0,X1] :
( ~ sP20(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f312,plain,
! [X0,X1] :
( ~ sP21(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f313,plain,
! [X0,X1] :
( ~ sP22(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f314,plain,
! [X0,X1] :
( ~ sP23(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f315,plain,
! [X0,X1] :
( ~ sP24(X0,X1)
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f316,plain,
! [X0,X1] :
( n0 != X1
| pull(agent2,trolley2) != X0
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f317,plain,
! [X0,X1] :
( n0 != X1
| push(agent1,trolley1) != X0
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f318,plain,
! [X0,X1] :
( n0 != X1
| pull(agent1,trolley1) != X0
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f321,plain,
! [X0,X1] :
( n0 != X1
| push(agent2,trolley2) != X0
| sP24(X0,X1) ),
inference(cnf_transformation,[],[f156]) ).
fof(f324,plain,
! [X0,X1] :
( n0 != X1
| pull(agent3,trolley3) != X0
| sP23(X0,X1) ),
inference(cnf_transformation,[],[f158]) ).
fof(f327,plain,
! [X0,X1] :
( n0 != X1
| push(agent3,trolley3) != X0
| sP22(X0,X1) ),
inference(cnf_transformation,[],[f160]) ).
fof(f330,plain,
! [X0,X1] :
( n0 != X1
| pull(agent4,trolley4) != X0
| sP21(X0,X1) ),
inference(cnf_transformation,[],[f162]) ).
fof(f333,plain,
! [X0,X1] :
( n0 != X1
| push(agent4,trolley4) != X0
| sP20(X0,X1) ),
inference(cnf_transformation,[],[f164]) ).
fof(f336,plain,
! [X0,X1] :
( n0 != X1
| pull(agent5,trolley5) != X0
| sP19(X0,X1) ),
inference(cnf_transformation,[],[f166]) ).
fof(f339,plain,
! [X0,X1] :
( n0 != X1
| push(agent5,trolley5) != X0
| sP18(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
fof(f342,plain,
! [X0,X1] :
( n0 != X1
| pull(agent6,trolley6) != X0
| sP17(X0,X1) ),
inference(cnf_transformation,[],[f170]) ).
fof(f345,plain,
! [X0,X1] :
( n0 != X1
| push(agent6,trolley6) != X0
| sP16(X0,X1) ),
inference(cnf_transformation,[],[f172]) ).
fof(f348,plain,
! [X0,X1] :
( n0 != X1
| pull(agent7,trolley7) != X0
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f174]) ).
fof(f351,plain,
! [X0,X1] :
( n0 != X1
| push(agent7,trolley7) != X0
| sP14(X0,X1) ),
inference(cnf_transformation,[],[f176]) ).
fof(f354,plain,
! [X0,X1] :
( n0 != X1
| pull(agent8,trolley8) != X0
| sP13(X0,X1) ),
inference(cnf_transformation,[],[f178]) ).
fof(f357,plain,
! [X0,X1] :
( n0 != X1
| push(agent8,trolley8) != X0
| sP12(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f360,plain,
! [X0,X1] :
( n0 != X1
| pull(agent9,trolley9) != X0
| sP11(X0,X1) ),
inference(cnf_transformation,[],[f182]) ).
fof(f363,plain,
! [X0,X1] :
( n0 != X1
| push(agent9,trolley9) != X0
| sP10(X0,X1) ),
inference(cnf_transformation,[],[f184]) ).
fof(f366,plain,
! [X0,X1] :
( n0 != X1
| pull(agent10,trolley10) != X0
| sP9(X0,X1) ),
inference(cnf_transformation,[],[f186]) ).
fof(f371,plain,
! [X0,X1] :
( ~ sP25(X0,X1)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f189]) ).
fof(f493,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,[],[f78]) ).
fof(f514,plain,
! [X1] :
( n0 != X1
| sP25(pull(agent1,trolley1),X1) ),
inference(equality_resolution,[],[f318]) ).
fof(f515,plain,
sP25(pull(agent1,trolley1),n0),
inference(equality_resolution,[],[f514]) ).
fof(f516,plain,
! [X1] :
( n0 != X1
| sP25(push(agent1,trolley1),X1) ),
inference(equality_resolution,[],[f317]) ).
fof(f517,plain,
sP25(push(agent1,trolley1),n0),
inference(equality_resolution,[],[f516]) ).
fof(f518,plain,
! [X1] :
( n0 != X1
| sP25(pull(agent2,trolley2),X1) ),
inference(equality_resolution,[],[f316]) ).
fof(f519,plain,
sP25(pull(agent2,trolley2),n0),
inference(equality_resolution,[],[f518]) ).
fof(f520,plain,
! [X1] :
( n0 != X1
| sP24(push(agent2,trolley2),X1) ),
inference(equality_resolution,[],[f321]) ).
fof(f521,plain,
sP24(push(agent2,trolley2),n0),
inference(equality_resolution,[],[f520]) ).
fof(f522,plain,
! [X1] :
( n0 != X1
| sP23(pull(agent3,trolley3),X1) ),
inference(equality_resolution,[],[f324]) ).
fof(f523,plain,
sP23(pull(agent3,trolley3),n0),
inference(equality_resolution,[],[f522]) ).
fof(f524,plain,
! [X1] :
( n0 != X1
| sP22(push(agent3,trolley3),X1) ),
inference(equality_resolution,[],[f327]) ).
fof(f525,plain,
sP22(push(agent3,trolley3),n0),
inference(equality_resolution,[],[f524]) ).
fof(f526,plain,
! [X1] :
( n0 != X1
| sP21(pull(agent4,trolley4),X1) ),
inference(equality_resolution,[],[f330]) ).
fof(f527,plain,
sP21(pull(agent4,trolley4),n0),
inference(equality_resolution,[],[f526]) ).
fof(f528,plain,
! [X1] :
( n0 != X1
| sP20(push(agent4,trolley4),X1) ),
inference(equality_resolution,[],[f333]) ).
fof(f529,plain,
sP20(push(agent4,trolley4),n0),
inference(equality_resolution,[],[f528]) ).
fof(f530,plain,
! [X1] :
( n0 != X1
| sP19(pull(agent5,trolley5),X1) ),
inference(equality_resolution,[],[f336]) ).
fof(f531,plain,
sP19(pull(agent5,trolley5),n0),
inference(equality_resolution,[],[f530]) ).
fof(f532,plain,
! [X1] :
( n0 != X1
| sP18(push(agent5,trolley5),X1) ),
inference(equality_resolution,[],[f339]) ).
fof(f533,plain,
sP18(push(agent5,trolley5),n0),
inference(equality_resolution,[],[f532]) ).
fof(f534,plain,
! [X1] :
( n0 != X1
| sP17(pull(agent6,trolley6),X1) ),
inference(equality_resolution,[],[f342]) ).
fof(f535,plain,
sP17(pull(agent6,trolley6),n0),
inference(equality_resolution,[],[f534]) ).
fof(f536,plain,
! [X1] :
( n0 != X1
| sP16(push(agent6,trolley6),X1) ),
inference(equality_resolution,[],[f345]) ).
fof(f537,plain,
sP16(push(agent6,trolley6),n0),
inference(equality_resolution,[],[f536]) ).
fof(f538,plain,
! [X1] :
( n0 != X1
| sP15(pull(agent7,trolley7),X1) ),
inference(equality_resolution,[],[f348]) ).
fof(f539,plain,
sP15(pull(agent7,trolley7),n0),
inference(equality_resolution,[],[f538]) ).
fof(f540,plain,
! [X1] :
( n0 != X1
| sP14(push(agent7,trolley7),X1) ),
inference(equality_resolution,[],[f351]) ).
fof(f541,plain,
sP14(push(agent7,trolley7),n0),
inference(equality_resolution,[],[f540]) ).
fof(f542,plain,
! [X1] :
( n0 != X1
| sP13(pull(agent8,trolley8),X1) ),
inference(equality_resolution,[],[f354]) ).
fof(f543,plain,
sP13(pull(agent8,trolley8),n0),
inference(equality_resolution,[],[f542]) ).
fof(f544,plain,
! [X1] :
( n0 != X1
| sP12(push(agent8,trolley8),X1) ),
inference(equality_resolution,[],[f357]) ).
fof(f545,plain,
sP12(push(agent8,trolley8),n0),
inference(equality_resolution,[],[f544]) ).
fof(f546,plain,
! [X1] :
( n0 != X1
| sP11(pull(agent9,trolley9),X1) ),
inference(equality_resolution,[],[f360]) ).
fof(f547,plain,
sP11(pull(agent9,trolley9),n0),
inference(equality_resolution,[],[f546]) ).
fof(f548,plain,
! [X1] :
( n0 != X1
| sP10(push(agent9,trolley9),X1) ),
inference(equality_resolution,[],[f363]) ).
fof(f549,plain,
sP10(push(agent9,trolley9),n0),
inference(equality_resolution,[],[f548]) ).
fof(f550,plain,
! [X1] :
( n0 != X1
| sP9(pull(agent10,trolley10),X1) ),
inference(equality_resolution,[],[f366]) ).
fof(f551,plain,
sP9(pull(agent10,trolley10),n0),
inference(equality_resolution,[],[f550]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] :
( holdsAt(X1,plus(X2,n1))
| ~ happens(X0,X2)
| ~ initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f198]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( initiates(X0,X3,X4)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_115,plain,
plus(n0,n1) = n1,
inference(cnf_transformation,[],[f256]) ).
tcf(c_150,plain,
sP25(pull(agent1,trolley1),n0),
inference(cnf_transformation,[],[f515]) ).
tcf(c_151,plain,
sP25(push(agent1,trolley1),n0),
inference(cnf_transformation,[],[f517]) ).
tcf(c_152,plain,
sP25(pull(agent2,trolley2),n0),
inference(cnf_transformation,[],[f519]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP24(X0,X1) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_154,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP23(X0,X1) ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_155,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP22(X0,X1) ),
inference(cnf_transformation,[],[f313]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP21(X0,X1) ),
inference(cnf_transformation,[],[f312]) ).
tcf(c_157,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP20(X0,X1) ),
inference(cnf_transformation,[],[f311]) ).
tcf(c_158,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP19(X0,X1) ),
inference(cnf_transformation,[],[f310]) ).
tcf(c_159,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP18(X0,X1) ),
inference(cnf_transformation,[],[f309]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP17(X0,X1) ),
inference(cnf_transformation,[],[f308]) ).
tcf(c_161,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP16(X0,X1) ),
inference(cnf_transformation,[],[f307]) ).
tcf(c_162,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP15(X0,X1) ),
inference(cnf_transformation,[],[f306]) ).
tcf(c_163,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP14(X0,X1) ),
inference(cnf_transformation,[],[f305]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP13(X0,X1) ),
inference(cnf_transformation,[],[f304]) ).
tcf(c_165,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP12(X0,X1) ),
inference(cnf_transformation,[],[f303]) ).
tcf(c_166,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP11(X0,X1) ),
inference(cnf_transformation,[],[f302]) ).
tcf(c_167,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP10(X0,X1) ),
inference(cnf_transformation,[],[f301]) ).
tcf(c_168,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP9(X0,X1) ),
inference(cnf_transformation,[],[f300]) ).
tcf(c_169,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP8(X0,X1) ),
inference(cnf_transformation,[],[f299]) ).
tcf(c_178,plain,
sP24(push(agent2,trolley2),n0),
inference(cnf_transformation,[],[f521]) ).
tcf(c_181,plain,
sP23(pull(agent3,trolley3),n0),
inference(cnf_transformation,[],[f523]) ).
tcf(c_184,plain,
sP22(push(agent3,trolley3),n0),
inference(cnf_transformation,[],[f525]) ).
tcf(c_187,plain,
sP21(pull(agent4,trolley4),n0),
inference(cnf_transformation,[],[f527]) ).
tcf(c_190,plain,
sP20(push(agent4,trolley4),n0),
inference(cnf_transformation,[],[f529]) ).
tcf(c_193,plain,
sP19(pull(agent5,trolley5),n0),
inference(cnf_transformation,[],[f531]) ).
tcf(c_196,plain,
sP18(push(agent5,trolley5),n0),
inference(cnf_transformation,[],[f533]) ).
tcf(c_199,plain,
sP17(pull(agent6,trolley6),n0),
inference(cnf_transformation,[],[f535]) ).
tcf(c_202,plain,
sP16(push(agent6,trolley6),n0),
inference(cnf_transformation,[],[f537]) ).
tcf(c_205,plain,
sP15(pull(agent7,trolley7),n0),
inference(cnf_transformation,[],[f539]) ).
tcf(c_208,plain,
sP14(push(agent7,trolley7),n0),
inference(cnf_transformation,[],[f541]) ).
tcf(c_211,plain,
sP13(pull(agent8,trolley8),n0),
inference(cnf_transformation,[],[f543]) ).
tcf(c_214,plain,
sP12(push(agent8,trolley8),n0),
inference(cnf_transformation,[],[f545]) ).
tcf(c_217,plain,
sP11(pull(agent9,trolley9),n0),
inference(cnf_transformation,[],[f547]) ).
tcf(c_220,plain,
sP10(push(agent9,trolley9),n0),
inference(cnf_transformation,[],[f549]) ).
tcf(c_223,plain,
sP9(pull(agent10,trolley10),n0),
inference(cnf_transformation,[],[f551]) ).
tcf(c_229,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ~ sP25(X0,X1) ),
inference(cnf_transformation,[],[f371]) ).
tcf(c_352,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(cnf_transformation,[],[f493]) ).
tcf(c_521,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ~ sP25(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_229]) ).
tcf(c_659,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP24(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_153]) ).
tcf(c_665,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP23(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_154]) ).
tcf(c_671,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP22(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_155]) ).
tcf(c_677,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP21(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_156]) ).
tcf(c_683,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP20(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_157]) ).
tcf(c_689,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP19(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_158]) ).
tcf(c_695,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP18(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_159]) ).
tcf(c_701,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP17(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_160]) ).
tcf(c_707,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP16(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_161]) ).
tcf(c_713,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP15(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_162]) ).
tcf(c_719,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP14(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_163]) ).
tcf(c_725,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP13(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_164]) ).
tcf(c_731,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP12(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_165]) ).
tcf(c_737,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP11(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_166]) ).
tcf(c_743,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP10(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_167]) ).
tcf(c_749,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP9(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_168]) ).
tcf(c_755,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ~ sP8(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_169]) ).
tcf(c_3970,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( push(agent2,trolley2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_659,c_178]) ).
tcf(c_3971,plain,
sP25(push(agent2,trolley2),n0),
inference(unflattening,[status(thm)],[c_3970]) ).
tcf(c_4032,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( pull(agent3,trolley3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_665,c_181]) ).
tcf(c_4033,plain,
sP25(pull(agent3,trolley3),n0),
inference(unflattening,[status(thm)],[c_4032]) ).
tcf(c_4094,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( push(agent3,trolley3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_671,c_184]) ).
tcf(c_4095,plain,
sP25(push(agent3,trolley3),n0),
inference(unflattening,[status(thm)],[c_4094]) ).
tcf(c_4156,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( pull(agent4,trolley4) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_677,c_187]) ).
tcf(c_4157,plain,
sP25(pull(agent4,trolley4),n0),
inference(unflattening,[status(thm)],[c_4156]) ).
tcf(c_4218,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( push(agent4,trolley4) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_683,c_190]) ).
tcf(c_4219,plain,
sP25(push(agent4,trolley4),n0),
inference(unflattening,[status(thm)],[c_4218]) ).
tcf(c_4280,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( pull(agent5,trolley5) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_689,c_193]) ).
tcf(c_4281,plain,
sP25(pull(agent5,trolley5),n0),
inference(unflattening,[status(thm)],[c_4280]) ).
tcf(c_4342,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( push(agent5,trolley5) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_695,c_196]) ).
tcf(c_4343,plain,
sP25(push(agent5,trolley5),n0),
inference(unflattening,[status(thm)],[c_4342]) ).
tcf(c_4404,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( pull(agent6,trolley6) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_701,c_199]) ).
tcf(c_4405,plain,
sP25(pull(agent6,trolley6),n0),
inference(unflattening,[status(thm)],[c_4404]) ).
tcf(c_4466,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( push(agent6,trolley6) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_707,c_202]) ).
tcf(c_4467,plain,
sP25(push(agent6,trolley6),n0),
inference(unflattening,[status(thm)],[c_4466]) ).
tcf(c_4528,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( pull(agent7,trolley7) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_713,c_205]) ).
tcf(c_4529,plain,
sP25(pull(agent7,trolley7),n0),
inference(unflattening,[status(thm)],[c_4528]) ).
tcf(c_4590,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( push(agent7,trolley7) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_719,c_208]) ).
tcf(c_4591,plain,
sP25(push(agent7,trolley7),n0),
inference(unflattening,[status(thm)],[c_4590]) ).
tcf(c_4652,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( pull(agent8,trolley8) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_725,c_211]) ).
tcf(c_4653,plain,
sP25(pull(agent8,trolley8),n0),
inference(unflattening,[status(thm)],[c_4652]) ).
tcf(c_4714,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( push(agent8,trolley8) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_731,c_214]) ).
tcf(c_4715,plain,
sP25(push(agent8,trolley8),n0),
inference(unflattening,[status(thm)],[c_4714]) ).
tcf(c_4776,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( pull(agent9,trolley9) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_737,c_217]) ).
tcf(c_4777,plain,
sP25(pull(agent9,trolley9),n0),
inference(unflattening,[status(thm)],[c_4776]) ).
tcf(c_4838,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( push(agent9,trolley9) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_743,c_220]) ).
tcf(c_4839,plain,
sP25(push(agent9,trolley9),n0),
inference(unflattening,[status(thm)],[c_4838]) ).
tcf(c_4900,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( pull(agent10,trolley10) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_749,c_223]) ).
tcf(c_4901,plain,
sP25(pull(agent10,trolley10),n0),
inference(unflattening,[status(thm)],[c_4900]) ).
tcf(c_10068,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent1,trolley1) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_150,c_521]) ).
tcf(c_10069,plain,
happens(pull(agent1,trolley1),n0),
inference(unflattening,[status(thm)],[c_10068]) ).
tcf(c_10077,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent1,trolley1) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_151,c_521]) ).
tcf(c_10078,plain,
happens(push(agent1,trolley1),n0),
inference(unflattening,[status(thm)],[c_10077]) ).
tcf(c_10086,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent2,trolley2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_152,c_521]) ).
tcf(c_10087,plain,
happens(pull(agent2,trolley2),n0),
inference(unflattening,[status(thm)],[c_10086]) ).
tcf(c_10095,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent2,trolley2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_3971]) ).
tcf(c_10096,plain,
happens(push(agent2,trolley2),n0),
inference(unflattening,[status(thm)],[c_10095]) ).
tcf(c_10104,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent3,trolley3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4033]) ).
tcf(c_10105,plain,
happens(pull(agent3,trolley3),n0),
inference(unflattening,[status(thm)],[c_10104]) ).
tcf(c_10113,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent3,trolley3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4095]) ).
tcf(c_10114,plain,
happens(push(agent3,trolley3),n0),
inference(unflattening,[status(thm)],[c_10113]) ).
tcf(c_10122,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent4,trolley4) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4157]) ).
tcf(c_10123,plain,
happens(pull(agent4,trolley4),n0),
inference(unflattening,[status(thm)],[c_10122]) ).
tcf(c_10131,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent4,trolley4) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4219]) ).
tcf(c_10132,plain,
happens(push(agent4,trolley4),n0),
inference(unflattening,[status(thm)],[c_10131]) ).
tcf(c_10140,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent5,trolley5) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4281]) ).
tcf(c_10141,plain,
happens(pull(agent5,trolley5),n0),
inference(unflattening,[status(thm)],[c_10140]) ).
tcf(c_10149,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent5,trolley5) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4343]) ).
tcf(c_10150,plain,
happens(push(agent5,trolley5),n0),
inference(unflattening,[status(thm)],[c_10149]) ).
tcf(c_10158,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent6,trolley6) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4405]) ).
tcf(c_10159,plain,
happens(pull(agent6,trolley6),n0),
inference(unflattening,[status(thm)],[c_10158]) ).
tcf(c_10167,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent6,trolley6) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4467]) ).
tcf(c_10168,plain,
happens(push(agent6,trolley6),n0),
inference(unflattening,[status(thm)],[c_10167]) ).
tcf(c_10176,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent7,trolley7) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4529]) ).
tcf(c_10177,plain,
happens(pull(agent7,trolley7),n0),
inference(unflattening,[status(thm)],[c_10176]) ).
tcf(c_10185,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent7,trolley7) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4591]) ).
tcf(c_10186,plain,
happens(push(agent7,trolley7),n0),
inference(unflattening,[status(thm)],[c_10185]) ).
tcf(c_10194,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent8,trolley8) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4653]) ).
tcf(c_10195,plain,
happens(pull(agent8,trolley8),n0),
inference(unflattening,[status(thm)],[c_10194]) ).
tcf(c_10203,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent8,trolley8) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4715]) ).
tcf(c_10204,plain,
happens(push(agent8,trolley8),n0),
inference(unflattening,[status(thm)],[c_10203]) ).
tcf(c_10212,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent9,trolley9) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4777]) ).
tcf(c_10213,plain,
happens(pull(agent9,trolley9),n0),
inference(unflattening,[status(thm)],[c_10212]) ).
tcf(c_10221,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent9,trolley9) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4839]) ).
tcf(c_10222,plain,
happens(push(agent9,trolley9),n0),
inference(unflattening,[status(thm)],[c_10221]) ).
tcf(c_10230,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent10,trolley10) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4901]) ).
tcf(c_10231,plain,
happens(pull(agent10,trolley10),n0),
inference(unflattening,[status(thm)],[c_10230]) ).
tcf(c_15249,definition,
iPr_def_10 = spinning(trolley1),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_15250,definition,
iPr_def_11 = spinning(trolley2),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_15251,definition,
iPr_def_12 = spinning(trolley3),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_15252,definition,
iPr_def_13 = spinning(trolley4),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_15253,definition,
iPr_def_14 = spinning(trolley5),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_15254,definition,
iPr_def_15 = spinning(trolley6),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_15255,definition,
iPr_def_16 = spinning(trolley7),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_15256,definition,
iPr_def_17 = spinning(trolley8),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_15257,definition,
iPr_def_18 = spinning(trolley9),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_15258,definition,
iPr_def_19 = spinning(trolley10),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_15259,negated_conjecture,
( ~ holdsAt(iPr_def_19,n1)
| ~ holdsAt(iPr_def_18,n1)
| ~ holdsAt(iPr_def_17,n1)
| ~ holdsAt(iPr_def_16,n1)
| ~ holdsAt(iPr_def_15,n1)
| ~ holdsAt(iPr_def_14,n1)
| ~ holdsAt(iPr_def_13,n1)
| ~ holdsAt(iPr_def_12,n1)
| ~ holdsAt(iPr_def_11,n1)
| ~ holdsAt(iPr_def_10,n1) ),
inference(demodulation,[status(thm)],[c_352,c_15258,c_15257,c_15256,c_15255,c_15254,c_15253,c_15252,c_15251,c_15250,c_15249]) ).
fof(f79,definition,
! [X0,X4,X3,X1,X2] :
( sP0(X0,X4,X3,X1,X2)
<=> ( happens(push(X3,X4),X2)
& X1 = spinning(X4)
& X0 = pull(X3,X4) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f80,definition,
! [X0,X4,X3,X1,X2] :
( sP1(X0,X4,X3,X1,X2)
<=> ( ~ happens(push(X3,X4),X2)
& X1 = backwards(X4)
& X0 = pull(X3,X4) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f81,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ? [X3,X4] :
( sP0(X0,X4,X3,X1,X2)
| sP1(X0,X4,X3,X1,X2)
| ( ~ happens(pull(X3,X4),X2)
& X1 = forwards(X4)
& X0 = push(X3,X4) ) ) ),
inference(definition_folding,[],[f13,f80,f79]) ).
fof(f89,definition,
! [X0,X1] :
( sP8(X0,X1)
<=> ( X1 = n0
& X0 = push(agent10,trolley10) ) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f90,definition,
! [X0,X1] :
( sP9(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent10,trolley10) ) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f91,definition,
! [X0,X1] :
( sP10(X0,X1)
<=> ( X1 = n0
& X0 = push(agent9,trolley9) ) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f92,definition,
! [X0,X1] :
( sP11(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent9,trolley9) ) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f93,definition,
! [X0,X1] :
( sP12(X0,X1)
<=> ( X1 = n0
& X0 = push(agent8,trolley8) ) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f94,definition,
! [X0,X1] :
( sP13(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent8,trolley8) ) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f95,definition,
! [X0,X1] :
( sP14(X0,X1)
<=> ( X1 = n0
& X0 = push(agent7,trolley7) ) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f96,definition,
! [X0,X1] :
( sP15(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent7,trolley7) ) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f97,definition,
! [X0,X1] :
( sP16(X0,X1)
<=> ( X1 = n0
& X0 = push(agent6,trolley6) ) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f98,definition,
! [X0,X1] :
( sP17(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent6,trolley6) ) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f99,definition,
! [X0,X1] :
( sP18(X0,X1)
<=> ( X1 = n0
& X0 = push(agent5,trolley5) ) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f100,definition,
! [X0,X1] :
( sP19(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent5,trolley5) ) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f101,definition,
! [X0,X1] :
( sP20(X0,X1)
<=> ( X1 = n0
& X0 = push(agent4,trolley4) ) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f102,definition,
! [X0,X1] :
( sP21(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent4,trolley4) ) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f103,definition,
! [X0,X1] :
( sP22(X0,X1)
<=> ( X1 = n0
& X0 = push(agent3,trolley3) ) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f104,definition,
! [X0,X1] :
( sP23(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent3,trolley3) ) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f105,definition,
! [X0,X1] :
( sP24(X0,X1)
<=> ( X1 = n0
& X0 = push(agent2,trolley2) ) ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f106,definition,
! [X0,X1] :
( sP25(X0,X1)
<=> ( sP8(X0,X1)
| sP9(X0,X1)
| sP10(X0,X1)
| sP11(X0,X1)
| sP12(X0,X1)
| sP13(X0,X1)
| sP14(X0,X1)
| sP15(X0,X1)
| sP16(X0,X1)
| sP17(X0,X1)
| sP18(X0,X1)
| sP19(X0,X1)
| sP20(X0,X1)
| sP21(X0,X1)
| sP22(X0,X1)
| sP23(X0,X1)
| sP24(X0,X1)
| ( X1 = n0
& X0 = pull(agent2,trolley2) )
| ( X1 = n0
& X0 = push(agent1,trolley1) )
| ( X1 = n0
& X0 = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f107,plain,
! [X0,X1] :
( happens(X0,X1)
<=> sP25(X0,X1) ),
inference(definition_folding,[],[f45,f106,f105,f104,f103,f102,f101,f100,f99,f98,f97,f96,f95,f94,f93,f92,f91,f90,f89]) ).
fof(f115,plain,
! [X0,X4,X3,X1,X2] :
( ( ~ sP0(X0,X4,X3,X1,X2)
| ( happens(push(X3,X4),X2)
& X1 = spinning(X4)
& X0 = pull(X3,X4) ) )
& ( ~ happens(push(X3,X4),X2)
| spinning(X4) != X1
| pull(X3,X4) != X0
| sP0(X0,X4,X3,X1,X2) ) ),
inference(nnf_transformation,[],[f79]) ).
fof(f116,plain,
! [X0,X4,X3,X1,X2] :
( ( ~ sP0(X0,X4,X3,X1,X2)
| ( happens(push(X3,X4),X2)
& X1 = spinning(X4)
& X0 = pull(X3,X4) ) )
& ( ~ happens(push(X3,X4),X2)
| spinning(X4) != X1
| pull(X3,X4) != X0
| sP0(X0,X4,X3,X1,X2) ) ),
inference(flattening,[],[f115]) ).
fof(f117,plain,
! [X0,X1,X2,X3,X4] :
( ( ~ sP0(X0,X1,X2,X3,X4)
| ( happens(push(X2,X1),X4)
& spinning(X1) = X3
& pull(X2,X1) = X0 ) )
& ( ~ happens(push(X2,X1),X4)
| spinning(X1) != X3
| pull(X2,X1) != X0
| sP0(X0,X1,X2,X3,X4) ) ),
inference(rectify,[],[f116]) ).
fof(f187,plain,
! [X0,X1] :
( ( ~ sP8(X0,X1)
| ( X1 = n0
& X0 = push(agent10,trolley10) ) )
& ( n0 != X1
| push(agent10,trolley10) != X0
| sP8(X0,X1) ) ),
inference(nnf_transformation,[],[f89]) ).
fof(f188,plain,
! [X0,X1] :
( ( ~ sP8(X0,X1)
| ( X1 = n0
& X0 = push(agent10,trolley10) ) )
& ( n0 != X1
| push(agent10,trolley10) != X0
| sP8(X0,X1) ) ),
inference(flattening,[],[f187]) ).
fof(f210,plain,
! [X2,X3,X0,X1,X4] :
( ~ happens(push(X2,X1),X4)
| spinning(X1) != X3
| pull(X2,X1) != X0
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f117]) ).
fof(f369,plain,
! [X0,X1] :
( n0 != X1
| push(agent10,trolley10) != X0
| sP8(X0,X1) ),
inference(cnf_transformation,[],[f188]) ).
fof(f496,plain,
! [X2,X3,X1,X4] :
( ~ happens(push(X2,X1),X4)
| spinning(X1) != X3
| sP0(pull(X2,X1),X1,X2,X3,X4) ),
inference(equality_resolution,[],[f210]) ).
fof(f497,plain,
! [X2,X1,X4] :
( ~ happens(push(X2,X1),X4)
| sP0(pull(X2,X1),X1,X2,spinning(X1),X4) ),
inference(equality_resolution,[],[f496]) ).
fof(f552,plain,
! [X1] :
( n0 != X1
| sP8(push(agent10,trolley10),X1) ),
inference(equality_resolution,[],[f369]) ).
fof(f553,plain,
sP8(push(agent10,trolley10),n0),
inference(equality_resolution,[],[f552]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP0(pull(X0,X1),X1,X0,spinning(X1),X2)
| ~ happens(push(X0,X1),X2) ),
inference(cnf_transformation,[],[f497]) ).
tcf(c_226,plain,
sP8(push(agent10,trolley10),n0),
inference(cnf_transformation,[],[f553]) ).
tcf(c_4961,plain,
! [X0: $i,X1: $i] :
( sP25(X0,X1)
| ( X1 != n0 )
| ( push(agent10,trolley10) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_755,c_226]) ).
tcf(c_4962,plain,
sP25(push(agent10,trolley10),n0),
inference(unflattening,[status(thm)],[c_4961]) ).
tcf(c_10239,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent10,trolley10) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_521,c_4962]) ).
tcf(c_10240,plain,
happens(push(agent10,trolley10),n0),
inference(unflattening,[status(thm)],[c_10239]) ).
tcf(c_19887,plain,
! [X0: $i,X1: $i,X2: $i] :
( initiates(pull(X0,X1),spinning(X1),X2)
| ~ happens(push(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_66,c_72]) ).
tcf(c_27923,plain,
! [X0: $i,X1: $i] :
( initiates(pull(X0,trolley1),iPr_def_10,X1)
| ~ happens(push(X0,trolley1),X1) ),
inference(superposition,[status(thm)],[c_15249,c_19887]) ).
tcf(c_27924,plain,
! [X0: $i,X1: $i] :
( initiates(pull(X0,trolley2),iPr_def_11,X1)
| ~ happens(push(X0,trolley2),X1) ),
inference(superposition,[status(thm)],[c_15250,c_19887]) ).
tcf(c_27925,plain,
! [X0: $i,X1: $i] :
( initiates(pull(X0,trolley3),iPr_def_12,X1)
| ~ happens(push(X0,trolley3),X1) ),
inference(superposition,[status(thm)],[c_15251,c_19887]) ).
tcf(c_27926,plain,
! [X0: $i,X1: $i] :
( initiates(pull(X0,trolley4),iPr_def_13,X1)
| ~ happens(push(X0,trolley4),X1) ),
inference(superposition,[status(thm)],[c_15252,c_19887]) ).
tcf(c_27927,plain,
! [X0: $i,X1: $i] :
( initiates(pull(X0,trolley5),iPr_def_14,X1)
| ~ happens(push(X0,trolley5),X1) ),
inference(superposition,[status(thm)],[c_15253,c_19887]) ).
tcf(c_27928,plain,
! [X0: $i,X1: $i] :
( initiates(pull(X0,trolley6),iPr_def_15,X1)
| ~ happens(push(X0,trolley6),X1) ),
inference(superposition,[status(thm)],[c_15254,c_19887]) ).
tcf(c_27929,plain,
! [X0: $i,X1: $i] :
( initiates(pull(X0,trolley7),iPr_def_16,X1)
| ~ happens(push(X0,trolley7),X1) ),
inference(superposition,[status(thm)],[c_15255,c_19887]) ).
tcf(c_27930,plain,
! [X0: $i,X1: $i] :
( initiates(pull(X0,trolley8),iPr_def_17,X1)
| ~ happens(push(X0,trolley8),X1) ),
inference(superposition,[status(thm)],[c_15256,c_19887]) ).
tcf(c_27931,plain,
! [X0: $i,X1: $i] :
( initiates(pull(X0,trolley9),iPr_def_18,X1)
| ~ happens(push(X0,trolley9),X1) ),
inference(superposition,[status(thm)],[c_15257,c_19887]) ).
tcf(c_27932,plain,
! [X0: $i,X1: $i] :
( initiates(pull(X0,trolley10),iPr_def_19,X1)
| ~ happens(push(X0,trolley10),X1) ),
inference(superposition,[status(thm)],[c_15258,c_19887]) ).
tcf(c_27972,plain,
! [X0: $i,X1: $i] :
( holdsAt(iPr_def_10,plus(X1,n1))
| ~ happens(push(X0,trolley1),X1)
| ~ happens(pull(X0,trolley1),X1) ),
inference(superposition,[status(thm)],[c_27923,c_57]) ).
tcf(c_27988,plain,
! [X0: $i,X1: $i] :
( holdsAt(iPr_def_11,plus(X1,n1))
| ~ happens(push(X0,trolley2),X1)
| ~ happens(pull(X0,trolley2),X1) ),
inference(superposition,[status(thm)],[c_27924,c_57]) ).
tcf(c_27997,plain,
! [X0: $i,X1: $i] :
( holdsAt(iPr_def_12,plus(X1,n1))
| ~ happens(push(X0,trolley3),X1)
| ~ happens(pull(X0,trolley3),X1) ),
inference(superposition,[status(thm)],[c_27925,c_57]) ).
tcf(c_28006,plain,
! [X0: $i,X1: $i] :
( holdsAt(iPr_def_13,plus(X1,n1))
| ~ happens(push(X0,trolley4),X1)
| ~ happens(pull(X0,trolley4),X1) ),
inference(superposition,[status(thm)],[c_27926,c_57]) ).
tcf(c_28015,plain,
! [X0: $i,X1: $i] :
( holdsAt(iPr_def_14,plus(X1,n1))
| ~ happens(push(X0,trolley5),X1)
| ~ happens(pull(X0,trolley5),X1) ),
inference(superposition,[status(thm)],[c_27927,c_57]) ).
tcf(c_28024,plain,
! [X0: $i,X1: $i] :
( holdsAt(iPr_def_15,plus(X1,n1))
| ~ happens(push(X0,trolley6),X1)
| ~ happens(pull(X0,trolley6),X1) ),
inference(superposition,[status(thm)],[c_27928,c_57]) ).
tcf(c_28033,plain,
! [X0: $i,X1: $i] :
( holdsAt(iPr_def_16,plus(X1,n1))
| ~ happens(push(X0,trolley7),X1)
| ~ happens(pull(X0,trolley7),X1) ),
inference(superposition,[status(thm)],[c_27929,c_57]) ).
tcf(c_28042,plain,
! [X0: $i,X1: $i] :
( holdsAt(iPr_def_17,plus(X1,n1))
| ~ happens(push(X0,trolley8),X1)
| ~ happens(pull(X0,trolley8),X1) ),
inference(superposition,[status(thm)],[c_27930,c_57]) ).
tcf(c_28051,plain,
! [X0: $i,X1: $i] :
( holdsAt(iPr_def_18,plus(X1,n1))
| ~ happens(push(X0,trolley9),X1)
| ~ happens(pull(X0,trolley9),X1) ),
inference(superposition,[status(thm)],[c_27931,c_57]) ).
tcf(c_28060,plain,
! [X0: $i,X1: $i] :
( holdsAt(iPr_def_19,plus(X1,n1))
| ~ happens(push(X0,trolley10),X1)
| ~ happens(pull(X0,trolley10),X1) ),
inference(superposition,[status(thm)],[c_27932,c_57]) ).
tcf(c_31797,plain,
( holdsAt(iPr_def_10,plus(n0,n1))
| ~ happens(push(agent1,trolley1),n0) ),
inference(superposition,[status(thm)],[c_10069,c_27972]) ).
tcf(c_31798,plain,
( holdsAt(iPr_def_10,n1)
| ~ happens(push(agent1,trolley1),n0) ),
inference(light_normalisation,[status(thm)],[c_31797,c_115]) ).
tcf(c_31799,plain,
holdsAt(iPr_def_10,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_31798,c_10078]) ).
tcf(c_31802,plain,
( ~ holdsAt(iPr_def_19,n1)
| ~ holdsAt(iPr_def_18,n1)
| ~ holdsAt(iPr_def_17,n1)
| ~ holdsAt(iPr_def_16,n1)
| ~ holdsAt(iPr_def_15,n1)
| ~ holdsAt(iPr_def_14,n1)
| ~ holdsAt(iPr_def_13,n1)
| ~ holdsAt(iPr_def_12,n1)
| ~ holdsAt(iPr_def_11,n1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_15259,c_31799]) ).
tcf(c_31824,plain,
( holdsAt(iPr_def_11,plus(n0,n1))
| ~ happens(push(agent2,trolley2),n0) ),
inference(superposition,[status(thm)],[c_10087,c_27988]) ).
tcf(c_31825,plain,
( holdsAt(iPr_def_11,n1)
| ~ happens(push(agent2,trolley2),n0) ),
inference(light_normalisation,[status(thm)],[c_31824,c_115]) ).
tcf(c_31826,plain,
holdsAt(iPr_def_11,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_31825,c_10096]) ).
tcf(c_31841,plain,
( holdsAt(iPr_def_12,plus(n0,n1))
| ~ happens(push(agent3,trolley3),n0) ),
inference(superposition,[status(thm)],[c_10105,c_27997]) ).
tcf(c_31842,plain,
( holdsAt(iPr_def_12,n1)
| ~ happens(push(agent3,trolley3),n0) ),
inference(light_normalisation,[status(thm)],[c_31841,c_115]) ).
tcf(c_31843,plain,
holdsAt(iPr_def_12,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_31842,c_10114]) ).
tcf(c_31854,plain,
( holdsAt(iPr_def_13,plus(n0,n1))
| ~ happens(push(agent4,trolley4),n0) ),
inference(superposition,[status(thm)],[c_10123,c_28006]) ).
tcf(c_31855,plain,
( holdsAt(iPr_def_13,n1)
| ~ happens(push(agent4,trolley4),n0) ),
inference(light_normalisation,[status(thm)],[c_31854,c_115]) ).
tcf(c_31856,plain,
holdsAt(iPr_def_13,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_31855,c_10132]) ).
tcf(c_31881,plain,
( ~ holdsAt(iPr_def_19,n1)
| ~ holdsAt(iPr_def_18,n1)
| ~ holdsAt(iPr_def_17,n1)
| ~ holdsAt(iPr_def_16,n1)
| ~ holdsAt(iPr_def_15,n1)
| ~ holdsAt(iPr_def_14,n1) ),
inference(global_subsumption_just,[status(thm)],[c_31802,c_31802,c_31826,c_31843,c_31856]) ).
tcf(c_32054,plain,
( holdsAt(iPr_def_14,plus(n0,n1))
| ~ happens(push(agent5,trolley5),n0) ),
inference(superposition,[status(thm)],[c_10141,c_28015]) ).
tcf(c_32055,plain,
( holdsAt(iPr_def_14,n1)
| ~ happens(push(agent5,trolley5),n0) ),
inference(light_normalisation,[status(thm)],[c_32054,c_115]) ).
tcf(c_32056,plain,
holdsAt(iPr_def_14,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_32055,c_10150]) ).
tcf(c_32057,plain,
( ~ holdsAt(iPr_def_19,n1)
| ~ holdsAt(iPr_def_18,n1)
| ~ holdsAt(iPr_def_17,n1)
| ~ holdsAt(iPr_def_16,n1)
| ~ holdsAt(iPr_def_15,n1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_31881,c_32056]) ).
tcf(c_32073,plain,
( holdsAt(iPr_def_15,plus(n0,n1))
| ~ happens(push(agent6,trolley6),n0) ),
inference(superposition,[status(thm)],[c_10159,c_28024]) ).
tcf(c_32074,plain,
( holdsAt(iPr_def_15,n1)
| ~ happens(push(agent6,trolley6),n0) ),
inference(light_normalisation,[status(thm)],[c_32073,c_115]) ).
tcf(c_32075,plain,
holdsAt(iPr_def_15,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_32074,c_10168]) ).
tcf(c_32086,plain,
( holdsAt(iPr_def_16,plus(n0,n1))
| ~ happens(push(agent7,trolley7),n0) ),
inference(superposition,[status(thm)],[c_10177,c_28033]) ).
tcf(c_32087,plain,
( holdsAt(iPr_def_16,n1)
| ~ happens(push(agent7,trolley7),n0) ),
inference(light_normalisation,[status(thm)],[c_32086,c_115]) ).
tcf(c_32088,plain,
holdsAt(iPr_def_16,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_32087,c_10186]) ).
tcf(c_32099,plain,
( holdsAt(iPr_def_17,plus(n0,n1))
| ~ happens(push(agent8,trolley8),n0) ),
inference(superposition,[status(thm)],[c_10195,c_28042]) ).
tcf(c_32100,plain,
( holdsAt(iPr_def_17,n1)
| ~ happens(push(agent8,trolley8),n0) ),
inference(light_normalisation,[status(thm)],[c_32099,c_115]) ).
tcf(c_32101,plain,
holdsAt(iPr_def_17,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_32100,c_10204]) ).
tcf(c_32118,plain,
( ~ holdsAt(iPr_def_19,n1)
| ~ holdsAt(iPr_def_18,n1) ),
inference(global_subsumption_just,[status(thm)],[c_32057,c_32057,c_32075,c_32088,c_32101]) ).
tcf(c_32193,plain,
( holdsAt(iPr_def_18,plus(n0,n1))
| ~ happens(push(agent9,trolley9),n0) ),
inference(superposition,[status(thm)],[c_10213,c_28051]) ).
tcf(c_32194,plain,
( holdsAt(iPr_def_18,n1)
| ~ happens(push(agent9,trolley9),n0) ),
inference(light_normalisation,[status(thm)],[c_32193,c_115]) ).
tcf(c_32195,plain,
holdsAt(iPr_def_18,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_32194,c_10222]) ).
tcf(c_32207,plain,
( holdsAt(iPr_def_19,plus(n0,n1))
| ~ happens(push(agent10,trolley10),n0) ),
inference(superposition,[status(thm)],[c_10231,c_28060]) ).
tcf(c_32208,plain,
( holdsAt(iPr_def_19,n1)
| ~ happens(push(agent10,trolley10),n0) ),
inference(light_normalisation,[status(thm)],[c_32207,c_115]) ).
tcf(c_32209,plain,
holdsAt(iPr_def_19,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_32208,c_10240]) ).
tcf(c_32210,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_32209,c_32195,c_32118]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR024+1.010 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.38 % Computer : n005.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Fri Sep 25 08:08:33 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 2.81/1.75 % SZS status Started for theBenchmark.p
% 2.81/1.75 % SZS status Theorem for theBenchmark.p
% 2.81/1.75
% 2.81/1.75 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.81/1.75
% 2.81/1.75 % ------ iProver source info
% 2.81/1.75
% 2.81/1.75 % git: date: 2026-07-19 20:42:38 +0200
% 2.81/1.75 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.81/1.75 % git: non_committed_changes: false
% 2.81/1.75
% 2.81/1.75 % ------ Parsing...
% 2.81/1.75 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.81/1.75
% 2.81/1.75 % ------ Preprocessing... sup_sim: 0 sf_s rm: 3 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe_e sup_sim: 0 sf_s rm: 20 0s sf_e pe_s pe_e %
% 2.81/1.75
% 2.81/1.75 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.81/1.75
% 2.81/1.75 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 2.81/1.75 % ------ Proving...
% 2.81/1.75 % ------ Problem Properties
% 2.81/1.75
% 2.81/1.75 %
% 2.81/1.75 % clauses 244
% 2.81/1.75 % conjectures 1
% 2.81/1.75 % EPR 124
% 2.81/1.75 % Horn 223
% 2.81/1.75 % unary 168
% 2.81/1.75 % binary 58
% 2.81/1.75 % lits 375
% 2.81/1.75 % lits eq 162
% 2.81/1.75 % fd_pure 0
% 2.81/1.75 % fd_pseudo 0
% 2.81/1.75 % fd_cond 2
% 2.81/1.75 % fd_pseudo_cond 18
% 2.81/1.75 % AC symbols 0
% 2.81/1.75
% 2.81/1.75 % ------ Schedule dynamic 5 is on
% 2.81/1.75
% 2.81/1.75 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 2.81/1.75
% 2.81/1.75
% 2.81/1.75 % ------
% 2.81/1.75 % Current options:
% 2.81/1.75 % ------
% 2.81/1.75
% 2.81/1.75
% 2.81/1.75 %
% 2.81/1.75
% 2.81/1.75 % ------ Proving...
% 2.81/1.75 %
% 2.81/1.75
% 2.81/1.75 % SZS status Theorem for theBenchmark.p
% 2.81/1.75
% 2.81/1.75 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.81/1.75
% 2.81/1.75
%------------------------------------------------------------------------------