Problem SK90 2.61

Tool CaT

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.61

stdout:

YES(?,O(n^1))

Problem:
 f(j(x,y),y) -> g(f(x,k(y)))
 f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
 g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
 h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
 i(f(x,h(y))) -> y
 i(h2(s(x),y,h1(x,z))) -> z
 k(h(x)) -> h1(0(),x)
 k(h1(x,y)) -> h1(s(x),y)

Proof:
 Complexity Transformation Processor:
  strict:
   f(j(x,y),y) -> g(f(x,k(y)))
   f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
   g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
   h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
   i(f(x,h(y))) -> y
   i(h2(s(x),y,h1(x,z))) -> z
   k(h(x)) -> h1(0(),x)
   k(h1(x,y)) -> h1(s(x),y)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [i](x0) = x0 + 14,
     
     [h](x0) = x0 + 10,
     
     [s](x0) = x0,
     
     [h2](x0, x1, x2) = x0 + x1 + x2 + 5,
     
     [0] = 9,
     
     [h1](x0, x1) = x0 + x1 + 4,
     
     [g](x0) = x0 + 7,
     
     [k](x0) = x0 + 3,
     
     [f](x0, x1) = x0 + x1 + 1,
     
     [j](x0, x1) = x0 + x1 + 10
    orientation:
     f(j(x,y),y) = x + 2y + 11 >= x + y + 11 = g(f(x,k(y)))
     
     f(x,h1(y,z)) = x + y + z + 5 >= x + y + z + 18 = h2(0(),x,h1(y,z))
     
     g(h2(x,y,h1(z,u))) = u + x + y + z + 16 >= u + x + y + z + 9 = h2(s(x),y,h1(z,u))
     
     h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z + 23 >= u + x + y + z + 9 = h2(s(x),y,h1(s(z),u))
     
     i(f(x,h(y))) = x + y + 25 >= y = y
     
     i(h2(s(x),y,h1(x,z))) = 2x + y + z + 23 >= z = z
     
     k(h(x)) = x + 13 >= x + 13 = h1(0(),x)
     
     k(h1(x,y)) = x + y + 7 >= x + y + 4 = h1(s(x),y)
    problem:
     strict:
      f(j(x,y),y) -> g(f(x,k(y)))
      f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
      k(h(x)) -> h1(0(),x)
     weak:
      g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
      h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
      i(f(x,h(y))) -> y
      i(h2(s(x),y,h1(x,z))) -> z
      k(h1(x,y)) -> h1(s(x),y)
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [i](x0) = x0 + 128,
       
       [h](x0) = x0 + 1,
       
       [s](x0) = x0 + 3,
       
       [h2](x0, x1, x2) = x0 + x1 + x2,
       
       [0] = 1,
       
       [h1](x0, x1) = x0 + x1 + 65,
       
       [g](x0) = x0 + 167,
       
       [k](x0) = x0 + 8,
       
       [f](x0, x1) = x0 + x1 + 128,
       
       [j](x0, x1) = x0 + x1 + 109
      orientation:
       f(j(x,y),y) = x + 2y + 237 >= x + y + 303 = g(f(x,k(y)))
       
       f(x,h1(y,z)) = x + y + z + 193 >= x + y + z + 66 = h2(0(),x,h1(y,z))
       
       k(h(x)) = x + 9 >= x + 66 = h1(0(),x)
       
       g(h2(x,y,h1(z,u))) = u + x + y + z + 232 >= u + x + y + z + 68 = h2(s(x),y,h1(z,u))
       
       h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z + 239 >= u + x + y + z + 71 = h2(s(x),y,h1(s(z),u))
       
       i(f(x,h(y))) = x + y + 257 >= y = y
       
       i(h2(s(x),y,h1(x,z))) = 2x + y + z + 196 >= z = z
       
       k(h1(x,y)) = x + y + 73 >= x + y + 68 = h1(s(x),y)
      problem:
       strict:
        f(j(x,y),y) -> g(f(x,k(y)))
        k(h(x)) -> h1(0(),x)
       weak:
        f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
        g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
        h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
        i(f(x,h(y))) -> y
        i(h2(s(x),y,h1(x,z))) -> z
        k(h1(x,y)) -> h1(s(x),y)
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [i](x0) = x0,
         
         [h](x0) = x0,
         
         [s](x0) = x0,
         
         [h2](x0, x1, x2) = x0 + x1 + x2,
         
         [0] = 0,
         
         [h1](x0, x1) = x0 + x1,
         
         [g](x0) = x0,
         
         [k](x0) = x0 + 1,
         
         [f](x0, x1) = x0 + x1,
         
         [j](x0, x1) = x0 + x1
        orientation:
         f(j(x,y),y) = x + 2y >= x + y + 1 = g(f(x,k(y)))
         
         k(h(x)) = x + 1 >= x = h1(0(),x)
         
         f(x,h1(y,z)) = x + y + z >= x + y + z = h2(0(),x,h1(y,z))
         
         g(h2(x,y,h1(z,u))) = u + x + y + z >= u + x + y + z = h2(s(x),y,h1(z,u))
         
         h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z >= u + x + y + z = h2(s(x),y,h1(s(z),u))
         
         i(f(x,h(y))) = x + y >= y = y
         
         i(h2(s(x),y,h1(x,z))) = 2x + y + z >= z = z
         
         k(h1(x,y)) = x + y + 1 >= x + y = h1(s(x),y)
        problem:
         strict:
          f(j(x,y),y) -> g(f(x,k(y)))
         weak:
          k(h(x)) -> h1(0(),x)
          f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
          g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
          h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
          i(f(x,h(y))) -> y
          i(h2(s(x),y,h1(x,z))) -> z
          k(h1(x,y)) -> h1(s(x),y)
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [i](x0) = x0,
           
           [h](x0) = x0 + 8,
           
           [s](x0) = x0 + 1,
           
           [h2](x0, x1, x2) = x0 + x1 + x2 + 26,
           
           [0] = 6,
           
           [h1](x0, x1) = x0 + x1,
           
           [g](x0) = x0 + 1,
           
           [k](x0) = x0 + 4,
           
           [f](x0, x1) = x0 + x1 + 58,
           
           [j](x0, x1) = x0 + x1 + 6
          orientation:
           f(j(x,y),y) = x + 2y + 64 >= x + y + 63 = g(f(x,k(y)))
           
           k(h(x)) = x + 12 >= x + 6 = h1(0(),x)
           
           f(x,h1(y,z)) = x + y + z + 58 >= x + y + z + 32 = h2(0(),x,h1(y,z))
           
           g(h2(x,y,h1(z,u))) = u + x + y + z + 27 >= u + x + y + z + 27 = h2(s(x),y,h1(z,u))
           
           h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z + 32 >= u + x + y + z + 28 = h2(s(x),y,h1(s(z),u))
           
           i(f(x,h(y))) = x + y + 66 >= y = y
           
           i(h2(s(x),y,h1(x,z))) = 2x + y + z + 27 >= z = z
           
           k(h1(x,y)) = x + y + 4 >= x + y + 1 = h1(s(x),y)
          problem:
           strict:
            
           weak:
            f(j(x,y),y) -> g(f(x,k(y)))
            k(h(x)) -> h1(0(),x)
            f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
            g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
            h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
            i(f(x,h(y))) -> y
            i(h2(s(x),y,h1(x,z))) -> z
            k(h1(x,y)) -> h1(s(x),y)
          Qed
   

