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-1
f(y) = (((y+ (z+x)@ )@ + (y+x)@ )@ ).        % CND-absorb
end_of_list.
