; Automatically generated by map2smt

(set-logic HORN)




(declare-fun new9 (Int) Bool)
(declare-fun new6 (Bool Int) Bool)
(declare-fun new51 (Int Int) Bool)
(declare-fun new37 (Int Int) Bool)
(declare-fun new33 (Int) Bool)
(declare-fun new3 (Bool Int) Bool)
(declare-fun new27 (Int Int) Bool)
(declare-fun new2 (Int Int Int Bool) Bool)
(declare-fun new13 (Int Int) Bool)
(declare-fun new1 (Int Int Int Bool) Bool)
(declare-fun diff_new8 (Int Int Int Int) Bool)
(declare-fun diff_new5 (Int Int Int Int) Bool)
(declare-fun diff_new44 (Int Int Int) Bool)
(declare-fun diff_new39 (Int Int Int) Bool)
(declare-fun diff_new20 (Int Int Int) Bool)
(declare-fun diff_new15 (Int Int Int) Bool)
(declare-fun not_fun_diff_new44 () Bool)
(declare-fun constr (Bool) Bool)
(declare-fun not_fun_diff_new39 () Bool)
(declare-fun not_fun_diff_new20 () Bool)
(declare-fun not_fun_diff_new15 () Bool)
(declare-fun not_fun_diff_new8 () Bool)
(declare-fun not_fun_diff_new5 () Bool)
(declare-fun ff () Bool)

