; Automatically generated by map2smt

(set-logic HORN)




(declare-fun new6 (Bool) Bool)
(declare-fun new4 (Bool Int) Bool)
(declare-fun new188 (Int Int Int Bool Int) Bool)
(declare-fun new151 (Int Int Int Int Int) Bool)
(declare-fun new149 (Int Bool Int Int Int) Bool)
(declare-fun new147 (Int Int Int Int) Bool)
(declare-fun new145 (Int Bool Int Int Int Int) Bool)
(declare-fun new139 (Int Int Int Int Bool) Bool)
(declare-fun new138 (Int Int) Bool)
(declare-fun new135 (Int) Bool)
(declare-fun new134 (Int Int Int Bool) Bool)
(declare-fun new125 (Int Int Int Int) Bool)
(declare-fun new123 (Int Bool Int Int) Bool)
(declare-fun new121 (Int Int Int) Bool)
(declare-fun new120 (Int Bool) Bool)
(declare-fun new115 (Int Int Int Int Bool Int) Bool)
(declare-fun new108 (Int Bool Int) Bool)
(declare-fun new10 (Int) Bool)
(declare-fun new1 (Bool) Bool)
(declare-fun diff_new588 (Bool Bool Int) Bool)
(declare-fun diff_new3 (Bool Int Int Bool) Bool)
(declare-fun diff_new137 (Bool Int Bool) Bool)
(declare-fun diff_new132 (Bool Int Bool Int) Bool)
(declare-fun diff_new113 (Bool Int Bool Int) Bool)
(declare-fun diff_new110 (Bool Int Bool Int Int) Bool)
(declare-fun not_fun_diff_new588 () Bool)
(declare-fun constr (Bool) Bool)
(declare-fun not_fun_diff_new137 () Bool)
(declare-fun not_fun_diff_new132 () Bool)
(declare-fun not_fun_diff_new113 () Bool)
(declare-fun not_fun_diff_new110 () Bool)
(declare-fun not_fun_diff_new3 () Bool)
(declare-fun ff () Bool)

