%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : CSR080+3 : TPTP v9.3.1. Bugfixed v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n002.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 09:45:01 AM UTC 2026 % Result : Timeout 300.24s 45.35s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : CSR080+3 : TPTP v9.3.1. Bugfixed v7.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.26 % Computer : n002.cluster.edu % 0.11/0.26 % Model : x86_64 x86_64 % 0.11/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.26 % Memory : 8046.5625MB % 0.11/0.26 % OS : Linux 6.8.0-71-generic % 0.11/0.26 % CPULimit : 300 % 0.11/0.26 % WCLimit : 300 % 0.11/0.26 % DateTime : Mon Sep 28 22:30:37 UTC 2026 % 0.11/0.26 % CPUTime : % 0.11/0.26 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.26/0.31 Running first-order model finding % 0.26/0.32 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 % 45.17/9.43 % (854133)Will run a generic schedule for satisfiability detection. % 45.17/9.43 % (854140)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=29388273_2968 on theBenchmark for (2968ds/0Mi) % 45.17/9.43 % (854141)% WARNING: option uhcvi not known. % 45.17/9.43 % (854141)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1712490351:i=135531:add=off:rawr=on_2968 on theBenchmark for (2968ds/135531Mi) % 45.17/9.43 % (854142)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=37405568:i=88024:add=on:rawr=on_2968 on theBenchmark for (2968ds/88024Mi) % 45.17/9.43 % (854143)dis+10_1_sil=32000:sp=arity:random_seed=1303345885:i=103:fgj=on_2968 on theBenchmark for (2968ds/103Mi) % 45.17/9.43 % (854145)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2369581861:i=116_2968 on theBenchmark for (2968ds/116Mi) % 45.17/9.43 % (854147)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3660072336:i=131_2968 on theBenchmark for (2968ds/131Mi) % 45.17/9.43 % (854148)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4014389542:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2968 on theBenchmark for (2968ds/159Mi) % 45.17/9.43 % (854143)Instruction limit reached! % 45.17/9.43 % (854143)------------------------------ % 45.17/9.43 % (854143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.17/9.43 % (854143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.17/9.43 % (854143)CaDiCaL version: 2.1.3 % 45.17/9.43 % (854143)Termination reason: Instruction limit % 45.17/9.43 % (854143)Termination phase: Preprocessing 1 % 45.17/9.43 % (854143)Time elapsed: 0.107 s % 45.17/9.43 % (854143)Peak memory usage: 155 MB % 45.17/9.43 % (854143)Instructions burned: 103 (million) % 45.17/9.43 % (854145)Instruction limit reached! % 45.17/9.43 % (854145)------------------------------ % 45.17/9.43 % (854145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.17/9.43 % (854145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.17/9.43 % (854145)CaDiCaL version: 2.1.3 % 45.17/9.43 % (854145)Termination reason: Instruction limit % 45.17/9.43 % (854145)Termination phase: Preprocessing 1 % 45.17/9.43 % (854145)Time elapsed: 0.132 s % 45.17/9.43 % (854145)Peak memory usage: 155 MB % 45.17/9.43 % (854145)Instructions burned: 116 (million) % 45.17/9.43 % (854147)Instruction limit reached! % 45.17/9.43 % (854147)------------------------------ % 45.17/9.43 % (854147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.17/9.43 % (854147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.17/9.43 % (854147)CaDiCaL version: 2.1.3 % 45.17/9.43 % (854147)Termination reason: Instruction limit % 45.17/9.43 % (854147)Termination phase: Preprocessing 1 % 45.17/9.43 % (854147)Time elapsed: 0.137 s % 45.17/9.43 % (854147)Peak memory usage: 155 MB % 45.17/9.43 % (854147)Instructions burned: 131 (million) % 45.17/9.43 % (854154)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=751515487:i=714:nm=2_2966 on theBenchmark for (2966ds/714Mi) % 45.17/9.43 % (854148)Instruction limit reached! % 45.17/9.43 % (854148)------------------------------ % 45.17/9.43 % (854148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.17/9.43 % (854148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.17/9.43 % (854148)CaDiCaL version: 2.1.3 % 45.17/9.43 % (854148)Termination reason: Instruction limit % 45.17/9.43 % (854148)Termination phase: Preprocessing 1 % 45.17/9.43 % (854148)Time elapsed: 0.161 s % 45.17/9.43 % (854148)Peak memory usage: 155 MB % 45.17/9.43 % (854148)Instructions burned: 159 (million) % 45.17/9.43 % (854155)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=487363569:i=131:bd=preordered:fsd=on_2966 on theBenchmark for (2966ds/131Mi) % 45.17/9.43 % (854157)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=3437943826:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2966 on theBenchmark for (2966ds/684Mi) % 45.17/9.43 % (854159)ott-21_1_sil=16000:fs=off:random_seed=1663646205:i=180:av=off:fsr=off_2965 on theBenchmark for (2965ds/180Mi) % 45.17/9.43 % (854155)Instruction limit reached! % 45.17/9.43 % (854155)------------------------------ % 45.17/9.43 % (854155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.17/9.43 % (854155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.17/9.43 % (854155)CaDiCaL version: 2.1.3 % 45.17/9.43 % (854155)Termination reason: Instruction limit % 85.26/15.07 % (854155)Termination phase: Preprocessing 1 % 85.26/15.07 % (854155)Time elapsed: 0.134 s % 85.26/15.07 % (854155)Peak memory usage: 155 MB % 85.26/15.07 % (854155)Instructions burned: 131 (million) % 85.26/15.07 % (854162)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4176550073:i=477:bd=all_2964 on theBenchmark for (2964ds/477Mi) % 85.26/15.07 % (854159)Instruction limit reached! % 85.26/15.07 % (854159)------------------------------ % 85.26/15.07 % (854159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.26/15.07 % (854159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.26/15.07 % (854159)CaDiCaL version: 2.1.3 % 85.26/15.07 % (854159)Termination reason: Instruction limit % 85.26/15.07 % (854159)Termination phase: Preprocessing 1 % 85.26/15.07 % (854159)Time elapsed: 0.191 s % 85.26/15.07 % (854159)Peak memory usage: 155 MB % 85.26/15.07 % (854159)Instructions burned: 180 (million) % 85.26/15.07 % (854164)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4175842400:fmbsr=1.3:i=865:ins=25_2963 on theBenchmark for (2963ds/865Mi) % 85.26/15.07 % (854157)Instruction limit reached! % 85.26/15.07 % (854157)------------------------------ % 85.26/15.07 % (854157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.26/15.07 % (854157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.26/15.07 % (854157)CaDiCaL version: 2.1.3 % 85.26/15.07 % (854157)Termination reason: Instruction limit % 85.26/15.07 % (854157)Termination phase: Preprocessing 1 % 85.26/15.07 % (854157)Time elapsed: 0.641 s % 85.26/15.07 % (854157)Peak memory usage: 158 MB % 85.26/15.07 % (854157)Instructions burned: 684 (million) % 85.26/15.07 % (854154)Instruction limit reached! % 85.26/15.07 % (854154)------------------------------ % 85.26/15.07 % (854154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.26/15.07 % (854154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.26/15.07 % (854154)CaDiCaL version: 2.1.3 % 85.26/15.07 % (854154)Termination reason: Instruction limit % 85.26/15.07 % (854154)Termination phase: Unused predicate definition removal % 85.26/15.07 % (854154)Time elapsed: 0.695 s % 85.26/15.07 % (854154)Peak memory usage: 189 MB % 85.26/15.07 % (854154)Instructions burned: 715 (million) % 85.26/15.07 % (854162)Instruction limit reached! % 85.26/15.07 % (854162)------------------------------ % 85.26/15.07 % (854162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.26/15.07 % (854162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.26/15.07 % (854162)CaDiCaL version: 2.1.3 % 85.26/15.07 % (854162)Termination reason: Instruction limit % 85.26/15.07 % (854162)Termination phase: Naming % 85.26/15.07 % (854162)Time elapsed: 0.486 s % 85.26/15.07 % (854162)Peak memory usage: 164 MB % 85.26/15.07 % (854162)Instructions burned: 478 (million) % 85.26/15.07 % (854174)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=826056886:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2958 on theBenchmark for (2958ds/692Mi) % 85.26/15.07 % (854172)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3784601974:i=1179_2958 on theBenchmark for (2958ds/1179Mi) % 85.26/15.07 % (854173)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=91304066:i=889:ins=1_2958 on theBenchmark for (2958ds/889Mi) % 85.26/15.07 % (854164)Instruction limit reached! % 85.26/15.07 % (854164)------------------------------ % 85.26/15.07 % (854164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.26/15.07 % (854164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.26/15.07 % (854164)CaDiCaL version: 2.1.3 % 85.26/15.07 % (854164)Termination reason: Instruction limit % 85.26/15.07 % (854164)Termination phase: Preprocessing 2 % 85.26/15.07 % (854164)Time elapsed: 0.839 s % 85.26/15.07 % (854164)Peak memory usage: 203 MB % 85.26/15.07 % (854164)Instructions burned: 866 (million) % 85.26/15.07 % (854178)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1931442869:i=879:kws=inv_precedence:fsr=off_2954 on theBenchmark for (2954ds/879Mi) % 85.26/15.07 % (854174)Instruction limit reached! % 85.26/15.07 % (854174)------------------------------ % 85.26/15.07 % (854174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.26/15.07 % (854174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.26/15.07 % (854174)CaDiCaL version: 2.1.3 % 85.26/15.07 % (854174)Termination reason: Instruction limit % 85.26/15.07 % (854174)Termination phase: Preprocessing 1 % 141.14/22.90 % (854174)Time elapsed: 0.603 s % 141.14/22.90 % (854174)Peak memory usage: 158 MB % 141.14/22.90 % (854174)Instructions burned: 692 (million) % 141.14/22.90 % (854180)fmb+10_1_sil=64000:random_seed=1728381341:i=22061:nm=2:gsp=on_2952 on theBenchmark for (2952ds/22061Mi) % 141.14/22.90 % (854173)Instruction limit reached! % 141.14/22.90 % (854173)------------------------------ % 141.14/22.90 % (854173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.14/22.90 % (854173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.14/22.90 % (854173)CaDiCaL version: 2.1.3 % 141.14/22.90 % (854173)Termination reason: Instruction limit % 141.14/22.90 % (854173)Termination phase: Preprocessing 2 % 141.14/22.90 % (854173)Time elapsed: 0.915 s % 141.14/22.90 % (854173)Peak memory usage: 194 MB % 141.14/22.90 % (854173)Instructions burned: 889 (million) % 141.14/22.90 % (854182)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=720668991:i=9515:nm=5_2948 on theBenchmark for (2948ds/9515Mi) % 141.14/22.90 % (854172)Instruction limit reached! % 141.14/22.90 % (854172)------------------------------ % 141.14/22.90 % (854172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.14/22.90 % (854172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.14/22.90 % (854172)CaDiCaL version: 2.1.3 % 141.14/22.90 % (854172)Termination reason: Instruction limit % 141.14/22.90 % (854172)Termination phase: Property scanning % 141.14/22.90 % (854172)Time elapsed: 1.226 s % 141.14/22.90 % (854172)Peak memory usage: 185 MB % 141.14/22.90 % (854172)Instructions burned: 1179 (million) % 141.14/22.90 % (854185)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1398005888:fmbsr=1.7:i=920_2945 on theBenchmark for (2945ds/920Mi) % 141.14/22.90 % (854178)Instruction limit reached! % 141.14/22.90 % (854178)------------------------------ % 141.14/22.90 % (854178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.14/22.90 % (854178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.14/22.90 % (854178)CaDiCaL version: 2.1.3 % 141.14/22.90 % (854178)Termination reason: Instruction limit % 141.14/22.90 % (854178)Termination phase: NewCNF % 141.14/22.90 % (854178)Time elapsed: 0.820 s % 141.14/22.90 % (854178)Peak memory usage: 178 MB % 141.14/22.90 % (854178)Instructions burned: 881 (million) % 141.14/22.90 % (854188)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1908147449:i=5131_2945 on theBenchmark for (2945ds/5131Mi) % 141.14/22.90 % (854185)Instruction limit reached! % 141.14/22.90 % (854185)------------------------------ % 141.14/22.90 % (854185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.14/22.90 % (854185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.14/22.90 % (854185)CaDiCaL version: 2.1.3 % 141.14/22.90 % (854185)Termination reason: Instruction limit % 141.14/22.90 % (854185)Termination phase: Preprocessing 2 % 141.14/22.90 % (854185)Time elapsed: 0.937 s % 141.14/22.90 % (854185)Peak memory usage: 197 MB % 141.14/22.90 % (854185)Instructions burned: 920 (million) % 141.14/22.90 % (854192)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3750948092:i=1472:ins=7:fdi=8:gsp=on_2935 on theBenchmark for (2935ds/1472Mi) % 141.14/22.90 % (854192)Instruction limit reached! % 141.14/22.90 % (854192)------------------------------ % 141.14/22.90 % (854192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.14/22.90 % (854192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.14/22.90 % (854192)CaDiCaL version: 2.1.3 % 141.14/22.90 % (854192)Termination reason: Instruction limit % 141.14/22.90 % (854192)Termination phase: Property scanning % 141.14/22.90 % (854192)Time elapsed: 1.503 s % 141.14/22.90 % (854192)Peak memory usage: 185 MB % 141.14/22.90 % (854192)Instructions burned: 1472 (million) % 141.14/22.90 % (854200)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1752900487:i=6324_2920 on theBenchmark for (2920ds/6324Mi) % 141.14/22.90 % (854188)Instruction limit reached! % 141.14/22.90 % (854188)------------------------------ % 141.14/22.90 % (854188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.14/22.90 % (854188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.14/22.90 % (854188)CaDiCaL version: 2.1.3 % 141.14/22.90 % (854188)Termination reason: Instruction limit % 141.14/22.90 % (854188)Termination phase: Saturation % 141.14/22.90 % (854188)Time elapsed: 3.501 s % 141.14/22.90 % (854188)Peak memory usage: 200 MB % 141.14/22.90 % (854188)Instructions burned: 5131 (million) % 141.14/22.90 % (854202)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4202169869:fmbsr=2.30978:i=2174_2909 on theBenchmark for (2909ds/2174Mi) % 207.97/32.39 % (854202)Instruction limit reached! % 207.97/32.39 % (854202)------------------------------ % 207.97/32.39 % (854202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.97/32.39 % (854202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.97/32.39 % (854202)CaDiCaL version: 2.1.3 % 207.97/32.39 % (854202)Termination reason: Instruction limit % 207.97/32.39 % (854202)Termination phase: Property scanning % 207.97/32.39 % (854202)Time elapsed: 2.104 s % 207.97/32.39 % (854202)Peak memory usage: 241 MB % 207.97/32.39 % (854202)Instructions burned: 2174 (million) % 207.97/32.39 % (854210)ott-2_1_sil=16000:newcnf=on:random_seed=4083707713:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2887 on theBenchmark for (2887ds/869Mi) % 207.97/32.39 % Detected minimum model sizes of [617] % 207.97/32.39 % Detected maximum model sizes of [max] % 207.97/32.39 % (854140)Cannot represent all propositional literals internally % 207.97/32.39 % (854140)Refutation not found, incomplete strategy % 207.97/32.39 % (854140)------------------------------ % 207.97/32.39 % (854140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.97/32.39 % (854140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.97/32.39 % (854140)CaDiCaL version: 2.1.3 % 207.97/32.39 % (854140)Termination reason: Refutation not found, incomplete strategy % 207.97/32.39 % (854140)Time elapsed: 8.550 s % 207.97/32.39 % (854140)Peak memory usage: 476 MB % 207.97/32.39 % (854140)Instructions burned: 17365 (million) % 207.97/32.39 % (854140)------------------------------ % 207.97/32.39 % (854140)------------------------------ % 207.97/32.39 % (854215)ott+10_1_sil=32000:tgt=ground:random_seed=2261093298:i=5114:av=off_2879 on theBenchmark for (2879ds/5114Mi) % 207.97/32.39 % (854210)Instruction limit reached! % 207.97/32.39 % (854210)------------------------------ % 207.97/32.39 % (854210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.97/32.39 % (854210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.97/32.39 % (854210)CaDiCaL version: 2.1.3 % 207.97/32.39 % (854210)Termination reason: Instruction limit % 207.97/32.39 % (854210)Termination phase: NewCNF % 207.97/32.39 % (854210)Time elapsed: 0.831 s % 207.97/32.39 % (854210)Peak memory usage: 178 MB % 207.97/32.39 % (854210)Instructions burned: 870 (million) % 207.97/32.39 % (854218)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2087957331:i=54282_2878 on theBenchmark for (2878ds/54282Mi) % 207.97/32.39 % (854182)Instruction limit reached! % 207.97/32.39 % (854182)------------------------------ % 207.97/32.39 % (854182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.97/32.39 % (854182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.97/32.39 % (854182)CaDiCaL version: 2.1.3 % 207.97/32.39 % (854182)Termination reason: Instruction limit % 207.97/32.39 % (854182)Termination phase: Finite model building preprocessing % 207.97/32.39 % (854182)Time elapsed: 8.672 s % 207.97/32.39 % (854182)Peak memory usage: 342 MB % 207.97/32.39 % (854182)Instructions burned: 9515 (million) % 207.97/32.39 % (854230)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1435217069:i=3512:aac=none_2861 on theBenchmark for (2861ds/3512Mi) % 207.97/32.39 % (854200)Instruction limit reached! % 207.97/32.39 % (854200)------------------------------ % 207.97/32.39 % (854200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.97/32.39 % (854200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.97/32.39 % (854200)CaDiCaL version: 2.1.3 % 207.97/32.39 % (854200)Termination reason: Instruction limit % 207.97/32.39 % (854200)Termination phase: Property scanning % 207.97/32.39 % (854200)Time elapsed: 6.131 s % 207.97/32.39 % (854200)Peak memory usage: 298 MB % 207.97/32.39 % (854200)Instructions burned: 6325 (million) % 207.97/32.39 % (854232)dis+21_1_sil=32000:sas=cadical:random_seed=3966257624:i=3773:amm=off_2857 on theBenchmark for (2857ds/3773Mi) % 207.97/32.39 % (854215)Instruction limit reached! % 207.97/32.39 % (854215)------------------------------ % 207.97/32.39 % (854215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.97/32.39 % (854215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.97/32.39 % (854215)CaDiCaL version: 2.1.3 % 207.97/32.39 % (854215)Termination reason: Instruction limit % 207.97/32.39 % (854215)Termination phase: Saturation % 207.97/32.39 % (854215)Time elapsed: 2.595 s % 207.97/32.39 % (854215)Peak memory usage: 248 MB % 207.97/32.39 % (854215)Instructions burned: 5116 (million) % 207.97/32.39 % (854236)ott+11_1_sil=16000:gs=on:random_seed=1668291703:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2852 on theBenchmark for (2852ds/2251Mi) % 210.28/37.54 % (854236)Instruction limit reached! % 210.28/37.54 % (854236)------------------------------ % 210.28/37.54 % (854236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.28/37.54 % (854236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.28/37.54 % (854236)CaDiCaL version: 2.1.3 % 210.28/37.54 % (854236)Termination reason: Instruction limit % 210.28/37.54 % (854236)Termination phase: Property scanning % 210.28/37.54 % (854236)Time elapsed: 1.240 s % 210.28/37.54 % (854236)Peak memory usage: 188 MB % 210.28/37.54 % (854236)Instructions burned: 2252 (million) % 210.28/37.54 % (854242)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2045202485:fmbsr=1.6:i=67534_2839 on theBenchmark for (2839ds/67534Mi) % 210.28/37.54 % Detected minimum model sizes of [617] % 210.28/37.54 % Detected maximum model sizes of [max] % 210.28/37.54 % (854180)Cannot represent all propositional literals internally % 210.28/37.54 % (854180)Refutation not found, incomplete strategy % 210.28/37.54 % (854180)------------------------------ % 210.28/37.54 % (854180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.28/37.54 % (854180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.28/37.54 % (854180)CaDiCaL version: 2.1.3 % 210.28/37.54 % (854180)Termination reason: Refutation not found, incomplete strategy % 210.28/37.54 % (854180)Time elapsed: 11.883 s % 210.28/37.54 % (854180)Peak memory usage: 388 MB % 210.28/37.54 % (854180)Instructions burned: 13611 (million) % 210.28/37.54 % (854180)------------------------------ % 210.28/37.54 % (854180)------------------------------ % 210.28/37.54 % (854246)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2401031138:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2828 on theBenchmark for (2828ds/4591Mi) % 210.28/37.54 % (854230)Instruction limit reached! % 210.28/37.54 % (854230)------------------------------ % 210.28/37.54 % (854230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.28/37.54 % (854230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.28/37.54 % (854230)CaDiCaL version: 2.1.3 % 210.28/37.54 % (854230)Termination reason: Instruction limit % 210.28/37.54 % (854230)Termination phase: Saturation % 210.28/37.54 % (854230)Time elapsed: 3.269 s % 210.28/37.54 % (854230)Peak memory usage: 205 MB % 210.28/37.54 % (854230)Instructions burned: 3512 (million) % 210.28/37.54 % (854248)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1379731602:i=29340_2827 on theBenchmark for (2827ds/29340Mi) % 210.28/37.54 % (854232)Instruction limit reached! % 210.28/37.54 % (854232)------------------------------ % 210.28/37.54 % (854232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.28/37.54 % (854232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.28/37.54 % (854232)CaDiCaL version: 2.1.3 % 210.28/37.54 % (854232)Termination reason: Instruction limit % 210.28/37.54 % (854232)Termination phase: Saturation % 210.28/37.54 % (854232)Time elapsed: 3.591 s % 210.28/37.54 % (854232)Peak memory usage: 211 MB % 210.28/37.54 % (854232)Instructions burned: 3773 (million) % 210.28/37.54 % (854252)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2729635529:i=5211_2821 on theBenchmark for (2821ds/5211Mi) % 210.28/37.54 % (854246)Instruction limit reached! % 210.28/37.54 % (854246)------------------------------ % 210.28/37.54 % (854246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.28/37.54 % (854246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.28/37.54 % (854246)CaDiCaL version: 2.1.3 % 210.28/37.54 % (854246)Termination reason: Instruction limit % 210.28/37.54 % (854246)Termination phase: Saturation % 210.28/37.54 % (854246)Time elapsed: 4.293 s % 210.28/37.54 % (854246)Peak memory usage: 238 MB % 210.28/37.54 % (854246)Instructions burned: 4591 (million) % 210.28/37.54 % (854262)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3047489114:i=5497:nm=2_2785 on theBenchmark for (2785ds/5497Mi) % 210.28/37.54 % (854252)Instruction limit reached! % 210.28/37.54 % (854252)------------------------------ % 210.28/37.54 % (854252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.28/37.54 % (854252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.28/37.54 % (854252)CaDiCaL version: 2.1.3 % 210.28/37.54 % (854252)Termination reason: Instruction limit % 210.28/37.54 % (854252)Termination phase: Saturation % 210.28/37.54 % (854252)TiTerminated %------------------------------------------------------------------------------