%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW651_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n017.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:35 PM UTC 2026 % Result : Timeout 300.25s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW651_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 % Computer : n017.cluster.edu % 0.09/0.22 % Model : x86_64 x86_64 % 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.22 % Memory : 8046.5625MB % 0.09/0.22 % OS : Linux 6.8.0-71-generic % 0.09/0.22 % CPULimit : 300 % 0.09/0.22 % WCLimit : 300 % 0.09/0.22 % DateTime : Mon Sep 28 14:19:21 UTC 2026 % 0.09/0.22 % CPUTime : % 0.09/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.26 Running first-order model finding % 0.09/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 % 6.42/1.22 % (3587688)Will run a generic schedule for satisfiability detection. % 6.42/1.22 % (3587695)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3443510321:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.42/1.22 % (3587694)% WARNING: option uhcvi not known. % 6.42/1.22 % (3587693)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1498767118_2999 on theBenchmark for (2999ds/0Mi) % 6.42/1.22 % (3587694)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2444325683:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.42/1.22 % (3587696)dis+10_1_sil=32000:sp=arity:random_seed=236060036:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.42/1.22 % (3587697)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2227376911:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.42/1.22 % (3587698)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2368520317:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.42/1.22 % (3587699)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2359243112:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.42/1.23 % (3587693)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.42/1.23 % (3587693)Terminated due to inappropriate strategy. % 6.42/1.23 % (3587693)------------------------------ % 6.42/1.23 % (3587693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.42/1.23 % (3587693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.42/1.23 % (3587693)CaDiCaL version: 2.1.3 % 6.42/1.23 % (3587693)Termination reason: Inappropriate % 6.42/1.23 % (3587693)Time elapsed: 0.007 s % 6.42/1.23 % (3587693)Peak memory usage: 10 MB % 6.42/1.23 % (3587693)Instructions burned: 7 (million) % 6.42/1.23 % (3587693)------------------------------ % 6.42/1.23 % (3587693)------------------------------ % 6.42/1.23 % (3587707)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1091269779:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.42/1.23 % (3587707)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.42/1.23 % (3587707)Terminated due to inappropriate strategy. % 6.42/1.23 % (3587707)------------------------------ % 6.42/1.23 % (3587707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.42/1.23 % (3587707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.42/1.23 % (3587707)CaDiCaL version: 2.1.3 % 6.42/1.23 % (3587707)Termination reason: Inappropriate % 6.42/1.23 % (3587707)Time elapsed: 0.004 s % 6.42/1.23 % (3587707)Peak memory usage: 10 MB % 6.42/1.23 % (3587707)Instructions burned: 7 (million) % 6.42/1.23 % (3587707)------------------------------ % 6.42/1.23 % (3587707)------------------------------ % 6.42/1.23 % (3587709)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=28021279:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.42/1.23 % (3587696)Instruction limit reached! % 6.42/1.23 % (3587696)------------------------------ % 6.42/1.23 % (3587696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.42/1.23 % (3587696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.42/1.23 % (3587696)CaDiCaL version: 2.1.3 % 6.42/1.23 % (3587696)Termination reason: Instruction limit % 6.42/1.23 % (3587696)Termination phase: Saturation % 6.42/1.23 % (3587696)Time elapsed: 0.107 s % 6.42/1.23 % (3587696)Peak memory usage: 13 MB % 6.42/1.23 % (3587696)Instructions burned: 104 (million) % 6.42/1.23 % (3587697)Instruction limit reached! % 6.42/1.23 % (3587697)------------------------------ % 6.42/1.23 % (3587697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.42/1.23 % (3587697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.42/1.23 % (3587697)CaDiCaL version: 2.1.3 % 6.42/1.23 % (3587697)Termination reason: Instruction limit % 6.42/1.23 % (3587697)Termination phase: Saturation % 6.42/1.23 % (3587697)Time elapsed: 0.122 s % 6.42/1.23 % (3587697)Peak memory usage: 13 MB % 6.42/1.23 % (3587697)Instructions burned: 116 (million) % 6.42/1.23 % (3587711)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=3956802381:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.42/1.23 % (3587698)Instruction limit reached! % 6.42/1.23 % (3587698)------------------------------ % 6.42/1.23 % (3587698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.04/1.69 % (3587698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.04/1.69 % (3587698)CaDiCaL version: 2.1.3 % 8.04/1.69 % (3587698)Termination reason: Instruction limit % 8.04/1.69 % (3587698)Termination phase: Saturation % 8.04/1.69 % (3587698)Time elapsed: 0.132 s % 8.04/1.69 % (3587698)Peak memory usage: 13 MB % 8.04/1.69 % (3587698)Instructions burned: 131 (million) % 8.04/1.69 % (3587712)ott-21_1_sil=16000:fs=off:random_seed=4006075722:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.04/1.69 % (3587699)Instruction limit reached! % 8.04/1.69 % (3587699)------------------------------ % 8.04/1.69 % (3587699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.04/1.69 % (3587699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.04/1.69 % (3587699)CaDiCaL version: 2.1.3 % 8.04/1.69 % (3587699)Termination reason: Instruction limit % 8.04/1.69 % (3587699)Termination phase: Saturation % 8.04/1.69 % (3587699)Time elapsed: 0.157 s % 8.04/1.69 % (3587699)Peak memory usage: 13 MB % 8.04/1.69 % (3587699)Instructions burned: 159 (million) % 8.04/1.69 % (3587714)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1496599121:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.04/1.69 % (3587716)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2966175893:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 8.04/1.69 % (3587716)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.04/1.69 % (3587716)Terminated due to inappropriate strategy. % 8.04/1.69 % (3587716)------------------------------ % 8.04/1.69 % (3587716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.04/1.69 % (3587716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.04/1.69 % (3587716)CaDiCaL version: 2.1.3 % 8.04/1.69 % (3587716)Termination reason: Inappropriate % 8.04/1.69 % (3587716)Time elapsed: 0.003 s % 8.04/1.69 % (3587716)Peak memory usage: 10 MB % 8.04/1.69 % (3587716)Instructions burned: 5 (million) % 8.04/1.69 % (3587716)------------------------------ % 8.04/1.69 % (3587716)------------------------------ % 8.04/1.69 % (3587719)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=308643255:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 8.04/1.70 % (3587709)Instruction limit reached! % 8.04/1.70 % (3587709)------------------------------ % 8.04/1.70 % (3587709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.04/1.70 % (3587709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.04/1.70 % (3587709)CaDiCaL version: 2.1.3 % 8.04/1.70 % (3587709)Termination reason: Instruction limit % 8.04/1.70 % (3587709)Termination phase: Saturation % 8.04/1.70 % (3587709)Time elapsed: 0.145 s % 8.04/1.70 % (3587709)Peak memory usage: 13 MB % 8.04/1.70 % (3587709)Instructions burned: 131 (million) % 8.04/1.70 % (3587721)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=153374232:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 8.04/1.70 % (3587721)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 8.04/1.70 % (3587721)Terminated due to inappropriate strategy. % 8.04/1.70 % (3587721)------------------------------ % 8.04/1.70 % (3587721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.04/1.70 % (3587721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.04/1.70 % (3587721)CaDiCaL version: 2.1.3 % 8.04/1.70 % (3587721)Termination reason: Inappropriate % 8.04/1.70 % (3587721)Time elapsed: 0.007 s % 8.04/1.70 % (3587721)Peak memory usage: 10 MB % 8.04/1.70 % (3587721)Instructions burned: 6 (million) % 8.04/1.70 % (3587721)------------------------------ % 8.04/1.70 % (3587721)------------------------------ % 8.04/1.70 % (3587723)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=2842008738:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 8.04/1.70 % (3587712)Instruction limit reached! % 8.04/1.70 % (3587712)------------------------------ % 8.04/1.70 % (3587712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.04/1.70 % (3587712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.04/1.70 % (3587712)CaDiCaL version: 2.1.3 % 8.04/1.70 % (3587712)Termination reason: Instruction limit % 8.04/1.70 % (3587712)Termination phase: Saturation % 33.94/5.07 % (3587712)Time elapsed: 0.164 s % 33.94/5.07 % (3587712)Peak memory usage: 13 MB % 33.94/5.07 % (3587712)Instructions burned: 181 (million) % 33.94/5.07 % (3587725)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=614081596:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 33.94/5.07 % (3587714)Instruction limit reached! % 33.94/5.07 % (3587714)------------------------------ % 33.94/5.07 % (3587714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.94/5.07 % (3587714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.94/5.07 % (3587714)CaDiCaL version: 2.1.3 % 33.94/5.07 % (3587714)Termination reason: Instruction limit % 33.94/5.07 % (3587714)Termination phase: Saturation % 33.94/5.07 % (3587714)Time elapsed: 0.499 s % 33.94/5.07 % (3587714)Peak memory usage: 14 MB % 33.94/5.07 % (3587714)Instructions burned: 478 (million) % 33.94/5.07 % (3587727)fmb+10_1_sil=64000:random_seed=2209194049:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 33.94/5.07 % (3587727)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 33.94/5.07 % (3587727)Terminated due to inappropriate strategy. % 33.94/5.07 % (3587727)------------------------------ % 33.94/5.07 % (3587727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.94/5.07 % (3587727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.94/5.07 % (3587727)CaDiCaL version: 2.1.3 % 33.94/5.07 % (3587727)Termination reason: Inappropriate % 33.94/5.07 % (3587727)Time elapsed: 0.004 s % 33.94/5.07 % (3587727)Peak memory usage: 10 MB % 33.94/5.07 % (3587727)Instructions burned: 7 (million) % 33.94/5.07 % (3587727)------------------------------ % 33.94/5.07 % (3587727)------------------------------ % 33.94/5.07 % (3587729)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2581704548:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 33.94/5.07 % (3587729)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 33.94/5.07 % (3587729)Terminated due to inappropriate strategy. % 33.94/5.07 % (3587729)------------------------------ % 33.94/5.07 % (3587729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.94/5.07 % (3587729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.94/5.07 % (3587729)CaDiCaL version: 2.1.3 % 33.94/5.07 % (3587729)Termination reason: Inappropriate % 33.94/5.07 % (3587729)Time elapsed: 0.004 s % 33.94/5.07 % (3587729)Peak memory usage: 10 MB % 33.94/5.07 % (3587729)Instructions burned: 6 (million) % 33.94/5.07 % (3587729)------------------------------ % 33.94/5.07 % (3587729)------------------------------ % 33.94/5.07 % (3587731)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2353463615:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 33.94/5.07 % (3587731)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 33.94/5.07 % (3587731)Terminated due to inappropriate strategy. % 33.94/5.07 % (3587731)------------------------------ % 33.94/5.07 % (3587731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.94/5.07 % (3587731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.94/5.07 % (3587731)CaDiCaL version: 2.1.3 % 33.94/5.07 % (3587731)Termination reason: Inappropriate % 33.94/5.07 % (3587731)Time elapsed: 0.004 s % 33.94/5.07 % (3587731)Peak memory usage: 10 MB % 33.94/5.07 % (3587731)Instructions burned: 6 (million) % 33.94/5.07 % (3587731)------------------------------ % 33.94/5.07 % (3587731)------------------------------ % 33.94/5.07 % (3587735)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1971242842:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 33.94/5.07 % (3587711)Instruction limit reached! % 33.94/5.07 % (3587711)------------------------------ % 33.94/5.07 % (3587711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.94/5.07 % (3587711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.94/5.07 % (3587711)CaDiCaL version: 2.1.3 % 33.94/5.07 % (3587711)Termination reason: Instruction limit % 33.94/5.07 % (3587711)Termination phase: Saturation % 33.94/5.07 % (3587711)Time elapsed: 0.651 s % 33.94/5.07 % (3587711)Peak memory usage: 17 MB % 33.94/5.07 % (3587711)Instructions burned: 684 (million) % 33.94/5.07 % (3587737)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1442925924:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 33.94/5.07 % (3587723)Instruction limit reached! % 33.94/5.07 % (3587723)------------------------------ % 44.57/6.63 % (3587723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.57/6.63 % (3587723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.57/6.63 % (3587723)CaDiCaL version: 2.1.3 % 44.57/6.63 % (3587723)Termination reason: Instruction limit % 44.57/6.63 % (3587723)Termination phase: Saturation % 44.57/6.63 % (3587723)Time elapsed: 0.613 s % 44.57/6.63 % (3587723)Peak memory usage: 15 MB % 44.57/6.63 % (3587723)Instructions burned: 692 (million) % 44.57/6.63 % (3587739)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2151258456:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 44.57/6.63 % (3587739)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 44.57/6.63 % (3587739)Terminated due to inappropriate strategy. % 44.57/6.63 % (3587739)------------------------------ % 44.57/6.63 % (3587739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.57/6.63 % (3587739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.57/6.63 % (3587739)CaDiCaL version: 2.1.3 % 44.57/6.63 % (3587739)Termination reason: Inappropriate % 44.57/6.64 % (3587739)Time elapsed: 0.004 s % 44.57/6.64 % (3587739)Peak memory usage: 10 MB % 44.57/6.64 % (3587739)Instructions burned: 7 (million) % 44.57/6.64 % (3587739)------------------------------ % 44.57/6.64 % (3587739)------------------------------ % 44.57/6.64 % (3587741)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1974622244:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 44.57/6.64 % (3587741)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 44.57/6.64 % (3587741)Terminated due to inappropriate strategy. % 44.57/6.64 % (3587741)------------------------------ % 44.57/6.64 % (3587741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.57/6.64 % (3587741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.57/6.64 % (3587741)CaDiCaL version: 2.1.3 % 44.57/6.64 % (3587741)Termination reason: Inappropriate % 44.57/6.64 % (3587741)Time elapsed: 0.007 s % 44.57/6.64 % (3587741)Peak memory usage: 10 MB % 44.57/6.64 % (3587741)Instructions burned: 6 (million) % 44.57/6.64 % (3587741)------------------------------ % 44.57/6.64 % (3587741)------------------------------ % 44.57/6.64 % (3587743)ott-2_1_sil=16000:newcnf=on:random_seed=658146561:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 44.57/6.64 % (3587725)Instruction limit reached! % 44.57/6.64 % (3587725)------------------------------ % 44.57/6.64 % (3587725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.57/6.64 % (3587725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.57/6.64 % (3587725)CaDiCaL version: 2.1.3 % 44.57/6.64 % (3587725)Termination reason: Instruction limit % 44.57/6.64 % (3587725)Termination phase: Saturation % 44.57/6.64 % (3587725)Time elapsed: 0.798 s % 44.57/6.64 % (3587725)Peak memory usage: 16 MB % 44.57/6.64 % (3587725)Instructions burned: 879 (million) % 44.57/6.64 % (3587752)ott+10_1_sil=32000:tgt=ground:random_seed=4016364727:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi) % 44.57/6.64 % (3587719)Instruction limit reached! % 44.57/6.64 % (3587719)------------------------------ % 44.57/6.64 % (3587719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.57/6.64 % (3587719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.57/6.64 % (3587719)CaDiCaL version: 2.1.3 % 44.57/6.64 % (3587719)Termination reason: Instruction limit % 44.57/6.64 % (3587719)Termination phase: Saturation % 44.57/6.64 % (3587719)Time elapsed: 1.120 s % 44.57/6.64 % (3587719)Peak memory usage: 22 MB % 44.57/6.64 % (3587719)Instructions burned: 1179 (million) % 44.57/6.64 % (3587761)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3485125790:i=54282_2986 on theBenchmark for (2986ds/54282Mi) % 44.57/6.64 % (3587761)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 44.57/6.64 % (3587761)Terminated due to inappropriate strategy. % 44.57/6.64 % (3587761)------------------------------ % 44.57/6.64 % (3587761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.57/6.64 % (3587761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.57/6.64 % (3587761)CaDiCaL version: 2.1.3 % 44.57/6.64 % (3587761)Termination reason: Inappropriate % 44.57/6.64 % (3587761)Time elapsed: 0.009 s % 44.57/6.64 % (3587761)Peak memory usage: 10 MB % 44.57/6.64 % (3587761)Instructions burned: 7 (million) % 157.49/22.49 % (3587761)------------------------------ % 157.49/22.49 % (3587761)------------------------------ % 157.49/22.49 % (3587763)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=128184627:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 157.49/22.49 % (3587737)Instruction limit reached! % 157.49/22.49 % (3587737)------------------------------ % 157.49/22.49 % (3587737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.49/22.49 % (3587737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.49/22.49 % (3587737)CaDiCaL version: 2.1.3 % 157.49/22.49 % (3587737)Termination reason: Instruction limit % 157.49/22.49 % (3587737)Termination phase: Saturation % 157.49/22.49 % (3587737)Time elapsed: 0.723 s % 157.49/22.49 % (3587737)Peak memory usage: 25 MB % 157.49/22.49 % (3587737)Instructions burned: 1473 (million) % 157.49/22.49 % (3587765)dis+21_1_sil=32000:sas=cadical:random_seed=785591396:i=3773:amm=off_2984 on theBenchmark for (2984ds/3773Mi) % 157.49/22.49 % (3587743)Instruction limit reached! % 157.49/22.49 % (3587743)------------------------------ % 157.49/22.49 % (3587743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.49/22.49 % (3587743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.49/22.49 % (3587743)CaDiCaL version: 2.1.3 % 157.49/22.49 % (3587743)Termination reason: Instruction limit % 157.49/22.49 % (3587743)Termination phase: Saturation % 157.49/22.49 % (3587743)Time elapsed: 0.736 s % 157.49/22.49 % (3587743)Peak memory usage: 15 MB % 157.49/22.49 % (3587743)Instructions burned: 870 (million) % 157.49/22.49 % (3587767)ott+11_1_sil=16000:gs=on:random_seed=1806016008:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2982 on theBenchmark for (2982ds/2251Mi) % 157.49/22.49 % (3587765)Instruction limit reached! % 157.49/22.49 % (3587765)------------------------------ % 157.49/22.49 % (3587765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.49/22.49 % (3587765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.49/22.49 % (3587765)CaDiCaL version: 2.1.3 % 157.49/22.49 % (3587765)Termination reason: Instruction limit % 157.49/22.49 % (3587765)Termination phase: Saturation % 157.49/22.49 % (3587765)Time elapsed: 1.933 s % 157.49/22.49 % (3587765)Peak memory usage: 38 MB % 157.49/22.49 % (3587765)Instructions burned: 3773 (million) % 157.49/22.49 % (3587769)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=166296810:fmbsr=1.6:i=67534_2964 on theBenchmark for (2964ds/67534Mi) % 157.49/22.49 % (3587769)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.49/22.49 % (3587769)Terminated due to inappropriate strategy. % 157.49/22.49 % (3587769)------------------------------ % 157.49/22.49 % (3587769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.49/22.49 % (3587769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.49/22.49 % (3587769)CaDiCaL version: 2.1.3 % 157.49/22.49 % (3587769)Termination reason: Inappropriate % 157.49/22.49 % (3587769)Time elapsed: 0.004 s % 157.49/22.49 % (3587769)Peak memory usage: 10 MB % 157.49/22.49 % (3587769)Instructions burned: 7 (million) % 157.49/22.49 % (3587769)------------------------------ % 157.49/22.49 % (3587769)------------------------------ % 157.49/22.49 % (3587771)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2319108912:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2964 on theBenchmark for (2964ds/4591Mi) % 157.49/22.49 % (3587767)Instruction limit reached! % 157.49/22.49 % (3587767)------------------------------ % 157.49/22.49 % (3587767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.49/22.49 % (3587767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.49/22.49 % (3587767)CaDiCaL version: 2.1.3 % 157.49/22.49 % (3587767)Termination reason: Instruction limit % 157.49/22.49 % (3587767)Termination phase: Saturation % 157.49/22.49 % (3587767)Time elapsed: 2.218 s % 157.49/22.49 % (3587767)Peak memory usage: 32 MB % 157.49/22.49 % (3587767)Instructions burned: 2252 (million) % 157.49/22.49 % (3587773)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2896517323:i=29340_2959 on theBenchmark for (2959ds/29340Mi) % 157.49/22.49 % (3587763)Instruction limit reached! % 157.49/22.49 % (3587763)------------------------------ % 157.49/22.49 % (3587763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.49/22.49 % (3587763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.49/22.49 % (3587763)CaDiCaL version: 2.1.3 % 157.49/22.49 % (3587763)Termination reason: Instruction limit % 195.20/27.78 % (3587763)Termination phase: Saturation % 195.20/27.78 % (3587763)Time elapsed: 3.329 s % 195.20/27.78 % (3587763)Peak memory usage: 33 MB % 195.20/27.78 % (3587763)Instructions burned: 3512 (million) % 195.20/27.78 % (3587775)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=694322114:i=5211_2952 on theBenchmark for (2952ds/5211Mi) % 195.20/27.78 % (3587735)Instruction limit reached! % 195.20/27.78 % (3587735)------------------------------ % 195.20/27.78 % (3587735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.20/27.78 % (3587735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.20/27.78 % (3587735)CaDiCaL version: 2.1.3 % 195.20/27.78 % (3587735)Termination reason: Instruction limit % 195.20/27.78 % (3587735)Termination phase: Saturation % 195.20/27.78 % (3587735)Time elapsed: 4.752 s % 195.20/27.78 % (3587735)Peak memory usage: 43 MB % 195.20/27.78 % (3587735)Instructions burned: 5131 (million) % 195.20/27.78 % (3587777)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1434891370:i=5497:nm=2_2944 on theBenchmark for (2944ds/5497Mi) % 195.20/27.78 % (3587777)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 195.20/27.78 % (3587777)Terminated due to inappropriate strategy. % 195.20/27.78 % (3587777)------------------------------ % 195.20/27.78 % (3587777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.20/27.78 % (3587777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.20/27.78 % (3587777)CaDiCaL version: 2.1.3 % 195.20/27.78 % (3587777)Termination reason: Inappropriate % 195.20/27.78 % (3587777)Time elapsed: 0.005 s % 195.20/27.78 % (3587777)Peak memory usage: 11 MB % 195.20/27.78 % (3587777)Instructions burned: 7 (million) % 195.20/27.78 % (3587777)------------------------------ % 195.20/27.78 % (3587777)------------------------------ % 195.20/27.78 % (3587779)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1876740715:fmbsr=2:i=46332_2944 on theBenchmark for (2944ds/46332Mi) % 195.20/27.78 % (3587779)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 195.20/27.78 % (3587779)Terminated due to inappropriate strategy. % 195.20/27.78 % (3587779)------------------------------ % 195.20/27.78 % (3587779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.20/27.78 % (3587779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.20/27.78 % (3587779)CaDiCaL version: 2.1.3 % 195.20/27.78 % (3587779)Termination reason: Inappropriate % 195.20/27.78 % (3587779)Time elapsed: 0.005 s % 195.20/27.78 % (3587779)Peak memory usage: 11 MB % 195.20/27.78 % (3587779)Instructions burned: 7 (million) % 195.20/27.78 % (3587779)------------------------------ % 195.20/27.78 % (3587779)------------------------------ % 195.20/27.78 % (3587781)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1119799352:i=14071_2943 on theBenchmark for (2943ds/14071Mi) % 195.20/27.78 % (3587781)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 195.20/27.78 % (3587781)Terminated due to inappropriate strategy. % 195.20/27.78 % (3587781)------------------------------ % 195.20/27.78 % (3587781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.20/27.78 % (3587781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.20/27.78 % (3587781)CaDiCaL version: 2.1.3 % 195.20/27.78 % (3587781)Termination reason: Inappropriate % 195.20/27.78 % (3587781)Time elapsed: 0.008 s % 195.20/27.78 % (3587781)Peak memory usage: 10 MB % 195.20/27.78 % (3587781)Instructions burned: 7 (million) % 195.20/27.78 % (3587781)------------------------------ % 195.20/27.78 % (3587781)------------------------------ % 195.20/27.78 % (3587783)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=484902059:i=22565:add=on:rawr=on_2943 on theBenchmark for (2943ds/22565Mi) % 195.20/27.78 % (3587771)Instruction limit reached! % 195.20/27.78 % (3587771)------------------------------ % 195.20/27.78 % (3587771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.20/27.78 % (3587771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.20/27.78 % (3587771)CaDiCaL version: 2.1.3 % 195.20/27.78 % (3587771)Termination reason: Instruction limit % 195.20/27.78 % (3587771)Termination phase: Saturation % 195.20/27.78 % (3587771)Time elapsed: 2.301 s % 195.20/27.78 % (3587771)Peak memory usage: 49 MB % 195.20/27.78 % (3587771)Instructions burned: 4591 (million) % 195.20/27.78 % (3587785)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2271391135:i=8173:av=off_2941 on theBenchmark for (2941ds/8173Mi) % 195.20/27.78 % (3587752)Instruction limit reached! % 196.60/27.90 % (3587752)------------------------------ % 196.60/27.90 % (3587752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.60/27.90 % (3587752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.60/27.90 % (3587752)CaDiCaL version: 2.1.3 % 196.60/27.90 % (3587752)Termination reason: Instruction limit % 196.60/27.90 % (3587752)Termination phase: Saturation % 196.60/27.90 % (3587752)Time elapsed: 5.146 s % 196.60/27.90 % (3587752)Peak memory usage: 44 MB % 196.60/27.90 % (3587752)Instructions burned: 5114 (million) % 196.60/27.90 % (3587787)dis+10_16:1_sil=16000:random_seed=3678099081:i=9155:fsr=off_2936 on theBenchmark for (2936ds/9155Mi) % 196.60/27.90 % (3587775)Instruction limit reached! % 196.60/27.90 % (3587775)------------------------------ % 196.60/27.90 % (3587775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.60/27.90 % (3587775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.60/27.90 % (3587775)CaDiCaL version: 2.1.3 % 196.60/27.90 % (3587775)Termination reason: Instruction limit % 196.60/27.90 % (3587775)Termination phase: Saturation % 196.60/27.90 % (3587775)Time elapsed: 4.631 s % 196.60/27.90 % (3587775)Peak memory usage: 46 MB % 196.60/27.90 % (3587775)Instructions burned: 5211 (million) % 196.60/27.90 % (3587803)ott-3_8_sil=64000:random_seed=3745510760:i=20139:bs=on_2905 on theBenchmark for (2905ds/20139Mi) % 196.60/27.90 % (3587785)Instruction limit reached! % 196.60/27.90 % (3587785)------------------------------ % 196.60/27.90 % (3587785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.60/27.90 % (3587785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.60/27.90 % (3587785)CaDiCaL version: 2.1.3 % 196.60/27.90 % (3587785)Termination reason: Instruction limit % 196.60/27.90 % (3587785)Termination phase: Saturation % 196.60/27.90 % (3587785)Time elapsed: 4.413 s % 196.60/27.90 % (3587785)Peak memory usage: 67 MB % 196.60/27.90 % (3587785)Instructions burned: 8173 (million) % 196.60/27.90 % (3587807)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1862429659:fmbsr=2:i=32576_2896 on theBenchmark for (2896ds/32576Mi) % 196.60/27.90 % (3587807)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 196.60/27.90 % (3587807)Terminated due to inappropriate strategy. % 196.60/27.90 % (3587807)------------------------------ % 196.60/27.90 % (3587807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.60/27.90 % (3587807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.60/27.90 % (3587807)CaDiCaL version: 2.1.3 % 196.60/27.90 % (3587807)Termination reason: Inappropriate % 196.60/27.90 % (3587807)Time elapsed: 0.004 s % 196.60/27.90 % (3587807)Peak memory usage: 11 MB % 196.60/27.90 % (3587807)Instructions burned: 7 (million) % 196.60/27.90 % (3587807)------------------------------ % 196.60/27.90 % (3587807)------------------------------ % 196.60/27.90 % (3587809)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=559185231:i=11404_2896 on theBenchmark for (2896ds/11404Mi) % 196.60/27.90 % (3587787)Instruction limit reached! % 196.60/27.90 % (3587787)------------------------------ % 196.60/27.90 % (3587787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.60/27.90 % (3587787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.60/27.90 % (3587787)CaDiCaL version: 2.1.3 % 196.60/27.90 % (3587787)Termination reason: Instruction limit % 196.60/27.90 % (3587787)Termination phase: Saturation % 196.60/27.90 % (3587787)Time elapsed: 7.650 s % 196.60/27.90 % (3587787)Peak memory usage: 58 MB % 196.60/27.90 % (3587787)Instructions burned: 9156 (million) % 196.60/27.90 % (3587823)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4088973482:i=14134_2859 on theBenchmark for (2859ds/14134Mi) % 196.60/27.90 % (3587809)Instruction limit reached! % 196.60/27.90 % (3587809)------------------------------ % 196.60/27.90 % (3587809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.60/27.90 % (3587809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.60/27.90 % (3587809)CaDiCaL version: 2.1.3 % 196.60/27.90 % (3587809)Termination reason: Instruction limit % 196.60/27.90 % (3587809)Termination phase: Saturation % 196.60/27.90 % (3587809)Time elapsed: 6.402 s % 196.60/27.90 % (3587809)Peak memory usage: 75 MB % 196.60/27.90 % (3587809)Instructions burned: 11405 (million) % 196.60/27.90 % (3587837)dis+33_16_sil=32000:sac=on:random_seed=2941437583:i=15851:nm=0_2832 on theBenchmark for (2832ds/15851Mi) % 196.60/27.90 % (3587783)Instruction limit reached! % 196.60/27.90 % (3587783)------------------------------ % 196.60/27.90 % (3587783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.47/33.44 % (3587783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.47/33.44 % (3587783)CaDiCaL version: 2.1.3 % 235.47/33.44 % (3587783)Termination reason: Instruction limit % 235.47/33.44 % (3587783)Termination phase: Saturation % 235.47/33.44 % (3587783)Time elapsed: 16.511 s % 235.47/33.44 % (3587783)Peak memory usage: 258 MB % 235.47/33.44 % (3587783)Instructions burned: 22566 (million) % 235.47/33.44 % (3587847)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4014875764:avsq=on:i=17627:add=on:amm=off_2777 on theBenchmark for (2777ds/17627Mi) % 235.47/33.44 % (3587837)Instruction limit reached! % 235.47/33.44 % (3587837)------------------------------ % 235.47/33.44 % (3587837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.47/33.44 % (3587837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.47/33.44 % (3587837)CaDiCaL version: 2.1.3 % 235.47/33.44 % (3587837)Termination reason: Instruction limit % 235.47/33.44 % (3587837)Termination phase: Saturation % 235.47/33.44 % (3587837)Time elapsed: 8.001 s % 235.47/33.44 % (3587837)Peak memory usage: 106 MB % 235.47/33.44 % (3587837)Instructions burned: 15852 (million) % 235.47/33.44 % (3587853)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=996065595:s2a=on:i=53295_2751 on theBenchmark for (2751ds/53295Mi) % 235.47/33.44 % (3587773)Instruction limit reached! % 235.47/33.44 % (3587773)------------------------------ % 235.47/33.44 % (3587773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.47/33.44 % (3587773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.47/33.44 % (3587773)CaDiCaL version: 2.1.3 % 235.47/33.44 % (3587773)Termination reason: Instruction limit % 235.47/33.44 % (3587773)Termination phase: Saturation % 235.47/33.44 % (3587773)Time elapsed: 22.551 s % 235.47/33.44 % (3587773)Peak memory usage: 164 MB % 235.47/33.44 % (3587773)Instructions burned: 29341 (million) % 235.47/33.44 % (3588008)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2352471546:i=26857:ins=20_2733 on theBenchmark for (2733ds/26857Mi) % 235.47/33.44 % (3588008)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 235.47/33.44 % (3588008)Terminated due to inappropriate strategy. % 235.47/33.44 % (3588008)------------------------------ % 235.47/33.44 % (3588008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.47/33.44 % (3588008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.47/33.44 % (3588008)CaDiCaL version: 2.1.3 % 235.47/33.44 % (3588008)Termination reason: Inappropriate % 235.47/33.44 % (3588008)Time elapsed: 0.003 s % 235.47/33.44 % (3588008)Peak memory usage: 10 MB % 235.47/33.44 % (3588008)Instructions burned: 6 (million) % 235.47/33.44 % (3588008)------------------------------ % 235.47/33.44 % (3588008)------------------------------ % 235.47/33.44 % (3588010)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3899348655:i=28120:bs=on:fsr=off_2733 on theBenchmark for (2733ds/28120Mi) % 235.47/33.44 % (3587823)Instruction limit reached! % 235.47/33.44 % (3587823)------------------------------ % 235.47/33.44 % (3587823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.47/33.44 % (3587823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.47/33.44 % (3587823)CaDiCaL version: 2.1.3 % 235.47/33.44 % (3587823)Termination reason: Instruction limit % 235.47/33.44 % (3587823)Termination phase: Saturation % 235.47/33.44 % (3587823)Time elapsed: 13.359 s % 235.47/33.44 % (3587823)Peak memory usage: 88 MB % 235.47/33.44 % (3587823)Instructions burned: 14135 (million) % 235.47/33.44 % (3588012)fmb+10_1_sil=256000:fmbss=7:random_seed=3991238791:fmbsr=1.6:i=182295_2725 on theBenchmark for (2725ds/182295Mi) % 235.47/33.44 % (3588012)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 235.47/33.44 % (3588012)Terminated due to inappropriate strategy. % 235.47/33.44 % (3588012)------------------------------ % 235.47/33.44 % (3588012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.47/33.44 % (3588012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.47/33.44 % (3588012)CaDiCaL version: 2.1.3 % 235.47/33.44 % (3588012)Termination reason: Inappropriate % 235.47/33.44 % (3588012)Time elapsed: 0.003 s % 235.47/33.44 % (3588012)Peak memory usage: 10 MB % 235.47/33.44 % (3588012)Instructions burned: 6 (million) % 235.47/33.44 % (3588012)------------------------------ % 235.47/33.44 % (3588012)------------------------------ % 235.47/33.44 % (3588014)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=558503676:i=44625:gsp=on_2725 on theBenchmark for (2725ds/44625Mi) % 249.16/35.36 % (3588014)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.16/35.36 % (3588014)Terminated due to inappropriate strategy. % 249.16/35.36 % (3588014)------------------------------ % 249.16/35.36 % (3588014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.16/35.36 % (3588014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.16/35.36 % (3588014)CaDiCaL version: 2.1.3 % 249.16/35.36 % (3588014)Termination reason: Inappropriate % 249.16/35.36 % (3588014)Time elapsed: 0.004 s % 249.16/35.36 % (3588014)Peak memory usage: 10 MB % 249.16/35.36 % (3588014)Instructions burned: 6 (million) % 249.16/35.36 % (3588014)------------------------------ % 249.16/35.36 % (3588014)------------------------------ % 249.16/35.36 % (3588016)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1864586422:i=160505_2724 on theBenchmark for (2724ds/160505Mi) % 249.16/35.36 % (3588016)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.16/35.36 % (3588016)Terminated due to inappropriate strategy. % 249.16/35.36 % (3588016)------------------------------ % 249.16/35.36 % (3588016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.16/35.36 % (3588016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.16/35.36 % (3588016)CaDiCaL version: 2.1.3 % 249.16/35.36 % (3588016)Termination reason: Inappropriate % 249.16/35.36 % (3588016)Time elapsed: 0.003 s % 249.16/35.36 % (3588016)Peak memory usage: 10 MB % 249.16/35.36 % (3588016)Instructions burned: 6 (million) % 249.16/35.36 % (3588016)------------------------------ % 249.16/35.36 % (3588016)------------------------------ % 249.16/35.36 % (3588018)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2398063127:fmbsr=1.3:i=225729_2724 on theBenchmark for (2724ds/225729Mi) % 249.16/35.36 % (3588018)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.16/35.36 % (3588018)Terminated due to inappropriate strategy. % 249.16/35.36 % (3588018)------------------------------ % 249.16/35.36 % (3588018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.16/35.36 % (3588018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.16/35.36 % (3588018)CaDiCaL version: 2.1.3 % 249.16/35.36 % (3588018)Termination reason: Inappropriate % 249.16/35.36 % (3588018)Time elapsed: 0.004 s % 249.16/35.36 % (3588018)Peak memory usage: 10 MB % 249.16/35.36 % (3588018)Instructions burned: 7 (million) % 249.16/35.36 % (3588018)------------------------------ % 249.16/35.36 % (3588018)------------------------------ % 249.16/35.36 % (3588020)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=326448253:fmbsr=2:i=185024:ins=7_2724 on theBenchmark for (2724ds/185024Mi) % 249.16/35.36 % (3588020)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.16/35.36 % (3588020)Terminated due to inappropriate strategy. % 249.16/35.36 % (3588020)------------------------------ % 249.16/35.36 % (3588020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.16/35.36 % (3588020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.16/35.36 % (3588020)CaDiCaL version: 2.1.3 % 249.16/35.36 % (3588020)Termination reason: Inappropriate % 249.16/35.36 % (3588020)Time elapsed: 0.004 s % 249.16/35.36 % (3588020)Peak memory usage: 10 MB % 249.16/35.36 % (3588020)Instructions burned: 7 (million) % 249.16/35.36 % (3588020)------------------------------ % 249.16/35.36 % (3588020)------------------------------ % 249.16/35.36 % (3588022)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1484499457:rtra=on_2724 on theBenchmark for (2724ds/0Mi) % 249.16/35.36 % (3588022)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 249.16/35.36 % (3588022)Terminated due to inappropriate strategy. % 249.16/35.36 % (3588022)------------------------------ % 249.16/35.36 % (3588022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 249.16/35.36 % (3588022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.16/35.36 % (3588022)CaDiCaL version: 2.1.3 % 249.16/35.36 % (3588022)Termination reason: Inappropriate % 249.16/35.36 % (3588022)Time elapsed: 0.004 s % 249.16/35.36 % (3588022)Peak memory usage: 10 MB % 249.16/35.36 % (3588022)Instructions burned: 8 (million) % 249.16/35.36 % (3588022)------------------------------ % 249.16/35.36 % (3588022)------------------------------ % 249.16/35.36 % (3588024)% WARNING: option uhcvi not known. % 249.16/35.36 % (3588024)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=374013279:i=271062:add=off:rtra=on:rawr=on_2723 on theBenchmark for (2723ds/271062Mi) % 272.59/38.64 % (3587803)Instruction limit reached! % 272.59/38.64 % (3587803)------------------------------ % 272.59/38.64 % (3587803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.59/38.64 % (3587803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.59/38.64 % (3587803)CaDiCaL version: 2.1.3 % 272.59/38.64 % (3587803)Termination reason: Instruction limit % 272.59/38.64 % (3587803)Termination phase: Saturation % 272.59/38.64 % (3587803)Time elapsed: 18.634 s % 272.59/38.64 % (3587803)Peak memory usage: 76 MB % 272.59/38.64 % (3587803)Instructions burned: 20140 (million) % 272.59/38.64 % (3588026)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1893604525:i=176048:add=on:rtra=on:rawr=on_2718 on theBenchmark for (2718ds/176048Mi) % 272.59/38.64 % (3587847)Instruction limit reached! % 272.59/38.64 % (3587847)------------------------------ % 272.59/38.64 % (3587847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.59/38.64 % (3587847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.59/38.64 % (3587847)CaDiCaL version: 2.1.3 % 272.59/38.64 % (3587847)Termination reason: Instruction limit % 272.59/38.64 % (3587847)Termination phase: Saturation % 272.59/38.64 % (3587847)Time elapsed: 10.062 s % 272.59/38.64 % (3587847)Peak memory usage: 190 MB % 272.59/38.64 % (3587847)Instructions burned: 17627 (million) % 272.59/38.64 % (3588387)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3064409999:i=206:fgj=on:rtra=on_2676 on theBenchmark for (2676ds/206Mi) % 272.59/38.64 % (3588387)Instruction limit reached! % 272.59/38.64 % (3588387)------------------------------ % 272.59/38.64 % (3588387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.59/38.64 % (3588387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.59/38.64 % (3588387)CaDiCaL version: 2.1.3 % 272.59/38.64 % (3588387)Termination reason: Instruction limit % 272.59/38.64 % (3588387)Termination phase: Saturation % 272.59/38.64 % (3588387)Time elapsed: 0.133 s % 272.59/38.64 % (3588387)Peak memory usage: 14 MB % 272.59/38.64 % (3588387)Instructions burned: 206 (million) % 272.59/38.64 % (3588389)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2087006810:i=232:rtra=on_2674 on theBenchmark for (2674ds/232Mi) % 272.59/38.64 % (3588389)Instruction limit reached! % 272.59/38.64 % (3588389)------------------------------ % 272.59/38.64 % (3588389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.59/38.64 % (3588389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.59/38.64 % (3588389)CaDiCaL version: 2.1.3 % 272.59/38.64 % (3588389)Termination reason: Instruction limit % 272.59/38.64 % (3588389)Termination phase: Saturation % 272.59/38.64 % (3588389)Time elapsed: 0.153 s % 272.59/38.64 % (3588389)Peak memory usage: 14 MB % 272.59/38.64 % (3588389)Instructions burned: 237 (million) % 272.59/38.64 % (3588391)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2658282039:i=262:rtra=on_2672 on theBenchmark for (2672ds/262Mi) % 272.59/38.64 % (3588391)Instruction limit reached! % 272.59/38.64 % (3588391)------------------------------ % 272.59/38.64 % (3588391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.59/38.64 % (3588391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.59/38.64 % (3588391)CaDiCaL version: 2.1.3 % 272.59/38.64 % (3588391)Termination reason: Instruction limit % 272.59/38.64 % (3588391)Termination phase: Saturation % 272.59/38.64 % (3588391)Time elapsed: 0.172 s % 272.59/38.64 % (3588391)Peak memory usage: 14 MB % 272.59/38.64 % (3588391)Instructions burned: 263 (million) % 272.59/38.64 % (3588393)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3076279531:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2670 on theBenchmark for (2670ds/318Mi) % 272.59/38.64 % (3588393)Instruction limit reached! % 272.59/38.64 % (3588393)------------------------------ % 272.59/38.64 % (3588393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.59/38.64 % (3588393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.59/38.64 % (3588393)CaDiCaL version: 2.1.3 % 272.59/38.64 % (3588393)Termination reason: Instruction limit % 272.59/38.64 % (3588393)Termination phase: Saturation % 272.59/38.64 % (3588393)Time elapsed: 0.203 s % 272.59/38.64 % (3588393)Peak memory usage: 14 MB % 272.59/38.64 % (3588393)Instructions burned: 318 (million) % 272.59/38.64 % (3588395)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1185858996:i=1428:nm=2:rtra=on_2668 on theBenchmark for (2668ds/1428Mi) % 278.97/39.58 % (3588395)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 278.97/39.58 % (3588395)Terminated due to inappropriate strategy. % 278.97/39.58 % (3588395)------------------------------ % 278.97/39.58 % (3588395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.97/39.58 % (3588395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.97/39.58 % (3588395)CaDiCaL version: 2.1.3 % 278.97/39.58 % (3588395)Termination reason: Inappropriate % 278.97/39.58 % (3588395)Time elapsed: 0.004 s % 278.97/39.58 % (3588395)Peak memory usage: 10 MB % 278.97/39.58 % (3588395)Instructions burned: 8 (million) % 278.97/39.58 % (3588395)------------------------------ % 278.97/39.58 % (3588395)------------------------------ % 278.97/39.58 % (3588397)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2716839181:i=262:bd=preordered:rtra=on:fsd=on_2668 on theBenchmark for (2668ds/262Mi) % 278.97/39.58 % (3588397)Instruction limit reached! % 278.97/39.58 % (3588397)------------------------------ % 278.97/39.58 % (3588397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.97/39.58 % (3588397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.97/39.58 % (3588397)CaDiCaL version: 2.1.3 % 278.97/39.58 % (3588397)Termination reason: Instruction limit % 278.97/39.58 % (3588397)Termination phase: Saturation % 278.97/39.58 % (3588397)Time elapsed: 0.171 s % 278.97/39.58 % (3588397)Peak memory usage: 15 MB % 278.97/39.58 % (3588397)Instructions burned: 262 (million) % 278.97/39.58 % (3588399)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=795936335:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2666 on theBenchmark for (2666ds/1368Mi) % 278.97/39.58 % (3588399)Instruction limit reached! % 278.97/39.58 % (3588399)------------------------------ % 278.97/39.58 % (3588399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.97/39.58 % (3588399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.97/39.58 % (3588399)CaDiCaL version: 2.1.3 % 278.97/39.58 % (3588399)Termination reason: Instruction limit % 278.97/39.58 % (3588399)Termination phase: Saturation % 278.97/39.58 % (3588399)Time elapsed: 0.816 s % 278.97/39.58 % (3588399)Peak memory usage: 21 MB % 278.97/39.58 % (3588399)Instructions burned: 1369 (million) % 278.97/39.58 % (3588401)ott-21_1_sil=16000:si=on:fs=off:random_seed=3107138507:i=360:av=off:fsr=off:rtra=on_2657 on theBenchmark for (2657ds/360Mi) % 278.97/39.58 % (3588401)Instruction limit reached! % 278.97/39.58 % (3588401)------------------------------ % 278.97/39.58 % (3588401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.97/39.58 % (3588401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.97/39.58 % (3588401)CaDiCaL version: 2.1.3 % 278.97/39.58 % (3588401)Termination reason: Instruction limit % 278.97/39.58 % (3588401)Termination phase: Saturation % 278.97/39.58 % (3588401)Time elapsed: 0.180 s % 278.97/39.58 % (3588401)Peak memory usage: 13 MB % 278.97/39.58 % (3588401)Instructions burned: 361 (million) % 278.97/39.58 % (3588403)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3762222586:i=954:bd=all:rtra=on_2655 on theBenchmark for (2655ds/954Mi) % 278.97/39.58 % (3588403)Instruction limit reached! % 278.97/39.58 % (3588403)------------------------------ % 278.97/39.58 % (3588403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.97/39.58 % (3588403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.97/39.58 % (3588403)CaDiCaL version: 2.1.3 % 278.97/39.58 % (3588403)Termination reason: Instruction limit % 278.97/39.58 % (3588403)Termination phase: Saturation % 278.97/39.58 % (3588403)Time elapsed: 0.636 s % 278.97/39.58 % (3588403)Peak memory usage: 16 MB % 278.97/39.58 % (3588403)Instructions burned: 954 (million) % 278.97/39.58 % (3588405)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2767123607:fmbsr=1.3:i=1730:ins=25:rtra=on_2649 on theBenchmark for (2649ds/1730Mi) % 278.97/39.58 % (3588405)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 278.97/39.58 % (3588405)Terminated due to inappropriate strategy. % 278.97/39.58 % (3588405)------------------------------ % 278.97/39.58 % (3588405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.97/39.58 % (3588405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.97/39.58 % (3588405)CaDiCaL version: 2.1.3 % 278.97/39.58 % (3588405)Termination reason: Inappropriate % 278.97/39.58 % (3Terminated % 300.25/42.54 % Vampire exiting %------------------------------------------------------------------------------