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.