%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW248+1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n013.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:39:42 PM UTC 2026 % Result : Timeout 300.12s 42.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW248+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n013.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 13:23:36 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 14.86/2.48 % (1172448)Will run a generic schedule for satisfiability detection. % 14.86/2.48 % (1172457)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1625904400:i=116_2999 on theBenchmark for (2999ds/116Mi) % 14.86/2.48 % (1172454)% WARNING: option uhcvi not known. % 14.86/2.48 % (1172458)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=62050011:i=131_2999 on theBenchmark for (2999ds/131Mi) % 14.86/2.48 % (1172454)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2350072069:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 14.86/2.48 % (1172455)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1555731157:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 14.86/2.48 % (1172456)dis+10_1_sil=32000:sp=arity:random_seed=119505048:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 14.86/2.48 % (1172459)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4220115911:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 14.86/2.48 % (1172453)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=336673313_2999 on theBenchmark for (2999ds/0Mi) % 14.86/2.48 % (1172457)Instruction limit reached! % 14.86/2.48 % (1172457)------------------------------ % 14.86/2.48 % (1172457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.86/2.48 % (1172457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.86/2.48 % (1172457)CaDiCaL version: 2.1.3 % 14.86/2.48 % (1172457)Termination reason: Instruction limit % 14.86/2.48 % (1172457)Termination phase: Saturation % 14.86/2.48 % (1172457)Time elapsed: 0.032 s % 14.86/2.48 % (1172457)Peak memory usage: 14 MB % 14.86/2.48 % (1172457)Instructions burned: 117 (million) % 14.86/2.48 % (1172467)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1019652423:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 14.86/2.48 % (1172456)Instruction limit reached! % 14.86/2.48 % (1172456)------------------------------ % 14.86/2.48 % (1172456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.86/2.48 % (1172456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.86/2.48 % (1172456)CaDiCaL version: 2.1.3 % 14.86/2.48 % (1172456)Termination reason: Instruction limit % 14.86/2.48 % (1172456)Termination phase: Saturation % 14.86/2.48 % (1172456)Time elapsed: 0.053 s % 14.86/2.48 % (1172456)Peak memory usage: 14 MB % 14.86/2.48 % (1172456)Instructions burned: 103 (million) % 14.86/2.48 % (1172458)Instruction limit reached! % 14.86/2.48 % (1172458)------------------------------ % 14.86/2.48 % (1172458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.86/2.48 % (1172458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.86/2.48 % (1172458)CaDiCaL version: 2.1.3 % 14.86/2.48 % (1172458)Termination reason: Instruction limit % 14.86/2.48 % (1172458)Termination phase: Saturation % 14.86/2.48 % (1172458)Time elapsed: 0.056 s % 14.86/2.48 % (1172458)Peak memory usage: 15 MB % 14.86/2.48 % (1172458)Instructions burned: 134 (million) % 14.86/2.48 % (1172470)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=3167831414:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 14.86/2.48 % (1172469)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=720277725:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 14.86/2.48 % (1172459)Instruction limit reached! % 14.86/2.48 % (1172459)------------------------------ % 14.86/2.48 % (1172459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.86/2.48 % (1172459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.86/2.48 % (1172459)CaDiCaL version: 2.1.3 % 14.86/2.48 % (1172459)Termination reason: Instruction limit % 14.86/2.48 % (1172459)Termination phase: Saturation % 14.86/2.48 % (1172459)Time elapsed: 0.095 s % 14.86/2.48 % (1172459)Peak memory usage: 16 MB % 14.86/2.48 % (1172459)Instructions burned: 159 (million) % 14.86/2.48 % (1172473)ott-21_1_sil=16000:fs=off:random_seed=3717266880:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 14.86/2.48 % (1172469)Instruction limit reached! % 14.86/2.48 % (1172469)------------------------------ % 14.86/2.48 % (1172469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.86/2.48 % (1172469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.86/2.48 % (1172469)CaDiCaL version: 2.1.3 % 48.42/7.15 % (1172469)Termination reason: Instruction limit % 48.42/7.15 % (1172469)Termination phase: Saturation % 48.42/7.15 % (1172469)Time elapsed: 0.094 s % 48.42/7.15 % (1172469)Peak memory usage: 14 MB % 48.42/7.15 % (1172469)Instructions burned: 135 (million) % 48.42/7.15 % (1172473)Instruction limit reached! % 48.42/7.15 % (1172473)------------------------------ % 48.42/7.15 % (1172473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.42/7.15 % (1172473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.42/7.15 % (1172473)CaDiCaL version: 2.1.3 % 48.42/7.15 % (1172473)Termination reason: Instruction limit % 48.42/7.15 % (1172473)Termination phase: Saturation % 48.42/7.15 % (1172473)Time elapsed: 0.090 s % 48.42/7.15 % (1172473)Peak memory usage: 14 MB % 48.42/7.15 % (1172473)Instructions burned: 181 (million) % 48.42/7.15 % (1172478)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=822324096:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 48.42/7.15 % (1172485)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2877526916:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 48.42/7.15 % (1172470)Instruction limit reached! % 48.42/7.15 % (1172470)------------------------------ % 48.42/7.15 % (1172470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.42/7.15 % (1172470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.42/7.15 % (1172470)CaDiCaL version: 2.1.3 % 48.42/7.15 % (1172470)Termination reason: Instruction limit % 48.42/7.15 % (1172470)Termination phase: Saturation % 48.42/7.15 % (1172470)Time elapsed: 0.214 s % 48.42/7.15 % (1172470)Peak memory usage: 20 MB % 48.42/7.15 % (1172470)Instructions burned: 687 (million) % 48.42/7.15 % (1172504)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=337279959:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 48.42/7.15 % (1172467)Instruction limit reached! % 48.42/7.15 % (1172467)------------------------------ % 48.42/7.15 % (1172467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.42/7.15 % (1172467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.42/7.15 % (1172467)CaDiCaL version: 2.1.3 % 48.42/7.15 % (1172467)Termination reason: Instruction limit % 48.42/7.15 % (1172467)Termination phase: Finite model building preprocessing % 48.42/7.15 % (1172467)Time elapsed: 0.354 s % 48.42/7.15 % (1172467)Peak memory usage: 22 MB % 48.42/7.15 % (1172467)Instructions burned: 715 (million) % 48.42/7.15 % (1172550)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2048029564:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 48.42/7.15 % TRYING [1] % 48.42/7.15 % TRYING [2] % 48.42/7.15 % (1172478)Instruction limit reached! % 48.42/7.15 % (1172478)------------------------------ % 48.42/7.15 % (1172478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.42/7.15 % (1172478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.42/7.15 % (1172478)CaDiCaL version: 2.1.3 % 48.42/7.15 % (1172478)Termination reason: Instruction limit % 48.42/7.15 % (1172478)Termination phase: Saturation % 48.42/7.15 % (1172478)Time elapsed: 0.314 s % 48.42/7.15 % (1172478)Peak memory usage: 16 MB % 48.42/7.15 % (1172478)Instructions burned: 478 (million) % 48.42/7.15 % (1172582)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=3575669256:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi) % 48.42/7.15 % (1172485)Instruction limit reached! % 48.42/7.15 % (1172485)------------------------------ % 48.42/7.15 % (1172485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.42/7.15 % (1172485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.42/7.15 % (1172485)CaDiCaL version: 2.1.3 % 48.42/7.15 % (1172485)Termination reason: Instruction limit % 48.42/7.15 % (1172485)Termination phase: Finite model building preprocessing % 48.42/7.15 % (1172485)Time elapsed: 0.435 s % 48.42/7.15 % (1172485)Peak memory usage: 27 MB % 48.42/7.15 % (1172485)Instructions burned: 867 (million) % 48.42/7.15 % (1172615)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=884705252:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi) % 48.42/7.15 % TRYING [3] % 48.42/7.15 % (1172504)Instruction limit reached! % 48.42/7.15 % (1172504)------------------------------ % 48.42/7.15 % (1172504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 48.42/7.15 % (1172504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.08/12.31 % (1172504)CaDiCaL version: 2.1.3 % 85.08/12.31 % (1172504)Termination reason: Instruction limit % 85.08/12.31 % (1172504)Termination phase: Saturation % 85.08/12.31 % (1172504)Time elapsed: 0.417 s % 85.08/12.31 % (1172504)Peak memory usage: 23 MB % 85.08/12.31 % (1172504)Instructions burned: 1181 (million) % 85.08/12.31 % (1172617)fmb+10_1_sil=64000:random_seed=1317855810:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi) % 85.08/12.31 % (1172550)Instruction limit reached! % 85.08/12.31 % (1172550)------------------------------ % 85.08/12.31 % (1172550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.08/12.31 % (1172550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.08/12.31 % (1172550)CaDiCaL version: 2.1.3 % 85.08/12.31 % (1172550)Termination reason: Instruction limit % 85.08/12.31 % (1172550)Termination phase: Finite model building constraint generation % 85.08/12.31 % (1172550)Time elapsed: 0.451 s % 85.08/12.31 % (1172550)Peak memory usage: 41 MB % 85.08/12.31 % (1172550)Instructions burned: 891 (million) % 85.08/12.31 % (1172619)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1669426352:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 85.08/12.31 % TRYING [1] % 85.08/12.31 % TRYING [2] % 85.08/12.31 % (1172582)Instruction limit reached! % 85.08/12.31 % (1172582)------------------------------ % 85.08/12.31 % (1172582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.08/12.31 % (1172582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.08/12.31 % (1172582)CaDiCaL version: 2.1.3 % 85.08/12.31 % (1172582)Termination reason: Instruction limit % 85.08/12.31 % (1172582)Termination phase: Saturation % 85.08/12.31 % (1172582)Time elapsed: 0.445 s % 85.08/12.31 % (1172582)Peak memory usage: 21 MB % 85.08/12.31 % (1172582)Instructions burned: 693 (million) % 85.08/12.31 % (1172621)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3657335780:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 85.08/12.31 % (1172615)Instruction limit reached! % 85.08/12.31 % (1172615)------------------------------ % 85.08/12.31 % (1172615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.08/12.31 % (1172615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.08/12.31 % (1172615)CaDiCaL version: 2.1.3 % 85.08/12.31 % (1172615)Termination reason: Instruction limit % 85.08/12.31 % (1172615)Termination phase: Saturation % 85.08/12.31 % (1172615)Time elapsed: 0.459 s % 85.08/12.31 % (1172615)Peak memory usage: 21 MB % 85.08/12.31 % (1172615)Instructions burned: 879 (million) % 85.08/12.31 % (1172623)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1142492671:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 85.08/12.31 % (1172619)Cannot represent all propositional literals internally % 85.08/12.31 % (1172619)Refutation not found, incomplete strategy % 85.08/12.31 % (1172619)------------------------------ % 85.08/12.31 % (1172619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.08/12.31 % (1172619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.08/12.31 % (1172619)CaDiCaL version: 2.1.3 % 85.08/12.31 % (1172619)Termination reason: Refutation not found, incomplete strategy % 85.08/12.31 % (1172619)Time elapsed: 0.376 s % 85.08/12.31 % (1172619)Peak memory usage: 24 MB % 85.08/12.31 % (1172619)Instructions burned: 770 (million) % 85.08/12.31 % (1172619)------------------------------ % 85.08/12.31 % (1172619)------------------------------ % 85.08/12.32 % (1172625)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=302462034:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 85.08/12.32 % TRYING [8] % 85.08/12.32 % TRYING [3] % 85.08/12.32 % (1172621)Instruction limit reached! % 85.08/12.32 % (1172621)------------------------------ % 85.08/12.32 % (1172621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.08/12.32 % (1172621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.08/12.32 % (1172621)CaDiCaL version: 2.1.3 % 85.08/12.32 % (1172621)Termination reason: Instruction limit % 85.08/12.32 % (1172621)Termination phase: Finite model building constraint generation % 85.08/12.32 % (1172621)Time elapsed: 0.454 s % 85.08/12.32 % (1172621)Peak memory usage: 32 MB % 85.08/12.32 % (1172621)Instructions burned: 921 (million) % 85.08/12.32 % (1172635)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3356186205:i=6324_2984 on theBenchmark for (2984ds/6324Mi) % 85.08/12.32 % (1172635)Cannot represent all propositional literals internally % 85.08/12.32 % (1172635)Refutation not found, incomplete strategy % 181.80/28.24 % (1172635)------------------------------ % 181.80/28.24 % (1172635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.80/28.24 % (1172635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.80/28.24 % (1172635)CaDiCaL version: 2.1.3 % 181.80/28.24 % (1172635)Termination reason: Refutation not found, incomplete strategy % 181.80/28.24 % (1172635)Time elapsed: 0.648 s % 181.80/28.24 % (1172635)Peak memory usage: 25 MB % 181.80/28.24 % (1172635)Instructions burned: 794 (million) % 181.80/28.24 % (1172635)------------------------------ % 181.80/28.24 % (1172635)------------------------------ % 181.80/28.24 % TRYING [4] % 181.80/28.24 % (1172654)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3010340495:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi) % 181.80/28.24 % (1172625)Instruction limit reached! % 181.80/28.24 % (1172625)------------------------------ % 181.80/28.24 % (1172625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.80/28.24 % (1172625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.80/28.24 % (1172625)CaDiCaL version: 2.1.3 % 181.80/28.24 % (1172625)Termination reason: Instruction limit % 181.80/28.24 % (1172625)Termination phase: Saturation % 181.80/28.24 % (1172625)Time elapsed: 1.271 s % 181.80/28.24 % (1172625)Peak memory usage: 34 MB % 181.80/28.24 % (1172625)Instructions burned: 1472 (million) % 181.80/28.24 % (1172666)ott-2_1_sil=16000:newcnf=on:random_seed=2199181229:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2973 on theBenchmark for (2973ds/869Mi) % 181.80/28.24 % (1172666)Instruction limit reached! % 181.80/28.24 % (1172666)------------------------------ % 181.80/28.24 % (1172666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.80/28.24 % (1172666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.80/28.24 % (1172666)CaDiCaL version: 2.1.3 % 181.80/28.24 % (1172666)Termination reason: Instruction limit % 181.80/28.24 % (1172666)Termination phase: Saturation % 181.80/28.24 % (1172666)Time elapsed: 0.715 s % 181.80/28.24 % (1172666)Peak memory usage: 22 MB % 181.80/28.24 % (1172666)Instructions burned: 869 (million) % 181.80/28.24 % (1172673)ott+10_1_sil=32000:tgt=ground:random_seed=2993666659:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi) % 181.80/28.24 % (1172654)Instruction limit reached! % 181.80/28.24 % (1172654)------------------------------ % 181.80/28.24 % (1172654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.80/28.24 % (1172654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.80/28.24 % (1172654)CaDiCaL version: 2.1.3 % 181.80/28.24 % (1172654)Termination reason: Instruction limit % 181.80/28.24 % (1172654)Termination phase: Finite model building preprocessing % 181.80/28.24 % (1172654)Time elapsed: 1.374 s % 181.80/28.24 % (1172654)Peak memory usage: 32 MB % 181.80/28.24 % (1172654)Instructions burned: 2174 (million) % 181.80/28.24 % (1172699)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=906984680:i=54282_2963 on theBenchmark for (2963ds/54282Mi) % 181.80/28.24 % TRYING [4] % 181.80/28.24 % TRYING [1] % 181.80/28.24 % TRYING [2] % 181.80/28.24 % TRYING [3] % 181.80/28.24 % (1172623)Instruction limit reached! % 181.80/28.24 % (1172623)------------------------------ % 181.80/28.24 % (1172623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.80/28.24 % (1172623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.80/28.24 % (1172623)CaDiCaL version: 2.1.3 % 181.80/28.24 % (1172623)Termination reason: Instruction limit % 181.80/28.24 % (1172623)Termination phase: Saturation % 181.80/28.24 % (1172623)Time elapsed: 3.629 s % 181.80/28.24 % (1172623)Peak memory usage: 40 MB % 181.80/28.24 % (1172623)Instructions burned: 5131 (million) % 181.80/28.24 % (1172716)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4132725013:i=3512:aac=none_2951 on theBenchmark for (2951ds/3512Mi) % 181.80/28.24 % TRYING [4] % 181.80/28.24 % (1172673)Instruction limit reached! % 181.80/28.24 % (1172673)------------------------------ % 181.80/28.24 % (1172673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.80/28.24 % (1172673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.80/28.24 % (1172673)CaDiCaL version: 2.1.3 % 181.80/28.24 % (1172673)Termination reason: Instruction limit % 181.80/28.24 % (1172673)Termination phase: Saturation % 181.80/28.24 % (1172673)Time elapsed: 3.174 s % 181.80/28.24 % (1172673)Peak memory usage: 48 MB % 181.80/28.24 % (1172673)Instructions burned: 5115 (million) % 181.80/28.24 % (1172718)dis+21_1_sil=32000:sas=cadical:random_seed=911297357:i=3773:amm=off_2933 on theBenchmark for (2933ds/3773Mi) % 181.80/28.24 % (1172617)Instruction limit reached! % 282.98/40.22 % (1172617)------------------------------ % 282.98/40.22 % (1172617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.98/40.22 % (1172617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.98/40.22 % (1172617)CaDiCaL version: 2.1.3 % 282.98/40.22 % (1172617)Termination reason: Instruction limit % 282.98/40.22 % (1172617)Termination phase: Finite model building SAT solving % 282.98/40.22 % (1172617)Time elapsed: 6.084 s % 282.98/40.22 % (1172617)Peak memory usage: 599 MB % 282.98/40.22 % (1172617)Instructions burned: 22064 (million) % 282.98/40.22 % (1172720)ott+11_1_sil=16000:gs=on:random_seed=4248752942:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2930 on theBenchmark for (2930ds/2251Mi) % 282.98/40.22 % (1172716)Instruction limit reached! % 282.98/40.22 % (1172716)------------------------------ % 282.98/40.22 % (1172716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.98/40.22 % (1172716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.98/40.22 % (1172716)CaDiCaL version: 2.1.3 % 282.98/40.22 % (1172716)Termination reason: Instruction limit % 282.98/40.22 % (1172716)Termination phase: Saturation % 282.98/40.22 % (1172716)Time elapsed: 2.115 s % 282.98/40.22 % (1172716)Peak memory usage: 34 MB % 282.98/40.22 % (1172716)Instructions burned: 3513 (million) % 282.98/40.22 % (1172722)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3076874149:fmbsr=1.6:i=67534_2929 on theBenchmark for (2929ds/67534Mi) % 282.98/40.22 % (1172720)Instruction limit reached! % 282.98/40.22 % (1172720)------------------------------ % 282.98/40.22 % (1172720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.98/40.22 % (1172720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.98/40.22 % (1172720)CaDiCaL version: 2.1.3 % 282.98/40.22 % (1172720)Termination reason: Instruction limit % 282.98/40.22 % (1172720)Termination phase: Saturation % 282.98/40.22 % (1172720)Time elapsed: 0.677 s % 282.98/40.22 % (1172720)Peak memory usage: 27 MB % 282.98/40.22 % (1172720)Instructions burned: 2253 (million) % 282.98/40.22 % (1172724)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2265649847:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2923 on theBenchmark for (2923ds/4591Mi) % 282.98/40.22 % TRYING [5] % 282.98/40.22 % (1172724)Instruction limit reached! % 282.98/40.22 % (1172724)------------------------------ % 282.98/40.22 % (1172724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.98/40.22 % (1172724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.98/40.22 % (1172724)CaDiCaL version: 2.1.3 % 282.98/40.22 % (1172724)Termination reason: Instruction limit % 282.98/40.22 % (1172724)Termination phase: Saturation % 282.98/40.22 % (1172724)Time elapsed: 1.139 s % 282.98/40.22 % (1172724)Peak memory usage: 48 MB % 282.98/40.22 % (1172724)Instructions burned: 4594 (million) % 282.98/40.22 % (1172726)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3603995461:i=29340_2912 on theBenchmark for (2912ds/29340Mi) % 282.98/40.22 % (1172718)Instruction limit reached! % 282.98/40.22 % (1172718)------------------------------ % 282.98/40.22 % (1172718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.98/40.22 % (1172718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.98/40.22 % (1172718)CaDiCaL version: 2.1.3 % 282.98/40.22 % (1172718)Termination reason: Instruction limit % 282.98/40.22 % (1172718)Termination phase: Saturation % 282.98/40.22 % (1172718)Time elapsed: 2.263 s % 282.98/40.22 % (1172718)Peak memory usage: 37 MB % 282.98/40.22 % (1172718)Instructions burned: 3773 (million) % 282.98/40.22 % (1172728)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3050924873:i=5211_2910 on theBenchmark for (2910ds/5211Mi) % 282.98/40.22 % TRYING [7] % 282.98/40.22 % TRYING [5] % 282.98/40.22 % (1172728)Instruction limit reached! % 282.98/40.22 % (1172728)------------------------------ % 282.98/40.22 % (1172728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.98/40.22 % (1172728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.98/40.22 % (1172728)CaDiCaL version: 2.1.3 % 282.98/40.22 % (1172728)Termination reason: Instruction limit % 282.98/40.22 % (1172728)Termination phase: Saturation % 282.98/40.22 % (1172728)Time elapsed: 2.721 s % 282.98/40.22 % (1172728)Peak memory usage: 49 MB % 282.98/40.22 % (1172728)Instructions burned: 5212 (million) % 282.98/40.22 % (1172730)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4257178797:i=5497:nm=2_2883 on theBenchmark for (2883ds/5497Mi) % 282.98/40.22 % (1172730)Cannot represent all propositional literals internally % 300.12/42.73 % (1172730)Refutation not found, incomplete strategy % 300.12/42.73 % (1172730)------------------------------ % 300.12/42.73 % (1172730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.12/42.73 % (1172730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.12/42.73 % (1172730)CaDiCaL version: 2.1.3 % 300.12/42.73 % (1172730)Termination reason: Refutation not found, incomplete strategy % 300.12/42.73 % (1172730)Time elapsed: 0.375 s % 300.12/42.73 % (1172730)Peak memory usage: 25 MB % 300.12/42.73 % (1172730)Instructions burned: 764 (million) % 300.12/42.73 % (1172730)------------------------------ % 300.12/42.73 % (1172730)------------------------------ % 300.12/42.73 % (1172732)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3145881544:fmbsr=2:i=46332_2879 on theBenchmark for (2879ds/46332Mi) % 300.12/42.73 % TRYING [15] % 300.12/42.73 % (1172726)Instruction limit reached! % 300.12/42.73 % (1172726)------------------------------ % 300.12/42.73 % (1172726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.12/42.73 % (1172726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.12/42.73 % (1172726)CaDiCaL version: 2.1.3 % 300.12/42.73 % (1172726)Termination reason: Instruction limit % 300.12/42.73 % (1172726)Termination phase: Saturation % 300.12/42.73 % (1172726)Time elapsed: 7.678 s % 300.12/42.73 % (1172726)Peak memory usage: 210 MB % 300.12/42.73 % (1172726)Instructions burned: 29343 (million) % 300.12/42.73 % (1172734)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1313837769:i=14071_2834 on theBenchmark for (2834ds/14071Mi) % 300.12/42.73 % TRYING [12] % 300.12/42.73 % (1172734)Instruction limit reached! % 300.12/42.73 % (1172734)------------------------------ % 300.12/42.73 % (1172734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.12/42.73 % (1172734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.12/42.73 % (1172734)CaDiCaL version: 2.1.3 % 300.12/42.73 % (1172734)Termination reason: Instruction limit % 300.12/42.73 % (1172734)Termination phase: Finite model building constraint generation % 300.12/42.73 % (1172734)Time elapsed: 2.719 s % 300.12/42.73 % (1172734)Peak memory usage: 865 MB % 300.12/42.73 % (1172734)Instructions burned: 14076 (million) % 300.12/42.73 % (1172736)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1628800968:i=22565:add=on:rawr=on_2806 on theBenchmark for (2806ds/22565Mi) % 300.12/42.73 % (1172699)Instruction limit reached! % 300.12/42.73 % (1172699)------------------------------ % 300.12/42.73 % (1172699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.12/42.73 % (1172699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.12/42.73 % (1172699)CaDiCaL version: 2.1.3 % 300.12/42.73 % (1172699)Termination reason: Instruction limit % 300.12/42.73 % (1172699)Termination phase: Finite model building constraint generation % 300.12/42.73 % (1172699)Time elapsed: 21.512 s % 300.12/42.73 % (1172699)Peak memory usage: 2353 MB % 300.12/42.73 % (1172699)Instructions burned: 54282 (million) % 300.12/42.73 % (1172740)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=154219198:i=8173:av=off_2744 on theBenchmark for (2744ds/8173Mi) % 300.12/42.73 % (1172736)Instruction limit reached! % 300.12/42.73 % (1172736)------------------------------ % 300.12/42.73 % (1172736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.12/42.73 % (1172736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.12/42.73 % (1172736)CaDiCaL version: 2.1.3 % 300.12/42.73 % (1172736)Termination reason: Instruction limit % 300.12/42.73 % (1172736)Termination phase: Saturation % 300.12/42.73 % (1172736)Time elapsed: 6.469 s % 300.12/42.73 % (1172736)Peak memory usage: 106 MB % 300.12/42.73 % (1172736)Instructions burned: 22566 (million) % 300.12/42.73 % (1172742)dis+10_16:1_sil=16000:random_seed=2154427745:i=9155:fsr=off_2742 on theBenchmark for (2742ds/9155Mi) % 300.12/42.73 % TRYING [6] % 300.12/42.73 % (1172732)Instruction limit reached! % 300.12/42.73 % (1172732)------------------------------ % 300.12/42.73 % (1172732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.12/42.73 % (1172732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.12/42.73 % (1172732)CaDiCaL version: 2.1.3 % 300.12/42.73 % (1172732)Termination reason: Instruction limit % 300.12/42.73 % (1172732)Termination phase: Finite model building constraint generation % 300.12/42.73 % (1172732)Time elapsed: 15.554 s % 300.12/42.73 % (1172732)Peak memory usage: 2343 MB % 300.12/42.73 % (1172732)Instructions burned: 46332 (million) % 300.12/42.73 % (1 % 300.12/42.74 Terminated % 300.12/42.74 % Vampire exiting %------------------------------------------------------------------------------