%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO466+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:52:43 AM UTC 2026
% Result : Theorem 34.12s 12.87s
% Output : Refutation 78.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 3
% Syntax : Number of formulae : 18 ( 7 unt; 0 def)
% Number of atoms : 43 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 45 ( 20 ~; 12 |; 10 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 36 ( 28 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3304,axiom,
! [X0,X1,X2,X3] :
( ( p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),subspace),s(fun(cart(real,X0),bool),X3))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X1))),s(fun(cart(real,X0),bool),X3))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X2))),s(fun(cart(real,X0),bool),X3)))) )
=> p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X1))),s(cart(real,X0),X2))))),s(fun(cart(real,X0),bool),X3)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSUBSPACEu_SUB) ).
fof(f3315,axiom,
! [X0,X1] : p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),subspace),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X1)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSUBSPACEu_SPAN) ).
fof(f3338,conjecture,
! [X0,X1,X2,X3] :
( ( p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X2))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3)))))) )
=> p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X1))),s(cart(real,X0),X2))))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3)))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSPANu_SUB) ).
fof(f3339,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( ( p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X2))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3)))))) )
=> p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X1))),s(cart(real,X0),X2))))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3)))))) ),
inference(negated_conjecture,[status(cth)],[f3338]) ).
fof(f4312,plain,
! [X0,X1,X2,X3] :
( p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X1))),s(cart(real,X0),X2))))),s(fun(cart(real,X0),bool),X3))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),subspace),s(fun(cart(real,X0),bool),X3))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X1))),s(fun(cart(real,X0),bool),X3))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X2))),s(fun(cart(real,X0),bool),X3)))) ),
inference(ennf_transformation,[],[f3304]) ).
fof(f4313,plain,
! [X0,X1,X2,X3] :
( p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X1))),s(cart(real,X0),X2))))),s(fun(cart(real,X0),bool),X3))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),subspace),s(fun(cart(real,X0),bool),X3))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X1))),s(fun(cart(real,X0),bool),X3))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X2))),s(fun(cart(real,X0),bool),X3)))) ),
inference(flattening,[],[f4312]) ).
fof(f4349,plain,
? [X0,X1,X2,X3] :
( ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X1))),s(cart(real,X0),X2))))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X2))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3)))))) ),
inference(ennf_transformation,[],[f3339]) ).
fof(f4350,plain,
? [X0,X1,X2,X3] :
( ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X1))),s(cart(real,X0),X2))))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X1))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X2))),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X3)))))) ),
inference(flattening,[],[f4349]) ).
fof(f6865,plain,
( ~ p(s(bool,i(s(fun(fun(cart(real,sK719),bool),bool),i(s(fun(cart(real,sK719),fun(fun(cart(real,sK719),bool),bool)),in),s(cart(real,sK719),i(s(fun(cart(real,sK719),cart(real,sK719)),i(s(fun(cart(real,sK719),fun(cart(real,sK719),cart(real,sK719))),vectoru_sub),s(cart(real,sK719),sK720))),s(cart(real,sK719),sK721))))),s(fun(cart(real,sK719),bool),i(s(fun(fun(cart(real,sK719),bool),fun(cart(real,sK719),bool)),span),s(fun(cart(real,sK719),bool),sK722))))))
& p(s(bool,i(s(fun(fun(cart(real,sK719),bool),bool),i(s(fun(cart(real,sK719),fun(fun(cart(real,sK719),bool),bool)),in),s(cart(real,sK719),sK720))),s(fun(cart(real,sK719),bool),i(s(fun(fun(cart(real,sK719),bool),fun(cart(real,sK719),bool)),span),s(fun(cart(real,sK719),bool),sK722))))))
& p(s(bool,i(s(fun(fun(cart(real,sK719),bool),bool),i(s(fun(cart(real,sK719),fun(fun(cart(real,sK719),bool),bool)),in),s(cart(real,sK719),sK721))),s(fun(cart(real,sK719),bool),i(s(fun(fun(cart(real,sK719),bool),fun(cart(real,sK719),bool)),span),s(fun(cart(real,sK719),bool),sK722)))))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK719,sK720,sK721,sK722]),skolemize(X0,sK719),skolemize(X1,sK720),skolemize(X2,sK721),skolemize(X3,sK722)],[f4350]) ).
fof(f10747,plain,
! [X2,X3,X0,X1] :
( p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X1))),s(cart(real,X0),X2))))),s(fun(cart(real,X0),bool),X3))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),subspace),s(fun(cart(real,X0),bool),X3))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X1))),s(fun(cart(real,X0),bool),X3))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),bool)),in),s(cart(real,X0),X2))),s(fun(cart(real,X0),bool),X3)))) ),
inference(cnf_transformation,[],[f4313]) ).
fof(f10767,plain,
! [X0,X1] : p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),subspace),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X1)))))),
inference(cnf_transformation,[],[f3315]) ).
fof(f10793,plain,
p(s(bool,i(s(fun(fun(cart(real,sK719),bool),bool),i(s(fun(cart(real,sK719),fun(fun(cart(real,sK719),bool),bool)),in),s(cart(real,sK719),sK721))),s(fun(cart(real,sK719),bool),i(s(fun(fun(cart(real,sK719),bool),fun(cart(real,sK719),bool)),span),s(fun(cart(real,sK719),bool),sK722)))))),
inference(cnf_transformation,[],[f6865]) ).
fof(f10794,plain,
p(s(bool,i(s(fun(fun(cart(real,sK719),bool),bool),i(s(fun(cart(real,sK719),fun(fun(cart(real,sK719),bool),bool)),in),s(cart(real,sK719),sK720))),s(fun(cart(real,sK719),bool),i(s(fun(fun(cart(real,sK719),bool),fun(cart(real,sK719),bool)),span),s(fun(cart(real,sK719),bool),sK722)))))),
inference(cnf_transformation,[],[f6865]) ).
fof(f10795,plain,
~ p(s(bool,i(s(fun(fun(cart(real,sK719),bool),bool),i(s(fun(cart(real,sK719),fun(fun(cart(real,sK719),bool),bool)),in),s(cart(real,sK719),i(s(fun(cart(real,sK719),cart(real,sK719)),i(s(fun(cart(real,sK719),fun(cart(real,sK719),cart(real,sK719))),vectoru_sub),s(cart(real,sK719),sK720))),s(cart(real,sK719),sK721))))),s(fun(cart(real,sK719),bool),i(s(fun(fun(cart(real,sK719),bool),fun(cart(real,sK719),bool)),span),s(fun(cart(real,sK719),bool),sK722)))))),
inference(cnf_transformation,[],[f6865]) ).
fof(f18740,plain,
( ~ p(s(bool,i(s(fun(fun(cart(real,sK719),bool),bool),subspace),s(fun(cart(real,sK719),bool),i(s(fun(fun(cart(real,sK719),bool),fun(cart(real,sK719),bool)),span),s(fun(cart(real,sK719),bool),sK722))))))
| ~ p(s(bool,i(s(fun(fun(cart(real,sK719),bool),bool),i(s(fun(cart(real,sK719),fun(fun(cart(real,sK719),bool),bool)),in),s(cart(real,sK719),sK720))),s(fun(cart(real,sK719),bool),i(s(fun(fun(cart(real,sK719),bool),fun(cart(real,sK719),bool)),span),s(fun(cart(real,sK719),bool),sK722))))))
| ~ p(s(bool,i(s(fun(fun(cart(real,sK719),bool),bool),i(s(fun(cart(real,sK719),fun(fun(cart(real,sK719),bool),bool)),in),s(cart(real,sK719),sK721))),s(fun(cart(real,sK719),bool),i(s(fun(fun(cart(real,sK719),bool),fun(cart(real,sK719),bool)),span),s(fun(cart(real,sK719),bool),sK722)))))) ),
inference(resolution,[],[f10795,f10747]) ).
fof(f19256,plain,
( ~ p(s(bool,i(s(fun(fun(cart(real,sK719),bool),bool),i(s(fun(cart(real,sK719),fun(fun(cart(real,sK719),bool),bool)),in),s(cart(real,sK719),sK720))),s(fun(cart(real,sK719),bool),i(s(fun(fun(cart(real,sK719),bool),fun(cart(real,sK719),bool)),span),s(fun(cart(real,sK719),bool),sK722))))))
| ~ p(s(bool,i(s(fun(fun(cart(real,sK719),bool),bool),i(s(fun(cart(real,sK719),fun(fun(cart(real,sK719),bool),bool)),in),s(cart(real,sK719),sK721))),s(fun(cart(real,sK719),bool),i(s(fun(fun(cart(real,sK719),bool),fun(cart(real,sK719),bool)),span),s(fun(cart(real,sK719),bool),sK722)))))) ),
inference(forward_subsumption_resolution,[],[f18740,f10767]) ).
fof(f19257,plain,
~ p(s(bool,i(s(fun(fun(cart(real,sK719),bool),bool),i(s(fun(cart(real,sK719),fun(fun(cart(real,sK719),bool),bool)),in),s(cart(real,sK719),sK721))),s(fun(cart(real,sK719),bool),i(s(fun(fun(cart(real,sK719),bool),fun(cart(real,sK719),bool)),span),s(fun(cart(real,sK719),bool),sK722)))))),
inference(forward_subsumption_resolution,[],[f19256,f10794]) ).
fof(f19258,plain,
$false,
inference(forward_subsumption_resolution,[],[f19257,f10793]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO466+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 08:17:10 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 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
% 16.80/4.05 % (194101)Detected formulas, will run a generic FOF schedule.
% 16.80/4.05 % (194226)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3123405771:s2a=on:i=139:gtg=position_2989 on theBenchmark for (2989ds/139Mi)
% 16.80/4.05 % (194226)Instruction limit reached!
% 16.80/4.05 % (194226)------------------------------
% 16.80/4.05 % (194226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.80/4.05 % (194226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/4.05 % (194226)CaDiCaL version: 2.1.3
% 16.80/4.05 % (194226)Termination reason: Instruction limit
% 16.80/4.05 % (194226)Termination phase: Property scanning
% 16.80/4.05 % (194226)Time elapsed: 0.026 s
% 16.80/4.05 % (194226)Peak memory usage: 90 MB
% 16.80/4.05 % (194226)Instructions burned: 140 (million)
% 16.80/4.05 % (194222)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=701660606:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2989 on theBenchmark for (2989ds/134677Mi)
% 16.80/4.05 % (194225)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=453254747:i=119:av=off:ss=axioms_2989 on theBenchmark for (2989ds/119Mi)
% 16.80/4.05 % (194221)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=1234818552:i=141193_2989 on theBenchmark for (2989ds/141193Mi)
% 16.80/4.05 % (194223)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=443988128:i=141695:sd=1:nm=32:gsp=on:ss=included_2989 on theBenchmark for (2989ds/141695Mi)
% 16.80/4.05 % (194227)dis-21_1_sil=8000:lcm=predicate:random_seed=3358935669:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2989 on theBenchmark for (2989ds/129Mi)
% 16.80/4.05 % (194224)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2366194314:i=109:sd=1:ins=1:gsp=on:ss=axioms_2989 on theBenchmark for (2989ds/109Mi)
% 16.80/4.05 % (194225)Instruction limit reached!
% 16.80/4.05 % (194225)------------------------------
% 16.80/4.05 % (194225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.80/4.05 % (194225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/4.05 % (194225)CaDiCaL version: 2.1.3
% 16.80/4.05 % (194225)Termination reason: Instruction limit
% 16.80/4.05 % (194225)Termination phase: Preprocessing 1
% 16.80/4.05 % (194225)Time elapsed: 0.063 s
% 16.80/4.05 % (194225)Peak memory usage: 91 MB
% 16.80/4.05 % (194225)Instructions burned: 119 (million)
% 16.80/4.05 % (194227)Instruction limit reached!
% 16.80/4.05 % (194227)------------------------------
% 16.80/4.05 % (194227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.80/4.05 % (194227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/4.05 % (194227)CaDiCaL version: 2.1.3
% 16.80/4.05 % (194227)Termination reason: Instruction limit
% 16.80/4.05 % (194227)Termination phase: SInE selection
% 16.80/4.05 % (194227)Time elapsed: 0.062 s
% 16.80/4.05 % (194227)Peak memory usage: 90 MB
% 16.80/4.05 % (194227)Instructions burned: 131 (million)
% 16.80/4.05 % (194224)Instruction limit reached!
% 16.80/4.05 % (194224)------------------------------
% 16.80/4.05 % (194224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.80/4.05 % (194224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/4.05 % (194224)CaDiCaL version: 2.1.3
% 16.80/4.05 % (194224)Termination reason: Instruction limit
% 16.80/4.05 % (194224)Termination phase: General splitting
% 16.80/4.05 % (194224)Time elapsed: 0.068 s
% 16.80/4.05 % (194224)Peak memory usage: 92 MB
% 16.80/4.05 % (194224)Instructions burned: 111 (million)
% 16.80/4.05 % (194233)lrs+10_1_sil=8000:sp=occurrence:random_seed=3452867859:i=285:sd=3:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/285Mi)
% 16.80/4.05 % (194236)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4254175962:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/157Mi)
% 16.80/4.05 % (194233)Instruction limit reached!
% 16.80/4.05 % (194233)------------------------------
% 16.80/4.05 % (194233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.80/4.05 % (194233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.80/4.05 % (194233)CaDiCaL version: 2.1.3
% 16.80/4.05 % (194233)Termination reason: Instruction limit
% 16.80/4.05 % (194233)Termination phase: Property scanning
% 26.24/5.42 % (194233)Time elapsed: 0.080 s
% 26.24/5.42 % (194233)Peak memory usage: 96 MB
% 26.24/5.42 % (194233)Instructions burned: 285 (million)
% 26.24/5.42 % (194237)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1366185227:i=325:sd=1:ss=axioms:sgt=32_2987 on theBenchmark for (2987ds/325Mi)
% 26.24/5.42 % (194238)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=2706147610:s2a=on:i=248:s2at=1.23:gtg=position_2987 on theBenchmark for (2987ds/248Mi)
% 26.24/5.42 % (194236)Instruction limit reached!
% 26.24/5.42 % (194236)------------------------------
% 26.24/5.42 % (194236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.24/5.42 % (194236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.24/5.42 % (194236)CaDiCaL version: 2.1.3
% 26.24/5.42 % (194236)Termination reason: Instruction limit
% 26.24/5.42 % (194236)Termination phase: Property scanning
% 26.24/5.42 % (194236)Time elapsed: 0.057 s
% 26.24/5.42 % (194236)Peak memory usage: 90 MB
% 26.24/5.42 % (194236)Instructions burned: 160 (million)
% 26.24/5.42 % (194241)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1300961726:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2986 on theBenchmark for (2986ds/294Mi)
% 26.24/5.42 % (194238)Instruction limit reached!
% 26.24/5.42 % (194238)------------------------------
% 26.24/5.42 % (194238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.24/5.42 % (194238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.24/5.42 % (194238)CaDiCaL version: 2.1.3
% 26.24/5.42 % (194238)Termination reason: Instruction limit
% 26.24/5.42 % (194238)Termination phase: Property scanning
% 26.24/5.42 % (194238)Time elapsed: 0.089 s
% 26.24/5.42 % (194238)Peak memory usage: 90 MB
% 26.24/5.42 % (194238)Instructions burned: 248 (million)
% 26.24/5.42 % (194237)Instruction limit reached!
% 26.24/5.42 % (194237)------------------------------
% 26.24/5.42 % (194237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.24/5.42 % (194237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.24/5.42 % (194237)CaDiCaL version: 2.1.3
% 26.24/5.42 % (194237)Termination reason: Instruction limit
% 26.24/5.42 % (194237)Termination phase: Saturation
% 26.24/5.42 % (194237)Time elapsed: 0.168 s
% 26.24/5.42 % (194237)Peak memory usage: 97 MB
% 26.24/5.42 % (194237)Instructions burned: 326 (million)
% 26.24/5.42 % (194241)Instruction limit reached!
% 26.24/5.42 % (194241)------------------------------
% 26.24/5.42 % (194241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.24/5.42 % (194241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.24/5.42 % (194241)CaDiCaL version: 2.1.3
% 26.24/5.42 % (194241)Termination reason: Instruction limit
% 26.24/5.42 % (194241)Termination phase: Preprocessing 3
% 26.24/5.42 % (194241)Time elapsed: 0.080 s
% 26.24/5.42 % (194241)Peak memory usage: 95 MB
% 26.24/5.42 % (194241)Instructions burned: 297 (million)
% 26.24/5.42 % (194244)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=575446784:i=2350_2985 on theBenchmark for (2985ds/2350Mi)
% 26.24/5.42 % (194246)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=818045096:cts=off:i=113:fsr=off:ss=included:sgt=4_2985 on theBenchmark for (2985ds/113Mi)
% 26.24/5.42 % (194248)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2915839718:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 26.24/5.42 % (194246)Instruction limit reached!
% 26.24/5.42 % (194246)------------------------------
% 26.24/5.42 % (194246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.24/5.42 % (194246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.24/5.42 % (194246)CaDiCaL version: 2.1.3
% 26.24/5.42 % (194246)Termination reason: Instruction limit
% 26.24/5.42 % (194246)Termination phase: Preprocessing 1
% 26.24/5.42 % (194246)Time elapsed: 0.071 s
% 26.24/5.42 % (194246)Peak memory usage: 90 MB
% 26.24/5.42 % (194246)Instructions burned: 113 (million)
% 26.24/5.42 % (194248)Instruction limit reached!
% 26.24/5.42 % (194248)------------------------------
% 26.24/5.42 % (194248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.24/5.42 % (194248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.24/5.42 % (194248)CaDiCaL version: 2.1.3
% 26.24/5.42 % (194248)Termination reason: Instruction limit
% 26.24/5.42 % (194248)Termination phase: Property scanning
% 26.24/5.42 % (194248)Time elapsed: 0.037 s
% 77.70/12.72 % (194248)Peak memory usage: 90 MB
% 77.70/12.72 % (194248)Instructions burned: 116 (million)
% 77.70/12.72 % (194247)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=608894746:i=127:av=off:fsr=off:sup=off_2984 on theBenchmark for (2984ds/127Mi)
% 77.70/12.72 % (194247)Instruction limit reached!
% 77.70/12.72 % (194247)------------------------------
% 77.70/12.72 % (194247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.70/12.72 % (194247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.70/12.72 % (194247)CaDiCaL version: 2.1.3
% 77.70/12.72 % (194247)Termination reason: Instruction limit
% 77.70/12.72 % (194247)Termination phase: Naming
% 77.70/12.72 % (194247)Time elapsed: 0.111 s
% 77.70/12.72 % (194247)Peak memory usage: 93 MB
% 77.70/12.72 % (194247)Instructions burned: 128 (million)
% 77.70/12.72 % (194259)lrs+10_1_sil=8000:sp=occurrence:random_seed=3039901188:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2982 on theBenchmark for (2982ds/907Mi)
% 77.70/12.72 % (194260)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3061320062:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 77.70/12.72 % (194271)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3779716287:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi)
% 77.70/12.72 % (194260)Instruction limit reached!
% 77.70/12.72 % (194260)------------------------------
% 77.70/12.72 % (194260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.70/12.72 % (194260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.70/12.72 % (194260)CaDiCaL version: 2.1.3
% 77.70/12.72 % (194260)Termination reason: Instruction limit
% 77.70/12.72 % (194260)Termination phase: Property scanning
% 77.70/12.72 % (194260)Time elapsed: 0.198 s
% 77.70/12.72 % (194260)Peak memory usage: 99 MB
% 77.70/12.72 % (194260)Instructions burned: 439 (million)
% 77.70/12.72 % (194281)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=388207843:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 77.70/12.72 % (194281)Instruction limit reached!
% 77.70/12.72 % (194281)------------------------------
% 77.70/12.72 % (194281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.70/12.72 % (194281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.70/12.72 % (194281)CaDiCaL version: 2.1.3
% 77.70/12.72 % (194281)Termination reason: Instruction limit
% 77.70/12.72 % (194281)Termination phase: Preprocessing 1
% 77.70/12.72 % (194281)Time elapsed: 0.062 s
% 77.70/12.72 % (194281)Peak memory usage: 91 MB
% 77.70/12.72 % (194281)Instructions burned: 135 (million)
% 77.70/12.72 % (194259)Instruction limit reached!
% 77.70/12.72 % (194259)------------------------------
% 77.70/12.72 % (194259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.70/12.72 % (194259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.70/12.72 % (194259)CaDiCaL version: 2.1.3
% 77.70/12.72 % (194259)Termination reason: Instruction limit
% 77.70/12.72 % (194259)Termination phase: Property scanning
% 77.70/12.72 % (194259)Time elapsed: 0.698 s
% 77.70/12.72 % (194259)Peak memory usage: 99 MB
% 77.70/12.72 % (194259)Instructions burned: 907 (million)
% 77.70/12.72 % (194288)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1670284530:st=8:i=592:sd=3:ep=RST:ss=axioms_2975 on theBenchmark for (2975ds/592Mi)
% 77.70/12.72 % (194292)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=591468094:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 77.70/12.72 % (194288)Instruction limit reached!
% 77.70/12.72 % (194288)------------------------------
% 77.70/12.72 % (194288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.70/12.72 % (194288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.70/12.72 % (194288)CaDiCaL version: 2.1.3
% 77.70/12.72 % (194288)Termination reason: Instruction limit
% 77.70/12.72 % (194288)Termination phase: Preprocessing 3
% 77.70/12.72 % (194288)Time elapsed: 0.262 s
% 77.70/12.72 % (194288)Peak memory usage: 102 MB
% 77.70/12.72 % (194288)Instructions burned: 593 (million)
% 77.70/12.72 % (194300)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=947947998:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/125Mi)
% 77.70/12.72 % (194300)Instruction limit reached!
% 77.70/12.72 % (194300)------------------------------
% 34.12/12.87 % (194300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.12/12.87 % (194300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.12/12.87 % (194300)CaDiCaL version: 2.1.3
% 34.12/12.87 % (194300)Termination reason: Instruction limit
% 34.12/12.87 % (194300)Termination phase: Property scanning
% 34.12/12.87 % (194300)Time elapsed: 0.049 s
% 34.12/12.87 % (194300)Peak memory usage: 90 MB
% 34.12/12.87 % (194300)Instructions burned: 128 (million)
% 34.12/12.87 % (194244)Instruction limit reached!
% 34.12/12.87 % (194244)------------------------------
% 34.12/12.87 % (194244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.12/12.87 % (194244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.12/12.87 % (194244)CaDiCaL version: 2.1.3
% 34.12/12.87 % (194244)Termination reason: Instruction limit
% 34.12/12.87 % (194244)Termination phase: Twee Goal Transformation
% 34.12/12.87 % (194244)Time elapsed: 1.695 s
% 34.12/12.87 % (194244)Peak memory usage: 105 MB
% 34.12/12.87 % (194244)Instructions burned: 2351 (million)
% 34.12/12.87 % (194305)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3710439902:i=134:gtgl=5:slsql=off:gtg=exists_sym_2967 on theBenchmark for (2967ds/134Mi)
% 34.12/12.87 % (194305)Instruction limit reached!
% 34.12/12.87 % (194305)------------------------------
% 34.12/12.87 % (194305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.12/12.87 % (194305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.12/12.87 % (194305)CaDiCaL version: 2.1.3
% 34.12/12.87 % (194305)Termination reason: Instruction limit
% 34.12/12.87 % (194305)Termination phase: Property scanning
% 34.12/12.87 % (194305)Time elapsed: 0.052 s
% 34.12/12.87 % (194305)Peak memory usage: 90 MB
% 34.12/12.87 % (194305)Instructions burned: 136 (million)
% 34.12/12.87 % (194306)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4115596718:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/141Mi)
% 34.12/12.87 % (194306)Instruction limit reached!
% 34.12/12.87 % (194306)------------------------------
% 34.12/12.87 % (194306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.12/12.87 % (194306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.12/12.87 % (194306)CaDiCaL version: 2.1.3
% 34.12/12.87 % (194306)Termination reason: Instruction limit
% 34.12/12.87 % (194306)Termination phase: Saturation
% 34.12/12.87 % (194306)Time elapsed: 0.118 s
% 34.12/12.87 % (194306)Peak memory usage: 94 MB
% 34.12/12.87 % (194306)Instructions burned: 141 (million)
% 34.12/12.87 % (194310)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=100549532:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2965 on theBenchmark for (2965ds/431Mi)
% 34.12/12.87 % (194314)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=1445043963:i=6060:aac=none:ins=25_2963 on theBenchmark for (2963ds/6060Mi)
% 34.12/12.87 % (194310)Instruction limit reached!
% 34.12/12.87 % (194310)------------------------------
% 34.12/12.87 % (194310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.12/12.87 % (194310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.12/12.87 % (194310)CaDiCaL version: 2.1.3
% 34.12/12.87 % (194310)Termination reason: Instruction limit
% 34.12/12.87 % (194310)Termination phase: Saturation
% 34.12/12.87 % (194310)Time elapsed: 0.193 s
% 34.12/12.87 % (194310)Peak memory usage: 96 MB
% 34.12/12.87 % (194310)Instructions burned: 432 (million)
% 34.12/12.87 % (194318)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=452171351:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2960 on theBenchmark for (2960ds/150Mi)
% 34.12/12.87 % (194318)Instruction limit reached!
% 34.12/12.87 % (194318)------------------------------
% 34.12/12.87 % (194318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.12/12.87 % (194318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.12/12.87 % (194318)CaDiCaL version: 2.1.3
% 34.12/12.87 % (194318)Termination reason: Instruction limit
% 34.12/12.87 % (194318)Termination phase: Preprocessing 1
% 34.12/12.87 % (194318)Time elapsed: 0.079 s
% 34.12/12.87 % (194318)Peak memory usage: 91 MB
% 34.12/12.87 % (194318)Instructions burned: 151 (million)
% 34.12/12.87 % (194323)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2910413842:i=14155:bd=all_2957 on theBenchmark for (2957ds/14155Mi)
% 34.12/12.87 % (194271)Instruction limit reached!
% 34.12/12.87 % (194271)------------------------------
% 34.12/12.87 % (194271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.12/12.87 % (194271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.12/12.87 % (194271)CaDiCaL version: 2.1.3
% 34.12/12.87 % (194271)Termination reason: Instruction limit
% 34.12/12.87 % (194271)Termination phase: Saturation
% 34.12/12.87 % (194271)Time elapsed: 4.882 s
% 34.12/12.87 % (194271)Peak memory usage: 223 MB
% 34.12/12.87 % (194271)Instructions burned: 5202 (million)
% 34.12/12.87 % (194337)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1479959059:i=667:av=off:fsr=off_2929 on theBenchmark for (2929ds/667Mi)
% 34.12/12.87 % (194337)Instruction limit reached!
% 34.12/12.87 % (194337)------------------------------
% 34.12/12.87 % (194337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.12/12.87 % (194337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.12/12.87 % (194337)CaDiCaL version: 2.1.3
% 34.12/12.87 % (194337)Termination reason: Instruction limit
% 34.12/12.87 % (194337)Termination phase: Property scanning
% 34.12/12.87 % (194337)Time elapsed: 0.555 s
% 34.12/12.87 % (194337)Peak memory usage: 102 MB
% 34.12/12.87 % (194337)Instructions burned: 667 (million)
% 34.12/12.87 % (194339)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=294394309:s2a=on:i=185:s2at=1.8:fdi=4_2920 on theBenchmark for (2920ds/185Mi)
% 34.12/12.87 % (194339)Instruction limit reached!
% 34.12/12.87 % (194339)------------------------------
% 34.12/12.87 % (194339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.12/12.87 % (194339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.12/12.87 % (194339)CaDiCaL version: 2.1.3
% 34.12/12.87 % (194339)Termination reason: Instruction limit
% 34.12/12.87 % (194339)Termination phase: Preprocessing 1
% 34.12/12.87 % (194339)Time elapsed: 0.144 s
% 34.12/12.87 % (194339)Peak memory usage: 91 MB
% 34.12/12.87 % (194339)Instructions burned: 188 (million)
% 34.12/12.87 % (194342)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4065967550:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2916 on theBenchmark for (2916ds/193Mi)
% 34.12/12.87 % (194342)Instruction limit reached!
% 34.12/12.87 % (194342)------------------------------
% 34.12/12.87 % (194342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.12/12.87 % (194342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.12/12.87 % (194342)CaDiCaL version: 2.1.3
% 34.12/12.87 % (194342)Termination reason: Instruction limit
% 34.12/12.87 % (194342)Termination phase: Preprocessing 1
% 34.12/12.87 % (194342)Time elapsed: 0.165 s
% 34.12/12.87 % (194342)Peak memory usage: 90 MB
% 34.12/12.87 % (194342)Instructions burned: 193 (million)
% 34.12/12.87 % (194345)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3815160799:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2912 on theBenchmark for (2912ds/4850Mi)
% 34.12/12.87 % (194314)Instruction limit reached!
% 34.12/12.87 % (194314)------------------------------
% 34.12/12.87 % (194314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.12/12.87 % (194314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.12/12.87 % (194314)CaDiCaL version: 2.1.3
% 34.12/12.87 % (194314)Termination reason: Instruction limit
% 34.12/12.87 % (194314)Termination phase: Saturation
% 34.12/12.87 % (194314)Time elapsed: 6.404 s
% 34.12/12.87 % (194314)Peak memory usage: 426 MB
% 34.12/12.87 % (194314)Instructions burned: 6060 (million)
% 34.12/12.87 % (194353)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=97360073:i=12111:sd=1:ss=included_2896 on theBenchmark for (2896ds/12111Mi)
% 34.12/12.87 % (194345)First to succeed.
% 34.12/12.87 % (194345)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-194101"
% 34.12/12.87 % (194323)Instruction limit reached!
% 34.12/12.87 % (194323)------------------------------
% 34.12/12.87 % (194323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.12/12.87 % (194323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.12/12.87 % (194323)CaDiCaL version: 2.1.3
% 34.12/12.87 % (194323)Termination reason: Instruction limit
% 34.12/12.87 % (194323)Termination phase: Saturation
% 34.12/12.87 % (194323)Time elapsed: 7.301 s
% 34.12/12.87 % (194323)Peak memory usage: 336 MB
% 34.12/12.87 % (194323)Instructions burned: 14156 (million)
% 34.12/12.87 % (194292)Also succeeded, but the first one will report.
% 34.12/12.87 % (194345)Refutation found. Thanks to Tanya!
% 34.12/12.87 % SZS status Theorem for theBenchmark
% 34.12/12.87 % SZS output start Proof for theBenchmark
% See solution above
% 78.83/13.11 % (194345)------------------------------
% 78.83/13.11 % (194345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.83/13.11 % (194345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.83/13.11 % (194345)CaDiCaL version: 2.1.3
% 78.83/13.11 % (194345)Termination reason: Refutation
% 78.83/13.11 % (194345)Time elapsed: 2.083 s
% 78.83/13.11 % (194345)Peak memory usage: 126 MB
% 78.83/13.11 % (194345)Instructions burned: 2633 (million)
% 78.83/13.11 % (194345)------------------------------
% 78.83/13.11 % (194345)------------------------------
% 78.83/13.11 % (194101)Success in time 12.012 s
% 78.83/13.11 % Vampire exiting
%------------------------------------------------------------------------------