; File generated by sugar.Output (int x ((2 9))) (int y ((2 3) (5 5) (8 9))) (int z ((1 3) (5 5) (7 9))) (int w ((-927 1000))) ; \$I1 : (abs w) (int \$I1 ((0 1000))) ; \$I2 : \$I1+y+0 (int \$I2 ((2 1009))) ; \$I3 : w+z+0 (int \$I3 ((-918 1009))) (bool p) (bool q) (bool r) (bool \$B1) (bool \$B2) (bool \$B3) (bool \$B4) (bool \$B5) (bool \$B6) (bool \$B7) (bool \$B8) (bool \$B9) (bool \$B10) (bool \$B11) (bool \$B12) (bool \$B13) (bool \$B14) (bool \$B15) (relation r 2 (conflicts (1 2) (3 4))) ; (imp p (imp q r)) (or (not p) (not q) r) (or (not \$B2) (not (r x y))) (or (not \$B3) (r y x)) (or \$B2 \$B3) (or (not \$B4) (r x y)) (or (not \$B5) (not (r y x))) (or \$B4 \$B5) ; (gt (add x y) 10) (wsum ((1 x) (1 y)) ge 11) ; (imp (eq x 9) (and p q (eq z 1))) (or (wsum ((1 x)) le 8) \$B1) (or p (not \$B1)) (or q (not \$B1)) (or (wsum ((1 z)) le 1) (not \$B1)) (or (not \$B6) (wsum ((1 x) (1 y)) ge 10)) (or (not \$B7) (wsum ((1 y) (1 z)) ge 10)) (or \$B6 \$B7) ; \$I1 == (abs w) (wsum ((1 \$I1) (-1 w)) ge 0) (wsum ((1 \$I1) (1 w)) ge 0) (or (not \$B8) (wsum ((1 \$I1) (-1 w)) le 0)) (or (not \$B9) (wsum ((1 \$I1) (1 w)) le 0)) (or \$B8 \$B9) ; \$I2 == (add 0 (mul 1 \$I1) (mul 1 y)) (wsum ((-1 \$I1) (1 \$I2) (-1 y)) le 0) (wsum ((-1 \$I1) (1 \$I2) (-1 y)) ge 0) ; \$I3 == (add 0 (mul 1 w) (mul 1 z)) (wsum ((1 \$I3) (-1 w) (-1 z)) le 0) (wsum ((1 \$I3) (-1 w) (-1 z)) ge 0) ; (ge (add w (abs w) x y z) 100) (wsum ((1 \$I2) (1 \$I3) (1 x)) ge 100) (or (not \$B10) (wsum ((1 x) (-1 y)) le -1)) (or (not \$B11) (wsum ((1 x) (-1 y)) ge 1)) (or \$B10 \$B11) (or (not \$B12) (wsum ((1 x) (-1 z)) le -1)) (or (not \$B13) (wsum ((1 x) (-1 z)) ge 1)) (or \$B12 \$B13) (or (not \$B14) (wsum ((1 y) (-1 z)) le -1)) (or (not \$B15) (wsum ((1 y) (-1 z)) ge 1)) (or \$B14 \$B15) (or (wsum ((1 x)) ge 3) (wsum ((1 y)) ge 3) (wsum ((1 z)) ge 3)) (or (wsum ((1 x)) le 7) (wsum ((1 y)) le 7) (wsum ((1 z)) le 7))