(set-option :incremental false)
(set-logic QF_BV)
(declare-fun a11 () (_ BitVec 5))
(declare-fun a12 () (_ BitVec 5))
(declare-fun a13 () (_ BitVec 5))
(declare-fun a21 () (_ BitVec 5))
(declare-fun a22 () (_ BitVec 5))
(declare-fun a23 () (_ BitVec 5))
(declare-fun a31 () (_ BitVec 5))
(declare-fun a32 () (_ BitVec 5))
(declare-fun a33 () (_ BitVec 5))
(declare-fun sum () (_ BitVec 5))
(declare-fun soo () (_ BitVec 5))
(declare-fun sii () (_ BitVec 5))
(declare-fun sol () (_ BitVec 5))
(declare-fun sor () (_ BitVec 5))
(declare-fun sul () (_ BitVec 5))
(declare-fun sur () (_ BitVec 5))
(assert (or (= a11 (_ bv1 5)) (= a11 (_ bv2 5)) (= a11 (_ bv3 5)) (= a11 (_ bv4 5)) (= a11 (_ bv5 5)) (= a11 (_ bv6 5)) (= a11 (_ bv7 5)) (= a11 (_ bv8 5)) (= a11 (_ bv9 5))))
(assert (or (= a12 (_ bv1 5)) (= a12 (_ bv2 5)) (= a12 (_ bv3 5)) (= a12 (_ bv4 5)) (= a12 (_ bv5 5)) (= a12 (_ bv6 5)) (= a12 (_ bv7 5)) (= a12 (_ bv8 5)) (= a12 (_ bv9 5))))
(assert (or (= a13 (_ bv1 5)) (= a13 (_ bv2 5)) (= a13 (_ bv3 5)) (= a13 (_ bv4 5)) (= a13 (_ bv5 5)) (= a13 (_ bv6 5)) (= a13 (_ bv7 5)) (= a13 (_ bv8 5)) (= a13 (_ bv9 5))))
(assert (or (= a21 (_ bv1 5)) (= a21 (_ bv2 5)) (= a21 (_ bv3 5)) (= a21 (_ bv4 5)) (= a21 (_ bv5 5)) (= a21 (_ bv6 5)) (= a21 (_ bv7 5)) (= a21 (_ bv8 5)) (= a21 (_ bv9 5))))
(assert (or (= a22 (_ bv1 5)) (= a22 (_ bv2 5)) (= a22 (_ bv3 5)) (= a22 (_ bv4 5)) (= a22 (_ bv5 5)) (= a22 (_ bv6 5)) (= a22 (_ bv7 5)) (= a22 (_ bv8 5)) (= a22 (_ bv9 5))))
(assert (or (= a23 (_ bv1 5)) (= a23 (_ bv2 5)) (= a23 (_ bv3 5)) (= a23 (_ bv4 5)) (= a23 (_ bv5 5)) (= a23 (_ bv6 5)) (= a23 (_ bv7 5)) (= a23 (_ bv8 5)) (= a23 (_ bv9 5))))
(assert (or (= a31 (_ bv1 5)) (= a31 (_ bv2 5)) (= a31 (_ bv3 5)) (= a31 (_ bv4 5)) (= a31 (_ bv5 5)) (= a31 (_ bv6 5)) (= a31 (_ bv7 5)) (= a31 (_ bv8 5)) (= a31 (_ bv9 5))))
(assert (or (= a32 (_ bv1 5)) (= a32 (_ bv2 5)) (= a32 (_ bv3 5)) (= a32 (_ bv4 5)) (= a32 (_ bv5 5)) (= a32 (_ bv6 5)) (= a32 (_ bv7 5)) (= a32 (_ bv8 5)) (= a32 (_ bv9 5))))
(assert (or (= a33 (_ bv1 5)) (= a33 (_ bv2 5)) (= a33 (_ bv3 5)) (= a33 (_ bv4 5)) (= a33 (_ bv5 5)) (= a33 (_ bv6 5)) (= a33 (_ bv7 5)) (= a33 (_ bv8 5)) (= a33 (_ bv9 5))))
(assert (distinct a11 a12))
(assert (distinct a11 a13))
(assert (distinct a11 a21))
(assert (distinct a11 a22))
(assert (distinct a11 a23))
(assert (distinct a11 a31))
(assert (distinct a11 a32))
(assert (distinct a11 a33))
(assert (distinct a12 a13))
(assert (distinct a12 a21))
(assert (distinct a12 a22))
(assert (distinct a12 a23))
(assert (distinct a12 a31))
(assert (distinct a12 a32))
(assert (distinct a12 a33))
(assert (distinct a13 a21))
(assert (distinct a13 a22))
(assert (distinct a13 a23))
(assert (distinct a13 a31))
(assert (distinct a13 a32))
(assert (distinct a13 a33))
(assert (distinct a21 a22))
(assert (distinct a21 a23))
(assert (distinct a21 a31))
(assert (distinct a21 a32))
(assert (distinct a21 a33))
(assert (distinct a22 a23))
(assert (distinct a22 a31))
(assert (distinct a22 a32))
(assert (distinct a22 a33))
(assert (distinct a23 a31))
(assert (distinct a23 a32))
(assert (distinct a23 a33))
(assert (distinct a31 a32))
(assert (distinct a31 a33))
(assert (distinct a32 a33))
(assert (= soo (bvadd (bvadd (bvadd a11 a13) a33) a31)))
(assert (= soo sum))
(assert (= sii (bvadd (bvadd (bvadd a12 a23) a32) a21)))
(assert (= sii sum))
(assert (= sol (bvadd (bvadd (bvadd a11 a12) a22) a21)))
(assert (= sol sum))
(assert (= sor (bvadd (bvadd (bvadd a12 a13) a23) a22)))
(assert (= sor sum))
(assert (= sur (bvadd (bvadd (bvadd a22 a23) a33) a32)))
(assert (= sur sum))
(assert (= sul (bvadd (bvadd (bvadd a21 a22) a32) a31)))
(assert (= sul sum))
(check-sat)