%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW471_20 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n012.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:40:07 PM UTC 2026 % Result : Timeout 300.15s 42.84s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW471_20 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.15 % Computer : n012.cluster.edu % 0.07/0.15 % Model : x86_64 x86_64 % 0.07/0.15 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.15 % Memory : 8046.5625MB % 0.07/0.15 % OS : Linux 6.8.0-71-generic % 0.07/0.15 % CPULimit : 300 % 0.07/0.15 % WCLimit : 300 % 0.07/0.15 % DateTime : Mon Sep 28 14:02:34 UTC 2026 % 0.07/0.15 % CPUTime : % 0.07/0.15 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.18 Running first-order model finding % 0.07/0.18 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 % 24.37/3.72 % (3390790)Will run a generic schedule for satisfiability detection. % 24.37/3.72 % (3390796)% WARNING: option uhcvi not known. % 24.37/3.72 % (3390797)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1397276608:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 24.37/3.72 % (3390796)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3865461325:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 24.37/3.72 % (3390801)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4007024975:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 24.37/3.72 % (3390800)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1359536820:i=131_2999 on theBenchmark for (2999ds/131Mi) % 24.37/3.72 % (3390799)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3166339456:i=116_2999 on theBenchmark for (2999ds/116Mi) % 24.37/3.72 % (3390798)dis+10_1_sil=32000:sp=arity:random_seed=291988287:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 24.37/3.72 % (3390795)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=905411852_2999 on theBenchmark for (2999ds/0Mi) % 24.37/3.72 % (3390798)Instruction limit reached! % 24.37/3.72 % (3390798)------------------------------ % 24.37/3.72 % (3390798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.37/3.72 % (3390798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.37/3.72 % (3390798)CaDiCaL version: 2.1.3 % 24.37/3.72 % (3390798)Termination reason: Instruction limit % 24.37/3.72 % (3390798)Termination phase: Saturation % 24.37/3.72 % (3390798)Time elapsed: 0.052 s % 24.37/3.72 % (3390798)Peak memory usage: 14 MB % 24.37/3.72 % (3390798)Instructions burned: 104 (million) % 24.37/3.72 % (3390799)Instruction limit reached! % 24.37/3.72 % (3390799)------------------------------ % 24.37/3.72 % (3390799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.37/3.72 % (3390799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.37/3.72 % (3390799)CaDiCaL version: 2.1.3 % 24.37/3.72 % (3390799)Termination reason: Instruction limit % 24.37/3.72 % (3390799)Termination phase: Saturation % 24.37/3.72 % (3390799)Time elapsed: 0.055 s % 24.37/3.72 % (3390799)Peak memory usage: 14 MB % 24.37/3.72 % (3390799)Instructions burned: 116 (million) % 24.37/3.72 % (3390800)Instruction limit reached! % 24.37/3.72 % (3390800)------------------------------ % 24.37/3.72 % (3390800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.37/3.72 % (3390800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.37/3.72 % (3390800)CaDiCaL version: 2.1.3 % 24.37/3.72 % (3390800)Termination reason: Instruction limit % 24.37/3.72 % (3390800)Termination phase: Saturation % 24.37/3.72 % (3390800)Time elapsed: 0.064 s % 24.37/3.72 % (3390800)Peak memory usage: 14 MB % 24.37/3.72 % (3390800)Instructions burned: 132 (million) % 24.37/3.72 % (3390810)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=102844548:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 24.37/3.72 % (3390809)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=118964212:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 24.37/3.72 % (3390801)Instruction limit reached! % 24.37/3.72 % (3390801)------------------------------ % 24.37/3.72 % (3390801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.37/3.72 % (3390801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.37/3.72 % (3390801)CaDiCaL version: 2.1.3 % 24.37/3.72 % (3390801)Termination reason: Instruction limit % 24.37/3.72 % (3390801)Termination phase: Saturation % 24.37/3.72 % (3390801)Time elapsed: 0.081 s % 24.37/3.72 % (3390801)Peak memory usage: 15 MB % 24.37/3.72 % (3390801)Instructions burned: 160 (million) % 24.37/3.72 % (3390811)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=424574130:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 24.37/3.72 % (3390814)ott-21_1_sil=16000:fs=off:random_seed=463944881:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 24.37/3.72 % (3390810)Instruction limit reached! % 24.37/3.72 % (3390810)------------------------------ % 24.37/3.72 % (3390810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.37/3.72 % (3390810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.37/3.72 % (3390810)CaDiCaL version: 2.1.3 % 48.48/7.13 % (3390810)Termination reason: Instruction limit % 48.48/7.13 % (3390810)Termination phase: Saturation % 48.48/7.13 % (3390810)Time elapsed: 0.063 s % 48.48/7.13 % (3390810)Peak memory usage: 14 MB % 48.48/7.13 % (3390810)Instructions burned: 131 (million) % 48.48/7.13 % (3390817)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1069504413:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 48.48/7.13 % (3390814)Instruction limit reached! % 48.48/7.13 % (3390814)------------------------------ % 48.48/7.13 % (3390814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.48/7.13 % (3390814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.48/7.13 % (3390814)CaDiCaL version: 2.1.3 % 48.48/7.13 % (3390814)Termination reason: Instruction limit % 48.48/7.13 % (3390814)Termination phase: Saturation % 48.48/7.13 % (3390814)Time elapsed: 0.087 s % 48.48/7.13 % (3390814)Peak memory usage: 14 MB % 48.48/7.13 % (3390814)Instructions burned: 186 (million) % 48.48/7.13 % (3390819)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1180360484:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 48.48/7.13 % (3390817)Instruction limit reached! % 48.48/7.13 % (3390817)------------------------------ % 48.48/7.13 % (3390817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.48/7.13 % (3390817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.48/7.13 % (3390817)CaDiCaL version: 2.1.3 % 48.48/7.13 % (3390817)Termination reason: Instruction limit % 48.48/7.13 % (3390817)Termination phase: Saturation % 48.48/7.13 % (3390817)Time elapsed: 0.248 s % 48.48/7.13 % (3390817)Peak memory usage: 16 MB % 48.48/7.13 % (3390817)Instructions burned: 477 (million) % 48.48/7.13 % (3390809)Instruction limit reached! % 48.48/7.13 % (3390809)------------------------------ % 48.48/7.13 % (3390809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.48/7.13 % (3390809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.48/7.13 % (3390809)CaDiCaL version: 2.1.3 % 48.48/7.13 % (3390809)Termination reason: Instruction limit % 48.48/7.13 % (3390809)Termination phase: Finite model building preprocessing % 48.48/7.13 % (3390809)Time elapsed: 0.324 s % 48.48/7.13 % (3390809)Peak memory usage: 19 MB % 48.48/7.13 % (3390809)Instructions burned: 715 (million) % 48.48/7.13 % (3390821)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1052009944:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 48.48/7.13 % (3390822)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=918381725:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 48.48/7.13 % (3390811)Instruction limit reached! % 48.48/7.13 % (3390811)------------------------------ % 48.48/7.13 % (3390811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.48/7.13 % (3390811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.48/7.13 % (3390811)CaDiCaL version: 2.1.3 % 48.48/7.13 % (3390811)Termination reason: Instruction limit % 48.48/7.13 % (3390811)Termination phase: Saturation % 48.48/7.13 % (3390811)Time elapsed: 0.357 s % 48.48/7.13 % (3390811)Peak memory usage: 19 MB % 48.48/7.13 % (3390811)Instructions burned: 684 (million) % 48.48/7.13 % (3390825)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=534136534: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) % 48.48/7.13 % (3390819)Instruction limit reached! % 48.48/7.13 % (3390819)------------------------------ % 48.48/7.13 % (3390819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.48/7.13 % (3390819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.48/7.13 % (3390819)CaDiCaL version: 2.1.3 % 48.48/7.13 % (3390819)Termination reason: Instruction limit % 48.48/7.13 % (3390819)Termination phase: Finite model building preprocessing % 48.48/7.13 % (3390819)Time elapsed: 0.402 s % 48.48/7.13 % (3390819)Peak memory usage: 28 MB % 48.48/7.13 % (3390819)Instructions burned: 867 (million) % 48.48/7.13 % (3390827)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3292097334:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 48.48/7.13 % (3390825)Instruction limit reached! % 48.48/7.13 % (3390825)------------------------------ % 48.48/7.13 % (3390825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.48/7.13 % (3390825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.70/11.34 % (3390825)CaDiCaL version: 2.1.3 % 77.70/11.34 % (3390825)Termination reason: Instruction limit % 77.70/11.34 % (3390825)Termination phase: Saturation % 77.70/11.34 % (3390825)Time elapsed: 0.375 s % 77.70/11.34 % (3390825)Peak memory usage: 20 MB % 77.70/11.34 % (3390825)Instructions burned: 692 (million) % 77.70/11.34 % (3390822)Instruction limit reached! % 77.70/11.34 % (3390822)------------------------------ % 77.70/11.34 % (3390822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.70/11.34 % (3390822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.70/11.34 % (3390822)CaDiCaL version: 2.1.3 % 77.70/11.34 % (3390822)Termination reason: Instruction limit % 77.70/11.34 % (3390822)Termination phase: Finite model building preprocessing % 77.70/11.34 % (3390822)Time elapsed: 0.437 s % 77.70/11.34 % (3390822)Peak memory usage: 29 MB % 77.70/11.34 % (3390822)Instructions burned: 890 (million) % 77.70/11.34 % (3390829)fmb+10_1_sil=64000:random_seed=1162423237:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi) % 77.70/11.34 % (3390830)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4006002081:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 77.70/11.34 % (3390821)Instruction limit reached! % 77.70/11.34 % (3390821)------------------------------ % 77.70/11.34 % (3390821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.70/11.34 % (3390821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.70/11.34 % (3390821)CaDiCaL version: 2.1.3 % 77.70/11.34 % (3390821)Termination reason: Instruction limit % 77.70/11.34 % (3390821)Termination phase: Saturation % 77.70/11.34 % (3390821)Time elapsed: 0.536 s % 77.70/11.34 % (3390821)Peak memory usage: 24 MB % 77.70/11.34 % (3390821)Instructions burned: 1180 (million) % 77.70/11.34 % (3390833)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=889613960:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 77.70/11.34 % (3390827)Instruction limit reached! % 77.70/11.34 % (3390827)------------------------------ % 77.70/11.34 % (3390827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.70/11.34 % (3390827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.70/11.34 % (3390827)CaDiCaL version: 2.1.3 % 77.70/11.34 % (3390827)Termination reason: Instruction limit % 77.70/11.34 % (3390827)Termination phase: Saturation % 77.70/11.34 % (3390827)Time elapsed: 0.401 s % 77.70/11.34 % (3390827)Peak memory usage: 20 MB % 77.70/11.34 % (3390827)Instructions burned: 880 (million) % 77.70/11.34 % (3390835)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=48363321:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 77.70/11.34 % (3390833)Instruction limit reached! % 77.70/11.34 % (3390833)------------------------------ % 77.70/11.34 % (3390833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.70/11.34 % (3390833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.70/11.34 % (3390833)CaDiCaL version: 2.1.3 % 77.70/11.34 % (3390833)Termination reason: Instruction limit % 77.70/11.34 % (3390833)Termination phase: Finite model building preprocessing % 77.70/11.34 % (3390833)Time elapsed: 0.445 s % 77.70/11.34 % (3390833)Peak memory usage: 29 MB % 77.70/11.34 % (3390833)Instructions burned: 921 (million) % 77.70/11.34 % (3390837)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=593877538:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi) % 77.70/11.34 % (3390837)Instruction limit reached! % 77.70/11.34 % (3390837)------------------------------ % 77.70/11.34 % (3390837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.70/11.34 % (3390837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.70/11.34 % (3390837)CaDiCaL version: 2.1.3 % 77.70/11.34 % (3390837)Termination reason: Instruction limit % 77.70/11.34 % (3390837)Termination phase: Saturation % 77.70/11.34 % (3390837)Time elapsed: 0.675 s % 77.70/11.34 % (3390837)Peak memory usage: 26 MB % 77.70/11.34 % (3390837)Instructions burned: 1473 (million) % 77.70/11.34 % (3390839)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3977347399:i=6324_2978 on theBenchmark for (2978ds/6324Mi) % 77.70/11.34 % (3390835)Instruction limit reached! % 77.70/11.34 % (3390835)------------------------------ % 77.70/11.34 % (3390835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.70/11.34 % (3390835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.70/11.34 % (3390835)CaDiCaL version: 2.1.3 % 77.70/11.34 % (3390835)Termination reason: Instruction limit % 77.70/11.34 % (3390835)Termination phase: Saturation % 147.87/21.27 % (3390835)Time elapsed: 2.369 s % 147.87/21.27 % (3390835)Peak memory usage: 40 MB % 147.87/21.27 % (3390835)Instructions burned: 5133 (million) % 147.87/21.27 % (3390843)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1253669688:fmbsr=2.30978:i=2174_2964 on theBenchmark for (2964ds/2174Mi) % 147.87/21.27 % (3390843)Instruction limit reached! % 147.87/21.27 % (3390843)------------------------------ % 147.87/21.27 % (3390843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.87/21.27 % (3390843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.87/21.27 % (3390843)CaDiCaL version: 2.1.3 % 147.87/21.27 % (3390843)Termination reason: Instruction limit % 147.87/21.27 % (3390843)Termination phase: Finite model building preprocessing % 147.87/21.27 % (3390843)Time elapsed: 0.886 s % 147.87/21.27 % (3390843)Peak memory usage: 39 MB % 147.87/21.27 % (3390843)Instructions burned: 2176 (million) % 147.87/21.27 % (3390845)ott-2_1_sil=16000:newcnf=on:random_seed=4139145478:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi) % 147.87/21.27 % (3390845)Instruction limit reached! % 147.87/21.27 % (3390845)------------------------------ % 147.87/21.27 % (3390845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.87/21.27 % (3390845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.87/21.27 % (3390845)CaDiCaL version: 2.1.3 % 147.87/21.27 % (3390845)Termination reason: Instruction limit % 147.87/21.27 % (3390845)Termination phase: Saturation % 147.87/21.27 % (3390845)Time elapsed: 0.283 s % 147.87/21.27 % (3390845)Peak memory usage: 24 MB % 147.87/21.27 % (3390845)Instructions burned: 871 (million) % 147.87/21.27 % (3390847)ott+10_1_sil=32000:tgt=ground:random_seed=2714430640:i=5114:av=off_2952 on theBenchmark for (2952ds/5114Mi) % 147.87/21.27 % (3390839)Instruction limit reached! % 147.87/21.27 % (3390839)------------------------------ % 147.87/21.27 % (3390839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.87/21.27 % (3390839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.87/21.27 % (3390839)CaDiCaL version: 2.1.3 % 147.87/21.27 % (3390839)Termination reason: Instruction limit % 147.87/21.27 % (3390839)Termination phase: Finite model building preprocessing % 147.87/21.27 % (3390839)Time elapsed: 2.869 s % 147.87/21.27 % (3390839)Peak memory usage: 57 MB % 147.87/21.27 % (3390839)Instructions burned: 6325 (million) % 147.87/21.27 % (3390849)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=395343673:i=54282_2949 on theBenchmark for (2949ds/54282Mi) % 147.87/21.27 % (3390830)Instruction limit reached! % 147.87/21.27 % (3390830)------------------------------ % 147.87/21.27 % (3390830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.87/21.27 % (3390830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.87/21.27 % (3390830)CaDiCaL version: 2.1.3 % 147.87/21.27 % (3390830)Termination reason: Instruction limit % 147.87/21.27 % (3390830)Termination phase: Finite model building preprocessing % 147.87/21.27 % (3390830)Time elapsed: 4.455 s % 147.87/21.27 % (3390830)Peak memory usage: 73 MB % 147.87/21.27 % (3390830)Instructions burned: 9516 (million) % 147.87/21.27 % (3390853)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2033786274:i=3512:aac=none_2945 on theBenchmark for (2945ds/3512Mi) % 147.87/21.27 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 147.87/21.27 % Detected maximum model sizes of [2,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max] % 147.87/21.27 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 147.87/21.27 % TRYING [1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1] % 147.87/21.27 % TRYING [1,1,1,1,1,1,1,1,1,1,1,3,1,1,1,1,1,1] % 147.87/21.27 % TRYING [1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1] % 147.87/21.27 % TRYING [1,1,1,1,1,1,1,1,1,1,1,5,1,1,1,1,1,1] % 147.87/21.27 % TRYING [1,1,1,1,1,1,1,1,1,1,1,6,1,1,1,1,1,1] % 147.87/21.27 % TRYING [1,1,1,1,1,1,1,1,2,1,1,6,1,1,1,1,1,1] % 147.87/21.27 % TRYING [1,1,1,1,1,1,1,1,3,1,1,6,1,1,1,1,1,1] % 147.87/21.27 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 147.87/21.27 % Detected maximum model sizes of [2,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max] % 147.87/21.27 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 147.87/21.27 % TRYING [1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1] % 147.87/21.27 % TRYING [1,1,1,1,1,1,1,1,1,1,1,3,1,1,1,1,1,1] % 147.87/21.27 % (3390853)Instruction limit reached! % 147.87/21.27 % (3390853)------------------------------ % 147.87/21.27 % (3390853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.87/21.27 % (3390853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.61/30.82 % (3390853)CaDiCaL version: 2.1.3 % 215.61/30.82 % (3390853)Termination reason: Instruction limit % 215.61/30.82 % (3390853)Termination phase: Saturation % 215.61/30.82 % (3390853)Time elapsed: 1.531 s % 215.61/30.82 % (3390853)Peak memory usage: 36 MB % 215.61/30.82 % (3390853)Instructions burned: 3513 (million) % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,4,1,1,6,1,1,1,1,1,1] % 215.61/30.82 % (3390857)dis+21_1_sil=32000:sas=cadical:random_seed=138623022:i=3773:amm=off_2930 on theBenchmark for (2930ds/3773Mi) % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1] % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,1,1,1,5,1,1,1,1,1,1] % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,1,1,1,6,1,1,1,1,1,1] % 215.61/30.82 % (3390847)Instruction limit reached! % 215.61/30.82 % (3390847)------------------------------ % 215.61/30.82 % (3390847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.61/30.82 % (3390847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.61/30.82 % (3390847)CaDiCaL version: 2.1.3 % 215.61/30.82 % (3390847)Termination reason: Instruction limit % 215.61/30.82 % (3390847)Termination phase: Saturation % 215.61/30.82 % (3390847)Time elapsed: 2.463 s % 215.61/30.82 % (3390847)Peak memory usage: 35 MB % 215.61/30.82 % (3390847)Instructions burned: 5115 (million) % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,5,1,1,6,1,1,1,1,1,1] % 215.61/30.82 % (3390859)ott+11_1_sil=16000:gs=on:random_seed=3617318077:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2927 on theBenchmark for (2927ds/2251Mi) % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,1,2,1,6,1,1,1,1,1,1] % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,1,3,1,6,1,1,1,1,1,1] % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,6,1,1,6,1,1,1,1,1,1] % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,1,3,1,7,1,1,1,1,1,1] % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,7,1,1,6,1,1,1,1,1,1] % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,1,4,1,7,1,1,1,1,1,1] % 215.61/30.82 % (3390859)Instruction limit reached! % 215.61/30.82 % (3390859)------------------------------ % 215.61/30.82 % (3390859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.61/30.82 % (3390859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.61/30.82 % (3390859)CaDiCaL version: 2.1.3 % 215.61/30.82 % (3390859)Termination reason: Instruction limit % 215.61/30.82 % (3390859)Termination phase: Saturation % 215.61/30.82 % (3390859)Time elapsed: 1.013 s % 215.61/30.82 % (3390859)Peak memory usage: 34 MB % 215.61/30.82 % (3390859)Instructions burned: 2251 (million) % 215.61/30.82 % (3390865)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=683570042:fmbsr=1.6:i=67534_2917 on theBenchmark for (2917ds/67534Mi) % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,2,4,1,7,1,1,1,1,1,1] % 215.61/30.82 % (3390857)Instruction limit reached! % 215.61/30.82 % (3390857)------------------------------ % 215.61/30.82 % (3390857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.61/30.82 % (3390857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.61/30.82 % (3390857)CaDiCaL version: 2.1.3 % 215.61/30.82 % (3390857)Termination reason: Instruction limit % 215.61/30.82 % (3390857)Termination phase: Saturation % 215.61/30.82 % (3390857)Time elapsed: 1.821 s % 215.61/30.82 % (3390857)Peak memory usage: 39 MB % 215.61/30.82 % (3390857)Instructions burned: 3774 (million) % 215.61/30.82 % (3390867)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2378778099:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2911 on theBenchmark for (2911ds/4591Mi) % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,7,2,1,6,1,1,1,1,1,1] % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,3,4,1,7,1,1,1,1,1,1] % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,7,3,1,6,1,1,1,1,1,1] % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,4,4,1,7,1,1,1,1,1,1] % 215.61/30.82 % TRYING [1,1,1,1,1,1,1,1,7,2,1,7,1,1,1,1,1,1] % 215.61/30.82 % (3390829)Instruction limit reached! % 215.61/30.82 % (3390829)------------------------------ % 215.61/30.82 % (3390829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.61/30.82 % (3390829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.61/30.82 % (3390829)CaDiCaL version: 2.1.3 % 215.61/30.82 % (3390829)Termination reason: Instruction limit % 215.61/30.82 % (3390829)Termination phase: Finite model building SAT solving % 215.61/30.82 % (3390829)Time elapsed: 9.886 s % 215.61/30.82 % (3390829)Peak memory usage: 137 MB % 215.61/30.82 % (3390829)Instructions burned: 22061 (million) % 215.61/30.82 % (3390871)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=725962013:i=29340_2891 on theBenchmark for (2891ds/29340Mi) % 215.61/30.82 % (3390867)Instruction limit reached! % 215.61/30.82 % (3390867)------------------------------ % 215.61/30.82 % (3390867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.07/37.78 % (3390867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.07/37.78 % (3390867)CaDiCaL version: 2.1.3 % 264.07/37.78 % (3390867)Termination reason: Instruction limit % 264.07/37.78 % (3390867)Termination phase: Saturation % 264.07/37.78 % (3390867)Time elapsed: 2.316 s % 264.07/37.78 % (3390867)Peak memory usage: 81 MB % 264.07/37.78 % (3390867)Instructions burned: 4591 (million) % 264.07/37.78 % (3390873)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1008263339:i=5211_2888 on theBenchmark for (2888ds/5211Mi) % 264.07/37.78 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 264.07/37.78 % Detected maximum model sizes of [2,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,1,1,1,3,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,1,1,1,5,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,1,1,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,7,4,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,2,1,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,3,1,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,4,1,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,5,1,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,2,1,7,4,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,6,1,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [7] % 264.07/37.78 % (3390873)Instruction limit reached! % 264.07/37.78 % (3390873)------------------------------ % 264.07/37.78 % (3390873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.07/37.78 % (3390873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.07/37.78 % (3390873)CaDiCaL version: 2.1.3 % 264.07/37.78 % (3390873)Termination reason: Instruction limit % 264.07/37.78 % (3390873)Termination phase: Saturation % 264.07/37.78 % (3390873)Time elapsed: 2.279 s % 264.07/37.78 % (3390873)Peak memory usage: 43 MB % 264.07/37.78 % (3390873)Instructions burned: 5212 (million) % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,7,1,1,6,1,1,1,1,1,1] % 264.07/37.78 % (3390877)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1401823479:i=5497:nm=2_2865 on theBenchmark for (2865ds/5497Mi) % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,8,4,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,7,2,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,7,3,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,2,1,2,1,7,4,1,6,1,1,1,1,1,1] % 264.07/37.78 % (3390877)Instruction limit reached! % 264.07/37.78 % (3390877)------------------------------ % 264.07/37.78 % (3390877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.07/37.78 % (3390877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.07/37.78 % (3390877)CaDiCaL version: 2.1.3 % 264.07/37.78 % (3390877)Termination reason: Instruction limit % 264.07/37.78 % (3390877)Termination phase: Finite model building preprocessing % 264.07/37.78 % (3390877)Time elapsed: 2.464 s % 264.07/37.78 % (3390877)Peak memory usage: 52 MB % 264.07/37.78 % (3390877)Instructions burned: 5497 (million) % 264.07/37.78 % (3390883)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3806084985:fmbsr=2:i=46332_2840 on theBenchmark for (2840ds/46332Mi) % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,7,2,1,7,1,1,1,1,1,1] % 264.07/37.78 % (3390883)Cannot represent all propositional literals internally % 264.07/37.78 % (3390883)Refutation not found, incomplete strategy % 264.07/37.78 % (3390883)------------------------------ % 264.07/37.78 % (3390883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.07/37.78 % (3390883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.07/37.78 % (3390883)CaDiCaL version: 2.1.3 % 264.07/37.78 % (3390883)Termination reason: Refutation not found, incomplete strategy % 264.07/37.78 % (3390883)Time elapsed: 0.432 s % 264.07/37.78 % (3390883)Peak memory usage: 24 MB % 264.07/37.78 % (3390883)Instructions burned: 992 (million) % 264.07/37.78 % (3390883)------------------------------ % 264.07/37.78 % (3390883)------------------------------ % 264.07/37.78 % (3390885)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2707672610:i=14071_2835 on theBenchmark for (2835ds/14071Mi) % 264.07/37.78 % TRYING [1,1,1,1,1,1,2,1,8,4,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,7,4,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,2,1,7,4,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,2,1,2,1,2,1,7,4,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [2,1,2,1,2,1,2,1,7,4,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,1,1,1,1,8,4,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [2,1,2,1,2,1,2,1,7,5,1,6,1,1,1,1,1,1] % 264.07/37.78 % TRYING [1,1,1,1,2,1,2,1,7,4,1,6,1,1,1,1,1,1] % 300.15/42.84 % TRYING [1,1,1,1,1,1,1,1,9,4,1,6,1,1,1,1,1,1] % 300.15/42.84 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 300.15/42.84 % Detected maximum model sizes of [2,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max] % 300.15/42.84 % fmb_start_size (= 12) larger than a detected sort maximum size! % 300.15/42.84 % (3390885)Refutation not found, incomplete strategy % 300.15/42.84 % (3390885)------------------------------ % 300.15/42.84 % (3390885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.84 % (3390885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.84 % (3390885)CaDiCaL version: 2.1.3 % 300.15/42.84 % (3390885)Termination reason: Refutation not found, incomplete strategy % 300.15/42.84 % (3390885)Time elapsed: 5.761 s % 300.15/42.84 % (3390885)Peak memory usage: 95 MB % 300.15/42.84 % (3390885)Instructions burned: 13847 (million) % 300.15/42.84 % (3390885)------------------------------ % 300.15/42.84 % (3390885)------------------------------ % 300.15/42.84 % (3390895)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2681589311:i=22565:add=on:rawr=on_2777 on theBenchmark for (2777ds/22565Mi) % 300.15/42.84 % TRYING [1,1,1,1,1,1,2,1,8,4,1,6,1,1,1,1,1,1] % 300.15/42.84 % TRYING [1,1,2,1,2,1,2,1,7,4,1,6,1,1,1,1,1,1] % 300.15/42.84 % TRYING [2,1,2,1,2,1,2,1,7,6,1,6,1,1,1,1,1,1] % 300.15/42.84 % (3390871)Instruction limit reached! % 300.15/42.84 % (3390871)------------------------------ % 300.15/42.84 % (3390871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.84 % (3390871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.84 % (3390871)CaDiCaL version: 2.1.3 % 300.15/42.84 % (3390871)Termination reason: Instruction limit % 300.15/42.84 % (3390871)Termination phase: Saturation % 300.15/42.84 % (3390871)Time elapsed: 13.617 s % 300.15/42.84 % (3390871)Peak memory usage: 220 MB % 300.15/42.84 % (3390871)Instructions burned: 29341 (million) % 300.15/42.84 % (3390897)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1788215391:i=8173:av=off_2755 on theBenchmark for (2755ds/8173Mi) % 300.15/42.84 % TRYING [2,1,2,1,2,1,2,1,7,4,1,6,1,1,1,1,1,1] % 300.15/42.84 % TRYING [2,1,2,1,2,1,2,1,7,5,1,7,1,1,1,1,1,1] % 300.15/42.84 % TRYING [2,1,2,1,2,1,2,1,7,5,1,6,1,1,1,1,1,1] % 300.15/42.84 % TRYING [2,1,2,1,2,1,2,1,7,7,1,6,1,1,1,1,1,1] % 300.15/42.84 % (3390849)Instruction limit reached! % 300.15/42.84 % (3390849)------------------------------ % 300.15/42.84 % (3390849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.84 % (3390849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.84 % (3390849)CaDiCaL version: 2.1.3 % 300.15/42.84 % (3390849)Termination reason: Instruction limit % 300.15/42.84 % (3390849)Termination phase: Finite model building constraint generation % 300.15/42.84 % (3390849)Time elapsed: 22.495 s % 300.15/42.84 % (3390849)Peak memory usage: 458 MB % 300.15/42.84 % (3390849)Instructions burned: 54283 (million) % 300.15/42.84 % (3390903)dis+10_16:1_sil=16000:random_seed=1150203495:i=9155:fsr=off_2723 on theBenchmark for (2723ds/9155Mi) % 300.15/42.84 % (3390897)Instruction limit reached! % 300.15/42.84 % (3390897)------------------------------ % 300.15/42.84 % (3390897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.84 % (3390897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.84 % (3390897)CaDiCaL version: 2.1.3 % 300.15/42.84 % (3390897)Termination reason: Instruction limit % 300.15/42.84 % (3390897)Termination phase: Saturation % 300.15/42.84 % (3390897)Time elapsed: 3.764 s % 300.15/42.84 % (3390897)Peak memory usage: 53 MB % 300.15/42.84 % (3390897)Instructions burned: 8176 (million) % 300.15/42.84 % (3390991)ott-3_8_sil=64000:random_seed=1814088605:i=20139:bs=on_2717 on theBenchmark for (2717ds/20139Mi) % 300.15/42.84 % TRYING [1,1,1,1,2,1,2,1,8,4,1,6,1,1,1,1,1,1] % 300.15/42.84 % TRYING [1,1,1,1,1,1,2,1,9,4,1,6,1,1,1,1,1,1] % 300.15/42.84 % TRYING [2,1,2,1,2,1,2,1,8,5,1,7,1,1,1,1,1,1] % 300.15/42.84 % (3390903)Instruction limit reached! % 300.15/42.84 % (3390903)------------------------------ % 300.15/42.84 % (3390903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.84 % (3390903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.84 % (3390903)CaDiCaL version: 2.1.3 % 300.15/42.84 % (3390903)Termination reason: Instruction limit % 300.15/42.84 % (3390903)Termination phase: Saturation % 300.15/42.84 % (3390903)Time elapsed: 2.934 s % 300.15/42.84 % (3390903)Peak memory usage: 68 MB % 300.15/42.84 % (3390903)Instructions burned: 9156 (million) % 300.15/42.84 % (3391063)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=o % 300.15/42.84 Terminated % 300.15/42.84 % Vampire exiting %------------------------------------------------------------------------------