op(400, xfx, ^). op(400, xfx, v). set(demod_inf). set(sos_queue). assign(max_given, 1). % Construct a single axiom for WAL. % In (17) and (18), constants B, and C are used to prevent % introduction of unnecessary variables. In the result, B % and C are replaced with x1 and x2, respectively. list(demodulators). p(x,y,z) = (x ^ z) v (y ^ (x v z)). % (10) f(x) = ((x v B) ^ (C v x)) ^ x. % (17) g(x) = ((x ^ B) v (C ^ x)) v x. % (18) end_of_list. list(sos). p(p(x,y,y),p(x,p(y,z,f(y)),g(y)),u)=y. % (8) end_of_list.