What're the constraints of mutual recursion in PI?

[yangdinglou]

Hi, I'm learning something with mutual recursion. The force ordering at https://github.com/logic-and-learning-lab/Popper/blob/main/popper/lp/alan.pl#L714 is already commented out, but some valid mutual recursive programs are not found.

For example, a simple example of even/odd is here

%% intended 
% even(X):- zero(X).
% even(X):- prev(X, Y), inv1(Y).
% inv1(X):- prev(X, Y), even(Y).
%% bias
max_vars(2).
max_body(2).
max_clauses(3).
enable_recursion.
enable_pi.

head_pred(even,1).
body_pred(zero,1).
body_pred(prev,2).
body_pred(succ,2).

:-
    not clause(1).
:-
    not clause(2).

:-
    head_literal(0,P,_,_),
    not head_literal(1,P,_,_).

:-
    head_literal(1,P,_,_),
    head_literal(2,P,_,_).

:-
    not head_literal(2, _, 1, _).

%% bk
succ(A,B):-
    B is A+1.

prev(A,B):-
    B is A-1.   

zero(0).

%% ex

pos(even(0)).
pos(even(2)).
pos(even(4)).

neg(even(1)).

Then no valid model is found. May I know what's the reason?