YES(?,O(n^1)) 739.09/297.13 YES(?,O(n^1)) 739.09/297.13 739.09/297.13 We are left with following problem, upon which TcT provides the 739.09/297.13 certificate YES(?,O(n^1)). 739.09/297.13 739.09/297.13 Strict Trs: 739.09/297.13 { active(incr(X)) -> incr(active(X)) 739.09/297.13 , active(incr(nil())) -> mark(nil()) 739.09/297.13 , active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))) 739.09/297.13 , active(cons(X1, X2)) -> cons(active(X1), X2) 739.09/297.13 , active(s(X)) -> s(active(X)) 739.09/297.13 , active(adx(X)) -> adx(active(X)) 739.09/297.13 , active(adx(nil())) -> mark(nil()) 739.09/297.13 , active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))) 739.09/297.13 , active(nats()) -> mark(adx(zeros())) 739.09/297.13 , active(zeros()) -> mark(cons(0(), zeros())) 739.09/297.13 , active(head(X)) -> head(active(X)) 739.09/297.13 , active(head(cons(X, L))) -> mark(X) 739.09/297.13 , active(tail(X)) -> tail(active(X)) 739.09/297.13 , active(tail(cons(X, L))) -> mark(L) 739.09/297.13 , incr(mark(X)) -> mark(incr(X)) 739.09/297.13 , incr(ok(X)) -> ok(incr(X)) 739.09/297.13 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 739.09/297.13 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 739.09/297.13 , s(mark(X)) -> mark(s(X)) 739.09/297.13 , s(ok(X)) -> ok(s(X)) 739.09/297.13 , adx(mark(X)) -> mark(adx(X)) 739.09/297.13 , adx(ok(X)) -> ok(adx(X)) 739.09/297.13 , head(mark(X)) -> mark(head(X)) 739.09/297.13 , head(ok(X)) -> ok(head(X)) 739.09/297.13 , tail(mark(X)) -> mark(tail(X)) 739.09/297.13 , tail(ok(X)) -> ok(tail(X)) 739.09/297.13 , proper(incr(X)) -> incr(proper(X)) 739.09/297.13 , proper(nil()) -> ok(nil()) 739.09/297.13 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 739.09/297.13 , proper(s(X)) -> s(proper(X)) 739.09/297.13 , proper(adx(X)) -> adx(proper(X)) 739.09/297.13 , proper(nats()) -> ok(nats()) 739.09/297.13 , proper(zeros()) -> ok(zeros()) 739.09/297.13 , proper(0()) -> ok(0()) 739.09/297.13 , proper(head(X)) -> head(proper(X)) 739.09/297.13 , proper(tail(X)) -> tail(proper(X)) 739.09/297.13 , top(mark(X)) -> top(proper(X)) 739.09/297.13 , top(ok(X)) -> top(active(X)) } 739.09/297.13 Obligation: 739.09/297.13 runtime complexity 739.09/297.13 Answer: 739.09/297.13 YES(?,O(n^1)) 739.09/297.13 739.09/297.13 The problem is match-bounded by 10. The enriched problem is 739.09/297.13 compatible with the following automaton. 739.09/297.13 { active_0(3) -> 1 739.09/297.13 , active_0(4) -> 1 739.09/297.13 , active_0(8) -> 1 739.09/297.13 , active_0(9) -> 1 739.09/297.13 , active_0(10) -> 1 739.09/297.13 , active_0(14) -> 1 739.09/297.13 , active_1(3) -> 26 739.09/297.13 , active_1(4) -> 26 739.09/297.13 , active_1(8) -> 26 739.09/297.13 , active_1(9) -> 26 739.09/297.13 , active_1(10) -> 26 739.09/297.13 , active_1(14) -> 26 739.09/297.13 , active_2(17) -> 27 739.09/297.13 , active_2(18) -> 27 739.09/297.13 , active_2(25) -> 27 739.09/297.13 , active_3(34) -> 33 739.09/297.13 , active_4(29) -> 40 739.09/297.13 , active_4(30) -> 39 739.09/297.13 , active_4(42) -> 44 739.09/297.13 , active_5(37) -> 46 739.09/297.13 , active_5(38) -> 45 739.09/297.13 , active_5(56) -> 51 739.09/297.13 , active_6(48) -> 67 739.09/297.13 , active_6(55) -> 54 739.09/297.13 , active_6(65) -> 66 739.09/297.13 , active_7(60) -> 77 739.09/297.13 , active_7(64) -> 68 739.09/297.13 , active_7(87) -> 76 739.09/297.13 , active_8(84) -> 98 739.09/297.13 , active_8(85) -> 79 739.09/297.13 , active_8(92) -> 93 739.09/297.13 , active_9(88) -> 94 739.09/297.13 , active_9(102) -> 115 739.09/297.13 , active_9(108) -> 120 739.09/297.13 , active_9(113) -> 101 739.09/297.13 , active_10(109) -> 119 739.09/297.13 , active_10(117) -> 118 739.09/297.13 , incr_0(3) -> 2 739.09/297.13 , incr_0(4) -> 2 739.09/297.13 , incr_0(8) -> 2 739.09/297.13 , incr_0(9) -> 2 739.09/297.13 , incr_0(10) -> 2 739.09/297.13 , incr_0(14) -> 2 739.09/297.13 , incr_1(3) -> 19 739.09/297.13 , incr_1(4) -> 19 739.09/297.13 , incr_1(8) -> 19 739.09/297.13 , incr_1(9) -> 19 739.09/297.13 , incr_1(10) -> 19 739.09/297.13 , incr_1(14) -> 19 739.09/297.13 , incr_6(62) -> 61 739.09/297.13 , incr_7(70) -> 69 739.09/297.13 , incr_7(72) -> 66 739.09/297.13 , incr_7(78) -> 91 739.09/297.13 , incr_7(85) -> 87 739.09/297.13 , incr_8(79) -> 76 739.09/297.13 , incr_8(86) -> 97 739.09/297.13 , incr_8(88) -> 92 739.09/297.13 , incr_8(103) -> 100 739.09/297.13 , incr_9(94) -> 93 739.09/297.13 , incr_9(110) -> 105 739.09/297.13 , incr_9(114) -> 116 739.09/297.13 , nil_0() -> 3 739.09/297.13 , nil_1() -> 25 739.09/297.13 , mark_0(3) -> 4 739.09/297.13 , mark_0(4) -> 4 739.09/297.13 , mark_0(8) -> 4 739.09/297.13 , mark_0(9) -> 4 739.09/297.13 , mark_0(10) -> 4 739.09/297.13 , mark_0(14) -> 4 739.09/297.13 , mark_1(16) -> 1 739.09/297.13 , mark_1(16) -> 26 739.09/297.13 , mark_1(19) -> 2 739.09/297.13 , mark_1(19) -> 19 739.09/297.13 , mark_1(20) -> 5 739.09/297.13 , mark_1(20) -> 20 739.09/297.13 , mark_1(21) -> 6 739.09/297.13 , mark_1(21) -> 21 739.09/297.13 , mark_1(22) -> 7 739.09/297.13 , mark_1(22) -> 22 739.09/297.13 , mark_1(23) -> 11 739.09/297.13 , mark_1(23) -> 23 739.09/297.13 , mark_1(24) -> 12 739.09/297.13 , mark_1(24) -> 24 739.09/297.13 , mark_2(28) -> 27 739.09/297.13 , mark_3(41) -> 40 739.09/297.13 , mark_4(43) -> 33 739.09/297.13 , mark_4(47) -> 46 739.09/297.13 , mark_5(50) -> 44 739.09/297.13 , mark_6(61) -> 51 739.09/297.13 , mark_7(69) -> 66 739.09/297.13 , mark_7(89) -> 76 739.09/297.13 , mark_8(95) -> 93 739.09/297.13 , cons_0(3, 3) -> 5 739.09/297.13 , cons_0(3, 4) -> 5 739.09/297.13 , cons_0(3, 8) -> 5 739.09/297.13 , cons_0(3, 9) -> 5 739.09/297.13 , cons_0(3, 10) -> 5 739.09/297.13 , cons_0(3, 14) -> 5 739.09/297.13 , cons_0(4, 3) -> 5 739.09/297.13 , cons_0(4, 4) -> 5 739.09/297.13 , cons_0(4, 8) -> 5 739.09/297.13 , cons_0(4, 9) -> 5 739.09/297.13 , cons_0(4, 10) -> 5 739.09/297.13 , cons_0(4, 14) -> 5 739.09/297.13 , cons_0(8, 3) -> 5 739.09/297.13 , cons_0(8, 4) -> 5 739.09/297.13 , cons_0(8, 8) -> 5 739.09/297.13 , cons_0(8, 9) -> 5 739.09/297.13 , cons_0(8, 10) -> 5 739.09/297.13 , cons_0(8, 14) -> 5 739.09/297.13 , cons_0(9, 3) -> 5 739.09/297.13 , cons_0(9, 4) -> 5 739.09/297.13 , cons_0(9, 8) -> 5 739.09/297.13 , cons_0(9, 9) -> 5 739.09/297.13 , cons_0(9, 10) -> 5 739.09/297.13 , cons_0(9, 14) -> 5 739.09/297.13 , cons_0(10, 3) -> 5 739.09/297.13 , cons_0(10, 4) -> 5 739.09/297.13 , cons_0(10, 8) -> 5 739.09/297.13 , cons_0(10, 9) -> 5 739.09/297.13 , cons_0(10, 10) -> 5 739.09/297.13 , cons_0(10, 14) -> 5 739.09/297.13 , cons_0(14, 3) -> 5 739.09/297.13 , cons_0(14, 4) -> 5 739.09/297.13 , cons_0(14, 8) -> 5 739.09/297.13 , cons_0(14, 9) -> 5 739.09/297.13 , cons_0(14, 10) -> 5 739.09/297.13 , cons_0(14, 14) -> 5 739.09/297.13 , cons_1(3, 3) -> 20 739.09/297.13 , cons_1(3, 4) -> 20 739.09/297.13 , cons_1(3, 8) -> 20 739.09/297.13 , cons_1(3, 9) -> 20 739.09/297.13 , cons_1(3, 10) -> 20 739.09/297.13 , cons_1(3, 14) -> 20 739.09/297.13 , cons_1(4, 3) -> 20 739.09/297.13 , cons_1(4, 4) -> 20 739.09/297.13 , cons_1(4, 8) -> 20 739.09/297.13 , cons_1(4, 9) -> 20 739.09/297.13 , cons_1(4, 10) -> 20 739.09/297.13 , cons_1(4, 14) -> 20 739.09/297.13 , cons_1(8, 3) -> 20 739.09/297.13 , cons_1(8, 4) -> 20 739.09/297.13 , cons_1(8, 8) -> 20 739.09/297.13 , cons_1(8, 9) -> 20 739.09/297.13 , cons_1(8, 10) -> 20 739.09/297.13 , cons_1(8, 14) -> 20 739.09/297.13 , cons_1(9, 3) -> 20 739.09/297.13 , cons_1(9, 4) -> 20 739.09/297.13 , cons_1(9, 8) -> 20 739.09/297.13 , cons_1(9, 9) -> 20 739.09/297.13 , cons_1(9, 10) -> 20 739.09/297.13 , cons_1(9, 14) -> 20 739.09/297.13 , cons_1(10, 3) -> 20 739.09/297.13 , cons_1(10, 4) -> 20 739.09/297.13 , cons_1(10, 8) -> 20 739.09/297.13 , cons_1(10, 9) -> 20 739.09/297.13 , cons_1(10, 10) -> 20 739.09/297.13 , cons_1(10, 14) -> 20 739.09/297.13 , cons_1(14, 3) -> 20 739.09/297.13 , cons_1(14, 4) -> 20 739.09/297.13 , cons_1(14, 8) -> 20 739.09/297.13 , cons_1(14, 9) -> 20 739.09/297.13 , cons_1(14, 10) -> 20 739.09/297.13 , cons_1(14, 14) -> 20 739.09/297.13 , cons_1(18, 17) -> 16 739.09/297.13 , cons_2(30, 29) -> 28 739.09/297.13 , cons_2(31, 32) -> 27 739.09/297.13 , cons_3(30, 29) -> 34 739.09/297.13 , cons_3(35, 36) -> 33 739.09/297.13 , cons_3(38, 37) -> 41 739.09/297.13 , cons_4(38, 37) -> 42 739.09/297.13 , cons_4(39, 29) -> 33 739.09/297.13 , cons_4(48, 49) -> 47 739.09/297.13 , cons_4(52, 53) -> 46 739.09/297.13 , cons_5(45, 37) -> 44 739.09/297.13 , cons_5(48, 49) -> 55 739.09/297.13 , cons_5(57, 58) -> 54 739.09/297.13 , cons_6(48, 63) -> 62 739.09/297.13 , cons_6(60, 59) -> 64 739.09/297.13 , cons_6(60, 78) -> 85 739.09/297.13 , cons_6(67, 49) -> 54 739.09/297.13 , cons_7(60, 71) -> 70 739.09/297.13 , cons_7(73, 74) -> 72 739.09/297.13 , cons_7(77, 59) -> 68 739.09/297.13 , cons_7(77, 78) -> 79 739.09/297.13 , cons_7(84, 86) -> 88 739.09/297.13 , cons_7(90, 91) -> 89 739.09/297.13 , cons_8(80, 81) -> 79 739.09/297.13 , cons_8(96, 97) -> 95 739.09/297.13 , cons_8(98, 86) -> 94 739.09/297.13 , cons_8(99, 100) -> 93 739.09/297.13 , cons_8(102, 97) -> 113 739.09/297.13 , cons_9(104, 105) -> 101 739.09/297.13 , cons_9(109, 116) -> 117 739.09/297.13 , cons_9(115, 97) -> 101 739.09/297.13 , cons_10(119, 116) -> 118 739.09/297.13 , s_0(3) -> 6 739.09/297.13 , s_0(4) -> 6 739.09/297.13 , s_0(8) -> 6 739.09/297.13 , s_0(9) -> 6 739.09/297.13 , s_0(10) -> 6 739.09/297.13 , s_0(14) -> 6 739.09/297.13 , s_1(3) -> 21 739.09/297.13 , s_1(4) -> 21 739.09/297.13 , s_1(8) -> 21 739.09/297.13 , s_1(9) -> 21 739.09/297.13 , s_1(10) -> 21 739.09/297.13 , s_1(14) -> 21 739.09/297.13 , s_7(60) -> 90 739.09/297.13 , s_7(84) -> 102 739.09/297.13 , s_8(80) -> 99 739.09/297.13 , s_8(84) -> 96 739.09/297.13 , s_8(98) -> 115 739.09/297.13 , s_8(108) -> 109 739.09/297.13 , s_9(106) -> 104 739.09/297.13 , s_9(120) -> 119 739.09/297.13 , adx_0(3) -> 7 739.09/297.13 , adx_0(4) -> 7 739.09/297.13 , adx_0(8) -> 7 739.09/297.14 , adx_0(9) -> 7 739.09/297.14 , adx_0(10) -> 7 739.09/297.14 , adx_0(14) -> 7 739.09/297.14 , adx_1(3) -> 22 739.09/297.14 , adx_1(4) -> 22 739.09/297.14 , adx_1(8) -> 22 739.09/297.14 , adx_1(9) -> 22 739.09/297.14 , adx_1(10) -> 22 739.09/297.14 , adx_1(14) -> 22 739.09/297.14 , adx_1(17) -> 16 739.09/297.14 , adx_2(29) -> 28 739.09/297.14 , adx_2(32) -> 27 739.09/297.14 , adx_3(29) -> 34 739.09/297.14 , adx_3(36) -> 33 739.09/297.14 , adx_4(37) -> 42 739.09/297.14 , adx_4(40) -> 33 739.09/297.14 , adx_4(41) -> 43 739.09/297.14 , adx_5(46) -> 44 739.09/297.14 , adx_5(47) -> 50 739.09/297.14 , adx_6(49) -> 63 739.09/297.14 , adx_6(54) -> 51 739.09/297.14 , adx_6(55) -> 56 739.09/297.14 , adx_6(59) -> 78 739.09/297.14 , adx_7(59) -> 71 739.09/297.14 , adx_7(64) -> 65 739.09/297.14 , adx_7(68) -> 66 739.09/297.14 , adx_7(75) -> 74 739.09/297.14 , adx_7(83) -> 86 739.09/297.14 , adx_7(107) -> 103 739.09/297.14 , adx_8(82) -> 81 739.09/297.14 , adx_8(111) -> 110 739.09/297.14 , adx_8(112) -> 114 739.09/297.14 , nats_0() -> 8 739.09/297.14 , nats_1() -> 25 739.09/297.14 , zeros_0() -> 9 739.09/297.14 , zeros_1() -> 17 739.09/297.14 , zeros_2() -> 29 739.09/297.14 , zeros_3() -> 37 739.09/297.14 , zeros_4() -> 49 739.09/297.14 , zeros_5() -> 59 739.09/297.14 , zeros_6() -> 83 739.09/297.14 , zeros_7() -> 112 739.09/297.14 , 0_0() -> 10 739.09/297.14 , 0_1() -> 18 739.09/297.14 , 0_2() -> 30 739.09/297.14 , 0_3() -> 38 739.09/297.14 , 0_4() -> 48 739.09/297.14 , 0_5() -> 60 739.09/297.14 , 0_6() -> 84 739.09/297.14 , 0_7() -> 108 739.09/297.14 , head_0(3) -> 11 739.09/297.14 , head_0(4) -> 11 739.09/297.14 , head_0(8) -> 11 739.09/297.14 , head_0(9) -> 11 739.09/297.14 , head_0(10) -> 11 739.09/297.14 , head_0(14) -> 11 739.09/297.14 , head_1(3) -> 23 739.09/297.14 , head_1(4) -> 23 739.09/297.14 , head_1(8) -> 23 739.09/297.14 , head_1(9) -> 23 739.09/297.14 , head_1(10) -> 23 739.09/297.14 , head_1(14) -> 23 739.09/297.14 , tail_0(3) -> 12 739.09/297.14 , tail_0(4) -> 12 739.09/297.14 , tail_0(8) -> 12 739.09/297.14 , tail_0(9) -> 12 739.09/297.14 , tail_0(10) -> 12 739.09/297.14 , tail_0(14) -> 12 739.09/297.14 , tail_1(3) -> 24 739.09/297.14 , tail_1(4) -> 24 739.09/297.14 , tail_1(8) -> 24 739.09/297.14 , tail_1(9) -> 24 739.09/297.14 , tail_1(10) -> 24 739.09/297.14 , tail_1(14) -> 24 739.09/297.14 , proper_0(3) -> 13 739.09/297.14 , proper_0(4) -> 13 739.09/297.14 , proper_0(8) -> 13 739.09/297.14 , proper_0(9) -> 13 739.09/297.14 , proper_0(10) -> 13 739.09/297.14 , proper_0(14) -> 13 739.09/297.14 , proper_1(3) -> 26 739.09/297.14 , proper_1(4) -> 26 739.09/297.14 , proper_1(8) -> 26 739.09/297.14 , proper_1(9) -> 26 739.09/297.14 , proper_1(10) -> 26 739.09/297.14 , proper_1(14) -> 26 739.09/297.14 , proper_2(16) -> 27 739.09/297.14 , proper_2(17) -> 32 739.09/297.14 , proper_2(18) -> 31 739.09/297.14 , proper_3(28) -> 33 739.09/297.14 , proper_3(29) -> 36 739.09/297.14 , proper_3(30) -> 35 739.09/297.14 , proper_4(37) -> 53 739.09/297.14 , proper_4(38) -> 52 739.09/297.14 , proper_4(43) -> 44 739.09/297.14 , proper_5(41) -> 46 739.09/297.14 , proper_5(48) -> 57 739.09/297.14 , proper_5(49) -> 58 739.09/297.14 , proper_5(50) -> 51 739.09/297.14 , proper_6(47) -> 54 739.09/297.14 , proper_6(61) -> 66 739.09/297.14 , proper_7(48) -> 73 739.09/297.14 , proper_7(49) -> 75 739.09/297.14 , proper_7(59) -> 107 739.09/297.14 , proper_7(62) -> 72 739.09/297.14 , proper_7(63) -> 74 739.09/297.14 , proper_7(69) -> 76 739.09/297.14 , proper_8(59) -> 82 739.09/297.14 , proper_8(60) -> 80 739.09/297.14 , proper_8(70) -> 79 739.09/297.14 , proper_8(71) -> 81 739.09/297.14 , proper_8(78) -> 103 739.09/297.14 , proper_8(83) -> 111 739.09/297.14 , proper_8(89) -> 93 739.09/297.14 , proper_8(90) -> 99 739.09/297.14 , proper_8(91) -> 100 739.09/297.14 , proper_9(84) -> 106 739.09/297.14 , proper_9(86) -> 110 739.09/297.14 , proper_9(95) -> 101 739.09/297.14 , proper_9(96) -> 104 739.09/297.14 , proper_9(97) -> 105 739.09/297.14 , ok_0(3) -> 14 739.09/297.14 , ok_0(4) -> 14 739.09/297.14 , ok_0(8) -> 14 739.09/297.14 , ok_0(9) -> 14 739.09/297.14 , ok_0(10) -> 14 739.09/297.14 , ok_0(14) -> 14 739.09/297.14 , ok_1(17) -> 13 739.09/297.14 , ok_1(17) -> 26 739.09/297.14 , ok_1(18) -> 13 739.09/297.14 , ok_1(18) -> 26 739.09/297.14 , ok_1(19) -> 2 739.09/297.14 , ok_1(19) -> 19 739.09/297.14 , ok_1(20) -> 5 739.09/297.14 , ok_1(20) -> 20 739.09/297.14 , ok_1(21) -> 6 739.09/297.14 , ok_1(21) -> 21 739.09/297.14 , ok_1(22) -> 7 739.09/297.14 , ok_1(22) -> 22 739.09/297.14 , ok_1(23) -> 11 739.09/297.14 , ok_1(23) -> 23 739.09/297.14 , ok_1(24) -> 12 739.09/297.14 , ok_1(24) -> 24 739.09/297.14 , ok_1(25) -> 13 739.09/297.14 , ok_1(25) -> 26 739.09/297.14 , ok_2(29) -> 32 739.09/297.14 , ok_2(30) -> 31 739.09/297.14 , ok_3(34) -> 27 739.09/297.14 , ok_3(37) -> 36 739.09/297.14 , ok_3(38) -> 35 739.09/297.14 , ok_4(42) -> 33 739.09/297.14 , ok_4(48) -> 52 739.09/297.14 , ok_4(49) -> 53 739.09/297.14 , ok_5(55) -> 46 739.09/297.14 , ok_5(59) -> 58 739.09/297.14 , ok_5(59) -> 75 739.09/297.14 , ok_5(60) -> 57 739.09/297.14 , ok_5(60) -> 73 739.09/297.14 , ok_6(56) -> 44 739.09/297.14 , ok_6(64) -> 54 739.09/297.14 , ok_6(78) -> 74 739.09/297.14 , ok_6(83) -> 82 739.09/297.14 , ok_6(83) -> 107 739.09/297.14 , ok_6(84) -> 80 739.09/297.14 , ok_6(85) -> 72 739.09/297.14 , ok_7(65) -> 51 739.09/297.14 , ok_7(86) -> 81 739.09/297.14 , ok_7(86) -> 103 739.09/297.14 , ok_7(87) -> 66 739.09/297.14 , ok_7(88) -> 79 739.09/297.14 , ok_7(102) -> 99 739.09/297.14 , ok_7(108) -> 106 739.09/297.14 , ok_7(112) -> 111 739.09/297.14 , ok_8(92) -> 76 739.09/297.14 , ok_8(97) -> 100 739.09/297.14 , ok_8(109) -> 104 739.09/297.14 , ok_8(113) -> 93 739.09/297.14 , ok_8(114) -> 110 739.09/297.14 , ok_9(116) -> 105 739.09/297.14 , ok_9(117) -> 101 739.09/297.14 , top_0(3) -> 15 739.09/297.14 , top_0(4) -> 15 739.09/297.14 , top_0(8) -> 15 739.09/297.14 , top_0(9) -> 15 739.09/297.14 , top_0(10) -> 15 739.09/297.14 , top_0(14) -> 15 739.09/297.14 , top_1(26) -> 15 739.09/297.14 , top_2(27) -> 15 739.09/297.14 , top_3(33) -> 15 739.09/297.14 , top_4(44) -> 15 739.09/297.14 , top_5(51) -> 15 739.09/297.14 , top_6(66) -> 15 739.09/297.14 , top_7(76) -> 15 739.09/297.14 , top_8(93) -> 15 739.09/297.14 , top_9(101) -> 15 739.09/297.14 , top_10(118) -> 15 } 739.09/297.14 739.09/297.14 Hurray, we answered YES(?,O(n^1)) 739.09/297.14 EOF