%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC469_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 : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:06:02 PM UTC 2026 % Result : Timeout 300.57s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWC469_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.02 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.00/0.10 % Computer : n012.cluster.edu % 0.00/0.10 % Model : x86_64 x86_64 % 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.10 % Memory : 8046.5625MB % 0.00/0.10 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 09:39:19 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.12 Running first-order model finding % 0.08/0.12 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.06/0.47 % (3262382)Will run a generic schedule for satisfiability detection. % 2.06/0.47 % (3262388)% WARNING: option uhcvi not known. % 2.06/0.47 % (3262387)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3342665145_2999 on theBenchmark for (2999ds/0Mi) % 2.06/0.47 % (3262390)dis+10_1_sil=32000:sp=arity:random_seed=3254945569:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.06/0.47 % (3262389)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=30361351:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.06/0.47 % (3262388)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2810269661:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.06/0.47 % (3262391)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3535968456:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.06/0.47 % (3262392)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3525411118:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.06/0.47 % (3262393)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2484746123:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.06/0.47 % (3262387)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.06/0.47 % (3262387)Terminated due to inappropriate strategy. % 2.06/0.47 % (3262387)------------------------------ % 2.06/0.47 % (3262387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.06/0.47 % (3262387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.06/0.47 % (3262387)CaDiCaL version: 2.1.3 % 2.06/0.47 % (3262387)Termination reason: Inappropriate % 2.06/0.47 % (3262387)Time elapsed: 0.0000 s % 2.06/0.47 % (3262387)Peak memory usage: 10 MB % 2.06/0.47 % (3262387)Instructions burned: 1 (million) % 2.06/0.47 % (3262387)------------------------------ % 2.06/0.47 % (3262387)------------------------------ % 2.06/0.47 % (3262401)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3828370335:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.06/0.47 % (3262401)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.06/0.47 % (3262401)Terminated due to inappropriate strategy. % 2.06/0.47 % (3262401)------------------------------ % 2.06/0.47 % (3262401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.06/0.47 % (3262401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.06/0.47 % (3262401)CaDiCaL version: 2.1.3 % 2.06/0.47 % (3262401)Termination reason: Inappropriate % 2.06/0.47 % (3262401)Time elapsed: 0.0000 s % 2.06/0.47 % (3262401)Peak memory usage: 10 MB % 2.06/0.47 % (3262401)Instructions burned: 1 (million) % 2.06/0.47 % (3262401)------------------------------ % 2.06/0.47 % (3262401)------------------------------ % 2.06/0.47 % (3262403)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1613095224:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.06/0.47 % (3262390)Instruction limit reached! % 2.06/0.47 % (3262390)------------------------------ % 2.06/0.47 % (3262390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.06/0.47 % (3262390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.06/0.47 % (3262390)CaDiCaL version: 2.1.3 % 2.06/0.47 % (3262390)Termination reason: Instruction limit % 2.06/0.47 % (3262390)Termination phase: Saturation % 2.06/0.47 % (3262390)Time elapsed: 0.035 s % 2.06/0.47 % (3262390)Peak memory usage: 12 MB % 2.06/0.47 % (3262390)Instructions burned: 106 (million) % 2.06/0.47 % (3262391)Instruction limit reached! % 2.06/0.47 % (3262391)------------------------------ % 2.06/0.47 % (3262391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.06/0.47 % (3262391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.06/0.47 % (3262391)CaDiCaL version: 2.1.3 % 2.06/0.47 % (3262391)Termination reason: Instruction limit % 2.06/0.47 % (3262391)Termination phase: Saturation % 2.06/0.47 % (3262391)Time elapsed: 0.039 s % 2.06/0.47 % (3262391)Peak memory usage: 12 MB % 2.06/0.47 % (3262391)Instructions burned: 118 (million) % 2.06/0.47 % (3262392)Instruction limit reached! % 2.06/0.47 % (3262392)------------------------------ % 2.06/0.47 % (3262392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.06/0.47 % (3262392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.06/0.47 % (3262392)CaDiCaL version: 2.1.3 % 2.06/0.47 % (3262392)Termination reason: Instruction limit % 3.28/0.63 % (3262392)Termination phase: Saturation % 3.28/0.63 % (3262392)Time elapsed: 0.044 s % 3.28/0.63 % (3262392)Peak memory usage: 13 MB % 3.28/0.63 % (3262392)Instructions burned: 133 (million) % 3.28/0.63 % (3262405)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=3855144132:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.28/0.63 % (3262406)ott-21_1_sil=16000:fs=off:random_seed=1027315705:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.28/0.63 % (3262407)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2761368656:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 3.28/0.63 % (3262393)Instruction limit reached! % 3.28/0.63 % (3262393)------------------------------ % 3.28/0.63 % (3262393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.63 % (3262393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.63 % (3262393)CaDiCaL version: 2.1.3 % 3.28/0.63 % (3262393)Termination reason: Instruction limit % 3.28/0.63 % (3262393)Termination phase: Saturation % 3.28/0.63 % (3262393)Time elapsed: 0.060 s % 3.28/0.63 % (3262393)Peak memory usage: 13 MB % 3.28/0.63 % (3262393)Instructions burned: 161 (million) % 3.28/0.63 % (3262411)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=538098010:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 3.28/0.63 % (3262403)Instruction limit reached! % 3.28/0.63 % (3262403)------------------------------ % 3.28/0.63 % (3262403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.63 % (3262403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.63 % (3262403)CaDiCaL version: 2.1.3 % 3.28/0.63 % (3262403)Termination reason: Instruction limit % 3.28/0.63 % (3262403)Termination phase: Saturation % 3.28/0.63 % (3262403)Time elapsed: 0.048 s % 3.28/0.63 % (3262403)Peak memory usage: 12 MB % 3.28/0.63 % (3262403)Instructions burned: 133 (million) % 3.28/0.63 % (3262411)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.28/0.63 % (3262411)Terminated due to inappropriate strategy. % 3.28/0.63 % (3262411)------------------------------ % 3.28/0.63 % (3262411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.63 % (3262411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.63 % (3262411)CaDiCaL version: 2.1.3 % 3.28/0.63 % (3262411)Termination reason: Inappropriate % 3.28/0.63 % (3262411)Time elapsed: 0.0000 s % 3.28/0.63 % (3262411)Peak memory usage: 10 MB % 3.28/0.63 % (3262411)Instructions burned: 1 (million) % 3.28/0.63 % (3262411)------------------------------ % 3.28/0.63 % (3262411)------------------------------ % 3.28/0.63 % (3262413)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3519262805:i=1179_2999 on theBenchmark for (2999ds/1179Mi) % 3.28/0.63 % (3262414)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=217824340:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi) % 3.28/0.63 % (3262414)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.28/0.63 % (3262414)Terminated due to inappropriate strategy. % 3.28/0.63 % (3262414)------------------------------ % 3.28/0.63 % (3262414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.63 % (3262414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.63 % (3262414)CaDiCaL version: 2.1.3 % 3.28/0.63 % (3262414)Termination reason: Inappropriate % 3.28/0.63 % (3262414)Time elapsed: 0.0000 s % 3.28/0.63 % (3262414)Peak memory usage: 11 MB % 3.28/0.63 % (3262414)Instructions burned: 1 (million) % 3.28/0.63 % (3262414)------------------------------ % 3.28/0.63 % (3262414)------------------------------ % 3.28/0.63 % (3262406)Instruction limit reached! % 3.28/0.63 % (3262406)------------------------------ % 3.28/0.63 % (3262406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.63 % (3262406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.63 % (3262406)CaDiCaL version: 2.1.3 % 3.28/0.63 % (3262406)Termination reason: Instruction limit % 3.28/0.63 % (3262406)Termination phase: Saturation % 3.28/0.63 % (3262406)Time elapsed: 0.042 s % 3.28/0.63 % (3262406)Peak memory usage: 12 MB % 3.28/0.63 % (3262406)Instructions burned: 181 (million) % 3.28/0.63 % (3262417)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=263248147:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 11.22/1.88 % (3262418)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=938979979:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 11.22/1.88 % (3262407)Instruction limit reached! % 11.22/1.88 % (3262407)------------------------------ % 11.22/1.88 % (3262407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.22/1.88 % (3262407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.22/1.88 % (3262407)CaDiCaL version: 2.1.3 % 11.22/1.88 % (3262407)Termination reason: Instruction limit % 11.22/1.88 % (3262407)Termination phase: Saturation % 11.22/1.88 % (3262407)Time elapsed: 0.155 s % 11.22/1.88 % (3262407)Peak memory usage: 14 MB % 11.22/1.88 % (3262407)Instructions burned: 479 (million) % 11.22/1.88 % (3262421)fmb+10_1_sil=64000:random_seed=2563408853:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 11.22/1.88 % (3262421)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.22/1.88 % (3262421)Terminated due to inappropriate strategy. % 11.22/1.88 % (3262421)------------------------------ % 11.22/1.88 % (3262421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.22/1.88 % (3262421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.22/1.88 % (3262421)CaDiCaL version: 2.1.3 % 11.22/1.88 % (3262421)Termination reason: Inappropriate % 11.22/1.88 % (3262421)Time elapsed: 0.0000 s % 11.22/1.88 % (3262421)Peak memory usage: 10 MB % 11.22/1.88 % (3262421)Instructions burned: 1 (million) % 11.22/1.88 % (3262421)------------------------------ % 11.22/1.88 % (3262421)------------------------------ % 11.22/1.88 % (3262423)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=144600221:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 11.22/1.88 % (3262423)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.22/1.88 % (3262423)Terminated due to inappropriate strategy. % 11.22/1.88 % (3262423)------------------------------ % 11.22/1.88 % (3262423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.22/1.88 % (3262423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.22/1.88 % (3262423)CaDiCaL version: 2.1.3 % 11.22/1.88 % (3262423)Termination reason: Inappropriate % 11.22/1.88 % (3262423)Time elapsed: 0.0000 s % 11.22/1.88 % (3262423)Peak memory usage: 10 MB % 11.22/1.88 % (3262423)Instructions burned: 1 (million) % 11.22/1.88 % (3262423)------------------------------ % 11.22/1.88 % (3262423)------------------------------ % 11.22/1.88 % (3262405)Instruction limit reached! % 11.22/1.88 % (3262405)------------------------------ % 11.22/1.88 % (3262405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.22/1.88 % (3262405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.22/1.88 % (3262405)CaDiCaL version: 2.1.3 % 11.22/1.88 % (3262405)Termination reason: Instruction limit % 11.22/1.88 % (3262405)Termination phase: Saturation % 11.22/1.88 % (3262405)Time elapsed: 0.188 s % 11.22/1.88 % (3262405)Peak memory usage: 17 MB % 11.22/1.88 % (3262405)Instructions burned: 685 (million) % 11.22/1.88 % (3262425)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2500097153:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 11.22/1.88 % (3262425)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.22/1.88 % (3262425)Terminated due to inappropriate strategy. % 11.22/1.88 % (3262425)------------------------------ % 11.22/1.88 % (3262425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.22/1.88 % (3262425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.22/1.88 % (3262425)CaDiCaL version: 2.1.3 % 11.22/1.88 % (3262425)Termination reason: Inappropriate % 11.22/1.88 % (3262425)Time elapsed: 0.0000 s % 11.22/1.88 % (3262425)Peak memory usage: 10 MB % 11.22/1.88 % (3262425)Instructions burned: 1 (million) % 11.22/1.88 % (3262426)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2093419954:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 11.22/1.88 % (3262425)------------------------------ % 11.22/1.88 % (3262425)------------------------------ % 11.22/1.88 % (3262429)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3101573218:i=1472:ins=7:fdi=8:gsp=on_2997 on theBenchmark for (2997ds/1472Mi) % 11.22/1.88 % (3262417)Instruction limit reached! % 11.22/1.88 % (3262417)------------------------------ % 17.61/2.74 % (3262417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.61/2.74 % (3262417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.61/2.74 % (3262417)CaDiCaL version: 2.1.3 % 17.61/2.74 % (3262417)Termination reason: Instruction limit % 17.61/2.74 % (3262417)Termination phase: Saturation % 17.61/2.74 % (3262417)Time elapsed: 0.224 s % 17.61/2.74 % (3262417)Peak memory usage: 18 MB % 17.61/2.74 % (3262417)Instructions burned: 692 (million) % 17.61/2.74 % (3262431)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=592383820:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 17.61/2.74 % (3262431)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.61/2.74 % (3262431)Terminated due to inappropriate strategy. % 17.61/2.74 % (3262431)------------------------------ % 17.61/2.74 % (3262431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.61/2.74 % (3262431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.61/2.74 % (3262431)CaDiCaL version: 2.1.3 % 17.61/2.74 % (3262431)Termination reason: Inappropriate % 17.61/2.74 % (3262431)Time elapsed: 0.0000 s % 17.61/2.74 % (3262431)Peak memory usage: 10 MB % 17.61/2.74 % (3262431)Instructions burned: 1 (million) % 17.61/2.74 % (3262431)------------------------------ % 17.61/2.74 % (3262431)------------------------------ % 17.61/2.74 % (3262433)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2657225837:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi) % 17.61/2.74 % (3262433)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.61/2.74 % (3262433)Terminated due to inappropriate strategy. % 17.61/2.74 % (3262433)------------------------------ % 17.61/2.74 % (3262433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.61/2.74 % (3262433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.61/2.74 % (3262433)CaDiCaL version: 2.1.3 % 17.61/2.74 % (3262433)Termination reason: Inappropriate % 17.61/2.74 % (3262433)Time elapsed: 0.0000 s % 17.61/2.74 % (3262433)Peak memory usage: 10 MB % 17.61/2.74 % (3262433)Instructions burned: 1 (million) % 17.61/2.74 % (3262433)------------------------------ % 17.61/2.74 % (3262433)------------------------------ % 17.61/2.74 % (3262435)ott-2_1_sil=16000:newcnf=on:random_seed=2915434771:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2996 on theBenchmark for (2996ds/869Mi) % 17.61/2.74 % (3262418)Instruction limit reached! % 17.61/2.74 % (3262418)------------------------------ % 17.61/2.74 % (3262418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.61/2.74 % (3262418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.61/2.74 % (3262418)CaDiCaL version: 2.1.3 % 17.61/2.74 % (3262418)Termination reason: Instruction limit % 17.61/2.74 % (3262418)Termination phase: Saturation % 17.61/2.74 % (3262418)Time elapsed: 0.269 s % 17.61/2.74 % (3262418)Peak memory usage: 19 MB % 17.61/2.74 % (3262418)Instructions burned: 879 (million) % 17.61/2.74 % (3262437)ott+10_1_sil=32000:tgt=ground:random_seed=428250290:i=5114:av=off_2996 on theBenchmark for (2996ds/5114Mi) % 17.61/2.74 % (3262413)Instruction limit reached! % 17.61/2.74 % (3262413)------------------------------ % 17.61/2.74 % (3262413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.61/2.74 % (3262413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.61/2.74 % (3262413)CaDiCaL version: 2.1.3 % 17.61/2.74 % (3262413)Termination reason: Instruction limit % 17.61/2.74 % (3262413)Termination phase: Saturation % 17.61/2.74 % (3262413)Time elapsed: 0.384 s % 17.61/2.74 % (3262413)Peak memory usage: 19 MB % 17.61/2.74 % (3262413)Instructions burned: 1179 (million) % 17.61/2.74 % (3262439)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1798612656:i=54282_2995 on theBenchmark for (2995ds/54282Mi) % 17.61/2.74 % (3262439)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.61/2.74 % (3262439)Terminated due to inappropriate strategy. % 17.61/2.74 % (3262439)------------------------------ % 17.61/2.74 % (3262439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.61/2.74 % (3262439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.61/2.74 % (3262439)CaDiCaL version: 2.1.3 % 17.61/2.74 % (3262439)Termination reason: Inappropriate % 17.61/2.74 % (3262439)Time elapsed: 0.0000 s % 17.61/2.74 % (3262439)Peak memory usage: 10 MB % 17.61/2.74 % (3262439)Instructions burned: 1 (million) % 58.93/8.54 % (3262439)------------------------------ % 58.93/8.54 % (3262439)------------------------------ % 58.93/8.54 % (3262441)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=839584120:i=3512:aac=none_2994 on theBenchmark for (2994ds/3512Mi) % 58.93/8.54 % (3262435)Instruction limit reached! % 58.93/8.54 % (3262435)------------------------------ % 58.93/8.54 % (3262435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.93/8.54 % (3262435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.93/8.54 % (3262435)CaDiCaL version: 2.1.3 % 58.93/8.54 % (3262435)Termination reason: Instruction limit % 58.93/8.54 % (3262435)Termination phase: Saturation % 58.93/8.54 % (3262435)Time elapsed: 0.281 s % 58.93/8.54 % (3262435)Peak memory usage: 15 MB % 58.93/8.54 % (3262435)Instructions burned: 872 (million) % 58.93/8.54 % (3262429)Instruction limit reached! % 58.93/8.54 % (3262429)------------------------------ % 58.93/8.54 % (3262429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.93/8.54 % (3262429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.93/8.54 % (3262429)CaDiCaL version: 2.1.3 % 58.93/8.54 % (3262429)Termination reason: Instruction limit % 58.93/8.54 % (3262429)Termination phase: Saturation % 58.93/8.54 % (3262429)Time elapsed: 0.387 s % 58.93/8.54 % (3262429)Peak memory usage: 23 MB % 58.93/8.54 % (3262429)Instructions burned: 1476 (million) % 58.93/8.54 % (3262443)dis+21_1_sil=32000:sas=cadical:random_seed=2388355951:i=3773:amm=off_2993 on theBenchmark for (2993ds/3773Mi) % 58.93/8.54 % (3262444)ott+11_1_sil=16000:gs=on:random_seed=3492458234:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2993 on theBenchmark for (2993ds/2251Mi) % 58.93/8.54 % (3262444)Instruction limit reached! % 58.93/8.54 % (3262444)------------------------------ % 58.93/8.54 % (3262444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.93/8.54 % (3262444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.93/8.54 % (3262444)CaDiCaL version: 2.1.3 % 58.93/8.54 % (3262444)Termination reason: Instruction limit % 58.93/8.54 % (3262444)Termination phase: Saturation % 58.93/8.54 % (3262444)Time elapsed: 0.661 s % 58.93/8.54 % (3262444)Peak memory usage: 24 MB % 58.93/8.54 % (3262444)Instructions burned: 2256 (million) % 58.93/8.55 % (3262447)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2426474510:fmbsr=1.6:i=67534_2986 on theBenchmark for (2986ds/67534Mi) % 58.93/8.55 % (3262447)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 58.93/8.55 % (3262447)Terminated due to inappropriate strategy. % 58.93/8.55 % (3262447)------------------------------ % 58.93/8.55 % (3262447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.93/8.55 % (3262447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.93/8.55 % (3262447)CaDiCaL version: 2.1.3 % 58.93/8.55 % (3262447)Termination reason: Inappropriate % 58.93/8.55 % (3262447)Time elapsed: 0.0000 s % 58.93/8.55 % (3262447)Peak memory usage: 10 MB % 58.93/8.55 % (3262447)Instructions burned: 1 (million) % 58.93/8.55 % (3262447)------------------------------ % 58.93/8.55 % (3262447)------------------------------ % 58.93/8.55 % (3262449)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=894457302:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2986 on theBenchmark for (2986ds/4591Mi) % 58.93/8.55 % (3262441)Instruction limit reached! % 58.93/8.55 % (3262441)------------------------------ % 58.93/8.55 % (3262441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.93/8.55 % (3262441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.93/8.55 % (3262441)CaDiCaL version: 2.1.3 % 58.93/8.55 % (3262441)Termination reason: Instruction limit % 58.93/8.55 % (3262441)Termination phase: Saturation % 58.93/8.55 % (3262441)Time elapsed: 0.996 s % 58.93/8.55 % (3262441)Peak memory usage: 35 MB % 58.93/8.55 % (3262441)Instructions burned: 3514 (million) % 58.93/8.55 % (3262451)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1742666280:i=29340_2984 on theBenchmark for (2984ds/29340Mi) % 58.93/8.55 % (3262426)Instruction limit reached! % 58.93/8.55 % (3262426)------------------------------ % 58.93/8.55 % (3262426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.93/8.55 % (3262426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.93/8.55 % (3262426)CaDiCaL version: 2.1.3 % 58.93/8.55 % (3262426)Termination reason: Instruction limit % 68.27/9.99 % (3262426)Termination phase: Saturation % 68.27/9.99 % (3262426)Time elapsed: 1.479 s % 68.27/9.99 % (3262426)Peak memory usage: 41 MB % 68.27/9.99 % (3262426)Instructions burned: 5131 (million) % 68.27/9.99 % (3262443)Instruction limit reached! % 68.27/9.99 % (3262443)------------------------------ % 68.27/9.99 % (3262443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 68.27/9.99 % (3262443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.27/9.99 % (3262443)CaDiCaL version: 2.1.3 % 68.27/9.99 % (3262443)Termination reason: Instruction limit % 68.27/9.99 % (3262443)Termination phase: Saturation % 68.27/9.99 % (3262443)Time elapsed: 1.086 s % 68.27/9.99 % (3262443)Peak memory usage: 31 MB % 68.27/9.99 % (3262443)Instructions burned: 3775 (million) % 68.27/9.99 % (3262453)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1905502821:i=5211_2982 on theBenchmark for (2982ds/5211Mi) % 68.27/9.99 % (3262454)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1172781348:i=5497:nm=2_2982 on theBenchmark for (2982ds/5497Mi) % 68.27/9.99 % (3262454)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 68.27/9.99 % (3262454)Terminated due to inappropriate strategy. % 68.27/9.99 % (3262454)------------------------------ % 68.27/9.99 % (3262454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 68.27/9.99 % (3262454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.27/9.99 % (3262454)CaDiCaL version: 2.1.3 % 68.27/9.99 % (3262454)Termination reason: Inappropriate % 68.27/9.99 % (3262454)Time elapsed: 0.0000 s % 68.27/9.99 % (3262454)Peak memory usage: 10 MB % 68.27/9.99 % (3262454)Instructions burned: 1 (million) % 68.27/9.99 % (3262454)------------------------------ % 68.27/9.99 % (3262454)------------------------------ % 68.27/9.99 % (3262457)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2771709370:fmbsr=2:i=46332_2982 on theBenchmark for (2982ds/46332Mi) % 68.27/9.99 % (3262457)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 68.27/9.99 % (3262457)Terminated due to inappropriate strategy. % 68.27/9.99 % (3262457)------------------------------ % 68.27/9.99 % (3262457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 68.27/9.99 % (3262457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.27/9.99 % (3262457)CaDiCaL version: 2.1.3 % 68.27/9.99 % (3262457)Termination reason: Inappropriate % 68.27/9.99 % (3262457)Time elapsed: 0.0000 s % 68.27/9.99 % (3262457)Peak memory usage: 10 MB % 68.27/9.99 % (3262457)Instructions burned: 1 (million) % 68.27/9.99 % (3262457)------------------------------ % 68.27/9.99 % (3262457)------------------------------ % 68.27/9.99 % (3262459)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2345134939:i=14071_2982 on theBenchmark for (2982ds/14071Mi) % 68.27/9.99 % (3262459)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 68.27/9.99 % (3262459)Terminated due to inappropriate strategy. % 68.27/9.99 % (3262459)------------------------------ % 68.27/9.99 % (3262459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 68.27/9.99 % (3262459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.27/9.99 % (3262459)CaDiCaL version: 2.1.3 % 68.27/9.99 % (3262459)Termination reason: Inappropriate % 68.27/9.99 % (3262459)Time elapsed: 0.0000 s % 68.27/9.99 % (3262459)Peak memory usage: 10 MB % 68.27/9.99 % (3262459)Instructions burned: 1 (million) % 68.27/9.99 % (3262459)------------------------------ % 68.27/9.99 % (3262459)------------------------------ % 68.27/9.99 % (3262461)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3936340600:i=22565:add=on:rawr=on_2982 on theBenchmark for (2982ds/22565Mi) % 68.27/9.99 % (3262437)Instruction limit reached! % 68.27/9.99 % (3262437)------------------------------ % 68.27/9.99 % (3262437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 68.27/9.99 % (3262437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.27/9.99 % (3262437)CaDiCaL version: 2.1.3 % 68.27/9.99 % (3262437)Termination reason: Instruction limit % 68.27/9.99 % (3262437)Termination phase: Saturation % 68.27/9.99 % (3262437)Time elapsed: 1.729 s % 68.27/9.99 % (3262437)Peak memory usage: 41 MB % 68.27/9.99 % (3262437)Instructions burned: 5115 (million) % 68.27/9.99 % (3262463)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3530727534:i=8173:av=off_2978 on theBenchmark for (2978ds/8173Mi) % 68.27/9.99 % (3262449)Instruction limit reached! % 69.66/10.05 % (3262449)------------------------------ % 69.66/10.05 % (3262449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.66/10.05 % (3262449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.66/10.05 % (3262449)CaDiCaL version: 2.1.3 % 69.66/10.05 % (3262449)Termination reason: Instruction limit % 69.66/10.05 % (3262449)Termination phase: Saturation % 69.66/10.05 % (3262449)Time elapsed: 1.244 s % 69.66/10.05 % (3262449)Peak memory usage: 50 MB % 69.66/10.05 % (3262449)Instructions burned: 4593 (million) % 69.66/10.05 % (3262465)dis+10_16:1_sil=16000:random_seed=233196449:i=9155:fsr=off_2973 on theBenchmark for (2973ds/9155Mi) % 69.66/10.05 % (3262453)Instruction limit reached! % 69.66/10.05 % (3262453)------------------------------ % 69.66/10.05 % (3262453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.66/10.05 % (3262453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.66/10.05 % (3262453)CaDiCaL version: 2.1.3 % 69.66/10.05 % (3262453)Termination reason: Instruction limit % 69.66/10.05 % (3262453)Termination phase: Saturation % 69.66/10.05 % (3262453)Time elapsed: 1.479 s % 69.66/10.05 % (3262453)Peak memory usage: 49 MB % 69.66/10.05 % (3262453)Instructions burned: 5214 (million) % 69.66/10.05 % (3262467)ott-3_8_sil=64000:random_seed=2290208212:i=20139:bs=on_2967 on theBenchmark for (2967ds/20139Mi) % 69.66/10.05 % (3262463)Instruction limit reached! % 69.66/10.05 % (3262463)------------------------------ % 69.66/10.05 % (3262463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.66/10.05 % (3262463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.66/10.05 % (3262463)CaDiCaL version: 2.1.3 % 69.66/10.05 % (3262463)Termination reason: Instruction limit % 69.66/10.05 % (3262463)Termination phase: Saturation % 69.66/10.05 % (3262463)Time elapsed: 2.780 s % 69.66/10.05 % (3262463)Peak memory usage: 51 MB % 69.66/10.05 % (3262463)Instructions burned: 8173 (million) % 69.66/10.05 % (3262469)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=963098786:fmbsr=2:i=32576_2950 on theBenchmark for (2950ds/32576Mi) % 69.66/10.05 % (3262469)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 69.66/10.05 % (3262469)Terminated due to inappropriate strategy. % 69.66/10.05 % (3262469)------------------------------ % 69.66/10.05 % (3262469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.66/10.05 % (3262469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.66/10.05 % (3262469)CaDiCaL version: 2.1.3 % 69.66/10.05 % (3262469)Termination reason: Inappropriate % 69.66/10.05 % (3262469)Time elapsed: 0.0000 s % 69.66/10.05 % (3262469)Peak memory usage: 10 MB % 69.66/10.05 % (3262469)Instructions burned: 1 (million) % 69.66/10.05 % (3262469)------------------------------ % 69.66/10.05 % (3262469)------------------------------ % 69.66/10.05 % (3262471)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2066323616:i=11404_2950 on theBenchmark for (2950ds/11404Mi) % 69.66/10.05 % (3262465)Instruction limit reached! % 69.66/10.05 % (3262465)------------------------------ % 69.66/10.05 % (3262465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.66/10.05 % (3262465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.66/10.05 % (3262465)CaDiCaL version: 2.1.3 % 69.66/10.05 % (3262465)Termination reason: Instruction limit % 69.66/10.05 % (3262465)Termination phase: Saturation % 69.66/10.05 % (3262465)Time elapsed: 2.478 s % 69.66/10.05 % (3262465)Peak memory usage: 52 MB % 69.66/10.05 % (3262465)Instructions burned: 9157 (million) % 69.66/10.05 % (3262473)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1114860509:i=14134_2948 on theBenchmark for (2948ds/14134Mi) % 69.66/10.05 % (3262461)Instruction limit reached! % 69.66/10.05 % (3262461)------------------------------ % 69.66/10.05 % (3262461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.66/10.05 % (3262461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.66/10.05 % (3262461)CaDiCaL version: 2.1.3 % 69.66/10.05 % (3262461)Termination reason: Instruction limit % 69.66/10.05 % (3262461)Termination phase: Saturation % 69.66/10.05 % (3262461)Time elapsed: 5.112 s % 69.66/10.05 % (3262461)Peak memory usage: 75 MB % 69.66/10.05 % (3262461)Instructions burned: 22567 (million) % 69.66/10.05 % (3262475)dis+33_16_sil=32000:sac=on:random_seed=2630819637:i=15851:nm=0_2930 on theBenchmark for (2930ds/15851Mi) % 69.66/10.05 % (3262451)Instruction limit reached! % 69.66/10.05 % (3262451)------------------------------ % 69.66/10.05 % (3262451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.43/13.44 % (3262451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.43/13.44 % (3262451)CaDiCaL version: 2.1.3 % 93.43/13.44 % (3262451)Termination reason: Instruction limit % 93.43/13.44 % (3262451)Termination phase: Saturation % 93.43/13.44 % (3262451)Time elapsed: 6.895 s % 93.43/13.44 % (3262451)Peak memory usage: 168 MB % 93.43/13.44 % (3262451)Instructions burned: 29343 (million) % 93.43/13.44 % (3262477)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1666712469:avsq=on:i=17627:add=on:amm=off_2915 on theBenchmark for (2915ds/17627Mi) % 93.43/13.44 % (3262471)Instruction limit reached! % 93.43/13.44 % (3262471)------------------------------ % 93.43/13.44 % (3262471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.43/13.44 % (3262471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.43/13.44 % (3262471)CaDiCaL version: 2.1.3 % 93.43/13.44 % (3262471)Termination reason: Instruction limit % 93.43/13.44 % (3262471)Termination phase: Saturation % 93.43/13.44 % (3262471)Time elapsed: 3.833 s % 93.43/13.44 % (3262471)Peak memory usage: 71 MB % 93.43/13.44 % (3262471)Instructions burned: 11405 (million) % 93.43/13.44 % (3262479)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2191299304:s2a=on:i=53295_2912 on theBenchmark for (2912ds/53295Mi) % 93.43/13.44 % (3262467)Instruction limit reached! % 93.43/13.44 % (3262467)------------------------------ % 93.43/13.44 % (3262467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.43/13.44 % (3262467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.43/13.44 % (3262467)CaDiCaL version: 2.1.3 % 93.43/13.44 % (3262467)Termination reason: Instruction limit % 93.43/13.44 % (3262467)Termination phase: Saturation % 93.43/13.44 % (3262467)Time elapsed: 5.940 s % 93.43/13.44 % (3262467)Peak memory usage: 57 MB % 93.43/13.44 % (3262467)Instructions burned: 20140 (million) % 93.43/13.44 % (3262481)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3692563484:i=26857:ins=20_2907 on theBenchmark for (2907ds/26857Mi) % 93.43/13.44 % (3262481)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 93.43/13.44 % (3262481)Terminated due to inappropriate strategy. % 93.43/13.44 % (3262481)------------------------------ % 93.43/13.44 % (3262481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.43/13.44 % (3262481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.43/13.44 % (3262481)CaDiCaL version: 2.1.3 % 93.43/13.44 % (3262481)Termination reason: Inappropriate % 93.43/13.44 % (3262481)Time elapsed: 0.0000 s % 93.43/13.44 % (3262481)Peak memory usage: 10 MB % 93.43/13.44 % (3262481)Instructions burned: 1 (million) % 93.43/13.44 % (3262481)------------------------------ % 93.43/13.44 % (3262481)------------------------------ % 93.43/13.44 % (3262483)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2665456805:i=28120:bs=on:fsr=off_2907 on theBenchmark for (2907ds/28120Mi) % 93.43/13.44 % (3262473)Instruction limit reached! % 93.43/13.44 % (3262473)------------------------------ % 93.43/13.44 % (3262473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.43/13.44 % (3262473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.43/13.44 % (3262473)CaDiCaL version: 2.1.3 % 93.43/13.44 % (3262473)Termination reason: Instruction limit % 93.43/13.44 % (3262473)Termination phase: Saturation % 93.43/13.44 % (3262473)Time elapsed: 4.713 s % 93.43/13.44 % (3262473)Peak memory usage: 73 MB % 93.43/13.44 % (3262473)Instructions burned: 14134 (million) % 93.43/13.44 % (3262485)fmb+10_1_sil=256000:fmbss=7:random_seed=448287279:fmbsr=1.6:i=182295_2901 on theBenchmark for (2901ds/182295Mi) % 93.43/13.44 % (3262485)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 93.43/13.44 % (3262485)Terminated due to inappropriate strategy. % 93.43/13.44 % (3262485)------------------------------ % 93.43/13.44 % (3262485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.43/13.44 % (3262485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.43/13.44 % (3262485)CaDiCaL version: 2.1.3 % 93.43/13.44 % (3262485)Termination reason: Inappropriate % 93.43/13.44 % (3262485)Time elapsed: 0.0000 s % 93.43/13.44 % (3262485)Peak memory usage: 10 MB % 93.43/13.44 % (3262485)Instructions burned: 1 (million) % 93.43/13.44 % (3262485)------------------------------ % 93.43/13.44 % (3262485)------------------------------ % 93.43/13.44 % (3262487)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4137980338:i=44625:gsp=on_2901 on theBenchmark for (2901ds/44625Mi) % 100.58/14.40 % (3262487)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 100.58/14.40 % (3262487)Terminated due to inappropriate strategy. % 100.58/14.40 % (3262487)------------------------------ % 100.58/14.40 % (3262487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.58/14.40 % (3262487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.58/14.40 % (3262487)CaDiCaL version: 2.1.3 % 100.58/14.40 % (3262487)Termination reason: Inappropriate % 100.58/14.40 % (3262487)Time elapsed: 0.0000 s % 100.58/14.40 % (3262487)Peak memory usage: 10 MB % 100.58/14.40 % (3262487)Instructions burned: 1 (million) % 100.58/14.40 % (3262487)------------------------------ % 100.58/14.40 % (3262487)------------------------------ % 100.58/14.40 % (3262489)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=400387990:i=160505_2901 on theBenchmark for (2901ds/160505Mi) % 100.58/14.40 % (3262489)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 100.58/14.40 % (3262489)Terminated due to inappropriate strategy. % 100.58/14.40 % (3262489)------------------------------ % 100.58/14.40 % (3262489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.58/14.40 % (3262489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.58/14.40 % (3262489)CaDiCaL version: 2.1.3 % 100.58/14.40 % (3262489)Termination reason: Inappropriate % 100.58/14.40 % (3262489)Time elapsed: 0.0000 s % 100.58/14.40 % (3262489)Peak memory usage: 10 MB % 100.58/14.40 % (3262489)Instructions burned: 1 (million) % 100.58/14.40 % (3262489)------------------------------ % 100.58/14.40 % (3262489)------------------------------ % 100.58/14.40 % (3262491)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1049288636:fmbsr=1.3:i=225729_2901 on theBenchmark for (2901ds/225729Mi) % 100.58/14.40 % (3262491)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 100.58/14.40 % (3262491)Terminated due to inappropriate strategy. % 100.58/14.40 % (3262491)------------------------------ % 100.58/14.40 % (3262491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.58/14.40 % (3262491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.58/14.40 % (3262491)CaDiCaL version: 2.1.3 % 100.58/14.40 % (3262491)Termination reason: Inappropriate % 100.58/14.40 % (3262491)Time elapsed: 0.0000 s % 100.58/14.40 % (3262491)Peak memory usage: 11 MB % 100.58/14.40 % (3262491)Instructions burned: 1 (million) % 100.58/14.40 % (3262491)------------------------------ % 100.58/14.40 % (3262491)------------------------------ % 100.58/14.40 % (3262493)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3506356552:fmbsr=2:i=185024:ins=7_2901 on theBenchmark for (2901ds/185024Mi) % 100.58/14.40 % (3262493)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 100.58/14.40 % (3262493)Terminated due to inappropriate strategy. % 100.58/14.40 % (3262493)------------------------------ % 100.58/14.40 % (3262493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.58/14.40 % (3262493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.58/14.40 % (3262493)CaDiCaL version: 2.1.3 % 100.58/14.40 % (3262493)Termination reason: Inappropriate % 100.58/14.40 % (3262493)Time elapsed: 0.0000 s % 100.58/14.40 % (3262493)Peak memory usage: 11 MB % 100.58/14.40 % (3262493)Instructions burned: 1 (million) % 100.58/14.40 % (3262493)------------------------------ % 100.58/14.40 % (3262493)------------------------------ % 100.58/14.40 % (3262495)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4153463526:rtra=on_2901 on theBenchmark for (2901ds/0Mi) % 100.58/14.40 % (3262495)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 100.58/14.40 % (3262495)Terminated due to inappropriate strategy. % 100.58/14.40 % (3262495)------------------------------ % 100.58/14.40 % (3262495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.58/14.40 % (3262495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.58/14.40 % (3262495)CaDiCaL version: 2.1.3 % 100.58/14.40 % (3262495)Termination reason: Inappropriate % 100.58/14.40 % (3262495)Time elapsed: 0.0000 s % 100.58/14.40 % (3262495)Peak memory usage: 10 MB % 100.58/14.40 % (3262495)Instructions burned: 1 (million) % 100.58/14.40 % (3262495)------------------------------ % 100.58/14.40 % (3262495)------------------------------ % 100.58/14.40 % (3262497)% WARNING: option uhcvi not known. % 100.58/14.40 % (3262497)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2358057715:i=271062:add=off:rtra=on:rawr=on_2900 on theBenchmark for (2900ds/271062Mi) % 108.96/15.63 % (3262475)Instruction limit reached! % 108.96/15.63 % (3262475)------------------------------ % 108.96/15.63 % (3262475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.96/15.63 % (3262475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.96/15.63 % (3262475)CaDiCaL version: 2.1.3 % 108.96/15.63 % (3262475)Termination reason: Instruction limit % 108.96/15.63 % (3262475)Termination phase: Saturation % 108.96/15.63 % (3262475)Time elapsed: 3.803 s % 108.96/15.63 % (3262475)Peak memory usage: 204 MB % 108.96/15.63 % (3262475)Instructions burned: 15851 (million) % 108.96/15.63 % (3262499)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4232938279:i=176048:add=on:rtra=on:rawr=on_2892 on theBenchmark for (2892ds/176048Mi) % 108.96/15.63 % (3262477)Instruction limit reached! % 108.96/15.63 % (3262477)------------------------------ % 108.96/15.63 % (3262477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.96/15.63 % (3262477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.96/15.63 % (3262477)CaDiCaL version: 2.1.3 % 108.96/15.63 % (3262477)Termination reason: Instruction limit % 108.96/15.63 % (3262477)Termination phase: Saturation % 108.96/15.63 % (3262477)Time elapsed: 4.441 s % 108.96/15.63 % (3262477)Peak memory usage: 234 MB % 108.96/15.63 % (3262477)Instructions burned: 17631 (million) % 108.96/15.63 % (3262501)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2817413808:i=206:fgj=on:rtra=on_2870 on theBenchmark for (2870ds/206Mi) % 108.96/15.63 % (3262501)Instruction limit reached! % 108.96/15.63 % (3262501)------------------------------ % 108.96/15.63 % (3262501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.96/15.63 % (3262501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.96/15.63 % (3262501)CaDiCaL version: 2.1.3 % 108.96/15.63 % (3262501)Termination reason: Instruction limit % 108.96/15.63 % (3262501)Termination phase: Saturation % 108.96/15.63 % (3262501)Time elapsed: 0.069 s % 108.96/15.63 % (3262501)Peak memory usage: 13 MB % 108.96/15.63 % (3262501)Instructions burned: 209 (million) % 108.96/15.63 % (3262503)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3336942883:i=232:rtra=on_2870 on theBenchmark for (2870ds/232Mi) % 108.96/15.63 % (3262503)Instruction limit reached! % 108.96/15.63 % (3262503)------------------------------ % 108.96/15.63 % (3262503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.96/15.63 % (3262503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.96/15.63 % (3262503)CaDiCaL version: 2.1.3 % 108.96/15.63 % (3262503)Termination reason: Instruction limit % 108.96/15.63 % (3262503)Termination phase: Saturation % 108.96/15.63 % (3262503)Time elapsed: 0.078 s % 108.96/15.63 % (3262503)Peak memory usage: 13 MB % 108.96/15.63 % (3262503)Instructions burned: 234 (million) % 108.96/15.63 % (3262505)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=596141094:i=262:rtra=on_2869 on theBenchmark for (2869ds/262Mi) % 108.96/15.63 % (3262505)Instruction limit reached! % 108.96/15.63 % (3262505)------------------------------ % 108.96/15.63 % (3262505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.96/15.63 % (3262505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.96/15.63 % (3262505)CaDiCaL version: 2.1.3 % 108.96/15.63 % (3262505)Termination reason: Instruction limit % 108.96/15.63 % (3262505)Termination phase: Saturation % 108.96/15.63 % (3262505)Time elapsed: 0.088 s % 108.96/15.63 % (3262505)Peak memory usage: 14 MB % 108.96/15.63 % (3262505)Instructions burned: 263 (million) % 108.96/15.63 % (3262507)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1348072152:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2868 on theBenchmark for (2868ds/318Mi) % 108.96/15.63 % (3262507)Instruction limit reached! % 108.96/15.63 % (3262507)------------------------------ % 108.96/15.63 % (3262507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.96/15.63 % (3262507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.96/15.63 % (3262507)CaDiCaL version: 2.1.3 % 108.96/15.63 % (3262507)Termination reason: Instruction limit % 108.96/15.63 % (3262507)Termination phase: Saturation % 108.96/15.63 % (3262507)Time elapsed: 0.119 s % 108.96/15.63 % (3262507)Peak memory usage: 15 MB % 108.96/15.63 % (3262507)Instructions burned: 319 (million) % 108.96/15.63 % (3262509)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=383895696:i=1428:nm=2:rtra=on_2866 on theBenchmark for (2866ds/1428Mi) % 118.20/16.91 % (3262509)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 118.20/16.91 % (3262509)Terminated due to inappropriate strategy. % 118.20/16.91 % (3262509)------------------------------ % 118.20/16.91 % (3262509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.20/16.91 % (3262509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.20/16.91 % (3262509)CaDiCaL version: 2.1.3 % 118.20/16.91 % (3262509)Termination reason: Inappropriate % 118.20/16.91 % (3262509)Time elapsed: 0.0000 s % 118.20/16.91 % (3262509)Peak memory usage: 10 MB % 118.20/16.91 % (3262509)Instructions burned: 1 (million) % 118.20/16.91 % (3262509)------------------------------ % 118.20/16.91 % (3262509)------------------------------ % 118.20/16.91 % (3262511)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=674871556:i=262:bd=preordered:rtra=on:fsd=on_2866 on theBenchmark for (2866ds/262Mi) % 118.20/16.91 % (3262511)Instruction limit reached! % 118.20/16.91 % (3262511)------------------------------ % 118.20/16.91 % (3262511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.20/16.91 % (3262511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.20/16.91 % (3262511)CaDiCaL version: 2.1.3 % 118.20/16.91 % (3262511)Termination reason: Instruction limit % 118.20/16.91 % (3262511)Termination phase: Saturation % 118.20/16.91 % (3262511)Time elapsed: 0.093 s % 118.20/16.91 % (3262511)Peak memory usage: 14 MB % 118.20/16.91 % (3262511)Instructions burned: 262 (million) % 118.20/16.91 % (3262513)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=1766713019:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2865 on theBenchmark for (2865ds/1368Mi) % 118.20/16.91 % (3262513)Instruction limit reached! % 118.20/16.91 % (3262513)------------------------------ % 118.20/16.91 % (3262513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.20/16.91 % (3262513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.20/16.91 % (3262513)CaDiCaL version: 2.1.3 % 118.20/16.91 % (3262513)Termination reason: Instruction limit % 118.20/16.91 % (3262513)Termination phase: Saturation % 118.20/16.91 % (3262513)Time elapsed: 0.391 s % 118.20/16.91 % (3262513)Peak memory usage: 20 MB % 118.20/16.91 % (3262513)Instructions burned: 1372 (million) % 118.20/16.91 % (3262515)ott-21_1_sil=16000:si=on:fs=off:random_seed=584504626:i=360:av=off:fsr=off:rtra=on_2861 on theBenchmark for (2861ds/360Mi) % 118.20/16.91 % (3262515)Instruction limit reached! % 118.20/16.91 % (3262515)------------------------------ % 118.20/16.91 % (3262515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.20/16.91 % (3262515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.20/16.91 % (3262515)CaDiCaL version: 2.1.3 % 118.20/16.91 % (3262515)Termination reason: Instruction limit % 118.20/16.91 % (3262515)Termination phase: Saturation % 118.20/16.91 % (3262515)Time elapsed: 0.085 s % 118.20/16.91 % (3262515)Peak memory usage: 13 MB % 118.20/16.91 % (3262515)Instructions burned: 364 (million) % 118.20/16.91 % (3262517)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4105679256:i=954:bd=all:rtra=on_2860 on theBenchmark for (2860ds/954Mi) % 118.20/16.91 % (3262517)Instruction limit reached! % 118.20/16.91 % (3262517)------------------------------ % 118.20/16.91 % (3262517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.20/16.91 % (3262517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.20/16.91 % (3262517)CaDiCaL version: 2.1.3 % 118.20/16.91 % (3262517)Termination reason: Instruction limit % 118.20/16.91 % (3262517)Termination phase: Saturation % 118.20/16.91 % (3262517)Time elapsed: 0.329 s % 118.20/16.91 % (3262517)Peak memory usage: 15 MB % 118.20/16.91 % (3262517)Instructions burned: 956 (million) % 118.20/16.91 % (3262519)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1670487534:fmbsr=1.3:i=1730:ins=25:rtra=on_2857 on theBenchmark for (2857ds/1730Mi) % 118.20/16.91 % (3262519)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 118.20/16.91 % (3262519)Terminated due to inappropriate strategy. % 118.20/16.91 % (3262519)------------------------------ % 118.20/16.91 % (3262519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.20/16.91 % (3262519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.20/16.91 % (3262519)CaDiCaL version: 2.1.3 % 118.20/16.91 % (3262519)Termination reason: Inappropriate % 150.81/21.63 % (3262519)Time elapsed: 0.0000 s % 150.81/21.63 % (3262519)Peak memory usage: 10 MB % 150.81/21.63 % (3262519)Instructions burned: 1 (million) % 150.81/21.63 % (3262519)------------------------------ % 150.81/21.63 % (3262519)------------------------------ % 150.81/21.63 % (3262521)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=16579478:i=2358:rtra=on_2857 on theBenchmark for (2857ds/2358Mi) % 150.81/21.63 % (3262521)Instruction limit reached! % 150.81/21.63 % (3262521)------------------------------ % 150.81/21.63 % (3262521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.81/21.63 % (3262521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.81/21.63 % (3262521)CaDiCaL version: 2.1.3 % 150.81/21.63 % (3262521)Termination reason: Instruction limit % 150.81/21.63 % (3262521)Termination phase: Saturation % 150.81/21.63 % (3262521)Time elapsed: 0.688 s % 150.81/21.63 % (3262521)Peak memory usage: 22 MB % 150.81/21.63 % (3262521)Instructions burned: 2358 (million) % 150.81/21.63 % (3262523)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3250022276:i=1778:ins=1:rtra=on_2850 on theBenchmark for (2850ds/1778Mi) % 150.81/21.63 % (3262523)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.81/21.63 % (3262523)Terminated due to inappropriate strategy. % 150.81/21.63 % (3262523)------------------------------ % 150.81/21.63 % (3262523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.81/21.63 % (3262523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.81/21.63 % (3262523)CaDiCaL version: 2.1.3 % 150.81/21.63 % (3262523)Termination reason: Inappropriate % 150.81/21.63 % (3262523)Time elapsed: 0.0000 s % 150.81/21.63 % (3262523)Peak memory usage: 10 MB % 150.81/21.63 % (3262523)Instructions burned: 1 (million) % 150.81/21.63 % (3262523)------------------------------ % 150.81/21.63 % (3262523)------------------------------ % 150.81/21.63 % (3262525)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3843316017:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2850 on theBenchmark for (2850ds/1384Mi) % 150.81/21.63 % (3262525)Instruction limit reached! % 150.81/21.63 % (3262525)------------------------------ % 150.81/21.63 % (3262525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.81/21.63 % (3262525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.81/21.63 % (3262525)CaDiCaL version: 2.1.3 % 150.81/21.63 % (3262525)Termination reason: Instruction limit % 150.81/21.63 % (3262525)Termination phase: Saturation % 150.81/21.63 % (3262525)Time elapsed: 0.404 s % 150.81/21.63 % (3262525)Peak memory usage: 20 MB % 150.81/21.63 % (3262525)Instructions burned: 1384 (million) % 150.81/21.63 % (3262527)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3985586391:i=1758:kws=inv_precedence:fsr=off:rtra=on_2845 on theBenchmark for (2845ds/1758Mi) % 150.81/21.63 % (3262483)Instruction limit reached! % 150.81/21.63 % (3262483)------------------------------ % 150.81/21.63 % (3262483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.81/21.63 % (3262483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.81/21.63 % (3262483)CaDiCaL version: 2.1.3 % 150.81/21.63 % (3262483)Termination reason: Instruction limit % 150.81/21.63 % (3262483)Termination phase: Saturation % 150.81/21.63 % (3262483)Time elapsed: 6.257 s % 150.81/21.63 % (3262483)Peak memory usage: 23 MB % 150.81/21.63 % (3262483)Instructions burned: 28123 (million) % 150.81/21.63 % (3262529)fmb+10_1_sil=64000:si=on:random_seed=2523294451:i=44122:nm=2:rtra=on:gsp=on_2845 on theBenchmark for (2845ds/44122Mi) % 150.81/21.63 % (3262529)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.81/21.63 % (3262529)Terminated due to inappropriate strategy. % 150.81/21.63 % (3262529)------------------------------ % 150.81/21.63 % (3262529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.81/21.63 % (3262529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.81/21.63 % (3262529)CaDiCaL version: 2.1.3 % 150.81/21.63 % (3262529)Termination reason: Inappropriate % 150.81/21.63 % (3262529)Time elapsed: 0.0000 s % 150.81/21.63 % (3262529)Peak memory usage: 10 MB % 150.81/21.63 % (3262529)Instructions burned: 1 (million) % 150.81/21.63 % (3262529)------------------------------ % 150.81/21.63 % (3262529)------------------------------ % 150.81/21.63 % (3262531)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2873623992:i=19030:nm=5:rtra=on_2845 on theBenchmark for (2845ds/19030Mi) % 163.68/23.42 % (3262531)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 163.68/23.42 % (3262531)Terminated due to inappropriate strategy. % 163.68/23.42 % (3262531)------------------------------ % 163.68/23.42 % (3262531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.68/23.42 % (3262531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.68/23.42 % (3262531)CaDiCaL version: 2.1.3 % 163.68/23.42 % (3262531)Termination reason: Inappropriate % 163.68/23.42 % (3262531)Time elapsed: 0.0000 s % 163.68/23.42 % (3262531)Peak memory usage: 10 MB % 163.68/23.42 % (3262531)Instructions burned: 1 (million) % 163.68/23.42 % (3262531)------------------------------ % 163.68/23.42 % (3262531)------------------------------ % 163.68/23.42 % (3262533)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2738264787:fmbsr=1.7:i=1840:rtra=on_2844 on theBenchmark for (2844ds/1840Mi) % 163.68/23.42 % (3262533)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 163.68/23.42 % (3262533)Terminated due to inappropriate strategy. % 163.68/23.42 % (3262533)------------------------------ % 163.68/23.42 % (3262533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.68/23.42 % (3262533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.68/23.42 % (3262533)CaDiCaL version: 2.1.3 % 163.68/23.42 % (3262533)Termination reason: Inappropriate % 163.68/23.42 % (3262533)Time elapsed: 0.0000 s % 163.68/23.42 % (3262533)Peak memory usage: 10 MB % 163.68/23.42 % (3262533)Instructions burned: 1 (million) % 163.68/23.42 % (3262533)------------------------------ % 163.68/23.42 % (3262533)------------------------------ % 163.68/23.42 % (3262535)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=379469094:i=10262:rtra=on_2844 on theBenchmark for (2844ds/10262Mi) % 163.68/23.42 % (3262527)Instruction limit reached! % 163.68/23.42 % (3262527)------------------------------ % 163.68/23.42 % (3262527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.68/23.42 % (3262527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.68/23.42 % (3262527)CaDiCaL version: 2.1.3 % 163.68/23.42 % (3262527)Termination reason: Instruction limit % 163.68/23.42 % (3262527)Termination phase: Saturation % 163.68/23.42 % (3262527)Time elapsed: 0.544 s % 163.68/23.42 % (3262527)Peak memory usage: 26 MB % 163.68/23.42 % (3262527)Instructions burned: 1761 (million) % 163.68/23.42 % (3262538)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2018939755:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2840 on theBenchmark for (2840ds/2944Mi) % 163.68/23.42 % (3262538)Instruction limit reached! % 163.68/23.42 % (3262538)------------------------------ % 163.68/23.42 % (3262538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.68/23.42 % (3262538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.68/23.42 % (3262538)CaDiCaL version: 2.1.3 % 163.68/23.42 % (3262538)Termination reason: Instruction limit % 163.68/23.42 % (3262538)Termination phase: Saturation % 163.68/23.42 % (3262538)Time elapsed: 0.779 s % 163.68/23.42 % (3262538)Peak memory usage: 32 MB % 163.68/23.42 % (3262538)Instructions burned: 2948 (million) % 163.68/23.42 % (3262540)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=236694890:i=12648:rtra=on_2832 on theBenchmark for (2832ds/12648Mi) % 163.68/23.42 % (3262540)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 163.68/23.42 % (3262540)Terminated due to inappropriate strategy. % 163.68/23.42 % (3262540)------------------------------ % 163.68/23.42 % (3262540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.68/23.42 % (3262540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.68/23.42 % (3262540)CaDiCaL version: 2.1.3 % 163.68/23.42 % (3262540)Termination reason: Inappropriate % 163.68/23.42 % (3262540)Time elapsed: 0.0000 s % 163.68/23.42 % (3262540)Peak memory usage: 10 MB % 163.68/23.42 % (3262540)Instructions burned: 1 (million) % 163.68/23.42 % (3262540)------------------------------ % 163.68/23.42 % (3262540)------------------------------ % 163.68/23.42 % (3262542)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3108027088:fmbsr=2.30978:i=4348:rtra=on_2832 on theBenchmark for (2832ds/4348Mi) % 163.68/23.42 % (3262542)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 163.68/23.42 % (3262542)Terminated due to inappropriate strategy. % 163.68/23.42 % (3262542)------------------------------ % 220.94/31.59 % (3262542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.94/31.59 % (3262542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.94/31.59 % (3262542)CaDiCaL version: 2.1.3 % 220.94/31.59 % (3262542)Termination reason: Inappropriate % 220.94/31.59 % (3262542)Time elapsed: 0.0000 s % 220.94/31.59 % (3262542)Peak memory usage: 10 MB % 220.94/31.59 % (3262542)Instructions burned: 1 (million) % 220.94/31.59 % (3262542)------------------------------ % 220.94/31.59 % (3262542)------------------------------ % 220.94/31.59 % (3262544)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=4269844591:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2832 on theBenchmark for (2832ds/1738Mi) % 220.94/31.59 % (3262544)Instruction limit reached! % 220.94/31.59 % (3262544)------------------------------ % 220.94/31.59 % (3262544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.94/31.59 % (3262544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.94/31.59 % (3262544)CaDiCaL version: 2.1.3 % 220.94/31.59 % (3262544)Termination reason: Instruction limit % 220.94/31.59 % (3262544)Termination phase: Saturation % 220.94/31.59 % (3262544)Time elapsed: 0.603 s % 220.94/31.59 % (3262544)Peak memory usage: 18 MB % 220.94/31.59 % (3262544)Instructions burned: 1740 (million) % 220.94/31.59 % (3262546)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=482214301:i=10228:av=off:rtra=on_2826 on theBenchmark for (2826ds/10228Mi) % 220.94/31.59 % (3262535)Instruction limit reached! % 220.94/31.59 % (3262535)------------------------------ % 220.94/31.59 % (3262535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.94/31.59 % (3262535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.94/31.59 % (3262535)CaDiCaL version: 2.1.3 % 220.94/31.59 % (3262535)Termination reason: Instruction limit % 220.94/31.59 % (3262535)Termination phase: Saturation % 220.94/31.59 % (3262535)Time elapsed: 3.220 s % 220.94/31.59 % (3262535)Peak memory usage: 68 MB % 220.94/31.59 % (3262535)Instructions burned: 10264 (million) % 220.94/31.59 % (3262548)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=947685481:i=108564:rtra=on_2812 on theBenchmark for (2812ds/108564Mi) % 220.94/31.59 % (3262548)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 220.94/31.59 % (3262548)Terminated due to inappropriate strategy. % 220.94/31.59 % (3262548)------------------------------ % 220.94/31.59 % (3262548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.94/31.59 % (3262548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.94/31.59 % (3262548)CaDiCaL version: 2.1.3 % 220.94/31.59 % (3262548)Termination reason: Inappropriate % 220.94/31.59 % (3262548)Time elapsed: 0.0000 s % 220.94/31.59 % (3262548)Peak memory usage: 10 MB % 220.94/31.59 % (3262548)Instructions burned: 1 (million) % 220.94/31.59 % (3262548)------------------------------ % 220.94/31.59 % (3262548)------------------------------ % 220.94/31.59 % (3262550)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1162858151:i=7024:aac=none:rtra=on_2812 on theBenchmark for (2812ds/7024Mi) % 220.94/31.59 % (3262550)Instruction limit reached! % 220.94/31.59 % (3262550)------------------------------ % 220.94/31.59 % (3262550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.94/31.59 % (3262550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.94/31.59 % (3262550)CaDiCaL version: 2.1.3 % 220.94/31.59 % (3262550)Termination reason: Instruction limit % 220.94/31.59 % (3262550)Termination phase: Saturation % 220.94/31.59 % (3262550)Time elapsed: 2.151 s % 220.94/31.59 % (3262550)Peak memory usage: 58 MB % 220.94/31.59 % (3262550)Instructions burned: 7024 (million) % 220.94/31.59 % (3262552)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1755952322:i=7546:rtra=on:amm=off_2790 on theBenchmark for (2790ds/7546Mi) % 220.94/31.59 % (3262546)Instruction limit reached! % 220.94/31.59 % (3262546)------------------------------ % 220.94/31.59 % (3262546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 220.94/31.59 % (3262546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.94/31.59 % (3262546)CaDiCaL version: 2.1.3 % 220.94/31.59 % (3262546)Termination reason: Instruction limit % 220.94/31.59 % (3262546)Termination phase: Saturation % 220.94/31.59 % (3262546)Time elapsed: 4.077 s % 220.94/31.59 % (3262546)Peak memory usage: 64 MB % 220.94/31.59 % (3262546)Instructions burned: 10228 (million) % 220.94/31.59 % (3262554)ott+11_1_sil=16000:si=on:gs=on:random_seed=292326810:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2785 on theBenchmark for (2785ds/4502Mi) % 256.13/42.51 % (3262479)Instruction limit reached! % 256.13/42.51 % (3262479)------------------------------ % 256.13/42.51 % (3262479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.13/42.51 % (3262479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.13/42.51 % (3262479)CaDiCaL version: 2.1.3 % 256.13/42.51 % (3262479)Termination reason: Instruction limit % 256.13/42.51 % (3262479)Termination phase: Saturation % 256.13/42.51 % (3262479)Time elapsed: 13.369 s % 256.13/42.51 % (3262479)Peak memory usage: 307 MB % 256.13/42.51 % (3262479)Instructions burned: 53301 (million) % 256.13/42.51 % (3262556)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=1234050541:fmbsr=1.6:i=135068:rtra=on_2777 on theBenchmark for (2777ds/135068Mi) % 256.13/42.51 % (3262556)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 256.13/42.51 % (3262556)Terminated due to inappropriate strategy. % 256.13/42.51 % (3262556)------------------------------ % 256.13/42.51 % (3262556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.13/42.51 % (3262556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.13/42.51 % (3262556)CaDiCaL version: 2.1.3 % 256.13/42.51 % (3262556)Termination reason: Inappropriate % 256.13/42.51 % (3262556)Time elapsed: 0.0000 s % 256.13/42.51 % (3262556)Peak memory usage: 10 MB % 256.13/42.51 % (3262556)Instructions burned: 1 (million) % 256.13/42.51 % (3262556)------------------------------ % 256.13/42.51 % (3262556)------------------------------ % 256.13/42.51 % (3262558)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1829798641:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2777 on theBenchmark for (2777ds/9182Mi) % 256.13/42.51 % (3262389)Instruction limit reached! % 256.13/42.51 % (3262389)------------------------------ % 256.13/42.51 % (3262389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.13/42.51 % (3262389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.13/42.51 % (3262389)CaDiCaL version: 2.1.3 % 256.13/42.51 % (3262389)Termination reason: Instruction limit % 256.13/42.51 % (3262389)Termination phase: Saturation % 256.13/42.51 % (3262389)Time elapsed: 22.383 s % 256.13/42.51 % (3262389)Peak memory usage: 1296 MB % 256.13/42.51 % (3262389)Instructions burned: 88026 (million) % 256.13/42.51 % (3262560)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=599959098:i=58680:rtra=on_2774 on theBenchmark for (2774ds/58680Mi) % 256.13/42.51 % (3262554)Instruction limit reached! % 256.13/42.51 % (3262554)------------------------------ % 256.13/42.51 % (3262554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.13/42.51 % (3262554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.13/42.51 % (3262554)CaDiCaL version: 2.1.3 % 256.13/42.51 % (3262554)Termination reason: Instruction limit % 256.13/42.51 % (3262554)Termination phase: Saturation % 256.13/42.51 % (3262554)Time elapsed: 1.412 s % 256.13/42.51 % (3262554)Peak memory usage: 33 MB % 256.13/42.51 % (3262554)Instructions burned: 4504 (million) % 256.13/42.51 % (3262562)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=3070841016:i=10422:rtra=on_2770 on theBenchmark for (2770ds/10422Mi) % 256.13/42.51 % (3262552)Instruction limit reached! % 256.13/42.51 % (3262552)------------------------------ % 256.13/42.51 % (3262552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.13/42.51 % (3262552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.13/42.51 % (3262552)CaDiCaL version: 2.1.3 % 256.13/42.51 % (3262552)Termination reason: Instruction limit % 256.13/42.51 % (3262552)Termination phase: Saturation % 256.13/42.51 % (3262552)Time elapsed: 2.333 s % 256.13/42.51 % (3262552)Peak memory usage: 50 MB % 256.13/42.51 % (3262552)Instructions burned: 7548 (million) % 256.13/42.51 % (3262564)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=1508687926:i=10994:nm=2:rtra=on_2767 on theBenchmark for (2767ds/10994Mi) % 256.13/42.51 % (3262564)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 256.13/42.51 % (3262564)Terminated due to inappropriate strategy. % 256.13/42.51 % (3262564)------------------------------ % 256.13/42.51 % (3262564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.13/42.51 % (3262564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.13/42.51 % (3262564)CaDiCaL version: 2.1.3 % 256.13/42.51 % (3262564)Termination reason: Inappropriate % 256.13/42.51 % Terminated % 300.57/42.83 % Vampire exiting % 300.57/42.83 Terminated %------------------------------------------------------------------------------