MAYBE

Problem:
 g(A()) -> A()
 g(B()) -> A()
 g(B()) -> B()
 g(C()) -> A()
 g(C()) -> B()
 g(C()) -> C()
 foldB(t,0()) -> t
 foldB(t,s(n)) -> f(foldB(t,n),B())
 foldC(t,0()) -> t
 foldC(t,s(n)) -> f(foldC(t,n),C())
 f(t,x) -> f'(t,g(x))
 f'(triple(a,b,c),C()) -> triple(a,b,s(c))
 f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
 f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
 f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c)

Proof:
 Complexity Transformation Processor:
  strict:
   g(A()) -> A()
   g(B()) -> A()
   g(B()) -> B()
   g(C()) -> A()
   g(C()) -> B()
   g(C()) -> C()
   foldB(t,0()) -> t
   foldB(t,s(n)) -> f(foldB(t,n),B())
   foldC(t,0()) -> t
   foldC(t,s(n)) -> f(foldC(t,n),C())
   f(t,x) -> f'(t,g(x))
   f'(triple(a,b,c),C()) -> triple(a,b,s(c))
   f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
   f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
   f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [f''](x0) = x0 + 1,
     
     [triple](x0, x1, x2) = x0 + x1 + x2,
     
     [f'](x0, x1) = x0 + x1,
     
     [foldC](x0, x1) = x0 + x1,
     
     [f](x0, x1) = x0 + x1,
     
     [s](x0) = x0,
     
     [foldB](x0, x1) = x0 + x1,
     
     [0] = 0,
     
     [C] = 0,
     
     [B] = 0,
     
     [g](x0) = x0,
     
     [A] = 0
    orientation:
     g(A()) = 0 >= 0 = A()
     
     g(B()) = 0 >= 0 = A()
     
     g(B()) = 0 >= 0 = B()
     
     g(C()) = 0 >= 0 = A()
     
     g(C()) = 0 >= 0 = B()
     
     g(C()) = 0 >= 0 = C()
     
     foldB(t,0()) = t >= t = t
     
     foldB(t,s(n)) = n + t >= n + t = f(foldB(t,n),B())
     
     foldC(t,0()) = t >= t = t
     
     foldC(t,s(n)) = n + t >= n + t = f(foldC(t,n),C())
     
     f(t,x) = t + x >= t + x = f'(t,g(x))
     
     f'(triple(a,b,c),C()) = a + b + c >= a + b + c = triple(a,b,s(c))
     
     f'(triple(a,b,c),B()) = a + b + c >= a + b + c = f(triple(a,b,c),A())
     
     f'(triple(a,b,c),A()) = a + b + c >= a + b + c + 1 = f''(foldB(triple(s(a),0(),c),b))
     
     f''(triple(a,b,c)) = a + b + c + 1 >= a + b + c = foldC(triple(a,b,0()),c)
    problem:
     strict:
      g(A()) -> A()
      g(B()) -> A()
      g(B()) -> B()
      g(C()) -> A()
      g(C()) -> B()
      g(C()) -> C()
      foldB(t,0()) -> t
      foldB(t,s(n)) -> f(foldB(t,n),B())
      foldC(t,0()) -> t
      foldC(t,s(n)) -> f(foldC(t,n),C())
      f(t,x) -> f'(t,g(x))
      f'(triple(a,b,c),C()) -> triple(a,b,s(c))
      f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
      f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
     weak:
      f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c)
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [f''](x0) = x0,
       
       [triple](x0, x1, x2) = x0 + x1 + x2,
       
       [f'](x0, x1) = x0 + x1 + 1,
       
       [foldC](x0, x1) = x0 + x1,
       
       [f](x0, x1) = x0 + x1,
       
       [s](x0) = x0,
       
       [foldB](x0, x1) = x0 + x1,
       
       [0] = 0,
       
       [C] = 0,
       
       [B] = 0,
       
       [g](x0) = x0,
       
       [A] = 0
      orientation:
       g(A()) = 0 >= 0 = A()
       
       g(B()) = 0 >= 0 = A()
       
       g(B()) = 0 >= 0 = B()
       
       g(C()) = 0 >= 0 = A()
       
       g(C()) = 0 >= 0 = B()
       
       g(C()) = 0 >= 0 = C()
       
       foldB(t,0()) = t >= t = t
       
       foldB(t,s(n)) = n + t >= n + t = f(foldB(t,n),B())
       
       foldC(t,0()) = t >= t = t
       
       foldC(t,s(n)) = n + t >= n + t = f(foldC(t,n),C())
       
       f(t,x) = t + x >= t + x + 1 = f'(t,g(x))
       
       f'(triple(a,b,c),C()) = a + b + c + 1 >= a + b + c = triple(a,b,s(c))
       
       f'(triple(a,b,c),B()) = a + b + c + 1 >= a + b + c = f(triple(a,b,c),A())
       
       f'(triple(a,b,c),A()) = a + b + c + 1 >= a + b + c = f''(foldB(triple(s(a),0(),c),b))
       
       f''(triple(a,b,c)) = a + b + c >= a + b + c = foldC(triple(a,b,0()),c)
      problem:
       strict:
        g(A()) -> A()
        g(B()) -> A()
        g(B()) -> B()
        g(C()) -> A()
        g(C()) -> B()
        g(C()) -> C()
        foldB(t,0()) -> t
        foldB(t,s(n)) -> f(foldB(t,n),B())
        foldC(t,0()) -> t
        foldC(t,s(n)) -> f(foldC(t,n),C())
        f(t,x) -> f'(t,g(x))
       weak:
        f'(triple(a,b,c),C()) -> triple(a,b,s(c))
        f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
        f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
        f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c)
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [f''](x0) = x0,
         
         [triple](x0, x1, x2) = x0 + x1 + x2,
         
         [f'](x0, x1) = x0 + x1,
         
         [foldC](x0, x1) = x0 + x1,
         
         [f](x0, x1) = x0 + x1 + 1,
         
         [s](x0) = x0,
         
         [foldB](x0, x1) = x0 + x1,
         
         [0] = 0,
         
         [C] = 0,
         
         [B] = 1,
         
         [g](x0) = x0,
         
         [A] = 0
        orientation:
         g(A()) = 0 >= 0 = A()
         
         g(B()) = 1 >= 0 = A()
         
         g(B()) = 1 >= 1 = B()
         
         g(C()) = 0 >= 0 = A()
         
         g(C()) = 0 >= 1 = B()
         
         g(C()) = 0 >= 0 = C()
         
         foldB(t,0()) = t >= t = t
         
         foldB(t,s(n)) = n + t >= n + t + 2 = f(foldB(t,n),B())
         
         foldC(t,0()) = t >= t = t
         
         foldC(t,s(n)) = n + t >= n + t + 1 = f(foldC(t,n),C())
         
         f(t,x) = t + x + 1 >= t + x = f'(t,g(x))
         
         f'(triple(a,b,c),C()) = a + b + c >= a + b + c = triple(a,b,s(c))
         
         f'(triple(a,b,c),B()) = a + b + c + 1 >= a + b + c + 1 = f(triple(a,b,c),A())
         
         f'(triple(a,b,c),A()) = a + b + c >= a + b + c = f''(foldB(triple(s(a),0(),c),b))
         
         f''(triple(a,b,c)) = a + b + c >= a + b + c = foldC(triple(a,b,0()),c)
        problem:
         strict:
          g(A()) -> A()
          g(B()) -> B()
          g(C()) -> A()
          g(C()) -> B()
          g(C()) -> C()
          foldB(t,0()) -> t
          foldB(t,s(n)) -> f(foldB(t,n),B())
          foldC(t,0()) -> t
          foldC(t,s(n)) -> f(foldC(t,n),C())
         weak:
          g(B()) -> A()
          f(t,x) -> f'(t,g(x))
          f'(triple(a,b,c),C()) -> triple(a,b,s(c))
          f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
          f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
          f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c)
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [f''](x0) = x0,
           
           [triple](x0, x1, x2) = x0 + x1 + x2,
           
           [f'](x0, x1) = x0 + x1,
           
           [foldC](x0, x1) = x0 + x1,
           
           [f](x0, x1) = x0 + x1,
           
           [s](x0) = x0,
           
           [foldB](x0, x1) = x0 + x1 + 1,
           
           [0] = 0,
           
           [C] = 0,
           
           [B] = 1,
           
           [g](x0) = x0,
           
           [A] = 1
          orientation:
           g(A()) = 1 >= 1 = A()
           
           g(B()) = 1 >= 1 = B()
           
           g(C()) = 0 >= 1 = A()
           
           g(C()) = 0 >= 1 = B()
           
           g(C()) = 0 >= 0 = C()
           
           foldB(t,0()) = t + 1 >= t = t
           
           foldB(t,s(n)) = n + t + 1 >= n + t + 2 = f(foldB(t,n),B())
           
           foldC(t,0()) = t >= t = t
           
           foldC(t,s(n)) = n + t >= n + t = f(foldC(t,n),C())
           
           g(B()) = 1 >= 1 = A()
           
           f(t,x) = t + x >= t + x = f'(t,g(x))
           
           f'(triple(a,b,c),C()) = a + b + c >= a + b + c = triple(a,b,s(c))
           
           f'(triple(a,b,c),B()) = a + b + c + 1 >= a + b + c + 1 = f(triple(a,b,c),A())
           
           f'(triple(a,b,c),A()) = a + b + c + 1 >= a + b + c + 1 = f''(foldB(triple(s(a),0(),c),b))
           
           f''(triple(a,b,c)) = a + b + c >= a + b + c = foldC(triple(a,b,0()),c)
          problem:
           strict:
            g(A()) -> A()
            g(B()) -> B()
            g(C()) -> A()
            g(C()) -> B()
            g(C()) -> C()
            foldB(t,s(n)) -> f(foldB(t,n),B())
            foldC(t,0()) -> t
            foldC(t,s(n)) -> f(foldC(t,n),C())
           weak:
            foldB(t,0()) -> t
            g(B()) -> A()
            f(t,x) -> f'(t,g(x))
            f'(triple(a,b,c),C()) -> triple(a,b,s(c))
            f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
            f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
            f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c)
          Matrix Interpretation Processor:
           dimension: 1
           max_matrix:
            1
            interpretation:
             [f''](x0) = x0,
             
             [triple](x0, x1, x2) = x0 + x1 + x2,
             
             [f'](x0, x1) = x0 + x1,
             
             [foldC](x0, x1) = x0 + x1,
             
             [f](x0, x1) = x0 + x1 + 1,
             
             [s](x0) = x0,
             
             [foldB](x0, x1) = x0 + x1,
             
             [0] = 0,
             
             [C] = 0,
             
             [B] = 1,
             
             [g](x0) = x0 + 1,
             
             [A] = 0
            orientation:
             g(A()) = 1 >= 0 = A()
             
             g(B()) = 2 >= 1 = B()
             
             g(C()) = 1 >= 0 = A()
             
             g(C()) = 1 >= 1 = B()
             
             g(C()) = 1 >= 0 = C()
             
             foldB(t,s(n)) = n + t >= n + t + 2 = f(foldB(t,n),B())
             
             foldC(t,0()) = t >= t = t
             
             foldC(t,s(n)) = n + t >= n + t + 1 = f(foldC(t,n),C())
             
             foldB(t,0()) = t >= t = t
             
             g(B()) = 2 >= 0 = A()
             
             f(t,x) = t + x + 1 >= t + x + 1 = f'(t,g(x))
             
             f'(triple(a,b,c),C()) = a + b + c >= a + b + c = triple(a,b,s(c))
             
             f'(triple(a,b,c),B()) = a + b + c + 1 >= a + b + c + 1 = f(triple(a,b,c),A())
             
             f'(triple(a,b,c),A()) = a + b + c >= a + b + c = f''(foldB(triple(s(a),0(),c),b))
             
             f''(triple(a,b,c)) = a + b + c >= a + b + c = foldC(triple(a,b,0()),c)
            problem:
             strict:
              g(C()) -> B()
              foldB(t,s(n)) -> f(foldB(t,n),B())
              foldC(t,0()) -> t
              foldC(t,s(n)) -> f(foldC(t,n),C())
             weak:
              g(A()) -> A()
              g(B()) -> B()
              g(C()) -> A()
              g(C()) -> C()
              foldB(t,0()) -> t
              g(B()) -> A()
              f(t,x) -> f'(t,g(x))
              f'(triple(a,b,c),C()) -> triple(a,b,s(c))
              f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
              f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
              f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c)
            Matrix Interpretation Processor:
             dimension: 1
             max_matrix:
              1
              interpretation:
               [f''](x0) = x0,
               
               [triple](x0, x1, x2) = x0 + x1 + x2,
               
               [f'](x0, x1) = x0 + x1 + 1,
               
               [foldC](x0, x1) = x0 + x1,
               
               [f](x0, x1) = x0 + x1 + 1,
               
               [s](x0) = x0 + 1,
               
               [foldB](x0, x1) = x0 + x1,
               
               [0] = 0,
               
               [C] = 1,
               
               [B] = 0,
               
               [g](x0) = x0,
               
               [A] = 0
              orientation:
               g(C()) = 1 >= 0 = B()
               
               foldB(t,s(n)) = n + t + 1 >= n + t + 1 = f(foldB(t,n),B())
               
               foldC(t,0()) = t >= t = t
               
               foldC(t,s(n)) = n + t + 1 >= n + t + 2 = f(foldC(t,n),C())
               
               g(A()) = 0 >= 0 = A()
               
               g(B()) = 0 >= 0 = B()
               
               g(C()) = 1 >= 0 = A()
               
               g(C()) = 1 >= 1 = C()
               
               foldB(t,0()) = t >= t = t
               
               g(B()) = 0 >= 0 = A()
               
               f(t,x) = t + x + 1 >= t + x + 1 = f'(t,g(x))
               
               f'(triple(a,b,c),C()) = a + b + c + 2 >= a + b + c + 1 = triple(a,b,s(c))
               
               f'(triple(a,b,c),B()) = a + b + c + 1 >= a + b + c + 1 = f(triple(a,b,c),A())
               
               f'(triple(a,b,c),A()) = a + b + c + 1 >= a + b + c + 1 = f''(foldB(triple(s(a),0(),c),b))
               
               f''(triple(a,b,c)) = a + b + c >= a + b + c = foldC(triple(a,b,0()),c)
              problem:
               strict:
                foldB(t,s(n)) -> f(foldB(t,n),B())
                foldC(t,0()) -> t
                foldC(t,s(n)) -> f(foldC(t,n),C())
               weak:
                g(C()) -> B()
                g(A()) -> A()
                g(B()) -> B()
                g(C()) -> A()
                g(C()) -> C()
                foldB(t,0()) -> t
                g(B()) -> A()
                f(t,x) -> f'(t,g(x))
                f'(triple(a,b,c),C()) -> triple(a,b,s(c))
                f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
                f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
                f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c)
              Matrix Interpretation Processor:
               dimension: 1
               max_matrix:
                1
                interpretation:
                 [f''](x0) = x0 + 1,
                 
                 [triple](x0, x1, x2) = x0 + x1 + x2,
                 
                 [f'](x0, x1) = x0 + x1 + 1,
                 
                 [foldC](x0, x1) = x0 + x1,
                 
                 [f](x0, x1) = x0 + x1 + 1,
                 
                 [s](x0) = x0,
                 
                 [foldB](x0, x1) = x0 + x1,
                 
                 [0] = 1,
                 
                 [C] = 1,
                 
                 [B] = 1,
                 
                 [g](x0) = x0,
                 
                 [A] = 1
                orientation:
                 foldB(t,s(n)) = n + t >= n + t + 2 = f(foldB(t,n),B())
                 
                 foldC(t,0()) = t + 1 >= t = t
                 
                 foldC(t,s(n)) = n + t >= n + t + 2 = f(foldC(t,n),C())
                 
                 g(C()) = 1 >= 1 = B()
                 
                 g(A()) = 1 >= 1 = A()
                 
                 g(B()) = 1 >= 1 = B()
                 
                 g(C()) = 1 >= 1 = A()
                 
                 g(C()) = 1 >= 1 = C()
                 
                 foldB(t,0()) = t + 1 >= t = t
                 
                 g(B()) = 1 >= 1 = A()
                 
                 f(t,x) = t + x + 1 >= t + x + 1 = f'(t,g(x))
                 
                 f'(triple(a,b,c),C()) = a + b + c + 2 >= a + b + c = triple(a,b,s(c))
                 
                 f'(triple(a,b,c),B()) = a + b + c + 2 >= a + b + c + 2 = f(triple(a,b,c),A())
                 
                 f'(triple(a,b,c),A()) = a + b + c + 2 >= a + b + c + 2 = f''(foldB(triple(s(a),0(),c),b))
                 
                 f''(triple(a,b,c)) = a + b + c + 1 >= a + b + c + 1 = foldC(triple(a,b,0()),c)
                problem:
                 strict:
                  foldB(t,s(n)) -> f(foldB(t,n),B())
                  foldC(t,s(n)) -> f(foldC(t,n),C())
                 weak:
                  foldC(t,0()) -> t
                  g(C()) -> B()
                  g(A()) -> A()
                  g(B()) -> B()
                  g(C()) -> A()
                  g(C()) -> C()
                  foldB(t,0()) -> t
                  g(B()) -> A()
                  f(t,x) -> f'(t,g(x))
                  f'(triple(a,b,c),C()) -> triple(a,b,s(c))
                  f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
                  f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
                  f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c)
                Matrix Interpretation Processor:
                 dimension: 2
                 max_matrix:
                  [1 1]
                  [0 1]
                  interpretation:
                               [1 0]  
                   [f''](x0) = [0 0]x0,
                   
                                          [1 0]     [1 1]     [1 0]     [1]
                   [triple](x0, x1, x2) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0],
                   
                                       [1 0]  
                   [f'](x0, x1) = x0 + [0 0]x1,
                   
                                          [1 0]  
                   [foldC](x0, x1) = x0 + [0 0]x1,
                   
                                      [1 0]  
                   [f](x0, x1) = x0 + [0 0]x1,
                   
                                  [1]
                   [s](x0) = x0 + [1],
                   
                                          [1 1]  
                   [foldB](x0, x1) = x0 + [0 0]x1,
                   
                         [0]
                   [0] = [0],
                   
                         [1]
                   [C] = [0],
                   
                         [1]
                   [B] = [0],
                   
                             [1 0]  
                   [g](x0) = [0 0]x0,
                   
                         [1]
                   [A] = [0]
                  orientation:
                                   [1 1]        [2]    [1 1]        [1]                    
                   foldB(t,s(n)) = [0 0]n + t + [0] >= [0 0]n + t + [0] = f(foldB(t,n),B())
                   
                                   [1 0]        [1]    [1 0]        [1]                    
                   foldC(t,s(n)) = [0 0]n + t + [0] >= [0 0]n + t + [0] = f(foldC(t,n),C())
                   
                                            
                   foldC(t,0()) = t >= t = t
                   
                            [1]    [1]      
                   g(C()) = [0] >= [0] = B()
                   
                            [1]    [1]      
                   g(A()) = [0] >= [0] = A()
                   
                            [1]    [1]      
                   g(B()) = [0] >= [0] = B()
                   
                            [1]    [1]      
                   g(C()) = [0] >= [0] = A()
                   
                            [1]    [1]      
                   g(C()) = [0] >= [0] = C()
                   
                                            
                   foldB(t,0()) = t >= t = t
                   
                            [1]    [1]      
                   g(B()) = [0] >= [0] = A()
                   
                                [1 0]         [1 0]              
                   f(t,x) = t + [0 0]x >= t + [0 0]x = f'(t,g(x))
                   
                                           [1 0]    [1 1]    [1 0]    [2]    [1 0]    [1 1]    [1 0]    [2]                   
                   f'(triple(a,b,c),C()) = [0 0]a + [0 0]b + [0 0]c + [0] >= [0 0]a + [0 0]b + [0 0]c + [0] = triple(a,b,s(c))
                   
                                           [1 0]    [1 1]    [1 0]    [2]    [1 0]    [1 1]    [1 0]    [2]                       
                   f'(triple(a,b,c),B()) = [0 0]a + [0 0]b + [0 0]c + [0] >= [0 0]a + [0 0]b + [0 0]c + [0] = f(triple(a,b,c),A())
                   
                                           [1 0]    [1 1]    [1 0]    [2]    [1 0]    [1 1]    [1 0]    [2]                                   
                   f'(triple(a,b,c),A()) = [0 0]a + [0 0]b + [0 0]c + [0] >= [0 0]a + [0 0]b + [0 0]c + [0] = f''(foldB(triple(s(a),0(),c),b))
                   
                                        [1 0]    [1 1]    [1 0]    [1]    [1 0]    [1 1]    [1 0]    [1]                           
                   f''(triple(a,b,c)) = [0 0]a + [0 0]b + [0 0]c + [0] >= [0 0]a + [0 0]b + [0 0]c + [0] = foldC(triple(a,b,0()),c)
                  problem:
                   strict:
                    foldC(t,s(n)) -> f(foldC(t,n),C())
                   weak:
                    foldB(t,s(n)) -> f(foldB(t,n),B())
                    foldC(t,0()) -> t
                    g(C()) -> B()
                    g(A()) -> A()
                    g(B()) -> B()
                    g(C()) -> A()
                    g(C()) -> C()
                    foldB(t,0()) -> t
                    g(B()) -> A()
                    f(t,x) -> f'(t,g(x))
                    f'(triple(a,b,c),C()) -> triple(a,b,s(c))
                    f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
                    f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
                    f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c)
                  Open