%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV965-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n012.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:26:44 PM UTC 2026 % Result : Timeout 300.57s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWV965-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.00/0.11 % Computer : n012.cluster.edu % 0.00/0.11 % Model : x86_64 x86_64 % 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.11 % Memory : 8046.5625MB % 0.00/0.11 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 13:02:04 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.13 Running first-order model finding % 0.08/0.13 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 % 3.89/0.84 % (3360292)Will run a generic schedule for satisfiability detection. % 3.89/0.84 % (3360298)% WARNING: option uhcvi not known. % 3.89/0.84 % (3360299)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1846806761:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.89/0.84 % (3360297)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=403569886_2999 on theBenchmark for (2999ds/0Mi) % 3.89/0.84 % (3360300)dis+10_1_sil=32000:sp=arity:random_seed=2105471772:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.89/0.84 % (3360298)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=810572717:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.89/0.84 % (3360301)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=364438617:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.89/0.84 % (3360302)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3605383778:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.89/0.84 % (3360303)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3998494216:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.89/0.84 % (3360300)Instruction limit reached! % 3.89/0.84 % (3360300)------------------------------ % 3.89/0.84 % (3360300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.89/0.84 % (3360300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.89/0.84 % (3360300)CaDiCaL version: 2.1.3 % 3.89/0.84 % (3360300)Termination reason: Instruction limit % 3.89/0.84 % (3360300)Termination phase: Saturation % 3.89/0.84 % (3360300)Time elapsed: 0.029 s % 3.89/0.84 % (3360300)Peak memory usage: 12 MB % 3.89/0.84 % (3360300)Instructions burned: 104 (million) % 3.89/0.84 % (3360301)Instruction limit reached! % 3.89/0.84 % (3360301)------------------------------ % 3.89/0.84 % (3360301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.89/0.84 % (3360301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.89/0.84 % (3360301)CaDiCaL version: 2.1.3 % 3.89/0.84 % (3360301)Termination reason: Instruction limit % 3.89/0.84 % (3360301)Termination phase: Saturation % 3.89/0.84 % (3360301)Time elapsed: 0.031 s % 3.89/0.84 % (3360301)Peak memory usage: 12 MB % 3.89/0.84 % (3360301)Instructions burned: 117 (million) % 3.89/0.84 % (3360303)Instruction limit reached! % 3.89/0.84 % (3360303)------------------------------ % 3.89/0.84 % (3360303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.89/0.84 % (3360303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.89/0.84 % (3360303)CaDiCaL version: 2.1.3 % 3.89/0.84 % (3360303)Termination reason: Instruction limit % 3.89/0.84 % (3360303)Termination phase: Saturation % 3.89/0.84 % (3360303)Time elapsed: 0.032 s % 3.89/0.84 % (3360303)Peak memory usage: 12 MB % 3.89/0.84 % (3360303)Instructions burned: 163 (million) % 3.89/0.84 % Detected minimum model sizes of [4] % 3.89/0.84 % Detected maximum model sizes of [max] % 3.89/0.84 % TRYING [4] % 3.89/0.84 % (3360302)Instruction limit reached! % 3.89/0.84 % (3360302)------------------------------ % 3.89/0.84 % (3360302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.89/0.84 % (3360302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.89/0.84 % (3360302)CaDiCaL version: 2.1.3 % 3.89/0.84 % (3360302)Termination reason: Instruction limit % 3.89/0.84 % (3360302)Termination phase: Saturation % 3.89/0.84 % (3360302)Time elapsed: 0.037 s % 3.89/0.84 % (3360302)Peak memory usage: 12 MB % 3.89/0.84 % (3360302)Instructions burned: 134 (million) % 3.89/0.84 % (3360311)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=622224894:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.89/0.84 % (3360312)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3820113735:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.89/0.84 % (3360313)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=3750150162:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.89/0.84 % (3360314)ott-21_1_sil=16000:fs=off:random_seed=2429056662:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.89/0.84 % Detected minimum model sizes of [4] % 3.89/0.84 % Detected maximum model sizes of [max] % 3.89/0.84 % TRYING [4] % 3.89/0.84 % (3360312)Instruction limit reached! % 3.89/0.84 % (3360312)------------------------------ % 3.89/0.84 % (3360312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.44/1.86 % (3360312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/1.86 % (3360312)CaDiCaL version: 2.1.3 % 10.44/1.86 % (3360312)Termination reason: Instruction limit % 10.44/1.86 % (3360312)Termination phase: Saturation % 10.44/1.86 % (3360312)Time elapsed: 0.036 s % 10.44/1.86 % (3360312)Peak memory usage: 12 MB % 10.44/1.86 % (3360312)Instructions burned: 134 (million) % 10.44/1.86 % (3360319)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2852696302:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 10.44/1.86 % (3360314)Instruction limit reached! % 10.44/1.86 % (3360314)------------------------------ % 10.44/1.86 % (3360314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.44/1.86 % (3360314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/1.86 % (3360314)CaDiCaL version: 2.1.3 % 10.44/1.86 % (3360314)Termination reason: Instruction limit % 10.44/1.86 % (3360314)Termination phase: Saturation % 10.44/1.86 % (3360314)Time elapsed: 0.047 s % 10.44/1.86 % (3360314)Peak memory usage: 12 MB % 10.44/1.86 % (3360314)Instructions burned: 181 (million) % 10.44/1.86 % (3360321)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2415617396:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 10.44/1.86 % Detected minimum model sizes of [4] % 10.44/1.86 % Detected maximum model sizes of [max] % 10.44/1.86 % (3360311)Instruction limit reached! % 10.44/1.86 % (3360311)------------------------------ % 10.44/1.86 % (3360311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.44/1.86 % (3360311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/1.86 % (3360311)CaDiCaL version: 2.1.3 % 10.44/1.86 % (3360311)Termination reason: Instruction limit % 10.44/1.86 % (3360311)Termination phase: Finite model building constraint generation % 10.44/1.86 % (3360311)Time elapsed: 0.134 s % 10.44/1.86 % (3360311)Peak memory usage: 33 MB % 10.44/1.86 % (3360311)Instructions burned: 719 (million) % 10.44/1.86 % (3360323)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=166356141:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 10.44/1.86 % (3360313)Instruction limit reached! % 10.44/1.86 % (3360313)------------------------------ % 10.44/1.86 % (3360313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.44/1.86 % (3360313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/1.86 % (3360313)CaDiCaL version: 2.1.3 % 10.44/1.86 % (3360313)Termination reason: Instruction limit % 10.44/1.86 % (3360313)Termination phase: Saturation % 10.44/1.86 % (3360313)Time elapsed: 0.180 s % 10.44/1.86 % (3360313)Peak memory usage: 15 MB % 10.44/1.86 % (3360313)Instructions burned: 686 (million) % 10.44/1.86 % (3360319)Instruction limit reached! % 10.44/1.86 % (3360319)------------------------------ % 10.44/1.86 % (3360319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.44/1.86 % (3360319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/1.86 % (3360319)CaDiCaL version: 2.1.3 % 10.44/1.86 % (3360319)Termination reason: Instruction limit % 10.44/1.86 % (3360319)Termination phase: Saturation % 10.44/1.86 % (3360319)Time elapsed: 0.137 s % 10.44/1.86 % (3360319)Peak memory usage: 14 MB % 10.44/1.86 % (3360319)Instructions burned: 478 (million) % 10.44/1.86 % (3360325)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4134723710:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 10.44/1.86 % (3360326)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=3602391489:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 10.44/1.86 % (3360325)Cannot represent all propositional literals internally % 10.44/1.86 % (3360325)Refutation not found, incomplete strategy % 10.44/1.86 % (3360325)------------------------------ % 10.44/1.86 % (3360325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.44/1.86 % (3360325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.44/1.86 % (3360325)CaDiCaL version: 2.1.3 % 10.44/1.86 % (3360325)Termination reason: Refutation not found, incomplete strategy % 10.44/1.86 % (3360325)Time elapsed: 0.032 s % 10.44/1.86 % (3360325)Peak memory usage: 12 MB % 10.44/1.86 % (3360325)Instructions burned: 126 (million) % 10.44/1.86 % (3360325)------------------------------ % 10.44/1.86 % (3360325)------------------------------ % 10.44/1.86 % (3360329)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=922583829:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 50.39/7.31 % (3360321)Instruction limit reached! % 50.39/7.31 % (3360321)------------------------------ % 50.39/7.31 % (3360321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.39/7.31 % (3360321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.39/7.31 % (3360321)CaDiCaL version: 2.1.3 % 50.39/7.31 % (3360321)Termination reason: Instruction limit % 50.39/7.31 % (3360321)Termination phase: Finite model building constraint generation % 50.39/7.31 % (3360321)Time elapsed: 0.241 s % 50.39/7.31 % (3360321)Peak memory usage: 99 MB % 50.39/7.31 % (3360321)Instructions burned: 867 (million) % 50.39/7.31 % (3360331)fmb+10_1_sil=64000:random_seed=2880854521:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 50.39/7.31 % Detected minimum model sizes of [4] % 50.39/7.31 % Detected maximum model sizes of [max] % 50.39/7.31 % (3360326)Instruction limit reached! % 50.39/7.31 % (3360326)------------------------------ % 50.39/7.31 % (3360326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.39/7.31 % (3360326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.39/7.31 % (3360326)CaDiCaL version: 2.1.3 % 50.39/7.31 % (3360326)Termination reason: Instruction limit % 50.39/7.31 % (3360326)Termination phase: Saturation % 50.39/7.31 % (3360326)Time elapsed: 0.220 s % 50.39/7.31 % (3360326)Peak memory usage: 21 MB % 50.39/7.31 % (3360326)Instructions burned: 693 (million) % 50.39/7.31 % (3360333)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=146113810:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 50.39/7.31 % (3360323)Instruction limit reached! % 50.39/7.31 % (3360323)------------------------------ % 50.39/7.31 % (3360323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.39/7.31 % (3360323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.39/7.31 % (3360323)CaDiCaL version: 2.1.3 % 50.39/7.31 % (3360323)Termination reason: Instruction limit % 50.39/7.31 % (3360323)Termination phase: Saturation % 50.39/7.31 % (3360323)Time elapsed: 0.289 s % 50.39/7.31 % (3360323)Peak memory usage: 15 MB % 50.39/7.31 % (3360323)Instructions burned: 1181 (million) % 50.39/7.31 % (3360335)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1629653594:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 50.39/7.31 % Detected minimum model sizes of [4] % 50.39/7.31 % Detected maximum model sizes of [max] % 50.39/7.31 % (3360333)Cannot represent all propositional literals internally % 50.39/7.31 % (3360333)Refutation not found, incomplete strategy % 50.39/7.31 % (3360333)------------------------------ % 50.39/7.31 % (3360333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.39/7.31 % (3360333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.39/7.31 % (3360333)CaDiCaL version: 2.1.3 % 50.39/7.31 % (3360333)Termination reason: Refutation not found, incomplete strategy % 50.39/7.31 % (3360333)Time elapsed: 0.032 s % 50.39/7.31 % (3360333)Peak memory usage: 12 MB % 50.39/7.31 % (3360333)Instructions burned: 121 (million) % 50.39/7.31 % (3360333)------------------------------ % 50.39/7.31 % (3360333)------------------------------ % 50.39/7.31 % (3360337)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=722802897:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 50.39/7.31 % (3360329)Instruction limit reached! % 50.39/7.31 % (3360329)------------------------------ % 50.39/7.31 % (3360329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.39/7.31 % (3360329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.39/7.31 % (3360329)CaDiCaL version: 2.1.3 % 50.39/7.31 % (3360329)Termination reason: Instruction limit % 50.39/7.31 % (3360329)Termination phase: Saturation % 50.39/7.31 % (3360329)Time elapsed: 0.239 s % 50.39/7.31 % (3360329)Peak memory usage: 17 MB % 50.39/7.31 % (3360329)Instructions burned: 881 (million) % 50.39/7.31 % Detected minimum model sizes of [4] % 50.39/7.31 % Detected maximum model sizes of [max] % 50.39/7.31 % TRYING [8] % 50.39/7.31 % (3360339)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1791742654:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 50.39/7.31 % (3360335)Instruction limit reached! % 50.39/7.31 % (3360335)------------------------------ % 50.39/7.31 % (3360335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.39/7.31 % (3360335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.57/11.31 % (3360335)CaDiCaL version: 2.1.3 % 78.57/11.31 % (3360335)Termination reason: Instruction limit % 78.57/11.31 % (3360335)Termination phase: Finite model building constraint generation % 78.57/11.31 % (3360335)Time elapsed: 0.182 s % 78.57/11.31 % (3360335)Peak memory usage: 60 MB % 78.57/11.31 % (3360335)Instructions burned: 923 (million) % 78.57/11.31 % (3360341)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3035299434:i=6324_2992 on theBenchmark for (2992ds/6324Mi) % 78.57/11.31 % Detected minimum model sizes of [4] % 78.57/11.31 % Detected maximum model sizes of [max] % 78.57/11.31 % (3360341)Cannot represent all propositional literals internally % 78.57/11.31 % (3360341)Refutation not found, incomplete strategy % 78.57/11.31 % (3360341)------------------------------ % 78.57/11.31 % (3360341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 78.57/11.31 % (3360341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.57/11.31 % (3360341)CaDiCaL version: 2.1.3 % 78.57/11.31 % (3360341)Termination reason: Refutation not found, incomplete strategy % 78.57/11.31 % (3360341)Time elapsed: 0.034 s % 78.57/11.31 % (3360341)Peak memory usage: 12 MB % 78.57/11.31 % (3360341)Instructions burned: 131 (million) % 78.57/11.31 % (3360341)------------------------------ % 78.57/11.31 % (3360341)------------------------------ % 78.57/11.31 % (3360343)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3568882006:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 78.57/11.31 % (3360339)Instruction limit reached! % 78.57/11.31 % (3360339)------------------------------ % 78.57/11.31 % (3360339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 78.57/11.31 % (3360339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.57/11.31 % (3360339)CaDiCaL version: 2.1.3 % 78.57/11.31 % (3360339)Termination reason: Instruction limit % 78.57/11.31 % (3360339)Termination phase: Saturation % 78.57/11.31 % (3360339)Time elapsed: 0.408 s % 78.57/11.31 % (3360339)Peak memory usage: 23 MB % 78.57/11.31 % (3360339)Instructions burned: 1474 (million) % 78.57/11.31 % Detected minimum model sizes of [4] % 78.57/11.31 % Detected maximum model sizes of [max] % 78.57/11.31 % (3360343)Cannot represent all propositional literals internally % 78.57/11.31 % (3360343)Refutation not found, incomplete strategy % 78.57/11.31 % (3360343)------------------------------ % 78.57/11.31 % (3360343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 78.57/11.31 % (3360343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.57/11.31 % (3360343)CaDiCaL version: 2.1.3 % 78.57/11.31 % (3360343)Termination reason: Refutation not found, incomplete strategy % 78.57/11.31 % (3360343)Time elapsed: 0.204 s % 78.57/11.31 % (3360343)Peak memory usage: 18 MB % 78.57/11.31 % (3360343)Instructions burned: 777 (million) % 78.57/11.31 % (3360343)------------------------------ % 78.57/11.31 % (3360343)------------------------------ % 78.57/11.31 % (3360345)ott-2_1_sil=16000:newcnf=on:random_seed=2721781410:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 78.57/11.31 % (3360346)ott+10_1_sil=32000:tgt=ground:random_seed=414801555:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi) % 78.57/11.31 % TRYING [4] % 78.57/11.31 % (3360345)Instruction limit reached! % 78.57/11.31 % (3360345)------------------------------ % 78.57/11.31 % (3360345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 78.57/11.31 % (3360345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.57/11.31 % (3360345)CaDiCaL version: 2.1.3 % 78.57/11.31 % (3360345)Termination reason: Instruction limit % 78.57/11.31 % (3360345)Termination phase: Saturation % 78.57/11.31 % (3360345)Time elapsed: 0.183 s % 78.57/11.31 % (3360345)Peak memory usage: 12 MB % 78.57/11.31 % (3360345)Instructions burned: 871 (million) % 78.57/11.31 % (3360349)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1345404710:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 78.57/11.31 % Detected minimum model sizes of [4] % 78.57/11.31 % Detected maximum model sizes of [max] % 78.57/11.31 % TRYING [4] % 78.57/11.31 % (3360337)Instruction limit reached! % 78.57/11.31 % (3360337)------------------------------ % 78.57/11.31 % (3360337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 78.57/11.31 % (3360337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.57/11.31 % (3360337)CaDiCaL version: 2.1.3 % 78.57/11.31 % (3360337)Termination reason: Instruction limit % 78.57/11.31 % (3360337)Termination phase: Saturation % 78.57/11.31 % (3360337)Time elapsed: 1.180 s % 78.57/11.31 % (3360337)Peak memory usage: 23 MB % 78.57/11.31 % (3360337)Instructions burned: 5133 (million) % 125.95/18.09 % (3360351)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2414272423:i=3512:aac=none_2982 on theBenchmark for (2982ds/3512Mi) % 125.95/18.09 % (3360346)Instruction limit reached! % 125.95/18.09 % (3360346)------------------------------ % 125.95/18.09 % (3360346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.95/18.09 % (3360346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.95/18.09 % (3360346)CaDiCaL version: 2.1.3 % 125.95/18.09 % (3360346)Termination reason: Instruction limit % 125.95/18.09 % (3360346)Termination phase: Saturation % 125.95/18.09 % (3360346)Time elapsed: 1.226 s % 125.95/18.09 % (3360346)Peak memory usage: 21 MB % 125.95/18.09 % (3360346)Instructions burned: 5117 (million) % 125.95/18.09 % (3360353)dis+21_1_sil=32000:sas=cadical:random_seed=3759687183:i=3773:amm=off_2977 on theBenchmark for (2977ds/3773Mi) % 125.95/18.09 % (3360351)Instruction limit reached! % 125.95/18.09 % (3360351)------------------------------ % 125.95/18.09 % (3360351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.95/18.09 % (3360351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.95/18.09 % (3360351)CaDiCaL version: 2.1.3 % 125.95/18.09 % (3360351)Termination reason: Instruction limit % 125.95/18.09 % (3360351)Termination phase: Saturation % 125.95/18.09 % (3360351)Time elapsed: 0.803 s % 125.95/18.09 % (3360351)Peak memory usage: 18 MB % 125.95/18.09 % (3360351)Instructions burned: 3514 (million) % 125.95/18.09 % (3360355)ott+11_1_sil=16000:gs=on:random_seed=643405288:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2974 on theBenchmark for (2974ds/2251Mi) % 125.95/18.09 % (3360355)Instruction limit reached! % 125.95/18.09 % (3360355)------------------------------ % 125.95/18.09 % (3360355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.95/18.09 % (3360355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.95/18.09 % (3360355)CaDiCaL version: 2.1.3 % 125.95/18.09 % (3360355)Termination reason: Instruction limit % 125.95/18.09 % (3360355)Termination phase: Saturation % 125.95/18.09 % (3360355)Time elapsed: 0.512 s % 125.95/18.09 % (3360355)Peak memory usage: 15 MB % 125.95/18.09 % (3360355)Instructions burned: 2256 (million) % 125.95/18.09 % (3360357)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3328887868:fmbsr=1.6:i=67534_2969 on theBenchmark for (2969ds/67534Mi) % 125.95/18.09 % (3360353)Instruction limit reached! % 125.95/18.09 % (3360353)------------------------------ % 125.95/18.09 % (3360353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.95/18.09 % (3360353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.95/18.09 % (3360353)CaDiCaL version: 2.1.3 % 125.95/18.09 % (3360353)Termination reason: Instruction limit % 125.95/18.09 % (3360353)Termination phase: Saturation % 125.95/18.09 % (3360353)Time elapsed: 0.886 s % 125.95/18.09 % (3360353)Peak memory usage: 18 MB % 125.95/18.09 % (3360353)Instructions burned: 3777 (million) % 125.95/18.09 % Detected minimum model sizes of [4] % 125.95/18.09 % Detected maximum model sizes of [max] % 125.95/18.09 % (3360359)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1650436440:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2968 on theBenchmark for (2968ds/4591Mi) % 125.95/18.09 % (3360359)Instruction limit reached! % 125.95/18.09 % (3360359)------------------------------ % 125.95/18.09 % (3360359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.95/18.09 % (3360359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.95/18.09 % (3360359)CaDiCaL version: 2.1.3 % 125.95/18.09 % (3360359)Termination reason: Instruction limit % 125.95/18.09 % (3360359)Termination phase: Saturation % 125.95/18.09 % (3360359)Time elapsed: 0.788 s % 125.95/18.09 % (3360359)Peak memory usage: 16 MB % 125.95/18.09 % (3360359)Instructions burned: 4592 (million) % 125.95/18.09 % (3360361)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1053784206:i=29340_2960 on theBenchmark for (2960ds/29340Mi) % 125.95/18.09 % TRYING [5] % 125.95/18.09 % TRYING [5] % 125.95/18.09 % (3360331)Instruction limit reached! % 125.95/18.09 % (3360331)------------------------------ % 125.95/18.09 % (3360331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.95/18.09 % (3360331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.95/18.09 % (3360331)CaDiCaL version: 2.1.3 % 125.95/18.09 % (3360331)Termination reason: Instruction limit % 125.95/18.09 % (3360331)Termination phase: Finite model building SAT solving % 125.95/18.09 % (3360331)Time elapsed: 6.775 s % 151.87/21.96 % (3360331)Peak memory usage: 949 MB % 151.87/21.96 % (3360331)Instructions burned: 22062 (million) % 151.87/21.96 % (3360363)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2925264463:i=5211_2927 on theBenchmark for (2927ds/5211Mi) % 151.87/21.96 % (3360363)Instruction limit reached! % 151.87/21.96 % (3360363)------------------------------ % 151.87/21.96 % (3360363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.87/21.96 % (3360363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.87/21.96 % (3360363)CaDiCaL version: 2.1.3 % 151.87/21.96 % (3360363)Termination reason: Instruction limit % 151.87/21.96 % (3360363)Termination phase: Saturation % 151.87/21.96 % (3360363)Time elapsed: 1.393 s % 151.87/21.96 % (3360363)Peak memory usage: 43 MB % 151.87/21.96 % (3360363)Instructions burned: 5211 (million) % 151.87/21.96 % (3360365)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1058361767:i=5497:nm=2_2913 on theBenchmark for (2913ds/5497Mi) % 151.87/21.96 % Detected minimum model sizes of [4] % 151.87/21.96 % Detected maximum model sizes of [max] % 151.87/21.96 % (3360365)Cannot represent all propositional literals internally % 151.87/21.96 % (3360365)Refutation not found, incomplete strategy % 151.87/21.96 % (3360365)------------------------------ % 151.87/21.96 % (3360365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.87/21.96 % (3360365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.87/21.96 % (3360365)CaDiCaL version: 2.1.3 % 151.87/21.96 % (3360365)Termination reason: Refutation not found, incomplete strategy % 151.87/21.96 % (3360365)Time elapsed: 0.034 s % 151.87/21.96 % (3360365)Peak memory usage: 12 MB % 151.87/21.96 % (3360365)Instructions burned: 131 (million) % 151.87/21.96 % (3360365)------------------------------ % 151.87/21.96 % (3360365)------------------------------ % 151.87/21.96 % (3360367)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3317412114:fmbsr=2:i=46332_2912 on theBenchmark for (2912ds/46332Mi) % 151.87/21.96 % Detected minimum model sizes of [4] % 151.87/21.96 % Detected maximum model sizes of [max] % 151.87/21.96 % (3360367)Cannot represent all propositional literals internally % 151.87/21.96 % (3360367)Refutation not found, incomplete strategy % 151.87/21.96 % (3360367)------------------------------ % 151.87/21.96 % (3360367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.87/21.96 % (3360367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.87/21.96 % (3360367)CaDiCaL version: 2.1.3 % 151.87/21.96 % (3360367)Termination reason: Refutation not found, incomplete strategy % 151.87/21.96 % (3360367)Time elapsed: 0.035 s % 151.87/21.96 % (3360367)Peak memory usage: 12 MB % 151.87/21.96 % (3360367)Instructions burned: 141 (million) % 151.87/21.96 % (3360367)------------------------------ % 151.87/21.96 % (3360367)------------------------------ % 151.87/21.96 % (3360369)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2928249023:i=14071_2912 on theBenchmark for (2912ds/14071Mi) % 151.87/21.96 % Detected minimum model sizes of [4] % 151.87/21.96 % Detected maximum model sizes of [max] % 151.87/21.96 % (3360369)Cannot represent all propositional literals internally % 151.87/21.96 % (3360369)Refutation not found, incomplete strategy % 151.87/21.96 % (3360369)------------------------------ % 151.87/21.96 % (3360369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.87/21.96 % (3360369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.87/21.96 % (3360369)CaDiCaL version: 2.1.3 % 151.87/21.96 % (3360369)Termination reason: Refutation not found, incomplete strategy % 151.87/21.96 % (3360369)Time elapsed: 0.032 s % 151.87/21.96 % (3360369)Peak memory usage: 12 MB % 151.87/21.96 % (3360369)Instructions burned: 121 (million) % 151.87/21.96 % (3360369)------------------------------ % 151.87/21.96 % (3360369)------------------------------ % 151.87/21.96 % (3360371)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=620067957:i=22565:add=on:rawr=on_2911 on theBenchmark for (2911ds/22565Mi) % 151.87/21.96 % (3360361)Instruction limit reached! % 151.87/21.96 % (3360361)------------------------------ % 151.87/21.96 % (3360361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.87/21.96 % (3360361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.87/21.96 % (3360361)CaDiCaL version: 2.1.3 % 151.87/21.96 % (3360361)Termination reason: Instruction limit % 151.87/21.96 % (3360361)Termination phase: Saturation % 151.87/21.96 % (3360361)Time elapsed: 7.247 s % 151.87/21.96 % (3360361)Peak memory usage: 182 MB % 151.87/21.96 % (3360361)Instructions burned: 29343 (million) % 177.95/25.49 % (3360373)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=798921987:i=8173:av=off_2888 on theBenchmark for (2888ds/8173Mi) % 177.95/25.49 % (3360373)Instruction limit reached! % 177.95/25.49 % (3360373)------------------------------ % 177.95/25.49 % (3360373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.95/25.49 % (3360373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.95/25.49 % (3360373)CaDiCaL version: 2.1.3 % 177.95/25.49 % (3360373)Termination reason: Instruction limit % 177.95/25.49 % (3360373)Termination phase: Saturation % 177.95/25.49 % (3360373)Time elapsed: 1.967 s % 177.95/25.49 % (3360373)Peak memory usage: 27 MB % 177.95/25.49 % (3360373)Instructions burned: 8177 (million) % 177.95/25.49 % (3360375)dis+10_16:1_sil=16000:random_seed=1296840159:i=9155:fsr=off_2868 on theBenchmark for (2868ds/9155Mi) % 177.95/25.49 % (3360349)Instruction limit reached! % 177.95/25.49 % (3360349)------------------------------ % 177.95/25.49 % (3360349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.95/25.49 % (3360349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.95/25.49 % (3360349)CaDiCaL version: 2.1.3 % 177.95/25.49 % (3360349)Termination reason: Instruction limit % 177.95/25.49 % (3360349)Termination phase: Finite model building constraint generation % 177.95/25.49 % (3360349)Time elapsed: 12.404 s % 177.95/25.49 % (3360349)Peak memory usage: 2551 MB % 177.95/25.49 % (3360349)Instructions burned: 54283 (million) % 177.95/25.49 % (3360377)ott-3_8_sil=64000:random_seed=1241589926:i=20139:bs=on_2862 on theBenchmark for (2862ds/20139Mi) % 177.95/25.49 % (3360371)Instruction limit reached! % 177.95/25.49 % (3360371)------------------------------ % 177.95/25.49 % (3360371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.95/25.49 % (3360371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.95/25.49 % (3360371)CaDiCaL version: 2.1.3 % 177.95/25.49 % (3360371)Termination reason: Instruction limit % 177.95/25.49 % (3360371)Termination phase: Saturation % 177.95/25.49 % (3360371)Time elapsed: 5.636 s % 177.95/25.49 % (3360371)Peak memory usage: 63 MB % 177.95/25.49 % (3360371)Instructions burned: 22565 (million) % 177.95/25.49 % (3360379)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1787657714:fmbsr=2:i=32576_2855 on theBenchmark for (2855ds/32576Mi) % 177.95/25.49 % Detected minimum model sizes of [4] % 177.95/25.49 % Detected maximum model sizes of [max] % 177.95/25.49 % TRYING [9] % 177.95/25.49 % (3360375)Instruction limit reached! % 177.95/25.49 % (3360375)------------------------------ % 177.95/25.49 % (3360375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.95/25.49 % (3360375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.95/25.49 % (3360375)CaDiCaL version: 2.1.3 % 177.95/25.49 % (3360375)Termination reason: Instruction limit % 177.95/25.49 % (3360375)Termination phase: Saturation % 177.95/25.49 % (3360375)Time elapsed: 2.079 s % 177.95/25.49 % (3360375)Peak memory usage: 29 MB % 177.95/25.49 % (3360375)Instructions burned: 9157 (million) % 177.95/25.49 % (3360381)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1803186796:i=11404_2847 on theBenchmark for (2847ds/11404Mi) % 177.95/25.49 % (3360377)Instruction limit reached! % 177.95/25.49 % (3360377)------------------------------ % 177.95/25.49 % (3360377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.95/25.49 % (3360377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.95/25.49 % (3360377)CaDiCaL version: 2.1.3 % 177.95/25.49 % (3360377)Termination reason: Instruction limit % 177.95/25.49 % (3360377)Termination phase: Saturation % 177.95/25.49 % (3360377)Time elapsed: 3.081 s % 177.95/25.49 % (3360377)Peak memory usage: 12 MB % 177.95/25.49 % (3360377)Instructions burned: 20147 (million) % 177.95/25.49 % (3360383)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1765595024:i=14134_2831 on theBenchmark for (2831ds/14134Mi) % 177.95/25.49 % (3360381)Instruction limit reached! % 177.95/25.49 % (3360381)------------------------------ % 177.95/25.49 % (3360381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.95/25.49 % (3360381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.95/25.49 % (3360381)CaDiCaL version: 2.1.3 % 177.95/25.49 % (3360381)Termination reason: Instruction limit % 177.95/25.49 % (3360381)Termination phase: Saturation % 177.95/25.49 % (3360381)Time elapsed: 2.665 s % 177.95/25.49 % (3360381)Peak memory usage: 23 MB % 177.95/25.49 % (3360381)Instructions burned: 11408 (million) % 177.95/25.49 % (3360385)dis+33_16_sil=32000:sac=on:random_seed=1292721447:i=15851:nm=0_2820 on theBenchmark for (2820ds/15851Mi) % 223.77/31.95 % (3360383)Instruction limit reached! % 223.77/31.95 % (3360383)------------------------------ % 223.77/31.95 % (3360383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.77/31.95 % (3360383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.77/31.95 % (3360383)CaDiCaL version: 2.1.3 % 223.77/31.95 % (3360383)Termination reason: Instruction limit % 223.77/31.95 % (3360383)Termination phase: Saturation % 223.77/31.95 % (3360383)Time elapsed: 2.420 s % 223.77/31.95 % (3360383)Peak memory usage: 14 MB % 223.77/31.95 % (3360383)Instructions burned: 14137 (million) % 223.77/31.95 % (3360387)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=179496217:avsq=on:i=17627:add=on:amm=off_2806 on theBenchmark for (2806ds/17627Mi) % 223.77/31.95 % (3360357)Instruction limit reached! % 223.77/31.95 % (3360357)------------------------------ % 223.77/31.95 % (3360357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.77/31.95 % (3360357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.77/31.95 % (3360357)CaDiCaL version: 2.1.3 % 223.77/31.95 % (3360357)Termination reason: Instruction limit % 223.77/31.95 % (3360357)Termination phase: Finite model building constraint generation % 223.77/31.95 % (3360357)Time elapsed: 16.265 s % 223.77/31.95 % (3360357)Peak memory usage: 6498 MB % 223.77/31.95 % (3360357)Instructions burned: 67539 (million) % 223.77/31.95 % (3360389)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2191063957:s2a=on:i=53295_2798 on theBenchmark for (2798ds/53295Mi) % 223.77/31.95 % (3360379)Instruction limit reached! % 223.77/31.95 % (3360379)------------------------------ % 223.77/31.95 % (3360379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.77/31.95 % (3360379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.77/31.95 % (3360379)CaDiCaL version: 2.1.3 % 223.77/31.95 % (3360379)Termination reason: Instruction limit % 223.77/31.95 % (3360379)Termination phase: Finite model building constraint generation % 223.77/31.95 % (3360379)Time elapsed: 6.399 s % 223.77/31.95 % (3360379)Peak memory usage: 2085 MB % 223.77/31.95 % (3360379)Instructions burned: 32579 (million) % 223.77/31.95 % (3360299)Instruction limit reached! % 223.77/31.95 % (3360299)------------------------------ % 223.77/31.95 % (3360299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.77/31.95 % (3360299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.77/31.95 % (3360299)CaDiCaL version: 2.1.3 % 223.77/31.95 % (3360299)Termination reason: Instruction limit % 223.77/31.95 % (3360299)Termination phase: Saturation % 223.77/31.95 % (3360299)Time elapsed: 20.994 s % 223.77/31.95 % (3360299)Peak memory usage: 84 MB % 223.77/31.95 % (3360299)Instructions burned: 88026 (million) % 223.77/31.95 % (3360391)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2911030533:i=26857:ins=20_2789 on theBenchmark for (2789ds/26857Mi) % 223.77/31.95 % (3360392)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=190354034:i=28120:bs=on:fsr=off_2789 on theBenchmark for (2789ds/28120Mi) % 223.77/31.95 % Detected minimum model sizes of [4] % 223.77/31.95 % Detected maximum model sizes of [max] % 223.77/31.95 % (3360391)Cannot represent all propositional literals internally % 223.77/31.95 % (3360391)Refutation not found, incomplete strategy % 223.77/31.95 % (3360391)------------------------------ % 223.77/31.95 % (3360391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.77/31.95 % (3360391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.77/31.95 % (3360391)CaDiCaL version: 2.1.3 % 223.77/31.95 % (3360391)Termination reason: Refutation not found, incomplete strategy % 223.77/31.95 % (3360391)Time elapsed: 0.032 s % 223.77/31.95 % (3360391)Peak memory usage: 12 MB % 223.77/31.95 % (3360391)Instructions burned: 121 (million) % 223.77/31.95 % (3360391)------------------------------ % 223.77/31.95 % (3360391)------------------------------ % 223.77/31.95 % (3360395)fmb+10_1_sil=256000:fmbss=7:random_seed=1812498503:fmbsr=1.6:i=182295_2789 on theBenchmark for (2789ds/182295Mi) % 223.77/31.95 % Detected minimum model sizes of [4] % 223.77/31.95 % Detected maximum model sizes of [max] % 223.77/31.95 % (3360385)Instruction limit reached! % 223.77/31.95 % (3360385)------------------------------ % 223.77/31.95 % (3360385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.77/31.95 % (3360385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.77/31.95 % (3360385)CaDiCaL version: 2.1.3 % 223.77/31.95 % (3360385)Termination reason: Instruction limit % 223.77/31.95 % (3360385)Termination phase: Saturation % 232.35/33.14 % (3360385)Time elapsed: 3.874 s % 232.35/33.14 % (3360385)Peak memory usage: 71 MB % 232.35/33.14 % (3360385)Instructions burned: 15851 (million) % 232.35/33.14 % (3360397)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3564351272:i=44625:gsp=on_2781 on theBenchmark for (2781ds/44625Mi) % 232.35/33.14 % Detected minimum model sizes of [4] % 232.35/33.14 % Detected maximum model sizes of [max] % 232.35/33.14 % (3360397)Cannot represent all propositional literals internally % 232.35/33.14 % (3360397)Refutation not found, incomplete strategy % 232.35/33.14 % (3360397)------------------------------ % 232.35/33.14 % (3360397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.35/33.14 % (3360397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.35/33.14 % (3360397)CaDiCaL version: 2.1.3 % 232.35/33.14 % (3360397)Termination reason: Refutation not found, incomplete strategy % 232.35/33.14 % (3360397)Time elapsed: 0.034 s % 232.35/33.14 % (3360397)Peak memory usage: 12 MB % 232.35/33.14 % (3360397)Instructions burned: 128 (million) % 232.35/33.14 % (3360397)------------------------------ % 232.35/33.14 % (3360397)------------------------------ % 232.35/33.14 % (3360399)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2072311203:i=160505_2781 on theBenchmark for (2781ds/160505Mi) % 232.35/33.14 % Detected minimum model sizes of [4] % 232.35/33.14 % Detected maximum model sizes of [max] % 232.35/33.14 % (3360399)Cannot represent all propositional literals internally % 232.35/33.14 % (3360399)Refutation not found, incomplete strategy % 232.35/33.14 % (3360399)------------------------------ % 232.35/33.14 % (3360399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.35/33.14 % (3360399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.35/33.14 % (3360399)CaDiCaL version: 2.1.3 % 232.35/33.14 % (3360399)Termination reason: Refutation not found, incomplete strategy % 232.35/33.14 % (3360399)Time elapsed: 0.032 s % 232.35/33.14 % (3360399)Peak memory usage: 12 MB % 232.35/33.14 % (3360399)Instructions burned: 121 (million) % 232.35/33.14 % (3360399)------------------------------ % 232.35/33.14 % (3360399)------------------------------ % 232.35/33.14 % (3360401)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3474760297:fmbsr=1.3:i=225729_2780 on theBenchmark for (2780ds/225729Mi) % 232.35/33.14 % Detected minimum model sizes of [4] % 232.35/33.14 % Detected maximum model sizes of [max] % 232.35/33.14 % (3360401)Cannot represent all propositional literals internally % 232.35/33.14 % (3360401)Refutation not found, incomplete strategy % 232.35/33.14 % (3360401)------------------------------ % 232.35/33.14 % (3360401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.35/33.14 % (3360401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.35/33.14 % (3360401)CaDiCaL version: 2.1.3 % 232.35/33.14 % (3360401)Termination reason: Refutation not found, incomplete strategy % 232.35/33.14 % (3360401)Time elapsed: 0.032 s % 232.35/33.14 % (3360401)Peak memory usage: 12 MB % 232.35/33.14 % (3360401)Instructions burned: 121 (million) % 232.35/33.14 % (3360401)------------------------------ % 232.35/33.14 % (3360401)------------------------------ % 232.35/33.14 % (3360403)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1747339313:fmbsr=2:i=185024:ins=7_2780 on theBenchmark for (2780ds/185024Mi) % 232.35/33.14 % Detected minimum model sizes of [4] % 232.35/33.14 % Detected maximum model sizes of [max] % 232.35/33.14 % (3360403)Cannot represent all propositional literals internally % 232.35/33.14 % (3360403)Refutation not found, incomplete strategy % 232.35/33.14 % (3360403)------------------------------ % 232.35/33.14 % (3360403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.35/33.14 % (3360403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.35/33.14 % (3360403)CaDiCaL version: 2.1.3 % 232.35/33.14 % (3360403)Termination reason: Refutation not found, incomplete strategy % 232.35/33.14 % (3360403)Time elapsed: 0.032 s % 232.35/33.14 % (3360403)Peak memory usage: 12 MB % 232.35/33.14 % (3360403)Instructions burned: 121 (million) % 232.35/33.14 % (3360403)------------------------------ % 232.35/33.14 % (3360403)------------------------------ % 232.35/33.14 % (3360405)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1957945773:rtra=on_2779 on theBenchmark for (2779ds/0Mi) % 232.35/33.14 % Detected minimum model sizes of [4] % 232.35/33.14 % Detected maximum model sizes of [max] % 232.35/33.14 % TRYING [4] % 232.35/33.14 % (3360387)Instruction limit reached! % 232.35/33.14 % (3360387)------------------------------ % 232.35/33.14 % (3360387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 232.35/33.14 % (3360387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.50/36.17 % (3360387)CaDiCaL version: 2.1.3 % 253.50/36.17 % (3360387)Termination reason: Instruction limit % 253.50/36.17 % (3360387)Termination phase: Saturation % 253.50/36.17 % (3360387)Time elapsed: 6.033 s % 253.50/36.17 % (3360387)Peak memory usage: 484 MB % 253.50/36.17 % (3360387)Instructions burned: 17630 (million) % 253.50/36.17 % (3360407)% WARNING: option uhcvi not known. % 253.50/36.17 % (3360407)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=794445805:i=271062:add=off:rtra=on:rawr=on_2746 on theBenchmark for (2746ds/271062Mi) % 253.50/36.17 % (3360392)Instruction limit reached! % 253.50/36.17 % (3360392)------------------------------ % 253.50/36.17 % (3360392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.50/36.17 % (3360392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.50/36.17 % (3360392)CaDiCaL version: 2.1.3 % 253.50/36.17 % (3360392)Termination reason: Instruction limit % 253.50/36.17 % (3360392)Termination phase: Saturation % 253.50/36.17 % (3360392)Time elapsed: 5.562 s % 253.50/36.17 % (3360392)Peak memory usage: 31 MB % 253.50/36.17 % (3360392)Instructions burned: 28123 (million) % 253.50/36.17 % (3360409)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1222577799:i=176048:add=on:rtra=on:rawr=on_2733 on theBenchmark for (2733ds/176048Mi) % 253.50/36.17 % (3360298)Instruction limit reached! % 253.50/36.17 % (3360298)------------------------------ % 253.50/36.17 % (3360298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.50/36.17 % (3360298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.50/36.17 % (3360298)CaDiCaL version: 2.1.3 % 253.50/36.17 % (3360298)Termination reason: Instruction limit % 253.50/36.17 % (3360298)Termination phase: Saturation % 253.50/36.17 % (3360298)Time elapsed: 31.464 s % 253.50/36.17 % (3360298)Peak memory usage: 235 MB % 253.50/36.17 % (3360298)Instructions burned: 135532 (million) % 253.50/36.17 % (3360412)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3311287515:i=206:fgj=on:rtra=on_2684 on theBenchmark for (2684ds/206Mi) % 253.50/36.17 % (3360412)Instruction limit reached! % 253.50/36.17 % (3360412)------------------------------ % 253.50/36.17 % (3360412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.50/36.17 % (3360412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.50/36.17 % (3360412)CaDiCaL version: 2.1.3 % 253.50/36.17 % (3360412)Termination reason: Instruction limit % 253.50/36.17 % (3360412)Termination phase: Saturation % 253.50/36.17 % (3360412)Time elapsed: 0.057 s % 253.50/36.17 % (3360412)Peak memory usage: 12 MB % 253.50/36.17 % (3360412)Instructions burned: 208 (million) % 253.50/36.17 % (3360414)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=804486957:i=232:rtra=on_2684 on theBenchmark for (2684ds/232Mi) % 253.50/36.17 % (3360414)Instruction limit reached! % 253.50/36.17 % (3360414)------------------------------ % 253.50/36.17 % (3360414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.50/36.17 % (3360414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.50/36.17 % (3360414)CaDiCaL version: 2.1.3 % 253.50/36.17 % (3360414)Termination reason: Instruction limit % 253.50/36.17 % (3360414)Termination phase: Saturation % 253.50/36.17 % (3360414)Time elapsed: 0.065 s % 253.50/36.17 % (3360414)Peak memory usage: 13 MB % 253.50/36.17 % (3360414)Instructions burned: 233 (million) % 253.50/36.17 % (3360416)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=144704530:i=262:rtra=on_2683 on theBenchmark for (2683ds/262Mi) % 253.50/36.17 % (3360416)Instruction limit reached! % 253.50/36.17 % (3360416)------------------------------ % 253.50/36.17 % (3360416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.50/36.17 % (3360416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.50/36.17 % (3360416)CaDiCaL version: 2.1.3 % 253.50/36.17 % (3360416)Termination reason: Instruction limit % 253.50/36.17 % (3360416)Termination phase: Saturation % 253.50/36.17 % (3360416)Time elapsed: 0.076 s % 253.50/36.17 % (3360416)Peak memory usage: 13 MB % 253.50/36.17 % (3360416)Instructions burned: 265 (million) % 253.50/36.17 % (3360418)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3441244208:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2682 on theBenchmark for (2682ds/318Mi) % 253.50/36.17 % (3360418)Instruction limit reached! % 253.50/36.17 % (3360418)------------------------------ % 253.50/36.17 % (3360418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.50/36.17 % (3360418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.26/40.21 % (3360418)CaDiCaL version: 2.1.3 % 282.26/40.21 % (3360418)Termination reason: Instruction limit % 282.26/40.21 % (3360418)Termination phase: Saturation % 282.26/40.21 % (3360418)Time elapsed: 0.059 s % 282.26/40.21 % (3360418)Peak memory usage: 12 MB % 282.26/40.21 % (3360418)Instructions burned: 324 (million) % 282.26/40.21 % (3360420)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=60472684:i=1428:nm=2:rtra=on_2681 on theBenchmark for (2681ds/1428Mi) % 282.26/40.21 % Detected minimum model sizes of [4] % 282.26/40.21 % Detected maximum model sizes of [max] % 282.26/40.21 % TRYING [4] % 282.26/40.21 % (3360420)Instruction limit reached! % 282.26/40.21 % (3360420)------------------------------ % 282.26/40.21 % (3360420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.26/40.21 % (3360420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.26/40.21 % (3360420)CaDiCaL version: 2.1.3 % 282.26/40.21 % (3360420)Termination reason: Instruction limit % 282.26/40.21 % (3360420)Termination phase: Finite model building constraint generation % 282.26/40.21 % (3360420)Time elapsed: 0.263 s % 282.26/40.21 % (3360420)Peak memory usage: 53 MB % 282.26/40.21 % (3360420)Instructions burned: 1433 (million) % 282.26/40.21 % (3360422)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=335821570:i=262:bd=preordered:rtra=on:fsd=on_2678 on theBenchmark for (2678ds/262Mi) % 282.26/40.21 % (3360422)Instruction limit reached! % 282.26/40.21 % (3360422)------------------------------ % 282.26/40.21 % (3360422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.26/40.21 % (3360422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.26/40.21 % (3360422)CaDiCaL version: 2.1.3 % 282.26/40.21 % (3360422)Termination reason: Instruction limit % 282.26/40.21 % (3360422)Termination phase: Saturation % 282.26/40.21 % (3360422)Time elapsed: 0.075 s % 282.26/40.21 % (3360422)Peak memory usage: 13 MB % 282.26/40.21 % (3360422)Instructions burned: 262 (million) % 282.26/40.21 % (3360424)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=1850606833:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2678 on theBenchmark for (2678ds/1368Mi) % 282.26/40.21 % (3360424)Instruction limit reached! % 282.26/40.21 % (3360424)------------------------------ % 282.26/40.21 % (3360424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.26/40.21 % (3360424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.26/40.21 % (3360424)CaDiCaL version: 2.1.3 % 282.26/40.21 % (3360424)Termination reason: Instruction limit % 282.26/40.21 % (3360424)Termination phase: Saturation % 282.26/40.21 % (3360424)Time elapsed: 0.357 s % 282.26/40.21 % (3360424)Peak memory usage: 17 MB % 282.26/40.21 % (3360424)Instructions burned: 1369 (million) % 282.26/40.21 % (3360426)ott-21_1_sil=16000:si=on:fs=off:random_seed=588335323:i=360:av=off:fsr=off:rtra=on_2674 on theBenchmark for (2674ds/360Mi) % 282.26/40.21 % (3360426)Instruction limit reached! % 282.26/40.21 % (3360426)------------------------------ % 282.26/40.21 % (3360426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.26/40.21 % (3360426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.26/40.21 % (3360426)CaDiCaL version: 2.1.3 % 282.26/40.21 % (3360426)Termination reason: Instruction limit % 282.26/40.21 % (3360426)Termination phase: Saturation % 282.26/40.21 % (3360426)Time elapsed: 0.098 s % 282.26/40.21 % (3360426)Peak memory usage: 13 MB % 282.26/40.21 % (3360426)Instructions burned: 360 (million) % 282.26/40.21 % (3360428)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2291153108:i=954:bd=all:rtra=on_2673 on theBenchmark for (2673ds/954Mi) % 282.26/40.21 % (3360428)Instruction limit reached! % 282.26/40.21 % (3360428)------------------------------ % 282.26/40.21 % (3360428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.26/40.21 % (3360428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.26/40.21 % (3360428)CaDiCaL version: 2.1.3 % 282.26/40.21 % (3360428)Termination reason: Instruction limit % 282.26/40.21 % (3360428)Termination phase: Saturation % 282.26/40.21 % (3360428)Time elapsed: 0.271 s % 282.26/40.21 % (3360428)Peak memory usage: 15 MB % 282.26/40.21 % (3360428)Instructions burned: 955 (million) % 282.26/40.21 % (3360430)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2384039306:fmbsr=1.3:i=1730:ins=25:rtra=on_2670 on theBenchmark for (2670ds/1730Mi) % 282.26/40.21 % Detected minimum model sizes of [4] % 282.26/40.21 % Detected maximum model sizes of [max] % 300.57/42.83 % (3360430)Instruction limit reached! % 300.57/42.83 % (3360430)------------------------------ % 300.57/42.83 % (3360430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.83 % (3360430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.83 % (3360430)CaDiCaL version: 2.1.3 % 300.57/42.83 % (3360430)Termination reason: Instruction limit % 300.57/42.83 % (3360430)Termination phase: Finite model building constraint generation % 300.57/42.83 % (3360430)Time elapsed: 0.446 s % 300.57/42.83 % (3360430)Peak memory usage: 187 MB % 300.57/42.83 % (3360430)Instructions burned: 1733 (million) % 300.57/42.83 % (3360432)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=458751876:i=2358:rtra=on_2665 on theBenchmark for (2665ds/2358Mi) % 300.57/42.83 % TRYING [5] % 300.57/42.83 % (3360432)Instruction limit reached! % 300.57/42.83 % (3360432)------------------------------ % 300.57/42.83 % (3360432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.83 % (3360432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.83 % (3360432)CaDiCaL version: 2.1.3 % 300.57/42.83 % (3360432)Termination reason: Instruction limit % 300.57/42.83 % (3360432)Termination phase: Saturation % 300.57/42.83 % (3360432)Time elapsed: 0.676 s % 300.57/42.83 % (3360432)Peak memory usage: 19 MB % 300.57/42.83 % (3360432)Instructions burned: 2358 (million) % 300.57/42.83 % (3360434)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1306757482:i=1778:ins=1:rtra=on_2658 on theBenchmark for (2658ds/1778Mi) % 300.57/42.83 % (3360434)Cannot represent all propositional literals internally % 300.57/42.83 % (3360434)Refutation not found, incomplete strategy % 300.57/42.83 % (3360434)------------------------------ % 300.57/42.83 % (3360434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.83 % (3360434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.83 % (3360434)CaDiCaL version: 2.1.3 % 300.57/42.83 % (3360434)Termination reason: Refutation not found, incomplete strategy % 300.57/42.83 % (3360434)Time elapsed: 0.035 s % 300.57/42.83 % (3360434)Peak memory usage: 12 MB % 300.57/42.83 % (3360434)Instructions burned: 126 (million) % 300.57/42.83 % (3360434)------------------------------ % 300.57/42.83 % (3360434)------------------------------ % 300.57/42.83 % (3360436)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=1447040176:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2658 on theBenchmark for (2658ds/1384Mi) % 300.57/42.83 % (3360436)Instruction limit reached! % 300.57/42.83 % (3360436)------------------------------ % 300.57/42.83 % (3360436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.83 % (3360436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.83 % (3360436)CaDiCaL version: 2.1.3 % 300.57/42.83 % (3360436)Termination reason: Instruction limit % 300.57/42.83 % (3360436)Termination phase: Saturation % 300.57/42.83 % (3360436)Time elapsed: 0.478 s % 300.57/42.83 % (3360436)Peak memory usage: 29 MB % 300.57/42.83 % (3360436)Instructions burned: 1386 (million) % 300.57/42.83 % (3360438)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2792586140:i=1758:kws=inv_precedence:fsr=off:rtra=on_2653 on theBenchmark for (2653ds/1758Mi) % 300.57/42.83 % (3360438)Instruction limit reached! % 300.57/42.83 % (3360438)------------------------------ % 300.57/42.83 % (3360438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.83 % (3360438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.83 % (3360438)CaDiCaL version: 2.1.3 % 300.57/42.83 % (3360438)Termination reason: Instruction limit % 300.57/42.83 % (3360438)Termination phase: Saturation % 300.57/42.83 % (3360438)Time elapsed: 0.491 s % 300.57/42.83 % (3360438)Peak memory usage: 19 MB % 300.57/42.83 % (3360438)Instructions burned: 1761 (million) % 300.57/42.83 % (3360440)fmb+10_1_sil=64000:si=on:random_seed=3282523456:i=44122:nm=2:rtra=on:gsp=on_2648 on theBenchmark for (2648ds/44122Mi) % 300.57/42.83 % Detected minimum model sizes of [4] % 300.57/42.83 % Detected maximum model sizes of [max] % 300.57/42.83 % TRYING [4] % 300.57/42.83 % (3360389)Instruction limit reached! % 300.57/42.83 % (3360389)------------------------------ % 300.57/42.83 % (3360389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.57/42.83 % (3360389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.57/42.83 % (3360389)CaDiCaL version: 2.1.3 % 300.57/42.83 % (3360 % 300.57/42.83 Terminated % 300.57/42.83 % Vampire exiting %------------------------------------------------------------------------------