MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            f(t,x) -> f'(t,g(x))
            f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
            f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
            f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c))
            f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c)
            foldf(x,cons(y,z)) -> f(foldf(x,z),y)
            foldf(x,nil()) -> x
            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,foldf/2,g/1} / {A/0,B/0,C/0,cons/2,nil/0,triple/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,f',f'',foldf,g} and constructors {A,B,C,cons,nil
            ,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''#(foldf(triple(cons(A(),a),nil(),c),b))
                                       ,foldf#(triple(cons(A(),a),nil(),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(foldf#(triple(a,b,nil()),c))
          foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z))
          foldf#(x,nil()) -> c_7()
          g#(A()) -> c_8()
          g#(B()) -> c_9()
          g#(B()) -> c_10()
          g#(C()) -> c_11()
          g#(C()) -> c_12()
          g#(C()) -> c_13()
        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''#(foldf(triple(cons(A(),a),nil(),c),b))
                                         ,foldf#(triple(cons(A(),a),nil(),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(foldf#(triple(a,b,nil()),c))
            foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z))
            foldf#(x,nil()) -> c_7()
            g#(A()) -> c_8()
            g#(B()) -> c_9()
            g#(B()) -> c_10()
            g#(C()) -> c_11()
            g#(C()) -> c_12()
            g#(C()) -> c_13()
        - Weak TRS:
            f(t,x) -> f'(t,g(x))
            f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
            f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
            f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c))
            f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c)
            foldf(x,cons(y,z)) -> f(foldf(x,z),y)
            foldf(x,nil()) -> x
            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,foldf/2,g/1,f#/2,f'#/2,f''#/1,foldf#/2,g#/1} / {A/0,B/0,C/0,cons/2,nil/0,triple/3,c_1/2
            ,c_2/2,c_3/1,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,foldf#,g#} and constructors {A,B,C,cons,nil
            ,triple}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {4,7,8,9,10,11,12,13}
        by application of
          Pre({4,7,8,9,10,11,12,13}) = {1,2,5,6}.
        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''#(foldf(triple(cons(A(),a),nil(),c),b))
                                          ,foldf#(triple(cons(A(),a),nil(),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(foldf#(triple(a,b,nil()),c))
          6: foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z))
          7: foldf#(x,nil()) -> c_7()
          8: g#(A()) -> c_8()
          9: g#(B()) -> c_9()
          10: g#(B()) -> c_10()
          11: g#(C()) -> c_11()
          12: g#(C()) -> c_12()
          13: g#(C()) -> c_13()
