YES(?,O(n^1))
678.59/297.04	YES(?,O(n^1))
678.59/297.04	
678.59/297.04	We are left with following problem, upon which TcT provides the
678.59/297.04	certificate YES(?,O(n^1)).
678.59/297.04	
678.59/297.04	Strict Trs:
678.59/297.04	  { 2(5(x1)) -> 2(2(0(5(0(1(x1))))))
678.59/297.04	  , 2(5(x1)) -> 1(3(3(0(1(0(x1))))))
678.59/297.04	  , 2(5(2(x1))) -> 4(0(2(2(3(3(x1))))))
678.59/297.04	  , 2(5(1(x1))) -> 2(2(2(1(2(3(x1))))))
678.59/297.04	  , 2(5(3(x1))) -> 2(0(4(1(3(3(x1))))))
678.59/297.04	  , 2(5(4(x1))) -> 2(0(5(1(0(1(x1))))))
678.59/297.04	  , 5(5(3(x1))) -> 5(1(0(1(2(2(x1))))))
678.59/297.04	  , 5(5(4(x1))) -> 5(1(0(4(2(2(x1))))))
678.59/297.04	  , 1(2(5(x1))) -> 2(0(1(3(1(0(x1))))))
678.59/297.04	  , 1(2(5(x1))) -> 1(2(2(1(0(1(x1))))))
678.59/297.04	  , 1(2(5(x1))) -> 1(0(5(0(5(4(x1))))))
678.59/297.04	  , 1(4(5(x1))) -> 1(2(4(0(2(1(x1))))))
678.59/297.04	  , 3(2(5(x1))) -> 3(2(0(1(0(5(x1))))))
678.59/297.04	  , 3(5(x1)) -> 1(3(2(0(0(1(x1))))))
678.59/297.04	  , 3(5(x1)) -> 3(2(0(5(3(0(x1))))))
678.59/297.04	  , 3(5(2(x1))) -> 2(3(3(2(1(2(x1))))))
678.59/297.04	  , 3(5(2(x1))) -> 2(0(2(2(3(0(x1))))))
678.59/297.04	  , 3(5(2(x1))) -> 0(4(3(2(2(2(x1))))))
678.59/297.04	  , 3(5(5(x1))) -> 0(5(4(1(0(5(x1))))))
678.59/297.04	  , 3(5(1(x1))) -> 2(1(4(1(0(1(x1))))))
678.59/297.04	  , 3(5(1(x1))) -> 0(4(2(2(3(4(x1))))))
678.59/297.04	  , 3(5(1(x1))) -> 0(4(2(0(0(5(x1))))))
678.59/297.04	  , 3(5(3(x1))) -> 2(3(4(0(4(2(x1))))))
678.59/297.04	  , 3(5(3(x1))) -> 0(2(4(3(3(0(x1))))))
678.59/297.04	  , 3(5(3(x1))) -> 0(5(4(3(3(0(x1))))))
678.59/297.04	  , 3(5(4(x1))) -> 0(2(0(5(0(0(x1))))))
678.59/297.04	  , 3(5(4(x1))) -> 0(5(0(0(1(2(x1))))))
678.59/297.04	  , 3(4(2(x1))) -> 3(4(0(2(2(2(x1))))))
678.59/297.04	  , 4(5(x1)) -> 2(2(1(3(2(1(x1))))))
678.59/297.04	  , 4(5(x1)) -> 3(2(0(5(0(0(x1))))))
678.59/297.04	  , 4(5(2(x1))) -> 0(5(1(0(0(4(x1))))))
678.59/297.04	  , 4(5(1(x1))) -> 2(1(0(5(3(3(x1))))))
678.59/297.04	  , 4(5(4(x1))) -> 2(2(1(0(4(2(x1))))))
678.59/297.04	  , 4(5(4(x1))) -> 3(2(0(3(2(0(x1)))))) }
678.59/297.04	Obligation:
678.59/297.04	  derivational complexity
678.59/297.04	Answer:
678.59/297.04	  YES(?,O(n^1))
678.59/297.04	
678.59/297.04	The problem is match-bounded by 2. The enriched problem is
678.59/297.04	compatible with the following automaton.
678.59/297.04	{ 2_0(1) -> 1
678.59/297.04	, 2_1(1) -> 26
678.59/297.04	, 2_1(2) -> 1
678.59/297.04	, 2_1(2) -> 6
678.59/297.04	, 2_1(2) -> 16
678.59/297.04	, 2_1(2) -> 26
678.59/297.04	, 2_1(2) -> 32
678.59/297.04	, 2_1(2) -> 55
678.59/297.04	, 2_1(3) -> 2
678.59/297.04	, 2_1(6) -> 34
678.59/297.04	, 2_1(9) -> 35
678.59/297.04	, 2_1(11) -> 133
678.59/297.04	, 2_1(12) -> 26
678.59/297.04	, 2_1(14) -> 13
678.59/297.04	, 2_1(15) -> 14
678.59/297.04	, 2_1(16) -> 18
678.59/297.04	, 2_1(17) -> 3
678.59/297.04	, 2_1(21) -> 28
678.59/297.04	, 2_1(25) -> 59
678.59/297.04	, 2_1(26) -> 25
678.59/297.04	, 2_1(28) -> 7
678.59/297.04	, 2_1(35) -> 26
678.59/297.04	, 2_1(36) -> 35
678.59/297.04	, 2_1(40) -> 8
678.59/297.04	, 2_1(46) -> 56
678.59/297.04	, 2_1(48) -> 26
678.59/297.04	, 2_1(55) -> 54
678.59/297.04	, 2_1(56) -> 19
678.59/297.04	, 2_1(57) -> 26
678.59/297.04	, 2_1(67) -> 58
678.59/297.04	, 2_1(68) -> 67
678.59/297.04	, 2_1(83) -> 57
678.59/297.04	, 2_1(166) -> 1
678.59/297.04	, 2_2(2) -> 98
678.59/297.04	, 2_2(3) -> 98
678.59/297.04	, 2_2(10) -> 203
678.59/297.04	, 2_2(11) -> 82
678.59/297.04	, 2_2(15) -> 203
678.59/297.04	, 2_2(28) -> 98
678.59/297.04	, 2_2(32) -> 97
678.59/297.04	, 2_2(37) -> 203
678.59/297.04	, 2_2(43) -> 42
678.59/297.04	, 2_2(45) -> 102
678.59/297.04	, 2_2(49) -> 48
678.59/297.04	, 2_2(60) -> 174
678.59/297.04	, 2_2(62) -> 16
678.59/297.04	, 2_2(67) -> 207
678.59/297.04	, 2_2(71) -> 70
678.59/297.04	, 2_2(72) -> 71
678.59/297.04	, 2_2(78) -> 27
678.59/297.04	, 2_2(84) -> 203
678.59/297.04	, 2_2(86) -> 85
678.59/297.04	, 2_2(97) -> 96
678.59/297.04	, 2_2(98) -> 97
678.59/297.04	, 2_2(99) -> 32
678.59/297.04	, 2_2(100) -> 99
678.59/297.04	, 2_2(103) -> 60
678.59/297.04	, 2_2(104) -> 103
678.59/297.04	, 2_2(107) -> 106
678.59/297.04	, 2_2(109) -> 108
678.59/297.04	, 2_2(112) -> 194
678.59/297.04	, 2_2(113) -> 112
678.59/297.04	, 2_2(132) -> 144
678.59/297.04	, 2_2(136) -> 26
678.59/297.04	, 2_2(137) -> 136
678.59/297.04	, 2_2(143) -> 137
678.59/297.04	, 2_2(145) -> 55
678.59/297.04	, 2_2(149) -> 148
678.59/297.04	, 2_2(150) -> 149
678.59/297.04	, 2_2(156) -> 155
678.59/297.04	, 2_2(160) -> 159
678.59/297.04	, 2_2(163) -> 162
678.59/297.04	, 2_2(166) -> 1
678.59/297.04	, 2_2(166) -> 32
678.59/297.04	, 2_2(168) -> 167
678.59/297.04	, 2_2(169) -> 168
678.59/297.04	, 2_2(174) -> 173
678.59/297.04	, 2_2(183) -> 172
678.59/297.04	, 2_2(184) -> 183
678.59/297.04	, 2_2(195) -> 171
678.59/297.04	, 2_2(203) -> 272
678.59/297.04	, 2_2(206) -> 205
678.59/297.04	, 2_2(207) -> 206
678.59/297.04	, 2_2(218) -> 10
678.59/297.04	, 2_2(232) -> 231
678.59/297.04	, 2_2(233) -> 232
678.59/297.04	, 2_2(261) -> 202
678.59/297.04	, 2_2(271) -> 203
678.59/297.04	, 5_0(1) -> 1
678.59/297.04	, 5_1(1) -> 39
678.59/297.04	, 5_1(5) -> 4
678.59/297.04	, 5_1(7) -> 39
678.59/297.04	, 5_1(15) -> 124
678.59/297.04	, 5_1(21) -> 19
678.59/297.04	, 5_1(22) -> 1
678.59/297.04	, 5_1(22) -> 39
678.59/297.04	, 5_1(23) -> 39
678.59/297.04	, 5_1(30) -> 29
678.59/297.04	, 5_1(32) -> 31
678.59/297.04	, 5_1(41) -> 39
678.59/297.04	, 5_1(46) -> 10
678.59/297.04	, 5_1(60) -> 57
678.59/297.04	, 5_1(83) -> 57
678.59/297.04	, 5_1(91) -> 90
678.59/297.04	, 5_2(23) -> 75
678.59/297.04	, 5_2(44) -> 138
678.59/297.04	, 5_2(51) -> 50
678.59/297.04	, 5_2(86) -> 85
678.59/297.04	, 5_2(111) -> 110
678.59/297.04	, 5_2(115) -> 114
678.59/297.04	, 5_2(117) -> 187
678.59/297.04	, 5_2(131) -> 130
678.59/297.04	, 5_2(152) -> 151
678.59/297.04	, 5_2(154) -> 153
678.59/297.04	, 5_2(161) -> 222
678.59/297.04	, 5_2(165) -> 164
678.59/297.04	, 5_2(195) -> 171
678.59/297.04	, 5_2(200) -> 199
678.59/297.04	, 5_2(258) -> 255
678.59/297.04	, 5_2(268) -> 267
678.59/297.04	, 5_2(270) -> 269
678.59/297.04	, 1_0(1) -> 1
678.59/297.04	, 1_1(1) -> 6
678.59/297.04	, 1_1(5) -> 21
678.59/297.04	, 1_1(7) -> 1
678.59/297.04	, 1_1(7) -> 6
678.59/297.04	, 1_1(7) -> 16
678.59/297.04	, 1_1(7) -> 26
678.59/297.04	, 1_1(7) -> 55
678.59/297.04	, 1_1(11) -> 10
678.59/297.04	, 1_1(12) -> 6
678.59/297.04	, 1_1(15) -> 20
678.59/297.04	, 1_1(18) -> 17
678.59/297.04	, 1_1(22) -> 6
678.59/297.04	, 1_1(23) -> 22
678.59/297.04	, 1_1(25) -> 24
678.59/297.04	, 1_1(26) -> 55
678.59/297.04	, 1_1(27) -> 19
678.59/297.04	, 1_1(38) -> 37
678.59/297.04	, 1_1(41) -> 1
678.59/297.04	, 1_1(53) -> 3
678.59/297.04	, 1_1(60) -> 2
678.59/297.04	, 1_1(61) -> 2
678.59/297.04	, 1_1(68) -> 20
678.59/297.04	, 1_1(76) -> 3
678.59/297.04	, 1_1(117) -> 60
678.59/297.04	, 1_2(10) -> 260
678.59/297.04	, 1_2(15) -> 260
678.59/297.04	, 1_2(22) -> 45
678.59/297.04	, 1_2(23) -> 66
678.59/297.04	, 1_2(37) -> 260
678.59/297.04	, 1_2(41) -> 1
678.59/297.04	, 1_2(41) -> 16
678.59/297.04	, 1_2(41) -> 32
678.59/297.04	, 1_2(44) -> 150
678.59/297.04	, 1_2(46) -> 107
678.59/297.04	, 1_2(52) -> 142
678.59/297.04	, 1_2(60) -> 45
678.59/297.04	, 1_2(63) -> 62
678.59/297.04	, 1_2(65) -> 64
678.59/297.04	, 1_2(83) -> 45
678.59/297.04	, 1_2(84) -> 260
678.59/297.04	, 1_2(101) -> 100
678.59/297.04	, 1_2(105) -> 104
678.59/297.04	, 1_2(116) -> 229
678.59/297.04	, 1_2(117) -> 182
678.59/297.04	, 1_2(129) -> 99
678.59/297.04	, 1_2(139) -> 26
678.59/297.04	, 1_2(144) -> 143
678.59/297.04	, 1_2(147) -> 146
678.59/297.04	, 1_2(148) -> 55
678.59/297.04	, 1_2(155) -> 2
678.59/297.04	, 1_2(155) -> 45
678.59/297.04	, 1_2(158) -> 27
678.59/297.04	, 1_2(161) -> 218
678.59/297.04	, 1_2(179) -> 166
678.59/297.04	, 1_2(181) -> 180
678.59/297.04	, 1_2(203) -> 202
678.59/297.04	, 1_2(226) -> 203
678.59/297.04	, 1_2(244) -> 243
678.59/297.04	, 1_2(257) -> 256
678.59/297.04	, 1_2(259) -> 258
678.59/297.04	, 1_2(263) -> 262
678.59/297.04	, 1_2(271) -> 260
678.59/297.04	, 3_0(1) -> 1
678.59/297.04	, 3_1(1) -> 16
678.59/297.04	, 3_1(2) -> 16
678.59/297.04	, 3_1(7) -> 16
678.59/297.04	, 3_1(8) -> 7
678.59/297.04	, 3_1(9) -> 8
678.59/297.04	, 3_1(10) -> 27
678.59/297.04	, 3_1(11) -> 46
678.59/297.04	, 3_1(16) -> 15
678.59/297.04	, 3_1(23) -> 16
678.59/297.04	, 3_1(25) -> 58
678.59/297.04	, 3_1(32) -> 68
678.59/297.04	, 3_1(34) -> 53
678.59/297.04	, 3_1(35) -> 1
678.59/297.04	, 3_1(35) -> 16
678.59/297.04	, 3_1(35) -> 32
678.59/297.04	, 3_1(35) -> 68
678.59/297.04	, 3_1(41) -> 16
678.59/297.04	, 3_1(46) -> 84
678.59/297.04	, 3_1(48) -> 16
678.59/297.04	, 3_1(53) -> 2
678.59/297.04	, 3_1(54) -> 53
678.59/297.04	, 3_1(57) -> 1
678.59/297.04	, 3_1(57) -> 32
678.59/297.04	, 3_1(59) -> 58
678.59/297.04	, 3_1(133) -> 10
678.59/297.04	, 3_1(166) -> 16
678.59/297.04	, 3_2(11) -> 245
678.59/297.04	, 3_2(23) -> 132
678.59/297.04	, 3_2(42) -> 41
678.59/297.04	, 3_2(48) -> 1
678.59/297.04	, 3_2(48) -> 16
678.59/297.04	, 3_2(48) -> 32
678.59/297.04	, 3_2(52) -> 51
678.59/297.04	, 3_2(60) -> 257
678.59/297.04	, 3_2(73) -> 72
678.59/297.04	, 3_2(79) -> 78
678.59/297.04	, 3_2(88) -> 87
678.59/297.04	, 3_2(89) -> 88
678.59/297.04	, 3_2(94) -> 68
678.59/297.04	, 3_2(101) -> 166
678.59/297.04	, 3_2(102) -> 101
678.59/297.04	, 3_2(103) -> 234
678.59/297.04	, 3_2(106) -> 105
678.59/297.04	, 3_2(108) -> 32
678.59/297.04	, 3_2(112) -> 60
678.59/297.04	, 3_2(116) -> 165
678.59/297.04	, 3_2(117) -> 132
678.59/297.04	, 3_2(132) -> 131
678.59/297.04	, 3_2(140) -> 139
678.59/297.04	, 3_2(141) -> 140
678.59/297.04	, 3_2(142) -> 147
678.59/297.04	, 3_2(159) -> 158
678.59/297.04	, 3_2(162) -> 27
678.59/297.04	, 3_2(170) -> 169
678.59/297.04	, 3_2(173) -> 172
678.59/297.04	, 3_2(185) -> 184
678.59/297.04	, 3_2(197) -> 196
678.59/297.04	, 3_2(198) -> 197
678.59/297.04	, 3_2(227) -> 226
678.59/297.04	, 3_2(228) -> 227
678.59/297.04	, 3_2(229) -> 263
678.59/297.04	, 3_2(234) -> 233
678.59/297.04	, 3_2(245) -> 244
678.59/297.04	, 0_0(1) -> 1
678.59/297.04	, 0_1(1) -> 11
678.59/297.04	, 0_1(2) -> 11
678.59/297.04	, 0_1(4) -> 3
678.59/297.04	, 0_1(5) -> 40
678.59/297.04	, 0_1(6) -> 5
678.59/297.04	, 0_1(10) -> 9
678.59/297.04	, 0_1(11) -> 91
678.59/297.04	, 0_1(12) -> 11
678.59/297.04	, 0_1(13) -> 12
678.59/297.04	, 0_1(19) -> 2
678.59/297.04	, 0_1(22) -> 11
678.59/297.04	, 0_1(24) -> 23
678.59/297.04	, 0_1(25) -> 93
678.59/297.04	, 0_1(29) -> 7
678.59/297.04	, 0_1(31) -> 30
678.59/297.04	, 0_1(32) -> 119
678.59/297.04	, 0_1(34) -> 33
678.59/297.04	, 0_1(35) -> 11
678.59/297.04	, 0_1(37) -> 36
678.59/297.04	, 0_1(38) -> 67
678.59/297.04	, 0_1(39) -> 38
678.59/297.04	, 0_1(48) -> 11
678.59/297.04	, 0_1(55) -> 90
678.59/297.04	, 0_1(57) -> 1
678.59/297.04	, 0_1(57) -> 16
678.59/297.04	, 0_1(57) -> 32
678.59/297.04	, 0_1(59) -> 93
678.59/297.04	, 0_1(77) -> 76
678.59/297.04	, 0_1(90) -> 83
678.59/297.04	, 0_1(119) -> 117
678.59/297.04	, 0_1(124) -> 60
678.59/297.04	, 0_1(166) -> 11
678.59/297.04	, 0_2(10) -> 201
678.59/297.04	, 0_2(11) -> 89
678.59/297.04	, 0_2(15) -> 201
678.59/297.04	, 0_2(22) -> 52
678.59/297.04	, 0_2(37) -> 201
678.59/297.04	, 0_2(44) -> 43
678.59/297.04	, 0_2(45) -> 44
678.59/297.04	, 0_2(46) -> 116
678.59/297.04	, 0_2(50) -> 49
678.59/297.04	, 0_2(52) -> 111
678.59/297.04	, 0_2(60) -> 52
678.59/297.04	, 0_2(66) -> 65
678.59/297.04	, 0_2(69) -> 16
678.59/297.04	, 0_2(74) -> 71
678.59/297.04	, 0_2(75) -> 74
678.59/297.04	, 0_2(81) -> 80
678.59/297.04	, 0_2(83) -> 52
678.59/297.04	, 0_2(84) -> 201
678.59/297.04	, 0_2(85) -> 27
678.59/297.04	, 0_2(96) -> 95
678.59/297.04	, 0_2(103) -> 170
678.59/297.04	, 0_2(106) -> 157
678.59/297.04	, 0_2(107) -> 161
678.59/297.04	, 0_2(110) -> 109
678.59/297.04	, 0_2(112) -> 198
678.59/297.04	, 0_2(114) -> 113
678.59/297.04	, 0_2(116) -> 115
678.59/297.04	, 0_2(130) -> 129
678.59/297.04	, 0_2(138) -> 137
678.59/297.04	, 0_2(142) -> 141
678.59/297.04	, 0_2(146) -> 145
678.59/297.04	, 0_2(151) -> 148
678.59/297.04	, 0_2(153) -> 152
678.59/297.04	, 0_2(161) -> 160
678.59/297.04	, 0_2(164) -> 163
678.59/297.04	, 0_2(167) -> 166
678.59/297.04	, 0_2(171) -> 1
678.59/297.04	, 0_2(171) -> 32
678.59/297.04	, 0_2(182) -> 181
678.59/297.04	, 0_2(186) -> 183
678.59/297.04	, 0_2(187) -> 186
678.59/297.04	, 0_2(193) -> 192
678.59/297.04	, 0_2(199) -> 195
678.59/297.04	, 0_2(201) -> 200
678.59/297.04	, 0_2(202) -> 199
678.59/297.04	, 0_2(205) -> 204
678.59/297.04	, 0_2(222) -> 218
678.59/297.04	, 0_2(229) -> 228
678.59/297.04	, 0_2(231) -> 230
678.59/297.04	, 0_2(239) -> 10
678.59/297.04	, 0_2(255) -> 136
678.59/297.04	, 0_2(260) -> 259
678.59/297.04	, 0_2(262) -> 261
678.59/297.04	, 0_2(267) -> 203
678.59/297.04	, 0_2(269) -> 268
678.59/297.04	, 0_2(271) -> 201
678.59/297.04	, 0_2(272) -> 271
678.59/297.04	, 4_0(1) -> 1
678.59/297.04	, 4_1(1) -> 32
678.59/297.04	, 4_1(2) -> 32
678.59/297.04	, 4_1(7) -> 32
678.59/297.04	, 4_1(10) -> 60
678.59/297.04	, 4_1(12) -> 1
678.59/297.04	, 4_1(12) -> 26
678.59/297.04	, 4_1(15) -> 83
678.59/297.04	, 4_1(20) -> 19
678.59/297.04	, 4_1(21) -> 61
678.59/297.04	, 4_1(22) -> 32
678.59/297.04	, 4_1(23) -> 32
678.59/297.04	, 4_1(25) -> 24
678.59/297.04	, 4_1(26) -> 77
678.59/297.04	, 4_1(33) -> 28
678.59/297.04	, 4_1(37) -> 60
678.59/297.04	, 4_1(41) -> 32
678.59/297.04	, 4_1(58) -> 57
678.59/297.04	, 4_1(76) -> 53
678.59/297.04	, 4_1(84) -> 83
678.59/297.04	, 4_1(93) -> 35
678.59/297.04	, 4_1(166) -> 32
678.59/297.04	, 4_2(22) -> 154
678.59/297.04	, 4_2(23) -> 73
678.59/297.04	, 4_2(46) -> 270
678.59/297.04	, 4_2(60) -> 154
678.59/297.04	, 4_2(64) -> 63
678.59/297.04	, 4_2(70) -> 69
678.59/297.04	, 4_2(80) -> 79
678.59/297.04	, 4_2(82) -> 81
678.59/297.04	, 4_2(83) -> 154
678.59/297.04	, 4_2(87) -> 86
678.59/297.04	, 4_2(95) -> 94
678.59/297.04	, 4_2(117) -> 185
678.59/297.04	, 4_2(157) -> 156
678.59/297.04	, 4_2(172) -> 171
678.59/297.04	, 4_2(180) -> 179
678.59/297.04	, 4_2(192) -> 101
678.59/297.04	, 4_2(194) -> 193
678.59/297.04	, 4_2(196) -> 195
678.59/297.04	, 4_2(204) -> 48
678.59/297.04	, 4_2(230) -> 26
678.59/297.04	, 4_2(243) -> 239
678.59/297.04	, 4_2(256) -> 255
678.59/297.04	, 4_2(271) -> 60 }
678.59/297.04	
678.59/297.04	Hurray, we answered YES(?,O(n^1))
678.71/297.12	EOF