(set-logic QF_AUFNIA) (set-info :status unsat) (declare-fun i () Int) (declare-fun j () Int) (declare-fun k () Int) (declare-fun l () Int) (declare-fun m () Int) (declare-fun n () Int) (declare-fun a () (Array Int (Array Int Int))) (declare-fun b () (Array Int (Array Int Int))) (declare-fun c () (Array Int (Array Int Int))) (declare-fun d () (Array Int (Array Int Int))) (declare-fun e () (Array Int (Array Int Int))) (declare-fun f () (Array Int (Array Int Int))) (declare-fun g () (Array Int (Array Int Int))) (declare-fun h () (Array Int (Array Int Int))) (assert (not (= k 0))) (assert (<= j k)) (assert (>= j k)) (assert (= b (store a j (store (select a j) 0 0)))) (assert (= d (store b 0 (store (select b 0) 0 (select (select d 0) 0))))) (assert (<= i 0)) (assert (>= i (select (store (select d j) m 0) 0))) (assert (not (= i 0))) (check-sat) (exit)