Problem Secret 06 SRS aprove03

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputSecret 06 SRS aprove03

stdout:

MAYBE

Problem:
 thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
 thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
 half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
 half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
 half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
 sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
 sixtimes(s(x1)) ->
 p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
 p(p(s(x1))) -> p(x1)
 p(s(x1)) -> x1
 p(0(x1)) -> 0(s(s(s(s(x1)))))
 0(x1) -> x1

Proof:
 Complexity Transformation Processor:
  strict:
   thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
   thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
   half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
   half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
   half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
   sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
   sixtimes(s(x1)) ->
   p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
   p(p(s(x1))) -> p(x1)
   p(s(x1)) -> x1
   p(0(x1)) -> 0(s(s(s(s(x1)))))
   0(x1) -> x1
  weak:
   
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [half](x0) = x0,
    
    [sixtimes](x0) = x0,
    
    [p](x0) = x0,
    
    [s](x0) = x0,
    
    [thrice](x0) = x0,
    
    [0](x0) = 1x0
   orientation:
    thrice(0(x1)) = 1x1 >= 1x1 = p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
    
    thrice(s(x1)) = x1 >= x1 = p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
    
    half(0(x1)) = 1x1 >= 1x1 = p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
    
    half(s(x1)) = x1 >= x1 = p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
    
    half(s(s(x1))) = x1 >= x1 = p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
    
    sixtimes(0(x1)) = 1x1 >= 1x1 = p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
    
    sixtimes(s(x1)) = x1 >= x1 = p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
    
    p(p(s(x1))) = x1 >= x1 = p(x1)
    
    p(s(x1)) = x1 >= x1 = x1
    
    p(0(x1)) = 1x1 >= 1x1 = 0(s(s(s(s(x1)))))
    
    0(x1) = 1x1 >= x1 = x1
   problem:
    strict:
     thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
     thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
     half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
     half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
     half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
     sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
     sixtimes(s(x1)) ->
     p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
     p(p(s(x1))) -> p(x1)
     p(s(x1)) -> x1
     p(0(x1)) -> 0(s(s(s(s(x1)))))
    weak:
     0(x1) -> x1
   Arctic Interpretation Processor:
    dimension: 1
    interpretation:
     [half](x0) = 2x0,
     
     [sixtimes](x0) = x0,
     
     [p](x0) = x0,
     
     [s](x0) = x0,
     
     [thrice](x0) = 3x0,
     
     [0](x0) = x0
    orientation:
     thrice(0(x1)) = 3x1 >= x1 = p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
     
     thrice(s(x1)) = 3x1 >= 2x1 = p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
     
     half(0(x1)) = 2x1 >= x1 = p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
     
     half(s(x1)) = 2x1 >= 2x1 = p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
     
     half(s(s(x1))) = 2x1 >= 2x1 = p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
     
     sixtimes(0(x1)) = x1 >= x1 = p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
     
     sixtimes(s(x1)) = x1 >= x1 = p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
     
     p(p(s(x1))) = x1 >= x1 = p(x1)
     
     p(s(x1)) = x1 >= x1 = x1
     
     p(0(x1)) = x1 >= x1 = 0(s(s(s(s(x1)))))
     
     0(x1) = x1 >= x1 = x1
    problem:
     strict:
      half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
      half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
      sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
      sixtimes(s(x1)) ->
      p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
      p(p(s(x1))) -> p(x1)
      p(s(x1)) -> x1
      p(0(x1)) -> 0(s(s(s(s(x1)))))
     weak:
      thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
      thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
      half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
      0(x1) -> x1
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [half](x0) = 1x0,
      
      [sixtimes](x0) = 2x0,
      
      [p](x0) = x0,
      
      [s](x0) = x0,
      
      [thrice](x0) = 4x0,
      
      [0](x0) = x0
     orientation:
      half(s(x1)) = 1x1 >= 1x1 = p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
      
      half(s(s(x1))) = 1x1 >= 1x1 = p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
      
      sixtimes(0(x1)) = 2x1 >= x1 = p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
      
      sixtimes(s(x1)) = 2x1 >= 2x1 = p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
      
      p(p(s(x1))) = x1 >= x1 = p(x1)
      
      p(s(x1)) = x1 >= x1 = x1
      
      p(0(x1)) = x1 >= x1 = 0(s(s(s(s(x1)))))
      
      thrice(0(x1)) = 4x1 >= x1 = p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
      
      thrice(s(x1)) = 4x1 >= 3x1 = p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
      
      half(0(x1)) = 1x1 >= x1 = p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
      
      0(x1) = x1 >= x1 = x1
     problem:
      strict:
       half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
       half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
       sixtimes(s(x1)) ->
       p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
       p(p(s(x1))) -> p(x1)
       p(s(x1)) -> x1
       p(0(x1)) -> 0(s(s(s(s(x1)))))
      weak:
       sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
       thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
       thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
       half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
       0(x1) -> x1
     Matrix Interpretation Processor:
      dimension: 1
      max_matrix:
       1
       interpretation:
        [half](x0) = x0 + 8,
        
        [sixtimes](x0) = x0 + 18,
        
        [p](x0) = x0 + 1,
        
        [s](x0) = x0,
        
        [thrice](x0) = x0 + 44,
        
        [0](x0) = x0
       orientation:
        half(s(x1)) = x1 + 8 >= x1 + 16 = p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
        
        half(s(s(x1))) = x1 + 8 >= x1 + 15 = p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
        
        sixtimes(s(x1)) = x1 + 18 >= x1 + 27 = p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
        
        p(p(s(x1))) = x1 + 2 >= x1 + 1 = p(x1)
        
        p(s(x1)) = x1 + 1 >= x1 = x1
        
        p(0(x1)) = x1 + 1 >= x1 = 0(s(s(s(s(x1)))))
        
        sixtimes(0(x1)) = x1 + 18 >= x1 + 4 = p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
        
        thrice(0(x1)) = x1 + 44 >= x1 + 6 = p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
        
        thrice(s(x1)) = x1 + 44 >= x1 + 34 = p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
        
        half(0(x1)) = x1 + 8 >= x1 + 4 = p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
        
        0(x1) = x1 >= x1 = x1
       problem:
        strict:
         half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
         half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
         sixtimes(s(x1)) ->
         p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
        weak:
         p(p(s(x1))) -> p(x1)
         p(s(x1)) -> x1
         p(0(x1)) -> 0(s(s(s(s(x1)))))
         sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
         thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
         thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
         half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
         0(x1) -> x1
       Open
 

Tool IRC1

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSecret 06 SRS aprove03

stdout:

YES(?,O(n^1))

Tool IRC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSecret 06 SRS aprove03

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:
    {  thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
     , thrice(s(x1)) ->
       p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
     , half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
     , half(s(x1)) ->
       p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
     , half(s(s(x1))) ->
       p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
     , sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
     , sixtimes(s(x1)) ->
       p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
     , p(p(s(x1))) -> p(x1)
     , p(s(x1)) -> x1
     , p(0(x1)) -> 0(s(s(s(s(x1)))))
     , 0(x1) -> x1}

