%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ARI621_2 : TPTP v9.3.1. Released v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:33:30 AM UTC 2026
% Result : Theorem 12.10s 2.62s
% Output : Refutation 12.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 12
% Syntax : Number of formulae : 45 ( 3 unt; 0 typ; 11 def)
% Number of atoms : 154 ( 45 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 162 ( 53 ~; 62 |; 29 &)
% ( 15 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 164 ( 15 atm; 20 fun; 107 num; 22 var)
% Number of types : 2 ( 0 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 16 ( 12 usr; 12 prp; 0-2 aty)
% Number of functors : 5 ( 1 usr; 3 con; 0-2 aty)
% Number of variables : 22 ( 15 !; 7 ?; 22 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_7,type,
sK0: $rat > $rat ).
tff(pred_def_1,type,
pow2: $rat > $o ).
tff(f1,conjecture,
( ! [X0: $rat] :
( pow2(X0)
<=> ( ( $lesseq(2/1,X0)
& ? [X1: $rat] :
( ( $product(2/1,X1) = X0 )
& pow2(X1) ) )
| ( X0 = 1/1 ) ) )
=> ~ pow2(12/1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_pow_of_2_10) ).
tff(f2,negated_conjecture,
~ ( ! [X0: $rat] :
( pow2(X0)
<=> ( ( $lesseq(2/1,X0)
& ? [X1: $rat] :
( ( $product(2/1,X1) = X0 )
& pow2(X1) ) )
| ( X0 = 1/1 ) ) )
=> ~ pow2(12/1) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
tff(f3,plain,
~ ( ! [X0: $rat] :
( ( ( X0 = 1/1 )
| ( ~ $less(X0,2/1)
& ? [X1: $rat] :
( ( $product(2/1,X1) = X0 )
& pow2(X1) ) ) )
<=> pow2(X0) )
=> ~ pow2(12/1) ),
inference(theory_normalization,[],[f2]) ).
tff(f21,plain,
( pow2(12/1)
& ! [X0: $rat] :
( ( ( X0 = 1/1 )
| ( ~ $less(X0,2/1)
& ? [X1: $rat] :
( ( $product(2/1,X1) = X0 )
& pow2(X1) ) ) )
<=> pow2(X0) ) ),
inference(ennf_transformation,[],[f3]) ).
tff(f22,plain,
( pow2(12/1)
& ! [X0: $rat] :
( ( ( X0 = 1/1 )
| ( ~ $less(X0,2/1)
& ? [X1: $rat] :
( ( $product(2/1,X1) = X0 )
& pow2(X1) ) )
| ~ pow2(X0) )
& ( pow2(X0)
| ( ( 1/1 != X0 )
& ( $less(X0,2/1)
| ! [X1: $rat] :
( ( $product(2/1,X1) != X0 )
| ~ pow2(X1) ) ) ) ) ) ),
inference(nnf_transformation,[],[f21]) ).
tff(f23,plain,
( pow2(12/1)
& ! [X0: $rat] :
( ( ( X0 = 1/1 )
| ( ~ $less(X0,2/1)
& ? [X1: $rat] :
( ( $product(2/1,X1) = X0 )
& pow2(X1) ) )
| ~ pow2(X0) )
& ( pow2(X0)
| ( ( 1/1 != X0 )
& ( $less(X0,2/1)
| ! [X1: $rat] :
( ( $product(2/1,X1) != X0 )
| ~ pow2(X1) ) ) ) ) ) ),
inference(flattening,[],[f22]) ).
tff(f24,plain,
( pow2(12/1)
& ! [X0: $rat] :
( ( ( X0 = 1/1 )
| ( ~ $less(X0,2/1)
& ? [X1: $rat] :
( ( $product(2/1,X1) = X0 )
& pow2(X1) ) )
| ~ pow2(X0) )
& ( pow2(X0)
| ( ( 1/1 != X0 )
& ( $less(X0,2/1)
| ! [X2: $rat] :
( ( $product(2/1,X2) != X0 )
| ~ pow2(X2) ) ) ) ) ) ),
inference(rectify,[],[f23]) ).
tff(f25,plain,
( pow2(12/1)
& ! [X0: $rat] :
( ( ( X0 = 1/1 )
| ( ~ $less(X0,2/1)
& ( $product(2/1,sK0(X0)) = X0 )
& pow2(sK0(X0)) )
| ~ pow2(X0) )
& ( pow2(X0)
| ( ( 1/1 != X0 )
& ( $less(X0,2/1)
| ! [X2: $rat] :
( ( $product(2/1,X2) != X0 )
| ~ pow2(X2) ) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[f24]) ).
tff(f28,plain,
! [X0: $rat] :
( ~ pow2(X0)
| pow2(sK0(X0))
| ( 1/1 = X0 ) ),
inference(cnf_transformation,[],[f25]) ).
tff(f29,plain,
! [X0: $rat] :
( ~ pow2(X0)
| ( $product(2/1,sK0(X0)) = X0 )
| ( 1/1 = X0 ) ),
inference(cnf_transformation,[],[f25]) ).
tff(f30,plain,
! [X0: $rat] :
( ~ pow2(X0)
| ~ $less(X0,2/1)
| ( 1/1 = X0 ) ),
inference(cnf_transformation,[],[f25]) ).
tff(f31,plain,
pow2(12/1),
inference(cnf_transformation,[],[f25]) ).
tff(f33,definition,
( spl1_1
<=> pow2(12/1) ),
introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition]) ).
tff(f35,plain,
( pow2(12/1)
| ~ spl1_1 ),
inference(avatar_component_clause,[],[f33]) ).
tff(f36,plain,
spl1_1,
inference(avatar_split_clause,[],[f31,f33]) ).
tff(f48,plain,
( pow2(sK0(12/1))
| ( 1/1 = 12/1 )
| ~ spl1_1 ),
inference(resolution,[],[f28,f35]) ).
tff(f50,plain,
( pow2(sK0(12/1))
| ~ spl1_1 ),
inference(evaluation,[],[f48]) ).
tff(f52,definition,
( spl1_3
<=> pow2(sK0(12/1)) ),
introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition]) ).
tff(f54,plain,
( pow2(sK0(12/1))
| ~ spl1_3 ),
inference(avatar_component_clause,[],[f52]) ).
tff(f55,plain,
( spl1_3
| ~ spl1_1 ),
inference(avatar_split_clause,[],[f50,f33,f52]) ).
tff(f58,plain,
( ( 12/1 = $product(2/1,sK0(12/1)) )
| ( 1/1 = 12/1 )
| ~ spl1_1 ),
inference(resolution,[],[f29,f35]) ).
tff(f60,plain,
( ( 12/1 = $product(2/1,sK0(12/1)) )
| ~ spl1_1 ),
inference(evaluation,[],[f58]) ).
tff(f62,definition,
( spl1_4
<=> ( 12/1 = $product(2/1,sK0(12/1)) ) ),
introduced(definition,[new_symbols(definition,[spl1_4])],[avatar_definition]) ).
tff(f65,plain,
( spl1_4
| ~ spl1_1 ),
inference(avatar_split_clause,[],[f60,f33,f62]) ).
tff(f81,plain,
( ( 1/1 = sK0(12/1) )
| ( $product(2/1,sK0(sK0(12/1))) = sK0(12/1) )
| ~ spl1_3 ),
inference(resolution,[],[f54,f29]) ).
tff(f83,plain,
( ( 1/1 = sK0(12/1) )
| pow2(sK0(sK0(12/1)))
| ~ spl1_3 ),
inference(resolution,[],[f54,f28]) ).
tff(f86,definition,
( spl1_6
<=> ( 1/1 = sK0(12/1) ) ),
introduced(definition,[new_symbols(definition,[spl1_6])],[avatar_definition]) ).
tff(f90,definition,
( spl1_7
<=> pow2(sK0(sK0(12/1))) ),
introduced(definition,[new_symbols(definition,[spl1_7])],[avatar_definition]) ).
tff(f92,plain,
( pow2(sK0(sK0(12/1)))
| ~ spl1_7 ),
inference(avatar_component_clause,[],[f90]) ).
tff(f93,plain,
( spl1_6
| spl1_7
| ~ spl1_3 ),
inference(avatar_split_clause,[],[f83,f52,f90,f86]) ).
tff(f100,definition,
( spl1_9
<=> ( $product(2/1,sK0(sK0(12/1))) = sK0(12/1) ) ),
introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition]) ).
tff(f103,plain,
( spl1_6
| spl1_9
| ~ spl1_3 ),
inference(avatar_split_clause,[],[f81,f52,f100,f86]) ).
tff(f138,plain,
( ( sK0(sK0(12/1)) = $product(2/1,sK0(sK0(sK0(12/1)))) )
| ( 1/1 = sK0(sK0(12/1)) )
| ~ spl1_7 ),
inference(resolution,[],[f92,f29]) ).
tff(f140,plain,
( ( 1/1 = sK0(sK0(12/1)) )
| pow2(sK0(sK0(sK0(12/1))))
| ~ spl1_7 ),
inference(resolution,[],[f92,f28]) ).
tff(f142,definition,
( spl1_12
<=> ( 1/1 = sK0(sK0(12/1)) ) ),
introduced(definition,[new_symbols(definition,[spl1_12])],[avatar_definition]) ).
tff(f146,definition,
( spl1_13
<=> pow2(sK0(sK0(sK0(12/1)))) ),
introduced(definition,[new_symbols(definition,[spl1_13])],[avatar_definition]) ).
tff(f148,plain,
( pow2(sK0(sK0(sK0(12/1))))
| ~ spl1_13 ),
inference(avatar_component_clause,[],[f146]) ).
tff(f149,plain,
( spl1_12
| spl1_13
| ~ spl1_7 ),
inference(avatar_split_clause,[],[f140,f90,f146,f142]) ).
tff(f151,definition,
( spl1_14
<=> ( sK0(sK0(12/1)) = $product(2/1,sK0(sK0(sK0(12/1)))) ) ),
introduced(definition,[new_symbols(definition,[spl1_14])],[avatar_definition]) ).
tff(f154,plain,
( spl1_12
| spl1_14
| ~ spl1_7 ),
inference(avatar_split_clause,[],[f138,f90,f151,f142]) ).
tff(f330,plain,
( ~ $less(sK0(sK0(sK0(12/1))),2/1)
| ( 1/1 = sK0(sK0(sK0(12/1))) )
| ~ spl1_13 ),
inference(resolution,[],[f148,f30]) ).
tff(f334,definition,
( spl1_30
<=> ( 1/1 = sK0(sK0(sK0(12/1))) ) ),
introduced(definition,[new_symbols(definition,[spl1_30])],[avatar_definition]) ).
tff(f343,definition,
( spl1_32
<=> $less(sK0(sK0(sK0(12/1))),2/1) ),
introduced(definition,[new_symbols(definition,[spl1_32])],[avatar_definition]) ).
tff(f346,plain,
( spl1_30
| ~ spl1_32
| ~ spl1_13 ),
inference(avatar_split_clause,[],[f330,f146,f343,f334]) ).
tff(f352,plain,
$false,
inference(avatar_smt_refutation,[],[f346,f154,f149,f103,f93,f65,f55,f36]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ARI621_2 : TPTP v9.3.1. Released v5.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n007.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 20:51:55 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.92/1.70 % (2809784)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.92/1.70 % (2809929)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3359976810:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.92/1.70 % (2809926)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=282704712:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.92/1.70 % (2809926)Instruction limit reached!
% 5.92/1.70 % (2809926)------------------------------
% 5.92/1.70 % (2809926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.92/1.70 % (2809926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.70 % (2809926)CaDiCaL version: 2.1.3
% 5.92/1.70 % (2809926)Termination reason: Instruction limit
% 5.92/1.70 % (2809926)Termination phase: Saturation
% 5.92/1.70 % (2809926)Time elapsed: 0.006 s
% 5.92/1.70 % (2809926)Peak memory usage: 88 MB
% 5.92/1.70 % (2809926)Instructions burned: 7 (million)
% 5.92/1.70 % (2809920)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3853622505:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.92/1.70 % (2809929)Instruction limit reached!
% 5.92/1.70 % (2809929)------------------------------
% 5.92/1.70 % (2809929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.92/1.70 % (2809929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.70 % (2809929)CaDiCaL version: 2.1.3
% 5.92/1.70 % (2809929)Termination reason: Instruction limit
% 5.92/1.70 % (2809929)Termination phase: Saturation
% 5.92/1.70 % (2809929)Time elapsed: 0.039 s
% 5.92/1.70 % (2809929)Peak memory usage: 116 MB
% 5.92/1.70 % (2809929)Instructions burned: 33 (million)
% 5.92/1.70 % (2809923)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2101379882:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.92/1.70 % (2809927)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1187300560:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.92/1.70 % (2809924)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=693204420:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.92/1.70 % (2809928)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=4211071416:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.92/1.70 % (2809920)Instruction limit reached!
% 5.92/1.70 % (2809920)------------------------------
% 5.92/1.70 % (2809920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.92/1.70 % (2809920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.70 % (2809920)CaDiCaL version: 2.1.3
% 5.92/1.70 % (2809920)Termination reason: Instruction limit
% 5.92/1.70 % (2809920)Termination phase: Saturation
% 5.92/1.70 % (2809920)Time elapsed: 0.046 s
% 5.92/1.70 % (2809920)Peak memory usage: 115 MB
% 5.92/1.70 % (2809920)Instructions burned: 14 (million)
% 5.92/1.70 % (2809927)Instruction limit reached!
% 5.92/1.70 % (2809927)------------------------------
% 5.92/1.70 % (2809927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.92/1.70 % (2809927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.70 % (2809927)CaDiCaL version: 2.1.3
% 5.92/1.70 % (2809927)Termination reason: Instruction limit
% 5.92/1.70 % (2809927)Termination phase: Saturation
% 5.92/1.70 % (2809927)Time elapsed: 0.008 s
% 5.92/1.70 % (2809927)Peak memory usage: 88 MB
% 5.92/1.70 % (2809927)Instructions burned: 5 (million)
% 5.92/1.70 % (2809923)Refutation not found, incomplete strategy
% 5.92/1.70 % (2809923)------------------------------
% 5.92/1.70 % (2809923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.92/1.70 % (2809923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.70 % (2809923)CaDiCaL version: 2.1.3
% 5.92/1.70 % (2809923)Termination reason: Refutation not found, incomplete strategy
% 5.92/1.70 % (2809923)Time elapsed: 0.041 s
% 5.92/1.70 % (2809923)Peak memory usage: 114 MB
% 5.92/1.70 % (2809923)Instructions burned: 6 (million)
% 5.92/1.70 % (2809928)Instruction limit reached!
% 5.92/1.70 % (2809928)------------------------------
% 5.92/1.70 % (2809928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.92/1.70 % (2809928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.94 % (2809928)CaDiCaL version: 2.1.3
% 7.60/1.94 % (2809928)Termination reason: Instruction limit
% 7.60/1.94 % (2809928)Termination phase: Saturation
% 7.60/1.94 % (2809928)Time elapsed: 0.083 s
% 7.60/1.94 % (2809928)Peak memory usage: 115 MB
% 7.60/1.94 % (2809928)Instructions burned: 47 (million)
% 7.60/1.94 % (2809936)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2184398954:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 7.60/1.94 % (2809936)Instruction limit reached!
% 7.60/1.94 % (2809936)------------------------------
% 7.60/1.94 % (2809936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.60/1.94 % (2809936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.94 % (2809936)CaDiCaL version: 2.1.3
% 7.60/1.94 % (2809936)Termination reason: Instruction limit
% 7.60/1.94 % (2809936)Termination phase: Saturation
% 7.60/1.94 % (2809936)Time elapsed: 0.009 s
% 7.60/1.94 % (2809936)Peak memory usage: 88 MB
% 7.60/1.94 % (2809936)Instructions burned: 16 (million)
% 7.60/1.94 % (2809938)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=1046571873:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 7.60/1.94 % (2809938)Instruction limit reached!
% 7.60/1.94 % (2809938)------------------------------
% 7.60/1.94 % (2809938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.60/1.94 % (2809938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.94 % (2809938)CaDiCaL version: 2.1.3
% 7.60/1.94 % (2809938)Termination reason: Instruction limit
% 7.60/1.94 % (2809938)Termination phase: Saturation
% 7.60/1.94 % (2809938)Time elapsed: 0.029 s
% 7.60/1.94 % (2809938)Peak memory usage: 88 MB
% 7.60/1.94 % (2809938)Instructions burned: 29 (million)
% 7.60/1.94 % (2809924)Instruction limit reached!
% 7.60/1.94 % (2809924)------------------------------
% 7.60/1.94 % (2809924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.60/1.94 % (2809924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.94 % (2809924)CaDiCaL version: 2.1.3
% 7.60/1.94 % (2809924)Termination reason: Instruction limit
% 7.60/1.94 % (2809924)Termination phase: Saturation
% 7.60/1.94 % (2809924)Time elapsed: 0.267 s
% 7.60/1.94 % (2809924)Peak memory usage: 117 MB
% 7.60/1.94 % (2809924)Instructions burned: 203 (million)
% 7.60/1.94 % (2809944)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1489420283:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 7.60/1.94 % (2809943)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4260504833:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 7.60/1.94 % (2809943)Refutation not found, incomplete strategy
% 7.60/1.94 % (2809943)------------------------------
% 7.60/1.94 % (2809943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.60/1.94 % (2809943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.94 % (2809943)CaDiCaL version: 2.1.3
% 7.60/1.94 % (2809943)Termination reason: Refutation not found, incomplete strategy
% 7.60/1.94 % (2809943)Time elapsed: 0.014 s
% 7.60/1.94 % (2809943)Peak memory usage: 90 MB
% 7.60/1.94 % (2809943)Instructions burned: 12 (million)
% 7.60/1.94 % (2809946)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=2394893322:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 7.60/1.94 % (2809944)Instruction limit reached!
% 7.60/1.94 % (2809944)------------------------------
% 7.60/1.94 % (2809944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.60/1.94 % (2809944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.94 % (2809944)CaDiCaL version: 2.1.3
% 7.60/1.94 % (2809944)Termination reason: Instruction limit
% 7.60/1.94 % (2809944)Termination phase: Saturation
% 7.60/1.94 % (2809944)Time elapsed: 0.029 s
% 7.60/1.94 % (2809944)Peak memory usage: 89 MB
% 7.60/1.94 % (2809944)Instructions burned: 24 (million)
% 7.60/1.94 % (2809946)Instruction limit reached!
% 7.60/1.94 % (2809946)------------------------------
% 7.60/1.94 % (2809946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.60/1.94 % (2809946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.21 % (2809946)CaDiCaL version: 2.1.3
% 10.46/2.21 % (2809946)Termination reason: Instruction limit
% 10.46/2.21 % (2809946)Termination phase: Saturation
% 10.46/2.21 % (2809946)Time elapsed: 0.014 s
% 10.46/2.21 % (2809946)Peak memory usage: 89 MB
% 10.46/2.21 % (2809946)Instructions burned: 29 (million)
% 10.46/2.21 % (2809923)------------------------------
% 10.46/2.21 % (2809923)------------------------------
% 10.46/2.21 % (2809950)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1707443905:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi)
% 10.46/2.21 % (2809959)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3956935644:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi)
% 10.46/2.21 % (2809959)Instruction limit reached!
% 10.46/2.21 % (2809959)------------------------------
% 10.46/2.21 % (2809959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.21 % (2809959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.21 % (2809959)CaDiCaL version: 2.1.3
% 10.46/2.21 % (2809959)Termination reason: Instruction limit
% 10.46/2.21 % (2809959)Termination phase: Saturation
% 10.46/2.21 % (2809959)Time elapsed: 0.004 s
% 10.46/2.21 % (2809959)Peak memory usage: 89 MB
% 10.46/2.21 % (2809959)Instructions burned: 2 (million)
% 10.46/2.21 % (2809950)Instruction limit reached!
% 10.46/2.21 % (2809950)------------------------------
% 10.46/2.21 % (2809950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.21 % (2809950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.21 % (2809950)CaDiCaL version: 2.1.3
% 10.46/2.21 % (2809950)Termination reason: Instruction limit
% 10.46/2.21 % (2809950)Termination phase: Saturation
% 10.46/2.21 % (2809950)Time elapsed: 0.090 s
% 10.46/2.21 % (2809950)Peak memory usage: 89 MB
% 10.46/2.21 % (2809950)Instructions burned: 86 (million)
% 10.46/2.21 % (2809965)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=114257521:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 10.46/2.21 % (2809962)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1870695860:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 10.46/2.21 % (2809962)Refutation not found, incomplete strategy
% 10.46/2.21 % (2809962)------------------------------
% 10.46/2.21 % (2809962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.21 % (2809962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.21 % (2809962)CaDiCaL version: 2.1.3
% 10.46/2.21 % (2809962)Termination reason: Refutation not found, incomplete strategy
% 10.46/2.21 % (2809962)Time elapsed: 0.002 s
% 10.46/2.21 % (2809962)Peak memory usage: 89 MB
% 10.46/2.21 % (2809962)Instructions burned: 1 (million)
% 10.46/2.21 % (2809964)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=962318857:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 10.46/2.21 % (2809965)Instruction limit reached!
% 10.46/2.21 % (2809965)------------------------------
% 10.46/2.21 % (2809965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.21 % (2809965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.21 % (2809965)CaDiCaL version: 2.1.3
% 10.46/2.21 % (2809965)Termination reason: Instruction limit
% 10.46/2.21 % (2809965)Termination phase: Saturation
% 10.46/2.21 % (2809965)Time elapsed: 0.074 s
% 10.46/2.21 % (2809965)Peak memory usage: 133 MB
% 10.46/2.21 % (2809965)Instructions burned: 67 (million)
% 10.46/2.21 % (2809964)Instruction limit reached!
% 10.46/2.21 % (2809964)------------------------------
% 10.46/2.21 % (2809964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.21 % (2809964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.21 % (2809964)CaDiCaL version: 2.1.3
% 10.46/2.21 % (2809964)Termination reason: Instruction limit
% 10.46/2.21 % (2809964)Termination phase: Saturation
% 10.46/2.21 % (2809964)Time elapsed: 0.006 s
% 10.46/2.21 % (2809964)Peak memory usage: 88 MB
% 10.46/2.21 % (2809964)Instructions burned: 4 (million)
% 10.46/2.21 % (2809966)lrs+10_1_thi=all:si=on:fd=off:random_seed=3623718635:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi)
% 10.46/2.21 % (2809943)------------------------------
% 10.46/2.21 % (2809943)------------------------------
% 10.46/2.21 % (2809966)Instruction limit reached!
% 10.46/2.21 % (2809966)------------------------------
% 10.46/2.21 % (2809966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.36 % (2809966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.36 % (2809966)CaDiCaL version: 2.1.3
% 10.93/2.36 % (2809966)Termination reason: Instruction limit
% 10.93/2.36 % (2809966)Termination phase: Saturation
% 10.93/2.36 % (2809966)Time elapsed: 0.093 s
% 10.93/2.36 % (2809966)Peak memory usage: 116 MB
% 10.93/2.36 % (2809966)Instructions burned: 54 (million)
% 10.93/2.36 % (2809977)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1649495918:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi)
% 10.93/2.36 % (2809977)Instruction limit reached!
% 10.93/2.36 % (2809977)------------------------------
% 10.93/2.36 % (2809977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.36 % (2809977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.36 % (2809977)CaDiCaL version: 2.1.3
% 10.93/2.36 % (2809977)Termination reason: Instruction limit
% 10.93/2.36 % (2809977)Termination phase: Saturation
% 10.93/2.36 % (2809977)Time elapsed: 0.003 s
% 10.93/2.36 % (2809977)Peak memory usage: 90 MB
% 10.93/2.36 % (2809977)Instructions burned: 3 (million)
% 10.93/2.36 % (2809974)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=435702413:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/8Mi)
% 10.93/2.36 % (2809974)Instruction limit reached!
% 10.93/2.36 % (2809974)------------------------------
% 10.93/2.36 % (2809974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.36 % (2809974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.36 % (2809974)CaDiCaL version: 2.1.3
% 10.93/2.36 % (2809974)Termination reason: Instruction limit
% 10.93/2.36 % (2809974)Termination phase: Saturation
% 10.93/2.36 % (2809974)Time elapsed: 0.011 s
% 10.93/2.36 % (2809974)Peak memory usage: 88 MB
% 10.93/2.36 % (2809974)Instructions burned: 8 (million)
% 10.93/2.36 % (2809985)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=29426854:i=2:doe=on:canc=force:asg=cautious:rtra=on_2991 on theBenchmark for (2991ds/2Mi)
% 10.93/2.36 % (2809985)Instruction limit reached!
% 10.93/2.36 % (2809985)------------------------------
% 10.93/2.36 % (2809985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.36 % (2809985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.36 % (2809985)CaDiCaL version: 2.1.3
% 10.93/2.36 % (2809985)Termination reason: Instruction limit
% 10.93/2.36 % (2809985)Termination phase: Saturation
% 10.93/2.36 % (2809985)Time elapsed: 0.004 s
% 10.93/2.36 % (2809985)Peak memory usage: 89 MB
% 10.93/2.36 % (2809985)Instructions burned: 2 (million)
% 10.93/2.36 % (2809986)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2201097250:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi)
% 10.93/2.36 % (2809962)------------------------------
% 10.93/2.36 % (2809962)------------------------------
% 10.93/2.36 % (2809993)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1849695553:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2989 on theBenchmark for (2989ds/35Mi)
% 10.93/2.36 % (2809989)dis+10_1_si=on:random_seed=4145653113:i=10:ep=R:rtra=on_2990 on theBenchmark for (2990ds/10Mi)
% 10.93/2.36 % (2809990)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3736782593:i=26:canc=cautious:av=off:rtra=on_2990 on theBenchmark for (2990ds/26Mi)
% 10.93/2.36 % (2809986)First to succeed.
% 10.93/2.36 % (2809986)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2809784"
% 10.93/2.36 % (2809990)Refutation not found, incomplete strategy
% 10.93/2.36 % (2809990)------------------------------
% 10.93/2.36 % (2809990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.36 % (2809990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.36 % (2809990)CaDiCaL version: 2.1.3
% 10.93/2.36 % (2809990)Termination reason: Refutation not found, incomplete strategy
% 10.93/2.36 % (2809990)Time elapsed: 0.003 s
% 10.93/2.36 % (2809990)Peak memory usage: 89 MB
% 10.93/2.36 % (2809990)Instructions burned: 1 (million)
% 10.93/2.36 % (2809993)Instruction limit reached!
% 10.93/2.36 % (2809993)------------------------------
% 10.93/2.36 % (2809993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.36 % (2809993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.62 % (2809993)CaDiCaL version: 2.1.3
% 12.10/2.62 % (2809993)Termination reason: Instruction limit
% 12.10/2.62 % (2809993)Termination phase: Saturation
% 12.10/2.62 % (2809993)Time elapsed: 0.030 s
% 12.10/2.62 % (2809993)Peak memory usage: 89 MB
% 12.10/2.62 % (2809993)Instructions burned: 36 (million)
% 12.10/2.62 % (2809989)Instruction limit reached!
% 12.10/2.62 % (2809989)------------------------------
% 12.10/2.62 % (2809989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.62 % (2809989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.62 % (2809989)CaDiCaL version: 2.1.3
% 12.10/2.62 % (2809989)Termination reason: Instruction limit
% 12.10/2.62 % (2809989)Termination phase: Saturation
% 12.10/2.62 % (2809989)Time elapsed: 0.012 s
% 12.10/2.62 % (2809989)Peak memory usage: 88 MB
% 12.10/2.62 % (2809989)Instructions burned: 10 (million)
% 12.10/2.62 % (2809994)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2111241035:i=2:fsr=off:rtra=on:inst=on_2989 on theBenchmark for (2989ds/2Mi)
% 12.10/2.62 % (2809994)Instruction limit reached!
% 12.10/2.62 % (2809994)------------------------------
% 12.10/2.62 % (2809994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.62 % (2809994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.62 % (2809994)CaDiCaL version: 2.1.3
% 12.10/2.62 % (2809994)Termination reason: Instruction limit
% 12.10/2.62 % (2809994)Termination phase: Saturation
% 12.10/2.62 % (2809994)Time elapsed: 0.005 s
% 12.10/2.62 % (2809994)Peak memory usage: 89 MB
% 12.10/2.62 % (2809994)Instructions burned: 2 (million)
% 12.10/2.62 % (2809996)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3246456995:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2989 on theBenchmark for (2989ds/8Mi)
% 12.10/2.62 % (2809996)Instruction limit reached!
% 12.10/2.62 % (2809996)------------------------------
% 12.10/2.62 % (2809996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.62 % (2809996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.62 % (2809996)CaDiCaL version: 2.1.3
% 12.10/2.62 % (2809996)Termination reason: Instruction limit
% 12.10/2.62 % (2809996)Termination phase: Saturation
% 12.10/2.62 % (2809996)Time elapsed: 0.012 s
% 12.10/2.62 % (2809996)Peak memory usage: 89 MB
% 12.10/2.62 % (2809996)Instructions burned: 8 (million)
% 12.10/2.62 % (2809998)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1052627065:i=370:ep=RS:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/370Mi)
% 12.10/2.62 % (2809998)Refutation not found, incomplete strategy
% 12.10/2.62 % (2809998)------------------------------
% 12.10/2.62 % (2809998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.62 % (2809998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.62 % (2809998)CaDiCaL version: 2.1.3
% 12.10/2.62 % (2809998)Termination reason: Refutation not found, incomplete strategy
% 12.10/2.62 % (2809998)Time elapsed: 0.002 s
% 12.10/2.62 % (2809998)Peak memory usage: 88 MB
% 12.10/2.62 % (2810003)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1498909774:i=226:rtra=on:gtg=position:ss=axioms_2987 on theBenchmark for (2987ds/226Mi)
% 12.10/2.62 % (2810003)Refutation not found, incomplete strategy
% 12.10/2.62 % (2810003)------------------------------
% 12.10/2.62 % (2810003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.62 % (2810003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.62 % (2810003)CaDiCaL version: 2.1.3
% 12.10/2.62 % (2810003)Termination reason: Refutation not found, incomplete strategy
% 12.10/2.62 % (2810003)Time elapsed: 0.024 s
% 12.10/2.62 % (2810003)Peak memory usage: 115 MB
% 12.10/2.62 % (2810003)Instructions burned: 6 (million)
% 12.10/2.62 % (2810005)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2232127682:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi)
% 12.10/2.62 % (2810002)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3475806659:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2987 on theBenchmark for (2987ds/13Mi)
% 12.10/2.62 % (2810005)Refutation not found, incomplete strategy
% 12.10/2.62 % (2810005)------------------------------
% 12.10/2.62 % (2810005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.62 % (2810005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.62 % (2810005)CaDiCaL version: 2.1.3
% 12.10/2.62 % (2810005)Termination reason: Refutation not found, incomplete strategy
% 12.10/2.62 % (2810005)Time elapsed: 0.003 s
% 12.10/2.62 % (2810005)Peak memory usage: 88 MB
% 12.10/2.62 % (2810002)Instruction limit reached!
% 12.10/2.62 % (2810002)------------------------------
% 12.10/2.62 % (2810002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.62 % (2810002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.62 % (2810002)CaDiCaL version: 2.1.3
% 12.10/2.62 % (2810002)Termination reason: Instruction limit
% 12.10/2.62 % (2810002)Termination phase: Saturation
% 12.10/2.62 % (2810002)Time elapsed: 0.047 s
% 12.10/2.62 % (2810002)Peak memory usage: 116 MB
% 12.10/2.62 % (2810002)Instructions burned: 13 (million)
% 12.10/2.62 % (2809990)------------------------------
% 12.10/2.62 % (2809990)------------------------------
% 12.10/2.62 % (2809986)Refutation found. Thanks to Tanya!
% 12.10/2.62 % SZS status Theorem for theBenchmark
% 12.10/2.62 % SZS output start Proof for theBenchmark
% See solution above
% 12.10/2.62 % (2809986)------------------------------
% 12.10/2.62 % (2809986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.62 % (2809986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.62 % (2809986)CaDiCaL version: 2.1.3
% 12.10/2.62 % (2809986)Termination reason: Refutation
% 12.10/2.62 % (2809986)Time elapsed: 0.092 s
% 12.10/2.62 % (2809986)Peak memory usage: 117 MB
% 12.10/2.62 % (2809986)Instructions burned: 48 (million)
% 12.10/2.62 % (2809986)------------------------------
% 12.10/2.62 % (2809986)------------------------------
% 12.10/2.62 % (2809784)Success in time 1.617 s
% 12.10/2.62 % Vampire exiting
%------------------------------------------------------------------------------