%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PLA060_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 12:28:32 PM UTC 2026
% Result : Theorem 11.14s 2.54s
% Output : Refutation 11.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 4
% Syntax : Number of formulae : 32 ( 1 unt; 0 typ; 0 def)
% Number of atoms : 103 ( 6 equ)
% Maximal formula atoms : 4 ( 3 avg)
% Number of connectives : 100 ( 29 ~; 43 |; 14 &)
% ( 0 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number arithmetic : 186 ( 44 atm; 10 fun; 49 num; 83 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 : 10 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 2 usr; 6 con; 0-2 aty)
% Number of variables : 83 ( 75 !; 8 ?; 83 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_8,type,
'$inst0': $int ).
tff(func_def_9,type,
'$inst1': $int ).
tff(pred_def_1,type,
s0: ( $int * $int ) > $o ).
tff(pred_def_2,type,
s1: ( $int * $int ) > $o ).
tff(pred_def_3,type,
s2: ( $int * $int ) > $o ).
tff(pred_def_4,type,
s3: ( $int * $int ) > $o ).
tff(pred_def_5,type,
s4: ( $int * $int ) > $o ).
tff(f2,axiom,
! [X0: $int,X1: $int] :
( ( $lesseq(X0,200)
& s0(X0,X1) )
=> s3(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
tff(f4,axiom,
! [X0: $int,X1: $int,X2: $int] :
( ( s3(X0,X1)
& $greatereq(X2,0)
& $lesseq(X2,40) )
=> s4(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
tff(f6,axiom,
! [X1: $int,X2: $int,X0: $int] :
( ( ( X2 = $sum(X0,X1) )
& s4(X0,X1) )
=> s0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
tff(f7,conjecture,
( ! [X1: $int,X0: $int] :
( $lesseq(X0,200)
=> s0(X0,X1) )
=> ? [X2: $int,X3: $int] :
( s0(X2,X3)
& $greatereq(X2,240) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj1) ).
tff(f8,negated_conjecture,
~ ( ! [X1: $int,X0: $int] :
( $lesseq(X0,200)
=> s0(X0,X1) )
=> ? [X2: $int,X3: $int] :
( s0(X2,X3)
& $greatereq(X2,240) ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
tff(f10,plain,
! [X0: $int,X2: $int,X1: $int] :
( ( s3(X0,X1)
& ~ $less(X2,0)
& ~ $less(40,X2) )
=> s4(X0,X2) ),
inference(theory_normalization,[],[f4]) ).
tff(f12,plain,
~ ( ! [X1: $int,X0: $int] :
( ~ $less(200,X0)
=> s0(X0,X1) )
=> ? [X2: $int,X3: $int] :
( ~ $less(X2,240)
& s0(X2,X3) ) ),
inference(theory_normalization,[],[f8]) ).
tff(f13,plain,
! [X0: $int,X1: $int] :
( ( ~ $less(200,X0)
& s0(X0,X1) )
=> s3(X0,X1) ),
inference(theory_normalization,[],[f2]) ).
tff(f16,plain,
! [X0: $int,X2: $int,X1: $int] :
( ( ( $sum(X2,X0) = X1 )
& s4(X2,X0) )
=> s0(X1,X0) ),
inference(rectify,[],[f6]) ).
tff(f18,plain,
~ ( ! [X1: $int,X0: $int] :
( ~ $less(200,X1)
=> s0(X1,X0) )
=> ? [X2: $int,X3: $int] :
( ~ $less(X2,240)
& s0(X2,X3) ) ),
inference(rectify,[],[f12]) ).
tff(f24,plain,
! [X0: $int,X2: $int,X1: $int] :
( s0(X1,X0)
| ( $sum(X2,X0) != X1 )
| ~ s4(X2,X0) ),
inference(ennf_transformation,[],[f16]) ).
tff(f25,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ s4(X2,X0)
| s0(X1,X0)
| ( $sum(X2,X0) != X1 ) ),
inference(flattening,[],[f24]) ).
tff(f26,plain,
! [X0: $int,X1: $int] :
( s3(X0,X1)
| $less(200,X0)
| ~ s0(X0,X1) ),
inference(ennf_transformation,[],[f13]) ).
tff(f27,plain,
! [X0: $int,X1: $int] :
( s3(X0,X1)
| $less(200,X0)
| ~ s0(X0,X1) ),
inference(flattening,[],[f26]) ).
tff(f28,plain,
( ! [X1: $int,X0: $int] :
( s0(X1,X0)
| $less(200,X1) )
& ! [X2: $int,X3: $int] :
( ~ s0(X2,X3)
| $less(X2,240) ) ),
inference(ennf_transformation,[],[f18]) ).
tff(f31,plain,
! [X0: $int,X2: $int,X1: $int] :
( s4(X0,X2)
| ~ s3(X0,X1)
| $less(X2,0)
| $less(40,X2) ),
inference(ennf_transformation,[],[f10]) ).
tff(f32,plain,
! [X0: $int,X1: $int,X2: $int] :
( ~ s3(X0,X1)
| $less(40,X2)
| $less(X2,0)
| s4(X0,X2) ),
inference(flattening,[],[f31]) ).
tff(f34,plain,
! [X0: $int,X1: $int,X2: $int] :
( ~ s4(X0,X1)
| s0(X2,X1)
| ( $sum(X0,X1) != X2 ) ),
inference(rectify,[],[f25]) ).
tff(f36,plain,
( ! [X0: $int,X1: $int] :
( s0(X0,X1)
| $less(200,X0) )
& ! [X2: $int,X3: $int] :
( ~ s0(X2,X3)
| $less(X2,240) ) ),
inference(rectify,[],[f28]) ).
tff(f39,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ s4(X0,X1)
| s0(X2,X1)
| ( $sum(X0,X1) != X2 ) ),
inference(cnf_transformation,[],[f34]) ).
tff(f40,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ s3(X0,X1)
| $less(40,X2)
| $less(X2,0)
| s4(X0,X2) ),
inference(cnf_transformation,[],[f32]) ).
tff(f42,plain,
! [X2: $int,X3: $int] :
( ~ s0(X2,X3)
| $less(X2,240) ),
inference(cnf_transformation,[],[f36]) ).
tff(f43,plain,
! [X0: $int,X1: $int] :
( s0(X0,X1)
| $less(200,X0) ),
inference(cnf_transformation,[],[f36]) ).
tff(f44,plain,
! [X0: $int,X1: $int] :
( ~ s0(X0,X1)
| $less(200,X0)
| s3(X0,X1) ),
inference(cnf_transformation,[],[f27]) ).
tff(f46,plain,
! [X0: $int,X1: $int] :
( s0($sum(X0,X1),X1)
| ~ s4(X0,X1) ),
inference(equality_resolution,[],[f39]) ).
tff(f55,plain,
! [X0: $int,X1: $int] :
( ~ s4(X0,X1)
| $less($sum(X0,X1),240) ),
inference(resolution,[],[f46,f42]) ).
tff(f59,plain,
! [X0: $int,X1: $int] :
( s3(X0,X1)
| $less(200,X0)
| $less(200,X0) ),
inference(resolution,[],[f44,f43]) ).
tff(f63,plain,
! [X0: $int,X1: $int] :
( s3(X0,X1)
| $less(200,X0) ),
inference(duplicate_literal_removal,[],[f59]) ).
tff(f87,plain,
! [X0: $int,X1: $int] :
( s4(X1,X0)
| $less(X0,0)
| $less(200,X1)
| $less(40,X0) ),
inference(resolution,[],[f40,f63]) ).
tff(f151,plain,
! [X0: $int,X1: $int] :
( $less($sum(X1,X0),240)
| $less(X0,0)
| $less(40,X0)
| $less(200,X1) ),
inference(resolution,[],[f87,f55]) ).
tff(f167,plain,
( $less($sum(200,40),240)
| $less(40,0)
| $less(40,40)
| $less(200,200) ),
inference(instantiation,[],[f151]) ).
tff(f168,plain,
$false,
inference(interpreted_simplification,[],[f167]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PLA060_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n002.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 22:18:36 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 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
% 3.71/1.45 % (3945473)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.71/1.45 % (3945481)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2503480785:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.71/1.45 % (3945481)Instruction limit reached!
% 3.71/1.45 % (3945481)------------------------------
% 3.71/1.45 % (3945481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.71/1.45 % (3945481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.71/1.45 % (3945481)CaDiCaL version: 2.1.3
% 3.71/1.45 % (3945481)Termination reason: Instruction limit
% 3.71/1.45 % (3945481)Termination phase: Saturation
% 3.71/1.45 % (3945481)Time elapsed: 0.004 s
% 3.71/1.45 % (3945481)Peak memory usage: 88 MB
% 3.71/1.45 % (3945481)Instructions burned: 10 (million)
% 3.71/1.45 % (3945484)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=531274413:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.71/1.45 % (3945482)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2862610550:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.71/1.45 % (3945478)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2086305289:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.71/1.45 % (3945479)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1933837920:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.71/1.45 % (3945480)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2498685550:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.71/1.45 % (3945483)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1247944996:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.71/1.45 % (3945482)Instruction limit reached!
% 3.71/1.45 % (3945482)------------------------------
% 3.71/1.45 % (3945482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.71/1.45 % (3945482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.71/1.45 % (3945482)CaDiCaL version: 2.1.3
% 3.71/1.45 % (3945482)Termination reason: Instruction limit
% 3.71/1.45 % (3945482)Termination phase: Saturation
% 3.71/1.45 % (3945482)Time elapsed: 0.005 s
% 3.71/1.45 % (3945482)Peak memory usage: 88 MB
% 3.71/1.45 % (3945482)Instructions burned: 5 (million)
% 3.71/1.45 % (3945479)Refutation not found, incomplete strategy
% 3.71/1.45 % (3945479)------------------------------
% 3.71/1.45 % (3945479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.71/1.45 % (3945479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.71/1.45 % (3945479)CaDiCaL version: 2.1.3
% 3.71/1.45 % (3945479)Termination reason: Refutation not found, incomplete strategy
% 3.71/1.45 % (3945479)Time elapsed: 0.027 s
% 3.71/1.45 % (3945479)Peak memory usage: 112 MB
% 3.71/1.45 % (3945479)Instructions burned: 5 (million)
% 3.71/1.45 % (3945478)Refutation not found, incomplete strategy
% 3.71/1.45 % (3945478)------------------------------
% 3.71/1.45 % (3945478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.71/1.45 % (3945478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.71/1.45 % (3945478)CaDiCaL version: 2.1.3
% 3.71/1.45 % (3945478)Termination reason: Refutation not found, incomplete strategy
% 3.71/1.45 % (3945478)Time elapsed: 0.027 s
% 3.71/1.45 % (3945478)Peak memory usage: 112 MB
% 3.71/1.45 % (3945478)Instructions burned: 6 (million)
% 3.71/1.45 % (3945484)Instruction limit reached!
% 3.71/1.45 % (3945484)------------------------------
% 3.71/1.45 % (3945484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.71/1.45 % (3945484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.71/1.45 % (3945484)CaDiCaL version: 2.1.3
% 3.71/1.45 % (3945484)Termination reason: Instruction limit
% 3.71/1.45 % (3945484)Termination phase: Saturation
% 3.71/1.45 % (3945484)Time elapsed: 0.045 s
% 3.71/1.45 % (3945484)Peak memory usage: 115 MB
% 3.71/1.45 % (3945484)Instructions burned: 33 (million)
% 3.71/1.45 % (3945483)Instruction limit reached!
% 3.71/1.45 % (3945483)------------------------------
% 3.71/1.45 % (3945483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.71/1.45 % (3945483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.63 % (3945483)CaDiCaL version: 2.1.3
% 4.73/1.63 % (3945483)Termination reason: Instruction limit
% 4.73/1.63 % (3945483)Termination phase: Saturation
% 4.73/1.63 % (3945483)Time elapsed: 0.047 s
% 4.73/1.63 % (3945483)Peak memory usage: 111 MB
% 4.73/1.63 % (3945483)Instructions burned: 48 (million)
% 4.73/1.63 % (3945486)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2736152703:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.73/1.63 % (3945486)Instruction limit reached!
% 4.73/1.63 % (3945486)------------------------------
% 4.73/1.63 % (3945486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.63 % (3945486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.63 % (3945486)CaDiCaL version: 2.1.3
% 4.73/1.63 % (3945486)Termination reason: Instruction limit
% 4.73/1.63 % (3945486)Termination phase: Saturation
% 4.73/1.63 % (3945486)Time elapsed: 0.005 s
% 4.73/1.63 % (3945486)Peak memory usage: 88 MB
% 4.73/1.63 % (3945486)Instructions burned: 17 (million)
% 4.73/1.63 % (3945493)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=2905089376:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.73/1.63 % (3945480)Instruction limit reached!
% 4.73/1.63 % (3945480)------------------------------
% 4.73/1.63 % (3945480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.63 % (3945480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.63 % (3945480)CaDiCaL version: 2.1.3
% 4.73/1.63 % (3945480)Termination reason: Instruction limit
% 4.73/1.63 % (3945480)Termination phase: Saturation
% 4.73/1.63 % (3945480)Time elapsed: 0.174 s
% 4.73/1.63 % (3945480)Peak memory usage: 117 MB
% 4.73/1.63 % (3945480)Instructions burned: 202 (million)
% 4.73/1.63 % (3945493)Instruction limit reached!
% 4.73/1.63 % (3945493)------------------------------
% 4.73/1.63 % (3945493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.63 % (3945493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.63 % (3945493)CaDiCaL version: 2.1.3
% 4.73/1.63 % (3945493)Termination reason: Instruction limit
% 4.73/1.64 % (3945493)Termination phase: Saturation
% 4.73/1.64 % (3945493)Time elapsed: 0.020 s
% 4.73/1.64 % (3945493)Peak memory usage: 88 MB
% 4.73/1.64 % (3945493)Instructions burned: 30 (million)
% 4.73/1.64 % (3945495)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2289171968:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.73/1.64 % (3945494)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=56755373:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.73/1.64 % (3945497)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=2128878495:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.73/1.64 % (3945494)Instruction limit reached!
% 4.73/1.64 % (3945494)------------------------------
% 4.73/1.64 % (3945494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.64 % (3945494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.64 % (3945494)CaDiCaL version: 2.1.3
% 4.73/1.64 % (3945494)Termination reason: Instruction limit
% 4.73/1.64 % (3945494)Termination phase: Saturation
% 4.73/1.64 % (3945494)Time elapsed: 0.009 s
% 4.73/1.64 % (3945494)Peak memory usage: 90 MB
% 4.73/1.64 % (3945494)Instructions burned: 17 (million)
% 4.73/1.64 % (3945495)Instruction limit reached!
% 4.73/1.64 % (3945495)------------------------------
% 4.73/1.64 % (3945495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.64 % (3945495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.64 % (3945495)CaDiCaL version: 2.1.3
% 4.73/1.64 % (3945495)Termination reason: Instruction limit
% 4.73/1.64 % (3945495)Termination phase: Saturation
% 4.73/1.64 % (3945495)Time elapsed: 0.017 s
% 4.73/1.64 % (3945495)Peak memory usage: 89 MB
% 4.73/1.64 % (3945495)Instructions burned: 24 (million)
% 4.73/1.64 % (3945497)Instruction limit reached!
% 4.73/1.64 % (3945497)------------------------------
% 4.73/1.64 % (3945497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.64 % (3945497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.90/1.81 % (3945497)CaDiCaL version: 2.1.3
% 5.90/1.81 % (3945497)Termination reason: Instruction limit
% 5.90/1.81 % (3945497)Termination phase: Saturation
% 5.90/1.81 % (3945497)Time elapsed: 0.011 s
% 5.90/1.81 % (3945497)Peak memory usage: 89 MB
% 5.90/1.81 % (3945497)Instructions burned: 29 (million)
% 5.90/1.81 % (3945478)------------------------------
% 5.90/1.81 % (3945478)------------------------------
% 5.90/1.81 % (3945479)------------------------------
% 5.90/1.81 % (3945479)------------------------------
% 5.90/1.81 % (3945499)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2292106709:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 5.90/1.81 % (3945505)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2243060048:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.90/1.81 % (3945505)Instruction limit reached!
% 5.90/1.81 % (3945505)------------------------------
% 5.90/1.81 % (3945505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.90/1.81 % (3945505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.90/1.81 % (3945505)CaDiCaL version: 2.1.3
% 5.90/1.81 % (3945505)Termination reason: Instruction limit
% 5.90/1.81 % (3945505)Termination phase: Saturation
% 5.90/1.81 % (3945505)Time elapsed: 0.003 s
% 5.90/1.81 % (3945505)Peak memory usage: 88 MB
% 5.90/1.81 % (3945505)Instructions burned: 7 (million)
% 5.90/1.81 % (3945502)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3878037312:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.90/1.81 % (3945502)Instruction limit reached!
% 5.90/1.81 % (3945502)------------------------------
% 5.90/1.81 % (3945502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.90/1.81 % (3945502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.90/1.81 % (3945502)CaDiCaL version: 2.1.3
% 5.90/1.81 % (3945502)Termination reason: Instruction limit
% 5.90/1.81 % (3945502)Termination phase: Saturation
% 5.90/1.81 % (3945502)Time elapsed: 0.003 s
% 5.90/1.81 % (3945502)Peak memory usage: 88 MB
% 5.90/1.81 % (3945502)Instructions burned: 3 (million)
% 5.90/1.81 % (3945504)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2024961144:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.90/1.81 % (3945504)Refutation not found, incomplete strategy
% 5.90/1.81 % (3945504)------------------------------
% 5.90/1.81 % (3945504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.90/1.81 % (3945504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.90/1.81 % (3945504)CaDiCaL version: 2.1.3
% 5.90/1.81 % (3945504)Termination reason: Refutation not found, incomplete strategy
% 5.90/1.81 % (3945504)Time elapsed: 0.001 s
% 5.90/1.81 % (3945504)Peak memory usage: 88 MB
% 5.90/1.81 % (3945506)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3222844358:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.90/1.81 % (3945499)Instruction limit reached!
% 5.90/1.81 % (3945499)------------------------------
% 5.90/1.81 % (3945499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.90/1.81 % (3945499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.90/1.81 % (3945499)CaDiCaL version: 2.1.3
% 5.90/1.81 % (3945499)Termination reason: Instruction limit
% 5.90/1.81 % (3945499)Termination phase: Saturation
% 5.90/1.81 % (3945499)Time elapsed: 0.059 s
% 5.90/1.81 % (3945499)Peak memory usage: 89 MB
% 5.90/1.81 % (3945499)Instructions burned: 86 (million)
% 5.90/1.81 % (3945507)lrs+10_1_thi=all:si=on:fd=off:random_seed=1588095330:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 5.90/1.81 % (3945508)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=1023718029:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 5.90/1.81 % (3945512)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3056995882:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.90/1.81 % (3945512)Instruction limit reached!
% 5.90/1.81 % (3945512)------------------------------
% 5.90/1.81 % (3945512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.90/1.81 % (3945512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.86/2.07 % (3945512)CaDiCaL version: 2.1.3
% 8.86/2.07 % (3945512)Termination reason: Instruction limit
% 8.86/2.07 % (3945512)Termination phase: Saturation
% 8.86/2.07 % (3945512)Time elapsed: 0.002 s
% 8.86/2.07 % (3945512)Peak memory usage: 90 MB
% 8.86/2.07 % (3945512)Instructions burned: 5 (million)
% 8.86/2.07 % (3945508)Instruction limit reached!
% 8.86/2.07 % (3945508)------------------------------
% 8.86/2.07 % (3945508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.86/2.07 % (3945508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.86/2.07 % (3945508)CaDiCaL version: 2.1.3
% 8.86/2.07 % (3945508)Termination reason: Instruction limit
% 8.86/2.07 % (3945508)Termination phase: Saturation
% 8.86/2.07 % (3945508)Time elapsed: 0.007 s
% 8.86/2.07 % (3945508)Peak memory usage: 88 MB
% 8.86/2.07 % (3945508)Instructions burned: 9 (million)
% 8.86/2.07 % (3945506)Instruction limit reached!
% 8.86/2.07 % (3945506)------------------------------
% 8.86/2.07 % (3945506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.86/2.07 % (3945506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.86/2.07 % (3945506)CaDiCaL version: 2.1.3
% 8.86/2.07 % (3945506)Termination reason: Instruction limit
% 8.86/2.07 % (3945506)Termination phase: Saturation
% 8.86/2.07 % (3945506)Time elapsed: 0.096 s
% 8.86/2.07 % (3945506)Peak memory usage: 133 MB
% 8.86/2.07 % (3945506)Instructions burned: 67 (million)
% 8.86/2.07 % (3945513)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1344513480:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi)
% 8.86/2.07 % (3945513)Instruction limit reached!
% 8.86/2.07 % (3945513)------------------------------
% 8.86/2.07 % (3945513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.86/2.07 % (3945513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.86/2.07 % (3945513)CaDiCaL version: 2.1.3
% 8.86/2.07 % (3945513)Termination reason: Instruction limit
% 8.86/2.07 % (3945513)Termination phase: Saturation
% 8.86/2.07 % (3945513)Time elapsed: 0.002 s
% 8.86/2.07 % (3945513)Peak memory usage: 89 MB
% 8.86/2.07 % (3945513)Instructions burned: 2 (million)
% 8.86/2.07 % (3945507)Instruction limit reached!
% 8.86/2.07 % (3945507)------------------------------
% 8.86/2.07 % (3945507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.86/2.07 % (3945507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.86/2.07 % (3945507)CaDiCaL version: 2.1.3
% 8.86/2.07 % (3945507)Termination reason: Instruction limit
% 8.86/2.07 % (3945507)Termination phase: Saturation
% 8.86/2.07 % (3945507)Time elapsed: 0.065 s
% 8.86/2.07 % (3945507)Peak memory usage: 116 MB
% 8.86/2.07 % (3945507)Instructions burned: 53 (million)
% 8.86/2.07 % (3945516)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3329500558:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 8.86/2.07 % (3945520)dis+10_1_si=on:random_seed=3013726364:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 8.86/2.07 % (3945520)Instruction limit reached!
% 8.86/2.07 % (3945520)------------------------------
% 8.86/2.07 % (3945520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.86/2.07 % (3945520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.86/2.07 % (3945520)CaDiCaL version: 2.1.3
% 8.86/2.07 % (3945520)Termination reason: Instruction limit
% 8.86/2.07 % (3945520)Termination phase: Saturation
% 8.86/2.07 % (3945520)Time elapsed: 0.004 s
% 8.86/2.07 % (3945520)Peak memory usage: 88 MB
% 8.86/2.07 % (3945520)Instructions burned: 11 (million)
% 8.86/2.07 % (3945521)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3284892726:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi)
% 8.86/2.07 % (3945521)Refutation not found, incomplete strategy
% 8.86/2.07 % (3945521)------------------------------
% 8.86/2.07 % (3945521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.86/2.07 % (3945521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.86/2.07 % (3945521)CaDiCaL version: 2.1.3
% 8.86/2.07 % (3945521)Termination reason: Refutation not found, incomplete strategy
% 8.86/2.07 % (3945521)Time elapsed: 0.002 s
% 8.86/2.07 % (3945521)Peak memory usage: 89 MB
% 8.86/2.07 % (3945521)Instructions burned: 1 (million)
% 8.86/2.07 % (3945504)------------------------------
% 8.86/2.07 % (3945504)------------------------------
% 8.86/2.07 % (3945522)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2240593286: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_2993 on theBenchmark for (2993ds/35Mi)
% 9.71/2.34 % (3945524)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=879574273:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 9.71/2.34 % (3945516)Instruction limit reached!
% 9.71/2.34 % (3945516)------------------------------
% 9.71/2.34 % (3945516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.71/2.34 % (3945516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.71/2.34 % (3945516)CaDiCaL version: 2.1.3
% 9.71/2.34 % (3945516)Termination reason: Instruction limit
% 9.71/2.34 % (3945516)Termination phase: Saturation
% 9.71/2.34 % (3945516)Time elapsed: 0.111 s
% 9.71/2.34 % (3945516)Peak memory usage: 116 MB
% 9.71/2.34 % (3945516)Instructions burned: 127 (million)
% 9.71/2.34 % (3945524)Instruction limit reached!
% 9.71/2.34 % (3945524)------------------------------
% 9.71/2.34 % (3945524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.71/2.34 % (3945524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.71/2.34 % (3945524)CaDiCaL version: 2.1.3
% 9.71/2.34 % (3945524)Termination reason: Instruction limit
% 9.71/2.34 % (3945524)Termination phase: Saturation
% 9.71/2.34 % (3945524)Time elapsed: 0.003 s
% 9.71/2.34 % (3945524)Peak memory usage: 89 MB
% 9.71/2.34 % (3945524)Instructions burned: 3 (million)
% 9.71/2.34 % (3945522)Instruction limit reached!
% 9.71/2.34 % (3945522)------------------------------
% 9.71/2.34 % (3945522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.71/2.34 % (3945522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.71/2.34 % (3945522)CaDiCaL version: 2.1.3
% 9.71/2.34 % (3945522)Termination reason: Instruction limit
% 9.71/2.34 % (3945522)Termination phase: Saturation
% 9.71/2.34 % (3945522)Time elapsed: 0.029 s
% 9.71/2.34 % (3945522)Peak memory usage: 89 MB
% 9.71/2.34 % (3945522)Instructions burned: 36 (million)
% 9.71/2.34 % (3945525)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3347538435:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 9.71/2.34 % (3945528)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3400476753:i=370:ep=RS:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/370Mi)
% 9.71/2.34 % (3945528)Refutation not found, incomplete strategy
% 9.71/2.34 % (3945528)------------------------------
% 9.71/2.34 % (3945528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.71/2.34 % (3945528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.71/2.34 % (3945528)CaDiCaL version: 2.1.3
% 9.71/2.34 % (3945528)Termination reason: Refutation not found, incomplete strategy
% 9.71/2.34 % (3945528)Time elapsed: 0.001 s
% 9.71/2.34 % (3945528)Peak memory usage: 88 MB
% 9.71/2.34 % (3945525)Instruction limit reached!
% 9.71/2.34 % (3945525)------------------------------
% 9.71/2.34 % (3945525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.71/2.34 % (3945525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.71/2.34 % (3945525)CaDiCaL version: 2.1.3
% 9.71/2.34 % (3945525)Termination reason: Instruction limit
% 9.71/2.34 % (3945525)Termination phase: Saturation
% 9.71/2.34 % (3945525)Time elapsed: 0.007 s
% 9.71/2.34 % (3945525)Peak memory usage: 88 MB
% 9.71/2.34 % (3945525)Instructions burned: 8 (million)
% 9.71/2.34 % (3945530)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1491299143:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi)
% 9.71/2.34 % (3945534)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1857102882:i=10:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 9.71/2.34 % (3945533)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1866202942:i=226:rtra=on:gtg=position:ss=axioms_2991 on theBenchmark for (2991ds/226Mi)
% 9.71/2.34 % (3945534)Refutation not found, incomplete strategy
% 9.71/2.34 % (3945534)------------------------------
% 9.71/2.34 % (3945534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.71/2.34 % (3945534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.71/2.34 % (3945534)CaDiCaL version: 2.1.3
% 9.71/2.34 % (3945534)Termination reason: Refutation not found, incomplete strategy
% 9.71/2.34 % (3945534)Time elapsed: 0.002 s
% 9.71/2.34 % (3945534)Peak memory usage: 88 MB
% 9.71/2.34 % (3945534)Instructions burned: 1 (million)
% 9.71/2.34 % (3945530)Instruction limit reached!
% 9.71/2.34 % (3945530)------------------------------
% 9.71/2.34 % (3945530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.71/2.34 % (3945530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.71/2.34 % (3945530)CaDiCaL version: 2.1.3
% 9.71/2.34 % (3945530)Termination reason: Instruction limit
% 9.71/2.34 % (3945530)Termination phase: Saturation
% 9.71/2.34 % (3945530)Time elapsed: 0.033 s
% 9.71/2.34 % (3945530)Peak memory usage: 116 MB
% 9.71/2.34 % (3945530)Instructions burned: 13 (million)
% 9.71/2.34 % (3945535)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1487775506:i=71:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/71Mi)
% 9.71/2.34 % (3945528)------------------------------
% 9.71/2.34 % (3945528)------------------------------
% 9.71/2.34 % (3945533)Refutation not found, incomplete strategy
% 9.71/2.34 % (3945533)------------------------------
% 9.71/2.34 % (3945533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.71/2.34 % (3945533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.71/2.34 % (3945533)CaDiCaL version: 2.1.3
% 9.71/2.34 % (3945533)Termination reason: Refutation not found, incomplete strategy
% 9.71/2.34 % (3945533)Time elapsed: 0.027 s
% 9.71/2.34 % (3945533)Peak memory usage: 112 MB
% 9.71/2.34 % (3945533)Instructions burned: 5 (million)
% 9.71/2.34 % (3945521)------------------------------
% 9.71/2.34 % (3945521)------------------------------
% 9.71/2.34 % (3945538)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=4135015119:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2991 on theBenchmark for (2991ds/75Mi)
% 9.71/2.34 % (3945535)Refutation not found, incomplete strategy
% 9.71/2.34 % (3945535)------------------------------
% 9.71/2.34 % (3945535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.71/2.34 % (3945535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.71/2.34 % (3945535)CaDiCaL version: 2.1.3
% 9.71/2.34 % (3945535)Termination reason: Refutation not found, incomplete strategy
% 9.71/2.34 % (3945535)Time elapsed: 0.057 s
% 9.71/2.34 % (3945535)Peak memory usage: 132 MB
% 9.71/2.34 % (3945535)Instructions burned: 14 (million)
% 9.71/2.34 % (3945538)Instruction limit reached!
% 9.71/2.34 % (3945538)------------------------------
% 9.71/2.34 % (3945538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.71/2.34 % (3945538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.71/2.34 % (3945538)CaDiCaL version: 2.1.3
% 9.71/2.34 % (3945538)Termination reason: Instruction limit
% 9.71/2.34 % (3945538)Termination phase: Saturation
% 9.71/2.34 % (3945538)Time elapsed: 0.046 s
% 9.71/2.34 % (3945538)Peak memory usage: 89 MB
% 9.71/2.34 % (3945538)Instructions burned: 76 (million)
% 9.71/2.34 % (3945544)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=181818865:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi)
% 9.71/2.34 % (3945543)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=3827189292:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2990 on theBenchmark for (2990ds/294Mi)
% 9.71/2.34 % (3945544)Instruction limit reached!
% 9.71/2.34 % (3945544)------------------------------
% 9.71/2.34 % (3945544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.71/2.34 % (3945544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.71/2.34 % (3945544)CaDiCaL version: 2.1.3
% 9.71/2.34 % (3945544)Termination reason: Instruction limit
% 9.71/2.34 % (3945544)Termination phase: Saturation
% 9.71/2.34 % (3945544)Time elapsed: 0.046 s
% 9.71/2.34 % (3945544)Peak memory usage: 115 MB
% 9.71/2.34 % (3945544)Instructions burned: 130 (million)
% 9.71/2.34 % (3945546)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3901563341:i=131:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 9.71/2.34 % (3945534)------------------------------
% 9.71/2.34 % (3945534)------------------------------
% 9.71/2.34 % (3945547)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=867259410:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/40Mi)
% 11.14/2.54 % (3945546)First to succeed.
% 11.14/2.54 % (3945533)------------------------------
% 11.14/2.54 % (3945533)------------------------------
% 11.14/2.54 % (3945546)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3945473"
% 11.14/2.54 % (3945543)Instruction limit reached!
% 11.14/2.54 % (3945543)------------------------------
% 11.14/2.54 % (3945543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.14/2.54 % (3945543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.14/2.54 % (3945543)CaDiCaL version: 2.1.3
% 11.14/2.54 % (3945543)Termination reason: Instruction limit
% 11.14/2.54 % (3945543)Termination phase: Saturation
% 11.14/2.54 % (3945543)Time elapsed: 0.155 s
% 11.14/2.54 % (3945543)Peak memory usage: 89 MB
% 11.14/2.54 % (3945543)Instructions burned: 295 (million)
% 11.14/2.54 % (3945535)------------------------------
% 11.14/2.54 % (3945535)------------------------------
% 11.14/2.54 % (3945551)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3724562660:i=307:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/307Mi)
% 11.14/2.54 % (3945547)Instruction limit reached!
% 11.14/2.54 % (3945547)------------------------------
% 11.14/2.54 % (3945547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.14/2.54 % (3945547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.14/2.54 % (3945547)CaDiCaL version: 2.1.3
% 11.14/2.54 % (3945547)Termination reason: Instruction limit
% 11.14/2.54 % (3945547)Termination phase: Saturation
% 11.14/2.54 % (3945547)Time elapsed: 0.074 s
% 11.14/2.54 % (3945547)Peak memory usage: 133 MB
% 11.14/2.54 % (3945547)Instructions burned: 41 (million)
% 11.14/2.54 % (3945553)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1649085244:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/598Mi)
% 11.14/2.54 % (3945551)Instruction limit reached!
% 11.14/2.54 % (3945551)------------------------------
% 11.14/2.54 % (3945551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.14/2.54 % (3945551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.14/2.54 % (3945551)CaDiCaL version: 2.1.3
% 11.14/2.54 % (3945551)Termination reason: Instruction limit
% 11.14/2.54 % (3945551)Termination phase: Saturation
% 11.14/2.54 % (3945551)Time elapsed: 0.100 s
% 11.14/2.54 % (3945551)Peak memory usage: 90 MB
% 11.14/2.54 % (3945551)Instructions burned: 308 (million)
% 11.14/2.54 % (3945554)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2203651656:i=131:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/131Mi)
% 11.14/2.54 % (3945557)dis+10_1_si=on:random_seed=340102335:s2a=on:i=1000:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/1000Mi)
% 11.14/2.54 % (3945555)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=675265099:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2987 on theBenchmark for (2987ds/259Mi)
% 11.14/2.54 % (3945553)Refutation not found, incomplete strategy
% 11.14/2.54 % (3945553)------------------------------
% 11.14/2.54 % (3945553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.14/2.54 % (3945553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.14/2.54 % (3945553)CaDiCaL version: 2.1.3
% 11.14/2.54 % (3945553)Termination reason: Refutation not found, incomplete strategy
% 11.14/2.54 % (3945553)Time elapsed: 0.070 s
% 11.14/2.54 % (3945553)Peak memory usage: 133 MB
% 11.14/2.54 % (3945553)Instructions burned: 30 (million)
% 11.14/2.54 % (3945558)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1493937730:i=383:fsr=off:rtra=on:ev=force_2986 on theBenchmark for (2986ds/383Mi)
% 11.14/2.54 % (3945558)Refutation not found, incomplete strategy
% 11.14/2.54 % (3945558)------------------------------
% 11.14/2.54 % (3945558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.14/2.54 % (3945558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.14/2.54 % (3945558)CaDiCaL version: 2.1.3
% 11.14/2.54 % (3945558)Termination reason: Refutation not found, incomplete strategy
% 11.14/2.54 % (3945558)Time elapsed: 0.002 s
% 11.14/2.54 % (3945558)Peak memory usage: 89 MB
% 11.14/2.54 % (3945558)Instructions burned: 1 (million)
% 11.14/2.54 % (3945546)Refutation found. Thanks to Tanya!
% 11.14/2.54 % SZS status Theorem for theBenchmark
% 11.14/2.54 % SZS output start Proof for theBenchmark
% See solution above
% 11.14/2.54 % (3945546)------------------------------
% 11.14/2.54 % (3945546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.14/2.54 % (3945546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.14/2.54 % (3945546)CaDiCaL version: 2.1.3
% 11.14/2.54 % (3945546)Termination reason: Refutation
% 11.14/2.54 % (3945546)Time elapsed: 0.073 s
% 11.14/2.54 % (3945546)Peak memory usage: 133 MB
% 11.14/2.54 % (3945546)Instructions burned: 34 (million)
% 11.14/2.54 % (3945546)------------------------------
% 11.14/2.54 % (3945546)------------------------------
% 11.14/2.54 % (3945473)Success in time 1.493 s
% 11.14/2.54 % Vampire exiting
%------------------------------------------------------------------------------