YES(?,O(n^1))
1088.84/297.45	YES(?,O(n^1))
1088.84/297.45	
1088.84/297.45	We are left with following problem, upon which TcT provides the
1088.84/297.45	certificate YES(?,O(n^1)).
1088.84/297.45	
1088.84/297.45	Strict Trs:
1088.84/297.45	  { 0(1(2(3(4(5(1(x1))))))) ->
1088.84/297.45	    0(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))
1088.84/297.45	  , 0(1(2(3(4(5(1(x1))))))) ->
1088.84/297.45	    1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))))
1088.84/297.45	  , 0(1(2(3(4(5(1(x1))))))) ->
1088.84/297.45	    1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1))))))))))))))))))))))))))))))) }
1088.84/297.45	Obligation:
1088.84/297.45	  derivational complexity
1088.84/297.45	Answer:
1088.84/297.45	  YES(?,O(n^1))
1088.84/297.45	
1088.84/297.45	The problem is match-bounded by 3. The enriched problem is
1088.84/297.45	compatible with the following automaton.
1088.84/297.45	{ 0_0(1) -> 1
1088.84/297.45	, 0_1(2) -> 1
1088.84/297.45	, 0_1(2) -> 14
1088.84/297.45	, 0_1(9) -> 8
1088.84/297.45	, 0_1(15) -> 14
1088.84/297.45	, 0_1(20) -> 1
1088.84/297.45	, 0_1(27) -> 26
1088.84/297.45	, 0_2(63) -> 62
1088.84/297.45	, 0_2(69) -> 68
1088.84/297.45	, 0_2(75) -> 74
1088.84/297.45	, 0_2(81) -> 80
1088.84/297.45	, 0_2(86) -> 8
1088.84/297.45	, 0_2(86) -> 14
1088.84/297.45	, 0_2(86) -> 26
1088.84/297.45	, 0_3(99) -> 98
1088.84/297.45	, 0_3(105) -> 104
1088.84/297.45	, 0_3(111) -> 110
1088.84/297.45	, 0_3(117) -> 116
1088.84/297.45	, 0_3(122) -> 80
1088.84/297.45	, 0_3(128) -> 74
1088.84/297.45	, 0_3(135) -> 134
1088.84/297.45	, 0_3(141) -> 140
1088.84/297.45	, 0_3(153) -> 152
1088.84/297.45	, 0_3(165) -> 164
1088.84/297.45	, 0_3(171) -> 170
1088.84/297.45	, 0_3(177) -> 176
1088.84/297.45	, 0_3(183) -> 182
1088.84/297.45	, 0_3(188) -> 68
1088.84/297.45	, 0_3(194) -> 62
1088.84/297.45	, 0_3(201) -> 200
1088.84/297.45	, 0_3(207) -> 206
1088.84/297.45	, 0_3(219) -> 218
1088.84/297.45	, 1_0(1) -> 1
1088.84/297.45	, 1_1(7) -> 6
1088.84/297.45	, 1_1(8) -> 7
1088.84/297.45	, 1_1(10) -> 9
1088.84/297.45	, 1_1(16) -> 15
1088.84/297.45	, 1_1(20) -> 1
1088.84/297.45	, 1_1(20) -> 14
1088.84/297.45	, 1_1(25) -> 24
1088.84/297.45	, 1_1(26) -> 25
1088.84/297.45	, 1_1(28) -> 27
1088.84/297.45	, 1_2(56) -> 8
1088.84/297.45	, 1_2(56) -> 14
1088.84/297.45	, 1_2(56) -> 26
1088.84/297.45	, 1_2(61) -> 60
1088.84/297.45	, 1_2(62) -> 61
1088.84/297.45	, 1_2(64) -> 63
1088.84/297.45	, 1_2(68) -> 61
1088.84/297.45	, 1_2(70) -> 69
1088.84/297.45	, 1_2(74) -> 91
1088.84/297.45	, 1_2(76) -> 75
1088.84/297.45	, 1_2(82) -> 81
1088.84/297.45	, 1_2(91) -> 90
1088.84/297.45	, 1_3(92) -> 80
1088.84/297.45	, 1_3(97) -> 96
1088.84/297.45	, 1_3(98) -> 97
1088.84/297.45	, 1_3(100) -> 99
1088.84/297.45	, 1_3(104) -> 97
1088.84/297.45	, 1_3(106) -> 105
1088.84/297.45	, 1_3(110) -> 127
1088.84/297.45	, 1_3(112) -> 111
1088.84/297.45	, 1_3(118) -> 117
1088.84/297.45	, 1_3(127) -> 126
1088.84/297.45	, 1_3(133) -> 132
1088.84/297.45	, 1_3(134) -> 133
1088.84/297.45	, 1_3(136) -> 135
1088.84/297.45	, 1_3(142) -> 141
1088.84/297.45	, 1_3(146) -> 74
1088.84/297.45	, 1_3(151) -> 150
1088.84/297.45	, 1_3(152) -> 151
1088.84/297.45	, 1_3(154) -> 153
1088.84/297.45	, 1_3(158) -> 68
1088.84/297.45	, 1_3(163) -> 162
1088.84/297.45	, 1_3(164) -> 163
1088.84/297.45	, 1_3(166) -> 165
1088.84/297.45	, 1_3(170) -> 163
1088.84/297.45	, 1_3(172) -> 171
1088.84/297.45	, 1_3(176) -> 193
1088.84/297.45	, 1_3(178) -> 177
1088.84/297.45	, 1_3(184) -> 183
1088.84/297.45	, 1_3(193) -> 192
1088.84/297.45	, 1_3(199) -> 198
1088.84/297.45	, 1_3(200) -> 199
1088.84/297.45	, 1_3(202) -> 201
1088.84/297.45	, 1_3(208) -> 207
1088.84/297.45	, 1_3(212) -> 62
1088.84/297.45	, 1_3(217) -> 216
1088.84/297.45	, 1_3(218) -> 217
1088.84/297.45	, 1_3(220) -> 219
1088.84/297.45	, 2_0(1) -> 1
1088.84/297.45	, 2_1(3) -> 2
1088.84/297.45	, 2_1(11) -> 10
1088.84/297.45	, 2_1(17) -> 16
1088.84/297.45	, 2_1(21) -> 20
1088.84/297.45	, 2_1(29) -> 28
1088.84/297.45	, 2_2(57) -> 56
1088.84/297.45	, 2_2(65) -> 64
1088.84/297.45	, 2_2(71) -> 70
1088.84/297.45	, 2_2(77) -> 76
1088.84/297.45	, 2_2(83) -> 82
1088.84/297.45	, 2_2(87) -> 86
1088.84/297.45	, 2_3(93) -> 92
1088.84/297.45	, 2_3(101) -> 100
1088.84/297.45	, 2_3(107) -> 106
1088.84/297.45	, 2_3(113) -> 112
1088.84/297.45	, 2_3(119) -> 118
1088.84/297.45	, 2_3(123) -> 122
1088.84/297.45	, 2_3(129) -> 128
1088.84/297.45	, 2_3(137) -> 136
1088.84/297.45	, 2_3(143) -> 142
1088.84/297.45	, 2_3(147) -> 146
1088.84/297.45	, 2_3(155) -> 154
1088.84/297.45	, 2_3(159) -> 158
1088.84/297.45	, 2_3(167) -> 166
1088.84/297.45	, 2_3(173) -> 172
1088.84/297.45	, 2_3(179) -> 178
1088.84/297.45	, 2_3(185) -> 184
1088.84/297.45	, 2_3(189) -> 188
1088.84/297.45	, 2_3(195) -> 194
1088.84/297.45	, 2_3(203) -> 202
1088.84/297.45	, 2_3(209) -> 208
1088.84/297.45	, 2_3(213) -> 212
1088.84/297.45	, 2_3(221) -> 220
1088.84/297.45	, 3_0(1) -> 1
1088.84/297.45	, 3_1(4) -> 3
1088.84/297.45	, 3_1(12) -> 11
1088.84/297.45	, 3_1(18) -> 17
1088.84/297.45	, 3_1(22) -> 21
1088.84/297.45	, 3_1(30) -> 29
1088.84/297.45	, 3_2(58) -> 57
1088.84/297.45	, 3_2(66) -> 65
1088.84/297.45	, 3_2(72) -> 71
1088.84/297.45	, 3_2(78) -> 77
1088.84/297.45	, 3_2(84) -> 83
1088.84/297.45	, 3_2(88) -> 87
1088.84/297.45	, 3_3(94) -> 93
1088.84/297.45	, 3_3(102) -> 101
1088.84/297.45	, 3_3(108) -> 107
1088.84/297.45	, 3_3(114) -> 113
1088.84/297.45	, 3_3(120) -> 119
1088.84/297.45	, 3_3(124) -> 123
1088.84/297.45	, 3_3(130) -> 129
1088.84/297.45	, 3_3(138) -> 137
1088.84/297.45	, 3_3(144) -> 143
1088.84/297.45	, 3_3(148) -> 147
1088.84/297.45	, 3_3(156) -> 155
1088.84/297.45	, 3_3(160) -> 159
1088.84/297.45	, 3_3(168) -> 167
1088.84/297.45	, 3_3(174) -> 173
1088.84/297.45	, 3_3(180) -> 179
1088.84/297.45	, 3_3(186) -> 185
1088.84/297.45	, 3_3(190) -> 189
1088.84/297.45	, 3_3(196) -> 195
1088.84/297.45	, 3_3(204) -> 203
1088.84/297.45	, 3_3(210) -> 209
1088.84/297.45	, 3_3(214) -> 213
1088.84/297.45	, 3_3(222) -> 221
1088.84/297.45	, 4_0(1) -> 1
1088.84/297.45	, 4_1(5) -> 4
1088.84/297.45	, 4_1(13) -> 12
1088.84/297.45	, 4_1(19) -> 18
1088.84/297.45	, 4_1(23) -> 22
1088.84/297.45	, 4_1(31) -> 30
1088.84/297.45	, 4_2(59) -> 58
1088.84/297.45	, 4_2(67) -> 66
1088.84/297.45	, 4_2(73) -> 72
1088.84/297.45	, 4_2(79) -> 78
1088.84/297.45	, 4_2(85) -> 84
1088.84/297.45	, 4_2(89) -> 88
1088.84/297.45	, 4_3(95) -> 94
1088.84/297.45	, 4_3(103) -> 102
1088.84/297.45	, 4_3(109) -> 108
1088.84/297.45	, 4_3(115) -> 114
1088.84/297.45	, 4_3(121) -> 120
1088.84/297.45	, 4_3(125) -> 124
1088.84/297.45	, 4_3(131) -> 130
1088.84/297.45	, 4_3(139) -> 138
1088.84/297.45	, 4_3(145) -> 144
1088.84/297.45	, 4_3(149) -> 148
1088.84/297.45	, 4_3(157) -> 156
1088.84/297.45	, 4_3(161) -> 160
1088.84/297.45	, 4_3(169) -> 168
1088.84/297.45	, 4_3(175) -> 174
1088.84/297.45	, 4_3(181) -> 180
1088.84/297.45	, 4_3(187) -> 186
1088.84/297.45	, 4_3(191) -> 190
1088.84/297.45	, 4_3(197) -> 196
1088.84/297.45	, 4_3(205) -> 204
1088.84/297.45	, 4_3(211) -> 210
1088.84/297.45	, 4_3(215) -> 214
1088.84/297.45	, 4_3(223) -> 222
1088.84/297.45	, 5_0(1) -> 1
1088.84/297.45	, 5_1(1) -> 19
1088.84/297.45	, 5_1(6) -> 5
1088.84/297.45	, 5_1(8) -> 31
1088.84/297.45	, 5_1(14) -> 13
1088.84/297.45	, 5_1(20) -> 13
1088.84/297.45	, 5_1(24) -> 23
1088.84/297.45	, 5_1(25) -> 13
1088.84/297.45	, 5_1(26) -> 31
1088.84/297.45	, 5_2(20) -> 85
1088.84/297.45	, 5_2(26) -> 85
1088.84/297.45	, 5_2(56) -> 85
1088.84/297.45	, 5_2(60) -> 59
1088.84/297.45	, 5_2(68) -> 67
1088.84/297.45	, 5_2(74) -> 73
1088.84/297.45	, 5_2(80) -> 79
1088.84/297.45	, 5_2(90) -> 89
1088.84/297.45	, 5_3(56) -> 121
1088.84/297.45	, 5_3(92) -> 145
1088.84/297.45	, 5_3(96) -> 95
1088.84/297.45	, 5_3(104) -> 103
1088.84/297.45	, 5_3(110) -> 109
1088.84/297.45	, 5_3(116) -> 115
1088.84/297.45	, 5_3(126) -> 125
1088.84/297.45	, 5_3(132) -> 131
1088.84/297.45	, 5_3(134) -> 157
1088.84/297.45	, 5_3(140) -> 139
1088.84/297.45	, 5_3(146) -> 187
1088.84/297.45	, 5_3(150) -> 149
1088.84/297.45	, 5_3(152) -> 157
1088.84/297.45	, 5_3(158) -> 211
1088.84/297.45	, 5_3(162) -> 161
1088.84/297.45	, 5_3(170) -> 169
1088.84/297.45	, 5_3(176) -> 175
1088.84/297.45	, 5_3(182) -> 181
1088.84/297.45	, 5_3(192) -> 191
1088.84/297.45	, 5_3(198) -> 197
1088.84/297.45	, 5_3(200) -> 223
1088.84/297.45	, 5_3(206) -> 205
1088.84/297.45	, 5_3(216) -> 215
1088.84/297.45	, 5_3(218) -> 223 }
1088.84/297.45	
1088.84/297.45	Hurray, we answered YES(?,O(n^1))
1089.70/298.13	EOF