LOCAL Int.

ThFl(x, y ) <- y = x * 1000.

P(x,x).

CkLt(x,y,z) <- z = x + y.

%% CkLt2(x,y,z) <- z = [x < y] x + y.