Is this the smallest Prolog program whose halting is unknown?

Question

It is unknown whether the following 6-clause "pure" Prolog program halts.

:- f(s(s(s(s(s(s(s(s(N)))))))),F), m(S,S,s(F)).
    
f(o,s(o)).   
f(s(N),G) :- f(N,F), m(s(N),F,G).

m(o,_,o).    
m(s(X),Y,Z) :- a(Y,P,Z), m(X,Y,P).

a(o,Y,Y).
a(s(X),Y,s(Z)) :- a(X,Y,Z).

It is based on a conjecture, related to Brocard's Problem, that n!+1=m^2 only has solutions for n < 8.

Is there a smaller Prolog program whose halting is unknown?

Only "pure" Prolog is allowed, so library and standard predicates, numbers, not and cut are forbidden.

I examined many unsolved problems but could not find a corresponding smaller program. Brocard's Problem is also one of the smallest in: https://codegolf.stackexchange.com/questions/97004/does-the-code-terminate

EDIT: Determining if a program halts can be challenging. I moved an example to a new Question.

Answer 1

Is there a smaller Prolog program whose halting is unknown?

It all depends on your metrics of program size. If you just take the number of clauses (or literals) but do not take the size of terms into account, then the answer is yes, there are such programs. A Turing machine can be encoded with a single (recursive) binary rule and one fact. And since you are only interested in halting, the fact is not even needed. See this question for the (idea of) the encoding.

Answer 2

I found a smaller Prolog program based on an unsolved problem found at https://mathoverflow.net/questions/453225/are-these-equations-solvable-in-positive-integers. The equation is y(x^3 - z^2) = z. I added some s's to avoid trivial solutions.

:- mul(X,X,X2), mul(X,X2,X3),      % generate x^3
   add(s(V),Q,X3), mul(Z,Z,s(V)),  % z^2 + q = x^3 (ensure z > 0)
   mul(Y,Q,Z).                     % does q | z?

mul( o,    _, o ).
mul( s(X), Y, Z ) :-  add(Y,XY,Z), mul(Y,X,XY).

add( o,    Y, Y    ).
add( s(X), Y, s(Z) ) :- add(X,Y,Z).