The example encoding assumed that derived predicates weren’t necessary in the final time step. This is, however, incorrect, as the goal may have a precondition that requires derived predicates. In this case, the derived variables must be evaluated for the final time step.