; Automatically generated by map2smt

(set-logic HORN)




(declare-fun new5 (Bool Int) Bool)
(declare-fun new2 (Bool) Bool)
(declare-fun new189 (Int Int Int Bool Int) Bool)
(declare-fun new152 (Int Int Int Int Int) Bool)
(declare-fun new150 (Int Bool Int Int Int) Bool)
(declare-fun new148 (Int Int Int Int) Bool)
(declare-fun new146 (Int Bool Int Int Int Int) Bool)
(declare-fun new140 (Int Int Int Int Bool) Bool)
(declare-fun new139 (Int Int) Bool)
(declare-fun new136 (Int) Bool)
(declare-fun new135 (Int Int Int Bool) Bool)
(declare-fun new126 (Int Int Int Int) Bool)
(declare-fun new124 (Int Bool Int Int) Bool)
(declare-fun new122 (Int Int Int) Bool)
(declare-fun new121 (Int Bool) Bool)
(declare-fun new116 (Int Int Int Int Bool Int) Bool)
(declare-fun new11 (Int) Bool)
(declare-fun new109 (Int Bool Int) Bool)
(declare-fun new1 (Bool Bool) Bool)
(declare-fun diff_new597 (Bool Bool Int) Bool)
(declare-fun diff_new4 (Bool Int Int Bool) Bool)
(declare-fun diff_new138 (Bool Int Bool) Bool)
(declare-fun diff_new133 (Bool Int Bool Int) Bool)
(declare-fun diff_new114 (Bool Int Bool Int) Bool)
(declare-fun diff_new111 (Bool Int Bool Int Int) Bool)
(declare-fun not_fun_diff_new597 () Bool)
(declare-fun constr (Bool) Bool)
(declare-fun not_fun_diff_new138 () Bool)
(declare-fun not_fun_diff_new133 () Bool)
(declare-fun not_fun_diff_new114 () Bool)
(declare-fun not_fun_diff_new111 () Bool)
(declare-fun not_fun_diff_new4 () Bool)
(declare-fun ff () Bool)

