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