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
}"""