%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC444_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n008.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:06:01 PM UTC 2026 % Result : Timeout 300.30s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWC444_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.27 % Computer : n008.cluster.edu % 0.11/0.27 % Model : x86_64 x86_64 % 0.11/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.27 % Memory : 8046.5625MB % 0.11/0.27 % 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 09:38:54 UTC 2026 % 0.11/0.28 % CPUTime : % 0.11/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.27/0.32 Running first-order model finding % 0.27/0.32 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.87/1.20 % (2127930)Will run a generic schedule for satisfiability detection. % 5.87/1.20 % (2127936)% WARNING: option uhcvi not known. % 5.87/1.20 % (2127936)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3485336507:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.87/1.20 % (2127935)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=12084010_2999 on theBenchmark for (2999ds/0Mi) % 5.87/1.20 % (2127941)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3085334447:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.87/1.20 % (2127935)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.87/1.20 % (2127938)dis+10_1_sil=32000:sp=arity:random_seed=1675452102:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.87/1.20 % (2127935)Terminated due to inappropriate strategy. % 5.87/1.20 % (2127935)------------------------------ % 5.87/1.20 % (2127935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.87/1.20 % (2127935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.87/1.20 % (2127935)CaDiCaL version: 2.1.3 % 5.87/1.20 % (2127935)Termination reason: Inappropriate % 5.87/1.20 % (2127935)Time elapsed: 0.002 s % 5.87/1.20 % (2127935)Peak memory usage: 10 MB % 5.87/1.20 % (2127935)Instructions burned: 2 (million) % 5.87/1.20 % (2127939)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2003590077:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.87/1.20 % (2127937)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=651336079:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.87/1.20 % (2127940)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=310633539:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.87/1.20 % (2127935)------------------------------ % 5.87/1.20 % (2127935)------------------------------ % 5.87/1.20 % (2127949)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=882729797:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.87/1.20 % (2127949)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.87/1.20 % (2127949)Terminated due to inappropriate strategy. % 5.87/1.20 % (2127949)------------------------------ % 5.87/1.20 % (2127949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.87/1.20 % (2127949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.87/1.20 % (2127949)CaDiCaL version: 2.1.3 % 5.87/1.20 % (2127949)Termination reason: Inappropriate % 5.87/1.20 % (2127949)Time elapsed: 0.002 s % 5.87/1.20 % (2127949)Peak memory usage: 10 MB % 5.87/1.20 % (2127949)Instructions burned: 2 (million) % 5.87/1.20 % (2127949)------------------------------ % 5.87/1.20 % (2127949)------------------------------ % 5.87/1.20 % (2127951)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2384115941:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.87/1.20 % (2127938)Instruction limit reached! % 5.87/1.20 % (2127938)------------------------------ % 5.87/1.20 % (2127938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.87/1.20 % (2127938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.87/1.20 % (2127938)CaDiCaL version: 2.1.3 % 5.87/1.20 % (2127938)Termination reason: Instruction limit % 5.87/1.20 % (2127938)Termination phase: Saturation % 5.87/1.20 % (2127938)Time elapsed: 0.101 s % 5.87/1.20 % (2127938)Peak memory usage: 12 MB % 5.87/1.20 % (2127938)Instructions burned: 103 (million) % 5.87/1.20 % (2127940)Instruction limit reached! % 5.87/1.20 % (2127940)------------------------------ % 5.87/1.20 % (2127940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.87/1.20 % (2127940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.87/1.20 % (2127940)CaDiCaL version: 2.1.3 % 5.87/1.20 % (2127940)Termination reason: Instruction limit % 5.87/1.20 % (2127940)Termination phase: Saturation % 5.87/1.20 % (2127940)Time elapsed: 0.114 s % 5.87/1.20 % (2127940)Peak memory usage: 12 MB % 5.87/1.20 % (2127940)Instructions burned: 131 (million) % 5.87/1.20 % (2127939)Instruction limit reached! % 5.87/1.20 % (2127939)------------------------------ % 5.87/1.20 % (2127939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.87/1.20 % (2127939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.87/1.20 % (2127939)CaDiCaL version: 2.1.3 % 5.87/1.20 % (2127939)Termination reason: Instruction limit % 7.37/1.55 % (2127939)Termination phase: Saturation % 7.37/1.55 % (2127939)Time elapsed: 0.120 s % 7.37/1.55 % (2127939)Peak memory usage: 12 MB % 7.37/1.55 % (2127939)Instructions burned: 116 (million) % 7.37/1.55 % (2127953)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=1092117681:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.37/1.55 % (2127954)ott-21_1_sil=16000:fs=off:random_seed=3371738093:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.37/1.55 % (2127955)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2310196070:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.37/1.55 % (2127941)Instruction limit reached! % 7.37/1.55 % (2127941)------------------------------ % 7.37/1.55 % (2127941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.37/1.55 % (2127941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/1.55 % (2127941)CaDiCaL version: 2.1.3 % 7.37/1.55 % (2127941)Termination reason: Instruction limit % 7.37/1.55 % (2127941)Termination phase: Saturation % 7.37/1.55 % (2127941)Time elapsed: 0.170 s % 7.37/1.55 % (2127941)Peak memory usage: 13 MB % 7.37/1.55 % (2127941)Instructions burned: 159 (million) % 7.37/1.55 % (2127951)Instruction limit reached! % 7.37/1.55 % (2127951)------------------------------ % 7.37/1.55 % (2127951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.37/1.55 % (2127951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/1.55 % (2127951)CaDiCaL version: 2.1.3 % 7.37/1.55 % (2127951)Termination reason: Instruction limit % 7.37/1.55 % (2127951)Termination phase: Saturation % 7.37/1.55 % (2127951)Time elapsed: 0.128 s % 7.37/1.55 % (2127951)Peak memory usage: 12 MB % 7.37/1.55 % (2127951)Instructions burned: 132 (million) % 7.37/1.55 % (2127959)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=550817723:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 7.37/1.55 % (2127959)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.37/1.55 % (2127959)Terminated due to inappropriate strategy. % 7.37/1.55 % (2127959)------------------------------ % 7.37/1.55 % (2127959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.37/1.55 % (2127959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/1.55 % (2127959)CaDiCaL version: 2.1.3 % 7.37/1.55 % (2127959)Termination reason: Inappropriate % 7.37/1.55 % (2127959)Time elapsed: 0.003 s % 7.37/1.55 % (2127959)Peak memory usage: 10 MB % 7.37/1.55 % (2127959)Instructions burned: 2 (million) % 7.37/1.55 % (2127959)------------------------------ % 7.37/1.55 % (2127959)------------------------------ % 7.37/1.55 % (2127960)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2061762301:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 7.37/1.55 % (2127962)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2466679761:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.37/1.55 % (2127962)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.37/1.55 % (2127962)Terminated due to inappropriate strategy. % 7.37/1.55 % (2127962)------------------------------ % 7.37/1.55 % (2127962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.37/1.55 % (2127962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/1.55 % (2127962)CaDiCaL version: 2.1.3 % 7.37/1.55 % (2127962)Termination reason: Inappropriate % 7.37/1.55 % (2127962)Time elapsed: 0.002 s % 7.37/1.55 % (2127962)Peak memory usage: 11 MB % 7.37/1.55 % (2127962)Instructions burned: 2 (million) % 7.37/1.55 % (2127962)------------------------------ % 7.37/1.55 % (2127962)------------------------------ % 7.37/1.55 % (2127954)Instruction limit reached! % 7.37/1.55 % (2127954)------------------------------ % 7.37/1.55 % (2127954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.37/1.55 % (2127954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/1.55 % (2127954)CaDiCaL version: 2.1.3 % 7.37/1.55 % (2127954)Termination reason: Instruction limit % 7.37/1.55 % (2127954)Termination phase: Saturation % 7.37/1.55 % (2127954)Time elapsed: 0.137 s % 7.37/1.55 % (2127954)Peak memory usage: 12 MB % 7.37/1.55 % (2127954)Instructions burned: 181 (million) % 7.37/1.55 % (2127968)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2384145250:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 31.18/4.72 % (2127966)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=600479010:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 31.18/4.72 % (2127955)Instruction limit reached! % 31.18/4.72 % (2127955)------------------------------ % 31.18/4.72 % (2127955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.18/4.72 % (2127955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.18/4.72 % (2127955)CaDiCaL version: 2.1.3 % 31.18/4.72 % (2127955)Termination reason: Instruction limit % 31.18/4.72 % (2127955)Termination phase: Saturation % 31.18/4.72 % (2127955)Time elapsed: 0.514 s % 31.18/4.72 % (2127955)Peak memory usage: 14 MB % 31.18/4.72 % (2127955)Instructions burned: 477 (million) % 31.18/4.72 % (2127971)fmb+10_1_sil=64000:random_seed=3252428356:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 31.18/4.72 % (2127971)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.18/4.72 % (2127971)Terminated due to inappropriate strategy. % 31.18/4.72 % (2127971)------------------------------ % 31.18/4.72 % (2127971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.18/4.72 % (2127971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.18/4.72 % (2127971)CaDiCaL version: 2.1.3 % 31.18/4.72 % (2127971)Termination reason: Inappropriate % 31.18/4.72 % (2127971)Time elapsed: 0.002 s % 31.18/4.72 % (2127971)Peak memory usage: 10 MB % 31.18/4.72 % (2127971)Instructions burned: 2 (million) % 31.18/4.72 % (2127971)------------------------------ % 31.18/4.72 % (2127971)------------------------------ % 31.18/4.72 % (2127968)Instruction limit reached! % 31.18/4.72 % (2127968)------------------------------ % 31.18/4.72 % (2127968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.18/4.72 % (2127968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.18/4.72 % (2127968)CaDiCaL version: 2.1.3 % 31.18/4.72 % (2127968)Termination reason: Instruction limit % 31.18/4.72 % (2127968)Termination phase: Saturation % 31.18/4.72 % (2127968)Time elapsed: 0.444 s % 31.18/4.72 % (2127968)Peak memory usage: 18 MB % 31.18/4.72 % (2127968)Instructions burned: 881 (million) % 31.18/4.72 % (2127973)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1271374838:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 31.18/4.72 % (2127974)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=171574722:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 31.18/4.72 % (2127974)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.18/4.72 % (2127974)Terminated due to inappropriate strategy. % 31.18/4.72 % (2127974)------------------------------ % 31.18/4.72 % (2127974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.18/4.72 % (2127974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.18/4.72 % (2127974)CaDiCaL version: 2.1.3 % 31.18/4.72 % (2127974)Termination reason: Inappropriate % 31.18/4.72 % (2127974)Time elapsed: 0.001 s % 31.18/4.72 % (2127974)Peak memory usage: 10 MB % 31.18/4.72 % (2127974)Instructions burned: 2 (million) % 31.18/4.72 % (2127973)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.18/4.72 % (2127973)Terminated due to inappropriate strategy. % 31.18/4.72 % (2127973)------------------------------ % 31.18/4.72 % (2127973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.18/4.72 % (2127973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.18/4.72 % (2127974)------------------------------ % 31.18/4.72 % (2127974)------------------------------ % 31.18/4.72 % (2127973)CaDiCaL version: 2.1.3 % 31.18/4.72 % (2127973)Termination reason: Inappropriate % 31.18/4.72 % (2127973)Time elapsed: 0.002 s % 31.18/4.72 % (2127973)Peak memory usage: 10 MB % 31.18/4.72 % (2127973)Instructions burned: 2 (million) % 31.18/4.72 % (2127973)------------------------------ % 31.18/4.72 % (2127973)------------------------------ % 31.18/4.72 % (2127977)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1664763365:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 31.18/4.72 % (2127978)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=730128143:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 31.18/4.72 % (2127953)Instruction limit reached! % 31.18/4.72 % (2127953)------------------------------ % 44.20/6.67 % (2127953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.20/6.67 % (2127953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.20/6.67 % (2127953)CaDiCaL version: 2.1.3 % 44.20/6.67 % (2127953)Termination reason: Instruction limit % 44.20/6.67 % (2127953)Termination phase: Saturation % 44.20/6.67 % (2127953)Time elapsed: 0.690 s % 44.20/6.67 % (2127953)Peak memory usage: 16 MB % 44.20/6.67 % (2127953)Instructions burned: 685 (million) % 44.20/6.67 % (2127981)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1317167844:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 44.20/6.67 % (2127981)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 44.20/6.67 % (2127981)Terminated due to inappropriate strategy. % 44.20/6.67 % (2127981)------------------------------ % 44.20/6.67 % (2127981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.20/6.67 % (2127981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.20/6.67 % (2127981)CaDiCaL version: 2.1.3 % 44.20/6.67 % (2127981)Termination reason: Inappropriate % 44.20/6.67 % (2127981)Time elapsed: 0.003 s % 44.20/6.67 % (2127981)Peak memory usage: 11 MB % 44.20/6.67 % (2127981)Instructions burned: 2 (million) % 44.20/6.67 % (2127981)------------------------------ % 44.20/6.67 % (2127981)------------------------------ % 44.20/6.67 % (2127983)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4124647269:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 44.20/6.67 % (2127983)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 44.20/6.67 % (2127983)Terminated due to inappropriate strategy. % 44.20/6.67 % (2127983)------------------------------ % 44.20/6.67 % (2127983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.20/6.67 % (2127983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.20/6.67 % (2127983)CaDiCaL version: 2.1.3 % 44.20/6.67 % (2127983)Termination reason: Inappropriate % 44.20/6.67 % (2127983)Time elapsed: 0.001 s % 44.20/6.67 % (2127983)Peak memory usage: 11 MB % 44.20/6.67 % (2127983)Instructions burned: 2 (million) % 44.20/6.67 % (2127983)------------------------------ % 44.20/6.67 % (2127983)------------------------------ % 44.20/6.67 % (2127985)ott-2_1_sil=16000:newcnf=on:random_seed=3982311860:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 44.20/6.67 % (2127966)Instruction limit reached! % 44.20/6.67 % (2127966)------------------------------ % 44.20/6.67 % (2127966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.20/6.67 % (2127966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.20/6.67 % (2127966)CaDiCaL version: 2.1.3 % 44.20/6.67 % (2127966)Termination reason: Instruction limit % 44.20/6.67 % (2127966)Termination phase: Saturation % 44.20/6.67 % (2127966)Time elapsed: 0.692 s % 44.20/6.67 % (2127966)Peak memory usage: 17 MB % 44.20/6.67 % (2127966)Instructions burned: 693 (million) % 44.20/6.67 % (2127987)ott+10_1_sil=32000:tgt=ground:random_seed=1268033671:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 44.20/6.67 % (2127960)Instruction limit reached! % 44.20/6.67 % (2127960)------------------------------ % 44.20/6.67 % (2127960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.20/6.67 % (2127960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.20/6.67 % (2127960)CaDiCaL version: 2.1.3 % 44.20/6.67 % (2127960)Termination reason: Instruction limit % 44.20/6.67 % (2127960)Termination phase: Saturation % 44.20/6.67 % (2127960)Time elapsed: 0.928 s % 44.20/6.67 % (2127960)Peak memory usage: 16 MB % 44.20/6.67 % (2127960)Instructions burned: 1180 (million) % 44.20/6.67 % (2127989)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1417882358:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 44.20/6.67 % (2127989)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 44.20/6.67 % (2127989)Terminated due to inappropriate strategy. % 44.20/6.67 % (2127989)------------------------------ % 44.20/6.67 % (2127989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.20/6.67 % (2127989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.20/6.67 % (2127989)CaDiCaL version: 2.1.3 % 44.20/6.67 % (2127989)Termination reason: Inappropriate % 44.20/6.67 % (2127989)Time elapsed: 0.001 s % 44.20/6.67 % (2127989)Peak memory usage: 11 MB % 44.20/6.67 % (2127989)Instructions burned: 2 (million) % 129.98/18.61 % (2127989)------------------------------ % 129.98/18.61 % (2127989)------------------------------ % 129.98/18.61 % (2127991)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=381418190:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 129.98/18.61 % (2127985)Instruction limit reached! % 129.98/18.61 % (2127985)------------------------------ % 129.98/18.61 % (2127985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.98/18.61 % (2127985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.98/18.61 % (2127985)CaDiCaL version: 2.1.3 % 129.98/18.61 % (2127985)Termination reason: Instruction limit % 129.98/18.61 % (2127985)Termination phase: Saturation % 129.98/18.61 % (2127985)Time elapsed: 0.831 s % 129.98/18.61 % (2127985)Peak memory usage: 16 MB % 129.98/18.61 % (2127985)Instructions burned: 869 (million) % 129.98/18.61 % (2127993)dis+21_1_sil=32000:sas=cadical:random_seed=636615209:i=3773:amm=off_2981 on theBenchmark for (2981ds/3773Mi) % 129.98/18.61 % (2127978)Instruction limit reached! % 129.98/18.61 % (2127978)------------------------------ % 129.98/18.61 % (2127978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.98/18.61 % (2127978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.98/18.61 % (2127978)CaDiCaL version: 2.1.3 % 129.98/18.61 % (2127978)Termination reason: Instruction limit % 129.98/18.61 % (2127978)Termination phase: Saturation % 129.98/18.61 % (2127978)Time elapsed: 1.330 s % 129.98/18.61 % (2127978)Peak memory usage: 20 MB % 129.98/18.61 % (2127978)Instructions burned: 1472 (million) % 129.98/18.61 % (2127995)ott+11_1_sil=16000:gs=on:random_seed=1407634825:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 129.98/18.61 % (2127977)Instruction limit reached! % 129.98/18.61 % (2127977)------------------------------ % 129.98/18.61 % (2127977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.98/18.61 % (2127977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.98/18.61 % (2127977)CaDiCaL version: 2.1.3 % 129.98/18.61 % (2127977)Termination reason: Instruction limit % 129.98/18.61 % (2127977)Termination phase: Saturation % 129.98/18.61 % (2127977)Time elapsed: 2.625 s % 129.98/18.61 % (2127977)Peak memory usage: 42 MB % 129.98/18.61 % (2127977)Instructions burned: 5132 (million) % 129.98/18.61 % (2127997)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3681006589:fmbsr=1.6:i=67534_2965 on theBenchmark for (2965ds/67534Mi) % 129.98/18.61 % (2127997)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 129.98/18.61 % (2127997)Terminated due to inappropriate strategy. % 129.98/18.61 % (2127997)------------------------------ % 129.98/18.61 % (2127997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.98/18.61 % (2127997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.98/18.61 % (2127997)CaDiCaL version: 2.1.3 % 129.98/18.61 % (2127997)Termination reason: Inappropriate % 129.98/18.61 % (2127997)Time elapsed: 0.001 s % 129.98/18.61 % (2127997)Peak memory usage: 10 MB % 129.98/18.61 % (2127997)Instructions burned: 2 (million) % 129.98/18.61 % (2127997)------------------------------ % 129.98/18.61 % (2127997)------------------------------ % 129.98/18.61 % (2127999)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=762780420:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2965 on theBenchmark for (2965ds/4591Mi) % 129.98/18.61 % (2127991)Instruction limit reached! % 129.98/18.61 % (2127991)------------------------------ % 129.98/18.61 % (2127991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.98/18.61 % (2127991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.98/18.61 % (2127991)CaDiCaL version: 2.1.3 % 129.98/18.61 % (2127991)Termination reason: Instruction limit % 129.98/18.61 % (2127991)Termination phase: Saturation % 129.98/18.61 % (2127991)Time elapsed: 3.093 s % 129.98/18.61 % (2127991)Peak memory usage: 35 MB % 129.98/18.61 % (2127991)Instructions burned: 3512 (million) % 129.98/18.61 % (2128003)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=854288440:i=29340_2956 on theBenchmark for (2956ds/29340Mi) % 129.98/18.61 % (2127995)Instruction limit reached! % 129.98/18.61 % (2127995)------------------------------ % 129.98/18.61 % (2127995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.98/18.61 % (2127995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.98/18.61 % (2127995)CaDiCaL version: 2.1.3 % 129.98/18.61 % (2127995)Termination reason: Instruction limit % 155.56/22.21 % (2127995)Termination phase: Saturation % 155.56/22.21 % (2127995)Time elapsed: 2.181 s % 155.56/22.21 % (2127995)Peak memory usage: 22 MB % 155.56/22.21 % (2127995)Instructions burned: 2252 (million) % 155.56/22.21 % (2128005)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2799853028:i=5211_2956 on theBenchmark for (2956ds/5211Mi) % 155.56/22.21 % (2127993)Instruction limit reached! % 155.56/22.21 % (2127993)------------------------------ % 155.56/22.21 % (2127993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.56/22.21 % (2127993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.56/22.21 % (2127993)CaDiCaL version: 2.1.3 % 155.56/22.21 % (2127993)Termination reason: Instruction limit % 155.56/22.21 % (2127993)Termination phase: Saturation % 155.56/22.21 % (2127993)Time elapsed: 3.390 s % 155.56/22.21 % (2127993)Peak memory usage: 32 MB % 155.56/22.21 % (2127993)Instructions burned: 3774 (million) % 155.56/22.21 % (2128007)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1543472487:i=5497:nm=2_2947 on theBenchmark for (2947ds/5497Mi) % 155.56/22.21 % (2128007)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.56/22.21 % (2128007)Terminated due to inappropriate strategy. % 155.56/22.21 % (2128007)------------------------------ % 155.56/22.21 % (2128007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.56/22.21 % (2128007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.56/22.21 % (2128007)CaDiCaL version: 2.1.3 % 155.56/22.21 % (2128007)Termination reason: Inappropriate % 155.56/22.21 % (2128007)Time elapsed: 0.002 s % 155.56/22.21 % (2128007)Peak memory usage: 10 MB % 155.56/22.21 % (2128007)Instructions burned: 2 (million) % 155.56/22.21 % (2128007)------------------------------ % 155.56/22.21 % (2128007)------------------------------ % 155.56/22.21 % (2128009)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4020412915:fmbsr=2:i=46332_2947 on theBenchmark for (2947ds/46332Mi) % 155.56/22.21 % (2128009)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.56/22.21 % (2128009)Terminated due to inappropriate strategy. % 155.56/22.21 % (2128009)------------------------------ % 155.56/22.21 % (2128009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.56/22.21 % (2128009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.56/22.21 % (2128009)CaDiCaL version: 2.1.3 % 155.56/22.21 % (2128009)Termination reason: Inappropriate % 155.56/22.21 % (2128009)Time elapsed: 0.001 s % 155.56/22.21 % (2128009)Peak memory usage: 11 MB % 155.56/22.21 % (2128009)Instructions burned: 2 (million) % 155.56/22.21 % (2128009)------------------------------ % 155.56/22.21 % (2128009)------------------------------ % 155.56/22.21 % (2128011)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2908466200:i=14071_2946 on theBenchmark for (2946ds/14071Mi) % 155.56/22.21 % (2128011)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.56/22.21 % (2128011)Terminated due to inappropriate strategy. % 155.56/22.21 % (2128011)------------------------------ % 155.56/22.21 % (2128011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.56/22.21 % (2128011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.56/22.21 % (2128011)CaDiCaL version: 2.1.3 % 155.56/22.21 % (2128011)Termination reason: Inappropriate % 155.56/22.21 % (2128011)Time elapsed: 0.001 s % 155.56/22.21 % (2128011)Peak memory usage: 11 MB % 155.56/22.21 % (2128011)Instructions burned: 2 (million) % 155.56/22.21 % (2128011)------------------------------ % 155.56/22.21 % (2128011)------------------------------ % 155.56/22.21 % (2128013)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2088853041:i=22565:add=on:rawr=on_2946 on theBenchmark for (2946ds/22565Mi) % 155.56/22.21 % (2127999)Instruction limit reached! % 155.56/22.21 % (2127999)------------------------------ % 155.56/22.21 % (2127999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.56/22.21 % (2127999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.56/22.21 % (2127999)CaDiCaL version: 2.1.3 % 155.56/22.21 % (2127999)Termination reason: Instruction limit % 155.56/22.21 % (2127999)Termination phase: Saturation % 155.56/22.21 % (2127999)Time elapsed: 2.284 s % 155.56/22.21 % (2127999)Peak memory usage: 41 MB % 155.56/22.21 % (2127999)Instructions burned: 4592 (million) % 155.56/22.21 % (2128019)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=428746262:i=8173:av=off_2942 on theBenchmark for (2942ds/8173Mi) % 155.56/22.21 % (2127987)Instruction limit reached! % 156.29/22.32 % (2127987)------------------------------ % 156.29/22.32 % (2127987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.29/22.32 % (2127987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.29/22.32 % (2127987)CaDiCaL version: 2.1.3 % 156.29/22.32 % (2127987)Termination reason: Instruction limit % 156.29/22.32 % (2127987)Termination phase: Saturation % 156.29/22.32 % (2127987)Time elapsed: 5.262 s % 156.29/22.32 % (2127987)Peak memory usage: 33 MB % 156.29/22.32 % (2127987)Instructions burned: 5114 (million) % 156.29/22.32 % (2128021)dis+10_16:1_sil=16000:random_seed=3508197209:i=9155:fsr=off_2936 on theBenchmark for (2936ds/9155Mi) % 156.29/22.32 % (2128005)Instruction limit reached! % 156.29/22.32 % (2128005)------------------------------ % 156.29/22.32 % (2128005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.29/22.32 % (2128005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.29/22.32 % (2128005)CaDiCaL version: 2.1.3 % 156.29/22.32 % (2128005)Termination reason: Instruction limit % 156.29/22.32 % (2128005)Termination phase: Saturation % 156.29/22.32 % (2128005)Time elapsed: 4.731 s % 156.29/22.32 % (2128005)Peak memory usage: 52 MB % 156.29/22.32 % (2128005)Instructions burned: 5212 (million) % 156.29/22.32 % (2128025)ott-3_8_sil=64000:random_seed=1469828466:i=20139:bs=on_2908 on theBenchmark for (2908ds/20139Mi) % 156.29/22.32 % (2128019)Instruction limit reached! % 156.29/22.32 % (2128019)------------------------------ % 156.29/22.32 % (2128019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.29/22.32 % (2128019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.29/22.32 % (2128019)CaDiCaL version: 2.1.3 % 156.29/22.32 % (2128019)Termination reason: Instruction limit % 156.29/22.32 % (2128019)Termination phase: Saturation % 156.29/22.32 % (2128019)Time elapsed: 4.420 s % 156.29/22.32 % (2128019)Peak memory usage: 71 MB % 156.29/22.32 % (2128019)Instructions burned: 8174 (million) % 156.29/22.32 % (2128027)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3943158504:fmbsr=2:i=32576_2897 on theBenchmark for (2897ds/32576Mi) % 156.29/22.32 % (2128027)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.29/22.32 % (2128027)Terminated due to inappropriate strategy. % 156.29/22.32 % (2128027)------------------------------ % 156.29/22.32 % (2128027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.29/22.32 % (2128027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.29/22.32 % (2128027)CaDiCaL version: 2.1.3 % 156.29/22.32 % (2128027)Termination reason: Inappropriate % 156.29/22.32 % (2128027)Time elapsed: 0.001 s % 156.29/22.32 % (2128027)Peak memory usage: 11 MB % 156.29/22.32 % (2128027)Instructions burned: 2 (million) % 156.29/22.32 % (2128027)------------------------------ % 156.29/22.32 % (2128027)------------------------------ % 156.29/22.32 % (2128029)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3737576845:i=11404_2897 on theBenchmark for (2897ds/11404Mi) % 156.29/22.32 % (2128021)Instruction limit reached! % 156.29/22.32 % (2128021)------------------------------ % 156.29/22.32 % (2128021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.29/22.32 % (2128021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.29/22.32 % (2128021)CaDiCaL version: 2.1.3 % 156.29/22.32 % (2128021)Termination reason: Instruction limit % 156.29/22.32 % (2128021)Termination phase: Saturation % 156.29/22.32 % (2128021)Time elapsed: 7.679 s % 156.29/22.32 % (2128021)Peak memory usage: 52 MB % 156.29/22.32 % (2128021)Instructions burned: 9156 (million) % 156.29/22.32 % (2128098)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=206267587:i=14134_2859 on theBenchmark for (2859ds/14134Mi) % 156.29/22.32 % (2128029)Instruction limit reached! % 156.29/22.32 % (2128029)------------------------------ % 156.29/22.32 % (2128029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.29/22.32 % (2128029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.29/22.32 % (2128029)CaDiCaL version: 2.1.3 % 156.29/22.32 % (2128029)Termination reason: Instruction limit % 156.29/22.32 % (2128029)Termination phase: Saturation % 156.29/22.32 % (2128029)Time elapsed: 4.955 s % 156.29/22.32 % (2128029)Peak memory usage: 137 MB % 156.29/22.32 % (2128029)Instructions burned: 11407 (million) % 156.29/22.32 % (2128100)dis+33_16_sil=32000:sac=on:random_seed=4012387651:i=15851:nm=0_2847 on theBenchmark for (2847ds/15851Mi) % 156.29/22.32 % (2128013)Instruction limit reached! % 156.29/22.32 % (2128013)------------------------------ % 156.29/22.32 % (2128013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.99/27.56 % (2128013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.99/27.56 % (2128013)CaDiCaL version: 2.1.3 % 192.99/27.56 % (2128013)Termination reason: Instruction limit % 192.99/27.56 % (2128013)Termination phase: Saturation % 192.99/27.56 % (2128013)Time elapsed: 12.904 s % 192.99/27.56 % (2128013)Peak memory usage: 20 MB % 192.99/27.56 % (2128013)Instructions burned: 22567 (million) % 192.99/27.56 % (2128103)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2103061272:avsq=on:i=17627:add=on:amm=off_2817 on theBenchmark for (2817ds/17627Mi) % 192.99/27.56 % (2128100)Instruction limit reached! % 192.99/27.56 % (2128100)------------------------------ % 192.99/27.56 % (2128100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.99/27.56 % (2128100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.99/27.56 % (2128100)CaDiCaL version: 2.1.3 % 192.99/27.56 % (2128100)Termination reason: Instruction limit % 192.99/27.56 % (2128100)Termination phase: Saturation % 192.99/27.56 % (2128100)Time elapsed: 4.231 s % 192.99/27.56 % (2128100)Peak memory usage: 140 MB % 192.99/27.56 % (2128100)Instructions burned: 15853 (million) % 192.99/27.56 % (2128105)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2451012810:s2a=on:i=53295_2805 on theBenchmark for (2805ds/53295Mi) % 192.99/27.56 % (2128003)Instruction limit reached! % 192.99/27.56 % (2128003)------------------------------ % 192.99/27.56 % (2128003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.99/27.56 % (2128003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.99/27.56 % (2128003)CaDiCaL version: 2.1.3 % 192.99/27.56 % (2128003)Termination reason: Instruction limit % 192.99/27.56 % (2128003)Termination phase: Saturation % 192.99/27.56 % (2128003)Time elapsed: 16.057 s % 192.99/27.56 % (2128003)Peak memory usage: 149 MB % 192.99/27.56 % (2128003)Instructions burned: 29342 (million) % 192.99/27.56 % (2128107)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1725785885:i=26857:ins=20_2795 on theBenchmark for (2795ds/26857Mi) % 192.99/27.56 % (2128107)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.99/27.56 % (2128107)Terminated due to inappropriate strategy. % 192.99/27.56 % (2128107)------------------------------ % 192.99/27.56 % (2128107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.99/27.56 % (2128107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.99/27.56 % (2128107)CaDiCaL version: 2.1.3 % 192.99/27.56 % (2128107)Termination reason: Inappropriate % 192.99/27.56 % (2128107)Time elapsed: 0.001 s % 192.99/27.56 % (2128107)Peak memory usage: 10 MB % 192.99/27.56 % (2128107)Instructions burned: 2 (million) % 192.99/27.56 % (2128107)------------------------------ % 192.99/27.56 % (2128107)------------------------------ % 192.99/27.56 % (2128109)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2066365549:i=28120:bs=on:fsr=off_2795 on theBenchmark for (2795ds/28120Mi) % 192.99/27.56 % (2128025)Instruction limit reached! % 192.99/27.56 % (2128025)------------------------------ % 192.99/27.56 % (2128025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.99/27.56 % (2128025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.99/27.56 % (2128025)CaDiCaL version: 2.1.3 % 192.99/27.56 % (2128025)Termination reason: Instruction limit % 192.99/27.56 % (2128025)Termination phase: Saturation % 192.99/27.56 % (2128025)Time elapsed: 12.621 s % 192.99/27.56 % (2128025)Peak memory usage: 66 MB % 192.99/27.56 % (2128025)Instructions burned: 20139 (million) % 192.99/27.56 % (2128111)fmb+10_1_sil=256000:fmbss=7:random_seed=2471408894:fmbsr=1.6:i=182295_2781 on theBenchmark for (2781ds/182295Mi) % 192.99/27.56 % (2128111)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.99/27.56 % (2128111)Terminated due to inappropriate strategy. % 192.99/27.56 % (2128111)------------------------------ % 192.99/27.56 % (2128111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.99/27.56 % (2128111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.99/27.56 % (2128111)CaDiCaL version: 2.1.3 % 192.99/27.56 % (2128111)Termination reason: Inappropriate % 192.99/27.56 % (2128111)Time elapsed: 0.001 s % 192.99/27.56 % (2128111)Peak memory usage: 10 MB % 192.99/27.56 % (2128111)Instructions burned: 2 (million) % 192.99/27.56 % (2128111)------------------------------ % 192.99/27.56 % (2128111)------------------------------ % 192.99/27.56 % (2128113)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3821028962:i=44625:gsp=on_2781 on theBenchmark for (2781ds/44625Mi) % 206.64/29.46 % (2128113)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.64/29.46 % (2128113)Terminated due to inappropriate strategy. % 206.64/29.46 % (2128113)------------------------------ % 206.64/29.46 % (2128113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.64/29.46 % (2128113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.64/29.46 % (2128113)CaDiCaL version: 2.1.3 % 206.64/29.46 % (2128113)Termination reason: Inappropriate % 206.64/29.46 % (2128113)Time elapsed: 0.001 s % 206.64/29.46 % (2128113)Peak memory usage: 11 MB % 206.64/29.46 % (2128113)Instructions burned: 2 (million) % 206.64/29.46 % (2128113)------------------------------ % 206.64/29.46 % (2128113)------------------------------ % 206.64/29.46 % (2128115)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3298784185:i=160505_2781 on theBenchmark for (2781ds/160505Mi) % 206.64/29.46 % (2128115)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.64/29.46 % (2128115)Terminated due to inappropriate strategy. % 206.64/29.46 % (2128115)------------------------------ % 206.64/29.46 % (2128115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.64/29.46 % (2128115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.64/29.46 % (2128115)CaDiCaL version: 2.1.3 % 206.64/29.46 % (2128115)Termination reason: Inappropriate % 206.64/29.46 % (2128115)Time elapsed: 0.001 s % 206.64/29.46 % (2128115)Peak memory usage: 11 MB % 206.64/29.46 % (2128115)Instructions burned: 2 (million) % 206.64/29.46 % (2128115)------------------------------ % 206.64/29.46 % (2128115)------------------------------ % 206.64/29.46 % (2128117)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2641194473:fmbsr=1.3:i=225729_2781 on theBenchmark for (2781ds/225729Mi) % 206.64/29.46 % (2128117)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.64/29.46 % (2128117)Terminated due to inappropriate strategy. % 206.64/29.46 % (2128117)------------------------------ % 206.64/29.46 % (2128117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.64/29.46 % (2128117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.64/29.46 % (2128117)CaDiCaL version: 2.1.3 % 206.64/29.46 % (2128117)Termination reason: Inappropriate % 206.64/29.46 % (2128117)Time elapsed: 0.001 s % 206.64/29.46 % (2128117)Peak memory usage: 10 MB % 206.64/29.46 % (2128117)Instructions burned: 2 (million) % 206.64/29.46 % (2128117)------------------------------ % 206.64/29.46 % (2128117)------------------------------ % 206.64/29.46 % (2128119)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=504303805:fmbsr=2:i=185024:ins=7_2780 on theBenchmark for (2780ds/185024Mi) % 206.64/29.46 % (2128119)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.64/29.46 % (2128119)Terminated due to inappropriate strategy. % 206.64/29.46 % (2128119)------------------------------ % 206.64/29.46 % (2128119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.64/29.46 % (2128119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.64/29.46 % (2128119)CaDiCaL version: 2.1.3 % 206.64/29.46 % (2128119)Termination reason: Inappropriate % 206.64/29.46 % (2128119)Time elapsed: 0.001 s % 206.64/29.46 % (2128119)Peak memory usage: 10 MB % 206.64/29.46 % (2128119)Instructions burned: 2 (million) % 206.64/29.46 % (2128119)------------------------------ % 206.64/29.46 % (2128119)------------------------------ % 206.64/29.46 % (2128121)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=995468875:rtra=on_2780 on theBenchmark for (2780ds/0Mi) % 206.64/29.46 % (2128121)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.64/29.46 % (2128121)Terminated due to inappropriate strategy. % 206.64/29.46 % (2128121)------------------------------ % 206.64/29.46 % (2128121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.64/29.46 % (2128121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.64/29.46 % (2128121)CaDiCaL version: 2.1.3 % 206.64/29.46 % (2128121)Termination reason: Inappropriate % 206.64/29.46 % (2128121)Time elapsed: 0.001 s % 206.64/29.46 % (2128121)Peak memory usage: 10 MB % 206.64/29.46 % (2128121)Instructions burned: 2 (million) % 206.64/29.46 % (2128121)------------------------------ % 206.64/29.46 % (2128121)------------------------------ % 206.64/29.46 % (2128123)% WARNING: option uhcvi not known. % 206.64/29.46 % (2128123)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3969222126:i=271062:add=off:rtra=on:rawr=on_2780 on theBenchmark for (2780ds/271062Mi) % 226.52/32.28 % (2128098)Instruction limit reached! % 226.52/32.28 % (2128098)------------------------------ % 226.52/32.28 % (2128098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.52/32.28 % (2128098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.52/32.28 % (2128098)CaDiCaL version: 2.1.3 % 226.52/32.28 % (2128098)Termination reason: Instruction limit % 226.52/32.28 % (2128098)Termination phase: Saturation % 226.52/32.28 % (2128098)Time elapsed: 8.576 s % 226.52/32.28 % (2128098)Peak memory usage: 80 MB % 226.52/32.28 % (2128098)Instructions burned: 14134 (million) % 226.52/32.28 % (2128125)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1427672618:i=176048:add=on:rtra=on:rawr=on_2773 on theBenchmark for (2773ds/176048Mi) % 226.52/32.28 % (2128103)Instruction limit reached! % 226.52/32.28 % (2128103)------------------------------ % 226.52/32.28 % (2128103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.52/32.28 % (2128103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.52/32.28 % (2128103)CaDiCaL version: 2.1.3 % 226.52/32.28 % (2128103)Termination reason: Instruction limit % 226.52/32.28 % (2128103)Termination phase: Saturation % 226.52/32.28 % (2128103)Time elapsed: 8.162 s % 226.52/32.28 % (2128103)Peak memory usage: 221 MB % 226.52/32.28 % (2128103)Instructions burned: 17628 (million) % 226.52/32.28 % (2128214)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2710956517:i=206:fgj=on:rtra=on_2735 on theBenchmark for (2735ds/206Mi) % 226.52/32.28 % (2128214)Instruction limit reached! % 226.52/32.28 % (2128214)------------------------------ % 226.52/32.28 % (2128214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.52/32.28 % (2128214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.52/32.28 % (2128214)CaDiCaL version: 2.1.3 % 226.52/32.28 % (2128214)Termination reason: Instruction limit % 226.52/32.28 % (2128214)Termination phase: Saturation % 226.52/32.28 % (2128214)Time elapsed: 0.126 s % 226.52/32.28 % (2128214)Peak memory usage: 13 MB % 226.52/32.28 % (2128214)Instructions burned: 206 (million) % 226.52/32.28 % (2128216)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1523742733:i=232:rtra=on_2733 on theBenchmark for (2733ds/232Mi) % 226.52/32.28 % (2128216)Instruction limit reached! % 226.52/32.28 % (2128216)------------------------------ % 226.52/32.28 % (2128216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.52/32.28 % (2128216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.52/32.28 % (2128216)CaDiCaL version: 2.1.3 % 226.52/32.28 % (2128216)Termination reason: Instruction limit % 226.52/32.28 % (2128216)Termination phase: Saturation % 226.52/32.28 % (2128216)Time elapsed: 0.145 s % 226.52/32.28 % (2128216)Peak memory usage: 13 MB % 226.52/32.28 % (2128216)Instructions burned: 232 (million) % 226.52/32.28 % (2128218)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2921764752:i=262:rtra=on_2732 on theBenchmark for (2732ds/262Mi) % 226.52/32.28 % (2128218)Instruction limit reached! % 226.52/32.28 % (2128218)------------------------------ % 226.52/32.28 % (2128218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.52/32.28 % (2128218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.52/32.28 % (2128218)CaDiCaL version: 2.1.3 % 226.52/32.28 % (2128218)Termination reason: Instruction limit % 226.52/32.28 % (2128218)Termination phase: Saturation % 226.52/32.28 % (2128218)Time elapsed: 0.161 s % 226.52/32.28 % (2128218)Peak memory usage: 14 MB % 226.52/32.28 % (2128218)Instructions burned: 263 (million) % 226.52/32.28 % (2128220)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=129894279:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2730 on theBenchmark for (2730ds/318Mi) % 226.52/32.28 % (2128220)Instruction limit reached! % 226.52/32.28 % (2128220)------------------------------ % 226.52/32.28 % (2128220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 226.52/32.28 % (2128220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.52/32.28 % (2128220)CaDiCaL version: 2.1.3 % 226.52/32.28 % (2128220)Termination reason: Instruction limit % 226.52/32.28 % (2128220)Termination phase: Saturation % 226.52/32.28 % (2128220)Time elapsed: 0.210 s % 226.52/32.28 % (2128220)Peak memory usage: 15 MB % 226.52/32.28 % (2128220)Instructions burned: 318 (million) % 226.52/32.28 % (2128222)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3861142786:i=1428:nm=2:rtra=on_2727 on theBenchmark for (2727ds/1428Mi) % 235.74/33.56 % (2128222)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 235.74/33.56 % (2128222)Terminated due to inappropriate strategy. % 235.74/33.56 % (2128222)------------------------------ % 235.74/33.56 % (2128222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.74/33.56 % (2128222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.74/33.56 % (2128222)CaDiCaL version: 2.1.3 % 235.74/33.56 % (2128222)Termination reason: Inappropriate % 235.74/33.56 % (2128222)Time elapsed: 0.001 s % 235.74/33.56 % (2128222)Peak memory usage: 10 MB % 235.74/33.56 % (2128222)Instructions burned: 2 (million) % 235.74/33.56 % (2128222)------------------------------ % 235.74/33.56 % (2128222)------------------------------ % 235.74/33.56 % (2128224)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=161858968:i=262:bd=preordered:rtra=on:fsd=on_2727 on theBenchmark for (2727ds/262Mi) % 235.74/33.56 % (2128224)Instruction limit reached! % 235.74/33.56 % (2128224)------------------------------ % 235.74/33.56 % (2128224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.74/33.56 % (2128224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.74/33.56 % (2128224)CaDiCaL version: 2.1.3 % 235.74/33.56 % (2128224)Termination reason: Instruction limit % 235.74/33.56 % (2128224)Termination phase: Saturation % 235.74/33.56 % (2128224)Time elapsed: 0.158 s % 235.74/33.56 % (2128224)Peak memory usage: 13 MB % 235.74/33.56 % (2128224)Instructions burned: 263 (million) % 235.74/33.56 % (2128226)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=2852561508:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2725 on theBenchmark for (2725ds/1368Mi) % 235.74/33.56 % (2128226)Instruction limit reached! % 235.74/33.56 % (2128226)------------------------------ % 235.74/33.56 % (2128226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.74/33.56 % (2128226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.74/33.56 % (2128226)CaDiCaL version: 2.1.3 % 235.74/33.56 % (2128226)Termination reason: Instruction limit % 235.74/33.56 % (2128226)Termination phase: Saturation % 235.74/33.56 % (2128226)Time elapsed: 0.856 s % 235.74/33.56 % (2128226)Peak memory usage: 21 MB % 235.74/33.56 % (2128226)Instructions burned: 1368 (million) % 235.74/33.56 % (2128228)ott-21_1_sil=16000:si=on:fs=off:random_seed=1737187329:i=360:av=off:fsr=off:rtra=on_2717 on theBenchmark for (2717ds/360Mi) % 235.74/33.56 % (2128228)Instruction limit reached! % 235.74/33.56 % (2128228)------------------------------ % 235.74/33.56 % (2128228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.74/33.56 % (2128228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.74/33.56 % (2128228)CaDiCaL version: 2.1.3 % 235.74/33.56 % (2128228)Termination reason: Instruction limit % 235.74/33.56 % (2128228)Termination phase: Saturation % 235.74/33.56 % (2128228)Time elapsed: 0.161 s % 235.74/33.56 % (2128228)Peak memory usage: 13 MB % 235.74/33.56 % (2128228)Instructions burned: 362 (million) % 235.74/33.56 % (2128230)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3224491717:i=954:bd=all:rtra=on_2715 on theBenchmark for (2715ds/954Mi) % 235.74/33.56 % (2128230)Instruction limit reached! % 235.74/33.56 % (2128230)------------------------------ % 235.74/33.56 % (2128230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.74/33.56 % (2128230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.74/33.56 % (2128230)CaDiCaL version: 2.1.3 % 235.74/33.56 % (2128230)Termination reason: Instruction limit % 235.74/33.56 % (2128230)Termination phase: Saturation % 235.74/33.56 % (2128230)Time elapsed: 0.617 s % 235.74/33.56 % (2128230)Peak memory usage: 15 MB % 235.74/33.56 % (2128230)Instructions burned: 954 (million) % 235.74/33.56 % (2128234)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=22484712:fmbsr=1.3:i=1730:ins=25:rtra=on_2708 on theBenchmark for (2708ds/1730Mi) % 235.74/33.56 % (2128234)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 235.74/33.56 % (2128234)Terminated due to inappropriate strategy. % 235.74/33.56 % (2128234)------------------------------ % 235.74/33.56 % (2128234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.74/33.56 % (2128234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.74/33.56 % (2128234)CaDiCaL version: 2.1.3 % 235.74/33.56 % (2128234)Termination reason: Inappropriate % 235.74/33.56 % (2128234)Time elapsed: 0.001 s % 266.26/37.81 % (2128234)Peak memory usage: 10 MB % 266.26/37.81 % (2128234)Instructions burned: 2 (million) % 266.26/37.81 % (2128234)------------------------------ % 266.26/37.81 % (2128234)------------------------------ % 266.26/37.81 % (2128236)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3054869807:i=2358:rtra=on_2708 on theBenchmark for (2708ds/2358Mi) % 266.26/37.81 % (2128236)Instruction limit reached! % 266.26/37.81 % (2128236)------------------------------ % 266.26/37.81 % (2128236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.26/37.81 % (2128236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.26/37.81 % (2128236)CaDiCaL version: 2.1.3 % 266.26/37.81 % (2128236)Termination reason: Instruction limit % 266.26/37.81 % (2128236)Termination phase: Saturation % 266.26/37.81 % (2128236)Time elapsed: 0.962 s % 266.26/37.81 % (2128236)Peak memory usage: 17 MB % 266.26/37.81 % (2128236)Instructions burned: 2360 (million) % 266.26/37.81 % (2128298)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4279624725:i=1778:ins=1:rtra=on_2698 on theBenchmark for (2698ds/1778Mi) % 266.26/37.81 % (2128298)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 266.26/37.81 % (2128298)Terminated due to inappropriate strategy. % 266.26/37.81 % (2128298)------------------------------ % 266.26/37.81 % (2128298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.26/37.81 % (2128298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.26/37.81 % (2128298)CaDiCaL version: 2.1.3 % 266.26/37.81 % (2128298)Termination reason: Inappropriate % 266.26/37.81 % (2128298)Time elapsed: 0.001 s % 266.26/37.81 % (2128298)Peak memory usage: 10 MB % 266.26/37.81 % (2128298)Instructions burned: 2 (million) % 266.26/37.81 % (2128298)------------------------------ % 266.26/37.81 % (2128298)------------------------------ % 266.26/37.81 % (2128300)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=1289861527:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2698 on theBenchmark for (2698ds/1384Mi) % 266.26/37.81 % (2128300)Instruction limit reached! % 266.26/37.81 % (2128300)------------------------------ % 266.26/37.81 % (2128300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.26/37.81 % (2128300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.26/37.81 % (2128300)CaDiCaL version: 2.1.3 % 266.26/37.81 % (2128300)Termination reason: Instruction limit % 266.26/37.81 % (2128300)Termination phase: Saturation % 266.26/37.81 % (2128300)Time elapsed: 0.822 s % 266.26/37.81 % (2128300)Peak memory usage: 20 MB % 266.26/37.81 % (2128300)Instructions burned: 1384 (million) % 266.26/37.81 % (2128302)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1685209800:i=1758:kws=inv_precedence:fsr=off:rtra=on_2690 on theBenchmark for (2690ds/1758Mi) % 266.26/37.81 % (2128105)Instruction limit reached! % 266.26/37.81 % (2128105)------------------------------ % 266.26/37.81 % (2128105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.26/37.81 % (2128105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.26/37.81 % (2128105)CaDiCaL version: 2.1.3 % 266.26/37.81 % (2128105)Termination reason: Instruction limit % 266.26/37.81 % (2128105)Termination phase: Saturation % 266.26/37.81 % (2128105)Time elapsed: 12.391 s % 266.26/37.81 % (2128105)Peak memory usage: 411 MB % 266.26/37.81 % (2128105)Instructions burned: 53297 (million) % 266.26/37.81 % (2128304)fmb+10_1_sil=64000:si=on:random_seed=384912480:i=44122:nm=2:rtra=on:gsp=on_2680 on theBenchmark for (2680ds/44122Mi) % 266.26/37.81 % (2128304)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 266.26/37.81 % (2128304)Terminated due to inappropriate strategy. % 266.26/37.81 % (2128304)------------------------------ % 266.26/37.81 % (2128304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.26/37.81 % (2128304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.26/37.81 % (2128304)CaDiCaL version: 2.1.3 % 266.26/37.81 % (2128304)Termination reason: Inappropriate % 266.26/37.81 % (2128304)Time elapsed: 0.001 s % 266.26/37.81 % (2128304)Peak memory usage: 10 MB % 266.26/37.81 % (2128304)Instructions burned: 2 (million) % 266.26/37.81 % (2128304)------------------------------ % 266.26/37.81 % (2128304)------------------------------ % 266.26/37.81 % (2128306)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2701267431:i=19030:nm=5:rtra=on_2680 on theBenchmark foTerminated % 300.30/42.64 % Vampire exiting %------------------------------------------------------------------------------