%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW671_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:37 PM UTC 2026 % Result : Timeout 291.80s 41.58s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWW671_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.00/0.11 % Computer : n012.cluster.edu % 0.00/0.11 % Model : x86_64 x86_64 % 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.11 % Memory : 8046.5625MB % 0.00/0.11 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 14:24:04 UTC 2026 % 0.00/0.12 % CPUTime : % 0.00/0.12 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.14 Running first-order model finding % 0.09/0.14 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.61/0.71 % (3411531)Will run a generic schedule for satisfiability detection. % 3.61/0.71 % (3411537)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=454196523_2999 on theBenchmark for (2999ds/0Mi) % 3.61/0.71 % (3411537)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.61/0.71 % (3411537)Terminated due to inappropriate strategy. % 3.61/0.71 % (3411537)------------------------------ % 3.61/0.71 % (3411537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.71 % (3411537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.71 % (3411537)CaDiCaL version: 2.1.3 % 3.61/0.71 % (3411537)Termination reason: Inappropriate % 3.61/0.71 % (3411537)Time elapsed: 0.002 s % 3.61/0.71 % (3411537)Peak memory usage: 11 MB % 3.61/0.71 % (3411537)Instructions burned: 5 (million) % 3.61/0.71 % (3411538)% WARNING: option uhcvi not known. % 3.61/0.71 % (3411537)------------------------------ % 3.61/0.71 % (3411537)------------------------------ % 3.61/0.71 % (3411542)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3441521689:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.61/0.71 % (3411540)dis+10_1_sil=32000:sp=arity:random_seed=153710301:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.61/0.71 % (3411541)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1836421621:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.61/0.71 % (3411538)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=858203509:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.61/0.71 % (3411539)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3983626362:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.61/0.71 % (3411543)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3448424229:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.61/0.71 % (3411546)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1001170839:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.61/0.71 % (3411546)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.61/0.71 % (3411546)Terminated due to inappropriate strategy. % 3.61/0.71 % (3411546)------------------------------ % 3.61/0.71 % (3411546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.71 % (3411546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.71 % (3411546)CaDiCaL version: 2.1.3 % 3.61/0.71 % (3411546)Termination reason: Inappropriate % 3.61/0.71 % (3411546)Time elapsed: 0.002 s % 3.61/0.71 % (3411546)Peak memory usage: 10 MB % 3.61/0.71 % (3411546)Instructions burned: 4 (million) % 3.61/0.71 % (3411546)------------------------------ % 3.61/0.71 % (3411546)------------------------------ % 3.61/0.71 % (3411556)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1428094991:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.61/0.71 % (3411540)Instruction limit reached! % 3.61/0.71 % (3411540)------------------------------ % 3.61/0.71 % (3411540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.71 % (3411540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.71 % (3411540)CaDiCaL version: 2.1.3 % 3.61/0.71 % (3411540)Termination reason: Instruction limit % 3.61/0.71 % (3411540)Termination phase: Saturation % 3.61/0.71 % (3411540)Time elapsed: 0.058 s % 3.61/0.71 % (3411540)Peak memory usage: 12 MB % 3.61/0.71 % (3411540)Instructions burned: 103 (million) % 3.61/0.71 % (3411541)Instruction limit reached! % 3.61/0.71 % (3411541)------------------------------ % 3.61/0.71 % (3411541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.71 % (3411541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.71 % (3411541)CaDiCaL version: 2.1.3 % 3.61/0.71 % (3411541)Termination reason: Instruction limit % 3.61/0.71 % (3411541)Termination phase: Saturation % 3.61/0.71 % (3411541)Time elapsed: 0.064 s % 3.61/0.71 % (3411541)Peak memory usage: 12 MB % 3.61/0.71 % (3411541)Instructions burned: 117 (million) % 3.61/0.71 % (3411542)Instruction limit reached! % 3.61/0.71 % (3411542)------------------------------ % 3.61/0.71 % (3411542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.71 % (3411542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.71 % (3411542)CaDiCaL version: 2.1.3 % 3.61/0.71 % (3411542)Termination reason: Instruction limit % 4.07/0.83 % (3411542)Termination phase: Saturation % 4.07/0.83 % (3411542)Time elapsed: 0.070 s % 4.07/0.83 % (3411542)Peak memory usage: 12 MB % 4.07/0.83 % (3411542)Instructions burned: 131 (million) % 4.07/0.83 % (3411543)Instruction limit reached! % 4.07/0.83 % (3411543)------------------------------ % 4.07/0.83 % (3411543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.07/0.83 % (3411543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.07/0.83 % (3411543)CaDiCaL version: 2.1.3 % 4.07/0.83 % (3411543)Termination reason: Instruction limit % 4.07/0.83 % (3411543)Termination phase: Saturation % 4.07/0.83 % (3411543)Time elapsed: 0.074 s % 4.07/0.83 % (3411543)Peak memory usage: 13 MB % 4.07/0.83 % (3411543)Instructions burned: 160 (million) % 4.07/0.83 % (3411560)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=3327746216:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.07/0.83 % (3411561)ott-21_1_sil=16000:fs=off:random_seed=419602526:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 4.07/0.83 % (3411563)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=506473256:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 4.07/0.83 % (3411564)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=655658399:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 4.07/0.83 % (3411564)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.07/0.83 % (3411564)Terminated due to inappropriate strategy. % 4.07/0.83 % (3411564)------------------------------ % 4.07/0.83 % (3411564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.07/0.83 % (3411564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.07/0.83 % (3411564)CaDiCaL version: 2.1.3 % 4.07/0.83 % (3411564)Termination reason: Inappropriate % 4.07/0.83 % (3411564)Time elapsed: 0.002 s % 4.07/0.83 % (3411564)Peak memory usage: 10 MB % 4.07/0.83 % (3411564)Instructions burned: 3 (million) % 4.07/0.83 % (3411564)------------------------------ % 4.07/0.83 % (3411564)------------------------------ % 4.07/0.83 % (3411556)Instruction limit reached! % 4.07/0.83 % (3411556)------------------------------ % 4.07/0.83 % (3411556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.07/0.83 % (3411556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.07/0.83 % (3411556)CaDiCaL version: 2.1.3 % 4.07/0.83 % (3411556)Termination reason: Instruction limit % 4.07/0.83 % (3411556)Termination phase: Saturation % 4.07/0.83 % (3411556)Time elapsed: 0.081 s % 4.07/0.83 % (3411556)Peak memory usage: 13 MB % 4.07/0.83 % (3411556)Instructions burned: 132 (million) % 4.07/0.83 % (3411569)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3703807652:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.07/0.83 % (3411570)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2498855962:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.07/0.83 % (3411570)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.07/0.83 % (3411570)Terminated due to inappropriate strategy. % 4.07/0.83 % (3411570)------------------------------ % 4.07/0.83 % (3411570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.07/0.83 % (3411570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.07/0.83 % (3411570)CaDiCaL version: 2.1.3 % 4.07/0.83 % (3411570)Termination reason: Inappropriate % 4.07/0.83 % (3411570)Time elapsed: 0.003 s % 4.07/0.83 % (3411570)Peak memory usage: 10 MB % 4.07/0.83 % (3411570)Instructions burned: 5 (million) % 4.07/0.83 % (3411570)------------------------------ % 4.07/0.83 % (3411570)------------------------------ % 4.07/0.83 % (3411574)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=1197219093:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 4.07/0.83 % (3411561)Instruction limit reached! % 4.07/0.83 % (3411561)------------------------------ % 4.07/0.83 % (3411561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.07/0.83 % (3411561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.07/0.83 % (3411561)CaDiCaL version: 2.1.3 % 4.07/0.83 % (3411561)Termination reason: Instruction limit % 4.07/0.83 % (3411561)Termination phase: Saturation % 18.40/2.98 % (3411561)Time elapsed: 0.084 s % 18.40/2.98 % (3411561)Peak memory usage: 12 MB % 18.40/2.98 % (3411561)Instructions burned: 180 (million) % 18.40/2.98 % (3411580)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1176443644:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 18.40/2.98 % (3411560)Instruction limit reached! % 18.40/2.98 % (3411560)------------------------------ % 18.40/2.98 % (3411560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.40/2.98 % (3411560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.40/2.98 % (3411560)CaDiCaL version: 2.1.3 % 18.40/2.98 % (3411560)Termination reason: Instruction limit % 18.40/2.98 % (3411560)Termination phase: Saturation % 18.40/2.98 % (3411560)Time elapsed: 0.275 s % 18.40/2.98 % (3411560)Peak memory usage: 16 MB % 18.40/2.98 % (3411560)Instructions burned: 684 (million) % 18.40/2.98 % (3411563)Instruction limit reached! % 18.40/2.98 % (3411563)------------------------------ % 18.40/2.98 % (3411563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.40/2.98 % (3411563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.40/2.98 % (3411563)CaDiCaL version: 2.1.3 % 18.40/2.98 % (3411563)Termination reason: Instruction limit % 18.40/2.98 % (3411563)Termination phase: Saturation % 18.40/2.98 % (3411563)Time elapsed: 0.277 s % 18.40/2.98 % (3411563)Peak memory usage: 15 MB % 18.40/2.98 % (3411563)Instructions burned: 478 (million) % 18.40/2.98 % (3411587)fmb+10_1_sil=64000:random_seed=2992672394:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 18.40/2.98 % (3411587)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.40/2.98 % (3411587)Terminated due to inappropriate strategy. % 18.40/2.98 % (3411587)------------------------------ % 18.40/2.98 % (3411587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.40/2.98 % (3411587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.40/2.98 % (3411587)CaDiCaL version: 2.1.3 % 18.40/2.98 % (3411587)Termination reason: Inappropriate % 18.40/2.98 % (3411587)Time elapsed: 0.001 s % 18.40/2.98 % (3411587)Peak memory usage: 11 MB % 18.40/2.98 % (3411587)Instructions burned: 4 (million) % 18.40/2.98 % (3411587)------------------------------ % 18.40/2.98 % (3411587)------------------------------ % 18.40/2.98 % (3411590)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1309994521:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 18.40/2.98 % (3411590)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.40/2.98 % (3411590)Terminated due to inappropriate strategy. % 18.40/2.98 % (3411590)------------------------------ % 18.40/2.98 % (3411590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.40/2.98 % (3411590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.40/2.98 % (3411590)CaDiCaL version: 2.1.3 % 18.40/2.98 % (3411590)Termination reason: Inappropriate % 18.40/2.98 % (3411590)Time elapsed: 0.001 s % 18.40/2.98 % (3411590)Peak memory usage: 10 MB % 18.40/2.98 % (3411590)Instructions burned: 4 (million) % 18.40/2.98 % (3411590)------------------------------ % 18.40/2.98 % (3411590)------------------------------ % 18.40/2.98 % (3411589)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3807430750:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 18.40/2.98 % (3411589)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.40/2.98 % (3411589)Terminated due to inappropriate strategy. % 18.40/2.98 % (3411589)------------------------------ % 18.40/2.98 % (3411589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.40/2.98 % (3411589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.40/2.98 % (3411589)CaDiCaL version: 2.1.3 % 18.40/2.98 % (3411589)Termination reason: Inappropriate % 18.40/2.98 % (3411589)Time elapsed: 0.003 s % 18.40/2.98 % (3411589)Peak memory usage: 11 MB % 18.40/2.98 % (3411589)Instructions burned: 4 (million) % 18.40/2.98 % (3411589)------------------------------ % 18.40/2.98 % (3411589)------------------------------ % 18.40/2.98 % (3411594)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=724878269:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 18.40/2.98 % (3411593)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2991242718:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 18.40/2.98 % (3411574)Instruction limit reached! % 18.40/2.98 % (3411574)------------------------------ % 24.45/3.72 % (3411574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.45/3.72 % (3411574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.45/3.72 % (3411574)CaDiCaL version: 2.1.3 % 24.45/3.72 % (3411574)Termination reason: Instruction limit % 24.45/3.72 % (3411574)Termination phase: Saturation % 24.45/3.72 % (3411574)Time elapsed: 0.392 s % 24.45/3.72 % (3411574)Peak memory usage: 17 MB % 24.45/3.72 % (3411574)Instructions burned: 692 (million) % 24.45/3.72 % (3411605)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2534800902:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 24.45/3.72 % (3411605)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.45/3.72 % (3411605)Terminated due to inappropriate strategy. % 24.45/3.72 % (3411605)------------------------------ % 24.45/3.72 % (3411605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.45/3.72 % (3411605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.45/3.72 % (3411605)CaDiCaL version: 2.1.3 % 24.45/3.72 % (3411605)Termination reason: Inappropriate % 24.45/3.72 % (3411605)Time elapsed: 0.002 s % 24.45/3.72 % (3411605)Peak memory usage: 10 MB % 24.45/3.72 % (3411605)Instructions burned: 5 (million) % 24.45/3.72 % (3411605)------------------------------ % 24.45/3.72 % (3411605)------------------------------ % 24.45/3.72 % (3411607)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4161719543:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 24.45/3.72 % (3411607)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.45/3.72 % (3411607)Terminated due to inappropriate strategy. % 24.45/3.72 % (3411607)------------------------------ % 24.45/3.72 % (3411607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.45/3.72 % (3411607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.45/3.72 % (3411607)CaDiCaL version: 2.1.3 % 24.45/3.72 % (3411607)Termination reason: Inappropriate % 24.45/3.72 % (3411607)Time elapsed: 0.003 s % 24.45/3.72 % (3411607)Peak memory usage: 10 MB % 24.45/3.72 % (3411607)Instructions burned: 4 (million) % 24.45/3.72 % (3411607)------------------------------ % 24.45/3.72 % (3411607)------------------------------ % 24.45/3.72 % (3411610)ott-2_1_sil=16000:newcnf=on:random_seed=3064223472:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 24.45/3.72 % (3411569)Instruction limit reached! % 24.45/3.72 % (3411569)------------------------------ % 24.45/3.72 % (3411569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.45/3.72 % (3411569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.45/3.72 % (3411569)CaDiCaL version: 2.1.3 % 24.45/3.72 % (3411569)Termination reason: Instruction limit % 24.45/3.72 % (3411569)Termination phase: Saturation % 24.45/3.72 % (3411569)Time elapsed: 0.501 s % 24.45/3.72 % (3411569)Peak memory usage: 17 MB % 24.45/3.72 % (3411569)Instructions burned: 1180 (million) % 24.45/3.72 % (3411615)ott+10_1_sil=32000:tgt=ground:random_seed=1101526444:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 24.45/3.72 % (3411580)Instruction limit reached! % 24.45/3.72 % (3411580)------------------------------ % 24.45/3.72 % (3411580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.45/3.72 % (3411580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.45/3.72 % (3411580)CaDiCaL version: 2.1.3 % 24.45/3.72 % (3411580)Termination reason: Instruction limit % 24.45/3.72 % (3411580)Termination phase: Saturation % 24.45/3.72 % (3411580)Time elapsed: 0.459 s % 24.45/3.72 % (3411580)Peak memory usage: 18 MB % 24.45/3.72 % (3411580)Instructions burned: 881 (million) % 24.45/3.72 % (3411617)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2318679327:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 24.45/3.72 % (3411617)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.45/3.72 % (3411617)Terminated due to inappropriate strategy. % 24.45/3.72 % (3411617)------------------------------ % 24.45/3.72 % (3411617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.45/3.72 % (3411617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.45/3.72 % (3411617)CaDiCaL version: 2.1.3 % 24.45/3.72 % (3411617)Termination reason: Inappropriate % 24.45/3.72 % (3411617)Time elapsed: 0.002 s % 24.45/3.72 % (3411617)Peak memory usage: 10 MB % 24.45/3.72 % (3411617)Instructions burned: 5 (million) % 99.79/14.36 % (3411617)------------------------------ % 99.79/14.36 % (3411617)------------------------------ % 99.79/14.36 % (3411619)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1199039394:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi) % 99.79/14.36 % (3411610)Instruction limit reached! % 99.79/14.36 % (3411610)------------------------------ % 99.79/14.36 % (3411610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.36 % (3411610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.36 % (3411610)CaDiCaL version: 2.1.3 % 99.79/14.36 % (3411610)Termination reason: Instruction limit % 99.79/14.36 % (3411610)Termination phase: Saturation % 99.79/14.36 % (3411610)Time elapsed: 0.480 s % 99.79/14.36 % (3411610)Peak memory usage: 19 MB % 99.79/14.36 % (3411610)Instructions burned: 869 (million) % 99.79/14.36 % (3411625)dis+21_1_sil=32000:sas=cadical:random_seed=3350019914:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 99.79/14.36 % (3411594)Instruction limit reached! % 99.79/14.36 % (3411594)------------------------------ % 99.79/14.36 % (3411594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.36 % (3411594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.36 % (3411594)CaDiCaL version: 2.1.3 % 99.79/14.36 % (3411594)Termination reason: Instruction limit % 99.79/14.36 % (3411594)Termination phase: Saturation % 99.79/14.36 % (3411594)Time elapsed: 0.704 s % 99.79/14.36 % (3411594)Peak memory usage: 26 MB % 99.79/14.36 % (3411594)Instructions burned: 1474 (million) % 99.79/14.36 % (3411627)ott+11_1_sil=16000:gs=on:random_seed=1635756638:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 99.79/14.36 % (3411627)Instruction limit reached! % 99.79/14.36 % (3411627)------------------------------ % 99.79/14.36 % (3411627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.36 % (3411627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.36 % (3411627)CaDiCaL version: 2.1.3 % 99.79/14.36 % (3411627)Termination reason: Instruction limit % 99.79/14.36 % (3411627)Termination phase: Saturation % 99.79/14.36 % (3411627)Time elapsed: 0.972 s % 99.79/14.36 % (3411627)Peak memory usage: 25 MB % 99.79/14.36 % (3411627)Instructions burned: 2251 (million) % 99.79/14.36 % (3411633)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3124893385:fmbsr=1.6:i=67534_2978 on theBenchmark for (2978ds/67534Mi) % 99.79/14.36 % (3411633)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 99.79/14.36 % (3411633)Terminated due to inappropriate strategy. % 99.79/14.36 % (3411633)------------------------------ % 99.79/14.36 % (3411633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.36 % (3411633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.36 % (3411633)CaDiCaL version: 2.1.3 % 99.79/14.36 % (3411633)Termination reason: Inappropriate % 99.79/14.36 % (3411633)Time elapsed: 0.001 s % 99.79/14.36 % (3411633)Peak memory usage: 11 MB % 99.79/14.36 % (3411633)Instructions burned: 5 (million) % 99.79/14.36 % (3411633)------------------------------ % 99.79/14.36 % (3411633)------------------------------ % 99.79/14.36 % (3411635)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2942409489:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2978 on theBenchmark for (2978ds/4591Mi) % 99.79/14.36 % (3411619)Instruction limit reached! % 99.79/14.36 % (3411619)------------------------------ % 99.79/14.36 % (3411619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.36 % (3411619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.36 % (3411619)CaDiCaL version: 2.1.3 % 99.79/14.36 % (3411619)Termination reason: Instruction limit % 99.79/14.36 % (3411619)Termination phase: Saturation % 99.79/14.36 % (3411619)Time elapsed: 1.668 s % 99.79/14.36 % (3411619)Peak memory usage: 30 MB % 99.79/14.36 % (3411619)Instructions burned: 3515 (million) % 99.79/14.36 % (3411639)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=56951685:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 99.79/14.36 % (3411593)Instruction limit reached! % 99.79/14.36 % (3411593)------------------------------ % 99.79/14.36 % (3411593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.79/14.36 % (3411593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.79/14.36 % (3411593)CaDiCaL version: 2.1.3 % 99.79/14.36 % (3411593)Termination reason: Instruction limit % 114.30/16.40 % (3411593)Termination phase: Saturation % 114.30/16.40 % (3411593)Time elapsed: 2.414 s % 114.30/16.40 % (3411593)Peak memory usage: 44 MB % 114.30/16.40 % (3411593)Instructions burned: 5134 (million) % 114.30/16.40 % (3411649)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2387640493:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 114.30/16.40 % (3411625)Instruction limit reached! % 114.30/16.40 % (3411625)------------------------------ % 114.30/16.40 % (3411625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.30/16.40 % (3411625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.30/16.40 % (3411625)CaDiCaL version: 2.1.3 % 114.30/16.40 % (3411625)Termination reason: Instruction limit % 114.30/16.40 % (3411625)Termination phase: Saturation % 114.30/16.40 % (3411625)Time elapsed: 1.933 s % 114.30/16.40 % (3411625)Peak memory usage: 32 MB % 114.30/16.40 % (3411625)Instructions burned: 3775 (million) % 114.30/16.40 % (3411655)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2388680403:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 114.30/16.40 % (3411655)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.30/16.40 % (3411655)Terminated due to inappropriate strategy. % 114.30/16.40 % (3411655)------------------------------ % 114.30/16.40 % (3411655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.30/16.40 % (3411655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.30/16.40 % (3411655)CaDiCaL version: 2.1.3 % 114.30/16.40 % (3411655)Termination reason: Inappropriate % 114.30/16.40 % (3411655)Time elapsed: 0.003 s % 114.30/16.40 % (3411655)Peak memory usage: 10 MB % 114.30/16.40 % (3411655)Instructions burned: 5 (million) % 114.30/16.40 % (3411655)------------------------------ % 114.30/16.40 % (3411655)------------------------------ % 114.30/16.40 % (3411657)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=471608058:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 114.30/16.40 % (3411657)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.30/16.40 % (3411657)Terminated due to inappropriate strategy. % 114.30/16.40 % (3411657)------------------------------ % 114.30/16.40 % (3411657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.30/16.40 % (3411657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.30/16.40 % (3411657)CaDiCaL version: 2.1.3 % 114.30/16.40 % (3411657)Termination reason: Inappropriate % 114.30/16.40 % (3411657)Time elapsed: 0.001 s % 114.30/16.40 % (3411657)Peak memory usage: 11 MB % 114.30/16.40 % (3411657)Instructions burned: 5 (million) % 114.30/16.40 % (3411657)------------------------------ % 114.30/16.40 % (3411657)------------------------------ % 114.30/16.40 % (3411659)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2615216746:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 114.30/16.40 % (3411659)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.30/16.40 % (3411659)Terminated due to inappropriate strategy. % 114.30/16.40 % (3411659)------------------------------ % 114.30/16.40 % (3411659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.30/16.40 % (3411659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.30/16.40 % (3411659)CaDiCaL version: 2.1.3 % 114.30/16.40 % (3411659)Termination reason: Inappropriate % 114.30/16.40 % (3411659)Time elapsed: 0.003 s % 114.30/16.40 % (3411659)Peak memory usage: 10 MB % 114.30/16.40 % (3411659)Instructions burned: 5 (million) % 114.30/16.40 % (3411659)------------------------------ % 114.30/16.40 % (3411659)------------------------------ % 114.30/16.40 % (3411663)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=939234699:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 114.30/16.40 % (3411615)Instruction limit reached! % 114.30/16.40 % (3411615)------------------------------ % 114.30/16.40 % (3411615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.30/16.40 % (3411615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.30/16.40 % (3411615)CaDiCaL version: 2.1.3 % 114.30/16.40 % (3411615)Termination reason: Instruction limit % 114.30/16.40 % (3411615)Termination phase: Saturation % 114.30/16.40 % (3411615)Time elapsed: 2.731 s % 114.30/16.40 % (3411615)Peak memory usage: 32 MB % 114.30/16.40 % (3411615)Instructions burned: 5115 (million) % 114.30/16.40 % (3411667)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1666016160:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 114.30/16.40 % (3411635)Instruction limit reached! % 114.30/16.47 % (3411635)------------------------------ % 114.30/16.47 % (3411635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.30/16.47 % (3411635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.30/16.47 % (3411635)CaDiCaL version: 2.1.3 % 114.30/16.47 % (3411635)Termination reason: Instruction limit % 114.30/16.47 % (3411635)Termination phase: Saturation % 114.30/16.47 % (3411635)Time elapsed: 1.437 s % 114.30/16.47 % (3411635)Peak memory usage: 28 MB % 114.30/16.47 % (3411635)Instructions burned: 4597 (million) % 114.30/16.47 % (3411669)dis+10_16:1_sil=16000:random_seed=3713009322:i=9155:fsr=off_2964 on theBenchmark for (2964ds/9155Mi) % 114.30/16.47 % (3411649)Instruction limit reached! % 114.30/16.47 % (3411649)------------------------------ % 114.30/16.47 % (3411649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.30/16.47 % (3411649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.30/16.47 % (3411649)CaDiCaL version: 2.1.3 % 114.30/16.47 % (3411649)Termination reason: Instruction limit % 114.30/16.47 % (3411649)Termination phase: Saturation % 114.30/16.47 % (3411649)Time elapsed: 2.444 s % 114.30/16.47 % (3411649)Peak memory usage: 52 MB % 114.30/16.47 % (3411649)Instructions burned: 5211 (million) % 114.30/16.47 % (3411673)ott-3_8_sil=64000:random_seed=2516224912:i=20139:bs=on_2946 on theBenchmark for (2946ds/20139Mi) % 114.30/16.47 % (3411667)Instruction limit reached! % 114.30/16.47 % (3411667)------------------------------ % 114.30/16.47 % (3411667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.30/16.47 % (3411667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.30/16.47 % (3411667)CaDiCaL version: 2.1.3 % 114.30/16.47 % (3411667)Termination reason: Instruction limit % 114.30/16.47 % (3411667)Termination phase: Saturation % 114.30/16.47 % (3411667)Time elapsed: 4.336 s % 114.30/16.47 % (3411667)Peak memory usage: 46 MB % 114.30/16.47 % (3411667)Instructions burned: 8175 (million) % 114.30/16.47 % (3411681)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2335826025:fmbsr=2:i=32576_2922 on theBenchmark for (2922ds/32576Mi) % 114.30/16.47 % (3411681)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.30/16.47 % (3411681)Terminated due to inappropriate strategy. % 114.30/16.48 % (3411681)------------------------------ % 114.30/16.48 % (3411681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.30/16.48 % (3411681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.30/16.48 % (3411681)CaDiCaL version: 2.1.3 % 114.30/16.48 % (3411681)Termination reason: Inappropriate % 114.30/16.48 % (3411681)Time elapsed: 0.002 s % 114.30/16.48 % (3411681)Peak memory usage: 10 MB % 114.30/16.48 % (3411681)Instructions burned: 5 (million) % 114.30/16.48 % (3411681)------------------------------ % 114.30/16.48 % (3411681)------------------------------ % 114.30/16.48 % (3411683)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=724261030:i=11404_2922 on theBenchmark for (2922ds/11404Mi) % 114.30/16.48 % (3411669)Instruction limit reached! % 114.30/16.48 % (3411669)------------------------------ % 114.30/16.48 % (3411669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.30/16.48 % (3411669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.30/16.48 % (3411669)CaDiCaL version: 2.1.3 % 114.30/16.48 % (3411669)Termination reason: Instruction limit % 114.30/16.48 % (3411669)Termination phase: Saturation % 114.30/16.48 % (3411669)Time elapsed: 4.232 s % 114.30/16.48 % (3411669)Peak memory usage: 51 MB % 114.30/16.48 % (3411669)Instructions burned: 9157 (million) % 114.30/16.48 % (3411685)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=700326160:i=14134_2921 on theBenchmark for (2921ds/14134Mi) % 114.30/16.48 % (3411663)Instruction limit reached! % 114.30/16.48 % (3411663)------------------------------ % 114.30/16.48 % (3411663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.30/16.48 % (3411663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.30/16.48 % (3411663)CaDiCaL version: 2.1.3 % 114.30/16.48 % (3411663)Termination reason: Instruction limit % 114.30/16.48 % (3411663)Termination phase: Saturation % 114.30/16.48 % (3411663)Time elapsed: 8.742 s % 114.30/16.48 % (3411663)Peak memory usage: 176 MB % 114.30/16.48 % (3411663)Instructions burned: 22565 (million) % 114.30/16.48 % (3411691)dis+33_16_sil=32000:sac=on:random_seed=1052035020:i=15851:nm=0_2880 on theBenchmark for (2880ds/15851Mi) % 114.30/16.48 % (3411683)Instruction limit reached! % 114.30/16.48 % (3411683)------------------------------ % 114.30/16.48 % (3411683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.14/23.18 % (3411683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.14/23.18 % (3411683)CaDiCaL version: 2.1.3 % 162.14/23.18 % (3411683)Termination reason: Instruction limit % 162.14/23.18 % (3411683)Termination phase: Saturation % 162.14/23.18 % (3411683)Time elapsed: 6.439 s % 162.14/23.18 % (3411683)Peak memory usage: 63 MB % 162.14/23.18 % (3411683)Instructions burned: 11406 (million) % 162.14/23.18 % (3411699)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=152401264:avsq=on:i=17627:add=on:amm=off_2857 on theBenchmark for (2857ds/17627Mi) % 162.14/23.18 % (3411639)Instruction limit reached! % 162.14/23.18 % (3411639)------------------------------ % 162.14/23.18 % (3411639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.14/23.18 % (3411639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.14/23.18 % (3411639)CaDiCaL version: 2.1.3 % 162.14/23.18 % (3411639)Termination reason: Instruction limit % 162.14/23.18 % (3411639)Termination phase: Saturation % 162.14/23.18 % (3411639)Time elapsed: 12.650 s % 162.14/23.18 % (3411639)Peak memory usage: 91 MB % 162.14/23.18 % (3411639)Instructions burned: 29340 (million) % 162.14/23.18 % (3411701)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=699650566:s2a=on:i=53295_2849 on theBenchmark for (2849ds/53295Mi) % 162.14/23.18 % (3411685)Instruction limit reached! % 162.14/23.18 % (3411685)------------------------------ % 162.14/23.18 % (3411685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.14/23.18 % (3411685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.14/23.18 % (3411685)CaDiCaL version: 2.1.3 % 162.14/23.18 % (3411685)Termination reason: Instruction limit % 162.14/23.18 % (3411685)Termination phase: Saturation % 162.14/23.18 % (3411685)Time elapsed: 8.046 s % 162.14/23.18 % (3411685)Peak memory usage: 73 MB % 162.14/23.18 % (3411685)Instructions burned: 14135 (million) % 162.14/23.18 % (3411717)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=488613414:i=26857:ins=20_2841 on theBenchmark for (2841ds/26857Mi) % 162.14/23.18 % (3411717)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.14/23.18 % (3411717)Terminated due to inappropriate strategy. % 162.14/23.18 % (3411717)------------------------------ % 162.14/23.18 % (3411717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.14/23.18 % (3411717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.14/23.18 % (3411717)CaDiCaL version: 2.1.3 % 162.14/23.18 % (3411717)Termination reason: Inappropriate % 162.14/23.18 % (3411717)Time elapsed: 0.002 s % 162.14/23.18 % (3411717)Peak memory usage: 11 MB % 162.14/23.18 % (3411717)Instructions burned: 5 (million) % 162.14/23.18 % (3411717)------------------------------ % 162.14/23.18 % (3411717)------------------------------ % 162.14/23.18 % (3411719)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2265134981:i=28120:bs=on:fsr=off_2840 on theBenchmark for (2840ds/28120Mi) % 162.14/23.18 % (3411673)Instruction limit reached! % 162.14/23.18 % (3411673)------------------------------ % 162.14/23.18 % (3411673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.14/23.18 % (3411673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.14/23.18 % (3411673)CaDiCaL version: 2.1.3 % 162.14/23.18 % (3411673)Termination reason: Instruction limit % 162.14/23.18 % (3411673)Termination phase: Saturation % 162.14/23.18 % (3411673)Time elapsed: 10.901 s % 162.14/23.18 % (3411673)Peak memory usage: 77 MB % 162.14/23.18 % (3411673)Instructions burned: 20139 (million) % 162.14/23.18 % (3411723)fmb+10_1_sil=256000:fmbss=7:random_seed=1693683336:fmbsr=1.6:i=182295_2837 on theBenchmark for (2837ds/182295Mi) % 162.14/23.18 % (3411723)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.14/23.18 % (3411723)Terminated due to inappropriate strategy. % 162.14/23.18 % (3411723)------------------------------ % 162.14/23.18 % (3411723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.14/23.18 % (3411723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.14/23.18 % (3411723)CaDiCaL version: 2.1.3 % 162.14/23.18 % (3411723)Termination reason: Inappropriate % 162.14/23.18 % (3411723)Time elapsed: 0.001 s % 162.14/23.18 % (3411723)Peak memory usage: 10 MB % 162.14/23.18 % (3411723)Instructions burned: 4 (million) % 162.14/23.18 % (3411723)------------------------------ % 162.14/23.18 % (3411723)------------------------------ % 162.14/23.18 % (3411725)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2518197203:i=44625:gsp=on_2837 on theBenchmark for (2837ds/44625Mi) % 170.41/24.35 % (3411725)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.41/24.35 % (3411725)Terminated due to inappropriate strategy. % 170.41/24.35 % (3411725)------------------------------ % 170.41/24.35 % (3411725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.41/24.35 % (3411725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.41/24.35 % (3411725)CaDiCaL version: 2.1.3 % 170.41/24.35 % (3411725)Termination reason: Inappropriate % 170.41/24.35 % (3411725)Time elapsed: 0.002 s % 170.41/24.35 % (3411725)Peak memory usage: 10 MB % 170.41/24.35 % (3411725)Instructions burned: 8 (million) % 170.41/24.35 % (3411725)------------------------------ % 170.41/24.35 % (3411725)------------------------------ % 170.41/24.35 % (3411727)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3146644547:i=160505_2837 on theBenchmark for (2837ds/160505Mi) % 170.41/24.35 % (3411727)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.41/24.35 % (3411727)Terminated due to inappropriate strategy. % 170.41/24.35 % (3411727)------------------------------ % 170.41/24.35 % (3411727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.41/24.35 % (3411727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.41/24.35 % (3411727)CaDiCaL version: 2.1.3 % 170.41/24.35 % (3411727)Termination reason: Inappropriate % 170.41/24.35 % (3411727)Time elapsed: 0.001 s % 170.41/24.35 % (3411727)Peak memory usage: 10 MB % 170.41/24.35 % (3411727)Instructions burned: 4 (million) % 170.41/24.35 % (3411727)------------------------------ % 170.41/24.35 % (3411727)------------------------------ % 170.41/24.35 % (3411729)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1432187575:fmbsr=1.3:i=225729_2837 on theBenchmark for (2837ds/225729Mi) % 170.41/24.35 % (3411729)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.41/24.35 % (3411729)Terminated due to inappropriate strategy. % 170.41/24.35 % (3411729)------------------------------ % 170.41/24.35 % (3411729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.41/24.35 % (3411729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.41/24.35 % (3411729)CaDiCaL version: 2.1.3 % 170.41/24.35 % (3411729)Termination reason: Inappropriate % 170.41/24.35 % (3411729)Time elapsed: 0.001 s % 170.41/24.35 % (3411729)Peak memory usage: 10 MB % 170.41/24.35 % (3411729)Instructions burned: 5 (million) % 170.41/24.35 % (3411729)------------------------------ % 170.41/24.35 % (3411729)------------------------------ % 170.41/24.35 % (3411731)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4203355936:fmbsr=2:i=185024:ins=7_2837 on theBenchmark for (2837ds/185024Mi) % 170.41/24.35 % (3411731)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.41/24.35 % (3411731)Terminated due to inappropriate strategy. % 170.41/24.35 % (3411731)------------------------------ % 170.41/24.35 % (3411731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.41/24.35 % (3411731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.41/24.35 % (3411731)CaDiCaL version: 2.1.3 % 170.41/24.35 % (3411731)Termination reason: Inappropriate % 170.41/24.35 % (3411731)Time elapsed: 0.001 s % 170.41/24.35 % (3411731)Peak memory usage: 10 MB % 170.41/24.35 % (3411731)Instructions burned: 5 (million) % 170.41/24.35 % (3411731)------------------------------ % 170.41/24.35 % (3411731)------------------------------ % 170.41/24.35 % (3411733)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2439991641:rtra=on_2836 on theBenchmark for (2836ds/0Mi) % 170.41/24.35 % (3411733)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 170.41/24.35 % (3411733)Terminated due to inappropriate strategy. % 170.41/24.35 % (3411733)------------------------------ % 170.41/24.35 % (3411733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.41/24.35 % (3411733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.41/24.35 % (3411733)CaDiCaL version: 2.1.3 % 170.41/24.35 % (3411733)Termination reason: Inappropriate % 170.41/24.35 % (3411733)Time elapsed: 0.002 s % 170.41/24.35 % (3411733)Peak memory usage: 10 MB % 170.41/24.35 % (3411733)Instructions burned: 6 (million) % 170.41/24.35 % (3411733)------------------------------ % 170.41/24.35 % (3411733)------------------------------ % 170.41/24.35 % (3411735)% WARNING: option uhcvi not known. % 170.41/24.35 % (3411735)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2103772081:i=271062:add=off:rtra=on:rawr=on_2836 on theBenchmark for (2836ds/271062Mi) % 193.05/27.53 % (3411691)Instruction limit reached! % 193.05/27.53 % (3411691)------------------------------ % 193.05/27.53 % (3411691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.05/27.53 % (3411691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.05/27.53 % (3411691)CaDiCaL version: 2.1.3 % 193.05/27.53 % (3411691)Termination reason: Instruction limit % 193.05/27.53 % (3411691)Termination phase: Saturation % 193.05/27.53 % (3411691)Time elapsed: 7.186 s % 193.05/27.53 % (3411691)Peak memory usage: 124 MB % 193.05/27.53 % (3411691)Instructions burned: 15852 (million) % 193.05/27.53 % (3411759)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2009235352:i=176048:add=on:rtra=on:rawr=on_2808 on theBenchmark for (2808ds/176048Mi) % 193.05/27.53 % (3411699)Instruction limit reached! % 193.05/27.53 % (3411699)------------------------------ % 193.05/27.53 % (3411699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.05/27.53 % (3411699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.05/27.53 % (3411699)CaDiCaL version: 2.1.3 % 193.05/27.53 % (3411699)Termination reason: Instruction limit % 193.05/27.53 % (3411699)Termination phase: Saturation % 193.05/27.53 % (3411699)Time elapsed: 8.201 s % 193.05/27.53 % (3411699)Peak memory usage: 165 MB % 193.05/27.53 % (3411699)Instructions burned: 17627 (million) % 193.05/27.53 % (3411777)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4229201177:i=206:fgj=on:rtra=on_2775 on theBenchmark for (2775ds/206Mi) % 193.05/27.53 % (3411777)Instruction limit reached! % 193.05/27.53 % (3411777)------------------------------ % 193.05/27.53 % (3411777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.05/27.53 % (3411777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.05/27.53 % (3411777)CaDiCaL version: 2.1.3 % 193.05/27.53 % (3411777)Termination reason: Instruction limit % 193.05/27.53 % (3411777)Termination phase: Saturation % 193.05/27.53 % (3411777)Time elapsed: 0.075 s % 193.05/27.53 % (3411777)Peak memory usage: 14 MB % 193.05/27.53 % (3411777)Instructions burned: 206 (million) % 193.05/27.53 % (3411779)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1943452345:i=232:rtra=on_2774 on theBenchmark for (2774ds/232Mi) % 193.05/27.53 % (3411779)Instruction limit reached! % 193.05/27.53 % (3411779)------------------------------ % 193.05/27.53 % (3411779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.05/27.53 % (3411779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.05/27.53 % (3411779)CaDiCaL version: 2.1.3 % 193.05/27.53 % (3411779)Termination reason: Instruction limit % 193.05/27.53 % (3411779)Termination phase: Saturation % 193.05/27.53 % (3411779)Time elapsed: 0.086 s % 193.05/27.53 % (3411779)Peak memory usage: 14 MB % 193.05/27.53 % (3411779)Instructions burned: 233 (million) % 193.05/27.53 % (3411781)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1445232406:i=262:rtra=on_2773 on theBenchmark for (2773ds/262Mi) % 193.05/27.53 % (3411781)Instruction limit reached! % 193.05/27.53 % (3411781)------------------------------ % 193.05/27.53 % (3411781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.05/27.53 % (3411781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.05/27.53 % (3411781)CaDiCaL version: 2.1.3 % 193.05/27.53 % (3411781)Termination reason: Instruction limit % 193.05/27.53 % (3411781)Termination phase: Saturation % 193.05/27.53 % (3411781)Time elapsed: 0.109 s % 193.05/27.53 % (3411781)Peak memory usage: 15 MB % 193.05/27.53 % (3411781)Instructions burned: 263 (million) % 193.05/27.53 % (3411783)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1621751803:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2772 on theBenchmark for (2772ds/318Mi) % 193.05/27.53 % (3411783)Instruction limit reached! % 193.05/27.53 % (3411783)------------------------------ % 193.05/27.53 % (3411783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.05/27.53 % (3411783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.05/27.53 % (3411783)CaDiCaL version: 2.1.3 % 193.05/27.53 % (3411783)Termination reason: Instruction limit % 193.05/27.53 % (3411783)Termination phase: Saturation % 193.05/27.53 % (3411783)Time elapsed: 0.203 s % 193.05/27.53 % (3411783)Peak memory usage: 14 MB % 193.05/27.53 % (3411783)Instructions burned: 319 (million) % 193.05/27.53 % (3411785)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3865689553:i=1428:nm=2:rtra=on_2769 on theBenchmark for (2769ds/1428Mi) % 207.86/29.62 % (3411785)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.86/29.62 % (3411785)Terminated due to inappropriate strategy. % 207.86/29.62 % (3411785)------------------------------ % 207.86/29.62 % (3411785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.86/29.62 % (3411785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.86/29.62 % (3411785)CaDiCaL version: 2.1.3 % 207.86/29.62 % (3411785)Termination reason: Inappropriate % 207.86/29.62 % (3411785)Time elapsed: 0.002 s % 207.86/29.62 % (3411785)Peak memory usage: 11 MB % 207.86/29.62 % (3411785)Instructions burned: 5 (million) % 207.86/29.62 % (3411785)------------------------------ % 207.86/29.62 % (3411785)------------------------------ % 207.86/29.62 % (3411787)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2947049785:i=262:bd=preordered:rtra=on:fsd=on_2769 on theBenchmark for (2769ds/262Mi) % 207.86/29.62 % (3411787)Instruction limit reached! % 207.86/29.62 % (3411787)------------------------------ % 207.86/29.62 % (3411787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.86/29.62 % (3411787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.86/29.62 % (3411787)CaDiCaL version: 2.1.3 % 207.86/29.62 % (3411787)Termination reason: Instruction limit % 207.86/29.62 % (3411787)Termination phase: Saturation % 207.86/29.62 % (3411787)Time elapsed: 0.116 s % 207.86/29.62 % (3411787)Peak memory usage: 15 MB % 207.86/29.62 % (3411787)Instructions burned: 262 (million) % 207.86/29.62 % (3411789)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=2413138043:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2768 on theBenchmark for (2768ds/1368Mi) % 207.86/29.62 % (3411789)Instruction limit reached! % 207.86/29.62 % (3411789)------------------------------ % 207.86/29.62 % (3411789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.86/29.62 % (3411789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.86/29.62 % (3411789)CaDiCaL version: 2.1.3 % 207.86/29.62 % (3411789)Termination reason: Instruction limit % 207.86/29.62 % (3411789)Termination phase: Saturation % 207.86/29.62 % (3411789)Time elapsed: 0.474 s % 207.86/29.62 % (3411789)Peak memory usage: 19 MB % 207.86/29.62 % (3411789)Instructions burned: 1370 (million) % 207.86/29.62 % (3411797)ott-21_1_sil=16000:si=on:fs=off:random_seed=2313644333:i=360:av=off:fsr=off:rtra=on_2763 on theBenchmark for (2763ds/360Mi) % 207.86/29.62 % (3411797)Instruction limit reached! % 207.86/29.62 % (3411797)------------------------------ % 207.86/29.62 % (3411797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.86/29.62 % (3411797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.86/29.62 % (3411797)CaDiCaL version: 2.1.3 % 207.86/29.62 % (3411797)Termination reason: Instruction limit % 207.86/29.62 % (3411797)Termination phase: Saturation % 207.86/29.62 % (3411797)Time elapsed: 0.100 s % 207.86/29.62 % (3411797)Peak memory usage: 13 MB % 207.86/29.62 % (3411797)Instructions burned: 360 (million) % 207.86/29.62 % (3411799)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1430522556:i=954:bd=all:rtra=on_2762 on theBenchmark for (2762ds/954Mi) % 207.86/29.62 % (3411799)Instruction limit reached! % 207.86/29.62 % (3411799)------------------------------ % 207.86/29.62 % (3411799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.86/29.62 % (3411799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.86/29.62 % (3411799)CaDiCaL version: 2.1.3 % 207.86/29.62 % (3411799)Termination reason: Instruction limit % 207.86/29.62 % (3411799)Termination phase: Saturation % 207.86/29.62 % (3411799)Time elapsed: 0.388 s % 207.86/29.62 % (3411799)Peak memory usage: 16 MB % 207.86/29.62 % (3411799)Instructions burned: 955 (million) % 207.86/29.62 % (3411803)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=643187780:fmbsr=1.3:i=1730:ins=25:rtra=on_2758 on theBenchmark for (2758ds/1730Mi) % 207.86/29.62 % (3411803)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 207.86/29.62 % (3411803)Terminated due to inappropriate strategy. % 207.86/29.62 % (3411803)------------------------------ % 207.86/29.62 % (3411803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 207.86/29.62 % (3411803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.86/29.62 % (3411803)CaDiCaL version: 2.1.3 % 207.86/29.62 % (3411803)Termination reason: Inappropriate % 207.86/29.62 % (3411803)Time elapsed: 0.001 s % 260.17/37.04 % (3411803)Peak memory usage: 10 MB % 260.17/37.04 % (3411803)Instructions burned: 4 (million) % 260.17/37.04 % (3411803)------------------------------ % 260.17/37.04 % (3411803)------------------------------ % 260.17/37.04 % (3411805)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3909569863:i=2358:rtra=on_2757 on theBenchmark for (2757ds/2358Mi) % 260.17/37.04 % (3411805)Instruction limit reached! % 260.17/37.04 % (3411805)------------------------------ % 260.17/37.04 % (3411805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.17/37.04 % (3411805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.17/37.04 % (3411805)CaDiCaL version: 2.1.3 % 260.17/37.04 % (3411805)Termination reason: Instruction limit % 260.17/37.04 % (3411805)Termination phase: Saturation % 260.17/37.04 % (3411805)Time elapsed: 1.293 s % 260.17/37.04 % (3411805)Peak memory usage: 24 MB % 260.17/37.04 % (3411805)Instructions burned: 2358 (million) % 260.17/37.04 % (3411811)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3022927682:i=1778:ins=1:rtra=on_2744 on theBenchmark for (2744ds/1778Mi) % 260.17/37.04 % (3411811)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 260.17/37.04 % (3411811)Terminated due to inappropriate strategy. % 260.17/37.04 % (3411811)------------------------------ % 260.17/37.04 % (3411811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.17/37.04 % (3411811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.17/37.04 % (3411811)CaDiCaL version: 2.1.3 % 260.17/37.04 % (3411811)Termination reason: Inappropriate % 260.17/37.04 % (3411811)Time elapsed: 0.003 s % 260.17/37.04 % (3411811)Peak memory usage: 10 MB % 260.17/37.04 % (3411811)Instructions burned: 5 (million) % 260.17/37.04 % (3411811)------------------------------ % 260.17/37.04 % (3411811)------------------------------ % 260.17/37.04 % (3411813)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=990808615:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2744 on theBenchmark for (2744ds/1384Mi) % 260.17/37.04 % (3411813)Instruction limit reached! % 260.17/37.04 % (3411813)------------------------------ % 260.17/37.04 % (3411813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.17/37.04 % (3411813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.17/37.04 % (3411813)CaDiCaL version: 2.1.3 % 260.17/37.04 % (3411813)Termination reason: Instruction limit % 260.17/37.04 % (3411813)Termination phase: Saturation % 260.17/37.04 % (3411813)Time elapsed: 0.799 s % 260.17/37.04 % (3411813)Peak memory usage: 22 MB % 260.17/37.04 % (3411813)Instructions burned: 1385 (million) % 260.17/37.04 % (3411815)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2772401892:i=1758:kws=inv_precedence:fsr=off:rtra=on_2736 on theBenchmark for (2736ds/1758Mi) % 260.17/37.04 % (3411815)Instruction limit reached! % 260.17/37.04 % (3411815)------------------------------ % 260.17/37.04 % (3411815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.17/37.04 % (3411815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.17/37.04 % (3411815)CaDiCaL version: 2.1.3 % 260.17/37.04 % (3411815)Termination reason: Instruction limit % 260.17/37.04 % (3411815)Termination phase: Saturation % 260.17/37.04 % (3411815)Time elapsed: 0.939 s % 260.17/37.04 % (3411815)Peak memory usage: 25 MB % 260.17/37.04 % (3411815)Instructions burned: 1760 (million) % 260.17/37.04 % (3411819)fmb+10_1_sil=64000:si=on:random_seed=583704881:i=44122:nm=2:rtra=on:gsp=on_2726 on theBenchmark for (2726ds/44122Mi) % 260.17/37.04 % (3411819)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 260.17/37.04 % (3411819)Terminated due to inappropriate strategy. % 260.17/37.04 % (3411819)------------------------------ % 260.17/37.04 % (3411819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.17/37.04 % (3411819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.17/37.04 % (3411819)CaDiCaL version: 2.1.3 % 260.17/37.04 % (3411819)Termination reason: Inappropriate % 260.17/37.04 % (3411819)Time elapsed: 0.002 s % 260.17/37.04 % (3411819)Peak memory usage: 11 MB % 260.17/37.04 % (3411819)Instructions burned: 5 (million) % 260.17/37.04 % (3411819)------------------------------ % 260.17/37.04 % (3411819)------------------------------ % 260.17/37.04 % (3411821)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=4147515188:i=19030:nm=5:rtra=on_2726 on theBenchmark for (2726ds/19030Mi) % 291.80/41.58 % (3411821)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 291.80/41.58 % (3411821)Terminated due to inappropriate strategy. % 291.80/41.58 % (3411821)------------------------------ % 291.80/41.58 % (3411821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.80/41.58 % (3411821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.80/41.58 % (3411821)CaDiCaL version: 2.1.3 % 291.80/41.58 % (3411821)Termination reason: Inappropriate % 291.80/41.58 % (3411821)Time elapsed: 0.003 s % 291.80/41.58 % (3411821)Peak memory usage: 10 MB % 291.80/41.58 % (3411821)Instructions burned: 5 (million) % 291.80/41.58 % (3411821)------------------------------ % 291.80/41.58 % (3411821)------------------------------ % 291.80/41.58 % (3411823)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2233316445:fmbsr=1.7:i=1840:rtra=on_2726 on theBenchmark for (2726ds/1840Mi) % 291.80/41.58 % (3411823)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 291.80/41.58 % (3411823)Terminated due to inappropriate strategy. % 291.80/41.58 % (3411823)------------------------------ % 291.80/41.58 % (3411823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.80/41.58 % (3411823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.80/41.58 % (3411823)CaDiCaL version: 2.1.3 % 291.80/41.58 % (3411823)Termination reason: Inappropriate % 291.80/41.58 % (3411823)Time elapsed: 0.003 s % 291.80/41.58 % (3411823)Peak memory usage: 10 MB % 291.80/41.58 % (3411823)Instructions burned: 5 (million) % 291.80/41.58 % (3411823)------------------------------ % 291.80/41.58 % (3411823)------------------------------ % 291.80/41.58 % (3411825)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1697488578:i=10262:rtra=on_2725 on theBenchmark for (2725ds/10262Mi) % 291.80/41.58 % (3411719)Instruction limit reached! % 291.80/41.58 % (3411719)------------------------------ % 291.80/41.58 % (3411719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.80/41.58 % (3411719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.80/41.58 % (3411719)CaDiCaL version: 2.1.3 % 291.80/41.58 % (3411719)Termination reason: Instruction limit % 291.80/41.58 % (3411719)Termination phase: Saturation % 291.80/41.58 % (3411719)Time elapsed: 12.044 s % 291.80/41.58 % (3411719)Peak memory usage: 30 MB % 291.80/41.58 % (3411719)Instructions burned: 28120 (million) % 291.80/41.58 % (3411827)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=75400139:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2720 on theBenchmark for (2720ds/2944Mi) % 291.80/41.58 % (3411827)Instruction limit reached! % 291.80/41.58 % (3411827)------------------------------ % 291.80/41.58 % (3411827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.80/41.58 % (3411827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.80/41.58 % (3411827)CaDiCaL version: 2.1.3 % 291.80/41.58 % (3411827)Termination reason: Instruction limit % 291.80/41.58 % (3411827)Termination phase: Saturation % 291.80/41.58 % (3411827)Time elapsed: 1.433 s % 291.80/41.58 % (3411827)Peak memory usage: 36 MB % 291.80/41.58 % (3411827)Instructions burned: 2945 (million) % 291.80/41.58 % (3411831)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3107505519:i=12648:rtra=on_2705 on theBenchmark for (2705ds/12648Mi) % 291.80/41.58 % (3411831)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 291.80/41.58 % (3411831)Terminated due to inappropriate strategy. % 291.80/41.58 % (3411831)------------------------------ % 291.80/41.58 % (3411831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.80/41.58 % (3411831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.80/41.58 % (3411831)CaDiCaL version: 2.1.3 % 291.80/41.58 % (3411831)Termination reason: Inappropriate % 291.80/41.58 % (3411831)Time elapsed: 0.003 s % 291.80/41.58 % (3411831)Peak memory usage: 11 MB % 291.80/41.58 % (3411831)Instructions burned: 6 (million) % 291.80/41.58 % (3411831)------------------------------ % 291.80/41.58 % (3411831)------------------------------ % 291.80/41.58 % (3411833)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1381023712:fmbsr=2.30978:i=4348:rtra=on_2705 on theBenchmark for (2705ds/4348Mi) % 291.80/41.58 % (3411833)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 291.80/41.58 % (3411833)Terminated due to inappropriate strategy. % 291.80/41.58 % (3411833)------------------------------ % 291.80/41.58 % (3411833)Version: VaTerminated % 300.19/42.74 Terminated %------------------------------------------------------------------------------