%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX125_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:31 PM UTC 2026 % Result : Timeout 300.69s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX125_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n008.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 15:03:24 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.13/0.73 % (2315811)Will run a generic schedule for satisfiability detection. % 3.13/0.73 % (2315817)% WARNING: option uhcvi not known. % 3.13/0.73 % (2315817)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=412859311:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.13/0.73 % (2315816)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1350521479_2999 on theBenchmark for (2999ds/0Mi) % 3.13/0.73 % (2315818)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3335473270:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.13/0.73 % (2315819)dis+10_1_sil=32000:sp=arity:random_seed=567888001:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.13/0.73 % (2315820)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3552136271:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.13/0.73 % (2315821)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1714662849:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.13/0.73 % (2315822)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3300894210:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.13/0.73 % (2315816)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.13/0.73 % (2315816)Terminated due to inappropriate strategy. % 3.13/0.73 % (2315816)------------------------------ % 3.13/0.73 % (2315816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.13/0.73 % (2315816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.13/0.73 % (2315816)CaDiCaL version: 2.1.3 % 3.13/0.73 % (2315816)Termination reason: Inappropriate % 3.13/0.73 % (2315816)Time elapsed: 0.007 s % 3.13/0.73 % (2315816)Peak memory usage: 10 MB % 3.13/0.73 % (2315816)Instructions burned: 16 (million) % 3.13/0.73 % (2315816)------------------------------ % 3.13/0.73 % (2315816)------------------------------ % 3.13/0.73 % (2315830)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=648289999:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.13/0.73 % (2315830)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.13/0.73 % (2315830)Terminated due to inappropriate strategy. % 3.13/0.73 % (2315830)------------------------------ % 3.13/0.73 % (2315830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.13/0.73 % (2315830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.13/0.73 % (2315830)CaDiCaL version: 2.1.3 % 3.13/0.73 % (2315830)Termination reason: Inappropriate % 3.13/0.73 % (2315830)Time elapsed: 0.007 s % 3.13/0.73 % (2315830)Peak memory usage: 11 MB % 3.13/0.73 % (2315830)Instructions burned: 16 (million) % 3.13/0.73 % (2315830)------------------------------ % 3.13/0.73 % (2315830)------------------------------ % 3.13/0.73 % (2315819)Instruction limit reached! % 3.13/0.73 % (2315819)------------------------------ % 3.13/0.73 % (2315819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.13/0.73 % (2315819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.13/0.73 % (2315819)CaDiCaL version: 2.1.3 % 3.13/0.73 % (2315819)Termination reason: Instruction limit % 3.13/0.73 % (2315819)Termination phase: Saturation % 3.13/0.73 % (2315819)Time elapsed: 0.044 s % 3.13/0.73 % (2315819)Peak memory usage: 12 MB % 3.13/0.73 % (2315819)Instructions burned: 105 (million) % 3.13/0.73 % (2315820)Instruction limit reached! % 3.13/0.73 % (2315820)------------------------------ % 3.13/0.73 % (2315820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.13/0.73 % (2315820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.13/0.73 % (2315820)CaDiCaL version: 2.1.3 % 3.13/0.73 % (2315820)Termination reason: Instruction limit % 3.13/0.73 % (2315820)Termination phase: Saturation % 3.13/0.73 % (2315820)Time elapsed: 0.051 s % 3.13/0.73 % (2315820)Peak memory usage: 13 MB % 3.13/0.73 % (2315820)Instructions burned: 116 (million) % 3.13/0.73 % (2315832)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2566738080:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.13/0.73 % (2315821)Instruction limit reached! % 3.13/0.73 % (2315821)------------------------------ % 3.13/0.73 % (2315821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.13/0.73 % (2315821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.13/0.73 % (2315821)CaDiCaL version: 2.1.3 % 3.13/0.73 % (2315821)Termination reason: Instruction limit % 3.97/0.90 % (2315821)Termination phase: Saturation % 3.97/0.90 % (2315821)Time elapsed: 0.063 s % 3.97/0.90 % (2315821)Peak memory usage: 13 MB % 3.97/0.90 % (2315821)Instructions burned: 131 (million) % 3.97/0.90 % (2315833)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=3220619053:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.97/0.90 % (2315834)ott-21_1_sil=16000:fs=off:random_seed=2718576816:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.97/0.90 % (2315822)Instruction limit reached! % 3.97/0.90 % (2315822)------------------------------ % 3.97/0.90 % (2315822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.97/0.90 % (2315822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.97/0.90 % (2315822)CaDiCaL version: 2.1.3 % 3.97/0.90 % (2315822)Termination reason: Instruction limit % 3.97/0.90 % (2315822)Termination phase: Saturation % 3.97/0.90 % (2315822)Time elapsed: 0.081 s % 3.97/0.90 % (2315822)Peak memory usage: 13 MB % 3.97/0.90 % (2315822)Instructions burned: 159 (million) % 3.97/0.90 % (2315836)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3413345563:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 3.97/0.90 % (2315839)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=162568:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.97/0.90 % (2315839)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.97/0.90 % (2315839)Terminated due to inappropriate strategy. % 3.97/0.90 % (2315839)------------------------------ % 3.97/0.90 % (2315839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.97/0.90 % (2315839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.97/0.90 % (2315839)CaDiCaL version: 2.1.3 % 3.97/0.90 % (2315839)Termination reason: Inappropriate % 3.97/0.90 % (2315839)Time elapsed: 0.005 s % 3.97/0.90 % (2315839)Peak memory usage: 10 MB % 3.97/0.90 % (2315839)Instructions burned: 12 (million) % 3.97/0.90 % (2315839)------------------------------ % 3.97/0.90 % (2315839)------------------------------ % 3.97/0.90 % (2315832)Instruction limit reached! % 3.97/0.90 % (2315832)------------------------------ % 3.97/0.90 % (2315832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.97/0.90 % (2315832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.97/0.90 % (2315832)CaDiCaL version: 2.1.3 % 3.97/0.90 % (2315832)Termination reason: Instruction limit % 3.97/0.90 % (2315832)Termination phase: Saturation % 3.97/0.90 % (2315832)Time elapsed: 0.060 s % 3.97/0.90 % (2315832)Peak memory usage: 13 MB % 3.97/0.90 % (2315832)Instructions burned: 134 (million) % 3.97/0.90 % (2315842)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2634671700:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.97/0.90 % (2315843)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3625158203:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.97/0.90 % (2315843)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.97/0.90 % (2315843)Terminated due to inappropriate strategy. % 3.97/0.90 % (2315843)------------------------------ % 3.97/0.90 % (2315843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.97/0.90 % (2315843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.97/0.90 % (2315843)CaDiCaL version: 2.1.3 % 3.97/0.90 % (2315843)Termination reason: Inappropriate % 3.97/0.90 % (2315843)Time elapsed: 0.005 s % 3.97/0.90 % (2315843)Peak memory usage: 10 MB % 3.97/0.90 % (2315843)Instructions burned: 12 (million) % 3.97/0.90 % (2315843)------------------------------ % 3.97/0.90 % (2315843)------------------------------ % 3.97/0.90 % (2315834)Instruction limit reached! % 3.97/0.90 % (2315834)------------------------------ % 3.97/0.90 % (2315834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.97/0.90 % (2315834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.97/0.90 % (2315834)CaDiCaL version: 2.1.3 % 3.97/0.90 % (2315834)Termination reason: Instruction limit % 3.97/0.90 % (2315834)Termination phase: Saturation % 3.97/0.90 % (2315834)Time elapsed: 0.075 s % 3.97/0.90 % (2315834)Peak memory usage: 13 MB % 3.97/0.90 % (2315834)Instructions burned: 183 (million) % 3.97/0.90 % (2315846)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=961783836: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) % 16.24/2.65 % (2315847)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2662652877:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 16.24/2.65 % (2315836)Instruction limit reached! % 16.24/2.65 % (2315836)------------------------------ % 16.24/2.65 % (2315836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.24/2.65 % (2315836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.24/2.65 % (2315836)CaDiCaL version: 2.1.3 % 16.24/2.65 % (2315836)Termination reason: Instruction limit % 16.24/2.65 % (2315836)Termination phase: Saturation % 16.24/2.65 % (2315836)Time elapsed: 0.188 s % 16.24/2.65 % (2315836)Peak memory usage: 13 MB % 16.24/2.65 % (2315836)Instructions burned: 479 (million) % 16.24/2.65 % (2315850)fmb+10_1_sil=64000:random_seed=316142151:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 16.24/2.65 % (2315850)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.24/2.65 % (2315850)Terminated due to inappropriate strategy. % 16.24/2.65 % (2315850)------------------------------ % 16.24/2.65 % (2315850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.24/2.65 % (2315850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.24/2.65 % (2315850)CaDiCaL version: 2.1.3 % 16.24/2.65 % (2315850)Termination reason: Inappropriate % 16.24/2.65 % (2315850)Time elapsed: 0.007 s % 16.24/2.65 % (2315850)Peak memory usage: 11 MB % 16.24/2.65 % (2315850)Instructions burned: 16 (million) % 16.24/2.65 % (2315850)------------------------------ % 16.24/2.65 % (2315850)------------------------------ % 16.24/2.65 % (2315852)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=959817845:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 16.24/2.65 % (2315852)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.24/2.65 % (2315852)Terminated due to inappropriate strategy. % 16.24/2.65 % (2315852)------------------------------ % 16.24/2.65 % (2315852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.24/2.65 % (2315852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.24/2.65 % (2315852)CaDiCaL version: 2.1.3 % 16.24/2.65 % (2315852)Termination reason: Inappropriate % 16.24/2.65 % (2315852)Time elapsed: 0.007 s % 16.24/2.65 % (2315852)Peak memory usage: 10 MB % 16.24/2.65 % (2315852)Instructions burned: 16 (million) % 16.24/2.65 % (2315852)------------------------------ % 16.24/2.65 % (2315852)------------------------------ % 16.24/2.65 % (2315854)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=394057954:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 16.24/2.65 % (2315854)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.24/2.65 % (2315854)Terminated due to inappropriate strategy. % 16.24/2.65 % (2315854)------------------------------ % 16.24/2.65 % (2315854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.24/2.65 % (2315854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.24/2.65 % (2315854)CaDiCaL version: 2.1.3 % 16.24/2.65 % (2315854)Termination reason: Inappropriate % 16.24/2.65 % (2315854)Time elapsed: 0.007 s % 16.24/2.65 % (2315854)Peak memory usage: 10 MB % 16.24/2.65 % (2315854)Instructions burned: 16 (million) % 16.24/2.65 % (2315854)------------------------------ % 16.24/2.65 % (2315854)------------------------------ % 16.24/2.65 % (2315856)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1985547090:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 16.24/2.65 % (2315833)Instruction limit reached! % 16.24/2.65 % (2315833)------------------------------ % 16.24/2.65 % (2315833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.24/2.65 % (2315833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.24/2.65 % (2315833)CaDiCaL version: 2.1.3 % 16.24/2.65 % (2315833)Termination reason: Instruction limit % 16.24/2.65 % (2315833)Termination phase: Saturation % 16.24/2.65 % (2315833)Time elapsed: 0.349 s % 16.24/2.65 % (2315833)Peak memory usage: 19 MB % 16.24/2.65 % (2315833)Instructions burned: 686 (million) % 16.24/2.65 % (2315858)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1937193175:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 16.24/2.65 % (2315846)Instruction limit reached! % 16.24/2.65 % (2315846)------------------------------ % 30.91/4.67 % (2315846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.91/4.67 % (2315846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.91/4.67 % (2315846)CaDiCaL version: 2.1.3 % 30.91/4.67 % (2315846)Termination reason: Instruction limit % 30.91/4.67 % (2315846)Termination phase: Saturation % 30.91/4.67 % (2315846)Time elapsed: 0.278 s % 30.91/4.67 % (2315846)Peak memory usage: 14 MB % 30.91/4.67 % (2315846)Instructions burned: 694 (million) % 30.91/4.67 % (2315860)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1560010763:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 30.91/4.67 % (2315860)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.91/4.67 % (2315860)Terminated due to inappropriate strategy. % 30.91/4.67 % (2315860)------------------------------ % 30.91/4.67 % (2315860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.91/4.67 % (2315860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.91/4.67 % (2315860)CaDiCaL version: 2.1.3 % 30.91/4.67 % (2315860)Termination reason: Inappropriate % 30.91/4.67 % (2315860)Time elapsed: 0.007 s % 30.91/4.67 % (2315860)Peak memory usage: 11 MB % 30.91/4.67 % (2315860)Instructions burned: 16 (million) % 30.91/4.67 % (2315860)------------------------------ % 30.91/4.67 % (2315860)------------------------------ % 30.91/4.67 % (2315862)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3891517852:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 30.91/4.67 % (2315862)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.91/4.67 % (2315862)Terminated due to inappropriate strategy. % 30.91/4.67 % (2315862)------------------------------ % 30.91/4.67 % (2315862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.91/4.67 % (2315862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.91/4.67 % (2315862)CaDiCaL version: 2.1.3 % 30.91/4.67 % (2315862)Termination reason: Inappropriate % 30.91/4.67 % (2315862)Time elapsed: 0.007 s % 30.91/4.67 % (2315862)Peak memory usage: 10 MB % 30.91/4.67 % (2315862)Instructions burned: 16 (million) % 30.91/4.67 % (2315862)------------------------------ % 30.91/4.67 % (2315862)------------------------------ % 30.91/4.67 % (2315847)Instruction limit reached! % 30.91/4.67 % (2315847)------------------------------ % 30.91/4.67 % (2315847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.91/4.67 % (2315847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.91/4.67 % (2315847)CaDiCaL version: 2.1.3 % 30.91/4.67 % (2315847)Termination reason: Instruction limit % 30.91/4.67 % (2315847)Termination phase: Saturation % 30.91/4.67 % (2315847)Time elapsed: 0.341 s % 30.91/4.67 % (2315847)Peak memory usage: 14 MB % 30.91/4.67 % (2315847)Instructions burned: 881 (million) % 30.91/4.67 % (2315864)ott-2_1_sil=16000:newcnf=on:random_seed=2215649573:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 30.91/4.67 % (2315865)ott+10_1_sil=32000:tgt=ground:random_seed=2306922321:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 30.91/4.67 % (2315842)Instruction limit reached! % 30.91/4.67 % (2315842)------------------------------ % 30.91/4.67 % (2315842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.91/4.67 % (2315842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.91/4.67 % (2315842)CaDiCaL version: 2.1.3 % 30.91/4.67 % (2315842)Termination reason: Instruction limit % 30.91/4.67 % (2315842)Termination phase: Saturation % 30.91/4.67 % (2315842)Time elapsed: 0.457 s % 30.91/4.67 % (2315842)Peak memory usage: 13 MB % 30.91/4.67 % (2315842)Instructions burned: 1179 (million) % 30.91/4.67 % (2315868)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3006930207:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 30.91/4.67 % (2315868)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.91/4.67 % (2315868)Terminated due to inappropriate strategy. % 30.91/4.67 % (2315868)------------------------------ % 30.91/4.67 % (2315868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.91/4.67 % (2315868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.91/4.67 % (2315868)CaDiCaL version: 2.1.3 % 30.91/4.67 % (2315868)Termination reason: Inappropriate % 30.91/4.67 % (2315868)Time elapsed: 0.007 s % 30.91/4.67 % (2315868)Peak memory usage: 11 MB % 30.91/4.67 % (2315868)Instructions burned: 16 (million) % 83.72/12.05 % (2315868)------------------------------ % 83.72/12.05 % (2315868)------------------------------ % 83.72/12.05 % (2315870)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2279682631:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi) % 83.72/12.05 % (2315864)Instruction limit reached! % 83.72/12.05 % (2315864)------------------------------ % 83.72/12.05 % (2315864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.72/12.05 % (2315864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.72/12.05 % (2315864)CaDiCaL version: 2.1.3 % 83.72/12.05 % (2315864)Termination reason: Instruction limit % 83.72/12.05 % (2315864)Termination phase: Saturation % 83.72/12.05 % (2315864)Time elapsed: 0.351 s % 83.72/12.05 % (2315864)Peak memory usage: 14 MB % 83.72/12.05 % (2315864)Instructions burned: 870 (million) % 83.72/12.05 % (2315872)dis+21_1_sil=32000:sas=cadical:random_seed=518561217:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 83.72/12.05 % (2315858)Instruction limit reached! % 83.72/12.05 % (2315858)------------------------------ % 83.72/12.05 % (2315858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.72/12.05 % (2315858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.72/12.05 % (2315858)CaDiCaL version: 2.1.3 % 83.72/12.05 % (2315858)Termination reason: Instruction limit % 83.72/12.05 % (2315858)Termination phase: Saturation % 83.72/12.05 % (2315858)Time elapsed: 0.803 s % 83.72/12.05 % (2315858)Peak memory usage: 24 MB % 83.72/12.05 % (2315858)Instructions burned: 1473 (million) % 83.72/12.05 % (2315874)ott+11_1_sil=16000:gs=on:random_seed=4118404922:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 83.72/12.05 % (2315870)Instruction limit reached! % 83.72/12.05 % (2315870)------------------------------ % 83.72/12.05 % (2315870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.72/12.05 % (2315870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.72/12.05 % (2315870)CaDiCaL version: 2.1.3 % 83.72/12.05 % (2315870)Termination reason: Instruction limit % 83.72/12.05 % (2315870)Termination phase: Saturation % 83.72/12.05 % (2315870)Time elapsed: 1.360 s % 83.72/12.05 % (2315870)Peak memory usage: 16 MB % 83.72/12.05 % (2315870)Instructions burned: 3514 (million) % 83.72/12.05 % (2315876)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3974704711:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 83.72/12.05 % (2315876)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.72/12.05 % (2315876)Terminated due to inappropriate strategy. % 83.72/12.05 % (2315876)------------------------------ % 83.72/12.05 % (2315876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.72/12.05 % (2315876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.72/12.05 % (2315876)CaDiCaL version: 2.1.3 % 83.72/12.05 % (2315876)Termination reason: Inappropriate % 83.72/12.05 % (2315876)Time elapsed: 0.007 s % 83.72/12.05 % (2315876)Peak memory usage: 10 MB % 83.72/12.05 % (2315876)Instructions burned: 16 (million) % 83.72/12.05 % (2315876)------------------------------ % 83.72/12.05 % (2315876)------------------------------ % 83.72/12.05 % (2315878)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2931589971:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2979 on theBenchmark for (2979ds/4591Mi) % 83.72/12.05 % (2315874)Instruction limit reached! % 83.72/12.05 % (2315874)------------------------------ % 83.72/12.05 % (2315874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.72/12.05 % (2315874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.72/12.05 % (2315874)CaDiCaL version: 2.1.3 % 83.72/12.05 % (2315874)Termination reason: Instruction limit % 83.72/12.05 % (2315874)Termination phase: Saturation % 83.72/12.05 % (2315874)Time elapsed: 0.866 s % 83.72/12.05 % (2315874)Peak memory usage: 13 MB % 83.72/12.05 % (2315874)Instructions burned: 2252 (million) % 83.72/12.05 % (2315880)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=337089315:i=29340_2978 on theBenchmark for (2978ds/29340Mi) % 83.72/12.05 % (2315872)Instruction limit reached! % 83.72/12.05 % (2315872)------------------------------ % 83.72/12.05 % (2315872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.72/12.05 % (2315872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.72/12.05 % (2315872)CaDiCaL version: 2.1.3 % 83.72/12.05 % (2315872)Termination reason: Instruction limit % 95.54/13.80 % (2315872)Termination phase: Saturation % 95.54/13.80 % (2315872)Time elapsed: 1.468 s % 95.54/13.80 % (2315872)Peak memory usage: 16 MB % 95.54/13.80 % (2315872)Instructions burned: 3775 (million) % 95.54/13.80 % (2315882)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=62640723:i=5211_2975 on theBenchmark for (2975ds/5211Mi) % 95.54/13.80 % (2315856)Instruction limit reached! % 95.54/13.80 % (2315856)------------------------------ % 95.54/13.80 % (2315856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.54/13.80 % (2315856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.54/13.80 % (2315856)CaDiCaL version: 2.1.3 % 95.54/13.80 % (2315856)Termination reason: Instruction limit % 95.54/13.80 % (2315856)Termination phase: Saturation % 95.54/13.80 % (2315856)Time elapsed: 2.024 s % 95.54/13.80 % (2315856)Peak memory usage: 19 MB % 95.54/13.80 % (2315856)Instructions burned: 5132 (million) % 95.54/13.80 % (2315884)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=169900950:i=5497:nm=2_2975 on theBenchmark for (2975ds/5497Mi) % 95.54/13.80 % (2315884)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 95.54/13.80 % (2315884)Terminated due to inappropriate strategy. % 95.54/13.80 % (2315884)------------------------------ % 95.54/13.80 % (2315884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.54/13.80 % (2315884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.54/13.80 % (2315884)CaDiCaL version: 2.1.3 % 95.54/13.80 % (2315884)Termination reason: Inappropriate % 95.54/13.80 % (2315884)Time elapsed: 0.007 s % 95.54/13.80 % (2315884)Peak memory usage: 11 MB % 95.54/13.80 % (2315884)Instructions burned: 16 (million) % 95.54/13.80 % (2315884)------------------------------ % 95.54/13.80 % (2315884)------------------------------ % 95.54/13.80 % (2315886)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3036598980:fmbsr=2:i=46332_2975 on theBenchmark for (2975ds/46332Mi) % 95.54/13.80 % (2315886)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 95.54/13.80 % (2315886)Terminated due to inappropriate strategy. % 95.54/13.80 % (2315886)------------------------------ % 95.54/13.80 % (2315886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.54/13.80 % (2315886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.54/13.80 % (2315886)CaDiCaL version: 2.1.3 % 95.54/13.80 % (2315886)Termination reason: Inappropriate % 95.54/13.80 % (2315886)Time elapsed: 0.007 s % 95.54/13.80 % (2315886)Peak memory usage: 10 MB % 95.54/13.80 % (2315886)Instructions burned: 16 (million) % 95.54/13.80 % (2315886)------------------------------ % 95.54/13.80 % (2315886)------------------------------ % 95.54/13.80 % (2315888)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1854669300:i=14071_2974 on theBenchmark for (2974ds/14071Mi) % 95.54/13.80 % (2315888)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 95.54/13.80 % (2315888)Terminated due to inappropriate strategy. % 95.54/13.80 % (2315888)------------------------------ % 95.54/13.80 % (2315888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.54/13.80 % (2315888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.54/13.80 % (2315888)CaDiCaL version: 2.1.3 % 95.54/13.80 % (2315888)Termination reason: Inappropriate % 95.54/13.80 % (2315888)Time elapsed: 0.007 s % 96.13/13.80 % (2315888)Peak memory usage: 10 MB % 96.13/13.80 % (2315888)Instructions burned: 16 (million) % 96.13/13.80 % (2315888)------------------------------ % 96.13/13.80 % (2315888)------------------------------ % 96.13/13.80 % (2315890)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=400521588:i=22565:add=on:rawr=on_2974 on theBenchmark for (2974ds/22565Mi) % 96.13/13.80 % (2315865)Instruction limit reached! % 96.13/13.80 % (2315865)------------------------------ % 96.13/13.80 % (2315865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.13/13.80 % (2315865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.13/13.80 % (2315865)CaDiCaL version: 2.1.3 % 96.13/13.80 % (2315865)Termination reason: Instruction limit % 96.13/13.80 % (2315865)Termination phase: Saturation % 96.13/13.80 % (2315865)Time elapsed: 2.013 s % 96.13/13.80 % (2315865)Peak memory usage: 14 MB % 96.13/13.80 % (2315865)Instructions burned: 5114 (million) % 96.13/13.80 % (2315892)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2397574369:i=8173:av=off_2974 on theBenchmark for (2974ds/8173Mi) % 96.13/13.80 % (2315882)Instruction limit reached! % 96.76/13.94 % (2315882)------------------------------ % 96.76/13.94 % (2315882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.76/13.94 % (2315882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.76/13.94 % (2315882)CaDiCaL version: 2.1.3 % 96.76/13.94 % (2315882)Termination reason: Instruction limit % 96.76/13.94 % (2315882)Termination phase: Saturation % 96.76/13.94 % (2315882)Time elapsed: 2.006 s % 96.76/13.94 % (2315882)Peak memory usage: 21 MB % 96.76/13.94 % (2315882)Instructions burned: 5213 (million) % 96.76/13.94 % (2315894)dis+10_16:1_sil=16000:random_seed=2137452960:i=9155:fsr=off_2955 on theBenchmark for (2955ds/9155Mi) % 96.76/13.94 % (2315878)Instruction limit reached! % 96.76/13.94 % (2315878)------------------------------ % 96.76/13.94 % (2315878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.76/13.94 % (2315878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.76/13.94 % (2315878)CaDiCaL version: 2.1.3 % 96.76/13.94 % (2315878)Termination reason: Instruction limit % 96.76/13.94 % (2315878)Termination phase: Saturation % 96.76/13.94 % (2315878)Time elapsed: 2.632 s % 96.76/13.94 % (2315878)Peak memory usage: 44 MB % 96.76/13.94 % (2315878)Instructions burned: 4592 (million) % 96.76/13.94 % (2315896)ott-3_8_sil=64000:random_seed=1800909705:i=20139:bs=on_2952 on theBenchmark for (2952ds/20139Mi) % 96.76/13.94 % (2315892)Instruction limit reached! % 96.76/13.94 % (2315892)------------------------------ % 96.76/13.94 % (2315892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.76/13.94 % (2315892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.76/13.94 % (2315892)CaDiCaL version: 2.1.3 % 96.76/13.94 % (2315892)Termination reason: Instruction limit % 96.76/13.94 % (2315892)Termination phase: Saturation % 96.76/13.94 % (2315892)Time elapsed: 3.214 s % 96.76/13.94 % (2315892)Peak memory usage: 16 MB % 96.76/13.94 % (2315892)Instructions burned: 8176 (million) % 96.76/13.94 % (2315898)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=509339869:fmbsr=2:i=32576_2941 on theBenchmark for (2941ds/32576Mi) % 96.76/13.94 % (2315898)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 96.76/13.94 % (2315898)Terminated due to inappropriate strategy. % 96.76/13.94 % (2315898)------------------------------ % 96.76/13.94 % (2315898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.76/13.94 % (2315898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.76/13.94 % (2315898)CaDiCaL version: 2.1.3 % 96.76/13.94 % (2315898)Termination reason: Inappropriate % 96.76/13.94 % (2315898)Time elapsed: 0.007 s % 96.76/13.94 % (2315898)Peak memory usage: 11 MB % 96.76/13.94 % (2315898)Instructions burned: 16 (million) % 96.76/13.94 % (2315898)------------------------------ % 96.76/13.94 % (2315898)------------------------------ % 96.76/13.94 % (2315900)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3167647077:i=11404_2941 on theBenchmark for (2941ds/11404Mi) % 96.76/13.94 % (2315894)Instruction limit reached! % 96.76/13.94 % (2315894)------------------------------ % 96.76/13.94 % (2315894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.76/13.94 % (2315894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.76/13.94 % (2315894)CaDiCaL version: 2.1.3 % 96.76/13.94 % (2315894)Termination reason: Instruction limit % 96.76/13.94 % (2315894)Termination phase: Saturation % 96.76/13.94 % (2315894)Time elapsed: 3.490 s % 96.76/13.94 % (2315894)Peak memory usage: 18 MB % 96.76/13.94 % (2315894)Instructions burned: 9157 (million) % 96.76/13.94 % (2315902)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3299736015:i=14134_2920 on theBenchmark for (2920ds/14134Mi) % 96.76/13.94 % (2315900)Instruction limit reached! % 96.76/13.94 % (2315900)------------------------------ % 96.76/13.94 % (2315900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 96.76/13.94 % (2315900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.76/13.94 % (2315900)CaDiCaL version: 2.1.3 % 96.76/13.94 % (2315900)Termination reason: Instruction limit % 96.76/13.94 % (2315900)Termination phase: Saturation % 96.76/13.94 % (2315900)Time elapsed: 4.617 s % 96.76/13.94 % (2315900)Peak memory usage: 17 MB % 96.76/13.94 % (2315900)Instructions burned: 11405 (million) % 96.76/13.94 % (2315904)dis+33_16_sil=32000:sac=on:random_seed=2072525076:i=15851:nm=0_2895 on theBenchmark for (2895ds/15851Mi) % 96.76/13.94 % (2315890)Instruction limit reached! % 96.76/13.94 % (2315890)------------------------------ % 96.76/13.94 % (2315890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.94/23.93 % (2315890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.94/23.93 % (2315890)CaDiCaL version: 2.1.3 % 167.94/23.93 % (2315890)Termination reason: Instruction limit % 167.94/23.93 % (2315890)Termination phase: Saturation % 167.94/23.93 % (2315890)Time elapsed: 9.258 s % 167.94/23.93 % (2315890)Peak memory usage: 17 MB % 167.94/23.93 % (2315890)Instructions burned: 22566 (million) % 167.94/23.93 % (2315906)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=582830342:avsq=on:i=17627:add=on:amm=off_2881 on theBenchmark for (2881ds/17627Mi) % 167.94/23.93 % (2315896)Instruction limit reached! % 167.94/23.93 % (2315896)------------------------------ % 167.94/23.93 % (2315896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.94/23.93 % (2315896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.94/23.93 % (2315896)CaDiCaL version: 2.1.3 % 167.94/23.93 % (2315896)Termination reason: Instruction limit % 167.94/23.93 % (2315896)Termination phase: Saturation % 167.94/23.93 % (2315896)Time elapsed: 7.771 s % 167.94/23.93 % (2315896)Peak memory usage: 22 MB % 167.94/23.93 % (2315896)Instructions burned: 20141 (million) % 167.94/23.93 % (2315908)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2230581760:s2a=on:i=53295_2874 on theBenchmark for (2874ds/53295Mi) % 167.94/23.93 % (2315880)Instruction limit reached! % 167.94/23.93 % (2315880)------------------------------ % 167.94/23.93 % (2315880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.94/23.93 % (2315880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.94/23.93 % (2315880)CaDiCaL version: 2.1.3 % 167.94/23.93 % (2315880)Termination reason: Instruction limit % 167.94/23.93 % (2315880)Termination phase: Saturation % 167.94/23.93 % (2315880)Time elapsed: 11.177 s % 167.94/23.93 % (2315880)Peak memory usage: 25 MB % 167.94/23.93 % (2315880)Instructions burned: 29340 (million) % 167.94/23.93 % (2315910)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=225586691:i=26857:ins=20_2866 on theBenchmark for (2866ds/26857Mi) % 167.94/23.93 % (2315910)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.94/23.93 % (2315910)Terminated due to inappropriate strategy. % 167.94/23.93 % (2315910)------------------------------ % 167.94/23.93 % (2315910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.94/23.93 % (2315910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.94/23.93 % (2315910)CaDiCaL version: 2.1.3 % 167.94/23.93 % (2315910)Termination reason: Inappropriate % 167.94/23.93 % (2315910)Time elapsed: 0.007 s % 167.94/23.93 % (2315910)Peak memory usage: 10 MB % 167.94/23.93 % (2315910)Instructions burned: 16 (million) % 167.94/23.93 % (2315910)------------------------------ % 167.94/23.93 % (2315910)------------------------------ % 167.94/23.93 % (2315912)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2830719384:i=28120:bs=on:fsr=off_2865 on theBenchmark for (2865ds/28120Mi) % 167.94/23.93 % (2315902)Instruction limit reached! % 167.94/23.93 % (2315902)------------------------------ % 167.94/23.93 % (2315902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.94/23.93 % (2315902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.94/23.93 % (2315902)CaDiCaL version: 2.1.3 % 167.94/23.93 % (2315902)Termination reason: Instruction limit % 167.94/23.93 % (2315902)Termination phase: Saturation % 167.94/23.93 % (2315902)Time elapsed: 5.542 s % 167.94/23.93 % (2315902)Peak memory usage: 18 MB % 167.94/23.93 % (2315902)Instructions burned: 14135 (million) % 167.94/23.93 % (2315914)fmb+10_1_sil=256000:fmbss=7:random_seed=1205556147:fmbsr=1.6:i=182295_2864 on theBenchmark for (2864ds/182295Mi) % 167.94/23.93 % (2315914)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.94/23.93 % (2315914)Terminated due to inappropriate strategy. % 167.94/23.93 % (2315914)------------------------------ % 167.94/23.93 % (2315914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.94/23.93 % (2315914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.94/23.93 % (2315914)CaDiCaL version: 2.1.3 % 167.94/23.93 % (2315914)Termination reason: Inappropriate % 167.94/23.93 % (2315914)Time elapsed: 0.007 s % 167.94/23.93 % (2315914)Peak memory usage: 10 MB % 167.94/23.93 % (2315914)Instructions burned: 16 (million) % 167.94/23.93 % (2315914)------------------------------ % 167.94/23.93 % (2315914)------------------------------ % 167.94/23.93 % (2315916)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2027663886:i=44625:gsp=on_2864 on theBenchmark for (2864ds/44625Mi) % 183.63/26.17 % (2315916)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 183.63/26.17 % (2315916)Terminated due to inappropriate strategy. % 183.63/26.17 % (2315916)------------------------------ % 183.63/26.17 % (2315916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.63/26.17 % (2315916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.63/26.17 % (2315916)CaDiCaL version: 2.1.3 % 183.63/26.17 % (2315916)Termination reason: Inappropriate % 183.63/26.17 % (2315916)Time elapsed: 0.007 s % 183.63/26.17 % (2315916)Peak memory usage: 11 MB % 183.63/26.17 % (2315916)Instructions burned: 16 (million) % 183.63/26.17 % (2315916)------------------------------ % 183.63/26.17 % (2315916)------------------------------ % 183.63/26.17 % (2315918)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2992593208:i=160505_2864 on theBenchmark for (2864ds/160505Mi) % 183.63/26.17 % (2315918)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 183.63/26.17 % (2315918)Terminated due to inappropriate strategy. % 183.63/26.17 % (2315918)------------------------------ % 183.63/26.17 % (2315918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.63/26.17 % (2315918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.63/26.17 % (2315918)CaDiCaL version: 2.1.3 % 183.63/26.17 % (2315918)Termination reason: Inappropriate % 183.63/26.17 % (2315918)Time elapsed: 0.007 s % 183.63/26.17 % (2315918)Peak memory usage: 10 MB % 183.63/26.17 % (2315918)Instructions burned: 16 (million) % 183.63/26.17 % (2315918)------------------------------ % 183.63/26.17 % (2315918)------------------------------ % 183.63/26.17 % (2315920)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2835696281:fmbsr=1.3:i=225729_2864 on theBenchmark for (2864ds/225729Mi) % 183.63/26.17 % (2315920)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 183.63/26.17 % (2315920)Terminated due to inappropriate strategy. % 183.63/26.17 % (2315920)------------------------------ % 183.63/26.17 % (2315920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.63/26.17 % (2315920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.63/26.17 % (2315920)CaDiCaL version: 2.1.3 % 183.63/26.17 % (2315920)Termination reason: Inappropriate % 183.63/26.17 % (2315920)Time elapsed: 0.007 s % 183.63/26.17 % (2315920)Peak memory usage: 10 MB % 183.63/26.17 % (2315920)Instructions burned: 16 (million) % 183.63/26.17 % (2315920)------------------------------ % 183.63/26.17 % (2315920)------------------------------ % 183.63/26.17 % (2315922)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4005855579:fmbsr=2:i=185024:ins=7_2863 on theBenchmark for (2863ds/185024Mi) % 183.63/26.17 % (2315922)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 183.63/26.17 % (2315922)Terminated due to inappropriate strategy. % 183.63/26.17 % (2315922)------------------------------ % 183.63/26.17 % (2315922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.63/26.17 % (2315922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.63/26.17 % (2315922)CaDiCaL version: 2.1.3 % 183.63/26.17 % (2315922)Termination reason: Inappropriate % 183.63/26.17 % (2315922)Time elapsed: 0.007 s % 183.63/26.17 % (2315922)Peak memory usage: 10 MB % 183.63/26.17 % (2315922)Instructions burned: 16 (million) % 183.63/26.17 % (2315922)------------------------------ % 183.63/26.17 % (2315922)------------------------------ % 183.63/26.17 % (2315924)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=807617154:rtra=on_2863 on theBenchmark for (2863ds/0Mi) % 183.63/26.17 % (2315924)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 183.63/26.17 % (2315924)Terminated due to inappropriate strategy. % 183.63/26.17 % (2315924)------------------------------ % 183.63/26.17 % (2315924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.63/26.17 % (2315924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.63/26.17 % (2315924)CaDiCaL version: 2.1.3 % 183.63/26.17 % (2315924)Termination reason: Inappropriate % 183.63/26.17 % (2315924)Time elapsed: 0.007 s % 183.63/26.17 % (2315924)Peak memory usage: 11 MB % 183.63/26.17 % (2315924)Instructions burned: 16 (million) % 183.63/26.17 % (2315924)------------------------------ % 183.63/26.17 % (2315924)------------------------------ % 183.63/26.17 % (2315926)% WARNING: option uhcvi not known. % 183.63/26.17 % (2315926)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=204289284:i=271062:add=off:rtra=on:rawr=on_2863 on theBenchmark for (2863ds/271062Mi) % 214.48/30.42 % (2315904)Instruction limit reached! % 214.48/30.42 % (2315904)------------------------------ % 214.48/30.42 % (2315904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.48/30.42 % (2315904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.48/30.42 % (2315904)CaDiCaL version: 2.1.3 % 214.48/30.42 % (2315904)Termination reason: Instruction limit % 214.48/30.42 % (2315904)Termination phase: Saturation % 214.48/30.42 % (2315904)Time elapsed: 7.717 s % 214.48/30.42 % (2315904)Peak memory usage: 25 MB % 214.48/30.42 % (2315904)Instructions burned: 15851 (million) % 214.48/30.42 % (2316250)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3365991572:i=176048:add=on:rtra=on:rawr=on_2817 on theBenchmark for (2817ds/176048Mi) % 214.48/30.42 % (2315906)Instruction limit reached! % 214.48/30.42 % (2315906)------------------------------ % 214.48/30.42 % (2315906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.48/30.42 % (2315906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.48/30.42 % (2315906)CaDiCaL version: 2.1.3 % 214.48/30.42 % (2315906)Termination reason: Instruction limit % 214.48/30.42 % (2315906)Termination phase: Saturation % 214.48/30.42 % (2315906)Time elapsed: 10.984 s % 214.48/30.42 % (2315906)Peak memory usage: 103 MB % 214.48/30.42 % (2315906)Instructions burned: 17627 (million) % 214.48/30.42 % (2316270)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3880279895:i=206:fgj=on:rtra=on_2771 on theBenchmark for (2771ds/206Mi) % 214.48/30.42 % (2316270)Instruction limit reached! % 214.48/30.42 % (2316270)------------------------------ % 214.48/30.42 % (2316270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.48/30.42 % (2316270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.48/30.42 % (2316270)CaDiCaL version: 2.1.3 % 214.48/30.42 % (2316270)Termination reason: Instruction limit % 214.48/30.42 % (2316270)Termination phase: Saturation % 214.48/30.42 % (2316270)Time elapsed: 0.138 s % 214.48/30.42 % (2316270)Peak memory usage: 12 MB % 214.48/30.42 % (2316270)Instructions burned: 206 (million) % 214.48/30.42 % (2316272)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4162916068:i=232:rtra=on_2769 on theBenchmark for (2769ds/232Mi) % 214.48/30.42 % (2316272)Instruction limit reached! % 214.48/30.42 % (2316272)------------------------------ % 214.48/30.42 % (2316272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.48/30.42 % (2316272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.48/30.42 % (2316272)CaDiCaL version: 2.1.3 % 214.48/30.42 % (2316272)Termination reason: Instruction limit % 214.48/30.42 % (2316272)Termination phase: Saturation % 214.48/30.42 % (2316272)Time elapsed: 0.166 s % 214.48/30.42 % (2316272)Peak memory usage: 12 MB % 214.48/30.42 % (2316272)Instructions burned: 233 (million) % 214.48/30.42 % (2316274)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2944553838:i=262:rtra=on_2767 on theBenchmark for (2767ds/262Mi) % 214.48/30.42 % (2316274)Instruction limit reached! % 214.48/30.42 % (2316274)------------------------------ % 214.48/30.42 % (2316274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.48/30.42 % (2316274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.48/30.42 % (2316274)CaDiCaL version: 2.1.3 % 214.48/30.42 % (2316274)Termination reason: Instruction limit % 214.48/30.42 % (2316274)Termination phase: Saturation % 214.48/30.42 % (2316274)Time elapsed: 0.147 s % 214.48/30.42 % (2316274)Peak memory usage: 12 MB % 214.48/30.42 % (2316274)Instructions burned: 262 (million) % 214.48/30.42 % (2316276)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2022686417:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2766 on theBenchmark for (2766ds/318Mi) % 214.48/30.42 % (2316276)Instruction limit reached! % 214.48/30.42 % (2316276)------------------------------ % 214.48/30.42 % (2316276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.48/30.42 % (2316276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.48/30.42 % (2316276)CaDiCaL version: 2.1.3 % 214.48/30.42 % (2316276)Termination reason: Instruction limit % 214.48/30.42 % (2316276)Termination phase: Saturation % 214.48/30.42 % (2316276)Time elapsed: 0.250 s % 214.48/30.42 % (2316276)Peak memory usage: 13 MB % 214.48/30.42 % (2316276)Instructions burned: 319 (million) % 214.48/30.42 % (2316280)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2724672642:i=1428:nm=2:rtra=on_2763 on theBenchmark for (2763ds/1428Mi) % 247.64/35.13 % (2316280)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 247.64/35.13 % (2316280)Terminated due to inappropriate strategy. % 247.64/35.13 % (2316280)------------------------------ % 247.64/35.13 % (2316280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.64/35.13 % (2316280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.64/35.13 % (2316280)CaDiCaL version: 2.1.3 % 247.64/35.13 % (2316280)Termination reason: Inappropriate % 247.64/35.13 % (2316280)Time elapsed: 0.011 s % 247.64/35.13 % (2316280)Peak memory usage: 11 MB % 247.64/35.13 % (2316280)Instructions burned: 16 (million) % 247.64/35.13 % (2316280)------------------------------ % 247.64/35.13 % (2316280)------------------------------ % 247.64/35.13 % (2316283)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1016156166:i=262:bd=preordered:rtra=on:fsd=on_2763 on theBenchmark for (2763ds/262Mi) % 247.64/35.13 % (2316283)Instruction limit reached! % 247.64/35.13 % (2316283)------------------------------ % 247.64/35.13 % (2316283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.64/35.13 % (2316283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.64/35.13 % (2316283)CaDiCaL version: 2.1.3 % 247.64/35.13 % (2316283)Termination reason: Instruction limit % 247.64/35.13 % (2316283)Termination phase: Saturation % 247.64/35.13 % (2316283)Time elapsed: 0.197 s % 247.64/35.13 % (2316283)Peak memory usage: 12 MB % 247.64/35.13 % (2316283)Instructions burned: 262 (million) % 247.64/35.13 % (2316286)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=3168904594:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2760 on theBenchmark for (2760ds/1368Mi) % 247.64/35.13 % (2316286)Instruction limit reached! % 247.64/35.13 % (2316286)------------------------------ % 247.64/35.13 % (2316286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.64/35.13 % (2316286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.64/35.13 % (2316286)CaDiCaL version: 2.1.3 % 247.64/35.13 % (2316286)Termination reason: Instruction limit % 247.64/35.13 % (2316286)Termination phase: Saturation % 247.64/35.13 % (2316286)Time elapsed: 1.087 s % 247.64/35.13 % (2316286)Peak memory usage: 17 MB % 247.64/35.13 % (2316286)Instructions burned: 1369 (million) % 247.64/35.13 % (2316288)ott-21_1_sil=16000:si=on:fs=off:random_seed=612980554:i=360:av=off:fsr=off:rtra=on_2749 on theBenchmark for (2749ds/360Mi) % 247.64/35.13 % (2316288)Instruction limit reached! % 247.64/35.13 % (2316288)------------------------------ % 247.64/35.13 % (2316288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.64/35.13 % (2316288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.64/35.13 % (2316288)CaDiCaL version: 2.1.3 % 247.64/35.13 % (2316288)Termination reason: Instruction limit % 247.64/35.13 % (2316288)Termination phase: Saturation % 247.64/35.13 % (2316288)Time elapsed: 0.265 s % 247.64/35.13 % (2316288)Peak memory usage: 12 MB % 247.64/35.13 % (2316288)Instructions burned: 361 (million) % 247.64/35.13 % (2316290)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3493507123:i=954:bd=all:rtra=on_2746 on theBenchmark for (2746ds/954Mi) % 247.64/35.13 % (2316290)Instruction limit reached! % 247.64/35.13 % (2316290)------------------------------ % 247.64/35.13 % (2316290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.64/35.13 % (2316290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.64/35.13 % (2316290)CaDiCaL version: 2.1.3 % 247.64/35.13 % (2316290)Termination reason: Instruction limit % 247.64/35.13 % (2316290)Termination phase: Saturation % 247.64/35.13 % (2316290)Time elapsed: 0.501 s % 247.64/35.13 % (2316290)Peak memory usage: 13 MB % 247.64/35.13 % (2316290)Instructions burned: 955 (million) % 247.64/35.13 % (2316296)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1148146647:fmbsr=1.3:i=1730:ins=25:rtra=on_2741 on theBenchmark for (2741ds/1730Mi) % 247.64/35.13 % (2316296)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 247.64/35.13 % (2316296)Terminated due to inappropriate strategy. % 247.64/35.13 % (2316296)------------------------------ % 247.64/35.13 % (2316296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.64/35.13 % (2316296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.64/35.13 % (2316296)CaDiCaL version: 2.1.3 % 247.64/35.13 % (2316296)Termination reason: InapprTerminated % 300.69/42.54 % Vampire exiting % 300.69/42.54 Terminated %------------------------------------------------------------------------------