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