; Automatically generated by map2smt

(set-logic HORN)




(declare-fun new79 (Int Bool) Bool)
(declare-fun new78 (Int Bool) Bool)
(declare-fun new77 (Int Int Bool) Bool)
(declare-fun new7 (Int Bool) Bool)
(declare-fun new6 (Int Bool) Bool)
(declare-fun new5 (Int Int Bool) Bool)
(declare-fun new4 (Int Bool Int Int Bool) Bool)
(declare-fun new39 (Int Int Bool) Bool)
(declare-fun new37 (Int Bool) Bool)
(declare-fun new35 (Int Int Bool) Bool)
(declare-fun new34 (Int Int Bool) Bool)
(declare-fun new33 (Int Bool) Bool)
(declare-fun new3 (Int Bool Int Int Bool) Bool)
(declare-fun new2 (Int Bool Int Int Bool) Bool)
(declare-fun new113 (Int Bool) Bool)
(declare-fun new112 (Int Int Bool) Bool)
(declare-fun new111 (Int Bool) Bool)
(declare-fun new1 (Int Bool Int Int Bool) Bool)
(declare-fun ff () Bool)

(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new113 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new113 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new113 A B)
      )
      (new113 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new113 A B)
      )
      (new113 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new113 A B)
        (new113 A B)
      )
      (new113 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new113 A B)
        (new113 A B)
      )
      (new113 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= C false)
        (= C false)
        (>= (- A B) 1)
        (<= (- B A) (- 1))
      )
      (new112 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (<= B (- A 1))
      )
      (new112 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (<= D (- A 1))
        (new111 B C)
      )
      (new112 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (<= D (- A 1))
        (new112 A B C)
      )
      (new112 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- B D) 1)
        (>= (- A B) 1)
        (<= D (- A 1))
        (new111 B C)
        (new112 A B C)
      )
      (new112 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- A B) 1)
        (<= (- B D) (- 1))
        (<= D (- A 1))
        (new111 B C)
        (new112 A B C)
      )
      (new112 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (>= D A)
        (new112 A B C)
      )
      (new112 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (>= D A)
        (new111 B C)
      )
      (new112 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- A B) 1)
        (>= D A)
        (<= (- B D) (- 1))
        (new112 A B C)
        (new111 B C)
      )
      (new112 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new111 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new111 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new111 A B)
      )
      (new111 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new111 A B)
      )
      (new111 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new111 A B)
        (new111 A B)
      )
      (new111 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new111 A B)
        (new111 A B)
      )
      (new111 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new79 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new79 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new79 A B)
      )
      (new79 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new79 A B)
      )
      (new79 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new79 A B)
        (new79 A B)
      )
      (new79 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new79 A B)
        (new79 A B)
      )
      (new79 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new78 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new78 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new78 A B)
      )
      (new78 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new78 A B)
      )
      (new78 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new78 A B)
        (new78 A B)
      )
      (new78 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new78 A B)
        (new78 A B)
      )
      (new78 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= C false)
        (= C false)
        (>= (- B A) 1)
        (<= (- A B) (- 1))
      )
      (new77 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (<= (- A B) (- 1))
        (<= D (- A 1))
        (new78 B C)
      )
      (new77 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (<= (- A B) (- 1))
        (<= D (- A 1))
        (new77 A B C)
      )
      (new77 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- B D) 1)
        (<= (- A B) (- 1))
        (<= D (- A 1))
        (new78 B C)
        (new77 A B C)
      )
      (new77 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (>= B A)
        (<= (- A B) (- 1))
      )
      (new77 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= D A)
        (<= (- A B) (- 1))
        (new77 A B C)
      )
      (new77 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= D A)
        (<= (- A B) (- 1))
        (new78 B C)
      )
      (new77 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- B D) 1)
        (>= D A)
        (<= (- A B) (- 1))
        (new77 A B C)
        (new78 B C)
      )
      (new77 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= D A)
        (<= (- B D) (- 1))
        (<= (- A B) (- 1))
        (new77 A B C)
        (new78 B C)
      )
      (new77 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new39 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= C false)
        (= C false)
        (>= (- B A) 1)
      )
      (new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= C false)
        (= C false)
        (<= (- B A) (- 1))
      )
      (new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (<= B (- A 1))
      )
      (new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (<= D (- A 1))
        (new33 B C)
      )
      (new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (<= D (- A 1))
        (new39 A B C)
      )
      (new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- B D) 1)
        (<= D (- A 1))
        (new33 B C)
        (new39 A B C)
      )
      (new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (<= (- B D) (- 1))
        (<= D (- A 1))
        (new33 B C)
        (new34 A B C)
      )
      (new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (>= B A)
      )
      (new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= D A)
        (new39 A B C)
      )
      (new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= D A)
        (new33 B C)
      )
      (new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- B D) 1)
        (>= D A)
        (new35 A B C)
        (new33 B C)
      )
      (new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= D A)
        (<= (- B D) (- 1))
        (new39 A B C)
        (new33 B C)
      )
      (new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new37 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new37 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new37 A B)
      )
      (new37 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new37 A B)
      )
      (new37 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new37 A B)
        (new37 A B)
      )
      (new37 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new37 A B)
        (new37 A B)
      )
      (new37 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (<= (- A A) 0)
      )
      (new35 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= C false)
        (= C false)
        (>= (- B A) 1)
        (<= (- A B) 0)
      )
      (new35 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (<= (- A B) 0)
        (<= D (- A 1))
        (new33 B C)
      )
      (new35 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (<= (- A B) 0)
        (<= D (- A 1))
        (new35 A B C)
      )
      (new35 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- B D) 1)
        (<= (- A B) 0)
        (<= D (- A 1))
        (new33 B C)
        (new35 A B C)
      )
      (new35 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (>= B A)
        (<= (- A B) 0)
      )
      (new35 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= D A)
        (<= (- A B) 0)
        (new35 A B C)
      )
      (new35 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= D A)
        (<= (- A B) 0)
        (new33 B C)
      )
      (new35 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- B D) 1)
        (>= D A)
        (<= (- A B) 0)
        (new35 A B C)
        (new33 B C)
      )
      (new35 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= D A)
        (<= (- B D) (- 1))
        (<= (- A B) 0)
        (new35 A B C)
        (new33 B C)
      )
      (new35 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= C false)
        (= C false)
        (>= (- A B) 1)
        (<= (- B A) (- 1))
      )
      (new34 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (<= B (- A 1))
      )
      (new34 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (<= D (- A 1))
        (new33 B C)
      )
      (new34 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (<= D (- A 1))
        (new34 A B C)
      )
      (new34 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- B D) 1)
        (>= (- A B) 1)
        (<= D (- A 1))
        (new33 B C)
        (new34 A B C)
      )
      (new34 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- A B) 1)
        (<= (- B D) (- 1))
        (<= D (- A 1))
        (new33 B C)
        (new34 A B C)
      )
      (new34 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (>= D A)
        (new34 A B C)
      )
      (new34 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (>= D A)
        (new33 B C)
      )
      (new34 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- A B) 1)
        (>= D A)
        (<= (- B D) (- 1))
        (new34 A B C)
        (new33 B C)
      )
      (new34 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new33 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new33 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new33 A B)
      )
      (new33 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new33 A B)
      )
      (new33 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new33 A B)
        (new33 A B)
      )
      (new33 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new33 A B)
        (new33 A B)
      )
      (new33 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new7 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new7 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new7 A B)
      )
      (new7 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new7 A B)
      )
      (new7 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new7 A B)
        (new7 A B)
      )
      (new7 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new7 A B)
        (new7 A B)
      )
      (new7 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new6 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new6 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new6 A B)
      )
      (new6 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new6 A B)
      )
      (new6 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new6 A B)
        (new6 A B)
      )
      (new6 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new6 A B)
        (new6 A B)
      )
      (new6 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new5 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (<= C (- A 1))
        (new6 A B)
      )
      (new5 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (<= C (- A 1))
        (new5 A A B)
      )
      (new5 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (<= C (- A 1))
        (new6 A B)
        (new5 A A B)
      )
      (new5 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (>= A A)
      )
      (new5 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (>= C A)
        (new5 A A B)
      )
      (new5 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (>= C A)
        (new6 A B)
      )
      (new5 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= C A)
        (<= (- A C) (- 1))
        (new5 A A B)
        (new6 A B)
      )
      (new5 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) )
    (=>
      (and
        (= C true)
        (= B false)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) )
    (=>
      (and
        (= C true)
        (= B true)
        (>= A A)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) )
    (=>
      (and
        (= C true)
        (= B true)
        (>= A A)
        (new5 A A C)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) )
    (=>
      (and
        (= C true)
        (= B true)
        (>= A A)
        (new6 A C)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (<= C (- A 1))
        (new7 A B)
      )
      (new4 A B A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= B true)
        (<= D (- A 1))
        (new5 A A C)
        (new7 A B)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) )
    (=>
      (and
        (= C true)
        (= B true)
        (>= A A)
        (new7 A B)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= B true)
        (>= D A)
        (new4 A B A A C)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= B true)
        (>= D A)
        (new6 A C)
        (new7 A B)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= B true)
        (>= D A)
        (<= (- A D) (- 1))
        (new4 A B A A C)
        (new6 A C)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= B true)
        (<= D (- A 1))
        (new6 A C)
        (new7 A B)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= B true)
        (<= D (- A 1))
        (new4 A B A A C)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (= B true)
        (>= (- A D) 1)
        (<= D (- A 1))
        (new4 A B A A C)
        (new6 A C)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) )
    (=>
      (and
        (= C true)
        (= B true)
        (>= A A)
        (new7 A B)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= B true)
        (>= D A)
        (new5 A A C)
        (new7 A B)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= C A)
        (new7 A B)
      )
      (new4 A B A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= B false)
        (>= (- A D) 1)
        (<= D (- A 1))
        (new4 A B A A C)
        (new7 A B)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= (- A C) 1)
        (>= (- A C) 1)
        (<= C (- A 1))
        (new4 A B A A B)
        (new7 A B)
      )
      (new4 A B A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (= B false)
        (>= D A)
        (<= (- A D) (- 1))
        (new4 A B A A C)
        (new7 A B)
      )
      (new4 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= C A)
        (<= (- A C) (- 1))
        (<= (- A C) (- 1))
        (new4 A B A A B)
        (new7 A B)
      )
      (new4 A B A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Bool) )
    (=>
      (and
        (= C true)
        (= B false)
      )
      (new3 A B A A C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D false)
        (= D false)
        (= D false)
        (= B false)
        (>= (- A C) 1)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D false)
        (= D false)
        (= D false)
        (= B false)
        (<= (- A C) (- 1))
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= A (- C 1))
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= A (- C 1))
        (new33 A D)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= A (- C 1))
        (new34 C A D)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= A C)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= A C)
        (new35 C A D)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= A C)
        (new33 A D)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= A (- C 1))
        (new37 A B)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (<= D (- C 1))
        (new37 A B)
      )
      (new3 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= E (- C 1))
        (new39 C A D)
        (new37 A B)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= A C)
        (new37 A B)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= E C)
        (new3 A B C A D)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= E C)
        (new33 A D)
        (new37 A B)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B true)
        (>= (- A E) 1)
        (>= E C)
        (new3 A B C A D)
        (new33 A D)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B true)
        (>= E C)
        (<= (- A E) (- 1))
        (new3 A B C A D)
        (new33 A D)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= A (- C 1))
        (new37 A B)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= E (- C 1))
        (new33 A D)
        (new37 A B)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= E (- C 1))
        (new3 A B C A D)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B true)
        (>= (- A E) 1)
        (<= E (- C 1))
        (new3 A B C A D)
        (new33 A D)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B true)
        (<= (- A E) (- 1))
        (<= E (- C 1))
        (new3 A B C A D)
        (new33 A D)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= A C)
        (new37 A B)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= E C)
        (new39 C A D)
        (new37 A B)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= D C)
        (new37 A B)
      )
      (new3 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B false)
        (>= (- A E) 1)
        (<= E (- C 1))
        (new3 A B C A D)
        (new37 A B)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= (- A D) 1)
        (>= (- A D) 1)
        (<= D (- C 1))
        (new3 A B C A B)
        (new37 A B)
      )
      (new3 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B false)
        (>= (- A E) 1)
        (>= E C)
        (new3 A B C A D)
        (new37 A B)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= (- A D) 1)
        (>= (- A D) 1)
        (>= D C)
        (new3 A B C A B)
        (new37 A B)
      )
      (new3 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B false)
        (<= (- A E) (- 1))
        (<= E (- C 1))
        (new3 A B C A D)
        (new37 A B)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (<= (- A D) (- 1))
        (<= (- A D) (- 1))
        (<= D (- C 1))
        (new3 A B C A B)
        (new37 A B)
      )
      (new3 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B false)
        (>= E C)
        (<= (- A E) (- 1))
        (new3 A B C A D)
        (new37 A B)
      )
      (new3 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= D C)
        (<= (- A D) (- 1))
        (<= (- A D) (- 1))
        (new3 A B C A B)
        (new37 A B)
      )
      (new3 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D false)
        (= D false)
        (= D false)
        (= B false)
        (>= (- A C) 1)
        (>= (- A C) 1)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= (- A C) 1)
        (>= A C)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= (- A C) 1)
        (>= A C)
        (new77 C A D)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= (- A C) 1)
        (>= A C)
        (new78 A D)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= (- A C) 1)
        (<= D (- C 1))
        (new79 A B)
      )
      (new2 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= (- A C) 1)
        (<= E (- C 1))
        (new77 C A D)
        (new79 A B)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= (- A C) 1)
        (>= A C)
        (new79 A B)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= (- A C) 1)
        (>= E C)
        (new2 A B C A D)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= (- A C) 1)
        (>= E C)
        (new78 A D)
        (new79 A B)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B true)
        (>= (- A E) 1)
        (>= (- A C) 1)
        (>= E C)
        (new2 A B C A D)
        (new78 A D)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B true)
        (>= (- A C) 1)
        (>= E C)
        (<= (- A E) (- 1))
        (new2 A B C A D)
        (new78 A D)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= (- A C) 1)
        (<= E (- C 1))
        (new78 A D)
        (new79 A B)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= (- A C) 1)
        (<= E (- C 1))
        (new2 A B C A D)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B true)
        (>= (- A E) 1)
        (>= (- A C) 1)
        (<= E (- C 1))
        (new2 A B C A D)
        (new78 A D)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= (- A C) 1)
        (>= A C)
        (new79 A B)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= (- A C) 1)
        (>= E C)
        (new77 C A D)
        (new79 A B)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= (- A C) 1)
        (>= D C)
        (new79 A B)
      )
      (new2 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B false)
        (>= (- A E) 1)
        (>= (- A C) 1)
        (<= E (- C 1))
        (new2 A B C A D)
        (new79 A B)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= (- A D) 1)
        (>= (- A D) 1)
        (>= (- A C) 1)
        (<= D (- C 1))
        (new2 A B C A B)
        (new79 A B)
      )
      (new2 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B false)
        (>= (- A E) 1)
        (>= (- A C) 1)
        (>= E C)
        (new2 A B C A D)
        (new79 A B)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= (- A D) 1)
        (>= (- A D) 1)
        (>= (- A C) 1)
        (>= D C)
        (new2 A B C A B)
        (new79 A B)
      )
      (new2 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B false)
        (>= (- A C) 1)
        (>= E C)
        (<= (- A E) (- 1))
        (new2 A B C A D)
        (new79 A B)
      )
      (new2 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= (- A C) 1)
        (>= D C)
        (<= (- A D) (- 1))
        (<= (- A D) (- 1))
        (new2 A B C A B)
        (new79 A B)
      )
      (new2 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D false)
        (= D false)
        (= D false)
        (= B false)
        (<= (- A C) (- 1))
        (<= (- A C) (- 1))
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= (- A C) (- 1))
        (<= A (- C 1))
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= (- A C) (- 1))
        (<= A (- C 1))
        (new111 A D)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= (- A C) (- 1))
        (<= A (- C 1))
        (new112 C A D)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= (- A C) (- 1))
        (<= A (- C 1))
        (new113 A B)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (<= (- A C) (- 1))
        (<= D (- C 1))
        (new113 A B)
      )
      (new1 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= (- A C) (- 1))
        (<= E (- C 1))
        (new112 C A D)
        (new113 A B)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= E C)
        (<= (- A C) (- 1))
        (new1 A B C A D)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= E C)
        (<= (- A C) (- 1))
        (new111 A D)
        (new113 A B)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B true)
        (>= E C)
        (<= (- A E) (- 1))
        (<= (- A C) (- 1))
        (new1 A B C A D)
        (new111 A D)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= (- A C) (- 1))
        (<= A (- C 1))
        (new113 A B)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= (- A C) (- 1))
        (<= E (- C 1))
        (new111 A D)
        (new113 A B)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (<= (- A C) (- 1))
        (<= E (- C 1))
        (new1 A B C A D)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B true)
        (>= (- A E) 1)
        (<= (- A C) (- 1))
        (<= E (- C 1))
        (new1 A B C A D)
        (new111 A D)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D false)
        (= B true)
        (<= (- A E) (- 1))
        (<= (- A C) (- 1))
        (<= E (- C 1))
        (new1 A B C A D)
        (new111 A D)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B true)
        (>= E C)
        (<= (- A C) (- 1))
        (new112 C A D)
        (new113 A B)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B true)
        (= B true)
        (>= D C)
        (<= (- A C) (- 1))
        (new113 A B)
      )
      (new1 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B false)
        (>= (- A E) 1)
        (<= (- A C) (- 1))
        (<= E (- C 1))
        (new1 A B C A D)
        (new113 A B)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= (- A D) 1)
        (>= (- A D) 1)
        (<= (- A C) (- 1))
        (<= D (- C 1))
        (new1 A B C A B)
        (new113 A B)
      )
      (new1 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B false)
        (<= (- A E) (- 1))
        (<= (- A C) (- 1))
        (<= E (- C 1))
        (new1 A B C A D)
        (new113 A B)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (<= (- A D) (- 1))
        (<= (- A D) (- 1))
        (<= (- A C) (- 1))
        (<= D (- C 1))
        (new1 A B C A B)
        (new113 A B)
      )
      (new1 A B C A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Bool) (E Int) )
    (=>
      (and
        (= D true)
        (= B false)
        (>= E C)
        (<= (- A E) (- 1))
        (<= (- A C) (- 1))
        (new1 A B C A D)
        (new113 A B)
      )
      (new1 A B C A D)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= B false)
        (= B false)
        (>= D C)
        (<= (- A D) (- 1))
        (<= (- A D) (- 1))
        (<= (- A C) (- 1))
        (new1 A B C A B)
        (new113 A B)
      )
      (new1 A B C A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= A true)
        (= B false)
        (>= (- C D) 1)
        (new1 D B C D A)
      )
      ff
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= A true)
        (= B false)
        (<= (- C D) (- 1))
        (new2 D B C D A)
      )
      ff
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= B true)
        (new3 C B D C A)
      )
      ff
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Bool) )
    (=>
      (and
        (= A false)
        (new4 B C B B A)
      )
      ff
    )
  )
)

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