%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW604_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n026.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:31 PM UTC 2026 % Result : Timeout 300.43s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW604_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n026.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 14:23:42 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.65/0.88 % (3880804)Will run a generic schedule for satisfiability detection. % 3.65/0.88 % (3880814)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1681227318:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.65/0.88 % (3880810)% WARNING: option uhcvi not known. % 3.65/0.88 % (3880812)dis+10_1_sil=32000:sp=arity:random_seed=3674723316:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.65/0.88 % (3880809)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2896258199_2999 on theBenchmark for (2999ds/0Mi) % 3.65/0.88 % (3880810)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1140021871:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.65/0.88 % (3880811)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1231803266:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.65/0.88 % (3880813)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2815305474:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.65/0.88 % (3880815)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2783675286:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.65/0.88 % (3880809)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.65/0.88 % (3880809)Terminated due to inappropriate strategy. % 3.65/0.88 % (3880809)------------------------------ % 3.65/0.88 % (3880809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.88 % (3880809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.88 % (3880809)CaDiCaL version: 2.1.3 % 3.65/0.88 % (3880809)Termination reason: Inappropriate % 3.65/0.88 % (3880809)Time elapsed: 0.005 s % 3.65/0.88 % (3880809)Peak memory usage: 11 MB % 3.65/0.88 % (3880809)Instructions burned: 9 (million) % 3.65/0.88 % (3880809)------------------------------ % 3.65/0.88 % (3880809)------------------------------ % 3.65/0.88 % (3880823)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2654649397:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.65/0.88 % (3880823)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.65/0.88 % (3880823)Terminated due to inappropriate strategy. % 3.65/0.88 % (3880823)------------------------------ % 3.65/0.88 % (3880823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.88 % (3880823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.88 % (3880823)CaDiCaL version: 2.1.3 % 3.65/0.88 % (3880823)Termination reason: Inappropriate % 3.65/0.88 % (3880823)Time elapsed: 0.004 s % 3.65/0.88 % (3880823)Peak memory usage: 10 MB % 3.65/0.88 % (3880823)Instructions burned: 8 (million) % 3.65/0.88 % (3880823)------------------------------ % 3.65/0.88 % (3880823)------------------------------ % 3.65/0.88 % (3880814)Instruction limit reached! % 3.65/0.88 % (3880814)------------------------------ % 3.65/0.88 % (3880814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.88 % (3880814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.88 % (3880814)CaDiCaL version: 2.1.3 % 3.65/0.88 % (3880814)Termination reason: Instruction limit % 3.65/0.88 % (3880814)Termination phase: Saturation % 3.65/0.88 % (3880814)Time elapsed: 0.048 s % 3.65/0.88 % (3880814)Peak memory usage: 14 MB % 3.65/0.88 % (3880814)Instructions burned: 133 (million) % 3.65/0.88 % (3880825)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=373432655:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.65/0.88 % (3880826)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=3990341044:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.65/0.88 % (3880812)Instruction limit reached! % 3.65/0.88 % (3880812)------------------------------ % 3.65/0.88 % (3880812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/0.88 % (3880812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/0.88 % (3880812)CaDiCaL version: 2.1.3 % 3.65/0.88 % (3880812)Termination reason: Instruction limit % 3.65/0.88 % (3880812)Termination phase: Saturation % 3.65/0.88 % (3880812)Time elapsed: 0.067 s % 3.65/0.88 % (3880812)Peak memory usage: 13 MB % 3.65/0.88 % (3880812)Instructions burned: 104 (million) % 3.65/0.88 % (3880813)Instruction limit reached! % 3.65/0.88 % (3880813)------------------------------ % 3.65/0.88 % (3880813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.76/1.23 % (3880813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.76/1.23 % (3880813)CaDiCaL version: 2.1.3 % 6.76/1.23 % (3880813)Termination reason: Instruction limit % 6.76/1.23 % (3880813)Termination phase: Saturation % 6.76/1.23 % (3880813)Time elapsed: 0.076 s % 6.76/1.23 % (3880813)Peak memory usage: 13 MB % 6.76/1.23 % (3880813)Instructions burned: 117 (million) % 6.76/1.23 % (3880829)ott-21_1_sil=16000:fs=off:random_seed=89995618:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.76/1.23 % (3880830)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3655507392:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.76/1.23 % (3880815)Instruction limit reached! % 6.76/1.23 % (3880815)------------------------------ % 6.76/1.23 % (3880815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.76/1.23 % (3880815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.76/1.23 % (3880815)CaDiCaL version: 2.1.3 % 6.76/1.23 % (3880815)Termination reason: Instruction limit % 6.76/1.23 % (3880815)Termination phase: Saturation % 6.76/1.23 % (3880815)Time elapsed: 0.105 s % 6.76/1.23 % (3880815)Peak memory usage: 13 MB % 6.76/1.23 % (3880815)Instructions burned: 160 (million) % 6.76/1.23 % (3880833)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1023851235:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.76/1.23 % (3880833)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.76/1.23 % (3880833)Terminated due to inappropriate strategy. % 6.76/1.23 % (3880833)------------------------------ % 6.76/1.23 % (3880833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.76/1.23 % (3880833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.76/1.23 % (3880833)CaDiCaL version: 2.1.3 % 6.76/1.23 % (3880833)Termination reason: Inappropriate % 6.76/1.23 % (3880833)Time elapsed: 0.004 s % 6.76/1.23 % (3880833)Peak memory usage: 11 MB % 6.76/1.23 % (3880833)Instructions burned: 8 (million) % 6.76/1.23 % (3880833)------------------------------ % 6.76/1.23 % (3880833)------------------------------ % 6.76/1.23 % (3880825)Instruction limit reached! % 6.76/1.23 % (3880825)------------------------------ % 6.76/1.23 % (3880825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.76/1.23 % (3880825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.76/1.23 % (3880825)CaDiCaL version: 2.1.3 % 6.76/1.23 % (3880825)Termination reason: Instruction limit % 6.76/1.23 % (3880825)Termination phase: Saturation % 6.76/1.23 % (3880825)Time elapsed: 0.090 s % 6.76/1.23 % (3880825)Peak memory usage: 14 MB % 6.76/1.23 % (3880825)Instructions burned: 132 (million) % 6.76/1.23 % (3880835)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=951864538:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.76/1.23 % (3880836)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=485663992:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.76/1.23 % (3880836)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.76/1.23 % (3880836)Terminated due to inappropriate strategy. % 6.76/1.23 % (3880836)------------------------------ % 6.76/1.23 % (3880836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.76/1.23 % (3880836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.76/1.23 % (3880836)CaDiCaL version: 2.1.3 % 6.76/1.23 % (3880836)Termination reason: Inappropriate % 6.76/1.23 % (3880836)Time elapsed: 0.004 s % 6.76/1.23 % (3880836)Peak memory usage: 10 MB % 6.76/1.23 % (3880836)Instructions burned: 8 (million) % 6.76/1.23 % (3880836)------------------------------ % 6.76/1.23 % (3880836)------------------------------ % 6.76/1.23 % (3880829)Instruction limit reached! % 6.76/1.23 % (3880829)------------------------------ % 6.76/1.23 % (3880829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.76/1.23 % (3880829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.76/1.23 % (3880829)CaDiCaL version: 2.1.3 % 6.76/1.23 % (3880829)Termination reason: Instruction limit % 6.76/1.23 % (3880829)Termination phase: Saturation % 6.76/1.23 % (3880829)Time elapsed: 0.096 s % 6.76/1.23 % (3880829)Peak memory usage: 13 MB % 6.76/1.23 % (3880829)Instructions burned: 180 (million) % 6.76/1.23 % (3880839)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=1904635654:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 20.95/3.29 % (3880840)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1064495942:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.95/3.29 % (3880826)Instruction limit reached! % 20.95/3.29 % (3880826)------------------------------ % 20.95/3.29 % (3880826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.95/3.29 % (3880826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.29 % (3880826)CaDiCaL version: 2.1.3 % 20.95/3.29 % (3880826)Termination reason: Instruction limit % 20.95/3.29 % (3880826)Termination phase: Saturation % 20.95/3.29 % (3880826)Time elapsed: 0.229 s % 20.95/3.29 % (3880826)Peak memory usage: 18 MB % 20.95/3.29 % (3880826)Instructions burned: 684 (million) % 20.95/3.29 % (3880843)fmb+10_1_sil=64000:random_seed=3250659217:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 20.95/3.29 % (3880843)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.95/3.29 % (3880843)Terminated due to inappropriate strategy. % 20.95/3.29 % (3880843)------------------------------ % 20.95/3.29 % (3880843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.95/3.29 % (3880843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.29 % (3880843)CaDiCaL version: 2.1.3 % 20.95/3.29 % (3880843)Termination reason: Inappropriate % 20.95/3.29 % (3880843)Time elapsed: 0.002 s % 20.95/3.29 % (3880843)Peak memory usage: 10 MB % 20.95/3.29 % (3880843)Instructions burned: 8 (million) % 20.95/3.29 % (3880843)------------------------------ % 20.95/3.29 % (3880843)------------------------------ % 20.95/3.29 % (3880845)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2879060335:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 20.95/3.29 % (3880845)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.95/3.29 % (3880845)Terminated due to inappropriate strategy. % 20.95/3.29 % (3880845)------------------------------ % 20.95/3.29 % (3880845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.95/3.29 % (3880845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.29 % (3880845)CaDiCaL version: 2.1.3 % 20.95/3.29 % (3880845)Termination reason: Inappropriate % 20.95/3.29 % (3880845)Time elapsed: 0.002 s % 20.95/3.29 % (3880845)Peak memory usage: 10 MB % 20.95/3.29 % (3880845)Instructions burned: 8 (million) % 20.95/3.29 % (3880845)------------------------------ % 20.95/3.29 % (3880845)------------------------------ % 20.95/3.29 % (3880847)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1693719874:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 20.95/3.29 % (3880847)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.95/3.29 % (3880847)Terminated due to inappropriate strategy. % 20.95/3.29 % (3880847)------------------------------ % 20.95/3.29 % (3880847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.95/3.29 % (3880847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.29 % (3880847)CaDiCaL version: 2.1.3 % 20.95/3.29 % (3880847)Termination reason: Inappropriate % 20.95/3.29 % (3880847)Time elapsed: 0.002 s % 20.95/3.29 % (3880847)Peak memory usage: 10 MB % 20.95/3.29 % (3880847)Instructions burned: 8 (million) % 20.95/3.29 % (3880847)------------------------------ % 20.95/3.29 % (3880847)------------------------------ % 20.95/3.29 % (3880849)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=593285131:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 20.95/3.29 % (3880830)Instruction limit reached! % 20.95/3.29 % (3880830)------------------------------ % 20.95/3.29 % (3880830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.95/3.29 % (3880830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.29 % (3880830)CaDiCaL version: 2.1.3 % 20.95/3.29 % (3880830)Termination reason: Instruction limit % 20.95/3.29 % (3880830)Termination phase: Saturation % 20.95/3.29 % (3880830)Time elapsed: 0.324 s % 20.95/3.29 % (3880830)Peak memory usage: 15 MB % 20.95/3.29 % (3880830)Instructions burned: 478 (million) % 20.95/3.29 % (3880851)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1550110841:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 20.95/3.29 % (3880839)Instruction limit reached! % 20.95/3.29 % (3880839)------------------------------ % 26.86/4.08 % (3880839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.86/4.08 % (3880839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.86/4.08 % (3880839)CaDiCaL version: 2.1.3 % 26.86/4.08 % (3880839)Termination reason: Instruction limit % 26.86/4.08 % (3880839)Termination phase: Saturation % 26.86/4.08 % (3880839)Time elapsed: 0.414 s % 26.86/4.08 % (3880839)Peak memory usage: 19 MB % 26.86/4.08 % (3880839)Instructions burned: 692 (million) % 26.86/4.08 % (3880854)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3047967157:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 26.86/4.08 % (3880854)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.86/4.08 % (3880854)Terminated due to inappropriate strategy. % 26.86/4.08 % (3880854)------------------------------ % 26.86/4.08 % (3880854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.86/4.08 % (3880854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.86/4.08 % (3880854)CaDiCaL version: 2.1.3 % 26.86/4.08 % (3880854)Termination reason: Inappropriate % 26.86/4.08 % (3880854)Time elapsed: 0.005 s % 26.86/4.08 % (3880854)Peak memory usage: 11 MB % 26.86/4.08 % (3880854)Instructions burned: 9 (million) % 26.86/4.08 % (3880854)------------------------------ % 26.86/4.08 % (3880854)------------------------------ % 26.86/4.08 % (3880856)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1062733243:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 26.86/4.08 % (3880856)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.86/4.08 % (3880856)Terminated due to inappropriate strategy. % 26.86/4.08 % (3880856)------------------------------ % 26.86/4.08 % (3880856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.86/4.08 % (3880856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.86/4.08 % (3880856)CaDiCaL version: 2.1.3 % 26.86/4.08 % (3880856)Termination reason: Inappropriate % 26.86/4.08 % (3880856)Time elapsed: 0.004 s % 26.86/4.08 % (3880856)Peak memory usage: 10 MB % 26.86/4.08 % (3880856)Instructions burned: 8 (million) % 26.86/4.08 % (3880856)------------------------------ % 26.86/4.08 % (3880856)------------------------------ % 26.86/4.08 % (3880858)ott-2_1_sil=16000:newcnf=on:random_seed=2666605053:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 26.86/4.08 % (3880840)Instruction limit reached! % 26.86/4.08 % (3880840)------------------------------ % 26.86/4.08 % (3880840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.86/4.08 % (3880840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.86/4.08 % (3880840)CaDiCaL version: 2.1.3 % 26.86/4.08 % (3880840)Termination reason: Instruction limit % 26.86/4.08 % (3880840)Termination phase: Saturation % 26.86/4.08 % (3880840)Time elapsed: 0.512 s % 26.86/4.08 % (3880840)Peak memory usage: 18 MB % 26.86/4.08 % (3880840)Instructions burned: 879 (million) % 26.86/4.08 % (3880860)ott+10_1_sil=32000:tgt=ground:random_seed=3699930293:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 26.86/4.08 % (3880835)Instruction limit reached! % 26.86/4.08 % (3880835)------------------------------ % 26.86/4.08 % (3880835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.86/4.08 % (3880835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.86/4.08 % (3880835)CaDiCaL version: 2.1.3 % 26.86/4.08 % (3880835)Termination reason: Instruction limit % 26.86/4.08 % (3880835)Termination phase: Saturation % 26.86/4.08 % (3880835)Time elapsed: 0.771 s % 26.86/4.08 % (3880835)Peak memory usage: 23 MB % 26.86/4.08 % (3880835)Instructions burned: 1179 (million) % 26.86/4.08 % (3880862)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3687244311:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 26.86/4.08 % (3880862)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.86/4.08 % (3880862)Terminated due to inappropriate strategy. % 26.86/4.08 % (3880862)------------------------------ % 26.86/4.08 % (3880862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.86/4.08 % (3880862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.86/4.08 % (3880862)CaDiCaL version: 2.1.3 % 26.86/4.08 % (3880862)Termination reason: Inappropriate % 26.86/4.08 % (3880862)Time elapsed: 0.005 s % 26.86/4.08 % (3880862)Peak memory usage: 11 MB % 26.86/4.08 % (3880862)Instructions burned: 9 (million) % 94.79/13.62 % (3880862)------------------------------ % 94.79/13.62 % (3880862)------------------------------ % 94.79/13.62 % (3880864)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1564757233:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 94.79/13.62 % (3880858)Instruction limit reached! % 94.79/13.62 % (3880858)------------------------------ % 94.79/13.62 % (3880858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.79/13.62 % (3880858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.79/13.62 % (3880858)CaDiCaL version: 2.1.3 % 94.79/13.62 % (3880858)Termination reason: Instruction limit % 94.79/13.62 % (3880858)Termination phase: Saturation % 94.79/13.62 % (3880858)Time elapsed: 0.497 s % 94.79/13.62 % (3880858)Peak memory usage: 16 MB % 94.79/13.62 % (3880858)Instructions burned: 870 (million) % 94.79/13.62 % (3880866)dis+21_1_sil=32000:sas=cadical:random_seed=3474202317:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 94.79/13.62 % (3880851)Instruction limit reached! % 94.79/13.62 % (3880851)------------------------------ % 94.79/13.62 % (3880851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.79/13.62 % (3880851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.79/13.62 % (3880851)CaDiCaL version: 2.1.3 % 94.79/13.62 % (3880851)Termination reason: Instruction limit % 94.79/13.62 % (3880851)Termination phase: Saturation % 94.79/13.62 % (3880851)Time elapsed: 0.858 s % 94.79/13.62 % (3880851)Peak memory usage: 29 MB % 94.79/13.62 % (3880851)Instructions burned: 1472 (million) % 94.79/13.62 % (3880868)ott+11_1_sil=16000:gs=on:random_seed=3550275022:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 94.79/13.62 % (3880849)Instruction limit reached! % 94.79/13.62 % (3880849)------------------------------ % 94.79/13.62 % (3880849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.79/13.62 % (3880849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.79/13.62 % (3880849)CaDiCaL version: 2.1.3 % 94.79/13.62 % (3880849)Termination reason: Instruction limit % 94.79/13.62 % (3880849)Termination phase: Saturation % 94.79/13.62 % (3880849)Time elapsed: 1.549 s % 94.79/13.62 % (3880849)Peak memory usage: 44 MB % 94.79/13.62 % (3880849)Instructions burned: 5133 (million) % 94.79/13.62 % (3880870)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=973945880:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 94.79/13.62 % (3880870)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 94.79/13.62 % (3880870)Terminated due to inappropriate strategy. % 94.79/13.62 % (3880870)------------------------------ % 94.79/13.62 % (3880870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.79/13.62 % (3880870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.79/13.62 % (3880870)CaDiCaL version: 2.1.3 % 94.79/13.62 % (3880870)Termination reason: Inappropriate % 94.79/13.62 % (3880870)Time elapsed: 0.002 s % 94.79/13.62 % (3880870)Peak memory usage: 10 MB % 94.79/13.62 % (3880870)Instructions burned: 8 (million) % 94.79/13.62 % (3880870)------------------------------ % 94.79/13.62 % (3880870)------------------------------ % 94.79/13.62 % (3880872)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=83146524:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 94.79/13.62 % (3880868)Instruction limit reached! % 94.79/13.62 % (3880868)------------------------------ % 94.79/13.62 % (3880868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.79/13.62 % (3880868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.79/13.62 % (3880868)CaDiCaL version: 2.1.3 % 94.79/13.62 % (3880868)Termination reason: Instruction limit % 94.79/13.62 % (3880868)Termination phase: Saturation % 94.79/13.62 % (3880868)Time elapsed: 1.179 s % 94.79/13.62 % (3880868)Peak memory usage: 19 MB % 94.79/13.62 % (3880868)Instructions burned: 2251 (million) % 94.79/13.62 % (3880874)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1940816642:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 94.79/13.62 % (3880864)Instruction limit reached! % 94.79/13.62 % (3880864)------------------------------ % 94.79/13.62 % (3880864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.79/13.62 % (3880864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.79/13.62 % (3880864)CaDiCaL version: 2.1.3 % 94.79/13.62 % (3880864)Termination reason: Instruction limit % 141.70/20.25 % (3880864)Termination phase: Saturation % 141.70/20.25 % (3880864)Time elapsed: 2.035 s % 141.70/20.25 % (3880864)Peak memory usage: 32 MB % 141.70/20.25 % (3880864)Instructions burned: 3513 (million) % 141.70/20.25 % (3880876)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=531628970:i=5211_2969 on theBenchmark for (2969ds/5211Mi) % 141.70/20.25 % (3880872)Instruction limit reached! % 141.70/20.25 % (3880872)------------------------------ % 141.70/20.25 % (3880872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.70/20.25 % (3880872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.70/20.25 % (3880872)CaDiCaL version: 2.1.3 % 141.70/20.25 % (3880872)Termination reason: Instruction limit % 141.70/20.25 % (3880872)Termination phase: Saturation % 141.70/20.25 % (3880872)Time elapsed: 1.205 s % 141.70/20.25 % (3880872)Peak memory usage: 56 MB % 141.70/20.25 % (3880872)Instructions burned: 4593 (million) % 141.70/20.25 % (3880878)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1751560052:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 141.70/20.25 % (3880878)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.70/20.25 % (3880878)Terminated due to inappropriate strategy. % 141.70/20.25 % (3880878)------------------------------ % 141.70/20.25 % (3880878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.70/20.25 % (3880878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.70/20.25 % (3880878)CaDiCaL version: 2.1.3 % 141.70/20.25 % (3880878)Termination reason: Inappropriate % 141.70/20.25 % (3880878)Time elapsed: 0.003 s % 141.70/20.25 % (3880878)Peak memory usage: 11 MB % 141.70/20.25 % (3880878)Instructions burned: 9 (million) % 141.70/20.25 % (3880878)------------------------------ % 141.70/20.25 % (3880878)------------------------------ % 141.70/20.25 % (3880880)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4046272548:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 141.70/20.25 % (3880880)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.70/20.25 % (3880880)Terminated due to inappropriate strategy. % 141.70/20.25 % (3880880)------------------------------ % 141.70/20.25 % (3880880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.70/20.25 % (3880880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.70/20.25 % (3880880)CaDiCaL version: 2.1.3 % 141.70/20.25 % (3880880)Termination reason: Inappropriate % 141.70/20.25 % (3880880)Time elapsed: 0.004 s % 141.70/20.25 % (3880880)Peak memory usage: 11 MB % 141.70/20.25 % (3880880)Instructions burned: 8 (million) % 141.70/20.25 % (3880880)------------------------------ % 141.70/20.25 % (3880880)------------------------------ % 141.70/20.25 % (3880882)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2778580033:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 141.70/20.25 % (3880882)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.70/20.25 % (3880882)Terminated due to inappropriate strategy. % 141.70/20.25 % (3880882)------------------------------ % 141.70/20.25 % (3880882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.70/20.25 % (3880882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.70/20.25 % (3880882)CaDiCaL version: 2.1.3 % 141.70/20.25 % (3880882)Termination reason: Inappropriate % 141.70/20.25 % (3880882)Time elapsed: 0.004 s % 141.70/20.25 % (3880882)Peak memory usage: 11 MB % 141.70/20.25 % (3880882)Instructions burned: 8 (million) % 141.70/20.25 % (3880882)------------------------------ % 141.70/20.25 % (3880882)------------------------------ % 141.70/20.25 % (3880884)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2978618355:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 141.70/20.25 % (3880866)Instruction limit reached! % 141.70/20.25 % (3880866)------------------------------ % 141.70/20.25 % (3880866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.70/20.25 % (3880866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.70/20.25 % (3880866)CaDiCaL version: 2.1.3 % 141.70/20.25 % (3880866)Termination reason: Instruction limit % 141.70/20.25 % (3880866)Termination phase: Saturation % 141.70/20.25 % (3880866)Time elapsed: 2.222 s % 141.70/20.25 % (3880866)Peak memory usage: 38 MB % 141.70/20.25 % (3880866)Instructions burned: 3774 (million) % 141.70/20.25 % (3880886)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=678535022:i=8173:av=off_2965 on theBenchmark for (2965ds/8173Mi) % 141.70/20.25 % (3880860)Instruction limit reached! % 128.44/20.40 % (3880860)------------------------------ % 128.44/20.40 % (3880860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.44/20.40 % (3880860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.44/20.40 % (3880860)CaDiCaL version: 2.1.3 % 128.44/20.40 % (3880860)Termination reason: Instruction limit % 128.44/20.40 % (3880860)Termination phase: Saturation % 128.44/20.40 % (3880860)Time elapsed: 3.066 s % 128.44/20.40 % (3880860)Peak memory usage: 39 MB % 128.44/20.40 % (3880860)Instructions burned: 5114 (million) % 128.44/20.40 % (3880888)dis+10_16:1_sil=16000:random_seed=3726039663:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi) % 128.44/20.40 % (3880876)Instruction limit reached! % 128.44/20.40 % (3880876)------------------------------ % 128.44/20.40 % (3880876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.44/20.40 % (3880876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.44/20.40 % (3880876)CaDiCaL version: 2.1.3 % 128.44/20.40 % (3880876)Termination reason: Instruction limit % 128.44/20.40 % (3880876)Termination phase: Saturation % 128.44/20.40 % (3880876)Time elapsed: 2.630 s % 128.44/20.40 % (3880876)Peak memory usage: 45 MB % 128.44/20.40 % (3880876)Instructions burned: 5212 (million) % 128.44/20.40 % (3880890)ott-3_8_sil=64000:random_seed=479231650:i=20139:bs=on_2943 on theBenchmark for (2943ds/20139Mi) % 128.44/20.40 % (3880886)Instruction limit reached! % 128.44/20.40 % (3880886)------------------------------ % 128.44/20.40 % (3880886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.44/20.40 % (3880886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.44/20.40 % (3880886)CaDiCaL version: 2.1.3 % 128.44/20.40 % (3880886)Termination reason: Instruction limit % 128.44/20.40 % (3880886)Termination phase: Saturation % 128.44/20.40 % (3880886)Time elapsed: 4.847 s % 128.44/20.40 % (3880886)Peak memory usage: 67 MB % 128.44/20.40 % (3880886)Instructions burned: 8174 (million) % 128.44/20.40 % (3880892)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3211566476:fmbsr=2:i=32576_2916 on theBenchmark for (2916ds/32576Mi) % 128.44/20.40 % (3880892)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.44/20.40 % (3880892)Terminated due to inappropriate strategy. % 128.44/20.40 % (3880892)------------------------------ % 128.44/20.40 % (3880892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.44/20.40 % (3880892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.44/20.40 % (3880892)CaDiCaL version: 2.1.3 % 128.44/20.40 % (3880892)Termination reason: Inappropriate % 128.44/20.40 % (3880892)Time elapsed: 0.005 s % 128.44/20.40 % (3880892)Peak memory usage: 11 MB % 128.44/20.40 % (3880892)Instructions burned: 9 (million) % 128.44/20.40 % (3880892)------------------------------ % 128.44/20.40 % (3880892)------------------------------ % 128.44/20.40 % (3880894)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2205203128:i=11404_2916 on theBenchmark for (2916ds/11404Mi) % 128.44/20.40 % (3880884)Instruction limit reached! % 128.44/20.40 % (3880884)------------------------------ % 128.44/20.40 % (3880884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.44/20.40 % (3880884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.44/20.40 % (3880884)CaDiCaL version: 2.1.3 % 128.44/20.40 % (3880884)Termination reason: Instruction limit % 128.44/20.40 % (3880884)Termination phase: Saturation % 128.44/20.40 % (3880884)Time elapsed: 5.290 s % 128.44/20.40 % (3880884)Peak memory usage: 33 MB % 128.44/20.40 % (3880884)Instructions burned: 22569 (million) % 128.44/20.40 % (3880896)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=691113008:i=14134_2914 on theBenchmark for (2914ds/14134Mi) % 128.44/20.40 % (3880888)Instruction limit reached! % 128.44/20.40 % (3880888)------------------------------ % 128.44/20.40 % (3880888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.44/20.40 % (3880888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.44/20.40 % (3880888)CaDiCaL version: 2.1.3 % 128.44/20.40 % (3880888)Termination reason: Instruction limit % 128.44/20.40 % (3880888)Termination phase: Saturation % 128.44/20.40 % (3880888)Time elapsed: 4.866 s % 128.44/20.40 % (3880888)Peak memory usage: 56 MB % 128.44/20.40 % (3880888)Instructions burned: 9156 (million) % 128.44/20.40 % (3880898)dis+33_16_sil=32000:sac=on:random_seed=945720786:i=15851:nm=0_2912 on theBenchmark for (2912ds/15851Mi) % 128.44/20.40 % (3880896)Instruction limit reached! % 128.44/20.40 % (3880896)------------------------------ % 128.44/20.40 % (3880896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.78/23.04 % (3880896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.78/23.04 % (3880896)CaDiCaL version: 2.1.3 % 160.78/23.04 % (3880896)Termination reason: Instruction limit % 160.78/23.04 % (3880896)Termination phase: Saturation % 160.78/23.04 % (3880896)Time elapsed: 4.832 s % 160.78/23.04 % (3880896)Peak memory usage: 90 MB % 160.78/23.04 % (3880896)Instructions burned: 14138 (million) % 160.78/23.04 % (3880944)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1147658770:avsq=on:i=17627:add=on:amm=off_2866 on theBenchmark for (2866ds/17627Mi) % 160.78/23.04 % (3880894)Instruction limit reached! % 160.78/23.04 % (3880894)------------------------------ % 160.78/23.04 % (3880894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.78/23.04 % (3880894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.78/23.04 % (3880894)CaDiCaL version: 2.1.3 % 160.78/23.04 % (3880894)Termination reason: Instruction limit % 160.78/23.04 % (3880894)Termination phase: Saturation % 160.78/23.04 % (3880894)Time elapsed: 8.056 s % 160.78/23.04 % (3880894)Peak memory usage: 84 MB % 160.78/23.04 % (3880894)Instructions burned: 11404 (million) % 160.78/23.04 % (3881235)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1707028971:s2a=on:i=53295_2835 on theBenchmark for (2835ds/53295Mi) % 160.78/23.04 % (3880874)Instruction limit reached! % 160.78/23.04 % (3880874)------------------------------ % 160.78/23.04 % (3880874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.78/23.04 % (3880874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.78/23.04 % (3880874)CaDiCaL version: 2.1.3 % 160.78/23.04 % (3880874)Termination reason: Instruction limit % 160.78/23.04 % (3880874)Termination phase: Saturation % 160.78/23.04 % (3880874)Time elapsed: 14.138 s % 160.78/23.04 % (3880874)Peak memory usage: 198 MB % 160.78/23.04 % (3880874)Instructions burned: 29341 (million) % 160.78/23.04 % (3881248)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=173476727:i=26857:ins=20_2832 on theBenchmark for (2832ds/26857Mi) % 160.78/23.04 % (3881248)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.78/23.04 % (3881248)Terminated due to inappropriate strategy. % 160.78/23.04 % (3881248)------------------------------ % 160.78/23.04 % (3881248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.78/23.04 % (3881248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.78/23.04 % (3881248)CaDiCaL version: 2.1.3 % 160.78/23.04 % (3881248)Termination reason: Inappropriate % 160.78/23.04 % (3881248)Time elapsed: 0.007 s % 160.78/23.04 % (3881248)Peak memory usage: 10 MB % 160.78/23.04 % (3881248)Instructions burned: 8 (million) % 160.78/23.04 % (3881248)------------------------------ % 160.78/23.04 % (3881248)------------------------------ % 160.78/23.04 % (3881250)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=96234094:i=28120:bs=on:fsr=off_2832 on theBenchmark for (2832ds/28120Mi) % 160.78/23.04 % (3880898)Instruction limit reached! % 160.78/23.04 % (3880898)------------------------------ % 160.78/23.04 % (3880898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.78/23.04 % (3880898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.78/23.04 % (3880898)CaDiCaL version: 2.1.3 % 160.78/23.04 % (3880898)Termination reason: Instruction limit % 160.78/23.04 % (3880898)Termination phase: Saturation % 160.78/23.04 % (3880898)Time elapsed: 11.138 s % 160.78/23.04 % (3880898)Peak memory usage: 158 MB % 160.78/23.04 % (3880898)Instructions burned: 15852 (million) % 160.78/23.04 % (3881332)fmb+10_1_sil=256000:fmbss=7:random_seed=535272077:fmbsr=1.6:i=182295_2800 on theBenchmark for (2800ds/182295Mi) % 160.78/23.04 % (3881332)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.78/23.04 % (3881332)Terminated due to inappropriate strategy. % 160.78/23.04 % (3881332)------------------------------ % 160.78/23.04 % (3881332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.78/23.04 % (3881332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.78/23.04 % (3881332)CaDiCaL version: 2.1.3 % 160.78/23.04 % (3881332)Termination reason: Inappropriate % 160.78/23.04 % (3881332)Time elapsed: 0.008 s % 160.78/23.04 % (3881332)Peak memory usage: 10 MB % 160.78/23.04 % (3881332)Instructions burned: 8 (million) % 160.78/23.04 % (3881332)------------------------------ % 160.78/23.04 % (3881332)------------------------------ % 160.78/23.04 % (3881335)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3877870821:i=44625:gsp=on_2800 on theBenchmark for (2800ds/44625Mi) % 180.29/25.79 % (3881335)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.29/25.79 % (3881335)Terminated due to inappropriate strategy. % 180.29/25.79 % (3881335)------------------------------ % 180.29/25.79 % (3881335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.29/25.79 % (3881335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.29/25.79 % (3881335)CaDiCaL version: 2.1.3 % 180.29/25.79 % (3881335)Termination reason: Inappropriate % 180.29/25.79 % (3881335)Time elapsed: 0.005 s % 180.29/25.79 % (3881335)Peak memory usage: 11 MB % 180.29/25.79 % (3881335)Instructions burned: 8 (million) % 180.29/25.79 % (3881335)------------------------------ % 180.29/25.79 % (3881335)------------------------------ % 180.29/25.79 % (3881337)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2770581967:i=160505_2799 on theBenchmark for (2799ds/160505Mi) % 180.29/25.79 % (3881337)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.29/25.79 % (3881337)Terminated due to inappropriate strategy. % 180.29/25.79 % (3881337)------------------------------ % 180.29/25.79 % (3881337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.29/25.79 % (3881337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.29/25.79 % (3881337)CaDiCaL version: 2.1.3 % 180.29/25.79 % (3881337)Termination reason: Inappropriate % 180.29/25.79 % (3881337)Time elapsed: 0.005 s % 180.29/25.79 % (3881337)Peak memory usage: 11 MB % 180.29/25.79 % (3881337)Instructions burned: 8 (million) % 180.29/25.79 % (3881337)------------------------------ % 180.29/25.79 % (3881337)------------------------------ % 180.29/25.79 % (3881340)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=227759366:fmbsr=1.3:i=225729_2799 on theBenchmark for (2799ds/225729Mi) % 180.29/25.79 % (3881340)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.29/25.79 % (3881340)Terminated due to inappropriate strategy. % 180.29/25.79 % (3881340)------------------------------ % 180.29/25.79 % (3881340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.29/25.79 % (3881340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.29/25.79 % (3881340)CaDiCaL version: 2.1.3 % 180.29/25.79 % (3881340)Termination reason: Inappropriate % 180.29/25.79 % (3881340)Time elapsed: 0.010 s % 180.29/25.79 % (3881340)Peak memory usage: 11 MB % 180.29/25.79 % (3881340)Instructions burned: 8 (million) % 180.29/25.79 % (3881340)------------------------------ % 180.29/25.79 % (3881340)------------------------------ % 180.29/25.79 % (3881342)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=793331898:fmbsr=2:i=185024:ins=7_2799 on theBenchmark for (2799ds/185024Mi) % 180.29/25.79 % (3881342)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.29/25.79 % (3881342)Terminated due to inappropriate strategy. % 180.29/25.79 % (3881342)------------------------------ % 180.29/25.79 % (3881342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.29/25.79 % (3881342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.29/25.79 % (3881342)CaDiCaL version: 2.1.3 % 180.29/25.79 % (3881342)Termination reason: Inappropriate % 180.29/25.79 % (3881342)Time elapsed: 0.005 s % 180.29/25.79 % (3881342)Peak memory usage: 11 MB % 180.29/25.79 % (3881342)Instructions burned: 8 (million) % 180.29/25.79 % (3881342)------------------------------ % 180.29/25.79 % (3881342)------------------------------ % 180.29/25.79 % (3880890)Instruction limit reached! % 180.29/25.79 % (3880890)------------------------------ % 180.29/25.79 % (3880890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.29/25.79 % (3880890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.29/25.79 % (3880890)CaDiCaL version: 2.1.3 % 180.29/25.79 % (3880890)Termination reason: Instruction limit % 180.29/25.79 % (3880890)Termination phase: Saturation % 180.29/25.79 % (3880890)Time elapsed: 14.407 s % 180.29/25.79 % (3880890)Peak memory usage: 172 MB % 180.29/25.79 % (3880890)Instructions burned: 20139 (million) % 180.29/25.79 % (3881344)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4158695196:rtra=on_2798 on theBenchmark for (2798ds/0Mi) % 180.29/25.79 % (3881344)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.29/25.79 % (3881344)Terminated due to inappropriate strategy. % 180.29/25.79 % (3881344)------------------------------ % 180.29/25.79 % (3881344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.29/25.79 % (3881344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.71/29.05 % (3881344)CaDiCaL version: 2.1.3 % 202.71/29.05 % (3881344)Termination reason: Inappropriate % 202.71/29.05 % (3881344)Time elapsed: 0.010 s % 202.71/29.05 % (3881344)Peak memory usage: 11 MB % 202.71/29.05 % (3881344)Instructions burned: 10 (million) % 202.71/29.05 % (3881344)------------------------------ % 202.71/29.05 % (3881344)------------------------------ % 202.71/29.05 % (3881349)% WARNING: option uhcvi not known. % 202.71/29.05 % (3881349)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3816241804:i=271062:add=off:rtra=on:rawr=on_2798 on theBenchmark for (2798ds/271062Mi) % 202.71/29.05 % (3881350)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1934949259:i=176048:add=on:rtra=on:rawr=on_2798 on theBenchmark for (2798ds/176048Mi) % 202.71/29.05 % (3880944)Instruction limit reached! % 202.71/29.05 % (3880944)------------------------------ % 202.71/29.05 % (3880944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.71/29.05 % (3880944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.71/29.05 % (3880944)CaDiCaL version: 2.1.3 % 202.71/29.05 % (3880944)Termination reason: Instruction limit % 202.71/29.05 % (3880944)Termination phase: Saturation % 202.71/29.05 % (3880944)Time elapsed: 8.520 s % 202.71/29.05 % (3880944)Peak memory usage: 117 MB % 202.71/29.05 % (3880944)Instructions burned: 17627 (million) % 202.71/29.05 % (3881381)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1953595620:i=206:fgj=on:rtra=on_2780 on theBenchmark for (2780ds/206Mi) % 202.71/29.05 % (3881381)Instruction limit reached! % 202.71/29.05 % (3881381)------------------------------ % 202.71/29.05 % (3881381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.71/29.05 % (3881381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.71/29.05 % (3881381)CaDiCaL version: 2.1.3 % 202.71/29.05 % (3881381)Termination reason: Instruction limit % 202.71/29.05 % (3881381)Termination phase: Saturation % 202.71/29.05 % (3881381)Time elapsed: 0.190 s % 202.71/29.05 % (3881381)Peak memory usage: 14 MB % 202.71/29.05 % (3881381)Instructions burned: 207 (million) % 202.71/29.05 % (3881385)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3993531599:i=232:rtra=on_2778 on theBenchmark for (2778ds/232Mi) % 202.71/29.05 % (3881385)Instruction limit reached! % 202.71/29.05 % (3881385)------------------------------ % 202.71/29.05 % (3881385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.71/29.05 % (3881385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.71/29.05 % (3881385)CaDiCaL version: 2.1.3 % 202.71/29.05 % (3881385)Termination reason: Instruction limit % 202.71/29.05 % (3881385)Termination phase: Saturation % 202.71/29.05 % (3881385)Time elapsed: 0.170 s % 202.71/29.05 % (3881385)Peak memory usage: 14 MB % 202.71/29.05 % (3881385)Instructions burned: 233 (million) % 202.71/29.05 % (3881388)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=828763829:i=262:rtra=on_2776 on theBenchmark for (2776ds/262Mi) % 202.71/29.05 % (3881388)Instruction limit reached! % 202.71/29.05 % (3881388)------------------------------ % 202.71/29.05 % (3881388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.71/29.05 % (3881388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.71/29.05 % (3881388)CaDiCaL version: 2.1.3 % 202.71/29.05 % (3881388)Termination reason: Instruction limit % 202.71/29.05 % (3881388)Termination phase: Saturation % 202.71/29.05 % (3881388)Time elapsed: 0.179 s % 202.71/29.05 % (3881388)Peak memory usage: 15 MB % 202.71/29.05 % (3881388)Instructions burned: 263 (million) % 202.71/29.05 % (3881391)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2430122125:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2774 on theBenchmark for (2774ds/318Mi) % 202.71/29.05 % (3881391)Instruction limit reached! % 202.71/29.05 % (3881391)------------------------------ % 202.71/29.05 % (3881391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.71/29.05 % (3881391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.71/29.05 % (3881391)CaDiCaL version: 2.1.3 % 202.71/29.05 % (3881391)Termination reason: Instruction limit % 202.71/29.05 % (3881391)Termination phase: Saturation % 202.71/29.05 % (3881391)Time elapsed: 0.201 s % 202.71/29.05 % (3881391)Peak memory usage: 15 MB % 202.71/29.05 % (3881391)Instructions burned: 319 (million) % 202.71/29.05 % (3881395)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4111459247:i=1428:nm=2:rtra=on_2772 on theBenchmark for (2772ds/1428Mi) % 256.94/36.42 % (3881395)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 256.94/36.42 % (3881395)Terminated due to inappropriate strategy. % 256.94/36.42 % (3881395)------------------------------ % 256.94/36.42 % (3881395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.94/36.42 % (3881395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.94/36.42 % (3881395)CaDiCaL version: 2.1.3 % 256.94/36.42 % (3881395)Termination reason: Inappropriate % 256.94/36.42 % (3881395)Time elapsed: 0.005 s % 256.94/36.42 % (3881395)Peak memory usage: 10 MB % 256.94/36.42 % (3881395)Instructions burned: 9 (million) % 256.94/36.42 % (3881395)------------------------------ % 256.94/36.42 % (3881395)------------------------------ % 256.94/36.42 % (3881397)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3816905195:i=262:bd=preordered:rtra=on:fsd=on_2771 on theBenchmark for (2771ds/262Mi) % 256.94/36.42 % (3881397)Instruction limit reached! % 256.94/36.42 % (3881397)------------------------------ % 256.94/36.42 % (3881397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.94/36.42 % (3881397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.94/36.42 % (3881397)CaDiCaL version: 2.1.3 % 256.94/36.42 % (3881397)Termination reason: Instruction limit % 256.94/36.42 % (3881397)Termination phase: Saturation % 256.94/36.42 % (3881397)Time elapsed: 0.268 s % 256.94/36.42 % (3881397)Peak memory usage: 15 MB % 256.94/36.42 % (3881397)Instructions burned: 263 (million) % 256.94/36.42 % (3881402)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=1136371483:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2769 on theBenchmark for (2769ds/1368Mi) % 256.94/36.42 % (3881402)Instruction limit reached! % 256.94/36.42 % (3881402)------------------------------ % 256.94/36.42 % (3881402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.94/36.42 % (3881402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.94/36.42 % (3881402)CaDiCaL version: 2.1.3 % 256.94/36.42 % (3881402)Termination reason: Instruction limit % 256.94/36.42 % (3881402)Termination phase: Saturation % 256.94/36.42 % (3881402)Time elapsed: 1.471 s % 256.94/36.42 % (3881402)Peak memory usage: 25 MB % 256.94/36.42 % (3881402)Instructions burned: 1369 (million) % 256.94/36.42 % (3881411)ott-21_1_sil=16000:si=on:fs=off:random_seed=38974673:i=360:av=off:fsr=off:rtra=on_2753 on theBenchmark for (2753ds/360Mi) % 256.94/36.42 % (3881411)Instruction limit reached! % 256.94/36.42 % (3881411)------------------------------ % 256.94/36.42 % (3881411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.94/36.42 % (3881411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.94/36.42 % (3881411)CaDiCaL version: 2.1.3 % 256.94/36.42 % (3881411)Termination reason: Instruction limit % 256.94/36.42 % (3881411)Termination phase: Saturation % 256.94/36.42 % (3881411)Time elapsed: 0.327 s % 256.94/36.42 % (3881411)Peak memory usage: 14 MB % 256.94/36.42 % (3881411)Instructions burned: 361 (million) % 256.94/36.42 % (3881416)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2503514147:i=954:bd=all:rtra=on_2750 on theBenchmark for (2750ds/954Mi) % 256.94/36.42 % (3881416)Instruction limit reached! % 256.94/36.42 % (3881416)------------------------------ % 256.94/36.42 % (3881416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.94/36.42 % (3881416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.94/36.42 % (3881416)CaDiCaL version: 2.1.3 % 256.94/36.42 % (3881416)Termination reason: Instruction limit % 256.94/36.42 % (3881416)Termination phase: Saturation % 256.94/36.42 % (3881416)Time elapsed: 0.532 s % 256.94/36.42 % (3881416)Peak memory usage: 16 MB % 256.94/36.42 % (3881416)Instructions burned: 956 (million) % 256.94/36.42 % (3881422)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2541941592:fmbsr=1.3:i=1730:ins=25:rtra=on_2744 on theBenchmark for (2744ds/1730Mi) % 256.94/36.42 % (3881422)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 256.94/36.42 % (3881422)Terminated due to inappropriate strategy. % 256.94/36.42 % (3881422)------------------------------ % 256.94/36.42 % (3881422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.94/36.42 % (3881422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.94/36.42 % (3881422)CaDiCaL version: 2.1.3 % 256.94/36.42 % (3881422)Termination reason: Inappropriate % 256.94/36.42 % (3881422)Time elapsed: 0.005 s % 300.43/42.63 % (3881422)Peak memory usage: 11 MB % 300.43/42.63 % (3881422)Instructions burned: 9 (million) % 300.43/42.63 % (3881422)------------------------------ % 300.43/42.63 % (3881422)------------------------------ % 300.43/42.63 % (3881424)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1632996906:i=2358:rtra=on_2744 on theBenchmark for (2744ds/2358Mi) % 300.43/42.63 % (3881424)Instruction limit reached! % 300.43/42.63 % (3881424)------------------------------ % 300.43/42.63 % (3881424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3881424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3881424)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3881424)Termination reason: Instruction limit % 300.43/42.63 % (3881424)Termination phase: Saturation % 300.43/42.63 % (3881424)Time elapsed: 1.416 s % 300.43/42.63 % (3881424)Peak memory usage: 32 MB % 300.43/42.63 % (3881424)Instructions burned: 2358 (million) % 300.43/42.63 % (3881427)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2444122638:i=1778:ins=1:rtra=on_2730 on theBenchmark for (2730ds/1778Mi) % 300.43/42.63 % (3881427)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.43/42.63 % (3881427)Terminated due to inappropriate strategy. % 300.43/42.63 % (3881427)------------------------------ % 300.43/42.63 % (3881427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3881427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3881427)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3881427)Termination reason: Inappropriate % 300.43/42.63 % (3881427)Time elapsed: 0.006 s % 300.43/42.63 % (3881427)Peak memory usage: 11 MB % 300.43/42.63 % (3881427)Instructions burned: 9 (million) % 300.43/42.63 % (3881427)------------------------------ % 300.43/42.63 % (3881427)------------------------------ % 300.43/42.63 % (3881429)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=1802180275:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2729 on theBenchmark for (2729ds/1384Mi) % 300.43/42.63 % (3881429)Instruction limit reached! % 300.43/42.63 % (3881429)------------------------------ % 300.43/42.63 % (3881429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3881429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3881429)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3881429)Termination reason: Instruction limit % 300.43/42.63 % (3881429)Termination phase: Saturation % 300.43/42.63 % (3881429)Time elapsed: 0.778 s % 300.43/42.63 % (3881429)Peak memory usage: 22 MB % 300.43/42.63 % (3881429)Instructions burned: 1384 (million) % 300.43/42.63 % (3881437)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=512617490:i=1758:kws=inv_precedence:fsr=off:rtra=on_2721 on theBenchmark for (2721ds/1758Mi) % 300.43/42.63 % (3881437)Instruction limit reached! % 300.43/42.63 % (3881437)------------------------------ % 300.43/42.63 % (3881437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3881437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3881437)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3881437)Termination reason: Instruction limit % 300.43/42.63 % (3881437)Termination phase: Saturation % 300.43/42.63 % (3881437)Time elapsed: 0.910 s % 300.43/42.63 % (3881437)Peak memory usage: 24 MB % 300.43/42.63 % (3881437)Instructions burned: 1760 (million) % 300.43/42.63 % (3881444)fmb+10_1_sil=64000:si=on:random_seed=1007783437:i=44122:nm=2:rtra=on:gsp=on_2712 on theBenchmark for (2712ds/44122Mi) % 300.43/42.63 % (3881444)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.43/42.63 % (3881444)Terminated due to inappropriate strategy. % 300.43/42.63 % (3881444)------------------------------ % 300.43/42.63 % (3881444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3881444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3881444)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3881444)Termination reason: Inappropriate % 300.43/42.63 % (3881444)Time elapsed: 0.005 s % 300.43/42.63 % (3881444)Peak memory usage: 10 MB % 300.43/42.63 % (3881444)Instructions burned: 9 (million) % 300.43/42.63 % (3881444)------------------------------ % 300.43/42.63 % (3881444)------------------------------ % 300.43/42.63 % (3881446)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=983748999:i=19030:nm=5:rtra=on_2712 on theBenchmark for (2712ds/19030Mi) % 300.43/42.63 % (3881446)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.43/42.63 % (3881446)Terminated due to inappropriate strategy. % 300.43/42.63 % (3881446)------------------------------ % 300.43/42.63 % (3881446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3881446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3881446)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3881446)Termination reason: Inappropriate % 300.43/42.63 % (3881446)Time elapsed: 0.005 s % 300.43/42.63 % (3881446)Peak memory usage: 10 MB % 300.43/42.63 % (3881446)Instructions burned: 9 (million) % 300.43/42.63 % (3881446)------------------------------ % 300.43/42.63 % (3881446)------------------------------ % 300.43/42.63 % (3881448)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3492148165:fmbsr=1.7:i=1840:rtra=on_2711 on theBenchmark for (2711ds/1840Mi) % 300.43/42.63 % (3881448)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.43/42.63 % (3881448)Terminated due to inappropriate strategy. % 300.43/42.63 % (3881448)------------------------------ % 300.43/42.63 % (3881448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3881448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3881448)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3881448)Termination reason: Inappropriate % 300.43/42.63 % (3881448)Time elapsed: 0.006 s % 300.43/42.63 % (3881448)Peak memory usage: 11 MB % 300.43/42.63 % (3881448)Instructions burned: 9 (million) % 300.43/42.63 % (3881448)------------------------------ % 300.43/42.63 % (3881448)------------------------------ % 300.43/42.63 % (3881450)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2099290379:i=10262:rtra=on_2711 on theBenchmark for (2711ds/10262Mi) % 300.43/42.63 % (3881450)Instruction limit reached! % 300.43/42.63 % (3881450)------------------------------ % 300.43/42.63 % (3881450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3881450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3881450)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3881450)Termination reason: Instruction limit % 300.43/42.63 % (3881450)Termination phase: Saturation % 300.43/42.63 % (3881450)Time elapsed: 5.673 s % 300.43/42.63 % (3881450)Peak memory usage: 74 MB % 300.43/42.63 % (3881450)Instructions burned: 10263 (million) % 300.43/42.63 % (3881464)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3694150994:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2654 on theBenchmark for (2654ds/2944Mi) % 300.43/42.63 % (3881464)Instruction limit reached! % 300.43/42.63 % (3881464)------------------------------ % 300.43/42.63 % (3881464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3881464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3881464)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3881464)Termination reason: Instruction limit % 300.43/42.63 % (3881464)Termination phase: Saturation % 300.43/42.63 % (3881464)Time elapsed: 1.553 s % 300.43/42.63 % (3881464)Peak memory usage: 40 MB % 300.43/42.63 % (3881464)Instructions burned: 2945 (million) % 300.43/42.63 % (3881466)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=4248741841:i=12648:rtra=on_2638 on theBenchmark for (2638ds/12648Mi) % 300.43/42.63 % (3881466)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.43/42.63 % (3881466)Terminated due to inappropriate strategy. % 300.43/42.63 % (3881466)------------------------------ % 300.43/42.63 % (3881466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3881466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3881466)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3881466)Termination reason: Inappropriate % 300.43/42.63 % (3881466)Time elapsed: 0.007 s % 300.43/42.63 % (3881466)Peak memory usage: 11 MB % 300.43/42.63 % (3881466)Instructions burned: 10 (million) % 300.43/42.63 % (3881466)------------------------------ % 300.43/42.63 % (3881466)------------------------------ % 300.43/42.63 % (3881468)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=4158595380:fmbsr=2.30978:i=4348:rtra=on_2638 on theBenchmark for (2638ds/4348Mi) % 300.43/42.63 % (3881468)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.43/42.63 % (3881468)Terminated due to inappropriate strategy. % 300.43/42.63 % (3881468)------------------------------ % 300.43/42.63 % (3881468)Version: Vam % 300.43/42.63 Terminated % 300.43/42.63 % Vampire exiting % 300.43/42.64 Terminated %------------------------------------------------------------------------------