Diassociative loops are not finitely based

A loop is a quasigroup with unit. As a sloppy but intuitivesaying has it "a loop is a group minus associativity". In this context, two classes of loops are of particular interest: power-associative loops (such that each one-generated subloop is a group) and diassociative, (such that each two-generated subloop is a group). It is easy to see that both classes are varieties. T. Evans and B.H. Neumann in their paper "On varieties of groupoids and loops" (J. London Math. Soc., 28, 1953, 342--350) proved that the variety of power-associative loops is not finitely based. In the same paper they asked whether the variety of diassociative loops was finitely based. Somewhat surprisingly, this question remained open for the following 55 years, despite (or perhaps because of) a widely held belief that the answer should be negative. I will present a proof of the following: Theorem. Diassociative loops are not finitely based relative to power-associative loops.