%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ANA005-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:30:50 AM UTC 2026
% Result : Unsatisfiable 31.57s 8.50s
% Output : Refutation 0.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 25
% Syntax : Number of formulae : 82 ( 24 unt; 6 def)
% Number of atoms : 191 ( 18 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 184 ( 75 ~; 108 |; 0 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 2 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 8 con; 0-2 aty)
% Number of variables : 116 ( 0 sgn 116 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X2,X0,X1] :
( ~ less_or_equal(add(absolute(X0),absolute(X1)),X2)
| less_or_equal(absolute(add(X0,X1)),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absolute_sum_less_or_equal_sum_of_absolutes2) ).
fof(f5,axiom,
! [X2,X0,X1] :
( ~ less_or_equal(X0,minimum(X1,X2))
| less_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minimum3) ).
fof(f7,axiom,
! [X0,X1] :
( minimum(X1,X0) = X0
| ~ less_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minimum5) ).
fof(f10,axiom,
! [X0,X1] :
( less_or_equal(X0,minimum(X1,X0))
| ~ less_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minimum8) ).
fof(f12,axiom,
! [X0] : add(half(X0),half(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',half_plus_half_is_whole) ).
fof(f16,axiom,
! [X0] :
( ~ less_or_equal(half(X0),n0)
| less_or_equal(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',zero_and_half) ).
fof(f18,axiom,
! [X2,X3,X0,X1] :
( less_or_equal(add(X0,X2),add(X1,X3))
| ~ less_or_equal(X2,X3)
| ~ less_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',add_to_both_sides_of_less_equal2) ).
fof(f19,axiom,
! [X0,X1] :
( less_or_equal(X1,X0)
| less_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_less_or_equal) ).
fof(f20,axiom,
! [X2,X0,X1] :
( less_or_equal(X0,X2)
| ~ less_or_equal(X1,X2)
| ~ less_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_of_less_or_equal) ).
fof(f21,axiom,
! [X0,X1] : add(X0,X1) = add(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_add) ).
fof(f23,axiom,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X0,add(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_add) ).
fof(f26,axiom,
! [X0,X1] :
( X0 != X1
| less_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equal_implies_less_or_equal) ).
fof(f27,axiom,
! [X0] :
( ~ less_or_equal(delta_1(X0),n0)
| less_or_equal(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1) ).
fof(f28,axiom,
! [X0] :
( ~ less_or_equal(delta_2(X0),n0)
| less_or_equal(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2) ).
fof(f29,axiom,
! [X0,X1] :
( less_or_equal(X0,n0)
| ~ less_or_equal(absolute(add(X1,negate(a_real_number))),delta_1(X0))
| less_or_equal(absolute(add(f(X1),negate(f(a_real_number)))),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3) ).
fof(f30,axiom,
! [X0,X1] :
( less_or_equal(X0,n0)
| ~ less_or_equal(absolute(add(X1,negate(a_real_number))),delta_2(X0))
| less_or_equal(absolute(add(g(X1),negate(g(a_real_number)))),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4) ).
fof(f31,axiom,
~ less_or_equal(epsilon_0,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5) ).
fof(f32,axiom,
! [X0] :
( less_or_equal(absolute(add(xs(X0),negate(a_real_number))),X0)
| less_or_equal(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6) ).
fof(f33,negated_conjecture,
! [X0] :
( less_or_equal(X0,n0)
| ~ less_or_equal(absolute(add(add(f(xs(X0)),g(xs(X0))),add(negate(f(a_real_number)),negate(g(a_real_number))))),epsilon_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_7) ).
fof(f34,plain,
! [X1] : less_or_equal(X1,X1),
inference(equality_resolution,[],[f26]) ).
fof(f35,definition,
sF0 = f(a_real_number),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f36,plain,
f(a_real_number) = sF0,
inference(reorient_equations,[],[f35]) ).
fof(f37,definition,
sF1 = negate(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f38,plain,
negate(sF0) = sF1,
inference(reorient_equations,[],[f37]) ).
fof(f39,definition,
sF2 = g(a_real_number),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f40,plain,
g(a_real_number) = sF2,
inference(reorient_equations,[],[f39]) ).
fof(f41,definition,
sF3 = negate(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f42,plain,
negate(sF2) = sF3,
inference(reorient_equations,[],[f41]) ).
fof(f43,definition,
sF4 = add(sF1,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f44,plain,
add(sF1,sF3) = sF4,
inference(reorient_equations,[],[f43]) ).
fof(f45,plain,
! [X0] :
( less_or_equal(X0,n0)
| ~ less_or_equal(absolute(add(add(f(xs(X0)),g(xs(X0))),sF4)),epsilon_0) ),
inference(definition_folding,[],[f33,f44,f42,f40,f38,f36]) ).
fof(f46,plain,
! [X0] :
( ~ less_or_equal(absolute(add(f(xs(X0)),add(g(xs(X0)),sF4))),epsilon_0)
| less_or_equal(X0,n0) ),
inference(backward_demodulation,[],[f45,f23]) ).
fof(f51,plain,
negate(f(a_real_number)) = sF1,
inference(forward_demodulation,[],[f38,f36]) ).
fof(f52,plain,
negate(g(a_real_number)) = sF3,
inference(forward_demodulation,[],[f42,f40]) ).
fof(f53,plain,
! [X0,X1] :
( ~ less_or_equal(absolute(add(X1,negate(a_real_number))),delta_1(X0))
| less_or_equal(X0,n0)
| less_or_equal(absolute(add(f(X1),sF1)),X0) ),
inference(backward_demodulation,[],[f29,f51]) ).
fof(f54,plain,
! [X0,X1] :
( ~ less_or_equal(absolute(add(X1,negate(a_real_number))),delta_2(X0))
| less_or_equal(X0,n0)
| less_or_equal(absolute(add(g(X1),sF3)),X0) ),
inference(backward_demodulation,[],[f30,f52]) ).
fof(f59,plain,
! [X0] : add(sF1,add(sF3,X0)) = add(sF4,X0),
inference(superposition,[],[f23,f44]) ).
fof(f79,plain,
! [X0] :
( less_or_equal(X0,n0)
| less_or_equal(absolute(add(f(xs(delta_1(X0))),sF1)),X0)
| less_or_equal(delta_1(X0),n0) ),
inference(resolution,[],[f53,f32]) ).
fof(f84,plain,
! [X0] :
( less_or_equal(absolute(add(f(xs(delta_1(X0))),sF1)),X0)
| less_or_equal(X0,n0) ),
inference(forward_subsumption_resolution,[],[f79,f27]) ).
fof(f85,plain,
! [X0] :
( less_or_equal(X0,n0)
| less_or_equal(absolute(add(g(xs(delta_2(X0))),sF3)),X0)
| less_or_equal(delta_2(X0),n0) ),
inference(resolution,[],[f54,f32]) ).
fof(f90,plain,
! [X0] :
( less_or_equal(absolute(add(g(xs(delta_2(X0))),sF3)),X0)
| less_or_equal(X0,n0) ),
inference(forward_subsumption_resolution,[],[f85,f28]) ).
fof(f145,plain,
! [X0,X1] :
( ~ less_or_equal(absolute(add(f(xs(X1)),add(g(xs(X1)),sF4))),X0)
| ~ less_or_equal(X0,epsilon_0)
| less_or_equal(X1,n0) ),
inference(resolution,[],[f20,f46]) ).
fof(f238,plain,
! [X0,X1] :
( less_or_equal(absolute(add(xs(minimum(X0,X1)),negate(a_real_number))),X0)
| less_or_equal(minimum(X0,X1),n0) ),
inference(resolution,[],[f5,f32]) ).
fof(f281,plain,
! [X0] :
( less_or_equal(absolute(add(sF3,g(xs(delta_2(X0))))),X0)
| less_or_equal(X0,n0) ),
inference(superposition,[],[f90,f21]) ).
fof(f284,plain,
! [X2,X3,X0,X1] :
( less_or_equal(absolute(add(X2,X0)),add(X3,X1))
| ~ less_or_equal(absolute(X2),X3)
| ~ less_or_equal(absolute(X0),X1) ),
inference(resolution,[],[f18,f2]) ).
fof(f320,plain,
! [X0,X1] :
( ~ less_or_equal(absolute(add(f(xs(X0)),add(sF4,g(xs(X0))))),X1)
| ~ less_or_equal(X1,epsilon_0)
| less_or_equal(X0,n0) ),
inference(superposition,[],[f145,f21]) ).
fof(f342,plain,
! [X0,X1] :
( ~ less_or_equal(half(X0),X1)
| ~ less_or_equal(X1,n0)
| less_or_equal(X0,n0) ),
inference(resolution,[],[f16,f20]) ).
fof(f521,plain,
! [X2,X3,X0,X1,X4] :
( less_or_equal(absolute(add(X0,add(X1,X2))),add(X3,X4))
| ~ less_or_equal(absolute(add(X0,X1)),X3)
| ~ less_or_equal(absolute(X2),X4) ),
inference(superposition,[],[f284,f23]) ).
fof(f802,plain,
! [X0,X1] :
( less_or_equal(absolute(add(xs(X0),negate(a_real_number))),X1)
| less_or_equal(X0,n0)
| ~ less_or_equal(X0,X1) ),
inference(superposition,[],[f238,f7]) ).
fof(f960,plain,
! [X0,X1] :
( less_or_equal(absolute(add(f(xs(X0)),sF1)),X1)
| ~ less_or_equal(X0,delta_1(X1))
| less_or_equal(X1,n0)
| less_or_equal(X0,n0) ),
inference(resolution,[],[f802,f53]) ).
fof(f963,plain,
! [X2,X0,X1] :
( less_or_equal(absolute(add(xs(X0),negate(a_real_number))),X1)
| ~ less_or_equal(X0,minimum(X1,X2))
| less_or_equal(X0,n0) ),
inference(resolution,[],[f802,f5]) ).
fof(f1155,plain,
! [X2,X3,X0,X1] :
( less_or_equal(absolute(add(X1,add(sF4,X0))),add(X2,X3))
| ~ less_or_equal(absolute(add(X1,sF1)),X2)
| ~ less_or_equal(absolute(add(sF3,X0)),X3) ),
inference(superposition,[],[f521,f59]) ).
fof(f2323,plain,
! [X2,X0,X1] :
( less_or_equal(absolute(add(g(xs(X0)),sF3)),X1)
| less_or_equal(X0,n0)
| less_or_equal(X1,n0)
| ~ less_or_equal(X0,minimum(delta_2(X1),X2)) ),
inference(resolution,[],[f963,f54]) ).
fof(f3684,definition,
( spl5_50
<=> less_or_equal(half(epsilon_0),n0) ),
introduced(definition,[new_symbols(definition,[spl5_50])],[avatar_definition]) ).
fof(f3685,plain,
( ~ less_or_equal(half(epsilon_0),n0)
| spl5_50 ),
inference(avatar_component_clause,[],[f3684]) ).
fof(f3686,plain,
( less_or_equal(half(epsilon_0),n0)
| ~ spl5_50 ),
inference(avatar_component_clause,[],[f3684]) ).
fof(f6144,plain,
( ~ less_or_equal(n0,n0)
| less_or_equal(epsilon_0,n0)
| ~ spl5_50 ),
inference(resolution,[],[f3686,f342]) ).
fof(f6155,plain,
( less_or_equal(epsilon_0,n0)
| ~ spl5_50 ),
inference(forward_subsumption_resolution,[],[f6144,f34]) ).
fof(f6158,plain,
( $false
| ~ spl5_50 ),
inference(forward_subsumption_resolution,[],[f6155,f31]) ).
fof(f6159,plain,
~ spl5_50,
inference(avatar_contradiction_clause,[],[f6158]) ).
fof(f13218,plain,
! [X2,X0,X1] :
( ~ less_or_equal(absolute(add(sF3,g(xs(X0)))),X2)
| ~ less_or_equal(absolute(add(f(xs(X0)),sF1)),X1)
| ~ less_or_equal(add(X1,X2),epsilon_0)
| less_or_equal(X0,n0) ),
inference(resolution,[],[f1155,f320]) ).
fof(f13249,plain,
! [X0,X1] :
( ~ less_or_equal(absolute(add(f(xs(delta_2(X0))),sF1)),X1)
| ~ less_or_equal(add(X1,X0),epsilon_0)
| less_or_equal(delta_2(X0),n0)
| less_or_equal(X0,n0) ),
inference(resolution,[],[f13218,f281]) ).
fof(f13301,plain,
! [X2,X0,X1] :
( ~ less_or_equal(absolute(add(g(xs(X0)),sF3)),X1)
| ~ less_or_equal(absolute(add(f(xs(X0)),sF1)),X2)
| ~ less_or_equal(add(X2,X1),epsilon_0)
| less_or_equal(X0,n0) ),
inference(superposition,[],[f13218,f21]) ).
fof(f13307,plain,
! [X0,X1] :
( ~ less_or_equal(absolute(add(f(xs(delta_2(X0))),sF1)),X1)
| ~ less_or_equal(add(X1,X0),epsilon_0)
| less_or_equal(X0,n0) ),
inference(forward_subsumption_resolution,[],[f13249,f28]) ).
fof(f13313,plain,
! [X0,X1] :
( ~ less_or_equal(add(X0,X1),epsilon_0)
| less_or_equal(X1,n0)
| ~ less_or_equal(delta_2(X1),delta_1(X0))
| less_or_equal(X0,n0)
| less_or_equal(delta_2(X1),n0) ),
inference(resolution,[],[f13307,f960]) ).
fof(f13390,plain,
! [X0,X1] :
( ~ less_or_equal(delta_2(X1),delta_1(X0))
| less_or_equal(X1,n0)
| ~ less_or_equal(add(X0,X1),epsilon_0)
| less_or_equal(X0,n0) ),
inference(forward_subsumption_resolution,[],[f13313,f28]) ).
fof(f13412,plain,
! [X0,X1] :
( less_or_equal(X0,n0)
| ~ less_or_equal(add(X1,X0),epsilon_0)
| less_or_equal(X1,n0)
| less_or_equal(delta_1(X1),delta_2(X0)) ),
inference(resolution,[],[f13390,f19]) ).
fof(f30340,plain,
! [X2,X3,X0,X1] :
( ~ less_or_equal(absolute(add(f(xs(X0)),sF1)),X1)
| ~ less_or_equal(add(X1,X2),epsilon_0)
| less_or_equal(X0,n0)
| less_or_equal(X0,n0)
| less_or_equal(X2,n0)
| ~ less_or_equal(X0,minimum(delta_2(X2),X3)) ),
inference(resolution,[],[f13301,f2323]) ).
fof(f30406,plain,
! [X2,X3,X0,X1] :
( ~ less_or_equal(absolute(add(f(xs(X0)),sF1)),X1)
| ~ less_or_equal(add(X1,X2),epsilon_0)
| less_or_equal(X0,n0)
| less_or_equal(X2,n0)
| ~ less_or_equal(X0,minimum(delta_2(X2),X3)) ),
inference(duplicate_literal_removal,[],[f30340]) ).
fof(f30507,plain,
! [X2,X0,X1] :
( ~ less_or_equal(add(X0,X1),epsilon_0)
| less_or_equal(delta_1(X0),n0)
| less_or_equal(X1,n0)
| ~ less_or_equal(delta_1(X0),minimum(delta_2(X1),X2))
| less_or_equal(X0,n0) ),
inference(resolution,[],[f30406,f84]) ).
fof(f30600,plain,
! [X2,X0,X1] :
( ~ less_or_equal(delta_1(X0),minimum(delta_2(X1),X2))
| less_or_equal(X1,n0)
| ~ less_or_equal(add(X0,X1),epsilon_0)
| less_or_equal(X0,n0) ),
inference(forward_subsumption_resolution,[],[f30507,f27]) ).
fof(f30605,plain,
! [X0,X1] :
( less_or_equal(X0,n0)
| ~ less_or_equal(add(X1,X0),epsilon_0)
| less_or_equal(X1,n0)
| ~ less_or_equal(delta_1(X1),delta_2(X0)) ),
inference(resolution,[],[f30600,f10]) ).
fof(f30613,plain,
! [X0,X1] :
( ~ less_or_equal(add(X1,X0),epsilon_0)
| less_or_equal(X0,n0)
| less_or_equal(X1,n0) ),
inference(forward_subsumption_resolution,[],[f30605,f13412]) ).
fof(f30629,plain,
! [X0] :
( ~ less_or_equal(X0,epsilon_0)
| less_or_equal(half(X0),n0)
| less_or_equal(half(X0),n0) ),
inference(superposition,[],[f30613,f12]) ).
fof(f30635,plain,
! [X0] :
( less_or_equal(half(X0),n0)
| ~ less_or_equal(X0,epsilon_0) ),
inference(duplicate_literal_removal,[],[f30629]) ).
fof(f30661,plain,
( ~ less_or_equal(epsilon_0,epsilon_0)
| spl5_50 ),
inference(resolution,[],[f30635,f3685]) ).
fof(f30663,plain,
( $false
| spl5_50 ),
inference(forward_subsumption_resolution,[],[f30661,f34]) ).
fof(f30664,plain,
spl5_50,
inference(avatar_contradiction_clause,[],[f30663]) ).
cnf(s123,plain,
~ spl5_50,
inference(sat_conversion,[],[f6159]) ).
cnf(s417,plain,
spl5_50,
inference(sat_conversion,[],[f30664]) ).
cnf(s420,plain,
$false,
inference(rat,[],[s123,s417]) ).
fof(f30670,plain,
$false,
inference(avatar_sat_refutation,[],[s420]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ANA005-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.27/0.30 % Computer : n008.cluster.edu
% 0.27/0.30 % Model : x86_64 x86_64
% 0.27/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.27/0.30 % Memory : 8046.5625MB
% 0.27/0.30 % OS : Linux 6.8.0-71-generic
% 0.27/0.30 % CPULimit : 300
% 0.27/0.30 % WCLimit : 300
% 0.27/0.30 % DateTime : Mon Sep 28 20:27:09 UTC 2026
% 0.27/0.30 % CPUTime :
% 0.27/0.30 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.27/0.36 Running first-order theorem proving
% 0.27/0.36 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.55/3.17 % (2590171)Input is clausal, will run a generic CNF schedule.
% 17.55/3.17 % (2590188)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1161317316:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 17.55/3.17 % (2590188)Instruction limit reached!
% 17.55/3.17 % (2590188)------------------------------
% 17.55/3.17 % (2590188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.55/3.17 % (2590188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.55/3.17 % (2590188)CaDiCaL version: 2.1.3
% 17.55/3.17 % (2590188)Termination reason: Instruction limit
% 17.55/3.17 % (2590188)Termination phase: Saturation
% 17.55/3.17 % (2590188)Time elapsed: 0.059 s
% 17.55/3.17 % (2590188)Peak memory usage: 89 MB
% 17.55/3.17 % (2590188)Instructions burned: 115 (million)
% 17.55/3.17 % (2590186)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3423150216:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 17.55/3.17 % (2590184)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=4287212325:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 17.55/3.17 % (2590185)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2201837020:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 17.55/3.17 % (2590190)dis-21_1_sil=8000:lcm=predicate:random_seed=3853707829: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.55/3.17 % (2590187)lrs+10_1_sil=8000:sp=occurrence:random_seed=1885508445:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 17.55/3.17 % (2590189)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=894094138:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 17.55/3.17 % (2590187)Instruction limit reached!
% 17.55/3.17 % (2590187)------------------------------
% 17.55/3.17 % (2590187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.55/3.17 % (2590187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.55/3.17 % (2590187)CaDiCaL version: 2.1.3
% 17.55/3.17 % (2590187)Termination reason: Instruction limit
% 17.55/3.17 % (2590187)Termination phase: Saturation
% 17.55/3.17 % (2590187)Time elapsed: 0.094 s
% 17.55/3.17 % (2590187)Peak memory usage: 88 MB
% 17.55/3.17 % (2590187)Instructions burned: 107 (million)
% 17.55/3.17 % (2590190)Instruction limit reached!
% 17.55/3.17 % (2590190)------------------------------
% 17.55/3.17 % (2590190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.55/3.17 % (2590190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.55/3.17 % (2590190)CaDiCaL version: 2.1.3
% 17.55/3.17 % (2590190)Termination reason: Instruction limit
% 17.55/3.17 % (2590190)Termination phase: Saturation
% 17.55/3.17 % (2590190)Time elapsed: 0.110 s
% 17.55/3.17 % (2590190)Peak memory usage: 89 MB
% 17.55/3.17 % (2590190)Instructions burned: 117 (million)
% 17.55/3.17 % (2590189)Instruction limit reached!
% 17.55/3.17 % (2590189)------------------------------
% 17.55/3.17 % (2590189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.55/3.17 % (2590189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.55/3.17 % (2590189)CaDiCaL version: 2.1.3
% 17.55/3.17 % (2590189)Termination reason: Instruction limit
% 17.55/3.17 % (2590189)Termination phase: Saturation
% 17.55/3.17 % (2590189)Time elapsed: 0.170 s
% 17.55/3.17 % (2590189)Peak memory usage: 89 MB
% 17.55/3.17 % (2590189)Instructions burned: 180 (million)
% 17.55/3.17 % (2590195)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=2362020523:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 17.55/3.17 % (2590195)Instruction limit reached!
% 17.55/3.17 % (2590195)------------------------------
% 17.55/3.17 % (2590195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.55/3.17 % (2590195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.55/3.17 % (2590195)CaDiCaL version: 2.1.3
% 17.55/3.17 % (2590195)Termination reason: Instruction limit
% 17.55/3.17 % (2590195)Termination phase: Saturation
% 17.55/3.17 % (2590195)Time elapsed: 0.071 s
% 17.55/3.17 % (2590195)Peak memory usage: 89 MB
% 17.55/3.17 % (2590195)Instructions burned: 144 (million)
% 17.55/3.17 % (2590199)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1262914232: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)
% 30.99/5.12 % (2590200)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3781764909:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 30.99/5.12 % (2590201)lrs+10_64_to=lpo:sil=8000:random_seed=2509836185:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 30.99/5.12 % (2590203)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1902412432:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 30.99/5.12 % (2590199)Instruction limit reached!
% 30.99/5.12 % (2590199)------------------------------
% 30.99/5.12 % (2590199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.12 % (2590199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.12 % (2590199)CaDiCaL version: 2.1.3
% 30.99/5.12 % (2590199)Termination reason: Instruction limit
% 30.99/5.12 % (2590199)Termination phase: Saturation
% 30.99/5.12 % (2590199)Time elapsed: 0.163 s
% 30.99/5.12 % (2590199)Peak memory usage: 90 MB
% 30.99/5.12 % (2590199)Instructions burned: 190 (million)
% 30.99/5.12 % (2590200)Instruction limit reached!
% 30.99/5.12 % (2590200)------------------------------
% 30.99/5.12 % (2590200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.12 % (2590200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.12 % (2590200)CaDiCaL version: 2.1.3
% 30.99/5.12 % (2590200)Termination reason: Instruction limit
% 30.99/5.12 % (2590200)Termination phase: Saturation
% 30.99/5.12 % (2590200)Time elapsed: 0.200 s
% 30.99/5.12 % (2590200)Peak memory usage: 89 MB
% 30.99/5.12 % (2590200)Instructions burned: 220 (million)
% 30.99/5.12 % (2590201)Instruction limit reached!
% 30.99/5.12 % (2590201)------------------------------
% 30.99/5.12 % (2590201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.12 % (2590201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.12 % (2590201)CaDiCaL version: 2.1.3
% 30.99/5.12 % (2590201)Termination reason: Instruction limit
% 30.99/5.12 % (2590201)Termination phase: Saturation
% 30.99/5.12 % (2590201)Time elapsed: 0.104 s
% 30.99/5.12 % (2590201)Peak memory usage: 89 MB
% 30.99/5.12 % (2590201)Instructions burned: 126 (million)
% 30.99/5.12 % (2590203)Instruction limit reached!
% 30.99/5.12 % (2590203)------------------------------
% 30.99/5.12 % (2590203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.12 % (2590203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.12 % (2590203)CaDiCaL version: 2.1.3
% 30.99/5.12 % (2590203)Termination reason: Instruction limit
% 30.99/5.12 % (2590203)Termination phase: Saturation
% 30.99/5.12 % (2590203)Time elapsed: 0.086 s
% 30.99/5.12 % (2590203)Peak memory usage: 90 MB
% 30.99/5.12 % (2590203)Instructions burned: 194 (million)
% 30.99/5.12 % (2590211)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2120276037:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 30.99/5.12 % (2590208)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=622582088:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 30.99/5.12 % (2590211)Instruction limit reached!
% 30.99/5.12 % (2590211)------------------------------
% 30.99/5.12 % (2590211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.99/5.12 % (2590211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.99/5.12 % (2590211)CaDiCaL version: 2.1.3
% 30.99/5.12 % (2590211)Termination reason: Instruction limit
% 30.99/5.12 % (2590211)Termination phase: Saturation
% 30.99/5.12 % (2590211)Time elapsed: 0.048 s
% 30.99/5.12 % (2590211)Peak memory usage: 88 MB
% 30.99/5.12 % (2590211)Instructions burned: 108 (million)
% 30.99/5.12 % (2590210)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=2689049923:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 30.99/5.12 % (2590209)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=476385066:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 30.99/5.12 % (2590210)Instruction limit reached!
% 30.99/5.12 % (2590210)------------------------------
% 30.99/5.12 % (2590210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.13/8.28 % (2590210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.13/8.28 % (2590210)CaDiCaL version: 2.1.3
% 53.13/8.28 % (2590210)Termination reason: Instruction limit
% 53.13/8.28 % (2590210)Termination phase: Saturation
% 53.13/8.28 % (2590210)Time elapsed: 0.089 s
% 53.13/8.28 % (2590210)Peak memory usage: 89 MB
% 53.13/8.28 % (2590210)Instructions burned: 107 (million)
% 53.13/8.28 % (2590208)Instruction limit reached!
% 53.13/8.28 % (2590208)------------------------------
% 53.13/8.28 % (2590208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.13/8.28 % (2590208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.13/8.28 % (2590208)CaDiCaL version: 2.1.3
% 53.13/8.28 % (2590208)Termination reason: Instruction limit
% 53.13/8.28 % (2590208)Termination phase: Saturation
% 53.13/8.28 % (2590208)Time elapsed: 0.154 s
% 53.13/8.28 % (2590208)Peak memory usage: 90 MB
% 53.13/8.28 % (2590208)Instructions burned: 158 (million)
% 53.13/8.28 % (2590216)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3548122325:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2988 on theBenchmark for (2988ds/242Mi)
% 53.13/8.28 % (2590216)Instruction limit reached!
% 53.13/8.28 % (2590216)------------------------------
% 53.13/8.28 % (2590216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.13/8.28 % (2590216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.13/8.28 % (2590216)CaDiCaL version: 2.1.3
% 53.13/8.28 % (2590216)Termination reason: Instruction limit
% 53.13/8.28 % (2590216)Termination phase: Saturation
% 53.13/8.28 % (2590216)Time elapsed: 0.112 s
% 53.13/8.28 % (2590216)Peak memory usage: 89 MB
% 53.13/8.28 % (2590216)Instructions burned: 242 (million)
% 53.13/8.28 % (2590217)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3460041939:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 53.13/8.28 % (2590218)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2217030527:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 53.13/8.28 % (2590218)Instruction limit reached!
% 53.13/8.28 % (2590218)------------------------------
% 53.13/8.28 % (2590218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.13/8.28 % (2590218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.13/8.28 % (2590218)CaDiCaL version: 2.1.3
% 53.13/8.28 % (2590218)Termination reason: Instruction limit
% 53.13/8.28 % (2590218)Termination phase: Saturation
% 53.13/8.28 % (2590218)Time elapsed: 0.130 s
% 53.13/8.28 % (2590218)Peak memory usage: 89 MB
% 53.13/8.28 % (2590218)Instructions burned: 134 (million)
% 53.13/8.28 % (2590220)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4172115982:i=499:bd=all_2985 on theBenchmark for (2985ds/499Mi)
% 53.13/8.28 % (2590220)Instruction limit reached!
% 53.13/8.28 % (2590220)------------------------------
% 53.13/8.28 % (2590220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.13/8.28 % (2590220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.13/8.28 % (2590220)CaDiCaL version: 2.1.3
% 53.13/8.28 % (2590220)Termination reason: Instruction limit
% 53.13/8.28 % (2590220)Termination phase: Saturation
% 53.13/8.28 % (2590220)Time elapsed: 0.237 s
% 53.13/8.28 % (2590220)Peak memory usage: 95 MB
% 53.13/8.28 % (2590220)Instructions burned: 501 (million)
% 53.13/8.28 % (2590223)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2168619202:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 53.13/8.28 % (2590223)Instruction limit reached!
% 53.13/8.28 % (2590223)------------------------------
% 53.13/8.28 % (2590223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.13/8.28 % (2590223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.13/8.28 % (2590223)CaDiCaL version: 2.1.3
% 53.13/8.28 % (2590223)Termination reason: Instruction limit
% 53.13/8.28 % (2590223)Termination phase: Saturation
% 53.13/8.28 % (2590223)Time elapsed: 0.165 s
% 53.13/8.28 % (2590223)Peak memory usage: 91 MB
% 53.13/8.28 % (2590223)Instructions burned: 192 (million)
% 53.13/8.28 % (2590225)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3710073236:i=264:kws=precedence:fsr=off_2980 on theBenchmark for (2980ds/264Mi)
% 53.13/8.28 % (2590227)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3989035993:cond=on:i=156:bs=on:gtg=exists_all:er=known_2978 on theBenchmark for (2978ds/156Mi)
% 31.57/8.50 % (2590225)Instruction limit reached!
% 31.57/8.50 % (2590225)------------------------------
% 31.57/8.50 % (2590225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/8.50 % (2590225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/8.50 % (2590225)CaDiCaL version: 2.1.3
% 31.57/8.50 % (2590225)Termination reason: Instruction limit
% 31.57/8.50 % (2590225)Termination phase: Saturation
% 31.57/8.50 % (2590225)Time elapsed: 0.226 s
% 31.57/8.50 % (2590225)Peak memory usage: 91 MB
% 31.57/8.50 % (2590225)Instructions burned: 265 (million)
% 31.57/8.50 % (2590227)Instruction limit reached!
% 31.57/8.50 % (2590227)------------------------------
% 31.57/8.50 % (2590227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/8.50 % (2590227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/8.50 % (2590227)CaDiCaL version: 2.1.3
% 31.57/8.50 % (2590227)Termination reason: Instruction limit
% 31.57/8.50 % (2590227)Termination phase: Saturation
% 31.57/8.50 % (2590227)Time elapsed: 0.135 s
% 31.57/8.50 % (2590227)Peak memory usage: 89 MB
% 31.57/8.50 % (2590227)Instructions burned: 157 (million)
% 31.57/8.50 % (2590230)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=1646414436:i=3256:kws=precedence:bd=preordered:av=off_2975 on theBenchmark for (2975ds/3256Mi)
% 31.57/8.50 % (2590231)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=503410738:i=537:av=off:ss=included_2974 on theBenchmark for (2974ds/537Mi)
% 31.57/8.50 % (2590231)Instruction limit reached!
% 31.57/8.50 % (2590231)------------------------------
% 31.57/8.50 % (2590231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/8.50 % (2590231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/8.50 % (2590231)CaDiCaL version: 2.1.3
% 31.57/8.50 % (2590231)Termination reason: Instruction limit
% 31.57/8.50 % (2590231)Termination phase: Saturation
% 31.57/8.50 % (2590231)Time elapsed: 0.437 s
% 31.57/8.50 % (2590231)Peak memory usage: 89 MB
% 31.57/8.50 % (2590231)Instructions burned: 538 (million)
% 31.57/8.50 % (2590209)Instruction limit reached!
% 31.57/8.50 % (2590209)------------------------------
% 31.57/8.50 % (2590209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/8.50 % (2590209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/8.50 % (2590209)CaDiCaL version: 2.1.3
% 31.57/8.50 % (2590209)Termination reason: Instruction limit
% 31.57/8.50 % (2590209)Termination phase: Saturation
% 31.57/8.50 % (2590209)Time elapsed: 2.262 s
% 31.57/8.50 % (2590209)Peak memory usage: 149 MB
% 31.57/8.50 % (2590209)Instructions burned: 3395 (million)
% 31.57/8.50 % (2590234)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2091658303:i=180:bd=preordered:av=off_2967 on theBenchmark for (2967ds/180Mi)
% 31.57/8.50 % (2590235)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=4210390298:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2965 on theBenchmark for (2965ds/10307Mi)
% 31.57/8.50 % (2590234)Instruction limit reached!
% 31.57/8.50 % (2590234)------------------------------
% 31.57/8.50 % (2590234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/8.50 % (2590234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/8.50 % (2590234)CaDiCaL version: 2.1.3
% 31.57/8.50 % (2590234)Termination reason: Instruction limit
% 31.57/8.50 % (2590234)Termination phase: Saturation
% 31.57/8.50 % (2590234)Time elapsed: 0.156 s
% 31.57/8.50 % (2590234)Peak memory usage: 89 MB
% 31.57/8.50 % (2590234)Instructions burned: 180 (million)
% 31.57/8.50 % (2590238)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=3597516407:i=412:gtgl=4:gtg=exists_all_2962 on theBenchmark for (2962ds/412Mi)
% 31.57/8.50 % (2590238)Instruction limit reached!
% 31.57/8.50 % (2590238)------------------------------
% 31.57/8.50 % (2590238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/8.50 % (2590238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/8.50 % (2590238)CaDiCaL version: 2.1.3
% 31.57/8.50 % (2590238)Termination reason: Instruction limit
% 31.57/8.50 % (2590238)Termination phase: Saturation
% 31.57/8.50 % (2590238)Time elapsed: 0.345 s
% 31.57/8.50 % (2590238)Peak memory usage: 91 MB
% 31.57/8.50 % (2590238)Instructions burned: 412 (million)
% 31.57/8.50 % (2590240)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=302131898:s2pl=no:i=8478:s2at=4:nm=6_2956 on theBenchmark for (2956ds/8478Mi)
% 31.57/8.50 % (2590230)Instruction limit reached!
% 31.57/8.50 % (2590230)------------------------------
% 31.57/8.50 % (2590230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/8.50 % (2590230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/8.50 % (2590230)CaDiCaL version: 2.1.3
% 31.57/8.50 % (2590230)Termination reason: Instruction limit
% 31.57/8.50 % (2590230)Termination phase: Saturation
% 31.57/8.50 % (2590230)Time elapsed: 3.150 s
% 31.57/8.50 % (2590230)Peak memory usage: 151 MB
% 31.57/8.50 % (2590230)Instructions burned: 3256 (million)
% 31.57/8.50 % (2590245)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=2334054676:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2940 on theBenchmark for (2940ds/303Mi)
% 31.57/8.50 % (2590245)Instruction limit reached!
% 31.57/8.50 % (2590245)------------------------------
% 31.57/8.50 % (2590245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/8.50 % (2590245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/8.50 % (2590245)CaDiCaL version: 2.1.3
% 31.57/8.50 % (2590245)Termination reason: Instruction limit
% 31.57/8.50 % (2590245)Termination phase: Saturation
% 31.57/8.50 % (2590245)Time elapsed: 0.220 s
% 31.57/8.50 % (2590245)Peak memory usage: 90 MB
% 31.57/8.50 % (2590245)Instructions burned: 304 (million)
% 31.57/8.50 % (2590217)Instruction limit reached!
% 31.57/8.50 % (2590217)------------------------------
% 31.57/8.50 % (2590217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/8.50 % (2590217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/8.50 % (2590217)CaDiCaL version: 2.1.3
% 31.57/8.50 % (2590217)Termination reason: Instruction limit
% 31.57/8.50 % (2590217)Termination phase: Saturation
% 31.57/8.50 % (2590217)Time elapsed: 4.986 s
% 31.57/8.50 % (2590217)Peak memory usage: 162 MB
% 31.57/8.50 % (2590217)Instructions burned: 5208 (million)
% 31.57/8.50 % (2590247)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1695067157:st=4:i=720:sd=3:fsr=off:ss=axioms_2935 on theBenchmark for (2935ds/720Mi)
% 31.57/8.50 % (2590248)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=691745059:i=598:bs=on:bd=preordered:av=off:ss=axioms_2934 on theBenchmark for (2934ds/598Mi)
% 31.57/8.50 % (2590248)Instruction limit reached!
% 31.57/8.50 % (2590248)------------------------------
% 31.57/8.50 % (2590248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/8.50 % (2590248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/8.50 % (2590248)CaDiCaL version: 2.1.3
% 31.57/8.50 % (2590248)Termination reason: Instruction limit
% 31.57/8.50 % (2590248)Termination phase: Saturation
% 31.57/8.50 % (2590248)Time elapsed: 0.537 s
% 31.57/8.50 % (2590248)Peak memory usage: 95 MB
% 31.57/8.50 % (2590248)Instructions burned: 598 (million)
% 31.57/8.50 % (2590247)Instruction limit reached!
% 31.57/8.50 % (2590247)------------------------------
% 31.57/8.50 % (2590247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.57/8.50 % (2590247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.57/8.50 % (2590247)CaDiCaL version: 2.1.3
% 31.57/8.50 % (2590247)Termination reason: Instruction limit
% 31.57/8.50 % (2590247)Termination phase: Saturation
% 31.57/8.50 % (2590247)Time elapsed: 0.629 s
% 31.57/8.50 % (2590247)Peak memory usage: 100 MB
% 31.57/8.50 % (2590247)Instructions burned: 722 (million)
% 31.57/8.50 % (2590186)First to succeed.
% 31.57/8.50 % (2590186)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2590171"
% 31.57/8.50 % (2590254)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=3345864970:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2926 on theBenchmark for (2926ds/1997Mi)
% 31.57/8.50 % (2590253)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=684512874:i=2989:sd=3:ss=axioms:sgt=60_2926 on theBenchmark for (2926ds/2989Mi)
% 31.57/8.50 % (2590186)Refutation found. Thanks to Tanya!
% 31.57/8.50 % SZS status Unsatisfiable for theBenchmark
% 31.57/8.50 % SZS output start Proof for theBenchmark
% See solution above
% 0.34/8.70 % (2590186)------------------------------
% 0.34/8.70 % (2590186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.34/8.70 % (2590186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.34/8.70 % (2590186)CaDiCaL version: 2.1.3
% 0.34/8.70 % (2590186)Termination reason: Refutation
% 0.34/8.70 % (2590186)Time elapsed: 7.194 s
% 0.34/8.70 % (2590186)Peak memory usage: 161 MB
% 0.34/8.70 % (2590186)Instructions burned: 7466 (million)
% 0.34/8.70 % (2590186)------------------------------
% 0.34/8.70 % (2590186)------------------------------
% 0.34/8.70 % (2590171)Success in time 7.754 s
% 0.34/8.70 % Vampire exiting
%------------------------------------------------------------------------------