%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW741_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:41 PM UTC 2026 % Result : Timeout 300.07s 42.73s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWW741_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.00/0.11 % Computer : n012.cluster.edu % 0.00/0.11 % Model : x86_64 x86_64 % 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.11 % Memory : 8046.5625MB % 0.00/0.11 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 14:28:34 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.13 Running first-order model finding % 0.08/0.13 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.90/0.58 % (3414816)Will run a generic schedule for satisfiability detection. % 2.90/0.58 % (3414827)% WARNING: option uhcvi not known. % 2.90/0.58 % (3414827)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1095131922:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.90/0.58 % (3414829)dis+10_1_sil=32000:sp=arity:random_seed=1999849507:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.90/0.58 % (3414830)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2680388963:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.90/0.58 % (3414832)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2843605031:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.90/0.58 % (3414833)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2907919237:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.90/0.58 % (3414828)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2432743252:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.90/0.58 % (3414826)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1087845756_2999 on theBenchmark for (2999ds/0Mi) % 2.90/0.58 % (3414829)Instruction limit reached! % 2.90/0.58 % (3414829)------------------------------ % 2.90/0.58 % (3414829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.90/0.58 % (3414829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.90/0.58 % (3414829)CaDiCaL version: 2.1.3 % 2.90/0.58 % (3414829)Termination reason: Instruction limit % 2.90/0.58 % (3414829)Termination phase: Saturation % 2.90/0.58 % (3414829)Time elapsed: 0.029 s % 2.90/0.58 % (3414829)Peak memory usage: 14 MB % 2.90/0.58 % (3414829)Instructions burned: 106 (million) % 2.90/0.58 % (3414826)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.90/0.58 % (3414826)Terminated due to inappropriate strategy. % 2.90/0.58 % (3414826)------------------------------ % 2.90/0.58 % (3414826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.90/0.58 % (3414826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.90/0.58 % (3414826)CaDiCaL version: 2.1.3 % 2.90/0.58 % (3414826)Termination reason: Inappropriate % 2.90/0.58 % (3414826)Time elapsed: 0.028 s % 2.90/0.58 % (3414826)Peak memory usage: 12 MB % 2.90/0.58 % (3414826)Instructions burned: 109 (million) % 2.90/0.58 % (3414830)Instruction limit reached! % 2.90/0.58 % (3414830)------------------------------ % 2.90/0.58 % (3414830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.90/0.58 % (3414830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.90/0.58 % (3414830)CaDiCaL version: 2.1.3 % 2.90/0.58 % (3414830)Termination reason: Instruction limit % 2.90/0.58 % (3414830)Termination phase: Blocked clause elimination % 2.90/0.58 % (3414830)Time elapsed: 0.029 s % 2.90/0.58 % (3414830)Peak memory usage: 11 MB % 2.90/0.58 % (3414830)Instructions burned: 119 (million) % 2.90/0.58 % (3414826)------------------------------ % 2.90/0.58 % (3414826)------------------------------ % 2.90/0.58 % (3414832)Instruction limit reached! % 2.90/0.58 % (3414832)------------------------------ % 2.90/0.58 % (3414832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.90/0.58 % (3414832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.90/0.58 % (3414832)CaDiCaL version: 2.1.3 % 2.90/0.58 % (3414832)Termination reason: Instruction limit % 2.90/0.58 % (3414832)Termination phase: Saturation % 2.90/0.58 % (3414832)Time elapsed: 0.037 s % 2.90/0.58 % (3414832)Peak memory usage: 15 MB % 2.90/0.58 % (3414832)Instructions burned: 134 (million) % 2.90/0.58 % (3414858)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=662583749:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.90/0.58 % (3414859)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2632529074:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.90/0.58 % (3414860)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=1994883515:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.90/0.58 % (3414858)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.90/0.58 % (3414858)Terminated due to inappropriate strategy. % 2.90/0.58 % (3414858)------------------------------ % 2.90/0.58 % (3414858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.32/0.85 % (3414858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.32/0.85 % (3414858)CaDiCaL version: 2.1.3 % 4.32/0.85 % (3414858)Termination reason: Inappropriate % 4.32/0.85 % (3414858)Time elapsed: 0.007 s % 4.32/0.85 % (3414858)Peak memory usage: 11 MB % 4.32/0.85 % (3414858)Instructions burned: 29 (million) % 4.32/0.85 % (3414858)------------------------------ % 4.32/0.85 % (3414858)------------------------------ % 4.32/0.85 % (3414864)ott-21_1_sil=16000:fs=off:random_seed=3076947820:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 4.32/0.85 % (3414833)Instruction limit reached! % 4.32/0.85 % (3414833)------------------------------ % 4.32/0.85 % (3414833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.32/0.85 % (3414833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.32/0.85 % (3414833)CaDiCaL version: 2.1.3 % 4.32/0.85 % (3414833)Termination reason: Instruction limit % 4.32/0.85 % (3414833)Termination phase: Saturation % 4.32/0.85 % (3414833)Time elapsed: 0.052 s % 4.32/0.85 % (3414833)Peak memory usage: 15 MB % 4.32/0.85 % (3414833)Instructions burned: 160 (million) % 4.32/0.85 % (3414876)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2542527086:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 4.32/0.85 % (3414873)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2185163041:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 4.32/0.85 % (3414876)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.32/0.85 % (3414876)Terminated due to inappropriate strategy. % 4.32/0.85 % (3414876)------------------------------ % 4.32/0.85 % (3414876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.32/0.85 % (3414876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.32/0.85 % (3414876)CaDiCaL version: 2.1.3 % 4.32/0.85 % (3414876)Termination reason: Inappropriate % 4.32/0.85 % (3414876)Time elapsed: 0.009 s % 4.32/0.85 % (3414876)Peak memory usage: 12 MB % 4.32/0.85 % (3414876)Instructions burned: 38 (million) % 4.32/0.85 % (3414876)------------------------------ % 4.32/0.85 % (3414876)------------------------------ % 4.32/0.85 % (3414859)Instruction limit reached! % 4.32/0.85 % (3414859)------------------------------ % 4.32/0.85 % (3414859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.32/0.85 % (3414859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.32/0.85 % (3414859)CaDiCaL version: 2.1.3 % 4.32/0.85 % (3414859)Termination reason: Instruction limit % 4.32/0.85 % (3414859)Termination phase: Saturation % 4.32/0.85 % (3414859)Time elapsed: 0.035 s % 4.32/0.85 % (3414859)Peak memory usage: 13 MB % 4.32/0.85 % (3414859)Instructions burned: 132 (million) % 4.32/0.85 % (3414888)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1638571427:i=1179_2999 on theBenchmark for (2999ds/1179Mi) % 4.32/0.85 % (3414889)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2777143955:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.32/0.85 % (3414889)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.32/0.85 % (3414889)Terminated due to inappropriate strategy. % 4.32/0.85 % (3414889)------------------------------ % 4.32/0.85 % (3414889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.32/0.85 % (3414889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.32/0.85 % (3414889)CaDiCaL version: 2.1.3 % 4.32/0.85 % (3414889)Termination reason: Inappropriate % 4.32/0.85 % (3414889)Time elapsed: 0.008 s % 4.32/0.85 % (3414889)Peak memory usage: 11 MB % 4.32/0.85 % (3414889)Instructions burned: 32 (million) % 4.32/0.85 % (3414889)------------------------------ % 4.32/0.85 % (3414889)------------------------------ % 4.32/0.85 % (3414864)Instruction limit reached! % 4.32/0.85 % (3414864)------------------------------ % 4.32/0.85 % (3414864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.32/0.85 % (3414864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.32/0.85 % (3414864)CaDiCaL version: 2.1.3 % 4.32/0.85 % (3414864)Termination reason: Instruction limit % 4.32/0.85 % (3414864)Termination phase: Saturation % 4.32/0.85 % (3414864)Time elapsed: 0.057 s % 4.32/0.85 % (3414864)Peak memory usage: 13 MB % 4.32/0.85 % (3414864)Instructions burned: 180 (million) % 4.32/0.85 % (3414901)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=1902764780:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 13.85/2.12 % (3414902)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2691453940:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 13.85/2.12 % (3414873)Instruction limit reached! % 13.85/2.12 % (3414873)------------------------------ % 13.85/2.12 % (3414873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.85/2.12 % (3414873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.12 % (3414873)CaDiCaL version: 2.1.3 % 13.85/2.12 % (3414873)Termination reason: Instruction limit % 13.85/2.12 % (3414873)Termination phase: Saturation % 13.85/2.12 % (3414873)Time elapsed: 0.200 s % 13.85/2.12 % (3414873)Peak memory usage: 16 MB % 13.85/2.12 % (3414873)Instructions burned: 478 (million) % 13.85/2.12 % (3414929)fmb+10_1_sil=64000:random_seed=3129143630:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 13.85/2.12 % (3414929)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.85/2.12 % (3414929)Terminated due to inappropriate strategy. % 13.85/2.12 % (3414929)------------------------------ % 13.85/2.12 % (3414929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.85/2.12 % (3414929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.12 % (3414929)CaDiCaL version: 2.1.3 % 13.85/2.12 % (3414929)Termination reason: Inappropriate % 13.85/2.12 % (3414929)Time elapsed: 0.014 s % 13.85/2.12 % (3414929)Peak memory usage: 11 MB % 13.85/2.12 % (3414929)Instructions burned: 31 (million) % 13.85/2.12 % (3414929)------------------------------ % 13.85/2.12 % (3414929)------------------------------ % 13.85/2.12 % (3414934)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1419880005:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 13.85/2.12 % (3414934)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.85/2.12 % (3414934)Terminated due to inappropriate strategy. % 13.85/2.12 % (3414934)------------------------------ % 13.85/2.12 % (3414934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.85/2.12 % (3414934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.12 % (3414934)CaDiCaL version: 2.1.3 % 13.85/2.12 % (3414934)Termination reason: Inappropriate % 13.85/2.12 % (3414934)Time elapsed: 0.013 s % 13.85/2.12 % (3414934)Peak memory usage: 11 MB % 13.85/2.12 % (3414934)Instructions burned: 30 (million) % 13.85/2.12 % (3414934)------------------------------ % 13.85/2.12 % (3414934)------------------------------ % 13.85/2.12 % (3414939)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3551912284:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 13.85/2.12 % (3414860)Instruction limit reached! % 13.85/2.12 % (3414860)------------------------------ % 13.85/2.12 % (3414860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.85/2.12 % (3414860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.12 % (3414860)CaDiCaL version: 2.1.3 % 13.85/2.12 % (3414860)Termination reason: Instruction limit % 13.85/2.12 % (3414860)Termination phase: Saturation % 13.85/2.12 % (3414860)Time elapsed: 0.325 s % 13.85/2.12 % (3414860)Peak memory usage: 18 MB % 13.85/2.12 % (3414860)Instructions burned: 685 (million) % 13.85/2.12 % (3414939)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 13.85/2.12 % (3414939)Terminated due to inappropriate strategy. % 13.85/2.12 % (3414939)------------------------------ % 13.85/2.12 % (3414939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.85/2.12 % (3414939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.85/2.12 % (3414939)CaDiCaL version: 2.1.3 % 13.85/2.12 % (3414939)Termination reason: Inappropriate % 13.85/2.12 % (3414939)Time elapsed: 0.014 s % 13.85/2.12 % (3414939)Peak memory usage: 11 MB % 13.85/2.12 % (3414939)Instructions burned: 32 (million) % 13.85/2.12 % (3414939)------------------------------ % 13.85/2.12 % (3414939)------------------------------ % 13.85/2.12 % (3414943)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3791473115:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 13.85/2.12 % (3414944)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3597589771:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 13.85/2.12 % (3414901)Instruction limit reached! % 15.41/2.44 % (3414901)------------------------------ % 15.41/2.44 % (3414901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.41/2.44 % (3414901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.41/2.44 % (3414901)CaDiCaL version: 2.1.3 % 15.41/2.44 % (3414901)Termination reason: Instruction limit % 15.41/2.44 % (3414901)Termination phase: Saturation % 15.41/2.44 % (3414901)Time elapsed: 0.310 s % 15.41/2.44 % (3414901)Peak memory usage: 19 MB % 15.41/2.44 % (3414901)Instructions burned: 693 (million) % 15.41/2.44 % (3414949)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3530401512:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 15.41/2.44 % (3414949)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.41/2.44 % (3414949)Terminated due to inappropriate strategy. % 15.41/2.44 % (3414949)------------------------------ % 15.41/2.44 % (3414949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.41/2.44 % (3414949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.41/2.44 % (3414949)CaDiCaL version: 2.1.3 % 15.41/2.44 % (3414949)Termination reason: Inappropriate % 15.41/2.44 % (3414949)Time elapsed: 0.028 s % 15.41/2.44 % (3414949)Peak memory usage: 12 MB % 15.41/2.44 % (3414949)Instructions burned: 108 (million) % 15.41/2.44 % (3414949)------------------------------ % 15.41/2.44 % (3414949)------------------------------ % 15.41/2.44 % (3414951)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1716826120:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 15.41/2.44 % (3414951)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.41/2.44 % (3414951)Terminated due to inappropriate strategy. % 15.41/2.44 % (3414951)------------------------------ % 15.41/2.44 % (3414951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.41/2.44 % (3414951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.41/2.44 % (3414951)CaDiCaL version: 2.1.3 % 15.41/2.44 % (3414951)Termination reason: Inappropriate % 15.41/2.44 % (3414951)Time elapsed: 0.016 s % 15.41/2.44 % (3414951)Peak memory usage: 11 MB % 15.41/2.44 % (3414951)Instructions burned: 32 (million) % 15.41/2.44 % (3414951)------------------------------ % 15.41/2.44 % (3414951)------------------------------ % 15.41/2.44 % (3414902)Instruction limit reached! % 15.41/2.44 % (3414902)------------------------------ % 15.41/2.44 % (3414902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.41/2.44 % (3414902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.41/2.44 % (3414902)CaDiCaL version: 2.1.3 % 15.41/2.44 % (3414902)Termination reason: Instruction limit % 15.41/2.44 % (3414902)Termination phase: Saturation % 15.41/2.44 % (3414902)Time elapsed: 0.383 s % 15.41/2.44 % (3414902)Peak memory usage: 20 MB % 15.41/2.44 % (3414902)Instructions burned: 880 (million) % 15.41/2.44 % (3414955)ott-2_1_sil=16000:newcnf=on:random_seed=1447121791:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 15.41/2.44 % (3414956)ott+10_1_sil=32000:tgt=ground:random_seed=3471098017:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 15.41/2.44 % (3414888)Instruction limit reached! % 15.41/2.44 % (3414888)------------------------------ % 15.41/2.44 % (3414888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.41/2.44 % (3414888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.41/2.44 % (3414888)CaDiCaL version: 2.1.3 % 15.41/2.44 % (3414888)Termination reason: Instruction limit % 15.41/2.44 % (3414888)Termination phase: Saturation % 15.41/2.44 % (3414888)Time elapsed: 0.544 s % 15.41/2.44 % (3414888)Peak memory usage: 20 MB % 15.41/2.44 % (3414888)Instructions burned: 1179 (million) % 15.41/2.44 % (3414965)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2086625418:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 15.41/2.44 % (3414965)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.41/2.44 % (3414965)Terminated due to inappropriate strategy. % 15.41/2.44 % (3414965)------------------------------ % 15.41/2.44 % (3414965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.41/2.44 % (3414965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.41/2.44 % (3414965)CaDiCaL version: 2.1.3 % 15.41/2.44 % (3414965)Termination reason: Inappropriate % 15.41/2.44 % (3414965)Time elapsed: 0.047 s % 15.41/2.44 % (3414965)Peak memory usage: 12 MB % 15.41/2.44 % (3414965)Instructions burned: 109 (million) % 65.21/9.44 % (3414965)------------------------------ % 65.21/9.44 % (3414965)------------------------------ % 65.21/9.44 % (3414969)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2644143655:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 65.21/9.44 % (3414955)Instruction limit reached! % 65.21/9.44 % (3414955)------------------------------ % 65.21/9.44 % (3414955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.21/9.44 % (3414955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.21/9.44 % (3414955)CaDiCaL version: 2.1.3 % 65.21/9.44 % (3414955)Termination reason: Instruction limit % 65.21/9.44 % (3414955)Termination phase: Saturation % 65.21/9.44 % (3414955)Time elapsed: 0.359 s % 65.21/9.44 % (3414955)Peak memory usage: 20 MB % 65.21/9.44 % (3414955)Instructions burned: 869 (million) % 65.21/9.44 % (3414995)dis+21_1_sil=32000:sas=cadical:random_seed=276077089:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 65.21/9.44 % (3414944)Instruction limit reached! % 65.21/9.44 % (3414944)------------------------------ % 65.21/9.44 % (3414944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.21/9.44 % (3414944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.21/9.44 % (3414944)CaDiCaL version: 2.1.3 % 65.21/9.44 % (3414944)Termination reason: Instruction limit % 65.21/9.44 % (3414944)Termination phase: Saturation % 65.21/9.44 % (3414944)Time elapsed: 0.573 s % 65.21/9.44 % (3414944)Peak memory usage: 28 MB % 65.21/9.44 % (3414944)Instructions burned: 1473 (million) % 65.21/9.44 % (3415038)ott+11_1_sil=16000:gs=on:random_seed=2141760712:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2990 on theBenchmark for (2990ds/2251Mi) % 65.21/9.44 % (3415038)Instruction limit reached! % 65.21/9.44 % (3415038)------------------------------ % 65.21/9.44 % (3415038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.21/9.44 % (3415038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.21/9.44 % (3415038)CaDiCaL version: 2.1.3 % 65.21/9.44 % (3415038)Termination reason: Instruction limit % 65.21/9.44 % (3415038)Termination phase: Saturation % 65.21/9.44 % (3415038)Time elapsed: 0.687 s % 65.21/9.44 % (3415038)Peak memory usage: 26 MB % 65.21/9.44 % (3415038)Instructions burned: 2253 (million) % 65.21/9.44 % (3415128)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1958965927:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi) % 65.21/9.44 % (3415128)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 65.21/9.44 % (3415128)Terminated due to inappropriate strategy. % 65.21/9.44 % (3415128)------------------------------ % 65.21/9.44 % (3415128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.21/9.44 % (3415128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.21/9.44 % (3415128)CaDiCaL version: 2.1.3 % 65.21/9.44 % (3415128)Termination reason: Inappropriate % 65.21/9.44 % (3415128)Time elapsed: 0.007 s % 65.21/9.44 % (3415128)Peak memory usage: 11 MB % 65.21/9.44 % (3415128)Instructions burned: 32 (million) % 65.21/9.44 % (3415128)------------------------------ % 65.21/9.44 % (3415128)------------------------------ % 65.21/9.44 % (3415130)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4203682049:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 65.21/9.44 % (3414969)Instruction limit reached! % 65.21/9.44 % (3414969)------------------------------ % 65.21/9.44 % (3414969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.21/9.44 % (3414969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.21/9.44 % (3414969)CaDiCaL version: 2.1.3 % 65.21/9.44 % (3414969)Termination reason: Instruction limit % 65.21/9.44 % (3414969)Termination phase: Saturation % 65.21/9.44 % (3414969)Time elapsed: 1.040 s % 65.21/9.44 % (3414969)Peak memory usage: 31 MB % 65.21/9.44 % (3414969)Instructions burned: 3516 (million) % 65.21/9.44 % (3415132)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3721448848:i=29340_2982 on theBenchmark for (2982ds/29340Mi) % 65.21/9.44 % (3414995)Instruction limit reached! % 65.21/9.44 % (3414995)------------------------------ % 65.21/9.44 % (3414995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.21/9.44 % (3414995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.21/9.44 % (3414995)CaDiCaL version: 2.1.3 % 76.63/11.11 % (3414995)Termination reason: Instruction limit % 76.63/11.11 % (3414995)Termination phase: Saturation % 76.63/11.11 % (3414995)Time elapsed: 1.084 s % 76.63/11.11 % (3414995)Peak memory usage: 33 MB % 76.63/11.11 % (3414995)Instructions burned: 3775 (million) % 76.63/11.11 % (3415134)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1382670249:i=5211_2980 on theBenchmark for (2980ds/5211Mi) % 76.63/11.11 % (3414943)Instruction limit reached! % 76.63/11.11 % (3414943)------------------------------ % 76.63/11.11 % (3414943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.63/11.11 % (3414943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.63/11.11 % (3414943)CaDiCaL version: 2.1.3 % 76.63/11.11 % (3414943)Termination reason: Instruction limit % 76.63/11.11 % (3414943)Termination phase: Saturation % 76.63/11.11 % (3414943)Time elapsed: 1.600 s % 76.63/11.11 % (3414943)Peak memory usage: 41 MB % 76.63/11.11 % (3414943)Instructions burned: 5132 (million) % 76.63/11.11 % (3415136)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=924363550:i=5497:nm=2_2979 on theBenchmark for (2979ds/5497Mi) % 76.63/11.11 % (3415136)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 76.63/11.11 % (3415136)Terminated due to inappropriate strategy. % 76.63/11.11 % (3415136)------------------------------ % 76.63/11.11 % (3415136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.63/11.11 % (3415136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.63/11.11 % (3415136)CaDiCaL version: 2.1.3 % 76.63/11.11 % (3415136)Termination reason: Inappropriate % 76.63/11.11 % (3415136)Time elapsed: 0.017 s % 76.63/11.11 % (3415136)Peak memory usage: 11 MB % 76.63/11.11 % (3415136)Instructions burned: 68 (million) % 76.63/11.11 % (3415136)------------------------------ % 76.63/11.11 % (3415136)------------------------------ % 76.63/11.11 % (3415138)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2203923265:fmbsr=2:i=46332_2979 on theBenchmark for (2979ds/46332Mi) % 76.63/11.11 % (3415138)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 76.63/11.11 % (3415138)Terminated due to inappropriate strategy. % 76.63/11.11 % (3415138)------------------------------ % 76.63/11.11 % (3415138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.63/11.11 % (3415138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.63/11.11 % (3415138)CaDiCaL version: 2.1.3 % 76.63/11.11 % (3415138)Termination reason: Inappropriate % 76.63/11.11 % (3415138)Time elapsed: 0.007 s % 76.63/11.11 % (3415138)Peak memory usage: 11 MB % 76.63/11.11 % (3415138)Instructions burned: 32 (million) % 76.63/11.11 % (3415138)------------------------------ % 76.63/11.11 % (3415138)------------------------------ % 76.63/11.11 % (3415140)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3095041080:i=14071_2979 on theBenchmark for (2979ds/14071Mi) % 76.63/11.11 % (3415140)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 76.63/11.11 % (3415140)Terminated due to inappropriate strategy. % 76.63/11.11 % (3415140)------------------------------ % 76.63/11.11 % (3415140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.63/11.11 % (3415140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.63/11.11 % (3415140)CaDiCaL version: 2.1.3 % 76.63/11.11 % (3415140)Termination reason: Inappropriate % 76.63/11.11 % (3415140)Time elapsed: 0.007 s % 76.63/11.11 % (3415140)Peak memory usage: 11 MB % 76.63/11.11 % (3415140)Instructions burned: 32 (million) % 76.63/11.11 % (3415140)------------------------------ % 76.63/11.11 % (3415140)------------------------------ % 76.63/11.11 % (3415142)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2851625503:i=22565:add=on:rawr=on_2979 on theBenchmark for (2979ds/22565Mi) % 76.63/11.11 % (3414956)Instruction limit reached! % 76.63/11.11 % (3414956)------------------------------ % 76.63/11.11 % (3414956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.63/11.11 % (3414956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.63/11.11 % (3414956)CaDiCaL version: 2.1.3 % 76.63/11.11 % (3414956)Termination reason: Instruction limit % 76.63/11.11 % (3414956)Termination phase: Saturation % 76.63/11.11 % (3414956)Time elapsed: 1.762 s % 76.63/11.11 % (3414956)Peak memory usage: 31 MB % 76.63/11.11 % (3414956)Instructions burned: 5116 (million) % 76.63/11.11 % (3415144)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=755866978:i=8173:av=off_2977 on theBenchmark for (2977ds/8173Mi) % 77.92/11.23 % (3415130)Instruction limit reached! % 77.92/11.23 % (3415130)------------------------------ % 77.92/11.23 % (3415130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.92/11.23 % (3415130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.92/11.23 % (3415130)CaDiCaL version: 2.1.3 % 77.92/11.23 % (3415130)Termination reason: Instruction limit % 77.92/11.23 % (3415130)Termination phase: Saturation % 77.92/11.23 % (3415130)Time elapsed: 1.463 s % 77.92/11.23 % (3415130)Peak memory usage: 45 MB % 77.92/11.23 % (3415130)Instructions burned: 4592 (million) % 77.92/11.23 % (3415146)dis+10_16:1_sil=16000:random_seed=1724372832:i=9155:fsr=off_2968 on theBenchmark for (2968ds/9155Mi) % 77.92/11.23 % (3415134)Instruction limit reached! % 77.92/11.23 % (3415134)------------------------------ % 77.92/11.23 % (3415134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.92/11.23 % (3415134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.92/11.23 % (3415134)CaDiCaL version: 2.1.3 % 77.92/11.23 % (3415134)Termination reason: Instruction limit % 77.92/11.23 % (3415134)Termination phase: Saturation % 77.92/11.23 % (3415134)Time elapsed: 1.434 s % 77.92/11.23 % (3415134)Peak memory usage: 51 MB % 77.92/11.23 % (3415134)Instructions burned: 5212 (million) % 77.92/11.23 % (3415148)ott-3_8_sil=64000:random_seed=614845737:i=20139:bs=on_2965 on theBenchmark for (2965ds/20139Mi) % 77.92/11.23 % (3415144)Instruction limit reached! % 77.92/11.23 % (3415144)------------------------------ % 77.92/11.23 % (3415144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.92/11.23 % (3415144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.92/11.23 % (3415144)CaDiCaL version: 2.1.3 % 77.92/11.23 % (3415144)Termination reason: Instruction limit % 77.92/11.23 % (3415144)Termination phase: Saturation % 77.92/11.23 % (3415144)Time elapsed: 2.793 s % 77.92/11.23 % (3415144)Peak memory usage: 47 MB % 77.92/11.23 % (3415144)Instructions burned: 8175 (million) % 77.92/11.23 % (3415150)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2409738117:fmbsr=2:i=32576_2948 on theBenchmark for (2948ds/32576Mi) % 77.92/11.23 % (3415150)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 77.92/11.23 % (3415150)Terminated due to inappropriate strategy. % 77.92/11.23 % (3415150)------------------------------ % 77.92/11.23 % (3415150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.92/11.23 % (3415150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.92/11.23 % (3415150)CaDiCaL version: 2.1.3 % 77.92/11.23 % (3415150)Termination reason: Inappropriate % 77.92/11.23 % (3415150)Time elapsed: 0.027 s % 77.92/11.23 % (3415150)Peak memory usage: 12 MB % 77.92/11.23 % (3415150)Instructions burned: 108 (million) % 77.92/11.23 % (3415150)------------------------------ % 77.92/11.23 % (3415150)------------------------------ % 77.92/11.23 % (3415152)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=176402190:i=11404_2948 on theBenchmark for (2948ds/11404Mi) % 77.92/11.23 % (3415146)Instruction limit reached! % 77.92/11.23 % (3415146)------------------------------ % 77.92/11.23 % (3415146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.92/11.23 % (3415146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.92/11.23 % (3415146)CaDiCaL version: 2.1.3 % 77.92/11.23 % (3415146)Termination reason: Instruction limit % 77.92/11.23 % (3415146)Termination phase: Saturation % 77.92/11.23 % (3415146)Time elapsed: 2.573 s % 77.92/11.23 % (3415146)Peak memory usage: 51 MB % 77.92/11.23 % (3415146)Instructions burned: 9155 (million) % 77.92/11.23 % (3415154)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2051113909:i=14134_2942 on theBenchmark for (2942ds/14134Mi) % 77.92/11.23 % (3415142)Instruction limit reached! % 77.92/11.23 % (3415142)------------------------------ % 77.92/11.23 % (3415142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.92/11.23 % (3415142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.92/11.23 % (3415142)CaDiCaL version: 2.1.3 % 77.92/11.23 % (3415142)Termination reason: Instruction limit % 77.92/11.23 % (3415142)Termination phase: Saturation % 77.92/11.23 % (3415142)Time elapsed: 4.852 s % 77.92/11.23 % (3415142)Peak memory usage: 25 MB % 77.92/11.23 % (3415142)Instructions burned: 22567 (million) % 77.92/11.23 % (3415156)dis+33_16_sil=32000:sac=on:random_seed=2615890102:i=15851:nm=0_2930 on theBenchmark for (2930ds/15851Mi) % 77.92/11.23 % (3415152)Instruction limit reached! % 77.92/11.23 % (3415152)------------------------------ % 110.66/17.39 % (3415152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.66/17.39 % (3415152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.66/17.39 % (3415152)CaDiCaL version: 2.1.3 % 110.66/17.39 % (3415152)Termination reason: Instruction limit % 110.66/17.39 % (3415152)Termination phase: Saturation % 110.66/17.39 % (3415152)Time elapsed: 4.148 s % 110.66/17.39 % (3415152)Peak memory usage: 47 MB % 110.66/17.39 % (3415152)Instructions burned: 11406 (million) % 110.66/17.39 % (3415158)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3844747822:avsq=on:i=17627:add=on:amm=off_2906 on theBenchmark for (2906ds/17627Mi) % 110.66/17.39 % (3415132)Instruction limit reached! % 110.66/17.39 % (3415132)------------------------------ % 110.66/17.39 % (3415132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.66/17.39 % (3415132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.66/17.39 % (3415132)CaDiCaL version: 2.1.3 % 110.66/17.39 % (3415132)Termination reason: Instruction limit % 110.66/17.39 % (3415132)Termination phase: Saturation % 110.66/17.39 % (3415132)Time elapsed: 7.873 s % 110.66/17.39 % (3415132)Peak memory usage: 157 MB % 110.66/17.39 % (3415132)Instructions burned: 29344 (million) % 110.66/17.39 % (3415148)Instruction limit reached! % 110.66/17.39 % (3415148)------------------------------ % 110.66/17.39 % (3415148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.66/17.39 % (3415148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.66/17.39 % (3415148)CaDiCaL version: 2.1.3 % 110.66/17.39 % (3415148)Termination reason: Instruction limit % 110.66/17.39 % (3415148)Termination phase: Saturation % 110.66/17.39 % (3415148)Time elapsed: 6.228 s % 110.66/17.39 % (3415148)Peak memory usage: 59 MB % 110.66/17.39 % (3415148)Instructions burned: 20139 (million) % 110.66/17.39 % (3415160)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3415346956:s2a=on:i=53295_2903 on theBenchmark for (2903ds/53295Mi) % 110.66/17.39 % (3415161)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3171133205:i=26857:ins=20_2903 on theBenchmark for (2903ds/26857Mi) % 110.66/17.39 % (3415161)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.66/17.39 % (3415161)Terminated due to inappropriate strategy. % 110.66/17.39 % (3415161)------------------------------ % 110.66/17.39 % (3415161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.66/17.39 % (3415161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.66/17.39 % (3415161)CaDiCaL version: 2.1.3 % 110.66/17.39 % (3415161)Termination reason: Inappropriate % 110.66/17.39 % (3415161)Time elapsed: 0.007 s % 110.66/17.39 % (3415161)Peak memory usage: 11 MB % 110.66/17.39 % (3415161)Instructions burned: 32 (million) % 110.66/17.39 % (3415161)------------------------------ % 110.66/17.39 % (3415161)------------------------------ % 110.66/17.39 % (3415164)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3179046532:i=28120:bs=on:fsr=off_2902 on theBenchmark for (2902ds/28120Mi) % 110.66/17.39 % (3415154)Instruction limit reached! % 110.66/17.39 % (3415154)------------------------------ % 110.66/17.39 % (3415154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.66/17.39 % (3415154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.66/17.39 % (3415154)CaDiCaL version: 2.1.3 % 110.66/17.39 % (3415154)Termination reason: Instruction limit % 110.66/17.39 % (3415154)Termination phase: Saturation % 110.66/17.39 % (3415154)Time elapsed: 5.157 s % 110.66/17.39 % (3415154)Peak memory usage: 56 MB % 110.66/17.39 % (3415154)Instructions burned: 14135 (million) % 110.66/17.39 % (3415166)fmb+10_1_sil=256000:fmbss=7:random_seed=3314331861:fmbsr=1.6:i=182295_2890 on theBenchmark for (2890ds/182295Mi) % 110.66/17.39 % (3415166)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.66/17.39 % (3415166)Terminated due to inappropriate strategy. % 110.66/17.39 % (3415166)------------------------------ % 110.66/17.39 % (3415166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.66/17.39 % (3415166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.66/17.39 % (3415166)CaDiCaL version: 2.1.3 % 110.66/17.39 % (3415166)Termination reason: Inappropriate % 110.66/17.39 % (3415166)Time elapsed: 0.007 s % 110.66/17.39 % (3415166)Peak memory usage: 11 MB % 110.66/17.39 % (3415166)Instructions burned: 32 (million) % 110.66/17.39 % (3415166)------------------------------ % 110.66/17.39 % (3415166)------------------------------ % 110.66/17.39 % (3415168)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3428369208:i=44625:gsp=on_2890 on theBenchmark for (2890ds/44625Mi) % 124.61/17.97 % (3415168)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.61/17.97 % (3415168)Terminated due to inappropriate strategy. % 124.61/17.97 % (3415168)------------------------------ % 124.61/17.97 % (3415168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.61/17.97 % (3415168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.61/17.97 % (3415168)CaDiCaL version: 2.1.3 % 124.61/17.97 % (3415168)Termination reason: Inappropriate % 124.61/17.97 % (3415168)Time elapsed: 0.011 s % 124.61/17.97 % (3415168)Peak memory usage: 11 MB % 124.61/17.97 % (3415168)Instructions burned: 48 (million) % 124.61/17.97 % (3415168)------------------------------ % 124.61/17.97 % (3415168)------------------------------ % 124.61/17.97 % (3415170)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1023979446:i=160505_2890 on theBenchmark for (2890ds/160505Mi) % 124.61/17.97 % (3415170)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.61/17.97 % (3415170)Terminated due to inappropriate strategy. % 124.61/17.97 % (3415170)------------------------------ % 124.61/17.97 % (3415170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.61/17.97 % (3415170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.61/17.97 % (3415170)CaDiCaL version: 2.1.3 % 124.61/17.97 % (3415170)Termination reason: Inappropriate % 124.61/17.97 % (3415170)Time elapsed: 0.007 s % 124.61/17.97 % (3415170)Peak memory usage: 11 MB % 124.61/17.97 % (3415170)Instructions burned: 32 (million) % 124.61/17.97 % (3415170)------------------------------ % 124.61/17.97 % (3415170)------------------------------ % 124.61/17.97 % (3415172)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4192542472:fmbsr=1.3:i=225729_2889 on theBenchmark for (2889ds/225729Mi) % 124.61/17.97 % (3415172)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.61/17.97 % (3415172)Terminated due to inappropriate strategy. % 124.61/17.97 % (3415172)------------------------------ % 124.61/17.97 % (3415172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.61/17.97 % (3415172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.61/17.97 % (3415172)CaDiCaL version: 2.1.3 % 124.61/17.97 % (3415172)Termination reason: Inappropriate % 124.61/17.97 % (3415172)Time elapsed: 0.007 s % 124.61/17.97 % (3415172)Peak memory usage: 11 MB % 124.61/17.97 % (3415172)Instructions burned: 32 (million) % 124.61/17.97 % (3415172)------------------------------ % 124.61/17.97 % (3415172)------------------------------ % 124.61/17.97 % (3415174)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3819946727:fmbsr=2:i=185024:ins=7_2889 on theBenchmark for (2889ds/185024Mi) % 124.61/17.97 % (3415174)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.61/17.97 % (3415174)Terminated due to inappropriate strategy. % 124.61/17.97 % (3415174)------------------------------ % 124.61/17.97 % (3415174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.61/17.97 % (3415174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.61/17.97 % (3415174)CaDiCaL version: 2.1.3 % 124.61/17.97 % (3415174)Termination reason: Inappropriate % 124.61/17.97 % (3415174)Time elapsed: 0.007 s % 124.61/17.97 % (3415174)Peak memory usage: 11 MB % 124.61/17.97 % (3415174)Instructions burned: 32 (million) % 124.61/17.97 % (3415174)------------------------------ % 124.61/17.97 % (3415174)------------------------------ % 124.61/17.97 % (3415176)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4138109686:rtra=on_2889 on theBenchmark for (2889ds/0Mi) % 124.61/17.97 % (3415176)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.61/17.97 % (3415176)Terminated due to inappropriate strategy. % 124.61/17.97 % (3415176)------------------------------ % 124.61/17.97 % (3415176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.61/17.97 % (3415176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.61/17.97 % (3415176)CaDiCaL version: 2.1.3 % 124.61/17.97 % (3415176)Termination reason: Inappropriate % 124.61/17.97 % (3415176)Time elapsed: 0.026 s % 124.61/17.97 % (3415176)Peak memory usage: 12 MB % 124.61/17.97 % (3415176)Instructions burned: 99 (million) % 124.61/17.97 % (3415176)------------------------------ % 124.61/17.97 % (3415176)------------------------------ % 124.61/17.97 % (3415178)% WARNING: option uhcvi not known. % 124.61/17.97 % (3415178)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2183528258:i=271062:add=off:rtra=on:rawr=on_2889 on theBenchmark for (2889ds/271062Mi) % 131.30/18.88 % (3415158)Instruction limit reached! % 131.30/18.88 % (3415158)------------------------------ % 131.30/18.88 % (3415158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.30/18.88 % (3415158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.30/18.88 % (3415158)CaDiCaL version: 2.1.3 % 131.30/18.88 % (3415158)Termination reason: Instruction limit % 131.30/18.88 % (3415158)Termination phase: Saturation % 131.30/18.88 % (3415158)Time elapsed: 5.520 s % 131.30/18.88 % (3415158)Peak memory usage: 253 MB % 131.30/18.88 % (3415158)Instructions burned: 17630 (million) % 131.30/18.88 % (3415312)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3849905507:i=176048:add=on:rtra=on:rawr=on_2851 on theBenchmark for (2851ds/176048Mi) % 131.30/18.88 % (3415156)Instruction limit reached! % 131.30/18.88 % (3415156)------------------------------ % 131.30/18.88 % (3415156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.30/18.88 % (3415156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.30/18.88 % (3415156)CaDiCaL version: 2.1.3 % 131.30/18.88 % (3415156)Termination reason: Instruction limit % 131.30/18.88 % (3415156)Termination phase: Clausification % 131.30/18.88 % (3415156)Time elapsed: 9.765 s % 131.30/18.88 % (3415156)Peak memory usage: 8631 MB % 131.30/18.88 % (3415156)Instructions burned: 15851 (million) % 131.30/18.88 % (3415164)Instruction limit reached! % 131.30/18.88 % (3415164)------------------------------ % 131.30/18.88 % (3415164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.30/18.88 % (3415164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.30/18.88 % (3415164)CaDiCaL version: 2.1.3 % 131.30/18.88 % (3415164)Termination reason: Instruction limit % 131.30/18.88 % (3415164)Termination phase: Saturation % 131.30/18.88 % (3415164)Time elapsed: 7.189 s % 131.30/18.88 % (3415164)Peak memory usage: 36 MB % 131.30/18.88 % (3415164)Instructions burned: 28122 (million) % 131.30/18.88 % (3415445)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4108296176:i=206:fgj=on:rtra=on_2830 on theBenchmark for (2830ds/206Mi) % 131.30/18.88 % (3415445)Instruction limit reached! % 131.30/18.88 % (3415445)------------------------------ % 131.30/18.88 % (3415445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.30/18.88 % (3415445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.30/18.88 % (3415445)CaDiCaL version: 2.1.3 % 131.30/18.88 % (3415445)Termination reason: Instruction limit % 131.30/18.88 % (3415445)Termination phase: Saturation % 131.30/18.88 % (3415445)Time elapsed: 0.064 s % 131.30/18.88 % (3415445)Peak memory usage: 15 MB % 131.30/18.88 % (3415445)Instructions burned: 208 (million) % 131.30/18.88 % (3415447)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2545172142:i=232:rtra=on_2830 on theBenchmark for (2830ds/232Mi) % 131.30/18.88 % (3415447)Instruction limit reached! % 131.30/18.88 % (3415447)------------------------------ % 131.30/18.88 % (3415447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.30/18.88 % (3415447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.30/18.88 % (3415447)CaDiCaL version: 2.1.3 % 131.30/18.88 % (3415447)Termination reason: Instruction limit % 131.30/18.88 % (3415447)Termination phase: Saturation % 131.30/18.88 % (3415447)Time elapsed: 0.059 s % 131.30/18.88 % (3415447)Peak memory usage: 14 MB % 131.30/18.88 % (3415447)Instructions burned: 232 (million) % 131.30/18.88 % (3415449)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=131850304:i=262:rtra=on_2829 on theBenchmark for (2829ds/262Mi) % 131.30/18.88 % (3415449)Instruction limit reached! % 131.30/18.88 % (3415449)------------------------------ % 131.30/18.88 % (3415449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.30/18.88 % (3415449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.30/18.88 % (3415449)CaDiCaL version: 2.1.3 % 131.30/18.88 % (3415449)Termination reason: Instruction limit % 131.30/18.88 % (3415449)Termination phase: Saturation % 131.30/18.88 % (3415449)Time elapsed: 0.075 s % 131.30/18.88 % (3415449)Peak memory usage: 16 MB % 131.30/18.88 % (3415449)Instructions burned: 264 (million) % 131.30/18.88 % (3415451)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1177208886:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2828 on theBenchmark for (2828ds/318Mi) % 131.30/18.88 % (3415451)Instruction limit reached! % 131.30/18.88 % (3415451)------------------------------ % 140.20/20.10 % (3415451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.20/20.10 % (3415451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.20/20.10 % (3415451)CaDiCaL version: 2.1.3 % 140.20/20.10 % (3415451)Termination reason: Instruction limit % 140.20/20.10 % (3415451)Termination phase: Saturation % 140.20/20.10 % (3415451)Time elapsed: 0.107 s % 140.20/20.10 % (3415451)Peak memory usage: 17 MB % 140.20/20.10 % (3415451)Instructions burned: 319 (million) % 140.20/20.10 % (3415453)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3771514265:i=1428:nm=2:rtra=on_2827 on theBenchmark for (2827ds/1428Mi) % 140.20/20.10 % (3415453)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 140.20/20.10 % (3415453)Terminated due to inappropriate strategy. % 140.20/20.10 % (3415453)------------------------------ % 140.20/20.10 % (3415453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.20/20.10 % (3415453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.20/20.10 % (3415453)CaDiCaL version: 2.1.3 % 140.20/20.10 % (3415453)Termination reason: Inappropriate % 140.20/20.10 % (3415453)Time elapsed: 0.007 s % 140.20/20.10 % (3415453)Peak memory usage: 11 MB % 140.20/20.10 % (3415453)Instructions burned: 31 (million) % 140.20/20.10 % (3415453)------------------------------ % 140.20/20.10 % (3415453)------------------------------ % 140.20/20.10 % (3415455)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3809223306:i=262:bd=preordered:rtra=on:fsd=on_2827 on theBenchmark for (2827ds/262Mi) % 140.20/20.10 % (3415455)Instruction limit reached! % 140.20/20.10 % (3415455)------------------------------ % 140.20/20.10 % (3415455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.20/20.10 % (3415455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.20/20.10 % (3415455)CaDiCaL version: 2.1.3 % 140.20/20.10 % (3415455)Termination reason: Instruction limit % 140.20/20.10 % (3415455)Termination phase: Saturation % 140.20/20.10 % (3415455)Time elapsed: 0.079 s % 140.20/20.10 % (3415455)Peak memory usage: 15 MB % 140.20/20.10 % (3415455)Instructions burned: 262 (million) % 140.20/20.10 % (3415457)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=4245996772:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2826 on theBenchmark for (2826ds/1368Mi) % 140.20/20.10 % (3415459)ott-21_1_sil=16000:si=on:fs=off:random_seed=1302642767:i=360:av=off:fsr=off:rtra=on_2825 on theBenchmark for (2825ds/360Mi) % 140.20/20.10 % (3415459)Instruction limit reached! % 140.20/20.10 % (3415459)------------------------------ % 140.20/20.10 % (3415459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.20/20.10 % (3415459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.20/20.10 % (3415459)CaDiCaL version: 2.1.3 % 140.20/20.10 % (3415459)Termination reason: Instruction limit % 140.20/20.10 % (3415459)Termination phase: Saturation % 140.20/20.10 % (3415459)Time elapsed: 0.086 s % 140.20/20.10 % (3415459)Peak memory usage: 14 MB % 140.20/20.10 % (3415459)Instructions burned: 360 (million) % 140.20/20.10 % (3415461)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=301754076:i=954:bd=all:rtra=on_2824 on theBenchmark for (2824ds/954Mi) % 140.20/20.10 % (3415457)Instruction limit reached! % 140.20/20.10 % (3415457)------------------------------ % 140.20/20.10 % (3415457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.20/20.10 % (3415457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.20/20.10 % (3415457)CaDiCaL version: 2.1.3 % 140.20/20.10 % (3415457)Termination reason: Instruction limit % 140.20/20.10 % (3415457)Termination phase: Saturation % 140.20/20.10 % (3415457)Time elapsed: 0.436 s % 140.20/20.10 % (3415457)Peak memory usage: 28 MB % 140.20/20.10 % (3415457)Instructions burned: 1370 (million) % 140.20/20.10 % (3415463)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3586455081:fmbsr=1.3:i=1730:ins=25:rtra=on_2821 on theBenchmark for (2821ds/1730Mi) % 140.20/20.10 % (3415463)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 140.20/20.10 % (3415463)Terminated due to inappropriate strategy. % 140.20/20.10 % (3415463)------------------------------ % 140.20/20.10 % (3415463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.20/20.10 % (3415463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.20/20.10 % (3415463)CaDiCaL version: 2.1.3 % 185.84/26.53 % (3415463)Termination reason: Inappropriate % 185.84/26.53 % (3415463)Time elapsed: 0.010 s % 185.84/26.53 % (3415463)Peak memory usage: 12 MB % 185.84/26.53 % (3415463)Instructions burned: 40 (million) % 185.84/26.53 % (3415463)------------------------------ % 185.84/26.53 % (3415463)------------------------------ % 185.84/26.53 % (3415465)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2983118654:i=2358:rtra=on_2821 on theBenchmark for (2821ds/2358Mi) % 185.84/26.53 % (3415461)Instruction limit reached! % 185.84/26.53 % (3415461)------------------------------ % 185.84/26.53 % (3415461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.84/26.53 % (3415461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.84/26.53 % (3415461)CaDiCaL version: 2.1.3 % 185.84/26.53 % (3415461)Termination reason: Instruction limit % 185.84/26.53 % (3415461)Termination phase: Saturation % 185.84/26.53 % (3415461)Time elapsed: 0.343 s % 185.84/26.53 % (3415461)Peak memory usage: 18 MB % 185.84/26.53 % (3415461)Instructions burned: 954 (million) % 185.84/26.53 % (3415467)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1816872303:i=1778:ins=1:rtra=on_2820 on theBenchmark for (2820ds/1778Mi) % 185.84/26.53 % (3415467)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.84/26.53 % (3415467)Terminated due to inappropriate strategy. % 185.84/26.53 % (3415467)------------------------------ % 185.84/26.53 % (3415467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.84/26.53 % (3415467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.84/26.53 % (3415467)CaDiCaL version: 2.1.3 % 185.84/26.53 % (3415467)Termination reason: Inappropriate % 185.84/26.53 % (3415467)Time elapsed: 0.008 s % 185.84/26.53 % (3415467)Peak memory usage: 11 MB % 185.84/26.53 % (3415467)Instructions burned: 34 (million) % 185.84/26.53 % (3415467)------------------------------ % 185.84/26.53 % (3415467)------------------------------ % 185.84/26.53 % (3415469)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=2852229604:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2820 on theBenchmark for (2820ds/1384Mi) % 185.84/26.53 % (3415469)Instruction limit reached! % 185.84/26.53 % (3415469)------------------------------ % 185.84/26.53 % (3415469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.84/26.53 % (3415469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.84/26.53 % (3415469)CaDiCaL version: 2.1.3 % 185.84/26.53 % (3415469)Termination reason: Instruction limit % 185.84/26.53 % (3415469)Termination phase: Saturation % 185.84/26.53 % (3415469)Time elapsed: 0.488 s % 185.84/26.53 % (3415469)Peak memory usage: 29 MB % 185.84/26.53 % (3415469)Instructions burned: 1385 (million) % 185.84/26.53 % (3415471)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1455183227:i=1758:kws=inv_precedence:fsr=off:rtra=on_2815 on theBenchmark for (2815ds/1758Mi) % 185.84/26.53 % (3415465)Instruction limit reached! % 185.84/26.53 % (3415465)------------------------------ % 185.84/26.53 % (3415465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.84/26.53 % (3415465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.84/26.53 % (3415465)CaDiCaL version: 2.1.3 % 185.84/26.53 % (3415465)Termination reason: Instruction limit % 185.84/26.53 % (3415465)Termination phase: Saturation % 185.84/26.53 % (3415465)Time elapsed: 0.851 s % 185.84/26.53 % (3415465)Peak memory usage: 24 MB % 185.84/26.53 % (3415465)Instructions burned: 2359 (million) % 185.84/26.53 % (3415473)fmb+10_1_sil=64000:si=on:random_seed=3405080291:i=44122:nm=2:rtra=on:gsp=on_2812 on theBenchmark for (2812ds/44122Mi) % 185.84/26.53 % (3415473)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.84/26.53 % (3415473)Terminated due to inappropriate strategy. % 185.84/26.53 % (3415473)------------------------------ % 185.84/26.53 % (3415473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.84/26.53 % (3415473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.84/26.53 % (3415473)CaDiCaL version: 2.1.3 % 185.84/26.53 % (3415473)Termination reason: Inappropriate % 185.84/26.53 % (3415473)Time elapsed: 0.008 s % 185.84/26.53 % (3415473)Peak memory usage: 11 MB % 185.84/26.53 % (3415473)Instructions burned: 33 (million) % 185.84/26.53 % (3415473)------------------------------ % 185.84/26.53 % (3415473)------------------------------ % 185.84/26.53 % (3415475)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2805760749:i=19030:nm=5:rtra=on_2812 on theBenchmark for (2812ds/19030Mi) % 199.73/28.56 % (3415475)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 199.73/28.56 % (3415475)Terminated due to inappropriate strategy. % 199.73/28.56 % (3415475)------------------------------ % 199.73/28.56 % (3415475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.73/28.56 % (3415475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.73/28.56 % (3415475)CaDiCaL version: 2.1.3 % 199.73/28.56 % (3415475)Termination reason: Inappropriate % 199.73/28.56 % (3415475)Time elapsed: 0.007 s % 199.73/28.56 % (3415475)Peak memory usage: 11 MB % 199.73/28.56 % (3415475)Instructions burned: 32 (million) % 199.73/28.56 % (3415475)------------------------------ % 199.73/28.56 % (3415475)------------------------------ % 199.73/28.56 % (3415477)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=4114282762:fmbsr=1.7:i=1840:rtra=on_2812 on theBenchmark for (2812ds/1840Mi) % 199.73/28.56 % (3415477)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 199.73/28.56 % (3415477)Terminated due to inappropriate strategy. % 199.73/28.56 % (3415477)------------------------------ % 199.73/28.56 % (3415477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.73/28.56 % (3415477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.73/28.56 % (3415477)CaDiCaL version: 2.1.3 % 199.73/28.56 % (3415477)Termination reason: Inappropriate % 199.73/28.56 % (3415477)Time elapsed: 0.008 s % 199.73/28.56 % (3415477)Peak memory usage: 11 MB % 199.73/28.56 % (3415477)Instructions burned: 34 (million) % 199.73/28.56 % (3415477)------------------------------ % 199.73/28.56 % (3415477)------------------------------ % 199.73/28.56 % (3415479)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=1744667202:i=10262:rtra=on_2812 on theBenchmark for (2812ds/10262Mi) % 199.73/28.56 % (3415471)Instruction limit reached! % 199.73/28.56 % (3415471)------------------------------ % 199.73/28.56 % (3415471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.73/28.56 % (3415471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.73/28.56 % (3415471)CaDiCaL version: 2.1.3 % 199.73/28.56 % (3415471)Termination reason: Instruction limit % 199.73/28.56 % (3415471)Termination phase: Saturation % 199.73/28.56 % (3415471)Time elapsed: 0.547 s % 199.73/28.56 % (3415471)Peak memory usage: 25 MB % 199.73/28.56 % (3415471)Instructions burned: 1760 (million) % 199.73/28.56 % (3415481)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2021540521:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2809 on theBenchmark for (2809ds/2944Mi) % 199.73/28.56 % (3415481)Instruction limit reached! % 199.73/28.56 % (3415481)------------------------------ % 199.73/28.56 % (3415481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.73/28.56 % (3415481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.73/28.56 % (3415481)CaDiCaL version: 2.1.3 % 199.73/28.56 % (3415481)Termination reason: Instruction limit % 199.73/28.56 % (3415481)Termination phase: Saturation % 199.73/28.56 % (3415481)Time elapsed: 0.882 s % 199.73/28.56 % (3415481)Peak memory usage: 38 MB % 199.73/28.56 % (3415481)Instructions burned: 2944 (million) % 199.73/28.56 % (3415483)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3109975846:i=12648:rtra=on_2800 on theBenchmark for (2800ds/12648Mi) % 199.73/28.56 % (3415483)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 199.73/28.56 % (3415483)Terminated due to inappropriate strategy. % 199.73/28.56 % (3415483)------------------------------ % 199.73/28.56 % (3415483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.73/28.56 % (3415483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.73/28.56 % (3415483)CaDiCaL version: 2.1.3 % 199.73/28.56 % (3415483)Termination reason: Inappropriate % 199.73/28.56 % (3415483)Time elapsed: 0.024 s % 199.73/28.56 % (3415483)Peak memory usage: 12 MB % 199.73/28.56 % (3415483)Instructions burned: 94 (million) % 199.73/28.56 % (3415483)------------------------------ % 199.73/28.56 % (3415483)------------------------------ % 199.73/28.56 % (3415485)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=4080569951:fmbsr=2.30978:i=4348:rtra=on_2800 on theBenchmark for (2800ds/4348Mi) % 199.73/28.56 % (3415485)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 199.73/28.56 % (3415485)Terminated due to inappropriate strategy. % 261.28/37.22 % (3415485)------------------------------ % 261.28/37.22 % (3415485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.28/37.22 % (3415485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.28/37.22 % (3415485)CaDiCaL version: 2.1.3 % 261.28/37.22 % (3415485)Termination reason: Inappropriate % 261.28/37.22 % (3415485)Time elapsed: 0.008 s % 261.28/37.22 % (3415485)Peak memory usage: 11 MB % 261.28/37.22 % (3415485)Instructions burned: 34 (million) % 261.28/37.22 % (3415485)------------------------------ % 261.28/37.22 % (3415485)------------------------------ % 261.28/37.22 % (3415487)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=232945754:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2800 on theBenchmark for (2800ds/1738Mi) % 261.28/37.22 % (3415487)Instruction limit reached! % 261.28/37.22 % (3415487)------------------------------ % 261.28/37.22 % (3415487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.28/37.22 % (3415487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.28/37.22 % (3415487)CaDiCaL version: 2.1.3 % 261.28/37.22 % (3415487)Termination reason: Instruction limit % 261.28/37.22 % (3415487)Termination phase: Saturation % 261.28/37.22 % (3415487)Time elapsed: 0.807 s % 261.28/37.22 % (3415487)Peak memory usage: 27 MB % 261.28/37.22 % (3415487)Instructions burned: 1739 (million) % 261.28/37.22 % (3415535)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=691917742:i=10228:av=off:rtra=on_2792 on theBenchmark for (2792ds/10228Mi) % 261.28/37.22 % (3415479)Instruction limit reached! % 261.28/37.22 % (3415479)------------------------------ % 261.28/37.22 % (3415479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.28/37.22 % (3415479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.28/37.22 % (3415479)CaDiCaL version: 2.1.3 % 261.28/37.22 % (3415479)Termination reason: Instruction limit % 261.28/37.22 % (3415479)Termination phase: Saturation % 261.28/37.22 % (3415479)Time elapsed: 4.110 s % 261.28/37.22 % (3415479)Peak memory usage: 69 MB % 261.28/37.22 % (3415479)Instructions burned: 10263 (million) % 261.28/37.22 % (3415628)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1515283121:i=108564:rtra=on_2770 on theBenchmark for (2770ds/108564Mi) % 261.28/37.22 % (3415628)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.28/37.22 % (3415628)Terminated due to inappropriate strategy. % 261.28/37.22 % (3415628)------------------------------ % 261.28/37.22 % (3415628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.28/37.22 % (3415628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.28/37.22 % (3415628)CaDiCaL version: 2.1.3 % 261.28/37.22 % (3415628)Termination reason: Inappropriate % 261.28/37.22 % (3415628)Time elapsed: 0.036 s % 261.28/37.22 % (3415628)Peak memory usage: 12 MB % 261.28/37.22 % (3415628)Instructions burned: 94 (million) % 261.28/37.22 % (3415628)------------------------------ % 261.28/37.22 % (3415628)------------------------------ % 261.28/37.22 % (3415630)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2901506303:i=7024:aac=none:rtra=on_2770 on theBenchmark for (2770ds/7024Mi) % 261.28/37.22 % (3415160)Instruction limit reached! % 261.28/37.22 % (3415160)------------------------------ % 261.28/37.22 % (3415160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.28/37.22 % (3415160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.28/37.22 % (3415160)CaDiCaL version: 2.1.3 % 261.28/37.22 % (3415160)Termination reason: Instruction limit % 261.28/37.22 % (3415160)Termination phase: Saturation % 261.28/37.22 % (3415160)Time elapsed: 15.251 s % 261.28/37.22 % (3415160)Peak memory usage: 349 MB % 261.28/37.22 % (3415160)Instructions burned: 53296 (million) % 261.28/37.22 % (3415683)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1211807221:i=7546:rtra=on:amm=off_2750 on theBenchmark for (2750ds/7546Mi) % 261.28/37.22 % (3415630)Instruction limit reached! % 261.28/37.22 % (3415630)------------------------------ % 261.28/37.22 % (3415630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.28/37.22 % (3415630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.28/37.22 % (3415630)CaDiCaL version: 2.1.3 % 261.28/37.22 % (3415630)Termination reason: Instruction limit % 261.28/37.22 % (3415630)Termination phase: Saturation % 261.28/37.22 % (3415630)Time elapsed: 3.396 s % 261.28/37.22 % (3415630)Peak memory usage: 45 MB % 261.28/37.22 % (3415630)Instructions burned: 7024 (million) % 261.28/37.22 % (3415701)ott+11_1_sil=16000:si=on:gs=on:random_seed=3794881492:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2736 on theBenchmark for (2736ds/4502Mi) % 300.07/42.73 % (3415535)Instruction limit reached! % 300.07/42.73 % (3415535)------------------------------ % 300.07/42.73 % (3415535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.07/42.73 % (3415535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/42.73 % (3415535)CaDiCaL version: 2.1.3 % 300.07/42.73 % (3415535)Termination reason: Instruction limit % 300.07/42.73 % (3415535)Termination phase: Saturation % 300.07/42.73 % (3415535)Time elapsed: 5.738 s % 300.07/42.73 % (3415535)Peak memory usage: 50 MB % 300.07/42.73 % (3415535)Instructions burned: 10229 (million) % 300.07/42.73 % (3415703)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=4084034077:fmbsr=1.6:i=135068:rtra=on_2734 on theBenchmark for (2734ds/135068Mi) % 300.07/42.73 % (3415703)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.07/42.73 % (3415703)Terminated due to inappropriate strategy. % 300.07/42.73 % (3415703)------------------------------ % 300.07/42.73 % (3415703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.07/42.73 % (3415703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/42.73 % (3415703)CaDiCaL version: 2.1.3 % 300.07/42.73 % (3415703)Termination reason: Inappropriate % 300.07/42.73 % (3415703)Time elapsed: 0.015 s % 300.07/42.73 % (3415703)Peak memory usage: 11 MB % 300.07/42.73 % (3415703)Instructions burned: 34 (million) % 300.07/42.73 % (3415703)------------------------------ % 300.07/42.73 % (3415703)------------------------------ % 300.07/42.73 % (3415706)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2804963008:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2733 on theBenchmark for (2733ds/9182Mi) % 300.07/42.73 % (3414828)Instruction limit reached! % 300.07/42.73 % (3414828)------------------------------ % 300.07/42.73 % (3414828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.07/42.73 % (3414828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/42.73 % (3414828)CaDiCaL version: 2.1.3 % 300.07/42.73 % (3414828)Termination reason: Instruction limit % 300.07/42.73 % (3414828)Termination phase: Saturation % 300.07/42.73 % (3414828)Time elapsed: 27.334 s % 300.07/42.73 % (3414828)Peak memory usage: 1559 MB % 300.07/42.73 % (3414828)Instructions burned: 88024 (million) % 300.07/42.73 % (3415713)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=1841500340:i=58680:rtra=on_2725 on theBenchmark for (2725ds/58680Mi) % 300.07/42.73 % (3415683)Instruction limit reached! % 300.07/42.73 % (3415683)------------------------------ % 300.07/42.73 % (3415683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.07/42.73 % (3415683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/42.73 % (3415683)CaDiCaL version: 2.1.3 % 300.07/42.73 % (3415683)Termination reason: Instruction limit % 300.07/42.73 % (3415683)Termination phase: Saturation % 300.07/42.73 % (3415683)Time elapsed: 3.149 s % 300.07/42.73 % (3415683)Peak memory usage: 53 MB % 300.07/42.73 % (3415683)Instructions burned: 7546 (million) % 300.07/42.73 % (3415715)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=3538017684:i=10422:rtra=on_2718 on theBenchmark for (2718ds/10422Mi) % 300.07/42.73 % (3415701)Instruction limit reached! % 300.07/42.73 % (3415701)------------------------------ % 300.07/42.73 % (3415701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.07/42.73 % (3415701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/42.73 % (3415701)CaDiCaL version: 2.1.3 % 300.07/42.73 % (3415701)Termination reason: Instruction limit % 300.07/42.73 % (3415701)Termination phase: Saturation % 300.07/42.73 % (3415701)Time elapsed: 1.994 s % 300.07/42.73 % (3415701)Peak memory usage: 34 MB % 300.07/42.73 % (3415701)Instructions burned: 4505 (million) % 300.07/42.73 % (3415718)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=873745183:i=10994:nm=2:rtra=on_2716 on theBenchmark for (2716ds/10994Mi) % 300.07/42.73 % (3415718)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.07/42.73 % (3415718)Terminated due to inappropriate strategy. % 300.07/42.73 % (3415718)------------------------------ % 300.07/42.73 % (3415718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.07/42.73 % (3415718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/42.73 % (3415718)CaDiCaL version: 2.1.3 % 300.07/42.73 % (341 % 300.07/42.73 Terminated % 300.07/42.73 % Vampire exiting %------------------------------------------------------------------------------