assign(new_constants, 1).

clauses(sos).

x v (y v z) = y v (x v z).              % AJ
x v (x ^ y) = x.                        % B1
x ^ y = c(c(x) v c(y)).                 % DM
c(c(x)) = x.                            % CC
x v c(x) = y v c(y).                    % ONE
x v (y ^ (x v z)) = x v (z ^ (x v y)).  % MOD

f(x,y) = c(x) v c(y).      % DEF_SS

end_of_list.

clauses(goals).

f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z)))  # answer(A_SS).
f(f(x,x),f(x,y)) = x                           # answer(B_SS).
f(x,f(x,x)) = f(y,f(y,y))                      # answer(ONE_SS).
f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y))))  # answer(MOD_SS).

x v y = f(f(x,x),f(y,y))  # answer(DEF_J).
x ^ y = f(f(x,y),f(x,y))  # answer(DEF_M).
c(x) = f(x,x)             # answer(DEF_C).

end_of_list.