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

$input int n1;
$assume (n1>=0);
$input int X1[n1];
$input int X2[n1];

void main(){
  $assert(
	  ($forall {int i | i > 0 && i < n1} X1[i] == X2[i])
	  && ($forall {int i | i > 0 && i < n1} X1[i] == X2[i])
	  );
}