gistfile1.txt

(define l_y1 :: int)
(define l_y2 :: int)
(define l_y3 :: int)
(define l_x1 :: int)
(define l_x2 :: int)
(define l_x3 :: int)
(define l_x4 :: int)

(assert (<= l_x1 3))
(assert (>= l_x1 0))
(assert (<= l_x2 3))
(assert (>= l_x2 0))
(assert (<= l_x3 3))
(assert (>= l_x3 0))
(assert (<= l_x4 3))
(assert (>= l_x4 0))

(assert (<= l_y1 3))
(assert (>= l_y1 1))
(assert (<= l_y2 3))
(assert (>= l_y2 1))
(assert (<= l_y3 3))
(assert (>= l_y3 1))

; L(y_i) = L(y_j) => y_i = y_j (each line number has only one component)
(assert (/= l_y1 l_y2))
(assert (/= l_y1 l_y3))
(assert (/= l_y2 l_y3))

; l_x1 < l_y1, l_x2 < l_y2, l_x3 < l_y3, l_x4 < l_y4
(assert (< l_x1 l_y1))
(assert (< l_x2 l_y2))
(assert (< l_x3 l_y3))
(assert (< l_x4 l_y3))

(check)