; Automatically generated by map2smt

(set-logic HORN)




(declare-fun new81 (Int Bool Int) Bool)
(declare-fun new73 (Int) Bool)
(declare-fun new71 (Int Int Bool) Bool)
(declare-fun new69 (Int Bool Int) Bool)
(declare-fun new61 (Int) Bool)
(declare-fun new59 (Int Int Bool) Bool)
(declare-fun new53 (Int Bool Int) Bool)
(declare-fun new5 (Int Bool Int Int) Bool)
(declare-fun new45 (Int) Bool)
(declare-fun new43 (Int Int Bool) Bool)
(declare-fun new41 (Int Bool Int) Bool)
(declare-fun new4 (Bool Int) Bool)
(declare-fun new33 (Int) Bool)
(declare-fun new31 (Int Int Bool) Bool)
(declare-fun new3 (Bool Int) Bool)
(declare-fun new25 (Int Bool Int Int) Bool)
(declare-fun new2 (Int Int Int Bool Bool) Bool)
(declare-fun new19 (Int Bool Int Int) Bool)
(declare-fun new18 (Bool Int) Bool)
(declare-fun new17 (Bool Int) Bool)
(declare-fun new11 (Int Bool Int Int) Bool)
(declare-fun new1 (Int Int Int Bool Bool) Bool)
(declare-fun diff_new7 (Bool Bool Int Int Int Int Int Bool Int Int Int Int Int Int) Bool)
(declare-fun diff_new27 (Bool Bool Int Int Int Int Int Bool Int Int Int Int Int Int) Bool)
(declare-fun diff_new21 (Bool Bool Int Int Int Int Int Bool Int Int Int Int Int Int) Bool)
(declare-fun diff_new13 (Bool Bool Int Int Int Int Int Bool Int Int Int Int Int Int) Bool)
(declare-fun ff () Bool)

