; Automatically generated by map2smt

(set-logic HORN)

(declare-datatypes ((pairOfIntInt 0) )
  (((pair-pairOfIntInt (fst-pairOfIntInt Int) (snd-pairOfIntInt Int)) )))
(declare-datatypes ((listOfpairOfIntInt 0) )
(((cons-listOfpairOfIntInt (head-listOfpairOfIntInt pairOfIntInt) (tail-listOfpairOfIntInt listOfpairOfIntInt)) (nil-listOfpairOfIntInt))))
(declare-datatypes ((listOfInt 0) )
(((cons-listOfInt (head-listOfInt Int) (tail-listOfInt listOfInt)) (nil-listOfInt))))



(declare-fun adt_eqlistpairs (listOfpairOfIntInt listOfpairOfIntInt Bool) Bool)
(declare-fun leq (Int Int Bool) Bool)
(declare-fun zip (listOfInt listOfInt listOfpairOfIntInt) Bool)
(declare-fun ff () Bool)

(assert
  (forall ( (A Bool) )
    (=>
      (= A true)
      (adt_eqlistpairs nil-listOfpairOfIntInt nil-listOfpairOfIntInt A)
    )
  )
)
(assert
  (forall ( (A pairOfIntInt) (B listOfpairOfIntInt) (C Bool) )
    (=>
      (= C false)
      (adt_eqlistpairs nil-listOfpairOfIntInt (cons-listOfpairOfIntInt A B) C)
    )
  )
)
(assert
  (forall ( (A pairOfIntInt) (B listOfpairOfIntInt) (C Bool) )
    (=>
      (= C false)
      (adt_eqlistpairs (cons-listOfpairOfIntInt A B) nil-listOfpairOfIntInt C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C listOfpairOfIntInt) (D Int) (E Int) (F listOfpairOfIntInt) (G Bool) )
    (=>
      (and
        (= G false)
        (>= A (+ D 1))
      )
      (adt_eqlistpairs (cons-listOfpairOfIntInt (pair-pairOfIntInt A B) C) (cons-listOfpairOfIntInt (pair-pairOfIntInt D E) F) G)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C listOfpairOfIntInt) (D Int) (E Int) (F listOfpairOfIntInt) (G Bool) )
    (=>
      (and
        (= G false)
        (<= A (- D 1))
      )
      (adt_eqlistpairs (cons-listOfpairOfIntInt (pair-pairOfIntInt A B) C) (cons-listOfpairOfIntInt (pair-pairOfIntInt D E) F) G)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C listOfpairOfIntInt) (D Int) (E Int) (F listOfpairOfIntInt) (G Bool) )
    (=>
      (and
        (= G false)
        (>= B (+ E 1))
      )
      (adt_eqlistpairs (cons-listOfpairOfIntInt (pair-pairOfIntInt A B) C) (cons-listOfpairOfIntInt (pair-pairOfIntInt D E) F) G)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C listOfpairOfIntInt) (D Int) (E Int) (F listOfpairOfIntInt) (G Bool) )
    (=>
      (and
        (= G false)
        (<= B (- E 1))
      )
      (adt_eqlistpairs (cons-listOfpairOfIntInt (pair-pairOfIntInt A B) C) (cons-listOfpairOfIntInt (pair-pairOfIntInt D E) F) G)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C listOfpairOfIntInt) (D listOfpairOfIntInt) (E Bool) )
    (=>
      (adt_eqlistpairs C D E)
      (adt_eqlistpairs (cons-listOfpairOfIntInt (pair-pairOfIntInt A B) C) (cons-listOfpairOfIntInt (pair-pairOfIntInt A B) D) E)
    )
  )
)
(assert
  (forall ( (A listOfInt) )
    (zip nil-listOfInt A nil-listOfpairOfIntInt)
  )
)
(assert
  (forall ( (A listOfInt) )
    (zip A nil-listOfInt nil-listOfpairOfIntInt)
  )
)
(assert
  (forall ( (A Int) (B listOfInt) (C Int) (D listOfInt) (E listOfpairOfIntInt) )
    (=>
      (zip B D E)
      (zip (cons-listOfInt A B) (cons-listOfInt C D) (cons-listOfpairOfIntInt (pair-pairOfIntInt A C) E))
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C listOfInt) (D Int) (E listOfInt) (F listOfpairOfIntInt) (G listOfpairOfIntInt) )
    (=>
      (and
        (= A true)
        (zip (cons-listOfInt B C) (cons-listOfInt D E) F)
        (zip C E G)
        (adt_eqlistpairs F (cons-listOfpairOfIntInt (pair-pairOfIntInt B D) G) A)
      )
      ff
    )
  )
)

(assert (not ff))
(check-sat)