YES(?,O(n^1))
377.29/181.26	YES(?,O(n^1))
377.29/181.26	
377.29/181.26	We are left with following problem, upon which TcT provides the
377.29/181.26	certificate YES(?,O(n^1)).
377.29/181.26	
377.29/181.26	Strict Trs:
377.29/181.26	  { 0(1(2(3(4(x1))))) -> 0(2(3(1(4(x1)))))
377.29/181.26	  , 0(5(1(2(3(4(x1)))))) -> 0(1(2(5(3(4(x1))))))
377.29/181.26	  , 0(5(1(2(3(4(x1)))))) -> 0(5(2(1(3(4(x1))))))
377.29/181.26	  , 0(5(1(2(3(4(x1)))))) -> 5(0(2(3(1(4(x1))))))
377.29/181.26	  , 0(5(2(3(1(4(x1)))))) -> 0(1(5(2(3(4(x1)))))) }
377.29/181.26	Obligation:
377.29/181.26	  derivational complexity
377.29/181.26	Answer:
377.29/181.26	  YES(?,O(n^1))
377.29/181.26	
377.29/181.26	The problem is match-bounded by 1. The enriched problem is
377.29/181.26	compatible with the following automaton.
377.29/181.26	{ 0_0(1) -> 1
377.29/181.26	, 0_0(2) -> 1
377.29/181.26	, 0_0(3) -> 1
377.29/181.26	, 0_0(4) -> 1
377.29/181.26	, 0_0(5) -> 1
377.29/181.26	, 0_0(6) -> 1
377.29/181.26	, 0_1(7) -> 1
377.29/181.26	, 1_0(1) -> 2
377.29/181.26	, 1_0(2) -> 2
377.29/181.26	, 1_0(3) -> 2
377.29/181.26	, 1_0(4) -> 2
377.29/181.26	, 1_0(5) -> 2
377.29/181.26	, 1_0(6) -> 2
377.29/181.26	, 1_1(10) -> 9
377.29/181.26	, 1_1(11) -> 7
377.29/181.26	, 1_1(13) -> 15
377.29/181.26	, 2_0(1) -> 3
377.29/181.26	, 2_0(2) -> 3
377.29/181.26	, 2_0(3) -> 3
377.29/181.26	, 2_0(4) -> 3
377.29/181.26	, 2_0(5) -> 3
377.29/181.26	, 2_0(6) -> 3
377.29/181.26	, 2_1(8) -> 7
377.29/181.26	, 2_1(12) -> 11
377.29/181.26	, 2_1(13) -> 16
377.29/181.26	, 2_1(15) -> 14
377.29/181.26	, 3_0(1) -> 4
377.29/181.26	, 3_0(2) -> 4
377.29/181.26	, 3_0(3) -> 4
377.29/181.26	, 3_0(4) -> 4
377.29/181.26	, 3_0(5) -> 4
377.29/181.26	, 3_0(6) -> 4
377.29/181.26	, 3_1(9) -> 8
377.29/181.26	, 3_1(10) -> 13
377.29/181.26	, 4_0(1) -> 5
377.29/181.26	, 4_0(2) -> 5
377.29/181.26	, 4_0(3) -> 5
377.29/181.26	, 4_0(4) -> 5
377.29/181.26	, 4_0(5) -> 5
377.29/181.26	, 4_0(6) -> 5
377.29/181.26	, 4_1(1) -> 10
377.29/181.26	, 4_1(2) -> 10
377.29/181.26	, 4_1(3) -> 10
377.29/181.26	, 4_1(4) -> 10
377.29/181.26	, 4_1(5) -> 10
377.29/181.26	, 4_1(6) -> 10
377.29/181.26	, 5_0(1) -> 6
377.29/181.26	, 5_0(2) -> 6
377.29/181.26	, 5_0(3) -> 6
377.29/181.26	, 5_0(4) -> 6
377.29/181.26	, 5_0(5) -> 6
377.29/181.26	, 5_0(6) -> 6
377.29/181.26	, 5_1(1) -> 1
377.29/181.26	, 5_1(13) -> 12
377.29/181.26	, 5_1(14) -> 7
377.29/181.26	, 5_1(16) -> 11 }
377.29/181.26	
377.29/181.26	Hurray, we answered YES(?,O(n^1))
377.57/181.32	EOF