% 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.