% original version at http://www.ii.uib.no/~bezem/GL/ser.in
% p(n) iff not p(k) for all k>n  leads to a contradiction
% it suffices that the domain is non-empty and < is transitive and serial

:- op(1200,xfx,':=').
:- op(1199,xfx,'=>').

:- dynamic(p/1).
:- dynamic(notp/1).
:- dynamic(less/2).
:- dynamic(dom/1).

flag(keywords).
flag(quiet).
flag(quick).

% domain element o

dom(o).

% the systematic translation based on the tableaux method yields:

[left_to_right,X,Y] := p(X),less(X,Y),p(Y) => false.
[right_to_left,X] := dom(X) => p(X);dom(Y),less(X,Y),p(Y). 

% basic facts on less

[transitive_less,X,Y,Z] := less(X,Y),less(Y,Z) => less(X,Z).
[serial_less,X] := dom(X) => dom(Y),less(X,Y). % last!

% NB inconsistency is proved without a clause for goal!