vars x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 rules x2 >= 1 -> x0' = x0+1, x2' = x2-1; x0 >= 1 -> x0' = x0-1, x1' = x1+1; x1 >= 1 -> x0' = x0+1, x1' = x1-1; x0 >= 1 -> x0' = x0-1, x3' = x3+1; x3 >= 1, x6 >= 1, x10 >= 1 -> x2' = x2+1, x3' = x3-1, x4' = x4+1, x6' = x6-1, x8' = x8+1, x10' = x10-1; x4 >= 1 -> x4' = x4-1, x5' = x5+1; x5 >= 1 -> x4' = x4+1, x5' = x5-1; x4 >= 1 -> x4' = x4-1, x7' = x7+1; x7 >= 1, x11 >= 1, x14 >= 1 -> x6' = x6+1, x7' = x7-1, x10' = x10+1, x11' = x11-1, x12' = x12+1, x14' = x14-1; x8 >= 1 -> x8' = x8-1, x9' = x9+1; x9 >= 1 -> x8' = x8+1, x9' = x9-1; x8 >= 1 -> x8' = x8-1, x11' = x11+1; x12 >= 1 -> x12' = x12-1, x13' = x13+1; x13 >= 1 -> x12' = x12+1, x13' = x13-1; x12 >= 1 -> x12' = x12-1, x15' = x15+1; x15 >= 1 -> x14' = x14+1, x15' = x15-1; init x0 = 0, x1 = 0, x2 >= 1, x3 = 0, x4 = 0, x5 = 0, x6 >= 1, x7 = 0, x8 = 0, x9 = 0, x10 >= 1, x11 = 0, x12 = 0, x13 = 0, x14 >= 1, x15 = 0 target x4 >= 2, x6 >= 4, x10 >= 4, x13 >= 6, x14 >= 4 invariants