(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (diff_new588 A B C)
        (diff_new588 D E F)
        (and (= A D) (or (not (= B E)) (not (= C F))))
      )
      not_fun_diff_new588
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Bool) )
    (=>
      (and
        (diff_new137 A B C)
        (diff_new137 D E F)
        (and (= A D) (or (not (= B E)) (not (= C F))))
      )
      not_fun_diff_new137
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Bool) (F Int) (G Bool) (H Int) )
    (=>
      (and
        (diff_new132 A B C D)
        (diff_new132 E F G H)
        (and (= A E) (or (not (= B F)) (or (not (= C G)) (not (= D H)))))
      )
      not_fun_diff_new132
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Bool) (F Int) (G Bool) (H Int) )
    (=>
      (and
        (diff_new113 A B C D)
        (diff_new113 E F G H)
        (and (= A E) (or (not (= B F)) (or (not (= C G)) (not (= D H)))))
      )
      not_fun_diff_new113
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Bool) (G Int) (H Bool) (I Int) (J Int) )
    (=>
      (and
        (diff_new110 A B C D E)
        (diff_new110 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_new110
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Bool) )
    (=>
      (and
        (diff_new3 A B C D)
        (diff_new3 E F G H)
        (and (and (= A E) (and (= B F) (= C G))) (not (= D H)))
      )
      not_fun_diff_new3
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (= A true)
        (= C 0)
      )
      (diff_new588 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))
        (new4 A D)
        (new4 A C)
      )
      (diff_new588 A A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= B (+ 1 C))
        (new10 C)
        (new6 A)
      )
      (diff_new588 A A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (= C (+ 1 D))
        (new4 B D)
        (new6 A)
      )
      (diff_new588 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))
        (new4 A E)
        (new10 D)
      )
      (diff_new588 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))
        (new10 E)
        (new6 A)
      )
      (diff_new588 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))
        (new10 E)
        (new6 A)
      )
      (diff_new588 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (= C (+ 1 D))
        (new6 B)
        (new4 A D)
      )
      (diff_new588 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= B (+ 1 C))
        (new4 A C)
      )
      (diff_new588 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))
        (new10 E)
        (new4 A D)
      )
      (diff_new588 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))
        (new4 A E)
      )
      (diff_new588 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))
        (new4 A E)
      )
      (diff_new588 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))
        (new4 B E)
        (new10 D)
      )
      (diff_new588 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))
        (new4 B D)
        (new10 E)
      )
      (diff_new588 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))
        (new10 E)
        (new10 D)
      )
      (diff_new588 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))
        (new10 E)
        (new10 D)
      )
      (diff_new588 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))
        (new10 F)
        (new10 E)
      )
      (diff_new588 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))
        (new6 B)
        (new10 E)
      )
      (diff_new588 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))
        (new4 B E)
      )
      (diff_new588 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))
        (new10 E)
        (new10 D)
      )
      (diff_new588 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))
        (new10 E)
      )
      (diff_new588 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))
        (new6 B)
        (new10 E)
      )
      (diff_new588 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))
        (new4 B E)
      )
      (diff_new588 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))
        (new10 F)
        (new10 E)
      )
      (diff_new588 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))
        (new10 E)
      )
      (diff_new588 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= D 0)
        (= A 1)
      )
      (new188 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)
        (new4 D I)
        (new4 D H)
      )
      (new188 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)
        (new6 D)
        (new10 K)
      )
      (new188 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)
        (new4 D K)
      )
      (new188 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)
        (new10 I)
        (new10 H)
      )
      (new188 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)
        (new10 I)
      )
      (new188 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)
        (new10 I)
      )
      (new188 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)
        (new4 D K)
        (new4 D J)
      )
      (new188 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)
        (new6 D)
        (new10 L)
      )
      (new188 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)
        (new4 D L)
      )
      (new188 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)
        (new10 I)
        (new10 H)
      )
      (new188 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)
        (new10 J)
      )
      (new188 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)
        (new10 J)
      )
      (new188 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)
        (new108 L D J)
        (new188 K B C D I)
      )
      (new188 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)
        (new120 J D)
        (new147 I B C K)
      )
      (new188 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)
        (new135 J)
        (new188 I B C D K)
      )
      (new188 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)
        (new138 L I)
        (new147 K B C H)
      )
      (new188 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)
        (new135 L)
        (new147 K B C J)
      )
      (new188 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)
        (new135 L)
        (new147 K B C I)
      )
      (new188 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)
        (new188 H B C D K)
        (new108 I D L)
      )
      (new188 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)
        (new147 H B C K)
        (new120 I D)
      )
      (new188 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)
        (new188 H B C D K)
        (new135 I)
      )
      (new188 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)
        (new147 J B C H)
        (new138 K I)
      )
      (new188 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)
        (new147 H B C L)
        (new135 I)
      )
      (new188 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)
        (new147 J B C I)
        (new135 K)
      )
      (new188 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))
      )
      (new151 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))
        (new10 L)
      )
      (new151 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))
        (new10 M)
      )
      (new151 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))
        (new135 J)
        (new151 I L C D K)
      )
      (new151 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))
        (new147 H C D K)
        (new138 I L)
      )
      (new151 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)
      )
      (new149 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)
        (new4 B I)
        (new4 B H)
      )
      (new149 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)
        (new10 K)
        (new6 B)
      )
      (new149 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)
        (new4 B K)
      )
      (new149 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)
        (new10 I)
        (new10 H)
      )
      (new149 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)
        (new10 I)
      )
      (new149 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)
        (new10 I)
      )
      (new149 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)
        (new10 M)
      )
      (new149 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)
        (new10 L)
      )
      (new149 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)
        (new10 L)
      )
      (new149 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)
        (new4 B K)
        (new4 B J)
      )
      (new149 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)
        (new10 L)
        (new6 B)
      )
      (new149 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)
        (new4 B L)
      )
      (new149 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)
        (new10 I)
        (new10 H)
      )
      (new149 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)
        (new10 J)
      )
      (new149 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)
        (new10 J)
      )
      (new149 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)
        (new10 M)
      )
      (new149 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)
        (new108 L B J)
        (new145 K B I C D M)
      )
      (new149 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)
        (new120 J B)
        (new147 I C D K)
      )
      (new149 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)
        (new135 J)
        (new149 I B C D K)
      )
      (new149 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)
        (new138 L I)
        (new151 K H C D M)
      )
      (new149 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)
        (new135 K)
        (new151 J I C D L)
      )
      (new149 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)
        (new135 K)
        (new151 J H C D L)
      )
      (new149 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)
        (new145 H B L C D M)
        (new108 I B K)
      )
      (new149 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)
        (new149 H B C D K)
        (new135 I)
      )
      (new149 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)
        (new147 H C D K)
        (new120 I B)
      )
      (new149 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)
        (new151 J I C D M)
        (new138 K H)
      )
      (new149 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)
        (new147 H C D L)
        (new138 I K)
      )
      (new149 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)
        (new147 H C D L)
        (new138 I J)
      )
      (new149 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (and
        (= C 0)
        (= A 1)
      )
      (new147 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)
        (new10 J)
      )
      (new147 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)
        (new10 K)
      )
      (new147 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)
        (new135 I)
        (new147 H B C J)
      )
      (new147 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)
        (new147 G B C J)
        (new135 H)
      )
      (new147 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))
      )
      (new145 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))
        (new4 B J)
        (new4 B I)
      )
      (new145 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))
        (new6 B)
        (new10 M)
      )
      (new145 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))
        (new4 B M)
      )
      (new145 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))
        (new10 J)
        (new10 I)
      )
      (new145 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))
        (new10 J)
      )
      (new145 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))
        (new10 J)
      )
      (new145 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))
        (new10 N)
      )
      (new145 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))
        (new10 M)
      )
      (new145 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))
        (new10 M)
      )
      (new145 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))
        (new4 B L)
        (new4 B K)
      )
      (new145 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))
        (new10 N)
        (new6 B)
      )
      (new145 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))
        (new4 B N)
      )
      (new145 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))
        (new10 J)
        (new10 I)
      )
      (new145 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))
        (new10 K)
      )
      (new145 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))
        (new10 K)
      )
      (new145 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))
        (new10 N)
      )
      (new145 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))
        (new108 M B K)
        (new145 L B J D E N)
      )
      (new145 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))
        (new120 K B)
        (new151 J M D E L)
      )
      (new145 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))
        (new135 K)
        (new145 J B M D E L)
      )
      (new145 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))
        (new138 M J)
        (new151 L I D E N)
      )
      (new145 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))
        (new135 L)
        (new151 K J D E M)
      )
      (new145 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))
        (new135 L)
        (new151 K I D E M)
      )
      (new145 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))
        (new145 I B M D E N)
        (new108 J B L)
      )
      (new145 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))
        (new149 I B D E L)
        (new138 J M)
      )
      (new145 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))
        (new147 I D E L)
        (new108 J B M)
      )
      (new145 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))
        (new151 K J D E N)
        (new138 L I)
      )
      (new145 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))
        (new147 I D E M)
        (new138 J L)
      )
      (new145 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))
        (new147 I D E M)
        (new138 J K)
      )
      (new145 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))
      )
      (new139 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))
        (new4 E I)
        (new4 E H)
      )
      (new139 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))
        (new6 E)
        (new10 L)
      )
      (new139 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))
        (new4 E L)
      )
      (new139 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))
        (new10 I)
        (new10 H)
      )
      (new139 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))
        (new10 I)
      )
      (new139 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))
        (new10 I)
      )
      (new139 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))
        (new4 E K)
        (new4 E J)
      )
      (new139 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))
        (new6 E)
      )
      (new139 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))
        (new6 E)
      )
      (new139 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))
        (new10 I)
        (new10 H)
      )
      (new139 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))
        (new10 J)
      )
      (new139 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))
        (new10 J)
      )
      (new139 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))
        (new108 L E J)
        (new115 K N C D E I)
      )
      (new139 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))
        (new120 J E)
        (new125 I K C D)
      )
      (new139 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))
        (new135 J)
        (new139 I K C D E)
      )
      (new139 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))
        (new138 L I)
        (new151 K M C D H)
      )
      (new139 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))
        (new135 L)
        (new151 K M C D J)
      )
      (new139 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))
        (new135 L)
        (new151 K M C D I)
      )
      (new139 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))
        (new188 H C D E K)
        (new108 I E L)
      )
      (new139 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))
        (new121 H C D)
        (new108 I E K)
      )
      (new139 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))
        (new134 H C D E)
        (new138 I K)
      )
      (new139 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))
        (new147 J C D H)
        (new138 K I)
      )
      (new139 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))
        (new147 H C D L)
        (new138 I M)
      )
      (new139 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))
        (new147 J C D I)
        (new138 K M)
      )
      (new139 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= B 0)
        (= A 0)
      )
      (new138 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (and
        (= B (+ 1 C))
        (new10 C)
      )
      (new138 A B)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new135 A)
    )
  )
)
(assert
  (forall ( (A Int) )
    (new135 A)
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= A true)
        (= B 0)
      )
      (diff_new137 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))
        (new4 A D)
        (new4 A C)
      )
      (diff_new137 A B A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (new6 A)
      )
      (diff_new137 A B A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
        (new6 C)
        (new6 A)
      )
      (diff_new137 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))
        (new4 A E)
        (new10 D)
      )
      (diff_new137 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 D))
        (new10 D)
        (new6 A)
      )
      (diff_new137 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 D) 1))
        (new10 D)
        (new6 A)
      )
      (diff_new137 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
        (new6 C)
        (new6 A)
      )
      (diff_new137 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (new6 A)
      )
      (diff_new137 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))
        (new10 E)
        (new4 A D)
      )
      (diff_new137 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 D))
        (new4 A D)
      )
      (diff_new137 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 D) 1))
        (new4 A D)
      )
      (diff_new137 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))
        (new4 C E)
        (new10 D)
      )
      (diff_new137 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))
        (new4 C D)
        (new10 E)
      )
      (diff_new137 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))
        (new10 E)
        (new10 D)
      )
      (diff_new137 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))
        (new10 E)
        (new10 D)
      )
      (diff_new137 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))
        (new10 E)
        (new10 D)
      )
      (diff_new137 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 D))
        (new6 C)
        (new10 D)
      )
      (diff_new137 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 D))
        (new4 C D)
      )
      (diff_new137 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))
        (new10 E)
        (new10 D)
      )
      (diff_new137 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ B 1) (+ 1 D))
        (new10 D)
      )
      (diff_new137 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 D) 1))
        (new6 C)
        (new10 D)
      )
      (diff_new137 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 D) 1))
        (new4 C D)
      )
      (diff_new137 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))
        (new10 E)
        (new10 D)
      )
      (diff_new137 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= B (+ (+ 1 D) 1))
        (new10 D)
      )
      (diff_new137 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= A 1)
      )
      (new134 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)
        (new4 D H)
        (new4 D G)
      )
      (new134 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)
        (new6 D)
      )
      (new134 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)
        (new6 D)
      )
      (new134 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)
        (new10 H)
        (new10 G)
      )
      (new134 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)
        (new10 H)
      )
      (new134 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)
        (new10 H)
      )
      (new134 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)
        (new4 D J)
        (new4 D I)
      )
      (new134 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)
        (new6 D)
      )
      (new134 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)
        (new6 D)
      )
      (new134 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)
        (new10 H)
        (new10 G)
      )
      (new134 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)
        (new10 I)
      )
      (new134 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)
        (new10 I)
      )
      (new134 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)
        (new108 K D I)
        (new188 J B C D H)
      )
      (new134 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)
        (new120 I D)
        (new121 H B C)
      )
      (new134 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)
        (new135 I)
        (new134 H B C D)
      )
      (new134 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)
        (new138 K H)
        (new147 J B C G)
      )
      (new134 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)
        (new135 K)
        (new147 J B C I)
      )
      (new134 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)
        (new135 K)
        (new147 J B C H)
      )
      (new134 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)
        (new188 G B C D J)
        (new108 H D K)
      )
      (new134 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)
        (new121 G B C)
        (new120 H D)
      )
      (new134 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)
        (new134 G B C D)
        (new135 H)
      )
      (new134 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)
        (new147 I B C G)
        (new138 J H)
      )
      (new134 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)
        (new147 G B C K)
        (new135 H)
      )
      (new134 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)
        (new147 I B C H)
        (new135 J)
      )
      (new134 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= A true)
        (= D 0)
        (= B 0)
      )
      (diff_new132 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))
        (new4 A E)
        (new4 A D)
      )
      (diff_new132 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (new10 D)
        (new6 A)
      )
      (diff_new132 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (new4 C E)
        (new6 A)
      )
      (diff_new132 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))
        (new4 A F)
        (new10 E)
      )
      (diff_new132 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))
        (new10 E)
        (new6 A)
      )
      (diff_new132 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))
        (new10 E)
        (new6 A)
      )
      (diff_new132 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (new6 C)
        (new4 A E)
      )
      (diff_new132 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (new4 A D)
      )
      (diff_new132 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))
        (new10 F)
        (new4 A E)
      )
      (diff_new132 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))
        (new4 A E)
      )
      (diff_new132 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))
        (new4 A E)
      )
      (diff_new132 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))
        (new4 C F)
        (new10 E)
      )
      (diff_new132 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))
        (new4 C E)
        (new10 F)
      )
      (diff_new132 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))
        (new10 F)
        (new10 E)
      )
      (diff_new132 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))
        (new10 F)
        (new10 E)
      )
      (diff_new132 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))
        (new10 F)
        (new10 E)
      )
      (diff_new132 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))
        (new6 C)
        (new10 E)
      )
      (diff_new132 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))
        (new4 C E)
      )
      (diff_new132 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))
        (new10 F)
        (new10 E)
      )
      (diff_new132 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))
        (new10 E)
      )
      (diff_new132 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))
        (new6 C)
        (new10 E)
      )
      (diff_new132 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))
        (new4 C E)
      )
      (diff_new132 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))
        (new10 F)
        (new10 E)
      )
      (diff_new132 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))
        (new10 E)
      )
      (diff_new132 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= D 0)
        (= A 1)
        (= B (+ 1 D))
      )
      (new125 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))
        (new10 K)
      )
      (new125 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))
      )
      (new125 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))
        (new135 I)
        (new125 H J C D)
      )
      (new125 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))
        (new121 G C D)
        (new138 H J)
      )
      (new125 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)
      )
      (new123 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)
        (new4 B H)
        (new4 B G)
      )
      (new123 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)
        (new6 B)
      )
      (new123 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)
        (new6 B)
      )
      (new123 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)
        (new10 H)
        (new10 G)
      )
      (new123 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)
        (new10 H)
      )
      (new123 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)
        (new10 H)
      )
      (new123 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)
        (new10 L)
      )
      (new123 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)
        (new10 K)
      )
      (new123 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)
        (new10 K)
      )
      (new123 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)
        (new4 B J)
        (new4 B I)
      )
      (new123 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)
        (new6 B)
      )
      (new123 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)
        (new6 B)
      )
      (new123 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)
        (new10 H)
        (new10 G)
      )
      (new123 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)
        (new10 I)
      )
      (new123 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)
        (new10 I)
      )
      (new123 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)
        (new10 L)
      )
      (new123 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_new588 L B H)
        (new108 K B I)
        (new123 J L C D)
      )
      (new123 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)
        (new120 I B)
        (new121 H C D)
      )
      (new123 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)
        (new135 I)
        (new123 H B C D)
      )
      (new123 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)
        (new138 K H)
        (new125 J G C D)
      )
      (new123 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)
        (new135 J)
        (new125 I H C D)
      )
      (new123 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)
        (new135 J)
        (new125 I G C D)
      )
      (new123 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_new588 L B K)
        (new123 H L C D)
        (new108 I B J)
      )
      (new123 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)
        (new123 G B C D)
        (new135 H)
      )
      (new123 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)
        (new121 G C D)
        (new120 H B)
      )
      (new123 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)
        (new125 I H C D)
        (new138 J G)
      )
      (new123 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)
        (new121 G C D)
        (new138 H J)
      )
      (new123 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)
        (new121 G C D)
        (new138 H I)
      )
      (new123 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (= A 1)
      (new121 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)
      )
      (new121 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)
      )
      (new121 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)
        (new135 H)
        (new121 G B C)
      )
      (new121 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)
        (new121 F B C)
        (new135 G)
      )
      (new121 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (= A 0)
      )
      (new120 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (<= C D)
        (= A (+ 1 C))
        (new4 B D)
        (new4 B C)
      )
      (new120 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B false)
        (new6 B)
      )
      (new120 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B false)
        (new6 B)
      )
      (new120 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= C (+ D 1))
        (new10 D)
        (new10 C)
      )
      (new120 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (+ A 1) (+ 1 C))
        (new10 C)
      )
      (new120 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= A (+ (+ 1 C) 1))
        (new10 C)
      )
      (new120 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))
      )
      (new115 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))
        (new4 E J)
        (new4 E I)
      )
      (new115 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))
        (new6 E)
        (new10 M)
      )
      (new115 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))
        (new4 E M)
      )
      (new115 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))
        (new10 J)
        (new10 I)
      )
      (new115 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))
        (new10 J)
      )
      (new115 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))
        (new10 J)
      )
      (new115 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))
        (new4 E L)
        (new4 E K)
      )
      (new115 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))
        (new6 E)
        (new10 N)
      )
      (new115 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))
        (new4 E N)
      )
      (new115 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))
        (new10 J)
        (new10 I)
      )
      (new115 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))
        (new10 K)
      )
      (new115 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))
        (new10 K)
      )
      (new115 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))
        (new108 M E K)
        (new115 L O C D E J)
      )
      (new115 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))
        (new120 K E)
        (new151 J M C D L)
      )
      (new115 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))
        (new135 K)
        (new115 J M C D E L)
      )
      (new115 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))
        (new138 M J)
        (new151 L N C D I)
      )
      (new115 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))
        (new135 M)
        (new151 L N C D K)
      )
      (new115 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))
        (new135 M)
        (new151 L N C D J)
      )
      (new115 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))
        (new188 I C D E L)
        (new108 J E M)
      )
      (new115 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))
        (new147 I C D L)
        (new108 J E M)
      )
      (new115 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))
        (new188 I C D E L)
        (new138 J M)
      )
      (new115 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))
        (new147 K C D I)
        (new138 L J)
      )
      (new115 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))
        (new147 I C D M)
        (new138 J N)
      )
      (new115 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))
        (new147 K C D J)
        (new138 L N)
      )
      (new115 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_new113 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)
        (new10 E)
      )
      (diff_new113 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)
        (new4 A E)
        (new4 A D)
      )
      (diff_new113 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))
        (new10 F)
        (new4 A E)
        (new4 A D)
      )
      (diff_new113 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C 0)
        (new6 A)
      )
      (diff_new113 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D 0)
        (new6 C)
        (new6 A)
      )
      (diff_new113 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)
        (new4 A F)
        (new10 E)
      )
      (diff_new113 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)
        (new10 E)
        (new6 A)
      )
      (diff_new113 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)
        (new10 E)
        (new6 A)
      )
      (diff_new113 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (new10 D)
        (new6 A)
      )
      (diff_new113 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (new6 C)
        (new10 E)
        (new6 A)
      )
      (diff_new113 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))
        (new4 A F)
        (new10 E)
        (new10 G)
      )
      (diff_new113 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))
        (new10 E)
        (new10 F)
        (new6 A)
      )
      (diff_new113 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))
        (new10 E)
        (new10 F)
        (new6 A)
      )
      (diff_new113 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D 0)
        (new6 C)
        (new6 A)
      )
      (diff_new113 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C 0)
        (new6 A)
      )
      (diff_new113 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)
        (new10 F)
        (new4 A E)
      )
      (diff_new113 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)
        (new4 A E)
      )
      (diff_new113 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)
        (new4 A E)
      )
      (diff_new113 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (new6 C)
        (new10 E)
        (new6 A)
      )
      (diff_new113 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (new10 D)
        (new6 A)
      )
      (diff_new113 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))
        (new10 F)
        (new4 A E)
        (new10 G)
      )
      (diff_new113 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))
        (new4 A E)
        (new10 F)
      )
      (diff_new113 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))
        (new4 A E)
        (new10 F)
      )
      (diff_new113 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)
        (new4 C F)
        (new10 E)
      )
      (diff_new113 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)
        (new4 C E)
        (new10 F)
      )
      (diff_new113 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)
        (new10 F)
        (new10 E)
      )
      (diff_new113 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)
        (new10 F)
        (new10 E)
      )
      (diff_new113 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)
        (new10 F)
        (new10 E)
      )
      (diff_new113 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))
        (new4 C F)
        (new10 G)
        (new10 E)
      )
      (diff_new113 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))
        (new4 C E)
        (new10 G)
        (new10 F)
      )
      (diff_new113 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))
        (new10 G)
        (new10 F)
        (new10 E)
      )
      (diff_new113 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))
        (new10 G)
        (new10 F)
        (new10 E)
      )
      (diff_new113 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))
        (new10 G)
        (new10 F)
        (new10 E)
      )
      (diff_new113 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)
        (new6 C)
        (new10 E)
      )
      (diff_new113 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)
        (new4 C E)
      )
      (diff_new113 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)
        (new10 F)
        (new10 E)
      )
      (diff_new113 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)
        (new10 E)
      )
      (diff_new113 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))
        (new6 C)
        (new10 F)
        (new10 E)
      )
      (diff_new113 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))
        (new4 C E)
        (new10 F)
      )
      (diff_new113 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))
        (new10 F)
        (new10 G)
        (new10 E)
      )
      (diff_new113 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))
        (new10 F)
        (new10 E)
      )
      (diff_new113 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)
        (new6 C)
        (new10 E)
      )
      (diff_new113 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)
        (new4 C E)
      )
      (diff_new113 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)
        (new10 F)
        (new10 E)
      )
      (diff_new113 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)
        (new10 E)
      )
      (diff_new113 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))
        (new6 C)
        (new10 F)
        (new10 E)
      )
      (diff_new113 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))
        (new4 C E)
        (new10 F)
      )
      (diff_new113 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))
        (new10 F)
        (new10 G)
        (new10 E)
      )
      (diff_new113 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))
        (new10 F)
        (new10 E)
      )
      (diff_new113 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (= C 0)
        (= A 0)
      )
      (new108 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))
        (new4 B E)
        (new4 B D)
      )
      (new108 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= C (+ 1 D))
        (new10 D)
        (new6 B)
      )
      (new108 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= C (+ 1 D))
        (new4 B D)
      )
      (new108 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))
        (new10 E)
        (new10 D)
      )
      (new108 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (<= (+ A 1) (+ 1 D))
        (= C (+ 1 D))
        (new10 D)
      )
      (new108 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (>= A (+ (+ 1 D) 1))
        (= C (+ 1 D))
        (new10 D)
      )
      (new108 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_new110 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)
        (new10 F)
      )
      (diff_new110 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))
        (new4 A F)
        (new4 A E)
      )
      (diff_new110 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))
        (new10 G)
        (new4 A F)
        (new4 A E)
      )
      (diff_new110 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))
        (new10 E)
        (new6 A)
      )
      (diff_new110 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))
        (new4 C F)
        (new6 A)
      )
      (diff_new110 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))
        (new4 A G)
        (new10 F)
      )
      (diff_new110 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))
        (new10 F)
        (new6 A)
      )
      (diff_new110 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))
        (new10 F)
        (new6 A)
      )
      (diff_new110 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))
        (new10 F)
        (new10 E)
        (new6 A)
      )
      (diff_new110 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))
        (new4 C G)
        (new10 F)
        (new6 A)
      )
      (diff_new110 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))
        (new4 A G)
        (new10 F)
        (new10 H)
      )
      (diff_new110 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))
        (new10 F)
        (new10 G)
        (new6 A)
      )
      (diff_new110 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))
        (new10 F)
        (new10 G)
        (new6 A)
      )
      (diff_new110 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))
        (new6 C)
        (new4 A F)
      )
      (diff_new110 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))
        (new4 A E)
      )
      (diff_new110 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))
        (new10 G)
        (new4 A F)
      )
      (diff_new110 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))
        (new4 A F)
      )
      (diff_new110 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))
        (new4 A F)
      )
      (diff_new110 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))
        (new6 C)
        (new4 A G)
        (new10 F)
      )
      (diff_new110 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))
        (new4 A F)
        (new10 E)
      )
      (diff_new110 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))
        (new10 G)
        (new4 A F)
        (new10 H)
      )
      (diff_new110 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))
        (new4 A F)
        (new10 G)
      )
      (diff_new110 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))
        (new4 A F)
        (new10 G)
      )
      (diff_new110 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))
        (new4 C G)
        (new10 F)
      )
      (diff_new110 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))
        (new4 C F)
        (new10 G)
      )
      (diff_new110 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))
        (new10 G)
        (new10 F)
      )
      (diff_new110 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))
        (new10 G)
        (new10 F)
      )
      (diff_new110 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))
        (new10 G)
        (new10 F)
      )
      (diff_new110 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))
        (new4 C G)
        (new10 H)
        (new10 F)
      )
      (diff_new110 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))
        (new4 C F)
        (new10 H)
        (new10 G)
      )
      (diff_new110 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))
        (new10 H)
        (new10 G)
        (new10 F)
      )
      (diff_new110 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))
        (new10 H)
        (new10 G)
        (new10 F)
      )
      (diff_new110 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))
        (new10 H)
        (new10 G)
        (new10 F)
      )
      (diff_new110 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))
        (new6 C)
        (new10 F)
      )
      (diff_new110 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))
        (new4 C F)
      )
      (diff_new110 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))
        (new10 G)
        (new10 F)
      )
      (diff_new110 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))
        (new10 F)
      )
      (diff_new110 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))
        (new6 C)
        (new10 G)
        (new10 F)
      )
      (diff_new110 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))
        (new4 C F)
        (new10 G)
      )
      (diff_new110 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))
        (new10 G)
        (new10 H)
        (new10 F)
      )
      (diff_new110 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))
        (new10 G)
        (new10 F)
      )
      (diff_new110 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))
        (new6 C)
        (new10 F)
      )
      (diff_new110 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))
        (new4 C F)
      )
      (diff_new110 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))
        (new10 G)
        (new10 F)
      )
      (diff_new110 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))
        (new10 F)
      )
      (diff_new110 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))
        (new6 C)
        (new10 G)
        (new10 F)
      )
      (diff_new110 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))
        (new4 C F)
        (new10 G)
      )
      (diff_new110 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))
        (new10 G)
        (new10 H)
        (new10 F)
      )
      (diff_new110 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))
        (new10 G)
        (new10 F)
      )
      (diff_new110 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new10 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= A (+ 1 B))
        (new10 B)
      )
      (new10 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A true)
      (new6 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (<= B C)
        (= D (+ 1 B))
        (new4 A C)
        (new4 A B)
      )
      (new6 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (and
        (= A false)
        (new6 A)
      )
      (new6 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (and
        (= A false)
        (new6 A)
      )
      (new6 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= B (+ C 1))
        (new10 C)
        (new10 B)
      )
      (new6 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (<= (+ B 1) (+ 1 C))
        (new10 C)
      )
      (new6 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (>= B (+ (+ 1 C) 1))
        (new10 C)
      )
      (new6 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A true)
        (= B 0)
      )
      (new4 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (<= C D)
        (= E (+ 1 C))
        (= B (+ 1 C))
        (new4 A D)
        (new4 A C)
      )
      (new4 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= B (+ 1 C))
        (new10 C)
        (new6 A)
      )
      (new4 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= B (+ 1 C))
        (new4 A C)
      )
      (new4 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= C (+ D 1))
        (= B (+ 1 C))
        (new10 D)
        (new10 C)
      )
      (new4 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (<= (+ C 1) (+ 1 D))
        (= B (+ 1 D))
        (new10 D)
      )
      (new4 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (>= C (+ (+ 1 D) 1))
        (= B (+ 1 D))
        (new10 D)
      )
      (new4 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_new3 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)
        (new4 A G)
        (new4 A F)
      )
      (diff_new3 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)
        (new6 A)
      )
      (diff_new3 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)
        (new6 A)
        (new6 D)
      )
      (diff_new3 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)
        (new4 A H)
        (new10 G)
      )
      (diff_new3 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)
        (new6 A)
        (new10 H)
      )
      (diff_new3 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)
        (new6 A)
        (new10 H)
      )
      (diff_new3 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)
        (new6 A)
        (new10 L)
      )
      (diff_new3 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)
        (new6 A)
        (new10 L)
      )
      (diff_new3 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)
        (new6 A)
        (new10 L)
      )
      (diff_new3 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)
        (new6 A)
        (new6 D)
      )
      (diff_new3 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)
        (new6 A)
      )
      (diff_new3 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)
        (new4 A G)
        (new10 H)
      )
      (diff_new3 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)
        (new4 A H)
      )
      (diff_new3 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)
        (new4 A H)
      )
      (diff_new3 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)
        (new4 A L)
      )
      (diff_new3 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)
        (new4 A L)
      )
      (diff_new3 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)
        (new4 A L)
      )
      (diff_new3 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)
        (new4 D H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 H)
        (new4 D G)
      )
      (diff_new3 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)
        (new10 H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 J)
        (new10 I)
      )
      (diff_new3 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)
        (new10 H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 H)
        (new6 D)
      )
      (diff_new3 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)
        (new4 D H)
      )
      (diff_new3 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)
        (new10 H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 H)
      )
      (diff_new3 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)
        (new10 J)
      )
      (diff_new3 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)
        (new10 J)
      )
      (diff_new3 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)
        (new10 H)
        (new6 D)
      )
      (diff_new3 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)
        (new4 D H)
      )
      (diff_new3 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)
        (new10 H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 H)
      )
      (diff_new3 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)
        (new10 J)
      )
      (diff_new3 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)
        (new4 A I)
        (new4 A H)
      )
      (diff_new3 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)
        (new6 A)
      )
      (diff_new3 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)
        (new6 A)
        (new6 D)
      )
      (diff_new3 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)
        (new4 A H)
        (new10 G)
      )
      (diff_new3 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)
        (new6 A)
        (new10 I)
      )
      (diff_new3 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)
        (new6 A)
        (new10 I)
      )
      (diff_new3 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)
        (new6 A)
        (new10 L)
      )
      (diff_new3 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)
        (new6 A)
        (new6 D)
      )
      (diff_new3 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)
        (new6 A)
      )
      (diff_new3 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)
        (new4 A G)
        (new10 H)
      )
      (diff_new3 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)
        (new4 A I)
      )
      (diff_new3 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)
        (new4 A I)
      )
      (diff_new3 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)
        (new4 A L)
      )
      (diff_new3 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)
        (new4 D H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 H)
        (new4 D G)
      )
      (diff_new3 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)
        (new10 H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 J)
        (new10 I)
      )
      (diff_new3 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)
        (new10 I)
        (new6 D)
      )
      (diff_new3 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)
        (new4 D I)
      )
      (diff_new3 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)
        (new10 H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 I)
      )
      (diff_new3 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)
        (new10 I)
        (new6 D)
      )
      (diff_new3 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)
        (new4 D I)
      )
      (diff_new3 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)
        (new10 H)
        (new10 G)
      )
      (diff_new3 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)
        (new10 I)
      )
      (diff_new3 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)
        (new10 K)
      )
      (diff_new3 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_new110 N J A I G)
        (new108 K A H)
        (diff_new3 A B C N)
      )
      (diff_new3 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_new113 N J D H)
        (new108 K A I)
        (diff_new3 A B C N)
      )
      (diff_new3 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)
        (new108 L A H)
        (new115 K G B C A J)
      )
      (diff_new3 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)
        (new108 M A K)
        (new115 L I B C A J)
      )
      (diff_new3 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)
        (new108 M A K)
        (new115 L H B C A J)
      )
      (diff_new3 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)
        (new120 H A)
        (new121 G B C)
      )
      (diff_new3 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)
        (new120 I A)
        (new123 H D B C)
      )
      (diff_new3 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)
        (new108 K A H)
        (new125 J G B C)
      )
      (diff_new3 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)
        (new120 K A)
        (new125 J I B C)
      )
      (diff_new3 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)
        (new120 K A)
        (new125 J H B C)
      )
      (diff_new3 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_new132 M J D H)
        (new108 K D I)
        (diff_new3 A B C M)
      )
      (diff_new3 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)
        (new120 I D)
        (new134 H B C A)
      )
      (diff_new3 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_new137 K H D)
        (new135 I)
        (diff_new3 A B C K)
      )
      (diff_new3 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)
        (new138 K H)
        (new139 J G B C A)
      )
      (diff_new3 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)
        (new135 K)
        (new139 J I B C A)
      )
      (diff_new3 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)
        (new135 K)
        (new139 J H B C A)
      )
      (diff_new3 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)
        (new108 L D H)
        (new145 K D J B C G)
      )
      (diff_new3 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)
        (new108 K D H)
        (new147 J B C G)
      )
      (diff_new3 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)
        (new138 K H)
        (new149 J D B C G)
      )
      (diff_new3 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)
        (new138 L H)
        (new151 K G B C I)
      )
      (diff_new3 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)
        (new138 M H)
        (new151 L K B C G)
      )
      (diff_new3 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)
        (new138 M H)
        (new151 L J B C G)
      )
      (diff_new3 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)
        (new108 M D K)
        (new145 L D J B C I)
      )
      (diff_new3 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)
        (new120 K D)
        (new147 J B C I)
      )
      (diff_new3 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)
        (new135 K)
        (new149 J D B C I)
      )
      (diff_new3 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)
        (new138 M H)
        (new151 L G B C K)
      )
      (diff_new3 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)
        (new135 M)
        (new151 L K B C I)
      )
      (diff_new3 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)
        (new135 M)
        (new151 L H B C K)
      )
      (diff_new3 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)
        (new108 M D K)
        (new145 L D J B C H)
      )
      (diff_new3 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)
        (new120 K D)
        (new147 J B C H)
      )
      (diff_new3 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)
        (new135 K)
        (new149 J D B C H)
      )
      (diff_new3 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)
        (new138 M J)
        (new151 L I B C H)
      )
      (diff_new3 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)
        (new135 M)
        (new151 L K B C H)
      )
      (diff_new3 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)
        (new135 M)
        (new151 L J B C H)
      )
      (diff_new3 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_new110 N F A K I)
        (diff_new3 A B C N)
        (new108 G A J)
      )
      (diff_new3 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_new113 N G D J)
        (diff_new3 A B C N)
        (new108 H A K)
      )
      (diff_new3 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)
        (new115 I H B C A L)
        (new108 J A G)
      )
      (diff_new3 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)
        (new188 G B C A L)
        (new108 H A K)
      )
      (diff_new3 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)
        (new188 G B C A L)
        (new108 H A J)
      )
      (diff_new3 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)
        (new123 G D B C)
        (new120 H A)
      )
      (diff_new3 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)
        (new121 F B C)
        (new120 G A)
      )
      (diff_new3 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)
        (new125 I H B C)
        (new108 J A G)
      )
      (diff_new3 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)
        (new121 G B C)
        (new108 H A K)
      )
      (diff_new3 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)
        (new121 G B C)
        (new108 H A J)
      )
      (diff_new3 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_new132 M G D K)
        (diff_new3 A B C M)
        (new108 H D J)
      )
      (diff_new3 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_new137 K G D)
        (diff_new3 A B C K)
        (new135 H)
      )
      (diff_new3 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)
        (new134 G B C A)
        (new120 H D)
      )
      (diff_new3 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)
        (new139 I H B C A)
        (new138 J G)
      )
      (diff_new3 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)
        (new134 G B C A)
        (new138 H K)
      )
      (diff_new3 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)
        (new134 G B C A)
        (new138 H J)
      )
      (diff_new3 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)
        (new145 I D L B C G)
        (new108 J D H)
      )
      (diff_new3 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)
        (new149 I D B C G)
        (new138 J H)
      )
      (diff_new3 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)
        (new147 I B C G)
        (new108 J D H)
      )
      (diff_new3 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)
        (new151 J H B C I)
        (new138 K G)
      )
      (diff_new3 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)
        (new147 I B C G)
        (new138 J H)
      )
      (diff_new3 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)
        (new147 I B C G)
        (new138 J H)
      )
      (diff_new3 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)
        (new145 G D M B C K)
        (new108 H D L)
      )
      (diff_new3 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)
        (new149 G D B C K)
        (new135 H)
      )
      (diff_new3 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)
        (new147 G B C K)
        (new120 H D)
      )
      (diff_new3 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)
        (new151 I H B C M)
        (new138 J G)
      )
      (diff_new3 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)
        (new147 G B C K)
        (new138 H M)
      )
      (diff_new3 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)
        (new147 G B C M)
        (new138 H J)
      )
      (diff_new3 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)
        (new145 I D M B C H)
        (new108 J D L)
      )
      (diff_new3 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)
        (new149 I D B C H)
        (new135 J)
      )
      (diff_new3 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)
        (new147 I B C H)
        (new120 J D)
      )
      (diff_new3 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)
        (new151 K J B C H)
        (new138 L I)
      )
      (diff_new3 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)
        (new147 I B C H)
        (new138 J M)
      )
      (diff_new3 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)
        (new147 I B C H)
        (new138 J L)
      )
      (diff_new3 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A true)
      (new1 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= B 1)
        (diff_new3 C B D A)
        (new1 C)
      )
      (new1 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (and
        (= A false)
        (new1 A)
      )
      ff
    )
  )
)

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