Non-unifiability in linear temporal logic of knowledge with multi-agent relations

The paper is devoted to the study of the unification problem in the linear temporal logic of knowledge with multi-agent relations (denoted in the sequel as $LFPK$). This logic is based on frames (models) with time points represented by integer numbers from $Z$ and the information clusters $C^i$ for $i \in Z$ with multi-agent accessibility relations $R_i$.
The first main result is a theorem describing a criterion for formulas to be not unifiable in $LFPK$. The second one is a construction of a basis for all inference rules passive in $LFPK$.