MAYBE

Problem:
 f(nil()) -> nil()
 f(.(nil(),y)) -> .(nil(),f(y))
 f(.(.(x,y),z)) -> f(.(x,.(y,z)))
 g(nil()) -> nil()
 g(.(x,nil())) -> .(g(x),nil())
 g(.(x,.(y,z))) -> g(.(.(x,y),z))

Proof:
 DP Processor:
  DPs:
   f#(.(nil(),y)) -> f#(y)
   f#(.(.(x,y),z)) -> f#(.(x,.(y,z)))
   g#(.(x,nil())) -> g#(x)
   g#(.(x,.(y,z))) -> g#(.(.(x,y),z))
  TRS:
   f(nil()) -> nil()
   f(.(nil(),y)) -> .(nil(),f(y))
   f(.(.(x,y),z)) -> f(.(x,.(y,z)))
   g(nil()) -> nil()
   g(.(x,nil())) -> .(g(x),nil())
   g(.(x,.(y,z))) -> g(.(.(x,y),z))
  EDG Processor:
   DPs:
    f#(.(nil(),y)) -> f#(y)
    f#(.(.(x,y),z)) -> f#(.(x,.(y,z)))
    g#(.(x,nil())) -> g#(x)
    g#(.(x,.(y,z))) -> g#(.(.(x,y),z))
   TRS:
    f(nil()) -> nil()
    f(.(nil(),y)) -> .(nil(),f(y))
    f(.(.(x,y),z)) -> f(.(x,.(y,z)))
    g(nil()) -> nil()
    g(.(x,nil())) -> .(g(x),nil())
    g(.(x,.(y,z))) -> g(.(.(x,y),z))
   graph:
    g#(.(x,.(y,z))) -> g#(.(.(x,y),z)) -> g#(.(x,nil())) -> g#(x)
    g#(.(x,.(y,z))) -> g#(.(.(x,y),z)) -> g#(.(x,.(y,z))) -> g#(.(.(x,y),z))
    g#(.(x,nil())) -> g#(x) -> g#(.(x,nil())) -> g#(x)
    g#(.(x,nil())) -> g#(x) -> g#(.(x,.(y,z))) -> g#(.(.(x,y),z))
    f#(.(.(x,y),z)) -> f#(.(x,.(y,z))) -> f#(.(nil(),y)) -> f#(y)
    f#(.(.(x,y),z)) -> f#(.(x,.(y,z))) -> f#(.(.(x,y),z)) -> f#(.(x,.(y,z)))
    f#(.(nil(),y)) -> f#(y) -> f#(.(nil(),y)) -> f#(y)
    f#(.(nil(),y)) -> f#(y) -> f#(.(.(x,y),z)) -> f#(.(x,.(y,z)))
   SCC Processor:
    #sccs: 2
    #rules: 4
    #arcs: 8/16
    DPs:
     f#(.(.(x,y),z)) -> f#(.(x,.(y,z)))
     f#(.(nil(),y)) -> f#(y)
    TRS:
     f(nil()) -> nil()
     f(.(nil(),y)) -> .(nil(),f(y))
     f(.(.(x,y),z)) -> f(.(x,.(y,z)))
     g(nil()) -> nil()
     g(.(x,nil())) -> .(g(x),nil())
     g(.(x,.(y,z))) -> g(.(.(x,y),z))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [f#](x0) = x0 + 1,
      
      [g](x0) = x0,
      
      [.](x0, x1) = x0 + x1,
      
      [f](x0) = x0,
      
      [nil] = 1
     orientation:
      f#(.(.(x,y),z)) = x + y + z + 1 >= x + y + z + 1 = f#(.(x,.(y,z)))
      
      f#(.(nil(),y)) = y + 2 >= y + 1 = f#(y)
      
      f(nil()) = 1 >= 1 = nil()
      
      f(.(nil(),y)) = y + 1 >= y + 1 = .(nil(),f(y))
      
      f(.(.(x,y),z)) = x + y + z >= x + y + z = f(.(x,.(y,z)))
      
      g(nil()) = 1 >= 1 = nil()
      
      g(.(x,nil())) = x + 1 >= x + 1 = .(g(x),nil())
      
      g(.(x,.(y,z))) = x + y + z >= x + y + z = g(.(.(x,y),z))
     problem:
      DPs:
       f#(.(.(x,y),z)) -> f#(.(x,.(y,z)))
      TRS:
       f(nil()) -> nil()
       f(.(nil(),y)) -> .(nil(),f(y))
       f(.(.(x,y),z)) -> f(.(x,.(y,z)))
       g(nil()) -> nil()
       g(.(x,nil())) -> .(g(x),nil())
       g(.(x,.(y,z))) -> g(.(.(x,y),z))
     Open
    
    DPs:
     g#(.(x,.(y,z))) -> g#(.(.(x,y),z))
     g#(.(x,nil())) -> g#(x)
    TRS:
     f(nil()) -> nil()
     f(.(nil(),y)) -> .(nil(),f(y))
     f(.(.(x,y),z)) -> f(.(x,.(y,z)))
     g(nil()) -> nil()
     g(.(x,nil())) -> .(g(x),nil())
     g(.(x,.(y,z))) -> g(.(.(x,y),z))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [g#](x0) = x0,
      
      [g](x0) = x0 + 1,
      
      [.](x0, x1) = x0 + x1 + 1,
      
      [f](x0) = x0,
      
      [nil] = 1
     orientation:
      g#(.(x,.(y,z))) = x + y + z + 2 >= x + y + z + 2 = g#(.(.(x,y),z))
      
      g#(.(x,nil())) = x + 2 >= x = g#(x)
      
      f(nil()) = 1 >= 1 = nil()
      
      f(.(nil(),y)) = y + 2 >= y + 2 = .(nil(),f(y))
      
      f(.(.(x,y),z)) = x + y + z + 2 >= x + y + z + 2 = f(.(x,.(y,z)))
      
      g(nil()) = 2 >= 1 = nil()
      
      g(.(x,nil())) = x + 3 >= x + 3 = .(g(x),nil())
      
      g(.(x,.(y,z))) = x + y + z + 3 >= x + y + z + 3 = g(.(.(x,y),z))
     problem:
      DPs:
       g#(.(x,.(y,z))) -> g#(.(.(x,y),z))
      TRS:
       f(nil()) -> nil()
       f(.(nil(),y)) -> .(nil(),f(y))
       f(.(.(x,y),z)) -> f(.(x,.(y,z)))
       g(nil()) -> nil()
       g(.(x,nil())) -> .(g(x),nil())
       g(.(x,.(y,z))) -> g(.(.(x,y),z))
     Open