MAYBE
* Step 1: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            f(0(),x2) -> 0()
            f(S(x),0()) -> 0()
            f(S(x'),S(x)) -> h(g(x',S(x)),f(S(S(S(x'))),x))
            g(0(),x2) -> 0()
            g(S(x),0()) -> 0()
            g(S(x),S(x')) -> h(f(S(x),S(x')),g(x,S(S(S(x')))))
            h(0(),0()) -> 0()
            h(0(),S(x)) -> h(0(),x)
            h(S(x),x2) -> h(x,x2)
        - Signature:
            {f/2,g/2,h/2} / {0/0,S/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g,h} and constructors {0,S}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(h) = {1,2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
            p(0) = [0]                  
            p(S) = [1] x1 + [8]         
            p(f) = [0]                  
            p(g) = [0]                  
            p(h) = [1] x1 + [1] x2 + [0]
          
          Following rules are strictly oriented:
          h(0(),S(x)) = [1] x + [8]         
                      > [1] x + [0]         
                      = h(0(),x)            
          
           h(S(x),x2) = [1] x + [1] x2 + [8]
                      > [1] x + [1] x2 + [0]
                      = h(x,x2)             
          
          
          Following rules are (at-least) weakly oriented:
              f(0(),x2) =  [0]                              
                        >= [0]                              
                        =  0()                              
          
            f(S(x),0()) =  [0]                              
                        >= [0]                              
                        =  0()                              
          
          f(S(x'),S(x)) =  [0]                              
                        >= [0]                              
                        =  h(g(x',S(x)),f(S(S(S(x'))),x))   
          
              g(0(),x2) =  [0]                              
                        >= [0]                              
                        =  0()                              
          
            g(S(x),0()) =  [0]                              
                        >= [0]                              
                        =  0()                              
          
          g(S(x),S(x')) =  [0]                              
                        >= [0]                              
                        =  h(f(S(x),S(x')),g(x,S(S(S(x')))))
          
             h(0(),0()) =  [0]                              
                        >= [0]                              
                        =  0()                              
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            f(0(),x2) -> 0()
            f(S(x),0()) -> 0()
            f(S(x'),S(x)) -> h(g(x',S(x)),f(S(S(S(x'))),x))
            g(0(),x2) -> 0()
            g(S(x),0()) -> 0()
            g(S(x),S(x')) -> h(f(S(x),S(x')),g(x,S(S(S(x')))))
            h(0(),0()) -> 0()
        - Weak TRS:
            h(0(),S(x)) -> h(0(),x)
            h(S(x),x2) -> h(x,x2)
        - Signature:
            {f/2,g/2,h/2} / {0/0,S/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g,h} and constructors {0,S}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(h) = {1,2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
            p(0) = [0]                  
            p(S) = [1] x1 + [0]         
            p(f) = [9]                  
            p(g) = [0]                  
            p(h) = [1] x1 + [1] x2 + [1]
          
          Following rules are strictly oriented:
            f(0(),x2) = [9]
                      > [0]
                      = 0()
          
          f(S(x),0()) = [9]
                      > [0]
                      = 0()
          
           h(0(),0()) = [1]
                      > [0]
                      = 0()
          
          
          Following rules are (at-least) weakly oriented:
          f(S(x'),S(x)) =  [9]                              
                        >= [10]                             
                        =  h(g(x',S(x)),f(S(S(S(x'))),x))   
          
              g(0(),x2) =  [0]                              
                        >= [0]                              
                        =  0()                              
          
            g(S(x),0()) =  [0]                              
                        >= [0]                              
                        =  0()                              
          
          g(S(x),S(x')) =  [0]                              
                        >= [10]                             
                        =  h(f(S(x),S(x')),g(x,S(S(S(x')))))
          
            h(0(),S(x)) =  [1] x + [1]                      
                        >= [1] x + [1]                      
                        =  h(0(),x)                         
          
             h(S(x),x2) =  [1] x + [1] x2 + [1]             
                        >= [1] x + [1] x2 + [1]             
                        =  h(x,x2)                          
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            f(S(x'),S(x)) -> h(g(x',S(x)),f(S(S(S(x'))),x))
            g(0(),x2) -> 0()
            g(S(x),0()) -> 0()
            g(S(x),S(x')) -> h(f(S(x),S(x')),g(x,S(S(S(x')))))
        - Weak TRS:
            f(0(),x2) -> 0()
            f(S(x),0()) -> 0()
            h(0(),0()) -> 0()
            h(0(),S(x)) -> h(0(),x)
            h(S(x),x2) -> h(x,x2)
        - Signature:
            {f/2,g/2,h/2} / {0/0,S/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g,h} and constructors {0,S}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(h) = {1,2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
            p(0) = [2]                  
            p(S) = [1] x1 + [8]         
            p(f) = [6]                  
            p(g) = [13]                 
            p(h) = [1] x1 + [1] x2 + [2]
          
          Following rules are strictly oriented:
            g(0(),x2) = [13]
                      > [2] 
                      = 0() 
          
          g(S(x),0()) = [13]
                      > [2] 
                      = 0() 
          
          
          Following rules are (at-least) weakly oriented:
              f(0(),x2) =  [6]                              
                        >= [2]                              
                        =  0()                              
          
            f(S(x),0()) =  [6]                              
                        >= [2]                              
                        =  0()                              
          
          f(S(x'),S(x)) =  [6]                              
                        >= [21]                             
                        =  h(g(x',S(x)),f(S(S(S(x'))),x))   
          
          g(S(x),S(x')) =  [13]                             
                        >= [21]                             
                        =  h(f(S(x),S(x')),g(x,S(S(S(x')))))
          
             h(0(),0()) =  [6]                              
                        >= [2]                              
                        =  0()                              
          
            h(0(),S(x)) =  [1] x + [12]                     
                        >= [1] x + [4]                      
                        =  h(0(),x)                         
          
             h(S(x),x2) =  [1] x + [1] x2 + [10]            
                        >= [1] x + [1] x2 + [2]             
                        =  h(x,x2)                          
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          f(S(x'),S(x)) -> h(g(x',S(x)),f(S(S(S(x'))),x))
          g(S(x),S(x')) -> h(f(S(x),S(x')),g(x,S(S(S(x')))))
      - Weak TRS:
          f(0(),x2) -> 0()
          f(S(x),0()) -> 0()
          g(0(),x2) -> 0()
          g(S(x),0()) -> 0()
          h(0(),0()) -> 0()
          h(0(),S(x)) -> h(0(),x)
          h(S(x),x2) -> h(x,x2)
      - Signature:
          {f/2,g/2,h/2} / {0/0,S/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {f,g,h} and constructors {0,S}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE