$input int N;
$assume(N > 0);

int main(int argc, char** argv) {
  
  $assert($forall (int i:0..3) (i >= N ? N + i : N - i));
}