YES(?,O(n^1))
1091.32/297.06	YES(?,O(n^1))
1091.32/297.06	
1091.32/297.06	We are left with following problem, upon which TcT provides the
1091.32/297.06	certificate YES(?,O(n^1)).
1091.32/297.06	
1091.32/297.06	Strict Trs:
1091.32/297.06	  { 0(1(2(3(4(5(1(x1))))))) ->
1091.32/297.06	    1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))
1091.32/297.06	  , 0(1(2(3(4(5(1(x1))))))) ->
1091.32/297.06	    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))))))))))))))))))))))))) }
1091.32/297.06	Obligation:
1091.32/297.06	  derivational complexity
1091.32/297.06	Answer:
1091.32/297.06	  YES(?,O(n^1))
1091.32/297.06	
1091.32/297.06	The problem is match-bounded by 3. The enriched problem is
1091.32/297.06	compatible with the following automaton.
1091.32/297.06	{ 0_0(1) -> 1
1091.32/297.06	, 0_1(9) -> 8
1091.32/297.06	, 0_1(15) -> 14
1091.32/297.06	, 0_2(53) -> 52
1091.32/297.06	, 0_2(59) -> 58
1091.32/297.06	, 0_2(65) -> 64
1091.32/297.06	, 0_3(98) -> 97
1091.32/297.06	, 0_3(104) -> 103
1091.32/297.06	, 0_3(110) -> 109
1091.32/297.06	, 0_3(122) -> 121
1091.32/297.06	, 0_3(128) -> 127
1091.32/297.06	, 0_3(140) -> 139
1091.32/297.06	, 0_3(146) -> 145
1091.32/297.06	, 0_3(152) -> 151
1091.32/297.06	, 1_0(1) -> 1
1091.32/297.06	, 1_1(2) -> 1
1091.32/297.06	, 1_1(2) -> 14
1091.32/297.06	, 1_1(7) -> 6
1091.32/297.06	, 1_1(8) -> 7
1091.32/297.06	, 1_1(10) -> 9
1091.32/297.06	, 1_1(16) -> 15
1091.32/297.06	, 1_2(46) -> 8
1091.32/297.06	, 1_2(46) -> 14
1091.32/297.06	, 1_2(51) -> 50
1091.32/297.06	, 1_2(52) -> 51
1091.32/297.06	, 1_2(54) -> 53
1091.32/297.06	, 1_2(58) -> 75
1091.32/297.06	, 1_2(60) -> 59
1091.32/297.06	, 1_2(66) -> 65
1091.32/297.06	, 1_2(70) -> 8
1091.32/297.06	, 1_2(70) -> 14
1091.32/297.06	, 1_2(75) -> 74
1091.32/297.06	, 1_3(91) -> 64
1091.32/297.06	, 1_3(96) -> 95
1091.32/297.06	, 1_3(97) -> 96
1091.32/297.06	, 1_3(99) -> 98
1091.32/297.06	, 1_3(103) -> 96
1091.32/297.06	, 1_3(105) -> 104
1091.32/297.06	, 1_3(111) -> 110
1091.32/297.06	, 1_3(115) -> 58
1091.32/297.06	, 1_3(120) -> 119
1091.32/297.06	, 1_3(121) -> 120
1091.32/297.06	, 1_3(123) -> 122
1091.32/297.06	, 1_3(129) -> 128
1091.32/297.06	, 1_3(133) -> 52
1091.32/297.06	, 1_3(138) -> 137
1091.32/297.06	, 1_3(139) -> 138
1091.32/297.06	, 1_3(141) -> 140
1091.32/297.06	, 1_3(145) -> 138
1091.32/297.06	, 1_3(147) -> 146
1091.32/297.06	, 1_3(153) -> 152
1091.32/297.06	, 2_0(1) -> 1
1091.32/297.06	, 2_1(3) -> 2
1091.32/297.06	, 2_1(11) -> 10
1091.32/297.06	, 2_1(17) -> 16
1091.32/297.06	, 2_2(47) -> 46
1091.32/297.06	, 2_2(55) -> 54
1091.32/297.06	, 2_2(61) -> 60
1091.32/297.06	, 2_2(67) -> 66
1091.32/297.06	, 2_2(71) -> 70
1091.32/297.06	, 2_3(92) -> 91
1091.32/297.06	, 2_3(100) -> 99
1091.32/297.06	, 2_3(106) -> 105
1091.32/297.06	, 2_3(112) -> 111
1091.32/297.06	, 2_3(116) -> 115
1091.32/297.06	, 2_3(124) -> 123
1091.32/297.06	, 2_3(130) -> 129
1091.32/297.06	, 2_3(134) -> 133
1091.32/297.06	, 2_3(142) -> 141
1091.32/297.06	, 2_3(148) -> 147
1091.32/297.06	, 2_3(154) -> 153
1091.32/297.06	, 3_0(1) -> 1
1091.32/297.06	, 3_1(4) -> 3
1091.32/297.06	, 3_1(12) -> 11
1091.32/297.06	, 3_1(18) -> 17
1091.32/297.06	, 3_2(48) -> 47
1091.32/297.06	, 3_2(56) -> 55
1091.32/297.06	, 3_2(62) -> 61
1091.32/297.06	, 3_2(68) -> 67
1091.32/297.06	, 3_2(72) -> 71
1091.32/297.06	, 3_3(93) -> 92
1091.32/297.06	, 3_3(101) -> 100
1091.32/297.06	, 3_3(107) -> 106
1091.32/297.06	, 3_3(113) -> 112
1091.32/297.06	, 3_3(117) -> 116
1091.32/297.06	, 3_3(125) -> 124
1091.32/297.06	, 3_3(131) -> 130
1091.32/297.06	, 3_3(135) -> 134
1091.32/297.06	, 3_3(143) -> 142
1091.32/297.06	, 3_3(149) -> 148
1091.32/297.06	, 3_3(155) -> 154
1091.32/297.06	, 4_0(1) -> 1
1091.32/297.06	, 4_1(5) -> 4
1091.32/297.06	, 4_1(13) -> 12
1091.32/297.06	, 4_1(19) -> 18
1091.32/297.06	, 4_2(49) -> 48
1091.32/297.06	, 4_2(57) -> 56
1091.32/297.06	, 4_2(63) -> 62
1091.32/297.06	, 4_2(69) -> 68
1091.32/297.06	, 4_2(73) -> 72
1091.32/297.06	, 4_3(94) -> 93
1091.32/297.06	, 4_3(102) -> 101
1091.32/297.06	, 4_3(108) -> 107
1091.32/297.06	, 4_3(114) -> 113
1091.32/297.06	, 4_3(118) -> 117
1091.32/297.06	, 4_3(126) -> 125
1091.32/297.06	, 4_3(132) -> 131
1091.32/297.06	, 4_3(136) -> 135
1091.32/297.06	, 4_3(144) -> 143
1091.32/297.06	, 4_3(150) -> 149
1091.32/297.06	, 4_3(156) -> 155
1091.32/297.06	, 5_0(1) -> 1
1091.32/297.06	, 5_1(1) -> 19
1091.32/297.06	, 5_1(2) -> 13
1091.32/297.06	, 5_1(6) -> 5
1091.32/297.06	, 5_1(7) -> 13
1091.32/297.06	, 5_1(8) -> 13
1091.32/297.06	, 5_1(14) -> 13
1091.32/297.06	, 5_2(2) -> 69
1091.32/297.06	, 5_2(8) -> 69
1091.32/297.06	, 5_2(46) -> 69
1091.32/297.06	, 5_2(50) -> 49
1091.32/297.06	, 5_2(58) -> 57
1091.32/297.06	, 5_2(64) -> 63
1091.32/297.06	, 5_2(70) -> 69
1091.32/297.06	, 5_2(74) -> 73
1091.32/297.06	, 5_3(46) -> 108
1091.32/297.06	, 5_3(70) -> 114
1091.32/297.06	, 5_3(91) -> 132
1091.32/297.06	, 5_3(95) -> 94
1091.32/297.06	, 5_3(97) -> 102
1091.32/297.06	, 5_3(103) -> 102
1091.32/297.06	, 5_3(109) -> 108
1091.32/297.06	, 5_3(115) -> 156
1091.32/297.06	, 5_3(119) -> 118
1091.32/297.06	, 5_3(121) -> 126
1091.32/297.06	, 5_3(127) -> 126
1091.32/297.06	, 5_3(137) -> 136
1091.32/297.06	, 5_3(145) -> 144
1091.32/297.06	, 5_3(151) -> 150 }
1091.32/297.06	
1091.32/297.06	Hurray, we answered YES(?,O(n^1))
1092.15/297.77	EOF