MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            a(1(),id()) -> 1()
            a(1(),p(x,y)) -> x
            a(a(x,y),z) -> a(x,a(y,z))
            a(id(),x) -> x
            a(lambda(x),y) -> lambda(a(x,p(1(),a(y,t()))))
            a(p(x,y),z) -> p(a(x,z),a(y,z))
            a(t(),id()) -> t()
            a(t(),p(x,y)) -> y
        - Signature:
            {a/2} / {1/0,id/0,lambda/1,p/2,t/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a} and constructors {1,id,lambda,p,t}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          a#(1(),id()) -> c_1()
          a#(1(),p(x,y)) -> c_2()
          a#(a(x,y),z) -> c_3(a#(x,a(y,z)),a#(y,z))
          a#(id(),x) -> c_4()
          a#(lambda(x),y) -> c_5(a#(x,p(1(),a(y,t()))),a#(y,t()))
          a#(p(x,y),z) -> c_6(a#(x,z),a#(y,z))
          a#(t(),id()) -> c_7()
          a#(t(),p(x,y)) -> c_8()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            a#(1(),id()) -> c_1()
            a#(1(),p(x,y)) -> c_2()
            a#(a(x,y),z) -> c_3(a#(x,a(y,z)),a#(y,z))
            a#(id(),x) -> c_4()
            a#(lambda(x),y) -> c_5(a#(x,p(1(),a(y,t()))),a#(y,t()))
            a#(p(x,y),z) -> c_6(a#(x,z),a#(y,z))
            a#(t(),id()) -> c_7()
            a#(t(),p(x,y)) -> c_8()
        - Weak TRS:
            a(1(),id()) -> 1()
            a(1(),p(x,y)) -> x
            a(a(x,y),z) -> a(x,a(y,z))
            a(id(),x) -> x
            a(lambda(x),y) -> lambda(a(x,p(1(),a(y,t()))))
            a(p(x,y),z) -> p(a(x,z),a(y,z))
            a(t(),id()) -> t()
            a(t(),p(x,y)) -> y
        - Signature:
            {a/2,a#/2} / {1/0,id/0,lambda/1,p/2,t/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/2,c_6/2,c_7/0,c_8/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#} and constructors {1,id,lambda,p,t}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,2,4,7,8}
        by application of
          Pre({1,2,4,7,8}) = {3,5,6}.
        Here rules are labelled as follows:
          1: a#(1(),id()) -> c_1()
          2: a#(1(),p(x,y)) -> c_2()
          3: a#(a(x,y),z) -> c_3(a#(x,a(y,z)),a#(y,z))
          4: a#(id(),x) -> c_4()
          5: a#(lambda(x),y) -> c_5(a#(x,p(1(),a(y,t()))),a#(y,t()))
          6: a#(p(x,y),z) -> c_6(a#(x,z),a#(y,z))
          7: a#(t(),id()) -> c_7()
          8: a#(t(),p(x,y)) -> c_8()
* Step 3: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            a#(a(x,y),z) -> c_3(a#(x,a(y,z)),a#(y,z))
            a#(lambda(x),y) -> c_5(a#(x,p(1(),a(y,t()))),a#(y,t()))
            a#(p(x,y),z) -> c_6(a#(x,z),a#(y,z))
        - Weak DPs:
            a#(1(),id()) -> c_1()
            a#(1(),p(x,y)) -> c_2()
            a#(id(),x) -> c_4()
            a#(t(),id()) -> c_7()
            a#(t(),p(x,y)) -> c_8()
        - Weak TRS:
            a(1(),id()) -> 1()
            a(1(),p(x,y)) -> x
            a(a(x,y),z) -> a(x,a(y,z))
            a(id(),x) -> x
            a(lambda(x),y) -> lambda(a(x,p(1(),a(y,t()))))
            a(p(x,y),z) -> p(a(x,z),a(y,z))
            a(t(),id()) -> t()
            a(t(),p(x,y)) -> y
        - Signature:
            {a/2,a#/2} / {1/0,id/0,lambda/1,p/2,t/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/2,c_6/2,c_7/0,c_8/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#} and constructors {1,id,lambda,p,t}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:a#(a(x,y),z) -> c_3(a#(x,a(y,z)),a#(y,z))
             -->_2 a#(p(x,y),z) -> c_6(a#(x,z),a#(y,z)):3
             -->_1 a#(p(x,y),z) -> c_6(a#(x,z),a#(y,z)):3
             -->_2 a#(lambda(x),y) -> c_5(a#(x,p(1(),a(y,t()))),a#(y,t())):2
             -->_1 a#(lambda(x),y) -> c_5(a#(x,p(1(),a(y,t()))),a#(y,t())):2
             -->_2 a#(t(),p(x,y)) -> c_8():8
             -->_1 a#(t(),p(x,y)) -> c_8():8
             -->_2 a#(t(),id()) -> c_7():7
             -->_1 a#(t(),id()) -> c_7():7
             -->_2 a#(id(),x) -> c_4():6
             -->_1 a#(id(),x) -> c_4():6
             -->_2 a#(1(),p(x,y)) -> c_2():5
             -->_1 a#(1(),p(x,y)) -> c_2():5
             -->_2 a#(1(),id()) -> c_1():4
             -->_1 a#(1(),id()) -> c_1():4
             -->_2 a#(a(x,y),z) -> c_3(a#(x,a(y,z)),a#(y,z)):1
             -->_1 a#(a(x,y),z) -> c_3(a#(x,a(y,z)),a#(y,z)):1
          
          2:S:a#(lambda(x),y) -> c_5(a#(x,p(1(),a(y,t()))),a#(y,t()))
             -->_2 a#(p(x,y),z) -> c_6(a#(x,z),a#(y,z)):3
             -->_1 a#(p(x,y),z) -> c_6(a#(x,z),a#(y,z)):3
             -->_1 a#(t(),p(x,y)) -> c_8():8
             -->_2 a#(id(),x) -> c_4():6
             -->_1 a#(id(),x) -> c_4():6
             -->_1 a#(1(),p(x,y)) -> c_2():5
             -->_2 a#(lambda(x),y) -> c_5(a#(x,p(1(),a(y,t()))),a#(y,t())):2
             -->_1 a#(lambda(x),y) -> c_5(a#(x,p(1(),a(y,t()))),a#(y,t())):2
             -->_2 a#(a(x,y),z) -> c_3(a#(x,a(y,z)),a#(y,z)):1
             -->_1 a#(a(x,y),z) -> c_3(a#(x,a(y,z)),a#(y,z)):1
          
          3:S:a#(p(x,y),z) -> c_6(a#(x,z),a#(y,z))
             -->_2 a#(t(),p(x,y)) -> c_8():8
             -->_1 a#(t(),p(x,y)) -> c_8():8
             -->_2 a#(t(),id()) -> c_7():7
             -->_1 a#(t(),id()) -> c_7():7
             -->_2 a#(id(),x) -> c_4():6
             -->_1 a#(id(),x) -> c_4():6
             -->_2 a#(1(),p(x,y)) -> c_2():5
             -->_1 a#(1(),p(x,y)) -> c_2():5
             -->_2 a#(1(),id()) -> c_1():4
             -->_1 a#(1(),id()) -> c_1():4
             -->_2 a#(p(x,y),z) -> c_6(a#(x,z),a#(y,z)):3
             -->_1 a#(p(x,y),z) -> c_6(a#(x,z),a#(y,z)):3
             -->_2 a#(lambda(x),y) -> c_5(a#(x,p(1(),a(y,t()))),a#(y,t())):2
             -->_1 a#(lambda(x),y) -> c_5(a#(x,p(1(),a(y,t()))),a#(y,t())):2
             -->_2 a#(a(x,y),z) -> c_3(a#(x,a(y,z)),a#(y,z)):1
             -->_1 a#(a(x,y),z) -> c_3(a#(x,a(y,z)),a#(y,z)):1
          
          4:W:a#(1(),id()) -> c_1()
             
          
          5:W:a#(1(),p(x,y)) -> c_2()
             
          
          6:W:a#(id(),x) -> c_4()
             
          
          7:W:a#(t(),id()) -> c_7()
             
          
          8:W:a#(t(),p(x,y)) -> c_8()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          4: a#(1(),id()) -> c_1()
          5: a#(1(),p(x,y)) -> c_2()
          6: a#(id(),x) -> c_4()
          7: a#(t(),id()) -> c_7()
          8: a#(t(),p(x,y)) -> c_8()
* Step 4: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          a#(a(x,y),z) -> c_3(a#(x,a(y,z)),a#(y,z))
          a#(lambda(x),y) -> c_5(a#(x,p(1(),a(y,t()))),a#(y,t()))
          a#(p(x,y),z) -> c_6(a#(x,z),a#(y,z))
      - Weak TRS:
          a(1(),id()) -> 1()
          a(1(),p(x,y)) -> x
          a(a(x,y),z) -> a(x,a(y,z))
          a(id(),x) -> x
          a(lambda(x),y) -> lambda(a(x,p(1(),a(y,t()))))
          a(p(x,y),z) -> p(a(x,z),a(y,z))
          a(t(),id()) -> t()
          a(t(),p(x,y)) -> y
      - Signature:
          {a/2,a#/2} / {1/0,id/0,lambda/1,p/2,t/0,c_1/0,c_2/0,c_3/2,c_4/0,c_5/2,c_6/2,c_7/0,c_8/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {a#} and constructors {1,id,lambda,p,t}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE