drop maxHeartbeats overrides: dispatch cheap name-clash case first

fibred lookup theorems for solving reduced instances

virtual normal form