%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX090_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n006.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:46:28 PM UTC 2026 % Result : Timeout 300.08s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX090_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.18 % Computer : n006.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 15:00:10 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.00/0.81 % (4029298)Will run a generic schedule for satisfiability detection. % 4.00/0.81 % (4029305)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2621392426:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.00/0.81 % (4029304)% WARNING: option uhcvi not known. % 4.00/0.81 % (4029303)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2926785353_2999 on theBenchmark for (2999ds/0Mi) % 4.00/0.81 % (4029304)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2074996751:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.00/0.81 % (4029306)dis+10_1_sil=32000:sp=arity:random_seed=2566115671:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.00/0.81 % (4029309)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2118452260:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.00/0.81 % (4029307)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=289486478:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.00/0.81 % (4029308)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2519135917:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.00/0.81 % (4029303)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.00/0.81 % (4029303)Terminated due to inappropriate strategy. % 4.00/0.81 % (4029303)------------------------------ % 4.00/0.81 % (4029303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.00/0.81 % (4029303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.00/0.81 % (4029303)CaDiCaL version: 2.1.3 % 4.00/0.81 % (4029303)Termination reason: Inappropriate % 4.00/0.81 % (4029303)Time elapsed: 0.006 s % 4.00/0.81 % (4029303)Peak memory usage: 11 MB % 4.00/0.81 % (4029303)Instructions burned: 12 (million) % 4.00/0.81 % (4029303)------------------------------ % 4.00/0.81 % (4029303)------------------------------ % 4.00/0.81 % (4029317)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=139812127:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.00/0.81 % (4029317)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.00/0.81 % (4029317)Terminated due to inappropriate strategy. % 4.00/0.81 % (4029317)------------------------------ % 4.00/0.81 % (4029317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.00/0.81 % (4029317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.00/0.81 % (4029317)CaDiCaL version: 2.1.3 % 4.00/0.81 % (4029317)Termination reason: Inappropriate % 4.00/0.81 % (4029317)Time elapsed: 0.004 s % 4.00/0.81 % (4029317)Peak memory usage: 10 MB % 4.00/0.81 % (4029317)Instructions burned: 7 (million) % 4.00/0.81 % (4029317)------------------------------ % 4.00/0.81 % (4029317)------------------------------ % 4.00/0.81 % (4029319)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2019287939:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.00/0.81 % (4029306)Instruction limit reached! % 4.00/0.81 % (4029306)------------------------------ % 4.00/0.81 % (4029306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.00/0.81 % (4029306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.00/0.81 % (4029306)CaDiCaL version: 2.1.3 % 4.00/0.81 % (4029306)Termination reason: Instruction limit % 4.00/0.81 % (4029306)Termination phase: Saturation % 4.00/0.81 % (4029306)Time elapsed: 0.055 s % 4.00/0.81 % (4029306)Peak memory usage: 12 MB % 4.00/0.81 % (4029306)Instructions burned: 104 (million) % 4.00/0.81 % (4029307)Instruction limit reached! % 4.00/0.81 % (4029307)------------------------------ % 4.00/0.81 % (4029307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.00/0.81 % (4029307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.00/0.81 % (4029307)CaDiCaL version: 2.1.3 % 4.00/0.81 % (4029307)Termination reason: Instruction limit % 4.00/0.81 % (4029307)Termination phase: Saturation % 4.00/0.81 % (4029307)Time elapsed: 0.062 s % 4.00/0.81 % (4029307)Peak memory usage: 13 MB % 4.00/0.81 % (4029307)Instructions burned: 117 (million) % 4.00/0.81 % (4029308)Instruction limit reached! % 4.00/0.81 % (4029308)------------------------------ % 4.00/0.81 % (4029308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.00/0.81 % (4029308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.00/0.81 % (4029308)CaDiCaL version: 2.1.3 % 4.00/0.81 % (4029308)Termination reason: Instruction limit % 4.41/0.93 % (4029308)Termination phase: Saturation % 4.41/0.93 % (4029308)Time elapsed: 0.070 s % 4.41/0.93 % (4029308)Peak memory usage: 13 MB % 4.41/0.93 % (4029308)Instructions burned: 131 (million) % 4.41/0.93 % (4029321)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=4058067846:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.41/0.93 % (4029322)ott-21_1_sil=16000:fs=off:random_seed=2493483979:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 4.41/0.93 % (4029323)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=852033414:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 4.41/0.93 % (4029309)Instruction limit reached! % 4.41/0.93 % (4029309)------------------------------ % 4.41/0.93 % (4029309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.41/0.93 % (4029309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.41/0.93 % (4029309)CaDiCaL version: 2.1.3 % 4.41/0.93 % (4029309)Termination reason: Instruction limit % 4.41/0.93 % (4029309)Termination phase: Saturation % 4.41/0.93 % (4029309)Time elapsed: 0.102 s % 4.41/0.93 % (4029309)Peak memory usage: 15 MB % 4.41/0.93 % (4029309)Instructions burned: 160 (million) % 4.41/0.93 % (4029327)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1454494284:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.41/0.93 % (4029319)Instruction limit reached! % 4.41/0.93 % (4029319)------------------------------ % 4.41/0.93 % (4029319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.41/0.93 % (4029319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.41/0.93 % (4029319)CaDiCaL version: 2.1.3 % 4.41/0.93 % (4029319)Termination reason: Instruction limit % 4.41/0.93 % (4029319)Termination phase: Saturation % 4.41/0.93 % (4029319)Time elapsed: 0.073 s % 4.41/0.93 % (4029319)Peak memory usage: 13 MB % 4.41/0.93 % (4029319)Instructions burned: 132 (million) % 4.41/0.93 % (4029327)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.41/0.93 % (4029327)Terminated due to inappropriate strategy. % 4.41/0.93 % (4029327)------------------------------ % 4.41/0.93 % (4029327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.41/0.93 % (4029327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.41/0.93 % (4029327)CaDiCaL version: 2.1.3 % 4.41/0.93 % (4029327)Termination reason: Inappropriate % 4.41/0.93 % (4029327)Time elapsed: 0.003 s % 4.41/0.93 % (4029327)Peak memory usage: 10 MB % 4.41/0.93 % (4029327)Instructions burned: 5 (million) % 4.41/0.93 % (4029327)------------------------------ % 4.41/0.93 % (4029327)------------------------------ % 4.41/0.93 % (4029329)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2121438063:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.41/0.93 % (4029330)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2867685258:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.41/0.93 % (4029330)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.41/0.93 % (4029330)Terminated due to inappropriate strategy. % 4.41/0.93 % (4029330)------------------------------ % 4.41/0.93 % (4029330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.41/0.93 % (4029330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.41/0.93 % (4029330)CaDiCaL version: 2.1.3 % 4.41/0.93 % (4029330)Termination reason: Inappropriate % 4.41/0.93 % (4029330)Time elapsed: 0.004 s % 4.41/0.93 % (4029330)Peak memory usage: 10 MB % 4.41/0.93 % (4029330)Instructions burned: 6 (million) % 4.41/0.93 % (4029330)------------------------------ % 4.41/0.93 % (4029330)------------------------------ % 4.41/0.93 % (4029322)Instruction limit reached! % 4.41/0.93 % (4029322)------------------------------ % 4.41/0.93 % (4029322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.41/0.93 % (4029322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.41/0.93 % (4029322)CaDiCaL version: 2.1.3 % 4.41/0.93 % (4029322)Termination reason: Instruction limit % 4.41/0.93 % (4029322)Termination phase: Saturation % 4.41/0.93 % (4029322)Time elapsed: 0.085 s % 4.41/0.93 % (4029322)Peak memory usage: 12 MB % 4.41/0.93 % (4029322)Instructions burned: 181 (million) % 4.41/0.93 % (4029333)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=3264389347:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 18.76/2.90 % (4029334)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=138878093:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 18.76/2.90 % (4029323)Instruction limit reached! % 18.76/2.90 % (4029323)------------------------------ % 18.76/2.90 % (4029323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.76/2.90 % (4029323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.76/2.90 % (4029323)CaDiCaL version: 2.1.3 % 18.76/2.90 % (4029323)Termination reason: Instruction limit % 18.76/2.90 % (4029323)Termination phase: Saturation % 18.76/2.90 % (4029323)Time elapsed: 0.318 s % 18.76/2.90 % (4029323)Peak memory usage: 14 MB % 18.76/2.90 % (4029323)Instructions burned: 478 (million) % 18.76/2.90 % (4029337)fmb+10_1_sil=64000:random_seed=3381106961:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 18.76/2.90 % (4029337)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.76/2.90 % (4029337)Terminated due to inappropriate strategy. % 18.76/2.90 % (4029337)------------------------------ % 18.76/2.90 % (4029337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.76/2.90 % (4029337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.76/2.90 % (4029337)CaDiCaL version: 2.1.3 % 18.76/2.90 % (4029337)Termination reason: Inappropriate % 18.76/2.90 % (4029337)Time elapsed: 0.005 s % 18.76/2.90 % (4029337)Peak memory usage: 10 MB % 18.76/2.90 % (4029337)Instructions burned: 9 (million) % 18.76/2.90 % (4029337)------------------------------ % 18.76/2.90 % (4029337)------------------------------ % 18.76/2.90 % (4029321)Instruction limit reached! % 18.76/2.90 % (4029321)------------------------------ % 18.76/2.90 % (4029321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.76/2.90 % (4029321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.76/2.90 % (4029321)CaDiCaL version: 2.1.3 % 18.76/2.90 % (4029321)Termination reason: Instruction limit % 18.76/2.90 % (4029321)Termination phase: Saturation % 18.76/2.90 % (4029321)Time elapsed: 0.378 s % 18.76/2.90 % (4029321)Peak memory usage: 21 MB % 18.76/2.90 % (4029321)Instructions burned: 684 (million) % 18.76/2.90 % (4029339)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=843997503:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 18.76/2.90 % (4029339)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.76/2.90 % (4029339)Terminated due to inappropriate strategy. % 18.76/2.90 % (4029339)------------------------------ % 18.76/2.90 % (4029339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.76/2.90 % (4029339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.76/2.90 % (4029339)CaDiCaL version: 2.1.3 % 18.76/2.90 % (4029339)Termination reason: Inappropriate % 18.76/2.90 % (4029339)Time elapsed: 0.004 s % 18.76/2.90 % (4029339)Peak memory usage: 10 MB % 18.76/2.90 % (4029339)Instructions burned: 7 (million) % 18.76/2.90 % (4029339)------------------------------ % 18.76/2.90 % (4029339)------------------------------ % 18.76/2.90 % (4029341)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1845093349:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 18.76/2.90 % (4029341)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.76/2.90 % (4029341)Terminated due to inappropriate strategy. % 18.76/2.90 % (4029341)------------------------------ % 18.76/2.90 % (4029341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.76/2.90 % (4029341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.76/2.90 % (4029341)CaDiCaL version: 2.1.3 % 18.76/2.90 % (4029341)Termination reason: Inappropriate % 18.76/2.90 % (4029341)Time elapsed: 0.004 s % 18.76/2.90 % (4029341)Peak memory usage: 10 MB % 18.76/2.90 % (4029341)Instructions burned: 7 (million) % 18.76/2.90 % (4029342)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=24949539:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 18.76/2.90 % (4029341)------------------------------ % 18.76/2.90 % (4029341)------------------------------ % 18.76/2.90 % (4029345)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3502937635:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 18.76/2.90 % (4029329)Instruction limit reached! % 18.76/2.90 % (4029329)------------------------------ % 29.66/4.41 % (4029329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.66/4.41 % (4029329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.66/4.41 % (4029329)CaDiCaL version: 2.1.3 % 29.66/4.41 % (4029329)Termination reason: Instruction limit % 29.66/4.41 % (4029329)Termination phase: Saturation % 29.66/4.41 % (4029329)Time elapsed: 0.412 s % 29.66/4.41 % (4029329)Peak memory usage: 14 MB % 29.66/4.41 % (4029329)Instructions burned: 1181 (million) % 29.66/4.41 % (4029347)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1334887112:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 29.66/4.41 % (4029347)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.66/4.41 % (4029347)Terminated due to inappropriate strategy. % 29.66/4.41 % (4029347)------------------------------ % 29.66/4.41 % (4029347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.66/4.41 % (4029347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.66/4.41 % (4029347)CaDiCaL version: 2.1.3 % 29.66/4.41 % (4029347)Termination reason: Inappropriate % 29.66/4.41 % (4029347)Time elapsed: 0.006 s % 29.66/4.41 % (4029347)Peak memory usage: 11 MB % 29.66/4.41 % (4029347)Instructions burned: 12 (million) % 29.66/4.41 % (4029347)------------------------------ % 29.66/4.41 % (4029347)------------------------------ % 29.66/4.41 % (4029333)Instruction limit reached! % 29.66/4.41 % (4029333)------------------------------ % 29.66/4.41 % (4029333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.66/4.41 % (4029333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.66/4.41 % (4029333)CaDiCaL version: 2.1.3 % 29.66/4.41 % (4029333)Termination reason: Instruction limit % 29.66/4.41 % (4029333)Termination phase: Saturation % 29.66/4.41 % (4029333)Time elapsed: 0.415 s % 29.66/4.41 % (4029333)Peak memory usage: 19 MB % 29.66/4.41 % (4029333)Instructions burned: 693 (million) % 29.66/4.41 % (4029349)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2733460957:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 29.66/4.41 % (4029350)ott-2_1_sil=16000:newcnf=on:random_seed=401793968:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 29.66/4.41 % (4029349)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.66/4.41 % (4029349)Terminated due to inappropriate strategy. % 29.66/4.41 % (4029349)------------------------------ % 29.66/4.41 % (4029349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.66/4.41 % (4029349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.66/4.41 % (4029349)CaDiCaL version: 2.1.3 % 29.66/4.41 % (4029349)Termination reason: Inappropriate % 29.66/4.41 % (4029349)Time elapsed: 0.004 s % 29.66/4.41 % (4029349)Peak memory usage: 10 MB % 29.66/4.41 % (4029349)Instructions burned: 7 (million) % 29.66/4.41 % (4029349)------------------------------ % 29.66/4.41 % (4029349)------------------------------ % 29.66/4.41 % (4029353)ott+10_1_sil=32000:tgt=ground:random_seed=128970293:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 29.66/4.41 % (4029334)Instruction limit reached! % 29.66/4.41 % (4029334)------------------------------ % 29.66/4.41 % (4029334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.66/4.41 % (4029334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.66/4.41 % (4029334)CaDiCaL version: 2.1.3 % 29.66/4.41 % (4029334)Termination reason: Instruction limit % 29.66/4.41 % (4029334)Termination phase: Saturation % 29.66/4.41 % (4029334)Time elapsed: 0.464 s % 29.66/4.41 % (4029334)Peak memory usage: 19 MB % 29.66/4.41 % (4029334)Instructions burned: 879 (million) % 29.66/4.41 % (4029355)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=441537929:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 29.66/4.41 % (4029355)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.66/4.41 % (4029355)Terminated due to inappropriate strategy. % 29.66/4.41 % (4029355)------------------------------ % 29.66/4.41 % (4029355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.66/4.41 % (4029355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.66/4.41 % (4029355)CaDiCaL version: 2.1.3 % 29.66/4.41 % (4029355)Termination reason: Inappropriate % 29.66/4.41 % (4029355)Time elapsed: 0.006 s % 29.66/4.41 % (4029355)Peak memory usage: 11 MB % 29.66/4.41 % (4029355)Instructions burned: 12 (million) % 91.68/13.17 % (4029355)------------------------------ % 91.68/13.17 % (4029355)------------------------------ % 91.68/13.17 % (4029357)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=866824892:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 91.68/13.17 % (4029350)Instruction limit reached! % 91.68/13.17 % (4029350)------------------------------ % 91.68/13.17 % (4029350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.68/13.17 % (4029350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.68/13.17 % (4029350)CaDiCaL version: 2.1.3 % 91.68/13.17 % (4029350)Termination reason: Instruction limit % 91.68/13.17 % (4029350)Termination phase: Saturation % 91.68/13.17 % (4029350)Time elapsed: 0.496 s % 91.68/13.17 % (4029350)Peak memory usage: 20 MB % 91.68/13.17 % (4029350)Instructions burned: 870 (million) % 91.68/13.17 % (4029359)dis+21_1_sil=32000:sas=cadical:random_seed=1419136772:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 91.68/13.17 % (4029345)Instruction limit reached! % 91.68/13.17 % (4029345)------------------------------ % 91.68/13.17 % (4029345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.68/13.17 % (4029345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.68/13.17 % (4029345)CaDiCaL version: 2.1.3 % 91.68/13.17 % (4029345)Termination reason: Instruction limit % 91.68/13.17 % (4029345)Termination phase: Saturation % 91.68/13.17 % (4029345)Time elapsed: 0.858 s % 91.68/13.17 % (4029345)Peak memory usage: 30 MB % 91.68/13.17 % (4029345)Instructions burned: 1472 (million) % 91.68/13.17 % (4029361)ott+11_1_sil=16000:gs=on:random_seed=3368170904:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 91.68/13.17 % (4029357)Instruction limit reached! % 91.68/13.17 % (4029357)------------------------------ % 91.68/13.17 % (4029357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.68/13.17 % (4029357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.68/13.17 % (4029357)CaDiCaL version: 2.1.3 % 91.68/13.17 % (4029357)Termination reason: Instruction limit % 91.68/13.17 % (4029357)Termination phase: Saturation % 91.68/13.17 % (4029357)Time elapsed: 1.752 s % 91.68/13.17 % (4029357)Peak memory usage: 38 MB % 91.68/13.17 % (4029357)Instructions burned: 3512 (million) % 91.68/13.17 % (4029363)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3904724490:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi) % 91.68/13.17 % (4029363)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 91.68/13.17 % (4029363)Terminated due to inappropriate strategy. % 91.68/13.17 % (4029363)------------------------------ % 91.68/13.17 % (4029363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.68/13.17 % (4029363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.68/13.17 % (4029363)CaDiCaL version: 2.1.3 % 91.68/13.17 % (4029363)Termination reason: Inappropriate % 91.68/13.17 % (4029363)Time elapsed: 0.004 s % 91.68/13.17 % (4029363)Peak memory usage: 10 MB % 91.68/13.17 % (4029363)Instructions burned: 7 (million) % 91.68/13.17 % (4029363)------------------------------ % 91.68/13.17 % (4029363)------------------------------ % 91.68/13.17 % (4029365)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2954669624:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2974 on theBenchmark for (2974ds/4591Mi) % 91.68/13.17 % (4029361)Instruction limit reached! % 91.68/13.17 % (4029361)------------------------------ % 91.68/13.17 % (4029361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.68/13.17 % (4029361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.68/13.17 % (4029361)CaDiCaL version: 2.1.3 % 91.68/13.17 % (4029361)Termination reason: Instruction limit % 91.68/13.17 % (4029361)Termination phase: Saturation % 91.68/13.17 % (4029361)Time elapsed: 1.163 s % 91.68/13.17 % (4029361)Peak memory usage: 28 MB % 91.68/13.17 % (4029361)Instructions burned: 2251 (million) % 91.68/13.17 % (4029367)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=109115695:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 91.68/13.17 % (4029353)Instruction limit reached! % 91.68/13.17 % (4029353)------------------------------ % 91.68/13.17 % (4029353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.68/13.17 % (4029353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.68/13.17 % (4029353)CaDiCaL version: 2.1.3 % 91.68/13.17 % (4029353)Termination reason: Instruction limit % 116.15/16.63 % (4029353)Termination phase: Saturation % 116.15/16.63 % (4029353)Time elapsed: 2.026 s % 116.15/16.63 % (4029353)Peak memory usage: 26 MB % 116.15/16.63 % (4029353)Instructions burned: 5114 (million) % 116.15/16.63 % (4029369)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2699512516:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 116.15/16.63 % (4029359)Instruction limit reached! % 116.15/16.63 % (4029359)------------------------------ % 116.15/16.63 % (4029359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.15/16.63 % (4029359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.15/16.63 % (4029359)CaDiCaL version: 2.1.3 % 116.15/16.63 % (4029359)Termination reason: Instruction limit % 116.15/16.63 % (4029359)Termination phase: Saturation % 116.15/16.63 % (4029359)Time elapsed: 1.552 s % 116.15/16.63 % (4029359)Peak memory usage: 18 MB % 116.15/16.63 % (4029359)Instructions burned: 3774 (million) % 116.15/16.63 % (4029371)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3422642841:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi) % 116.15/16.63 % (4029371)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.15/16.63 % (4029371)Terminated due to inappropriate strategy. % 116.15/16.63 % (4029371)------------------------------ % 116.15/16.63 % (4029371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.15/16.63 % (4029371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.15/16.63 % (4029371)CaDiCaL version: 2.1.3 % 116.15/16.63 % (4029371)Termination reason: Inappropriate % 116.15/16.63 % (4029371)Time elapsed: 0.006 s % 116.15/16.63 % (4029371)Peak memory usage: 11 MB % 116.15/16.63 % (4029371)Instructions burned: 12 (million) % 116.15/16.63 % (4029371)------------------------------ % 116.15/16.63 % (4029371)------------------------------ % 116.15/16.63 % (4029373)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=509912441:fmbsr=2:i=46332_2972 on theBenchmark for (2972ds/46332Mi) % 116.15/16.63 % (4029373)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.15/16.63 % (4029373)Terminated due to inappropriate strategy. % 116.15/16.63 % (4029373)------------------------------ % 116.15/16.63 % (4029373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.15/16.63 % (4029373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.15/16.63 % (4029373)CaDiCaL version: 2.1.3 % 116.15/16.63 % (4029373)Termination reason: Inappropriate % 116.15/16.63 % (4029373)Time elapsed: 0.004 s % 116.15/16.63 % (4029373)Peak memory usage: 11 MB % 116.15/16.63 % (4029373)Instructions burned: 7 (million) % 116.15/16.63 % (4029373)------------------------------ % 116.15/16.63 % (4029373)------------------------------ % 116.15/16.63 % (4029375)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3371079414:i=14071_2972 on theBenchmark for (2972ds/14071Mi) % 116.15/16.63 % (4029375)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.15/16.63 % (4029375)Terminated due to inappropriate strategy. % 116.15/16.63 % (4029375)------------------------------ % 116.15/16.63 % (4029375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.15/16.63 % (4029375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.15/16.63 % (4029375)CaDiCaL version: 2.1.3 % 116.15/16.63 % (4029375)Termination reason: Inappropriate % 116.15/16.63 % (4029375)Time elapsed: 0.004 s % 116.15/16.63 % (4029375)Peak memory usage: 11 MB % 116.15/16.63 % (4029375)Instructions burned: 7 (million) % 116.15/16.63 % (4029375)------------------------------ % 116.15/16.63 % (4029375)------------------------------ % 116.15/16.63 % (4029377)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1141539807:i=22565:add=on:rawr=on_2972 on theBenchmark for (2972ds/22565Mi) % 116.15/16.63 % (4029342)Instruction limit reached! % 116.15/16.63 % (4029342)------------------------------ % 116.15/16.63 % (4029342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.15/16.63 % (4029342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.15/16.63 % (4029342)CaDiCaL version: 2.1.3 % 116.15/16.63 % (4029342)Termination reason: Instruction limit % 116.15/16.63 % (4029342)Termination phase: Saturation % 116.15/16.63 % (4029342)Time elapsed: 2.731 s % 116.15/16.63 % (4029342)Peak memory usage: 40 MB % 116.15/16.63 % (4029342)Instructions burned: 5132 (million) % 116.15/16.63 % (4029379)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=755699083:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 116.15/16.63 % (4029365)Instruction limit reached! % 116.80/16.77 % (4029365)------------------------------ % 116.80/16.77 % (4029365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.80/16.77 % (4029365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.80/16.77 % (4029365)CaDiCaL version: 2.1.3 % 116.80/16.77 % (4029365)Termination reason: Instruction limit % 116.80/16.77 % (4029365)Termination phase: Saturation % 116.80/16.77 % (4029365)Time elapsed: 1.658 s % 116.80/16.77 % (4029365)Peak memory usage: 32 MB % 116.80/16.77 % (4029365)Instructions burned: 4592 (million) % 116.80/16.77 % (4029381)dis+10_16:1_sil=16000:random_seed=3911821415:i=9155:fsr=off_2958 on theBenchmark for (2958ds/9155Mi) % 116.80/16.77 % (4029369)Instruction limit reached! % 116.80/16.77 % (4029369)------------------------------ % 116.80/16.77 % (4029369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.80/16.77 % (4029369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.80/16.77 % (4029369)CaDiCaL version: 2.1.3 % 116.80/16.77 % (4029369)Termination reason: Instruction limit % 116.80/16.77 % (4029369)Termination phase: Saturation % 116.80/16.77 % (4029369)Time elapsed: 2.352 s % 116.80/16.77 % (4029369)Peak memory usage: 33 MB % 116.80/16.77 % (4029369)Instructions burned: 5211 (million) % 116.80/16.77 % (4029383)ott-3_8_sil=64000:random_seed=1951806972:i=20139:bs=on_2949 on theBenchmark for (2949ds/20139Mi) % 116.80/16.77 % (4029379)Instruction limit reached! % 116.80/16.77 % (4029379)------------------------------ % 116.80/16.77 % (4029379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.80/16.77 % (4029379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.80/16.77 % (4029379)CaDiCaL version: 2.1.3 % 116.80/16.77 % (4029379)Termination reason: Instruction limit % 116.80/16.77 % (4029379)Termination phase: Saturation % 116.80/16.77 % (4029379)Time elapsed: 3.670 s % 116.80/16.77 % (4029379)Peak memory usage: 29 MB % 116.80/16.77 % (4029379)Instructions burned: 8174 (million) % 116.80/16.77 % (4029385)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3723227722:fmbsr=2:i=32576_2930 on theBenchmark for (2930ds/32576Mi) % 116.80/16.77 % (4029385)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.80/16.77 % (4029385)Terminated due to inappropriate strategy. % 116.80/16.77 % (4029385)------------------------------ % 116.80/16.77 % (4029385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.80/16.77 % (4029385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.80/16.77 % (4029385)CaDiCaL version: 2.1.3 % 116.80/16.77 % (4029385)Termination reason: Inappropriate % 116.80/16.77 % (4029385)Time elapsed: 0.006 s % 116.80/16.77 % (4029385)Peak memory usage: 11 MB % 116.80/16.77 % (4029385)Instructions burned: 12 (million) % 116.80/16.77 % (4029385)------------------------------ % 116.80/16.77 % (4029385)------------------------------ % 116.80/16.77 % (4029387)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1285423309:i=11404_2930 on theBenchmark for (2930ds/11404Mi) % 116.80/16.77 % (4029381)Instruction limit reached! % 116.80/16.77 % (4029381)------------------------------ % 116.80/16.77 % (4029381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.80/16.77 % (4029381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.80/16.77 % (4029381)CaDiCaL version: 2.1.3 % 116.80/16.77 % (4029381)Termination reason: Instruction limit % 116.80/16.77 % (4029381)Termination phase: Saturation % 116.80/16.77 % (4029381)Time elapsed: 3.080 s % 116.80/16.77 % (4029381)Peak memory usage: 19 MB % 116.80/16.77 % (4029381)Instructions burned: 9156 (million) % 116.80/16.77 % (4029389)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3036370779:i=14134_2927 on theBenchmark for (2927ds/14134Mi) % 116.80/16.77 % (4029387)Instruction limit reached! % 116.80/16.77 % (4029387)------------------------------ % 116.80/16.77 % (4029387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.80/16.77 % (4029387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.80/16.77 % (4029387)CaDiCaL version: 2.1.3 % 116.80/16.77 % (4029387)Termination reason: Instruction limit % 116.80/16.77 % (4029387)Termination phase: Saturation % 116.80/16.77 % (4029387)Time elapsed: 3.780 s % 116.80/16.77 % (4029387)Peak memory usage: 19 MB % 116.80/16.77 % (4029387)Instructions burned: 11405 (million) % 116.80/16.77 % (4029391)dis+33_16_sil=32000:sac=on:random_seed=3383099654:i=15851:nm=0_2892 on theBenchmark for (2892ds/15851Mi) % 116.80/16.77 % (4029383)Instruction limit reached! % 116.80/16.77 % (4029383)------------------------------ % 116.80/16.77 % (4029383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.13/26.31 % (4029383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.13/26.31 % (4029383)CaDiCaL version: 2.1.3 % 185.13/26.31 % (4029383)Termination reason: Instruction limit % 185.13/26.31 % (4029383)Termination phase: Saturation % 185.13/26.31 % (4029383)Time elapsed: 7.872 s % 185.13/26.31 % (4029383)Peak memory usage: 26 MB % 185.13/26.31 % (4029383)Instructions burned: 20141 (million) % 185.13/26.31 % (4029393)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3554809753:avsq=on:i=17627:add=on:amm=off_2870 on theBenchmark for (2870ds/17627Mi) % 185.13/26.31 % (4029377)Instruction limit reached! % 185.13/26.31 % (4029377)------------------------------ % 185.13/26.31 % (4029377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.13/26.31 % (4029377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.13/26.31 % (4029377)CaDiCaL version: 2.1.3 % 185.13/26.31 % (4029377)Termination reason: Instruction limit % 185.13/26.31 % (4029377)Termination phase: Saturation % 185.13/26.31 % (4029377)Time elapsed: 10.463 s % 185.13/26.31 % (4029377)Peak memory usage: 406 MB % 185.13/26.31 % (4029377)Instructions burned: 22566 (million) % 185.13/26.31 % (4029395)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3833947137:s2a=on:i=53295_2866 on theBenchmark for (2866ds/53295Mi) % 185.13/26.31 % (4029389)Instruction limit reached! % 185.13/26.31 % (4029389)------------------------------ % 185.13/26.31 % (4029389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.13/26.31 % (4029389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.13/26.31 % (4029389)CaDiCaL version: 2.1.3 % 185.13/26.31 % (4029389)Termination reason: Instruction limit % 185.13/26.31 % (4029389)Termination phase: Saturation % 185.13/26.31 % (4029389)Time elapsed: 8.903 s % 185.13/26.31 % (4029389)Peak memory usage: 71 MB % 185.13/26.31 % (4029389)Instructions burned: 14135 (million) % 185.13/26.31 % (4029746)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2019708747:i=26857:ins=20_2837 on theBenchmark for (2837ds/26857Mi) % 185.13/26.31 % (4029746)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.13/26.31 % (4029746)Terminated due to inappropriate strategy. % 185.13/26.31 % (4029746)------------------------------ % 185.13/26.31 % (4029746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.13/26.31 % (4029746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.13/26.31 % (4029746)CaDiCaL version: 2.1.3 % 185.13/26.31 % (4029746)Termination reason: Inappropriate % 185.13/26.31 % (4029746)Time elapsed: 0.004 s % 185.13/26.31 % (4029746)Peak memory usage: 10 MB % 185.13/26.31 % (4029746)Instructions burned: 7 (million) % 185.13/26.31 % (4029746)------------------------------ % 185.13/26.31 % (4029746)------------------------------ % 185.13/26.31 % (4029748)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2343556461:i=28120:bs=on:fsr=off_2837 on theBenchmark for (2837ds/28120Mi) % 185.13/26.31 % (4029367)Instruction limit reached! % 185.13/26.31 % (4029367)------------------------------ % 185.13/26.31 % (4029367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.13/26.31 % (4029367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.13/26.31 % (4029367)CaDiCaL version: 2.1.3 % 185.13/26.31 % (4029367)Termination reason: Instruction limit % 185.13/26.31 % (4029367)Termination phase: Saturation % 185.13/26.31 % (4029367)Time elapsed: 13.747 s % 185.13/26.31 % (4029367)Peak memory usage: 112 MB % 185.13/26.31 % (4029367)Instructions burned: 29340 (million) % 185.13/26.31 % (4029750)fmb+10_1_sil=256000:fmbss=7:random_seed=1443288685:fmbsr=1.6:i=182295_2836 on theBenchmark for (2836ds/182295Mi) % 185.13/26.31 % (4029750)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.13/26.31 % (4029750)Terminated due to inappropriate strategy. % 185.13/26.31 % (4029750)------------------------------ % 185.13/26.31 % (4029750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.13/26.31 % (4029750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.13/26.31 % (4029750)CaDiCaL version: 2.1.3 % 185.13/26.31 % (4029750)Termination reason: Inappropriate % 185.13/26.31 % (4029750)Time elapsed: 0.004 s % 185.13/26.31 % (4029750)Peak memory usage: 10 MB % 185.13/26.31 % (4029750)Instructions burned: 7 (million) % 185.13/26.31 % (4029750)------------------------------ % 185.13/26.31 % (4029750)------------------------------ % 185.13/26.31 % (4029752)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1201005257:i=44625:gsp=on_2836 on theBenchmark for (2836ds/44625Mi) % 191.91/27.30 % (4029752)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.91/27.30 % (4029752)Terminated due to inappropriate strategy. % 191.91/27.30 % (4029752)------------------------------ % 191.91/27.30 % (4029752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.91/27.30 % (4029752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.91/27.30 % (4029752)CaDiCaL version: 2.1.3 % 191.91/27.30 % (4029752)Termination reason: Inappropriate % 191.91/27.30 % (4029752)Time elapsed: 0.005 s % 191.91/27.30 % (4029752)Peak memory usage: 11 MB % 191.91/27.30 % (4029752)Instructions burned: 9 (million) % 191.91/27.30 % (4029752)------------------------------ % 191.91/27.30 % (4029752)------------------------------ % 191.91/27.30 % (4029754)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2515217885:i=160505_2835 on theBenchmark for (2835ds/160505Mi) % 191.91/27.30 % (4029754)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.91/27.30 % (4029754)Terminated due to inappropriate strategy. % 191.91/27.30 % (4029754)------------------------------ % 191.91/27.30 % (4029754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.91/27.30 % (4029754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.91/27.30 % (4029754)CaDiCaL version: 2.1.3 % 191.91/27.30 % (4029754)Termination reason: Inappropriate % 191.91/27.30 % (4029754)Time elapsed: 0.004 s % 191.91/27.30 % (4029754)Peak memory usage: 10 MB % 191.91/27.30 % (4029754)Instructions burned: 7 (million) % 191.91/27.30 % (4029754)------------------------------ % 191.91/27.30 % (4029754)------------------------------ % 191.91/27.30 % (4029756)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2427152184:fmbsr=1.3:i=225729_2835 on theBenchmark for (2835ds/225729Mi) % 191.91/27.30 % (4029756)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.91/27.30 % (4029756)Terminated due to inappropriate strategy. % 191.91/27.30 % (4029756)------------------------------ % 191.91/27.30 % (4029756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.91/27.30 % (4029756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.91/27.30 % (4029756)CaDiCaL version: 2.1.3 % 191.91/27.30 % (4029756)Termination reason: Inappropriate % 191.91/27.30 % (4029756)Time elapsed: 0.004 s % 191.91/27.30 % (4029756)Peak memory usage: 11 MB % 191.91/27.30 % (4029756)Instructions burned: 7 (million) % 191.91/27.30 % (4029756)------------------------------ % 191.91/27.30 % (4029756)------------------------------ % 191.91/27.30 % (4029758)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3432541870:fmbsr=2:i=185024:ins=7_2835 on theBenchmark for (2835ds/185024Mi) % 191.91/27.30 % (4029758)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.91/27.30 % (4029758)Terminated due to inappropriate strategy. % 191.91/27.30 % (4029758)------------------------------ % 191.91/27.30 % (4029758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.91/27.30 % (4029758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.91/27.30 % (4029758)CaDiCaL version: 2.1.3 % 191.91/27.30 % (4029758)Termination reason: Inappropriate % 191.91/27.30 % (4029758)Time elapsed: 0.004 s % 191.91/27.30 % (4029758)Peak memory usage: 11 MB % 191.91/27.30 % (4029758)Instructions burned: 7 (million) % 191.91/27.30 % (4029758)------------------------------ % 191.91/27.30 % (4029758)------------------------------ % 191.91/27.30 % (4029760)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3113860559:rtra=on_2834 on theBenchmark for (2834ds/0Mi) % 191.91/27.30 % (4029760)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.91/27.30 % (4029760)Terminated due to inappropriate strategy. % 191.91/27.30 % (4029760)------------------------------ % 191.91/27.30 % (4029760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.91/27.30 % (4029760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.91/27.30 % (4029760)CaDiCaL version: 2.1.3 % 191.91/27.30 % (4029760)Termination reason: Inappropriate % 191.91/27.30 % (4029760)Time elapsed: 0.007 s % 191.91/27.30 % (4029760)Peak memory usage: 11 MB % 191.91/27.30 % (4029760)Instructions burned: 12 (million) % 191.91/27.30 % (4029760)------------------------------ % 191.91/27.30 % (4029760)------------------------------ % 191.91/27.30 % (4029762)% WARNING: option uhcvi not known. % 191.91/27.30 % (4029762)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2951261713:i=271062:add=off:rtra=on:rawr=on_2834 on theBenchmark for (2834ds/271062Mi) % 194.49/27.88 % (4029391)Instruction limit reached! % 194.49/27.88 % (4029391)------------------------------ % 194.49/27.88 % (4029391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.49/27.88 % (4029391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.49/27.88 % (4029391)CaDiCaL version: 2.1.3 % 194.49/27.88 % (4029391)Termination reason: Instruction limit % 194.49/27.88 % (4029391)Termination phase: Saturation % 194.49/27.88 % (4029391)Time elapsed: 6.489 s % 194.49/27.88 % (4029391)Peak memory usage: 56 MB % 194.49/27.88 % (4029391)Instructions burned: 15852 (million) % 194.49/27.88 % (4029764)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2590314515:i=176048:add=on:rtra=on:rawr=on_2827 on theBenchmark for (2827ds/176048Mi) % 194.49/27.88 % (4029393)Instruction limit reached! % 194.49/27.88 % (4029393)------------------------------ % 194.49/27.88 % (4029393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.49/27.88 % (4029393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.49/27.88 % (4029393)CaDiCaL version: 2.1.3 % 194.49/27.88 % (4029393)Termination reason: Instruction limit % 194.49/27.88 % (4029393)Termination phase: Saturation % 194.49/27.88 % (4029393)Time elapsed: 12.423 s % 194.49/27.88 % (4029393)Peak memory usage: 97 MB % 194.49/27.88 % (4029393)Instructions burned: 17628 (million) % 194.49/27.88 % (4029767)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2018943767:i=206:fgj=on:rtra=on_2745 on theBenchmark for (2745ds/206Mi) % 194.49/27.88 % (4029767)Instruction limit reached! % 194.49/27.88 % (4029767)------------------------------ % 194.49/27.88 % (4029767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.49/27.88 % (4029767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.49/27.88 % (4029767)CaDiCaL version: 2.1.3 % 194.49/27.88 % (4029767)Termination reason: Instruction limit % 194.49/27.88 % (4029767)Termination phase: Saturation % 194.49/27.88 % (4029767)Time elapsed: 0.112 s % 194.49/27.88 % (4029767)Peak memory usage: 13 MB % 194.49/27.88 % (4029767)Instructions burned: 208 (million) % 194.49/27.88 % (4029769)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1012909669:i=232:rtra=on_2744 on theBenchmark for (2744ds/232Mi) % 194.49/27.88 % (4029769)Instruction limit reached! % 194.49/27.88 % (4029769)------------------------------ % 194.49/27.88 % (4029769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.49/27.88 % (4029769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.49/27.88 % (4029769)CaDiCaL version: 2.1.3 % 194.49/27.88 % (4029769)Termination reason: Instruction limit % 194.49/27.88 % (4029769)Termination phase: Saturation % 194.49/27.88 % (4029769)Time elapsed: 0.131 s % 194.49/27.88 % (4029769)Peak memory usage: 14 MB % 194.49/27.88 % (4029769)Instructions burned: 232 (million) % 194.49/27.88 % (4029771)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3745606552:i=262:rtra=on_2742 on theBenchmark for (2742ds/262Mi) % 194.49/27.88 % (4029771)Instruction limit reached! % 194.49/27.88 % (4029771)------------------------------ % 194.49/27.88 % (4029771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.49/27.88 % (4029771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.49/27.88 % (4029771)CaDiCaL version: 2.1.3 % 194.49/27.89 % (4029771)Termination reason: Instruction limit % 194.49/27.89 % (4029771)Termination phase: Saturation % 194.49/27.89 % (4029771)Time elapsed: 0.115 s % 194.49/27.89 % (4029771)Peak memory usage: 13 MB % 194.49/27.89 % (4029771)Instructions burned: 262 (million) % 194.49/27.89 % (4029773)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1665295879:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2741 on theBenchmark for (2741ds/318Mi) % 194.49/27.89 % (4029773)Instruction limit reached! % 194.49/27.89 % (4029773)------------------------------ % 194.49/27.89 % (4029773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.49/27.89 % (4029773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.49/27.89 % (4029773)CaDiCaL version: 2.1.3 % 194.49/27.89 % (4029773)Termination reason: Instruction limit % 194.49/27.89 % (4029773)Termination phase: Saturation % 194.49/27.89 % (4029773)Time elapsed: 0.203 s % 194.49/27.89 % (4029773)Peak memory usage: 15 MB % 194.49/27.89 % (4029773)Instructions burned: 318 (million) % 194.49/27.89 % (4029775)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2052448861:i=1428:nm=2:rtra=on_2739 on theBenchmark for (2739ds/1428Mi) % 199.99/28.44 % (4029775)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 199.99/28.44 % (4029775)Terminated due to inappropriate strategy. % 199.99/28.44 % (4029775)------------------------------ % 199.99/28.44 % (4029775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.99/28.44 % (4029775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.99/28.44 % (4029775)CaDiCaL version: 2.1.3 % 199.99/28.44 % (4029775)Termination reason: Inappropriate % 199.99/28.44 % (4029775)Time elapsed: 0.005 s % 199.99/28.44 % (4029775)Peak memory usage: 10 MB % 199.99/28.44 % (4029775)Instructions burned: 8 (million) % 199.99/28.44 % (4029775)------------------------------ % 199.99/28.44 % (4029775)------------------------------ % 199.99/28.44 % (4029777)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=516128636:i=262:bd=preordered:rtra=on:fsd=on_2738 on theBenchmark for (2738ds/262Mi) % 199.99/28.44 % (4029777)Instruction limit reached! % 199.99/28.44 % (4029777)------------------------------ % 199.99/28.44 % (4029777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.99/28.44 % (4029777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.99/28.44 % (4029777)CaDiCaL version: 2.1.3 % 199.99/28.44 % (4029777)Termination reason: Instruction limit % 199.99/28.44 % (4029777)Termination phase: Saturation % 199.99/28.44 % (4029777)Time elapsed: 0.150 s % 199.99/28.44 % (4029777)Peak memory usage: 13 MB % 199.99/28.44 % (4029777)Instructions burned: 263 (million) % 199.99/28.44 % (4029779)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=237327766:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2737 on theBenchmark for (2737ds/1368Mi) % 199.99/28.44 % (4029305)Instruction limit reached! % 199.99/28.44 % (4029305)------------------------------ % 199.99/28.44 % (4029305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.99/28.44 % (4029305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.99/28.44 % (4029305)CaDiCaL version: 2.1.3 % 199.99/28.44 % (4029305)Termination reason: Instruction limit % 199.99/28.44 % (4029305)Termination phase: Saturation % 199.99/28.44 % (4029305)Time elapsed: 26.439 s % 199.99/28.44 % (4029305)Peak memory usage: 2629 MB % 199.99/28.44 % (4029305)Instructions burned: 88025 (million) % 199.99/28.44 % (4029781)ott-21_1_sil=16000:si=on:fs=off:random_seed=995310689:i=360:av=off:fsr=off:rtra=on_2733 on theBenchmark for (2733ds/360Mi) % 199.99/28.44 % (4029781)Instruction limit reached! % 199.99/28.44 % (4029781)------------------------------ % 199.99/28.44 % (4029781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.99/28.44 % (4029781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.99/28.44 % (4029781)CaDiCaL version: 2.1.3 % 199.99/28.44 % (4029781)Termination reason: Instruction limit % 199.99/28.44 % (4029781)Termination phase: Saturation % 199.99/28.44 % (4029781)Time elapsed: 0.087 s % 199.99/28.44 % (4029781)Peak memory usage: 13 MB % 199.99/28.44 % (4029781)Instructions burned: 365 (million) % 199.99/28.44 % (4029783)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2574355211:i=954:bd=all:rtra=on_2732 on theBenchmark for (2732ds/954Mi) % 199.99/28.44 % (4029779)Instruction limit reached! % 199.99/28.44 % (4029779)------------------------------ % 199.99/28.44 % (4029779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.99/28.44 % (4029779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.99/28.44 % (4029779)CaDiCaL version: 2.1.3 % 199.99/28.44 % (4029779)Termination reason: Instruction limit % 199.99/28.44 % (4029779)Termination phase: Saturation % 199.99/28.44 % (4029779)Time elapsed: 0.763 s % 199.99/28.44 % (4029779)Peak memory usage: 22 MB % 199.99/28.44 % (4029779)Instructions burned: 1370 (million) % 199.99/28.44 % (4029785)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1075921518:fmbsr=1.3:i=1730:ins=25:rtra=on_2729 on theBenchmark for (2729ds/1730Mi) % 199.99/28.44 % (4029785)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 199.99/28.44 % (4029785)Terminated due to inappropriate strategy. % 199.99/28.44 % (4029785)------------------------------ % 199.99/28.44 % (4029785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.99/28.44 % (4029785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.99/28.44 % (4029785)CaDiCaL version: 2.1.3 % 199.99/28.44 % (4029785)Termination reason: Inappropriate % 227.71/32.37 % (4029785)Time elapsed: 0.003 s % 227.71/32.37 % (4029785)Peak memory usage: 10 MB % 227.71/32.37 % (4029785)Instructions burned: 5 (million) % 227.71/32.37 % (4029785)------------------------------ % 227.71/32.37 % (4029785)------------------------------ % 227.71/32.37 % (4029787)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1752977121:i=2358:rtra=on_2729 on theBenchmark for (2729ds/2358Mi) % 227.71/32.37 % (4029783)Instruction limit reached! % 227.71/32.37 % (4029783)------------------------------ % 227.71/32.37 % (4029783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.71/32.37 % (4029783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.71/32.37 % (4029783)CaDiCaL version: 2.1.3 % 227.71/32.37 % (4029783)Termination reason: Instruction limit % 227.71/32.37 % (4029783)Termination phase: Saturation % 227.71/32.37 % (4029783)Time elapsed: 0.347 s % 227.71/32.37 % (4029783)Peak memory usage: 18 MB % 227.71/32.37 % (4029783)Instructions burned: 954 (million) % 227.71/32.37 % (4029789)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2380017570:i=1778:ins=1:rtra=on_2728 on theBenchmark for (2728ds/1778Mi) % 227.71/32.37 % (4029789)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.71/32.37 % (4029789)Terminated due to inappropriate strategy. % 227.71/32.37 % (4029789)------------------------------ % 227.71/32.37 % (4029789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.71/32.37 % (4029789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.71/32.37 % (4029789)CaDiCaL version: 2.1.3 % 227.71/32.37 % (4029789)Termination reason: Inappropriate % 227.71/32.37 % (4029789)Time elapsed: 0.002 s % 227.71/32.37 % (4029789)Peak memory usage: 10 MB % 227.71/32.37 % (4029789)Instructions burned: 7 (million) % 227.71/32.37 % (4029789)------------------------------ % 227.71/32.37 % (4029789)------------------------------ % 227.71/32.37 % (4029791)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=1942623223:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2728 on theBenchmark for (2728ds/1384Mi) % 227.71/32.37 % (4029748)Instruction limit reached! % 227.71/32.37 % (4029748)------------------------------ % 227.71/32.37 % (4029748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.71/32.37 % (4029748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.71/32.37 % (4029748)CaDiCaL version: 2.1.3 % 227.71/32.37 % (4029748)Termination reason: Instruction limit % 227.71/32.37 % (4029748)Termination phase: Saturation % 227.71/32.37 % (4029748)Time elapsed: 10.942 s % 227.71/32.37 % (4029748)Peak memory usage: 27 MB % 227.71/32.37 % (4029748)Instructions burned: 28123 (million) % 227.71/32.37 % (4029793)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3230520453:i=1758:kws=inv_precedence:fsr=off:rtra=on_2727 on theBenchmark for (2727ds/1758Mi) % 227.71/32.37 % (4029791)Instruction limit reached! % 227.71/32.37 % (4029791)------------------------------ % 227.71/32.37 % (4029791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.71/32.37 % (4029791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.71/32.37 % (4029791)CaDiCaL version: 2.1.3 % 227.71/32.37 % (4029791)Termination reason: Instruction limit % 227.71/32.37 % (4029791)Termination phase: Saturation % 227.71/32.37 % (4029791)Time elapsed: 0.463 s % 227.71/32.37 % (4029791)Peak memory usage: 24 MB % 227.71/32.37 % (4029791)Instructions burned: 1384 (million) % 227.71/32.37 % (4029795)fmb+10_1_sil=64000:si=on:random_seed=1138335451:i=44122:nm=2:rtra=on:gsp=on_2723 on theBenchmark for (2723ds/44122Mi) % 227.71/32.37 % (4029795)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.71/32.37 % (4029795)Terminated due to inappropriate strategy. % 227.71/32.37 % (4029795)------------------------------ % 227.71/32.37 % (4029795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.71/32.37 % (4029795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.71/32.37 % (4029795)CaDiCaL version: 2.1.3 % 227.71/32.37 % (4029795)Termination reason: Inappropriate % 227.71/32.37 % (4029795)Time elapsed: 0.003 s % 227.71/32.37 % (4029795)Peak memory usage: 10 MB % 227.71/32.37 % (4029795)Instructions burned: 10 (million) % 227.71/32.37 % (4029795)------------------------------ % 227.71/32.37 % (4029795)------------------------------ % 227.71/32.37 % (4029797)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1150399264:i=19030:nm=5:rtra=on_2723 on theBenchmark for (2723ds/19030Mi) % 269.07/38.13 % (4029797)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.07/38.13 % (4029797)Terminated due to inappropriate strategy. % 269.07/38.13 % (4029797)------------------------------ % 269.07/38.13 % (4029797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.07/38.13 % (4029797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.07/38.13 % (4029797)CaDiCaL version: 2.1.3 % 269.07/38.13 % (4029797)Termination reason: Inappropriate % 269.07/38.13 % (4029797)Time elapsed: 0.002 s % 269.07/38.13 % (4029797)Peak memory usage: 10 MB % 269.07/38.13 % (4029797)Instructions burned: 8 (million) % 269.07/38.13 % (4029797)------------------------------ % 269.07/38.13 % (4029797)------------------------------ % 269.07/38.13 % (4029799)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=958889904:fmbsr=1.7:i=1840:rtra=on_2723 on theBenchmark for (2723ds/1840Mi) % 269.07/38.13 % (4029799)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.07/38.13 % (4029799)Terminated due to inappropriate strategy. % 269.07/38.13 % (4029799)------------------------------ % 269.07/38.13 % (4029799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.07/38.13 % (4029799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.07/38.13 % (4029799)CaDiCaL version: 2.1.3 % 269.07/38.13 % (4029799)Termination reason: Inappropriate % 269.07/38.13 % (4029799)Time elapsed: 0.002 s % 269.07/38.13 % (4029799)Peak memory usage: 10 MB % 269.07/38.13 % (4029799)Instructions burned: 8 (million) % 269.07/38.13 % (4029799)------------------------------ % 269.07/38.13 % (4029799)------------------------------ % 269.07/38.13 % (4029801)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1345701638:i=10262:rtra=on_2723 on theBenchmark for (2723ds/10262Mi) % 269.07/38.13 % (4029787)Instruction limit reached! % 269.07/38.13 % (4029787)------------------------------ % 269.07/38.13 % (4029787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.07/38.13 % (4029787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.07/38.13 % (4029787)CaDiCaL version: 2.1.3 % 269.07/38.13 % (4029787)Termination reason: Instruction limit % 269.07/38.13 % (4029787)Termination phase: Saturation % 269.07/38.13 % (4029787)Time elapsed: 1.050 s % 269.07/38.13 % (4029787)Peak memory usage: 20 MB % 269.07/38.13 % (4029787)Instructions burned: 2359 (million) % 269.07/38.13 % (4029793)Instruction limit reached! % 269.07/38.13 % (4029793)------------------------------ % 269.07/38.13 % (4029793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.07/38.13 % (4029793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.07/38.13 % (4029793)CaDiCaL version: 2.1.3 % 269.07/38.13 % (4029793)Termination reason: Instruction limit % 269.07/38.13 % (4029793)Termination phase: Saturation % 269.07/38.13 % (4029793)Time elapsed: 0.927 s % 269.07/38.13 % (4029793)Peak memory usage: 24 MB % 269.07/38.13 % (4029793)Instructions burned: 1759 (million) % 269.07/38.13 % (4029803)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4261491863:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2718 on theBenchmark for (2718ds/2944Mi) % 269.07/38.13 % (4029804)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=82979335:i=12648:rtra=on_2718 on theBenchmark for (2718ds/12648Mi) % 269.07/38.13 % (4029804)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.07/38.13 % (4029804)Terminated due to inappropriate strategy. % 269.07/38.13 % (4029804)------------------------------ % 269.07/38.13 % (4029804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.07/38.13 % (4029804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.07/38.13 % (4029804)CaDiCaL version: 2.1.3 % 269.07/38.13 % (4029804)Termination reason: Inappropriate % 269.07/38.13 % (4029804)Time elapsed: 0.007 s % 269.07/38.13 % (4029804)Peak memory usage: 11 MB % 269.07/38.13 % (4029804)Instructions burned: 12 (million) % 269.07/38.13 % (4029804)------------------------------ % 269.07/38.13 % (4029804)------------------------------ % 269.07/38.13 % (4029807)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3673641838:fmbsr=2.30978:i=4348:rtra=on_2718 on theBenchmark for (2718ds/4348Mi) % 269.07/38.13 % (4029807)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.07/38.13 % (4029807)Terminated due to inappropriate strategy. % 269.07/38.13 % (4029807)------------------------------ % 269.07/38.13 % (402980Terminated % 300.08/42.54 % Vampire exiting % 300.08/42.54 Terminated %------------------------------------------------------------------------------