Ex (z-x==1 && Ey x-4y==0)