Problem Secret 06 SRS aprove07

Tool CaT

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

stdout:

YES(?,O(n^1))

Problem:
 foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1))))))))))
 foo(s(x1)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
 bar(0(x1)) -> 0(p(s(s(s(x1)))))
 bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
 p(p(s(x1))) -> p(x1)
 p(s(x1)) -> x1
 p(0(x1)) -> 0(s(s(s(s(x1)))))

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {5,4,3}
   transitions:
    02(223) -> 224*
    01(15) -> 16*
    01(114) -> 115*
    01(86) -> 87*
    03(247) -> 248*
    s1(45) -> 46*
    s1(35) -> 36*
    s1(30) -> 31*
    s1(10) -> 11*
    s1(92) -> 93*
    s1(52) -> 53*
    s1(47) -> 48*
    s1(42) -> 43*
    s1(37) -> 38*
    s1(84) -> 85*
    s1(44) -> 45*
    s1(14) -> 15*
    s1(9) -> 10*
    s1(96) -> 97*
    s1(6) -> 7*
    s1(113) -> 114*
    s1(93) -> 94*
    s1(83) -> 84*
    s1(48) -> 49*
    s1(38) -> 39*
    s1(8) -> 9*
    s1(90) -> 91*
    s3(242) -> 243*
    s3(264) -> 265*
    s3(246) -> 247*
    s3(241) -> 242*
    s3(238) -> 239*
    s3(240) -> 241*
    p1(50) -> 51*
    p1(40) -> 41*
    p1(97) -> 98*
    p1(32) -> 33*
    p1(12) -> 13*
    p1(7) -> 8*
    p1(94) -> 95*
    p1(89) -> 90*
    p1(49) -> 50*
    p1(39) -> 40*
    p1(51) -> 52*
    p1(46) -> 47*
    p1(36) -> 37*
    p1(11) -> 12*
    p1(88) -> 89*
    p1(53) -> 54*
    p1(43) -> 44*
    p1(33) -> 34*
    p1(13) -> 14*
    p1(95) -> 96*
    p1(85) -> 86*
    p4(266) -> 267*
    p4(270) -> 271*
    foo1(91) -> 92*
    foo1(41) -> 42*
    bar1(34) -> 35*
    p2(182) -> 183*
    p2(172) -> 173*
    p2(137) -> 138*
    p2(127) -> 128*
    p2(117) -> 118*
    p2(219) -> 220*
    p2(174) -> 175*
    p2(139) -> 140*
    p2(134) -> 135*
    p2(124) -> 125*
    p2(221) -> 222*
    p2(141) -> 142*
    p2(131) -> 132*
    p2(121) -> 122*
    p2(188) -> 189*
    p2(138) -> 139*
    p2(128) -> 129*
    p2(220) -> 221*
    p2(215) -> 216*
    p2(200) -> 201*
    p2(190) -> 191*
    p2(180) -> 181*
    p2(120) -> 121*
    foo0(2) -> 3*
    foo0(1) -> 3*
    s2(222) -> 223*
    s2(217) -> 218*
    s2(132) -> 133*
    s2(214) -> 215*
    s2(119) -> 120*
    s2(216) -> 217*
    s2(136) -> 137*
    s2(126) -> 127*
    s2(116) -> 117*
    s2(218) -> 219*
    s2(133) -> 134*
    s2(123) -> 124*
    s2(118) -> 119*
    s2(140) -> 141*
    s2(135) -> 136*
    s2(130) -> 131*
    s2(125) -> 126*
    00(2) -> 1*
    00(1) -> 1*
    foo2(129) -> 130*
    s0(2) -> 2*
    s0(1) -> 2*
    bar2(122) -> 123*
    p0(2) -> 5*
    p0(1) -> 5*
    p3(262) -> 263*
    p3(244) -> 245*
    p3(239) -> 240*
    p3(204) -> 205*
    p3(194) -> 195*
    p3(236) -> 237*
    p3(206) -> 207*
    p3(243) -> 244*
    p3(245) -> 246*
    p3(210) -> 211*
    bar0(2) -> 4*
    bar0(1) -> 4*
    1 -> 5,30
    2 -> 5,6
    6 -> 175,8
    7 -> 83*
    8 -> 183,34
    9 -> 189,33,182
    10 -> 12,188,32
    16 -> 3*
    30 -> 175,8
    31 -> 7*
    35 -> 37*
    37 -> 123,125,205,173
    38 -> 40,172
    41 -> 35*
    42 -> 44*
    44 -> 201*
    45 -> 47*
    47 -> 191,51,200
    48 -> 50,190
    52 -> 54*
    54 -> 3*
    83 -> 89,174
    84 -> 86,88
    85 -> 113*
    86 -> 214*
    87 -> 123,125,205,35,37,41,4
    90 -> 116*
    92 -> 181*
    93 -> 95,180
    96 -> 98,4
    98 -> 37,41,4
    115 -> 5*
    116 -> 118*
    118 -> 207,122
    119 -> 121,206
    123 -> 125*
    125 -> 205,129
    126 -> 128,204
    130 -> 132*
    132 -> 211,140,142
    133 -> 135*
    135 -> 195,210
    136 -> 138,194
    140 -> 142,92
    142 -> 92*
    173 -> 41*
    175 -> 90*
    181 -> 96*
    183 -> 14,34
    189 -> 13*
    191 -> 51*
    195 -> 139*
    201 -> 52*
    205 -> 129*
    207 -> 122*
    211 -> 140,142,96
    214 -> 216*
    216 -> 263,222
    217 -> 237,221,262
    218 -> 220,236
    223 -> 238*
    224 -> 130,132,140,181,98,37,123,129,42,44,52,3
    237 -> 221*
    238 -> 240*
    240 -> 271*
    241 -> 267,245,270
    242 -> 244,266
    247 -> 264*
    248 -> 130,42,44,52,3,132,140,181,98,37,123,129
    263 -> 222*
    264 -> 240*
    265 -> 239*
    267 -> 245*
    271 -> 246*
  problem:
   
  Qed

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputSecret 06 SRS aprove07

stdout:

MAYBE

Tool IRC2

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

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:
    {  foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1))))))))))
     , foo(s(x1)) ->
       p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
     , bar(0(x1)) -> 0(p(s(s(s(x1)))))
     , bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
     , p(p(s(x1))) -> p(x1)
     , p(s(x1)) -> x1
     , p(0(x1)) -> 0(s(s(s(s(x1)))))}

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:
         {  foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1))))))))))
          , foo(s(x1)) ->
            p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
          , bar(0(x1)) -> 0(p(s(s(s(x1)))))
          , bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
          , p(p(s(x1))) -> p(x1)
          , p(s(x1)) -> x1
          , p(0(x1)) -> 0(s(s(s(s(x1)))))}
     
     Proof Output:    
       The problem is match-bounded by 4.
       The enriched problem is compatible with the following automaton:
       {  foo_0(2) -> 1
        , foo_1(24) -> 1
        , foo_1(24) -> 13
        , foo_1(24) -> 21
        , foo_1(24) -> 23
        , foo_1(24) -> 24
        , foo_1(24) -> 28
        , foo_1(24) -> 30
        , foo_1(24) -> 51
        , foo_1(24) -> 55
        , foo_1(24) -> 57
        , foo_1(37) -> 1
        , foo_1(37) -> 13
        , foo_1(37) -> 24
        , foo_1(37) -> 28
        , foo_1(37) -> 30
        , foo_1(37) -> 36
        , foo_1(37) -> 51
        , foo_1(37) -> 55
        , foo_1(37) -> 57
        , foo_2(51) -> 1
        , foo_2(51) -> 13
        , foo_2(51) -> 24
        , foo_2(51) -> 28
        , foo_2(51) -> 30
        , foo_2(51) -> 36
        , foo_2(51) -> 40
        , foo_2(51) -> 48
        , foo_2(51) -> 50
        , foo_2(51) -> 51
        , foo_2(51) -> 55
        , foo_2(51) -> 57
        , 0_0(2) -> 1
        , 0_0(2) -> 2
        , 0_0(2) -> 4
        , 0_0(2) -> 10
        , 0_0(2) -> 31
        , 0_0(2) -> 38
        , 0_0(2) -> 58
        , 0_0(2) -> 62
        , 0_1(3) -> 1
        , 0_1(3) -> 24
        , 0_1(3) -> 28
        , 0_1(3) -> 30
        , 0_1(3) -> 51
        , 0_1(3) -> 55
        , 0_1(3) -> 57
        , 0_2(64) -> 1
        , 0_2(64) -> 13
        , 0_2(64) -> 21
        , 0_2(64) -> 23
        , 0_2(64) -> 24
        , 0_2(64) -> 28
        , 0_2(64) -> 30
        , 0_2(64) -> 36
        , 0_2(64) -> 40
        , 0_2(64) -> 48
        , 0_2(64) -> 50
        , 0_2(64) -> 51
        , 0_2(64) -> 55
        , 0_2(64) -> 57
        , 0_3(73) -> 1
        , 0_3(73) -> 13
        , 0_3(73) -> 24
        , 0_3(73) -> 28
        , 0_3(73) -> 30
        , 0_3(73) -> 36
        , 0_3(73) -> 40
        , 0_3(73) -> 48
        , 0_3(73) -> 50
        , 0_3(73) -> 51
        , 0_3(73) -> 55
        , 0_3(73) -> 57
        , s_0(2) -> 1
        , s_0(2) -> 2
        , s_0(2) -> 4
        , s_0(2) -> 10
        , s_0(2) -> 31
        , s_0(2) -> 38
        , s_0(2) -> 58
        , s_0(2) -> 62
        , s_1(2) -> 11
        , s_1(2) -> 39
        , s_1(4) -> 3
        , s_1(4) -> 65
        , s_1(4) -> 71
        , s_1(8) -> 7
        , s_1(9) -> 6
        , s_1(9) -> 8
        , s_1(10) -> 5
        , s_1(10) -> 9
        , s_1(10) -> 32
        , s_1(11) -> 3
        , s_1(11) -> 34
        , s_1(11) -> 65
        , s_1(11) -> 71
        , s_1(13) -> 12
        , s_1(17) -> 16
        , s_1(18) -> 15
        , s_1(18) -> 17
        , s_1(20) -> 19
        , s_1(21) -> 14
        , s_1(21) -> 18
        , s_1(21) -> 20
        , s_1(23) -> 22
        , s_1(27) -> 26
        , s_1(28) -> 25
        , s_1(28) -> 27
        , s_1(30) -> 29
        , s_1(33) -> 3
        , s_1(33) -> 65
        , s_1(33) -> 71
        , s_1(34) -> 33
        , s_1(35) -> 15
        , s_1(36) -> 14
        , s_1(36) -> 35
        , s_1(38) -> 37
        , s_2(3) -> 72
        , s_2(38) -> 63
        , s_2(40) -> 14
        , s_2(40) -> 35
        , s_2(44) -> 43
        , s_2(45) -> 42
        , s_2(45) -> 44
        , s_2(47) -> 46
        , s_2(48) -> 41
        , s_2(48) -> 45
        , s_2(48) -> 47
        , s_2(50) -> 49
        , s_2(54) -> 53
        , s_2(55) -> 52
        , s_2(55) -> 54
        , s_2(57) -> 56
        , s_2(61) -> 60
        , s_2(62) -> 59
        , s_2(62) -> 61
        , s_2(64) -> 72
        , s_2(65) -> 64
        , s_2(65) -> 65
        , s_2(65) -> 71
        , s_2(65) -> 74
        , s_2(65) -> 80
        , s_2(69) -> 68
        , s_2(70) -> 67
        , s_2(70) -> 69
        , s_2(71) -> 66
        , s_2(71) -> 70
        , s_2(73) -> 72
        , s_3(64) -> 81
        , s_3(73) -> 81
        , s_3(74) -> 65
        , s_3(74) -> 71
        , s_3(74) -> 73
        , s_3(74) -> 74
        , s_3(74) -> 80
        , s_3(78) -> 77
        , s_3(79) -> 76
        , s_3(79) -> 78
        , s_3(80) -> 75
        , s_3(80) -> 79
        , p_0(2) -> 1
        , p_1(5) -> 4
        , p_1(6) -> 5
        , p_1(7) -> 6
        , p_1(8) -> 32
        , p_1(11) -> 4
        , p_1(11) -> 10
        , p_1(11) -> 31
        , p_1(12) -> 1
        , p_1(12) -> 24
        , p_1(12) -> 28
        , p_1(12) -> 30
        , p_1(12) -> 51
        , p_1(12) -> 55
        , p_1(12) -> 57
        , p_1(14) -> 1
        , p_1(14) -> 13
        , p_1(14) -> 24
        , p_1(14) -> 28
        , p_1(14) -> 30
        , p_1(14) -> 51
        , p_1(14) -> 55
        , p_1(14) -> 57
        , p_1(15) -> 14
        , p_1(16) -> 15
        , p_1(19) -> 14
        , p_1(19) -> 18
        , p_1(22) -> 1
        , p_1(22) -> 13
        , p_1(22) -> 21
        , p_1(22) -> 24
        , p_1(22) -> 28
        , p_1(22) -> 30
        , p_1(22) -> 51
        , p_1(22) -> 55
        , p_1(22) -> 57
        , p_1(25) -> 24
        , p_1(26) -> 25
        , p_1(29) -> 24
        , p_1(29) -> 28
        , p_1(29) -> 51
        , p_1(29) -> 55
        , p_1(29) -> 57
        , p_1(32) -> 31
        , p_1(33) -> 3
        , p_1(33) -> 65
        , p_1(33) -> 71
        , p_1(34) -> 39
        , p_1(39) -> 38
        , p_1(39) -> 58
        , p_1(39) -> 62
        , p_2(8) -> 5
        , p_2(9) -> 4
        , p_2(9) -> 31
        , p_2(11) -> 38
        , p_2(11) -> 58
        , p_2(11) -> 62
        , p_2(17) -> 14
        , p_2(18) -> 1
        , p_2(18) -> 13
        , p_2(18) -> 24
        , p_2(18) -> 28
        , p_2(18) -> 30
        , p_2(18) -> 51
        , p_2(18) -> 55
        , p_2(18) -> 57
        , p_2(20) -> 1
        , p_2(20) -> 13
        , p_2(20) -> 24
        , p_2(20) -> 28
        , p_2(20) -> 30
        , p_2(20) -> 51
        , p_2(20) -> 55
        , p_2(20) -> 57
        , p_2(27) -> 24
        , p_2(35) -> 1
        , p_2(35) -> 13
        , p_2(35) -> 24
        , p_2(35) -> 28
        , p_2(35) -> 30
        , p_2(35) -> 36
        , p_2(35) -> 51
        , p_2(35) -> 55
        , p_2(35) -> 57
        , p_2(41) -> 1
        , p_2(41) -> 13
        , p_2(41) -> 24
        , p_2(41) -> 28
        , p_2(41) -> 30
        , p_2(41) -> 36
        , p_2(41) -> 40
        , p_2(41) -> 51
        , p_2(41) -> 55
        , p_2(41) -> 57
        , p_2(42) -> 41
        , p_2(43) -> 42
        , p_2(46) -> 41
        , p_2(46) -> 45
        , p_2(49) -> 1
        , p_2(49) -> 13
        , p_2(49) -> 24
        , p_2(49) -> 28
        , p_2(49) -> 30
        , p_2(49) -> 36
        , p_2(49) -> 40
        , p_2(49) -> 48
        , p_2(49) -> 51
        , p_2(49) -> 55
        , p_2(49) -> 57
        , p_2(52) -> 51
        , p_2(53) -> 52
        , p_2(56) -> 51
        , p_2(56) -> 55
        , p_2(59) -> 58
        , p_2(60) -> 59
        , p_2(63) -> 58
        , p_2(63) -> 62
        , p_2(66) -> 65
        , p_2(67) -> 66
        , p_2(68) -> 67
        , p_2(72) -> 65
        , p_2(72) -> 71
        , p_3(44) -> 41
        , p_3(45) -> 1
        , p_3(45) -> 13
        , p_3(45) -> 24
        , p_3(45) -> 28
        , p_3(45) -> 30
        , p_3(45) -> 36
        , p_3(45) -> 40
        , p_3(45) -> 51
        , p_3(45) -> 55
        , p_3(45) -> 57
        , p_3(47) -> 1
        , p_3(47) -> 13
        , p_3(47) -> 24
        , p_3(47) -> 28
        , p_3(47) -> 30
        , p_3(47) -> 36
        , p_3(47) -> 40
        , p_3(47) -> 51
        , p_3(47) -> 55
        , p_3(47) -> 57
        , p_3(54) -> 51
        , p_3(61) -> 58
        , p_3(69) -> 66
        , p_3(70) -> 65
        , p_3(75) -> 74
        , p_3(76) -> 75
        , p_3(77) -> 76
        , p_3(81) -> 74
        , p_3(81) -> 80
        , p_4(78) -> 75
        , p_4(79) -> 74
        , bar_0(2) -> 1
        , bar_1(31) -> 24
        , bar_1(31) -> 28
        , bar_1(31) -> 30
        , bar_1(31) -> 51
        , bar_1(31) -> 55
        , bar_1(31) -> 57
        , bar_2(58) -> 51
        , bar_2(58) -> 55
        , bar_2(58) -> 57}

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputSecret 06 SRS aprove07

