%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW646_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 : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:35 PM UTC 2026 % Result : Timeout 300.52s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW646_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.26 % Computer : n003.cluster.edu % 0.11/0.26 % Model : x86_64 x86_64 % 0.11/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.26 % Memory : 8046.5625MB % 0.11/0.26 % OS : Linux 6.8.0-71-generic % 0.11/0.27 % CPULimit : 300 % 0.11/0.27 % WCLimit : 300 % 0.11/0.27 % DateTime : Mon Sep 28 14:25:12 UTC 2026 % 0.27/0.27 % CPUTime : % 0.27/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.27/0.31 Running first-order model finding % 0.27/0.31 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 % 6.96/1.36 % (1623108)Will run a generic schedule for satisfiability detection. % 6.96/1.36 % (1623113)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3571793427_2999 on theBenchmark for (2999ds/0Mi) % 6.96/1.36 % (1623114)% WARNING: option uhcvi not known. % 6.96/1.36 % (1623113)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.96/1.36 % (1623113)Terminated due to inappropriate strategy. % 6.96/1.36 % (1623113)------------------------------ % 6.96/1.36 % (1623113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.96/1.36 % (1623113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.36 % (1623113)CaDiCaL version: 2.1.3 % 6.96/1.36 % (1623113)Termination reason: Inappropriate % 6.96/1.36 % (1623113)Time elapsed: 0.008 s % 6.96/1.36 % (1623113)Peak memory usage: 11 MB % 6.96/1.36 % (1623113)Instructions burned: 16 (million) % 6.96/1.36 % (1623113)------------------------------ % 6.96/1.36 % (1623113)------------------------------ % 6.96/1.36 % (1623118)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1391001637:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.96/1.36 % (1623117)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4246566551:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.96/1.36 % (1623114)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=950858332:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.96/1.36 % (1623119)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2836515313:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.96/1.36 % (1623115)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1747327564:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.96/1.36 % (1623116)dis+10_1_sil=32000:sp=arity:random_seed=3008978139:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.96/1.36 % (1623121)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1316646616:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.96/1.36 % (1623121)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.96/1.36 % (1623121)Terminated due to inappropriate strategy. % 6.96/1.36 % (1623121)------------------------------ % 6.96/1.36 % (1623121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.96/1.36 % (1623121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.36 % (1623121)CaDiCaL version: 2.1.3 % 6.96/1.36 % (1623121)Termination reason: Inappropriate % 6.96/1.36 % (1623121)Time elapsed: 0.006 s % 6.96/1.36 % (1623121)Peak memory usage: 11 MB % 6.96/1.36 % (1623121)Instructions burned: 12 (million) % 6.96/1.36 % (1623121)------------------------------ % 6.96/1.36 % (1623121)------------------------------ % 6.96/1.36 % (1623129)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1640567777:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.96/1.36 % (1623116)Instruction limit reached! % 6.96/1.36 % (1623116)------------------------------ % 6.96/1.36 % (1623116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.96/1.36 % (1623116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.36 % (1623116)CaDiCaL version: 2.1.3 % 6.96/1.36 % (1623116)Termination reason: Instruction limit % 6.96/1.36 % (1623116)Termination phase: Saturation % 6.96/1.36 % (1623116)Time elapsed: 0.102 s % 6.96/1.36 % (1623116)Peak memory usage: 13 MB % 6.96/1.36 % (1623116)Instructions burned: 103 (million) % 6.96/1.36 % (1623117)Instruction limit reached! % 6.96/1.36 % (1623117)------------------------------ % 6.96/1.36 % (1623117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.96/1.36 % (1623117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.36 % (1623117)CaDiCaL version: 2.1.3 % 6.96/1.36 % (1623117)Termination reason: Instruction limit % 6.96/1.36 % (1623117)Termination phase: Saturation % 6.96/1.36 % (1623117)Time elapsed: 0.117 s % 6.96/1.36 % (1623117)Peak memory usage: 13 MB % 6.96/1.36 % (1623117)Instructions burned: 117 (million) % 6.96/1.36 % (1623129)Instruction limit reached! % 6.96/1.36 % (1623129)------------------------------ % 6.96/1.36 % (1623129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.96/1.36 % (1623129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.36 % (1623129)CaDiCaL version: 2.1.3 % 6.96/1.36 % (1623129)Termination reason: Instruction limit % 9.36/1.82 % (1623129)Termination phase: Saturation % 9.36/1.82 % (1623129)Time elapsed: 0.081 s % 9.36/1.82 % (1623129)Peak memory usage: 13 MB % 9.36/1.82 % (1623129)Instructions burned: 131 (million) % 9.36/1.82 % (1623118)Instruction limit reached! % 9.36/1.82 % (1623118)------------------------------ % 9.36/1.82 % (1623118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.36/1.82 % (1623118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.36/1.82 % (1623118)CaDiCaL version: 2.1.3 % 9.36/1.82 % (1623118)Termination reason: Instruction limit % 9.36/1.82 % (1623118)Termination phase: Saturation % 9.36/1.82 % (1623118)Time elapsed: 0.134 s % 9.36/1.82 % (1623118)Peak memory usage: 13 MB % 9.36/1.82 % (1623118)Instructions burned: 131 (million) % 9.36/1.82 % (1623131)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=1945739515:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 9.36/1.82 % (1623133)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2990408178:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 9.36/1.82 % (1623132)ott-21_1_sil=16000:fs=off:random_seed=1138804034:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 9.36/1.82 % (1623134)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1891753170:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 9.36/1.82 % (1623134)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.36/1.82 % (1623134)Terminated due to inappropriate strategy. % 9.36/1.82 % (1623134)------------------------------ % 9.36/1.82 % (1623134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.36/1.82 % (1623134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.36/1.82 % (1623134)CaDiCaL version: 2.1.3 % 9.36/1.82 % (1623134)Termination reason: Inappropriate % 9.36/1.82 % (1623134)Time elapsed: 0.007 s % 9.36/1.82 % (1623134)Peak memory usage: 11 MB % 9.36/1.82 % (1623134)Instructions burned: 13 (million) % 9.36/1.82 % (1623134)------------------------------ % 9.36/1.82 % (1623134)------------------------------ % 9.36/1.82 % (1623119)Instruction limit reached! % 9.36/1.82 % (1623119)------------------------------ % 9.36/1.82 % (1623119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.36/1.82 % (1623119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.36/1.82 % (1623119)CaDiCaL version: 2.1.3 % 9.36/1.82 % (1623119)Termination reason: Instruction limit % 9.36/1.82 % (1623119)Termination phase: Saturation % 9.36/1.82 % (1623119)Time elapsed: 0.185 s % 9.36/1.82 % (1623119)Peak memory usage: 14 MB % 9.36/1.82 % (1623119)Instructions burned: 159 (million) % 9.36/1.82 % (1623139)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1472169731:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 9.36/1.82 % (1623140)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=959775448:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 9.36/1.82 % (1623140)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 9.36/1.82 % (1623140)Terminated due to inappropriate strategy. % 9.36/1.82 % (1623140)------------------------------ % 9.36/1.82 % (1623140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.36/1.82 % (1623140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.36/1.82 % (1623140)CaDiCaL version: 2.1.3 % 9.36/1.82 % (1623140)Termination reason: Inappropriate % 9.36/1.82 % (1623140)Time elapsed: 0.012 s % 9.36/1.82 % (1623140)Peak memory usage: 11 MB % 9.36/1.82 % (1623140)Instructions burned: 12 (million) % 9.36/1.82 % (1623140)------------------------------ % 9.36/1.82 % (1623140)------------------------------ % 9.36/1.82 % (1623143)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=3329706392: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) % 9.36/1.82 % (1623132)Instruction limit reached! % 9.36/1.82 % (1623132)------------------------------ % 9.36/1.82 % (1623132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.36/1.82 % (1623132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.36/1.82 % (1623132)CaDiCaL version: 2.1.3 % 9.36/1.82 % (1623132)Termination reason: Instruction limit % 9.36/1.82 % (1623132)Termination phase: Saturation % 34.68/5.23 % (1623132)Time elapsed: 0.169 s % 34.68/5.23 % (1623132)Peak memory usage: 12 MB % 34.68/5.23 % (1623132)Instructions burned: 180 (million) % 34.68/5.23 % (1623145)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3470446971:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 34.68/5.23 % (1623133)Instruction limit reached! % 34.68/5.23 % (1623133)------------------------------ % 34.68/5.23 % (1623133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.68/5.23 % (1623133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.68/5.23 % (1623133)CaDiCaL version: 2.1.3 % 34.68/5.23 % (1623133)Termination reason: Instruction limit % 34.68/5.23 % (1623133)Termination phase: Saturation % 34.68/5.23 % (1623133)Time elapsed: 0.206 s % 34.68/5.23 % (1623133)Peak memory usage: 13 MB % 34.68/5.23 % (1623133)Instructions burned: 478 (million) % 34.68/5.23 % (1623147)fmb+10_1_sil=64000:random_seed=2868603584:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 34.68/5.23 % (1623147)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.68/5.23 % (1623147)Terminated due to inappropriate strategy. % 34.68/5.23 % (1623147)------------------------------ % 34.68/5.23 % (1623147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.68/5.23 % (1623147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.68/5.23 % (1623147)CaDiCaL version: 2.1.3 % 34.68/5.23 % (1623147)Termination reason: Inappropriate % 34.68/5.23 % (1623147)Time elapsed: 0.007 s % 34.68/5.23 % (1623147)Peak memory usage: 11 MB % 34.68/5.23 % (1623147)Instructions burned: 12 (million) % 34.68/5.23 % (1623147)------------------------------ % 34.68/5.23 % (1623147)------------------------------ % 34.68/5.23 % (1623149)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=332979270:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 34.68/5.23 % (1623149)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.68/5.23 % (1623149)Terminated due to inappropriate strategy. % 34.68/5.23 % (1623149)------------------------------ % 34.68/5.23 % (1623149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.68/5.23 % (1623149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.68/5.23 % (1623149)CaDiCaL version: 2.1.3 % 34.68/5.23 % (1623149)Termination reason: Inappropriate % 34.68/5.23 % (1623149)Time elapsed: 0.007 s % 34.68/5.23 % (1623149)Peak memory usage: 11 MB % 34.68/5.23 % (1623149)Instructions burned: 12 (million) % 34.68/5.23 % (1623149)------------------------------ % 34.68/5.23 % (1623149)------------------------------ % 34.68/5.23 % (1623151)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4076163206:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 34.68/5.23 % (1623151)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.68/5.23 % (1623151)Terminated due to inappropriate strategy. % 34.68/5.23 % (1623151)------------------------------ % 34.68/5.23 % (1623151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.68/5.23 % (1623151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.68/5.23 % (1623151)CaDiCaL version: 2.1.3 % 34.68/5.23 % (1623151)Termination reason: Inappropriate % 34.68/5.23 % (1623151)Time elapsed: 0.008 s % 34.68/5.23 % (1623151)Peak memory usage: 11 MB % 34.68/5.23 % (1623151)Instructions burned: 12 (million) % 34.68/5.23 % (1623151)------------------------------ % 34.68/5.23 % (1623151)------------------------------ % 34.68/5.23 % (1623153)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4220716029:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 34.68/5.23 % (1623131)Instruction limit reached! % 34.68/5.23 % (1623131)------------------------------ % 34.68/5.23 % (1623131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.68/5.23 % (1623131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.68/5.23 % (1623131)CaDiCaL version: 2.1.3 % 34.68/5.23 % (1623131)Termination reason: Instruction limit % 34.68/5.23 % (1623131)Termination phase: Saturation % 34.68/5.23 % (1623131)Time elapsed: 0.681 s % 34.68/5.23 % (1623131)Peak memory usage: 18 MB % 34.68/5.23 % (1623131)Instructions burned: 684 (million) % 34.68/5.23 % (1623155)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=771103638:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 34.68/5.23 % (1623143)Instruction limit reached! % 34.68/5.23 % (1623143)------------------------------ % 39.04/5.95 % (1623143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.95 % (1623143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.95 % (1623143)CaDiCaL version: 2.1.3 % 39.04/5.95 % (1623143)Termination reason: Instruction limit % 39.04/5.95 % (1623143)Termination phase: Saturation % 39.04/5.95 % (1623143)Time elapsed: 0.736 s % 39.04/5.95 % (1623143)Peak memory usage: 22 MB % 39.04/5.95 % (1623143)Instructions burned: 692 (million) % 39.04/5.95 % (1623157)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2984215272:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 39.04/5.95 % (1623157)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.04/5.95 % (1623157)Terminated due to inappropriate strategy. % 39.04/5.95 % (1623157)------------------------------ % 39.04/5.95 % (1623157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.95 % (1623157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.95 % (1623157)CaDiCaL version: 2.1.3 % 39.04/5.95 % (1623157)Termination reason: Inappropriate % 39.04/5.95 % (1623157)Time elapsed: 0.011 s % 39.04/5.95 % (1623157)Peak memory usage: 11 MB % 39.04/5.95 % (1623157)Instructions burned: 15 (million) % 39.04/5.95 % (1623157)------------------------------ % 39.04/5.95 % (1623157)------------------------------ % 39.04/5.95 % (1623159)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3403818304:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 39.04/5.95 % (1623159)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.04/5.95 % (1623159)Terminated due to inappropriate strategy. % 39.04/5.95 % (1623159)------------------------------ % 39.04/5.95 % (1623159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.95 % (1623159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.95 % (1623159)CaDiCaL version: 2.1.3 % 39.04/5.95 % (1623159)Termination reason: Inappropriate % 39.04/5.95 % (1623159)Time elapsed: 0.009 s % 39.04/5.95 % (1623159)Peak memory usage: 11 MB % 39.04/5.95 % (1623159)Instructions burned: 12 (million) % 39.04/5.95 % (1623159)------------------------------ % 39.04/5.95 % (1623159)------------------------------ % 39.04/5.95 % (1623161)ott-2_1_sil=16000:newcnf=on:random_seed=4288558286:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi) % 39.04/5.95 % (1623145)Instruction limit reached! % 39.04/5.95 % (1623145)------------------------------ % 39.04/5.95 % (1623145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.95 % (1623145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.95 % (1623145)CaDiCaL version: 2.1.3 % 39.04/5.95 % (1623145)Termination reason: Instruction limit % 39.04/5.95 % (1623145)Termination phase: Saturation % 39.04/5.95 % (1623145)Time elapsed: 0.820 s % 39.04/5.95 % (1623145)Peak memory usage: 18 MB % 39.04/5.95 % (1623145)Instructions burned: 879 (million) % 39.04/5.95 % (1623163)ott+10_1_sil=32000:tgt=ground:random_seed=1142574967:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi) % 39.04/5.95 % (1623139)Instruction limit reached! % 39.04/5.95 % (1623139)------------------------------ % 39.04/5.95 % (1623139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.95 % (1623139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.95 % (1623139)CaDiCaL version: 2.1.3 % 39.04/5.95 % (1623139)Termination reason: Instruction limit % 39.04/5.95 % (1623139)Termination phase: Saturation % 39.04/5.95 % (1623139)Time elapsed: 1.205 s % 39.04/5.95 % (1623139)Peak memory usage: 23 MB % 39.04/5.95 % (1623139)Instructions burned: 1180 (million) % 39.04/5.95 % (1623165)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1116018271:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 39.04/5.95 % (1623165)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.04/5.95 % (1623165)Terminated due to inappropriate strategy. % 39.04/5.95 % (1623165)------------------------------ % 39.04/5.95 % (1623165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.04/5.95 % (1623165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.04/5.95 % (1623165)CaDiCaL version: 2.1.3 % 39.04/5.95 % (1623165)Termination reason: Inappropriate % 39.04/5.95 % (1623165)Time elapsed: 0.015 s % 39.04/5.95 % (1623165)Peak memory usage: 11 MB % 39.04/5.95 % (1623165)Instructions burned: 16 (million) % 127.11/18.20 % (1623165)------------------------------ % 127.11/18.20 % (1623165)------------------------------ % 127.11/18.20 % (1623167)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2507375057:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi) % 127.11/18.20 % (1623161)Instruction limit reached! % 127.11/18.20 % (1623161)------------------------------ % 127.11/18.20 % (1623161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.11/18.20 % (1623161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.11/18.20 % (1623161)CaDiCaL version: 2.1.3 % 127.11/18.20 % (1623161)Termination reason: Instruction limit % 127.11/18.20 % (1623161)Termination phase: Saturation % 127.11/18.20 % (1623161)Time elapsed: 0.858 s % 127.11/18.20 % (1623161)Peak memory usage: 16 MB % 127.11/18.20 % (1623161)Instructions burned: 870 (million) % 127.11/18.20 % (1623169)dis+21_1_sil=32000:sas=cadical:random_seed=2452479891:i=3773:amm=off_2980 on theBenchmark for (2980ds/3773Mi) % 127.11/18.20 % (1623155)Instruction limit reached! % 127.11/18.20 % (1623155)------------------------------ % 127.11/18.20 % (1623155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.11/18.20 % (1623155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.11/18.20 % (1623155)CaDiCaL version: 2.1.3 % 127.11/18.20 % (1623155)Termination reason: Instruction limit % 127.11/18.20 % (1623155)Termination phase: Saturation % 127.11/18.20 % (1623155)Time elapsed: 1.377 s % 127.11/18.20 % (1623155)Peak memory usage: 29 MB % 127.11/18.20 % (1623155)Instructions burned: 1473 (million) % 127.11/18.20 % (1623171)ott+11_1_sil=16000:gs=on:random_seed=485478415:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2977 on theBenchmark for (2977ds/2251Mi) % 127.11/18.20 % (1623153)Instruction limit reached! % 127.11/18.20 % (1623153)------------------------------ % 127.11/18.20 % (1623153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.11/18.20 % (1623153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.11/18.20 % (1623153)CaDiCaL version: 2.1.3 % 127.11/18.20 % (1623153)Termination reason: Instruction limit % 127.11/18.20 % (1623153)Termination phase: Saturation % 127.11/18.20 % (1623153)Time elapsed: 2.512 s % 127.11/18.20 % (1623153)Peak memory usage: 32 MB % 127.11/18.20 % (1623153)Instructions burned: 5133 (million) % 127.11/18.20 % (1623173)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2624514723:fmbsr=1.6:i=67534_2969 on theBenchmark for (2969ds/67534Mi) % 127.11/18.20 % (1623173)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.11/18.20 % (1623173)Terminated due to inappropriate strategy. % 127.11/18.20 % (1623173)------------------------------ % 127.11/18.20 % (1623173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.11/18.20 % (1623173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.11/18.20 % (1623173)CaDiCaL version: 2.1.3 % 127.11/18.20 % (1623173)Termination reason: Inappropriate % 127.11/18.20 % (1623173)Time elapsed: 0.007 s % 127.11/18.20 % (1623173)Peak memory usage: 11 MB % 127.11/18.20 % (1623173)Instructions burned: 12 (million) % 127.11/18.20 % (1623173)------------------------------ % 127.11/18.20 % (1623173)------------------------------ % 127.11/18.20 % (1623175)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3008496037:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2969 on theBenchmark for (2969ds/4591Mi) % 127.11/18.20 % (1623171)Instruction limit reached! % 127.11/18.20 % (1623171)------------------------------ % 127.11/18.20 % (1623171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.11/18.20 % (1623171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.11/18.20 % (1623171)CaDiCaL version: 2.1.3 % 127.11/18.20 % (1623171)Termination reason: Instruction limit % 127.11/18.20 % (1623171)Termination phase: Saturation % 127.11/18.20 % (1623171)Time elapsed: 2.220 s % 127.11/18.20 % (1623171)Peak memory usage: 23 MB % 127.11/18.20 % (1623171)Instructions burned: 2252 (million) % 127.11/18.20 % (1623177)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3486429025:i=29340_2954 on theBenchmark for (2954ds/29340Mi) % 127.11/18.20 % (1623167)Instruction limit reached! % 127.11/18.20 % (1623167)------------------------------ % 127.11/18.20 % (1623167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.11/18.20 % (1623167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.11/18.20 % (1623167)CaDiCaL version: 2.1.3 % 127.11/18.20 % (1623167)Termination reason: Instruction limit % 153.06/23.19 % (1623167)Termination phase: Saturation % 153.06/23.19 % (1623167)Time elapsed: 3.383 s % 153.06/23.19 % (1623167)Peak memory usage: 29 MB % 153.06/23.19 % (1623167)Instructions burned: 3513 (million) % 153.06/23.19 % (1623179)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=214943065:i=5211_2950 on theBenchmark for (2950ds/5211Mi) % 153.06/23.19 % (1623175)Instruction limit reached! % 153.06/23.19 % (1623175)------------------------------ % 153.06/23.19 % (1623175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.06/23.19 % (1623175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.06/23.19 % (1623175)CaDiCaL version: 2.1.3 % 153.06/23.19 % (1623175)Termination reason: Instruction limit % 153.06/23.19 % (1623175)Termination phase: Saturation % 153.06/23.19 % (1623175)Time elapsed: 2.386 s % 153.06/23.19 % (1623175)Peak memory usage: 52 MB % 153.06/23.19 % (1623175)Instructions burned: 4592 (million) % 153.06/23.19 % (1623181)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2914930632:i=5497:nm=2_2945 on theBenchmark for (2945ds/5497Mi) % 153.06/23.19 % (1623181)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 153.06/23.19 % (1623181)Terminated due to inappropriate strategy. % 153.06/23.19 % (1623181)------------------------------ % 153.06/23.19 % (1623181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.06/23.19 % (1623181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.06/23.19 % (1623181)CaDiCaL version: 2.1.3 % 153.06/23.19 % (1623181)Termination reason: Inappropriate % 153.06/23.19 % (1623181)Time elapsed: 0.012 s % 153.06/23.19 % (1623181)Peak memory usage: 11 MB % 153.06/23.19 % (1623181)Instructions burned: 15 (million) % 153.06/23.19 % (1623181)------------------------------ % 153.06/23.19 % (1623181)------------------------------ % 153.06/23.19 % (1623183)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1661467090:fmbsr=2:i=46332_2944 on theBenchmark for (2944ds/46332Mi) % 153.06/23.19 % (1623183)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 153.06/23.19 % (1623183)Terminated due to inappropriate strategy. % 153.06/23.19 % (1623183)------------------------------ % 153.06/23.19 % (1623183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.06/23.19 % (1623183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.06/23.19 % (1623183)CaDiCaL version: 2.1.3 % 153.06/23.19 % (1623183)Termination reason: Inappropriate % 153.06/23.19 % (1623183)Time elapsed: 0.015 s % 153.06/23.19 % (1623183)Peak memory usage: 11 MB % 153.06/23.19 % (1623183)Instructions burned: 12 (million) % 153.06/23.19 % (1623183)------------------------------ % 153.06/23.19 % (1623183)------------------------------ % 153.06/23.19 % (1623169)Instruction limit reached! % 153.06/23.19 % (1623169)------------------------------ % 153.06/23.19 % (1623169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.06/23.19 % (1623169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.06/23.19 % (1623169)CaDiCaL version: 2.1.3 % 153.06/23.19 % (1623169)Termination reason: Instruction limit % 153.06/23.19 % (1623169)Termination phase: Saturation % 153.06/23.19 % (1623169)Time elapsed: 3.565 s % 153.06/23.19 % (1623169)Peak memory usage: 33 MB % 153.06/23.19 % (1623169)Instructions burned: 3773 (million) % 153.06/23.19 % (1623185)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3728565729:i=14071_2944 on theBenchmark for (2944ds/14071Mi) % 153.06/23.19 % (1623185)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 153.06/23.19 % (1623185)Terminated due to inappropriate strategy. % 153.06/23.19 % (1623185)------------------------------ % 153.06/23.19 % (1623185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.06/23.19 % (1623185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.06/23.19 % (1623185)CaDiCaL version: 2.1.3 % 153.06/23.19 % (1623185)Termination reason: Inappropriate % 153.06/23.19 % (1623185)Time elapsed: 0.007 s % 153.06/23.19 % (1623185)Peak memory usage: 11 MB % 153.06/23.19 % (1623185)Instructions burned: 12 (million) % 153.06/23.19 % (1623185)------------------------------ % 153.06/23.19 % (1623185)------------------------------ % 153.06/23.19 % (1623186)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3473415141:i=22565:add=on:rawr=on_2944 on theBenchmark for (2944ds/22565Mi) % 153.06/23.19 % (1623188)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=209993960:i=8173:av=off_2943 on theBenchmark for (2943ds/8173Mi) % 162.38/23.29 % (1623163)Instruction limit reached! % 162.38/23.29 % (1623163)------------------------------ % 162.38/23.29 % (1623163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.38/23.29 % (1623163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.38/23.29 % (1623163)CaDiCaL version: 2.1.3 % 162.38/23.29 % (1623163)Termination reason: Instruction limit % 162.38/23.29 % (1623163)Termination phase: Saturation % 162.38/23.29 % (1623163)Time elapsed: 5.034 s % 162.38/23.29 % (1623163)Peak memory usage: 45 MB % 162.38/23.29 % (1623163)Instructions burned: 5115 (million) % 162.38/23.29 % (1623191)dis+10_16:1_sil=16000:random_seed=2225865888:i=9155:fsr=off_2937 on theBenchmark for (2937ds/9155Mi) % 162.38/23.29 % (1623179)Instruction limit reached! % 162.38/23.29 % (1623179)------------------------------ % 162.38/23.29 % (1623179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.38/23.29 % (1623179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.38/23.29 % (1623179)CaDiCaL version: 2.1.3 % 162.38/23.29 % (1623179)Termination reason: Instruction limit % 162.38/23.29 % (1623179)Termination phase: Saturation % 162.38/23.29 % (1623179)Time elapsed: 4.491 s % 162.38/23.29 % (1623179)Peak memory usage: 45 MB % 162.38/23.29 % (1623179)Instructions burned: 5212 (million) % 162.38/23.29 % (1623195)ott-3_8_sil=64000:random_seed=509393812:i=20139:bs=on_2905 on theBenchmark for (2905ds/20139Mi) % 162.38/23.29 % (1623186)Instruction limit reached! % 162.38/23.29 % (1623186)------------------------------ % 162.38/23.29 % (1623186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.38/23.29 % (1623186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.38/23.29 % (1623186)CaDiCaL version: 2.1.3 % 162.38/23.29 % (1623186)Termination reason: Instruction limit % 162.38/23.29 % (1623186)Termination phase: Saturation % 162.38/23.29 % (1623186)Time elapsed: 8.314 s % 162.38/23.29 % (1623186)Peak memory usage: 21 MB % 162.38/23.29 % (1623186)Instructions burned: 22571 (million) % 162.38/23.29 % (1623188)Instruction limit reached! % 162.38/23.29 % (1623188)------------------------------ % 162.38/23.29 % (1623188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.38/23.29 % (1623188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.38/23.29 % (1623188)CaDiCaL version: 2.1.3 % 162.38/23.29 % (1623188)Termination reason: Instruction limit % 162.38/23.29 % (1623188)Termination phase: Saturation % 162.38/23.29 % (1623298)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2169665435:fmbsr=2:i=32576_2860 on theBenchmark for (2860ds/32576Mi) % 162.38/23.29 % (1623188)Time elapsed: 8.313 s % 162.38/23.29 % (1623188)Peak memory usage: 63 MB % 162.38/23.29 % (1623188)Instructions burned: 8174 (million) % 162.38/23.29 % (1623298)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 162.38/23.29 % (1623298)Terminated due to inappropriate strategy. % 162.38/23.29 % (1623298)------------------------------ % 162.38/23.29 % (1623298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.38/23.29 % (1623298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.38/23.29 % (1623298)CaDiCaL version: 2.1.3 % 162.38/23.29 % (1623298)Termination reason: Inappropriate % 162.38/23.29 % (1623298)Time elapsed: 0.004 s % 162.38/23.29 % (1623298)Peak memory usage: 11 MB % 162.38/23.29 % (1623298)Instructions burned: 16 (million) % 162.38/23.29 % (1623298)------------------------------ % 162.38/23.29 % (1623298)------------------------------ % 162.38/23.29 % (1623305)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4170598914:i=11404_2860 on theBenchmark for (2860ds/11404Mi) % 162.38/23.29 % (1623306)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2564069453:i=14134_2860 on theBenchmark for (2860ds/14134Mi) % 162.38/23.29 % (1623191)Instruction limit reached! % 162.38/23.29 % (1623191)------------------------------ % 162.38/23.29 % (1623191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.38/23.29 % (1623191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.38/23.29 % (1623191)CaDiCaL version: 2.1.3 % 162.38/23.29 % (1623191)Termination reason: Instruction limit % 162.38/23.29 % (1623191)Termination phase: Saturation % 162.38/23.29 % (1623191)Time elapsed: 7.860 s % 162.38/23.29 % (1623191)Peak memory usage: 53 MB % 162.38/23.29 % (1623191)Instructions burned: 9156 (million) % 162.38/23.29 % (1623356)dis+33_16_sil=32000:sac=on:random_seed=2100008912:i=15851:nm=0_2858 on theBenchmark for (2858ds/15851Mi) % 162.38/23.29 % (1623305)Instruction limit reached! % 162.38/23.29 % (1623305)------------------------------ % 162.38/23.29 % (1623305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.33/24.64 % (1623305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.33/24.64 % (1623305)CaDiCaL version: 2.1.3 % 172.33/24.64 % (1623305)Termination reason: Instruction limit % 172.33/24.64 % (1623305)Termination phase: Saturation % 172.33/24.64 % (1623305)Time elapsed: 3.922 s % 172.33/24.64 % (1623305)Peak memory usage: 65 MB % 172.33/24.64 % (1623305)Instructions burned: 11410 (million) % 172.33/24.64 % (1623358)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3059472129:avsq=on:i=17627:add=on:amm=off_2821 on theBenchmark for (2821ds/17627Mi) % 172.33/24.64 % (1623358)Instruction limit reached! % 172.33/24.64 % (1623358)------------------------------ % 172.33/24.64 % (1623358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.33/24.64 % (1623358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.33/24.64 % (1623358)CaDiCaL version: 2.1.3 % 172.33/24.64 % (1623358)Termination reason: Instruction limit % 172.33/24.64 % (1623358)Termination phase: Saturation % 172.33/24.64 % (1623358)Time elapsed: 4.806 s % 172.33/24.64 % (1623358)Peak memory usage: 97 MB % 172.33/24.64 % (1623358)Instructions burned: 17631 (million) % 172.33/24.64 % (1623360)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2427865353:s2a=on:i=53295_2772 on theBenchmark for (2772ds/53295Mi) % 172.33/24.64 % (1623177)Instruction limit reached! % 172.33/24.64 % (1623177)------------------------------ % 172.33/24.64 % (1623177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.33/24.64 % (1623177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.33/24.64 % (1623177)CaDiCaL version: 2.1.3 % 172.33/24.64 % (1623177)Termination reason: Instruction limit % 172.33/24.64 % (1623177)Termination phase: Saturation % 172.33/24.64 % (1623177)Time elapsed: 18.210 s % 172.33/24.64 % (1623177)Peak memory usage: 183 MB % 172.33/24.64 % (1623177)Instructions burned: 29340 (million) % 172.33/24.64 % (1623306)Instruction limit reached! % 172.33/24.64 % (1623306)------------------------------ % 172.33/24.64 % (1623306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.33/24.64 % (1623306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.33/24.64 % (1623306)CaDiCaL version: 2.1.3 % 172.33/24.64 % (1623306)Termination reason: Instruction limit % 172.33/24.64 % (1623306)Termination phase: Saturation % 172.33/24.64 % (1623306)Time elapsed: 8.841 s % 172.33/24.64 % (1623306)Peak memory usage: 70 MB % 172.33/24.64 % (1623306)Instructions burned: 14135 (million) % 172.33/24.64 % (1623362)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=848669608:i=26857:ins=20_2772 on theBenchmark for (2772ds/26857Mi) % 172.33/24.64 % (1623362)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.33/24.64 % (1623362)Terminated due to inappropriate strategy. % 172.33/24.64 % (1623362)------------------------------ % 172.33/24.64 % (1623362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.33/24.64 % (1623362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.33/24.64 % (1623362)CaDiCaL version: 2.1.3 % 172.33/24.64 % (1623362)Termination reason: Inappropriate % 172.33/24.64 % (1623362)Time elapsed: 0.006 s % 172.33/24.64 % (1623362)Peak memory usage: 11 MB % 172.33/24.64 % (1623362)Instructions burned: 12 (million) % 172.33/24.64 % (1623362)------------------------------ % 172.33/24.64 % (1623362)------------------------------ % 172.33/24.64 % (1623363)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3611187131:i=28120:bs=on:fsr=off_2771 on theBenchmark for (2771ds/28120Mi) % 172.33/24.64 % (1623365)fmb+10_1_sil=256000:fmbss=7:random_seed=2253783692:fmbsr=1.6:i=182295_2771 on theBenchmark for (2771ds/182295Mi) % 172.33/24.64 % (1623365)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 172.33/24.64 % (1623365)Terminated due to inappropriate strategy. % 172.33/24.64 % (1623365)------------------------------ % 172.33/24.64 % (1623365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.33/24.64 % (1623365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.33/24.64 % (1623365)CaDiCaL version: 2.1.3 % 172.33/24.64 % (1623365)Termination reason: Inappropriate % 172.33/24.64 % (1623365)Time elapsed: 0.006 s % 172.33/24.64 % (1623365)Peak memory usage: 11 MB % 172.33/24.64 % (1623365)Instructions burned: 12 (million) % 172.33/24.64 % (1623365)------------------------------ % 172.33/24.64 % (1623365)------------------------------ % 172.33/24.64 % (1623368)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=356494166:i=44625:gsp=on_2771 on theBenchmark for (2771ds/44625Mi) % 185.32/26.43 % (1623368)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.32/26.43 % (1623368)Terminated due to inappropriate strategy. % 185.32/26.43 % (1623368)------------------------------ % 185.32/26.43 % (1623368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.32/26.43 % (1623368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.32/26.43 % (1623368)CaDiCaL version: 2.1.3 % 185.32/26.43 % (1623368)Termination reason: Inappropriate % 185.32/26.43 % (1623368)Time elapsed: 0.006 s % 185.32/26.43 % (1623368)Peak memory usage: 11 MB % 185.32/26.43 % (1623368)Instructions burned: 12 (million) % 185.32/26.43 % (1623368)------------------------------ % 185.32/26.43 % (1623368)------------------------------ % 185.32/26.43 % (1623370)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2875361378:i=160505_2771 on theBenchmark for (2771ds/160505Mi) % 185.32/26.43 % (1623370)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.32/26.43 % (1623370)Terminated due to inappropriate strategy. % 185.32/26.43 % (1623370)------------------------------ % 185.32/26.43 % (1623370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.32/26.43 % (1623370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.32/26.43 % (1623370)CaDiCaL version: 2.1.3 % 185.32/26.43 % (1623370)Termination reason: Inappropriate % 185.32/26.43 % (1623370)Time elapsed: 0.006 s % 185.32/26.43 % (1623370)Peak memory usage: 11 MB % 185.32/26.43 % (1623370)Instructions burned: 12 (million) % 185.32/26.43 % (1623370)------------------------------ % 185.32/26.43 % (1623370)------------------------------ % 185.32/26.43 % (1623356)Instruction limit reached! % 185.32/26.43 % (1623356)------------------------------ % 185.32/26.43 % (1623356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.32/26.43 % (1623356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.32/26.43 % (1623356)CaDiCaL version: 2.1.3 % 185.32/26.43 % (1623356)Termination reason: Instruction limit % 185.32/26.43 % (1623356)Termination phase: Saturation % 185.32/26.43 % (1623356)Time elapsed: 8.728 s % 185.32/26.43 % (1623356)Peak memory usage: 120 MB % 185.32/26.43 % (1623356)Instructions burned: 15852 (million) % 185.32/26.43 % (1623372)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1895527543:fmbsr=1.3:i=225729_2770 on theBenchmark for (2770ds/225729Mi) % 185.32/26.43 % (1623372)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.32/26.43 % (1623372)Terminated due to inappropriate strategy. % 185.32/26.43 % (1623372)------------------------------ % 185.32/26.43 % (1623372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.32/26.43 % (1623372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.32/26.43 % (1623372)CaDiCaL version: 2.1.3 % 185.32/26.43 % (1623372)Termination reason: Inappropriate % 185.32/26.43 % (1623372)Time elapsed: 0.006 s % 185.32/26.43 % (1623372)Peak memory usage: 11 MB % 185.32/26.43 % (1623372)Instructions burned: 12 (million) % 185.32/26.43 % (1623372)------------------------------ % 185.32/26.43 % (1623372)------------------------------ % 185.32/26.43 % (1623374)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2429334194:fmbsr=2:i=185024:ins=7_2770 on theBenchmark for (2770ds/185024Mi) % 185.32/26.43 % (1623375)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4227978255:rtra=on_2770 on theBenchmark for (2770ds/0Mi) % 185.32/26.43 % (1623374)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.32/26.43 % (1623374)Terminated due to inappropriate strategy. % 185.32/26.43 % (1623374)------------------------------ % 185.32/26.43 % (1623374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.32/26.43 % (1623374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.32/26.43 % (1623374)CaDiCaL version: 2.1.3 % 185.32/26.43 % (1623374)Termination reason: Inappropriate % 185.32/26.43 % (1623374)Time elapsed: 0.006 s % 185.32/26.43 % (1623374)Peak memory usage: 11 MB % 185.32/26.43 % (1623374)Instructions burned: 12 (million) % 185.32/26.43 % (1623374)------------------------------ % 185.32/26.43 % (1623374)------------------------------ % 185.32/26.43 % (1623375)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.32/26.43 % (1623375)Terminated due to inappropriate strategy. % 185.32/26.43 % (1623375)------------------------------ % 185.32/26.43 % (1623375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.74/29.74 % (1623375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.74/29.74 % (1623375)CaDiCaL version: 2.1.3 % 208.74/29.74 % (1623375)Termination reason: Inappropriate % 208.74/29.74 % (1623375)Time elapsed: 0.008 s % 208.74/29.74 % (1623375)Peak memory usage: 11 MB % 208.74/29.74 % (1623375)Instructions burned: 15 (million) % 208.74/29.74 % (1623375)------------------------------ % 208.74/29.74 % (1623375)------------------------------ % 208.74/29.74 % (1623378)% WARNING: option uhcvi not known. % 208.74/29.74 % (1623378)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3119681489:i=271062:add=off:rtra=on:rawr=on_2770 on theBenchmark for (2770ds/271062Mi) % 208.74/29.74 % (1623379)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3933846351:i=176048:add=on:rtra=on:rawr=on_2770 on theBenchmark for (2770ds/176048Mi) % 208.74/29.74 % (1623195)Instruction limit reached! % 208.74/29.74 % (1623195)------------------------------ % 208.74/29.74 % (1623195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.74/29.74 % (1623195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.74/29.74 % (1623195)CaDiCaL version: 2.1.3 % 208.74/29.74 % (1623195)Termination reason: Instruction limit % 208.74/29.74 % (1623195)Termination phase: Saturation % 208.74/29.74 % (1623195)Time elapsed: 14.091 s % 208.74/29.74 % (1623195)Peak memory usage: 80 MB % 208.74/29.74 % (1623195)Instructions burned: 20140 (million) % 208.74/29.74 % (1623382)dis+10_1_sil=32000:si=on:sp=arity:random_seed=755763310:i=206:fgj=on:rtra=on_2764 on theBenchmark for (2764ds/206Mi) % 208.74/29.74 % (1623382)Instruction limit reached! % 208.74/29.74 % (1623382)------------------------------ % 208.74/29.74 % (1623382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.74/29.74 % (1623382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.74/29.74 % (1623382)CaDiCaL version: 2.1.3 % 208.74/29.74 % (1623382)Termination reason: Instruction limit % 208.74/29.74 % (1623382)Termination phase: Saturation % 208.74/29.74 % (1623382)Time elapsed: 0.123 s % 208.74/29.74 % (1623382)Peak memory usage: 13 MB % 208.74/29.74 % (1623382)Instructions burned: 207 (million) % 208.74/29.74 % (1623384)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1013603390:i=232:rtra=on_2762 on theBenchmark for (2762ds/232Mi) % 208.74/29.74 % (1623384)Instruction limit reached! % 208.74/29.74 % (1623384)------------------------------ % 208.74/29.74 % (1623384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.74/29.74 % (1623384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.74/29.74 % (1623384)CaDiCaL version: 2.1.3 % 208.74/29.74 % (1623384)Termination reason: Instruction limit % 208.74/29.74 % (1623384)Termination phase: Saturation % 208.74/29.74 % (1623384)Time elapsed: 0.141 s % 208.74/29.74 % (1623384)Peak memory usage: 14 MB % 208.74/29.74 % (1623384)Instructions burned: 232 (million) % 208.74/29.74 % (1623386)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=813838725:i=262:rtra=on_2761 on theBenchmark for (2761ds/262Mi) % 208.74/29.74 % (1623386)Instruction limit reached! % 208.74/29.74 % (1623386)------------------------------ % 208.74/29.74 % (1623386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.74/29.74 % (1623386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.74/29.74 % (1623386)CaDiCaL version: 2.1.3 % 208.74/29.74 % (1623386)Termination reason: Instruction limit % 208.74/29.74 % (1623386)Termination phase: Saturation % 208.74/29.74 % (1623386)Time elapsed: 0.160 s % 208.74/29.74 % (1623386)Peak memory usage: 15 MB % 208.74/29.74 % (1623386)Instructions burned: 263 (million) % 208.74/29.74 % (1623388)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2020069733:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2759 on theBenchmark for (2759ds/318Mi) % 208.74/29.74 % (1623388)Instruction limit reached! % 208.74/29.74 % (1623388)------------------------------ % 208.74/29.74 % (1623388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.74/29.74 % (1623388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.74/29.74 % (1623388)CaDiCaL version: 2.1.3 % 208.74/29.74 % (1623388)Termination reason: Instruction limit % 208.74/29.74 % (1623388)Termination phase: Saturation % 208.74/29.74 % (1623388)Time elapsed: 0.223 s % 208.74/29.74 % (1623388)Peak memory usage: 15 MB % 208.74/29.74 % (1623388)Instructions burned: 318 (million) % 208.74/29.74 % (1623390)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=196122557:i=1428:nm=2:rtra=on_2757 on theBenchmark for (2757ds/1428Mi) % 279.61/39.79 % (1623390)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.61/39.79 % (1623390)Terminated due to inappropriate strategy. % 279.61/39.79 % (1623390)------------------------------ % 279.61/39.79 % (1623390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.61/39.79 % (1623390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.61/39.79 % (1623390)CaDiCaL version: 2.1.3 % 279.61/39.79 % (1623390)Termination reason: Inappropriate % 279.61/39.79 % (1623390)Time elapsed: 0.007 s % 279.61/39.79 % (1623390)Peak memory usage: 11 MB % 279.61/39.79 % (1623390)Instructions burned: 13 (million) % 279.61/39.79 % (1623390)------------------------------ % 279.61/39.79 % (1623390)------------------------------ % 279.61/39.79 % (1623392)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3127062944:i=262:bd=preordered:rtra=on:fsd=on_2756 on theBenchmark for (2756ds/262Mi) % 279.61/39.79 % (1623392)Instruction limit reached! % 279.61/39.79 % (1623392)------------------------------ % 279.61/39.79 % (1623392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.61/39.79 % (1623392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.61/39.79 % (1623392)CaDiCaL version: 2.1.3 % 279.61/39.79 % (1623392)Termination reason: Instruction limit % 279.61/39.79 % (1623392)Termination phase: Saturation % 279.61/39.79 % (1623392)Time elapsed: 0.171 s % 279.61/39.79 % (1623392)Peak memory usage: 14 MB % 279.61/39.79 % (1623392)Instructions burned: 263 (million) % 279.61/39.79 % (1623394)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=3490435334:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2754 on theBenchmark for (2754ds/1368Mi) % 279.61/39.79 % (1623394)Instruction limit reached! % 279.61/39.79 % (1623394)------------------------------ % 279.61/39.79 % (1623394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.61/39.79 % (1623394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.61/39.79 % (1623394)CaDiCaL version: 2.1.3 % 279.61/39.79 % (1623394)Termination reason: Instruction limit % 279.61/39.79 % (1623394)Termination phase: Saturation % 279.61/39.79 % (1623394)Time elapsed: 0.828 s % 279.61/39.79 % (1623394)Peak memory usage: 23 MB % 279.61/39.79 % (1623394)Instructions burned: 1368 (million) % 279.61/39.79 % (1623396)ott-21_1_sil=16000:si=on:fs=off:random_seed=2007664869:i=360:av=off:fsr=off:rtra=on_2746 on theBenchmark for (2746ds/360Mi) % 279.61/39.79 % (1623396)Instruction limit reached! % 279.61/39.79 % (1623396)------------------------------ % 279.61/39.79 % (1623396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.61/39.79 % (1623396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.61/39.79 % (1623396)CaDiCaL version: 2.1.3 % 279.61/39.79 % (1623396)Termination reason: Instruction limit % 279.61/39.79 % (1623396)Termination phase: Saturation % 279.61/39.79 % (1623396)Time elapsed: 0.176 s % 279.61/39.79 % (1623396)Peak memory usage: 13 MB % 279.61/39.79 % (1623396)Instructions burned: 361 (million) % 279.61/39.79 % (1623398)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=630836464:i=954:bd=all:rtra=on_2744 on theBenchmark for (2744ds/954Mi) % 279.61/39.79 % (1623398)Instruction limit reached! % 279.61/39.79 % (1623398)------------------------------ % 279.61/39.79 % (1623398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.61/39.79 % (1623398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.61/39.79 % (1623398)CaDiCaL version: 2.1.3 % 279.61/39.79 % (1623398)Termination reason: Instruction limit % 279.61/39.79 % (1623398)Termination phase: Saturation % 279.61/39.79 % (1623398)Time elapsed: 0.498 s % 279.61/39.79 % (1623398)Peak memory usage: 13 MB % 279.61/39.79 % (1623398)Instructions burned: 954 (million) % 279.61/39.79 % (1623400)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2922484279:fmbsr=1.3:i=1730:ins=25:rtra=on_2739 on theBenchmark for (2739ds/1730Mi) % 279.61/39.79 % (1623400)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.61/39.79 % (1623400)Terminated due to inappropriate strategy. % 279.61/39.79 % (1623400)------------------------------ % 279.61/39.79 % (1623400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.61/39.79 % (1623400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.61/39.79 % (1623400)CaDiCaL version: 2.1.3 % 279.61/39.79 % (1623400)Termination reasTerminated % 300.52/42.64 % Vampire exiting % 300.52/42.64 Terminated %------------------------------------------------------------------------------