%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX150_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n026.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:46:33 PM UTC 2026 % Result : Timeout 299.46s 42.42s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX150_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n026.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 15:07:27 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.58/0.81 % (3920421)Will run a generic schedule for satisfiability detection. % 3.58/0.81 % (3920427)% WARNING: option uhcvi not known. % 3.58/0.81 % (3920427)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1136930714:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.58/0.81 % (3920426)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3889292785_2999 on theBenchmark for (2999ds/0Mi) % 3.58/0.81 % (3920428)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1072096428:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.58/0.81 % (3920429)dis+10_1_sil=32000:sp=arity:random_seed=557390821:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.58/0.81 % (3920430)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2024176185:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.58/0.81 % (3920431)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2336216844:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.58/0.81 % (3920432)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2364477213:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.58/0.81 % (3920426)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.58/0.81 % (3920426)Terminated due to inappropriate strategy. % 3.58/0.81 % (3920426)------------------------------ % 3.58/0.81 % (3920426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.58/0.81 % (3920426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.58/0.81 % (3920426)CaDiCaL version: 2.1.3 % 3.58/0.81 % (3920426)Termination reason: Inappropriate % 3.58/0.81 % (3920426)Time elapsed: 0.035 s % 3.58/0.81 % (3920426)Peak memory usage: 11 MB % 3.58/0.81 % (3920426)Instructions burned: 60 (million) % 3.58/0.81 % (3920426)------------------------------ % 3.58/0.81 % (3920426)------------------------------ % 3.58/0.81 % (3920429)Instruction limit reached! % 3.58/0.81 % (3920429)------------------------------ % 3.58/0.81 % (3920429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.58/0.81 % (3920429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.58/0.81 % (3920429)CaDiCaL version: 2.1.3 % 3.58/0.81 % (3920429)Termination reason: Instruction limit % 3.58/0.81 % (3920429)Termination phase: Saturation % 3.58/0.81 % (3920429)Time elapsed: 0.044 s % 3.58/0.81 % (3920429)Peak memory usage: 12 MB % 3.58/0.81 % (3920429)Instructions burned: 103 (million) % 3.58/0.81 % (3920430)Instruction limit reached! % 3.58/0.81 % (3920430)------------------------------ % 3.58/0.81 % (3920430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.58/0.81 % (3920430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.58/0.81 % (3920430)CaDiCaL version: 2.1.3 % 3.58/0.81 % (3920430)Termination reason: Instruction limit % 3.58/0.81 % (3920430)Termination phase: Saturation % 3.58/0.81 % (3920430)Time elapsed: 0.050 s % 3.58/0.81 % (3920430)Peak memory usage: 13 MB % 3.58/0.81 % (3920430)Instructions burned: 116 (million) % 3.58/0.81 % (3920431)Instruction limit reached! % 3.58/0.81 % (3920431)------------------------------ % 3.58/0.81 % (3920431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.58/0.81 % (3920431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.58/0.81 % (3920431)CaDiCaL version: 2.1.3 % 3.58/0.81 % (3920431)Termination reason: Instruction limit % 3.58/0.81 % (3920431)Termination phase: Saturation % 3.58/0.81 % (3920431)Time elapsed: 0.060 s % 3.58/0.81 % (3920431)Peak memory usage: 14 MB % 3.58/0.81 % (3920431)Instructions burned: 131 (million) % 3.58/0.81 % (3920440)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1098014434:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 3.58/0.81 % (3920441)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2453263914:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.58/0.81 % (3920442)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=2430499169:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 3.58/0.81 % (3920443)ott-21_1_sil=16000:fs=off:random_seed=2716896788:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 3.58/0.81 % (3920440)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.58/0.81 % (3920440)Terminated due to inappropriate strategy. % 4.06/0.99 % (3920440)------------------------------ % 4.06/0.99 % (3920440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.06/0.99 % (3920440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/0.99 % (3920440)CaDiCaL version: 2.1.3 % 4.06/0.99 % (3920440)Termination reason: Inappropriate % 4.06/0.99 % (3920440)Time elapsed: 0.025 s % 4.06/0.99 % (3920440)Peak memory usage: 11 MB % 4.06/0.99 % (3920440)Instructions burned: 60 (million) % 4.06/0.99 % (3920440)------------------------------ % 4.06/0.99 % (3920440)------------------------------ % 4.06/0.99 % (3920448)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1024328413:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 4.06/0.99 % (3920432)Instruction limit reached! % 4.06/0.99 % (3920432)------------------------------ % 4.06/0.99 % (3920432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.06/0.99 % (3920432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/0.99 % (3920432)CaDiCaL version: 2.1.3 % 4.06/0.99 % (3920432)Termination reason: Instruction limit % 4.06/0.99 % (3920432)Termination phase: Saturation % 4.06/0.99 % (3920432)Time elapsed: 0.111 s % 4.06/0.99 % (3920432)Peak memory usage: 14 MB % 4.06/0.99 % (3920432)Instructions burned: 159 (million) % 4.06/0.99 % (3920441)Instruction limit reached! % 4.06/0.99 % (3920441)------------------------------ % 4.06/0.99 % (3920441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.06/0.99 % (3920441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/0.99 % (3920441)CaDiCaL version: 2.1.3 % 4.06/0.99 % (3920441)Termination reason: Instruction limit % 4.06/0.99 % (3920441)Termination phase: Saturation % 4.06/0.99 % (3920441)Time elapsed: 0.056 s % 4.06/0.99 % (3920441)Peak memory usage: 14 MB % 4.06/0.99 % (3920441)Instructions burned: 131 (million) % 4.06/0.99 % (3920452)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4253174437:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.06/0.99 % (3920456)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=874317381:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 4.06/0.99 % (3920452)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.06/0.99 % (3920452)Terminated due to inappropriate strategy. % 4.06/0.99 % (3920452)------------------------------ % 4.06/0.99 % (3920452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.06/0.99 % (3920452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/0.99 % (3920452)CaDiCaL version: 2.1.3 % 4.06/0.99 % (3920452)Termination reason: Inappropriate % 4.06/0.99 % (3920452)Time elapsed: 0.019 s % 4.06/0.99 % (3920452)Peak memory usage: 11 MB % 4.06/0.99 % (3920452)Instructions burned: 45 (million) % 4.06/0.99 % (3920452)------------------------------ % 4.06/0.99 % (3920452)------------------------------ % 4.06/0.99 % (3920443)Instruction limit reached! % 4.06/0.99 % (3920443)------------------------------ % 4.06/0.99 % (3920443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.06/0.99 % (3920443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/0.99 % (3920443)CaDiCaL version: 2.1.3 % 4.06/0.99 % (3920443)Termination reason: Instruction limit % 4.06/0.99 % (3920443)Termination phase: Saturation % 4.06/0.99 % (3920443)Time elapsed: 0.082 s % 4.06/0.99 % (3920443)Peak memory usage: 13 MB % 4.06/0.99 % (3920443)Instructions burned: 181 (million) % 4.06/0.99 % (3920466)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2852492364:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 4.06/0.99 % (3920469)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=3500177283: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) % 4.06/0.99 % (3920466)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.06/0.99 % (3920466)Terminated due to inappropriate strategy. % 4.06/0.99 % (3920466)------------------------------ % 4.06/0.99 % (3920466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.06/0.99 % (3920466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.06/0.99 % (3920466)CaDiCaL version: 2.1.3 % 4.06/0.99 % (3920466)Termination reason: Inappropriate % 4.06/0.99 % (3920466)Time elapsed: 0.019 s % 4.06/0.99 % (3920466)Peak memory usage: 11 MB % 26.75/4.11 % (3920466)Instructions burned: 45 (million) % 26.75/4.11 % (3920466)------------------------------ % 26.75/4.11 % (3920466)------------------------------ % 26.75/4.11 % (3920479)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=803279611:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 26.75/4.11 % (3920448)Instruction limit reached! % 26.75/4.11 % (3920448)------------------------------ % 26.75/4.11 % (3920448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.75/4.11 % (3920448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.75/4.11 % (3920448)CaDiCaL version: 2.1.3 % 26.75/4.11 % (3920448)Termination reason: Instruction limit % 26.75/4.11 % (3920448)Termination phase: Saturation % 26.75/4.11 % (3920448)Time elapsed: 0.194 s % 26.75/4.11 % (3920448)Peak memory usage: 14 MB % 26.75/4.11 % (3920448)Instructions burned: 480 (million) % 26.75/4.11 % (3920520)fmb+10_1_sil=64000:random_seed=3695488121:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 26.75/4.11 % (3920442)Instruction limit reached! % 26.75/4.11 % (3920442)------------------------------ % 26.75/4.11 % (3920442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.75/4.11 % (3920442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.75/4.11 % (3920442)CaDiCaL version: 2.1.3 % 26.75/4.11 % (3920442)Termination reason: Instruction limit % 26.75/4.11 % (3920442)Termination phase: Saturation % 26.75/4.11 % (3920442)Time elapsed: 0.282 s % 26.75/4.11 % (3920442)Peak memory usage: 16 MB % 26.75/4.11 % (3920442)Instructions burned: 684 (million) % 26.75/4.11 % (3920520)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.75/4.11 % (3920520)Terminated due to inappropriate strategy. % 26.75/4.11 % (3920520)------------------------------ % 26.75/4.11 % (3920520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.75/4.11 % (3920520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.75/4.11 % (3920520)CaDiCaL version: 2.1.3 % 26.75/4.11 % (3920520)Termination reason: Inappropriate % 26.75/4.11 % (3920520)Time elapsed: 0.035 s % 26.75/4.11 % (3920520)Peak memory usage: 11 MB % 26.75/4.11 % (3920520)Instructions burned: 60 (million) % 26.75/4.11 % (3920520)------------------------------ % 26.75/4.11 % (3920520)------------------------------ % 26.75/4.11 % (3920531)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=942062676:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 26.75/4.11 % (3920535)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1276520357:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 26.75/4.11 % (3920531)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.75/4.11 % (3920531)Terminated due to inappropriate strategy. % 26.75/4.11 % (3920531)------------------------------ % 26.75/4.11 % (3920531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.75/4.11 % (3920531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.75/4.11 % (3920531)CaDiCaL version: 2.1.3 % 26.75/4.11 % (3920531)Termination reason: Inappropriate % 26.75/4.11 % (3920531)Time elapsed: 0.026 s % 26.75/4.11 % (3920531)Peak memory usage: 11 MB % 26.75/4.11 % (3920531)Instructions burned: 60 (million) % 26.75/4.11 % (3920531)------------------------------ % 26.75/4.11 % (3920531)------------------------------ % 26.75/4.11 % (3920535)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.75/4.11 % (3920535)Terminated due to inappropriate strategy. % 26.75/4.11 % (3920535)------------------------------ % 26.75/4.11 % (3920535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.75/4.11 % (3920535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.75/4.11 % (3920535)CaDiCaL version: 2.1.3 % 26.75/4.11 % (3920535)Termination reason: Inappropriate % 26.75/4.11 % (3920535)Time elapsed: 0.026 s % 26.75/4.11 % (3920535)Peak memory usage: 11 MB % 26.75/4.11 % (3920535)Instructions burned: 60 (million) % 26.75/4.11 % (3920535)------------------------------ % 26.75/4.11 % (3920535)------------------------------ % 26.75/4.11 % (3920549)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2200178831:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 26.75/4.11 % (3920550)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=335272052:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 26.75/4.11 % (3920469)Instruction limit reached! % 26.75/4.11 % (3920469)------------------------------ % 29.49/4.56 % (3920469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.49/4.56 % (3920469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.49/4.56 % (3920469)CaDiCaL version: 2.1.3 % 29.49/4.56 % (3920469)Termination reason: Instruction limit % 29.49/4.56 % (3920469)Termination phase: Saturation % 29.49/4.56 % (3920469)Time elapsed: 0.317 s % 29.49/4.56 % (3920469)Peak memory usage: 18 MB % 29.49/4.56 % (3920469)Instructions burned: 692 (million) % 29.49/4.56 % (3920575)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2825029793:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 29.49/4.56 % (3920575)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.49/4.56 % (3920575)Terminated due to inappropriate strategy. % 29.49/4.56 % (3920575)------------------------------ % 29.49/4.56 % (3920575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.49/4.56 % (3920575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.49/4.56 % (3920575)CaDiCaL version: 2.1.3 % 29.49/4.56 % (3920575)Termination reason: Inappropriate % 29.49/4.56 % (3920575)Time elapsed: 0.026 s % 29.49/4.56 % (3920575)Peak memory usage: 11 MB % 29.49/4.56 % (3920575)Instructions burned: 60 (million) % 29.49/4.56 % (3920575)------------------------------ % 29.49/4.56 % (3920575)------------------------------ % 29.49/4.56 % (3920479)Instruction limit reached! % 29.49/4.56 % (3920479)------------------------------ % 29.49/4.56 % (3920479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.49/4.56 % (3920479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.49/4.56 % (3920479)CaDiCaL version: 2.1.3 % 29.49/4.56 % (3920479)Termination reason: Instruction limit % 29.49/4.56 % (3920479)Termination phase: Saturation % 29.49/4.56 % (3920479)Time elapsed: 0.355 s % 29.49/4.56 % (3920479)Peak memory usage: 15 MB % 29.49/4.56 % (3920479)Instructions burned: 880 (million) % 29.49/4.56 % (3920587)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1521066603:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 29.49/4.56 % (3920592)ott-2_1_sil=16000:newcnf=on:random_seed=2582647162:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 29.49/4.56 % (3920587)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.49/4.56 % (3920587)Terminated due to inappropriate strategy. % 29.49/4.56 % (3920587)------------------------------ % 29.49/4.56 % (3920587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.49/4.56 % (3920587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.49/4.56 % (3920587)CaDiCaL version: 2.1.3 % 29.49/4.56 % (3920587)Termination reason: Inappropriate % 29.49/4.56 % (3920587)Time elapsed: 0.028 s % 29.49/4.56 % (3920587)Peak memory usage: 11 MB % 29.49/4.56 % (3920587)Instructions burned: 60 (million) % 29.49/4.56 % (3920587)------------------------------ % 29.49/4.56 % (3920587)------------------------------ % 29.49/4.56 % (3920600)ott+10_1_sil=32000:tgt=ground:random_seed=1554029941:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 29.49/4.56 % (3920456)Instruction limit reached! % 29.49/4.56 % (3920456)------------------------------ % 29.49/4.56 % (3920456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.49/4.56 % (3920456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.49/4.56 % (3920456)CaDiCaL version: 2.1.3 % 29.49/4.56 % (3920456)Termination reason: Instruction limit % 29.49/4.56 % (3920456)Termination phase: Saturation % 29.49/4.56 % (3920456)Time elapsed: 0.492 s % 29.49/4.56 % (3920456)Peak memory usage: 17 MB % 29.49/4.56 % (3920456)Instructions burned: 1181 (million) % 29.49/4.56 % (3920608)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2315167970:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 29.49/4.56 % (3920608)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.49/4.56 % (3920608)Terminated due to inappropriate strategy. % 29.49/4.56 % (3920608)------------------------------ % 29.49/4.56 % (3920608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.49/4.56 % (3920608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.49/4.56 % (3920608)CaDiCaL version: 2.1.3 % 29.49/4.56 % (3920608)Termination reason: Inappropriate % 29.49/4.56 % (3920608)Time elapsed: 0.024 s % 29.49/4.56 % (3920608)Peak memory usage: 11 MB % 29.49/4.56 % (3920608)Instructions burned: 60 (million) % 136.71/19.53 % (3920608)------------------------------ % 136.71/19.53 % (3920608)------------------------------ % 136.71/19.53 % (3920617)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3075413253:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 136.71/19.53 % (3920592)Instruction limit reached! % 136.71/19.53 % (3920592)------------------------------ % 136.71/19.53 % (3920592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.71/19.53 % (3920592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.71/19.53 % (3920592)CaDiCaL version: 2.1.3 % 136.71/19.53 % (3920592)Termination reason: Instruction limit % 136.71/19.53 % (3920592)Termination phase: Saturation % 136.71/19.53 % (3920592)Time elapsed: 0.570 s % 136.71/19.53 % (3920592)Peak memory usage: 19 MB % 136.71/19.53 % (3920592)Instructions burned: 869 (million) % 136.71/19.53 % (3920646)dis+21_1_sil=32000:sas=cadical:random_seed=1127040519:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 136.71/19.53 % (3920550)Instruction limit reached! % 136.71/19.53 % (3920550)------------------------------ % 136.71/19.53 % (3920550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.71/19.53 % (3920550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.71/19.53 % (3920550)CaDiCaL version: 2.1.3 % 136.71/19.53 % (3920550)Termination reason: Instruction limit % 136.71/19.53 % (3920550)Termination phase: Saturation % 136.71/19.53 % (3920550)Time elapsed: 0.929 s % 136.71/19.53 % (3920550)Peak memory usage: 17 MB % 136.71/19.53 % (3920550)Instructions burned: 1472 (million) % 136.71/19.53 % (3920652)ott+11_1_sil=16000:gs=on:random_seed=2809622274:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2985 on theBenchmark for (2985ds/2251Mi) % 136.71/19.53 % (3920652)Instruction limit reached! % 136.71/19.53 % (3920652)------------------------------ % 136.71/19.53 % (3920652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.71/19.53 % (3920652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.71/19.53 % (3920652)CaDiCaL version: 2.1.3 % 136.71/19.53 % (3920652)Termination reason: Instruction limit % 136.71/19.53 % (3920652)Termination phase: Saturation % 136.71/19.53 % (3920652)Time elapsed: 1.476 s % 136.71/19.53 % (3920652)Peak memory usage: 17 MB % 136.71/19.53 % (3920652)Instructions burned: 2251 (million) % 136.71/19.53 % (3920676)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=541642795:fmbsr=1.6:i=67534_2970 on theBenchmark for (2970ds/67534Mi) % 136.71/19.53 % (3920676)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.71/19.53 % (3920676)Terminated due to inappropriate strategy. % 136.71/19.53 % (3920676)------------------------------ % 136.71/19.53 % (3920676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.71/19.53 % (3920676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.71/19.53 % (3920676)CaDiCaL version: 2.1.3 % 136.71/19.53 % (3920676)Termination reason: Inappropriate % 136.71/19.53 % (3920676)Time elapsed: 0.033 s % 136.71/19.53 % (3920676)Peak memory usage: 11 MB % 136.71/19.53 % (3920676)Instructions burned: 60 (million) % 136.71/19.53 % (3920676)------------------------------ % 136.71/19.53 % (3920676)------------------------------ % 136.71/19.53 % (3920678)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2551513906:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2969 on theBenchmark for (2969ds/4591Mi) % 136.71/19.53 % (3920617)Instruction limit reached! % 136.71/19.53 % (3920617)------------------------------ % 136.71/19.53 % (3920617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.71/19.53 % (3920617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.71/19.53 % (3920617)CaDiCaL version: 2.1.3 % 136.71/19.53 % (3920617)Termination reason: Instruction limit % 136.71/19.53 % (3920617)Termination phase: Saturation % 136.71/19.53 % (3920617)Time elapsed: 2.569 s % 136.71/19.53 % (3920617)Peak memory usage: 18 MB % 136.71/19.53 % (3920617)Instructions burned: 3514 (million) % 136.71/19.53 % (3920680)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=669281123:i=29340_2966 on theBenchmark for (2966ds/29340Mi) % 136.71/19.53 % (3920646)Instruction limit reached! % 136.71/19.53 % (3920646)------------------------------ % 136.71/19.53 % (3920646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.71/19.53 % (3920646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.71/19.53 % (3920646)CaDiCaL version: 2.1.3 % 136.71/19.53 % (3920646)Termination reason: Instruction limit % 170.14/24.22 % (3920646)Termination phase: Saturation % 170.14/24.22 % (3920646)Time elapsed: 2.604 s % 170.14/24.22 % (3920646)Peak memory usage: 17 MB % 170.14/24.22 % (3920646)Instructions burned: 3773 (million) % 170.14/24.22 % (3920549)Instruction limit reached! % 170.14/24.22 % (3920549)------------------------------ % 170.14/24.22 % (3920549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.14/24.22 % (3920549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.14/24.22 % (3920549)CaDiCaL version: 2.1.3 % 170.14/24.22 % (3920549)Termination reason: Instruction limit % 170.14/24.22 % (3920549)Termination phase: Saturation % 170.14/24.22 % (3920549)Time elapsed: 3.393 s % 170.14/24.22 % (3920549)Peak memory usage: 16 MB % 170.14/24.22 % (3920549)Instructions burned: 5131 (million) % 170.14/24.22 % (3920682)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3654432204:i=5211_2961 on theBenchmark for (2961ds/5211Mi) % 170.14/24.22 % (3920683)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2307063471:i=5497:nm=2_2961 on theBenchmark for (2961ds/5497Mi) % 170.14/24.22 % (3920683)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.14/24.22 % (3920683)Terminated due to inappropriate strategy. % 170.14/24.22 % (3920683)------------------------------ % 170.14/24.22 % (3920683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.14/24.22 % (3920683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.14/24.22 % (3920683)CaDiCaL version: 2.1.3 % 170.14/24.22 % (3920683)Termination reason: Inappropriate % 170.14/24.22 % (3920683)Time elapsed: 0.050 s % 170.14/24.22 % (3920683)Peak memory usage: 11 MB % 170.14/24.22 % (3920683)Instructions burned: 60 (million) % 170.14/24.22 % (3920683)------------------------------ % 170.14/24.22 % (3920683)------------------------------ % 170.14/24.22 % (3920686)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3142219506:fmbsr=2:i=46332_2960 on theBenchmark for (2960ds/46332Mi) % 170.14/24.22 % (3920686)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.14/24.22 % (3920686)Terminated due to inappropriate strategy. % 170.14/24.22 % (3920686)------------------------------ % 170.14/24.22 % (3920686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.14/24.22 % (3920686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.14/24.22 % (3920686)CaDiCaL version: 2.1.3 % 170.14/24.22 % (3920686)Termination reason: Inappropriate % 170.14/24.22 % (3920686)Time elapsed: 0.029 s % 170.14/24.22 % (3920686)Peak memory usage: 11 MB % 170.14/24.22 % (3920686)Instructions burned: 60 (million) % 170.14/24.22 % (3920686)------------------------------ % 170.14/24.22 % (3920686)------------------------------ % 170.14/24.22 % (3920688)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=246890450:i=14071_2959 on theBenchmark for (2959ds/14071Mi) % 170.14/24.22 % (3920688)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.14/24.22 % (3920688)Terminated due to inappropriate strategy. % 170.14/24.22 % (3920688)------------------------------ % 170.14/24.22 % (3920688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.14/24.22 % (3920688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.14/24.22 % (3920688)CaDiCaL version: 2.1.3 % 170.14/24.22 % (3920688)Termination reason: Inappropriate % 170.14/24.22 % (3920688)Time elapsed: 0.049 s % 170.14/24.22 % (3920688)Peak memory usage: 11 MB % 170.14/24.22 % (3920688)Instructions burned: 60 (million) % 170.14/24.22 % (3920688)------------------------------ % 170.14/24.22 % (3920688)------------------------------ % 170.14/24.22 % (3920690)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2328738436:i=22565:add=on:rawr=on_2958 on theBenchmark for (2958ds/22565Mi) % 170.14/24.22 % (3920600)Instruction limit reached! % 170.14/24.22 % (3920600)------------------------------ % 170.14/24.22 % (3920600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.14/24.22 % (3920600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.14/24.22 % (3920600)CaDiCaL version: 2.1.3 % 170.14/24.22 % (3920600)Termination reason: Instruction limit % 170.14/24.22 % (3920600)Termination phase: Saturation % 170.14/24.22 % (3920600)Time elapsed: 3.590 s % 170.14/24.22 % (3920600)Peak memory usage: 17 MB % 170.14/24.22 % (3920600)Instructions burned: 5115 (million) % 170.14/24.22 % (3920696)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1826886331:i=8173:av=off_2957 on theBenchmark for (2957ds/8173Mi) % 172.26/24.59 % (3920678)Instruction limit reached! % 172.26/24.59 % (3920678)------------------------------ % 172.26/24.59 % (3920678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.26/24.59 % (3920678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.26/24.59 % (3920678)CaDiCaL version: 2.1.3 % 172.26/24.59 % (3920678)Termination reason: Instruction limit % 172.26/24.59 % (3920678)Termination phase: Saturation % 172.26/24.59 % (3920678)Time elapsed: 3.640 s % 172.26/24.59 % (3920678)Peak memory usage: 32 MB % 172.26/24.59 % (3920678)Instructions burned: 4591 (million) % 172.26/24.59 % (3920712)dis+10_16:1_sil=16000:random_seed=3350643614:i=9155:fsr=off_2933 on theBenchmark for (2933ds/9155Mi) % 172.26/24.59 % (3920682)Instruction limit reached! % 172.26/24.59 % (3920682)------------------------------ % 172.26/24.59 % (3920682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.26/24.59 % (3920682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.26/24.59 % (3920682)CaDiCaL version: 2.1.3 % 172.26/24.59 % (3920682)Termination reason: Instruction limit % 172.26/24.59 % (3920682)Termination phase: Saturation % 172.26/24.59 % (3920682)Time elapsed: 3.306 s % 172.26/24.59 % (3920682)Peak memory usage: 17 MB % 172.26/24.59 % (3920682)Instructions burned: 5212 (million) % 172.26/24.59 % (3920714)ott-3_8_sil=64000:random_seed=2631680080:i=20139:bs=on_2927 on theBenchmark for (2927ds/20139Mi) % 172.26/24.59 % (3920696)Instruction limit reached! % 172.26/24.59 % (3920696)------------------------------ % 172.26/24.59 % (3920696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.26/24.59 % (3920696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.26/24.59 % (3920696)CaDiCaL version: 2.1.3 % 172.26/24.59 % (3920696)Termination reason: Instruction limit % 172.26/24.59 % (3920696)Termination phase: Saturation % 172.26/24.59 % (3920696)Time elapsed: 5.833 s % 172.26/24.59 % (3920696)Peak memory usage: 17 MB % 172.26/24.59 % (3920696)Instructions burned: 8174 (million) % 172.26/24.59 % (3920720)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2727363715:fmbsr=2:i=32576_2898 on theBenchmark for (2898ds/32576Mi) % 172.26/24.59 % (3920720)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.26/24.59 % (3920720)Terminated due to inappropriate strategy. % 172.26/24.59 % (3920720)------------------------------ % 172.26/24.59 % (3920720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.26/24.59 % (3920720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.26/24.59 % (3920720)CaDiCaL version: 2.1.3 % 172.26/24.59 % (3920720)Termination reason: Inappropriate % 172.26/24.59 % (3920720)Time elapsed: 0.032 s % 172.26/24.59 % (3920720)Peak memory usage: 11 MB % 172.26/24.59 % (3920720)Instructions burned: 60 (million) % 172.26/24.59 % (3920720)------------------------------ % 172.26/24.59 % (3920720)------------------------------ % 172.26/24.59 % (3920722)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2431434519:i=11404_2897 on theBenchmark for (2897ds/11404Mi) % 172.26/24.59 % (3920712)Instruction limit reached! % 172.26/24.59 % (3920712)------------------------------ % 172.26/24.59 % (3920712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.26/24.59 % (3920712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.26/24.59 % (3920712)CaDiCaL version: 2.1.3 % 172.26/24.59 % (3920712)Termination reason: Instruction limit % 172.26/24.59 % (3920712)Termination phase: Saturation % 172.26/24.59 % (3920712)Time elapsed: 6.565 s % 172.26/24.59 % (3920712)Peak memory usage: 19 MB % 172.26/24.59 % (3920712)Instructions burned: 9156 (million) % 172.26/24.59 % (3920728)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3076443265:i=14134_2867 on theBenchmark for (2867ds/14134Mi) % 172.26/24.59 % (3920722)Instruction limit reached! % 172.26/24.59 % (3920722)------------------------------ % 172.26/24.59 % (3920722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.26/24.59 % (3920722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.26/24.59 % (3920722)CaDiCaL version: 2.1.3 % 172.26/24.59 % (3920722)Termination reason: Instruction limit % 172.26/24.59 % (3920722)Termination phase: Saturation % 172.26/24.59 % (3920722)Time elapsed: 8.098 s % 172.26/24.59 % (3920722)Peak memory usage: 18 MB % 172.26/24.59 % (3920722)Instructions burned: 11404 (million) % 172.26/24.59 % (3920732)dis+33_16_sil=32000:sac=on:random_seed=770661150:i=15851:nm=0_2816 on theBenchmark for (2816ds/15851Mi) % 172.26/24.59 % (3920690)Instruction limit reached! % 172.26/24.59 % (3920690)------------------------------ % 172.26/24.59 % (3920690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.11/34.06 % (3920690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.11/34.06 % (3920690)CaDiCaL version: 2.1.3 % 240.11/34.06 % (3920690)Termination reason: Instruction limit % 240.11/34.06 % (3920690)Termination phase: Saturation % 240.11/34.06 % (3920690)Time elapsed: 15.169 s % 240.11/34.06 % (3920690)Peak memory usage: 18 MB % 240.11/34.06 % (3920690)Instructions burned: 22566 (million) % 240.11/34.06 % (3920734)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=215813021:avsq=on:i=17627:add=on:amm=off_2806 on theBenchmark for (2806ds/17627Mi) % 240.11/34.06 % (3920714)Instruction limit reached! % 240.11/34.06 % (3920714)------------------------------ % 240.11/34.06 % (3920714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.11/34.06 % (3920714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.11/34.06 % (3920714)CaDiCaL version: 2.1.3 % 240.11/34.06 % (3920714)Termination reason: Instruction limit % 240.11/34.06 % (3920714)Termination phase: Saturation % 240.11/34.06 % (3920714)Time elapsed: 14.222 s % 240.11/34.06 % (3920714)Peak memory usage: 20 MB % 240.11/34.06 % (3920714)Instructions burned: 20140 (million) % 240.11/34.06 % (3920740)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3003299455:s2a=on:i=53295_2785 on theBenchmark for (2785ds/53295Mi) % 240.11/34.06 % (3920728)Instruction limit reached! % 240.11/34.06 % (3920728)------------------------------ % 240.11/34.06 % (3920728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.11/34.06 % (3920728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.11/34.06 % (3920728)CaDiCaL version: 2.1.3 % 240.11/34.06 % (3920728)Termination reason: Instruction limit % 240.11/34.06 % (3920728)Termination phase: Saturation % 240.11/34.06 % (3920728)Time elapsed: 10.036 s % 240.11/34.06 % (3920728)Peak memory usage: 18 MB % 240.11/34.06 % (3920728)Instructions burned: 14135 (million) % 240.11/34.06 % (3920744)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3697392396:i=26857:ins=20_2766 on theBenchmark for (2766ds/26857Mi) % 240.11/34.06 % (3920744)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 240.11/34.06 % (3920744)Terminated due to inappropriate strategy. % 240.11/34.06 % (3920744)------------------------------ % 240.11/34.06 % (3920744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.11/34.06 % (3920744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.11/34.06 % (3920744)CaDiCaL version: 2.1.3 % 240.11/34.06 % (3920744)Termination reason: Inappropriate % 240.11/34.06 % (3920744)Time elapsed: 0.050 s % 240.11/34.06 % (3920744)Peak memory usage: 11 MB % 240.11/34.06 % (3920744)Instructions burned: 60 (million) % 240.11/34.06 % (3920744)------------------------------ % 240.11/34.06 % (3920744)------------------------------ % 240.11/34.06 % (3920746)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2042754055:i=28120:bs=on:fsr=off_2765 on theBenchmark for (2765ds/28120Mi) % 240.11/34.06 % (3920680)Instruction limit reached! % 240.11/34.06 % (3920680)------------------------------ % 240.11/34.06 % (3920680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.11/34.06 % (3920680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.11/34.06 % (3920680)CaDiCaL version: 2.1.3 % 240.11/34.06 % (3920680)Termination reason: Instruction limit % 240.11/34.06 % (3920680)Termination phase: Saturation % 240.11/34.06 % (3920680)Time elapsed: 20.476 s % 240.11/34.06 % (3920680)Peak memory usage: 26 MB % 240.11/34.06 % (3920680)Instructions burned: 29340 (million) % 240.11/34.06 % (3920748)fmb+10_1_sil=256000:fmbss=7:random_seed=1496355358:fmbsr=1.6:i=182295_2761 on theBenchmark for (2761ds/182295Mi) % 240.11/34.06 % (3920748)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 240.11/34.06 % (3920748)Terminated due to inappropriate strategy. % 240.11/34.06 % (3920748)------------------------------ % 240.11/34.06 % (3920748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 240.11/34.06 % (3920748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.11/34.06 % (3920748)CaDiCaL version: 2.1.3 % 240.11/34.06 % (3920748)Termination reason: Inappropriate % 240.11/34.06 % (3920748)Time elapsed: 0.050 s % 240.11/34.06 % (3920748)Peak memory usage: 11 MB % 240.11/34.06 % (3920748)Instructions burned: 60 (million) % 240.11/34.06 % (3920748)------------------------------ % 240.11/34.06 % (3920748)------------------------------ % 240.11/34.06 % (3920750)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1209162863:i=44625:gsp=on_2760 on theBenchmark for (2760ds/44625Mi) % 248.31/35.23 % (3920750)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 248.31/35.23 % (3920750)Terminated due to inappropriate strategy. % 248.31/35.23 % (3920750)------------------------------ % 248.31/35.23 % (3920750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.31/35.23 % (3920750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.31/35.23 % (3920750)CaDiCaL version: 2.1.3 % 248.31/35.23 % (3920750)Termination reason: Inappropriate % 248.31/35.23 % (3920750)Time elapsed: 0.053 s % 248.31/35.23 % (3920750)Peak memory usage: 11 MB % 248.31/35.23 % (3920750)Instructions burned: 60 (million) % 248.31/35.23 % (3920750)------------------------------ % 248.31/35.23 % (3920750)------------------------------ % 248.31/35.23 % (3920752)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=330730349:i=160505_2759 on theBenchmark for (2759ds/160505Mi) % 248.31/35.23 % (3920752)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 248.31/35.23 % (3920752)Terminated due to inappropriate strategy. % 248.31/35.23 % (3920752)------------------------------ % 248.31/35.23 % (3920752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.31/35.23 % (3920752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.31/35.23 % (3920752)CaDiCaL version: 2.1.3 % 248.31/35.23 % (3920752)Termination reason: Inappropriate % 248.31/35.23 % (3920752)Time elapsed: 0.052 s % 248.31/35.23 % (3920752)Peak memory usage: 11 MB % 248.31/35.23 % (3920752)Instructions burned: 60 (million) % 248.31/35.23 % (3920752)------------------------------ % 248.31/35.23 % (3920752)------------------------------ % 248.31/35.23 % (3920754)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=883962316:fmbsr=1.3:i=225729_2758 on theBenchmark for (2758ds/225729Mi) % 248.31/35.23 % (3920754)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 248.31/35.23 % (3920754)Terminated due to inappropriate strategy. % 248.31/35.23 % (3920754)------------------------------ % 248.31/35.23 % (3920754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.31/35.23 % (3920754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.31/35.23 % (3920754)CaDiCaL version: 2.1.3 % 248.31/35.23 % (3920754)Termination reason: Inappropriate % 248.31/35.23 % (3920754)Time elapsed: 0.032 s % 248.31/35.23 % (3920754)Peak memory usage: 11 MB % 248.31/35.23 % (3920754)Instructions burned: 60 (million) % 248.31/35.23 % (3920754)------------------------------ % 248.31/35.23 % (3920754)------------------------------ % 248.31/35.23 % (3920756)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2664010983:fmbsr=2:i=185024:ins=7_2758 on theBenchmark for (2758ds/185024Mi) % 248.31/35.23 % (3920756)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 248.31/35.23 % (3920756)Terminated due to inappropriate strategy. % 248.31/35.23 % (3920756)------------------------------ % 248.31/35.23 % (3920756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.31/35.23 % (3920756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.31/35.23 % (3920756)CaDiCaL version: 2.1.3 % 248.31/35.23 % (3920756)Termination reason: Inappropriate % 248.31/35.23 % (3920756)Time elapsed: 0.030 s % 248.31/35.23 % (3920756)Peak memory usage: 11 MB % 248.31/35.23 % (3920756)Instructions burned: 60 (million) % 248.31/35.23 % (3920756)------------------------------ % 248.31/35.23 % (3920756)------------------------------ % 248.31/35.23 % (3920758)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2081631363:rtra=on_2757 on theBenchmark for (2757ds/0Mi) % 248.31/35.23 % (3920758)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 248.31/35.23 % (3920758)Terminated due to inappropriate strategy. % 248.31/35.23 % (3920758)------------------------------ % 248.31/35.23 % (3920758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.31/35.23 % (3920758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.31/35.23 % (3920758)CaDiCaL version: 2.1.3 % 248.31/35.23 % (3920758)Termination reason: Inappropriate % 248.31/35.23 % (3920758)Time elapsed: 0.059 s % 248.31/35.23 % (3920758)Peak memory usage: 11 MB % 248.31/35.23 % (3920758)Instructions burned: 62 (million) % 248.31/35.23 % (3920758)------------------------------ % 248.31/35.23 % (3920758)------------------------------ % 248.31/35.23 % (3920760)% WARNING: option uhcvi not known. % 248.31/35.23 % (3920760)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3897140317:i=271062:add=off:rtra=on:rawr=on_2756 on theBenchmark for (2756ds/271062Mi) % 262.04/37.20 % (3920732)Instruction limit reached! % 262.04/37.20 % (3920732)------------------------------ % 262.04/37.20 % (3920732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.04/37.20 % (3920732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.04/37.20 % (3920732)CaDiCaL version: 2.1.3 % 262.04/37.20 % (3920732)Termination reason: Instruction limit % 262.04/37.20 % (3920732)Termination phase: Saturation % 262.04/37.20 % (3920732)Time elapsed: 11.714 s % 262.04/37.20 % (3920732)Peak memory usage: 23 MB % 262.04/37.20 % (3920732)Instructions burned: 15852 (million) % 262.04/37.20 % (3920780)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3073519551:i=176048:add=on:rtra=on:rawr=on_2699 on theBenchmark for (2699ds/176048Mi) % 262.04/37.20 % (3920734)Instruction limit reached! % 262.04/37.20 % (3920734)------------------------------ % 262.04/37.20 % (3920734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.04/37.20 % (3920734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.04/37.20 % (3920734)CaDiCaL version: 2.1.3 % 262.04/37.20 % (3920734)Termination reason: Instruction limit % 262.04/37.20 % (3920734)Termination phase: Saturation % 262.04/37.20 % (3920734)Time elapsed: 13.727 s % 262.04/37.20 % (3920734)Peak memory usage: 95 MB % 262.04/37.20 % (3920734)Instructions burned: 17627 (million) % 262.04/37.20 % (3920788)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4232530026:i=206:fgj=on:rtra=on_2669 on theBenchmark for (2669ds/206Mi) % 262.04/37.20 % (3920788)Instruction limit reached! % 262.04/37.20 % (3920788)------------------------------ % 262.04/37.20 % (3920788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.04/37.20 % (3920788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.04/37.20 % (3920788)CaDiCaL version: 2.1.3 % 262.04/37.20 % (3920788)Termination reason: Instruction limit % 262.04/37.20 % (3920788)Termination phase: Saturation % 262.04/37.20 % (3920788)Time elapsed: 0.160 s % 262.04/37.20 % (3920788)Peak memory usage: 13 MB % 262.04/37.20 % (3920788)Instructions burned: 207 (million) % 262.04/37.20 % (3920793)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3654637634:i=232:rtra=on_2667 on theBenchmark for (2667ds/232Mi) % 262.04/37.20 % (3920793)Instruction limit reached! % 262.04/37.20 % (3920793)------------------------------ % 262.04/37.20 % (3920793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.04/37.20 % (3920793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.04/37.20 % (3920793)CaDiCaL version: 2.1.3 % 262.04/37.20 % (3920793)Termination reason: Instruction limit % 262.04/37.20 % (3920793)Termination phase: Saturation % 262.04/37.20 % (3920793)Time elapsed: 0.177 s % 262.04/37.20 % (3920793)Peak memory usage: 13 MB % 262.04/37.20 % (3920793)Instructions burned: 232 (million) % 262.04/37.20 % (3920800)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=815864466:i=262:rtra=on_2665 on theBenchmark for (2665ds/262Mi) % 262.04/37.20 % (3920800)Instruction limit reached! % 262.04/37.20 % (3920800)------------------------------ % 262.04/37.20 % (3920800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.04/37.20 % (3920800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.04/37.20 % (3920800)CaDiCaL version: 2.1.3 % 262.04/37.20 % (3920800)Termination reason: Instruction limit % 262.04/37.20 % (3920800)Termination phase: Saturation % 262.04/37.20 % (3920800)Time elapsed: 0.121 s % 262.04/37.20 % (3920800)Peak memory usage: 13 MB % 262.04/37.20 % (3920800)Instructions burned: 263 (million) % 262.04/37.20 % (3920804)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1812916972:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2663 on theBenchmark for (2663ds/318Mi) % 262.04/37.20 % (3920804)Instruction limit reached! % 262.04/37.20 % (3920804)------------------------------ % 262.04/37.20 % (3920804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.04/37.20 % (3920804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.04/37.20 % (3920804)CaDiCaL version: 2.1.3 % 262.04/37.20 % (3920804)Termination reason: Instruction limit % 262.04/37.20 % (3920804)Termination phase: Saturation % 262.04/37.20 % (3920804)Time elapsed: 0.163 s % 262.04/37.20 % (3920804)Peak memory usage: 15 MB % 262.04/37.20 % (3920804)Instructions burned: 320 (million) % 262.04/37.20 % (3920806)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1303340266:i=1428:nm=2:rtra=on_2661 on theBenchmark for (2661ds/1428Mi) % 299.46/42.42 % (3920806)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 299.46/42.42 % (3920806)Terminated due to inappropriate strategy. % 299.46/42.42 % (3920806)------------------------------ % 299.46/42.42 % (3920806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.46/42.42 % (3920806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.46/42.42 % (3920806)CaDiCaL version: 2.1.3 % 299.46/42.42 % (3920806)Termination reason: Inappropriate % 299.46/42.42 % (3920806)Time elapsed: 0.029 s % 299.46/42.42 % (3920806)Peak memory usage: 11 MB % 299.46/42.42 % (3920806)Instructions burned: 61 (million) % 299.46/42.42 % (3920806)------------------------------ % 299.46/42.42 % (3920806)------------------------------ % 299.46/42.42 % (3920808)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4294853706:i=262:bd=preordered:rtra=on:fsd=on_2661 on theBenchmark for (2661ds/262Mi) % 299.46/42.42 % (3920808)Instruction limit reached! % 299.46/42.42 % (3920808)------------------------------ % 299.46/42.42 % (3920808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.46/42.42 % (3920808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.46/42.42 % (3920808)CaDiCaL version: 2.1.3 % 299.46/42.42 % (3920808)Termination reason: Instruction limit % 299.46/42.42 % (3920808)Termination phase: Saturation % 299.46/42.42 % (3920808)Time elapsed: 0.080 s % 299.46/42.42 % (3920808)Peak memory usage: 17 MB % 299.46/42.42 % (3920808)Instructions burned: 265 (million) % 299.46/42.42 % (3920812)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=2224365835:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2660 on theBenchmark for (2660ds/1368Mi) % 299.46/42.42 % (3920812)Instruction limit reached! % 299.46/42.42 % (3920812)------------------------------ % 299.46/42.42 % (3920812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.46/42.42 % (3920812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.46/42.42 % (3920812)CaDiCaL version: 2.1.3 % 299.46/42.42 % (3920812)Termination reason: Instruction limit % 299.46/42.42 % (3920812)Termination phase: Saturation % 299.46/42.42 % (3920812)Time elapsed: 0.438 s % 299.46/42.42 % (3920812)Peak memory usage: 18 MB % 299.46/42.42 % (3920812)Instructions burned: 1369 (million) % 299.46/42.42 % (3920816)ott-21_1_sil=16000:si=on:fs=off:random_seed=108360092:i=360:av=off:fsr=off:rtra=on_2655 on theBenchmark for (2655ds/360Mi) % 299.46/42.42 % (3920816)Instruction limit reached! % 299.46/42.42 % (3920816)------------------------------ % 299.46/42.42 % (3920816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.46/42.42 % (3920816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.46/42.42 % (3920816)CaDiCaL version: 2.1.3 % 299.46/42.42 % (3920816)Termination reason: Instruction limit % 299.46/42.42 % (3920816)Termination phase: Saturation % 299.46/42.42 % (3920816)Time elapsed: 0.140 s % 299.46/42.42 % (3920816)Peak memory usage: 13 MB % 299.46/42.42 % (3920816)Instructions burned: 363 (million) % 299.46/42.42 % (3920823)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=296722165:i=954:bd=all:rtra=on_2654 on theBenchmark for (2654ds/954Mi) % 299.46/42.42 % (3920823)Instruction limit reached! % 299.46/42.42 % (3920823)------------------------------ % 299.46/42.42 % (3920823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.46/42.42 % (3920823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.46/42.42 % (3920823)CaDiCaL version: 2.1.3 % 299.46/42.42 % (3920823)Termination reason: Instruction limit % 299.46/42.42 % (3920823)Termination phase: Saturation % 299.46/42.42 % (3920823)Time elapsed: 0.370 s % 299.46/42.42 % (3920823)Peak memory usage: 15 MB % 299.46/42.42 % (3920823)Instructions burned: 955 (million) % 299.46/42.42 % (3920828)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3670365648:fmbsr=1.3:i=1730:ins=25:rtra=on_2650 on theBenchmark for (2650ds/1730Mi) % 299.46/42.42 % (3920828)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 299.46/42.42 % (3920828)Terminated due to inappropriate strategy. % 299.46/42.42 % (3920828)------------------------------ % 299.46/42.42 % (3920828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.46/42.42 % (3920828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.46/42.42 % (3920828)CaDiCaL version: 2.1.3 % 299.46/42.42 % (3920828)Termination reaTerminated % 300.11/42.54 % Vampire exiting % 300.11/42.54 Terminated %------------------------------------------------------------------------------