Tool IRC1

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.61

stdout:

YES(?,O(n^1))

Tool IRC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.61

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  f(j(x, y), y) -> g(f(x, k(y)))
     , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
     , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
     , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
     , i(f(x, h(y))) -> y
     , i(h2(s(x), y, h1(x, z))) -> z
     , k(h(x)) -> h1(0(), x)
     , k(h1(x, y)) -> h1(s(x), y)}

Proof Output:    
  'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
  
  Details:
  --------
    'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with minimal-enrichment and initial automaton 'match''
     --------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  f(j(x, y), y) -> g(f(x, k(y)))
          , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
          , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
          , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
          , i(f(x, h(y))) -> y
          , i(h2(s(x), y, h1(x, z))) -> z
          , k(h(x)) -> h1(0(), x)
          , k(h1(x, y)) -> h1(s(x), y)}
     
     Proof Output:    
       The problem is match-bounded by 2.
       The enriched problem is compatible with the following automaton:
       {  f_0(2, 2) -> 1
        , f_1(2, 4) -> 3
        , j_0(2, 2) -> 2
        , g_0(2) -> 1
        , g_1(3) -> 1
        , g_1(3) -> 3
        , k_0(2) -> 1
        , k_1(2) -> 4
        , h1_0(2, 2) -> 2
        , h1_1(2, 2) -> 6
        , h1_1(5, 2) -> 1
        , h1_1(5, 2) -> 4
        , h1_2(2, 2) -> 8
        , h1_2(5, 2) -> 8
        , h2_0(2, 2, 2) -> 1
        , h2_1(5, 2, 6) -> 1
        , h2_1(5, 2, 6) -> 3
        , h2_1(10, 2, 6) -> 3
        , h2_2(7, 2, 8) -> 3
        , h2_2(9, 2, 8) -> 1
        , h2_2(9, 2, 8) -> 3
        , 0_0() -> 2
        , 0_1() -> 5
        , 0_2() -> 7
        , s_0(2) -> 2
        , s_1(2) -> 2
        , s_1(2) -> 5
        , s_1(5) -> 5
        , s_1(7) -> 10
        , s_1(9) -> 5
        , s_1(10) -> 5
        , s_2(5) -> 9
        , s_2(7) -> 9
        , s_2(9) -> 9
        , s_2(10) -> 9
        , i_0(2) -> 1
        , h_0(2) -> 2}

