; Automatically generated by map2smt

(set-logic HORN)




(declare-fun new84 (Bool Int Bool Bool Int Bool) Bool)
(declare-fun new83 (Int Bool Bool Int Bool) Bool)
(declare-fun new82 (Int Bool Bool Int Bool) Bool)
(declare-fun new81 (Bool Bool Bool) Bool)
(declare-fun new80 (Bool Bool Int Bool) Bool)
(declare-fun new79 (Int Bool Bool Bool) Bool)
(declare-fun new66 (Bool Int Bool) Bool)
(declare-fun new60 (Int Int Bool Bool Bool Bool) Bool)
(declare-fun new6 (Bool) Bool)
(declare-fun new57 (Bool Bool) Bool)
(declare-fun new44 (Int Bool Int Bool Bool) Bool)
(declare-fun new37 (Int Bool Int Bool Bool) Bool)
(declare-fun new28 (Bool Int Bool Bool) Bool)
(declare-fun new25 (Bool) Bool)
(declare-fun new235 (Bool Bool) Bool)
(declare-fun new21 (Int Bool Bool) Bool)
(declare-fun new20 (Int Bool Int Bool) Bool)
(declare-fun new16 (Int Int Bool) Bool)
(declare-fun new13 (Int Bool Int Bool) Bool)
(declare-fun new11 (Int Bool) Bool)
(declare-fun new101 (Bool Int Bool) Bool)
(declare-fun new10 (Bool Int) Bool)
(declare-fun new1 (Bool) Bool)
(declare-fun diff_new8 (Int Int Bool Bool Bool Bool) Bool)
(declare-fun diff_new5 (Bool Int Bool) Bool)
(declare-fun diff_new3 (Int Int Bool Bool) Bool)
(declare-fun diff_new15 (Int Int Int Int Bool Bool) Bool)
(declare-fun diff_new144 (Int Bool Int Int Bool) Bool)
(declare-fun not_fun_diff_new144 () Bool)
(declare-fun constr (Bool) Bool)
(declare-fun not_fun_diff_new15 () Bool)
(declare-fun not_fun_diff_new8 () Bool)
(declare-fun not_fun_diff_new5 () Bool)
(declare-fun not_fun_diff_new3 () Bool)
(declare-fun inst_fold () Bool)
(declare-fun ff () Bool)

