%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM451+1 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/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 12:24:22 PM UTC 2026 % Result : Timeout 300.65s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM451+1 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.12/0.38 % Computer : n004.cluster.edu % 0.12/0.38 % Model : x86_64 x86_64 % 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.38 % Memory : 8046.5625MB % 0.12/0.38 % OS : Linux 6.8.0-71-generic % 0.12/0.38 % CPULimit : 300 % 0.12/0.38 % WCLimit : 300 % 0.12/0.38 % DateTime : Sun Sep 27 19:58:37 UTC 2026 % 0.12/0.38 % CPUTime : % 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.12/0.40 Running first-order model finding % 0.12/0.40 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 % 14.79/2.54 % (3841802)Will run a generic schedule for satisfiability detection. % 14.79/2.54 % (3841812)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=92092813:i=131_2999 on theBenchmark for (2999ds/131Mi) % 14.79/2.54 % (3841807)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=956873440_2999 on theBenchmark for (2999ds/0Mi) % 14.79/2.54 % (3841813)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3944854858:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 14.79/2.54 % (3841809)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1316568497:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 14.79/2.54 % (3841810)dis+10_1_sil=32000:sp=arity:random_seed=1811956252:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 14.79/2.54 % (3841811)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4251187339:i=116_2999 on theBenchmark for (2999ds/116Mi) % 14.79/2.54 % (3841808)% WARNING: option uhcvi not known. % 14.79/2.54 % (3841808)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3213654485:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 14.79/2.54 % TRYING [1] % 14.79/2.54 % TRYING [2] % 14.79/2.54 % TRYING [3] % 14.79/2.54 % TRYING [4] % 14.79/2.54 % (3841812)Instruction limit reached! % 14.79/2.54 % (3841812)------------------------------ % 14.79/2.54 % (3841812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.79/2.54 % (3841812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.79/2.54 % (3841812)CaDiCaL version: 2.1.3 % 14.79/2.54 % (3841812)Termination reason: Instruction limit % 14.79/2.54 % (3841812)Termination phase: Saturation % 14.79/2.54 % (3841812)Time elapsed: 0.036 s % 14.79/2.54 % (3841812)Peak memory usage: 12 MB % 14.79/2.54 % (3841812)Instructions burned: 132 (million) % 14.79/2.54 % (3841821)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3896425946:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 14.79/2.54 % TRYING [1] % 14.79/2.54 % TRYING [2] % 14.79/2.54 % TRYING [3] % 14.79/2.54 % TRYING [4] % 14.79/2.54 % (3841810)Instruction limit reached! % 14.79/2.54 % (3841810)------------------------------ % 14.79/2.54 % (3841810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.79/2.54 % (3841810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.79/2.54 % (3841810)CaDiCaL version: 2.1.3 % 14.79/2.54 % (3841810)Termination reason: Instruction limit % 14.79/2.54 % (3841810)Termination phase: Saturation % 14.79/2.54 % (3841810)Time elapsed: 0.067 s % 14.79/2.54 % (3841810)Peak memory usage: 13 MB % 14.79/2.54 % (3841810)Instructions burned: 104 (million) % 14.79/2.54 % TRYING [5] % 14.79/2.54 % (3841811)Instruction limit reached! % 14.79/2.54 % (3841811)------------------------------ % 14.79/2.54 % (3841811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.79/2.54 % (3841811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.79/2.54 % (3841811)CaDiCaL version: 2.1.3 % 14.79/2.54 % (3841811)Termination reason: Instruction limit % 14.79/2.54 % (3841811)Termination phase: Saturation % 14.79/2.54 % (3841811)Time elapsed: 0.071 s % 14.79/2.54 % (3841811)Peak memory usage: 13 MB % 14.79/2.54 % (3841811)Instructions burned: 117 (million) % 14.79/2.54 % TRYING [5] % 14.79/2.54 % (3841823)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3298344600:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 14.79/2.54 % (3841824)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=2185283927:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 14.79/2.54 % (3841813)Instruction limit reached! % 14.79/2.54 % (3841813)------------------------------ % 14.79/2.54 % (3841813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.79/2.54 % (3841813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.79/2.54 % (3841813)CaDiCaL version: 2.1.3 % 14.79/2.54 % (3841813)Termination reason: Instruction limit % 14.79/2.54 % (3841813)Termination phase: Saturation % 14.79/2.54 % (3841813)Time elapsed: 0.093 s % 14.79/2.54 % (3841813)Peak memory usage: 14 MB % 14.79/2.54 % (3841813)Instructions burned: 159 (million) % 14.79/2.54 % (3841827)ott-21_1_sil=16000:fs=off:random_seed=149706033:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 14.79/2.54 % TRYING [6] % 14.79/2.54 % (3841823)Instruction limit reached! % 14.79/2.54 % (3841823)------------------------------ % 14.79/2.54 % (3841823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.88/6.69 % (3841823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.88/6.69 % (3841823)CaDiCaL version: 2.1.3 % 43.88/6.69 % (3841823)Termination reason: Instruction limit % 43.88/6.69 % (3841823)Termination phase: Saturation % 43.88/6.69 % (3841823)Time elapsed: 0.065 s % 43.88/6.69 % (3841823)Peak memory usage: 12 MB % 43.88/6.69 % (3841823)Instructions burned: 131 (million) % 43.88/6.69 % (3841829)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=594976717:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 43.88/6.69 % TRYING [6] % 43.88/6.69 % (3841821)Instruction limit reached! % 43.88/6.69 % (3841821)------------------------------ % 43.88/6.69 % (3841821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.88/6.69 % (3841821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.88/6.69 % (3841821)CaDiCaL version: 2.1.3 % 43.88/6.69 % (3841821)Termination reason: Instruction limit % 43.88/6.69 % (3841821)Termination phase: Finite model building constraint generation % 43.88/6.69 % (3841821)Time elapsed: 0.150 s % 43.88/6.69 % (3841821)Peak memory usage: 29 MB % 43.88/6.69 % (3841821)Instructions burned: 717 (million) % 43.88/6.69 % (3841831)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=487828061:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 43.88/6.69 % (3841827)Instruction limit reached! % 43.88/6.69 % (3841827)------------------------------ % 43.88/6.69 % (3841827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.88/6.69 % (3841827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.88/6.69 % (3841827)CaDiCaL version: 2.1.3 % 43.88/6.69 % (3841827)Termination reason: Instruction limit % 43.88/6.69 % (3841827)Termination phase: Saturation % 43.88/6.69 % (3841827)Time elapsed: 0.096 s % 43.88/6.69 % (3841827)Peak memory usage: 13 MB % 43.88/6.69 % (3841827)Instructions burned: 182 (million) % 43.88/6.69 % TRYING [1] % 43.88/6.69 % TRYING [2] % 43.88/6.69 % TRYING [3] % 43.88/6.69 % (3841833)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3578184049:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 43.88/6.69 % TRYING [4] % 43.88/6.69 % TRYING [5] % 43.88/6.69 % (3841831)Instruction limit reached! % 43.88/6.69 % (3841831)------------------------------ % 43.88/6.69 % (3841831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.88/6.69 % (3841831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.88/6.69 % (3841831)CaDiCaL version: 2.1.3 % 43.88/6.69 % (3841831)Termination reason: Instruction limit % 43.88/6.69 % (3841831)Termination phase: Finite model building SAT solving % 43.88/6.69 % (3841831)Time elapsed: 0.182 s % 43.88/6.69 % (3841831)Peak memory usage: 24 MB % 43.88/6.69 % (3841831)Instructions burned: 868 (million) % 43.88/6.69 % (3841835)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=187046508:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 43.88/6.69 % (3841824)Instruction limit reached! % 43.88/6.69 % (3841824)------------------------------ % 43.88/6.69 % (3841824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.88/6.69 % (3841824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.88/6.69 % (3841824)CaDiCaL version: 2.1.3 % 43.88/6.69 % (3841824)Termination reason: Instruction limit % 43.88/6.69 % (3841824)Termination phase: Saturation % 43.88/6.69 % (3841824)Time elapsed: 0.356 s % 43.88/6.69 % (3841824)Peak memory usage: 19 MB % 43.88/6.69 % (3841824)Instructions burned: 684 (million) % 43.88/6.69 % (3841837)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=1608817513:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 43.88/6.69 % (3841829)Instruction limit reached! % 43.88/6.69 % (3841829)------------------------------ % 43.88/6.69 % (3841829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.88/6.69 % (3841829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.88/6.69 % (3841829)CaDiCaL version: 2.1.3 % 43.88/6.69 % (3841829)Termination reason: Instruction limit % 43.88/6.69 % (3841829)Termination phase: Saturation % 43.88/6.69 % (3841829)Time elapsed: 0.313 s % 43.88/6.69 % (3841829)Peak memory usage: 15 MB % 43.88/6.69 % (3841829)Instructions burned: 478 (million) % 43.88/6.69 % (3841839)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2182327550:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 43.88/6.69 % TRYING [14] % 43.88/6.69 % TRYING [7] % 43.88/6.69 % (3841835)Instruction limit reached! % 71.51/10.50 % (3841835)------------------------------ % 71.51/10.50 % (3841835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.51/10.50 % (3841835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.51/10.50 % (3841835)CaDiCaL version: 2.1.3 % 71.51/10.50 % (3841835)Termination reason: Instruction limit % 71.51/10.50 % (3841835)Termination phase: Finite model building constraint generation % 71.51/10.50 % (3841835)Time elapsed: 0.205 s % 71.51/10.50 % (3841835)Peak memory usage: 85 MB % 71.51/10.50 % (3841835)Instructions burned: 893 (million) % 71.51/10.50 % (3841841)fmb+10_1_sil=64000:random_seed=955075446:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 71.51/10.50 % TRYING [1] % 71.51/10.50 % TRYING [2] % 71.51/10.50 % TRYING [3] % 71.51/10.50 % TRYING [4] % 71.51/10.50 % TRYING [5] % 71.51/10.50 % TRYING [6] % 71.51/10.50 % (3841837)Instruction limit reached! % 71.51/10.50 % (3841837)------------------------------ % 71.51/10.50 % (3841837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.51/10.50 % (3841837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.51/10.50 % (3841837)CaDiCaL version: 2.1.3 % 71.51/10.50 % (3841837)Termination reason: Instruction limit % 71.51/10.50 % (3841837)Termination phase: Saturation % 71.51/10.50 % (3841837)Time elapsed: 0.377 s % 71.51/10.50 % (3841837)Peak memory usage: 16 MB % 71.51/10.50 % (3841837)Instructions burned: 693 (million) % 71.51/10.50 % (3841843)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=455945122:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 71.51/10.50 % TRYING [20] % 71.51/10.50 % (3841833)Instruction limit reached! % 71.51/10.50 % (3841833)------------------------------ % 71.51/10.50 % (3841833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.51/10.50 % (3841833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.51/10.50 % (3841833)CaDiCaL version: 2.1.3 % 71.51/10.50 % (3841833)Termination reason: Instruction limit % 71.51/10.50 % (3841833)Termination phase: Saturation % 71.51/10.50 % (3841833)Time elapsed: 0.685 s % 71.51/10.50 % (3841833)Peak memory usage: 27 MB % 71.51/10.50 % (3841833)Instructions burned: 1179 (million) % 71.51/10.50 % (3841845)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3228958193:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 71.51/10.50 % TRYING [8] % 71.51/10.50 % (3841839)Instruction limit reached! % 71.51/10.50 % (3841839)------------------------------ % 71.51/10.50 % (3841839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.51/10.50 % (3841839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.51/10.50 % (3841839)CaDiCaL version: 2.1.3 % 71.51/10.50 % (3841839)Termination reason: Instruction limit % 71.51/10.50 % (3841839)Termination phase: Saturation % 71.51/10.50 % (3841839)Time elapsed: 0.488 s % 71.51/10.50 % (3841839)Peak memory usage: 20 MB % 71.51/10.50 % (3841839)Instructions burned: 880 (million) % 71.51/10.50 % (3841847)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=291324825:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 71.51/10.50 % TRYING [7] % 71.51/10.50 % (3841845)Instruction limit reached! % 71.51/10.50 % (3841845)------------------------------ % 71.51/10.50 % (3841845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.51/10.50 % (3841845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.51/10.50 % (3841845)CaDiCaL version: 2.1.3 % 71.51/10.50 % (3841845)Termination reason: Instruction limit % 71.51/10.50 % (3841845)Termination phase: Finite model building constraint generation % 71.51/10.50 % (3841845)Time elapsed: 0.344 s % 71.51/10.50 % (3841845)Peak memory usage: 71 MB % 71.51/10.50 % (3841845)Instructions burned: 922 (million) % 71.51/10.50 % (3841849)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4205845894:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 71.51/10.50 % (3841849)Instruction limit reached! % 71.51/10.50 % (3841849)------------------------------ % 71.51/10.50 % (3841849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.51/10.50 % (3841849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.51/10.50 % (3841849)CaDiCaL version: 2.1.3 % 71.51/10.50 % (3841849)Termination reason: Instruction limit % 71.51/10.50 % (3841849)Termination phase: Saturation % 71.51/10.50 % (3841849)Time elapsed: 0.761 s % 71.51/10.50 % (3841849)Peak memory usage: 33 MB % 71.51/10.50 % (3841849)Instructions burned: 1474 (million) % 71.51/10.50 % (3841851)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=162230060:i=6324_2978 on theBenchmark for (2978ds/6324Mi) % 229.02/32.80 % TRYING [77] % 229.02/32.80 % TRYING [8] % 229.02/32.80 % TRYING [8] % 229.02/32.80 % (3841847)Instruction limit reached! % 229.02/32.80 % (3841847)------------------------------ % 229.02/32.80 % (3841847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.02/32.80 % (3841847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.02/32.80 % (3841847)CaDiCaL version: 2.1.3 % 229.02/32.80 % (3841847)Termination reason: Instruction limit % 229.02/32.80 % (3841847)Termination phase: Saturation % 229.02/32.80 % (3841847)Time elapsed: 2.585 s % 229.02/32.80 % (3841847)Peak memory usage: 31 MB % 229.02/32.80 % (3841847)Instructions burned: 5132 (million) % 229.02/32.80 % (3841853)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2017448534:fmbsr=2.30978:i=2174_2963 on theBenchmark for (2963ds/2174Mi) % 229.02/32.80 % TRYING [16] % 229.02/32.80 % (3841851)Instruction limit reached! % 229.02/32.80 % (3841851)------------------------------ % 229.02/32.80 % (3841851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.02/32.80 % (3841851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.02/32.80 % (3841851)CaDiCaL version: 2.1.3 % 229.02/32.80 % (3841851)Termination reason: Instruction limit % 229.02/32.80 % (3841851)Termination phase: Finite model building constraint generation % 229.02/32.80 % (3841851)Time elapsed: 2.089 s % 229.02/32.80 % (3841851)Peak memory usage: 327 MB % 229.02/32.80 % (3841851)Instructions burned: 6324 (million) % 229.02/32.80 % (3841843)Instruction limit reached! % 229.02/32.80 % (3841843)------------------------------ % 229.02/32.80 % (3841843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.02/32.80 % (3841843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.02/32.80 % (3841843)CaDiCaL version: 2.1.3 % 229.02/32.80 % (3841843)Termination reason: Instruction limit % 229.02/32.80 % (3841843)Termination phase: Finite model building constraint generation % 229.02/32.80 % (3841843)Time elapsed: 3.344 s % 229.02/32.80 % (3841843)Peak memory usage: 568 MB % 229.02/32.80 % (3841843)Instructions burned: 9517 (million) % 229.02/32.80 % (3841855)ott-2_1_sil=16000:newcnf=on:random_seed=3803143607:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi) % 229.02/32.80 % (3841857)ott+10_1_sil=32000:tgt=ground:random_seed=77008668:i=5114:av=off_2956 on theBenchmark for (2956ds/5114Mi) % 229.02/32.80 % (3841853)Instruction limit reached! % 229.02/32.80 % (3841853)------------------------------ % 229.02/32.80 % (3841853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.02/32.80 % (3841853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.02/32.80 % (3841853)CaDiCaL version: 2.1.3 % 229.02/32.80 % (3841853)Termination reason: Instruction limit % 229.02/32.80 % (3841853)Termination phase: Finite model building constraint generation % 229.02/32.80 % (3841853)Time elapsed: 0.754 s % 229.02/32.80 % (3841853)Peak memory usage: 133 MB % 229.02/32.80 % (3841853)Instructions burned: 2175 (million) % 229.02/32.80 % (3841859)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2997664240:i=54282_2955 on theBenchmark for (2955ds/54282Mi) % 229.02/32.80 % TRYING [1] % 229.02/32.80 % TRYING [2] % 229.02/32.80 % TRYING [3] % 229.02/32.80 % TRYING [4] % 229.02/32.80 % TRYING [5] % 229.02/32.80 % TRYING [6] % 229.02/32.80 % (3841855)Instruction limit reached! % 229.02/32.80 % (3841855)------------------------------ % 229.02/32.80 % (3841855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.02/32.80 % (3841855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.02/32.80 % (3841855)CaDiCaL version: 2.1.3 % 229.02/32.80 % (3841855)Termination reason: Instruction limit % 229.02/32.80 % (3841855)Termination phase: Saturation % 229.02/32.80 % (3841855)Time elapsed: 0.468 s % 229.02/32.80 % (3841855)Peak memory usage: 21 MB % 229.02/32.80 % (3841855)Instructions burned: 871 (million) % 229.02/32.80 % (3841861)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3313279451:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi) % 229.02/32.80 % TRYING [7] % 229.02/32.80 % TRYING [9] % 229.02/32.80 % (3841841)Instruction limit reached! % 229.02/32.80 % (3841841)------------------------------ % 229.02/32.80 % (3841841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.02/32.80 % (3841841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.02/32.80 % (3841841)CaDiCaL version: 2.1.3 % 229.02/32.80 % (3841841)Termination reason: Instruction limit % 229.02/32.80 % (3841841)Termination phase: Finite model building SAT solving % 229.02/32.80 % (3841841)Time elapsed: 5.625 s % 229.02/32.80 % (3841841)Peak memory usage: 156 MB % 229.02/32.80 % (3841841)Instructions burned: 22067 (million) % 300.65/42.83 % (3841863)dis+21_1_sil=32000:sas=cadical:random_seed=224486012:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi) % 300.65/42.83 % (3841861)Instruction limit reached! % 300.65/42.83 % (3841861)------------------------------ % 300.65/42.83 % (3841861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.65/42.83 % (3841861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.65/42.83 % (3841861)CaDiCaL version: 2.1.3 % 300.65/42.83 % (3841861)Termination reason: Instruction limit % 300.65/42.83 % (3841861)Termination phase: Saturation % 300.65/42.83 % (3841861)Time elapsed: 1.940 s % 300.65/42.83 % (3841861)Peak memory usage: 35 MB % 300.65/42.83 % (3841861)Instructions burned: 3513 (million) % 300.65/42.83 % (3841865)ott+11_1_sil=16000:gs=on:random_seed=2912293558:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2932 on theBenchmark for (2932ds/2251Mi) % 300.65/42.83 % TRYING [8] % 300.65/42.83 % (3841857)Instruction limit reached! % 300.65/42.83 % (3841857)------------------------------ % 300.65/42.83 % (3841857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.65/42.83 % (3841857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.65/42.83 % (3841857)CaDiCaL version: 2.1.3 % 300.65/42.83 % (3841857)Termination reason: Instruction limit % 300.65/42.83 % (3841857)Termination phase: Saturation % 300.65/42.83 % (3841857)Time elapsed: 2.965 s % 300.65/42.83 % (3841857)Peak memory usage: 77 MB % 300.65/42.83 % (3841857)Instructions burned: 5115 (million) % 300.65/42.83 % (3841867)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1216358940:fmbsr=1.6:i=67534_2926 on theBenchmark for (2926ds/67534Mi) % 300.65/42.83 % TRYING [7] % 300.65/42.83 % (3841863)Instruction limit reached! % 300.65/42.83 % (3841863)------------------------------ % 300.65/42.83 % (3841863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.65/42.83 % (3841863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.65/42.83 % (3841863)CaDiCaL version: 2.1.3 % 300.65/42.83 % (3841863)Termination reason: Instruction limit % 300.65/42.83 % (3841863)Termination phase: Saturation % 300.65/42.83 % (3841863)Time elapsed: 1.089 s % 300.65/42.83 % (3841863)Peak memory usage: 40 MB % 300.65/42.83 % (3841863)Instructions burned: 3776 (million) % 300.65/42.83 % (3841869)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1581106897:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2926 on theBenchmark for (2926ds/4591Mi) % 300.65/42.83 % (3841865)Instruction limit reached! % 300.65/42.83 % (3841865)------------------------------ % 300.65/42.83 % (3841865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.65/42.83 % (3841865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.65/42.83 % (3841865)CaDiCaL version: 2.1.3 % 300.65/42.83 % (3841865)Termination reason: Instruction limit % 300.65/42.83 % (3841865)Termination phase: Saturation % 300.65/42.83 % (3841865)Time elapsed: 0.913 s % 300.65/42.83 % (3841865)Peak memory usage: 15 MB % 300.65/42.83 % (3841865)Instructions burned: 2253 (million) % 300.65/42.83 % (3841871)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3460124509:i=29340_2923 on theBenchmark for (2923ds/29340Mi) % 300.65/42.83 % (3841869)Instruction limit reached! % 300.65/42.83 % (3841869)------------------------------ % 300.65/42.83 % (3841869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.65/42.83 % (3841869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.65/42.83 % (3841869)CaDiCaL version: 2.1.3 % 300.65/42.83 % (3841869)Termination reason: Instruction limit % 300.65/42.83 % (3841869)Termination phase: Saturation % 300.65/42.83 % (3841869)Time elapsed: 1.248 s % 300.65/42.83 % (3841869)Peak memory usage: 64 MB % 300.65/42.83 % (3841869)Instructions burned: 4591 (million) % 300.65/42.83 % (3841873)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3110567525:i=5211_2913 on theBenchmark for (2913ds/5211Mi) % 300.65/42.83 % TRYING [8] % 300.65/42.83 % (3841873)Instruction limit reached! % 300.65/42.83 % (3841873)------------------------------ % 300.65/42.83 % (3841873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.65/42.83 % (3841873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.65/42.83 % (3841873)CaDiCaL version: 2.1.3 % 300.65/42.83 % (3841873)Termination reason: Instruction limit % 300.65/42.83 % (3841873)Termination phase: Saturation % 300.65/42.83 % (3841873)Time elapsed: 1.405 s % 300.65/42.83 % (3841873)Peak memory usage: 43 MB % 300.65/42.83 % (3841873)Instructions burned: 5212 (million) % 300.65/42.83 % (3841875)fmb+10_1_sil=32 % 300.65/42.84 Terminated % 300.65/42.84 % Vampire exiting % 300.65/42.84 Terminated %------------------------------------------------------------------------------