YES(?,O(n^1))
864.54/297.03	YES(?,O(n^1))
864.54/297.03	
864.54/297.03	We are left with following problem, upon which TcT provides the
864.54/297.03	certificate YES(?,O(n^1)).
864.54/297.03	
864.54/297.03	Strict Trs:
864.54/297.03	  { 4(4(2(4(2(x1))))) -> 2(0(5(2(1(4(0(2(0(1(x1))))))))))
864.54/297.03	  , 4(4(0(5(4(2(2(x1))))))) -> 4(0(4(3(4(4(4(5(4(1(x1))))))))))
864.54/297.03	  , 4(2(4(x1))) -> 2(0(0(5(3(3(5(2(0(4(x1))))))))))
864.54/297.03	  , 4(1(4(5(0(5(4(x1))))))) -> 4(1(5(3(1(0(5(3(1(0(x1))))))))))
864.54/297.03	  , 0(5(4(2(4(3(x1)))))) -> 5(1(5(5(3(5(3(0(0(0(x1))))))))))
864.54/297.03	  , 5(4(5(3(2(4(3(x1))))))) -> 2(5(5(5(0(4(5(0(1(4(x1))))))))))
864.54/297.03	  , 3(2(4(2(4(1(x1)))))) -> 0(2(1(1(1(5(3(1(3(3(x1))))))))))
864.54/297.03	  , 3(3(0(4(1(2(x1)))))) -> 3(5(1(2(0(2(0(5(3(1(x1))))))))))
864.54/297.03	  , 3(1(4(3(1(2(x1)))))) -> 0(0(1(1(4(2(3(0(0(3(x1))))))))))
864.54/297.03	  , 1(1(4(5(3(3(x1)))))) -> 1(3(1(1(3(0(1(2(2(1(x1)))))))))) }
864.54/297.03	Obligation:
864.54/297.03	  derivational complexity
864.54/297.03	Answer:
864.54/297.03	  YES(?,O(n^1))
864.54/297.03	
864.54/297.03	The problem is match-bounded by 1. The enriched problem is
864.54/297.03	compatible with the following automaton.
864.54/297.03	{ 4_0(1) -> 1
864.54/297.03	, 4_1(1) -> 25
864.54/297.03	, 4_1(7) -> 6
864.54/297.03	, 4_1(10) -> 18
864.54/297.03	, 4_1(11) -> 1
864.54/297.03	, 4_1(11) -> 18
864.54/297.03	, 4_1(11) -> 25
864.54/297.03	, 4_1(13) -> 12
864.54/297.03	, 4_1(15) -> 14
864.54/297.03	, 4_1(16) -> 15
864.54/297.03	, 4_1(17) -> 16
864.54/297.03	, 4_1(45) -> 44
864.54/297.03	, 4_1(57) -> 25
864.54/297.03	, 4_1(68) -> 67
864.54/297.03	, 2_0(1) -> 1
864.54/297.03	, 2_1(2) -> 1
864.54/297.03	, 2_1(2) -> 25
864.54/297.03	, 2_1(5) -> 4
864.54/297.03	, 2_1(9) -> 8
864.54/297.03	, 2_1(10) -> 79
864.54/297.03	, 2_1(24) -> 23
864.54/297.03	, 2_1(49) -> 48
864.54/297.03	, 2_1(60) -> 59
864.54/297.03	, 2_1(62) -> 61
864.54/297.03	, 2_1(69) -> 68
864.54/297.03	, 2_1(79) -> 78
864.54/297.03	, 0_0(1) -> 1
864.54/297.03	, 0_1(1) -> 24
864.54/297.03	, 0_1(3) -> 2
864.54/297.03	, 0_1(8) -> 7
864.54/297.03	, 0_1(10) -> 9
864.54/297.03	, 0_1(11) -> 24
864.54/297.03	, 0_1(12) -> 11
864.54/297.03	, 0_1(19) -> 3
864.54/297.03	, 0_1(24) -> 40
864.54/297.03	, 0_1(25) -> 24
864.54/297.03	, 0_1(30) -> 29
864.54/297.03	, 0_1(40) -> 39
864.54/297.03	, 0_1(44) -> 43
864.54/297.03	, 0_1(47) -> 46
864.54/297.03	, 0_1(48) -> 1
864.54/297.03	, 0_1(48) -> 56
864.54/297.03	, 0_1(48) -> 64
864.54/297.03	, 0_1(56) -> 71
864.54/297.03	, 0_1(57) -> 24
864.54/297.03	, 0_1(61) -> 60
864.54/297.03	, 0_1(63) -> 62
864.54/297.03	, 0_1(65) -> 48
864.54/297.03	, 0_1(71) -> 70
864.54/297.03	, 0_1(77) -> 76
864.54/297.03	, 5_0(1) -> 1
864.54/297.03	, 5_1(4) -> 3
864.54/297.03	, 5_1(18) -> 17
864.54/297.03	, 5_1(20) -> 19
864.54/297.03	, 5_1(23) -> 22
864.54/297.03	, 5_1(27) -> 26
864.54/297.03	, 5_1(31) -> 30
864.54/297.03	, 5_1(33) -> 1
864.54/297.03	, 5_1(33) -> 24
864.54/297.03	, 5_1(35) -> 34
864.54/297.03	, 5_1(36) -> 35
864.54/297.03	, 5_1(38) -> 37
864.54/297.03	, 5_1(41) -> 2
864.54/297.03	, 5_1(42) -> 41
864.54/297.03	, 5_1(43) -> 42
864.54/297.03	, 5_1(46) -> 45
864.54/297.03	, 5_1(53) -> 52
864.54/297.03	, 5_1(58) -> 57
864.54/297.03	, 5_1(64) -> 63
864.54/297.03	, 3_0(1) -> 1
864.54/297.03	, 3_1(1) -> 56
864.54/297.03	, 3_1(2) -> 56
864.54/297.03	, 3_1(10) -> 64
864.54/297.03	, 3_1(14) -> 13
864.54/297.03	, 3_1(21) -> 20
864.54/297.03	, 3_1(22) -> 21
864.54/297.03	, 3_1(26) -> 56
864.54/297.03	, 3_1(28) -> 27
864.54/297.03	, 3_1(32) -> 31
864.54/297.03	, 3_1(37) -> 36
864.54/297.03	, 3_1(39) -> 38
864.54/297.03	, 3_1(54) -> 53
864.54/297.03	, 3_1(56) -> 55
864.54/297.03	, 3_1(57) -> 1
864.54/297.03	, 3_1(57) -> 55
864.54/297.03	, 3_1(57) -> 56
864.54/297.03	, 3_1(70) -> 69
864.54/297.03	, 3_1(72) -> 56
864.54/297.03	, 3_1(73) -> 72
864.54/297.03	, 3_1(76) -> 75
864.54/297.03	, 1_0(1) -> 1
864.54/297.03	, 1_1(1) -> 10
864.54/297.03	, 1_1(2) -> 10
864.54/297.03	, 1_1(6) -> 5
864.54/297.03	, 1_1(24) -> 32
864.54/297.03	, 1_1(25) -> 47
864.54/297.03	, 1_1(26) -> 11
864.54/297.03	, 1_1(29) -> 28
864.54/297.03	, 1_1(34) -> 33
864.54/297.03	, 1_1(50) -> 49
864.54/297.03	, 1_1(51) -> 50
864.54/297.03	, 1_1(52) -> 51
864.54/297.03	, 1_1(55) -> 54
864.54/297.03	, 1_1(57) -> 10
864.54/297.03	, 1_1(59) -> 58
864.54/297.03	, 1_1(66) -> 65
864.54/297.03	, 1_1(67) -> 66
864.54/297.03	, 1_1(72) -> 1
864.54/297.03	, 1_1(72) -> 10
864.54/297.03	, 1_1(74) -> 73
864.54/297.03	, 1_1(75) -> 74
864.54/297.03	, 1_1(78) -> 77 }
864.54/297.03	
864.54/297.03	Hurray, we answered YES(?,O(n^1))
865.27/297.72	EOF