询问：该Prolog程序是否存在简洁的非停机性证明？

以下是待分析的Prolog程序：

:-  p(f(X),f(f(Y)),f(f(b))).

p(f(a),f(X),f(f(X))).
p(f(a),f(a),f(f(X))).
p(X,f(f(Y)),X) :- p(Y,f(f(Y)),f(f(X))).
p(f(X),Y,Z) :- p(X,f(Y),f(f(Z))).

我已经构思出一种基于归纳法的证明思路，包含若干子情况，例如：

p(f(X),f(f(X)),f(f(b)))会无限展开（即非停机）可由以下结论推导而来：

p( X, fⁿ(X), fⁿ⁺¹(b) )会无限展开（即非停机）

若0 ≤ k < m，则p(fᵏ(b),fˡ(b),fᵐ(b))推导失败。

若(l - k) mod 3 = 0，则p(fᵏ(b),fˡ(b),fᵏ(b))推导失败。

其中fⁿ(X)表示n次迭代：f(f(...f(X)...))。

我打算完成该归纳法证明，但想知道是否存在更简洁的非停机性证明。此处的「停机」采用Prolog标准过程语义：子句按顺序执行，子目标按从左到右顺序执行（本例中该规则不影响结果）。

内容的提问来源于stack exchange，提问作者Lewis Baxter