%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW470_30 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:05 PM UTC 2026 % Result : Timeout 300.06s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW470_30 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.16 % Computer : n004.cluster.edu % 0.09/0.16 % Model : x86_64 x86_64 % 0.09/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.16 % Memory : 8046.5625MB % 0.09/0.16 % OS : Linux 6.8.0-71-generic % 0.09/0.16 % CPULimit : 300 % 0.09/0.16 % WCLimit : 300 % 0.09/0.16 % DateTime : Mon Sep 28 14:02:37 UTC 2026 % 0.09/0.16 % CPUTime : % 0.09/0.16 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 Running first-order model finding % 0.09/0.20 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 % 29.09/4.43 % (367801)Will run a generic schedule for satisfiability detection. % 29.09/4.43 % (367815)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3838754795:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 29.09/4.43 % (367819)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=988429394:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 29.09/4.43 % (367814)% WARNING: option uhcvi not known. % 29.09/4.43 % (367813)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=782476398_2998 on theBenchmark for (2998ds/0Mi) % 29.09/4.43 % (367816)dis+10_1_sil=32000:sp=arity:random_seed=907451344:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 29.09/4.43 % (367817)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=543689043:i=116_2998 on theBenchmark for (2998ds/116Mi) % 29.09/4.43 % (367818)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2582895620:i=131_2998 on theBenchmark for (2998ds/131Mi) % 29.09/4.43 % (367814)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=140522763:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 29.09/4.43 % (367819)Instruction limit reached! % 29.09/4.43 % (367819)------------------------------ % 29.09/4.43 % (367819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.09/4.43 % (367819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.09/4.43 % (367819)CaDiCaL version: 2.1.3 % 29.09/4.43 % (367819)Termination reason: Instruction limit % 29.09/4.43 % (367819)Termination phase: Saturation % 29.09/4.43 % (367819)Time elapsed: 0.086 s % 29.09/4.43 % (367819)Peak memory usage: 16 MB % 29.09/4.43 % (367819)Instructions burned: 159 (million) % 29.09/4.43 % (367816)Instruction limit reached! % 29.09/4.43 % (367816)------------------------------ % 29.09/4.43 % (367816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.09/4.43 % (367816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.09/4.43 % (367816)CaDiCaL version: 2.1.3 % 29.09/4.43 % (367816)Termination reason: Instruction limit % 29.09/4.43 % (367816)Termination phase: Property scanning % 29.09/4.43 % (367816)Time elapsed: 0.083 s % 29.09/4.43 % (367816)Peak memory usage: 13 MB % 29.09/4.43 % (367816)Instructions burned: 103 (million) % 29.09/4.43 % (367817)Instruction limit reached! % 29.09/4.43 % (367817)------------------------------ % 29.09/4.43 % (367817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.09/4.43 % (367817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.09/4.43 % (367817)CaDiCaL version: 2.1.3 % 29.09/4.43 % (367817)Termination reason: Instruction limit % 29.09/4.43 % (367817)Termination phase: Blocked clause elimination % 29.09/4.43 % (367817)Time elapsed: 0.096 s % 29.09/4.43 % (367817)Peak memory usage: 14 MB % 29.09/4.43 % (367817)Instructions burned: 117 (million) % 29.09/4.43 % (367833)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2157828846:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 29.09/4.43 % (367832)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2820809066:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi) % 29.09/4.43 % (367818)Instruction limit reached! % 29.09/4.43 % (367818)------------------------------ % 29.09/4.43 % (367818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.09/4.43 % (367818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.09/4.43 % (367818)CaDiCaL version: 2.1.3 % 29.09/4.43 % (367818)Termination reason: Instruction limit % 29.09/4.43 % (367818)Termination phase: Saturation % 29.09/4.43 % (367818)Time elapsed: 0.112 s % 29.09/4.43 % (367818)Peak memory usage: 15 MB % 29.09/4.43 % (367818)Instructions burned: 132 (million) % 29.09/4.43 % (367835)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=2736094840:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 29.09/4.43 % (367840)ott-21_1_sil=16000:fs=off:random_seed=3413822689:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 29.09/4.43 % (367833)Instruction limit reached! % 29.09/4.43 % (367833)------------------------------ % 29.09/4.43 % (367833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.09/4.43 % (367833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.09/4.43 % (367833)CaDiCaL version: 2.1.3 % 29.09/4.43 % (367833)Termination reason: Instruction limit % 67.35/9.89 % (367833)Termination phase: Blocked clause elimination % 67.35/9.89 % (367833)Time elapsed: 0.108 s % 67.35/9.89 % (367833)Peak memory usage: 14 MB % 67.35/9.89 % (367833)Instructions burned: 137 (million) % 67.35/9.89 % (367844)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2546006750:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi) % 67.35/9.89 % (367840)Instruction limit reached! % 67.35/9.89 % (367840)------------------------------ % 67.35/9.89 % (367840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.35/9.89 % (367840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.35/9.89 % (367840)CaDiCaL version: 2.1.3 % 67.35/9.89 % (367840)Termination reason: Instruction limit % 67.35/9.89 % (367840)Termination phase: Saturation % 67.35/9.89 % (367840)Time elapsed: 0.163 s % 67.35/9.89 % (367840)Peak memory usage: 15 MB % 67.35/9.89 % (367840)Instructions burned: 181 (million) % 67.35/9.89 % (367847)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2680216270:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 67.35/9.89 % (367832)Instruction limit reached! % 67.35/9.89 % (367832)------------------------------ % 67.35/9.89 % (367832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.35/9.89 % (367832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.35/9.89 % (367832)CaDiCaL version: 2.1.3 % 67.35/9.89 % (367832)Termination reason: Instruction limit % 67.35/9.89 % (367832)Termination phase: Finite model building preprocessing % 67.35/9.89 % (367832)Time elapsed: 0.566 s % 67.35/9.89 % (367832)Peak memory usage: 17 MB % 67.35/9.89 % (367832)Instructions burned: 714 (million) % 67.35/9.89 % (367844)Instruction limit reached! % 67.35/9.89 % (367844)------------------------------ % 67.35/9.89 % (367844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.35/9.89 % (367844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.35/9.89 % (367844)CaDiCaL version: 2.1.3 % 67.35/9.89 % (367844)Termination reason: Instruction limit % 67.35/9.89 % (367844)Termination phase: Saturation % 67.35/9.89 % (367844)Time elapsed: 0.445 s % 67.35/9.89 % (367844)Peak memory usage: 17 MB % 67.35/9.89 % (367844)Instructions burned: 477 (million) % 67.35/9.89 % (367855)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4200055740:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi) % 67.35/9.89 % (367854)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2042584713:i=1179_2991 on theBenchmark for (2991ds/1179Mi) % 67.35/9.89 % (367835)Instruction limit reached! % 67.35/9.89 % (367835)------------------------------ % 67.35/9.89 % (367835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.35/9.89 % (367835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.35/9.89 % (367835)CaDiCaL version: 2.1.3 % 67.35/9.89 % (367835)Termination reason: Instruction limit % 67.35/9.89 % (367835)Termination phase: Saturation % 67.35/9.89 % (367835)Time elapsed: 0.599 s % 67.35/9.89 % (367835)Peak memory usage: 20 MB % 67.35/9.89 % (367835)Instructions burned: 684 (million) % 67.35/9.89 % (367858)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=3010334937:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi) % 67.35/9.89 % (367847)Instruction limit reached! % 67.35/9.89 % (367847)------------------------------ % 67.35/9.89 % (367847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.35/9.89 % (367847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.35/9.89 % (367847)CaDiCaL version: 2.1.3 % 67.35/9.89 % (367847)Termination reason: Instruction limit % 67.35/9.89 % (367847)Termination phase: Finite model building preprocessing % 67.35/9.89 % (367847)Time elapsed: 0.546 s % 67.35/9.89 % (367847)Peak memory usage: 27 MB % 67.35/9.89 % (367847)Instructions burned: 866 (million) % 67.35/9.89 % (367860)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1398260006:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi) % 67.35/9.89 % (367858)Instruction limit reached! % 67.35/9.89 % (367858)------------------------------ % 67.35/9.89 % (367858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 67.35/9.89 % (367858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.35/9.89 % (367858)CaDiCaL version: 2.1.3 % 67.35/9.89 % (367858)Termination reason: Instruction limit % 131.85/19.02 % (367858)Termination phase: Saturation % 131.85/19.02 % (367858)Time elapsed: 0.394 s % 131.85/19.02 % (367858)Peak memory usage: 19 MB % 131.85/19.02 % (367858)Instructions burned: 692 (million) % 131.85/19.02 % (367855)Instruction limit reached! % 131.85/19.02 % (367855)------------------------------ % 131.85/19.02 % (367855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.85/19.02 % (367855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.85/19.02 % (367855)CaDiCaL version: 2.1.3 % 131.85/19.02 % (367855)Termination reason: Instruction limit % 131.85/19.02 % (367855)Termination phase: Finite model building preprocessing % 131.85/19.02 % (367855)Time elapsed: 0.444 s % 131.85/19.02 % (367855)Peak memory usage: 27 MB % 131.85/19.02 % (367855)Instructions burned: 891 (million) % 131.85/19.02 % (367885)fmb+10_1_sil=64000:random_seed=1820374417:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi) % 131.85/19.02 % (367888)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1628996280:i=9515:nm=5_2987 on theBenchmark for (2987ds/9515Mi) % 131.85/19.02 % (367860)Instruction limit reached! % 131.85/19.02 % (367860)------------------------------ % 131.85/19.02 % (367860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.85/19.02 % (367860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.85/19.02 % (367860)CaDiCaL version: 2.1.3 % 131.85/19.02 % (367860)Termination reason: Instruction limit % 131.85/19.02 % (367860)Termination phase: Saturation % 131.85/19.02 % (367860)Time elapsed: 0.437 s % 131.85/19.02 % (367860)Peak memory usage: 20 MB % 131.85/19.02 % (367860)Instructions burned: 879 (million) % 131.85/19.02 % (367854)Instruction limit reached! % 131.85/19.02 % (367854)------------------------------ % 131.85/19.02 % (367854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.85/19.02 % (367854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.85/19.02 % (367854)CaDiCaL version: 2.1.3 % 131.85/19.02 % (367854)Termination reason: Instruction limit % 131.85/19.02 % (367854)Termination phase: Saturation % 131.85/19.02 % (367854)Time elapsed: 0.651 s % 131.85/19.02 % (367854)Peak memory usage: 24 MB % 131.85/19.02 % (367854)Instructions burned: 1179 (million) % 131.85/19.02 % (367957)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1501028296:fmbsr=1.7:i=920_2985 on theBenchmark for (2985ds/920Mi) % 131.85/19.02 % (367963)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2162487064:i=5131_2984 on theBenchmark for (2984ds/5131Mi) % 131.85/19.02 % (367957)Instruction limit reached! % 131.85/19.02 % (367957)------------------------------ % 131.85/19.02 % (367957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.85/19.02 % (367957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.85/19.02 % (367957)CaDiCaL version: 2.1.3 % 131.85/19.02 % (367957)Termination reason: Instruction limit % 131.85/19.02 % (367957)Termination phase: Finite model building preprocessing % 131.85/19.02 % (367957)Time elapsed: 0.461 s % 131.85/19.02 % (367957)Peak memory usage: 27 MB % 131.85/19.02 % (367957)Instructions burned: 920 (million) % 131.85/19.02 % (368023)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2376867709:i=1472:ins=7:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/1472Mi) % 131.85/19.02 % (368023)Instruction limit reached! % 131.85/19.02 % (368023)------------------------------ % 131.85/19.02 % (368023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.85/19.02 % (368023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.85/19.02 % (368023)CaDiCaL version: 2.1.3 % 131.85/19.02 % (368023)Termination reason: Instruction limit % 131.85/19.02 % (368023)Termination phase: Saturation % 131.85/19.02 % (368023)Time elapsed: 0.778 s % 131.85/19.02 % (368023)Peak memory usage: 28 MB % 131.85/19.02 % (368023)Instructions burned: 1475 (million) % 131.85/19.02 % (368025)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3255974051:i=6324_2972 on theBenchmark for (2972ds/6324Mi) % 131.85/19.02 % (367963)Instruction limit reached! % 131.85/19.02 % (367963)------------------------------ % 131.85/19.02 % (367963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.85/19.02 % (367963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.85/19.02 % (367963)CaDiCaL version: 2.1.3 % 131.85/19.02 % (367963)Termination reason: Instruction limit % 131.85/19.02 % (367963)Termination phase: Saturation % 131.85/19.02 % (367963)Time elapsed: 2.694 s % 131.85/19.02 % (367963)Peak memory usage: 43 MB % 131.85/19.02 % (367963)Instructions burned: 5133 (million) % 195.86/32.54 % (368027)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3046117096:fmbsr=2.30978:i=2174_2957 on theBenchmark for (2957ds/2174Mi) % 195.86/32.54 % (368027)Instruction limit reached! % 195.86/32.54 % (368027)------------------------------ % 195.86/32.54 % (368027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.86/32.54 % (368027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.86/32.54 % (368027)CaDiCaL version: 2.1.3 % 195.86/32.54 % (368027)Termination reason: Instruction limit % 195.86/32.54 % (368027)Termination phase: Finite model building preprocessing % 195.86/32.54 % (368027)Time elapsed: 1.043 s % 195.86/32.54 % (368027)Peak memory usage: 34 MB % 195.86/32.54 % (368027)Instructions burned: 2174 (million) % 195.86/32.54 % (368029)ott-2_1_sil=16000:newcnf=on:random_seed=2792482488:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2947 on theBenchmark for (2947ds/869Mi) % 195.86/32.54 % (367888)Instruction limit reached! % 195.86/32.54 % (367888)------------------------------ % 195.86/32.54 % (367888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.86/32.54 % (367888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.86/32.54 % (367888)CaDiCaL version: 2.1.3 % 195.86/32.54 % (367888)Termination reason: Instruction limit % 195.86/32.54 % (367888)Termination phase: Finite model building preprocessing % 195.86/32.54 % (367888)Time elapsed: 4.367 s % 195.86/32.54 % (367888)Peak memory usage: 82 MB % 195.86/32.54 % (367888)Instructions burned: 9515 (million) % 195.86/32.54 % (368031)ott+10_1_sil=32000:tgt=ground:random_seed=3009560202:i=5114:av=off_2943 on theBenchmark for (2943ds/5114Mi) % 195.86/32.54 % (368025)Instruction limit reached! % 195.86/32.54 % (368025)------------------------------ % 195.86/32.54 % (368025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.86/32.54 % (368025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.86/32.54 % (368025)CaDiCaL version: 2.1.3 % 195.86/32.54 % (368025)Termination reason: Instruction limit % 195.86/32.54 % (368025)Termination phase: Finite model building preprocessing % 195.86/32.54 % (368025)Time elapsed: 2.920 s % 195.86/32.54 % (368025)Peak memory usage: 65 MB % 195.86/32.54 % (368025)Instructions burned: 6326 (million) % 195.86/32.54 % (368033)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1531194299:i=54282_2942 on theBenchmark for (2942ds/54282Mi) % 195.86/32.54 % (368029)Instruction limit reached! % 195.86/32.54 % (368029)------------------------------ % 195.86/32.54 % (368029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.86/32.54 % (368029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.86/32.54 % (368029)CaDiCaL version: 2.1.3 % 195.86/32.54 % (368029)Termination reason: Instruction limit % 195.86/32.54 % (368029)Termination phase: Saturation % 195.86/32.54 % (368029)Time elapsed: 0.429 s % 195.86/32.54 % (368029)Peak memory usage: 21 MB % 195.86/32.54 % (368029)Instructions burned: 870 (million) % 195.86/32.54 % (368035)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3826300214:i=3512:aac=none_2942 on theBenchmark for (2942ds/3512Mi) % 195.86/32.54 % (368035)Instruction limit reached! % 195.86/32.54 % (368035)------------------------------ % 195.86/32.54 % (368035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.86/32.54 % (368035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.86/32.54 % (368035)CaDiCaL version: 2.1.3 % 195.86/32.54 % (368035)Termination reason: Instruction limit % 195.86/32.54 % (368035)Termination phase: Saturation % 195.86/32.54 % (368035)Time elapsed: 2.089 s % 195.86/32.54 % (368035)Peak memory usage: 38 MB % 195.86/32.54 % (368035)Instructions burned: 3512 (million) % 195.86/32.54 % (368037)dis+21_1_sil=32000:sas=cadical:random_seed=92874594:i=3773:amm=off_2921 on theBenchmark for (2921ds/3773Mi) % 195.86/32.54 % (368031)Instruction limit reached! % 195.86/32.54 % (368031)------------------------------ % 195.86/32.54 % (368031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.86/32.54 % (368031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.86/32.54 % (368031)CaDiCaL version: 2.1.3 % 195.86/32.54 % (368031)Termination reason: Instruction limit % 195.86/32.54 % (368031)Termination phase: Saturation % 195.86/32.54 % (368031)Time elapsed: 2.674 s % 195.86/32.54 % (368031)Peak memory usage: 33 MB % 195.86/32.54 % (368031)Instructions burned: 5114 (million) % 195.86/32.54 % (368039)ott+11_1_sil=16000:gs=on:random_seed=2505831092:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2916 on theBenchmark for (2916ds/2251Mi) % 195.86/32.54 %Terminated % 300.06/42.64 % Vampire exiting % 300.06/42.64 Terminated %------------------------------------------------------------------------------