set(build_proof_object).
set(auto).
set(prolog_style_variables).

list(usable).
% NAME: reflexivity
X = X.
% NAME: commutativity
X+Y = Y+X.
% NAME: associativity
(X+Y)+Z = X+Y+Z.
% NAME: huntington
n(X+n(Y))+n(n(X)+n(Y)) = Y.
% NAME: idempotency
X+X = X.
% NAME: involution
n(n(X)) = X.

% NAME: goal
n(n(a)+n(b+c)) != n(n(a)+n(b))+n(n(a)+n(c)).


end_of_list.