#include <stdio.h>

$input int x, y, z, w;
$input int N, M, L, K;
$input int offset;

$assume(0< N && N <= 2);
$assume(0< M && M <= 2);
$assume(0< L && L <= 2);
$assume(0< K && K <= 2);
$assume(0 <= x && x < N);
$assume(0 <= y && y < M);
$assume(0 <= z && z < L);
$assume(0 <= w && w < K);
$assume(0 <= offset );
$assume((offset + x*M*L*K + y*L*K + z*K + w) < M*N*L*K);

void main(){

  int realIndex, finalIndex, X, Y, Z, W;

  realIndex = x * M *  L * K + y * L * K + z * K + w;
  finalIndex = realIndex + offset;
  X = finalIndex / (M * L * K);
  finalIndex = finalIndex - X * M * L * K;
  Y = finalIndex / (L * K);
  finalIndex = finalIndex - Y * L * K;
  Z = finalIndex / K;
  W = finalIndex - Z * K;

  printf("X=%d, Y=%d, Z=%d, W=%d\n", X,Y,Z,W);
  $assert(X < N);
  $assert(Y < M);
  $assert(Z < L);
  $assert(W < K);
}