Tool RC1

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.61

stdout:

YES(?,O(n^1))

Tool RC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.61

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  f(j(x, y), y) -> g(f(x, k(y)))
     , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
     , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
     , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
     , i(f(x, h(y))) -> y
     , i(h2(s(x), y, h1(x, z))) -> z
     , k(h(x)) -> h1(0(), x)
     , k(h1(x, y)) -> h1(s(x), y)}

Proof Output:    
  'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
  
  Details:
  --------
    'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with minimal-enrichment and initial automaton 'match''
     --------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    runtime-complexity with respect to
       Rules:
         {  f(j(x, y), y) -> g(f(x, k(y)))
          , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
          , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
          , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
          , i(f(x, h(y))) -> y
          , i(h2(s(x), y, h1(x, z))) -> z
          , k(h(x)) -> h1(0(), x)
          , k(h1(x, y)) -> h1(s(x), y)}
     
     Proof Output:    
       The problem is match-bounded by 2.
       The enriched problem is compatible with the following automaton:
       {  f_0(2, 2) -> 1
        , f_1(2, 4) -> 3
        , j_0(2, 2) -> 2
        , g_0(2) -> 1
        , g_1(3) -> 1
        , g_1(3) -> 3
        , k_0(2) -> 1
        , k_1(2) -> 4
        , h1_0(2, 2) -> 2
        , h1_1(2, 2) -> 6
        , h1_1(5, 2) -> 1
        , h1_1(5, 2) -> 4
        , h1_2(2, 2) -> 8
        , h1_2(5, 2) -> 8
        , h2_0(2, 2, 2) -> 1
        , h2_1(5, 2, 6) -> 1
        , h2_1(5, 2, 6) -> 3
        , h2_1(10, 2, 6) -> 3
        , h2_2(7, 2, 8) -> 3
        , h2_2(9, 2, 8) -> 1
        , h2_2(9, 2, 8) -> 3
        , 0_0() -> 2
        , 0_1() -> 5
        , 0_2() -> 7
        , s_0(2) -> 2
        , s_1(2) -> 2
        , s_1(2) -> 5
        , s_1(5) -> 5
        , s_1(7) -> 10
        , s_1(9) -> 5
        , s_1(10) -> 5
        , s_2(5) -> 9
        , s_2(7) -> 9
        , s_2(9) -> 9
        , s_2(10) -> 9
        , i_0(2) -> 1
        , h_0(2) -> 2}

