x= readInt() y = readInt() z = readInt() assert x >= 0 assert x != 0 assert (x == 0) # UNABLE TO VERIFY assert (z == 2) # UNABLE TO VERIFY """{ 1.OK x >= 0 premise 2.OK x != 0 premise 3.OK x > 0 algebra 2 1 4.?? x == 0 premise 5.?? z == 2 algebra }"""