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

end_of_list.

