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(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(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(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(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(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(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) = [0]                  
            p(g) = [0]                  
            p(h) = [1] x1 + [1] x2 + [3]
          
          Following rules are strictly oriented:
          h(0(),0()) = [3]
                     > [0]
                     = 0()
          
          
          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]                           
                        >= [3]                           
                        =  h(g(x',S(x)),f(S(S(x')),x))   
          
              g(0(),x2) =  [0]                           
                        >= [0]                           
                        =  0()                           
          
            g(S(x),0()) =  [0]                           
                        >= [0]                           
                        =  0()                           
          
          g(S(x),S(x')) =  [0]                           
                        >= [3]                           
                        =  h(f(S(x),S(x')),g(x,S(S(x'))))
          
            h(0(),S(x)) =  [1] x + [3]                   
                        >= [1] x + [3]                   
                        =  h(0(),x)                      
          
             h(S(x),x2) =  [1] x + [1] x2 + [3]          
                        >= [1] x + [1] x2 + [3]          
                        =  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(0(),x2) -> 0()
            f(S(x),0()) -> 0()
            f(S(x'),S(x)) -> h(g(x',S(x)),f(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(x'))))
        - Weak TRS:
            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 + [1]         
            p(f) = [1]                  
            p(g) = [2]                  
            p(h) = [1] x1 + [1] x2 + [8]
          
          Following rules are strictly oriented:
            f(0(),x2) = [1]
                      > [0]
                      = 0()
          
          f(S(x),0()) = [1]
                      > [0]
                      = 0()
          
            g(0(),x2) = [2]
                      > [0]
                      = 0()
          
          g(S(x),0()) = [2]
                      > [0]
                      = 0()
          
          
          Following rules are (at-least) weakly oriented:
          f(S(x'),S(x)) =  [1]                           
                        >= [11]                          
                        =  h(g(x',S(x)),f(S(S(x')),x))   
          
          g(S(x),S(x')) =  [2]                           
                        >= [11]                          
                        =  h(f(S(x),S(x')),g(x,S(S(x'))))
          
             h(0(),0()) =  [8]                           
                        >= [0]                           
                        =  0()                           
          
            h(0(),S(x)) =  [1] x + [9]                   
                        >= [1] x + [8]                   
                        =  h(0(),x)                      
          
             h(S(x),x2) =  [1] x + [1] x2 + [9]          
                        >= [1] x + [1] x2 + [8]          
                        =  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(x')),x))
          g(S(x),S(x')) -> h(f(S(x),S(x')),g(x,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