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.