%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX133_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n009.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:32 PM UTC 2026 % Result : Timeout 295.33s 41.93s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX133_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 % Computer : n009.cluster.edu % 0.09/0.22 % Model : x86_64 x86_64 % 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.22 % Memory : 8046.5625MB % 0.09/0.22 % OS : Linux 6.8.0-71-generic % 0.09/0.22 % CPULimit : 300 % 0.09/0.22 % WCLimit : 300 % 0.09/0.22 % DateTime : Mon Sep 28 15:03:15 UTC 2026 % 0.09/0.22 % CPUTime : % 0.09/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.27 Running first-order model finding % 0.09/0.27 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 % 5.38/1.14 % (3129002)Will run a generic schedule for satisfiability detection. % 5.38/1.14 % (3129008)% WARNING: option uhcvi not known. % 5.38/1.14 % (3129008)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4206083876:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.38/1.14 % (3129010)dis+10_1_sil=32000:sp=arity:random_seed=3805170996:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.38/1.14 % (3129007)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2339036006_2999 on theBenchmark for (2999ds/0Mi) % 5.38/1.14 % (3129009)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3899762510:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.38/1.14 % (3129013)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1902557119:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.38/1.14 % (3129012)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2560835831:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.38/1.14 % (3129011)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2145400562:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.52/1.14 % (3129007)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.52/1.14 % (3129007)Terminated due to inappropriate strategy. % 5.52/1.14 % (3129007)------------------------------ % 5.52/1.14 % (3129007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.52/1.14 % (3129007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.52/1.14 % (3129007)CaDiCaL version: 2.1.3 % 5.52/1.14 % (3129007)Termination reason: Inappropriate % 5.52/1.14 % (3129007)Time elapsed: 0.026 s % 5.52/1.14 % (3129007)Peak memory usage: 10 MB % 5.52/1.14 % (3129007)Instructions burned: 31 (million) % 5.52/1.14 % (3129007)------------------------------ % 5.52/1.14 % (3129007)------------------------------ % 5.52/1.14 % (3129010)Instruction limit reached! % 5.52/1.14 % (3129010)------------------------------ % 5.52/1.14 % (3129010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.52/1.14 % (3129010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.52/1.14 % (3129010)CaDiCaL version: 2.1.3 % 5.52/1.14 % (3129010)Termination reason: Instruction limit % 5.52/1.14 % (3129010)Termination phase: Saturation % 5.52/1.14 % (3129010)Time elapsed: 0.070 s % 5.52/1.14 % (3129010)Peak memory usage: 12 MB % 5.52/1.14 % (3129010)Instructions burned: 103 (million) % 5.52/1.14 % (3129023)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=865795076:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.52/1.14 % (3129011)Instruction limit reached! % 5.52/1.14 % (3129011)------------------------------ % 5.52/1.14 % (3129011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.52/1.14 % (3129011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.52/1.14 % (3129011)CaDiCaL version: 2.1.3 % 5.52/1.14 % (3129011)Termination reason: Instruction limit % 5.52/1.14 % (3129011)Termination phase: Saturation % 5.52/1.14 % (3129011)Time elapsed: 0.090 s % 5.52/1.14 % (3129011)Peak memory usage: 13 MB % 5.52/1.14 % (3129011)Instructions burned: 117 (million) % 5.52/1.14 % (3129023)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.52/1.14 % (3129023)Terminated due to inappropriate strategy. % 5.52/1.14 % (3129023)------------------------------ % 5.52/1.14 % (3129023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.52/1.14 % (3129023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.52/1.14 % (3129023)CaDiCaL version: 2.1.3 % 5.52/1.14 % (3129023)Termination reason: Inappropriate % 5.52/1.14 % (3129023)Time elapsed: 0.027 s % 5.52/1.14 % (3129023)Peak memory usage: 10 MB % 5.52/1.14 % (3129023)Instructions burned: 31 (million) % 5.52/1.14 % (3129024)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1543215608:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 5.52/1.14 % (3129023)------------------------------ % 5.52/1.14 % (3129023)------------------------------ % 5.52/1.14 % (3129012)Instruction limit reached! % 5.52/1.14 % (3129012)------------------------------ % 5.52/1.14 % (3129012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.52/1.14 % (3129012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.52/1.14 % (3129012)CaDiCaL version: 2.1.3 % 5.52/1.14 % (3129012)Termination reason: Instruction limit % 7.62/1.44 % (3129012)Termination phase: Saturation % 7.62/1.44 % (3129012)Time elapsed: 0.096 s % 7.62/1.44 % (3129012)Peak memory usage: 13 MB % 7.62/1.44 % (3129012)Instructions burned: 132 (million) % 7.62/1.44 % (3129029)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4028952689:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.62/1.44 % (3129026)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=2392206761:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.62/1.44 % (3129028)ott-21_1_sil=16000:fs=off:random_seed=3496382095:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.62/1.44 % (3129013)Instruction limit reached! % 7.62/1.44 % (3129013)------------------------------ % 7.62/1.44 % (3129013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.62/1.44 % (3129013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.62/1.44 % (3129013)CaDiCaL version: 2.1.3 % 7.62/1.44 % (3129013)Termination reason: Instruction limit % 7.62/1.44 % (3129013)Termination phase: Saturation % 7.62/1.44 % (3129013)Time elapsed: 0.130 s % 7.62/1.44 % (3129013)Peak memory usage: 14 MB % 7.62/1.44 % (3129013)Instructions burned: 159 (million) % 7.62/1.44 % (3129034)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2844727725:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.62/1.44 % (3129034)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.62/1.44 % (3129034)Terminated due to inappropriate strategy. % 7.62/1.44 % (3129034)------------------------------ % 7.62/1.44 % (3129034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.62/1.44 % (3129034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.62/1.44 % (3129034)CaDiCaL version: 2.1.3 % 7.62/1.44 % (3129034)Termination reason: Inappropriate % 7.62/1.44 % (3129034)Time elapsed: 0.020 s % 7.62/1.44 % (3129034)Peak memory usage: 10 MB % 7.62/1.44 % (3129034)Instructions burned: 23 (million) % 7.62/1.44 % (3129034)------------------------------ % 7.62/1.44 % (3129034)------------------------------ % 7.62/1.44 % (3129024)Instruction limit reached! % 7.62/1.44 % (3129024)------------------------------ % 7.62/1.44 % (3129024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.62/1.44 % (3129024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.62/1.44 % (3129024)CaDiCaL version: 2.1.3 % 7.62/1.44 % (3129024)Termination reason: Instruction limit % 7.62/1.44 % (3129024)Termination phase: Saturation % 7.62/1.44 % (3129024)Time elapsed: 0.104 s % 7.62/1.44 % (3129024)Peak memory usage: 14 MB % 7.62/1.44 % (3129024)Instructions burned: 131 (million) % 7.62/1.44 % (3129037)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3121151799:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 7.62/1.44 % (3129038)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=482748318:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.62/1.44 % (3129028)Instruction limit reached! % 7.62/1.44 % (3129028)------------------------------ % 7.62/1.44 % (3129028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.62/1.44 % (3129028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.62/1.44 % (3129028)CaDiCaL version: 2.1.3 % 7.62/1.44 % (3129028)Termination reason: Instruction limit % 7.62/1.44 % (3129028)Termination phase: Saturation % 7.62/1.44 % (3129028)Time elapsed: 0.130 s % 7.62/1.44 % (3129028)Peak memory usage: 13 MB % 7.62/1.44 % (3129028)Instructions burned: 180 (million) % 7.62/1.44 % (3129038)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.62/1.44 % (3129038)Terminated due to inappropriate strategy. % 7.62/1.44 % (3129038)------------------------------ % 7.62/1.44 % (3129038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.62/1.44 % (3129038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.62/1.44 % (3129038)CaDiCaL version: 2.1.3 % 7.62/1.44 % (3129038)Termination reason: Inappropriate % 7.62/1.44 % (3129038)Time elapsed: 0.023 s % 7.62/1.44 % (3129038)Peak memory usage: 10 MB % 7.62/1.44 % (3129038)Instructions burned: 23 (million) % 7.62/1.44 % (3129038)------------------------------ % 7.62/1.44 % (3129038)------------------------------ % 7.62/1.44 % (3129042)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1911618261:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 26.76/4.08 % (3129041)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=1426934794:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 26.76/4.08 % (3129029)Instruction limit reached! % 26.76/4.08 % (3129029)------------------------------ % 26.76/4.08 % (3129029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.76/4.08 % (3129029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.76/4.08 % (3129029)CaDiCaL version: 2.1.3 % 26.76/4.08 % (3129029)Termination reason: Instruction limit % 26.76/4.08 % (3129029)Termination phase: Saturation % 26.76/4.08 % (3129029)Time elapsed: 0.346 s % 26.76/4.08 % (3129029)Peak memory usage: 13 MB % 26.76/4.08 % (3129029)Instructions burned: 477 (million) % 26.76/4.08 % (3129049)fmb+10_1_sil=64000:random_seed=1685422581:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 26.76/4.08 % (3129049)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.76/4.08 % (3129049)Terminated due to inappropriate strategy. % 26.76/4.08 % (3129049)------------------------------ % 26.76/4.08 % (3129049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.76/4.08 % (3129049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.76/4.08 % (3129049)CaDiCaL version: 2.1.3 % 26.76/4.08 % (3129049)Termination reason: Inappropriate % 26.76/4.08 % (3129049)Time elapsed: 0.015 s % 26.76/4.08 % (3129049)Peak memory usage: 11 MB % 26.76/4.08 % (3129049)Instructions burned: 31 (million) % 26.76/4.08 % (3129049)------------------------------ % 26.76/4.08 % (3129049)------------------------------ % 26.76/4.08 % (3129052)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3466839843:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 26.76/4.08 % (3129052)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.76/4.08 % (3129052)Terminated due to inappropriate strategy. % 26.76/4.08 % (3129052)------------------------------ % 26.76/4.08 % (3129052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.76/4.08 % (3129052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.76/4.08 % (3129052)CaDiCaL version: 2.1.3 % 26.76/4.08 % (3129052)Termination reason: Inappropriate % 26.76/4.08 % (3129052)Time elapsed: 0.014 s % 26.76/4.08 % (3129052)Peak memory usage: 11 MB % 26.76/4.08 % (3129052)Instructions burned: 31 (million) % 26.76/4.08 % (3129052)------------------------------ % 26.76/4.08 % (3129052)------------------------------ % 26.76/4.08 % (3129055)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2465775304:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 26.76/4.08 % (3129055)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.76/4.08 % (3129055)Terminated due to inappropriate strategy. % 26.76/4.08 % (3129055)------------------------------ % 26.76/4.08 % (3129055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.76/4.08 % (3129055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.76/4.08 % (3129055)CaDiCaL version: 2.1.3 % 26.76/4.08 % (3129055)Termination reason: Inappropriate % 26.76/4.08 % (3129055)Time elapsed: 0.025 s % 26.76/4.08 % (3129055)Peak memory usage: 10 MB % 26.76/4.08 % (3129055)Instructions burned: 31 (million) % 26.76/4.08 % (3129055)------------------------------ % 26.76/4.08 % (3129055)------------------------------ % 26.76/4.08 % (3129057)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3765646349:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 26.76/4.08 % (3129026)Instruction limit reached! % 26.76/4.08 % (3129026)------------------------------ % 26.76/4.08 % (3129026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.76/4.08 % (3129026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.76/4.08 % (3129026)CaDiCaL version: 2.1.3 % 26.76/4.08 % (3129026)Termination reason: Instruction limit % 26.76/4.08 % (3129026)Termination phase: Saturation % 26.76/4.08 % (3129026)Time elapsed: 0.541 s % 26.76/4.08 % (3129026)Peak memory usage: 15 MB % 26.76/4.08 % (3129026)Instructions burned: 684 (million) % 26.76/4.08 % (3129059)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=599846354:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 26.76/4.08 % (3129041)Instruction limit reached! % 26.76/4.08 % (3129041)------------------------------ % 31.25/4.84 % (3129041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.25/4.84 % (3129041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.25/4.84 % (3129041)CaDiCaL version: 2.1.3 % 31.25/4.84 % (3129041)Termination reason: Instruction limit % 31.25/4.84 % (3129041)Termination phase: Saturation % 31.25/4.84 % (3129041)Time elapsed: 0.508 s % 31.25/4.84 % (3129041)Peak memory usage: 15 MB % 31.25/4.84 % (3129041)Instructions burned: 693 (million) % 31.25/4.84 % (3129061)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2685229254:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 31.25/4.84 % (3129061)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.25/4.84 % (3129061)Terminated due to inappropriate strategy. % 31.25/4.84 % (3129061)------------------------------ % 31.25/4.84 % (3129061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.25/4.84 % (3129061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.25/4.84 % (3129061)CaDiCaL version: 2.1.3 % 31.25/4.84 % (3129061)Termination reason: Inappropriate % 31.25/4.84 % (3129061)Time elapsed: 0.028 s % 31.25/4.84 % (3129061)Peak memory usage: 10 MB % 31.25/4.84 % (3129061)Instructions burned: 31 (million) % 31.25/4.84 % (3129061)------------------------------ % 31.25/4.84 % (3129061)------------------------------ % 31.25/4.84 % (3129063)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2849910176:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 31.25/4.84 % (3129063)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.25/4.84 % (3129063)Terminated due to inappropriate strategy. % 31.25/4.84 % (3129063)------------------------------ % 31.25/4.84 % (3129063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.25/4.84 % (3129063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.25/4.84 % (3129063)CaDiCaL version: 2.1.3 % 31.25/4.84 % (3129063)Termination reason: Inappropriate % 31.25/4.84 % (3129063)Time elapsed: 0.007 s % 31.25/4.84 % (3129063)Peak memory usage: 10 MB % 31.25/4.84 % (3129063)Instructions burned: 31 (million) % 31.25/4.84 % (3129063)------------------------------ % 31.25/4.84 % (3129063)------------------------------ % 31.25/4.84 % (3129065)ott-2_1_sil=16000:newcnf=on:random_seed=3024447386:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 31.25/4.84 % (3129042)Instruction limit reached! % 31.25/4.84 % (3129042)------------------------------ % 31.25/4.84 % (3129042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.25/4.84 % (3129042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.25/4.84 % (3129042)CaDiCaL version: 2.1.3 % 31.25/4.84 % (3129042)Termination reason: Instruction limit % 31.25/4.84 % (3129042)Termination phase: Saturation % 31.25/4.84 % (3129042)Time elapsed: 0.647 s % 31.25/4.84 % (3129042)Peak memory usage: 14 MB % 31.25/4.84 % (3129042)Instructions burned: 879 (million) % 31.25/4.84 % (3129067)ott+10_1_sil=32000:tgt=ground:random_seed=1551768845:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi) % 31.25/4.84 % (3129037)Instruction limit reached! % 31.25/4.84 % (3129037)------------------------------ % 31.25/4.84 % (3129037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.25/4.84 % (3129037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.25/4.84 % (3129037)CaDiCaL version: 2.1.3 % 31.25/4.84 % (3129037)Termination reason: Instruction limit % 31.25/4.84 % (3129037)Termination phase: Saturation % 31.25/4.84 % (3129037)Time elapsed: 0.845 s % 31.25/4.84 % (3129037)Peak memory usage: 14 MB % 31.25/4.84 % (3129037)Instructions burned: 1179 (million) % 31.25/4.84 % (3129069)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3499627603:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 31.25/4.84 % (3129069)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.25/4.84 % (3129069)Terminated due to inappropriate strategy. % 31.25/4.84 % (3129069)------------------------------ % 31.25/4.84 % (3129069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.25/4.84 % (3129069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.25/4.84 % (3129069)CaDiCaL version: 2.1.3 % 31.25/4.84 % (3129069)Termination reason: Inappropriate % 31.25/4.84 % (3129069)Time elapsed: 0.014 s % 31.25/4.84 % (3129069)Peak memory usage: 11 MB % 31.25/4.84 % (3129069)Instructions burned: 31 (million) % 120.77/17.39 % (3129069)------------------------------ % 120.77/17.39 % (3129069)------------------------------ % 120.77/17.39 % (3129071)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3077307902:i=3512:aac=none_2988 on theBenchmark for (2988ds/3512Mi) % 120.77/17.39 % (3129065)Instruction limit reached! % 120.77/17.39 % (3129065)------------------------------ % 120.77/17.39 % (3129065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.77/17.39 % (3129065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.77/17.39 % (3129065)CaDiCaL version: 2.1.3 % 120.77/17.39 % (3129065)Termination reason: Instruction limit % 120.77/17.39 % (3129065)Termination phase: Saturation % 120.77/17.39 % (3129065)Time elapsed: 0.332 s % 120.77/17.39 % (3129065)Peak memory usage: 15 MB % 120.77/17.39 % (3129065)Instructions burned: 870 (million) % 120.77/17.39 % (3129073)dis+21_1_sil=32000:sas=cadical:random_seed=2274054624:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 120.77/17.39 % (3129059)Instruction limit reached! % 120.77/17.39 % (3129059)------------------------------ % 120.77/17.39 % (3129059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.77/17.39 % (3129059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.77/17.39 % (3129059)CaDiCaL version: 2.1.3 % 120.77/17.39 % (3129059)Termination reason: Instruction limit % 120.77/17.39 % (3129059)Termination phase: Saturation % 120.77/17.39 % (3129059)Time elapsed: 1.310 s % 120.77/17.39 % (3129059)Peak memory usage: 23 MB % 120.77/17.39 % (3129059)Instructions burned: 1472 (million) % 120.77/17.39 % (3129079)ott+11_1_sil=16000:gs=on:random_seed=3857078639:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2979 on theBenchmark for (2979ds/2251Mi) % 120.77/17.39 % (3129073)Instruction limit reached! % 120.77/17.39 % (3129073)------------------------------ % 120.77/17.39 % (3129073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.77/17.39 % (3129073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.77/17.39 % (3129073)CaDiCaL version: 2.1.3 % 120.77/17.39 % (3129073)Termination reason: Instruction limit % 120.77/17.39 % (3129073)Termination phase: Saturation % 120.77/17.39 % (3129073)Time elapsed: 1.493 s % 120.77/17.39 % (3129073)Peak memory usage: 16 MB % 120.77/17.39 % (3129073)Instructions burned: 3774 (million) % 120.77/17.39 % (3129085)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2044138215:fmbsr=1.6:i=67534_2971 on theBenchmark for (2971ds/67534Mi) % 120.77/17.39 % (3129085)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.77/17.39 % (3129085)Terminated due to inappropriate strategy. % 120.77/17.39 % (3129085)------------------------------ % 120.77/17.39 % (3129085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.77/17.39 % (3129085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.77/17.39 % (3129085)CaDiCaL version: 2.1.3 % 120.77/17.39 % (3129085)Termination reason: Inappropriate % 120.77/17.39 % (3129085)Time elapsed: 0.013 s % 120.77/17.39 % (3129085)Peak memory usage: 10 MB % 120.77/17.39 % (3129085)Instructions burned: 31 (million) % 120.77/17.39 % (3129085)------------------------------ % 120.77/17.39 % (3129085)------------------------------ % 120.77/17.39 % (3129087)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=193981387:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2971 on theBenchmark for (2971ds/4591Mi) % 120.77/17.39 % (3129079)Instruction limit reached! % 120.77/17.39 % (3129079)------------------------------ % 120.77/17.39 % (3129079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.77/17.39 % (3129079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.77/17.39 % (3129079)CaDiCaL version: 2.1.3 % 120.77/17.39 % (3129079)Termination reason: Instruction limit % 120.77/17.39 % (3129079)Termination phase: Saturation % 120.77/17.39 % (3129079)Time elapsed: 1.562 s % 120.77/17.39 % (3129079)Peak memory usage: 14 MB % 120.77/17.39 % (3129079)Instructions burned: 2251 (million) % 120.77/17.39 % (3129089)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1865043533:i=29340_2963 on theBenchmark for (2963ds/29340Mi) % 120.77/17.39 % (3129071)Instruction limit reached! % 120.77/17.39 % (3129071)------------------------------ % 120.77/17.39 % (3129071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.77/17.39 % (3129071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.77/17.39 % (3129071)CaDiCaL version: 2.1.3 % 120.77/17.39 % (3129071)Termination reason: Instruction limit % 152.58/21.96 % (3129071)Termination phase: Saturation % 152.58/21.96 % (3129071)Time elapsed: 2.616 s % 152.58/21.96 % (3129071)Peak memory usage: 16 MB % 152.58/21.96 % (3129071)Instructions burned: 3514 (million) % 152.58/21.96 % (3129091)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2688655548:i=5211_2961 on theBenchmark for (2961ds/5211Mi) % 152.58/21.96 % (3129067)Instruction limit reached! % 152.58/21.96 % (3129067)------------------------------ % 152.58/21.96 % (3129067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.58/21.96 % (3129067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.58/21.96 % (3129067)CaDiCaL version: 2.1.3 % 152.58/21.96 % (3129067)Termination reason: Instruction limit % 152.58/21.96 % (3129067)Termination phase: Saturation % 152.58/21.96 % (3129067)Time elapsed: 3.385 s % 152.58/21.96 % (3129067)Peak memory usage: 14 MB % 152.58/21.96 % (3129067)Instructions burned: 5114 (million) % 152.58/21.96 % (3129057)Instruction limit reached! % 152.58/21.96 % (3129057)------------------------------ % 152.58/21.96 % (3129057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.58/21.96 % (3129057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.58/21.96 % (3129057)CaDiCaL version: 2.1.3 % 152.58/21.96 % (3129057)Termination reason: Instruction limit % 152.58/21.96 % (3129057)Termination phase: Saturation % 152.58/21.96 % (3129057)Time elapsed: 3.757 s % 152.58/21.96 % (3129057)Peak memory usage: 20 MB % 152.58/21.96 % (3129057)Instructions burned: 5132 (million) % 152.58/21.96 % (3129096)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1876532257:i=5497:nm=2_2955 on theBenchmark for (2955ds/5497Mi) % 152.58/21.96 % (3129097)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=927043231:fmbsr=2:i=46332_2955 on theBenchmark for (2955ds/46332Mi) % 152.58/21.96 % (3129096)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 152.58/21.96 % (3129096)Terminated due to inappropriate strategy. % 152.58/21.96 % (3129096)------------------------------ % 152.58/21.96 % (3129096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.58/21.96 % (3129096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.58/21.96 % (3129096)CaDiCaL version: 2.1.3 % 152.58/21.96 % (3129096)Termination reason: Inappropriate % 152.58/21.96 % (3129096)Time elapsed: 0.028 s % 152.58/21.96 % (3129096)Peak memory usage: 11 MB % 152.58/21.96 % (3129096)Instructions burned: 31 (million) % 152.58/21.96 % (3129096)------------------------------ % 152.58/21.96 % (3129096)------------------------------ % 152.58/21.96 % (3129097)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 152.58/21.96 % (3129097)Terminated due to inappropriate strategy. % 152.58/21.96 % (3129097)------------------------------ % 152.58/21.96 % (3129097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.58/21.96 % (3129097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.58/21.96 % (3129097)CaDiCaL version: 2.1.3 % 152.58/21.96 % (3129097)Termination reason: Inappropriate % 152.58/21.96 % (3129097)Time elapsed: 0.014 s % 152.58/21.96 % (3129097)Peak memory usage: 11 MB % 152.58/21.96 % (3129097)Instructions burned: 31 (million) % 152.58/21.96 % (3129097)------------------------------ % 152.58/21.96 % (3129097)------------------------------ % 152.58/21.96 % (3129102)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3523750647:i=22565:add=on:rawr=on_2955 on theBenchmark for (2955ds/22565Mi) % 152.58/21.96 % (3129101)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3249368436:i=14071_2955 on theBenchmark for (2955ds/14071Mi) % 152.58/21.96 % (3129101)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 152.58/21.96 % (3129101)Terminated due to inappropriate strategy. % 152.58/21.96 % (3129101)------------------------------ % 152.58/21.96 % (3129101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.58/21.96 % (3129101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.58/21.96 % (3129101)CaDiCaL version: 2.1.3 % 152.58/21.96 % (3129101)Termination reason: Inappropriate % 152.58/21.96 % (3129101)Time elapsed: 0.027 s % 152.58/21.96 % (3129101)Peak memory usage: 10 MB % 152.58/21.96 % (3129101)Instructions burned: 31 (million) % 152.58/21.96 % (3129101)------------------------------ % 152.58/21.96 % (3129101)------------------------------ % 152.58/21.96 % (3129105)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3648909500:i=8173:av=off_2954 on theBenchmark for (2954ds/8173Mi) % 155.44/22.22 % (3129087)Instruction limit reached! % 155.44/22.22 % (3129087)------------------------------ % 155.44/22.22 % (3129087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.44/22.22 % (3129087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.44/22.22 % (3129087)CaDiCaL version: 2.1.3 % 155.44/22.22 % (3129087)Termination reason: Instruction limit % 155.44/22.22 % (3129087)Termination phase: Saturation % 155.44/22.22 % (3129087)Time elapsed: 2.306 s % 155.44/22.22 % (3129087)Peak memory usage: 47 MB % 155.44/22.22 % (3129087)Instructions burned: 4591 (million) % 155.44/22.22 % (3129107)dis+10_16:1_sil=16000:random_seed=4113286679:i=9155:fsr=off_2948 on theBenchmark for (2948ds/9155Mi) % 155.44/22.22 % (3129091)Instruction limit reached! % 155.44/22.22 % (3129091)------------------------------ % 155.44/22.22 % (3129091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.44/22.22 % (3129091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.44/22.22 % (3129091)CaDiCaL version: 2.1.3 % 155.44/22.22 % (3129091)Termination reason: Instruction limit % 155.44/22.22 % (3129091)Termination phase: Saturation % 155.44/22.22 % (3129091)Time elapsed: 3.686 s % 155.44/22.22 % (3129091)Peak memory usage: 22 MB % 155.44/22.22 % (3129091)Instructions burned: 5211 (million) % 155.44/22.22 % (3129119)ott-3_8_sil=64000:random_seed=824201484:i=20139:bs=on_2924 on theBenchmark for (2924ds/20139Mi) % 155.44/22.22 % (3129107)Instruction limit reached! % 155.44/22.22 % (3129107)------------------------------ % 155.44/22.22 % (3129107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.44/22.22 % (3129107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.44/22.22 % (3129107)CaDiCaL version: 2.1.3 % 155.44/22.22 % (3129107)Termination reason: Instruction limit % 155.44/22.22 % (3129107)Termination phase: Saturation % 155.44/22.22 % (3129107)Time elapsed: 3.536 s % 155.44/22.22 % (3129107)Peak memory usage: 18 MB % 155.44/22.22 % (3129107)Instructions burned: 9156 (million) % 155.44/22.22 % (3129121)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1629277043:fmbsr=2:i=32576_2912 on theBenchmark for (2912ds/32576Mi) % 155.44/22.22 % (3129121)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.44/22.22 % (3129121)Terminated due to inappropriate strategy. % 155.44/22.22 % (3129121)------------------------------ % 155.44/22.22 % (3129121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.44/22.22 % (3129121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.44/22.22 % (3129121)CaDiCaL version: 2.1.3 % 155.44/22.22 % (3129121)Termination reason: Inappropriate % 155.44/22.22 % (3129121)Time elapsed: 0.026 s % 155.44/22.22 % (3129121)Peak memory usage: 10 MB % 155.44/22.22 % (3129121)Instructions burned: 31 (million) % 155.44/22.22 % (3129121)------------------------------ % 155.44/22.22 % (3129121)------------------------------ % 155.44/22.22 % (3129123)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3694797914:i=11404_2912 on theBenchmark for (2912ds/11404Mi) % 155.44/22.22 % (3129105)Instruction limit reached! % 155.44/22.22 % (3129105)------------------------------ % 155.44/22.22 % (3129105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.44/22.22 % (3129105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.44/22.22 % (3129105)CaDiCaL version: 2.1.3 % 155.44/22.22 % (3129105)Termination reason: Instruction limit % 155.44/22.22 % (3129105)Termination phase: Saturation % 155.44/22.22 % (3129105)Time elapsed: 5.920 s % 155.44/22.22 % (3129105)Peak memory usage: 15 MB % 155.44/22.22 % (3129105)Instructions burned: 8173 (million) % 155.44/22.22 % (3129125)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3932849043:i=14134_2895 on theBenchmark for (2895ds/14134Mi) % 155.44/22.22 % (3129102)Instruction limit reached! % 155.44/22.22 % (3129102)------------------------------ % 155.44/22.22 % (3129102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.44/22.22 % (3129102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.44/22.22 % (3129102)CaDiCaL version: 2.1.3 % 155.44/22.22 % (3129102)Termination reason: Instruction limit % 155.44/22.22 % (3129102)Termination phase: Saturation % 155.44/22.22 % (3129102)Time elapsed: 10.184 s % 155.44/22.22 % (3129102)Peak memory usage: 17 MB % 155.44/22.22 % (3129102)Instructions burned: 22565 (million) % 155.44/22.22 % (3129135)dis+33_16_sil=32000:sac=on:random_seed=26067877:i=15851:nm=0_2853 on theBenchmark for (2853ds/15851Mi) % 155.44/22.22 % (3129123)Instruction limit reached! % 155.44/22.22 % (3129123)------------------------------ % 155.44/22.22 % (3129123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.08/29.94 % (3129123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.08/29.94 % (3129123)CaDiCaL version: 2.1.3 % 210.08/29.94 % (3129123)Termination reason: Instruction limit % 210.08/29.94 % (3129123)Termination phase: Saturation % 210.08/29.94 % (3129123)Time elapsed: 8.301 s % 210.08/29.94 % (3129123)Peak memory usage: 16 MB % 210.08/29.94 % (3129123)Instructions burned: 11405 (million) % 210.08/29.94 % (3129143)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2973207186:avsq=on:i=17627:add=on:amm=off_2828 on theBenchmark for (2828ds/17627Mi) % 210.08/29.94 % (3129135)Instruction limit reached! % 210.08/29.94 % (3129135)------------------------------ % 210.08/29.94 % (3129135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.08/29.94 % (3129135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.08/29.94 % (3129135)CaDiCaL version: 2.1.3 % 210.08/29.94 % (3129135)Termination reason: Instruction limit % 210.08/29.94 % (3129135)Termination phase: Saturation % 210.08/29.94 % (3129135)Time elapsed: 5.909 s % 210.08/29.94 % (3129135)Peak memory usage: 22 MB % 210.08/29.94 % (3129135)Instructions burned: 15851 (million) % 210.08/29.94 % (3129145)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1506314863:s2a=on:i=53295_2793 on theBenchmark for (2793ds/53295Mi) % 210.08/29.94 % (3129125)Instruction limit reached! % 210.08/29.94 % (3129125)------------------------------ % 210.08/29.94 % (3129125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.08/29.94 % (3129125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.08/29.94 % (3129125)CaDiCaL version: 2.1.3 % 210.08/29.94 % (3129125)Termination reason: Instruction limit % 210.08/29.94 % (3129125)Termination phase: Saturation % 210.08/29.94 % (3129125)Time elapsed: 10.266 s % 210.08/29.94 % (3129125)Peak memory usage: 16 MB % 210.08/29.94 % (3129125)Instructions burned: 14135 (million) % 210.08/29.94 % (3129147)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3795086717:i=26857:ins=20_2792 on theBenchmark for (2792ds/26857Mi) % 210.08/29.94 % (3129147)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 210.08/29.94 % (3129147)Terminated due to inappropriate strategy. % 210.08/29.94 % (3129147)------------------------------ % 210.08/29.94 % (3129147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.08/29.94 % (3129147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.08/29.94 % (3129147)CaDiCaL version: 2.1.3 % 210.08/29.94 % (3129147)Termination reason: Inappropriate % 210.08/29.94 % (3129147)Time elapsed: 0.015 s % 210.08/29.94 % (3129147)Peak memory usage: 11 MB % 210.08/29.94 % (3129147)Instructions burned: 31 (million) % 210.08/29.94 % (3129147)------------------------------ % 210.08/29.94 % (3129147)------------------------------ % 210.08/29.94 % (3129149)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1697358475:i=28120:bs=on:fsr=off_2791 on theBenchmark for (2791ds/28120Mi) % 210.08/29.94 % (3129119)Instruction limit reached! % 210.08/29.94 % (3129119)------------------------------ % 210.08/29.94 % (3129119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.08/29.94 % (3129119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.08/29.94 % (3129119)CaDiCaL version: 2.1.3 % 210.08/29.94 % (3129119)Termination reason: Instruction limit % 210.08/29.94 % (3129119)Termination phase: Saturation % 210.08/29.94 % (3129119)Time elapsed: 14.073 s % 210.08/29.94 % (3129119)Peak memory usage: 19 MB % 210.08/29.94 % (3129119)Instructions burned: 20140 (million) % 210.08/29.94 % (3129153)fmb+10_1_sil=256000:fmbss=7:random_seed=3098477939:fmbsr=1.6:i=182295_2783 on theBenchmark for (2783ds/182295Mi) % 210.08/29.94 % (3129153)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 210.08/29.94 % (3129153)Terminated due to inappropriate strategy. % 210.08/29.94 % (3129153)------------------------------ % 210.08/29.94 % (3129153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.08/29.94 % (3129153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.08/29.94 % (3129153)CaDiCaL version: 2.1.3 % 210.08/29.94 % (3129153)Termination reason: Inappropriate % 210.08/29.94 % (3129153)Time elapsed: 0.018 s % 210.08/29.94 % (3129153)Peak memory usage: 10 MB % 210.08/29.94 % (3129153)Instructions burned: 31 (million) % 210.08/29.94 % (3129153)------------------------------ % 210.08/29.94 % (3129153)------------------------------ % 210.08/29.94 % (3129155)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2206809614:i=44625:gsp=on_2783 on theBenchmark for (2783ds/44625Mi) % 219.47/31.23 % (3129155)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 219.47/31.23 % (3129155)Terminated due to inappropriate strategy. % 219.47/31.23 % (3129155)------------------------------ % 219.47/31.23 % (3129155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.47/31.23 % (3129155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.23 % (3129155)CaDiCaL version: 2.1.3 % 219.47/31.23 % (3129155)Termination reason: Inappropriate % 219.47/31.23 % (3129155)Time elapsed: 0.014 s % 219.47/31.23 % (3129155)Peak memory usage: 11 MB % 219.47/31.23 % (3129155)Instructions burned: 31 (million) % 219.47/31.23 % (3129155)------------------------------ % 219.47/31.23 % (3129155)------------------------------ % 219.47/31.23 % (3129157)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1353685758:i=160505_2783 on theBenchmark for (2783ds/160505Mi) % 219.47/31.23 % (3129157)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 219.47/31.23 % (3129157)Terminated due to inappropriate strategy. % 219.47/31.23 % (3129157)------------------------------ % 219.47/31.23 % (3129157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.47/31.23 % (3129157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.23 % (3129157)CaDiCaL version: 2.1.3 % 219.47/31.23 % (3129157)Termination reason: Inappropriate % 219.47/31.23 % (3129157)Time elapsed: 0.024 s % 219.47/31.23 % (3129157)Peak memory usage: 10 MB % 219.47/31.23 % (3129157)Instructions burned: 31 (million) % 219.47/31.23 % (3129157)------------------------------ % 219.47/31.23 % (3129157)------------------------------ % 219.47/31.23 % (3129159)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1135916454:fmbsr=1.3:i=225729_2782 on theBenchmark for (2782ds/225729Mi) % 219.47/31.23 % (3129159)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 219.47/31.23 % (3129159)Terminated due to inappropriate strategy. % 219.47/31.23 % (3129159)------------------------------ % 219.47/31.23 % (3129159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.47/31.23 % (3129159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.23 % (3129159)CaDiCaL version: 2.1.3 % 219.47/31.23 % (3129159)Termination reason: Inappropriate % 219.47/31.23 % (3129159)Time elapsed: 0.031 s % 219.47/31.23 % (3129159)Peak memory usage: 10 MB % 219.47/31.23 % (3129159)Instructions burned: 31 (million) % 219.47/31.23 % (3129159)------------------------------ % 219.47/31.23 % (3129159)------------------------------ % 219.47/31.23 % (3129161)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1589127426:fmbsr=2:i=185024:ins=7_2781 on theBenchmark for (2781ds/185024Mi) % 219.47/31.23 % (3129161)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 219.47/31.23 % (3129161)Terminated due to inappropriate strategy. % 219.47/31.23 % (3129161)------------------------------ % 219.47/31.23 % (3129161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.47/31.23 % (3129161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.23 % (3129161)CaDiCaL version: 2.1.3 % 219.47/31.23 % (3129161)Termination reason: Inappropriate % 219.47/31.23 % (3129161)Time elapsed: 0.015 s % 219.47/31.23 % (3129161)Peak memory usage: 11 MB % 219.47/31.23 % (3129161)Instructions burned: 31 (million) % 219.47/31.23 % (3129161)------------------------------ % 219.47/31.23 % (3129161)------------------------------ % 219.47/31.23 % (3129163)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4187259340:rtra=on_2781 on theBenchmark for (2781ds/0Mi) % 219.47/31.23 % (3129163)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 219.47/31.23 % (3129163)Terminated due to inappropriate strategy. % 219.47/31.23 % (3129163)------------------------------ % 219.47/31.23 % (3129163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.47/31.23 % (3129163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.47/31.23 % (3129163)CaDiCaL version: 2.1.3 % 219.47/31.23 % (3129163)Termination reason: Inappropriate % 219.47/31.23 % (3129163)Time elapsed: 0.031 s % 219.47/31.23 % (3129163)Peak memory usage: 11 MB % 219.47/31.23 % (3129163)Instructions burned: 31 (million) % 219.47/31.23 % (3129163)------------------------------ % 219.47/31.23 % (3129163)------------------------------ % 219.47/31.23 % (3129165)% WARNING: option uhcvi not known. % 219.47/31.23 % (3129165)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=490432907:i=271062:add=off:rtra=on:rawr=on_2780 on theBenchmark for (2780ds/271062Mi) % 235.76/33.51 % (3129089)Instruction limit reached! % 235.76/33.51 % (3129089)------------------------------ % 235.76/33.51 % (3129089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.76/33.51 % (3129089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.76/33.51 % (3129089)CaDiCaL version: 2.1.3 % 235.76/33.51 % (3129089)Termination reason: Instruction limit % 235.76/33.51 % (3129089)Termination phase: Saturation % 235.76/33.51 % (3129089)Time elapsed: 19.956 s % 235.76/33.51 % (3129089)Peak memory usage: 21 MB % 235.76/33.51 % (3129089)Instructions burned: 29340 (million) % 235.76/33.51 % (3129169)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=372857634:i=176048:add=on:rtra=on:rawr=on_2763 on theBenchmark for (2763ds/176048Mi) % 235.76/33.51 % (3129143)Instruction limit reached! % 235.76/33.51 % (3129143)------------------------------ % 235.76/33.51 % (3129143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.76/33.51 % (3129143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.76/33.51 % (3129143)CaDiCaL version: 2.1.3 % 235.76/33.51 % (3129143)Termination reason: Instruction limit % 235.76/33.51 % (3129143)Termination phase: Saturation % 235.76/33.51 % (3129143)Time elapsed: 11.990 s % 235.76/33.51 % (3129143)Peak memory usage: 98 MB % 235.76/33.51 % (3129143)Instructions burned: 17628 (million) % 235.76/33.51 % (3129224)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2911797977:i=206:fgj=on:rtra=on_2708 on theBenchmark for (2708ds/206Mi) % 235.76/33.51 % (3129224)Instruction limit reached! % 235.76/33.51 % (3129224)------------------------------ % 235.76/33.51 % (3129224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.76/33.51 % (3129224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.76/33.51 % (3129224)CaDiCaL version: 2.1.3 % 235.76/33.51 % (3129224)Termination reason: Instruction limit % 235.76/33.51 % (3129224)Termination phase: Saturation % 235.76/33.51 % (3129224)Time elapsed: 0.084 s % 235.76/33.51 % (3129224)Peak memory usage: 13 MB % 235.76/33.51 % (3129224)Instructions burned: 206 (million) % 235.76/33.51 % (3129226)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1291594092:i=232:rtra=on_2707 on theBenchmark for (2707ds/232Mi) % 235.76/33.51 % (3129226)Instruction limit reached! % 235.76/33.51 % (3129226)------------------------------ % 235.76/33.51 % (3129226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.76/33.51 % (3129226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.76/33.51 % (3129226)CaDiCaL version: 2.1.3 % 235.76/33.51 % (3129226)Termination reason: Instruction limit % 235.76/33.51 % (3129226)Termination phase: Saturation % 235.76/33.51 % (3129226)Time elapsed: 0.091 s % 235.76/33.51 % (3129226)Peak memory usage: 12 MB % 235.76/33.51 % (3129226)Instructions burned: 233 (million) % 235.76/33.51 % (3129228)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=791430174:i=262:rtra=on_2706 on theBenchmark for (2706ds/262Mi) % 235.76/33.51 % (3129228)Instruction limit reached! % 235.76/33.51 % (3129228)------------------------------ % 235.76/33.51 % (3129228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.76/33.51 % (3129228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.76/33.51 % (3129228)CaDiCaL version: 2.1.3 % 235.76/33.51 % (3129228)Termination reason: Instruction limit % 235.76/33.51 % (3129228)Termination phase: Saturation % 235.76/33.51 % (3129228)Time elapsed: 0.104 s % 235.76/33.51 % (3129228)Peak memory usage: 12 MB % 235.76/33.51 % (3129228)Instructions burned: 264 (million) % 235.76/33.51 % (3129230)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=4034810678:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2705 on theBenchmark for (2705ds/318Mi) % 235.76/33.51 % (3129230)Instruction limit reached! % 235.76/33.51 % (3129230)------------------------------ % 235.76/33.51 % (3129230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.76/33.51 % (3129230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.76/33.51 % (3129230)CaDiCaL version: 2.1.3 % 235.76/33.51 % (3129230)Termination reason: Instruction limit % 235.76/33.51 % (3129230)Termination phase: Saturation % 235.76/33.51 % (3129230)Time elapsed: 0.142 s % 235.76/33.51 % (3129230)Peak memory usage: 14 MB % 235.76/33.51 % (3129230)Instructions burned: 320 (million) % 235.76/33.51 % (3129232)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2792665541:i=1428:nm=2:rtra=on_2703 on theBenchmark for (2703ds/1428Mi) % 249.70/35.57 % (3129232)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.70/35.57 % (3129232)Terminated due to inappropriate strategy. % 249.70/35.57 % (3129232)------------------------------ % 249.70/35.57 % (3129232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.70/35.57 % (3129232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.70/35.57 % (3129232)CaDiCaL version: 2.1.3 % 249.70/35.57 % (3129232)Termination reason: Inappropriate % 249.70/35.57 % (3129232)Time elapsed: 0.013 s % 249.70/35.57 % (3129232)Peak memory usage: 11 MB % 249.70/35.57 % (3129232)Instructions burned: 32 (million) % 249.70/35.57 % (3129232)------------------------------ % 249.70/35.57 % (3129232)------------------------------ % 249.70/35.57 % (3129234)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2014838859:i=262:bd=preordered:rtra=on:fsd=on_2703 on theBenchmark for (2703ds/262Mi) % 249.70/35.57 % (3129234)Instruction limit reached! % 249.70/35.57 % (3129234)------------------------------ % 249.70/35.57 % (3129234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.70/35.57 % (3129234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.70/35.57 % (3129234)CaDiCaL version: 2.1.3 % 249.70/35.57 % (3129234)Termination reason: Instruction limit % 249.70/35.57 % (3129234)Termination phase: Saturation % 249.70/35.57 % (3129234)Time elapsed: 0.111 s % 249.70/35.57 % (3129234)Peak memory usage: 15 MB % 249.70/35.57 % (3129234)Instructions burned: 262 (million) % 249.70/35.57 % (3129236)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=264375435:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2701 on theBenchmark for (2701ds/1368Mi) % 249.70/35.57 % (3129236)Instruction limit reached! % 249.70/35.57 % (3129236)------------------------------ % 249.70/35.57 % (3129236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.70/35.57 % (3129236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.70/35.57 % (3129236)CaDiCaL version: 2.1.3 % 249.70/35.57 % (3129236)Termination reason: Instruction limit % 249.70/35.57 % (3129236)Termination phase: Saturation % 249.70/35.57 % (3129236)Time elapsed: 0.540 s % 249.70/35.57 % (3129236)Peak memory usage: 16 MB % 249.70/35.57 % (3129236)Instructions burned: 1369 (million) % 249.70/35.57 % (3129238)ott-21_1_sil=16000:si=on:fs=off:random_seed=4068972524:i=360:av=off:fsr=off:rtra=on_2696 on theBenchmark for (2696ds/360Mi) % 249.70/35.57 % (3129238)Instruction limit reached! % 249.70/35.57 % (3129238)------------------------------ % 249.70/35.57 % (3129238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.70/35.57 % (3129238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.70/35.57 % (3129238)CaDiCaL version: 2.1.3 % 249.70/35.57 % (3129238)Termination reason: Instruction limit % 249.70/35.57 % (3129238)Termination phase: Saturation % 249.70/35.57 % (3129238)Time elapsed: 0.137 s % 249.70/35.57 % (3129238)Peak memory usage: 12 MB % 249.70/35.57 % (3129238)Instructions burned: 362 (million) % 249.70/35.57 % (3129240)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1716345187:i=954:bd=all:rtra=on_2694 on theBenchmark for (2694ds/954Mi) % 249.70/35.57 % (3129240)Instruction limit reached! % 249.70/35.57 % (3129240)------------------------------ % 249.70/35.57 % (3129240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.70/35.57 % (3129240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.70/35.57 % (3129240)CaDiCaL version: 2.1.3 % 249.70/35.57 % (3129240)Termination reason: Instruction limit % 249.70/35.57 % (3129240)Termination phase: Saturation % 249.70/35.57 % (3129240)Time elapsed: 0.372 s % 249.70/35.57 % (3129240)Peak memory usage: 14 MB % 249.70/35.57 % (3129240)Instructions burned: 957 (million) % 249.70/35.57 % (3129242)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4172443739:fmbsr=1.3:i=1730:ins=25:rtra=on_2690 on theBenchmark for (2690ds/1730Mi) % 249.70/35.57 % (3129242)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.70/35.57 % (3129242)Terminated due to inappropriate strategy. % 249.70/35.57 % (3129242)------------------------------ % 249.70/35.57 % (3129242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.70/35.57 % (3129242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.70/35.57 % (3129242)CaDiCaL version: 2.1.3 % 249.70/35.57 % (3129242)Termination reason: Inappropriate % 269.80/38.31 % (3129242)Time elapsed: 0.010 s % 269.80/38.31 % (3129242)Peak memory usage: 10 MB % 269.80/38.31 % (3129242)Instructions burned: 24 (million) % 269.80/38.31 % (3129242)------------------------------ % 269.80/38.31 % (3129242)------------------------------ % 269.80/38.31 % (3129244)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=452268597:i=2358:rtra=on_2690 on theBenchmark for (2690ds/2358Mi) % 269.80/38.31 % (3129244)Instruction limit reached! % 269.80/38.31 % (3129244)------------------------------ % 269.80/38.31 % (3129244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.80/38.31 % (3129244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.80/38.31 % (3129244)CaDiCaL version: 2.1.3 % 269.80/38.31 % (3129244)Termination reason: Instruction limit % 269.80/38.31 % (3129244)Termination phase: Saturation % 269.80/38.31 % (3129244)Time elapsed: 0.907 s % 269.80/38.31 % (3129244)Peak memory usage: 13 MB % 269.80/38.31 % (3129244)Instructions burned: 2359 (million) % 269.80/38.31 % (3129246)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=461061432:i=1778:ins=1:rtra=on_2681 on theBenchmark for (2681ds/1778Mi) % 269.80/38.31 % (3129246)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.80/38.31 % (3129246)Terminated due to inappropriate strategy. % 269.80/38.31 % (3129246)------------------------------ % 269.80/38.31 % (3129246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.80/38.31 % (3129246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.80/38.31 % (3129246)CaDiCaL version: 2.1.3 % 269.80/38.31 % (3129246)Termination reason: Inappropriate % 269.80/38.31 % (3129246)Time elapsed: 0.010 s % 269.80/38.31 % (3129246)Peak memory usage: 10 MB % 269.80/38.31 % (3129246)Instructions burned: 24 (million) % 269.80/38.31 % (3129246)------------------------------ % 269.80/38.31 % (3129246)------------------------------ % 269.80/38.31 % (3129248)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=3442600091:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2680 on theBenchmark for (2680ds/1384Mi) % 269.80/38.31 % (3129248)Instruction limit reached! % 269.80/38.31 % (3129248)------------------------------ % 269.80/38.31 % (3129248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.80/38.31 % (3129248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.80/38.31 % (3129248)CaDiCaL version: 2.1.3 % 269.80/38.31 % (3129248)Termination reason: Instruction limit % 269.80/38.31 % (3129248)Termination phase: Saturation % 269.80/38.31 % (3129248)Time elapsed: 0.548 s % 269.80/38.31 % (3129248)Peak memory usage: 16 MB % 269.80/38.31 % (3129248)Instructions burned: 1386 (million) % 269.80/38.31 % (3129250)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=105295210:i=1758:kws=inv_precedence:fsr=off:rtra=on_2675 on theBenchmark for (2675ds/1758Mi) % 269.80/38.31 % (3129250)Instruction limit reached! % 269.80/38.31 % (3129250)------------------------------ % 269.80/38.31 % (3129250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.80/38.31 % (3129250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.80/38.31 % (3129250)CaDiCaL version: 2.1.3 % 269.80/38.31 % (3129250)Termination reason: Instruction limit % 269.80/38.31 % (3129250)Termination phase: Saturation % 269.80/38.31 % (3129250)Time elapsed: 0.680 s % 269.80/38.31 % (3129250)Peak memory usage: 15 MB % 269.80/38.31 % (3129250)Instructions burned: 1761 (million) % 269.80/38.31 % (3129252)fmb+10_1_sil=64000:si=on:random_seed=3424429495:i=44122:nm=2:rtra=on:gsp=on_2668 on theBenchmark for (2668ds/44122Mi) % 269.80/38.31 % (3129252)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 269.80/38.31 % (3129252)Terminated due to inappropriate strategy. % 269.80/38.31 % (3129252)------------------------------ % 269.80/38.31 % (3129252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 269.80/38.31 % (3129252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.80/38.31 % (3129252)CaDiCaL version: 2.1.3 % 269.80/38.31 % (3129252)Termination reason: Inappropriate % 269.80/38.31 % (3129252)Time elapsed: 0.013 s % 269.80/38.31 % (3129252)Peak memory usage: 11 MB % 269.80/38.31 % (3129252)Instructions burned: 32 (million) % 269.80/38.31 % (3129252)------------------------------ % 269.80/38.31 % (3129252)------------------------------ % 269.80/38.31 % (3129254)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3870031087:i=19030:nm=5:rtra=on_2667 on theBenchmark for (2667ds/19030Mi) % 295.33/41.93 % (3129254)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 295.33/41.93 % (3129254)Terminated due to inappropriate strategy. % 295.33/41.93 % (3129254)------------------------------ % 295.33/41.93 % (3129254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.33/41.93 % (3129254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.33/41.93 % (3129254)CaDiCaL version: 2.1.3 % 295.33/41.93 % (3129254)Termination reason: Inappropriate % 295.33/41.93 % (3129254)Time elapsed: 0.013 s % 295.33/41.93 % (3129254)Peak memory usage: 11 MB % 295.33/41.93 % (3129254)Instructions burned: 31 (million) % 295.33/41.93 % (3129254)------------------------------ % 295.33/41.93 % (3129254)------------------------------ % 295.33/41.93 % (3129256)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1946614216:fmbsr=1.7:i=1840:rtra=on_2667 on theBenchmark for (2667ds/1840Mi) % 295.33/41.93 % (3129256)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 295.33/41.93 % (3129256)Terminated due to inappropriate strategy. % 295.33/41.93 % (3129256)------------------------------ % 295.33/41.93 % (3129256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.33/41.93 % (3129256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.33/41.93 % (3129256)CaDiCaL version: 2.1.3 % 295.33/41.93 % (3129256)Termination reason: Inappropriate % 295.33/41.93 % (3129256)Time elapsed: 0.013 s % 295.33/41.93 % (3129256)Peak memory usage: 11 MB % 295.33/41.93 % (3129256)Instructions burned: 31 (million) % 295.33/41.93 % (3129256)------------------------------ % 295.33/41.93 % (3129256)------------------------------ % 295.33/41.93 % (3129258)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=844923885:i=10262:rtra=on_2667 on theBenchmark for (2667ds/10262Mi) % 295.33/41.93 % (3129149)Instruction limit reached! % 295.33/41.93 % (3129149)------------------------------ % 295.33/41.93 % (3129149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.33/41.93 % (3129149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.33/41.93 % (3129149)CaDiCaL version: 2.1.3 % 295.33/41.93 % (3129149)Termination reason: Instruction limit % 295.33/41.93 % (3129149)Termination phase: Saturation % 295.33/41.93 % (3129149)Time elapsed: 14.070 s % 295.33/41.93 % (3129149)Peak memory usage: 19 MB % 295.33/41.93 % (3129149)Instructions burned: 28121 (million) % 295.33/41.93 % (3129261)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1489081622:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2650 on theBenchmark for (2650ds/2944Mi) % 295.33/41.93 % (3129145)Instruction limit reached! % 295.33/41.93 % (3129145)------------------------------ % 295.33/41.93 % (3129145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.33/41.93 % (3129145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.33/41.93 % (3129145)CaDiCaL version: 2.1.3 % 295.33/41.93 % (3129145)Termination reason: Instruction limit % 295.33/41.93 % (3129145)Termination phase: Saturation % 295.33/41.93 % (3129145)Time elapsed: 14.613 s % 295.33/41.93 % (3129145)Peak memory usage: 43 MB % 295.33/41.93 % (3129145)Instructions burned: 53296 (million) % 295.33/41.93 % (3129263)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1120295480:i=12648:rtra=on_2647 on theBenchmark for (2647ds/12648Mi) % 295.33/41.93 % (3129263)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 295.33/41.93 % (3129263)Terminated due to inappropriate strategy. % 295.33/41.93 % (3129263)------------------------------ % 295.33/41.93 % (3129263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.33/41.93 % (3129263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.33/41.93 % (3129263)CaDiCaL version: 2.1.3 % 295.33/41.93 % (3129263)Termination reason: Inappropriate % 295.33/41.93 % (3129263)Time elapsed: 0.007 s % 295.33/41.93 % (3129263)Peak memory usage: 11 MB % 295.33/41.93 % (3129263)Instructions burned: 31 (million) % 295.33/41.93 % (3129263)------------------------------ % 295.33/41.93 % (3129263)------------------------------ % 295.33/41.93 % (3129265)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3468382095:fmbsr=2.30978:i=4348:rtra=on_2647 on theBenchmark for (2647ds/4348Mi) % 295.33/41.93 % (3129265)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 295.33/41.93 % (3129265)Terminated due to inappropriate strategy. % 295.33/41.93 % (3129265)-----------------Terminated % 300.33/42.64 % Vampire exiting %------------------------------------------------------------------------------