YES(?,O(n^1))
1168.21/297.02	YES(?,O(n^1))
1168.21/297.02	
1168.21/297.02	We are left with following problem, upon which TcT provides the
1168.21/297.02	certificate YES(?,O(n^1)).
1168.21/297.02	
1168.21/297.02	Strict Trs: { a(a(b(b(x1)))) -> b(b(b(a(a(a(a(a(x1)))))))) }
1168.21/297.02	Obligation:
1168.21/297.02	  derivational complexity
1168.21/297.02	Answer:
1168.21/297.02	  YES(?,O(n^1))
1168.21/297.02	
1168.21/297.02	The problem is match-bounded by 7. The enriched problem is
1168.21/297.02	compatible with the following automaton.
1168.21/297.02	{ a_0(1) -> 1
1168.21/297.02	, a_0(2) -> 1
1168.21/297.02	, a_1(1) -> 9
1168.21/297.02	, a_1(2) -> 9
1168.21/297.02	, a_1(3) -> 9
1168.21/297.02	, a_1(4) -> 9
1168.21/297.02	, a_1(6) -> 5
1168.21/297.02	, a_1(7) -> 6
1168.21/297.02	, a_1(8) -> 7
1168.21/297.02	, a_1(9) -> 8
1168.21/297.02	, a_2(4) -> 16
1168.21/297.02	, a_2(5) -> 16
1168.21/297.02	, a_2(10) -> 16
1168.21/297.02	, a_2(11) -> 16
1168.21/297.02	, a_2(13) -> 12
1168.21/297.02	, a_2(14) -> 13
1168.21/297.02	, a_2(15) -> 14
1168.21/297.02	, a_2(16) -> 15
1168.21/297.02	, a_3(11) -> 23
1168.21/297.02	, a_3(12) -> 23
1168.21/297.02	, a_3(18) -> 30
1168.21/297.02	, a_3(20) -> 19
1168.21/297.02	, a_3(21) -> 20
1168.21/297.02	, a_3(22) -> 21
1168.21/297.02	, a_3(23) -> 22
1168.21/297.02	, a_3(24) -> 23
1168.21/297.02	, a_3(25) -> 30
1168.21/297.02	, a_3(27) -> 26
1168.21/297.02	, a_3(28) -> 27
1168.21/297.02	, a_3(29) -> 28
1168.21/297.02	, a_3(30) -> 29
1168.21/297.02	, a_4(18) -> 44
1168.21/297.02	, a_4(25) -> 37
1168.21/297.02	, a_4(26) -> 37
1168.21/297.02	, a_4(32) -> 44
1168.21/297.02	, a_4(34) -> 33
1168.21/297.02	, a_4(35) -> 34
1168.21/297.02	, a_4(36) -> 35
1168.21/297.02	, a_4(37) -> 36
1168.21/297.02	, a_4(38) -> 51
1168.21/297.02	, a_4(41) -> 40
1168.21/297.02	, a_4(42) -> 41
1168.21/297.02	, a_4(43) -> 42
1168.21/297.02	, a_4(44) -> 43
1168.21/297.02	, a_4(46) -> 58
1168.21/297.02	, a_4(48) -> 47
1168.21/297.02	, a_4(49) -> 48
1168.21/297.02	, a_4(50) -> 49
1168.21/297.02	, a_4(51) -> 50
1168.21/297.02	, a_4(53) -> 79
1168.21/297.02	, a_4(55) -> 54
1168.21/297.02	, a_4(56) -> 55
1168.21/297.02	, a_4(57) -> 56
1168.21/297.02	, a_4(58) -> 57
1168.21/297.02	, a_4(76) -> 75
1168.21/297.02	, a_4(77) -> 76
1168.21/297.02	, a_4(78) -> 77
1168.21/297.02	, a_4(79) -> 78
1168.21/297.02	, a_5(40) -> 65
1168.21/297.02	, a_5(46) -> 72
1168.21/297.02	, a_5(60) -> 86
1168.21/297.02	, a_5(62) -> 61
1168.21/297.02	, a_5(63) -> 62
1168.21/297.02	, a_5(64) -> 63
1168.21/297.02	, a_5(65) -> 64
1168.21/297.02	, a_5(67) -> 93
1168.21/297.02	, a_5(69) -> 68
1168.21/297.02	, a_5(70) -> 69
1168.21/297.02	, a_5(71) -> 70
1168.21/297.02	, a_5(72) -> 71
1168.21/297.02	, a_5(74) -> 100
1168.21/297.02	, a_5(83) -> 82
1168.21/297.02	, a_5(84) -> 83
1168.21/297.02	, a_5(85) -> 84
1168.21/297.02	, a_5(86) -> 85
1168.21/297.02	, a_5(90) -> 89
1168.21/297.02	, a_5(91) -> 90
1168.21/297.02	, a_5(92) -> 91
1168.21/297.02	, a_5(93) -> 92
1168.21/297.02	, a_5(95) -> 114
1168.21/297.02	, a_5(97) -> 96
1168.21/297.02	, a_5(98) -> 97
1168.21/297.02	, a_5(99) -> 98
1168.21/297.02	, a_5(100) -> 99
1168.21/297.02	, a_5(108) -> 128
1168.21/297.02	, a_5(111) -> 110
1168.21/297.02	, a_5(112) -> 111
1168.21/297.02	, a_5(113) -> 112
1168.21/297.02	, a_5(114) -> 113
1168.21/297.02	, a_5(123) -> 72
1168.21/297.02	, a_5(125) -> 124
1168.21/297.02	, a_5(126) -> 125
1168.21/297.02	, a_5(127) -> 126
1168.21/297.02	, a_5(128) -> 127
1168.21/297.02	, a_6(88) -> 107
1168.21/297.02	, a_6(102) -> 121
1168.21/297.02	, a_6(104) -> 103
1168.21/297.02	, a_6(105) -> 104
1168.21/297.02	, a_6(106) -> 105
1168.21/297.02	, a_6(107) -> 106
1168.21/297.02	, a_6(110) -> 142
1168.21/297.02	, a_6(115) -> 135
1168.21/297.02	, a_6(118) -> 117
1168.21/297.02	, a_6(119) -> 118
1168.21/297.02	, a_6(120) -> 119
1168.21/297.02	, a_6(121) -> 120
1168.21/297.02	, a_6(130) -> 149
1168.21/297.02	, a_6(132) -> 131
1168.21/297.02	, a_6(133) -> 132
1168.21/297.02	, a_6(134) -> 133
1168.21/297.02	, a_6(135) -> 134
1168.21/297.02	, a_6(137) -> 163
1168.21/297.02	, a_6(139) -> 138
1168.21/297.02	, a_6(140) -> 139
1168.21/297.02	, a_6(141) -> 140
1168.21/297.02	, a_6(142) -> 141
1168.21/297.02	, a_6(146) -> 145
1168.21/297.02	, a_6(147) -> 146
1168.21/297.02	, a_6(148) -> 147
1168.21/297.02	, a_6(149) -> 148
1168.21/297.02	, a_6(160) -> 159
1168.21/297.02	, a_6(161) -> 160
1168.21/297.02	, a_6(162) -> 161
1168.21/297.02	, a_6(163) -> 162
1168.21/297.02	, a_7(117) -> 156
1168.21/297.02	, a_7(151) -> 170
1168.21/297.02	, a_7(153) -> 152
1168.21/297.02	, a_7(154) -> 153
1168.21/297.02	, a_7(155) -> 154
1168.21/297.02	, a_7(156) -> 155
1168.21/297.02	, a_7(167) -> 166
1168.21/297.02	, a_7(168) -> 167
1168.21/297.02	, a_7(169) -> 168
1168.21/297.02	, a_7(170) -> 169
1168.21/297.02	, b_0(1) -> 2
1168.21/297.02	, b_0(2) -> 2
1168.21/297.02	, b_1(3) -> 1
1168.21/297.02	, b_1(3) -> 8
1168.21/297.02	, b_1(3) -> 9
1168.21/297.02	, b_1(4) -> 3
1168.21/297.02	, b_1(5) -> 4
1168.21/297.02	, b_2(10) -> 5
1168.21/297.02	, b_2(10) -> 6
1168.21/297.02	, b_2(10) -> 7
1168.21/297.02	, b_2(10) -> 8
1168.21/297.02	, b_2(10) -> 15
1168.21/297.02	, b_2(10) -> 16
1168.21/297.02	, b_2(11) -> 10
1168.21/297.02	, b_2(12) -> 11
1168.21/297.02	, b_3(17) -> 13
1168.21/297.02	, b_3(17) -> 14
1168.21/297.02	, b_3(17) -> 15
1168.21/297.02	, b_3(17) -> 22
1168.21/297.02	, b_3(18) -> 17
1168.21/297.02	, b_3(19) -> 18
1168.21/297.02	, b_3(24) -> 12
1168.21/297.02	, b_3(24) -> 13
1168.21/297.02	, b_3(24) -> 23
1168.21/297.02	, b_3(25) -> 24
1168.21/297.02	, b_3(26) -> 25
1168.21/297.02	, b_4(31) -> 21
1168.21/297.02	, b_4(31) -> 22
1168.21/297.02	, b_4(32) -> 31
1168.21/297.02	, b_4(33) -> 32
1168.21/297.02	, b_4(38) -> 19
1168.21/297.02	, b_4(38) -> 20
1168.21/297.02	, b_4(39) -> 38
1168.21/297.02	, b_4(40) -> 39
1168.21/297.02	, b_4(45) -> 29
1168.21/297.02	, b_4(45) -> 43
1168.21/297.02	, b_4(46) -> 45
1168.21/297.02	, b_4(47) -> 46
1168.21/297.02	, b_4(52) -> 27
1168.21/297.02	, b_4(53) -> 52
1168.21/297.02	, b_4(54) -> 53
1168.21/297.02	, b_4(73) -> 37
1168.21/297.02	, b_4(74) -> 73
1168.21/297.02	, b_4(75) -> 74
1168.21/297.02	, b_5(59) -> 50
1168.21/297.02	, b_5(60) -> 59
1168.21/297.02	, b_5(61) -> 60
1168.21/297.02	, b_5(66) -> 41
1168.21/297.02	, b_5(67) -> 66
1168.21/297.02	, b_5(68) -> 67
1168.21/297.02	, b_5(80) -> 48
1168.21/297.02	, b_5(81) -> 80
1168.21/297.02	, b_5(82) -> 81
1168.21/297.02	, b_5(87) -> 65
1168.21/297.02	, b_5(88) -> 87
1168.21/297.02	, b_5(89) -> 88
1168.21/297.02	, b_5(94) -> 35
1168.21/297.02	, b_5(95) -> 94
1168.21/297.02	, b_5(96) -> 95
1168.21/297.02	, b_5(108) -> 33
1168.21/297.02	, b_5(109) -> 108
1168.21/297.02	, b_5(110) -> 109
1168.21/297.02	, b_5(122) -> 43
1168.21/297.02	, b_5(123) -> 122
1168.21/297.02	, b_5(124) -> 123
1168.21/297.02	, b_6(101) -> 63
1168.21/297.02	, b_6(102) -> 101
1168.21/297.02	, b_6(103) -> 102
1168.21/297.02	, b_6(115) -> 61
1168.21/297.02	, b_6(116) -> 115
1168.21/297.02	, b_6(117) -> 116
1168.21/297.02	, b_6(129) -> 85
1168.21/297.02	, b_6(130) -> 129
1168.21/297.02	, b_6(131) -> 130
1168.21/297.02	, b_6(136) -> 127
1168.21/297.02	, b_6(137) -> 136
1168.21/297.02	, b_6(138) -> 137
1168.21/297.02	, b_6(143) -> 83
1168.21/297.02	, b_6(144) -> 143
1168.21/297.02	, b_6(145) -> 144
1168.21/297.02	, b_6(157) -> 125
1168.21/297.02	, b_6(158) -> 157
1168.21/297.02	, b_6(159) -> 158
1168.21/297.02	, b_7(150) -> 134
1168.21/297.02	, b_7(151) -> 150
1168.21/297.02	, b_7(152) -> 151
1168.21/297.02	, b_7(164) -> 132
1168.21/297.02	, b_7(165) -> 164
1168.21/297.02	, b_7(166) -> 165 }
1168.21/297.02	
1168.21/297.02	Hurray, we answered YES(?,O(n^1))
1168.74/297.54	EOF