%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX051+1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n004.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:24 PM UTC 2026 % Result : Timeout 300.19s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX051+1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.17 % Computer : n004.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 14:54:37 UTC 2026 % 0.08/0.17 % CPUTime : % 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/0.21 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 % 18.20/2.85 % (435687)Will run a generic schedule for satisfiability detection. % 18.20/2.85 % (435707)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2187771038:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 18.20/2.85 % (435706)% WARNING: option uhcvi not known. % 18.20/2.85 % (435708)dis+10_1_sil=32000:sp=arity:random_seed=3028895891:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 18.20/2.85 % (435706)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3831740670:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 18.20/2.85 % (435710)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3507971023:i=116_2999 on theBenchmark for (2999ds/116Mi) % 18.20/2.85 % (435711)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2210901018:i=131_2999 on theBenchmark for (2999ds/131Mi) % 18.20/2.85 % (435712)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4234631688:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 18.20/2.85 % (435705)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=950185278_2999 on theBenchmark for (2999ds/0Mi) % 18.20/2.85 % TRYING [1] % 18.20/2.85 % TRYING [2] % 18.20/2.85 % TRYING [3] % 18.20/2.85 % (435708)Instruction limit reached! % 18.20/2.85 % (435708)------------------------------ % 18.20/2.85 % (435708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.20/2.85 % (435708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.20/2.85 % (435708)CaDiCaL version: 2.1.3 % 18.20/2.85 % (435708)Termination reason: Instruction limit % 18.20/2.85 % (435708)Termination phase: Saturation % 18.20/2.85 % (435708)Time elapsed: 0.067 s % 18.20/2.85 % (435708)Peak memory usage: 13 MB % 18.20/2.85 % (435708)Instructions burned: 103 (million) % 18.20/2.85 % (435710)Instruction limit reached! % 18.20/2.85 % (435710)------------------------------ % 18.20/2.85 % (435710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.20/2.85 % (435710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.20/2.85 % (435710)CaDiCaL version: 2.1.3 % 18.20/2.85 % (435710)Termination reason: Instruction limit % 18.20/2.85 % (435710)Termination phase: Saturation % 18.20/2.85 % (435710)Time elapsed: 0.071 s % 18.20/2.85 % (435710)Peak memory usage: 14 MB % 18.20/2.85 % (435710)Instructions burned: 117 (million) % 18.20/2.85 % (435711)Instruction limit reached! % 18.20/2.85 % (435711)------------------------------ % 18.20/2.85 % (435711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.20/2.85 % (435711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.20/2.85 % (435711)CaDiCaL version: 2.1.3 % 18.20/2.85 % (435711)Termination reason: Instruction limit % 18.20/2.85 % (435711)Termination phase: Saturation % 18.20/2.85 % (435711)Time elapsed: 0.085 s % 18.20/2.85 % (435711)Peak memory usage: 13 MB % 18.20/2.85 % (435711)Instructions burned: 131 (million) % 18.20/2.85 % (435755)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=964468909:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 18.20/2.85 % (435756)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=215283049:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 18.20/2.85 % (435712)Instruction limit reached! % 18.20/2.85 % (435712)------------------------------ % 18.20/2.85 % (435712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.20/2.86 % (435712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.20/2.86 % (435712)CaDiCaL version: 2.1.3 % 18.20/2.86 % (435712)Termination reason: Instruction limit % 18.20/2.86 % (435712)Termination phase: Saturation % 18.20/2.86 % (435712)Time elapsed: 0.102 s % 18.20/2.86 % (435712)Peak memory usage: 14 MB % 18.20/2.86 % (435712)Instructions burned: 161 (million) % 18.20/2.86 % (435761)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=1861867671:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 18.20/2.86 % (435767)ott-21_1_sil=16000:fs=off:random_seed=2201958978:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 18.20/2.86 % TRYING [1] % 18.20/2.86 % TRYING [2] % 18.20/2.86 % TRYING [4] % 18.20/2.86 % TRYING [3] % 18.20/2.86 % (435767)Instruction limit reached! % 18.20/2.86 % (435767)------------------------------ % 18.20/2.86 % (435767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.20/2.86 % (435767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.41/7.27 % (435767)CaDiCaL version: 2.1.3 % 49.41/7.27 % (435767)Termination reason: Instruction limit % 49.41/7.27 % (435767)Termination phase: Saturation % 49.41/7.27 % (435767)Time elapsed: 0.047 s % 49.41/7.27 % (435767)Peak memory usage: 13 MB % 49.41/7.27 % (435767)Instructions burned: 181 (million) % 49.41/7.27 % (435780)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=519297429:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 49.41/7.27 % (435756)Instruction limit reached! % 49.41/7.27 % (435756)------------------------------ % 49.41/7.27 % (435756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 49.41/7.27 % (435756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.41/7.27 % (435756)CaDiCaL version: 2.1.3 % 49.41/7.27 % (435756)Termination reason: Instruction limit % 49.41/7.27 % (435756)Termination phase: Saturation % 49.41/7.27 % (435756)Time elapsed: 0.075 s % 49.41/7.27 % (435756)Peak memory usage: 13 MB % 49.41/7.27 % (435756)Instructions burned: 132 (million) % 49.41/7.27 % (435782)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3001879385:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 49.41/7.27 % TRYING [4] % 49.41/7.27 % TRYING [1] % 49.41/7.27 % TRYING [2] % 49.41/7.27 % TRYING [3] % 49.41/7.27 % (435780)Instruction limit reached! % 49.41/7.27 % (435780)------------------------------ % 49.41/7.27 % (435780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 49.41/7.27 % (435780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.41/7.27 % (435780)CaDiCaL version: 2.1.3 % 49.41/7.27 % (435780)Termination reason: Instruction limit % 49.41/7.27 % (435780)Termination phase: Saturation % 49.41/7.27 % (435780)Time elapsed: 0.181 s % 49.41/7.27 % (435780)Peak memory usage: 15 MB % 49.41/7.27 % (435780)Instructions burned: 479 (million) % 49.41/7.27 % TRYING [5] % 49.41/7.27 % (435824)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3809473191:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 49.41/7.27 % (435755)Instruction limit reached! % 49.41/7.27 % (435755)------------------------------ % 49.41/7.27 % (435755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 49.41/7.27 % (435755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.41/7.27 % (435755)CaDiCaL version: 2.1.3 % 49.41/7.27 % (435755)Termination reason: Instruction limit % 49.41/7.27 % (435755)Termination phase: Finite model building constraint generation % 49.41/7.27 % (435755)Time elapsed: 0.315 s % 49.41/7.27 % (435755)Peak memory usage: 41 MB % 49.41/7.27 % (435755)Instructions burned: 716 (million) % 49.41/7.27 % (435833)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3045474741:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 49.41/7.27 % TRYING [4] % 49.41/7.27 % (435761)Instruction limit reached! % 49.41/7.27 % (435761)------------------------------ % 49.41/7.27 % (435761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 49.41/7.27 % (435761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.41/7.27 % (435761)CaDiCaL version: 2.1.3 % 49.41/7.27 % (435761)Termination reason: Instruction limit % 49.41/7.27 % (435761)Termination phase: Saturation % 49.41/7.27 % (435761)Time elapsed: 0.455 s % 49.41/7.27 % (435761)Peak memory usage: 19 MB % 49.41/7.27 % (435761)Instructions burned: 686 (million) % 49.41/7.27 % (435782)Instruction limit reached! % 49.41/7.27 % (435782)------------------------------ % 49.41/7.27 % (435782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 49.41/7.27 % (435782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.41/7.27 % (435782)CaDiCaL version: 2.1.3 % 49.41/7.27 % (435782)Termination reason: Instruction limit % 49.41/7.27 % (435782)Termination phase: Finite model building constraint generation % 49.41/7.27 % (435782)Time elapsed: 0.369 s % 49.41/7.27 % (435782)Peak memory usage: 32 MB % 49.41/7.27 % (435782)Instructions burned: 867 (million) % 49.41/7.27 % (435835)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=1127627349:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi) % 49.41/7.27 % (435836)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1635090012:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 49.41/7.27 % (435824)Instruction limit reached! % 49.41/7.27 % (435824)------------------------------ % 49.41/7.27 % (435824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 49.41/7.27 % (435824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.90/11.58 % (435824)CaDiCaL version: 2.1.3 % 79.90/11.58 % (435824)Termination reason: Instruction limit % 79.90/11.58 % (435824)Termination phase: Saturation % 79.90/11.58 % (435824)Time elapsed: 0.444 s % 79.90/11.58 % (435824)Peak memory usage: 27 MB % 79.90/11.58 % (435824)Instructions burned: 1180 (million) % 79.90/11.58 % (435839)fmb+10_1_sil=64000:random_seed=2632580216:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi) % 79.90/11.58 % TRYING [1] % 79.90/11.58 % TRYING [2] % 79.90/11.58 % (435833)Instruction limit reached! % 79.90/11.58 % (435833)------------------------------ % 79.90/11.58 % (435833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.90/11.58 % (435833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.90/11.58 % (435833)CaDiCaL version: 2.1.3 % 79.90/11.58 % (435833)Termination reason: Instruction limit % 79.90/11.58 % (435833)Termination phase: Finite model building constraint generation % 79.90/11.58 % (435833)Time elapsed: 0.437 s % 79.90/11.58 % (435833)Peak memory usage: 102 MB % 79.90/11.58 % (435833)Instructions burned: 891 (million) % 79.90/11.58 % TRYING [3] % 79.90/11.58 % (435841)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1945990399:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 79.90/11.58 % TRYING [20] % 79.90/11.58 % TRYING [4] % 79.90/11.58 % (435835)Instruction limit reached! % 79.90/11.58 % (435835)------------------------------ % 79.90/11.58 % (435835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.90/11.58 % (435835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.90/11.58 % (435835)CaDiCaL version: 2.1.3 % 79.90/11.58 % (435835)Termination reason: Instruction limit % 79.90/11.58 % (435835)Termination phase: Saturation % 79.90/11.58 % (435835)Time elapsed: 0.446 s % 79.90/11.58 % (435835)Peak memory usage: 21 MB % 79.90/11.58 % (435835)Instructions burned: 692 (million) % 79.90/11.58 % (435836)Instruction limit reached! % 79.90/11.58 % (435836)------------------------------ % 79.90/11.58 % (435836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.90/11.58 % (435836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.90/11.58 % (435836)CaDiCaL version: 2.1.3 % 79.90/11.58 % (435836)Termination reason: Instruction limit % 79.90/11.58 % (435836)Termination phase: Saturation % 79.90/11.58 % (435836)Time elapsed: 0.483 s % 79.90/11.58 % (435836)Peak memory usage: 19 MB % 79.90/11.58 % (435836)Instructions burned: 879 (million) % 79.90/11.58 % TRYING [6] % 79.90/11.58 % (435851)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2684936550:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 79.90/11.58 % TRYING [8] % 79.90/11.58 % (435852)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=542699834:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 79.90/11.58 % (435851)Instruction limit reached! % 79.90/11.58 % (435851)------------------------------ % 79.90/11.58 % (435851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.90/11.58 % (435851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.90/11.58 % (435851)CaDiCaL version: 2.1.3 % 79.90/11.58 % (435851)Termination reason: Instruction limit % 79.90/11.58 % (435851)Termination phase: Finite model building constraint generation % 79.90/11.58 % (435851)Time elapsed: 0.600 s % 79.90/11.58 % (435851)Peak memory usage: 66 MB % 79.90/11.58 % (435851)Instructions burned: 921 (million) % 79.90/11.58 % TRYING [5] % 79.90/11.58 % (435871)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2171497432:i=1472:ins=7:fdi=8:gsp=on_2982 on theBenchmark for (2982ds/1472Mi) % 79.90/11.58 % (435871)Instruction limit reached! % 79.90/11.58 % (435871)------------------------------ % 79.90/11.58 % (435871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 79.90/11.58 % (435871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.90/11.58 % (435871)CaDiCaL version: 2.1.3 % 79.90/11.58 % (435871)Termination reason: Instruction limit % 79.90/11.58 % (435871)Termination phase: Saturation % 79.90/11.58 % (435871)Time elapsed: 0.798 s % 79.90/11.58 % (435871)Peak memory usage: 26 MB % 79.90/11.58 % (435871)Instructions burned: 1473 (million) % 79.90/11.58 % (435922)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1700334206:i=6324_2974 on theBenchmark for (2974ds/6324Mi) % 79.90/11.58 % (435922)Cannot represent all propositional literals internally % 79.90/11.58 % (435922)Refutation not found, incomplete strategy % 79.90/11.58 % (435922)------------------------------ % 79.90/11.58 % (435922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.57/38.76 % (435922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.57/38.76 % (435922)CaDiCaL version: 2.1.3 % 272.57/38.76 % (435922)Termination reason: Refutation not found, incomplete strategy % 272.57/38.76 % (435922)Time elapsed: 0.030 s % 272.57/38.76 % (435922)Peak memory usage: 12 MB % 272.57/38.76 % (435922)Instructions burned: 60 (million) % 272.57/38.76 % (435922)------------------------------ % 272.57/38.76 % (435922)------------------------------ % 272.57/38.76 % (435947)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2711620799:fmbsr=2.30978:i=2174_2973 on theBenchmark for (2973ds/2174Mi) % 272.57/38.76 % TRYING [16] % 272.57/38.76 % TRYING [7] % 272.57/38.76 % TRYING [6] % 272.57/38.76 % (435947)Instruction limit reached! % 272.57/38.76 % (435947)------------------------------ % 272.57/38.76 % (435947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.57/38.76 % (435947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.57/38.76 % (435947)CaDiCaL version: 2.1.3 % 272.57/38.76 % (435947)Termination reason: Instruction limit % 272.57/38.76 % (435947)Termination phase: Finite model building constraint generation % 272.57/38.77 % (435947)Time elapsed: 0.790 s % 272.57/38.77 % (435947)Peak memory usage: 126 MB % 272.57/38.77 % (435947)Instructions burned: 2176 (million) % 272.57/38.77 % (436034)ott-2_1_sil=16000:newcnf=on:random_seed=4137150145:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2965 on theBenchmark for (2965ds/869Mi) % 272.57/38.77 % (436034)Instruction limit reached! % 272.57/38.77 % (436034)------------------------------ % 272.57/38.77 % (436034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.57/38.77 % (436034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.57/38.77 % (436034)CaDiCaL version: 2.1.3 % 272.57/38.77 % (436034)Termination reason: Instruction limit % 272.57/38.77 % (436034)Termination phase: Saturation % 272.57/38.77 % (436034)Time elapsed: 0.562 s % 272.57/38.77 % (436034)Peak memory usage: 22 MB % 272.57/38.77 % (436034)Instructions burned: 869 (million) % 272.57/38.77 % (436036)ott+10_1_sil=32000:tgt=ground:random_seed=1978253578:i=5114:av=off_2959 on theBenchmark for (2959ds/5114Mi) % 272.57/38.77 % (435852)Instruction limit reached! % 272.57/38.77 % (435852)------------------------------ % 272.57/38.77 % (435852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.57/38.77 % (435852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.57/38.77 % (435852)CaDiCaL version: 2.1.3 % 272.57/38.77 % (435852)Termination reason: Instruction limit % 272.57/38.77 % (435852)Termination phase: Saturation % 272.57/38.77 % (435852)Time elapsed: 3.201 s % 272.57/38.77 % (435852)Peak memory usage: 42 MB % 272.57/38.77 % (435852)Instructions burned: 5133 (million) % 272.57/38.77 % (436038)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1345876520:i=54282_2956 on theBenchmark for (2956ds/54282Mi) % 272.57/38.77 % TRYING [1] % 272.57/38.77 % TRYING [2] % 272.57/38.77 % TRYING [3] % 272.57/38.77 % TRYING [4] % 272.57/38.77 % TRYING [5] % 272.57/38.77 % (435841)Instruction limit reached! % 272.57/38.77 % (435841)------------------------------ % 272.57/38.77 % (435841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.57/38.77 % (435841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.57/38.77 % (435841)CaDiCaL version: 2.1.3 % 272.57/38.77 % (435841)Termination reason: Instruction limit % 272.57/38.77 % (435841)Termination phase: Finite model building constraint generation % 272.57/38.77 % (435841)Time elapsed: 3.938 s % 272.57/38.77 % (435841)Peak memory usage: 599 MB % 272.57/38.77 % (435841)Instructions burned: 9516 (million) % 272.57/38.77 % (436040)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1817783962:i=3512:aac=none_2950 on theBenchmark for (2950ds/3512Mi) % 272.57/38.77 % TRYING [6] % 272.57/38.77 % TRYING [8] % 272.57/38.77 % TRYING [7] % 272.57/38.77 % (435839)Instruction limit reached! % 272.57/38.77 % (435839)------------------------------ % 272.57/38.77 % (435839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.57/38.77 % (435839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.57/38.77 % (435839)CaDiCaL version: 2.1.3 % 272.57/38.77 % (435839)Termination reason: Instruction limit % 272.57/38.77 % (435839)Termination phase: Finite model building constraint generation % 272.57/38.77 % (435839)Time elapsed: 5.874 s % 272.57/38.77 % (435839)Peak memory usage: 208 MB % 272.57/38.77 % (435839)Instructions burned: 22069 (million) % 272.57/38.77 % (436042)dis+21_1_sil=32000:sas=cadical:random_seed=857312016:i=3773:amm=off_2932 on theBenchmark for (2932ds/3773Mi) % 272.57/38.77 % TRYING [7] % 272.57/38.77 % (436040)Instruction limit reached! % 272.57/38.77 % (436040)---------------------------Terminated % 300.19/42.54 % Vampire exiting %------------------------------------------------------------------------------