MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { __(X1, X2) -> n____(X1, X2)
  , __(X, nil()) -> X
  , __(__(X, Y), Z) -> __(X, __(Y, Z))
  , __(nil(), X) -> X
  , nil() -> n__nil()
  , U11(tt(), V) -> U12(isNeList(activate(V)))
  , U12(tt()) -> tt()
  , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V))
  , isNeList(n____(V1, V2)) ->
    U41(and(isPalListKind(activate(V1)),
            n__isPalListKind(activate(V2))),
        activate(V1),
        activate(V2))
  , isNeList(n____(V1, V2)) ->
    U51(and(isPalListKind(activate(V1)),
            n__isPalListKind(activate(V2))),
        activate(V1),
        activate(V2))
  , activate(X) -> X
  , activate(n__nil()) -> nil()
  , activate(n____(X1, X2)) -> __(activate(X1), activate(X2))
  , activate(n__isPalListKind(X)) -> isPalListKind(X)
  , activate(n__and(X1, X2)) -> and(activate(X1), X2)
  , activate(n__isPal(X)) -> isPal(X)
  , activate(n__a()) -> a()
  , activate(n__e()) -> e()
  , activate(n__i()) -> i()
  , activate(n__o()) -> o()
  , activate(n__u()) -> u()
  , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2))
  , U22(tt(), V2) -> U23(isList(activate(V2)))
  , isList(V) -> U11(isPalListKind(activate(V)), activate(V))
  , isList(n__nil()) -> tt()
  , isList(n____(V1, V2)) ->
    U21(and(isPalListKind(activate(V1)),
            n__isPalListKind(activate(V2))),
        activate(V1),
        activate(V2))
  , U23(tt()) -> tt()
  , U31(tt(), V) -> U32(isQid(activate(V)))
  , U32(tt()) -> tt()
  , isQid(n__a()) -> tt()
  , isQid(n__e()) -> tt()
  , isQid(n__i()) -> tt()
  , isQid(n__o()) -> tt()
  , isQid(n__u()) -> tt()
  , U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2))
  , U42(tt(), V2) -> U43(isNeList(activate(V2)))
  , U43(tt()) -> tt()
  , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2))
  , U52(tt(), V2) -> U53(isList(activate(V2)))
  , U53(tt()) -> tt()
  , U61(tt(), V) -> U62(isQid(activate(V)))
  , U62(tt()) -> tt()
  , U71(tt(), V) -> U72(isNePal(activate(V)))
  , U72(tt()) -> tt()
  , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V))
  , isNePal(n____(I, n____(P, I))) ->
    and(and(isQid(activate(I)), n__isPalListKind(activate(I))),
        n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))
  , and(X1, X2) -> n__and(X1, X2)
  , and(tt(), X) -> activate(X)
  , isPalListKind(X) -> n__isPalListKind(X)
  , isPalListKind(n__nil()) -> tt()
  , isPalListKind(n____(V1, V2)) ->
    and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))
  , isPalListKind(n__a()) -> tt()
  , isPalListKind(n__e()) -> tt()
  , isPalListKind(n__i()) -> tt()
  , isPalListKind(n__o()) -> tt()
  , isPalListKind(n__u()) -> tt()
  , isPal(V) -> U71(isPalListKind(activate(V)), activate(V))
  , isPal(X) -> n__isPal(X)
  , isPal(n__nil()) -> tt()
  , a() -> n__a()
  , e() -> n__e()
  , i() -> n__i()
  , o() -> n__o()
  , u() -> n__u() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Arguments of following rules are not normal-forms:

{ __(X, nil()) -> X
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, __(nil(), X) -> X }

