%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX098_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n015.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:46:29 PM UTC 2026 % Result : Timeout 300.50s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX098_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.25 % Computer : n015.cluster.edu % 0.11/0.25 % Model : x86_64 x86_64 % 0.11/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.25 % Memory : 8046.5625MB % 0.11/0.25 % OS : Linux 6.8.0-71-generic % 0.11/0.25 % CPULimit : 300 % 0.11/0.25 % WCLimit : 300 % 0.11/0.25 % DateTime : Mon Sep 28 15:04:17 UTC 2026 % 0.11/0.26 % CPUTime : % 0.11/0.26 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.26/0.30 Running first-order model finding % 0.26/0.30 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 % 5.36/1.10 % (2695475)Will run a generic schedule for satisfiability detection. % 5.36/1.10 % (2695481)% WARNING: option uhcvi not known. % 5.36/1.10 % (2695480)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1137391279_2999 on theBenchmark for (2999ds/0Mi) % 5.36/1.10 % (2695481)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3653425327:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.36/1.10 % (2695480)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.36/1.10 % (2695480)Terminated due to inappropriate strategy. % 5.36/1.10 % (2695480)------------------------------ % 5.36/1.10 % (2695480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.36/1.10 % (2695480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.36/1.10 % (2695480)CaDiCaL version: 2.1.3 % 5.36/1.10 % (2695480)Termination reason: Inappropriate % 5.36/1.10 % (2695480)Time elapsed: 0.006 s % 5.36/1.10 % (2695480)Peak memory usage: 11 MB % 5.36/1.10 % (2695480)Instructions burned: 13 (million) % 5.36/1.10 % (2695480)------------------------------ % 5.36/1.10 % (2695480)------------------------------ % 5.36/1.10 % (2695484)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2825754049:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.36/1.10 % (2695485)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3281439634:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.36/1.10 % (2695483)dis+10_1_sil=32000:sp=arity:random_seed=2088172022:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.36/1.10 % (2695486)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1515100600:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.36/1.10 % (2695482)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1199661612:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.36/1.10 % (2695489)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1066114905:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.36/1.10 % (2695489)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.36/1.10 % (2695489)Terminated due to inappropriate strategy. % 5.36/1.10 % (2695489)------------------------------ % 5.36/1.10 % (2695489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.36/1.10 % (2695489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.36/1.10 % (2695489)CaDiCaL version: 2.1.3 % 5.36/1.10 % (2695489)Termination reason: Inappropriate % 5.36/1.10 % (2695489)Time elapsed: 0.004 s % 5.36/1.10 % (2695489)Peak memory usage: 10 MB % 5.36/1.10 % (2695489)Instructions burned: 8 (million) % 5.36/1.10 % (2695489)------------------------------ % 5.36/1.10 % (2695489)------------------------------ % 5.36/1.10 % (2695496)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4243498302:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.36/1.10 % (2695483)Instruction limit reached! % 5.36/1.10 % (2695483)------------------------------ % 5.36/1.10 % (2695483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.36/1.10 % (2695483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.36/1.10 % (2695483)CaDiCaL version: 2.1.3 % 5.36/1.10 % (2695483)Termination reason: Instruction limit % 5.36/1.10 % (2695483)Termination phase: Saturation % 5.36/1.10 % (2695483)Time elapsed: 0.088 s % 5.36/1.10 % (2695483)Peak memory usage: 12 MB % 5.36/1.10 % (2695483)Instructions burned: 103 (million) % 5.36/1.10 % (2695484)Instruction limit reached! % 5.36/1.10 % (2695484)------------------------------ % 5.36/1.10 % (2695484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.36/1.10 % (2695484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.36/1.10 % (2695484)CaDiCaL version: 2.1.3 % 5.36/1.10 % (2695484)Termination reason: Instruction limit % 5.36/1.10 % (2695484)Termination phase: Saturation % 5.36/1.10 % (2695484)Time elapsed: 0.095 s % 5.36/1.10 % (2695484)Peak memory usage: 13 MB % 5.36/1.10 % (2695484)Instructions burned: 117 (million) % 5.36/1.10 % (2695485)Instruction limit reached! % 5.36/1.10 % (2695485)------------------------------ % 5.36/1.10 % (2695485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.36/1.10 % (2695485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.36/1.10 % (2695485)CaDiCaL version: 2.1.3 % 5.36/1.10 % (2695485)Termination reason: Instruction limit % 6.91/1.44 % (2695485)Termination phase: Saturation % 6.91/1.44 % (2695485)Time elapsed: 0.107 s % 6.91/1.44 % (2695485)Peak memory usage: 13 MB % 6.91/1.44 % (2695485)Instructions burned: 131 (million) % 6.91/1.44 % (2695498)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=328516451:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.91/1.44 % (2695496)Instruction limit reached! % 6.91/1.44 % (2695496)------------------------------ % 6.91/1.44 % (2695496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.91/1.44 % (2695496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.44 % (2695496)CaDiCaL version: 2.1.3 % 6.91/1.44 % (2695496)Termination reason: Instruction limit % 6.91/1.44 % (2695496)Termination phase: Saturation % 6.91/1.44 % (2695496)Time elapsed: 0.069 s % 6.91/1.44 % (2695496)Peak memory usage: 13 MB % 6.91/1.44 % (2695496)Instructions burned: 132 (million) % 6.91/1.44 % (2695499)ott-21_1_sil=16000:fs=off:random_seed=2470173746:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.91/1.44 % (2695500)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=521504451:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.91/1.44 % (2695502)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=299791023:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.91/1.44 % (2695502)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.91/1.44 % (2695502)Terminated due to inappropriate strategy. % 6.91/1.44 % (2695502)------------------------------ % 6.91/1.44 % (2695502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.91/1.44 % (2695502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.44 % (2695502)CaDiCaL version: 2.1.3 % 6.91/1.44 % (2695502)Termination reason: Inappropriate % 6.91/1.44 % (2695502)Time elapsed: 0.003 s % 6.91/1.44 % (2695502)Peak memory usage: 10 MB % 6.91/1.44 % (2695502)Instructions burned: 6 (million) % 6.91/1.44 % (2695502)------------------------------ % 6.91/1.44 % (2695502)------------------------------ % 6.91/1.44 % (2695486)Instruction limit reached! % 6.91/1.44 % (2695486)------------------------------ % 6.91/1.44 % (2695486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.91/1.44 % (2695486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.44 % (2695486)CaDiCaL version: 2.1.3 % 6.91/1.44 % (2695486)Termination reason: Instruction limit % 6.91/1.44 % (2695486)Termination phase: Saturation % 6.91/1.44 % (2695486)Time elapsed: 0.171 s % 6.91/1.44 % (2695486)Peak memory usage: 14 MB % 6.91/1.44 % (2695486)Instructions burned: 159 (million) % 6.91/1.44 % (2695506)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2720912384:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 6.91/1.44 % (2695507)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=752540916:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 6.91/1.44 % (2695507)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.91/1.44 % (2695507)Terminated due to inappropriate strategy. % 6.91/1.44 % (2695507)------------------------------ % 6.91/1.44 % (2695507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.91/1.44 % (2695507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.44 % (2695507)CaDiCaL version: 2.1.3 % 6.91/1.44 % (2695507)Termination reason: Inappropriate % 6.91/1.44 % (2695507)Time elapsed: 0.004 s % 6.91/1.44 % (2695507)Peak memory usage: 11 MB % 6.91/1.44 % (2695507)Instructions burned: 7 (million) % 6.91/1.44 % (2695507)------------------------------ % 6.91/1.44 % (2695507)------------------------------ % 6.91/1.44 % (2695510)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=4253444784: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.91/1.44 % (2695499)Instruction limit reached! % 6.91/1.44 % (2695499)------------------------------ % 6.91/1.44 % (2695499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.91/1.44 % (2695499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.44 % (2695499)CaDiCaL version: 2.1.3 % 6.91/1.44 % (2695499)Termination reason: Instruction limit % 6.91/1.44 % (2695499)Termination phase: Saturation % 29.93/4.57 % (2695499)Time elapsed: 0.149 s % 29.93/4.57 % (2695499)Peak memory usage: 13 MB % 29.93/4.57 % (2695499)Instructions burned: 181 (million) % 29.93/4.57 % (2695512)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1214035519:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 29.93/4.57 % (2695506)Instruction limit reached! % 29.93/4.57 % (2695506)------------------------------ % 29.93/4.57 % (2695506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.93/4.57 % (2695506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.93/4.57 % (2695506)CaDiCaL version: 2.1.3 % 29.93/4.57 % (2695506)Termination reason: Instruction limit % 29.93/4.57 % (2695506)Termination phase: Saturation % 29.93/4.57 % (2695506)Time elapsed: 0.401 s % 29.93/4.57 % (2695506)Peak memory usage: 14 MB % 29.93/4.57 % (2695506)Instructions burned: 1182 (million) % 29.93/4.57 % (2695514)fmb+10_1_sil=64000:random_seed=426664250:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 29.93/4.57 % (2695514)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.93/4.57 % (2695514)Terminated due to inappropriate strategy. % 29.93/4.57 % (2695514)------------------------------ % 29.93/4.57 % (2695514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.93/4.57 % (2695514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.93/4.57 % (2695514)CaDiCaL version: 2.1.3 % 29.93/4.57 % (2695514)Termination reason: Inappropriate % 29.93/4.57 % (2695514)Time elapsed: 0.007 s % 29.93/4.57 % (2695514)Peak memory usage: 11 MB % 29.93/4.57 % (2695514)Instructions burned: 10 (million) % 29.93/4.57 % (2695514)------------------------------ % 29.93/4.57 % (2695514)------------------------------ % 29.93/4.57 % (2695500)Instruction limit reached! % 29.93/4.57 % (2695500)------------------------------ % 29.93/4.57 % (2695500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.93/4.57 % (2695500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.93/4.57 % (2695500)CaDiCaL version: 2.1.3 % 29.93/4.57 % (2695500)Termination reason: Instruction limit % 29.93/4.57 % (2695500)Termination phase: Saturation % 29.93/4.57 % (2695500)Time elapsed: 0.499 s % 29.93/4.57 % (2695500)Peak memory usage: 14 MB % 29.93/4.57 % (2695500)Instructions burned: 477 (million) % 29.93/4.57 % (2695516)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2743713866:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 29.93/4.57 % (2695517)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4065853773:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 29.93/4.57 % (2695517)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.93/4.57 % (2695517)Terminated due to inappropriate strategy. % 29.93/4.57 % (2695517)------------------------------ % 29.93/4.57 % (2695517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.93/4.57 % (2695517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.93/4.57 % (2695517)CaDiCaL version: 2.1.3 % 29.93/4.57 % (2695517)Termination reason: Inappropriate % 29.93/4.57 % (2695517)Time elapsed: 0.004 s % 29.93/4.57 % (2695517)Peak memory usage: 10 MB % 29.93/4.57 % (2695517)Instructions burned: 8 (million) % 29.93/4.57 % (2695516)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.93/4.57 % (2695516)Terminated due to inappropriate strategy. % 29.93/4.57 % (2695516)------------------------------ % 29.93/4.57 % (2695516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.93/4.57 % (2695516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.93/4.57 % (2695516)CaDiCaL version: 2.1.3 % 29.93/4.57 % (2695516)Termination reason: Inappropriate % 29.93/4.57 % (2695516)Time elapsed: 0.009 s % 29.93/4.57 % (2695516)Peak memory usage: 10 MB % 29.93/4.57 % (2695516)Instructions burned: 8 (million) % 29.93/4.57 % (2695517)------------------------------ % 29.93/4.57 % (2695517)------------------------------ % 29.93/4.57 % (2695516)------------------------------ % 29.93/4.57 % (2695516)------------------------------ % 29.93/4.57 % (2695520)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=840812938:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 29.93/4.57 % (2695521)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3437865231:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 29.93/4.57 % (2695498)Instruction limit reached! % 29.93/4.57 % (2695498)------------------------------ % 39.03/5.95 % (2695498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.03/5.95 % (2695498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.03/5.95 % (2695498)CaDiCaL version: 2.1.3 % 39.03/5.95 % (2695498)Termination reason: Instruction limit % 39.03/5.95 % (2695498)Termination phase: Saturation % 39.03/5.95 % (2695498)Time elapsed: 0.627 s % 39.03/5.95 % (2695498)Peak memory usage: 18 MB % 39.03/5.95 % (2695498)Instructions burned: 684 (million) % 39.03/5.95 % (2695524)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1706996654:i=6324_2992 on theBenchmark for (2992ds/6324Mi) % 39.03/5.95 % (2695524)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.03/5.95 % (2695524)Terminated due to inappropriate strategy. % 39.03/5.95 % (2695524)------------------------------ % 39.03/5.95 % (2695524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.03/5.95 % (2695524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.03/5.95 % (2695524)CaDiCaL version: 2.1.3 % 39.03/5.95 % (2695524)Termination reason: Inappropriate % 39.03/5.95 % (2695524)Time elapsed: 0.007 s % 39.03/5.95 % (2695524)Peak memory usage: 11 MB % 39.03/5.95 % (2695524)Instructions burned: 13 (million) % 39.03/5.95 % (2695524)------------------------------ % 39.03/5.95 % (2695524)------------------------------ % 39.03/5.95 % (2695526)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2581207603:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi) % 39.03/5.95 % (2695526)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.03/5.95 % (2695526)Terminated due to inappropriate strategy. % 39.03/5.95 % (2695526)------------------------------ % 39.03/5.95 % (2695526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.03/5.95 % (2695526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.03/5.95 % (2695526)CaDiCaL version: 2.1.3 % 39.03/5.95 % (2695526)Termination reason: Inappropriate % 39.03/5.95 % (2695526)Time elapsed: 0.008 s % 39.03/5.95 % (2695526)Peak memory usage: 11 MB % 39.03/5.95 % (2695526)Instructions burned: 8 (million) % 39.03/5.95 % (2695526)------------------------------ % 39.03/5.95 % (2695526)------------------------------ % 39.03/5.95 % (2695528)ott-2_1_sil=16000:newcnf=on:random_seed=1580153507:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 39.03/5.95 % (2695510)Instruction limit reached! % 39.03/5.95 % (2695510)------------------------------ % 39.03/5.95 % (2695510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.03/5.95 % (2695510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.03/5.95 % (2695510)CaDiCaL version: 2.1.3 % 39.03/5.95 % (2695510)Termination reason: Instruction limit % 39.03/5.95 % (2695510)Termination phase: Saturation % 39.03/5.95 % (2695510)Time elapsed: 0.719 s % 39.03/5.95 % (2695510)Peak memory usage: 20 MB % 39.03/5.95 % (2695510)Instructions burned: 692 (million) % 39.03/5.95 % (2695530)ott+10_1_sil=32000:tgt=ground:random_seed=3313952398:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 39.03/5.95 % (2695512)Instruction limit reached! % 39.03/5.95 % (2695512)------------------------------ % 39.03/5.95 % (2695512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.03/5.95 % (2695512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.03/5.95 % (2695512)CaDiCaL version: 2.1.3 % 39.03/5.95 % (2695512)Termination reason: Instruction limit % 39.03/5.95 % (2695512)Termination phase: Saturation % 39.03/5.95 % (2695512)Time elapsed: 0.696 s % 39.03/5.95 % (2695512)Peak memory usage: 19 MB % 39.03/5.95 % (2695512)Instructions burned: 879 (million) % 39.03/5.95 % (2695532)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3727304934:i=54282_2989 on theBenchmark for (2989ds/54282Mi) % 39.03/5.95 % (2695532)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.03/5.95 % (2695532)Terminated due to inappropriate strategy. % 39.03/5.95 % (2695532)------------------------------ % 39.03/5.95 % (2695532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.03/5.95 % (2695532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.03/5.95 % (2695532)CaDiCaL version: 2.1.3 % 39.03/5.95 % (2695532)Termination reason: Inappropriate % 39.03/5.95 % (2695532)Time elapsed: 0.012 s % 39.03/5.95 % (2695532)Peak memory usage: 11 MB % 39.03/5.95 % (2695532)Instructions burned: 13 (million) % 113.02/16.23 % (2695532)------------------------------ % 113.02/16.23 % (2695532)------------------------------ % 113.02/16.23 % (2695534)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4012197421:i=3512:aac=none_2988 on theBenchmark for (2988ds/3512Mi) % 113.02/16.23 % (2695528)Instruction limit reached! % 113.02/16.23 % (2695528)------------------------------ % 113.02/16.23 % (2695528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.02/16.23 % (2695528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.02/16.23 % (2695528)CaDiCaL version: 2.1.3 % 113.02/16.23 % (2695528)Termination reason: Instruction limit % 113.02/16.23 % (2695528)Termination phase: Saturation % 113.02/16.23 % (2695528)Time elapsed: 0.826 s % 113.02/16.23 % (2695528)Peak memory usage: 20 MB % 113.02/16.23 % (2695528)Instructions burned: 869 (million) % 113.02/16.23 % (2695536)dis+21_1_sil=32000:sas=cadical:random_seed=49560390:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi) % 113.02/16.23 % (2695521)Instruction limit reached! % 113.02/16.23 % (2695521)------------------------------ % 113.02/16.23 % (2695521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.02/16.23 % (2695521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.02/16.23 % (2695521)CaDiCaL version: 2.1.3 % 113.02/16.23 % (2695521)Termination reason: Instruction limit % 113.02/16.23 % (2695521)Termination phase: Saturation % 113.02/16.23 % (2695521)Time elapsed: 1.403 s % 113.02/16.23 % (2695521)Peak memory usage: 28 MB % 113.02/16.23 % (2695521)Instructions burned: 1472 (million) % 113.02/16.23 % (2695540)ott+11_1_sil=16000:gs=on:random_seed=2446927679:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 113.02/16.23 % (2695520)Instruction limit reached! % 113.02/16.23 % (2695520)------------------------------ % 113.02/16.23 % (2695520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.02/16.23 % (2695520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.02/16.23 % (2695520)CaDiCaL version: 2.1.3 % 113.02/16.23 % (2695520)Termination reason: Instruction limit % 113.02/16.23 % (2695520)Termination phase: Saturation % 113.02/16.23 % (2695520)Time elapsed: 2.323 s % 113.02/16.23 % (2695520)Peak memory usage: 41 MB % 113.02/16.23 % (2695520)Instructions burned: 5133 (million) % 113.02/16.23 % (2695544)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2324871508:fmbsr=1.6:i=67534_2969 on theBenchmark for (2969ds/67534Mi) % 113.02/16.23 % (2695544)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.02/16.23 % (2695544)Terminated due to inappropriate strategy. % 113.02/16.23 % (2695544)------------------------------ % 113.02/16.23 % (2695544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.02/16.23 % (2695544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.02/16.23 % (2695544)CaDiCaL version: 2.1.3 % 113.02/16.23 % (2695544)Termination reason: Inappropriate % 113.02/16.23 % (2695544)Time elapsed: 0.004 s % 113.02/16.23 % (2695544)Peak memory usage: 10 MB % 113.02/16.23 % (2695544)Instructions burned: 8 (million) % 113.02/16.23 % (2695544)------------------------------ % 113.02/16.23 % (2695544)------------------------------ % 113.02/16.23 % (2695546)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3352990775:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2968 on theBenchmark for (2968ds/4591Mi) % 113.02/16.23 % (2695536)Instruction limit reached! % 113.02/16.23 % (2695536)------------------------------ % 113.02/16.23 % (2695536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.02/16.23 % (2695536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.02/16.23 % (2695536)CaDiCaL version: 2.1.3 % 113.02/16.23 % (2695536)Termination reason: Instruction limit % 113.02/16.23 % (2695536)Termination phase: Saturation % 113.02/16.23 % (2695536)Time elapsed: 2.408 s % 113.02/16.23 % (2695536)Peak memory usage: 19 MB % 113.02/16.23 % (2695536)Instructions burned: 3773 (million) % 113.02/16.23 % (2695549)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1618634913:i=29340_2957 on theBenchmark for (2957ds/29340Mi) % 113.02/16.23 % (2695534)Instruction limit reached! % 113.02/16.23 % (2695534)------------------------------ % 113.02/16.23 % (2695534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.02/16.23 % (2695534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.02/16.23 % (2695534)CaDiCaL version: 2.1.3 % 113.02/16.23 % (2695534)Termination reason: Instruction limit % 158.44/22.63 % (2695534)Termination phase: Saturation % 158.44/22.63 % (2695534)Time elapsed: 3.074 s % 158.44/22.63 % (2695534)Peak memory usage: 30 MB % 158.44/22.63 % (2695534)Instructions burned: 3513 (million) % 158.44/22.63 % (2695540)Instruction limit reached! % 158.44/22.63 % (2695540)------------------------------ % 158.44/22.63 % (2695540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.44/22.63 % (2695540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.44/22.63 % (2695540)CaDiCaL version: 2.1.3 % 158.44/22.63 % (2695540)Termination reason: Instruction limit % 158.44/22.63 % (2695540)Termination phase: Saturation % 158.44/22.63 % (2695540)Time elapsed: 2.082 s % 158.44/22.63 % (2695540)Peak memory usage: 28 MB % 158.44/22.63 % (2695540)Instructions burned: 2252 (million) % 158.44/22.63 % (2695551)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=95981518:i=5211_2957 on theBenchmark for (2957ds/5211Mi) % 158.44/22.63 % (2695552)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1036207734:i=5497:nm=2_2956 on theBenchmark for (2956ds/5497Mi) % 158.44/22.63 % (2695552)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.44/22.63 % (2695552)Terminated due to inappropriate strategy. % 158.44/22.63 % (2695552)------------------------------ % 158.44/22.63 % (2695552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.44/22.63 % (2695552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.44/22.63 % (2695552)CaDiCaL version: 2.1.3 % 158.44/22.63 % (2695552)Termination reason: Inappropriate % 158.44/22.63 % (2695552)Time elapsed: 0.009 s % 158.44/22.63 % (2695552)Peak memory usage: 11 MB % 158.44/22.63 % (2695552)Instructions burned: 13 (million) % 158.44/22.63 % (2695552)------------------------------ % 158.44/22.63 % (2695552)------------------------------ % 158.44/22.63 % (2695555)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1336128241:fmbsr=2:i=46332_2956 on theBenchmark for (2956ds/46332Mi) % 158.44/22.63 % (2695555)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.44/22.63 % (2695555)Terminated due to inappropriate strategy. % 158.44/22.63 % (2695555)------------------------------ % 158.44/22.63 % (2695555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.44/22.63 % (2695555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.44/22.63 % (2695555)CaDiCaL version: 2.1.3 % 158.44/22.63 % (2695555)Termination reason: Inappropriate % 158.44/22.63 % (2695555)Time elapsed: 0.005 s % 158.44/22.63 % (2695555)Peak memory usage: 11 MB % 158.44/22.63 % (2695555)Instructions burned: 8 (million) % 158.44/22.63 % (2695555)------------------------------ % 158.44/22.63 % (2695555)------------------------------ % 158.44/22.63 % (2695557)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3019254933:i=14071_2956 on theBenchmark for (2956ds/14071Mi) % 158.44/22.63 % (2695557)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.44/22.63 % (2695557)Terminated due to inappropriate strategy. % 158.44/22.63 % (2695557)------------------------------ % 158.44/22.63 % (2695557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.44/22.63 % (2695557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.44/22.63 % (2695557)CaDiCaL version: 2.1.3 % 158.44/22.63 % (2695557)Termination reason: Inappropriate % 158.44/22.63 % (2695557)Time elapsed: 0.009 s % 158.44/22.63 % (2695557)Peak memory usage: 11 MB % 158.44/22.63 % (2695557)Instructions burned: 8 (million) % 158.44/22.63 % (2695557)------------------------------ % 158.44/22.63 % (2695557)------------------------------ % 158.44/22.63 % (2695559)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3965527261:i=22565:add=on:rawr=on_2955 on theBenchmark for (2955ds/22565Mi) % 158.44/22.63 % (2695530)Instruction limit reached! % 158.44/22.63 % (2695530)------------------------------ % 158.44/22.63 % (2695530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.44/22.63 % (2695530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.44/22.63 % (2695530)CaDiCaL version: 2.1.3 % 158.44/22.63 % (2695530)Termination reason: Instruction limit % 158.44/22.63 % (2695530)Termination phase: Saturation % 158.44/22.63 % (2695530)Time elapsed: 3.699 s % 158.44/22.63 % (2695530)Peak memory usage: 28 MB % 158.44/22.63 % (2695530)Instructions burned: 5114 (million) % 158.44/22.63 % (2695561)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3272803876:i=8173:av=off_2952 on theBenchmark for (2952ds/8173Mi) % 158.44/22.63 % (2695546)Instruction limit reached! % 158.44/22.67 % (2695546)------------------------------ % 158.44/22.67 % (2695546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.44/22.67 % (2695546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.44/22.67 % (2695546)CaDiCaL version: 2.1.3 % 158.44/22.67 % (2695546)Termination reason: Instruction limit % 158.44/22.67 % (2695546)Termination phase: Saturation % 158.44/22.67 % (2695546)Time elapsed: 2.496 s % 158.44/22.67 % (2695546)Peak memory usage: 42 MB % 158.44/22.67 % (2695546)Instructions burned: 4593 (million) % 158.44/22.67 % (2695563)dis+10_16:1_sil=16000:random_seed=2112944187:i=9155:fsr=off_2943 on theBenchmark for (2943ds/9155Mi) % 158.44/22.67 % (2695551)Instruction limit reached! % 158.44/22.67 % (2695551)------------------------------ % 158.44/22.67 % (2695551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.44/22.67 % (2695551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.44/22.67 % (2695551)CaDiCaL version: 2.1.3 % 158.44/22.67 % (2695551)Termination reason: Instruction limit % 158.44/22.67 % (2695551)Termination phase: Saturation % 158.44/22.67 % (2695551)Time elapsed: 4.109 s % 158.44/22.67 % (2695551)Peak memory usage: 37 MB % 158.44/22.67 % (2695551)Instructions burned: 5212 (million) % 158.44/22.67 % (2695565)ott-3_8_sil=64000:random_seed=2019889158:i=20139:bs=on_2915 on theBenchmark for (2915ds/20139Mi) % 158.44/22.67 % (2695563)Instruction limit reached! % 158.44/22.67 % (2695563)------------------------------ % 158.44/22.67 % (2695563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.44/22.67 % (2695563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.44/22.67 % (2695563)CaDiCaL version: 2.1.3 % 158.44/22.67 % (2695563)Termination reason: Instruction limit % 158.44/22.67 % (2695563)Termination phase: Saturation % 158.44/22.67 % (2695563)Time elapsed: 2.976 s % 158.44/22.67 % (2695563)Peak memory usage: 21 MB % 158.44/22.67 % (2695563)Instructions burned: 9156 (million) % 158.44/22.67 % (2695567)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2991178546:fmbsr=2:i=32576_2913 on theBenchmark for (2913ds/32576Mi) % 158.44/22.67 % (2695567)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.44/22.67 % (2695567)Terminated due to inappropriate strategy. % 158.44/22.67 % (2695567)------------------------------ % 158.44/22.67 % (2695567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.44/22.67 % (2695567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.44/22.67 % (2695567)CaDiCaL version: 2.1.3 % 158.44/22.67 % (2695567)Termination reason: Inappropriate % 158.44/22.67 % (2695567)Time elapsed: 0.007 s % 158.44/22.67 % (2695567)Peak memory usage: 11 MB % 158.44/22.67 % (2695567)Instructions burned: 13 (million) % 158.44/22.67 % (2695567)------------------------------ % 158.44/22.67 % (2695567)------------------------------ % 158.44/22.67 % (2695569)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4180449245:i=11404_2912 on theBenchmark for (2912ds/11404Mi) % 158.44/22.67 % (2695561)Instruction limit reached! % 158.44/22.67 % (2695561)------------------------------ % 158.44/22.67 % (2695561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.44/22.67 % (2695561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.44/22.67 % (2695561)CaDiCaL version: 2.1.3 % 158.44/22.67 % (2695561)Termination reason: Instruction limit % 158.44/22.67 % (2695561)Termination phase: Saturation % 158.44/22.67 % (2695561)Time elapsed: 5.764 s % 158.44/22.67 % (2695561)Peak memory usage: 31 MB % 158.44/22.67 % (2695561)Instructions burned: 8173 (million) % 158.44/22.67 % (2695573)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2205684084:i=14134_2894 on theBenchmark for (2894ds/14134Mi) % 158.44/22.67 % (2695569)Instruction limit reached! % 158.44/22.67 % (2695569)------------------------------ % 158.44/22.67 % (2695569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.44/22.67 % (2695569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.44/22.67 % (2695569)CaDiCaL version: 2.1.3 % 158.44/22.67 % (2695569)Termination reason: Instruction limit % 158.44/22.67 % (2695569)Termination phase: Saturation % 158.44/22.67 % (2695569)Time elapsed: 2.943 s % 158.44/22.67 % (2695569)Peak memory usage: 20 MB % 158.44/22.67 % (2695569)Instructions burned: 11406 (million) % 158.44/22.67 % (2695575)dis+33_16_sil=32000:sac=on:random_seed=2521085588:i=15851:nm=0_2883 on theBenchmark for (2883ds/15851Mi) % 158.44/22.67 % (2695575)Instruction limit reached! % 158.44/22.67 % (2695575)------------------------------ % 158.44/22.67 % (2695575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.25/23.37 % (2695575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.25/23.37 % (2695575)CaDiCaL version: 2.1.3 % 163.25/23.37 % (2695575)Termination reason: Instruction limit % 163.25/23.37 % (2695575)Termination phase: Saturation % 163.25/23.37 % (2695575)Time elapsed: 4.196 s % 163.25/23.37 % (2695575)Peak memory usage: 80 MB % 163.25/23.37 % (2695575)Instructions burned: 15855 (million) % 163.25/23.37 % (2695732)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1689297866:avsq=on:i=17627:add=on:amm=off_2840 on theBenchmark for (2840ds/17627Mi) % 163.25/23.37 % (2695565)Instruction limit reached! % 163.25/23.37 % (2695565)------------------------------ % 163.25/23.37 % (2695565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.25/23.37 % (2695565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.25/23.37 % (2695565)CaDiCaL version: 2.1.3 % 163.25/23.37 % (2695565)Termination reason: Instruction limit % 163.25/23.37 % (2695565)Termination phase: Saturation % 163.25/23.37 % (2695565)Time elapsed: 9.783 s % 163.25/23.37 % (2695565)Peak memory usage: 32 MB % 163.25/23.37 % (2695565)Instructions burned: 20141 (million) % 163.25/23.37 % (2695734)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2095326279:s2a=on:i=53295_2817 on theBenchmark for (2817ds/53295Mi) % 163.25/23.37 % (2695573)Instruction limit reached! % 163.25/23.37 % (2695573)------------------------------ % 163.25/23.37 % (2695573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.25/23.37 % (2695573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.25/23.37 % (2695573)CaDiCaL version: 2.1.3 % 163.25/23.37 % (2695573)Termination reason: Instruction limit % 163.25/23.37 % (2695573)Termination phase: Saturation % 163.25/23.37 % (2695573)Time elapsed: 7.940 s % 163.25/23.37 % (2695573)Peak memory usage: 66 MB % 163.25/23.37 % (2695573)Instructions burned: 14136 (million) % 163.25/23.37 % (2695736)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=626163161:i=26857:ins=20_2814 on theBenchmark for (2814ds/26857Mi) % 163.25/23.37 % (2695736)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 163.25/23.37 % (2695736)Terminated due to inappropriate strategy. % 163.25/23.37 % (2695736)------------------------------ % 163.25/23.37 % (2695736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.25/23.37 % (2695736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.25/23.37 % (2695736)CaDiCaL version: 2.1.3 % 163.25/23.37 % (2695736)Termination reason: Inappropriate % 163.25/23.37 % (2695736)Time elapsed: 0.004 s % 163.25/23.37 % (2695736)Peak memory usage: 10 MB % 163.25/23.37 % (2695736)Instructions burned: 8 (million) % 163.25/23.37 % (2695736)------------------------------ % 163.25/23.37 % (2695736)------------------------------ % 163.25/23.37 % (2695738)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1550902597:i=28120:bs=on:fsr=off_2813 on theBenchmark for (2813ds/28120Mi) % 163.25/23.37 % (2695559)Instruction limit reached! % 163.25/23.37 % (2695559)------------------------------ % 163.25/23.37 % (2695559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.25/23.37 % (2695559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.25/23.37 % (2695559)CaDiCaL version: 2.1.3 % 163.25/23.37 % (2695559)Termination reason: Instruction limit % 163.25/23.37 % (2695559)Termination phase: Saturation % 163.25/23.37 % (2695559)Time elapsed: 17.775 s % 163.25/23.37 % (2695559)Peak memory usage: 115 MB % 163.25/23.37 % (2695559)Instructions burned: 22566 (million) % 163.25/23.37 % (2695740)fmb+10_1_sil=256000:fmbss=7:random_seed=1363780327:fmbsr=1.6:i=182295_2777 on theBenchmark for (2777ds/182295Mi) % 163.25/23.37 % (2695740)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 163.25/23.37 % (2695740)Terminated due to inappropriate strategy. % 163.25/23.37 % (2695740)------------------------------ % 163.25/23.37 % (2695740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 163.25/23.37 % (2695740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.25/23.37 % (2695740)CaDiCaL version: 2.1.3 % 163.25/23.37 % (2695740)Termination reason: Inappropriate % 163.25/23.37 % (2695740)Time elapsed: 0.004 s % 163.25/23.37 % (2695740)Peak memory usage: 10 MB % 163.25/23.37 % (2695740)Instructions burned: 8 (million) % 163.25/23.37 % (2695740)------------------------------ % 163.25/23.37 % (2695740)------------------------------ % 163.25/23.37 % (2695742)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2624631031:i=44625:gsp=on_2777 on theBenchmark for (2777ds/44625Mi) % 176.43/25.20 % (2695732)Instruction limit reached! % 176.43/25.20 % (2695732)------------------------------ % 176.43/25.20 % (2695732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.43/25.20 % (2695732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.43/25.20 % (2695732)CaDiCaL version: 2.1.3 % 176.43/25.20 % (2695732)Termination reason: Instruction limit % 176.43/25.20 % (2695732)Termination phase: Saturation % 176.43/25.20 % (2695732)Time elapsed: 6.383 s % 176.43/25.20 % (2695732)Peak memory usage: 106 MB % 176.43/25.20 % (2695732)Instructions burned: 17627 (million) % 176.43/25.20 % (2695742)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.43/25.20 % (2695742)Terminated due to inappropriate strategy. % 176.43/25.20 % (2695742)------------------------------ % 176.43/25.20 % (2695742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.43/25.20 % (2695742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.43/25.20 % (2695742)CaDiCaL version: 2.1.3 % 176.43/25.20 % (2695742)Termination reason: Inappropriate % 176.43/25.20 % (2695742)Time elapsed: 0.005 s % 176.43/25.20 % (2695742)Peak memory usage: 11 MB % 176.43/25.20 % (2695742)Instructions burned: 10 (million) % 176.43/25.20 % (2695742)------------------------------ % 176.43/25.20 % (2695742)------------------------------ % 176.43/25.20 % (2695549)Instruction limit reached! % 176.43/25.20 % (2695549)------------------------------ % 176.43/25.20 % (2695549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.43/25.20 % (2695549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.43/25.20 % (2695549)CaDiCaL version: 2.1.3 % 176.43/25.20 % (2695549)Termination reason: Instruction limit % 176.43/25.20 % (2695549)Termination phase: Saturation % 176.43/25.20 % (2695549)Time elapsed: 18.090 s % 176.43/25.20 % (2695549)Peak memory usage: 59 MB % 176.43/25.20 % (2695549)Instructions burned: 29341 (million) % 176.43/25.20 % (2695745)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2961084004:fmbsr=1.3:i=225729_2776 on theBenchmark for (2776ds/225729Mi) % 176.43/25.20 % (2695744)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1674407298:i=160505_2776 on theBenchmark for (2776ds/160505Mi) % 176.43/25.20 % (2695745)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.43/25.20 % (2695745)Terminated due to inappropriate strategy. % 176.43/25.20 % (2695745)------------------------------ % 176.43/25.20 % (2695745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.43/25.20 % (2695745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.43/25.20 % (2695745)CaDiCaL version: 2.1.3 % 176.43/25.20 % (2695745)Termination reason: Inappropriate % 176.43/25.20 % (2695745)Time elapsed: 0.002 s % 176.43/25.20 % (2695745)Peak memory usage: 11 MB % 176.43/25.20 % (2695745)Instructions burned: 8 (million) % 176.43/25.20 % (2695745)------------------------------ % 176.43/25.20 % (2695745)------------------------------ % 176.43/25.20 % (2695744)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.43/25.20 % (2695744)Terminated due to inappropriate strategy. % 176.43/25.20 % (2695744)------------------------------ % 176.43/25.20 % (2695744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.43/25.20 % (2695744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.43/25.20 % (2695744)CaDiCaL version: 2.1.3 % 176.43/25.20 % (2695744)Termination reason: Inappropriate % 176.43/25.20 % (2695744)Time elapsed: 0.004 s % 176.43/25.20 % (2695744)Peak memory usage: 10 MB % 176.43/25.20 % (2695744)Instructions burned: 8 (million) % 176.43/25.20 % (2695744)------------------------------ % 176.43/25.20 % (2695744)------------------------------ % 176.43/25.20 % (2695749)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1493773236:rtra=on_2776 on theBenchmark for (2776ds/0Mi) % 176.43/25.20 % (2695749)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.43/25.20 % (2695749)Terminated due to inappropriate strategy. % 176.43/25.20 % (2695749)------------------------------ % 176.43/25.20 % (2695749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.43/25.20 % (2695749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.43/25.20 % (2695749)CaDiCaL version: 2.1.3 % 176.43/25.20 % (2695749)Termination reason: Inappropriate % 176.43/25.20 % (2695749)Time elapsed: 0.003 s % 176.43/25.20 % (2695749)Peak memory usage: 11 MB % 176.43/25.20 % (2695749)Instructions burned: 12 (million) % 176.43/25.20 % (2695749)------------------------------ % 195.34/27.86 % (2695749)------------------------------ % 195.34/27.86 % (2695747)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1340823505:fmbsr=2:i=185024:ins=7_2776 on theBenchmark for (2776ds/185024Mi) % 195.34/27.86 % (2695750)% WARNING: option uhcvi not known. % 195.34/27.86 % (2695747)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 195.34/27.86 % (2695747)Terminated due to inappropriate strategy. % 195.34/27.86 % (2695747)------------------------------ % 195.34/27.86 % (2695747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.34/27.86 % (2695747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.34/27.86 % (2695747)CaDiCaL version: 2.1.3 % 195.34/27.86 % (2695747)Termination reason: Inappropriate % 195.34/27.86 % (2695747)Time elapsed: 0.004 s % 195.34/27.86 % (2695747)Peak memory usage: 11 MB % 195.34/27.86 % (2695747)Instructions burned: 8 (million) % 195.34/27.86 % (2695747)------------------------------ % 195.34/27.86 % (2695747)------------------------------ % 195.34/27.86 % (2695750)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1800864656:i=271062:add=off:rtra=on:rawr=on_2776 on theBenchmark for (2776ds/271062Mi) % 195.34/27.86 % (2695752)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1259867149:i=176048:add=on:rtra=on:rawr=on_2776 on theBenchmark for (2776ds/176048Mi) % 195.34/27.86 % (2695754)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2391485837:i=206:fgj=on:rtra=on_2776 on theBenchmark for (2776ds/206Mi) % 195.34/27.86 % (2695754)Instruction limit reached! % 195.34/27.86 % (2695754)------------------------------ % 195.34/27.86 % (2695754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.34/27.86 % (2695754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.34/27.86 % (2695754)CaDiCaL version: 2.1.3 % 195.34/27.86 % (2695754)Termination reason: Instruction limit % 195.34/27.86 % (2695754)Termination phase: Saturation % 195.34/27.86 % (2695754)Time elapsed: 0.116 s % 195.34/27.86 % (2695754)Peak memory usage: 14 MB % 195.34/27.86 % (2695754)Instructions burned: 208 (million) % 195.34/27.86 % (2695758)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=245831774:i=232:rtra=on_2774 on theBenchmark for (2774ds/232Mi) % 195.34/27.86 % (2695758)Instruction limit reached! % 195.34/27.86 % (2695758)------------------------------ % 195.34/27.86 % (2695758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.34/27.86 % (2695758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.34/27.86 % (2695758)CaDiCaL version: 2.1.3 % 195.34/27.86 % (2695758)Termination reason: Instruction limit % 195.34/27.86 % (2695758)Termination phase: Saturation % 195.34/27.86 % (2695758)Time elapsed: 0.129 s % 195.34/27.86 % (2695758)Peak memory usage: 14 MB % 195.34/27.86 % (2695758)Instructions burned: 233 (million) % 195.34/27.86 % (2695760)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3871629368:i=262:rtra=on_2773 on theBenchmark for (2773ds/262Mi) % 195.34/27.86 % (2695760)Instruction limit reached! % 195.34/27.86 % (2695760)------------------------------ % 195.34/27.86 % (2695760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.34/27.86 % (2695760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.34/27.86 % (2695760)CaDiCaL version: 2.1.3 % 195.34/27.86 % (2695760)Termination reason: Instruction limit % 195.34/27.86 % (2695760)Termination phase: Saturation % 195.34/27.86 % (2695760)Time elapsed: 0.144 s % 195.34/27.86 % (2695760)Peak memory usage: 14 MB % 195.34/27.86 % (2695760)Instructions burned: 262 (million) % 195.34/27.86 % (2695762)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2717033283:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2771 on theBenchmark for (2771ds/318Mi) % 195.34/27.86 % (2695762)Instruction limit reached! % 195.34/27.86 % (2695762)------------------------------ % 195.34/27.86 % (2695762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.34/27.86 % (2695762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.34/27.86 % (2695762)CaDiCaL version: 2.1.3 % 195.34/27.86 % (2695762)Termination reason: Instruction limit % 195.34/27.86 % (2695762)Termination phase: Saturation % 195.34/27.86 % (2695762)Time elapsed: 0.195 s % 195.34/27.86 % (2695762)Peak memory usage: 16 MB % 195.34/27.86 % (2695762)Instructions burned: 319 (million) % 195.34/27.86 % (2695764)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1087725468:i=1428:nm=2:rtra=on_2769 on theBenchmark for (2769ds/1428Mi) % 233.29/33.15 % (2695764)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 233.29/33.15 % (2695764)Terminated due to inappropriate strategy. % 233.29/33.15 % (2695764)------------------------------ % 233.29/33.15 % (2695764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.29/33.15 % (2695764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.29/33.15 % (2695764)CaDiCaL version: 2.1.3 % 233.29/33.15 % (2695764)Termination reason: Inappropriate % 233.29/33.15 % (2695764)Time elapsed: 0.005 s % 233.29/33.15 % (2695764)Peak memory usage: 10 MB % 233.29/33.15 % (2695764)Instructions burned: 9 (million) % 233.29/33.15 % (2695764)------------------------------ % 233.29/33.15 % (2695764)------------------------------ % 233.29/33.15 % (2695766)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3645646502:i=262:bd=preordered:rtra=on:fsd=on_2769 on theBenchmark for (2769ds/262Mi) % 233.29/33.15 % (2695766)Instruction limit reached! % 233.29/33.15 % (2695766)------------------------------ % 233.29/33.15 % (2695766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.29/33.15 % (2695766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.29/33.15 % (2695766)CaDiCaL version: 2.1.3 % 233.29/33.15 % (2695766)Termination reason: Instruction limit % 233.29/33.15 % (2695766)Termination phase: Saturation % 233.29/33.15 % (2695766)Time elapsed: 0.139 s % 233.29/33.15 % (2695766)Peak memory usage: 13 MB % 233.29/33.15 % (2695766)Instructions burned: 263 (million) % 233.29/33.15 % (2695768)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=2470736979:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2767 on theBenchmark for (2767ds/1368Mi) % 233.29/33.15 % (2695768)Instruction limit reached! % 233.29/33.15 % (2695768)------------------------------ % 233.29/33.15 % (2695768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.29/33.15 % (2695768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.29/33.15 % (2695768)CaDiCaL version: 2.1.3 % 233.29/33.15 % (2695768)Termination reason: Instruction limit % 233.29/33.15 % (2695768)Termination phase: Saturation % 233.29/33.15 % (2695768)Time elapsed: 0.742 s % 233.29/33.15 % (2695768)Peak memory usage: 20 MB % 233.29/33.15 % (2695768)Instructions burned: 1370 (million) % 233.29/33.15 % (2695770)ott-21_1_sil=16000:si=on:fs=off:random_seed=1160542915:i=360:av=off:fsr=off:rtra=on_2760 on theBenchmark for (2760ds/360Mi) % 233.29/33.15 % (2695770)Instruction limit reached! % 233.29/33.15 % (2695770)------------------------------ % 233.29/33.15 % (2695770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.29/33.15 % (2695770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.29/33.15 % (2695770)CaDiCaL version: 2.1.3 % 233.29/33.15 % (2695770)Termination reason: Instruction limit % 233.29/33.15 % (2695770)Termination phase: Saturation % 233.29/33.15 % (2695770)Time elapsed: 0.165 s % 233.29/33.15 % (2695770)Peak memory usage: 13 MB % 233.29/33.15 % (2695770)Instructions burned: 361 (million) % 233.29/33.15 % (2695772)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=917814955:i=954:bd=all:rtra=on_2758 on theBenchmark for (2758ds/954Mi) % 233.29/33.15 % (2695772)Instruction limit reached! % 233.29/33.15 % (2695772)------------------------------ % 233.29/33.15 % (2695772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.29/33.15 % (2695772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.29/33.15 % (2695772)CaDiCaL version: 2.1.3 % 233.29/33.15 % (2695772)Termination reason: Instruction limit % 233.29/33.15 % (2695772)Termination phase: Saturation % 233.29/33.15 % (2695772)Time elapsed: 0.653 s % 233.29/33.15 % (2695772)Peak memory usage: 17 MB % 233.29/33.15 % (2695772)Instructions burned: 954 (million) % 233.29/33.15 % (2695774)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1571717527:fmbsr=1.3:i=1730:ins=25:rtra=on_2751 on theBenchmark for (2751ds/1730Mi) % 233.29/33.15 % (2695774)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 233.29/33.15 % (2695774)Terminated due to inappropriate strategy. % 233.29/33.15 % (2695774)------------------------------ % 233.29/33.15 % (2695774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.29/33.15 % (2695774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.29/33.15 % (2695774)CaDiCaL version: 2.1.3 % 233.29/33.15 % (2695774)Termination reason: Inappropriate % 267.10/37.94 % (2695774)Time elapsed: 0.004 s % 267.10/37.94 % (2695774)Peak memory usage: 10 MB % 267.10/37.94 % (2695774)Instructions burned: 6 (million) % 267.10/37.94 % (2695774)------------------------------ % 267.10/37.94 % (2695774)------------------------------ % 267.10/37.94 % (2695776)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=413242175:i=2358:rtra=on_2751 on theBenchmark for (2751ds/2358Mi) % 267.10/37.94 % (2695776)Instruction limit reached! % 267.10/37.94 % (2695776)------------------------------ % 267.10/37.94 % (2695776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.10/37.94 % (2695776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.10/37.94 % (2695776)CaDiCaL version: 2.1.3 % 267.10/37.94 % (2695776)Termination reason: Instruction limit % 267.10/37.94 % (2695776)Termination phase: Saturation % 267.10/37.94 % (2695776)Time elapsed: 0.878 s % 267.10/37.94 % (2695776)Peak memory usage: 15 MB % 267.10/37.94 % (2695776)Instructions burned: 2358 (million) % 267.10/37.94 % (2695778)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2035943811:i=1778:ins=1:rtra=on_2742 on theBenchmark for (2742ds/1778Mi) % 267.10/37.94 % (2695778)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 267.10/37.94 % (2695778)Terminated due to inappropriate strategy. % 267.10/37.94 % (2695778)------------------------------ % 267.10/37.94 % (2695778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.10/37.94 % (2695778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.10/37.94 % (2695778)CaDiCaL version: 2.1.3 % 267.10/37.94 % (2695778)Termination reason: Inappropriate % 267.10/37.94 % (2695778)Time elapsed: 0.005 s % 267.10/37.94 % (2695778)Peak memory usage: 10 MB % 267.10/37.94 % (2695778)Instructions burned: 8 (million) % 267.10/37.94 % (2695778)------------------------------ % 267.10/37.94 % (2695778)------------------------------ % 267.10/37.94 % (2695780)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=4061316974:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2741 on theBenchmark for (2741ds/1384Mi) % 267.10/37.94 % (2695780)Instruction limit reached! % 267.10/37.94 % (2695780)------------------------------ % 267.10/37.94 % (2695780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.10/37.94 % (2695780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.10/37.94 % (2695780)CaDiCaL version: 2.1.3 % 267.10/37.94 % (2695780)Termination reason: Instruction limit % 267.10/37.94 % (2695780)Termination phase: Saturation % 267.10/37.94 % (2695780)Time elapsed: 0.750 s % 267.10/37.94 % (2695780)Peak memory usage: 22 MB % 267.10/37.94 % (2695780)Instructions burned: 1384 (million) % 267.10/37.94 % (2695782)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2289081532:i=1758:kws=inv_precedence:fsr=off:rtra=on_2734 on theBenchmark for (2734ds/1758Mi) % 267.10/37.94 % (2695782)Instruction limit reached! % 267.10/37.94 % (2695782)------------------------------ % 267.10/37.94 % (2695782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.10/37.94 % (2695782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.10/37.94 % (2695782)CaDiCaL version: 2.1.3 % 267.10/37.94 % (2695782)Termination reason: Instruction limit % 267.10/37.94 % (2695782)Termination phase: Saturation % 267.10/37.94 % (2695782)Time elapsed: 0.879 s % 267.10/37.94 % (2695782)Peak memory usage: 22 MB % 267.10/37.94 % (2695782)Instructions burned: 1760 (million) % 267.10/37.94 % (2695784)fmb+10_1_sil=64000:si=on:random_seed=3974486370:i=44122:nm=2:rtra=on:gsp=on_2725 on theBenchmark for (2725ds/44122Mi) % 267.10/37.94 % (2695784)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 267.10/37.94 % (2695784)Terminated due to inappropriate strategy. % 267.10/37.94 % (2695784)------------------------------ % 267.10/37.94 % (2695784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 267.10/37.94 % (2695784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.10/37.94 % (2695784)CaDiCaL version: 2.1.3 % 267.10/37.94 % (2695784)Termination reason: Inappropriate % 267.10/37.94 % (2695784)Time elapsed: 0.006 s % 267.10/37.94 % (2695784)Peak memory usage: 10 MB % 267.10/37.94 % (2695784)Instructions burned: 10 (million) % 267.10/37.94 % (2695784)------------------------------ % 267.10/37.94 % (2695784)------------------------------ % 267.10/37.94 % (2695786)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=795771734:i=19030:nm=5:rtra=on_2724 on theBenchmark for (2724ds/19030Mi) % 300.50/42.64 % (2695786)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.50/42.64 % (2695786)Terminated due to inappropriate strategy. % 300.50/42.64 % (2695786)------------------------------ % 300.50/42.64 % (2695786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.64 % (2695786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.64 % (2695786)CaDiCaL version: 2.1.3 % 300.50/42.64 % (2695786)Termination reason: Inappropriate % 300.50/42.64 % (2695786)Time elapsed: 0.005 s % 300.50/42.64 % (2695786)Peak memory usage: 10 MB % 300.50/42.64 % (2695786)Instructions burned: 9 (million) % 300.50/42.64 % (2695786)------------------------------ % 300.50/42.64 % (2695786)------------------------------ % 300.50/42.64 % (2695788)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1883514345:fmbsr=1.7:i=1840:rtra=on_2724 on theBenchmark for (2724ds/1840Mi) % 300.50/42.64 % (2695788)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.50/42.64 % (2695788)Terminated due to inappropriate strategy. % 300.50/42.64 % (2695788)------------------------------ % 300.50/42.64 % (2695788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.64 % (2695788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.64 % (2695788)CaDiCaL version: 2.1.3 % 300.50/42.64 % (2695788)Termination reason: Inappropriate % 300.50/42.64 % (2695788)Time elapsed: 0.005 s % 300.50/42.64 % (2695788)Peak memory usage: 10 MB % 300.50/42.64 % (2695788)Instructions burned: 9 (million) % 300.50/42.64 % (2695788)------------------------------ % 300.50/42.64 % (2695788)------------------------------ % 300.50/42.64 % (2695790)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=246321083:i=10262:rtra=on_2724 on theBenchmark for (2724ds/10262Mi) % 300.50/42.64 % (2695738)Instruction limit reached! % 300.50/42.64 % (2695738)------------------------------ % 300.50/42.64 % (2695738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.64 % (2695738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.64 % (2695738)CaDiCaL version: 2.1.3 % 300.50/42.64 % (2695738)Termination reason: Instruction limit % 300.50/42.64 % (2695738)Termination phase: Saturation % 300.50/42.64 % (2695738)Time elapsed: 11.451 s % 300.50/42.64 % (2695738)Peak memory usage: 34 MB % 300.50/42.64 % (2695738)Instructions burned: 28120 (million) % 300.50/42.64 % (2696067)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=985054208:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2699 on theBenchmark for (2699ds/2944Mi) % 300.50/42.64 % (2696067)Instruction limit reached! % 300.50/42.64 % (2696067)------------------------------ % 300.50/42.64 % (2696067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.64 % (2696067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.64 % (2696067)CaDiCaL version: 2.1.3 % 300.50/42.64 % (2696067)Termination reason: Instruction limit % 300.50/42.64 % (2696067)Termination phase: Saturation % 300.50/42.64 % (2696067)Time elapsed: 2.639 s % 300.50/42.64 % (2696067)Peak memory usage: 41 MB % 300.50/42.64 % (2696067)Instructions burned: 2945 (million) % 300.50/42.64 % (2696199)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1514031272:i=12648:rtra=on_2672 on theBenchmark for (2672ds/12648Mi) % 300.50/42.64 % (2696199)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.50/42.64 % (2696199)Terminated due to inappropriate strategy. % 300.50/42.64 % (2696199)------------------------------ % 300.50/42.64 % (2696199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.50/42.64 % (2696199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/42.64 % (2696199)CaDiCaL version: 2.1.3 % 300.50/42.64 % (2696199)Termination reason: Inappropriate % 300.50/42.64 % (2696199)Time elapsed: 0.007 s % 300.50/42.64 % (2696199)Peak memory usage: 11 MB % 300.50/42.64 % (2696199)Instructions burned: 13 (million) % 300.50/42.64 % (2696199)------------------------------ % 300.50/42.64 % (2696199)------------------------------ % 300.50/42.64 % (2696209)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1296083057:fmbsr=2.30978:i=4348:rtra=on_2671 on theBenchmark for (2671ds/4348Mi) % 300.50/42.64 % (2696209)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.50/42.64 % (2696209)Terminated due to inappropriate strategy. % 300.50/42.64 % (2696209)------------------------------ % 300.50/42.64 % (269620 % 300.50/42.64 Terminated % 300.50/42.64 % Vampire exiting % 300.50/42.64 Terminated %------------------------------------------------------------------------------