Proof Output:    
  'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:
  
  Details:
  --------
    'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with perSymbol-enrichment and initial automaton 'match''
     ----------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
          , thrice(s(x1)) ->
            p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
          , half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
          , half(s(x1)) ->
            p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
          , half(s(s(x1))) ->
            p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
          , sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
          , sixtimes(s(x1)) ->
            p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
          , p(p(s(x1))) -> p(x1)
          , p(s(x1)) -> x1
          , p(0(x1)) -> 0(s(s(s(s(x1)))))
          , 0(x1) -> x1}
     
     Proof Output:    
       The problem is match-bounded by 3.
       The enriched problem is compatible with the following automaton:
       {  thrice_0(4) -> 1
        , 0_0(4) -> 2
        , p_0(4) -> 3
        , p_1(7) -> 1
        , p_1(8) -> 7
        , p_1(12) -> 11
        , p_1(13) -> 12
        , p_1(16) -> 11
        , p_1(16) -> 15
        , p_1(19) -> 18
        , p_1(21) -> 18
        , p_1(21) -> 20
        , p_1(22) -> 21
        , p_1(23) -> 34
        , p_1(23) -> 38
        , p_1(24) -> 5
        , p_1(24) -> 25
        , p_1(24) -> 29
        , p_1(24) -> 33
        , p_1(26) -> 5
        , p_1(26) -> 25
        , p_1(26) -> 29
        , p_1(26) -> 33
        , p_1(27) -> 5
        , p_1(27) -> 25
        , p_1(27) -> 26
        , p_1(27) -> 29
        , p_1(27) -> 33
        , p_1(30) -> 5
        , p_1(30) -> 25
        , p_1(30) -> 29
        , p_1(30) -> 33
        , p_1(31) -> 30
        , p_1(35) -> 34
        , p_1(36) -> 35
        , p_1(39) -> 6
        , p_1(39) -> 11
        , p_1(39) -> 15
        , p_1(39) -> 17
        , p_1(39) -> 54
        , p_1(39) -> 150
        , p_1(39) -> 154
        , p_1(40) -> 39
        , p_1(48) -> 47
        , p_1(48) -> 133
        , p_1(48) -> 137
        , p_1(49) -> 48
        , p_1(51) -> 48
        , p_1(51) -> 50
        , p_1(56) -> 55
        , p_1(58) -> 55
        , p_1(58) -> 57
        , p_1(59) -> 58
        , p_1(60) -> 59
        , p_2(9) -> 1
        , p_2(9) -> 10
        , p_2(14) -> 11
        , p_2(22) -> 58
        , p_2(23) -> 18
        , p_2(23) -> 20
        , p_2(23) -> 55
        , p_2(23) -> 57
        , p_2(28) -> 5
        , p_2(28) -> 25
        , p_2(28) -> 29
        , p_2(28) -> 33
        , p_2(32) -> 5
        , p_2(32) -> 25
        , p_2(32) -> 29
        , p_2(32) -> 33
        , p_2(37) -> 34
        , p_2(41) -> 6
        , p_2(41) -> 11
        , p_2(41) -> 15
        , p_2(41) -> 17
        , p_2(41) -> 54
        , p_2(41) -> 150
        , p_2(41) -> 154
        , p_2(50) -> 47
        , p_2(50) -> 133
        , p_2(50) -> 137
        , p_2(52) -> 47
        , p_2(52) -> 133
        , p_2(52) -> 137
        , p_2(61) -> 1
        , p_2(61) -> 10
        , p_2(61) -> 61
        , p_2(61) -> 65
        , p_2(61) -> 69
        , p_2(61) -> 77
        , p_2(61) -> 81
        , p_2(61) -> 91
        , p_2(61) -> 95
        , p_2(61) -> 102
        , p_2(61) -> 111
        , p_2(61) -> 128
        , p_2(61) -> 132
        , p_2(61) -> 139
        , p_2(61) -> 148
        , p_2(62) -> 1
        , p_2(62) -> 10
        , p_2(62) -> 61
        , p_2(63) -> 62
        , p_2(66) -> 1
        , p_2(66) -> 10
        , p_2(66) -> 61
        , p_2(66) -> 65
        , p_2(66) -> 69
        , p_2(66) -> 77
        , p_2(66) -> 81
        , p_2(66) -> 91
        , p_2(66) -> 95
        , p_2(66) -> 102
        , p_2(66) -> 111
        , p_2(66) -> 128
        , p_2(66) -> 132
        , p_2(66) -> 139
        , p_2(66) -> 148
        , p_2(67) -> 66
        , p_2(68) -> 1
        , p_2(68) -> 10
        , p_2(68) -> 61
        , p_2(68) -> 65
        , p_2(68) -> 69
        , p_2(68) -> 77
        , p_2(68) -> 81
        , p_2(68) -> 91
        , p_2(68) -> 95
        , p_2(68) -> 102
        , p_2(68) -> 111
        , p_2(68) -> 128
        , p_2(68) -> 132
        , p_2(68) -> 139
        , p_2(68) -> 148
        , p_2(71) -> 70
        , p_2(72) -> 71
        , p_2(75) -> 70
        , p_2(75) -> 74
        , p_2(78) -> 1
        , p_2(78) -> 10
        , p_2(78) -> 61
        , p_2(78) -> 65
        , p_2(78) -> 69
        , p_2(78) -> 77
        , p_2(78) -> 81
        , p_2(78) -> 91
        , p_2(78) -> 95
        , p_2(78) -> 102
        , p_2(78) -> 111
        , p_2(78) -> 128
        , p_2(78) -> 132
        , p_2(78) -> 139
        , p_2(78) -> 148
        , p_2(79) -> 78
        , p_2(80) -> 1
        , p_2(80) -> 10
        , p_2(80) -> 61
        , p_2(80) -> 65
        , p_2(80) -> 69
        , p_2(80) -> 77
        , p_2(80) -> 81
        , p_2(80) -> 91
        , p_2(80) -> 95
        , p_2(80) -> 102
        , p_2(80) -> 111
        , p_2(80) -> 128
        , p_2(80) -> 132
        , p_2(80) -> 139
        , p_2(80) -> 148
        , p_2(83) -> 82
        , p_2(84) -> 83
        , p_2(87) -> 82
        , p_2(87) -> 86
        , p_2(88) -> 1
        , p_2(88) -> 10
        , p_2(88) -> 61
        , p_2(88) -> 65
        , p_2(88) -> 69
        , p_2(88) -> 77
        , p_2(88) -> 81
        , p_2(88) -> 91
        , p_2(88) -> 95
        , p_2(88) -> 102
        , p_2(88) -> 111
        , p_2(88) -> 128
        , p_2(88) -> 132
        , p_2(88) -> 139
        , p_2(88) -> 148
        , p_2(89) -> 1
        , p_2(89) -> 10
        , p_2(89) -> 61
        , p_2(89) -> 65
        , p_2(89) -> 69
        , p_2(89) -> 77
        , p_2(89) -> 81
        , p_2(89) -> 88
        , p_2(89) -> 91
        , p_2(89) -> 95
        , p_2(89) -> 102
        , p_2(89) -> 111
        , p_2(89) -> 128
        , p_2(89) -> 132
        , p_2(89) -> 139
        , p_2(89) -> 148
        , p_2(92) -> 1
        , p_2(92) -> 10
        , p_2(92) -> 61
        , p_2(92) -> 65
        , p_2(92) -> 69
        , p_2(92) -> 77
        , p_2(92) -> 81
        , p_2(92) -> 91
        , p_2(92) -> 95
        , p_2(92) -> 102
        , p_2(92) -> 111
        , p_2(92) -> 128
        , p_2(92) -> 132
        , p_2(92) -> 139
        , p_2(92) -> 148
        , p_2(93) -> 92
        , p_2(94) -> 1
        , p_2(94) -> 10
        , p_2(94) -> 61
        , p_2(94) -> 65
        , p_2(94) -> 69
        , p_2(94) -> 77
        , p_2(94) -> 81
        , p_2(94) -> 91
        , p_2(94) -> 95
        , p_2(94) -> 102
        , p_2(94) -> 111
        , p_2(94) -> 128
        , p_2(94) -> 132
        , p_2(94) -> 139
        , p_2(94) -> 148
        , p_2(97) -> 96
        , p_2(98) -> 97
        , p_2(101) -> 96
        , p_2(101) -> 100
        , p_2(103) -> 1
        , p_2(103) -> 10
        , p_2(103) -> 61
        , p_2(103) -> 65
        , p_2(103) -> 69
        , p_2(103) -> 77
        , p_2(103) -> 81
        , p_2(103) -> 91
        , p_2(103) -> 95
        , p_2(103) -> 102
        , p_2(103) -> 111
        , p_2(103) -> 128
        , p_2(103) -> 132
        , p_2(103) -> 139
        , p_2(103) -> 148
        , p_2(104) -> 103
        , p_2(109) -> 1
        , p_2(109) -> 10
        , p_2(109) -> 61
        , p_2(109) -> 65
        , p_2(109) -> 69
        , p_2(109) -> 77
        , p_2(109) -> 81
        , p_2(109) -> 91
        , p_2(109) -> 95
        , p_2(109) -> 102
        , p_2(109) -> 111
        , p_2(109) -> 128
        , p_2(109) -> 132
        , p_2(109) -> 139
        , p_2(109) -> 148
        , p_2(114) -> 113
        , p_2(115) -> 114
        , p_2(118) -> 113
        , p_2(118) -> 117
        , p_2(125) -> 1
        , p_2(125) -> 10
        , p_2(125) -> 61
        , p_2(125) -> 65
        , p_2(125) -> 69
        , p_2(125) -> 77
        , p_2(125) -> 81
        , p_2(125) -> 91
        , p_2(125) -> 95
        , p_2(125) -> 102
        , p_2(125) -> 111
        , p_2(125) -> 128
        , p_2(125) -> 132
        , p_2(125) -> 139
        , p_2(125) -> 148
        , p_2(126) -> 1
        , p_2(126) -> 10
        , p_2(126) -> 61
        , p_2(126) -> 65
        , p_2(126) -> 69
        , p_2(126) -> 77
        , p_2(126) -> 81
        , p_2(126) -> 91
        , p_2(126) -> 95
        , p_2(126) -> 102
        , p_2(126) -> 111
        , p_2(126) -> 125
        , p_2(126) -> 128
        , p_2(126) -> 132
        , p_2(126) -> 139
        , p_2(126) -> 148
        , p_2(129) -> 1
        , p_2(129) -> 10
        , p_2(129) -> 61
        , p_2(129) -> 65
        , p_2(129) -> 69
        , p_2(129) -> 77
        , p_2(129) -> 81
        , p_2(129) -> 91
        , p_2(129) -> 95
        , p_2(129) -> 102
        , p_2(129) -> 111
        , p_2(129) -> 128
        , p_2(129) -> 132
        , p_2(129) -> 139
        , p_2(129) -> 148
        , p_2(130) -> 129
        , p_2(134) -> 133
        , p_2(135) -> 134
        , p_2(138) -> 133
        , p_2(138) -> 137
        , p_2(140) -> 1
        , p_2(140) -> 10
        , p_2(140) -> 61
        , p_2(140) -> 65
        , p_2(140) -> 69
        , p_2(140) -> 77
        , p_2(140) -> 81
        , p_2(140) -> 91
        , p_2(140) -> 95
        , p_2(140) -> 102
        , p_2(140) -> 111
        , p_2(140) -> 128
        , p_2(140) -> 132
        , p_2(140) -> 139
        , p_2(140) -> 148
        , p_2(141) -> 140
        , p_2(151) -> 150
        , p_2(152) -> 151
        , p_2(155) -> 150
        , p_2(155) -> 154
        , p_3(64) -> 1
        , p_3(64) -> 10
        , p_3(64) -> 61
        , p_3(65) -> 1
        , p_3(65) -> 10
        , p_3(65) -> 61
        , p_3(65) -> 65
        , p_3(65) -> 69
        , p_3(65) -> 77
        , p_3(65) -> 81
        , p_3(65) -> 91
        , p_3(65) -> 95
        , p_3(65) -> 102
        , p_3(65) -> 111
        , p_3(65) -> 128
        , p_3(65) -> 132
        , p_3(65) -> 139
        , p_3(65) -> 148
        , p_3(68) -> 1
        , p_3(68) -> 10
        , p_3(68) -> 61
        , p_3(68) -> 65
        , p_3(68) -> 69
        , p_3(68) -> 77
        , p_3(68) -> 81
        , p_3(68) -> 91
        , p_3(68) -> 95
        , p_3(68) -> 102
        , p_3(68) -> 111
        , p_3(68) -> 128
        , p_3(68) -> 132
        , p_3(68) -> 139
        , p_3(68) -> 148
        , p_3(69) -> 1
        , p_3(69) -> 10
        , p_3(69) -> 61
        , p_3(69) -> 65
        , p_3(69) -> 69
        , p_3(69) -> 77
        , p_3(69) -> 81
        , p_3(69) -> 91
        , p_3(69) -> 95
        , p_3(69) -> 102
        , p_3(69) -> 111
        , p_3(69) -> 128
        , p_3(69) -> 132
        , p_3(69) -> 139
        , p_3(69) -> 148
        , p_3(73) -> 70
        , p_3(76) -> 1
        , p_3(76) -> 10
        , p_3(76) -> 61
        , p_3(76) -> 65
        , p_3(76) -> 69
        , p_3(76) -> 77
        , p_3(76) -> 81
        , p_3(76) -> 91
        , p_3(76) -> 95
        , p_3(76) -> 102
        , p_3(76) -> 111
        , p_3(76) -> 128
        , p_3(76) -> 132
        , p_3(76) -> 139
        , p_3(76) -> 148
        , p_3(77) -> 1
        , p_3(77) -> 10
        , p_3(77) -> 61
        , p_3(77) -> 65
        , p_3(77) -> 69
        , p_3(77) -> 77
        , p_3(77) -> 81
        , p_3(77) -> 91
        , p_3(77) -> 95
        , p_3(77) -> 102
        , p_3(77) -> 111
        , p_3(77) -> 128
        , p_3(77) -> 132
        , p_3(77) -> 139
        , p_3(77) -> 148
        , p_3(80) -> 1
        , p_3(80) -> 10
        , p_3(80) -> 61
        , p_3(80) -> 65
        , p_3(80) -> 69
        , p_3(80) -> 77
        , p_3(80) -> 81
        , p_3(80) -> 91
        , p_3(80) -> 95
        , p_3(80) -> 102
        , p_3(80) -> 111
        , p_3(80) -> 128
        , p_3(80) -> 132
        , p_3(80) -> 139
        , p_3(80) -> 148
        , p_3(81) -> 1
        , p_3(81) -> 10
        , p_3(81) -> 61
        , p_3(81) -> 65
        , p_3(81) -> 69
        , p_3(81) -> 77
        , p_3(81) -> 81
        , p_3(81) -> 91
        , p_3(81) -> 95
        , p_3(81) -> 102
        , p_3(81) -> 111
        , p_3(81) -> 128
        , p_3(81) -> 132
        , p_3(81) -> 139
        , p_3(81) -> 148
        , p_3(85) -> 82
        , p_3(88) -> 1
        , p_3(88) -> 10
        , p_3(88) -> 61
        , p_3(88) -> 65
        , p_3(88) -> 69
        , p_3(88) -> 77
        , p_3(88) -> 81
        , p_3(88) -> 91
        , p_3(88) -> 95
        , p_3(88) -> 102
        , p_3(88) -> 111
        , p_3(88) -> 128
        , p_3(88) -> 132
        , p_3(88) -> 139
        , p_3(88) -> 148
        , p_3(90) -> 1
        , p_3(90) -> 10
        , p_3(90) -> 61
        , p_3(90) -> 65
        , p_3(90) -> 69
        , p_3(90) -> 77
        , p_3(90) -> 81
        , p_3(90) -> 91
        , p_3(90) -> 95
        , p_3(90) -> 102
        , p_3(90) -> 111
        , p_3(90) -> 128
        , p_3(90) -> 132
        , p_3(90) -> 139
        , p_3(90) -> 148
        , p_3(91) -> 1
        , p_3(91) -> 10
        , p_3(91) -> 61
        , p_3(91) -> 65
        , p_3(91) -> 69
        , p_3(91) -> 77
        , p_3(91) -> 81
        , p_3(91) -> 91
        , p_3(91) -> 95
        , p_3(91) -> 102
        , p_3(91) -> 111
        , p_3(91) -> 128
        , p_3(91) -> 132
        , p_3(91) -> 139
        , p_3(91) -> 148
        , p_3(94) -> 1
        , p_3(94) -> 10
        , p_3(94) -> 61
        , p_3(94) -> 65
        , p_3(94) -> 69
        , p_3(94) -> 77
        , p_3(94) -> 81
        , p_3(94) -> 91
        , p_3(94) -> 95
        , p_3(94) -> 102
        , p_3(94) -> 111
        , p_3(94) -> 128
        , p_3(94) -> 132
        , p_3(94) -> 139
        , p_3(94) -> 148
        , p_3(95) -> 1
        , p_3(95) -> 10
        , p_3(95) -> 61
        , p_3(95) -> 65
        , p_3(95) -> 69
        , p_3(95) -> 77
        , p_3(95) -> 81
        , p_3(95) -> 91
        , p_3(95) -> 95
        , p_3(95) -> 102
        , p_3(95) -> 111
        , p_3(95) -> 128
        , p_3(95) -> 132
        , p_3(95) -> 139
        , p_3(95) -> 148
        , p_3(99) -> 96
        , p_3(102) -> 1
        , p_3(102) -> 10
        , p_3(102) -> 61
        , p_3(102) -> 65
        , p_3(102) -> 69
        , p_3(102) -> 77
        , p_3(102) -> 81
        , p_3(102) -> 91
        , p_3(102) -> 95
        , p_3(102) -> 102
        , p_3(102) -> 111
        , p_3(102) -> 128
        , p_3(102) -> 132
        , p_3(102) -> 139
        , p_3(102) -> 148
        , p_3(109) -> 1
        , p_3(109) -> 10
        , p_3(109) -> 61
        , p_3(109) -> 65
        , p_3(109) -> 69
        , p_3(109) -> 77
        , p_3(109) -> 81
        , p_3(109) -> 91
        , p_3(109) -> 95
        , p_3(109) -> 102
        , p_3(109) -> 111
        , p_3(109) -> 128
        , p_3(109) -> 132
        , p_3(109) -> 139
        , p_3(109) -> 148
        , p_3(111) -> 1
        , p_3(111) -> 10
        , p_3(111) -> 61
        , p_3(111) -> 65
        , p_3(111) -> 69
        , p_3(111) -> 77
        , p_3(111) -> 81
        , p_3(111) -> 91
        , p_3(111) -> 95
        , p_3(111) -> 102
        , p_3(111) -> 111
        , p_3(111) -> 128
        , p_3(111) -> 132
        , p_3(111) -> 139
        , p_3(111) -> 148
        , p_3(116) -> 113
        , p_3(125) -> 1
        , p_3(125) -> 10
        , p_3(125) -> 61
        , p_3(125) -> 65
        , p_3(125) -> 69
        , p_3(125) -> 77
        , p_3(125) -> 81
        , p_3(125) -> 91
        , p_3(125) -> 95
        , p_3(125) -> 102
        , p_3(125) -> 111
        , p_3(125) -> 128
        , p_3(125) -> 132
        , p_3(125) -> 139
        , p_3(125) -> 148
        , p_3(127) -> 1
        , p_3(127) -> 10
        , p_3(127) -> 61
        , p_3(127) -> 65
        , p_3(127) -> 69
        , p_3(127) -> 77
        , p_3(127) -> 81
        , p_3(127) -> 91
        , p_3(127) -> 95
        , p_3(127) -> 102
        , p_3(127) -> 111
        , p_3(127) -> 128
        , p_3(127) -> 132
        , p_3(127) -> 139
        , p_3(127) -> 148
        , p_3(128) -> 1
        , p_3(128) -> 10
        , p_3(128) -> 61
        , p_3(128) -> 65
        , p_3(128) -> 69
        , p_3(128) -> 77
        , p_3(128) -> 81
        , p_3(128) -> 91
        , p_3(128) -> 95
        , p_3(128) -> 102
        , p_3(128) -> 111
        , p_3(128) -> 128
        , p_3(128) -> 132
        , p_3(128) -> 139
        , p_3(128) -> 148
        , p_3(131) -> 1
        , p_3(131) -> 10
        , p_3(131) -> 61
        , p_3(131) -> 65
        , p_3(131) -> 69
        , p_3(131) -> 77
        , p_3(131) -> 81
        , p_3(131) -> 91
        , p_3(131) -> 95
        , p_3(131) -> 102
        , p_3(131) -> 111
        , p_3(131) -> 128
        , p_3(131) -> 132
        , p_3(131) -> 139
        , p_3(131) -> 148
        , p_3(132) -> 1
        , p_3(132) -> 10
        , p_3(132) -> 61
        , p_3(132) -> 65
        , p_3(132) -> 69
        , p_3(132) -> 77
        , p_3(132) -> 81
        , p_3(132) -> 91
        , p_3(132) -> 95
        , p_3(132) -> 102
        , p_3(132) -> 111
        , p_3(132) -> 128
        , p_3(132) -> 132
        , p_3(132) -> 139
        , p_3(132) -> 148
        , p_3(136) -> 133
        , p_3(139) -> 1
        , p_3(139) -> 10
        , p_3(139) -> 61
        , p_3(139) -> 65
        , p_3(139) -> 69
        , p_3(139) -> 77
        , p_3(139) -> 81
        , p_3(139) -> 91
        , p_3(139) -> 95
        , p_3(139) -> 102
        , p_3(139) -> 111
        , p_3(139) -> 128
        , p_3(139) -> 132
        , p_3(139) -> 139
        , p_3(139) -> 148
        , p_3(146) -> 1
        , p_3(146) -> 10
        , p_3(146) -> 61
        , p_3(146) -> 65
        , p_3(146) -> 69
        , p_3(146) -> 77
        , p_3(146) -> 81
        , p_3(146) -> 91
        , p_3(146) -> 95
        , p_3(146) -> 102
        , p_3(146) -> 111
        , p_3(146) -> 128
        , p_3(146) -> 132
        , p_3(146) -> 139
        , p_3(146) -> 148
        , p_3(148) -> 1
        , p_3(148) -> 10
        , p_3(148) -> 61
        , p_3(148) -> 65
        , p_3(148) -> 69
        , p_3(148) -> 77
        , p_3(148) -> 81
        , p_3(148) -> 91
        , p_3(148) -> 95
        , p_3(148) -> 102
        , p_3(148) -> 111
        , p_3(148) -> 128
        , p_3(148) -> 132
        , p_3(148) -> 139
        , p_3(148) -> 148
        , p_3(153) -> 150
        , s_0(4) -> 2
        , s_0(4) -> 3
        , s_0(4) -> 4
        , s_0(4) -> 18
        , s_0(4) -> 20
        , s_0(4) -> 34
        , s_0(4) -> 38
        , s_0(4) -> 55
        , s_0(4) -> 57
        , s_1(4) -> 21
        , s_1(4) -> 23
        , s_1(4) -> 58
        , s_1(9) -> 8
        , s_1(10) -> 7
        , s_1(10) -> 9
        , s_1(14) -> 13
        , s_1(15) -> 12
        , s_1(15) -> 14
        , s_1(17) -> 16
        , s_1(20) -> 19
        , s_1(22) -> 60
        , s_1(23) -> 22
        , s_1(23) -> 59
        , s_1(25) -> 24
        , s_1(26) -> 24
        , s_1(28) -> 27
        , s_1(29) -> 5
        , s_1(29) -> 25
        , s_1(29) -> 26
        , s_1(29) -> 28
        , s_1(29) -> 29
        , s_1(29) -> 33
        , s_1(32) -> 31
        , s_1(33) -> 30
        , s_1(33) -> 32
        , s_1(37) -> 36
        , s_1(38) -> 35
        , s_1(38) -> 37
        , s_1(41) -> 40
        , s_1(42) -> 39
        , s_1(42) -> 41
        , s_1(43) -> 6
        , s_1(43) -> 11
        , s_1(43) -> 15
        , s_1(43) -> 17
        , s_1(43) -> 42
        , s_1(43) -> 54
        , s_1(43) -> 150
        , s_1(43) -> 154
        , s_1(44) -> 43
        , s_1(44) -> 70
        , s_1(44) -> 74
        , s_1(45) -> 44
        , s_1(45) -> 82
        , s_1(45) -> 86
        , s_1(46) -> 45
        , s_1(46) -> 96
        , s_1(46) -> 100
        , s_1(47) -> 46
        , s_1(47) -> 113
        , s_1(47) -> 117
        , s_1(50) -> 49
        , s_1(52) -> 51
        , s_1(53) -> 48
        , s_1(53) -> 50
        , s_1(53) -> 52
        , s_1(54) -> 47
        , s_1(54) -> 53
        , s_1(54) -> 133
        , s_1(54) -> 137
        , s_1(57) -> 56
        , s_2(43) -> 75
        , s_2(44) -> 87
        , s_2(45) -> 101
        , s_2(46) -> 118
        , s_2(47) -> 138
        , s_2(54) -> 155
        , s_2(61) -> 7
        , s_2(61) -> 9
        , s_2(64) -> 63
        , s_2(65) -> 62
        , s_2(65) -> 64
        , s_2(68) -> 67
        , s_2(69) -> 66
        , s_2(69) -> 68
        , s_2(73) -> 72
        , s_2(74) -> 71
        , s_2(74) -> 73
        , s_2(76) -> 62
        , s_2(77) -> 1
        , s_2(77) -> 10
        , s_2(77) -> 61
        , s_2(77) -> 76
        , s_2(80) -> 79
        , s_2(81) -> 78
        , s_2(81) -> 80
        , s_2(85) -> 84
        , s_2(86) -> 83
        , s_2(86) -> 85
        , s_2(88) -> 66
        , s_2(90) -> 89
        , s_2(91) -> 1
        , s_2(91) -> 10
        , s_2(91) -> 61
        , s_2(91) -> 65
        , s_2(91) -> 69
        , s_2(91) -> 77
        , s_2(91) -> 81
        , s_2(91) -> 88
        , s_2(91) -> 90
        , s_2(91) -> 91
        , s_2(91) -> 95
        , s_2(91) -> 102
        , s_2(91) -> 111
        , s_2(91) -> 128
        , s_2(91) -> 132
        , s_2(91) -> 139
        , s_2(91) -> 148
        , s_2(94) -> 93
        , s_2(95) -> 92
        , s_2(95) -> 94
        , s_2(99) -> 98
        , s_2(100) -> 97
        , s_2(100) -> 99
        , s_2(102) -> 1
        , s_2(102) -> 10
        , s_2(102) -> 61
        , s_2(102) -> 65
        , s_2(102) -> 69
        , s_2(102) -> 77
        , s_2(102) -> 81
        , s_2(102) -> 91
        , s_2(102) -> 95
        , s_2(102) -> 102
        , s_2(102) -> 111
        , s_2(102) -> 128
        , s_2(102) -> 132
        , s_2(102) -> 139
        , s_2(102) -> 148
        , s_2(109) -> 104
        , s_2(111) -> 103
        , s_2(111) -> 109
        , s_2(116) -> 115
        , s_2(117) -> 114
        , s_2(117) -> 116
        , s_2(125) -> 66
        , s_2(125) -> 68
        , s_2(127) -> 126
        , s_2(128) -> 1
        , s_2(128) -> 10
        , s_2(128) -> 61
        , s_2(128) -> 65
        , s_2(128) -> 69
        , s_2(128) -> 77
        , s_2(128) -> 81
        , s_2(128) -> 91
        , s_2(128) -> 95
        , s_2(128) -> 102
        , s_2(128) -> 111
        , s_2(128) -> 125
        , s_2(128) -> 127
        , s_2(128) -> 128
        , s_2(128) -> 132
        , s_2(128) -> 139
        , s_2(128) -> 148
        , s_2(131) -> 130
        , s_2(132) -> 129
        , s_2(132) -> 131
        , s_2(136) -> 135
        , s_2(137) -> 134
        , s_2(137) -> 136
        , s_2(139) -> 1
        , s_2(139) -> 10
        , s_2(139) -> 61
        , s_2(139) -> 65
        , s_2(139) -> 69
        , s_2(139) -> 77
        , s_2(139) -> 81
        , s_2(139) -> 91
        , s_2(139) -> 95
        , s_2(139) -> 102
        , s_2(139) -> 111
        , s_2(139) -> 128
        , s_2(139) -> 132
        , s_2(139) -> 139
        , s_2(139) -> 148
        , s_2(146) -> 141
        , s_2(148) -> 140
        , s_2(148) -> 146
        , s_2(153) -> 152
        , s_2(154) -> 151
        , s_2(154) -> 153
        , half_0(4) -> 5
        , half_1(11) -> 1
        , half_1(11) -> 10
        , half_1(34) -> 5
        , half_1(34) -> 25
        , half_1(34) -> 29
        , half_1(34) -> 33
        , half_2(70) -> 1
        , half_2(70) -> 10
        , half_2(70) -> 61
        , half_2(70) -> 65
        , half_2(70) -> 69
        , half_2(70) -> 77
        , half_2(70) -> 81
        , half_2(70) -> 91
        , half_2(70) -> 95
        , half_2(70) -> 102
        , half_2(70) -> 111
        , half_2(70) -> 128
        , half_2(70) -> 132
        , half_2(70) -> 139
        , half_2(70) -> 148
        , half_2(82) -> 1
        , half_2(82) -> 10
        , half_2(82) -> 61
        , half_2(82) -> 65
        , half_2(82) -> 69
        , half_2(82) -> 77
        , half_2(82) -> 81
        , half_2(82) -> 91
        , half_2(82) -> 95
        , half_2(82) -> 102
        , half_2(82) -> 111
        , half_2(82) -> 128
        , half_2(82) -> 132
        , half_2(82) -> 139
        , half_2(82) -> 148
        , half_2(96) -> 1
        , half_2(96) -> 10
        , half_2(96) -> 61
        , half_2(96) -> 65
        , half_2(96) -> 69
        , half_2(96) -> 77
        , half_2(96) -> 81
        , half_2(96) -> 91
        , half_2(96) -> 95
        , half_2(96) -> 102
        , half_2(96) -> 111
        , half_2(96) -> 128
        , half_2(96) -> 132
        , half_2(96) -> 139
        , half_2(96) -> 148
        , half_2(113) -> 1
        , half_2(113) -> 10
        , half_2(113) -> 61
        , half_2(113) -> 65
        , half_2(113) -> 69
        , half_2(113) -> 77
        , half_2(113) -> 81
        , half_2(113) -> 91
        , half_2(113) -> 95
        , half_2(113) -> 102
        , half_2(113) -> 111
        , half_2(113) -> 128
        , half_2(113) -> 132
        , half_2(113) -> 139
        , half_2(113) -> 148
        , half_2(133) -> 1
        , half_2(133) -> 10
        , half_2(133) -> 61
        , half_2(133) -> 65
        , half_2(133) -> 69
        , half_2(133) -> 77
        , half_2(133) -> 81
        , half_2(133) -> 91
        , half_2(133) -> 95
        , half_2(133) -> 102
        , half_2(133) -> 111
        , half_2(133) -> 128
        , half_2(133) -> 132
        , half_2(133) -> 139
        , half_2(133) -> 148
        , half_2(150) -> 1
        , half_2(150) -> 10
        , half_2(150) -> 61
        , half_2(150) -> 65
        , half_2(150) -> 69
        , half_2(150) -> 77
        , half_2(150) -> 81
        , half_2(150) -> 91
        , half_2(150) -> 95
        , half_2(150) -> 102
        , half_2(150) -> 111
        , half_2(150) -> 128
        , half_2(150) -> 132
        , half_2(150) -> 139
        , half_2(150) -> 148
        , sixtimes_0(4) -> 6
        , sixtimes_1(18) -> 11
        , sixtimes_1(18) -> 15
        , sixtimes_1(18) -> 17
        , sixtimes_1(55) -> 54
        , sixtimes_1(55) -> 150
        , sixtimes_1(55) -> 154}

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputSecret 06 SRS aprove03

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputSecret 06 SRS aprove03

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
     , thrice(s(x1)) ->
       p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
     , half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
     , half(s(x1)) ->
       p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
     , half(s(s(x1))) ->
       p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
     , sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
     , sixtimes(s(x1)) ->
       p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
     , p(p(s(x1))) -> p(x1)
     , p(s(x1)) -> x1
     , p(0(x1)) -> 0(s(s(s(s(x1)))))
     , 0(x1) -> x1}

