MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            f(t,x) -> f'(t,g(x))
            f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
            f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
            f'(triple(a,b,c),C()) -> triple(a,b,s(c))
            f''(triple(a,b,c)) -> foldC(triple(a,b,0()),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())
            g(A()) -> A()
            g(B()) -> A()
            g(B()) -> B()
            g(C()) -> A()
            g(C()) -> B()
            g(C()) -> C()
        - Signature:
            {f/2,f'/2,f''/1,foldB/2,foldC/2,g/1} / {0/0,A/0,B/0,C/0,s/1,triple/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,f',f'',foldB,foldC,g} and constructors {0,A,B,C,s
            ,triple}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          f#(t,x) -> c_1(f'#(t,g(x)),g#(x))
          f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b))
          f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A()))
          f'#(triple(a,b,c),C()) -> c_4()
          f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c))
          foldB#(t,0()) -> c_6()
          foldB#(t,s(n)) -> c_7(f#(foldB(t,n),B()),foldB#(t,n))
          foldC#(t,0()) -> c_8()
          foldC#(t,s(n)) -> c_9(f#(foldC(t,n),C()),foldC#(t,n))
          g#(A()) -> c_10()
          g#(B()) -> c_11()
          g#(B()) -> c_12()
          g#(C()) -> c_13()
          g#(C()) -> c_14()
          g#(C()) -> c_15()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            f#(t,x) -> c_1(f'#(t,g(x)),g#(x))
            f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b))
            f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A()))
            f'#(triple(a,b,c),C()) -> c_4()
            f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c))
            foldB#(t,0()) -> c_6()
            foldB#(t,s(n)) -> c_7(f#(foldB(t,n),B()),foldB#(t,n))
            foldC#(t,0()) -> c_8()
            foldC#(t,s(n)) -> c_9(f#(foldC(t,n),C()),foldC#(t,n))
            g#(A()) -> c_10()
            g#(B()) -> c_11()
            g#(B()) -> c_12()
            g#(C()) -> c_13()
            g#(C()) -> c_14()
            g#(C()) -> c_15()
        - Weak TRS:
            f(t,x) -> f'(t,g(x))
            f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
            f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
            f'(triple(a,b,c),C()) -> triple(a,b,s(c))
            f''(triple(a,b,c)) -> foldC(triple(a,b,0()),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())
            g(A()) -> A()
            g(B()) -> A()
            g(B()) -> B()
            g(C()) -> A()
            g(C()) -> B()
            g(C()) -> C()
        - Signature:
            {f/2,f'/2,f''/1,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0,C/0,s/1
            ,triple/3,c_1/2,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,foldB#,foldC#,g#} and constructors {0,A,B,C,s
            ,triple}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {4,6,8,10,11,12,13,14,15}
        by application of
          Pre({4,6,8,10,11,12,13,14,15}) = {1,2,5,7,9}.
        Here rules are labelled as follows:
          1: f#(t,x) -> c_1(f'#(t,g(x)),g#(x))
          2: f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b))
          3: f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A()))
          4: f'#(triple(a,b,c),C()) -> c_4()
          5: f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c))
          6: foldB#(t,0()) -> c_6()
          7: foldB#(t,s(n)) -> c_7(f#(foldB(t,n),B()),foldB#(t,n))
          8: foldC#(t,0()) -> c_8()
          9: foldC#(t,s(n)) -> c_9(f#(foldC(t,n),C()),foldC#(t,n))
          10: g#(A()) -> c_10()
          11: g#(B()) -> c_11()
          12: g#(B()) -> c_12()
          13: g#(C()) -> c_13()
          14: g#(C()) -> c_14()
          15: g#(C()) -> c_15()
