I was going to say the same thing. 'cut', of course, destroys the purely algebraic nature of the thing, and forces you to understand the whole search-tree and

I was going to say the same thing. 'cut', of course, destroys the purely algebraic nature of the thing, and forces you to understand the whole search-tree and backtracking part of the language, but the basics work.