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