%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW053_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n018.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:38:48 PM UTC 2026 % Result : Timeout 301.35s 42.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW053_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.17 % Computer : n018.cluster.edu % 0.10/0.17 % Model : x86_64 x86_64 % 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.17 % Memory : 8046.5625MB % 0.10/0.17 % OS : Linux 6.8.0-71-generic % 0.10/0.17 % CPULimit : 300 % 0.10/0.17 % WCLimit : 300 % 0.10/0.17 % DateTime : Mon Sep 28 13:12:25 UTC 2026 % 0.10/0.17 % CPUTime : % 0.10/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.20 Running first-order model finding % 0.10/0.20 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.60/0.86 % (3375281)Will run a generic schedule for satisfiability detection. % 3.60/0.86 % (3375289)dis+10_1_sil=32000:sp=arity:random_seed=1622646996:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.60/0.86 % (3375287)% WARNING: option uhcvi not known. % 3.60/0.86 % (3375286)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4072994725_2999 on theBenchmark for (2999ds/0Mi) % 3.60/0.86 % (3375287)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1736414592:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.60/0.86 % (3375288)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1494082582:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.60/0.86 % (3375290)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2959626650:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.60/0.86 % (3375291)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=595238919:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.60/0.86 % (3375292)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3192066622:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.60/0.86 % (3375289)Instruction limit reached! % 3.60/0.86 % (3375289)------------------------------ % 3.60/0.86 % (3375289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.86 % (3375289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.86 % (3375289)CaDiCaL version: 2.1.3 % 3.60/0.86 % (3375289)Termination reason: Instruction limit % 3.60/0.86 % (3375289)Termination phase: Saturation % 3.60/0.86 % (3375289)Time elapsed: 0.024 s % 3.60/0.86 % (3375289)Peak memory usage: 14 MB % 3.60/0.86 % (3375289)Instructions burned: 106 (million) % 3.60/0.86 % (3375300)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=18607252:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.60/0.86 % (3375286)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.60/0.86 % (3375286)Terminated due to inappropriate strategy. % 3.60/0.86 % (3375286)------------------------------ % 3.60/0.86 % (3375286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.86 % (3375286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.86 % (3375286)CaDiCaL version: 2.1.3 % 3.60/0.86 % (3375286)Termination reason: Inappropriate % 3.60/0.86 % (3375286)Time elapsed: 0.038 s % 3.60/0.86 % (3375286)Peak memory usage: 13 MB % 3.60/0.86 % (3375286)Instructions burned: 87 (million) % 3.60/0.86 % (3375286)------------------------------ % 3.60/0.86 % (3375286)------------------------------ % 3.60/0.86 % (3375300)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.60/0.86 % (3375300)Terminated due to inappropriate strategy. % 3.60/0.86 % (3375300)------------------------------ % 3.60/0.86 % (3375300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.86 % (3375300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.86 % (3375300)CaDiCaL version: 2.1.3 % 3.60/0.86 % (3375300)Termination reason: Inappropriate % 3.60/0.86 % (3375300)Time elapsed: 0.020 s % 3.60/0.86 % (3375300)Peak memory usage: 13 MB % 3.60/0.86 % (3375300)Instructions burned: 86 (million) % 3.60/0.86 % (3375300)------------------------------ % 3.60/0.86 % (3375300)------------------------------ % 3.60/0.86 % (3375291)Instruction limit reached! % 3.60/0.86 % (3375291)------------------------------ % 3.60/0.86 % (3375291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.86 % (3375291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.86 % (3375291)CaDiCaL version: 2.1.3 % 3.60/0.86 % (3375291)Termination reason: Instruction limit % 3.60/0.86 % (3375291)Termination phase: Saturation % 3.60/0.86 % (3375291)Time elapsed: 0.057 s % 3.60/0.86 % (3375291)Peak memory usage: 15 MB % 3.60/0.86 % (3375291)Instructions burned: 140 (million) % 3.60/0.86 % (3375290)Instruction limit reached! % 3.60/0.86 % (3375290)------------------------------ % 3.60/0.86 % (3375290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.60/0.86 % (3375290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.60/0.86 % (3375290)CaDiCaL version: 2.1.3 % 3.60/0.86 % (3375290)Termination reason: Instruction limit % 3.60/0.86 % (3375290)Termination phase: Saturation % 3.60/0.86 % (3375290)Time elapsed: 0.057 s % 3.60/0.86 % (3375290)Peak memory usage: 15 MB % 3.60/0.86 % (3375290)Instructions burned: 126 (million) % 5.62/1.04 % (3375302)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3116607141:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 5.62/1.04 % (3375303)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=1914017001:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.62/1.04 % (3375292)Instruction limit reached! % 5.62/1.04 % (3375292)------------------------------ % 5.62/1.04 % (3375292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.62/1.04 % (3375292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.62/1.04 % (3375292)CaDiCaL version: 2.1.3 % 5.62/1.04 % (3375292)Termination reason: Instruction limit % 5.62/1.04 % (3375292)Termination phase: Saturation % 5.62/1.04 % (3375292)Time elapsed: 0.065 s % 5.62/1.04 % (3375292)Peak memory usage: 16 MB % 5.62/1.04 % (3375292)Instructions burned: 159 (million) % 5.62/1.04 % (3375304)ott-21_1_sil=16000:fs=off:random_seed=1859349219:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.62/1.04 % (3375305)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=989628853:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.62/1.04 % (3375308)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2438366183:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.62/1.04 % (3375302)Instruction limit reached! % 5.62/1.04 % (3375302)------------------------------ % 5.62/1.04 % (3375302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.62/1.04 % (3375302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.62/1.04 % (3375302)CaDiCaL version: 2.1.3 % 5.62/1.04 % (3375302)Termination reason: Instruction limit % 5.62/1.04 % (3375302)Termination phase: Saturation % 5.62/1.04 % (3375302)Time elapsed: 0.055 s % 5.62/1.04 % (3375302)Peak memory usage: 15 MB % 5.62/1.04 % (3375302)Instructions burned: 132 (million) % 5.62/1.04 % (3375308)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.62/1.04 % (3375308)Terminated due to inappropriate strategy. % 5.62/1.04 % (3375308)------------------------------ % 5.62/1.04 % (3375308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.62/1.04 % (3375308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.62/1.04 % (3375308)CaDiCaL version: 2.1.3 % 5.62/1.04 % (3375308)Termination reason: Inappropriate % 5.62/1.04 % (3375308)Time elapsed: 0.037 s % 5.62/1.04 % (3375308)Peak memory usage: 13 MB % 5.62/1.04 % (3375308)Instructions burned: 86 (million) % 5.62/1.04 % (3375308)------------------------------ % 5.62/1.04 % (3375308)------------------------------ % 5.62/1.04 % (3375312)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2368066696:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.62/1.04 % (3375313)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=10649003:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.62/1.04 % (3375304)Instruction limit reached! % 5.62/1.04 % (3375304)------------------------------ % 5.62/1.04 % (3375304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.62/1.04 % (3375304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.62/1.04 % (3375304)CaDiCaL version: 2.1.3 % 5.62/1.04 % (3375304)Termination reason: Instruction limit % 5.62/1.04 % (3375304)Termination phase: Saturation % 5.62/1.04 % (3375304)Time elapsed: 0.087 s % 5.62/1.04 % (3375304)Peak memory usage: 15 MB % 5.62/1.04 % (3375304)Instructions burned: 187 (million) % 5.62/1.04 % (3375316)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=2948472553: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.62/1.04 % (3375313)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.62/1.04 % (3375313)Terminated due to inappropriate strategy. % 5.62/1.04 % (3375313)------------------------------ % 5.62/1.04 % (3375313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.62/1.04 % (3375313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.62/1.04 % (3375313)CaDiCaL version: 2.1.3 % 5.62/1.04 % (3375313)Termination reason: Inappropriate % 5.62/1.04 % (3375313)Time elapsed: 0.051 s % 5.62/1.04 % (3375313)Peak memory usage: 15 MB % 16.95/2.83 % (3375313)Instructions burned: 119 (million) % 16.95/2.83 % (3375313)------------------------------ % 16.95/2.83 % (3375313)------------------------------ % 16.95/2.83 % (3375318)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3771671980:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 16.95/2.83 % (3375303)Instruction limit reached! % 16.95/2.83 % (3375303)------------------------------ % 16.95/2.83 % (3375303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.95/2.83 % (3375303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/2.83 % (3375303)CaDiCaL version: 2.1.3 % 16.95/2.83 % (3375303)Termination reason: Instruction limit % 16.95/2.83 % (3375303)Termination phase: Saturation % 16.95/2.83 % (3375303)Time elapsed: 0.178 s % 16.95/2.83 % (3375303)Peak memory usage: 20 MB % 16.95/2.83 % (3375303)Instructions burned: 686 (million) % 16.95/2.83 % (3375320)fmb+10_1_sil=64000:random_seed=2585920261:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 16.95/2.83 % (3375320)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.95/2.83 % (3375320)Terminated due to inappropriate strategy. % 16.95/2.83 % (3375320)------------------------------ % 16.95/2.83 % (3375320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.95/2.83 % (3375320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/2.83 % (3375320)CaDiCaL version: 2.1.3 % 16.95/2.83 % (3375320)Termination reason: Inappropriate % 16.95/2.83 % (3375320)Time elapsed: 0.022 s % 16.95/2.83 % (3375320)Peak memory usage: 13 MB % 16.95/2.83 % (3375320)Instructions burned: 95 (million) % 16.95/2.83 % (3375320)------------------------------ % 16.95/2.83 % (3375320)------------------------------ % 16.95/2.83 % (3375322)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=431298799:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 16.95/2.83 % (3375322)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.95/2.83 % (3375322)Terminated due to inappropriate strategy. % 16.95/2.83 % (3375322)------------------------------ % 16.95/2.83 % (3375322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.95/2.83 % (3375322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/2.83 % (3375322)CaDiCaL version: 2.1.3 % 16.95/2.83 % (3375322)Termination reason: Inappropriate % 16.95/2.83 % (3375322)Time elapsed: 0.019 s % 16.95/2.83 % (3375322)Peak memory usage: 14 MB % 16.95/2.83 % (3375322)Instructions burned: 87 (million) % 16.95/2.83 % (3375322)------------------------------ % 16.95/2.83 % (3375322)------------------------------ % 16.95/2.83 % (3375324)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1065499844:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 16.95/2.83 % (3375324)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.95/2.83 % (3375324)Terminated due to inappropriate strategy. % 16.95/2.83 % (3375324)------------------------------ % 16.95/2.83 % (3375324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.95/2.83 % (3375324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/2.83 % (3375324)CaDiCaL version: 2.1.3 % 16.95/2.83 % (3375324)Termination reason: Inappropriate % 16.95/2.83 % (3375324)Time elapsed: 0.019 s % 16.95/2.83 % (3375324)Peak memory usage: 13 MB % 16.95/2.83 % (3375324)Instructions burned: 86 (million) % 16.95/2.83 % (3375324)------------------------------ % 16.95/2.83 % (3375324)------------------------------ % 16.95/2.83 % (3375326)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=24127320:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 16.95/2.83 % (3375305)Instruction limit reached! % 16.95/2.83 % (3375305)------------------------------ % 16.95/2.83 % (3375305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.95/2.83 % (3375305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/2.83 % (3375305)CaDiCaL version: 2.1.3 % 16.95/2.83 % (3375305)Termination reason: Instruction limit % 16.95/2.83 % (3375305)Termination phase: Saturation % 16.95/2.83 % (3375305)Time elapsed: 0.271 s % 16.95/2.83 % (3375305)Peak memory usage: 17 MB % 16.95/2.83 % (3375305)Instructions burned: 478 (million) % 16.95/2.83 % (3375328)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2149894385:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 16.95/2.83 % (3375316)Instruction limit reached! % 16.95/2.83 % (3375316)------------------------------ % 21.47/3.39 % (3375316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.47/3.39 % (3375316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.47/3.39 % (3375316)CaDiCaL version: 2.1.3 % 21.47/3.39 % (3375316)Termination reason: Instruction limit % 21.47/3.39 % (3375316)Termination phase: Saturation % 21.47/3.39 % (3375316)Time elapsed: 0.403 s % 21.47/3.39 % (3375316)Peak memory usage: 22 MB % 21.47/3.39 % (3375316)Instructions burned: 693 (million) % 21.47/3.39 % (3375330)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2679605652:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 21.47/3.39 % (3375330)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.47/3.39 % (3375330)Terminated due to inappropriate strategy. % 21.47/3.39 % (3375330)------------------------------ % 21.47/3.39 % (3375330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.47/3.39 % (3375330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.47/3.39 % (3375330)CaDiCaL version: 2.1.3 % 21.47/3.39 % (3375330)Termination reason: Inappropriate % 21.47/3.39 % (3375330)Time elapsed: 0.037 s % 21.47/3.39 % (3375330)Peak memory usage: 13 MB % 21.47/3.39 % (3375330)Instructions burned: 87 (million) % 21.47/3.39 % (3375330)------------------------------ % 21.47/3.39 % (3375330)------------------------------ % 21.47/3.39 % (3375332)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1431755376:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 21.47/3.39 % (3375312)Instruction limit reached! % 21.47/3.39 % (3375312)------------------------------ % 21.47/3.39 % (3375312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.47/3.39 % (3375312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.47/3.39 % (3375312)CaDiCaL version: 2.1.3 % 21.47/3.39 % (3375312)Termination reason: Instruction limit % 21.47/3.39 % (3375312)Termination phase: Saturation % 21.47/3.39 % (3375312)Time elapsed: 0.533 s % 21.47/3.39 % (3375312)Peak memory usage: 19 MB % 21.47/3.39 % (3375312)Instructions burned: 1181 (million) % 21.47/3.39 % (3375334)ott-2_1_sil=16000:newcnf=on:random_seed=4259993316:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 21.47/3.39 % (3375332)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.47/3.39 % (3375332)Terminated due to inappropriate strategy. % 21.47/3.39 % (3375332)------------------------------ % 21.47/3.39 % (3375332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.47/3.39 % (3375332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.47/3.39 % (3375332)CaDiCaL version: 2.1.3 % 21.47/3.39 % (3375332)Termination reason: Inappropriate % 21.47/3.39 % (3375332)Time elapsed: 0.037 s % 21.47/3.39 % (3375332)Peak memory usage: 13 MB % 21.47/3.39 % (3375332)Instructions burned: 87 (million) % 21.47/3.39 % (3375332)------------------------------ % 21.47/3.39 % (3375332)------------------------------ % 21.47/3.39 % (3375318)Instruction limit reached! % 21.47/3.39 % (3375318)------------------------------ % 21.47/3.39 % (3375318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.47/3.39 % (3375318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.47/3.39 % (3375318)CaDiCaL version: 2.1.3 % 21.47/3.39 % (3375318)Termination reason: Instruction limit % 21.47/3.39 % (3375318)Termination phase: Saturation % 21.47/3.39 % (3375318)Time elapsed: 0.493 s % 21.47/3.39 % (3375318)Peak memory usage: 21 MB % 21.47/3.39 % (3375318)Instructions burned: 880 (million) % 21.47/3.39 % (3375336)ott+10_1_sil=32000:tgt=ground:random_seed=932258613:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 21.47/3.39 % (3375337)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4014095135:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 21.47/3.39 % (3375337)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.47/3.39 % (3375337)Terminated due to inappropriate strategy. % 21.47/3.39 % (3375337)------------------------------ % 21.47/3.39 % (3375337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.47/3.39 % (3375337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.47/3.39 % (3375337)CaDiCaL version: 2.1.3 % 21.47/3.39 % (3375337)Termination reason: Inappropriate % 21.47/3.39 % (3375337)Time elapsed: 0.037 s % 21.47/3.39 % (3375337)Peak memory usage: 13 MB % 21.47/3.39 % (3375337)Instructions burned: 87 (million) % 87.01/12.53 % (3375337)------------------------------ % 87.01/12.53 % (3375337)------------------------------ % 87.01/12.53 % (3375340)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3456927867:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 87.01/12.53 % (3375328)Instruction limit reached! % 87.01/12.53 % (3375328)------------------------------ % 87.01/12.53 % (3375328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.01/12.53 % (3375328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.01/12.53 % (3375328)CaDiCaL version: 2.1.3 % 87.01/12.53 % (3375328)Termination reason: Instruction limit % 87.01/12.53 % (3375328)Termination phase: Saturation % 87.01/12.53 % (3375328)Time elapsed: 0.519 s % 87.01/12.53 % (3375328)Peak memory usage: 17 MB % 87.01/12.53 % (3375328)Instructions burned: 1473 (million) % 87.01/12.53 % (3375342)dis+21_1_sil=32000:sas=cadical:random_seed=734199219:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 87.01/12.53 % (3375334)Instruction limit reached! % 87.01/12.53 % (3375334)------------------------------ % 87.01/12.53 % (3375334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.01/12.53 % (3375334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.01/12.53 % (3375334)CaDiCaL version: 2.1.3 % 87.01/12.53 % (3375334)Termination reason: Instruction limit % 87.01/12.53 % (3375334)Termination phase: Saturation % 87.01/12.53 % (3375334)Time elapsed: 0.452 s % 87.01/12.53 % (3375334)Peak memory usage: 20 MB % 87.01/12.53 % (3375334)Instructions burned: 869 (million) % 87.01/12.53 % (3375344)ott+11_1_sil=16000:gs=on:random_seed=1150660785:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 87.01/12.53 % (3375326)Instruction limit reached! % 87.01/12.53 % (3375326)------------------------------ % 87.01/12.53 % (3375326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.01/12.53 % (3375326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.01/12.53 % (3375326)CaDiCaL version: 2.1.3 % 87.01/12.53 % (3375326)Termination reason: Instruction limit % 87.01/12.53 % (3375326)Termination phase: Saturation % 87.01/12.53 % (3375326)Time elapsed: 1.441 s % 87.01/12.53 % (3375326)Peak memory usage: 44 MB % 87.01/12.53 % (3375326)Instructions burned: 5133 (million) % 87.01/12.53 % (3375346)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3200585558:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 87.01/12.53 % (3375346)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 87.01/12.53 % (3375346)Terminated due to inappropriate strategy. % 87.01/12.53 % (3375346)------------------------------ % 87.01/12.53 % (3375346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.01/12.53 % (3375346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.01/12.53 % (3375346)CaDiCaL version: 2.1.3 % 87.01/12.53 % (3375346)Termination reason: Inappropriate % 87.01/12.53 % (3375346)Time elapsed: 0.026 s % 87.01/12.53 % (3375346)Peak memory usage: 14 MB % 87.01/12.53 % (3375346)Instructions burned: 117 (million) % 87.01/12.53 % (3375346)------------------------------ % 87.01/12.53 % (3375346)------------------------------ % 87.01/12.53 % (3375348)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1114427300:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 87.01/12.53 % (3375344)Instruction limit reached! % 87.01/12.53 % (3375344)------------------------------ % 87.01/12.53 % (3375344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.01/12.53 % (3375344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.01/12.53 % (3375344)CaDiCaL version: 2.1.3 % 87.01/12.53 % (3375344)Termination reason: Instruction limit % 87.01/12.53 % (3375344)Termination phase: Saturation % 87.01/12.53 % (3375344)Time elapsed: 0.852 s % 87.01/12.53 % (3375344)Peak memory usage: 19 MB % 87.01/12.53 % (3375344)Instructions burned: 2252 (million) % 87.01/12.53 % (3375350)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4065249832:i=29340_2979 on theBenchmark for (2979ds/29340Mi) % 87.01/12.53 % (3375340)Instruction limit reached! % 87.01/12.53 % (3375340)------------------------------ % 87.01/12.53 % (3375340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.01/12.53 % (3375340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.01/12.53 % (3375340)CaDiCaL version: 2.1.3 % 87.01/12.53 % (3375340)Termination reason: Instruction limit % 116.09/16.63 % (3375340)Termination phase: Saturation % 116.09/16.63 % (3375340)Time elapsed: 1.770 s % 116.09/16.63 % (3375340)Peak memory usage: 30 MB % 116.09/16.63 % (3375340)Instructions burned: 3513 (million) % 116.09/16.63 % (3375342)Instruction limit reached! % 116.09/16.63 % (3375342)------------------------------ % 116.09/16.63 % (3375342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.09/16.63 % (3375342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.09/16.63 % (3375342)CaDiCaL version: 2.1.3 % 116.09/16.63 % (3375342)Termination reason: Instruction limit % 116.09/16.63 % (3375342)Termination phase: Saturation % 116.09/16.63 % (3375342)Time elapsed: 1.669 s % 116.09/16.63 % (3375342)Peak memory usage: 24 MB % 116.09/16.63 % (3375342)Instructions burned: 3775 (million) % 116.09/16.63 % (3375352)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=882751767:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 116.09/16.63 % (3375353)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3807567135:i=5497:nm=2_2973 on theBenchmark for (2973ds/5497Mi) % 116.09/16.63 % (3375353)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.09/16.63 % (3375353)Terminated due to inappropriate strategy. % 116.09/16.63 % (3375353)------------------------------ % 116.09/16.63 % (3375353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.09/16.63 % (3375353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.09/16.63 % (3375353)CaDiCaL version: 2.1.3 % 116.09/16.63 % (3375353)Termination reason: Inappropriate % 116.09/16.63 % (3375353)Time elapsed: 0.039 s % 116.09/16.63 % (3375353)Peak memory usage: 13 MB % 116.09/16.63 % (3375353)Instructions burned: 87 (million) % 116.09/16.63 % (3375353)------------------------------ % 116.09/16.63 % (3375353)------------------------------ % 116.09/16.63 % (3375356)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1028153171:fmbsr=2:i=46332_2972 on theBenchmark for (2972ds/46332Mi) % 116.09/16.63 % (3375356)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.09/16.63 % (3375356)Terminated due to inappropriate strategy. % 116.09/16.63 % (3375356)------------------------------ % 116.09/16.63 % (3375356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.09/16.63 % (3375356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.09/16.63 % (3375356)CaDiCaL version: 2.1.3 % 116.09/16.63 % (3375356)Termination reason: Inappropriate % 116.09/16.63 % (3375356)Time elapsed: 0.050 s % 116.09/16.63 % (3375356)Peak memory usage: 14 MB % 116.09/16.63 % (3375356)Instructions burned: 121 (million) % 116.09/16.63 % (3375356)------------------------------ % 116.09/16.63 % (3375356)------------------------------ % 116.09/16.63 % (3375358)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4060782252:i=14071_2972 on theBenchmark for (2972ds/14071Mi) % 116.09/16.63 % (3375358)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.09/16.63 % (3375358)Terminated due to inappropriate strategy. % 116.09/16.63 % (3375358)------------------------------ % 116.09/16.63 % (3375358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.09/16.63 % (3375358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.09/16.63 % (3375358)CaDiCaL version: 2.1.3 % 116.09/16.63 % (3375358)Termination reason: Inappropriate % 116.09/16.63 % (3375358)Time elapsed: 0.050 s % 116.09/16.63 % (3375358)Peak memory usage: 14 MB % 116.09/16.63 % (3375358)Instructions burned: 120 (million) % 116.09/16.63 % (3375358)------------------------------ % 116.09/16.63 % (3375358)------------------------------ % 116.09/16.63 % (3375360)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1779661911:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi) % 116.09/16.63 % (3375348)Instruction limit reached! % 116.09/16.63 % (3375348)------------------------------ % 116.09/16.63 % (3375348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.09/16.63 % (3375348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.09/16.63 % (3375348)CaDiCaL version: 2.1.3 % 116.09/16.63 % (3375348)Termination reason: Instruction limit % 116.09/16.63 % (3375348)Termination phase: Saturation % 116.09/16.63 % (3375348)Time elapsed: 1.259 s % 116.09/16.63 % (3375348)Peak memory usage: 46 MB % 116.09/16.63 % (3375348)Instructions burned: 4593 (million) % 116.09/16.63 % (3375362)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1790393839:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 118.23/16.97 % (3375336)Instruction limit reached! % 118.23/16.97 % (3375336)------------------------------ % 118.23/16.97 % (3375336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.23/16.97 % (3375336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.23/16.97 % (3375336)CaDiCaL version: 2.1.3 % 118.23/16.97 % (3375336)Termination reason: Instruction limit % 118.23/16.97 % (3375336)Termination phase: Saturation % 118.23/16.97 % (3375336)Time elapsed: 2.979 s % 118.23/16.97 % (3375336)Peak memory usage: 33 MB % 118.23/16.97 % (3375336)Instructions burned: 5115 (million) % 118.23/16.97 % (3375364)dis+10_16:1_sil=16000:random_seed=3697021789:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi) % 118.23/16.97 % (3375362)Instruction limit reached! % 118.23/16.97 % (3375362)------------------------------ % 118.23/16.97 % (3375362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.23/16.97 % (3375362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.23/16.97 % (3375362)CaDiCaL version: 2.1.3 % 118.23/16.97 % (3375362)Termination reason: Instruction limit % 118.23/16.97 % (3375362)Termination phase: Saturation % 118.23/16.97 % (3375362)Time elapsed: 1.857 s % 118.23/16.97 % (3375362)Peak memory usage: 36 MB % 118.23/16.97 % (3375362)Instructions burned: 8175 (million) % 118.23/16.97 % (3375366)ott-3_8_sil=64000:random_seed=3373028151:i=20139:bs=on_2949 on theBenchmark for (2949ds/20139Mi) % 118.23/16.97 % (3375352)Instruction limit reached! % 118.23/16.97 % (3375352)------------------------------ % 118.23/16.97 % (3375352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.23/16.97 % (3375352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.23/16.97 % (3375352)CaDiCaL version: 2.1.3 % 118.23/16.97 % (3375352)Termination reason: Instruction limit % 118.23/16.97 % (3375352)Termination phase: Saturation % 118.23/16.97 % (3375352)Time elapsed: 2.776 s % 118.23/16.97 % (3375352)Peak memory usage: 48 MB % 118.23/16.97 % (3375352)Instructions burned: 5211 (million) % 118.23/16.97 % (3375368)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1758636773:fmbsr=2:i=32576_2945 on theBenchmark for (2945ds/32576Mi) % 118.23/16.97 % (3375368)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 118.23/16.97 % (3375368)Terminated due to inappropriate strategy. % 118.23/16.97 % (3375368)------------------------------ % 118.23/16.97 % (3375368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.23/16.97 % (3375368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.23/16.97 % (3375368)CaDiCaL version: 2.1.3 % 118.23/16.97 % (3375368)Termination reason: Inappropriate % 118.23/16.97 % (3375368)Time elapsed: 0.048 s % 118.23/16.97 % (3375368)Peak memory usage: 14 MB % 118.23/16.97 % (3375368)Instructions burned: 117 (million) % 118.23/16.97 % (3375368)------------------------------ % 118.23/16.97 % (3375368)------------------------------ % 118.23/16.97 % (3375370)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2807873166:i=11404_2945 on theBenchmark for (2945ds/11404Mi) % 118.23/16.97 % (3375364)Instruction limit reached! % 118.23/16.97 % (3375364)------------------------------ % 118.23/16.97 % (3375364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.23/16.97 % (3375364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.23/16.97 % (3375364)CaDiCaL version: 2.1.3 % 118.23/16.97 % (3375364)Termination reason: Instruction limit % 118.23/16.97 % (3375364)Termination phase: Saturation % 118.23/16.97 % (3375364)Time elapsed: 4.705 s % 118.23/16.97 % (3375364)Peak memory usage: 55 MB % 118.23/16.97 % (3375364)Instructions burned: 9155 (million) % 118.23/16.97 % (3375372)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1321584192:i=14134_2914 on theBenchmark for (2914ds/14134Mi) % 118.23/16.97 % (3375366)Instruction limit reached! % 118.23/16.97 % (3375366)------------------------------ % 118.23/16.97 % (3375366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.23/16.97 % (3375366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.23/16.97 % (3375366)CaDiCaL version: 2.1.3 % 118.23/16.97 % (3375366)Termination reason: Instruction limit % 118.23/16.97 % (3375366)Termination phase: Saturation % 118.23/16.97 % (3375366)Time elapsed: 6.378 s % 118.23/16.97 % (3375366)Peak memory usage: 64 MB % 118.23/16.97 % (3375366)Instructions burned: 20141 (million) % 118.23/16.97 % (3375374)dis+33_16_sil=32000:sac=on:random_seed=1337680342:i=15851:nm=0_2885 on theBenchmark for (2885ds/15851Mi) % 118.23/16.97 % (3375360)Instruction limit reached! % 118.23/16.97 % (3375360)------------------------------ % 118.23/16.97 % (3375360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.99/21.85 % (3375360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.99/21.85 % (3375360)CaDiCaL version: 2.1.3 % 152.99/21.85 % (3375360)Termination reason: Instruction limit % 152.99/21.85 % (3375360)Termination phase: Saturation % 152.99/21.85 % (3375360)Time elapsed: 9.451 s % 152.99/21.85 % (3375360)Peak memory usage: 79 MB % 152.99/21.85 % (3375360)Instructions burned: 22568 (million) % 152.99/21.85 % (3375376)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=757144680:avsq=on:i=17627:add=on:amm=off_2876 on theBenchmark for (2876ds/17627Mi) % 152.99/21.85 % (3375370)Instruction limit reached! % 152.99/21.85 % (3375370)------------------------------ % 152.99/21.85 % (3375370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.99/21.85 % (3375370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.99/21.85 % (3375370)CaDiCaL version: 2.1.3 % 152.99/21.85 % (3375370)Termination reason: Instruction limit % 152.99/21.85 % (3375370)Termination phase: Saturation % 152.99/21.85 % (3375370)Time elapsed: 7.364 s % 152.99/21.85 % (3375370)Peak memory usage: 48 MB % 152.99/21.85 % (3375370)Instructions burned: 11405 (million) % 152.99/21.85 % (3375378)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2250427793:s2a=on:i=53295_2871 on theBenchmark for (2871ds/53295Mi) % 152.99/21.85 % (3375374)Instruction limit reached! % 152.99/21.85 % (3375374)------------------------------ % 152.99/21.85 % (3375374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.99/21.85 % (3375374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.99/21.85 % (3375374)CaDiCaL version: 2.1.3 % 152.99/21.85 % (3375374)Termination reason: Instruction limit % 152.99/21.85 % (3375374)Termination phase: Saturation % 152.99/21.85 % (3375374)Time elapsed: 3.889 s % 152.99/21.85 % (3375374)Peak memory usage: 34 MB % 152.99/21.85 % (3375374)Instructions burned: 15854 (million) % 152.99/21.85 % (3375677)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2588933324:i=26857:ins=20_2846 on theBenchmark for (2846ds/26857Mi) % 152.99/21.85 % (3375677)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 152.99/21.85 % (3375677)Terminated due to inappropriate strategy. % 152.99/21.85 % (3375677)------------------------------ % 152.99/21.85 % (3375677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.99/21.85 % (3375677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.99/21.85 % (3375677)CaDiCaL version: 2.1.3 % 152.99/21.85 % (3375677)Termination reason: Inappropriate % 152.99/21.85 % (3375677)Time elapsed: 0.020 s % 152.99/21.85 % (3375677)Peak memory usage: 13 MB % 152.99/21.85 % (3375677)Instructions burned: 87 (million) % 152.99/21.85 % (3375677)------------------------------ % 152.99/21.85 % (3375677)------------------------------ % 152.99/21.85 % (3375679)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2171148464:i=28120:bs=on:fsr=off_2846 on theBenchmark for (2846ds/28120Mi) % 152.99/21.85 % (3375350)Instruction limit reached! % 152.99/21.85 % (3375350)------------------------------ % 152.99/21.85 % (3375350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.99/21.85 % (3375350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.99/21.85 % (3375350)CaDiCaL version: 2.1.3 % 152.99/21.85 % (3375350)Termination reason: Instruction limit % 152.99/21.85 % (3375350)Termination phase: Saturation % 152.99/21.85 % (3375350)Time elapsed: 14.238 s % 152.99/21.85 % (3375350)Peak memory usage: 41 MB % 152.99/21.85 % (3375350)Instructions burned: 29340 (million) % 152.99/21.85 % (3375833)fmb+10_1_sil=256000:fmbss=7:random_seed=1315445984:fmbsr=1.6:i=182295_2836 on theBenchmark for (2836ds/182295Mi) % 152.99/21.85 % (3375833)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 152.99/21.85 % (3375833)Terminated due to inappropriate strategy. % 152.99/21.85 % (3375833)------------------------------ % 152.99/21.85 % (3375833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.99/21.85 % (3375833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.99/21.85 % (3375833)CaDiCaL version: 2.1.3 % 152.99/21.85 % (3375833)Termination reason: Inappropriate % 152.99/21.85 % (3375833)Time elapsed: 0.040 s % 152.99/21.85 % (3375833)Peak memory usage: 14 MB % 152.99/21.85 % (3375833)Instructions burned: 87 (million) % 152.99/21.85 % (3375833)------------------------------ % 152.99/21.85 % (3375833)------------------------------ % 152.99/21.85 % (3375835)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1328143490:i=44625:gsp=on_2835 on theBenchmark for (2835ds/44625Mi) % 160.12/22.83 % (3375835)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.12/22.83 % (3375835)Terminated due to inappropriate strategy. % 160.12/22.83 % (3375835)------------------------------ % 160.12/22.83 % (3375835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.12/22.83 % (3375835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.12/22.83 % (3375835)CaDiCaL version: 2.1.3 % 160.12/22.83 % (3375835)Termination reason: Inappropriate % 160.12/22.83 % (3375835)Time elapsed: 0.042 s % 160.12/22.83 % (3375835)Peak memory usage: 14 MB % 160.12/22.83 % (3375835)Instructions burned: 91 (million) % 160.12/22.83 % (3375835)------------------------------ % 160.12/22.83 % (3375835)------------------------------ % 160.12/22.83 % (3375837)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3105955718:i=160505_2835 on theBenchmark for (2835ds/160505Mi) % 160.12/22.83 % (3375837)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.12/22.83 % (3375837)Terminated due to inappropriate strategy. % 160.12/22.83 % (3375837)------------------------------ % 160.12/22.83 % (3375837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.12/22.83 % (3375837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.12/22.83 % (3375837)CaDiCaL version: 2.1.3 % 160.12/22.83 % (3375837)Termination reason: Inappropriate % 160.12/22.83 % (3375837)Time elapsed: 0.037 s % 160.12/22.83 % (3375837)Peak memory usage: 13 MB % 160.12/22.83 % (3375837)Instructions burned: 87 (million) % 160.12/22.83 % (3375837)------------------------------ % 160.12/22.83 % (3375837)------------------------------ % 160.12/22.83 % (3375839)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3979593305:fmbsr=1.3:i=225729_2834 on theBenchmark for (2834ds/225729Mi) % 160.12/22.83 % (3375839)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.12/22.83 % (3375839)Terminated due to inappropriate strategy. % 160.12/22.83 % (3375839)------------------------------ % 160.12/22.83 % (3375839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.12/22.83 % (3375839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.12/22.83 % (3375839)CaDiCaL version: 2.1.3 % 160.12/22.83 % (3375839)Termination reason: Inappropriate % 160.12/22.83 % (3375839)Time elapsed: 0.051 s % 160.12/22.83 % (3375839)Peak memory usage: 14 MB % 160.12/22.83 % (3375839)Instructions burned: 120 (million) % 160.12/22.83 % (3375839)------------------------------ % 160.12/22.83 % (3375839)------------------------------ % 160.12/22.83 % (3375841)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2721016334:fmbsr=2:i=185024:ins=7_2833 on theBenchmark for (2833ds/185024Mi) % 160.12/22.83 % (3375841)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.12/22.83 % (3375841)Terminated due to inappropriate strategy. % 160.12/22.83 % (3375841)------------------------------ % 160.12/22.83 % (3375841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.12/22.83 % (3375841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.12/22.83 % (3375841)CaDiCaL version: 2.1.3 % 160.12/22.83 % (3375841)Termination reason: Inappropriate % 160.12/22.83 % (3375841)Time elapsed: 0.051 s % 160.12/22.83 % (3375841)Peak memory usage: 14 MB % 160.12/22.83 % (3375841)Instructions burned: 121 (million) % 160.12/22.83 % (3375841)------------------------------ % 160.12/22.83 % (3375841)------------------------------ % 160.12/22.83 % (3375843)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2875966493:rtra=on_2833 on theBenchmark for (2833ds/0Mi) % 160.12/22.83 % (3375843)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 160.12/22.83 % (3375843)Terminated due to inappropriate strategy. % 160.12/22.83 % (3375843)------------------------------ % 160.12/22.83 % (3375843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.12/22.83 % (3375843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.12/22.83 % (3375843)CaDiCaL version: 2.1.3 % 160.12/22.83 % (3375843)Termination reason: Inappropriate % 160.12/22.83 % (3375843)Time elapsed: 0.049 s % 160.12/22.83 % (3375843)Peak memory usage: 15 MB % 160.12/22.83 % (3375843)Instructions burned: 101 (million) % 160.12/22.83 % (3375843)------------------------------ % 160.12/22.83 % (3375843)------------------------------ % 160.12/22.83 % (3375845)% WARNING: option uhcvi not known. % 160.12/22.83 % (3375845)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=116739950:i=271062:add=off:rtra=on:rawr=on_2832 on theBenchmark for (2832ds/271062Mi) % 171.46/24.48 % (3375372)Instruction limit reached! % 171.46/24.48 % (3375372)------------------------------ % 171.46/24.48 % (3375372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.46/24.48 % (3375372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.46/24.48 % (3375372)CaDiCaL version: 2.1.3 % 171.46/24.48 % (3375372)Termination reason: Instruction limit % 171.46/24.48 % (3375372)Termination phase: Saturation % 171.46/24.48 % (3375372)Time elapsed: 9.205 s % 171.46/24.48 % (3375372)Peak memory usage: 53 MB % 171.46/24.48 % (3375372)Instructions burned: 14134 (million) % 171.46/24.48 % (3375847)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1578160965:i=176048:add=on:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/176048Mi) % 171.46/24.48 % (3375679)Instruction limit reached! % 171.46/24.48 % (3375679)------------------------------ % 171.46/24.48 % (3375679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.46/24.48 % (3375679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.46/24.48 % (3375679)CaDiCaL version: 2.1.3 % 171.46/24.48 % (3375679)Termination reason: Instruction limit % 171.46/24.48 % (3375679)Termination phase: Saturation % 171.46/24.48 % (3375679)Time elapsed: 5.929 s % 171.46/24.48 % (3375679)Peak memory usage: 27 MB % 171.46/24.48 % (3375679)Instructions burned: 28121 (million) % 171.46/24.48 % (3375849)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3955306838:i=206:fgj=on:rtra=on_2786 on theBenchmark for (2786ds/206Mi) % 171.46/24.48 % (3375849)Instruction limit reached! % 171.46/24.48 % (3375849)------------------------------ % 171.46/24.48 % (3375849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.46/24.48 % (3375849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.46/24.48 % (3375849)CaDiCaL version: 2.1.3 % 171.46/24.48 % (3375849)Termination reason: Instruction limit % 171.46/24.48 % (3375849)Termination phase: Saturation % 171.46/24.48 % (3375849)Time elapsed: 0.057 s % 171.46/24.48 % (3375849)Peak memory usage: 17 MB % 171.46/24.48 % (3375849)Instructions burned: 206 (million) % 171.46/24.48 % (3375851)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2704954011:i=232:rtra=on_2786 on theBenchmark for (2786ds/232Mi) % 171.46/24.48 % (3375851)Instruction limit reached! % 171.46/24.48 % (3375851)------------------------------ % 171.46/24.48 % (3375851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.46/24.48 % (3375851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.46/24.48 % (3375851)CaDiCaL version: 2.1.3 % 171.46/24.48 % (3375851)Termination reason: Instruction limit % 171.46/24.48 % (3375851)Termination phase: Saturation % 171.46/24.48 % (3375851)Time elapsed: 0.061 s % 171.46/24.48 % (3375851)Peak memory usage: 17 MB % 171.46/24.48 % (3375851)Instructions burned: 234 (million) % 171.46/24.48 % (3375853)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3973180915:i=262:rtra=on_2785 on theBenchmark for (2785ds/262Mi) % 171.46/24.48 % (3375853)Instruction limit reached! % 171.46/24.48 % (3375853)------------------------------ % 171.46/24.48 % (3375853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.46/24.48 % (3375853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.46/24.48 % (3375853)CaDiCaL version: 2.1.3 % 171.46/24.48 % (3375853)Termination reason: Instruction limit % 171.46/24.48 % (3375853)Termination phase: Saturation % 171.46/24.48 % (3375853)Time elapsed: 0.066 s % 171.46/24.48 % (3375853)Peak memory usage: 17 MB % 171.46/24.48 % (3375853)Instructions burned: 266 (million) % 171.46/24.48 % (3375855)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2890250939:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2784 on theBenchmark for (2784ds/318Mi) % 171.46/24.48 % (3375855)Instruction limit reached! % 171.46/24.48 % (3375855)------------------------------ % 171.46/24.48 % (3375855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.46/24.48 % (3375855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.46/24.48 % (3375855)CaDiCaL version: 2.1.3 % 171.46/24.48 % (3375855)Termination reason: Instruction limit % 171.46/24.48 % (3375855)Termination phase: Saturation % 171.46/24.48 % (3375855)Time elapsed: 0.091 s % 171.46/24.48 % (3375855)Peak memory usage: 19 MB % 171.46/24.48 % (3375855)Instructions burned: 320 (million) % 171.46/24.48 % (3375857)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1376163886:i=1428:nm=2:rtra=on_2783 on theBenchmark for (2783ds/1428Mi) % 187.07/26.63 % (3375857)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.07/26.63 % (3375857)Terminated due to inappropriate strategy. % 187.07/26.63 % (3375857)------------------------------ % 187.07/26.63 % (3375857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.07/26.63 % (3375857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.07/26.63 % (3375857)CaDiCaL version: 2.1.3 % 187.07/26.63 % (3375857)Termination reason: Inappropriate % 187.07/26.63 % (3375857)Time elapsed: 0.026 s % 187.07/26.63 % (3375857)Peak memory usage: 15 MB % 187.07/26.63 % (3375857)Instructions burned: 101 (million) % 187.07/26.63 % (3375857)------------------------------ % 187.07/26.63 % (3375857)------------------------------ % 187.07/26.63 % (3375859)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3019919591:i=262:bd=preordered:rtra=on:fsd=on_2783 on theBenchmark for (2783ds/262Mi) % 187.07/26.63 % (3375859)Instruction limit reached! % 187.07/26.63 % (3375859)------------------------------ % 187.07/26.63 % (3375859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.07/26.63 % (3375859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.07/26.63 % (3375859)CaDiCaL version: 2.1.3 % 187.07/26.63 % (3375859)Termination reason: Instruction limit % 187.07/26.63 % (3375859)Termination phase: Saturation % 187.07/26.63 % (3375859)Time elapsed: 0.066 s % 187.07/26.63 % (3375859)Peak memory usage: 17 MB % 187.07/26.63 % (3375859)Instructions burned: 265 (million) % 187.07/26.63 % (3375861)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=3701044820:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2782 on theBenchmark for (2782ds/1368Mi) % 187.07/26.63 % (3375861)Instruction limit reached! % 187.07/26.63 % (3375861)------------------------------ % 187.07/26.63 % (3375861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.07/26.63 % (3375861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.07/26.63 % (3375861)CaDiCaL version: 2.1.3 % 187.07/26.63 % (3375861)Termination reason: Instruction limit % 187.07/26.63 % (3375861)Termination phase: Saturation % 187.07/26.63 % (3375861)Time elapsed: 0.376 s % 187.07/26.63 % (3375861)Peak memory usage: 23 MB % 187.07/26.63 % (3375861)Instructions burned: 1371 (million) % 187.07/26.63 % (3375863)ott-21_1_sil=16000:si=on:fs=off:random_seed=159278266:i=360:av=off:fsr=off:rtra=on_2778 on theBenchmark for (2778ds/360Mi) % 187.07/26.63 % (3375863)Instruction limit reached! % 187.07/26.63 % (3375863)------------------------------ % 187.07/26.63 % (3375863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.07/26.63 % (3375863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.07/26.63 % (3375863)CaDiCaL version: 2.1.3 % 187.07/26.63 % (3375863)Termination reason: Instruction limit % 187.07/26.63 % (3375863)Termination phase: Saturation % 187.07/26.63 % (3375863)Time elapsed: 0.097 s % 187.07/26.63 % (3375863)Peak memory usage: 17 MB % 187.07/26.63 % (3375863)Instructions burned: 362 (million) % 187.07/26.63 % (3375865)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1847731940:i=954:bd=all:rtra=on_2777 on theBenchmark for (2777ds/954Mi) % 187.07/26.63 % (3375865)Instruction limit reached! % 187.07/26.63 % (3375865)------------------------------ % 187.07/26.63 % (3375865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.07/26.63 % (3375865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.07/26.63 % (3375865)CaDiCaL version: 2.1.3 % 187.07/26.63 % (3375865)Termination reason: Instruction limit % 187.07/26.63 % (3375865)Termination phase: Saturation % 187.07/26.63 % (3375865)Time elapsed: 0.318 s % 187.07/26.63 % (3375865)Peak memory usage: 21 MB % 187.07/26.63 % (3375865)Instructions burned: 954 (million) % 187.07/26.63 % (3375867)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=515904321:fmbsr=1.3:i=1730:ins=25:rtra=on_2774 on theBenchmark for (2774ds/1730Mi) % 187.07/26.63 % (3375867)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.07/26.63 % (3375867)Terminated due to inappropriate strategy. % 187.07/26.63 % (3375867)------------------------------ % 187.07/26.63 % (3375867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.07/26.63 % (3375867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.07/26.63 % (3375867)CaDiCaL version: 2.1.3 % 187.07/26.63 % (3375867)Termination reason: Inappropriate % 233.96/33.29 % (3375867)Time elapsed: 0.026 s % 233.96/33.29 % (3375867)Peak memory usage: 15 MB % 233.96/33.29 % (3375867)Instructions burned: 100 (million) % 233.96/33.29 % (3375867)------------------------------ % 233.96/33.29 % (3375867)------------------------------ % 233.96/33.29 % (3375869)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=282824682:i=2358:rtra=on_2773 on theBenchmark for (2773ds/2358Mi) % 233.96/33.29 % (3375869)Instruction limit reached! % 233.96/33.29 % (3375869)------------------------------ % 233.96/33.29 % (3375869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.96/33.29 % (3375869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.96/33.29 % (3375869)CaDiCaL version: 2.1.3 % 233.96/33.29 % (3375869)Termination reason: Instruction limit % 233.96/33.29 % (3375869)Termination phase: Saturation % 233.96/33.29 % (3375869)Time elapsed: 0.581 s % 233.96/33.29 % (3375869)Peak memory usage: 22 MB % 233.96/33.29 % (3375869)Instructions burned: 2359 (million) % 233.96/33.29 % (3375871)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3478480018:i=1778:ins=1:rtra=on_2767 on theBenchmark for (2767ds/1778Mi) % 233.96/33.29 % (3375871)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 233.96/33.29 % (3375871)Terminated due to inappropriate strategy. % 233.96/33.29 % (3375871)------------------------------ % 233.96/33.29 % (3375871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.96/33.29 % (3375871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.96/33.29 % (3375871)CaDiCaL version: 2.1.3 % 233.96/33.29 % (3375871)Termination reason: Inappropriate % 233.96/33.29 % (3375871)Time elapsed: 0.036 s % 233.96/33.29 % (3375871)Peak memory usage: 17 MB % 233.96/33.29 % (3375871)Instructions burned: 134 (million) % 233.96/33.29 % (3375871)------------------------------ % 233.96/33.29 % (3375871)------------------------------ % 233.96/33.29 % (3375873)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2608864055:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2767 on theBenchmark for (2767ds/1384Mi) % 233.96/33.29 % (3375873)Instruction limit reached! % 233.96/33.29 % (3375873)------------------------------ % 233.96/33.29 % (3375873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.96/33.29 % (3375873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.96/33.29 % (3375873)CaDiCaL version: 2.1.3 % 233.96/33.29 % (3375873)Termination reason: Instruction limit % 233.96/33.29 % (3375873)Termination phase: Saturation % 233.96/33.29 % (3375873)Time elapsed: 0.342 s % 233.96/33.29 % (3375873)Peak memory usage: 21 MB % 233.96/33.29 % (3375873)Instructions burned: 1385 (million) % 233.96/33.29 % (3375875)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2017710195:i=1758:kws=inv_precedence:fsr=off:rtra=on_2763 on theBenchmark for (2763ds/1758Mi) % 233.96/33.29 % (3375875)Instruction limit reached! % 233.96/33.29 % (3375875)------------------------------ % 233.96/33.29 % (3375875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.96/33.29 % (3375875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.96/33.29 % (3375875)CaDiCaL version: 2.1.3 % 233.96/33.29 % (3375875)Termination reason: Instruction limit % 233.96/33.29 % (3375875)Termination phase: Saturation % 233.96/33.29 % (3375875)Time elapsed: 0.573 s % 233.96/33.29 % (3375875)Peak memory usage: 28 MB % 233.96/33.29 % (3375875)Instructions burned: 1759 (million) % 233.96/33.29 % (3375877)fmb+10_1_sil=64000:si=on:random_seed=3833280469:i=44122:nm=2:rtra=on:gsp=on_2757 on theBenchmark for (2757ds/44122Mi) % 233.96/33.29 % (3375877)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 233.96/33.29 % (3375877)Terminated due to inappropriate strategy. % 233.96/33.29 % (3375877)------------------------------ % 233.96/33.29 % (3375877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.96/33.29 % (3375877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.96/33.29 % (3375877)CaDiCaL version: 2.1.3 % 233.96/33.29 % (3375877)Termination reason: Inappropriate % 233.96/33.29 % (3375877)Time elapsed: 0.028 s % 233.96/33.29 % (3375877)Peak memory usage: 15 MB % 233.96/33.29 % (3375877)Instructions burned: 109 (million) % 233.96/33.29 % (3375877)------------------------------ % 233.96/33.29 % (3375877)------------------------------ % 233.96/33.29 % (3375879)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1009332839:i=19030:nm=5:rtra=on_2757 on theBenchmark for (2757ds/19030Mi) % 281.50/40.00 % (3375879)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 281.50/40.00 % (3375879)Terminated due to inappropriate strategy. % 281.50/40.00 % (3375879)------------------------------ % 281.50/40.00 % (3375879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.50/40.00 % (3375879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.50/40.00 % (3375879)CaDiCaL version: 2.1.3 % 281.50/40.00 % (3375879)Termination reason: Inappropriate % 281.50/40.00 % (3375879)Time elapsed: 0.026 s % 281.50/40.00 % (3375879)Peak memory usage: 15 MB % 281.50/40.00 % (3375879)Instructions burned: 101 (million) % 281.50/40.00 % (3375879)------------------------------ % 281.50/40.00 % (3375879)------------------------------ % 281.50/40.00 % (3375881)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2373736356:fmbsr=1.7:i=1840:rtra=on_2757 on theBenchmark for (2757ds/1840Mi) % 281.50/40.00 % (3375881)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 281.50/40.00 % (3375881)Terminated due to inappropriate strategy. % 281.50/40.00 % (3375881)------------------------------ % 281.50/40.00 % (3375881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.50/40.00 % (3375881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.50/40.00 % (3375881)CaDiCaL version: 2.1.3 % 281.50/40.00 % (3375881)Termination reason: Inappropriate % 281.50/40.00 % (3375881)Time elapsed: 0.026 s % 281.50/40.00 % (3375881)Peak memory usage: 15 MB % 281.50/40.00 % (3375881)Instructions burned: 101 (million) % 281.50/40.00 % (3375881)------------------------------ % 281.50/40.00 % (3375881)------------------------------ % 281.50/40.00 % (3375883)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2270641345:i=10262:rtra=on_2756 on theBenchmark for (2756ds/10262Mi) % 281.50/40.00 % (3375376)Instruction limit reached! % 281.50/40.00 % (3375376)------------------------------ % 281.50/40.00 % (3375376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.50/40.00 % (3375376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.50/40.00 % (3375376)CaDiCaL version: 2.1.3 % 281.50/40.00 % (3375376)Termination reason: Instruction limit % 281.50/40.00 % (3375376)Termination phase: Saturation % 281.50/40.00 % (3375376)Time elapsed: 12.191 s % 281.50/40.00 % (3375376)Peak memory usage: 263 MB % 281.50/40.00 % (3375376)Instructions burned: 17627 (million) % 281.50/40.00 % (3375885)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3352770857:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2754 on theBenchmark for (2754ds/2944Mi) % 281.50/40.00 % (3375885)Instruction limit reached! % 281.50/40.00 % (3375885)------------------------------ % 281.50/40.00 % (3375885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.50/40.00 % (3375885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.50/40.00 % (3375885)CaDiCaL version: 2.1.3 % 281.50/40.00 % (3375885)Termination reason: Instruction limit % 281.50/40.00 % (3375885)Termination phase: Saturation % 281.50/40.00 % (3375885)Time elapsed: 1.686 s % 281.50/40.00 % (3375885)Peak memory usage: 33 MB % 281.50/40.00 % (3375885)Instructions burned: 2945 (million) % 281.50/40.00 % (3375887)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=131373854:i=12648:rtra=on_2737 on theBenchmark for (2737ds/12648Mi) % 281.50/40.00 % (3375887)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 281.50/40.00 % (3375887)Terminated due to inappropriate strategy. % 281.50/40.00 % (3375887)------------------------------ % 281.50/40.00 % (3375887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.50/40.00 % (3375887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.50/40.00 % (3375887)CaDiCaL version: 2.1.3 % 281.50/40.00 % (3375887)Termination reason: Inappropriate % 281.50/40.00 % (3375887)Time elapsed: 0.049 s % 281.50/40.00 % (3375887)Peak memory usage: 15 MB % 281.50/40.00 % (3375887)Instructions burned: 101 (million) % 281.50/40.00 % (3375887)------------------------------ % 281.50/40.00 % (3375887)------------------------------ % 281.50/40.00 % (3375889)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2449900653:fmbsr=2.30978:i=4348:rtra=on_2736 on theBenchmark for (2736ds/4348Mi) % 281.50/40.00 % (3375889)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 281.50/40.00 % (3375889)Terminated due to inappropriate strategy. % 281.50/40.00 % (3375889)------------------------------ % 301.35/42.73 % (3375889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 301.35/42.73 % (3375889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.35/42.73 % (3375889)CaDiCaL version: 2.1.3 % 301.35/42.73 % (3375889)Termination reason: Inappropriate % 301.35/42.73 % (3375889)Time elapsed: 0.049 s % 301.35/42.73 % (3375889)Peak memory usage: 15 MB % 301.35/42.73 % (3375889)Instructions burned: 101 (million) % 301.35/42.73 % (3375889)------------------------------ % 301.35/42.73 % (3375889)------------------------------ % 301.35/42.73 % (3375891)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2071509852:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2735 on theBenchmark for (2735ds/1738Mi) % 301.35/42.73 % (3375891)Instruction limit reached! % 301.35/42.73 % (3375891)------------------------------ % 301.35/42.73 % (3375891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 301.35/42.73 % (3375891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.35/42.73 % (3375891)CaDiCaL version: 2.1.3 % 301.35/42.73 % (3375891)Termination reason: Instruction limit % 301.35/42.73 % (3375891)Termination phase: Saturation % 301.35/42.73 % (3375891)Time elapsed: 1.078 s % 301.35/42.73 % (3375891)Peak memory usage: 24 MB % 301.35/42.73 % (3375891)Instructions burned: 1739 (million) % 301.35/42.73 % (3375883)Instruction limit reached! % 301.35/42.73 % (3375883)------------------------------ % 301.35/42.73 % (3375883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 301.35/42.73 % (3375883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.35/42.73 % (3375883)CaDiCaL version: 2.1.3 % 301.35/42.73 % (3375883)Termination reason: Instruction limit % 301.35/42.73 % (3375883)Termination phase: Saturation % 301.35/42.73 % (3375883)Time elapsed: 3.180 s % 301.35/42.73 % (3375883)Peak memory usage: 71 MB % 301.35/42.73 % (3375883)Instructions burned: 10262 (million) % 301.35/42.73 % (3375893)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1216602258:i=10228:av=off:rtra=on_2724 on theBenchmark for (2724ds/10228Mi) % 301.35/42.73 % (3375894)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1327230088:i=108564:rtra=on_2724 on theBenchmark for (2724ds/108564Mi) % 301.35/42.73 % (3375894)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 301.35/42.73 % (3375894)Terminated due to inappropriate strategy. % 301.35/42.73 % (3375894)------------------------------ % 301.35/42.73 % (3375894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 301.35/42.73 % (3375894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.35/42.73 % (3375894)CaDiCaL version: 2.1.3 % 301.35/42.73 % (3375894)Termination reason: Inappropriate % 301.35/42.73 % (3375894)Time elapsed: 0.026 s % 301.35/42.73 % (3375894)Peak memory usage: 15 MB % 301.35/42.73 % (3375894)Instructions burned: 101 (million) % 301.35/42.73 % (3375894)------------------------------ % 301.35/42.73 % (3375894)------------------------------ % 301.35/42.73 % (3375897)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3768272937:i=7024:aac=none:rtra=on_2724 on theBenchmark for (2724ds/7024Mi) % 301.35/42.73 % (3375897)Instruction limit reached! % 301.35/42.73 % (3375897)------------------------------ % 301.35/42.73 % (3375897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 301.35/42.73 % (3375897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.35/42.73 % (3375897)CaDiCaL version: 2.1.3 % 301.35/42.73 % (3375897)Termination reason: Instruction limit % 301.35/42.73 % (3375897)Termination phase: Saturation % 301.35/42.73 % (3375897)Time elapsed: 2.238 s % 301.35/42.73 % (3375897)Peak memory usage: 48 MB % 301.35/42.73 % (3375897)Instructions burned: 7024 (million) % 301.35/42.73 % (3376161)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1985823039:i=7546:rtra=on:amm=off_2701 on theBenchmark for (2701ds/7546Mi) % 301.35/42.73 % (3376161)Instruction limit reached! % 301.35/42.73 % (3376161)------------------------------ % 301.35/42.73 % (3376161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 301.35/42.73 % (3376161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.35/42.73 % (3376161)CaDiCaL version: 2.1.3 % 301.35/42.73 % (3376161)Termination reason: Instruction limit % 301.35/42.73 % (3376161)Termination phase: Saturation % 301.35/42.73 % (3376161)Time elapsed: 3.224 s % 301.35/42.73 % (3376161)Peak memory usage: 26 MB % 301.35/42.73 % (3376161)Instructions burned: 7547 (million) % 301.35/42.73 % (3376350)ott+11_1_sil=16000:si=on:gs=on:random_seed=529827817:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr= % 301.35/42.73 Terminated % 301.35/42.73 % Vampire exiting %------------------------------------------------------------------------------