%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR024+1.009 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:41:59 AM UTC 2026
% Result : Theorem 4.68s 1.38s
% Output : Refutation 5.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 32
% Syntax : Number of formulae : 240 ( 91 unt; 27 def)
% Number of atoms : 797 ( 311 equ)
% Maximal formula atoms : 44 ( 3 avg)
% Number of connectives : 860 ( 303 ~; 333 |; 192 &)
% ( 31 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 32 ( 30 usr; 10 prp; 0-5 aty)
% Number of functors : 28 ( 28 usr; 20 con; 0-3 aty)
% Number of variables : 277 ( 0 sgn 269 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& initiates(X0,X2,X1) )
=> holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_holds) ).
fof(f23,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_1) ).
fof(f45,axiom,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ? [X3,X4] :
( ( X0 = push(X3,X4)
& X1 = forwards(X4)
& ~ happens(pull(X3,X4),X2) )
| ( X0 = pull(X3,X4)
& X1 = backwards(X4)
& ~ happens(push(X3,X4),X2) )
| ( X0 = pull(X3,X4)
& X1 = spinning(X4)
& happens(push(X3,X4),X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',initiates_all_defn) ).
fof(f48,axiom,
! [X0,X1] :
( happens(X0,X1)
<=> ( ( X0 = pull(agent1,trolley1)
& X1 = n0 )
| ( X0 = push(agent1,trolley1)
& X1 = n0 )
| ( X0 = pull(agent2,trolley2)
& X1 = n0 )
| ( X0 = push(agent2,trolley2)
& X1 = n0 )
| ( X0 = pull(agent3,trolley3)
& X1 = n0 )
| ( X0 = push(agent3,trolley3)
& X1 = n0 )
| ( X0 = pull(agent4,trolley4)
& X1 = n0 )
| ( X0 = push(agent4,trolley4)
& X1 = n0 )
| ( X0 = pull(agent5,trolley5)
& X1 = n0 )
| ( X0 = push(agent5,trolley5)
& X1 = n0 )
| ( X0 = pull(agent6,trolley6)
& X1 = n0 )
| ( X0 = push(agent6,trolley6)
& X1 = n0 )
| ( X0 = pull(agent7,trolley7)
& X1 = n0 )
| ( X0 = push(agent7,trolley7)
& X1 = n0 )
| ( X0 = pull(agent8,trolley8)
& X1 = n0 )
| ( X0 = push(agent8,trolley8)
& X1 = n0 )
| ( X0 = pull(agent9,trolley9)
& X1 = n0 )
| ( X0 = push(agent9,trolley9)
& X1 = n0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_all_defn) ).
fof(f58,conjecture,
( holdsAt(spinning(trolley1),n1)
& holdsAt(spinning(trolley2),n1)
& holdsAt(spinning(trolley3),n1)
& holdsAt(spinning(trolley4),n1)
& holdsAt(spinning(trolley5),n1)
& holdsAt(spinning(trolley6),n1)
& holdsAt(spinning(trolley7),n1)
& holdsAt(spinning(trolley8),n1)
& holdsAt(spinning(trolley9),n1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',spinning_3) ).
fof(f59,negated_conjecture,
~ ( holdsAt(spinning(trolley1),n1)
& holdsAt(spinning(trolley2),n1)
& holdsAt(spinning(trolley3),n1)
& holdsAt(spinning(trolley4),n1)
& holdsAt(spinning(trolley5),n1)
& holdsAt(spinning(trolley6),n1)
& holdsAt(spinning(trolley7),n1)
& holdsAt(spinning(trolley8),n1)
& holdsAt(spinning(trolley9),n1) ),
inference(negated_conjecture,[status(cth)],[f58]) ).
fof(f66,plain,
( ~ holdsAt(spinning(trolley1),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley9),n1) ),
inference(ennf_transformation,[],[f59]) ).
fof(f70,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f71,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(flattening,[],[f70]) ).
fof(f92,definition,
! [X0,X1] :
( sP0(X0,X1)
<=> ( X0 = push(agent9,trolley9)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f93,definition,
! [X0,X1] :
( sP1(X0,X1)
<=> ( X0 = pull(agent9,trolley9)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f94,definition,
! [X0,X1] :
( sP2(X0,X1)
<=> ( X0 = push(agent8,trolley8)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f95,definition,
! [X0,X1] :
( sP3(X0,X1)
<=> ( X0 = pull(agent8,trolley8)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f96,definition,
! [X0,X1] :
( sP4(X0,X1)
<=> ( X0 = push(agent7,trolley7)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f97,definition,
! [X0,X1] :
( sP5(X0,X1)
<=> ( X0 = pull(agent7,trolley7)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f98,definition,
! [X0,X1] :
( sP6(X0,X1)
<=> ( X0 = push(agent6,trolley6)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f99,definition,
! [X0,X1] :
( sP7(X0,X1)
<=> ( X0 = pull(agent6,trolley6)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f100,definition,
! [X0,X1] :
( sP8(X0,X1)
<=> ( X0 = push(agent5,trolley5)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f101,definition,
! [X0,X1] :
( sP9(X0,X1)
<=> ( X0 = pull(agent5,trolley5)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f102,definition,
! [X0,X1] :
( sP10(X0,X1)
<=> ( X0 = push(agent4,trolley4)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f103,definition,
! [X0,X1] :
( sP11(X0,X1)
<=> ( X0 = pull(agent4,trolley4)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f104,definition,
! [X0,X1] :
( sP12(X0,X1)
<=> ( X0 = push(agent3,trolley3)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f105,definition,
! [X0,X1] :
( sP13(X0,X1)
<=> ( X0 = pull(agent3,trolley3)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f106,definition,
! [X0,X1] :
( sP14(X0,X1)
<=> ( X0 = push(agent2,trolley2)
& X1 = n0 ) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f107,definition,
! [X0,X1] :
( sP15(X0,X1)
<=> ( ( X0 = pull(agent1,trolley1)
& X1 = n0 )
| ( X0 = push(agent1,trolley1)
& X1 = n0 )
| ( X0 = pull(agent2,trolley2)
& X1 = n0 )
| sP14(X0,X1)
| sP13(X0,X1)
| sP12(X0,X1)
| sP11(X0,X1)
| sP10(X0,X1)
| sP9(X0,X1)
| sP8(X0,X1)
| sP7(X0,X1)
| sP6(X0,X1)
| sP5(X0,X1)
| sP4(X0,X1)
| sP3(X0,X1)
| sP2(X0,X1)
| sP1(X0,X1)
| sP0(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f108,plain,
! [X0,X1] :
( happens(X0,X1)
<=> sP15(X0,X1) ),
inference(definition_folding,[],[f48,f107,f106,f105,f104,f103,f102,f101,f100,f99,f98,f97,f96,f95,f94,f93,f92]) ).
fof(f123,definition,
! [X0,X4,X3,X1,X2] :
( sP28(X0,X4,X3,X1,X2)
<=> ( X0 = pull(X3,X4)
& X1 = spinning(X4)
& happens(push(X3,X4),X2) ) ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f124,definition,
! [X0,X4,X3,X1,X2] :
( sP29(X0,X4,X3,X1,X2)
<=> ( X0 = pull(X3,X4)
& X1 = backwards(X4)
& ~ happens(push(X3,X4),X2) ) ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f125,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ? [X3,X4] :
( ( X0 = push(X3,X4)
& X1 = forwards(X4)
& ~ happens(pull(X3,X4),X2) )
| sP29(X0,X4,X3,X1,X2)
| sP28(X0,X4,X3,X1,X2) ) ),
inference(definition_folding,[],[f45,f124,f123]) ).
fof(f132,plain,
! [X0,X1] :
( ( sP15(X0,X1)
| ( ( pull(agent1,trolley1) != X0
| n0 != X1 )
& ( push(agent1,trolley1) != X0
| n0 != X1 )
& ( pull(agent2,trolley2) != X0
| n0 != X1 )
& ~ sP14(X0,X1)
& ~ sP13(X0,X1)
& ~ sP12(X0,X1)
& ~ sP11(X0,X1)
& ~ sP10(X0,X1)
& ~ sP9(X0,X1)
& ~ sP8(X0,X1)
& ~ sP7(X0,X1)
& ~ sP6(X0,X1)
& ~ sP5(X0,X1)
& ~ sP4(X0,X1)
& ~ sP3(X0,X1)
& ~ sP2(X0,X1)
& ~ sP1(X0,X1)
& ~ sP0(X0,X1) ) )
& ( ( X0 = pull(agent1,trolley1)
& X1 = n0 )
| ( X0 = push(agent1,trolley1)
& X1 = n0 )
| ( X0 = pull(agent2,trolley2)
& X1 = n0 )
| sP14(X0,X1)
| sP13(X0,X1)
| sP12(X0,X1)
| sP11(X0,X1)
| sP10(X0,X1)
| sP9(X0,X1)
| sP8(X0,X1)
| sP7(X0,X1)
| sP6(X0,X1)
| sP5(X0,X1)
| sP4(X0,X1)
| sP3(X0,X1)
| sP2(X0,X1)
| sP1(X0,X1)
| sP0(X0,X1)
| ~ sP15(X0,X1) ) ),
inference(nnf_transformation,[],[f107]) ).
fof(f133,plain,
! [X0,X1] :
( ( sP15(X0,X1)
| ( ( pull(agent1,trolley1) != X0
| n0 != X1 )
& ( push(agent1,trolley1) != X0
| n0 != X1 )
& ( pull(agent2,trolley2) != X0
| n0 != X1 )
& ~ sP14(X0,X1)
& ~ sP13(X0,X1)
& ~ sP12(X0,X1)
& ~ sP11(X0,X1)
& ~ sP10(X0,X1)
& ~ sP9(X0,X1)
& ~ sP8(X0,X1)
& ~ sP7(X0,X1)
& ~ sP6(X0,X1)
& ~ sP5(X0,X1)
& ~ sP4(X0,X1)
& ~ sP3(X0,X1)
& ~ sP2(X0,X1)
& ~ sP1(X0,X1)
& ~ sP0(X0,X1) ) )
& ( ( X0 = pull(agent1,trolley1)
& X1 = n0 )
| ( X0 = push(agent1,trolley1)
& X1 = n0 )
| ( X0 = pull(agent2,trolley2)
& X1 = n0 )
| sP14(X0,X1)
| sP13(X0,X1)
| sP12(X0,X1)
| sP11(X0,X1)
| sP10(X0,X1)
| sP9(X0,X1)
| sP8(X0,X1)
| sP7(X0,X1)
| sP6(X0,X1)
| sP5(X0,X1)
| sP4(X0,X1)
| sP3(X0,X1)
| sP2(X0,X1)
| sP1(X0,X1)
| sP0(X0,X1)
| ~ sP15(X0,X1) ) ),
inference(flattening,[],[f132]) ).
fof(f134,plain,
! [X0,X1] :
( ( sP14(X0,X1)
| push(agent2,trolley2) != X0
| n0 != X1 )
& ( ( X0 = push(agent2,trolley2)
& X1 = n0 )
| ~ sP14(X0,X1) ) ),
inference(nnf_transformation,[],[f106]) ).
fof(f135,plain,
! [X0,X1] :
( ( sP14(X0,X1)
| push(agent2,trolley2) != X0
| n0 != X1 )
& ( ( X0 = push(agent2,trolley2)
& X1 = n0 )
| ~ sP14(X0,X1) ) ),
inference(flattening,[],[f134]) ).
fof(f136,plain,
! [X0,X1] :
( ( sP13(X0,X1)
| pull(agent3,trolley3) != X0
| n0 != X1 )
& ( ( X0 = pull(agent3,trolley3)
& X1 = n0 )
| ~ sP13(X0,X1) ) ),
inference(nnf_transformation,[],[f105]) ).
fof(f137,plain,
! [X0,X1] :
( ( sP13(X0,X1)
| pull(agent3,trolley3) != X0
| n0 != X1 )
& ( ( X0 = pull(agent3,trolley3)
& X1 = n0 )
| ~ sP13(X0,X1) ) ),
inference(flattening,[],[f136]) ).
fof(f138,plain,
! [X0,X1] :
( ( sP12(X0,X1)
| push(agent3,trolley3) != X0
| n0 != X1 )
& ( ( X0 = push(agent3,trolley3)
& X1 = n0 )
| ~ sP12(X0,X1) ) ),
inference(nnf_transformation,[],[f104]) ).
fof(f139,plain,
! [X0,X1] :
( ( sP12(X0,X1)
| push(agent3,trolley3) != X0
| n0 != X1 )
& ( ( X0 = push(agent3,trolley3)
& X1 = n0 )
| ~ sP12(X0,X1) ) ),
inference(flattening,[],[f138]) ).
fof(f140,plain,
! [X0,X1] :
( ( sP11(X0,X1)
| pull(agent4,trolley4) != X0
| n0 != X1 )
& ( ( X0 = pull(agent4,trolley4)
& X1 = n0 )
| ~ sP11(X0,X1) ) ),
inference(nnf_transformation,[],[f103]) ).
fof(f141,plain,
! [X0,X1] :
( ( sP11(X0,X1)
| pull(agent4,trolley4) != X0
| n0 != X1 )
& ( ( X0 = pull(agent4,trolley4)
& X1 = n0 )
| ~ sP11(X0,X1) ) ),
inference(flattening,[],[f140]) ).
fof(f142,plain,
! [X0,X1] :
( ( sP10(X0,X1)
| push(agent4,trolley4) != X0
| n0 != X1 )
& ( ( X0 = push(agent4,trolley4)
& X1 = n0 )
| ~ sP10(X0,X1) ) ),
inference(nnf_transformation,[],[f102]) ).
fof(f143,plain,
! [X0,X1] :
( ( sP10(X0,X1)
| push(agent4,trolley4) != X0
| n0 != X1 )
& ( ( X0 = push(agent4,trolley4)
& X1 = n0 )
| ~ sP10(X0,X1) ) ),
inference(flattening,[],[f142]) ).
fof(f144,plain,
! [X0,X1] :
( ( sP9(X0,X1)
| pull(agent5,trolley5) != X0
| n0 != X1 )
& ( ( X0 = pull(agent5,trolley5)
& X1 = n0 )
| ~ sP9(X0,X1) ) ),
inference(nnf_transformation,[],[f101]) ).
fof(f145,plain,
! [X0,X1] :
( ( sP9(X0,X1)
| pull(agent5,trolley5) != X0
| n0 != X1 )
& ( ( X0 = pull(agent5,trolley5)
& X1 = n0 )
| ~ sP9(X0,X1) ) ),
inference(flattening,[],[f144]) ).
fof(f146,plain,
! [X0,X1] :
( ( sP8(X0,X1)
| push(agent5,trolley5) != X0
| n0 != X1 )
& ( ( X0 = push(agent5,trolley5)
& X1 = n0 )
| ~ sP8(X0,X1) ) ),
inference(nnf_transformation,[],[f100]) ).
fof(f147,plain,
! [X0,X1] :
( ( sP8(X0,X1)
| push(agent5,trolley5) != X0
| n0 != X1 )
& ( ( X0 = push(agent5,trolley5)
& X1 = n0 )
| ~ sP8(X0,X1) ) ),
inference(flattening,[],[f146]) ).
fof(f148,plain,
! [X0,X1] :
( ( sP7(X0,X1)
| pull(agent6,trolley6) != X0
| n0 != X1 )
& ( ( X0 = pull(agent6,trolley6)
& X1 = n0 )
| ~ sP7(X0,X1) ) ),
inference(nnf_transformation,[],[f99]) ).
fof(f149,plain,
! [X0,X1] :
( ( sP7(X0,X1)
| pull(agent6,trolley6) != X0
| n0 != X1 )
& ( ( X0 = pull(agent6,trolley6)
& X1 = n0 )
| ~ sP7(X0,X1) ) ),
inference(flattening,[],[f148]) ).
fof(f150,plain,
! [X0,X1] :
( ( sP6(X0,X1)
| push(agent6,trolley6) != X0
| n0 != X1 )
& ( ( X0 = push(agent6,trolley6)
& X1 = n0 )
| ~ sP6(X0,X1) ) ),
inference(nnf_transformation,[],[f98]) ).
fof(f151,plain,
! [X0,X1] :
( ( sP6(X0,X1)
| push(agent6,trolley6) != X0
| n0 != X1 )
& ( ( X0 = push(agent6,trolley6)
& X1 = n0 )
| ~ sP6(X0,X1) ) ),
inference(flattening,[],[f150]) ).
fof(f152,plain,
! [X0,X1] :
( ( sP5(X0,X1)
| pull(agent7,trolley7) != X0
| n0 != X1 )
& ( ( X0 = pull(agent7,trolley7)
& X1 = n0 )
| ~ sP5(X0,X1) ) ),
inference(nnf_transformation,[],[f97]) ).
fof(f153,plain,
! [X0,X1] :
( ( sP5(X0,X1)
| pull(agent7,trolley7) != X0
| n0 != X1 )
& ( ( X0 = pull(agent7,trolley7)
& X1 = n0 )
| ~ sP5(X0,X1) ) ),
inference(flattening,[],[f152]) ).
fof(f154,plain,
! [X0,X1] :
( ( sP4(X0,X1)
| push(agent7,trolley7) != X0
| n0 != X1 )
& ( ( X0 = push(agent7,trolley7)
& X1 = n0 )
| ~ sP4(X0,X1) ) ),
inference(nnf_transformation,[],[f96]) ).
fof(f155,plain,
! [X0,X1] :
( ( sP4(X0,X1)
| push(agent7,trolley7) != X0
| n0 != X1 )
& ( ( X0 = push(agent7,trolley7)
& X1 = n0 )
| ~ sP4(X0,X1) ) ),
inference(flattening,[],[f154]) ).
fof(f156,plain,
! [X0,X1] :
( ( sP3(X0,X1)
| pull(agent8,trolley8) != X0
| n0 != X1 )
& ( ( X0 = pull(agent8,trolley8)
& X1 = n0 )
| ~ sP3(X0,X1) ) ),
inference(nnf_transformation,[],[f95]) ).
fof(f157,plain,
! [X0,X1] :
( ( sP3(X0,X1)
| pull(agent8,trolley8) != X0
| n0 != X1 )
& ( ( X0 = pull(agent8,trolley8)
& X1 = n0 )
| ~ sP3(X0,X1) ) ),
inference(flattening,[],[f156]) ).
fof(f158,plain,
! [X0,X1] :
( ( sP2(X0,X1)
| push(agent8,trolley8) != X0
| n0 != X1 )
& ( ( X0 = push(agent8,trolley8)
& X1 = n0 )
| ~ sP2(X0,X1) ) ),
inference(nnf_transformation,[],[f94]) ).
fof(f159,plain,
! [X0,X1] :
( ( sP2(X0,X1)
| push(agent8,trolley8) != X0
| n0 != X1 )
& ( ( X0 = push(agent8,trolley8)
& X1 = n0 )
| ~ sP2(X0,X1) ) ),
inference(flattening,[],[f158]) ).
fof(f160,plain,
! [X0,X1] :
( ( sP1(X0,X1)
| pull(agent9,trolley9) != X0
| n0 != X1 )
& ( ( X0 = pull(agent9,trolley9)
& X1 = n0 )
| ~ sP1(X0,X1) ) ),
inference(nnf_transformation,[],[f93]) ).
fof(f161,plain,
! [X0,X1] :
( ( sP1(X0,X1)
| pull(agent9,trolley9) != X0
| n0 != X1 )
& ( ( X0 = pull(agent9,trolley9)
& X1 = n0 )
| ~ sP1(X0,X1) ) ),
inference(flattening,[],[f160]) ).
fof(f162,plain,
! [X0,X1] :
( ( sP0(X0,X1)
| push(agent9,trolley9) != X0
| n0 != X1 )
& ( ( X0 = push(agent9,trolley9)
& X1 = n0 )
| ~ sP0(X0,X1) ) ),
inference(nnf_transformation,[],[f92]) ).
fof(f163,plain,
! [X0,X1] :
( ( sP0(X0,X1)
| push(agent9,trolley9) != X0
| n0 != X1 )
& ( ( X0 = push(agent9,trolley9)
& X1 = n0 )
| ~ sP0(X0,X1) ) ),
inference(flattening,[],[f162]) ).
fof(f164,plain,
! [X0,X1] :
( ( happens(X0,X1)
| ~ sP15(X0,X1) )
& ( sP15(X0,X1)
| ~ happens(X0,X1) ) ),
inference(nnf_transformation,[],[f108]) ).
fof(f212,plain,
! [X0,X4,X3,X1,X2] :
( ( sP28(X0,X4,X3,X1,X2)
| pull(X3,X4) != X0
| spinning(X4) != X1
| ~ happens(push(X3,X4),X2) )
& ( ( X0 = pull(X3,X4)
& X1 = spinning(X4)
& happens(push(X3,X4),X2) )
| ~ sP28(X0,X4,X3,X1,X2) ) ),
inference(nnf_transformation,[],[f123]) ).
fof(f213,plain,
! [X0,X4,X3,X1,X2] :
( ( sP28(X0,X4,X3,X1,X2)
| pull(X3,X4) != X0
| spinning(X4) != X1
| ~ happens(push(X3,X4),X2) )
& ( ( X0 = pull(X3,X4)
& X1 = spinning(X4)
& happens(push(X3,X4),X2) )
| ~ sP28(X0,X4,X3,X1,X2) ) ),
inference(flattening,[],[f212]) ).
fof(f214,plain,
! [X0,X1,X2,X3,X4] :
( ( sP28(X0,X1,X2,X3,X4)
| pull(X2,X1) != X0
| spinning(X1) != X3
| ~ happens(push(X2,X1),X4) )
& ( ( pull(X2,X1) = X0
& spinning(X1) = X3
& happens(push(X2,X1),X4) )
| ~ sP28(X0,X1,X2,X3,X4) ) ),
inference(rectify,[],[f213]) ).
fof(f215,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ! [X3,X4] :
( ( push(X3,X4) != X0
| forwards(X4) != X1
| happens(pull(X3,X4),X2) )
& ~ sP29(X0,X4,X3,X1,X2)
& ~ sP28(X0,X4,X3,X1,X2) ) )
& ( ? [X3,X4] :
( ( X0 = push(X3,X4)
& X1 = forwards(X4)
& ~ happens(pull(X3,X4),X2) )
| sP29(X0,X4,X3,X1,X2)
| sP28(X0,X4,X3,X1,X2) )
| ~ initiates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f125]) ).
fof(f216,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ! [X3,X4] :
( ( push(X3,X4) != X0
| forwards(X4) != X1
| happens(pull(X3,X4),X2) )
& ~ sP29(X0,X4,X3,X1,X2)
& ~ sP28(X0,X4,X3,X1,X2) ) )
& ( ? [X5,X6] :
( ( push(X5,X6) = X0
& forwards(X6) = X1
& ~ happens(pull(X5,X6),X2) )
| sP29(X0,X6,X5,X1,X2)
| sP28(X0,X6,X5,X1,X2) )
| ~ initiates(X0,X1,X2) ) ),
inference(rectify,[],[f215]) ).
fof(f217,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ! [X3,X4] :
( ( push(X3,X4) != X0
| forwards(X4) != X1
| happens(pull(X3,X4),X2) )
& ~ sP29(X0,X4,X3,X1,X2)
& ~ sP28(X0,X4,X3,X1,X2) ) )
& ( ( push(sK40(X0,X1,X2),sK41(X0,X1,X2)) = X0
& forwards(sK41(X0,X1,X2)) = X1
& ~ happens(pull(sK40(X0,X1,X2),sK41(X0,X1,X2)),X2) )
| sP29(X0,sK41(X0,X1,X2),sK40(X0,X1,X2),X1,X2)
| sP28(X0,sK41(X0,X1,X2),sK40(X0,X1,X2),X1,X2)
| ~ initiates(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40,sK41]),skolemize(X5,sK40(X0,X1,X2)),skolemize(X6,sK41(X0,X1,X2))],[f216]) ).
fof(f327,plain,
( ~ holdsAt(spinning(trolley1),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley9),n1) ),
inference(cnf_transformation,[],[f66]) ).
fof(f331,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f23]) ).
fof(f340,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f71]) ).
fof(f353,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f354,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f355,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f356,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f357,plain,
! [X0,X1] :
( ~ sP4(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f358,plain,
! [X0,X1] :
( ~ sP5(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f359,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f360,plain,
! [X0,X1] :
( ~ sP7(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f361,plain,
! [X0,X1] :
( ~ sP8(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f362,plain,
! [X0,X1] :
( ~ sP9(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f363,plain,
! [X0,X1] :
( ~ sP10(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f364,plain,
! [X0,X1] :
( ~ sP11(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f365,plain,
! [X0,X1] :
( ~ sP12(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f366,plain,
! [X0,X1] :
( ~ sP13(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f367,plain,
! [X0,X1] :
( ~ sP14(X0,X1)
| sP15(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f368,plain,
! [X0,X1] :
( sP15(X0,X1)
| pull(agent2,trolley2) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f133]) ).
fof(f369,plain,
! [X0,X1] :
( sP15(X0,X1)
| push(agent1,trolley1) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f133]) ).
fof(f370,plain,
! [X0,X1] :
( sP15(X0,X1)
| pull(agent1,trolley1) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f133]) ).
fof(f373,plain,
! [X0,X1] :
( sP14(X0,X1)
| push(agent2,trolley2) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f135]) ).
fof(f376,plain,
! [X0,X1] :
( sP13(X0,X1)
| pull(agent3,trolley3) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f137]) ).
fof(f379,plain,
! [X0,X1] :
( sP12(X0,X1)
| push(agent3,trolley3) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f139]) ).
fof(f382,plain,
! [X0,X1] :
( sP11(X0,X1)
| pull(agent4,trolley4) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f141]) ).
fof(f385,plain,
! [X0,X1] :
( sP10(X0,X1)
| push(agent4,trolley4) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f143]) ).
fof(f388,plain,
! [X0,X1] :
( sP9(X0,X1)
| pull(agent5,trolley5) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f145]) ).
fof(f391,plain,
! [X0,X1] :
( sP8(X0,X1)
| push(agent5,trolley5) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f147]) ).
fof(f394,plain,
! [X0,X1] :
( sP7(X0,X1)
| pull(agent6,trolley6) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f149]) ).
fof(f397,plain,
! [X0,X1] :
( sP6(X0,X1)
| push(agent6,trolley6) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f151]) ).
fof(f400,plain,
! [X0,X1] :
( sP5(X0,X1)
| pull(agent7,trolley7) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f153]) ).
fof(f403,plain,
! [X0,X1] :
( sP4(X0,X1)
| push(agent7,trolley7) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f155]) ).
fof(f406,plain,
! [X0,X1] :
( sP3(X0,X1)
| pull(agent8,trolley8) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f157]) ).
fof(f409,plain,
! [X0,X1] :
( sP2(X0,X1)
| push(agent8,trolley8) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f159]) ).
fof(f412,plain,
! [X0,X1] :
( sP1(X0,X1)
| pull(agent9,trolley9) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f161]) ).
fof(f415,plain,
! [X0,X1] :
( sP0(X0,X1)
| push(agent9,trolley9) != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f163]) ).
fof(f417,plain,
! [X0,X1] :
( ~ sP15(X0,X1)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f164]) ).
fof(f501,plain,
! [X2,X3,X0,X1,X4] :
( sP28(X0,X1,X2,X3,X4)
| pull(X2,X1) != X0
| spinning(X1) != X3
| ~ happens(push(X2,X1),X4) ),
inference(cnf_transformation,[],[f214]) ).
fof(f505,plain,
! [X2,X3,X0,X1,X4] :
( ~ sP28(X0,X4,X3,X1,X2)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f217]) ).
fof(f530,plain,
! [X1] :
( sP15(pull(agent1,trolley1),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f370]) ).
fof(f531,plain,
sP15(pull(agent1,trolley1),n0),
inference(equality_resolution,[],[f530]) ).
fof(f532,plain,
! [X1] :
( sP15(push(agent1,trolley1),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f369]) ).
fof(f533,plain,
sP15(push(agent1,trolley1),n0),
inference(equality_resolution,[],[f532]) ).
fof(f534,plain,
! [X1] :
( sP15(pull(agent2,trolley2),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f368]) ).
fof(f535,plain,
sP15(pull(agent2,trolley2),n0),
inference(equality_resolution,[],[f534]) ).
fof(f536,plain,
! [X1] :
( sP14(push(agent2,trolley2),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f373]) ).
fof(f537,plain,
sP14(push(agent2,trolley2),n0),
inference(equality_resolution,[],[f536]) ).
fof(f538,plain,
! [X1] :
( sP13(pull(agent3,trolley3),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f376]) ).
fof(f539,plain,
sP13(pull(agent3,trolley3),n0),
inference(equality_resolution,[],[f538]) ).
fof(f540,plain,
! [X1] :
( sP12(push(agent3,trolley3),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f379]) ).
fof(f541,plain,
sP12(push(agent3,trolley3),n0),
inference(equality_resolution,[],[f540]) ).
fof(f542,plain,
! [X1] :
( sP11(pull(agent4,trolley4),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f382]) ).
fof(f543,plain,
sP11(pull(agent4,trolley4),n0),
inference(equality_resolution,[],[f542]) ).
fof(f544,plain,
! [X1] :
( sP10(push(agent4,trolley4),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f385]) ).
fof(f545,plain,
sP10(push(agent4,trolley4),n0),
inference(equality_resolution,[],[f544]) ).
fof(f546,plain,
! [X1] :
( sP9(pull(agent5,trolley5),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f388]) ).
fof(f547,plain,
sP9(pull(agent5,trolley5),n0),
inference(equality_resolution,[],[f546]) ).
fof(f548,plain,
! [X1] :
( sP8(push(agent5,trolley5),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f391]) ).
fof(f549,plain,
sP8(push(agent5,trolley5),n0),
inference(equality_resolution,[],[f548]) ).
fof(f550,plain,
! [X1] :
( sP7(pull(agent6,trolley6),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f394]) ).
fof(f551,plain,
sP7(pull(agent6,trolley6),n0),
inference(equality_resolution,[],[f550]) ).
fof(f552,plain,
! [X1] :
( sP6(push(agent6,trolley6),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f397]) ).
fof(f553,plain,
sP6(push(agent6,trolley6),n0),
inference(equality_resolution,[],[f552]) ).
fof(f554,plain,
! [X1] :
( sP5(pull(agent7,trolley7),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f400]) ).
fof(f555,plain,
sP5(pull(agent7,trolley7),n0),
inference(equality_resolution,[],[f554]) ).
fof(f556,plain,
! [X1] :
( sP4(push(agent7,trolley7),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f403]) ).
fof(f557,plain,
sP4(push(agent7,trolley7),n0),
inference(equality_resolution,[],[f556]) ).
fof(f558,plain,
! [X1] :
( sP3(pull(agent8,trolley8),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f406]) ).
fof(f559,plain,
sP3(pull(agent8,trolley8),n0),
inference(equality_resolution,[],[f558]) ).
fof(f560,plain,
! [X1] :
( sP2(push(agent8,trolley8),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f409]) ).
fof(f561,plain,
sP2(push(agent8,trolley8),n0),
inference(equality_resolution,[],[f560]) ).
fof(f562,plain,
! [X1] :
( sP1(pull(agent9,trolley9),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f412]) ).
fof(f563,plain,
sP1(pull(agent9,trolley9),n0),
inference(equality_resolution,[],[f562]) ).
fof(f564,plain,
! [X1] :
( sP0(push(agent9,trolley9),X1)
| n0 != X1 ),
inference(equality_resolution,[],[f415]) ).
fof(f565,plain,
sP0(push(agent9,trolley9),n0),
inference(equality_resolution,[],[f564]) ).
fof(f594,plain,
! [X2,X3,X1,X4] :
( sP28(pull(X2,X1),X1,X2,X3,X4)
| spinning(X1) != X3
| ~ happens(push(X2,X1),X4) ),
inference(equality_resolution,[],[f501]) ).
fof(f595,plain,
! [X2,X1,X4] :
( sP28(pull(X2,X1),X1,X2,spinning(X1),X4)
| ~ happens(push(X2,X1),X4) ),
inference(equality_resolution,[],[f594]) ).
fof(f623,definition,
( spl44_1
<=> holdsAt(spinning(trolley9),n1) ),
introduced(definition,[new_symbols(definition,[spl44_1])],[avatar_definition]) ).
fof(f625,plain,
( ~ holdsAt(spinning(trolley9),n1)
| spl44_1 ),
inference(avatar_component_clause,[],[f623]) ).
fof(f627,definition,
( spl44_2
<=> holdsAt(spinning(trolley8),n1) ),
introduced(definition,[new_symbols(definition,[spl44_2])],[avatar_definition]) ).
fof(f631,definition,
( spl44_3
<=> holdsAt(spinning(trolley7),n1) ),
introduced(definition,[new_symbols(definition,[spl44_3])],[avatar_definition]) ).
fof(f635,definition,
( spl44_4
<=> holdsAt(spinning(trolley6),n1) ),
introduced(definition,[new_symbols(definition,[spl44_4])],[avatar_definition]) ).
fof(f639,definition,
( spl44_5
<=> holdsAt(spinning(trolley5),n1) ),
introduced(definition,[new_symbols(definition,[spl44_5])],[avatar_definition]) ).
fof(f643,definition,
( spl44_6
<=> holdsAt(spinning(trolley4),n1) ),
introduced(definition,[new_symbols(definition,[spl44_6])],[avatar_definition]) ).
fof(f647,definition,
( spl44_7
<=> holdsAt(spinning(trolley3),n1) ),
introduced(definition,[new_symbols(definition,[spl44_7])],[avatar_definition]) ).
fof(f651,definition,
( spl44_8
<=> holdsAt(spinning(trolley2),n1) ),
introduced(definition,[new_symbols(definition,[spl44_8])],[avatar_definition]) ).
fof(f655,definition,
( spl44_9
<=> holdsAt(spinning(trolley1),n1) ),
introduced(definition,[new_symbols(definition,[spl44_9])],[avatar_definition]) ).
fof(f658,plain,
( ~ spl44_1
| ~ spl44_2
| ~ spl44_3
| ~ spl44_4
| ~ spl44_5
| ~ spl44_6
| ~ spl44_7
| ~ spl44_8
| ~ spl44_9 ),
inference(avatar_split_clause,[],[f327,f655,f651,f647,f643,f639,f635,f631,f627,f623]) ).
fof(f759,plain,
sP15(push(agent9,trolley9),n0),
inference(resolution,[],[f353,f565]) ).
fof(f760,plain,
sP15(pull(agent9,trolley9),n0),
inference(resolution,[],[f354,f563]) ).
fof(f761,plain,
sP15(push(agent8,trolley8),n0),
inference(resolution,[],[f355,f561]) ).
fof(f762,plain,
sP15(pull(agent8,trolley8),n0),
inference(resolution,[],[f356,f559]) ).
fof(f763,plain,
sP15(push(agent7,trolley7),n0),
inference(resolution,[],[f357,f557]) ).
fof(f764,plain,
sP15(pull(agent7,trolley7),n0),
inference(resolution,[],[f358,f555]) ).
fof(f765,plain,
sP15(push(agent6,trolley6),n0),
inference(resolution,[],[f359,f553]) ).
fof(f766,plain,
sP15(pull(agent6,trolley6),n0),
inference(resolution,[],[f360,f551]) ).
fof(f767,plain,
sP15(push(agent5,trolley5),n0),
inference(resolution,[],[f361,f549]) ).
fof(f768,plain,
sP15(pull(agent5,trolley5),n0),
inference(resolution,[],[f362,f547]) ).
fof(f769,plain,
sP15(push(agent4,trolley4),n0),
inference(resolution,[],[f363,f545]) ).
fof(f770,plain,
sP15(pull(agent4,trolley4),n0),
inference(resolution,[],[f364,f543]) ).
fof(f771,plain,
sP15(push(agent3,trolley3),n0),
inference(resolution,[],[f365,f541]) ).
fof(f772,plain,
sP15(pull(agent3,trolley3),n0),
inference(resolution,[],[f366,f539]) ).
fof(f773,plain,
sP15(push(agent2,trolley2),n0),
inference(resolution,[],[f367,f537]) ).
fof(f789,plain,
happens(pull(agent1,trolley1),n0),
inference(resolution,[],[f417,f531]) ).
fof(f790,plain,
happens(pull(agent2,trolley2),n0),
inference(resolution,[],[f417,f535]) ).
fof(f791,plain,
happens(pull(agent3,trolley3),n0),
inference(resolution,[],[f417,f772]) ).
fof(f792,plain,
happens(pull(agent4,trolley4),n0),
inference(resolution,[],[f417,f770]) ).
fof(f793,plain,
happens(pull(agent5,trolley5),n0),
inference(resolution,[],[f417,f768]) ).
fof(f794,plain,
happens(pull(agent6,trolley6),n0),
inference(resolution,[],[f417,f766]) ).
fof(f795,plain,
happens(pull(agent7,trolley7),n0),
inference(resolution,[],[f417,f764]) ).
fof(f796,plain,
happens(pull(agent8,trolley8),n0),
inference(resolution,[],[f417,f762]) ).
fof(f797,plain,
happens(pull(agent9,trolley9),n0),
inference(resolution,[],[f417,f760]) ).
fof(f798,plain,
happens(push(agent1,trolley1),n0),
inference(resolution,[],[f417,f533]) ).
fof(f799,plain,
happens(push(agent2,trolley2),n0),
inference(resolution,[],[f417,f773]) ).
fof(f800,plain,
happens(push(agent3,trolley3),n0),
inference(resolution,[],[f417,f771]) ).
fof(f801,plain,
happens(push(agent4,trolley4),n0),
inference(resolution,[],[f417,f769]) ).
fof(f802,plain,
happens(push(agent5,trolley5),n0),
inference(resolution,[],[f417,f767]) ).
fof(f803,plain,
happens(push(agent6,trolley6),n0),
inference(resolution,[],[f417,f765]) ).
fof(f804,plain,
happens(push(agent7,trolley7),n0),
inference(resolution,[],[f417,f763]) ).
fof(f805,plain,
happens(push(agent8,trolley8),n0),
inference(resolution,[],[f417,f761]) ).
fof(f806,plain,
happens(push(agent9,trolley9),n0),
inference(resolution,[],[f417,f759]) ).
fof(f993,plain,
! [X2,X0,X1] :
( initiates(pull(X0,X1),spinning(X1),X2)
| ~ happens(push(X0,X1),X2) ),
inference(resolution,[],[f595,f505]) ).
fof(f1091,plain,
! [X2,X0,X1] :
( ~ happens(pull(X0,X1),X2)
| ~ happens(push(X0,X1),X2)
| holdsAt(spinning(X1),plus(X2,n1)) ),
inference(resolution,[],[f993,f340]) ).
fof(f1503,plain,
( ~ happens(push(agent1,trolley1),n0)
| holdsAt(spinning(trolley1),plus(n0,n1)) ),
inference(resolution,[],[f1091,f789]) ).
fof(f1504,plain,
( ~ happens(push(agent2,trolley2),n0)
| holdsAt(spinning(trolley2),plus(n0,n1)) ),
inference(resolution,[],[f1091,f790]) ).
fof(f1505,plain,
( ~ happens(push(agent3,trolley3),n0)
| holdsAt(spinning(trolley3),plus(n0,n1)) ),
inference(resolution,[],[f1091,f791]) ).
fof(f1506,plain,
( ~ happens(push(agent4,trolley4),n0)
| holdsAt(spinning(trolley4),plus(n0,n1)) ),
inference(resolution,[],[f1091,f792]) ).
fof(f1507,plain,
( ~ happens(push(agent5,trolley5),n0)
| holdsAt(spinning(trolley5),plus(n0,n1)) ),
inference(resolution,[],[f1091,f793]) ).
fof(f1508,plain,
( ~ happens(push(agent6,trolley6),n0)
| holdsAt(spinning(trolley6),plus(n0,n1)) ),
inference(resolution,[],[f1091,f794]) ).
fof(f1509,plain,
( ~ happens(push(agent7,trolley7),n0)
| holdsAt(spinning(trolley7),plus(n0,n1)) ),
inference(resolution,[],[f1091,f795]) ).
fof(f1510,plain,
( ~ happens(push(agent8,trolley8),n0)
| holdsAt(spinning(trolley8),plus(n0,n1)) ),
inference(resolution,[],[f1091,f796]) ).
fof(f1511,plain,
( ~ happens(push(agent9,trolley9),n0)
| holdsAt(spinning(trolley9),plus(n0,n1)) ),
inference(resolution,[],[f1091,f797]) ).
fof(f1512,plain,
holdsAt(spinning(trolley9),plus(n0,n1)),
inference(forward_subsumption_resolution,[],[f1511,f806]) ).
fof(f1513,plain,
holdsAt(spinning(trolley8),plus(n0,n1)),
inference(forward_subsumption_resolution,[],[f1510,f805]) ).
fof(f1514,plain,
holdsAt(spinning(trolley7),plus(n0,n1)),
inference(forward_subsumption_resolution,[],[f1509,f804]) ).
fof(f1515,plain,
holdsAt(spinning(trolley6),plus(n0,n1)),
inference(forward_subsumption_resolution,[],[f1508,f803]) ).
fof(f1516,plain,
holdsAt(spinning(trolley5),plus(n0,n1)),
inference(forward_subsumption_resolution,[],[f1507,f802]) ).
fof(f1517,plain,
holdsAt(spinning(trolley4),plus(n0,n1)),
inference(forward_subsumption_resolution,[],[f1506,f801]) ).
fof(f1518,plain,
holdsAt(spinning(trolley3),plus(n0,n1)),
inference(forward_subsumption_resolution,[],[f1505,f800]) ).
fof(f1519,plain,
holdsAt(spinning(trolley2),plus(n0,n1)),
inference(forward_subsumption_resolution,[],[f1504,f799]) ).
fof(f1520,plain,
holdsAt(spinning(trolley1),plus(n0,n1)),
inference(forward_subsumption_resolution,[],[f1503,f798]) ).
fof(f1521,plain,
holdsAt(spinning(trolley9),n1),
inference(forward_demodulation,[],[f1512,f331]) ).
fof(f1522,plain,
holdsAt(spinning(trolley8),n1),
inference(forward_demodulation,[],[f1513,f331]) ).
fof(f1523,plain,
holdsAt(spinning(trolley7),n1),
inference(forward_demodulation,[],[f1514,f331]) ).
fof(f1524,plain,
holdsAt(spinning(trolley6),n1),
inference(forward_demodulation,[],[f1515,f331]) ).
fof(f1525,plain,
holdsAt(spinning(trolley5),n1),
inference(forward_demodulation,[],[f1516,f331]) ).
fof(f1526,plain,
holdsAt(spinning(trolley4),n1),
inference(forward_demodulation,[],[f1517,f331]) ).
fof(f1527,plain,
holdsAt(spinning(trolley3),n1),
inference(forward_demodulation,[],[f1518,f331]) ).
fof(f1528,plain,
holdsAt(spinning(trolley2),n1),
inference(forward_demodulation,[],[f1519,f331]) ).
fof(f1529,plain,
holdsAt(spinning(trolley1),n1),
inference(forward_demodulation,[],[f1520,f331]) ).
fof(f1530,plain,
( $false
| spl44_1 ),
inference(forward_subsumption_resolution,[],[f1521,f625]) ).
fof(f1531,plain,
spl44_1,
inference(avatar_contradiction_clause,[],[f1530]) ).
fof(f1532,plain,
spl44_2,
inference(avatar_split_clause,[],[f1522,f627]) ).
fof(f1533,plain,
spl44_3,
inference(avatar_split_clause,[],[f1523,f631]) ).
fof(f1534,plain,
spl44_4,
inference(avatar_split_clause,[],[f1524,f635]) ).
fof(f1535,plain,
spl44_5,
inference(avatar_split_clause,[],[f1525,f639]) ).
fof(f1536,plain,
spl44_6,
inference(avatar_split_clause,[],[f1526,f643]) ).
fof(f1537,plain,
spl44_7,
inference(avatar_split_clause,[],[f1527,f647]) ).
fof(f1538,plain,
spl44_8,
inference(avatar_split_clause,[],[f1528,f651]) ).
fof(f1539,plain,
spl44_9,
inference(avatar_split_clause,[],[f1529,f655]) ).
cnf(s1,plain,
( ~ spl44_1
| ~ spl44_2
| ~ spl44_3
| ~ spl44_4
| ~ spl44_5
| ~ spl44_6
| ~ spl44_7
| ~ spl44_8
| ~ spl44_9 ),
inference(sat_conversion,[],[f658]) ).
cnf(s4,plain,
spl44_1,
inference(sat_conversion,[],[f1531]) ).
cnf(s5,plain,
spl44_2,
inference(sat_conversion,[],[f1532]) ).
cnf(s6,plain,
spl44_3,
inference(sat_conversion,[],[f1533]) ).
cnf(s7,plain,
spl44_4,
inference(sat_conversion,[],[f1534]) ).
cnf(s8,plain,
spl44_5,
inference(sat_conversion,[],[f1535]) ).
cnf(s9,plain,
spl44_6,
inference(sat_conversion,[],[f1536]) ).
cnf(s10,plain,
spl44_7,
inference(sat_conversion,[],[f1537]) ).
cnf(s11,plain,
spl44_8,
inference(sat_conversion,[],[f1538]) ).
cnf(s12,plain,
spl44_9,
inference(sat_conversion,[],[f1539]) ).
cnf(s14,plain,
$false,
inference(rat,[],[s1,s12,s11,s10,s9,s8,s7,s6,s5,s4]) ).
fof(f1540,plain,
$false,
inference(avatar_sat_refutation,[],[s14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR024+1.009 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n002.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 22:08:37 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.68/1.38 % (828916)Detected formulas, will run a generic FOF schedule.
% 4.68/1.38 % (829012)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3425510792:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.68/1.38 % (829014)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1518294675:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.68/1.38 % (829008)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4155684336:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.68/1.38 % (829011)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=200445964:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.68/1.38 % (829017)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1452055093:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.68/1.38 % (829020)dis-21_1_sil=8000:lcm=predicate:random_seed=3086743688:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.68/1.38 % (829018)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1801591470:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.68/1.38 % (829014)Refutation not found, incomplete strategy
% 4.68/1.38 % (829014)------------------------------
% 4.68/1.38 % (829014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.68/1.38 % (829014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.68/1.38 % (829014)CaDiCaL version: 2.1.3
% 4.68/1.38 % (829014)Termination reason: Refutation not found, incomplete strategy
% 4.68/1.38 % (829014)Time elapsed: 0.015 s
% 4.68/1.38 % (829014)Peak memory usage: 88 MB
% 4.68/1.38 % (829014)Instructions burned: 31 (million)
% 4.68/1.38 % (829020)Instruction limit reached!
% 4.68/1.38 % (829020)------------------------------
% 4.68/1.38 % (829020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.68/1.38 % (829020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.68/1.38 % (829020)CaDiCaL version: 2.1.3
% 4.68/1.38 % (829020)Termination reason: Instruction limit
% 4.68/1.38 % (829020)Termination phase: Saturation
% 4.68/1.38 % (829020)Time elapsed: 0.073 s
% 4.68/1.38 % (829020)Peak memory usage: 90 MB
% 4.68/1.38 % (829020)Instructions burned: 130 (million)
% 4.68/1.38 % (829017)Instruction limit reached!
% 4.68/1.38 % (829017)------------------------------
% 4.68/1.38 % (829017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.68/1.38 % (829017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.68/1.38 % (829017)CaDiCaL version: 2.1.3
% 4.68/1.38 % (829017)Termination reason: Instruction limit
% 4.68/1.38 % (829017)Termination phase: Saturation
% 4.68/1.38 % (829017)Time elapsed: 0.092 s
% 4.68/1.38 % (829017)Peak memory usage: 88 MB
% 4.68/1.38 % (829017)Instructions burned: 120 (million)
% 4.68/1.38 % (829018)Instruction limit reached!
% 4.68/1.38 % (829018)------------------------------
% 4.68/1.38 % (829018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.68/1.38 % (829018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.68/1.38 % (829018)CaDiCaL version: 2.1.3
% 4.68/1.38 % (829018)Termination reason: Instruction limit
% 4.68/1.38 % (829018)Termination phase: Saturation
% 4.68/1.38 % (829018)Time elapsed: 0.112 s
% 4.68/1.38 % (829018)Peak memory usage: 90 MB
% 4.68/1.38 % (829018)Instructions burned: 140 (million)
% 4.68/1.38 % (829076)lrs+10_1_sil=8000:sp=occurrence:random_seed=3250130611:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 4.68/1.38 % (829080)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3252897558:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.68/1.38 % (829014)------------------------------
% 4.68/1.38 % (829014)------------------------------
% 4.68/1.38 % (829080)Refutation not found, incomplete strategy
% 4.68/1.38 % (829080)------------------------------
% 4.68/1.38 % (829080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.68/1.38 % (829080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.68/1.38 % (829080)CaDiCaL version: 2.1.3
% 4.68/1.38 % (829080)Termination reason: Refutation not found, incomplete strategy
% 4.68/1.38 % (829080)Time elapsed: 0.003 s
% 4.68/1.38 % (829080)Peak memory usage: 88 MB
% 4.68/1.38 % (829080)Instructions burned: 3 (million)
% 4.68/1.38 % (829081)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3847467529:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 4.68/1.38 % (829076)First to succeed.
% 4.68/1.38 % (829076)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-828916"
% 4.68/1.38 % (829086)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=710086545:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 4.68/1.38 % (829081)Instruction limit reached!
% 4.68/1.38 % (829081)------------------------------
% 4.68/1.38 % (829081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.68/1.38 % (829081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.68/1.38 % (829081)CaDiCaL version: 2.1.3
% 4.68/1.38 % (829081)Termination reason: Instruction limit
% 4.68/1.38 % (829081)Termination phase: Saturation
% 4.68/1.38 % (829081)Time elapsed: 0.192 s
% 4.68/1.38 % (829081)Peak memory usage: 91 MB
% 4.68/1.38 % (829081)Instructions burned: 325 (million)
% 4.68/1.38 % (829080)------------------------------
% 4.68/1.38 % (829080)------------------------------
% 4.68/1.38 % (829076)Refutation found. Thanks to Tanya!
% 4.68/1.38 % SZS status Theorem for theBenchmark
% 4.68/1.38 % SZS output start Proof for theBenchmark
% See solution above
% 5.60/1.58 % (829076)------------------------------
% 5.60/1.58 % (829076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.58 % (829076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.58 % (829076)CaDiCaL version: 2.1.3
% 5.60/1.58 % (829076)Termination reason: Refutation
% 5.60/1.58 % (829076)Time elapsed: 0.035 s
% 5.60/1.58 % (829076)Peak memory usage: 90 MB
% 5.60/1.58 % (829076)Instructions burned: 59 (million)
% 5.60/1.58 % (829076)------------------------------
% 5.60/1.58 % (829076)------------------------------
% 5.60/1.58 % (828916)Success in time 0.71 s
% 5.60/1.58 % Vampire exiting
%------------------------------------------------------------------------------