%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR095+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/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:42:56 AM UTC 2026
% Result : ContradictoryAxioms 27.63s 5.00s
% Output : Refutation 28.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 18
% Syntax : Number of formulae : 124 ( 37 unt; 0 def)
% Number of atoms : 432 ( 0 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 559 ( 251 ~; 249 |; 38 &)
% ( 7 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-4 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-4 aty)
% Number of variables : 207 ( 204 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_26) ).
fof(f27,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/sandbox2/benchmark/theBenchmark.p',kb_SUMO_27) ).
fof(f531,axiom,
! [X0,X1,X2,X3] :
( s__instance(X0,s__Class)
=> ( s__partition_4(X0,X1,X2,X3)
<=> ( s__exhaustiveDecomposition_4(X0,X1,X2,X3)
& s__disjointDecomposition_4(X0,X1,X2,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_531) ).
fof(f607,axiom,
! [X0] :
( s__instance(X0,s__SetOrClass)
=> ( s__instance(X0,s__Class)
<=> s__subclass(X0,s__Entity) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_608) ).
fof(f608,axiom,
s__subclass(s__Physical,s__Entity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_609) ).
fof(f613,axiom,
s__subclass(s__Object,s__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_614) ).
fof(f826,axiom,
s__subclass(s__Agent,s__Object),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_827) ).
fof(f1536,axiom,
! [X0,X1,X2] :
( ( s__instance(X2,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__subclass(X1,X2) )
=> s__subclass(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_1539) ).
fof(f1792,axiom,
! [X0,X1,X2,X3] :
( s__exhaustiveDecomposition_4(X1,X0,X2,X3)
=> ! [X4] :
( s__instance(X1,s__Class)
=> ( s__instance(X4,X1)
=> ? [X5] :
( s__instance(X5,s__SetOrClass)
& s__inList(X5,s__ListFn_3(X0,X2,X3))
& s__instance(X4,X5) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_1797) ).
fof(f1799,axiom,
! [X0,X1,X2,X3] :
( s__disjointDecomposition_4(X1,X0,X2,X3)
=> ! [X4] :
( ( s__instance(X4,s__SetOrClass)
& s__instance(X1,s__Class) )
=> ( s__inList(X4,s__ListFn_3(X0,X2,X3))
=> s__subclass(X4,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_1804) ).
fof(f1811,axiom,
! [X0,X1,X2,X3] :
( ( s__instance(X3,s__SetOrClass)
& s__instance(X2,s__SetOrClass)
& s__instance(X1,s__Class)
& s__instance(X0,s__SetOrClass) )
=> ( s__disjointDecomposition_4(X1,X0,X2,X3)
<=> ( s__disjoint(X0,X2)
& s__disjoint(X2,X3)
& s__disjoint(X3,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_1816) ).
fof(f7056,axiom,
s__subclass(s__Organism,s__Agent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_7129) ).
fof(f7058,axiom,
s__partition_4(s__Organism,s__Animal,s__Plant,s__Microorganism),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_7131) ).
fof(f7080,axiom,
s__subclass(s__NonFloweringPlant,s__Plant),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_7154) ).
fof(f7100,axiom,
s__subclass(s__Animal,s__Organism),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_7174) ).
fof(f7103,axiom,
s__subclass(s__Microorganism,s__Organism),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_7177) ).
fof(f16749,axiom,
s__instance(s__Organism25_1,s__Organism),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_1) ).
fof(f16750,axiom,
~ s__instance(s__Organism25_1,s__Microorganism),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_2) ).
fof(f16832,plain,
! [X0,X1,X2] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f1536]) ).
fof(f16833,plain,
! [X0,X1,X2] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f16832]) ).
fof(f16837,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,[],[f27]) ).
fof(f16838,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,[],[f16837]) ).
fof(f16839,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f16844,plain,
! [X0,X1,X2,X3] :
( ( s__partition_4(X0,X1,X2,X3)
<=> ( s__exhaustiveDecomposition_4(X0,X1,X2,X3)
& s__disjointDecomposition_4(X0,X1,X2,X3) ) )
| ~ s__instance(X0,s__Class) ),
inference(ennf_transformation,[],[f531]) ).
fof(f16960,plain,
! [X0,X1,X2,X3] :
( ( s__disjointDecomposition_4(X1,X0,X2,X3)
<=> ( s__disjoint(X0,X2)
& s__disjoint(X2,X3)
& s__disjoint(X3,X0) ) )
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__Class)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f1811]) ).
fof(f16961,plain,
! [X0,X1,X2,X3] :
( ( s__disjointDecomposition_4(X1,X0,X2,X3)
<=> ( s__disjoint(X0,X2)
& s__disjoint(X2,X3)
& s__disjoint(X3,X0) ) )
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__Class)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f16960]) ).
fof(f16964,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( s__subclass(X4,X1)
| ~ s__inList(X4,s__ListFn_3(X0,X2,X3))
| ~ s__instance(X4,s__SetOrClass)
| ~ s__instance(X1,s__Class) )
| ~ s__disjointDecomposition_4(X1,X0,X2,X3) ),
inference(ennf_transformation,[],[f1799]) ).
fof(f16965,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( s__subclass(X4,X1)
| ~ s__inList(X4,s__ListFn_3(X0,X2,X3))
| ~ s__instance(X4,s__SetOrClass)
| ~ s__instance(X1,s__Class) )
| ~ s__disjointDecomposition_4(X1,X0,X2,X3) ),
inference(flattening,[],[f16964]) ).
fof(f17023,plain,
! [X0] :
( ( s__instance(X0,s__Class)
<=> s__subclass(X0,s__Entity) )
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f607]) ).
fof(f17134,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ? [X5] :
( s__instance(X5,s__SetOrClass)
& s__inList(X5,s__ListFn_3(X0,X2,X3))
& s__instance(X4,X5) )
| ~ s__instance(X4,X1)
| ~ s__instance(X1,s__Class) )
| ~ s__exhaustiveDecomposition_4(X1,X0,X2,X3) ),
inference(ennf_transformation,[],[f1792]) ).
fof(f17135,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ? [X5] :
( s__instance(X5,s__SetOrClass)
& s__inList(X5,s__ListFn_3(X0,X2,X3))
& s__instance(X4,X5) )
| ~ s__instance(X4,X1)
| ~ s__instance(X1,s__Class) )
| ~ s__exhaustiveDecomposition_4(X1,X0,X2,X3) ),
inference(flattening,[],[f17134]) ).
fof(f17198,plain,
! [X0,X1,X2,X3] :
( ( ( s__partition_4(X0,X1,X2,X3)
| ~ s__exhaustiveDecomposition_4(X0,X1,X2,X3)
| ~ s__disjointDecomposition_4(X0,X1,X2,X3) )
& ( ( s__exhaustiveDecomposition_4(X0,X1,X2,X3)
& s__disjointDecomposition_4(X0,X1,X2,X3) )
| ~ s__partition_4(X0,X1,X2,X3) ) )
| ~ s__instance(X0,s__Class) ),
inference(nnf_transformation,[],[f16844]) ).
fof(f17199,plain,
! [X0,X1,X2,X3] :
( ( ( s__partition_4(X0,X1,X2,X3)
| ~ s__exhaustiveDecomposition_4(X0,X1,X2,X3)
| ~ s__disjointDecomposition_4(X0,X1,X2,X3) )
& ( ( s__exhaustiveDecomposition_4(X0,X1,X2,X3)
& s__disjointDecomposition_4(X0,X1,X2,X3) )
| ~ s__partition_4(X0,X1,X2,X3) ) )
| ~ s__instance(X0,s__Class) ),
inference(flattening,[],[f17198]) ).
fof(f17218,plain,
! [X0,X1,X2,X3] :
( ( ( s__disjointDecomposition_4(X1,X0,X2,X3)
| ~ s__disjoint(X0,X2)
| ~ s__disjoint(X2,X3)
| ~ s__disjoint(X3,X0) )
& ( ( s__disjoint(X0,X2)
& s__disjoint(X2,X3)
& s__disjoint(X3,X0) )
| ~ s__disjointDecomposition_4(X1,X0,X2,X3) ) )
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__Class)
| ~ s__instance(X0,s__SetOrClass) ),
inference(nnf_transformation,[],[f16961]) ).
fof(f17219,plain,
! [X0,X1,X2,X3] :
( ( ( s__disjointDecomposition_4(X1,X0,X2,X3)
| ~ s__disjoint(X0,X2)
| ~ s__disjoint(X2,X3)
| ~ s__disjoint(X3,X0) )
& ( ( s__disjoint(X0,X2)
& s__disjoint(X2,X3)
& s__disjoint(X3,X0) )
| ~ s__disjointDecomposition_4(X1,X0,X2,X3) ) )
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__Class)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f17218]) ).
fof(f17228,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,[],[f17023]) ).
fof(f17232,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ( s__instance(sK32(X0,X2,X3,X4),s__SetOrClass)
& s__inList(sK32(X0,X2,X3,X4),s__ListFn_3(X0,X2,X3))
& s__instance(X4,sK32(X0,X2,X3,X4)) )
| ~ s__instance(X4,X1)
| ~ s__instance(X1,s__Class) )
| ~ s__exhaustiveDecomposition_4(X1,X0,X2,X3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32]),skolemize(X5,sK32(X0,X2,X3,X4))],[f17135]) ).
fof(f17245,plain,
s__subclass(s__NonFloweringPlant,s__Plant),
inference(cnf_transformation,[],[f7080]) ).
fof(f17248,plain,
s__partition_4(s__Organism,s__Animal,s__Plant,s__Microorganism),
inference(cnf_transformation,[],[f7058]) ).
fof(f17250,plain,
~ s__instance(s__Organism25_1,s__Microorganism),
inference(cnf_transformation,[],[f16750]) ).
fof(f17251,plain,
s__instance(s__Organism25_1,s__Organism),
inference(cnf_transformation,[],[f16749]) ).
fof(f17258,plain,
s__subclass(s__Organism,s__Agent),
inference(cnf_transformation,[],[f7056]) ).
fof(f17267,plain,
s__subclass(s__Agent,s__Object),
inference(cnf_transformation,[],[f826]) ).
fof(f17277,plain,
s__subclass(s__Animal,s__Organism),
inference(cnf_transformation,[],[f7100]) ).
fof(f17291,plain,
! [X2,X0,X1] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f16833]) ).
fof(f17294,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,[],[f16838]) ).
fof(f17295,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f16839]) ).
fof(f17296,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f16839]) ).
fof(f17311,plain,
! [X2,X3,X0,X1] :
( ~ s__partition_4(X0,X1,X2,X3)
| s__disjointDecomposition_4(X0,X1,X2,X3)
| ~ s__instance(X0,s__Class) ),
inference(cnf_transformation,[],[f17199]) ).
fof(f17312,plain,
! [X2,X3,X0,X1] :
( ~ s__partition_4(X0,X1,X2,X3)
| s__exhaustiveDecomposition_4(X0,X1,X2,X3)
| ~ s__instance(X0,s__Class) ),
inference(cnf_transformation,[],[f17199]) ).
fof(f17325,plain,
s__subclass(s__Microorganism,s__Organism),
inference(cnf_transformation,[],[f7103]) ).
fof(f17480,plain,
! [X2,X3,X0,X1] :
( ~ s__disjointDecomposition_4(X1,X0,X2,X3)
| s__disjoint(X3,X0)
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__Class)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f17219]) ).
fof(f17481,plain,
! [X2,X3,X0,X1] :
( ~ s__disjointDecomposition_4(X1,X0,X2,X3)
| s__disjoint(X2,X3)
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__Class)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f17219]) ).
fof(f17482,plain,
! [X2,X3,X0,X1] :
( ~ s__disjointDecomposition_4(X1,X0,X2,X3)
| s__disjoint(X0,X2)
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__Class)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f17219]) ).
fof(f17483,plain,
! [X2,X3,X0,X1] :
( s__disjointDecomposition_4(X1,X0,X2,X3)
| ~ s__disjoint(X0,X2)
| ~ s__disjoint(X2,X3)
| ~ s__disjoint(X3,X0)
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__Class)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f17219]) ).
fof(f17485,plain,
! [X2,X3,X0,X1,X4] :
( ~ s__inList(X4,s__ListFn_3(X0,X2,X3))
| s__subclass(X4,X1)
| ~ s__instance(X4,s__SetOrClass)
| ~ s__instance(X1,s__Class)
| ~ s__disjointDecomposition_4(X1,X0,X2,X3) ),
inference(cnf_transformation,[],[f16965]) ).
fof(f17552,plain,
! [X0] :
( ~ s__subclass(X0,s__Entity)
| s__instance(X0,s__Class)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f17228]) ).
fof(f17647,plain,
! [X2,X3,X0,X1,X4] :
( ~ s__exhaustiveDecomposition_4(X1,X0,X2,X3)
| ~ s__instance(X4,X1)
| ~ s__instance(X1,s__Class)
| s__instance(X4,sK32(X0,X2,X3,X4)) ),
inference(cnf_transformation,[],[f17232]) ).
fof(f17648,plain,
! [X2,X3,X0,X1,X4] :
( ~ s__exhaustiveDecomposition_4(X1,X0,X2,X3)
| ~ s__instance(X4,X1)
| ~ s__instance(X1,s__Class)
| s__inList(sK32(X0,X2,X3,X4),s__ListFn_3(X0,X2,X3)) ),
inference(cnf_transformation,[],[f17232]) ).
fof(f17649,plain,
! [X2,X3,X0,X1,X4] :
( ~ s__exhaustiveDecomposition_4(X1,X0,X2,X3)
| ~ s__instance(X4,X1)
| ~ s__instance(X1,s__Class)
| s__instance(sK32(X0,X2,X3,X4),s__SetOrClass) ),
inference(cnf_transformation,[],[f17232]) ).
fof(f17694,plain,
s__subclass(s__Object,s__Physical),
inference(cnf_transformation,[],[f613]) ).
fof(f17695,plain,
s__subclass(s__Physical,s__Entity),
inference(cnf_transformation,[],[f608]) ).
fof(f17785,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,[],[f17294,f17295]) ).
fof(f17787,plain,
! [X2,X0,X1] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f17291,f17295]) ).
fof(f17797,plain,
! [X2,X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X2,X1)
| ~ s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f17785,f17296]) ).
fof(f17799,plain,
! [X2,X0,X1] :
( s__subclass(X0,X2)
| ~ s__subclass(X0,X1)
| ~ s__subclass(X1,X2)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f17787,f17295]) ).
fof(f17803,plain,
! [X2,X0,X1] :
( ~ s__subclass(X1,X2)
| ~ s__subclass(X0,X1)
| s__subclass(X0,X2) ),
inference(forward_subsumption_resolution,[],[f17799,f17296]) ).
fof(f17807,plain,
s__instance(s__Organism,s__SetOrClass),
inference(resolution,[],[f17296,f17258]) ).
fof(f17809,plain,
s__instance(s__Plant,s__SetOrClass),
inference(resolution,[],[f17245,f17295]) ).
fof(f17817,plain,
s__instance(s__Animal,s__SetOrClass),
inference(resolution,[],[f17277,f17296]) ).
fof(f17885,plain,
s__instance(s__Microorganism,s__SetOrClass),
inference(resolution,[],[f17325,f17296]) ).
fof(f17994,plain,
! [X0] :
( ~ s__subclass(X0,s__Physical)
| s__subclass(X0,s__Entity) ),
inference(resolution,[],[f17803,f17695]) ).
fof(f17995,plain,
! [X0] :
( ~ s__subclass(X0,s__Agent)
| s__subclass(X0,s__Object) ),
inference(resolution,[],[f17803,f17267]) ).
fof(f18069,plain,
s__subclass(s__Object,s__Entity),
inference(resolution,[],[f17994,f17694]) ).
fof(f18072,plain,
! [X0] :
( ~ s__subclass(X0,s__Object)
| s__subclass(X0,s__Entity) ),
inference(resolution,[],[f18069,f17803]) ).
fof(f18236,plain,
s__subclass(s__Organism,s__Object),
inference(resolution,[],[f17995,f17258]) ).
fof(f18273,plain,
s__subclass(s__Organism,s__Entity),
inference(resolution,[],[f18236,f18072]) ).
fof(f18358,plain,
( s__instance(s__Organism,s__Class)
| ~ s__instance(s__Organism,s__SetOrClass) ),
inference(resolution,[],[f18273,f17552]) ).
fof(f18359,plain,
! [X0] :
( ~ s__subclass(X0,s__Organism)
| s__subclass(X0,s__Entity) ),
inference(resolution,[],[f18273,f17803]) ).
fof(f18373,plain,
s__instance(s__Organism,s__Class),
inference(forward_subsumption_resolution,[],[f18358,f17807]) ).
fof(f18395,plain,
s__subclass(s__Microorganism,s__Entity),
inference(resolution,[],[f18359,f17325]) ).
fof(f18845,plain,
( s__instance(s__Microorganism,s__Class)
| ~ s__instance(s__Microorganism,s__SetOrClass) ),
inference(resolution,[],[f18395,f17552]) ).
fof(f18860,plain,
s__instance(s__Microorganism,s__Class),
inference(forward_subsumption_resolution,[],[f18845,f17885]) ).
fof(f21050,plain,
( s__exhaustiveDecomposition_4(s__Organism,s__Animal,s__Plant,s__Microorganism)
| ~ s__instance(s__Organism,s__Class) ),
inference(resolution,[],[f17312,f17248]) ).
fof(f21051,plain,
s__exhaustiveDecomposition_4(s__Organism,s__Animal,s__Plant,s__Microorganism),
inference(forward_subsumption_resolution,[],[f21050,f18373]) ).
fof(f21052,plain,
! [X0] :
( ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Organism,s__Class)
| s__inList(sK32(s__Animal,s__Plant,s__Microorganism,X0),s__ListFn_3(s__Animal,s__Plant,s__Microorganism)) ),
inference(resolution,[],[f21051,f17648]) ).
fof(f21053,plain,
! [X0] :
( ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Organism,s__Class)
| s__instance(sK32(s__Animal,s__Plant,s__Microorganism,X0),s__SetOrClass) ),
inference(resolution,[],[f21051,f17649]) ).
fof(f21054,plain,
! [X0] :
( ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Organism,s__Class)
| s__instance(X0,sK32(s__Animal,s__Plant,s__Microorganism,X0)) ),
inference(resolution,[],[f21051,f17647]) ).
fof(f21055,plain,
! [X0] :
( s__instance(X0,sK32(s__Animal,s__Plant,s__Microorganism,X0))
| ~ s__instance(X0,s__Organism) ),
inference(forward_subsumption_resolution,[],[f21054,f18373]) ).
fof(f21056,plain,
! [X0] :
( s__instance(sK32(s__Animal,s__Plant,s__Microorganism,X0),s__SetOrClass)
| ~ s__instance(X0,s__Organism) ),
inference(forward_subsumption_resolution,[],[f21053,f18373]) ).
fof(f21057,plain,
! [X0] :
( s__inList(sK32(s__Animal,s__Plant,s__Microorganism,X0),s__ListFn_3(s__Animal,s__Plant,s__Microorganism))
| ~ s__instance(X0,s__Organism) ),
inference(forward_subsumption_resolution,[],[f21052,f18373]) ).
fof(f21954,plain,
( s__disjointDecomposition_4(s__Organism,s__Animal,s__Plant,s__Microorganism)
| ~ s__instance(s__Organism,s__Class) ),
inference(resolution,[],[f17311,f17248]) ).
fof(f21955,plain,
s__disjointDecomposition_4(s__Organism,s__Animal,s__Plant,s__Microorganism),
inference(forward_subsumption_resolution,[],[f21954,f18373]) ).
fof(f21957,plain,
( s__disjoint(s__Microorganism,s__Animal)
| ~ s__instance(s__Microorganism,s__SetOrClass)
| ~ s__instance(s__Plant,s__SetOrClass)
| ~ s__instance(s__Organism,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(resolution,[],[f21955,f17480]) ).
fof(f21958,plain,
( s__disjoint(s__Animal,s__Plant)
| ~ s__instance(s__Microorganism,s__SetOrClass)
| ~ s__instance(s__Plant,s__SetOrClass)
| ~ s__instance(s__Organism,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(resolution,[],[f21955,f17482]) ).
fof(f21959,plain,
( s__disjoint(s__Plant,s__Microorganism)
| ~ s__instance(s__Microorganism,s__SetOrClass)
| ~ s__instance(s__Plant,s__SetOrClass)
| ~ s__instance(s__Organism,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(resolution,[],[f21955,f17481]) ).
fof(f21960,plain,
( s__disjoint(s__Plant,s__Microorganism)
| ~ s__instance(s__Plant,s__SetOrClass)
| ~ s__instance(s__Organism,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f21959,f17885]) ).
fof(f21961,plain,
( s__disjoint(s__Animal,s__Plant)
| ~ s__instance(s__Plant,s__SetOrClass)
| ~ s__instance(s__Organism,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f21958,f17885]) ).
fof(f21962,plain,
( s__disjoint(s__Microorganism,s__Animal)
| ~ s__instance(s__Plant,s__SetOrClass)
| ~ s__instance(s__Organism,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f21957,f17885]) ).
fof(f21963,plain,
( s__disjoint(s__Plant,s__Microorganism)
| ~ s__instance(s__Organism,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f21960,f17809]) ).
fof(f21964,plain,
( s__disjoint(s__Animal,s__Plant)
| ~ s__instance(s__Organism,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f21961,f17809]) ).
fof(f21965,plain,
( s__disjoint(s__Microorganism,s__Animal)
| ~ s__instance(s__Organism,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f21962,f17809]) ).
fof(f21966,plain,
( s__disjoint(s__Plant,s__Microorganism)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f21963,f18373]) ).
fof(f21967,plain,
( s__disjoint(s__Animal,s__Plant)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f21964,f18373]) ).
fof(f21968,plain,
( s__disjoint(s__Microorganism,s__Animal)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f21965,f18373]) ).
fof(f21969,plain,
s__disjoint(s__Plant,s__Microorganism),
inference(forward_subsumption_resolution,[],[f21966,f17817]) ).
fof(f21970,plain,
s__disjoint(s__Animal,s__Plant),
inference(forward_subsumption_resolution,[],[f21967,f17817]) ).
fof(f21971,plain,
s__disjoint(s__Microorganism,s__Animal),
inference(forward_subsumption_resolution,[],[f21968,f17817]) ).
fof(f22038,plain,
! [X0,X1] :
( s__subclass(sK32(s__Animal,s__Plant,s__Microorganism,X0),X1)
| ~ s__instance(sK32(s__Animal,s__Plant,s__Microorganism,X0),s__SetOrClass)
| ~ s__instance(X1,s__Class)
| ~ s__disjointDecomposition_4(X1,s__Animal,s__Plant,s__Microorganism)
| ~ s__instance(X0,s__Organism) ),
inference(resolution,[],[f17485,f21057]) ).
fof(f22039,plain,
! [X0,X1] :
( s__subclass(sK32(s__Animal,s__Plant,s__Microorganism,X0),X1)
| ~ s__instance(X1,s__Class)
| ~ s__disjointDecomposition_4(X1,s__Animal,s__Plant,s__Microorganism)
| ~ s__instance(X0,s__Organism) ),
inference(forward_subsumption_resolution,[],[f22038,f21056]) ).
fof(f22044,plain,
! [X2,X0,X1] :
( ~ s__instance(X2,sK32(s__Animal,s__Plant,s__Microorganism,X1))
| ~ s__disjointDecomposition_4(X0,s__Animal,s__Plant,s__Microorganism)
| ~ s__instance(X1,s__Organism)
| s__instance(X2,X0)
| ~ s__instance(X0,s__Class) ),
inference(resolution,[],[f22039,f17797]) ).
fof(f23012,plain,
! [X0,X1] :
( ~ s__disjointDecomposition_4(X0,s__Animal,s__Plant,s__Microorganism)
| ~ s__instance(X1,s__Organism)
| s__instance(X1,X0)
| ~ s__instance(X0,s__Class)
| ~ s__instance(X1,s__Organism) ),
inference(resolution,[],[f22044,f21055]) ).
fof(f23015,plain,
! [X0,X1] :
( ~ s__disjointDecomposition_4(X0,s__Animal,s__Plant,s__Microorganism)
| ~ s__instance(X1,s__Organism)
| s__instance(X1,X0)
| ~ s__instance(X0,s__Class) ),
inference(duplicate_literal_removal,[],[f23012]) ).
fof(f25181,plain,
! [X0,X1] :
( ~ s__disjoint(s__Animal,s__Plant)
| ~ s__disjoint(s__Plant,s__Microorganism)
| ~ s__disjoint(s__Microorganism,s__Animal)
| ~ s__instance(s__Microorganism,s__SetOrClass)
| ~ s__instance(s__Plant,s__SetOrClass)
| ~ s__instance(X0,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X1,s__Organism)
| s__instance(X1,X0)
| ~ s__instance(X0,s__Class) ),
inference(resolution,[],[f17483,f23015]) ).
fof(f25251,plain,
! [X0,X1] :
( ~ s__disjoint(s__Animal,s__Plant)
| ~ s__disjoint(s__Plant,s__Microorganism)
| ~ s__disjoint(s__Microorganism,s__Animal)
| ~ s__instance(s__Microorganism,s__SetOrClass)
| ~ s__instance(s__Plant,s__SetOrClass)
| ~ s__instance(X0,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X1,s__Organism)
| s__instance(X1,X0) ),
inference(duplicate_literal_removal,[],[f25181]) ).
fof(f25324,plain,
! [X0,X1] :
( ~ s__disjoint(s__Plant,s__Microorganism)
| ~ s__disjoint(s__Microorganism,s__Animal)
| ~ s__instance(s__Microorganism,s__SetOrClass)
| ~ s__instance(s__Plant,s__SetOrClass)
| ~ s__instance(X0,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X1,s__Organism)
| s__instance(X1,X0) ),
inference(forward_subsumption_resolution,[],[f25251,f21970]) ).
fof(f25393,plain,
! [X0,X1] :
( ~ s__disjoint(s__Microorganism,s__Animal)
| ~ s__instance(s__Microorganism,s__SetOrClass)
| ~ s__instance(s__Plant,s__SetOrClass)
| ~ s__instance(X0,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X1,s__Organism)
| s__instance(X1,X0) ),
inference(forward_subsumption_resolution,[],[f25324,f21969]) ).
fof(f25462,plain,
! [X0,X1] :
( ~ s__instance(s__Microorganism,s__SetOrClass)
| ~ s__instance(s__Plant,s__SetOrClass)
| ~ s__instance(X0,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X1,s__Organism)
| s__instance(X1,X0) ),
inference(forward_subsumption_resolution,[],[f25393,f21971]) ).
fof(f25531,plain,
! [X0,X1] :
( ~ s__instance(s__Plant,s__SetOrClass)
| ~ s__instance(X0,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X1,s__Organism)
| s__instance(X1,X0) ),
inference(forward_subsumption_resolution,[],[f25462,f17885]) ).
fof(f25600,plain,
! [X0,X1] :
( ~ s__instance(X0,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X1,s__Organism)
| s__instance(X1,X0) ),
inference(forward_subsumption_resolution,[],[f25531,f17809]) ).
fof(f25669,plain,
! [X0,X1] :
( ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Class)
| s__instance(X1,X0) ),
inference(forward_subsumption_resolution,[],[f25600,f17817]) ).
fof(f25766,plain,
! [X0] :
( ~ s__instance(X0,s__Class)
| s__instance(s__Organism25_1,X0) ),
inference(resolution,[],[f25669,f17251]) ).
fof(f25802,plain,
s__instance(s__Organism25_1,s__Microorganism),
inference(resolution,[],[f25766,f18860]) ).
fof(f25817,plain,
$false,
inference(forward_subsumption_resolution,[],[f25802,f17250]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR095+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/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:47:52 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.92/2.38 % (861741)Detected formulas, will run a generic FOF schedule.
% 8.92/2.38 % (861746)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=1782222798:i=141193_2995 on theBenchmark for (2995ds/141193Mi)
% 8.92/2.38 % (861747)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=4105018938:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2995 on theBenchmark for (2995ds/134677Mi)
% 8.92/2.38 % (861748)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=1370610119:i=141695:sd=1:nm=32:gsp=on:ss=included_2995 on theBenchmark for (2995ds/141695Mi)
% 8.92/2.38 % (861752)dis-21_1_sil=8000:lcm=predicate:random_seed=266222553:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2995 on theBenchmark for (2995ds/129Mi)
% 8.92/2.38 % (861749)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=820211602:i=109:sd=1:ins=1:gsp=on:ss=axioms_2995 on theBenchmark for (2995ds/109Mi)
% 8.92/2.38 % (861751)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1997670529:s2a=on:i=139:gtg=position_2995 on theBenchmark for (2995ds/139Mi)
% 8.92/2.38 % (861750)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3842061785:i=119:av=off:ss=axioms_2995 on theBenchmark for (2995ds/119Mi)
% 8.92/2.38 % (861749)Refutation not found, incomplete strategy
% 8.92/2.38 % (861749)------------------------------
% 8.92/2.38 % (861749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.92/2.38 % (861749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.38 % (861749)CaDiCaL version: 2.1.3
% 8.92/2.38 % (861749)Termination reason: Refutation not found, incomplete strategy
% 8.92/2.38 % (861749)Time elapsed: 0.039 s
% 8.92/2.38 % (861749)Peak memory usage: 101 MB
% 8.92/2.38 % (861749)Instructions burned: 59 (million)
% 8.92/2.38 % (861751)Instruction limit reached!
% 8.92/2.38 % (861751)------------------------------
% 8.92/2.38 % (861751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.92/2.38 % (861751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.38 % (861751)CaDiCaL version: 2.1.3
% 8.92/2.38 % (861751)Termination reason: Instruction limit
% 8.92/2.38 % (861751)Termination phase: SInE selection
% 8.92/2.38 % (861751)Time elapsed: 0.073 s
% 8.92/2.38 % (861751)Peak memory usage: 99 MB
% 8.92/2.38 % (861751)Instructions burned: 139 (million)
% 8.92/2.38 % (861750)Instruction limit reached!
% 8.92/2.38 % (861750)------------------------------
% 8.92/2.38 % (861750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.92/2.38 % (861750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.38 % (861750)CaDiCaL version: 2.1.3
% 8.92/2.38 % (861750)Termination reason: Instruction limit
% 8.92/2.38 % (861750)Termination phase: Saturation
% 8.92/2.38 % (861750)Time elapsed: 0.075 s
% 8.92/2.38 % (861750)Peak memory usage: 102 MB
% 8.92/2.38 % (861750)Instructions burned: 119 (million)
% 8.92/2.38 % (861752)Instruction limit reached!
% 8.92/2.38 % (861752)------------------------------
% 8.92/2.38 % (861752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.92/2.38 % (861752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.92/2.38 % (861752)CaDiCaL version: 2.1.3
% 8.92/2.38 % (861752)Termination reason: Instruction limit
% 8.92/2.38 % (861752)Termination phase: Saturation
% 8.92/2.38 % (861752)Time elapsed: 0.083 s
% 8.92/2.38 % (861752)Peak memory usage: 102 MB
% 8.92/2.38 % (861752)Instructions burned: 129 (million)
% 8.92/2.38 % (861761)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1449025200:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/157Mi)
% 8.92/2.38 % (861760)lrs+10_1_sil=8000:sp=occurrence:random_seed=219210599:i=285:sd=3:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/285Mi)
% 8.92/2.38 % (861762)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3797604509:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 8.92/2.38 % (861749)------------------------------
% 8.92/2.38 % (861749)------------------------------
% 8.92/2.38 % (861760)Refutation not found, incomplete strategy
% 8.92/2.38 % (861760)------------------------------
% 8.92/2.38 % (861760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.92/2.38 % (861760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.28 % (861760)CaDiCaL version: 2.1.3
% 15.53/3.28 % (861760)Termination reason: Refutation not found, incomplete strategy
% 15.53/3.28 % (861760)Time elapsed: 0.041 s
% 15.53/3.28 % (861760)Peak memory usage: 102 MB
% 15.53/3.28 % (861760)Instructions burned: 50 (million)
% 15.53/3.28 % (861762)Refutation not found, incomplete strategy
% 15.53/3.28 % (861762)------------------------------
% 15.53/3.28 % (861762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.28 % (861762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.28 % (861762)CaDiCaL version: 2.1.3
% 15.53/3.28 % (861762)Termination reason: Refutation not found, incomplete strategy
% 15.53/3.28 % (861762)Time elapsed: 0.039 s
% 15.53/3.28 % (861762)Peak memory usage: 102 MB
% 15.53/3.28 % (861762)Instructions burned: 47 (million)
% 15.53/3.28 % (861761)Refutation not found, incomplete strategy
% 15.53/3.28 % (861761)------------------------------
% 15.53/3.28 % (861761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.28 % (861761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.28 % (861761)CaDiCaL version: 2.1.3
% 15.53/3.28 % (861761)Termination reason: Refutation not found, incomplete strategy
% 15.53/3.28 % (861761)Time elapsed: 0.082 s
% 15.53/3.28 % (861761)Peak memory usage: 102 MB
% 15.53/3.28 % (861761)Instructions burned: 154 (million)
% 15.53/3.28 [W928 22:47:54.234269172 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.53/3.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.53/3.28 [W928 22:47:54.234366439 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.53/3.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.53/3.28 [W928 22:47:54.234410505 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.53/3.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.53/3.28 [W928 22:47:54.234423899 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.53/3.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.53/3.28 [W928 22:47:54.234449979 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.53/3.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.53/3.28 [W928 22:47:54.234461499 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.53/3.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.53/3.28 % (861766)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=1833501837:s2a=on:i=248:s2at=1.23:gtg=position_2991 on theBenchmark for (2991ds/248Mi)
% 15.53/3.28 % (861760)------------------------------
% 15.53/3.28 % (861760)------------------------------
% 15.53/3.28 % (861762)------------------------------
% 15.53/3.28 % (861762)------------------------------
% 15.53/3.28 % (861761)------------------------------
% 15.53/3.28 % (861761)------------------------------
% 15.53/3.28 % (861766)Instruction limit reached!
% 15.53/3.28 % (861766)------------------------------
% 15.53/3.28 % (861766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.53/3.28 % (861766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.53/3.28 % (861766)CaDiCaL version: 2.1.3
% 15.53/3.28 % (861766)Termination reason: Instruction limit
% 15.53/3.28 % (861766)Termination phase: Preprocessing 3
% 15.53/3.28 % (861766)Time elapsed: 0.155 s
% 15.53/3.28 % (861766)Peak memory usage: 104 MB
% 25.49/4.61 % (861766)Instructions burned: 249 (million)
% 25.49/4.61 % (861769)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1475540522:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 25.49/4.61 % (861768)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=640516340:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 25.49/4.61 % (861748)Refutation not found, incomplete strategy
% 25.49/4.61 % (861748)------------------------------
% 25.49/4.61 % (861748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.49/4.61 % (861748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.49/4.61 % (861748)CaDiCaL version: 2.1.3
% 25.49/4.61 % (861748)Termination reason: Refutation not found, incomplete strategy
% 25.49/4.61 % (861748)Time elapsed: 0.712 s
% 25.49/4.61 % (861748)Peak memory usage: 157 MB
% 25.49/4.61 % (861748)Instructions burned: 1219 (million)
% 25.49/4.61 % (861770)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4167475912:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 25.49/4.61 % (861768)Refutation not found, incomplete strategy
% 25.49/4.61 % (861768)------------------------------
% 25.49/4.61 % (861768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.49/4.61 % (861768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.49/4.61 % (861768)CaDiCaL version: 2.1.3
% 25.49/4.61 % (861768)Termination reason: Refutation not found, incomplete strategy
% 25.49/4.61 % (861768)Time elapsed: 0.055 s
% 25.49/4.61 % (861768)Peak memory usage: 102 MB
% 25.49/4.61 % (861768)Instructions burned: 82 (million)
% 25.49/4.61 % (861771)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1805891144:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 25.49/4.61 % (861770)Instruction limit reached!
% 25.49/4.61 % (861770)------------------------------
% 25.49/4.61 % (861770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.49/4.61 % (861770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.49/4.61 % (861770)CaDiCaL version: 2.1.3
% 25.49/4.61 % (861770)Termination reason: Instruction limit
% 25.49/4.61 % (861770)Termination phase: Saturation
% 25.49/4.61 % (861770)Time elapsed: 0.085 s
% 25.49/4.61 % (861770)Peak memory usage: 103 MB
% 25.49/4.61 % (861770)Instructions burned: 114 (million)
% 25.49/4.61 % (861748)------------------------------
% 25.49/4.61 % (861748)------------------------------
% 25.49/4.61 % (861771)Instruction limit reached!
% 25.49/4.61 % (861771)------------------------------
% 25.49/4.61 % (861771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.49/4.61 % (861771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.49/4.61 % (861771)CaDiCaL version: 2.1.3
% 25.49/4.61 % (861771)Termination reason: Instruction limit
% 25.49/4.61 % (861771)Termination phase: Preprocessing 3
% 25.49/4.61 % (861771)Time elapsed: 0.093 s
% 25.49/4.61 % (861771)Peak memory usage: 104 MB
% 25.49/4.61 % (861771)Instructions burned: 128 (million)
% 25.49/4.61 % (861776)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1545631639:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 25.49/4.61 % (861777)lrs+10_1_sil=8000:sp=occurrence:random_seed=2640221827:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 25.49/4.61 % (861768)------------------------------
% 25.49/4.61 % (861768)------------------------------
% 25.49/4.61 % (861776)Instruction limit reached!
% 25.49/4.61 % (861776)------------------------------
% 25.49/4.61 % (861776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.49/4.61 % (861776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.49/4.61 % (861776)CaDiCaL version: 2.1.3
% 25.49/4.61 % (861776)Termination reason: Instruction limit
% 25.49/4.61 % (861776)Termination phase: Initialization
% 25.49/4.61 % (861776)Time elapsed: 0.057 s
% 25.49/4.61 % (861776)Peak memory usage: 98 MB
% 25.49/4.61 % (861776)Instructions burned: 114 (million)
% 25.49/4.61 % (861778)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2245636883:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 25.49/4.61 % (861778)Refutation not found, incomplete strategy
% 25.49/4.61 % (861778)------------------------------
% 25.49/4.61 % (861778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.49/4.61 % (861778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.63/5.00 % (861778)CaDiCaL version: 2.1.3
% 27.63/5.00 % (861778)Termination reason: Refutation not found, incomplete strategy
% 27.63/5.00 % (861778)Time elapsed: 0.040 s
% 27.63/5.00 % (861778)Peak memory usage: 102 MB
% 27.63/5.00 % (861778)Instructions burned: 47 (million)
% 27.63/5.00 % (861781)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1495647830:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 27.63/5.00 % (861782)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=321769011:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2983 on theBenchmark for (2983ds/134Mi)
% 27.63/5.00 % (861782)Refutation not found, incomplete strategy
% 27.63/5.00 % (861782)------------------------------
% 27.63/5.00 % (861782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.63/5.00 % (861782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.63/5.00 % (861782)CaDiCaL version: 2.1.3
% 27.63/5.00 % (861782)Termination reason: Refutation not found, incomplete strategy
% 27.63/5.00 % (861782)Time elapsed: 0.048 s
% 27.63/5.00 % (861782)Peak memory usage: 103 MB
% 27.63/5.00 % (861782)Instructions burned: 65 (million)
% 27.63/5.00 % (861778)------------------------------
% 27.63/5.00 % (861778)------------------------------
% 27.63/5.00 % (861777)Instruction limit reached!
% 27.63/5.00 % (861777)------------------------------
% 27.63/5.00 % (861777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.63/5.00 % (861777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.63/5.00 % (861777)CaDiCaL version: 2.1.3
% 27.63/5.00 % (861777)Termination reason: Instruction limit
% 27.63/5.00 % (861777)Termination phase: Saturation
% 27.63/5.00 % (861777)Time elapsed: 0.514 s
% 27.63/5.00 % (861777)Peak memory usage: 117 MB
% 27.63/5.00 % (861777)Instructions burned: 909 (million)
% 27.63/5.00 % (861782)------------------------------
% 27.63/5.00 % (861782)------------------------------
% 27.63/5.00 % (861786)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1419926390:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 27.63/5.00 % (861786)Refutation not found, incomplete strategy
% 27.63/5.00 % (861786)------------------------------
% 27.63/5.00 % (861786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.63/5.00 % (861786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.63/5.00 % (861786)CaDiCaL version: 2.1.3
% 27.63/5.00 % (861786)Termination reason: Refutation not found, incomplete strategy
% 27.63/5.00 % (861786)Time elapsed: 0.098 s
% 27.63/5.00 % (861786)Peak memory usage: 104 MB
% 27.63/5.00 % (861786)Instructions burned: 156 (million)
% 27.63/5.00 % (861787)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3847179390:st=3:i=13193:sd=3:ss=axioms_2978 on theBenchmark for (2978ds/13193Mi)
% 27.63/5.00 % (861788)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=4099433062:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/125Mi)
% 27.63/5.00 % (861788)Instruction limit reached!
% 27.63/5.00 % (861788)------------------------------
% 27.63/5.00 % (861788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.63/5.00 % (861788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.63/5.00 % (861788)CaDiCaL version: 2.1.3
% 27.63/5.00 % (861788)Termination reason: Instruction limit
% 27.63/5.00 % (861788)Termination phase: SInE selection
% 27.63/5.00 % (861788)Time elapsed: 0.066 s
% 27.63/5.00 % (861788)Peak memory usage: 99 MB
% 27.63/5.00 % (861788)Instructions burned: 126 (million)
% 27.63/5.00 % (861786)------------------------------
% 27.63/5.00 % (861786)------------------------------
% 27.63/5.00 % (861792)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=156343815:i=134:gtgl=5:slsql=off:gtg=exists_sym_2976 on theBenchmark for (2976ds/134Mi)
% 27.63/5.00 % (861792)Instruction limit reached!
% 27.63/5.00 % (861792)------------------------------
% 27.63/5.00 % (861792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.63/5.00 % (861792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.63/5.00 % (861792)CaDiCaL version: 2.1.3
% 27.63/5.00 % (861792)Termination reason: Instruction limit
% 27.63/5.00 % (861792)Termination phase: Property scanning
% 27.63/5.00 % (861792)Time elapsed: 0.070 s
% 27.63/5.00 % (861792)Peak memory usage: 98 MB
% 27.63/5.00 % (861792)Instructions burned: 136 (million)
% 27.63/5.00 % (861793)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1852341621:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/141Mi)
% 27.63/5.00 % (861793)Refutation not found, incomplete strategy
% 27.63/5.00 % (861793)------------------------------
% 27.63/5.00 % (861793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.63/5.00 % (861793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.63/5.00 % (861793)CaDiCaL version: 2.1.3
% 27.63/5.00 % (861793)Termination reason: Refutation not found, incomplete strategy
% 27.63/5.00 % (861793)Time elapsed: 0.043 s
% 27.63/5.00 % (861793)Peak memory usage: 102 MB
% 27.63/5.00 % (861793)Instructions burned: 59 (million)
% 27.63/5.00 % (861795)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=890805350:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2973 on theBenchmark for (2973ds/431Mi)
% 27.63/5.00 % (861795)Refutation not found, incomplete strategy
% 27.63/5.00 % (861795)------------------------------
% 27.63/5.00 % (861795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.63/5.00 % (861795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.63/5.00 % (861795)CaDiCaL version: 2.1.3
% 27.63/5.00 % (861795)Termination reason: Refutation not found, incomplete strategy
% 27.63/5.00 % (861795)Time elapsed: 0.040 s
% 27.63/5.00 % (861795)Peak memory usage: 102 MB
% 27.63/5.00 % (861795)Instructions burned: 47 (million)
% 27.63/5.00 % (861769)Instruction limit reached!
% 27.63/5.00 % (861769)------------------------------
% 27.63/5.00 % (861769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.63/5.00 % (861769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.63/5.00 % (861769)CaDiCaL version: 2.1.3
% 27.63/5.00 % (861769)Termination reason: Instruction limit
% 27.63/5.00 % (861769)Termination phase: Saturation
% 27.63/5.00 % (861769)Time elapsed: 1.586 s
% 27.63/5.00 % (861769)Peak memory usage: 261 MB
% 27.63/5.00 % (861769)Instructions burned: 2353 (million)
% 27.63/5.00 % (861793)------------------------------
% 27.63/5.00 % (861793)------------------------------
% 27.63/5.00 % (861795)------------------------------
% 27.63/5.00 % (861795)------------------------------
% 27.63/5.00 % (861798)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=940741823:i=6060:aac=none:ins=25_2970 on theBenchmark for (2970ds/6060Mi)
% 27.63/5.00 % (861799)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1135595750:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2970 on theBenchmark for (2970ds/150Mi)
% 27.63/5.00 % (861799)Instruction limit reached!
% 27.63/5.00 % (861799)------------------------------
% 27.63/5.00 % (861799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.63/5.00 % (861799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.63/5.00 % (861799)CaDiCaL version: 2.1.3
% 27.63/5.00 % (861799)Termination reason: Instruction limit
% 27.63/5.00 % (861799)Termination phase: Preprocessing 3
% 27.63/5.00 % (861799)Time elapsed: 0.104 s
% 27.63/5.00 % (861799)Peak memory usage: 104 MB
% 27.63/5.00 % (861799)Instructions burned: 151 (million)
% 27.63/5.00 % (861800)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4157234571:i=14155:bd=all_2969 on theBenchmark for (2969ds/14155Mi)
% 27.63/5.00 % (861803)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2741786107:i=667:av=off:fsr=off_2967 on theBenchmark for (2967ds/667Mi)
% 27.63/5.00 % (861803)Instruction limit reached!
% 27.63/5.00 % (861803)------------------------------
% 27.63/5.00 % (861803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.63/5.00 % (861803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.63/5.00 % (861803)CaDiCaL version: 2.1.3
% 27.63/5.00 % (861803)Termination reason: Instruction limit
% 27.63/5.00 % (861803)Termination phase: Saturation
% 27.63/5.00 % (861803)Time elapsed: 0.368 s
% 27.63/5.00 % (861803)Peak memory usage: 117 MB
% 27.63/5.00 % (861803)Instructions burned: 667 (million)
% 27.63/5.00 % (861806)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=251799382:s2a=on:i=185:s2at=1.8:fdi=4_2962 on theBenchmark for (2962ds/185Mi)
% 27.63/5.00 % (861787)First to succeed.
% 27.63/5.00 % (861787)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-861741"
% 27.63/5.00 % (861806)Instruction limit reached!
% 27.63/5.00 % (861806)------------------------------
% 27.63/5.00 % (861806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.63/5.00 % (861806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.63/5.00 % (861806)CaDiCaL version: 2.1.3
% 27.63/5.00 % (861806)Termination reason: Instruction limit
% 27.63/5.00 % (861806)Termination phase: NewCNF
% 27.63/5.00 % (861806)Time elapsed: 0.136 s
% 27.63/5.00 % (861806)Peak memory usage: 106 MB
% 27.63/5.00 % (861806)Instructions burned: 186 (million)
% 27.63/5.00 % (861808)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1950261034:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2959 on theBenchmark for (2959ds/193Mi)
% 27.63/5.00 % (861787)Refutation found. Thanks to Tanya!
% 27.63/5.00 % SZS status ContradictoryAxioms for theBenchmark
% 27.63/5.00 % SZS output start Proof for theBenchmark
% See solution above
% 28.58/5.25 % (861787)------------------------------
% 28.58/5.25 % (861787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.58/5.25 % (861787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.58/5.25 % (861787)CaDiCaL version: 2.1.3
% 28.58/5.25 % (861787)Termination reason: Refutation
% 28.58/5.25 % (861787)Time elapsed: 1.699 s
% 28.58/5.25 % (861787)Peak memory usage: 174 MB
% 28.58/5.25 % (861787)Instructions burned: 2484 (million)
% 28.58/5.25 % (861787)------------------------------
% 28.58/5.25 % (861787)------------------------------
% 28.58/5.25 % (861741)Success in time 4.335 s
% 28.58/5.25 % Vampire exiting
%------------------------------------------------------------------------------