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