Unsatisfiable subset due to time in Project MCS

I was told to post this as an issue after asking an assistent.

With the attached idp file (solution.idp), if I run the checkWin procedure, I get the following message:

The following is an unsatisfiable subset, given that functions can map to at most one element (and exactly one if not partial) and the interpretation of types and symbols in the structure: Next(2,+int,int : int) <- time(+int,int : int). instantiated from line 71 with t=2.