%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PLA031-1.003 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:38 PM UTC 2026
% Result : Unsatisfiable 62.17s 14.45s
% Output : Refutation 62.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 20
% Syntax : Number of formulae : 35 ( 25 unt; 0 def)
% Number of atoms : 49 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 37 ( 23 ~; 14 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-8 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 86 ( 86 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ s(X0,X1,X2,X3,X4,X5,X0,X6)
| s(truck1,X1,X2,X3,X4,X5,X0,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load1) ).
fof(f2,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ s(truck1,X1,X2,X3,X4,X5,X0,X6)
| s(X0,X1,X2,X3,X4,X5,X0,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load2) ).
fof(f9,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ s(X0,X1,X2,X3,X4,X5,X2,X6)
| s(X0,X1,truck1,X3,X4,X5,X2,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load9) ).
fof(f10,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ s(X0,X1,truck1,X3,X4,X5,X2,X6)
| s(X0,X1,X2,X3,X4,X5,X2,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load10) ).
fof(f13,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ s(X0,X1,X2,X3,X4,X5,X3,X6)
| s(X0,X1,X2,truck1,X4,X5,X3,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load13) ).
fof(f14,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ s(X0,X1,X2,truck1,X4,X5,X3,X6)
| s(X0,X1,X2,X3,X4,X5,X3,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load14) ).
fof(f21,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ s(X0,X1,X2,X3,X4,X5,X5,X6)
| ~ neq(X4,truck1)
| s(X0,X1,X2,X3,X4,truck1,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',board5) ).
fof(f27,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ s(X0,X1,X2,X3,X4,truck1,X5,X6)
| ~ link(X5,X7)
| s(X0,X1,X2,X3,X4,truck1,X7,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive3) ).
fof(f29,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ s(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ path(X4,X8)
| s(X0,X1,X2,X3,X8,X5,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',walk1) ).
fof(f30,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ s(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ path(X5,X8)
| s(X0,X1,X2,X3,X4,X8,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',walk2) ).
fof(f79,axiom,
neq(p1_2,truck1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq49) ).
fof(f95,axiom,
path(s0,p0_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map1) ).
fof(f98,axiom,
path(p0_1,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map4) ).
fof(f100,axiom,
path(p1_2,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map6) ).
fof(f101,axiom,
path(s2,p1_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map7) ).
fof(f107,axiom,
link(s1,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map13) ).
fof(f109,axiom,
link(s2,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map15) ).
fof(f110,axiom,
link(s0,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map16) ).
fof(f111,axiom,
s(s1,s2,s2,s0,s2,s0,s1,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',init) ).
fof(f112,negated_conjecture,
! [X0,X1] : ~ s(s2,s2,s0,s2,s1,X0,s0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f113,plain,
s(truck1,s2,s2,s0,s2,s0,s1,s1),
inference(unit_resulting_resolution,[],[f1,f111]) ).
fof(f129,plain,
! [X0,X1] : ~ s(s2,s2,truck1,s2,s1,X0,s0,X1),
inference(unit_resulting_resolution,[],[f10,f112]) ).
fof(f697,plain,
! [X0] : ~ s(s2,s2,truck1,s2,s1,truck1,s2,X0),
inference(unit_resulting_resolution,[],[f27,f109,f129]) ).
fof(f764,plain,
! [X0] : ~ s(s2,s2,s2,s2,s1,truck1,s2,X0),
inference(unit_resulting_resolution,[],[f9,f697]) ).
fof(f999,plain,
! [X0] : ~ s(truck1,s2,s2,s2,s1,truck1,s2,X0),
inference(unit_resulting_resolution,[],[f2,f764]) ).
fof(f1681,plain,
s(truck1,s2,s2,s0,p1_2,s0,s1,s1),
inference(unit_resulting_resolution,[],[f29,f101,f113]) ).
fof(f4912,plain,
! [X0] : ~ s(truck1,s2,s2,truck1,s1,truck1,s2,X0),
inference(unit_resulting_resolution,[],[f14,f999]) ).
fof(f5480,plain,
s(truck1,s2,s2,s0,p1_2,p0_1,s1,s1),
inference(unit_resulting_resolution,[],[f30,f95,f1681]) ).
fof(f14965,plain,
! [X0] : ~ s(truck1,s2,s2,truck1,s1,truck1,s0,X0),
inference(unit_resulting_resolution,[],[f27,f110,f4912]) ).
fof(f20810,plain,
s(truck1,s2,s2,s0,p1_2,s1,s1,s1),
inference(unit_resulting_resolution,[],[f30,f98,f5480]) ).
fof(f41791,plain,
! [X0] : ~ s(truck1,s2,s2,s0,s1,truck1,s0,X0),
inference(unit_resulting_resolution,[],[f13,f14965]) ).
fof(f50280,plain,
s(truck1,s2,s2,s0,p1_2,truck1,s1,s1),
inference(unit_resulting_resolution,[],[f21,f79,f20810]) ).
fof(f99439,plain,
s(truck1,s2,s2,s0,s1,truck1,s1,s1),
inference(unit_resulting_resolution,[],[f29,f100,f50280]) ).
fof(f103254,plain,
! [X0] : ~ s(truck1,s2,s2,s0,s1,truck1,s2,X0),
inference(unit_resulting_resolution,[],[f27,f109,f41791]) ).
fof(f224563,plain,
$false,
inference(unit_resulting_resolution,[],[f27,f107,f99439,f103254]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PLA031-1.003 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.34 % Computer : n012.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Sun Sep 27 22:10:34 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.06/0.34 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.37 Running first-order model finding
% 0.06/0.37 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.16/1.53 % (2805448)Will run a generic schedule for satisfiability detection.
% 7.16/1.53 % (2805454)% WARNING: option uhcvi not known.
% 7.16/1.53 % (2805454)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2962976938:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.16/1.53 % (2805453)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2187087563_2999 on theBenchmark for (2999ds/0Mi)
% 7.16/1.53 % (2805455)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2078023989:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.16/1.53 % (2805456)dis+10_1_sil=32000:sp=arity:random_seed=1790297396:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.16/1.53 % (2805457)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1521557835:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.16/1.53 % (2805458)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1109262925:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.16/1.53 % (2805459)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=210903232:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.16/1.53 % Detected minimum model sizes of [1]
% 7.16/1.53 % Detected maximum model sizes of [8]
% 7.16/1.53 % TRYING [1]
% 7.16/1.53 % TRYING [2]
% 7.16/1.53 % TRYING [3]
% 7.16/1.53 % (2805456)Instruction limit reached!
% 7.16/1.53 % (2805456)------------------------------
% 7.16/1.53 % (2805456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.16/1.53 % (2805456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.53 % (2805456)CaDiCaL version: 2.1.3
% 7.16/1.53 % (2805456)Termination reason: Instruction limit
% 7.16/1.53 % (2805456)Termination phase: Saturation
% 7.16/1.53 % (2805456)Time elapsed: 0.052 s
% 7.16/1.53 % (2805456)Peak memory usage: 12 MB
% 7.16/1.53 % (2805456)Instructions burned: 104 (million)
% 7.16/1.53 % (2805457)Instruction limit reached!
% 7.16/1.53 % (2805457)------------------------------
% 7.16/1.53 % (2805457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.16/1.53 % (2805457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.53 % (2805457)CaDiCaL version: 2.1.3
% 7.16/1.53 % (2805457)Termination reason: Instruction limit
% 7.16/1.53 % (2805457)Termination phase: Saturation
% 7.16/1.53 % (2805457)Time elapsed: 0.054 s
% 7.16/1.53 % (2805457)Peak memory usage: 12 MB
% 7.16/1.53 % (2805457)Instructions burned: 116 (million)
% 7.16/1.53 % (2805458)Instruction limit reached!
% 7.16/1.53 % (2805458)------------------------------
% 7.16/1.53 % (2805458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.16/1.53 % (2805458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.53 % (2805458)CaDiCaL version: 2.1.3
% 7.16/1.53 % (2805458)Termination reason: Instruction limit
% 7.16/1.53 % (2805458)Termination phase: Saturation
% 7.16/1.53 % (2805458)Time elapsed: 0.061 s
% 7.16/1.53 % (2805458)Peak memory usage: 12 MB
% 7.16/1.53 % (2805458)Instructions burned: 132 (million)
% 7.16/1.53 % (2805467)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3070529024:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.16/1.53 % Detected minimum model sizes of [1]
% 7.16/1.53 % Detected maximum model sizes of [8]
% 7.16/1.53 % TRYING [1]
% 7.16/1.53 % TRYING [2]
% 7.16/1.53 % TRYING [3]
% 7.16/1.53 % (2805468)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=462436347:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.16/1.53 % (2805459)Instruction limit reached!
% 7.16/1.53 % (2805459)------------------------------
% 7.16/1.53 % (2805459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.16/1.53 % (2805459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.53 % (2805459)CaDiCaL version: 2.1.3
% 7.16/1.53 % (2805459)Termination reason: Instruction limit
% 7.16/1.53 % (2805459)Termination phase: Saturation
% 7.16/1.53 % (2805459)Time elapsed: 0.076 s
% 7.16/1.53 % (2805459)Peak memory usage: 13 MB
% 7.16/1.53 % (2805459)Instructions burned: 161 (million)
% 7.16/1.53 % (2805469)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3748466973:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 7.16/1.53 % (2805472)ott-21_1_sil=16000:fs=off:random_seed=4135008618:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 7.16/1.53 % (2805468)Instruction limit reached!
% 7.16/1.53 % (2805468)------------------------------
% 24.83/3.90 % (2805468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.83/3.90 % (2805468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.83/3.90 % (2805468)CaDiCaL version: 2.1.3
% 24.83/3.90 % (2805468)Termination reason: Instruction limit
% 24.83/3.90 % (2805468)Termination phase: Saturation
% 24.83/3.90 % (2805468)Time elapsed: 0.063 s
% 24.83/3.90 % (2805468)Peak memory usage: 12 MB
% 24.83/3.90 % (2805468)Instructions burned: 139 (million)
% 24.83/3.90 % (2805475)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2303249706:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 24.83/3.90 % (2805472)Instruction limit reached!
% 24.83/3.90 % (2805472)------------------------------
% 24.83/3.90 % (2805472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.83/3.90 % (2805472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.83/3.90 % (2805472)CaDiCaL version: 2.1.3
% 24.83/3.90 % (2805472)Termination reason: Instruction limit
% 24.83/3.90 % (2805472)Termination phase: Saturation
% 24.83/3.90 % (2805472)Time elapsed: 0.082 s
% 24.83/3.90 % (2805472)Peak memory usage: 12 MB
% 24.83/3.90 % (2805472)Instructions burned: 182 (million)
% 24.83/3.90 % (2805477)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3564721394:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 24.83/3.90 % Detected minimum model sizes of [1]
% 24.83/3.90 % Detected maximum model sizes of [8]
% 24.83/3.90 % TRYING [1]
% 24.83/3.90 % TRYING [2]
% 24.83/3.90 % TRYING [3]
% 24.83/3.90 % TRYING [4]
% 24.83/3.90 % TRYING [4]
% 24.83/3.90 % (2805467)Instruction limit reached!
% 24.83/3.90 % (2805467)------------------------------
% 24.83/3.90 % (2805467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.83/3.90 % (2805467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.83/3.90 % (2805467)CaDiCaL version: 2.1.3
% 24.83/3.90 % (2805467)Termination reason: Instruction limit
% 24.83/3.90 % (2805467)Termination phase: Finite model building constraint generation
% 24.83/3.90 % (2805467)Time elapsed: 0.243 s
% 24.83/3.90 % (2805467)Peak memory usage: 38 MB
% 24.83/3.90 % (2805467)Instructions burned: 716 (million)
% 24.83/3.90 % (2805479)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2341063813:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 24.83/3.90 % (2805475)Instruction limit reached!
% 24.83/3.90 % (2805475)------------------------------
% 24.83/3.90 % (2805475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.83/3.90 % (2805475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.83/3.90 % (2805475)CaDiCaL version: 2.1.3
% 24.83/3.90 % (2805475)Termination reason: Instruction limit
% 24.83/3.90 % (2805475)Termination phase: Saturation
% 24.83/3.90 % (2805475)Time elapsed: 0.241 s
% 24.83/3.90 % (2805475)Peak memory usage: 16 MB
% 24.83/3.90 % (2805475)Instructions burned: 477 (million)
% 24.83/3.90 % (2805481)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=834659112:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 24.83/3.90 % Detected minimum model sizes of [1]
% 24.83/3.90 % Detected maximum model sizes of [8]
% 24.83/3.90 % fmb_start_size (= 14) larger than a detected sort maximum size!
% 24.83/3.90 % (2805481)Refutation not found, incomplete strategy
% 24.83/3.90 % (2805481)------------------------------
% 24.83/3.90 % (2805481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.83/3.90 % (2805481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.83/3.90 % (2805481)CaDiCaL version: 2.1.3
% 24.83/3.90 % (2805481)Termination reason: Refutation not found, incomplete strategy
% 24.83/3.90 % (2805481)Time elapsed: 0.002 s
% 24.83/3.90 % (2805481)Peak memory usage: 10 MB
% 24.83/3.90 % (2805481)Instructions burned: 6 (million)
% 24.83/3.90 % (2805481)------------------------------
% 24.83/3.90 % (2805481)------------------------------
% 24.83/3.90 % (2805469)Instruction limit reached!
% 24.83/3.90 % (2805469)------------------------------
% 24.83/3.90 % (2805469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.83/3.90 % (2805469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.83/3.90 % (2805469)CaDiCaL version: 2.1.3
% 24.83/3.90 % (2805469)Termination reason: Instruction limit
% 24.83/3.90 % (2805469)Termination phase: Saturation
% 24.83/3.90 % (2805469)Time elapsed: 0.345 s
% 24.83/3.90 % (2805469)Peak memory usage: 18 MB
% 24.83/3.90 % (2805469)Instructions burned: 685 (million)
% 24.83/3.90 % (2805483)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2009025294:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 70.66/10.42 % (2805484)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2273006508:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 70.66/10.42 % (2805477)Instruction limit reached!
% 70.66/10.42 % (2805477)------------------------------
% 70.66/10.42 % (2805477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.66/10.42 % (2805477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.66/10.42 % (2805477)CaDiCaL version: 2.1.3
% 70.66/10.42 % (2805477)Termination reason: Instruction limit
% 70.66/10.42 % (2805477)Termination phase: Finite model building constraint generation
% 70.66/10.42 % (2805477)Time elapsed: 0.296 s
% 70.66/10.42 % (2805477)Peak memory usage: 39 MB
% 70.66/10.42 % (2805477)Instructions burned: 867 (million)
% 70.66/10.42 % (2805489)fmb+10_1_sil=64000:random_seed=2669946369:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 70.66/10.42 % Detected minimum model sizes of [1]
% 70.66/10.42 % Detected maximum model sizes of [8]
% 70.66/10.42 % TRYING [1]
% 70.66/10.42 % TRYING [2]
% 70.66/10.42 % TRYING [3]
% 70.66/10.42 % (2805484)Instruction limit reached!
% 70.66/10.42 % (2805484)------------------------------
% 70.66/10.42 % (2805484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.66/10.42 % (2805484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.66/10.42 % (2805484)CaDiCaL version: 2.1.3
% 70.66/10.42 % (2805484)Termination reason: Instruction limit
% 70.66/10.42 % (2805484)Termination phase: Saturation
% 70.66/10.42 % (2805484)Time elapsed: 0.358 s
% 70.66/10.42 % (2805484)Peak memory usage: 16 MB
% 70.66/10.42 % (2805484)Instructions burned: 881 (million)
% 70.66/10.42 % (2805483)Instruction limit reached!
% 70.66/10.42 % (2805483)------------------------------
% 70.66/10.42 % (2805483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.66/10.42 % (2805483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.66/10.42 % (2805483)CaDiCaL version: 2.1.3
% 70.66/10.42 % (2805483)Termination reason: Instruction limit
% 70.66/10.42 % (2805483)Termination phase: Saturation
% 70.66/10.42 % (2805483)Time elapsed: 0.368 s
% 70.66/10.42 % (2805483)Peak memory usage: 21 MB
% 70.66/10.42 % (2805483)Instructions burned: 693 (million)
% 70.66/10.42 % (2805492)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=791948170:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 70.66/10.42 % (2805491)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=179652924:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 70.66/10.42 % Detected minimum model sizes of [1]
% 70.66/10.42 % Detected maximum model sizes of [8]
% 70.66/10.42 % TRYING [8]
% 70.66/10.42 % Detected minimum model sizes of [1]
% 70.66/10.42 % Detected maximum model sizes of [8]
% 70.66/10.42 % fmb_start_size (= 20) larger than a detected sort maximum size!
% 70.66/10.42 % (2805491)Refutation not found, incomplete strategy
% 70.66/10.42 % (2805491)------------------------------
% 70.66/10.42 % (2805491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.66/10.42 % (2805491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.66/10.42 % (2805491)CaDiCaL version: 2.1.3
% 70.66/10.42 % (2805491)Termination reason: Refutation not found, incomplete strategy
% 70.66/10.42 % (2805491)Time elapsed: 0.003 s
% 70.66/10.42 % (2805491)Peak memory usage: 10 MB
% 70.66/10.42 % (2805491)Instructions burned: 6 (million)
% 70.66/10.42 % (2805491)------------------------------
% 70.66/10.42 % (2805491)------------------------------
% 70.66/10.42 % (2805495)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1833537691:i=5131_2991 on theBenchmark for (2991ds/5131Mi)
% 70.66/10.42 % (2805479)Instruction limit reached!
% 70.66/10.42 % (2805479)------------------------------
% 70.66/10.42 % (2805479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.66/10.42 % (2805479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.66/10.42 % (2805479)CaDiCaL version: 2.1.3
% 70.66/10.42 % (2805479)Termination reason: Instruction limit
% 70.66/10.42 % (2805479)Termination phase: Saturation
% 70.66/10.42 % (2805479)Time elapsed: 0.593 s
% 70.66/10.42 % (2805479)Peak memory usage: 22 MB
% 70.66/10.42 % (2805479)Instructions burned: 1179 (million)
% 70.66/10.42 % (2805497)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1213932644:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi)
% 70.66/10.42 % TRYING [4]
% 70.66/10.42 % (2805492)Instruction limit reached!
% 62.17/14.44 % (2805492)------------------------------
% 62.17/14.44 % (2805492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.44 % (2805492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.44 % (2805492)CaDiCaL version: 2.1.3
% 62.17/14.44 % (2805492)Termination reason: Instruction limit
% 62.17/14.44 % (2805492)Termination phase: Finite model building constraint generation
% 62.17/14.44 % (2805492)Time elapsed: 0.318 s
% 62.17/14.44 % (2805492)Peak memory usage: 59 MB
% 62.17/14.44 % (2805492)Instructions burned: 921 (million)
% 62.17/14.44 % (2805499)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3720464153:i=6324_2988 on theBenchmark for (2988ds/6324Mi)
% 62.17/14.44 % Detected minimum model sizes of [1]
% 62.17/14.44 % Detected maximum model sizes of [8]
% 62.17/14.44 % fmb_start_size (= 77) larger than a detected sort maximum size!
% 62.17/14.44 % (2805499)Refutation not found, incomplete strategy
% 62.17/14.44 % (2805499)------------------------------
% 62.17/14.44 % (2805499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.44 % (2805499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.44 % (2805499)CaDiCaL version: 2.1.3
% 62.17/14.44 % (2805499)Termination reason: Refutation not found, incomplete strategy
% 62.17/14.44 % (2805499)Time elapsed: 0.002 s
% 62.17/14.44 % (2805499)Peak memory usage: 11 MB
% 62.17/14.44 % (2805499)Instructions burned: 8 (million)
% 62.17/14.44 % (2805499)------------------------------
% 62.17/14.44 % (2805499)------------------------------
% 62.17/14.44 % (2805501)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4290207772:fmbsr=2.30978:i=2174_2988 on theBenchmark for (2988ds/2174Mi)
% 62.17/14.44 % Detected minimum model sizes of [1]
% 62.17/14.44 % Detected maximum model sizes of [8]
% 62.17/14.44 % fmb_start_size (= 16) larger than a detected sort maximum size!
% 62.17/14.44 % (2805501)Refutation not found, incomplete strategy
% 62.17/14.44 % (2805501)------------------------------
% 62.17/14.44 % (2805501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.44 % (2805501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.44 % (2805501)CaDiCaL version: 2.1.3
% 62.17/14.44 % (2805501)Termination reason: Refutation not found, incomplete strategy
% 62.17/14.44 % (2805501)Time elapsed: 0.002 s
% 62.17/14.44 % (2805501)Peak memory usage: 10 MB
% 62.17/14.44 % (2805501)Instructions burned: 6 (million)
% 62.17/14.44 % (2805501)------------------------------
% 62.17/14.44 % (2805501)------------------------------
% 62.17/14.44 % (2805503)ott-2_1_sil=16000:newcnf=on:random_seed=3787546601:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi)
% 62.17/14.44 % (2805503)Instruction limit reached!
% 62.17/14.44 % (2805503)------------------------------
% 62.17/14.44 % (2805503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.44 % (2805503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.44 % (2805503)CaDiCaL version: 2.1.3
% 62.17/14.44 % (2805503)Termination reason: Instruction limit
% 62.17/14.44 % (2805503)Termination phase: Saturation
% 62.17/14.44 % (2805503)Time elapsed: 0.355 s
% 62.17/14.44 % (2805503)Peak memory usage: 19 MB
% 62.17/14.44 % (2805503)Instructions burned: 870 (million)
% 62.17/14.44 % (2805505)ott+10_1_sil=32000:tgt=ground:random_seed=175222541:i=5114:av=off_2984 on theBenchmark for (2984ds/5114Mi)
% 62.17/14.44 % (2805497)Instruction limit reached!
% 62.17/14.44 % (2805497)------------------------------
% 62.17/14.44 % (2805497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.44 % (2805497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.44 % (2805497)CaDiCaL version: 2.1.3
% 62.17/14.44 % (2805497)Termination reason: Instruction limit
% 62.17/14.44 % (2805497)Termination phase: Saturation
% 62.17/14.44 % (2805497)Time elapsed: 0.671 s
% 62.17/14.44 % (2805497)Peak memory usage: 27 MB
% 62.17/14.44 % (2805497)Instructions burned: 1473 (million)
% 62.17/14.44 % (2805511)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=334037140:i=54282_2983 on theBenchmark for (2983ds/54282Mi)
% 62.17/14.44 % Detected minimum model sizes of [1]
% 62.17/14.44 % Detected maximum model sizes of [8]
% 62.17/14.44 % TRYING [1]
% 62.17/14.44 % TRYING [2]
% 62.17/14.44 % TRYING [3]
% 62.17/14.44 % TRYING [4]
% 62.17/14.44 % TRYING [5]
% 62.17/14.44 % (2805495)Instruction limit reached!
% 62.17/14.44 % (2805495)------------------------------
% 62.17/14.44 % (2805495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.44 % (2805495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.44 % (2805495)CaDiCaL version: 2.1.3
% 62.17/14.44 % (2805495)Termination reason: Instruction limit
% 62.17/14.44 % (2805495)Termination phase: Saturation
% 62.17/14.44 % (2805495)Time elapsed: 2.659 s
% 62.17/14.44 % (2805495)Peak memory usage: 46 MB
% 62.17/14.44 % (2805495)Instructions burned: 5133 (million)
% 62.17/14.44 % (2805525)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2838209423:i=3512:aac=none_2964 on theBenchmark for (2964ds/3512Mi)
% 62.17/14.44 % (2805505)Instruction limit reached!
% 62.17/14.44 % (2805505)------------------------------
% 62.17/14.44 % (2805505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.44 % (2805505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.44 % (2805505)CaDiCaL version: 2.1.3
% 62.17/14.44 % (2805505)Termination reason: Instruction limit
% 62.17/14.44 % (2805505)Termination phase: Saturation
% 62.17/14.44 % (2805505)Time elapsed: 2.700 s
% 62.17/14.44 % (2805505)Peak memory usage: 45 MB
% 62.17/14.44 % (2805505)Instructions burned: 5114 (million)
% 62.17/14.44 % (2805527)dis+21_1_sil=32000:sas=cadical:random_seed=2284324986:i=3773:amm=off_2957 on theBenchmark for (2957ds/3773Mi)
% 62.17/14.44 % TRYING [5]
% 62.17/14.44 % (2805525)Instruction limit reached!
% 62.17/14.44 % (2805525)------------------------------
% 62.17/14.44 % (2805525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.44 % (2805525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.44 % (2805525)CaDiCaL version: 2.1.3
% 62.17/14.44 % (2805525)Termination reason: Instruction limit
% 62.17/14.44 % (2805525)Termination phase: Saturation
% 62.17/14.44 % (2805525)Time elapsed: 1.825 s
% 62.17/14.44 % (2805525)Peak memory usage: 36 MB
% 62.17/14.44 % (2805525)Instructions burned: 3514 (million)
% 62.17/14.44 % (2805531)ott+11_1_sil=16000:gs=on:random_seed=2884295472:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2946 on theBenchmark for (2946ds/2251Mi)
% 62.17/14.44 % TRYING [5]
% 62.17/14.44 % (2805527)Instruction limit reached!
% 62.17/14.44 % (2805527)------------------------------
% 62.17/14.44 % (2805527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.44 % (2805527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.44 % (2805527)CaDiCaL version: 2.1.3
% 62.17/14.44 % (2805527)Termination reason: Instruction limit
% 62.17/14.44 % (2805527)Termination phase: Saturation
% 62.17/14.44 % (2805527)Time elapsed: 2.024 s
% 62.17/14.44 % (2805527)Peak memory usage: 43 MB
% 62.17/14.44 % (2805527)Instructions burned: 3773 (million)
% 62.17/14.44 % (2805535)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3871436414:fmbsr=1.6:i=67534_2936 on theBenchmark for (2936ds/67534Mi)
% 62.17/14.44 % Detected minimum model sizes of [1]
% 62.17/14.44 % Detected maximum model sizes of [8]
% 62.17/14.44 % (2805531)Instruction limit reached!
% 62.17/14.44 % (2805531)------------------------------
% 62.17/14.44 % (2805531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.44 % (2805531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.44 % (2805531)CaDiCaL version: 2.1.3
% 62.17/14.44 % (2805531)Termination reason: Instruction limit
% 62.17/14.44 % (2805531)Termination phase: Saturation
% 62.17/14.44 % (2805531)Time elapsed: 1.099 s
% 62.17/14.44 % (2805531)Peak memory usage: 97 MB
% 62.17/14.44 % (2805531)Instructions burned: 2252 (million)
% 62.17/14.44 % (2805537)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1574032764:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2934 on theBenchmark for (2934ds/4591Mi)
% 62.17/14.44 % (2805537)Instruction limit reached!
% 62.17/14.44 % (2805537)------------------------------
% 62.17/14.44 % (2805537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.44 % (2805537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.44 % (2805537)CaDiCaL version: 2.1.3
% 62.17/14.44 % (2805537)Termination reason: Instruction limit
% 62.17/14.44 % (2805537)Termination phase: Saturation
% 62.17/14.44 % (2805537)Time elapsed: 2.447 s
% 62.17/14.44 % (2805537)Peak memory usage: 48 MB
% 62.17/14.44 % (2805537)Instructions burned: 4593 (million)
% 62.17/14.44 % (2805539)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1547289498:i=29340_2910 on theBenchmark for (2910ds/29340Mi)
% 62.17/14.44 % (2805489)Instruction limit reached!
% 62.17/14.44 % (2805489)------------------------------
% 62.17/14.44 % (2805489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.45 % (2805489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.45 % (2805489)CaDiCaL version: 2.1.3
% 62.17/14.45 % (2805489)Termination reason: Instruction limit
% 62.17/14.45 % (2805489)Termination phase: Finite model building constraint generation
% 62.17/14.45 % (2805489)Time elapsed: 9.503 s
% 62.17/14.45 % (2805489)Peak memory usage: 667 MB
% 62.17/14.45 % (2805489)Instructions burned: 22061 (million)
% 62.17/14.45 % (2805541)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2877609594:i=5211_2898 on theBenchmark for (2898ds/5211Mi)
% 62.17/14.45 % TRYING [7]
% 62.17/14.45 % (2805541)Instruction limit reached!
% 62.17/14.45 % (2805541)------------------------------
% 62.17/14.45 % (2805541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.45 % (2805541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.45 % (2805541)CaDiCaL version: 2.1.3
% 62.17/14.45 % (2805541)Termination reason: Instruction limit
% 62.17/14.45 % (2805541)Termination phase: Saturation
% 62.17/14.45 % (2805541)Time elapsed: 2.147 s
% 62.17/14.45 % (2805541)Peak memory usage: 38 MB
% 62.17/14.45 % (2805541)Instructions burned: 5212 (million)
% 62.17/14.45 % (2805543)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1951862918:i=5497:nm=2_2877 on theBenchmark for (2877ds/5497Mi)
% 62.17/14.45 % Detected minimum model sizes of [1]
% 62.17/14.45 % Detected maximum model sizes of [8]
% 62.17/14.45 % fmb_start_size (= 17) larger than a detected sort maximum size!
% 62.17/14.45 % (2805543)Refutation not found, incomplete strategy
% 62.17/14.45 % (2805543)------------------------------
% 62.17/14.45 % (2805543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.45 % (2805543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.45 % (2805543)CaDiCaL version: 2.1.3
% 62.17/14.45 % (2805543)Termination reason: Refutation not found, incomplete strategy
% 62.17/14.45 % (2805543)Time elapsed: 0.002 s
% 62.17/14.45 % (2805543)Peak memory usage: 11 MB
% 62.17/14.45 % (2805543)Instructions burned: 8 (million)
% 62.17/14.45 % (2805543)------------------------------
% 62.17/14.45 % (2805543)------------------------------
% 62.17/14.45 % (2805545)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4099052662:fmbsr=2:i=46332_2876 on theBenchmark for (2876ds/46332Mi)
% 62.17/14.45 % Detected minimum model sizes of [1]
% 62.17/14.45 % Detected maximum model sizes of [8]
% 62.17/14.45 % fmb_start_size (= 15) larger than a detected sort maximum size!
% 62.17/14.45 % (2805545)Refutation not found, incomplete strategy
% 62.17/14.45 % (2805545)------------------------------
% 62.17/14.45 % (2805545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.45 % (2805545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.45 % (2805545)CaDiCaL version: 2.1.3
% 62.17/14.45 % (2805545)Termination reason: Refutation not found, incomplete strategy
% 62.17/14.45 % (2805545)Time elapsed: 0.002 s
% 62.17/14.45 % (2805545)Peak memory usage: 10 MB
% 62.17/14.45 % (2805545)Instructions burned: 6 (million)
% 62.17/14.45 % (2805545)------------------------------
% 62.17/14.45 % (2805545)------------------------------
% 62.17/14.45 % (2805547)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=986110557:i=14071_2876 on theBenchmark for (2876ds/14071Mi)
% 62.17/14.45 % Detected minimum model sizes of [1]
% 62.17/14.45 % Detected maximum model sizes of [8]
% 62.17/14.45 % fmb_start_size (= 12) larger than a detected sort maximum size!
% 62.17/14.45 % (2805547)Refutation not found, incomplete strategy
% 62.17/14.45 % (2805547)------------------------------
% 62.17/14.45 % (2805547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.45 % (2805547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.45 % (2805547)CaDiCaL version: 2.1.3
% 62.17/14.45 % (2805547)Termination reason: Refutation not found, incomplete strategy
% 62.17/14.45 % (2805547)Time elapsed: 0.002 s
% 62.17/14.45 % (2805547)Peak memory usage: 10 MB
% 62.17/14.45 % (2805547)Instructions burned: 6 (million)
% 62.17/14.45 % (2805547)------------------------------
% 62.17/14.45 % (2805547)------------------------------
% 62.17/14.45 % (2805549)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3215516379:i=22565:add=on:rawr=on_2876 on theBenchmark for (2876ds/22565Mi)
% 62.17/14.45 % (2805539) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2805448-2805539"...
% 62.17/14.45 % (2805539)...printing done.
% 62.17/14.45 % (2805539)Refutation found. Thanks to Tanya!
% 62.17/14.45 % SZS status Unsatisfiable for theBenchmark
% 62.17/14.45 % SZS output start Proof for theBenchmark
% See solution above
% 62.17/14.45 % (2805539)------------------------------
% 62.17/14.45 % (2805539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.17/14.45 % (2805539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/14.45 % (2805539)CaDiCaL version: 2.1.3
% 62.17/14.45 % (2805539)Termination reason: Refutation
% 62.17/14.45 % (2805539)Time elapsed: 4.768 s
% 62.17/14.45 % (2805539)Peak memory usage: 71 MB
% 62.17/14.45 % (2805539)Instructions burned: 9819 (million)
% 62.17/14.45 % (2805448)Success in time 14.071 s
% 62.17/14.45 % Vampire exiting
%------------------------------------------------------------------------------