predicates([p1,p2,p3,p4,p5,p6]).

% This example is parametric in n, with n=5 below.
% The set of clauses is inconsistent
% as for X=f^m(d0), with m = n!, none of the pi(X) can be true.

p1(X), X = d0 -> [].
p1(X) -> f(d0) = d0.

p2(X), X = d1 -> [].
p2(X) -> f(d0) = d1.
p2(X) -> f(d1) = d0.

p3(X) ,X = d2 -> [].
p3(X) -> f(d0) = d1.
p3(X) -> f(d1) = d2.
p3(X) -> f(d2) = d0.

p4(X), X = d3 -> [].
p4(X) -> f(d0) = d1.
p4(X) -> f(d1) = d2.
p4(X) -> f(d2) = d3.
p4(X) -> f(d3) = d0.

p5(X), X = d4 -> [].
p5(X) -> f(d0) = d1.
p5(X) -> f(d1) = d2.
p5(X) -> f(d2) = d3.
p5(X) -> f(d3) = d4.
p5(X) -> f(d4) = d0.

/*  the case n=6 takes about 7 times longer

p6(X), X = d5 -> [].
p6(X) -> f(d0) = d1.
p6(X) -> f(d1) = d2.
p6(X) -> f(d2) = d3.
p6(X) -> f(d3) = d4.
p6(X) -> f(d4) = d5.
p6(X) -> f(d5) = d0.

p1(X) , p2(X), p3(X), p4(X), p4(X), p5(X), p6(X).

precedence([f,d0,d1,d2,d3,d4,d5,p1,p2,p3,p4,p5,p6]). % other orderings work less well

*/

%/*
p1(X) , p2(X), p3(X), p4(X), p4(X), p5(X).


precedence([f,d0,d1,d2,d3,d4,p1,p2,p3,p4,p5]). % other orderings work less well
%*/


:-sama([2]).  % positive strategy
%:-saci([2]).
:-sarp(+[3,15]).  % full rewriting + backwards subsumption (cruicial)

% for this almost ground example constraint inheritance
% yields longer proof search for n=5 but inproves search behaviour
% for n=6