; Automatically generated by map2smt

(set-logic HORN)




(declare-fun new8 (Int Int) Bool)
(declare-fun new7 (Int Int) Bool)
(declare-fun new26 (Int Int) Bool)
(declare-fun new25 (Int Int) Bool)
(declare-fun new24 (Int Int) Bool)
(declare-fun new23 (Int Int) Bool)
(declare-fun new2 (Int Int) Bool)
(declare-fun new19 (Int Int Int Int Int) Bool)
(declare-fun new18 (Int Int Int Int Int) Bool)
(declare-fun new16 (Int Int) Bool)
(declare-fun new15 (Int Int) Bool)
(declare-fun new11 (Int Int Int Int Int) Bool)
(declare-fun new10 (Int Int Int Int Int) Bool)
(declare-fun new1 (Int Int) Bool)
(declare-fun diff_new6 (Int Int Int Int Int Int) Bool)
(declare-fun diff_new4 (Int Int Int Int Int Int) Bool)
(declare-fun ff () Bool)

(assert
  (forall ( (A Int) )
    (new26 A A)
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (new26 C B)
      (new26 A B)
    )
  )
)
(assert
  (forall ( (A Int) )
    (new25 A A)
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (new25 C B)
      (new25 A B)
    )
  )
)
(assert
  (forall ( (A Int) )
    (new24 A A)
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (new24 C B)
      (new24 A B)
    )
  )
)
(assert
  (forall ( (A Int) )
    (new23 A A)
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (new23 C B)
      (new23 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (new23 B C)
      (new19 A B C B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (new24 B C)
      (new18 A B C B C)
    )
  )
)
(assert
  (forall ( (A Int) )
    (new16 A A)
  )
)
(assert
  (forall ( (A Int) )
    (new15 A A)
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (new25 B C)
      (new11 A B C B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (new26 B C)
      (new10 A B C B C)
    )
  )
)
(assert
  (forall ( (A Int) )
    (new8 A A)
  )
)
(assert
  (forall ( (A Int) )
    (new7 A A)
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (new7 C D)
        (new8 B E)
      )
      (diff_new6 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (new7 C D)
        (new10 F G E G B)
      )
      (diff_new6 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (new11 F G D G C)
        (new8 B E)
      )
      (diff_new6 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (new11 F G D G C)
        (new10 H I E I B)
      )
      (diff_new6 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (new15 C D)
        (new16 B E)
      )
      (diff_new4 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (new15 C D)
        (new18 F G E G B)
      )
      (diff_new4 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (new19 F G D G C)
        (new16 B E)
      )
      (diff_new4 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (new19 F G D G C)
        (new18 H I E I B)
      )
      (diff_new4 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (diff_new4 C D E F B A)
        (new2 E F)
      )
      (new2 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (diff_new6 C D E F B A)
        (new1 E F)
      )
      (new1 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (>= (- A B) 1)
        (new1 B A)
      )
      ff
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (<= (- A B) (- 1))
        (new2 B A)
      )
      ff
    )
  )
)

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