stdout:

MAYBE

Tool RC2

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

stdout:

YES(?,O(n^1))

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

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:
         {  foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1))))))))))
          , foo(s(x1)) ->
            p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
          , bar(0(x1)) -> 0(p(s(s(s(x1)))))
          , bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
          , p(p(s(x1))) -> p(x1)
          , p(s(x1)) -> x1
          , p(0(x1)) -> 0(s(s(s(s(x1)))))}
     
     Proof Output:    
       The problem is match-bounded by 4.
       The enriched problem is compatible with the following automaton:
       {  foo_0(2) -> 1
        , foo_1(24) -> 1
        , foo_1(24) -> 13
        , foo_1(24) -> 21
        , foo_1(24) -> 23
        , foo_1(24) -> 24
        , foo_1(24) -> 28
        , foo_1(24) -> 30
        , foo_1(24) -> 51
        , foo_1(24) -> 55
        , foo_1(24) -> 57
        , foo_1(37) -> 1
        , foo_1(37) -> 13
        , foo_1(37) -> 24
        , foo_1(37) -> 28
        , foo_1(37) -> 30
        , foo_1(37) -> 36
        , foo_1(37) -> 51
        , foo_1(37) -> 55
        , foo_1(37) -> 57
        , foo_2(51) -> 1
        , foo_2(51) -> 13
        , foo_2(51) -> 24
        , foo_2(51) -> 28
        , foo_2(51) -> 30
        , foo_2(51) -> 36
        , foo_2(51) -> 40
        , foo_2(51) -> 48
        , foo_2(51) -> 50
        , foo_2(51) -> 51
        , foo_2(51) -> 55
        , foo_2(51) -> 57
        , 0_0(2) -> 1
        , 0_0(2) -> 2
        , 0_0(2) -> 4
        , 0_0(2) -> 10
        , 0_0(2) -> 31
        , 0_0(2) -> 38
        , 0_0(2) -> 58
        , 0_0(2) -> 62
        , 0_1(3) -> 1
        , 0_1(3) -> 24
        , 0_1(3) -> 28
        , 0_1(3) -> 30
        , 0_1(3) -> 51
        , 0_1(3) -> 55
        , 0_1(3) -> 57
        , 0_2(64) -> 1
        , 0_2(64) -> 13
        , 0_2(64) -> 21
        , 0_2(64) -> 23
        , 0_2(64) -> 24
        , 0_2(64) -> 28
        , 0_2(64) -> 30
        , 0_2(64) -> 36
        , 0_2(64) -> 40
        , 0_2(64) -> 48
        , 0_2(64) -> 50
        , 0_2(64) -> 51
        , 0_2(64) -> 55
        , 0_2(64) -> 57
        , 0_3(73) -> 1
        , 0_3(73) -> 13
        , 0_3(73) -> 24
        , 0_3(73) -> 28
        , 0_3(73) -> 30
        , 0_3(73) -> 36
        , 0_3(73) -> 40
        , 0_3(73) -> 48
        , 0_3(73) -> 50
        , 0_3(73) -> 51
        , 0_3(73) -> 55
        , 0_3(73) -> 57
        , s_0(2) -> 1
        , s_0(2) -> 2
        , s_0(2) -> 4
        , s_0(2) -> 10
        , s_0(2) -> 31
        , s_0(2) -> 38
        , s_0(2) -> 58
        , s_0(2) -> 62
        , s_1(2) -> 11
        , s_1(2) -> 39
        , s_1(4) -> 3
        , s_1(4) -> 65
        , s_1(4) -> 71
        , s_1(8) -> 7
        , s_1(9) -> 6
        , s_1(9) -> 8
        , s_1(10) -> 5
        , s_1(10) -> 9
        , s_1(10) -> 32
        , s_1(11) -> 3
        , s_1(11) -> 34
        , s_1(11) -> 65
        , s_1(11) -> 71
        , s_1(13) -> 12
        , s_1(17) -> 16
        , s_1(18) -> 15
        , s_1(18) -> 17
        , s_1(20) -> 19
        , s_1(21) -> 14
        , s_1(21) -> 18
        , s_1(21) -> 20
        , s_1(23) -> 22
        , s_1(27) -> 26
        , s_1(28) -> 25
        , s_1(28) -> 27
        , s_1(30) -> 29
        , s_1(33) -> 3
        , s_1(33) -> 65
        , s_1(33) -> 71
        , s_1(34) -> 33
        , s_1(35) -> 15
        , s_1(36) -> 14
        , s_1(36) -> 35
        , s_1(38) -> 37
        , s_2(3) -> 72
        , s_2(38) -> 63
        , s_2(40) -> 14
        , s_2(40) -> 35
        , s_2(44) -> 43
        , s_2(45) -> 42
        , s_2(45) -> 44
        , s_2(47) -> 46
        , s_2(48) -> 41
        , s_2(48) -> 45
        , s_2(48) -> 47
        , s_2(50) -> 49
        , s_2(54) -> 53
        , s_2(55) -> 52
        , s_2(55) -> 54
        , s_2(57) -> 56
        , s_2(61) -> 60
        , s_2(62) -> 59
        , s_2(62) -> 61
        , s_2(64) -> 72
        , s_2(65) -> 64
        , s_2(65) -> 65
        , s_2(65) -> 71
        , s_2(65) -> 74
        , s_2(65) -> 80
        , s_2(69) -> 68
        , s_2(70) -> 67
        , s_2(70) -> 69
        , s_2(71) -> 66
        , s_2(71) -> 70
        , s_2(73) -> 72
        , s_3(64) -> 81
        , s_3(73) -> 81
        , s_3(74) -> 65
        , s_3(74) -> 71
        , s_3(74) -> 73
        , s_3(74) -> 74
        , s_3(74) -> 80
        , s_3(78) -> 77
        , s_3(79) -> 76
        , s_3(79) -> 78
        , s_3(80) -> 75
        , s_3(80) -> 79
        , p_0(2) -> 1
        , p_1(5) -> 4
        , p_1(6) -> 5
        , p_1(7) -> 6
        , p_1(8) -> 32
        , p_1(11) -> 4
        , p_1(11) -> 10
        , p_1(11) -> 31
        , p_1(12) -> 1
        , p_1(12) -> 24
        , p_1(12) -> 28
        , p_1(12) -> 30
        , p_1(12) -> 51
        , p_1(12) -> 55
        , p_1(12) -> 57
        , p_1(14) -> 1
        , p_1(14) -> 13
        , p_1(14) -> 24
        , p_1(14) -> 28
        , p_1(14) -> 30
        , p_1(14) -> 51
        , p_1(14) -> 55
        , p_1(14) -> 57
        , p_1(15) -> 14
        , p_1(16) -> 15
        , p_1(19) -> 14
        , p_1(19) -> 18
        , p_1(22) -> 1
        , p_1(22) -> 13
        , p_1(22) -> 21
        , p_1(22) -> 24
        , p_1(22) -> 28
        , p_1(22) -> 30
        , p_1(22) -> 51
        , p_1(22) -> 55
        , p_1(22) -> 57
        , p_1(25) -> 24
        , p_1(26) -> 25
        , p_1(29) -> 24
        , p_1(29) -> 28
        , p_1(29) -> 51
        , p_1(29) -> 55
        , p_1(29) -> 57
        , p_1(32) -> 31
        , p_1(33) -> 3
        , p_1(33) -> 65
        , p_1(33) -> 71
        , p_1(34) -> 39
        , p_1(39) -> 38
        , p_1(39) -> 58
        , p_1(39) -> 62
        , p_2(8) -> 5
        , p_2(9) -> 4
        , p_2(9) -> 31
        , p_2(11) -> 38
        , p_2(11) -> 58
        , p_2(11) -> 62
        , p_2(17) -> 14
        , p_2(18) -> 1
        , p_2(18) -> 13
        , p_2(18) -> 24
        , p_2(18) -> 28
        , p_2(18) -> 30
        , p_2(18) -> 51
        , p_2(18) -> 55
        , p_2(18) -> 57
        , p_2(20) -> 1
        , p_2(20) -> 13
        , p_2(20) -> 24
        , p_2(20) -> 28
        , p_2(20) -> 30
        , p_2(20) -> 51
        , p_2(20) -> 55
        , p_2(20) -> 57
        , p_2(27) -> 24
        , p_2(35) -> 1
        , p_2(35) -> 13
        , p_2(35) -> 24
        , p_2(35) -> 28
        , p_2(35) -> 30
        , p_2(35) -> 36
        , p_2(35) -> 51
        , p_2(35) -> 55
        , p_2(35) -> 57
        , p_2(41) -> 1
        , p_2(41) -> 13
        , p_2(41) -> 24
        , p_2(41) -> 28
        , p_2(41) -> 30
        , p_2(41) -> 36
        , p_2(41) -> 40
        , p_2(41) -> 51
        , p_2(41) -> 55
        , p_2(41) -> 57
        , p_2(42) -> 41
        , p_2(43) -> 42
        , p_2(46) -> 41
        , p_2(46) -> 45
        , p_2(49) -> 1
        , p_2(49) -> 13
        , p_2(49) -> 24
        , p_2(49) -> 28
        , p_2(49) -> 30
        , p_2(49) -> 36
        , p_2(49) -> 40
        , p_2(49) -> 48
        , p_2(49) -> 51
        , p_2(49) -> 55
        , p_2(49) -> 57
        , p_2(52) -> 51
        , p_2(53) -> 52
        , p_2(56) -> 51
        , p_2(56) -> 55
        , p_2(59) -> 58
        , p_2(60) -> 59
        , p_2(63) -> 58
        , p_2(63) -> 62
        , p_2(66) -> 65
        , p_2(67) -> 66
        , p_2(68) -> 67
        , p_2(72) -> 65
        , p_2(72) -> 71
        , p_3(44) -> 41
        , p_3(45) -> 1
        , p_3(45) -> 13
        , p_3(45) -> 24
        , p_3(45) -> 28
        , p_3(45) -> 30
        , p_3(45) -> 36
        , p_3(45) -> 40
        , p_3(45) -> 51
        , p_3(45) -> 55
        , p_3(45) -> 57
        , p_3(47) -> 1
        , p_3(47) -> 13
        , p_3(47) -> 24
        , p_3(47) -> 28
        , p_3(47) -> 30
        , p_3(47) -> 36
        , p_3(47) -> 40
        , p_3(47) -> 51
        , p_3(47) -> 55
        , p_3(47) -> 57
        , p_3(54) -> 51
        , p_3(61) -> 58
        , p_3(69) -> 66
        , p_3(70) -> 65
        , p_3(75) -> 74
        , p_3(76) -> 75
        , p_3(77) -> 76
        , p_3(81) -> 74
        , p_3(81) -> 80
        , p_4(78) -> 75
        , p_4(79) -> 74
        , bar_0(2) -> 1
        , bar_1(31) -> 24
        , bar_1(31) -> 28
        , bar_1(31) -> 30
        , bar_1(31) -> 51
        , bar_1(31) -> 55
        , bar_1(31) -> 57
        , bar_2(58) -> 51
        , bar_2(58) -> 55
        , bar_2(58) -> 57}