% 1.  If a lattice with join operation + and meet operation *
% satisfies the equation x+(y*z) = (x+y)*(x+z) then it satisfies
% the equation x*(y+z) = (x*y)+(x*z). This example illustrates
% the sos_queue flag.
%
% Contributed by John Kalman (kalman@math.auckland.ac.nz)

  set(knuth_bendix).
  clear(print_kept). clear(print_new_demod).
  clear(print_back_demod). clear(print_back_sub).
  set(sos_queue).
  % assign(pick_given_ratio,1).
  assign(max_mem,5000).
  assign(stats_level,1).

  list(usable).
    x=x.
    x+y=y+x.
    x*y=y*x.
    (x+y)+z=x+y+z. 
    (x*y)*z=x*y*z. 
    x+ (x*y)=x.
    x* (x+y)=x.
  end_of_list.

  list(sos).
    x+ (y*z)= (x+y)* (x+z).
    a* (b+c)!= (a*b)+ (a*c).
  end_of_list.