(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Int) (I Int) (J Bool) )
    (=>
      (and
        (diff_new144 A B C D E)
        (diff_new144 F G H I J)
        (and (and (= A F) (and (= B G) (and (= C H) (= D I)))) (not (= E J)))
      )
      not_fun_diff_new144
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Bool) (L Bool) )
    (=>
      (and
        (diff_new15 A B C D E F)
        (diff_new15 G H I J K L)
        (and (and (= A G) (and (= B H) (and (= C I) (and (= D J) (= E K))))) (not (= F L)))
      )
      not_fun_diff_new15
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Bool) (F Bool) (G Int) (H Int) (I Bool) (J Bool) (K Bool) (L Bool) )
    (=>
      (and
        (diff_new8 A B C D E F)
        (diff_new8 G H I J K L)
        (and (and (= A G) (and (= B H) (and (= C I) (= D J)))) (or (not (= E K)) (not (= F L))))
      )
      not_fun_diff_new8
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Bool) )
    (=>
      (and
        (diff_new5 A B C)
        (diff_new5 D E F)
        (and (and (= A D) (= B E)) (not (= C F)))
      )
      not_fun_diff_new5
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Int) (F Int) (G Bool) (H Bool) )
    (=>
      (and
        (diff_new3 A B C D)
        (diff_new3 E F G H)
        (and (and (= A E) (and (= B F) (= C G))) (not (= D H)))
      )
      not_fun_diff_new3
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B false)
        (= A false)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= (- C D) 1)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (- C D) (- 1))
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= A false)
        (new25 B)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B false)
        (= A false)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B true)
        (= A false)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B false)
        (= A true)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B true)
        (= A true)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= (- C D) 1)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= (- C D) 1)
        (>= (- C E) 1)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= (- C D) 1)
        (<= (- C E) (- 1))
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (>= (- C D) 1)
        (new25 B)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (- C D) (- 1))
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= (- C D) 1)
        (<= (- C E) (- 1))
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (- C D) (- 1))
        (<= (- C E) (- 1))
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (<= (- C D) (- 1))
        (new25 B)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B false)
        (new25 A)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (>= (- C D) 1)
        (new25 A)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (<= (- C D) (- 1))
        (new25 A)
      )
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (new235 B A)
      (new235 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) )
    (=>
      (and
        (= E false)
        (= B false)
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- F C) 1)
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (<= (- F C) (- 1))
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) )
    (=>
      (and
        (= B false)
        inst_fold
        (new25 E)
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- F A) 1)
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- F C) 1)
        (>= (- G A) 1)
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- F A) 1)
        (<= (- G C) (- 1))
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= B false)
        (>= (- F A) 1)
        inst_fold
        (new25 E)
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (<= (- F A) (- 1))
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- F C) 1)
        (<= (- G A) (- 1))
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (<= (- F C) (- 1))
        (<= (- G A) (- 1))
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= B false)
        (<= (- F A) (- 1))
        inst_fold
        (new25 E)
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) )
    (=>
      (and
        (= E false)
        (new25 B)
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (>= (- F C) 1)
        (new25 B)
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (<= (- F C) (- 1))
        (new25 B)
      )
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) (E Bool) )
    (=>
      (new66 B D E)
      (diff_new144 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- B D) 1)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- B D) (- 1))
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= A false)
        inst_fold
        (new25 C)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- B D) 1)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- B D) (- 1))
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= A false)
        (new6 C)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A true)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A true)
        (>= (- B D) 1)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A true)
        (<= (- B D) (- 1))
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= A true)
        (new6 C)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- D E) 1)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- D E) 1)
        (>= (- B F) 1)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- D E) 1)
        (<= (- B F) (- 1))
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (>= (- D E) 1)
        inst_fold
        (new25 C)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- D E) (- 1))
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- B D) 1)
        (<= (- E F) (- 1))
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- D E) (- 1))
        (<= (- B F) (- 1))
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (<= (- D E) (- 1))
        inst_fold
        (new25 C)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (new25 A)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- B D) 1)
        (new25 A)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (<= (- B D) (- 1))
        (new25 A)
      )
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (new101 A D C)
      (new101 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F B) 1)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (<= (- F B) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D true)
        (= C false)
        (= A false)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- B F) 1)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- F B) 1)
        (>= (- B G) 1)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- B G) 1)
        (<= (- F B) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (>= (- B F) 1)
        (>= (- B F) 1)
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- B F) 1)
        (<= (- G F) (- 1))
        (<= (- G B) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= A false)
        (>= (- B F) 1)
        (<= (- F B) (- 1))
        (new25 D)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (<= (- B F) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- F B) 1)
        (<= (- B G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F B) 1)
        (<= (- F G) (- 1))
        (<= (- B G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (<= (- F G) (- 1))
        (<= (- F B) (- 1))
        (<= (- B G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (<= (- B F) (- 1))
        (<= (- B F) (- 1))
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= A false)
        (>= (- F B) 1)
        (<= (- B F) (- 1))
        (new25 D)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A false)
        inst_fold
        (new25 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A false)
        (>= (- F B) 1)
        (>= (- F B) 1)
        inst_fold
        (new25 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A false)
        (<= (- F B) (- 1))
        (<= (- F B) (- 1))
        inst_fold
        (new25 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= A false)
        (new79 F C D E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F B) 1)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (<= (- F B) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D true)
        (= C false)
        (= A false)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- B F) 1)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- F B) 1)
        (>= (- B G) 1)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- B G) 1)
        (<= (- F B) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (>= (- B F) 1)
        (>= (- B F) 1)
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- B F) 1)
        (<= (- G F) (- 1))
        (<= (- G B) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= A false)
        (>= (- B F) 1)
        (<= (- F B) (- 1))
        (new25 D)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (<= (- B F) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- F B) 1)
        (<= (- B G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F B) 1)
        (<= (- F G) (- 1))
        (<= (- B G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (<= (- F G) (- 1))
        (<= (- F B) (- 1))
        (<= (- B G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (<= (- B F) (- 1))
        (<= (- B F) (- 1))
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= A false)
        (>= (- F B) 1)
        (<= (- B F) (- 1))
        (new25 D)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A false)
        (new6 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A false)
        (>= (- F B) 1)
        (>= (- F B) 1)
        (new6 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A false)
        (<= (- F B) (- 1))
        (<= (- F B) (- 1))
        (new6 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= A false)
        (new80 C D F E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A true)
        (>= (- F B) 1)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A true)
        (<= (- F B) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A true)
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D true)
        (= C false)
        (= A true)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A true)
        (>= (- B F) 1)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A true)
        (>= (- F G) 1)
        (>= (- F B) 1)
        (>= (- B G) 1)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A true)
        (>= (- F G) 1)
        (>= (- B G) 1)
        (<= (- F B) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A true)
        (>= (- B F) 1)
        (>= (- B F) 1)
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A true)
        (>= (- B F) 1)
        (<= (- G F) (- 1))
        (<= (- G B) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= A true)
        (>= (- B F) 1)
        (<= (- F B) (- 1))
        (new25 D)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A true)
        (<= (- B F) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A true)
        (>= (- F G) 1)
        (>= (- F B) 1)
        (<= (- B G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A true)
        (>= (- F B) 1)
        (<= (- F G) (- 1))
        (<= (- B G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A true)
        (<= (- F G) (- 1))
        (<= (- F B) (- 1))
        (<= (- B G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A true)
        (<= (- B F) (- 1))
        (<= (- B F) (- 1))
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= A true)
        (>= (- F B) 1)
        (<= (- B F) (- 1))
        (new25 D)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A true)
        (new6 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A true)
        (>= (- F B) 1)
        (>= (- F B) 1)
        (new6 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A true)
        (<= (- F B) (- 1))
        (<= (- F B) (- 1))
        (new6 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= A true)
        (new81 C D E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F B) 1)
        (>= (- G H) 1)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (<= (- H B) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D true)
        (= C false)
        (= A false)
        (>= (- F G) 1)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- B H) 1)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- F B) 1)
        (>= (- H I) 1)
        (>= (- B G) 1)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- H I) 1)
        (>= (- B I) 1)
        (<= (- H B) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- B H) 1)
        (>= (- B H) 1)
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- B H) 1)
        (<= (- I H) (- 1))
        (<= (- I B) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- B H) 1)
        (<= (- H B) (- 1))
        (new25 D)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (<= (- B H) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- F B) 1)
        (>= (- H I) 1)
        (<= (- B G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- H B) 1)
        (<= (- H I) (- 1))
        (<= (- B I) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (<= (- H I) (- 1))
        (<= (- H B) (- 1))
        (<= (- B I) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (<= (- B H) (- 1))
        (<= (- B H) (- 1))
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- H B) 1)
        (<= (- B H) (- 1))
        (new25 D)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A false)
        (>= (- F G) 1)
        inst_fold
        (new25 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A false)
        (>= (- F B) 1)
        (>= (- F B) 1)
        (>= (- G H) 1)
        inst_fold
        (new25 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A false)
        (>= (- F G) 1)
        (<= (- H B) (- 1))
        (<= (- H B) (- 1))
        inst_fold
        (new25 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (>= (- F G) 1)
        (new82 F C D G E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F B) 1)
        (<= (- G H) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (<= (- F B) (- 1))
        (<= (- G H) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (<= (- F G) (- 1))
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D true)
        (= C false)
        (= A false)
        (<= (- F G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- B F) 1)
        (<= (- G H) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- F B) 1)
        (>= (- B G) 1)
        (<= (- H I) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- B G) 1)
        (<= (- F B) (- 1))
        (<= (- H I) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (>= (- B F) 1)
        (>= (- B F) 1)
        (<= (- G H) (- 1))
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- B F) 1)
        (<= (- G F) (- 1))
        (<= (- G B) (- 1))
        (<= (- H I) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= A false)
        (>= (- B F) 1)
        (<= (- G H) (- 1))
        (<= (- F B) (- 1))
        (new25 D)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (<= (- F G) (- 1))
        (<= (- B H) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F G) 1)
        (>= (- F B) 1)
        (<= (- H I) (- 1))
        (<= (- B G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (>= (- F B) 1)
        (<= (- F G) (- 1))
        (<= (- H I) (- 1))
        (<= (- B G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= A false)
        (<= (- F G) (- 1))
        (<= (- F B) (- 1))
        (<= (- H I) (- 1))
        (<= (- B G) (- 1))
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (<= (- F G) (- 1))
        (<= (- B H) (- 1))
        (<= (- B H) (- 1))
        inst_fold
        (new25 E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= A false)
        (>= (- F B) 1)
        (<= (- G H) (- 1))
        (<= (- B F) (- 1))
        (new25 D)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A false)
        (<= (- F G) (- 1))
        inst_fold
        (new25 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A false)
        (>= (- F B) 1)
        (>= (- F B) 1)
        (<= (- G H) (- 1))
        inst_fold
        (new25 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= A false)
        (<= (- F B) (- 1))
        (<= (- F B) (- 1))
        (<= (- G H) (- 1))
        inst_fold
        (new25 C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (<= (- F G) (- 1))
        (new83 F C D G E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= (- F B) 1)
        (new25 A)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (<= (- F B) (- 1))
        (new25 A)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (new66 A F E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D true)
        (= C false)
        (new25 A)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= (- B F) 1)
        (new25 A)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= (- F G) 1)
        (>= (- F B) 1)
        (>= (- B G) 1)
        (new25 A)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= (- F G) 1)
        (>= (- B G) 1)
        (<= (- F B) (- 1))
        (new25 A)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (>= (- B F) 1)
        (>= (- B F) 1)
        (new66 A G E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= (- B F) 1)
        (<= (- G F) (- 1))
        (<= (- G B) (- 1))
        (new25 A)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (>= (- B F) 1)
        (<= (- F B) (- 1))
        (new25 D)
        (new25 A)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (<= (- B F) (- 1))
        (new25 A)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= (- F G) 1)
        (>= (- F B) 1)
        (<= (- B G) (- 1))
        (new25 A)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= (- F B) 1)
        (<= (- F G) (- 1))
        (<= (- B G) (- 1))
        (new25 A)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (<= (- F G) (- 1))
        (<= (- F B) (- 1))
        (<= (- B G) (- 1))
        (new25 A)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (<= (- B F) (- 1))
        (<= (- B F) (- 1))
        (new66 A G E)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (>= (- F B) 1)
        (<= (- B F) (- 1))
        (new25 D)
        (new25 A)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (new101 A F C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (>= (- F B) 1)
        (>= (- F B) 1)
        (new101 A G C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (<= (- F B) (- 1))
        (<= (- F B) (- 1))
        (new101 A G C)
      )
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (new84 A F C D F E)
      (new84 A B C D B E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- F D) 1)
        (<= (- A D) (- 1))
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (<= (- F D) (- 1))
        (<= (- A D) (- 1))
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) )
    (=>
      (and
        (= C false)
        (= B false)
        (<= (- A D) (- 1))
        (new25 E)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) )
    (=>
      (and
        (= E false)
        (= C true)
        (= B false)
        (<= (- A D) (- 1))
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- A F) 1)
        (<= (- A D) (- 1))
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- F D) 1)
        (>= (- A G) 1)
        (<= (- A D) (- 1))
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- A G) 1)
        (<= (- F D) (- 1))
        (<= (- A D) (- 1))
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= (- D F) 1)
        (>= (- A F) 1)
        (<= (- A D) (- 1))
        (new25 E)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- A F) 1)
        (<= (- G F) (- 1))
        (<= (- G D) (- 1))
        (<= (- A D) (- 1))
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- A F) 1)
        (<= (- F D) (- 1))
        (<= (- A D) (- 1))
        (new25 C)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (<= (- A F) (- 1))
        (<= (- A D) (- 1))
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- F D) 1)
        (<= (- A G) (- 1))
        (<= (- A D) (- 1))
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (<= (- F D) (- 1))
        (<= (- A G) (- 1))
        (<= (- A D) (- 1))
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= (- D F) 1)
        (<= (- A F) (- 1))
        (<= (- A D) (- 1))
        (new25 E)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- F D) 1)
        (<= (- F G) (- 1))
        (<= (- A G) (- 1))
        (<= (- A D) (- 1))
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (<= (- F G) (- 1))
        (<= (- F D) (- 1))
        (<= (- A G) (- 1))
        (<= (- A D) (- 1))
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (<= (- D F) (- 1))
        (<= (- A F) (- 1))
        (<= (- A D) (- 1))
        (new25 E)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- F D) 1)
        (<= (- A F) (- 1))
        (<= (- A D) (- 1))
        (new25 C)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (<= (- F D) (- 1))
        (<= (- A F) (- 1))
        (<= (- A D) (- 1))
        (new25 C)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) )
    (=>
      (and
        (= B false)
        (<= (- A D) (- 1))
        (<= (- A D) (- 1))
        (new235 E C)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) )
    (=>
      (and
        (= E false)
        (= C false)
        (<= (- A D) (- 1))
        (new25 B)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (>= (- F A) 1)
        (>= (- F D) 1)
        (<= (- A D) (- 1))
        (new25 B)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (>= (- F A) 1)
        (<= (- F D) (- 1))
        (<= (- A D) (- 1))
        (new25 B)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) )
    (=>
      (and
        (= C false)
        (>= (- D A) 1)
        (<= (- A D) (- 1))
        (new25 E)
        (new25 B)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (<= (- F A) (- 1))
        (<= (- F D) (- 1))
        (<= (- A D) (- 1))
        (new25 B)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) )
    (=>
      (and
        (= E false)
        (<= (- A D) (- 1))
        (<= (- A D) (- 1))
        (new57 C B)
      )
      (new83 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- F D) 1)
        (>= (- A D) 1)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- A D) 1)
        (<= (- F D) (- 1))
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= (- A D) 1)
        (new25 E)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) )
    (=>
      (and
        (= E false)
        (= C true)
        (= B false)
        (>= (- A D) 1)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A D) 1)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- F D) 1)
        (>= (- A G) 1)
        (>= (- A D) 1)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- A G) 1)
        (>= (- A D) 1)
        (<= (- F D) (- 1))
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= (- D F) 1)
        (>= (- A F) 1)
        (>= (- A D) 1)
        (new25 E)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- F D) 1)
        (>= (- A G) 1)
        (>= (- A D) 1)
        (<= (- F G) (- 1))
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A D) 1)
        (<= (- G F) (- 1))
        (<= (- G D) (- 1))
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A D) 1)
        (<= (- D F) (- 1))
        (new25 E)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- F D) 1)
        (>= (- A F) 1)
        (>= (- A D) 1)
        (new25 C)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A D) 1)
        (<= (- F D) (- 1))
        (new25 C)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) )
    (=>
      (and
        (= B false)
        (>= (- A D) 1)
        (>= (- A D) 1)
        (new235 E C)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- A D) 1)
        (<= (- A F) (- 1))
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- F D) 1)
        (>= (- A D) 1)
        (<= (- A G) (- 1))
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- F D) 1)
        (>= (- A D) 1)
        (<= (- F G) (- 1))
        (<= (- A G) (- 1))
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (= B false)
        (>= (- A D) 1)
        (<= (- F G) (- 1))
        (<= (- F D) (- 1))
        (<= (- A G) (- 1))
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= (- A D) 1)
        (<= (- D F) (- 1))
        (<= (- A F) (- 1))
        (new25 E)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- F D) 1)
        (>= (- A D) 1)
        (<= (- A F) (- 1))
        (new25 C)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) )
    (=>
      (and
        (= E false)
        (= C false)
        (>= (- A D) 1)
        (new25 B)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (>= (- F A) 1)
        (>= (- F D) 1)
        (>= (- A D) 1)
        (new25 B)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (>= (- F D) 1)
        (>= (- A D) 1)
        (<= (- F A) (- 1))
        (new25 B)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= C false)
        (>= (- A D) 1)
        (<= (- F A) (- 1))
        (<= (- F D) (- 1))
        (new25 B)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) )
    (=>
      (and
        (= C false)
        (>= (- A D) 1)
        (<= (- D A) (- 1))
        (new25 E)
        (new25 B)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Bool) )
    (=>
      (and
        (= E false)
        (>= (- A D) 1)
        (>= (- A D) 1)
        (new57 C B)
      )
      (new82 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Bool) )
    (=>
      (and
        (= C true)
        (= B false)
        (= A false)
      )
      (new81 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (= A false)
        (>= (- D E) 1)
      )
      (new81 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (= A false)
        (<= (- D E) (- 1))
      )
      (new81 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
        (new25 B)
      )
      (new81 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Bool) )
    (=>
      (and
        (= C false)
        (= B false)
        (= A true)
      )
      (new81 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Bool) )
    (=>
      (and
        (= C true)
        (= B true)
        (= A true)
      )
      (new81 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D false)
        (= B false)
        (= A false)
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Int) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (= A false)
        (>= (- E F) 1)
        (>= (- E C) 1)
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Int) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (= A false)
        (>= (- E F) 1)
        (<= (- E C) (- 1))
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= (- C E) 1)
        (new25 D)
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Int) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (= A false)
        (>= (- E C) 1)
        (<= (- E F) (- 1))
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Int) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (= A false)
        (<= (- E F) (- 1))
        (<= (- E C) (- 1))
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (- C E) (- 1))
        (new25 D)
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= A false)
        (>= (- E C) 1)
        (new25 B)
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= A false)
        (<= (- E C) (- 1))
        (new25 B)
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= A false)
        (new235 D B)
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (= A true)
        (>= (- E C) 1)
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (= A true)
        (<= (- E C) (- 1))
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= B false)
        (= A true)
        (new25 D)
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D false)
        (= B true)
        (= A true)
      )
      (new80 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) )
    (=>
      (and
        (= D false)
        (= C false)
        (= B false)
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) )
    (=>
      (and
        (= D true)
        (= C true)
        (= B false)
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= C false)
        (= B false)
        (>= (- A E) 1)
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Int) (F Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= B false)
        (>= (- E F) 1)
        (>= (- A F) 1)
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Int) (F Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= B false)
        (>= (- A E) 1)
        (<= (- F E) (- 1))
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- A E) 1)
        (new25 C)
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= C false)
        (= B false)
        (<= (- A E) (- 1))
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Int) (F Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= B false)
        (>= (- E F) 1)
        (<= (- A F) (- 1))
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Int) (F Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= B false)
        (<= (- E F) (- 1))
        (<= (- A F) (- 1))
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (<= (- A E) (- 1))
        (new25 C)
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) )
    (=>
      (and
        (= D true)
        (= C false)
        (new25 B)
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (>= (- E A) 1)
        (new25 B)
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (<= (- E A) (- 1))
        (new25 B)
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) )
    (=>
      (and
        (= D false)
        (new57 C B)
      )
      (new79 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- D B) 1)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- D B) (- 1))
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= A false)
        inst_fold
        (new25 C)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- D B) 1)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- D B) (- 1))
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= A false)
        inst_fold
        (new25 C)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A true)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A true)
        (>= (- D B) 1)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A true)
        (<= (- D B) (- 1))
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= A true)
        inst_fold
        (new25 C)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- D E) 1)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- D B) 1)
        (>= (- E F) 1)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- D E) 1)
        (<= (- F B) (- 1))
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (>= (- D E) 1)
        inst_fold
        (new25 C)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- D E) (- 1))
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- D B) 1)
        (<= (- E F) (- 1))
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) (F Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- D B) (- 1))
        (<= (- E F) (- 1))
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (<= (- D E) (- 1))
        inst_fold
        (new25 C)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (new25 A)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- D B) 1)
        (new25 A)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (<= (- D B) (- 1))
        (new25 A)
      )
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (new66 A D C)
      (new66 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B true)
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (<= (- F G) (- 1))
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (new66 B F C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B true)
        (>= (- A F) 1)
        (>= (- A F) 1)
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        (>= (- A H) 1)
        (>= (- A H) 1)
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (<= (- G H) (- 1))
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (new66 B G C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (<= (- A F) (- 1))
        (<= (- A F) (- 1))
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (<= (- A F) (- 1))
        (<= (- A F) (- 1))
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B true)
        (<= (- A F) (- 1))
        (<= (- A F) (- 1))
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        (<= (- A H) (- 1))
        (<= (- A H) (- 1))
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (<= (- F G) (- 1))
        (<= (- A H) (- 1))
        (<= (- A H) (- 1))
        inst_fold
        (new25 C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (<= (- A F) (- 1))
        (<= (- A F) (- 1))
        (new66 B G C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= B false)
        (new79 F E D C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= B false)
        (new80 E D F C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= B true)
        (new81 E D C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= B false)
        (>= (- F G) 1)
        (new82 F E D G C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= B false)
        (<= (- F G) (- 1))
        (new83 F E D G C)
      )
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (new84 B F E D F C)
      (new60 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B false)
        (= A false)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B true)
        (= A false)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B false)
        (= A false)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= (- C D) 1)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (- C D) (- 1))
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= A false)
        (new25 B)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B false)
        (= A true)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B true)
        (= A true)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= (- C D) 1)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= (- C D) 1)
        (>= (- E D) 1)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= (- C D) 1)
        (<= (- E D) (- 1))
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (>= (- C D) 1)
        (new25 B)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (- C D) (- 1))
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= (- C D) 1)
        (<= (- E D) (- 1))
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (- C D) (- 1))
        (<= (- E D) (- 1))
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (<= (- C D) (- 1))
        (new25 B)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B false)
        (new25 A)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (>= (- C D) 1)
        (new25 A)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (<= (- C D) (- 1))
        (new25 A)
      )
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (new57 B A)
      (new57 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E true)
        (= D false)
        (= B false)
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (<= (- F G) (- 1))
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= D false)
        (= B false)
        (<= (- A C) (- 1))
        (new25 E)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (>= (- A F) 1)
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (>= (- A F) 1)
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E true)
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (>= (- A F) 1)
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        (>= (- C H) 1)
        (>= (- A H) 1)
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (>= (- A F) 1)
        (<= (- G H) (- 1))
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (>= (- A F) 1)
        (<= (- A C) (- 1))
        (new25 E)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (<= (- A F) (- 1))
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (<= (- A F) (- 1))
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E true)
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (<= (- A F) (- 1))
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        (>= (- C H) 1)
        (<= (- A H) (- 1))
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (<= (- G H) (- 1))
        (<= (- A F) (- 1))
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (<= (- A F) (- 1))
        (<= (- A C) (- 1))
        (new25 E)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (<= (- C F) (- 1))
        (<= (- A F) (- 1))
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (<= (- C F) (- 1))
        (<= (- A F) (- 1))
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E true)
        (= D false)
        (= B false)
        (<= (- C F) (- 1))
        (<= (- A F) (- 1))
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        (<= (- C H) (- 1))
        (<= (- A H) (- 1))
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (<= (- F G) (- 1))
        (<= (- C H) (- 1))
        (<= (- A H) (- 1))
        (<= (- A C) (- 1))
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (<= (- C F) (- 1))
        (<= (- A F) (- 1))
        (<= (- A C) (- 1))
        (new25 E)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= B false)
        (<= (- A C) (- 1))
        (<= (- A C) (- 1))
        inst_fold
        (new25 D)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= B false)
        (<= (- A C) (- 1))
        (<= (- A C) (- 1))
        (new6 D)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E true)
        (= B false)
        (<= (- A C) (- 1))
        (<= (- A C) (- 1))
        (new6 D)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- F G) 1)
        (<= (- A C) (- 1))
        (<= (- A C) (- 1))
        inst_fold
        (new25 D)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (<= (- F G) (- 1))
        (<= (- A C) (- 1))
        (<= (- A C) (- 1))
        inst_fold
        (new25 D)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (<= (- A C) (- 1))
        (new101 E F D)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (>= (- C A) 1)
        (<= (- A C) (- 1))
        (new25 B)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (>= (- C A) 1)
        (<= (- A C) (- 1))
        (new25 B)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E true)
        (= D false)
        (>= (- C A) 1)
        (<= (- A C) (- 1))
        (new25 B)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (>= (- F G) 1)
        (>= (- C A) 1)
        (<= (- A C) (- 1))
        (new25 B)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (>= (- C A) 1)
        (<= (- F G) (- 1))
        (<= (- A C) (- 1))
        (new25 B)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= D false)
        (>= (- C A) 1)
        (<= (- A C) (- 1))
        (new25 E)
        (new25 B)
      )
      (new44 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A C) 1)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A C) 1)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E true)
        (= D false)
        (= B false)
        (>= (- A C) 1)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        (>= (- A C) 1)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A C) 1)
        (<= (- F G) (- 1))
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- A C) 1)
        (new25 E)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (>= (- A F) 1)
        (>= (- A C) 1)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (>= (- A F) 1)
        (>= (- A C) 1)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E true)
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (>= (- A F) 1)
        (>= (- A C) 1)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        (>= (- C H) 1)
        (>= (- A H) 1)
        (>= (- A C) 1)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (>= (- A F) 1)
        (>= (- A C) 1)
        (<= (- G H) (- 1))
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- C F) 1)
        (>= (- A F) 1)
        (>= (- A C) 1)
        (new25 E)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A C) 1)
        (<= (- C F) (- 1))
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A C) 1)
        (<= (- C F) (- 1))
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E true)
        (= D false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A C) 1)
        (<= (- C F) (- 1))
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        (>= (- A H) 1)
        (>= (- A C) 1)
        (<= (- C H) (- 1))
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A C) 1)
        (<= (- G H) (- 1))
        (<= (- C F) (- 1))
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A C) 1)
        (<= (- C F) (- 1))
        (new25 E)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- A C) 1)
        (>= (- A C) 1)
        inst_fold
        (new25 D)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- A C) 1)
        (>= (- A C) 1)
        (new6 D)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E true)
        (= B false)
        (>= (- A C) 1)
        (>= (- A C) 1)
        (new6 D)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- F G) 1)
        (>= (- A C) 1)
        (>= (- A C) 1)
        inst_fold
        (new25 D)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- A C) 1)
        (>= (- A C) 1)
        (<= (- F G) (- 1))
        inst_fold
        (new25 D)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (>= (- A C) 1)
        (new101 E F D)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A C) 1)
        (<= (- C F) (- 1))
        (<= (- A F) (- 1))
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A C) 1)
        (<= (- C F) (- 1))
        (<= (- A F) (- 1))
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E true)
        (= D false)
        (= B false)
        (>= (- A C) 1)
        (<= (- C F) (- 1))
        (<= (- A F) (- 1))
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        (>= (- A C) 1)
        (<= (- C H) (- 1))
        (<= (- A H) (- 1))
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A C) 1)
        (<= (- F G) (- 1))
        (<= (- C H) (- 1))
        (<= (- A H) (- 1))
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- A C) 1)
        (<= (- C F) (- 1))
        (<= (- A F) (- 1))
        (new25 E)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (>= (- A C) 1)
        (<= (- C A) (- 1))
        (new25 B)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (>= (- A C) 1)
        (<= (- C A) (- 1))
        (new25 B)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E true)
        (= D false)
        (>= (- A C) 1)
        (<= (- C A) (- 1))
        (new25 B)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (>= (- F G) 1)
        (>= (- A C) 1)
        (<= (- C A) (- 1))
        (new25 B)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (>= (- A C) 1)
        (<= (- F G) (- 1))
        (<= (- C A) (- 1))
        (new25 B)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= D false)
        (>= (- A C) 1)
        (<= (- C A) (- 1))
        (new25 E)
        (new25 B)
      )
      (new37 A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (>= (- B E) 1)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (>= (- B E) 1)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= C false)
        (= A false)
        (>= (- B E) 1)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (>= (- E F) 1)
        (>= (- B G) 1)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (>= (- B E) 1)
        (<= (- F G) (- 1))
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- B E) 1)
        (new25 D)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (<= (- B E) (- 1))
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (<= (- B E) (- 1))
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= C false)
        (= A false)
        (<= (- B E) (- 1))
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (>= (- E F) 1)
        (<= (- B G) (- 1))
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (<= (- E F) (- 1))
        (<= (- B G) (- 1))
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- B E) (- 1))
        (new25 D)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= D false)
        (= A false)
        inst_fold
        (new25 C)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= D false)
        (= A false)
        (new6 C)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= D true)
        (= A false)
        (new6 C)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Int) )
    (=>
      (and
        (= D false)
        (= A false)
        (>= (- E F) 1)
        inst_fold
        (new25 C)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Int) )
    (=>
      (and
        (= D false)
        (= A false)
        (<= (- E F) (- 1))
        inst_fold
        (new25 C)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= A false)
        (new101 D E C)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A true)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A true)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= D true)
        (= C false)
        (= A true)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A true)
        (>= (- E F) 1)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) (F Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A true)
        (<= (- E F) (- 1))
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= C false)
        (= A true)
        (new25 D)
      )
      (new28 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A false)
      (new25 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A false)
      (new25 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A true)
      (new25 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (>= (- B C) 1)
      )
      (new25 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (<= (- B C) (- 1))
      )
      (new25 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (new25 A)
      (new25 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) )
    (=>
      (and
        (= C true)
        (= B false)
      )
      (new21 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= (- A D) 1)
      )
      (new21 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (<= (- A D) (- 1))
      )
      (new21 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) )
    (=>
      (and
        (= C false)
        (new25 B)
      )
      (new21 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D false)
        (= B false)
      )
      (new20 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- C E) 1)
        (>= (- A E) 1)
      )
      (new20 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- A E) 1)
        (<= (- C E) (- 1))
      )
      (new20 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new25 D)
      )
      (new20 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- C E) 1)
        (<= (- A E) (- 1))
      )
      (new20 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (<= (- C E) (- 1))
        (<= (- A E) (- 1))
      )
      (new20 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new25 D)
      )
      (new20 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D false)
        (>= (- C A) 1)
        (new25 B)
      )
      (new20 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D false)
        (<= (- C A) (- 1))
        (new25 B)
      )
      (new20 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) )
    (=>
      (new57 C B)
      (new20 A B A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (>= A 1)
        inst_fold
        (new25 C)
      )
      (new16 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) (E Bool) (F Int) )
    (=>
      (and
        (>= A 1)
        (diff_new144 D E B F C)
        (new16 A D E)
      )
      (new16 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (>= B 1)
        (new16 B A C)
      )
      (diff_new15 A A B B C C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) )
    (=>
      (and
        (= C true)
        (= D true)
        (= B true)
        (>= A 1)
        (>= A 1)
      )
      (new13 A B A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D true)
        (= E true)
        (= C false)
        (= B false)
        (>= (- F A) 1)
        (>= F 1)
        (>= F 1)
        (>= A 1)
      )
      (new13 A B A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D true)
        (= E true)
        (= C false)
        (= B false)
        (>= F 1)
        (>= F 1)
        (>= A 1)
        (<= (- F A) (- 1))
      )
      (new13 A B A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= D true)
        (= E true)
        (= B false)
        (>= A 1)
        (>= A 1)
        (>= A 1)
        (new11 A C)
      )
      (new13 A B A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= E false)
        (>= A 1)
        (<= F 0)
        (<= F 0)
        (new13 A B A C)
      )
      (new13 A B A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) )
    (=>
      (and
        (= C true)
        (= B false)
        (>= A 1)
        (>= A 1)
      )
      (new11 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= B false)
        (>= D 1)
        (>= A 1)
      )
      (new11 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= A 1)
        (<= D 0)
        (new11 A B)
      )
      (new11 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (>= B 1)
      )
      (new10 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A false)
        (>= B 1)
      )
      (new10 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= A 1)
        (<= (- A F) (- 1))
        (<= (- A F) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= A 1)
        (new20 F E G D)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C true)
        (= B false)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C true)
        (= B false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C true)
        (= B false)
        (>= A 1)
        (<= (- A F) (- 1))
        (<= (- A F) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= C true)
        (= B false)
        (>= A 1)
        (new21 F E D)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= A 1)
        (<= (- A F) (- 1))
        (<= (- A F) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= A 1)
        (new6 D)
      )
      (diff_new8 A A B C D D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- A H) 1)
        (>= (- A H) 1)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
        (<= (- A H) (- 1))
        (<= (- A H) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
        (new21 F D E)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= A 1)
        (<= (- F G) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (>= A 1)
        (<= (- G H) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= A 1)
        (<= (- F G) (- 1))
        (<= (- A H) (- 1))
        (<= (- A H) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= A 1)
        (<= (- F G) (- 1))
        (new21 F D E)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= A 1)
        (new25 C)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (>= A 1)
        (new25 C)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= A 1)
        (<= (- A F) (- 1))
        (<= (- A F) (- 1))
        (new25 C)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= B false)
        (>= A 1)
        (new28 E F D C)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B true)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B true)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B true)
        (>= A 1)
        (<= (- A F) (- 1))
        (<= (- A F) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= C false)
        (= B true)
        (>= A 1)
        (new21 F D E)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C true)
        (= B true)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C true)
        (= B true)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C true)
        (= B true)
        (>= A 1)
        (<= (- A F) (- 1))
        (<= (- A F) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) )
    (=>
      (and
        (= C true)
        (= B true)
        (>= A 1)
        (new6 D)
      )
      (diff_new8 A A B C D D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- A H) 1)
        (>= (- A H) 1)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
        (<= (- A H) (- 1))
        (<= (- A H) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
        (new21 F E D)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- H G) 1)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- H G) 1)
        (>= (- A I) 1)
        (>= (- A I) 1)
        (>= A 1)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- H G) 1)
        (>= A 1)
        (<= (- A I) (- 1))
        (<= (- A I) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- H G) 1)
        (>= A 1)
        (new20 H E F D)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
        (<= (- H G) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- A H) 1)
        (>= (- A H) 1)
        (>= A 1)
        (<= (- I G) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
        (<= (- H G) (- 1))
        (<= (- A I) (- 1))
        (<= (- A I) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
        (<= (- H G) (- 1))
        (new20 F E H D)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
        (new25 C)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        (>= (- A H) 1)
        (>= (- A H) 1)
        (>= A 1)
        (new25 C)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
        (<= (- A H) (- 1))
        (<= (- A H) (- 1))
        (new25 C)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
        (new37 F E G D C)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= A 1)
        (<= (- F G) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (>= A 1)
        (<= (- G H) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= A 1)
        (<= (- F G) (- 1))
        (<= (- A H) (- 1))
        (<= (- A H) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= A 1)
        (<= (- F G) (- 1))
        (new21 F E D)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
        (<= (- H G) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- A H) 1)
        (>= (- A H) 1)
        (>= A 1)
        (<= (- I G) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
        (<= (- H G) (- 1))
        (<= (- A I) (- 1))
        (<= (- A I) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= A 1)
        (<= (- H G) (- 1))
        (new20 H E F D)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= A 1)
        (<= (- F G) (- 1))
        (<= (- H G) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (>= A 1)
        (<= (- G H) (- 1))
        (<= (- I H) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
        (>= A 1)
        (<= (- F G) (- 1))
        (<= (- H G) (- 1))
        (<= (- A I) (- 1))
        (<= (- A I) (- 1))
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= C false)
        (= B false)
        (>= A 1)
        (<= (- F G) (- 1))
        (<= (- H G) (- 1))
        (new20 H E F D)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= A 1)
        (<= (- F G) (- 1))
        (new25 C)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (>= A 1)
        (<= (- G H) (- 1))
        (new25 C)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= A 1)
        (<= (- F G) (- 1))
        (<= (- A H) (- 1))
        (<= (- A H) (- 1))
        (new25 C)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= B false)
        (>= A 1)
        (<= (- F G) (- 1))
        (new44 F E G D C)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= A 1)
        (new25 B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (>= A 1)
        (new25 B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= A 1)
        (<= (- A F) (- 1))
        (<= (- A F) (- 1))
        (new25 B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= C false)
        (>= A 1)
        (new28 D F E B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= (- F G) 1)
        (>= A 1)
        (new25 B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= (- F G) 1)
        (>= (- A H) 1)
        (>= (- A H) 1)
        (>= A 1)
        (new25 B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= (- F G) 1)
        (>= A 1)
        (<= (- A H) (- 1))
        (<= (- A H) (- 1))
        (new25 B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (>= (- F G) 1)
        (>= A 1)
        (new37 F D G E B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= A 1)
        (<= (- F G) (- 1))
        (new25 B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (>= A 1)
        (<= (- G H) (- 1))
        (new25 B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (>= A 1)
        (<= (- F G) (- 1))
        (<= (- A H) (- 1))
        (<= (- A H) (- 1))
        (new25 B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= C false)
        (>= A 1)
        (<= (- F G) (- 1))
        (new44 F D G E B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (>= A 1)
        (new57 C B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (>= (- A F) 1)
        (>= (- A F) 1)
        (>= A 1)
        (new57 C B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= D false)
        (>= A 1)
        (<= (- A F) (- 1))
        (<= (- A F) (- 1))
        (new57 C B)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (>= A 1)
        (new60 F F C B E D)
      )
      (diff_new8 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A false)
      (new6 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A true)
      (new6 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (<= B 0)
        (<= B 0)
        (new6 A)
      )
      (diff_new5 A B A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Bool) (I Bool) )
    (=>
      (and
        (= D true)
        (= E true)
        (>= F 1)
        (<= B 0)
        (diff_new8 F G H I A C)
        (diff_new5 I B H)
      )
      (diff_new5 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= E false)
        (<= F 0)
        (<= F 0)
        (<= B 0)
        (diff_new5 A B C)
      )
      (diff_new5 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) )
    (=>
      (and
        (= C true)
        (= D true)
        (= B true)
        (>= A 1)
        (>= A 1)
      )
      (diff_new3 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= C false)
        (= B false)
        (>= (- A E) 1)
        (>= A 1)
        (>= A 1)
      )
      (diff_new3 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= C false)
        (= B false)
        (>= A 1)
        (>= A 1)
        (<= (- A E) (- 1))
      )
      (diff_new3 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) )
    (=>
      (and
        (= D true)
        (= B false)
        (>= A 1)
        (>= A 1)
        (new10 C A)
      )
      (diff_new3 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D true)
        (= E true)
        (= C false)
        (= B false)
        (>= (- F A) 1)
        (>= F 1)
        (>= F 1)
        (>= A 1)
      )
      (diff_new3 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D true)
        (= E true)
        (= C false)
        (= B false)
        (>= F 1)
        (>= F 1)
        (>= A 1)
        (<= (- F A) (- 1))
      )
      (diff_new3 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= D true)
        (= E true)
        (= B false)
        (>= A 1)
        (>= A 1)
        (>= A 1)
        (new11 A C)
      )
      (diff_new3 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= D true)
        (= E true)
        (= C false)
        (= B false)
        (>= (- F G) 1)
        (>= (- F G) 1)
        (>= F 1)
        (>= F 1)
        (>= A 1)
      )
      (diff_new3 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) )
    (=>
      (and
        (= D true)
        (= E true)
        (= C false)
        (= B false)
        (>= F 1)
        (>= F 1)
        (>= A 1)
        (<= (- F G) (- 1))
        (<= (- F G) (- 1))
      )
      (diff_new3 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D true)
        (= E true)
        (>= F 1)
        (>= F 1)
        (>= A 1)
        (diff_new3 A A B C)
      )
      (diff_new3 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= E false)
        (>= A 1)
        (<= F 0)
        (<= F 0)
        (new13 A B A C)
      )
      (diff_new3 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) (G Int) (H Int) (I Int) (J Bool) )
    (=>
      (and
        (= D false)
        (= E false)
        (>= A 1)
        (<= F 0)
        (diff_new15 G H A I J C)
        inst_fold
        (diff_new3 A A B J)
      )
      (diff_new3 A A B C)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A true)
      (new1 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) (E Bool) )
    (=>
      (and
        (= B true)
        (>= C 1)
        (diff_new3 C D E A)
        (new1 E)
      )
      (new1 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= B false)
        (<= C 0)
        (diff_new5 D C A)
        (new1 D)
      )
      (new1 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (and
        (= A false)
        (new1 A)
      )
      ff
    )
  )
)
(assert
    inst_fold
)

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