Tool pair1rc

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.61

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  f(j(x, y), y) -> g(f(x, k(y)))
     , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
     , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
     , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
     , i(f(x, h(y))) -> y
     , i(h2(s(x), y, h1(x, z))) -> z
     , k(h(x)) -> h1(0(), x)
     , k(h1(x, y)) -> h1(s(x), y)}
  StartTerms: basic terms
  Strategy: none

Certificate: YES(?,O(n^1))

Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
  The processor is not applicable, reason is:
   Input problem is not restricted to innermost rewriting
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  f(j(x, y), y) -> g(f(x, k(y)))
     , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
     , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
     , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
     , i(f(x, h(y))) -> y
     , i(h2(s(x), y, h1(x, z))) -> z
     , k(h(x)) -> h1(0(), x)
     , k(h1(x, y)) -> h1(s(x), y)}
  StartTerms: basic terms
  Strategy: none
  
  1) 'Fastest' proved the goal fastest:
     
     'Fastest' proved the goal fastest:
     
     'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
     
     The problem is match-bounded by 2.
     The enriched problem is compatible with the following automaton:
     {  f_0(2, 2) -> 1
      , f_1(2, 4) -> 3
      , j_0(2, 2) -> 2
      , g_0(2) -> 1
      , g_1(3) -> 1
      , g_1(3) -> 3
      , k_0(2) -> 1
      , k_1(2) -> 4
      , h1_0(2, 2) -> 2
      , h1_1(2, 2) -> 6
      , h1_1(5, 2) -> 1
      , h1_1(5, 2) -> 4
      , h1_2(2, 2) -> 8
      , h1_2(5, 2) -> 8
      , h2_0(2, 2, 2) -> 1
      , h2_1(5, 2, 6) -> 1
      , h2_1(5, 2, 6) -> 3
      , h2_1(10, 2, 6) -> 3
      , h2_2(7, 2, 8) -> 3
      , h2_2(9, 2, 8) -> 1
      , h2_2(9, 2, 8) -> 3
      , 0_0() -> 2
      , 0_1() -> 5
      , 0_2() -> 7
      , s_0(2) -> 2
      , s_1(2) -> 2
      , s_1(2) -> 5
      , s_1(5) -> 5
      , s_1(7) -> 10
      , s_1(9) -> 5
      , s_1(10) -> 5
      , s_2(5) -> 9
      , s_2(7) -> 9
      , s_2(9) -> 9
      , s_2(10) -> 9
      , i_0(2) -> 1
      , h_0(2) -> 2}
  

Hurray, we answered YES(?,O(n^1))

Tool pair2rc

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.61

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  f(j(x, y), y) -> g(f(x, k(y)))
     , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
     , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
     , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
     , i(f(x, h(y))) -> y
     , i(h2(s(x), y, h1(x, z))) -> z
     , k(h(x)) -> h1(0(), x)
     , k(h1(x, y)) -> h1(s(x), y)}
  StartTerms: basic terms
  Strategy: none

