MAYBE
* Step 1: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            a__c() -> a()
            a__c() -> b()
            a__c() -> c()
            a__f(X1,X2,X3) -> f(X1,X2,X3)
            a__f(a(),b(),X) -> a__f(X,X,mark(X))
            mark(a()) -> a()
            mark(b()) -> b()
            mark(c()) -> a__c()
            mark(f(X1,X2,X3)) -> a__f(X1,X2,mark(X3))
        - Signature:
            {a__c/0,a__f/3,mark/1} / {a/0,b/0,c/0,f/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__c,a__f,mark} and constructors {a,b,c,f}
    + 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(a__f) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
               p(a) = [0]         
            p(a__c) = [8]         
            p(a__f) = [1] x3 + [5]
               p(b) = [0]         
               p(c) = [0]         
               p(f) = [1] x3 + [0]
            p(mark) = [1] x1 + [0]
          
          Following rules are strictly oriented:
                  a__c() = [8]         
                         > [0]         
                         = a()         
          
                  a__c() = [8]         
                         > [0]         
                         = b()         
          
                  a__c() = [8]         
                         > [0]         
                         = c()         
          
          a__f(X1,X2,X3) = [1] X3 + [5]
                         > [1] X3 + [0]
                         = f(X1,X2,X3) 
          
          
          Following rules are (at-least) weakly oriented:
            a__f(a(),b(),X) =  [1] X + [5]         
                            >= [1] X + [5]         
                            =  a__f(X,X,mark(X))   
          
                  mark(a()) =  [0]                 
                            >= [0]                 
                            =  a()                 
          
                  mark(b()) =  [0]                 
                            >= [0]                 
                            =  b()                 
          
                  mark(c()) =  [0]                 
                            >= [8]                 
                            =  a__c()              
          
          mark(f(X1,X2,X3)) =  [1] X3 + [0]        
                            >= [1] X3 + [5]        
                            =  a__f(X1,X2,mark(X3))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            a__f(a(),b(),X) -> a__f(X,X,mark(X))
            mark(a()) -> a()
            mark(b()) -> b()
            mark(c()) -> a__c()
            mark(f(X1,X2,X3)) -> a__f(X1,X2,mark(X3))
        - Weak TRS:
            a__c() -> a()
            a__c() -> b()
            a__c() -> c()
            a__f(X1,X2,X3) -> f(X1,X2,X3)
        - Signature:
            {a__c/0,a__f/3,mark/1} / {a/0,b/0,c/0,f/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__c,a__f,mark} and constructors {a,b,c,f}
    + 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(a__f) = {3}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
               p(a) = [0]         
            p(a__c) = [0]         
            p(a__f) = [1] x3 + [6]
               p(b) = [0]         
               p(c) = [0]         
               p(f) = [0]         
            p(mark) = [1]         
          
          Following rules are strictly oriented:
          mark(a()) = [1]   
                    > [0]   
                    = a()   
          
          mark(b()) = [1]   
                    > [0]   
                    = b()   
          
          mark(c()) = [1]   
                    > [0]   
                    = a__c()
          
          
          Following rules are (at-least) weakly oriented:
                     a__c() =  [0]                 
                            >= [0]                 
                            =  a()                 
          
                     a__c() =  [0]                 
                            >= [0]                 
                            =  b()                 
          
                     a__c() =  [0]                 
                            >= [0]                 
                            =  c()                 
          
             a__f(X1,X2,X3) =  [1] X3 + [6]        
                            >= [0]                 
                            =  f(X1,X2,X3)         
          
            a__f(a(),b(),X) =  [1] X + [6]         
                            >= [7]                 
                            =  a__f(X,X,mark(X))   
          
          mark(f(X1,X2,X3)) =  [1]                 
                            >= [7]                 
                            =  a__f(X1,X2,mark(X3))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          a__f(a(),b(),X) -> a__f(X,X,mark(X))
          mark(f(X1,X2,X3)) -> a__f(X1,X2,mark(X3))
      - Weak TRS:
          a__c() -> a()
          a__c() -> b()
          a__c() -> c()
          a__f(X1,X2,X3) -> f(X1,X2,X3)
          mark(a()) -> a()
          mark(b()) -> b()
          mark(c()) -> a__c()
      - Signature:
          {a__c/0,a__f/3,mark/1} / {a/0,b/0,c/0,f/3}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {a__c,a__f,mark} and constructors {a,b,c,f}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE