%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV967-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n007.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:26:44 PM UTC 2026 % Result : Timeout 289.83s 43.00s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV967-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n007.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 13:00:11 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 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 % 8.30/1.56 % (2372675)Will run a generic schedule for satisfiability detection. % 8.30/1.56 % (2372681)% WARNING: option uhcvi not known. % 8.30/1.56 % (2372681)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2869674671:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.30/1.56 % (2372683)dis+10_1_sil=32000:sp=arity:random_seed=727819168:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.30/1.56 % (2372680)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1849694534_2999 on theBenchmark for (2999ds/0Mi) % 8.30/1.56 % (2372682)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4288782637:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.30/1.56 % (2372685)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1520140069:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.30/1.56 % (2372684)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2175887318:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.30/1.56 % (2372686)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1977060829:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.30/1.56 % TRYING [1] % 8.30/1.56 % TRYING [2] % 8.30/1.56 % TRYING [3] % 8.30/1.56 % (2372686)Instruction limit reached! % 8.30/1.56 % (2372686)------------------------------ % 8.30/1.56 % (2372686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.30/1.56 % (2372686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.30/1.56 % (2372686)CaDiCaL version: 2.1.3 % 8.30/1.56 % (2372686)Termination reason: Instruction limit % 8.30/1.56 % (2372686)Termination phase: Saturation % 8.30/1.56 % (2372686)Time elapsed: 0.058 s % 8.30/1.56 % (2372686)Peak memory usage: 11 MB % 8.30/1.56 % (2372686)Instructions burned: 160 (million) % 8.30/1.56 % (2372684)Instruction limit reached! % 8.30/1.56 % (2372684)------------------------------ % 8.30/1.56 % (2372684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.30/1.56 % (2372684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.30/1.56 % (2372684)CaDiCaL version: 2.1.3 % 8.30/1.56 % (2372684)Termination reason: Instruction limit % 8.30/1.56 % (2372684)Termination phase: Saturation % 8.30/1.56 % (2372684)Time elapsed: 0.059 s % 8.30/1.56 % (2372684)Peak memory usage: 12 MB % 8.30/1.56 % (2372684)Instructions burned: 116 (million) % 8.30/1.56 % (2372683)Instruction limit reached! % 8.30/1.56 % (2372683)------------------------------ % 8.30/1.56 % (2372683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.30/1.56 % (2372683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.30/1.56 % (2372683)CaDiCaL version: 2.1.3 % 8.30/1.56 % (2372683)Termination reason: Instruction limit % 8.30/1.56 % (2372683)Termination phase: Saturation % 8.30/1.56 % (2372683)Time elapsed: 0.066 s % 8.30/1.56 % (2372683)Peak memory usage: 12 MB % 8.30/1.56 % (2372683)Instructions burned: 104 (million) % 8.30/1.56 % (2372685)Instruction limit reached! % 8.30/1.56 % (2372685)------------------------------ % 8.30/1.56 % (2372685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.30/1.56 % (2372685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.30/1.56 % (2372685)CaDiCaL version: 2.1.3 % 8.30/1.56 % (2372685)Termination reason: Instruction limit % 8.30/1.56 % (2372685)Termination phase: Saturation % 8.30/1.56 % (2372685)Time elapsed: 0.078 s % 8.30/1.56 % (2372685)Peak memory usage: 12 MB % 8.30/1.56 % (2372685)Instructions burned: 132 (million) % 8.30/1.56 % (2372694)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=372437745:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.30/1.56 % (2372695)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1917643738:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.30/1.56 % (2372696)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=4243038426:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.30/1.56 % (2372697)ott-21_1_sil=16000:fs=off:random_seed=1104186453:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.30/1.56 % TRYING [1] % 8.30/1.56 % TRYING [2] % 8.30/1.56 % TRYING [3] % 8.30/1.56 % (2372695)Instruction limit reached! % 8.30/1.56 % (2372695)------------------------------ % 8.30/1.56 % (2372695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.30/1.56 % (2372695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.56/4.42 % (2372695)CaDiCaL version: 2.1.3 % 29.56/4.42 % (2372695)Termination reason: Instruction limit % 29.56/4.42 % (2372695)Termination phase: Saturation % 29.56/4.42 % (2372695)Time elapsed: 0.084 s % 29.56/4.42 % (2372695)Peak memory usage: 13 MB % 29.56/4.42 % (2372695)Instructions burned: 131 (million) % 29.56/4.42 % (2372702)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3262073438:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 29.56/4.42 % (2372697)Instruction limit reached! % 29.56/4.42 % (2372697)------------------------------ % 29.56/4.42 % (2372697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.56/4.42 % (2372697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.56/4.42 % (2372697)CaDiCaL version: 2.1.3 % 29.56/4.42 % (2372697)Termination reason: Instruction limit % 29.56/4.42 % (2372697)Termination phase: Saturation % 29.56/4.42 % (2372697)Time elapsed: 0.094 s % 29.56/4.42 % (2372697)Peak memory usage: 12 MB % 29.56/4.42 % (2372697)Instructions burned: 180 (million) % 29.56/4.42 % (2372704)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2410867386:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 29.56/4.42 % TRYING [1] % 29.56/4.42 % TRYING [2] % 29.56/4.42 % TRYING [4] % 29.56/4.42 % TRYING [3] % 29.56/4.42 % (2372694)Instruction limit reached! % 29.56/4.42 % (2372694)------------------------------ % 29.56/4.42 % (2372694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.56/4.42 % (2372694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.56/4.42 % (2372694)CaDiCaL version: 2.1.3 % 29.56/4.42 % (2372694)Termination reason: Instruction limit % 29.56/4.42 % (2372694)Termination phase: Finite model building constraint generation % 29.56/4.42 % (2372694)Time elapsed: 0.283 s % 29.56/4.42 % (2372694)Peak memory usage: 49 MB % 29.56/4.42 % (2372694)Instructions burned: 717 (million) % 29.56/4.42 % (2372706)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=305942424:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 29.56/4.42 % (2372702)Instruction limit reached! % 29.56/4.42 % (2372702)------------------------------ % 29.56/4.42 % (2372702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.56/4.42 % (2372702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.56/4.42 % (2372702)CaDiCaL version: 2.1.3 % 29.56/4.42 % (2372702)Termination reason: Instruction limit % 29.56/4.42 % (2372702)Termination phase: Saturation % 29.56/4.42 % (2372702)Time elapsed: 0.284 s % 29.56/4.42 % (2372702)Peak memory usage: 14 MB % 29.56/4.42 % (2372702)Instructions burned: 477 (million) % 29.56/4.42 % (2372696)Instruction limit reached! % 29.56/4.42 % (2372696)------------------------------ % 29.56/4.42 % (2372696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.56/4.42 % (2372696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.56/4.42 % (2372696)CaDiCaL version: 2.1.3 % 29.56/4.42 % (2372696)Termination reason: Instruction limit % 29.56/4.42 % (2372696)Termination phase: Saturation % 29.56/4.42 % (2372696)Time elapsed: 0.398 s % 29.56/4.42 % (2372696)Peak memory usage: 17 MB % 29.56/4.42 % (2372696)Instructions burned: 685 (million) % 29.56/4.42 % (2372708)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2432601890:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 29.56/4.42 % (2372709)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=310362167: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) % 29.56/4.42 % (2372708)Cannot represent all propositional literals internally % 29.56/4.42 % (2372708)Refutation not found, incomplete strategy % 29.56/4.42 % (2372708)------------------------------ % 29.56/4.42 % (2372708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.56/4.42 % (2372708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.56/4.42 % (2372708)CaDiCaL version: 2.1.3 % 29.56/4.42 % (2372708)Termination reason: Refutation not found, incomplete strategy % 29.56/4.42 % (2372708)Time elapsed: 0.019 s % 29.56/4.42 % (2372708)Peak memory usage: 11 MB % 29.56/4.42 % (2372708)Instructions burned: 37 (million) % 29.56/4.42 % (2372708)------------------------------ % 29.56/4.42 % (2372708)------------------------------ % 29.56/4.42 % (2372712)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2173299961:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 105.04/15.10 % (2372704)Instruction limit reached! % 105.04/15.10 % (2372704)------------------------------ % 105.04/15.10 % (2372704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.04/15.10 % (2372704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.04/15.10 % (2372704)CaDiCaL version: 2.1.3 % 105.04/15.10 % (2372704)Termination reason: Instruction limit % 105.04/15.10 % (2372704)Termination phase: Finite model building SAT solving % 105.04/15.10 % (2372704)Time elapsed: 0.386 s % 105.04/15.10 % (2372704)Peak memory usage: 41 MB % 105.04/15.10 % (2372704)Instructions burned: 867 (million) % 105.04/15.10 % (2372714)fmb+10_1_sil=64000:random_seed=1216163295:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 105.04/15.10 % TRYING [1] % 105.04/15.10 % TRYING [2] % 105.04/15.10 % TRYING [3] % 105.04/15.10 % (2372712)Instruction limit reached! % 105.04/15.10 % (2372712)------------------------------ % 105.04/15.10 % (2372712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.04/15.10 % (2372712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.04/15.10 % (2372712)CaDiCaL version: 2.1.3 % 105.04/15.10 % (2372712)Termination reason: Instruction limit % 105.04/15.10 % (2372712)Termination phase: Saturation % 105.04/15.10 % (2372712)Time elapsed: 0.392 s % 105.04/15.10 % (2372712)Peak memory usage: 14 MB % 105.04/15.10 % (2372712)Instructions burned: 879 (million) % 105.04/15.10 % (2372709)Instruction limit reached! % 105.04/15.10 % (2372709)------------------------------ % 105.04/15.10 % (2372709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.04/15.10 % (2372709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.04/15.10 % (2372709)CaDiCaL version: 2.1.3 % 105.04/15.10 % (2372709)Termination reason: Instruction limit % 105.04/15.10 % (2372709)Termination phase: Saturation % 105.04/15.10 % (2372709)Time elapsed: 0.423 s % 105.04/15.10 % (2372709)Peak memory usage: 19 MB % 105.04/15.10 % (2372709)Instructions burned: 692 (million) % 105.04/15.10 % (2372716)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3196088473:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 105.04/15.10 % (2372717)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=210372748:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 105.04/15.10 % (2372716)Cannot represent all propositional literals internally % 105.04/15.10 % (2372716)Refutation not found, incomplete strategy % 105.04/15.10 % (2372716)------------------------------ % 105.04/15.10 % (2372716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.04/15.10 % (2372716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.04/15.10 % (2372716)CaDiCaL version: 2.1.3 % 105.04/15.10 % (2372716)Termination reason: Refutation not found, incomplete strategy % 105.04/15.10 % (2372716)Time elapsed: 0.019 s % 105.04/15.10 % (2372716)Peak memory usage: 11 MB % 105.04/15.10 % (2372716)Instructions burned: 37 (million) % 105.04/15.10 % (2372716)------------------------------ % 105.04/15.10 % (2372716)------------------------------ % 105.04/15.10 % TRYING [8] % 105.04/15.10 % (2372720)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3167714312:i=5131_2990 on theBenchmark for (2990ds/5131Mi) % 105.04/15.10 % (2372706)Instruction limit reached! % 105.04/15.10 % (2372706)------------------------------ % 105.04/15.10 % (2372706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.04/15.10 % (2372706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.04/15.10 % (2372706)CaDiCaL version: 2.1.3 % 105.04/15.10 % (2372706)Termination reason: Instruction limit % 105.04/15.10 % (2372706)Termination phase: Saturation % 105.04/15.10 % (2372706)Time elapsed: 0.687 s % 105.04/15.10 % (2372706)Peak memory usage: 20 MB % 105.04/15.10 % (2372706)Instructions burned: 1179 (million) % 105.04/15.10 % (2372722)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1454006484:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi) % 105.04/15.10 % (2372717)Instruction limit reached! % 105.04/15.10 % (2372717)------------------------------ % 105.04/15.10 % (2372717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.04/15.10 % (2372717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.04/15.10 % (2372717)CaDiCaL version: 2.1.3 % 105.04/15.10 % (2372717)Termination reason: Instruction limit % 105.04/15.10 % (2372717)Termination phase: Finite model building constraint generation % 105.04/15.10 % (2372717)Time elapsed: 0.318 s % 105.04/15.10 % (2372717)Peak memory usage: 67 MB % 105.04/15.10 % (2372717)Instructions burned: 921 (million) % 105.04/15.10 % TRYING [4] % 105.04/15.10 % (2372724)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3488353229:i=6324_2986 on theBenchmark for (2986ds/6324Mi) % 196.29/27.92 % (2372724)Cannot represent all propositional literals internally % 196.29/27.92 % (2372724)Refutation not found, incomplete strategy % 196.29/27.92 % (2372724)------------------------------ % 196.29/27.92 % (2372724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.29/27.92 % (2372724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.29/27.92 % (2372724)CaDiCaL version: 2.1.3 % 196.29/27.92 % (2372724)Termination reason: Refutation not found, incomplete strategy % 196.29/27.92 % (2372724)Time elapsed: 0.018 s % 196.29/27.92 % (2372724)Peak memory usage: 11 MB % 196.29/27.92 % (2372724)Instructions burned: 34 (million) % 196.29/27.92 % (2372724)------------------------------ % 196.29/27.92 % (2372724)------------------------------ % 196.29/27.92 % (2372726)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3970610217:fmbsr=2.30978:i=2174_2986 on theBenchmark for (2986ds/2174Mi) % 196.29/27.92 % (2372726)Cannot represent all propositional literals internally % 196.29/27.92 % (2372726)Refutation not found, incomplete strategy % 196.29/27.92 % (2372726)------------------------------ % 196.29/27.92 % (2372726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.29/27.92 % (2372726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.29/27.92 % (2372726)CaDiCaL version: 2.1.3 % 196.29/27.92 % (2372726)Termination reason: Refutation not found, incomplete strategy % 196.29/27.92 % (2372726)Time elapsed: 0.076 s % 196.29/27.92 % (2372726)Peak memory usage: 12 MB % 196.29/27.92 % (2372726)Instructions burned: 155 (million) % 196.29/27.92 % (2372726)------------------------------ % 196.29/27.92 % (2372726)------------------------------ % 196.29/27.92 % (2372728)ott-2_1_sil=16000:newcnf=on:random_seed=1409648103:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2985 on theBenchmark for (2985ds/869Mi) % 196.29/27.92 % (2372728)Instruction limit reached! % 196.29/27.92 % (2372728)------------------------------ % 196.29/27.92 % (2372728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.29/27.92 % (2372728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.29/27.92 % (2372728)CaDiCaL version: 2.1.3 % 196.29/27.92 % (2372728)Termination reason: Instruction limit % 196.29/27.92 % (2372728)Termination phase: Saturation % 196.29/27.92 % (2372728)Time elapsed: 0.292 s % 196.29/27.92 % (2372728)Peak memory usage: 11 MB % 196.29/27.92 % (2372728)Instructions burned: 869 (million) % 196.29/27.92 % (2372730)ott+10_1_sil=32000:tgt=ground:random_seed=1864229724:i=5114:av=off_2982 on theBenchmark for (2982ds/5114Mi) % 196.29/27.92 % (2372722)Instruction limit reached! % 196.29/27.92 % (2372722)------------------------------ % 196.29/27.92 % (2372722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.29/27.92 % (2372722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.29/27.92 % (2372722)CaDiCaL version: 2.1.3 % 196.29/27.92 % (2372722)Termination reason: Instruction limit % 196.29/27.92 % (2372722)Termination phase: Saturation % 196.29/27.92 % (2372722)Time elapsed: 0.958 s % 196.29/27.92 % (2372722)Peak memory usage: 38 MB % 196.29/27.92 % (2372722)Instructions burned: 1473 (million) % 196.29/27.92 % (2372732)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1956683817:i=54282_2979 on theBenchmark for (2979ds/54282Mi) % 196.29/27.92 % TRYING [1] % 196.29/27.92 % TRYING [2] % 196.29/27.92 % TRYING [5] % 196.29/27.92 % TRYING [3] % 196.29/27.92 % TRYING [4] % 196.29/27.92 % (2372720)Instruction limit reached! % 196.29/27.92 % (2372720)------------------------------ % 196.29/27.92 % (2372720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.29/27.92 % (2372720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.29/27.92 % (2372720)CaDiCaL version: 2.1.3 % 196.29/27.92 % (2372720)Termination reason: Instruction limit % 196.29/27.92 % (2372720)Termination phase: Saturation % 196.29/27.92 % (2372720)Time elapsed: 1.833 s % 196.29/27.92 % (2372720)Peak memory usage: 16 MB % 196.29/27.92 % (2372720)Instructions burned: 5131 (million) % 196.29/27.92 % (2372734)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1023675933:i=3512:aac=none_2971 on theBenchmark for (2971ds/3512Mi) % 196.29/27.92 % (2372734)Instruction limit reached! % 196.29/27.92 % (2372734)------------------------------ % 196.29/27.92 % (2372734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.29/27.92 % (2372734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.29/27.92 % (2372734)CaDiCaL version: 2.1.3 % 196.29/27.92 % (2372734)Termination reason: Instruction limit % 262.24/37.28 % (2372734)Termination phase: Saturation % 262.24/37.28 % (2372734)Time elapsed: 1.318 s % 262.24/37.28 % (2372734)Peak memory usage: 15 MB % 262.24/37.28 % (2372734)Instructions burned: 3513 (million) % 262.24/37.28 % (2372736)dis+21_1_sil=32000:sas=cadical:random_seed=3979950057:i=3773:amm=off_2958 on theBenchmark for (2958ds/3773Mi) % 262.24/37.28 % TRYING [5] % 262.24/37.28 % (2372730)Instruction limit reached! % 262.24/37.28 % (2372730)------------------------------ % 262.24/37.28 % (2372730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.24/37.28 % (2372730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.24/37.28 % (2372730)CaDiCaL version: 2.1.3 % 262.24/37.28 % (2372730)Termination reason: Instruction limit % 262.24/37.28 % (2372730)Termination phase: Saturation % 262.24/37.28 % (2372730)Time elapsed: 2.805 s % 262.24/37.28 % (2372730)Peak memory usage: 44 MB % 262.24/37.28 % (2372730)Instructions burned: 5115 (million) % 262.24/37.28 % (2372738)ott+11_1_sil=16000:gs=on:random_seed=3191577519:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2954 on theBenchmark for (2954ds/2251Mi) % 262.24/37.28 % TRYING [5] % 262.24/37.28 % (2372738)Instruction limit reached! % 262.24/37.28 % (2372738)------------------------------ % 262.24/37.28 % (2372738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.24/37.28 % (2372738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.24/37.28 % (2372738)CaDiCaL version: 2.1.3 % 262.24/37.28 % (2372738)Termination reason: Instruction limit % 262.24/37.28 % (2372738)Termination phase: Saturation % 262.24/37.28 % (2372738)Time elapsed: 1.280 s % 262.24/37.28 % (2372738)Peak memory usage: 27 MB % 262.24/37.28 % (2372738)Instructions burned: 2252 (million) % 262.24/37.28 % (2372740)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4168781723:fmbsr=1.6:i=67534_2941 on theBenchmark for (2941ds/67534Mi) % 262.24/37.28 % (2372736)Instruction limit reached! % 262.24/37.28 % (2372736)------------------------------ % 262.24/37.28 % (2372736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.24/37.28 % (2372736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.24/37.28 % (2372736)CaDiCaL version: 2.1.3 % 262.24/37.28 % (2372736)Termination reason: Instruction limit % 262.24/37.28 % (2372736)Termination phase: Saturation % 262.24/37.28 % (2372736)Time elapsed: 2.021 s % 262.24/37.28 % (2372736)Peak memory usage: 31 MB % 262.24/37.28 % (2372736)Instructions burned: 3774 (million) % 262.24/37.28 % (2372742)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2106620955:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2937 on theBenchmark for (2937ds/4591Mi) % 262.24/37.28 % (2372742)Instruction limit reached! % 262.24/37.28 % (2372742)------------------------------ % 262.24/37.28 % (2372742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.24/37.28 % (2372742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.24/37.28 % (2372742)CaDiCaL version: 2.1.3 % 262.24/37.28 % (2372742)Termination reason: Instruction limit % 262.24/37.28 % (2372742)Termination phase: Saturation % 262.24/37.28 % (2372742)Time elapsed: 1.426 s % 262.24/37.28 % (2372742)Peak memory usage: 12 MB % 262.24/37.28 % (2372742)Instructions burned: 4591 (million) % 262.24/37.28 % (2372744)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2866637590:i=29340_2923 on theBenchmark for (2923ds/29340Mi) % 262.24/37.28 % (2372714)Instruction limit reached! % 262.24/37.28 % (2372714)------------------------------ % 262.24/37.28 % (2372714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.24/37.28 % (2372714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.24/37.28 % (2372714)CaDiCaL version: 2.1.3 % 262.24/37.28 % (2372714)Termination reason: Instruction limit % 262.24/37.28 % (2372714)Termination phase: Finite model building constraint generation % 262.24/37.28 % (2372714)Time elapsed: 12.195 s % 262.24/37.28 % (2372714)Peak memory usage: 841 MB % 262.24/37.28 % (2372714)Instructions burned: 22061 (million) % 262.24/37.28 % (2372746)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3595697328:i=5211_2870 on theBenchmark for (2870ds/5211Mi) % 262.24/37.28 % TRYING [7] % 262.24/37.28 % TRYING [6] % 262.24/37.28 % (2372746)Instruction limit reached! % 262.24/37.28 % (2372746)------------------------------ % 262.24/37.28 % (2372746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 262.24/37.28 % (2372746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.24/37.28 % (2372746)CaDiCaL version: 2.1.3 % 262.24/37.28 % (2372746)Termination reason: Instruction limit % 289.83/43.00 % (2372746)Termination phase: Saturation % 289.83/43.00 % (2372746)Time elapsed: 1.888 s % 289.83/43.00 % (2372746)Peak memory usage: 19 MB % 289.83/43.00 % (2372746)Instructions burned: 5213 (million) % 289.83/43.00 % (2372748)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1653875066:i=5497:nm=2_2851 on theBenchmark for (2851ds/5497Mi) % 289.83/43.00 % (2372748)Cannot represent all propositional literals internally % 289.83/43.00 % (2372748)Refutation not found, incomplete strategy % 289.83/43.00 % (2372748)------------------------------ % 289.83/43.00 % (2372748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/43.00 % (2372748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/43.00 % (2372748)CaDiCaL version: 2.1.3 % 289.83/43.00 % (2372748)Termination reason: Refutation not found, incomplete strategy % 289.83/43.00 % (2372748)Time elapsed: 0.018 s % 289.83/43.00 % (2372748)Peak memory usage: 11 MB % 289.83/43.00 % (2372748)Instructions burned: 34 (million) % 289.83/43.00 % (2372748)------------------------------ % 289.83/43.00 % (2372748)------------------------------ % 289.83/43.00 % (2372750)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1038626133:fmbsr=2:i=46332_2850 on theBenchmark for (2850ds/46332Mi) % 289.83/43.00 % (2372750)Cannot represent all propositional literals internally % 289.83/43.00 % (2372750)Refutation not found, incomplete strategy % 289.83/43.00 % (2372750)------------------------------ % 289.83/43.00 % (2372750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/43.00 % (2372750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/43.00 % (2372750)CaDiCaL version: 2.1.3 % 289.83/43.00 % (2372750)Termination reason: Refutation not found, incomplete strategy % 289.83/43.00 % (2372750)Time elapsed: 0.020 s % 289.83/43.00 % (2372750)Peak memory usage: 10 MB % 289.83/43.00 % (2372750)Instructions burned: 41 (million) % 289.83/43.00 % (2372750)------------------------------ % 289.83/43.00 % (2372750)------------------------------ % 289.83/43.00 % (2372752)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=297071137:i=14071_2850 on theBenchmark for (2850ds/14071Mi) % 289.83/43.00 % TRYING [12] % 289.83/43.00 % TRYING [6] % 289.83/43.00 % (2372752)Instruction limit reached! % 289.83/43.00 % (2372752)------------------------------ % 289.83/43.00 % (2372752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/43.00 % (2372752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/43.00 % (2372752)CaDiCaL version: 2.1.3 % 289.83/43.00 % (2372752)Termination reason: Instruction limit % 289.83/43.00 % (2372752)Termination phase: Finite model building constraint generation % 289.83/43.00 % (2372752)Time elapsed: 4.830 s % 289.83/43.00 % (2372752)Peak memory usage: 891 MB % 289.83/43.00 % (2372752)Instructions burned: 14074 (million) % 289.83/43.00 % (2372754)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1861676930:i=22565:add=on:rawr=on_2800 on theBenchmark for (2800ds/22565Mi) % 289.83/43.00 % (2372744)Instruction limit reached! % 289.83/43.00 % (2372744)------------------------------ % 289.83/43.00 % (2372744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/43.00 % (2372744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/43.00 % (2372744)CaDiCaL version: 2.1.3 % 289.83/43.00 % (2372744)Termination reason: Instruction limit % 289.83/43.00 % (2372744)Termination phase: Saturation % 289.83/43.00 % (2372744)Time elapsed: 15.381 s % 289.83/43.00 % (2372744)Peak memory usage: 202 MB % 289.83/43.00 % (2372744)Instructions burned: 29341 (million) % 289.83/43.00 % (2372756)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=68638765:i=8173:av=off_2768 on theBenchmark for (2768ds/8173Mi) % 289.83/43.00 % (2372732)Instruction limit reached! % 289.83/43.00 % (2372732)------------------------------ % 289.83/43.00 % (2372732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/43.00 % (2372732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/43.00 % (2372732)CaDiCaL version: 2.1.3 % 289.83/43.00 % (2372732)Termination reason: Instruction limit % 289.83/43.00 % (2372732)Termination phase: Finite model building constraint generation % 289.83/43.00 % (2372732)Time elapsed: 23.985 s % 289.83/43.00 % (2372732)Peak memory usage: 2512 MB % 289.83/43.00 % (2372732)Instructions burned: 54283 (million) % 289.83/43.00 % (2372758)dis+10_16:1_sil=16000:random_seed=3251488694:i=9155:fsr=off_2735 on theBenchmark for (2735ds/9155Mi) % 289.83/43.00 % (2372756)Instruction limit reached! % 289.83/43.00 % (2372756)------------------------------ % 303.61/43.07 % (2372756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.61/43.07 % (2372756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.61/43.07 % (2372756)CaDiCaL version: 2.1.3 % 303.61/43.07 % (2372756)Termination reason: Instruction limit % 303.61/43.07 % (2372756)Termination phase: Saturation % 303.61/43.07 % (2372756)Time elapsed: 4.561 s % 303.61/43.07 % (2372756)Peak memory usage: 85 MB % 303.61/43.07 % (2372756)Instructions burned: 8174 (million) % 303.61/43.07 % (2372760)ott-3_8_sil=64000:random_seed=527303464:i=20139:bs=on_2722 on theBenchmark for (2722ds/20139Mi) % 303.61/43.07 % (2372740)Instruction limit reached! % 303.61/43.07 % (2372740)------------------------------ % 303.61/43.07 % (2372740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.61/43.07 % (2372740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.61/43.07 % (2372740)CaDiCaL version: 2.1.3 % 303.61/43.07 % (2372740)Termination reason: Instruction limit % 303.61/43.07 % (2372740)Termination phase: Finite model building constraint generation % 303.61/43.07 % (2372740)Time elapsed: 24.331 s % 303.61/43.07 % (2372740)Peak memory usage: 4004 MB % 303.61/43.07 % (2372740)Instructions burned: 67535 (million) % 303.61/43.07 % (2372762)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2137567739:fmbsr=2:i=32576_2691 on theBenchmark for (2691ds/32576Mi) % 303.61/43.07 % (2372758)Instruction limit reached! % 303.61/43.07 % (2372758)------------------------------ % 303.61/43.07 % (2372758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.61/43.07 % (2372758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.61/43.07 % (2372758)CaDiCaL version: 2.1.3 % 303.61/43.07 % (2372758)Termination reason: Instruction limit % 303.61/43.07 % (2372758)Termination phase: Saturation % 303.61/43.07 % (2372758)Time elapsed: 4.416 s % 303.61/43.07 % (2372758)Peak memory usage: 62 MB % 303.61/43.07 % (2372758)Instructions burned: 9156 (million) % 303.61/43.07 % TRYING [9] % 303.61/43.07 % (2372764)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3675211865:i=11404_2691 on theBenchmark for (2691ds/11404Mi) % 303.61/43.07 % (2372754)Instruction limit reached! % 303.61/43.07 % (2372754)------------------------------ % 303.61/43.07 % (2372754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.61/43.07 % (2372754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.61/43.07 % (2372754)CaDiCaL version: 2.1.3 % 303.61/43.07 % (2372754)Termination reason: Instruction limit % 303.61/43.07 % (2372754)Termination phase: Saturation % 303.61/43.07 % (2372754)Time elapsed: 11.590 s % 303.61/43.07 % (2372754)Peak memory usage: 205 MB % 303.61/43.07 % (2372754)Instructions burned: 22566 (million) % 303.61/43.07 % (2372766)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1997962734:i=14134_2684 on theBenchmark for (2684ds/14134Mi) % 303.61/43.07 % (2372760)Instruction limit reached! % 303.61/43.07 % (2372760)------------------------------ % 303.61/43.07 % (2372760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.61/43.07 % (2372760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.61/43.07 % (2372760)CaDiCaL version: 2.1.3 % 303.61/43.07 % (2372760)Termination reason: Instruction limit % 303.61/43.07 % (2372760)Termination phase: Saturation % 303.61/43.07 % (2372760)Time elapsed: 5.945 s % 303.61/43.07 % (2372760)Peak memory usage: 12 MB % 303.61/43.07 % (2372760)Instructions burned: 20142 (million) % 303.61/43.07 % (2372768)dis+33_16_sil=32000:sac=on:random_seed=3678953123:i=15851:nm=0_2663 on theBenchmark for (2663ds/15851Mi) % 303.61/43.07 % (2372766)Instruction limit reached! % 303.61/43.07 % (2372766)------------------------------ % 303.61/43.07 % (2372766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.61/43.07 % (2372766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.61/43.07 % (2372766)CaDiCaL version: 2.1.3 % 303.61/43.07 % (2372766)Termination reason: Instruction limit % 303.61/43.07 % (2372766)Termination phase: Saturation % 303.61/43.07 % (2372766)Time elapsed: 4.203 s % 303.61/43.07 % (2372766)Peak memory usage: 12 MB % 303.61/43.07 % (2372766)Instructions burned: 14134 (million) % 303.61/43.07 % (2372770)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1111765582:avsq=on:i=17627:add=on:amm=off_2642 on theBenchmark for (2642ds/17627Mi) % 303.61/43.07 % (2372764)Instruction limit reached! % 303.61/43.07 % (2372764)------------------------------ % 303.61/43.07 % (2372764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.61/43.07 % (2372764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.61/43.07 % (2372764)CaDiCaL version: 2.1.3 % 303.61/43.07 % (2372764)Termination reason: Instruction limit % 303.61/43.07 % (2372764)Termination phase: Saturation % 303.61/43.07 % (2372764)Time elapsed: 6.186 s % 303.61/43.07 % (2372764)Peak memory usage: 77 MB % 303.61/43.07 % (2372764)Instructions burned: 11407 (million) % 303.61/43.07 % (2372772)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2098703023:s2a=on:i=53295_2629 on theBenchmark for (2629ds/53295Mi) % 303.61/43.07 % (2372681)Instruction limit reached! % 303.61/43.07 % (2372681)------------------------------ % 303.61/43.07 % (2372681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.61/43.07 % (2372681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.61/43.07 % (2372681)CaDiCaL version: 2.1.3 % 303.61/43.07 % (2372681)Termination reason: Instruction limit % 303.61/43.07 % (2372681)Termination phase: Saturation % 303.61/43.07 % (2372681)Time elapsed: 39.009 s % 303.61/43.07 % (2372681)Peak memory usage: 198 MB % 303.61/43.07 % (2372681)Instructions burned: 135535 (million) % 303.61/43.07 % (2372774)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2709693380:i=26857:ins=20_2609 on theBenchmark for (2609ds/26857Mi) % 303.61/43.07 % (2372774)Cannot represent all propositional literals internally % 303.61/43.07 % (2372774)Refutation not found, incomplete strategy % 303.61/43.07 % (2372774)------------------------------ % 303.61/43.07 % (2372774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.61/43.07 % (2372774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.61/43.07 % (2372774)CaDiCaL version: 2.1.3 % 303.61/43.07 % (2372774)Termination reason: Refutation not found, incomplete strategy % 303.61/43.07 % (2372774)Time elapsed: 0.010 s % 303.61/43.07 % (2372774)Peak memory usage: 11 MB % 303.61/43.07 % (2372774)Instructions burned: 37 (million) % 303.61/43.07 % (2372774)------------------------------ % 303.61/43.07 % (2372774)------------------------------ % 303.61/43.07 % (2372776)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3945580620:i=28120:bs=on:fsr=off_2609 on theBenchmark for (2609ds/28120Mi) % 303.61/43.07 % (2372768)Instruction limit reached! % 303.61/43.07 % (2372768)------------------------------ % 303.61/43.07 % (2372768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.61/43.07 % (2372768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.61/43.07 % (2372768)CaDiCaL version: 2.1.3 % 303.61/43.07 % (2372768)Termination reason: Instruction limit % 303.61/43.07 % (2372768)Termination phase: Saturation % 303.61/43.07 % (2372768)Time elapsed: 8.101 s % 303.61/43.07 % (2372768)Peak memory usage: 94 MB % 303.61/43.07 % (2372768)Instructions burned: 15853 (million) % 303.61/43.07 % (2372778)fmb+10_1_sil=256000:fmbss=7:random_seed=2625500048:fmbsr=1.6:i=182295_2581 on theBenchmark for (2581ds/182295Mi) % 303.61/43.07 % (2372762)Instruction limit reached! % 303.61/43.07 % (2372762)------------------------------ % 303.61/43.07 % (2372762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.61/43.07 % (2372762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.61/43.07 % (2372762)CaDiCaL version: 2.1.3 % 303.61/43.07 % (2372762)Termination reason: Instruction limit % 303.61/43.07 % (2372762)Termination phase: Finite model building constraint generation % 303.61/43.07 % (2372762)Time elapsed: 11.568 s % 303.61/43.07 % (2372762)Peak memory usage: 2062 MB % 303.61/43.07 % (2372762)Instructions burned: 32576 (million) % 303.61/43.07 % (2372780)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1491887829:i=44625:gsp=on_2573 on theBenchmark for (2573ds/44625Mi) % 303.61/43.07 % (2372780)Cannot represent all propositional literals internally % 303.61/43.07 % (2372780)Refutation not found, incomplete strategy % 303.61/43.07 % (2372780)------------------------------ % 303.61/43.07 % (2372780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 303.61/43.07 % (2372780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 303.61/43.07 % (2372780)CaDiCaL version: 2.1.3 % 303.61/43.07 % (2372780)Termination reason: Refutation not found, incomplete strategy % 303.61/43.07 % (2372780)Time elapsed: 0.018 s % 303.61/43.07 % (2372780)Peak memory usage: 10 MB % 303.61/43.07 % (2372780)Instructions burned: 35 (million) % 303.61/43.07 % (2372780)------------------------------ % 303.61/43.07 % (2372780)------------------------------ % 303.61/43.07 % (2372782)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2546713371:i=160505_2572 on theBenchmark for (2572ds/160505Mi) % 303.61/43.07 % (2372782)Cannot represent all propositional lit % 303.61/43.07 Terminated % 303.61/43.07 % Vampire exiting % 303.61/43.07 Terminated %------------------------------------------------------------------------------