%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR244+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:10 AM UTC 2026
% Result : Theorem 13.62s 4.70s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 25
% Syntax : Number of formulae : 122 ( 39 unt; 0 def)
% Number of atoms : 293 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 353 ( 182 ~; 133 |; 22 &)
% ( 5 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 20 con; 0-1 aty)
% Number of variables : 155 ( 147 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( p__d__subclass(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__subclass(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA8) ).
fof(f4,axiom,
! [X0,X1,X2] :
( ( p__d__instance(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__instance(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA12) ).
fof(f86,axiom,
p__d__instance(c__subAttribute,c__PartialOrderingRelation),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA136) ).
fof(f89,axiom,
! [X0,X1,X2] :
( ( p__subAttribute(X1,X2)
& p__d__instance(X2,X0) )
=> p__d__instance(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA141) ).
fof(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA176) ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA178) ).
fof(f115,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA181) ).
fof(f477,axiom,
! [X0] :
( p__d__instance(X0,c__BinaryRelation)
=> ( p__d__instance(X0,c__ReflexiveRelation)
<=> ! [X1] : p__d__holds3(X0,X1,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA592) ).
fof(f495,axiom,
p__d__subclass(c__PartialOrderingRelation,c__ReflexiveRelation),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA610) ).
fof(f1691,axiom,
p__initialPart(c__VocalCords,c__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2440) ).
fof(f2092,axiom,
p__d__subclass(c__Vertebrate,c__Animal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2942) ).
fof(f2105,axiom,
p__d__subclass(c__WarmBloodedVertebrate,c__Vertebrate),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2955) ).
fof(f2112,axiom,
p__d__subclass(c__Mammal,c__WarmBloodedVertebrate),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2962) ).
fof(f2123,axiom,
p__d__subclass(c__Primate,c__Mammal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2973) ).
fof(f2127,axiom,
p__d__subclass(c__Hominid,c__Primate),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2977) ).
fof(f2128,axiom,
p__d__subclass(c__Human,c__Hominid),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2978) ).
fof(f2131,axiom,
p__d__subclass(c__Man,c__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2981) ).
fof(f2132,axiom,
! [X0] :
( p__d__instance(X0,c__Man)
=> p__attribute(X0,c__Male) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2982) ).
fof(f2588,axiom,
p__subAttribute(c__Liquid,c__Fluid),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA3566) ).
fof(f6281,axiom,
! [X0,X1] :
( ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Attribute) )
=> ( p__d__holds3(c__subAttribute,X0,X1)
<=> p__subAttribute(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',schemaBinaryRelationA3) ).
fof(f6855,axiom,
! [X0,X1] :
( p__subAttribute(X0,X1)
=> ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Attribute) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',typeA2) ).
fof(f6856,axiom,
! [X0,X1,X2] :
( p__d__holds3(X0,X1,X2)
=> p__d__instance(X0,c__BinaryRelation) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',typeA3) ).
fof(f6921,axiom,
! [X0,X1] :
( p__attribute(X0,X1)
=> ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Object) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',typeA68) ).
fof(f7234,axiom,
! [X0,X1] :
( p__initialPart(X0,X1)
=> ( p__d__subclass(X1,c__Object)
& p__d__subclass(X0,c__Object) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',typeA381) ).
fof(f7433,conjecture,
? [X0] :
( p__d__instance(X0,c__Object)
& p__d__instance(X0,c__Animal)
& ? [X1] :
( p__d__instance(X1,c__Attribute)
& p__subAttribute(X1,c__Male)
& p__attribute(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multipleMapping0018) ).
fof(f7434,negated_conjecture,
~ ? [X0] :
( p__d__instance(X0,c__Object)
& p__d__instance(X0,c__Animal)
& ? [X1] :
( p__d__instance(X1,c__Attribute)
& p__subAttribute(X1,c__Male)
& p__attribute(X0,X1) ) ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7524,plain,
! [X0] :
( ~ p__d__instance(X0,c__Object)
| ~ p__d__instance(X0,c__Animal)
| ! [X1] :
( ~ p__d__instance(X1,c__Attribute)
| ~ p__subAttribute(X1,c__Male)
| ~ p__attribute(X0,X1) ) ),
inference(ennf_transformation,[],[f7434]) ).
fof(f7525,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7526,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7525]) ).
fof(f7527,plain,
! [X0,X1] :
( ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Object) )
| ~ p__attribute(X0,X1) ),
inference(ennf_transformation,[],[f6921]) ).
fof(f7532,plain,
! [X0,X1] :
( ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Attribute) )
| ~ p__subAttribute(X0,X1) ),
inference(ennf_transformation,[],[f6855]) ).
fof(f7533,plain,
! [X0,X1,X2] :
( p__d__instance(X1,X0)
| ~ p__subAttribute(X1,X2)
| ~ p__d__instance(X2,X0) ),
inference(ennf_transformation,[],[f89]) ).
fof(f7534,plain,
! [X0,X1,X2] :
( p__d__instance(X1,X0)
| ~ p__subAttribute(X1,X2)
| ~ p__d__instance(X2,X0) ),
inference(flattening,[],[f7533]) ).
fof(f7551,plain,
! [X0] :
( p__attribute(X0,c__Male)
| ~ p__d__instance(X0,c__Man) ),
inference(ennf_transformation,[],[f2132]) ).
fof(f7552,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7553,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7552]) ).
fof(f7960,plain,
! [X0] :
( ? [X1] : p__d__instance(X1,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(ennf_transformation,[],[f110]) ).
fof(f8729,plain,
! [X0,X1] :
( ( p__d__holds3(c__subAttribute,X0,X1)
<=> p__subAttribute(X0,X1) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) ),
inference(ennf_transformation,[],[f6281]) ).
fof(f8730,plain,
! [X0,X1] :
( ( p__d__holds3(c__subAttribute,X0,X1)
<=> p__subAttribute(X0,X1) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) ),
inference(flattening,[],[f8729]) ).
fof(f8762,plain,
! [X0,X1,X2] :
( p__d__instance(X0,c__BinaryRelation)
| ~ p__d__holds3(X0,X1,X2) ),
inference(ennf_transformation,[],[f6856]) ).
fof(f8770,plain,
! [X0] :
( ( p__d__instance(X0,c__ReflexiveRelation)
<=> ! [X1] : p__d__holds3(X0,X1,X1) )
| ~ p__d__instance(X0,c__BinaryRelation) ),
inference(ennf_transformation,[],[f477]) ).
fof(f9344,plain,
! [X0,X1] :
( ( p__d__subclass(X1,c__Object)
& p__d__subclass(X0,c__Object) )
| ~ p__initialPart(X0,X1) ),
inference(ennf_transformation,[],[f7234]) ).
fof(f9727,plain,
! [X0] :
( p__d__instance(sK154(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK154]),skolemize(X1,sK154(X0))],[f7960]) ).
fof(f10084,plain,
! [X0,X1] :
( ( ( p__d__holds3(c__subAttribute,X0,X1)
| ~ p__subAttribute(X0,X1) )
& ( p__subAttribute(X0,X1)
| ~ p__d__holds3(c__subAttribute,X0,X1) ) )
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) ),
inference(nnf_transformation,[],[f8730]) ).
fof(f10109,plain,
! [X0] :
( ( ( p__d__instance(X0,c__ReflexiveRelation)
| ? [X1] : ~ p__d__holds3(X0,X1,X1) )
& ( ! [X1] : p__d__holds3(X0,X1,X1)
| ~ p__d__instance(X0,c__ReflexiveRelation) ) )
| ~ p__d__instance(X0,c__BinaryRelation) ),
inference(nnf_transformation,[],[f8770]) ).
fof(f10110,plain,
! [X0] :
( ( ( p__d__instance(X0,c__ReflexiveRelation)
| ? [X1] : ~ p__d__holds3(X0,X1,X1) )
& ( ! [X2] : p__d__holds3(X0,X2,X2)
| ~ p__d__instance(X0,c__ReflexiveRelation) ) )
| ~ p__d__instance(X0,c__BinaryRelation) ),
inference(rectify,[],[f10109]) ).
fof(f10111,plain,
! [X0] :
( ( ( p__d__instance(X0,c__ReflexiveRelation)
| ~ p__d__holds3(X0,sK529(X0),sK529(X0)) )
& ( ! [X2] : p__d__holds3(X0,X2,X2)
| ~ p__d__instance(X0,c__ReflexiveRelation) ) )
| ~ p__d__instance(X0,c__BinaryRelation) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK529]),skolemize(X1,sK529(X0))],[f10110]) ).
fof(f10429,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Object)
| ~ p__d__instance(X0,c__Animal)
| ~ p__d__instance(X1,c__Attribute)
| ~ p__subAttribute(X1,c__Male)
| ~ p__attribute(X0,X1) ),
inference(cnf_transformation,[],[f7524]) ).
fof(f10430,plain,
! [X2,X0,X1] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7526]) ).
fof(f10431,plain,
! [X0,X1] :
( p__d__instance(X0,c__Object)
| ~ p__attribute(X0,X1) ),
inference(cnf_transformation,[],[f7527]) ).
fof(f10432,plain,
! [X0,X1] :
( p__d__instance(X1,c__Attribute)
| ~ p__attribute(X0,X1) ),
inference(cnf_transformation,[],[f7527]) ).
fof(f10435,plain,
! [X0,X1] :
( p__d__instance(X0,c__Attribute)
| ~ p__subAttribute(X0,X1) ),
inference(cnf_transformation,[],[f7532]) ).
fof(f10436,plain,
! [X0,X1] :
( p__d__instance(X1,c__Attribute)
| ~ p__subAttribute(X0,X1) ),
inference(cnf_transformation,[],[f7532]) ).
fof(f10437,plain,
! [X2,X0,X1] :
( p__d__instance(X1,X0)
| ~ p__subAttribute(X1,X2)
| ~ p__d__instance(X2,X0) ),
inference(cnf_transformation,[],[f7534]) ).
fof(f10466,plain,
! [X0] :
( p__attribute(X0,c__Male)
| ~ p__d__instance(X0,c__Man) ),
inference(cnf_transformation,[],[f7551]) ).
fof(f10467,plain,
! [X2,X0,X1] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7553]) ).
fof(f10802,plain,
p__d__subclass(c__Man,c__Human),
inference(cnf_transformation,[],[f2131]) ).
fof(f11465,plain,
p__d__subclass(c__Object,c__Physical),
inference(cnf_transformation,[],[f115]) ).
fof(f11516,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[],[f112]) ).
fof(f11519,plain,
! [X0] :
( p__d__instance(sK154(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[],[f9727]) ).
fof(f11667,plain,
p__d__subclass(c__WarmBloodedVertebrate,c__Vertebrate),
inference(cnf_transformation,[],[f2105]) ).
fof(f11669,plain,
p__d__subclass(c__Vertebrate,c__Animal),
inference(cnf_transformation,[],[f2092]) ).
fof(f12181,plain,
p__d__subclass(c__Primate,c__Mammal),
inference(cnf_transformation,[],[f2123]) ).
fof(f12186,plain,
p__d__subclass(c__Mammal,c__WarmBloodedVertebrate),
inference(cnf_transformation,[],[f2112]) ).
fof(f12441,plain,
p__subAttribute(c__Liquid,c__Fluid),
inference(cnf_transformation,[],[f2588]) ).
fof(f13317,plain,
! [X0,X1] :
( p__subAttribute(X0,X1)
| ~ p__d__holds3(c__subAttribute,X0,X1)
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) ),
inference(cnf_transformation,[],[f10084]) ).
fof(f13318,plain,
! [X0,X1] :
( p__d__holds3(c__subAttribute,X0,X1)
| ~ p__subAttribute(X0,X1)
| ~ p__d__instance(X1,c__Attribute)
| ~ p__d__instance(X0,c__Attribute) ),
inference(cnf_transformation,[],[f10084]) ).
fof(f13319,plain,
p__d__instance(c__subAttribute,c__PartialOrderingRelation),
inference(cnf_transformation,[],[f86]) ).
fof(f13372,plain,
! [X2,X0,X1] :
( p__d__instance(X0,c__BinaryRelation)
| ~ p__d__holds3(X0,X1,X2) ),
inference(cnf_transformation,[],[f8762]) ).
fof(f13394,plain,
! [X2,X0] :
( p__d__holds3(X0,X2,X2)
| ~ p__d__instance(X0,c__ReflexiveRelation)
| ~ p__d__instance(X0,c__BinaryRelation) ),
inference(cnf_transformation,[],[f10111]) ).
fof(f13972,plain,
p__d__subclass(c__Hominid,c__Primate),
inference(cnf_transformation,[],[f2127]) ).
fof(f13975,plain,
p__d__subclass(c__Human,c__Hominid),
inference(cnf_transformation,[],[f2128]) ).
fof(f14139,plain,
p__d__subclass(c__PartialOrderingRelation,c__ReflexiveRelation),
inference(cnf_transformation,[],[f495]) ).
fof(f14713,plain,
! [X0,X1] :
( p__d__subclass(X1,c__Object)
| ~ p__initialPart(X0,X1) ),
inference(cnf_transformation,[],[f9344]) ).
fof(f14717,plain,
p__initialPart(c__VocalCords,c__Human),
inference(cnf_transformation,[],[f1691]) ).
fof(f15278,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Animal)
| ~ p__d__instance(X1,c__Attribute)
| ~ p__subAttribute(X1,c__Male)
| ~ p__attribute(X0,X1) ),
inference(forward_subsumption_resolution,[],[f10429,f10431]) ).
fof(f15279,plain,
! [X0,X1] :
( ~ p__subAttribute(X1,c__Male)
| ~ p__d__instance(X0,c__Animal)
| ~ p__attribute(X0,X1) ),
inference(forward_subsumption_resolution,[],[f15278,f10435]) ).
fof(f15280,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Animal)
| ~ p__attribute(X0,X1)
| ~ p__d__holds3(c__subAttribute,X1,c__Male)
| ~ p__d__instance(c__Male,c__Attribute)
| ~ p__d__instance(X1,c__Attribute) ),
inference(resolution,[],[f15279,f13317]) ).
fof(f15281,plain,
! [X0,X1] :
( ~ p__d__holds3(c__subAttribute,X1,c__Male)
| ~ p__attribute(X0,X1)
| ~ p__d__instance(X0,c__Animal)
| ~ p__d__instance(c__Male,c__Attribute) ),
inference(forward_subsumption_resolution,[],[f15280,f10432]) ).
fof(f15287,plain,
! [X0] :
( ~ p__attribute(X0,c__Male)
| ~ p__d__instance(X0,c__Animal)
| ~ p__d__instance(c__Male,c__Attribute)
| ~ p__d__instance(c__subAttribute,c__ReflexiveRelation)
| ~ p__d__instance(c__subAttribute,c__BinaryRelation) ),
inference(resolution,[],[f15281,f13394]) ).
fof(f15289,plain,
! [X0] :
( ~ p__attribute(X0,c__Male)
| ~ p__d__instance(X0,c__Animal)
| ~ p__d__instance(c__subAttribute,c__ReflexiveRelation)
| ~ p__d__instance(c__subAttribute,c__BinaryRelation) ),
inference(forward_subsumption_resolution,[],[f15287,f10432]) ).
fof(f15295,plain,
! [X0] :
( ~ p__d__instance(c__subAttribute,c__ReflexiveRelation)
| ~ p__d__instance(X0,c__Animal)
| ~ p__d__instance(c__subAttribute,c__BinaryRelation)
| ~ p__d__instance(X0,c__Man) ),
inference(resolution,[],[f15289,f10466]) ).
fof(f15335,plain,
! [X0,X1] :
( ~ p__d__subclass(X1,c__ReflexiveRelation)
| ~ p__d__instance(c__subAttribute,c__BinaryRelation)
| ~ p__d__instance(X0,c__Man)
| ~ p__d__instance(c__subAttribute,X1)
| ~ p__d__instance(X0,c__Animal) ),
inference(resolution,[],[f15295,f10430]) ).
fof(f15535,plain,
! [X0] :
( ~ p__d__instance(c__subAttribute,c__BinaryRelation)
| ~ p__d__instance(X0,c__Man)
| ~ p__d__instance(c__subAttribute,c__PartialOrderingRelation)
| ~ p__d__instance(X0,c__Animal) ),
inference(resolution,[],[f15335,f14139]) ).
fof(f15538,plain,
! [X0] :
( ~ p__d__instance(c__subAttribute,c__BinaryRelation)
| ~ p__d__instance(X0,c__Man)
| ~ p__d__instance(X0,c__Animal) ),
inference(forward_subsumption_resolution,[],[f15535,f13319]) ).
fof(f15539,plain,
! [X2,X0,X1] :
( ~ p__d__holds3(c__subAttribute,X1,X2)
| ~ p__d__instance(X0,c__Animal)
| ~ p__d__instance(X0,c__Man) ),
inference(resolution,[],[f15538,f13372]) ).
fof(f15567,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X0,c__Animal)
| ~ p__d__instance(X0,c__Man)
| ~ p__subAttribute(X1,X2)
| ~ p__d__instance(X2,c__Attribute)
| ~ p__d__instance(X1,c__Attribute) ),
inference(resolution,[],[f15539,f13318]) ).
fof(f15583,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X0,c__Animal)
| ~ p__d__instance(X0,c__Man)
| ~ p__subAttribute(X1,X2)
| ~ p__d__instance(X2,c__Attribute) ),
inference(forward_subsumption_resolution,[],[f15567,f10437]) ).
fof(f15585,plain,
! [X2,X0,X1] :
( ~ p__subAttribute(X1,X2)
| ~ p__d__instance(X0,c__Man)
| ~ p__d__instance(X0,c__Animal) ),
inference(forward_subsumption_resolution,[],[f15583,f10436]) ).
fof(f15588,plain,
! [X0] :
( ~ p__d__instance(X0,c__Man)
| ~ p__d__instance(X0,c__Animal) ),
inference(resolution,[],[f15585,f12441]) ).
fof(f15648,plain,
( ~ p__d__subclass(c__Man,c__Entity)
| ~ p__d__instance(sK154(c__Man),c__Animal) ),
inference(resolution,[],[f15588,f11519]) ).
fof(f15736,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(c__Man,X0)
| ~ p__d__instance(sK154(c__Man),c__Animal) ),
inference(resolution,[],[f15648,f10467]) ).
fof(f18173,plain,
( ~ p__d__subclass(c__Man,c__Physical)
| ~ p__d__instance(sK154(c__Man),c__Animal) ),
inference(resolution,[],[f15736,f11516]) ).
fof(f18184,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Physical)
| ~ p__d__subclass(c__Man,X0)
| ~ p__d__instance(sK154(c__Man),c__Animal) ),
inference(resolution,[],[f18173,f10467]) ).
fof(f18291,plain,
( ~ p__d__subclass(c__Man,c__Object)
| ~ p__d__instance(sK154(c__Man),c__Animal) ),
inference(resolution,[],[f18184,f11465]) ).
fof(f18302,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Object)
| ~ p__d__subclass(c__Man,X0)
| ~ p__d__instance(sK154(c__Man),c__Animal) ),
inference(resolution,[],[f18291,f10467]) ).
fof(f18564,plain,
! [X0,X1] :
( ~ p__initialPart(X1,X0)
| ~ p__d__instance(sK154(c__Man),c__Animal)
| ~ p__d__subclass(c__Man,X0) ),
inference(resolution,[],[f18302,f14713]) ).
fof(f18736,plain,
( ~ p__d__instance(sK154(c__Man),c__Animal)
| ~ p__d__subclass(c__Man,c__Human) ),
inference(resolution,[],[f18564,f14717]) ).
fof(f18739,plain,
~ p__d__instance(sK154(c__Man),c__Animal),
inference(forward_subsumption_resolution,[],[f18736,f10802]) ).
fof(f18750,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Animal)
| ~ p__d__instance(sK154(c__Man),X0) ),
inference(resolution,[],[f18739,f10430]) ).
fof(f18822,plain,
~ p__d__instance(sK154(c__Man),c__Vertebrate),
inference(resolution,[],[f18750,f11669]) ).
fof(f18830,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Vertebrate)
| ~ p__d__instance(sK154(c__Man),X0) ),
inference(resolution,[],[f18822,f10430]) ).
fof(f19156,plain,
~ p__d__instance(sK154(c__Man),c__WarmBloodedVertebrate),
inference(resolution,[],[f18830,f11667]) ).
fof(f19160,plain,
! [X0] :
( ~ p__d__subclass(X0,c__WarmBloodedVertebrate)
| ~ p__d__instance(sK154(c__Man),X0) ),
inference(resolution,[],[f19156,f10430]) ).
fof(f19608,plain,
~ p__d__instance(sK154(c__Man),c__Mammal),
inference(resolution,[],[f19160,f12186]) ).
fof(f19612,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Mammal)
| ~ p__d__instance(sK154(c__Man),X0) ),
inference(resolution,[],[f19608,f10430]) ).
fof(f19960,plain,
~ p__d__instance(sK154(c__Man),c__Primate),
inference(resolution,[],[f19612,f12181]) ).
fof(f20098,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Primate)
| ~ p__d__instance(sK154(c__Man),X0) ),
inference(resolution,[],[f19960,f10430]) ).
fof(f20814,plain,
~ p__d__instance(sK154(c__Man),c__Hominid),
inference(resolution,[],[f20098,f13972]) ).
fof(f20819,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Hominid)
| ~ p__d__instance(sK154(c__Man),X0) ),
inference(resolution,[],[f20814,f10430]) ).
fof(f21164,plain,
~ p__d__instance(sK154(c__Man),c__Human),
inference(resolution,[],[f20819,f13975]) ).
fof(f21187,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Human)
| ~ p__d__instance(sK154(c__Man),X0) ),
inference(resolution,[],[f21164,f10430]) ).
fof(f21327,plain,
~ p__d__instance(sK154(c__Man),c__Man),
inference(resolution,[],[f21187,f10802]) ).
fof(f21331,plain,
~ p__d__subclass(c__Man,c__Entity),
inference(resolution,[],[f21327,f11519]) ).
fof(f21362,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Entity)
| ~ p__d__subclass(c__Man,X0) ),
inference(resolution,[],[f21331,f10467]) ).
fof(f21432,plain,
~ p__d__subclass(c__Man,c__Physical),
inference(resolution,[],[f21362,f11516]) ).
fof(f21437,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Physical)
| ~ p__d__subclass(c__Man,X0) ),
inference(resolution,[],[f21432,f10467]) ).
fof(f21546,plain,
~ p__d__subclass(c__Man,c__Object),
inference(resolution,[],[f21437,f11465]) ).
fof(f21562,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Object)
| ~ p__d__subclass(c__Man,X0) ),
inference(resolution,[],[f21546,f10467]) ).
fof(f21759,plain,
! [X0,X1] :
( ~ p__initialPart(X1,X0)
| ~ p__d__subclass(c__Man,X0) ),
inference(resolution,[],[f21562,f14713]) ).
fof(f21960,plain,
~ p__d__subclass(c__Man,c__Human),
inference(resolution,[],[f21759,f14717]) ).
fof(f21963,plain,
$false,
inference(forward_subsumption_resolution,[],[f21960,f10802]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR244+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n009.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 23:53:13 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 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
% 7.83/2.00 % (3611869)Detected formulas, will run a generic FOF schedule.
% 7.83/2.00 % (3611880)dis-21_1_sil=8000:lcm=predicate:random_seed=3412198398:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 7.83/2.00 % (3611879)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2092876544:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.83/2.00 % (3611875)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=2012126801:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.83/2.00 % (3611876)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=3500941553:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.83/2.00 % (3611874)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=3881706480:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.83/2.00 % (3611877)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1691982100:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.83/2.00 % (3611878)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2003767345:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.83/2.00 % (3611877)Refutation not found, incomplete strategy
% 7.83/2.00 % (3611877)------------------------------
% 7.83/2.00 % (3611877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.83/2.00 % (3611877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.83/2.00 % (3611877)CaDiCaL version: 2.1.3
% 7.83/2.00 % (3611877)Termination reason: Refutation not found, incomplete strategy
% 7.83/2.00 % (3611877)Time elapsed: 0.016 s
% 7.83/2.00 % (3611877)Peak memory usage: 93 MB
% 7.83/2.00 % (3611877)Instructions burned: 24 (million)
% 7.83/2.00 % (3611878)Refutation not found, incomplete strategy
% 7.83/2.00 % (3611878)------------------------------
% 7.83/2.00 % (3611878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.83/2.00 % (3611878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.83/2.00 % (3611878)CaDiCaL version: 2.1.3
% 7.83/2.00 % (3611878)Termination reason: Refutation not found, incomplete strategy
% 7.83/2.00 % (3611878)Time elapsed: 0.017 s
% 7.83/2.00 % (3611878)Peak memory usage: 93 MB
% 7.83/2.00 % (3611878)Instructions burned: 25 (million)
% 7.83/2.00 % (3611880)Instruction limit reached!
% 7.83/2.00 % (3611880)------------------------------
% 7.83/2.00 % (3611880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.83/2.00 % (3611880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.83/2.00 % (3611880)CaDiCaL version: 2.1.3
% 7.83/2.00 % (3611880)Termination reason: Instruction limit
% 7.83/2.00 % (3611880)Termination phase: Saturation
% 7.83/2.00 % (3611880)Time elapsed: 0.042 s
% 7.83/2.00 % (3611880)Peak memory usage: 95 MB
% 7.83/2.00 % (3611880)Instructions burned: 131 (million)
% 7.83/2.00 % (3611879)Instruction limit reached!
% 7.83/2.00 % (3611879)------------------------------
% 7.83/2.00 % (3611879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.83/2.00 % (3611879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.83/2.00 % (3611879)CaDiCaL version: 2.1.3
% 7.83/2.00 % (3611879)Termination reason: Instruction limit
% 7.83/2.00 % (3611879)Termination phase: Preprocessing 3
% 7.83/2.00 % (3611879)Time elapsed: 0.086 s
% 7.83/2.00 % (3611879)Peak memory usage: 94 MB
% 7.83/2.00 % (3611879)Instructions burned: 140 (million)
% 7.83/2.00 % (3611888)lrs+10_1_sil=8000:sp=occurrence:random_seed=1485328306:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 7.83/2.00 % (3611888)Instruction limit reached!
% 7.83/2.00 % (3611888)------------------------------
% 7.83/2.00 % (3611888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.83/2.00 % (3611888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.83/2.00 % (3611888)CaDiCaL version: 2.1.3
% 7.83/2.00 % (3611888)Termination reason: Instruction limit
% 7.83/2.00 % (3611888)Termination phase: Saturation
% 7.83/2.00 % (3611888)Time elapsed: 0.072 s
% 7.83/2.00 % (3611888)Peak memory usage: 94 MB
% 7.83/2.00 % (3611888)Instructions burned: 286 (million)
% 13.72/2.48 % (3611889)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1063906112:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.72/2.48 % (3611889)Refutation not found, incomplete strategy
% 13.72/2.48 % (3611889)------------------------------
% 13.72/2.48 % (3611889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.72/2.48 % (3611889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.72/2.48 % (3611889)CaDiCaL version: 2.1.3
% 13.72/2.48 % (3611889)Termination reason: Refutation not found, incomplete strategy
% 13.72/2.48 % (3611889)Time elapsed: 0.033 s
% 13.72/2.48 % (3611889)Peak memory usage: 93 MB
% 13.72/2.48 % (3611889)Instructions burned: 60 (million)
% 13.72/2.48 % (3611878)------------------------------
% 13.72/2.48 % (3611878)------------------------------
% 13.72/2.48 % (3611877)------------------------------
% 13.72/2.48 % (3611877)------------------------------
% 13.72/2.48 % (3611891)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3817686018:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 13.72/2.48 % (3611891)Refutation not found, incomplete strategy
% 13.72/2.48 % (3611891)------------------------------
% 13.72/2.48 % (3611891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.72/2.48 % (3611891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.72/2.48 % (3611891)CaDiCaL version: 2.1.3
% 13.72/2.48 % (3611891)Termination reason: Refutation not found, incomplete strategy
% 13.72/2.48 % (3611891)Time elapsed: 0.009 s
% 13.72/2.48 % (3611891)Peak memory usage: 93 MB
% 13.72/2.48 % (3611891)Instructions burned: 20 (million)
% 13.72/2.48 % (3611894)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3921764392:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 13.72/2.48 % (3611893)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=2911772060:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 13.72/2.48 % (3611894)Refutation not found, incomplete strategy
% 13.72/2.48 % (3611894)------------------------------
% 13.72/2.48 % (3611894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.72/2.48 % (3611894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.72/2.48 % (3611894)CaDiCaL version: 2.1.3
% 13.72/2.48 % (3611894)Termination reason: Refutation not found, incomplete strategy
% 13.72/2.48 % (3611894)Time elapsed: 0.028 s
% 13.72/2.48 % (3611894)Peak memory usage: 94 MB
% 13.72/2.48 % (3611894)Instructions burned: 37 (million)
% 13.72/2.48 % (3611891)------------------------------
% 13.72/2.48 % (3611891)------------------------------
% 13.72/2.48 % (3611889)------------------------------
% 13.72/2.48 % (3611889)------------------------------
% 13.72/2.48 % (3611898)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4210932381:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 13.72/2.48 % (3611893)Instruction limit reached!
% 13.72/2.48 % (3611893)------------------------------
% 13.72/2.48 % (3611893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.72/2.48 % (3611893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.72/2.48 % (3611893)CaDiCaL version: 2.1.3
% 13.72/2.48 % (3611893)Termination reason: Instruction limit
% 13.72/2.48 % (3611893)Termination phase: Saturation
% 13.72/2.48 % (3611893)Time elapsed: 0.135 s
% 13.72/2.48 % (3611893)Peak memory usage: 98 MB
% 13.72/2.48 % (3611893)Instructions burned: 249 (million)
% 13.72/2.48 % (3611876)Refutation not found, incomplete strategy
% 13.72/2.48 % (3611876)------------------------------
% 13.72/2.48 % (3611876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.72/2.48 % (3611876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.72/2.48 % (3611876)CaDiCaL version: 2.1.3
% 13.72/2.48 % (3611876)Termination reason: Refutation not found, incomplete strategy
% 13.72/2.48 % (3611876)Time elapsed: 0.636 s
% 13.72/2.48 % (3611876)Peak memory usage: 136 MB
% 13.72/2.48 % (3611876)Instructions burned: 959 (million)
% 13.72/2.48 % (3611899)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=773742314:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 13.72/2.48 % (3611899)Refutation not found, incomplete strategy
% 13.72/2.48 % (3611899)------------------------------
% 13.72/2.48 % (3611899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.72/2.48 % (3611899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.52/4.09 % (3611899)CaDiCaL version: 2.1.3
% 25.52/4.09 % (3611899)Termination reason: Refutation not found, incomplete strategy
% 25.52/4.09 % (3611899)Time elapsed: 0.018 s
% 25.52/4.09 % (3611899)Peak memory usage: 93 MB
% 25.52/4.09 % (3611899)Instructions burned: 24 (million)
% 25.52/4.09 % (3611894)------------------------------
% 25.52/4.09 % (3611894)------------------------------
% 25.52/4.09 % (3611901)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3957894894:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 25.52/4.09 % (3611901)Instruction limit reached!
% 25.52/4.09 % (3611901)------------------------------
% 25.52/4.09 % (3611901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.52/4.09 % (3611901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.52/4.09 % (3611901)CaDiCaL version: 2.1.3
% 25.52/4.09 % (3611901)Termination reason: Instruction limit
% 25.52/4.09 % (3611901)Termination phase: Property scanning
% 25.52/4.09 % (3611901)Time elapsed: 0.081 s
% 25.52/4.09 % (3611901)Peak memory usage: 96 MB
% 25.52/4.09 % (3611901)Instructions burned: 128 (million)
% 25.52/4.09 % (3611904)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3547141283:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 25.52/4.09 % (3611876)------------------------------
% 25.52/4.09 % (3611876)------------------------------
% 25.52/4.09 % (3611904)Instruction limit reached!
% 25.52/4.09 % (3611904)------------------------------
% 25.52/4.09 % (3611904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.52/4.09 % (3611904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.52/4.09 % (3611904)CaDiCaL version: 2.1.3
% 25.52/4.09 % (3611904)Termination reason: Instruction limit
% 25.52/4.09 % (3611904)Termination phase: Property scanning
% 25.52/4.09 % (3611904)Time elapsed: 0.063 s
% 25.52/4.09 % (3611904)Peak memory usage: 91 MB
% 25.52/4.09 % (3611904)Instructions burned: 114 (million)
% 25.52/4.09 % (3611899)------------------------------
% 25.52/4.09 % (3611899)------------------------------
% 25.52/4.09 % (3611905)lrs+10_1_sil=8000:sp=occurrence:random_seed=3415123819:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 25.52/4.09 % (3611908)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2439126656:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 25.52/4.09 % (3611907)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2241657139:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 25.52/4.09 % (3611907)Refutation not found, incomplete strategy
% 25.52/4.09 % (3611907)------------------------------
% 25.52/4.09 % (3611907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.52/4.09 % (3611907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.52/4.09 % (3611907)CaDiCaL version: 2.1.3
% 25.52/4.09 % (3611907)Termination reason: Refutation not found, incomplete strategy
% 25.52/4.09 % (3611907)Time elapsed: 0.016 s
% 25.52/4.09 % (3611907)Peak memory usage: 93 MB
% 25.52/4.09 % (3611907)Instructions burned: 19 (million)
% 25.52/4.09 % (3611910)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3606251510:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 25.52/4.09 % (3611910)Refutation not found, incomplete strategy
% 25.52/4.09 % (3611910)------------------------------
% 25.52/4.09 % (3611910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.52/4.09 % (3611910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.52/4.09 % (3611910)CaDiCaL version: 2.1.3
% 25.52/4.09 % (3611910)Termination reason: Refutation not found, incomplete strategy
% 25.52/4.09 % (3611910)Time elapsed: 0.019 s
% 25.52/4.09 % (3611910)Peak memory usage: 94 MB
% 25.52/4.09 % (3611910)Instructions burned: 25 (million)
% 25.52/4.09 % (3611907)------------------------------
% 25.52/4.09 % (3611907)------------------------------
% 25.52/4.09 % (3611910)------------------------------
% 25.52/4.09 % (3611910)------------------------------
% 25.52/4.09 % (3611898)Instruction limit reached!
% 25.52/4.09 % (3611898)------------------------------
% 25.52/4.09 % (3611898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.52/4.09 % (3611898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.52/4.09 % (3611898)CaDiCaL version: 2.1.3
% 13.62/4.70 % (3611898)Termination reason: Instruction limit
% 13.62/4.70 % (3611898)Termination phase: Saturation
% 13.62/4.70 % (3611898)Time elapsed: 0.879 s
% 13.62/4.70 % (3611898)Peak memory usage: 211 MB
% 13.62/4.70 % (3611898)Instructions burned: 2353 (million)
% 13.62/4.70 % (3611914)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4252003886:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 13.62/4.70 % (3611905)Instruction limit reached!
% 13.62/4.70 % (3611905)------------------------------
% 13.62/4.70 % (3611905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/4.70 % (3611905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/4.70 % (3611905)CaDiCaL version: 2.1.3
% 13.62/4.70 % (3611905)Termination reason: Instruction limit
% 13.62/4.70 % (3611905)Termination phase: Saturation
% 13.62/4.70 % (3611905)Time elapsed: 0.537 s
% 13.62/4.70 % (3611905)Peak memory usage: 111 MB
% 13.62/4.70 % (3611905)Instructions burned: 907 (million)
% 13.62/4.70 % (3611915)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1560640711:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 13.62/4.70 % (3611917)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=1692165293:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 13.62/4.70 % (3611917)Refutation not found, incomplete strategy
% 13.62/4.70 % (3611917)------------------------------
% 13.62/4.70 % (3611917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/4.70 % (3611917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/4.70 % (3611917)CaDiCaL version: 2.1.3
% 13.62/4.70 % (3611917)Termination reason: Refutation not found, incomplete strategy
% 13.62/4.70 % (3611917)Time elapsed: 0.023 s
% 13.62/4.70 % (3611917)Peak memory usage: 94 MB
% 13.62/4.70 % (3611917)Instructions burned: 80 (million)
% 13.62/4.70 % (3611914)Refutation not found, incomplete strategy
% 13.62/4.70 % (3611914)------------------------------
% 13.62/4.70 % (3611914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/4.70 % (3611914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/4.70 % (3611914)CaDiCaL version: 2.1.3
% 13.62/4.70 % (3611914)Termination reason: Refutation not found, incomplete strategy
% 13.62/4.70 % (3611914)Time elapsed: 0.092 s
% 13.62/4.70 % (3611914)Peak memory usage: 96 MB
% 13.62/4.70 % (3611914)Instructions burned: 151 (million)
% 13.62/4.70 % (3611919)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2252636426:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 13.62/4.70 % (3611919)Instruction limit reached!
% 13.62/4.70 % (3611919)------------------------------
% 13.62/4.70 % (3611919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/4.70 % (3611919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/4.70 % (3611919)CaDiCaL version: 2.1.3
% 13.62/4.70 % (3611919)Termination reason: Instruction limit
% 13.62/4.70 % (3611919)Termination phase: Preprocessing 2
% 13.62/4.70 % (3611919)Time elapsed: 0.073 s
% 13.62/4.70 % (3611919)Peak memory usage: 92 MB
% 13.62/4.70 % (3611919)Instructions burned: 134 (million)
% 13.62/4.70 % (3611917)------------------------------
% 13.62/4.70 % (3611917)------------------------------
% 13.62/4.70 % (3611924)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4024110378:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 13.62/4.70 % (3611914)------------------------------
% 13.62/4.70 % (3611914)------------------------------
% 13.62/4.70 % (3611923)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1168879122:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/141Mi)
% 13.62/4.70 % (3611923)Refutation not found, incomplete strategy
% 13.62/4.70 % (3611923)------------------------------
% 13.62/4.70 % (3611923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/4.70 % (3611923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/4.70 % (3611923)CaDiCaL version: 2.1.3
% 13.62/4.70 % (3611923)Termination reason: Refutation not found, incomplete strategy
% 13.62/4.70 % (3611923)Time elapsed: 0.018 s
% 13.62/4.70 % (3611923)Peak memory usage: 93 MB
% 13.62/4.70 % (3611923)Instructions burned: 24 (million)
% 13.62/4.70 % (3611924)Instruction limit reached!
% 13.62/4.70 % (3611924)------------------------------
% 13.62/4.70 % (3611924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/4.70 % (3611924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/4.70 % (3611924)CaDiCaL version: 2.1.3
% 13.62/4.70 % (3611924)Termination reason: Instruction limit
% 13.62/4.70 % (3611924)Termination phase: Saturation
% 13.62/4.70 % (3611924)Time elapsed: 0.124 s
% 13.62/4.70 % (3611924)Peak memory usage: 98 MB
% 13.62/4.70 % (3611924)Instructions burned: 432 (million)
% 13.62/4.70 % (3611926)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=1934780609:i=6060:aac=none:ins=25_2980 on theBenchmark for (2980ds/6060Mi)
% 13.62/4.70 % (3611928)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=639335970:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2979 on theBenchmark for (2979ds/150Mi)
% 13.62/4.70 % (3611928)Instruction limit reached!
% 13.62/4.70 % (3611928)------------------------------
% 13.62/4.70 % (3611928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/4.70 % (3611928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/4.70 % (3611928)CaDiCaL version: 2.1.3
% 13.62/4.70 % (3611928)Termination reason: Instruction limit
% 13.62/4.70 % (3611928)Termination phase: Property scanning
% 13.62/4.70 % (3611928)Time elapsed: 0.051 s
% 13.62/4.70 % (3611928)Peak memory usage: 96 MB
% 13.62/4.70 % (3611928)Instructions burned: 152 (million)
% 13.62/4.70 % (3611923)------------------------------
% 13.62/4.70 % (3611923)------------------------------
% 13.62/4.70 % (3611931)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1162370193:i=14155:bd=all_2977 on theBenchmark for (2977ds/14155Mi)
% 13.62/4.70 % (3611932)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3607839172:i=667:av=off:fsr=off_2977 on theBenchmark for (2977ds/667Mi)
% 13.62/4.70 % (3611932)Refutation not found, incomplete strategy
% 13.62/4.70 % (3611932)------------------------------
% 13.62/4.70 % (3611932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/4.70 % (3611932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/4.70 % (3611932)CaDiCaL version: 2.1.3
% 13.62/4.70 % (3611932)Termination reason: Refutation not found, incomplete strategy
% 13.62/4.70 % (3611932)Time elapsed: 0.229 s
% 13.62/4.70 % (3611932)Peak memory usage: 103 MB
% 13.62/4.70 % (3611932)Instructions burned: 417 (million)
% 13.62/4.70 % (3611932)------------------------------
% 13.62/4.70 % (3611932)------------------------------
% 13.62/4.70 % (3611935)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=528277064:s2a=on:i=185:s2at=1.8:fdi=4_2971 on theBenchmark for (2971ds/185Mi)
% 13.62/4.70 % (3611935)Instruction limit reached!
% 13.62/4.70 % (3611935)------------------------------
% 13.62/4.70 % (3611935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/4.70 % (3611935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/4.70 % (3611935)CaDiCaL version: 2.1.3
% 13.62/4.70 % (3611935)Termination reason: Instruction limit
% 13.62/4.70 % (3611935)Termination phase: Property scanning
% 13.62/4.70 % (3611935)Time elapsed: 0.119 s
% 13.62/4.70 % (3611935)Peak memory usage: 96 MB
% 13.62/4.70 % (3611935)Instructions burned: 186 (million)
% 13.62/4.70 % (3611937)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1753532877:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2968 on theBenchmark for (2968ds/193Mi)
% 13.62/4.70 % (3611937)Refutation not found, incomplete strategy
% 13.62/4.70 % (3611937)------------------------------
% 13.62/4.70 % (3611937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.62/4.70 % (3611937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/4.70 % (3611937)CaDiCaL version: 2.1.3
% 13.62/4.70 % (3611937)Termination reason: Refutation not found, incomplete strategy
% 13.62/4.70 % (3611937)Time elapsed: 0.031 s
% 13.62/4.70 % (3611937)Peak memory usage: 94 MB
% 13.62/4.70 % (3611937)Instructions burned: 45 (million)
% 13.62/4.70 % (3611937)------------------------------
% 13.62/4.70 % (3611937)------------------------------
% 13.62/4.70 % (3611939)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3139728619:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2964 on theBenchmark for (2964ds/4850Mi)
% 13.62/4.70 % (3611939)First to succeed.
% 13.62/4.70 % (3611939)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3611869"
% 13.62/4.70 % (3611939)Refutation found. Thanks to Tanya!
% 13.62/4.70 % SZS status Theorem for theBenchmark
% 13.62/4.70 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/4.80 % (3611939)------------------------------
% 0.18/4.80 % (3611939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/4.80 % (3611939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/4.80 % (3611939)CaDiCaL version: 2.1.3
% 0.18/4.80 % (3611939)Termination reason: Refutation
% 0.18/4.80 % (3611939)Time elapsed: 0.332 s
% 0.18/4.80 % (3611939)Peak memory usage: 101 MB
% 0.18/4.80 % (3611939)Instructions burned: 649 (million)
% 0.18/4.80 % (3611939)------------------------------
% 0.18/4.80 % (3611939)------------------------------
% 0.18/4.80 % (3611869)Success in time 4.304 s
% 0.18/4.80 % Vampire exiting
%------------------------------------------------------------------------------