Updated with two methods to introduce hint-please. It seems that :in-theory is doing better.
Updated with two methods to introduce hint-please. It seems that :in-theory is doing better.

pennyan/Smtlink,pennyan/Smtlink