%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV624-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:09 PM UTC 2026 % Result : Timeout 300.46s 42.93s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWV624-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.10 % Computer : n012.cluster.edu % 0.00/0.10 % Model : x86_64 x86_64 % 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.10 % Memory : 8046.5625MB % 0.00/0.10 % OS : Linux 6.8.0-71-generic % 0.00/0.10 % CPULimit : 300 % 0.00/0.10 % WCLimit : 300 % 0.00/0.10 % DateTime : Mon Sep 28 12:04:11 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.12 Running first-order model finding % 0.09/0.12 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 % 6.66/1.12 % (3337815)Will run a generic schedule for satisfiability detection. % 6.66/1.12 % (3337821)% WARNING: option uhcvi not known. % 6.66/1.12 % (3337823)dis+10_1_sil=32000:sp=arity:random_seed=3140949940:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.66/1.12 % (3337820)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2792189526_2999 on theBenchmark for (2999ds/0Mi) % 6.66/1.12 % (3337821)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1064824621:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.66/1.12 % (3337822)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=976846511:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.66/1.12 % (3337824)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1427307485:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.66/1.12 % (3337825)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=651337309:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.66/1.12 % (3337826)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2733581154:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.66/1.12 % (3337823)Instruction limit reached! % 6.66/1.12 % (3337823)------------------------------ % 6.66/1.12 % (3337823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.66/1.12 % (3337823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.66/1.12 % (3337823)CaDiCaL version: 2.1.3 % 6.66/1.12 % (3337823)Termination reason: Instruction limit % 6.66/1.12 % (3337823)Termination phase: Saturation % 6.66/1.12 % (3337823)Time elapsed: 0.034 s % 6.66/1.12 % (3337823)Peak memory usage: 13 MB % 6.66/1.12 % (3337823)Instructions burned: 106 (million) % 6.66/1.12 % (3337824)Instruction limit reached! % 6.66/1.12 % (3337824)------------------------------ % 6.66/1.12 % (3337824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.66/1.12 % (3337824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.66/1.12 % (3337824)CaDiCaL version: 2.1.3 % 6.66/1.12 % (3337824)Termination reason: Instruction limit % 6.66/1.12 % (3337824)Termination phase: Saturation % 6.66/1.12 % (3337824)Time elapsed: 0.036 s % 6.66/1.12 % (3337824)Peak memory usage: 14 MB % 6.66/1.12 % (3337824)Instructions burned: 118 (million) % 6.66/1.12 % (3337825)Instruction limit reached! % 6.66/1.12 % (3337825)------------------------------ % 6.66/1.12 % (3337825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.66/1.12 % (3337825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.66/1.12 % (3337825)CaDiCaL version: 2.1.3 % 6.66/1.12 % (3337825)Termination reason: Instruction limit % 6.66/1.12 % (3337825)Termination phase: Saturation % 6.66/1.12 % (3337825)Time elapsed: 0.043 s % 6.66/1.12 % (3337825)Peak memory usage: 14 MB % 6.66/1.12 % (3337825)Instructions burned: 131 (million) % 6.66/1.12 % (3337834)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=156257174:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.66/1.12 % (3337835)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=191722579:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.66/1.12 % (3337836)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=1578855354:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 6.66/1.12 % (3337826)Instruction limit reached! % 6.66/1.12 % (3337826)------------------------------ % 6.66/1.12 % (3337826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.66/1.12 % (3337826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.66/1.12 % (3337826)CaDiCaL version: 2.1.3 % 6.66/1.12 % (3337826)Termination reason: Instruction limit % 6.66/1.12 % (3337826)Termination phase: Saturation % 6.66/1.12 % (3337826)Time elapsed: 0.054 s % 6.66/1.12 % (3337826)Peak memory usage: 14 MB % 6.66/1.12 % (3337826)Instructions burned: 161 (million) % 6.66/1.12 % (3337840)ott-21_1_sil=16000:fs=off:random_seed=2238277645:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 6.66/1.12 % (3337835)Instruction limit reached! % 6.66/1.12 % (3337835)------------------------------ % 6.66/1.12 % (3337835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.66/1.12 % (3337835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.66/1.12 % (3337835)CaDiCaL version: 2.1.3 % 22.14/3.36 % (3337835)Termination reason: Instruction limit % 22.14/3.36 % (3337835)Termination phase: Saturation % 22.14/3.36 % (3337835)Time elapsed: 0.043 s % 22.14/3.36 % (3337835)Peak memory usage: 14 MB % 22.14/3.36 % (3337835)Instructions burned: 133 (million) % 22.14/3.36 % (3337842)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=117155455:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 22.14/3.36 % TRYING [1] % 22.14/3.36 % TRYING [2] % 22.14/3.36 % (3337840)Instruction limit reached! % 22.14/3.36 % (3337840)------------------------------ % 22.14/3.36 % (3337840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.14/3.36 % (3337840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.14/3.36 % (3337840)CaDiCaL version: 2.1.3 % 22.14/3.36 % (3337840)Termination reason: Instruction limit % 22.14/3.36 % (3337840)Termination phase: Saturation % 22.14/3.36 % (3337840)Time elapsed: 0.051 s % 22.14/3.36 % (3337840)Peak memory usage: 14 MB % 22.14/3.36 % (3337840)Instructions burned: 183 (million) % 22.14/3.36 % (3337844)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3249467704:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 22.14/3.36 % TRYING [1] % 22.14/3.36 % TRYING [2] % 22.14/3.36 % TRYING [3] % 22.14/3.36 % TRYING [3] % 22.14/3.36 % (3337834)Instruction limit reached! % 22.14/3.36 % (3337834)------------------------------ % 22.14/3.36 % (3337834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.14/3.36 % (3337834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.14/3.36 % (3337834)CaDiCaL version: 2.1.3 % 22.14/3.36 % (3337834)Termination reason: Instruction limit % 22.14/3.36 % (3337834)Termination phase: Finite model building constraint generation % 22.14/3.36 % (3337834)Time elapsed: 0.171 s % 22.14/3.36 % (3337834)Peak memory usage: 33 MB % 22.14/3.36 % (3337834)Instructions burned: 718 (million) % 22.14/3.36 % TRYING [1] % 22.14/3.36 % (3337846)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1495844089:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 22.14/3.36 % TRYING [2] % 22.14/3.36 % (3337842)Instruction limit reached! % 22.14/3.36 % (3337842)------------------------------ % 22.14/3.36 % (3337842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.14/3.36 % (3337842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.14/3.36 % (3337842)CaDiCaL version: 2.1.3 % 22.14/3.36 % (3337842)Termination reason: Instruction limit % 22.14/3.36 % (3337842)Termination phase: Saturation % 22.14/3.36 % (3337842)Time elapsed: 0.168 s % 22.14/3.36 % (3337842)Peak memory usage: 15 MB % 22.14/3.36 % (3337842)Instructions burned: 478 (million) % 22.14/3.36 % (3337848)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=101166209:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 22.14/3.36 % (3337836)Instruction limit reached! % 22.14/3.36 % (3337836)------------------------------ % 22.14/3.36 % (3337836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.14/3.36 % (3337836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.14/3.36 % (3337836)CaDiCaL version: 2.1.3 % 22.14/3.36 % (3337836)Termination reason: Instruction limit % 22.14/3.36 % (3337836)Termination phase: Saturation % 22.14/3.36 % (3337836)Time elapsed: 0.236 s % 22.14/3.36 % (3337836)Peak memory usage: 18 MB % 22.14/3.36 % (3337836)Instructions burned: 685 (million) % 22.14/3.36 % (3337850)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=3932299909:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 22.14/3.36 % (3337844)Instruction limit reached! % 22.14/3.36 % (3337844)------------------------------ % 22.14/3.36 % (3337844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.14/3.36 % (3337844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.14/3.36 % (3337844)CaDiCaL version: 2.1.3 % 22.14/3.36 % (3337844)Termination reason: Instruction limit % 22.14/3.36 % (3337844)Termination phase: Finite model building SAT solving % 22.14/3.36 % (3337844)Time elapsed: 0.220 s % 22.14/3.36 % (3337844)Peak memory usage: 32 MB % 22.14/3.36 % (3337844)Instructions burned: 874 (million) % 22.14/3.36 % (3337852)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3900440226:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 22.14/3.36 % (3337848)Instruction limit reached! % 22.14/3.36 % (3337848)------------------------------ % 22.14/3.36 % (3337848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.19/7.78 % (3337848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.19/7.78 % (3337848)CaDiCaL version: 2.1.3 % 53.19/7.78 % (3337848)Termination reason: Instruction limit % 53.19/7.78 % (3337848)Termination phase: Finite model building constraint generation % 53.19/7.78 % (3337848)Time elapsed: 0.240 s % 53.19/7.78 % (3337848)Peak memory usage: 80 MB % 53.19/7.78 % (3337848)Instructions burned: 892 (million) % 53.19/7.78 % (3337854)fmb+10_1_sil=64000:random_seed=1703037530:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 53.19/7.78 % TRYING [4] % 53.19/7.78 % (3337850)Instruction limit reached! % 53.19/7.78 % (3337850)------------------------------ % 53.19/7.78 % (3337850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.19/7.78 % (3337850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.19/7.78 % (3337850)CaDiCaL version: 2.1.3 % 53.19/7.78 % (3337850)Termination reason: Instruction limit % 53.19/7.78 % (3337850)Termination phase: Saturation % 53.19/7.78 % (3337850)Time elapsed: 0.247 s % 53.19/7.78 % (3337850)Peak memory usage: 19 MB % 53.19/7.78 % (3337850)Instructions burned: 692 (million) % 53.19/7.78 % (3337856)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2734026346:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 53.19/7.78 % (3337846)Instruction limit reached! % 53.19/7.78 % (3337846)------------------------------ % 53.19/7.78 % (3337846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.19/7.78 % (3337846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.19/7.78 % (3337846)CaDiCaL version: 2.1.3 % 53.19/7.78 % (3337846)Termination reason: Instruction limit % 53.19/7.78 % (3337846)Termination phase: Saturation % 53.19/7.78 % (3337846)Time elapsed: 0.381 s % 53.19/7.78 % (3337846)Peak memory usage: 19 MB % 53.19/7.78 % (3337846)Instructions burned: 1179 (million) % 53.19/7.78 % (3337852)Instruction limit reached! % 53.19/7.78 % (3337852)------------------------------ % 53.19/7.78 % (3337852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.19/7.78 % (3337852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.19/7.78 % (3337852)CaDiCaL version: 2.1.3 % 53.19/7.78 % (3337852)Termination reason: Instruction limit % 53.19/7.78 % (3337852)Termination phase: Saturation % 53.19/7.78 % (3337852)Time elapsed: 0.261 s % 53.19/7.78 % (3337852)Peak memory usage: 20 MB % 53.19/7.78 % (3337852)Instructions burned: 880 (million) % 53.19/7.78 % (3337858)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=9213246:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 53.19/7.78 % (3337859)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1466869975:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 53.19/7.78 % TRYING [1] % 53.19/7.78 % (3337856)Cannot represent all propositional literals internally % 53.19/7.78 % (3337856)Refutation not found, incomplete strategy % 53.19/7.78 % (3337856)------------------------------ % 53.19/7.78 % (3337856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.19/7.78 % (3337856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.19/7.78 % (3337856)CaDiCaL version: 2.1.3 % 53.19/7.78 % (3337856)Termination reason: Refutation not found, incomplete strategy % 53.19/7.78 % (3337856)Time elapsed: 0.100 s % 53.19/7.78 % (3337856)Peak memory usage: 17 MB % 53.19/7.78 % (3337856)Instructions burned: 390 (million) % 53.19/7.78 % TRYING [2] % 53.19/7.78 % (3337856)------------------------------ % 53.19/7.78 % (3337856)------------------------------ % 53.19/7.78 % (3337862)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1157623529:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 53.19/7.78 % TRYING [8] % 53.19/7.78 % (3337858)Instruction limit reached! % 53.19/7.78 % (3337858)------------------------------ % 53.19/7.78 % (3337858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.19/7.78 % (3337858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.19/7.78 % (3337858)CaDiCaL version: 2.1.3 % 53.19/7.78 % (3337858)Termination reason: Instruction limit % 53.19/7.78 % (3337858)Termination phase: Finite model building constraint generation % 53.19/7.78 % (3337858)Time elapsed: 0.201 s % 53.19/7.78 % (3337858)Peak memory usage: 50 MB % 53.19/7.78 % (3337858)Instructions burned: 921 (million) % 53.19/7.78 % (3337864)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3541134344:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 53.19/7.78 % TRYING [3] % 53.19/7.78 % (3337864)Cannot represent all propositional literals internally % 124.30/17.98 % (3337864)Refutation not found, incomplete strategy % 124.30/17.98 % (3337864)------------------------------ % 124.30/17.98 % (3337864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.30/17.98 % (3337864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.30/17.98 % (3337864)CaDiCaL version: 2.1.3 % 124.30/17.98 % (3337864)Termination reason: Refutation not found, incomplete strategy % 124.30/17.98 % (3337864)Time elapsed: 0.106 s % 124.30/17.98 % (3337864)Peak memory usage: 18 MB % 124.30/17.98 % (3337864)Instructions burned: 409 (million) % 124.30/17.98 % (3337864)------------------------------ % 124.30/17.98 % (3337864)------------------------------ % 124.30/17.98 % (3337866)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=814385181:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 124.30/17.98 % (3337862)Instruction limit reached! % 124.30/17.98 % (3337862)------------------------------ % 124.30/17.98 % (3337862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.30/17.98 % (3337862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.30/17.98 % (3337862)CaDiCaL version: 2.1.3 % 124.30/17.98 % (3337862)Termination reason: Instruction limit % 124.30/17.98 % (3337862)Termination phase: Saturation % 124.30/17.98 % (3337862)Time elapsed: 0.440 s % 124.30/17.98 % (3337862)Peak memory usage: 28 MB % 124.30/17.98 % (3337862)Instructions burned: 1472 (million) % 124.30/17.98 % (3337868)ott-2_1_sil=16000:newcnf=on:random_seed=4006145073:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi) % 124.30/17.98 % (3337868)Instruction limit reached! % 124.30/17.98 % (3337868)------------------------------ % 124.30/17.98 % (3337868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.30/17.98 % (3337868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.30/17.98 % (3337868)CaDiCaL version: 2.1.3 % 124.30/17.98 % (3337868)Termination reason: Instruction limit % 124.30/17.98 % (3337868)Termination phase: Saturation % 124.30/17.98 % (3337868)Time elapsed: 0.281 s % 124.30/17.98 % (3337868)Peak memory usage: 17 MB % 124.30/17.98 % (3337868)Instructions burned: 871 (million) % 124.30/17.98 % (3337870)ott+10_1_sil=32000:tgt=ground:random_seed=1862007088:i=5114:av=off_2985 on theBenchmark for (2985ds/5114Mi) % 124.30/17.98 % (3337866)Cannot represent all propositional literals internally % 124.30/17.98 % (3337866)Refutation not found, incomplete strategy % 124.30/17.98 % (3337866)------------------------------ % 124.30/17.98 % (3337866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.30/17.98 % (3337866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.30/17.98 % (3337866)CaDiCaL version: 2.1.3 % 124.30/17.98 % (3337866)Termination reason: Refutation not found, incomplete strategy % 124.30/17.98 % (3337866)Time elapsed: 0.528 s % 124.30/17.98 % (3337866)Peak memory usage: 32 MB % 124.30/17.98 % (3337866)Instructions burned: 2011 (million) % 124.30/17.98 % (3337866)------------------------------ % 124.30/17.98 % (3337866)------------------------------ % 124.30/17.98 % (3337872)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3656038270:i=54282_2984 on theBenchmark for (2984ds/54282Mi) % 124.30/17.98 % TRYING [1] % 124.30/17.98 % TRYING [2] % 124.30/17.98 % TRYING [3] % 124.30/17.98 % TRYING [4] % 124.30/17.98 % TRYING [4] % 124.30/17.98 % (3337859)Instruction limit reached! % 124.30/17.98 % (3337859)------------------------------ % 124.30/17.98 % (3337859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.30/17.98 % (3337859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.30/17.98 % (3337859)CaDiCaL version: 2.1.3 % 124.30/17.98 % (3337859)Termination reason: Instruction limit % 124.30/17.98 % (3337859)Termination phase: Saturation % 124.30/17.98 % (3337859)Time elapsed: 1.549 s % 124.30/17.98 % (3337859)Peak memory usage: 33 MB % 124.30/17.98 % (3337859)Instructions burned: 5133 (million) % 124.30/17.98 % (3337874)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1471525527:i=3512:aac=none_2977 on theBenchmark for (2977ds/3512Mi) % 124.30/17.98 % TRYING [5] % 124.30/17.98 % (3337870)Instruction limit reached! % 124.30/17.98 % (3337870)------------------------------ % 124.30/17.98 % (3337870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.30/17.98 % (3337870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.30/17.98 % (3337870)CaDiCaL version: 2.1.3 % 124.30/17.98 % (3337870)Termination reason: Instruction limit % 124.30/17.98 % (3337870)Termination phase: Saturation % 124.30/17.98 % (3337870)Time elapsed: 1.765 s % 124.30/17.98 % (3337870)Peak memory usage: 31 MB % 169.47/24.27 % (3337870)Instructions burned: 5116 (million) % 169.47/24.27 % (3337876)dis+21_1_sil=32000:sas=cadical:random_seed=20320367:i=3773:amm=off_2967 on theBenchmark for (2967ds/3773Mi) % 169.47/24.27 % (3337874)Instruction limit reached! % 169.47/24.27 % (3337874)------------------------------ % 169.47/24.27 % (3337874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.47/24.27 % (3337874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.47/24.27 % (3337874)CaDiCaL version: 2.1.3 % 169.47/24.27 % (3337874)Termination reason: Instruction limit % 169.47/24.27 % (3337874)Termination phase: Saturation % 169.47/24.27 % (3337874)Time elapsed: 1.101 s % 169.47/24.27 % (3337874)Peak memory usage: 30 MB % 169.47/24.27 % (3337874)Instructions burned: 3514 (million) % 169.47/24.27 % (3337878)ott+11_1_sil=16000:gs=on:random_seed=3370568562:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2966 on theBenchmark for (2966ds/2251Mi) % 169.47/24.27 % TRYING [5] % 169.47/24.27 % (3337878)Instruction limit reached! % 169.47/24.27 % (3337878)------------------------------ % 169.47/24.27 % (3337878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.47/24.27 % (3337878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.47/24.27 % (3337878)CaDiCaL version: 2.1.3 % 169.47/24.27 % (3337878)Termination reason: Instruction limit % 169.47/24.27 % (3337878)Termination phase: Saturation % 169.47/24.27 % (3337878)Time elapsed: 0.736 s % 169.47/24.27 % (3337878)Peak memory usage: 38 MB % 169.47/24.27 % (3337878)Instructions burned: 2251 (million) % 169.47/24.27 % (3337880)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=426529205:fmbsr=1.6:i=67534_2958 on theBenchmark for (2958ds/67534Mi) % 169.47/24.27 % (3337876)Instruction limit reached! % 169.47/24.27 % (3337876)------------------------------ % 169.47/24.27 % (3337876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.47/24.27 % (3337876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.47/24.27 % (3337876)CaDiCaL version: 2.1.3 % 169.47/24.27 % (3337876)Termination reason: Instruction limit % 169.47/24.27 % (3337876)Termination phase: Saturation % 169.47/24.27 % (3337876)Time elapsed: 1.191 s % 169.47/24.27 % (3337876)Peak memory usage: 32 MB % 169.47/24.27 % (3337876)Instructions burned: 3773 (million) % 169.47/24.27 % (3337882)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3265604566:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2955 on theBenchmark for (2955ds/4591Mi) % 169.47/24.27 % TRYING [7] % 169.47/24.27 % (3337882)Instruction limit reached! % 169.47/24.27 % (3337882)------------------------------ % 169.47/24.27 % (3337882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.47/24.27 % (3337882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.47/24.27 % (3337882)CaDiCaL version: 2.1.3 % 169.47/24.27 % (3337882)Termination reason: Instruction limit % 169.47/24.27 % (3337882)Termination phase: Saturation % 169.47/24.27 % (3337882)Time elapsed: 1.360 s % 169.47/24.27 % (3337882)Peak memory usage: 54 MB % 169.47/24.27 % (3337882)Instructions burned: 4594 (million) % 169.47/24.27 % (3337884)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=37752459:i=29340_2941 on theBenchmark for (2941ds/29340Mi) % 169.47/24.27 % TRYING [5] % 169.47/24.27 % (3337854)Instruction limit reached! % 169.47/24.27 % (3337854)------------------------------ % 169.47/24.27 % (3337854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.47/24.27 % (3337854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.47/24.27 % (3337854)CaDiCaL version: 2.1.3 % 169.47/24.27 % (3337854)Termination reason: Instruction limit % 169.47/24.27 % (3337854)Termination phase: Finite model building constraint generation % 169.47/24.27 % (3337854)Time elapsed: 5.545 s % 169.47/24.27 % (3337854)Peak memory usage: 437 MB % 169.47/24.27 % (3337854)Instructions burned: 22062 (million) % 169.47/24.27 % (3337886)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3468429506:i=5211_2938 on theBenchmark for (2938ds/5211Mi) % 169.47/24.27 % (3337886)Instruction limit reached! % 169.47/24.27 % (3337886)------------------------------ % 169.47/24.27 % (3337886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.47/24.27 % (3337886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.47/24.27 % (3337886)CaDiCaL version: 2.1.3 % 169.47/24.27 % (3337886)Termination reason: Instruction limit % 169.47/24.27 % (3337886)Termination phase: Saturation % 169.47/24.27 % (3337886)Time elapsed: 1.477 s % 169.47/24.27 % (3337886)Peak memory usage: 42 MB % 169.47/24.27 % (3337886)Instructions burned: 5212 (million) % 208.25/29.79 % (3338065)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2041799711:i=5497:nm=2_2923 on theBenchmark for (2923ds/5497Mi) % 208.25/29.79 % TRYING [17] % 208.25/29.79 % (3338065)Instruction limit reached! % 208.25/29.79 % (3338065)------------------------------ % 208.25/29.79 % (3338065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.25/29.79 % (3338065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.25/29.79 % (3338065)CaDiCaL version: 2.1.3 % 208.25/29.79 % (3338065)Termination reason: Instruction limit % 208.25/29.79 % (3338065)Termination phase: Finite model building constraint generation % 208.25/29.79 % (3338065)Time elapsed: 1.283 s % 208.25/29.79 % (3338065)Peak memory usage: 344 MB % 208.25/29.79 % (3338065)Instructions burned: 5497 (million) % 208.25/29.79 % (3338149)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4185653817:fmbsr=2:i=46332_2910 on theBenchmark for (2910ds/46332Mi) % 208.25/29.79 % TRYING [15] % 208.25/29.79 % TRYING [6] % 208.25/29.79 % TRYING [6] % 208.25/29.79 % (3337872)Instruction limit reached! % 208.25/29.79 % (3337872)------------------------------ % 208.25/29.79 % (3337872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.25/29.79 % (3337872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.25/29.79 % (3337872)CaDiCaL version: 2.1.3 % 208.25/29.79 % (3337872)Termination reason: Instruction limit % 208.25/29.79 % (3337872)Termination phase: Finite model building constraint generation % 208.25/29.79 % (3337872)Time elapsed: 12.124 s % 208.25/29.79 % (3337872)Peak memory usage: 1552 MB % 208.25/29.79 % (3337872)Instructions burned: 54312 (million) % 208.25/29.79 % (3337884)Instruction limit reached! % 208.25/29.79 % (3337884)------------------------------ % 208.25/29.79 % (3337884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.25/29.79 % (3337884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.25/29.79 % (3337884)CaDiCaL version: 2.1.3 % 208.25/29.79 % (3337884)Termination reason: Instruction limit % 208.25/29.79 % (3337884)Termination phase: Saturation % 208.25/29.79 % (3337884)Time elapsed: 7.973 s % 208.25/29.79 % (3337884)Peak memory usage: 180 MB % 208.25/29.79 % (3337884)Instructions burned: 29342 (million) % 208.25/29.79 % (3338151)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2763620653:i=14071_2861 on theBenchmark for (2861ds/14071Mi) % 208.25/29.79 % (3338153)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3367529565:i=22565:add=on:rawr=on_2861 on theBenchmark for (2861ds/22565Mi) % 208.25/29.79 % TRYING [12] % 208.25/29.79 % (3338151)Instruction limit reached! % 208.25/29.79 % (3338151)------------------------------ % 208.25/29.79 % (3338151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.25/29.79 % (3338151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.25/29.79 % (3338151)CaDiCaL version: 2.1.3 % 208.25/29.79 % (3338151)Termination reason: Instruction limit % 208.25/29.79 % (3338151)Termination phase: Finite model building constraint generation % 208.25/29.79 % (3338151)Time elapsed: 2.668 s % 208.25/29.79 % (3338151)Peak memory usage: 803 MB % 208.25/29.79 % (3338151)Instructions burned: 14072 (million) % 208.25/29.79 % (3338155)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=535343940:i=8173:av=off_2834 on theBenchmark for (2834ds/8173Mi) % 208.25/29.79 % (3337880)Instruction limit reached! % 208.25/29.79 % (3337880)------------------------------ % 208.25/29.79 % (3337880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.25/29.79 % (3337880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.25/29.79 % (3337880)CaDiCaL version: 2.1.3 % 208.25/29.79 % (3337880)Termination reason: Instruction limit % 208.25/29.79 % (3337880)Termination phase: Finite model building constraint generation % 208.25/29.79 % (3337880)Time elapsed: 12.589 s % 208.25/29.79 % (3337880)Peak memory usage: 3425 MB % 208.25/29.79 % (3337880)Instructions burned: 67540 (million) % 208.25/29.79 % (3338157)dis+10_16:1_sil=16000:random_seed=1450906403:i=9155:fsr=off_2829 on theBenchmark for (2829ds/9155Mi) % 208.25/29.79 % (3337822)Instruction limit reached! % 208.25/29.79 % (3337822)------------------------------ % 208.25/29.79 % (3337822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.25/29.79 % (3337822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.25/29.79 % (3337822)CaDiCaL version: 2.1.3 % 208.25/29.79 % (3337822)Termination reason: Instruction limit % 208.25/29.79 % (3337822)Termination phase: Saturation % 300.46/42.93 % (3337822)Time elapsed: 17.807 s % 300.46/42.93 % (3337822)Peak memory usage: 147 MB % 300.46/42.93 % (3337822)Instructions burned: 88027 (million) % 300.46/42.93 % (3338159)ott-3_8_sil=64000:random_seed=2300249782:i=20139:bs=on_2821 on theBenchmark for (2821ds/20139Mi) % 300.46/42.93 % (3338149)Instruction limit reached! % 300.46/42.93 % (3338149)------------------------------ % 300.46/42.93 % (3338149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.46/42.93 % (3338149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.46/42.93 % (3338149)CaDiCaL version: 2.1.3 % 300.46/42.93 % (3338149)Termination reason: Instruction limit % 300.46/42.93 % (3338149)Termination phase: Finite model building constraint generation % 300.46/42.93 % (3338149)Time elapsed: 8.888 s % 300.46/42.93 % (3338149)Peak memory usage: 2618 MB % 300.46/42.93 % (3338149)Instructions burned: 46335 (million) % 300.46/42.93 % (3338161)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=766641638:fmbsr=2:i=32576_2818 on theBenchmark for (2818ds/32576Mi) % 300.46/42.93 % TRYING [9] % 300.46/42.93 % (3338153)Instruction limit reached! % 300.46/42.93 % (3338153)------------------------------ % 300.46/42.93 % (3338153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.46/42.93 % (3338153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.46/42.93 % (3338153)CaDiCaL version: 2.1.3 % 300.46/42.93 % (3338153)Termination reason: Instruction limit % 300.46/42.93 % (3338153)Termination phase: Saturation % 300.46/42.93 % (3338153)Time elapsed: 4.544 s % 300.46/42.93 % (3338153)Peak memory usage: 42 MB % 300.46/42.93 % (3338153)Instructions burned: 22568 (million) % 300.46/42.93 % (3338163)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2975450201:i=11404_2816 on theBenchmark for (2816ds/11404Mi) % 300.46/42.93 % (3338155)Instruction limit reached! % 300.46/42.93 % (3338155)------------------------------ % 300.46/42.93 % (3338155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.46/42.93 % (3338155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.46/42.93 % (3338155)CaDiCaL version: 2.1.3 % 300.46/42.93 % (3338155)Termination reason: Instruction limit % 300.46/42.93 % (3338155)Termination phase: Saturation % 300.46/42.93 % (3338155)Time elapsed: 2.828 s % 300.46/42.93 % (3338155)Peak memory usage: 67 MB % 300.46/42.93 % (3338155)Instructions burned: 8176 (million) % 300.46/42.93 % (3338165)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=24975323:i=14134_2806 on theBenchmark for (2806ds/14134Mi) % 300.46/42.93 % (3338157)Instruction limit reached! % 300.46/42.93 % (3338157)------------------------------ % 300.46/42.93 % (3338157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.46/42.93 % (3338157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.46/42.93 % (3338157)CaDiCaL version: 2.1.3 % 300.46/42.93 % (3338157)Termination reason: Instruction limit % 300.46/42.93 % (3338157)Termination phase: Saturation % 300.46/42.93 % (3338157)Time elapsed: 2.491 s % 300.46/42.93 % (3338157)Peak memory usage: 84 MB % 300.46/42.93 % (3338157)Instructions burned: 9158 (million) % 300.46/42.93 % (3338167)dis+33_16_sil=32000:sac=on:random_seed=600243017:i=15851:nm=0_2804 on theBenchmark for (2804ds/15851Mi) % 300.46/42.93 % (3338163)Instruction limit reached! % 300.46/42.93 % (3338163)------------------------------ % 300.46/42.93 % (3338163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.46/42.93 % (3338163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.46/42.93 % (3338163)CaDiCaL version: 2.1.3 % 300.46/42.93 % (3338163)Termination reason: Instruction limit % 300.46/42.93 % (3338163)Termination phase: Saturation % 300.46/42.93 % (3338163)Time elapsed: 4.259 s % 300.46/42.93 % (3338163)Peak memory usage: 82 MB % 300.46/42.93 % (3338163)Instructions burned: 11404 (million) % 300.46/42.93 % (3338169)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1221120901:avsq=on:i=17627:add=on:amm=off_2773 on theBenchmark for (2773ds/17627Mi) % 300.46/42.93 % (3338167)Instruction limit reached! % 300.46/42.93 % (3338167)------------------------------ % 300.46/42.93 % (3338167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.46/42.93 % (3338167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.46/42.93 % (3338167)CaDiCaL version: 2.1.3 % 300.46/42.93 % (3338167)Termination reason: Instruction limit % 300.46/42.93 % (3338167)Termination phase: Saturation % 300.46/42.93 % (3338167)Time elapsed: 4.584 s % 300.46/42.93 % (3338167)Peak memory usage: 93 MB % 300.46/42.93 % (3338167)Instructions burned: 15851 (million) % 300.46/42.93 % (3338171)ott+10_64_anc=all:si % 300.46/42.93 Terminated % 300.46/42.93 % Vampire exiting %------------------------------------------------------------------------------