%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW746_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:42 PM UTC 2026 % Result : Timeout 292.41s 41.56s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW746_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.22 % Computer : n018.cluster.edu % 0.10/0.22 % Model : x86_64 x86_64 % 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.22 % Memory : 8046.5625MB % 0.10/0.22 % OS : Linux 6.8.0-71-generic % 0.10/0.22 % CPULimit : 300 % 0.10/0.22 % WCLimit : 300 % 0.10/0.22 % DateTime : Mon Sep 28 14:31:25 UTC 2026 % 0.10/0.22 % CPUTime : % 0.10/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.26 Running first-order model finding % 0.10/0.26 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 % 2.73/0.78 % (3431305)Will run a generic schedule for satisfiability detection. % 2.73/0.78 % (3431315)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2458891954:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.73/0.78 % (3431311)% WARNING: option uhcvi not known. % 2.73/0.78 % (3431310)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2122773982_2999 on theBenchmark for (2999ds/0Mi) % 2.73/0.78 % (3431314)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2053446301:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.73/0.78 % (3431312)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=108389616:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.73/0.78 % (3431313)dis+10_1_sil=32000:sp=arity:random_seed=1783652737:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.73/0.78 % (3431311)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3453248921:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.73/0.78 % (3431316)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3034000735:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.73/0.78 % (3431315)Instruction limit reached! % 2.73/0.78 % (3431315)------------------------------ % 2.73/0.78 % (3431315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.73/0.78 % (3431315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.73/0.78 % (3431315)CaDiCaL version: 2.1.3 % 2.73/0.78 % (3431315)Termination reason: Instruction limit % 2.73/0.78 % (3431315)Termination phase: Saturation % 2.73/0.78 % (3431315)Time elapsed: 0.037 s % 2.73/0.78 % (3431315)Peak memory usage: 16 MB % 2.73/0.78 % (3431315)Instructions burned: 133 (million) % 2.73/0.78 % (3431324)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2449836275:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.73/0.78 % (3431313)Instruction limit reached! % 2.73/0.78 % (3431313)------------------------------ % 2.73/0.78 % (3431313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.73/0.78 % (3431313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.73/0.78 % (3431313)CaDiCaL version: 2.1.3 % 2.73/0.78 % (3431313)Termination reason: Instruction limit % 2.73/0.78 % (3431313)Termination phase: Saturation % 2.73/0.78 % (3431313)Time elapsed: 0.047 s % 2.73/0.78 % (3431313)Peak memory usage: 14 MB % 2.73/0.78 % (3431313)Instructions burned: 104 (million) % 2.73/0.78 % (3431314)Instruction limit reached! % 2.73/0.78 % (3431314)------------------------------ % 2.73/0.78 % (3431314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.73/0.78 % (3431314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.73/0.78 % (3431314)CaDiCaL version: 2.1.3 % 2.73/0.78 % (3431314)Termination reason: Instruction limit % 2.73/0.78 % (3431314)Termination phase: Blocked clause elimination % 2.73/0.78 % (3431314)Time elapsed: 0.051 s % 2.73/0.78 % (3431314)Peak memory usage: 13 MB % 2.73/0.78 % (3431314)Instructions burned: 116 (million) % 2.73/0.78 % (3431324)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.73/0.78 % (3431324)Terminated due to inappropriate strategy. % 2.73/0.78 % (3431324)------------------------------ % 2.73/0.78 % (3431324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.73/0.78 % (3431324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.73/0.78 % (3431324)CaDiCaL version: 2.1.3 % 2.73/0.78 % (3431324)Termination reason: Inappropriate % 2.73/0.78 % (3431324)Time elapsed: 0.018 s % 2.73/0.78 % (3431324)Peak memory usage: 13 MB % 2.73/0.78 % (3431324)Instructions burned: 74 (million) % 2.73/0.78 % (3431324)------------------------------ % 2.73/0.78 % (3431324)------------------------------ % 2.73/0.78 % (3431326)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=260661611:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 2.73/0.78 % (3431327)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=3559464171:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 2.73/0.78 % (3431328)ott-21_1_sil=16000:fs=off:random_seed=1897642686:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 2.73/0.78 % (3431316)Instruction limit reached! % 2.73/0.78 % (3431316)------------------------------ % 2.73/0.78 % (3431316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.44/1.25 % (3431316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.44/1.25 % (3431316)CaDiCaL version: 2.1.3 % 6.44/1.25 % (3431316)Termination reason: Instruction limit % 6.44/1.25 % (3431316)Termination phase: Saturation % 6.44/1.25 % (3431316)Time elapsed: 0.079 s % 6.44/1.25 % (3431316)Peak memory usage: 17 MB % 6.44/1.25 % (3431316)Instructions burned: 159 (million) % 6.44/1.25 % (3431332)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1102460798:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.44/1.25 % (3431328)Instruction limit reached! % 6.44/1.25 % (3431328)------------------------------ % 6.44/1.25 % (3431328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.44/1.25 % (3431328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.44/1.25 % (3431328)CaDiCaL version: 2.1.3 % 6.44/1.25 % (3431328)Termination reason: Instruction limit % 6.44/1.25 % (3431328)Termination phase: Saturation % 6.44/1.25 % (3431328)Time elapsed: 0.046 s % 6.44/1.25 % (3431328)Peak memory usage: 14 MB % 6.44/1.25 % (3431328)Instructions burned: 181 (million) % 6.44/1.25 % (3431326)Instruction limit reached! % 6.44/1.25 % (3431326)------------------------------ % 6.44/1.25 % (3431326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.44/1.25 % (3431326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.44/1.25 % (3431326)CaDiCaL version: 2.1.3 % 6.44/1.25 % (3431326)Termination reason: Instruction limit % 6.44/1.25 % (3431326)Termination phase: Blocked clause elimination % 6.44/1.25 % (3431326)Time elapsed: 0.060 s % 6.44/1.25 % (3431326)Peak memory usage: 13 MB % 6.44/1.25 % (3431326)Instructions burned: 132 (million) % 6.44/1.25 % (3431334)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3389967735:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.44/1.25 % (3431310)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.44/1.25 % (3431310)Terminated due to inappropriate strategy. % 6.44/1.25 % (3431310)------------------------------ % 6.44/1.25 % (3431310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.44/1.25 % (3431310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.44/1.25 % (3431310)CaDiCaL version: 2.1.3 % 6.44/1.25 % (3431310)Termination reason: Inappropriate % 6.44/1.25 % (3431310)Time elapsed: 0.147 s % 6.44/1.25 % (3431310)Peak memory usage: 14 MB % 6.44/1.25 % (3431310)Instructions burned: 294 (million) % 6.44/1.25 % (3431310)------------------------------ % 6.44/1.25 % (3431310)------------------------------ % 6.44/1.25 % (3431336)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=387535033:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.44/1.25 % (3431334)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.44/1.25 % (3431334)Terminated due to inappropriate strategy. % 6.44/1.25 % (3431334)------------------------------ % 6.44/1.25 % (3431334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.44/1.25 % (3431334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.44/1.25 % (3431334)CaDiCaL version: 2.1.3 % 6.44/1.25 % (3431334)Termination reason: Inappropriate % 6.44/1.25 % (3431334)Time elapsed: 0.023 s % 6.44/1.25 % (3431334)Peak memory usage: 14 MB % 6.44/1.25 % (3431334)Instructions burned: 92 (million) % 6.44/1.25 % (3431334)------------------------------ % 6.44/1.25 % (3431334)------------------------------ % 6.44/1.25 % (3431339)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=3462984654:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 6.44/1.25 % (3431337)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1930209896:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 6.44/1.25 % (3431337)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.44/1.25 % (3431337)Terminated due to inappropriate strategy. % 6.44/1.25 % (3431337)------------------------------ % 6.44/1.25 % (3431337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.44/1.25 % (3431337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.44/1.25 % (3431337)CaDiCaL version: 2.1.3 % 6.44/1.25 % (3431337)Termination reason: Inappropriate % 6.44/1.25 % (3431337)Time elapsed: 0.036 s % 19.51/3.11 % (3431337)Peak memory usage: 12 MB % 19.51/3.11 % (3431337)Instructions burned: 82 (million) % 19.51/3.11 % (3431337)------------------------------ % 19.51/3.11 % (3431337)------------------------------ % 19.51/3.11 % (3431342)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2123046719:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 19.51/3.11 % (3431332)Instruction limit reached! % 19.51/3.11 % (3431332)------------------------------ % 19.51/3.11 % (3431332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.51/3.11 % (3431332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.51/3.11 % (3431332)CaDiCaL version: 2.1.3 % 19.51/3.11 % (3431332)Termination reason: Instruction limit % 19.51/3.11 % (3431332)Termination phase: Saturation % 19.51/3.11 % (3431332)Time elapsed: 0.244 s % 19.51/3.11 % (3431332)Peak memory usage: 17 MB % 19.51/3.11 % (3431332)Instructions burned: 478 (million) % 19.51/3.11 % (3431344)fmb+10_1_sil=64000:random_seed=2075880792:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 19.51/3.11 % (3431339)Instruction limit reached! % 19.51/3.11 % (3431339)------------------------------ % 19.51/3.11 % (3431339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.51/3.11 % (3431339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.51/3.11 % (3431339)CaDiCaL version: 2.1.3 % 19.51/3.11 % (3431339)Termination reason: Instruction limit % 19.51/3.11 % (3431339)Termination phase: Saturation % 19.51/3.11 % (3431339)Time elapsed: 0.228 s % 19.51/3.11 % (3431339)Peak memory usage: 23 MB % 19.51/3.11 % (3431339)Instructions burned: 695 (million) % 19.51/3.11 % (3431344)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.51/3.11 % (3431344)Terminated due to inappropriate strategy. % 19.51/3.11 % (3431344)------------------------------ % 19.51/3.11 % (3431344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.51/3.11 % (3431344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.51/3.11 % (3431344)CaDiCaL version: 2.1.3 % 19.51/3.11 % (3431344)Termination reason: Inappropriate % 19.51/3.11 % (3431344)Time elapsed: 0.034 s % 19.51/3.11 % (3431344)Peak memory usage: 12 MB % 19.51/3.11 % (3431344)Instructions burned: 80 (million) % 19.51/3.11 % (3431344)------------------------------ % 19.51/3.11 % (3431344)------------------------------ % 19.51/3.11 % (3431327)Instruction limit reached! % 19.51/3.11 % (3431327)------------------------------ % 19.51/3.11 % (3431327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.51/3.11 % (3431327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.51/3.11 % (3431327)CaDiCaL version: 2.1.3 % 19.51/3.11 % (3431327)Termination reason: Instruction limit % 19.51/3.11 % (3431327)Termination phase: Saturation % 19.51/3.11 % (3431327)Time elapsed: 0.336 s % 19.51/3.11 % (3431327)Peak memory usage: 26 MB % 19.51/3.11 % (3431327)Instructions burned: 684 (million) % 19.51/3.11 % (3431357)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4052964453:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 19.51/3.11 % (3431359)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3541325776:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 19.51/3.11 % (3431357)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.51/3.11 % (3431357)Terminated due to inappropriate strategy. % 19.51/3.11 % (3431357)------------------------------ % 19.51/3.11 % (3431357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.51/3.11 % (3431357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.51/3.11 % (3431357)CaDiCaL version: 2.1.3 % 19.51/3.11 % (3431357)Termination reason: Inappropriate % 19.51/3.11 % (3431357)Time elapsed: 0.017 s % 19.51/3.11 % (3431357)Peak memory usage: 12 MB % 19.51/3.11 % (3431357)Instructions burned: 76 (million) % 19.51/3.11 % (3431357)------------------------------ % 19.51/3.11 % (3431357)------------------------------ % 19.51/3.11 % (3431363)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4292453792:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 19.51/3.11 % (3431373)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2934537198:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 19.51/3.11 % (3431359)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.51/3.11 % (3431359)Terminated due to inappropriate strategy. % 19.51/3.11 % (3431359)------------------------------ % 24.57/4.04 % (3431359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.57/4.04 % (3431359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.57/4.04 % (3431359)CaDiCaL version: 2.1.3 % 24.57/4.04 % (3431359)Termination reason: Inappropriate % 24.57/4.04 % (3431359)Time elapsed: 0.034 s % 24.57/4.04 % (3431359)Peak memory usage: 12 MB % 24.57/4.04 % (3431359)Instructions burned: 81 (million) % 24.57/4.04 % (3431359)------------------------------ % 24.57/4.04 % (3431359)------------------------------ % 24.57/4.04 % (3431388)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=50429339:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 24.57/4.04 % (3431342)Instruction limit reached! % 24.57/4.04 % (3431342)------------------------------ % 24.57/4.04 % (3431342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.57/4.04 % (3431342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.57/4.04 % (3431342)CaDiCaL version: 2.1.3 % 24.57/4.04 % (3431342)Termination reason: Instruction limit % 24.57/4.04 % (3431342)Termination phase: Saturation % 24.57/4.04 % (3431342)Time elapsed: 0.347 s % 24.57/4.04 % (3431342)Peak memory usage: 20 MB % 24.57/4.04 % (3431342)Instructions burned: 880 (million) % 24.57/4.04 % (3431427)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1430925259:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 24.57/4.04 % (3431388)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.57/4.04 % (3431388)Terminated due to inappropriate strategy. % 24.57/4.04 % (3431388)------------------------------ % 24.57/4.04 % (3431388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.57/4.04 % (3431388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.57/4.04 % (3431388)CaDiCaL version: 2.1.3 % 24.57/4.04 % (3431388)Termination reason: Inappropriate % 24.57/4.04 % (3431388)Time elapsed: 0.144 s % 24.57/4.04 % (3431388)Peak memory usage: 13 MB % 24.57/4.04 % (3431388)Instructions burned: 293 (million) % 24.57/4.04 % (3431388)------------------------------ % 24.57/4.04 % (3431388)------------------------------ % 24.57/4.04 % (3431427)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.57/4.04 % (3431427)Terminated due to inappropriate strategy. % 24.57/4.04 % (3431427)------------------------------ % 24.57/4.04 % (3431427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.57/4.04 % (3431427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.57/4.04 % (3431427)CaDiCaL version: 2.1.3 % 24.57/4.04 % (3431427)Termination reason: Inappropriate % 24.57/4.04 % (3431427)Time elapsed: 0.036 s % 24.57/4.04 % (3431427)Peak memory usage: 12 MB % 24.57/4.04 % (3431427)Instructions burned: 81 (million) % 24.57/4.04 % (3431427)------------------------------ % 24.57/4.04 % (3431427)------------------------------ % 24.57/4.04 % (3431439)ott-2_1_sil=16000:newcnf=on:random_seed=1067879725:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 24.57/4.04 % (3431446)ott+10_1_sil=32000:tgt=ground:random_seed=397911395:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 24.57/4.04 % (3431336)Instruction limit reached! % 24.57/4.04 % (3431336)------------------------------ % 24.57/4.04 % (3431336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.57/4.04 % (3431336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.57/4.04 % (3431336)CaDiCaL version: 2.1.3 % 24.57/4.04 % (3431336)Termination reason: Instruction limit % 24.57/4.04 % (3431336)Termination phase: Saturation % 24.57/4.04 % (3431336)Time elapsed: 0.681 s % 24.57/4.04 % (3431336)Peak memory usage: 25 MB % 24.57/4.04 % (3431336)Instructions burned: 1180 (million) % 24.57/4.04 % (3431483)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2381151389:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 24.57/4.04 % (3431373)Instruction limit reached! % 24.57/4.04 % (3431373)------------------------------ % 24.57/4.04 % (3431373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.57/4.04 % (3431373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.57/4.04 % (3431373)CaDiCaL version: 2.1.3 % 24.57/4.04 % (3431373)Termination reason: Instruction limit % 24.57/4.04 % (3431373)Termination phase: Saturation % 24.57/4.04 % (3431373)Time elapsed: 0.459 s % 24.57/4.04 % (3431373)Peak memory usage: 32 MB % 24.57/4.04 % (3431373)Instructions burned: 1472 (million) % 24.57/4.04 % (3431485)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2624705342:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 108.57/15.61 % (3431483)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.57/15.61 % (3431483)Terminated due to inappropriate strategy. % 108.57/15.61 % (3431483)------------------------------ % 108.57/15.61 % (3431483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.57/15.61 % (3431483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.57/15.61 % (3431483)CaDiCaL version: 2.1.3 % 108.57/15.61 % (3431483)Termination reason: Inappropriate % 108.57/15.61 % (3431483)Time elapsed: 0.139 s % 108.57/15.61 % (3431483)Peak memory usage: 13 MB % 108.57/15.61 % (3431483)Instructions burned: 294 (million) % 108.57/15.61 % (3431483)------------------------------ % 108.57/15.61 % (3431483)------------------------------ % 108.57/15.61 % (3431487)dis+21_1_sil=32000:sas=cadical:random_seed=1862561205:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 108.57/15.61 % (3431439)Instruction limit reached! % 108.57/15.61 % (3431439)------------------------------ % 108.57/15.61 % (3431439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.57/15.61 % (3431439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.57/15.61 % (3431439)CaDiCaL version: 2.1.3 % 108.57/15.61 % (3431439)Termination reason: Instruction limit % 108.57/15.61 % (3431439)Termination phase: Saturation % 108.57/15.61 % (3431439)Time elapsed: 0.464 s % 108.57/15.61 % (3431439)Peak memory usage: 24 MB % 108.57/15.61 % (3431439)Instructions burned: 870 (million) % 108.57/15.61 % (3431489)ott+11_1_sil=16000:gs=on:random_seed=2857572673:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 108.57/15.61 % (3431489)Instruction limit reached! % 108.57/15.61 % (3431489)------------------------------ % 108.57/15.61 % (3431489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.57/15.61 % (3431489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.57/15.61 % (3431489)CaDiCaL version: 2.1.3 % 108.57/15.61 % (3431489)Termination reason: Instruction limit % 108.57/15.61 % (3431489)Termination phase: Saturation % 108.57/15.61 % (3431489)Time elapsed: 1.224 s % 108.57/15.61 % (3431489)Peak memory usage: 31 MB % 108.57/15.61 % (3431489)Instructions burned: 2252 (million) % 108.57/15.61 % (3431491)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1219494900:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi) % 108.57/15.61 % (3431491)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.57/15.61 % (3431491)Terminated due to inappropriate strategy. % 108.57/15.61 % (3431491)------------------------------ % 108.57/15.61 % (3431491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.57/15.61 % (3431491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.57/15.61 % (3431491)CaDiCaL version: 2.1.3 % 108.57/15.61 % (3431491)Termination reason: Inappropriate % 108.57/15.61 % (3431491)Time elapsed: 0.035 s % 108.57/15.61 % (3431491)Peak memory usage: 12 MB % 108.57/15.61 % (3431491)Instructions burned: 81 (million) % 108.57/15.61 % (3431491)------------------------------ % 108.57/15.61 % (3431491)------------------------------ % 108.57/15.61 % (3431493)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3115787513:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2975 on theBenchmark for (2975ds/4591Mi) % 108.57/15.61 % (3431487)Instruction limit reached! % 108.57/15.61 % (3431487)------------------------------ % 108.57/15.61 % (3431487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.57/15.61 % (3431487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.57/15.61 % (3431487)CaDiCaL version: 2.1.3 % 108.57/15.61 % (3431487)Termination reason: Instruction limit % 108.57/15.61 % (3431487)Termination phase: Saturation % 108.57/15.61 % (3431487)Time elapsed: 1.651 s % 108.57/15.61 % (3431487)Peak memory usage: 52 MB % 108.57/15.61 % (3431487)Instructions burned: 3774 (million) % 108.57/15.61 % (3431495)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1500411464:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 108.57/15.61 % (3431485)Instruction limit reached! % 108.57/15.61 % (3431485)------------------------------ % 108.57/15.61 % (3431485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.57/15.61 % (3431485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.57/15.61 % (3431485)CaDiCaL version: 2.1.3 % 156.14/22.31 % (3431485)Termination reason: Instruction limit % 156.14/22.31 % (3431485)Termination phase: Saturation % 156.14/22.31 % (3431485)Time elapsed: 1.857 s % 156.14/22.31 % (3431485)Peak memory usage: 35 MB % 156.14/22.31 % (3431485)Instructions burned: 3514 (million) % 156.14/22.31 % (3431497)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=99095102:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 156.14/22.31 % (3431363)Instruction limit reached! % 156.14/22.31 % (3431363)------------------------------ % 156.14/22.31 % (3431363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.14/22.31 % (3431363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.14/22.31 % (3431363)CaDiCaL version: 2.1.3 % 156.14/22.31 % (3431363)Termination reason: Instruction limit % 156.14/22.31 % (3431363)Termination phase: Saturation % 156.14/22.31 % (3431363)Time elapsed: 2.734 s % 156.14/22.31 % (3431363)Peak memory usage: 50 MB % 156.14/22.31 % (3431363)Instructions burned: 5131 (million) % 156.14/22.31 % (3431499)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3713044899:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 156.14/22.31 % (3431499)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.14/22.31 % (3431499)Terminated due to inappropriate strategy. % 156.14/22.31 % (3431499)------------------------------ % 156.14/22.31 % (3431499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.14/22.31 % (3431499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.14/22.31 % (3431499)CaDiCaL version: 2.1.3 % 156.14/22.31 % (3431499)Termination reason: Inappropriate % 156.14/22.31 % (3431499)Time elapsed: 0.085 s % 156.14/22.31 % (3431499)Peak memory usage: 14 MB % 156.14/22.31 % (3431499)Instructions burned: 177 (million) % 156.14/22.31 % (3431499)------------------------------ % 156.14/22.31 % (3431499)------------------------------ % 156.14/22.31 % (3431501)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2646831481:fmbsr=2:i=46332_2966 on theBenchmark for (2966ds/46332Mi) % 156.14/22.31 % (3431501)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.14/22.31 % (3431501)Terminated due to inappropriate strategy. % 156.14/22.31 % (3431501)------------------------------ % 156.14/22.31 % (3431501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.14/22.31 % (3431501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.14/22.31 % (3431501)CaDiCaL version: 2.1.3 % 156.14/22.31 % (3431501)Termination reason: Inappropriate % 156.14/22.31 % (3431501)Time elapsed: 0.034 s % 156.14/22.31 % (3431501)Peak memory usage: 12 MB % 156.14/22.31 % (3431501)Instructions burned: 81 (million) % 156.14/22.31 % (3431501)------------------------------ % 156.14/22.31 % (3431501)------------------------------ % 156.14/22.31 % (3431503)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3344577875:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 156.14/22.31 % (3431503)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.14/22.31 % (3431503)Terminated due to inappropriate strategy. % 156.14/22.31 % (3431503)------------------------------ % 156.14/22.31 % (3431503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.14/22.31 % (3431503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.14/22.31 % (3431503)CaDiCaL version: 2.1.3 % 156.14/22.31 % (3431503)Termination reason: Inappropriate % 156.14/22.31 % (3431503)Time elapsed: 0.035 s % 156.14/22.31 % (3431503)Peak memory usage: 12 MB % 156.14/22.31 % (3431503)Instructions burned: 81 (million) % 156.14/22.31 % (3431503)------------------------------ % 156.14/22.31 % (3431503)------------------------------ % 156.14/22.31 % (3431505)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1951140253:i=22565:add=on:rawr=on_2965 on theBenchmark for (2965ds/22565Mi) % 156.14/22.31 % (3431446)Instruction limit reached! % 156.14/22.31 % (3431446)------------------------------ % 156.14/22.31 % (3431446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.14/22.31 % (3431446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.14/22.31 % (3431446)CaDiCaL version: 2.1.3 % 156.14/22.31 % (3431446)Termination reason: Instruction limit % 156.14/22.31 % (3431446)Termination phase: Saturation % 156.14/22.31 % (3431446)Time elapsed: 3.038 s % 156.14/22.31 % (3431446)Peak memory usage: 36 MB % 156.14/22.31 % (3431446)Instructions burned: 5114 (million) % 156.14/22.31 % (3431507)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1745141845:i=8173:av=off_2962 on theBenchmark for (2962ds/8173Mi) % 158.95/22.70 % (3431493)Instruction limit reached! % 158.95/22.70 % (3431493)------------------------------ % 158.95/22.70 % (3431493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.95/22.70 % (3431493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.95/22.70 % (3431493)CaDiCaL version: 2.1.3 % 158.95/22.70 % (3431493)Termination reason: Instruction limit % 158.95/22.70 % (3431493)Termination phase: Saturation % 158.95/22.70 % (3431493)Time elapsed: 2.427 s % 158.95/22.70 % (3431493)Peak memory usage: 51 MB % 158.95/22.70 % (3431493)Instructions burned: 4592 (million) % 158.95/22.70 % (3431533)dis+10_16:1_sil=16000:random_seed=4058988349:i=9155:fsr=off_2950 on theBenchmark for (2950ds/9155Mi) % 158.95/22.70 % (3431497)Instruction limit reached! % 158.95/22.70 % (3431497)------------------------------ % 158.95/22.70 % (3431497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.95/22.70 % (3431497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.95/22.70 % (3431497)CaDiCaL version: 2.1.3 % 158.95/22.70 % (3431497)Termination reason: Instruction limit % 158.95/22.70 % (3431497)Termination phase: Saturation % 158.95/22.70 % (3431497)Time elapsed: 2.208 s % 158.95/22.70 % (3431497)Peak memory usage: 61 MB % 158.95/22.70 % (3431497)Instructions burned: 5213 (million) % 158.95/22.70 % (3431539)ott-3_8_sil=64000:random_seed=430004217:i=20139:bs=on_2949 on theBenchmark for (2949ds/20139Mi) % 158.95/22.70 % (3431507)Instruction limit reached! % 158.95/22.70 % (3431507)------------------------------ % 158.95/22.70 % (3431507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.95/22.70 % (3431507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.95/22.70 % (3431507)CaDiCaL version: 2.1.3 % 158.95/22.70 % (3431507)Termination reason: Instruction limit % 158.95/22.70 % (3431507)Termination phase: Saturation % 158.95/22.70 % (3431507)Time elapsed: 7.129 s % 158.95/22.70 % (3431507)Peak memory usage: 50 MB % 158.95/22.70 % (3431507)Instructions burned: 8174 (million) % 158.95/22.70 % (3431579)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3644253228:fmbsr=2:i=32576_2890 on theBenchmark for (2890ds/32576Mi) % 158.95/22.70 % (3431579)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.95/22.70 % (3431579)Terminated due to inappropriate strategy. % 158.95/22.70 % (3431579)------------------------------ % 158.95/22.70 % (3431579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.95/22.70 % (3431579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.95/22.70 % (3431579)CaDiCaL version: 2.1.3 % 158.95/22.70 % (3431579)Termination reason: Inappropriate % 158.95/22.70 % (3431579)Time elapsed: 0.143 s % 158.95/22.70 % (3431579)Peak memory usage: 13 MB % 158.95/22.70 % (3431579)Instructions burned: 292 (million) % 158.95/22.70 % (3431579)------------------------------ % 158.95/22.70 % (3431579)------------------------------ % 158.95/22.70 % (3431581)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2132289339:i=11404_2889 on theBenchmark for (2889ds/11404Mi) % 158.95/22.70 % (3431533)Instruction limit reached! % 158.95/22.70 % (3431533)------------------------------ % 158.95/22.70 % (3431533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.95/22.70 % (3431533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.95/22.70 % (3431533)CaDiCaL version: 2.1.3 % 158.95/22.70 % (3431533)Termination reason: Instruction limit % 158.95/22.70 % (3431533)Termination phase: Saturation % 158.95/22.70 % (3431533)Time elapsed: 7.431 s % 158.95/22.70 % (3431533)Peak memory usage: 59 MB % 158.95/22.70 % (3431533)Instructions burned: 9155 (million) % 158.95/22.70 % (3431628)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=941058302:i=14134_2876 on theBenchmark for (2876ds/14134Mi) % 158.95/22.70 % (3431539)Instruction limit reached! % 158.95/22.70 % (3431539)------------------------------ % 158.95/22.70 % (3431539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.95/22.70 % (3431539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.95/22.70 % (3431539)CaDiCaL version: 2.1.3 % 158.95/22.70 % (3431539)Termination reason: Instruction limit % 158.95/22.70 % (3431539)Termination phase: Saturation % 158.95/22.70 % (3431539)Time elapsed: 8.311 s % 158.95/22.70 % (3431539)Peak memory usage: 58 MB % 158.95/22.70 % (3431539)Instructions burned: 20142 (million) % 158.95/22.70 % (3431691)dis+33_16_sil=32000:sac=on:random_seed=3375366272:i=15851:nm=0_2865 on theBenchmark for (2865ds/15851Mi) % 158.95/22.70 % (3431505)Instruction limit reached! % 158.95/22.70 % (3431505)------------------------------ % 180.27/25.71 % (3431505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.27/25.71 % (3431505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.27/25.71 % (3431505)CaDiCaL version: 2.1.3 % 180.27/25.71 % (3431505)Termination reason: Instruction limit % 180.27/25.71 % (3431505)Termination phase: Saturation % 180.27/25.71 % (3431505)Time elapsed: 11.875 s % 180.27/25.71 % (3431505)Peak memory usage: 29 MB % 180.27/25.71 % (3431505)Instructions burned: 22565 (million) % 180.27/25.71 % (3431740)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3721958946:avsq=on:i=17627:add=on:amm=off_2846 on theBenchmark for (2846ds/17627Mi) % 180.27/25.71 % (3431581)Instruction limit reached! % 180.27/25.71 % (3431581)------------------------------ % 180.27/25.71 % (3431581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.27/25.71 % (3431581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.27/25.71 % (3431581)CaDiCaL version: 2.1.3 % 180.27/25.71 % (3431581)Termination reason: Instruction limit % 180.27/25.71 % (3431581)Termination phase: Saturation % 180.27/25.71 % (3431581)Time elapsed: 7.609 s % 180.27/25.71 % (3431581)Peak memory usage: 54 MB % 180.27/25.71 % (3431581)Instructions burned: 11404 (million) % 180.27/25.71 % (3431742)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4020502750:s2a=on:i=53295_2812 on theBenchmark for (2812ds/53295Mi) % 180.27/25.71 % (3431628)Instruction limit reached! % 180.27/25.71 % (3431628)------------------------------ % 180.27/25.71 % (3431628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.27/25.71 % (3431628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.27/25.71 % (3431628)CaDiCaL version: 2.1.3 % 180.27/25.71 % (3431628)Termination reason: Instruction limit % 180.27/25.71 % (3431628)Termination phase: Saturation % 180.27/25.71 % (3431628)Time elapsed: 9.165 s % 180.27/25.71 % (3431628)Peak memory usage: 61 MB % 180.27/25.71 % (3431628)Instructions burned: 14135 (million) % 180.27/25.71 % (3431744)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2468575044:i=26857:ins=20_2784 on theBenchmark for (2784ds/26857Mi) % 180.27/25.71 % (3431744)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.27/25.71 % (3431744)Terminated due to inappropriate strategy. % 180.27/25.71 % (3431744)------------------------------ % 180.27/25.71 % (3431744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.27/25.71 % (3431744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.27/25.71 % (3431744)CaDiCaL version: 2.1.3 % 180.27/25.71 % (3431744)Termination reason: Inappropriate % 180.27/25.71 % (3431744)Time elapsed: 0.035 s % 180.27/25.71 % (3431744)Peak memory usage: 12 MB % 180.27/25.71 % (3431744)Instructions burned: 81 (million) % 180.27/25.71 % (3431744)------------------------------ % 180.27/25.71 % (3431744)------------------------------ % 180.27/25.71 % (3431746)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2927839286:i=28120:bs=on:fsr=off_2783 on theBenchmark for (2783ds/28120Mi) % 180.27/25.71 % (3431495)Instruction limit reached! % 180.27/25.71 % (3431495)------------------------------ % 180.27/25.71 % (3431495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.27/25.71 % (3431495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.27/25.71 % (3431495)CaDiCaL version: 2.1.3 % 180.27/25.71 % (3431495)Termination reason: Instruction limit % 180.27/25.71 % (3431495)Termination phase: Saturation % 180.27/25.71 % (3431495)Time elapsed: 19.205 s % 180.27/25.71 % (3431495)Peak memory usage: 96 MB % 180.27/25.71 % (3431495)Instructions burned: 29340 (million) % 180.27/25.71 % (3431748)fmb+10_1_sil=256000:fmbss=7:random_seed=4286940266:fmbsr=1.6:i=182295_2780 on theBenchmark for (2780ds/182295Mi) % 180.27/25.71 % (3431748)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.27/25.71 % (3431748)Terminated due to inappropriate strategy. % 180.27/25.71 % (3431748)------------------------------ % 180.27/25.71 % (3431748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.27/25.71 % (3431748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.27/25.71 % (3431748)CaDiCaL version: 2.1.3 % 180.27/25.71 % (3431748)Termination reason: Inappropriate % 180.27/25.71 % (3431748)Time elapsed: 0.035 s % 180.27/25.71 % (3431748)Peak memory usage: 12 MB % 180.27/25.71 % (3431748)Instructions burned: 81 (million) % 180.27/25.71 % (3431748)------------------------------ % 180.27/25.71 % (3431748)------------------------------ % 180.27/25.71 % (3431750)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2354758640:i=44625:gsp=on_2779 on theBenchmark for (2779ds/44625Mi) % 192.28/27.42 % (3431750)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.28/27.42 % (3431750)Terminated due to inappropriate strategy. % 192.28/27.42 % (3431750)------------------------------ % 192.28/27.42 % (3431750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.28/27.42 % (3431750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.28/27.42 % (3431750)CaDiCaL version: 2.1.3 % 192.28/27.42 % (3431750)Termination reason: Inappropriate % 192.28/27.42 % (3431750)Time elapsed: 0.051 s % 192.28/27.42 % (3431750)Peak memory usage: 12 MB % 192.28/27.42 % (3431750)Instructions burned: 123 (million) % 192.28/27.42 % (3431750)------------------------------ % 192.28/27.42 % (3431750)------------------------------ % 192.28/27.42 % (3431752)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2482209762:i=160505_2778 on theBenchmark for (2778ds/160505Mi) % 192.28/27.42 % (3431752)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.28/27.42 % (3431752)Terminated due to inappropriate strategy. % 192.28/27.42 % (3431752)------------------------------ % 192.28/27.42 % (3431752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.28/27.42 % (3431752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.28/27.42 % (3431752)CaDiCaL version: 2.1.3 % 192.28/27.42 % (3431752)Termination reason: Inappropriate % 192.28/27.42 % (3431752)Time elapsed: 0.035 s % 192.28/27.42 % (3431752)Peak memory usage: 12 MB % 192.28/27.42 % (3431752)Instructions burned: 81 (million) % 192.28/27.42 % (3431752)------------------------------ % 192.28/27.42 % (3431752)------------------------------ % 192.28/27.42 % (3431754)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2524252790:fmbsr=1.3:i=225729_2778 on theBenchmark for (2778ds/225729Mi) % 192.28/27.42 % (3431754)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.28/27.42 % (3431754)Terminated due to inappropriate strategy. % 192.28/27.42 % (3431754)------------------------------ % 192.28/27.42 % (3431754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.28/27.42 % (3431754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.28/27.42 % (3431754)CaDiCaL version: 2.1.3 % 192.28/27.42 % (3431754)Termination reason: Inappropriate % 192.28/27.42 % (3431754)Time elapsed: 0.035 s % 192.28/27.42 % (3431754)Peak memory usage: 12 MB % 192.28/27.42 % (3431754)Instructions burned: 81 (million) % 192.28/27.42 % (3431754)------------------------------ % 192.28/27.42 % (3431754)------------------------------ % 192.28/27.42 % (3431756)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=651038692:fmbsr=2:i=185024:ins=7_2777 on theBenchmark for (2777ds/185024Mi) % 192.28/27.42 % (3431756)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.28/27.42 % (3431756)Terminated due to inappropriate strategy. % 192.28/27.42 % (3431756)------------------------------ % 192.28/27.42 % (3431756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.28/27.42 % (3431756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.28/27.42 % (3431756)CaDiCaL version: 2.1.3 % 192.28/27.42 % (3431756)Termination reason: Inappropriate % 192.28/27.42 % (3431756)Time elapsed: 0.035 s % 192.28/27.42 % (3431756)Peak memory usage: 12 MB % 192.28/27.42 % (3431756)Instructions burned: 81 (million) % 192.28/27.42 % (3431756)------------------------------ % 192.28/27.42 % (3431756)------------------------------ % 192.28/27.42 % (3431758)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3107980784:rtra=on_2777 on theBenchmark for (2777ds/0Mi) % 192.28/27.42 % (3431758)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.28/27.42 % (3431758)Terminated due to inappropriate strategy. % 192.28/27.42 % (3431758)------------------------------ % 192.28/27.42 % (3431758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.28/27.42 % (3431758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.28/27.42 % (3431758)CaDiCaL version: 2.1.3 % 192.28/27.42 % (3431758)Termination reason: Inappropriate % 192.28/27.42 % (3431758)Time elapsed: 0.119 s % 192.28/27.42 % (3431758)Peak memory usage: 14 MB % 192.28/27.42 % (3431758)Instructions burned: 245 (million) % 192.28/27.42 % (3431758)------------------------------ % 192.28/27.42 % (3431758)------------------------------ % 192.28/27.42 % (3431760)% WARNING: option uhcvi not known. % 192.28/27.42 % (3431760)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=536561881:i=271062:add=off:rtra=on:rawr=on_2775 on theBenchmark for (2775ds/271062Mi) % 216.43/30.84 % (3431691)Instruction limit reached! % 216.43/30.84 % (3431691)------------------------------ % 216.43/30.84 % (3431691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.43/30.84 % (3431691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.43/30.84 % (3431691)CaDiCaL version: 2.1.3 % 216.43/30.84 % (3431691)Termination reason: Instruction limit % 216.43/30.84 % (3431691)Termination phase: Clausification % 216.43/30.84 % (3431691)Time elapsed: 9.356 s % 216.43/30.84 % (3431691)Peak memory usage: 8622 MB % 216.43/30.84 % (3431691)Instructions burned: 15852 (million) % 216.43/30.84 % (3431762)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1485531916:i=176048:add=on:rtra=on:rawr=on_2766 on theBenchmark for (2766ds/176048Mi) % 216.43/30.84 % (3431740)Instruction limit reached! % 216.43/30.84 % (3431740)------------------------------ % 216.43/30.84 % (3431740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.43/30.84 % (3431740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.43/30.84 % (3431740)CaDiCaL version: 2.1.3 % 216.43/30.84 % (3431740)Termination reason: Instruction limit % 216.43/30.84 % (3431740)Termination phase: Saturation % 216.43/30.84 % (3431740)Time elapsed: 9.419 s % 216.43/30.84 % (3431740)Peak memory usage: 266 MB % 216.43/30.84 % (3431740)Instructions burned: 17627 (million) % 216.43/30.84 % (3431764)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2381075553:i=206:fgj=on:rtra=on_2751 on theBenchmark for (2751ds/206Mi) % 216.43/30.84 % (3431764)Instruction limit reached! % 216.43/30.84 % (3431764)------------------------------ % 216.43/30.84 % (3431764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.43/30.84 % (3431764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.43/30.84 % (3431764)CaDiCaL version: 2.1.3 % 216.43/30.84 % (3431764)Termination reason: Instruction limit % 216.43/30.84 % (3431764)Termination phase: Saturation % 216.43/30.84 % (3431764)Time elapsed: 0.102 s % 216.43/30.84 % (3431764)Peak memory usage: 17 MB % 216.43/30.84 % (3431764)Instructions burned: 206 (million) % 216.43/30.84 % (3431766)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=288658601:i=232:rtra=on_2750 on theBenchmark for (2750ds/232Mi) % 216.43/30.84 % (3431766)Instruction limit reached! % 216.43/30.84 % (3431766)------------------------------ % 216.43/30.84 % (3431766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.43/30.84 % (3431766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.43/30.84 % (3431766)CaDiCaL version: 2.1.3 % 216.43/30.84 % (3431766)Termination reason: Instruction limit % 216.43/30.84 % (3431766)Termination phase: Blocked clause elimination % 216.43/30.84 % (3431766)Time elapsed: 0.106 s % 216.43/30.84 % (3431766)Peak memory usage: 14 MB % 216.43/30.84 % (3431766)Instructions burned: 233 (million) % 216.43/30.84 % (3431768)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=968682519:i=262:rtra=on_2749 on theBenchmark for (2749ds/262Mi) % 216.43/30.84 % (3431768)Instruction limit reached! % 216.43/30.84 % (3431768)------------------------------ % 216.43/30.84 % (3431768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.43/30.84 % (3431768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.43/30.84 % (3431768)CaDiCaL version: 2.1.3 % 216.43/30.84 % (3431768)Termination reason: Instruction limit % 216.43/30.84 % (3431768)Termination phase: Saturation % 216.43/30.84 % (3431768)Time elapsed: 0.139 s % 216.43/30.84 % (3431768)Peak memory usage: 18 MB % 216.43/30.84 % (3431768)Instructions burned: 263 (million) % 216.43/30.84 % (3431770)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2709410163:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2747 on theBenchmark for (2747ds/318Mi) % 216.43/30.84 % (3431770)Instruction limit reached! % 216.43/30.84 % (3431770)------------------------------ % 216.43/30.84 % (3431770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.43/30.84 % (3431770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.43/30.84 % (3431770)CaDiCaL version: 2.1.3 % 216.43/30.84 % (3431770)Termination reason: Instruction limit % 216.43/30.84 % (3431770)Termination phase: Saturation % 216.43/30.84 % (3431770)Time elapsed: 0.169 s % 216.43/30.84 % (3431770)Peak memory usage: 19 MB % 216.43/30.84 % (3431770)Instructions burned: 320 (million) % 216.43/30.84 % (3431772)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=826719930:i=1428:nm=2:rtra=on_2745 on theBenchmark for (2745ds/1428Mi) % 256.91/36.54 % (3431772)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 256.91/36.54 % (3431772)Terminated due to inappropriate strategy. % 256.91/36.54 % (3431772)------------------------------ % 256.91/36.54 % (3431772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.91/36.54 % (3431772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.91/36.54 % (3431772)CaDiCaL version: 2.1.3 % 256.91/36.54 % (3431772)Termination reason: Inappropriate % 256.91/36.54 % (3431772)Time elapsed: 0.035 s % 256.91/36.54 % (3431772)Peak memory usage: 13 MB % 256.91/36.54 % (3431772)Instructions burned: 77 (million) % 256.91/36.54 % (3431772)------------------------------ % 256.91/36.54 % (3431772)------------------------------ % 256.91/36.54 % (3431774)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3105383529:i=262:bd=preordered:rtra=on:fsd=on_2745 on theBenchmark for (2745ds/262Mi) % 256.91/36.54 % (3431774)Instruction limit reached! % 256.91/36.54 % (3431774)------------------------------ % 256.91/36.54 % (3431774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.91/36.54 % (3431774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.91/36.54 % (3431774)CaDiCaL version: 2.1.3 % 256.91/36.54 % (3431774)Termination reason: Instruction limit % 256.91/36.54 % (3431774)Termination phase: Saturation % 256.91/36.54 % (3431774)Time elapsed: 0.125 s % 256.91/36.54 % (3431774)Peak memory usage: 14 MB % 256.91/36.54 % (3431774)Instructions burned: 263 (million) % 256.91/36.54 % (3431776)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3921428865:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2743 on theBenchmark for (2743ds/1368Mi) % 256.91/36.54 % (3431776)Instruction limit reached! % 256.91/36.54 % (3431776)------------------------------ % 256.91/36.54 % (3431776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.91/36.54 % (3431776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.91/36.54 % (3431776)CaDiCaL version: 2.1.3 % 256.91/36.54 % (3431776)Termination reason: Instruction limit % 256.91/36.54 % (3431776)Termination phase: Saturation % 256.91/36.54 % (3431776)Time elapsed: 0.707 s % 256.91/36.54 % (3431776)Peak memory usage: 35 MB % 256.91/36.54 % (3431776)Instructions burned: 1368 (million) % 256.91/36.54 % (3431778)ott-21_1_sil=16000:si=on:fs=off:random_seed=3630743613:i=360:av=off:fsr=off:rtra=on_2736 on theBenchmark for (2736ds/360Mi) % 256.91/36.54 % (3431778)Instruction limit reached! % 256.91/36.54 % (3431778)------------------------------ % 256.91/36.54 % (3431778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.91/36.54 % (3431778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.91/36.54 % (3431778)CaDiCaL version: 2.1.3 % 256.91/36.54 % (3431778)Termination reason: Instruction limit % 256.91/36.54 % (3431778)Termination phase: Saturation % 256.91/36.54 % (3431778)Time elapsed: 0.174 s % 256.91/36.54 % (3431778)Peak memory usage: 16 MB % 256.91/36.54 % (3431778)Instructions burned: 360 (million) % 256.91/36.54 % (3431780)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4267326694:i=954:bd=all:rtra=on_2734 on theBenchmark for (2734ds/954Mi) % 256.91/36.54 % (3431780)Instruction limit reached! % 256.91/36.54 % (3431780)------------------------------ % 256.91/36.54 % (3431780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.91/36.54 % (3431780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.91/36.54 % (3431780)CaDiCaL version: 2.1.3 % 256.91/36.54 % (3431780)Termination reason: Instruction limit % 256.91/36.54 % (3431780)Termination phase: Saturation % 256.91/36.54 % (3431780)Time elapsed: 0.517 s % 256.91/36.54 % (3431780)Peak memory usage: 20 MB % 256.91/36.54 % (3431780)Instructions burned: 955 (million) % 256.91/36.54 % (3431782)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3227235757:fmbsr=1.3:i=1730:ins=25:rtra=on_2729 on theBenchmark for (2729ds/1730Mi) % 256.91/36.54 % (3431782)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 256.91/36.54 % (3431782)Terminated due to inappropriate strategy. % 256.91/36.54 % (3431782)------------------------------ % 256.91/36.54 % (3431782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 256.91/36.54 % (3431782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.91/36.54 % (3431782)CaDiCaL version: 2.1.3 % 292.41/41.56 % (3431782)Termination reason: Inappropriate % 292.41/41.56 % (3431782)Time elapsed: 0.044 s % 292.41/41.56 % (3431782)Peak memory usage: 14 MB % 292.41/41.56 % (3431782)Instructions burned: 97 (million) % 292.41/41.56 % (3431782)------------------------------ % 292.41/41.56 % (3431782)------------------------------ % 292.41/41.56 % (3431784)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1785133383:i=2358:rtra=on_2728 on theBenchmark for (2728ds/2358Mi) % 292.41/41.56 % (3431784)Instruction limit reached! % 292.41/41.56 % (3431784)------------------------------ % 292.41/41.56 % (3431784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.41/41.56 % (3431784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.41/41.56 % (3431784)CaDiCaL version: 2.1.3 % 292.41/41.56 % (3431784)Termination reason: Instruction limit % 292.41/41.56 % (3431784)Termination phase: Saturation % 292.41/41.56 % (3431784)Time elapsed: 1.502 s % 292.41/41.56 % (3431784)Peak memory usage: 31 MB % 292.41/41.56 % (3431784)Instructions burned: 2359 (million) % 292.41/41.56 % (3431895)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1395049542:i=1778:ins=1:rtra=on_2713 on theBenchmark for (2713ds/1778Mi) % 292.41/41.56 % (3431895)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 292.41/41.56 % (3431895)Terminated due to inappropriate strategy. % 292.41/41.56 % (3431895)------------------------------ % 292.41/41.56 % (3431895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.41/41.56 % (3431895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.41/41.56 % (3431895)CaDiCaL version: 2.1.3 % 292.41/41.56 % (3431895)Termination reason: Inappropriate % 292.41/41.56 % (3431895)Time elapsed: 0.038 s % 292.41/41.56 % (3431895)Peak memory usage: 13 MB % 292.41/41.56 % (3431895)Instructions burned: 86 (million) % 292.41/41.56 % (3431895)------------------------------ % 292.41/41.56 % (3431895)------------------------------ % 292.41/41.56 % (3431923)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1439687413:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2712 on theBenchmark for (2712ds/1384Mi) % 292.41/41.56 % (3431923)Instruction limit reached! % 292.41/41.56 % (3431923)------------------------------ % 292.41/41.56 % (3431923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.41/41.56 % (3431923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.41/41.56 % (3431923)CaDiCaL version: 2.1.3 % 292.41/41.56 % (3431923)Termination reason: Instruction limit % 292.41/41.56 % (3431923)Termination phase: Saturation % 292.41/41.56 % (3431923)Time elapsed: 0.908 s % 292.41/41.56 % (3431923)Peak memory usage: 30 MB % 292.41/41.56 % (3431923)Instructions burned: 1385 (million) % 292.41/41.56 % (3432107)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=4030066480:i=1758:kws=inv_precedence:fsr=off:rtra=on_2703 on theBenchmark for (2703ds/1758Mi) % 292.41/41.56 % (3432107)Instruction limit reached! % 292.41/41.56 % (3432107)------------------------------ % 292.41/41.56 % (3432107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.41/41.56 % (3432107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.41/41.56 % (3432107)CaDiCaL version: 2.1.3 % 292.41/41.56 % (3432107)Termination reason: Instruction limit % 292.41/41.56 % (3432107)Termination phase: Saturation % 292.41/41.56 % (3432107)Time elapsed: 0.800 s % 292.41/41.56 % (3432107)Peak memory usage: 23 MB % 292.41/41.56 % (3432107)Instructions burned: 1759 (million) % 292.41/41.56 % (3432151)fmb+10_1_sil=64000:si=on:random_seed=2474348092:i=44122:nm=2:rtra=on:gsp=on_2695 on theBenchmark for (2695ds/44122Mi) % 292.41/41.56 % (3432151)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 292.41/41.56 % (3432151)Terminated due to inappropriate strategy. % 292.41/41.56 % (3432151)------------------------------ % 292.41/41.56 % (3432151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.41/41.56 % (3432151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.41/41.56 % (3432151)CaDiCaL version: 2.1.3 % 292.41/41.56 % (3432151)Termination reason: Inappropriate % 292.41/41.56 % (3432151)Time elapsed: 0.037 s % 292.41/41.56 % (3432151)Peak memory usage: 13 MB % 292.41/41.56 % (3432151)Instructions burned: 84 (million) % 292.41/41.56 % (3432151)------------------------------ % 292.41/41.56 % (3432151)------------------------------ % 292.41/41.56 % (3432153)fmb+10_1_sil=16000:sas=cadTerminated % 300.54/42.73 % Vampire exiting % 300.54/42.73 Terminated %------------------------------------------------------------------------------