adjust backward check formula
The formula is supposed to check for double occurrences of the end node before reaching a root. But the first argument of EU has to be the negation of the roots. With just the roots there, the formula always failed (failure of the formula is a sign that everything is ok).