; Automatically generated by map2smt

(set-logic HORN)




(declare-fun new9 (Int Int Bool) Bool)
(declare-fun new6 (Int) Bool)
(declare-fun new37 (Int Int Bool Int Int Int Int Int Bool Bool Int Int Int Bool Int) Bool)
(declare-fun new31 (Int Int Bool Int Int Int Int Bool Int Int Int Bool Bool Int Int) Bool)
(declare-fun new30 (Int Int Bool Int) Bool)
(declare-fun new3 (Int) Bool)
(declare-fun new27 (Int) Bool)
(declare-fun new26 (Int Int Bool) Bool)
(declare-fun new20 (Int Int Bool Int Int Int Int Int Bool Bool Int Int Int Bool Int) Bool)
(declare-fun new2 (Int Int Int Bool) Bool)
(declare-fun new14 (Int Int Bool Int Int Int Int Bool Int Int Int Bool Bool Int Int) Bool)
(declare-fun new13 (Int Int Bool Int) Bool)
(declare-fun new10 (Int) Bool)
(declare-fun new1 (Int Int Int Bool) Bool)
(declare-fun diff_new8 (Bool Bool Int Int Int Bool Int Int Int Int Int) Bool)
(declare-fun diff_new5 (Bool Bool Int Int Int Bool Int Int Int Int Int) Bool)
(declare-fun ff () Bool)

