; Automatically generated by map2smt

(set-logic HORN)




(declare-fun new90 (Int Int Int Int Int Int) Bool)
(declare-fun new89 (Int Int Int) Bool)
(declare-fun new86 (Int Int) Bool)
(declare-fun new85 (Int Int Int Int Int) Bool)
(declare-fun new84 (Int Bool Int) Bool)
(declare-fun new81 (Int Bool Int Int) Bool)
(declare-fun new8 (Int) Bool)
(declare-fun new7 (Bool Int) Bool)
(declare-fun new63 (Int Int) Bool)
(declare-fun new60 (Int) Bool)
(declare-fun new59 (Bool Int) Bool)
(declare-fun new57 (Bool Int Int) Bool)
(declare-fun new5 (Bool Int Int) Bool)
(declare-fun new4 (Int Int Int Bool Int) Bool)
(declare-fun new38 (Int Int Int Int Int Int) Bool)
(declare-fun new37 (Int Int Int) Bool)
(declare-fun new361 (Int) Bool)
(declare-fun new357 (Bool) Bool)
(declare-fun new353 (Bool Int) Bool)
(declare-fun new34 (Int Int) Bool)
(declare-fun new33 (Int Int Int Int Int) Bool)
(declare-fun new32 (Int Bool Int) Bool)
(declare-fun new3 (Int Int Int Bool Int) Bool)
(declare-fun new29 (Int Bool Int Int) Bool)
(declare-fun new2 (Int Int Int Bool) Bool)
(declare-fun new127 (Int) Bool)
(declare-fun new123 (Bool) Bool)
(declare-fun new119 (Bool Int) Bool)
(declare-fun new11 (Int Int) Bool)
(declare-fun new1 (Int Int Int Bool) Bool)
(declare-fun diff_new88 (Bool Int Bool) Bool)
(declare-fun diff_new83 (Bool Int Bool Int) Bool)
(declare-fun diff_new36 (Bool Int Bool) Bool)
(declare-fun diff_new31 (Bool Int Bool Int) Bool)
(declare-fun not_fun_diff_new88 () Bool)
(declare-fun constr (Bool) Bool)
(declare-fun not_fun_diff_new83 () Bool)
(declare-fun not_fun_diff_new36 () Bool)
(declare-fun not_fun_diff_new31 () Bool)
(declare-fun ff () Bool)

