op(400, xfx, [*,+,#]).  % infix operators
op(300, yf, @).         % postfix operator

set(demod_inf).
assign(max_given, 1).

list(sos).
p(p(x,x,y),p(f(z),u,z),z)=y.  % Schema-1
end_of_list.

list(demodulators).
p(x,y,z) = ((x + y@)@ + ((x + z)@ + (y@ + z)@))@.      % Pixley-9
f(y) = ((((x+z)@ +y)@ + (y+x)@ )@ ).                   % DN-absorb
end_of_list.