; Automatically generated by map2smt

(set-logic HORN)




(declare-fun new93 (Int Bool) Bool)
(declare-fun new92 (Int Int Bool) Bool)
(declare-fun new91 (Int Bool) Bool)
(declare-fun new59 (Int Bool) Bool)
(declare-fun new58 (Int Bool) Bool)
(declare-fun new57 (Int Int Bool) Bool)
(declare-fun new5 (Int Bool) Bool)
(declare-fun new4 (Int Int Bool) Bool)
(declare-fun new3 (Int Bool Int Int Bool) Bool)
(declare-fun new2 (Int Bool Int Int Bool) Bool)
(declare-fun new19 (Int Int Bool) Bool)
(declare-fun new17 (Int Bool) Bool)
(declare-fun new15 (Int Int Bool) Bool)
(declare-fun new14 (Int Int Bool) Bool)
(declare-fun new13 (Int Bool) Bool)
(declare-fun new1 (Int Bool Int Int Bool) Bool)
(declare-fun ff () Bool)

(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new93 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new93 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new93 A B)
      )
      (new93 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new93 A B)
      )
      (new93 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new93 A B)
        (new93 A B)
      )
      (new93 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new93 A B)
        (new93 A B)
      )
      (new93 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= C false)
        (= C false)
        (>= (- A B) 1)
        (<= (- B A) (- 1))
      )
      (new92 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (<= B (- A 1))
      )
      (new92 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (<= D (- A 1))
        (new91 B C)
      )
      (new92 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (<= D (- A 1))
        (new92 A B C)
      )
      (new92 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))
        (new91 B C)
        (new92 A B C)
      )
      (new92 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))
        (new91 B C)
        (new92 A B C)
      )
      (new92 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (>= D A)
        (new92 A B C)
      )
      (new92 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (>= D A)
        (new91 B C)
      )
      (new92 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- A B) 1)
        (>= D A)
        (<= (- B D) (- 1))
        (new92 A B C)
        (new91 B C)
      )
      (new92 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new91 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new91 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new91 A B)
      )
      (new91 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new91 A B)
      )
      (new91 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new91 A B)
        (new91 A B)
      )
      (new91 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new91 A B)
        (new91 A B)
      )
      (new91 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new59 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new59 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new59 A B)
      )
      (new59 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new59 A B)
      )
      (new59 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new59 A B)
        (new59 A B)
      )
      (new59 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new59 A B)
        (new59 A B)
      )
      (new59 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new58 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new58 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new58 A B)
      )
      (new58 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new58 A B)
      )
      (new58 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new58 A B)
        (new58 A B)
      )
      (new58 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new58 A B)
        (new58 A B)
      )
      (new58 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= C false)
        (= C false)
        (>= (- B A) 1)
        (<= (- A B) (- 1))
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (<= (- A B) (- 1))
        (<= D (- A 1))
        (new58 B C)
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (<= (- A B) (- 1))
        (<= D (- A 1))
        (new57 A B C)
      )
      (new57 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))
        (new58 B C)
        (new57 A B C)
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (>= B A)
        (<= (- A B) (- 1))
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= D A)
        (<= (- A B) (- 1))
        (new57 A B C)
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= D A)
        (<= (- A B) (- 1))
        (new58 B C)
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- B D) 1)
        (>= D A)
        (<= (- A B) (- 1))
        (new57 A B C)
        (new58 B C)
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= D A)
        (<= (- B D) (- 1))
        (<= (- A B) (- 1))
        (new57 A B C)
        (new58 B C)
      )
      (new57 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new19 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= C false)
        (= C false)
        (>= (- B A) 1)
      )
      (new19 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= C false)
        (= C false)
        (<= (- B A) (- 1))
      )
      (new19 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (<= B (- A 1))
      )
      (new19 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (<= D (- A 1))
        (new13 B C)
      )
      (new19 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (<= D (- A 1))
        (new19 A B C)
      )
      (new19 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- B D) 1)
        (<= D (- A 1))
        (new13 B C)
        (new19 A B C)
      )
      (new19 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (<= (- B D) (- 1))
        (<= D (- A 1))
        (new13 B C)
        (new14 A B C)
      )
      (new19 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (>= B A)
      )
      (new19 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= D A)
        (new19 A B C)
      )
      (new19 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= D A)
        (new13 B C)
      )
      (new19 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- B D) 1)
        (>= D A)
        (new15 A B C)
        (new13 B C)
      )
      (new19 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= D A)
        (<= (- B D) (- 1))
        (new19 A B C)
        (new13 B C)
      )
      (new19 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new17 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new17 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new17 A B)
      )
      (new17 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new17 A B)
      )
      (new17 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new17 A B)
        (new17 A B)
      )
      (new17 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new17 A B)
        (new17 A B)
      )
      (new17 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (<= (- A A) 0)
      )
      (new15 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= C false)
        (= C false)
        (>= (- B A) 1)
        (<= (- A B) 0)
      )
      (new15 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (<= (- A B) 0)
        (<= D (- A 1))
        (new13 B C)
      )
      (new15 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (<= (- A B) 0)
        (<= D (- A 1))
        (new15 A B C)
      )
      (new15 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))
        (new13 B C)
        (new15 A B C)
      )
      (new15 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (>= B A)
        (<= (- A B) 0)
      )
      (new15 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= D A)
        (<= (- A B) 0)
        (new15 A B C)
      )
      (new15 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= D A)
        (<= (- A B) 0)
        (new13 B C)
      )
      (new15 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- B D) 1)
        (>= D A)
        (<= (- A B) 0)
        (new15 A B C)
        (new13 B C)
      )
      (new15 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= D A)
        (<= (- B D) (- 1))
        (<= (- A B) 0)
        (new15 A B C)
        (new13 B C)
      )
      (new15 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C false)
        (= C false)
        (= C false)
        (>= (- A B) 1)
        (<= (- B A) (- 1))
      )
      (new14 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (<= B (- A 1))
      )
      (new14 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (<= D (- A 1))
        (new13 B C)
      )
      (new14 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (<= D (- A 1))
        (new14 A B C)
      )
      (new14 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))
        (new13 B C)
        (new14 A B C)
      )
      (new14 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))
        (new13 B C)
        (new14 A B C)
      )
      (new14 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (>= D A)
        (new14 A B C)
      )
      (new14 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C true)
        (>= (- A B) 1)
        (>= D A)
        (new13 B C)
      )
      (new14 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) (D Int) )
    (=>
      (and
        (= C false)
        (>= (- A B) 1)
        (>= D A)
        (<= (- B D) (- 1))
        (new14 A B C)
        (new13 B C)
      )
      (new14 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new13 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new13 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new13 A B)
      )
      (new13 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new13 A B)
      )
      (new13 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new13 A B)
        (new13 A B)
      )
      (new13 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new13 A B)
        (new13 A B)
      )
      (new13 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B false)
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new5 A B)
      )
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (new5 A B)
      )
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (new5 A B)
        (new5 A B)
      )
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (<= (- A C) (- 1))
        (new5 A B)
        (new5 A B)
      )
      (new5 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (= B true)
      (new4 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (<= C (- A 1))
        (new5 A B)
      )
      (new4 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (<= C (- A 1))
        (new4 A A B)
      )
      (new4 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= (- A C) 1)
        (<= C (- A 1))
        (new5 A B)
        (new4 A A B)
      )
      (new4 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) )
    (=>
      (and
        (= B true)
        (>= A A)
      )
      (new4 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (>= C A)
        (new4 A A B)
      )
      (new4 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B true)
        (>= C A)
        (new5 A B)
      )
      (new4 A A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Bool) (C Int) )
    (=>
      (and
        (= B false)
        (>= C A)
        (<= (- A C) (- 1))
        (new4 A A B)
        (new5 A B)
      )
      (new4 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))
        (new13 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))
        (new14 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)
        (new15 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)
        (new13 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))
        (new17 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))
        (new17 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))
        (new19 C A D)
        (new17 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)
        (new17 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)
        (new13 A D)
        (new17 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)
        (new13 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)
        (new13 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))
        (new17 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))
        (new13 A D)
        (new17 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)
        (new13 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)
        (new13 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)
        (new17 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)
        (new19 C A D)
        (new17 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)
        (new17 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)
        (new17 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)
        (new17 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)
        (new17 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)
        (new17 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)
        (new17 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)
        (new17 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)
        (new17 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)
        (new17 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)
        (new57 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)
        (new58 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))
        (new59 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))
        (new57 C A D)
        (new59 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)
        (new59 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)
        (new58 A D)
        (new59 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)
        (new58 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)
        (new58 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))
        (new58 A D)
        (new59 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)
        (new58 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)
        (new59 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)
        (new57 C A D)
        (new59 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)
        (new59 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)
        (new59 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)
        (new59 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)
        (new59 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)
        (new59 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)
        (new59 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)
        (new59 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))
        (new91 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))
        (new92 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))
        (new93 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))
        (new93 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))
        (new92 C A D)
        (new93 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))
        (new91 A D)
        (new93 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)
        (new91 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))
        (new93 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))
        (new91 A D)
        (new93 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)
        (new91 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)
        (new91 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))
        (new92 C A D)
        (new93 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))
        (new93 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)
        (new93 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)
        (new93 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)
        (new93 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)
        (new93 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)
        (new93 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)
        (new93 A B)
      )
      (new1 A B C A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= B false)
        (>= (- C D) 1)
        (new1 D B C D A)
      )
      ff
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= A false)
        (= B false)
        (<= (- C D) (- 1))
        (new2 D B C D A)
      )
      ff
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Int) )
    (=>
      (and
        (= A true)
        (= B true)
        (new3 C B D C A)
      )
      ff
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A true)
        (new4 B B A)
      )
      ff
    )
  )
)

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