(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Bool) (L Int) (M Int) )
    (=>
      (and
        (= C true)
        (= K true)
        (= C true)
        (>= G 0)
        (>= F 0)
        (<= I H)
        (= M (+ F G))
        (= L 0)
        (= J 0)
        (= A (+ 1 I))
        (= D (+ 1 I))
        (= B (+ 1 M))
        (new26 H F C)
        (new26 I G C)
      )
      (new37 A B C D A E F G C C H I J K L)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Bool) (J Int) (K Int) (L Int) (M Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 1)
        (= P 1)
        (= M true)
        (= C true)
        (= M true)
        (= C true)
        (>= Q 0)
        (>= R 0)
        (>= S 0)
        (>= G 0)
        (<= T J)
        (<= U V)
        (<= W X)
        (<= Y (- F 1))
        (= A (+ 1 W))
        (= A (+ 1 T))
        (= Z (+ 1 U))
        (= A1 (+ R Q))
        (= B1 (+ G S))
        (= N (+ 1 U))
        (= L (+ 1 A1))
        (= D (+ 1 T))
        (= B (+ 1 B1))
        (new30 X G C J)
        (new31 W S C T Z Y H I K R Q M M V U)
      )
      (new37 A B C D E F G H C I J K L M N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Bool) (J Int) (K Int) (L Int) (M Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 0)
        (= P 1)
        (= M true)
        (= C true)
        (= M true)
        (= C true)
        (>= Q (+ R 1))
        (>= S 0)
        (>= T 0)
        (>= G 0)
        (>= U 0)
        (<= J V)
        (<= W X)
        (<= Y (- F 1))
        (= A (+ 1 R))
        (= A (+ 1 J))
        (= Z (+ 1 W))
        (= A1 (+ T S))
        (= B1 (+ U G))
        (= N (+ 1 W))
        (= L (+ 1 A1))
        (= D (+ 1 J))
        (= B (+ 1 B1))
        (new31 Q U C V Z Y H I K T S M M X W)
        (new30 R G C J)
      )
      (new37 A B C D E F G H C I J K L M N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Bool) (J Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 1)
        (= P 0)
        (= C true)
        (= C true)
        (= C true)
        (= C true)
        (>= Q F)
        (>= R 0)
        (>= S 0)
        (>= T 0)
        (>= S 0)
        (<= U V)
        (<= W V)
        (<= X Y)
        (= Z (+ 1 W))
        (= A (+ 1 X))
        (= A (+ 1 U))
        (= A1 (+ S R))
        (= B1 (+ S T))
        (= N (+ 1 W))
        (= M (+ 1 A1))
        (= D (+ 1 U))
        (= B (+ 1 B1))
        (new30 Y S C V)
        (new37 X T C U E F G H I J K L R C W)
      )
      (new37 A B C D E F G H I J K L M C N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Bool) (J Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 0)
        (= P 0)
        (= C true)
        (= C true)
        (= C true)
        (= C true)
        (>= Q (+ R 1))
        (>= S F)
        (>= T 0)
        (>= U 0)
        (>= U 0)
        (>= V 0)
        (<= W X)
        (<= Y W)
        (= Z (+ 1 Y))
        (= A (+ 1 R))
        (= A (+ 1 W))
        (= A1 (+ U T))
        (= B1 (+ V U))
        (= N (+ 1 Y))
        (= M (+ 1 A1))
        (= D (+ 1 W))
        (= B (+ 1 B1))
        (new37 Q V C X E F G H I J K L T C Y)
        (new30 R U C W)
      )
      (new37 A B C D E F G H I J K L M C N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= C true)
        (= G true)
        (= C true)
        (>= J 0)
        (>= I 0)
        (<= L K)
        (= M (+ I J))
        (= H 0)
        (= F 0)
        (= A (+ 1 L))
        (= D (+ 1 L))
        (= B (+ 1 M))
        (new26 K I C)
        (new26 L J C)
      )
      (new31 A B C D A E F G H I J C C K L)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Bool) (L Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 1)
        (= P 1)
        (= C true)
        (= C true)
        (= C true)
        (= C true)
        (>= Q 0)
        (>= R 0)
        (>= S 0)
        (>= R 0)
        (<= T U)
        (<= V U)
        (<= W X)
        (<= F (- Y 1))
        (= Z (+ 1 V))
        (= A (+ 1 W))
        (= A (+ 1 T))
        (= A1 (+ R Q))
        (= B1 (+ R S))
        (= H (+ 1 V))
        (= G (+ 1 A1))
        (= D (+ 1 T))
        (= B (+ 1 B1))
        (new30 X R C U)
        (new31 W S C T E F Q C V I J K L M N)
      )
      (new31 A B C D E F G C H I J K L M N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Bool) (L Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 0)
        (= P 1)
        (= C true)
        (= C true)
        (= C true)
        (= C true)
        (>= Q (+ R 1))
        (>= S 0)
        (>= T 0)
        (>= T 0)
        (>= U 0)
        (<= V W)
        (<= X V)
        (<= F (- Y 1))
        (= Z (+ 1 X))
        (= A (+ 1 R))
        (= A (+ 1 V))
        (= A1 (+ T S))
        (= B1 (+ U T))
        (= H (+ 1 X))
        (= G (+ 1 A1))
        (= D (+ 1 V))
        (= B (+ 1 B1))
        (new31 Q U C W E F S C X I J K L M N)
        (new30 R T C V)
      )
      (new31 A B C D E F G C H I J K L M N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Bool) (I Int) (J Int) (K Int) (L Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 1)
        (= P 0)
        (= H true)
        (= C true)
        (= H true)
        (= C true)
        (>= Q 0)
        (>= R 0)
        (>= S 0)
        (>= J 0)
        (>= F T)
        (<= U M)
        (<= V W)
        (<= X Y)
        (= A (+ 1 X))
        (= A (+ 1 U))
        (= Z (+ 1 V))
        (= A1 (+ R Q))
        (= B1 (+ J S))
        (= I (+ 1 V))
        (= G (+ 1 A1))
        (= D (+ 1 U))
        (= B (+ 1 B1))
        (new30 Y J C M)
        (new37 X S C U Z T R Q H H W V K L N)
      )
      (new31 A B C D E F G H I J K C L M N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Bool) (I Int) (J Int) (K Int) (L Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 0)
        (= P 0)
        (= H true)
        (= C true)
        (= H true)
        (= C true)
        (>= Q (+ R 1))
        (>= S 0)
        (>= T 0)
        (>= J 0)
        (>= U 0)
        (>= F V)
        (<= M W)
        (<= X Y)
        (= A (+ 1 R))
        (= A (+ 1 M))
        (= Z (+ 1 X))
        (= A1 (+ T S))
        (= B1 (+ U J))
        (= I (+ 1 X))
        (= G (+ 1 A1))
        (= D (+ 1 M))
        (= B (+ 1 B1))
        (new37 Q U C W Z V T S H H Y X K L N)
        (new30 R J C M)
      )
      (new31 A B C D E F G H I J K C L M N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= D 0)
        (= B 0)
        (= A 0)
      )
      (new30 A B C D)
    )
  )
)
(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)
        (>= E 0)
        (>= F 0)
        (<= G H)
        (= A (+ 1 G))
        (= I (+ F E))
        (= D (+ 1 G))
        (= B (+ 1 I))
        (new26 H F C)
        (new26 G E C)
      )
      (new30 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new27 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= A (+ 1 B))
        (new27 B)
      )
      (new27 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= B 0)
        (= A 0)
      )
      (new26 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 I))
        (= A (+ 1 F))
        (new26 G E C)
        (new26 F D C)
      )
      (new26 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Bool) (L Int) (M Int) )
    (=>
      (and
        (= C true)
        (= K true)
        (= C true)
        (>= G 0)
        (>= F 0)
        (<= I H)
        (= M (+ F G))
        (= L 0)
        (= J 0)
        (= A (+ 1 I))
        (= D (+ 1 I))
        (= B (+ 1 M))
        (new9 H F C)
        (new9 I G C)
      )
      (new20 A B C D A E F G C C H I J K L)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Bool) (J Int) (K Int) (L Int) (M Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 1)
        (= P 1)
        (= M true)
        (= C true)
        (= M true)
        (= C true)
        (>= Q 0)
        (>= R 0)
        (>= S 0)
        (>= G 0)
        (<= T J)
        (<= U V)
        (<= W X)
        (<= Y (- F 1))
        (= A (+ 1 W))
        (= A (+ 1 T))
        (= Z (+ 1 U))
        (= A1 (+ R Q))
        (= B1 (+ G S))
        (= N (+ 1 U))
        (= L (+ 1 A1))
        (= D (+ 1 T))
        (= B (+ 1 B1))
        (new13 X G C J)
        (new14 W S C T Z Y H I K R Q M M V U)
      )
      (new20 A B C D E F G H C I J K L M N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Bool) (J Int) (K Int) (L Int) (M Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 0)
        (= P 1)
        (= M true)
        (= C true)
        (= M true)
        (= C true)
        (>= Q (+ R 1))
        (>= S 0)
        (>= T 0)
        (>= G 0)
        (>= U 0)
        (<= J V)
        (<= W X)
        (<= Y (- F 1))
        (= A (+ 1 R))
        (= A (+ 1 J))
        (= Z (+ 1 W))
        (= A1 (+ T S))
        (= B1 (+ U G))
        (= N (+ 1 W))
        (= L (+ 1 A1))
        (= D (+ 1 J))
        (= B (+ 1 B1))
        (new14 Q U C V Z Y H I K T S M M X W)
        (new13 R G C J)
      )
      (new20 A B C D E F G H C I J K L M N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Bool) (J Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 1)
        (= P 0)
        (= C true)
        (= C true)
        (= C true)
        (= C true)
        (>= Q F)
        (>= R 0)
        (>= S 0)
        (>= T 0)
        (>= S 0)
        (<= U V)
        (<= W V)
        (<= X Y)
        (= Z (+ 1 W))
        (= A (+ 1 X))
        (= A (+ 1 U))
        (= A1 (+ S R))
        (= B1 (+ S T))
        (= N (+ 1 W))
        (= M (+ 1 A1))
        (= D (+ 1 U))
        (= B (+ 1 B1))
        (new13 Y S C V)
        (new20 X T C U E F G H I J K L R C W)
      )
      (new20 A B C D E F G H I J K L M C N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Bool) (J Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 0)
        (= P 0)
        (= C true)
        (= C true)
        (= C true)
        (= C true)
        (>= Q (+ R 1))
        (>= S F)
        (>= T 0)
        (>= U 0)
        (>= U 0)
        (>= V 0)
        (<= W X)
        (<= Y W)
        (= Z (+ 1 Y))
        (= A (+ 1 R))
        (= A (+ 1 W))
        (= A1 (+ U T))
        (= B1 (+ V U))
        (= N (+ 1 Y))
        (= M (+ 1 A1))
        (= D (+ 1 W))
        (= B (+ 1 B1))
        (new20 Q V C X E F G H I J K L T C Y)
        (new13 R U C W)
      )
      (new20 A B C D E F G H I J K L M C N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= C true)
        (= G true)
        (= C true)
        (>= J 0)
        (>= I 0)
        (<= L K)
        (= M (+ I J))
        (= H 0)
        (= F 0)
        (= A (+ 1 L))
        (= D (+ 1 L))
        (= B (+ 1 M))
        (new9 K I C)
        (new9 L J C)
      )
      (new14 A B C D A E F G H I J C C K L)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Bool) (L Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 1)
        (= P 1)
        (= C true)
        (= C true)
        (= C true)
        (= C true)
        (>= Q 0)
        (>= R 0)
        (>= S 0)
        (>= R 0)
        (<= T U)
        (<= V U)
        (<= W X)
        (<= F (- Y 1))
        (= Z (+ 1 V))
        (= A (+ 1 W))
        (= A (+ 1 T))
        (= A1 (+ R Q))
        (= B1 (+ R S))
        (= H (+ 1 V))
        (= G (+ 1 A1))
        (= D (+ 1 T))
        (= B (+ 1 B1))
        (new13 X R C U)
        (new14 W S C T E F Q C V I J K L M N)
      )
      (new14 A B C D E F G C H I J K L M N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Bool) (L Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 0)
        (= P 1)
        (= C true)
        (= C true)
        (= C true)
        (= C true)
        (>= Q (+ R 1))
        (>= S 0)
        (>= T 0)
        (>= T 0)
        (>= U 0)
        (<= V W)
        (<= X V)
        (<= F (- Y 1))
        (= Z (+ 1 X))
        (= A (+ 1 R))
        (= A (+ 1 V))
        (= A1 (+ T S))
        (= B1 (+ U T))
        (= H (+ 1 X))
        (= G (+ 1 A1))
        (= D (+ 1 V))
        (= B (+ 1 B1))
        (new14 Q U C W E F S C X I J K L M N)
        (new13 R T C V)
      )
      (new14 A B C D E F G C H I J K L M N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Bool) (I Int) (J Int) (K Int) (L Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 1)
        (= P 0)
        (= H true)
        (= C true)
        (= H true)
        (= C true)
        (>= Q 0)
        (>= R 0)
        (>= S 0)
        (>= J 0)
        (>= F T)
        (<= U M)
        (<= V W)
        (<= X Y)
        (= A (+ 1 X))
        (= A (+ 1 U))
        (= Z (+ 1 V))
        (= A1 (+ R Q))
        (= B1 (+ J S))
        (= I (+ 1 V))
        (= G (+ 1 A1))
        (= D (+ 1 U))
        (= B (+ 1 B1))
        (new13 Y J C M)
        (new20 X S C U Z T R Q H H W V K L N)
      )
      (new14 A B C D E F G H I J K C L M N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Bool) (I Int) (J Int) (K Int) (L Bool) (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 Int) (B1 Int) )
    (=>
      (and
        (= O 0)
        (= P 0)
        (= H true)
        (= C true)
        (= H true)
        (= C true)
        (>= Q (+ R 1))
        (>= S 0)
        (>= T 0)
        (>= J 0)
        (>= U 0)
        (>= F V)
        (<= M W)
        (<= X Y)
        (= A (+ 1 R))
        (= A (+ 1 M))
        (= Z (+ 1 X))
        (= A1 (+ T S))
        (= B1 (+ U J))
        (= I (+ 1 X))
        (= G (+ 1 A1))
        (= D (+ 1 M))
        (= B (+ 1 B1))
        (new20 Q U C W Z V T S H H Y X K L N)
        (new13 R J C M)
      )
      (new14 A B C D E F G H I J K C L M N)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= D 0)
        (= B 0)
        (= A 0)
      )
      (new13 A B C D)
    )
  )
)
(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)
        (>= E 0)
        (>= F 0)
        (<= G H)
        (= A (+ 1 G))
        (= I (+ F E))
        (= D (+ 1 G))
        (= B (+ 1 I))
        (new9 H F C)
        (new9 G E C)
      )
      (new13 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new10 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= A (+ 1 B))
        (new10 B)
      )
      (new10 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= B 0)
        (= A 0)
      )
      (new9 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 I))
        (= A (+ 1 F))
        (new9 G E C)
        (new9 F D C)
      )
      (new9 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= B true)
        (= H 0)
        (= G 0)
        (= D (+ 1 I))
        (new9 F E A)
        (new10 I)
      )
      (diff_new8 A B C D E A F E G H I)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= A true)
        (= G 0)
        (= F 0)
        (= D (+ 1 I))
        (new9 H E B)
        (new10 I)
      )
      (diff_new8 A B C D E B F G H E I)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (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 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) )
    (=>
      (and
        (= K 1)
        (= L 1)
        (= A true)
        (= B true)
        (= A true)
        (= A true)
        (= B true)
        (= A true)
        (>= M 0)
        (>= N 0)
        (>= O 0)
        (>= P 0)
        (>= Q 0)
        (>= P 0)
        (<= R S)
        (<= T U)
        (<= V S)
        (<= W X)
        (<= Y (- Z 1))
        (= A1 (+ 1 V))
        (= B1 (+ 1 R))
        (= B1 (+ 1 W))
        (= C1 (+ 1 T))
        (= D1 (+ N M))
        (= E1 (+ P O))
        (= F1 (+ P Q))
        (= I (+ 1 D1))
        (= H (+ 1 T))
        (= G (+ 1 E1))
        (= F (+ 1 V))
        (= E (+ 1 F1))
        (= D (+ 1 J))
        (new13 X P A S)
        (new14 W Q A R C1 Y O A V N M B B U T)
        (new10 J)
      )
      (diff_new8 A B C D E A F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (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 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) )
    (=>
      (and
        (= K 0)
        (= L 1)
        (= A true)
        (= B true)
        (= A true)
        (= A true)
        (= B true)
        (= A true)
        (>= M (+ N 1))
        (>= O 0)
        (>= P 0)
        (>= Q 0)
        (>= R 0)
        (>= R 0)
        (>= S 0)
        (<= T U)
        (<= V W)
        (<= X T)
        (<= Y (- Z 1))
        (= A1 (+ 1 X))
        (= B1 (+ 1 T))
        (= B1 (+ 1 N))
        (= C1 (+ 1 V))
        (= D1 (+ P O))
        (= E1 (+ R Q))
        (= F1 (+ S R))
        (= I (+ 1 D1))
        (= H (+ 1 V))
        (= G (+ 1 E1))
        (= F (+ 1 X))
        (= E (+ 1 F1))
        (= D (+ 1 J))
        (new14 M S A U C1 Y Q A X P O B B W V)
        (new13 N R A T)
        (new10 J)
      )
      (diff_new8 A B C D E A F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (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 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) )
    (=>
      (and
        (= K 1)
        (= L 0)
        (= B true)
        (= B true)
        (= A true)
        (= B true)
        (= B true)
        (= A true)
        (>= M N)
        (>= O 0)
        (>= P 0)
        (>= Q 0)
        (>= R 0)
        (>= S 0)
        (>= P 0)
        (<= T U)
        (<= V U)
        (<= W X)
        (<= Y Z)
        (= A1 (+ 1 V))
        (= B1 (+ 1 T))
        (= B1 (+ 1 Y))
        (= C1 (+ 1 W))
        (= D1 (+ P O))
        (= E1 (+ R Q))
        (= F1 (+ P S))
        (= I (+ 1 D1))
        (= H (+ 1 V))
        (= G (+ 1 E1))
        (= F (+ 1 W))
        (= E (+ 1 F1))
        (= D (+ 1 J))
        (new13 Z P B U)
        (new20 Y S B T C1 N R Q A A X W O B V)
        (new10 J)
      )
      (diff_new8 A B C D E B F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (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 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) )
    (=>
      (and
        (= K 0)
        (= L 0)
        (= B true)
        (= B true)
        (= A true)
        (= B true)
        (= B true)
        (= A true)
        (>= M (+ N 1))
        (>= O P)
        (>= Q 0)
        (>= R 0)
        (>= S 0)
        (>= T 0)
        (>= R 0)
        (>= U 0)
        (<= V W)
        (<= X V)
        (<= Y Z)
        (= A1 (+ 1 X))
        (= B1 (+ 1 V))
        (= B1 (+ 1 N))
        (= C1 (+ 1 Y))
        (= D1 (+ R Q))
        (= E1 (+ T S))
        (= F1 (+ U R))
        (= I (+ 1 D1))
        (= H (+ 1 X))
        (= G (+ 1 E1))
        (= F (+ 1 Y))
        (= E (+ 1 F1))
        (= D (+ 1 J))
        (new20 M U B W C1 P T S A A Z Y Q B X)
        (new13 N R B V)
        (new10 J)
      )
      (diff_new8 A B C D E B F G H I J)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new6 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= A (+ 1 B))
        (new6 B)
      )
      (new6 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= B true)
        (= H 0)
        (= G 0)
        (= D (+ 1 I))
        (new26 F E A)
        (new27 I)
      )
      (diff_new5 A B C D E A F E G H I)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= A true)
        (= G 0)
        (= F 0)
        (= D (+ 1 I))
        (new26 H E B)
        (new27 I)
      )
      (diff_new5 A B C D E B F G H E I)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (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 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) )
    (=>
      (and
        (= K 1)
        (= L 1)
        (= A true)
        (= B true)
        (= A true)
        (= A true)
        (= B true)
        (= A true)
        (>= M 0)
        (>= N 0)
        (>= O 0)
        (>= P 0)
        (>= Q 0)
        (>= P 0)
        (<= R S)
        (<= T U)
        (<= V S)
        (<= W X)
        (<= Y (- Z 1))
        (= A1 (+ 1 V))
        (= B1 (+ 1 R))
        (= B1 (+ 1 W))
        (= C1 (+ 1 T))
        (= D1 (+ N M))
        (= E1 (+ P O))
        (= F1 (+ P Q))
        (= I (+ 1 D1))
        (= H (+ 1 T))
        (= G (+ 1 E1))
        (= F (+ 1 V))
        (= E (+ 1 F1))
        (= D (+ 1 J))
        (new30 X P A S)
        (new31 W Q A R C1 Y O A V N M B B U T)
        (new27 J)
      )
      (diff_new5 A B C D E A F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (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 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) )
    (=>
      (and
        (= K 0)
        (= L 1)
        (= A true)
        (= B true)
        (= A true)
        (= A true)
        (= B true)
        (= A true)
        (>= M (+ N 1))
        (>= O 0)
        (>= P 0)
        (>= Q 0)
        (>= R 0)
        (>= R 0)
        (>= S 0)
        (<= T U)
        (<= V W)
        (<= X T)
        (<= Y (- Z 1))
        (= A1 (+ 1 X))
        (= B1 (+ 1 T))
        (= B1 (+ 1 N))
        (= C1 (+ 1 V))
        (= D1 (+ P O))
        (= E1 (+ R Q))
        (= F1 (+ S R))
        (= I (+ 1 D1))
        (= H (+ 1 V))
        (= G (+ 1 E1))
        (= F (+ 1 X))
        (= E (+ 1 F1))
        (= D (+ 1 J))
        (new31 M S A U C1 Y Q A X P O B B W V)
        (new30 N R A T)
        (new27 J)
      )
      (diff_new5 A B C D E A F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (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 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) )
    (=>
      (and
        (= K 1)
        (= L 0)
        (= B true)
        (= B true)
        (= A true)
        (= B true)
        (= B true)
        (= A true)
        (>= M N)
        (>= O 0)
        (>= P 0)
        (>= Q 0)
        (>= R 0)
        (>= S 0)
        (>= P 0)
        (<= T U)
        (<= V U)
        (<= W X)
        (<= Y Z)
        (= A1 (+ 1 V))
        (= B1 (+ 1 T))
        (= B1 (+ 1 Y))
        (= C1 (+ 1 W))
        (= D1 (+ P O))
        (= E1 (+ R Q))
        (= F1 (+ P S))
        (= I (+ 1 D1))
        (= H (+ 1 V))
        (= G (+ 1 E1))
        (= F (+ 1 W))
        (= E (+ 1 F1))
        (= D (+ 1 J))
        (new30 Z P B U)
        (new37 Y S B T C1 N R Q A A X W O B V)
        (new27 J)
      )
      (diff_new5 A B C D E B F G H I J)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (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 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) )
    (=>
      (and
        (= K 0)
        (= L 0)
        (= B true)
        (= B true)
        (= A true)
        (= B true)
        (= B true)
        (= A true)
        (>= M (+ N 1))
        (>= O P)
        (>= Q 0)
        (>= R 0)
        (>= S 0)
        (>= T 0)
        (>= R 0)
        (>= U 0)
        (<= V W)
        (<= X V)
        (<= Y Z)
        (= A1 (+ 1 X))
        (= B1 (+ 1 V))
        (= B1 (+ 1 N))
        (= C1 (+ 1 Y))
        (= D1 (+ R Q))
        (= E1 (+ T S))
        (= F1 (+ U R))
        (= I (+ 1 D1))
        (= H (+ 1 X))
        (= G (+ 1 E1))
        (= F (+ 1 Y))
        (= E (+ 1 F1))
        (= D (+ 1 J))
        (new37 M U B W C1 P T S A A Z Y Q B X)
        (new30 N R B V)
        (new27 J)
      )
      (diff_new5 A B C D E B F G H I J)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new3 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= A (+ 1 B))
        (new3 B)
      )
      (new3 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= B 0)
        (new3 A)
      )
      (new2 A B A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Bool) (L Int) (M Int) (N Int) (O Bool) )
    (=>
      (and
        (= D true)
        (>= E 0)
        (>= F 0)
        (<= G H)
        (= I (+ 1 G))
        (= J (+ F E))
        (= B (+ 1 J))
        (diff_new5 D K L M N O H F G E C)
        (new2 A N M O)
      )
      (new2 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= B 0)
        (new6 A)
      )
      (new1 A B A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Bool) (L Int) (M Int) (N Int) (O Bool) )
    (=>
      (and
        (= D true)
        (>= E 0)
        (>= F 0)
        (<= G H)
        (= I (+ 1 G))
        (= J (+ F E))
        (= B (+ 1 J))
        (diff_new8 D K L M N O H F G E C)
        (new1 A N M O)
      )
      (new1 A B C D)
    )
  )
)
(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)
      )
      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)
      )
      ff
    )
  )
)

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