%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC480_1 : TPTP v9.3.1. Bugfixed v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n013.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:06:03 PM UTC 2026 % Result : Timeout 291.17s 41.30s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC480_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.20 % Computer : n013.cluster.edu % 0.08/0.20 % Model : x86_64 x86_64 % 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.20 % Memory : 8046.5625MB % 0.08/0.20 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 09:39:51 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.23 Running first-order model finding % 0.08/0.23 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 % 4.05/0.92 % (1054531)Will run a generic schedule for satisfiability detection. % 4.05/0.92 % (1054539)dis+10_1_sil=32000:sp=arity:random_seed=1191197385:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.05/0.92 % (1054537)% WARNING: option uhcvi not known. % 4.05/0.92 % (1054536)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3267391283_2999 on theBenchmark for (2999ds/0Mi) % 4.05/0.92 % (1054537)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3789245875:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.05/0.92 % (1054538)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3403299461:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.05/0.92 % (1054540)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2610946176:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.05/0.92 % (1054536)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.05/0.92 % (1054536)Terminated due to inappropriate strategy. % 4.05/0.92 % (1054536)------------------------------ % 4.05/0.92 % (1054536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.05/0.92 % (1054536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.05/0.92 % (1054536)CaDiCaL version: 2.1.3 % 4.05/0.92 % (1054536)Termination reason: Inappropriate % 4.05/0.92 % (1054536)Time elapsed: 0.001 s % 4.05/0.92 % (1054536)Peak memory usage: 10 MB % 4.05/0.92 % (1054536)Instructions burned: 1 (million) % 4.05/0.92 % (1054536)------------------------------ % 4.05/0.92 % (1054536)------------------------------ % 4.05/0.92 % (1054541)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2006991743:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.05/0.92 % (1054542)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3366679436:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.05/0.92 % (1054548)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2850381823:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.05/0.92 % (1054548)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.05/0.92 % (1054548)Terminated due to inappropriate strategy. % 4.05/0.92 % (1054548)------------------------------ % 4.05/0.92 % (1054548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.05/0.92 % (1054548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.05/0.92 % (1054548)CaDiCaL version: 2.1.3 % 4.05/0.92 % (1054548)Termination reason: Inappropriate % 4.05/0.92 % (1054548)Time elapsed: 0.001 s % 4.05/0.92 % (1054548)Peak memory usage: 11 MB % 4.05/0.92 % (1054548)Instructions burned: 1 (million) % 4.05/0.92 % (1054548)------------------------------ % 4.05/0.92 % (1054548)------------------------------ % 4.05/0.92 % (1054539)Instruction limit reached! % 4.05/0.92 % (1054539)------------------------------ % 4.05/0.92 % (1054539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.05/0.92 % (1054539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.05/0.92 % (1054539)CaDiCaL version: 2.1.3 % 4.05/0.92 % (1054539)Termination reason: Instruction limit % 4.05/0.92 % (1054539)Termination phase: Saturation % 4.05/0.92 % (1054539)Time elapsed: 0.035 s % 4.05/0.92 % (1054539)Peak memory usage: 12 MB % 4.05/0.92 % (1054539)Instructions burned: 105 (million) % 4.05/0.92 % (1054553)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=190353398:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.05/0.92 % (1054552)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1591523726:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.05/0.92 % (1054540)Instruction limit reached! % 4.05/0.92 % (1054540)------------------------------ % 4.05/0.92 % (1054540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.05/0.92 % (1054540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.05/0.92 % (1054540)CaDiCaL version: 2.1.3 % 4.05/0.92 % (1054540)Termination reason: Instruction limit % 4.05/0.92 % (1054540)Termination phase: Saturation % 4.05/0.92 % (1054540)Time elapsed: 0.071 s % 4.05/0.92 % (1054540)Peak memory usage: 12 MB % 4.05/0.92 % (1054540)Instructions burned: 117 (million) % 4.05/0.92 % (1054541)Instruction limit reached! % 4.05/0.92 % (1054541)------------------------------ % 4.05/0.92 % (1054541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.57/1.24 % (1054541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.57/1.24 % (1054541)CaDiCaL version: 2.1.3 % 6.57/1.24 % (1054541)Termination reason: Instruction limit % 6.57/1.24 % (1054541)Termination phase: Saturation % 6.57/1.24 % (1054541)Time elapsed: 0.082 s % 6.57/1.24 % (1054541)Peak memory usage: 13 MB % 6.57/1.24 % (1054541)Instructions burned: 131 (million) % 6.57/1.24 % (1054556)ott-21_1_sil=16000:fs=off:random_seed=3390272472:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.57/1.24 % (1054557)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1600521143:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.57/1.24 % (1054552)Instruction limit reached! % 6.57/1.24 % (1054552)------------------------------ % 6.57/1.24 % (1054552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.57/1.24 % (1054552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.57/1.24 % (1054552)CaDiCaL version: 2.1.3 % 6.57/1.24 % (1054552)Termination reason: Instruction limit % 6.57/1.24 % (1054552)Termination phase: Saturation % 6.57/1.24 % (1054552)Time elapsed: 0.090 s % 6.57/1.24 % (1054552)Peak memory usage: 13 MB % 6.57/1.24 % (1054552)Instructions burned: 131 (million) % 6.57/1.24 % (1054542)Instruction limit reached! % 6.57/1.24 % (1054542)------------------------------ % 6.57/1.24 % (1054542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.57/1.24 % (1054542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.57/1.24 % (1054542)CaDiCaL version: 2.1.3 % 6.57/1.24 % (1054542)Termination reason: Instruction limit % 6.57/1.24 % (1054542)Termination phase: Saturation % 6.57/1.24 % (1054542)Time elapsed: 0.141 s % 6.57/1.24 % (1054542)Peak memory usage: 13 MB % 6.57/1.24 % (1054542)Instructions burned: 160 (million) % 6.57/1.24 % (1054573)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2029386874:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.57/1.24 % (1054573)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.57/1.24 % (1054573)Terminated due to inappropriate strategy. % 6.57/1.24 % (1054573)------------------------------ % 6.57/1.24 % (1054573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.57/1.24 % (1054573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.57/1.24 % (1054573)CaDiCaL version: 2.1.3 % 6.57/1.24 % (1054573)Termination reason: Inappropriate % 6.57/1.24 % (1054573)Time elapsed: 0.001 s % 6.57/1.24 % (1054573)Peak memory usage: 10 MB % 6.57/1.24 % (1054573)Instructions burned: 1 (million) % 6.57/1.24 % (1054573)------------------------------ % 6.57/1.24 % (1054573)------------------------------ % 6.57/1.24 % (1054576)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=576298242:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.57/1.24 % (1054556)Instruction limit reached! % 6.57/1.24 % (1054556)------------------------------ % 6.57/1.24 % (1054556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.57/1.24 % (1054556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.57/1.24 % (1054556)CaDiCaL version: 2.1.3 % 6.57/1.24 % (1054556)Termination reason: Instruction limit % 6.57/1.24 % (1054556)Termination phase: Saturation % 6.57/1.24 % (1054556)Time elapsed: 0.080 s % 6.57/1.24 % (1054556)Peak memory usage: 12 MB % 6.57/1.24 % (1054556)Instructions burned: 181 (million) % 6.57/1.24 % (1054580)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1360564597:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.57/1.24 % (1054580)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.57/1.24 % (1054580)Terminated due to inappropriate strategy. % 6.57/1.24 % (1054580)------------------------------ % 6.57/1.24 % (1054580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.57/1.24 % (1054580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.57/1.24 % (1054580)CaDiCaL version: 2.1.3 % 6.57/1.24 % (1054580)Termination reason: Inappropriate % 6.57/1.24 % (1054580)Time elapsed: 0.001 s % 6.57/1.24 % (1054580)Peak memory usage: 10 MB % 6.57/1.24 % (1054580)Instructions burned: 1 (million) % 6.57/1.24 % (1054580)------------------------------ % 6.57/1.24 % (1054580)------------------------------ % 6.57/1.24 % (1054587)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=246169663:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 27.02/4.14 % (1054592)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2143547280:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 27.02/4.14 % (1054553)Instruction limit reached! % 27.02/4.14 % (1054553)------------------------------ % 27.02/4.14 % (1054553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.02/4.14 % (1054553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.14 % (1054553)CaDiCaL version: 2.1.3 % 27.02/4.14 % (1054553)Termination reason: Instruction limit % 27.02/4.14 % (1054553)Termination phase: Saturation % 27.02/4.14 % (1054553)Time elapsed: 0.194 s % 27.02/4.14 % (1054553)Peak memory usage: 18 MB % 27.02/4.14 % (1054553)Instructions burned: 685 (million) % 27.02/4.14 % (1054612)fmb+10_1_sil=64000:random_seed=2011674859:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 27.02/4.14 % (1054612)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.02/4.14 % (1054612)Terminated due to inappropriate strategy. % 27.02/4.14 % (1054612)------------------------------ % 27.02/4.14 % (1054612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.02/4.14 % (1054612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.14 % (1054612)CaDiCaL version: 2.1.3 % 27.02/4.14 % (1054612)Termination reason: Inappropriate % 27.02/4.14 % (1054612)Time elapsed: 0.0000 s % 27.02/4.14 % (1054612)Peak memory usage: 11 MB % 27.02/4.14 % (1054612)Instructions burned: 1 (million) % 27.02/4.14 % (1054612)------------------------------ % 27.02/4.14 % (1054612)------------------------------ % 27.02/4.14 % (1054618)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1641942157:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 27.02/4.14 % (1054618)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.02/4.14 % (1054618)Terminated due to inappropriate strategy. % 27.02/4.14 % (1054618)------------------------------ % 27.02/4.14 % (1054618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.02/4.14 % (1054618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.14 % (1054618)CaDiCaL version: 2.1.3 % 27.02/4.14 % (1054618)Termination reason: Inappropriate % 27.02/4.14 % (1054618)Time elapsed: 0.0000 s % 27.02/4.14 % (1054618)Peak memory usage: 10 MB % 27.02/4.14 % (1054618)Instructions burned: 1 (million) % 27.02/4.14 % (1054618)------------------------------ % 27.02/4.14 % (1054618)------------------------------ % 27.02/4.14 % (1054626)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3697548269:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 27.02/4.14 % (1054626)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.02/4.14 % (1054626)Terminated due to inappropriate strategy. % 27.02/4.14 % (1054626)------------------------------ % 27.02/4.14 % (1054626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.02/4.14 % (1054626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.14 % (1054626)CaDiCaL version: 2.1.3 % 27.02/4.14 % (1054626)Termination reason: Inappropriate % 27.02/4.14 % (1054626)Time elapsed: 0.0000 s % 27.02/4.14 % (1054626)Peak memory usage: 11 MB % 27.02/4.14 % (1054626)Instructions burned: 1 (million) % 27.02/4.14 % (1054626)------------------------------ % 27.02/4.14 % (1054626)------------------------------ % 27.02/4.14 % (1054636)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2905044233:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 27.02/4.14 % (1054557)Instruction limit reached! % 27.02/4.14 % (1054557)------------------------------ % 27.02/4.14 % (1054557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.02/4.14 % (1054557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.14 % (1054557)CaDiCaL version: 2.1.3 % 27.02/4.14 % (1054557)Termination reason: Instruction limit % 27.02/4.14 % (1054557)Termination phase: Saturation % 27.02/4.14 % (1054557)Time elapsed: 0.291 s % 27.02/4.14 % (1054557)Peak memory usage: 14 MB % 27.02/4.14 % (1054557)Instructions burned: 477 (million) % 27.02/4.14 % (1054661)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2924119118:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 27.02/4.14 % (1054587)Instruction limit reached! % 27.02/4.14 % (1054587)------------------------------ % 39.41/5.81 % (1054587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.41/5.81 % (1054587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.41/5.81 % (1054587)CaDiCaL version: 2.1.3 % 39.41/5.81 % (1054587)Termination reason: Instruction limit % 39.41/5.81 % (1054587)Termination phase: Saturation % 39.41/5.81 % (1054587)Time elapsed: 0.452 s % 39.41/5.81 % (1054587)Peak memory usage: 17 MB % 39.41/5.81 % (1054587)Instructions burned: 692 (million) % 39.41/5.81 % (1054710)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=633126425:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 39.41/5.81 % (1054710)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.41/5.81 % (1054710)Terminated due to inappropriate strategy. % 39.41/5.81 % (1054710)------------------------------ % 39.41/5.81 % (1054710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.41/5.81 % (1054710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.41/5.81 % (1054710)CaDiCaL version: 2.1.3 % 39.41/5.81 % (1054710)Termination reason: Inappropriate % 39.41/5.81 % (1054710)Time elapsed: 0.001 s % 39.41/5.81 % (1054710)Peak memory usage: 10 MB % 39.41/5.81 % (1054710)Instructions burned: 1 (million) % 39.41/5.81 % (1054710)------------------------------ % 39.41/5.81 % (1054710)------------------------------ % 39.41/5.81 % (1054712)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2146027197:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 39.41/5.81 % (1054712)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.41/5.81 % (1054712)Terminated due to inappropriate strategy. % 39.41/5.81 % (1054712)------------------------------ % 39.41/5.81 % (1054712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.41/5.81 % (1054712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.41/5.81 % (1054712)CaDiCaL version: 2.1.3 % 39.41/5.81 % (1054712)Termination reason: Inappropriate % 39.41/5.81 % (1054712)Time elapsed: 0.001 s % 39.41/5.81 % (1054712)Peak memory usage: 10 MB % 39.41/5.81 % (1054712)Instructions burned: 1 (million) % 39.41/5.81 % (1054712)------------------------------ % 39.41/5.81 % (1054712)------------------------------ % 39.41/5.81 % (1054714)ott-2_1_sil=16000:newcnf=on:random_seed=726099020:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 39.41/5.81 % (1054592)Instruction limit reached! % 39.41/5.81 % (1054592)------------------------------ % 39.41/5.81 % (1054592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.41/5.81 % (1054592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.41/5.81 % (1054592)CaDiCaL version: 2.1.3 % 39.41/5.81 % (1054592)Termination reason: Instruction limit % 39.41/5.81 % (1054592)Termination phase: Saturation % 39.41/5.81 % (1054592)Time elapsed: 0.562 s % 39.41/5.81 % (1054592)Peak memory usage: 18 MB % 39.41/5.81 % (1054592)Instructions burned: 879 (million) % 39.41/5.81 % (1054716)ott+10_1_sil=32000:tgt=ground:random_seed=150193043:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi) % 39.41/5.81 % (1054576)Instruction limit reached! % 39.41/5.81 % (1054576)------------------------------ % 39.41/5.81 % (1054576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.41/5.81 % (1054576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.41/5.81 % (1054576)CaDiCaL version: 2.1.3 % 39.41/5.81 % (1054576)Termination reason: Instruction limit % 39.41/5.81 % (1054576)Termination phase: Saturation % 39.41/5.81 % (1054576)Time elapsed: 0.774 s % 39.41/5.81 % (1054576)Peak memory usage: 18 MB % 39.41/5.81 % (1054576)Instructions burned: 1180 (million) % 39.41/5.81 % (1054718)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2718198230:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 39.41/5.81 % (1054718)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.41/5.81 % (1054718)Terminated due to inappropriate strategy. % 39.41/5.81 % (1054718)------------------------------ % 39.41/5.81 % (1054718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.41/5.81 % (1054718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.41/5.81 % (1054718)CaDiCaL version: 2.1.3 % 39.41/5.81 % (1054718)Termination reason: Inappropriate % 39.41/5.81 % (1054718)Time elapsed: 0.001 s % 39.41/5.81 % (1054718)Peak memory usage: 11 MB % 39.41/5.81 % (1054718)Instructions burned: 1 (million) % 146.85/21.04 % (1054718)------------------------------ % 146.85/21.04 % (1054718)------------------------------ % 146.85/21.04 % (1054720)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3682674043:i=3512:aac=none_2989 on theBenchmark for (2989ds/3512Mi) % 146.85/21.04 % (1054661)Instruction limit reached! % 146.85/21.04 % (1054661)------------------------------ % 146.85/21.04 % (1054661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.85/21.04 % (1054661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.85/21.04 % (1054661)CaDiCaL version: 2.1.3 % 146.85/21.04 % (1054661)Termination reason: Instruction limit % 146.85/21.04 % (1054661)Termination phase: Saturation % 146.85/21.04 % (1054661)Time elapsed: 0.719 s % 146.85/21.04 % (1054661)Peak memory usage: 22 MB % 146.85/21.04 % (1054661)Instructions burned: 1474 (million) % 146.85/21.04 % (1054722)dis+21_1_sil=32000:sas=cadical:random_seed=3451211296:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 146.85/21.04 % (1054714)Instruction limit reached! % 146.85/21.04 % (1054714)------------------------------ % 146.85/21.04 % (1054714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.85/21.04 % (1054714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.85/21.04 % (1054714)CaDiCaL version: 2.1.3 % 146.85/21.04 % (1054714)Termination reason: Instruction limit % 146.85/21.04 % (1054714)Termination phase: Saturation % 146.85/21.04 % (1054714)Time elapsed: 0.515 s % 146.85/21.04 % (1054714)Peak memory usage: 15 MB % 146.85/21.04 % (1054714)Instructions burned: 869 (million) % 146.85/21.04 % (1054732)ott+11_1_sil=16000:gs=on:random_seed=549207980:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 146.85/21.04 % (1054636)Instruction limit reached! % 146.85/21.04 % (1054636)------------------------------ % 146.85/21.04 % (1054636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.85/21.04 % (1054636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.85/21.04 % (1054636)CaDiCaL version: 2.1.3 % 146.85/21.04 % (1054636)Termination reason: Instruction limit % 146.85/21.04 % (1054636)Termination phase: Saturation % 146.85/21.04 % (1054636)Time elapsed: 1.777 s % 146.85/21.04 % (1054636)Peak memory usage: 42 MB % 146.85/21.04 % (1054636)Instructions burned: 5132 (million) % 146.85/21.04 % (1054766)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=181882767:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 146.85/21.04 % (1054766)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.85/21.04 % (1054766)Terminated due to inappropriate strategy. % 146.85/21.04 % (1054766)------------------------------ % 146.85/21.04 % (1054766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.85/21.04 % (1054766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.85/21.04 % (1054766)CaDiCaL version: 2.1.3 % 146.85/21.04 % (1054766)Termination reason: Inappropriate % 146.85/21.04 % (1054766)Time elapsed: 0.001 s % 146.85/21.04 % (1054766)Peak memory usage: 10 MB % 146.85/21.04 % (1054766)Instructions burned: 1 (million) % 146.85/21.04 % (1054766)------------------------------ % 146.85/21.04 % (1054766)------------------------------ % 146.85/21.04 % (1054770)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=433450332:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2978 on theBenchmark for (2978ds/4591Mi) % 146.85/21.04 % (1054732)Instruction limit reached! % 146.85/21.04 % (1054732)------------------------------ % 146.85/21.04 % (1054732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.85/21.04 % (1054732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.85/21.04 % (1054732)CaDiCaL version: 2.1.3 % 146.85/21.04 % (1054732)Termination reason: Instruction limit % 146.85/21.04 % (1054732)Termination phase: Saturation % 146.85/21.04 % (1054732)Time elapsed: 1.987 s % 146.85/21.04 % (1054732)Peak memory usage: 24 MB % 146.85/21.04 % (1054732)Instructions burned: 2251 (million) % 146.85/21.04 % (1054815)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2958980217:i=29340_2966 on theBenchmark for (2966ds/29340Mi) % 146.85/21.04 % (1054720)Instruction limit reached! % 146.85/21.04 % (1054720)------------------------------ % 146.85/21.04 % (1054720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.85/21.04 % (1054720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.85/21.04 % (1054720)CaDiCaL version: 2.1.3 % 146.85/21.04 % (1054720)Termination reason: Instruction limit % 179.59/25.54 % (1054720)Termination phase: Saturation % 179.59/25.54 % (1054720)Time elapsed: 2.879 s % 179.59/25.54 % (1054720)Peak memory usage: 35 MB % 179.59/25.54 % (1054720)Instructions burned: 3512 (million) % 179.59/25.54 % (1054836)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1326483316:i=5211_2960 on theBenchmark for (2960ds/5211Mi) % 179.59/25.54 % (1054722)Instruction limit reached! % 179.59/25.54 % (1054722)------------------------------ % 179.59/25.54 % (1054722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.59/25.54 % (1054722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.59/25.54 % (1054722)CaDiCaL version: 2.1.3 % 179.59/25.54 % (1054722)Termination reason: Instruction limit % 179.59/25.54 % (1054722)Termination phase: Saturation % 179.59/25.54 % (1054722)Time elapsed: 3.213 s % 179.59/25.54 % (1054722)Peak memory usage: 30 MB % 179.59/25.54 % (1054722)Instructions burned: 3773 (million) % 179.59/25.54 % (1054851)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3143319762:i=5497:nm=2_2955 on theBenchmark for (2955ds/5497Mi) % 179.59/25.54 % (1054851)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.59/25.54 % (1054851)Terminated due to inappropriate strategy. % 179.59/25.54 % (1054851)------------------------------ % 179.59/25.54 % (1054851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.59/25.54 % (1054851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.59/25.54 % (1054851)CaDiCaL version: 2.1.3 % 179.59/25.54 % (1054851)Termination reason: Inappropriate % 179.59/25.54 % (1054851)Time elapsed: 0.001 s % 179.59/25.54 % (1054851)Peak memory usage: 11 MB % 179.59/25.54 % (1054851)Instructions burned: 1 (million) % 179.59/25.54 % (1054851)------------------------------ % 179.59/25.54 % (1054851)------------------------------ % 179.59/25.54 % (1054770)Instruction limit reached! % 179.59/25.54 % (1054770)------------------------------ % 179.59/25.54 % (1054770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.59/25.54 % (1054770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.59/25.54 % (1054770)CaDiCaL version: 2.1.3 % 179.59/25.54 % (1054770)Termination reason: Instruction limit % 179.59/25.54 % (1054770)Termination phase: Saturation % 179.59/25.54 % (1054770)Time elapsed: 2.279 s % 179.59/25.54 % (1054770)Peak memory usage: 42 MB % 179.59/25.54 % (1054770)Instructions burned: 4592 (million) % 179.59/25.54 % (1054853)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2859737823:fmbsr=2:i=46332_2955 on theBenchmark for (2955ds/46332Mi) % 179.59/25.54 % (1054853)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.59/25.54 % (1054853)Terminated due to inappropriate strategy. % 179.59/25.54 % (1054853)------------------------------ % 179.59/25.54 % (1054853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.59/25.54 % (1054853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.59/25.54 % (1054853)CaDiCaL version: 2.1.3 % 179.59/25.54 % (1054853)Termination reason: Inappropriate % 179.59/25.54 % (1054853)Time elapsed: 0.001 s % 179.59/25.54 % (1054853)Peak memory usage: 11 MB % 179.59/25.54 % (1054853)Instructions burned: 1 (million) % 179.59/25.54 % (1054853)------------------------------ % 179.59/25.54 % (1054853)------------------------------ % 179.59/25.54 % (1054854)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3952848676:i=14071_2955 on theBenchmark for (2955ds/14071Mi) % 179.59/25.54 % (1054854)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.59/25.54 % (1054854)Terminated due to inappropriate strategy. % 179.59/25.54 % (1054854)------------------------------ % 179.59/25.54 % (1054854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.59/25.54 % (1054854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.59/25.54 % (1054854)CaDiCaL version: 2.1.3 % 179.59/25.54 % (1054854)Termination reason: Inappropriate % 179.59/25.54 % (1054854)Time elapsed: 0.002 s % 179.59/25.54 % (1054854)Peak memory usage: 10 MB % 179.59/25.54 % (1054854)Instructions burned: 1 (million) % 179.59/25.54 % (1054854)------------------------------ % 179.59/25.54 % (1054854)------------------------------ % 179.59/25.54 % (1054858)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3529392859:i=22565:add=on:rawr=on_2955 on theBenchmark for (2955ds/22565Mi) % 179.59/25.54 % (1054860)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1860069277:i=8173:av=off_2955 on theBenchmark for (2955ds/8173Mi) % 179.59/25.54 % (1054716)Instruction limit reached! % 180.28/25.70 % (1054716)------------------------------ % 180.28/25.70 % (1054716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.28/25.70 % (1054716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.28/25.70 % (1054716)CaDiCaL version: 2.1.3 % 180.28/25.70 % (1054716)Termination reason: Instruction limit % 180.28/25.70 % (1054716)Termination phase: Saturation % 180.28/25.70 % (1054716)Time elapsed: 4.733 s % 180.28/25.70 % (1054716)Peak memory usage: 42 MB % 180.28/25.70 % (1054716)Instructions burned: 5114 (million) % 180.28/25.70 % (1054891)dis+10_16:1_sil=16000:random_seed=3416928707:i=9155:fsr=off_2944 on theBenchmark for (2944ds/9155Mi) % 180.28/25.70 % (1054836)Instruction limit reached! % 180.28/25.70 % (1054836)------------------------------ % 180.28/25.70 % (1054836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.28/25.70 % (1054836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.28/25.70 % (1054836)CaDiCaL version: 2.1.3 % 180.28/25.70 % (1054836)Termination reason: Instruction limit % 180.28/25.70 % (1054836)Termination phase: Saturation % 180.28/25.70 % (1054836)Time elapsed: 2.821 s % 180.28/25.70 % (1054836)Peak memory usage: 48 MB % 180.28/25.70 % (1054836)Instructions burned: 5211 (million) % 180.28/25.70 % (1054918)ott-3_8_sil=64000:random_seed=2500062605:i=20139:bs=on_2932 on theBenchmark for (2932ds/20139Mi) % 180.28/25.70 % (1054860)Instruction limit reached! % 180.28/25.70 % (1054860)------------------------------ % 180.28/25.70 % (1054860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.28/25.70 % (1054860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.28/25.70 % (1054860)CaDiCaL version: 2.1.3 % 180.28/25.70 % (1054860)Termination reason: Instruction limit % 180.28/25.70 % (1054860)Termination phase: Saturation % 180.28/25.70 % (1054860)Time elapsed: 8.165 s % 180.28/25.70 % (1054860)Peak memory usage: 51 MB % 180.28/25.70 % (1054860)Instructions burned: 8173 (million) % 180.28/25.70 % (1054984)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1997196101:fmbsr=2:i=32576_2872 on theBenchmark for (2872ds/32576Mi) % 180.28/25.70 % (1054984)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.28/25.70 % (1054984)Terminated due to inappropriate strategy. % 180.28/25.70 % (1054984)------------------------------ % 180.28/25.70 % (1054984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.28/25.70 % (1054984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.28/25.70 % (1054984)CaDiCaL version: 2.1.3 % 180.28/25.70 % (1054984)Termination reason: Inappropriate % 180.28/25.70 % (1054984)Time elapsed: 0.001 s % 180.28/25.70 % (1054984)Peak memory usage: 10 MB % 180.28/25.70 % (1054984)Instructions burned: 1 (million) % 180.28/25.70 % (1054984)------------------------------ % 180.28/25.70 % (1054984)------------------------------ % 180.28/25.70 % (1054986)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3789898686:i=11404_2872 on theBenchmark for (2872ds/11404Mi) % 180.28/25.70 % (1054891)Instruction limit reached! % 180.28/25.70 % (1054891)------------------------------ % 180.28/25.70 % (1054891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.28/25.70 % (1054891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.28/25.70 % (1054891)CaDiCaL version: 2.1.3 % 180.28/25.70 % (1054891)Termination reason: Instruction limit % 180.28/25.70 % (1054891)Termination phase: Saturation % 180.28/25.70 % (1054891)Time elapsed: 7.954 s % 180.28/25.70 % (1054891)Peak memory usage: 51 MB % 180.28/25.70 % (1054891)Instructions burned: 9156 (million) % 180.28/25.70 % (1054992)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3663428515:i=14134_2864 on theBenchmark for (2864ds/14134Mi) % 180.28/25.70 % (1054918)Instruction limit reached! % 180.28/25.70 % (1054918)------------------------------ % 180.28/25.70 % (1054918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.28/25.70 % (1054918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.28/25.70 % (1054918)CaDiCaL version: 2.1.3 % 180.28/25.70 % (1054918)Termination reason: Instruction limit % 180.28/25.70 % (1054918)Termination phase: Saturation % 180.28/25.70 % (1054918)Time elapsed: 10.176 s % 180.28/25.70 % (1054918)Peak memory usage: 56 MB % 180.28/25.70 % (1054918)Instructions burned: 20139 (million) % 180.28/25.70 % (1055002)dis+33_16_sil=32000:sac=on:random_seed=3169249465:i=15851:nm=0_2830 on theBenchmark for (2830ds/15851Mi) % 180.28/25.70 % (1054858)Instruction limit reached! % 180.28/25.70 % (1054858)------------------------------ % 180.28/25.70 % (1054858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.67/36.50 % (1054858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.67/36.50 % (1054858)CaDiCaL version: 2.1.3 % 256.67/36.50 % (1054858)Termination reason: Instruction limit % 256.67/36.50 % (1054858)Termination phase: Saturation % 256.67/36.50 % (1054858)Time elapsed: 16.291 s % 256.67/36.50 % (1054858)Peak memory usage: 73 MB % 256.67/36.50 % (1054858)Instructions burned: 22565 (million) % 256.67/36.50 % (1055024)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2565474609:avsq=on:i=17627:add=on:amm=off_2791 on theBenchmark for (2791ds/17627Mi) % 256.67/36.50 % (1054986)Instruction limit reached! % 256.67/36.50 % (1054986)------------------------------ % 256.67/36.50 % (1054986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.67/36.50 % (1054986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.67/36.50 % (1054986)CaDiCaL version: 2.1.3 % 256.67/36.50 % (1054986)Termination reason: Instruction limit % 256.67/36.50 % (1054986)Termination phase: Saturation % 256.67/36.50 % (1054986)Time elapsed: 11.209 s % 256.67/36.50 % (1054986)Peak memory usage: 71 MB % 256.67/36.50 % (1054986)Instructions burned: 11404 (million) % 256.67/36.50 % (1055036)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3807789490:s2a=on:i=53295_2760 on theBenchmark for (2760ds/53295Mi) % 256.67/36.50 % (1055002)Instruction limit reached! % 256.67/36.50 % (1055002)------------------------------ % 256.67/36.50 % (1055002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.67/36.50 % (1055002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.67/36.50 % (1055002)CaDiCaL version: 2.1.3 % 256.67/36.50 % (1055002)Termination reason: Instruction limit % 256.67/36.50 % (1055002)Termination phase: Saturation % 256.67/36.50 % (1055002)Time elapsed: 7.308 s % 256.67/36.50 % (1055002)Peak memory usage: 204 MB % 256.67/36.50 % (1055002)Instructions burned: 15852 (million) % 256.67/36.50 % (1055040)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=915542866:i=26857:ins=20_2756 on theBenchmark for (2756ds/26857Mi) % 256.67/36.50 % (1055040)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 256.67/36.50 % (1055040)Terminated due to inappropriate strategy. % 256.67/36.50 % (1055040)------------------------------ % 256.67/36.50 % (1055040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.67/36.50 % (1055040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.67/36.50 % (1055040)CaDiCaL version: 2.1.3 % 256.67/36.50 % (1055040)Termination reason: Inappropriate % 256.67/36.50 % (1055040)Time elapsed: 0.001 s % 256.67/36.50 % (1055040)Peak memory usage: 10 MB % 256.67/36.50 % (1055040)Instructions burned: 1 (million) % 256.67/36.50 % (1055040)------------------------------ % 256.67/36.50 % (1055040)------------------------------ % 256.67/36.50 % (1055042)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=858663896:i=28120:bs=on:fsr=off_2756 on theBenchmark for (2756ds/28120Mi) % 256.67/36.50 % (1054815)Instruction limit reached! % 256.67/36.50 % (1054815)------------------------------ % 256.67/36.50 % (1054815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.67/36.50 % (1054815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.67/36.50 % (1054815)CaDiCaL version: 2.1.3 % 256.67/36.50 % (1054815)Termination reason: Instruction limit % 256.67/36.50 % (1054815)Termination phase: Saturation % 256.67/36.50 % (1054815)Time elapsed: 21.902 s % 256.67/36.50 % (1054815)Peak memory usage: 171 MB % 256.67/36.50 % (1054815)Instructions burned: 29342 (million) % 256.67/36.50 % (1055049)fmb+10_1_sil=256000:fmbss=7:random_seed=1423307886:fmbsr=1.6:i=182295_2747 on theBenchmark for (2747ds/182295Mi) % 256.67/36.50 % (1055049)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 256.67/36.50 % (1055049)Terminated due to inappropriate strategy. % 256.67/36.50 % (1055049)------------------------------ % 256.67/36.50 % (1055049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.67/36.50 % (1055049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.67/36.50 % (1055049)CaDiCaL version: 2.1.3 % 256.67/36.50 % (1055049)Termination reason: Inappropriate % 256.67/36.50 % (1055049)Time elapsed: 0.001 s % 256.67/36.50 % (1055049)Peak memory usage: 11 MB % 256.67/36.50 % (1055049)Instructions burned: 1 (million) % 256.67/36.50 % (1055049)------------------------------ % 256.67/36.50 % (1055049)------------------------------ % 256.67/36.50 % (1055051)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1608132631:i=44625:gsp=on_2747 on theBenchmark for (2747ds/44625Mi) % 263.90/37.41 % (1055051)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 263.90/37.41 % (1055051)Terminated due to inappropriate strategy. % 263.90/37.41 % (1055051)------------------------------ % 263.90/37.41 % (1055051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.90/37.41 % (1055051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.90/37.41 % (1055051)CaDiCaL version: 2.1.3 % 263.90/37.41 % (1055051)Termination reason: Inappropriate % 263.90/37.41 % (1055051)Time elapsed: 0.001 s % 263.90/37.41 % (1055051)Peak memory usage: 11 MB % 263.90/37.41 % (1055051)Instructions burned: 1 (million) % 263.90/37.41 % (1055051)------------------------------ % 263.90/37.41 % (1055051)------------------------------ % 263.90/37.41 % (1055053)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1782676948:i=160505_2746 on theBenchmark for (2746ds/160505Mi) % 263.90/37.41 % (1055053)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 263.90/37.41 % (1055053)Terminated due to inappropriate strategy. % 263.90/37.41 % (1055053)------------------------------ % 263.90/37.41 % (1055053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.90/37.41 % (1055053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.90/37.41 % (1055053)CaDiCaL version: 2.1.3 % 263.90/37.41 % (1055053)Termination reason: Inappropriate % 263.90/37.41 % (1055053)Time elapsed: 0.001 s % 263.90/37.41 % (1055053)Peak memory usage: 11 MB % 263.90/37.41 % (1055053)Instructions burned: 1 (million) % 263.90/37.41 % (1055053)------------------------------ % 263.90/37.41 % (1055053)------------------------------ % 263.90/37.41 % (1055055)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2206582571:fmbsr=1.3:i=225729_2746 on theBenchmark for (2746ds/225729Mi) % 263.90/37.41 % (1055055)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 263.90/37.41 % (1055055)Terminated due to inappropriate strategy. % 263.90/37.41 % (1055055)------------------------------ % 263.90/37.41 % (1055055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.90/37.41 % (1055055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.90/37.41 % (1055055)CaDiCaL version: 2.1.3 % 263.90/37.41 % (1055055)Termination reason: Inappropriate % 263.90/37.41 % (1055055)Time elapsed: 0.002 s % 263.90/37.41 % (1055055)Peak memory usage: 11 MB % 263.90/37.41 % (1055055)Instructions burned: 1 (million) % 263.90/37.41 % (1055055)------------------------------ % 263.90/37.41 % (1055055)------------------------------ % 263.90/37.41 % (1055058)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2065551531:fmbsr=2:i=185024:ins=7_2746 on theBenchmark for (2746ds/185024Mi) % 263.90/37.41 % (1055058)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 263.90/37.41 % (1055058)Terminated due to inappropriate strategy. % 263.90/37.41 % (1055058)------------------------------ % 263.90/37.41 % (1055058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.90/37.41 % (1055058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.90/37.41 % (1055058)CaDiCaL version: 2.1.3 % 263.90/37.41 % (1055058)Termination reason: Inappropriate % 263.90/37.41 % (1055058)Time elapsed: 0.001 s % 263.90/37.41 % (1055058)Peak memory usage: 10 MB % 263.90/37.41 % (1055058)Instructions burned: 1 (million) % 263.90/37.41 % (1055058)------------------------------ % 263.90/37.41 % (1055058)------------------------------ % 263.90/37.41 % (1055060)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2774914763:rtra=on_2745 on theBenchmark for (2745ds/0Mi) % 263.90/37.41 % (1055060)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 263.90/37.41 % (1055060)Terminated due to inappropriate strategy. % 263.90/37.41 % (1055060)------------------------------ % 263.90/37.41 % (1055060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 263.90/37.41 % (1055060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.90/37.41 % (1055060)CaDiCaL version: 2.1.3 % 263.90/37.41 % (1055060)Termination reason: Inappropriate % 263.90/37.41 % (1055060)Time elapsed: 0.001 s % 263.90/37.41 % (1055060)Peak memory usage: 10 MB % 263.90/37.41 % (1055060)Instructions burned: 1 (million) % 263.90/37.41 % (1055060)------------------------------ % 263.90/37.41 % (1055060)------------------------------ % 263.90/37.41 % (1055062)% WARNING: option uhcvi not known. % 263.90/37.41 % (1055062)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1256568298:i=271062:add=off:rtra=on:rawr=on_2745 on theBenchmark for (2745ds/271062Mi) % 279.80/39.61 % (1054992)Instruction limit reached! % 279.80/39.61 % (1054992)------------------------------ % 279.80/39.61 % (1054992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.80/39.61 % (1054992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.80/39.61 % (1054992)CaDiCaL version: 2.1.3 % 279.80/39.61 % (1054992)Termination reason: Instruction limit % 279.80/39.61 % (1054992)Termination phase: Saturation % 279.80/39.61 % (1054992)Time elapsed: 13.668 s % 279.80/39.61 % (1054992)Peak memory usage: 72 MB % 279.80/39.61 % (1054992)Instructions burned: 14134 (million) % 279.80/39.61 % (1055064)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2770378798:i=176048:add=on:rtra=on:rawr=on_2727 on theBenchmark for (2727ds/176048Mi) % 279.80/39.61 % (1055024)Instruction limit reached! % 279.80/39.61 % (1055024)------------------------------ % 279.80/39.61 % (1055024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.80/39.61 % (1055024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.80/39.61 % (1055024)CaDiCaL version: 2.1.3 % 279.80/39.61 % (1055024)Termination reason: Instruction limit % 279.80/39.61 % (1055024)Termination phase: Saturation % 279.80/39.61 % (1055024)Time elapsed: 14.776 s % 279.80/39.61 % (1055024)Peak memory usage: 234 MB % 279.80/39.61 % (1055024)Instructions burned: 17628 (million) % 279.80/39.61 % (1055179)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2819059533:i=206:fgj=on:rtra=on_2643 on theBenchmark for (2643ds/206Mi) % 279.80/39.61 % (1055179)Instruction limit reached! % 279.80/39.61 % (1055179)------------------------------ % 279.80/39.61 % (1055179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.80/39.61 % (1055179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.80/39.61 % (1055179)CaDiCaL version: 2.1.3 % 279.80/39.61 % (1055179)Termination reason: Instruction limit % 279.80/39.61 % (1055179)Termination phase: Saturation % 279.80/39.61 % (1055179)Time elapsed: 0.204 s % 279.80/39.61 % (1055179)Peak memory usage: 13 MB % 279.80/39.61 % (1055179)Instructions burned: 207 (million) % 279.80/39.61 % (1055042)Instruction limit reached! % 279.80/39.61 % (1055042)------------------------------ % 279.80/39.61 % (1055042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.80/39.61 % (1055042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.80/39.61 % (1055042)CaDiCaL version: 2.1.3 % 279.80/39.61 % (1055042)Termination reason: Instruction limit % 279.80/39.61 % (1055042)Termination phase: Saturation % 279.80/39.61 % (1055042)Time elapsed: 11.539 s % 279.80/39.61 % (1055042)Peak memory usage: 25 MB % 279.80/39.61 % (1055042)Instructions burned: 28120 (million) % 279.80/39.61 % (1055186)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4196533913:i=232:rtra=on_2640 on theBenchmark for (2640ds/232Mi) % 279.80/39.61 % (1055188)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1101108068:i=262:rtra=on_2640 on theBenchmark for (2640ds/262Mi) % 279.80/39.61 % (1055186)Instruction limit reached! % 279.80/39.61 % (1055186)------------------------------ % 279.80/39.61 % (1055186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.80/39.61 % (1055186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.80/39.61 % (1055186)CaDiCaL version: 2.1.3 % 279.80/39.61 % (1055186)Termination reason: Instruction limit % 279.80/39.61 % (1055186)Termination phase: Saturation % 279.80/39.61 % (1055186)Time elapsed: 0.247 s % 279.80/39.61 % (1055186)Peak memory usage: 13 MB % 279.80/39.61 % (1055186)Instructions burned: 232 (million) % 279.80/39.61 % (1055188)Instruction limit reached! % 279.80/39.61 % (1055188)------------------------------ % 279.80/39.61 % (1055188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.80/39.61 % (1055188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.80/39.61 % (1055188)CaDiCaL version: 2.1.3 % 279.80/39.61 % (1055188)Termination reason: Instruction limit % 279.80/39.61 % (1055188)Termination phase: Saturation % 279.80/39.61 % (1055188)Time elapsed: 0.207 s % 279.80/39.61 % (1055188)Peak memory usage: 13 MB % 279.80/39.61 % (1055188)Instructions burned: 263 (million) % 279.80/39.61 % (1055192)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=635781464:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2637 on theBenchmark for (2637ds/318Mi) % 279.80/39.61 % (1055193)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3114737596:i=1428:nm=2:rtra=on_2637 on theBenchmark for (2637ds/1428Mi) % 291.17/41.30 % (1055193)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 291.17/41.30 % (1055193)Terminated due to inappropriate strategy. % 291.17/41.30 % (1055193)------------------------------ % 291.17/41.30 % (1055193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.17/41.30 % (1055193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.17/41.30 % (1055193)CaDiCaL version: 2.1.3 % 291.17/41.30 % (1055193)Termination reason: Inappropriate % 291.17/41.30 % (1055193)Time elapsed: 0.001 s % 291.17/41.30 % (1055193)Peak memory usage: 11 MB % 291.17/41.30 % (1055193)Instructions burned: 1 (million) % 291.17/41.30 % (1055193)------------------------------ % 291.17/41.30 % (1055193)------------------------------ % 291.17/41.30 % (1055197)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1646756205:i=262:bd=preordered:rtra=on:fsd=on_2637 on theBenchmark for (2637ds/262Mi) % 291.17/41.30 % (1055197)Instruction limit reached! % 291.17/41.30 % (1055197)------------------------------ % 291.17/41.30 % (1055197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.17/41.30 % (1055197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.17/41.30 % (1055197)CaDiCaL version: 2.1.3 % 291.17/41.30 % (1055197)Termination reason: Instruction limit % 291.17/41.30 % (1055197)Termination phase: Saturation % 291.17/41.30 % (1055197)Time elapsed: 0.160 s % 291.17/41.30 % (1055197)Peak memory usage: 14 MB % 291.17/41.30 % (1055197)Instructions burned: 262 (million) % 291.17/41.30 % (1055200)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=387643094:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2635 on theBenchmark for (2635ds/1368Mi) % 291.17/41.30 % (1055192)Instruction limit reached! % 291.17/41.30 % (1055192)------------------------------ % 291.17/41.30 % (1055192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.17/41.30 % (1055192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.17/41.30 % (1055192)CaDiCaL version: 2.1.3 % 291.17/41.30 % (1055192)Termination reason: Instruction limit % 291.17/41.30 % (1055192)Termination phase: Saturation % 291.17/41.30 % (1055192)Time elapsed: 0.309 s % 291.17/41.30 % (1055192)Peak memory usage: 14 MB % 291.17/41.30 % (1055192)Instructions burned: 318 (million) % 291.17/41.30 % (1055203)ott-21_1_sil=16000:si=on:fs=off:random_seed=4171744920:i=360:av=off:fsr=off:rtra=on_2634 on theBenchmark for (2634ds/360Mi) % 291.17/41.30 % (1055203)Instruction limit reached! % 291.17/41.30 % (1055203)------------------------------ % 291.17/41.30 % (1055203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.17/41.30 % (1055203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.17/41.30 % (1055203)CaDiCaL version: 2.1.3 % 291.17/41.30 % (1055203)Termination reason: Instruction limit % 291.17/41.30 % (1055203)Termination phase: Saturation % 291.17/41.30 % (1055203)Time elapsed: 0.279 s % 291.17/41.30 % (1055203)Peak memory usage: 13 MB % 291.17/41.30 % (1055203)Instructions burned: 360 (million) % 291.17/41.30 % (1055211)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3654653223:i=954:bd=all:rtra=on_2631 on theBenchmark for (2631ds/954Mi) % 291.17/41.30 % (1055200)Instruction limit reached! % 291.17/41.30 % (1055200)------------------------------ % 291.17/41.30 % (1055200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.17/41.30 % (1055200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.17/41.30 % (1055200)CaDiCaL version: 2.1.3 % 291.17/41.30 % (1055200)Termination reason: Instruction limit % 291.17/41.30 % (1055200)Termination phase: Saturation % 291.17/41.30 % (1055200)Time elapsed: 0.665 s % 291.17/41.30 % (1055200)Peak memory usage: 22 MB % 291.17/41.30 % (1055200)Instructions burned: 1370 (million) % 291.17/41.30 % (1055215)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=597875809:fmbsr=1.3:i=1730:ins=25:rtra=on_2628 on theBenchmark for (2628ds/1730Mi) % 291.17/41.30 % (1055215)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 291.17/41.30 % (1055215)Terminated due to inappropriate strategy. % 291.17/41.30 % (1055215)------------------------------ % 291.17/41.30 % (1055215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.17/41.30 % (1055215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.17/41.30 % (1055215)CaDiCaL version: 2.1.3 % 291.17/41.30 % (1055215)Termination reason: InappropTerminated % 300.19/42.53 % Vampire exiting % 300.19/42.54 Terminated %------------------------------------------------------------------------------