%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR170+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:00 AM UTC 2026
% Result : Theorem 151.21s 22.39s
% Output : Refutation 151.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 23
% Syntax : Number of formulae : 95 ( 57 unt; 3 def)
% Number of atoms : 213 ( 16 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 201 ( 83 ~; 74 |; 37 &)
% ( 1 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 18 con; 0-2 aty)
% Number of variables : 101 ( 83 !; 18 ?)
% 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/sandbox/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/sandbox/benchmark/theBenchmark.p',predefinitionsA12) ).
fof(f5,axiom,
! [X0,X1] :
( p__d__disjoint(X0,X1)
<=> ! [X2] :
( ~ p__d__instance(X2,X0)
| ~ p__d__instance(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',predefinitionsA15) ).
fof(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA176) ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA178) ).
fof(f115,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA181) ).
fof(f171,axiom,
p__d__subclass(c__CorpuscularObject,c__SelfConnectedObject),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA251) ).
fof(f176,axiom,
p__d__subclass(c__Collection,c__Object),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA256) ).
fof(f177,axiom,
p__d__disjoint(c__Collection,c__SelfConnectedObject),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA257) ).
fof(f225,axiom,
p__d__subclass(c__Agent,c__Object),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA312) ).
fof(f2059,axiom,
p__d__subclass(c__OrganicObject,c__CorpuscularObject),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA2902) ).
fof(f2062,axiom,
p__d__subclass(c__Organism,c__OrganicObject),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA2905) ).
fof(f2063,axiom,
p__d__subclass(c__Organism,c__Agent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA2906) ).
fof(f2681,axiom,
p__d__subclass(c__DevelopmentalAttribute,c__BiologicalAttribute),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA3681) ).
fof(f2686,axiom,
! [X0] :
( p__d__instance(X0,c__Organism)
=> ? [X1] :
( p__d__instance(X1,c__DevelopmentalAttribute)
& p__attribute(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mergeA3688) ).
fof(f4987,axiom,
p__d__instance(c__LineFormation,c__ShapeAttribute),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',miloA2821) ).
fof(f5390,axiom,
p__d__subclass(c__Convoy,c__Collection),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',miloA3298) ).
fof(f5392,axiom,
! [X0] :
( p__d__instance(X0,c__Convoy)
=> p__attribute(X0,c__LineFormation) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',miloA3301) ).
fof(f6921,axiom,
! [X0,X1] :
( p__attribute(X0,X1)
=> ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Object) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',typeA68) ).
fof(f7433,conjecture,
? [X0,X1] :
( p__d__instance(X1,c__Object)
& p__d__instance(X0,c__Object)
& ? [X2] :
( p__d__instance(X2,c__Attribute)
& p__d__instance(X2,c__BiologicalAttribute)
& p__attribute(X1,X2) )
& ? [X2] :
( p__d__instance(X2,c__Attribute)
& p__d__instance(X2,c__ShapeAttribute)
& p__attribute(X0,X2) )
& X0 != X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antonymPattern30817) ).
fof(f7434,negated_conjecture,
~ ? [X0,X1] :
( p__d__instance(X1,c__Object)
& p__d__instance(X0,c__Object)
& ? [X2] :
( p__d__instance(X2,c__Attribute)
& p__d__instance(X2,c__BiologicalAttribute)
& p__attribute(X1,X2) )
& ? [X2] :
( p__d__instance(X2,c__Attribute)
& p__d__instance(X2,c__ShapeAttribute)
& p__attribute(X0,X2) )
& X0 != X1 ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7435,plain,
~ ? [X0,X1] :
( p__d__instance(X1,c__Object)
& p__d__instance(X0,c__Object)
& ? [X2] :
( p__d__instance(X2,c__Attribute)
& p__d__instance(X2,c__BiologicalAttribute)
& p__attribute(X1,X2) )
& ? [X3] :
( p__d__instance(X3,c__Attribute)
& p__d__instance(X3,c__ShapeAttribute)
& p__attribute(X0,X3) )
& X0 != X1 ),
inference(rectify,[],[f7434]) ).
fof(f7498,plain,
! [X0,X1] :
( ~ p__d__instance(X1,c__Object)
| ~ p__d__instance(X0,c__Object)
| ! [X2] :
( ~ p__d__instance(X2,c__Attribute)
| ~ p__d__instance(X2,c__BiologicalAttribute)
| ~ p__attribute(X1,X2) )
| ! [X3] :
( ~ p__d__instance(X3,c__Attribute)
| ~ p__d__instance(X3,c__ShapeAttribute)
| ~ p__attribute(X0,X3) )
| X0 = X1 ),
inference(ennf_transformation,[],[f7435]) ).
fof(f7501,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7502,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7501]) ).
fof(f7504,plain,
! [X0,X1] :
( ( p__d__instance(X1,c__Attribute)
& p__d__instance(X0,c__Object) )
| ~ p__attribute(X0,X1) ),
inference(ennf_transformation,[],[f6921]) ).
fof(f7515,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7516,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7515]) ).
fof(f7534,plain,
! [X0] :
( p__attribute(X0,c__LineFormation)
| ~ p__d__instance(X0,c__Convoy) ),
inference(ennf_transformation,[],[f5392]) ).
fof(f7581,plain,
! [X0] :
( ? [X1] :
( p__d__instance(X1,c__DevelopmentalAttribute)
& p__attribute(X0,X1) )
| ~ p__d__instance(X0,c__Organism) ),
inference(ennf_transformation,[],[f2686]) ).
fof(f7643,plain,
! [X0] :
( ? [X1] : p__d__instance(X1,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(ennf_transformation,[],[f110]) ).
fof(f7916,plain,
! [X0] :
( ( p__d__instance(sK34(X0),c__DevelopmentalAttribute)
& p__attribute(X0,sK34(X0)) )
| ~ p__d__instance(X0,c__Organism) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(X1,sK34(X0))],[f7581]) ).
fof(f7953,plain,
! [X0] :
( p__d__instance(sK59(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK59]),skolemize(X1,sK59(X0))],[f7643]) ).
fof(f7957,plain,
! [X0,X1] :
( ( p__d__disjoint(X0,X1)
| ? [X2] :
( p__d__instance(X2,X0)
& p__d__instance(X2,X1) ) )
& ( ! [X2] :
( ~ p__d__instance(X2,X0)
| ~ p__d__instance(X2,X1) )
| ~ p__d__disjoint(X0,X1) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f7958,plain,
! [X0,X1] :
( ( p__d__disjoint(X0,X1)
| ? [X2] :
( p__d__instance(X2,X0)
& p__d__instance(X2,X1) ) )
& ( ! [X3] :
( ~ p__d__instance(X3,X0)
| ~ p__d__instance(X3,X1) )
| ~ p__d__disjoint(X0,X1) ) ),
inference(rectify,[],[f7957]) ).
fof(f7959,plain,
! [X0,X1] :
( ( p__d__disjoint(X0,X1)
| ( p__d__instance(sK63(X0,X1),X0)
& p__d__instance(sK63(X0,X1),X1) ) )
& ( ! [X3] :
( ~ p__d__instance(X3,X0)
| ~ p__d__instance(X3,X1) )
| ~ p__d__disjoint(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK63]),skolemize(X2,sK63(X0,X1))],[f7958]) ).
fof(f8061,plain,
! [X2,X3,X0,X1] :
( ~ p__d__instance(X1,c__Object)
| ~ p__d__instance(X0,c__Object)
| ~ p__d__instance(X2,c__Attribute)
| ~ p__d__instance(X2,c__BiologicalAttribute)
| ~ p__attribute(X1,X2)
| ~ p__d__instance(X3,c__Attribute)
| ~ p__d__instance(X3,c__ShapeAttribute)
| ~ p__attribute(X0,X3)
| X0 = X1 ),
inference(cnf_transformation,[],[f7498]) ).
fof(f8063,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X0,X1)
| p__d__instance(X0,X2)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7502]) ).
fof(f8065,plain,
! [X0,X1] :
( ~ p__attribute(X0,X1)
| p__d__instance(X0,c__Object) ),
inference(cnf_transformation,[],[f7504]) ).
fof(f8066,plain,
! [X0,X1] :
( ~ p__attribute(X0,X1)
| p__d__instance(X1,c__Attribute) ),
inference(cnf_transformation,[],[f7504]) ).
fof(f8076,plain,
p__d__subclass(c__Agent,c__Object),
inference(cnf_transformation,[],[f225]) ).
fof(f8077,plain,
p__d__instance(c__LineFormation,c__ShapeAttribute),
inference(cnf_transformation,[],[f4987]) ).
fof(f8087,plain,
p__d__subclass(c__DevelopmentalAttribute,c__BiologicalAttribute),
inference(cnf_transformation,[],[f2681]) ).
fof(f8093,plain,
! [X2,X0,X1] :
( ~ p__d__subclass(X1,X2)
| ~ p__d__subclass(X0,X1)
| p__d__subclass(X0,X2) ),
inference(cnf_transformation,[],[f7516]) ).
fof(f8144,plain,
p__d__subclass(c__Organism,c__Agent),
inference(cnf_transformation,[],[f2063]) ).
fof(f8147,plain,
! [X0] :
( ~ p__d__instance(X0,c__Convoy)
| p__attribute(X0,c__LineFormation) ),
inference(cnf_transformation,[],[f7534]) ).
fof(f8210,plain,
p__d__disjoint(c__Collection,c__SelfConnectedObject),
inference(cnf_transformation,[],[f177]) ).
fof(f8258,plain,
! [X0] :
( p__attribute(X0,sK34(X0))
| ~ p__d__instance(X0,c__Organism) ),
inference(cnf_transformation,[],[f7916]) ).
fof(f8259,plain,
! [X0] :
( p__d__instance(sK34(X0),c__DevelopmentalAttribute)
| ~ p__d__instance(X0,c__Organism) ),
inference(cnf_transformation,[],[f7916]) ).
fof(f8280,plain,
p__d__subclass(c__Organism,c__OrganicObject),
inference(cnf_transformation,[],[f2062]) ).
fof(f8282,plain,
p__d__subclass(c__OrganicObject,c__CorpuscularObject),
inference(cnf_transformation,[],[f2059]) ).
fof(f8410,plain,
p__d__subclass(c__Object,c__Physical),
inference(cnf_transformation,[],[f115]) ).
fof(f8503,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[],[f112]) ).
fof(f8506,plain,
! [X0] :
( p__d__instance(sK59(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[],[f7953]) ).
fof(f8523,plain,
p__d__subclass(c__CorpuscularObject,c__SelfConnectedObject),
inference(cnf_transformation,[],[f171]) ).
fof(f8546,plain,
! [X3,X0,X1] :
( ~ p__d__disjoint(X0,X1)
| ~ p__d__instance(X3,X1)
| ~ p__d__instance(X3,X0) ),
inference(cnf_transformation,[],[f7959]) ).
fof(f8574,plain,
p__d__subclass(c__Convoy,c__Collection),
inference(cnf_transformation,[],[f5390]) ).
fof(f8576,plain,
p__d__subclass(c__Collection,c__Object),
inference(cnf_transformation,[],[f176]) ).
fof(f9128,plain,
! [X2,X3,X0,X1] :
( ~ p__d__instance(X0,c__Object)
| ~ p__d__instance(X2,c__Attribute)
| ~ p__d__instance(X2,c__BiologicalAttribute)
| ~ p__attribute(X1,X2)
| ~ p__d__instance(X3,c__Attribute)
| ~ p__d__instance(X3,c__ShapeAttribute)
| ~ p__attribute(X0,X3)
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f8061,f8065]) ).
fof(f9203,plain,
! [X2,X3,X0,X1] :
( ~ p__d__instance(X2,c__Attribute)
| ~ p__d__instance(X2,c__BiologicalAttribute)
| ~ p__attribute(X1,X2)
| ~ p__d__instance(X3,c__Attribute)
| ~ p__d__instance(X3,c__ShapeAttribute)
| ~ p__attribute(X0,X3)
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f9128,f8065]) ).
fof(f9228,plain,
! [X2,X3,X0,X1] :
( ~ p__d__instance(X2,c__BiologicalAttribute)
| ~ p__attribute(X1,X2)
| ~ p__d__instance(X3,c__Attribute)
| ~ p__d__instance(X3,c__ShapeAttribute)
| ~ p__attribute(X0,X3)
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f9203,f8066]) ).
fof(f9230,plain,
! [X2,X3,X0,X1] :
( ~ p__attribute(X1,X2)
| ~ p__d__instance(X2,c__BiologicalAttribute)
| ~ p__d__instance(X3,c__ShapeAttribute)
| ~ p__attribute(X0,X3)
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f9228,f8066]) ).
fof(f9377,plain,
p__d__subclass(c__Organism,c__Object),
inference(unit_resulting_resolution,[],[f8093,f8144,f8076]) ).
fof(f9406,plain,
p__d__subclass(c__Organism,c__CorpuscularObject),
inference(unit_resulting_resolution,[],[f8093,f8280,f8282]) ).
fof(f9455,plain,
p__d__subclass(c__Organism,c__SelfConnectedObject),
inference(unit_resulting_resolution,[],[f8093,f8523,f9406]) ).
fof(f9491,plain,
p__d__subclass(c__Organism,c__Physical),
inference(unit_resulting_resolution,[],[f8093,f8410,f9377]) ).
fof(f9714,plain,
p__d__subclass(c__Object,c__Entity),
inference(unit_resulting_resolution,[],[f8093,f8410,f8503]) ).
fof(f9722,plain,
p__d__subclass(c__Organism,c__Entity),
inference(unit_resulting_resolution,[],[f8093,f9491,f8503]) ).
fof(f9865,plain,
p__d__subclass(c__Convoy,c__Object),
inference(unit_resulting_resolution,[],[f8093,f8574,f8576]) ).
fof(f11157,plain,
p__d__subclass(c__Convoy,c__Entity),
inference(unit_resulting_resolution,[],[f8093,f9714,f9865]) ).
fof(f16073,plain,
p__d__instance(sK59(c__Organism),c__Organism),
inference(unit_resulting_resolution,[],[f8506,f9722]) ).
fof(f16148,plain,
p__d__instance(sK59(c__Convoy),c__Convoy),
inference(unit_resulting_resolution,[],[f8506,f11157]) ).
fof(f16616,plain,
p__d__instance(sK34(sK59(c__Organism)),c__DevelopmentalAttribute),
inference(unit_resulting_resolution,[],[f8259,f16073]) ).
fof(f16617,plain,
p__attribute(sK59(c__Organism),sK34(sK59(c__Organism))),
inference(unit_resulting_resolution,[],[f8258,f16073]) ).
fof(f16621,plain,
p__d__instance(sK59(c__Organism),c__SelfConnectedObject),
inference(unit_resulting_resolution,[],[f8063,f9455,f16073]) ).
fof(f16631,definition,
sF169 = sK59(c__Organism),
introduced(definition,[new_symbols(definition,[sF169])],[function_definition]) ).
fof(f16632,plain,
sK59(c__Organism) = sF169,
inference(reorient_equations,[],[f16631]) ).
fof(f16644,plain,
p__d__instance(sK34(sF169),c__DevelopmentalAttribute),
inference(backward_demodulation,[],[f16616,f16632]) ).
fof(f16645,plain,
p__attribute(sF169,sK34(sF169)),
inference(backward_demodulation,[],[f16617,f16632]) ).
fof(f16648,plain,
p__d__instance(sF169,c__SelfConnectedObject),
inference(backward_demodulation,[],[f16621,f16632]) ).
fof(f22646,plain,
p__attribute(sK59(c__Convoy),c__LineFormation),
inference(unit_resulting_resolution,[],[f8147,f16148]) ).
fof(f22650,plain,
p__d__instance(sK59(c__Convoy),c__Collection),
inference(unit_resulting_resolution,[],[f8063,f8574,f16148]) ).
fof(f22656,definition,
sF225 = sK59(c__Convoy),
introduced(definition,[new_symbols(definition,[sF225])],[function_definition]) ).
fof(f22657,plain,
sK59(c__Convoy) = sF225,
inference(reorient_equations,[],[f22656]) ).
fof(f22666,plain,
p__d__instance(sF225,c__Collection),
inference(backward_demodulation,[],[f22650,f22657]) ).
fof(f22669,plain,
p__attribute(sF225,c__LineFormation),
inference(backward_demodulation,[],[f22646,f22657]) ).
fof(f22687,plain,
~ p__d__instance(sF225,c__SelfConnectedObject),
inference(unit_resulting_resolution,[],[f8546,f8210,f22666]) ).
fof(f23143,plain,
p__d__instance(sK34(sF169),c__BiologicalAttribute),
inference(unit_resulting_resolution,[],[f8063,f8087,f16644]) ).
fof(f23149,definition,
sF236 = sK34(sF169),
introduced(definition,[new_symbols(definition,[sF236])],[function_definition]) ).
fof(f23150,plain,
sK34(sF169) = sF236,
inference(reorient_equations,[],[f23149]) ).
fof(f23153,plain,
p__d__instance(sF236,c__BiologicalAttribute),
inference(backward_demodulation,[],[f23143,f23150]) ).
fof(f23158,plain,
p__attribute(sF169,sF236),
inference(backward_demodulation,[],[f16645,f23150]) ).
fof(f23173,plain,
sF169 = sF225,
inference(unit_resulting_resolution,[],[f9230,f22669,f8077,f23158,f23153]) ).
fof(f23193,plain,
~ p__d__instance(sF169,c__SelfConnectedObject),
inference(backward_demodulation,[],[f22687,f23173]) ).
fof(f23197,plain,
$false,
inference(forward_subsumption_resolution,[],[f23193,f16648]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR170+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.26 % Computer : n005.cluster.edu
% 0.13/0.26 % Model : x86_64 x86_64
% 0.13/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.26 % Memory : 8046.5625MB
% 0.13/0.26 % OS : Linux 6.8.0-71-generic
% 0.13/0.27 % CPULimit : 300
% 0.13/0.27 % WCLimit : 300
% 0.13/0.27 % DateTime : Mon Sep 28 23:38:47 UTC 2026
% 0.13/0.27 % CPUTime :
% 0.13/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.27/0.32 Running first-order theorem proving
% 0.27/0.32 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.24/3.03 % (1290272)Detected formulas, will run a generic FOF schedule.
% 12.24/3.03 % (1290292)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1194501619:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 12.24/3.03 % (1290295)dis-21_1_sil=8000:lcm=predicate:random_seed=542887973:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 12.24/3.03 % (1290292)Refutation not found, incomplete strategy
% 12.24/3.03 % (1290292)------------------------------
% 12.24/3.03 % (1290292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.24/3.03 % (1290292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.24/3.03 % (1290292)CaDiCaL version: 2.1.3
% 12.24/3.03 % (1290292)Termination reason: Refutation not found, incomplete strategy
% 12.24/3.03 % (1290292)Time elapsed: 0.014 s
% 12.24/3.03 % (1290292)Peak memory usage: 93 MB
% 12.24/3.03 % (1290292)Instructions burned: 24 (million)
% 12.24/3.03 % (1290290)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=1769417879:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 12.24/3.03 % (1290291)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=3830870750:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 12.24/3.03 % (1290289)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=1467963470:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 12.24/3.03 % (1290293)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1969820547:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 12.24/3.03 % (1290294)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=316085872:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 12.24/3.03 % (1290295)Instruction limit reached!
% 12.24/3.03 % (1290295)------------------------------
% 12.24/3.03 % (1290295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.24/3.03 % (1290295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.24/3.03 % (1290295)CaDiCaL version: 2.1.3
% 12.24/3.03 % (1290295)Termination reason: Instruction limit
% 12.24/3.03 % (1290295)Termination phase: Saturation
% 12.24/3.03 % (1290295)Time elapsed: 0.084 s
% 12.24/3.03 % (1290295)Peak memory usage: 95 MB
% 12.24/3.03 % (1290295)Instructions burned: 130 (million)
% 12.24/3.03 % (1290293)Instruction limit reached!
% 12.24/3.03 % (1290293)------------------------------
% 12.24/3.03 % (1290293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.24/3.03 % (1290293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.24/3.03 % (1290293)CaDiCaL version: 2.1.3
% 12.24/3.03 % (1290293)Termination reason: Instruction limit
% 12.24/3.03 % (1290293)Termination phase: Saturation
% 12.24/3.03 % (1290293)Time elapsed: 0.111 s
% 12.24/3.03 % (1290293)Peak memory usage: 93 MB
% 12.24/3.03 % (1290293)Instructions burned: 119 (million)
% 12.24/3.03 % (1290294)Instruction limit reached!
% 12.24/3.03 % (1290294)------------------------------
% 12.24/3.03 % (1290294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.24/3.03 % (1290294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.24/3.03 % (1290294)CaDiCaL version: 2.1.3
% 12.24/3.03 % (1290294)Termination reason: Instruction limit
% 12.24/3.03 % (1290294)Termination phase: Preprocessing 3
% 12.24/3.03 % (1290294)Time elapsed: 0.145 s
% 12.24/3.03 % (1290294)Peak memory usage: 94 MB
% 12.24/3.03 % (1290294)Instructions burned: 139 (million)
% 12.24/3.03 % (1290307)lrs+10_1_sil=8000:sp=occurrence:random_seed=1251815346:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 12.24/3.03 % (1290292)------------------------------
% 12.24/3.03 % (1290292)------------------------------
% 12.24/3.03 % (1290307)Refutation not found, incomplete strategy
% 12.24/3.03 % (1290307)------------------------------
% 12.24/3.03 % (1290307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.24/3.03 % (1290307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.24/3.03 % (1290307)CaDiCaL version: 2.1.3
% 12.24/3.03 % (1290307)Termination reason: Refutation not found, incomplete strategy
% 12.24/3.03 % (1290307)Time elapsed: 0.024 s
% 21.43/4.06 % (1290307)Peak memory usage: 94 MB
% 21.43/4.06 % (1290307)Instructions burned: 22 (million)
% 21.43/4.06 % (1290308)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3905330072:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/157Mi)
% 21.43/4.06 % (1290310)lrs+1011_1_sil=32000:sp=occurrence:random_seed=442919155:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 21.43/4.06 % (1290308)Refutation not found, incomplete strategy
% 21.43/4.06 % (1290308)------------------------------
% 21.43/4.06 % (1290308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.43/4.06 % (1290308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.43/4.06 % (1290308)CaDiCaL version: 2.1.3
% 21.43/4.06 % (1290308)Termination reason: Refutation not found, incomplete strategy
% 21.43/4.06 % (1290308)Time elapsed: 0.056 s
% 21.43/4.06 % (1290308)Peak memory usage: 94 MB
% 21.43/4.06 % (1290308)Instructions burned: 60 (million)
% 21.43/4.06 % (1290311)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=1176891431:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 21.43/4.06 % (1290310)Refutation not found, incomplete strategy
% 21.43/4.06 % (1290310)------------------------------
% 21.43/4.06 % (1290310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.43/4.06 % (1290310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.43/4.06 % (1290310)CaDiCaL version: 2.1.3
% 21.43/4.06 % (1290310)Termination reason: Refutation not found, incomplete strategy
% 21.43/4.06 % (1290310)Time elapsed: 0.027 s
% 21.43/4.06 % (1290310)Peak memory usage: 94 MB
% 21.43/4.06 % (1290310)Instructions burned: 21 (million)
% 21.43/4.06 % (1290307)------------------------------
% 21.43/4.06 % (1290307)------------------------------
% 21.43/4.06 % (1290316)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1693121618:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 21.43/4.06 % (1290311)Instruction limit reached!
% 21.43/4.06 % (1290311)------------------------------
% 21.43/4.06 % (1290311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.43/4.06 % (1290311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.43/4.06 % (1290311)CaDiCaL version: 2.1.3
% 21.43/4.06 % (1290311)Termination reason: Instruction limit
% 21.43/4.06 % (1290311)Termination phase: Saturation
% 21.43/4.06 % (1290311)Time elapsed: 0.230 s
% 21.43/4.06 % (1290311)Peak memory usage: 98 MB
% 21.43/4.06 % (1290311)Instructions burned: 249 (million)
% 21.43/4.06 % (1290316)Instruction limit reached!
% 21.43/4.06 % (1290316)------------------------------
% 21.43/4.06 % (1290316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.43/4.06 % (1290316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.43/4.06 % (1290316)CaDiCaL version: 2.1.3
% 21.43/4.06 % (1290316)Termination reason: Instruction limit
% 21.43/4.06 % (1290316)Termination phase: Saturation
% 21.43/4.06 % (1290316)Time elapsed: 0.137 s
% 21.43/4.06 % (1290316)Peak memory usage: 95 MB
% 21.43/4.06 % (1290316)Instructions burned: 295 (million)
% 21.43/4.06 % (1290308)------------------------------
% 21.43/4.06 % (1290308)------------------------------
% 21.43/4.06 % (1290310)------------------------------
% 21.43/4.06 % (1290310)------------------------------
% 21.43/4.06 % (1290321)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2650952441:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 21.43/4.06 % (1290323)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=811792048:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 21.43/4.06 % (1290322)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1921929177:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 21.43/4.06 % (1290291)Refutation not found, incomplete strategy
% 21.43/4.06 % (1290291)------------------------------
% 21.43/4.06 % (1290291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.43/4.06 % (1290291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.43/4.06 % (1290291)CaDiCaL version: 2.1.3
% 21.43/4.06 % (1290291)Termination reason: Refutation not found, incomplete strategy
% 21.43/4.06 % (1290291)Time elapsed: 0.991 s
% 21.43/4.06 % (1290291)Peak memory usage: 144 MB
% 21.43/4.06 % (1290291)Instructions burned: 953 (million)
% 21.43/4.06 % (1290322)Refutation not found, incomplete strategy
% 29.22/5.19 % (1290322)------------------------------
% 29.22/5.19 % (1290322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.19 % (1290322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.19 % (1290322)CaDiCaL version: 2.1.3
% 29.22/5.19 % (1290322)Termination reason: Refutation not found, incomplete strategy
% 29.22/5.19 % (1290322)Time elapsed: 0.028 s
% 29.22/5.19 % (1290322)Peak memory usage: 94 MB
% 29.22/5.19 % (1290322)Instructions burned: 24 (million)
% 29.22/5.19 % (1290323)Instruction limit reached!
% 29.22/5.19 % (1290323)------------------------------
% 29.22/5.19 % (1290323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.19 % (1290323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.19 % (1290323)CaDiCaL version: 2.1.3
% 29.22/5.19 % (1290323)Termination reason: Instruction limit
% 29.22/5.19 % (1290323)Termination phase: Property scanning
% 29.22/5.19 % (1290323)Time elapsed: 0.075 s
% 29.22/5.19 % (1290323)Peak memory usage: 96 MB
% 29.22/5.19 % (1290323)Instructions burned: 127 (million)
% 29.22/5.19 % (1290325)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=512570337:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 29.22/5.19 % (1290325)Instruction limit reached!
% 29.22/5.19 % (1290325)------------------------------
% 29.22/5.19 % (1290325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.19 % (1290325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.19 % (1290325)CaDiCaL version: 2.1.3
% 29.22/5.19 % (1290325)Termination reason: Instruction limit
% 29.22/5.19 % (1290325)Termination phase: Property scanning
% 29.22/5.19 % (1290325)Time elapsed: 0.107 s
% 29.22/5.19 % (1290325)Peak memory usage: 91 MB
% 29.22/5.19 % (1290325)Instructions burned: 115 (million)
% 29.22/5.19 % (1290328)lrs+10_1_sil=8000:sp=occurrence:random_seed=515462072:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 29.22/5.19 % (1290291)------------------------------
% 29.22/5.19 % (1290291)------------------------------
% 29.22/5.19 % (1290322)------------------------------
% 29.22/5.19 % (1290322)------------------------------
% 29.22/5.19 % (1290330)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3160328057:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 29.22/5.19 % (1290330)Refutation not found, incomplete strategy
% 29.22/5.19 % (1290330)------------------------------
% 29.22/5.19 % (1290330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.19 % (1290330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.19 % (1290330)CaDiCaL version: 2.1.3
% 29.22/5.19 % (1290330)Termination reason: Refutation not found, incomplete strategy
% 29.22/5.19 % (1290330)Time elapsed: 0.024 s
% 29.22/5.19 % (1290330)Peak memory usage: 93 MB
% 29.22/5.19 % (1290330)Instructions burned: 19 (million)
% 29.22/5.19 % (1290290)Refutation not found, incomplete strategy
% 29.22/5.19 % (1290290)------------------------------
% 29.22/5.19 % (1290290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.19 % (1290290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.19 % (1290290)CaDiCaL version: 2.1.3
% 29.22/5.19 % (1290290)Termination reason: Refutation not found, incomplete strategy
% 29.22/5.19 % (1290290)Time elapsed: 1.482 s
% 29.22/5.19 % (1290290)Peak memory usage: 148 MB
% 29.22/5.19 % (1290290)Instructions burned: 1336 (million)
% 29.22/5.19 % (1290334)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3186266497:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2981 on theBenchmark for (2981ds/134Mi)
% 29.22/5.19 % (1290334)Refutation not found, incomplete strategy
% 29.22/5.19 % (1290334)------------------------------
% 29.22/5.19 % (1290334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.19 % (1290334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.19 % (1290334)CaDiCaL version: 2.1.3
% 29.22/5.19 % (1290334)Termination reason: Refutation not found, incomplete strategy
% 29.22/5.19 % (1290334)Time elapsed: 0.021 s
% 29.22/5.19 % (1290334)Peak memory usage: 94 MB
% 29.22/5.19 % (1290334)Instructions burned: 25 (million)
% 29.22/5.19 % (1290333)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1403832177:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi)
% 29.22/5.19 % (1290328)Instruction limit reached!
% 29.22/5.19 % (1290328)------------------------------
% 49.79/8.09 % (1290328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.79/8.09 % (1290328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.79/8.09 % (1290328)CaDiCaL version: 2.1.3
% 49.79/8.09 % (1290328)Termination reason: Instruction limit
% 49.79/8.09 % (1290328)Termination phase: Saturation
% 49.79/8.09 % (1290328)Time elapsed: 0.491 s
% 49.79/8.09 % (1290328)Peak memory usage: 111 MB
% 49.79/8.09 % (1290328)Instructions burned: 908 (million)
% 49.79/8.09 % (1290330)------------------------------
% 49.79/8.09 % (1290330)------------------------------
% 49.79/8.09 % (1290338)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2273102260:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 49.79/8.09 % (1290290)------------------------------
% 49.79/8.09 % (1290290)------------------------------
% 49.79/8.09 % (1290334)------------------------------
% 49.79/8.09 % (1290334)------------------------------
% 49.79/8.09 % (1290342)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=942253463:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 49.79/8.09 % (1290344)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=4015041268:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/125Mi)
% 49.79/8.09 % (1290338)Instruction limit reached!
% 49.79/8.09 % (1290338)------------------------------
% 49.79/8.09 % (1290338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.79/8.09 % (1290338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.79/8.09 % (1290338)CaDiCaL version: 2.1.3
% 49.79/8.09 % (1290338)Termination reason: Instruction limit
% 49.79/8.09 % (1290338)Termination phase: Saturation
% 49.79/8.09 % (1290338)Time elapsed: 0.281 s
% 49.79/8.09 % (1290338)Peak memory usage: 100 MB
% 49.79/8.09 % (1290338)Instructions burned: 592 (million)
% 49.79/8.09 % (1290345)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4004242154:i=134:gtgl=5:slsql=off:gtg=exists_sym_2975 on theBenchmark for (2975ds/134Mi)
% 49.79/8.09 % (1290344)Refutation not found, incomplete strategy
% 49.79/8.09 % (1290344)------------------------------
% 49.79/8.09 % (1290344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.79/8.09 % (1290344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.79/8.09 % (1290344)CaDiCaL version: 2.1.3
% 49.79/8.09 % (1290344)Termination reason: Refutation not found, incomplete strategy
% 49.79/8.09 % (1290344)Time elapsed: 0.078 s
% 49.79/8.09 % (1290344)Peak memory usage: 94 MB
% 49.79/8.09 % (1290344)Instructions burned: 79 (million)
% 49.79/8.09 % (1290345)Instruction limit reached!
% 49.79/8.09 % (1290345)------------------------------
% 49.79/8.09 % (1290345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.79/8.09 % (1290345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.79/8.09 % (1290345)CaDiCaL version: 2.1.3
% 49.79/8.09 % (1290345)Termination reason: Instruction limit
% 49.79/8.09 % (1290345)Termination phase: Preprocessing 2
% 49.79/8.09 % (1290345)Time elapsed: 0.127 s
% 49.79/8.09 % (1290345)Peak memory usage: 92 MB
% 49.79/8.09 % (1290345)Instructions burned: 134 (million)
% 49.79/8.09 % (1290348)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4166471542:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/141Mi)
% 49.79/8.09 % (1290348)Refutation not found, incomplete strategy
% 49.79/8.09 % (1290348)------------------------------
% 49.79/8.09 % (1290348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.79/8.09 % (1290348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.79/8.09 % (1290348)CaDiCaL version: 2.1.3
% 49.79/8.09 % (1290348)Termination reason: Refutation not found, incomplete strategy
% 49.79/8.09 % (1290348)Time elapsed: 0.017 s
% 49.79/8.09 % (1290348)Peak memory usage: 93 MB
% 49.79/8.09 % (1290348)Instructions burned: 24 (million)
% 49.79/8.09 % (1290351)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3256375015:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2972 on theBenchmark for (2972ds/431Mi)
% 49.79/8.09 % (1290348)------------------------------
% 49.79/8.09 % (1290348)------------------------------
% 49.79/8.09 % (1290344)------------------------------
% 49.79/8.09 % (1290344)------------------------------
% 49.79/8.09 % (1290353)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=1242997190:i=6060:aac=none:ins=25_2969 on theBenchmark for (2969ds/6060Mi)
% 65.17/10.25 % (1290355)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=3493217356:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2969 on theBenchmark for (2969ds/150Mi)
% 65.17/10.25 % (1290351)Instruction limit reached!
% 65.17/10.25 % (1290351)------------------------------
% 65.17/10.25 % (1290351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.17/10.25 % (1290351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.17/10.25 % (1290351)CaDiCaL version: 2.1.3
% 65.17/10.25 % (1290351)Termination reason: Instruction limit
% 65.17/10.25 % (1290351)Termination phase: Saturation
% 65.17/10.25 % (1290351)Time elapsed: 0.380 s
% 65.17/10.25 % (1290351)Peak memory usage: 99 MB
% 65.17/10.25 % (1290351)Instructions burned: 432 (million)
% 65.17/10.25 % (1290355)Instruction limit reached!
% 65.17/10.25 % (1290355)------------------------------
% 65.17/10.25 % (1290355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.17/10.25 % (1290355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.17/10.25 % (1290355)CaDiCaL version: 2.1.3
% 65.17/10.25 % (1290355)Termination reason: Instruction limit
% 65.17/10.25 % (1290355)Termination phase: Property scanning
% 65.17/10.25 % (1290355)Time elapsed: 0.158 s
% 65.17/10.25 % (1290355)Peak memory usage: 96 MB
% 65.17/10.25 % (1290355)Instructions burned: 150 (million)
% 65.17/10.25 % (1290321)Instruction limit reached!
% 65.17/10.25 % (1290321)------------------------------
% 65.17/10.25 % (1290321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.17/10.25 % (1290321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.17/10.25 % (1290321)CaDiCaL version: 2.1.3
% 65.17/10.25 % (1290321)Termination reason: Instruction limit
% 65.17/10.25 % (1290321)Termination phase: Saturation
% 65.17/10.25 % (1290321)Time elapsed: 2.294 s
% 65.17/10.25 % (1290321)Peak memory usage: 214 MB
% 65.17/10.25 % (1290321)Instructions burned: 2350 (million)
% 65.17/10.25 % (1290359)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2607101212:i=14155:bd=all_2966 on theBenchmark for (2966ds/14155Mi)
% 65.17/10.25 % (1290360)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3898409219:i=667:av=off:fsr=off_2965 on theBenchmark for (2965ds/667Mi)
% 65.17/10.25 % (1290362)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=1852784565:s2a=on:i=185:s2at=1.8:fdi=4_2964 on theBenchmark for (2964ds/185Mi)
% 65.17/10.25 % (1290362)Instruction limit reached!
% 65.17/10.25 % (1290362)------------------------------
% 65.17/10.25 % (1290362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.17/10.25 % (1290362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.17/10.25 % (1290362)CaDiCaL version: 2.1.3
% 65.17/10.25 % (1290362)Termination reason: Instruction limit
% 65.17/10.25 % (1290362)Termination phase: Property scanning
% 65.17/10.25 % (1290362)Time elapsed: 0.193 s
% 65.17/10.25 % (1290362)Peak memory usage: 97 MB
% 65.17/10.25 % (1290362)Instructions burned: 186 (million)
% 65.17/10.25 % (1290365)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3582118837:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2960 on theBenchmark for (2960ds/193Mi)
% 65.17/10.25 % (1290365)Refutation not found, incomplete strategy
% 65.17/10.25 % (1290365)------------------------------
% 65.17/10.25 % (1290365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.17/10.25 % (1290365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.17/10.25 % (1290365)CaDiCaL version: 2.1.3
% 65.17/10.25 % (1290365)Termination reason: Refutation not found, incomplete strategy
% 65.17/10.25 % (1290365)Time elapsed: 0.062 s
% 65.17/10.25 % (1290365)Peak memory usage: 94 MB
% 65.17/10.25 % (1290365)Instructions burned: 51 (million)
% 65.17/10.25 % (1290360)Instruction limit reached!
% 65.17/10.25 % (1290360)------------------------------
% 65.17/10.25 % (1290360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.17/10.25 % (1290360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.80/17.91 % (1290360)CaDiCaL version: 2.1.3
% 119.80/17.91 % (1290360)Termination reason: Instruction limit
% 119.80/17.91 % (1290360)Termination phase: Saturation
% 119.80/17.91 % (1290360)Time elapsed: 0.609 s
% 119.80/17.91 % (1290360)Peak memory usage: 104 MB
% 119.80/17.91 % (1290360)Instructions burned: 667 (million)
% 119.80/17.91 % (1290369)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1970763053:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2956 on theBenchmark for (2956ds/4850Mi)
% 119.80/17.91 % (1290365)------------------------------
% 119.80/17.91 % (1290365)------------------------------
% 119.80/17.91 % (1290369)Refutation not found, incomplete strategy
% 119.80/17.91 % (1290369)------------------------------
% 119.80/17.91 % (1290369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.80/17.91 % (1290369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.80/17.91 % (1290369)CaDiCaL version: 2.1.3
% 119.80/17.91 % (1290369)Termination reason: Refutation not found, incomplete strategy
% 119.80/17.91 % (1290369)Time elapsed: 0.214 s
% 119.80/17.91 % (1290369)Peak memory usage: 98 MB
% 119.80/17.91 % (1290369)Instructions burned: 208 (million)
% 119.80/17.91 % (1290371)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1032595933:i=12111:sd=1:ss=included_2953 on theBenchmark for (2953ds/12111Mi)
% 119.80/17.91 % (1290369)------------------------------
% 119.80/17.91 % (1290369)------------------------------
% 119.80/17.91 % (1290373)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1125896893:i=319:kws=precedence:fsr=off_2948 on theBenchmark for (2948ds/319Mi)
% 119.80/17.91 % (1290373)Instruction limit reached!
% 119.80/17.91 % (1290373)------------------------------
% 119.80/17.91 % (1290373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.80/17.91 % (1290373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.80/17.91 % (1290373)CaDiCaL version: 2.1.3
% 119.80/17.91 % (1290373)Termination reason: Instruction limit
% 119.80/17.91 % (1290373)Termination phase: Saturation
% 119.80/17.91 % (1290373)Time elapsed: 0.282 s
% 119.80/17.91 % (1290373)Peak memory usage: 100 MB
% 119.80/17.91 % (1290373)Instructions burned: 319 (million)
% 119.80/17.91 % (1290371)Refutation not found, incomplete strategy
% 119.80/17.91 % (1290371)------------------------------
% 119.80/17.91 % (1290371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.80/17.91 % (1290371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.80/17.91 % (1290371)CaDiCaL version: 2.1.3
% 119.80/17.91 % (1290371)Termination reason: Refutation not found, incomplete strategy
% 119.80/17.91 % (1290371)Time elapsed: 1.066 s
% 119.80/17.91 % (1290371)Peak memory usage: 148 MB
% 119.80/17.91 % (1290371)Instructions burned: 1024 (million)
% 119.80/17.91 % (1290377)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1842793815:i=2064:ep=RST_2943 on theBenchmark for (2943ds/2064Mi)
% 119.80/17.91 % (1290371)------------------------------
% 119.80/17.91 % (1290371)------------------------------
% 119.80/17.91 % (1290353)Instruction limit reached!
% 119.80/17.91 % (1290353)------------------------------
% 119.80/17.91 % (1290353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.80/17.91 % (1290353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.80/17.91 % (1290353)CaDiCaL version: 2.1.3
% 119.80/17.91 % (1290353)Termination reason: Instruction limit
% 119.80/17.91 % (1290353)Termination phase: Saturation
% 119.80/17.91 % (1290353)Time elapsed: 3.280 s
% 119.80/17.91 % (1290353)Peak memory usage: 238 MB
% 119.80/17.91 % (1290353)Instructions burned: 6061 (million)
% 119.80/17.91 % (1290379)dis-1011_128_sil=32000:random_seed=455943586:i=3706:ep=RST:av=off_2937 on theBenchmark for (2937ds/3706Mi)
% 119.80/17.91 % (1290381)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4162959670:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2935 on theBenchmark for (2935ds/757Mi)
% 119.80/17.91 % (1290381)Instruction limit reached!
% 119.80/17.91 % (1290381)------------------------------
% 119.80/17.91 % (1290381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.80/17.91 % (1290381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.80/17.91 % (1290381)CaDiCaL version: 2.1.3
% 119.80/17.91 % (1290381)Termination reason: Instruction limit
% 119.80/17.91 % (1290381)Termination phase: Saturation
% 119.80/17.91 % (1290381)Time elapsed: 0.423 s
% 119.80/17.91 % (1290381)Peak memory usage: 99 MB
% 119.80/17.91 % (1290381)Instructions burned: 757 (million)
% 119.80/17.91 % (1290383)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=28632254:i=13913:ss=axioms:sgt=8_2929 on theBenchmark for (2929ds/13913Mi)
% 136.28/20.27 % (1290377)Instruction limit reached!
% 136.28/20.27 % (1290377)------------------------------
% 136.28/20.27 % (1290377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.28/20.27 % (1290377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.28/20.27 % (1290377)CaDiCaL version: 2.1.3
% 136.28/20.27 % (1290377)Termination reason: Instruction limit
% 136.28/20.27 % (1290377)Termination phase: Saturation
% 136.28/20.27 % (1290377)Time elapsed: 1.734 s
% 136.28/20.27 % (1290377)Peak memory usage: 118 MB
% 136.28/20.27 % (1290377)Instructions burned: 2065 (million)
% 136.28/20.27 % (1290333)Instruction limit reached!
% 136.28/20.27 % (1290333)------------------------------
% 136.28/20.27 % (1290333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.28/20.27 % (1290333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.28/20.27 % (1290333)CaDiCaL version: 2.1.3
% 136.28/20.27 % (1290333)Termination reason: Instruction limit
% 136.28/20.27 % (1290333)Termination phase: Saturation
% 136.28/20.27 % (1290333)Time elapsed: 5.664 s
% 136.28/20.27 % (1290333)Peak memory usage: 216 MB
% 136.28/20.27 % (1290333)Instructions burned: 5202 (million)
% 136.28/20.27 % (1290385)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=560145146:i=9925:aac=none_2923 on theBenchmark for (2923ds/9925Mi)
% 136.28/20.27 % (1290383)Refutation not found, incomplete strategy
% 136.28/20.27 % (1290383)------------------------------
% 136.28/20.27 % (1290383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.28/20.27 % (1290383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.28/20.27 % (1290383)CaDiCaL version: 2.1.3
% 136.28/20.27 % (1290383)Termination reason: Refutation not found, incomplete strategy
% 136.28/20.27 % (1290383)Time elapsed: 0.648 s
% 136.28/20.27 % (1290383)Peak memory usage: 137 MB
% 136.28/20.27 % (1290383)Instructions burned: 1072 (million)
% 136.28/20.27 % (1290386)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2850323893:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2922 on theBenchmark for (2922ds/2479Mi)
% 136.28/20.27 % (1290386)Refutation not found, incomplete strategy
% 136.28/20.27 % (1290386)------------------------------
% 136.28/20.27 % (1290386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.28/20.27 % (1290386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.28/20.27 % (1290386)CaDiCaL version: 2.1.3
% 136.28/20.27 % (1290386)Termination reason: Refutation not found, incomplete strategy
% 136.28/20.27 % (1290386)Time elapsed: 0.046 s
% 136.28/20.27 % (1290386)Peak memory usage: 93 MB
% 136.28/20.27 % (1290386)Instructions burned: 42 (million)
% 136.28/20.27 % (1290383)------------------------------
% 136.28/20.27 % (1290383)------------------------------
% 136.28/20.27 % (1290391)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=971600554:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2918 on theBenchmark for (2918ds/440Mi)
% 136.28/20.27 % (1290386)------------------------------
% 136.28/20.27 % (1290386)------------------------------
% 136.28/20.27 % (1290391)Instruction limit reached!
% 136.28/20.27 % (1290391)------------------------------
% 136.28/20.27 % (1290391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.28/20.27 % (1290391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.28/20.27 % (1290391)CaDiCaL version: 2.1.3
% 136.28/20.27 % (1290391)Termination reason: Instruction limit
% 136.28/20.27 % (1290391)Termination phase: Saturation
% 136.28/20.27 % (1290391)Time elapsed: 0.219 s
% 136.28/20.27 % (1290391)Peak memory usage: 102 MB
% 136.28/20.27 % (1290391)Instructions burned: 440 (million)
% 136.28/20.27 % (1290396)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1784145534:cts=off:i=3034:av=off:er=known:fsd=on_2915 on theBenchmark for (2915ds/3034Mi)
% 136.28/20.27 % (1290395)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2888361091:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2915 on theBenchmark for (2915ds/11145Mi)
% 136.28/20.27 % (1290379)Instruction limit reached!
% 136.28/20.27 % (1290379)------------------------------
% 136.28/20.27 % (1290379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.28/20.27 % (1290379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290379)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290379)Termination reason: Instruction limit
% 151.21/22.39 % (1290379)Termination phase: Saturation
% 151.21/22.39 % (1290379)Time elapsed: 2.891 s
% 151.21/22.39 % (1290379)Peak memory usage: 102 MB
% 151.21/22.39 % (1290379)Instructions burned: 3707 (million)
% 151.21/22.39 % (1290399)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1100861919:st=2:s2a=on:i=524:s2at=2:ss=axioms_2906 on theBenchmark for (2906ds/524Mi)
% 151.21/22.39 % (1290399)Instruction limit reached!
% 151.21/22.39 % (1290399)------------------------------
% 151.21/22.39 % (1290399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290399)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290399)Termination reason: Instruction limit
% 151.21/22.39 % (1290399)Termination phase: Saturation
% 151.21/22.39 % (1290399)Time elapsed: 0.483 s
% 151.21/22.39 % (1290399)Peak memory usage: 100 MB
% 151.21/22.39 % (1290399)Instructions burned: 524 (million)
% 151.21/22.39 % (1290396)Instruction limit reached!
% 151.21/22.39 % (1290396)------------------------------
% 151.21/22.39 % (1290396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290396)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290396)Termination reason: Instruction limit
% 151.21/22.39 % (1290396)Termination phase: Saturation
% 151.21/22.39 % (1290396)Time elapsed: 1.585 s
% 151.21/22.39 % (1290396)Peak memory usage: 204 MB
% 151.21/22.39 % (1290396)Instructions burned: 3035 (million)
% 151.21/22.39 % (1290401)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3988068770:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2898 on theBenchmark for (2898ds/1016Mi)
% 151.21/22.39 % (1290401)Refutation not found, incomplete strategy
% 151.21/22.39 % (1290401)------------------------------
% 151.21/22.39 % (1290401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290401)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290401)Termination reason: Refutation not found, incomplete strategy
% 151.21/22.39 % (1290401)Time elapsed: 0.027 s
% 151.21/22.39 % (1290401)Peak memory usage: 94 MB
% 151.21/22.39 % (1290401)Instructions burned: 24 (million)
% 151.21/22.39 % (1290402)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=48547567:i=14123:bd=preordered:ins=4_2897 on theBenchmark for (2897ds/14123Mi)
% 151.21/22.39 % (1290401)------------------------------
% 151.21/22.39 % (1290401)------------------------------
% 151.21/22.39 % (1290407)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3119603646:i=5781:kws=precedence:bd=all:rawr=on_2892 on theBenchmark for (2892ds/5781Mi)
% 151.21/22.39 % (1290407)Instruction limit reached!
% 151.21/22.39 % (1290407)------------------------------
% 151.21/22.39 % (1290407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290407)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290407)Termination reason: Instruction limit
% 151.21/22.39 % (1290407)Termination phase: Saturation
% 151.21/22.39 % (1290407)Time elapsed: 4.455 s
% 151.21/22.39 % (1290407)Peak memory usage: 121 MB
% 151.21/22.39 % (1290407)Instructions burned: 5782 (million)
% 151.21/22.39 % (1290413)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=1343332719:i=2448:gtgl=5:bd=preordered:gtg=all_2845 on theBenchmark for (2845ds/2448Mi)
% 151.21/22.39 % (1290342)Instruction limit reached!
% 151.21/22.39 % (1290342)------------------------------
% 151.21/22.39 % (1290342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290342)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290342)Termination reason: Instruction limit
% 151.21/22.39 % (1290342)Termination phase: Saturation
% 151.21/22.39 % (1290342)Time elapsed: 14.318 s
% 151.21/22.39 % (1290342)Peak memory usage: 243 MB
% 151.21/22.39 % (1290342)Instructions burned: 13194 (million)
% 151.21/22.39 % (1290417)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3702501566:i=3223:kws=precedence:fgj=on:av=off_2831 on theBenchmark for (2831ds/3223Mi)
% 151.21/22.39 % (1290385)Instruction limit reached!
% 151.21/22.39 % (1290385)------------------------------
% 151.21/22.39 % (1290385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290385)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290385)Termination reason: Instruction limit
% 151.21/22.39 % (1290385)Termination phase: Saturation
% 151.21/22.39 % (1290385)Time elapsed: 9.331 s
% 151.21/22.39 % (1290385)Peak memory usage: 288 MB
% 151.21/22.39 % (1290385)Instructions burned: 9926 (million)
% 151.21/22.39 % (1290419)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3912016122:st=5.6:i=2033:sd=3:ss=axioms_2827 on theBenchmark for (2827ds/2033Mi)
% 151.21/22.39 % (1290413)Instruction limit reached!
% 151.21/22.39 % (1290413)------------------------------
% 151.21/22.39 % (1290413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290413)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290413)Termination reason: Instruction limit
% 151.21/22.39 % (1290413)Termination phase: Saturation
% 151.21/22.39 % (1290413)Time elapsed: 2.174 s
% 151.21/22.39 % (1290413)Peak memory usage: 208 MB
% 151.21/22.39 % (1290413)Instructions burned: 2448 (million)
% 151.21/22.39 % (1290402)Instruction limit reached!
% 151.21/22.39 % (1290402)------------------------------
% 151.21/22.39 % (1290402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290402)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290402)Termination reason: Instruction limit
% 151.21/22.39 % (1290402)Termination phase: Saturation
% 151.21/22.39 % (1290402)Time elapsed: 7.481 s
% 151.21/22.39 % (1290402)Peak memory usage: 243 MB
% 151.21/22.39 % (1290402)Instructions burned: 14124 (million)
% 151.21/22.39 % (1290424)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=816643345:i=21611:sd=3:ss=axioms_2820 on theBenchmark for (2820ds/21611Mi)
% 151.21/22.39 % (1290423)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=175847235:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2821 on theBenchmark for (2821ds/2055Mi)
% 151.21/22.39 % (1290359)Instruction limit reached!
% 151.21/22.39 % (1290359)------------------------------
% 151.21/22.39 % (1290359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290359)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290359)Termination reason: Instruction limit
% 151.21/22.39 % (1290359)Termination phase: Saturation
% 151.21/22.39 % (1290359)Time elapsed: 14.718 s
% 151.21/22.39 % (1290359)Peak memory usage: 253 MB
% 151.21/22.39 % (1290359)Instructions burned: 14155 (million)
% 151.21/22.39 % (1290427)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=4214927911:i=4835:sd=13:ss=axioms:sgt=23_2816 on theBenchmark for (2816ds/4835Mi)
% 151.21/22.39 % (1290424)Refutation not found, incomplete strategy
% 151.21/22.39 % (1290424)------------------------------
% 151.21/22.39 % (1290424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290424)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290424)Termination reason: Refutation not found, incomplete strategy
% 151.21/22.39 % (1290424)Time elapsed: 0.637 s
% 151.21/22.39 % (1290424)Peak memory usage: 145 MB
% 151.21/22.39 % (1290424)Instructions burned: 1052 (million)
% 151.21/22.39 % (1290424)------------------------------
% 151.21/22.39 % (1290424)------------------------------
% 151.21/22.39 % (1290429)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=1470227836:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2810 on theBenchmark for (2810ds/797Mi)
% 151.21/22.39 % (1290395)Instruction limit reached!
% 151.21/22.39 % (1290395)------------------------------
% 151.21/22.39 % (1290395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290395)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290395)Termination reason: Instruction limit
% 151.21/22.39 % (1290395)Termination phase: Saturation
% 151.21/22.39 % (1290395)Time elapsed: 10.701 s
% 151.21/22.39 % (1290395)Peak memory usage: 156 MB
% 151.21/22.39 % (1290395)Instructions burned: 11145 (million)
% 151.21/22.39 % (1290419)Instruction limit reached!
% 151.21/22.39 % (1290419)------------------------------
% 151.21/22.39 % (1290419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290419)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290419)Termination reason: Instruction limit
% 151.21/22.39 % (1290419)Termination phase: Saturation
% 151.21/22.39 % (1290419)Time elapsed: 2.037 s
% 151.21/22.39 % (1290419)Peak memory usage: 148 MB
% 151.21/22.39 % (1290419)Instructions burned: 2034 (million)
% 151.21/22.39 % (1290429)Instruction limit reached!
% 151.21/22.39 % (1290429)------------------------------
% 151.21/22.39 % (1290429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290429)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290429)Termination reason: Instruction limit
% 151.21/22.39 % (1290429)Termination phase: Saturation
% 151.21/22.39 % (1290429)Time elapsed: 0.436 s
% 151.21/22.39 % (1290429)Peak memory usage: 106 MB
% 151.21/22.39 % (1290429)Instructions burned: 799 (million)
% 151.21/22.39 % (1290431)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=4070077715:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2805 on theBenchmark for (2805ds/2326Mi)
% 151.21/22.39 % (1290432)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2189778290:i=6038:nm=6_2805 on theBenchmark for (2805ds/6038Mi)
% 151.21/22.39 % (1290433)lrs+10_1_sil=32000:sp=occurrence:random_seed=4234232224:st=2:i=33334:sd=3:ss=included:sgt=32_2804 on theBenchmark for (2804ds/33334Mi)
% 151.21/22.39 % (1290423)Instruction limit reached!
% 151.21/22.39 % (1290423)------------------------------
% 151.21/22.39 % (1290423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290423)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290423)Termination reason: Instruction limit
% 151.21/22.39 % (1290423)Termination phase: Saturation
% 151.21/22.39 % (1290423)Time elapsed: 1.999 s
% 151.21/22.39 % (1290423)Peak memory usage: 145 MB
% 151.21/22.39 % (1290423)Instructions burned: 2055 (million)
% 151.21/22.39 % (1290417)Instruction limit reached!
% 151.21/22.39 % (1290417)------------------------------
% 151.21/22.39 % (1290417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.21/22.39 % (1290417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.21/22.39 % (1290417)CaDiCaL version: 2.1.3
% 151.21/22.39 % (1290417)Termination reason: Instruction limit
% 151.21/22.39 % (1290417)Termination phase: Saturation
% 151.21/22.39 % (1290417)Time elapsed: 3.162 s
% 151.21/22.39 % (1290417)Peak memory usage: 208 MB
% 151.21/22.39 % (1290417)Instructions burned: 3224 (million)
% 151.21/22.39 % (1290441)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2784602861:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2798 on theBenchmark for (2798ds/1008Mi)
% 151.21/22.39 % (1290442)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=3363890986:i=8327:s2at=5:bd=preordered_2797 on theBenchmark for (2797ds/8327Mi)
% 151.21/22.39 % (1290441)First to succeed.
% 151.21/22.39 % (1290441)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1290272"
% 151.21/22.39 % (1290441)Refutation found. Thanks to Tanya!
% 151.21/22.39 % SZS status Theorem for theBenchmark
% 151.21/22.39 % SZS output start Proof for theBenchmark
% See solution above
% 151.88/22.64 % (1290441)------------------------------
% 151.88/22.64 % (1290441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.88/22.64 % (1290441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.88/22.64 % (1290441)CaDiCaL version: 2.1.3
% 151.88/22.64 % (1290441)Termination reason: Refutation
% 151.88/22.64 % (1290441)Time elapsed: 0.679 s
% 151.88/22.64 % (1290441)Peak memory usage: 99 MB
% 151.88/22.64 % (1290441)Instructions burned: 727 (million)
% 151.88/22.64 % (1290441)------------------------------
% 151.88/22.64 % (1290441)------------------------------
% 151.88/22.64 % (1290272)Success in time 21.518 s
% 151.88/22.64 % Vampire exiting
%------------------------------------------------------------------------------