%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM277-2 : TPTP v9.3.1. Bugfixed v2.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n006.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 12:18:11 PM UTC 2026 % Result : Timeout 300.07s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM277-2 : TPTP v9.3.1. Bugfixed v2.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.37 % Computer : n006.cluster.edu % 0.09/0.37 % Model : x86_64 x86_64 % 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.37 % Memory : 8046.5625MB % 0.09/0.37 % OS : Linux 6.8.0-71-generic % 0.09/0.37 % CPULimit : 300 % 0.09/0.37 % WCLimit : 300 % 0.09/0.37 % DateTime : Sun Sep 27 19:26:10 UTC 2026 % 0.09/0.38 % CPUTime : % 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.41 Running first-order model finding % 0.09/0.41 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 % 15.31/2.69 % (3265359)Will run a generic schedule for satisfiability detection. % 15.31/2.69 % (3265370)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3143791356:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 15.31/2.69 % (3265365)% WARNING: option uhcvi not known. % 15.31/2.69 % (3265368)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1081529063:i=116_2999 on theBenchmark for (2999ds/116Mi) % 15.31/2.69 % (3265364)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=972854256_2999 on theBenchmark for (2999ds/0Mi) % 15.31/2.69 % (3265365)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=643988646:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 15.31/2.69 % (3265366)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1950411011:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 15.31/2.69 % (3265367)dis+10_1_sil=32000:sp=arity:random_seed=645666394:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 15.31/2.69 % (3265369)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2114421857:i=131_2999 on theBenchmark for (2999ds/131Mi) % 15.31/2.69 % (3265370)Instruction limit reached! % 15.31/2.69 % (3265370)------------------------------ % 15.31/2.69 % (3265370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.31/2.69 % (3265370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.31/2.69 % (3265370)CaDiCaL version: 2.1.3 % 15.31/2.69 % (3265370)Termination reason: Instruction limit % 15.31/2.69 % (3265370)Termination phase: Saturation % 15.31/2.69 % (3265370)Time elapsed: 0.060 s % 15.31/2.69 % (3265370)Peak memory usage: 13 MB % 15.31/2.69 % (3265370)Instructions burned: 160 (million) % 15.31/2.69 % (3265368)Instruction limit reached! % 15.31/2.69 % (3265368)------------------------------ % 15.31/2.69 % (3265368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.31/2.69 % (3265368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.31/2.69 % (3265368)CaDiCaL version: 2.1.3 % 15.31/2.69 % (3265368)Termination reason: Instruction limit % 15.31/2.69 % (3265368)Termination phase: Saturation % 15.31/2.69 % (3265368)Time elapsed: 0.068 s % 15.31/2.69 % (3265368)Peak memory usage: 13 MB % 15.31/2.69 % (3265368)Instructions burned: 117 (million) % 15.31/2.69 % (3265367)Instruction limit reached! % 15.31/2.69 % (3265367)------------------------------ % 15.31/2.69 % (3265367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.31/2.69 % (3265367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.31/2.69 % (3265367)CaDiCaL version: 2.1.3 % 15.31/2.69 % (3265367)Termination reason: Instruction limit % 15.31/2.69 % (3265367)Termination phase: Saturation % 15.31/2.69 % (3265367)Time elapsed: 0.071 s % 15.31/2.69 % (3265367)Peak memory usage: 13 MB % 15.31/2.69 % (3265367)Instructions burned: 104 (million) % 15.31/2.69 % (3265378)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=167549139:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 15.31/2.69 % (3265379)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1600382834:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 15.31/2.69 % (3265369)Instruction limit reached! % 15.31/2.69 % (3265369)------------------------------ % 15.31/2.69 % (3265369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.31/2.69 % (3265369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.31/2.69 % (3265369)CaDiCaL version: 2.1.3 % 15.31/2.69 % (3265369)Termination reason: Instruction limit % 15.31/2.69 % (3265369)Termination phase: Saturation % 15.31/2.69 % (3265369)Time elapsed: 0.088 s % 15.31/2.69 % (3265369)Peak memory usage: 13 MB % 15.31/2.69 % (3265369)Instructions burned: 134 (million) % 15.31/2.69 % (3265380)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=2460505911:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 15.31/2.69 % (3265383)ott-21_1_sil=16000:fs=off:random_seed=803481939:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 15.31/2.69 % (3265379)Instruction limit reached! % 15.31/2.69 % (3265379)------------------------------ % 15.31/2.69 % (3265379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.31/2.69 % (3265379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.31/2.69 % (3265379)CaDiCaL version: 2.1.3 % 39.78/6.09 % (3265379)Termination reason: Instruction limit % 39.78/6.09 % (3265379)Termination phase: Saturation % 39.78/6.09 % (3265379)Time elapsed: 0.088 s % 39.78/6.09 % (3265379)Peak memory usage: 12 MB % 39.78/6.09 % (3265379)Instructions burned: 132 (million) % 39.78/6.09 % (3265386)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3314479433:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 39.78/6.09 % TRYING [1] % 39.78/6.09 % TRYING [2] % 39.78/6.09 % TRYING [1] % 39.78/6.09 % (3265383)Instruction limit reached! % 39.78/6.09 % (3265383)------------------------------ % 39.78/6.09 % (3265383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.78/6.09 % (3265383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.78/6.09 % (3265383)CaDiCaL version: 2.1.3 % 39.78/6.09 % (3265383)Termination reason: Instruction limit % 39.78/6.09 % (3265383)Termination phase: Saturation % 39.78/6.09 % (3265383)Time elapsed: 0.103 s % 39.78/6.09 % (3265383)Peak memory usage: 12 MB % 39.78/6.09 % (3265383)Instructions burned: 181 (million) % 39.78/6.09 % TRYING [3] % 39.78/6.09 % TRYING [2] % 39.78/6.09 % (3265388)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=595941947:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 39.78/6.09 % TRYING [3] % 39.78/6.09 % (3265378)Instruction limit reached! % 39.78/6.09 % (3265378)------------------------------ % 39.78/6.09 % (3265378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.78/6.09 % (3265378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.78/6.09 % (3265378)CaDiCaL version: 2.1.3 % 39.78/6.09 % (3265378)Termination reason: Instruction limit % 39.78/6.09 % (3265378)Termination phase: Finite model building constraint generation % 39.78/6.09 % (3265378)Time elapsed: 0.186 s % 39.78/6.09 % (3265378)Peak memory usage: 31 MB % 39.78/6.09 % (3265378)Instructions burned: 715 (million) % 39.78/6.09 % (3265390)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3825861380:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 39.78/6.09 % TRYING [4] % 39.78/6.09 % TRYING [1] % 39.78/6.09 % TRYING [2] % 39.78/6.09 % (3265380)Instruction limit reached! % 39.78/6.09 % (3265380)------------------------------ % 39.78/6.09 % (3265380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.78/6.09 % (3265380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.78/6.09 % (3265380)CaDiCaL version: 2.1.3 % 39.78/6.09 % (3265380)Termination reason: Instruction limit % 39.78/6.09 % (3265380)Termination phase: Saturation % 39.78/6.09 % (3265380)Time elapsed: 0.434 s % 39.78/6.09 % (3265380)Peak memory usage: 18 MB % 39.78/6.09 % (3265380)Instructions burned: 685 (million) % 39.78/6.09 % (3265386)Instruction limit reached! % 39.78/6.09 % (3265386)------------------------------ % 39.78/6.09 % (3265386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.78/6.09 % (3265386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.78/6.09 % (3265386)CaDiCaL version: 2.1.3 % 39.78/6.09 % (3265386)Termination reason: Instruction limit % 39.78/6.09 % (3265386)Termination phase: Saturation % 39.78/6.09 % (3265386)Time elapsed: 0.343 s % 39.78/6.09 % (3265386)Peak memory usage: 14 MB % 39.78/6.09 % (3265386)Instructions burned: 477 (million) % 39.78/6.09 % (3265392)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4013360523:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 39.78/6.09 % (3265393)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=4278745993: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) % 39.78/6.09 % TRYING [3] % 39.78/6.09 % (3265388)Instruction limit reached! % 39.78/6.09 % (3265388)------------------------------ % 39.78/6.09 % (3265388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.78/6.09 % (3265388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.78/6.09 % (3265388)CaDiCaL version: 2.1.3 % 39.78/6.09 % (3265388)Termination reason: Instruction limit % 39.78/6.09 % (3265388)Termination phase: Finite model building constraint generation % 39.78/6.09 % (3265388)Time elapsed: 0.407 s % 39.78/6.09 % (3265388)Peak memory usage: 26 MB % 39.78/6.09 % (3265388)Instructions burned: 867 (million) % 39.78/6.09 % (3265396)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2605286670:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 39.78/6.09 % (3265390)Instruction limit reached! % 39.78/6.09 % (3265390)------------------------------ % 39.78/6.09 % (3265390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.07/12.70 % (3265390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.07/12.70 % (3265390)CaDiCaL version: 2.1.3 % 87.07/12.70 % (3265390)Termination reason: Instruction limit % 87.07/12.70 % (3265390)Termination phase: Saturation % 87.07/12.70 % (3265390)Time elapsed: 0.398 s % 87.07/12.70 % (3265390)Peak memory usage: 23 MB % 87.07/12.70 % (3265390)Instructions burned: 1181 (million) % 87.07/12.70 % (3265398)fmb+10_1_sil=64000:random_seed=3820368608:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 87.07/12.70 % TRYING [1] % 87.07/12.70 % TRYING [2] % 87.07/12.70 % TRYING [3] % 87.07/12.70 % (3265393)Instruction limit reached! % 87.07/12.70 % (3265393)------------------------------ % 87.07/12.70 % (3265393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.07/12.70 % (3265393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.07/12.70 % (3265393)CaDiCaL version: 2.1.3 % 87.07/12.70 % (3265393)Termination reason: Instruction limit % 87.07/12.70 % (3265393)Termination phase: Saturation % 87.07/12.70 % (3265393)Time elapsed: 0.412 s % 87.07/12.70 % (3265393)Peak memory usage: 18 MB % 87.07/12.70 % (3265393)Instructions burned: 693 (million) % 87.07/12.70 % (3265400)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1192292983:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 87.07/12.70 % (3265392)Instruction limit reached! % 87.07/12.70 % (3265392)------------------------------ % 87.07/12.70 % (3265392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.07/12.70 % (3265392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.07/12.70 % (3265392)CaDiCaL version: 2.1.3 % 87.07/12.70 % (3265392)Termination reason: Instruction limit % 87.07/12.70 % (3265392)Termination phase: Finite model building constraint generation % 87.07/12.70 % (3265392)Time elapsed: 0.448 s % 87.07/12.70 % (3265392)Peak memory usage: 75 MB % 87.07/12.70 % (3265392)Instructions burned: 889 (million) % 87.07/12.70 % (3265402)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2753564803:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 87.07/12.70 % (3265396)Instruction limit reached! % 87.07/12.70 % (3265396)------------------------------ % 87.07/12.70 % (3265396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.07/12.70 % (3265396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.07/12.70 % (3265396)CaDiCaL version: 2.1.3 % 87.07/12.70 % (3265396)Termination reason: Instruction limit % 87.07/12.70 % (3265396)Termination phase: Saturation % 87.07/12.70 % (3265396)Time elapsed: 0.486 s % 87.07/12.70 % (3265396)Peak memory usage: 19 MB % 87.07/12.70 % (3265396)Instructions burned: 880 (million) % 87.07/12.70 % (3265404)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1612663596:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 87.07/12.70 % TRYING [20] % 87.07/12.70 % TRYING [8] % 87.07/12.70 % TRYING [4] % 87.07/12.70 % TRYING [5] % 87.07/12.70 % (3265402)Instruction limit reached! % 87.07/12.70 % (3265402)------------------------------ % 87.07/12.70 % (3265402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.07/12.70 % (3265402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.07/12.70 % (3265402)CaDiCaL version: 2.1.3 % 87.07/12.70 % (3265402)Termination reason: Instruction limit % 87.07/12.70 % (3265402)Termination phase: Finite model building constraint generation % 87.07/12.70 % (3265402)Time elapsed: 0.387 s % 87.07/12.70 % (3265402)Peak memory usage: 46 MB % 87.07/12.70 % (3265402)Instructions burned: 922 (million) % 87.07/12.70 % (3265406)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1325144908:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi) % 87.07/12.70 % (3265406)Instruction limit reached! % 87.07/12.70 % (3265406)------------------------------ % 87.07/12.70 % (3265406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 87.07/12.70 % (3265406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.07/12.70 % (3265406)CaDiCaL version: 2.1.3 % 87.07/12.70 % (3265406)Termination reason: Instruction limit % 87.07/12.70 % (3265406)Termination phase: Saturation % 87.07/12.70 % (3265406)Time elapsed: 0.576 s % 87.07/12.70 % (3265406)Peak memory usage: 19 MB % 87.07/12.70 % (3265406)Instructions burned: 1472 (million) % 87.07/12.70 % (3265408)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3909255428:i=6324_2979 on theBenchmark for (2979ds/6324Mi) % 87.07/12.70 % (3265408)Cannot represent all propositional literals internally % 87.07/12.70 % (3265408)Refutation not found, incomplete strategy % 209.97/30.10 % (3265408)------------------------------ % 209.97/30.10 % (3265408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.97/30.10 % (3265408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.97/30.10 % (3265408)CaDiCaL version: 2.1.3 % 209.97/30.10 % (3265408)Termination reason: Refutation not found, incomplete strategy % 209.97/30.10 % (3265408)Time elapsed: 0.213 s % 209.97/30.10 % (3265408)Peak memory usage: 13 MB % 209.97/30.10 % (3265408)Instructions burned: 410 (million) % 209.97/30.10 % (3265408)------------------------------ % 209.97/30.10 % (3265408)------------------------------ % 209.97/30.10 % (3265410)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1043628363:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi) % 209.97/30.10 % TRYING [5] % 209.97/30.10 % (3265410)Cannot represent all propositional literals internally % 209.97/30.10 % (3265410)Refutation not found, incomplete strategy % 209.97/30.10 % (3265410)------------------------------ % 209.97/30.10 % (3265410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.97/30.10 % (3265410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.97/30.10 % (3265410)CaDiCaL version: 2.1.3 % 209.97/30.10 % (3265410)Termination reason: Refutation not found, incomplete strategy % 209.97/30.10 % (3265410)Time elapsed: 1.126 s % 209.97/30.10 % (3265410)Peak memory usage: 18 MB % 209.97/30.10 % (3265410)Instructions burned: 2072 (million) % 209.97/30.10 % (3265410)------------------------------ % 209.97/30.10 % (3265410)------------------------------ % 209.97/30.10 % (3265412)ott-2_1_sil=16000:newcnf=on:random_seed=1014347413:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2965 on theBenchmark for (2965ds/869Mi) % 209.97/30.10 % (3265412)Instruction limit reached! % 209.97/30.10 % (3265412)------------------------------ % 209.97/30.10 % (3265412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.97/30.10 % (3265412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.97/30.10 % (3265412)CaDiCaL version: 2.1.3 % 209.97/30.10 % (3265412)Termination reason: Instruction limit % 209.97/30.10 % (3265412)Termination phase: Saturation % 209.97/30.10 % (3265412)Time elapsed: 0.506 s % 209.97/30.10 % (3265412)Peak memory usage: 17 MB % 209.97/30.10 % (3265412)Instructions burned: 870 (million) % 209.97/30.10 % (3265414)ott+10_1_sil=32000:tgt=ground:random_seed=1840895585:i=5114:av=off_2960 on theBenchmark for (2960ds/5114Mi) % 209.97/30.10 % (3265404)Instruction limit reached! % 209.97/30.10 % (3265404)------------------------------ % 209.97/30.10 % (3265404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.97/30.10 % (3265404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.97/30.10 % (3265404)CaDiCaL version: 2.1.3 % 209.97/30.10 % (3265404)Termination reason: Instruction limit % 209.97/30.10 % (3265404)Termination phase: Saturation % 209.97/30.10 % (3265404)Time elapsed: 3.024 s % 209.97/30.10 % (3265404)Peak memory usage: 36 MB % 209.97/30.10 % (3265404)Instructions burned: 5131 (million) % 209.97/30.10 % (3265416)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2181268393:i=54282_2957 on theBenchmark for (2957ds/54282Mi) % 209.97/30.10 % (3265400)Instruction limit reached! % 209.97/30.10 % (3265400)------------------------------ % 209.97/30.10 % (3265400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.97/30.10 % (3265400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.97/30.10 % (3265400)CaDiCaL version: 2.1.3 % 209.97/30.10 % (3265400)Termination reason: Instruction limit % 209.97/30.10 % (3265400)Termination phase: Finite model building constraint generation % 209.97/30.10 % (3265400)Time elapsed: 3.354 s % 209.97/30.10 % (3265400)Peak memory usage: 550 MB % 209.97/30.10 % (3265400)Instructions burned: 9518 (million) % 209.97/30.10 % (3265418)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1009215847:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi) % 209.97/30.10 % TRYING [1] % 209.97/30.10 % TRYING [2] % 209.97/30.10 % TRYING [3] % 209.97/30.10 % TRYING [4] % 209.97/30.10 % TRYING [6] % 209.97/30.10 % TRYING [5] % 209.97/30.10 % (3265398)Instruction limit reached! % 209.97/30.10 % (3265398)------------------------------ % 209.97/30.10 % (3265398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.97/30.10 % (3265398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.97/30.10 % (3265398)CaDiCaL version: 2.1.3 % 209.97/30.10 % (3265398)Termination reason: Instruction limit % 209.97/30.10 % (3265398)Termination phase: Finite model building SAT solving % 209.97/30.10 % (3265398)Time elapsed: 4.962 s % 209.97/30.10 % (3265398)Peak memory usage: 436 MB % 209.97/30.10 % (3265398)Instructions burned: 22063 (million) % 284.87/40.69 % (3265420)dis+21_1_sil=32000:sas=cadical:random_seed=1256972160:i=3773:amm=off_2942 on theBenchmark for (2942ds/3773Mi) % 284.87/40.69 % (3265418)Instruction limit reached! % 284.87/40.69 % (3265418)------------------------------ % 284.87/40.69 % (3265418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.87/40.69 % (3265418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.87/40.69 % (3265418)CaDiCaL version: 2.1.3 % 284.87/40.69 % (3265418)Termination reason: Instruction limit % 284.87/40.69 % (3265418)Termination phase: Saturation % 284.87/40.69 % (3265418)Time elapsed: 1.997 s % 284.87/40.69 % (3265418)Peak memory usage: 36 MB % 284.87/40.69 % (3265418)Instructions burned: 3512 (million) % 284.87/40.69 % (3265422)ott+11_1_sil=16000:gs=on:random_seed=2072626868:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2935 on theBenchmark for (2935ds/2251Mi) % 284.87/40.69 % (3265420)Instruction limit reached! % 284.87/40.69 % (3265420)------------------------------ % 284.87/40.69 % (3265420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.87/40.69 % (3265420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.87/40.69 % (3265420)CaDiCaL version: 2.1.3 % 284.87/40.69 % (3265420)Termination reason: Instruction limit % 284.87/40.69 % (3265420)Termination phase: Saturation % 284.87/40.69 % (3265420)Time elapsed: 1.192 s % 284.87/40.69 % (3265420)Peak memory usage: 40 MB % 284.87/40.69 % (3265420)Instructions burned: 3775 (million) % 284.87/40.69 % (3265424)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2551042606:fmbsr=1.6:i=67534_2930 on theBenchmark for (2930ds/67534Mi) % 284.87/40.69 % (3265414)Instruction limit reached! % 284.87/40.69 % (3265414)------------------------------ % 284.87/40.69 % (3265414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.87/40.69 % (3265414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.87/40.69 % (3265414)CaDiCaL version: 2.1.3 % 284.87/40.69 % (3265414)Termination reason: Instruction limit % 284.87/40.69 % (3265414)Termination phase: Saturation % 284.87/40.69 % (3265414)Time elapsed: 3.218 s % 284.87/40.69 % (3265414)Peak memory usage: 49 MB % 284.87/40.69 % (3265414)Instructions burned: 5114 (million) % 284.87/40.69 % (3265426)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3709646238:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2927 on theBenchmark for (2927ds/4591Mi) % 284.87/40.69 % TRYING [7] % 284.87/40.69 % (3265422)Instruction limit reached! % 284.87/40.69 % (3265422)------------------------------ % 284.87/40.69 % (3265422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.87/40.69 % (3265422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.87/40.69 % (3265422)CaDiCaL version: 2.1.3 % 284.87/40.69 % (3265422)Termination reason: Instruction limit % 284.87/40.69 % (3265422)Termination phase: Saturation % 284.87/40.69 % (3265422)Time elapsed: 1.137 s % 284.87/40.69 % (3265422)Peak memory usage: 22 MB % 284.87/40.69 % (3265422)Instructions burned: 2252 (million) % 284.87/40.69 % (3265428)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1212847365:i=29340_2923 on theBenchmark for (2923ds/29340Mi) % 284.87/40.69 % TRYING [6] % 284.87/40.69 % (3265426)Instruction limit reached! % 284.87/40.69 % (3265426)------------------------------ % 284.87/40.69 % (3265426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.87/40.69 % (3265426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.87/40.69 % (3265426)CaDiCaL version: 2.1.3 % 284.87/40.69 % (3265426)Termination reason: Instruction limit % 284.87/40.69 % (3265426)Termination phase: Saturation % 284.87/40.69 % (3265426)Time elapsed: 2.607 s % 284.87/40.69 % (3265426)Peak memory usage: 48 MB % 284.87/40.69 % (3265426)Instructions burned: 4591 (million) % 284.87/40.69 % (3265430)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=457172386:i=5211_2901 on theBenchmark for (2901ds/5211Mi) % 284.87/40.69 % (3265430)Instruction limit reached! % 284.87/40.69 % (3265430)------------------------------ % 284.87/40.69 % (3265430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.87/40.69 % (3265430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.87/40.69 % (3265430)CaDiCaL version: 2.1.3 % 284.87/40.69 % (3265430)Termination reason: Instruction limit % 284.87/40.69 % (3265430)Termination phase: Saturation % 284.87/40.69 % (3265430)Time elapsed: 2.408 s % 284.87/40.69 % (3265430)Peak memory usage: 44 MB % 284.87/40.69 % (3265430)Instructions burned: 5213 (million) % 284.87/40.69 % (32654Terminated % 300.07/42.83 % Vampire exiting %------------------------------------------------------------------------------