%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW587_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 : 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 01:40:29 PM UTC 2026 % Result : Timeout 293.83s 41.96s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWW587_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.00/0.11 % Computer : n012.cluster.edu % 0.00/0.11 % Model : x86_64 x86_64 % 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.11 % Memory : 8046.5625MB % 0.00/0.11 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.06/0.11 % DateTime : Mon Sep 28 14:19:49 UTC 2026 % 0.06/0.11 % CPUTime : % 0.06/0.12 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.13 Running first-order model finding % 0.06/0.13 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 % 2.19/0.48 % (3404339)Will run a generic schedule for satisfiability detection. % 2.19/0.48 % (3404347)% WARNING: option uhcvi not known. % 2.19/0.48 % (3404349)dis+10_1_sil=32000:sp=arity:random_seed=247615512:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.19/0.48 % (3404350)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1482987929:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.19/0.48 % (3404346)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1548783317_2999 on theBenchmark for (2999ds/0Mi) % 2.19/0.48 % (3404351)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2077084847:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.19/0.48 % (3404347)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2693202502:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.19/0.48 % (3404352)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2139369962:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.19/0.48 % (3404348)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1602245445:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.19/0.48 % (3404346)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.19/0.48 % (3404346)Terminated due to inappropriate strategy. % 2.19/0.48 % (3404346)------------------------------ % 2.19/0.48 % (3404346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.19/0.48 % (3404346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.19/0.48 % (3404346)CaDiCaL version: 2.1.3 % 2.19/0.48 % (3404346)Termination reason: Inappropriate % 2.19/0.48 % (3404346)Time elapsed: 0.004 s % 2.19/0.48 % (3404346)Peak memory usage: 10 MB % 2.19/0.48 % (3404346)Instructions burned: 15 (million) % 2.19/0.48 % (3404346)------------------------------ % 2.19/0.48 % (3404346)------------------------------ % 2.19/0.48 % (3404366)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4162480102:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.19/0.48 % (3404366)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.19/0.48 % (3404366)Terminated due to inappropriate strategy. % 2.19/0.48 % (3404366)------------------------------ % 2.19/0.48 % (3404366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.19/0.48 % (3404366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.19/0.48 % (3404366)CaDiCaL version: 2.1.3 % 2.19/0.48 % (3404366)Termination reason: Inappropriate % 2.19/0.48 % (3404366)Time elapsed: 0.003 s % 2.19/0.48 % (3404366)Peak memory usage: 10 MB % 2.19/0.48 % (3404366)Instructions burned: 12 (million) % 2.19/0.48 % (3404366)------------------------------ % 2.19/0.48 % (3404366)------------------------------ % 2.19/0.48 % (3404350)Instruction limit reached! % 2.19/0.48 % (3404350)------------------------------ % 2.19/0.48 % (3404350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.19/0.48 % (3404350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.19/0.48 % (3404350)CaDiCaL version: 2.1.3 % 2.19/0.48 % (3404350)Termination reason: Instruction limit % 2.19/0.48 % (3404350)Termination phase: Saturation % 2.19/0.48 % (3404350)Time elapsed: 0.029 s % 2.19/0.48 % (3404350)Peak memory usage: 12 MB % 2.19/0.48 % (3404350)Instructions burned: 117 (million) % 2.19/0.48 % (3404376)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3470070140:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.19/0.48 % (3404351)Instruction limit reached! % 2.19/0.48 % (3404351)------------------------------ % 2.19/0.48 % (3404351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.19/0.48 % (3404351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.19/0.48 % (3404351)CaDiCaL version: 2.1.3 % 2.19/0.48 % (3404351)Termination reason: Instruction limit % 2.19/0.48 % (3404351)Termination phase: Saturation % 2.19/0.48 % (3404351)Time elapsed: 0.032 s % 2.19/0.48 % (3404351)Peak memory usage: 12 MB % 2.19/0.48 % (3404351)Instructions burned: 132 (million) % 2.19/0.48 % (3404349)Instruction limit reached! % 2.19/0.48 % (3404349)------------------------------ % 2.19/0.48 % (3404349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.19/0.48 % (3404349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.19/0.48 % (3404349)CaDiCaL version: 2.1.3 % 2.19/0.48 % (3404349)Termination reason: Instruction limit % 3.53/0.71 % (3404349)Termination phase: Saturation % 3.53/0.71 % (3404349)Time elapsed: 0.036 s % 3.53/0.71 % (3404349)Peak memory usage: 12 MB % 3.53/0.71 % (3404349)Instructions burned: 112 (million) % 3.53/0.71 % (3404379)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=2924196585:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.53/0.71 % (3404352)Instruction limit reached! % 3.53/0.71 % (3404352)------------------------------ % 3.53/0.71 % (3404352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.53/0.71 % (3404352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.53/0.71 % (3404352)CaDiCaL version: 2.1.3 % 3.53/0.71 % (3404352)Termination reason: Instruction limit % 3.53/0.71 % (3404352)Termination phase: Saturation % 3.53/0.71 % (3404352)Time elapsed: 0.040 s % 3.53/0.71 % (3404352)Peak memory usage: 13 MB % 3.53/0.71 % (3404352)Instructions burned: 160 (million) % 3.53/0.71 % (3404381)ott-21_1_sil=16000:fs=off:random_seed=2701203973:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.53/0.71 % (3404383)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2882485412:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 3.53/0.71 % (3404387)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2767773036:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 3.53/0.71 % (3404387)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.53/0.71 % (3404387)Terminated due to inappropriate strategy. % 3.53/0.71 % (3404387)------------------------------ % 3.53/0.71 % (3404387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.53/0.71 % (3404387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.53/0.71 % (3404387)CaDiCaL version: 2.1.3 % 3.53/0.71 % (3404387)Termination reason: Inappropriate % 3.53/0.71 % (3404387)Time elapsed: 0.004 s % 3.53/0.71 % (3404387)Peak memory usage: 10 MB % 3.53/0.71 % (3404387)Instructions burned: 15 (million) % 3.53/0.71 % (3404387)------------------------------ % 3.53/0.71 % (3404387)------------------------------ % 3.53/0.71 % (3404376)Instruction limit reached! % 3.53/0.71 % (3404376)------------------------------ % 3.53/0.71 % (3404376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.53/0.71 % (3404397)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=228908456:i=1179_2999 on theBenchmark for (2999ds/1179Mi) % 3.53/0.71 % (3404376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.53/0.71 % (3404376)CaDiCaL version: 2.1.3 % 3.53/0.71 % (3404376)Termination reason: Instruction limit % 3.53/0.71 % (3404376)Termination phase: Saturation % 3.53/0.71 % (3404376)Time elapsed: 0.037 s % 3.53/0.71 % (3404376)Peak memory usage: 13 MB % 3.53/0.71 % (3404376)Instructions burned: 134 (million) % 3.53/0.71 % (3404399)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1961650477:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi) % 3.53/0.71 % (3404399)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.53/0.71 % (3404399)Terminated due to inappropriate strategy. % 3.53/0.71 % (3404399)------------------------------ % 3.53/0.71 % (3404399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.53/0.71 % (3404399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.53/0.71 % (3404399)CaDiCaL version: 2.1.3 % 3.53/0.71 % (3404399)Termination reason: Inappropriate % 3.53/0.71 % (3404399)Time elapsed: 0.003 s % 3.53/0.71 % (3404399)Peak memory usage: 10 MB % 3.53/0.71 % (3404399)Instructions burned: 12 (million) % 3.53/0.71 % (3404399)------------------------------ % 3.53/0.71 % (3404399)------------------------------ % 3.53/0.71 % (3404381)Instruction limit reached! % 3.53/0.71 % (3404381)------------------------------ % 3.53/0.71 % (3404381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.53/0.71 % (3404381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.53/0.71 % (3404381)CaDiCaL version: 2.1.3 % 3.53/0.71 % (3404381)Termination reason: Instruction limit % 3.53/0.71 % (3404381)Termination phase: Saturation % 3.53/0.71 % (3404381)Time elapsed: 0.050 s % 3.53/0.71 % (3404381)Peak memory usage: 13 MB % 3.53/0.71 % (3404381)Instructions burned: 182 (million) % 3.53/0.71 % (3404401)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=543709437: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) % 14.27/2.25 % (3404402)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2760038335:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 14.27/2.25 % (3404383)Instruction limit reached! % 14.27/2.25 % (3404383)------------------------------ % 14.27/2.25 % (3404383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.27/2.25 % (3404383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.27/2.25 % (3404383)CaDiCaL version: 2.1.3 % 14.27/2.25 % (3404383)Termination reason: Instruction limit % 14.27/2.25 % (3404383)Termination phase: Saturation % 14.27/2.25 % (3404383)Time elapsed: 0.104 s % 14.27/2.25 % (3404383)Peak memory usage: 13 MB % 14.27/2.25 % (3404383)Instructions burned: 478 (million) % 14.27/2.25 % (3404405)fmb+10_1_sil=64000:random_seed=1285416602:i=22061:nm=2:gsp=on_2998 on theBenchmark for (2998ds/22061Mi) % 14.27/2.25 % (3404405)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.27/2.25 % (3404405)Terminated due to inappropriate strategy. % 14.27/2.25 % (3404405)------------------------------ % 14.27/2.25 % (3404405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.27/2.25 % (3404405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.27/2.25 % (3404405)CaDiCaL version: 2.1.3 % 14.27/2.25 % (3404405)Termination reason: Inappropriate % 14.27/2.25 % (3404405)Time elapsed: 0.003 s % 14.27/2.25 % (3404405)Peak memory usage: 10 MB % 14.27/2.25 % (3404405)Instructions burned: 13 (million) % 14.27/2.25 % (3404405)------------------------------ % 14.27/2.25 % (3404405)------------------------------ % 14.27/2.25 % (3404407)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1531988426:i=9515:nm=5_2998 on theBenchmark for (2998ds/9515Mi) % 14.27/2.25 % (3404407)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.27/2.25 % (3404407)Terminated due to inappropriate strategy. % 14.27/2.25 % (3404407)------------------------------ % 14.27/2.25 % (3404407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.27/2.25 % (3404407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.27/2.25 % (3404407)CaDiCaL version: 2.1.3 % 14.27/2.25 % (3404407)Termination reason: Inappropriate % 14.27/2.25 % (3404407)Time elapsed: 0.003 s % 14.27/2.25 % (3404407)Peak memory usage: 10 MB % 14.27/2.25 % (3404407)Instructions burned: 12 (million) % 14.27/2.25 % (3404407)------------------------------ % 14.27/2.25 % (3404407)------------------------------ % 14.27/2.25 % (3404409)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1237494263:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 14.27/2.25 % (3404409)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.27/2.25 % (3404409)Terminated due to inappropriate strategy. % 14.27/2.25 % (3404409)------------------------------ % 14.27/2.25 % (3404409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.27/2.25 % (3404409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.27/2.25 % (3404409)CaDiCaL version: 2.1.3 % 14.27/2.25 % (3404409)Termination reason: Inappropriate % 14.27/2.25 % (3404409)Time elapsed: 0.003 s % 14.27/2.25 % (3404409)Peak memory usage: 10 MB % 14.27/2.25 % (3404409)Instructions burned: 12 (million) % 14.27/2.25 % (3404409)------------------------------ % 14.27/2.25 % (3404409)------------------------------ % 14.27/2.25 % (3404411)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3947892646:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 14.27/2.25 % (3404379)Instruction limit reached! % 14.27/2.25 % (3404379)------------------------------ % 14.27/2.25 % (3404379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.27/2.25 % (3404379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.27/2.25 % (3404379)CaDiCaL version: 2.1.3 % 14.27/2.25 % (3404379)Termination reason: Instruction limit % 14.27/2.25 % (3404379)Termination phase: Saturation % 14.27/2.25 % (3404379)Time elapsed: 0.190 s % 14.27/2.25 % (3404379)Peak memory usage: 16 MB % 14.27/2.25 % (3404379)Instructions burned: 684 (million) % 14.27/2.25 % (3404413)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3881218207:i=1472:ins=7:fdi=8:gsp=on_2997 on theBenchmark for (2997ds/1472Mi) % 14.27/2.25 % (3404401)Instruction limit reached! % 14.27/2.25 % (3404401)------------------------------ % 15.75/2.55 % (3404401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.75/2.55 % (3404401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.75/2.55 % (3404401)CaDiCaL version: 2.1.3 % 15.75/2.55 % (3404401)Termination reason: Instruction limit % 15.75/2.55 % (3404401)Termination phase: Saturation % 15.75/2.55 % (3404401)Time elapsed: 0.220 s % 15.75/2.55 % (3404401)Peak memory usage: 18 MB % 15.75/2.55 % (3404401)Instructions burned: 692 (million) % 15.75/2.55 % (3404420)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3175344981:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 15.75/2.55 % (3404420)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.75/2.55 % (3404420)Terminated due to inappropriate strategy. % 15.75/2.55 % (3404420)------------------------------ % 15.75/2.55 % (3404420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.75/2.55 % (3404420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.75/2.55 % (3404420)CaDiCaL version: 2.1.3 % 15.75/2.55 % (3404420)Termination reason: Inappropriate % 15.75/2.55 % (3404420)Time elapsed: 0.007 s % 15.75/2.55 % (3404420)Peak memory usage: 11 MB % 15.75/2.55 % (3404420)Instructions burned: 15 (million) % 15.75/2.55 % (3404420)------------------------------ % 15.75/2.55 % (3404420)------------------------------ % 15.75/2.55 % (3404425)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3438667773:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi) % 15.75/2.55 % (3404402)Instruction limit reached! % 15.75/2.55 % (3404402)------------------------------ % 15.75/2.55 % (3404402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.75/2.55 % (3404402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.75/2.55 % (3404402)CaDiCaL version: 2.1.3 % 15.75/2.55 % (3404402)Termination reason: Instruction limit % 15.75/2.55 % (3404402)Termination phase: Saturation % 15.75/2.55 % (3404402)Time elapsed: 0.294 s % 15.75/2.55 % (3404402)Peak memory usage: 18 MB % 15.75/2.55 % (3404402)Instructions burned: 880 (million) % 15.75/2.55 % (3404425)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.75/2.55 % (3404425)Terminated due to inappropriate strategy. % 15.75/2.55 % (3404425)------------------------------ % 15.75/2.55 % (3404425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.75/2.55 % (3404425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.75/2.55 % (3404425)CaDiCaL version: 2.1.3 % 15.75/2.55 % (3404425)Termination reason: Inappropriate % 15.75/2.55 % (3404425)Time elapsed: 0.005 s % 15.75/2.55 % (3404425)Peak memory usage: 10 MB % 15.75/2.55 % (3404425)Instructions burned: 12 (million) % 15.75/2.55 % (3404425)------------------------------ % 15.75/2.55 % (3404425)------------------------------ % 15.75/2.55 % (3404427)ott-2_1_sil=16000:newcnf=on:random_seed=2257778811:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi) % 15.75/2.55 % (3404428)ott+10_1_sil=32000:tgt=ground:random_seed=3109791373:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi) % 15.75/2.55 % (3404397)Instruction limit reached! % 15.75/2.55 % (3404397)------------------------------ % 15.75/2.55 % (3404397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.75/2.55 % (3404397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.75/2.55 % (3404397)CaDiCaL version: 2.1.3 % 15.75/2.55 % (3404397)Termination reason: Instruction limit % 15.75/2.55 % (3404397)Termination phase: Saturation % 15.75/2.55 % (3404397)Time elapsed: 0.436 s % 15.75/2.55 % (3404397)Peak memory usage: 21 MB % 15.75/2.55 % (3404397)Instructions burned: 1180 (million) % 15.75/2.55 % (3404442)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2825912925:i=54282_2994 on theBenchmark for (2994ds/54282Mi) % 15.75/2.55 % (3404442)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.75/2.55 % (3404442)Terminated due to inappropriate strategy. % 15.75/2.55 % (3404442)------------------------------ % 15.75/2.55 % (3404442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.75/2.55 % (3404442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.75/2.55 % (3404442)CaDiCaL version: 2.1.3 % 15.75/2.55 % (3404442)Termination reason: Inappropriate % 15.75/2.55 % (3404442)Time elapsed: 0.007 s % 15.75/2.55 % (3404442)Peak memory usage: 11 MB % 15.75/2.55 % (3404442)Instructions burned: 15 (million) % 48.31/7.09 % (3404442)------------------------------ % 48.31/7.09 % (3404442)------------------------------ % 48.31/7.09 % (3404447)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3889319801:i=3512:aac=none_2994 on theBenchmark for (2994ds/3512Mi) % 48.31/7.09 % (3404427)Instruction limit reached! % 48.31/7.09 % (3404427)------------------------------ % 48.31/7.09 % (3404427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.31/7.09 % (3404427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.31/7.09 % (3404427)CaDiCaL version: 2.1.3 % 48.31/7.09 % (3404427)Termination reason: Instruction limit % 48.31/7.09 % (3404427)Termination phase: Saturation % 48.31/7.09 % (3404427)Time elapsed: 0.247 s % 48.31/7.09 % (3404427)Peak memory usage: 13 MB % 48.31/7.09 % (3404427)Instructions burned: 870 (million) % 48.31/7.09 % (3404461)dis+21_1_sil=32000:sas=cadical:random_seed=1036489475:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 48.31/7.09 % (3404413)Instruction limit reached! % 48.31/7.09 % (3404413)------------------------------ % 48.31/7.09 % (3404413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.31/7.09 % (3404413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.31/7.09 % (3404413)CaDiCaL version: 2.1.3 % 48.31/7.09 % (3404413)Termination reason: Instruction limit % 48.31/7.09 % (3404413)Termination phase: Saturation % 48.31/7.09 % (3404413)Time elapsed: 0.754 s % 48.31/7.09 % (3404413)Peak memory usage: 27 MB % 48.31/7.09 % (3404413)Instructions burned: 1473 (million) % 48.31/7.09 % (3404490)ott+11_1_sil=16000:gs=on:random_seed=2484262850:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi) % 48.31/7.09 % (3404490)Instruction limit reached! % 48.31/7.09 % (3404490)------------------------------ % 48.31/7.09 % (3404490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.31/7.09 % (3404490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.31/7.09 % (3404490)CaDiCaL version: 2.1.3 % 48.31/7.09 % (3404490)Termination reason: Instruction limit % 48.31/7.09 % (3404490)Termination phase: Saturation % 48.31/7.09 % (3404490)Time elapsed: 0.675 s % 48.31/7.09 % (3404490)Peak memory usage: 14 MB % 48.31/7.09 % (3404490)Instructions burned: 2254 (million) % 48.31/7.09 % (3404521)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1999912926:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 48.31/7.09 % (3404521)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 48.31/7.09 % (3404521)Terminated due to inappropriate strategy. % 48.31/7.09 % (3404521)------------------------------ % 48.31/7.09 % (3404521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.31/7.09 % (3404521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.31/7.09 % (3404521)CaDiCaL version: 2.1.3 % 48.31/7.09 % (3404521)Termination reason: Inappropriate % 48.31/7.09 % (3404521)Time elapsed: 0.003 s % 48.31/7.09 % (3404521)Peak memory usage: 10 MB % 48.31/7.09 % (3404521)Instructions burned: 13 (million) % 48.31/7.09 % (3404521)------------------------------ % 48.31/7.09 % (3404521)------------------------------ % 48.31/7.09 % (3404523)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2782757715:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 48.31/7.09 % (3404447)Instruction limit reached! % 48.31/7.09 % (3404447)------------------------------ % 48.31/7.09 % (3404447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.31/7.09 % (3404447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.31/7.09 % (3404447)CaDiCaL version: 2.1.3 % 48.31/7.09 % (3404447)Termination reason: Instruction limit % 48.31/7.09 % (3404447)Termination phase: Saturation % 48.31/7.09 % (3404447)Time elapsed: 1.340 s % 48.31/7.09 % (3404447)Peak memory usage: 30 MB % 48.31/7.09 % (3404447)Instructions burned: 3512 (million) % 48.31/7.09 % (3404564)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3271794588:i=29340_2980 on theBenchmark for (2980ds/29340Mi) % 48.31/7.09 % (3404411)Instruction limit reached! % 48.31/7.09 % (3404411)------------------------------ % 48.31/7.09 % (3404411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.31/7.09 % (3404411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.31/7.09 % (3404411)CaDiCaL version: 2.1.3 % 48.31/7.09 % (3404411)Termination reason: Instruction limit % 63.59/9.24 % (3404411)Termination phase: Saturation % 63.59/9.24 % (3404411)Time elapsed: 1.880 s % 63.59/9.24 % (3404411)Peak memory usage: 33 MB % 63.59/9.24 % (3404411)Instructions burned: 5131 (million) % 63.59/9.24 % (3404566)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3409444635:i=5211_2978 on theBenchmark for (2978ds/5211Mi) % 63.59/9.24 % (3404461)Instruction limit reached! % 63.59/9.24 % (3404461)------------------------------ % 63.59/9.24 % (3404461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.59/9.24 % (3404461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.59/9.24 % (3404461)CaDiCaL version: 2.1.3 % 63.59/9.24 % (3404461)Termination reason: Instruction limit % 63.59/9.24 % (3404461)Termination phase: Saturation % 63.59/9.24 % (3404461)Time elapsed: 1.473 s % 63.59/9.24 % (3404461)Peak memory usage: 36 MB % 63.59/9.24 % (3404461)Instructions burned: 3774 (million) % 63.59/9.24 % (3404568)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1004986111:i=5497:nm=2_2977 on theBenchmark for (2977ds/5497Mi) % 63.59/9.24 % (3404568)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 63.59/9.24 % (3404568)Terminated due to inappropriate strategy. % 63.59/9.24 % (3404568)------------------------------ % 63.59/9.24 % (3404568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.59/9.24 % (3404568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.59/9.24 % (3404568)CaDiCaL version: 2.1.3 % 63.59/9.24 % (3404568)Termination reason: Inappropriate % 63.59/9.24 % (3404568)Time elapsed: 0.004 s % 63.59/9.24 % (3404568)Peak memory usage: 11 MB % 63.59/9.24 % (3404568)Instructions burned: 14 (million) % 63.59/9.24 % (3404568)------------------------------ % 63.59/9.24 % (3404568)------------------------------ % 63.59/9.24 % (3404570)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1435033717:fmbsr=2:i=46332_2977 on theBenchmark for (2977ds/46332Mi) % 63.59/9.24 % (3404570)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 63.59/9.24 % (3404570)Terminated due to inappropriate strategy. % 63.59/9.24 % (3404570)------------------------------ % 63.59/9.24 % (3404570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.59/9.24 % (3404570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.59/9.24 % (3404570)CaDiCaL version: 2.1.3 % 63.59/9.24 % (3404570)Termination reason: Inappropriate % 63.59/9.24 % (3404570)Time elapsed: 0.004 s % 63.59/9.24 % (3404570)Peak memory usage: 11 MB % 63.59/9.24 % (3404570)Instructions burned: 13 (million) % 63.59/9.24 % (3404570)------------------------------ % 63.59/9.24 % (3404570)------------------------------ % 63.59/9.24 % (3404572)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3670526071:i=14071_2977 on theBenchmark for (2977ds/14071Mi) % 63.59/9.24 % (3404572)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 63.59/9.24 % (3404572)Terminated due to inappropriate strategy. % 63.59/9.24 % (3404572)------------------------------ % 63.59/9.24 % (3404572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.59/9.24 % (3404572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.59/9.24 % (3404572)CaDiCaL version: 2.1.3 % 63.59/9.24 % (3404572)Termination reason: Inappropriate % 63.59/9.24 % (3404572)Time elapsed: 0.004 s % 63.59/9.24 % (3404572)Peak memory usage: 11 MB % 63.59/9.24 % (3404572)Instructions burned: 13 (million) % 63.59/9.24 % (3404572)------------------------------ % 63.59/9.24 % (3404572)------------------------------ % 63.59/9.24 % (3404574)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3646605272:i=22565:add=on:rawr=on_2977 on theBenchmark for (2977ds/22565Mi) % 63.59/9.24 % (3404428)Instruction limit reached! % 63.59/9.24 % (3404428)------------------------------ % 63.59/9.24 % (3404428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 63.59/9.24 % (3404428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.59/9.24 % (3404428)CaDiCaL version: 2.1.3 % 63.59/9.24 % (3404428)Termination reason: Instruction limit % 63.59/9.24 % (3404428)Termination phase: Saturation % 63.59/9.24 % (3404428)Time elapsed: 1.941 s % 63.59/9.24 % (3404428)Peak memory usage: 54 MB % 63.59/9.24 % (3404428)Instructions burned: 5115 (million) % 63.59/9.24 % (3404576)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=319708322:i=8173:av=off_2975 on theBenchmark for (2975ds/8173Mi) % 64.19/9.31 % (3404523)Instruction limit reached! % 64.19/9.31 % (3404523)------------------------------ % 64.19/9.31 % (3404523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.19/9.31 % (3404523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.19/9.31 % (3404523)CaDiCaL version: 2.1.3 % 64.19/9.31 % (3404523)Termination reason: Instruction limit % 64.19/9.31 % (3404523)Termination phase: Saturation % 64.19/9.31 % (3404523)Time elapsed: 0.818 s % 64.19/9.31 % (3404523)Peak memory usage: 14 MB % 64.19/9.31 % (3404523)Instructions burned: 4591 (million) % 64.19/9.31 % (3404578)dis+10_16:1_sil=16000:random_seed=2321361987:i=9155:fsr=off_2974 on theBenchmark for (2974ds/9155Mi) % 64.19/9.31 % (3404566)Instruction limit reached! % 64.19/9.31 % (3404566)------------------------------ % 64.19/9.31 % (3404566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.19/9.31 % (3404566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.19/9.31 % (3404566)CaDiCaL version: 2.1.3 % 64.19/9.31 % (3404566)Termination reason: Instruction limit % 64.19/9.31 % (3404566)Termination phase: Saturation % 64.19/9.31 % (3404566)Time elapsed: 1.364 s % 64.19/9.31 % (3404566)Peak memory usage: 40 MB % 64.19/9.31 % (3404566)Instructions burned: 5215 (million) % 64.19/9.31 % (3404580)ott-3_8_sil=64000:random_seed=3027136692:i=20139:bs=on_2965 on theBenchmark for (2965ds/20139Mi) % 64.19/9.31 % (3404576)Instruction limit reached! % 64.19/9.31 % (3404576)------------------------------ % 64.19/9.31 % (3404576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.19/9.31 % (3404576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.19/9.31 % (3404576)CaDiCaL version: 2.1.3 % 64.19/9.31 % (3404576)Termination reason: Instruction limit % 64.19/9.31 % (3404576)Termination phase: Saturation % 64.19/9.31 % (3404576)Time elapsed: 2.582 s % 64.19/9.31 % (3404576)Peak memory usage: 79 MB % 64.19/9.31 % (3404576)Instructions burned: 8173 (million) % 64.19/9.31 % (3404582)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3625160394:fmbsr=2:i=32576_2949 on theBenchmark for (2949ds/32576Mi) % 64.19/9.31 % (3404582)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 64.19/9.31 % (3404582)Terminated due to inappropriate strategy. % 64.19/9.31 % (3404582)------------------------------ % 64.19/9.31 % (3404582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.19/9.31 % (3404582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.19/9.31 % (3404582)CaDiCaL version: 2.1.3 % 64.19/9.31 % (3404582)Termination reason: Inappropriate % 64.19/9.31 % (3404582)Time elapsed: 0.004 s % 64.19/9.31 % (3404582)Peak memory usage: 11 MB % 64.19/9.31 % (3404582)Instructions burned: 16 (million) % 64.19/9.31 % (3404582)------------------------------ % 64.19/9.31 % (3404582)------------------------------ % 64.19/9.31 % (3404584)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3737398102:i=11404_2949 on theBenchmark for (2949ds/11404Mi) % 64.19/9.31 % (3404578)Instruction limit reached! % 64.19/9.31 % (3404578)------------------------------ % 64.19/9.31 % (3404578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.19/9.31 % (3404578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.19/9.31 % (3404578)CaDiCaL version: 2.1.3 % 64.19/9.31 % (3404578)Termination reason: Instruction limit % 64.19/9.31 % (3404578)Termination phase: Saturation % 64.19/9.31 % (3404578)Time elapsed: 2.530 s % 64.19/9.31 % (3404578)Peak memory usage: 64 MB % 64.19/9.31 % (3404578)Instructions burned: 9158 (million) % 64.19/9.31 % (3404586)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2697235882:i=14134_2948 on theBenchmark for (2948ds/14134Mi) % 64.19/9.31 % (3404574)Instruction limit reached! % 64.19/9.31 % (3404574)------------------------------ % 64.19/9.31 % (3404574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.19/9.31 % (3404574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.19/9.31 % (3404574)CaDiCaL version: 2.1.3 % 64.19/9.31 % (3404574)Termination reason: Instruction limit % 64.19/9.31 % (3404574)Termination phase: Saturation % 64.19/9.31 % (3404574)Time elapsed: 4.004 s % 64.19/9.31 % (3404574)Peak memory usage: 18 MB % 64.19/9.31 % (3404574)Instructions burned: 22566 (million) % 64.19/9.31 % (3404588)dis+33_16_sil=32000:sac=on:random_seed=3687793212:i=15851:nm=0_2937 on theBenchmark for (2937ds/15851Mi) % 64.19/9.31 % (3404564)Instruction limit reached! % 64.19/9.31 % (3404564)------------------------------ % 64.19/9.31 % (3404564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.56/10.64 % (3404564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.56/10.64 % (3404564)CaDiCaL version: 2.1.3 % 73.56/10.64 % (3404564)Termination reason: Instruction limit % 73.56/10.64 % (3404564)Termination phase: Saturation % 73.56/10.64 % (3404564)Time elapsed: 4.986 s % 73.56/10.64 % (3404564)Peak memory usage: 13 MB % 73.56/10.64 % (3404564)Instructions burned: 29345 (million) % 73.56/10.64 % (3404590)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1462246986:avsq=on:i=17627:add=on:amm=off_2930 on theBenchmark for (2930ds/17627Mi) % 73.56/10.64 % (3404580)Instruction limit reached! % 73.56/10.64 % (3404580)------------------------------ % 73.56/10.64 % (3404580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.56/10.64 % (3404580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.56/10.64 % (3404580)CaDiCaL version: 2.1.3 % 73.56/10.64 % (3404580)Termination reason: Instruction limit % 73.56/10.64 % (3404580)Termination phase: Saturation % 73.56/10.64 % (3404580)Time elapsed: 3.542 s % 73.56/10.64 % (3404580)Peak memory usage: 15 MB % 73.56/10.64 % (3404580)Instructions burned: 20140 (million) % 73.56/10.64 % (3404592)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=67948546:s2a=on:i=53295_2929 on theBenchmark for (2929ds/53295Mi) % 73.56/10.64 % (3404584)Instruction limit reached! % 73.56/10.64 % (3404584)------------------------------ % 73.56/10.64 % (3404584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.56/10.64 % (3404584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.56/10.64 % (3404584)CaDiCaL version: 2.1.3 % 73.56/10.64 % (3404584)Termination reason: Instruction limit % 73.56/10.64 % (3404584)Termination phase: Saturation % 73.56/10.64 % (3404584)Time elapsed: 3.873 s % 73.56/10.64 % (3404584)Peak memory usage: 105 MB % 73.56/10.64 % (3404584)Instructions burned: 11404 (million) % 73.56/10.64 % (3404594)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3050059562:i=26857:ins=20_2910 on theBenchmark for (2910ds/26857Mi) % 73.56/10.64 % (3404594)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 73.56/10.64 % (3404594)Terminated due to inappropriate strategy. % 73.56/10.64 % (3404594)------------------------------ % 73.56/10.64 % (3404594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.56/10.64 % (3404594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.56/10.64 % (3404594)CaDiCaL version: 2.1.3 % 73.56/10.64 % (3404594)Termination reason: Inappropriate % 73.56/10.64 % (3404594)Time elapsed: 0.003 s % 73.56/10.64 % (3404594)Peak memory usage: 10 MB % 73.56/10.64 % (3404594)Instructions burned: 12 (million) % 73.56/10.64 % (3404594)------------------------------ % 73.56/10.64 % (3404594)------------------------------ % 73.56/10.64 % (3404596)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2639556458:i=28120:bs=on:fsr=off_2910 on theBenchmark for (2910ds/28120Mi) % 73.56/10.64 % (3404588)Instruction limit reached! % 73.56/10.64 % (3404588)------------------------------ % 73.56/10.64 % (3404588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.56/10.64 % (3404588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.56/10.64 % (3404588)CaDiCaL version: 2.1.3 % 73.56/10.64 % (3404588)Termination reason: Instruction limit % 73.56/10.64 % (3404588)Termination phase: Saturation % 73.56/10.64 % (3404588)Time elapsed: 2.792 s % 73.56/10.64 % (3404588)Peak memory usage: 13 MB % 73.56/10.64 % (3404588)Instructions burned: 15855 (million) % 73.56/10.64 % (3404598)fmb+10_1_sil=256000:fmbss=7:random_seed=2183561259:fmbsr=1.6:i=182295_2909 on theBenchmark for (2909ds/182295Mi) % 73.56/10.64 % (3404598)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 73.56/10.64 % (3404598)Terminated due to inappropriate strategy. % 73.56/10.64 % (3404598)------------------------------ % 73.56/10.64 % (3404598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.56/10.64 % (3404598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.56/10.64 % (3404598)CaDiCaL version: 2.1.3 % 73.56/10.64 % (3404598)Termination reason: Inappropriate % 73.56/10.64 % (3404598)Time elapsed: 0.003 s % 73.56/10.64 % (3404598)Peak memory usage: 10 MB % 73.56/10.64 % (3404598)Instructions burned: 12 (million) % 73.56/10.64 % (3404598)------------------------------ % 73.56/10.64 % (3404598)------------------------------ % 73.56/10.64 % (3404600)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=430114600:i=44625:gsp=on_2909 on theBenchmark for (2909ds/44625Mi) % 79.08/11.47 % (3404600)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 79.08/11.47 % (3404600)Terminated due to inappropriate strategy. % 79.08/11.47 % (3404600)------------------------------ % 79.08/11.47 % (3404600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.08/11.47 % (3404600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.08/11.47 % (3404600)CaDiCaL version: 2.1.3 % 79.08/11.47 % (3404600)Termination reason: Inappropriate % 79.08/11.47 % (3404600)Time elapsed: 0.004 s % 79.08/11.47 % (3404600)Peak memory usage: 11 MB % 79.08/11.47 % (3404600)Instructions burned: 14 (million) % 79.08/11.47 % (3404600)------------------------------ % 79.08/11.47 % (3404600)------------------------------ % 79.08/11.47 % (3404602)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3314682521:i=160505_2908 on theBenchmark for (2908ds/160505Mi) % 79.08/11.47 % (3404602)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 79.08/11.47 % (3404602)Terminated due to inappropriate strategy. % 79.08/11.47 % (3404602)------------------------------ % 79.08/11.47 % (3404602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.08/11.47 % (3404602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.08/11.47 % (3404602)CaDiCaL version: 2.1.3 % 79.08/11.47 % (3404602)Termination reason: Inappropriate % 79.08/11.47 % (3404602)Time elapsed: 0.003 s % 79.08/11.47 % (3404602)Peak memory usage: 10 MB % 79.08/11.47 % (3404602)Instructions burned: 12 (million) % 79.08/11.47 % (3404602)------------------------------ % 79.08/11.47 % (3404602)------------------------------ % 79.08/11.47 % (3404604)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=435526833:fmbsr=1.3:i=225729_2908 on theBenchmark for (2908ds/225729Mi) % 79.08/11.47 % (3404604)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 79.08/11.47 % (3404604)Terminated due to inappropriate strategy. % 79.08/11.47 % (3404604)------------------------------ % 79.08/11.47 % (3404604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.08/11.47 % (3404604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.08/11.47 % (3404604)CaDiCaL version: 2.1.3 % 79.08/11.47 % (3404604)Termination reason: Inappropriate % 79.08/11.47 % (3404604)Time elapsed: 0.004 s % 79.08/11.47 % (3404604)Peak memory usage: 11 MB % 79.08/11.47 % (3404604)Instructions burned: 13 (million) % 79.08/11.47 % (3404604)------------------------------ % 79.08/11.47 % (3404604)------------------------------ % 79.08/11.47 % (3404606)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1859589660:fmbsr=2:i=185024:ins=7_2908 on theBenchmark for (2908ds/185024Mi) % 79.08/11.47 % (3404606)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 79.08/11.47 % (3404606)Terminated due to inappropriate strategy. % 79.08/11.47 % (3404606)------------------------------ % 79.08/11.47 % (3404606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.08/11.47 % (3404606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.08/11.47 % (3404606)CaDiCaL version: 2.1.3 % 79.08/11.47 % (3404606)Termination reason: Inappropriate % 79.08/11.47 % (3404606)Time elapsed: 0.004 s % 79.08/11.47 % (3404606)Peak memory usage: 11 MB % 79.08/11.47 % (3404606)Instructions burned: 13 (million) % 79.08/11.47 % (3404606)------------------------------ % 79.08/11.47 % (3404606)------------------------------ % 79.08/11.47 % (3404608)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3988788575:rtra=on_2908 on theBenchmark for (2908ds/0Mi) % 79.08/11.47 % (3404608)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 79.08/11.47 % (3404608)Terminated due to inappropriate strategy. % 79.08/11.47 % (3404608)------------------------------ % 79.08/11.47 % (3404608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.08/11.47 % (3404608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.08/11.47 % (3404608)CaDiCaL version: 2.1.3 % 79.08/11.47 % (3404608)Termination reason: Inappropriate % 79.08/11.47 % (3404608)Time elapsed: 0.004 s % 79.08/11.47 % (3404608)Peak memory usage: 11 MB % 79.08/11.47 % (3404608)Instructions burned: 15 (million) % 79.08/11.47 % (3404608)------------------------------ % 79.08/11.47 % (3404608)------------------------------ % 79.08/11.47 % (3404610)% WARNING: option uhcvi not known. % 79.08/11.47 % (3404610)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2342436236:i=271062:add=off:rtra=on:rawr=on_2908 on theBenchmark for (2908ds/271062Mi) % 92.66/13.32 % (3404586)Instruction limit reached! % 92.66/13.32 % (3404586)------------------------------ % 92.66/13.32 % (3404586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.66/13.32 % (3404586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.66/13.32 % (3404586)CaDiCaL version: 2.1.3 % 92.66/13.32 % (3404586)Termination reason: Instruction limit % 92.66/13.32 % (3404586)Termination phase: Saturation % 92.66/13.32 % (3404586)Time elapsed: 4.541 s % 92.66/13.32 % (3404586)Peak memory usage: 86 MB % 92.66/13.32 % (3404586)Instructions burned: 14136 (million) % 92.66/13.32 % (3404612)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1645056058:i=176048:add=on:rtra=on:rawr=on_2902 on theBenchmark for (2902ds/176048Mi) % 92.66/13.32 % (3404590)Instruction limit reached! % 92.66/13.32 % (3404590)------------------------------ % 92.66/13.32 % (3404590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.66/13.32 % (3404590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.66/13.32 % (3404590)CaDiCaL version: 2.1.3 % 92.66/13.32 % (3404590)Termination reason: Instruction limit % 92.66/13.32 % (3404590)Termination phase: Saturation % 92.66/13.32 % (3404590)Time elapsed: 3.224 s % 92.66/13.32 % (3404590)Peak memory usage: 17 MB % 92.66/13.32 % (3404590)Instructions burned: 17628 (million) % 92.66/13.32 % (3404614)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2713971282:i=206:fgj=on:rtra=on_2898 on theBenchmark for (2898ds/206Mi) % 92.66/13.32 % (3404614)Instruction limit reached! % 92.66/13.32 % (3404614)------------------------------ % 92.66/13.32 % (3404614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.66/13.32 % (3404614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.66/13.32 % (3404614)CaDiCaL version: 2.1.3 % 92.66/13.32 % (3404614)Termination reason: Instruction limit % 92.66/13.32 % (3404614)Termination phase: Saturation % 92.66/13.32 % (3404614)Time elapsed: 0.066 s % 92.66/13.32 % (3404614)Peak memory usage: 13 MB % 92.66/13.32 % (3404614)Instructions burned: 207 (million) % 92.66/13.32 % (3404616)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1313003895:i=232:rtra=on_2897 on theBenchmark for (2897ds/232Mi) % 92.66/13.32 % (3404616)Instruction limit reached! % 92.66/13.32 % (3404616)------------------------------ % 92.66/13.32 % (3404616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.66/13.32 % (3404616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.66/13.32 % (3404616)CaDiCaL version: 2.1.3 % 92.66/13.32 % (3404616)Termination reason: Instruction limit % 92.66/13.32 % (3404616)Termination phase: Saturation % 92.66/13.32 % (3404616)Time elapsed: 0.056 s % 92.66/13.32 % (3404616)Peak memory usage: 12 MB % 92.66/13.32 % (3404616)Instructions burned: 236 (million) % 92.66/13.32 % (3404618)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4018831471:i=262:rtra=on_2896 on theBenchmark for (2896ds/262Mi) % 92.66/13.32 % (3404618)Instruction limit reached! % 92.66/13.32 % (3404618)------------------------------ % 92.66/13.32 % (3404618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.66/13.32 % (3404618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.66/13.32 % (3404618)CaDiCaL version: 2.1.3 % 92.66/13.32 % (3404618)Termination reason: Instruction limit % 92.66/13.32 % (3404618)Termination phase: Saturation % 92.66/13.32 % (3404618)Time elapsed: 0.062 s % 92.66/13.32 % (3404618)Peak memory usage: 12 MB % 92.66/13.32 % (3404618)Instructions burned: 265 (million) % 92.66/13.32 % (3404620)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3898696284:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2895 on theBenchmark for (2895ds/318Mi) % 92.66/13.32 % (3404620)Instruction limit reached! % 92.66/13.32 % (3404620)------------------------------ % 92.66/13.32 % (3404620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.66/13.32 % (3404620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.66/13.32 % (3404620)CaDiCaL version: 2.1.3 % 92.66/13.32 % (3404620)Termination reason: Instruction limit % 92.66/13.32 % (3404620)Termination phase: Saturation % 92.66/13.32 % (3404620)Time elapsed: 0.070 s % 92.66/13.32 % (3404620)Peak memory usage: 12 MB % 92.66/13.32 % (3404620)Instructions burned: 320 (million) % 92.66/13.32 % (3404622)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1793616088:i=1428:nm=2:rtra=on_2895 on theBenchmark for (2895ds/1428Mi) % 102.52/14.74 % (3404622)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 102.52/14.74 % (3404622)Terminated due to inappropriate strategy. % 102.52/14.74 % (3404622)------------------------------ % 102.52/14.74 % (3404622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.52/14.74 % (3404622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.52/14.74 % (3404622)CaDiCaL version: 2.1.3 % 102.52/14.74 % (3404622)Termination reason: Inappropriate % 102.52/14.74 % (3404622)Time elapsed: 0.004 s % 102.52/14.74 % (3404622)Peak memory usage: 11 MB % 102.52/14.74 % (3404622)Instructions burned: 13 (million) % 102.52/14.74 % (3404622)------------------------------ % 102.52/14.74 % (3404622)------------------------------ % 102.52/14.74 % (3404624)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4228289266:i=262:bd=preordered:rtra=on:fsd=on_2894 on theBenchmark for (2894ds/262Mi) % 102.52/14.74 % (3404624)Instruction limit reached! % 102.52/14.74 % (3404624)------------------------------ % 102.52/14.74 % (3404624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.52/14.74 % (3404624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.52/14.74 % (3404624)CaDiCaL version: 2.1.3 % 102.52/14.74 % (3404624)Termination reason: Instruction limit % 102.52/14.74 % (3404624)Termination phase: Saturation % 102.52/14.74 % (3404624)Time elapsed: 0.069 s % 102.52/14.74 % (3404624)Peak memory usage: 13 MB % 102.52/14.74 % (3404624)Instructions burned: 262 (million) % 102.52/14.74 % (3404626)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=1898472711:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2894 on theBenchmark for (2894ds/1368Mi) % 102.52/14.74 % (3404626)Instruction limit reached! % 102.52/14.74 % (3404626)------------------------------ % 102.52/14.74 % (3404626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.52/14.74 % (3404626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.52/14.74 % (3404626)CaDiCaL version: 2.1.3 % 102.52/14.74 % (3404626)Termination reason: Instruction limit % 102.52/14.74 % (3404626)Termination phase: Saturation % 102.52/14.74 % (3404626)Time elapsed: 0.384 s % 102.52/14.74 % (3404626)Peak memory usage: 19 MB % 102.52/14.74 % (3404626)Instructions burned: 1371 (million) % 102.52/14.74 % (3404628)ott-21_1_sil=16000:si=on:fs=off:random_seed=2580362792:i=360:av=off:fsr=off:rtra=on_2890 on theBenchmark for (2890ds/360Mi) % 102.52/14.74 % (3404628)Instruction limit reached! % 102.52/14.74 % (3404628)------------------------------ % 102.52/14.74 % (3404628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.52/14.74 % (3404628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.52/14.74 % (3404628)CaDiCaL version: 2.1.3 % 102.52/14.74 % (3404628)Termination reason: Instruction limit % 102.52/14.74 % (3404628)Termination phase: Saturation % 102.52/14.74 % (3404628)Time elapsed: 0.097 s % 102.52/14.74 % (3404628)Peak memory usage: 14 MB % 102.52/14.74 % (3404628)Instructions burned: 364 (million) % 102.52/14.74 % (3404630)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3530972838:i=954:bd=all:rtra=on_2889 on theBenchmark for (2889ds/954Mi) % 102.52/14.74 % (3404630)Instruction limit reached! % 102.52/14.74 % (3404630)------------------------------ % 102.52/14.74 % (3404630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.52/14.74 % (3404630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.52/14.74 % (3404630)CaDiCaL version: 2.1.3 % 102.52/14.74 % (3404630)Termination reason: Instruction limit % 102.52/14.74 % (3404630)Termination phase: Saturation % 102.52/14.74 % (3404630)Time elapsed: 0.205 s % 102.52/14.74 % (3404630)Peak memory usage: 13 MB % 102.52/14.74 % (3404630)Instructions burned: 959 (million) % 102.52/14.74 % (3404632)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1577975218:fmbsr=1.3:i=1730:ins=25:rtra=on_2886 on theBenchmark for (2886ds/1730Mi) % 102.52/14.74 % (3404632)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 102.52/14.74 % (3404632)Terminated due to inappropriate strategy. % 102.52/14.74 % (3404632)------------------------------ % 102.52/14.74 % (3404632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.52/14.74 % (3404632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.52/14.74 % (3404632)CaDiCaL version: 2.1.3 % 102.52/14.74 % (3404632)Termination reason: Inappropriate % 123.69/17.78 % (3404632)Time elapsed: 0.005 s % 123.69/17.78 % (3404632)Peak memory usage: 11 MB % 123.69/17.78 % (3404632)Instructions burned: 16 (million) % 123.69/17.78 % (3404632)------------------------------ % 123.69/17.78 % (3404632)------------------------------ % 123.69/17.78 % (3404634)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2120972602:i=2358:rtra=on_2886 on theBenchmark for (2886ds/2358Mi) % 123.69/17.78 % (3404634)Instruction limit reached! % 123.69/17.78 % (3404634)------------------------------ % 123.69/17.78 % (3404634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.69/17.78 % (3404634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.69/17.78 % (3404634)CaDiCaL version: 2.1.3 % 123.69/17.78 % (3404634)Termination reason: Instruction limit % 123.69/17.78 % (3404634)Termination phase: Saturation % 123.69/17.78 % (3404634)Time elapsed: 0.741 s % 123.69/17.78 % (3404634)Peak memory usage: 28 MB % 123.69/17.78 % (3404634)Instructions burned: 2360 (million) % 123.69/17.78 % (3404636)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2121654479:i=1778:ins=1:rtra=on_2879 on theBenchmark for (2879ds/1778Mi) % 123.69/17.78 % (3404636)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.69/17.78 % (3404636)Terminated due to inappropriate strategy. % 123.69/17.78 % (3404636)------------------------------ % 123.69/17.78 % (3404636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.69/17.78 % (3404636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.69/17.78 % (3404636)CaDiCaL version: 2.1.3 % 123.69/17.78 % (3404636)Termination reason: Inappropriate % 123.69/17.78 % (3404636)Time elapsed: 0.004 s % 123.69/17.78 % (3404636)Peak memory usage: 11 MB % 123.69/17.78 % (3404636)Instructions burned: 13 (million) % 123.69/17.78 % (3404636)------------------------------ % 123.69/17.78 % (3404636)------------------------------ % 123.69/17.78 % (3404638)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=754619670:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2878 on theBenchmark for (2878ds/1384Mi) % 123.69/17.78 % (3404638)Instruction limit reached! % 123.69/17.78 % (3404638)------------------------------ % 123.69/17.78 % (3404638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.69/17.78 % (3404638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.69/17.78 % (3404638)CaDiCaL version: 2.1.3 % 123.69/17.78 % (3404638)Termination reason: Instruction limit % 123.69/17.78 % (3404638)Termination phase: Saturation % 123.69/17.78 % (3404638)Time elapsed: 0.482 s % 123.69/17.78 % (3404638)Peak memory usage: 28 MB % 123.69/17.78 % (3404638)Instructions burned: 1385 (million) % 123.69/17.78 % (3404640)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3448841274:i=1758:kws=inv_precedence:fsr=off:rtra=on_2873 on theBenchmark for (2873ds/1758Mi) % 123.69/17.78 % (3404640)Instruction limit reached! % 123.69/17.78 % (3404640)------------------------------ % 123.69/17.78 % (3404640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.69/17.78 % (3404640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.69/17.78 % (3404640)CaDiCaL version: 2.1.3 % 123.69/17.78 % (3404640)Termination reason: Instruction limit % 123.69/17.78 % (3404640)Termination phase: Saturation % 123.69/17.78 % (3404640)Time elapsed: 0.540 s % 123.69/17.78 % (3404640)Peak memory usage: 23 MB % 123.69/17.78 % (3404640)Instructions burned: 1761 (million) % 123.69/17.78 % (3404642)fmb+10_1_sil=64000:si=on:random_seed=362764498:i=44122:nm=2:rtra=on:gsp=on_2868 on theBenchmark for (2868ds/44122Mi) % 123.69/17.78 % (3404642)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.69/17.78 % (3404642)Terminated due to inappropriate strategy. % 123.69/17.78 % (3404642)------------------------------ % 123.69/17.78 % (3404642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.69/17.78 % (3404642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.69/17.78 % (3404642)CaDiCaL version: 2.1.3 % 123.69/17.78 % (3404642)Termination reason: Inappropriate % 123.69/17.78 % (3404642)Time elapsed: 0.004 s % 123.69/17.78 % (3404642)Peak memory usage: 11 MB % 123.69/17.78 % (3404642)Instructions burned: 14 (million) % 123.69/17.78 % (3404642)------------------------------ % 123.69/17.78 % (3404642)------------------------------ % 123.69/17.78 % (3404644)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3422236037:i=19030:nm=5:rtra=on_2868 on theBenchmark for (2868ds/19030Mi) % 137.08/19.60 % (3404644)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.08/19.60 % (3404644)Terminated due to inappropriate strategy. % 137.08/19.60 % (3404644)------------------------------ % 137.08/19.60 % (3404644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.08/19.60 % (3404644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.08/19.60 % (3404644)CaDiCaL version: 2.1.3 % 137.08/19.60 % (3404644)Termination reason: Inappropriate % 137.08/19.60 % (3404644)Time elapsed: 0.004 s % 137.08/19.60 % (3404644)Peak memory usage: 11 MB % 137.08/19.60 % (3404644)Instructions burned: 13 (million) % 137.08/19.60 % (3404644)------------------------------ % 137.08/19.60 % (3404644)------------------------------ % 137.08/19.60 % (3404646)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1852316457:fmbsr=1.7:i=1840:rtra=on_2868 on theBenchmark for (2868ds/1840Mi) % 137.08/19.60 % (3404646)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.08/19.60 % (3404646)Terminated due to inappropriate strategy. % 137.08/19.60 % (3404646)------------------------------ % 137.08/19.60 % (3404646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.08/19.60 % (3404646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.08/19.60 % (3404646)CaDiCaL version: 2.1.3 % 137.08/19.60 % (3404646)Termination reason: Inappropriate % 137.08/19.60 % (3404646)Time elapsed: 0.004 s % 137.08/19.60 % (3404646)Peak memory usage: 11 MB % 137.08/19.60 % (3404646)Instructions burned: 13 (million) % 137.08/19.60 % (3404646)------------------------------ % 137.08/19.60 % (3404646)------------------------------ % 137.08/19.60 % (3404648)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=946121372:i=10262:rtra=on_2867 on theBenchmark for (2867ds/10262Mi) % 137.08/19.60 % (3404596)Instruction limit reached! % 137.08/19.60 % (3404596)------------------------------ % 137.08/19.60 % (3404596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.08/19.60 % (3404596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.08/19.60 % (3404596)CaDiCaL version: 2.1.3 % 137.08/19.60 % (3404596)Termination reason: Instruction limit % 137.08/19.60 % (3404596)Termination phase: Saturation % 137.08/19.60 % (3404596)Time elapsed: 4.633 s % 137.08/19.60 % (3404596)Peak memory usage: 15 MB % 137.08/19.60 % (3404596)Instructions burned: 28123 (million) % 137.08/19.60 % (3404650)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2234890830:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2864 on theBenchmark for (2864ds/2944Mi) % 137.08/19.60 % (3404650)Instruction limit reached! % 137.08/19.60 % (3404650)------------------------------ % 137.08/19.60 % (3404650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.08/19.60 % (3404650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.08/19.60 % (3404650)CaDiCaL version: 2.1.3 % 137.08/19.60 % (3404650)Termination reason: Instruction limit % 137.08/19.60 % (3404650)Termination phase: Saturation % 137.08/19.60 % (3404650)Time elapsed: 0.983 s % 137.08/19.60 % (3404650)Peak memory usage: 41 MB % 137.08/19.60 % (3404650)Instructions burned: 2945 (million) % 137.08/19.60 % (3404652)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1337630999:i=12648:rtra=on_2854 on theBenchmark for (2854ds/12648Mi) % 137.08/19.60 % (3404652)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.08/19.60 % (3404652)Terminated due to inappropriate strategy. % 137.08/19.60 % (3404652)------------------------------ % 137.08/19.60 % (3404652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.08/19.60 % (3404652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.08/19.60 % (3404652)CaDiCaL version: 2.1.3 % 137.08/19.60 % (3404652)Termination reason: Inappropriate % 137.08/19.60 % (3404652)Time elapsed: 0.005 s % 137.08/19.60 % (3404652)Peak memory usage: 11 MB % 137.08/19.60 % (3404652)Instructions burned: 16 (million) % 137.08/19.60 % (3404652)------------------------------ % 137.08/19.60 % (3404652)------------------------------ % 137.08/19.60 % (3404654)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2681223490:fmbsr=2.30978:i=4348:rtra=on_2854 on theBenchmark for (2854ds/4348Mi) % 137.08/19.60 % (3404654)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.08/19.60 % (3404654)Terminated due to inappropriate strategy. % 137.08/19.60 % (3404654)------------------------------ % 189.40/27.07 % (3404654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.40/27.07 % (3404654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.40/27.07 % (3404654)CaDiCaL version: 2.1.3 % 189.40/27.07 % (3404654)Termination reason: Inappropriate % 189.40/27.07 % (3404654)Time elapsed: 0.004 s % 189.40/27.07 % (3404654)Peak memory usage: 11 MB % 189.40/27.07 % (3404654)Instructions burned: 13 (million) % 189.40/27.07 % (3404654)------------------------------ % 189.40/27.07 % (3404654)------------------------------ % 189.40/27.07 % (3404656)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1601098962:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2853 on theBenchmark for (2853ds/1738Mi) % 189.40/27.07 % (3404656)Instruction limit reached! % 189.40/27.07 % (3404656)------------------------------ % 189.40/27.07 % (3404656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.40/27.07 % (3404656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.40/27.07 % (3404656)CaDiCaL version: 2.1.3 % 189.40/27.07 % (3404656)Termination reason: Instruction limit % 189.40/27.07 % (3404656)Termination phase: Saturation % 189.40/27.07 % (3404656)Time elapsed: 0.347 s % 189.40/27.07 % (3404656)Peak memory usage: 13 MB % 189.40/27.07 % (3404656)Instructions burned: 1738 (million) % 189.40/27.07 % (3404658)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2994727873:i=10228:av=off:rtra=on_2850 on theBenchmark for (2850ds/10228Mi) % 189.40/27.07 % (3404348)Instruction limit reached! % 189.40/27.07 % (3404348)------------------------------ % 189.40/27.07 % (3404348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.40/27.07 % (3404348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.40/27.07 % (3404348)CaDiCaL version: 2.1.3 % 189.40/27.07 % (3404348)Termination reason: Instruction limit % 189.40/27.07 % (3404348)Termination phase: Saturation % 189.40/27.07 % (3404348)Time elapsed: 15.352 s % 189.40/27.07 % (3404348)Peak memory usage: 22 MB % 189.40/27.07 % (3404348)Instructions burned: 88029 (million) % 189.40/27.07 % (3404660)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=779463174:i=108564:rtra=on_2846 on theBenchmark for (2846ds/108564Mi) % 189.40/27.07 % (3404660)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 189.40/27.07 % (3404660)Terminated due to inappropriate strategy. % 189.40/27.07 % (3404660)------------------------------ % 189.40/27.07 % (3404660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.40/27.07 % (3404660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.40/27.07 % (3404660)CaDiCaL version: 2.1.3 % 189.40/27.07 % (3404660)Termination reason: Inappropriate % 189.40/27.07 % (3404660)Time elapsed: 0.005 s % 189.40/27.07 % (3404660)Peak memory usage: 11 MB % 189.40/27.07 % (3404660)Instructions burned: 16 (million) % 189.40/27.07 % (3404660)------------------------------ % 189.40/27.07 % (3404660)------------------------------ % 189.40/27.07 % (3404662)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3630812566:i=7024:aac=none:rtra=on_2846 on theBenchmark for (2846ds/7024Mi) % 189.40/27.07 % (3404648)Instruction limit reached! % 189.40/27.07 % (3404648)------------------------------ % 189.40/27.07 % (3404648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.40/27.07 % (3404648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.40/27.07 % (3404648)CaDiCaL version: 2.1.3 % 189.40/27.07 % (3404648)Termination reason: Instruction limit % 189.40/27.07 % (3404648)Termination phase: Saturation % 189.40/27.07 % (3404648)Time elapsed: 3.208 s % 189.40/27.07 % (3404648)Peak memory usage: 52 MB % 189.40/27.07 % (3404648)Instructions burned: 10263 (million) % 189.40/27.07 % (3404664)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1430231368:i=7546:rtra=on:amm=off_2835 on theBenchmark for (2835ds/7546Mi) % 189.40/27.07 % (3404662)Instruction limit reached! % 189.40/27.07 % (3404662)------------------------------ % 189.40/27.07 % (3404662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.40/27.07 % (3404662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.40/27.07 % (3404662)CaDiCaL version: 2.1.3 % 189.40/27.07 % (3404662)Termination reason: Instruction limit % 189.40/27.07 % (3404662)Termination phase: Saturation % 189.40/27.07 % (3404662)Time elapsed: 2.222 s % 189.40/27.07 % (3404662)Peak memory usage: 47 MB % 189.40/27.07 % (3404662)Instructions burned: 7025 (million) % 189.40/27.07 % (3404666)ott+11_1_sil=16000:si=on:gs=on:random_seed=3871841663:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2823 on theBenchmark for (2823ds/4502Mi) % 247.79/35.37 % (3404658)Instruction limit reached! % 247.79/35.37 % (3404658)------------------------------ % 247.79/35.37 % (3404658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.79/35.37 % (3404658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.79/35.37 % (3404658)CaDiCaL version: 2.1.3 % 247.79/35.37 % (3404658)Termination reason: Instruction limit % 247.79/35.37 % (3404658)Termination phase: Saturation % 247.79/35.37 % (3404658)Time elapsed: 3.367 s % 247.79/35.37 % (3404658)Peak memory usage: 79 MB % 247.79/35.37 % (3404658)Instructions burned: 10229 (million) % 247.79/35.37 % (3404668)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=2720998872:fmbsr=1.6:i=135068:rtra=on_2816 on theBenchmark for (2816ds/135068Mi) % 247.79/35.37 % (3404668)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 247.79/35.37 % (3404668)Terminated due to inappropriate strategy. % 247.79/35.37 % (3404668)------------------------------ % 247.79/35.37 % (3404668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.79/35.37 % (3404668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.79/35.37 % (3404668)CaDiCaL version: 2.1.3 % 247.79/35.37 % (3404668)Termination reason: Inappropriate % 247.79/35.37 % (3404668)Time elapsed: 0.004 s % 247.79/35.37 % (3404668)Peak memory usage: 11 MB % 247.79/35.37 % (3404668)Instructions burned: 14 (million) % 247.79/35.37 % (3404668)------------------------------ % 247.79/35.37 % (3404668)------------------------------ % 247.79/35.37 % (3404670)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1410461637:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2816 on theBenchmark for (2816ds/9182Mi) % 247.79/35.37 % (3404666)Instruction limit reached! % 247.79/35.37 % (3404666)------------------------------ % 247.79/35.37 % (3404666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.79/35.37 % (3404666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.79/35.37 % (3404666)CaDiCaL version: 2.1.3 % 247.79/35.37 % (3404666)Termination reason: Instruction limit % 247.79/35.37 % (3404666)Termination phase: Saturation % 247.79/35.37 % (3404666)Time elapsed: 1.026 s % 247.79/35.37 % (3404666)Peak memory usage: 19 MB % 247.79/35.37 % (3404666)Instructions burned: 4505 (million) % 247.79/35.37 % (3404672)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=2393656539:i=58680:rtra=on_2813 on theBenchmark for (2813ds/58680Mi) % 247.79/35.37 % (3404664)Instruction limit reached! % 247.79/35.37 % (3404664)------------------------------ % 247.79/35.37 % (3404664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.79/35.37 % (3404664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.79/35.37 % (3404664)CaDiCaL version: 2.1.3 % 247.79/35.37 % (3404664)Termination reason: Instruction limit % 247.79/35.37 % (3404664)Termination phase: Saturation % 247.79/35.37 % (3404664)Time elapsed: 2.388 s % 247.79/35.37 % (3404664)Peak memory usage: 45 MB % 247.79/35.37 % (3404664)Instructions burned: 7548 (million) % 247.79/35.37 % (3404674)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=3904257346:i=10422:rtra=on_2811 on theBenchmark for (2811ds/10422Mi) % 247.79/35.37 % (3404592)Instruction limit reached! % 247.79/35.37 % (3404592)------------------------------ % 247.79/35.37 % (3404592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.79/35.37 % (3404592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.79/35.37 % (3404592)CaDiCaL version: 2.1.3 % 247.79/35.37 % (3404592)Termination reason: Instruction limit % 247.79/35.37 % (3404592)Termination phase: Saturation % 247.79/35.37 % (3404592)Time elapsed: 12.348 s % 247.79/35.37 % (3404592)Peak memory usage: 437 MB % 247.79/35.37 % (3404592)Instructions burned: 53297 (million) % 247.79/35.37 % (3404676)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=513719072:i=10994:nm=2:rtra=on_2805 on theBenchmark for (2805ds/10994Mi) % 247.79/35.37 % (3404676)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 247.79/35.37 % (3404676)Terminated due to inappropriate strategy. % 247.79/35.37 % (3404676)------------------------------ % 247.79/35.37 % (3404676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.79/35.37 % (3404676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.79/35.37 % (3404676)CaDiCaL version: 2.1.3 % 247.79/35.37 % (3404676)Termination reason: Inappropriate % 225.14/37.47 % (3404676)Time elapsed: 0.004 s % 225.14/37.47 % (3404676)Peak memory usage: 11 MB % 225.14/37.47 % (3404676)Instructions burned: 15 (million) % 225.14/37.47 % (3404676)------------------------------ % 225.14/37.47 % (3404676)------------------------------ % 225.14/37.47 % (3404678)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:si=on:fmbss=15:random_seed=2326063869:fmbsr=2:i=92664:rtra=on_2805 on theBenchmark for (2805ds/92664Mi) % 225.14/37.47 % (3404678)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.14/37.47 % (3404678)Terminated due to inappropriate strategy. % 225.14/37.47 % (3404678)------------------------------ % 225.14/37.47 % (3404678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.14/37.47 % (3404678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.14/37.47 % (3404678)CaDiCaL version: 2.1.3 % 225.14/37.47 % (3404678)Termination reason: Inappropriate % 225.14/37.47 % (3404678)Time elapsed: 0.004 s % 225.14/37.47 % (3404678)Peak memory usage: 11 MB % 225.14/37.47 % (3404678)Instructions burned: 14 (million) % 225.14/37.47 % (3404678)------------------------------ % 225.14/37.47 % (3404678)------------------------------ % 225.14/37.47 % (3404680)fmb+10_1_sil=128000:tgt=full:sas=cadical:si=on:fmbss=12:random_seed=1244993479:i=28142:rtra=on_2805 on theBenchmark for (2805ds/28142Mi) % 225.14/37.47 % (3404680)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 225.14/37.47 % (3404680)Terminated due to inappropriate strategy. % 225.14/37.47 % (3404680)------------------------------ % 225.14/37.47 % (3404680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.14/37.47 % (3404680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.14/37.47 % (3404680)CaDiCaL version: 2.1.3 % 225.14/37.47 % (3404680)Termination reason: Inappropriate % 225.14/37.47 % (3404680)Time elapsed: 0.004 s % 225.14/37.47 % (3404680)Peak memory usage: 11 MB % 225.14/37.47 % (3404680)Instructions burned: 14 (million) % 225.14/37.47 % (3404680)------------------------------ % 225.14/37.47 % (3404680)------------------------------ % 225.14/37.47 % (3404682)dis+10_161_sil=128000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4210963400:i=45130:add=on:rtra=on:rawr=on_2805 on theBenchmark for (2805ds/45130Mi) % 225.14/37.47 % (3404670)Instruction limit reached! % 225.14/37.47 % (3404670)------------------------------ % 225.14/37.47 % (3404670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.14/37.47 % (3404670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.14/37.47 % (3404670)CaDiCaL version: 2.1.3 % 225.14/37.47 % (3404670)Termination reason: Instruction limit % 225.14/37.47 % (3404670)Termination phase: Saturation % 225.14/37.47 % (3404670)Time elapsed: 1.694 s % 225.14/37.47 % (3404670)Peak memory usage: 14 MB % 225.14/37.47 % (3404670)Instructions burned: 9183 (million) % 225.14/37.47 % (3404686)ott+4_1_sil=16000:si=on:sp=arity:gs=on:random_seed=641874188:i=16346:av=off:rtra=on_2799 on theBenchmark for (2799ds/16346Mi) % 225.14/37.47 % (3404674)Instruction limit reached! % 225.14/37.47 % (3404674)------------------------------ % 225.14/37.47 % (3404674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.14/37.47 % (3404674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.14/37.47 % (3404674)CaDiCaL version: 2.1.3 % 225.14/37.47 % (3404674)Termination reason: Instruction limit % 225.14/37.47 % (3404674)Termination phase: Saturation % 225.14/37.47 % (3404674)Time elapsed: 2.824 s % 225.14/37.47 % (3404674)Peak memory usage: 67 MB % 225.14/37.47 % (3404674)Instructions burned: 10424 (million) % 225.14/37.47 % (3404688)dis+10_16:1_sil=16000:si=on:random_seed=1664706178:i=18310:fsr=off:rtra=on_2783 on theBenchmark for (2783ds/18310Mi) % 225.14/37.47 % (3404686)Instruction limit reached! % 225.14/37.47 % (3404686)------------------------------ % 225.14/37.47 % (3404686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 225.14/37.47 % (3404686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.14/37.47 % (3404686)CaDiCaL version: 2.1.3 % 225.14/37.47 % (3404686)Termination reason: Instruction limit % 225.14/37.47 % (3404686)Termination phase: Saturation % 225.14/37.47 % (3404686)Time elapsed: 5.643 s % 225.14/37.47 % (3404686)Peak memory usage: 145 MB % 225.14/37.47 % (3404686)Instructions burned: 16348 (million) % 225.14/37.47 % (3404690)ott-3_8_sil=64000:si=on:random_seed=1641392079:i=40278:bs=on:rtra=on_2742 on theBenchmark for (2742ds/40278Mi) % 225.14/37.47 % (3404688)Instruction limit reached! % 225.14/37.47 % (3404688)------------------------------ % 274.02/39.03 % (3404688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.02/39.03 % (3404688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.02/39.03 % (3404688)CaDiCaL version: 2.1.3 % 274.02/39.03 % (3404688)Termination reason: Instruction limit % 274.02/39.03 % (3404688)Termination phase: Saturation % 274.02/39.03 % (3404688)Time elapsed: 5.255 s % 274.02/39.03 % (3404688)Peak memory usage: 90 MB % 274.02/39.03 % (3404688)Instructions burned: 18311 (million) % 274.02/39.03 % (3404692)fmb+10_1_sil=64000:tgt=ground:sas=cadical:si=on:bce=on:fmbss=9:random_seed=2362824073:fmbsr=2:i=65152:rtra=on_2730 on theBenchmark for (2730ds/65152Mi) % 274.02/39.03 % (3404692)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 274.02/39.03 % (3404692)Terminated due to inappropriate strategy. % 274.02/39.03 % (3404692)------------------------------ % 274.02/39.03 % (3404692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.02/39.03 % (3404692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.02/39.03 % (3404692)CaDiCaL version: 2.1.3 % 274.02/39.03 % (3404692)Termination reason: Inappropriate % 274.02/39.03 % (3404692)Time elapsed: 0.005 s % 274.02/39.03 % (3404692)Peak memory usage: 11 MB % 274.02/39.03 % (3404692)Instructions burned: 17 (million) % 274.02/39.03 % (3404692)------------------------------ % 274.02/39.03 % (3404692)------------------------------ % 274.02/39.03 % (3404694)ott+10_8:1_sil=16000:si=on:sp=arity:gs=on:random_seed=888081737:i=22808:rtra=on_2730 on theBenchmark for (2730ds/22808Mi) % 274.02/39.03 % (3404682)Instruction limit reached! % 274.02/39.03 % (3404682)------------------------------ % 274.02/39.03 % (3404682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.02/39.03 % (3404682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.02/39.03 % (3404682)CaDiCaL version: 2.1.3 % 274.02/39.03 % (3404682)Termination reason: Instruction limit % 274.02/39.03 % (3404682)Termination phase: Saturation % 274.02/39.03 % (3404682)Time elapsed: 7.926 s % 274.02/39.03 % (3404682)Peak memory usage: 20 MB % 274.02/39.03 % (3404682)Instructions burned: 45133 (million) % 274.02/39.03 % (3404696)ott-11_1_sil=16000:si=on:alpa=false:sac=on:random_seed=3927909643:i=28268:rtra=on_2725 on theBenchmark for (2725ds/28268Mi) % 274.02/39.03 % (3404672)Instruction limit reached! % 274.02/39.03 % (3404672)------------------------------ % 274.02/39.03 % (3404672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.02/39.03 % (3404672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.02/39.03 % (3404672)CaDiCaL version: 2.1.3 % 274.02/39.03 % (3404672)Termination reason: Instruction limit % 274.02/39.03 % (3404672)Termination phase: Saturation % 274.02/39.03 % (3404672)Time elapsed: 11.005 s % 274.02/39.03 % (3404672)Peak memory usage: 16 MB % 274.02/39.03 % (3404672)Instructions burned: 58681 (million) % 274.02/39.03 % (3404698)dis+33_16_sil=32000:si=on:sac=on:random_seed=758515891:i=31702:nm=0:rtra=on_2703 on theBenchmark for (2703ds/31702Mi) % 274.02/39.03 % (3404690)Instruction limit reached! % 274.02/39.03 % (3404690)------------------------------ % 274.02/39.03 % (3404690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.02/39.03 % (3404690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.02/39.03 % (3404690)CaDiCaL version: 2.1.3 % 274.02/39.03 % (3404690)Termination reason: Instruction limit % 274.02/39.03 % (3404690)Termination phase: Saturation % 274.02/39.03 % (3404690)Time elapsed: 6.946 s % 274.02/39.03 % (3404690)Peak memory usage: 15 MB % 274.02/39.03 % (3404690)Instructions burned: 40280 (million) % 274.02/39.03 % (3404701)dis+4_1024_sil=32000:si=on:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=567488771:avsq=on:i=35254:add=on:rtra=on:amm=off_2672 on theBenchmark for (2672ds/35254Mi) % 274.02/39.03 % (3404698)Instruction limit reached! % 274.02/39.03 % (3404698)------------------------------ % 274.02/39.03 % (3404698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.02/39.03 % (3404698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.02/39.03 % (3404698)CaDiCaL version: 2.1.3 % 274.02/39.03 % (3404698)Termination reason: Instruction limit % 274.02/39.03 % (3404698)Termination phase: Saturation % 274.02/39.03 % (3404698)Time elapsed: 5.519 s % 274.02/39.03 % (3404698)Peak memory usage: 14 MB % 274.02/39.03 % (3404698)Instructions burned: 31703 (million) % 274.02/39.03 % (3404703)ott+10_64_anc=all:sil=128000:sas=cadical:si=on:bsr=unit_only:nwc=1:cn=on:random_seed=50221143:s2a=on:i=106590:rtra=on_2647 on theBenchmark for (2647ds/106590Mi) % 277.96/39.61 % (3404694)Instruction limit reached! % 277.96/39.61 % (3404694)------------------------------ % 277.96/39.61 % (3404694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.96/39.61 % (3404694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.96/39.61 % (3404694)CaDiCaL version: 2.1.3 % 277.96/39.61 % (3404694)Termination reason: Instruction limit % 277.96/39.61 % (3404694)Termination phase: Saturation % 277.96/39.61 % (3404694)Time elapsed: 9.122 s % 277.96/39.61 % (3404694)Peak memory usage: 237 MB % 277.96/39.61 % (3404694)Instructions burned: 22808 (million) % 277.96/39.61 % (3404705)fmb+10_1_sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3120255640:i=53714:ins=20:rtra=on_2638 on theBenchmark for (2638ds/53714Mi) % 277.96/39.61 % (3404705)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.96/39.61 % (3404705)Terminated due to inappropriate strategy. % 277.96/39.61 % (3404705)------------------------------ % 277.96/39.61 % (3404705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.96/39.61 % (3404705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.96/39.61 % (3404705)CaDiCaL version: 2.1.3 % 277.96/39.61 % (3404705)Termination reason: Inappropriate % 277.96/39.61 % (3404705)Time elapsed: 0.004 s % 277.96/39.61 % (3404705)Peak memory usage: 11 MB % 277.96/39.61 % (3404705)Instructions burned: 13 (million) % 277.96/39.61 % (3404705)------------------------------ % 277.96/39.61 % (3404705)------------------------------ % 277.96/39.61 % (3404707)ott+10_1_sil=64000:plsq=on:plsqc=4:si=on:bsr=unit_only:gs=on:random_seed=2928880753:i=56240:bs=on:fsr=off:rtra=on_2638 on theBenchmark for (2638ds/56240Mi) % 277.96/39.61 % (3404347)Instruction limit reached! % 277.96/39.61 % (3404347)------------------------------ % 277.96/39.61 % (3404347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.96/39.61 % (3404347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.96/39.61 % (3404347)CaDiCaL version: 2.1.3 % 277.96/39.61 % (3404347)Termination reason: Instruction limit % 277.96/39.61 % (3404347)Termination phase: Saturation % 277.96/39.61 % (3404347)Time elapsed: 37.233 s % 277.96/39.61 % (3404347)Peak memory usage: 321 MB % 277.96/39.61 % (3404347)Instructions burned: 135534 (million) % 277.96/39.61 % (3404709)fmb+10_1_sil=256000:si=on:fmbss=7:random_seed=4032535715:fmbsr=1.6:i=364590:rtra=on_2627 on theBenchmark for (2627ds/364590Mi) % 277.96/39.61 % (3404709)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.96/39.61 % (3404709)Terminated due to inappropriate strategy. % 277.96/39.61 % (3404709)------------------------------ % 277.96/39.61 % (3404709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.96/39.61 % (3404709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.96/39.61 % (3404709)CaDiCaL version: 2.1.3 % 277.96/39.61 % (3404709)Termination reason: Inappropriate % 277.96/39.61 % (3404709)Time elapsed: 0.004 s % 277.96/39.61 % (3404709)Peak memory usage: 11 MB % 277.96/39.61 % (3404709)Instructions burned: 13 (million) % 277.96/39.61 % (3404709)------------------------------ % 277.96/39.61 % (3404709)------------------------------ % 277.96/39.61 % (3404711)fmb+10_1_sil=128000:si=on:fmbss=21:newcnf=on:random_seed=3742146593:i=89250:rtra=on:gsp=on_2626 on theBenchmark for (2626ds/89250Mi) % 277.96/39.61 % (3404711)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.96/39.61 % (3404711)Terminated due to inappropriate strategy. % 277.96/39.61 % (3404711)------------------------------ % 277.96/39.61 % (3404711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.96/39.61 % (3404711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.96/39.61 % (3404711)CaDiCaL version: 2.1.3 % 277.96/39.61 % (3404711)Termination reason: Inappropriate % 277.96/39.61 % (3404711)Time elapsed: 0.004 s % 277.96/39.61 % (3404711)Peak memory usage: 11 MB % 277.96/39.61 % (3404711)Instructions burned: 14 (million) % 277.96/39.61 % (3404711)------------------------------ % 277.96/39.61 % (3404711)------------------------------ % 277.96/39.61 % (3404713)fmb+10_1_sil=256000:sas=cadical:si=on:fmbss=15:random_seed=615802101:i=321010:rtra=on_2626 on theBenchmark for (2626ds/321010Mi) % 277.96/39.61 % (3404713)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 277.96/39.61 % (3404713)Terminated due to inappropriate strategy. % 277.96/39.61 % (3404713)------------------------------ % 277.96/39.61 % (3404713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.96/39.61 % (3404713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.72/40.40 % (3404713)CaDiCaL version: 2.1.3 % 283.72/40.40 % (3404713)Termination reason: Inappropriate % 283.72/40.40 % (3404713)Time elapsed: 0.004 s % 283.72/40.40 % (3404713)Peak memory usage: 11 MB % 283.72/40.40 % (3404713)Instructions burned: 13 (million) % 283.72/40.40 % (3404713)------------------------------ % 283.72/40.40 % (3404713)------------------------------ % 283.72/40.40 % (3404715)fmb+10_1_sil=256000:tgt=full:si=on:fmbss=10:random_seed=612084640:fmbsr=1.3:i=451458:rtra=on_2626 on theBenchmark for (2626ds/451458Mi) % 283.72/40.40 % (3404715)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.72/40.40 % (3404715)Terminated due to inappropriate strategy. % 283.72/40.40 % (3404715)------------------------------ % 283.72/40.40 % (3404715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.72/40.40 % (3404715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.72/40.40 % (3404715)CaDiCaL version: 2.1.3 % 283.72/40.40 % (3404715)Termination reason: Inappropriate % 283.72/40.40 % (3404715)Time elapsed: 0.004 s % 283.72/40.40 % (3404715)Peak memory usage: 11 MB % 283.72/40.40 % (3404715)Instructions burned: 14 (million) % 283.72/40.40 % (3404715)------------------------------ % 283.72/40.40 % (3404715)------------------------------ % 283.72/40.40 % (3404717)fmb+10_1_sil=256000:tgt=full:sas=cadical:si=on:fmbss=10:random_seed=2381305860:fmbsr=2:i=370048:ins=7:rtra=on_2626 on theBenchmark for (2626ds/370048Mi) % 283.72/40.40 % (3404717)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.72/40.40 % (3404717)Terminated due to inappropriate strategy. % 283.72/40.40 % (3404717)------------------------------ % 283.72/40.40 % (3404717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.72/40.40 % (3404717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.72/40.40 % (3404717)CaDiCaL version: 2.1.3 % 283.72/40.40 % (3404717)Termination reason: Inappropriate % 283.72/40.40 % (3404717)Time elapsed: 0.004 s % 283.72/40.40 % (3404717)Peak memory usage: 11 MB % 283.72/40.40 % (3404717)Instructions burned: 14 (million) % 283.72/40.40 % (3404717)------------------------------ % 283.72/40.40 % (3404717)------------------------------ % 283.72/40.40 % (3404719)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2342921655:rtra=on_2626 on theBenchmark for (2626ds/0Mi) % 283.72/40.40 % (3404719)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.72/40.40 % (3404719)Terminated due to inappropriate strategy. % 283.72/40.40 % (3404719)------------------------------ % 283.72/40.40 % (3404719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.72/40.40 % (3404719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.72/40.40 % (3404719)CaDiCaL version: 2.1.3 % 283.72/40.40 % (3404719)Termination reason: Inappropriate % 283.72/40.40 % (3404719)Time elapsed: 0.005 s % 283.72/40.40 % (3404719)Peak memory usage: 11 MB % 283.72/40.40 % (3404719)Instructions burned: 16 (million) % 283.72/40.40 % (3404719)------------------------------ % 283.72/40.40 % (3404719)------------------------------ % 283.72/40.40 % (3404721)% WARNING: option uhcvi not known. % 283.72/40.40 % (3404721)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=333481113:i=542124:add=off:rtra=on:rawr=on_2626 on theBenchmark for (2626ds/542124Mi) % 283.72/40.40 % (3404696)Instruction limit reached! % 283.72/40.40 % (3404696)------------------------------ % 283.72/40.40 % (3404696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.72/40.40 % (3404696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.72/40.40 % (3404696)CaDiCaL version: 2.1.3 % 283.72/40.40 % (3404696)Termination reason: Instruction limit % 283.72/40.40 % (3404696)Termination phase: Saturation % 283.72/40.40 % (3404696)Time elapsed: 10.506 s % 283.72/40.40 % (3404696)Peak memory usage: 130 MB % 283.72/40.40 % (3404696)Instructions burned: 28270 (million) % 283.72/40.40 % (3404723)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2467135807:i=352096:add=on:rtra=on:rawr=on_2620 on theBenchmark for (2620ds/352096Mi) % 283.72/40.40 % (3404612)Instruction limit reached! % 283.72/40.40 % (3404612)------------------------------ % 283.72/40.40 % (3404612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.72/40.40 % (3404612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.72/40.40 % (3404612)CaDiCaL version: 2.1.3 % 283.72/40.40 % (3404612)Termination reason: Instruction limit % 293.83/41.96 % (3404612)Termination phase: Saturation % 293.83/41.96 % (3404612)Time elapsed: 29.182 s % 293.83/41.96 % (3404612)Peak memory usage: 33 MB % 293.83/41.96 % (3404612)Instructions burned: 176054 (million) % 293.83/41.96 % (3404725)dis+10_1_sil=32000:si=on:sp=arity:random_seed=405063524:i=412:fgj=on:rtra=on_2611 on theBenchmark for (2611ds/412Mi) % 293.83/41.96 % (3404725)Instruction limit reached! % 293.83/41.96 % (3404725)------------------------------ % 293.83/41.96 % (3404725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.83/41.96 % (3404725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.83/41.96 % (3404725)CaDiCaL version: 2.1.3 % 293.83/41.96 % (3404725)Termination reason: Instruction limit % 293.83/41.96 % (3404725)Termination phase: Saturation % 293.83/41.96 % (3404725)Time elapsed: 0.135 s % 293.83/41.96 % (3404725)Peak memory usage: 15 MB % 293.83/41.96 % (3404725)Instructions burned: 414 (million) % 293.83/41.96 % (3404727)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1989331015:i=464:rtra=on_2609 on theBenchmark for (2609ds/464Mi) % 293.83/41.96 % (3404727)Instruction limit reached! % 293.83/41.96 % (3404727)------------------------------ % 293.83/41.96 % (3404727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.83/41.96 % (3404727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.83/41.96 % (3404727)CaDiCaL version: 2.1.3 % 293.83/41.96 % (3404727)Termination reason: Instruction limit % 293.83/41.96 % (3404727)Termination phase: Saturation % 293.83/41.96 % (3404727)Time elapsed: 0.109 s % 293.83/41.96 % (3404727)Peak memory usage: 13 MB % 293.83/41.96 % (3404727)Instructions burned: 469 (million) % 293.83/41.96 % (3404729)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4044165572:i=524:rtra=on_2608 on theBenchmark for (2608ds/524Mi) % 293.83/41.96 % (3404729)Instruction limit reached! % 293.83/41.96 % (3404729)------------------------------ % 293.83/41.96 % (3404729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.83/41.96 % (3404729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.83/41.96 % (3404729)CaDiCaL version: 2.1.3 % 293.83/41.96 % (3404729)Termination reason: Instruction limit % 293.83/41.96 % (3404729)Termination phase: Saturation % 293.83/41.96 % (3404729)Time elapsed: 0.146 s % 293.83/41.97 % (3404729)Peak memory usage: 15 MB % 293.83/41.97 % (3404729)Instructions burned: 525 (million) % 293.83/41.97 % (3404731)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1699138406:i=636:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2606 on theBenchmark for (2606ds/636Mi) % 293.83/41.97 % (3404701)Instruction limit reached! % 293.83/41.97 % (3404701)------------------------------ % 293.83/41.97 % (3404701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.83/41.97 % (3404701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.83/41.97 % (3404701)CaDiCaL version: 2.1.3 % 293.83/41.97 % (3404701)Termination reason: Instruction limit % 293.83/41.97 % (3404701)Termination phase: Saturation % 293.83/41.97 % (3404701)Time elapsed: 6.680 s % 293.83/41.97 % (3404701)Peak memory usage: 17 MB % 293.83/41.97 % (3404701)Instructions burned: 35255 (million) % 293.83/41.97 % (3404733)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1810899540:i=2856:nm=2:rtra=on_2606 on theBenchmark for (2606ds/2856Mi) % 293.83/41.97 % (3404733)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 293.83/41.97 % (3404733)Terminated due to inappropriate strategy. % 293.83/41.97 % (3404733)------------------------------ % 293.83/41.97 % (3404733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.83/41.97 % (3404733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.83/41.97 % (3404733)CaDiCaL version: 2.1.3 % 293.83/41.97 % (3404733)Termination reason: Inappropriate % 293.83/41.97 % (3404733)Time elapsed: 0.004 s % 293.83/41.97 % (3404733)Peak memory usage: 11 MB % 293.83/41.97 % (3404733)Instructions burned: 13 (million) % 293.83/41.97 % (3404733)------------------------------ % 293.83/41.97 % (3404733)------------------------------ % 293.83/41.97 % (3404735)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2485713312:i=524:bd=preordered:rtra=on:fsd=on_2605 on theBenchmark for (2605ds/524Mi) % 293.83/41.97 % (3404731)Instruction limit reached! % 293.83/41.97 % (3404731)------------------------------ % 293.83/41.97 % (3404731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.83/41.97 % (3404731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-91Terminated % 300.36/42.83 % Vampire exiting %------------------------------------------------------------------------------