% -----------------------------------------------------
% The following is output from the gL clause generator.
% -----------------------------------------------------

formulas(assumptions).

% Signature:  [['f', 2], ['g', 2]]
% Clauses to implement gL to nesting level 1

f(z,x0) != f(z,y0) | f(w,x0) = f(w,y0) # label("gL").
f(f(z,x0),x1) != f(f(z,y0),y1) | f(f(w,x0),x1) = f(f(w,y0),y1) # label("gL").
f(x0,f(z,x1)) != f(y0,f(z,y1)) | f(x0,f(w,x1)) = f(y0,f(w,y1)) # label("gL").
g(f(z,x0),x1) != g(f(z,y0),y1) | g(f(w,x0),x1) = g(f(w,y0),y1) # label("gL").
g(x0,f(z,x1)) != g(y0,f(z,y1)) | g(x0,f(w,x1)) = g(y0,f(w,y1)) # label("gL").
f(x0,z) != f(y0,z) | f(x0,w) = f(y0,w) # label("gL").
f(f(x0,z),x1) != f(f(y0,z),y1) | f(f(x0,w),x1) = f(f(y0,w),y1) # label("gL").
f(x0,f(x1,z)) != f(y0,f(y1,z)) | f(x0,f(x1,w)) = f(y0,f(y1,w)) # label("gL").
g(f(x0,z),x1) != g(f(y0,z),y1) | g(f(x0,w),x1) = g(f(y0,w),y1) # label("gL").
g(x0,f(x1,z)) != g(y0,f(y1,z)) | g(x0,f(x1,w)) = g(y0,f(y1,w)) # label("gL").
g(z,x0) != g(z,y0) | g(w,x0) = g(w,y0) # label("gL").
f(g(z,x0),x1) != f(g(z,y0),y1) | f(g(w,x0),x1) = f(g(w,y0),y1) # label("gL").
f(x0,g(z,x1)) != f(y0,g(z,y1)) | f(x0,g(w,x1)) = f(y0,g(w,y1)) # label("gL").
g(g(z,x0),x1) != g(g(z,y0),y1) | g(g(w,x0),x1) = g(g(w,y0),y1) # label("gL").
g(x0,g(z,x1)) != g(y0,g(z,y1)) | g(x0,g(w,x1)) = g(y0,g(w,y1)) # label("gL").
g(x0,z) != g(y0,z) | g(x0,w) = g(y0,w) # label("gL").
f(g(x0,z),x1) != f(g(y0,z),y1) | f(g(x0,w),x1) = f(g(y0,w),y1) # label("gL").
f(x0,g(x1,z)) != f(y0,g(y1,z)) | f(x0,g(x1,w)) = f(y0,g(y1,w)) # label("gL").
g(g(x0,z),x1) != g(g(y0,z),y1) | g(g(x0,w),x1) = g(g(y0,w),y1) # label("gL").
g(x0,g(x1,z)) != g(y0,g(y1,z)) | g(x0,g(x1,w)) = g(y0,g(y1,w)) # label("gL").

end_of_list.