%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW841_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n011.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:03 PM UTC 2026 % Result : Timeout 297.71s 42.16s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW841_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.19 % Computer : n011.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 14:32:37 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.83/0.89 % (3430277)Will run a generic schedule for satisfiability detection. % 3.83/0.89 % (3430284)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=877984083:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.83/0.89 % (3430283)% WARNING: option uhcvi not known. % 3.83/0.89 % (3430282)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3366904586_2999 on theBenchmark for (2999ds/0Mi) % 3.83/0.89 % (3430283)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3584507013:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.83/0.89 % (3430285)dis+10_1_sil=32000:sp=arity:random_seed=811600095:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.83/0.89 % (3430286)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2238825731:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.83/0.89 % (3430287)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4199908566:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.83/0.89 % (3430288)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1195661344:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.83/0.89 % (3430282)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.83/0.89 % (3430282)Terminated due to inappropriate strategy. % 3.83/0.89 % (3430282)------------------------------ % 3.83/0.89 % (3430282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.83/0.89 % (3430282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.83/0.89 % (3430282)CaDiCaL version: 2.1.3 % 3.83/0.89 % (3430282)Termination reason: Inappropriate % 3.83/0.89 % (3430282)Time elapsed: 0.020 s % 3.83/0.89 % (3430282)Peak memory usage: 11 MB % 3.83/0.89 % (3430282)Instructions burned: 43 (million) % 3.83/0.89 % (3430282)------------------------------ % 3.83/0.89 % (3430282)------------------------------ % 3.83/0.89 % (3430296)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4187890736:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.83/0.89 % (3430285)Instruction limit reached! % 3.83/0.89 % (3430285)------------------------------ % 3.83/0.89 % (3430285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.83/0.89 % (3430285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.83/0.89 % (3430285)CaDiCaL version: 2.1.3 % 3.83/0.89 % (3430285)Termination reason: Instruction limit % 3.83/0.89 % (3430285)Termination phase: Saturation % 3.83/0.89 % (3430285)Time elapsed: 0.058 s % 3.83/0.89 % (3430285)Peak memory usage: 13 MB % 3.83/0.89 % (3430285)Instructions burned: 104 (million) % 3.83/0.89 % (3430296)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.83/0.89 % (3430296)Terminated due to inappropriate strategy. % 3.83/0.89 % (3430296)------------------------------ % 3.83/0.89 % (3430296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.83/0.89 % (3430296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.83/0.89 % (3430296)CaDiCaL version: 2.1.3 % 3.83/0.89 % (3430296)Termination reason: Inappropriate % 3.83/0.89 % (3430296)Time elapsed: 0.019 s % 3.83/0.89 % (3430296)Peak memory usage: 11 MB % 3.83/0.89 % (3430296)Instructions burned: 43 (million) % 3.83/0.89 % (3430296)------------------------------ % 3.83/0.89 % (3430296)------------------------------ % 3.83/0.89 % (3430286)Instruction limit reached! % 3.83/0.89 % (3430286)------------------------------ % 3.83/0.89 % (3430286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.83/0.89 % (3430286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.83/0.89 % (3430286)CaDiCaL version: 2.1.3 % 3.83/0.89 % (3430286)Termination reason: Instruction limit % 3.83/0.89 % (3430286)Termination phase: Saturation % 3.83/0.89 % (3430286)Time elapsed: 0.065 s % 3.83/0.89 % (3430286)Peak memory usage: 13 MB % 3.83/0.89 % (3430286)Instructions burned: 117 (million) % 3.83/0.89 % (3430287)Instruction limit reached! % 3.83/0.89 % (3430287)------------------------------ % 3.83/0.89 % (3430287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.83/0.89 % (3430287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.83/0.89 % (3430287)CaDiCaL version: 2.1.3 % 3.83/0.89 % (3430287)Termination reason: Instruction limit % 3.83/0.89 % (3430287)Termination phase: Saturation % 3.83/0.89 % (3430287)Time elapsed: 0.072 s % 3.83/0.89 % (3430287)Peak memory usage: 14 MB % 3.83/0.89 % (3430287)Instructions burned: 131 (million) % 5.55/1.11 % (3430298)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3936627172:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 5.55/1.11 % (3430299)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=239052935:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.55/1.11 % (3430300)ott-21_1_sil=16000:fs=off:random_seed=3265577786:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.55/1.11 % (3430288)Instruction limit reached! % 5.55/1.11 % (3430288)------------------------------ % 5.55/1.11 % (3430288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.55/1.11 % (3430288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.55/1.11 % (3430288)CaDiCaL version: 2.1.3 % 5.55/1.11 % (3430288)Termination reason: Instruction limit % 5.55/1.11 % (3430288)Termination phase: Saturation % 5.55/1.11 % (3430288)Time elapsed: 0.091 s % 5.55/1.11 % (3430288)Peak memory usage: 13 MB % 5.55/1.11 % (3430288)Instructions burned: 159 (million) % 5.55/1.11 % (3430301)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2727104399:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.55/1.11 % (3430306)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3717186620:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.55/1.11 % (3430306)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.55/1.11 % (3430306)Terminated due to inappropriate strategy. % 5.55/1.11 % (3430306)------------------------------ % 5.55/1.11 % (3430306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.55/1.11 % (3430306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.55/1.11 % (3430306)CaDiCaL version: 2.1.3 % 5.55/1.11 % (3430306)Termination reason: Inappropriate % 5.55/1.11 % (3430306)Time elapsed: 0.019 s % 5.55/1.11 % (3430306)Peak memory usage: 11 MB % 5.55/1.11 % (3430306)Instructions burned: 42 (million) % 5.55/1.11 % (3430306)------------------------------ % 5.55/1.11 % (3430306)------------------------------ % 5.55/1.11 % (3430308)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4286547880:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.55/1.11 % (3430298)Instruction limit reached! % 5.55/1.11 % (3430298)------------------------------ % 5.55/1.11 % (3430298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.55/1.11 % (3430298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.55/1.11 % (3430298)CaDiCaL version: 2.1.3 % 5.55/1.11 % (3430298)Termination reason: Instruction limit % 5.55/1.11 % (3430298)Termination phase: Saturation % 5.55/1.11 % (3430298)Time elapsed: 0.076 s % 5.55/1.11 % (3430298)Peak memory usage: 14 MB % 5.55/1.11 % (3430298)Instructions burned: 131 (million) % 5.55/1.11 % (3430300)Instruction limit reached! % 5.55/1.11 % (3430300)------------------------------ % 5.55/1.11 % (3430300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.55/1.11 % (3430300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.55/1.11 % (3430300)CaDiCaL version: 2.1.3 % 5.55/1.11 % (3430300)Termination reason: Instruction limit % 5.55/1.11 % (3430300)Termination phase: Saturation % 5.55/1.11 % (3430300)Time elapsed: 0.082 s % 5.55/1.11 % (3430300)Peak memory usage: 13 MB % 5.55/1.11 % (3430300)Instructions burned: 181 (million) % 5.55/1.11 % (3430310)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=158720760:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 5.55/1.11 % (3430311)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=2875823867: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) % 5.55/1.11 % (3430310)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.55/1.11 % (3430310)Terminated due to inappropriate strategy. % 5.55/1.11 % (3430310)------------------------------ % 5.55/1.11 % (3430310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.55/1.11 % (3430310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.55/1.11 % (3430310)CaDiCaL version: 2.1.3 % 5.55/1.11 % (3430310)Termination reason: Inappropriate % 5.55/1.11 % (3430310)Time elapsed: 0.019 s % 5.55/1.11 % (3430310)Peak memory usage: 11 MB % 21.66/3.39 % (3430310)Instructions burned: 43 (million) % 21.66/3.39 % (3430310)------------------------------ % 21.66/3.39 % (3430310)------------------------------ % 21.66/3.39 % (3430314)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=490247378:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.66/3.39 % (3430301)Instruction limit reached! % 21.66/3.39 % (3430301)------------------------------ % 21.66/3.39 % (3430301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.66/3.39 % (3430301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.66/3.39 % (3430301)CaDiCaL version: 2.1.3 % 21.66/3.39 % (3430301)Termination reason: Instruction limit % 21.66/3.39 % (3430301)Termination phase: Saturation % 21.66/3.39 % (3430301)Time elapsed: 0.276 s % 21.66/3.39 % (3430301)Peak memory usage: 16 MB % 21.66/3.39 % (3430301)Instructions burned: 478 (million) % 21.66/3.39 % (3430316)fmb+10_1_sil=64000:random_seed=2975337764:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 21.66/3.39 % (3430316)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.66/3.39 % (3430316)Terminated due to inappropriate strategy. % 21.66/3.39 % (3430316)------------------------------ % 21.66/3.39 % (3430316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.66/3.39 % (3430316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.66/3.39 % (3430316)CaDiCaL version: 2.1.3 % 21.66/3.39 % (3430316)Termination reason: Inappropriate % 21.66/3.39 % (3430316)Time elapsed: 0.019 s % 21.66/3.39 % (3430316)Peak memory usage: 11 MB % 21.66/3.39 % (3430316)Instructions burned: 43 (million) % 21.66/3.39 % (3430316)------------------------------ % 21.66/3.39 % (3430316)------------------------------ % 21.66/3.39 % (3430318)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1714468073:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 21.66/3.39 % (3430318)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.66/3.39 % (3430318)Terminated due to inappropriate strategy. % 21.66/3.39 % (3430318)------------------------------ % 21.66/3.39 % (3430318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.66/3.39 % (3430318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.66/3.39 % (3430318)CaDiCaL version: 2.1.3 % 21.66/3.39 % (3430318)Termination reason: Inappropriate % 21.66/3.39 % (3430318)Time elapsed: 0.019 s % 21.66/3.39 % (3430318)Peak memory usage: 11 MB % 21.66/3.39 % (3430318)Instructions burned: 43 (million) % 21.66/3.39 % (3430318)------------------------------ % 21.66/3.39 % (3430318)------------------------------ % 21.66/3.39 % (3430299)Instruction limit reached! % 21.66/3.39 % (3430299)------------------------------ % 21.66/3.39 % (3430299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.66/3.39 % (3430299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.66/3.39 % (3430299)CaDiCaL version: 2.1.3 % 21.66/3.39 % (3430299)Termination reason: Instruction limit % 21.66/3.39 % (3430299)Termination phase: Saturation % 21.66/3.39 % (3430299)Time elapsed: 0.371 s % 21.66/3.39 % (3430299)Peak memory usage: 17 MB % 21.66/3.39 % (3430299)Instructions burned: 685 (million) % 21.66/3.39 % (3430320)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1546048527:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 21.66/3.39 % (3430321)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1635280089:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 21.66/3.39 % (3430320)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.66/3.39 % (3430320)Terminated due to inappropriate strategy. % 21.66/3.39 % (3430320)------------------------------ % 21.66/3.39 % (3430320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.66/3.39 % (3430320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.66/3.39 % (3430320)CaDiCaL version: 2.1.3 % 21.66/3.39 % (3430320)Termination reason: Inappropriate % 21.66/3.39 % (3430320)Time elapsed: 0.019 s % 21.66/3.39 % (3430320)Peak memory usage: 11 MB % 21.66/3.39 % (3430320)Instructions burned: 43 (million) % 21.66/3.39 % (3430320)------------------------------ % 21.66/3.39 % (3430320)------------------------------ % 21.66/3.39 % (3430324)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2237847723:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 21.66/3.39 % (3430311)Instruction limit reached! % 21.66/3.39 % (3430311)------------------------------ % 23.99/3.79 % (3430311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.99/3.79 % (3430311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.99/3.79 % (3430311)CaDiCaL version: 2.1.3 % 23.99/3.79 % (3430311)Termination reason: Instruction limit % 23.99/3.79 % (3430311)Termination phase: Saturation % 23.99/3.79 % (3430311)Time elapsed: 0.424 s % 23.99/3.79 % (3430311)Peak memory usage: 19 MB % 23.99/3.79 % (3430311)Instructions burned: 692 (million) % 23.99/3.79 % (3430326)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4275069923:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 23.99/3.79 % (3430326)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.99/3.79 % (3430326)Terminated due to inappropriate strategy. % 23.99/3.79 % (3430326)------------------------------ % 23.99/3.79 % (3430326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.99/3.79 % (3430326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.99/3.79 % (3430326)CaDiCaL version: 2.1.3 % 23.99/3.79 % (3430326)Termination reason: Inappropriate % 23.99/3.79 % (3430326)Time elapsed: 0.019 s % 23.99/3.79 % (3430326)Peak memory usage: 11 MB % 23.99/3.79 % (3430326)Instructions burned: 43 (million) % 23.99/3.79 % (3430326)------------------------------ % 23.99/3.79 % (3430326)------------------------------ % 23.99/3.79 % (3430328)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1791547846:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 23.99/3.79 % (3430314)Instruction limit reached! % 23.99/3.79 % (3430314)------------------------------ % 23.99/3.79 % (3430314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.99/3.79 % (3430314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.99/3.79 % (3430314)CaDiCaL version: 2.1.3 % 23.99/3.79 % (3430314)Termination reason: Instruction limit % 23.99/3.79 % (3430314)Termination phase: Saturation % 23.99/3.79 % (3430314)Time elapsed: 0.470 s % 23.99/3.79 % (3430314)Peak memory usage: 18 MB % 23.99/3.79 % (3430314)Instructions burned: 880 (million) % 23.99/3.79 % (3430328)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.99/3.79 % (3430328)Terminated due to inappropriate strategy. % 23.99/3.79 % (3430328)------------------------------ % 23.99/3.79 % (3430328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.99/3.79 % (3430328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.99/3.79 % (3430328)CaDiCaL version: 2.1.3 % 23.99/3.79 % (3430328)Termination reason: Inappropriate % 23.99/3.79 % (3430328)Time elapsed: 0.019 s % 23.99/3.79 % (3430328)Peak memory usage: 12 MB % 23.99/3.79 % (3430328)Instructions burned: 43 (million) % 23.99/3.79 % (3430328)------------------------------ % 23.99/3.79 % (3430328)------------------------------ % 23.99/3.79 % (3430330)ott-2_1_sil=16000:newcnf=on:random_seed=2858507838:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 23.99/3.79 % (3430331)ott+10_1_sil=32000:tgt=ground:random_seed=2664635347:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 23.99/3.79 % (3430308)Instruction limit reached! % 23.99/3.79 % (3430308)------------------------------ % 23.99/3.79 % (3430308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.99/3.79 % (3430308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.99/3.79 % (3430308)CaDiCaL version: 2.1.3 % 23.99/3.79 % (3430308)Termination reason: Instruction limit % 23.99/3.79 % (3430308)Termination phase: Saturation % 23.99/3.79 % (3430308)Time elapsed: 0.637 s % 23.99/3.79 % (3430308)Peak memory usage: 23 MB % 23.99/3.79 % (3430308)Instructions burned: 1180 (million) % 23.99/3.79 % (3430334)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=354359840:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 23.99/3.79 % (3430334)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.99/3.79 % (3430334)Terminated due to inappropriate strategy. % 23.99/3.79 % (3430334)------------------------------ % 23.99/3.79 % (3430334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.99/3.79 % (3430334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.99/3.79 % (3430334)CaDiCaL version: 2.1.3 % 23.99/3.79 % (3430334)Termination reason: Inappropriate % 23.99/3.79 % (3430334)Time elapsed: 0.019 s % 23.99/3.79 % (3430334)Peak memory usage: 11 MB % 23.99/3.79 % (3430334)Instructions burned: 43 (million) % 128.28/18.32 % (3430334)------------------------------ % 128.28/18.32 % (3430334)------------------------------ % 128.28/18.32 % (3430336)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2367482602:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 128.28/18.32 % (3430330)Instruction limit reached! % 128.28/18.32 % (3430330)------------------------------ % 128.28/18.32 % (3430330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.28/18.32 % (3430330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.28/18.32 % (3430330)CaDiCaL version: 2.1.3 % 128.28/18.32 % (3430330)Termination reason: Instruction limit % 128.28/18.32 % (3430330)Termination phase: Saturation % 128.28/18.32 % (3430330)Time elapsed: 0.473 s % 128.28/18.32 % (3430330)Peak memory usage: 19 MB % 128.28/18.32 % (3430330)Instructions burned: 871 (million) % 128.28/18.32 % (3430338)dis+21_1_sil=32000:sas=cadical:random_seed=1360238008:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 128.28/18.32 % (3430324)Instruction limit reached! % 128.28/18.32 % (3430324)------------------------------ % 128.28/18.32 % (3430324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.28/18.32 % (3430324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.28/18.32 % (3430324)CaDiCaL version: 2.1.3 % 128.28/18.32 % (3430324)Termination reason: Instruction limit % 128.28/18.32 % (3430324)Termination phase: Saturation % 128.28/18.32 % (3430324)Time elapsed: 0.772 s % 128.28/18.32 % (3430324)Peak memory usage: 31 MB % 128.28/18.32 % (3430324)Instructions burned: 1472 (million) % 128.28/18.32 % (3430340)ott+11_1_sil=16000:gs=on:random_seed=1607643706:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 128.28/18.32 % (3430340)Instruction limit reached! % 128.28/18.32 % (3430340)------------------------------ % 128.28/18.32 % (3430340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.28/18.32 % (3430340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.28/18.32 % (3430340)CaDiCaL version: 2.1.3 % 128.28/18.32 % (3430340)Termination reason: Instruction limit % 128.28/18.32 % (3430340)Termination phase: Saturation % 128.28/18.32 % (3430340)Time elapsed: 1.233 s % 128.28/18.32 % (3430340)Peak memory usage: 29 MB % 128.28/18.32 % (3430340)Instructions burned: 2251 (million) % 128.28/18.32 % (3430342)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=669096048:fmbsr=1.6:i=67534_2974 on theBenchmark for (2974ds/67534Mi) % 128.28/18.32 % (3430342)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.28/18.32 % (3430342)Terminated due to inappropriate strategy. % 128.28/18.32 % (3430342)------------------------------ % 128.28/18.32 % (3430342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.28/18.32 % (3430342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.28/18.32 % (3430342)CaDiCaL version: 2.1.3 % 128.28/18.32 % (3430342)Termination reason: Inappropriate % 128.28/18.32 % (3430342)Time elapsed: 0.019 s % 128.28/18.32 % (3430342)Peak memory usage: 11 MB % 128.28/18.32 % (3430342)Instructions burned: 43 (million) % 128.28/18.32 % (3430342)------------------------------ % 128.28/18.32 % (3430342)------------------------------ % 128.28/18.32 % (3430344)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1412066410:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2973 on theBenchmark for (2973ds/4591Mi) % 128.28/18.32 % (3430336)Instruction limit reached! % 128.28/18.32 % (3430336)------------------------------ % 128.28/18.32 % (3430336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.28/18.32 % (3430336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.28/18.32 % (3430336)CaDiCaL version: 2.1.3 % 128.28/18.32 % (3430336)Termination reason: Instruction limit % 128.28/18.32 % (3430336)Termination phase: Saturation % 128.28/18.32 % (3430336)Time elapsed: 1.781 s % 128.28/18.32 % (3430336)Peak memory usage: 38 MB % 128.28/18.32 % (3430336)Instructions burned: 3513 (million) % 128.28/18.32 % (3430346)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3307564820:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 128.28/18.32 % (3430321)Instruction limit reached! % 128.28/18.32 % (3430321)------------------------------ % 128.28/18.32 % (3430321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.28/18.32 % (3430321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.28/18.32 % (3430321)CaDiCaL version: 2.1.3 % 128.28/18.32 % (3430321)Termination reason: Instruction limit % 156.03/22.30 % (3430321)Termination phase: Saturation % 156.03/22.30 % (3430321)Time elapsed: 2.631 s % 156.03/22.30 % (3430321)Peak memory usage: 43 MB % 156.03/22.30 % (3430321)Instructions burned: 5131 (million) % 156.03/22.30 % (3430338)Instruction limit reached! % 156.03/22.30 % (3430338)------------------------------ % 156.03/22.30 % (3430338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.03/22.30 % (3430338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.03/22.30 % (3430338)CaDiCaL version: 2.1.3 % 156.03/22.30 % (3430338)Termination reason: Instruction limit % 156.03/22.30 % (3430338)Termination phase: Saturation % 156.03/22.30 % (3430338)Time elapsed: 1.912 s % 156.03/22.30 % (3430338)Peak memory usage: 35 MB % 156.03/22.30 % (3430338)Instructions burned: 3774 (million) % 156.03/22.30 % (3430348)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2471005403:i=5211_2968 on theBenchmark for (2968ds/5211Mi) % 156.03/22.30 % (3430349)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=171002553:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 156.03/22.30 % (3430349)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.03/22.30 % (3430349)Terminated due to inappropriate strategy. % 156.03/22.30 % (3430349)------------------------------ % 156.03/22.30 % (3430349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.03/22.30 % (3430349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.03/22.30 % (3430349)CaDiCaL version: 2.1.3 % 156.03/22.30 % (3430349)Termination reason: Inappropriate % 156.03/22.30 % (3430349)Time elapsed: 0.019 s % 156.03/22.30 % (3430349)Peak memory usage: 11 MB % 156.03/22.30 % (3430349)Instructions burned: 43 (million) % 156.03/22.30 % (3430349)------------------------------ % 156.03/22.30 % (3430349)------------------------------ % 156.03/22.30 % (3430352)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1392079272:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 156.03/22.30 % (3430352)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.03/22.30 % (3430352)Terminated due to inappropriate strategy. % 156.03/22.30 % (3430352)------------------------------ % 156.03/22.30 % (3430352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.03/22.30 % (3430352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.03/22.30 % (3430352)CaDiCaL version: 2.1.3 % 156.03/22.30 % (3430352)Termination reason: Inappropriate % 156.03/22.30 % (3430352)Time elapsed: 0.019 s % 156.03/22.30 % (3430352)Peak memory usage: 11 MB % 156.03/22.30 % (3430352)Instructions burned: 43 (million) % 156.03/22.30 % (3430352)------------------------------ % 156.03/22.30 % (3430352)------------------------------ % 156.03/22.30 % (3430354)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4273576407:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 156.03/22.30 % (3430354)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.03/22.30 % (3430354)Terminated due to inappropriate strategy. % 156.03/22.30 % (3430354)------------------------------ % 156.03/22.30 % (3430354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.03/22.30 % (3430354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.03/22.30 % (3430354)CaDiCaL version: 2.1.3 % 156.03/22.30 % (3430354)Termination reason: Inappropriate % 156.03/22.30 % (3430354)Time elapsed: 0.019 s % 156.03/22.30 % (3430354)Peak memory usage: 11 MB % 156.03/22.30 % (3430354)Instructions burned: 43 (million) % 156.03/22.30 % (3430354)------------------------------ % 156.03/22.30 % (3430354)------------------------------ % 156.03/22.30 % (3430356)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4045752738:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 156.03/22.30 % (3430331)Instruction limit reached! % 156.03/22.30 % (3430331)------------------------------ % 156.03/22.30 % (3430331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.03/22.30 % (3430331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.03/22.30 % (3430331)CaDiCaL version: 2.1.3 % 156.03/22.30 % (3430331)Termination reason: Instruction limit % 156.03/22.30 % (3430331)Termination phase: Saturation % 156.03/22.30 % (3430331)Time elapsed: 2.766 s % 156.03/22.30 % (3430331)Peak memory usage: 45 MB % 156.03/22.30 % (3430331)Instructions burned: 5115 (million) % 156.03/22.30 % (3430358)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1916942986:i=8173:av=off_2964 on theBenchmark for (2964ds/8173Mi) % 158.83/22.70 % (3430344)Instruction limit reached! % 158.83/22.70 % (3430344)------------------------------ % 158.83/22.70 % (3430344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.83/22.70 % (3430344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.83/22.70 % (3430344)CaDiCaL version: 2.1.3 % 158.83/22.70 % (3430344)Termination reason: Instruction limit % 158.83/22.70 % (3430344)Termination phase: Saturation % 158.83/22.70 % (3430344)Time elapsed: 2.161 s % 158.83/22.70 % (3430344)Peak memory usage: 50 MB % 158.83/22.70 % (3430344)Instructions burned: 4592 (million) % 158.83/22.70 % (3430360)dis+10_16:1_sil=16000:random_seed=2349989739:i=9155:fsr=off_2951 on theBenchmark for (2951ds/9155Mi) % 158.83/22.70 % (3430348)Instruction limit reached! % 158.83/22.70 % (3430348)------------------------------ % 158.83/22.70 % (3430348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.83/22.70 % (3430348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.83/22.70 % (3430348)CaDiCaL version: 2.1.3 % 158.83/22.70 % (3430348)Termination reason: Instruction limit % 158.83/22.70 % (3430348)Termination phase: Saturation % 158.83/22.70 % (3430348)Time elapsed: 2.768 s % 158.83/22.70 % (3430348)Peak memory usage: 46 MB % 158.83/22.70 % (3430348)Instructions burned: 5211 (million) % 158.83/22.70 % (3430362)ott-3_8_sil=64000:random_seed=3595121517:i=20139:bs=on_2940 on theBenchmark for (2940ds/20139Mi) % 158.83/22.70 % (3430358)Instruction limit reached! % 158.83/22.70 % (3430358)------------------------------ % 158.83/22.70 % (3430358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.83/22.70 % (3430358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.83/22.70 % (3430358)CaDiCaL version: 2.1.3 % 158.83/22.70 % (3430358)Termination reason: Instruction limit % 158.83/22.70 % (3430358)Termination phase: Saturation % 158.83/22.70 % (3430358)Time elapsed: 4.613 s % 158.83/22.70 % (3430358)Peak memory usage: 68 MB % 158.83/22.70 % (3430358)Instructions burned: 8174 (million) % 158.83/22.70 % (3430602)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3574783399:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 158.83/22.70 % (3430602)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.83/22.70 % (3430602)Terminated due to inappropriate strategy. % 158.83/22.70 % (3430602)------------------------------ % 158.83/22.70 % (3430602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.83/22.70 % (3430602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.83/22.70 % (3430602)CaDiCaL version: 2.1.3 % 158.83/22.70 % (3430602)Termination reason: Inappropriate % 158.83/22.70 % (3430602)Time elapsed: 0.020 s % 158.83/22.70 % (3430602)Peak memory usage: 12 MB % 158.83/22.70 % (3430602)Instructions burned: 43 (million) % 158.83/22.70 % (3430602)------------------------------ % 158.83/22.70 % (3430602)------------------------------ % 158.83/22.70 % (3430614)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1504348046:i=11404_2917 on theBenchmark for (2917ds/11404Mi) % 158.83/22.70 % (3430360)Instruction limit reached! % 158.83/22.70 % (3430360)------------------------------ % 158.83/22.70 % (3430360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.83/22.70 % (3430360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.83/22.70 % (3430360)CaDiCaL version: 2.1.3 % 158.83/22.70 % (3430360)Termination reason: Instruction limit % 158.83/22.70 % (3430360)Termination phase: Saturation % 158.83/22.70 % (3430360)Time elapsed: 4.823 s % 158.83/22.70 % (3430360)Peak memory usage: 53 MB % 158.83/22.70 % (3430360)Instructions burned: 9155 (million) % 158.83/22.70 % (3430658)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1392777371:i=14134_2903 on theBenchmark for (2903ds/14134Mi) % 158.83/22.70 % (3430356)Instruction limit reached! % 158.83/22.70 % (3430356)------------------------------ % 158.83/22.70 % (3430356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.83/22.70 % (3430356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.83/22.70 % (3430356)CaDiCaL version: 2.1.3 % 158.83/22.70 % (3430356)Termination reason: Instruction limit % 158.83/22.70 % (3430356)Termination phase: Saturation % 158.83/22.70 % (3430356)Time elapsed: 8.873 s % 158.83/22.70 % (3430356)Peak memory usage: 84 MB % 158.83/22.70 % (3430356)Instructions burned: 22567 (million) % 158.83/22.70 % (3430686)dis+33_16_sil=32000:sac=on:random_seed=2624939870:i=15851:nm=0_2878 on theBenchmark for (2878ds/15851Mi) % 158.83/22.70 % (3430686)Instruction limit reached! % 158.83/22.70 % (3430686)------------------------------ % 158.83/22.70 % (3430686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.20/27.35 % (3430686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.20/27.35 % (3430686)CaDiCaL version: 2.1.3 % 192.20/27.35 % (3430686)Termination reason: Instruction limit % 192.20/27.35 % (3430686)Termination phase: Saturation % 192.20/27.35 % (3430686)Time elapsed: 5.882 s % 192.20/27.35 % (3430686)Peak memory usage: 19 MB % 192.20/27.35 % (3430686)Instructions burned: 15853 (million) % 192.20/27.35 % (3430710)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2724383332:avsq=on:i=17627:add=on:amm=off_2819 on theBenchmark for (2819ds/17627Mi) % 192.20/27.35 % (3430614)Instruction limit reached! % 192.20/27.35 % (3430614)------------------------------ % 192.20/27.35 % (3430614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.20/27.35 % (3430614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.20/27.35 % (3430614)CaDiCaL version: 2.1.3 % 192.20/27.35 % (3430614)Termination reason: Instruction limit % 192.20/27.35 % (3430614)Termination phase: Saturation % 192.20/27.35 % (3430614)Time elapsed: 10.679 s % 192.20/27.35 % (3430614)Peak memory usage: 81 MB % 192.20/27.35 % (3430614)Instructions burned: 11405 (million) % 192.20/27.35 % (3430713)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=784403950:s2a=on:i=53295_2810 on theBenchmark for (2810ds/53295Mi) % 192.20/27.35 % (3430362)Instruction limit reached! % 192.20/27.35 % (3430362)------------------------------ % 192.20/27.35 % (3430362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.20/27.35 % (3430362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.20/27.35 % (3430362)CaDiCaL version: 2.1.3 % 192.20/27.35 % (3430362)Termination reason: Instruction limit % 192.20/27.35 % (3430362)Termination phase: Saturation % 192.20/27.35 % (3430362)Time elapsed: 13.313 s % 192.20/27.35 % (3430362)Peak memory usage: 58 MB % 192.20/27.35 % (3430362)Instructions burned: 20139 (million) % 192.20/27.35 % (3430716)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2743708766:i=26857:ins=20_2807 on theBenchmark for (2807ds/26857Mi) % 192.20/27.35 % (3430716)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.20/27.35 % (3430716)Terminated due to inappropriate strategy. % 192.20/27.35 % (3430716)------------------------------ % 192.20/27.35 % (3430716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.20/27.35 % (3430716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.20/27.35 % (3430716)CaDiCaL version: 2.1.3 % 192.20/27.35 % (3430716)Termination reason: Inappropriate % 192.20/27.35 % (3430716)Time elapsed: 0.038 s % 192.20/27.35 % (3430716)Peak memory usage: 11 MB % 192.20/27.35 % (3430716)Instructions burned: 43 (million) % 192.20/27.35 % (3430716)------------------------------ % 192.20/27.35 % (3430716)------------------------------ % 192.20/27.35 % (3430718)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=887448776:i=28120:bs=on:fsr=off_2806 on theBenchmark for (2806ds/28120Mi) % 192.20/27.35 % (3430346)Instruction limit reached! % 192.20/27.35 % (3430346)------------------------------ % 192.20/27.35 % (3430346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.20/27.35 % (3430346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.20/27.35 % (3430346)CaDiCaL version: 2.1.3 % 192.20/27.35 % (3430346)Termination reason: Instruction limit % 192.20/27.35 % (3430346)Termination phase: Saturation % 192.20/27.35 % (3430346)Time elapsed: 19.242 s % 192.20/27.35 % (3430346)Peak memory usage: 50 MB % 192.20/27.35 % (3430346)Instructions burned: 29340 (million) % 192.20/27.35 % (3430722)fmb+10_1_sil=256000:fmbss=7:random_seed=668685793:fmbsr=1.6:i=182295_2780 on theBenchmark for (2780ds/182295Mi) % 192.20/27.35 % (3430722)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.20/27.35 % (3430722)Terminated due to inappropriate strategy. % 192.20/27.35 % (3430722)------------------------------ % 192.20/27.35 % (3430722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.20/27.35 % (3430722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.20/27.35 % (3430722)CaDiCaL version: 2.1.3 % 192.20/27.35 % (3430722)Termination reason: Inappropriate % 192.20/27.35 % (3430722)Time elapsed: 0.045 s % 192.20/27.35 % (3430722)Peak memory usage: 11 MB % 192.20/27.35 % (3430722)Instructions burned: 43 (million) % 192.20/27.35 % (3430722)------------------------------ % 192.20/27.35 % (3430722)------------------------------ % 192.20/27.35 % (3430724)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2003910465:i=44625:gsp=on_2779 on theBenchmark for (2779ds/44625Mi) % 213.50/30.38 % (3430724)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.50/30.38 % (3430724)Terminated due to inappropriate strategy. % 213.50/30.38 % (3430724)------------------------------ % 213.50/30.38 % (3430724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.50/30.38 % (3430724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.50/30.38 % (3430724)CaDiCaL version: 2.1.3 % 213.50/30.38 % (3430724)Termination reason: Inappropriate % 213.50/30.38 % (3430724)Time elapsed: 0.041 s % 213.50/30.38 % (3430724)Peak memory usage: 11 MB % 213.50/30.38 % (3430724)Instructions burned: 42 (million) % 213.50/30.38 % (3430724)------------------------------ % 213.50/30.38 % (3430724)------------------------------ % 213.50/30.38 % (3430726)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=825133838:i=160505_2778 on theBenchmark for (2778ds/160505Mi) % 213.50/30.38 % (3430726)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.50/30.38 % (3430726)Terminated due to inappropriate strategy. % 213.50/30.38 % (3430726)------------------------------ % 213.50/30.38 % (3430726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.50/30.38 % (3430726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.50/30.38 % (3430726)CaDiCaL version: 2.1.3 % 213.50/30.38 % (3430726)Termination reason: Inappropriate % 213.50/30.38 % (3430726)Time elapsed: 0.043 s % 213.50/30.38 % (3430726)Peak memory usage: 11 MB % 213.50/30.38 % (3430726)Instructions burned: 43 (million) % 213.50/30.38 % (3430726)------------------------------ % 213.50/30.38 % (3430726)------------------------------ % 213.50/30.38 % (3430728)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1086775940:fmbsr=1.3:i=225729_2778 on theBenchmark for (2778ds/225729Mi) % 213.50/30.38 % (3430728)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.50/30.38 % (3430728)Terminated due to inappropriate strategy. % 213.50/30.38 % (3430728)------------------------------ % 213.50/30.38 % (3430728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.50/30.38 % (3430728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.50/30.38 % (3430728)CaDiCaL version: 2.1.3 % 213.50/30.38 % (3430728)Termination reason: Inappropriate % 213.50/30.38 % (3430728)Time elapsed: 0.043 s % 213.50/30.38 % (3430728)Peak memory usage: 11 MB % 213.50/30.38 % (3430728)Instructions burned: 43 (million) % 213.50/30.38 % (3430728)------------------------------ % 213.50/30.38 % (3430728)------------------------------ % 213.50/30.38 % (3430730)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=836231772:fmbsr=2:i=185024:ins=7_2777 on theBenchmark for (2777ds/185024Mi) % 213.50/30.38 % (3430730)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.50/30.38 % (3430730)Terminated due to inappropriate strategy. % 213.50/30.38 % (3430730)------------------------------ % 213.50/30.38 % (3430730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.50/30.38 % (3430730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.50/30.38 % (3430730)CaDiCaL version: 2.1.3 % 213.50/30.38 % (3430730)Termination reason: Inappropriate % 213.50/30.38 % (3430730)Time elapsed: 0.040 s % 213.50/30.38 % (3430730)Peak memory usage: 11 MB % 213.50/30.38 % (3430730)Instructions burned: 43 (million) % 213.50/30.38 % (3430730)------------------------------ % 213.50/30.38 % (3430730)------------------------------ % 213.50/30.38 % (3430733)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3756204459:rtra=on_2776 on theBenchmark for (2776ds/0Mi) % 213.50/30.38 % (3430733)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.50/30.38 % (3430733)Terminated due to inappropriate strategy. % 213.50/30.38 % (3430733)------------------------------ % 213.50/30.38 % (3430733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.50/30.38 % (3430733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.50/30.38 % (3430733)CaDiCaL version: 2.1.3 % 213.50/30.38 % (3430733)Termination reason: Inappropriate % 213.50/30.38 % (3430733)Time elapsed: 0.034 s % 213.50/30.38 % (3430733)Peak memory usage: 12 MB % 213.50/30.38 % (3430733)Instructions burned: 47 (million) % 213.50/30.38 % (3430733)------------------------------ % 213.50/30.38 % (3430733)------------------------------ % 213.50/30.38 % (3430735)% WARNING: option uhcvi not known. % 213.50/30.38 % (3430735)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3550971141:i=271062:add=off:rtra=on:rawr=on_2775 on theBenchmark for (2775ds/271062Mi) % 252.65/35.81 % (3430658)Instruction limit reached! % 252.65/35.81 % (3430658)------------------------------ % 252.65/35.81 % (3430658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.65/35.81 % (3430658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.65/35.81 % (3430658)CaDiCaL version: 2.1.3 % 252.65/35.81 % (3430658)Termination reason: Instruction limit % 252.65/35.81 % (3430658)Termination phase: Saturation % 252.65/35.81 % (3430658)Time elapsed: 13.074 s % 252.65/35.81 % (3430658)Peak memory usage: 87 MB % 252.65/35.81 % (3430658)Instructions burned: 14135 (million) % 252.65/35.81 % (3430738)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2982360678:i=176048:add=on:rtra=on:rawr=on_2771 on theBenchmark for (2771ds/176048Mi) % 252.65/35.81 % (3430710)Instruction limit reached! % 252.65/35.81 % (3430710)------------------------------ % 252.65/35.81 % (3430710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.65/35.81 % (3430710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.65/35.81 % (3430710)CaDiCaL version: 2.1.3 % 252.65/35.81 % (3430710)Termination reason: Instruction limit % 252.65/35.81 % (3430710)Termination phase: Saturation % 252.65/35.81 % (3430710)Time elapsed: 8.043 s % 252.65/35.81 % (3430710)Peak memory usage: 195 MB % 252.65/35.81 % (3430710)Instructions burned: 17627 (million) % 252.65/35.81 % (3430741)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3380543323:i=206:fgj=on:rtra=on_2738 on theBenchmark for (2738ds/206Mi) % 252.65/35.81 % (3430741)Instruction limit reached! % 252.65/35.81 % (3430741)------------------------------ % 252.65/35.81 % (3430741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.65/35.81 % (3430741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.65/35.81 % (3430741)CaDiCaL version: 2.1.3 % 252.65/35.81 % (3430741)Termination reason: Instruction limit % 252.65/35.81 % (3430741)Termination phase: Saturation % 252.65/35.81 % (3430741)Time elapsed: 0.088 s % 252.65/35.81 % (3430741)Peak memory usage: 15 MB % 252.65/35.81 % (3430741)Instructions burned: 208 (million) % 252.65/35.81 % (3430744)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4130232769:i=232:rtra=on_2737 on theBenchmark for (2737ds/232Mi) % 252.65/35.81 % (3430744)Instruction limit reached! % 252.65/35.81 % (3430744)------------------------------ % 252.65/35.81 % (3430744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.65/35.81 % (3430744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.65/35.81 % (3430744)CaDiCaL version: 2.1.3 % 252.65/35.81 % (3430744)Termination reason: Instruction limit % 252.65/35.81 % (3430744)Termination phase: Saturation % 252.65/35.81 % (3430744)Time elapsed: 0.131 s % 252.65/35.81 % (3430744)Peak memory usage: 15 MB % 252.65/35.81 % (3430744)Instructions burned: 232 (million) % 252.65/35.81 % (3430747)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3905872648:i=262:rtra=on_2735 on theBenchmark for (2735ds/262Mi) % 252.65/35.81 % (3430747)Instruction limit reached! % 252.65/35.81 % (3430747)------------------------------ % 252.65/35.81 % (3430747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.65/35.81 % (3430747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.65/35.81 % (3430747)CaDiCaL version: 2.1.3 % 252.65/35.81 % (3430747)Termination reason: Instruction limit % 252.65/35.81 % (3430747)Termination phase: Saturation % 252.65/35.81 % (3430747)Time elapsed: 0.250 s % 252.65/35.81 % (3430747)Peak memory usage: 15 MB % 252.65/35.81 % (3430747)Instructions burned: 263 (million) % 252.65/35.81 % (3430750)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1601964296:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2732 on theBenchmark for (2732ds/318Mi) % 252.65/35.81 % (3430750)Instruction limit reached! % 252.65/35.81 % (3430750)------------------------------ % 252.65/35.81 % (3430750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.65/35.81 % (3430750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.65/35.81 % (3430750)CaDiCaL version: 2.1.3 % 252.65/35.81 % (3430750)Termination reason: Instruction limit % 252.65/35.81 % (3430750)Termination phase: Saturation % 252.65/35.81 % (3430750)Time elapsed: 0.351 s % 252.65/35.81 % (3430750)Peak memory usage: 15 MB % 252.65/35.81 % (3430750)Instructions burned: 318 (million) % 252.65/35.81 % (3430754)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1142870266:i=1428:nm=2:rtra=on_2729 on theBenchmark for (2729ds/1428Mi) % 297.71/42.16 % (3430754)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 297.71/42.16 % (3430754)Terminated due to inappropriate strategy. % 297.71/42.16 % (3430754)------------------------------ % 297.71/42.16 % (3430754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.71/42.16 % (3430754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.71/42.16 % (3430754)CaDiCaL version: 2.1.3 % 297.71/42.16 % (3430754)Termination reason: Inappropriate % 297.71/42.16 % (3430754)Time elapsed: 0.042 s % 297.71/42.16 % (3430754)Peak memory usage: 11 MB % 297.71/42.16 % (3430754)Instructions burned: 47 (million) % 297.71/42.16 % (3430754)------------------------------ % 297.71/42.16 % (3430754)------------------------------ % 297.71/42.16 % (3430756)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1726471739:i=262:bd=preordered:rtra=on:fsd=on_2728 on theBenchmark for (2728ds/262Mi) % 297.71/42.16 % (3430756)Instruction limit reached! % 297.71/42.16 % (3430756)------------------------------ % 297.71/42.16 % (3430756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.71/42.16 % (3430756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.71/42.16 % (3430756)CaDiCaL version: 2.1.3 % 297.71/42.16 % (3430756)Termination reason: Instruction limit % 297.71/42.16 % (3430756)Termination phase: Saturation % 297.71/42.16 % (3430756)Time elapsed: 0.253 s % 297.71/42.16 % (3430756)Peak memory usage: 16 MB % 297.71/42.16 % (3430756)Instructions burned: 263 (million) % 297.71/42.16 % (3430758)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=4120744771:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2725 on theBenchmark for (2725ds/1368Mi) % 297.71/42.16 % (3430758)Instruction limit reached! % 297.71/42.16 % (3430758)------------------------------ % 297.71/42.16 % (3430758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.71/42.16 % (3430758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.71/42.16 % (3430758)CaDiCaL version: 2.1.3 % 297.71/42.16 % (3430758)Termination reason: Instruction limit % 297.71/42.16 % (3430758)Termination phase: Saturation % 297.71/42.16 % (3430758)Time elapsed: 1.249 s % 297.71/42.16 % (3430758)Peak memory usage: 20 MB % 297.71/42.16 % (3430758)Instructions burned: 1368 (million) % 297.71/42.16 % (3430765)ott-21_1_sil=16000:si=on:fs=off:random_seed=164349676:i=360:av=off:fsr=off:rtra=on_2712 on theBenchmark for (2712ds/360Mi) % 297.71/42.16 % (3430765)Instruction limit reached! % 297.71/42.16 % (3430765)------------------------------ % 297.71/42.16 % (3430765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.71/42.16 % (3430765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.71/42.16 % (3430765)CaDiCaL version: 2.1.3 % 297.71/42.16 % (3430765)Termination reason: Instruction limit % 297.71/42.16 % (3430765)Termination phase: Saturation % 297.71/42.16 % (3430765)Time elapsed: 0.330 s % 297.71/42.16 % (3430765)Peak memory usage: 14 MB % 297.71/42.16 % (3430765)Instructions burned: 361 (million) % 297.71/42.16 % (3430768)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=675928247:i=954:bd=all:rtra=on_2709 on theBenchmark for (2709ds/954Mi) % 297.71/42.16 % (3430768)Instruction limit reached! % 297.71/42.16 % (3430768)------------------------------ % 297.71/42.16 % (3430768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.71/42.16 % (3430768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.71/42.16 % (3430768)CaDiCaL version: 2.1.3 % 297.71/42.16 % (3430768)Termination reason: Instruction limit % 297.71/42.16 % (3430768)Termination phase: Saturation % 297.71/42.16 % (3430768)Time elapsed: 0.944 s % 297.71/42.16 % (3430768)Peak memory usage: 18 MB % 297.71/42.16 % (3430768)Instructions burned: 954 (million) % 297.71/42.16 % (3430772)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3794042188:fmbsr=1.3:i=1730:ins=25:rtra=on_2699 on theBenchmark for (2699ds/1730Mi) % 297.71/42.16 % (3430772)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 297.71/42.16 % (3430772)Terminated due to inappropriate strategy. % 297.71/42.16 % (3430772)------------------------------ % 297.71/42.16 % (3430772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.71/42.16 % (3430772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.71/42.16 % (3430772)CaDiCaL version: 2.1.3 % 297.71/42.16 % (3430772)Termination reasTerminated % 300.63/42.63 % Vampire exiting % 300.63/42.64 Terminated %------------------------------------------------------------------------------