%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW614_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:31 PM UTC 2026 % Result : Timeout 286.85s 40.69s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW614_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n008.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 14:23:27 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/0.22 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 % 3.67/0.85 % (2284558)Will run a generic schedule for satisfiability detection. % 3.67/0.85 % (2284569)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3709614168:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.67/0.85 % (2284564)% WARNING: option uhcvi not known. % 3.67/0.85 % (2284563)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3785279225_2999 on theBenchmark for (2999ds/0Mi) % 3.67/0.85 % (2284565)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4263363023:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.67/0.85 % (2284566)dis+10_1_sil=32000:sp=arity:random_seed=3375993778:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.67/0.85 % (2284564)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1941740488:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.67/0.85 % (2284568)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3108474953:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.67/0.85 % (2284567)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1488237083:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.67/0.85 % (2284563)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.67/0.85 % (2284563)Terminated due to inappropriate strategy. % 3.67/0.85 % (2284563)------------------------------ % 3.67/0.85 % (2284563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/0.85 % (2284563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/0.85 % (2284563)CaDiCaL version: 2.1.3 % 3.67/0.85 % (2284563)Termination reason: Inappropriate % 3.67/0.85 % (2284563)Time elapsed: 0.002 s % 3.67/0.85 % (2284563)Peak memory usage: 10 MB % 3.67/0.85 % (2284563)Instructions burned: 4 (million) % 3.67/0.85 % (2284563)------------------------------ % 3.67/0.85 % (2284563)------------------------------ % 3.67/0.85 % (2284577)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1594413132:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.67/0.85 % (2284577)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.67/0.85 % (2284577)Terminated due to inappropriate strategy. % 3.67/0.85 % (2284577)------------------------------ % 3.67/0.85 % (2284577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/0.85 % (2284577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/0.85 % (2284577)CaDiCaL version: 2.1.3 % 3.67/0.85 % (2284577)Termination reason: Inappropriate % 3.67/0.85 % (2284577)Time elapsed: 0.002 s % 3.67/0.85 % (2284577)Peak memory usage: 11 MB % 3.67/0.85 % (2284577)Instructions burned: 3 (million) % 3.67/0.85 % (2284577)------------------------------ % 3.67/0.85 % (2284577)------------------------------ % 3.67/0.85 % (2284579)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1378391254:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.67/0.85 % (2284569)Instruction limit reached! % 3.67/0.85 % (2284569)------------------------------ % 3.67/0.85 % (2284569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/0.85 % (2284569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/0.85 % (2284569)CaDiCaL version: 2.1.3 % 3.67/0.85 % (2284569)Termination reason: Instruction limit % 3.67/0.85 % (2284569)Termination phase: Saturation % 3.67/0.85 % (2284569)Time elapsed: 0.060 s % 3.67/0.85 % (2284569)Peak memory usage: 14 MB % 3.67/0.85 % (2284569)Instructions burned: 160 (million) % 3.67/0.85 % (2284581)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=1187220206:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.67/0.85 % (2284566)Instruction limit reached! % 3.67/0.85 % (2284566)------------------------------ % 3.67/0.85 % (2284566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/0.85 % (2284566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/0.85 % (2284566)CaDiCaL version: 2.1.3 % 3.67/0.85 % (2284566)Termination reason: Instruction limit % 3.67/0.85 % (2284566)Termination phase: Saturation % 3.67/0.85 % (2284566)Time elapsed: 0.067 s % 3.67/0.85 % (2284566)Peak memory usage: 12 MB % 3.67/0.85 % (2284566)Instructions burned: 103 (million) % 3.67/0.85 % (2284567)Instruction limit reached! % 3.67/0.85 % (2284567)------------------------------ % 3.67/0.85 % (2284567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.74/1.10 % (2284567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.10 % (2284567)CaDiCaL version: 2.1.3 % 5.74/1.10 % (2284567)Termination reason: Instruction limit % 5.74/1.10 % (2284567)Termination phase: Saturation % 5.74/1.10 % (2284567)Time elapsed: 0.075 s % 5.74/1.10 % (2284567)Peak memory usage: 13 MB % 5.74/1.10 % (2284567)Instructions burned: 116 (million) % 5.74/1.10 % (2284568)Instruction limit reached! % 5.74/1.10 % (2284568)------------------------------ % 5.74/1.10 % (2284568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.74/1.10 % (2284568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.10 % (2284568)CaDiCaL version: 2.1.3 % 5.74/1.10 % (2284568)Termination reason: Instruction limit % 5.74/1.10 % (2284568)Termination phase: Saturation % 5.74/1.10 % (2284568)Time elapsed: 0.081 s % 5.74/1.10 % (2284568)Peak memory usage: 13 MB % 5.74/1.10 % (2284568)Instructions burned: 131 (million) % 5.74/1.10 % (2284583)ott-21_1_sil=16000:fs=off:random_seed=4182378379:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 5.74/1.10 % (2284584)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=450998194:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.74/1.10 % (2284585)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3708541406:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.74/1.10 % (2284585)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.74/1.10 % (2284585)Terminated due to inappropriate strategy. % 5.74/1.10 % (2284585)------------------------------ % 5.74/1.10 % (2284585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.74/1.10 % (2284585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.10 % (2284585)CaDiCaL version: 2.1.3 % 5.74/1.10 % (2284585)Termination reason: Inappropriate % 5.74/1.10 % (2284585)Time elapsed: 0.002 s % 5.74/1.10 % (2284585)Peak memory usage: 11 MB % 5.74/1.10 % (2284585)Instructions burned: 3 (million) % 5.74/1.10 % (2284585)------------------------------ % 5.74/1.10 % (2284585)------------------------------ % 5.74/1.10 % (2284589)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1292484549:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.74/1.10 % (2284579)Instruction limit reached! % 5.74/1.10 % (2284579)------------------------------ % 5.74/1.10 % (2284579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.74/1.10 % (2284579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.10 % (2284579)CaDiCaL version: 2.1.3 % 5.74/1.10 % (2284579)Termination reason: Instruction limit % 5.74/1.10 % (2284579)Termination phase: Saturation % 5.74/1.10 % (2284579)Time elapsed: 0.092 s % 5.74/1.10 % (2284579)Peak memory usage: 13 MB % 5.74/1.10 % (2284579)Instructions burned: 131 (million) % 5.74/1.10 % (2284591)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=124367291:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.74/1.10 % (2284591)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.74/1.10 % (2284591)Terminated due to inappropriate strategy. % 5.74/1.10 % (2284591)------------------------------ % 5.74/1.10 % (2284591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.74/1.10 % (2284591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.10 % (2284591)CaDiCaL version: 2.1.3 % 5.74/1.10 % (2284591)Termination reason: Inappropriate % 5.74/1.10 % (2284591)Time elapsed: 0.002 s % 5.74/1.10 % (2284591)Peak memory usage: 10 MB % 5.74/1.10 % (2284591)Instructions burned: 3 (million) % 5.74/1.10 % (2284591)------------------------------ % 5.74/1.10 % (2284591)------------------------------ % 5.74/1.10 % (2284583)Instruction limit reached! % 5.74/1.10 % (2284583)------------------------------ % 5.74/1.10 % (2284583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.74/1.10 % (2284583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.74/1.10 % (2284583)CaDiCaL version: 2.1.3 % 5.74/1.10 % (2284583)Termination reason: Instruction limit % 5.74/1.10 % (2284583)Termination phase: Saturation % 5.74/1.10 % (2284583)Time elapsed: 0.087 s % 5.74/1.10 % (2284583)Peak memory usage: 12 MB % 5.74/1.10 % (2284583)Instructions burned: 181 (million) % 5.74/1.10 % (2284593)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=708119014:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 20.64/3.14 % (2284594)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2822311898:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.64/3.14 % (2284581)Instruction limit reached! % 20.64/3.14 % (2284581)------------------------------ % 20.64/3.14 % (2284581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.64/3.14 % (2284581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.64/3.14 % (2284581)CaDiCaL version: 2.1.3 % 20.64/3.14 % (2284581)Termination reason: Instruction limit % 20.64/3.14 % (2284581)Termination phase: Saturation % 20.64/3.14 % (2284581)Time elapsed: 0.182 s % 20.64/3.14 % (2284581)Peak memory usage: 16 MB % 20.64/3.14 % (2284581)Instructions burned: 687 (million) % 20.64/3.14 % (2284597)fmb+10_1_sil=64000:random_seed=1013881004:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 20.64/3.14 % (2284597)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.64/3.14 % (2284597)Terminated due to inappropriate strategy. % 20.64/3.14 % (2284597)------------------------------ % 20.64/3.14 % (2284597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.64/3.14 % (2284597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.64/3.14 % (2284597)CaDiCaL version: 2.1.3 % 20.64/3.14 % (2284597)Termination reason: Inappropriate % 20.64/3.14 % (2284597)Time elapsed: 0.001 s % 20.64/3.14 % (2284597)Peak memory usage: 11 MB % 20.64/3.14 % (2284597)Instructions burned: 3 (million) % 20.64/3.14 % (2284597)------------------------------ % 20.64/3.14 % (2284597)------------------------------ % 20.64/3.14 % (2284599)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2443367691:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 20.64/3.14 % (2284599)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.64/3.14 % (2284599)Terminated due to inappropriate strategy. % 20.64/3.14 % (2284599)------------------------------ % 20.64/3.14 % (2284599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.64/3.14 % (2284599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.64/3.14 % (2284599)CaDiCaL version: 2.1.3 % 20.64/3.14 % (2284599)Termination reason: Inappropriate % 20.64/3.14 % (2284599)Time elapsed: 0.001 s % 20.64/3.14 % (2284599)Peak memory usage: 11 MB % 20.64/3.14 % (2284599)Instructions burned: 3 (million) % 20.64/3.14 % (2284599)------------------------------ % 20.64/3.14 % (2284599)------------------------------ % 20.64/3.14 % (2284601)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1316094824:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 20.64/3.14 % (2284601)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.64/3.14 % (2284601)Terminated due to inappropriate strategy. % 20.64/3.14 % (2284601)------------------------------ % 20.64/3.14 % (2284601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.64/3.14 % (2284601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.64/3.14 % (2284601)CaDiCaL version: 2.1.3 % 20.64/3.14 % (2284601)Termination reason: Inappropriate % 20.64/3.14 % (2284601)Time elapsed: 0.001 s % 20.64/3.14 % (2284601)Peak memory usage: 10 MB % 20.64/3.14 % (2284601)Instructions burned: 3 (million) % 20.64/3.14 % (2284601)------------------------------ % 20.64/3.14 % (2284601)------------------------------ % 20.64/3.14 % (2284603)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1673091606:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 20.64/3.14 % (2284584)Instruction limit reached! % 20.64/3.14 % (2284584)------------------------------ % 20.64/3.14 % (2284584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.64/3.14 % (2284584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.64/3.14 % (2284584)CaDiCaL version: 2.1.3 % 20.64/3.14 % (2284584)Termination reason: Instruction limit % 20.64/3.14 % (2284584)Termination phase: Saturation % 20.64/3.14 % (2284584)Time elapsed: 0.270 s % 20.64/3.14 % (2284584)Peak memory usage: 13 MB % 20.64/3.14 % (2284584)Instructions burned: 478 (million) % 20.64/3.14 % (2284605)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1166993212:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 20.64/3.14 % (2284593)Instruction limit reached! % 20.64/3.14 % (2284593)------------------------------ % 28.20/4.23 % (2284593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.20/4.23 % (2284593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.20/4.23 % (2284593)CaDiCaL version: 2.1.3 % 28.20/4.23 % (2284593)Termination reason: Instruction limit % 28.20/4.23 % (2284593)Termination phase: Saturation % 28.20/4.23 % (2284593)Time elapsed: 0.413 s % 28.20/4.23 % (2284593)Peak memory usage: 20 MB % 28.20/4.23 % (2284593)Instructions burned: 694 (million) % 28.20/4.23 % (2284607)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3167833617:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 28.20/4.23 % (2284607)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.20/4.23 % (2284607)Terminated due to inappropriate strategy. % 28.20/4.23 % (2284607)------------------------------ % 28.20/4.23 % (2284607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.20/4.23 % (2284607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.20/4.23 % (2284607)CaDiCaL version: 2.1.3 % 28.20/4.23 % (2284607)Termination reason: Inappropriate % 28.20/4.23 % (2284607)Time elapsed: 0.002 s % 28.20/4.23 % (2284607)Peak memory usage: 11 MB % 28.20/4.23 % (2284607)Instructions burned: 4 (million) % 28.20/4.23 % (2284607)------------------------------ % 28.20/4.23 % (2284607)------------------------------ % 28.20/4.23 % (2284609)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3871087810:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 28.20/4.23 % (2284609)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.20/4.23 % (2284609)Terminated due to inappropriate strategy. % 28.20/4.23 % (2284609)------------------------------ % 28.20/4.23 % (2284609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.20/4.23 % (2284609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.20/4.23 % (2284609)CaDiCaL version: 2.1.3 % 28.20/4.23 % (2284609)Termination reason: Inappropriate % 28.20/4.23 % (2284609)Time elapsed: 0.002 s % 28.20/4.23 % (2284609)Peak memory usage: 11 MB % 28.20/4.23 % (2284609)Instructions burned: 3 (million) % 28.20/4.23 % (2284609)------------------------------ % 28.20/4.23 % (2284609)------------------------------ % 28.20/4.23 % (2284611)ott-2_1_sil=16000:newcnf=on:random_seed=1108417381:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 28.20/4.23 % (2284594)Instruction limit reached! % 28.20/4.23 % (2284594)------------------------------ % 28.20/4.23 % (2284594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.20/4.23 % (2284594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.20/4.23 % (2284594)CaDiCaL version: 2.1.3 % 28.20/4.23 % (2284594)Termination reason: Instruction limit % 28.20/4.23 % (2284594)Termination phase: Saturation % 28.20/4.23 % (2284594)Time elapsed: 0.505 s % 28.20/4.23 % (2284594)Peak memory usage: 19 MB % 28.20/4.23 % (2284594)Instructions burned: 881 (million) % 28.20/4.23 % (2284613)ott+10_1_sil=32000:tgt=ground:random_seed=2056173125:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 28.20/4.23 % (2284589)Instruction limit reached! % 28.20/4.23 % (2284589)------------------------------ % 28.20/4.23 % (2284589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.20/4.23 % (2284589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.20/4.23 % (2284589)CaDiCaL version: 2.1.3 % 28.20/4.23 % (2284589)Termination reason: Instruction limit % 28.20/4.23 % (2284589)Termination phase: Saturation % 28.20/4.23 % (2284589)Time elapsed: 0.697 s % 28.20/4.23 % (2284589)Peak memory usage: 20 MB % 28.20/4.23 % (2284589)Instructions burned: 1179 (million) % 28.20/4.23 % (2284615)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=666423158:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 28.20/4.23 % (2284615)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.20/4.23 % (2284615)Terminated due to inappropriate strategy. % 28.20/4.23 % (2284615)------------------------------ % 28.20/4.23 % (2284615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.20/4.23 % (2284615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.20/4.23 % (2284615)CaDiCaL version: 2.1.3 % 28.20/4.23 % (2284615)Termination reason: Inappropriate % 28.20/4.23 % (2284615)Time elapsed: 0.002 s % 28.20/4.23 % (2284615)Peak memory usage: 11 MB % 28.20/4.23 % (2284615)Instructions burned: 4 (million) % 108.40/15.56 % (2284615)------------------------------ % 108.40/15.56 % (2284615)------------------------------ % 108.40/15.56 % (2284617)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3712716152:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 108.40/15.56 % (2284611)Instruction limit reached! % 108.40/15.56 % (2284611)------------------------------ % 108.40/15.56 % (2284611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.40/15.56 % (2284611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.40/15.56 % (2284611)CaDiCaL version: 2.1.3 % 108.40/15.56 % (2284611)Termination reason: Instruction limit % 108.40/15.56 % (2284611)Termination phase: Saturation % 108.40/15.56 % (2284611)Time elapsed: 0.538 s % 108.40/15.56 % (2284611)Peak memory usage: 18 MB % 108.40/15.56 % (2284611)Instructions burned: 870 (million) % 108.40/15.56 % (2284605)Instruction limit reached! % 108.40/15.56 % (2284605)------------------------------ % 108.40/15.56 % (2284605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.40/15.56 % (2284605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.40/15.56 % (2284605)CaDiCaL version: 2.1.3 % 108.40/15.56 % (2284605)Termination reason: Instruction limit % 108.40/15.56 % (2284605)Termination phase: Saturation % 108.40/15.56 % (2284605)Time elapsed: 0.815 s % 108.40/15.56 % (2284605)Peak memory usage: 28 MB % 108.40/15.56 % (2284605)Instructions burned: 1472 (million) % 108.40/15.56 % (2284619)dis+21_1_sil=32000:sas=cadical:random_seed=732536276:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 108.40/15.56 % (2284620)ott+11_1_sil=16000:gs=on:random_seed=1133854804:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 108.40/15.56 % (2284603)Instruction limit reached! % 108.40/15.56 % (2284603)------------------------------ % 108.40/15.56 % (2284603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.40/15.56 % (2284603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.40/15.56 % (2284603)CaDiCaL version: 2.1.3 % 108.40/15.56 % (2284603)Termination reason: Instruction limit % 108.40/15.56 % (2284603)Termination phase: Saturation % 108.40/15.56 % (2284603)Time elapsed: 1.500 s % 108.40/15.56 % (2284603)Peak memory usage: 43 MB % 108.40/15.56 % (2284603)Instructions burned: 5131 (million) % 108.40/15.56 % (2284623)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1370425231:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 108.40/15.56 % (2284623)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.40/15.56 % (2284623)Terminated due to inappropriate strategy. % 108.40/15.56 % (2284623)------------------------------ % 108.40/15.56 % (2284623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.40/15.56 % (2284623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.40/15.56 % (2284623)CaDiCaL version: 2.1.3 % 108.40/15.56 % (2284623)Termination reason: Inappropriate % 108.40/15.56 % (2284623)Time elapsed: 0.001 s % 108.40/15.56 % (2284623)Peak memory usage: 11 MB % 108.40/15.56 % (2284623)Instructions burned: 3 (million) % 108.40/15.56 % (2284623)------------------------------ % 108.40/15.56 % (2284623)------------------------------ % 108.40/15.56 % (2284625)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1183334777:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 108.40/15.56 % (2284620)Instruction limit reached! % 108.40/15.56 % (2284620)------------------------------ % 108.40/15.56 % (2284620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.40/15.56 % (2284620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.40/15.56 % (2284620)CaDiCaL version: 2.1.3 % 108.40/15.56 % (2284620)Termination reason: Instruction limit % 108.40/15.56 % (2284620)Termination phase: Saturation % 108.40/15.56 % (2284620)Time elapsed: 1.387 s % 108.40/15.56 % (2284620)Peak memory usage: 25 MB % 108.40/15.56 % (2284620)Instructions burned: 2252 (million) % 108.40/15.56 % (2284627)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1393000458:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 108.40/15.56 % (2284617)Instruction limit reached! % 108.40/15.56 % (2284617)------------------------------ % 108.40/15.56 % (2284617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.40/15.56 % (2284617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.40/15.56 % (2284617)CaDiCaL version: 2.1.3 % 108.40/15.56 % (2284617)Termination reason: Instruction limit % 121.19/17.37 % (2284617)Termination phase: Saturation % 121.19/17.37 % (2284617)Time elapsed: 2.015 s % 121.19/17.37 % (2284617)Peak memory usage: 32 MB % 121.19/17.37 % (2284617)Instructions burned: 3512 (million) % 121.19/17.37 % (2284629)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4246026859:i=5211_2970 on theBenchmark for (2970ds/5211Mi) % 121.19/17.37 % (2284625)Instruction limit reached! % 121.19/17.37 % (2284625)------------------------------ % 121.19/17.37 % (2284625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.19/17.37 % (2284625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.19/17.37 % (2284625)CaDiCaL version: 2.1.3 % 121.19/17.37 % (2284625)Termination reason: Instruction limit % 121.19/17.37 % (2284625)Termination phase: Saturation % 121.19/17.37 % (2284625)Time elapsed: 1.216 s % 121.19/17.37 % (2284625)Peak memory usage: 52 MB % 121.19/17.37 % (2284625)Instructions burned: 4592 (million) % 121.19/17.37 % (2284631)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2417031069:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 121.19/17.37 % (2284631)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.19/17.37 % (2284631)Terminated due to inappropriate strategy. % 121.19/17.37 % (2284631)------------------------------ % 121.19/17.37 % (2284631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.19/17.37 % (2284631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.19/17.37 % (2284631)CaDiCaL version: 2.1.3 % 121.19/17.37 % (2284631)Termination reason: Inappropriate % 121.19/17.37 % (2284631)Time elapsed: 0.001 s % 121.19/17.37 % (2284631)Peak memory usage: 11 MB % 121.19/17.37 % (2284631)Instructions burned: 4 (million) % 121.19/17.37 % (2284631)------------------------------ % 121.19/17.37 % (2284631)------------------------------ % 121.19/17.37 % (2284633)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3925293285:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 121.19/17.37 % (2284633)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.19/17.37 % (2284633)Terminated due to inappropriate strategy. % 121.19/17.37 % (2284633)------------------------------ % 121.19/17.37 % (2284633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.19/17.37 % (2284633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.19/17.37 % (2284633)CaDiCaL version: 2.1.3 % 121.19/17.37 % (2284633)Termination reason: Inappropriate % 121.19/17.37 % (2284633)Time elapsed: 0.001 s % 121.19/17.37 % (2284633)Peak memory usage: 11 MB % 121.19/17.37 % (2284633)Instructions burned: 3 (million) % 121.19/17.37 % (2284633)------------------------------ % 121.19/17.37 % (2284633)------------------------------ % 121.19/17.37 % (2284635)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=490177484:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 121.19/17.37 % (2284635)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.19/17.37 % (2284635)Terminated due to inappropriate strategy. % 121.19/17.37 % (2284635)------------------------------ % 121.19/17.37 % (2284635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.19/17.37 % (2284635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.19/17.37 % (2284635)CaDiCaL version: 2.1.3 % 121.19/17.37 % (2284635)Termination reason: Inappropriate % 121.19/17.37 % (2284635)Time elapsed: 0.001 s % 121.19/17.37 % (2284635)Peak memory usage: 11 MB % 121.19/17.37 % (2284635)Instructions burned: 3 (million) % 121.19/17.37 % (2284635)------------------------------ % 121.19/17.37 % (2284635)------------------------------ % 121.19/17.37 % (2284637)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4042353102:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 121.19/17.37 % (2284619)Instruction limit reached! % 121.19/17.37 % (2284619)------------------------------ % 121.19/17.37 % (2284619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.19/17.37 % (2284619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.19/17.37 % (2284619)CaDiCaL version: 2.1.3 % 121.19/17.37 % (2284619)Termination reason: Instruction limit % 121.19/17.37 % (2284619)Termination phase: Saturation % 121.19/17.37 % (2284619)Time elapsed: 2.216 s % 121.19/17.37 % (2284619)Peak memory usage: 32 MB % 121.19/17.37 % (2284619)Instructions burned: 3775 (million) % 121.19/17.37 % (2284639)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3482335723:i=8173:av=off_2965 on theBenchmark for (2965ds/8173Mi) % 121.19/17.37 % (2284613)Instruction limit reached! % 121.90/17.48 % (2284613)------------------------------ % 121.90/17.48 % (2284613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.90/17.48 % (2284613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.90/17.48 % (2284613)CaDiCaL version: 2.1.3 % 121.90/17.48 % (2284613)Termination reason: Instruction limit % 121.90/17.48 % (2284613)Termination phase: Saturation % 121.90/17.48 % (2284613)Time elapsed: 3.256 s % 121.90/17.48 % (2284613)Peak memory usage: 38 MB % 121.90/17.48 % (2284613)Instructions burned: 5115 (million) % 121.90/17.48 % (2284641)dis+10_16:1_sil=16000:random_seed=390484563:i=9155:fsr=off_2959 on theBenchmark for (2959ds/9155Mi) % 121.90/17.48 % (2284629)Instruction limit reached! % 121.90/17.48 % (2284629)------------------------------ % 121.90/17.48 % (2284629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.90/17.48 % (2284629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.90/17.48 % (2284629)CaDiCaL version: 2.1.3 % 121.90/17.48 % (2284629)Termination reason: Instruction limit % 121.90/17.48 % (2284629)Termination phase: Saturation % 121.90/17.48 % (2284629)Time elapsed: 2.857 s % 121.90/17.48 % (2284629)Peak memory usage: 51 MB % 121.90/17.48 % (2284629)Instructions burned: 5212 (million) % 121.90/17.48 % (2284643)ott-3_8_sil=64000:random_seed=2253571714:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi) % 121.90/17.48 % (2284639)Instruction limit reached! % 121.90/17.48 % (2284639)------------------------------ % 121.90/17.48 % (2284639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.90/17.48 % (2284639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.90/17.48 % (2284639)CaDiCaL version: 2.1.3 % 121.90/17.48 % (2284639)Termination reason: Instruction limit % 121.90/17.48 % (2284639)Termination phase: Saturation % 121.90/17.48 % (2284639)Time elapsed: 5.358 s % 121.90/17.48 % (2284639)Peak memory usage: 63 MB % 121.90/17.48 % (2284639)Instructions burned: 8173 (million) % 121.90/17.48 % (2284641)Instruction limit reached! % 121.90/17.48 % (2284641)------------------------------ % 121.90/17.48 % (2284641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.90/17.48 % (2284641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.90/17.48 % (2284641)CaDiCaL version: 2.1.3 % 121.90/17.48 % (2284641)Termination reason: Instruction limit % 121.90/17.48 % (2284641)Termination phase: Saturation % 121.90/17.48 % (2284641)Time elapsed: 4.829 s % 121.90/17.48 % (2284641)Peak memory usage: 53 MB % 121.90/17.48 % (2284641)Instructions burned: 9157 (million) % 121.90/17.48 % (2284645)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3649327212:fmbsr=2:i=32576_2911 on theBenchmark for (2911ds/32576Mi) % 121.90/17.48 % (2284645)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.90/17.48 % (2284645)Terminated due to inappropriate strategy. % 121.90/17.48 % (2284645)------------------------------ % 121.90/17.48 % (2284645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.90/17.48 % (2284645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.90/17.48 % (2284645)CaDiCaL version: 2.1.3 % 121.90/17.48 % (2284645)Termination reason: Inappropriate % 121.90/17.48 % (2284645)Time elapsed: 0.002 s % 121.90/17.48 % (2284645)Peak memory usage: 11 MB % 121.90/17.48 % (2284645)Instructions burned: 4 (million) % 121.90/17.48 % (2284645)------------------------------ % 121.90/17.48 % (2284645)------------------------------ % 121.90/17.48 % (2284646)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3672177132:i=11404_2911 on theBenchmark for (2911ds/11404Mi) % 121.90/17.48 % (2284648)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1491579833:i=14134_2911 on theBenchmark for (2911ds/14134Mi) % 121.90/17.48 % (2284637)Instruction limit reached! % 121.90/17.48 % (2284637)------------------------------ % 121.90/17.48 % (2284637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.90/17.48 % (2284637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.90/17.48 % (2284637)CaDiCaL version: 2.1.3 % 121.90/17.48 % (2284637)Termination reason: Instruction limit % 121.90/17.48 % (2284637)Termination phase: Saturation % 121.90/17.48 % (2284637)Time elapsed: 8.287 s % 121.90/17.48 % (2284637)Peak memory usage: 203 MB % 121.90/17.48 % (2284637)Instructions burned: 22566 (million) % 121.90/17.48 % (2284782)dis+33_16_sil=32000:sac=on:random_seed=2994801616:i=15851:nm=0_2885 on theBenchmark for (2885ds/15851Mi) % 121.90/17.48 % (2284627)Instruction limit reached! % 121.90/17.48 % (2284627)------------------------------ % 121.90/17.48 % (2284627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.13/21.49 % (2284627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.13/21.49 % (2284627)CaDiCaL version: 2.1.3 % 150.13/21.49 % (2284627)Termination reason: Instruction limit % 150.13/21.49 % (2284627)Termination phase: Saturation % 150.13/21.49 % (2284627)Time elapsed: 12.667 s % 150.13/21.49 % (2284627)Peak memory usage: 142 MB % 150.13/21.49 % (2284627)Instructions burned: 29342 (million) % 150.13/21.49 % (2285012)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=136013622:avsq=on:i=17627:add=on:amm=off_2846 on theBenchmark for (2846ds/17627Mi) % 150.13/21.49 % (2284782)Instruction limit reached! % 150.13/21.49 % (2284782)------------------------------ % 150.13/21.49 % (2284782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.13/21.49 % (2284782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.13/21.49 % (2284782)CaDiCaL version: 2.1.3 % 150.13/21.49 % (2284782)Termination reason: Instruction limit % 150.13/21.49 % (2284782)Termination phase: Saturation % 150.13/21.49 % (2284782)Time elapsed: 4.435 s % 150.13/21.49 % (2284782)Peak memory usage: 169 MB % 150.13/21.49 % (2284782)Instructions burned: 15854 (million) % 150.13/21.49 % (2285014)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2546496913:s2a=on:i=53295_2841 on theBenchmark for (2841ds/53295Mi) % 150.13/21.49 % (2284646)Instruction limit reached! % 150.13/21.49 % (2284646)------------------------------ % 150.13/21.49 % (2284646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.13/21.49 % (2284646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.13/21.49 % (2284646)CaDiCaL version: 2.1.3 % 150.13/21.49 % (2284646)Termination reason: Instruction limit % 150.13/21.49 % (2284646)Termination phase: Saturation % 150.13/21.49 % (2284646)Time elapsed: 7.620 s % 150.13/21.49 % (2284646)Peak memory usage: 59 MB % 150.13/21.49 % (2284646)Instructions burned: 11404 (million) % 150.13/21.49 % (2285016)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1050499574:i=26857:ins=20_2834 on theBenchmark for (2834ds/26857Mi) % 150.13/21.49 % (2285016)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.13/21.49 % (2285016)Terminated due to inappropriate strategy. % 150.13/21.49 % (2285016)------------------------------ % 150.13/21.49 % (2285016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.13/21.49 % (2285016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.13/21.49 % (2285016)CaDiCaL version: 2.1.3 % 150.13/21.49 % (2285016)Termination reason: Inappropriate % 150.13/21.49 % (2285016)Time elapsed: 0.002 s % 150.13/21.49 % (2285016)Peak memory usage: 11 MB % 150.13/21.49 % (2285016)Instructions burned: 3 (million) % 150.13/21.49 % (2285016)------------------------------ % 150.13/21.49 % (2285016)------------------------------ % 150.13/21.49 % (2285018)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4013078176:i=28120:bs=on:fsr=off_2834 on theBenchmark for (2834ds/28120Mi) % 150.13/21.49 % (2284643)Instruction limit reached! % 150.13/21.49 % (2284643)------------------------------ % 150.13/21.49 % (2284643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.13/21.49 % (2284643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.13/21.49 % (2284643)CaDiCaL version: 2.1.3 % 150.13/21.49 % (2284643)Termination reason: Instruction limit % 150.13/21.49 % (2284643)Termination phase: Saturation % 150.13/21.49 % (2284643)Time elapsed: 11.276 s % 150.13/21.49 % (2284643)Peak memory usage: 87 MB % 150.13/21.49 % (2284643)Instructions burned: 20140 (million) % 150.13/21.49 % (2285020)fmb+10_1_sil=256000:fmbss=7:random_seed=101510042:fmbsr=1.6:i=182295_2828 on theBenchmark for (2828ds/182295Mi) % 150.13/21.49 % (2285020)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.13/21.49 % (2285020)Terminated due to inappropriate strategy. % 150.13/21.49 % (2285020)------------------------------ % 150.13/21.49 % (2285020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.13/21.49 % (2285020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.13/21.49 % (2285020)CaDiCaL version: 2.1.3 % 150.13/21.49 % (2285020)Termination reason: Inappropriate % 150.13/21.49 % (2285020)Time elapsed: 0.002 s % 150.13/21.49 % (2285020)Peak memory usage: 11 MB % 150.13/21.49 % (2285020)Instructions burned: 3 (million) % 150.13/21.49 % (2285020)------------------------------ % 150.13/21.49 % (2285020)------------------------------ % 150.13/21.49 % (2285022)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=484702395:i=44625:gsp=on_2828 on theBenchmark for (2828ds/44625Mi) % 163.05/23.23 % (2285022)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 163.05/23.23 % (2285022)Terminated due to inappropriate strategy. % 163.05/23.23 % (2285022)------------------------------ % 163.05/23.23 % (2285022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.05/23.23 % (2285022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.05/23.23 % (2285022)CaDiCaL version: 2.1.3 % 163.05/23.23 % (2285022)Termination reason: Inappropriate % 163.05/23.23 % (2285022)Time elapsed: 0.002 s % 163.05/23.23 % (2285022)Peak memory usage: 11 MB % 163.05/23.23 % (2285022)Instructions burned: 3 (million) % 163.05/23.23 % (2285022)------------------------------ % 163.05/23.23 % (2285022)------------------------------ % 163.05/23.23 % (2285024)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3825865241:i=160505_2828 on theBenchmark for (2828ds/160505Mi) % 163.05/23.23 % (2285024)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 163.05/23.23 % (2285024)Terminated due to inappropriate strategy. % 163.05/23.23 % (2285024)------------------------------ % 163.05/23.23 % (2285024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.05/23.23 % (2285024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.05/23.23 % (2285024)CaDiCaL version: 2.1.3 % 163.05/23.23 % (2285024)Termination reason: Inappropriate % 163.05/23.23 % (2285024)Time elapsed: 0.002 s % 163.05/23.23 % (2285024)Peak memory usage: 11 MB % 163.05/23.23 % (2285024)Instructions burned: 3 (million) % 163.05/23.23 % (2285024)------------------------------ % 163.05/23.23 % (2285024)------------------------------ % 163.05/23.23 % (2285026)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1985999941:fmbsr=1.3:i=225729_2828 on theBenchmark for (2828ds/225729Mi) % 163.05/23.23 % (2285026)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 163.05/23.23 % (2285026)Terminated due to inappropriate strategy. % 163.05/23.23 % (2285026)------------------------------ % 163.05/23.23 % (2285026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.05/23.23 % (2285026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.05/23.23 % (2285026)CaDiCaL version: 2.1.3 % 163.05/23.23 % (2285026)Termination reason: Inappropriate % 163.05/23.23 % (2285026)Time elapsed: 0.002 s % 163.05/23.23 % (2285026)Peak memory usage: 11 MB % 163.05/23.23 % (2285026)Instructions burned: 3 (million) % 163.05/23.23 % (2285026)------------------------------ % 163.05/23.23 % (2285026)------------------------------ % 163.05/23.23 % (2285028)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2022362963:fmbsr=2:i=185024:ins=7_2828 on theBenchmark for (2828ds/185024Mi) % 163.05/23.23 % (2285028)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 163.05/23.23 % (2285028)Terminated due to inappropriate strategy. % 163.05/23.23 % (2285028)------------------------------ % 163.05/23.23 % (2285028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.05/23.23 % (2285028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.05/23.23 % (2285028)CaDiCaL version: 2.1.3 % 163.05/23.23 % (2285028)Termination reason: Inappropriate % 163.05/23.23 % (2285028)Time elapsed: 0.002 s % 163.05/23.23 % (2285028)Peak memory usage: 11 MB % 163.05/23.23 % (2285028)Instructions burned: 3 (million) % 163.05/23.23 % (2285028)------------------------------ % 163.05/23.23 % (2285028)------------------------------ % 163.05/23.23 % (2285030)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2070464648:rtra=on_2827 on theBenchmark for (2827ds/0Mi) % 163.05/23.23 % (2285030)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 163.05/23.23 % (2285030)Terminated due to inappropriate strategy. % 163.05/23.23 % (2285030)------------------------------ % 163.05/23.23 % (2285030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.05/23.23 % (2285030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.05/23.23 % (2285030)CaDiCaL version: 2.1.3 % 163.05/23.23 % (2285030)Termination reason: Inappropriate % 163.05/23.23 % (2285030)Time elapsed: 0.003 s % 163.05/23.23 % (2285030)Peak memory usage: 11 MB % 163.05/23.23 % (2285030)Instructions burned: 4 (million) % 163.05/23.23 % (2285030)------------------------------ % 163.05/23.23 % (2285030)------------------------------ % 163.05/23.23 % (2285032)% WARNING: option uhcvi not known. % 163.05/23.23 % (2285032)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=44981828:i=271062:add=off:rtra=on:rawr=on_2827 on theBenchmark for (2827ds/271062Mi) % 188.62/26.88 % (2284648)Instruction limit reached! % 188.62/26.88 % (2284648)------------------------------ % 188.62/26.88 % (2284648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.62/26.88 % (2284648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.62/26.88 % (2284648)CaDiCaL version: 2.1.3 % 188.62/26.88 % (2284648)Termination reason: Instruction limit % 188.62/26.88 % (2284648)Termination phase: Saturation % 188.62/26.88 % (2284648)Time elapsed: 9.343 s % 188.62/26.88 % (2284648)Peak memory usage: 73 MB % 188.62/26.88 % (2284648)Instructions burned: 14135 (million) % 188.62/26.88 % (2285034)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2786501401:i=176048:add=on:rtra=on:rawr=on_2817 on theBenchmark for (2817ds/176048Mi) % 188.62/26.88 % (2285012)Instruction limit reached! % 188.62/26.88 % (2285012)------------------------------ % 188.62/26.88 % (2285012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.62/26.88 % (2285012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.62/26.88 % (2285012)CaDiCaL version: 2.1.3 % 188.62/26.88 % (2285012)Termination reason: Instruction limit % 188.62/26.88 % (2285012)Termination phase: Saturation % 188.62/26.88 % (2285012)Time elapsed: 5.111 s % 188.62/26.88 % (2285012)Peak memory usage: 31 MB % 188.62/26.88 % (2285012)Instructions burned: 17629 (million) % 188.62/26.88 % (2285036)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1104753011:i=206:fgj=on:rtra=on_2795 on theBenchmark for (2795ds/206Mi) % 188.62/26.88 % (2285036)Instruction limit reached! % 188.62/26.88 % (2285036)------------------------------ % 188.62/26.88 % (2285036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.62/26.88 % (2285036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.62/26.88 % (2285036)CaDiCaL version: 2.1.3 % 188.62/26.88 % (2285036)Termination reason: Instruction limit % 188.62/26.88 % (2285036)Termination phase: Saturation % 188.62/26.88 % (2285036)Time elapsed: 0.132 s % 188.62/26.88 % (2285036)Peak memory usage: 14 MB % 188.62/26.88 % (2285036)Instructions burned: 206 (million) % 188.62/26.88 % (2285038)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=628805994:i=232:rtra=on_2793 on theBenchmark for (2793ds/232Mi) % 188.62/26.88 % (2285038)Instruction limit reached! % 188.62/26.88 % (2285038)------------------------------ % 188.62/26.88 % (2285038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.62/26.88 % (2285038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.62/26.88 % (2285038)CaDiCaL version: 2.1.3 % 188.62/26.88 % (2285038)Termination reason: Instruction limit % 188.62/26.88 % (2285038)Termination phase: Saturation % 188.62/26.88 % (2285038)Time elapsed: 0.149 s % 188.62/26.88 % (2285038)Peak memory usage: 14 MB % 188.62/26.88 % (2285038)Instructions burned: 233 (million) % 188.62/26.88 % (2285040)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2259451205:i=262:rtra=on_2791 on theBenchmark for (2791ds/262Mi) % 188.62/26.88 % (2285040)Instruction limit reached! % 188.62/26.88 % (2285040)------------------------------ % 188.62/26.88 % (2285040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.62/26.88 % (2285040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.62/26.88 % (2285040)CaDiCaL version: 2.1.3 % 188.62/26.88 % (2285040)Termination reason: Instruction limit % 188.62/26.88 % (2285040)Termination phase: Saturation % 188.62/26.88 % (2285040)Time elapsed: 0.171 s % 188.62/26.88 % (2285040)Peak memory usage: 15 MB % 188.62/26.88 % (2285040)Instructions burned: 263 (million) % 188.62/26.88 % (2285042)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3305551865:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2790 on theBenchmark for (2790ds/318Mi) % 188.62/26.88 % (2285042)Instruction limit reached! % 188.62/26.88 % (2285042)------------------------------ % 188.62/26.88 % (2285042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.62/26.88 % (2285042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.62/26.88 % (2285042)CaDiCaL version: 2.1.3 % 188.62/26.88 % (2285042)Termination reason: Instruction limit % 188.62/26.88 % (2285042)Termination phase: Saturation % 188.62/26.88 % (2285042)Time elapsed: 0.227 s % 188.62/26.88 % (2285042)Peak memory usage: 15 MB % 188.62/26.88 % (2285042)Instructions burned: 318 (million) % 188.62/26.88 % (2285044)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=341805289:i=1428:nm=2:rtra=on_2787 on theBenchmark for (2787ds/1428Mi) % 234.86/33.37 % (2285044)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 234.86/33.37 % (2285044)Terminated due to inappropriate strategy. % 234.86/33.37 % (2285044)------------------------------ % 234.86/33.37 % (2285044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.86/33.37 % (2285044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.86/33.37 % (2285044)CaDiCaL version: 2.1.3 % 234.86/33.37 % (2285044)Termination reason: Inappropriate % 234.86/33.37 % (2285044)Time elapsed: 0.003 s % 234.86/33.37 % (2285044)Peak memory usage: 11 MB % 234.86/33.37 % (2285044)Instructions burned: 4 (million) % 234.86/33.37 % (2285044)------------------------------ % 234.86/33.37 % (2285044)------------------------------ % 234.86/33.37 % (2285046)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4183610113:i=262:bd=preordered:rtra=on:fsd=on_2787 on theBenchmark for (2787ds/262Mi) % 234.86/33.37 % (2285046)Instruction limit reached! % 234.86/33.37 % (2285046)------------------------------ % 234.86/33.37 % (2285046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.86/33.37 % (2285046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.86/33.37 % (2285046)CaDiCaL version: 2.1.3 % 234.86/33.37 % (2285046)Termination reason: Instruction limit % 234.86/33.37 % (2285046)Termination phase: Saturation % 234.86/33.37 % (2285046)Time elapsed: 0.184 s % 234.86/33.37 % (2285046)Peak memory usage: 14 MB % 234.86/33.37 % (2285046)Instructions burned: 263 (million) % 234.86/33.37 % (2285048)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=486509409:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2785 on theBenchmark for (2785ds/1368Mi) % 234.86/33.37 % (2285048)Instruction limit reached! % 234.86/33.37 % (2285048)------------------------------ % 234.86/33.37 % (2285048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.86/33.37 % (2285048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.86/33.37 % (2285048)CaDiCaL version: 2.1.3 % 234.86/33.37 % (2285048)Termination reason: Instruction limit % 234.86/33.37 % (2285048)Termination phase: Saturation % 234.86/33.37 % (2285048)Time elapsed: 0.662 s % 234.86/33.37 % (2285048)Peak memory usage: 19 MB % 234.86/33.37 % (2285048)Instructions burned: 1368 (million) % 234.86/33.37 % (2285050)ott-21_1_sil=16000:si=on:fs=off:random_seed=1197150874:i=360:av=off:fsr=off:rtra=on_2778 on theBenchmark for (2778ds/360Mi) % 234.86/33.37 % (2285050)Instruction limit reached! % 234.86/33.37 % (2285050)------------------------------ % 234.86/33.37 % (2285050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.86/33.37 % (2285050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.86/33.37 % (2285050)CaDiCaL version: 2.1.3 % 234.86/33.37 % (2285050)Termination reason: Instruction limit % 234.86/33.37 % (2285050)Termination phase: Saturation % 234.86/33.37 % (2285050)Time elapsed: 0.168 s % 234.86/33.37 % (2285050)Peak memory usage: 13 MB % 234.86/33.37 % (2285050)Instructions burned: 361 (million) % 234.86/33.37 % (2285052)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1021512169:i=954:bd=all:rtra=on_2776 on theBenchmark for (2776ds/954Mi) % 234.86/33.37 % (2285052)Instruction limit reached! % 234.86/33.37 % (2285052)------------------------------ % 234.86/33.37 % (2285052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.86/33.37 % (2285052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.86/33.37 % (2285052)CaDiCaL version: 2.1.3 % 234.86/33.37 % (2285052)Termination reason: Instruction limit % 234.86/33.37 % (2285052)Termination phase: Saturation % 234.86/33.37 % (2285052)Time elapsed: 0.610 s % 234.86/33.37 % (2285052)Peak memory usage: 15 MB % 234.86/33.37 % (2285052)Instructions burned: 954 (million) % 234.86/33.37 % (2285054)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2481798855:fmbsr=1.3:i=1730:ins=25:rtra=on_2770 on theBenchmark for (2770ds/1730Mi) % 234.86/33.37 % (2285054)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 234.86/33.37 % (2285054)Terminated due to inappropriate strategy. % 234.86/33.37 % (2285054)------------------------------ % 234.86/33.37 % (2285054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 234.86/33.37 % (2285054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.86/33.37 % (2285054)CaDiCaL version: 2.1.3 % 234.86/33.37 % (2285054)Termination reason: Inappropriate % 234.86/33.37 % (2285054)Time elapsed: 0.002 s % 286.85/40.69 % (2285054)Peak memory usage: 10 MB % 286.85/40.69 % (2285054)Instructions burned: 4 (million) % 286.85/40.69 % (2285054)------------------------------ % 286.85/40.69 % (2285054)------------------------------ % 286.85/40.69 % (2285056)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=297642236:i=2358:rtra=on_2769 on theBenchmark for (2769ds/2358Mi) % 286.85/40.69 % (2285056)Instruction limit reached! % 286.85/40.69 % (2285056)------------------------------ % 286.85/40.69 % (2285056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.85/40.69 % (2285056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.85/40.69 % (2285056)CaDiCaL version: 2.1.3 % 286.85/40.69 % (2285056)Termination reason: Instruction limit % 286.85/40.69 % (2285056)Termination phase: Saturation % 286.85/40.69 % (2285056)Time elapsed: 1.532 s % 286.85/40.69 % (2285056)Peak memory usage: 24 MB % 286.85/40.69 % (2285056)Instructions burned: 2359 (million) % 286.85/40.69 % (2285058)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3911594579:i=1778:ins=1:rtra=on_2754 on theBenchmark for (2754ds/1778Mi) % 286.85/40.69 % (2285058)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.85/40.69 % (2285058)Terminated due to inappropriate strategy. % 286.85/40.69 % (2285058)------------------------------ % 286.85/40.69 % (2285058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.85/40.69 % (2285058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.85/40.69 % (2285058)CaDiCaL version: 2.1.3 % 286.85/40.69 % (2285058)Termination reason: Inappropriate % 286.85/40.69 % (2285058)Time elapsed: 0.002 s % 286.85/40.69 % (2285058)Peak memory usage: 10 MB % 286.85/40.69 % (2285058)Instructions burned: 4 (million) % 286.85/40.69 % (2285058)------------------------------ % 286.85/40.69 % (2285058)------------------------------ % 286.85/40.69 % (2285060)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2716327057:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2754 on theBenchmark for (2754ds/1384Mi) % 286.85/40.69 % (2285060)Instruction limit reached! % 286.85/40.69 % (2285060)------------------------------ % 286.85/40.69 % (2285060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.85/40.69 % (2285060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.85/40.69 % (2285060)CaDiCaL version: 2.1.3 % 286.85/40.69 % (2285060)Termination reason: Instruction limit % 286.85/40.69 % (2285060)Termination phase: Saturation % 286.85/40.69 % (2285060)Time elapsed: 0.939 s % 286.85/40.69 % (2285060)Peak memory usage: 22 MB % 286.85/40.69 % (2285060)Instructions burned: 1385 (million) % 286.85/40.69 % (2285062)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1934648172:i=1758:kws=inv_precedence:fsr=off:rtra=on_2744 on theBenchmark for (2744ds/1758Mi) % 286.85/40.69 % (2285062)Instruction limit reached! % 286.85/40.69 % (2285062)------------------------------ % 286.85/40.69 % (2285062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.85/40.69 % (2285062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.85/40.69 % (2285062)CaDiCaL version: 2.1.3 % 286.85/40.69 % (2285062)Termination reason: Instruction limit % 286.85/40.69 % (2285062)Termination phase: Saturation % 286.85/40.69 % (2285062)Time elapsed: 1.044 s % 286.85/40.69 % (2285062)Peak memory usage: 29 MB % 286.85/40.69 % (2285062)Instructions burned: 1758 (million) % 286.85/40.69 % (2285196)fmb+10_1_sil=64000:si=on:random_seed=4146774324:i=44122:nm=2:rtra=on:gsp=on_2733 on theBenchmark for (2733ds/44122Mi) % 286.85/40.69 % (2285196)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.85/40.69 % (2285196)Terminated due to inappropriate strategy. % 286.85/40.69 % (2285196)------------------------------ % 286.85/40.69 % (2285196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.85/40.69 % (2285196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.85/40.69 % (2285196)CaDiCaL version: 2.1.3 % 286.85/40.69 % (2285196)Termination reason: Inappropriate % 286.85/40.69 % (2285196)Time elapsed: 0.003 s % 286.85/40.69 % (2285196)Peak memory usage: 11 MB % 286.85/40.69 % (2285196)Instructions burned: 4 (million) % 286.85/40.69 % (2285196)------------------------------ % 286.85/40.69 % (2285196)------------------------------ % 286.85/40.69 % (2285206)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1150630229:i=19030:nm=5:rtra=on_2733 on theBenchmark fTerminated % 300.22/42.54 % Vampire exiting % 300.22/42.54 Terminated %------------------------------------------------------------------------------