A mechanized multi-context solution to McCarthy's GLM problem