Implication is not strong enough. That permits e.g. f to be true and e to be false. Also I don't know the specifics of the language that tool uses, but typica

Implication is not strong enough. That permits e.g. f to be true and e to be false. Also I don't know the specifics of the language that tool uses, but typically variadic XOR simply constrains that an odd number of its operands are true. (It so happens that there are no solutions to this problem with 3 or 5 true answers.)