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.