Beginner: Integer EqualitiesSample answers

There is no need to declare anything in the “sorts” or “vocabulary” sections, as the solver can work out from the constraints that “mine” and “yours” are names for numbers, just like “x” in the first example in the guide. A solution to this problem is just any model (i.e. interpretation of the two symbols “mine” and “yours”) satisfying both of the two constraints. Of course, there is only one solution in this case.