Problem Strategy outermost added 08 PALINDROME nokinds-noand L

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 PALINDROME nokinds-noand L

stdout:

MAYBE

Problem:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil()) -> X
__(nil(),X) -> X
U11(tt()) -> tt()
U21(tt()) -> U22(isList())
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt()) -> U42(isNeList())
U42(tt()) -> tt()
U51(tt()) -> U52(isList())
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt()) -> U72(isPal())
U72(tt()) -> tt()
U81(tt()) -> tt()
isList() -> U11(isNeList())
isList() -> tt()
isList() -> U21(isList())
isNeList() -> U31(isQid())
isNeList() -> U41(isList())
isNeList() -> U51(isNeList())
isNePal() -> U61(isQid())
isNePal() -> U71(isQid())
isPal() -> U81(isNePal())
isPal() -> tt()
isQid() -> tt()

Proof:
Complexity Transformation Processor:
  strict:
   __(__(X,Y),Z) -> __(X,__(Y,Z))
   __(X,nil()) -> X
   __(nil(),X) -> X
   U11(tt()) -> tt()
   U21(tt()) -> U22(isList())
   U22(tt()) -> tt()
   U31(tt()) -> tt()
   U41(tt()) -> U42(isNeList())
   U42(tt()) -> tt()
   U51(tt()) -> U52(isList())
   U52(tt()) -> tt()
   U61(tt()) -> tt()
   U71(tt()) -> U72(isPal())
   U72(tt()) -> tt()
   U81(tt()) -> tt()
   isList() -> U11(isNeList())
   isList() -> tt()
   isList() -> U21(isList())
   isNeList() -> U31(isQid())
   isNeList() -> U41(isList())
   isNeList() -> U51(isNeList())
   isNePal() -> U61(isQid())
   isNePal() -> U71(isQid())
   isPal() -> U81(isNePal())
   isPal() -> tt()
   isQid() -> tt()
  weak:

  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [isNePal] = 0,

     [isQid] = 13,

     [U81](x0) = x0 + 4,

     [U72](x0) = x0 + 8,

     [isPal] = 0,

     [U71](x0) = x0,

     [U61](x0) = x0 + 6,

     [U52](x0) = x0 + 15,

     [U51](x0) = x0,

     [U42](x0) = x0 + 7,

     [isNeList] = 9,

     [U41](x0) = x0 + 7,

     [U31](x0) = x0 + 3,

     [U22](x0) = x0 + 9,

     [isList] = 1,

     [U21](x0) = x0,

     [U11](x0) = x0 + 7,

     [tt] = 8,

     [nil] = 2,

     [__](x0, x1) = x0 + x1 + 12
    orientation:
     __(__(X,Y),Z) = X + Y + Z + 24 >= X + Y + Z + 24 = __(X,__(Y,Z))

     __(X,nil()) = X + 14 >= X = X

     __(nil(),X) = X + 14 >= X = X

     U11(tt()) = 15 >= 8 = tt()

     U21(tt()) = 8 >= 10 = U22(isList())

     U22(tt()) = 17 >= 8 = tt()

     U31(tt()) = 11 >= 8 = tt()

     U41(tt()) = 15 >= 16 = U42(isNeList())

     U42(tt()) = 15 >= 8 = tt()

     U51(tt()) = 8 >= 16 = U52(isList())

     U52(tt()) = 23 >= 8 = tt()

     U61(tt()) = 14 >= 8 = tt()

     U71(tt()) = 8 >= 8 = U72(isPal())

     U72(tt()) = 16 >= 8 = tt()

     U81(tt()) = 12 >= 8 = tt()

     isList() = 1 >= 16 = U11(isNeList())

     isList() = 1 >= 8 = tt()

     isList() = 1 >= 1 = U21(isList())

     isNeList() = 9 >= 16 = U31(isQid())

     isNeList() = 9 >= 8 = U41(isList())

     isNeList() = 9 >= 9 = U51(isNeList())

     isNePal() = 0 >= 19 = U61(isQid())

     isNePal() = 0 >= 13 = U71(isQid())

     isPal() = 0 >= 4 = U81(isNePal())

     isPal() = 0 >= 8 = tt()

     isQid() = 13 >= 8 = tt()
    problem:
     strict:
      __(__(X,Y),Z) -> __(X,__(Y,Z))
      U21(tt()) -> U22(isList())
      U41(tt()) -> U42(isNeList())
      U51(tt()) -> U52(isList())
      U71(tt()) -> U72(isPal())
      isList() -> U11(isNeList())
      isList() -> tt()
      isList() -> U21(isList())
      isNeList() -> U31(isQid())
      isNeList() -> U51(isNeList())
      isNePal() -> U61(isQid())
      isNePal() -> U71(isQid())
      isPal() -> U81(isNePal())
      isPal() -> tt()
     weak:
      __(X,nil()) -> X
      __(nil(),X) -> X
      U11(tt()) -> tt()
      U22(tt()) -> tt()
      U31(tt()) -> tt()
      U42(tt()) -> tt()
      U52(tt()) -> tt()
      U61(tt()) -> tt()
      U72(tt()) -> tt()
      U81(tt()) -> tt()
      isNeList() -> U41(isList())
      isQid() -> tt()
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [isNePal] = 12,

       [isQid] = 0,

       [U81](x0) = x0,

       [U72](x0) = x0,

       [isPal] = 4,

       [U71](x0) = x0 + 12,

       [U61](x0) = x0,

       [U52](x0) = x0 + 15,

       [U51](x0) = x0,

       [U42](x0) = x0,

       [isNeList] = 8,

       [U41](x0) = x0 + 2,

       [U31](x0) = x0,

       [U22](x0) = x0,

       [isList] = 6,

       [U21](x0) = x0 + 12,

       [U11](x0) = x0 + 1,

       [tt] = 0,

       [nil] = 0,

       [__](x0, x1) = x0 + x1
      orientation:
       __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))

       U21(tt()) = 12 >= 6 = U22(isList())

       U41(tt()) = 2 >= 8 = U42(isNeList())

       U51(tt()) = 0 >= 21 = U52(isList())

       U71(tt()) = 12 >= 4 = U72(isPal())

       isList() = 6 >= 9 = U11(isNeList())

       isList() = 6 >= 0 = tt()

       isList() = 6 >= 18 = U21(isList())

       isNeList() = 8 >= 0 = U31(isQid())

       isNeList() = 8 >= 8 = U51(isNeList())

       isNePal() = 12 >= 0 = U61(isQid())

       isNePal() = 12 >= 12 = U71(isQid())

       isPal() = 4 >= 12 = U81(isNePal())

       isPal() = 4 >= 0 = tt()

       __(X,nil()) = X >= X = X

       __(nil(),X) = X >= X = X

       U11(tt()) = 1 >= 0 = tt()

       U22(tt()) = 0 >= 0 = tt()

       U31(tt()) = 0 >= 0 = tt()

       U42(tt()) = 0 >= 0 = tt()

       U52(tt()) = 15 >= 0 = tt()

       U61(tt()) = 0 >= 0 = tt()

       U72(tt()) = 0 >= 0 = tt()

       U81(tt()) = 0 >= 0 = tt()

       isNeList() = 8 >= 8 = U41(isList())

       isQid() = 0 >= 0 = tt()
      problem:
       strict:
        __(__(X,Y),Z) -> __(X,__(Y,Z))
        U41(tt()) -> U42(isNeList())
        U51(tt()) -> U52(isList())
        isList() -> U11(isNeList())
        isList() -> U21(isList())
        isNeList() -> U51(isNeList())
        isNePal() -> U71(isQid())
        isPal() -> U81(isNePal())
       weak:
        U21(tt()) -> U22(isList())
        U71(tt()) -> U72(isPal())
        isList() -> tt()
        isNeList() -> U31(isQid())
        isNePal() -> U61(isQid())
        isPal() -> tt()
        __(X,nil()) -> X
        __(nil(),X) -> X
        U11(tt()) -> tt()
        U22(tt()) -> tt()
        U31(tt()) -> tt()
        U42(tt()) -> tt()
        U52(tt()) -> tt()
        U61(tt()) -> tt()
        U72(tt()) -> tt()
        U81(tt()) -> tt()
        isNeList() -> U41(isList())
        isQid() -> tt()
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [isNePal] = 5,

         [isQid] = 0,

         [U81](x0) = x0 + 14,

         [U72](x0) = x0 + 1,

         [isPal] = 0,

         [U71](x0) = x0 + 1,

         [U61](x0) = x0 + 5,

         [U52](x0) = x0 + 2,

         [U51](x0) = x0 + 3,

         [U42](x0) = x0,

         [isNeList] = 13,

         [U41](x0) = x0 + 2,

         [U31](x0) = x0 + 13,

         [U22](x0) = x0,

         [isList] = 0,

         [U21](x0) = x0,

         [U11](x0) = x0 + 13,

         [tt] = 0,

         [nil] = 0,

         [__](x0, x1) = x0 + x1
        orientation:
         __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))

         U41(tt()) = 2 >= 13 = U42(isNeList())

         U51(tt()) = 3 >= 2 = U52(isList())

         isList() = 0 >= 26 = U11(isNeList())

         isList() = 0 >= 0 = U21(isList())

         isNeList() = 13 >= 16 = U51(isNeList())

         isNePal() = 5 >= 1 = U71(isQid())

         isPal() = 0 >= 19 = U81(isNePal())

         U21(tt()) = 0 >= 0 = U22(isList())

         U71(tt()) = 1 >= 1 = U72(isPal())

         isList() = 0 >= 0 = tt()

         isNeList() = 13 >= 13 = U31(isQid())

         isNePal() = 5 >= 5 = U61(isQid())

         isPal() = 0 >= 0 = tt()

         __(X,nil()) = X >= X = X

         __(nil(),X) = X >= X = X

         U11(tt()) = 13 >= 0 = tt()

         U22(tt()) = 0 >= 0 = tt()

         U31(tt()) = 13 >= 0 = tt()

         U42(tt()) = 0 >= 0 = tt()

         U52(tt()) = 2 >= 0 = tt()

         U61(tt()) = 5 >= 0 = tt()

         U72(tt()) = 1 >= 0 = tt()

         U81(tt()) = 14 >= 0 = tt()

         isNeList() = 13 >= 2 = U41(isList())

         isQid() = 0 >= 0 = tt()
        problem:
         strict:
          __(__(X,Y),Z) -> __(X,__(Y,Z))
          U41(tt()) -> U42(isNeList())
          isList() -> U11(isNeList())
          isList() -> U21(isList())
          isNeList() -> U51(isNeList())
          isPal() -> U81(isNePal())
         weak:
          U51(tt()) -> U52(isList())
          isNePal() -> U71(isQid())
          U21(tt()) -> U22(isList())
          U71(tt()) -> U72(isPal())
          isList() -> tt()
          isNeList() -> U31(isQid())
          isNePal() -> U61(isQid())
          isPal() -> tt()
          __(X,nil()) -> X
          __(nil(),X) -> X
          U11(tt()) -> tt()
          U22(tt()) -> tt()
          U31(tt()) -> tt()
          U42(tt()) -> tt()
          U52(tt()) -> tt()
          U61(tt()) -> tt()
          U72(tt()) -> tt()
          U81(tt()) -> tt()
          isNeList() -> U41(isList())
          isQid() -> tt()
        Bounds Processor:
         bound: 0
         enrichment: match
         automaton:
          final states: {20,19,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3}
          transitions:
           __0(1,2) -> 3*
           __0(2,1) -> 3*
           __0(1,1) -> 3*
           __0(2,2) -> 3*
           U410(5) -> 6*
           U410(2) -> 4*
           U410(1) -> 4*
           tt0() -> 4,11,9,8,6,10,20,19,18,17,16,15,14,13,12,7,5,1
           U420(2) -> 15*
           U420(6) -> 6,4
           U420(1) -> 15*
           isNeList0() -> 6*
           isList0() -> 5*
           U110(2) -> 12*
           U110(6) -> 5*
           U110(1) -> 12*
           U210(5) -> 5*
           U210(2) -> 10*
           U210(1) -> 10*
           U510(2) -> 8*
           U510(6) -> 6*
           U510(1) -> 8*
           isPal0() -> 7*
           U810(2) -> 19*
           U810(9) -> 7*
           U810(1) -> 19*
           isNePal0() -> 9*
           U520(5) -> 6,8
           U520(2) -> 16*
           U520(1) -> 16*
           U710(20) -> 9*
           U710(2) -> 11*
           U710(1) -> 11*
           isQid0() -> 20*
           U220(5) -> 5,10
           U220(2) -> 13*
           U220(1) -> 13*
           U720(7) -> 9,11
           U720(2) -> 18*
           U720(1) -> 18*
           U310(20) -> 6*
           U310(2) -> 14*
           U310(1) -> 14*
           U610(20) -> 9*
           U610(2) -> 17*
           U610(1) -> 17*
           nil0() -> 2*
           1 -> 3*
           2 -> 3*
         problem:
          strict:
           U41(tt()) -> U42(isNeList())
           isList() -> U11(isNeList())
           isList() -> U21(isList())
           isNeList() -> U51(isNeList())
           isPal() -> U81(isNePal())
          weak:
           __(__(X,Y),Z) -> __(X,__(Y,Z))
           U51(tt()) -> U52(isList())
           isNePal() -> U71(isQid())
           U21(tt()) -> U22(isList())
           U71(tt()) -> U72(isPal())
           isList() -> tt()
           isNeList() -> U31(isQid())
           isNePal() -> U61(isQid())
           isPal() -> tt()
           __(X,nil()) -> X
           __(nil(),X) -> X
           U11(tt()) -> tt()
           U22(tt()) -> tt()
           U31(tt()) -> tt()
           U42(tt()) -> tt()
           U52(tt()) -> tt()
           U61(tt()) -> tt()
           U72(tt()) -> tt()
           U81(tt()) -> tt()
           isNeList() -> U41(isList())
           isQid() -> tt()
         Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 PALINDROME nokinds-noand L

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Strategy outermost added 08 PALINDROME nokinds-noand L

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  __(__(X, Y), Z) -> __(X, __(Y, Z))
     , __(X, nil()) -> X
     , __(nil(), X) -> X
     , U11(tt()) -> tt()
     , U21(tt()) -> U22(isList())
     , U22(tt()) -> tt()
     , U31(tt()) -> tt()
     , U41(tt()) -> U42(isNeList())
     , U42(tt()) -> tt()
     , U51(tt()) -> U52(isList())
     , U52(tt()) -> tt()
     , U61(tt()) -> tt()
     , U71(tt()) -> U72(isPal())
     , U72(tt()) -> tt()
     , U81(tt()) -> tt()
     , isList() -> U11(isNeList())
     , isList() -> tt()
     , isList() -> U21(isList())
     , isNeList() -> U31(isQid())
     , isNeList() -> U41(isList())
     , isNeList() -> U51(isNeList())
     , isNePal() -> U61(isQid())
     , isNePal() -> U71(isQid())
     , isPal() -> U81(isNePal())
     , isPal() -> tt()
     , isQid() -> tt()}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Strategy outermost added 08 PALINDROME nokinds-noand L

stdout:

MAYBE
Warning when parsing problem:

Unsupported strategy 'OUTERMOST'

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Strategy outermost added 08 PALINDROME nokinds-noand L

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  __(__(X, Y), Z) -> __(X, __(Y, Z))
     , __(X, nil()) -> X
     , __(nil(), X) -> X
     , U11(tt()) -> tt()
     , U21(tt()) -> U22(isList())
     , U22(tt()) -> tt()
     , U31(tt()) -> tt()
     , U41(tt()) -> U42(isNeList())
     , U42(tt()) -> tt()
     , U51(tt()) -> U52(isList())
     , U52(tt()) -> tt()
     , U61(tt()) -> tt()
     , U71(tt()) -> U72(isPal())
     , U72(tt()) -> tt()
     , U81(tt()) -> tt()
     , isList() -> U11(isNeList())
     , isList() -> tt()
     , isList() -> U21(isList())
     , isNeList() -> U31(isQid())
     , isNeList() -> U41(isList())
     , isNeList() -> U51(isNeList())
     , isNePal() -> U61(isQid())
     , isNePal() -> U71(isQid())
     , isPal() -> U81(isNePal())
     , isPal() -> tt()
     , isQid() -> tt()}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds