We consider the following Problem: Strict Trs: { active(f(x)) -> mark(x) , top(active(c())) -> top(mark(c())) , top(mark(x)) -> top(check(x)) , check(f(x)) -> f(check(x)) , check(x) -> start(match(f(X()), x)) , match(f(x), f(y)) -> f(match(x, y)) , match(X(), x) -> proper(x) , proper(c()) -> ok(c()) , proper(f(x)) -> f(proper(x)) , f(ok(x)) -> ok(f(x)) , start(ok(x)) -> found(x) , f(found(x)) -> found(f(x)) , top(found(x)) -> top(active(x)) , active(f(x)) -> f(active(x)) , f(mark(x)) -> mark(f(x))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { active(f(x)) -> mark(x) , top(active(c())) -> top(mark(c())) , top(mark(x)) -> top(check(x)) , check(f(x)) -> f(check(x)) , check(x) -> start(match(f(X()), x)) , match(f(x), f(y)) -> f(match(x, y)) , match(X(), x) -> proper(x) , proper(c()) -> ok(c()) , proper(f(x)) -> f(proper(x)) , f(ok(x)) -> ok(f(x)) , start(ok(x)) -> found(x) , f(found(x)) -> found(f(x)) , top(found(x)) -> top(active(x)) , active(f(x)) -> f(active(x)) , f(mark(x)) -> mark(f(x))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { active(f(x)) -> mark(x) , top(active(c())) -> top(mark(c())) , start(ok(x)) -> found(x)} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1}, Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1}, Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(found) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 0] x1 + [1] [1 0] [1] f(x1) = [1 0] x1 + [0] [0 0] [1] mark(x1) = [1 0] x1 + [0] [0 0] [1] top(x1) = [1 0] x1 + [0] [0 0] [1] c() = [0] [0] check(x1) = [0 0] x1 + [0] [0 0] [1] start(x1) = [1 0] x1 + [1] [0 0] [1] match(x1, x2) = [0 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] X() = [0] [0] proper(x1) = [0 0] x1 + [1] [0 0] [1] ok(x1) = [1 0] x1 + [1] [0 0] [1] found(x1) = [1 0] x1 + [0] [0 0] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { top(mark(x)) -> top(check(x)) , check(f(x)) -> f(check(x)) , check(x) -> start(match(f(X()), x)) , match(f(x), f(y)) -> f(match(x, y)) , match(X(), x) -> proper(x) , proper(c()) -> ok(c()) , proper(f(x)) -> f(proper(x)) , f(ok(x)) -> ok(f(x)) , f(found(x)) -> found(f(x)) , top(found(x)) -> top(active(x)) , active(f(x)) -> f(active(x)) , f(mark(x)) -> mark(f(x))} Weak Trs: { active(f(x)) -> mark(x) , top(active(c())) -> top(mark(c())) , start(ok(x)) -> found(x)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {proper(c()) -> ok(c())} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1}, Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1}, Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(found) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 0] x1 + [0] [0 0] [1] f(x1) = [1 0] x1 + [1] [0 0] [1] mark(x1) = [1 0] x1 + [0] [0 0] [1] top(x1) = [1 0] x1 + [1] [0 0] [1] c() = [0] [0] check(x1) = [0 0] x1 + [0] [0 0] [1] start(x1) = [1 0] x1 + [1] [0 0] [1] match(x1, x2) = [0 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] X() = [0] [0] proper(x1) = [0 0] x1 + [1] [0 0] [1] ok(x1) = [1 0] x1 + [0] [0 0] [1] found(x1) = [1 0] x1 + [0] [0 0] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { top(mark(x)) -> top(check(x)) , check(f(x)) -> f(check(x)) , check(x) -> start(match(f(X()), x)) , match(f(x), f(y)) -> f(match(x, y)) , match(X(), x) -> proper(x) , proper(f(x)) -> f(proper(x)) , f(ok(x)) -> ok(f(x)) , f(found(x)) -> found(f(x)) , top(found(x)) -> top(active(x)) , active(f(x)) -> f(active(x)) , f(mark(x)) -> mark(f(x))} Weak Trs: { proper(c()) -> ok(c()) , active(f(x)) -> mark(x) , top(active(c())) -> top(mark(c())) , start(ok(x)) -> found(x)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {top(found(x)) -> top(active(x))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1}, Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1}, Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(found) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 0] x1 + [0] [0 0] [1] f(x1) = [1 0] x1 + [1] [0 0] [1] mark(x1) = [1 0] x1 + [0] [0 0] [1] top(x1) = [1 0] x1 + [1] [0 0] [1] c() = [0] [0] check(x1) = [0 0] x1 + [0] [0 0] [1] start(x1) = [1 0] x1 + [1] [0 0] [1] match(x1, x2) = [0 0] x1 + [0 0] x2 + [0] [0 0] [0 0] [1] X() = [0] [0] proper(x1) = [0 0] x1 + [1] [0 0] [1] ok(x1) = [1 0] x1 + [0] [0 0] [1] found(x1) = [1 0] x1 + [1] [0 0] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { top(mark(x)) -> top(check(x)) , check(f(x)) -> f(check(x)) , check(x) -> start(match(f(X()), x)) , match(f(x), f(y)) -> f(match(x, y)) , match(X(), x) -> proper(x) , proper(f(x)) -> f(proper(x)) , f(ok(x)) -> ok(f(x)) , f(found(x)) -> found(f(x)) , active(f(x)) -> f(active(x)) , f(mark(x)) -> mark(f(x))} Weak Trs: { top(found(x)) -> top(active(x)) , proper(c()) -> ok(c()) , active(f(x)) -> mark(x) , top(active(c())) -> top(mark(c())) , start(ok(x)) -> found(x)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {check(x) -> start(match(f(X()), x))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1}, Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1}, Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(found) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 0] x1 + [0] [1 0] [1] f(x1) = [1 0] x1 + [0] [0 0] [2] mark(x1) = [1 0] x1 + [0] [0 0] [1] top(x1) = [1 0] x1 + [0] [1 0] [1] c() = [0] [0] check(x1) = [0 0] x1 + [1] [1 0] [2] start(x1) = [1 0] x1 + [0] [0 0] [1] match(x1, x2) = [0 0] x1 + [0 0] x2 + [0] [0 1] [0 1] [1] X() = [0] [0] proper(x1) = [0 0] x1 + [1] [0 1] [3] ok(x1) = [1 0] x1 + [0] [0 0] [1] found(x1) = [1 0] x1 + [0] [0 0] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { top(mark(x)) -> top(check(x)) , check(f(x)) -> f(check(x)) , match(f(x), f(y)) -> f(match(x, y)) , match(X(), x) -> proper(x) , proper(f(x)) -> f(proper(x)) , f(ok(x)) -> ok(f(x)) , f(found(x)) -> found(f(x)) , active(f(x)) -> f(active(x)) , f(mark(x)) -> mark(f(x))} Weak Trs: { check(x) -> start(match(f(X()), x)) , top(found(x)) -> top(active(x)) , proper(c()) -> ok(c()) , active(f(x)) -> mark(x) , top(active(c())) -> top(mark(c())) , start(ok(x)) -> found(x)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {top(mark(x)) -> top(check(x))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1}, Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1}, Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(found) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 0] x1 + [0] [0 1] [0] f(x1) = [1 0] x1 + [0] [0 0] [2] mark(x1) = [1 0] x1 + [0] [0 0] [1] top(x1) = [1 2] x1 + [0] [0 0] [1] c() = [3] [1] check(x1) = [1 0] x1 + [0] [0 0] [0] start(x1) = [1 0] x1 + [0] [0 1] [0] match(x1, x2) = [0 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] X() = [0] [0] proper(x1) = [1 0] x1 + [1] [0 1] [3] ok(x1) = [1 0] x1 + [0] [0 1] [3] found(x1) = [1 0] x1 + [0] [0 1] [2] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { check(f(x)) -> f(check(x)) , match(f(x), f(y)) -> f(match(x, y)) , match(X(), x) -> proper(x) , proper(f(x)) -> f(proper(x)) , f(ok(x)) -> ok(f(x)) , f(found(x)) -> found(f(x)) , active(f(x)) -> f(active(x)) , f(mark(x)) -> mark(f(x))} Weak Trs: { top(mark(x)) -> top(check(x)) , check(x) -> start(match(f(X()), x)) , top(found(x)) -> top(active(x)) , proper(c()) -> ok(c()) , active(f(x)) -> mark(x) , top(active(c())) -> top(mark(c())) , start(ok(x)) -> found(x)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {match(f(x), f(y)) -> f(match(x, y))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1}, Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1}, Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(found) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 2] x1 + [0] [0 0] [0] f(x1) = [1 0] x1 + [0] [0 1] [1] mark(x1) = [1 2] x1 + [0] [0 0] [0] top(x1) = [1 0] x1 + [0] [0 0] [1] c() = [0] [0] check(x1) = [0 2] x1 + [0] [0 0] [3] start(x1) = [1 0] x1 + [0] [0 1] [2] match(x1, x2) = [0 0] x1 + [0 2] x2 + [0] [0 1] [0 0] [0] X() = [0] [0] proper(x1) = [0 0] x1 + [0] [0 0] [3] ok(x1) = [1 2] x1 + [0] [0 0] [2] found(x1) = [1 2] x1 + [0] [0 0] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { check(f(x)) -> f(check(x)) , match(X(), x) -> proper(x) , proper(f(x)) -> f(proper(x)) , f(ok(x)) -> ok(f(x)) , f(found(x)) -> found(f(x)) , active(f(x)) -> f(active(x)) , f(mark(x)) -> mark(f(x))} Weak Trs: { match(f(x), f(y)) -> f(match(x, y)) , top(mark(x)) -> top(check(x)) , check(x) -> start(match(f(X()), x)) , top(found(x)) -> top(active(x)) , proper(c()) -> ok(c()) , active(f(x)) -> mark(x) , top(active(c())) -> top(mark(c())) , start(ok(x)) -> found(x)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {match(X(), x) -> proper(x)} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1}, Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1}, Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(found) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 0] x1 + [1] [0 0] [0] f(x1) = [1 0] x1 + [0] [0 0] [0] mark(x1) = [1 0] x1 + [1] [0 0] [0] top(x1) = [1 0] x1 + [0] [0 0] [1] c() = [0] [0] check(x1) = [0 0] x1 + [1] [0 0] [0] start(x1) = [1 1] x1 + [0] [0 0] [0] match(x1, x2) = [0 0] x1 + [0 0] x2 + [1] [0 1] [0 0] [0] X() = [0] [2] proper(x1) = [0 0] x1 + [0] [0 0] [2] ok(x1) = [1 0] x1 + [0] [0 0] [2] found(x1) = [1 0] x1 + [1] [0 0] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { check(f(x)) -> f(check(x)) , proper(f(x)) -> f(proper(x)) , f(ok(x)) -> ok(f(x)) , f(found(x)) -> found(f(x)) , active(f(x)) -> f(active(x)) , f(mark(x)) -> mark(f(x))} Weak Trs: { match(X(), x) -> proper(x) , match(f(x), f(y)) -> f(match(x, y)) , top(mark(x)) -> top(check(x)) , check(x) -> start(match(f(X()), x)) , top(found(x)) -> top(active(x)) , proper(c()) -> ok(c()) , active(f(x)) -> mark(x) , top(active(c())) -> top(mark(c())) , start(ok(x)) -> found(x)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {check(f(x)) -> f(check(x))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1}, Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1}, Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(found) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 1] x1 + [0] [0 0] [2] f(x1) = [1 0] x1 + [0] [0 1] [2] mark(x1) = [1 1] x1 + [0] [0 0] [0] top(x1) = [1 0] x1 + [0] [0 0] [1] c() = [0] [0] check(x1) = [0 1] x1 + [0] [0 1] [2] start(x1) = [1 0] x1 + [0] [0 0] [1] match(x1, x2) = [0 0] x1 + [0 0] x2 + [0] [0 1] [0 0] [0] X() = [0] [0] proper(x1) = [0 0] x1 + [0] [0 0] [0] ok(x1) = [1 2] x1 + [0] [0 0] [0] found(x1) = [1 2] x1 + [0] [0 0] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { proper(f(x)) -> f(proper(x)) , f(ok(x)) -> ok(f(x)) , f(found(x)) -> found(f(x)) , active(f(x)) -> f(active(x)) , f(mark(x)) -> mark(f(x))} Weak Trs: { check(f(x)) -> f(check(x)) , match(X(), x) -> proper(x) , match(f(x), f(y)) -> f(match(x, y)) , top(mark(x)) -> top(check(x)) , check(x) -> start(match(f(X()), x)) , top(found(x)) -> top(active(x)) , proper(c()) -> ok(c()) , active(f(x)) -> mark(x) , top(active(c())) -> top(mark(c())) , start(ok(x)) -> found(x)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {proper(f(x)) -> f(proper(x))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1}, Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1}, Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(found) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 2] x1 + [0] [0 0] [3] f(x1) = [1 0] x1 + [0] [0 1] [1] mark(x1) = [1 2] x1 + [0] [0 0] [0] top(x1) = [1 0] x1 + [0] [0 0] [1] c() = [0] [0] check(x1) = [0 1] x1 + [0] [0 1] [0] start(x1) = [1 0] x1 + [0] [0 0] [0] match(x1, x2) = [0 0] x1 + [0 1] x2 + [0] [0 0] [0 1] [0] X() = [0] [0] proper(x1) = [0 1] x1 + [0] [0 1] [0] ok(x1) = [1 2] x1 + [0] [0 0] [0] found(x1) = [1 2] x1 + [0] [0 0] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { f(ok(x)) -> ok(f(x)) , f(found(x)) -> found(f(x)) , active(f(x)) -> f(active(x)) , f(mark(x)) -> mark(f(x))} Weak Trs: { proper(f(x)) -> f(proper(x)) , check(f(x)) -> f(check(x)) , match(X(), x) -> proper(x) , match(f(x), f(y)) -> f(match(x, y)) , top(mark(x)) -> top(check(x)) , check(x) -> start(match(f(X()), x)) , top(found(x)) -> top(active(x)) , proper(c()) -> ok(c()) , active(f(x)) -> mark(x) , top(active(c())) -> top(mark(c())) , start(ok(x)) -> found(x)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { f(ok(x)) -> ok(f(x)) , f(found(x)) -> found(f(x)) , active(f(x)) -> f(active(x)) , f(mark(x)) -> mark(f(x))} Weak Trs: { proper(f(x)) -> f(proper(x)) , check(f(x)) -> f(check(x)) , match(X(), x) -> proper(x) , match(f(x), f(y)) -> f(match(x, y)) , top(mark(x)) -> top(check(x)) , check(x) -> start(match(f(X()), x)) , top(found(x)) -> top(active(x)) , proper(c()) -> ok(c()) , active(f(x)) -> mark(x) , top(active(c())) -> top(mark(c())) , start(ok(x)) -> found(x)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The problem is match-bounded by 1. The enriched problem is compatible with the following automaton: { active_0(3) -> 1 , active_0(5) -> 1 , active_0(9) -> 1 , active_0(11) -> 1 , active_0(12) -> 1 , f_0(3) -> 2 , f_0(5) -> 2 , f_0(9) -> 2 , f_0(11) -> 2 , f_0(12) -> 2 , f_1(3) -> 14 , f_1(5) -> 14 , f_1(9) -> 14 , f_1(11) -> 14 , f_1(12) -> 14 , f_1(17) -> 16 , mark_0(3) -> 3 , mark_0(5) -> 3 , mark_0(9) -> 3 , mark_0(11) -> 3 , mark_0(12) -> 3 , mark_1(14) -> 2 , mark_1(14) -> 14 , top_0(1) -> 4 , top_0(3) -> 4 , top_0(5) -> 4 , top_0(6) -> 4 , top_0(9) -> 4 , top_0(11) -> 4 , top_0(12) -> 4 , c_0() -> 5 , check_0(3) -> 6 , check_0(5) -> 6 , check_0(9) -> 6 , check_0(11) -> 6 , check_0(12) -> 6 , start_0(3) -> 7 , start_0(5) -> 7 , start_0(9) -> 7 , start_0(11) -> 7 , start_0(12) -> 7 , start_0(13) -> 6 , start_1(15) -> 6 , match_0(2, 3) -> 13 , match_0(2, 5) -> 13 , match_0(2, 9) -> 13 , match_0(2, 11) -> 13 , match_0(2, 12) -> 13 , match_0(3, 3) -> 8 , match_0(3, 5) -> 8 , match_0(3, 9) -> 8 , match_0(3, 11) -> 8 , match_0(3, 12) -> 8 , match_0(5, 3) -> 8 , match_0(5, 5) -> 8 , match_0(5, 9) -> 8 , match_0(5, 11) -> 8 , match_0(5, 12) -> 8 , match_0(9, 3) -> 8 , match_0(9, 5) -> 8 , match_0(9, 9) -> 8 , match_0(9, 11) -> 8 , match_0(9, 12) -> 8 , match_0(11, 3) -> 8 , match_0(11, 5) -> 8 , match_0(11, 9) -> 8 , match_0(11, 11) -> 8 , match_0(11, 12) -> 8 , match_0(12, 3) -> 8 , match_0(12, 5) -> 8 , match_0(12, 9) -> 8 , match_0(12, 11) -> 8 , match_0(12, 12) -> 8 , match_1(16, 3) -> 15 , match_1(16, 5) -> 15 , match_1(16, 9) -> 15 , match_1(16, 11) -> 15 , match_1(16, 12) -> 15 , X_0() -> 9 , X_1() -> 17 , proper_0(3) -> 8 , proper_0(3) -> 10 , proper_0(5) -> 8 , proper_0(5) -> 10 , proper_0(9) -> 8 , proper_0(9) -> 10 , proper_0(11) -> 8 , proper_0(11) -> 10 , proper_0(12) -> 8 , proper_0(12) -> 10 , ok_0(3) -> 11 , ok_0(5) -> 8 , ok_0(5) -> 10 , ok_0(5) -> 11 , ok_0(9) -> 11 , ok_0(11) -> 11 , ok_0(12) -> 11 , ok_1(14) -> 2 , ok_1(14) -> 14 , found_0(3) -> 7 , found_0(3) -> 12 , found_0(5) -> 7 , found_0(5) -> 12 , found_0(9) -> 7 , found_0(9) -> 12 , found_0(11) -> 7 , found_0(11) -> 12 , found_0(12) -> 7 , found_0(12) -> 12 , found_1(14) -> 2 , found_1(14) -> 14} Hurray, we answered YES(?,O(n^1))