(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Bool) )
    (=>
      (and
        (diff_new88 A B C)
        (diff_new88 D E F)
        (and (= A D) (or (not (= B E)) (not (= C F))))
      )
      not_fun_diff_new88
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Bool) (F Int) (G Bool) (H Int) )
    (=>
      (and
        (diff_new83 A B C D)
        (diff_new83 E F G H)
        (and (= A E) (or (not (= B F)) (or (not (= C G)) (not (= D H)))))
      )
      not_fun_diff_new83
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Bool) )
    (=>
      (and
        (diff_new36 A B C)
        (diff_new36 D E F)
        (and (= A D) (or (not (= B E)) (not (= C F))))
      )
      not_fun_diff_new36
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Bool) (F Int) (G Bool) (H Int) )
    (=>
      (and
        (diff_new31 A B C D)
        (diff_new31 E F G H)
        (and (= A E) (or (not (= B F)) (or (not (= C G)) (not (= D H)))))
      )
      not_fun_diff_new31
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new361 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= A (+ 1 B))
        (new361 B)
      )
      (new361 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A true)
      (new357 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (<= B C)
        (= D (+ 1 B))
        (new353 A C)
        (new353 A B)
      )
      (new357 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (and
        (= A false)
        (new357 A)
      )
      (new357 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (and
        (= A false)
        (new357 A)
      )
      (new357 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= B (+ C 1))
        (new361 C)
        (new361 B)
      )
      (new357 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (<= (+ B 1) (+ 1 C))
        (new361 C)
      )
      (new357 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (>= B (+ (+ 1 C) 1))
        (new361 C)
      )
      (new357 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A true)
        (= B 0)
      )
      (new353 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))
        (new353 A D)
        (new353 A C)
      )
      (new353 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= B (+ 1 C))
        (new361 C)
        (new357 A)
      )
      (new353 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= B (+ 1 C))
        (new353 A C)
      )
      (new353 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= C (+ D 1))
        (= B (+ 1 C))
        (new361 D)
        (new361 C)
      )
      (new353 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (<= (+ C 1) (+ 1 D))
        (= B (+ 1 D))
        (new361 D)
      )
      (new353 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (>= C (+ (+ 1 D) 1))
        (= B (+ 1 D))
        (new361 D)
      )
      (new353 A B)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new127 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= A (+ 1 B))
        (new127 B)
      )
      (new127 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A true)
      (new123 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (<= B C)
        (= D (+ 1 B))
        (new119 A C)
        (new119 A B)
      )
      (new123 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (and
        (= A false)
        (new123 A)
      )
      (new123 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (and
        (= A false)
        (new123 A)
      )
      (new123 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= B (+ C 1))
        (new127 C)
        (new127 B)
      )
      (new123 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (<= (+ B 1) (+ 1 C))
        (new127 C)
      )
      (new123 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (>= B (+ (+ 1 C) 1))
        (new127 C)
      )
      (new123 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A true)
        (= B 0)
      )
      (new119 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))
        (new119 A D)
        (new119 A C)
      )
      (new119 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= B (+ 1 C))
        (new127 C)
        (new123 A)
      )
      (new119 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (= B (+ 1 C))
        (new119 A C)
      )
      (new119 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= C (+ D 1))
        (= B (+ 1 C))
        (new127 D)
        (new127 C)
      )
      (new119 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (<= (+ C 1) (+ 1 D))
        (= B (+ 1 D))
        (new127 D)
      )
      (new119 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (>= C (+ (+ 1 D) 1))
        (= B (+ 1 D))
        (new127 D)
      )
      (new119 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (>= F 0)
        (>= G 0)
        (= F 0)
        (= G 0)
        (= H (+ G F))
        (= E 0)
        (= D 0)
        (= A 1)
        (= B (+ 1 H))
      )
      (new90 A B A C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (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) (S Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (>= I 0)
        (>= J 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= L 0)
        (<= M (- D 1))
        (<= N O)
        (= P (+ J I))
        (= O 0)
        (= A (+ 1 N))
        (= K (+ 1 P))
        (= L 0)
        (= Q (+ J I))
        (= R (+ L K))
        (= F (+ 1 S))
        (= E (+ 1 Q))
        (= C 1)
        (= B (+ 1 R))
        (new63 S I)
        (new60 J)
      )
      (new90 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (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) (S Int) (T Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (>= I 0)
        (>= J 0)
        (>= K (+ L 1))
        (>= I 0)
        (>= J 0)
        (>= M 0)
        (>= N 0)
        (<= O (- D 1))
        (= P (+ J I))
        (= L 0)
        (= Q 0)
        (= A (+ 1 Q))
        (= M 0)
        (= N (+ 1 P))
        (= R (+ J I))
        (= S (+ N M))
        (= F (+ 1 T))
        (= E (+ 1 R))
        (= C 1)
        (= B (+ 1 S))
        (new63 T I)
        (new60 J)
      )
      (new90 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (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 false)
        (>= I D)
        (>= J 0)
        (>= K 0)
        (>= L 0)
        (>= K 0)
        (<= M N)
        (= A (+ 1 M))
        (= O (+ K J))
        (= P (+ K L))
        (= F (+ 1 Q))
        (= E (+ 1 O))
        (= C 1)
        (= B (+ 1 P))
        (new86 N K)
        (new90 M L C D J Q)
      )
      (new90 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (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 false)
        (= H false)
        (>= I (+ J 1))
        (>= K D)
        (>= L 0)
        (>= M 0)
        (>= M 0)
        (>= N 0)
        (= A (+ 1 J))
        (= O (+ M L))
        (= P (+ N M))
        (= F (+ 1 Q))
        (= E (+ 1 O))
        (= C 1)
        (= B (+ 1 P))
        (new90 I N C D L Q)
        (new86 J M)
      )
      (new90 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (and
        (= C 0)
        (= B 0)
        (= A 0)
      )
      (new89 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= C (+ 1 F))
        (= B (+ 1 G))
        (new63 G D)
        (new60 E)
      )
      (new89 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= B 0)
        (= A 0)
      )
      (new86 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (new60 D)
        (new60 C)
      )
      (new86 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= A true)
        (= B 0)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= A true)
      )
      (diff_new88 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 0)
        (new119 A D)
        (new119 A C)
      )
      (diff_new88 A B A)
    )
  )
)
(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))
        (new119 A D)
        (new119 A C)
      )
      (diff_new88 A B A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= B 0)
        (new123 A)
      )
      (diff_new88 A B A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
        (= B 0)
        (new123 C)
        (new123 A)
      )
      (diff_new88 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 0)
        (new119 A E)
        (new127 D)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= B 0)
        (new127 E)
        (new123 A)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= B 0)
        (new127 E)
        (new123 A)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (new123 A)
      )
      (diff_new88 A B A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
        (new123 C)
        (new123 A)
      )
      (diff_new88 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))
        (new119 A E)
        (new127 D)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (new127 E)
        (new123 A)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (new127 E)
        (new123 A)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
        (= B 0)
        (new123 C)
        (new123 A)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= B 0)
        (new123 A)
      )
      (diff_new88 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))
        (= B 0)
        (new127 E)
        (new119 A D)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= B 0)
        (new119 A E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= B 0)
        (new119 A E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
        (new123 C)
        (new123 A)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (new123 A)
      )
      (diff_new88 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))
        (new127 E)
        (new119 A D)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (new119 A E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (new119 A E)
      )
      (diff_new88 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 0)
        (new119 C E)
        (new127 D)
      )
      (diff_new88 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 0)
        (new119 C D)
        (new127 E)
      )
      (diff_new88 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))
        (= B 0)
        (new127 E)
        (new127 D)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (<= (+ F 1) (+ 1 D))
        (= B 0)
        (new127 E)
        (new127 D)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (= B 0)
        (new127 F)
        (new127 E)
      )
      (diff_new88 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))
        (new119 C E)
        (new127 D)
      )
      (diff_new88 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))
        (new119 C D)
        (new127 E)
      )
      (diff_new88 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))
        (new127 E)
        (new127 D)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (<= (+ F 1) (+ 1 D))
        (new127 E)
        (new127 D)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (new127 F)
        (new127 E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= B 0)
        (new123 C)
        (new127 E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= B 0)
        (new119 C E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (<= (+ F 1) (+ 1 D))
        (= B 0)
        (new127 E)
        (new127 D)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= B 0)
        (new127 E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (new123 C)
        (new127 E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (new119 C E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (<= (+ F 1) (+ 1 D))
        (new127 E)
        (new127 D)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (new127 E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= B 0)
        (new123 C)
        (new127 E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= B 0)
        (new119 C E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (= B 0)
        (new127 F)
        (new127 E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= B 0)
        (new127 E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (new123 C)
        (new127 E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (new119 C E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (new127 F)
        (new127 E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (new127 E)
      )
      (diff_new88 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (>= E 0)
        (>= F 0)
        (= E 0)
        (= F 0)
        (= G (+ F E))
        (= D 0)
        (= A 1)
        (= B (+ 1 G))
      )
      (new85 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) (M Int) (N Int) (O Int) (P Int) (Q Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (>= H 0)
        (>= I 0)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (<= L (- D 1))
        (<= M N)
        (= O (+ I H))
        (= N 0)
        (= A (+ 1 M))
        (= J (+ 1 O))
        (= K 0)
        (= P (+ I H))
        (= Q (+ K J))
        (= E (+ 1 P))
        (= C 1)
        (= B (+ 1 Q))
        (new60 I)
        (new60 H)
      )
      (new85 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= H 0)
        (>= I 0)
        (>= L 0)
        (>= M 0)
        (<= N (- D 1))
        (= O (+ I H))
        (= K 0)
        (= P 0)
        (= A (+ 1 P))
        (= L 0)
        (= M (+ 1 O))
        (= Q (+ I H))
        (= R (+ M L))
        (= E (+ 1 Q))
        (= C 1)
        (= B (+ 1 R))
        (new60 I)
        (new60 H)
      )
      (new85 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) (N Int) (O Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (>= H D)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= J 0)
        (<= L M)
        (= A (+ 1 L))
        (= N (+ J I))
        (= O (+ J K))
        (= E (+ 1 N))
        (= C 1)
        (= B (+ 1 O))
        (new86 M J)
        (new85 L K C D I)
      )
      (new85 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) (N Int) (O Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (>= H (+ I 1))
        (>= J D)
        (>= K 0)
        (>= L 0)
        (>= L 0)
        (>= M 0)
        (= A (+ 1 I))
        (= N (+ L K))
        (= O (+ M L))
        (= E (+ 1 N))
        (= C 1)
        (= B (+ 1 O))
        (new85 H M C D K)
        (new86 I L)
      )
      (new85 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (= C 0)
        (= A 0)
      )
      (new84 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= D 0)
        (>= E 0)
        (<= F G)
        (= A (+ 1 F))
        (= H (+ E D))
        (= C (+ 1 H))
        (new57 B G E)
        (new57 B F D)
      )
      (new84 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= B false)
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= C (+ 1 F))
        (new59 B E)
        (new60 D)
      )
      (new84 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= B false)
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= C (+ 1 F))
        (new60 E)
        (new59 B D)
      )
      (new84 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= D (+ E 1))
        (>= F 0)
        (>= G 0)
        (= H (+ G F))
        (= C (+ 1 H))
        (new63 E G)
        (new63 D F)
      )
      (new84 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= B false)
        (>= D 0)
        (>= E 0)
        (<= (+ A 1) (+ 1 F))
        (= G (+ E D))
        (= C (+ 1 G))
        (new60 E)
        (new63 F D)
      )
      (new84 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= B false)
        (>= A (+ (+ 1 D) 1))
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= C (+ 1 G))
        (new60 F)
        (new63 D E)
      )
      (new84 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= D 0)
        (= C 0)
        (= A 0)
      )
      (new81 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= E 0)
        (>= F 0)
        (<= G H)
        (= A (+ 1 G))
        (= I (+ F E))
        (= D (+ 1 I))
        (= C (+ 1 G))
        (new57 B H F)
        (new57 B G E)
      )
      (new81 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= B false)
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= D (+ 1 G))
        (= C (+ 1 H))
        (new59 B F)
        (new63 H E)
      )
      (new81 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= B false)
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= D (+ 1 G))
        (= C (+ 1 H))
        (new60 F)
        (new57 B H E)
      )
      (new81 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 false)
        (= B false)
        (>= E (+ F 1))
        (>= G 0)
        (>= H 0)
        (= I (+ H G))
        (= D (+ 1 I))
        (= C (+ 1 E))
        (new63 F H)
        (new63 E G)
      )
      (new81 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= B false)
        (>= E 0)
        (>= F 0)
        (<= (+ A 1) (+ 1 G))
        (= H (+ F E))
        (= D (+ 1 H))
        (= C (+ 1 G))
        (new60 F)
        (new63 G E)
      )
      (new81 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= B false)
        (>= A (+ (+ 1 E) 1))
        (>= F 0)
        (>= G 0)
        (= H (+ G F))
        (= D (+ 1 H))
        (= C (+ 1 E))
        (new60 G)
        (new63 E F)
      )
      (new81 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= A true)
        (= D 0)
        (= B 0)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= A true)
        (= D 0)
      )
      (diff_new83 A B C D)
    )
  )
)
(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)
        (= F (+ 1 D))
        (= C (+ 1 D))
        (= B 0)
        (new119 A E)
        (new119 A D)
      )
      (diff_new83 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)
        (= F (+ 1 D))
        (= C (+ 1 D))
        (new119 A E)
        (new119 A D)
      )
      (diff_new83 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (= B 0)
        (new127 D)
        (new123 A)
      )
      (diff_new83 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (= B 0)
        (new119 C E)
        (new123 A)
      )
      (diff_new83 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))
        (= B 0)
        (new119 A F)
        (new127 E)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (= B 0)
        (new127 F)
        (new123 A)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (= B 0)
        (new127 F)
        (new123 A)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (new127 D)
        (new123 A)
      )
      (diff_new83 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (new119 C E)
        (new123 A)
      )
      (diff_new83 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))
        (new119 A F)
        (new127 E)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (new127 F)
        (new123 A)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (new127 F)
        (new123 A)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (= B 0)
        (new123 C)
        (new119 A E)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (= B 0)
        (new119 A D)
      )
      (diff_new83 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))
        (= B 0)
        (new127 F)
        (new119 A E)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (= B 0)
        (new119 A F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (= B 0)
        (new119 A F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (new123 C)
        (new119 A E)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (new119 A D)
      )
      (diff_new83 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))
        (new127 F)
        (new119 A E)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (new119 A F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (new119 A F)
      )
      (diff_new83 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))
        (= B 0)
        (new119 C F)
        (new127 E)
      )
      (diff_new83 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))
        (= B 0)
        (new119 C E)
        (new127 F)
      )
      (diff_new83 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))
        (= B 0)
        (new127 F)
        (new127 E)
      )
      (diff_new83 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))
        (<= (+ G 1) (+ 1 E))
        (= D (+ 1 E))
        (= B 0)
        (new127 F)
        (new127 E)
      )
      (diff_new83 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 (+ (+ 1 F) 1))
        (>= F (+ G 1))
        (= D (+ 1 F))
        (= B 0)
        (new127 G)
        (new127 F)
      )
      (diff_new83 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))
        (new119 C F)
        (new127 E)
      )
      (diff_new83 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))
        (new119 C E)
        (new127 F)
      )
      (diff_new83 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))
        (new127 F)
        (new127 E)
      )
      (diff_new83 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))
        (<= (+ G 1) (+ 1 E))
        (= D (+ 1 E))
        (new127 F)
        (new127 E)
      )
      (diff_new83 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 (+ (+ 1 F) 1))
        (>= F (+ G 1))
        (= D (+ 1 F))
        (new127 G)
        (new127 F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (= B 0)
        (new123 C)
        (new127 F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (= B 0)
        (new119 C F)
      )
      (diff_new83 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))
        (<= (+ G 1) (+ 1 E))
        (= D (+ 1 E))
        (= B 0)
        (new127 F)
        (new127 E)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (= B 0)
        (new127 F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (new123 C)
        (new127 F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (new119 C F)
      )
      (diff_new83 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))
        (<= (+ G 1) (+ 1 E))
        (= D (+ 1 E))
        (new127 F)
        (new127 E)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (new127 F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (= B 0)
        (new123 C)
        (new127 F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (= B 0)
        (new119 C F)
      )
      (diff_new83 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 (+ (+ 1 F) 1))
        (>= F (+ G 1))
        (= D (+ 1 F))
        (= B 0)
        (new127 G)
        (new127 F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (= B 0)
        (new127 F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (new123 C)
        (new127 F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (new119 C F)
      )
      (diff_new83 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 (+ (+ 1 F) 1))
        (>= F (+ G 1))
        (= D (+ 1 F))
        (new127 G)
        (new127 F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (new127 F)
      )
      (diff_new83 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= B 0)
        (= A 0)
      )
      (new63 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (= A (+ 1 F))
        (new63 F C)
        (new60 D)
      )
      (new63 A B)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new60 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) )
    (=>
      (and
        (>= B 0)
        (>= C 0)
        (= D (+ B C))
        (= A (+ 1 D))
        (new60 B)
        (new60 C)
      )
      (new60 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A true)
        (= B 0)
      )
      (new59 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= C 0)
        (>= D 0)
        (<= E F)
        (= G (+ 1 E))
        (= H (+ D C))
        (= B (+ 1 H))
        (new57 A F D)
        (new57 A E C)
      )
      (new59 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (new59 A D)
        (new60 C)
      )
      (new59 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (new60 D)
        (new59 A C)
      )
      (new59 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= C (+ D 1))
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= B (+ 1 G))
        (new63 D F)
        (new63 C E)
      )
      (new59 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (>= C 0)
        (>= D 0)
        (<= (+ E 1) (+ 1 F))
        (= G (+ D C))
        (= B (+ 1 G))
        (new60 D)
        (new63 F C)
      )
      (new59 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (>= C (+ (+ 1 D) 1))
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= B (+ 1 G))
        (new60 F)
        (new63 D E)
      )
      (new59 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A true)
        (= C 0)
        (= B 0)
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= D 0)
        (>= E 0)
        (<= F G)
        (= H (+ 1 F))
        (= I (+ E D))
        (= C (+ 1 I))
        (= B (+ 1 F))
        (new57 A G E)
        (new57 A F D)
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= C (+ 1 F))
        (= B (+ 1 G))
        (new59 A E)
        (new63 G D)
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= C (+ 1 F))
        (= B (+ 1 G))
        (new60 E)
        (new57 A G D)
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= D (+ E 1))
        (>= F 0)
        (>= G 0)
        (= H (+ G F))
        (= C (+ 1 H))
        (= B (+ 1 D))
        (new63 E G)
        (new63 D F)
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A false)
        (>= D 0)
        (>= E 0)
        (<= (+ F 1) (+ 1 G))
        (= H (+ E D))
        (= C (+ 1 H))
        (= B (+ 1 G))
        (new60 E)
        (new63 G D)
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (>= F 0)
        (>= G 0)
        (= H (+ G F))
        (= C (+ 1 H))
        (= B (+ 1 E))
        (new60 G)
        (new63 E F)
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (>= F 0)
        (>= G 0)
        (= F 0)
        (= G 0)
        (= H (+ G F))
        (= E 0)
        (= D 0)
        (= A 1)
        (= B (+ 1 H))
      )
      (new38 A B A C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (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) (S Int) )
    (=>
      (and
        (= G true)
        (= H true)
        (>= I 0)
        (>= J 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= L 0)
        (<= M (- D 1))
        (<= N O)
        (= P (+ J I))
        (= O 0)
        (= A (+ 1 N))
        (= K (+ 1 P))
        (= L 0)
        (= Q (+ J I))
        (= R (+ L K))
        (= F (+ 1 S))
        (= E (+ 1 Q))
        (= C 1)
        (= B (+ 1 R))
        (new11 S I)
        (new8 J)
      )
      (new38 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (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) (S Int) (T Int) )
    (=>
      (and
        (= G false)
        (= H true)
        (>= I 0)
        (>= J 0)
        (>= K (+ L 1))
        (>= I 0)
        (>= J 0)
        (>= M 0)
        (>= N 0)
        (<= O (- D 1))
        (= P (+ J I))
        (= L 0)
        (= Q 0)
        (= A (+ 1 Q))
        (= M 0)
        (= N (+ 1 P))
        (= R (+ J I))
        (= S (+ N M))
        (= F (+ 1 T))
        (= E (+ 1 R))
        (= C 1)
        (= B (+ 1 S))
        (new11 T I)
        (new8 J)
      )
      (new38 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (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 false)
        (>= I D)
        (>= J 0)
        (>= K 0)
        (>= L 0)
        (>= K 0)
        (<= M N)
        (= A (+ 1 M))
        (= O (+ K J))
        (= P (+ K L))
        (= F (+ 1 Q))
        (= E (+ 1 O))
        (= C 1)
        (= B (+ 1 P))
        (new34 N K)
        (new38 M L C D J Q)
      )
      (new38 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (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 false)
        (= H false)
        (>= I (+ J 1))
        (>= K D)
        (>= L 0)
        (>= M 0)
        (>= M 0)
        (>= N 0)
        (= A (+ 1 J))
        (= O (+ M L))
        (= P (+ N M))
        (= F (+ 1 Q))
        (= E (+ 1 O))
        (= C 1)
        (= B (+ 1 P))
        (new38 I N C D L Q)
        (new34 J M)
      )
      (new38 A B C D E F)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (and
        (= C 0)
        (= B 0)
        (= A 0)
      )
      (new37 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= C (+ 1 F))
        (= B (+ 1 G))
        (new11 G D)
        (new8 E)
      )
      (new37 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= B 0)
        (= A 0)
      )
      (new34 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (new8 D)
        (new8 C)
      )
      (new34 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= A true)
        (= B 0)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (= A true)
      )
      (diff_new36 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 0)
        (new353 A D)
        (new353 A C)
      )
      (diff_new36 A B A)
    )
  )
)
(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))
        (new353 A D)
        (new353 A C)
      )
      (diff_new36 A B A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= B 0)
        (new357 A)
      )
      (diff_new36 A B A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
        (= B 0)
        (new357 C)
        (new357 A)
      )
      (diff_new36 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 0)
        (new353 A E)
        (new361 D)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= B 0)
        (new361 E)
        (new357 A)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= B 0)
        (new361 E)
        (new357 A)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (new357 A)
      )
      (diff_new36 A B A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
        (new357 C)
        (new357 A)
      )
      (diff_new36 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))
        (new353 A E)
        (new361 D)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (new361 E)
        (new357 A)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (new361 E)
        (new357 A)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
        (= B 0)
        (new357 C)
        (new357 A)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= B 0)
        (new357 A)
      )
      (diff_new36 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))
        (= B 0)
        (new361 E)
        (new353 A D)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= B 0)
        (new353 A E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= B 0)
        (new353 A E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
        (new357 C)
        (new357 A)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (new357 A)
      )
      (diff_new36 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))
        (new361 E)
        (new353 A D)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (new353 A E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (new353 A E)
      )
      (diff_new36 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 0)
        (new353 C E)
        (new361 D)
      )
      (diff_new36 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 0)
        (new353 C D)
        (new361 E)
      )
      (diff_new36 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))
        (= B 0)
        (new361 E)
        (new361 D)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (<= (+ F 1) (+ 1 D))
        (= B 0)
        (new361 E)
        (new361 D)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (= B 0)
        (new361 F)
        (new361 E)
      )
      (diff_new36 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))
        (new353 C E)
        (new361 D)
      )
      (diff_new36 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))
        (new353 C D)
        (new361 E)
      )
      (diff_new36 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))
        (new361 E)
        (new361 D)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (<= (+ F 1) (+ 1 D))
        (new361 E)
        (new361 D)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= A false)
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (new361 F)
        (new361 E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= B 0)
        (new357 C)
        (new361 E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= B 0)
        (new353 C E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (<= (+ F 1) (+ 1 D))
        (= B 0)
        (new361 E)
        (new361 D)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (= B 0)
        (new361 E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (new357 C)
        (new361 E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (new353 C E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= D (+ E 1))
        (<= (+ F 1) (+ 1 D))
        (new361 E)
        (new361 D)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ D 1) (+ 1 E))
        (new361 E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= B 0)
        (new357 C)
        (new361 E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= B 0)
        (new353 C E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (= B 0)
        (new361 F)
        (new361 E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (= B 0)
        (new361 E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (new357 C)
        (new361 E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (new353 C E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (>= E (+ F 1))
        (new361 F)
        (new361 E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (new361 E)
      )
      (diff_new36 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (>= E 0)
        (>= F 0)
        (= E 0)
        (= F 0)
        (= G (+ F E))
        (= D 0)
        (= A 1)
        (= B (+ 1 G))
      )
      (new33 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) (M Int) (N Int) (O Int) (P Int) (Q Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (>= H 0)
        (>= I 0)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (<= L (- D 1))
        (<= M N)
        (= O (+ I H))
        (= N 0)
        (= A (+ 1 M))
        (= J (+ 1 O))
        (= K 0)
        (= P (+ I H))
        (= Q (+ K J))
        (= E (+ 1 P))
        (= C 1)
        (= B (+ 1 Q))
        (new8 I)
        (new8 H)
      )
      (new33 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= H 0)
        (>= I 0)
        (>= L 0)
        (>= M 0)
        (<= N (- D 1))
        (= O (+ I H))
        (= K 0)
        (= P 0)
        (= A (+ 1 P))
        (= L 0)
        (= M (+ 1 O))
        (= Q (+ I H))
        (= R (+ M L))
        (= E (+ 1 Q))
        (= C 1)
        (= B (+ 1 R))
        (new8 I)
        (new8 H)
      )
      (new33 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) (N Int) (O Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (>= H D)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= J 0)
        (<= L M)
        (= A (+ 1 L))
        (= N (+ J I))
        (= O (+ J K))
        (= E (+ 1 N))
        (= C 1)
        (= B (+ 1 O))
        (new34 M J)
        (new33 L K C D I)
      )
      (new33 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) (N Int) (O Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (>= H (+ I 1))
        (>= J D)
        (>= K 0)
        (>= L 0)
        (>= L 0)
        (>= M 0)
        (= A (+ 1 I))
        (= N (+ L K))
        (= O (+ M L))
        (= E (+ 1 N))
        (= C 1)
        (= B (+ 1 O))
        (new33 H M C D K)
        (new34 I L)
      )
      (new33 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (= C 0)
        (= A 0)
      )
      (new32 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= D 0)
        (>= E 0)
        (<= F G)
        (= A (+ 1 F))
        (= H (+ E D))
        (= C (+ 1 H))
        (new5 B G E)
        (new5 B F D)
      )
      (new32 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= B false)
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= C (+ 1 F))
        (new7 B E)
        (new8 D)
      )
      (new32 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= B false)
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= C (+ 1 F))
        (new8 E)
        (new7 B D)
      )
      (new32 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= D (+ E 1))
        (>= F 0)
        (>= G 0)
        (= H (+ G F))
        (= C (+ 1 H))
        (new11 E G)
        (new11 D F)
      )
      (new32 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= B false)
        (>= D 0)
        (>= E 0)
        (<= (+ A 1) (+ 1 F))
        (= G (+ E D))
        (= C (+ 1 G))
        (new8 E)
        (new11 F D)
      )
      (new32 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= B false)
        (>= A (+ (+ 1 D) 1))
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= C (+ 1 G))
        (new8 F)
        (new11 D E)
      )
      (new32 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= D 0)
        (= C 0)
        (= A 0)
      )
      (new29 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= E 0)
        (>= F 0)
        (<= G H)
        (= A (+ 1 G))
        (= I (+ F E))
        (= D (+ 1 I))
        (= C (+ 1 G))
        (new5 B H F)
        (new5 B G E)
      )
      (new29 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= B false)
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= D (+ 1 G))
        (= C (+ 1 H))
        (new7 B F)
        (new11 H E)
      )
      (new29 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= B false)
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= D (+ 1 G))
        (= C (+ 1 H))
        (new8 F)
        (new5 B H E)
      )
      (new29 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 false)
        (= B false)
        (>= E (+ F 1))
        (>= G 0)
        (>= H 0)
        (= I (+ H G))
        (= D (+ 1 I))
        (= C (+ 1 E))
        (new11 F H)
        (new11 E G)
      )
      (new29 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= B false)
        (>= E 0)
        (>= F 0)
        (<= (+ A 1) (+ 1 G))
        (= H (+ F E))
        (= D (+ 1 H))
        (= C (+ 1 G))
        (new8 F)
        (new11 G E)
      )
      (new29 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= B false)
        (>= A (+ (+ 1 E) 1))
        (>= F 0)
        (>= G 0)
        (= H (+ G F))
        (= D (+ 1 H))
        (= C (+ 1 E))
        (new8 G)
        (new11 E F)
      )
      (new29 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= A true)
        (= D 0)
        (= B 0)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= A true)
        (= D 0)
      )
      (diff_new31 A B C D)
    )
  )
)
(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)
        (= F (+ 1 D))
        (= C (+ 1 D))
        (= B 0)
        (new353 A E)
        (new353 A D)
      )
      (diff_new31 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)
        (= F (+ 1 D))
        (= C (+ 1 D))
        (new353 A E)
        (new353 A D)
      )
      (diff_new31 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (= B 0)
        (new361 D)
        (new357 A)
      )
      (diff_new31 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (= B 0)
        (new353 C E)
        (new357 A)
      )
      (diff_new31 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))
        (= B 0)
        (new353 A F)
        (new361 E)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (= B 0)
        (new361 F)
        (new357 A)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (= B 0)
        (new361 F)
        (new357 A)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (new361 D)
        (new357 A)
      )
      (diff_new31 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (new353 C E)
        (new357 A)
      )
      (diff_new31 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))
        (new353 A F)
        (new361 E)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (new361 F)
        (new357 A)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (new361 F)
        (new357 A)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (= B 0)
        (new357 C)
        (new353 A E)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (= B 0)
        (new353 A D)
      )
      (diff_new31 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))
        (= B 0)
        (new361 F)
        (new353 A E)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (= B 0)
        (new353 A F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (= B 0)
        (new353 A F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (= D (+ 1 E))
        (new357 C)
        (new353 A E)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (= C (+ 1 D))
        (new353 A D)
      )
      (diff_new31 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))
        (new361 F)
        (new353 A E)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (new353 A F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (new353 A F)
      )
      (diff_new31 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))
        (= B 0)
        (new353 C F)
        (new361 E)
      )
      (diff_new31 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))
        (= B 0)
        (new353 C E)
        (new361 F)
      )
      (diff_new31 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))
        (= B 0)
        (new361 F)
        (new361 E)
      )
      (diff_new31 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))
        (<= (+ G 1) (+ 1 E))
        (= D (+ 1 E))
        (= B 0)
        (new361 F)
        (new361 E)
      )
      (diff_new31 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 (+ (+ 1 F) 1))
        (>= F (+ G 1))
        (= D (+ 1 F))
        (= B 0)
        (new361 G)
        (new361 F)
      )
      (diff_new31 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))
        (new353 C F)
        (new361 E)
      )
      (diff_new31 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))
        (new353 C E)
        (new361 F)
      )
      (diff_new31 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))
        (new361 F)
        (new361 E)
      )
      (diff_new31 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))
        (<= (+ G 1) (+ 1 E))
        (= D (+ 1 E))
        (new361 F)
        (new361 E)
      )
      (diff_new31 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 (+ (+ 1 F) 1))
        (>= F (+ G 1))
        (= D (+ 1 F))
        (new361 G)
        (new361 F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (= B 0)
        (new357 C)
        (new361 F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (= B 0)
        (new353 C F)
      )
      (diff_new31 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))
        (<= (+ G 1) (+ 1 E))
        (= D (+ 1 E))
        (= B 0)
        (new361 F)
        (new361 E)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (= B 0)
        (new361 F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (new357 C)
        (new361 F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (new353 C F)
      )
      (diff_new31 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))
        (<= (+ G 1) (+ 1 E))
        (= D (+ 1 E))
        (new361 F)
        (new361 E)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (+ E 1) (+ 1 F))
        (= D (+ 1 F))
        (new361 F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (= B 0)
        (new357 C)
        (new361 F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (= B 0)
        (new353 C F)
      )
      (diff_new31 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 (+ (+ 1 F) 1))
        (>= F (+ G 1))
        (= D (+ 1 F))
        (= B 0)
        (new361 G)
        (new361 F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (= B 0)
        (new361 F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (new357 C)
        (new361 F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (new353 C F)
      )
      (diff_new31 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 (+ (+ 1 F) 1))
        (>= F (+ G 1))
        (= D (+ 1 F))
        (new361 G)
        (new361 F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= E (+ (+ 1 F) 1))
        (= D (+ 1 F))
        (new361 F)
      )
      (diff_new31 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= B 0)
        (= A 0)
      )
      (new11 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (= A (+ 1 F))
        (new11 F C)
        (new8 D)
      )
      (new11 A B)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new8 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) )
    (=>
      (and
        (>= B 0)
        (>= C 0)
        (= D (+ B C))
        (= A (+ 1 D))
        (new8 B)
        (new8 C)
      )
      (new8 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A true)
        (= B 0)
      )
      (new7 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= C 0)
        (>= D 0)
        (<= E F)
        (= G (+ 1 E))
        (= H (+ D C))
        (= B (+ 1 H))
        (new5 A F D)
        (new5 A E C)
      )
      (new7 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (new7 A D)
        (new8 C)
      )
      (new7 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (new8 D)
        (new7 A C)
      )
      (new7 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= C (+ D 1))
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= B (+ 1 G))
        (new11 D F)
        (new11 C E)
      )
      (new7 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (>= C 0)
        (>= D 0)
        (<= (+ E 1) (+ 1 F))
        (= G (+ D C))
        (= B (+ 1 G))
        (new8 D)
        (new11 F C)
      )
      (new7 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (>= C (+ (+ 1 D) 1))
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= B (+ 1 G))
        (new8 F)
        (new11 D E)
      )
      (new7 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A true)
        (= C 0)
        (= B 0)
      )
      (new5 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= A true)
        (= A true)
        (>= D 0)
        (>= E 0)
        (<= F G)
        (= H (+ 1 F))
        (= I (+ E D))
        (= C (+ 1 I))
        (= B (+ 1 F))
        (new5 A G E)
        (new5 A F D)
      )
      (new5 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= C (+ 1 F))
        (= B (+ 1 G))
        (new7 A E)
        (new11 G D)
      )
      (new5 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= C (+ 1 F))
        (= B (+ 1 G))
        (new8 E)
        (new5 A G D)
      )
      (new5 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= D (+ E 1))
        (>= F 0)
        (>= G 0)
        (= H (+ G F))
        (= C (+ 1 H))
        (= B (+ 1 D))
        (new11 E G)
        (new11 D F)
      )
      (new5 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A false)
        (>= D 0)
        (>= E 0)
        (<= (+ F 1) (+ 1 G))
        (= H (+ E D))
        (= C (+ 1 H))
        (= B (+ 1 G))
        (new8 E)
        (new11 G D)
      )
      (new5 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= A false)
        (>= D (+ (+ 1 E) 1))
        (>= F 0)
        (>= G 0)
        (= H (+ G F))
        (= C (+ 1 H))
        (= B (+ 1 E))
        (new8 G)
        (new11 E F)
      )
      (new5 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= D true)
        (>= F 0)
        (>= G 0)
        (= F 0)
        (= G 0)
        (= H (+ G F))
        (= E (+ 1 H))
        (= C 0)
        (= A 1)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D true)
        (= D true)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= H 0)
        (>= I 0)
        (<= L M)
        (<= N (- B 1))
        (<= O P)
        (= Q (+ I H))
        (= P 0)
        (= R (+ 1 O))
        (= O (+ 1 L))
        (= J (+ 1 Q))
        (= K 0)
        (= S (+ K J))
        (= T (+ I H))
        (= E (+ 1 S))
        (= C (+ 1 T))
        (= A 1)
        (new5 D M I)
        (new5 D L H)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= H 0)
        (>= I 0)
        (<= L (- B 1))
        (<= M N)
        (= O (+ I H))
        (= N 0)
        (= P (+ 1 M))
        (= J (+ 1 O))
        (= K 0)
        (= Q (+ K J))
        (= R (+ I H))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new7 D I)
        (new8 H)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= H 0)
        (>= I 0)
        (<= L (- B 1))
        (<= M N)
        (= O (+ I H))
        (= N 0)
        (= P (+ 1 M))
        (= J (+ 1 O))
        (= K 0)
        (= Q (+ K J))
        (= R (+ I H))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new7 D H)
        (new8 I)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= L 0)
        (>= M 0)
        (>= H 0)
        (>= I 0)
        (<= N (- B 1))
        (<= O P)
        (= Q (+ I H))
        (= P 0)
        (= R (+ 1 O))
        (= L (+ 1 Q))
        (= M 0)
        (= S (+ M L))
        (= T (+ I H))
        (= E (+ 1 S))
        (= C (+ 1 T))
        (= A 1)
        (new11 K I)
        (new11 J H)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= H 0)
        (>= I 0)
        (<= (+ L 1) (+ 1 M))
        (<= N (- B 1))
        (<= L O)
        (= P (+ I H))
        (= O 0)
        (= Q (+ 1 L))
        (= J (+ 1 P))
        (= K 0)
        (= R (+ K J))
        (= S (+ I H))
        (= E (+ 1 R))
        (= C (+ 1 S))
        (= A 1)
        (new11 M H)
        (new8 I)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ (+ 1 K) 1))
        (>= L 0)
        (>= M 0)
        (>= H 0)
        (>= I 0)
        (<= N (- B 1))
        (<= J O)
        (= P (+ I H))
        (= O 0)
        (= Q (+ 1 J))
        (= L (+ 1 P))
        (= M 0)
        (= R (+ M L))
        (= S (+ I H))
        (= E (+ 1 R))
        (= C (+ 1 S))
        (= A 1)
        (new11 K H)
        (new8 I)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D true)
        (= D true)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= L 0)
        (>= M 0)
        (>= H 0)
        (>= I 0)
        (<= N O)
        (<= P (- B 1))
        (= Q (+ I H))
        (= K 0)
        (= R 0)
        (= S (+ 1 R))
        (= J (+ 1 N))
        (= L 0)
        (= M (+ 1 Q))
        (= T (+ M L))
        (= U (+ I H))
        (= E (+ 1 T))
        (= C (+ 1 U))
        (= A 1)
        (new5 D O I)
        (new5 D N H)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= L 0)
        (>= M 0)
        (>= H 0)
        (>= I 0)
        (<= N (- B 1))
        (= O (+ I H))
        (= K 0)
        (= P 0)
        (= Q (+ 1 P))
        (= L 0)
        (= M (+ 1 O))
        (= R (+ M L))
        (= S (+ I H))
        (= E (+ 1 R))
        (= C (+ 1 S))
        (= A 1)
        (new7 D I)
        (new8 H)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= L 0)
        (>= M 0)
        (>= H 0)
        (>= I 0)
        (<= N (- B 1))
        (= O (+ I H))
        (= K 0)
        (= P 0)
        (= Q (+ 1 P))
        (= L 0)
        (= M (+ 1 O))
        (= R (+ M L))
        (= S (+ I H))
        (= E (+ 1 R))
        (= C (+ 1 S))
        (= A 1)
        (new7 D H)
        (new8 I)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= L (+ M 1))
        (>= N 0)
        (>= O 0)
        (>= H 0)
        (>= I 0)
        (<= P (- B 1))
        (= Q (+ I H))
        (= M 0)
        (= R 0)
        (= S (+ 1 R))
        (= N 0)
        (= O (+ 1 Q))
        (= T (+ O N))
        (= U (+ I H))
        (= E (+ 1 T))
        (= C (+ 1 U))
        (= A 1)
        (new11 K I)
        (new11 J H)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= L 0)
        (>= M 0)
        (>= H 0)
        (>= I 0)
        (<= (+ J 1) (+ 1 N))
        (<= O (- B 1))
        (= P (+ I H))
        (= K 0)
        (= Q 0)
        (= R (+ 1 Q))
        (= L 0)
        (= M (+ 1 P))
        (= S (+ M L))
        (= T (+ I H))
        (= E (+ 1 S))
        (= C (+ 1 T))
        (= A 1)
        (new11 N H)
        (new8 I)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= J (+ (+ 1 L) 1))
        (>= M 0)
        (>= N 0)
        (>= H 0)
        (>= I 0)
        (<= O (- B 1))
        (= P (+ I H))
        (= K 0)
        (= Q 0)
        (= R (+ 1 Q))
        (= M 0)
        (= N (+ 1 P))
        (= S (+ N M))
        (= T (+ I H))
        (= E (+ 1 S))
        (= C (+ 1 T))
        (= A 1)
        (new11 L H)
        (new8 I)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Bool) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D true)
        (>= H B)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (<= L M)
        (<= N O)
        (= P (+ 1 L))
        (= Q (+ 1 N))
        (= R (+ K I))
        (= S (+ K J))
        (= E (+ 1 R))
        (= C (+ 1 S))
        (= A 1)
        (diff_new31 T N D L)
        (new29 O D M K)
        (new4 A B J T I)
      )
      (new4 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) (N Int) (O Int) (P Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (>= H B)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= J 0)
        (<= L M)
        (= N (+ 1 L))
        (= O (+ J I))
        (= P (+ J K))
        (= E (+ 1 O))
        (= C (+ 1 P))
        (= A 1)
        (new32 M D J)
        (new33 L I A B K)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Bool) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (>= H B)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (<= L M)
        (= N (+ 1 L))
        (= O (+ K I))
        (= P (+ K J))
        (= E (+ 1 O))
        (= C (+ 1 P))
        (= A 1)
        (diff_new36 Q L D)
        (new34 M K)
        (new4 A B J Q I)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (= D false)
        (>= H (+ I 1))
        (>= J B)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (>= L 0)
        (<= N O)
        (= P (+ 1 N))
        (= Q (+ L K))
        (= R (+ L M))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new37 O I L)
        (new38 N K A B M H)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (>= H B)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= J 0)
        (<= (+ L 1) (+ 1 M))
        (<= N O)
        (= P (+ 1 N))
        (= Q (+ J I))
        (= R (+ J K))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new34 O J)
        (new38 N I A B K M)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (>= H (+ (+ 1 I) 1))
        (>= J B)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (>= L 0)
        (<= N O)
        (= P (+ 1 N))
        (= Q (+ L K))
        (= R (+ L M))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new34 O L)
        (new38 N K A B M I)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Bool) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D true)
        (>= H (+ I 1))
        (>= J B)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (<= N O)
        (= P (+ 1 N))
        (= Q (+ 1 I))
        (= R (+ K M))
        (= S (+ M L))
        (= E (+ 1 R))
        (= C (+ 1 S))
        (= A 1)
        (diff_new31 T H D N)
        (new4 A B L T K)
        (new29 I D O M)
      )
      (new4 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) (N Int) (O Int) (P Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (>= H (+ I 1))
        (>= J B)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (>= K 0)
        (= N (+ 1 I))
        (= O (+ L K))
        (= P (+ K M))
        (= E (+ 1 O))
        (= C (+ 1 P))
        (= A 1)
        (new33 H L A B M)
        (new32 I D K)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Bool) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (>= H (+ I 1))
        (>= J B)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (= N (+ 1 I))
        (= O (+ K M))
        (= P (+ M L))
        (= E (+ 1 O))
        (= C (+ 1 P))
        (= A 1)
        (diff_new36 Q H D)
        (new4 A B L Q K)
        (new34 I M)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (= D false)
        (>= H (+ I 1))
        (>= J (+ K 1))
        (>= L B)
        (>= M 0)
        (>= N 0)
        (>= O 0)
        (>= M 0)
        (= P (+ 1 K))
        (= Q (+ N M))
        (= R (+ M O))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new38 J N A B O H)
        (new37 K I M)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (>= H (+ I 1))
        (>= J B)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (>= K 0)
        (<= (+ N 1) (+ 1 O))
        (= P (+ 1 I))
        (= Q (+ L K))
        (= R (+ K M))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new38 H L A B M O)
        (new34 I K)
      )
      (new4 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (>= H (+ (+ 1 I) 1))
        (>= J (+ K 1))
        (>= L B)
        (>= M 0)
        (>= N 0)
        (>= O 0)
        (>= M 0)
        (= P (+ 1 K))
        (= Q (+ N M))
        (= R (+ M O))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new38 J N A B O I)
        (new34 K M)
      )
      (new4 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= D true)
        (>= F 0)
        (>= G 0)
        (= F 0)
        (= G 0)
        (= H (+ G F))
        (= E (+ 1 H))
        (= C 0)
        (= A 1)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D true)
        (= D true)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= H 0)
        (>= I 0)
        (<= L M)
        (<= N (- B 1))
        (<= O P)
        (= Q (+ I H))
        (= P 0)
        (= R (+ 1 O))
        (= O (+ 1 L))
        (= J (+ 1 Q))
        (= K 0)
        (= S (+ K J))
        (= T (+ I H))
        (= E (+ 1 S))
        (= C (+ 1 T))
        (= A 1)
        (new57 D M I)
        (new57 D L H)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= H 0)
        (>= I 0)
        (<= L (- B 1))
        (<= M N)
        (= O (+ I H))
        (= N 0)
        (= P (+ 1 M))
        (= J (+ 1 O))
        (= K 0)
        (= Q (+ K J))
        (= R (+ I H))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new59 D I)
        (new60 H)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= H 0)
        (>= I 0)
        (<= L (- B 1))
        (<= M N)
        (= O (+ I H))
        (= N 0)
        (= P (+ 1 M))
        (= J (+ 1 O))
        (= K 0)
        (= Q (+ K J))
        (= R (+ I H))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new59 D H)
        (new60 I)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= L 0)
        (>= M 0)
        (>= H 0)
        (>= I 0)
        (<= N (- B 1))
        (<= O P)
        (= Q (+ I H))
        (= P 0)
        (= R (+ 1 O))
        (= L (+ 1 Q))
        (= M 0)
        (= S (+ M L))
        (= T (+ I H))
        (= E (+ 1 S))
        (= C (+ 1 T))
        (= A 1)
        (new63 K I)
        (new63 J H)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= H 0)
        (>= I 0)
        (<= (+ L 1) (+ 1 M))
        (<= N (- B 1))
        (<= L O)
        (= P (+ I H))
        (= O 0)
        (= Q (+ 1 L))
        (= J (+ 1 P))
        (= K 0)
        (= R (+ K J))
        (= S (+ I H))
        (= E (+ 1 R))
        (= C (+ 1 S))
        (= A 1)
        (new63 M H)
        (new60 I)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) )
    (=>
      (and
        (= F true)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ (+ 1 K) 1))
        (>= L 0)
        (>= M 0)
        (>= H 0)
        (>= I 0)
        (<= N (- B 1))
        (<= J O)
        (= P (+ I H))
        (= O 0)
        (= Q (+ 1 J))
        (= L (+ 1 P))
        (= M 0)
        (= R (+ M L))
        (= S (+ I H))
        (= E (+ 1 R))
        (= C (+ 1 S))
        (= A 1)
        (new63 K H)
        (new60 I)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D true)
        (= D true)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= L 0)
        (>= M 0)
        (>= H 0)
        (>= I 0)
        (<= N O)
        (<= P (- B 1))
        (= Q (+ I H))
        (= K 0)
        (= R 0)
        (= S (+ 1 R))
        (= J (+ 1 N))
        (= L 0)
        (= M (+ 1 Q))
        (= T (+ M L))
        (= U (+ I H))
        (= E (+ 1 T))
        (= C (+ 1 U))
        (= A 1)
        (new57 D O I)
        (new57 D N H)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= L 0)
        (>= M 0)
        (>= H 0)
        (>= I 0)
        (<= N (- B 1))
        (= O (+ I H))
        (= K 0)
        (= P 0)
        (= Q (+ 1 P))
        (= L 0)
        (= M (+ 1 O))
        (= R (+ M L))
        (= S (+ I H))
        (= E (+ 1 R))
        (= C (+ 1 S))
        (= A 1)
        (new59 D I)
        (new60 H)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= L 0)
        (>= M 0)
        (>= H 0)
        (>= I 0)
        (<= N (- B 1))
        (= O (+ I H))
        (= K 0)
        (= P 0)
        (= Q (+ 1 P))
        (= L 0)
        (= M (+ 1 O))
        (= R (+ M L))
        (= S (+ I H))
        (= E (+ 1 R))
        (= C (+ 1 S))
        (= A 1)
        (new59 D H)
        (new60 I)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= L (+ M 1))
        (>= N 0)
        (>= O 0)
        (>= H 0)
        (>= I 0)
        (<= P (- B 1))
        (= Q (+ I H))
        (= M 0)
        (= R 0)
        (= S (+ 1 R))
        (= N 0)
        (= O (+ 1 Q))
        (= T (+ O N))
        (= U (+ I H))
        (= E (+ 1 T))
        (= C (+ 1 U))
        (= A 1)
        (new63 K I)
        (new63 J H)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= L 0)
        (>= M 0)
        (>= H 0)
        (>= I 0)
        (<= (+ J 1) (+ 1 N))
        (<= O (- B 1))
        (= P (+ I H))
        (= K 0)
        (= Q 0)
        (= R (+ 1 Q))
        (= L 0)
        (= M (+ 1 P))
        (= S (+ M L))
        (= T (+ I H))
        (= E (+ 1 S))
        (= C (+ 1 T))
        (= A 1)
        (new63 N H)
        (new60 I)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) )
    (=>
      (and
        (= F false)
        (= G true)
        (= D false)
        (>= H 0)
        (>= I 0)
        (>= J (+ K 1))
        (>= J (+ (+ 1 L) 1))
        (>= M 0)
        (>= N 0)
        (>= H 0)
        (>= I 0)
        (<= O (- B 1))
        (= P (+ I H))
        (= K 0)
        (= Q 0)
        (= R (+ 1 Q))
        (= M 0)
        (= N (+ 1 P))
        (= S (+ N M))
        (= T (+ I H))
        (= E (+ 1 S))
        (= C (+ 1 T))
        (= A 1)
        (new63 L H)
        (new60 I)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Bool) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D true)
        (>= H B)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (<= L M)
        (<= N O)
        (= P (+ 1 L))
        (= Q (+ 1 N))
        (= R (+ K I))
        (= S (+ K J))
        (= E (+ 1 R))
        (= C (+ 1 S))
        (= A 1)
        (diff_new83 T N D L)
        (new81 O D M K)
        (new3 A B J T I)
      )
      (new3 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) (N Int) (O Int) (P Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (>= H B)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= J 0)
        (<= L M)
        (= N (+ 1 L))
        (= O (+ J I))
        (= P (+ J K))
        (= E (+ 1 O))
        (= C (+ 1 P))
        (= A 1)
        (new84 M D J)
        (new85 L I A B K)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Bool) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (>= H B)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (<= L M)
        (= N (+ 1 L))
        (= O (+ K I))
        (= P (+ K J))
        (= E (+ 1 O))
        (= C (+ 1 P))
        (= A 1)
        (diff_new88 Q L D)
        (new86 M K)
        (new3 A B J Q I)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (= D false)
        (>= H (+ I 1))
        (>= J B)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (>= L 0)
        (<= N O)
        (= P (+ 1 N))
        (= Q (+ L K))
        (= R (+ L M))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new89 O I L)
        (new90 N K A B M H)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (>= H B)
        (>= I 0)
        (>= J 0)
        (>= K 0)
        (>= J 0)
        (<= (+ L 1) (+ 1 M))
        (<= N O)
        (= P (+ 1 N))
        (= Q (+ J I))
        (= R (+ J K))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new86 O J)
        (new90 N I A B K M)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F true)
        (= G false)
        (= D false)
        (>= H (+ (+ 1 I) 1))
        (>= J B)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (>= L 0)
        (<= N O)
        (= P (+ 1 N))
        (= Q (+ L K))
        (= R (+ L M))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new86 O L)
        (new90 N K A B M I)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Bool) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D true)
        (>= H (+ I 1))
        (>= J B)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (<= N O)
        (= P (+ 1 N))
        (= Q (+ 1 I))
        (= R (+ K M))
        (= S (+ M L))
        (= E (+ 1 R))
        (= C (+ 1 S))
        (= A 1)
        (diff_new83 T H D N)
        (new3 A B L T K)
        (new81 I D O M)
      )
      (new3 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) (N Int) (O Int) (P Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (>= H (+ I 1))
        (>= J B)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (>= K 0)
        (= N (+ 1 I))
        (= O (+ L K))
        (= P (+ K M))
        (= E (+ 1 O))
        (= C (+ 1 P))
        (= A 1)
        (new85 H L A B M)
        (new84 I D K)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Bool) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (>= H (+ I 1))
        (>= J B)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (= N (+ 1 I))
        (= O (+ K M))
        (= P (+ M L))
        (= E (+ 1 O))
        (= C (+ 1 P))
        (= A 1)
        (diff_new88 Q H D)
        (new3 A B L Q K)
        (new86 I M)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (= D false)
        (>= H (+ I 1))
        (>= J (+ K 1))
        (>= L B)
        (>= M 0)
        (>= N 0)
        (>= O 0)
        (>= M 0)
        (= P (+ 1 K))
        (= Q (+ N M))
        (= R (+ M O))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new90 J N A B O H)
        (new89 K I M)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (>= H (+ I 1))
        (>= J B)
        (>= K 0)
        (>= L 0)
        (>= M 0)
        (>= K 0)
        (<= (+ N 1) (+ 1 O))
        (= P (+ 1 I))
        (= Q (+ L K))
        (= R (+ K M))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new90 H L A B M O)
        (new86 I K)
      )
      (new3 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) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= F false)
        (= G false)
        (= D false)
        (>= H (+ (+ 1 I) 1))
        (>= J (+ K 1))
        (>= L B)
        (>= M 0)
        (>= N 0)
        (>= O 0)
        (>= M 0)
        (= P (+ 1 K))
        (= Q (+ N M))
        (= R (+ M O))
        (= E (+ 1 Q))
        (= C (+ 1 R))
        (= A 1)
        (new90 J N A B O I)
        (new86 K M)
      )
      (new3 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= E 1)
        (new3 E A C D B)
      )
      (new2 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= E 1)
        (new4 E A C D B)
      )
      (new1 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A true)
        (<= (- B C) 0)
        (new1 D B C A)
      )
      ff
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) )
    (=>
      (and
        (= A true)
        (>= (- B C) 2)
        (new2 D B C A)
      )
      ff
    )
  )
)

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