(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) (distinct n0 n1 ) (assert (and (<= 0 (- (+ len_n1 0 ) (+ 1 0 ) ) ) (<= 0 (- (+ x0 0 ) (+ (select n1 0) 1) ) ) ) ) (assert (forall ((?y1 Int) (?y2 Int)) (=> (and (<= 1 ?y1) (<= ?y1 len_n1) (<= 1 ?y2) (<= ?y2 len_n1) (<= ?y1 ?y2) (<= 2 len_n1)) (and (<= 0 (- (+ (select n1 ?y1) 0 ) (+ (select n1 0) 0 ) ) ) (<= 0 (- (+ (select n1 ?y2) 0 ) (+ (select n1 ?y1) 0 ) ) ) (<= 0 (- (+ ?y2 0 ) (+ 1 0 ) ) ) (<= 0 (- (+ ?y1 0 ) (+ 1 0 ) ) ) (<= 0 (- (+ len_n1 0 ) (+ 2 0 ) ) ) (<= 0 (- (+ x0 0 ) (+ (select n1 ?y2) 1) ) ) ) ) ) ) (assert (forall ((?y1 Int)) (=> (and (<= 1 ?y1) (<= ?y1 len_n1) (<= 2 len_n1)) (and (<= 0 (- (+ (select n1 ?y1) 0 ) (+ (select n1 0) 0 ) ) ) (<= 0 (- (+ ?y1 0 ) (+ 1 0 ) ) ) (<= 0 (- (+ len_n1 0 ) (+ 2 0 ) ) ) (<= 0 (- (+ x0 0 ) (+ (select n1 ?y1) 1) ) ) ) ) ) ) (assert (not (and (<= 0 (- (+ len_n1 0 ) (+ 1 0 ) ) ) (forall ((?y1 Int) (?y2 Int)) (=> (and (<= 1 ?y1) (<= ?y1 len_n1) (<= 1 ?y2) (<= ?y2 len_n1) (<= ?y1 ?y2) (<= 2 len_n1)) (and (<= 0 (- (+ (select n1 ?y1) 0 ) (+ (select n1 0) 0 ) ) ) (<= 0 (- (+ (select n1 ?y2) 0 ) (+ (select n1 ?y1) 0 ) ) ) (<= 0 (- (+ ?y2 0 ) (+ 1 0 ) ) ) (<= 0 (- (+ ?y1 0 ) (+ 1 0 ) ) ) (<= 0 (- (+ len_n1 0 ) (+ 2 0 ) ) ) (<= 0 (- (+ x0 0 ) (+ (select n1 ?y2) 1) ) ) ) )) (forall ((?y1 Int)) (=> (and (<= 1 ?y1) (<= ?y1 len_n1) (<= 2 len_n1)) (and (<= 0 (- (+ (select n1 ?y1) 0 ) (+ (select n1 0) 0 ) ) ) (<= 0 (- (+ ?y1 0 ) (+ 1 0 ) ) ) (<= 0 (- (+ len_n1 0 ) (+ 2 0 ) ) ) (<= 0 (- (+ x0 0 ) (+ (select n1 ?y1) 1) ) ) ) )) ))) (check-sat)