Certificate: YES(?,O(n^1))

Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
  The processor is not applicable, reason is:
   Input problem is not restricted to innermost rewriting
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  f(j(x, y), y) -> g(f(x, k(y)))
     , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
     , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
     , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
     , i(f(x, h(y))) -> y
     , i(h2(s(x), y, h1(x, z))) -> z
     , k(h(x)) -> h1(0(), x)
     , k(h1(x, y)) -> h1(s(x), y)}
  StartTerms: basic terms
  Strategy: none
  
  1) 'Fastest' proved the goal fastest:
     
     'Fastest' proved the goal fastest:
     
     'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
     
     The problem is match-bounded by 2.
     The enriched problem is compatible with the following automaton:
     {  f_0(2, 2) -> 1
      , f_1(2, 4) -> 3
      , j_0(2, 2) -> 2
      , g_0(2) -> 1
      , g_1(3) -> 1
      , g_1(3) -> 3
      , k_0(2) -> 1
      , k_1(2) -> 4
      , h1_0(2, 2) -> 2
      , h1_1(2, 2) -> 6
      , h1_1(5, 2) -> 1
      , h1_1(5, 2) -> 4
      , h1_2(2, 2) -> 8
      , h1_2(5, 2) -> 8
      , h2_0(2, 2, 2) -> 1
      , h2_1(5, 2, 6) -> 1
      , h2_1(5, 2, 6) -> 3
      , h2_1(10, 2, 6) -> 3
      , h2_2(7, 2, 8) -> 3
      , h2_2(9, 2, 8) -> 1
      , h2_2(9, 2, 8) -> 3
      , 0_0() -> 2
      , 0_1() -> 5
      , 0_2() -> 7
      , s_0(2) -> 2
      , s_1(2) -> 2
      , s_1(2) -> 5
      , s_1(5) -> 5
      , s_1(7) -> 10
      , s_1(9) -> 5
      , s_1(10) -> 5
      , s_2(5) -> 9
      , s_2(7) -> 9
      , s_2(9) -> 9
      , s_2(10) -> 9
      , i_0(2) -> 1
      , h_0(2) -> 2}
  

Hurray, we answered YES(?,O(n^1))

Tool pair3irc

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.61

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  f(j(x, y), y) -> g(f(x, k(y)))
     , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
     , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
     , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
     , i(f(x, h(y))) -> y
     , i(h2(s(x), y, h1(x, z))) -> z
     , k(h(x)) -> h1(0(), x)
     , k(h1(x, y)) -> h1(s(x), y)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^1))

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  The input problem contains no overlaps that give rise to inapplicable rules.
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  f(j(x, y), y) -> g(f(x, k(y)))
     , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
     , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
     , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
     , i(f(x, h(y))) -> y
     , i(h2(s(x), y, h1(x, z))) -> z
     , k(h(x)) -> h1(0(), x)
     , k(h1(x, y)) -> h1(s(x), y)}
  StartTerms: basic terms
  Strategy: innermost
  
  1) 'Fastest' proved the goal fastest:
     
     'Fastest' proved the goal fastest:
     
     'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
     
     The problem is match-bounded by 2.
     The enriched problem is compatible with the following automaton:
     {  f_0(2, 2) -> 1
      , f_1(2, 4) -> 3
      , j_0(2, 2) -> 2
      , g_0(2) -> 1
      , g_1(3) -> 1
      , g_1(3) -> 3
      , k_0(2) -> 1
      , k_1(2) -> 4
      , h1_0(2, 2) -> 2
      , h1_1(2, 2) -> 6
      , h1_1(5, 2) -> 1
      , h1_1(5, 2) -> 4
      , h1_2(2, 2) -> 8
      , h1_2(5, 2) -> 8
      , h2_0(2, 2, 2) -> 1
      , h2_1(5, 2, 6) -> 1
      , h2_1(5, 2, 6) -> 3
      , h2_1(10, 2, 6) -> 3
      , h2_2(7, 2, 8) -> 3
      , h2_2(9, 2, 8) -> 1
      , h2_2(9, 2, 8) -> 3
      , 0_0() -> 2
      , 0_1() -> 5
      , 0_2() -> 7
      , s_0(2) -> 2
      , s_1(2) -> 2
      , s_1(2) -> 5
      , s_1(5) -> 5
      , s_1(7) -> 10
      , s_1(9) -> 5
      , s_1(10) -> 5
      , s_2(5) -> 9
      , s_2(7) -> 9
      , s_2(9) -> 9
      , s_2(10) -> 9
      , i_0(2) -> 1
      , h_0(2) -> 2}
  

