(COMMENTS
  Liveness problem: cars over the bridge 
)
(MODEL
  top(left (car(x, y), z)) -> top(right(y, z))
  top(right(x, car(y, z))) -> top( left(x, z))
  top(left (bot, x)) -> top(right(bot, x))
  top(right(x, bot)) -> top(left (x, bot))
  top(left (car(x, y), z)) ->= top(left (y, z))
  top(right(x, car(y, z))) ->= top(right(x, z))
  bot ->= car(new, bot)
)
(VAR x y z)
(RULES
  top(ok(left (car(x, y), z))) -> top(check(right(y, z)))
  top(ok(right(x, car(y, z)))) -> top(check( left(x, z)))
  top(ok(left (bot, x))) -> top(check(right(bot, x)))
  top(ok(right(x, bot))) -> top(check(left (x, bot)))
  top(ok(left (car(x, y), z))) ->= top(check(left (y, z)))
  top(ok(right(x, car(y, z)))) ->= top(check(right(x, z)))
  bot ->= car(new, bot)
				
  check(old) ->= ok(old)
  check(car(x, y)) ->= car(check(x), y)
  check(car(x, y)) ->= car(x, check(y))
  check(left(x, y)) ->= left(check(x), y)
  check(left(x, y)) ->= left(x, check(y))
  check(right(x, y)) ->= right(check(x), y)
  check(right(x, y)) ->= right(x, check(y))
  car(ok(x), y) ->= ok(car(x, y))
  car(x, ok(y)) ->= ok(car(x, y)) 
  left(ok(x), y) ->= ok(left(x, y))
  left(x, ok(y)) ->= ok(left(x, y))
  right(ok(x), y) ->= ok(right(x, y))
  right(x, ok(y)) ->= ok(right(x, y))
)