Chess Unwinnability Analyzer is an implementation of a decision procedure for checking whether there exists a sequence of legal moves that allows a certain player to checkmate their opponent in a given chess position.
It seems there is a typo in the PDF for pawn forwards moves.
For example for a White pawn forward move to a5, the pawn must move to a4 (predecessor) and a5 must be clearable. I understand the document says a4 must be clearable instead of a5.
That is I suggest the PDF on page 11 should state $\bigvee_\limits{u \in predP(s)}M{P \to u} \land Fs^{P.color}$ instead of $\bigvee\limits{u \in predP(s)}M{P \to u} \land F_u^{P.color}$.
It seems there is a typo in the PDF for pawn forwards moves.
For example for a White pawn forward move to a5, the pawn must move to a4 (predecessor) and a5 must be clearable. I understand the document says a4 must be clearable instead of a5.
That is I suggest the PDF on page 11 should state $\bigvee_\limits{u \in predP(s)}M{P \to u} \land Fs^{P.color}$ instead of $\bigvee\limits{u \in predP(s)}M{P \to u} \land F_u^{P.color}$.