(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (diff_new44 A B C)
        (diff_new44 D E F)
        (and (= A D) (or (not (= B E)) (not (= C F))))
      )
      not_fun_diff_new44
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (diff_new39 A B C)
        (diff_new39 D E F)
        (and (= A D) (or (not (= B E)) (not (= C F))))
      )
      not_fun_diff_new39
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (diff_new20 A B C)
        (diff_new20 D E F)
        (and (= A D) (or (not (= B E)) (not (= C F))))
      )
      not_fun_diff_new20
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (diff_new15 A B C)
        (diff_new15 D E F)
        (and (= A D) (or (not (= B E)) (not (= C F))))
      )
      not_fun_diff_new15
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (diff_new8 A B C D)
        (diff_new8 E F G H)
        (and (and (= A E) (and (= B F) (= C G))) (not (= D H)))
      )
      not_fun_diff_new8
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (diff_new5 A B C D)
        (diff_new5 E F G H)
        (and (and (= A E) (and (= B F) (= C G))) (not (= D H)))
      )
      not_fun_diff_new5
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= B 0)
        (= A 0)
      )
      (new51 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 F))
        (= A (+ 1 E))
        (new51 C F)
        (new33 D)
      )
      (new51 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (and
        (= C 0)
        (= B 0)
        (= A 0)
      )
      (diff_new44 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (>= D 0)
        (>= E 0)
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= G (+ E D))
        (= C (+ 1 H))
        (= B (+ 1 F))
        (= A (+ 1 G))
        (new51 D H)
        (new33 E)
      )
      (diff_new44 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= B 0)
        (= A 0)
      )
      (new37 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (new33 D)
        (new33 C)
      )
      (new37 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (and
        (= C 0)
        (= B 0)
        (= A 0)
      )
      (diff_new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (>= D 0)
        (>= E 0)
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= G (+ E D))
        (= C (+ 1 F))
        (= A (+ 1 G))
        (new33 E)
        (new33 D)
      )
      (diff_new39 A B C)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new33 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) )
    (=>
      (and
        (>= B 0)
        (>= C 0)
        (= D (+ B C))
        (= A (+ 1 D))
        (new33 B)
        (new33 C)
      )
      (new33 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= B 0)
        (= A 0)
      )
      (new27 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) )
    (=>
      (and
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 F))
        (= A (+ 1 E))
        (new27 C F)
        (new9 D)
      )
      (new27 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (and
        (= C 0)
        (= B 0)
        (= A 0)
      )
      (diff_new20 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (>= D 0)
        (>= E 0)
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= G (+ E D))
        (= C (+ 1 H))
        (= B (+ 1 F))
        (= A (+ 1 G))
        (new27 D H)
        (new9 E)
      )
      (diff_new20 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) )
    (=>
      (and
        (= B 0)
        (= A 0)
      )
      (new13 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (new9 D)
        (new9 C)
      )
      (new13 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) )
    (=>
      (and
        (= C 0)
        (= B 0)
        (= A 0)
      )
      (diff_new15 A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (>= D 0)
        (>= E 0)
        (>= D 0)
        (>= E 0)
        (= F (+ E D))
        (= G (+ E D))
        (= C (+ 1 F))
        (= A (+ 1 G))
        (new9 E)
        (new9 D)
      )
      (diff_new15 A B C)
    )
  )
)
(assert
  (forall ( (A Int) )
    (=>
      (= A 0)
      (new9 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) )
    (=>
      (and
        (>= B 0)
        (>= C 0)
        (= D (+ B C))
        (= A (+ 1 D))
        (new9 B)
        (new9 C)
      )
      (new9 A)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (>= E 0)
        (>= F 0)
        (= E 0)
        (= F 0)
        (= G (+ F E))
        (= D (+ 1 G))
        (= B 1)
        (= A 0)
      )
      (diff_new8 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (>= G 0)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= G 0)
        (>= H 0)
        (<= K (- C 1))
        (<= L M)
        (= N (+ H G))
        (= M 0)
        (= O (+ 1 L))
        (= I (+ 1 N))
        (= J 0)
        (= P (+ J I))
        (= Q (+ H G))
        (= D (+ 1 P))
        (= B 1)
        (= A (+ 1 Q))
        (new9 H)
        (new9 G)
      )
      (diff_new8 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (>= G 0)
        (>= H 0)
        (>= I (+ J 1))
        (>= K 0)
        (>= L 0)
        (>= G 0)
        (>= H 0)
        (<= M (- C 1))
        (= N (+ H G))
        (= J 0)
        (= O 0)
        (= P (+ 1 O))
        (= K 0)
        (= L (+ 1 N))
        (= Q (+ L K))
        (= R (+ H G))
        (= D (+ 1 Q))
        (= B 1)
        (= A (+ 1 R))
        (new9 H)
        (new9 G)
      )
      (diff_new8 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (>= G C)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (<= K L)
        (= M (+ 1 K))
        (= N (+ J H))
        (= O (+ J I))
        (= D (+ 1 N))
        (= B 1)
        (= A (+ 1 O))
        (diff_new15 P K H)
        (new13 L J)
        (diff_new8 I B C P)
      )
      (diff_new8 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (>= G (+ H 1))
        (>= I C)
        (>= J 0)
        (>= K 0)
        (>= L 0)
        (= M (+ 1 H))
        (= N (+ J L))
        (= O (+ L K))
        (= D (+ 1 N))
        (= B 1)
        (= A (+ 1 O))
        (diff_new15 P G J)
        (diff_new8 K B C P)
        (new13 H L)
      )
      (diff_new8 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A true)
        (= B 0)
      )
      (new6 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= A true)
        (>= C 0)
        (>= D 0)
        (<= E F)
        (= G (+ 1 E))
        (= H (+ D C))
        (= B (+ 1 H))
        (diff_new20 I C E)
        (diff_new20 J D F)
        (new6 A J)
        (new6 A I)
      )
      (new6 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (new6 A D)
        (new9 C)
      )
      (new6 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (new9 D)
        (new6 A C)
      )
      (new6 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= C (+ D 1))
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= B (+ 1 G))
        (new27 F D)
        (new27 E C)
      )
      (new6 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (>= C 0)
        (>= D 0)
        (<= (+ E 1) (+ 1 F))
        (= G (+ D C))
        (= B (+ 1 G))
        (new9 D)
        (new27 C F)
      )
      (new6 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (>= C (+ (+ 1 D) 1))
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= B (+ 1 G))
        (new9 F)
        (new27 E D)
      )
      (new6 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (>= E 0)
        (>= F 0)
        (= E 0)
        (= F 0)
        (= G (+ F E))
        (= D (+ 1 G))
        (= B 1)
        (= A 0)
      )
      (diff_new5 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) )
    (=>
      (and
        (= E true)
        (= F true)
        (>= G 0)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (>= G 0)
        (>= H 0)
        (<= K (- C 1))
        (<= L M)
        (= N (+ H G))
        (= M 0)
        (= O (+ 1 L))
        (= I (+ 1 N))
        (= J 0)
        (= P (+ J I))
        (= Q (+ H G))
        (= D (+ 1 P))
        (= B 1)
        (= A (+ 1 Q))
        (new33 H)
        (new33 G)
      )
      (diff_new5 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) )
    (=>
      (and
        (= E false)
        (= F true)
        (>= G 0)
        (>= H 0)
        (>= I (+ J 1))
        (>= K 0)
        (>= L 0)
        (>= G 0)
        (>= H 0)
        (<= M (- C 1))
        (= N (+ H G))
        (= J 0)
        (= O 0)
        (= P (+ 1 O))
        (= K 0)
        (= L (+ 1 N))
        (= Q (+ L K))
        (= R (+ H G))
        (= D (+ 1 Q))
        (= B 1)
        (= A (+ 1 R))
        (new33 H)
        (new33 G)
      )
      (diff_new5 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) )
    (=>
      (and
        (= E true)
        (= F false)
        (>= G C)
        (>= H 0)
        (>= I 0)
        (>= J 0)
        (<= K L)
        (= M (+ 1 K))
        (= N (+ J H))
        (= O (+ J I))
        (= D (+ 1 N))
        (= B 1)
        (= A (+ 1 O))
        (diff_new39 P K H)
        (new37 L J)
        (diff_new5 I B C P)
      )
      (diff_new5 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Int) (E Bool) (F Bool) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) )
    (=>
      (and
        (= E false)
        (= F false)
        (>= G (+ H 1))
        (>= I C)
        (>= J 0)
        (>= K 0)
        (>= L 0)
        (= M (+ 1 H))
        (= N (+ J L))
        (= O (+ L K))
        (= D (+ 1 N))
        (= B 1)
        (= A (+ 1 O))
        (diff_new39 P G J)
        (diff_new5 K B C P)
        (new37 H L)
      )
      (diff_new5 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) )
    (=>
      (and
        (= A true)
        (= B 0)
      )
      (new3 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) )
    (=>
      (and
        (= A true)
        (>= C 0)
        (>= D 0)
        (<= E F)
        (= G (+ 1 E))
        (= H (+ D C))
        (= B (+ 1 H))
        (diff_new44 I C E)
        (diff_new44 J D F)
        (new3 A J)
        (new3 A I)
      )
      (new3 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (new3 A D)
        (new33 C)
      )
      (new3 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A false)
        (>= C 0)
        (>= D 0)
        (= E (+ D C))
        (= B (+ 1 E))
        (new33 D)
        (new3 A C)
      )
      (new3 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (= A false)
        (>= C (+ D 1))
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= B (+ 1 G))
        (new51 F D)
        (new51 E C)
      )
      (new3 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (>= C 0)
        (>= D 0)
        (<= (+ E 1) (+ 1 F))
        (= G (+ D C))
        (= B (+ 1 G))
        (new33 D)
        (new51 C F)
      )
      (new3 A B)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) )
    (=>
      (and
        (= A false)
        (>= C (+ (+ 1 D) 1))
        (>= E 0)
        (>= F 0)
        (= G (+ F E))
        (= B (+ 1 G))
        (new33 F)
        (new51 E D)
      )
      (new3 A B)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= B 0)
        (new3 C A)
      )
      (new2 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E 1)
        (= C (+ 1 F))
        (diff_new5 G E H A)
        (new2 G B F D)
      )
      (new2 A B C D)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Bool) )
    (=>
      (and
        (= B 0)
        (new6 C A)
      )
      (new1 A A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Int) (F Int) (G Int) (H Int) )
    (=>
      (and
        (= E 1)
        (= C (+ 1 F))
        (diff_new8 G E H A)
        (new1 G B F D)
      )
      (new1 A B C D)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A true)
        (<= (+ B 1) C)
        (= (+ D E) B)
        (new1 C D E A)
      )
      ff
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Int) )
    (=>
      (and
        (= A true)
        (>= B (+ C 1))
        (= (+ D E) B)
        (new2 C D E A)
      )
      ff
    )
  )
)

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