(set-logic HORN)

(declare-fun P1 ( Int) Bool)
(declare-fun P2 ( Int  Int) Bool)

(assert (not (exists ((x0 Int)) (P1 x0))))

(assert (forall ((x0 Int) (x2 Int))
  (let ((a!1 (and (not (= x2 0)) (and (P2 0 x2) (not (= x2 0)))))
        (a!2 (and (and (P2 0 x2) (not (= x2 0))) (not (= x2 0)))))
  (let ((a!3 (and (not (= x2 0)) (and (not (= x2 0)) a!1)))
        (a!4 (and (and a!2 (not (= x2 0))))))
  (let ((a!5 (and (and a!3 (not (= x2 0))) (not (= x2 0)))))
  (let ((a!6 (and a!5 a!5 a!5 (and a!3 (not (= x2 0))) a!5)))
  (let ((a!7 (and (and a!4 a!4 (not (= x2 0)))
                   (and a!4 a!4 (not (= x2 0)))))
        (a!8 (and (and a!6 a!6 a!5))))
  (let ((a!9 (and a!7 a!7 a!7 (and a!4 a!4 (not (= x2 0))) a!7))
        (a!10 (and (and a!8 a!8 a!8 (and a!6 a!6 a!5) a!8)
                   (and a!8 a!8 a!8 (and a!6 a!6 a!5) a!8)
                   a!8)))
  (let ((a!11 (and (and (and (and a!9 a!7) a!9) (and a!9 a!7))
                   (and (and (and a!9 a!7) a!9) (and a!9 a!7))
                   (and (and (and a!9 a!7) a!9) (and a!9 a!7))
                   (and (and a!9 a!7) a!9)))
        (a!12 (and a!10 (and a!8 a!8 a!8 (and a!6 a!6 a!5) a!8))))
  (let ((a!13 (and a!11
                   (and (and a!9 a!7) (and a!9 a!7))))
        (a!14 (and (and (and a!12 a!10) (and a!12 a!10) a!12)
                   (and (and a!12 a!10) (and a!12 a!10) a!12)
                   (and (and a!12 a!10) (and a!12 a!10) a!12)
                   (and (and a!12 a!10) (and a!12 a!10) a!12)
                   (and (and a!12 a!10) (and a!12 a!10) a!12)
                   (and (and a!12 a!10) (and a!12 a!10) a!12)
                   (and (and a!12 a!10) (and a!12 a!10) a!12)
                   (and (and a!12 a!10) (and a!12 a!10) a!12)
                   (and (and a!12 a!10) (and a!12 a!10) a!12)
                   (and (and a!12 a!10) (and a!12 a!10) a!12)
                   (and (and a!12 a!10) (and a!12 a!10) a!12)
                   (and (and a!12 a!10) (and a!12 a!10) a!12))))
  (let ((a!15 (and a!14 a!14 (and (and a!12 a!10) (and a!12 a!10) a!12))))
  (let ((a!16 (and (and a!13 a!13)
                   (and a!13 a!13)
                   a!15
                   a!14
                   a!14
                   a!15
                   a!15
                   (not (= x2 0)))))
  (let ((a!17 (not (and a!16 a!16 (not (= x2 0))))))
    (or (P1 x0) a!17))))))))))))))
    
(assert (forall ((x1 Int) (x0 Int)) (or (not (= x1 x0)) (P2 x1 x0))))

(check-sat)