Предикат заказа невыполним

Кажется, я чего-то не понимаю в первой ветви предиката упорядочения в ff_next этой модели сплава.

open util/ordering[Exposure]
open util/ordering[Tile]
open util/ordering[Point]

sig Exposure {}

sig Tile {}

sig Point {
    ex: one Exposure,
    tl: one Tile
} fact {
    // Uncommenting the line below makes the model unsatisfiable
    // Point.ex = Exposure  
    Point.tl = Tile
}

pred ff_next[p, p': Point] {
    (p.tl = last) => (p'.ex = next[p.ex] and p'.tl = first)
    else (p'.ex = p.ex and p'.tl = next[p.tl])
}

fact ff_ordering {
    first.ex = first
    first.tl = first
    all p: Point - last | ff_next[p, next[p]]
}

run {}

Интуиция здесь такова, что у меня есть несколько экспозиций, каждую из которых я хочу выполнить на нескольких позициях плитки. Подумайте о том, чтобы делать панорамные изображения, а затем сшивать их вместе, но делать это несколько раз с разными настройками камеры.

С отмеченной строкой, закомментированной, первый экземпляр, который я получаю, таков:

Это эквивалентно одному проходу по панораме с одной экспозицией, а затем опусканию остальных экспозиций на пол.

Кажется, проблема в первой ветке после => в ff_next, но я не понимаю, что не так. Никогда не устраивала та ветвь, которая переходила бы к следующей экспозиции и началу панорамы. Если я раскомментирую строку Point.ex = Exposure, модель станет неудовлетворительной, потому что для нее требуется эта ветвь.

Любая помощь в том, почему эта ветвь не удовлетворяет?