(set-logic AUFLIA)
(define-sort Node () (Array Int Int) )
(declare-const x0 Int)
(declare-const x1 Int)
(declare-const n0 Node)
(declare-const len_n0 Int)
(declare-const n1 Node)
(declare-const len_n1 Int)
(distinct  n0  n1 )
(assert (and (= 0 (- (+  (select n1 0)  0 )  (+ 2 0 ) ) )
		 (<= 0 (- (+ (* 2 x1 ) 2)  (+ (* 3 x0 )  len_n1 ) ) )
		 (<= 0 (- (+  len_n1  0 )  (+ 3 0 ) ) )
		 (<= 0 (- (+ (* 2 x0 ) 2)  (+  x1  len_n1 ) ) )
		 
) )
(assert (forall ((?y1 Int) (?y2 Int))
		(=> (and (<= 1 ?y1) (<= ?y1 len_n1) (<= 1 ?y2) (<= ?y2 len_n1) (= (+ ?y1 1) ?y2) (<= 2 len_n1))
		    (and (= 0 (- (+  ?y2  0 )  (+  ?y1 1) ) )
		 (<= 0 (- (+   (select n1 ?y2)  2)  (+  ?y1   (select n1 ?y1)  ) ) )
		 (<= 0 (- (+  ?y1  0 )  (+ 1 0 ) ) )
		 (<= 0 (- (+  len_n1   (select n1 ?y2)  )  (+ (* 2 ?y1 )   (select n1 ?y1)  2) ) )
		 (<= 0 (- (+  len_n1  0 )  (+  ?y1 2) ) )
		 )
) ) )
(assert (forall ((?y1 Int))
		(=> (and (<= 1 ?y1) (<= ?y1 len_n1) (<= 2 len_n1) (= ?y1 (- len_n1 1)))
		    (and (= 0 (- (+  ?y1 1)  (+  len_n1  0 ) ) )
		 (= 0 (- (+  (select n1 0)  0 )  (+ 2 0 ) ) )
		 (= 0 (- (+  x0   (select n1 ?y1)  )  (+  x1  0 ) ) )
		 (<= 0 (- (+ (* 2 x1 ) 2)  (+ (* 3 x0 )  len_n1 ) ) )
		 (<= 0 (- (+  len_n1  0 )  (+ 3 0 ) ) )
		 (<= 0 (- (+ (* 2 x0 ) 2)  (+  x1  len_n1 ) ) )
		 )
) ) )
(assert (not (and (= 0 (- (+  (select n1 0)  0 )  (+ 2 0 ) ) )
		 (<= 0 (- (+ (* 2 x1 ) 2)  (+ (* 3 x0 )  len_n1 ) ) )
		 (<= 0 (- (+  len_n1  0 )  (+ 3 0 ) ) )
		 (<= 0 (- (+ (* 2 x0 ) 2)  (+  x1  len_n1 ) ) )
		 
	(forall ((?y1 Int) (?y2 Int))
		(=> (and (<= 1 ?y1) (<= ?y1 len_n1) (<= 1 ?y2) (<= ?y2 len_n1) (= (+ ?y1 1) ?y2) (<= 2 len_n1))
		     (and (= 0 (- (+  ?y2  0 )  (+  ?y1 1) ) )
		 (<= 0 (- (+   (select n1 ?y2)  2)  (+  ?y1   (select n1 ?y1)  ) ) )
		 (<= 0 (- (+  ?y1  0 )  (+ 1 0 ) ) )
		 (<= 0 (- (+  len_n1   (select n1 ?y2)  )  (+ (* 2 ?y1 )   (select n1 ?y1)  2) ) )
		 (<= 0 (- (+  len_n1  0 )  (+  ?y1 2) ) )
		 )
		))

	(forall ((?y1 Int))
		(=> (and (<= 1 ?y1) (<= ?y1 len_n1) (<= 2 len_n1) (= ?y1 (- len_n1 1)))
		     (and (= 0 (- (+  ?y1 1)  (+  len_n1  0 ) ) )
		 (= 0 (- (+  (select n1 0)  0 )  (+ 2 0 ) ) )
		 (= 0 (- (+  x0   (select n1 ?y1)  )  (+  x1  0 ) ) )
		 (<= 0 (- (+ (* 2 x1 ) 2)  (+ (* 3 x0 )  len_n1 ) ) )
		 (<= 0 (- (+  len_n1  0 )  (+ 3 0 ) ) )
		 (<= 0 (- (+ (* 2 x0 ) 2)  (+  x1  len_n1 ) ) )
		 )
		))
)))
(check-sat)