* Step 3: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            f#(t,x) -> c_1(f'#(t,g(x)),g#(x))
            f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b))
            f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A()))
            f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c))
            foldB#(t,s(n)) -> c_7(f#(foldB(t,n),B()),foldB#(t,n))
            foldC#(t,s(n)) -> c_9(f#(foldC(t,n),C()),foldC#(t,n))
        - Weak DPs:
            f'#(triple(a,b,c),C()) -> c_4()
            foldB#(t,0()) -> c_6()
            foldC#(t,0()) -> c_8()
            g#(A()) -> c_10()
            g#(B()) -> c_11()
            g#(B()) -> c_12()
            g#(C()) -> c_13()
            g#(C()) -> c_14()
            g#(C()) -> c_15()
        - Weak TRS:
            f(t,x) -> f'(t,g(x))
            f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
            f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
            f'(triple(a,b,c),C()) -> triple(a,b,s(c))
            f''(triple(a,b,c)) -> foldC(triple(a,b,0()),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())
            g(A()) -> A()
            g(B()) -> A()
            g(B()) -> B()
            g(C()) -> A()
            g(C()) -> B()
            g(C()) -> C()
        - Signature:
            {f/2,f'/2,f''/1,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0,C/0,s/1
            ,triple/3,c_1/2,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,foldB#,foldC#,g#} and constructors {0,A,B,C,s
            ,triple}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:f#(t,x) -> c_1(f'#(t,g(x)),g#(x))
             -->_1 f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())):3
             -->_1 f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)):2
             -->_2 g#(C()) -> c_15():15
             -->_2 g#(C()) -> c_14():14
             -->_2 g#(C()) -> c_13():13
             -->_2 g#(B()) -> c_12():12
             -->_2 g#(B()) -> c_11():11
             -->_2 g#(A()) -> c_10():10
             -->_1 f'#(triple(a,b,c),C()) -> c_4():7
          
          2:S:f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b))
             -->_2 foldB#(t,s(n)) -> c_7(f#(foldB(t,n),B()),foldB#(t,n)):5
             -->_1 f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)):4
             -->_2 foldB#(t,0()) -> c_6():8
          
          3:S:f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A()))
             -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1
          
          4:S:f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c))
             -->_1 foldC#(t,s(n)) -> c_9(f#(foldC(t,n),C()),foldC#(t,n)):6
             -->_1 foldC#(t,0()) -> c_8():9
          
          5:S:foldB#(t,s(n)) -> c_7(f#(foldB(t,n),B()),foldB#(t,n))
             -->_2 foldB#(t,0()) -> c_6():8
             -->_2 foldB#(t,s(n)) -> c_7(f#(foldB(t,n),B()),foldB#(t,n)):5
             -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1
          
          6:S:foldC#(t,s(n)) -> c_9(f#(foldC(t,n),C()),foldC#(t,n))
             -->_2 foldC#(t,0()) -> c_8():9
             -->_2 foldC#(t,s(n)) -> c_9(f#(foldC(t,n),C()),foldC#(t,n)):6
             -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1
          
          7:W:f'#(triple(a,b,c),C()) -> c_4()
             
          
          8:W:foldB#(t,0()) -> c_6()
             
          
          9:W:foldC#(t,0()) -> c_8()
             
          
          10:W:g#(A()) -> c_10()
             
          
          11:W:g#(B()) -> c_11()
             
          
          12:W:g#(B()) -> c_12()
             
          
          13:W:g#(C()) -> c_13()
             
          
          14:W:g#(C()) -> c_14()
             
          
          15:W:g#(C()) -> c_15()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          7: f'#(triple(a,b,c),C()) -> c_4()
          10: g#(A()) -> c_10()
          11: g#(B()) -> c_11()
          12: g#(B()) -> c_12()
          13: g#(C()) -> c_13()
          14: g#(C()) -> c_14()
          15: g#(C()) -> c_15()
          9: foldC#(t,0()) -> c_8()
          8: foldB#(t,0()) -> c_6()
* Step 4: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            f#(t,x) -> c_1(f'#(t,g(x)),g#(x))
            f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b))
            f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A()))
            f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c))
            foldB#(t,s(n)) -> c_7(f#(foldB(t,n),B()),foldB#(t,n))
            foldC#(t,s(n)) -> c_9(f#(foldC(t,n),C()),foldC#(t,n))
        - Weak TRS:
            f(t,x) -> f'(t,g(x))
            f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
            f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
            f'(triple(a,b,c),C()) -> triple(a,b,s(c))
            f''(triple(a,b,c)) -> foldC(triple(a,b,0()),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())
            g(A()) -> A()
            g(B()) -> A()
            g(B()) -> B()
            g(C()) -> A()
            g(C()) -> B()
            g(C()) -> C()
        - Signature:
            {f/2,f'/2,f''/1,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0,C/0,s/1
            ,triple/3,c_1/2,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,foldB#,foldC#,g#} and constructors {0,A,B,C,s
            ,triple}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:f#(t,x) -> c_1(f'#(t,g(x)),g#(x))
             -->_1 f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())):3
             -->_1 f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)):2
          
          2:S:f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b))
             -->_2 foldB#(t,s(n)) -> c_7(f#(foldB(t,n),B()),foldB#(t,n)):5
             -->_1 f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)):4
          
          3:S:f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A()))
             -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1
          
          4:S:f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c))
             -->_1 foldC#(t,s(n)) -> c_9(f#(foldC(t,n),C()),foldC#(t,n)):6
          
          5:S:foldB#(t,s(n)) -> c_7(f#(foldB(t,n),B()),foldB#(t,n))
             -->_2 foldB#(t,s(n)) -> c_7(f#(foldB(t,n),B()),foldB#(t,n)):5
             -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1
          
          6:S:foldC#(t,s(n)) -> c_9(f#(foldC(t,n),C()),foldC#(t,n))
             -->_2 foldC#(t,s(n)) -> c_9(f#(foldC(t,n),C()),foldC#(t,n)):6
             -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          f#(t,x) -> c_1(f'#(t,g(x)))
* Step 5: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          f#(t,x) -> c_1(f'#(t,g(x)))
          f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b))
          f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A()))
          f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c))
          foldB#(t,s(n)) -> c_7(f#(foldB(t,n),B()),foldB#(t,n))
          foldC#(t,s(n)) -> c_9(f#(foldC(t,n),C()),foldC#(t,n))
      - Weak TRS:
          f(t,x) -> f'(t,g(x))
          f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b))
          f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
          f'(triple(a,b,c),C()) -> triple(a,b,s(c))
          f''(triple(a,b,c)) -> foldC(triple(a,b,0()),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())
          g(A()) -> A()
          g(B()) -> A()
          g(B()) -> B()
          g(C()) -> A()
          g(C()) -> B()
          g(C()) -> C()
      - Signature:
          {f/2,f'/2,f''/1,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0,C/0,s/1
          ,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,foldB#,foldC#,g#} and constructors {0,A,B,C,s
          ,triple}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE