% In this version, equality is axiomatized with equality axioms
% instead of using the built-in equality relation "=".

formulas(sos).

y == m | p(y,m) | v1 == m | v1 == y | -p(y,v1) | -p(v1,y).
y == b | -p(y,b) | v == b | v == y | -p(y,v) | -p(v,y).
y == k | y == m | y == b | -p(y,k).
y == m | -p(y,m) | -(f(y) == m).
y == m | -p(y,m) | -(f(y) == y).
y == m | -p(y,m) | p(y,f(y)).
y == m | -p(y,m) | p(f(y),y).
y == b | p(y,b) | -(g(y) == b).
y == b | p(y,b) | -(g(y) == y).
y == b | p(y,b) | p(y,g(y)).
y == b | p(y,b) | p(g(y),y).
y == k | -(y == m) | p(y,k).
y == k | -(y == b) | p(y,k).

% equality axioms

x == x.
-(x == y) | y == x.
-(x == y) | -(y == z) | x == z.
-(x == y) | -p(x,z) | p(y,z).
-(x == y) | -p(z,x) | p(z,y).
-(x == y) | f(x) == f(y).
-(x == y) | g(x) == g(y).

end_of_list.