%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV983-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 : n009.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:46 PM UTC 2026 % Result : Timeout 300.32s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV983-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n009.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 13:05:15 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 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 % 8.13/1.44 % (3012907)Will run a generic schedule for satisfiability detection. % 8.13/1.44 % (3012913)% WARNING: option uhcvi not known. % 8.13/1.44 % (3012913)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2935593363:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.13/1.44 % (3012912)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2943550024_2999 on theBenchmark for (2999ds/0Mi) % 8.13/1.44 % (3012916)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=710935223:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.13/1.44 % (3012914)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=365130021:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.13/1.44 % (3012915)dis+10_1_sil=32000:sp=arity:random_seed=3018373230:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.13/1.44 % (3012917)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1036641201:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.13/1.44 % (3012918)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2865767450:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.13/1.44 % TRYING [1] % 8.13/1.44 % (3012916)Instruction limit reached! % 8.13/1.44 % (3012916)------------------------------ % 8.13/1.44 % (3012916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.13/1.44 % (3012916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.13/1.44 % (3012916)CaDiCaL version: 2.1.3 % 8.13/1.44 % (3012916)Termination reason: Instruction limit % 8.13/1.44 % (3012916)Termination phase: Saturation % 8.13/1.44 % (3012916)Time elapsed: 0.065 s % 8.13/1.44 % (3012916)Peak memory usage: 13 MB % 8.13/1.44 % (3012916)Instructions burned: 117 (million) % 8.13/1.44 % TRYING [2] % 8.13/1.44 % (3012915)Instruction limit reached! % 8.13/1.44 % (3012915)------------------------------ % 8.13/1.44 % (3012915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.13/1.44 % (3012915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.13/1.44 % (3012915)CaDiCaL version: 2.1.3 % 8.13/1.44 % (3012915)Termination reason: Instruction limit % 8.13/1.44 % (3012915)Termination phase: Saturation % 8.13/1.44 % (3012915)Time elapsed: 0.068 s % 8.13/1.44 % (3012915)Peak memory usage: 12 MB % 8.13/1.44 % (3012915)Instructions burned: 104 (million) % 8.13/1.44 % (3012917)Instruction limit reached! % 8.13/1.44 % (3012917)------------------------------ % 8.13/1.44 % (3012917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.13/1.44 % (3012917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.13/1.44 % (3012917)CaDiCaL version: 2.1.3 % 8.13/1.44 % (3012917)Termination reason: Instruction limit % 8.13/1.44 % (3012917)Termination phase: Saturation % 8.13/1.44 % (3012917)Time elapsed: 0.080 s % 8.13/1.44 % (3012917)Peak memory usage: 13 MB % 8.13/1.44 % (3012917)Instructions burned: 132 (million) % 8.13/1.44 % (3012926)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2085111658:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 8.13/1.44 % (3012927)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4014199960:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 8.13/1.44 % (3012928)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=1519165126:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.13/1.44 % (3012918)Instruction limit reached! % 8.13/1.44 % (3012918)------------------------------ % 8.13/1.44 % (3012918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.13/1.44 % (3012918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.13/1.44 % (3012918)CaDiCaL version: 2.1.3 % 8.13/1.44 % (3012918)Termination reason: Instruction limit % 8.13/1.44 % (3012918)Termination phase: Saturation % 8.13/1.44 % (3012918)Time elapsed: 0.104 s % 8.13/1.44 % (3012918)Peak memory usage: 13 MB % 8.13/1.44 % (3012918)Instructions burned: 159 (million) % 8.13/1.44 % (3012932)ott-21_1_sil=16000:fs=off:random_seed=2223136117:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.13/1.44 % TRYING [1] % 8.13/1.44 % TRYING [2] % 8.13/1.44 % (3012927)Instruction limit reached! % 8.13/1.44 % (3012927)------------------------------ % 8.13/1.44 % (3012927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.13/1.44 % (3012927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.15/5.21 % (3012927)CaDiCaL version: 2.1.3 % 35.15/5.21 % (3012927)Termination reason: Instruction limit % 35.15/5.21 % (3012927)Termination phase: Saturation % 35.15/5.21 % (3012927)Time elapsed: 0.085 s % 35.15/5.21 % (3012927)Peak memory usage: 13 MB % 35.15/5.21 % (3012927)Instructions burned: 131 (million) % 35.15/5.21 % (3012934)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=19773722:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 35.15/5.21 % (3012932)Instruction limit reached! % 35.15/5.21 % (3012932)------------------------------ % 35.15/5.21 % (3012932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.15/5.21 % (3012932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.15/5.21 % (3012932)CaDiCaL version: 2.1.3 % 35.15/5.21 % (3012932)Termination reason: Instruction limit % 35.15/5.21 % (3012932)Termination phase: Saturation % 35.15/5.21 % (3012932)Time elapsed: 0.071 s % 35.15/5.21 % (3012932)Peak memory usage: 11 MB % 35.15/5.21 % (3012932)Instructions burned: 181 (million) % 35.15/5.21 % (3012936)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=933161500:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 35.15/5.21 % TRYING [1] % 35.15/5.21 % (3012926)Instruction limit reached! % 35.15/5.21 % (3012926)------------------------------ % 35.15/5.21 % (3012926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.15/5.21 % (3012926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.15/5.21 % (3012926)CaDiCaL version: 2.1.3 % 35.15/5.21 % (3012926)Termination reason: Instruction limit % 35.15/5.21 % (3012926)Termination phase: Finite model building constraint generation % 35.15/5.21 % (3012926)Time elapsed: 0.260 s % 35.15/5.21 % (3012926)Peak memory usage: 22 MB % 35.15/5.21 % (3012926)Instructions burned: 717 (million) % 35.15/5.21 % (3012938)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1547089102:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 35.15/5.21 % (3012928)Instruction limit reached! % 35.15/5.21 % (3012928)------------------------------ % 35.15/5.21 % (3012928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.15/5.21 % (3012928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.15/5.21 % (3012928)CaDiCaL version: 2.1.3 % 35.15/5.21 % (3012928)Termination reason: Instruction limit % 35.15/5.21 % (3012928)Termination phase: Saturation % 35.15/5.21 % (3012928)Time elapsed: 0.373 s % 35.15/5.21 % (3012928)Peak memory usage: 17 MB % 35.15/5.21 % (3012928)Instructions burned: 686 (million) % 35.15/5.21 % (3012940)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1064042630:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 35.15/5.21 % (3012934)Instruction limit reached! % 35.15/5.21 % (3012934)------------------------------ % 35.15/5.21 % (3012934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.15/5.21 % (3012934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.15/5.21 % (3012934)CaDiCaL version: 2.1.3 % 35.15/5.21 % (3012934)Termination reason: Instruction limit % 35.15/5.21 % (3012934)Termination phase: Saturation % 35.15/5.21 % (3012934)Time elapsed: 0.303 s % 35.15/5.21 % (3012934)Peak memory usage: 15 MB % 35.15/5.21 % (3012934)Instructions burned: 478 (million) % 35.15/5.21 % (3012942)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=1074941253: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) % 35.15/5.21 % (3012940)Cannot represent all propositional literals internally % 35.15/5.21 % (3012940)Refutation not found, incomplete strategy % 35.15/5.21 % (3012940)------------------------------ % 35.15/5.21 % (3012940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.15/5.21 % (3012940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.15/5.21 % (3012940)CaDiCaL version: 2.1.3 % 35.15/5.21 % (3012940)Termination reason: Refutation not found, incomplete strategy % 35.15/5.21 % (3012940)Time elapsed: 0.066 s % 35.15/5.21 % (3012940)Peak memory usage: 12 MB % 35.15/5.21 % (3012940)Instructions burned: 125 (million) % 35.15/5.21 % (3012940)------------------------------ % 35.15/5.21 % (3012940)------------------------------ % 35.15/5.21 % (3012944)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=808056940:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 35.15/5.21 % (3012936)Instruction limit reached! % 35.15/5.21 % (3012936)------------------------------ % 72.73/10.52 % (3012936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.73/10.52 % (3012936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.52 % (3012936)CaDiCaL version: 2.1.3 % 72.73/10.52 % (3012936)Termination reason: Instruction limit % 72.73/10.52 % (3012936)Termination phase: Finite model building constraint generation % 72.73/10.52 % (3012936)Time elapsed: 0.411 s % 72.73/10.52 % (3012936)Peak memory usage: 97 MB % 72.73/10.52 % (3012936)Instructions burned: 866 (million) % 72.73/10.52 % (3012946)fmb+10_1_sil=64000:random_seed=3659069022:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 72.73/10.52 % TRYING [1] % 72.73/10.52 % (3012942)Instruction limit reached! % 72.73/10.52 % (3012942)------------------------------ % 72.73/10.52 % (3012942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.73/10.52 % (3012942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.52 % (3012942)CaDiCaL version: 2.1.3 % 72.73/10.52 % (3012942)Termination reason: Instruction limit % 72.73/10.52 % (3012942)Termination phase: Saturation % 72.73/10.52 % (3012942)Time elapsed: 0.450 s % 72.73/10.52 % (3012942)Peak memory usage: 20 MB % 72.73/10.52 % (3012942)Instructions burned: 693 (million) % 72.73/10.52 % (3012948)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3731148896:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 72.73/10.52 % (3012944)Instruction limit reached! % 72.73/10.52 % (3012944)------------------------------ % 72.73/10.52 % (3012944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.73/10.52 % (3012944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.52 % (3012944)CaDiCaL version: 2.1.3 % 72.73/10.52 % (3012944)Termination reason: Instruction limit % 72.73/10.52 % (3012944)Termination phase: Saturation % 72.73/10.52 % (3012944)Time elapsed: 0.477 s % 72.73/10.52 % (3012944)Peak memory usage: 19 MB % 72.73/10.52 % (3012944)Instructions burned: 879 (million) % 72.73/10.52 % (3012948)Cannot represent all propositional literals internally % 72.73/10.52 % (3012948)Refutation not found, incomplete strategy % 72.73/10.52 % (3012948)------------------------------ % 72.73/10.52 % (3012948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.73/10.52 % (3012948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.52 % (3012948)CaDiCaL version: 2.1.3 % 72.73/10.52 % (3012948)Termination reason: Refutation not found, incomplete strategy % 72.73/10.52 % (3012948)Time elapsed: 0.080 s % 72.73/10.52 % (3012948)Peak memory usage: 12 MB % 72.73/10.52 % (3012948)Instructions burned: 125 (million) % 72.73/10.52 % (3012948)------------------------------ % 72.73/10.52 % (3012948)------------------------------ % 72.73/10.52 % (3012950)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2483797983:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi) % 72.73/10.52 % (3012951)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3565016679:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 72.73/10.52 % (3012938)Instruction limit reached! % 72.73/10.52 % (3012938)------------------------------ % 72.73/10.52 % (3012938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.73/10.52 % (3012938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.52 % (3012938)CaDiCaL version: 2.1.3 % 72.73/10.52 % (3012938)Termination reason: Instruction limit % 72.73/10.52 % (3012938)Termination phase: Saturation % 72.73/10.52 % (3012938)Time elapsed: 0.767 s % 72.73/10.52 % (3012938)Peak memory usage: 22 MB % 72.73/10.52 % (3012938)Instructions burned: 1179 (million) % 72.73/10.52 % (3012950)Cannot represent all propositional literals internally % 72.73/10.52 % (3012950)Refutation not found, incomplete strategy % 72.73/10.52 % (3012950)------------------------------ % 72.73/10.52 % (3012950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.73/10.52 % (3012950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.52 % (3012950)CaDiCaL version: 2.1.3 % 72.73/10.52 % (3012950)Termination reason: Refutation not found, incomplete strategy % 72.73/10.52 % (3012950)Time elapsed: 0.067 s % 72.73/10.52 % (3012950)Peak memory usage: 12 MB % 72.73/10.52 % (3012950)Instructions burned: 125 (million) % 72.73/10.52 % (3012950)------------------------------ % 72.73/10.52 % (3012950)------------------------------ % 72.73/10.52 % (3012954)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3326844937:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi) % 72.73/10.52 % (3012955)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3423666022:i=6324_2988 on theBenchmark for (2988ds/6324Mi) % 118.13/17.00 % (3012955)Cannot represent all propositional literals internally % 118.13/17.00 % (3012955)Refutation not found, incomplete strategy % 118.13/17.00 % (3012955)------------------------------ % 118.13/17.00 % (3012955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.13/17.00 % (3012955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.13/17.00 % (3012955)CaDiCaL version: 2.1.3 % 118.13/17.00 % (3012955)Termination reason: Refutation not found, incomplete strategy % 118.13/17.00 % (3012955)Time elapsed: 0.064 s % 118.13/17.00 % (3012955)Peak memory usage: 13 MB % 118.13/17.00 % (3012955)Instructions burned: 123 (million) % 118.13/17.00 % (3012955)------------------------------ % 118.13/17.00 % (3012955)------------------------------ % 118.13/17.00 % (3012958)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2402838978:fmbsr=2.30978:i=2174_2987 on theBenchmark for (2987ds/2174Mi) % 118.13/17.00 % (3012958)Cannot represent all propositional literals internally % 118.13/17.00 % (3012958)Refutation not found, incomplete strategy % 118.13/17.00 % (3012958)------------------------------ % 118.13/17.00 % (3012958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.13/17.00 % (3012958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.13/17.00 % (3012958)CaDiCaL version: 2.1.3 % 118.13/17.00 % (3012958)Termination reason: Refutation not found, incomplete strategy % 118.13/17.00 % (3012958)Time elapsed: 0.549 s % 118.13/17.00 % (3012958)Peak memory usage: 20 MB % 118.13/17.00 % (3012958)Instructions burned: 1006 (million) % 118.13/17.00 % (3012958)------------------------------ % 118.13/17.00 % (3012958)------------------------------ % 118.13/17.00 % (3012960)ott-2_1_sil=16000:newcnf=on:random_seed=438667061:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2981 on theBenchmark for (2981ds/869Mi) % 118.13/17.00 % (3012954)Instruction limit reached! % 118.13/17.00 % (3012954)------------------------------ % 118.13/17.00 % (3012954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.13/17.00 % (3012954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.13/17.00 % (3012954)CaDiCaL version: 2.1.3 % 118.13/17.00 % (3012954)Termination reason: Instruction limit % 118.13/17.00 % (3012954)Termination phase: Saturation % 118.13/17.00 % (3012954)Time elapsed: 0.730 s % 118.13/17.00 % (3012954)Peak memory usage: 25 MB % 118.13/17.00 % (3012954)Instructions burned: 1474 (million) % 118.13/17.00 % (3012962)ott+10_1_sil=32000:tgt=ground:random_seed=3782548908:i=5114:av=off_2980 on theBenchmark for (2980ds/5114Mi) % 118.13/17.00 % (3012960)Instruction limit reached! % 118.13/17.00 % (3012960)------------------------------ % 118.13/17.00 % (3012960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.13/17.00 % (3012960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.13/17.00 % (3012960)CaDiCaL version: 2.1.3 % 118.13/17.00 % (3012960)Termination reason: Instruction limit % 118.13/17.00 % (3012960)Termination phase: Saturation % 118.13/17.00 % (3012960)Time elapsed: 0.476 s % 118.13/17.00 % (3012960)Peak memory usage: 15 MB % 118.13/17.00 % (3012960)Instructions burned: 869 (million) % 118.13/17.00 % (3012964)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1915377103:i=54282_2976 on theBenchmark for (2976ds/54282Mi) % 118.13/17.00 % TRYING [1] % 118.13/17.00 % TRYING [2] % 118.13/17.00 % (3012951)Instruction limit reached! % 118.13/17.00 % (3012951)------------------------------ % 118.13/17.00 % (3012951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.13/17.00 % (3012951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.13/17.00 % (3012951)CaDiCaL version: 2.1.3 % 118.13/17.00 % (3012951)Termination reason: Instruction limit % 118.13/17.00 % (3012951)Termination phase: Saturation % 118.13/17.00 % (3012951)Time elapsed: 2.678 s % 118.13/17.00 % (3012951)Peak memory usage: 46 MB % 118.13/17.00 % (3012951)Instructions burned: 5132 (million) % 118.13/17.00 % (3012966)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4054954474:i=3512:aac=none_2961 on theBenchmark for (2961ds/3512Mi) % 118.13/17.00 % (3012962)Instruction limit reached! % 118.13/17.00 % (3012962)------------------------------ % 118.13/17.00 % (3012962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.13/17.00 % (3012962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.13/17.00 % (3012962)CaDiCaL version: 2.1.3 % 118.13/17.00 % (3012962)Termination reason: Instruction limit % 118.13/17.00 % (3012962)Termination phase: Saturation % 206.77/29.44 % (3012962)Time elapsed: 3.029 s % 206.77/29.44 % (3012962)Peak memory usage: 90 MB % 206.77/29.44 % (3012962)Instructions burned: 5115 (million) % 206.77/29.44 % (3012968)dis+21_1_sil=32000:sas=cadical:random_seed=60933166:i=3773:amm=off_2950 on theBenchmark for (2950ds/3773Mi) % 206.77/29.44 % (3012966)Instruction limit reached! % 206.77/29.44 % (3012966)------------------------------ % 206.77/29.44 % (3012966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.77/29.44 % (3012966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.77/29.44 % (3012966)CaDiCaL version: 2.1.3 % 206.77/29.44 % (3012966)Termination reason: Instruction limit % 206.77/29.44 % (3012966)Termination phase: Saturation % 206.77/29.44 % (3012966)Time elapsed: 1.929 s % 206.77/29.44 % (3012966)Peak memory usage: 36 MB % 206.77/29.44 % (3012966)Instructions burned: 3512 (million) % 206.77/29.44 % (3012970)ott+11_1_sil=16000:gs=on:random_seed=623373584:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2942 on theBenchmark for (2942ds/2251Mi) % 206.77/29.44 % (3012968)Instruction limit reached! % 206.77/29.44 % (3012968)------------------------------ % 206.77/29.44 % (3012968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.77/29.44 % (3012968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.77/29.44 % (3012968)CaDiCaL version: 2.1.3 % 206.77/29.44 % (3012968)Termination reason: Instruction limit % 206.77/29.44 % (3012968)Termination phase: Saturation % 206.77/29.44 % (3012968)Time elapsed: 2.107 s % 206.77/29.44 % (3012968)Peak memory usage: 37 MB % 206.77/29.44 % (3012968)Instructions burned: 3775 (million) % 206.77/29.44 % (3012970)Instruction limit reached! % 206.77/29.44 % (3012970)------------------------------ % 206.77/29.44 % (3012970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.77/29.44 % (3012970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.77/29.44 % (3012970)CaDiCaL version: 2.1.3 % 206.77/29.44 % (3012970)Termination reason: Instruction limit % 206.77/29.44 % (3012970)Termination phase: Saturation % 206.77/29.44 % (3012970)Time elapsed: 1.344 s % 206.77/29.44 % (3012970)Peak memory usage: 40 MB % 206.77/29.44 % (3012970)Instructions burned: 2251 (million) % 206.77/29.44 % (3012972)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2763761501:fmbsr=1.6:i=67534_2928 on theBenchmark for (2928ds/67534Mi) % 206.77/29.44 % (3012974)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2103646901:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2928 on theBenchmark for (2928ds/4591Mi) % 206.77/29.44 % (3012972)Cannot represent all propositional literals internally % 206.77/29.44 % (3012972)Refutation not found, incomplete strategy % 206.77/29.44 % (3012972)------------------------------ % 206.77/29.44 % (3012972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.77/29.44 % (3012972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.77/29.44 % (3012972)CaDiCaL version: 2.1.3 % 206.77/29.44 % (3012972)Termination reason: Refutation not found, incomplete strategy % 206.77/29.44 % (3012972)Time elapsed: 0.080 s % 206.77/29.44 % (3012972)Peak memory usage: 13 MB % 206.77/29.44 % (3012972)Instructions burned: 165 (million) % 206.77/29.44 % (3012972)------------------------------ % 206.77/29.44 % (3012972)------------------------------ % 206.77/29.44 % (3012976)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4074079678:i=29340_2927 on theBenchmark for (2927ds/29340Mi) % 206.77/29.44 % (3012974)Instruction limit reached! % 206.77/29.44 % (3012974)------------------------------ % 206.77/29.44 % (3012974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.77/29.44 % (3012974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.77/29.44 % (3012974)CaDiCaL version: 2.1.3 % 206.77/29.44 % (3012974)Termination reason: Instruction limit % 206.77/29.44 % (3012974)Termination phase: Saturation % 206.77/29.44 % (3012974)Time elapsed: 1.996 s % 206.77/29.44 % (3012974)Peak memory usage: 44 MB % 206.77/29.44 % (3012974)Instructions burned: 4593 (million) % 206.77/29.44 % (3012978)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1259071788:i=5211_2908 on theBenchmark for (2908ds/5211Mi) % 206.77/29.44 % (3012946)Instruction limit reached! % 206.77/29.44 % (3012946)------------------------------ % 206.77/29.44 % (3012946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.77/29.44 % (3012946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.77/29.44 % (3012946)CaDiCaL version: 2.1.3 % 217.28/35.65 % (3012946)Termination reason: Instruction limit % 217.28/35.65 % (3012946)Termination phase: Finite model building constraint generation % 217.28/35.65 % (3012946)Time elapsed: 9.587 s % 217.28/35.65 % (3012946)Peak memory usage: 2128 MB % 217.28/35.65 % (3012946)Instructions burned: 22061 (million) % 217.28/35.65 % (3012980)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3432605915:i=5497:nm=2_2893 on theBenchmark for (2893ds/5497Mi) % 217.28/35.65 % (3012980)Cannot represent all propositional literals internally % 217.28/35.65 % (3012980)Refutation not found, incomplete strategy % 217.28/35.65 % (3012980)------------------------------ % 217.28/35.65 % (3012980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.28/35.65 % (3012980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.28/35.65 % (3012980)CaDiCaL version: 2.1.3 % 217.28/35.65 % (3012980)Termination reason: Refutation not found, incomplete strategy % 217.28/35.65 % (3012980)Time elapsed: 0.064 s % 217.28/35.65 % (3012980)Peak memory usage: 13 MB % 217.28/35.65 % (3012980)Instructions burned: 123 (million) % 217.28/35.65 % (3012980)------------------------------ % 217.28/35.65 % (3012980)------------------------------ % 217.28/35.65 % (3012982)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3467292845:fmbsr=2:i=46332_2892 on theBenchmark for (2892ds/46332Mi) % 217.28/35.65 % (3012982)Cannot represent all propositional literals internally % 217.28/35.65 % (3012982)Refutation not found, incomplete strategy % 217.28/35.65 % (3012982)------------------------------ % 217.28/35.65 % (3012982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.28/35.65 % (3012982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.28/35.65 % (3012982)CaDiCaL version: 2.1.3 % 217.28/35.65 % (3012982)Termination reason: Refutation not found, incomplete strategy % 217.28/35.65 % (3012982)Time elapsed: 0.080 s % 217.28/35.65 % (3012982)Peak memory usage: 13 MB % 217.28/35.65 % (3012982)Instructions burned: 165 (million) % 217.28/35.65 % (3012982)------------------------------ % 217.28/35.65 % (3012982)------------------------------ % 217.28/35.65 % (3012984)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2620287311:i=14071_2891 on theBenchmark for (2891ds/14071Mi) % 217.28/35.65 % (3012984)Cannot represent all propositional literals internally % 217.28/35.65 % (3012984)Refutation not found, incomplete strategy % 217.28/35.65 % (3012984)------------------------------ % 217.28/35.65 % (3012984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.28/35.65 % (3012984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.28/35.65 % (3012984)CaDiCaL version: 2.1.3 % 217.28/35.65 % (3012984)Termination reason: Refutation not found, incomplete strategy % 217.28/35.65 % (3012984)Time elapsed: 0.069 s % 217.28/35.65 % (3012984)Peak memory usage: 13 MB % 217.28/35.65 % (3012984)Instructions burned: 135 (million) % 217.28/35.65 % (3012984)------------------------------ % 217.28/35.65 % (3012984)------------------------------ % 217.28/35.65 % (3012986)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3830673889:i=22565:add=on:rawr=on_2890 on theBenchmark for (2890ds/22565Mi) % 217.28/35.65 % (3012978)Instruction limit reached! % 217.28/35.65 % (3012978)------------------------------ % 217.28/35.65 % (3012978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.28/35.65 % (3012978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.28/35.65 % (3012978)CaDiCaL version: 2.1.3 % 217.28/35.65 % (3012978)Termination reason: Instruction limit % 217.28/35.65 % (3012978)Termination phase: Saturation % 217.28/35.65 % (3012978)Time elapsed: 2.691 s % 217.28/35.65 % (3012978)Peak memory usage: 49 MB % 217.28/35.65 % (3012978)Instructions burned: 5212 (million) % 217.28/35.65 % (3012988)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3345111812:i=8173:av=off_2881 on theBenchmark for (2881ds/8173Mi) % 217.28/35.65 % (3012988)Instruction limit reached! % 217.28/35.65 % (3012988)------------------------------ % 217.28/35.65 % (3012988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.28/35.65 % (3012988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.28/35.65 % (3012988)CaDiCaL version: 2.1.3 % 217.28/35.65 % (3012988)Termination reason: Instruction limit % 217.28/35.65 % (3012988)Termination phase: Saturation % 217.28/35.65 % (3012988)Time elapsed: 4.831 s % 217.28/35.65 % (3012988)Peak memory usage: 133 MB % 217.28/35.65 % (3012988)Instructions burned: 8174 (million) % 217.28/35.65 % (3012990)dis+10_16:1_sil=16000:random_seed=1909340103:i=9155:fsr=off_2832 on theBenchmark for (2832ds/9155Mi) % 238.06/39.43 % (3012990)Instruction limit reached! % 238.06/39.43 % (3012990)------------------------------ % 238.06/39.43 % (3012990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.06/39.43 % (3012990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.06/39.43 % (3012990)CaDiCaL version: 2.1.3 % 238.06/39.43 % (3012990)Termination reason: Instruction limit % 238.06/39.43 % (3012990)Termination phase: Saturation % 238.06/39.43 % (3012990)Time elapsed: 4.927 s % 238.06/39.43 % (3012990)Peak memory usage: 75 MB % 238.06/39.43 % (3012990)Instructions burned: 9156 (million) % 238.06/39.43 % (3012992)ott-3_8_sil=64000:random_seed=3695273729:i=20139:bs=on_2782 on theBenchmark for (2782ds/20139Mi) % 238.06/39.43 % (3012986)Instruction limit reached! % 238.06/39.43 % (3012986)------------------------------ % 238.06/39.43 % (3012986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.06/39.43 % (3012986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.06/39.43 % (3012986)CaDiCaL version: 2.1.3 % 238.06/39.43 % (3012986)Termination reason: Instruction limit % 238.06/39.43 % (3012986)Termination phase: Saturation % 238.06/39.43 % (3012986)Time elapsed: 11.207 s % 238.06/39.43 % (3012986)Peak memory usage: 353 MB % 238.06/39.43 % (3012986)Instructions burned: 22566 (million) % 238.06/39.43 % (3012994)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3331575199:fmbsr=2:i=32576_2778 on theBenchmark for (2778ds/32576Mi) % 238.06/39.43 % (3012994)Cannot represent all propositional literals internally % 238.06/39.43 % (3012994)Refutation not found, incomplete strategy % 238.06/39.43 % (3012994)------------------------------ % 238.06/39.43 % (3012994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.06/39.43 % (3012994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.06/39.43 % (3012994)CaDiCaL version: 2.1.3 % 238.06/39.43 % (3012994)Termination reason: Refutation not found, incomplete strategy % 238.06/39.43 % (3012994)Time elapsed: 0.067 s % 238.06/39.43 % (3012994)Peak memory usage: 13 MB % 238.06/39.43 % (3012994)Instructions burned: 128 (million) % 238.06/39.43 % (3012994)------------------------------ % 238.06/39.43 % (3012994)------------------------------ % 238.06/39.43 % (3012996)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=598725918:i=11404_2777 on theBenchmark for (2777ds/11404Mi) % 238.06/39.43 % (3012976)Instruction limit reached! % 238.06/39.43 % (3012976)------------------------------ % 238.06/39.43 % (3012976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.06/39.43 % (3012976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.06/39.43 % (3012976)CaDiCaL version: 2.1.3 % 238.06/39.43 % (3012976)Termination reason: Instruction limit % 238.06/39.43 % (3012976)Termination phase: Saturation % 238.06/39.43 % (3012976)Time elapsed: 15.126 s % 238.06/39.43 % (3012976)Peak memory usage: 179 MB % 238.06/39.43 % (3012976)Instructions burned: 29341 (million) % 238.06/39.43 % (3012998)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1868540068:i=14134_2776 on theBenchmark for (2776ds/14134Mi) % 238.06/39.43 % (3012998)Instruction limit reached! % 238.06/39.43 % (3012998)------------------------------ % 238.06/39.43 % (3012998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.06/39.43 % (3012998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.06/39.43 % (3012998)CaDiCaL version: 2.1.3 % 238.06/39.43 % (3012998)Termination reason: Instruction limit % 238.06/39.43 % (3012998)Termination phase: Saturation % 238.06/39.43 % (3012998)Time elapsed: 4.111 s % 238.06/39.43 % (3012998)Peak memory usage: 12 MB % 238.06/39.43 % (3012998)Instructions burned: 14134 (million) % 238.06/39.43 % (3013000)dis+33_16_sil=32000:sac=on:random_seed=2766040448:i=15851:nm=0_2734 on theBenchmark for (2734ds/15851Mi) % 238.06/39.43 % (3012992)Instruction limit reached! % 238.06/39.43 % (3012992)------------------------------ % 238.06/39.43 % (3012992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.06/39.43 % (3012992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.06/39.43 % (3012992)CaDiCaL version: 2.1.3 % 238.06/39.43 % (3012992)Termination reason: Instruction limit % 238.06/39.43 % (3012992)Termination phase: Saturation % 238.06/39.43 % (3012992)Time elapsed: 6.048 s % 238.06/39.43 % (3012992)Peak memory usage: 12 MB % 238.06/39.43 % (3012992)Instructions burned: 20141 (million) % 238.06/39.43 % (3013002)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3411944468:avsq=on:i=17627:add=on:amm=off_2722 on theBenchmark for (2722ds/17627Mi) % 238.06/39.43 % (3012996)Instruction limit reached! % 300.32/42.63 % (3012996)------------------------------ % 300.32/42.63 % (3012996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.32/42.63 % (3012996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/42.63 % (3012996)CaDiCaL version: 2.1.3 % 300.32/42.63 % (3012996)Termination reason: Instruction limit % 300.32/42.63 % (3012996)Termination phase: Saturation % 300.32/42.63 % (3012996)Time elapsed: 6.906 s % 300.32/42.63 % (3012996)Peak memory usage: 184 MB % 300.32/42.63 % (3012996)Instructions burned: 11405 (million) % 300.32/42.63 % (3013004)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4133866606:s2a=on:i=53295_2707 on theBenchmark for (2707ds/53295Mi) % 300.32/42.63 % (3013002)Instruction limit reached! % 300.32/42.63 % (3013002)------------------------------ % 300.32/42.63 % (3013002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.32/42.63 % (3013002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/42.63 % (3013002)CaDiCaL version: 2.1.3 % 300.32/42.63 % (3013002)Termination reason: Instruction limit % 300.32/42.63 % (3013002)Termination phase: Saturation % 300.32/42.63 % (3013002)Time elapsed: 6.646 s % 300.32/42.63 % (3013002)Peak memory usage: 59 MB % 300.32/42.63 % (3013002)Instructions burned: 17629 (million) % 300.32/42.63 % (3013007)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=375760334:i=26857:ins=20_2655 on theBenchmark for (2655ds/26857Mi) % 300.32/42.63 % (3013007)Cannot represent all propositional literals internally % 300.32/42.63 % (3013007)Refutation not found, incomplete strategy % 300.32/42.63 % (3013007)------------------------------ % 300.32/42.63 % (3013007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.32/42.63 % (3013007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/42.63 % (3013007)CaDiCaL version: 2.1.3 % 300.32/42.63 % (3013007)Termination reason: Refutation not found, incomplete strategy % 300.32/42.63 % (3013007)Time elapsed: 0.066 s % 300.32/42.63 % (3013007)Peak memory usage: 12 MB % 300.32/42.63 % (3013007)Instructions burned: 125 (million) % 300.32/42.63 % (3013007)------------------------------ % 300.32/42.63 % (3013007)------------------------------ % 300.32/42.63 % (3013009)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3854082270:i=28120:bs=on:fsr=off_2654 on theBenchmark for (2654ds/28120Mi) % 300.32/42.63 % (3012964)Instruction limit reached! % 300.32/42.63 % (3012964)------------------------------ % 300.32/42.63 % (3012964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.32/42.63 % (3012964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/42.63 % (3012964)CaDiCaL version: 2.1.3 % 300.32/42.63 % (3012964)Termination reason: Instruction limit % 300.32/42.63 % (3012964)Termination phase: Finite model building constraint generation % 300.32/42.63 % (3012964)Time elapsed: 32.370 s % 300.32/42.63 % (3012964)Peak memory usage: 10690 MB % 300.32/42.63 % (3012964)Instructions burned: 54282 (million) % 300.32/42.63 % (3013000)Instruction limit reached! % 300.32/42.63 % (3013000)------------------------------ % 300.32/42.63 % (3013000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.32/42.63 % (3013000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/42.63 % (3013000)CaDiCaL version: 2.1.3 % 300.32/42.63 % (3013000)Termination reason: Instruction limit % 300.32/42.63 % (3013000)Termination phase: Saturation % 300.32/42.63 % (3013000)Time elapsed: 8.743 s % 300.32/42.63 % (3013000)Peak memory usage: 135 MB % 300.32/42.63 % (3013000)Instructions burned: 15852 (million) % 300.32/42.63 % (3013011)fmb+10_1_sil=256000:fmbss=7:random_seed=1331975779:fmbsr=1.6:i=182295_2646 on theBenchmark for (2646ds/182295Mi) % 300.32/42.63 % (3013011)Cannot represent all propositional literals internally % 300.32/42.63 % (3013011)Refutation not found, incomplete strategy % 300.32/42.63 % (3013011)------------------------------ % 300.32/42.63 % (3013011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.32/42.63 % (3013011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/42.63 % (3013011)CaDiCaL version: 2.1.3 % 300.32/42.63 % (3013011)Termination reason: Refutation not found, incomplete strategy % 300.32/42.63 % (3013011)Time elapsed: 0.067 s % 300.32/42.63 % (3013011)Peak memory usage: 12 MB % 300.32/42.63 % (3013011)Instructions burned: 125 (million) % 300.32/42.63 % (3013011)------------------------------ % 300.32/42.63 % (3013011)------------------------------ % 300.32/42.63 % (3013013)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2219060247:i=44625:gsp=on_2645 onTerminated % 300.32/42.64 % Vampire exiting % 300.32/42.64 Terminated %------------------------------------------------------------------------------