% ----------------------------------------------------- % The following is output from the gL clause generator. % ----------------------------------------------------- formulas(assumptions). % Signature: [['f', 2], ['g', 1]] % Clauses to implement gL to nesting level 2 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(f(f(z,x0),x1),x2) != f(f(f(z,y0),y1),y2) | f(f(f(w,x0),x1),x2) = f(f(f(w,y0),y1),y2) # label("gL"). f(x0,f(f(z,x1),x2)) != f(y0,f(f(z,y1),y2)) | f(x0,f(f(w,x1),x2)) = f(y0,f(f(w,y1),y2)) # label("gL"). g(f(f(z,x0),x1)) != g(f(f(z,y0),y1)) | g(f(f(w,x0),x1)) = g(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"). f(f(x0,f(z,x1)),x2) != f(f(y0,f(z,y1)),y2) | f(f(x0,f(w,x1)),x2) = f(f(y0,f(w,y1)),y2) # label("gL"). f(x0,f(x1,f(z,x2))) != f(y0,f(y1,f(z,y2))) | f(x0,f(x1,f(w,x2))) = f(y0,f(y1,f(w,y2))) # label("gL"). g(f(x0,f(z,x1))) != g(f(y0,f(z,y1))) | g(f(x0,f(w,x1))) = g(f(y0,f(w,y1))) # label("gL"). g(f(z,x0)) != g(f(z,y0)) | g(f(w,x0)) = g(f(w,y0)) # label("gL"). f(g(f(z,x0)),x1) != f(g(f(z,y0)),y1) | f(g(f(w,x0)),x1) = f(g(f(w,y0)),y1) # label("gL"). f(x0,g(f(z,x1))) != f(y0,g(f(z,y1))) | f(x0,g(f(w,x1))) = f(y0,g(f(w,y1))) # label("gL"). g(g(f(z,x0))) != g(g(f(z,y0))) | g(g(f(w,x0))) = g(g(f(w,y0))) # 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(f(f(x0,z),x1),x2) != f(f(f(y0,z),y1),y2) | f(f(f(x0,w),x1),x2) = f(f(f(y0,w),y1),y2) # label("gL"). f(x0,f(f(x1,z),x2)) != f(y0,f(f(y1,z),y2)) | f(x0,f(f(x1,w),x2)) = f(y0,f(f(y1,w),y2)) # label("gL"). g(f(f(x0,z),x1)) != g(f(f(y0,z),y1)) | g(f(f(x0,w),x1)) = g(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"). f(f(x0,f(x1,z)),x2) != f(f(y0,f(y1,z)),y2) | f(f(x0,f(x1,w)),x2) = f(f(y0,f(y1,w)),y2) # label("gL"). f(x0,f(x1,f(x2,z))) != f(y0,f(y1,f(y2,z))) | f(x0,f(x1,f(x2,w))) = f(y0,f(y1,f(y2,w))) # label("gL"). g(f(x0,f(x1,z))) != g(f(y0,f(y1,z))) | g(f(x0,f(x1,w))) = g(f(y0,f(y1,w))) # label("gL"). g(f(x0,z)) != g(f(y0,z)) | g(f(x0,w)) = g(f(y0,w)) # label("gL"). f(g(f(x0,z)),x1) != f(g(f(y0,z)),y1) | f(g(f(x0,w)),x1) = f(g(f(y0,w)),y1) # label("gL"). f(x0,g(f(x1,z))) != f(y0,g(f(y1,z))) | f(x0,g(f(x1,w))) = f(y0,g(f(y1,w))) # label("gL"). g(g(f(x0,z))) != g(g(f(y0,z))) | g(g(f(x0,w))) = g(g(f(y0,w))) # label("gL"). g(z) != g(z) | g(w) = g(w) # label("gL"). f(g(z),x0) != f(g(z),y0) | f(g(w),x0) = f(g(w),y0) # label("gL"). f(f(g(z),x0),x1) != f(f(g(z),y0),y1) | f(f(g(w),x0),x1) = f(f(g(w),y0),y1) # label("gL"). f(x0,f(g(z),x1)) != f(y0,f(g(z),y1)) | f(x0,f(g(w),x1)) = f(y0,f(g(w),y1)) # label("gL"). g(f(g(z),x0)) != g(f(g(z),y0)) | g(f(g(w),x0)) = g(f(g(w),y0)) # label("gL"). f(x0,g(z)) != f(y0,g(z)) | f(x0,g(w)) = f(y0,g(w)) # label("gL"). f(f(x0,g(z)),x1) != f(f(y0,g(z)),y1) | f(f(x0,g(w)),x1) = f(f(y0,g(w)),y1) # label("gL"). f(x0,f(x1,g(z))) != f(y0,f(y1,g(z))) | f(x0,f(x1,g(w))) = f(y0,f(y1,g(w))) # label("gL"). g(f(x0,g(z))) != g(f(y0,g(z))) | g(f(x0,g(w))) = g(f(y0,g(w))) # label("gL"). g(g(z)) != g(g(z)) | g(g(w)) = g(g(w)) # label("gL"). f(g(g(z)),x0) != f(g(g(z)),y0) | f(g(g(w)),x0) = f(g(g(w)),y0) # label("gL"). f(x0,g(g(z))) != f(y0,g(g(z))) | f(x0,g(g(w))) = f(y0,g(g(w))) # label("gL"). g(g(g(z))) != g(g(g(z))) | g(g(g(w))) = g(g(g(w))) # label("gL"). end_of_list.