YES(?,O(n^1))
1179.16/297.04	YES(?,O(n^1))
1179.16/297.04	
1179.16/297.04	We are left with following problem, upon which TcT provides the
1179.16/297.04	certificate YES(?,O(n^1)).
1179.16/297.04	
1179.16/297.04	Strict Trs:
1179.16/297.04	  { b(a(a(b(a(b(a(x1))))))) -> a(a(b(a(b(b(a(a(b(x1))))))))) }
1179.16/297.04	Obligation:
1179.16/297.04	  derivational complexity
1179.16/297.04	Answer:
1179.16/297.04	  YES(?,O(n^1))
1179.16/297.04	
1179.16/297.04	The problem is match-bounded by 4. The enriched problem is
1179.16/297.04	compatible with the following automaton.
1179.16/297.04	{ b_0(1) -> 1
1179.16/297.04	, b_1(1) -> 9
1179.16/297.04	, b_1(2) -> 9
1179.16/297.04	, b_1(4) -> 3
1179.16/297.04	, b_1(6) -> 5
1179.16/297.04	, b_1(7) -> 6
1179.16/297.04	, b_1(18) -> 9
1179.16/297.04	, b_2(2) -> 17
1179.16/297.04	, b_2(5) -> 25
1179.16/297.04	, b_2(12) -> 11
1179.16/297.04	, b_2(14) -> 13
1179.16/297.04	, b_2(15) -> 14
1179.16/297.04	, b_2(18) -> 17
1179.16/297.04	, b_2(20) -> 19
1179.16/297.04	, b_2(21) -> 25
1179.16/297.04	, b_2(22) -> 21
1179.16/297.04	, b_2(23) -> 22
1179.16/297.04	, b_3(18) -> 33
1179.16/297.04	, b_3(21) -> 41
1179.16/297.04	, b_3(28) -> 27
1179.16/297.04	, b_3(30) -> 29
1179.16/297.04	, b_3(31) -> 30
1179.16/297.04	, b_3(34) -> 33
1179.16/297.04	, b_3(36) -> 35
1179.16/297.04	, b_3(38) -> 37
1179.16/297.04	, b_3(39) -> 38
1179.16/297.04	, b_4(37) -> 49
1179.16/297.04	, b_4(44) -> 43
1179.16/297.04	, b_4(46) -> 45
1179.16/297.04	, b_4(47) -> 46
1179.16/297.04	, a_0(1) -> 1
1179.16/297.04	, a_1(2) -> 1
1179.16/297.04	, a_1(2) -> 6
1179.16/297.04	, a_1(2) -> 9
1179.16/297.04	, a_1(3) -> 2
1179.16/297.04	, a_1(5) -> 4
1179.16/297.04	, a_1(8) -> 7
1179.16/297.04	, a_1(9) -> 8
1179.16/297.04	, a_2(10) -> 5
1179.16/297.04	, a_2(10) -> 9
1179.16/297.04	, a_2(11) -> 10
1179.16/297.04	, a_2(13) -> 12
1179.16/297.04	, a_2(16) -> 15
1179.16/297.04	, a_2(17) -> 16
1179.16/297.04	, a_2(18) -> 6
1179.16/297.04	, a_2(18) -> 14
1179.16/297.04	, a_2(19) -> 18
1179.16/297.04	, a_2(21) -> 20
1179.16/297.04	, a_2(24) -> 23
1179.16/297.04	, a_2(25) -> 24
1179.16/297.04	, a_3(26) -> 25
1179.16/297.04	, a_3(27) -> 26
1179.16/297.04	, a_3(29) -> 28
1179.16/297.04	, a_3(32) -> 31
1179.16/297.04	, a_3(33) -> 32
1179.16/297.04	, a_3(34) -> 14
1179.16/297.04	, a_3(34) -> 30
1179.16/297.04	, a_3(35) -> 34
1179.16/297.04	, a_3(37) -> 36
1179.16/297.04	, a_3(40) -> 39
1179.16/297.04	, a_3(41) -> 40
1179.16/297.04	, a_4(42) -> 30
1179.16/297.04	, a_4(43) -> 42
1179.16/297.04	, a_4(45) -> 44
1179.16/297.04	, a_4(48) -> 47
1179.16/297.04	, a_4(49) -> 48 }
1179.16/297.04	
1179.16/297.04	Hurray, we answered YES(?,O(n^1))
1179.85/297.65	EOF