; Automatically generated by map2smt

(set-logic HORN)




(declare-fun new9 (Bool) Bool)
(declare-fun new67 (Bool Int Bool) Bool)
(declare-fun new5 (Int Bool) Bool)
(declare-fun new46 (Bool Bool) Bool)
(declare-fun new33 (Int Bool Int Bool Bool) Bool)
(declare-fun new26 (Int Bool Int Bool Bool) Bool)
(declare-fun new2 (Bool) Bool)
(declare-fun new16 (Int Bool Int Bool) Bool)
(declare-fun new15 (Bool Int Bool Bool) Bool)
(declare-fun new12 (Bool) Bool)
(declare-fun new10 (Bool Int Bool) Bool)
(declare-fun new1 (Bool) Bool)
(declare-fun diff_new7 (Int Int Bool Bool Bool Bool) Bool)
(declare-fun diff_new4 (Int Int Bool Bool) Bool)
(declare-fun not_fun_diff_new7 () Bool)
(declare-fun constr (Bool) Bool)
(declare-fun not_fun_diff_new4 () Bool)
(declare-fun inst_fold () Bool)
(declare-fun ff () Bool)

(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_new7 A B C D E F)
        (diff_new7 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_new7
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Bool) (E Int) (F Int) (G Bool) (H Bool) )
    (=>
      (and
        (diff_new4 A B C D)
        (diff_new4 E F G H)
        (and (and (= A E) (and (= B F) (= C G))) (not (= D H)))
      )
      not_fun_diff_new4
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- D B) 1)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- D B) (- 1))
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= A false)
        (new9 C)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A false)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- D B) 1)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- D B) (- 1))
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= A false)
        (new5 D C)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A true)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A true)
        (>= (- D B) 1)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A true)
        (<= (- D B) (- 1))
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= A true)
        (new9 C)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- D E) 1)
      )
      (new67 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)
      )
      (new67 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))
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (>= (- D E) 1)
        (new5 E C)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- D E) (- 1))
      )
      (new67 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))
      )
      (new67 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))
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (<= (- D E) (- 1))
        (new5 E C)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (new12 A)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- D B) 1)
        (new12 A)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (<= (- D B) (- 1))
        (new12 A)
      )
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (new67 A D C)
      (new67 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B false)
        (= A false)
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= (- C D) 1)
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (- C D) (- 1))
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= A false)
        (new12 B)
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B false)
        (= A false)
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B true)
        (= A false)
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B false)
        (= A true)
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B true)
        (= A true)
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (>= (- C D) 1)
      )
      (new46 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)
      )
      (new46 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))
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (>= (- C D) 1)
        (new12 B)
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= A false)
        (<= (- C D) (- 1))
      )
      (new46 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))
      )
      (new46 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))
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (<= (- C D) (- 1))
        (new12 B)
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (and
        (= B false)
        (new12 A)
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (>= (- C D) 1)
        (new12 A)
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (<= (- C D) (- 1))
        (new12 A)
      )
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) )
    (=>
      (new46 B A)
      (new46 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= B false)
        (>= (- A C) 1)
      )
      (new33 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)
      )
      (new33 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)
      )
      (new33 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)
      )
      (new33 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))
      )
      (new33 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)
        (new12 E)
      )
      (new33 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)
        (>= (- F C) 1)
        (>= (- F A) 1)
        (>= (- A C) 1)
      )
      (new33 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)
        (>= (- F C) 1)
        (>= (- F A) 1)
        (>= (- A C) 1)
      )
      (new33 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)
        (>= (- F C) 1)
        (>= (- F A) 1)
        (>= (- A C) 1)
      )
      (new33 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)
        (>= (- H C) 1)
        (>= (- H A) 1)
        (>= (- A C) 1)
      )
      (new33 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 C) 1)
        (>= (- F A) 1)
        (>= (- A C) 1)
        (<= (- G H) (- 1))
      )
      (new33 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- F C) 1)
        (>= (- F A) 1)
        (>= (- A C) 1)
        (new12 E)
      )
      (new33 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)
        (>= (- F C) 1)
        (>= (- A C) 1)
        (<= (- F A) (- 1))
      )
      (new33 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)
        (>= (- F C) 1)
        (>= (- A C) 1)
        (<= (- F A) (- 1))
      )
      (new33 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)
        (>= (- F C) 1)
        (>= (- A C) 1)
        (<= (- F A) (- 1))
      )
      (new33 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)
        (>= (- H C) 1)
        (>= (- A C) 1)
        (<= (- H A) (- 1))
      )
      (new33 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 C) 1)
        (>= (- A C) 1)
        (<= (- G H) (- 1))
        (<= (- F A) (- 1))
      )
      (new33 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- F C) 1)
        (>= (- A C) 1)
        (<= (- F A) (- 1))
        (new12 E)
      )
      (new33 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)
        (<= (- F C) (- 1))
        (<= (- F A) (- 1))
      )
      (new33 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)
        (<= (- F C) (- 1))
        (<= (- F A) (- 1))
      )
      (new33 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)
        (<= (- F C) (- 1))
        (<= (- F A) (- 1))
      )
      (new33 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)
        (<= (- H C) (- 1))
        (<= (- H A) (- 1))
      )
      (new33 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))
        (<= (- H C) (- 1))
        (<= (- H A) (- 1))
      )
      (new33 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)
        (<= (- F C) (- 1))
        (<= (- F A) (- 1))
        (new12 E)
      )
      (new33 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)
        (<= (- C A) (- 1))
        (new9 D)
      )
      (new33 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- A C) 1)
        (<= (- C A) (- 1))
        (new5 F D)
      )
      (new33 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)
        (<= (- C A) (- 1))
        (new9 D)
      )
      (new33 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)
        (<= (- C A) (- 1))
        (new5 G D)
      )
      (new33 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)
        (<= (- F G) (- 1))
        (<= (- C A) (- 1))
        (new5 G D)
      )
      (new33 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)
        (<= (- C A) (- 1))
        (new67 E F D)
      )
      (new33 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)
        (>= (- A C) 1)
        (new12 B)
      )
      (new33 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)
        (>= (- A C) 1)
        (new12 B)
      )
      (new33 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)
        (>= (- A C) 1)
        (new12 B)
      )
      (new33 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)
        (>= (- A C) 1)
        (new12 B)
      )
      (new33 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)
        (>= (- A C) 1)
        (<= (- F G) (- 1))
        (new12 B)
      )
      (new33 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= D false)
        (>= (- A C) 1)
        (>= (- A C) 1)
        (new12 E)
        (new12 B)
      )
      (new33 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))
      )
      (new26 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))
      )
      (new26 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))
      )
      (new26 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))
      )
      (new26 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))
      )
      (new26 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))
        (new12 E)
      )
      (new26 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)
        (>= (- F C) 1)
        (>= (- F A) 1)
        (<= (- A C) (- 1))
      )
      (new26 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)
        (>= (- F C) 1)
        (>= (- F A) 1)
        (<= (- A C) (- 1))
      )
      (new26 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)
        (>= (- F C) 1)
        (>= (- F A) 1)
        (<= (- A C) (- 1))
      )
      (new26 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)
        (>= (- H C) 1)
        (>= (- H A) 1)
        (<= (- A C) (- 1))
      )
      (new26 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 C) 1)
        (>= (- F A) 1)
        (<= (- G H) (- 1))
        (<= (- A C) (- 1))
      )
      (new26 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- F C) 1)
        (>= (- F A) 1)
        (<= (- A C) (- 1))
        (new12 E)
      )
      (new26 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)
        (>= (- F A) 1)
        (<= (- F C) (- 1))
        (<= (- A C) (- 1))
      )
      (new26 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)
        (>= (- F A) 1)
        (<= (- F C) (- 1))
        (<= (- A C) (- 1))
      )
      (new26 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)
        (>= (- F A) 1)
        (<= (- F C) (- 1))
        (<= (- A C) (- 1))
      )
      (new26 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)
        (>= (- H A) 1)
        (<= (- H C) (- 1))
        (<= (- A C) (- 1))
      )
      (new26 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 A) 1)
        (<= (- G H) (- 1))
        (<= (- F C) (- 1))
        (<= (- A C) (- 1))
      )
      (new26 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- F A) 1)
        (<= (- F C) (- 1))
        (<= (- A C) (- 1))
        (new12 E)
      )
      (new26 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- C A) 1)
        (<= (- A C) (- 1))
        (new9 D)
      )
      (new26 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= E false)
        (= B false)
        (>= (- C A) 1)
        (<= (- A C) (- 1))
        (new5 F D)
      )
      (new26 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= E true)
        (= B false)
        (>= (- C A) 1)
        (<= (- A C) (- 1))
        (new9 D)
      )
      (new26 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)
        (>= (- C A) 1)
        (<= (- A C) (- 1))
        (new5 G D)
      )
      (new26 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)
        (>= (- C A) 1)
        (<= (- F G) (- 1))
        (<= (- A C) (- 1))
        (new5 G D)
      )
      (new26 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= B false)
        (>= (- C A) 1)
        (<= (- A C) (- 1))
        (new67 E F D)
      )
      (new26 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)
        (<= (- F C) (- 1))
        (<= (- F A) (- 1))
        (<= (- A C) (- 1))
      )
      (new26 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)
        (<= (- F C) (- 1))
        (<= (- F A) (- 1))
        (<= (- A C) (- 1))
      )
      (new26 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)
        (<= (- F C) (- 1))
        (<= (- F A) (- 1))
        (<= (- A C) (- 1))
      )
      (new26 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)
        (<= (- H C) (- 1))
        (<= (- H A) (- 1))
        (<= (- A C) (- 1))
      )
      (new26 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))
        (<= (- H C) (- 1))
        (<= (- H A) (- 1))
        (<= (- A C) (- 1))
      )
      (new26 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (<= (- F C) (- 1))
        (<= (- F A) (- 1))
        (<= (- A C) (- 1))
        (new12 E)
      )
      (new26 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))
        (<= (- A C) (- 1))
        (new12 B)
      )
      (new26 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))
        (<= (- A C) (- 1))
        (new12 B)
      )
      (new26 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))
        (<= (- A C) (- 1))
        (new12 B)
      )
      (new26 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))
        (<= (- A C) (- 1))
        (new12 B)
      )
      (new26 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))
        (<= (- A C) (- 1))
        (new12 B)
      )
      (new26 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Bool) )
    (=>
      (and
        (= D false)
        (<= (- A C) (- 1))
        (<= (- A C) (- 1))
        (new12 E)
        (new12 B)
      )
      (new26 A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D false)
        (= B false)
      )
      (new16 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- E C) 1)
        (>= (- E A) 1)
      )
      (new16 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- E A) 1)
        (<= (- E C) (- 1))
      )
      (new16 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= B false)
        (>= (- C A) 1)
        (new12 D)
      )
      (new16 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (>= (- E C) 1)
        (<= (- E A) (- 1))
      )
      (new16 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B false)
        (<= (- E C) (- 1))
        (<= (- E A) (- 1))
      )
      (new16 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= B false)
        (<= (- C A) (- 1))
        (new12 D)
      )
      (new16 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D false)
        (>= (- A C) 1)
        (new12 B)
      )
      (new16 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D false)
        (<= (- A C) (- 1))
        (new12 B)
      )
      (new16 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) )
    (=>
      (new46 C B)
      (new16 A B A C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (>= (- E B) 1)
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (>= (- E B) 1)
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= C false)
        (= A false)
        (>= (- E B) 1)
      )
      (new15 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)
        (>= (- G B) 1)
      )
      (new15 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 B) 1)
        (<= (- F G) (- 1))
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- E B) 1)
        (new12 D)
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (<= (- E B) (- 1))
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A false)
        (<= (- E B) (- 1))
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= C false)
        (= A false)
        (<= (- E B) (- 1))
      )
      (new15 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)
        (<= (- G B) (- 1))
      )
      (new15 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))
        (<= (- G B) (- 1))
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- E B) (- 1))
        (new12 D)
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= D false)
        (= A false)
        (new9 C)
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= A false)
        (new5 E C)
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= D true)
        (= A false)
        (new9 C)
      )
      (new15 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)
        (new5 F C)
      )
      (new15 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))
        (new5 F C)
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) (E Int) )
    (=>
      (and
        (= A false)
        (new67 D E C)
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A true)
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= D false)
        (= C false)
        (= A true)
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= D true)
        (= C false)
        (= A true)
      )
      (new15 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)
      )
      (new15 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))
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Bool) )
    (=>
      (and
        (= C false)
        (= A true)
        (new12 D)
      )
      (new15 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A false)
      (new12 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A false)
      (new12 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A true)
      (new12 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (>= (- B C) 1)
      )
      (new12 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) )
    (=>
      (and
        (= A false)
        (<= (- B C) (- 1))
      )
      (new12 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (new12 A)
      (new12 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (>= (- D B) 1)
      )
      (new10 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= A false)
        (<= (- D B) (- 1))
      )
      (new10 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= A false)
        (new12 C)
      )
      (new10 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= A true)
      )
      (new10 A B C)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A false)
      (new9 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A true)
      (new9 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (= C false)
        (= B false)
      )
      (diff_new7 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)
        (>= (- F A) 1)
        (>= (- F A) 1)
      )
      (diff_new7 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)
        (<= (- F A) (- 1))
        (<= (- F A) (- 1))
      )
      (diff_new7 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) )
    (=>
      (and
        (= C false)
        (= B false)
        (new9 D)
      )
      (diff_new7 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)
      )
      (diff_new7 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 A) 1)
        (>= (- F A) 1)
        (>= (- G H) 1)
      )
      (diff_new7 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 A) (- 1))
        (<= (- H A) (- 1))
      )
      (diff_new7 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)
        (new10 E G D)
      )
      (diff_new7 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)
        (<= (- F G) (- 1))
      )
      (diff_new7 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 A) 1)
        (>= (- F A) 1)
        (<= (- G H) (- 1))
      )
      (diff_new7 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 A) (- 1))
        (<= (- F A) (- 1))
        (<= (- G H) (- 1))
      )
      (diff_new7 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))
        (new10 E G D)
      )
      (diff_new7 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)
        (new12 C)
      )
      (diff_new7 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)
        (>= (- F A) 1)
        (>= (- F A) 1)
        (new12 C)
      )
      (diff_new7 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)
        (<= (- F A) (- 1))
        (<= (- F A) (- 1))
        (new12 C)
      )
      (diff_new7 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= B false)
        (new15 E F D C)
      )
      (diff_new7 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)
      )
      (diff_new7 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)
        (>= (- F A) 1)
        (>= (- F A) 1)
      )
      (diff_new7 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)
        (<= (- F A) (- 1))
        (<= (- F A) (- 1))
      )
      (diff_new7 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)
        (new16 F E G D)
      )
      (diff_new7 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)
      )
      (diff_new7 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)
        (>= (- F A) 1)
        (>= (- F A) 1)
      )
      (diff_new7 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)
        (<= (- F A) (- 1))
        (<= (- F A) (- 1))
      )
      (diff_new7 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)
        (new10 D F E)
      )
      (diff_new7 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)
      )
      (diff_new7 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)
        (>= (- F A) 1)
        (>= (- F A) 1)
      )
      (diff_new7 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)
        (<= (- F A) (- 1))
        (<= (- F A) (- 1))
      )
      (diff_new7 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)
        (new10 E F D)
      )
      (diff_new7 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)
      )
      (diff_new7 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)
        (>= (- F A) 1)
        (>= (- F A) 1)
      )
      (diff_new7 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)
        (<= (- F A) (- 1))
        (<= (- F A) (- 1))
      )
      (diff_new7 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) )
    (=>
      (and
        (= C true)
        (= B true)
        (new9 D)
      )
      (diff_new7 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)
      )
      (diff_new7 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 A) 1)
        (>= (- F A) 1)
        (>= (- G H) 1)
      )
      (diff_new7 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 A) (- 1))
        (<= (- H A) (- 1))
      )
      (diff_new7 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)
        (new10 D G E)
      )
      (diff_new7 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)
        (>= (- F H) 1)
      )
      (diff_new7 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 A) 1)
        (>= (- F A) 1)
        (>= (- G H) 1)
        (>= (- G I) 1)
      )
      (diff_new7 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)
        (>= (- F H) 1)
        (<= (- I A) (- 1))
        (<= (- I A) (- 1))
      )
      (diff_new7 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)
        (>= (- F H) 1)
        (new16 H E G D)
      )
      (diff_new7 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)
        (<= (- F H) (- 1))
      )
      (diff_new7 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 A) 1)
        (>= (- F A) 1)
        (>= (- G H) 1)
        (<= (- G I) (- 1))
      )
      (diff_new7 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 A) (- 1))
        (<= (- H A) (- 1))
        (<= (- F I) (- 1))
      )
      (diff_new7 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)
        (<= (- F H) (- 1))
        (new16 G E H D)
      )
      (diff_new7 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)
        (new12 C)
      )
      (diff_new7 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 A) 1)
        (>= (- F A) 1)
        (>= (- G H) 1)
        (new12 C)
      )
      (diff_new7 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)
        (<= (- H A) (- 1))
        (<= (- H A) (- 1))
        (new12 C)
      )
      (diff_new7 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)
        (new26 G E F D C)
      )
      (diff_new7 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)
        (<= (- F G) (- 1))
      )
      (diff_new7 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 A) 1)
        (>= (- F A) 1)
        (<= (- G H) (- 1))
      )
      (diff_new7 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 A) (- 1))
        (<= (- F A) (- 1))
        (<= (- G H) (- 1))
      )
      (diff_new7 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))
        (new10 D G E)
      )
      (diff_new7 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)
        (<= (- F H) (- 1))
      )
      (diff_new7 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 A) 1)
        (>= (- F A) 1)
        (>= (- G H) 1)
        (<= (- G I) (- 1))
      )
      (diff_new7 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 A) (- 1))
        (<= (- H A) (- 1))
        (<= (- F I) (- 1))
      )
      (diff_new7 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)
        (<= (- F H) (- 1))
        (new16 H E G D)
      )
      (diff_new7 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))
        (<= (- F H) (- 1))
      )
      (diff_new7 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 A) 1)
        (>= (- F A) 1)
        (<= (- G H) (- 1))
        (<= (- G I) (- 1))
      )
      (diff_new7 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 A) (- 1))
        (<= (- F A) (- 1))
        (<= (- G H) (- 1))
        (<= (- G I) (- 1))
      )
      (diff_new7 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))
        (<= (- F H) (- 1))
        (new16 H E G D)
      )
      (diff_new7 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))
        (new12 C)
      )
      (diff_new7 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 A) 1)
        (>= (- F A) 1)
        (<= (- G H) (- 1))
        (new12 C)
      )
      (diff_new7 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 A) (- 1))
        (<= (- F A) (- 1))
        (<= (- G H) (- 1))
        (new12 C)
      )
      (diff_new7 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))
        (new33 G E F D C)
      )
      (diff_new7 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)
        (new12 B)
      )
      (diff_new7 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)
        (>= (- F A) 1)
        (>= (- F A) 1)
        (new12 B)
      )
      (diff_new7 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)
        (<= (- F A) (- 1))
        (<= (- F A) (- 1))
        (new12 B)
      )
      (diff_new7 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (and
        (= C false)
        (new15 D F E B)
      )
      (diff_new7 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)
        (new12 B)
      )
      (diff_new7 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 A) 1)
        (>= (- F A) 1)
        (>= (- G H) 1)
        (new12 B)
      )
      (diff_new7 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)
        (<= (- H A) (- 1))
        (<= (- H A) (- 1))
        (new12 B)
      )
      (diff_new7 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)
        (new26 G D F E B)
      )
      (diff_new7 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))
        (new12 B)
      )
      (diff_new7 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 A) 1)
        (>= (- F A) 1)
        (<= (- G H) (- 1))
        (new12 B)
      )
      (diff_new7 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 A) (- 1))
        (<= (- F A) (- 1))
        (<= (- G H) (- 1))
        (new12 B)
      )
      (diff_new7 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))
        (new33 G D F E B)
      )
      (diff_new7 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) )
    (=>
      (and
        (= E false)
        (= D false)
        (new46 C B)
      )
      (diff_new7 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)
        (>= (- F A) 1)
        (>= (- F A) 1)
        (new46 C B)
      )
      (diff_new7 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)
        (<= (- F A) (- 1))
        (<= (- F A) (- 1))
        (new46 C B)
      )
      (diff_new7 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Bool) (E Bool) (F Int) )
    (=>
      (diff_new7 F F C B E D)
      (diff_new7 A A B C D E)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- C A) 1)
      )
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- C A) (- 1))
      )
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (new12 B)
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (new5 A B)
      (diff_new4 A A B B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) (E Int) (F Bool) (G Bool) )
    (=>
      (and
        (diff_new7 D E F G B C)
        (diff_new4 A A G F)
      )
      (diff_new4 A A B C)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (= A true)
      (new2 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (new2 A)
      (new2 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (new2 A)
      (new1 A)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Bool) )
    (=>
      (and
        (diff_new4 B C D A)
        inst_fold
        (new1 D)
      )
      (new1 A)
    )
  )
)
(assert
  (forall ( (A Bool) )
    (=>
      (and
        (= A false)
        (new1 A)
      )
      ff
    )
  )
)
(assert
    inst_fold
)

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