(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 (- (+ x0 0 ) (+ 0 0 ) ) ) (<= 0 (- (+ len_n1 0 ) (+ 1 0 ) ) ) ) ) (assert (not (and (= 0 (- (+ x0 0 ) (+ 0 0 ) ) ) (<= 0 (- (+ len_n1 0 ) (+ 1 0 ) ) ) ))) (check-sat)