%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX065+1 : TPTP v9.3.1. Released v9.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:46:25 PM UTC 2026 % Result : Timeout 295.62s 41.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX065+1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n007.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 14:57:15 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/0.21 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 % 16.10/2.54 % (2474358)Will run a generic schedule for satisfiability detection. % 16.10/2.54 % (2474364)% WARNING: option uhcvi not known. % 16.10/2.54 % (2474364)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=278245691:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 16.10/2.54 % (2474363)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2194060246_2999 on theBenchmark for (2999ds/0Mi) % 16.10/2.54 % (2474365)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2404171754:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 16.10/2.54 % (2474366)dis+10_1_sil=32000:sp=arity:random_seed=885870813:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 16.10/2.54 % (2474367)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1243630059:i=116_2999 on theBenchmark for (2999ds/116Mi) % 16.10/2.54 % (2474368)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2029363104:i=131_2999 on theBenchmark for (2999ds/131Mi) % 16.10/2.54 % (2474369)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2358251841:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 16.10/2.54 % Detected minimum model sizes of [3] % 16.10/2.54 % Detected maximum model sizes of [max] % 16.10/2.54 % TRYING [3] % 16.10/2.54 % (2474367)Instruction limit reached! % 16.10/2.54 % (2474367)------------------------------ % 16.10/2.54 % (2474367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.10/2.54 % (2474367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.10/2.54 % (2474367)CaDiCaL version: 2.1.3 % 16.10/2.54 % (2474367)Termination reason: Instruction limit % 16.10/2.54 % (2474367)Termination phase: Saturation % 16.10/2.54 % (2474367)Time elapsed: 0.053 s % 16.10/2.54 % (2474367)Peak memory usage: 12 MB % 16.10/2.54 % (2474367)Instructions burned: 117 (million) % 16.10/2.54 % (2474366)Instruction limit reached! % 16.10/2.54 % (2474366)------------------------------ % 16.10/2.54 % (2474366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.10/2.54 % (2474366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.10/2.54 % (2474366)CaDiCaL version: 2.1.3 % 16.10/2.54 % (2474366)Termination reason: Instruction limit % 16.10/2.54 % (2474366)Termination phase: Saturation % 16.10/2.54 % (2474366)Time elapsed: 0.064 s % 16.10/2.54 % (2474366)Peak memory usage: 13 MB % 16.10/2.54 % (2474366)Instructions burned: 104 (million) % 16.10/2.54 % (2474368)Instruction limit reached! % 16.10/2.54 % (2474368)------------------------------ % 16.10/2.54 % (2474368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.10/2.54 % (2474368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.10/2.54 % (2474368)CaDiCaL version: 2.1.3 % 16.10/2.54 % (2474368)Termination reason: Instruction limit % 16.10/2.54 % (2474368)Termination phase: Saturation % 16.10/2.54 % (2474368)Time elapsed: 0.068 s % 16.10/2.54 % (2474368)Peak memory usage: 14 MB % 16.10/2.54 % (2474368)Instructions burned: 132 (million) % 16.10/2.54 % (2474377)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1762416084:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 16.10/2.54 % (2474378)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4005535782:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 16.10/2.54 % (2474379)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=3493375381:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 16.10/2.54 % (2474369)Instruction limit reached! % 16.10/2.54 % (2474369)------------------------------ % 16.10/2.54 % (2474369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.10/2.54 % (2474369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.10/2.54 % (2474369)CaDiCaL version: 2.1.3 % 16.10/2.54 % (2474369)Termination reason: Instruction limit % 16.10/2.54 % (2474369)Termination phase: Saturation % 16.10/2.54 % (2474369)Time elapsed: 0.091 s % 16.10/2.54 % (2474369)Peak memory usage: 15 MB % 16.10/2.54 % (2474369)Instructions burned: 159 (million) % 16.10/2.54 % (2474383)ott-21_1_sil=16000:fs=off:random_seed=3851557994:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 16.10/2.54 % Detected minimum model sizes of [3] % 16.10/2.54 % Detected maximum model sizes of [max] % 16.10/2.54 % TRYING [3] % 16.10/2.54 % (2474378)Instruction limit reached! % 16.10/2.54 % (2474378)------------------------------ % 16.10/2.54 % (2474378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.10/5.64 % (2474378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.10/5.64 % (2474378)CaDiCaL version: 2.1.3 % 38.10/5.64 % (2474378)Termination reason: Instruction limit % 38.10/5.64 % (2474378)Termination phase: Saturation % 38.10/5.64 % (2474378)Time elapsed: 0.072 s % 38.10/5.64 % (2474378)Peak memory usage: 14 MB % 38.10/5.64 % (2474378)Instructions burned: 131 (million) % 38.10/5.64 % TRYING [4] % 38.10/5.64 % (2474385)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2018627929:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 38.10/5.64 % (2474383)Instruction limit reached! % 38.10/5.64 % (2474383)------------------------------ % 38.10/5.64 % (2474383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.10/5.64 % (2474383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.10/5.64 % (2474383)CaDiCaL version: 2.1.3 % 38.10/5.64 % (2474383)Termination reason: Instruction limit % 38.10/5.64 % (2474383)Termination phase: Saturation % 38.10/5.64 % (2474383)Time elapsed: 0.095 s % 38.10/5.64 % (2474383)Peak memory usage: 13 MB % 38.10/5.64 % (2474383)Instructions burned: 181 (million) % 38.10/5.64 % TRYING [4] % 38.10/5.64 % (2474387)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3809094295:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 38.10/5.64 % Detected minimum model sizes of [3] % 38.10/5.64 % Detected maximum model sizes of [max] % 38.10/5.64 % TRYING [3] % 38.10/5.64 % (2474377)Instruction limit reached! % 38.10/5.64 % (2474377)------------------------------ % 38.10/5.64 % (2474377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.10/5.64 % (2474377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.10/5.64 % (2474377)CaDiCaL version: 2.1.3 % 38.10/5.64 % (2474377)Termination reason: Instruction limit % 38.10/5.64 % (2474377)Termination phase: Finite model building constraint generation % 38.10/5.64 % (2474377)Time elapsed: 0.272 s % 38.10/5.64 % (2474377)Peak memory usage: 41 MB % 38.10/5.64 % (2474377)Instructions burned: 716 (million) % 38.10/5.64 % (2474389)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=416391716:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 38.10/5.64 % (2474385)Instruction limit reached! % 38.10/5.64 % (2474385)------------------------------ % 38.10/5.64 % (2474385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.10/5.64 % (2474385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.10/5.64 % (2474385)CaDiCaL version: 2.1.3 % 38.10/5.64 % (2474385)Termination reason: Instruction limit % 38.10/5.64 % (2474385)Termination phase: Saturation % 38.10/5.64 % (2474385)Time elapsed: 0.321 s % 38.10/5.64 % (2474385)Peak memory usage: 15 MB % 38.10/5.64 % (2474385)Instructions burned: 477 (million) % 38.10/5.64 % (2474379)Instruction limit reached! % 38.10/5.64 % (2474379)------------------------------ % 38.10/5.64 % (2474379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.10/5.64 % (2474379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.10/5.64 % (2474379)CaDiCaL version: 2.1.3 % 38.10/5.64 % (2474379)Termination reason: Instruction limit % 38.10/5.64 % (2474379)Termination phase: Saturation % 38.10/5.64 % (2474379)Time elapsed: 0.416 s % 38.10/5.64 % (2474379)Peak memory usage: 19 MB % 38.10/5.64 % (2474379)Instructions burned: 684 (million) % 38.10/5.64 % (2474391)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=405124553:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 38.10/5.64 % (2474392)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=2171325802: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) % 38.10/5.64 % TRYING [5] % 38.10/5.64 % (2474387)Instruction limit reached! % 38.10/5.64 % (2474387)------------------------------ % 38.10/5.64 % (2474387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.10/5.64 % (2474387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.10/5.64 % (2474387)CaDiCaL version: 2.1.3 % 38.10/5.64 % (2474387)Termination reason: Instruction limit % 38.10/5.64 % (2474387)Termination phase: Finite model building constraint generation % 38.10/5.64 % (2474387)Time elapsed: 0.371 s % 38.10/5.64 % (2474387)Peak memory usage: 30 MB % 38.10/5.64 % (2474387)Instructions burned: 866 (million) % 38.10/5.64 % (2474395)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2918715960:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 76.68/11.05 % (2474392)Instruction limit reached! % 76.68/11.05 % (2474392)------------------------------ % 76.68/11.05 % (2474392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.68/11.05 % (2474392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.68/11.05 % (2474392)CaDiCaL version: 2.1.3 % 76.68/11.05 % (2474392)Termination reason: Instruction limit % 76.68/11.05 % (2474392)Termination phase: Saturation % 76.68/11.05 % (2474392)Time elapsed: 0.395 s % 76.68/11.05 % (2474392)Peak memory usage: 26 MB % 76.68/11.05 % (2474392)Instructions burned: 693 (million) % 76.68/11.05 % (2474391)Instruction limit reached! % 76.68/11.05 % (2474391)------------------------------ % 76.68/11.05 % (2474391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.68/11.05 % (2474391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.68/11.05 % (2474391)CaDiCaL version: 2.1.3 % 76.68/11.05 % (2474391)Termination reason: Instruction limit % 76.68/11.05 % (2474391)Termination phase: Finite model building constraint generation % 76.68/11.05 % (2474391)Time elapsed: 0.404 s % 76.68/11.05 % (2474391)Peak memory usage: 101 MB % 76.68/11.05 % (2474391)Instructions burned: 889 (million) % 76.68/11.05 % (2474397)fmb+10_1_sil=64000:random_seed=3976362094:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi) % 76.68/11.05 % (2474398)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=319903048:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 76.68/11.05 % Detected minimum model sizes of [3] % 76.68/11.05 % Detected maximum model sizes of [max] % 76.68/11.05 % TRYING [3] % 76.68/11.05 % Detected minimum model sizes of [3] % 76.68/11.05 % Detected maximum model sizes of [max] % 76.68/11.05 % TRYING [20] % 76.68/11.05 % (2474389)Instruction limit reached! % 76.68/11.05 % (2474389)------------------------------ % 76.68/11.05 % (2474389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.68/11.05 % (2474389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.68/11.05 % (2474389)CaDiCaL version: 2.1.3 % 76.68/11.05 % (2474389)Termination reason: Instruction limit % 76.68/11.05 % (2474389)Termination phase: Saturation % 76.68/11.05 % (2474389)Time elapsed: 0.688 s % 76.68/11.05 % (2474389)Peak memory usage: 26 MB % 76.68/11.05 % (2474389)Instructions burned: 1180 (million) % 76.68/11.05 % (2474395)Instruction limit reached! % 76.68/11.05 % (2474395)------------------------------ % 76.68/11.05 % (2474395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.68/11.05 % (2474395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.68/11.05 % (2474395)CaDiCaL version: 2.1.3 % 76.68/11.05 % (2474395)Termination reason: Instruction limit % 76.68/11.05 % (2474395)Termination phase: Saturation % 76.68/11.05 % (2474395)Time elapsed: 0.451 s % 76.68/11.05 % (2474395)Peak memory usage: 21 MB % 76.68/11.05 % (2474395)Instructions burned: 881 (million) % 76.68/11.05 % (2474401)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3048003421:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 76.68/11.05 % (2474402)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3722726409:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 76.68/11.05 % Detected minimum model sizes of [3] % 76.68/11.05 % Detected maximum model sizes of [max] % 76.68/11.05 % TRYING [8] % 76.68/11.05 % TRYING [4] % 76.68/11.05 % (2474401)Instruction limit reached! % 76.68/11.05 % (2474401)------------------------------ % 76.68/11.05 % (2474401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.68/11.05 % (2474401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.68/11.05 % (2474401)CaDiCaL version: 2.1.3 % 76.68/11.05 % (2474401)Termination reason: Instruction limit % 76.68/11.05 % (2474401)Termination phase: Finite model building constraint generation % 76.68/11.05 % (2474401)Time elapsed: 0.310 s % 76.68/11.05 % (2474401)Peak memory usage: 55 MB % 76.68/11.05 % (2474401)Instructions burned: 922 (million) % 76.68/11.05 % (2474405)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2432922700:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi) % 76.68/11.05 % TRYING [6] % 76.68/11.05 % TRYING [5] % 76.68/11.05 % (2474405)Instruction limit reached! % 76.68/11.05 % (2474405)------------------------------ % 76.68/11.05 % (2474405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.68/11.05 % (2474405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.68/11.05 % (2474405)CaDiCaL version: 2.1.3 % 76.68/11.05 % (2474405)Termination reason: Instruction limit % 212.18/30.19 % (2474405)Termination phase: Saturation % 212.18/30.19 % (2474405)Time elapsed: 0.871 s % 212.18/30.19 % (2474405)Peak memory usage: 36 MB % 212.18/30.19 % (2474405)Instructions burned: 1473 (million) % 212.18/30.19 % (2474407)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1845467814:i=6324_2976 on theBenchmark for (2976ds/6324Mi) % 212.18/30.19 % Detected minimum model sizes of [3] % 212.18/30.19 % Detected maximum model sizes of [max] % 212.18/30.19 % (2474407)Cannot represent all propositional literals internally % 212.18/30.19 % (2474407)Refutation not found, incomplete strategy % 212.18/30.19 % (2474407)------------------------------ % 212.18/30.19 % (2474407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.18/30.19 % (2474407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.18/30.19 % (2474407)CaDiCaL version: 2.1.3 % 212.18/30.19 % (2474407)Termination reason: Refutation not found, incomplete strategy % 212.18/30.19 % (2474407)Time elapsed: 0.053 s % 212.18/30.19 % (2474407)Peak memory usage: 13 MB % 212.18/30.19 % (2474407)Instructions burned: 112 (million) % 212.18/30.19 % (2474407)------------------------------ % 212.18/30.19 % (2474407)------------------------------ % 212.18/30.19 % (2474409)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2086309676:fmbsr=2.30978:i=2174_2975 on theBenchmark for (2975ds/2174Mi) % 212.18/30.19 % Detected minimum model sizes of [3] % 212.18/30.19 % Detected maximum model sizes of [max] % 212.18/30.19 % TRYING [16] % 212.18/30.19 % (2474409)Instruction limit reached! % 212.18/30.19 % (2474409)------------------------------ % 212.18/30.19 % (2474409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.18/30.19 % (2474409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.18/30.19 % (2474409)CaDiCaL version: 2.1.3 % 212.18/30.19 % (2474409)Termination reason: Instruction limit % 212.18/30.19 % (2474409)Termination phase: Finite model building constraint generation % 212.18/30.19 % (2474409)Time elapsed: 0.821 s % 212.18/30.19 % (2474409)Peak memory usage: 103 MB % 212.18/30.19 % (2474409)Instructions burned: 2177 (million) % 212.18/30.19 % (2474411)ott-2_1_sil=16000:newcnf=on:random_seed=3428457411:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2967 on theBenchmark for (2967ds/869Mi) % 212.18/30.19 % (2474411)Instruction limit reached! % 212.18/30.19 % (2474411)------------------------------ % 212.18/30.19 % (2474411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.18/30.19 % (2474411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.18/30.19 % (2474411)CaDiCaL version: 2.1.3 % 212.18/30.19 % (2474411)Termination reason: Instruction limit % 212.18/30.19 % (2474411)Termination phase: Saturation % 212.18/30.19 % (2474411)Time elapsed: 0.368 s % 212.18/30.19 % (2474411)Peak memory usage: 16 MB % 212.18/30.19 % (2474411)Instructions burned: 870 (million) % 212.18/30.19 % (2474413)ott+10_1_sil=32000:tgt=ground:random_seed=2474794481:i=5114:av=off_2963 on theBenchmark for (2963ds/5114Mi) % 212.18/30.19 % (2474402)Instruction limit reached! % 212.18/30.19 % (2474402)------------------------------ % 212.18/30.19 % (2474402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.18/30.19 % (2474402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.18/30.19 % (2474402)CaDiCaL version: 2.1.3 % 212.18/30.19 % (2474402)Termination reason: Instruction limit % 212.18/30.19 % (2474402)Termination phase: Saturation % 212.18/30.19 % (2474402)Time elapsed: 2.685 s % 212.18/30.19 % (2474402)Peak memory usage: 41 MB % 212.18/30.19 % (2474402)Instructions burned: 5131 (million) % 212.18/30.19 % (2474415)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3550351012:i=54282_2961 on theBenchmark for (2961ds/54282Mi) % 212.18/30.19 % Detected minimum model sizes of [3] % 212.18/30.19 % Detected maximum model sizes of [max] % 212.18/30.19 % TRYING [3] % 212.18/30.19 % TRYING [4] % 212.18/30.19 % TRYING [7] % 212.18/30.19 % (2474398)Instruction limit reached! % 212.18/30.19 % (2474398)------------------------------ % 212.18/30.19 % (2474398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.18/30.19 % (2474398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.18/30.19 % (2474398)CaDiCaL version: 2.1.3 % 212.18/30.19 % (2474398)Termination reason: Instruction limit % 212.18/30.19 % (2474398)Termination phase: Finite model building constraint generation % 212.18/30.19 % (2474398)Time elapsed: 3.401 s % 212.18/30.19 % (2474398)Peak memory usage: 647 MB % 212.18/30.19 % (2474398)Instructions burned: 9518 (million) % 212.18/30.19 % TRYING [5] % 212.18/30.19 % (2474417)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3455100250:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi) % 212.18/30.19 % TRYING [6] % 295.62/41.94 % TRYING [6] % 295.62/41.94 % (2474417)Instruction limit reached! % 295.62/41.94 % (2474417)------------------------------ % 295.62/41.94 % (2474417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.62/41.94 % (2474417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.62/41.94 % (2474417)CaDiCaL version: 2.1.3 % 295.62/41.94 % (2474417)Termination reason: Instruction limit % 295.62/41.94 % (2474417)Termination phase: Saturation % 295.62/41.94 % (2474417)Time elapsed: 2.081 s % 295.62/41.94 % (2474417)Peak memory usage: 35 MB % 295.62/41.94 % (2474417)Instructions burned: 3514 (million) % 295.62/41.94 % (2474419)dis+21_1_sil=32000:sas=cadical:random_seed=1952622130:i=3773:amm=off_2934 on theBenchmark for (2934ds/3773Mi) % 295.62/41.94 % (2474413)Instruction limit reached! % 295.62/41.94 % (2474413)------------------------------ % 295.62/41.94 % (2474413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.62/41.94 % (2474413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.62/41.94 % (2474413)CaDiCaL version: 2.1.3 % 295.62/41.94 % (2474413)Termination reason: Instruction limit % 295.62/41.94 % (2474413)Termination phase: Saturation % 295.62/41.94 % (2474413)Time elapsed: 3.037 s % 295.62/41.94 % (2474413)Peak memory usage: 52 MB % 295.62/41.94 % (2474413)Instructions burned: 5115 (million) % 295.62/41.94 % (2474421)ott+11_1_sil=16000:gs=on:random_seed=2666958796:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2932 on theBenchmark for (2932ds/2251Mi) % 295.62/41.94 % TRYING [7] % 295.62/41.94 % (2474421)Instruction limit reached! % 295.62/41.94 % (2474421)------------------------------ % 295.62/41.94 % (2474421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.62/41.94 % (2474421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.62/41.94 % (2474421)CaDiCaL version: 2.1.3 % 295.62/41.94 % (2474421)Termination reason: Instruction limit % 295.62/41.94 % (2474421)Termination phase: Saturation % 295.62/41.94 % (2474421)Time elapsed: 1.217 s % 295.62/41.94 % (2474421)Peak memory usage: 19 MB % 295.62/41.94 % (2474421)Instructions burned: 2253 (million) % 295.62/41.94 % (2474423)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1240385412:fmbsr=1.6:i=67534_2920 on theBenchmark for (2920ds/67534Mi) % 295.62/41.94 % Detected minimum model sizes of [3] % 295.62/41.94 % Detected maximum model sizes of [max] % 295.62/41.94 % TRYING [7] % 295.62/41.94 % (2474419)Instruction limit reached! % 295.62/41.94 % (2474419)------------------------------ % 295.62/41.94 % (2474419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.62/41.94 % (2474419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.62/41.94 % (2474419)CaDiCaL version: 2.1.3 % 295.62/41.94 % (2474419)Termination reason: Instruction limit % 295.62/41.94 % (2474419)Termination phase: Saturation % 295.62/41.94 % (2474419)Time elapsed: 2.146 s % 295.62/41.94 % (2474419)Peak memory usage: 44 MB % 295.62/41.94 % (2474419)Instructions burned: 3773 (million) % 295.62/41.94 % (2474425)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=592386736:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2912 on theBenchmark for (2912ds/4591Mi) % 295.62/41.94 % TRYING [8] % 295.62/41.94 % (2474397)Instruction limit reached! % 295.62/41.94 % (2474397)------------------------------ % 295.62/41.94 % (2474397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.62/41.94 % (2474397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.62/41.94 % (2474397)CaDiCaL version: 2.1.3 % 295.62/41.94 % (2474397)Termination reason: Instruction limit % 295.62/41.94 % (2474397)Termination phase: Finite model building SAT solving % 295.62/41.94 % (2474397)Time elapsed: 9.156 s % 295.62/41.94 % (2474397)Peak memory usage: 253 MB % 295.62/41.94 % (2474397)Instructions burned: 22064 (million) % 295.62/41.94 % (2474427)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2684301634:i=29340_2898 on theBenchmark for (2898ds/29340Mi) % 295.62/41.94 % (2474425)Instruction limit reached! % 295.62/41.94 % (2474425)------------------------------ % 295.62/41.94 % (2474425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.62/41.94 % (2474425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.62/41.94 % (2474425)CaDiCaL version: 2.1.3 % 295.62/41.94 % (2474425)Termination reason: Instruction limit % 295.62/41.94 % (2474425)Termination phase: Saturation % 295.62/41.94 % (2474425)Time elapsed: 2.038 s % 295.62/41.94 % (2474425)Peak memory usage: 46 MB % 295.62/41.94 % (2474425)Instructions burned: 4594 (million) % 295.62/41.94 % (2474429)dis-10_1_sil=6400Terminated % 300.30/42.73 % Vampire exiting %------------------------------------------------------------------------------