%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV754-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 : n012.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:21 PM UTC 2026 % Result : Timeout 300.63s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWV754-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.00/0.11 % Computer : n012.cluster.edu % 0.00/0.11 % Model : x86_64 x86_64 % 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.11 % Memory : 8046.5625MB % 0.00/0.11 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 12:26:19 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.12 Running first-order model finding % 0.09/0.12 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 % 10.11/1.67 % (3345665)Will run a generic schedule for satisfiability detection. % 10.11/1.67 % (3345671)% WARNING: option uhcvi not known. % 10.11/1.67 % (3345673)dis+10_1_sil=32000:sp=arity:random_seed=1724167100:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 10.11/1.67 % (3345671)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2074229967:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 10.11/1.67 % (3345670)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1086341602_2999 on theBenchmark for (2999ds/0Mi) % 10.11/1.67 % (3345672)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1566986693:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 10.11/1.67 % (3345674)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2492180474:i=116_2999 on theBenchmark for (2999ds/116Mi) % 10.11/1.67 % (3345675)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1788014772:i=131_2999 on theBenchmark for (2999ds/131Mi) % 10.11/1.67 % (3345676)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4002105439:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 10.11/1.67 % (3345673)Instruction limit reached! % 10.11/1.67 % (3345673)------------------------------ % 10.11/1.67 % (3345673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.11/1.67 % (3345673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/1.67 % (3345673)CaDiCaL version: 2.1.3 % 10.11/1.67 % (3345673)Termination reason: Instruction limit % 10.11/1.67 % (3345673)Termination phase: Saturation % 10.11/1.67 % (3345673)Time elapsed: 0.035 s % 10.11/1.67 % (3345673)Peak memory usage: 13 MB % 10.11/1.67 % (3345673)Instructions burned: 103 (million) % 10.11/1.67 % (3345674)Instruction limit reached! % 10.11/1.67 % (3345674)------------------------------ % 10.11/1.67 % (3345674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.11/1.67 % (3345674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/1.67 % (3345674)CaDiCaL version: 2.1.3 % 10.11/1.67 % (3345674)Termination reason: Instruction limit % 10.11/1.67 % (3345674)Termination phase: Saturation % 10.11/1.67 % (3345674)Time elapsed: 0.037 s % 10.11/1.67 % (3345674)Peak memory usage: 13 MB % 10.11/1.67 % (3345674)Instructions burned: 117 (million) % 10.11/1.67 % (3345675)Instruction limit reached! % 10.11/1.67 % (3345675)------------------------------ % 10.11/1.67 % (3345675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.11/1.67 % (3345675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/1.67 % (3345675)CaDiCaL version: 2.1.3 % 10.11/1.67 % (3345675)Termination reason: Instruction limit % 10.11/1.67 % (3345675)Termination phase: Saturation % 10.11/1.67 % (3345675)Time elapsed: 0.045 s % 10.11/1.67 % (3345675)Peak memory usage: 14 MB % 10.11/1.67 % (3345675)Instructions burned: 132 (million) % 10.11/1.67 % (3345684)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2009814810:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 10.11/1.67 % (3345685)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3742063922:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 10.11/1.67 % (3345676)Instruction limit reached! % 10.11/1.67 % (3345676)------------------------------ % 10.11/1.67 % (3345676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.11/1.67 % (3345676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/1.67 % (3345676)CaDiCaL version: 2.1.3 % 10.11/1.67 % (3345676)Termination reason: Instruction limit % 10.11/1.67 % (3345676)Termination phase: Saturation % 10.11/1.67 % (3345676)Time elapsed: 0.054 s % 10.11/1.67 % (3345676)Peak memory usage: 13 MB % 10.11/1.67 % (3345676)Instructions burned: 162 (million) % 10.11/1.67 % (3345686)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=993166333:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 10.11/1.67 % (3345689)ott-21_1_sil=16000:fs=off:random_seed=2820370483:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 10.11/1.67 % (3345685)Instruction limit reached! % 10.11/1.67 % (3345685)------------------------------ % 10.11/1.67 % (3345685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.11/1.67 % (3345685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/1.67 % (3345685)CaDiCaL version: 2.1.3 % 25.18/3.91 % (3345685)Termination reason: Instruction limit % 25.18/3.91 % (3345685)Termination phase: Saturation % 25.18/3.91 % (3345685)Time elapsed: 0.043 s % 25.18/3.91 % (3345685)Peak memory usage: 13 MB % 25.18/3.91 % (3345685)Instructions burned: 132 (million) % 25.18/3.91 % (3345689)Instruction limit reached! % 25.18/3.91 % (3345689)------------------------------ % 25.18/3.91 % (3345689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.18/3.91 % (3345689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.18/3.91 % (3345689)CaDiCaL version: 2.1.3 % 25.18/3.91 % (3345689)Termination reason: Instruction limit % 25.18/3.91 % (3345689)Termination phase: Saturation % 25.18/3.91 % (3345689)Time elapsed: 0.037 s % 25.18/3.91 % (3345689)Peak memory usage: 12 MB % 25.18/3.91 % (3345689)Instructions burned: 183 (million) % 25.18/3.91 % (3345692)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4041484050:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 25.18/3.91 % (3345693)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=893095456:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 25.18/3.91 % TRYING [1] % 25.18/3.91 % TRYING [2] % 25.18/3.91 % TRYING [1] % 25.18/3.91 % TRYING [2] % 25.18/3.91 % TRYING [3] % 25.18/3.91 % TRYING [3] % 25.18/3.91 % (3345684)Instruction limit reached! % 25.18/3.91 % (3345684)------------------------------ % 25.18/3.91 % (3345684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.18/3.91 % (3345684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.18/3.91 % (3345684)CaDiCaL version: 2.1.3 % 25.18/3.91 % (3345684)Termination reason: Instruction limit % 25.18/3.91 % (3345684)Termination phase: Finite model building constraint generation % 25.18/3.91 % (3345684)Time elapsed: 0.177 s % 25.18/3.91 % (3345684)Peak memory usage: 32 MB % 25.18/3.91 % (3345684)Instructions burned: 716 (million) % 25.18/3.91 % TRYING [1] % 25.18/3.91 % (3345696)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1486350088:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 25.18/3.91 % (3345692)Instruction limit reached! % 25.18/3.91 % (3345692)------------------------------ % 25.18/3.91 % (3345692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.18/3.91 % (3345692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.18/3.91 % (3345692)CaDiCaL version: 2.1.3 % 25.18/3.91 % (3345692)Termination reason: Instruction limit % 25.18/3.91 % (3345692)Termination phase: Saturation % 25.18/3.91 % (3345692)Time elapsed: 0.142 s % 25.18/3.91 % (3345692)Peak memory usage: 15 MB % 25.18/3.91 % (3345692)Instructions burned: 478 (million) % 25.18/3.91 % TRYING [2] % 25.18/3.91 % (3345698)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=871339480:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 25.18/3.91 % (3345686)Instruction limit reached! % 25.18/3.91 % (3345686)------------------------------ % 25.18/3.91 % (3345686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.18/3.91 % (3345686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.18/3.91 % (3345686)CaDiCaL version: 2.1.3 % 25.18/3.91 % (3345686)Termination reason: Instruction limit % 25.18/3.91 % (3345686)Termination phase: Saturation % 25.18/3.91 % (3345686)Time elapsed: 0.214 s % 25.18/3.91 % (3345686)Peak memory usage: 17 MB % 25.18/3.91 % (3345686)Instructions burned: 685 (million) % 25.18/3.91 % (3345700)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=290195123:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 25.18/3.91 % (3345693)Instruction limit reached! % 25.18/3.91 % (3345693)------------------------------ % 25.18/3.91 % (3345693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.18/3.91 % (3345693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.18/3.91 % (3345693)CaDiCaL version: 2.1.3 % 25.18/3.91 % (3345693)Termination reason: Instruction limit % 25.18/3.91 % (3345693)Termination phase: Finite model building SAT solving % 25.18/3.91 % (3345693)Time elapsed: 0.238 s % 25.18/3.91 % (3345693)Peak memory usage: 33 MB % 25.18/3.91 % (3345693)Instructions burned: 869 (million) % 25.18/3.91 % (3345702)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2294328628:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 25.18/3.91 % TRYING [4] % 25.18/3.91 % (3345698)Instruction limit reached! % 25.18/3.91 % (3345698)------------------------------ % 25.18/3.91 % (3345698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.69/8.26 % (3345698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.69/8.26 % (3345698)CaDiCaL version: 2.1.3 % 56.69/8.26 % (3345698)Termination reason: Instruction limit % 56.69/8.26 % (3345698)Termination phase: Finite model building constraint generation % 56.69/8.26 % (3345698)Time elapsed: 0.238 s % 56.69/8.26 % (3345698)Peak memory usage: 73 MB % 56.69/8.26 % (3345698)Instructions burned: 889 (million) % 56.69/8.26 % (3345704)fmb+10_1_sil=64000:random_seed=2609314025:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 56.69/8.26 % (3345700)Instruction limit reached! % 56.69/8.26 % (3345700)------------------------------ % 56.69/8.26 % (3345700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.69/8.26 % (3345700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.69/8.26 % (3345700)CaDiCaL version: 2.1.3 % 56.69/8.26 % (3345700)Termination reason: Instruction limit % 56.69/8.26 % (3345700)Termination phase: Saturation % 56.69/8.26 % (3345700)Time elapsed: 0.234 s % 56.69/8.26 % (3345700)Peak memory usage: 19 MB % 56.69/8.26 % (3345700)Instructions burned: 692 (million) % 56.69/8.26 % (3345706)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1642488923:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 56.69/8.26 % TRYING [1] % 56.69/8.26 % (3345696)Instruction limit reached! % 56.69/8.26 % (3345696)------------------------------ % 56.69/8.26 % (3345696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.69/8.26 % (3345696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.69/8.26 % (3345696)CaDiCaL version: 2.1.3 % 56.69/8.26 % (3345696)Termination reason: Instruction limit % 56.69/8.26 % (3345696)Termination phase: Saturation % 56.69/8.26 % (3345696)Time elapsed: 0.394 s % 56.69/8.26 % (3345696)Peak memory usage: 23 MB % 56.69/8.26 % (3345696)Instructions burned: 1180 (million) % 56.69/8.26 % (3345702)Instruction limit reached! % 56.69/8.26 % (3345702)------------------------------ % 56.69/8.26 % (3345702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.69/8.26 % (3345702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.69/8.26 % (3345702)CaDiCaL version: 2.1.3 % 56.69/8.26 % (3345702)Termination reason: Instruction limit % 56.69/8.26 % (3345702)Termination phase: Saturation % 56.69/8.26 % (3345702)Time elapsed: 0.272 s % 56.69/8.26 % (3345702)Peak memory usage: 20 MB % 56.69/8.26 % (3345702)Instructions burned: 880 (million) % 56.69/8.26 % TRYING [2] % 56.69/8.26 % TRYING [20] % 56.69/8.26 % (3345708)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3812781423:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 56.69/8.26 % (3345709)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4044216067:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 56.69/8.26 % TRYING [8] % 56.69/8.26 % TRYING [3] % 56.69/8.26 % (3345708)Instruction limit reached! % 56.69/8.26 % (3345708)------------------------------ % 56.69/8.26 % (3345708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.69/8.26 % (3345708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.69/8.26 % (3345708)CaDiCaL version: 2.1.3 % 56.69/8.26 % (3345708)Termination reason: Instruction limit % 56.69/8.26 % (3345708)Termination phase: Finite model building constraint generation % 56.69/8.26 % (3345708)Time elapsed: 0.210 s % 56.69/8.26 % (3345708)Peak memory usage: 53 MB % 56.69/8.26 % (3345708)Instructions burned: 921 (million) % 56.69/8.26 % (3345712)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2759901532:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 56.69/8.26 % (3345712)Instruction limit reached! % 56.69/8.26 % (3345712)------------------------------ % 56.69/8.26 % (3345712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 56.69/8.26 % (3345712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.69/8.26 % (3345712)CaDiCaL version: 2.1.3 % 56.69/8.26 % (3345712)Termination reason: Instruction limit % 56.69/8.26 % (3345712)Termination phase: Saturation % 56.69/8.26 % (3345712)Time elapsed: 0.499 s % 56.69/8.26 % (3345712)Peak memory usage: 37 MB % 56.69/8.26 % (3345712)Instructions burned: 1473 (million) % 56.69/8.26 % (3345714)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1938477015:i=6324_2985 on theBenchmark for (2985ds/6324Mi) % 56.69/8.26 % (3345714)Cannot represent all propositional literals internally % 56.69/8.26 % (3345714)Refutation not found, incomplete strategy % 56.69/8.26 % (3345714)------------------------------ % 141.31/20.27 % (3345714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.31/20.27 % (3345714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.31/20.27 % (3345714)CaDiCaL version: 2.1.3 % 141.31/20.27 % (3345714)Termination reason: Refutation not found, incomplete strategy % 141.31/20.27 % (3345714)Time elapsed: 0.117 s % 141.31/20.27 % (3345714)Peak memory usage: 18 MB % 141.31/20.27 % (3345714)Instructions burned: 436 (million) % 141.31/20.27 % (3345714)------------------------------ % 141.31/20.27 % (3345714)------------------------------ % 141.31/20.27 % (3345716)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3828894909:fmbsr=2.30978:i=2174_2984 on theBenchmark for (2984ds/2174Mi) % 141.31/20.27 % TRYING [4] % 141.31/20.27 % (3345716)Cannot represent all propositional literals internally % 141.31/20.27 % (3345716)Refutation not found, incomplete strategy % 141.31/20.27 % (3345716)------------------------------ % 141.31/20.27 % (3345716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.31/20.27 % (3345716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.31/20.27 % (3345716)CaDiCaL version: 2.1.3 % 141.31/20.27 % (3345716)Termination reason: Refutation not found, incomplete strategy % 141.31/20.27 % (3345716)Time elapsed: 0.433 s % 141.31/20.27 % (3345716)Peak memory usage: 29 MB % 141.31/20.27 % (3345716)Instructions burned: 1645 (million) % 141.31/20.27 % (3345716)------------------------------ % 141.31/20.27 % (3345716)------------------------------ % 141.31/20.27 % (3345718)ott-2_1_sil=16000:newcnf=on:random_seed=3972101739:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2980 on theBenchmark for (2980ds/869Mi) % 141.31/20.27 % (3345718)Instruction limit reached! % 141.31/20.27 % (3345718)------------------------------ % 141.31/20.27 % (3345718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.31/20.27 % (3345718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.31/20.27 % (3345718)CaDiCaL version: 2.1.3 % 141.31/20.27 % (3345718)Termination reason: Instruction limit % 141.31/20.27 % (3345718)Termination phase: Saturation % 141.31/20.27 % (3345718)Time elapsed: 0.261 s % 141.31/20.27 % (3345718)Peak memory usage: 19 MB % 141.31/20.27 % (3345718)Instructions burned: 870 (million) % 141.31/20.27 % (3345721)ott+10_1_sil=32000:tgt=ground:random_seed=2574738219:i=5114:av=off_2977 on theBenchmark for (2977ds/5114Mi) % 141.31/20.27 % (3345709)Instruction limit reached! % 141.31/20.27 % (3345709)------------------------------ % 141.31/20.27 % (3345709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.31/20.27 % (3345709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.31/20.27 % (3345709)CaDiCaL version: 2.1.3 % 141.31/20.27 % (3345709)Termination reason: Instruction limit % 141.31/20.27 % (3345709)Termination phase: Saturation % 141.31/20.27 % (3345709)Time elapsed: 1.651 s % 141.31/20.27 % (3345709)Peak memory usage: 45 MB % 141.31/20.27 % (3345709)Instructions burned: 5133 (million) % 141.31/20.27 % (3345723)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=373498062:i=54282_2976 on theBenchmark for (2976ds/54282Mi) % 141.31/20.27 % TRYING [1] % 141.31/20.27 % TRYING [2] % 141.31/20.27 % TRYING [5] % 141.31/20.27 % TRYING [3] % 141.31/20.27 % (3345706)Instruction limit reached! % 141.31/20.27 % (3345706)------------------------------ % 141.31/20.27 % (3345706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.31/20.27 % (3345706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.31/20.27 % (3345706)CaDiCaL version: 2.1.3 % 141.31/20.27 % (3345706)Termination reason: Instruction limit % 141.31/20.27 % (3345706)Termination phase: Finite model building constraint generation % 141.31/20.27 % (3345706)Time elapsed: 1.964 s % 141.31/20.27 % (3345706)Peak memory usage: 648 MB % 141.31/20.27 % (3345706)Instructions burned: 9520 (million) % 141.31/20.27 % (3345725)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1770649077:i=3512:aac=none_2974 on theBenchmark for (2974ds/3512Mi) % 141.31/20.27 % TRYING [4] % 141.31/20.27 % (3345725)Instruction limit reached! % 141.31/20.27 % (3345725)------------------------------ % 141.31/20.27 % (3345725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.31/20.27 % (3345725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.31/20.27 % (3345725)CaDiCaL version: 2.1.3 % 141.31/20.27 % (3345725)Termination reason: Instruction limit % 141.31/20.27 % (3345725)Termination phase: Saturation % 141.31/20.27 % (3345725)Time elapsed: 1.173 s % 141.31/20.27 % (3345725)Peak memory usage: 41 MB % 141.31/20.27 % (3345725)Instructions burned: 3515 (million) % 141.31/20.27 % (3345727)dis+21_1_sil=32000:sas=cadical:random_seed=1103837145:i=3773:amm=off_2962 on theBenchmark for (2962ds/3773Mi) % 189.56/28.03 % (3345721)Instruction limit reached! % 189.56/28.03 % (3345721)------------------------------ % 189.56/28.03 % (3345721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.56/28.03 % (3345721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.56/28.03 % (3345721)CaDiCaL version: 2.1.3 % 189.56/28.03 % (3345721)Termination reason: Instruction limit % 189.56/28.03 % (3345721)Termination phase: Saturation % 189.56/28.03 % (3345721)Time elapsed: 1.801 s % 189.56/28.03 % (3345721)Peak memory usage: 52 MB % 189.56/28.03 % (3345721)Instructions burned: 5117 (million) % 189.56/28.03 % (3345729)ott+11_1_sil=16000:gs=on:random_seed=3860331560:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2959 on theBenchmark for (2959ds/2251Mi) % 189.56/28.03 % TRYING [5] % 189.56/28.03 % (3345729)Instruction limit reached! % 189.56/28.03 % (3345729)------------------------------ % 189.56/28.03 % (3345729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.56/28.03 % (3345729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.56/28.03 % (3345729)CaDiCaL version: 2.1.3 % 189.56/28.03 % (3345729)Termination reason: Instruction limit % 189.56/28.03 % (3345729)Termination phase: Saturation % 189.56/28.03 % (3345729)Time elapsed: 0.741 s % 189.56/28.03 % (3345729)Peak memory usage: 28 MB % 189.56/28.03 % (3345729)Instructions burned: 2255 (million) % 189.56/28.03 % (3345731)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1535279233:fmbsr=1.6:i=67534_2951 on theBenchmark for (2951ds/67534Mi) % 189.56/28.03 % (3345727)Instruction limit reached! % 189.56/28.03 % (3345727)------------------------------ % 189.56/28.03 % (3345727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.56/28.03 % (3345727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.56/28.03 % (3345727)CaDiCaL version: 2.1.3 % 189.56/28.03 % (3345727)Termination reason: Instruction limit % 189.56/28.03 % (3345727)Termination phase: Saturation % 189.56/28.03 % (3345727)Time elapsed: 1.245 s % 189.56/28.03 % (3345727)Peak memory usage: 41 MB % 189.56/28.03 % (3345727)Instructions burned: 3775 (million) % 189.56/28.03 % (3345733)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1930787969:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2949 on theBenchmark for (2949ds/4591Mi) % 189.56/28.03 % (3345704)Instruction limit reached! % 189.56/28.03 % (3345704)------------------------------ % 189.56/28.03 % (3345704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.56/28.03 % (3345704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.56/28.03 % (3345704)CaDiCaL version: 2.1.3 % 189.56/28.03 % (3345704)Termination reason: Instruction limit % 189.56/28.03 % (3345704)Termination phase: Finite model building SAT solving % 189.56/28.03 % (3345704)Time elapsed: 5.132 s % 189.56/28.03 % (3345704)Peak memory usage: 292 MB % 189.56/28.03 % (3345704)Instructions burned: 22062 (million) % 189.56/28.03 % TRYING [7] % 189.56/28.03 % (3345735)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2687191535:i=29340_2942 on theBenchmark for (2942ds/29340Mi) % 189.56/28.03 % (3345733)Instruction limit reached! % 189.56/28.03 % (3345733)------------------------------ % 189.56/28.03 % (3345733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.56/28.03 % (3345733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.56/28.03 % (3345733)CaDiCaL version: 2.1.3 % 189.56/28.03 % (3345733)Termination reason: Instruction limit % 189.56/28.03 % (3345733)Termination phase: Saturation % 189.56/28.03 % (3345733)Time elapsed: 1.514 s % 189.56/28.03 % (3345733)Peak memory usage: 72 MB % 189.56/28.03 % (3345733)Instructions burned: 4593 (million) % 189.56/28.03 % (3345737)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1455891808:i=5211_2934 on theBenchmark for (2934ds/5211Mi) % 189.56/28.03 % (3345737)Instruction limit reached! % 189.56/28.03 % (3345737)------------------------------ % 189.56/28.03 % (3345737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.56/28.03 % (3345737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.56/28.03 % (3345737)CaDiCaL version: 2.1.3 % 189.56/28.03 % (3345737)Termination reason: Instruction limit % 189.56/28.03 % (3345737)Termination phase: Saturation % 189.56/28.03 % (3345737)Time elapsed: 1.543 s % 189.56/28.03 % (3345737)Peak memory usage: 53 MB % 189.56/28.03 % (3345737)Instructions burned: 5213 (million) % 189.56/28.03 % (3345739)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=439859453:i=5497:nm=2_2918 on theBenchmark for (2918ds/5497Mi) % 261.14/37.24 % TRYING [17] % 261.14/37.24 % (3345739)Instruction limit reached! % 261.14/37.24 % (3345739)------------------------------ % 261.14/37.24 % (3345739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.14/37.24 % (3345739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.14/37.24 % (3345739)CaDiCaL version: 2.1.3 % 261.14/37.24 % (3345739)Termination reason: Instruction limit % 261.14/37.24 % (3345739)Termination phase: Finite model building constraint generation % 261.14/37.24 % (3345739)Time elapsed: 1.107 s % 261.14/37.24 % (3345739)Peak memory usage: 370 MB % 261.14/37.24 % (3345739)Instructions burned: 5501 (million) % 261.14/37.24 % (3345741)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3279431374:fmbsr=2:i=46332_2907 on theBenchmark for (2907ds/46332Mi) % 261.14/37.24 % TRYING [15] % 261.14/37.24 % TRYING [6] % 261.14/37.24 % (3345735)Instruction limit reached! % 261.14/37.24 % (3345735)------------------------------ % 261.14/37.24 % (3345735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.14/37.24 % (3345735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.14/37.24 % (3345735)CaDiCaL version: 2.1.3 % 261.14/37.24 % (3345735)Termination reason: Instruction limit % 261.14/37.24 % (3345735)Termination phase: Saturation % 261.14/37.24 % (3345735)Time elapsed: 8.601 s % 261.14/37.24 % (3345735)Peak memory usage: 221 MB % 261.14/37.24 % (3345735)Instructions burned: 29341 (million) % 261.14/37.24 % (3345743)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1307117628:i=14071_2856 on theBenchmark for (2856ds/14071Mi) % 261.14/37.24 % TRYING [6] % 261.14/37.24 % TRYING [12] % 261.14/37.24 % (3345743)Instruction limit reached! % 261.14/37.24 % (3345743)------------------------------ % 261.14/37.24 % (3345743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.14/37.24 % (3345743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.14/37.24 % (3345743)CaDiCaL version: 2.1.3 % 261.14/37.24 % (3345743)Termination reason: Instruction limit % 261.14/37.24 % (3345743)Termination phase: Finite model building constraint generation % 261.14/37.24 % (3345743)Time elapsed: 2.846 s % 261.14/37.24 % (3345743)Peak memory usage: 1030 MB % 261.14/37.24 % (3345743)Instructions burned: 14074 (million) % 261.14/37.24 % (3345745)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2355894957:i=22565:add=on:rawr=on_2827 on theBenchmark for (2827ds/22565Mi) % 261.14/37.24 % (3345723)Instruction limit reached! % 261.14/37.24 % (3345723)------------------------------ % 261.14/37.24 % (3345723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.14/37.24 % (3345723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.14/37.24 % (3345723)CaDiCaL version: 2.1.3 % 261.14/37.24 % (3345723)Termination reason: Instruction limit % 261.14/37.24 % (3345723)Termination phase: Finite model building constraint generation % 261.14/37.24 % (3345723)Time elapsed: 15.605 s % 261.14/37.24 % (3345723)Peak memory usage: 1532 MB % 261.14/37.24 % (3345723)Instructions burned: 54285 (million) % 261.14/37.24 % (3345741)Instruction limit reached! % 261.14/37.24 % (3345741)------------------------------ % 261.14/37.24 % (3345741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.14/37.24 % (3345741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.14/37.24 % (3345741)CaDiCaL version: 2.1.3 % 261.14/37.24 % (3345741)Termination reason: Instruction limit % 261.14/37.24 % (3345741)Termination phase: Finite model building constraint generation % 261.14/37.24 % (3345741)Time elapsed: 8.708 s % 261.14/37.24 % (3345741)Peak memory usage: 2583 MB % 261.14/37.24 % (3345741)Instructions burned: 46337 (million) % 261.14/37.24 % (3345747)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=225097671:i=8173:av=off_2818 on theBenchmark for (2818ds/8173Mi) % 261.14/37.24 % (3345749)dis+10_16:1_sil=16000:random_seed=2525061524:i=9155:fsr=off_2817 on theBenchmark for (2817ds/9155Mi) % 261.14/37.24 % (3345731)Instruction limit reached! % 261.14/37.24 % (3345731)------------------------------ % 261.14/37.24 % (3345731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.14/37.24 % (3345731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.14/37.24 % (3345731)CaDiCaL version: 2.1.3 % 261.14/37.24 % (3345731)Termination reason: Instruction limit % 261.14/37.24 % (3345731)Termination phase: Finite model building constraint generation % 261.14/37.24 % (3345731)Time elapsed: 15.290 s % 261.14/37.24 % (3345731)Peak memory usage: 3776 MB % 261.14/37.24 % (3345731)Instructions burned: 67537 (million) % 300.63/42.83 % (3345751)ott-3_8_sil=64000:random_seed=2674931628:i=20139:bs=on_2795 on theBenchmark for (2795ds/20139Mi) % 300.63/42.83 % (3345747)Instruction limit reached! % 300.63/42.83 % (3345747)------------------------------ % 300.63/42.83 % (3345747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (3345747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (3345747)CaDiCaL version: 2.1.3 % 300.63/42.83 % (3345747)Termination reason: Instruction limit % 300.63/42.83 % (3345747)Termination phase: Saturation % 300.63/42.83 % (3345747)Time elapsed: 2.944 s % 300.63/42.83 % (3345747)Peak memory usage: 90 MB % 300.63/42.83 % (3345747)Instructions burned: 8173 (million) % 300.63/42.83 % (3345753)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3118351130:fmbsr=2:i=32576_2789 on theBenchmark for (2789ds/32576Mi) % 300.63/42.83 % (3345749)Instruction limit reached! % 300.63/42.83 % (3345749)------------------------------ % 300.63/42.83 % (3345749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (3345749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (3345749)CaDiCaL version: 2.1.3 % 300.63/42.83 % (3345749)Termination reason: Instruction limit % 300.63/42.83 % (3345749)Termination phase: Saturation % 300.63/42.83 % (3345749)Time elapsed: 2.845 s % 300.63/42.83 % (3345749)Peak memory usage: 70 MB % 300.63/42.83 % (3345749)Instructions burned: 9156 (million) % 300.63/42.83 % (3345755)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2535893540:i=11404_2789 on theBenchmark for (2789ds/11404Mi) % 300.63/42.83 % TRYING [9] % 300.63/42.83 % (3345745)Instruction limit reached! % 300.63/42.83 % (3345745)------------------------------ % 300.63/42.83 % (3345745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (3345745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (3345745)CaDiCaL version: 2.1.3 % 300.63/42.83 % (3345745)Termination reason: Instruction limit % 300.63/42.83 % (3345745)Termination phase: Saturation % 300.63/42.83 % (3345745)Time elapsed: 5.400 s % 300.63/42.83 % (3345745)Peak memory usage: 59 MB % 300.63/42.83 % (3345745)Instructions burned: 22568 (million) % 300.63/42.83 % (3345757)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2992370140:i=14134_2773 on theBenchmark for (2773ds/14134Mi) % 300.63/42.83 % (3345755)Instruction limit reached! % 300.63/42.83 % (3345755)------------------------------ % 300.63/42.83 % (3345755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (3345755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (3345755)CaDiCaL version: 2.1.3 % 300.63/42.83 % (3345755)Termination reason: Instruction limit % 300.63/42.83 % (3345755)Termination phase: Saturation % 300.63/42.83 % (3345755)Time elapsed: 4.152 s % 300.63/42.83 % (3345755)Peak memory usage: 98 MB % 300.63/42.83 % (3345755)Instructions burned: 11406 (million) % 300.63/42.83 % (3345759)dis+33_16_sil=32000:sac=on:random_seed=345469488:i=15851:nm=0_2747 on theBenchmark for (2747ds/15851Mi) % 300.63/42.83 % (3345753)Instruction limit reached! % 300.63/42.83 % (3345753)------------------------------ % 300.63/42.83 % (3345753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (3345753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (3345753)CaDiCaL version: 2.1.3 % 300.63/42.83 % (3345753)Termination reason: Instruction limit % 300.63/42.83 % (3345753)Termination phase: Finite model building constraint generation % 300.63/42.83 % (3345753)Time elapsed: 6.621 s % 300.63/42.83 % (3345753)Peak memory usage: 2054 MB % 300.63/42.83 % (3345753)Instructions burned: 32581 (million) % 300.63/42.83 % (3345757)Instruction limit reached! % 300.63/42.83 % (3345757)------------------------------ % 300.63/42.83 % (3345757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (3345757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (3345757)CaDiCaL version: 2.1.3 % 300.63/42.83 % (3345757)Termination reason: Instruction limit % 300.63/42.83 % (3345757)Termination phase: Saturation % 300.63/42.83 % (3345757)Time elapsed: 5.054 s % 300.63/42.83 % (3345757)Peak memory usage: 106 MB % 300.63/42.83 % (3345757)Instructions burned: 14135 (million) % 300.63/42.83 % (3345761)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4042621012:avsq=on:i=17627:add=on:amm=off_2722 on theBenchmark for (2722ds/17627Mi) % 300.63/42.83 % (3345763)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3727431221:s2a= % 300.63/42.83 Terminated % 300.63/42.83 % Vampire exiting %------------------------------------------------------------------------------