%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV760-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:22 PM UTC 2026 % Result : Timeout 300.13s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWV760-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.06/0.11 % Computer : n012.cluster.edu % 0.06/0.11 % Model : x86_64 x86_64 % 0.06/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.11 % Memory : 8046.5625MB % 0.06/0.11 % OS : Linux 6.8.0-71-generic % 0.06/0.11 % CPULimit : 300 % 0.06/0.11 % WCLimit : 300 % 0.06/0.11 % DateTime : Mon Sep 28 12:28:49 UTC 2026 % 0.06/0.11 % CPUTime : % 0.06/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.06/0.13 Running first-order model finding % 0.06/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 % 10.09/1.63 % (3346362)Will run a generic schedule for satisfiability detection. % 10.09/1.63 % (3346368)% WARNING: option uhcvi not known. % 10.09/1.63 % (3346370)dis+10_1_sil=32000:sp=arity:random_seed=654881030:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 10.09/1.63 % (3346369)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1952729425:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 10.09/1.63 % (3346367)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=911185683_2999 on theBenchmark for (2999ds/0Mi) % 10.09/1.63 % (3346368)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3159806269:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 10.09/1.63 % (3346371)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=200909231:i=116_2999 on theBenchmark for (2999ds/116Mi) % 10.09/1.63 % (3346372)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2918607714:i=131_2999 on theBenchmark for (2999ds/131Mi) % 10.09/1.63 % (3346373)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=550821429:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 10.09/1.63 % (3346370)Instruction limit reached! % 10.09/1.63 % (3346370)------------------------------ % 10.09/1.63 % (3346370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.09/1.63 % (3346370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/1.63 % (3346370)CaDiCaL version: 2.1.3 % 10.09/1.63 % (3346370)Termination reason: Instruction limit % 10.09/1.63 % (3346370)Termination phase: Saturation % 10.09/1.63 % (3346370)Time elapsed: 0.036 s % 10.09/1.63 % (3346370)Peak memory usage: 13 MB % 10.09/1.63 % (3346370)Instructions burned: 105 (million) % 10.09/1.63 % (3346371)Instruction limit reached! % 10.09/1.63 % (3346371)------------------------------ % 10.09/1.63 % (3346371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.09/1.63 % (3346371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/1.63 % (3346371)CaDiCaL version: 2.1.3 % 10.09/1.63 % (3346371)Termination reason: Instruction limit % 10.09/1.63 % (3346371)Termination phase: Saturation % 10.09/1.63 % (3346371)Time elapsed: 0.038 s % 10.09/1.63 % (3346371)Peak memory usage: 13 MB % 10.09/1.63 % (3346371)Instructions burned: 116 (million) % 10.09/1.63 % (3346372)Instruction limit reached! % 10.09/1.63 % (3346372)------------------------------ % 10.09/1.63 % (3346372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.09/1.63 % (3346372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/1.63 % (3346372)CaDiCaL version: 2.1.3 % 10.09/1.63 % (3346372)Termination reason: Instruction limit % 10.09/1.63 % (3346372)Termination phase: Saturation % 10.09/1.63 % (3346372)Time elapsed: 0.045 s % 10.09/1.63 % (3346372)Peak memory usage: 13 MB % 10.09/1.63 % (3346372)Instructions burned: 133 (million) % 10.09/1.63 % (3346381)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2153147094:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 10.09/1.63 % (3346382)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3229158267:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 10.09/1.63 % (3346383)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=1342058890:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 10.09/1.63 % (3346373)Instruction limit reached! % 10.09/1.63 % (3346373)------------------------------ % 10.09/1.63 % (3346373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.09/1.63 % (3346373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/1.63 % (3346373)CaDiCaL version: 2.1.3 % 10.09/1.63 % (3346373)Termination reason: Instruction limit % 10.09/1.63 % (3346373)Termination phase: Saturation % 10.09/1.63 % (3346373)Time elapsed: 0.058 s % 10.09/1.63 % (3346373)Peak memory usage: 13 MB % 10.09/1.63 % (3346373)Instructions burned: 162 (million) % 10.09/1.63 % (3346387)ott-21_1_sil=16000:fs=off:random_seed=1826384900:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 10.09/1.63 % (3346382)Instruction limit reached! % 10.09/1.63 % (3346382)------------------------------ % 10.09/1.63 % (3346382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.09/1.63 % (3346382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/1.63 % (3346382)CaDiCaL version: 2.1.3 % 25.67/3.86 % (3346382)Termination reason: Instruction limit % 25.67/3.86 % (3346382)Termination phase: Saturation % 25.67/3.86 % (3346382)Time elapsed: 0.045 s % 25.67/3.86 % (3346382)Peak memory usage: 13 MB % 25.67/3.86 % (3346382)Instructions burned: 133 (million) % 25.67/3.86 % TRYING [1] % 25.67/3.86 % TRYING [2] % 25.67/3.86 % (3346389)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1492538616:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 25.67/3.86 % (3346387)Instruction limit reached! % 25.67/3.86 % (3346387)------------------------------ % 25.67/3.86 % (3346387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.67/3.86 % (3346387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.67/3.86 % (3346387)CaDiCaL version: 2.1.3 % 25.67/3.86 % (3346387)Termination reason: Instruction limit % 25.67/3.86 % (3346387)Termination phase: Saturation % 25.67/3.86 % (3346387)Time elapsed: 0.037 s % 25.67/3.86 % (3346387)Peak memory usage: 12 MB % 25.67/3.86 % (3346387)Instructions burned: 185 (million) % 25.67/3.86 % (3346391)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1952939349:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 25.67/3.86 % TRYING [1] % 25.67/3.86 % TRYING [3] % 25.67/3.86 % TRYING [2] % 25.67/3.86 % TRYING [3] % 25.67/3.86 % (3346381)Instruction limit reached! % 25.67/3.86 % (3346381)------------------------------ % 25.67/3.86 % (3346381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.67/3.86 % (3346381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.67/3.86 % (3346381)CaDiCaL version: 2.1.3 % 25.67/3.86 % (3346381)Termination reason: Instruction limit % 25.67/3.86 % (3346381)Termination phase: Finite model building constraint generation % 25.67/3.86 % (3346381)Time elapsed: 0.170 s % 25.67/3.86 % (3346381)Peak memory usage: 29 MB % 25.67/3.86 % (3346381)Instructions burned: 716 (million) % 25.67/3.86 % TRYING [1] % 25.67/3.86 % (3346393)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1561045242:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 25.67/3.86 % TRYING [2] % 25.67/3.86 % (3346389)Instruction limit reached! % 25.67/3.86 % (3346389)------------------------------ % 25.67/3.86 % (3346389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.67/3.86 % (3346389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.67/3.86 % (3346389)CaDiCaL version: 2.1.3 % 25.67/3.86 % (3346389)Termination reason: Instruction limit % 25.67/3.86 % (3346389)Termination phase: Saturation % 25.67/3.86 % (3346389)Time elapsed: 0.158 s % 25.67/3.86 % (3346389)Peak memory usage: 14 MB % 25.67/3.86 % (3346389)Instructions burned: 478 (million) % 25.67/3.86 % (3346383)Instruction limit reached! % 25.67/3.86 % (3346383)------------------------------ % 25.67/3.86 % (3346383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.67/3.86 % (3346383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.67/3.86 % (3346383)CaDiCaL version: 2.1.3 % 25.67/3.86 % (3346383)Termination reason: Instruction limit % 25.67/3.86 % (3346383)Termination phase: Saturation % 25.67/3.86 % (3346383)Time elapsed: 0.212 s % 25.67/3.86 % (3346383)Peak memory usage: 17 MB % 25.67/3.86 % (3346383)Instructions burned: 685 (million) % 25.67/3.86 % (3346395)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2251624246:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 25.67/3.86 % (3346396)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=3251899483: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) % 25.67/3.86 % (3346391)Instruction limit reached! % 25.67/3.86 % (3346391)------------------------------ % 25.67/3.86 % (3346391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.67/3.86 % (3346391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.67/3.86 % (3346391)CaDiCaL version: 2.1.3 % 25.67/3.86 % (3346391)Termination reason: Instruction limit % 25.67/3.86 % (3346391)Termination phase: Finite model building SAT solving % 25.67/3.86 % (3346391)Time elapsed: 0.226 s % 25.67/3.86 % (3346391)Peak memory usage: 30 MB % 25.67/3.86 % (3346391)Instructions burned: 869 (million) % 25.67/3.86 % (3346399)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=703727576:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 25.67/3.86 % TRYING [4] % 25.67/3.86 % (3346396)Instruction limit reached! % 25.67/3.86 % (3346396)------------------------------ % 25.67/3.86 % (3346396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.11/8.16 % (3346396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.11/8.16 % (3346396)CaDiCaL version: 2.1.3 % 56.11/8.16 % (3346396)Termination reason: Instruction limit % 56.11/8.16 % (3346396)Termination phase: Saturation % 56.11/8.16 % (3346396)Time elapsed: 0.232 s % 56.11/8.16 % (3346396)Peak memory usage: 19 MB % 56.11/8.16 % (3346396)Instructions burned: 693 (million) % 56.11/8.16 % (3346395)Instruction limit reached! % 56.11/8.16 % (3346395)------------------------------ % 56.11/8.16 % (3346395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.11/8.16 % (3346395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.11/8.16 % (3346395)CaDiCaL version: 2.1.3 % 56.11/8.16 % (3346395)Termination reason: Instruction limit % 56.11/8.16 % (3346395)Termination phase: Finite model building constraint generation % 56.11/8.16 % (3346395)Time elapsed: 0.240 s % 56.11/8.16 % (3346395)Peak memory usage: 81 MB % 56.11/8.16 % (3346395)Instructions burned: 891 (million) % 56.11/8.16 % (3346401)fmb+10_1_sil=64000:random_seed=2578671114:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 56.11/8.16 % (3346402)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2242333712:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 56.11/8.16 % (3346399)Instruction limit reached! % 56.11/8.16 % (3346399)------------------------------ % 56.11/8.16 % (3346399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.11/8.16 % (3346399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.11/8.16 % (3346399)CaDiCaL version: 2.1.3 % 56.11/8.16 % (3346399)Termination reason: Instruction limit % 56.11/8.16 % (3346399)Termination phase: Saturation % 56.11/8.16 % (3346399)Time elapsed: 0.256 s % 56.11/8.16 % (3346399)Peak memory usage: 19 MB % 56.11/8.16 % (3346399)Instructions burned: 881 (million) % 56.11/8.16 % TRYING [1] % 56.11/8.16 % (3346405)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3949978817:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 56.11/8.16 % (3346393)Instruction limit reached! % 56.11/8.16 % (3346393)------------------------------ % 56.11/8.16 % (3346393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.11/8.16 % (3346393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.11/8.16 % (3346393)CaDiCaL version: 2.1.3 % 56.11/8.16 % (3346393)Termination reason: Instruction limit % 56.11/8.16 % (3346393)Termination phase: Saturation % 56.11/8.16 % (3346393)Time elapsed: 0.400 s % 56.11/8.16 % (3346393)Peak memory usage: 24 MB % 56.11/8.16 % (3346393)Instructions burned: 1181 (million) % 56.11/8.16 % TRYING [20] % 56.11/8.16 % TRYING [2] % 56.11/8.16 % (3346407)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4134871339:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 56.11/8.16 % TRYING [8] % 56.11/8.16 % TRYING [3] % 56.11/8.16 % (3346405)Instruction limit reached! % 56.11/8.16 % (3346405)------------------------------ % 56.11/8.16 % (3346405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.11/8.16 % (3346405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.11/8.16 % (3346405)CaDiCaL version: 2.1.3 % 56.11/8.16 % (3346405)Termination reason: Instruction limit % 56.11/8.16 % (3346405)Termination phase: Finite model building constraint generation % 56.11/8.16 % (3346405)Time elapsed: 0.201 s % 56.11/8.16 % (3346405)Peak memory usage: 51 MB % 56.11/8.16 % (3346405)Instructions burned: 922 (million) % 56.11/8.16 % (3346409)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2393243849:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 56.11/8.16 % (3346409)Instruction limit reached! % 56.11/8.16 % (3346409)------------------------------ % 56.11/8.16 % (3346409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.11/8.16 % (3346409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.11/8.16 % (3346409)CaDiCaL version: 2.1.3 % 56.11/8.16 % (3346409)Termination reason: Instruction limit % 56.11/8.16 % (3346409)Termination phase: Saturation % 56.11/8.16 % (3346409)Time elapsed: 0.499 s % 56.11/8.16 % (3346409)Peak memory usage: 31 MB % 56.11/8.16 % (3346409)Instructions burned: 1474 (million) % 56.11/8.16 % TRYING [5] % 56.11/8.16 % (3346411)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3407698567:i=6324_2986 on theBenchmark for (2986ds/6324Mi) % 56.11/8.16 % (3346411)Cannot represent all propositional literals internally % 56.11/8.16 % (3346411)Refutation not found, incomplete strategy % 56.11/8.16 % (3346411)------------------------------ % 141.28/20.26 % (3346411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.28/20.26 % (3346411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.28/20.26 % (3346411)CaDiCaL version: 2.1.3 % 141.28/20.26 % (3346411)Termination reason: Refutation not found, incomplete strategy % 141.28/20.26 % (3346411)Time elapsed: 0.103 s % 141.28/20.26 % (3346411)Peak memory usage: 17 MB % 141.28/20.26 % (3346411)Instructions burned: 382 (million) % 141.28/20.26 % (3346411)------------------------------ % 141.28/20.26 % (3346411)------------------------------ % 141.28/20.26 % (3346413)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=203691863:fmbsr=2.30978:i=2174_2985 on theBenchmark for (2985ds/2174Mi) % 141.28/20.26 % TRYING [4] % 141.28/20.26 % (3346413)Cannot represent all propositional literals internally % 141.28/20.26 % (3346413)Refutation not found, incomplete strategy % 141.28/20.26 % (3346413)------------------------------ % 141.28/20.26 % (3346413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.28/20.26 % (3346413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.28/20.26 % (3346413)CaDiCaL version: 2.1.3 % 141.28/20.26 % (3346413)Termination reason: Refutation not found, incomplete strategy % 141.28/20.26 % (3346413)Time elapsed: 0.380 s % 141.28/20.26 % (3346413)Peak memory usage: 26 MB % 141.28/20.26 % (3346413)Instructions burned: 1457 (million) % 141.28/20.26 % (3346413)------------------------------ % 141.28/20.26 % (3346413)------------------------------ % 141.28/20.26 % (3346415)ott-2_1_sil=16000:newcnf=on:random_seed=1464396:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2981 on theBenchmark for (2981ds/869Mi) % 141.28/20.26 % (3346415)Instruction limit reached! % 141.28/20.26 % (3346415)------------------------------ % 141.28/20.26 % (3346415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.28/20.26 % (3346415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.28/20.26 % (3346415)CaDiCaL version: 2.1.3 % 141.28/20.26 % (3346415)Termination reason: Instruction limit % 141.28/20.26 % (3346415)Termination phase: Saturation % 141.28/20.26 % (3346415)Time elapsed: 0.252 s % 141.28/20.26 % (3346415)Peak memory usage: 17 MB % 141.28/20.26 % (3346415)Instructions burned: 872 (million) % 141.28/20.26 % (3346417)ott+10_1_sil=32000:tgt=ground:random_seed=2386728335:i=5114:av=off_2978 on theBenchmark for (2978ds/5114Mi) % 141.28/20.26 % (3346407)Instruction limit reached! % 141.28/20.26 % (3346407)------------------------------ % 141.28/20.26 % (3346407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.28/20.26 % (3346407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.28/20.26 % (3346407)CaDiCaL version: 2.1.3 % 141.28/20.26 % (3346407)Termination reason: Instruction limit % 141.28/20.26 % (3346407)Termination phase: Saturation % 141.28/20.26 % (3346407)Time elapsed: 1.655 s % 141.28/20.26 % (3346407)Peak memory usage: 46 MB % 141.28/20.26 % (3346407)Instructions burned: 5134 (million) % 141.28/20.26 % (3346419)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1646331281:i=54282_2976 on theBenchmark for (2976ds/54282Mi) % 141.28/20.26 % TRYING [1] % 141.28/20.26 % TRYING [2] % 141.28/20.26 % (3346402)Instruction limit reached! % 141.28/20.26 % (3346402)------------------------------ % 141.28/20.26 % (3346402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.28/20.26 % (3346402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.28/20.26 % (3346402)CaDiCaL version: 2.1.3 % 141.28/20.26 % (3346402)Termination reason: Instruction limit % 141.28/20.26 % (3346402)Termination phase: Finite model building constraint generation % 141.28/20.26 % (3346402)Time elapsed: 1.930 s % 141.28/20.26 % (3346402)Peak memory usage: 637 MB % 141.28/20.26 % (3346402)Instructions burned: 9519 (million) % 141.28/20.26 % TRYING [3] % 141.28/20.26 % (3346421)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3521377167:i=3512:aac=none_2974 on theBenchmark for (2974ds/3512Mi) % 141.28/20.26 % TRYING [4] % 141.28/20.26 % (3346421)Instruction limit reached! % 141.28/20.26 % (3346421)------------------------------ % 141.28/20.26 % (3346421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.28/20.26 % (3346421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.28/20.26 % (3346421)CaDiCaL version: 2.1.3 % 141.28/20.26 % (3346421)Termination reason: Instruction limit % 141.28/20.26 % (3346421)Termination phase: Saturation % 141.28/20.26 % (3346421)Time elapsed: 1.153 s % 141.28/20.26 % (3346421)Peak memory usage: 40 MB % 141.28/20.26 % (3346421)Instructions burned: 3513 (million) % 141.28/20.26 % (3346423)dis+21_1_sil=32000:sas=cadical:random_seed=3643795475:i=3773:amm=off_2962 on theBenchmark for (2962ds/3773Mi) % 189.36/27.03 % TRYING [5] % 189.36/27.03 % (3346417)Instruction limit reached! % 189.36/27.03 % (3346417)------------------------------ % 189.36/27.03 % (3346417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.36/27.03 % (3346417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.36/27.03 % (3346417)CaDiCaL version: 2.1.3 % 189.36/27.03 % (3346417)Termination reason: Instruction limit % 189.36/27.03 % (3346417)Termination phase: Saturation % 189.36/27.03 % (3346417)Time elapsed: 1.782 s % 189.36/27.03 % (3346417)Peak memory usage: 53 MB % 189.36/27.03 % (3346417)Instructions burned: 5114 (million) % 189.36/27.03 % (3346425)ott+11_1_sil=16000:gs=on:random_seed=2271671677:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2960 on theBenchmark for (2960ds/2251Mi) % 189.36/27.03 % (3346425)Instruction limit reached! % 189.36/27.03 % (3346425)------------------------------ % 189.36/27.03 % (3346425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.36/27.03 % (3346425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.36/27.03 % (3346425)CaDiCaL version: 2.1.3 % 189.36/27.03 % (3346425)Termination reason: Instruction limit % 189.36/27.03 % (3346425)Termination phase: Saturation % 189.36/27.03 % (3346425)Time elapsed: 0.713 s % 189.36/27.03 % (3346425)Peak memory usage: 27 MB % 189.36/27.03 % (3346425)Instructions burned: 2252 (million) % 189.36/27.03 % (3346427)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3114657319:fmbsr=1.6:i=67534_2953 on theBenchmark for (2953ds/67534Mi) % 189.36/27.03 % (3346423)Instruction limit reached! % 189.36/27.03 % (3346423)------------------------------ % 189.36/27.03 % (3346423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.36/27.03 % (3346423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.36/27.03 % (3346423)CaDiCaL version: 2.1.3 % 189.36/27.03 % (3346423)Termination reason: Instruction limit % 189.36/27.03 % (3346423)Termination phase: Saturation % 189.36/27.03 % (3346423)Time elapsed: 1.218 s % 189.36/27.03 % (3346423)Peak memory usage: 40 MB % 189.36/27.03 % (3346423)Instructions burned: 3773 (million) % 189.36/27.03 % (3346429)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3143097943:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2950 on theBenchmark for (2950ds/4591Mi) % 189.36/27.03 % TRYING [6] % 189.36/27.03 % TRYING [7] % 189.36/27.03 % (3346401)Instruction limit reached! % 189.36/27.03 % (3346401)------------------------------ % 189.36/27.03 % (3346401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.36/27.03 % (3346401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.36/27.03 % (3346401)CaDiCaL version: 2.1.3 % 189.36/27.03 % (3346401)Termination reason: Instruction limit % 189.36/27.03 % (3346401)Termination phase: Finite model building constraint generation % 189.36/27.03 % (3346401)Time elapsed: 5.346 s % 189.36/27.03 % (3346401)Peak memory usage: 301 MB % 189.36/27.03 % (3346401)Instructions burned: 22066 (million) % 189.36/27.03 % (3346431)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4270852134:i=29340_2940 on theBenchmark for (2940ds/29340Mi) % 189.36/27.03 % (3346429)Instruction limit reached! % 189.36/27.03 % (3346429)------------------------------ % 189.36/27.03 % (3346429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.36/27.03 % (3346429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.36/27.03 % (3346429)CaDiCaL version: 2.1.3 % 189.36/27.03 % (3346429)Termination reason: Instruction limit % 189.36/27.03 % (3346429)Termination phase: Saturation % 189.36/27.03 % (3346429)Time elapsed: 1.454 s % 189.36/27.03 % (3346429)Peak memory usage: 56 MB % 189.36/27.03 % (3346429)Instructions burned: 4591 (million) % 189.36/27.03 % (3346433)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2933569346:i=5211_2935 on theBenchmark for (2935ds/5211Mi) % 189.36/27.03 % TRYING [6] % 189.36/27.03 % (3346433)Instruction limit reached! % 189.36/27.03 % (3346433)------------------------------ % 189.36/27.03 % (3346433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.36/27.03 % (3346433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.36/27.03 % (3346433)CaDiCaL version: 2.1.3 % 189.36/27.03 % (3346433)Termination reason: Instruction limit % 189.36/27.03 % (3346433)Termination phase: Saturation % 189.36/27.03 % (3346433)Time elapsed: 1.584 s % 189.36/27.03 % (3346433)Peak memory usage: 50 MB % 189.36/27.03 % (3346433)Instructions burned: 5211 (million) % 189.36/27.03 % (3346435)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3938389999:i=5497:nm=2_2919 on theBenchmark for (2919ds/5497Mi) % 223.33/32.62 % TRYING [17] % 223.33/32.62 % (3346435)Instruction limit reached! % 223.33/32.62 % (3346435)------------------------------ % 223.33/32.62 % (3346435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.33/32.62 % (3346435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.33/32.62 % (3346435)CaDiCaL version: 2.1.3 % 223.33/32.62 % (3346435)Termination reason: Instruction limit % 223.33/32.62 % (3346435)Termination phase: Finite model building constraint generation % 223.33/32.62 % (3346435)Time elapsed: 1.109 s % 223.33/32.62 % (3346435)Peak memory usage: 365 MB % 223.33/32.62 % (3346435)Instructions burned: 5500 (million) % 223.33/32.62 % (3346437)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3102117929:fmbsr=2:i=46332_2908 on theBenchmark for (2908ds/46332Mi) % 223.33/32.62 % TRYING [15] % 223.33/32.62 % (3346419)Instruction limit reached! % 223.33/32.62 % (3346419)------------------------------ % 223.33/32.62 % (3346419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.33/32.62 % (3346419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.33/32.62 % (3346419)CaDiCaL version: 2.1.3 % 223.33/32.62 % (3346419)Termination reason: Instruction limit % 223.33/32.62 % (3346419)Termination phase: Finite model building constraint generation % 223.33/32.62 % (3346419)Time elapsed: 11.757 s % 223.33/32.62 % (3346419)Peak memory usage: 2118 MB % 223.33/32.62 % (3346419)Instructions burned: 54285 (million) % 223.33/32.62 % (3346460)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3557909806:i=14071_2857 on theBenchmark for (2857ds/14071Mi) % 223.33/32.62 % TRYING [12] % 223.33/32.62 % (3346431)Instruction limit reached! % 223.33/32.62 % (3346431)------------------------------ % 223.33/32.62 % (3346431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.33/32.62 % (3346431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.33/32.62 % (3346431)CaDiCaL version: 2.1.3 % 223.33/32.62 % (3346431)Termination reason: Instruction limit % 223.33/32.62 % (3346431)Termination phase: Saturation % 223.33/32.62 % (3346431)Time elapsed: 8.553 s % 223.33/32.62 % (3346431)Peak memory usage: 212 MB % 223.33/32.62 % (3346431)Instructions burned: 29342 (million) % 223.33/32.62 % (3346487)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=817281105:i=22565:add=on:rawr=on_2854 on theBenchmark for (2854ds/22565Mi) % 223.33/32.62 % (3346460)Instruction limit reached! % 223.33/32.62 % (3346460)------------------------------ % 223.33/32.62 % (3346460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.33/32.62 % (3346460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.33/32.62 % (3346460)CaDiCaL version: 2.1.3 % 223.33/32.62 % (3346460)Termination reason: Instruction limit % 223.33/32.62 % (3346460)Termination phase: Finite model building constraint generation % 223.33/32.62 % (3346460)Time elapsed: 2.876 s % 223.33/32.62 % (3346460)Peak memory usage: 1027 MB % 223.33/32.62 % (3346460)Instructions burned: 14076 (million) % 223.33/32.62 % (3346489)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4107135012:i=8173:av=off_2827 on theBenchmark for (2827ds/8173Mi) % 223.33/32.62 % (3346437)Instruction limit reached! % 223.33/32.62 % (3346437)------------------------------ % 223.33/32.62 % (3346437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.33/32.62 % (3346437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.33/32.62 % (3346437)CaDiCaL version: 2.1.3 % 223.33/32.62 % (3346437)Termination reason: Instruction limit % 223.33/32.62 % (3346437)Termination phase: Finite model building constraint generation % 223.33/32.62 % (3346437)Time elapsed: 8.689 s % 223.33/32.62 % (3346437)Peak memory usage: 2538 MB % 223.33/32.62 % (3346437)Instructions burned: 46336 (million) % 223.33/32.62 % (3346491)dis+10_16:1_sil=16000:random_seed=3235493297:i=9155:fsr=off_2818 on theBenchmark for (2818ds/9155Mi) % 223.33/32.62 % TRYING [7] % 223.33/32.62 % (3346487)Instruction limit reached! % 223.33/32.62 % (3346487)------------------------------ % 223.33/32.62 % (3346487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.33/32.62 % (3346487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.33/32.62 % (3346487)CaDiCaL version: 2.1.3 % 223.33/32.62 % (3346487)Termination reason: Instruction limit % 223.33/32.62 % (3346487)Termination phase: Saturation % 223.33/32.62 % (3346487)Time elapsed: 5.604 s % 223.33/32.62 % (3346487)Peak memory usage: 55 MB % 223.33/32.62 % (3346487)Instructions burned: 22568 (million) % 300.13/42.83 % (3346493)ott-3_8_sil=64000:random_seed=1949965937:i=20139:bs=on_2798 on theBenchmark for (2798ds/20139Mi) % 300.13/42.83 % (3346489)Instruction limit reached! % 300.13/42.83 % (3346489)------------------------------ % 300.13/42.83 % (3346489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.13/42.83 % (3346489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/42.83 % (3346489)CaDiCaL version: 2.1.3 % 300.13/42.83 % (3346489)Termination reason: Instruction limit % 300.13/42.83 % (3346489)Termination phase: Saturation % 300.13/42.83 % (3346489)Time elapsed: 3.010 s % 300.13/42.83 % (3346489)Peak memory usage: 91 MB % 300.13/42.83 % (3346489)Instructions burned: 8176 (million) % 300.13/42.83 % (3346495)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1008007658:fmbsr=2:i=32576_2797 on theBenchmark for (2797ds/32576Mi) % 300.13/42.83 % TRYING [9] % 300.13/42.83 % (3346491)Instruction limit reached! % 300.13/42.83 % (3346491)------------------------------ % 300.13/42.83 % (3346491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.13/42.83 % (3346491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/42.83 % (3346491)CaDiCaL version: 2.1.3 % 300.13/42.83 % (3346491)Termination reason: Instruction limit % 300.13/42.83 % (3346491)Termination phase: Saturation % 300.13/42.83 % (3346491)Time elapsed: 2.859 s % 300.13/42.83 % (3346491)Peak memory usage: 69 MB % 300.13/42.83 % (3346491)Instructions burned: 9156 (million) % 300.13/42.83 % (3346497)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1027543795:i=11404_2790 on theBenchmark for (2790ds/11404Mi) % 300.13/42.83 % (3346427)Instruction limit reached! % 300.13/42.83 % (3346427)------------------------------ % 300.13/42.83 % (3346427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.13/42.83 % (3346427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/42.83 % (3346427)CaDiCaL version: 2.1.3 % 300.13/42.83 % (3346427)Termination reason: Instruction limit % 300.13/42.83 % (3346427)Termination phase: Finite model building constraint generation % 300.13/42.83 % (3346427)Time elapsed: 16.861 s % 300.13/42.83 % (3346427)Peak memory usage: 3711 MB % 300.13/42.83 % (3346427)Instructions burned: 67534 (million) % 300.13/42.83 % (3346499)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4240034127:i=14134_2780 on theBenchmark for (2780ds/14134Mi) % 300.13/42.83 % (3346369)Instruction limit reached! % 300.13/42.83 % (3346369)------------------------------ % 300.13/42.83 % (3346369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.13/42.83 % (3346369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/42.83 % (3346369)CaDiCaL version: 2.1.3 % 300.13/42.83 % (3346369)Termination reason: Instruction limit % 300.13/42.83 % (3346369)Termination phase: Saturation % 300.13/42.83 % (3346369)Time elapsed: 23.290 s % 300.13/42.83 % (3346369)Peak memory usage: 95 MB % 300.13/42.83 % (3346369)Instructions burned: 88025 (million) % 300.13/42.83 % (3346501)dis+33_16_sil=32000:sac=on:random_seed=3267578272:i=15851:nm=0_2766 on theBenchmark for (2766ds/15851Mi) % 300.13/42.83 % (3346497)Instruction limit reached! % 300.13/42.83 % (3346497)------------------------------ % 300.13/42.83 % (3346497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.13/42.83 % (3346497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/42.83 % (3346497)CaDiCaL version: 2.1.3 % 300.13/42.83 % (3346497)Termination reason: Instruction limit % 300.13/42.83 % (3346497)Termination phase: Saturation % 300.13/42.83 % (3346497)Time elapsed: 4.087 s % 300.13/42.83 % (3346497)Peak memory usage: 99 MB % 300.13/42.83 % (3346497)Instructions burned: 11404 (million) % 300.13/42.83 % (3346503)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2106040696:avsq=on:i=17627:add=on:amm=off_2749 on theBenchmark for (2749ds/17627Mi) % 300.13/42.83 % (3346499)Instruction limit reached! % 300.13/42.83 % (3346499)------------------------------ % 300.13/42.83 % (3346499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.13/42.83 % (3346499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/42.83 % (3346499)CaDiCaL version: 2.1.3 % 300.13/42.83 % (3346499)Termination reason: Instruction limit % 300.13/42.83 % (3346499)Termination phase: Saturation % 300.13/42.83 % (3346499)Time elapsed: 4.948 s % 300.13/42.83 % (3346499)Peak memory usage: 103 MB % 300.13/42.83 % (3346499)Instructions burned: 14136 (million) % 300.13/42.83 % (3346505)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4105931563:s2a=on:i=53295_27 % 300.13/42.83 Terminated % 300.13/42.83 % Vampire exiting % 300.13/42.83 Terminated %------------------------------------------------------------------------------