%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW471_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 : n026.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.56s 42.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW471_30 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.21 % Computer : n026.cluster.edu % 0.09/0.21 % Model : x86_64 x86_64 % 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.21 % Memory : 8046.5625MB % 0.09/0.21 % OS : Linux 6.8.0-71-generic % 0.09/0.21 % CPULimit : 300 % 0.09/0.21 % WCLimit : 300 % 0.09/0.21 % DateTime : Mon Sep 28 14:06:12 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.25 Running first-order model finding % 0.09/0.25 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 % 23.23/3.60 % (3865085)Will run a generic schedule for satisfiability detection. % 23.23/3.60 % (3865094)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4107628216:i=116_2999 on theBenchmark for (2999ds/116Mi) % 23.23/3.60 % (3865091)% WARNING: option uhcvi not known. % 23.23/3.60 % (3865090)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1232708987_2999 on theBenchmark for (2999ds/0Mi) % 23.23/3.60 % (3865092)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3747763088:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 23.23/3.60 % (3865091)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=107619302:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 23.23/3.60 % (3865093)dis+10_1_sil=32000:sp=arity:random_seed=3868063792:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 23.23/3.60 % (3865095)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=137955170:i=131_2999 on theBenchmark for (2999ds/131Mi) % 23.23/3.60 % (3865096)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1727373318:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 23.23/3.60 % (3865094)Instruction limit reached! % 23.23/3.60 % (3865094)------------------------------ % 23.23/3.60 % (3865094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.23/3.60 % (3865094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.23/3.60 % (3865094)CaDiCaL version: 2.1.3 % 23.23/3.60 % (3865094)Termination reason: Instruction limit % 23.23/3.60 % (3865094)Termination phase: Blocked clause elimination % 23.23/3.60 % (3865094)Time elapsed: 0.030 s % 23.23/3.60 % (3865094)Peak memory usage: 14 MB % 23.23/3.60 % (3865094)Instructions burned: 118 (million) % 23.23/3.60 % (3865104)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3338969859:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 23.23/3.60 % (3865093)Instruction limit reached! % 23.23/3.60 % (3865093)------------------------------ % 23.23/3.60 % (3865093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.23/3.60 % (3865093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.23/3.60 % (3865093)CaDiCaL version: 2.1.3 % 23.23/3.60 % (3865093)Termination reason: Instruction limit % 23.23/3.60 % (3865093)Termination phase: Property scanning % 23.23/3.60 % (3865093)Time elapsed: 0.048 s % 23.23/3.60 % (3865093)Peak memory usage: 14 MB % 23.23/3.60 % (3865093)Instructions burned: 103 (million) % 23.23/3.60 % (3865095)Instruction limit reached! % 23.23/3.60 % (3865095)------------------------------ % 23.23/3.60 % (3865095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.23/3.60 % (3865095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.23/3.60 % (3865095)CaDiCaL version: 2.1.3 % 23.23/3.60 % (3865095)Termination reason: Instruction limit % 23.23/3.60 % (3865095)Termination phase: Saturation % 23.23/3.60 % (3865095)Time elapsed: 0.062 s % 23.23/3.60 % (3865095)Peak memory usage: 15 MB % 23.23/3.60 % (3865095)Instructions burned: 132 (million) % 23.23/3.60 % (3865106)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1471737760:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 23.23/3.60 % (3865096)Instruction limit reached! % 23.23/3.60 % (3865096)------------------------------ % 23.23/3.60 % (3865096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.23/3.60 % (3865096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.23/3.60 % (3865096)CaDiCaL version: 2.1.3 % 23.23/3.60 % (3865096)Termination reason: Instruction limit % 23.23/3.60 % (3865096)Termination phase: Saturation % 23.23/3.60 % (3865096)Time elapsed: 0.079 s % 23.23/3.60 % (3865096)Peak memory usage: 15 MB % 23.23/3.60 % (3865096)Instructions burned: 159 (million) % 23.23/3.60 % (3865107)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=4146483071:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 23.23/3.60 % (3865109)ott-21_1_sil=16000:fs=off:random_seed=2136645736:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 23.23/3.60 % (3865106)Instruction limit reached! % 23.23/3.60 % (3865106)------------------------------ % 23.23/3.60 % (3865106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.23/3.60 % (3865106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.70 % (3865106)CaDiCaL version: 2.1.3 % 45.24/6.70 % (3865106)Termination reason: Instruction limit % 45.24/6.70 % (3865106)Termination phase: Blocked clause elimination % 45.24/6.70 % (3865106)Time elapsed: 0.060 s % 45.24/6.70 % (3865106)Peak memory usage: 14 MB % 45.24/6.70 % (3865106)Instructions burned: 133 (million) % 45.24/6.70 % (3865112)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4107677224:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 45.24/6.70 % (3865109)Instruction limit reached! % 45.24/6.70 % (3865109)------------------------------ % 45.24/6.70 % (3865109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.70 % (3865109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.70 % (3865109)CaDiCaL version: 2.1.3 % 45.24/6.70 % (3865109)Termination reason: Instruction limit % 45.24/6.70 % (3865109)Termination phase: Saturation % 45.24/6.70 % (3865109)Time elapsed: 0.083 s % 45.24/6.70 % (3865109)Peak memory usage: 15 MB % 45.24/6.70 % (3865109)Instructions burned: 181 (million) % 45.24/6.70 % (3865104)Instruction limit reached! % 45.24/6.70 % (3865104)------------------------------ % 45.24/6.70 % (3865104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.70 % (3865104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.70 % (3865104)CaDiCaL version: 2.1.3 % 45.24/6.70 % (3865104)Termination reason: Instruction limit % 45.24/6.70 % (3865104)Termination phase: Finite model building preprocessing % 45.24/6.70 % (3865104)Time elapsed: 0.156 s % 45.24/6.70 % (3865104)Peak memory usage: 15 MB % 45.24/6.70 % (3865104)Instructions burned: 717 (million) % 45.24/6.70 % (3865115)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=135920640:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 45.24/6.70 % (3865114)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=712304244:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 45.24/6.70 % (3865112)Instruction limit reached! % 45.24/6.70 % (3865112)------------------------------ % 45.24/6.70 % (3865112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.70 % (3865112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.70 % (3865112)CaDiCaL version: 2.1.3 % 45.24/6.70 % (3865112)Termination reason: Instruction limit % 45.24/6.70 % (3865112)Termination phase: Saturation % 45.24/6.70 % (3865112)Time elapsed: 0.262 s % 45.24/6.70 % (3865112)Peak memory usage: 17 MB % 45.24/6.70 % (3865112)Instructions burned: 478 (million) % 45.24/6.70 % (3865118)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4029276532:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 45.24/6.70 % (3865107)Instruction limit reached! % 45.24/6.70 % (3865107)------------------------------ % 45.24/6.70 % (3865107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.70 % (3865107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.70 % (3865107)CaDiCaL version: 2.1.3 % 45.24/6.70 % (3865107)Termination reason: Instruction limit % 45.24/6.70 % (3865107)Termination phase: Saturation % 45.24/6.70 % (3865107)Time elapsed: 0.365 s % 45.24/6.70 % (3865107)Peak memory usage: 21 MB % 45.24/6.70 % (3865107)Instructions burned: 684 (million) % 45.24/6.70 % (3865120)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=2335650689: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) % 45.24/6.70 % (3865115)Instruction limit reached! % 45.24/6.70 % (3865115)------------------------------ % 45.24/6.70 % (3865115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.70 % (3865115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.70 % (3865115)CaDiCaL version: 2.1.3 % 45.24/6.70 % (3865115)Termination reason: Instruction limit % 45.24/6.70 % (3865115)Termination phase: Saturation % 45.24/6.70 % (3865115)Time elapsed: 0.350 s % 45.24/6.70 % (3865115)Peak memory usage: 26 MB % 45.24/6.70 % (3865115)Instructions burned: 1180 (million) % 45.24/6.70 % (3865122)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=213777913:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 45.24/6.70 % (3865114)Instruction limit reached! % 45.24/6.70 % (3865114)------------------------------ % 45.24/6.70 % (3865114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.70 % (3865114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.29/16.31 % (3865114)CaDiCaL version: 2.1.3 % 113.29/16.31 % (3865114)Termination reason: Instruction limit % 113.29/16.31 % (3865114)Termination phase: Finite model building preprocessing % 113.29/16.31 % (3865114)Time elapsed: 0.424 s % 113.29/16.31 % (3865114)Peak memory usage: 27 MB % 113.29/16.31 % (3865114)Instructions burned: 865 (million) % 113.29/16.31 % (3865124)fmb+10_1_sil=64000:random_seed=4031079205:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 113.29/16.31 % (3865122)Instruction limit reached! % 113.29/16.31 % (3865122)------------------------------ % 113.29/16.31 % (3865122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.29/16.31 % (3865122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.29/16.31 % (3865122)CaDiCaL version: 2.1.3 % 113.29/16.31 % (3865122)Termination reason: Instruction limit % 113.29/16.31 % (3865122)Termination phase: Saturation % 113.29/16.31 % (3865122)Time elapsed: 0.231 s % 113.29/16.31 % (3865122)Peak memory usage: 21 MB % 113.29/16.31 % (3865122)Instructions burned: 883 (million) % 113.29/16.31 % (3865126)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2825114713:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 113.29/16.31 % (3865118)Instruction limit reached! % 113.29/16.31 % (3865118)------------------------------ % 113.29/16.31 % (3865118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.29/16.31 % (3865118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.29/16.31 % (3865118)CaDiCaL version: 2.1.3 % 113.29/16.31 % (3865118)Termination reason: Instruction limit % 113.29/16.31 % (3865118)Termination phase: Finite model building preprocessing % 113.29/16.31 % (3865118)Time elapsed: 0.439 s % 113.29/16.31 % (3865118)Peak memory usage: 27 MB % 113.29/16.31 % (3865118)Instructions burned: 889 (million) % 113.29/16.31 % (3865120)Instruction limit reached! % 113.29/16.31 % (3865120)------------------------------ % 113.29/16.31 % (3865120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.29/16.31 % (3865120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.29/16.31 % (3865120)CaDiCaL version: 2.1.3 % 113.29/16.31 % (3865120)Termination reason: Instruction limit % 113.29/16.31 % (3865120)Termination phase: Saturation % 113.29/16.31 % (3865120)Time elapsed: 0.411 s % 113.29/16.31 % (3865120)Peak memory usage: 20 MB % 113.29/16.31 % (3865120)Instructions burned: 693 (million) % 113.29/16.31 % (3865128)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4163453964:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 113.29/16.31 % (3865129)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1950035112:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 113.29/16.31 % (3865128)Instruction limit reached! % 113.29/16.31 % (3865128)------------------------------ % 113.29/16.31 % (3865128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.29/16.31 % (3865128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.29/16.31 % (3865128)CaDiCaL version: 2.1.3 % 113.29/16.31 % (3865128)Termination reason: Instruction limit % 113.29/16.31 % (3865128)Termination phase: Finite model building preprocessing % 113.29/16.31 % (3865128)Time elapsed: 0.456 s % 113.29/16.31 % (3865128)Peak memory usage: 27 MB % 113.29/16.31 % (3865128)Instructions burned: 921 (million) % 113.29/16.31 % (3865132)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3470871233:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi) % 113.29/16.31 % (3865132)Instruction limit reached! % 113.29/16.31 % (3865132)------------------------------ % 113.29/16.31 % (3865132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.29/16.31 % (3865132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.29/16.31 % (3865132)CaDiCaL version: 2.1.3 % 113.29/16.31 % (3865132)Termination reason: Instruction limit % 113.29/16.31 % (3865132)Termination phase: Saturation % 113.29/16.31 % (3865132)Time elapsed: 0.738 s % 113.29/16.31 % (3865132)Peak memory usage: 23 MB % 113.29/16.31 % (3865132)Instructions burned: 1472 (million) % 113.29/16.31 % (3865134)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3892759619:i=6324_2977 on theBenchmark for (2977ds/6324Mi) % 113.29/16.31 % (3865126)Instruction limit reached! % 113.29/16.31 % (3865126)------------------------------ % 113.29/16.31 % (3865126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.29/16.31 % (3865126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.29/16.31 % (3865126)CaDiCaL version: 2.1.3 % 113.29/16.31 % (3865126)Termination reason: Instruction limit % 168.87/24.16 % (3865126)Termination phase: Finite model building preprocessing % 168.87/24.16 % (3865126)Time elapsed: 2.420 s % 168.87/24.16 % (3865126)Peak memory usage: 82 MB % 168.87/24.16 % (3865126)Instructions burned: 9518 (million) % 168.87/24.16 % (3865136)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=625435694:fmbsr=2.30978:i=2174_2966 on theBenchmark for (2966ds/2174Mi) % 168.87/24.16 % (3865129)Instruction limit reached! % 168.87/24.16 % (3865129)------------------------------ % 168.87/24.16 % (3865129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.87/24.16 % (3865129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.87/24.16 % (3865129)CaDiCaL version: 2.1.3 % 168.87/24.16 % (3865129)Termination reason: Instruction limit % 168.87/24.16 % (3865129)Termination phase: Saturation % 168.87/24.16 % (3865129)Time elapsed: 2.686 s % 168.87/24.16 % (3865129)Peak memory usage: 43 MB % 168.87/24.16 % (3865129)Instructions burned: 5132 (million) % 168.87/24.16 % (3865138)ott-2_1_sil=16000:newcnf=on:random_seed=145285664:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2962 on theBenchmark for (2962ds/869Mi) % 168.87/24.16 % (3865136)Instruction limit reached! % 168.87/24.16 % (3865136)------------------------------ % 168.87/24.16 % (3865136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.87/24.16 % (3865136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.87/24.16 % (3865136)CaDiCaL version: 2.1.3 % 168.87/24.16 % (3865136)Termination reason: Instruction limit % 168.87/24.16 % (3865136)Termination phase: Finite model building preprocessing % 168.87/24.16 % (3865136)Time elapsed: 0.552 s % 168.87/24.16 % (3865136)Peak memory usage: 34 MB % 168.87/24.16 % (3865136)Instructions burned: 2174 (million) % 168.87/24.16 % (3865140)ott+10_1_sil=32000:tgt=ground:random_seed=3454209506:i=5114:av=off_2960 on theBenchmark for (2960ds/5114Mi) % 168.87/24.16 % (3865138)Instruction limit reached! % 168.87/24.16 % (3865138)------------------------------ % 168.87/24.16 % (3865138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.87/24.16 % (3865138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.87/24.16 % (3865138)CaDiCaL version: 2.1.3 % 168.87/24.16 % (3865138)Termination reason: Instruction limit % 168.87/24.16 % (3865138)Termination phase: Saturation % 168.87/24.16 % (3865138)Time elapsed: 0.453 s % 168.87/24.16 % (3865138)Peak memory usage: 22 MB % 168.87/24.16 % (3865138)Instructions burned: 870 (million) % 168.87/24.16 % (3865142)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4059208685:i=54282_2958 on theBenchmark for (2958ds/54282Mi) % 168.87/24.16 % (3865134)Instruction limit reached! % 168.87/24.16 % (3865134)------------------------------ % 168.87/24.16 % (3865134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.87/24.16 % (3865134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.87/24.16 % (3865134)CaDiCaL version: 2.1.3 % 168.87/24.16 % (3865134)Termination reason: Instruction limit % 168.87/24.16 % (3865134)Termination phase: Finite model building preprocessing % 168.87/24.16 % (3865134)Time elapsed: 2.931 s % 168.87/24.16 % (3865134)Peak memory usage: 65 MB % 168.87/24.16 % (3865134)Instructions burned: 6325 (million) % 168.87/24.16 % (3865144)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1241646068:i=3512:aac=none_2948 on theBenchmark for (2948ds/3512Mi) % 168.87/24.16 % (3865140)Instruction limit reached! % 168.87/24.16 % (3865140)------------------------------ % 168.87/24.16 % (3865140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.87/24.16 % (3865140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.87/24.16 % (3865140)CaDiCaL version: 2.1.3 % 168.87/24.16 % (3865140)Termination reason: Instruction limit % 168.87/24.16 % (3865140)Termination phase: Saturation % 168.87/24.16 % (3865140)Time elapsed: 1.388 s % 168.87/24.16 % (3865140)Peak memory usage: 28 MB % 168.87/24.16 % (3865140)Instructions burned: 5115 (million) % 168.87/24.16 % (3865146)dis+21_1_sil=32000:sas=cadical:random_seed=3971690500:i=3773:amm=off_2946 on theBenchmark for (2946ds/3773Mi) % 168.87/24.16 % (3865146)Instruction limit reached! % 168.87/24.16 % (3865146)------------------------------ % 168.87/24.16 % (3865146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 168.87/24.16 % (3865146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.87/24.16 % (3865146)CaDiCaL version: 2.1.3 % 168.87/24.16 % (3865146)Termination reason: Instruction limit % 168.87/24.16 % (3865146)Termination phase: Saturation % 168.87/24.16 % (3865146)Time elapsed: 1.118 s % 215.43/30.74 % (3865146)Peak memory usage: 42 MB % 215.43/30.74 % (3865146)Instructions burned: 3775 (million) % 215.43/30.74 % (3865148)ott+11_1_sil=16000:gs=on:random_seed=2506168697:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2935 on theBenchmark for (2935ds/2251Mi) % 215.43/30.74 % (3865148)Instruction limit reached! % 215.43/30.74 % (3865148)------------------------------ % 215.43/30.74 % (3865148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.43/30.74 % (3865148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.43/30.74 % (3865148)CaDiCaL version: 2.1.3 % 215.43/30.74 % (3865148)Termination reason: Instruction limit % 215.43/30.74 % (3865148)Termination phase: Saturation % 215.43/30.74 % (3865148)Time elapsed: 0.671 s % 215.43/30.74 % (3865148)Peak memory usage: 33 MB % 215.43/30.74 % (3865148)Instructions burned: 2253 (million) % 215.43/30.74 % (3865150)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3700062536:fmbsr=1.6:i=67534_2928 on theBenchmark for (2928ds/67534Mi) % 215.43/30.74 % (3865144)Instruction limit reached! % 215.43/30.74 % (3865144)------------------------------ % 215.43/30.74 % (3865144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.43/30.74 % (3865144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.43/30.74 % (3865144)CaDiCaL version: 2.1.3 % 215.43/30.74 % (3865144)Termination reason: Instruction limit % 215.43/30.74 % (3865144)Termination phase: Saturation % 215.43/30.74 % (3865144)Time elapsed: 2.026 s % 215.43/30.74 % (3865144)Peak memory usage: 38 MB % 215.43/30.74 % (3865144)Instructions burned: 3514 (million) % 215.43/30.74 % (3865152)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2227550981:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2927 on theBenchmark for (2927ds/4591Mi) % 215.43/30.74 % (3865152)Instruction limit reached! % 215.43/30.74 % (3865152)------------------------------ % 215.43/30.74 % (3865152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.43/30.74 % (3865152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.43/30.74 % (3865152)CaDiCaL version: 2.1.3 % 215.43/30.74 % (3865152)Termination reason: Instruction limit % 215.43/30.74 % (3865152)Termination phase: Saturation % 215.43/30.74 % (3865152)Time elapsed: 2.346 s % 215.43/30.74 % (3865152)Peak memory usage: 60 MB % 215.43/30.74 % (3865152)Instructions burned: 4591 (million) % 215.43/30.74 % (3865154)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=999009419:i=29340_2903 on theBenchmark for (2903ds/29340Mi) % 215.43/30.74 % (3865124)Instruction limit reached! % 215.43/30.74 % (3865124)------------------------------ % 215.43/30.74 % (3865124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.43/30.74 % (3865124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.43/30.74 % (3865124)CaDiCaL version: 2.1.3 % 215.43/30.74 % (3865124)Termination reason: Instruction limit % 215.43/30.74 % (3865124)Termination phase: Finite model building preprocessing % 215.43/30.74 % (3865124)Time elapsed: 10.105 s % 215.43/30.74 % (3865124)Peak memory usage: 146 MB % 215.43/30.74 % (3865124)Instructions burned: 22061 (million) % 215.43/30.74 % (3865156)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3510704409:i=5211_2891 on theBenchmark for (2891ds/5211Mi) % 215.43/30.74 % (3865156)Instruction limit reached! % 215.43/30.74 % (3865156)------------------------------ % 215.43/30.74 % (3865156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.43/30.74 % (3865156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.43/30.74 % (3865156)CaDiCaL version: 2.1.3 % 215.43/30.74 % (3865156)Termination reason: Instruction limit % 215.43/30.74 % (3865156)Termination phase: Saturation % 215.43/30.74 % (3865156)Time elapsed: 2.553 s % 215.43/30.74 % (3865156)Peak memory usage: 45 MB % 215.43/30.74 % (3865156)Instructions burned: 5214 (million) % 215.43/30.74 % (3865158)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=69107805:i=5497:nm=2_2865 on theBenchmark for (2865ds/5497Mi) % 215.43/30.74 % TRYING [7] % 215.43/30.74 % (3865158)Instruction limit reached! % 215.43/30.74 % (3865158)------------------------------ % 215.43/30.74 % (3865158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.43/30.74 % (3865158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.43/30.74 % (3865158)CaDiCaL version: 2.1.3 % 215.43/30.74 % (3865158)Termination reason: Instruction limit % 215.43/30.74 % (3865158)Termination phase: Finite model building preprocessing % 215.43/30.74 % (3865158)Time elapsed: 2.564 s % 300.56/42.73 % (3865158)Peak memory usage: 61 MB % 300.56/42.73 % (3865158)Instructions burned: 5497 (million) % 300.56/42.73 % (3865160)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2344927704:fmbsr=2:i=46332_2839 on theBenchmark for (2839ds/46332Mi) % 300.56/42.73 % (3865160)Cannot represent all propositional literals internally % 300.56/42.73 % (3865160)Refutation not found, incomplete strategy % 300.56/42.73 % (3865160)------------------------------ % 300.56/42.73 % (3865160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.56/42.73 % (3865160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.56/42.73 % (3865160)CaDiCaL version: 2.1.3 % 300.56/42.73 % (3865160)Termination reason: Refutation not found, incomplete strategy % 300.56/42.73 % (3865160)Time elapsed: 0.854 s % 300.56/42.73 % (3865160)Peak memory usage: 34 MB % 300.56/42.73 % (3865160)Instructions burned: 1840 (million) % 300.56/42.73 % (3865160)------------------------------ % 300.56/42.73 % (3865160)------------------------------ % 300.56/42.73 % (3865162)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3276973288:i=14071_2830 on theBenchmark for (2830ds/14071Mi) % 300.56/42.73 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % Detected maximum model sizes of [2,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max] % 300.56/42.73 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % TRYING [1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % TRYING [1,2,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % TRYING [1,3,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % TRYING [1,3,1,1,1,1,1,1,1,2,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % TRYING [1,3,1,1,1,1,1,1,1,3,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % TRYING [1,3,1,1,1,1,1,1,1,4,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % TRYING [1,3,1,1,1,1,1,1,1,5,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % TRYING [1,3,1,1,1,1,1,1,1,6,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % TRYING [1,3,1,1,1,1,1,1,1,7,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % TRYING [1,3,1,1,1,1,1,1,1,8,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % TRYING [1,3,1,1,1,1,1,1,1,9,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % TRYING [1,3,1,1,1,1,1,1,1,10,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.73 % (3865150)Instruction limit reached! % 300.56/42.73 % (3865150)------------------------------ % 300.56/42.73 % (3865150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.56/42.74 % (3865150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.56/42.74 % (3865150)CaDiCaL version: 2.1.3 % 300.56/42.74 % (3865150)Termination reason: Instruction limit % 300.56/42.74 % (3865150)Termination phase: Finite model building constraint generation % 300.56/42.74 % (3865150)Time elapsed: 14.910 s % 300.56/42.74 % (3865150)Peak memory usage: 4866 MB % 300.56/42.74 % (3865150)Instructions burned: 67535 (million) % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,11,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % (3865164)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3997053028:i=22565:add=on:rawr=on_2774 on theBenchmark for (2774ds/22565Mi) % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,12,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,13,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % Detected maximum model sizes of [2,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max] % 300.56/42.74 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,2,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % (3865162)Instruction limit reached! % 300.56/42.74 % (3865162)------------------------------ % 300.56/42.74 % (3865162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.56/42.74 % (3865162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.56/42.74 % (3865162)CaDiCaL version: 2.1.3 % 300.56/42.74 % (3865162)Termination reason: Instruction limit % 300.56/42.74 % (3865162)Termination phase: Finite model building preprocessing % 300.56/42.74 % (3865162)Time elapsed: 6.549 s % 300.56/42.74 % (3865162)Peak memory usage: 105 MB % 300.56/42.74 % (3865162)Instructions burned: 14073 (million) % 300.56/42.74 % (3865166)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2273375161:i=8173:av=off_2764 on theBenchmark for (2764ds/8173Mi) % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,2,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,14,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % (3865154)Instruction limit reached! % 300.56/42.74 % (3865154)------------------------------ % 300.56/42.74 % (3865154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.56/42.74 % (3865154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.56/42.74 % (3865154)CaDiCaL version: 2.1.3 % 300.56/42.74 % (3865154)Termination reason: Instruction limit % 300.56/42.74 % (3865154)Termination phase: Saturation % 300.56/42.74 % (3865154)Time elapsed: 14.274 s % 300.56/42.74 % (3865154)Peak memory usage: 262 MB % 300.56/42.74 % (3865154)Instructions burned: 29341 (million) % 300.56/42.74 % (3865168)dis+10_16:1_sil=16000:random_seed=1824404080:i=9155:fsr=off_2760 on theBenchmark for (2760ds/9155Mi) % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,3,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,4,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,5,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,15,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,6,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,7,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,8,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,16,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,9,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,10,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,17,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,11,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,12,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,18,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,13,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,14,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % (3865166)Instruction limit reached! % 300.56/42.74 % (3865166)------------------------------ % 300.56/42.74 % (3865166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.56/42.74 % (3865166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.56/42.74 % (3865166)CaDiCaL version: 2.1.3 % 300.56/42.74 % (3865166)Termination reason: Instruction limit % 300.56/42.74 % (3865166)Termination phase: Saturation % 300.56/42.74 % (3865166)Time elapsed: 4.688 s % 300.56/42.74 % (3865166)Peak memory usage: 58 MB % 300.56/42.74 % (3865166)Instructions burned: 8174 (million) % 300.56/42.74 % (3865170)ott-3_8_sil=64000:random_seed=1211544313:i=20139:bs=on_2717 on theBenchmark for (2717ds/20139Mi) % 300.56/42.74 % (3865142)Instruction limit reached! % 300.56/42.74 % (3865142)------------------------------ % 300.56/42.74 % (3865142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.56/42.74 % (3865142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.56/42.74 % (3865142)CaDiCaL version: 2.1.3 % 300.56/42.74 % (3865142)Termination reason: Instruction limit % 300.56/42.74 % (3865142)Termination phase: Finite model building constraint generation % 300.56/42.74 % (3865142)Time elapsed: 24.238 s % 300.56/42.74 % (3865142)Peak memory usage: 327 MB % 300.56/42.74 % (3865142)Instructions burned: 54283 (million) % 300.56/42.74 % (3865172)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1174518534:fmbsr=2:i=32576_2715 on theBenchmark for (2715ds/32576Mi) % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,19,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % (3865168)Instruction limit reached! % 300.56/42.74 % (3865168)------------------------------ % 300.56/42.74 % (3865168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.56/42.74 % (3865168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.56/42.74 % (3865168)CaDiCaL version: 2.1.3 % 300.56/42.74 % (3865168)Termination reason: Instruction limit % 300.56/42.74 % (3865168)Termination phase: Saturation % 300.56/42.74 % (3865168)Time elapsed: 5.153 s % 300.56/42.74 % (3865168)Peak memory usage: 73 MB % 300.56/42.74 % (3865168)Instructions burned: 9156 (million) % 300.56/42.74 % (3865174)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=526656348:i=11404_2708 on theBenchmark for (2708ds/11404Mi) % 300.56/42.74 % TRYING [1,3,1,1,1,1,1,1,1,20,1,2,1,1,1,1,1,1,1,1,1] % 300.56/42.74 % (3865164)Instruction limit reached! % 300.56/42.74 % (3865164)------------------------------ % 300.56/42.74 % (3865164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.56/42.74 % (3865164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.56/42.74 % (3865164)CaDiCaL version: 2.1.3 % 300.56/42.74 % (3865164)Termination reason: Instruction limit % 300.56/42.74 % (3865164)Termination phase: Saturation % 300.56/42.74 % (3865164)Time elapsed: 7.889 s % 300.56/42.74 % (3865164)Peak memory usage: 235 MB % 300.56/42.74 % (3865164)Instructions burned: 22568 (million) % 300.56/42.74 % (3865176)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=846444129:i % 300.56/42.74 Terminated % 300.56/42.74 % Vampire exiting %------------------------------------------------------------------------------