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) = ((y # (x # z)) # z) # (x # (y # (z # z))).  % Pixley-8 (P-21)
f(x) = (x # z) # (x # (y # z)).  % Veroff-27a
end_of_list.