Clause Generator for Inference Rule gL

Enter signature as a list of alternating name/arity values:
(for example, "f 2 g 2 h 3", with no punctuation)

Input maximum nesting level:

(where, for example, f(x,g(y,z)) is nesting level 1)

Action:

Note: Infix operators can be handled by generating prefix versions and then transforming the results with the "Rewriter" program (included in the Prover9 distribution).

Example output (signature "f 2 g 2" to nesting level 1). 

   % -----------------------------------------------------
   % 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.