(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (diff_new597 A B C)
        (diff_new597 D E F)
        (and (= A D) (or (not (= B E)) (not (= C F))))
      )
      not_fun_diff_new597
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Bool) )
    (=>
      (and
        (diff_new138 A B C)
        (diff_new138 D E F)
        (and (= A D) (or (not (= B E)) (not (= C F))))
      )
      not_fun_diff_new138
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Bool) (F Int) (G Bool) (H Int) )
    (=>
      (and
        (diff_new133 A B C D)
        (diff_new133 E F G H)
        (and (= A E) (or (not (= B F)) (or (not (= C G)) (not (= D H)))))
      )
      not_fun_diff_new133
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Bool) (F Int) (G Bool) (H Int) )
    (=>
      (and
        (diff_new114 A B C D)
        (diff_new114 E F G H)
        (and (= A E) (or (not (= B F)) (or (not (= C G)) (not (= D H)))))
      )
      not_fun_diff_new114
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Bool) (G Int) (H Bool) (I Int) (J Int) )
    (=>
      (and
        (diff_new111 A B C D E)
        (diff_new111 F G H I J)
        (and (= A F) (or (not (= B G)) (or (not (= C H)) (or (not (= D I)) (not (= E J))))))
      )
      not_fun_diff_new111
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Bool) )
    (=>
      (and
        (diff_new4 A B C D)
        (diff_new4 E F G H)
        (and (and (= A E) (and (= B F) (= C G))) (not (= D H)))
      )
      not_fun_diff_new4
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (= A true)
        (= C 0)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (<= C D)
        (<= C D)
        (= E (+ 1 C))
        (= B (+ 1 C))
        (new5 A D)
        (new5 A C)
      )
      (diff_new597 A A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= B (+ 1 C))
        (new11 C)
        (new2 A)
      )
      (diff_new597 A A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (= C (+ 1 D))
        (new5 B D)
        (new2 A)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (= A false)
        (>= D (+ E 1))
        (= C (+ 1 D))
        (new5 A E)
        (new11 D)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= C (+ 1 E))
        (new11 E)
        (new2 A)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= C (+ 1 E))
        (new11 E)
        (new2 A)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (= C (+ 1 D))
        (new2 B)
        (new5 A D)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= B (+ 1 C))
        (new5 A C)
      )
      (diff_new597 A A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (= A false)
        (>= D (+ E 1))
        (= C (+ 1 D))
        (new11 E)
        (new5 A D)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= C (+ 1 E))
        (new5 A E)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= C (+ 1 E))
        (new5 A E)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (= B false)
        (= A false)
        (>= D (+ E 1))
        (= C (+ 1 D))
        (new5 B E)
        (new11 D)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (= B false)
        (= A false)
        (>= D (+ E 1))
        (= C (+ 1 D))
        (new5 B D)
        (new11 E)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (= B false)
        (= A false)
        (>= D (+ E 1))
        (>= D (+ E 1))
        (= C (+ 1 D))
        (new11 E)
        (new11 D)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= B false)
        (= A false)
        (>= D (+ E 1))
        (<= (+ F 1) (+ 1 D))
        (= C (+ 1 D))
        (new11 E)
        (new11 D)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= B false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (= C (+ 1 E))
        (new11 F)
        (new11 E)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= C (+ 1 E))
        (new2 B)
        (new11 E)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= C (+ 1 E))
        (new5 B E)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (= A false)
        (>= D (+ E 1))
        (<= (+ F 1) (+ 1 D))
        (= C (+ 1 D))
        (new11 E)
        (new11 D)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= C (+ 1 E))
        (new11 E)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= C (+ 1 E))
        (new2 B)
        (new11 E)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= C (+ 1 E))
        (new5 B E)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (= C (+ 1 E))
        (new11 F)
        (new11 E)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= C (+ 1 E))
        (new11 E)
      )
      (diff_new597 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= D 0)
        (= A 1)
      )
      (new189 A A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D true)
        (= D true)
        (<= H I)
        (<= J (- C 1))
        (<= K L)
        (= L 0)
        (= A (+ 1 K))
        (= K (+ 1 H))
        (= E (+ 1 H))
        (= B 1)
        (new5 D I)
        (new5 D H)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (<= H (- C 1))
        (<= I J)
        (= J 0)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= B 1)
        (new2 D)
        (new11 K)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (<= H (- C 1))
        (<= I J)
        (= J 0)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= B 1)
        (new5 D K)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (= D false)
        (>= H (+ I 1))
        (<= J (- C 1))
        (<= K L)
        (= L 0)
        (= A (+ 1 K))
        (= E (+ 1 H))
        (= B 1)
        (new11 I)
        (new11 H)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (<= (+ H 1) (+ 1 I))
        (<= J (- C 1))
        (<= H K)
        (= K 0)
        (= A (+ 1 H))
        (= E (+ 1 I))
        (= B 1)
        (new11 I)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (>= H (+ (+ 1 I) 1))
        (<= J (- C 1))
        (<= H K)
        (= K 0)
        (= A (+ 1 H))
        (= E (+ 1 I))
        (= B 1)
        (new11 I)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D true)
        (= D true)
        (>= H (+ I 1))
        (<= J K)
        (<= L (- C 1))
        (= I 0)
        (= M 0)
        (= A (+ 1 M))
        (= H (+ 1 J))
        (= E (+ 1 J))
        (= B 1)
        (new5 D K)
        (new5 D J)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (>= H (+ I 1))
        (<= J (- C 1))
        (= I 0)
        (= K 0)
        (= A (+ 1 K))
        (= E (+ 1 L))
        (= B 1)
        (new2 D)
        (new11 L)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (>= H (+ I 1))
        (<= J (- C 1))
        (= I 0)
        (= K 0)
        (= A (+ 1 K))
        (= E (+ 1 L))
        (= B 1)
        (new5 D L)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (= D false)
        (>= H (+ I 1))
        (>= J (+ K 1))
        (<= L (- C 1))
        (= K 0)
        (= M 0)
        (= A (+ 1 M))
        (= E (+ 1 H))
        (= B 1)
        (new11 I)
        (new11 H)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (>= H (+ I 1))
        (<= (+ H 1) (+ 1 J))
        (<= K (- C 1))
        (= I 0)
        (= L 0)
        (= A (+ 1 L))
        (= E (+ 1 J))
        (= B 1)
        (new11 J)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (>= H (+ I 1))
        (>= H (+ (+ 1 J) 1))
        (<= K (- C 1))
        (= I 0)
        (= L 0)
        (= A (+ 1 L))
        (= E (+ 1 J))
        (= B 1)
        (new11 J)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D true)
        (= D true)
        (>= H C)
        (<= I J)
        (<= K L)
        (= M (+ 1 I))
        (= A (+ 1 K))
        (= E (+ 1 I))
        (= B 1)
        (new109 L D J)
        (new189 K B C D I)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (>= H C)
        (<= I J)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= B 1)
        (new121 J D)
        (new148 I B C K)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (>= H C)
        (<= I J)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= B 1)
        (new136 J)
        (new189 I B C D K)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (= D false)
        (>= H (+ I 1))
        (>= J C)
        (<= K L)
        (= A (+ 1 K))
        (= E (+ 1 H))
        (= B 1)
        (new139 L I)
        (new148 K B C H)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (>= H C)
        (<= (+ I 1) (+ 1 J))
        (<= K L)
        (= A (+ 1 K))
        (= E (+ 1 J))
        (= B 1)
        (new136 L)
        (new148 K B C J)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (>= H (+ (+ 1 I) 1))
        (>= J C)
        (<= K L)
        (= A (+ 1 K))
        (= E (+ 1 I))
        (= B 1)
        (new136 L)
        (new148 K B C I)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D true)
        (= D true)
        (>= H (+ I 1))
        (>= J C)
        (<= K L)
        (= M (+ 1 K))
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= B 1)
        (new189 H B C D K)
        (new109 I D L)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (>= H (+ I 1))
        (>= J C)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= B 1)
        (new148 H B C K)
        (new121 I D)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (>= H (+ I 1))
        (>= J C)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= B 1)
        (new189 H B C D K)
        (new136 I)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (= D false)
        (>= H (+ I 1))
        (>= J (+ K 1))
        (>= L C)
        (= A (+ 1 K))
        (= E (+ 1 H))
        (= B 1)
        (new148 J B C H)
        (new139 K I)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (>= H (+ I 1))
        (>= J C)
        (<= (+ K 1) (+ 1 L))
        (= A (+ 1 I))
        (= E (+ 1 L))
        (= B 1)
        (new148 H B C L)
        (new136 I)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (>= H (+ (+ 1 I) 1))
        (>= J (+ K 1))
        (>= L C)
        (= A (+ 1 K))
        (= E (+ 1 I))
        (= B 1)
        (new148 J B C I)
        (new136 K)
      )
      (new189 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= E 0)
        (= D 0)
        (= A 1)
        (= B (+ 1 E))
      )
      (new152 A B A C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (<= H (- D 1))
        (<= I J)
        (= J 0)
        (= A (+ 1 I))
        (= K (+ 1 L))
        (= E (+ 1 L))
        (= C 1)
        (= B (+ 1 K))
        (new11 L)
      )
      (new152 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (>= H (+ I 1))
        (<= J (- D 1))
        (= I 0)
        (= K 0)
        (= A (+ 1 K))
        (= L 0)
        (= E (+ 1 M))
        (= C 1)
        (= B (+ 1 L))
        (new11 M)
      )
      (new152 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (>= H D)
        (<= I J)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= C 1)
        (= B (+ 1 L))
        (new136 J)
        (new152 I L C D K)
      )
      (new152 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (>= H (+ I 1))
        (>= J D)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= C 1)
        (= B (+ 1 L))
        (new148 H C D K)
        (new139 I L)
      )
      (new152 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (<= E F)
        (= E 0)
        (= F 0)
        (= G 0)
        (= D 0)
        (= A (+ 1 G))
        (= A 1)
      )
      (new150 A B A C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (<= H I)
        (<= J K)
        (<= L (- D 1))
        (<= M N)
        (= J (+ 1 H))
        (= K 0)
        (= N 0)
        (= O (+ 1 H))
        (= A (+ 1 O))
        (= A (+ 1 M))
        (= M (+ 1 H))
        (= E (+ 1 H))
        (= C 1)
        (new5 B I)
        (new5 B H)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= B false)
        (= B false)
        (<= H (- D 1))
        (<= I J)
        (= J 0)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= C 1)
        (new11 K)
        (new2 B)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= B false)
        (= B false)
        (<= H (- D 1))
        (<= I J)
        (= J 0)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= C 1)
        (new5 B K)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= B false)
        (= B false)
        (= B false)
        (>= H (+ I 1))
        (<= J (- D 1))
        (<= K L)
        (= L 0)
        (= A (+ 1 K))
        (= E (+ 1 H))
        (= C 1)
        (new11 I)
        (new11 H)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= B false)
        (= B false)
        (<= (+ H 1) (+ 1 I))
        (<= J (- D 1))
        (<= H K)
        (= K 0)
        (= A (+ 1 H))
        (= E (+ 1 I))
        (= C 1)
        (new11 I)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= B false)
        (= B false)
        (>= H (+ (+ 1 I) 1))
        (<= J (- D 1))
        (<= H K)
        (= K 0)
        (= A (+ 1 H))
        (= E (+ 1 I))
        (= C 1)
        (new11 I)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= B false)
        (= B false)
        (>= H (+ I 1))
        (<= J (- D 1))
        (<= K L)
        (= H (+ 1 M))
        (= I 0)
        (= L 0)
        (= A (+ 1 K))
        (= E (+ 1 M))
        (= C 1)
        (new11 M)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= B false)
        (<= (+ A 1) (+ 1 H))
        (<= I (- D 1))
        (<= J K)
        (= H (+ 1 L))
        (= K 0)
        (= A (+ 1 J))
        (= E (+ 1 L))
        (= C 1)
        (new11 L)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= B false)
        (>= A (+ (+ 1 H) 1))
        (<= I (- D 1))
        (<= J K)
        (= H (+ 1 L))
        (= K 0)
        (= A (+ 1 J))
        (= E (+ 1 L))
        (= C 1)
        (new11 L)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (>= H (+ I 1))
        (<= J K)
        (<= L M)
        (<= N (- D 1))
        (= L 0)
        (= M (+ 1 J))
        (= I 0)
        (= O 0)
        (= P 0)
        (= A (+ 1 O))
        (= A (+ 1 P))
        (= H (+ 1 J))
        (= E (+ 1 J))
        (= C 1)
        (new5 B K)
        (new5 B J)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= B false)
        (= B false)
        (>= H (+ I 1))
        (<= J (- D 1))
        (= I 0)
        (= K 0)
        (= A (+ 1 K))
        (= E (+ 1 L))
        (= C 1)
        (new11 L)
        (new2 B)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= B false)
        (= B false)
        (>= H (+ I 1))
        (<= J (- D 1))
        (= I 0)
        (= K 0)
        (= A (+ 1 K))
        (= E (+ 1 L))
        (= C 1)
        (new5 B L)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= B false)
        (= B false)
        (= B false)
        (>= H (+ I 1))
        (>= J (+ K 1))
        (<= L (- D 1))
        (= K 0)
        (= M 0)
        (= A (+ 1 M))
        (= E (+ 1 H))
        (= C 1)
        (new11 I)
        (new11 H)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= B false)
        (= B false)
        (>= H (+ I 1))
        (<= (+ H 1) (+ 1 J))
        (<= K (- D 1))
        (= I 0)
        (= L 0)
        (= A (+ 1 L))
        (= E (+ 1 J))
        (= C 1)
        (new11 J)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= B false)
        (= B false)
        (>= H (+ I 1))
        (>= H (+ (+ 1 J) 1))
        (<= K (- D 1))
        (= I 0)
        (= L 0)
        (= A (+ 1 L))
        (= E (+ 1 J))
        (= C 1)
        (new11 J)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= B false)
        (= B false)
        (>= H (+ I 1))
        (>= J (+ K 1))
        (<= L (- D 1))
        (= H 0)
        (= I (+ 1 M))
        (= K 0)
        (= N 0)
        (= A (+ 1 N))
        (= E (+ 1 M))
        (= C 1)
        (new11 M)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= B true)
        (= B true)
        (>= H D)
        (<= I J)
        (<= K L)
        (= A (+ 1 I))
        (= A (+ 1 K))
        (= E (+ 1 M))
        (= C 1)
        (new109 L B J)
        (new146 K B I C D M)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= B false)
        (>= H D)
        (<= I J)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= C 1)
        (new121 J B)
        (new148 I C D K)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= B false)
        (>= H D)
        (<= I J)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= C 1)
        (new136 J)
        (new150 I B C D K)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= B false)
        (= B false)
        (>= H (+ I 1))
        (>= J D)
        (<= K L)
        (= A (+ 1 K))
        (= E (+ 1 M))
        (= C 1)
        (new139 L I)
        (new152 K H C D M)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= B false)
        (>= H D)
        (<= (+ A 1) (+ 1 I))
        (<= J K)
        (= A (+ 1 J))
        (= E (+ 1 L))
        (= C 1)
        (new136 K)
        (new152 J I C D L)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= B false)
        (>= A (+ (+ 1 H) 1))
        (>= I D)
        (<= J K)
        (= A (+ 1 J))
        (= E (+ 1 L))
        (= C 1)
        (new136 K)
        (new152 J H C D L)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= B true)
        (= B true)
        (>= H (+ I 1))
        (>= J D)
        (<= K L)
        (= A (+ 1 K))
        (= A (+ 1 I))
        (= E (+ 1 M))
        (= C 1)
        (new146 H B L C D M)
        (new109 I B K)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= B false)
        (>= H (+ I 1))
        (>= J D)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= C 1)
        (new150 H B C D K)
        (new136 I)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= B false)
        (>= H (+ I 1))
        (>= J D)
        (= A (+ 1 I))
        (= E (+ 1 K))
        (= C 1)
        (new148 H C D K)
        (new121 I B)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= B false)
        (= B false)
        (>= H (+ I 1))
        (>= J (+ K 1))
        (>= L D)
        (= A (+ 1 K))
        (= E (+ 1 M))
        (= C 1)
        (new152 J I C D M)
        (new139 K H)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= B false)
        (>= H (+ I 1))
        (>= J D)
        (<= (+ A 1) (+ 1 K))
        (= A (+ 1 I))
        (= E (+ 1 L))
        (= C 1)
        (new148 H C D L)
        (new139 I K)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= B false)
        (>= H (+ I 1))
        (>= A (+ (+ 1 J) 1))
        (>= K D)
        (= A (+ 1 I))
        (= E (+ 1 L))
        (= C 1)
        (new148 H C D L)
        (new139 I J)
      )
      (new150 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (and
        (= C 0)
        (= A 1)
      )
      (new148 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (<= G (- C 1))
        (<= H I)
        (= I 0)
        (= A (+ 1 H))
        (= D (+ 1 J))
        (= B 1)
        (new11 J)
      )
      (new148 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (>= G (+ H 1))
        (<= I (- C 1))
        (= H 0)
        (= J 0)
        (= A (+ 1 J))
        (= D (+ 1 K))
        (= B 1)
        (new11 K)
      )
      (new148 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (>= G C)
        (<= H I)
        (= A (+ 1 H))
        (= D (+ 1 J))
        (= B 1)
        (new136 I)
        (new148 H B C J)
      )
      (new148 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (>= G (+ H 1))
        (>= I C)
        (= A (+ 1 H))
        (= D (+ 1 J))
        (= B 1)
        (new148 G B C J)
        (new136 H)
      )
      (new148 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)
        (= B true)
        (= B true)
        (<= F G)
        (= F 0)
        (= G 0)
        (= H 0)
        (= I 0)
        (= E 0)
        (= A (+ 1 H))
        (= A 1)
        (= C (+ 1 I))
      )
      (new146 A B C A D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (<= I J)
        (<= K L)
        (<= M (- E 1))
        (<= N O)
        (= K (+ 1 I))
        (= L 0)
        (= O 0)
        (= P (+ 1 I))
        (= A (+ 1 P))
        (= A (+ 1 N))
        (= N (+ 1 I))
        (= Q (+ 1 I))
        (= F (+ 1 I))
        (= D 1)
        (= C (+ 1 Q))
        (new5 B J)
        (new5 B I)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= B false)
        (= B false)
        (<= I (- E 1))
        (<= J K)
        (= K 0)
        (= A (+ 1 J))
        (= L (+ 1 M))
        (= F (+ 1 M))
        (= D 1)
        (= C (+ 1 L))
        (new2 B)
        (new11 M)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= B false)
        (= B false)
        (<= I (- E 1))
        (<= J K)
        (= K 0)
        (= A (+ 1 J))
        (= L (+ 1 M))
        (= F (+ 1 M))
        (= D 1)
        (= C (+ 1 L))
        (new5 B M)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= B false)
        (= B false)
        (= B false)
        (>= I (+ J 1))
        (<= K (- E 1))
        (<= L M)
        (= M 0)
        (= A (+ 1 L))
        (= N (+ 1 I))
        (= F (+ 1 I))
        (= D 1)
        (= C (+ 1 N))
        (new11 J)
        (new11 I)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= B false)
        (= B false)
        (<= (+ I 1) (+ 1 J))
        (<= K (- E 1))
        (<= I L)
        (= L 0)
        (= A (+ 1 I))
        (= M (+ 1 J))
        (= F (+ 1 J))
        (= D 1)
        (= C (+ 1 M))
        (new11 J)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= B false)
        (= B false)
        (>= I (+ (+ 1 J) 1))
        (<= K (- E 1))
        (<= I L)
        (= L 0)
        (= A (+ 1 I))
        (= M (+ 1 J))
        (= F (+ 1 J))
        (= D 1)
        (= C (+ 1 M))
        (new11 J)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= B false)
        (= B false)
        (>= I (+ J 1))
        (<= K (- E 1))
        (<= L M)
        (= I (+ 1 N))
        (= J 0)
        (= M 0)
        (= A (+ 1 L))
        (= O (+ 1 N))
        (= F (+ 1 N))
        (= D 1)
        (= C (+ 1 O))
        (new11 N)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= B false)
        (<= (+ A 1) (+ 1 I))
        (<= J (- E 1))
        (<= K L)
        (= I (+ 1 M))
        (= L 0)
        (= A (+ 1 K))
        (= N (+ 1 M))
        (= F (+ 1 M))
        (= D 1)
        (= C (+ 1 N))
        (new11 M)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= B false)
        (>= A (+ (+ 1 I) 1))
        (<= J (- E 1))
        (<= K L)
        (= I (+ 1 M))
        (= L 0)
        (= A (+ 1 K))
        (= N (+ 1 M))
        (= F (+ 1 M))
        (= D 1)
        (= C (+ 1 N))
        (new11 M)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (>= I (+ J 1))
        (<= K L)
        (<= M N)
        (<= O (- E 1))
        (= M 0)
        (= N (+ 1 K))
        (= J 0)
        (= P 0)
        (= Q 0)
        (= A (+ 1 P))
        (= A (+ 1 Q))
        (= I (+ 1 K))
        (= R 0)
        (= F (+ 1 K))
        (= D 1)
        (= C (+ 1 R))
        (new5 B L)
        (new5 B K)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (= B false)
        (= B false)
        (>= I (+ J 1))
        (<= K (- E 1))
        (= J 0)
        (= L 0)
        (= A (+ 1 L))
        (= M 0)
        (= F (+ 1 N))
        (= D 1)
        (= C (+ 1 M))
        (new11 N)
        (new2 B)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (= B false)
        (= B false)
        (>= I (+ J 1))
        (<= K (- E 1))
        (= J 0)
        (= L 0)
        (= A (+ 1 L))
        (= M 0)
        (= F (+ 1 N))
        (= D 1)
        (= C (+ 1 M))
        (new5 B N)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (= B false)
        (= B false)
        (= B false)
        (>= I (+ J 1))
        (>= K (+ L 1))
        (<= M (- E 1))
        (= L 0)
        (= N 0)
        (= A (+ 1 N))
        (= O 0)
        (= F (+ 1 I))
        (= D 1)
        (= C (+ 1 O))
        (new11 J)
        (new11 I)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (= B false)
        (= B false)
        (>= I (+ J 1))
        (<= (+ I 1) (+ 1 K))
        (<= L (- E 1))
        (= J 0)
        (= M 0)
        (= A (+ 1 M))
        (= N 0)
        (= F (+ 1 K))
        (= D 1)
        (= C (+ 1 N))
        (new11 K)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (= B false)
        (= B false)
        (>= I (+ J 1))
        (>= I (+ (+ 1 K) 1))
        (<= L (- E 1))
        (= J 0)
        (= M 0)
        (= A (+ 1 M))
        (= N 0)
        (= F (+ 1 K))
        (= D 1)
        (= C (+ 1 N))
        (new11 K)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (= B false)
        (= B false)
        (>= I (+ J 1))
        (>= K (+ L 1))
        (<= M (- E 1))
        (= I 0)
        (= J (+ 1 N))
        (= L 0)
        (= O 0)
        (= A (+ 1 O))
        (= P 0)
        (= F (+ 1 N))
        (= D 1)
        (= C (+ 1 P))
        (new11 N)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G true)
        (= H false)
        (= B true)
        (= B true)
        (>= I E)
        (<= J K)
        (<= L M)
        (= A (+ 1 L))
        (= A (+ 1 J))
        (= F (+ 1 N))
        (= D 1)
        (= C (+ 1 J))
        (new109 M B K)
        (new146 L B J D E N)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H false)
        (= B false)
        (>= I E)
        (<= J K)
        (= A (+ 1 J))
        (= F (+ 1 L))
        (= D 1)
        (= C (+ 1 M))
        (new121 K B)
        (new152 J M D E L)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H false)
        (= B false)
        (>= I E)
        (<= J K)
        (= A (+ 1 J))
        (= F (+ 1 L))
        (= D 1)
        (= C (+ 1 M))
        (new136 K)
        (new146 J B M D E L)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G true)
        (= H false)
        (= B false)
        (= B false)
        (>= I (+ J 1))
        (>= K E)
        (<= L M)
        (= A (+ 1 L))
        (= F (+ 1 N))
        (= D 1)
        (= C (+ 1 I))
        (new139 M J)
        (new152 L I D E N)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H false)
        (= B false)
        (>= I E)
        (<= (+ A 1) (+ 1 J))
        (<= K L)
        (= A (+ 1 K))
        (= F (+ 1 M))
        (= D 1)
        (= C (+ 1 J))
        (new136 L)
        (new152 K J D E M)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H false)
        (= B false)
        (>= A (+ (+ 1 I) 1))
        (>= J E)
        (<= K L)
        (= A (+ 1 K))
        (= F (+ 1 M))
        (= D 1)
        (= C (+ 1 I))
        (new136 L)
        (new152 K I D E M)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G false)
        (= H false)
        (= B true)
        (= B true)
        (>= I (+ J 1))
        (>= K E)
        (<= L M)
        (= A (+ 1 J))
        (= A (+ 1 L))
        (= F (+ 1 N))
        (= D 1)
        (= C (+ 1 L))
        (new146 I B M D E N)
        (new109 J B L)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G false)
        (= H false)
        (= B false)
        (>= I (+ J 1))
        (>= K E)
        (= A (+ 1 J))
        (= F (+ 1 L))
        (= D 1)
        (= C (+ 1 M))
        (new150 I B D E L)
        (new139 J M)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G false)
        (= H false)
        (= B false)
        (>= I (+ J 1))
        (>= K E)
        (= A (+ 1 J))
        (= F (+ 1 L))
        (= D 1)
        (= C (+ 1 M))
        (new148 I D E L)
        (new109 J B M)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G false)
        (= H false)
        (= B false)
        (= B false)
        (>= I (+ J 1))
        (>= K (+ L 1))
        (>= M E)
        (= A (+ 1 L))
        (= F (+ 1 N))
        (= D 1)
        (= C (+ 1 I))
        (new152 K J D E N)
        (new139 L I)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G false)
        (= H false)
        (= B false)
        (>= I (+ J 1))
        (>= K E)
        (<= (+ A 1) (+ 1 L))
        (= A (+ 1 J))
        (= F (+ 1 M))
        (= D 1)
        (= C (+ 1 L))
        (new148 I D E M)
        (new139 J L)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G false)
        (= H false)
        (= B false)
        (>= I (+ J 1))
        (>= A (+ (+ 1 K) 1))
        (>= L E)
        (= A (+ 1 J))
        (= F (+ 1 M))
        (= D 1)
        (= C (+ 1 K))
        (new148 I D E M)
        (new139 J K)
      )
      (new146 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= E 0)
        (= A 1)
        (= B (+ 1 E))
      )
      (new140 A B A C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= E true)
        (= E true)
        (<= H I)
        (<= J (- D 1))
        (<= K L)
        (= L 0)
        (= A (+ 1 K))
        (= K (+ 1 H))
        (= M (+ 1 H))
        (= C 1)
        (= B (+ 1 M))
        (new5 E I)
        (new5 E H)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= E false)
        (<= H (- D 1))
        (<= I J)
        (= J 0)
        (= A (+ 1 I))
        (= K (+ 1 L))
        (= C 1)
        (= B (+ 1 K))
        (new2 E)
        (new11 L)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= E false)
        (<= H (- D 1))
        (<= I J)
        (= J 0)
        (= A (+ 1 I))
        (= K (+ 1 L))
        (= C 1)
        (= B (+ 1 K))
        (new5 E L)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= E false)
        (= E false)
        (>= H (+ I 1))
        (<= J (- D 1))
        (<= K L)
        (= L 0)
        (= A (+ 1 K))
        (= M (+ 1 H))
        (= C 1)
        (= B (+ 1 M))
        (new11 I)
        (new11 H)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= E false)
        (<= (+ H 1) (+ 1 I))
        (<= J (- D 1))
        (<= H K)
        (= K 0)
        (= A (+ 1 H))
        (= L (+ 1 I))
        (= C 1)
        (= B (+ 1 L))
        (new11 I)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= E false)
        (>= H (+ (+ 1 I) 1))
        (<= J (- D 1))
        (<= H K)
        (= K 0)
        (= A (+ 1 H))
        (= L (+ 1 I))
        (= C 1)
        (= B (+ 1 L))
        (new11 I)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= E true)
        (= E true)
        (>= H (+ I 1))
        (<= J K)
        (<= L (- D 1))
        (= I 0)
        (= M 0)
        (= A (+ 1 M))
        (= H (+ 1 J))
        (= N 0)
        (= C 1)
        (= B (+ 1 N))
        (new5 E K)
        (new5 E J)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= E false)
        (>= H (+ I 1))
        (<= J (- D 1))
        (= I 0)
        (= K 0)
        (= A (+ 1 K))
        (= L 0)
        (= C 1)
        (= B (+ 1 L))
        (new2 E)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= E false)
        (>= H (+ I 1))
        (<= J (- D 1))
        (= I 0)
        (= K 0)
        (= A (+ 1 K))
        (= L 0)
        (= C 1)
        (= B (+ 1 L))
        (new2 E)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= E false)
        (= E false)
        (>= H (+ I 1))
        (>= J (+ K 1))
        (<= L (- D 1))
        (= K 0)
        (= M 0)
        (= A (+ 1 M))
        (= N 0)
        (= C 1)
        (= B (+ 1 N))
        (new11 I)
        (new11 H)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= E false)
        (>= H (+ I 1))
        (<= (+ H 1) (+ 1 J))
        (<= K (- D 1))
        (= I 0)
        (= L 0)
        (= A (+ 1 L))
        (= M 0)
        (= C 1)
        (= B (+ 1 M))
        (new11 J)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= E false)
        (>= H (+ I 1))
        (>= H (+ (+ 1 J) 1))
        (<= K (- D 1))
        (= I 0)
        (= L 0)
        (= A (+ 1 L))
        (= M 0)
        (= C 1)
        (= B (+ 1 M))
        (new11 J)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= E true)
        (= E true)
        (>= H D)
        (<= I J)
        (<= K L)
        (= M (+ 1 I))
        (= A (+ 1 K))
        (= C 1)
        (= B (+ 1 N))
        (new109 L E J)
        (new116 K N C D E I)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= E false)
        (>= H D)
        (<= I J)
        (= A (+ 1 I))
        (= C 1)
        (= B (+ 1 K))
        (new121 J E)
        (new126 I K C D)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= E false)
        (>= H D)
        (<= I J)
        (= A (+ 1 I))
        (= C 1)
        (= B (+ 1 K))
        (new136 J)
        (new140 I K C D E)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= E false)
        (= E false)
        (>= H (+ I 1))
        (>= J D)
        (<= K L)
        (= A (+ 1 K))
        (= C 1)
        (= B (+ 1 M))
        (new139 L I)
        (new152 K M C D H)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= E false)
        (>= H D)
        (<= (+ I 1) (+ 1 J))
        (<= K L)
        (= A (+ 1 K))
        (= C 1)
        (= B (+ 1 M))
        (new136 L)
        (new152 K M C D J)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= E false)
        (>= H (+ (+ 1 I) 1))
        (>= J D)
        (<= K L)
        (= A (+ 1 K))
        (= C 1)
        (= B (+ 1 M))
        (new136 L)
        (new152 K M C D I)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= E true)
        (= E true)
        (>= H (+ I 1))
        (>= J D)
        (<= K L)
        (= M (+ 1 K))
        (= A (+ 1 I))
        (= C 1)
        (= B (+ 1 L))
        (new189 H C D E K)
        (new109 I E L)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= E false)
        (>= H (+ I 1))
        (>= J D)
        (= A (+ 1 I))
        (= C 1)
        (= B (+ 1 K))
        (new122 H C D)
        (new109 I E K)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= E false)
        (>= H (+ I 1))
        (>= J D)
        (= A (+ 1 I))
        (= C 1)
        (= B (+ 1 K))
        (new135 H C D E)
        (new139 I K)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= E false)
        (= E false)
        (>= H (+ I 1))
        (>= J (+ K 1))
        (>= L D)
        (= A (+ 1 K))
        (= C 1)
        (= B (+ 1 I))
        (new148 J C D H)
        (new139 K I)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= E false)
        (>= H (+ I 1))
        (>= J D)
        (<= (+ K 1) (+ 1 L))
        (= A (+ 1 I))
        (= C 1)
        (= B (+ 1 M))
        (new148 H C D L)
        (new139 I M)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= E false)
        (>= H (+ (+ 1 I) 1))
        (>= J (+ K 1))
        (>= L D)
        (= A (+ 1 K))
        (= C 1)
        (= B (+ 1 M))
        (new148 J C D I)
        (new139 K M)
      )
      (new140 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= B 0)
        (= A 0)
      )
      (new139 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (and
        (= B (+ 1 C))
        (new11 C)
      )
      (new139 A B)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new136 A)
    )
  )
)
(assert
  (forall ( (A Int) )
    (new136 A)
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= A true)
        (= B 0)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (<= C D)
        (<= C D)
        (= B (+ 1 C))
        (new5 A D)
        (new5 A C)
      )
      (diff_new138 A B A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (new2 A)
      )
      (diff_new138 A B A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
        (new2 C)
        (new2 A)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (new5 A E)
        (new11 D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 D))
        (new11 D)
        (new2 A)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 D) 1))
        (new11 D)
        (new2 A)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
        (new2 C)
        (new2 A)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (new2 A)
      )
      (diff_new138 A B A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (new11 E)
        (new5 A D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 D))
        (new5 A D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 D) 1))
        (new5 A D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (new5 C E)
        (new11 D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (new5 C D)
        (new11 E)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (>= D (+ E 1))
        (new11 E)
        (new11 D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (<= (+ B 1) (+ 1 D))
        (new11 E)
        (new11 D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= B (+ (+ 1 D) 1))
        (>= D (+ E 1))
        (new11 E)
        (new11 D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 D))
        (new2 C)
        (new11 D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 D))
        (new5 C D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (<= (+ B 1) (+ 1 D))
        (new11 E)
        (new11 D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 D))
        (new11 D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 D) 1))
        (new2 C)
        (new11 D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 D) 1))
        (new5 C D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= B (+ (+ 1 D) 1))
        (>= D (+ E 1))
        (new11 E)
        (new11 D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 D) 1))
        (new11 D)
      )
      (diff_new138 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= A 1)
      )
      (new135 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D true)
        (= D true)
        (<= G H)
        (<= I (- C 1))
        (<= J K)
        (= K 0)
        (= A (+ 1 J))
        (= J (+ 1 G))
        (= B 1)
        (new5 D H)
        (new5 D G)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (<= G (- C 1))
        (<= H I)
        (= I 0)
        (= A (+ 1 H))
        (= B 1)
        (new2 D)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (<= G (- C 1))
        (<= H I)
        (= I 0)
        (= A (+ 1 H))
        (= B 1)
        (new2 D)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (>= G (+ H 1))
        (<= I (- C 1))
        (<= J K)
        (= K 0)
        (= A (+ 1 J))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (<= (+ G 1) (+ 1 H))
        (<= I (- C 1))
        (<= G J)
        (= J 0)
        (= A (+ 1 G))
        (= B 1)
        (new11 H)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (>= G (+ (+ 1 H) 1))
        (<= I (- C 1))
        (<= G J)
        (= J 0)
        (= A (+ 1 G))
        (= B 1)
        (new11 H)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D true)
        (= D true)
        (>= G (+ H 1))
        (<= I J)
        (<= K (- C 1))
        (= H 0)
        (= L 0)
        (= A (+ 1 L))
        (= G (+ 1 I))
        (= B 1)
        (new5 D J)
        (new5 D I)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (>= G (+ H 1))
        (<= I (- C 1))
        (= H 0)
        (= J 0)
        (= A (+ 1 J))
        (= B 1)
        (new2 D)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (>= G (+ H 1))
        (<= I (- C 1))
        (= H 0)
        (= J 0)
        (= A (+ 1 J))
        (= B 1)
        (new2 D)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (<= K (- C 1))
        (= J 0)
        (= L 0)
        (= A (+ 1 L))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (>= G (+ H 1))
        (<= (+ G 1) (+ 1 I))
        (<= J (- C 1))
        (= H 0)
        (= K 0)
        (= A (+ 1 K))
        (= B 1)
        (new11 I)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (>= G (+ H 1))
        (>= G (+ (+ 1 I) 1))
        (<= J (- C 1))
        (= H 0)
        (= K 0)
        (= A (+ 1 K))
        (= B 1)
        (new11 I)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D true)
        (= D true)
        (>= G C)
        (<= H I)
        (<= J K)
        (= L (+ 1 H))
        (= A (+ 1 J))
        (= B 1)
        (new109 K D I)
        (new189 J B C D H)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (>= G C)
        (<= H I)
        (= A (+ 1 H))
        (= B 1)
        (new121 I D)
        (new122 H B C)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (>= G C)
        (<= H I)
        (= A (+ 1 H))
        (= B 1)
        (new136 I)
        (new135 H B C D)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= D false)
        (>= G (+ H 1))
        (>= I C)
        (<= J K)
        (= A (+ 1 J))
        (= B 1)
        (new139 K H)
        (new148 J B C G)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (>= G C)
        (<= (+ H 1) (+ 1 I))
        (<= J K)
        (= A (+ 1 J))
        (= B 1)
        (new136 K)
        (new148 J B C I)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (>= G (+ (+ 1 H) 1))
        (>= I C)
        (<= J K)
        (= A (+ 1 J))
        (= B 1)
        (new136 K)
        (new148 J B C H)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D true)
        (= D true)
        (>= G (+ H 1))
        (>= I C)
        (<= J K)
        (= L (+ 1 J))
        (= A (+ 1 H))
        (= B 1)
        (new189 G B C D J)
        (new109 H D K)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (>= G (+ H 1))
        (>= I C)
        (= A (+ 1 H))
        (= B 1)
        (new122 G B C)
        (new121 H D)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (>= G (+ H 1))
        (>= I C)
        (= A (+ 1 H))
        (= B 1)
        (new135 G B C D)
        (new136 H)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= D false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= K C)
        (= A (+ 1 J))
        (= B 1)
        (new148 I B C G)
        (new139 J H)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (>= G (+ H 1))
        (>= I C)
        (<= (+ J 1) (+ 1 K))
        (= A (+ 1 H))
        (= B 1)
        (new148 G B C K)
        (new136 H)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (>= G (+ (+ 1 H) 1))
        (>= I (+ J 1))
        (>= K C)
        (= A (+ 1 J))
        (= B 1)
        (new148 I B C H)
        (new136 J)
      )
      (new135 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= A true)
        (= D 0)
        (= B 0)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (<= D E)
        (<= D E)
        (= B (+ 1 D))
        (= C (+ 1 D))
        (new5 A E)
        (new5 A D)
      )
      (diff_new133 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (new11 D)
        (new2 A)
      )
      (diff_new133 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (new5 C E)
        (new2 A)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (= D (+ 1 E))
        (new5 A F)
        (new11 E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 E))
        (new11 E)
        (new2 A)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D (+ 1 E))
        (new11 E)
        (new2 A)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (new2 C)
        (new5 A E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (new5 A D)
      )
      (diff_new133 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (= D (+ 1 E))
        (new11 F)
        (new5 A E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 E))
        (new5 A E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D (+ 1 E))
        (new5 A E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (= D (+ 1 E))
        (new5 C F)
        (new11 E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (= D (+ 1 E))
        (new5 C E)
        (new11 F)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (>= E (+ F 1))
        (= D (+ 1 E))
        (new11 F)
        (new11 E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 E))
        (new11 F)
        (new11 E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (= D (+ 1 E))
        (new11 F)
        (new11 E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 E))
        (new2 C)
        (new11 E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 E))
        (new5 C E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 E))
        (new11 F)
        (new11 E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 E))
        (new11 E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D (+ 1 E))
        (new2 C)
        (new11 E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D (+ 1 E))
        (new5 C E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (= D (+ 1 E))
        (new11 F)
        (new11 E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D (+ 1 E))
        (new11 E)
      )
      (diff_new133 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= D 0)
        (= A 1)
        (= B (+ 1 D))
      )
      (new126 A B A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (<= G (- D 1))
        (<= H I)
        (= I 0)
        (= A (+ 1 H))
        (= J (+ 1 K))
        (= C 1)
        (= B (+ 1 J))
        (new11 K)
      )
      (new126 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (>= G (+ H 1))
        (<= I (- D 1))
        (= H 0)
        (= J 0)
        (= A (+ 1 J))
        (= K 0)
        (= C 1)
        (= B (+ 1 K))
      )
      (new126 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (>= G D)
        (<= H I)
        (= A (+ 1 H))
        (= C 1)
        (= B (+ 1 J))
        (new136 I)
        (new126 H J C D)
      )
      (new126 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (>= G (+ H 1))
        (>= I D)
        (= A (+ 1 H))
        (= C 1)
        (= B (+ 1 J))
        (new122 G C D)
        (new139 H J)
      )
      (new126 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (<= D E)
        (= D 0)
        (= E 0)
        (= F 0)
        (= A (+ 1 F))
        (= A 1)
      )
      (new124 A B A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (<= G H)
        (<= I J)
        (<= K (- D 1))
        (<= L M)
        (= I (+ 1 G))
        (= J 0)
        (= M 0)
        (= N (+ 1 G))
        (= A (+ 1 N))
        (= A (+ 1 L))
        (= L (+ 1 G))
        (= C 1)
        (new5 B H)
        (new5 B G)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= B false)
        (= B false)
        (<= G (- D 1))
        (<= H I)
        (= I 0)
        (= A (+ 1 H))
        (= C 1)
        (new2 B)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= B false)
        (= B false)
        (<= G (- D 1))
        (<= H I)
        (= I 0)
        (= A (+ 1 H))
        (= C 1)
        (new2 B)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= B false)
        (= B false)
        (= B false)
        (>= G (+ H 1))
        (<= I (- D 1))
        (<= J K)
        (= K 0)
        (= A (+ 1 J))
        (= C 1)
        (new11 H)
        (new11 G)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= B false)
        (= B false)
        (<= (+ G 1) (+ 1 H))
        (<= I (- D 1))
        (<= G J)
        (= J 0)
        (= A (+ 1 G))
        (= C 1)
        (new11 H)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= B false)
        (= B false)
        (>= G (+ (+ 1 H) 1))
        (<= I (- D 1))
        (<= G J)
        (= J 0)
        (= A (+ 1 G))
        (= C 1)
        (new11 H)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= B false)
        (= B false)
        (>= G (+ H 1))
        (<= I (- D 1))
        (<= J K)
        (= G (+ 1 L))
        (= H 0)
        (= K 0)
        (= A (+ 1 J))
        (= C 1)
        (new11 L)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= B false)
        (<= (+ A 1) (+ 1 G))
        (<= H (- D 1))
        (<= I J)
        (= G (+ 1 K))
        (= J 0)
        (= A (+ 1 I))
        (= C 1)
        (new11 K)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= B false)
        (>= A (+ (+ 1 G) 1))
        (<= H (- D 1))
        (<= I J)
        (= G (+ 1 K))
        (= J 0)
        (= A (+ 1 I))
        (= C 1)
        (new11 K)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (= B true)
        (>= G (+ H 1))
        (<= I J)
        (<= K L)
        (<= M (- D 1))
        (= K 0)
        (= L (+ 1 I))
        (= H 0)
        (= N 0)
        (= O 0)
        (= A (+ 1 N))
        (= A (+ 1 O))
        (= G (+ 1 I))
        (= C 1)
        (new5 B J)
        (new5 B I)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= B false)
        (= B false)
        (>= G (+ H 1))
        (<= I (- D 1))
        (= H 0)
        (= J 0)
        (= A (+ 1 J))
        (= C 1)
        (new2 B)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= B false)
        (= B false)
        (>= G (+ H 1))
        (<= I (- D 1))
        (= H 0)
        (= J 0)
        (= A (+ 1 J))
        (= C 1)
        (new2 B)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= B false)
        (= B false)
        (= B false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (<= K (- D 1))
        (= J 0)
        (= L 0)
        (= A (+ 1 L))
        (= C 1)
        (new11 H)
        (new11 G)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= B false)
        (= B false)
        (>= G (+ H 1))
        (<= (+ G 1) (+ 1 I))
        (<= J (- D 1))
        (= H 0)
        (= K 0)
        (= A (+ 1 K))
        (= C 1)
        (new11 I)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= B false)
        (= B false)
        (>= G (+ H 1))
        (>= G (+ (+ 1 I) 1))
        (<= J (- D 1))
        (= H 0)
        (= K 0)
        (= A (+ 1 K))
        (= C 1)
        (new11 I)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= B false)
        (= B false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (<= K (- D 1))
        (= G 0)
        (= H (+ 1 L))
        (= J 0)
        (= M 0)
        (= A (+ 1 M))
        (= C 1)
        (new11 L)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Bool) )
    (=>
      (and
        (= E true)
        (= F false)
        (= B true)
        (>= G D)
        (<= H I)
        (<= J K)
        (= C 1)
        (= A (+ 1 H))
        (= A (+ 1 J))
        (diff_new597 L B H)
        (new109 K B I)
        (new124 J L C D)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= B false)
        (>= G D)
        (<= H I)
        (= A (+ 1 H))
        (= C 1)
        (new121 I B)
        (new122 H C D)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= B false)
        (>= G D)
        (<= H I)
        (= A (+ 1 H))
        (= C 1)
        (new136 I)
        (new124 H B C D)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= B false)
        (= B false)
        (>= G (+ H 1))
        (>= I D)
        (<= J K)
        (= A (+ 1 J))
        (= C 1)
        (new139 K H)
        (new126 J G C D)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= B false)
        (>= G D)
        (<= (+ A 1) (+ 1 H))
        (<= I J)
        (= A (+ 1 I))
        (= C 1)
        (new136 J)
        (new126 I H C D)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= B false)
        (>= A (+ (+ 1 G) 1))
        (>= H D)
        (<= I J)
        (= A (+ 1 I))
        (= C 1)
        (new136 J)
        (new126 I G C D)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Bool) )
    (=>
      (and
        (= E false)
        (= F false)
        (= B true)
        (>= G D)
        (>= H (+ I 1))
        (<= J K)
        (= C 1)
        (= A (+ 1 J))
        (= A (+ 1 I))
        (diff_new597 L B K)
        (new124 H L C D)
        (new109 I B J)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= B false)
        (>= G (+ H 1))
        (>= I D)
        (= A (+ 1 H))
        (= C 1)
        (new124 G B C D)
        (new136 H)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= B false)
        (>= G (+ H 1))
        (>= I D)
        (= A (+ 1 H))
        (= C 1)
        (new122 G C D)
        (new121 H B)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= B false)
        (= B false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= K D)
        (= A (+ 1 J))
        (= C 1)
        (new126 I H C D)
        (new139 J G)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= B false)
        (>= G (+ H 1))
        (>= I D)
        (<= (+ A 1) (+ 1 J))
        (= A (+ 1 H))
        (= C 1)
        (new122 G C D)
        (new139 H J)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= B false)
        (>= G (+ H 1))
        (>= A (+ (+ 1 I) 1))
        (>= J D)
        (= A (+ 1 H))
        (= C 1)
        (new122 G C D)
        (new139 H I)
      )
      (new124 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (= A 1)
      (new122 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= D true)
        (= E true)
        (<= F (- C 1))
        (<= G H)
        (= H 0)
        (= A (+ 1 G))
        (= B 1)
      )
      (new122 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= D false)
        (= E true)
        (>= F (+ G 1))
        (<= H (- C 1))
        (= G 0)
        (= I 0)
        (= A (+ 1 I))
        (= B 1)
      )
      (new122 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= D true)
        (= E false)
        (>= F C)
        (<= G H)
        (= A (+ 1 G))
        (= B 1)
        (new136 H)
        (new122 G B C)
      )
      (new122 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= D false)
        (= E false)
        (>= F (+ G 1))
        (>= H C)
        (= A (+ 1 G))
        (= B 1)
        (new122 F B C)
        (new136 G)
      )
      (new122 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (= A 0)
      )
      (new121 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (<= C D)
        (= A (+ 1 C))
        (new5 B D)
        (new5 B C)
      )
      (new121 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B false)
        (new2 B)
      )
      (new121 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B false)
        (new2 B)
      )
      (new121 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= C (+ D 1))
        (new11 D)
        (new11 C)
      )
      (new121 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (+ A 1) (+ 1 C))
        (new11 C)
      )
      (new121 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= A (+ (+ 1 C) 1))
        (new11 C)
      )
      (new121 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Int) )
    (=>
      (and
        (= D true)
        (= F 0)
        (= E 0)
        (= A 1)
        (= B (+ 1 F))
      )
      (new116 A B A C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= E true)
        (= E true)
        (<= I J)
        (<= K (- D 1))
        (<= L M)
        (= M 0)
        (= A (+ 1 L))
        (= L (+ 1 I))
        (= N (+ 1 I))
        (= F (+ 1 I))
        (= C 1)
        (= B (+ 1 N))
        (new5 E J)
        (new5 E I)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= E false)
        (<= I (- D 1))
        (<= J K)
        (= K 0)
        (= A (+ 1 J))
        (= L (+ 1 M))
        (= F (+ 1 M))
        (= C 1)
        (= B (+ 1 L))
        (new2 E)
        (new11 M)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= E false)
        (<= I (- D 1))
        (<= J K)
        (= K 0)
        (= A (+ 1 J))
        (= L (+ 1 M))
        (= F (+ 1 M))
        (= C 1)
        (= B (+ 1 L))
        (new5 E M)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= E false)
        (= E false)
        (>= I (+ J 1))
        (<= K (- D 1))
        (<= L M)
        (= M 0)
        (= A (+ 1 L))
        (= N (+ 1 I))
        (= F (+ 1 I))
        (= C 1)
        (= B (+ 1 N))
        (new11 J)
        (new11 I)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= E false)
        (<= (+ I 1) (+ 1 J))
        (<= K (- D 1))
        (<= I L)
        (= L 0)
        (= A (+ 1 I))
        (= M (+ 1 J))
        (= F (+ 1 J))
        (= C 1)
        (= B (+ 1 M))
        (new11 J)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (= E false)
        (>= I (+ (+ 1 J) 1))
        (<= K (- D 1))
        (<= I L)
        (= L 0)
        (= A (+ 1 I))
        (= M (+ 1 J))
        (= F (+ 1 J))
        (= C 1)
        (= B (+ 1 M))
        (new11 J)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (= E true)
        (= E true)
        (>= I (+ J 1))
        (<= K L)
        (<= M (- D 1))
        (= J 0)
        (= N 0)
        (= A (+ 1 N))
        (= I (+ 1 K))
        (= O 0)
        (= F (+ 1 K))
        (= C 1)
        (= B (+ 1 O))
        (new5 E L)
        (new5 E K)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (= E false)
        (>= I (+ J 1))
        (<= K (- D 1))
        (= J 0)
        (= L 0)
        (= A (+ 1 L))
        (= M 0)
        (= F (+ 1 N))
        (= C 1)
        (= B (+ 1 M))
        (new2 E)
        (new11 N)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (= E false)
        (>= I (+ J 1))
        (<= K (- D 1))
        (= J 0)
        (= L 0)
        (= A (+ 1 L))
        (= M 0)
        (= F (+ 1 N))
        (= C 1)
        (= B (+ 1 M))
        (new5 E N)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (= E false)
        (= E false)
        (>= I (+ J 1))
        (>= K (+ L 1))
        (<= M (- D 1))
        (= L 0)
        (= N 0)
        (= A (+ 1 N))
        (= O 0)
        (= F (+ 1 I))
        (= C 1)
        (= B (+ 1 O))
        (new11 J)
        (new11 I)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (= E false)
        (>= I (+ J 1))
        (<= (+ I 1) (+ 1 K))
        (<= L (- D 1))
        (= J 0)
        (= M 0)
        (= A (+ 1 M))
        (= N 0)
        (= F (+ 1 K))
        (= C 1)
        (= B (+ 1 N))
        (new11 K)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (= E false)
        (>= I (+ J 1))
        (>= I (+ (+ 1 K) 1))
        (<= L (- D 1))
        (= J 0)
        (= M 0)
        (= A (+ 1 M))
        (= N 0)
        (= F (+ 1 K))
        (= C 1)
        (= B (+ 1 N))
        (new11 K)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) )
    (=>
      (and
        (= G true)
        (= H false)
        (= E true)
        (= E true)
        (>= I D)
        (<= J K)
        (<= L M)
        (= N (+ 1 J))
        (= A (+ 1 L))
        (= F (+ 1 J))
        (= C 1)
        (= B (+ 1 O))
        (new109 M E K)
        (new116 L O C D E J)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H false)
        (= E false)
        (>= I D)
        (<= J K)
        (= A (+ 1 J))
        (= F (+ 1 L))
        (= C 1)
        (= B (+ 1 M))
        (new121 K E)
        (new152 J M C D L)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G true)
        (= H false)
        (= E false)
        (>= I D)
        (<= J K)
        (= A (+ 1 J))
        (= F (+ 1 L))
        (= C 1)
        (= B (+ 1 M))
        (new136 K)
        (new116 J M C D E L)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G true)
        (= H false)
        (= E false)
        (= E false)
        (>= I (+ J 1))
        (>= K D)
        (<= L M)
        (= A (+ 1 L))
        (= F (+ 1 I))
        (= C 1)
        (= B (+ 1 N))
        (new139 M J)
        (new152 L N C D I)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G true)
        (= H false)
        (= E false)
        (>= I D)
        (<= (+ J 1) (+ 1 K))
        (<= L M)
        (= A (+ 1 L))
        (= F (+ 1 K))
        (= C 1)
        (= B (+ 1 N))
        (new136 M)
        (new152 L N C D K)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G true)
        (= H false)
        (= E false)
        (>= I (+ (+ 1 J) 1))
        (>= K D)
        (<= L M)
        (= A (+ 1 L))
        (= F (+ 1 J))
        (= C 1)
        (= B (+ 1 N))
        (new136 M)
        (new152 L N C D J)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G false)
        (= H false)
        (= E true)
        (= E true)
        (>= I (+ J 1))
        (>= K D)
        (<= L M)
        (= N (+ 1 L))
        (= A (+ 1 J))
        (= F (+ 1 L))
        (= C 1)
        (= B (+ 1 M))
        (new189 I C D E L)
        (new109 J E M)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G false)
        (= H false)
        (= E false)
        (>= I (+ J 1))
        (>= K D)
        (= A (+ 1 J))
        (= F (+ 1 L))
        (= C 1)
        (= B (+ 1 M))
        (new148 I C D L)
        (new109 J E M)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G false)
        (= H false)
        (= E false)
        (>= I (+ J 1))
        (>= K D)
        (= A (+ 1 J))
        (= F (+ 1 L))
        (= C 1)
        (= B (+ 1 M))
        (new189 I C D E L)
        (new139 J M)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= G false)
        (= H false)
        (= E false)
        (= E false)
        (>= I (+ J 1))
        (>= K (+ L 1))
        (>= M D)
        (= A (+ 1 L))
        (= F (+ 1 I))
        (= C 1)
        (= B (+ 1 J))
        (new148 K C D I)
        (new139 L J)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G false)
        (= H false)
        (= E false)
        (>= I (+ J 1))
        (>= K D)
        (<= (+ L 1) (+ 1 M))
        (= A (+ 1 J))
        (= F (+ 1 M))
        (= C 1)
        (= B (+ 1 N))
        (new148 I C D M)
        (new139 J N)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Bool) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= G false)
        (= H false)
        (= E false)
        (>= I (+ (+ 1 J) 1))
        (>= K (+ L 1))
        (>= M D)
        (= A (+ 1 L))
        (= F (+ 1 J))
        (= C 1)
        (= B (+ 1 N))
        (new148 K C D J)
        (new139 L N)
      )
      (new116 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= A true)
        (= D 0)
        (= B 0)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C true)
        (= A true)
        (= D (+ 1 E))
        (= B 0)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (<= D E)
        (<= D E)
        (= B (+ 1 D))
        (= C 0)
        (new5 A E)
        (new5 A D)
      )
      (diff_new114 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (<= D E)
        (<= D E)
        (= B (+ 1 D))
        (= C (+ 1 F))
        (new11 F)
        (new5 A E)
        (new5 A D)
      )
      (diff_new114 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C 0)
        (new2 A)
      )
      (diff_new114 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D 0)
        (new2 C)
        (new2 A)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (= D 0)
        (new5 A F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D 0)
        (new11 E)
        (new2 A)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D 0)
        (new11 E)
        (new2 A)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (new11 D)
        (new2 A)
      )
      (diff_new114 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (new2 C)
        (new11 E)
        (new2 A)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (= D (+ 1 G))
        (new5 A F)
        (new11 E)
        (new11 G)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 F))
        (new11 E)
        (new11 F)
        (new2 A)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D (+ 1 F))
        (new11 E)
        (new11 F)
        (new2 A)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D 0)
        (new2 C)
        (new2 A)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C 0)
        (new2 A)
      )
      (diff_new114 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (= D 0)
        (new11 F)
        (new5 A E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D 0)
        (new5 A E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D 0)
        (new5 A E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (new2 C)
        (new11 E)
        (new2 A)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (new11 D)
        (new2 A)
      )
      (diff_new114 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (= D (+ 1 G))
        (new11 F)
        (new5 A E)
        (new11 G)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 F))
        (new5 A E)
        (new11 F)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D (+ 1 F))
        (new5 A E)
        (new11 F)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (= D 0)
        (new5 C F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (= D 0)
        (new5 C E)
        (new11 F)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (>= E (+ F 1))
        (= D 0)
        (new11 F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (<= (+ B 1) (+ 1 E))
        (= D 0)
        (new11 F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (= D 0)
        (new11 F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (= D (+ 1 G))
        (new5 C F)
        (new11 G)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (= D (+ 1 G))
        (new5 C E)
        (new11 G)
        (new11 F)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (>= E (+ F 1))
        (= D (+ 1 G))
        (new11 G)
        (new11 F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 G))
        (new11 G)
        (new11 F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (= D (+ 1 G))
        (new11 G)
        (new11 F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D 0)
        (new2 C)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D 0)
        (new5 C E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (<= (+ B 1) (+ 1 E))
        (= D 0)
        (new11 F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D 0)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 F))
        (new2 C)
        (new11 F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 F))
        (new5 C E)
        (new11 F)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= E (+ F 1))
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 G))
        (new11 F)
        (new11 G)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 E))
        (= D (+ 1 F))
        (new11 F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D 0)
        (new2 C)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D 0)
        (new5 C E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (= D 0)
        (new11 F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D 0)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D (+ 1 F))
        (new2 C)
        (new11 F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D (+ 1 F))
        (new5 C E)
        (new11 F)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (= D (+ 1 G))
        (new11 F)
        (new11 G)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 E) 1))
        (= D (+ 1 F))
        (new11 F)
        (new11 E)
      )
      (diff_new114 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (= C 0)
        (= A 0)
      )
      (new109 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (<= D E)
        (= A (+ 1 D))
        (= C (+ 1 D))
        (new5 B E)
        (new5 B D)
      )
      (new109 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= C (+ 1 D))
        (new11 D)
        (new2 B)
      )
      (new109 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= C (+ 1 D))
        (new5 B D)
      )
      (new109 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= D (+ E 1))
        (= C (+ 1 D))
        (new11 E)
        (new11 D)
      )
      (new109 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (<= (+ A 1) (+ 1 D))
        (= C (+ 1 D))
        (new11 D)
      )
      (new109 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (>= A (+ (+ 1 D) 1))
        (= C (+ 1 D))
        (new11 D)
      )
      (new109 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C true)
        (= A true)
        (= E 0)
        (= D 0)
        (= B 0)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C true)
        (= A true)
        (= E (+ 1 F))
        (= D 0)
        (= B 0)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (<= E F)
        (<= E F)
        (= B (+ 1 E))
        (= D 0)
        (= C (+ 1 E))
        (new5 A F)
        (new5 A E)
      )
      (diff_new111 A B A C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (<= E F)
        (<= E F)
        (= B (+ 1 E))
        (= D (+ 1 G))
        (= C (+ 1 E))
        (new11 G)
        (new5 A F)
        (new5 A E)
      )
      (diff_new111 A B A C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= D 0)
        (= C (+ 1 E))
        (new11 E)
        (new2 A)
      )
      (diff_new111 A B A C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= E 0)
        (= D (+ 1 F))
        (new5 C F)
        (new2 A)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (= E 0)
        (= D (+ 1 F))
        (new5 A G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 F))
        (= E 0)
        (= D (+ 1 F))
        (new11 F)
        (new2 A)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (= E 0)
        (= D (+ 1 F))
        (new11 F)
        (new2 A)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= D (+ 1 E))
        (= C (+ 1 F))
        (new11 F)
        (new11 E)
        (new2 A)
      )
      (diff_new111 A B A C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= E (+ 1 F))
        (= D (+ 1 G))
        (new5 C G)
        (new11 F)
        (new2 A)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (= E (+ 1 H))
        (= D (+ 1 F))
        (new5 A G)
        (new11 F)
        (new11 H)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 F))
        (= E (+ 1 G))
        (= D (+ 1 F))
        (new11 F)
        (new11 G)
        (new2 A)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (= E (+ 1 G))
        (= D (+ 1 F))
        (new11 F)
        (new11 G)
        (new2 A)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= E 0)
        (= D (+ 1 F))
        (new2 C)
        (new5 A F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= D 0)
        (= C (+ 1 E))
        (new5 A E)
      )
      (diff_new111 A B A C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (= E 0)
        (= D (+ 1 F))
        (new11 G)
        (new5 A F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 F))
        (= E 0)
        (= D (+ 1 F))
        (new5 A F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (= E 0)
        (= D (+ 1 F))
        (new5 A F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= E (+ 1 F))
        (= D (+ 1 G))
        (new2 C)
        (new5 A G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= D (+ 1 E))
        (= C (+ 1 F))
        (new5 A F)
        (new11 E)
      )
      (diff_new111 A B A C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (= E (+ 1 H))
        (= D (+ 1 F))
        (new11 G)
        (new5 A F)
        (new11 H)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 F))
        (= E (+ 1 G))
        (= D (+ 1 F))
        (new5 A F)
        (new11 G)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (= E (+ 1 G))
        (= D (+ 1 F))
        (new5 A F)
        (new11 G)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (= E 0)
        (= D (+ 1 F))
        (new5 C G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (= E 0)
        (= D (+ 1 F))
        (new5 C F)
        (new11 G)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (>= F (+ G 1))
        (= E 0)
        (= D (+ 1 F))
        (new11 G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (<= (+ B 1) (+ 1 F))
        (= E 0)
        (= D (+ 1 F))
        (new11 G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (>= F (+ G 1))
        (= E 0)
        (= D (+ 1 F))
        (new11 G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (= E (+ 1 H))
        (= D (+ 1 F))
        (new5 C G)
        (new11 H)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (= E (+ 1 H))
        (= D (+ 1 F))
        (new5 C F)
        (new11 H)
        (new11 G)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (>= F (+ G 1))
        (= E (+ 1 H))
        (= D (+ 1 F))
        (new11 H)
        (new11 G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (<= (+ B 1) (+ 1 F))
        (= E (+ 1 H))
        (= D (+ 1 F))
        (new11 H)
        (new11 G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (>= F (+ G 1))
        (= E (+ 1 H))
        (= D (+ 1 F))
        (new11 H)
        (new11 G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 F))
        (= E 0)
        (= D (+ 1 F))
        (new2 C)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 F))
        (= E 0)
        (= D (+ 1 F))
        (new5 C F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (<= (+ B 1) (+ 1 F))
        (= E 0)
        (= D (+ 1 F))
        (new11 G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 F))
        (= E 0)
        (= D (+ 1 F))
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 F))
        (= E (+ 1 G))
        (= D (+ 1 F))
        (new2 C)
        (new11 G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 F))
        (= E (+ 1 G))
        (= D (+ 1 F))
        (new5 C F)
        (new11 G)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= F (+ G 1))
        (<= (+ B 1) (+ 1 F))
        (= E (+ 1 H))
        (= D (+ 1 F))
        (new11 G)
        (new11 H)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 F))
        (= E (+ 1 G))
        (= D (+ 1 F))
        (new11 G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (= E 0)
        (= D (+ 1 F))
        (new2 C)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (= E 0)
        (= D (+ 1 F))
        (new5 C F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (>= F (+ G 1))
        (= E 0)
        (= D (+ 1 F))
        (new11 G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (= E 0)
        (= D (+ 1 F))
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (= E (+ 1 G))
        (= D (+ 1 F))
        (new2 C)
        (new11 G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (= E (+ 1 G))
        (= D (+ 1 F))
        (new5 C F)
        (new11 G)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (>= F (+ G 1))
        (= E (+ 1 H))
        (= D (+ 1 F))
        (new11 G)
        (new11 H)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 F) 1))
        (= E (+ 1 G))
        (= D (+ 1 F))
        (new11 G)
        (new11 F)
      )
      (diff_new111 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new11 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= A (+ 1 B))
        (new11 B)
      )
      (new11 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A true)
        (= B 0)
      )
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (<= C D)
        (= E (+ 1 C))
        (= B (+ 1 C))
        (new5 A D)
        (new5 A C)
      )
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= B (+ 1 C))
        (new11 C)
        (new2 A)
      )
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= B (+ 1 C))
        (new5 A C)
      )
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= C (+ D 1))
        (= B (+ 1 C))
        (new11 D)
        (new11 C)
      )
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (<= (+ C 1) (+ 1 D))
        (= B (+ 1 D))
        (new11 D)
      )
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (>= C (+ (+ 1 D) 1))
        (= B (+ 1 D))
        (new11 D)
      )
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= D true)
        (= D true)
        (= D true)
        (= D true)
        (= A true)
        (<= E F)
        (= E 0)
        (= F 0)
        (= G 0)
        (= B (+ 1 G))
        (= B 1)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (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) )
    (=>
      (and
        (= D true)
        (= E true)
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (<= F G)
        (<= H I)
        (<= F G)
        (<= J (- C 1))
        (<= K L)
        (= H (+ 1 F))
        (= I 0)
        (= L 0)
        (= M (+ 1 F))
        (= N (+ 1 M))
        (= N (+ 1 K))
        (= K (+ 1 F))
        (= K (+ 1 F))
        (= B 1)
        (new5 A G)
        (new5 A F)
      )
      (diff_new4 A B C A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= D true)
        (= E true)
        (= A false)
        (= A false)
        (= A false)
        (<= F (- C 1))
        (<= G H)
        (= H 0)
        (= I (+ 1 G))
        (= B 1)
        (new2 A)
      )
      (diff_new4 A B C A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (<= G (- C 1))
        (<= H I)
        (= I 0)
        (= J (+ 1 H))
        (= B 1)
        (new2 A)
        (new2 D)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= I (- C 1))
        (<= J K)
        (= K 0)
        (= L (+ 1 J))
        (= B 1)
        (new5 A H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (<= (+ G 1) (+ 1 H))
        (<= I (- C 1))
        (<= G J)
        (= J 0)
        (= K (+ 1 G))
        (= B 1)
        (new2 A)
        (new11 H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (<= I (- C 1))
        (<= G J)
        (= J 0)
        (= K (+ 1 G))
        (= B 1)
        (new2 A)
        (new11 H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= I (- C 1))
        (<= J K)
        (= G (+ 1 L))
        (= H 0)
        (= K 0)
        (= M (+ 1 J))
        (= B 1)
        (new2 A)
        (new11 L)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= A false)
        (<= (+ G 1) (+ 1 H))
        (<= I (- C 1))
        (<= J K)
        (= H (+ 1 L))
        (= K 0)
        (= G (+ 1 J))
        (= B 1)
        (new2 A)
        (new11 L)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (<= I (- C 1))
        (<= J K)
        (= H (+ 1 L))
        (= K 0)
        (= G (+ 1 J))
        (= B 1)
        (new2 A)
        (new11 L)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (<= G (- C 1))
        (<= H I)
        (= I 0)
        (= J (+ 1 H))
        (= B 1)
        (new2 A)
        (new2 D)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= D true)
        (= E true)
        (= A false)
        (= A false)
        (= A false)
        (<= F (- C 1))
        (<= G H)
        (= H 0)
        (= I (+ 1 G))
        (= B 1)
        (new2 A)
      )
      (diff_new4 A B C A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= I (- C 1))
        (<= J K)
        (= K 0)
        (= L (+ 1 J))
        (= B 1)
        (new5 A G)
        (new11 H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (<= (+ G 1) (+ 1 H))
        (<= I (- C 1))
        (<= G J)
        (= J 0)
        (= K (+ 1 G))
        (= B 1)
        (new5 A H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (<= I (- C 1))
        (<= G J)
        (= J 0)
        (= K (+ 1 G))
        (= B 1)
        (new5 A H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= I (- C 1))
        (<= J K)
        (= G (+ 1 L))
        (= H 0)
        (= K 0)
        (= M (+ 1 J))
        (= B 1)
        (new5 A L)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= A false)
        (<= (+ G 1) (+ 1 H))
        (<= I (- C 1))
        (<= J K)
        (= H (+ 1 L))
        (= K 0)
        (= G (+ 1 J))
        (= B 1)
        (new5 A L)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (<= I (- C 1))
        (<= J K)
        (= H (+ 1 L))
        (= K 0)
        (= G (+ 1 J))
        (= B 1)
        (new5 A L)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= I (- C 1))
        (<= J K)
        (= K 0)
        (= L (+ 1 J))
        (= B 1)
        (new5 D H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= I (- C 1))
        (<= J K)
        (= K 0)
        (= L (+ 1 J))
        (= B 1)
        (new11 H)
        (new5 D G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= G (+ H 1))
        (<= I (- C 1))
        (<= J K)
        (= K 0)
        (= L (+ 1 J))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= (+ I 1) (+ 1 G))
        (<= J (- C 1))
        (<= I K)
        (= K 0)
        (= L (+ 1 I))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ (+ 1 G) 1))
        (<= J (- C 1))
        (<= I K)
        (= K 0)
        (= L (+ 1 I))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (<= K (- C 1))
        (<= L M)
        (= G (+ 1 I))
        (= H 0)
        (= M 0)
        (= N (+ 1 L))
        (= B 1)
        (new11 J)
        (new11 I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= (+ I 1) (+ 1 J))
        (<= K (- C 1))
        (<= L M)
        (= J (+ 1 G))
        (= M 0)
        (= I (+ 1 L))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ (+ 1 J) 1))
        (<= K (- C 1))
        (<= L M)
        (= J (+ 1 G))
        (= M 0)
        (= I (+ 1 L))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (<= (+ G 1) (+ 1 H))
        (<= I (- C 1))
        (<= G J)
        (= J 0)
        (= K (+ 1 G))
        (= B 1)
        (new11 H)
        (new2 D)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (<= (+ G 1) (+ 1 H))
        (<= I (- C 1))
        (<= G J)
        (= J 0)
        (= K (+ 1 G))
        (= B 1)
        (new5 D H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= (+ I 1) (+ 1 G))
        (<= J (- C 1))
        (<= I K)
        (= K 0)
        (= L (+ 1 I))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (<= (+ G 1) (+ 1 H))
        (<= (+ G 1) (+ 1 H))
        (<= I (- C 1))
        (<= G J)
        (= J 0)
        (= K (+ 1 G))
        (= B 1)
        (new11 H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= (+ I 1) (+ 1 J))
        (<= K (- C 1))
        (<= I L)
        (= G (+ 1 J))
        (= H 0)
        (= L 0)
        (= M (+ 1 I))
        (= B 1)
        (new11 J)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= A false)
        (<= (+ G 1) (+ 1 H))
        (<= (+ I 1) (+ 1 J))
        (<= K (- C 1))
        (<= I L)
        (= H (+ 1 J))
        (= L 0)
        (= G (+ 1 I))
        (= B 1)
        (new11 J)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (<= I (- C 1))
        (<= G J)
        (= J 0)
        (= K (+ 1 G))
        (= B 1)
        (new11 H)
        (new2 D)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (<= I (- C 1))
        (<= G J)
        (= J 0)
        (= K (+ 1 G))
        (= B 1)
        (new5 D H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ (+ 1 G) 1))
        (<= J (- C 1))
        (<= I K)
        (= K 0)
        (= L (+ 1 I))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= G (+ (+ 1 H) 1))
        (<= I (- C 1))
        (<= G J)
        (= J 0)
        (= K (+ 1 G))
        (= B 1)
        (new11 H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I (+ (+ 1 J) 1))
        (<= K (- C 1))
        (<= I L)
        (= H (+ 1 J))
        (= L 0)
        (= G (+ 1 I))
        (= B 1)
        (new11 J)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (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) )
    (=>
      (and
        (= D false)
        (= E true)
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (= A true)
        (>= F (+ G 1))
        (<= H I)
        (<= J K)
        (<= H I)
        (<= L (- C 1))
        (= J 0)
        (= K (+ 1 H))
        (= G 0)
        (= M 0)
        (= N 0)
        (= O (+ 1 M))
        (= O (+ 1 N))
        (= F (+ 1 H))
        (= F (+ 1 H))
        (= B 1)
        (new5 A I)
        (new5 A H)
      )
      (diff_new4 A B C A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= D false)
        (= E true)
        (= A false)
        (= A false)
        (= A false)
        (>= F (+ G 1))
        (<= H (- C 1))
        (= G 0)
        (= I 0)
        (= J (+ 1 I))
        (= B 1)
        (new2 A)
      )
      (diff_new4 A B C A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= I (- C 1))
        (= H 0)
        (= J 0)
        (= K (+ 1 J))
        (= B 1)
        (new2 A)
        (new2 D)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (<= K (- C 1))
        (= J 0)
        (= L 0)
        (= M (+ 1 L))
        (= B 1)
        (new5 A H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= (+ G 1) (+ 1 I))
        (<= J (- C 1))
        (= H 0)
        (= K 0)
        (= L (+ 1 K))
        (= B 1)
        (new2 A)
        (new11 I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= G (+ (+ 1 I) 1))
        (<= J (- C 1))
        (= H 0)
        (= K 0)
        (= L (+ 1 K))
        (= B 1)
        (new2 A)
        (new11 I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (<= K (- C 1))
        (= G 0)
        (= H (+ 1 L))
        (= J 0)
        (= M 0)
        (= N (+ 1 M))
        (= B 1)
        (new2 A)
        (new11 L)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= I (- C 1))
        (= H 0)
        (= J 0)
        (= K (+ 1 J))
        (= B 1)
        (new2 A)
        (new2 D)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= D false)
        (= E true)
        (= A false)
        (= A false)
        (= A false)
        (>= F (+ G 1))
        (<= H (- C 1))
        (= G 0)
        (= I 0)
        (= J (+ 1 I))
        (= B 1)
        (new2 A)
      )
      (diff_new4 A B C A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (<= K (- C 1))
        (= J 0)
        (= L 0)
        (= M (+ 1 L))
        (= B 1)
        (new5 A G)
        (new11 H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= (+ G 1) (+ 1 I))
        (<= J (- C 1))
        (= H 0)
        (= K 0)
        (= L (+ 1 K))
        (= B 1)
        (new5 A I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= G (+ (+ 1 I) 1))
        (<= J (- C 1))
        (= H 0)
        (= K 0)
        (= L (+ 1 K))
        (= B 1)
        (new5 A I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (<= K (- C 1))
        (= G 0)
        (= H (+ 1 L))
        (= J 0)
        (= M 0)
        (= N (+ 1 M))
        (= B 1)
        (new5 A L)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (<= K (- C 1))
        (= J 0)
        (= L 0)
        (= M (+ 1 L))
        (= B 1)
        (new5 D H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (<= K (- C 1))
        (= J 0)
        (= L 0)
        (= M (+ 1 L))
        (= B 1)
        (new11 H)
        (new5 D G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= G (+ H 1))
        (>= I (+ J 1))
        (<= K (- C 1))
        (= J 0)
        (= L 0)
        (= M (+ 1 L))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (<= (+ I 1) (+ 1 G))
        (<= K (- C 1))
        (= J 0)
        (= L 0)
        (= M (+ 1 L))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= I (+ (+ 1 G) 1))
        (<= K (- C 1))
        (= J 0)
        (= L 0)
        (= M (+ 1 L))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= K (+ L 1))
        (<= M (- C 1))
        (= G 0)
        (= H (+ 1 I))
        (= L 0)
        (= N 0)
        (= O (+ 1 N))
        (= B 1)
        (new11 J)
        (new11 I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= (+ G 1) (+ 1 I))
        (<= J (- C 1))
        (= H 0)
        (= K 0)
        (= L (+ 1 K))
        (= B 1)
        (new11 I)
        (new2 D)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= (+ G 1) (+ 1 I))
        (<= J (- C 1))
        (= H 0)
        (= K 0)
        (= L (+ 1 K))
        (= B 1)
        (new5 D I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (<= (+ I 1) (+ 1 G))
        (<= K (- C 1))
        (= J 0)
        (= L 0)
        (= M (+ 1 L))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (<= (+ G 1) (+ 1 I))
        (<= (+ G 1) (+ 1 I))
        (<= J (- C 1))
        (= H 0)
        (= K 0)
        (= L (+ 1 K))
        (= B 1)
        (new11 I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= G (+ (+ 1 I) 1))
        (<= J (- C 1))
        (= H 0)
        (= K 0)
        (= L (+ 1 K))
        (= B 1)
        (new11 I)
        (new2 D)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= G (+ (+ 1 I) 1))
        (<= J (- C 1))
        (= H 0)
        (= K 0)
        (= L (+ 1 K))
        (= B 1)
        (new5 D I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= I (+ (+ 1 G) 1))
        (<= K (- C 1))
        (= J 0)
        (= L 0)
        (= M (+ 1 L))
        (= B 1)
        (new11 H)
        (new11 G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= G (+ (+ 1 I) 1))
        (>= G (+ (+ 1 I) 1))
        (<= J (- C 1))
        (= H 0)
        (= K 0)
        (= L (+ 1 K))
        (= B 1)
        (new11 I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= I (+ (+ 1 K) 1))
        (<= L (- C 1))
        (= G 0)
        (= H (+ 1 K))
        (= J 0)
        (= M 0)
        (= N (+ 1 M))
        (= B 1)
        (new11 K)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (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 Bool) )
    (=>
      (and
        (= D true)
        (= E false)
        (= A true)
        (>= F C)
        (<= G H)
        (<= I H)
        (<= J K)
        (= L (+ 1 G))
        (= M (+ 1 I))
        (= M (+ 1 J))
        (= B 1)
        (diff_new111 N J A I G)
        (new109 K A H)
        (diff_new4 A B C N)
      )
      (diff_new4 A B C A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Bool) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A true)
        (>= G C)
        (<= H I)
        (<= J K)
        (= L (+ 1 H))
        (= M (+ 1 J))
        (= B 1)
        (diff_new114 N J D H)
        (new109 K A I)
        (diff_new4 A B C N)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A true)
        (= D false)
        (= A true)
        (>= G (+ H 1))
        (>= I C)
        (<= J H)
        (<= K L)
        (= M (+ 1 J))
        (= N (+ 1 K))
        (= B 1)
        (new109 L A H)
        (new116 K G B C A J)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= A true)
        (= D false)
        (= A true)
        (>= G C)
        (<= (+ H 1) (+ 1 I))
        (<= J K)
        (<= L M)
        (= N (+ 1 J))
        (= H (+ 1 L))
        (= B 1)
        (new109 M A K)
        (new116 L I B C A J)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= A true)
        (= D false)
        (= A true)
        (>= G (+ (+ 1 H) 1))
        (>= I C)
        (<= J K)
        (<= L M)
        (= N (+ 1 J))
        (= G (+ 1 L))
        (= B 1)
        (new109 M A K)
        (new116 L H B C A J)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= D true)
        (= E false)
        (= A false)
        (= A false)
        (>= F C)
        (<= G H)
        (= I (+ 1 G))
        (= B 1)
        (new121 H A)
        (new122 G B C)
      )
      (diff_new4 A B C A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G C)
        (<= H I)
        (= J (+ 1 H))
        (= B 1)
        (new121 I A)
        (new124 H D B C)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= J K)
        (= L (+ 1 J))
        (= B 1)
        (new109 K A H)
        (new126 J G B C)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G C)
        (<= (+ H 1) (+ 1 I))
        (<= J K)
        (= H (+ 1 J))
        (= B 1)
        (new121 K A)
        (new126 J I B C)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I C)
        (<= J K)
        (= G (+ 1 J))
        (= B 1)
        (new121 K A)
        (new126 J H B C)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Bool) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D true)
        (= A false)
        (>= G C)
        (<= H I)
        (<= J K)
        (= L (+ 1 H))
        (= L (+ 1 J))
        (= B 1)
        (diff_new133 M J D H)
        (new109 K D I)
        (diff_new4 A B C M)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G C)
        (<= H I)
        (= J (+ 1 H))
        (= B 1)
        (new121 I D)
        (new135 H B C A)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Bool) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G C)
        (<= H I)
        (= J (+ 1 H))
        (= B 1)
        (diff_new138 K H D)
        (new136 I)
        (diff_new4 A B C K)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= J K)
        (= L (+ 1 J))
        (= B 1)
        (new139 K H)
        (new140 J G B C A)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G C)
        (<= (+ H 1) (+ 1 I))
        (<= J K)
        (= H (+ 1 J))
        (= B 1)
        (new136 K)
        (new140 J I B C A)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I C)
        (<= J K)
        (= G (+ 1 J))
        (= B 1)
        (new136 K)
        (new140 J H B C A)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D true)
        (= A false)
        (= D true)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= J H)
        (<= K L)
        (= M (+ 1 J))
        (= M (+ 1 K))
        (= B 1)
        (new109 L D H)
        (new146 K D J B C G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= J K)
        (= L (+ 1 J))
        (= B 1)
        (new109 K D H)
        (new148 J B C G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= J K)
        (= L (+ 1 J))
        (= B 1)
        (new139 K H)
        (new150 J D B C G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ H 1))
        (>= J C)
        (<= K L)
        (= M (+ 1 K))
        (= B 1)
        (new139 L H)
        (new152 K G B C I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= (+ J 1) (+ 1 K))
        (<= L M)
        (= J (+ 1 L))
        (= B 1)
        (new139 M H)
        (new152 L K B C G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ (+ 1 J) 1))
        (>= K C)
        (<= L M)
        (= I (+ 1 L))
        (= B 1)
        (new139 M H)
        (new152 L J B C G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D true)
        (= D true)
        (= A false)
        (>= G C)
        (<= (+ H 1) (+ 1 I))
        (<= J K)
        (<= L M)
        (= N (+ 1 J))
        (= N (+ 1 L))
        (= B 1)
        (new109 M D K)
        (new146 L D J B C I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G C)
        (<= (+ H 1) (+ 1 I))
        (<= J K)
        (= L (+ 1 J))
        (= B 1)
        (new121 K D)
        (new148 J B C I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G C)
        (<= (+ H 1) (+ 1 I))
        (<= J K)
        (= L (+ 1 J))
        (= B 1)
        (new136 K)
        (new150 J D B C I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= (+ J 1) (+ 1 K))
        (<= L M)
        (= N (+ 1 L))
        (= B 1)
        (new139 M H)
        (new152 L G B C K)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G C)
        (<= (+ H 1) (+ 1 I))
        (<= (+ J 1) (+ 1 K))
        (<= L M)
        (= J (+ 1 L))
        (= B 1)
        (new136 M)
        (new152 L K B C I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I C)
        (<= (+ J 1) (+ 1 K))
        (<= L M)
        (= G (+ 1 L))
        (= B 1)
        (new136 M)
        (new152 L H B C K)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D true)
        (= D true)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I C)
        (<= J K)
        (<= L M)
        (= N (+ 1 J))
        (= N (+ 1 L))
        (= B 1)
        (new109 M D K)
        (new146 L D J B C H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I C)
        (<= J K)
        (= L (+ 1 J))
        (= B 1)
        (new121 K D)
        (new148 J B C H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I C)
        (<= J K)
        (= L (+ 1 J))
        (= B 1)
        (new136 K)
        (new150 J D B C H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I (+ J 1))
        (>= K C)
        (<= L M)
        (= N (+ 1 L))
        (= B 1)
        (new139 M J)
        (new152 L I B C H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I C)
        (<= (+ J 1) (+ 1 K))
        (<= L M)
        (= J (+ 1 L))
        (= B 1)
        (new136 M)
        (new152 L K B C H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I (+ (+ 1 J) 1))
        (>= K C)
        (<= L M)
        (= I (+ 1 L))
        (= B 1)
        (new136 M)
        (new152 L J B C H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (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 Bool) )
    (=>
      (and
        (= D false)
        (= E false)
        (= A true)
        (>= F (+ G 1))
        (>= H C)
        (<= I J)
        (<= J K)
        (= L (+ 1 I))
        (= M (+ 1 J))
        (= M (+ 1 G))
        (= B 1)
        (diff_new111 N F A K I)
        (diff_new4 A B C N)
        (new109 G A J)
      )
      (diff_new4 A B C A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Bool) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A true)
        (>= G (+ H 1))
        (>= I C)
        (<= J K)
        (= L (+ 1 J))
        (= M (+ 1 H))
        (= B 1)
        (diff_new114 N G D J)
        (diff_new4 A B C N)
        (new109 H A K)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A true)
        (= D false)
        (= A true)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= K C)
        (<= L G)
        (= M (+ 1 L))
        (= N (+ 1 J))
        (= B 1)
        (new116 I H B C A L)
        (new109 J A G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= A true)
        (= D false)
        (= A true)
        (>= G (+ H 1))
        (>= I C)
        (<= (+ J 1) (+ 1 K))
        (<= L K)
        (= M (+ 1 L))
        (= J (+ 1 H))
        (= B 1)
        (new189 G B C A L)
        (new109 H A K)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= A true)
        (= D false)
        (= A true)
        (>= G (+ H 1))
        (>= I (+ (+ 1 J) 1))
        (>= K C)
        (<= L J)
        (= M (+ 1 L))
        (= I (+ 1 H))
        (= B 1)
        (new189 G B C A L)
        (new109 H A J)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (= J (+ 1 H))
        (= B 1)
        (new124 G D B C)
        (new121 H A)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= D false)
        (= E false)
        (= A false)
        (= A false)
        (>= F (+ G 1))
        (>= H C)
        (= I (+ 1 G))
        (= B 1)
        (new122 F B C)
        (new121 G A)
      )
      (diff_new4 A B C A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= K C)
        (= L (+ 1 J))
        (= B 1)
        (new126 I H B C)
        (new109 J A G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= (+ J 1) (+ 1 K))
        (= J (+ 1 H))
        (= B 1)
        (new122 G B C)
        (new109 H A K)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ (+ 1 J) 1))
        (>= K C)
        (= I (+ 1 H))
        (= B 1)
        (new122 G B C)
        (new109 H A J)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Bool) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D true)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= J K)
        (= L (+ 1 J))
        (= L (+ 1 H))
        (= B 1)
        (diff_new133 M G D K)
        (diff_new4 A B C M)
        (new109 H D J)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Bool) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (= J (+ 1 H))
        (= B 1)
        (diff_new138 K G D)
        (diff_new4 A B C K)
        (new136 H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (= J (+ 1 H))
        (= B 1)
        (new135 G B C A)
        (new121 H D)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= K C)
        (= L (+ 1 J))
        (= B 1)
        (new140 I H B C A)
        (new139 J G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= (+ J 1) (+ 1 K))
        (= J (+ 1 H))
        (= B 1)
        (new135 G B C A)
        (new139 H K)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ (+ 1 J) 1))
        (>= K C)
        (= I (+ 1 H))
        (= B 1)
        (new135 G B C A)
        (new139 H J)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D true)
        (= A false)
        (= D true)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= K C)
        (<= H L)
        (= M (+ 1 H))
        (= M (+ 1 J))
        (= B 1)
        (new146 I D L B C G)
        (new109 J D H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= K C)
        (= L (+ 1 J))
        (= B 1)
        (new150 I D B C G)
        (new139 J H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= K C)
        (= L (+ 1 J))
        (= B 1)
        (new148 I B C G)
        (new109 J D H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ G 1))
        (>= J (+ K 1))
        (>= L C)
        (= M (+ 1 K))
        (= B 1)
        (new152 J H B C I)
        (new139 K G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= K C)
        (<= (+ L 1) (+ 1 H))
        (= L (+ 1 J))
        (= B 1)
        (new148 I B C G)
        (new139 J H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= A false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= K (+ (+ 1 H) 1))
        (>= L C)
        (= K (+ 1 J))
        (= B 1)
        (new148 I B C G)
        (new139 J H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D true)
        (= D true)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= (+ J 1) (+ 1 K))
        (<= L M)
        (= N (+ 1 L))
        (= N (+ 1 H))
        (= B 1)
        (new146 G D M B C K)
        (new109 H D L)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= (+ J 1) (+ 1 K))
        (= L (+ 1 H))
        (= B 1)
        (new150 G D B C K)
        (new136 H)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= (+ J 1) (+ 1 K))
        (= L (+ 1 H))
        (= B 1)
        (new148 G B C K)
        (new121 H D)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ J 1))
        (>= K C)
        (<= (+ L 1) (+ 1 M))
        (= N (+ 1 J))
        (= B 1)
        (new152 I H B C M)
        (new139 J G)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I C)
        (<= (+ J 1) (+ 1 K))
        (<= (+ L 1) (+ 1 M))
        (= L (+ 1 H))
        (= B 1)
        (new148 G B C K)
        (new139 H M)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ H 1))
        (>= I (+ (+ 1 J) 1))
        (>= K C)
        (<= (+ L 1) (+ 1 M))
        (= I (+ 1 H))
        (= B 1)
        (new148 G B C M)
        (new139 H J)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D true)
        (= D true)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I (+ J 1))
        (>= K C)
        (<= L M)
        (= N (+ 1 L))
        (= N (+ 1 J))
        (= B 1)
        (new146 I D M B C H)
        (new109 J D L)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I (+ J 1))
        (>= K C)
        (= L (+ 1 J))
        (= B 1)
        (new150 I D B C H)
        (new136 J)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I (+ J 1))
        (>= K C)
        (= L (+ 1 J))
        (= B 1)
        (new148 I B C H)
        (new121 J D)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I (+ J 1))
        (>= K (+ L 1))
        (>= M C)
        (= N (+ 1 L))
        (= B 1)
        (new152 K J B C H)
        (new139 L I)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I (+ J 1))
        (>= K C)
        (<= (+ L 1) (+ 1 M))
        (= L (+ 1 J))
        (= B 1)
        (new148 I B C H)
        (new139 J M)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (= D false)
        (= A false)
        (>= G (+ (+ 1 H) 1))
        (>= I (+ J 1))
        (>= K (+ (+ 1 L) 1))
        (>= M C)
        (= K (+ 1 J))
        (= B 1)
        (new148 I B C H)
        (new139 J L)
      )
      (diff_new4 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A true)
      (new2 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (<= B C)
        (= D (+ 1 B))
        (new5 A C)
        (new5 A B)
      )
      (new2 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (and
        (= A false)
        (new2 A)
      )
      (new2 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (and
        (= A false)
        (new2 A)
      )
      (new2 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= B (+ C 1))
        (new11 C)
        (new11 B)
      )
      (new2 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (<= (+ B 1) (+ 1 C))
        (new11 C)
      )
      (new2 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (>= B (+ (+ 1 C) 1))
        (new11 C)
      )
      (new2 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (new2 A)
      (new1 A A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= C 1)
        (diff_new4 D C E A)
        (new1 D B)
      )
      (new1 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= A true)
        (= B true)
        (new1 A B)
      )
      ff
    )
  )
)

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