Clojurians Log v2

That's only for fd logic variables though, I would think the question was equivalent to "at most one pair out of the 6 lvars can unify"

Can't think of an easy way to express that (besides macroexpanding all the permutations by brute force)

Oh yes, good point. I interpreted the question rather as “I know which 5 of the 6 lvars should be distinct”.