YES(?,O(n^1))
1180.81/297.05	YES(?,O(n^1))
1180.81/297.05	
1180.81/297.05	We are left with following problem, upon which TcT provides the
1180.81/297.05	certificate YES(?,O(n^1)).
1180.81/297.05	
1180.81/297.05	Strict Trs:
1180.81/297.05	  { f(a(), f(a(), f(b(), f(a(), f(a(), f(b(), f(a(), x))))))) ->
1180.81/297.05	    f(a(),
1180.81/297.05	      f(b(),
1180.81/297.05	        f(a(), f(a(), f(b(), f(a(), f(a(), f(a(), f(b(), x))))))))) }
1180.81/297.05	Obligation:
1180.81/297.05	  derivational complexity
1180.81/297.05	Answer:
1180.81/297.05	  YES(?,O(n^1))
1180.81/297.05	
1180.81/297.05	We uncurry the input using the following uncurry rules.
1180.81/297.05	
1180.81/297.05	  { f(a(), x_1) -> a_1(x_1)
1180.81/297.05	  , f(b(), x_1) -> b_1(x_1) }
1180.81/297.05	
1180.81/297.05	We are left with following problem, upon which TcT provides the
1180.81/297.05	certificate YES(?,O(n^1)).
1180.81/297.05	
1180.81/297.05	Strict Trs:
1180.81/297.05	  { a_1(a_1(b_1(a_1(a_1(b_1(a_1(x))))))) ->
1180.81/297.05	    a_1(b_1(a_1(a_1(b_1(a_1(a_1(a_1(b_1(x))))))))) }
1180.81/297.05	Weak Trs:
1180.81/297.05	  { f(a(), x_1) -> a_1(x_1)
1180.81/297.05	  , f(b(), x_1) -> b_1(x_1) }
1180.81/297.05	Obligation:
1180.81/297.05	  derivational complexity
1180.81/297.05	Answer:
1180.81/297.05	  YES(?,O(n^1))
1180.81/297.05	
1180.81/297.05	The problem is match-bounded by 3. The enriched problem is
1180.81/297.05	compatible with the following automaton.
1180.81/297.05	{ f_0(1, 1) -> 1
1180.81/297.05	, f_0(1, 2) -> 1
1180.81/297.05	, f_0(1, 3) -> 1
1180.81/297.05	, f_0(1, 4) -> 1
1180.81/297.05	, f_0(1, 5) -> 1
1180.81/297.05	, f_0(2, 1) -> 1
1180.81/297.05	, f_0(2, 2) -> 1
1180.81/297.05	, f_0(2, 3) -> 1
1180.81/297.05	, f_0(2, 4) -> 1
1180.81/297.05	, f_0(2, 5) -> 1
1180.81/297.05	, f_0(3, 1) -> 1
1180.81/297.05	, f_0(3, 2) -> 1
1180.81/297.05	, f_0(3, 3) -> 1
1180.81/297.05	, f_0(3, 4) -> 1
1180.81/297.05	, f_0(3, 5) -> 1
1180.81/297.05	, f_0(4, 1) -> 1
1180.81/297.05	, f_0(4, 2) -> 1
1180.81/297.05	, f_0(4, 3) -> 1
1180.81/297.05	, f_0(4, 4) -> 1
1180.81/297.05	, f_0(4, 5) -> 1
1180.81/297.05	, f_0(5, 1) -> 1
1180.81/297.05	, f_0(5, 2) -> 1
1180.81/297.05	, f_0(5, 3) -> 1
1180.81/297.05	, f_0(5, 4) -> 1
1180.81/297.05	, f_0(5, 5) -> 1
1180.81/297.05	, a_1_0(1) -> 1
1180.81/297.05	, a_1_0(1) -> 2
1180.81/297.05	, a_1_0(2) -> 1
1180.81/297.05	, a_1_0(2) -> 2
1180.81/297.05	, a_1_0(3) -> 1
1180.81/297.05	, a_1_0(3) -> 2
1180.81/297.05	, a_1_0(4) -> 1
1180.81/297.05	, a_1_0(4) -> 2
1180.81/297.05	, a_1_0(5) -> 1
1180.81/297.05	, a_1_0(5) -> 2
1180.81/297.05	, a_1_1(6) -> 1
1180.81/297.05	, a_1_1(6) -> 2
1180.81/297.05	, a_1_1(6) -> 11
1180.81/297.05	, a_1_1(6) -> 38
1180.81/297.05	, a_1_1(8) -> 7
1180.81/297.05	, a_1_1(9) -> 8
1180.81/297.05	, a_1_1(11) -> 10
1180.81/297.05	, a_1_1(12) -> 11
1180.81/297.05	, a_1_1(13) -> 12
1180.81/297.05	, a_1_2(17) -> 11
1180.81/297.05	, a_1_2(17) -> 38
1180.81/297.05	, a_1_2(17) -> 65
1180.81/297.05	, a_1_2(19) -> 18
1180.81/297.05	, a_1_2(20) -> 19
1180.81/297.05	, a_1_2(22) -> 21
1180.81/297.05	, a_1_2(23) -> 22
1180.81/297.05	, a_1_2(24) -> 23
1180.81/297.05	, a_1_2(25) -> 7
1180.81/297.05	, a_1_2(25) -> 34
1180.81/297.05	, a_1_2(27) -> 26
1180.81/297.05	, a_1_2(28) -> 27
1180.81/297.05	, a_1_2(30) -> 29
1180.81/297.05	, a_1_2(31) -> 30
1180.81/297.05	, a_1_2(32) -> 31
1180.81/297.05	, a_1_2(33) -> 10
1180.81/297.05	, a_1_2(33) -> 37
1180.81/297.05	, a_1_2(35) -> 34
1180.81/297.05	, a_1_2(36) -> 35
1180.81/297.05	, a_1_2(38) -> 37
1180.81/297.05	, a_1_2(39) -> 38
1180.81/297.05	, a_1_2(40) -> 39
1180.81/297.05	, a_1_3(52) -> 34
1180.81/297.05	, a_1_3(52) -> 61
1180.81/297.05	, a_1_3(54) -> 53
1180.81/297.05	, a_1_3(55) -> 54
1180.81/297.05	, a_1_3(57) -> 56
1180.81/297.05	, a_1_3(58) -> 57
1180.81/297.05	, a_1_3(59) -> 58
1180.81/297.05	, a_1_3(60) -> 37
1180.81/297.05	, a_1_3(60) -> 64
1180.81/297.05	, a_1_3(62) -> 61
1180.81/297.05	, a_1_3(63) -> 62
1180.81/297.05	, a_1_3(65) -> 64
1180.81/297.05	, a_1_3(66) -> 65
1180.81/297.05	, a_1_3(67) -> 66
1180.81/297.05	, b_1_0(1) -> 1
1180.81/297.05	, b_1_0(1) -> 3
1180.81/297.05	, b_1_0(2) -> 1
1180.81/297.05	, b_1_0(2) -> 3
1180.81/297.05	, b_1_0(3) -> 1
1180.81/297.05	, b_1_0(3) -> 3
1180.81/297.05	, b_1_0(4) -> 1
1180.81/297.05	, b_1_0(4) -> 3
1180.81/297.05	, b_1_0(5) -> 1
1180.81/297.05	, b_1_0(5) -> 3
1180.81/297.05	, b_1_1(1) -> 13
1180.81/297.05	, b_1_1(2) -> 13
1180.81/297.05	, b_1_1(3) -> 13
1180.81/297.05	, b_1_1(4) -> 13
1180.81/297.05	, b_1_1(5) -> 13
1180.81/297.05	, b_1_1(6) -> 13
1180.81/297.05	, b_1_1(7) -> 6
1180.81/297.05	, b_1_1(8) -> 13
1180.81/297.05	, b_1_1(10) -> 9
1180.81/297.05	, b_1_1(11) -> 13
1180.81/297.05	, b_1_1(25) -> 13
1180.81/297.05	, b_1_1(33) -> 13
1180.81/297.05	, b_1_2(6) -> 24
1180.81/297.05	, b_1_2(8) -> 32
1180.81/297.05	, b_1_2(9) -> 24
1180.81/297.05	, b_1_2(11) -> 40
1180.81/297.05	, b_1_2(12) -> 24
1180.81/297.05	, b_1_2(13) -> 24
1180.81/297.05	, b_1_2(17) -> 24
1180.81/297.05	, b_1_2(18) -> 17
1180.81/297.05	, b_1_2(19) -> 32
1180.81/297.05	, b_1_2(21) -> 20
1180.81/297.05	, b_1_2(22) -> 40
1180.81/297.05	, b_1_2(25) -> 32
1180.81/297.05	, b_1_2(26) -> 25
1180.81/297.05	, b_1_2(29) -> 28
1180.81/297.05	, b_1_2(33) -> 40
1180.81/297.05	, b_1_2(34) -> 33
1180.81/297.05	, b_1_2(37) -> 36
1180.81/297.05	, b_1_3(19) -> 59
1180.81/297.05	, b_1_3(22) -> 67
1180.81/297.05	, b_1_3(53) -> 52
1180.81/297.05	, b_1_3(56) -> 55
1180.81/297.05	, b_1_3(61) -> 60
1180.81/297.05	, b_1_3(64) -> 63
1180.81/297.05	, a_0() -> 4
1180.81/297.05	, b_0() -> 5 }
1180.81/297.05	
1180.81/297.05	Hurray, we answered YES(?,O(n^1))
1181.56/297.66	EOF