(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (= C 0)
        (= A 0)
      )
      (new81 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= D 0)
        (>= E 0)
        (<= F G)
        (= H (+ 1 F))
        (= I (+ E D))
        (= C (+ 1 F))
        (= A (+ 1 I))
        (new81 E B G)
        (new81 D B F)
      )
      (new81 A B C)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new73 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= A (+ 1 B))
        (new73 B)
      )
      (new73 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= B 0)
        (= A 0)
      )
      (new71 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= C true)
        (= C true)
        (>= D 0)
        (>= E 0)
        (<= F G)
        (= H (+ 1 F))
        (= I (+ E D))
        (= B (+ 1 F))
        (= A (+ 1 I))
        (new71 E G C)
        (new71 D F C)
      )
      (new71 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (= C 0)
        (= A 0)
      )
      (new69 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= D 0)
        (>= E 0)
        (<= F G)
        (= H (+ 1 F))
        (= I (+ E D))
        (= C (+ 1 F))
        (= A (+ 1 I))
        (new69 E B G)
        (new69 D B F)
      )
      (new69 A B C)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new61 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= A (+ 1 B))
        (new61 B)
      )
      (new61 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= B 0)
        (= A 0)
      )
      (new59 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= C true)
        (= C true)
        (>= D 0)
        (>= E 0)
        (<= F G)
        (= H (+ 1 F))
        (= I (+ E D))
        (= B (+ 1 F))
        (= A (+ 1 I))
        (new59 E G C)
        (new59 D F C)
      )
      (new59 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (= C 0)
        (= A 0)
      )
      (new53 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= D 0)
        (>= E 0)
        (<= F G)
        (= H (+ 1 F))
        (= I (+ E D))
        (= C (+ 1 F))
        (= A (+ 1 I))
        (new53 E B G)
        (new53 D B F)
      )
      (new53 A B C)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new45 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= A (+ 1 B))
        (new45 B)
      )
      (new45 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= B 0)
        (= A 0)
      )
      (new43 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= C true)
        (= C true)
        (>= D 0)
        (>= E 0)
        (<= F G)
        (= H (+ 1 F))
        (= I (+ E D))
        (= B (+ 1 F))
        (= A (+ 1 I))
        (new43 E G C)
        (new43 D F C)
      )
      (new43 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (= C 0)
        (= A 0)
      )
      (new41 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= D 0)
        (>= E 0)
        (<= F G)
        (= H (+ 1 F))
        (= I (+ E D))
        (= C (+ 1 F))
        (= A (+ 1 I))
        (new41 E B G)
        (new41 D B F)
      )
      (new41 A B C)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new33 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= A (+ 1 B))
        (new33 B)
      )
      (new33 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= B 0)
        (= A 0)
      )
      (new31 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= C true)
        (= C true)
        (>= D 0)
        (>= E 0)
        (<= F G)
        (= H (+ 1 F))
        (= I (+ E D))
        (= B (+ 1 F))
        (= A (+ 1 I))
        (new31 E G C)
        (new31 D F C)
      )
      (new31 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= D 0)
        (= C 0)
        (= A 0)
      )
      (new25 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= E 0)
        (>= F 0)
        (<= G H)
        (= A (+ 1 G))
        (= I (+ F E))
        (= D (+ 1 I))
        (= C (+ 1 G))
        (new41 F B H)
        (new41 E B G)
      )
      (new25 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= I 0)
        (>= H 0)
        (<= G F)
        (= K (+ H I))
        (= J 0)
        (= E 0)
        (= D (+ 1 K))
        (= C (+ 1 G))
        (new31 H F A)
        (new31 I G A)
      )
      (diff_new27 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= I 0)
        (>= H 0)
        (<= G F)
        (= K (+ H I))
        (= J (+ 1 L))
        (= E 0)
        (= D (+ 1 K))
        (= C (+ 1 G))
        (new33 L)
        (new31 H F A)
        (new31 I G A)
      )
      (diff_new27 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= I 0)
        (>= H 0)
        (<= G F)
        (= K (+ H I))
        (= J 0)
        (= D (+ 1 K))
        (= C (+ 1 G))
        (new31 H F A)
        (new31 I G A)
      )
      (diff_new27 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= I 0)
        (>= H 0)
        (<= G F)
        (= K (+ H I))
        (= J (+ 1 L))
        (= D (+ 1 K))
        (= C (+ 1 G))
        (new33 L)
        (new31 H F A)
        (new31 I G A)
      )
      (diff_new27 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= D 0)
        (= C 0)
        (= A 0)
      )
      (new19 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= E 0)
        (>= F 0)
        (<= G H)
        (= A (+ 1 G))
        (= I (+ F E))
        (= D (+ 1 I))
        (= C (+ 1 G))
        (new53 F B H)
        (new53 E B G)
      )
      (new19 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= J 0)
        (>= I 0)
        (<= H G)
        (= K (+ I J))
        (= F 0)
        (= E 0)
        (= D (+ 1 K))
        (= C (+ 1 H))
        (new43 I G A)
        (new43 J H A)
      )
      (diff_new21 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= J 0)
        (>= I 0)
        (<= H G)
        (= K (+ I J))
        (= F (+ 1 L))
        (= E 0)
        (= D (+ 1 K))
        (= C (+ 1 H))
        (new45 L)
        (new43 I G A)
        (new43 J H A)
      )
      (diff_new21 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= J 0)
        (>= I 0)
        (<= H G)
        (= K (+ I J))
        (= F 0)
        (= D (+ 1 K))
        (= C (+ 1 H))
        (new43 I G A)
        (new43 J H A)
      )
      (diff_new21 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= J 0)
        (>= I 0)
        (<= H G)
        (= K (+ I J))
        (= F (+ 1 L))
        (= D (+ 1 K))
        (= C (+ 1 H))
        (new45 L)
        (new43 I G A)
        (new43 J H A)
      )
      (diff_new21 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A true)
        (= B 0)
      )
      (new18 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= C 0)
        (>= D 0)
        (<= E F)
        (= G (+ 1 E))
        (= H (+ D C))
        (= B (+ 1 H))
        (new41 D A F)
        (new41 C A E)
      )
      (new18 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A true)
        (= B 0)
      )
      (new17 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= C 0)
        (>= D 0)
        (<= E F)
        (= G (+ 1 E))
        (= H (+ D C))
        (= B (+ 1 H))
        (new53 D A F)
        (new53 C A E)
      )
      (new17 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= D 0)
        (= C 0)
        (= A 0)
      )
      (new11 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= E 0)
        (>= F 0)
        (<= G H)
        (= A (+ 1 G))
        (= I (+ F E))
        (= D (+ 1 I))
        (= C (+ 1 G))
        (new69 F B H)
        (new69 E B G)
      )
      (new11 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= I 0)
        (>= H 0)
        (<= G F)
        (= K (+ H I))
        (= J 0)
        (= E 0)
        (= D (+ 1 K))
        (= C (+ 1 G))
        (new59 H F A)
        (new59 I G A)
      )
      (diff_new13 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= I 0)
        (>= H 0)
        (<= G F)
        (= K (+ H I))
        (= J (+ 1 L))
        (= E 0)
        (= D (+ 1 K))
        (= C (+ 1 G))
        (new61 L)
        (new59 H F A)
        (new59 I G A)
      )
      (diff_new13 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= I 0)
        (>= H 0)
        (<= G F)
        (= K (+ H I))
        (= J 0)
        (= D (+ 1 K))
        (= C (+ 1 G))
        (new59 H F A)
        (new59 I G A)
      )
      (diff_new13 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= I 0)
        (>= H 0)
        (<= G F)
        (= K (+ H I))
        (= J (+ 1 L))
        (= D (+ 1 K))
        (= C (+ 1 G))
        (new61 L)
        (new59 H F A)
        (new59 I G A)
      )
      (diff_new13 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= D 0)
        (= C 0)
        (= A 0)
      )
      (new5 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= E 0)
        (>= F 0)
        (<= G H)
        (= A (+ 1 G))
        (= I (+ F E))
        (= D (+ 1 I))
        (= C (+ 1 G))
        (new81 F B H)
        (new81 E B G)
      )
      (new5 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= J 0)
        (>= I 0)
        (<= H G)
        (= K (+ I J))
        (= F 0)
        (= E 0)
        (= D (+ 1 K))
        (= C (+ 1 H))
        (new71 I G A)
        (new71 J H A)
      )
      (diff_new7 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= J 0)
        (>= I 0)
        (<= H G)
        (= K (+ I J))
        (= F (+ 1 L))
        (= E 0)
        (= D (+ 1 K))
        (= C (+ 1 H))
        (new73 L)
        (new71 I G A)
        (new71 J H A)
      )
      (diff_new7 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= J 0)
        (>= I 0)
        (<= H G)
        (= K (+ I J))
        (= F 0)
        (= D (+ 1 K))
        (= C (+ 1 H))
        (new71 I G A)
        (new71 J H A)
      )
      (diff_new7 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= J 0)
        (>= I 0)
        (<= H G)
        (= K (+ I J))
        (= F (+ 1 L))
        (= D (+ 1 K))
        (= C (+ 1 H))
        (new73 L)
        (new71 I G A)
        (new71 J H A)
      )
      (diff_new7 A A B B C C D A E F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A true)
        (= B 0)
      )
      (new4 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= C 0)
        (>= D 0)
        (<= E F)
        (= G (+ 1 E))
        (= H (+ D C))
        (= B (+ 1 H))
        (new69 D A F)
        (new69 C A E)
      )
      (new4 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A true)
        (= B 0)
      )
      (new3 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= C 0)
        (>= D 0)
        (<= E F)
        (= G (+ 1 E))
        (= H (+ D C))
        (= B (+ 1 H))
        (new81 D A F)
        (new81 C A E)
      )
      (new3 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= D true)
        (= B 0)
        (new3 C A)
      )
      (new2 A A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= C true)
        (= B 0)
        (new4 D A)
      )
      (new2 A B A C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Bool) (B1 Int) (C1 Int) (D1 Int) (E1 Bool) )
    (=>
      (and
        (= F 1)
        (= G 1)
        (= E true)
        (= D true)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= L 0)
        (<= M N)
        (<= O P)
        (<= Q R)
        (<= S (- T 1))
        (= U (+ 1 M))
        (= V (+ 1 O))
        (= W (+ 1 Q))
        (= X (+ I H))
        (= Y (+ L J))
        (= Z (+ L K))
        (= C (+ 1 X))
        (= B (+ 1 Y))
        (= A (+ 1 Z))
        (diff_new7 E A1 S B1 W C1 D1 E1 O M R Q I H)
        (new5 P D N L)
        (new2 K J D1 D E1)
      )
      (new2 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Bool) (B1 Int) (C1 Int) (D1 Int) (E1 Bool) )
    (=>
      (and
        (= F 0)
        (= G 1)
        (= E true)
        (= D true)
        (>= H (+ I 1))
        (>= J 0)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (>= N 0)
        (<= O P)
        (<= Q R)
        (<= S (- T 1))
        (= U (+ 1 O))
        (= V (+ 1 I))
        (= W (+ 1 Q))
        (= X (+ K J))
        (= Y (+ M L))
        (= Z (+ N M))
        (= C (+ 1 X))
        (= B (+ 1 Y))
        (= A (+ 1 Z))
        (diff_new7 E A1 S B1 W C1 D1 E1 H O R Q K J)
        (new2 N L D1 D E1)
        (new5 I D P M)
      )
      (new2 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Bool) (B1 Int) (C1 Int) (D1 Int) (E1 Bool) )
    (=>
      (and
        (= F 1)
        (= G 0)
        (= E true)
        (= D true)
        (>= H I)
        (>= J 0)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (>= N 0)
        (<= O P)
        (<= Q R)
        (<= S T)
        (= U (+ 1 O))
        (= V (+ 1 Q))
        (= W (+ 1 S))
        (= X (+ N J))
        (= Y (+ L K))
        (= Z (+ N M))
        (= C (+ 1 X))
        (= B (+ 1 Y))
        (= A (+ 1 Z))
        (diff_new13 D A1 I B1 W C1 D1 E1 Q T S L K O)
        (new11 R E P N)
        (new2 M D1 J E1 E)
      )
      (new2 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Bool) (B1 Int) (C1 Int) (D1 Int) (E1 Bool) )
    (=>
      (and
        (= F 0)
        (= G 0)
        (= E true)
        (= D true)
        (>= H (+ I 1))
        (>= J K)
        (>= L 0)
        (>= M 0)
        (>= N 0)
        (>= O 0)
        (>= P 0)
        (<= Q R)
        (<= S T)
        (= U (+ 1 Q))
        (= V (+ 1 I))
        (= W (+ 1 S))
        (= X (+ O L))
        (= Y (+ N M))
        (= Z (+ P O))
        (= C (+ 1 X))
        (= B (+ 1 Y))
        (= A (+ 1 Z))
        (diff_new13 D A1 K B1 W C1 D1 E1 H T S N M Q)
        (new2 P D1 L E1 E)
        (new11 I E R O)
      )
      (new2 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= D true)
        (= B 0)
        (new17 C A)
      )
      (new1 A A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= C true)
        (= B 0)
        (new18 D A)
      )
      (new1 A B A C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Bool) (B1 Int) (C1 Int) (D1 Int) (E1 Bool) )
    (=>
      (and
        (= F 1)
        (= G 1)
        (= E true)
        (= D true)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= L 0)
        (<= M N)
        (<= O P)
        (<= Q R)
        (<= S (- T 1))
        (= U (+ 1 M))
        (= V (+ 1 O))
        (= W (+ 1 Q))
        (= X (+ I H))
        (= Y (+ L J))
        (= Z (+ L K))
        (= C (+ 1 X))
        (= B (+ 1 Y))
        (= A (+ 1 Z))
        (diff_new21 E A1 S B1 W C1 D1 E1 O M R Q I H)
        (new19 P D N L)
        (new1 K J D1 D E1)
      )
      (new1 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Bool) (B1 Int) (C1 Int) (D1 Int) (E1 Bool) )
    (=>
      (and
        (= F 0)
        (= G 1)
        (= E true)
        (= D true)
        (>= H (+ I 1))
        (>= J 0)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (>= N 0)
        (<= O P)
        (<= Q R)
        (<= S (- T 1))
        (= U (+ 1 O))
        (= V (+ 1 I))
        (= W (+ 1 Q))
        (= X (+ K J))
        (= Y (+ M L))
        (= Z (+ N M))
        (= C (+ 1 X))
        (= B (+ 1 Y))
        (= A (+ 1 Z))
        (diff_new21 E A1 S B1 W C1 D1 E1 H O R Q K J)
        (new1 N L D1 D E1)
        (new19 I D P M)
      )
      (new1 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Bool) (B1 Int) (C1 Int) (D1 Int) (E1 Bool) )
    (=>
      (and
        (= F 1)
        (= G 0)
        (= E true)
        (= D true)
        (>= H I)
        (>= J 0)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (>= N 0)
        (<= O P)
        (<= Q R)
        (<= S T)
        (= U (+ 1 O))
        (= V (+ 1 Q))
        (= W (+ 1 S))
        (= X (+ N J))
        (= Y (+ L K))
        (= Z (+ N M))
        (= C (+ 1 X))
        (= B (+ 1 Y))
        (= A (+ 1 Z))
        (diff_new27 D A1 I B1 W C1 D1 E1 Q T S L K O)
        (new25 R E P N)
        (new1 M D1 J E1 E)
      )
      (new1 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Bool) (B1 Int) (C1 Int) (D1 Int) (E1 Bool) )
    (=>
      (and
        (= F 0)
        (= G 0)
        (= E true)
        (= D true)
        (>= H (+ I 1))
        (>= J K)
        (>= L 0)
        (>= M 0)
        (>= N 0)
        (>= O 0)
        (>= P 0)
        (<= Q R)
        (<= S T)
        (= U (+ 1 Q))
        (= V (+ 1 I))
        (= W (+ 1 S))
        (= X (+ O L))
        (= Y (+ N M))
        (= Z (+ P O))
        (= C (+ 1 X))
        (= B (+ 1 Y))
        (= A (+ 1 Z))
        (diff_new27 D A1 K B1 W C1 D1 E1 H T S N M Q)
        (new1 P D1 L E1 E)
        (new25 I E R O)
      )
      (new1 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A true)
        (<= (+ B 1) C)
        (= (+ D E) B)
        (new1 C D E A A)
      )
      ff
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A true)
        (>= B (+ C 1))
        (= (+ D E) B)
        (new2 C D E A A)
      )
      ff
    )
  )
)

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