%------------------------------------------------------------------------------
% File : Vampire-SAT---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/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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:44:21 AM UTC 2026
% Result : Theorem 1.38s 0.48s
% Output : Refutation 1.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 14
% Syntax : Number of formulae : 199 ( 53 unt; 9 def)
% Number of atoms : 482 ( 101 equ)
% Maximal formula atoms : 37 ( 2 avg)
% Number of connectives : 496 ( 213 ~; 230 |; 41 &)
% ( 11 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 10 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 20 con; 0-2 aty)
% Number of variables : 173 ( 0 sgn 171 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& initiates(X0,X2,X1) )
=> holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',happens_holds) ).
fof(f13,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/sandbox2/benchmark/Axioms/CSR001+3.ax',initiates_all_defn) ).
fof(f23,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',plus0_1) ).
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/sandbox2/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/sandbox2/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(f74,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f75,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(flattening,[],[f74]) ).
fof(f91,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(f100,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f75]) ).
fof(f118,plain,
! [X2,X3,X0,X1,X4] :
( ~ happens(push(X3,X4),X2)
| spinning(X4) != X1
| pull(X3,X4) != X0
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f13]) ).
fof(f159,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f23]) ).
fof(f241,plain,
! [X0,X1] :
( n0 != X1
| pull(agent1,trolley1) != X0
| sP36(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f244,plain,
! [X0,X1] :
( n0 != X1
| push(agent1,trolley1) != X0
| sP35(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f247,plain,
! [X0,X1] :
( n0 != X1
| pull(agent2,trolley2) != X0
| sP34(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f250,plain,
! [X0,X1] :
( n0 != X1
| push(agent2,trolley2) != X0
| sP33(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f253,plain,
! [X0,X1] :
( n0 != X1
| pull(agent3,trolley3) != X0
| sP32(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f256,plain,
! [X0,X1] :
( n0 != X1
| push(agent3,trolley3) != X0
| sP31(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f259,plain,
! [X0,X1] :
( n0 != X1
| pull(agent4,trolley4) != X0
| sP30(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f262,plain,
! [X0,X1] :
( n0 != X1
| push(agent4,trolley4) != X0
| sP29(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f265,plain,
! [X0,X1] :
( n0 != X1
| pull(agent5,trolley5) != X0
| sP28(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f268,plain,
! [X0,X1] :
( n0 != X1
| push(agent5,trolley5) != X0
| sP27(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f271,plain,
! [X0,X1] :
( n0 != X1
| pull(agent6,trolley6) != X0
| sP26(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f274,plain,
! [X0,X1] :
( n0 != X1
| push(agent6,trolley6) != X0
| sP25(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f277,plain,
! [X0,X1] :
( n0 != X1
| pull(agent7,trolley7) != X0
| sP24(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f280,plain,
! [X0,X1] :
( n0 != X1
| push(agent7,trolley7) != X0
| sP23(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f283,plain,
! [X0,X1] :
( n0 != X1
| pull(agent8,trolley8) != X0
| sP22(X1,X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f286,plain,
! [X0,X1] :
( n0 != X1
| push(agent8,trolley8) != X0
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f295,plain,
! [X0,X1] :
( n0 != X1
| pull(agent9,trolley9) != X0
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f296,plain,
! [X0,X1] :
( n0 != X1
| push(agent9,trolley9) != X0
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f297,plain,
! [X0,X1] :
( ~ sP22(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f298,plain,
! [X0,X1] :
( ~ sP23(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f299,plain,
! [X0,X1] :
( ~ sP24(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f300,plain,
! [X0,X1] :
( ~ sP25(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f301,plain,
! [X0,X1] :
( ~ sP26(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f302,plain,
! [X0,X1] :
( ~ sP27(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f303,plain,
! [X0,X1] :
( ~ sP28(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f304,plain,
! [X0,X1] :
( ~ sP29(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f305,plain,
! [X0,X1] :
( ~ sP30(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f306,plain,
! [X0,X1] :
( ~ sP31(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f307,plain,
! [X0,X1] :
( ~ sP32(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f308,plain,
! [X0,X1] :
( ~ sP33(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f309,plain,
! [X0,X1] :
( ~ sP34(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f310,plain,
! [X0,X1] :
( ~ sP35(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f311,plain,
! [X0,X1] :
( ~ sP36(X1,X0)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f418,plain,
( ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(cnf_transformation,[],[f91]) ).
fof(f419,plain,
! [X2,X3,X0,X4] :
( ~ happens(push(X3,X4),X2)
| pull(X3,X4) != X0
| initiates(X0,spinning(X4),X2) ),
inference(equality_resolution,[],[f118]) ).
fof(f420,plain,
! [X2,X3,X4] :
( ~ happens(push(X3,X4),X2)
| initiates(pull(X3,X4),spinning(X4),X2) ),
inference(equality_resolution,[],[f419]) ).
fof(f457,plain,
! [X0] :
( push(agent9,trolley9) != X0
| happens(X0,n0) ),
inference(equality_resolution,[],[f296]) ).
fof(f458,plain,
happens(push(agent9,trolley9),n0),
inference(equality_resolution,[],[f457]) ).
fof(f459,plain,
! [X0] :
( pull(agent9,trolley9) != X0
| happens(X0,n0) ),
inference(equality_resolution,[],[f295]) ).
fof(f460,plain,
happens(pull(agent9,trolley9),n0),
inference(equality_resolution,[],[f459]) ).
fof(f461,plain,
! [X0] :
( push(agent8,trolley8) != X0
| happens(X0,n0) ),
inference(equality_resolution,[],[f286]) ).
fof(f462,plain,
happens(push(agent8,trolley8),n0),
inference(equality_resolution,[],[f461]) ).
fof(f463,plain,
! [X0] :
( pull(agent8,trolley8) != X0
| sP22(n0,X0) ),
inference(equality_resolution,[],[f283]) ).
fof(f464,plain,
sP22(n0,pull(agent8,trolley8)),
inference(equality_resolution,[],[f463]) ).
fof(f465,plain,
! [X0] :
( push(agent7,trolley7) != X0
| sP23(n0,X0) ),
inference(equality_resolution,[],[f280]) ).
fof(f466,plain,
sP23(n0,push(agent7,trolley7)),
inference(equality_resolution,[],[f465]) ).
fof(f467,plain,
! [X0] :
( pull(agent7,trolley7) != X0
| sP24(n0,X0) ),
inference(equality_resolution,[],[f277]) ).
fof(f468,plain,
sP24(n0,pull(agent7,trolley7)),
inference(equality_resolution,[],[f467]) ).
fof(f469,plain,
! [X0] :
( push(agent6,trolley6) != X0
| sP25(n0,X0) ),
inference(equality_resolution,[],[f274]) ).
fof(f470,plain,
sP25(n0,push(agent6,trolley6)),
inference(equality_resolution,[],[f469]) ).
fof(f471,plain,
! [X0] :
( pull(agent6,trolley6) != X0
| sP26(n0,X0) ),
inference(equality_resolution,[],[f271]) ).
fof(f472,plain,
sP26(n0,pull(agent6,trolley6)),
inference(equality_resolution,[],[f471]) ).
fof(f473,plain,
! [X0] :
( push(agent5,trolley5) != X0
| sP27(n0,X0) ),
inference(equality_resolution,[],[f268]) ).
fof(f474,plain,
sP27(n0,push(agent5,trolley5)),
inference(equality_resolution,[],[f473]) ).
fof(f475,plain,
! [X0] :
( pull(agent5,trolley5) != X0
| sP28(n0,X0) ),
inference(equality_resolution,[],[f265]) ).
fof(f476,plain,
sP28(n0,pull(agent5,trolley5)),
inference(equality_resolution,[],[f475]) ).
fof(f477,plain,
! [X0] :
( push(agent4,trolley4) != X0
| sP29(n0,X0) ),
inference(equality_resolution,[],[f262]) ).
fof(f478,plain,
sP29(n0,push(agent4,trolley4)),
inference(equality_resolution,[],[f477]) ).
fof(f479,plain,
! [X0] :
( pull(agent4,trolley4) != X0
| sP30(n0,X0) ),
inference(equality_resolution,[],[f259]) ).
fof(f480,plain,
sP30(n0,pull(agent4,trolley4)),
inference(equality_resolution,[],[f479]) ).
fof(f481,plain,
! [X0] :
( push(agent3,trolley3) != X0
| sP31(n0,X0) ),
inference(equality_resolution,[],[f256]) ).
fof(f482,plain,
sP31(n0,push(agent3,trolley3)),
inference(equality_resolution,[],[f481]) ).
fof(f483,plain,
! [X0] :
( pull(agent3,trolley3) != X0
| sP32(n0,X0) ),
inference(equality_resolution,[],[f253]) ).
fof(f484,plain,
sP32(n0,pull(agent3,trolley3)),
inference(equality_resolution,[],[f483]) ).
fof(f485,plain,
! [X0] :
( push(agent2,trolley2) != X0
| sP33(n0,X0) ),
inference(equality_resolution,[],[f250]) ).
fof(f486,plain,
sP33(n0,push(agent2,trolley2)),
inference(equality_resolution,[],[f485]) ).
fof(f487,plain,
! [X0] :
( pull(agent2,trolley2) != X0
| sP34(n0,X0) ),
inference(equality_resolution,[],[f247]) ).
fof(f488,plain,
sP34(n0,pull(agent2,trolley2)),
inference(equality_resolution,[],[f487]) ).
fof(f489,plain,
! [X0] :
( push(agent1,trolley1) != X0
| sP35(n0,X0) ),
inference(equality_resolution,[],[f244]) ).
fof(f490,plain,
sP35(n0,push(agent1,trolley1)),
inference(equality_resolution,[],[f489]) ).
fof(f491,plain,
! [X0] :
( pull(agent1,trolley1) != X0
| sP36(n0,X0) ),
inference(equality_resolution,[],[f241]) ).
fof(f492,plain,
sP36(n0,pull(agent1,trolley1)),
inference(equality_resolution,[],[f491]) ).
fof(f501,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| happens(X0,X1)
| ~ holdsAt(X2,plus(X1,n1)) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f507,plain,
! [X2,X3,X4] :
( initiates(pull(X3,X4),spinning(X4),X2)
| happens(push(X3,X4),X2) ),
inference(consistent_polarity_flipping,[],[f420]) ).
fof(f606,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| sP36(X1,X0) ),
inference(consistent_polarity_flipping,[],[f311]) ).
fof(f607,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| sP35(X1,X0) ),
inference(consistent_polarity_flipping,[],[f310]) ).
fof(f608,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| sP34(X1,X0) ),
inference(consistent_polarity_flipping,[],[f309]) ).
fof(f609,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| ~ sP33(X1,X0) ),
inference(consistent_polarity_flipping,[],[f308]) ).
fof(f610,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| sP32(X1,X0) ),
inference(consistent_polarity_flipping,[],[f307]) ).
fof(f611,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| sP31(X1,X0) ),
inference(consistent_polarity_flipping,[],[f306]) ).
fof(f612,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| sP30(X1,X0) ),
inference(consistent_polarity_flipping,[],[f305]) ).
fof(f613,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| sP29(X1,X0) ),
inference(consistent_polarity_flipping,[],[f304]) ).
fof(f614,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| ~ sP28(X1,X0) ),
inference(consistent_polarity_flipping,[],[f303]) ).
fof(f615,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| sP27(X1,X0) ),
inference(consistent_polarity_flipping,[],[f302]) ).
fof(f616,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| sP26(X1,X0) ),
inference(consistent_polarity_flipping,[],[f301]) ).
fof(f617,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| ~ sP25(X1,X0) ),
inference(consistent_polarity_flipping,[],[f300]) ).
fof(f618,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| sP24(X1,X0) ),
inference(consistent_polarity_flipping,[],[f299]) ).
fof(f619,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| ~ sP23(X1,X0) ),
inference(consistent_polarity_flipping,[],[f298]) ).
fof(f620,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| ~ sP22(X1,X0) ),
inference(consistent_polarity_flipping,[],[f297]) ).
fof(f621,plain,
~ happens(push(agent9,trolley9),n0),
inference(consistent_polarity_flipping,[],[f458]) ).
fof(f622,plain,
~ happens(pull(agent9,trolley9),n0),
inference(consistent_polarity_flipping,[],[f460]) ).
fof(f631,plain,
~ happens(push(agent8,trolley8),n0),
inference(consistent_polarity_flipping,[],[f462]) ).
fof(f634,plain,
~ sP24(n0,pull(agent7,trolley7)),
inference(consistent_polarity_flipping,[],[f468]) ).
fof(f637,plain,
~ sP26(n0,pull(agent6,trolley6)),
inference(consistent_polarity_flipping,[],[f472]) ).
fof(f640,plain,
~ sP27(n0,push(agent5,trolley5)),
inference(consistent_polarity_flipping,[],[f474]) ).
fof(f643,plain,
~ sP29(n0,push(agent4,trolley4)),
inference(consistent_polarity_flipping,[],[f478]) ).
fof(f646,plain,
~ sP30(n0,pull(agent4,trolley4)),
inference(consistent_polarity_flipping,[],[f480]) ).
fof(f649,plain,
~ sP31(n0,push(agent3,trolley3)),
inference(consistent_polarity_flipping,[],[f482]) ).
fof(f652,plain,
~ sP32(n0,pull(agent3,trolley3)),
inference(consistent_polarity_flipping,[],[f484]) ).
fof(f655,plain,
~ sP34(n0,pull(agent2,trolley2)),
inference(consistent_polarity_flipping,[],[f488]) ).
fof(f658,plain,
~ sP35(n0,push(agent1,trolley1)),
inference(consistent_polarity_flipping,[],[f490]) ).
fof(f661,plain,
~ sP36(n0,pull(agent1,trolley1)),
inference(consistent_polarity_flipping,[],[f492]) ).
fof(f689,plain,
( holdsAt(spinning(trolley9),n1)
| holdsAt(spinning(trolley8),n1)
| holdsAt(spinning(trolley7),n1)
| holdsAt(spinning(trolley6),n1)
| holdsAt(spinning(trolley5),n1)
| holdsAt(spinning(trolley4),n1)
| holdsAt(spinning(trolley3),n1)
| holdsAt(spinning(trolley2),n1)
| holdsAt(spinning(trolley1),n1) ),
inference(consistent_polarity_flipping,[],[f418]) ).
fof(f691,definition,
( spl37_1
<=> holdsAt(spinning(trolley1),n1) ),
introduced(definition,[new_symbols(definition,[spl37_1])],[avatar_definition]) ).
fof(f693,plain,
( holdsAt(spinning(trolley1),n1)
| ~ spl37_1 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f695,definition,
( spl37_2
<=> holdsAt(spinning(trolley2),n1) ),
introduced(definition,[new_symbols(definition,[spl37_2])],[avatar_definition]) ).
fof(f697,plain,
( holdsAt(spinning(trolley2),n1)
| ~ spl37_2 ),
inference(avatar_component_clause,[],[f695]) ).
fof(f699,definition,
( spl37_3
<=> holdsAt(spinning(trolley3),n1) ),
introduced(definition,[new_symbols(definition,[spl37_3])],[avatar_definition]) ).
fof(f701,plain,
( holdsAt(spinning(trolley3),n1)
| ~ spl37_3 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f703,definition,
( spl37_4
<=> holdsAt(spinning(trolley4),n1) ),
introduced(definition,[new_symbols(definition,[spl37_4])],[avatar_definition]) ).
fof(f705,plain,
( holdsAt(spinning(trolley4),n1)
| ~ spl37_4 ),
inference(avatar_component_clause,[],[f703]) ).
fof(f707,definition,
( spl37_5
<=> holdsAt(spinning(trolley5),n1) ),
introduced(definition,[new_symbols(definition,[spl37_5])],[avatar_definition]) ).
fof(f709,plain,
( holdsAt(spinning(trolley5),n1)
| ~ spl37_5 ),
inference(avatar_component_clause,[],[f707]) ).
fof(f711,definition,
( spl37_6
<=> holdsAt(spinning(trolley6),n1) ),
introduced(definition,[new_symbols(definition,[spl37_6])],[avatar_definition]) ).
fof(f713,plain,
( holdsAt(spinning(trolley6),n1)
| ~ spl37_6 ),
inference(avatar_component_clause,[],[f711]) ).
fof(f715,definition,
( spl37_7
<=> holdsAt(spinning(trolley7),n1) ),
introduced(definition,[new_symbols(definition,[spl37_7])],[avatar_definition]) ).
fof(f717,plain,
( holdsAt(spinning(trolley7),n1)
| ~ spl37_7 ),
inference(avatar_component_clause,[],[f715]) ).
fof(f719,definition,
( spl37_8
<=> holdsAt(spinning(trolley8),n1) ),
introduced(definition,[new_symbols(definition,[spl37_8])],[avatar_definition]) ).
fof(f721,plain,
( holdsAt(spinning(trolley8),n1)
| ~ spl37_8 ),
inference(avatar_component_clause,[],[f719]) ).
fof(f723,definition,
( spl37_9
<=> holdsAt(spinning(trolley9),n1) ),
introduced(definition,[new_symbols(definition,[spl37_9])],[avatar_definition]) ).
fof(f725,plain,
( holdsAt(spinning(trolley9),n1)
| ~ spl37_9 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f726,plain,
( spl37_1
| spl37_2
| spl37_3
| spl37_4
| spl37_5
| spl37_6
| spl37_7
| spl37_8
| spl37_9 ),
inference(avatar_split_clause,[],[f689,f723,f719,f715,f711,f707,f703,f699,f695,f691]) ).
fof(f1094,plain,
! [X2,X0,X1] :
( ~ holdsAt(spinning(X1),plus(X2,n1))
| happens(pull(X0,X1),X2)
| happens(push(X0,X1),X2) ),
inference(resolution,[],[f507,f501]) ).
fof(f1736,plain,
! [X0,X1] :
( ~ holdsAt(spinning(X0),n1)
| happens(pull(X1,X0),n0)
| happens(push(X1,X0),n0) ),
inference(superposition,[],[f1094,f159]) ).
fof(f3023,plain,
( ! [X0] :
( happens(pull(X0,trolley2),n0)
| happens(push(X0,trolley2),n0) )
| ~ spl37_2 ),
inference(resolution,[],[f1736,f697]) ).
fof(f3057,plain,
( ! [X0] :
( sP34(n0,pull(X0,trolley2))
| happens(push(X0,trolley2),n0) )
| ~ spl37_2 ),
inference(resolution,[],[f3023,f608]) ).
fof(f3177,plain,
( happens(push(agent2,trolley2),n0)
| ~ spl37_2 ),
inference(resolution,[],[f3057,f655]) ).
fof(f3181,plain,
( ~ sP33(n0,push(agent2,trolley2))
| ~ spl37_2 ),
inference(resolution,[],[f3177,f609]) ).
fof(f3201,plain,
( $false
| ~ spl37_2 ),
inference(forward_subsumption_resolution,[],[f3181,f486]) ).
fof(f3202,plain,
~ spl37_2,
inference(avatar_contradiction_clause,[],[f3201]) ).
fof(f3203,plain,
( ! [X0] :
( happens(pull(X0,trolley3),n0)
| happens(push(X0,trolley3),n0) )
| ~ spl37_3 ),
inference(resolution,[],[f701,f1736]) ).
fof(f3328,plain,
( ! [X0] :
( sP32(n0,pull(X0,trolley3))
| happens(push(X0,trolley3),n0) )
| ~ spl37_3 ),
inference(resolution,[],[f3203,f610]) ).
fof(f3402,plain,
( happens(push(agent3,trolley3),n0)
| ~ spl37_3 ),
inference(resolution,[],[f3328,f652]) ).
fof(f3423,plain,
( sP31(n0,push(agent3,trolley3))
| ~ spl37_3 ),
inference(resolution,[],[f3402,f611]) ).
fof(f3441,plain,
( $false
| ~ spl37_3 ),
inference(forward_subsumption_resolution,[],[f3423,f649]) ).
fof(f3442,plain,
~ spl37_3,
inference(avatar_contradiction_clause,[],[f3441]) ).
fof(f3443,plain,
( ! [X0] :
( happens(pull(X0,trolley4),n0)
| happens(push(X0,trolley4),n0) )
| ~ spl37_4 ),
inference(resolution,[],[f705,f1736]) ).
fof(f3576,plain,
( ! [X0] :
( sP30(n0,pull(X0,trolley4))
| happens(push(X0,trolley4),n0) )
| ~ spl37_4 ),
inference(resolution,[],[f3443,f612]) ).
fof(f3797,plain,
( happens(push(agent4,trolley4),n0)
| ~ spl37_4 ),
inference(resolution,[],[f3576,f646]) ).
fof(f3911,plain,
( sP29(n0,push(agent4,trolley4))
| ~ spl37_4 ),
inference(resolution,[],[f3797,f613]) ).
fof(f3927,plain,
( $false
| ~ spl37_4 ),
inference(forward_subsumption_resolution,[],[f3911,f643]) ).
fof(f3928,plain,
~ spl37_4,
inference(avatar_contradiction_clause,[],[f3927]) ).
fof(f3929,plain,
( ! [X0] :
( happens(pull(X0,trolley5),n0)
| happens(push(X0,trolley5),n0) )
| ~ spl37_5 ),
inference(resolution,[],[f709,f1736]) ).
fof(f4007,plain,
( ! [X0] :
( ~ sP28(n0,pull(X0,trolley5))
| happens(push(X0,trolley5),n0) )
| ~ spl37_5 ),
inference(resolution,[],[f3929,f614]) ).
fof(f4333,plain,
( happens(push(agent5,trolley5),n0)
| ~ spl37_5 ),
inference(resolution,[],[f4007,f476]) ).
fof(f4343,plain,
( sP27(n0,push(agent5,trolley5))
| ~ spl37_5 ),
inference(resolution,[],[f4333,f615]) ).
fof(f4357,plain,
( $false
| ~ spl37_5 ),
inference(forward_subsumption_resolution,[],[f4343,f640]) ).
fof(f4358,plain,
~ spl37_5,
inference(avatar_contradiction_clause,[],[f4357]) ).
fof(f4359,plain,
( ! [X0] :
( happens(pull(X0,trolley6),n0)
| happens(push(X0,trolley6),n0) )
| ~ spl37_6 ),
inference(resolution,[],[f713,f1736]) ).
fof(f4472,plain,
( ! [X0] :
( sP26(n0,pull(X0,trolley6))
| happens(push(X0,trolley6),n0) )
| ~ spl37_6 ),
inference(resolution,[],[f4359,f616]) ).
fof(f4811,plain,
( happens(push(agent6,trolley6),n0)
| ~ spl37_6 ),
inference(resolution,[],[f4472,f637]) ).
fof(f4823,plain,
( ~ sP25(n0,push(agent6,trolley6))
| ~ spl37_6 ),
inference(resolution,[],[f4811,f617]) ).
fof(f4835,plain,
( $false
| ~ spl37_6 ),
inference(forward_subsumption_resolution,[],[f4823,f470]) ).
fof(f4836,plain,
~ spl37_6,
inference(avatar_contradiction_clause,[],[f4835]) ).
fof(f4837,plain,
( ! [X0] :
( happens(pull(X0,trolley7),n0)
| happens(push(X0,trolley7),n0) )
| ~ spl37_7 ),
inference(resolution,[],[f717,f1736]) ).
fof(f5012,plain,
( ! [X0] :
( sP24(n0,pull(X0,trolley7))
| happens(push(X0,trolley7),n0) )
| ~ spl37_7 ),
inference(resolution,[],[f4837,f618]) ).
fof(f5533,plain,
( happens(push(agent7,trolley7),n0)
| ~ spl37_7 ),
inference(resolution,[],[f5012,f634]) ).
fof(f5547,plain,
( ~ sP23(n0,push(agent7,trolley7))
| ~ spl37_7 ),
inference(resolution,[],[f5533,f619]) ).
fof(f5557,plain,
( $false
| ~ spl37_7 ),
inference(forward_subsumption_resolution,[],[f5547,f466]) ).
fof(f5558,plain,
~ spl37_7,
inference(avatar_contradiction_clause,[],[f5557]) ).
fof(f5559,plain,
( ! [X0] :
( happens(pull(X0,trolley8),n0)
| happens(push(X0,trolley8),n0) )
| ~ spl37_8 ),
inference(resolution,[],[f721,f1736]) ).
fof(f5577,plain,
( ! [X0] :
( ~ sP22(n0,pull(X0,trolley8))
| happens(push(X0,trolley8),n0) )
| ~ spl37_8 ),
inference(resolution,[],[f5559,f620]) ).
fof(f6384,plain,
( happens(push(agent8,trolley8),n0)
| ~ spl37_8 ),
inference(resolution,[],[f5577,f464]) ).
fof(f6385,plain,
( $false
| ~ spl37_8 ),
inference(forward_subsumption_resolution,[],[f6384,f631]) ).
fof(f6386,plain,
~ spl37_8,
inference(avatar_contradiction_clause,[],[f6385]) ).
fof(f6387,plain,
( ! [X0] :
( happens(pull(X0,trolley9),n0)
| happens(push(X0,trolley9),n0) )
| ~ spl37_9 ),
inference(resolution,[],[f725,f1736]) ).
fof(f6391,plain,
( happens(push(agent9,trolley9),n0)
| ~ spl37_9 ),
inference(resolution,[],[f6387,f622]) ).
fof(f6412,plain,
( $false
| ~ spl37_9 ),
inference(forward_subsumption_resolution,[],[f6391,f621]) ).
fof(f6413,plain,
~ spl37_9,
inference(avatar_contradiction_clause,[],[f6412]) ).
fof(f6414,plain,
( ! [X0] :
( happens(pull(X0,trolley1),n0)
| happens(push(X0,trolley1),n0) )
| ~ spl37_1 ),
inference(resolution,[],[f693,f1736]) ).
fof(f6418,plain,
( ! [X0] :
( sP36(n0,pull(X0,trolley1))
| happens(push(X0,trolley1),n0) )
| ~ spl37_1 ),
inference(resolution,[],[f6414,f606]) ).
fof(f6562,plain,
( happens(push(agent1,trolley1),n0)
| ~ spl37_1 ),
inference(resolution,[],[f6418,f661]) ).
fof(f6565,plain,
( sP35(n0,push(agent1,trolley1))
| ~ spl37_1 ),
inference(resolution,[],[f6562,f607]) ).
fof(f6587,plain,
( $false
| ~ spl37_1 ),
inference(forward_subsumption_resolution,[],[f6565,f658]) ).
fof(f6588,plain,
~ spl37_1,
inference(avatar_contradiction_clause,[],[f6587]) ).
cnf(s1,plain,
( spl37_1
| spl37_2
| spl37_3
| spl37_4
| spl37_5
| spl37_6
| spl37_7
| spl37_8
| spl37_9 ),
inference(sat_conversion,[],[f726]) ).
cnf(s52,plain,
~ spl37_2,
inference(sat_conversion,[],[f3202]) ).
cnf(s53,plain,
~ spl37_3,
inference(sat_conversion,[],[f3442]) ).
cnf(s62,plain,
~ spl37_4,
inference(sat_conversion,[],[f3928]) ).
cnf(s63,plain,
~ spl37_5,
inference(sat_conversion,[],[f4358]) ).
cnf(s74,plain,
~ spl37_6,
inference(sat_conversion,[],[f4836]) ).
cnf(s81,plain,
~ spl37_7,
inference(sat_conversion,[],[f5558]) ).
cnf(s94,plain,
~ spl37_8,
inference(sat_conversion,[],[f6386]) ).
cnf(s95,plain,
~ spl37_9,
inference(sat_conversion,[],[f6413]) ).
cnf(s96,plain,
~ spl37_1,
inference(sat_conversion,[],[f6588]) ).
cnf(s102,plain,
$false,
inference(rat,[],[s1,s95,s94,s81,s74,s63,s62,s53,s52,s96]) ).
fof(f6589,plain,
$false,
inference(avatar_sat_refutation,[],[s102]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR024+1.009 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n016.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 22:10:49 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.38/0.48 % (4090045)Will run a generic schedule for satisfiability detection.
% 1.38/0.48 % (4090054)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4068720071:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.38/0.48 % (4090051)% WARNING: option uhcvi not known.
% 1.38/0.48 % (4090050)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2273252545_2999 on theBenchmark for (2999ds/0Mi)
% 1.38/0.48 % (4090051)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1380698091:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.38/0.48 % (4090052)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2538611537:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.38/0.48 % (4090053)dis+10_1_sil=32000:sp=arity:random_seed=1374647832:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.38/0.48 % (4090055)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1541897914:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.38/0.48 % (4090056)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3312348212:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.38/0.48 % Detected minimum model sizes of [9]
% 1.38/0.48 % Detected maximum model sizes of [max]
% 1.38/0.48 % TRYING [9]
% 1.38/0.48 % (4090054)Instruction limit reached!
% 1.38/0.48 % (4090054)------------------------------
% 1.38/0.48 % (4090054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.48 % (4090054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.48 % (4090054)CaDiCaL version: 2.1.3
% 1.38/0.48 % (4090054)Termination reason: Instruction limit
% 1.38/0.48 % (4090054)Termination phase: Saturation
% 1.38/0.48 % (4090054)Time elapsed: 0.036 s
% 1.38/0.48 % (4090054)Peak memory usage: 13 MB
% 1.38/0.48 % (4090054)Instructions burned: 116 (million)
% 1.38/0.48 % (4090064)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2371686738:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.38/0.48 % Detected minimum model sizes of [9]
% 1.38/0.48 % Detected maximum model sizes of [max]
% 1.38/0.48 % TRYING [9]
% 1.38/0.48 % (4090053)Instruction limit reached!
% 1.38/0.48 % (4090053)------------------------------
% 1.38/0.48 % (4090053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.48 % (4090053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.48 % (4090053)CaDiCaL version: 2.1.3
% 1.38/0.48 % (4090053)Termination reason: Instruction limit
% 1.38/0.48 % (4090053)Termination phase: Saturation
% 1.38/0.48 % (4090053)Time elapsed: 0.058 s
% 1.38/0.48 % (4090053)Peak memory usage: 12 MB
% 1.38/0.48 % (4090053)Instructions burned: 103 (million)
% 1.38/0.48 % (4090056)Instruction limit reached!
% 1.38/0.48 % (4090056)------------------------------
% 1.38/0.48 % (4090056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.48 % (4090056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.48 % (4090056)CaDiCaL version: 2.1.3
% 1.38/0.48 % (4090056)Termination reason: Instruction limit
% 1.38/0.48 % (4090056)Termination phase: Saturation
% 1.38/0.48 % (4090056)Time elapsed: 0.072 s
% 1.38/0.48 % (4090056)Peak memory usage: 12 MB
% 1.38/0.48 % (4090056)Instructions burned: 159 (million)
% 1.38/0.48 % (4090055)Instruction limit reached!
% 1.38/0.48 % (4090055)------------------------------
% 1.38/0.48 % (4090055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.48 % (4090055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.48 % (4090055)CaDiCaL version: 2.1.3
% 1.38/0.48 % (4090055)Termination reason: Instruction limit
% 1.38/0.48 % (4090055)Termination phase: Saturation
% 1.38/0.48 % (4090055)Time elapsed: 0.076 s
% 1.38/0.48 % (4090055)Peak memory usage: 13 MB
% 1.38/0.48 % (4090055)Instructions burned: 132 (million)
% 1.38/0.48 % (4090066)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=686302231:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.38/0.48 % (4090067)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2432423886:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.38/0.48 % (4090068)ott-21_1_sil=16000:fs=off:random_seed=1670672025:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.38/0.48 % (4090066)Instruction limit reached!
% 1.38/0.48 % (4090066)------------------------------
% 1.38/0.48 % (4090066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.48 % (4090066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.48 % (4090066)CaDiCaL version: 2.1.3
% 1.38/0.48 % (4090066)Termination reason: Instruction limit
% 1.38/0.48 % (4090066)Termination phase: Saturation
% 1.38/0.48 % (4090066)Time elapsed: 0.076 s
% 1.38/0.48 % (4090066)Peak memory usage: 13 MB
% 1.38/0.48 % (4090066)Instructions burned: 132 (million)
% 1.38/0.48 % (4090064)Instruction limit reached!
% 1.38/0.48 % (4090064)------------------------------
% 1.38/0.48 % (4090064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.48 % (4090064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.48 % (4090064)CaDiCaL version: 2.1.3
% 1.38/0.48 % (4090064)Termination reason: Instruction limit
% 1.38/0.48 % (4090064)Termination phase: Finite model building constraint generation
% 1.38/0.48 % (4090064)Time elapsed: 0.128 s
% 1.38/0.48 % (4090064)Peak memory usage: 42 MB
% 1.38/0.48 % (4090064)Instructions burned: 717 (million)
% 1.38/0.48 % (4090072)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4125596001:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.38/0.48 % (4090073)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=257089330:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.38/0.48 % (4090068)Instruction limit reached!
% 1.38/0.48 % (4090068)------------------------------
% 1.38/0.48 % (4090068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.48 % (4090068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.48 % (4090068)CaDiCaL version: 2.1.3
% 1.38/0.48 % (4090068)Termination reason: Instruction limit
% 1.38/0.48 % (4090068)Termination phase: Saturation
% 1.38/0.48 % (4090068)Time elapsed: 0.092 s
% 1.38/0.48 % (4090068)Peak memory usage: 13 MB
% 1.38/0.48 % (4090068)Instructions burned: 180 (million)
% 1.38/0.48 % Detected minimum model sizes of [9]
% 1.38/0.48 % Detected maximum model sizes of [max]
% 1.38/0.48 % (4090051) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4090045-4090051"...
% 1.38/0.48 % (4090076)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=623381458:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.38/0.48 % (4090051)...printing done.
% 1.38/0.48 % (4090051)Refutation found. Thanks to Tanya!
% 1.38/0.48 % SZS status Theorem for theBenchmark
% 1.38/0.48 % SZS output start Proof for theBenchmark
% See solution above
% 1.38/0.49 % (4090051)------------------------------
% 1.38/0.49 % (4090051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.49 % (4090051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.49 % (4090051)CaDiCaL version: 2.1.3
% 1.38/0.49 % (4090051)Termination reason: Refutation
% 1.38/0.49 % (4090051)Time elapsed: 0.209 s
% 1.38/0.49 % (4090051)Peak memory usage: 15 MB
% 1.38/0.49 % (4090051)Instructions burned: 376 (million)
% 1.38/0.49 % (4090045)Success in time 0.255 s
% 1.38/0.49 % Vampire exiting
%------------------------------------------------------------------------------