(set-logic QF_UFBV)
(declare-fun b ((_ BitVec 12) (_ BitVec 6)) Bool)
(declare-fun a ((_ BitVec 11) (_ BitVec 9) (_ BitVec 15)) (_ BitVec 10))
(declare-fun d () (_ BitVec 7))
(declare-fun c ((_ BitVec 15) (_ BitVec 15) (_ BitVec 1)) Bool)
(assert (let ((a!1 (a ((_ zero_extend 2) #b001010001)
              ((_ sign_extend 8) (ite (bvsle #b001010001 #b001010001) #b1 #b0))
              ((_ sign_extend 14) (ite (bvsle #b001010001 #b001010001) #b1 #b0))))
      (a!6 (b ((_ zero_extend 11) (ite (bvsle #b001010001 #b001010001) #b1 #b0))
              ((_ sign_extend 5) (ite (bvsle #b001010001 #b001010001) #b1 #b0)))))
(let ((a!2 (c ((_ zero_extend 14) (ite (bvsle #b001010001 #b001010001) #b1 #b0))
              ((_ zero_extend 6) #b001010001)
              ((_ extract 3 3) a!1)))
      (a!3 (bvule (ite (bvsle #b001010001 #b001010001) #b1 #b0)
                  (ite (b ((_ sign_extend 5) d) ((_ extract 7 2) a!1)) #b1 #b0)))
      (a!4 (ite (c ((_ sign_extend 5) (bvsrem a!1 a!1))
                   ((_ zero_extend 6) #b001010001)
                   ((_ extract 8 8) (bvsrem a!1 a!1)))
                #b1
                #b0)))
(let ((a!5 (bvslt a!4
                  (ite (b ((_ sign_extend 5) d) ((_ extract 7 2) a!1)) #b1 #b0))))
  (ite (= a!2 a!3) (xor a!5 a!6) (= a!2 a!3))))))
(set-info :status sat)
(check-sat)