%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC484_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:06:03 PM UTC 2026 % Result : Timeout 300.11s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC484_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.12/0.18 % Computer : n016.cluster.edu % 0.12/0.18 % Model : x86_64 x86_64 % 0.12/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.18 % Memory : 8046.5625MB % 0.12/0.18 % OS : Linux 6.8.0-71-generic % 0.12/0.18 % CPULimit : 300 % 0.12/0.18 % WCLimit : 300 % 0.12/0.18 % DateTime : Mon Sep 28 09:45:34 UTC 2026 % 0.12/0.19 % CPUTime : % 0.12/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.12/0.21 Running first-order model finding % 0.12/0.21 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 % 6.91/1.21 % (3514764)Will run a generic schedule for satisfiability detection. % 6.91/1.21 % (3514770)% WARNING: option uhcvi not known. % 6.91/1.21 % (3514770)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1172503967:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.91/1.21 % (3514772)dis+10_1_sil=32000:sp=arity:random_seed=81302118:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.91/1.21 % (3514775)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=288382085:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.91/1.21 % (3514773)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3030108029:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.91/1.21 % (3514769)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=998901093_2999 on theBenchmark for (2999ds/0Mi) % 6.91/1.21 % (3514769)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.91/1.21 % (3514769)Terminated due to inappropriate strategy. % 6.91/1.21 % (3514769)------------------------------ % 6.91/1.21 % (3514769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.91/1.21 % (3514769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.21 % (3514769)CaDiCaL version: 2.1.3 % 6.91/1.21 % (3514769)Termination reason: Inappropriate % 6.91/1.21 % (3514769)Time elapsed: 0.001 s % 6.91/1.21 % (3514771)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=404920650:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.91/1.21 % (3514769)Peak memory usage: 10 MB % 6.91/1.21 % (3514769)Instructions burned: 1 (million) % 6.91/1.21 % (3514774)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3543455580:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.91/1.21 % (3514769)------------------------------ % 6.91/1.21 % (3514769)------------------------------ % 6.91/1.21 % (3514791)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1133859360:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.91/1.21 % (3514791)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.91/1.21 % (3514791)Terminated due to inappropriate strategy. % 6.91/1.21 % (3514791)------------------------------ % 6.91/1.21 % (3514791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.91/1.21 % (3514791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.21 % (3514791)CaDiCaL version: 2.1.3 % 6.91/1.21 % (3514791)Termination reason: Inappropriate % 6.91/1.21 % (3514791)Time elapsed: 0.001 s % 6.91/1.21 % (3514791)Peak memory usage: 10 MB % 6.91/1.21 % (3514791)Instructions burned: 1 (million) % 6.91/1.21 % (3514791)------------------------------ % 6.91/1.21 % (3514791)------------------------------ % 6.91/1.21 % (3514773)Instruction limit reached! % 6.91/1.21 % (3514773)------------------------------ % 6.91/1.21 % (3514773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.91/1.21 % (3514773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.21 % (3514773)CaDiCaL version: 2.1.3 % 6.91/1.21 % (3514773)Termination reason: Instruction limit % 6.91/1.21 % (3514773)Termination phase: Saturation % 6.91/1.21 % (3514773)Time elapsed: 0.079 s % 6.91/1.21 % (3514773)Peak memory usage: 12 MB % 6.91/1.21 % (3514773)Instructions burned: 117 (million) % 6.91/1.21 % (3514793)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1081580301:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.91/1.21 % (3514794)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=229991015:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.91/1.21 % (3514772)Instruction limit reached! % 6.91/1.21 % (3514772)------------------------------ % 6.91/1.21 % (3514772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.91/1.21 % (3514772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.21 % (3514772)CaDiCaL version: 2.1.3 % 6.91/1.21 % (3514772)Termination reason: Instruction limit % 6.91/1.21 % (3514772)Termination phase: Saturation % 6.91/1.21 % (3514772)Time elapsed: 0.104 s % 6.91/1.21 % (3514772)Peak memory usage: 12 MB % 6.91/1.21 % (3514772)Instructions burned: 103 (million) % 6.91/1.21 % (3514774)Instruction limit reached! % 6.91/1.21 % (3514774)------------------------------ % 6.91/1.21 % (3514774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.15/1.64 % (3514774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.15/1.64 % (3514774)CaDiCaL version: 2.1.3 % 9.15/1.64 % (3514774)Termination reason: Instruction limit % 9.15/1.64 % (3514774)Termination phase: Saturation % 9.15/1.64 % (3514774)Time elapsed: 0.124 s % 9.15/1.64 % (3514774)Peak memory usage: 13 MB % 9.15/1.64 % (3514774)Instructions burned: 131 (million) % 9.15/1.64 % (3514797)ott-21_1_sil=16000:fs=off:random_seed=788370358:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 9.15/1.64 % (3514775)Instruction limit reached! % 9.15/1.64 % (3514775)------------------------------ % 9.15/1.64 % (3514775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.15/1.64 % (3514775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.15/1.64 % (3514775)CaDiCaL version: 2.1.3 % 9.15/1.64 % (3514775)Termination reason: Instruction limit % 9.15/1.64 % (3514775)Termination phase: Saturation % 9.15/1.64 % (3514775)Time elapsed: 0.152 s % 9.15/1.64 % (3514775)Peak memory usage: 13 MB % 9.15/1.64 % (3514775)Instructions burned: 159 (million) % 9.15/1.64 % (3514798)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2292726667:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 9.15/1.64 % (3514800)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3522454038:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 9.15/1.64 % (3514800)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.15/1.64 % (3514800)Terminated due to inappropriate strategy. % 9.15/1.64 % (3514800)------------------------------ % 9.15/1.64 % (3514800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.15/1.64 % (3514800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.15/1.64 % (3514800)CaDiCaL version: 2.1.3 % 9.15/1.64 % (3514800)Termination reason: Inappropriate % 9.15/1.64 % (3514800)Time elapsed: 0.001 s % 9.15/1.64 % (3514800)Peak memory usage: 10 MB % 9.15/1.64 % (3514800)Instructions burned: 1 (million) % 9.15/1.64 % (3514800)------------------------------ % 9.15/1.64 % (3514800)------------------------------ % 9.15/1.64 % (3514803)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1292637811:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 9.15/1.64 % (3514793)Instruction limit reached! % 9.15/1.64 % (3514793)------------------------------ % 9.15/1.64 % (3514793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.15/1.64 % (3514793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.15/1.64 % (3514793)CaDiCaL version: 2.1.3 % 9.15/1.64 % (3514793)Termination reason: Instruction limit % 9.15/1.64 % (3514793)Termination phase: Saturation % 9.15/1.64 % (3514793)Time elapsed: 0.126 s % 9.15/1.64 % (3514793)Peak memory usage: 12 MB % 9.15/1.64 % (3514793)Instructions burned: 132 (million) % 9.15/1.64 % (3514811)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3301402753:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 9.15/1.64 % (3514811)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.15/1.64 % (3514811)Terminated due to inappropriate strategy. % 9.15/1.64 % (3514811)------------------------------ % 9.15/1.64 % (3514811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.15/1.64 % (3514811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.15/1.64 % (3514811)CaDiCaL version: 2.1.3 % 9.15/1.64 % (3514811)Termination reason: Inappropriate % 9.15/1.64 % (3514811)Time elapsed: 0.002 s % 9.15/1.64 % (3514811)Peak memory usage: 10 MB % 9.15/1.64 % (3514811)Instructions burned: 1 (million) % 9.15/1.64 % (3514811)------------------------------ % 9.15/1.64 % (3514811)------------------------------ % 9.15/1.64 % (3514797)Instruction limit reached! % 9.15/1.64 % (3514797)------------------------------ % 9.15/1.64 % (3514797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.15/1.64 % (3514797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.15/1.64 % (3514797)CaDiCaL version: 2.1.3 % 9.15/1.64 % (3514797)Termination reason: Instruction limit % 9.15/1.64 % (3514797)Termination phase: Saturation % 9.15/1.64 % (3514797)Time elapsed: 0.138 s % 9.15/1.64 % (3514797)Peak memory usage: 12 MB % 9.15/1.64 % (3514797)Instructions burned: 181 (million) % 9.15/1.64 % (3514816)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=3756524724:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 25.24/3.99 % (3514817)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2280637415:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 25.24/3.99 % (3514798)Instruction limit reached! % 25.24/3.99 % (3514798)------------------------------ % 25.24/3.99 % (3514798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.24/3.99 % (3514798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.24/3.99 % (3514798)CaDiCaL version: 2.1.3 % 25.24/3.99 % (3514798)Termination reason: Instruction limit % 25.24/3.99 % (3514798)Termination phase: Saturation % 25.24/3.99 % (3514798)Time elapsed: 0.465 s % 25.24/3.99 % (3514798)Peak memory usage: 14 MB % 25.24/3.99 % (3514798)Instructions burned: 477 (million) % 25.24/3.99 % (3514835)fmb+10_1_sil=64000:random_seed=2667540956:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 25.24/3.99 % (3514835)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.24/3.99 % (3514835)Terminated due to inappropriate strategy. % 25.24/3.99 % (3514835)------------------------------ % 25.24/3.99 % (3514835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.24/3.99 % (3514835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.24/3.99 % (3514835)CaDiCaL version: 2.1.3 % 25.24/3.99 % (3514835)Termination reason: Inappropriate % 25.24/3.99 % (3514835)Time elapsed: 0.001 s % 25.24/3.99 % (3514835)Peak memory usage: 11 MB % 25.24/3.99 % (3514835)Instructions burned: 1 (million) % 25.24/3.99 % (3514835)------------------------------ % 25.24/3.99 % (3514835)------------------------------ % 25.24/3.99 % (3514794)Instruction limit reached! % 25.24/3.99 % (3514794)------------------------------ % 25.24/3.99 % (3514794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.24/3.99 % (3514794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.24/3.99 % (3514794)CaDiCaL version: 2.1.3 % 25.24/3.99 % (3514794)Termination reason: Instruction limit % 25.24/3.99 % (3514794)Termination phase: Saturation % 25.24/3.99 % (3514794)Time elapsed: 0.579 s % 25.24/3.99 % (3514794)Peak memory usage: 18 MB % 25.24/3.99 % (3514794)Instructions burned: 685 (million) % 25.24/3.99 % (3514838)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3137835882:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 25.24/3.99 % (3514838)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.24/3.99 % (3514838)Terminated due to inappropriate strategy. % 25.24/3.99 % (3514838)------------------------------ % 25.24/3.99 % (3514838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.24/3.99 % (3514838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.24/3.99 % (3514838)CaDiCaL version: 2.1.3 % 25.24/3.99 % (3514838)Termination reason: Inappropriate % 25.24/3.99 % (3514838)Time elapsed: 0.001 s % 25.24/3.99 % (3514838)Peak memory usage: 11 MB % 25.24/3.99 % (3514838)Instructions burned: 1 (million) % 25.24/3.99 % (3514838)------------------------------ % 25.24/3.99 % (3514838)------------------------------ % 25.24/3.99 % (3514839)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=309055220:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 25.24/3.99 % (3514839)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 25.24/3.99 % (3514839)Terminated due to inappropriate strategy. % 25.24/3.99 % (3514839)------------------------------ % 25.24/3.99 % (3514839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.24/3.99 % (3514839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.24/3.99 % (3514839)CaDiCaL version: 2.1.3 % 25.24/3.99 % (3514839)Termination reason: Inappropriate % 25.24/3.99 % (3514839)Time elapsed: 0.001 s % 25.24/3.99 % (3514839)Peak memory usage: 11 MB % 25.24/3.99 % (3514839)Instructions burned: 1 (million) % 25.24/3.99 % (3514839)------------------------------ % 25.24/3.99 % (3514839)------------------------------ % 25.24/3.99 % (3514841)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2471177792:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 25.24/3.99 % (3514844)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4182983840:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 25.24/3.99 % (3514816)Instruction limit reached! % 25.24/3.99 % (3514816)------------------------------ % 39.56/5.87 % (3514816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.56/5.87 % (3514816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.56/5.87 % (3514816)CaDiCaL version: 2.1.3 % 39.56/5.87 % (3514816)Termination reason: Instruction limit % 39.56/5.87 % (3514816)Termination phase: Saturation % 39.56/5.87 % (3514816)Time elapsed: 0.653 s % 39.56/5.87 % (3514816)Peak memory usage: 19 MB % 39.56/5.87 % (3514816)Instructions burned: 692 (million) % 39.56/5.87 % (3514856)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1121553624:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 39.56/5.87 % (3514856)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.56/5.87 % (3514856)Terminated due to inappropriate strategy. % 39.56/5.87 % (3514856)------------------------------ % 39.56/5.87 % (3514856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.56/5.87 % (3514856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.56/5.87 % (3514856)CaDiCaL version: 2.1.3 % 39.56/5.87 % (3514856)Termination reason: Inappropriate % 39.56/5.87 % (3514856)Time elapsed: 0.001 s % 39.56/5.87 % (3514856)Peak memory usage: 10 MB % 39.56/5.87 % (3514856)Instructions burned: 1 (million) % 39.56/5.87 % (3514856)------------------------------ % 39.56/5.87 % (3514856)------------------------------ % 39.56/5.87 % (3514860)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4209949894:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 39.56/5.87 % (3514860)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.56/5.87 % (3514860)Terminated due to inappropriate strategy. % 39.56/5.87 % (3514860)------------------------------ % 39.56/5.87 % (3514860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.56/5.87 % (3514860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.56/5.87 % (3514860)CaDiCaL version: 2.1.3 % 39.56/5.87 % (3514860)Termination reason: Inappropriate % 39.56/5.87 % (3514860)Time elapsed: 0.002 s % 39.56/5.87 % (3514860)Peak memory usage: 10 MB % 39.56/5.87 % (3514860)Instructions burned: 1 (million) % 39.56/5.87 % (3514860)------------------------------ % 39.56/5.87 % (3514860)------------------------------ % 39.56/5.87 % (3514817)Instruction limit reached! % 39.56/5.87 % (3514817)------------------------------ % 39.56/5.87 % (3514817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.56/5.87 % (3514817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.56/5.87 % (3514817)CaDiCaL version: 2.1.3 % 39.56/5.87 % (3514817)Termination reason: Instruction limit % 39.56/5.87 % (3514817)Termination phase: Saturation % 39.56/5.87 % (3514817)Time elapsed: 0.740 s % 39.56/5.87 % (3514817)Peak memory usage: 19 MB % 39.56/5.87 % (3514817)Instructions burned: 879 (million) % 39.56/5.87 % (3514865)ott-2_1_sil=16000:newcnf=on:random_seed=3047351893:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 39.56/5.87 % (3514867)ott+10_1_sil=32000:tgt=ground:random_seed=119231863:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 39.56/5.87 % (3514803)Instruction limit reached! % 39.56/5.87 % (3514803)------------------------------ % 39.56/5.87 % (3514803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.56/5.87 % (3514803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.56/5.87 % (3514803)CaDiCaL version: 2.1.3 % 39.56/5.87 % (3514803)Termination reason: Instruction limit % 39.56/5.87 % (3514803)Termination phase: Saturation % 39.56/5.87 % (3514803)Time elapsed: 1.151 s % 39.56/5.87 % (3514803)Peak memory usage: 20 MB % 39.56/5.87 % (3514803)Instructions burned: 1180 (million) % 39.56/5.87 % (3514881)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1126462690:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 39.56/5.87 % (3514881)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.56/5.87 % (3514881)Terminated due to inappropriate strategy. % 39.56/5.87 % (3514881)------------------------------ % 39.56/5.87 % (3514881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.56/5.87 % (3514881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.56/5.87 % (3514881)CaDiCaL version: 2.1.3 % 39.56/5.87 % (3514881)Termination reason: Inappropriate % 39.56/5.87 % (3514881)Time elapsed: 0.001 s % 39.56/5.87 % (3514881)Peak memory usage: 10 MB % 39.56/5.87 % (3514881)Instructions burned: 1 (million) % 120.49/17.21 % (3514881)------------------------------ % 120.49/17.21 % (3514881)------------------------------ % 120.49/17.21 % (3514883)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=511420964:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 120.49/17.21 % (3514865)Instruction limit reached! % 120.49/17.21 % (3514865)------------------------------ % 120.49/17.21 % (3514865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.49/17.21 % (3514865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.49/17.21 % (3514865)CaDiCaL version: 2.1.3 % 120.49/17.21 % (3514865)Termination reason: Instruction limit % 120.49/17.21 % (3514865)Termination phase: Saturation % 120.49/17.21 % (3514865)Time elapsed: 0.617 s % 120.49/17.21 % (3514865)Peak memory usage: 14 MB % 120.49/17.21 % (3514865)Instructions burned: 870 (million) % 120.49/17.21 % (3514886)dis+21_1_sil=32000:sas=cadical:random_seed=714156413:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi) % 120.49/17.21 % (3514844)Instruction limit reached! % 120.49/17.21 % (3514844)------------------------------ % 120.49/17.21 % (3514844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.49/17.21 % (3514844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.49/17.21 % (3514844)CaDiCaL version: 2.1.3 % 120.49/17.21 % (3514844)Termination reason: Instruction limit % 120.49/17.21 % (3514844)Termination phase: Saturation % 120.49/17.21 % (3514844)Time elapsed: 1.136 s % 120.49/17.21 % (3514844)Peak memory usage: 22 MB % 120.49/17.21 % (3514844)Instructions burned: 1472 (million) % 120.49/17.21 % (3514953)ott+11_1_sil=16000:gs=on:random_seed=1967753542:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2980 on theBenchmark for (2980ds/2251Mi) % 120.49/17.21 % (3514953)Instruction limit reached! % 120.49/17.21 % (3514953)------------------------------ % 120.49/17.21 % (3514953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.49/17.21 % (3514953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.49/17.21 % (3514953)CaDiCaL version: 2.1.3 % 120.49/17.21 % (3514953)Termination reason: Instruction limit % 120.49/17.21 % (3514953)Termination phase: Saturation % 120.49/17.21 % (3514953)Time elapsed: 1.263 s % 120.49/17.21 % (3514953)Peak memory usage: 22 MB % 120.49/17.21 % (3514953)Instructions burned: 2251 (million) % 120.49/17.21 % (3515042)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1144468584:fmbsr=1.6:i=67534_2968 on theBenchmark for (2968ds/67534Mi) % 120.49/17.21 % (3515042)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.49/17.21 % (3515042)Terminated due to inappropriate strategy. % 120.49/17.21 % (3515042)------------------------------ % 120.49/17.21 % (3515042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.49/17.21 % (3515042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.49/17.21 % (3515042)CaDiCaL version: 2.1.3 % 120.49/17.21 % (3515042)Termination reason: Inappropriate % 120.49/17.21 % (3515042)Time elapsed: 0.001 s % 120.49/17.21 % (3515042)Peak memory usage: 10 MB % 120.49/17.21 % (3515042)Instructions burned: 1 (million) % 120.49/17.21 % (3515042)------------------------------ % 120.49/17.21 % (3515042)------------------------------ % 120.49/17.21 % (3515044)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2771004977:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2967 on theBenchmark for (2967ds/4591Mi) % 120.49/17.21 % (3514883)Instruction limit reached! % 120.49/17.21 % (3514883)------------------------------ % 120.49/17.21 % (3514883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.49/17.21 % (3514883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.49/17.21 % (3514883)CaDiCaL version: 2.1.3 % 120.49/17.21 % (3514883)Termination reason: Instruction limit % 120.49/17.21 % (3514883)Termination phase: Saturation % 120.49/17.21 % (3514883)Time elapsed: 1.881 s % 120.49/17.21 % (3514883)Peak memory usage: 35 MB % 120.49/17.21 % (3514883)Instructions burned: 3512 (million) % 120.49/17.21 % (3515046)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2599262847:i=29340_2966 on theBenchmark for (2966ds/29340Mi) % 120.49/17.21 % (3514886)Instruction limit reached! % 120.49/17.21 % (3514886)------------------------------ % 120.49/17.21 % (3514886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.49/17.21 % (3514886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.49/17.21 % (3514886)CaDiCaL version: 2.1.3 % 120.49/17.21 % (3514886)Termination reason: Instruction limit % 137.49/19.68 % (3514886)Termination phase: Saturation % 137.49/19.68 % (3514886)Time elapsed: 2.030 s % 137.49/19.68 % (3514886)Peak memory usage: 31 MB % 137.49/19.68 % (3514886)Instructions burned: 3775 (million) % 137.49/19.68 % (3514841)Instruction limit reached! % 137.49/19.68 % (3514841)------------------------------ % 137.49/19.68 % (3514841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.49/19.68 % (3514841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.49/19.68 % (3514841)CaDiCaL version: 2.1.3 % 137.49/19.68 % (3514841)Termination reason: Instruction limit % 137.49/19.68 % (3514841)Termination phase: Saturation % 137.49/19.68 % (3514841)Time elapsed: 3.018 s % 137.49/19.68 % (3514841)Peak memory usage: 41 MB % 137.49/19.68 % (3514841)Instructions burned: 5132 (million) % 137.49/19.68 % (3515048)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3390382292:i=5211_2962 on theBenchmark for (2962ds/5211Mi) % 137.49/19.68 % (3515049)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3924456672:i=5497:nm=2_2962 on theBenchmark for (2962ds/5497Mi) % 137.49/19.68 % (3515049)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.49/19.68 % (3515049)Terminated due to inappropriate strategy. % 137.49/19.68 % (3515049)------------------------------ % 137.49/19.68 % (3515049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.49/19.68 % (3515049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.49/19.68 % (3515049)CaDiCaL version: 2.1.3 % 137.49/19.68 % (3515049)Termination reason: Inappropriate % 137.49/19.68 % (3515049)Time elapsed: 0.001 s % 137.49/19.68 % (3515049)Peak memory usage: 11 MB % 137.49/19.68 % (3515049)Instructions burned: 1 (million) % 137.49/19.68 % (3515049)------------------------------ % 137.49/19.68 % (3515049)------------------------------ % 137.49/19.68 % (3515052)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1792186518:fmbsr=2:i=46332_2961 on theBenchmark for (2961ds/46332Mi) % 137.49/19.68 % (3515052)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.49/19.68 % (3515052)Terminated due to inappropriate strategy. % 137.49/19.68 % (3515052)------------------------------ % 137.49/19.68 % (3515052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.49/19.68 % (3515052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.49/19.68 % (3515052)CaDiCaL version: 2.1.3 % 137.49/19.68 % (3515052)Termination reason: Inappropriate % 137.49/19.68 % (3515052)Time elapsed: 0.001 s % 137.49/19.68 % (3515052)Peak memory usage: 11 MB % 137.49/19.68 % (3515052)Instructions burned: 1 (million) % 137.49/19.68 % (3515052)------------------------------ % 137.49/19.68 % (3515052)------------------------------ % 137.49/19.68 % (3515054)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3275668194:i=14071_2961 on theBenchmark for (2961ds/14071Mi) % 137.49/19.68 % (3515054)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 137.49/19.68 % (3515054)Terminated due to inappropriate strategy. % 137.49/19.68 % (3515054)------------------------------ % 137.49/19.68 % (3515054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.49/19.68 % (3515054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.49/19.68 % (3515054)CaDiCaL version: 2.1.3 % 137.49/19.68 % (3515054)Termination reason: Inappropriate % 137.49/19.68 % (3515054)Time elapsed: 0.001 s % 137.49/19.68 % (3515054)Peak memory usage: 10 MB % 137.49/19.68 % (3515054)Instructions burned: 1 (million) % 137.49/19.68 % (3515054)------------------------------ % 137.49/19.68 % (3515054)------------------------------ % 137.49/19.68 % (3515056)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3082321352:i=22565:add=on:rawr=on_2961 on theBenchmark for (2961ds/22565Mi) % 137.49/19.68 % (3514867)Instruction limit reached! % 137.49/19.68 % (3514867)------------------------------ % 137.49/19.68 % (3514867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 137.49/19.68 % (3514867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.49/19.68 % (3514867)CaDiCaL version: 2.1.3 % 137.49/19.68 % (3514867)Termination reason: Instruction limit % 137.49/19.68 % (3514867)Termination phase: Saturation % 137.49/19.68 % (3514867)Time elapsed: 3.386 s % 137.49/19.68 % (3514867)Peak memory usage: 40 MB % 137.49/19.68 % (3514867)Instructions burned: 5114 (million) % 137.49/19.68 % (3515058)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1190020029:i=8173:av=off_2954 on theBenchmark for (2954ds/8173Mi) % 137.49/19.68 % (3515044)Instruction limit reached! % 138.11/19.79 % (3515044)------------------------------ % 138.11/19.79 % (3515044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.11/19.79 % (3515044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.11/19.79 % (3515044)CaDiCaL version: 2.1.3 % 138.11/19.79 % (3515044)Termination reason: Instruction limit % 138.11/19.79 % (3515044)Termination phase: Saturation % 138.11/19.79 % (3515044)Time elapsed: 2.408 s % 138.11/19.79 % (3515044)Peak memory usage: 49 MB % 138.11/19.79 % (3515044)Instructions burned: 4592 (million) % 138.11/19.79 % (3515060)dis+10_16:1_sil=16000:random_seed=3936939596:i=9155:fsr=off_2943 on theBenchmark for (2943ds/9155Mi) % 138.11/19.79 % (3515048)Instruction limit reached! % 138.11/19.79 % (3515048)------------------------------ % 138.11/19.79 % (3515048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.11/19.79 % (3515048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.11/19.79 % (3515048)CaDiCaL version: 2.1.3 % 138.11/19.79 % (3515048)Termination reason: Instruction limit % 138.11/19.79 % (3515048)Termination phase: Saturation % 138.11/19.79 % (3515048)Time elapsed: 2.737 s % 138.11/19.79 % (3515048)Peak memory usage: 47 MB % 138.11/19.79 % (3515048)Instructions burned: 5212 (million) % 138.11/19.79 % (3515062)ott-3_8_sil=64000:random_seed=1934231319:i=20139:bs=on_2934 on theBenchmark for (2934ds/20139Mi) % 138.11/19.79 % (3515058)Instruction limit reached! % 138.11/19.79 % (3515058)------------------------------ % 138.11/19.79 % (3515058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.11/19.79 % (3515058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.11/19.79 % (3515058)CaDiCaL version: 2.1.3 % 138.11/19.79 % (3515058)Termination reason: Instruction limit % 138.11/19.79 % (3515058)Termination phase: Saturation % 138.11/19.79 % (3515058)Time elapsed: 5.136 s % 138.11/19.79 % (3515058)Peak memory usage: 54 MB % 138.11/19.79 % (3515058)Instructions burned: 8173 (million) % 138.11/19.79 % (3515064)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=587543624:fmbsr=2:i=32576_2903 on theBenchmark for (2903ds/32576Mi) % 138.11/19.79 % (3515064)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 138.11/19.79 % (3515064)Terminated due to inappropriate strategy. % 138.11/19.79 % (3515064)------------------------------ % 138.11/19.79 % (3515064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.11/19.79 % (3515064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.11/19.79 % (3515064)CaDiCaL version: 2.1.3 % 138.11/19.79 % (3515064)Termination reason: Inappropriate % 138.11/19.79 % (3515064)Time elapsed: 0.001 s % 138.11/19.79 % (3515064)Peak memory usage: 10 MB % 138.11/19.79 % (3515064)Instructions burned: 1 (million) % 138.11/19.79 % (3515064)------------------------------ % 138.11/19.79 % (3515064)------------------------------ % 138.11/19.79 % (3515066)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3401294528:i=11404_2903 on theBenchmark for (2903ds/11404Mi) % 138.11/19.79 % (3515060)Instruction limit reached! % 138.11/19.79 % (3515060)------------------------------ % 138.11/19.79 % (3515060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.11/19.79 % (3515060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.11/19.79 % (3515060)CaDiCaL version: 2.1.3 % 138.11/19.79 % (3515060)Termination reason: Instruction limit % 138.11/19.79 % (3515060)Termination phase: Saturation % 138.11/19.79 % (3515060)Time elapsed: 4.634 s % 138.11/19.79 % (3515060)Peak memory usage: 51 MB % 138.11/19.79 % (3515060)Instructions burned: 9155 (million) % 138.11/19.79 % (3515068)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=863953245:i=14134_2896 on theBenchmark for (2896ds/14134Mi) % 138.11/19.79 % (3515056)Instruction limit reached! % 138.11/19.79 % (3515056)------------------------------ % 138.11/19.79 % (3515056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 138.11/19.79 % (3515056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.11/19.79 % (3515056)CaDiCaL version: 2.1.3 % 138.11/19.79 % (3515056)Termination reason: Instruction limit % 138.11/19.79 % (3515056)Termination phase: Saturation % 138.11/19.79 % (3515056)Time elapsed: 9.339 s % 138.11/19.79 % (3515056)Peak memory usage: 62 MB % 138.11/19.79 % (3515056)Instructions burned: 22568 (million) % 138.11/19.79 % (3515202)dis+33_16_sil=32000:sac=on:random_seed=3833309562:i=15851:nm=0_2867 on theBenchmark for (2867ds/15851Mi) % 138.11/19.79 % (3515066)Instruction limit reached! % 138.11/19.79 % (3515066)------------------------------ % 138.11/19.79 % (3515066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.69/27.48 % (3515066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.69/27.48 % (3515066)CaDiCaL version: 2.1.3 % 192.69/27.48 % (3515066)Termination reason: Instruction limit % 192.69/27.48 % (3515066)Termination phase: Saturation % 192.69/27.48 % (3515066)Time elapsed: 7.281 s % 192.69/27.48 % (3515066)Peak memory usage: 61 MB % 192.69/27.48 % (3515066)Instructions burned: 11405 (million) % 192.69/27.48 % (3515505)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1908704129:avsq=on:i=17627:add=on:amm=off_2830 on theBenchmark for (2830ds/17627Mi) % 192.69/27.48 % (3515046)Instruction limit reached! % 192.69/27.48 % (3515046)------------------------------ % 192.69/27.48 % (3515046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.69/27.48 % (3515046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.69/27.48 % (3515046)CaDiCaL version: 2.1.3 % 192.69/27.48 % (3515046)Termination reason: Instruction limit % 192.69/27.48 % (3515046)Termination phase: Saturation % 192.69/27.48 % (3515046)Time elapsed: 14.519 s % 192.69/27.48 % (3515046)Peak memory usage: 120 MB % 192.69/27.48 % (3515046)Instructions burned: 29341 (million) % 192.69/27.48 % (3515507)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=796995349:s2a=on:i=53295_2821 on theBenchmark for (2821ds/53295Mi) % 192.69/27.48 % (3515068)Instruction limit reached! % 192.69/27.48 % (3515068)------------------------------ % 192.69/27.48 % (3515068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.69/27.48 % (3515068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.69/27.48 % (3515068)CaDiCaL version: 2.1.3 % 192.69/27.48 % (3515068)Termination reason: Instruction limit % 192.69/27.48 % (3515068)Termination phase: Saturation % 192.69/27.48 % (3515068)Time elapsed: 8.990 s % 192.69/27.48 % (3515068)Peak memory usage: 70 MB % 192.69/27.48 % (3515068)Instructions burned: 14134 (million) % 192.69/27.48 % (3515509)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2046605474:i=26857:ins=20_2806 on theBenchmark for (2806ds/26857Mi) % 192.69/27.48 % (3515509)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.69/27.48 % (3515509)Terminated due to inappropriate strategy. % 192.69/27.48 % (3515509)------------------------------ % 192.69/27.48 % (3515509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.69/27.48 % (3515509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.69/27.48 % (3515509)CaDiCaL version: 2.1.3 % 192.69/27.48 % (3515509)Termination reason: Inappropriate % 192.69/27.48 % (3515509)Time elapsed: 0.001 s % 192.69/27.48 % (3515509)Peak memory usage: 10 MB % 192.69/27.48 % (3515509)Instructions burned: 1 (million) % 192.69/27.48 % (3515509)------------------------------ % 192.69/27.48 % (3515509)------------------------------ % 192.69/27.48 % (3515511)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1520718757:i=28120:bs=on:fsr=off_2806 on theBenchmark for (2806ds/28120Mi) % 192.69/27.48 % (3515062)Instruction limit reached! % 192.69/27.48 % (3515062)------------------------------ % 192.69/27.48 % (3515062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.69/27.48 % (3515062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.69/27.48 % (3515062)CaDiCaL version: 2.1.3 % 192.69/27.48 % (3515062)Termination reason: Instruction limit % 192.69/27.48 % (3515062)Termination phase: Saturation % 192.69/27.48 % (3515062)Time elapsed: 12.865 s % 192.69/27.48 % (3515062)Peak memory usage: 63 MB % 192.69/27.48 % (3515062)Instructions burned: 20140 (million) % 192.69/27.48 % (3515513)fmb+10_1_sil=256000:fmbss=7:random_seed=3393524847:fmbsr=1.6:i=182295_2805 on theBenchmark for (2805ds/182295Mi) % 192.69/27.48 % (3515513)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.69/27.48 % (3515513)Terminated due to inappropriate strategy. % 192.69/27.48 % (3515513)------------------------------ % 192.69/27.48 % (3515513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.69/27.48 % (3515513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.69/27.48 % (3515513)CaDiCaL version: 2.1.3 % 192.69/27.48 % (3515513)Termination reason: Inappropriate % 192.69/27.48 % (3515513)Time elapsed: 0.001 s % 192.69/27.48 % (3515513)Peak memory usage: 10 MB % 192.69/27.48 % (3515513)Instructions burned: 1 (million) % 192.69/27.48 % (3515513)------------------------------ % 192.69/27.48 % (3515513)------------------------------ % 192.69/27.48 % (3515515)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3013935573:i=44625:gsp=on_2805 on theBenchmark for (2805ds/44625Mi) % 207.10/29.46 % (3515515)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.10/29.46 % (3515515)Terminated due to inappropriate strategy. % 207.10/29.46 % (3515515)------------------------------ % 207.10/29.46 % (3515515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.10/29.46 % (3515515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.10/29.46 % (3515515)CaDiCaL version: 2.1.3 % 207.10/29.46 % (3515515)Termination reason: Inappropriate % 207.10/29.46 % (3515515)Time elapsed: 0.001 s % 207.10/29.46 % (3515515)Peak memory usage: 10 MB % 207.10/29.46 % (3515515)Instructions burned: 1 (million) % 207.10/29.46 % (3515515)------------------------------ % 207.10/29.46 % (3515515)------------------------------ % 207.10/29.46 % (3515517)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1267435666:i=160505_2805 on theBenchmark for (2805ds/160505Mi) % 207.10/29.46 % (3515517)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.10/29.46 % (3515517)Terminated due to inappropriate strategy. % 207.10/29.46 % (3515517)------------------------------ % 207.10/29.46 % (3515517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.10/29.46 % (3515517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.10/29.46 % (3515517)CaDiCaL version: 2.1.3 % 207.10/29.46 % (3515517)Termination reason: Inappropriate % 207.10/29.46 % (3515517)Time elapsed: 0.001 s % 207.10/29.46 % (3515517)Peak memory usage: 10 MB % 207.10/29.46 % (3515517)Instructions burned: 1 (million) % 207.10/29.46 % (3515517)------------------------------ % 207.10/29.46 % (3515517)------------------------------ % 207.10/29.46 % (3515519)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=855032572:fmbsr=1.3:i=225729_2805 on theBenchmark for (2805ds/225729Mi) % 207.10/29.46 % (3515519)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.10/29.46 % (3515519)Terminated due to inappropriate strategy. % 207.10/29.46 % (3515519)------------------------------ % 207.10/29.46 % (3515519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.10/29.46 % (3515519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.10/29.46 % (3515519)CaDiCaL version: 2.1.3 % 207.10/29.46 % (3515519)Termination reason: Inappropriate % 207.10/29.46 % (3515519)Time elapsed: 0.001 s % 207.10/29.46 % (3515519)Peak memory usage: 10 MB % 207.10/29.46 % (3515519)Instructions burned: 1 (million) % 207.10/29.46 % (3515519)------------------------------ % 207.10/29.46 % (3515519)------------------------------ % 207.10/29.46 % (3515521)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3303088451:fmbsr=2:i=185024:ins=7_2804 on theBenchmark for (2804ds/185024Mi) % 207.10/29.46 % (3515521)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.10/29.46 % (3515521)Terminated due to inappropriate strategy. % 207.10/29.46 % (3515521)------------------------------ % 207.10/29.46 % (3515521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.10/29.46 % (3515521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.10/29.46 % (3515521)CaDiCaL version: 2.1.3 % 207.10/29.46 % (3515521)Termination reason: Inappropriate % 207.10/29.46 % (3515521)Time elapsed: 0.001 s % 207.10/29.46 % (3515521)Peak memory usage: 10 MB % 207.10/29.46 % (3515521)Instructions burned: 1 (million) % 207.10/29.46 % (3515521)------------------------------ % 207.10/29.46 % (3515521)------------------------------ % 207.10/29.46 % (3515523)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4248804500:rtra=on_2804 on theBenchmark for (2804ds/0Mi) % 207.10/29.46 % (3515523)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.10/29.46 % (3515523)Terminated due to inappropriate strategy. % 207.10/29.46 % (3515523)------------------------------ % 207.10/29.46 % (3515523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.10/29.46 % (3515523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.10/29.46 % (3515523)CaDiCaL version: 2.1.3 % 207.10/29.46 % (3515523)Termination reason: Inappropriate % 207.10/29.46 % (3515523)Time elapsed: 0.001 s % 207.10/29.46 % (3515523)Peak memory usage: 10 MB % 207.10/29.46 % (3515523)Instructions burned: 1 (million) % 207.10/29.46 % (3515523)------------------------------ % 207.10/29.46 % (3515523)------------------------------ % 207.10/29.46 % (3515525)% WARNING: option uhcvi not known. % 207.10/29.46 % (3515525)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=938604591:i=271062:add=off:rtra=on:rawr=on_2804 on theBenchmark for (2804ds/271062Mi) % 224.02/31.94 % (3515202)Instruction limit reached! % 224.02/31.94 % (3515202)------------------------------ % 224.02/31.94 % (3515202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.02/31.94 % (3515202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.02/31.94 % (3515202)CaDiCaL version: 2.1.3 % 224.02/31.94 % (3515202)Termination reason: Instruction limit % 224.02/31.94 % (3515202)Termination phase: Saturation % 224.02/31.94 % (3515202)Time elapsed: 7.092 s % 224.02/31.94 % (3515202)Peak memory usage: 202 MB % 224.02/31.94 % (3515202)Instructions burned: 15853 (million) % 224.02/31.94 % (3515527)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=230398552:i=176048:add=on:rtra=on:rawr=on_2796 on theBenchmark for (2796ds/176048Mi) % 224.02/31.94 % (3515505)Instruction limit reached! % 224.02/31.94 % (3515505)------------------------------ % 224.02/31.94 % (3515505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.02/31.94 % (3515505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.02/31.94 % (3515505)CaDiCaL version: 2.1.3 % 224.02/31.94 % (3515505)Termination reason: Instruction limit % 224.02/31.94 % (3515505)Termination phase: Saturation % 224.02/31.94 % (3515505)Time elapsed: 9.472 s % 224.02/31.94 % (3515505)Peak memory usage: 79 MB % 224.02/31.94 % (3515505)Instructions burned: 17628 (million) % 224.02/31.94 % (3515529)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3839626262:i=206:fgj=on:rtra=on_2735 on theBenchmark for (2735ds/206Mi) % 224.02/31.94 % (3515529)Instruction limit reached! % 224.02/31.94 % (3515529)------------------------------ % 224.02/31.94 % (3515529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.02/31.94 % (3515529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.02/31.94 % (3515529)CaDiCaL version: 2.1.3 % 224.02/31.94 % (3515529)Termination reason: Instruction limit % 224.02/31.94 % (3515529)Termination phase: Saturation % 224.02/31.94 % (3515529)Time elapsed: 0.127 s % 224.02/31.94 % (3515529)Peak memory usage: 13 MB % 224.02/31.94 % (3515529)Instructions burned: 206 (million) % 224.02/31.94 % (3515531)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2178057043:i=232:rtra=on_2733 on theBenchmark for (2733ds/232Mi) % 224.02/31.94 % (3515531)Instruction limit reached! % 224.02/31.94 % (3515531)------------------------------ % 224.02/31.94 % (3515531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.02/31.94 % (3515531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.02/31.94 % (3515531)CaDiCaL version: 2.1.3 % 224.02/31.94 % (3515531)Termination reason: Instruction limit % 224.02/31.94 % (3515531)Termination phase: Saturation % 224.02/31.94 % (3515531)Time elapsed: 0.150 s % 224.02/31.94 % (3515531)Peak memory usage: 13 MB % 224.02/31.94 % (3515531)Instructions burned: 233 (million) % 224.02/31.94 % (3515533)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2184528565:i=262:rtra=on_2731 on theBenchmark for (2731ds/262Mi) % 224.02/31.94 % (3515533)Instruction limit reached! % 224.02/31.94 % (3515533)------------------------------ % 224.02/31.94 % (3515533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.02/31.94 % (3515533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.02/31.94 % (3515533)CaDiCaL version: 2.1.3 % 224.02/31.94 % (3515533)Termination reason: Instruction limit % 224.02/31.94 % (3515533)Termination phase: Saturation % 224.02/31.94 % (3515533)Time elapsed: 0.168 s % 224.02/31.94 % (3515533)Peak memory usage: 14 MB % 224.02/31.94 % (3515533)Instructions burned: 262 (million) % 224.02/31.94 % (3515535)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2667714817:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2729 on theBenchmark for (2729ds/318Mi) % 224.02/31.94 % (3515535)Instruction limit reached! % 224.02/31.94 % (3515535)------------------------------ % 224.02/31.94 % (3515535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.02/31.94 % (3515535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.02/31.94 % (3515535)CaDiCaL version: 2.1.3 % 224.02/31.94 % (3515535)Termination reason: Instruction limit % 224.02/31.94 % (3515535)Termination phase: Saturation % 224.02/31.94 % (3515535)Time elapsed: 0.224 s % 224.02/31.94 % (3515535)Peak memory usage: 15 MB % 224.02/31.94 % (3515535)Instructions burned: 318 (million) % 224.02/31.94 % (3515537)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3623778389:i=1428:nm=2:rtra=on_2727 on theBenchmark for (2727ds/1428Mi) % 238.32/33.87 % (3515537)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 238.32/33.87 % (3515537)Terminated due to inappropriate strategy. % 238.32/33.87 % (3515537)------------------------------ % 238.32/33.87 % (3515537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.32/33.87 % (3515537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.32/33.87 % (3515537)CaDiCaL version: 2.1.3 % 238.32/33.87 % (3515537)Termination reason: Inappropriate % 238.32/33.87 % (3515537)Time elapsed: 0.001 s % 238.32/33.87 % (3515537)Peak memory usage: 10 MB % 238.32/33.87 % (3515537)Instructions burned: 1 (million) % 238.32/33.87 % (3515537)------------------------------ % 238.32/33.87 % (3515537)------------------------------ % 238.32/33.87 % (3515539)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2591142449:i=262:bd=preordered:rtra=on:fsd=on_2727 on theBenchmark for (2727ds/262Mi) % 238.32/33.87 % (3515539)Instruction limit reached! % 238.32/33.87 % (3515539)------------------------------ % 238.32/33.87 % (3515539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.32/33.88 % (3515539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.32/33.88 % (3515539)CaDiCaL version: 2.1.3 % 238.32/33.88 % (3515539)Termination reason: Instruction limit % 238.32/33.88 % (3515539)Termination phase: Saturation % 238.32/33.88 % (3515539)Time elapsed: 0.173 s % 238.32/33.88 % (3515539)Peak memory usage: 14 MB % 238.32/33.88 % (3515539)Instructions burned: 263 (million) % 238.32/33.88 % (3515541)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=1363904360:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2725 on theBenchmark for (2725ds/1368Mi) % 238.32/33.88 % (3515541)Instruction limit reached! % 238.32/33.88 % (3515541)------------------------------ % 238.32/33.88 % (3515541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.32/33.88 % (3515541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.32/33.88 % (3515541)CaDiCaL version: 2.1.3 % 238.32/33.88 % (3515541)Termination reason: Instruction limit % 238.32/33.88 % (3515541)Termination phase: Saturation % 238.32/33.88 % (3515541)Time elapsed: 0.765 s % 238.32/33.88 % (3515541)Peak memory usage: 22 MB % 238.32/33.88 % (3515541)Instructions burned: 1369 (million) % 238.32/33.88 % (3515675)ott-21_1_sil=16000:si=on:fs=off:random_seed=4124811775:i=360:av=off:fsr=off:rtra=on_2717 on theBenchmark for (2717ds/360Mi) % 238.32/33.88 % (3515675)Instruction limit reached! % 238.32/33.88 % (3515675)------------------------------ % 238.32/33.88 % (3515675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.32/33.88 % (3515675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.32/33.88 % (3515675)CaDiCaL version: 2.1.3 % 238.32/33.88 % (3515675)Termination reason: Instruction limit % 238.32/33.88 % (3515675)Termination phase: Saturation % 238.32/33.88 % (3515675)Time elapsed: 0.160 s % 238.32/33.88 % (3515675)Peak memory usage: 13 MB % 238.32/33.88 % (3515675)Instructions burned: 360 (million) % 238.32/33.88 % (3515741)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3129015907:i=954:bd=all:rtra=on_2715 on theBenchmark for (2715ds/954Mi) % 238.32/33.88 % (3515741)Instruction limit reached! % 238.32/33.88 % (3515741)------------------------------ % 238.32/33.88 % (3515741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.32/33.88 % (3515741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.32/33.88 % (3515741)CaDiCaL version: 2.1.3 % 238.32/33.88 % (3515741)Termination reason: Instruction limit % 238.32/33.88 % (3515741)Termination phase: Saturation % 238.32/33.88 % (3515741)Time elapsed: 0.772 s % 238.32/33.88 % (3515741)Peak memory usage: 16 MB % 238.32/33.88 % (3515741)Instructions burned: 954 (million) % 238.32/33.88 % (3515838)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2030745736:fmbsr=1.3:i=1730:ins=25:rtra=on_2707 on theBenchmark for (2707ds/1730Mi) % 238.32/33.88 % (3515838)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 238.32/33.88 % (3515838)Terminated due to inappropriate strategy. % 238.32/33.88 % (3515838)------------------------------ % 238.32/33.88 % (3515838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.32/33.88 % (3515838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.32/33.88 % (3515838)CaDiCaL version: 2.1.3 % 238.32/33.88 % (3515838)Termination reason: Inappropriate % 238.32/33.88 % (3515838)Time elapsed: 0.001 s % 270.10/41.75 % (3515838)Peak memory usage: 10 MB % 270.10/41.75 % (3515838)Instructions burned: 1 (million) % 270.10/41.75 % (3515838)------------------------------ % 270.10/41.75 % (3515838)------------------------------ % 270.10/41.75 % (3515840)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2979944820:i=2358:rtra=on_2707 on theBenchmark for (2707ds/2358Mi) % 270.10/41.75 % (3515511)Instruction limit reached! % 270.10/41.75 % (3515511)------------------------------ % 270.10/41.75 % (3515511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.10/41.75 % (3515511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.10/41.75 % (3515511)CaDiCaL version: 2.1.3 % 270.10/41.75 % (3515511)Termination reason: Instruction limit % 270.10/41.75 % (3515511)Termination phase: Saturation % 270.10/41.75 % (3515511)Time elapsed: 11.474 s % 270.10/41.75 % (3515511)Peak memory usage: 24 MB % 270.10/41.75 % (3515511)Instructions burned: 28121 (million) % 270.10/41.75 % (3515840)Instruction limit reached! % 270.10/41.75 % (3515840)------------------------------ % 270.10/41.75 % (3515840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.10/41.75 % (3515840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.10/41.75 % (3515840)CaDiCaL version: 2.1.3 % 270.10/41.75 % (3515840)Termination reason: Instruction limit % 270.10/41.75 % (3515840)Termination phase: Saturation % 270.10/41.75 % (3515840)Time elapsed: 1.570 s % 270.10/41.75 % (3515840)Peak memory usage: 25 MB % 270.10/41.75 % (3515840)Instructions burned: 2358 (million) % 270.10/41.75 % (3515994)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2378291854:i=1778:ins=1:rtra=on_2691 on theBenchmark for (2691ds/1778Mi) % 270.10/41.75 % (3515994)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 270.10/41.75 % (3515994)Terminated due to inappropriate strategy. % 270.10/41.75 % (3515994)------------------------------ % 270.10/41.75 % (3515994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.10/41.75 % (3515994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.10/41.75 % (3515994)CaDiCaL version: 2.1.3 % 270.10/41.75 % (3515994)Termination reason: Inappropriate % 270.10/41.75 % (3515994)Time elapsed: 0.001 s % 270.10/41.75 % (3515994)Peak memory usage: 10 MB % 270.10/41.75 % (3515994)Instructions burned: 1 (million) % 270.10/41.75 % (3515995)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=1248119685:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2691 on theBenchmark for (2691ds/1384Mi) % 270.10/41.75 % (3515994)------------------------------ % 270.10/41.75 % (3515994)------------------------------ % 270.10/41.75 % (3515998)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1114987000:i=1758:kws=inv_precedence:fsr=off:rtra=on_2691 on theBenchmark for (2691ds/1758Mi) % 270.10/41.75 % (3515995)Instruction limit reached! % 270.10/41.75 % (3515995)------------------------------ % 270.10/41.75 % (3515995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.10/41.75 % (3515995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.10/41.75 % (3515995)CaDiCaL version: 2.1.3 % 270.10/41.75 % (3515995)Termination reason: Instruction limit % 270.10/41.75 % (3515995)Termination phase: Saturation % 270.10/41.75 % (3515995)Time elapsed: 0.808 s % 270.10/41.75 % (3515995)Peak memory usage: 26 MB % 270.10/41.75 % (3515995)Instructions burned: 1384 (million) % 270.10/41.75 % (3516000)fmb+10_1_sil=64000:si=on:random_seed=2629795311:i=44122:nm=2:rtra=on:gsp=on_2683 on theBenchmark for (2683ds/44122Mi) % 270.10/41.75 % (3516000)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 270.10/41.75 % (3516000)Terminated due to inappropriate strategy. % 270.10/41.75 % (3516000)------------------------------ % 270.10/41.75 % (3516000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.10/41.75 % (3516000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.10/41.75 % (3516000)CaDiCaL version: 2.1.3 % 270.10/41.75 % (3516000)Termination reason: Inappropriate % 270.10/41.75 % (3516000)Time elapsed: 0.001 s % 270.10/41.75 % (3516000)Peak memory usage: 10 MB % 270.10/41.75 % (3516000)Instructions burned: 1 (million) % 270.10/41.75 % (3516000)------------------------------ % 270.10/41.75 % (3516000)------------------------------ % 270.10/41.75 % (3516002)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4031047871:i=19030:nm=5:rtra=on_2683 on theBenchmark for (2683ds/19030Mi) % 300.11/42.63 % (3516002)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.11/42.63 % (3516002)Terminated due to inappropriate strategy. % 300.11/42.63 % (3516002)------------------------------ % 300.11/42.63 % (3516002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.63 % (3516002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.63 % (3516002)CaDiCaL version: 2.1.3 % 300.11/42.63 % (3516002)Termination reason: Inappropriate % 300.11/42.63 % (3516002)Time elapsed: 0.001 s % 300.11/42.63 % (3516002)Peak memory usage: 10 MB % 300.11/42.63 % (3516002)Instructions burned: 1 (million) % 300.11/42.63 % (3516002)------------------------------ % 300.11/42.63 % (3516002)------------------------------ % 300.11/42.63 % (3516004)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1291841562:fmbsr=1.7:i=1840:rtra=on_2682 on theBenchmark for (2682ds/1840Mi) % 300.11/42.63 % (3516004)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.11/42.63 % (3516004)Terminated due to inappropriate strategy. % 300.11/42.63 % (3516004)------------------------------ % 300.11/42.63 % (3516004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.63 % (3516004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.63 % (3516004)CaDiCaL version: 2.1.3 % 300.11/42.63 % (3516004)Termination reason: Inappropriate % 300.11/42.63 % (3516004)Time elapsed: 0.001 s % 300.11/42.63 % (3516004)Peak memory usage: 10 MB % 300.11/42.63 % (3516004)Instructions burned: 1 (million) % 300.11/42.63 % (3516004)------------------------------ % 300.11/42.63 % (3516004)------------------------------ % 300.11/42.63 % (3516006)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2158453336:i=10262:rtra=on_2682 on theBenchmark for (2682ds/10262Mi) % 300.11/42.63 % (3515998)Instruction limit reached! % 300.11/42.63 % (3515998)------------------------------ % 300.11/42.63 % (3515998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.63 % (3515998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.63 % (3515998)CaDiCaL version: 2.1.3 % 300.11/42.63 % (3515998)Termination reason: Instruction limit % 300.11/42.63 % (3515998)Termination phase: Saturation % 300.11/42.63 % (3515998)Time elapsed: 1.011 s % 300.11/42.63 % (3515998)Peak memory usage: 26 MB % 300.11/42.63 % (3515998)Instructions burned: 1759 (million) % 300.11/42.63 % (3516008)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1969874388:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2680 on theBenchmark for (2680ds/2944Mi) % 300.11/42.63 % (3516008)Instruction limit reached! % 300.11/42.63 % (3516008)------------------------------ % 300.11/42.63 % (3516008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.63 % (3516008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.63 % (3516008)CaDiCaL version: 2.1.3 % 300.11/42.63 % (3516008)Termination reason: Instruction limit % 300.11/42.63 % (3516008)Termination phase: Saturation % 300.11/42.63 % (3516008)Time elapsed: 1.691 s % 300.11/42.63 % (3516008)Peak memory usage: 37 MB % 300.11/42.63 % (3516008)Instructions burned: 2945 (million) % 300.11/42.63 % (3516011)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=516040088:i=12648:rtra=on_2663 on theBenchmark for (2663ds/12648Mi) % 300.11/42.63 % (3516011)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.11/42.63 % (3516011)Terminated due to inappropriate strategy. % 300.11/42.63 % (3516011)------------------------------ % 300.11/42.63 % (3516011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.63 % (3516011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.63 % (3516011)CaDiCaL version: 2.1.3 % 300.11/42.63 % (3516011)Termination reason: Inappropriate % 300.11/42.63 % (3516011)Time elapsed: 0.001 s % 300.11/42.63 % (3516011)Peak memory usage: 10 MB % 300.11/42.63 % (3516011)Instructions burned: 1 (million) % 300.11/42.63 % (3516011)------------------------------ % 300.11/42.63 % (3516011)------------------------------ % 300.11/42.63 % (3516013)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3165428351:fmbsr=2.30978:i=4348:rtra=on_2663 on theBenchmark for (2663ds/4348Mi) % 300.11/42.63 % (3516013)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.11/42.63 % (3516013)Terminated due to inappropriate strategy. % 300.11/42.63 % (3516013)------------------------------ % 300.11/42.63 % (3516013)Version: % 300.11/42.63 Terminated % 300.11/42.63 % Vampire exiting % 300.11/42.63 Terminated %------------------------------------------------------------------------------