YES(?,O(n^1))
1157.27/297.02	YES(?,O(n^1))
1157.27/297.02	
1157.27/297.02	We are left with following problem, upon which TcT provides the
1157.27/297.02	certificate YES(?,O(n^1)).
1157.27/297.02	
1157.27/297.02	Strict Trs:
1157.27/297.02	  { c(a(b(a(b(x1))))) -> a(b(a(b(b(a(b(b(c(a(b(c(a(x1))))))))))))) }
1157.27/297.02	Obligation:
1157.27/297.02	  derivational complexity
1157.27/297.02	Answer:
1157.27/297.02	  YES(?,O(n^1))
1157.27/297.02	
1157.27/297.02	The problem is match-bounded by 3. The enriched problem is
1157.27/297.02	compatible with the following automaton.
1157.27/297.02	{ c_0(1) -> 1
1157.27/297.02	, c_1(10) -> 9
1157.27/297.02	, c_1(13) -> 12
1157.27/297.02	, c_2(22) -> 21
1157.27/297.02	, c_2(25) -> 24
1157.27/297.02	, c_2(34) -> 33
1157.27/297.02	, c_2(37) -> 36
1157.27/297.02	, c_2(46) -> 45
1157.27/297.02	, c_2(49) -> 48
1157.27/297.02	, c_3(58) -> 57
1157.27/297.02	, c_3(61) -> 60
1157.27/297.02	, a_0(1) -> 1
1157.27/297.02	, a_1(1) -> 13
1157.27/297.02	, a_1(2) -> 1
1157.27/297.02	, a_1(2) -> 12
1157.27/297.02	, a_1(3) -> 13
1157.27/297.02	, a_1(4) -> 3
1157.27/297.02	, a_1(5) -> 13
1157.27/297.02	, a_1(7) -> 6
1157.27/297.02	, a_1(11) -> 10
1157.27/297.02	, a_2(3) -> 25
1157.27/297.02	, a_2(8) -> 37
1157.27/297.02	, a_2(14) -> 9
1157.27/297.02	, a_2(15) -> 49
1157.27/297.02	, a_2(16) -> 15
1157.27/297.02	, a_2(19) -> 18
1157.27/297.02	, a_2(23) -> 22
1157.27/297.02	, a_2(26) -> 12
1157.27/297.02	, a_2(27) -> 25
1157.27/297.02	, a_2(28) -> 27
1157.27/297.02	, a_2(31) -> 30
1157.27/297.02	, a_2(35) -> 34
1157.27/297.02	, a_2(38) -> 36
1157.27/297.02	, a_2(40) -> 39
1157.27/297.02	, a_2(43) -> 42
1157.27/297.02	, a_2(47) -> 46
1157.27/297.02	, a_3(39) -> 61
1157.27/297.02	, a_3(50) -> 33
1157.27/297.02	, a_3(52) -> 51
1157.27/297.02	, a_3(55) -> 54
1157.27/297.02	, a_3(59) -> 58
1157.27/297.02	, b_0(1) -> 1
1157.27/297.02	, b_1(3) -> 2
1157.27/297.02	, b_1(5) -> 4
1157.27/297.02	, b_1(6) -> 5
1157.27/297.02	, b_1(8) -> 7
1157.27/297.02	, b_1(9) -> 8
1157.27/297.02	, b_1(12) -> 11
1157.27/297.02	, b_2(15) -> 14
1157.27/297.02	, b_2(17) -> 16
1157.27/297.02	, b_2(18) -> 17
1157.27/297.02	, b_2(20) -> 19
1157.27/297.02	, b_2(21) -> 20
1157.27/297.02	, b_2(24) -> 23
1157.27/297.02	, b_2(27) -> 26
1157.27/297.02	, b_2(29) -> 28
1157.27/297.02	, b_2(30) -> 29
1157.27/297.02	, b_2(32) -> 31
1157.27/297.02	, b_2(33) -> 32
1157.27/297.02	, b_2(36) -> 35
1157.27/297.02	, b_2(39) -> 38
1157.27/297.02	, b_2(41) -> 40
1157.27/297.02	, b_2(42) -> 41
1157.27/297.02	, b_2(44) -> 43
1157.27/297.02	, b_2(45) -> 44
1157.27/297.02	, b_2(48) -> 47
1157.27/297.02	, b_3(51) -> 50
1157.27/297.02	, b_3(53) -> 52
1157.27/297.02	, b_3(54) -> 53
1157.27/297.02	, b_3(56) -> 55
1157.27/297.02	, b_3(57) -> 56
1157.27/297.02	, b_3(60) -> 59 }
1157.27/297.02	
1157.27/297.02	Hurray, we answered YES(?,O(n^1))
1157.82/297.59	EOF