%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR084+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:42:47 AM UTC 2026
% Result : Theorem 7.81s 3.53s
% Output : Refutation 14.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 17
% Syntax : Number of formulae : 94 ( 29 unt; 4 def)
% Number of atoms : 263 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 308 ( 139 ~; 135 |; 20 &)
% ( 6 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 5 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 9 con; 0-1 aty)
% Number of variables : 65 ( 0 sgn 61 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26456,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_26635) ).
fof(f26457,axiom,
! [X0,X1,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__instance(X2,X0) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_26636) ).
fof(f27193,axiom,
! [X0] :
( s__instance(X0,s__SetOrClass)
=> ( s__instance(X0,s__Class)
<=> s__subclass(X0,s__Entity) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_27373) ).
fof(f34847,axiom,
s__partition_3(s__Animal,s__Vertebrate,s__Invertebrate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_35100) ).
fof(f93544,axiom,
s__subclass(s__Vertebrate,s__Entity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_37958) ).
fof(f98697,axiom,
s__subclass(s__Animal,s__Object),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_43111) ).
fof(f98698,axiom,
s__subclass(s__Animal,s__Entity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_43112) ).
fof(f107634,axiom,
s__subclass(s__Invertebrate,s__Entity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_52048) ).
fof(f145102,axiom,
! [X0] :
( s__instance(X0,s__Object)
=> ( ( s__instance(X0,s__Animal)
& ~ ? [X1] :
( s__instance(X1,s__Object)
& s__instance(X1,s__SpinalColumn)
& s__part(X1,X0) ) )
=> ~ s__instance(X0,s__Vertebrate) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1) ).
fof(f145103,axiom,
~ ? [X0] :
( s__instance(X0,s__Object)
& s__instance(X0,s__SpinalColumn)
& s__part(X0,s__BananaSlug10_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_2) ).
fof(f145106,axiom,
! [X0,X1,X2,X3] :
( ( s__instance(X0,s__Class)
& s__instance(X1,s__Class)
& s__instance(X2,s__Class) )
=> ( ( s__partition_3(X0,X1,X2)
& s__instance(X3,X0)
& ~ s__instance(X3,X1) )
=> s__instance(X3,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_5) ).
fof(f145107,axiom,
s__instance(s__BananaSlug10_1,s__Animal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_6) ).
fof(f145109,conjecture,
s__instance(s__BananaSlug10_1,s__Invertebrate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_ALL) ).
fof(f145110,negated_conjecture,
~ s__instance(s__BananaSlug10_1,s__Invertebrate),
inference(negated_conjecture,[status(cth)],[f145109]) ).
fof(f145111,plain,
~ s__instance(s__BananaSlug10_1,s__Invertebrate),
inference(flattening,[],[f145110]) ).
fof(f145118,plain,
! [X0] :
( ~ s__instance(X0,s__Object)
| ~ s__instance(X0,s__SpinalColumn)
| ~ s__part(X0,s__BananaSlug10_1) ),
inference(ennf_transformation,[],[f145103]) ).
fof(f145119,plain,
! [X0,X1,X2,X3] :
( s__instance(X3,X2)
| ~ s__partition_3(X0,X1,X2)
| ~ s__instance(X3,X0)
| s__instance(X3,X1)
| ~ s__instance(X0,s__Class)
| ~ s__instance(X1,s__Class)
| ~ s__instance(X2,s__Class) ),
inference(ennf_transformation,[],[f145106]) ).
fof(f145120,plain,
! [X0,X1,X2,X3] :
( s__instance(X3,X2)
| ~ s__partition_3(X0,X1,X2)
| ~ s__instance(X3,X0)
| s__instance(X3,X1)
| ~ s__instance(X0,s__Class)
| ~ s__instance(X1,s__Class)
| ~ s__instance(X2,s__Class) ),
inference(flattening,[],[f145119]) ).
fof(f145141,plain,
! [X0] :
( ~ s__instance(X0,s__Vertebrate)
| ~ s__instance(X0,s__Animal)
| ? [X1] :
( s__instance(X1,s__Object)
& s__instance(X1,s__SpinalColumn)
& s__part(X1,X0) )
| ~ s__instance(X0,s__Object) ),
inference(ennf_transformation,[],[f145102]) ).
fof(f145142,plain,
! [X0] :
( ~ s__instance(X0,s__Vertebrate)
| ~ s__instance(X0,s__Animal)
| ? [X1] :
( s__instance(X1,s__Object)
& s__instance(X1,s__SpinalColumn)
& s__part(X1,X0) )
| ~ s__instance(X0,s__Object) ),
inference(flattening,[],[f145141]) ).
fof(f145144,plain,
! [X0] :
( ( s__instance(X0,s__Class)
<=> s__subclass(X0,s__Entity) )
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f27193]) ).
fof(f145186,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f26457]) ).
fof(f145187,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f145186]) ).
fof(f145188,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26456]) ).
fof(f145314,plain,
! [X0] :
( ~ s__instance(X0,s__Vertebrate)
| ~ s__instance(X0,s__Animal)
| ( s__instance(sK2(X0),s__Object)
& s__instance(sK2(X0),s__SpinalColumn)
& s__part(sK2(X0),X0) )
| ~ s__instance(X0,s__Object) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X1,sK2(X0))],[f145142]) ).
fof(f145318,plain,
! [X0] :
( ( ( s__instance(X0,s__Class)
| ~ s__subclass(X0,s__Entity) )
& ( s__subclass(X0,s__Entity)
| ~ s__instance(X0,s__Class) ) )
| ~ s__instance(X0,s__SetOrClass) ),
inference(nnf_transformation,[],[f145144]) ).
fof(f145330,plain,
~ s__instance(s__BananaSlug10_1,s__Invertebrate),
inference(cnf_transformation,[],[f145111]) ).
fof(f145332,plain,
s__subclass(s__Invertebrate,s__Entity),
inference(cnf_transformation,[],[f107634]) ).
fof(f145342,plain,
s__partition_3(s__Animal,s__Vertebrate,s__Invertebrate),
inference(cnf_transformation,[],[f34847]) ).
fof(f145345,plain,
s__instance(s__BananaSlug10_1,s__Animal),
inference(cnf_transformation,[],[f145107]) ).
fof(f145346,plain,
! [X0] :
( ~ s__part(X0,s__BananaSlug10_1)
| ~ s__instance(X0,s__SpinalColumn)
| ~ s__instance(X0,s__Object) ),
inference(cnf_transformation,[],[f145118]) ).
fof(f145348,plain,
s__subclass(s__Animal,s__Entity),
inference(cnf_transformation,[],[f98698]) ).
fof(f145349,plain,
s__subclass(s__Animal,s__Object),
inference(cnf_transformation,[],[f98697]) ).
fof(f145357,plain,
! [X2,X3,X0,X1] :
( ~ s__partition_3(X0,X1,X2)
| s__instance(X3,X2)
| ~ s__instance(X3,X0)
| s__instance(X3,X1)
| ~ s__instance(X0,s__Class)
| ~ s__instance(X1,s__Class)
| ~ s__instance(X2,s__Class) ),
inference(cnf_transformation,[],[f145120]) ).
fof(f145375,plain,
s__subclass(s__Vertebrate,s__Entity),
inference(cnf_transformation,[],[f93544]) ).
fof(f145448,plain,
! [X0] :
( s__part(sK2(X0),X0)
| ~ s__instance(X0,s__Animal)
| ~ s__instance(X0,s__Vertebrate)
| ~ s__instance(X0,s__Object) ),
inference(cnf_transformation,[],[f145314]) ).
fof(f145449,plain,
! [X0] :
( s__instance(sK2(X0),s__SpinalColumn)
| ~ s__instance(X0,s__Animal)
| ~ s__instance(X0,s__Vertebrate)
| ~ s__instance(X0,s__Object) ),
inference(cnf_transformation,[],[f145314]) ).
fof(f145450,plain,
! [X0] :
( s__instance(sK2(X0),s__Object)
| ~ s__instance(X0,s__Animal)
| ~ s__instance(X0,s__Vertebrate)
| ~ s__instance(X0,s__Object) ),
inference(cnf_transformation,[],[f145314]) ).
fof(f145477,plain,
! [X0] :
( s__instance(X0,s__Class)
| ~ s__subclass(X0,s__Entity)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f145318]) ).
fof(f145696,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f145187]) ).
fof(f145697,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f145188]) ).
fof(f145698,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f145188]) ).
fof(f146170,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f145696,f145697]) ).
fof(f146172,plain,
! [X0] :
( ~ s__subclass(X0,s__Entity)
| s__instance(X0,s__Class) ),
inference(forward_subsumption_resolution,[],[f145477,f145698]) ).
fof(f146174,plain,
! [X2,X0,X1] :
( ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| s__instance(X2,X1) ),
inference(forward_subsumption_resolution,[],[f146170,f145698]) ).
fof(f147078,plain,
s__instance(s__Animal,s__Class),
inference(resolution,[],[f146172,f145348]) ).
fof(f147134,plain,
s__instance(s__Invertebrate,s__Class),
inference(resolution,[],[f146172,f145332]) ).
fof(f147145,plain,
s__instance(s__Vertebrate,s__Class),
inference(resolution,[],[f146172,f145375]) ).
fof(f147284,plain,
! [X0] :
( ~ s__subclass(s__Animal,X0)
| s__instance(s__BananaSlug10_1,X0) ),
inference(resolution,[],[f146174,f145345]) ).
fof(f147741,definition,
( spl11_2
<=> s__instance(s__BananaSlug10_1,s__Object) ),
introduced(definition,[new_symbols(definition,[spl11_2])],[avatar_definition]) ).
fof(f147742,plain,
( s__instance(s__BananaSlug10_1,s__Object)
| ~ spl11_2 ),
inference(avatar_component_clause,[],[f147741]) ).
fof(f147743,plain,
( ~ s__instance(s__BananaSlug10_1,s__Object)
| spl11_2 ),
inference(avatar_component_clause,[],[f147741]) ).
fof(f148157,plain,
( ~ s__instance(s__BananaSlug10_1,s__Animal)
| ~ s__instance(s__BananaSlug10_1,s__Vertebrate)
| ~ s__instance(s__BananaSlug10_1,s__Object)
| ~ s__instance(sK2(s__BananaSlug10_1),s__SpinalColumn)
| ~ s__instance(sK2(s__BananaSlug10_1),s__Object) ),
inference(resolution,[],[f145448,f145346]) ).
fof(f150328,plain,
! [X0] :
( s__instance(X0,s__Invertebrate)
| ~ s__instance(X0,s__Animal)
| s__instance(X0,s__Vertebrate)
| ~ s__instance(s__Animal,s__Class)
| ~ s__instance(s__Vertebrate,s__Class)
| ~ s__instance(s__Invertebrate,s__Class) ),
inference(resolution,[],[f145357,f145342]) ).
fof(f150354,plain,
! [X0] :
( s__instance(X0,s__Invertebrate)
| ~ s__instance(X0,s__Animal)
| s__instance(X0,s__Vertebrate)
| ~ s__instance(s__Vertebrate,s__Class)
| ~ s__instance(s__Invertebrate,s__Class) ),
inference(forward_subsumption_resolution,[],[f150328,f147078]) ).
fof(f150368,plain,
! [X0] :
( s__instance(X0,s__Invertebrate)
| ~ s__instance(X0,s__Animal)
| s__instance(X0,s__Vertebrate)
| ~ s__instance(s__Invertebrate,s__Class) ),
inference(forward_subsumption_resolution,[],[f150354,f147145]) ).
fof(f150382,plain,
! [X0] :
( ~ s__instance(X0,s__Animal)
| s__instance(X0,s__Invertebrate)
| s__instance(X0,s__Vertebrate) ),
inference(forward_subsumption_resolution,[],[f150368,f147134]) ).
fof(f151588,plain,
s__instance(s__BananaSlug10_1,s__Object),
inference(resolution,[],[f147284,f145349]) ).
fof(f151595,plain,
( $false
| spl11_2 ),
inference(forward_subsumption_resolution,[],[f151588,f147743]) ).
fof(f151596,plain,
spl11_2,
inference(avatar_contradiction_clause,[],[f151595]) ).
fof(f151597,plain,
( ~ s__instance(s__BananaSlug10_1,s__Vertebrate)
| ~ s__instance(s__BananaSlug10_1,s__Object)
| ~ s__instance(sK2(s__BananaSlug10_1),s__SpinalColumn)
| ~ s__instance(sK2(s__BananaSlug10_1),s__Object) ),
inference(forward_subsumption_resolution,[],[f148157,f145345]) ).
fof(f151600,plain,
( ~ s__instance(s__BananaSlug10_1,s__Vertebrate)
| ~ s__instance(sK2(s__BananaSlug10_1),s__SpinalColumn)
| ~ s__instance(sK2(s__BananaSlug10_1),s__Object)
| ~ spl11_2 ),
inference(forward_subsumption_resolution,[],[f151597,f147742]) ).
fof(f151602,definition,
( spl11_171
<=> s__instance(sK2(s__BananaSlug10_1),s__Object) ),
introduced(definition,[new_symbols(definition,[spl11_171])],[avatar_definition]) ).
fof(f151604,plain,
( ~ s__instance(sK2(s__BananaSlug10_1),s__Object)
| spl11_171 ),
inference(avatar_component_clause,[],[f151602]) ).
fof(f151606,definition,
( spl11_172
<=> s__instance(sK2(s__BananaSlug10_1),s__SpinalColumn) ),
introduced(definition,[new_symbols(definition,[spl11_172])],[avatar_definition]) ).
fof(f151608,plain,
( ~ s__instance(sK2(s__BananaSlug10_1),s__SpinalColumn)
| spl11_172 ),
inference(avatar_component_clause,[],[f151606]) ).
fof(f151610,definition,
( spl11_173
<=> s__instance(s__BananaSlug10_1,s__Vertebrate) ),
introduced(definition,[new_symbols(definition,[spl11_173])],[avatar_definition]) ).
fof(f151611,plain,
( s__instance(s__BananaSlug10_1,s__Vertebrate)
| ~ spl11_173 ),
inference(avatar_component_clause,[],[f151610]) ).
fof(f151612,plain,
( ~ s__instance(s__BananaSlug10_1,s__Vertebrate)
| spl11_173 ),
inference(avatar_component_clause,[],[f151610]) ).
fof(f151613,plain,
( ~ spl11_171
| ~ spl11_172
| ~ spl11_173
| ~ spl11_2 ),
inference(avatar_split_clause,[],[f151600,f147741,f151610,f151606,f151602]) ).
fof(f151618,plain,
( ~ s__instance(s__BananaSlug10_1,s__Animal)
| ~ s__instance(s__BananaSlug10_1,s__Vertebrate)
| ~ s__instance(s__BananaSlug10_1,s__Object)
| spl11_171 ),
inference(resolution,[],[f151604,f145450]) ).
fof(f151619,plain,
( ~ s__instance(s__BananaSlug10_1,s__Vertebrate)
| ~ s__instance(s__BananaSlug10_1,s__Object)
| spl11_171 ),
inference(forward_subsumption_resolution,[],[f151618,f145345]) ).
fof(f151620,plain,
( ~ s__instance(s__BananaSlug10_1,s__Vertebrate)
| ~ spl11_2
| spl11_171 ),
inference(forward_subsumption_resolution,[],[f151619,f147742]) ).
fof(f151621,plain,
( ~ spl11_173
| ~ spl11_2
| spl11_171 ),
inference(avatar_split_clause,[],[f151620,f151602,f147741,f151610]) ).
fof(f154905,plain,
( s__instance(s__BananaSlug10_1,s__Invertebrate)
| s__instance(s__BananaSlug10_1,s__Vertebrate) ),
inference(resolution,[],[f150382,f145345]) ).
fof(f154906,plain,
s__instance(s__BananaSlug10_1,s__Vertebrate),
inference(forward_subsumption_resolution,[],[f154905,f145330]) ).
fof(f154907,plain,
( $false
| spl11_173 ),
inference(forward_subsumption_resolution,[],[f154906,f151612]) ).
fof(f154908,plain,
spl11_173,
inference(avatar_contradiction_clause,[],[f154907]) ).
fof(f154916,plain,
( ~ s__instance(s__BananaSlug10_1,s__Animal)
| ~ s__instance(s__BananaSlug10_1,s__Vertebrate)
| ~ s__instance(s__BananaSlug10_1,s__Object)
| spl11_172 ),
inference(resolution,[],[f151608,f145449]) ).
fof(f154917,plain,
( ~ s__instance(s__BananaSlug10_1,s__Vertebrate)
| ~ s__instance(s__BananaSlug10_1,s__Object)
| spl11_172 ),
inference(forward_subsumption_resolution,[],[f154916,f145345]) ).
fof(f154918,plain,
( ~ s__instance(s__BananaSlug10_1,s__Object)
| spl11_172
| ~ spl11_173 ),
inference(forward_subsumption_resolution,[],[f154917,f151611]) ).
fof(f154919,plain,
( $false
| ~ spl11_2
| spl11_172
| ~ spl11_173 ),
inference(forward_subsumption_resolution,[],[f154918,f147742]) ).
fof(f154920,plain,
( ~ spl11_2
| spl11_172
| ~ spl11_173 ),
inference(avatar_contradiction_clause,[],[f154919]) ).
cnf(s112,plain,
spl11_2,
inference(sat_conversion,[],[f151596]) ).
cnf(s113,plain,
( ~ spl11_2
| ~ spl11_171
| ~ spl11_172
| ~ spl11_173 ),
inference(sat_conversion,[],[f151613]) ).
cnf(s114,plain,
( ~ spl11_2
| spl11_171
| ~ spl11_173 ),
inference(sat_conversion,[],[f151621]) ).
cnf(s235,plain,
spl11_173,
inference(sat_conversion,[],[f154908]) ).
cnf(s236,plain,
( ~ spl11_2
| spl11_172
| ~ spl11_173 ),
inference(sat_conversion,[],[f154920]) ).
cnf(s246,plain,
( ~ spl11_2
| spl11_171 ),
inference(rat,[],[s114,s235]) ).
cnf(s247,plain,
( ~ spl11_2
| ~ spl11_171
| ~ spl11_172 ),
inference(rat,[],[s113,s235]) ).
cnf(s248,plain,
spl11_172,
inference(rat,[],[s236,s235,s112]) ).
cnf(s249,plain,
spl11_171,
inference(rat,[],[s246,s112]) ).
cnf(s250,plain,
$false,
inference(rat,[],[s247,s248,s249,s112]) ).
fof(f154921,plain,
$false,
inference(avatar_sat_refutation,[],[s250]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR084+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 22:33:04 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.13 Running first-order theorem proving
% 0.09/0.13 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
% 7.81/3.53 % (3869610)Detected formulas, will run a generic FOF schedule.
% 7.81/3.53 % (3869700)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=3116432818:i=141695:sd=1:nm=32:gsp=on:ss=included_2986 on theBenchmark for (2986ds/141695Mi)
% 7.81/3.53 % (3869699)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=3482752021:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2986 on theBenchmark for (2986ds/134677Mi)
% 7.81/3.53 % (3869701)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3959506218:i=109:sd=1:ins=1:gsp=on:ss=axioms_2986 on theBenchmark for (2986ds/109Mi)
% 7.81/3.53 % (3869697)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=3556463928:i=141193_2986 on theBenchmark for (2986ds/141193Mi)
% 7.81/3.53 % (3869704)dis-21_1_sil=8000:lcm=predicate:random_seed=2326001011:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2986 on theBenchmark for (2986ds/129Mi)
% 7.81/3.53 % (3869702)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=983997969:i=119:av=off:ss=axioms_2986 on theBenchmark for (2986ds/119Mi)
% 7.81/3.53 % (3869703)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4183794843:s2a=on:i=139:gtg=position_2986 on theBenchmark for (2986ds/139Mi)
% 7.81/3.53 % (3869701)Instruction limit reached!
% 7.81/3.53 % (3869701)------------------------------
% 7.81/3.53 % (3869701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869701)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869701)Termination reason: Instruction limit
% 7.81/3.53 % (3869701)Termination phase: SInE selection
% 7.81/3.53 % (3869701)Time elapsed: 0.056 s
% 7.81/3.53 % (3869701)Peak memory usage: 164 MB
% 7.81/3.53 % (3869701)Instructions burned: 111 (million)
% 7.81/3.53 % (3869704)Instruction limit reached!
% 7.81/3.53 % (3869704)------------------------------
% 7.81/3.53 % (3869704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869704)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869704)Termination reason: Instruction limit
% 7.81/3.53 % (3869704)Termination phase: SInE selection
% 7.81/3.53 % (3869704)Time elapsed: 0.061 s
% 7.81/3.53 % (3869704)Peak memory usage: 164 MB
% 7.81/3.53 % (3869704)Instructions burned: 130 (million)
% 7.81/3.53 % (3869702)Instruction limit reached!
% 7.81/3.53 % (3869702)------------------------------
% 7.81/3.53 % (3869702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869702)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869702)Termination reason: Instruction limit
% 7.81/3.53 % (3869702)Termination phase: SInE selection
% 7.81/3.53 % (3869702)Time elapsed: 0.064 s
% 7.81/3.53 % (3869702)Peak memory usage: 164 MB
% 7.81/3.53 % (3869702)Instructions burned: 121 (million)
% 7.81/3.53 % (3869703)Instruction limit reached!
% 7.81/3.53 % (3869703)------------------------------
% 7.81/3.53 % (3869703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869703)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869703)Termination reason: Instruction limit
% 7.81/3.53 % (3869703)Termination phase: Property scanning
% 7.81/3.53 % (3869703)Time elapsed: 0.075 s
% 7.81/3.53 % (3869703)Peak memory usage: 165 MB
% 7.81/3.53 % (3869703)Instructions burned: 139 (million)
% 7.81/3.53 % (3869716)lrs+10_1_sil=8000:sp=occurrence:random_seed=1504520533:i=285:sd=3:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/285Mi)
% 7.81/3.53 % (3869719)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2729274516:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/157Mi)
% 7.81/3.53 % (3869720)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3167441957:i=325:sd=1:ss=axioms:sgt=32_2983 on theBenchmark for (2983ds/325Mi)
% 7.81/3.53 % (3869721)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=744691298:s2a=on:i=248:s2at=1.23:gtg=position_2983 on theBenchmark for (2983ds/248Mi)
% 7.81/3.53 % (3869719)Instruction limit reached!
% 7.81/3.53 % (3869719)------------------------------
% 7.81/3.53 % (3869719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869719)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869719)Termination reason: Instruction limit
% 7.81/3.53 % (3869719)Termination phase: Property scanning
% 7.81/3.53 % (3869719)Time elapsed: 0.081 s
% 7.81/3.53 % (3869719)Peak memory usage: 165 MB
% 7.81/3.53 % (3869719)Instructions burned: 157 (million)
% 7.81/3.53 % (3869716)Instruction limit reached!
% 7.81/3.53 % (3869716)------------------------------
% 7.81/3.53 % (3869716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869716)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869716)Termination reason: Instruction limit
% 7.81/3.53 % (3869716)Termination phase: SInE selection
% 7.81/3.53 % (3869716)Time elapsed: 0.129 s
% 7.81/3.53 % (3869716)Peak memory usage: 164 MB
% 7.81/3.53 % (3869716)Instructions burned: 289 (million)
% 7.81/3.53 % (3869721)Instruction limit reached!
% 7.81/3.53 % (3869721)------------------------------
% 7.81/3.53 % (3869721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869721)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869721)Termination reason: Instruction limit
% 7.81/3.53 % (3869721)Termination phase: Property scanning
% 7.81/3.53 % (3869721)Time elapsed: 0.108 s
% 7.81/3.53 % (3869721)Peak memory usage: 165 MB
% 7.81/3.53 % (3869721)Instructions burned: 250 (million)
% 7.81/3.53 % (3869720)Instruction limit reached!
% 7.81/3.53 % (3869720)------------------------------
% 7.81/3.53 % (3869720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869720)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869720)Termination reason: Instruction limit
% 7.81/3.53 % (3869720)Termination phase: SInE selection
% 7.81/3.53 % (3869720)Time elapsed: 0.127 s
% 7.81/3.53 % (3869720)Peak memory usage: 165 MB
% 7.81/3.53 % (3869720)Instructions burned: 327 (million)
% 7.81/3.53 % (3869728)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3691099695:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2980 on theBenchmark for (2980ds/294Mi)
% 7.81/3.53 % (3869732)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1540462834:cts=off:i=113:fsr=off:ss=included:sgt=4_2980 on theBenchmark for (2980ds/113Mi)
% 7.81/3.53 % (3869733)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4294918605:i=127:av=off:fsr=off:sup=off_2980 on theBenchmark for (2980ds/127Mi)
% 7.81/3.53 % (3869731)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2529665019:i=2350_2980 on theBenchmark for (2980ds/2350Mi)
% 7.81/3.53 % (3869732)Instruction limit reached!
% 7.81/3.53 % (3869732)------------------------------
% 7.81/3.53 % (3869732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869732)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869732)Termination reason: Instruction limit
% 7.81/3.53 % (3869732)Termination phase: SInE selection
% 7.81/3.53 % (3869732)Time elapsed: 0.057 s
% 7.81/3.53 % (3869732)Peak memory usage: 164 MB
% 7.81/3.53 % (3869732)Instructions burned: 115 (million)
% 7.81/3.53 % (3869733)Instruction limit reached!
% 7.81/3.53 % (3869733)------------------------------
% 7.81/3.53 % (3869733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869733)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869733)Termination reason: Instruction limit
% 7.81/3.53 % (3869733)Termination phase: Preprocessing 1
% 7.81/3.53 % (3869733)Time elapsed: 0.076 s
% 7.81/3.53 % (3869733)Peak memory usage: 165 MB
% 7.81/3.53 % (3869733)Instructions burned: 127 (million)
% 7.81/3.53 % (3869728)Instruction limit reached!
% 7.81/3.53 % (3869728)------------------------------
% 7.81/3.53 % (3869728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869728)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869728)Termination reason: Instruction limit
% 7.81/3.53 % (3869728)Termination phase: SInE selection
% 7.81/3.53 % (3869728)Time elapsed: 0.137 s
% 7.81/3.53 % (3869728)Peak memory usage: 165 MB
% 7.81/3.53 % (3869728)Instructions burned: 295 (million)
% 7.81/3.53 % (3869742)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3149663849:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2978 on theBenchmark for (2978ds/114Mi)
% 7.81/3.53 % (3869743)lrs+10_1_sil=8000:sp=occurrence:random_seed=3134425562:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2977 on theBenchmark for (2977ds/907Mi)
% 7.81/3.53 % (3869742)Instruction limit reached!
% 7.81/3.53 % (3869742)------------------------------
% 7.81/3.53 % (3869742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869742)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869742)Termination reason: Instruction limit
% 7.81/3.53 % (3869742)Termination phase: Property scanning
% 7.81/3.53 % (3869742)Time elapsed: 0.065 s
% 7.81/3.53 % (3869742)Peak memory usage: 165 MB
% 7.81/3.53 % (3869742)Instructions burned: 114 (million)
% 7.81/3.53 % (3869746)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3603727927:i=437:sd=1:aac=none:ss=included_2977 on theBenchmark for (2977ds/437Mi)
% 7.81/3.53 % (3869751)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2280801100:i=5202:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/5202Mi)
% 7.81/3.53 % (3869746)Refutation not found, incomplete strategy
% 7.81/3.53 % (3869746)------------------------------
% 7.81/3.53 % (3869746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869746)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869746)Termination reason: Refutation not found, incomplete strategy
% 7.81/3.53 % (3869746)Time elapsed: 0.237 s
% 7.81/3.53 % (3869746)Peak memory usage: 169 MB
% 7.81/3.53 % (3869746)Instructions burned: 398 (million)
% 7.81/3.53 % (3869743)First to succeed.
% 7.81/3.53 % (3869743)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3869610"
% 7.81/3.53 % (3869700)Refutation not found, incomplete strategy
% 7.81/3.53 % (3869700)------------------------------
% 7.81/3.53 % (3869700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869700)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869700)Termination reason: Refutation not found, incomplete strategy
% 7.81/3.53 % (3869700)Time elapsed: 1.387 s
% 7.81/3.53 % (3869700)Peak memory usage: 298 MB
% 7.81/3.53 % (3869700)Instructions burned: 2547 (million)
% 7.81/3.53 % (3869746)------------------------------
% 7.81/3.53 % (3869746)------------------------------
% 7.81/3.53 % (3869731)Instruction limit reached!
% 7.81/3.53 % (3869731)------------------------------
% 7.81/3.53 % (3869731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.81/3.53 % (3869731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.81/3.53 % (3869731)CaDiCaL version: 2.1.3
% 7.81/3.53 % (3869731)Termination reason: Instruction limit
% 7.81/3.53 % (3869731)Termination phase: Property scanning
% 7.81/3.53 % (3869731)Time elapsed: 0.985 s
% 7.81/3.53 % (3869731)Peak memory usage: 193 MB
% 7.81/3.53 % (3869731)Instructions burned: 2352 (million)
% 7.81/3.53 % (3869743)Refutation found. Thanks to Tanya!
% 7.81/3.53 % SZS status Theorem for theBenchmark
% 7.81/3.53 % SZS output start Proof for theBenchmark
% See solution above
% 14.05/3.67 % (3869743)------------------------------
% 14.05/3.67 % (3869743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.05/3.67 % (3869743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.05/3.67 % (3869743)CaDiCaL version: 2.1.3
% 14.05/3.67 % (3869743)Termination reason: Refutation
% 14.05/3.67 % (3869743)Time elapsed: 0.427 s
% 14.05/3.67 % (3869743)Peak memory usage: 173 MB
% 14.05/3.67 % (3869743)Instructions burned: 759 (million)
% 14.05/3.67 % (3869743)------------------------------
% 14.05/3.67 % (3869743)------------------------------
% 14.05/3.67 % (3869610)Success in time 3.175 s
% 14.05/3.67 % Vampire exiting
%------------------------------------------------------------------------------