Hurray, we answered YES(?,O(n^1))

Tool pair3rc

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.61

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  f(j(x, y), y) -> g(f(x, k(y)))
     , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
     , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
     , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
     , i(f(x, h(y))) -> y
     , i(h2(s(x), y, h1(x, z))) -> z
     , k(h(x)) -> h1(0(), x)
     , k(h1(x, y)) -> h1(s(x), y)}
  StartTerms: basic terms
  Strategy: none

Certificate: YES(?,O(n^1))

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  The processor is not applicable, reason is:
   Input problem is not restricted to innermost rewriting
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  f(j(x, y), y) -> g(f(x, k(y)))
     , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
     , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
     , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
     , i(f(x, h(y))) -> y
     , i(h2(s(x), y, h1(x, z))) -> z
     , k(h(x)) -> h1(0(), x)
     , k(h1(x, y)) -> h1(s(x), y)}
  StartTerms: basic terms
  Strategy: none
  
  1) 'Fastest' proved the goal fastest:
     
     'Fastest' proved the goal fastest:
     
     'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
     
     The problem is match-bounded by 2.
     The enriched problem is compatible with the following automaton:
     {  f_0(2, 2) -> 1
      , f_1(2, 4) -> 3
      , j_0(2, 2) -> 2
      , g_0(2) -> 1
      , g_1(3) -> 1
      , g_1(3) -> 3
      , k_0(2) -> 1
      , k_1(2) -> 4
      , h1_0(2, 2) -> 2
      , h1_1(2, 2) -> 6
      , h1_1(5, 2) -> 1
      , h1_1(5, 2) -> 4
      , h1_2(2, 2) -> 8
      , h1_2(5, 2) -> 8
      , h2_0(2, 2, 2) -> 1
      , h2_1(5, 2, 6) -> 1
      , h2_1(5, 2, 6) -> 3
      , h2_1(10, 2, 6) -> 3
      , h2_2(7, 2, 8) -> 3
      , h2_2(9, 2, 8) -> 1
      , h2_2(9, 2, 8) -> 3
      , 0_0() -> 2
      , 0_1() -> 5
      , 0_2() -> 7
      , s_0(2) -> 2
      , s_1(2) -> 2
      , s_1(2) -> 5
      , s_1(5) -> 5
      , s_1(7) -> 10
      , s_1(9) -> 5
      , s_1(10) -> 5
      , s_2(5) -> 9
      , s_2(7) -> 9
      , s_2(9) -> 9
      , s_2(10) -> 9
      , i_0(2) -> 1
      , h_0(2) -> 2}
  

Hurray, we answered YES(?,O(n^1))

Tool rc

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSK90 2.61

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  f(j(x, y), y) -> g(f(x, k(y)))
     , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
     , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
     , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
     , i(f(x, h(y))) -> y
     , i(h2(s(x), y, h1(x, z))) -> z
     , k(h(x)) -> h1(0(), x)
     , k(h1(x, y)) -> h1(s(x), y)}
  StartTerms: basic terms
  Strategy: none