All above mentioned rules can be savely removed.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { __(X1, X2) -> n____(X1, X2)
  , nil() -> n__nil()
  , U11(tt(), V) -> U12(isNeList(activate(V)))
  , U12(tt()) -> tt()
  , isNeList(V) -> U31(isPalListKind(activate(V)), activate(V))
  , isNeList(n____(V1, V2)) ->
    U41(and(isPalListKind(activate(V1)),
            n__isPalListKind(activate(V2))),
        activate(V1),
        activate(V2))
  , isNeList(n____(V1, V2)) ->
    U51(and(isPalListKind(activate(V1)),
            n__isPalListKind(activate(V2))),
        activate(V1),
        activate(V2))
  , activate(X) -> X
  , activate(n__nil()) -> nil()
  , activate(n____(X1, X2)) -> __(activate(X1), activate(X2))
  , activate(n__isPalListKind(X)) -> isPalListKind(X)
  , activate(n__and(X1, X2)) -> and(activate(X1), X2)
  , activate(n__isPal(X)) -> isPal(X)
  , activate(n__a()) -> a()
  , activate(n__e()) -> e()
  , activate(n__i()) -> i()
  , activate(n__o()) -> o()
  , activate(n__u()) -> u()
  , U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2))
  , U22(tt(), V2) -> U23(isList(activate(V2)))
  , isList(V) -> U11(isPalListKind(activate(V)), activate(V))
  , isList(n__nil()) -> tt()
  , isList(n____(V1, V2)) ->
    U21(and(isPalListKind(activate(V1)),
            n__isPalListKind(activate(V2))),
        activate(V1),
        activate(V2))
  , U23(tt()) -> tt()
  , U31(tt(), V) -> U32(isQid(activate(V)))
  , U32(tt()) -> tt()
  , isQid(n__a()) -> tt()
  , isQid(n__e()) -> tt()
  , isQid(n__i()) -> tt()
  , isQid(n__o()) -> tt()
  , isQid(n__u()) -> tt()
  , U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2))
  , U42(tt(), V2) -> U43(isNeList(activate(V2)))
  , U43(tt()) -> tt()
  , U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2))
  , U52(tt(), V2) -> U53(isList(activate(V2)))
  , U53(tt()) -> tt()
  , U61(tt(), V) -> U62(isQid(activate(V)))
  , U62(tt()) -> tt()
  , U71(tt(), V) -> U72(isNePal(activate(V)))
  , U72(tt()) -> tt()
  , isNePal(V) -> U61(isPalListKind(activate(V)), activate(V))
  , isNePal(n____(I, n____(P, I))) ->
    and(and(isQid(activate(I)), n__isPalListKind(activate(I))),
        n__and(n__isPal(activate(P)), n__isPalListKind(activate(P))))
  , and(X1, X2) -> n__and(X1, X2)
  , and(tt(), X) -> activate(X)
  , isPalListKind(X) -> n__isPalListKind(X)
  , isPalListKind(n__nil()) -> tt()
  , isPalListKind(n____(V1, V2)) ->
    and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))
  , isPalListKind(n__a()) -> tt()
  , isPalListKind(n__e()) -> tt()
  , isPalListKind(n__i()) -> tt()
  , isPalListKind(n__o()) -> tt()
  , isPalListKind(n__u()) -> tt()
  , isPal(V) -> U71(isPalListKind(activate(V)), activate(V))
  , isPal(X) -> n__isPal(X)
  , isPal(n__nil()) -> tt()
  , a() -> n__a()
  , e() -> n__e()
  , i() -> n__i()
  , o() -> n__o()
  , u() -> n__u() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.

2) 'Best' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'WithProblem (timeout of 60 seconds)' failed due to the
      following reason:
      
      Computation stopped due to timeout after 60.0 seconds.
   
   2) 'Best' failed due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
         failed due to the following reason:
         
         Computation stopped due to timeout after 30.0 seconds.
      
      2) 'Best' failed due to the following reason:
         
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
         1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
            following reason:
            
            The input cannot be shown compatible
         
         2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
            to the following reason:
            
            The input cannot be shown compatible
         
      
      3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
         due to the following reason:
         
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
         1) 'Bounds with minimal-enrichment and initial automaton 'match''
            failed due to the following reason:
            
            match-boundness of the problem could not be verified.
         
         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
            failed due to the following reason:
            
            match-boundness of the problem could not be verified.
         
      
   


Arrrr..