assign(new_constants, 1).

clauses(sos).

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

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

end_of_list.

clauses(goals).

  x v (y v z) = y v (x v z)              # answer(AJ).
  x v (x ^ y) = x                        # answer(B1).
  x ^ y = c(c(x) v c(y))                 # answer(DM).
  c(c(x)) = x                            # answer(CC).
  x v c(x) = y v c(y)                    # answer(ONE).

  x v (y ^ (x v z)) = x v (z ^ (x v y))  # answer(MOD).

  f(x,y) = c(x) v c(y)                   # answer(DEF_SS).

end_of_list.