Avoid splitting when not necessary as it may incur in performance hit. Indeed,
splitting means more (tinier) goals to verify, hence more call to provers.