#include <stdio.h>
#include <civlc.cvh>

$input int X;
$assume(1 <= X && X <= 3);
$assume(X % 2 == 0);

int main(void) {
  $elaborate(X);
  printf("%d\n", X);
  $assert(X==2);
  return 0;
}