formulas(theory).

  % f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # label(A_SS).

  f(f(x,x),f(x,y)) = x                            # label(B_SS).
  f(x,f(x,x)) = 1                                 # label(ONE_CONSTANT).
  f(1,1) = 0.
  f(x,y) = f(y,x)                                 # label(commutativity).

  % f(x,f(x,f(x,y))) = f(x,y)                       # label(OM_SS).
  % f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y))))   # label(MOD_SS).
  % f(f(x,f(y,y)),f(x,y)) = x                       # label(CUT_SS).


  f(x,f(f(y,z),f(x,y))) = f(x,y)   # label(MOL_property).

  % denial of associativity

  f(A,f(f(B,C),f(B,C))) != f(B,f(f(A,C),f(A,C))) # label(A_SS).

end_of_list.