The decision problem for finite algebras from arithmetical varieties with equationally definable principal congruences (Q1117961)

Let V be a locally finite, congruence permutable variety with equationally definable principal congruences and 1-regular (i.e. there is a constant 1 such that \(1/R=1/s\) implies \(R=S\) for any congruences R, S of any algebra in V). If there is a subdirectly irreducible algebra whose congruences do not form a chain, then the class of all finitely generated free algebras in V has a hereditarily undecidable first order theory. The proof is by interpreting in this class the class of all finite biparpite graphs with at least 3 elements.