%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX194-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.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 01:46:07 PM UTC 2026
% Result : Unsatisfiable 153.58s 39.63s
% Output : Refutation 275.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 34
% Syntax : Number of formulae : 109 ( 109 unt; 0 def)
% Number of atoms : 109 ( 108 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 18 ( 18 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 3 con; 0-3 aty)
% Number of variables : 177 ( 177 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : aux2(X0,X1,btrue) = mul(n(suc(suc(zero))),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_002) ).
fof(f13,axiom,
! [X0,X1] : aux3(X0,X1,btrue) = mul(n(suc(suc(zero))),v(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_012) ).
fof(f14,plain,
! [X0,X1] : mul(n(suc(suc(zero))),v(X0)) = aux3(X0,X1,btrue),
inference(reorient_equations,[],[f13]) ).
fof(f17,axiom,
! [X0,X1] : aux4(X0,X1,btrue) = mul(n(suc(suc(zero))),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_014) ).
fof(f18,plain,
! [X0,X1] : mul(n(suc(suc(zero))),X0) = aux4(X0,X1,btrue),
inference(reorient_equations,[],[f17]) ).
fof(f21,axiom,
! [X0,X1] : aux4(v(X0),v(X1),bfalse) = aux3(X0,X1,eq2(X0,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_016) ).
fof(f47,axiom,
! [X2,X0,X1] : aux6(X0,X1,v(X2)) = fail4(y(X0),b(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_031) ).
fof(f48,plain,
! [X2,X0,X1] : fail4(y(X0),b(X1)) = aux6(X0,X1,v(X2)),
inference(reorient_equations,[],[f47]) ).
fof(f67,axiom,
! [X0,X1] : fail1(X0,X1) = aux2(X0,X1,eq3(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_042) ).
fof(f73,axiom,
! [X0,X1] : fail(X0,v(X1)) = fail1(X0,v(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_048) ).
fof(f100,axiom,
! [X0,X1] : fail13(X0,X1) = aux4(X0,X1,eq3(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_074) ).
fof(f106,axiom,
! [X0,X1] : fail4(X0,v(X1)) = fail13(X0,v(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_080) ).
fof(f107,axiom,
! [X0] : b(X0) = simp1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_081) ).
fof(f108,axiom,
! [X0] : y(X0) = simp1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_082) ).
fof(f140,axiom,
! [X0] : b2(X0) = simp1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_108) ).
fof(f141,plain,
! [X0] : simp1(X0) = b2(X0),
inference(reorient_equations,[],[f140]) ).
fof(f143,axiom,
! [X0] : b3(X0) = simp1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_110) ).
fof(f144,plain,
! [X0] : simp1(X0) = b3(X0),
inference(reorient_equations,[],[f143]) ).
fof(f164,axiom,
! [X0,X1] : simp1(add(X0,X1)) = aux6(X0,X1,y(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_127) ).
fof(f169,axiom,
! [X0] : simp1(v(X0)) = v(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_131) ).
fof(f170,plain,
! [X0] : v(X0) = simp1(v(X0)),
inference(reorient_equations,[],[f169]) ).
fof(f173,axiom,
! [X0,X1] : fetch(cons(X0,X1),zero) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_133) ).
fof(f174,axiom,
! [X2,X0,X1] : fetch(cons(X0,X1),suc(X2)) = fetch(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_134) ).
fof(f175,axiom,
! [X0] : addNat(zero,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_135) ).
fof(f176,axiom,
! [X0,X1] : addNat(suc(X0),X1) = suc(addNat(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_136) ).
fof(f177,axiom,
! [X0] : mulNat(zero,X0) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_137) ).
fof(f178,plain,
! [X0] : zero = mulNat(zero,X0),
inference(reorient_equations,[],[f177]) ).
fof(f179,axiom,
! [X0,X1] : mulNat(suc(X0),X1) = addNat(X1,mulNat(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_138) ).
fof(f180,axiom,
! [X0,X1] : eval(X0,n(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_139) ).
fof(f181,axiom,
! [X2,X0,X1] : eval(X0,add(X1,X2)) = addNat(eval(X0,X1),eval(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_140) ).
fof(f182,axiom,
! [X2,X0,X1] : eval(X0,mul(X1,X2)) = mulNat(eval(X0,X1),eval(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_141) ).
fof(f184,axiom,
! [X0,X1] : eval(X0,v(X1)) = fetch(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_143) ).
fof(f185,axiom,
! [X0,X1] : prop1(X0,X1) = eq4(eq2(eval(X0,X1),eval(X0,simp1(X1))),btrue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_144) ).
fof(f186,axiom,
eq4(bfalse,btrue) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_145) ).
fof(f187,plain,
bfalse = eq4(bfalse,btrue),
inference(reorient_equations,[],[f186]) ).
fof(f190,axiom,
! [X0,X1] : eq3(n(X0),n(X1)) = eq2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_147) ).
fof(f203,axiom,
! [X0,X1] : eq3(v(X0),v(X1)) = eq2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_154) ).
fof(f204,plain,
! [X0,X1] : eq2(X0,X1) = eq3(v(X0),v(X1)),
inference(reorient_equations,[],[f203]) ).
fof(f247,axiom,
! [X0] : eq2(zero,suc(X0)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_176) ).
fof(f248,plain,
! [X0] : bfalse = eq2(zero,suc(X0)),
inference(reorient_equations,[],[f247]) ).
fof(f249,axiom,
! [X0] : eq2(suc(X0),zero) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_177) ).
fof(f250,plain,
! [X0] : bfalse = eq2(suc(X0),zero),
inference(reorient_equations,[],[f249]) ).
fof(f253,axiom,
! [X0] : eq3(X0,X0) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_179) ).
fof(f254,plain,
! [X0] : btrue = eq3(X0,X0),
inference(reorient_equations,[],[f253]) ).
fof(f255,axiom,
! [X0] : eq4(X0,X0) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_180) ).
fof(f256,plain,
! [X0] : btrue = eq4(X0,X0),
inference(reorient_equations,[],[f255]) ).
fof(f257,negated_conjecture,
! [X0,X1] : eq4(prop1(X0,X1),bfalse) != btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f258,plain,
! [X0,X1] : btrue != eq4(prop1(X0,X1),bfalse),
inference(reorient_equations,[],[f257]) ).
fof(f259,plain,
! [X0,X1] : prop1(X0,X1) = eq4(eq3(n(eval(X0,X1)),n(eval(X0,b2(X1)))),btrue),
inference(definition_unfolding,[],[f185,f190,f141]) ).
fof(f260,plain,
! [X0] : b(X0) = b2(X0),
inference(definition_unfolding,[],[f107,f141]) ).
fof(f261,plain,
! [X0] : y(X0) = b2(X0),
inference(definition_unfolding,[],[f108,f141]) ).
fof(f267,plain,
! [X0,X1] : aux4(v(X0),v(X1),bfalse) = aux3(X0,X1,eq3(n(X0),n(X0))),
inference(definition_unfolding,[],[f21,f190]) ).
fof(f275,plain,
! [X2,X0,X1] : aux6(X0,X1,v(X2)) = fail4(b2(X0),b2(X1)),
inference(definition_unfolding,[],[f48,f261,f260]) ).
fof(f286,plain,
! [X0,X1] : fail(X0,v(X1)) = aux2(X0,v(X1),eq3(X0,v(X1))),
inference(definition_unfolding,[],[f73,f67]) ).
fof(f295,plain,
! [X0,X1] : fail4(X0,v(X1)) = aux4(X0,v(X1),eq3(X0,v(X1))),
inference(definition_unfolding,[],[f106,f100]) ).
fof(f300,plain,
! [X0] : b2(X0) = b3(X0),
inference(definition_unfolding,[],[f144,f141]) ).
fof(f304,plain,
! [X0,X1] : b2(add(X0,X1)) = aux6(X0,X1,b2(X0)),
inference(definition_unfolding,[],[f164,f141,f261]) ).
fof(f308,plain,
! [X0] : v(X0) = b2(v(X0)),
inference(definition_unfolding,[],[f170,f141]) ).
fof(f310,plain,
! [X0,X1] : eval(cons(X0,X1),v(zero)) = X0,
inference(definition_unfolding,[],[f173,f184]) ).
fof(f311,plain,
! [X2,X0,X1] : eval(cons(X0,X1),v(suc(X2))) = eval(X1,v(X2)),
inference(definition_unfolding,[],[f174,f184,f184]) ).
fof(f315,plain,
! [X0,X1] : eq3(n(X0),n(X1)) = eq3(v(X0),v(X1)),
inference(definition_unfolding,[],[f204,f190]) ).
fof(f325,plain,
! [X0] : bfalse = eq3(n(zero),n(suc(X0))),
inference(definition_unfolding,[],[f248,f190]) ).
fof(f326,plain,
! [X0] : bfalse = eq3(n(suc(X0)),n(zero)),
inference(definition_unfolding,[],[f250,f190]) ).
fof(f328,plain,
! [X0,X1] : btrue != eq4(eq4(eq3(n(eval(X0,X1)),n(eval(X0,b2(X1)))),btrue),bfalse),
inference(definition_unfolding,[],[f258,f259]) ).
fof(f334,plain,
! [X0] : v(X0) = b3(v(X0)),
inference(forward_demodulation,[],[f308,f300]) ).
fof(f391,plain,
! [X0] : mulNat(suc(zero),X0) = addNat(X0,zero),
inference(superposition,[],[f179,f178]) ).
fof(f392,plain,
! [X0] : mulNat(X0,zero) = mulNat(suc(X0),zero),
inference(superposition,[],[f179,f175]) ).
fof(f393,plain,
! [X0,X1] : suc(addNat(X0,mulNat(X1,suc(X0)))) = mulNat(suc(X1),suc(X0)),
inference(superposition,[],[f179,f176]) ).
fof(f397,plain,
! [X0,X1] : b2(add(X0,X1)) = aux6(X0,X1,b3(X0)),
inference(forward_demodulation,[],[f304,f300]) ).
fof(f398,plain,
! [X0,X1] : aux6(X0,X1,b3(X0)) = b3(add(X0,X1)),
inference(forward_demodulation,[],[f397,f300]) ).
fof(f408,plain,
! [X0,X1] : b3(add(v(X0),X1)) = aux6(v(X0),X1,v(X0)),
inference(superposition,[],[f398,f334]) ).
fof(f459,plain,
! [X2,X0,X1] : aux6(X0,X1,v(X2)) = fail4(b2(X0),b3(X1)),
inference(forward_demodulation,[],[f275,f300]) ).
fof(f460,plain,
! [X2,X0,X1] : aux6(X0,X1,v(X2)) = fail4(b3(X0),b3(X1)),
inference(forward_demodulation,[],[f459,f300]) ).
fof(f464,plain,
! [X0] : bfalse = eq3(v(zero),v(suc(X0))),
inference(superposition,[],[f315,f325]) ).
fof(f465,plain,
! [X0] : bfalse = eq3(v(suc(X0)),v(zero)),
inference(superposition,[],[f315,f326]) ).
fof(f469,plain,
! [X0,X1] : btrue != eq4(eq4(eq3(v(eval(X0,X1)),v(eval(X0,b2(X1)))),btrue),bfalse),
inference(superposition,[],[f328,f315]) ).
fof(f474,plain,
! [X0,X1] : btrue != eq4(eq4(eq3(v(eval(X0,X1)),v(eval(X0,b3(X1)))),btrue),bfalse),
inference(forward_demodulation,[],[f469,f300]) ).
fof(f745,plain,
! [X2,X0,X1] : eval(cons(X0,X1),add(v(zero),X2)) = addNat(X0,eval(cons(X0,X1),X2)),
inference(superposition,[],[f181,f310]) ).
fof(f763,plain,
! [X2,X0,X1] : eval(cons(X0,X1),mul(X2,v(zero))) = mulNat(eval(cons(X0,X1),X2),X0),
inference(superposition,[],[f182,f310]) ).
fof(f784,plain,
! [X0] : fail(v(X0),v(X0)) = aux2(v(X0),v(X0),btrue),
inference(superposition,[],[f286,f254]) ).
fof(f797,plain,
! [X0] : mul(n(suc(suc(zero))),v(X0)) = fail(v(X0),v(X0)),
inference(forward_demodulation,[],[f784,f3]) ).
fof(f840,plain,
! [X0] : fail4(v(X0),v(X0)) = aux4(v(X0),v(X0),btrue),
inference(superposition,[],[f295,f254]) ).
fof(f843,plain,
! [X0] : fail4(v(zero),v(suc(X0))) = aux4(v(zero),v(suc(X0)),bfalse),
inference(superposition,[],[f295,f464]) ).
fof(f853,plain,
! [X0] : mul(n(suc(suc(zero))),v(X0)) = fail4(v(X0),v(X0)),
inference(forward_demodulation,[],[f840,f18]) ).
fof(f942,plain,
! [X0,X1] : aux3(X0,X1,btrue) = aux4(v(X0),v(X1),bfalse),
inference(forward_demodulation,[],[f267,f254]) ).
fof(f1498,plain,
! [X0,X1] : b3(add(v(X0),X1)) = fail4(b3(v(X0)),b3(X1)),
inference(forward_demodulation,[],[f408,f460]) ).
fof(f1499,plain,
! [X0,X1] : b3(add(v(X0),X1)) = fail4(v(X0),b3(X1)),
inference(forward_demodulation,[],[f1498,f334]) ).
fof(f2804,plain,
! [X0,X1] : bfalse = eq3(v(mulNat(suc(X0),suc(X1))),v(zero)),
inference(superposition,[],[f465,f393]) ).
fof(f3305,plain,
! [X0] : fail(v(X0),v(X0)) = fail4(v(X0),v(X0)),
inference(superposition,[],[f853,f797]) ).
fof(f4711,plain,
! [X2,X0,X1] : btrue != eq4(eq4(eq3(v(addNat(X0,eval(cons(X0,X1),X2))),v(eval(cons(X0,X1),b3(add(v(zero),X2))))),btrue),bfalse),
inference(superposition,[],[f474,f745]) ).
fof(f4736,plain,
! [X2,X0,X1] : btrue != eq4(eq4(eq3(v(addNat(X0,eval(cons(X0,X1),X2))),v(eval(cons(X0,X1),fail4(v(zero),b3(X2))))),btrue),bfalse),
inference(forward_demodulation,[],[f4711,f1499]) ).
fof(f4886,plain,
! [X0,X1] : mulNat(eval(cons(X0,X1),n(suc(suc(zero)))),X0) = eval(cons(X0,X1),fail4(v(zero),v(zero))),
inference(superposition,[],[f763,f853]) ).
fof(f4955,plain,
! [X0,X1] : mulNat(suc(suc(zero)),X0) = eval(cons(X0,X1),fail4(v(zero),v(zero))),
inference(forward_demodulation,[],[f4886,f180]) ).
fof(f8175,plain,
! [X0,X1] : btrue != eq4(eq4(eq3(v(eval(cons(zero,X0),X1)),v(eval(cons(zero,X0),fail4(v(zero),b3(X1))))),btrue),bfalse),
inference(superposition,[],[f4736,f175]) ).
fof(f8202,plain,
! [X0,X1] : btrue != eq4(eq4(eq3(v(eval(X0,v(X1))),v(eval(cons(zero,X0),fail4(v(zero),b3(v(suc(X1))))))),btrue),bfalse),
inference(superposition,[],[f8175,f311]) ).
fof(f8225,plain,
! [X0,X1] : btrue != eq4(eq4(eq3(v(eval(X0,v(X1))),v(eval(cons(zero,X0),fail4(v(zero),v(suc(X1)))))),btrue),bfalse),
inference(forward_demodulation,[],[f8202,f334]) ).
fof(f8580,plain,
! [X0,X1] : btrue != eq4(eq4(eq3(v(X0),v(eval(cons(zero,cons(X0,X1)),fail4(v(zero),v(suc(zero)))))),btrue),bfalse),
inference(superposition,[],[f8225,f310]) ).
fof(f19468,plain,
! [X0] : fail4(v(zero),v(suc(X0))) = aux3(zero,suc(X0),btrue),
inference(forward_demodulation,[],[f843,f942]) ).
fof(f19469,plain,
! [X0] : fail4(v(zero),v(suc(X0))) = mul(n(suc(suc(zero))),v(zero)),
inference(forward_demodulation,[],[f19468,f14]) ).
fof(f19470,plain,
! [X0] : fail4(v(zero),v(suc(X0))) = fail(v(zero),v(zero)),
inference(forward_demodulation,[],[f19469,f797]) ).
fof(f19471,plain,
! [X0] : fail4(v(zero),v(suc(X0))) = fail4(v(zero),v(zero)),
inference(forward_demodulation,[],[f19470,f3305]) ).
fof(f22919,plain,
! [X0,X1] : btrue != eq4(eq4(eq3(v(X0),v(eval(cons(zero,cons(X0,X1)),fail4(v(zero),v(zero))))),btrue),bfalse),
inference(forward_demodulation,[],[f8580,f19471]) ).
fof(f24644,plain,
! [X0] : btrue != eq4(eq4(eq3(v(X0),v(mulNat(suc(suc(zero)),zero))),btrue),bfalse),
inference(superposition,[],[f22919,f4955]) ).
fof(f24685,plain,
! [X0] : btrue != eq4(eq4(eq3(v(X0),v(mulNat(suc(zero),zero))),btrue),bfalse),
inference(forward_demodulation,[],[f24644,f392]) ).
fof(f24692,plain,
! [X0] : btrue != eq4(eq4(eq3(v(X0),v(addNat(zero,zero))),btrue),bfalse),
inference(forward_demodulation,[],[f24685,f391]) ).
fof(f24696,plain,
! [X0] : btrue != eq4(eq4(eq3(v(X0),v(zero)),btrue),bfalse),
inference(forward_demodulation,[],[f24692,f175]) ).
fof(f24704,plain,
btrue != eq4(eq4(bfalse,btrue),bfalse),
inference(superposition,[],[f24696,f2804]) ).
fof(f24707,plain,
btrue != eq4(bfalse,bfalse),
inference(forward_demodulation,[],[f24704,f187]) ).
fof(f24710,plain,
$false,
inference(forward_subsumption_resolution,[],[f24707,f256]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX194-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 % Computer : n020.cluster.edu
% 0.10/0.23 % Model : x86_64 x86_64
% 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.23 % Memory : 8046.5625MB
% 0.10/0.23 % OS : Linux 6.8.0-71-generic
% 0.10/0.23 % CPULimit : 300
% 0.10/0.23 % WCLimit : 300
% 0.10/0.23 % DateTime : Mon Sep 28 15:07:50 UTC 2026
% 0.10/0.23 % CPUTime :
% 0.10/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.29 Running first-order theorem proving
% 0.10/0.29 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
% 17.35/3.20 % (232222)Input is clausal, will run a generic CNF schedule.
% 17.35/3.20 % (232236)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=3364347673:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 17.35/3.20 % (232239)lrs+10_1_sil=8000:sp=occurrence:random_seed=3901227272:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 17.35/3.20 % (232242)dis-21_1_sil=8000:lcm=predicate:random_seed=1841472068:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 17.35/3.20 % (232242)Refutation not found, incomplete strategy
% 17.35/3.20 % (232242)------------------------------
% 17.35/3.20 % (232242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.35/3.20 % (232242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.35/3.20 % (232242)CaDiCaL version: 2.1.3
% 17.35/3.20 % (232242)Termination reason: Refutation not found, incomplete strategy
% 17.35/3.20 % (232242)Time elapsed: 0.010 s
% 17.35/3.20 % (232242)Peak memory usage: 88 MB
% 17.35/3.20 % (232242)Instructions burned: 10 (million)
% 17.35/3.20 % (232237)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3171691587:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 17.35/3.20 % (232240)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4050503859:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 17.35/3.20 % (232241)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4168681779:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 17.35/3.20 % (232238)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2205876651:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 17.35/3.20 % (232239)Instruction limit reached!
% 17.35/3.20 % (232239)------------------------------
% 17.35/3.20 % (232239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.35/3.20 % (232239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.35/3.20 % (232239)CaDiCaL version: 2.1.3
% 17.35/3.20 % (232239)Termination reason: Instruction limit
% 17.35/3.20 % (232239)Termination phase: Saturation
% 17.35/3.20 % (232239)Time elapsed: 0.111 s
% 17.35/3.20 % (232239)Peak memory usage: 89 MB
% 17.35/3.20 % (232239)Instructions burned: 107 (million)
% 17.35/3.20 % (232240)Instruction limit reached!
% 17.35/3.20 % (232240)------------------------------
% 17.35/3.20 % (232240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.35/3.20 % (232240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.35/3.20 % (232240)CaDiCaL version: 2.1.3
% 17.35/3.20 % (232240)Termination reason: Instruction limit
% 17.35/3.20 % (232240)Termination phase: Saturation
% 17.35/3.20 % (232240)Time elapsed: 0.117 s
% 17.35/3.20 % (232240)Peak memory usage: 90 MB
% 17.35/3.20 % (232240)Instructions burned: 114 (million)
% 17.35/3.20 % (232241)Instruction limit reached!
% 17.35/3.20 % (232241)------------------------------
% 17.35/3.20 % (232241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.35/3.20 % (232241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.35/3.20 % (232241)CaDiCaL version: 2.1.3
% 17.35/3.20 % (232241)Termination reason: Instruction limit
% 17.35/3.20 % (232241)Termination phase: Saturation
% 17.35/3.20 % (232241)Time elapsed: 0.183 s
% 17.35/3.20 % (232241)Peak memory usage: 90 MB
% 17.35/3.20 % (232241)Instructions burned: 180 (million)
% 17.35/3.20 % (232255)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3773722728:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 17.35/3.20 % (232255)Refutation not found, incomplete strategy
% 17.35/3.20 % (232255)------------------------------
% 17.35/3.20 % (232255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.35/3.20 % (232255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.35/3.20 % (232255)CaDiCaL version: 2.1.3
% 17.35/3.20 % (232255)Termination reason: Refutation not found, incomplete strategy
% 17.35/3.20 % (232255)Time elapsed: 0.004 s
% 17.35/3.20 % (232255)Peak memory usage: 88 MB
% 17.35/3.20 % (232255)Instructions burned: 2 (million)
% 17.35/3.20 % (232256)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4288003212:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 27.58/4.90 % (232256)Refutation not found, incomplete strategy
% 27.58/4.90 % (232256)------------------------------
% 27.58/4.90 % (232256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.58/4.90 % (232256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.58/4.90 % (232256)CaDiCaL version: 2.1.3
% 27.58/4.90 % (232256)Termination reason: Refutation not found, incomplete strategy
% 27.58/4.90 % (232256)Time elapsed: 0.016 s
% 27.58/4.90 % (232256)Peak memory usage: 88 MB
% 27.58/4.90 % (232256)Instructions burned: 14 (million)
% 27.58/4.90 % (232257)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3489710473:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 27.58/4.90 % (232257)Refutation not found, incomplete strategy
% 27.58/4.90 % (232257)------------------------------
% 27.58/4.90 % (232257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.58/4.90 % (232257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.58/4.90 % (232257)CaDiCaL version: 2.1.3
% 27.58/4.90 % (232257)Termination reason: Refutation not found, incomplete strategy
% 27.58/4.90 % (232257)Time elapsed: 0.011 s
% 27.58/4.90 % (232257)Peak memory usage: 88 MB
% 27.58/4.90 % (232257)Instructions burned: 10 (million)
% 27.58/4.90 % (232242)------------------------------
% 27.58/4.90 % (232242)------------------------------
% 27.58/4.90 % (232261)lrs+10_64_to=lpo:sil=8000:random_seed=2509850593:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 27.58/4.90 % (232261)Instruction limit reached!
% 27.58/4.90 % (232261)------------------------------
% 27.58/4.90 % (232261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.58/4.90 % (232261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.58/4.90 % (232261)CaDiCaL version: 2.1.3
% 27.58/4.90 % (232261)Termination reason: Instruction limit
% 27.58/4.90 % (232261)Termination phase: Saturation
% 27.58/4.90 % (232261)Time elapsed: 0.064 s
% 27.58/4.90 % (232261)Peak memory usage: 89 MB
% 27.58/4.90 % (232261)Instructions burned: 126 (million)
% 27.58/4.90 % (232255)------------------------------
% 27.58/4.90 % (232255)------------------------------
% 27.58/4.90 % (232256)------------------------------
% 27.58/4.90 % (232256)------------------------------
% 27.58/4.90 % (232257)------------------------------
% 27.58/4.90 % (232257)------------------------------
% 27.58/4.90 % (232266)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=926984081:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 27.58/4.90 % (232265)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3637770909:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi)
% 27.58/4.90 % (232266)Instruction limit reached!
% 27.58/4.90 % (232266)------------------------------
% 27.58/4.90 % (232266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.58/4.90 % (232266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.58/4.90 % (232266)CaDiCaL version: 2.1.3
% 27.58/4.90 % (232266)Termination reason: Instruction limit
% 27.58/4.90 % (232266)Termination phase: Saturation
% 27.58/4.90 % (232266)Time elapsed: 0.081 s
% 27.58/4.90 % (232266)Peak memory usage: 90 MB
% 27.58/4.90 % (232266)Instructions burned: 158 (million)
% 27.58/4.90 % (232267)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2477791820:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 27.58/4.90 % (232268)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1848406181:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 27.58/4.90 % (232265)Instruction limit reached!
% 27.58/4.90 % (232265)------------------------------
% 27.58/4.90 % (232265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.58/4.90 % (232265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.58/4.90 % (232265)CaDiCaL version: 2.1.3
% 27.58/4.90 % (232265)Termination reason: Instruction limit
% 27.58/4.90 % (232265)Termination phase: Saturation
% 27.58/4.90 % (232265)Time elapsed: 0.200 s
% 27.58/4.90 % (232265)Peak memory usage: 89 MB
% 27.58/4.90 % (232265)Instructions burned: 194 (million)
% 27.58/4.90 % (232271)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4274816966:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 51.83/8.13 % (232268)Instruction limit reached!
% 51.83/8.13 % (232268)------------------------------
% 51.83/8.13 % (232268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.83/8.13 % (232268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.83/8.13 % (232268)CaDiCaL version: 2.1.3
% 51.83/8.13 % (232268)Termination reason: Instruction limit
% 51.83/8.13 % (232268)Termination phase: Saturation
% 51.83/8.13 % (232268)Time elapsed: 0.116 s
% 51.83/8.13 % (232268)Peak memory usage: 89 MB
% 51.83/8.13 % (232268)Instructions burned: 106 (million)
% 51.83/8.13 % (232271)Instruction limit reached!
% 51.83/8.13 % (232271)------------------------------
% 51.83/8.13 % (232271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.83/8.13 % (232271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.83/8.13 % (232271)CaDiCaL version: 2.1.3
% 51.83/8.13 % (232271)Termination reason: Instruction limit
% 51.83/8.13 % (232271)Termination phase: Saturation
% 51.83/8.13 % (232271)Time elapsed: 0.092 s
% 51.83/8.13 % (232271)Peak memory usage: 88 MB
% 51.83/8.13 % (232271)Instructions burned: 107 (million)
% 51.83/8.13 % (232274)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3046646968:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 51.83/8.13 % (232276)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=661178203:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 51.83/8.13 % (232277)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4153838151:i=134:sd=2:doe=on:ss=axioms:sgt=14_2986 on theBenchmark for (2986ds/134Mi)
% 51.83/8.13 % (232274)Instruction limit reached!
% 51.83/8.13 % (232274)------------------------------
% 51.83/8.13 % (232274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.83/8.13 % (232274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.83/8.13 % (232274)CaDiCaL version: 2.1.3
% 51.83/8.13 % (232274)Termination reason: Instruction limit
% 51.83/8.13 % (232274)Termination phase: Saturation
% 51.83/8.13 % (232274)Time elapsed: 0.230 s
% 51.83/8.13 % (232274)Peak memory usage: 91 MB
% 51.83/8.13 % (232274)Instructions burned: 242 (million)
% 51.83/8.13 % (232277)Instruction limit reached!
% 51.83/8.13 % (232277)------------------------------
% 51.83/8.13 % (232277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.83/8.13 % (232277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.83/8.13 % (232277)CaDiCaL version: 2.1.3
% 51.83/8.13 % (232277)Termination reason: Instruction limit
% 51.83/8.13 % (232277)Termination phase: Saturation
% 51.83/8.13 % (232277)Time elapsed: 0.136 s
% 51.83/8.13 % (232277)Peak memory usage: 90 MB
% 51.83/8.13 % (232277)Instructions burned: 134 (million)
% 51.83/8.13 % (232281)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1379599586:i=499:bd=all_2983 on theBenchmark for (2983ds/499Mi)
% 51.83/8.13 % (232282)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1026306433:i=191:fgj=on:bd=all_2982 on theBenchmark for (2982ds/191Mi)
% 51.83/8.13 % (232282)Instruction limit reached!
% 51.83/8.13 % (232282)------------------------------
% 51.83/8.14 % (232282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.83/8.14 % (232282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.83/8.14 % (232282)CaDiCaL version: 2.1.3
% 51.83/8.14 % (232282)Termination reason: Instruction limit
% 51.83/8.14 % (232282)Termination phase: Saturation
% 51.83/8.14 % (232282)Time elapsed: 0.197 s
% 51.83/8.14 % (232282)Peak memory usage: 89 MB
% 51.83/8.14 % (232282)Instructions burned: 192 (million)
% 51.83/8.14 % (232287)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=909158880:i=264:kws=precedence:fsr=off_2978 on theBenchmark for (2978ds/264Mi)
% 51.83/8.14 % (232281)Instruction limit reached!
% 51.83/8.14 % (232281)------------------------------
% 51.83/8.14 % (232281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.83/8.14 % (232281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.83/8.14 % (232281)CaDiCaL version: 2.1.3
% 51.83/8.14 % (232281)Termination reason: Instruction limit
% 51.83/8.14 % (232281)Termination phase: Saturation
% 51.83/8.14 % (232281)Time elapsed: 0.464 s
% 51.83/8.14 % (232281)Peak memory usage: 94 MB
% 86.25/12.93 % (232281)Instructions burned: 500 (million)
% 86.25/12.93 % (232289)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=995218137:cond=on:i=156:bs=on:gtg=exists_all:er=known_2976 on theBenchmark for (2976ds/156Mi)
% 86.25/12.93 % (232287)Instruction limit reached!
% 86.25/12.93 % (232287)------------------------------
% 86.25/12.93 % (232287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.25/12.93 % (232287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.25/12.93 % (232287)CaDiCaL version: 2.1.3
% 86.25/12.93 % (232287)Termination reason: Instruction limit
% 86.25/12.93 % (232287)Termination phase: Saturation
% 86.25/12.93 % (232287)Time elapsed: 0.265 s
% 86.25/12.93 % (232287)Peak memory usage: 91 MB
% 86.25/12.93 % (232287)Instructions burned: 264 (million)
% 86.25/12.93 % (232289)Instruction limit reached!
% 86.25/12.93 % (232289)------------------------------
% 86.25/12.93 % (232289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.25/12.93 % (232289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.25/12.93 % (232289)CaDiCaL version: 2.1.3
% 86.25/12.93 % (232289)Termination reason: Instruction limit
% 86.25/12.93 % (232289)Termination phase: Saturation
% 86.25/12.93 % (232289)Time elapsed: 0.147 s
% 86.25/12.93 % (232289)Peak memory usage: 89 MB
% 86.25/12.93 % (232289)Instructions burned: 156 (million)
% 86.25/12.93 % (232291)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3627735910:i=3256:kws=precedence:bd=preordered:av=off_2973 on theBenchmark for (2973ds/3256Mi)
% 86.25/12.93 % (232292)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=431304708:i=537:av=off:ss=included_2972 on theBenchmark for (2972ds/537Mi)
% 86.25/12.93 % (232267)Instruction limit reached!
% 86.25/12.93 % (232267)------------------------------
% 86.25/12.93 % (232267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.25/12.93 % (232267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.25/12.93 % (232267)CaDiCaL version: 2.1.3
% 86.25/12.93 % (232267)Termination reason: Instruction limit
% 86.25/12.93 % (232267)Termination phase: Saturation
% 86.25/12.93 % (232267)Time elapsed: 1.892 s
% 86.25/12.93 % (232267)Peak memory usage: 152 MB
% 86.25/12.93 % (232267)Instructions burned: 3395 (million)
% 86.25/12.93 % (232295)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2095961498:i=180:bd=preordered:av=off_2969 on theBenchmark for (2969ds/180Mi)
% 86.25/12.93 % (232295)Instruction limit reached!
% 86.25/12.93 % (232295)------------------------------
% 86.25/12.93 % (232295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.25/12.93 % (232295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.25/12.93 % (232295)CaDiCaL version: 2.1.3
% 86.25/12.93 % (232295)Termination reason: Instruction limit
% 86.25/12.93 % (232295)Termination phase: Saturation
% 86.25/12.93 % (232295)Time elapsed: 0.094 s
% 86.25/12.93 % (232295)Peak memory usage: 90 MB
% 86.25/12.93 % (232295)Instructions burned: 183 (million)
% 86.25/12.93 % (232292)Instruction limit reached!
% 86.25/12.93 % (232292)------------------------------
% 86.25/12.93 % (232292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.25/12.93 % (232292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.25/12.93 % (232292)CaDiCaL version: 2.1.3
% 86.25/12.93 % (232292)Termination reason: Instruction limit
% 86.25/12.93 % (232292)Termination phase: Saturation
% 86.25/12.93 % (232292)Time elapsed: 0.479 s
% 86.25/12.93 % (232292)Peak memory usage: 91 MB
% 86.25/12.93 % (232292)Instructions burned: 537 (million)
% 86.25/12.93 % (232297)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1808063600:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2966 on theBenchmark for (2966ds/10307Mi)
% 86.25/12.93 % (232298)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=1089905670:i=412:gtgl=4:gtg=exists_all_2965 on theBenchmark for (2965ds/412Mi)
% 86.25/12.93 % (232298)Instruction limit reached!
% 86.25/12.93 % (232298)------------------------------
% 86.25/12.93 % (232298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.25/12.93 % (232298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.25/12.93 % (232298)CaDiCaL version: 2.1.3
% 115.63/17.04 % (232298)Termination reason: Instruction limit
% 115.63/17.04 % (232298)Termination phase: Saturation
% 115.63/17.04 % (232298)Time elapsed: 0.403 s
% 115.63/17.04 % (232298)Peak memory usage: 98 MB
% 115.63/17.04 % (232298)Instructions burned: 412 (million)
% 115.63/17.04 % (232301)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1546751794:s2pl=no:i=8478:s2at=4:nm=6_2959 on theBenchmark for (2959ds/8478Mi)
% 115.63/17.04 % (232291)Instruction limit reached!
% 115.63/17.04 % (232291)------------------------------
% 115.63/17.04 % (232291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.63/17.04 % (232291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.63/17.04 % (232291)CaDiCaL version: 2.1.3
% 115.63/17.04 % (232291)Termination reason: Instruction limit
% 115.63/17.04 % (232291)Termination phase: Saturation
% 115.63/17.04 % (232291)Time elapsed: 2.223 s
% 115.63/17.04 % (232291)Peak memory usage: 152 MB
% 115.63/17.04 % (232291)Instructions burned: 3257 (million)
% 115.63/17.04 % (232305)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=749852563:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2949 on theBenchmark for (2949ds/303Mi)
% 115.63/17.04 % (232305)Instruction limit reached!
% 115.63/17.04 % (232305)------------------------------
% 115.63/17.04 % (232305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.63/17.04 % (232305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.63/17.04 % (232305)CaDiCaL version: 2.1.3
% 115.63/17.04 % (232305)Termination reason: Instruction limit
% 115.63/17.04 % (232305)Termination phase: Saturation
% 115.63/17.04 % (232305)Time elapsed: 0.149 s
% 115.63/17.04 % (232305)Peak memory usage: 92 MB
% 115.63/17.04 % (232305)Instructions burned: 305 (million)
% 115.63/17.04 % (232307)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1411509667:st=4:i=720:sd=3:fsr=off:ss=axioms_2946 on theBenchmark for (2946ds/720Mi)
% 115.63/17.04 % (232307)Refutation not found, incomplete strategy
% 115.63/17.04 % (232307)------------------------------
% 115.63/17.04 % (232307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.63/17.04 % (232307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.63/17.04 % (232307)CaDiCaL version: 2.1.3
% 115.63/17.04 % (232307)Termination reason: Refutation not found, incomplete strategy
% 115.63/17.04 % (232307)Time elapsed: 0.007 s
% 115.63/17.04 % (232307)Peak memory usage: 88 MB
% 115.63/17.04 % (232307)Instructions burned: 11 (million)
% 115.63/17.04 % (232307)------------------------------
% 115.63/17.04 % (232307)------------------------------
% 115.63/17.04 % (232309)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=320235593:i=598:bs=on:bd=preordered:av=off:ss=axioms_2942 on theBenchmark for (2942ds/598Mi)
% 115.63/17.04 % (232309)Instruction limit reached!
% 115.63/17.04 % (232309)------------------------------
% 115.63/17.04 % (232309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.63/17.04 % (232309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.63/17.04 % (232309)CaDiCaL version: 2.1.3
% 115.63/17.04 % (232309)Termination reason: Instruction limit
% 115.63/17.04 % (232309)Termination phase: Saturation
% 115.63/17.04 % (232309)Time elapsed: 0.319 s
% 115.63/17.04 % (232309)Peak memory usage: 92 MB
% 115.63/17.04 % (232309)Instructions burned: 598 (million)
% 115.63/17.04 % (232313)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=4079113867:i=2989:sd=3:ss=axioms:sgt=60_2937 on theBenchmark for (2937ds/2989Mi)
% 115.63/17.04 % (232276)Instruction limit reached!
% 115.63/17.04 % (232276)------------------------------
% 115.63/17.04 % (232276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.63/17.04 % (232276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.63/17.04 % (232276)CaDiCaL version: 2.1.3
% 115.63/17.04 % (232276)Termination reason: Instruction limit
% 115.63/17.04 % (232276)Termination phase: Saturation
% 115.63/17.04 % (232276)Time elapsed: 5.581 s
% 115.63/17.04 % (232276)Peak memory usage: 170 MB
% 115.63/17.04 % (232276)Instructions burned: 5208 (million)
% 115.63/17.04 % (232321)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1298565078:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2928 on theBenchmark for (2928ds/1997Mi)
% 155.26/22.77 % (232313)Instruction limit reached!
% 155.26/22.77 % (232313)------------------------------
% 155.26/22.77 % (232313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.26/22.77 % (232313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.26/22.77 % (232313)CaDiCaL version: 2.1.3
% 155.26/22.77 % (232313)Termination reason: Instruction limit
% 155.26/22.77 % (232313)Termination phase: Saturation
% 155.26/22.77 % (232313)Time elapsed: 1.686 s
% 155.26/22.77 % (232313)Peak memory usage: 147 MB
% 155.26/22.77 % (232313)Instructions burned: 2991 (million)
% 155.26/22.77 % (232324)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2014951925:i=2088:bd=preordered:av=off_2918 on theBenchmark for (2918ds/2088Mi)
% 155.26/22.77 % (232324)Instruction limit reached!
% 155.26/22.77 % (232324)------------------------------
% 155.26/22.77 % (232324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.26/22.77 % (232324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.26/22.77 % (232324)CaDiCaL version: 2.1.3
% 155.26/22.77 % (232324)Termination reason: Instruction limit
% 155.26/22.77 % (232324)Termination phase: Saturation
% 155.26/22.77 % (232324)Time elapsed: 1.234 s
% 155.26/22.77 % (232324)Peak memory usage: 140 MB
% 155.26/22.77 % (232324)Instructions burned: 2088 (million)
% 155.26/22.77 % (232321)Instruction limit reached!
% 155.26/22.77 % (232321)------------------------------
% 155.26/22.77 % (232321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.26/22.77 % (232321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.26/22.77 % (232321)CaDiCaL version: 2.1.3
% 155.26/22.77 % (232321)Termination reason: Instruction limit
% 155.26/22.77 % (232321)Termination phase: Saturation
% 155.26/22.77 % (232321)Time elapsed: 2.208 s
% 155.26/22.77 % (232321)Peak memory usage: 139 MB
% 155.26/22.77 % (232321)Instructions burned: 1997 (million)
% 155.26/22.77 % (232327)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2161844087:i=1098:nicw=on_2904 on theBenchmark for (2904ds/1098Mi)
% 155.26/22.77 % (232328)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2545023116:i=433:bd=preordered_2904 on theBenchmark for (2904ds/433Mi)
% 155.26/22.77 % (232327)Instruction limit reached!
% 155.26/22.77 % (232327)------------------------------
% 155.26/22.77 % (232327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.26/22.77 % (232327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.26/22.77 % (232327)CaDiCaL version: 2.1.3
% 155.26/22.77 % (232327)Termination reason: Instruction limit
% 155.26/22.77 % (232327)Termination phase: Saturation
% 155.26/22.77 % (232327)Time elapsed: 0.524 s
% 155.26/22.77 % (232327)Peak memory usage: 107 MB
% 155.26/22.77 % (232327)Instructions burned: 1100 (million)
% 155.26/22.77 % (232328)Instruction limit reached!
% 155.26/22.77 % (232328)------------------------------
% 155.26/22.77 % (232328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.26/22.77 % (232328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.26/22.77 % (232328)CaDiCaL version: 2.1.3
% 155.26/22.77 % (232328)Termination reason: Instruction limit
% 155.26/22.77 % (232328)Termination phase: Saturation
% 155.26/22.77 % (232328)Time elapsed: 0.454 s
% 155.26/22.77 % (232328)Peak memory usage: 96 MB
% 155.26/22.77 % (232328)Instructions burned: 433 (million)
% 155.26/22.77 % (232333)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1638308016:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2898 on theBenchmark for (2898ds/2942Mi)
% 155.26/22.77 % (232334)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2109091630:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2897 on theBenchmark for (2897ds/6922Mi)
% 155.26/22.77 % (232333)Instruction limit reached!
% 155.26/22.77 % (232333)------------------------------
% 155.26/22.77 % (232333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.26/22.77 % (232333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.26/22.77 % (232333)CaDiCaL version: 2.1.3
% 155.26/22.77 % (232333)Termination reason: Instruction limit
% 155.26/22.77 % (232333)Termination phase: Saturation
% 155.26/22.77 % (232333)Time elapsed: 1.769 s
% 155.26/22.77 % (232333)Peak memory usage: 152 MB
% 192.05/27.99 % (232333)Instructions burned: 2945 (million)
% 192.05/27.99 % (232343)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=4270051766:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2878 on theBenchmark for (2878ds/596Mi)
% 192.05/27.99 % (232343)Instruction limit reached!
% 192.05/27.99 % (232343)------------------------------
% 192.05/27.99 % (232343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.05/27.99 % (232343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.05/27.99 % (232343)CaDiCaL version: 2.1.3
% 192.05/27.99 % (232343)Termination reason: Instruction limit
% 192.05/27.99 % (232343)Termination phase: Saturation
% 192.05/27.99 % (232343)Time elapsed: 0.285 s
% 192.05/27.99 % (232343)Peak memory usage: 95 MB
% 192.05/27.99 % (232343)Instructions burned: 597 (million)
% 192.05/27.99 % (232345)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=4125546028:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2874 on theBenchmark for (2874ds/4123Mi)
% 192.05/27.99 % (232301)Instruction limit reached!
% 192.05/27.99 % (232301)------------------------------
% 192.05/27.99 % (232301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.05/27.99 % (232301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.05/27.99 % (232301)CaDiCaL version: 2.1.3
% 192.05/27.99 % (232301)Termination reason: Instruction limit
% 192.05/27.99 % (232301)Termination phase: Saturation
% 192.05/27.99 % (232301)Time elapsed: 8.969 s
% 192.05/27.99 % (232301)Peak memory usage: 199 MB
% 192.05/27.99 % (232301)Instructions burned: 8478 (million)
% 192.05/27.99 % (232349)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3307749095:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2867 on theBenchmark for (2867ds/16411Mi)
% 192.05/27.99 % (232297)Instruction limit reached!
% 192.05/27.99 % (232297)------------------------------
% 192.05/27.99 % (232297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.05/27.99 % (232297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.05/27.99 % (232297)CaDiCaL version: 2.1.3
% 192.05/27.99 % (232297)Termination reason: Instruction limit
% 192.05/27.99 % (232297)Termination phase: Saturation
% 192.05/27.99 % (232297)Time elapsed: 10.437 s
% 192.05/27.99 % (232297)Peak memory usage: 221 MB
% 192.05/27.99 % (232297)Instructions burned: 10308 (million)
% 192.05/27.99 % (232351)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1107365683:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2860 on theBenchmark for (2860ds/1670Mi)
% 192.05/27.99 % (232345)Instruction limit reached!
% 192.05/27.99 % (232345)------------------------------
% 192.05/27.99 % (232345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.05/27.99 % (232345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.05/27.99 % (232345)CaDiCaL version: 2.1.3
% 192.05/27.99 % (232345)Termination reason: Instruction limit
% 192.05/27.99 % (232345)Termination phase: Saturation
% 192.05/27.99 % (232345)Time elapsed: 2.388 s
% 192.05/27.99 % (232345)Peak memory usage: 161 MB
% 192.05/27.99 % (232345)Instructions burned: 4124 (million)
% 192.05/27.99 % (232353)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=13646643:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2848 on theBenchmark for (2848ds/1722Mi)
% 192.05/27.99 % (232351)Instruction limit reached!
% 192.05/27.99 % (232351)------------------------------
% 192.05/27.99 % (232351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.05/27.99 % (232351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.05/27.99 % (232351)CaDiCaL version: 2.1.3
% 192.05/27.99 % (232351)Termination reason: Instruction limit
% 192.05/27.99 % (232351)Termination phase: Saturation
% 192.05/27.99 % (232351)Time elapsed: 1.717 s
% 192.05/27.99 % (232351)Peak memory usage: 136 MB
% 192.05/27.99 % (232351)Instructions burned: 1670 (million)
% 192.05/27.99 % (232357)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=2883056766:cts=off:cond=on:i=9530:bs=on:fsd=on_2841 on theBenchmark for (2841ds/9530Mi)
% 192.05/27.99 % (232353)Instruction limit reached!
% 192.05/27.99 % (232353)------------------------------
% 228.32/33.03 % (232353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 228.32/33.03 % (232353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.32/33.03 % (232353)CaDiCaL version: 2.1.3
% 228.32/33.03 % (232353)Termination reason: Instruction limit
% 228.32/33.03 % (232353)Termination phase: Saturation
% 228.32/33.03 % (232353)Time elapsed: 0.942 s
% 228.32/33.03 % (232353)Peak memory usage: 136 MB
% 228.32/33.03 % (232353)Instructions burned: 1722 (million)
% 228.32/33.03 % (232360)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1376002876:st=2:i=4495:sd=10:ss=included_2837 on theBenchmark for (2837ds/4495Mi)
% 228.32/33.03 % (232334)Instruction limit reached!
% 228.32/33.03 % (232334)------------------------------
% 228.32/33.03 % (232334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 228.32/33.03 % (232334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.32/33.03 % (232334)CaDiCaL version: 2.1.3
% 228.32/33.03 % (232334)Termination reason: Instruction limit
% 228.32/33.03 % (232334)Termination phase: Saturation
% 228.32/33.03 % (232334)Time elapsed: 7.264 s
% 228.32/33.03 % (232334)Peak memory usage: 190 MB
% 228.32/33.03 % (232334)Instructions burned: 6922 (million)
% 228.32/33.03 % (232364)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=456468119:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2823 on theBenchmark for (2823ds/4920Mi)
% 228.32/33.03 % (232360)Instruction limit reached!
% 228.32/33.03 % (232360)------------------------------
% 228.32/33.03 % (232360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 228.32/33.03 % (232360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.32/33.03 % (232360)CaDiCaL version: 2.1.3
% 228.32/33.03 % (232360)Termination reason: Instruction limit
% 228.32/33.03 % (232360)Termination phase: Saturation
% 228.32/33.03 % (232360)Time elapsed: 2.526 s
% 228.32/33.03 % (232360)Peak memory usage: 163 MB
% 228.32/33.03 % (232360)Instructions burned: 4497 (million)
% 228.32/33.03 % (232366)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=2454387843:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2810 on theBenchmark for (2810ds/2083Mi)
% 228.32/33.03 % (232366)Instruction limit reached!
% 228.32/33.03 % (232366)------------------------------
% 228.32/33.03 % (232366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 228.32/33.03 % (232366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.32/33.03 % (232366)CaDiCaL version: 2.1.3
% 228.32/33.03 % (232366)Termination reason: Instruction limit
% 228.32/33.03 % (232366)Termination phase: Saturation
% 228.32/33.03 % (232366)Time elapsed: 1.196 s
% 228.32/33.03 % (232366)Peak memory usage: 139 MB
% 228.32/33.03 % (232366)Instructions burned: 2083 (million)
% 228.32/33.03 % (232368)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=1954013407:i=4629:av=off:gsp=on_2797 on theBenchmark for (2797ds/4629Mi)
% 228.32/33.03 % (232368)Refutation not found, incomplete strategy
% 228.32/33.03 % (232368)------------------------------
% 228.32/33.03 % (232368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 228.32/33.03 % (232368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.32/33.03 % (232368)CaDiCaL version: 2.1.3
% 228.32/33.03 % (232368)Termination reason: Refutation not found, incomplete strategy
% 228.32/33.03 % (232368)Time elapsed: 0.531 s
% 228.32/33.03 % (232368)Peak memory usage: 130 MB
% 228.32/33.03 % (232368)Instructions burned: 935 (million)
% 228.32/33.03 % (232368)------------------------------
% 228.32/33.03 % (232368)------------------------------
% 228.32/33.03 % (232370)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1194372575:i=1258:av=off_2787 on theBenchmark for (2787ds/1258Mi)
% 228.32/33.03 % (232370)Instruction limit reached!
% 228.32/33.03 % (232370)------------------------------
% 228.32/33.03 % (232370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 228.32/33.03 % (232370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.32/33.03 % (232370)CaDiCaL version: 2.1.3
% 228.32/33.03 % (232370)Termination reason: Instruction limit
% 228.32/33.03 % (232370)Termination phase: Saturation
% 228.32/33.03 % (232370)Time elapsed: 0.555 s
% 228.32/33.03 % (232370)Peak memory usage: 94 MB
% 228.32/33.03 % (232370)Instructions burned: 1258 (million)
% 266.76/38.34 % (232372)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=216966310:i=7343:av=off:ss=included_2780 on theBenchmark for (2780ds/7343Mi)
% 266.76/38.34 % (232364)Instruction limit reached!
% 266.76/38.34 % (232364)------------------------------
% 266.76/38.34 % (232364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 266.76/38.34 % (232364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 266.76/38.34 % (232364)CaDiCaL version: 2.1.3
% 266.76/38.34 % (232364)Termination reason: Instruction limit
% 266.76/38.34 % (232364)Termination phase: Saturation
% 266.76/38.34 % (232364)Time elapsed: 4.976 s
% 266.76/38.34 % (232364)Peak memory usage: 165 MB
% 266.76/38.34 % (232364)Instructions burned: 4920 (million)
% 266.76/38.34 % (232374)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1555926293:i=1325:sd=2:ss=axioms:sgt=16_2771 on theBenchmark for (2771ds/1325Mi)
% 266.76/38.34 % (232374)Instruction limit reached!
% 266.76/38.34 % (232374)------------------------------
% 266.76/38.34 % (232374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 266.76/38.34 % (232374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 266.76/38.34 % (232374)CaDiCaL version: 2.1.3
% 266.76/38.34 % (232374)Termination reason: Instruction limit
% 266.76/38.34 % (232374)Termination phase: Saturation
% 266.76/38.34 % (232374)Time elapsed: 1.208 s
% 266.76/38.34 % (232374)Peak memory usage: 100 MB
% 266.76/38.34 % (232374)Instructions burned: 1325 (million)
% 266.76/38.34 % (232376)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=3133311900:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2757 on theBenchmark for (2757ds/2646Mi)
% 266.76/38.34 % (232357)Instruction limit reached!
% 266.76/38.34 % (232357)------------------------------
% 266.76/38.34 % (232357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 266.76/38.34 % (232357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 266.76/38.34 % (232357)CaDiCaL version: 2.1.3
% 266.76/38.34 % (232357)Termination reason: Instruction limit
% 266.76/38.34 % (232357)Termination phase: Saturation
% 266.76/38.34 % (232357)Time elapsed: 9.912 s
% 266.76/38.34 % (232357)Peak memory usage: 203 MB
% 266.76/38.34 % (232357)Instructions burned: 9530 (million)
% 266.76/38.34 % (232372)Instruction limit reached!
% 266.76/38.34 % (232372)------------------------------
% 266.76/38.34 % (232372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 266.76/38.34 % (232372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 266.76/38.34 % (232372)CaDiCaL version: 2.1.3
% 266.76/38.34 % (232372)Termination reason: Instruction limit
% 266.76/38.34 % (232372)Termination phase: Saturation
% 266.76/38.34 % (232372)Time elapsed: 4.090 s
% 266.76/38.34 % (232372)Peak memory usage: 191 MB
% 266.76/38.34 % (232372)Instructions burned: 7344 (million)
% 266.76/38.34 % (232378)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1169375661:i=1489:sd=2:ep=R:ss=axioms_2739 on theBenchmark for (2739ds/1489Mi)
% 266.76/38.34 % (232379)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=756598054:i=1503_2737 on theBenchmark for (2737ds/1503Mi)
% 266.76/38.34 % (232379)Refutation not found, incomplete strategy
% 266.76/38.34 % (232379)------------------------------
% 266.76/38.34 % (232379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 266.76/38.34 % (232379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 266.76/38.34 % (232379)CaDiCaL version: 2.1.3
% 266.76/38.34 % (232379)Termination reason: Refutation not found, incomplete strategy
% 266.76/38.34 % (232379)Time elapsed: 0.528 s
% 266.76/38.34 % (232379)Peak memory usage: 129 MB
% 266.76/38.34 % (232379)Instructions burned: 885 (million)
% 266.76/38.34 % (232379)------------------------------
% 266.76/38.34 % (232379)------------------------------
% 266.76/38.34 % (232378)Refutation not found, incomplete strategy
% 266.76/38.34 % (232378)------------------------------
% 266.76/38.34 % (232378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 266.76/38.34 % (232378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 266.76/38.34 % (232378)CaDiCaL version: 2.1.3
% 266.76/38.34 % (232378)Termination reason: Refutation not found, incomplete strategy
% 266.76/38.34 % (232378)Time elapsed: 0.887 s
% 266.76/38.34 % (232378)Peak memory usage: 128 MB
% 153.58/39.63 % (232378)Instructions burned: 865 (million)
% 153.58/39.63 % (232376)Instruction limit reached!
% 153.58/39.63 % (232376)------------------------------
% 153.58/39.63 % (232376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.58/39.63 % (232376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.58/39.63 % (232376)CaDiCaL version: 2.1.3
% 153.58/39.63 % (232376)Termination reason: Instruction limit
% 153.58/39.63 % (232376)Termination phase: Saturation
% 153.58/39.63 % (232376)Time elapsed: 2.675 s
% 153.58/39.63 % (232376)Peak memory usage: 146 MB
% 153.58/39.63 % (232376)Instructions burned: 2647 (million)
% 153.58/39.63 % (232382)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3473453893:i=13942:kws=frequency_2728 on theBenchmark for (2728ds/13942Mi)
% 153.58/39.63 % (232383)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=3095702348:i=3604:fsr=off:er=filter_2728 on theBenchmark for (2728ds/3604Mi)
% 153.58/39.63 % (232378)------------------------------
% 153.58/39.63 % (232378)------------------------------
% 153.58/39.63 % (232386)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3247240192:i=1876:sd=1:ss=included:sgt=32_2724 on theBenchmark for (2724ds/1876Mi)
% 153.58/39.63 % (232386)Instruction limit reached!
% 153.58/39.63 % (232386)------------------------------
% 153.58/39.63 % (232386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.58/39.63 % (232386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.58/39.63 % (232386)CaDiCaL version: 2.1.3
% 153.58/39.63 % (232386)Termination reason: Instruction limit
% 153.58/39.63 % (232386)Termination phase: Saturation
% 153.58/39.63 % (232386)Time elapsed: 1.890 s
% 153.58/39.63 % (232386)Peak memory usage: 137 MB
% 153.58/39.63 % (232386)Instructions burned: 1877 (million)
% 153.58/39.63 % (232388)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=975957816:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2703 on theBenchmark for (2703ds/1932Mi)
% 153.58/39.63 % (232349)Instruction limit reached!
% 153.58/39.63 % (232349)------------------------------
% 153.58/39.63 % (232349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.58/39.63 % (232349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.58/39.63 % (232349)CaDiCaL version: 2.1.3
% 153.58/39.63 % (232349)Termination reason: Instruction limit
% 153.58/39.63 % (232349)Termination phase: Saturation
% 153.58/39.63 % (232349)Time elapsed: 16.863 s
% 153.58/39.63 % (232349)Peak memory usage: 294 MB
% 153.58/39.63 % (232349)Instructions burned: 16411 (million)
% 153.58/39.63 % (232390)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=645081242:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2696 on theBenchmark for (2696ds/1980Mi)
% 153.58/39.63 % (232383)Instruction limit reached!
% 153.58/39.63 % (232383)------------------------------
% 153.58/39.63 % (232383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.58/39.63 % (232383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.58/39.63 % (232383)CaDiCaL version: 2.1.3
% 153.58/39.63 % (232383)Termination reason: Instruction limit
% 153.58/39.63 % (232383)Termination phase: Saturation
% 153.58/39.63 % (232383)Time elapsed: 3.594 s
% 153.58/39.63 % (232383)Peak memory usage: 151 MB
% 153.58/39.63 % (232383)Instructions burned: 3604 (million)
% 153.58/39.63 % (232392)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=3536585934:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2689 on theBenchmark for (2689ds/3902Mi)
% 153.58/39.63 % (232388)Instruction limit reached!
% 153.58/39.63 % (232388)------------------------------
% 153.58/39.63 % (232388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.58/39.63 % (232388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.58/39.63 % (232388)CaDiCaL version: 2.1.3
% 153.58/39.63 % (232388)Termination reason: Instruction limit
% 153.58/39.63 % (232388)Termination phase: Saturation
% 153.58/39.63 % (232388)Time elapsed: 2.068 s
% 153.58/39.63 % (232388)Peak memory usage: 136 MB
% 153.58/39.63 % (232388)Instructions burned: 1933 (million)
% 153.58/39.63 % (232394)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2053621894:avsq=on:i=3916:aac=none:amm=off_2680 on theBenchmark for (2680ds/3916Mi)
% 153.58/39.63 % (232390)Instruction limit reached!
% 153.58/39.63 % (232390)------------------------------
% 153.58/39.63 % (232390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.58/39.63 % (232390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.58/39.63 % (232390)CaDiCaL version: 2.1.3
% 153.58/39.63 % (232390)Termination reason: Instruction limit
% 153.58/39.63 % (232390)Termination phase: Saturation
% 153.58/39.63 % (232390)Time elapsed: 2.111 s
% 153.58/39.63 % (232390)Peak memory usage: 138 MB
% 153.58/39.63 % (232390)Instructions burned: 1980 (million)
% 153.58/39.63 % (232396)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=99838788:cond=on:i=3940:av=off:er=known_2672 on theBenchmark for (2672ds/3940Mi)
% 153.58/39.63 % (232382)Instruction limit reached!
% 153.58/39.63 % (232382)------------------------------
% 153.58/39.63 % (232382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.58/39.63 % (232382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.58/39.63 % (232382)CaDiCaL version: 2.1.3
% 153.58/39.63 % (232382)Termination reason: Instruction limit
% 153.58/39.63 % (232382)Termination phase: Saturation
% 153.58/39.63 % (232382)Time elapsed: 7.736 s
% 153.58/39.63 % (232382)Peak memory usage: 258 MB
% 153.58/39.63 % (232382)Instructions burned: 13942 (million)
% 153.58/39.63 % (232398)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2373037063:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2649 on theBenchmark for (2649ds/3980Mi)
% 153.58/39.63 % (232392)Instruction limit reached!
% 153.58/39.63 % (232392)------------------------------
% 153.58/39.63 % (232392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.58/39.63 % (232392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.58/39.63 % (232392)CaDiCaL version: 2.1.3
% 153.58/39.63 % (232392)Termination reason: Instruction limit
% 153.58/39.63 % (232392)Termination phase: Saturation
% 153.58/39.63 % (232392)Time elapsed: 4.058 s
% 153.58/39.63 % (232392)Peak memory usage: 154 MB
% 153.58/39.63 % (232392)Instructions burned: 3902 (million)
% 153.58/39.63 % (232394)Instruction limit reached!
% 153.58/39.63 % (232394)------------------------------
% 153.58/39.63 % (232394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.58/39.63 % (232394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.58/39.63 % (232394)CaDiCaL version: 2.1.3
% 153.58/39.63 % (232394)Termination reason: Instruction limit
% 153.58/39.63 % (232394)Termination phase: Saturation
% 153.58/39.63 % (232394)Time elapsed: 3.283 s
% 153.58/39.63 % (232394)Peak memory usage: 115 MB
% 153.58/39.63 % (232394)Instructions burned: 3916 (million)
% 153.58/39.63 % (232400)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=2161415338:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2646 on theBenchmark for (2646ds/2087Mi)
% 153.58/39.63 % (232401)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1464933190:cts=off:cond=on:i=4272:bs=on:fsd=on_2645 on theBenchmark for (2645ds/4272Mi)
% 153.58/39.63 % (232396)Instruction limit reached!
% 153.58/39.63 % (232396)------------------------------
% 153.58/39.63 % (232396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.58/39.63 % (232396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.58/39.63 % (232396)CaDiCaL version: 2.1.3
% 153.58/39.63 % (232396)Termination reason: Instruction limit
% 153.58/39.63 % (232396)Termination phase: Saturation
% 153.58/39.63 % (232396)Time elapsed: 4.197 s
% 153.58/39.63 % (232396)Peak memory usage: 155 MB
% 153.58/39.63 % (232396)Instructions burned: 3941 (million)
% 153.58/39.63 % (232404)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3743251763:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2628 on theBenchmark for (2628ds/2197Mi)
% 153.58/39.63 % (232398)Instruction limit reached!
% 153.58/39.63 % (232398)------------------------------
% 153.58/39.63 % (232398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.58/39.63 % (232398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.58/39.63 % (232398)CaDiCaL version: 2.1.3
% 153.58/39.63 % (232398)Termination reason: Instruction limit
% 153.58/39.63 % (232398)Termination phase: Saturation
% 153.58/39.63 % (232398)Time elapsed: 2.268 s
% 153.58/39.63 % (232398)Peak memory usage: 159 MB
% 153.58/39.63 % (232398)Instructions burned: 3980 (million)
% 153.58/39.63 % (232408)dis+21_1_sil=8000:spb=goal_then_units:random_seed=848117182:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2624 on theBenchmark for (2624ds/6508Mi)
% 153.58/39.63 % (232400)Instruction limit reached!
% 153.58/39.63 % (232400)------------------------------
% 153.58/39.63 % (232400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.58/39.63 % (232400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.58/39.63 % (232400)CaDiCaL version: 2.1.3
% 153.58/39.63 % (232400)Termination reason: Instruction limit
% 153.58/39.63 % (232400)Termination phase: Saturation
% 153.58/39.63 % (232400)Time elapsed: 2.240 s
% 153.58/39.63 % (232400)Peak memory usage: 141 MB
% 153.58/39.63 % (232400)Instructions burned: 2087 (million)
% 153.58/39.63 % (232410)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=1270621815:i=2330:fgj=on:av=off:fsr=off_2622 on theBenchmark for (2622ds/2330Mi)
% 153.58/39.63 % (232408)First to succeed.
% 153.58/39.63 % (232408)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-232222"
% 153.58/39.63 % (232408)Refutation found. Thanks to Tanya!
% 153.58/39.63 % SZS status Unsatisfiable for theBenchmark
% 153.58/39.63 % SZS output start Proof for theBenchmark
% See solution above
% 275.93/39.83 % (232408)------------------------------
% 275.93/39.83 % (232408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 275.93/39.83 % (232408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 275.93/39.83 % (232408)CaDiCaL version: 2.1.3
% 275.93/39.83 % (232408)Termination reason: Refutation
% 275.93/39.83 % (232408)Time elapsed: 0.739 s
% 275.93/39.83 % (232408)Peak memory usage: 108 MB
% 275.93/39.83 % (232408)Instructions burned: 1398 (million)
% 275.93/39.83 % (232408)------------------------------
% 275.93/39.83 % (232408)------------------------------
% 275.93/39.83 % (232222)Success in time 38.798 s
% 275.93/39.83 % Vampire exiting
%------------------------------------------------------------------------------