%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW623_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n007.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:32 PM UTC 2026 % Result : Timeout 300.17s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW623_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.23 % Computer : n007.cluster.edu % 0.11/0.23 % Model : x86_64 x86_64 % 0.11/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.23 % Memory : 8046.5625MB % 0.11/0.23 % OS : Linux 6.8.0-71-generic % 0.11/0.23 % CPULimit : 300 % 0.11/0.23 % WCLimit : 300 % 0.11/0.23 % DateTime : Mon Sep 28 14:20:56 UTC 2026 % 0.11/0.23 % CPUTime : % 0.11/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.28 Running first-order model finding % 0.11/0.28 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.32/1.22 % (2415102)Will run a generic schedule for satisfiability detection. % 6.32/1.22 % (2415109)% WARNING: option uhcvi not known. % 6.32/1.22 % (2415109)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2224329825:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.32/1.22 % (2415114)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=362982216:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.32/1.22 % (2415111)dis+10_1_sil=32000:sp=arity:random_seed=2762096863:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.32/1.22 % (2415112)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=900576109:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.32/1.22 % (2415110)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3274021485:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.32/1.22 % (2415108)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3147699313_2999 on theBenchmark for (2999ds/0Mi) % 6.32/1.22 % (2415113)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2441777604:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.32/1.22 % (2415108)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.32/1.22 % (2415108)Terminated due to inappropriate strategy. % 6.32/1.22 % (2415108)------------------------------ % 6.32/1.22 % (2415108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.32/1.22 % (2415108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.22 % (2415108)CaDiCaL version: 2.1.3 % 6.32/1.22 % (2415108)Termination reason: Inappropriate % 6.32/1.22 % (2415108)Time elapsed: 0.013 s % 6.32/1.22 % (2415108)Peak memory usage: 11 MB % 6.32/1.22 % (2415108)Instructions burned: 13 (million) % 6.32/1.22 % (2415108)------------------------------ % 6.32/1.22 % (2415108)------------------------------ % 6.32/1.22 % (2415124)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3725338893:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.32/1.22 % (2415124)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.32/1.22 % (2415124)Terminated due to inappropriate strategy. % 6.32/1.22 % (2415124)------------------------------ % 6.32/1.22 % (2415124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.32/1.22 % (2415124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.22 % (2415124)CaDiCaL version: 2.1.3 % 6.32/1.22 % (2415124)Termination reason: Inappropriate % 6.32/1.22 % (2415124)Time elapsed: 0.006 s % 6.32/1.22 % (2415124)Peak memory usage: 11 MB % 6.32/1.22 % (2415124)Instructions burned: 11 (million) % 6.32/1.22 % (2415124)------------------------------ % 6.32/1.22 % (2415124)------------------------------ % 6.32/1.22 % (2415111)Instruction limit reached! % 6.32/1.22 % (2415111)------------------------------ % 6.32/1.22 % (2415111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.32/1.22 % (2415111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.22 % (2415111)CaDiCaL version: 2.1.3 % 6.32/1.22 % (2415111)Termination reason: Instruction limit % 6.32/1.22 % (2415111)Termination phase: Saturation % 6.32/1.22 % (2415111)Time elapsed: 0.092 s % 6.32/1.22 % (2415111)Peak memory usage: 13 MB % 6.32/1.22 % (2415111)Instructions burned: 103 (million) % 6.32/1.22 % (2415112)Instruction limit reached! % 6.32/1.22 % (2415112)------------------------------ % 6.32/1.22 % (2415112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.32/1.22 % (2415112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.22 % (2415112)CaDiCaL version: 2.1.3 % 6.32/1.22 % (2415112)Termination reason: Instruction limit % 6.32/1.22 % (2415112)Termination phase: Saturation % 6.32/1.22 % (2415112)Time elapsed: 0.107 s % 6.32/1.22 % (2415112)Peak memory usage: 13 MB % 6.32/1.22 % (2415112)Instructions burned: 117 (million) % 6.32/1.22 % (2415126)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1691978816:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 6.32/1.22 % (2415114)Instruction limit reached! % 6.32/1.22 % (2415114)------------------------------ % 6.32/1.22 % (2415114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.32/1.22 % (2415114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.32/1.22 % (2415114)CaDiCaL version: 2.1.3 % 6.32/1.22 % (2415114)Termination reason: Instruction limit % 7.14/1.47 % (2415114)Termination phase: Saturation % 7.14/1.47 % (2415114)Time elapsed: 0.121 s % 7.14/1.47 % (2415114)Peak memory usage: 14 MB % 7.14/1.47 % (2415114)Instructions burned: 159 (million) % 7.14/1.47 % (2415128)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=2907947066:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.14/1.47 % (2415131)ott-21_1_sil=16000:fs=off:random_seed=1302048181:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.14/1.47 % (2415133)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3253265842:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.14/1.47 % (2415113)Instruction limit reached! % 7.14/1.47 % (2415113)------------------------------ % 7.14/1.47 % (2415113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.14/1.47 % (2415113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.14/1.47 % (2415113)CaDiCaL version: 2.1.3 % 7.14/1.47 % (2415113)Termination reason: Instruction limit % 7.14/1.47 % (2415113)Termination phase: Saturation % 7.14/1.47 % (2415113)Time elapsed: 0.134 s % 7.14/1.47 % (2415113)Peak memory usage: 13 MB % 7.14/1.47 % (2415113)Instructions burned: 131 (million) % 7.14/1.47 % (2415141)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3512369747:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 7.14/1.47 % (2415141)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.14/1.47 % (2415141)Terminated due to inappropriate strategy. % 7.14/1.47 % (2415141)------------------------------ % 7.14/1.47 % (2415141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.14/1.47 % (2415141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.14/1.47 % (2415141)CaDiCaL version: 2.1.3 % 7.14/1.47 % (2415141)Termination reason: Inappropriate % 7.14/1.47 % (2415141)Time elapsed: 0.009 s % 7.14/1.47 % (2415141)Peak memory usage: 10 MB % 7.14/1.47 % (2415141)Instructions burned: 12 (million) % 7.14/1.47 % (2415141)------------------------------ % 7.14/1.47 % (2415141)------------------------------ % 7.14/1.47 % (2415126)Instruction limit reached! % 7.14/1.47 % (2415126)------------------------------ % 7.14/1.47 % (2415126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.14/1.47 % (2415126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.14/1.47 % (2415126)CaDiCaL version: 2.1.3 % 7.14/1.47 % (2415126)Termination reason: Instruction limit % 7.14/1.47 % (2415126)Termination phase: Saturation % 7.14/1.47 % (2415126)Time elapsed: 0.138 s % 7.14/1.47 % (2415126)Peak memory usage: 13 MB % 7.14/1.47 % (2415126)Instructions burned: 131 (million) % 7.14/1.47 % (2415131)Instruction limit reached! % 7.14/1.47 % (2415131)------------------------------ % 7.14/1.47 % (2415131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.14/1.47 % (2415131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.14/1.47 % (2415131)CaDiCaL version: 2.1.3 % 7.14/1.47 % (2415131)Termination reason: Instruction limit % 7.14/1.47 % (2415131)Termination phase: Saturation % 7.14/1.47 % (2415131)Time elapsed: 0.115 s % 7.14/1.47 % (2415131)Peak memory usage: 13 MB % 7.14/1.47 % (2415131)Instructions burned: 181 (million) % 7.14/1.47 % (2415144)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3980420122:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 7.14/1.47 % (2415147)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3562697504:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.14/1.47 % (2415148)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=2317932955: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) % 7.14/1.47 % (2415147)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.14/1.47 % (2415147)Terminated due to inappropriate strategy. % 7.14/1.47 % (2415147)------------------------------ % 7.14/1.47 % (2415147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.14/1.47 % (2415147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.14/1.47 % (2415147)CaDiCaL version: 2.1.3 % 7.14/1.47 % (2415147)Termination reason: Inappropriate % 7.14/1.47 % (2415147)Time elapsed: 0.011 s % 7.14/1.47 % (2415147)Peak memory usage: 10 MB % 23.47/3.71 % (2415147)Instructions burned: 11 (million) % 23.47/3.71 % (2415147)------------------------------ % 23.47/3.71 % (2415147)------------------------------ % 23.47/3.71 % (2415153)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=399247204:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 23.47/3.71 % (2415133)Instruction limit reached! % 23.47/3.71 % (2415133)------------------------------ % 23.47/3.71 % (2415133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.47/3.71 % (2415133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.47/3.71 % (2415133)CaDiCaL version: 2.1.3 % 23.47/3.71 % (2415133)Termination reason: Instruction limit % 23.47/3.71 % (2415133)Termination phase: Saturation % 23.47/3.71 % (2415133)Time elapsed: 0.486 s % 23.47/3.71 % (2415133)Peak memory usage: 14 MB % 23.47/3.71 % (2415133)Instructions burned: 477 (million) % 23.47/3.71 % (2415171)fmb+10_1_sil=64000:random_seed=2213712939:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 23.47/3.71 % (2415171)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.47/3.71 % (2415171)Terminated due to inappropriate strategy. % 23.47/3.71 % (2415171)------------------------------ % 23.47/3.71 % (2415171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.47/3.71 % (2415171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.47/3.71 % (2415171)CaDiCaL version: 2.1.3 % 23.47/3.71 % (2415171)Termination reason: Inappropriate % 23.47/3.71 % (2415171)Time elapsed: 0.014 s % 23.47/3.71 % (2415171)Peak memory usage: 11 MB % 23.47/3.71 % (2415171)Instructions burned: 12 (million) % 23.47/3.71 % (2415171)------------------------------ % 23.47/3.71 % (2415171)------------------------------ % 23.47/3.71 % (2415176)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1113722983:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 23.47/3.71 % (2415128)Instruction limit reached! % 23.47/3.71 % (2415128)------------------------------ % 23.47/3.71 % (2415128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.47/3.71 % (2415128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.47/3.71 % (2415128)CaDiCaL version: 2.1.3 % 23.47/3.71 % (2415128)Termination reason: Instruction limit % 23.47/3.71 % (2415128)Termination phase: Saturation % 23.47/3.71 % (2415128)Time elapsed: 0.612 s % 23.47/3.71 % (2415128)Peak memory usage: 17 MB % 23.47/3.71 % (2415128)Instructions burned: 684 (million) % 23.47/3.71 % (2415176)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.47/3.71 % (2415176)Terminated due to inappropriate strategy. % 23.47/3.71 % (2415176)------------------------------ % 23.47/3.71 % (2415176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.47/3.71 % (2415176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.47/3.71 % (2415176)CaDiCaL version: 2.1.3 % 23.47/3.71 % (2415176)Termination reason: Inappropriate % 23.47/3.71 % (2415176)Time elapsed: 0.012 s % 23.47/3.71 % (2415176)Peak memory usage: 11 MB % 23.47/3.71 % (2415176)Instructions burned: 11 (million) % 23.47/3.71 % (2415176)------------------------------ % 23.47/3.71 % (2415176)------------------------------ % 23.47/3.71 % (2415179)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3580413730:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 23.47/3.71 % (2415180)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2922604277:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 23.47/3.71 % (2415179)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.47/3.71 % (2415179)Terminated due to inappropriate strategy. % 23.47/3.71 % (2415179)------------------------------ % 23.47/3.71 % (2415179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.47/3.71 % (2415179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.47/3.71 % (2415179)CaDiCaL version: 2.1.3 % 23.47/3.71 % (2415179)Termination reason: Inappropriate % 23.47/3.71 % (2415179)Time elapsed: 0.010 s % 23.47/3.71 % (2415179)Peak memory usage: 11 MB % 23.47/3.71 % (2415179)Instructions burned: 11 (million) % 23.47/3.71 % (2415179)------------------------------ % 23.47/3.71 % (2415179)------------------------------ % 23.47/3.71 % (2415185)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3363745638:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 23.47/3.71 % (2415148)Instruction limit reached! % 23.47/3.71 % (2415148)------------------------------ % 28.23/4.30 % (2415148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.23/4.30 % (2415148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.23/4.30 % (2415148)CaDiCaL version: 2.1.3 % 28.23/4.30 % (2415148)Termination reason: Instruction limit % 28.23/4.30 % (2415148)Termination phase: Saturation % 28.23/4.30 % (2415148)Time elapsed: 0.608 s % 28.23/4.30 % (2415148)Peak memory usage: 21 MB % 28.23/4.30 % (2415148)Instructions burned: 693 (million) % 28.23/4.30 % (2415190)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3838392178:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 28.23/4.30 % (2415190)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.23/4.30 % (2415190)Terminated due to inappropriate strategy. % 28.23/4.30 % (2415190)------------------------------ % 28.23/4.30 % (2415190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.23/4.30 % (2415190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.23/4.30 % (2415190)CaDiCaL version: 2.1.3 % 28.23/4.30 % (2415190)Termination reason: Inappropriate % 28.23/4.30 % (2415190)Time elapsed: 0.007 s % 28.23/4.30 % (2415190)Peak memory usage: 11 MB % 28.23/4.30 % (2415190)Instructions burned: 13 (million) % 28.23/4.30 % (2415190)------------------------------ % 28.23/4.30 % (2415190)------------------------------ % 28.23/4.30 % (2415192)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1341037002:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 28.23/4.30 % (2415192)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.23/4.30 % (2415192)Terminated due to inappropriate strategy. % 28.23/4.30 % (2415192)------------------------------ % 28.23/4.30 % (2415192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.23/4.30 % (2415192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.23/4.30 % (2415192)CaDiCaL version: 2.1.3 % 28.23/4.30 % (2415192)Termination reason: Inappropriate % 28.23/4.30 % (2415192)Time elapsed: 0.006 s % 28.23/4.30 % (2415192)Peak memory usage: 11 MB % 28.23/4.30 % (2415192)Instructions burned: 11 (million) % 28.23/4.30 % (2415192)------------------------------ % 28.23/4.30 % (2415192)------------------------------ % 28.23/4.30 % (2415194)ott-2_1_sil=16000:newcnf=on:random_seed=2954676162:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 28.23/4.30 % (2415153)Instruction limit reached! % 28.23/4.30 % (2415153)------------------------------ % 28.23/4.30 % (2415153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.23/4.30 % (2415153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.23/4.30 % (2415153)CaDiCaL version: 2.1.3 % 28.23/4.30 % (2415153)Termination reason: Instruction limit % 28.23/4.30 % (2415153)Termination phase: Saturation % 28.23/4.30 % (2415153)Time elapsed: 0.675 s % 28.23/4.30 % (2415153)Peak memory usage: 19 MB % 28.23/4.30 % (2415153)Instructions burned: 880 (million) % 28.23/4.30 % (2415196)ott+10_1_sil=32000:tgt=ground:random_seed=3547399585:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 28.23/4.30 % (2415144)Instruction limit reached! % 28.23/4.30 % (2415144)------------------------------ % 28.23/4.30 % (2415144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.23/4.30 % (2415144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.23/4.30 % (2415144)CaDiCaL version: 2.1.3 % 28.23/4.30 % (2415144)Termination reason: Instruction limit % 28.23/4.30 % (2415144)Termination phase: Saturation % 28.23/4.30 % (2415144)Time elapsed: 0.865 s % 28.23/4.30 % (2415144)Peak memory usage: 21 MB % 28.23/4.30 % (2415144)Instructions burned: 1179 (million) % 28.23/4.30 % (2415198)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1311706182:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 28.23/4.30 % (2415198)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.23/4.30 % (2415198)Terminated due to inappropriate strategy. % 28.23/4.30 % (2415198)------------------------------ % 28.23/4.30 % (2415198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.23/4.30 % (2415198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.23/4.30 % (2415198)CaDiCaL version: 2.1.3 % 28.23/4.30 % (2415198)Termination reason: Inappropriate % 28.23/4.30 % (2415198)Time elapsed: 0.007 s % 28.23/4.30 % (2415198)Peak memory usage: 11 MB % 28.23/4.30 % (2415198)Instructions burned: 13 (million) % 133.30/19.06 % (2415198)------------------------------ % 133.30/19.06 % (2415198)------------------------------ % 133.30/19.06 % (2415200)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3879936301:i=3512:aac=none_2988 on theBenchmark for (2988ds/3512Mi) % 133.30/19.06 % (2415194)Instruction limit reached! % 133.30/19.06 % (2415194)------------------------------ % 133.30/19.06 % (2415194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.30/19.06 % (2415194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.30/19.06 % (2415194)CaDiCaL version: 2.1.3 % 133.30/19.06 % (2415194)Termination reason: Instruction limit % 133.30/19.06 % (2415194)Termination phase: Saturation % 133.30/19.06 % (2415194)Time elapsed: 0.344 s % 133.30/19.06 % (2415194)Peak memory usage: 14 MB % 133.30/19.06 % (2415194)Instructions burned: 870 (million) % 133.30/19.06 % (2415203)dis+21_1_sil=32000:sas=cadical:random_seed=4083183133:i=3773:amm=off_2986 on theBenchmark for (2986ds/3773Mi) % 133.30/19.06 % (2415185)Instruction limit reached! % 133.30/19.06 % (2415185)------------------------------ % 133.30/19.06 % (2415185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.30/19.06 % (2415185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.30/19.06 % (2415185)CaDiCaL version: 2.1.3 % 133.30/19.06 % (2415185)Termination reason: Instruction limit % 133.30/19.06 % (2415185)Termination phase: Saturation % 133.30/19.06 % (2415185)Time elapsed: 0.804 s % 133.30/19.06 % (2415185)Peak memory usage: 31 MB % 133.30/19.06 % (2415185)Instructions burned: 1472 (million) % 133.30/19.06 % (2415288)ott+11_1_sil=16000:gs=on:random_seed=3440740513:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2983 on theBenchmark for (2983ds/2251Mi) % 133.30/19.06 % (2415288)Instruction limit reached! % 133.30/19.06 % (2415288)------------------------------ % 133.30/19.06 % (2415288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.30/19.06 % (2415288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.30/19.06 % (2415288)CaDiCaL version: 2.1.3 % 133.30/19.06 % (2415288)Termination reason: Instruction limit % 133.30/19.06 % (2415288)Termination phase: Saturation % 133.30/19.06 % (2415288)Time elapsed: 1.184 s % 133.30/19.06 % (2415288)Peak memory usage: 20 MB % 133.30/19.06 % (2415288)Instructions burned: 2251 (million) % 133.30/19.06 % (2415359)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3939104041:fmbsr=1.6:i=67534_2971 on theBenchmark for (2971ds/67534Mi) % 133.30/19.06 % (2415359)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 133.30/19.06 % (2415359)Terminated due to inappropriate strategy. % 133.30/19.06 % (2415359)------------------------------ % 133.30/19.06 % (2415359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.30/19.06 % (2415359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.30/19.06 % (2415359)CaDiCaL version: 2.1.3 % 133.30/19.06 % (2415359)Termination reason: Inappropriate % 133.30/19.06 % (2415359)Time elapsed: 0.006 s % 133.30/19.06 % (2415359)Peak memory usage: 11 MB % 133.30/19.06 % (2415359)Instructions burned: 11 (million) % 133.30/19.06 % (2415359)------------------------------ % 133.30/19.06 % (2415359)------------------------------ % 133.30/19.06 % (2415361)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2143666797:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2971 on theBenchmark for (2971ds/4591Mi) % 133.30/19.06 % (2415200)Instruction limit reached! % 133.30/19.06 % (2415200)------------------------------ % 133.30/19.06 % (2415200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.30/19.06 % (2415200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.30/19.06 % (2415200)CaDiCaL version: 2.1.3 % 133.30/19.06 % (2415200)Termination reason: Instruction limit % 133.30/19.06 % (2415200)Termination phase: Saturation % 133.30/19.06 % (2415200)Time elapsed: 1.924 s % 133.30/19.06 % (2415200)Peak memory usage: 34 MB % 133.30/19.06 % (2415200)Instructions burned: 3512 (million) % 133.30/19.06 % (2415363)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4292517440:i=29340_2968 on theBenchmark for (2968ds/29340Mi) % 133.30/19.06 % (2415203)Instruction limit reached! % 133.30/19.06 % (2415203)------------------------------ % 133.30/19.06 % (2415203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.30/19.06 % (2415203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.30/19.06 % (2415203)CaDiCaL version: 2.1.3 % 133.30/19.06 % (2415203)Termination reason: Instruction limit % 166.46/23.70 % (2415203)Termination phase: Saturation % 166.46/23.70 % (2415203)Time elapsed: 2.055 s % 166.46/23.70 % (2415203)Peak memory usage: 33 MB % 166.46/23.70 % (2415203)Instructions burned: 3774 (million) % 166.46/23.70 % (2415365)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1528630647:i=5211_2965 on theBenchmark for (2965ds/5211Mi) % 166.46/23.70 % (2415180)Instruction limit reached! % 166.46/23.70 % (2415180)------------------------------ % 166.46/23.70 % (2415180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.46/23.70 % (2415180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.46/23.70 % (2415180)CaDiCaL version: 2.1.3 % 166.46/23.70 % (2415180)Termination reason: Instruction limit % 166.46/23.70 % (2415180)Termination phase: Saturation % 166.46/23.70 % (2415180)Time elapsed: 2.821 s % 166.46/23.70 % (2415180)Peak memory usage: 43 MB % 166.46/23.70 % (2415180)Instructions burned: 5131 (million) % 166.46/23.70 % (2415367)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4119167055:i=5497:nm=2_2963 on theBenchmark for (2963ds/5497Mi) % 166.46/23.70 % (2415367)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 166.46/23.70 % (2415367)Terminated due to inappropriate strategy. % 166.46/23.70 % (2415367)------------------------------ % 166.46/23.70 % (2415367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.46/23.70 % (2415367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.46/23.70 % (2415367)CaDiCaL version: 2.1.3 % 166.46/23.70 % (2415367)Termination reason: Inappropriate % 166.46/23.70 % (2415367)Time elapsed: 0.007 s % 166.46/23.70 % (2415367)Peak memory usage: 11 MB % 166.46/23.70 % (2415367)Instructions burned: 12 (million) % 166.46/23.70 % (2415367)------------------------------ % 166.46/23.70 % (2415367)------------------------------ % 166.46/23.70 % (2415369)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1533965018:fmbsr=2:i=46332_2963 on theBenchmark for (2963ds/46332Mi) % 166.46/23.70 % (2415369)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 166.46/23.70 % (2415369)Terminated due to inappropriate strategy. % 166.46/23.70 % (2415369)------------------------------ % 166.46/23.70 % (2415369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.46/23.70 % (2415369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.46/23.70 % (2415369)CaDiCaL version: 2.1.3 % 166.46/23.70 % (2415369)Termination reason: Inappropriate % 166.46/23.70 % (2415369)Time elapsed: 0.006 s % 166.46/23.70 % (2415369)Peak memory usage: 11 MB % 166.46/23.70 % (2415369)Instructions burned: 11 (million) % 166.46/23.70 % (2415369)------------------------------ % 166.46/23.70 % (2415369)------------------------------ % 166.46/23.70 % (2415371)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3582128501:i=14071_2963 on theBenchmark for (2963ds/14071Mi) % 166.46/23.70 % (2415371)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 166.46/23.70 % (2415371)Terminated due to inappropriate strategy. % 166.46/23.70 % (2415371)------------------------------ % 166.46/23.70 % (2415371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.46/23.70 % (2415371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.46/23.70 % (2415371)CaDiCaL version: 2.1.3 % 166.46/23.70 % (2415371)Termination reason: Inappropriate % 166.46/23.70 % (2415371)Time elapsed: 0.006 s % 166.46/23.70 % (2415371)Peak memory usage: 11 MB % 166.46/23.70 % (2415371)Instructions burned: 11 (million) % 166.46/23.70 % (2415371)------------------------------ % 166.46/23.70 % (2415371)------------------------------ % 166.46/23.70 % (2415373)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=803193256:i=22565:add=on:rawr=on_2962 on theBenchmark for (2962ds/22565Mi) % 166.46/23.70 % (2415196)Instruction limit reached! % 166.46/23.70 % (2415196)------------------------------ % 166.46/23.70 % (2415196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.46/23.70 % (2415196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.46/23.70 % (2415196)CaDiCaL version: 2.1.3 % 166.46/23.70 % (2415196)Termination reason: Instruction limit % 166.46/23.70 % (2415196)Termination phase: Saturation % 166.46/23.70 % (2415196)Time elapsed: 2.927 s % 166.46/23.70 % (2415196)Peak memory usage: 43 MB % 166.46/23.70 % (2415196)Instructions burned: 5115 (million) % 166.46/23.70 % (2415375)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3604871949:i=8173:av=off_2960 on theBenchmark for (2960ds/8173Mi) % 167.23/23.86 % (2415361)Instruction limit reached! % 167.23/23.86 % (2415361)------------------------------ % 167.23/23.86 % (2415361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.23/23.86 % (2415361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.23/23.86 % (2415361)CaDiCaL version: 2.1.3 % 167.23/23.86 % (2415361)Termination reason: Instruction limit % 167.23/23.86 % (2415361)Termination phase: Saturation % 167.23/23.86 % (2415361)Time elapsed: 2.213 s % 167.23/23.86 % (2415361)Peak memory usage: 52 MB % 167.23/23.86 % (2415361)Instructions burned: 4593 (million) % 167.23/23.86 % (2415377)dis+10_16:1_sil=16000:random_seed=4156961935:i=9155:fsr=off_2948 on theBenchmark for (2948ds/9155Mi) % 167.23/23.86 % (2415365)Instruction limit reached! % 167.23/23.86 % (2415365)------------------------------ % 167.23/23.86 % (2415365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.23/23.86 % (2415365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.23/23.86 % (2415365)CaDiCaL version: 2.1.3 % 167.23/23.86 % (2415365)Termination reason: Instruction limit % 167.23/23.86 % (2415365)Termination phase: Saturation % 167.23/23.86 % (2415365)Time elapsed: 2.790 s % 167.23/23.86 % (2415365)Peak memory usage: 55 MB % 167.23/23.86 % (2415365)Instructions burned: 5212 (million) % 167.23/23.86 % (2415379)ott-3_8_sil=64000:random_seed=3622141404:i=20139:bs=on_2937 on theBenchmark for (2937ds/20139Mi) % 167.23/23.86 % (2415375)Instruction limit reached! % 167.23/23.86 % (2415375)------------------------------ % 167.23/23.86 % (2415375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.23/23.86 % (2415375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.23/23.86 % (2415375)CaDiCaL version: 2.1.3 % 167.23/23.86 % (2415375)Termination reason: Instruction limit % 167.23/23.86 % (2415375)Termination phase: Saturation % 167.23/23.86 % (2415375)Time elapsed: 4.877 s % 167.23/23.86 % (2415375)Peak memory usage: 61 MB % 167.23/23.86 % (2415375)Instructions burned: 8174 (million) % 167.23/23.86 % (2415381)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3403425750:fmbsr=2:i=32576_2910 on theBenchmark for (2910ds/32576Mi) % 167.23/23.86 % (2415381)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 167.23/23.86 % (2415381)Terminated due to inappropriate strategy. % 167.23/23.86 % (2415381)------------------------------ % 167.23/23.86 % (2415381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.23/23.86 % (2415381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.23/23.86 % (2415381)CaDiCaL version: 2.1.3 % 167.23/23.86 % (2415381)Termination reason: Inappropriate % 167.23/23.86 % (2415381)Time elapsed: 0.007 s % 167.23/23.86 % (2415381)Peak memory usage: 11 MB % 167.23/23.86 % (2415381)Instructions burned: 13 (million) % 167.23/23.86 % (2415381)------------------------------ % 167.23/23.86 % (2415381)------------------------------ % 167.23/23.86 % (2415383)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1223699234:i=11404_2910 on theBenchmark for (2910ds/11404Mi) % 167.23/23.86 % (2415377)Instruction limit reached! % 167.23/23.86 % (2415377)------------------------------ % 167.23/23.86 % (2415377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.23/23.86 % (2415377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.23/23.86 % (2415377)CaDiCaL version: 2.1.3 % 167.23/23.86 % (2415377)Termination reason: Instruction limit % 167.23/23.86 % (2415377)Termination phase: Saturation % 167.23/23.86 % (2415377)Time elapsed: 4.866 s % 167.23/23.86 % (2415377)Peak memory usage: 53 MB % 167.23/23.86 % (2415377)Instructions burned: 9157 (million) % 167.23/23.86 % (2415385)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3868046174:i=14134_2899 on theBenchmark for (2899ds/14134Mi) % 167.23/23.86 % (2415383)Instruction limit reached! % 167.23/23.86 % (2415383)------------------------------ % 167.23/23.86 % (2415383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 167.23/23.86 % (2415383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.23/23.86 % (2415383)CaDiCaL version: 2.1.3 % 167.23/23.86 % (2415383)Termination reason: Instruction limit % 167.23/23.86 % (2415383)Termination phase: Saturation % 167.23/23.86 % (2415383)Time elapsed: 8.158 s % 167.23/23.86 % (2415383)Peak memory usage: 93 MB % 167.23/23.86 % (2415383)Instructions burned: 11404 (million) % 167.23/23.86 % (2415693)dis+33_16_sil=32000:sac=on:random_seed=3883908385:i=15851:nm=0_2828 on theBenchmark for (2828ds/15851Mi) % 167.23/23.86 % (2415373)Instruction limit reached! % 167.23/23.86 % (2415373)------------------------------ % 167.23/23.86 % (2415373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.01/34.98 % (2415373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.01/34.98 % (2415373)CaDiCaL version: 2.1.3 % 246.01/34.98 % (2415373)Termination reason: Instruction limit % 246.01/34.98 % (2415373)Termination phase: Saturation % 246.01/34.98 % (2415373)Time elapsed: 15.029 s % 246.01/34.98 % (2415373)Peak memory usage: 160 MB % 246.01/34.98 % (2415373)Instructions burned: 22565 (million) % 246.01/34.98 % (2415701)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=59290020:avsq=on:i=17627:add=on:amm=off_2811 on theBenchmark for (2811ds/17627Mi) % 246.01/34.98 % (2415363)Instruction limit reached! % 246.01/34.98 % (2415363)------------------------------ % 246.01/34.98 % (2415363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.01/34.98 % (2415363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.01/34.98 % (2415363)CaDiCaL version: 2.1.3 % 246.01/34.98 % (2415363)Termination reason: Instruction limit % 246.01/34.98 % (2415363)Termination phase: Saturation % 246.01/34.98 % (2415363)Time elapsed: 17.376 s % 246.01/34.98 % (2415363)Peak memory usage: 181 MB % 246.01/34.98 % (2415363)Instructions burned: 29340 (million) % 246.01/34.98 % (2415713)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3223087227:s2a=on:i=53295_2794 on theBenchmark for (2794ds/53295Mi) % 246.01/34.98 % (2415385)Instruction limit reached! % 246.01/34.98 % (2415385)------------------------------ % 246.01/34.98 % (2415385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.01/34.98 % (2415385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.01/34.98 % (2415385)CaDiCaL version: 2.1.3 % 246.01/34.98 % (2415385)Termination reason: Instruction limit % 246.01/34.98 % (2415385)Termination phase: Saturation % 246.01/34.98 % (2415385)Time elapsed: 11.218 s % 246.01/34.98 % (2415385)Peak memory usage: 87 MB % 246.01/34.98 % (2415385)Instructions burned: 14134 (million) % 246.01/34.98 % (2415717)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1953374327:i=26857:ins=20_2787 on theBenchmark for (2787ds/26857Mi) % 246.01/34.98 % (2415717)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 246.01/34.98 % (2415717)Terminated due to inappropriate strategy. % 246.01/34.98 % (2415717)------------------------------ % 246.01/34.98 % (2415717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.01/34.98 % (2415717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.01/34.98 % (2415717)CaDiCaL version: 2.1.3 % 246.01/34.98 % (2415717)Termination reason: Inappropriate % 246.01/34.98 % (2415717)Time elapsed: 0.009 s % 246.01/34.98 % (2415717)Peak memory usage: 11 MB % 246.01/34.98 % (2415717)Instructions burned: 11 (million) % 246.01/34.98 % (2415717)------------------------------ % 246.01/34.98 % (2415717)------------------------------ % 246.01/34.98 % (2415719)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=554520075:i=28120:bs=on:fsr=off_2786 on theBenchmark for (2786ds/28120Mi) % 246.01/34.98 % (2415379)Instruction limit reached! % 246.01/34.98 % (2415379)------------------------------ % 246.01/34.98 % (2415379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.01/34.98 % (2415379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.01/34.98 % (2415379)CaDiCaL version: 2.1.3 % 246.01/34.98 % (2415379)Termination reason: Instruction limit % 246.01/34.98 % (2415379)Termination phase: Saturation % 246.01/34.98 % (2415379)Time elapsed: 17.058 s % 246.01/34.98 % (2415379)Peak memory usage: 111 MB % 246.01/34.98 % (2415379)Instructions burned: 20139 (million) % 246.01/34.98 % (2415723)fmb+10_1_sil=256000:fmbss=7:random_seed=1111109802:fmbsr=1.6:i=182295_2766 on theBenchmark for (2766ds/182295Mi) % 246.01/34.98 % (2415723)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 246.01/34.98 % (2415723)Terminated due to inappropriate strategy. % 246.01/34.98 % (2415723)------------------------------ % 246.01/34.98 % (2415723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.01/34.98 % (2415723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.01/34.98 % (2415723)CaDiCaL version: 2.1.3 % 246.01/34.98 % (2415723)Termination reason: Inappropriate % 246.01/34.98 % (2415723)Time elapsed: 0.007 s % 246.01/34.98 % (2415723)Peak memory usage: 11 MB % 246.01/34.98 % (2415723)Instructions burned: 11 (million) % 246.01/34.98 % (2415723)------------------------------ % 246.01/34.98 % (2415723)------------------------------ % 246.01/34.98 % (2415725)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1127172029:i=44625:gsp=on_2766 on theBenchmark for (2766ds/44625Mi) % 251.44/35.89 % (2415725)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.44/35.89 % (2415725)Terminated due to inappropriate strategy. % 251.44/35.89 % (2415725)------------------------------ % 251.44/35.89 % (2415725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.44/35.89 % (2415725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.44/35.89 % (2415725)CaDiCaL version: 2.1.3 % 251.44/35.89 % (2415725)Termination reason: Inappropriate % 251.44/35.89 % (2415725)Time elapsed: 0.013 s % 251.44/35.89 % (2415725)Peak memory usage: 11 MB % 251.44/35.89 % (2415725)Instructions burned: 11 (million) % 251.44/35.89 % (2415725)------------------------------ % 251.44/35.89 % (2415725)------------------------------ % 251.44/35.89 % (2415727)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2687830454:i=160505_2765 on theBenchmark for (2765ds/160505Mi) % 251.44/35.89 % (2415727)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.44/35.89 % (2415727)Terminated due to inappropriate strategy. % 251.44/35.89 % (2415727)------------------------------ % 251.44/35.89 % (2415727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.44/35.89 % (2415727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.44/35.89 % (2415727)CaDiCaL version: 2.1.3 % 251.44/35.89 % (2415727)Termination reason: Inappropriate % 251.44/35.89 % (2415727)Time elapsed: 0.006 s % 251.44/35.89 % (2415727)Peak memory usage: 11 MB % 251.44/35.89 % (2415727)Instructions burned: 11 (million) % 251.44/35.89 % (2415727)------------------------------ % 251.44/35.89 % (2415727)------------------------------ % 251.44/35.89 % (2415729)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2825622641:fmbsr=1.3:i=225729_2765 on theBenchmark for (2765ds/225729Mi) % 251.44/35.89 % (2415729)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.44/35.89 % (2415729)Terminated due to inappropriate strategy. % 251.44/35.89 % (2415729)------------------------------ % 251.44/35.89 % (2415729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.44/35.89 % (2415729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.44/35.89 % (2415729)CaDiCaL version: 2.1.3 % 251.44/35.89 % (2415729)Termination reason: Inappropriate % 251.44/35.89 % (2415729)Time elapsed: 0.007 s % 251.44/35.89 % (2415729)Peak memory usage: 11 MB % 251.44/35.89 % (2415729)Instructions burned: 11 (million) % 251.44/35.89 % (2415729)------------------------------ % 251.44/35.89 % (2415729)------------------------------ % 251.44/35.89 % (2415731)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=413491242:fmbsr=2:i=185024:ins=7_2765 on theBenchmark for (2765ds/185024Mi) % 251.44/35.89 % (2415731)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.44/35.89 % (2415731)Terminated due to inappropriate strategy. % 251.44/35.89 % (2415731)------------------------------ % 251.44/35.89 % (2415731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.44/35.89 % (2415731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.44/35.89 % (2415731)CaDiCaL version: 2.1.3 % 251.44/35.89 % (2415731)Termination reason: Inappropriate % 251.44/35.89 % (2415731)Time elapsed: 0.010 s % 251.44/35.89 % (2415731)Peak memory usage: 11 MB % 251.44/35.89 % (2415731)Instructions burned: 11 (million) % 251.44/35.89 % (2415731)------------------------------ % 251.44/35.89 % (2415731)------------------------------ % 251.44/35.89 % (2415733)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2383269:rtra=on_2764 on theBenchmark for (2764ds/0Mi) % 251.44/35.89 % (2415733)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.44/35.89 % (2415733)Terminated due to inappropriate strategy. % 251.44/35.89 % (2415733)------------------------------ % 251.44/35.89 % (2415733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.44/35.89 % (2415733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.44/35.89 % (2415733)CaDiCaL version: 2.1.3 % 251.44/35.89 % (2415733)Termination reason: Inappropriate % 251.44/35.89 % (2415733)Time elapsed: 0.009 s % 251.44/35.89 % (2415733)Peak memory usage: 11 MB % 251.44/35.89 % (2415733)Instructions burned: 14 (million) % 251.44/35.89 % (2415733)------------------------------ % 251.44/35.89 % (2415733)------------------------------ % 251.44/35.89 % (2415735)% WARNING: option uhcvi not known. % 251.44/35.89 % (2415735)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2255986424:i=271062:add=off:rtra=on:rawr=on_2764 on theBenchmark for (2764ds/271062Mi) % 264.65/37.50 % (2415693)Instruction limit reached! % 264.65/37.50 % (2415693)------------------------------ % 264.65/37.50 % (2415693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.65/37.50 % (2415693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.65/37.50 % (2415693)CaDiCaL version: 2.1.3 % 264.65/37.50 % (2415693)Termination reason: Instruction limit % 264.65/37.50 % (2415693)Termination phase: Saturation % 264.65/37.50 % (2415693)Time elapsed: 14.361 s % 264.65/37.50 % (2415693)Peak memory usage: 132 MB % 264.65/37.50 % (2415693)Instructions burned: 15851 (million) % 264.65/37.50 % (2415898)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2087266600:i=176048:add=on:rtra=on:rawr=on_2684 on theBenchmark for (2684ds/176048Mi) % 264.65/37.50 % (2415701)Instruction limit reached! % 264.65/37.50 % (2415701)------------------------------ % 264.65/37.50 % (2415701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.65/37.50 % (2415701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.65/37.50 % (2415701)CaDiCaL version: 2.1.3 % 264.65/37.50 % (2415701)Termination reason: Instruction limit % 264.65/37.50 % (2415701)Termination phase: Saturation % 264.65/37.50 % (2415701)Time elapsed: 15.484 s % 264.65/37.50 % (2415701)Peak memory usage: 139 MB % 264.65/37.50 % (2415701)Instructions burned: 17627 (million) % 264.65/37.50 % (2415719)Instruction limit reached! % 264.65/37.50 % (2415719)------------------------------ % 264.65/37.50 % (2415719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.65/37.50 % (2415719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.65/37.50 % (2415719)CaDiCaL version: 2.1.3 % 264.65/37.50 % (2415719)Termination reason: Instruction limit % 264.65/37.50 % (2415719)Termination phase: Saturation % 264.65/37.50 % (2415719)Time elapsed: 12.986 s % 264.65/37.50 % (2415719)Peak memory usage: 14 MB % 264.65/37.50 % (2415719)Instructions burned: 28122 (million) % 264.65/37.50 % (2415901)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3467948179:i=206:fgj=on:rtra=on_2656 on theBenchmark for (2656ds/206Mi) % 264.65/37.50 % (2415902)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1876851758:i=232:rtra=on_2656 on theBenchmark for (2656ds/232Mi) % 264.65/37.50 % (2415901)Instruction limit reached! % 264.65/37.50 % (2415901)------------------------------ % 264.65/37.50 % (2415901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.65/37.50 % (2415901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.65/37.50 % (2415901)CaDiCaL version: 2.1.3 % 264.65/37.50 % (2415901)Termination reason: Instruction limit % 264.65/37.50 % (2415901)Termination phase: Saturation % 264.65/37.50 % (2415901)Time elapsed: 0.131 s % 264.65/37.50 % (2415901)Peak memory usage: 14 MB % 264.65/37.50 % (2415901)Instructions burned: 206 (million) % 264.65/37.50 % (2415905)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3252185608:i=262:rtra=on_2655 on theBenchmark for (2655ds/262Mi) % 264.65/37.50 % (2415902)Instruction limit reached! % 264.65/37.50 % (2415902)------------------------------ % 264.65/37.50 % (2415902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.65/37.50 % (2415902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.65/37.50 % (2415902)CaDiCaL version: 2.1.3 % 264.65/37.50 % (2415902)Termination reason: Instruction limit % 264.65/37.50 % (2415902)Termination phase: Saturation % 264.65/37.50 % (2415902)Time elapsed: 0.154 s % 264.65/37.50 % (2415902)Peak memory usage: 14 MB % 264.65/37.50 % (2415902)Instructions burned: 233 (million) % 264.65/37.50 % (2415907)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3755075650:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2654 on theBenchmark for (2654ds/318Mi) % 264.65/37.50 % (2415905)Instruction limit reached! % 264.65/37.50 % (2415905)------------------------------ % 264.65/37.50 % (2415905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.65/37.50 % (2415905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.65/37.50 % (2415905)CaDiCaL version: 2.1.3 % 264.65/37.50 % (2415905)Termination reason: Instruction limit % 264.65/37.50 % (2415905)Termination phase: Saturation % 264.65/37.50 % (2415905)Time elapsed: 0.163 s % 264.65/37.50 % (2415905)Peak memory usage: 15 MB % 264.65/37.50 % (2415905)Instructions burned: 263 (million) % 264.65/37.50 % (2415909)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1144755126:i=1428:nm=2:rtra=on_2653 on theBenchmark for (2653ds/1428Mi) % 279.57/39.64 % (2415909)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.57/39.64 % (2415909)Terminated due to inappropriate strategy. % 279.57/39.64 % (2415909)------------------------------ % 279.57/39.64 % (2415909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.57/39.64 % (2415909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.57/39.64 % (2415909)CaDiCaL version: 2.1.3 % 279.57/39.64 % (2415909)Termination reason: Inappropriate % 279.57/39.64 % (2415909)Time elapsed: 0.007 s % 279.57/39.64 % (2415909)Peak memory usage: 11 MB % 279.57/39.64 % (2415909)Instructions burned: 12 (million) % 279.57/39.64 % (2415909)------------------------------ % 279.57/39.64 % (2415909)------------------------------ % 279.57/39.64 % (2415911)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1413628826:i=262:bd=preordered:rtra=on:fsd=on_2652 on theBenchmark for (2652ds/262Mi) % 279.57/39.64 % (2415907)Instruction limit reached! % 279.57/39.64 % (2415907)------------------------------ % 279.57/39.64 % (2415907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.57/39.64 % (2415907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.57/39.64 % (2415907)CaDiCaL version: 2.1.3 % 279.57/39.64 % (2415907)Termination reason: Instruction limit % 279.57/39.64 % (2415907)Termination phase: Saturation % 279.57/39.64 % (2415907)Time elapsed: 0.211 s % 279.57/39.64 % (2415907)Peak memory usage: 16 MB % 279.57/39.64 % (2415907)Instructions burned: 319 (million) % 279.57/39.64 % (2415913)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=4273652255:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2652 on theBenchmark for (2652ds/1368Mi) % 279.57/39.64 % (2415911)Instruction limit reached! % 279.57/39.64 % (2415911)------------------------------ % 279.57/39.64 % (2415911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.57/39.64 % (2415911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.57/39.64 % (2415911)CaDiCaL version: 2.1.3 % 279.57/39.64 % (2415911)Termination reason: Instruction limit % 279.57/39.64 % (2415911)Termination phase: Saturation % 279.57/39.64 % (2415911)Time elapsed: 0.175 s % 279.57/39.64 % (2415911)Peak memory usage: 13 MB % 279.57/39.64 % (2415911)Instructions burned: 263 (million) % 279.57/39.64 % (2415915)ott-21_1_sil=16000:si=on:fs=off:random_seed=4283408007:i=360:av=off:fsr=off:rtra=on_2651 on theBenchmark for (2651ds/360Mi) % 279.57/39.64 % (2415915)Instruction limit reached! % 279.57/39.64 % (2415915)------------------------------ % 279.57/39.64 % (2415915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.57/39.64 % (2415915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.57/39.64 % (2415915)CaDiCaL version: 2.1.3 % 279.57/39.64 % (2415915)Termination reason: Instruction limit % 279.57/39.64 % (2415915)Termination phase: Saturation % 279.57/39.64 % (2415915)Time elapsed: 0.190 s % 279.57/39.64 % (2415915)Peak memory usage: 14 MB % 279.57/39.64 % (2415915)Instructions burned: 360 (million) % 279.57/39.64 % (2415917)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=17080609:i=954:bd=all:rtra=on_2648 on theBenchmark for (2648ds/954Mi) % 279.57/39.64 % (2415913)Instruction limit reached! % 279.57/39.64 % (2415913)------------------------------ % 279.57/39.64 % (2415913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.57/39.64 % (2415913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.57/39.64 % (2415913)CaDiCaL version: 2.1.3 % 279.57/39.64 % (2415913)Termination reason: Instruction limit % 279.57/39.64 % (2415913)Termination phase: Saturation % 279.57/39.64 % (2415913)Time elapsed: 0.802 s % 279.57/39.64 % (2415913)Peak memory usage: 22 MB % 279.57/39.64 % (2415913)Instructions burned: 1368 (million) % 279.57/39.64 % (2415919)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=806837327:fmbsr=1.3:i=1730:ins=25:rtra=on_2644 on theBenchmark for (2644ds/1730Mi) % 279.57/39.64 % (2415919)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.57/39.64 % (2415919)Terminated due to inappropriate strategy. % 279.57/39.64 % (2415919)------------------------------ % 279.57/39.64 % (2415919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.57/39.64 % (2415919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.57/39.64 % (2415919)CaDiCaL version: 2.1.3 % 279.57/39.64 % (2415919)TerminTerminated % 300.17/42.54 % Vampire exiting %------------------------------------------------------------------------------