Certificate: YES(?,O(n^1))

Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
  'Fastest' proved the goal fastest:
  
  'Fastest' proved the goal fastest:
  
  'Bounds with minimal-enrichment and initial automaton 'match' (timeout of 100.0 seconds)' proved the goal fastest:
  
  The problem is match-bounded by 2.
  The enriched problem is compatible with the following automaton:
  {  f_0(2, 2) -> 1
   , f_1(2, 4) -> 3
   , j_0(2, 2) -> 2
   , g_0(2) -> 1
   , g_1(3) -> 1
   , g_1(3) -> 3
   , k_0(2) -> 1
   , k_1(2) -> 4
   , h1_0(2, 2) -> 2
   , h1_1(2, 2) -> 6
   , h1_1(5, 2) -> 1
   , h1_1(5, 2) -> 4
   , h1_2(2, 2) -> 8
   , h1_2(5, 2) -> 8
   , h2_0(2, 2, 2) -> 1
   , h2_1(5, 2, 6) -> 1
   , h2_1(5, 2, 6) -> 3
   , h2_1(10, 2, 6) -> 3
   , h2_2(7, 2, 8) -> 3
   , h2_2(9, 2, 8) -> 1
   , h2_2(9, 2, 8) -> 3
   , 0_0() -> 2
   , 0_1() -> 5
   , 0_2() -> 7
   , s_0(2) -> 2
   , s_1(2) -> 2
   , s_1(2) -> 5
   , s_1(5) -> 5
   , s_1(7) -> 10
   , s_1(9) -> 5
   , s_1(10) -> 5
   , s_2(5) -> 9
   , s_2(7) -> 9
   , s_2(9) -> 9
   , s_2(10) -> 9
   , i_0(2) -> 1
   , h_0(2) -> 2}

Hurray, we answered YES(?,O(n^1))

Tool tup3irc

Execution Time0.117959976ms
Answer
YES(?,O(n^1))
InputSK90 2.61

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  f(j(x, y), y) -> g(f(x, k(y)))
     , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
     , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
     , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
     , i(f(x, h(y))) -> y
     , i(h2(s(x), y, h1(x, z))) -> z
     , k(h(x)) -> h1(0(), x)
     , k(h1(x, y)) -> h1(s(x), y)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^1))

Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
  The input problem contains no overlaps that give rise to inapplicable rules.
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  f(j(x, y), y) -> g(f(x, k(y)))
     , f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
     , g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
     , h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
     , i(f(x, h(y))) -> y
     , i(h2(s(x), y, h1(x, z))) -> z
     , k(h(x)) -> h1(0(), x)
     , k(h1(x, y)) -> h1(s(x), y)}
  StartTerms: basic terms
  Strategy: innermost
  
  1) 'Fastest' proved the goal fastest:
     
     'Fastest' proved the goal fastest:
     
     'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
     
     The problem is match-bounded by 2.
     The enriched problem is compatible with the following automaton:
     {  f_0(2, 2) -> 1
      , f_1(2, 4) -> 3
      , j_0(2, 2) -> 2
      , g_0(2) -> 1
      , g_1(3) -> 1
      , g_1(3) -> 3
      , k_0(2) -> 1
      , k_1(2) -> 4
      , h1_0(2, 2) -> 2
      , h1_1(2, 2) -> 6
      , h1_1(5, 2) -> 1
      , h1_1(5, 2) -> 4
      , h1_2(2, 2) -> 8
      , h1_2(5, 2) -> 8
      , h2_0(2, 2, 2) -> 1
      , h2_1(5, 2, 6) -> 1
      , h2_1(5, 2, 6) -> 3
      , h2_1(10, 2, 6) -> 3
      , h2_2(7, 2, 8) -> 3
      , h2_2(9, 2, 8) -> 1
      , h2_2(9, 2, 8) -> 3
      , 0_0() -> 2
      , 0_1() -> 5
      , 0_2() -> 7
      , s_0(2) -> 2
      , s_1(2) -> 2
      , s_1(2) -> 5
      , s_1(5) -> 5
      , s_1(7) -> 10
      , s_1(9) -> 5
      , s_1(10) -> 5
      , s_2(5) -> 9
      , s_2(7) -> 9
      , s_2(9) -> 9
      , s_2(10) -> 9
      , i_0(2) -> 1
      , h_0(2) -> 2}
  

Hurray, we answered YES(?,O(n^1))