% terminated after 2 stages (variant)
% terminated after 2 stages (subsumption)
%querytabled * 5 (app (lam [x] (app x x)) (lam [y] y)) -->* M'.

% terminated after 3 stages (variant)
% terminated after 3 stages (subsumption)

%querytabled * 6 (app (lam [x] (app x x)) (app (lam [y] y) (lam [z] z))) -->* M'.

% Parallel multi-step reduction

% terminate after 4 stages (variant)
% terminated after 4 stages (subsumption)
%querytabled * 10 (app (lam [x] (app x x)) (lam [y] y)) =>* M'.


% terminated after 5 stages (variant)
% terminated after 5 stages (subsumption)
%querytabled * 5 (app (lam [x] (app x x)) (app (lam [y] y) (lam [z] z))) =>* M'.


% parallel conversion