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

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

list(sos).

p(p(f1(x),x,f2(y)),y,p(z,u,p(z,v,v))) = z.  % Schema-2

end_of_list.

list(demodulators).

p(x,y,z) = (x # (y # (y # z))) # ((y # (y # x)) # z).  % Pixley-4

f1(x) = (x # z) # (x # (y # z)).  % Veroff-27a

f2(x) = (y # x) # (x # x).                             % Meredith-1c

end_of_list.