%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC454_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n019.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:01 PM UTC 2026 % Result : Timeout 286.28s 40.69s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC454_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 % Computer : n019.cluster.edu % 0.09/0.23 % Model : x86_64 x86_64 % 0.09/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.23 % Memory : 8046.5625MB % 0.09/0.23 % OS : Linux 6.8.0-71-generic % 0.09/0.23 % CPULimit : 300 % 0.09/0.23 % WCLimit : 300 % 0.09/0.23 % DateTime : Mon Sep 28 09:38:43 UTC 2026 % 0.09/0.23 % CPUTime : % 0.09/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.26 Running first-order model finding % 0.09/0.26 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.65/0.89 % (3878315)Will run a generic schedule for satisfiability detection. % 3.65/0.89 % (3878323)dis+10_1_sil=32000:sp=arity:random_seed=496246844:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.65/0.89 % (3878321)% WARNING: option uhcvi not known. % 3.65/0.89 % (3878320)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3393235755_2999 on theBenchmark for (2999ds/0Mi) % 3.65/0.89 % (3878321)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3672832380:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.65/0.89 % (3878322)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1708534254:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.65/0.89 % (3878324)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2839123691:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.65/0.89 % (3878325)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=877778526:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.65/0.89 % (3878326)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=758073755:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.65/0.89 % (3878320)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.65/0.89 % (3878320)Terminated due to inappropriate strategy. % 3.65/0.89 % (3878320)------------------------------ % 3.65/0.89 % (3878320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.89 % (3878320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.89 % (3878320)CaDiCaL version: 2.1.3 % 3.65/0.89 % (3878320)Termination reason: Inappropriate % 3.65/0.89 % (3878320)Time elapsed: 0.001 s % 3.65/0.89 % (3878320)Peak memory usage: 10 MB % 3.65/0.89 % (3878320)Instructions burned: 1 (million) % 3.65/0.89 % (3878320)------------------------------ % 3.65/0.89 % (3878320)------------------------------ % 3.65/0.89 % (3878334)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=404322418:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.65/0.89 % (3878334)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.65/0.89 % (3878334)Terminated due to inappropriate strategy. % 3.65/0.89 % (3878334)------------------------------ % 3.65/0.89 % (3878334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.89 % (3878334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.89 % (3878334)CaDiCaL version: 2.1.3 % 3.65/0.89 % (3878334)Termination reason: Inappropriate % 3.65/0.89 % (3878334)Time elapsed: 0.001 s % 3.65/0.89 % (3878334)Peak memory usage: 10 MB % 3.65/0.89 % (3878334)Instructions burned: 1 (million) % 3.65/0.89 % (3878334)------------------------------ % 3.65/0.89 % (3878334)------------------------------ % 3.65/0.89 % (3878323)Instruction limit reached! % 3.65/0.89 % (3878323)------------------------------ % 3.65/0.89 % (3878323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.89 % (3878323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.89 % (3878323)CaDiCaL version: 2.1.3 % 3.65/0.89 % (3878323)Termination reason: Instruction limit % 3.65/0.89 % (3878323)Termination phase: Saturation % 3.65/0.89 % (3878323)Time elapsed: 0.034 s % 3.65/0.89 % (3878323)Peak memory usage: 12 MB % 3.65/0.89 % (3878323)Instructions burned: 104 (million) % 3.65/0.89 % (3878336)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1406931092:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.65/0.89 % (3878337)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=2770863533:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.65/0.89 % (3878324)Instruction limit reached! % 3.65/0.89 % (3878324)------------------------------ % 3.65/0.89 % (3878324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.89 % (3878324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.89 % (3878324)CaDiCaL version: 2.1.3 % 3.65/0.89 % (3878324)Termination reason: Instruction limit % 3.65/0.89 % (3878324)Termination phase: Saturation % 3.65/0.89 % (3878324)Time elapsed: 0.072 s % 3.65/0.89 % (3878324)Peak memory usage: 13 MB % 3.65/0.89 % (3878324)Instructions burned: 117 (million) % 3.65/0.89 % (3878325)Instruction limit reached! % 3.65/0.89 % (3878325)------------------------------ % 3.65/0.89 % (3878325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.43/1.08 % (3878325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.08 % (3878325)CaDiCaL version: 2.1.3 % 5.43/1.08 % (3878325)Termination reason: Instruction limit % 5.43/1.08 % (3878325)Termination phase: Saturation % 5.43/1.08 % (3878325)Time elapsed: 0.078 s % 5.43/1.08 % (3878325)Peak memory usage: 13 MB % 5.43/1.08 % (3878325)Instructions burned: 131 (million) % 5.43/1.08 % (3878340)ott-21_1_sil=16000:fs=off:random_seed=1523183840:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.43/1.08 % (3878341)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1559190923:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.43/1.08 % (3878326)Instruction limit reached! % 5.43/1.08 % (3878326)------------------------------ % 5.43/1.08 % (3878326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.43/1.08 % (3878326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.08 % (3878326)CaDiCaL version: 2.1.3 % 5.43/1.08 % (3878326)Termination reason: Instruction limit % 5.43/1.08 % (3878326)Termination phase: Saturation % 5.43/1.08 % (3878326)Time elapsed: 0.107 s % 5.43/1.08 % (3878326)Peak memory usage: 13 MB % 5.43/1.08 % (3878326)Instructions burned: 160 (million) % 5.43/1.08 % (3878336)Instruction limit reached! % 5.43/1.08 % (3878336)------------------------------ % 5.43/1.08 % (3878336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.43/1.08 % (3878336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.08 % (3878336)CaDiCaL version: 2.1.3 % 5.43/1.08 % (3878336)Termination reason: Instruction limit % 5.43/1.08 % (3878336)Termination phase: Saturation % 5.43/1.08 % (3878336)Time elapsed: 0.079 s % 5.43/1.08 % (3878336)Peak memory usage: 12 MB % 5.43/1.08 % (3878336)Instructions burned: 131 (million) % 5.43/1.08 % (3878344)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2519446830:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.43/1.08 % (3878344)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.43/1.08 % (3878344)Terminated due to inappropriate strategy. % 5.43/1.08 % (3878344)------------------------------ % 5.43/1.08 % (3878344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.43/1.08 % (3878344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.08 % (3878344)CaDiCaL version: 2.1.3 % 5.43/1.08 % (3878344)Termination reason: Inappropriate % 5.43/1.08 % (3878344)Time elapsed: 0.001 s % 5.43/1.08 % (3878344)Peak memory usage: 10 MB % 5.43/1.08 % (3878344)Instructions burned: 1 (million) % 5.43/1.08 % (3878344)------------------------------ % 5.43/1.08 % (3878344)------------------------------ % 5.43/1.08 % (3878345)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1770642602:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.43/1.08 % (3878347)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=43079204:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.43/1.08 % (3878347)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.43/1.08 % (3878347)Terminated due to inappropriate strategy. % 5.43/1.08 % (3878347)------------------------------ % 5.43/1.08 % (3878347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.43/1.08 % (3878347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.08 % (3878347)CaDiCaL version: 2.1.3 % 5.43/1.08 % (3878347)Termination reason: Inappropriate % 5.43/1.08 % (3878347)Time elapsed: 0.001 s % 5.43/1.08 % (3878347)Peak memory usage: 11 MB % 5.43/1.08 % (3878347)Instructions burned: 1 (million) % 5.43/1.08 % (3878347)------------------------------ % 5.43/1.08 % (3878347)------------------------------ % 5.43/1.08 % (3878350)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=1054486617: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) % 5.43/1.08 % (3878340)Instruction limit reached! % 5.43/1.08 % (3878340)------------------------------ % 5.43/1.08 % (3878340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.43/1.08 % (3878340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.43/1.08 % (3878340)CaDiCaL version: 2.1.3 % 5.43/1.08 % (3878340)Termination reason: Instruction limit % 5.43/1.08 % (3878340)Termination phase: Saturation % 22.22/3.49 % (3878340)Time elapsed: 0.081 s % 22.22/3.49 % (3878340)Peak memory usage: 12 MB % 22.22/3.49 % (3878340)Instructions burned: 181 (million) % 22.22/3.49 % (3878352)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3829591600:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.22/3.49 % (3878341)Instruction limit reached! % 22.22/3.49 % (3878341)------------------------------ % 22.22/3.49 % (3878341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.22/3.49 % (3878341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.22/3.49 % (3878341)CaDiCaL version: 2.1.3 % 22.22/3.49 % (3878341)Termination reason: Instruction limit % 22.22/3.49 % (3878341)Termination phase: Saturation % 22.22/3.49 % (3878341)Time elapsed: 0.274 s % 22.22/3.49 % (3878341)Peak memory usage: 13 MB % 22.22/3.49 % (3878341)Instructions burned: 478 (million) % 22.22/3.49 % (3878354)fmb+10_1_sil=64000:random_seed=637106614:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 22.22/3.49 % (3878354)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.22/3.50 % (3878354)Terminated due to inappropriate strategy. % 22.22/3.50 % (3878354)------------------------------ % 22.22/3.50 % (3878354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.22/3.50 % (3878354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.22/3.50 % (3878354)CaDiCaL version: 2.1.3 % 22.22/3.50 % (3878354)Termination reason: Inappropriate % 22.22/3.50 % (3878354)Time elapsed: 0.001 s % 22.22/3.50 % (3878354)Peak memory usage: 10 MB % 22.22/3.50 % (3878354)Instructions burned: 1 (million) % 22.22/3.50 % (3878354)------------------------------ % 22.22/3.50 % (3878354)------------------------------ % 22.22/3.50 % (3878356)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1853583412:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.22/3.50 % (3878356)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.22/3.50 % (3878356)Terminated due to inappropriate strategy. % 22.22/3.50 % (3878356)------------------------------ % 22.22/3.50 % (3878356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.22/3.50 % (3878356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.22/3.50 % (3878356)CaDiCaL version: 2.1.3 % 22.22/3.50 % (3878356)Termination reason: Inappropriate % 22.22/3.50 % (3878356)Time elapsed: 0.001 s % 22.22/3.50 % (3878356)Peak memory usage: 11 MB % 22.22/3.50 % (3878356)Instructions burned: 1 (million) % 22.22/3.50 % (3878356)------------------------------ % 22.22/3.50 % (3878356)------------------------------ % 22.22/3.50 % (3878337)Instruction limit reached! % 22.22/3.50 % (3878337)------------------------------ % 22.22/3.50 % (3878337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.22/3.50 % (3878337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.22/3.50 % (3878337)CaDiCaL version: 2.1.3 % 22.22/3.50 % (3878337)Termination reason: Instruction limit % 22.22/3.50 % (3878337)Termination phase: Saturation % 22.22/3.50 % (3878337)Time elapsed: 0.372 s % 22.22/3.50 % (3878337)Peak memory usage: 17 MB % 22.22/3.50 % (3878337)Instructions burned: 685 (million) % 22.22/3.50 % (3878358)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2558411707:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.22/3.50 % (3878358)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.22/3.50 % (3878358)Terminated due to inappropriate strategy. % 22.22/3.50 % (3878358)------------------------------ % 22.22/3.50 % (3878358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.22/3.50 % (3878358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.22/3.50 % (3878358)CaDiCaL version: 2.1.3 % 22.22/3.50 % (3878358)Termination reason: Inappropriate % 22.22/3.50 % (3878358)Time elapsed: 0.001 s % 22.22/3.50 % (3878358)Peak memory usage: 10 MB % 22.22/3.50 % (3878358)Instructions burned: 1 (million) % 22.22/3.50 % (3878358)------------------------------ % 22.22/3.50 % (3878358)------------------------------ % 22.22/3.50 % (3878359)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3418153686:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 22.22/3.50 % (3878361)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=100346839:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 22.22/3.50 % (3878350)Instruction limit reached! % 22.22/3.50 % (3878350)------------------------------ % 35.69/5.34 % (3878350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.69/5.34 % (3878350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.34 % (3878350)CaDiCaL version: 2.1.3 % 35.69/5.34 % (3878350)Termination reason: Instruction limit % 35.69/5.34 % (3878350)Termination phase: Saturation % 35.69/5.34 % (3878350)Time elapsed: 0.419 s % 35.69/5.34 % (3878350)Peak memory usage: 19 MB % 35.69/5.34 % (3878350)Instructions burned: 694 (million) % 35.69/5.34 % (3878364)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1864483606:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 35.69/5.34 % (3878364)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.69/5.34 % (3878364)Terminated due to inappropriate strategy. % 35.69/5.34 % (3878364)------------------------------ % 35.69/5.34 % (3878364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.69/5.34 % (3878364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.34 % (3878364)CaDiCaL version: 2.1.3 % 35.69/5.34 % (3878364)Termination reason: Inappropriate % 35.69/5.34 % (3878364)Time elapsed: 0.001 s % 35.69/5.34 % (3878364)Peak memory usage: 10 MB % 35.69/5.34 % (3878364)Instructions burned: 1 (million) % 35.69/5.34 % (3878364)------------------------------ % 35.69/5.34 % (3878364)------------------------------ % 35.69/5.34 % (3878366)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3734714898:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 35.69/5.34 % (3878366)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.69/5.34 % (3878366)Terminated due to inappropriate strategy. % 35.69/5.34 % (3878366)------------------------------ % 35.69/5.34 % (3878366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.69/5.34 % (3878366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.34 % (3878366)CaDiCaL version: 2.1.3 % 35.69/5.34 % (3878366)Termination reason: Inappropriate % 35.69/5.34 % (3878366)Time elapsed: 0.001 s % 35.69/5.34 % (3878366)Peak memory usage: 10 MB % 35.69/5.34 % (3878366)Instructions burned: 1 (million) % 35.69/5.34 % (3878366)------------------------------ % 35.69/5.34 % (3878366)------------------------------ % 35.69/5.34 % (3878368)ott-2_1_sil=16000:newcnf=on:random_seed=256745614:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 35.69/5.34 % (3878352)Instruction limit reached! % 35.69/5.34 % (3878352)------------------------------ % 35.69/5.34 % (3878352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.69/5.34 % (3878352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.34 % (3878352)CaDiCaL version: 2.1.3 % 35.69/5.34 % (3878352)Termination reason: Instruction limit % 35.69/5.34 % (3878352)Termination phase: Saturation % 35.69/5.34 % (3878352)Time elapsed: 0.494 s % 35.69/5.34 % (3878352)Peak memory usage: 19 MB % 35.69/5.34 % (3878352)Instructions burned: 879 (million) % 35.69/5.34 % (3878370)ott+10_1_sil=32000:tgt=ground:random_seed=3263109868:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 35.69/5.34 % (3878345)Instruction limit reached! % 35.69/5.34 % (3878345)------------------------------ % 35.69/5.34 % (3878345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.69/5.34 % (3878345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.34 % (3878345)CaDiCaL version: 2.1.3 % 35.69/5.34 % (3878345)Termination reason: Instruction limit % 35.69/5.34 % (3878345)Termination phase: Saturation % 35.69/5.34 % (3878345)Time elapsed: 0.620 s % 35.69/5.34 % (3878345)Peak memory usage: 17 MB % 35.69/5.34 % (3878345)Instructions burned: 1179 (million) % 35.69/5.34 % (3878372)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3002342028:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 35.69/5.34 % (3878372)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.69/5.34 % (3878372)Terminated due to inappropriate strategy. % 35.69/5.34 % (3878372)------------------------------ % 35.69/5.34 % (3878372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.69/5.34 % (3878372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.69/5.34 % (3878372)CaDiCaL version: 2.1.3 % 35.69/5.34 % (3878372)Termination reason: Inappropriate % 35.69/5.34 % (3878372)Time elapsed: 0.001 s % 35.69/5.34 % (3878372)Peak memory usage: 10 MB % 35.69/5.34 % (3878372)Instructions burned: 1 (million) % 106.67/15.33 % (3878372)------------------------------ % 106.67/15.33 % (3878372)------------------------------ % 106.67/15.33 % (3878374)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=103775997:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 106.67/15.33 % (3878368)Instruction limit reached! % 106.67/15.33 % (3878368)------------------------------ % 106.67/15.33 % (3878368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.67/15.33 % (3878368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.67/15.33 % (3878368)CaDiCaL version: 2.1.3 % 106.67/15.33 % (3878368)Termination reason: Instruction limit % 106.67/15.33 % (3878368)Termination phase: Saturation % 106.67/15.33 % (3878368)Time elapsed: 0.457 s % 106.67/15.33 % (3878368)Peak memory usage: 17 MB % 106.67/15.33 % (3878368)Instructions burned: 869 (million) % 106.67/15.33 % (3878376)dis+21_1_sil=32000:sas=cadical:random_seed=997212362:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 106.67/15.33 % (3878361)Instruction limit reached! % 106.67/15.33 % (3878361)------------------------------ % 106.67/15.33 % (3878361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.67/15.33 % (3878361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.67/15.33 % (3878361)CaDiCaL version: 2.1.3 % 106.67/15.33 % (3878361)Termination reason: Instruction limit % 106.67/15.33 % (3878361)Termination phase: Saturation % 106.67/15.33 % (3878361)Time elapsed: 0.868 s % 106.67/15.33 % (3878361)Peak memory usage: 28 MB % 106.67/15.33 % (3878361)Instructions burned: 1473 (million) % 106.67/15.33 % (3878378)ott+11_1_sil=16000:gs=on:random_seed=4259938341:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 106.67/15.33 % (3878378)Instruction limit reached! % 106.67/15.33 % (3878378)------------------------------ % 106.67/15.33 % (3878378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.67/15.33 % (3878378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.67/15.33 % (3878378)CaDiCaL version: 2.1.3 % 106.67/15.33 % (3878378)Termination reason: Instruction limit % 106.67/15.33 % (3878378)Termination phase: Saturation % 106.67/15.33 % (3878378)Time elapsed: 1.235 s % 106.67/15.33 % (3878378)Peak memory usage: 22 MB % 106.67/15.33 % (3878378)Instructions burned: 2253 (million) % 106.67/15.33 % (3878380)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1629171873:fmbsr=1.6:i=67534_2973 on theBenchmark for (2973ds/67534Mi) % 106.67/15.33 % (3878380)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.67/15.33 % (3878380)Terminated due to inappropriate strategy. % 106.67/15.33 % (3878380)------------------------------ % 106.67/15.33 % (3878380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.67/15.33 % (3878380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.67/15.33 % (3878380)CaDiCaL version: 2.1.3 % 106.67/15.33 % (3878380)Termination reason: Inappropriate % 106.67/15.33 % (3878380)Time elapsed: 0.001 s % 106.67/15.33 % (3878380)Peak memory usage: 10 MB % 106.67/15.33 % (3878380)Instructions burned: 1 (million) % 106.67/15.33 % (3878380)------------------------------ % 106.67/15.33 % (3878380)------------------------------ % 106.67/15.33 % (3878382)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=194622317:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2973 on theBenchmark for (2973ds/4591Mi) % 106.67/15.33 % (3878374)Instruction limit reached! % 106.67/15.33 % (3878374)------------------------------ % 106.67/15.33 % (3878374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.67/15.33 % (3878374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.67/15.33 % (3878374)CaDiCaL version: 2.1.3 % 106.67/15.33 % (3878374)Termination reason: Instruction limit % 106.67/15.33 % (3878374)Termination phase: Saturation % 106.67/15.33 % (3878374)Time elapsed: 1.871 s % 106.67/15.33 % (3878374)Peak memory usage: 32 MB % 106.67/15.33 % (3878374)Instructions burned: 3513 (million) % 106.67/15.33 % (3878384)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1636450708:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 106.67/15.33 % (3878359)Instruction limit reached! % 106.67/15.33 % (3878359)------------------------------ % 106.67/15.33 % (3878359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.67/15.33 % (3878359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.67/15.33 % (3878359)CaDiCaL version: 2.1.3 % 106.67/15.33 % (3878359)Termination reason: Instruction limit % 130.11/18.63 % (3878359)Termination phase: Saturation % 130.11/18.63 % (3878359)Time elapsed: 2.754 s % 130.11/18.63 % (3878359)Peak memory usage: 41 MB % 130.11/18.63 % (3878359)Instructions burned: 5131 (million) % 130.11/18.63 % (3878386)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=613043883:i=5211_2967 on theBenchmark for (2967ds/5211Mi) % 130.11/18.63 % (3878376)Instruction limit reached! % 130.11/18.63 % (3878376)------------------------------ % 130.11/18.63 % (3878376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.11/18.63 % (3878376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.11/18.63 % (3878376)CaDiCaL version: 2.1.3 % 130.11/18.63 % (3878376)Termination reason: Instruction limit % 130.11/18.63 % (3878376)Termination phase: Saturation % 130.11/18.63 % (3878376)Time elapsed: 2.090 s % 130.11/18.63 % (3878376)Peak memory usage: 33 MB % 130.11/18.63 % (3878376)Instructions burned: 3773 (million) % 130.11/18.63 % (3878388)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2909175931:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 130.11/18.63 % (3878388)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.11/18.63 % (3878388)Terminated due to inappropriate strategy. % 130.11/18.63 % (3878388)------------------------------ % 130.11/18.63 % (3878388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.11/18.63 % (3878388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.11/18.63 % (3878388)CaDiCaL version: 2.1.3 % 130.11/18.63 % (3878388)Termination reason: Inappropriate % 130.11/18.63 % (3878388)Time elapsed: 0.001 s % 130.11/18.63 % (3878388)Peak memory usage: 10 MB % 130.11/18.63 % (3878388)Instructions burned: 1 (million) % 130.11/18.63 % (3878388)------------------------------ % 130.11/18.63 % (3878388)------------------------------ % 130.11/18.63 % (3878390)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3780916382:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 130.11/18.63 % (3878390)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.11/18.63 % (3878390)Terminated due to inappropriate strategy. % 130.11/18.63 % (3878390)------------------------------ % 130.11/18.63 % (3878390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.11/18.63 % (3878390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.11/18.63 % (3878390)CaDiCaL version: 2.1.3 % 130.11/18.63 % (3878390)Termination reason: Inappropriate % 130.11/18.63 % (3878390)Time elapsed: 0.001 s % 130.11/18.63 % (3878390)Peak memory usage: 10 MB % 130.11/18.63 % (3878390)Instructions burned: 1 (million) % 130.11/18.63 % (3878390)------------------------------ % 130.11/18.63 % (3878390)------------------------------ % 130.11/18.63 % (3878392)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=431927898:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 130.11/18.63 % (3878392)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.11/18.63 % (3878392)Terminated due to inappropriate strategy. % 130.11/18.63 % (3878392)------------------------------ % 130.11/18.63 % (3878392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.11/18.63 % (3878392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.11/18.63 % (3878392)CaDiCaL version: 2.1.3 % 130.11/18.63 % (3878392)Termination reason: Inappropriate % 130.11/18.63 % (3878392)Time elapsed: 0.001 s % 130.11/18.63 % (3878392)Peak memory usage: 10 MB % 130.11/18.63 % (3878392)Instructions burned: 1 (million) % 130.11/18.63 % (3878392)------------------------------ % 130.11/18.63 % (3878392)------------------------------ % 130.11/18.63 % (3878394)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3890703693:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 130.11/18.63 % (3878370)Instruction limit reached! % 130.11/18.63 % (3878370)------------------------------ % 130.11/18.63 % (3878370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.11/18.63 % (3878370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.11/18.63 % (3878370)CaDiCaL version: 2.1.3 % 130.11/18.63 % (3878370)Termination reason: Instruction limit % 130.11/18.63 % (3878370)Termination phase: Saturation % 130.11/18.63 % (3878370)Time elapsed: 3.171 s % 130.11/18.63 % (3878370)Peak memory usage: 33 MB % 130.11/18.63 % (3878370)Instructions burned: 5114 (million) % 130.11/18.63 % (3878396)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1714822998:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi) % 130.11/18.63 % (3878382)Instruction limit reached! % 130.86/18.74 % (3878382)------------------------------ % 130.86/18.74 % (3878382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.86/18.74 % (3878382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.86/18.74 % (3878382)CaDiCaL version: 2.1.3 % 130.86/18.74 % (3878382)Termination reason: Instruction limit % 130.86/18.74 % (3878382)Termination phase: Saturation % 130.86/18.74 % (3878382)Time elapsed: 2.412 s % 130.86/18.74 % (3878382)Peak memory usage: 45 MB % 130.86/18.74 % (3878382)Instructions burned: 4593 (million) % 130.86/18.74 % (3878398)dis+10_16:1_sil=16000:random_seed=507546887:i=9155:fsr=off_2949 on theBenchmark for (2949ds/9155Mi) % 130.86/18.74 % (3878386)Instruction limit reached! % 130.86/18.74 % (3878386)------------------------------ % 130.86/18.74 % (3878386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.86/18.74 % (3878386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.86/18.74 % (3878386)CaDiCaL version: 2.1.3 % 130.86/18.74 % (3878386)Termination reason: Instruction limit % 130.86/18.74 % (3878386)Termination phase: Saturation % 130.86/18.74 % (3878386)Time elapsed: 2.579 s % 130.86/18.74 % (3878386)Peak memory usage: 41 MB % 130.86/18.74 % (3878386)Instructions burned: 5212 (million) % 130.86/18.74 % (3878400)ott-3_8_sil=64000:random_seed=1683900917:i=20139:bs=on_2941 on theBenchmark for (2941ds/20139Mi) % 130.86/18.74 % (3878396)Instruction limit reached! % 130.86/18.74 % (3878396)------------------------------ % 130.86/18.74 % (3878396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.86/18.74 % (3878396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.86/18.74 % (3878396)CaDiCaL version: 2.1.3 % 130.86/18.74 % (3878396)Termination reason: Instruction limit % 130.86/18.74 % (3878396)Termination phase: Saturation % 130.86/18.74 % (3878396)Time elapsed: 5.091 s % 130.86/18.74 % (3878396)Peak memory usage: 58 MB % 130.86/18.74 % (3878396)Instructions burned: 8173 (million) % 130.86/18.74 % (3878402)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3457574382:fmbsr=2:i=32576_2909 on theBenchmark for (2909ds/32576Mi) % 130.86/18.74 % (3878402)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.86/18.74 % (3878402)Terminated due to inappropriate strategy. % 130.86/18.74 % (3878402)------------------------------ % 130.86/18.74 % (3878402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.86/18.74 % (3878402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.86/18.74 % (3878402)CaDiCaL version: 2.1.3 % 130.86/18.74 % (3878402)Termination reason: Inappropriate % 130.86/18.74 % (3878402)Time elapsed: 0.001 s % 130.86/18.74 % (3878402)Peak memory usage: 10 MB % 130.86/18.74 % (3878402)Instructions burned: 1 (million) % 130.86/18.74 % (3878402)------------------------------ % 130.86/18.74 % (3878402)------------------------------ % 130.86/18.74 % (3878404)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=331052215:i=11404_2909 on theBenchmark for (2909ds/11404Mi) % 130.86/18.74 % (3878398)Instruction limit reached! % 130.86/18.74 % (3878398)------------------------------ % 130.86/18.74 % (3878398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.86/18.74 % (3878398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.86/18.74 % (3878398)CaDiCaL version: 2.1.3 % 130.86/18.74 % (3878398)Termination reason: Instruction limit % 130.86/18.74 % (3878398)Termination phase: Saturation % 130.86/18.74 % (3878398)Time elapsed: 4.618 s % 130.86/18.74 % (3878398)Peak memory usage: 51 MB % 130.86/18.74 % (3878398)Instructions burned: 9156 (million) % 130.86/18.74 % (3878406)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2709446354:i=14134_2902 on theBenchmark for (2902ds/14134Mi) % 130.86/18.74 % (3878394)Instruction limit reached! % 130.86/18.74 % (3878394)------------------------------ % 130.86/18.74 % (3878394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.86/18.74 % (3878394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.86/18.74 % (3878394)CaDiCaL version: 2.1.3 % 130.86/18.74 % (3878394)Termination reason: Instruction limit % 130.86/18.74 % (3878394)Termination phase: Saturation % 130.86/18.74 % (3878394)Time elapsed: 8.943 s % 130.86/18.74 % (3878394)Peak memory usage: 58 MB % 130.86/18.74 % (3878394)Instructions burned: 22566 (million) % 130.86/18.74 % (3878408)dis+33_16_sil=32000:sac=on:random_seed=3462452445:i=15851:nm=0_2877 on theBenchmark for (2877ds/15851Mi) % 130.86/18.74 % (3878384)Instruction limit reached! % 130.86/18.74 % (3878384)------------------------------ % 130.86/18.74 % (3878384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.74/24.29 % (3878384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.74/24.29 % (3878384)CaDiCaL version: 2.1.3 % 169.74/24.29 % (3878384)Termination reason: Instruction limit % 169.74/24.29 % (3878384)Termination phase: Saturation % 169.74/24.29 % (3878384)Time elapsed: 12.337 s % 169.74/24.29 % (3878384)Peak memory usage: 174 MB % 169.74/24.29 % (3878384)Instructions burned: 29341 (million) % 169.74/24.29 % (3878410)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3115479228:avsq=on:i=17627:add=on:amm=off_2849 on theBenchmark for (2849ds/17627Mi) % 169.74/24.29 % (3878404)Instruction limit reached! % 169.74/24.29 % (3878404)------------------------------ % 169.74/24.29 % (3878404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.74/24.29 % (3878404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.74/24.29 % (3878404)CaDiCaL version: 2.1.3 % 169.74/24.29 % (3878404)Termination reason: Instruction limit % 169.74/24.29 % (3878404)Termination phase: Saturation % 169.74/24.29 % (3878404)Time elapsed: 6.981 s % 169.74/24.29 % (3878404)Peak memory usage: 64 MB % 169.74/24.29 % (3878404)Instructions burned: 11404 (million) % 169.74/24.29 % (3878412)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3563104237:s2a=on:i=53295_2839 on theBenchmark for (2839ds/53295Mi) % 169.74/24.29 % (3878400)Instruction limit reached! % 169.74/24.29 % (3878400)------------------------------ % 169.74/24.29 % (3878400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.74/24.29 % (3878400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.74/24.29 % (3878400)CaDiCaL version: 2.1.3 % 169.74/24.29 % (3878400)Termination reason: Instruction limit % 169.74/24.29 % (3878400)Termination phase: Saturation % 169.74/24.29 % (3878400)Time elapsed: 11.522 s % 169.74/24.29 % (3878400)Peak memory usage: 78 MB % 169.74/24.29 % (3878400)Instructions burned: 20140 (million) % 169.74/24.29 % (3878414)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3533478015:i=26857:ins=20_2826 on theBenchmark for (2826ds/26857Mi) % 169.74/24.29 % (3878414)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.74/24.29 % (3878414)Terminated due to inappropriate strategy. % 169.74/24.29 % (3878414)------------------------------ % 169.74/24.29 % (3878414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.74/24.29 % (3878414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.74/24.29 % (3878414)CaDiCaL version: 2.1.3 % 169.74/24.29 % (3878414)Termination reason: Inappropriate % 169.74/24.29 % (3878414)Time elapsed: 0.001 s % 169.74/24.29 % (3878414)Peak memory usage: 10 MB % 169.74/24.29 % (3878414)Instructions burned: 1 (million) % 169.74/24.29 % (3878414)------------------------------ % 169.74/24.29 % (3878414)------------------------------ % 169.74/24.29 % (3878416)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4286267933:i=28120:bs=on:fsr=off_2825 on theBenchmark for (2825ds/28120Mi) % 169.74/24.29 % (3878406)Instruction limit reached! % 169.74/24.29 % (3878406)------------------------------ % 169.74/24.29 % (3878406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.74/24.29 % (3878406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.74/24.29 % (3878406)CaDiCaL version: 2.1.3 % 169.74/24.29 % (3878406)Termination reason: Instruction limit % 169.74/24.29 % (3878406)Termination phase: Saturation % 169.74/24.29 % (3878406)Time elapsed: 8.576 s % 169.74/24.29 % (3878406)Peak memory usage: 78 MB % 169.74/24.29 % (3878406)Instructions burned: 14135 (million) % 169.74/24.29 % (3878418)fmb+10_1_sil=256000:fmbss=7:random_seed=1109116286:fmbsr=1.6:i=182295_2816 on theBenchmark for (2816ds/182295Mi) % 169.74/24.29 % (3878418)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.74/24.29 % (3878418)Terminated due to inappropriate strategy. % 169.74/24.29 % (3878418)------------------------------ % 169.74/24.29 % (3878418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.74/24.29 % (3878418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.74/24.29 % (3878418)CaDiCaL version: 2.1.3 % 169.74/24.29 % (3878418)Termination reason: Inappropriate % 169.74/24.29 % (3878418)Time elapsed: 0.001 s % 169.74/24.29 % (3878418)Peak memory usage: 10 MB % 169.74/24.29 % (3878418)Instructions burned: 1 (million) % 169.74/24.29 % (3878418)------------------------------ % 169.74/24.29 % (3878418)------------------------------ % 169.74/24.29 % (3878420)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3112334370:i=44625:gsp=on_2816 on theBenchmark for (2816ds/44625Mi) % 182.89/26.12 % (3878420)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 182.89/26.12 % (3878420)Terminated due to inappropriate strategy. % 182.89/26.12 % (3878420)------------------------------ % 182.89/26.12 % (3878420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.89/26.12 % (3878420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.89/26.12 % (3878420)CaDiCaL version: 2.1.3 % 182.89/26.12 % (3878420)Termination reason: Inappropriate % 182.89/26.12 % (3878420)Time elapsed: 0.001 s % 182.89/26.12 % (3878420)Peak memory usage: 11 MB % 182.89/26.12 % (3878420)Instructions burned: 1 (million) % 182.89/26.12 % (3878420)------------------------------ % 182.89/26.12 % (3878420)------------------------------ % 182.89/26.12 % (3878422)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1779505544:i=160505_2816 on theBenchmark for (2816ds/160505Mi) % 182.89/26.12 % (3878422)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 182.89/26.12 % (3878422)Terminated due to inappropriate strategy. % 182.89/26.12 % (3878422)------------------------------ % 182.89/26.12 % (3878422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.89/26.12 % (3878422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.89/26.12 % (3878422)CaDiCaL version: 2.1.3 % 182.89/26.12 % (3878422)Termination reason: Inappropriate % 182.89/26.12 % (3878422)Time elapsed: 0.001 s % 182.89/26.12 % (3878422)Peak memory usage: 10 MB % 182.89/26.12 % (3878422)Instructions burned: 1 (million) % 182.89/26.12 % (3878422)------------------------------ % 182.89/26.12 % (3878422)------------------------------ % 182.89/26.12 % (3878424)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1710630846:fmbsr=1.3:i=225729_2816 on theBenchmark for (2816ds/225729Mi) % 182.89/26.12 % (3878424)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 182.89/26.12 % (3878424)Terminated due to inappropriate strategy. % 182.89/26.12 % (3878424)------------------------------ % 182.89/26.12 % (3878424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.89/26.12 % (3878424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.89/26.12 % (3878424)CaDiCaL version: 2.1.3 % 182.89/26.12 % (3878424)Termination reason: Inappropriate % 182.89/26.12 % (3878424)Time elapsed: 0.001 s % 182.89/26.12 % (3878424)Peak memory usage: 10 MB % 182.89/26.12 % (3878424)Instructions burned: 1 (million) % 182.89/26.12 % (3878424)------------------------------ % 182.89/26.12 % (3878424)------------------------------ % 182.89/26.12 % (3878426)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=999262127:fmbsr=2:i=185024:ins=7_2815 on theBenchmark for (2815ds/185024Mi) % 182.89/26.12 % (3878426)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 182.89/26.12 % (3878426)Terminated due to inappropriate strategy. % 182.89/26.12 % (3878426)------------------------------ % 182.89/26.12 % (3878426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.89/26.12 % (3878426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.89/26.12 % (3878426)CaDiCaL version: 2.1.3 % 182.89/26.12 % (3878426)Termination reason: Inappropriate % 182.89/26.12 % (3878426)Time elapsed: 0.001 s % 182.89/26.12 % (3878426)Peak memory usage: 10 MB % 182.89/26.12 % (3878426)Instructions burned: 1 (million) % 182.89/26.12 % (3878426)------------------------------ % 182.89/26.12 % (3878426)------------------------------ % 182.89/26.12 % (3878428)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3293466814:rtra=on_2815 on theBenchmark for (2815ds/0Mi) % 182.89/26.12 % (3878428)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 182.89/26.12 % (3878428)Terminated due to inappropriate strategy. % 182.89/26.12 % (3878428)------------------------------ % 182.89/26.12 % (3878428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.89/26.12 % (3878428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.89/26.12 % (3878428)CaDiCaL version: 2.1.3 % 182.89/26.12 % (3878428)Termination reason: Inappropriate % 182.89/26.12 % (3878428)Time elapsed: 0.001 s % 182.89/26.12 % (3878428)Peak memory usage: 10 MB % 182.89/26.12 % (3878428)Instructions burned: 2 (million) % 182.89/26.12 % (3878428)------------------------------ % 182.89/26.12 % (3878428)------------------------------ % 182.89/26.12 % (3878430)% WARNING: option uhcvi not known. % 182.89/26.12 % (3878430)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=619904551:i=271062:add=off:rtra=on:rawr=on_2815 on theBenchmark for (2815ds/271062Mi) % 206.10/29.34 % (3878408)Instruction limit reached! % 206.10/29.34 % (3878408)------------------------------ % 206.10/29.34 % (3878408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.10/29.34 % (3878408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.10/29.34 % (3878408)CaDiCaL version: 2.1.3 % 206.10/29.34 % (3878408)Termination reason: Instruction limit % 206.10/29.34 % (3878408)Termination phase: Saturation % 206.10/29.34 % (3878408)Time elapsed: 7.116 s % 206.10/29.34 % (3878408)Peak memory usage: 200 MB % 206.10/29.34 % (3878408)Instructions burned: 15854 (million) % 206.10/29.34 % (3878432)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2152476988:i=176048:add=on:rtra=on:rawr=on_2805 on theBenchmark for (2805ds/176048Mi) % 206.10/29.34 % (3878410)Instruction limit reached! % 206.10/29.34 % (3878410)------------------------------ % 206.10/29.34 % (3878410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.10/29.34 % (3878410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.10/29.34 % (3878410)CaDiCaL version: 2.1.3 % 206.10/29.34 % (3878410)Termination reason: Instruction limit % 206.10/29.34 % (3878410)Termination phase: Saturation % 206.10/29.34 % (3878410)Time elapsed: 8.156 s % 206.10/29.34 % (3878410)Peak memory usage: 231 MB % 206.10/29.34 % (3878410)Instructions burned: 17629 (million) % 206.10/29.34 % (3878434)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2679698180:i=206:fgj=on:rtra=on_2767 on theBenchmark for (2767ds/206Mi) % 206.10/29.34 % (3878434)Instruction limit reached! % 206.10/29.34 % (3878434)------------------------------ % 206.10/29.34 % (3878434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.10/29.34 % (3878434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.10/29.34 % (3878434)CaDiCaL version: 2.1.3 % 206.10/29.34 % (3878434)Termination reason: Instruction limit % 206.10/29.34 % (3878434)Termination phase: Saturation % 206.10/29.34 % (3878434)Time elapsed: 0.124 s % 206.10/29.34 % (3878434)Peak memory usage: 13 MB % 206.10/29.34 % (3878434)Instructions burned: 206 (million) % 206.10/29.34 % (3878436)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4256597963:i=232:rtra=on_2765 on theBenchmark for (2765ds/232Mi) % 206.10/29.34 % (3878436)Instruction limit reached! % 206.10/29.34 % (3878436)------------------------------ % 206.10/29.34 % (3878436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.10/29.34 % (3878436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.10/29.34 % (3878436)CaDiCaL version: 2.1.3 % 206.10/29.34 % (3878436)Termination reason: Instruction limit % 206.10/29.34 % (3878436)Termination phase: Saturation % 206.10/29.34 % (3878436)Time elapsed: 0.147 s % 206.10/29.34 % (3878436)Peak memory usage: 13 MB % 206.10/29.34 % (3878436)Instructions burned: 233 (million) % 206.10/29.34 % (3878438)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=318717858:i=262:rtra=on_2763 on theBenchmark for (2763ds/262Mi) % 206.10/29.34 % (3878438)Instruction limit reached! % 206.10/29.34 % (3878438)------------------------------ % 206.10/29.34 % (3878438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.10/29.34 % (3878438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.10/29.34 % (3878438)CaDiCaL version: 2.1.3 % 206.10/29.34 % (3878438)Termination reason: Instruction limit % 206.10/29.34 % (3878438)Termination phase: Saturation % 206.10/29.34 % (3878438)Time elapsed: 0.156 s % 206.10/29.34 % (3878438)Peak memory usage: 14 MB % 206.10/29.34 % (3878438)Instructions burned: 263 (million) % 206.10/29.34 % (3878441)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3402859305:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2762 on theBenchmark for (2762ds/318Mi) % 206.10/29.34 % (3878441)Instruction limit reached! % 206.10/29.34 % (3878441)------------------------------ % 206.10/29.34 % (3878441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.10/29.34 % (3878441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.10/29.34 % (3878441)CaDiCaL version: 2.1.3 % 206.10/29.34 % (3878441)Termination reason: Instruction limit % 206.10/29.34 % (3878441)Termination phase: Saturation % 206.10/29.34 % (3878441)Time elapsed: 0.210 s % 206.10/29.34 % (3878441)Peak memory usage: 15 MB % 206.10/29.34 % (3878441)Instructions burned: 318 (million) % 206.10/29.34 % (3878443)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2237567906:i=1428:nm=2:rtra=on_2759 on theBenchmark for (2759ds/1428Mi) % 222.39/31.65 % (3878443)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.39/31.65 % (3878443)Terminated due to inappropriate strategy. % 222.39/31.65 % (3878443)------------------------------ % 222.39/31.65 % (3878443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.39/31.65 % (3878443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.39/31.65 % (3878443)CaDiCaL version: 2.1.3 % 222.39/31.65 % (3878443)Termination reason: Inappropriate % 222.39/31.65 % (3878443)Time elapsed: 0.001 s % 222.39/31.65 % (3878443)Peak memory usage: 10 MB % 222.39/31.65 % (3878443)Instructions burned: 2 (million) % 222.39/31.65 % (3878443)------------------------------ % 222.39/31.65 % (3878443)------------------------------ % 222.39/31.65 % (3878445)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2140764474:i=262:bd=preordered:rtra=on:fsd=on_2759 on theBenchmark for (2759ds/262Mi) % 222.39/31.65 % (3878445)Instruction limit reached! % 222.39/31.65 % (3878445)------------------------------ % 222.39/31.65 % (3878445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.39/31.65 % (3878445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.39/31.65 % (3878445)CaDiCaL version: 2.1.3 % 222.39/31.65 % (3878445)Termination reason: Instruction limit % 222.39/31.65 % (3878445)Termination phase: Saturation % 222.39/31.65 % (3878445)Time elapsed: 0.157 s % 222.39/31.65 % (3878445)Peak memory usage: 13 MB % 222.39/31.65 % (3878445)Instructions burned: 263 (million) % 222.39/31.65 % (3878447)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=2054252347:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2757 on theBenchmark for (2757ds/1368Mi) % 222.39/31.65 % (3878447)Instruction limit reached! % 222.39/31.65 % (3878447)------------------------------ % 222.39/31.65 % (3878447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.39/31.65 % (3878447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.39/31.65 % (3878447)CaDiCaL version: 2.1.3 % 222.39/31.65 % (3878447)Termination reason: Instruction limit % 222.39/31.65 % (3878447)Termination phase: Saturation % 222.39/31.65 % (3878447)Time elapsed: 0.771 s % 222.39/31.65 % (3878447)Peak memory usage: 21 MB % 222.39/31.65 % (3878447)Instructions burned: 1368 (million) % 222.39/31.65 % (3878449)ott-21_1_sil=16000:si=on:fs=off:random_seed=3049049931:i=360:av=off:fsr=off:rtra=on_2750 on theBenchmark for (2750ds/360Mi) % 222.39/31.65 % (3878449)Instruction limit reached! % 222.39/31.65 % (3878449)------------------------------ % 222.39/31.65 % (3878449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.39/31.65 % (3878449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.39/31.65 % (3878449)CaDiCaL version: 2.1.3 % 222.39/31.65 % (3878449)Termination reason: Instruction limit % 222.39/31.65 % (3878449)Termination phase: Saturation % 222.39/31.65 % (3878449)Time elapsed: 0.158 s % 222.39/31.65 % (3878449)Peak memory usage: 13 MB % 222.39/31.65 % (3878449)Instructions burned: 360 (million) % 222.39/31.65 % (3878451)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2418311836:i=954:bd=all:rtra=on_2748 on theBenchmark for (2748ds/954Mi) % 222.39/31.65 % (3878451)Instruction limit reached! % 222.39/31.65 % (3878451)------------------------------ % 222.39/31.65 % (3878451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.39/31.65 % (3878451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.39/31.65 % (3878451)CaDiCaL version: 2.1.3 % 222.39/31.65 % (3878451)Termination reason: Instruction limit % 222.39/31.65 % (3878451)Termination phase: Saturation % 222.39/31.65 % (3878451)Time elapsed: 0.633 s % 222.39/31.65 % (3878451)Peak memory usage: 16 MB % 222.39/31.65 % (3878451)Instructions burned: 954 (million) % 222.39/31.65 % (3878453)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4271738816:fmbsr=1.3:i=1730:ins=25:rtra=on_2741 on theBenchmark for (2741ds/1730Mi) % 222.39/31.65 % (3878453)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.39/31.65 % (3878453)Terminated due to inappropriate strategy. % 222.39/31.65 % (3878453)------------------------------ % 222.39/31.65 % (3878453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.39/31.65 % (3878453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.39/31.65 % (3878453)CaDiCaL version: 2.1.3 % 222.39/31.65 % (3878453)Termination reason: Inappropriate % 222.39/31.65 % (3878453)Time elapsed: 0.001 s % 257.89/36.65 % (3878453)Peak memory usage: 10 MB % 257.89/36.65 % (3878453)Instructions burned: 2 (million) % 257.89/36.65 % (3878453)------------------------------ % 257.89/36.65 % (3878453)------------------------------ % 257.89/36.65 % (3878455)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4123922946:i=2358:rtra=on_2741 on theBenchmark for (2741ds/2358Mi) % 257.89/36.65 % (3878455)Instruction limit reached! % 257.89/36.65 % (3878455)------------------------------ % 257.89/36.65 % (3878455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.89/36.65 % (3878455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.89/36.65 % (3878455)CaDiCaL version: 2.1.3 % 257.89/36.65 % (3878455)Termination reason: Instruction limit % 257.89/36.65 % (3878455)Termination phase: Saturation % 257.89/36.65 % (3878455)Time elapsed: 1.225 s % 257.89/36.65 % (3878455)Peak memory usage: 19 MB % 257.89/36.65 % (3878455)Instructions burned: 2358 (million) % 257.89/36.65 % (3878457)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3808519081:i=1778:ins=1:rtra=on_2729 on theBenchmark for (2729ds/1778Mi) % 257.89/36.65 % (3878457)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 257.89/36.65 % (3878457)Terminated due to inappropriate strategy. % 257.89/36.65 % (3878457)------------------------------ % 257.89/36.65 % (3878457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.89/36.65 % (3878457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.89/36.65 % (3878457)CaDiCaL version: 2.1.3 % 257.89/36.65 % (3878457)Termination reason: Inappropriate % 257.89/36.65 % (3878457)Time elapsed: 0.001 s % 257.89/36.65 % (3878457)Peak memory usage: 10 MB % 257.89/36.65 % (3878457)Instructions burned: 2 (million) % 257.89/36.65 % (3878457)------------------------------ % 257.89/36.65 % (3878457)------------------------------ % 257.89/36.65 % (3878459)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=2851571980:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2728 on theBenchmark for (2728ds/1384Mi) % 257.89/36.65 % (3878459)Instruction limit reached! % 257.89/36.65 % (3878459)------------------------------ % 257.89/36.65 % (3878459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.89/36.65 % (3878459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.89/36.65 % (3878459)CaDiCaL version: 2.1.3 % 257.89/36.65 % (3878459)Termination reason: Instruction limit % 257.89/36.65 % (3878459)Termination phase: Saturation % 257.89/36.65 % (3878459)Time elapsed: 0.876 s % 257.89/36.65 % (3878459)Peak memory usage: 26 MB % 257.89/36.65 % (3878459)Instructions burned: 1385 (million) % 257.89/36.65 % (3878461)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1720239708:i=1758:kws=inv_precedence:fsr=off:rtra=on_2719 on theBenchmark for (2719ds/1758Mi) % 257.89/36.65 % (3878461)Instruction limit reached! % 257.89/36.65 % (3878461)------------------------------ % 257.89/36.65 % (3878461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.89/36.65 % (3878461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.89/36.65 % (3878461)CaDiCaL version: 2.1.3 % 257.89/36.65 % (3878461)Termination reason: Instruction limit % 257.89/36.65 % (3878461)Termination phase: Saturation % 257.89/36.65 % (3878461)Time elapsed: 0.986 s % 257.89/36.66 % (3878461)Peak memory usage: 23 MB % 257.89/36.66 % (3878461)Instructions burned: 1759 (million) % 257.89/36.66 % (3878463)fmb+10_1_sil=64000:si=on:random_seed=2664473324:i=44122:nm=2:rtra=on:gsp=on_2709 on theBenchmark for (2709ds/44122Mi) % 257.89/36.66 % (3878463)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 257.89/36.66 % (3878463)Terminated due to inappropriate strategy. % 257.89/36.66 % (3878463)------------------------------ % 257.89/36.66 % (3878463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.89/36.66 % (3878463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.89/36.66 % (3878463)CaDiCaL version: 2.1.3 % 257.89/36.66 % (3878463)Termination reason: Inappropriate % 257.89/36.66 % (3878463)Time elapsed: 0.001 s % 257.89/36.66 % (3878463)Peak memory usage: 10 MB % 257.89/36.66 % (3878463)Instructions burned: 2 (million) % 257.89/36.66 % (3878463)------------------------------ % 257.89/36.66 % (3878463)------------------------------ % 257.89/36.66 % (3878465)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4065619128:i=19030:nm=5:rtra=on_2709 on theBenchmark for (2709ds/19030Mi) % 286.28/40.69 % (3878465)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.28/40.69 % (3878465)Terminated due to inappropriate strategy. % 286.28/40.69 % (3878465)------------------------------ % 286.28/40.69 % (3878465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.28/40.69 % (3878465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.28/40.69 % (3878465)CaDiCaL version: 2.1.3 % 286.28/40.69 % (3878465)Termination reason: Inappropriate % 286.28/40.69 % (3878465)Time elapsed: 0.001 s % 286.28/40.69 % (3878465)Peak memory usage: 10 MB % 286.28/40.69 % (3878465)Instructions burned: 2 (million) % 286.28/40.69 % (3878465)------------------------------ % 286.28/40.69 % (3878465)------------------------------ % 286.28/40.69 % (3878467)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2827177208:fmbsr=1.7:i=1840:rtra=on_2709 on theBenchmark for (2709ds/1840Mi) % 286.28/40.69 % (3878467)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.28/40.69 % (3878467)Terminated due to inappropriate strategy. % 286.28/40.69 % (3878467)------------------------------ % 286.28/40.69 % (3878467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.28/40.69 % (3878467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.28/40.69 % (3878467)CaDiCaL version: 2.1.3 % 286.28/40.69 % (3878467)Termination reason: Inappropriate % 286.28/40.69 % (3878467)Time elapsed: 0.001 s % 286.28/40.69 % (3878467)Peak memory usage: 10 MB % 286.28/40.69 % (3878467)Instructions burned: 2 (million) % 286.28/40.69 % (3878467)------------------------------ % 286.28/40.69 % (3878467)------------------------------ % 286.28/40.69 % (3878469)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1067926332:i=10262:rtra=on_2709 on theBenchmark for (2709ds/10262Mi) % 286.28/40.69 % (3878416)Instruction limit reached! % 286.28/40.69 % (3878416)------------------------------ % 286.28/40.69 % (3878416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.28/40.69 % (3878416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.28/40.69 % (3878416)CaDiCaL version: 2.1.3 % 286.28/40.69 % (3878416)Termination reason: Instruction limit % 286.28/40.69 % (3878416)Termination phase: Saturation % 286.28/40.69 % (3878416)Time elapsed: 12.263 s % 286.28/40.69 % (3878416)Peak memory usage: 31 MB % 286.28/40.69 % (3878416)Instructions burned: 28121 (million) % 286.28/40.69 % (3878471)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3551227452:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2703 on theBenchmark for (2703ds/2944Mi) % 286.28/40.69 % (3878471)Instruction limit reached! % 286.28/40.69 % (3878471)------------------------------ % 286.28/40.69 % (3878471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.28/40.69 % (3878471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.28/40.69 % (3878471)CaDiCaL version: 2.1.3 % 286.28/40.69 % (3878471)Termination reason: Instruction limit % 286.28/40.69 % (3878471)Termination phase: Saturation % 286.28/40.69 % (3878471)Time elapsed: 1.626 s % 286.28/40.69 % (3878471)Peak memory usage: 36 MB % 286.28/40.69 % (3878471)Instructions burned: 2944 (million) % 286.28/40.69 % (3878473)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=4032060949:i=12648:rtra=on_2686 on theBenchmark for (2686ds/12648Mi) % 286.28/40.69 % (3878473)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.28/40.69 % (3878473)Terminated due to inappropriate strategy. % 286.28/40.69 % (3878473)------------------------------ % 286.28/40.69 % (3878473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.28/40.69 % (3878473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.28/40.69 % (3878473)CaDiCaL version: 2.1.3 % 286.28/40.69 % (3878473)Termination reason: Inappropriate % 286.28/40.69 % (3878473)Time elapsed: 0.001 s % 286.28/40.69 % (3878473)Peak memory usage: 10 MB % 286.28/40.69 % (3878473)Instructions burned: 2 (million) % 286.28/40.69 % (3878473)------------------------------ % 286.28/40.69 % (3878473)------------------------------ % 286.28/40.69 % (3878475)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3572668630:fmbsr=2.30978:i=4348:rtra=on_2686 on theBenchmark for (2686ds/4348Mi) % 286.28/40.69 % (3878475)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 286.28/40.69 % (3878475)Terminated due to inappropriate strategy. % 286.28/40.69 % (3878475)------------------------------ % 286.28/40.69 % (3878475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.63 % (3878475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.63 % (3878475)CaDiCaL version: 2.1.3 % 300.47/42.63 % (3878475)Termination reason: Inappropriate % 300.47/42.63 % (3878475)Time elapsed: 0.001 s % 300.47/42.63 % (3878475)Peak memory usage: 10 MB % 300.47/42.63 % (3878475)Instructions burned: 2 (million) % 300.47/42.63 % (3878475)------------------------------ % 300.47/42.63 % (3878475)------------------------------ % 300.47/42.63 % (3878477)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3492390593:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2686 on theBenchmark for (2686ds/1738Mi) % 300.47/42.63 % (3878477)Instruction limit reached! % 300.47/42.63 % (3878477)------------------------------ % 300.47/42.63 % (3878477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.63 % (3878477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.63 % (3878477)CaDiCaL version: 2.1.3 % 300.47/42.63 % (3878477)Termination reason: Instruction limit % 300.47/42.63 % (3878477)Termination phase: Saturation % 300.47/42.63 % (3878477)Time elapsed: 0.995 s % 300.47/42.63 % (3878477)Peak memory usage: 22 MB % 300.47/42.63 % (3878477)Instructions burned: 1738 (million) % 300.47/42.63 % (3878479)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2666397514:i=10228:av=off:rtra=on_2676 on theBenchmark for (2676ds/10228Mi) % 300.47/42.63 % (3878321)Instruction limit reached! % 300.47/42.63 % (3878321)------------------------------ % 300.47/42.63 % (3878321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.63 % (3878321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.63 % (3878321)CaDiCaL version: 2.1.3 % 300.47/42.63 % (3878321)Termination reason: Instruction limit % 300.47/42.63 % (3878321)Termination phase: Saturation % 300.47/42.63 % (3878321)Time elapsed: 34.153 s % 300.47/42.63 % (3878321)Peak memory usage: 334 MB % 300.47/42.63 % (3878321)Instructions burned: 135534 (million) % 300.47/42.63 % (3878481)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3162373425:i=108564:rtra=on_2657 on theBenchmark for (2657ds/108564Mi) % 300.47/42.63 % (3878481)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.47/42.63 % (3878481)Terminated due to inappropriate strategy. % 300.47/42.64 % (3878481)------------------------------ % 300.47/42.64 % (3878481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.64 % (3878481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.64 % (3878481)CaDiCaL version: 2.1.3 % 300.47/42.64 % (3878481)Termination reason: Inappropriate % 300.47/42.64 % (3878481)Time elapsed: 0.001 s % 300.47/42.64 % (3878481)Peak memory usage: 10 MB % 300.47/42.64 % (3878481)Instructions burned: 2 (million) % 300.47/42.64 % (3878481)------------------------------ % 300.47/42.64 % (3878481)------------------------------ % 300.47/42.64 % (3878483)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=4180310797:i=7024:aac=none:rtra=on_2657 on theBenchmark for (2657ds/7024Mi) % 300.47/42.64 % (3878469)Instruction limit reached! % 300.47/42.64 % (3878469)------------------------------ % 300.47/42.64 % (3878469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.64 % (3878469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.64 % (3878469)CaDiCaL version: 2.1.3 % 300.47/42.64 % (3878469)Termination reason: Instruction limit % 300.47/42.64 % (3878469)Termination phase: Saturation % 300.47/42.64 % (3878469)Time elapsed: 5.942 s % 300.47/42.64 % (3878469)Peak memory usage: 67 MB % 300.47/42.64 % (3878469)Instructions burned: 10263 (million) % 300.47/42.64 % (3878485)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=110529897:i=7546:rtra=on:amm=off_2649 on theBenchmark for (2649ds/7546Mi) % 300.47/42.64 % (3878483)Instruction limit reached! % 300.47/42.64 % (3878483)------------------------------ % 300.47/42.64 % (3878483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.47/42.64 % (3878483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.47/42.64 % (3878483)CaDiCaL version: 2.1.3 % 300.47/42.64 % (3878483)Termination reason: Instruction limit % 300.47/42.64 % (3878483)Termination phase: Saturation % 300.47/42.64 % (3878483)Time elapsed: 2.136 s % 300.47/42.64 % (3878483)Peak memory usage: 47 MB % 300.47/42.64 % (3878483)Instructions burned: 7025 (million) % 300.47/42.64 % (3878487)ott+11_1_sil=16000:si=on:gs=on:random_seed=3850349547:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2636 on theBenchmark fo % 300.47/42.64 Terminated % 300.47/42.64 % Vampire exiting %------------------------------------------------------------------------------