%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV684-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n007.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:14 PM UTC 2026 % Result : Timeout 296.43s 42.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV684-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.18 % Computer : n007.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 12:12:10 UTC 2026 % 0.09/0.18 % CPUTime : % 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 Running first-order model finding % 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.29/1.71 % (2350978)Will run a generic schedule for satisfiability detection. % 9.29/1.71 % (2350988)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3946118075:i=131_2999 on theBenchmark for (2999ds/131Mi) % 9.29/1.71 % (2350984)% WARNING: option uhcvi not known. % 9.29/1.71 % (2350984)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=813207256:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 9.29/1.71 % (2350983)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2312371483_2999 on theBenchmark for (2999ds/0Mi) % 9.29/1.71 % (2350985)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=367740405:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 9.29/1.71 % (2350986)dis+10_1_sil=32000:sp=arity:random_seed=3145852382:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 9.29/1.71 % (2350987)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=45977816:i=116_2999 on theBenchmark for (2999ds/116Mi) % 9.29/1.71 % (2350989)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2330758029:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 9.29/1.71 % (2350988)Instruction limit reached! % 9.29/1.71 % (2350988)------------------------------ % 9.29/1.71 % (2350988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.29/1.71 % (2350988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.29/1.71 % (2350988)CaDiCaL version: 2.1.3 % 9.29/1.71 % (2350988)Termination reason: Instruction limit % 9.29/1.71 % (2350988)Termination phase: Saturation % 9.29/1.71 % (2350988)Time elapsed: 0.044 s % 9.29/1.71 % (2350988)Peak memory usage: 13 MB % 9.29/1.71 % (2350988)Instructions burned: 133 (million) % 9.29/1.71 % (2350997)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3469562841:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 9.29/1.71 % (2350986)Instruction limit reached! % 9.29/1.71 % (2350986)------------------------------ % 9.29/1.71 % (2350986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.29/1.71 % (2350986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.29/1.71 % (2350986)CaDiCaL version: 2.1.3 % 9.29/1.71 % (2350986)Termination reason: Instruction limit % 9.29/1.71 % (2350986)Termination phase: Saturation % 9.29/1.71 % (2350986)Time elapsed: 0.067 s % 9.29/1.71 % (2350986)Peak memory usage: 12 MB % 9.29/1.71 % (2350986)Instructions burned: 104 (million) % 9.29/1.71 % (2350987)Instruction limit reached! % 9.29/1.71 % (2350987)------------------------------ % 9.29/1.71 % (2350987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.29/1.71 % (2350987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.29/1.71 % (2350987)CaDiCaL version: 2.1.3 % 9.29/1.71 % (2350987)Termination reason: Instruction limit % 9.29/1.71 % (2350987)Termination phase: Saturation % 9.29/1.71 % (2350987)Time elapsed: 0.070 s % 9.29/1.71 % (2350987)Peak memory usage: 13 MB % 9.29/1.71 % (2350987)Instructions burned: 117 (million) % 9.29/1.71 % (2350999)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1543858963:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 9.29/1.71 % (2351000)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=3606939390:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 9.29/1.71 % (2350989)Instruction limit reached! % 9.29/1.71 % (2350989)------------------------------ % 9.29/1.71 % (2350989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.29/1.71 % (2350989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.29/1.71 % (2350989)CaDiCaL version: 2.1.3 % 9.29/1.71 % (2350989)Termination reason: Instruction limit % 9.29/1.71 % (2350989)Termination phase: Saturation % 9.29/1.71 % (2350989)Time elapsed: 0.099 s % 9.29/1.71 % (2350989)Peak memory usage: 13 MB % 9.29/1.71 % (2350989)Instructions burned: 159 (million) % 9.29/1.71 % (2351003)ott-21_1_sil=16000:fs=off:random_seed=2980200734:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 9.29/1.71 % TRYING [1] % 9.29/1.71 % TRYING [2] % 9.29/1.71 % (2350999)Instruction limit reached! % 9.29/1.71 % (2350999)------------------------------ % 9.29/1.71 % (2350999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.29/1.71 % (2350999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.85/4.12 % (2350999)CaDiCaL version: 2.1.3 % 26.85/4.12 % (2350999)Termination reason: Instruction limit % 26.85/4.12 % (2350999)Termination phase: Saturation % 26.85/4.12 % (2350999)Time elapsed: 0.080 s % 26.85/4.12 % (2350999)Peak memory usage: 14 MB % 26.85/4.12 % (2350999)Instructions burned: 131 (million) % 26.85/4.12 % (2351005)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4235070919:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 26.85/4.12 % (2351003)Instruction limit reached! % 26.85/4.12 % (2351003)------------------------------ % 26.85/4.12 % (2351003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.85/4.12 % (2351003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.85/4.12 % (2351003)CaDiCaL version: 2.1.3 % 26.85/4.12 % (2351003)Termination reason: Instruction limit % 26.85/4.12 % (2351003)Termination phase: Saturation % 26.85/4.12 % (2351003)Time elapsed: 0.091 s % 26.85/4.12 % (2351003)Peak memory usage: 12 MB % 26.85/4.12 % (2351003)Instructions burned: 181 (million) % 26.85/4.12 % TRYING [1] % 26.85/4.12 % TRYING [2] % 26.85/4.12 % (2351007)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1917941873:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 26.85/4.12 % (2350997)Instruction limit reached! % 26.85/4.12 % (2350997)------------------------------ % 26.85/4.12 % (2350997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.85/4.12 % (2350997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.85/4.12 % (2350997)CaDiCaL version: 2.1.3 % 26.85/4.12 % (2350997)Termination reason: Instruction limit % 26.85/4.12 % (2350997)Termination phase: Finite model building constraint generation % 26.85/4.12 % (2350997)Time elapsed: 0.182 s % 26.85/4.12 % (2350997)Peak memory usage: 36 MB % 26.85/4.12 % (2350997)Instructions burned: 715 (million) % 26.85/4.12 % (2351009)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2598054158:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 26.85/4.12 % TRYING [3] % 26.85/4.12 % (2351000)Instruction limit reached! % 26.85/4.12 % (2351000)------------------------------ % 26.85/4.12 % (2351000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.85/4.12 % (2351000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.85/4.12 % (2351000)CaDiCaL version: 2.1.3 % 26.85/4.12 % (2351000)Termination reason: Instruction limit % 26.85/4.12 % (2351000)Termination phase: Saturation % 26.85/4.12 % (2351000)Time elapsed: 0.339 s % 26.85/4.12 % (2351000)Peak memory usage: 17 MB % 26.85/4.12 % (2351000)Instructions burned: 684 (million) % 26.85/4.12 % (2351011)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=251940431:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 26.85/4.12 % TRYING [1] % 26.85/4.12 % (2351005)Instruction limit reached! % 26.85/4.12 % (2351005)------------------------------ % 26.85/4.12 % (2351005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.85/4.12 % (2351005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.85/4.12 % (2351005)CaDiCaL version: 2.1.3 % 26.85/4.12 % (2351005)Termination reason: Instruction limit % 26.85/4.12 % (2351005)Termination phase: Saturation % 26.85/4.12 % (2351005)Time elapsed: 0.301 s % 26.85/4.12 % (2351005)Peak memory usage: 13 MB % 26.85/4.12 % (2351005)Instructions burned: 478 (million) % 26.85/4.12 % TRYING [2] % 26.85/4.12 % (2351013)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=3721363872:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 26.85/4.12 % (2351009)Instruction limit reached! % 26.85/4.12 % (2351009)------------------------------ % 26.85/4.12 % (2351009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.85/4.12 % (2351009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.85/4.12 % (2351009)CaDiCaL version: 2.1.3 % 26.85/4.12 % (2351009)Termination reason: Instruction limit % 26.85/4.12 % (2351009)Termination phase: Saturation % 26.85/4.12 % (2351009)Time elapsed: 0.370 s % 26.85/4.12 % (2351009)Peak memory usage: 19 MB % 26.85/4.12 % (2351009)Instructions burned: 1182 (million) % 26.85/4.12 % (2351015)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=778954540:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 26.85/4.12 % (2351007)Instruction limit reached! % 26.85/4.12 % (2351007)------------------------------ % 26.85/4.12 % (2351007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.85/4.12 % (2351007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.70/13.12 % (2351007)CaDiCaL version: 2.1.3 % 90.70/13.12 % (2351007)Termination reason: Instruction limit % 90.70/13.12 % (2351007)Termination phase: Finite model building SAT solving % 90.70/13.12 % (2351007)Time elapsed: 0.400 s % 90.70/13.12 % (2351007)Peak memory usage: 35 MB % 90.70/13.12 % (2351007)Instructions burned: 865 (million) % 90.70/13.12 % (2351017)fmb+10_1_sil=64000:random_seed=1199127824:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 90.70/13.12 % TRYING [1] % 90.70/13.12 % (2351011)Instruction limit reached! % 90.70/13.12 % (2351011)------------------------------ % 90.70/13.12 % (2351011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.70/13.12 % (2351011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.70/13.12 % (2351011)CaDiCaL version: 2.1.3 % 90.70/13.12 % (2351011)Termination reason: Instruction limit % 90.70/13.12 % (2351011)Termination phase: Finite model building constraint generation % 90.70/13.12 % (2351011)Time elapsed: 0.437 s % 90.70/13.12 % (2351011)Peak memory usage: 77 MB % 90.70/13.12 % (2351011)Instructions burned: 889 (million) % 90.70/13.12 % (2351015)Instruction limit reached! % 90.70/13.12 % (2351015)------------------------------ % 90.70/13.12 % (2351015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.70/13.12 % (2351015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.70/13.12 % (2351015)CaDiCaL version: 2.1.3 % 90.70/13.12 % (2351015)Termination reason: Instruction limit % 90.70/13.12 % (2351015)Termination phase: Saturation % 90.70/13.12 % (2351015)Time elapsed: 0.264 s % 90.70/13.12 % (2351015)Peak memory usage: 19 MB % 90.70/13.12 % (2351015)Instructions burned: 882 (million) % 90.70/13.12 % (2351019)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4069227669:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 90.70/13.12 % TRYING [2] % 90.70/13.12 % (2351020)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3292943021:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 90.70/13.12 % (2351013)Instruction limit reached! % 90.70/13.12 % (2351013)------------------------------ % 90.70/13.12 % (2351013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.70/13.12 % (2351013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.70/13.12 % (2351013)CaDiCaL version: 2.1.3 % 90.70/13.12 % (2351013)Termination reason: Instruction limit % 90.70/13.12 % (2351013)Termination phase: Saturation % 90.70/13.12 % (2351013)Time elapsed: 0.422 s % 90.70/13.12 % (2351013)Peak memory usage: 16 MB % 90.70/13.12 % (2351013)Instructions burned: 692 (million) % 90.70/13.12 % (2351023)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1081476566:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 90.70/13.12 % (2351019)Cannot represent all propositional literals internally % 90.70/13.12 % (2351019)Refutation not found, incomplete strategy % 90.70/13.12 % (2351019)------------------------------ % 90.70/13.12 % (2351019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.70/13.12 % (2351019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.70/13.12 % (2351019)CaDiCaL version: 2.1.3 % 90.70/13.12 % (2351019)Termination reason: Refutation not found, incomplete strategy % 90.70/13.12 % (2351019)Time elapsed: 0.109 s % 90.70/13.12 % (2351019)Peak memory usage: 17 MB % 90.70/13.12 % (2351019)Instructions burned: 417 (million) % 90.70/13.12 % (2351019)------------------------------ % 90.70/13.12 % (2351019)------------------------------ % 90.70/13.12 % (2351025)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2765179927:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi) % 90.70/13.12 % TRYING [8] % 90.70/13.12 % (2351020)Instruction limit reached! % 90.70/13.12 % (2351020)------------------------------ % 90.70/13.12 % (2351020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.70/13.12 % (2351020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.70/13.12 % (2351020)CaDiCaL version: 2.1.3 % 90.70/13.12 % (2351020)Termination reason: Instruction limit % 90.70/13.12 % (2351020)Termination phase: Finite model building constraint generation % 90.70/13.12 % (2351020)Time elapsed: 0.376 s % 90.70/13.12 % (2351020)Peak memory usage: 51 MB % 90.70/13.12 % (2351020)Instructions burned: 922 (million) % 90.70/13.12 % TRYING [4] % 90.70/13.12 % (2351027)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1589403294:i=6324_2986 on theBenchmark for (2986ds/6324Mi) % 90.70/13.12 % (2351025)Instruction limit reached! % 90.70/13.12 % (2351025)------------------------------ % 159.25/22.77 % (2351025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.25/22.77 % (2351025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.25/22.77 % (2351025)CaDiCaL version: 2.1.3 % 159.25/22.77 % (2351025)Termination reason: Instruction limit % 159.25/22.77 % (2351025)Termination phase: Saturation % 159.25/22.77 % (2351025)Time elapsed: 0.398 s % 159.25/22.77 % (2351025)Peak memory usage: 26 MB % 159.25/22.77 % (2351025)Instructions burned: 1474 (million) % 159.25/22.77 % (2351029)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1300205538:fmbsr=2.30978:i=2174_2985 on theBenchmark for (2985ds/2174Mi) % 159.25/22.77 % (2351027)Cannot represent all propositional literals internally % 159.25/22.77 % (2351027)Refutation not found, incomplete strategy % 159.25/22.77 % (2351027)------------------------------ % 159.25/22.77 % (2351027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.25/22.77 % (2351027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.25/22.77 % (2351027)CaDiCaL version: 2.1.3 % 159.25/22.77 % (2351027)Termination reason: Refutation not found, incomplete strategy % 159.25/22.77 % (2351027)Time elapsed: 0.213 s % 159.25/22.77 % (2351027)Peak memory usage: 17 MB % 159.25/22.77 % (2351027)Instructions burned: 432 (million) % 159.25/22.77 % (2351027)------------------------------ % 159.25/22.77 % (2351027)------------------------------ % 159.25/22.77 % (2351031)ott-2_1_sil=16000:newcnf=on:random_seed=2879418355:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2984 on theBenchmark for (2984ds/869Mi) % 159.25/22.77 % TRYING [3] % 159.25/22.77 % (2351029)Cannot represent all propositional literals internally % 159.25/22.77 % (2351029)Refutation not found, incomplete strategy % 159.25/22.77 % (2351029)------------------------------ % 159.25/22.77 % (2351029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.25/22.77 % (2351029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.25/22.77 % (2351029)CaDiCaL version: 2.1.3 % 159.25/22.77 % (2351029)Termination reason: Refutation not found, incomplete strategy % 159.25/22.77 % (2351029)Time elapsed: 0.486 s % 159.25/22.77 % (2351029)Peak memory usage: 27 MB % 159.25/22.77 % (2351029)Instructions burned: 1869 (million) % 159.25/22.77 % (2351029)------------------------------ % 159.25/22.77 % (2351029)------------------------------ % 159.25/22.77 % (2351033)ott+10_1_sil=32000:tgt=ground:random_seed=2096938966:i=5114:av=off_2980 on theBenchmark for (2980ds/5114Mi) % 159.25/22.77 % (2351031)Instruction limit reached! % 159.25/22.77 % (2351031)------------------------------ % 159.25/22.77 % (2351031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.25/22.77 % (2351031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.25/22.77 % (2351031)CaDiCaL version: 2.1.3 % 159.25/22.77 % (2351031)Termination reason: Instruction limit % 159.25/22.77 % (2351031)Termination phase: Saturation % 159.25/22.77 % (2351031)Time elapsed: 0.497 s % 159.25/22.77 % (2351031)Peak memory usage: 14 MB % 159.25/22.77 % (2351031)Instructions burned: 870 (million) % 159.25/22.77 % (2351035)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3576839978:i=54282_2978 on theBenchmark for (2978ds/54282Mi) % 159.25/22.77 % TRYING [1] % 159.25/22.77 % TRYING [2] % 159.25/22.77 % TRYING [3] % 159.25/22.77 % TRYING [4] % 159.25/22.77 % (2351033)Instruction limit reached! % 159.25/22.77 % (2351033)------------------------------ % 159.25/22.77 % (2351033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.25/22.77 % (2351033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.25/22.77 % (2351033)CaDiCaL version: 2.1.3 % 159.25/22.77 % (2351033)Termination reason: Instruction limit % 159.25/22.77 % (2351033)Termination phase: Saturation % 159.25/22.77 % (2351033)Time elapsed: 1.775 s % 159.25/22.77 % (2351033)Peak memory usage: 38 MB % 159.25/22.77 % (2351033)Instructions burned: 5115 (million) % 159.25/22.77 % (2351039)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3674679629:i=3512:aac=none_2962 on theBenchmark for (2962ds/3512Mi) % 159.25/22.77 % (2351023)Instruction limit reached! % 159.25/22.77 % (2351023)------------------------------ % 159.25/22.77 % (2351023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 159.25/22.77 % (2351023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.25/22.77 % (2351023)CaDiCaL version: 2.1.3 % 159.25/22.77 % (2351023)Termination reason: Instruction limit % 159.25/22.77 % (2351023)Termination phase: Saturation % 159.25/22.77 % (2351023)Time elapsed: 2.877 s % 159.25/22.77 % (2351023)Peak memory usage: 34 MB % 159.25/22.77 % (2351023)Instructions burned: 5131 (million) % 243.69/34.61 % (2351041)dis+21_1_sil=32000:sas=cadical:random_seed=3213136378:i=3773:amm=off_2960 on theBenchmark for (2960ds/3773Mi) % 243.69/34.61 % TRYING [4] % 243.69/34.61 % (2351039)Instruction limit reached! % 243.69/34.61 % (2351039)------------------------------ % 243.69/34.61 % (2351039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.69/34.61 % (2351039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.69/34.61 % (2351039)CaDiCaL version: 2.1.3 % 243.69/34.61 % (2351039)Termination reason: Instruction limit % 243.69/34.61 % (2351039)Termination phase: Saturation % 243.69/34.61 % (2351039)Time elapsed: 1.075 s % 243.69/34.61 % (2351039)Peak memory usage: 26 MB % 243.69/34.61 % (2351039)Instructions burned: 3513 (million) % 243.69/34.61 % (2351043)ott+11_1_sil=16000:gs=on:random_seed=818368654:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2951 on theBenchmark for (2951ds/2251Mi) % 243.69/34.61 % (2351043)Instruction limit reached! % 243.69/34.61 % (2351043)------------------------------ % 243.69/34.61 % (2351043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.69/34.61 % (2351043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.69/34.61 % (2351043)CaDiCaL version: 2.1.3 % 243.69/34.61 % (2351043)Termination reason: Instruction limit % 243.69/34.61 % (2351043)Termination phase: Saturation % 243.69/34.61 % (2351043)Time elapsed: 0.668 s % 243.69/34.61 % (2351043)Peak memory usage: 22 MB % 243.69/34.61 % (2351043)Instructions burned: 2255 (million) % 243.69/34.61 % (2351045)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2333291557:fmbsr=1.6:i=67534_2944 on theBenchmark for (2944ds/67534Mi) % 243.69/34.61 % (2351041)Instruction limit reached! % 243.69/34.61 % (2351041)------------------------------ % 243.69/34.61 % (2351041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.69/34.61 % (2351041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.69/34.61 % (2351041)CaDiCaL version: 2.1.3 % 243.69/34.61 % (2351041)Termination reason: Instruction limit % 243.69/34.61 % (2351041)Termination phase: Saturation % 243.69/34.61 % (2351041)Time elapsed: 2.225 s % 243.69/34.61 % (2351041)Peak memory usage: 33 MB % 243.69/34.61 % (2351041)Instructions burned: 3774 (million) % 243.69/34.61 % (2351047)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2575225897:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2938 on theBenchmark for (2938ds/4591Mi) % 243.69/34.61 % TRYING [5] % 243.69/34.61 % (2351047)Instruction limit reached! % 243.69/34.61 % (2351047)------------------------------ % 243.69/34.61 % (2351047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.69/34.61 % (2351047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.69/34.61 % (2351047)CaDiCaL version: 2.1.3 % 243.69/34.61 % (2351047)Termination reason: Instruction limit % 243.69/34.61 % (2351047)Termination phase: Saturation % 243.69/34.61 % (2351047)Time elapsed: 1.842 s % 243.69/34.61 % (2351047)Peak memory usage: 38 MB % 243.69/34.61 % (2351047)Instructions burned: 4592 (million) % 243.69/34.61 % (2351049)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2531528372:i=29340_2919 on theBenchmark for (2919ds/29340Mi) % 243.69/34.61 % TRYING [7] % 243.69/34.61 % TRYING [5] % 243.69/34.61 % (2351017)Instruction limit reached! % 243.69/34.61 % (2351017)------------------------------ % 243.69/34.61 % (2351017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.69/34.61 % (2351017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.69/34.61 % (2351017)CaDiCaL version: 2.1.3 % 243.69/34.61 % (2351017)Termination reason: Instruction limit % 243.69/34.61 % (2351017)Termination phase: Finite model building SAT solving % 243.69/34.61 % (2351017)Time elapsed: 9.362 s % 243.69/34.61 % (2351017)Peak memory usage: 627 MB % 243.69/34.61 % (2351017)Instructions burned: 22062 (million) % 243.69/34.61 % (2351051)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2828425560:i=5211_2898 on theBenchmark for (2898ds/5211Mi) % 243.69/34.61 % (2351051)Instruction limit reached! % 243.69/34.61 % (2351051)------------------------------ % 243.69/34.61 % (2351051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 243.69/34.61 % (2351051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.69/34.61 % (2351051)CaDiCaL version: 2.1.3 % 243.69/34.61 % (2351051)Termination reason: Instruction limit % 243.69/34.61 % (2351051)Termination phase: Saturation % 243.69/34.61 % (2351051)Time elapsed: 2.708 s % 243.69/34.61 % (2351051)Peak memory usage: 48 MB % 243.69/34.61 % (2351051)Instructions burned: 5212 (million) % 296.43/42.08 % (2351053)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3173792578:i=5497:nm=2_2870 on theBenchmark for (2870ds/5497Mi) % 296.43/42.08 % (2351053)Cannot represent all propositional literals internally % 296.43/42.08 % (2351053)Refutation not found, incomplete strategy % 296.43/42.08 % (2351053)------------------------------ % 296.43/42.08 % (2351053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.43/42.08 % (2351053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.43/42.08 % (2351053)CaDiCaL version: 2.1.3 % 296.43/42.08 % (2351053)Termination reason: Refutation not found, incomplete strategy % 296.43/42.08 % (2351053)Time elapsed: 0.214 s % 296.43/42.08 % (2351053)Peak memory usage: 17 MB % 296.43/42.08 % (2351053)Instructions burned: 432 (million) % 296.43/42.08 % (2351053)------------------------------ % 296.43/42.08 % (2351053)------------------------------ % 296.43/42.08 % (2351055)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1806844992:fmbsr=2:i=46332_2868 on theBenchmark for (2868ds/46332Mi) % 296.43/42.08 % (2351055)Cannot represent all propositional literals internally % 296.43/42.08 % (2351055)Refutation not found, incomplete strategy % 296.43/42.08 % (2351055)------------------------------ % 296.43/42.08 % (2351055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.43/42.08 % (2351055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.43/42.08 % (2351055)CaDiCaL version: 2.1.3 % 296.43/42.08 % (2351055)Termination reason: Refutation not found, incomplete strategy % 296.43/42.08 % (2351055)Time elapsed: 0.212 s % 296.43/42.08 % (2351055)Peak memory usage: 16 MB % 296.43/42.08 % (2351055)Instructions burned: 438 (million) % 296.43/42.08 % (2351055)------------------------------ % 296.43/42.08 % (2351055)------------------------------ % 296.43/42.08 % (2351057)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=295277447:i=14071_2866 on theBenchmark for (2866ds/14071Mi) % 296.43/42.08 % TRYING [12] % 296.43/42.08 % (2351057)Instruction limit reached! % 296.43/42.08 % (2351057)------------------------------ % 296.43/42.08 % (2351057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.43/42.08 % (2351057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.43/42.08 % (2351057)CaDiCaL version: 2.1.3 % 296.43/42.08 % (2351057)Termination reason: Instruction limit % 296.43/42.08 % (2351057)Termination phase: Finite model building constraint generation % 296.43/42.08 % (2351057)Time elapsed: 4.809 s % 296.43/42.08 % (2351057)Peak memory usage: 843 MB % 296.43/42.08 % (2351057)Instructions burned: 14074 (million) % 296.43/42.08 % (2351045)Instruction limit reached! % 296.43/42.08 % (2351045)------------------------------ % 296.43/42.08 % (2351045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.43/42.08 % (2351045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.43/42.08 % (2351045)CaDiCaL version: 2.1.3 % 296.43/42.08 % (2351045)Termination reason: Instruction limit % 296.43/42.08 % (2351045)Termination phase: Finite model building constraint generation % 296.43/42.08 % (2351045)Time elapsed: 12.689 s % 296.43/42.08 % (2351045)Peak memory usage: 3834 MB % 296.43/42.08 % (2351045)Instructions burned: 67536 (million) % 296.43/42.08 % (2351059)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2298152390:i=22565:add=on:rawr=on_2816 on theBenchmark for (2816ds/22565Mi) % 296.43/42.08 % (2351061)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3408745039:i=8173:av=off_2814 on theBenchmark for (2814ds/8173Mi) % 296.43/42.08 % (2351061)Instruction limit reached! % 296.43/42.08 % (2351061)------------------------------ % 296.43/42.08 % (2351061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.43/42.08 % (2351061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.43/42.08 % (2351061)CaDiCaL version: 2.1.3 % 296.43/42.08 % (2351061)Termination reason: Instruction limit % 296.43/42.08 % (2351061)Termination phase: Saturation % 296.43/42.08 % (2351061)Time elapsed: 2.827 s % 296.43/42.08 % (2351061)Peak memory usage: 68 MB % 296.43/42.08 % (2351061)Instructions burned: 8173 (million) % 296.43/42.08 % (2351063)dis+10_16:1_sil=16000:random_seed=1495413640:i=9155:fsr=off_2785 on theBenchmark for (2785ds/9155Mi) % 296.43/42.08 % (2351049)Instruction limit reached! % 296.43/42.08 % (2351049)------------------------------ % 296.43/42.08 % (2351049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.43/42.08 % (2351049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.73 % (2351049)CaDiCaL version: 2.1.3 % 300.55/42.73 % (2351049)Termination reason: Instruction limit % 300.55/42.73 % (2351049)Termination phase: Saturation % 300.55/42.73 % (2351049)Time elapsed: 14.510 s % 300.55/42.73 % (2351049)Peak memory usage: 103 MB % 300.55/42.73 % (2351049)Instructions burned: 29342 (million) % 300.55/42.73 % (2351035)Instruction limit reached! % 300.55/42.73 % (2351035)------------------------------ % 300.55/42.73 % (2351035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.55/42.73 % (2351035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.73 % (2351035)CaDiCaL version: 2.1.3 % 300.55/42.73 % (2351035)Termination reason: Instruction limit % 300.55/42.73 % (2351035)Termination phase: Finite model building constraint generation % 300.55/42.73 % (2351035)Time elapsed: 20.429 s % 300.55/42.73 % (2351035)Peak memory usage: 2325 MB % 300.55/42.73 % (2351035)Instructions burned: 54283 (million) % 300.55/42.73 % (2351065)ott-3_8_sil=64000:random_seed=94872740:i=20139:bs=on_2774 on theBenchmark for (2774ds/20139Mi) % 300.55/42.73 % (2351067)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2319460358:fmbsr=2:i=32576_2771 on theBenchmark for (2771ds/32576Mi) % 300.55/42.73 % TRYING [9] % 300.55/42.73 % (2351063)Instruction limit reached! % 300.55/42.73 % (2351063)------------------------------ % 300.55/42.73 % (2351063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.55/42.73 % (2351063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.73 % (2351063)CaDiCaL version: 2.1.3 % 300.55/42.73 % (2351063)Termination reason: Instruction limit % 300.55/42.73 % (2351063)Termination phase: Saturation % 300.55/42.73 % (2351063)Time elapsed: 2.640 s % 300.55/42.73 % (2351063)Peak memory usage: 65 MB % 300.55/42.73 % (2351063)Instructions burned: 9157 (million) % 300.55/42.73 % (2351069)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1060107328:i=11404_2759 on theBenchmark for (2759ds/11404Mi) % 300.55/42.73 % (2351069)Instruction limit reached! % 300.55/42.73 % (2351069)------------------------------ % 300.55/42.73 % (2351069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.55/42.73 % (2351069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.73 % (2351069)CaDiCaL version: 2.1.3 % 300.55/42.73 % (2351069)Termination reason: Instruction limit % 300.55/42.73 % (2351069)Termination phase: Saturation % 300.55/42.73 % (2351069)Time elapsed: 4.108 s % 300.55/42.73 % (2351069)Peak memory usage: 87 MB % 300.55/42.73 % (2351069)Instructions burned: 11405 (million) % 300.55/42.73 % (2351071)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=465170272:i=14134_2717 on theBenchmark for (2717ds/14134Mi) % 300.55/42.73 % TRYING [6] % 300.55/42.73 % (2351059)Instruction limit reached! % 300.55/42.73 % (2351059)------------------------------ % 300.55/42.73 % (2351059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.55/42.73 % (2351059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.73 % (2351059)CaDiCaL version: 2.1.3 % 300.55/42.73 % (2351059)Termination reason: Instruction limit % 300.55/42.73 % (2351059)Termination phase: Saturation % 300.55/42.73 % (2351059)Time elapsed: 13.216 s % 300.55/42.73 % (2351059)Peak memory usage: 252 MB % 300.55/42.73 % (2351059)Instructions burned: 22565 (million) % 300.55/42.73 % (2351073)dis+33_16_sil=32000:sac=on:random_seed=2917877060:i=15851:nm=0_2684 on theBenchmark for (2684ds/15851Mi) % 300.55/42.73 % (2351071)Instruction limit reached! % 300.55/42.73 % (2351071)------------------------------ % 300.55/42.73 % (2351071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.55/42.73 % (2351071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.73 % (2351071)CaDiCaL version: 2.1.3 % 300.55/42.73 % (2351071)Termination reason: Instruction limit % 300.55/42.73 % (2351071)Termination phase: Saturation % 300.55/42.73 % (2351071)Time elapsed: 4.859 s % 300.55/42.73 % (2351071)Peak memory usage: 86 MB % 300.55/42.73 % (2351071)Instructions burned: 14138 (million) % 300.55/42.73 % (2351075)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1138003812:avsq=on:i=17627:add=on:amm=off_2669 on theBenchmark for (2669ds/17627Mi) % 300.55/42.73 % (2351067)Instruction limit reached! % 300.55/42.73 % (2351067)------------------------------ % 300.55/42.73 % (2351067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.55/42.73 % (2351067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.73 % (2351067)CaDiCaL version: 2.1.3 % 300.55/42.73 % (2351067)Termination reason: Instruction limit % 300.55/42.73 % (2351067)Termination phase: Fini % 300.55/42.73 Terminated % 300.55/42.73 % Vampire exiting % 300.55/42.74 Terminated %------------------------------------------------------------------------------