%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM896_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n014.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 12:26:01 PM UTC 2026 % Result : Timeout 290.70s 41.42s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM896_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.38 % Computer : n014.cluster.edu % 0.11/0.38 % Model : x86_64 x86_64 % 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.38 % Memory : 8046.5625MB % 0.11/0.38 % OS : Linux 6.8.0-71-generic % 0.11/0.38 % CPULimit : 300 % 0.11/0.38 % WCLimit : 300 % 0.11/0.38 % DateTime : Sun Sep 27 21:38:16 UTC 2026 % 0.11/0.38 % CPUTime : % 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.41 Running first-order model finding % 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.01/1.00 % (1191058)Will run a generic schedule for satisfiability detection. % 2.01/1.00 % (1191067)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4181568358:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.01/1.00 % (1191064)% WARNING: option uhcvi not known. % 2.01/1.00 % (1191064)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=317072971:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.01/1.00 % (1191066)dis+10_1_sil=32000:sp=arity:random_seed=2852188095:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.01/1.00 % (1191065)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4200624333:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.01/1.00 % (1191063)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4220550796_2999 on theBenchmark for (2999ds/0Mi) % 2.01/1.00 % (1191063)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.01/1.00 % (1191063)Terminated due to inappropriate strategy. % 2.01/1.00 % (1191063)------------------------------ % 2.01/1.00 % (1191063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.01/1.00 % (1191063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.01/1.00 % (1191063)CaDiCaL version: 2.1.3 % 2.01/1.00 % (1191063)Termination reason: Inappropriate % 2.01/1.00 % (1191063)Time elapsed: 0.0000 s % 2.01/1.00 % (1191063)Peak memory usage: 10 MB % 2.01/1.00 % (1191063)------------------------------ % 2.01/1.00 % (1191063)------------------------------ % 2.01/1.00 % (1191068)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2806870339:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.01/1.00 % (1191069)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1903600899:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.01/1.00 % (1191075)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3847740026:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.01/1.00 % (1191075)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.01/1.00 % (1191075)Terminated due to inappropriate strategy. % 2.01/1.00 % (1191075)------------------------------ % 2.01/1.00 % (1191075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.01/1.00 % (1191075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.01/1.00 % (1191075)CaDiCaL version: 2.1.3 % 2.01/1.00 % (1191075)Termination reason: Inappropriate % 2.01/1.00 % (1191075)Time elapsed: 0.0000 s % 2.01/1.00 % (1191075)Peak memory usage: 10 MB % 2.01/1.00 % (1191075)------------------------------ % 2.01/1.00 % (1191075)------------------------------ % 2.01/1.00 % (1191067)Instruction limit reached! % 2.01/1.00 % (1191067)------------------------------ % 2.01/1.00 % (1191067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.01/1.00 % (1191067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.01/1.00 % (1191067)CaDiCaL version: 2.1.3 % 2.01/1.00 % (1191067)Termination reason: Instruction limit % 2.01/1.00 % (1191067)Termination phase: Saturation % 2.01/1.00 % (1191067)Time elapsed: 0.039 s % 2.01/1.00 % (1191067)Peak memory usage: 12 MB % 2.01/1.00 % (1191067)Instructions burned: 119 (million) % 2.01/1.00 % (1191080)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=2971318020:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.01/1.00 % (1191079)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3805812299:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.01/1.00 % (1191066)Instruction limit reached! % 2.01/1.00 % (1191066)------------------------------ % 2.01/1.00 % (1191066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.01/1.00 % (1191066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.01/1.00 % (1191066)CaDiCaL version: 2.1.3 % 2.01/1.00 % (1191066)Termination reason: Instruction limit % 2.01/1.00 % (1191066)Termination phase: Saturation % 2.01/1.00 % (1191066)Time elapsed: 0.066 s % 2.01/1.00 % (1191066)Peak memory usage: 12 MB % 2.01/1.00 % (1191066)Instructions burned: 104 (million) % 2.01/1.00 % (1191096)ott-21_1_sil=16000:fs=off:random_seed=3062546244:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 2.01/1.00 % (1191068)Instruction limit reached! % 2.01/1.00 % (1191068)------------------------------ % 6.70/1.59 % (1191068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.70/1.59 % (1191068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.70/1.59 % (1191068)CaDiCaL version: 2.1.3 % 6.70/1.59 % (1191068)Termination reason: Instruction limit % 6.70/1.59 % (1191068)Termination phase: Saturation % 6.70/1.59 % (1191068)Time elapsed: 0.103 s % 6.70/1.59 % (1191068)Peak memory usage: 13 MB % 6.70/1.59 % (1191068)Instructions burned: 133 (million) % 6.70/1.59 % (1191079)Instruction limit reached! % 6.70/1.59 % (1191079)------------------------------ % 6.70/1.59 % (1191079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.70/1.59 % (1191079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.70/1.59 % (1191079)CaDiCaL version: 2.1.3 % 6.70/1.59 % (1191079)Termination reason: Instruction limit % 6.70/1.59 % (1191079)Termination phase: Saturation % 6.70/1.59 % (1191079)Time elapsed: 0.092 s % 6.70/1.59 % (1191079)Peak memory usage: 12 MB % 6.70/1.59 % (1191079)Instructions burned: 131 (million) % 6.70/1.59 % (1191116)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1530897050:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.70/1.59 % (1191069)Instruction limit reached! % 6.70/1.59 % (1191069)------------------------------ % 6.70/1.59 % (1191069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.70/1.59 % (1191069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.70/1.59 % (1191069)CaDiCaL version: 2.1.3 % 6.70/1.59 % (1191069)Termination reason: Instruction limit % 6.70/1.59 % (1191069)Termination phase: Saturation % 6.70/1.59 % (1191069)Time elapsed: 0.127 s % 6.70/1.59 % (1191069)Peak memory usage: 13 MB % 6.70/1.59 % (1191069)Instructions burned: 159 (million) % 6.70/1.59 % (1191124)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1735442605:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.70/1.59 % (1191124)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.70/1.59 % (1191124)Terminated due to inappropriate strategy. % 6.70/1.59 % (1191124)------------------------------ % 6.70/1.59 % (1191124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.70/1.59 % (1191124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.70/1.59 % (1191124)CaDiCaL version: 2.1.3 % 6.70/1.59 % (1191124)Termination reason: Inappropriate % 6.70/1.59 % (1191124)Time elapsed: 0.0000 s % 6.70/1.59 % (1191124)Peak memory usage: 10 MB % 6.70/1.59 % (1191124)------------------------------ % 6.70/1.59 % (1191124)------------------------------ % 6.70/1.59 % (1191096)Instruction limit reached! % 6.70/1.59 % (1191096)------------------------------ % 6.70/1.59 % (1191096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.70/1.59 % (1191096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.70/1.59 % (1191096)CaDiCaL version: 2.1.3 % 6.70/1.59 % (1191096)Termination reason: Instruction limit % 6.70/1.59 % (1191096)Termination phase: Saturation % 6.70/1.59 % (1191096)Time elapsed: 0.080 s % 6.70/1.59 % (1191096)Peak memory usage: 12 MB % 6.70/1.59 % (1191096)Instructions burned: 181 (million) % 6.70/1.59 % (1191131)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3076297475:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.70/1.59 % (1191138)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=18160498:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.70/1.59 % (1191138)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.70/1.59 % (1191138)Terminated due to inappropriate strategy. % 6.70/1.59 % (1191138)------------------------------ % 6.70/1.59 % (1191138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.70/1.59 % (1191138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.70/1.59 % (1191138)CaDiCaL version: 2.1.3 % 6.70/1.59 % (1191138)Termination reason: Inappropriate % 6.70/1.59 % (1191138)Time elapsed: 0.0000 s % 6.70/1.59 % (1191138)Peak memory usage: 10 MB % 6.70/1.59 % (1191138)------------------------------ % 6.70/1.59 % (1191138)------------------------------ % 6.70/1.59 % (1191142)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=1160661478:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 6.70/1.59 % (1191154)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1259418739:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.55/3.56 % (1191080)Instruction limit reached! % 21.55/3.56 % (1191080)------------------------------ % 21.55/3.56 % (1191080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.55/3.56 % (1191080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.55/3.56 % (1191080)CaDiCaL version: 2.1.3 % 21.55/3.56 % (1191080)Termination reason: Instruction limit % 21.55/3.56 % (1191080)Termination phase: Saturation % 21.55/3.56 % (1191080)Time elapsed: 0.217 s % 21.55/3.56 % (1191080)Peak memory usage: 18 MB % 21.55/3.56 % (1191080)Instructions burned: 684 (million) % 21.55/3.56 % (1191175)fmb+10_1_sil=64000:random_seed=1580955345:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 21.55/3.56 % (1191175)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.55/3.56 % (1191175)Terminated due to inappropriate strategy. % 21.55/3.56 % (1191175)------------------------------ % 21.55/3.56 % (1191175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.55/3.56 % (1191175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.55/3.56 % (1191175)CaDiCaL version: 2.1.3 % 21.55/3.56 % (1191175)Termination reason: Inappropriate % 21.55/3.56 % (1191175)Time elapsed: 0.0000 s % 21.55/3.56 % (1191175)Peak memory usage: 10 MB % 21.55/3.56 % (1191175)------------------------------ % 21.55/3.56 % (1191175)------------------------------ % 21.55/3.56 % (1191181)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3124452977:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 21.55/3.56 % (1191181)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.55/3.56 % (1191181)Terminated due to inappropriate strategy. % 21.55/3.56 % (1191181)------------------------------ % 21.55/3.56 % (1191181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.55/3.56 % (1191181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.55/3.56 % (1191181)CaDiCaL version: 2.1.3 % 21.55/3.56 % (1191181)Termination reason: Inappropriate % 21.55/3.56 % (1191181)Time elapsed: 0.0000 s % 21.55/3.56 % (1191181)Peak memory usage: 10 MB % 21.55/3.56 % (1191181)------------------------------ % 21.55/3.56 % (1191181)------------------------------ % 21.55/3.56 % (1191183)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2132234416:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 21.55/3.56 % (1191183)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.55/3.56 % (1191183)Terminated due to inappropriate strategy. % 21.55/3.56 % (1191183)------------------------------ % 21.55/3.56 % (1191183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.55/3.56 % (1191183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.55/3.56 % (1191183)CaDiCaL version: 2.1.3 % 21.55/3.56 % (1191183)Termination reason: Inappropriate % 21.55/3.56 % (1191183)Time elapsed: 0.0000 s % 21.55/3.56 % (1191183)Peak memory usage: 10 MB % 21.55/3.56 % (1191183)------------------------------ % 21.55/3.56 % (1191183)------------------------------ % 21.55/3.56 % (1191185)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=187141135:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 21.55/3.56 % (1191116)Instruction limit reached! % 21.55/3.56 % (1191116)------------------------------ % 21.55/3.56 % (1191116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.55/3.56 % (1191116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.55/3.56 % (1191116)CaDiCaL version: 2.1.3 % 21.55/3.56 % (1191116)Termination reason: Instruction limit % 21.55/3.56 % (1191116)Termination phase: Saturation % 21.55/3.56 % (1191116)Time elapsed: 0.315 s % 21.55/3.56 % (1191116)Peak memory usage: 15 MB % 21.55/3.56 % (1191116)Instructions burned: 477 (million) % 21.55/3.56 % (1191206)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1234462081:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 21.55/3.56 % (1191142)Instruction limit reached! % 21.55/3.56 % (1191142)------------------------------ % 21.55/3.56 % (1191142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.55/3.56 % (1191142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.55/3.56 % (1191142)CaDiCaL version: 2.1.3 % 21.55/3.56 % (1191142)Termination reason: Instruction limit % 27.41/4.39 % (1191142)Termination phase: Saturation % 27.41/4.39 % (1191142)Time elapsed: 0.361 s % 27.41/4.39 % (1191142)Peak memory usage: 15 MB % 27.41/4.39 % (1191142)Instructions burned: 693 (million) % 27.41/4.39 % (1191208)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1140233320:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 27.41/4.39 % (1191208)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.41/4.39 % (1191208)Terminated due to inappropriate strategy. % 27.41/4.39 % (1191208)------------------------------ % 27.41/4.39 % (1191208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.41/4.39 % (1191208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.41/4.39 % (1191208)CaDiCaL version: 2.1.3 % 27.41/4.39 % (1191208)Termination reason: Inappropriate % 27.41/4.39 % (1191208)Time elapsed: 0.0000 s % 27.41/4.39 % (1191208)Peak memory usage: 10 MB % 27.41/4.39 % (1191208)------------------------------ % 27.41/4.39 % (1191208)------------------------------ % 27.41/4.39 % (1191210)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2929365716:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 27.41/4.39 % (1191210)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.41/4.39 % (1191210)Terminated due to inappropriate strategy. % 27.41/4.39 % (1191210)------------------------------ % 27.41/4.39 % (1191210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.41/4.39 % (1191210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.41/4.39 % (1191210)CaDiCaL version: 2.1.3 % 27.41/4.39 % (1191210)Termination reason: Inappropriate % 27.41/4.39 % (1191210)Time elapsed: 0.0000 s % 27.41/4.39 % (1191210)Peak memory usage: 10 MB % 27.41/4.39 % (1191210)------------------------------ % 27.41/4.39 % (1191210)------------------------------ % 27.41/4.39 % (1191212)ott-2_1_sil=16000:newcnf=on:random_seed=3850300022:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 27.41/4.39 % (1191154)Instruction limit reached! % 27.41/4.39 % (1191154)------------------------------ % 27.41/4.39 % (1191154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.41/4.39 % (1191154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.41/4.39 % (1191154)CaDiCaL version: 2.1.3 % 27.41/4.39 % (1191154)Termination reason: Instruction limit % 27.41/4.39 % (1191154)Termination phase: Saturation % 27.41/4.39 % (1191154)Time elapsed: 0.501 s % 27.41/4.39 % (1191154)Peak memory usage: 20 MB % 27.41/4.39 % (1191154)Instructions burned: 880 (million) % 27.41/4.39 % (1191235)ott+10_1_sil=32000:tgt=ground:random_seed=3932065002:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 27.41/4.39 % (1191131)Instruction limit reached! % 27.41/4.39 % (1191131)------------------------------ % 27.41/4.39 % (1191131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.41/4.39 % (1191131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.41/4.39 % (1191131)CaDiCaL version: 2.1.3 % 27.41/4.39 % (1191131)Termination reason: Instruction limit % 27.41/4.39 % (1191131)Termination phase: Saturation % 27.41/4.39 % (1191131)Time elapsed: 0.785 s % 27.41/4.39 % (1191131)Peak memory usage: 17 MB % 27.41/4.39 % (1191131)Instructions burned: 1179 (million) % 27.41/4.39 % (1191308)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2472631756:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 27.41/4.39 % (1191308)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.41/4.39 % (1191308)Terminated due to inappropriate strategy. % 27.41/4.39 % (1191308)------------------------------ % 27.41/4.39 % (1191308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.41/4.39 % (1191308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.41/4.39 % (1191308)CaDiCaL version: 2.1.3 % 27.41/4.39 % (1191308)Termination reason: Inappropriate % 27.41/4.39 % (1191308)Time elapsed: 0.0000 s % 27.41/4.39 % (1191308)Peak memory usage: 10 MB % 27.41/4.39 % (1191308)------------------------------ % 27.41/4.39 % (1191308)------------------------------ % 27.41/4.39 % (1191317)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3837661524:i=3512:aac=none_2989 on theBenchmark for (2989ds/3512Mi) % 27.41/4.39 % (1191212)Instruction limit reached! % 27.41/4.39 % (1191212)------------------------------ % 27.41/4.39 % (1191212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.41/4.39 % (1191212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.88/16.21 % (1191212)CaDiCaL version: 2.1.3 % 111.88/16.21 % (1191212)Termination reason: Instruction limit % 111.88/16.21 % (1191212)Termination phase: Saturation % 111.88/16.21 % (1191212)Time elapsed: 0.522 s % 111.88/16.21 % (1191212)Peak memory usage: 15 MB % 111.88/16.21 % (1191212)Instructions burned: 869 (million) % 111.88/16.21 % (1191355)dis+21_1_sil=32000:sas=cadical:random_seed=913662052:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 111.88/16.21 % (1191206)Instruction limit reached! % 111.88/16.21 % (1191206)------------------------------ % 111.88/16.21 % (1191206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.88/16.21 % (1191206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.88/16.21 % (1191206)CaDiCaL version: 2.1.3 % 111.88/16.21 % (1191206)Termination reason: Instruction limit % 111.88/16.21 % (1191206)Termination phase: Saturation % 111.88/16.21 % (1191206)Time elapsed: 0.765 s % 111.88/16.21 % (1191206)Peak memory usage: 25 MB % 111.88/16.21 % (1191206)Instructions burned: 1472 (million) % 111.88/16.21 % (1191370)ott+11_1_sil=16000:gs=on:random_seed=674790541:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 111.88/16.21 % (1191185)Instruction limit reached! % 111.88/16.21 % (1191185)------------------------------ % 111.88/16.21 % (1191185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.88/16.21 % (1191185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.88/16.21 % (1191185)CaDiCaL version: 2.1.3 % 111.88/16.21 % (1191185)Termination reason: Instruction limit % 111.88/16.21 % (1191185)Termination phase: Saturation % 111.88/16.21 % (1191185)Time elapsed: 1.479 s % 111.88/16.21 % (1191185)Peak memory usage: 40 MB % 111.88/16.21 % (1191185)Instructions burned: 5135 (million) % 111.88/16.21 % (1191406)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1081028914:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 111.88/16.21 % (1191406)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 111.88/16.21 % (1191406)Terminated due to inappropriate strategy. % 111.88/16.21 % (1191406)------------------------------ % 111.88/16.21 % (1191406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.88/16.21 % (1191406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.88/16.21 % (1191406)CaDiCaL version: 2.1.3 % 111.88/16.21 % (1191406)Termination reason: Inappropriate % 111.88/16.21 % (1191406)Time elapsed: 0.0000 s % 111.88/16.21 % (1191406)Peak memory usage: 10 MB % 111.88/16.21 % (1191406)------------------------------ % 111.88/16.21 % (1191406)------------------------------ % 111.88/16.21 % (1191408)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3640382485:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 111.88/16.21 % (1191370)Instruction limit reached! % 111.88/16.21 % (1191370)------------------------------ % 111.88/16.21 % (1191370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.88/16.21 % (1191370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.88/16.21 % (1191370)CaDiCaL version: 2.1.3 % 111.88/16.21 % (1191370)Termination reason: Instruction limit % 111.88/16.21 % (1191370)Termination phase: Saturation % 111.88/16.21 % (1191370)Time elapsed: 1.212 s % 111.88/16.21 % (1191370)Peak memory usage: 21 MB % 111.88/16.21 % (1191370)Instructions burned: 2251 (million) % 111.88/16.21 % (1191410)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3656948651:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 111.88/16.21 % (1191317)Instruction limit reached! % 111.88/16.21 % (1191317)------------------------------ % 111.88/16.21 % (1191317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 111.88/16.21 % (1191317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.88/16.21 % (1191317)CaDiCaL version: 2.1.3 % 111.88/16.21 % (1191317)Termination reason: Instruction limit % 111.88/16.21 % (1191317)Termination phase: Saturation % 111.88/16.21 % (1191317)Time elapsed: 1.854 s % 111.88/16.21 % (1191317)Peak memory usage: 29 MB % 111.88/16.21 % (1191317)Instructions burned: 3512 (million) % 111.88/16.21 % (1191412)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=923611617:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 111.88/16.21 % (1191408)Instruction limit reached! % 111.88/16.21 % (1191408)------------------------------ % 111.88/16.21 % (1191408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.07/17.74 % (1191408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.07/17.74 % (1191408)CaDiCaL version: 2.1.3 % 117.07/17.74 % (1191408)Termination reason: Instruction limit % 117.07/17.74 % (1191408)Termination phase: Saturation % 117.07/17.74 % (1191408)Time elapsed: 1.294 s % 117.07/17.74 % (1191408)Peak memory usage: 30 MB % 117.07/17.74 % (1191408)Instructions burned: 4592 (million) % 117.07/17.74 % (1191414)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4160543122:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 117.07/17.74 % (1191414)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.07/17.74 % (1191414)Terminated due to inappropriate strategy. % 117.07/17.74 % (1191414)------------------------------ % 117.07/17.74 % (1191414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.07/17.74 % (1191414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.07/17.74 % (1191414)CaDiCaL version: 2.1.3 % 117.07/17.74 % (1191414)Termination reason: Inappropriate % 117.07/17.74 % (1191414)Time elapsed: 0.0000 s % 117.07/17.74 % (1191414)Peak memory usage: 10 MB % 117.07/17.74 % (1191414)------------------------------ % 117.07/17.74 % (1191414)------------------------------ % 117.07/17.74 % (1191416)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2697453348:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 117.07/17.74 % (1191416)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.07/17.74 % (1191416)Terminated due to inappropriate strategy. % 117.07/17.74 % (1191416)------------------------------ % 117.07/17.74 % (1191416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.07/17.74 % (1191416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.07/17.74 % (1191416)CaDiCaL version: 2.1.3 % 117.07/17.74 % (1191416)Termination reason: Inappropriate % 117.07/17.74 % (1191416)Time elapsed: 0.0000 s % 117.07/17.74 % (1191416)Peak memory usage: 10 MB % 117.07/17.74 % (1191416)------------------------------ % 117.07/17.74 % (1191416)------------------------------ % 117.07/17.74 % (1191418)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=115388068:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 117.07/17.74 % (1191418)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.07/17.74 % (1191418)Terminated due to inappropriate strategy. % 117.07/17.74 % (1191418)------------------------------ % 117.07/17.74 % (1191418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.07/17.74 % (1191418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.07/17.74 % (1191418)CaDiCaL version: 2.1.3 % 117.07/17.74 % (1191418)Termination reason: Inappropriate % 117.07/17.74 % (1191418)Time elapsed: 0.0000 s % 117.07/17.74 % (1191418)Peak memory usage: 10 MB % 117.07/17.74 % (1191418)------------------------------ % 117.07/17.74 % (1191418)------------------------------ % 117.07/17.74 % (1191420)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4075269567:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 117.07/17.74 % (1191355)Instruction limit reached! % 117.07/17.74 % (1191355)------------------------------ % 117.07/17.74 % (1191355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.07/17.74 % (1191355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.07/17.74 % (1191355)CaDiCaL version: 2.1.3 % 117.07/17.74 % (1191355)Termination reason: Instruction limit % 117.07/17.74 % (1191355)Termination phase: Saturation % 117.07/17.74 % (1191355)Time elapsed: 2.012 s % 117.07/17.74 % (1191355)Peak memory usage: 31 MB % 117.07/17.74 % (1191355)Instructions burned: 3774 (million) % 117.07/17.74 % (1191422)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3239728378:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 117.07/17.74 % (1191235)Instruction limit reached! % 117.07/17.74 % (1191235)------------------------------ % 117.07/17.74 % (1191235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.07/17.74 % (1191235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.07/17.74 % (1191235)CaDiCaL version: 2.1.3 % 117.07/17.74 % (1191235)Termination reason: Instruction limit % 117.07/17.74 % (1191235)Termination phase: Saturation % 117.07/17.74 % (1191235)Time elapsed: 3.177 s % 117.07/17.74 % (1191235)Peak memory usage: 30 MB % 117.07/17.74 % (1191235)Instructions burned: 5114 (million) % 117.07/17.74 % (1191424)dis+10_16:1_sil=16000:random_seed=2490365656:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 125.61/18.17 % (1191412)Instruction limit reached! % 125.61/18.17 % (1191412)------------------------------ % 125.61/18.17 % (1191412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.61/18.17 % (1191412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.61/18.17 % (1191412)CaDiCaL version: 2.1.3 % 125.61/18.17 % (1191412)Termination reason: Instruction limit % 125.61/18.17 % (1191412)Termination phase: Saturation % 125.61/18.17 % (1191412)Time elapsed: 2.810 s % 125.61/18.17 % (1191412)Peak memory usage: 52 MB % 125.61/18.17 % (1191412)Instructions burned: 5212 (million) % 125.61/18.17 % (1191426)ott-3_8_sil=64000:random_seed=1945465315:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi) % 125.61/18.17 % (1191420)Instruction limit reached! % 125.61/18.17 % (1191420)------------------------------ % 125.61/18.17 % (1191420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.61/18.17 % (1191420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.61/18.17 % (1191420)CaDiCaL version: 2.1.3 % 125.61/18.17 % (1191420)Termination reason: Instruction limit % 125.61/18.17 % (1191420)Termination phase: Saturation % 125.61/18.17 % (1191420)Time elapsed: 5.100 s % 125.61/18.17 % (1191420)Peak memory usage: 77 MB % 125.61/18.17 % (1191420)Instructions burned: 22567 (million) % 125.61/18.17 % (1191428)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2436782701:fmbsr=2:i=32576_2916 on theBenchmark for (2916ds/32576Mi) % 125.61/18.17 % (1191428)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 125.61/18.17 % (1191428)Terminated due to inappropriate strategy. % 125.61/18.17 % (1191428)------------------------------ % 125.61/18.17 % (1191428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.61/18.17 % (1191428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.61/18.17 % (1191428)CaDiCaL version: 2.1.3 % 125.61/18.17 % (1191428)Termination reason: Inappropriate % 125.61/18.17 % (1191428)Time elapsed: 0.0000 s % 125.61/18.17 % (1191428)Peak memory usage: 10 MB % 125.61/18.17 % (1191428)------------------------------ % 125.61/18.17 % (1191428)------------------------------ % 125.61/18.17 % (1191430)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=535583030:i=11404_2916 on theBenchmark for (2916ds/11404Mi) % 125.61/18.17 % (1191422)Instruction limit reached! % 125.61/18.17 % (1191422)------------------------------ % 125.61/18.17 % (1191422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.61/18.17 % (1191422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.61/18.17 % (1191422)CaDiCaL version: 2.1.3 % 125.61/18.17 % (1191422)Termination reason: Instruction limit % 125.61/18.17 % (1191422)Termination phase: Saturation % 125.61/18.17 % (1191422)Time elapsed: 5.224 s % 125.61/18.17 % (1191422)Peak memory usage: 45 MB % 125.61/18.17 % (1191422)Instructions burned: 8174 (million) % 125.61/18.17 % (1191432)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1918898525:i=14134_2915 on theBenchmark for (2915ds/14134Mi) % 125.61/18.17 % (1191424)Instruction limit reached! % 125.61/18.17 % (1191424)------------------------------ % 125.61/18.17 % (1191424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.61/18.17 % (1191424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.61/18.17 % (1191424)CaDiCaL version: 2.1.3 % 125.61/18.17 % (1191424)Termination reason: Instruction limit % 125.61/18.17 % (1191424)Termination phase: Saturation % 125.61/18.17 % (1191424)Time elapsed: 4.806 s % 125.61/18.17 % (1191424)Peak memory usage: 56 MB % 125.61/18.17 % (1191424)Instructions burned: 9155 (million) % 125.61/18.17 % (1191434)dis+33_16_sil=32000:sac=on:random_seed=2514507271:i=15851:nm=0_2912 on theBenchmark for (2912ds/15851Mi) % 125.61/18.17 % (1191430)Instruction limit reached! % 125.61/18.17 % (1191430)------------------------------ % 125.61/18.17 % (1191430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.61/18.17 % (1191430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.61/18.17 % (1191430)CaDiCaL version: 2.1.3 % 125.61/18.17 % (1191430)Termination reason: Instruction limit % 125.61/18.17 % (1191430)Termination phase: Saturation % 125.61/18.17 % (1191430)Time elapsed: 4.057 s % 125.61/18.17 % (1191430)Peak memory usage: 45 MB % 125.61/18.17 % (1191430)Instructions burned: 11407 (million) % 125.61/18.17 % (1191436)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3536173147:avsq=on:i=17627:add=on:amm=off_2876 on theBenchmark for (2876ds/17627Mi) % 125.61/18.17 % (1191426)Instruction limit reached! % 125.61/18.17 % (1191426)------------------------------ % 132.69/19.14 % (1191426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.69/19.14 % (1191426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.69/19.14 % (1191426)CaDiCaL version: 2.1.3 % 132.69/19.14 % (1191426)Termination reason: Instruction limit % 132.69/19.14 % (1191426)Termination phase: Saturation % 132.69/19.14 % (1191426)Time elapsed: 10.052 s % 132.69/19.14 % (1191426)Peak memory usage: 50 MB % 132.69/19.14 % (1191426)Instructions burned: 20141 (million) % 132.69/19.14 % (1191852)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=632375600:s2a=on:i=53295_2842 on theBenchmark for (2842ds/53295Mi) % 132.69/19.14 % (1191434)Instruction limit reached! % 132.69/19.14 % (1191434)------------------------------ % 132.69/19.14 % (1191434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.69/19.14 % (1191434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.69/19.14 % (1191434)CaDiCaL version: 2.1.3 % 132.69/19.14 % (1191434)Termination reason: Instruction limit % 132.69/19.14 % (1191434)Termination phase: Saturation % 132.69/19.14 % (1191434)Time elapsed: 7.911 s % 132.69/19.14 % (1191434)Peak memory usage: 142 MB % 132.69/19.14 % (1191434)Instructions burned: 15851 (million) % 132.69/19.14 % (1191854)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1112746578:i=26857:ins=20_2832 on theBenchmark for (2832ds/26857Mi) % 132.69/19.14 % (1191854)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.69/19.14 % (1191854)Terminated due to inappropriate strategy. % 132.69/19.14 % (1191854)------------------------------ % 132.69/19.14 % (1191854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.69/19.14 % (1191854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.69/19.14 % (1191854)CaDiCaL version: 2.1.3 % 132.69/19.14 % (1191854)Termination reason: Inappropriate % 132.69/19.14 % (1191854)Time elapsed: 0.0000 s % 132.69/19.14 % (1191854)Peak memory usage: 10 MB % 132.69/19.14 % (1191854)------------------------------ % 132.69/19.14 % (1191854)------------------------------ % 132.69/19.14 % (1191856)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3297967479:i=28120:bs=on:fsr=off_2832 on theBenchmark for (2832ds/28120Mi) % 132.69/19.14 % (1191436)Instruction limit reached! % 132.69/19.14 % (1191436)------------------------------ % 132.69/19.14 % (1191436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.69/19.14 % (1191436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.69/19.14 % (1191436)CaDiCaL version: 2.1.3 % 132.69/19.14 % (1191436)Termination reason: Instruction limit % 132.69/19.14 % (1191436)Termination phase: Saturation % 132.69/19.14 % (1191436)Time elapsed: 4.865 s % 132.69/19.14 % (1191436)Peak memory usage: 185 MB % 132.69/19.14 % (1191436)Instructions burned: 17630 (million) % 132.69/19.14 % (1191858)fmb+10_1_sil=256000:fmbss=7:random_seed=724994561:fmbsr=1.6:i=182295_2827 on theBenchmark for (2827ds/182295Mi) % 132.69/19.14 % (1191858)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.69/19.14 % (1191858)Terminated due to inappropriate strategy. % 132.69/19.14 % (1191858)------------------------------ % 132.69/19.14 % (1191858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.69/19.14 % (1191858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.69/19.14 % (1191858)CaDiCaL version: 2.1.3 % 132.69/19.14 % (1191858)Termination reason: Inappropriate % 132.69/19.14 % (1191858)Time elapsed: 0.0000 s % 132.69/19.14 % (1191858)Peak memory usage: 10 MB % 132.69/19.14 % (1191858)------------------------------ % 132.69/19.14 % (1191858)------------------------------ % 132.69/19.14 % (1191860)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1221872687:i=44625:gsp=on_2826 on theBenchmark for (2826ds/44625Mi) % 132.69/19.14 % (1191860)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 132.69/19.14 % (1191860)Terminated due to inappropriate strategy. % 132.69/19.14 % (1191860)------------------------------ % 132.69/19.14 % (1191860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 132.69/19.14 % (1191860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.69/19.14 % (1191860)CaDiCaL version: 2.1.3 % 132.69/19.14 % (1191860)Termination reason: Inappropriate % 132.69/19.14 % (1191860)Time elapsed: 0.0000 s % 132.69/19.14 % (1191860)Peak memory usage: 10 MB % 132.69/19.14 % (1191860)------------------------------ % 132.69/19.14 % (1191860)------------------------------ % 132.69/19.14 % (1191862)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3955660469:i=160505_2826 on theBenchmark for (2826ds/160505Mi) % 156.56/22.53 % (1191862)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.56/22.53 % (1191862)Terminated due to inappropriate strategy. % 156.56/22.53 % (1191862)------------------------------ % 156.56/22.53 % (1191862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.56/22.53 % (1191862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.56/22.53 % (1191862)CaDiCaL version: 2.1.3 % 156.56/22.53 % (1191862)Termination reason: Inappropriate % 156.56/22.53 % (1191862)Time elapsed: 0.0000 s % 156.56/22.53 % (1191862)Peak memory usage: 10 MB % 156.56/22.53 % (1191862)------------------------------ % 156.56/22.53 % (1191862)------------------------------ % 156.56/22.53 % (1191864)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3291388830:fmbsr=1.3:i=225729_2826 on theBenchmark for (2826ds/225729Mi) % 156.56/22.53 % (1191864)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.56/22.53 % (1191864)Terminated due to inappropriate strategy. % 156.56/22.53 % (1191864)------------------------------ % 156.56/22.53 % (1191864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.56/22.53 % (1191864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.56/22.53 % (1191864)CaDiCaL version: 2.1.3 % 156.56/22.53 % (1191864)Termination reason: Inappropriate % 156.56/22.53 % (1191864)Time elapsed: 0.0000 s % 156.56/22.53 % (1191864)Peak memory usage: 10 MB % 156.56/22.53 % (1191864)------------------------------ % 156.56/22.53 % (1191864)------------------------------ % 156.56/22.53 % (1191866)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3614774954:fmbsr=2:i=185024:ins=7_2826 on theBenchmark for (2826ds/185024Mi) % 156.56/22.53 % (1191866)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.56/22.53 % (1191866)Terminated due to inappropriate strategy. % 156.56/22.53 % (1191866)------------------------------ % 156.56/22.53 % (1191866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.56/22.53 % (1191866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.56/22.53 % (1191866)CaDiCaL version: 2.1.3 % 156.56/22.53 % (1191866)Termination reason: Inappropriate % 156.56/22.53 % (1191866)Time elapsed: 0.0000 s % 156.56/22.53 % (1191866)Peak memory usage: 10 MB % 156.56/22.53 % (1191866)------------------------------ % 156.56/22.53 % (1191866)------------------------------ % 156.56/22.53 % (1191868)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3615859425:rtra=on_2826 on theBenchmark for (2826ds/0Mi) % 156.56/22.53 % (1191868)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.56/22.53 % (1191868)Terminated due to inappropriate strategy. % 156.56/22.53 % (1191868)------------------------------ % 156.56/22.53 % (1191868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.56/22.53 % (1191868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.56/22.53 % (1191868)CaDiCaL version: 2.1.3 % 156.56/22.53 % (1191868)Termination reason: Inappropriate % 156.56/22.53 % (1191868)Time elapsed: 0.0000 s % 156.56/22.53 % (1191868)Peak memory usage: 10 MB % 156.56/22.53 % (1191868)------------------------------ % 156.56/22.53 % (1191868)------------------------------ % 156.56/22.53 % (1191870)% WARNING: option uhcvi not known. % 156.56/22.53 % (1191870)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2589565883:i=271062:add=off:rtra=on:rawr=on_2826 on theBenchmark for (2826ds/271062Mi) % 156.56/22.53 % (1191410)Instruction limit reached! % 156.56/22.53 % (1191410)------------------------------ % 156.56/22.53 % (1191410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.56/22.53 % (1191410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.56/22.53 % (1191410)CaDiCaL version: 2.1.3 % 156.56/22.53 % (1191410)Termination reason: Instruction limit % 156.56/22.53 % (1191410)Termination phase: Saturation % 156.56/22.53 % (1191410)Time elapsed: 15.154 s % 156.56/22.53 % (1191410)Peak memory usage: 129 MB % 156.56/22.53 % (1191410)Instructions burned: 29342 (million) % 156.56/22.53 % (1191872)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3798599493:i=176048:add=on:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/176048Mi) % 156.56/22.53 % (1191432)Instruction limit reached! % 156.56/22.53 % (1191432)------------------------------ % 156.56/22.53 % (1191432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.35/24.38 % (1191432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.35/24.38 % (1191432)CaDiCaL version: 2.1.3 % 169.35/24.38 % (1191432)Termination reason: Instruction limit % 169.35/24.38 % (1191432)Termination phase: Saturation % 169.35/24.38 % (1191432)Time elapsed: 9.279 s % 169.35/24.38 % (1191432)Peak memory usage: 51 MB % 169.35/24.38 % (1191432)Instructions burned: 14135 (million) % 169.35/24.38 % (1191874)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1933309156:i=206:fgj=on:rtra=on_2822 on theBenchmark for (2822ds/206Mi) % 169.35/24.38 % (1191874)Instruction limit reached! % 169.35/24.38 % (1191874)------------------------------ % 169.35/24.38 % (1191874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.35/24.38 % (1191874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.35/24.38 % (1191874)CaDiCaL version: 2.1.3 % 169.35/24.38 % (1191874)Termination reason: Instruction limit % 169.35/24.38 % (1191874)Termination phase: Saturation % 169.35/24.38 % (1191874)Time elapsed: 0.133 s % 169.35/24.38 % (1191874)Peak memory usage: 13 MB % 169.35/24.38 % (1191874)Instructions burned: 207 (million) % 169.35/24.38 % (1191876)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3675710637:i=232:rtra=on_2820 on theBenchmark for (2820ds/232Mi) % 169.35/24.38 % (1191876)Instruction limit reached! % 169.35/24.38 % (1191876)------------------------------ % 169.35/24.38 % (1191876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.35/24.38 % (1191876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.35/24.38 % (1191876)CaDiCaL version: 2.1.3 % 169.35/24.38 % (1191876)Termination reason: Instruction limit % 169.35/24.38 % (1191876)Termination phase: Saturation % 169.35/24.38 % (1191876)Time elapsed: 0.149 s % 169.35/24.38 % (1191876)Peak memory usage: 13 MB % 169.35/24.38 % (1191876)Instructions burned: 232 (million) % 169.35/24.38 % (1191878)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=497910447:i=262:rtra=on_2819 on theBenchmark for (2819ds/262Mi) % 169.35/24.38 % (1191878)Instruction limit reached! % 169.35/24.38 % (1191878)------------------------------ % 169.35/24.38 % (1191878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.35/24.38 % (1191878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.35/24.38 % (1191878)CaDiCaL version: 2.1.3 % 169.35/24.38 % (1191878)Termination reason: Instruction limit % 169.35/24.38 % (1191878)Termination phase: Saturation % 169.35/24.38 % (1191878)Time elapsed: 0.163 s % 169.35/24.38 % (1191878)Peak memory usage: 13 MB % 169.35/24.38 % (1191878)Instructions burned: 263 (million) % 169.35/24.38 % (1191880)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3409158335:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2817 on theBenchmark for (2817ds/318Mi) % 169.35/24.38 % (1191880)Instruction limit reached! % 169.35/24.38 % (1191880)------------------------------ % 169.35/24.38 % (1191880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.35/24.38 % (1191880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.35/24.38 % (1191880)CaDiCaL version: 2.1.3 % 169.35/24.38 % (1191880)Termination reason: Instruction limit % 169.35/24.38 % (1191880)Termination phase: Saturation % 169.35/24.38 % (1191880)Time elapsed: 0.222 s % 169.35/24.38 % (1191880)Peak memory usage: 14 MB % 169.35/24.38 % (1191880)Instructions burned: 319 (million) % 169.35/24.38 % (1191882)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3913911976:i=1428:nm=2:rtra=on_2814 on theBenchmark for (2814ds/1428Mi) % 169.35/24.38 % (1191882)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 169.35/24.38 % (1191882)Terminated due to inappropriate strategy. % 169.35/24.38 % (1191882)------------------------------ % 169.35/24.38 % (1191882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.35/24.38 % (1191882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.35/24.38 % (1191882)CaDiCaL version: 2.1.3 % 169.35/24.38 % (1191882)Termination reason: Inappropriate % 169.35/24.38 % (1191882)Time elapsed: 0.0000 s % 169.35/24.38 % (1191882)Peak memory usage: 10 MB % 169.35/24.38 % (1191882)------------------------------ % 169.35/24.38 % (1191882)------------------------------ % 169.35/24.38 % (1191884)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2550656852:i=262:bd=preordered:rtra=on:fsd=on_2814 on theBenchmark for (2814ds/262Mi) % 169.35/24.38 % (1191884)Instruction limit reached! % 169.35/24.38 % (1191884)------------------------------ % 169.35/24.38 % (1191884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.16/31.61 % (1191884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.16/31.61 % (1191884)CaDiCaL version: 2.1.3 % 221.16/31.61 % (1191884)Termination reason: Instruction limit % 221.16/31.61 % (1191884)Termination phase: Saturation % 221.16/31.61 % (1191884)Time elapsed: 0.176 s % 221.16/31.61 % (1191884)Peak memory usage: 14 MB % 221.16/31.61 % (1191884)Instructions burned: 262 (million) % 221.16/31.61 % (1191886)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=2162448156:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2812 on theBenchmark for (2812ds/1368Mi) % 221.16/31.61 % (1191886)Instruction limit reached! % 221.16/31.61 % (1191886)------------------------------ % 221.16/31.61 % (1191886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.16/31.61 % (1191886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.16/31.61 % (1191886)CaDiCaL version: 2.1.3 % 221.16/31.61 % (1191886)Termination reason: Instruction limit % 221.16/31.61 % (1191886)Termination phase: Saturation % 221.16/31.61 % (1191886)Time elapsed: 0.835 s % 221.16/31.61 % (1191886)Peak memory usage: 23 MB % 221.16/31.61 % (1191886)Instructions burned: 1368 (million) % 221.16/31.61 % (1191888)ott-21_1_sil=16000:si=on:fs=off:random_seed=3679300459:i=360:av=off:fsr=off:rtra=on_2804 on theBenchmark for (2804ds/360Mi) % 221.16/31.61 % (1191888)Instruction limit reached! % 221.16/31.61 % (1191888)------------------------------ % 221.16/31.61 % (1191888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.16/31.61 % (1191888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.16/31.61 % (1191888)CaDiCaL version: 2.1.3 % 221.16/31.61 % (1191888)Termination reason: Instruction limit % 221.16/31.61 % (1191888)Termination phase: Saturation % 221.16/31.61 % (1191888)Time elapsed: 0.160 s % 221.16/31.61 % (1191888)Peak memory usage: 12 MB % 221.16/31.61 % (1191888)Instructions burned: 362 (million) % 221.16/31.61 % (1191890)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=685514749:i=954:bd=all:rtra=on_2802 on theBenchmark for (2802ds/954Mi) % 221.16/31.61 % (1191890)Instruction limit reached! % 221.16/31.61 % (1191890)------------------------------ % 221.16/31.61 % (1191890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.16/31.61 % (1191890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.16/31.61 % (1191890)CaDiCaL version: 2.1.3 % 221.16/31.61 % (1191890)Termination reason: Instruction limit % 221.16/31.61 % (1191890)Termination phase: Saturation % 221.16/31.61 % (1191890)Time elapsed: 0.626 s % 221.16/31.61 % (1191890)Peak memory usage: 16 MB % 221.16/31.61 % (1191890)Instructions burned: 955 (million) % 221.16/31.61 % (1191892)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1148332316:fmbsr=1.3:i=1730:ins=25:rtra=on_2795 on theBenchmark for (2795ds/1730Mi) % 221.16/31.61 % (1191892)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 221.16/31.61 % (1191892)Terminated due to inappropriate strategy. % 221.16/31.61 % (1191892)------------------------------ % 221.16/31.61 % (1191892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.16/31.61 % (1191892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.16/31.61 % (1191892)CaDiCaL version: 2.1.3 % 221.16/31.61 % (1191892)Termination reason: Inappropriate % 221.16/31.61 % (1191892)Time elapsed: 0.0000 s % 221.16/31.61 % (1191892)Peak memory usage: 10 MB % 221.16/31.61 % (1191892)------------------------------ % 221.16/31.61 % (1191892)------------------------------ % 221.16/31.61 % (1191894)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=194319846:i=2358:rtra=on_2795 on theBenchmark for (2795ds/2358Mi) % 221.16/31.61 % (1191894)Instruction limit reached! % 221.16/31.61 % (1191894)------------------------------ % 221.16/31.61 % (1191894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.16/31.61 % (1191894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.16/31.61 % (1191894)CaDiCaL version: 2.1.3 % 221.16/31.61 % (1191894)Termination reason: Instruction limit % 221.16/31.61 % (1191894)Termination phase: Saturation % 221.16/31.61 % (1191894)Time elapsed: 1.643 s % 221.16/31.61 % (1191894)Peak memory usage: 23 MB % 221.16/31.61 % (1191894)Instructions burned: 2358 (million) % 221.16/31.61 % (1191896)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2803475403:i=1778:ins=1:rtra=on_2779 on theBenchmark for (2779ds/1778Mi) % 221.16/31.61 % (1191896)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.28/38.89 % (1191896)Terminated due to inappropriate strategy. % 272.28/38.89 % (1191896)------------------------------ % 272.28/38.89 % (1191896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.28/38.89 % (1191896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.28/38.89 % (1191896)CaDiCaL version: 2.1.3 % 272.28/38.89 % (1191896)Termination reason: Inappropriate % 272.28/38.89 % (1191896)Time elapsed: 0.0000 s % 272.28/38.89 % (1191896)Peak memory usage: 10 MB % 272.28/38.89 % (1191896)------------------------------ % 272.28/38.89 % (1191896)------------------------------ % 272.28/38.89 % (1191898)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=4193569289:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2778 on theBenchmark for (2778ds/1384Mi) % 272.28/38.89 % (1191898)Instruction limit reached! % 272.28/38.89 % (1191898)------------------------------ % 272.28/38.89 % (1191898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.28/38.89 % (1191898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.28/38.89 % (1191898)CaDiCaL version: 2.1.3 % 272.28/38.89 % (1191898)Termination reason: Instruction limit % 272.28/38.89 % (1191898)Termination phase: Saturation % 272.28/38.89 % (1191898)Time elapsed: 0.746 s % 272.28/38.89 % (1191898)Peak memory usage: 17 MB % 272.28/38.89 % (1191898)Instructions burned: 1384 (million) % 272.28/38.89 % (1191900)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1480113578:i=1758:kws=inv_precedence:fsr=off:rtra=on_2771 on theBenchmark for (2771ds/1758Mi) % 272.28/38.89 % (1191900)Instruction limit reached! % 272.28/38.89 % (1191900)------------------------------ % 272.28/38.89 % (1191900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.28/38.89 % (1191900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.28/38.89 % (1191900)CaDiCaL version: 2.1.3 % 272.28/38.89 % (1191900)Termination reason: Instruction limit % 272.28/38.89 % (1191900)Termination phase: Saturation % 272.28/38.89 % (1191900)Time elapsed: 0.993 s % 272.28/38.89 % (1191900)Peak memory usage: 28 MB % 272.28/38.89 % (1191900)Instructions burned: 1759 (million) % 272.28/38.89 % (1191902)fmb+10_1_sil=64000:si=on:random_seed=4198855459:i=44122:nm=2:rtra=on:gsp=on_2761 on theBenchmark for (2761ds/44122Mi) % 272.28/38.89 % (1191902)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.28/38.89 % (1191902)Terminated due to inappropriate strategy. % 272.28/38.89 % (1191902)------------------------------ % 272.28/38.89 % (1191902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.28/38.89 % (1191902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.28/38.89 % (1191902)CaDiCaL version: 2.1.3 % 272.28/38.89 % (1191902)Termination reason: Inappropriate % 272.28/38.89 % (1191902)Time elapsed: 0.0000 s % 272.28/38.89 % (1191902)Peak memory usage: 10 MB % 272.28/38.89 % (1191902)------------------------------ % 272.28/38.89 % (1191902)------------------------------ % 272.28/38.89 % (1191904)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1253766841:i=19030:nm=5:rtra=on_2760 on theBenchmark for (2760ds/19030Mi) % 272.28/38.89 % (1191904)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.28/38.89 % (1191904)Terminated due to inappropriate strategy. % 272.28/38.89 % (1191904)------------------------------ % 272.28/38.89 % (1191904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.28/38.89 % (1191904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.28/38.89 % (1191904)CaDiCaL version: 2.1.3 % 272.28/38.89 % (1191904)Termination reason: Inappropriate % 272.28/38.89 % (1191904)Time elapsed: 0.0000 s % 272.28/38.89 % (1191904)Peak memory usage: 10 MB % 272.28/38.89 % (1191904)------------------------------ % 272.28/38.89 % (1191904)------------------------------ % 272.28/38.89 % (1191906)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=183266630:fmbsr=1.7:i=1840:rtra=on_2760 on theBenchmark for (2760ds/1840Mi) % 272.28/38.89 % (1191906)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 272.28/38.89 % (1191906)Terminated due to inappropriate strategy. % 272.28/38.89 % (1191906)------------------------------ % 272.28/38.89 % (1191906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 272.28/38.89 % (1191906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.70/41.42 % (1191906)CaDiCaL version: 2.1.3 % 290.70/41.42 % (1191906)Termination reason: Inappropriate % 290.70/41.42 % (1191906)Time elapsed: 0.0000 s % 290.70/41.42 % (1191906)Peak memory usage: 10 MB % 290.70/41.42 % (1191906)------------------------------ % 290.70/41.42 % (1191906)------------------------------ % 290.70/41.42 % (1191908)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=4138870112:i=10262:rtra=on_2760 on theBenchmark for (2760ds/10262Mi) % 290.70/41.42 % (1191856)Instruction limit reached! % 290.70/41.42 % (1191856)------------------------------ % 290.70/41.42 % (1191856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.70/41.42 % (1191856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.70/41.42 % (1191856)CaDiCaL version: 2.1.3 % 290.70/41.42 % (1191856)Termination reason: Instruction limit % 290.70/41.42 % (1191856)Termination phase: Saturation % 290.70/41.42 % (1191856)Time elapsed: 11.989 s % 290.70/41.42 % (1191856)Peak memory usage: 26 MB % 290.70/41.42 % (1191856)Instructions burned: 28122 (million) % 290.70/41.42 % (1191920)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1865357587:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2712 on theBenchmark for (2712ds/2944Mi) % 290.70/41.42 % (1191908)Instruction limit reached! % 290.70/41.42 % (1191908)------------------------------ % 290.70/41.42 % (1191908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.70/41.42 % (1191908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.70/41.42 % (1191908)CaDiCaL version: 2.1.3 % 290.70/41.42 % (1191908)Termination reason: Instruction limit % 290.70/41.42 % (1191908)Termination phase: Saturation % 290.70/41.42 % (1191908)Time elapsed: 6.042 s % 290.70/41.42 % (1191908)Peak memory usage: 66 MB % 290.70/41.42 % (1191908)Instructions burned: 10263 (million) % 290.70/41.42 % (1192045)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1625805541:i=12648:rtra=on_2699 on theBenchmark for (2699ds/12648Mi) % 290.70/41.42 % (1192045)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.70/41.42 % (1192045)Terminated due to inappropriate strategy. % 290.70/41.42 % (1192045)------------------------------ % 290.70/41.42 % (1192045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.70/41.42 % (1192045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.70/41.42 % (1192045)CaDiCaL version: 2.1.3 % 290.70/41.42 % (1192045)Termination reason: Inappropriate % 290.70/41.42 % (1192045)Time elapsed: 0.0000 s % 290.70/41.42 % (1192045)Peak memory usage: 10 MB % 290.70/41.42 % (1192045)------------------------------ % 290.70/41.42 % (1192045)------------------------------ % 290.70/41.42 % (1192047)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2377820713:fmbsr=2.30978:i=4348:rtra=on_2699 on theBenchmark for (2699ds/4348Mi) % 290.70/41.42 % (1192047)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 290.70/41.42 % (1192047)Terminated due to inappropriate strategy. % 290.70/41.42 % (1192047)------------------------------ % 290.70/41.42 % (1192047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.70/41.42 % (1192047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.70/41.42 % (1192047)CaDiCaL version: 2.1.3 % 290.70/41.42 % (1192047)Termination reason: Inappropriate % 290.70/41.42 % (1192047)Time elapsed: 0.0000 s % 290.70/41.42 % (1192047)Peak memory usage: 10 MB % 290.70/41.42 % (1192047)------------------------------ % 290.70/41.42 % (1192047)------------------------------ % 290.70/41.42 % (1192049)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2000678411:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2699 on theBenchmark for (2699ds/1738Mi) % 290.70/41.42 % (1191920)Instruction limit reached! % 290.70/41.42 % (1191920)------------------------------ % 290.70/41.42 % (1191920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.70/41.42 % (1191920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.70/41.42 % (1191920)CaDiCaL version: 2.1.3 % 290.70/41.42 % (1191920)Termination reason: Instruction limit % 290.70/41.42 % (1191920)Termination phase: Saturation % 290.70/41.42 % (1191920)Time elapsed: 1.310 s % 290.70/41.42 % (1191920)Peak memory usage: 27 MB % 290.70/41.42 % (1191920)Instructions burned: 2948 (million) % 290.70/41.42 % (1192062)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3104855330:i=10228:av=off:rtra=on_2698 on theBenchmark for (2698ds/10228Mi) % 290.70/41.42 % (1192049)ITerminated % 300.67/42.84 % Vampire exiting % 300.67/42.84 Terminated %------------------------------------------------------------------------------