%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW829_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n014.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:45:02 PM UTC 2026 % Result : Timeout 296.44s 42.09s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW829_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.27 % Computer : n014.cluster.edu % 0.11/0.27 % Model : x86_64 x86_64 % 0.11/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.27 % Memory : 8046.5625MB % 0.11/0.27 % OS : Linux 6.8.0-71-generic % 0.11/0.27 % CPULimit : 300 % 0.11/0.27 % WCLimit : 300 % 0.11/0.27 % DateTime : Mon Sep 28 14:30:46 UTC 2026 % 0.11/0.27 % CPUTime : % 0.11/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.27/0.32 Running first-order model finding % 0.27/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.06/1.26 % (1818746)Will run a generic schedule for satisfiability detection. % 6.06/1.26 % (1818753)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1769851230_2999 on theBenchmark for (2999ds/0Mi) % 6.06/1.26 % (1818754)% WARNING: option uhcvi not known. % 6.06/1.26 % (1818754)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1299770116:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.06/1.26 % (1818755)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2904348479:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.06/1.26 % (1818756)dis+10_1_sil=32000:sp=arity:random_seed=1099803536:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.06/1.26 % (1818757)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2311956887:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.06/1.26 % (1818758)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=873952325:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.06/1.26 % (1818759)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1565160914:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.06/1.26 % (1818753)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.06/1.26 % (1818753)Terminated due to inappropriate strategy. % 6.06/1.26 % (1818753)------------------------------ % 6.06/1.26 % (1818753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.06/1.26 % (1818753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.06/1.26 % (1818753)CaDiCaL version: 2.1.3 % 6.06/1.26 % (1818753)Termination reason: Inappropriate % 6.06/1.26 % (1818753)Time elapsed: 0.035 s % 6.06/1.26 % (1818753)Peak memory usage: 13 MB % 6.06/1.26 % (1818753)Instructions burned: 75 (million) % 6.06/1.26 % (1818753)------------------------------ % 6.06/1.26 % (1818753)------------------------------ % 6.06/1.26 % (1818769)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2507831416:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.06/1.26 % (1818769)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.06/1.26 % (1818769)Terminated due to inappropriate strategy. % 6.06/1.26 % (1818769)------------------------------ % 6.06/1.26 % (1818769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.06/1.26 % (1818769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.06/1.26 % (1818769)CaDiCaL version: 2.1.3 % 6.06/1.26 % (1818769)Termination reason: Inappropriate % 6.06/1.26 % (1818769)Time elapsed: 0.034 s % 6.06/1.26 % (1818769)Peak memory usage: 12 MB % 6.06/1.26 % (1818769)Instructions burned: 73 (million) % 6.06/1.26 % (1818769)------------------------------ % 6.06/1.26 % (1818769)------------------------------ % 6.06/1.26 % (1818756)Instruction limit reached! % 6.06/1.26 % (1818756)------------------------------ % 6.06/1.26 % (1818756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.06/1.26 % (1818756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.06/1.26 % (1818756)CaDiCaL version: 2.1.3 % 6.06/1.26 % (1818756)Termination reason: Instruction limit % 6.06/1.26 % (1818756)Termination phase: Saturation % 6.06/1.26 % (1818756)Time elapsed: 0.093 s % 6.06/1.26 % (1818756)Peak memory usage: 13 MB % 6.06/1.26 % (1818756)Instructions burned: 103 (million) % 6.06/1.26 % (1818771)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2463944160:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 6.06/1.26 % (1818757)Instruction limit reached! % 6.06/1.26 % (1818757)------------------------------ % 6.06/1.26 % (1818757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.06/1.26 % (1818757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.06/1.26 % (1818757)CaDiCaL version: 2.1.3 % 6.06/1.26 % (1818757)Termination reason: Instruction limit % 6.06/1.26 % (1818757)Termination phase: Saturation % 6.06/1.26 % (1818757)Time elapsed: 0.103 s % 6.06/1.26 % (1818757)Peak memory usage: 13 MB % 6.06/1.26 % (1818757)Instructions burned: 116 (million) % 6.06/1.26 % (1818758)Instruction limit reached! % 6.06/1.26 % (1818758)------------------------------ % 6.06/1.26 % (1818758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.06/1.26 % (1818758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.06/1.26 % (1818758)CaDiCaL version: 2.1.3 % 6.06/1.26 % (1818758)Termination reason: Instruction limit % 6.79/1.60 % (1818758)Termination phase: Saturation % 6.79/1.60 % (1818758)Time elapsed: 0.121 s % 6.79/1.60 % (1818758)Peak memory usage: 14 MB % 6.79/1.60 % (1818758)Instructions burned: 131 (million) % 6.79/1.60 % (1818772)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=2596300436:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.79/1.60 % (1818774)ott-21_1_sil=16000:fs=off:random_seed=3681869468:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.79/1.60 % (1818775)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=154188780:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.79/1.60 % (1818759)Instruction limit reached! % 6.79/1.60 % (1818759)------------------------------ % 6.79/1.60 % (1818759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.79/1.60 % (1818759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.79/1.60 % (1818759)CaDiCaL version: 2.1.3 % 6.79/1.60 % (1818759)Termination reason: Instruction limit % 6.79/1.60 % (1818759)Termination phase: Saturation % 6.79/1.60 % (1818759)Time elapsed: 0.152 s % 6.79/1.60 % (1818759)Peak memory usage: 14 MB % 6.79/1.60 % (1818759)Instructions burned: 160 (million) % 6.79/1.60 % (1818771)Instruction limit reached! % 6.79/1.60 % (1818771)------------------------------ % 6.79/1.60 % (1818771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.79/1.60 % (1818771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.79/1.60 % (1818771)CaDiCaL version: 2.1.3 % 6.79/1.60 % (1818771)Termination reason: Instruction limit % 6.79/1.60 % (1818771)Termination phase: Saturation % 6.79/1.60 % (1818771)Time elapsed: 0.067 s % 6.79/1.60 % (1818771)Peak memory usage: 14 MB % 6.79/1.60 % (1818771)Instructions burned: 133 (million) % 6.79/1.60 % (1818780)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=670793823:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 6.79/1.60 % (1818779)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2756580071:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 6.79/1.60 % (1818779)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.79/1.60 % (1818779)Terminated due to inappropriate strategy. % 6.79/1.60 % (1818779)------------------------------ % 6.79/1.60 % (1818779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.79/1.60 % (1818779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.79/1.60 % (1818779)CaDiCaL version: 2.1.3 % 6.79/1.60 % (1818779)Termination reason: Inappropriate % 6.79/1.60 % (1818779)Time elapsed: 0.064 s % 6.79/1.60 % (1818779)Peak memory usage: 12 MB % 6.79/1.60 % (1818779)Instructions burned: 73 (million) % 6.79/1.60 % (1818779)------------------------------ % 6.79/1.60 % (1818779)------------------------------ % 6.79/1.60 % (1818785)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=447620072:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 6.79/1.60 % (1818774)Instruction limit reached! % 6.79/1.60 % (1818774)------------------------------ % 6.79/1.60 % (1818774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.79/1.60 % (1818774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.79/1.60 % (1818774)CaDiCaL version: 2.1.3 % 6.79/1.60 % (1818774)Termination reason: Instruction limit % 6.79/1.60 % (1818774)Termination phase: Saturation % 6.79/1.60 % (1818774)Time elapsed: 0.155 s % 6.79/1.60 % (1818774)Peak memory usage: 14 MB % 6.79/1.60 % (1818774)Instructions burned: 180 (million) % 6.79/1.60 % (1818785)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.79/1.60 % (1818785)Terminated due to inappropriate strategy. % 6.79/1.60 % (1818785)------------------------------ % 6.79/1.60 % (1818785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.79/1.60 % (1818785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.79/1.60 % (1818785)CaDiCaL version: 2.1.3 % 6.79/1.60 % (1818785)Termination reason: Inappropriate % 6.79/1.60 % (1818785)Time elapsed: 0.040 s % 6.79/1.60 % (1818785)Peak memory usage: 12 MB % 6.79/1.60 % (1818785)Instructions burned: 74 (million) % 6.79/1.60 % (1818785)------------------------------ % 6.79/1.60 % (1818785)------------------------------ % 6.79/1.60 % (1818788)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=172194907: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) % 36.71/5.59 % (1818790)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1598986308:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 36.71/5.59 % (1818775)Instruction limit reached! % 36.71/5.59 % (1818775)------------------------------ % 36.71/5.59 % (1818775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.71/5.59 % (1818775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.71/5.59 % (1818775)CaDiCaL version: 2.1.3 % 36.71/5.59 % (1818775)Termination reason: Instruction limit % 36.71/5.59 % (1818775)Termination phase: Saturation % 36.71/5.59 % (1818775)Time elapsed: 0.473 s % 36.71/5.59 % (1818775)Peak memory usage: 16 MB % 36.71/5.59 % (1818775)Instructions burned: 477 (million) % 36.71/5.59 % (1818793)fmb+10_1_sil=64000:random_seed=627662621:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 36.71/5.59 % (1818793)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.71/5.60 % (1818793)Terminated due to inappropriate strategy. % 36.71/5.60 % (1818793)------------------------------ % 36.71/5.60 % (1818793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.71/5.60 % (1818793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.71/5.60 % (1818793)CaDiCaL version: 2.1.3 % 36.71/5.60 % (1818793)Termination reason: Inappropriate % 36.71/5.60 % (1818793)Time elapsed: 0.065 s % 36.71/5.60 % (1818793)Peak memory usage: 12 MB % 36.71/5.60 % (1818793)Instructions burned: 74 (million) % 36.71/5.60 % (1818793)------------------------------ % 36.71/5.60 % (1818793)------------------------------ % 36.71/5.60 % (1818795)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1470489866:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 36.71/5.60 % (1818780)Instruction limit reached! % 36.71/5.60 % (1818780)------------------------------ % 36.71/5.60 % (1818780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.71/5.60 % (1818780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.71/5.60 % (1818780)CaDiCaL version: 2.1.3 % 36.71/5.60 % (1818780)Termination reason: Instruction limit % 36.71/5.60 % (1818780)Termination phase: Saturation % 36.71/5.60 % (1818780)Time elapsed: 0.580 s % 36.71/5.60 % (1818780)Peak memory usage: 21 MB % 36.71/5.60 % (1818780)Instructions burned: 1181 (million) % 36.71/5.60 % (1818772)Instruction limit reached! % 36.71/5.60 % (1818772)------------------------------ % 36.71/5.60 % (1818772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.71/5.60 % (1818772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.71/5.60 % (1818772)CaDiCaL version: 2.1.3 % 36.71/5.60 % (1818772)Termination reason: Instruction limit % 36.71/5.60 % (1818772)Termination phase: Saturation % 36.71/5.60 % (1818772)Time elapsed: 0.638 s % 36.71/5.60 % (1818772)Peak memory usage: 17 MB % 36.71/5.60 % (1818772)Instructions burned: 685 (million) % 36.71/5.60 % (1818799)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=662672386:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 36.71/5.60 % (1818798)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1968845164:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi) % 36.71/5.60 % (1818795)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.71/5.60 % (1818795)Terminated due to inappropriate strategy. % 36.71/5.60 % (1818795)------------------------------ % 36.71/5.60 % (1818795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.71/5.60 % (1818795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.71/5.60 % (1818795)CaDiCaL version: 2.1.3 % 36.71/5.60 % (1818795)Termination reason: Inappropriate % 36.71/5.60 % (1818795)Time elapsed: 0.069 s % 36.71/5.60 % (1818795)Peak memory usage: 12 MB % 36.71/5.60 % (1818795)Instructions burned: 74 (million) % 36.71/5.60 % (1818795)------------------------------ % 36.71/5.60 % (1818795)------------------------------ % 36.71/5.60 % (1818803)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=668217736:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 36.71/5.60 % (1818798)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 36.71/5.60 % (1818798)Terminated due to inappropriate strategy. % 36.71/5.60 % (1818798)------------------------------ % 36.71/5.60 % (1818798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.66/9.16 % (1818798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.66/9.16 % (1818798)CaDiCaL version: 2.1.3 % 62.66/9.16 % (1818798)Termination reason: Inappropriate % 62.66/9.16 % (1818798)Time elapsed: 0.066 s % 62.66/9.16 % (1818798)Peak memory usage: 12 MB % 62.66/9.16 % (1818798)Instructions burned: 74 (million) % 62.66/9.16 % (1818798)------------------------------ % 62.66/9.16 % (1818798)------------------------------ % 62.66/9.16 % (1818805)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2890060167:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 62.66/9.16 % (1818805)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 62.66/9.16 % (1818805)Terminated due to inappropriate strategy. % 62.66/9.16 % (1818805)------------------------------ % 62.66/9.16 % (1818805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.66/9.16 % (1818805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.66/9.16 % (1818805)CaDiCaL version: 2.1.3 % 62.66/9.16 % (1818805)Termination reason: Inappropriate % 62.66/9.16 % (1818805)Time elapsed: 0.065 s % 62.66/9.16 % (1818805)Peak memory usage: 12 MB % 62.66/9.16 % (1818805)Instructions burned: 75 (million) % 62.66/9.16 % (1818805)------------------------------ % 62.66/9.16 % (1818805)------------------------------ % 62.66/9.16 % (1818807)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2655961601:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 62.66/9.16 % (1818807)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 62.66/9.16 % (1818807)Terminated due to inappropriate strategy. % 62.66/9.16 % (1818807)------------------------------ % 62.66/9.16 % (1818807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.66/9.16 % (1818807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.66/9.16 % (1818807)CaDiCaL version: 2.1.3 % 62.66/9.16 % (1818807)Termination reason: Inappropriate % 62.66/9.16 % (1818807)Time elapsed: 0.038 s % 62.66/9.16 % (1818807)Peak memory usage: 12 MB % 62.66/9.16 % (1818807)Instructions burned: 74 (million) % 62.66/9.16 % (1818807)------------------------------ % 62.66/9.16 % (1818807)------------------------------ % 62.66/9.16 % (1818788)Instruction limit reached! % 62.66/9.16 % (1818788)------------------------------ % 62.66/9.16 % (1818788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.66/9.16 % (1818788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.66/9.16 % (1818788)CaDiCaL version: 2.1.3 % 62.66/9.16 % (1818788)Termination reason: Instruction limit % 62.66/9.16 % (1818788)Termination phase: Saturation % 62.66/9.16 % (1818788)Time elapsed: 0.704 s % 62.66/9.16 % (1818788)Peak memory usage: 20 MB % 62.66/9.16 % (1818788)Instructions burned: 692 (million) % 62.66/9.16 % (1818811)ott-2_1_sil=16000:newcnf=on:random_seed=3395958659:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 62.66/9.16 % (1818812)ott+10_1_sil=32000:tgt=ground:random_seed=419140715:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 62.66/9.16 % (1818790)Instruction limit reached! % 62.66/9.16 % (1818790)------------------------------ % 62.66/9.16 % (1818790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.66/9.16 % (1818790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.66/9.16 % (1818790)CaDiCaL version: 2.1.3 % 62.66/9.16 % (1818790)Termination reason: Instruction limit % 62.66/9.16 % (1818790)Termination phase: Saturation % 62.66/9.16 % (1818790)Time elapsed: 0.757 s % 62.66/9.16 % (1818790)Peak memory usage: 19 MB % 62.66/9.16 % (1818790)Instructions burned: 880 (million) % 62.66/9.16 % (1818815)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1183210986:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 62.66/9.16 % (1818815)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 62.66/9.16 % (1818815)Terminated due to inappropriate strategy. % 62.66/9.16 % (1818815)------------------------------ % 62.66/9.16 % (1818815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.66/9.16 % (1818815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.66/9.16 % (1818815)CaDiCaL version: 2.1.3 % 62.66/9.16 % (1818815)Termination reason: Inappropriate % 62.66/9.16 % (1818815)Time elapsed: 0.065 s % 62.66/9.16 % (1818815)Peak memory usage: 13 MB % 62.66/9.16 % (1818815)Instructions burned: 75 (million) % 175.79/25.13 % (1818815)------------------------------ % 175.79/25.13 % (1818815)------------------------------ % 175.79/25.13 % (1818817)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3399413181:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 175.79/25.13 % (1818811)Instruction limit reached! % 175.79/25.13 % (1818811)------------------------------ % 175.79/25.13 % (1818811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.79/25.13 % (1818811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.79/25.13 % (1818811)CaDiCaL version: 2.1.3 % 175.79/25.13 % (1818811)Termination reason: Instruction limit % 175.79/25.13 % (1818811)Termination phase: Saturation % 175.79/25.13 % (1818811)Time elapsed: 0.656 s % 175.79/25.13 % (1818811)Peak memory usage: 15 MB % 175.79/25.13 % (1818811)Instructions burned: 869 (million) % 175.79/25.13 % (1818819)dis+21_1_sil=32000:sas=cadical:random_seed=2948814217:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi) % 175.79/25.13 % (1818803)Instruction limit reached! % 175.79/25.13 % (1818803)------------------------------ % 175.79/25.13 % (1818803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.79/25.13 % (1818803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.79/25.13 % (1818803)CaDiCaL version: 2.1.3 % 175.79/25.13 % (1818803)Termination reason: Instruction limit % 175.79/25.13 % (1818803)Termination phase: Saturation % 175.79/25.13 % (1818803)Time elapsed: 1.437 s % 175.79/25.13 % (1818803)Peak memory usage: 30 MB % 175.79/25.13 % (1818803)Instructions burned: 1472 (million) % 175.79/25.13 % (1818822)ott+11_1_sil=16000:gs=on:random_seed=4019501513:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2976 on theBenchmark for (2976ds/2251Mi) % 175.79/25.13 % (1818817)Instruction limit reached! % 175.79/25.13 % (1818817)------------------------------ % 175.79/25.13 % (1818817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.79/25.13 % (1818817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.79/25.13 % (1818817)CaDiCaL version: 2.1.3 % 175.79/25.13 % (1818817)Termination reason: Instruction limit % 175.79/25.13 % (1818817)Termination phase: Saturation % 175.79/25.13 % (1818817)Time elapsed: 3.112 s % 175.79/25.13 % (1818817)Peak memory usage: 37 MB % 175.79/25.13 % (1818817)Instructions burned: 3512 (million) % 175.79/25.13 % (1818831)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2873097804:fmbsr=1.6:i=67534_2955 on theBenchmark for (2955ds/67534Mi) % 175.79/25.13 % (1818831)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 175.79/25.13 % (1818831)Terminated due to inappropriate strategy. % 175.79/25.13 % (1818831)------------------------------ % 175.79/25.13 % (1818831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.79/25.13 % (1818831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.79/25.13 % (1818831)CaDiCaL version: 2.1.3 % 175.79/25.13 % (1818831)Termination reason: Inappropriate % 175.79/25.13 % (1818831)Time elapsed: 0.064 s % 175.79/25.13 % (1818831)Peak memory usage: 12 MB % 175.79/25.13 % (1818831)Instructions burned: 74 (million) % 175.79/25.13 % (1818831)------------------------------ % 175.79/25.13 % (1818831)------------------------------ % 175.79/25.13 % (1818835)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3004256236:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2954 on theBenchmark for (2954ds/4591Mi) % 175.79/25.13 % (1818822)Instruction limit reached! % 175.79/25.13 % (1818822)------------------------------ % 175.79/25.13 % (1818822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.79/25.13 % (1818822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.79/25.13 % (1818822)CaDiCaL version: 2.1.3 % 175.79/25.13 % (1818822)Termination reason: Instruction limit % 175.79/25.13 % (1818822)Termination phase: Saturation % 175.79/25.13 % (1818822)Time elapsed: 2.151 s % 175.79/25.13 % (1818822)Peak memory usage: 33 MB % 175.79/25.13 % (1818822)Instructions burned: 2252 (million) % 175.79/25.13 % (1818839)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1262891092:i=29340_2954 on theBenchmark for (2954ds/29340Mi) % 175.79/25.13 % (1818819)Instruction limit reached! % 175.79/25.13 % (1818819)------------------------------ % 175.79/25.13 % (1818819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.79/25.13 % (1818819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.79/25.13 % (1818819)CaDiCaL version: 2.1.3 % 175.79/25.13 % (1818819)Termination reason: Instruction limit % 218.63/31.09 % (1818819)Termination phase: Saturation % 218.63/31.09 % (1818819)Time elapsed: 3.460 s % 218.63/31.09 % (1818819)Peak memory usage: 37 MB % 218.63/31.09 % (1818819)Instructions burned: 3773 (million) % 218.63/31.09 % (1818849)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=521388825:i=5211_2947 on theBenchmark for (2947ds/5211Mi) % 218.63/31.09 % (1818799)Instruction limit reached! % 218.63/31.09 % (1818799)------------------------------ % 218.63/31.09 % (1818799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.63/31.09 % (1818799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.63/31.09 % (1818799)CaDiCaL version: 2.1.3 % 218.63/31.09 % (1818799)Termination reason: Instruction limit % 218.63/31.09 % (1818799)Termination phase: Saturation % 218.63/31.09 % (1818799)Time elapsed: 4.515 s % 218.63/31.09 % (1818799)Peak memory usage: 46 MB % 218.63/31.09 % (1818799)Instructions burned: 5131 (million) % 218.63/31.09 % (1818851)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4257096838:i=5497:nm=2_2946 on theBenchmark for (2946ds/5497Mi) % 218.63/31.09 % (1818851)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 218.63/31.09 % (1818851)Terminated due to inappropriate strategy. % 218.63/31.09 % (1818851)------------------------------ % 218.63/31.09 % (1818851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.63/31.09 % (1818851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.63/31.09 % (1818851)CaDiCaL version: 2.1.3 % 218.63/31.09 % (1818851)Termination reason: Inappropriate % 218.63/31.09 % (1818851)Time elapsed: 0.039 s % 218.63/31.09 % (1818851)Peak memory usage: 12 MB % 218.63/31.09 % (1818851)Instructions burned: 74 (million) % 218.63/31.09 % (1818851)------------------------------ % 218.63/31.09 % (1818851)------------------------------ % 218.63/31.09 % (1818853)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3401398085:fmbsr=2:i=46332_2945 on theBenchmark for (2945ds/46332Mi) % 218.63/31.09 % (1818853)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 218.63/31.09 % (1818853)Terminated due to inappropriate strategy. % 218.63/31.09 % (1818853)------------------------------ % 218.63/31.09 % (1818853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.63/31.09 % (1818853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.63/31.09 % (1818853)CaDiCaL version: 2.1.3 % 218.63/31.09 % (1818853)Termination reason: Inappropriate % 218.63/31.09 % (1818853)Time elapsed: 0.066 s % 218.63/31.09 % (1818853)Peak memory usage: 12 MB % 218.63/31.09 % (1818853)Instructions burned: 74 (million) % 218.63/31.09 % (1818853)------------------------------ % 218.63/31.09 % (1818853)------------------------------ % 218.63/31.09 % (1818855)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2003292733:i=14071_2944 on theBenchmark for (2944ds/14071Mi) % 218.63/31.09 % (1818855)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 218.63/31.09 % (1818855)Terminated due to inappropriate strategy. % 218.63/31.09 % (1818855)------------------------------ % 218.63/31.09 % (1818855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.63/31.09 % (1818855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.63/31.09 % (1818855)CaDiCaL version: 2.1.3 % 218.63/31.09 % (1818855)Termination reason: Inappropriate % 218.63/31.09 % (1818855)Time elapsed: 0.066 s % 218.63/31.09 % (1818855)Peak memory usage: 12 MB % 218.63/31.09 % (1818855)Instructions burned: 74 (million) % 218.63/31.09 % (1818855)------------------------------ % 218.63/31.09 % (1818855)------------------------------ % 218.63/31.09 % (1818857)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3471664848:i=22565:add=on:rawr=on_2943 on theBenchmark for (2943ds/22565Mi) % 218.63/31.09 % (1818812)Instruction limit reached! % 218.63/31.09 % (1818812)------------------------------ % 218.63/31.09 % (1818812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 218.63/31.09 % (1818812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.63/31.09 % (1818812)CaDiCaL version: 2.1.3 % 218.63/31.09 % (1818812)Termination reason: Instruction limit % 218.63/31.09 % (1818812)Termination phase: Saturation % 218.63/31.09 % (1818812)Time elapsed: 4.894 s % 218.63/31.09 % (1818812)Peak memory usage: 53 MB % 218.63/31.09 % (1818812)Instructions burned: 5114 (million) % 218.63/31.09 % (1818859)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1218160360:i=8173:av=off_2939 on theBenchmark for (2939ds/8173Mi) % 221.68/31.51 % (1818835)Instruction limit reached! % 221.68/31.51 % (1818835)------------------------------ % 221.68/31.51 % (1818835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.68/31.51 % (1818835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.68/31.51 % (1818835)CaDiCaL version: 2.1.3 % 221.68/31.51 % (1818835)Termination reason: Instruction limit % 221.68/31.51 % (1818835)Termination phase: Saturation % 221.68/31.51 % (1818835)Time elapsed: 4.292 s % 221.68/31.51 % (1818835)Peak memory usage: 44 MB % 221.68/31.51 % (1818835)Instructions burned: 4592 (million) % 221.68/31.51 % (1818863)dis+10_16:1_sil=16000:random_seed=1182448899:i=9155:fsr=off_2911 on theBenchmark for (2911ds/9155Mi) % 221.68/31.51 % (1818849)Instruction limit reached! % 221.68/31.51 % (1818849)------------------------------ % 221.68/31.51 % (1818849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.68/31.51 % (1818849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.68/31.51 % (1818849)CaDiCaL version: 2.1.3 % 221.68/31.51 % (1818849)Termination reason: Instruction limit % 221.68/31.51 % (1818849)Termination phase: Saturation % 221.68/31.51 % (1818849)Time elapsed: 4.789 s % 221.68/31.51 % (1818849)Peak memory usage: 47 MB % 221.68/31.51 % (1818849)Instructions burned: 5212 (million) % 221.68/31.51 % (1818867)ott-3_8_sil=64000:random_seed=411827860:i=20139:bs=on_2899 on theBenchmark for (2899ds/20139Mi) % 221.68/31.51 % (1818859)Instruction limit reached! % 221.68/31.51 % (1818859)------------------------------ % 221.68/31.51 % (1818859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.68/31.51 % (1818859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.68/31.51 % (1818859)CaDiCaL version: 2.1.3 % 221.68/31.51 % (1818859)Termination reason: Instruction limit % 221.68/31.51 % (1818859)Termination phase: Saturation % 221.68/31.51 % (1818859)Time elapsed: 7.822 s % 221.68/31.51 % (1818859)Peak memory usage: 73 MB % 221.68/31.51 % (1818859)Instructions burned: 8174 (million) % 221.68/31.51 % (1818873)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1349636112:fmbsr=2:i=32576_2861 on theBenchmark for (2861ds/32576Mi) % 221.68/31.51 % (1818873)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 221.68/31.51 % (1818873)Terminated due to inappropriate strategy. % 221.68/31.51 % (1818873)------------------------------ % 221.68/31.51 % (1818873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.68/31.51 % (1818873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.68/31.51 % (1818873)CaDiCaL version: 2.1.3 % 221.68/31.51 % (1818873)Termination reason: Inappropriate % 221.68/31.51 % (1818873)Time elapsed: 0.044 s % 221.68/31.51 % (1818873)Peak memory usage: 12 MB % 221.68/31.51 % (1818873)Instructions burned: 75 (million) % 221.68/31.51 % (1818873)------------------------------ % 221.68/31.51 % (1818873)------------------------------ % 221.68/31.51 % (1818875)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2426158174:i=11404_2860 on theBenchmark for (2860ds/11404Mi) % 221.68/31.51 % (1818863)Instruction limit reached! % 221.68/31.51 % (1818863)------------------------------ % 221.68/31.51 % (1818863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.68/31.51 % (1818863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.68/31.51 % (1818863)CaDiCaL version: 2.1.3 % 221.68/31.51 % (1818863)Termination reason: Instruction limit % 221.68/31.51 % (1818863)Termination phase: Saturation % 221.68/31.51 % (1818863)Time elapsed: 8.282 s % 221.68/31.51 % (1818863)Peak memory usage: 59 MB % 221.68/31.51 % (1818863)Instructions burned: 9155 (million) % 221.68/31.51 % (1818877)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3416661091:i=14134_2828 on theBenchmark for (2828ds/14134Mi) % 221.68/31.51 % (1818857)Instruction limit reached! % 221.68/31.51 % (1818857)------------------------------ % 221.68/31.51 % (1818857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.68/31.51 % (1818857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.68/31.51 % (1818857)CaDiCaL version: 2.1.3 % 221.68/31.51 % (1818857)Termination reason: Instruction limit % 221.68/31.51 % (1818857)Termination phase: Saturation % 221.68/31.51 % (1818857)Time elapsed: 16.695 s % 221.68/31.51 % (1818857)Peak memory usage: 56 MB % 221.68/31.51 % (1818857)Instructions burned: 22565 (million) % 221.68/31.51 % (1818883)dis+33_16_sil=32000:sac=on:random_seed=3442052138:i=15851:nm=0_2776 on theBenchmark for (2776ds/15851Mi) % 221.68/31.51 % (1818875)Instruction limit reached! % 221.68/31.51 % (1818875)------------------------------ % 221.68/31.51 % (1818875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.28/36.81 % (1818875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.28/36.81 % (1818875)CaDiCaL version: 2.1.3 % 259.28/36.81 % (1818875)Termination reason: Instruction limit % 259.28/36.81 % (1818875)Termination phase: Saturation % 259.28/36.81 % (1818875)Time elapsed: 10.797 s % 259.28/36.81 % (1818875)Peak memory usage: 96 MB % 259.28/36.81 % (1818875)Instructions burned: 11404 (million) % 259.28/36.81 % (1818887)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1757477183:avsq=on:i=17627:add=on:amm=off_2751 on theBenchmark for (2751ds/17627Mi) % 259.28/36.81 % (1818867)Instruction limit reached! % 259.28/36.81 % (1818867)------------------------------ % 259.28/36.81 % (1818867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.28/36.81 % (1818867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.28/36.81 % (1818867)CaDiCaL version: 2.1.3 % 259.28/36.81 % (1818867)Termination reason: Instruction limit % 259.28/36.81 % (1818867)Termination phase: Saturation % 259.28/36.81 % (1818867)Time elapsed: 16.686 s % 259.28/36.81 % (1818867)Peak memory usage: 61 MB % 259.28/36.81 % (1818867)Instructions burned: 20139 (million) % 259.28/36.81 % (1818893)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4289696333:s2a=on:i=53295_2731 on theBenchmark for (2731ds/53295Mi) % 259.28/36.81 % (1818839)Instruction limit reached! % 259.28/36.81 % (1818839)------------------------------ % 259.28/36.81 % (1818839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.28/36.81 % (1818839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.28/36.81 % (1818839)CaDiCaL version: 2.1.3 % 259.28/36.81 % (1818839)Termination reason: Instruction limit % 259.28/36.81 % (1818839)Termination phase: Saturation % 259.28/36.81 % (1818839)Time elapsed: 24.167 s % 259.28/36.81 % (1818839)Peak memory usage: 50 MB % 259.28/36.81 % (1818839)Instructions burned: 29341 (million) % 259.28/36.81 % (1818911)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1942003214:i=26857:ins=20_2712 on theBenchmark for (2712ds/26857Mi) % 259.28/36.81 % (1818911)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.28/36.81 % (1818911)Terminated due to inappropriate strategy. % 259.28/36.81 % (1818911)------------------------------ % 259.28/36.81 % (1818911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.28/36.81 % (1818911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.28/36.81 % (1818911)CaDiCaL version: 2.1.3 % 259.28/36.81 % (1818911)Termination reason: Inappropriate % 259.28/36.81 % (1818911)Time elapsed: 0.043 s % 259.28/36.81 % (1818911)Peak memory usage: 12 MB % 259.28/36.81 % (1818911)Instructions burned: 74 (million) % 259.28/36.81 % (1818911)------------------------------ % 259.28/36.81 % (1818911)------------------------------ % 259.28/36.81 % (1818913)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=421472763:i=28120:bs=on:fsr=off_2711 on theBenchmark for (2711ds/28120Mi) % 259.28/36.81 % (1818877)Instruction limit reached! % 259.28/36.81 % (1818877)------------------------------ % 259.28/36.81 % (1818877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.28/36.81 % (1818877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.28/36.81 % (1818877)CaDiCaL version: 2.1.3 % 259.28/36.81 % (1818877)Termination reason: Instruction limit % 259.28/36.81 % (1818877)Termination phase: Saturation % 259.28/36.81 % (1818877)Time elapsed: 13.412 s % 259.28/36.81 % (1818877)Peak memory usage: 107 MB % 259.28/36.81 % (1818877)Instructions burned: 14134 (million) % 259.28/36.81 % (1818915)fmb+10_1_sil=256000:fmbss=7:random_seed=34319138:fmbsr=1.6:i=182295_2693 on theBenchmark for (2693ds/182295Mi) % 259.28/36.81 % (1818915)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 259.28/36.81 % (1818915)Terminated due to inappropriate strategy. % 259.28/36.81 % (1818915)------------------------------ % 259.28/36.81 % (1818915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 259.28/36.81 % (1818915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.28/36.81 % (1818915)CaDiCaL version: 2.1.3 % 259.28/36.81 % (1818915)Termination reason: Inappropriate % 259.28/36.81 % (1818915)Time elapsed: 0.068 s % 259.28/36.81 % (1818915)Peak memory usage: 12 MB % 259.28/36.81 % (1818915)Instructions burned: 74 (million) % 259.28/36.81 % (1818915)------------------------------ % 259.28/36.81 % (1818915)------------------------------ % 259.28/36.81 % (1818917)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=521969887:i=44625:gsp=on_2692 on theBenchmark for (2692ds/44625Mi) % 279.85/39.79 % (1818917)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.85/39.79 % (1818917)Terminated due to inappropriate strategy. % 279.85/39.79 % (1818917)------------------------------ % 279.85/39.79 % (1818917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.85/39.79 % (1818917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.85/39.79 % (1818917)CaDiCaL version: 2.1.3 % 279.85/39.79 % (1818917)Termination reason: Inappropriate % 279.85/39.79 % (1818917)Time elapsed: 0.069 s % 279.85/39.79 % (1818917)Peak memory usage: 12 MB % 279.85/39.79 % (1818917)Instructions burned: 80 (million) % 279.85/39.79 % (1818917)------------------------------ % 279.85/39.79 % (1818917)------------------------------ % 279.85/39.79 % (1818919)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1719529915:i=160505_2691 on theBenchmark for (2691ds/160505Mi) % 279.85/39.79 % (1818919)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.85/39.79 % (1818919)Terminated due to inappropriate strategy. % 279.85/39.79 % (1818919)------------------------------ % 279.85/39.79 % (1818919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.85/39.79 % (1818919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.85/39.79 % (1818919)CaDiCaL version: 2.1.3 % 279.85/39.79 % (1818919)Termination reason: Inappropriate % 279.85/39.79 % (1818919)Time elapsed: 0.043 s % 279.85/39.79 % (1818919)Peak memory usage: 12 MB % 279.85/39.79 % (1818919)Instructions burned: 74 (million) % 279.85/39.79 % (1818919)------------------------------ % 279.85/39.79 % (1818919)------------------------------ % 279.85/39.79 % (1818921)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=348593116:fmbsr=1.3:i=225729_2690 on theBenchmark for (2690ds/225729Mi) % 279.85/39.79 % (1818921)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.85/39.79 % (1818921)Terminated due to inappropriate strategy. % 279.85/39.79 % (1818921)------------------------------ % 279.85/39.79 % (1818921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.85/39.79 % (1818921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.85/39.79 % (1818921)CaDiCaL version: 2.1.3 % 279.85/39.79 % (1818921)Termination reason: Inappropriate % 279.85/39.79 % (1818921)Time elapsed: 0.039 s % 279.85/39.79 % (1818921)Peak memory usage: 12 MB % 279.85/39.79 % (1818921)Instructions burned: 74 (million) % 279.85/39.79 % (1818921)------------------------------ % 279.85/39.79 % (1818921)------------------------------ % 279.85/39.79 % (1818923)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=502160127:fmbsr=2:i=185024:ins=7_2690 on theBenchmark for (2690ds/185024Mi) % 279.85/39.79 % (1818923)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.85/39.79 % (1818923)Terminated due to inappropriate strategy. % 279.85/39.79 % (1818923)------------------------------ % 279.85/39.79 % (1818923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.85/39.79 % (1818923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.85/39.79 % (1818923)CaDiCaL version: 2.1.3 % 279.85/39.79 % (1818923)Termination reason: Inappropriate % 279.85/39.79 % (1818923)Time elapsed: 0.039 s % 279.85/39.79 % (1818923)Peak memory usage: 12 MB % 279.85/39.79 % (1818923)Instructions burned: 74 (million) % 279.85/39.79 % (1818923)------------------------------ % 279.85/39.79 % (1818923)------------------------------ % 279.85/39.79 % (1818925)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1412561064:rtra=on_2689 on theBenchmark for (2689ds/0Mi) % 279.85/39.79 % (1818925)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.85/39.79 % (1818925)Terminated due to inappropriate strategy. % 279.85/39.79 % (1818925)------------------------------ % 279.85/39.79 % (1818925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.85/39.79 % (1818925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.85/39.79 % (1818925)CaDiCaL version: 2.1.3 % 279.85/39.79 % (1818925)Termination reason: Inappropriate % 279.85/39.79 % (1818925)Time elapsed: 0.069 s % 279.85/39.79 % (1818925)Peak memory usage: 13 MB % 279.85/39.79 % (1818925)Instructions burned: 80 (million) % 279.85/39.79 % (1818925)------------------------------ % 279.85/39.79 % (1818925)------------------------------ % 279.85/39.79 % (1818927)% WARNING: option uhcvi not known. % 279.85/39.79 % (1818927)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1681573808:i=271062:add=off:rtra=on:rawr=on_2688 on theBenchmark for (2688ds/271062Mi) % 296.44/42.09 % (1818755)Instruction limit reached! % 296.44/42.09 % (1818755)------------------------------ % 296.44/42.09 % (1818755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.44/42.09 % (1818755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.44/42.09 % (1818755)CaDiCaL version: 2.1.3 % 296.44/42.09 % (1818755)Termination reason: Instruction limit % 296.44/42.09 % (1818755)Termination phase: Saturation % 296.44/42.09 % (1818755)Time elapsed: 33.662 s % 296.44/42.09 % (1818755)Peak memory usage: 245 MB % 296.44/42.09 % (1818755)Instructions burned: 88028 (million) % 296.44/42.09 % (1818929)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2521929088:i=176048:add=on:rtra=on:rawr=on_2662 on theBenchmark for (2662ds/176048Mi) % 296.44/42.09 % (1818883)Instruction limit reached! % 296.44/42.09 % (1818883)------------------------------ % 296.44/42.09 % (1818883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.44/42.09 % (1818883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.44/42.09 % (1818883)CaDiCaL version: 2.1.3 % 296.44/42.09 % (1818883)Termination reason: Instruction limit % 296.44/42.09 % (1818883)Termination phase: Saturation % 296.44/42.09 % (1818883)Time elapsed: 12.972 s % 296.44/42.09 % (1818883)Peak memory usage: 19 MB % 296.44/42.09 % (1818883)Instructions burned: 15852 (million) % 296.44/42.09 % (1818931)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3114992427:i=206:fgj=on:rtra=on_2646 on theBenchmark for (2646ds/206Mi) % 296.44/42.09 % (1818931)Instruction limit reached! % 296.44/42.09 % (1818931)------------------------------ % 296.44/42.09 % (1818931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.44/42.09 % (1818931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.44/42.09 % (1818931)CaDiCaL version: 2.1.3 % 296.44/42.09 % (1818931)Termination reason: Instruction limit % 296.44/42.09 % (1818931)Termination phase: Saturation % 296.44/42.09 % (1818931)Time elapsed: 0.178 s % 296.44/42.09 % (1818931)Peak memory usage: 15 MB % 296.44/42.09 % (1818931)Instructions burned: 206 (million) % 296.44/42.09 % (1818933)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2423173571:i=232:rtra=on_2644 on theBenchmark for (2644ds/232Mi) % 296.44/42.09 % (1818933)Instruction limit reached! % 296.44/42.09 % (1818933)------------------------------ % 296.44/42.09 % (1818933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.44/42.09 % (1818933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.44/42.09 % (1818933)CaDiCaL version: 2.1.3 % 296.44/42.09 % (1818933)Termination reason: Instruction limit % 296.44/42.09 % (1818933)Termination phase: Saturation % 296.44/42.09 % (1818933)Time elapsed: 0.205 s % 296.44/42.09 % (1818933)Peak memory usage: 15 MB % 296.44/42.09 % (1818933)Instructions burned: 233 (million) % 296.44/42.09 % (1818935)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3668845538:i=262:rtra=on_2641 on theBenchmark for (2641ds/262Mi) % 296.44/42.09 % (1818935)Instruction limit reached! % 296.44/42.09 % (1818935)------------------------------ % 296.44/42.09 % (1818935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.44/42.09 % (1818935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.44/42.09 % (1818935)CaDiCaL version: 2.1.3 % 296.44/42.09 % (1818935)Termination reason: Instruction limit % 296.44/42.09 % (1818935)Termination phase: Saturation % 296.44/42.09 % (1818935)Time elapsed: 0.207 s % 296.44/42.09 % (1818935)Peak memory usage: 16 MB % 296.44/42.09 % (1818935)Instructions burned: 262 (million) % 296.44/42.09 % (1818937)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=244067367:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2639 on theBenchmark for (2639ds/318Mi) % 296.44/42.09 % (1818937)Instruction limit reached! % 296.44/42.09 % (1818937)------------------------------ % 296.44/42.09 % (1818937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.44/42.09 % (1818937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.44/42.09 % (1818937)CaDiCaL version: 2.1.3 % 296.44/42.09 % (1818937)Termination reason: Instruction limit % 296.44/42.09 % (1818937)Termination phase: Saturation % 296.44/42.09 % (1818937)Time elapsed: 0.361 s % 296.44/42.09 % (1818937)Peak memory usage: 16 MB % 296.44/42.09 % (1818937)Instructions burned: 318 (million) % 296.44/42.09 % (1818939)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1994695951:i=1428:nm=2:rtra=on_2635 on theBenchmark for (2635ds/1428Mi) % 300.06/42.63 % (1818939)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.06/42.63 % (1818939)Terminated due to inappropriate strategy. % 300.06/42.63 % (1818939)------------------------------ % 300.06/42.63 % (1818939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.06/42.63 % (1818939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.06/42.63 % (1818939)CaDiCaL version: 2.1.3 % 300.06/42.63 % (1818939)Termination reason: Inappropriate % 300.06/42.63 % (1818939)Time elapsed: 0.073 s % 300.06/42.63 % (1818939)Peak memory usage: 13 MB % 300.06/42.63 % (1818939)Instructions burned: 79 (million) % 300.06/42.63 % (1818939)------------------------------ % 300.06/42.63 % (1818939)------------------------------ % 300.06/42.63 % (1818941)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1290466007:i=262:bd=preordered:rtra=on:fsd=on_2634 on theBenchmark for (2634ds/262Mi) % 300.06/42.63 % (1818941)Instruction limit reached! % 300.06/42.63 % (1818941)------------------------------ % 300.06/42.63 % (1818941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.06/42.63 % (1818941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.06/42.63 % (1818941)CaDiCaL version: 2.1.3 % 300.06/42.63 % (1818941)Termination reason: Instruction limit % 300.06/42.63 % (1818941)Termination phase: Saturation % 300.06/42.63 % (1818941)Time elapsed: 0.262 s % 300.06/42.63 % (1818941)Peak memory usage: 16 MB % 300.06/42.63 % (1818941)Instructions burned: 262 (million) % 300.06/42.63 % (1818943)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=1178863726:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2631 on theBenchmark for (2631ds/1368Mi) % 300.06/42.63 % (1818943)Instruction limit reached! % 300.06/42.63 % (1818943)------------------------------ % 300.06/42.63 % (1818943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.06/42.63 % (1818943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.06/42.63 % (1818943)CaDiCaL version: 2.1.3 % 300.06/42.63 % (1818943)Termination reason: Instruction limit % 300.06/42.63 % (1818943)Termination phase: Saturation % 300.06/42.63 % (1818943)Time elapsed: 1.210 s % 300.06/42.63 % (1818943)Peak memory usage: 21 MB % 300.06/42.63 % (1818943)Instructions burned: 1369 (million) % 300.06/42.63 % (1818947)ott-21_1_sil=16000:si=on:fs=off:random_seed=3671496113:i=360:av=off:fsr=off:rtra=on_2619 on theBenchmark for (2619ds/360Mi) % 300.06/42.63 % (1818947)Instruction limit reached! % 300.06/42.63 % (1818947)------------------------------ % 300.06/42.63 % (1818947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.06/42.63 % (1818947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.06/42.63 % (1818947)CaDiCaL version: 2.1.3 % 300.06/42.63 % (1818947)Termination reason: Instruction limit % 300.06/42.63 % (1818947)Termination phase: Saturation % 300.06/42.63 % (1818947)Time elapsed: 0.290 s % 300.06/42.63 % (1818947)Peak memory usage: 15 MB % 300.06/42.63 % (1818947)Instructions burned: 361 (million) % 300.06/42.63 % (1818951)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1982449992:i=954:bd=all:rtra=on_2615 on theBenchmark for (2615ds/954Mi) % 300.06/42.63 % (1818951)Instruction limit reached! % 300.06/42.63 % (1818951)------------------------------ % 300.06/42.63 % (1818951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.06/42.63 % (1818951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.06/42.63 % (1818951)CaDiCaL version: 2.1.3 % 300.06/42.63 % (1818951)Termination reason: Instruction limit % 300.06/42.63 % (1818951)Termination phase: Saturation % 300.06/42.63 % (1818951)Time elapsed: 0.960 s % 300.06/42.63 % (1818951)Peak memory usage: 19 MB % 300.06/42.63 % (1818951)Instructions burned: 954 (million) % 300.06/42.63 % (1818961)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2016080165:fmbsr=1.3:i=1730:ins=25:rtra=on_2606 on theBenchmark for (2606ds/1730Mi) % 300.06/42.63 % (1818961)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.06/42.63 % (1818961)Terminated due to inappropriate strategy. % 300.06/42.63 % (1818961)------------------------------ % 300.06/42.63 % (1818961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.06/42.63 % (1818961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.06/42.63 % (1818961)CaDiCaL version: 2.1.3 % 300.06/42.63 % (1818961)Termination rea % 300.06/42.63 Terminated % 300.06/42.63 % Vampire exiting % 300.06/42.64 Terminated %------------------------------------------------------------------------------