(set-option :smtlib2_compliant true)
(set-logic ALL)
(declare-fun divides (Int Int) Bool)
(declare-fun mul (Int Int) Int)
(define-fun s0 () Bool (forall ((l1_s0 Int) (l1_s1 Int))
  (let ((l1_s2 (mul l1_s0 l1_s1)))
  (let ((l1_s3 (* l1_s0 l1_s1)))
  (let ((l1_s4 (= l1_s2 l1_s3)))
  l1_s4)))))
(define-fun s1 () Bool (forall ((l1_s0 Int) (l1_s1 Int))
  (let ((l1_s3 0))
  (let ((l1_s11 1))
  (let ((l1_s12 (- 1)))
  (let ((l1_s2 (divides l1_s0 l1_s1)))
  (let ((l1_s4 (= l1_s0 l1_s3)))
  (let ((l1_s5 (mod l1_s1 l1_s0)))
  (let ((l1_s6 (ite l1_s4 l1_s1 l1_s5)))
  (let ((l1_s7 (>= l1_s1 l1_s3)))
  (let ((l1_s8 (= l1_s3 l1_s6)))
  (let ((l1_s9 (or l1_s7 l1_s8)))
  (let ((l1_s10 (> l1_s0 l1_s3)))
  (let ((l1_s13 (ite l1_s10 l1_s11 l1_s12)))
  (let ((l1_s14 (ite l1_s9 l1_s3 l1_s13)))
  (let ((l1_s15 (* l1_s0 l1_s14)))
  (let ((l1_s16 (- l1_s6 l1_s15)))
  (let ((l1_s17 (ite l1_s4 l1_s1 l1_s16)))
  (let ((l1_s18 (> l1_s17 l1_s3)))
  (let ((l1_s19 (< l1_s17 l1_s3)))
  (let ((l1_s20 (ite l1_s19 l1_s12 l1_s17)))
  (let ((l1_s21 (ite l1_s18 l1_s11 l1_s20)))
  (let ((l1_s22 (< l1_s0 l1_s3)))
  (let ((l1_s23 (ite l1_s22 l1_s12 l1_s0)))
  (let ((l1_s24 (ite l1_s10 l1_s11 l1_s23)))
  (let ((l1_s25 (- l1_s24)))
  (let ((l1_s26 (= l1_s21 l1_s25)))
  (let ((l1_s27 (+ l1_s0 l1_s17)))
  (let ((l1_s28 (ite l1_s26 l1_s27 l1_s17)))
  (let ((l1_s29 (ite l1_s4 l1_s1 l1_s28)))
  (let ((l1_s30 (= l1_s3 l1_s29)))
  (let ((l1_s31 (= l1_s2 l1_s30)))
  l1_s31))))))))))))))))))))))))))))))))
(define-fun s2 () Bool (and s0 s1))
(define-fun s3 () Bool (forall ((l1_s0 Int) (l1_s1 Int))
  (let ((l1_s2 0))
  (let ((l1_s13 1))
  (let ((l1_s14 (- 1)))
  (let ((l1_s3 (distinct l1_s1 l1_s2)))
  (let ((l1_s4 (divides l1_s0 l1_s1)))
  (let ((l1_s5 (and l1_s3 l1_s4)))
  (let ((l1_s6 (= l1_s1 l1_s2)))
  (let ((l1_s7 (mod l1_s0 l1_s1)))
  (let ((l1_s8 (ite l1_s6 l1_s0 l1_s7)))
  (let ((l1_s9 (>= l1_s0 l1_s2)))
  (let ((l1_s10 (= l1_s2 l1_s8)))
  (let ((l1_s11 (or l1_s9 l1_s10)))
  (let ((l1_s12 (> l1_s1 l1_s2)))
  (let ((l1_s15 (ite l1_s12 l1_s13 l1_s14)))
  (let ((l1_s16 (ite l1_s11 l1_s2 l1_s15)))
  (let ((l1_s17 (* l1_s1 l1_s16)))
  (let ((l1_s18 (- l1_s8 l1_s17)))
  (let ((l1_s19 (ite l1_s6 l1_s0 l1_s18)))
  (let ((l1_s20 (> l1_s19 l1_s2)))
  (let ((l1_s21 (< l1_s19 l1_s2)))
  (let ((l1_s22 (ite l1_s21 l1_s14 l1_s19)))
  (let ((l1_s23 (ite l1_s20 l1_s13 l1_s22)))
  (let ((l1_s24 (< l1_s1 l1_s2)))
  (let ((l1_s25 (ite l1_s24 l1_s14 l1_s1)))
  (let ((l1_s26 (ite l1_s12 l1_s13 l1_s25)))
  (let ((l1_s27 (- l1_s26)))
  (let ((l1_s28 (= l1_s23 l1_s27)))
  (let ((l1_s29 (div l1_s0 l1_s1)))
  (let ((l1_s30 (ite l1_s6 l1_s2 l1_s29)))
  (let ((l1_s31 (+ l1_s16 l1_s30)))
  (let ((l1_s32 (ite l1_s6 l1_s2 l1_s31)))
  (let ((l1_s33 (- l1_s32 l1_s13)))
  (let ((l1_s34 (ite l1_s28 l1_s33 l1_s32)))
  (let ((l1_s35 (ite l1_s6 l1_s2 l1_s34)))
  (let ((l1_s36 (mul l1_s35 l1_s1)))
  (let ((l1_s37 (= l1_s0 l1_s36)))
  (let ((l1_s38 (=> l1_s5 l1_s37)))
  l1_s38)))))))))))))))))))))))))))))))))))))))
(define-fun s4 () Bool (=> s2 s3))
(assert (not s4))
(check-sat)
(get-info :reason-unknown)