(declare-rel BB0 ())
(declare-rel BB1 ( Int Int))
(declare-rel BB2 ())
(declare-rel BB3 ( Int Int ))
(declare-rel BB4 ( Int Int ))
(declare-rel BB6 ( Int Int ))
(declare-rel BB9 ( Int Int ))
(declare-rel BB10 ( Int Int ))
(declare-rel BB7 ( Int Int ))
(declare-var contract@x_0_0 Int)
(declare-var contract@x_0_1 Int)
(declare-var contract@y_0_0 Int)
(declare-var contract@y_0_1 Int)
(rule BB0)
(rule (=> ( and BB0 (= contract@x_0_0 0) (= contract@y_0_0 0)) (BB1 contract@x_0_0 contract@y_0_0)))
(rule (=> ( and (BB1 contract@x_0_0 contract@y_0_0)) (BB3 contract@x_0_0 contract@y_0_0)))
(rule (=> ( and (BB1 contract@x_0_0 contract@y_0_0)) (BB6 contract@x_0_0 contract@y_0_0)))
(rule (=> ( and (BB3 contract@x_0_0 contract@y_0_0) (< contract@x_0_0 1000) (< contract@y_0_0 1000) (= contract@x_0_1 (+ contract@x_0_0 1)) (= contract@y_0_1 (+ contract@y_0_0 2))) (BB4 contract@x_0_1 contract@y_0_1)))
(rule (=> ( and (BB4 contract@x_0_0 contract@y_0_0)) (BB1 contract@x_0_0 contract@y_0_0)))
(rule (=> ( and (BB6 contract@x_0_0 contract@y_0_0)) (BB9 contract@x_0_0 contract@y_0_0)))
(rule (=> ( and (BB9 contract@x_0_0 contract@y_0_0) (>= contract@y_0_0 contract@x_0_0)) (BB10 contract@x_0_0 contract@y_0_0)))
(rule (=> ( and (BB9 contract@x_0_0 contract@y_0_0) (not (>= contract@y_0_0 contract@x_0_0))) BB2))
(rule (=> ( and (BB10 contract@x_0_0 contract@y_0_0)) (BB7 contract@x_0_0 contract@y_0_0)))
(rule (=> ( and (BB7 contract@x_0_0 contract@y_0_0)) (BB1 contract@x_0_0 contract@y_0_0)))
(query BB2 :print-certificate true)