Proof Output:    
  'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:
  
  Details:
  --------
    'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with perSymbol-enrichment and initial automaton 'match''
     ----------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    runtime-complexity with respect to
       Rules:
         {  thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
          , thrice(s(x1)) ->
            p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
          , half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
          , half(s(x1)) ->
            p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
          , half(s(s(x1))) ->
            p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
          , sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
          , sixtimes(s(x1)) ->
            p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
          , p(p(s(x1))) -> p(x1)
          , p(s(x1)) -> x1
          , p(0(x1)) -> 0(s(s(s(s(x1)))))
          , 0(x1) -> x1}
     
     Proof Output:    
       The problem is match-bounded by 3.
       The enriched problem is compatible with the following automaton:
       {  thrice_0(4) -> 1
        , 0_0(4) -> 2
        , p_0(4) -> 3
        , p_1(7) -> 1
        , p_1(8) -> 7
        , p_1(12) -> 11
        , p_1(13) -> 12
        , p_1(16) -> 11
        , p_1(16) -> 15
        , p_1(19) -> 18
        , p_1(21) -> 18
        , p_1(21) -> 20
        , p_1(22) -> 21
        , p_1(23) -> 34
        , p_1(23) -> 38
        , p_1(24) -> 5
        , p_1(24) -> 25
        , p_1(24) -> 29
        , p_1(24) -> 33
        , p_1(26) -> 5
        , p_1(26) -> 25
        , p_1(26) -> 29
        , p_1(26) -> 33
        , p_1(27) -> 5
        , p_1(27) -> 25
        , p_1(27) -> 26
        , p_1(27) -> 29
        , p_1(27) -> 33
        , p_1(30) -> 5
        , p_1(30) -> 25
        , p_1(30) -> 29
        , p_1(30) -> 33
        , p_1(31) -> 30
        , p_1(35) -> 34
        , p_1(36) -> 35
        , p_1(39) -> 6
        , p_1(39) -> 11
        , p_1(39) -> 15
        , p_1(39) -> 17
        , p_1(39) -> 54
        , p_1(39) -> 150
        , p_1(39) -> 154
        , p_1(40) -> 39
        , p_1(48) -> 47
        , p_1(48) -> 133
        , p_1(48) -> 137
        , p_1(49) -> 48
        , p_1(51) -> 48
        , p_1(51) -> 50
        , p_1(56) -> 55
        , p_1(58) -> 55
        , p_1(58) -> 57
        , p_1(59) -> 58
        , p_1(60) -> 59
        , p_2(9) -> 1
        , p_2(9) -> 10
        , p_2(14) -> 11
        , p_2(22) -> 58
        , p_2(23) -> 18
        , p_2(23) -> 20
        , p_2(23) -> 55
        , p_2(23) -> 57
        , p_2(28) -> 5
        , p_2(28) -> 25
        , p_2(28) -> 29
        , p_2(28) -> 33
        , p_2(32) -> 5
        , p_2(32) -> 25
        , p_2(32) -> 29
        , p_2(32) -> 33
        , p_2(37) -> 34
        , p_2(41) -> 6
        , p_2(41) -> 11
        , p_2(41) -> 15
        , p_2(41) -> 17
        , p_2(41) -> 54
        , p_2(41) -> 150
        , p_2(41) -> 154
        , p_2(50) -> 47
        , p_2(50) -> 133
        , p_2(50) -> 137
        , p_2(52) -> 47
        , p_2(52) -> 133
        , p_2(52) -> 137
        , p_2(61) -> 1
        , p_2(61) -> 10
        , p_2(61) -> 61
        , p_2(61) -> 65
        , p_2(61) -> 69
        , p_2(61) -> 77
        , p_2(61) -> 81
        , p_2(61) -> 91
        , p_2(61) -> 95
        , p_2(61) -> 102
        , p_2(61) -> 111
        , p_2(61) -> 128
        , p_2(61) -> 132
        , p_2(61) -> 139
        , p_2(61) -> 148
        , p_2(62) -> 1
        , p_2(62) -> 10
        , p_2(62) -> 61
        , p_2(63) -> 62
        , p_2(66) -> 1
        , p_2(66) -> 10
        , p_2(66) -> 61
        , p_2(66) -> 65
        , p_2(66) -> 69
        , p_2(66) -> 77
        , p_2(66) -> 81
        , p_2(66) -> 91
        , p_2(66) -> 95
        , p_2(66) -> 102
        , p_2(66) -> 111
        , p_2(66) -> 128
        , p_2(66) -> 132
        , p_2(66) -> 139
        , p_2(66) -> 148
        , p_2(67) -> 66
        , p_2(68) -> 1
        , p_2(68) -> 10
        , p_2(68) -> 61
        , p_2(68) -> 65
        , p_2(68) -> 69
        , p_2(68) -> 77
        , p_2(68) -> 81
        , p_2(68) -> 91
        , p_2(68) -> 95
        , p_2(68) -> 102
        , p_2(68) -> 111
        , p_2(68) -> 128
        , p_2(68) -> 132
        , p_2(68) -> 139
        , p_2(68) -> 148
        , p_2(71) -> 70
        , p_2(72) -> 71
        , p_2(75) -> 70
        , p_2(75) -> 74
        , p_2(78) -> 1
        , p_2(78) -> 10
        , p_2(78) -> 61
        , p_2(78) -> 65
        , p_2(78) -> 69
        , p_2(78) -> 77
        , p_2(78) -> 81
        , p_2(78) -> 91
        , p_2(78) -> 95
        , p_2(78) -> 102
        , p_2(78) -> 111
        , p_2(78) -> 128
        , p_2(78) -> 132
        , p_2(78) -> 139
        , p_2(78) -> 148
        , p_2(79) -> 78
        , p_2(80) -> 1
        , p_2(80) -> 10
        , p_2(80) -> 61
        , p_2(80) -> 65
        , p_2(80) -> 69
        , p_2(80) -> 77
        , p_2(80) -> 81
        , p_2(80) -> 91
        , p_2(80) -> 95
        , p_2(80) -> 102
        , p_2(80) -> 111
        , p_2(80) -> 128
        , p_2(80) -> 132
        , p_2(80) -> 139
        , p_2(80) -> 148
        , p_2(83) -> 82
        , p_2(84) -> 83
        , p_2(87) -> 82
        , p_2(87) -> 86
        , p_2(88) -> 1
        , p_2(88) -> 10
        , p_2(88) -> 61
        , p_2(88) -> 65
        , p_2(88) -> 69
        , p_2(88) -> 77
        , p_2(88) -> 81
        , p_2(88) -> 91
        , p_2(88) -> 95
        , p_2(88) -> 102
        , p_2(88) -> 111
        , p_2(88) -> 128
        , p_2(88) -> 132
        , p_2(88) -> 139
        , p_2(88) -> 148
        , p_2(89) -> 1
        , p_2(89) -> 10
        , p_2(89) -> 61
        , p_2(89) -> 65
        , p_2(89) -> 69
        , p_2(89) -> 77
        , p_2(89) -> 81
        , p_2(89) -> 88
        , p_2(89) -> 91
        , p_2(89) -> 95
        , p_2(89) -> 102
        , p_2(89) -> 111
        , p_2(89) -> 128
        , p_2(89) -> 132
        , p_2(89) -> 139
        , p_2(89) -> 148
        , p_2(92) -> 1
        , p_2(92) -> 10
        , p_2(92) -> 61
        , p_2(92) -> 65
        , p_2(92) -> 69
        , p_2(92) -> 77
        , p_2(92) -> 81
        , p_2(92) -> 91
        , p_2(92) -> 95
        , p_2(92) -> 102
        , p_2(92) -> 111
        , p_2(92) -> 128
        , p_2(92) -> 132
        , p_2(92) -> 139
        , p_2(92) -> 148
        , p_2(93) -> 92
        , p_2(94) -> 1
        , p_2(94) -> 10
        , p_2(94) -> 61
        , p_2(94) -> 65
        , p_2(94) -> 69
        , p_2(94) -> 77
        , p_2(94) -> 81
        , p_2(94) -> 91
        , p_2(94) -> 95
        , p_2(94) -> 102
        , p_2(94) -> 111
        , p_2(94) -> 128
        , p_2(94) -> 132
        , p_2(94) -> 139
        , p_2(94) -> 148
        , p_2(97) -> 96
        , p_2(98) -> 97
        , p_2(101) -> 96
        , p_2(101) -> 100
        , p_2(103) -> 1
        , p_2(103) -> 10
        , p_2(103) -> 61
        , p_2(103) -> 65
        , p_2(103) -> 69
        , p_2(103) -> 77
        , p_2(103) -> 81
        , p_2(103) -> 91
        , p_2(103) -> 95
        , p_2(103) -> 102
        , p_2(103) -> 111
        , p_2(103) -> 128
        , p_2(103) -> 132
        , p_2(103) -> 139
        , p_2(103) -> 148
        , p_2(104) -> 103
        , p_2(109) -> 1
        , p_2(109) -> 10
        , p_2(109) -> 61
        , p_2(109) -> 65
        , p_2(109) -> 69
        , p_2(109) -> 77
        , p_2(109) -> 81
        , p_2(109) -> 91
        , p_2(109) -> 95
        , p_2(109) -> 102
        , p_2(109) -> 111
        , p_2(109) -> 128
        , p_2(109) -> 132
        , p_2(109) -> 139
        , p_2(109) -> 148
        , p_2(114) -> 113
        , p_2(115) -> 114
        , p_2(118) -> 113
        , p_2(118) -> 117
        , p_2(125) -> 1
        , p_2(125) -> 10
        , p_2(125) -> 61
        , p_2(125) -> 65
        , p_2(125) -> 69
        , p_2(125) -> 77
        , p_2(125) -> 81
        , p_2(125) -> 91
        , p_2(125) -> 95
        , p_2(125) -> 102
        , p_2(125) -> 111
        , p_2(125) -> 128
        , p_2(125) -> 132
        , p_2(125) -> 139
        , p_2(125) -> 148
        , p_2(126) -> 1
        , p_2(126) -> 10
        , p_2(126) -> 61
        , p_2(126) -> 65
        , p_2(126) -> 69
        , p_2(126) -> 77
        , p_2(126) -> 81
        , p_2(126) -> 91
        , p_2(126) -> 95
        , p_2(126) -> 102
        , p_2(126) -> 111
        , p_2(126) -> 125
        , p_2(126) -> 128
        , p_2(126) -> 132
        , p_2(126) -> 139
        , p_2(126) -> 148
        , p_2(129) -> 1
        , p_2(129) -> 10
        , p_2(129) -> 61
        , p_2(129) -> 65
        , p_2(129) -> 69
        , p_2(129) -> 77
        , p_2(129) -> 81
        , p_2(129) -> 91
        , p_2(129) -> 95
        , p_2(129) -> 102
        , p_2(129) -> 111
        , p_2(129) -> 128
        , p_2(129) -> 132
        , p_2(129) -> 139
        , p_2(129) -> 148
        , p_2(130) -> 129
        , p_2(134) -> 133
        , p_2(135) -> 134
        , p_2(138) -> 133
        , p_2(138) -> 137
        , p_2(140) -> 1
        , p_2(140) -> 10
        , p_2(140) -> 61
        , p_2(140) -> 65
        , p_2(140) -> 69
        , p_2(140) -> 77
        , p_2(140) -> 81
        , p_2(140) -> 91
        , p_2(140) -> 95
        , p_2(140) -> 102
        , p_2(140) -> 111
        , p_2(140) -> 128
        , p_2(140) -> 132
        , p_2(140) -> 139
        , p_2(140) -> 148
        , p_2(141) -> 140
        , p_2(151) -> 150
        , p_2(152) -> 151
        , p_2(155) -> 150
        , p_2(155) -> 154
        , p_3(64) -> 1
        , p_3(64) -> 10
        , p_3(64) -> 61
        , p_3(65) -> 1
        , p_3(65) -> 10
        , p_3(65) -> 61
        , p_3(65) -> 65
        , p_3(65) -> 69
        , p_3(65) -> 77
        , p_3(65) -> 81
        , p_3(65) -> 91
        , p_3(65) -> 95
        , p_3(65) -> 102
        , p_3(65) -> 111
        , p_3(65) -> 128
        , p_3(65) -> 132
        , p_3(65) -> 139
        , p_3(65) -> 148
        , p_3(68) -> 1
        , p_3(68) -> 10
        , p_3(68) -> 61
        , p_3(68) -> 65
        , p_3(68) -> 69
        , p_3(68) -> 77
        , p_3(68) -> 81
        , p_3(68) -> 91
        , p_3(68) -> 95
        , p_3(68) -> 102
        , p_3(68) -> 111
        , p_3(68) -> 128
        , p_3(68) -> 132
        , p_3(68) -> 139
        , p_3(68) -> 148
        , p_3(69) -> 1
        , p_3(69) -> 10
        , p_3(69) -> 61
        , p_3(69) -> 65
        , p_3(69) -> 69
        , p_3(69) -> 77
        , p_3(69) -> 81
        , p_3(69) -> 91
        , p_3(69) -> 95
        , p_3(69) -> 102
        , p_3(69) -> 111
        , p_3(69) -> 128
        , p_3(69) -> 132
        , p_3(69) -> 139
        , p_3(69) -> 148
        , p_3(73) -> 70
        , p_3(76) -> 1
        , p_3(76) -> 10
        , p_3(76) -> 61
        , p_3(76) -> 65
        , p_3(76) -> 69
        , p_3(76) -> 77
        , p_3(76) -> 81
        , p_3(76) -> 91
        , p_3(76) -> 95
        , p_3(76) -> 102
        , p_3(76) -> 111
        , p_3(76) -> 128
        , p_3(76) -> 132
        , p_3(76) -> 139
        , p_3(76) -> 148
        , p_3(77) -> 1
        , p_3(77) -> 10
        , p_3(77) -> 61
        , p_3(77) -> 65
        , p_3(77) -> 69
        , p_3(77) -> 77
        , p_3(77) -> 81
        , p_3(77) -> 91
        , p_3(77) -> 95
        , p_3(77) -> 102
        , p_3(77) -> 111
        , p_3(77) -> 128
        , p_3(77) -> 132
        , p_3(77) -> 139
        , p_3(77) -> 148
        , p_3(80) -> 1
        , p_3(80) -> 10
        , p_3(80) -> 61
        , p_3(80) -> 65
        , p_3(80) -> 69
        , p_3(80) -> 77
        , p_3(80) -> 81
        , p_3(80) -> 91
        , p_3(80) -> 95
        , p_3(80) -> 102
        , p_3(80) -> 111
        , p_3(80) -> 128
        , p_3(80) -> 132
        , p_3(80) -> 139
        , p_3(80) -> 148
        , p_3(81) -> 1
        , p_3(81) -> 10
        , p_3(81) -> 61
        , p_3(81) -> 65
        , p_3(81) -> 69
        , p_3(81) -> 77
        , p_3(81) -> 81
        , p_3(81) -> 91
        , p_3(81) -> 95
        , p_3(81) -> 102
        , p_3(81) -> 111
        , p_3(81) -> 128
        , p_3(81) -> 132
        , p_3(81) -> 139
        , p_3(81) -> 148
        , p_3(85) -> 82
        , p_3(88) -> 1
        , p_3(88) -> 10
        , p_3(88) -> 61
        , p_3(88) -> 65
        , p_3(88) -> 69
        , p_3(88) -> 77
        , p_3(88) -> 81
        , p_3(88) -> 91
        , p_3(88) -> 95
        , p_3(88) -> 102
        , p_3(88) -> 111
        , p_3(88) -> 128
        , p_3(88) -> 132
        , p_3(88) -> 139
        , p_3(88) -> 148
        , p_3(90) -> 1
        , p_3(90) -> 10
        , p_3(90) -> 61
        , p_3(90) -> 65
        , p_3(90) -> 69
        , p_3(90) -> 77
        , p_3(90) -> 81
        , p_3(90) -> 91
        , p_3(90) -> 95
        , p_3(90) -> 102
        , p_3(90) -> 111
        , p_3(90) -> 128
        , p_3(90) -> 132
        , p_3(90) -> 139
        , p_3(90) -> 148
        , p_3(91) -> 1
        , p_3(91) -> 10
        , p_3(91) -> 61
        , p_3(91) -> 65
        , p_3(91) -> 69
        , p_3(91) -> 77
        , p_3(91) -> 81
        , p_3(91) -> 91
        , p_3(91) -> 95
        , p_3(91) -> 102
        , p_3(91) -> 111
        , p_3(91) -> 128
        , p_3(91) -> 132
        , p_3(91) -> 139
        , p_3(91) -> 148
        , p_3(94) -> 1
        , p_3(94) -> 10
        , p_3(94) -> 61
        , p_3(94) -> 65
        , p_3(94) -> 69
        , p_3(94) -> 77
        , p_3(94) -> 81
        , p_3(94) -> 91
        , p_3(94) -> 95
        , p_3(94) -> 102
        , p_3(94) -> 111
        , p_3(94) -> 128
        , p_3(94) -> 132
        , p_3(94) -> 139
        , p_3(94) -> 148
        , p_3(95) -> 1
        , p_3(95) -> 10
        , p_3(95) -> 61
        , p_3(95) -> 65
        , p_3(95) -> 69
        , p_3(95) -> 77
        , p_3(95) -> 81
        , p_3(95) -> 91
        , p_3(95) -> 95
        , p_3(95) -> 102
        , p_3(95) -> 111
        , p_3(95) -> 128
        , p_3(95) -> 132
        , p_3(95) -> 139
        , p_3(95) -> 148
        , p_3(99) -> 96
        , p_3(102) -> 1
        , p_3(102) -> 10
        , p_3(102) -> 61
        , p_3(102) -> 65
        , p_3(102) -> 69
        , p_3(102) -> 77
        , p_3(102) -> 81
        , p_3(102) -> 91
        , p_3(102) -> 95
        , p_3(102) -> 102
        , p_3(102) -> 111
        , p_3(102) -> 128
        , p_3(102) -> 132
        , p_3(102) -> 139
        , p_3(102) -> 148
        , p_3(109) -> 1
        , p_3(109) -> 10
        , p_3(109) -> 61
        , p_3(109) -> 65
        , p_3(109) -> 69
        , p_3(109) -> 77
        , p_3(109) -> 81
        , p_3(109) -> 91
        , p_3(109) -> 95
        , p_3(109) -> 102
        , p_3(109) -> 111
        , p_3(109) -> 128
        , p_3(109) -> 132
        , p_3(109) -> 139
        , p_3(109) -> 148
        , p_3(111) -> 1
        , p_3(111) -> 10
        , p_3(111) -> 61
        , p_3(111) -> 65
        , p_3(111) -> 69
        , p_3(111) -> 77
        , p_3(111) -> 81
        , p_3(111) -> 91
        , p_3(111) -> 95
        , p_3(111) -> 102
        , p_3(111) -> 111
        , p_3(111) -> 128
        , p_3(111) -> 132
        , p_3(111) -> 139
        , p_3(111) -> 148
        , p_3(116) -> 113
        , p_3(125) -> 1
        , p_3(125) -> 10
        , p_3(125) -> 61
        , p_3(125) -> 65
        , p_3(125) -> 69
        , p_3(125) -> 77
        , p_3(125) -> 81
        , p_3(125) -> 91
        , p_3(125) -> 95
        , p_3(125) -> 102
        , p_3(125) -> 111
        , p_3(125) -> 128
        , p_3(125) -> 132
        , p_3(125) -> 139
        , p_3(125) -> 148
        , p_3(127) -> 1
        , p_3(127) -> 10
        , p_3(127) -> 61
        , p_3(127) -> 65
        , p_3(127) -> 69
        , p_3(127) -> 77
        , p_3(127) -> 81
        , p_3(127) -> 91
        , p_3(127) -> 95
        , p_3(127) -> 102
        , p_3(127) -> 111
        , p_3(127) -> 128
        , p_3(127) -> 132
        , p_3(127) -> 139
        , p_3(127) -> 148
        , p_3(128) -> 1
        , p_3(128) -> 10
        , p_3(128) -> 61
        , p_3(128) -> 65
        , p_3(128) -> 69
        , p_3(128) -> 77
        , p_3(128) -> 81
        , p_3(128) -> 91
        , p_3(128) -> 95
        , p_3(128) -> 102
        , p_3(128) -> 111
        , p_3(128) -> 128
        , p_3(128) -> 132
        , p_3(128) -> 139
        , p_3(128) -> 148
        , p_3(131) -> 1
        , p_3(131) -> 10
        , p_3(131) -> 61
        , p_3(131) -> 65
        , p_3(131) -> 69
        , p_3(131) -> 77
        , p_3(131) -> 81
        , p_3(131) -> 91
        , p_3(131) -> 95
        , p_3(131) -> 102
        , p_3(131) -> 111
        , p_3(131) -> 128
        , p_3(131) -> 132
        , p_3(131) -> 139
        , p_3(131) -> 148
        , p_3(132) -> 1
        , p_3(132) -> 10
        , p_3(132) -> 61
        , p_3(132) -> 65
        , p_3(132) -> 69
        , p_3(132) -> 77
        , p_3(132) -> 81
        , p_3(132) -> 91
        , p_3(132) -> 95
        , p_3(132) -> 102
        , p_3(132) -> 111
        , p_3(132) -> 128
        , p_3(132) -> 132
        , p_3(132) -> 139
        , p_3(132) -> 148
        , p_3(136) -> 133
        , p_3(139) -> 1
        , p_3(139) -> 10
        , p_3(139) -> 61
        , p_3(139) -> 65
        , p_3(139) -> 69
        , p_3(139) -> 77
        , p_3(139) -> 81
        , p_3(139) -> 91
        , p_3(139) -> 95
        , p_3(139) -> 102
        , p_3(139) -> 111
        , p_3(139) -> 128
        , p_3(139) -> 132
        , p_3(139) -> 139
        , p_3(139) -> 148
        , p_3(146) -> 1
        , p_3(146) -> 10
        , p_3(146) -> 61
        , p_3(146) -> 65
        , p_3(146) -> 69
        , p_3(146) -> 77
        , p_3(146) -> 81
        , p_3(146) -> 91
        , p_3(146) -> 95
        , p_3(146) -> 102
        , p_3(146) -> 111
        , p_3(146) -> 128
        , p_3(146) -> 132
        , p_3(146) -> 139
        , p_3(146) -> 148
        , p_3(148) -> 1
        , p_3(148) -> 10
        , p_3(148) -> 61
        , p_3(148) -> 65
        , p_3(148) -> 69
        , p_3(148) -> 77
        , p_3(148) -> 81
        , p_3(148) -> 91
        , p_3(148) -> 95
        , p_3(148) -> 102
        , p_3(148) -> 111
        , p_3(148) -> 128
        , p_3(148) -> 132
        , p_3(148) -> 139
        , p_3(148) -> 148
        , p_3(153) -> 150
        , s_0(4) -> 2
        , s_0(4) -> 3
        , s_0(4) -> 4
        , s_0(4) -> 18
        , s_0(4) -> 20
        , s_0(4) -> 34
        , s_0(4) -> 38
        , s_0(4) -> 55
        , s_0(4) -> 57
        , s_1(4) -> 21
        , s_1(4) -> 23
        , s_1(4) -> 58
        , s_1(9) -> 8
        , s_1(10) -> 7
        , s_1(10) -> 9
        , s_1(14) -> 13
        , s_1(15) -> 12
        , s_1(15) -> 14
        , s_1(17) -> 16
        , s_1(20) -> 19
        , s_1(22) -> 60
        , s_1(23) -> 22
        , s_1(23) -> 59
        , s_1(25) -> 24
        , s_1(26) -> 24
        , s_1(28) -> 27
        , s_1(29) -> 5
        , s_1(29) -> 25
        , s_1(29) -> 26
        , s_1(29) -> 28
        , s_1(29) -> 29
        , s_1(29) -> 33
        , s_1(32) -> 31
        , s_1(33) -> 30
        , s_1(33) -> 32
        , s_1(37) -> 36
        , s_1(38) -> 35
        , s_1(38) -> 37
        , s_1(41) -> 40
        , s_1(42) -> 39
        , s_1(42) -> 41
        , s_1(43) -> 6
        , s_1(43) -> 11
        , s_1(43) -> 15
        , s_1(43) -> 17
        , s_1(43) -> 42
        , s_1(43) -> 54
        , s_1(43) -> 150
        , s_1(43) -> 154
        , s_1(44) -> 43
        , s_1(44) -> 70
        , s_1(44) -> 74
        , s_1(45) -> 44
        , s_1(45) -> 82
        , s_1(45) -> 86
        , s_1(46) -> 45
        , s_1(46) -> 96
        , s_1(46) -> 100
        , s_1(47) -> 46
        , s_1(47) -> 113
        , s_1(47) -> 117
        , s_1(50) -> 49
        , s_1(52) -> 51
        , s_1(53) -> 48
        , s_1(53) -> 50
        , s_1(53) -> 52
        , s_1(54) -> 47
        , s_1(54) -> 53
        , s_1(54) -> 133
        , s_1(54) -> 137
        , s_1(57) -> 56
        , s_2(43) -> 75
        , s_2(44) -> 87
        , s_2(45) -> 101
        , s_2(46) -> 118
        , s_2(47) -> 138
        , s_2(54) -> 155
        , s_2(61) -> 7
        , s_2(61) -> 9
        , s_2(64) -> 63
        , s_2(65) -> 62
        , s_2(65) -> 64
        , s_2(68) -> 67
        , s_2(69) -> 66
        , s_2(69) -> 68
        , s_2(73) -> 72
        , s_2(74) -> 71
        , s_2(74) -> 73
        , s_2(76) -> 62
        , s_2(77) -> 1
        , s_2(77) -> 10
        , s_2(77) -> 61
        , s_2(77) -> 76
        , s_2(80) -> 79
        , s_2(81) -> 78
        , s_2(81) -> 80
        , s_2(85) -> 84
        , s_2(86) -> 83
        , s_2(86) -> 85
        , s_2(88) -> 66
        , s_2(90) -> 89
        , s_2(91) -> 1
        , s_2(91) -> 10
        , s_2(91) -> 61
        , s_2(91) -> 65
        , s_2(91) -> 69
        , s_2(91) -> 77
        , s_2(91) -> 81
        , s_2(91) -> 88
        , s_2(91) -> 90
        , s_2(91) -> 91
        , s_2(91) -> 95
        , s_2(91) -> 102
        , s_2(91) -> 111
        , s_2(91) -> 128
        , s_2(91) -> 132
        , s_2(91) -> 139
        , s_2(91) -> 148
        , s_2(94) -> 93
        , s_2(95) -> 92
        , s_2(95) -> 94
        , s_2(99) -> 98
        , s_2(100) -> 97
        , s_2(100) -> 99
        , s_2(102) -> 1
        , s_2(102) -> 10
        , s_2(102) -> 61
        , s_2(102) -> 65
        , s_2(102) -> 69
        , s_2(102) -> 77
        , s_2(102) -> 81
        , s_2(102) -> 91
        , s_2(102) -> 95
        , s_2(102) -> 102
        , s_2(102) -> 111
        , s_2(102) -> 128
        , s_2(102) -> 132
        , s_2(102) -> 139
        , s_2(102) -> 148
        , s_2(109) -> 104
        , s_2(111) -> 103
        , s_2(111) -> 109
        , s_2(116) -> 115
        , s_2(117) -> 114
        , s_2(117) -> 116
        , s_2(125) -> 66
        , s_2(125) -> 68
        , s_2(127) -> 126
        , s_2(128) -> 1
        , s_2(128) -> 10
        , s_2(128) -> 61
        , s_2(128) -> 65
        , s_2(128) -> 69
        , s_2(128) -> 77
        , s_2(128) -> 81
        , s_2(128) -> 91
        , s_2(128) -> 95
        , s_2(128) -> 102
        , s_2(128) -> 111
        , s_2(128) -> 125
        , s_2(128) -> 127
        , s_2(128) -> 128
        , s_2(128) -> 132
        , s_2(128) -> 139
        , s_2(128) -> 148
        , s_2(131) -> 130
        , s_2(132) -> 129
        , s_2(132) -> 131
        , s_2(136) -> 135
        , s_2(137) -> 134
        , s_2(137) -> 136
        , s_2(139) -> 1
        , s_2(139) -> 10
        , s_2(139) -> 61
        , s_2(139) -> 65
        , s_2(139) -> 69
        , s_2(139) -> 77
        , s_2(139) -> 81
        , s_2(139) -> 91
        , s_2(139) -> 95
        , s_2(139) -> 102
        , s_2(139) -> 111
        , s_2(139) -> 128
        , s_2(139) -> 132
        , s_2(139) -> 139
        , s_2(139) -> 148
        , s_2(146) -> 141
        , s_2(148) -> 140
        , s_2(148) -> 146
        , s_2(153) -> 152
        , s_2(154) -> 151
        , s_2(154) -> 153
        , half_0(4) -> 5
        , half_1(11) -> 1
        , half_1(11) -> 10
        , half_1(34) -> 5
        , half_1(34) -> 25
        , half_1(34) -> 29
        , half_1(34) -> 33
        , half_2(70) -> 1
        , half_2(70) -> 10
        , half_2(70) -> 61
        , half_2(70) -> 65
        , half_2(70) -> 69
        , half_2(70) -> 77
        , half_2(70) -> 81
        , half_2(70) -> 91
        , half_2(70) -> 95
        , half_2(70) -> 102
        , half_2(70) -> 111
        , half_2(70) -> 128
        , half_2(70) -> 132
        , half_2(70) -> 139
        , half_2(70) -> 148
        , half_2(82) -> 1
        , half_2(82) -> 10
        , half_2(82) -> 61
        , half_2(82) -> 65
        , half_2(82) -> 69
        , half_2(82) -> 77
        , half_2(82) -> 81
        , half_2(82) -> 91
        , half_2(82) -> 95
        , half_2(82) -> 102
        , half_2(82) -> 111
        , half_2(82) -> 128
        , half_2(82) -> 132
        , half_2(82) -> 139
        , half_2(82) -> 148
        , half_2(96) -> 1
        , half_2(96) -> 10
        , half_2(96) -> 61
        , half_2(96) -> 65
        , half_2(96) -> 69
        , half_2(96) -> 77
        , half_2(96) -> 81
        , half_2(96) -> 91
        , half_2(96) -> 95
        , half_2(96) -> 102
        , half_2(96) -> 111
        , half_2(96) -> 128
        , half_2(96) -> 132
        , half_2(96) -> 139
        , half_2(96) -> 148
        , half_2(113) -> 1
        , half_2(113) -> 10
        , half_2(113) -> 61
        , half_2(113) -> 65
        , half_2(113) -> 69
        , half_2(113) -> 77
        , half_2(113) -> 81
        , half_2(113) -> 91
        , half_2(113) -> 95
        , half_2(113) -> 102
        , half_2(113) -> 111
        , half_2(113) -> 128
        , half_2(113) -> 132
        , half_2(113) -> 139
        , half_2(113) -> 148
        , half_2(133) -> 1
        , half_2(133) -> 10
        , half_2(133) -> 61
        , half_2(133) -> 65
        , half_2(133) -> 69
        , half_2(133) -> 77
        , half_2(133) -> 81
        , half_2(133) -> 91
        , half_2(133) -> 95
        , half_2(133) -> 102
        , half_2(133) -> 111
        , half_2(133) -> 128
        , half_2(133) -> 132
        , half_2(133) -> 139
        , half_2(133) -> 148
        , half_2(150) -> 1
        , half_2(150) -> 10
        , half_2(150) -> 61
        , half_2(150) -> 65
        , half_2(150) -> 69
        , half_2(150) -> 77
        , half_2(150) -> 81
        , half_2(150) -> 91
        , half_2(150) -> 95
        , half_2(150) -> 102
        , half_2(150) -> 111
        , half_2(150) -> 128
        , half_2(150) -> 132
        , half_2(150) -> 139
        , half_2(150) -> 148
        , sixtimes_0(4) -> 6
        , sixtimes_1(18) -> 11
        , sixtimes_1(18) -> 15
        , sixtimes_1(18) -> 17
        , sixtimes_1(55) -> 54
        , sixtimes_1(55) -> 150
        , sixtimes_1(55) -> 154}