* 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''#(foldf(triple(cons(A(),a),nil(),c),b))
                                         ,foldf#(triple(cons(A(),a),nil(),c),b))
            f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A()))
            f''#(triple(a,b,c)) -> c_5(foldf#(triple(a,b,nil()),c))
            foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z))
        - Weak DPs:
            f'#(triple(a,b,c),C()) -> c_4()
            foldf#(x,nil()) -> c_7()
            g#(A()) -> c_8()
            g#(B()) -> c_9()
            g#(B()) -> c_10()
            g#(C()) -> c_11()
            g#(C()) -> c_12()
            g#(C()) -> c_13()
        - Weak TRS:
            f(t,x) -> f'(t,g(x))
            f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
            f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
            f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c))
            f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c)
            foldf(x,cons(y,z)) -> f(foldf(x,z),y)
            foldf(x,nil()) -> x
            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,foldf/2,g/1,f#/2,f'#/2,f''#/1,foldf#/2,g#/1} / {A/0,B/0,C/0,cons/2,nil/0,triple/3,c_1/2
            ,c_2/2,c_3/1,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,foldf#,g#} and constructors {A,B,C,cons,nil
            ,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''#(foldf(triple(cons(A(),a),nil(),c),b))
                                                ,foldf#(triple(cons(A(),a),nil(),c),b)):2
             -->_2 g#(C()) -> c_13():13
             -->_2 g#(C()) -> c_12():12
             -->_2 g#(C()) -> c_11():11
             -->_2 g#(B()) -> c_10():10
             -->_2 g#(B()) -> c_9():9
             -->_2 g#(A()) -> c_8():8
             -->_1 f'#(triple(a,b,c),C()) -> c_4():6
          
          2:S:f'#(triple(a,b,c),A()) -> c_2(f''#(foldf(triple(cons(A(),a),nil(),c),b))
                                           ,foldf#(triple(cons(A(),a),nil(),c),b))
             -->_2 foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z)):5
             -->_1 f''#(triple(a,b,c)) -> c_5(foldf#(triple(a,b,nil()),c)):4
             -->_2 foldf#(x,nil()) -> c_7():7
          
          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(foldf#(triple(a,b,nil()),c))
             -->_1 foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z)):5
             -->_1 foldf#(x,nil()) -> c_7():7
          
          5:S:foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z))
             -->_2 foldf#(x,nil()) -> c_7():7
             -->_2 foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z)):5
             -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1
          
          6:W:f'#(triple(a,b,c),C()) -> c_4()
             
          
          7:W:foldf#(x,nil()) -> c_7()
             
          
          8:W:g#(A()) -> c_8()
             
          
          9:W:g#(B()) -> c_9()
             
          
          10:W:g#(B()) -> c_10()
             
          
          11:W:g#(C()) -> c_11()
             
          
          12:W:g#(C()) -> c_12()
             
          
          13:W:g#(C()) -> c_13()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          6: f'#(triple(a,b,c),C()) -> c_4()
          8: g#(A()) -> c_8()
          9: g#(B()) -> c_9()
          10: g#(B()) -> c_10()
          11: g#(C()) -> c_11()
          12: g#(C()) -> c_12()
          13: g#(C()) -> c_13()
          7: foldf#(x,nil()) -> c_7()
* 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''#(foldf(triple(cons(A(),a),nil(),c),b))
                                         ,foldf#(triple(cons(A(),a),nil(),c),b))
            f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A()))
            f''#(triple(a,b,c)) -> c_5(foldf#(triple(a,b,nil()),c))
            foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z))
        - Weak TRS:
            f(t,x) -> f'(t,g(x))
            f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
            f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
            f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c))
            f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c)
            foldf(x,cons(y,z)) -> f(foldf(x,z),y)
            foldf(x,nil()) -> x
            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,foldf/2,g/1,f#/2,f'#/2,f''#/1,foldf#/2,g#/1} / {A/0,B/0,C/0,cons/2,nil/0,triple/3,c_1/2
            ,c_2/2,c_3/1,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,foldf#,g#} and constructors {A,B,C,cons,nil
            ,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''#(foldf(triple(cons(A(),a),nil(),c),b))
                                                ,foldf#(triple(cons(A(),a),nil(),c),b)):2
          
          2:S:f'#(triple(a,b,c),A()) -> c_2(f''#(foldf(triple(cons(A(),a),nil(),c),b))
                                           ,foldf#(triple(cons(A(),a),nil(),c),b))
             -->_2 foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z)):5
             -->_1 f''#(triple(a,b,c)) -> c_5(foldf#(triple(a,b,nil()),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(foldf#(triple(a,b,nil()),c))
             -->_1 foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z)):5
          
          5:S:foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z))
             -->_2 foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z)):5
             -->_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''#(foldf(triple(cons(A(),a),nil(),c),b))
                                       ,foldf#(triple(cons(A(),a),nil(),c),b))
          f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A()))
          f''#(triple(a,b,c)) -> c_5(foldf#(triple(a,b,nil()),c))
          foldf#(x,cons(y,z)) -> c_6(f#(foldf(x,z),y),foldf#(x,z))
      - Weak TRS:
          f(t,x) -> f'(t,g(x))
          f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
          f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
          f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c))
          f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c)
          foldf(x,cons(y,z)) -> f(foldf(x,z),y)
          foldf(x,nil()) -> x
          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,foldf/2,g/1,f#/2,f'#/2,f''#/1,foldf#/2,g#/1} / {A/0,B/0,C/0,cons/2,nil/0,triple/3,c_1/1
          ,c_2/2,c_3/1,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,foldf#,g#} and constructors {A,B,C,cons,nil
          ,triple}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE