MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , quot(0(), s(y)) -> 0() , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) , shuffle(nil()) -> nil() , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) , concat(leaf(), y) -> y , concat(cons(u, v), y) -> cons(u, concat(v, y)) , less_leaves(x, leaf()) -> false() , less_leaves(leaf(), cons(w, z)) -> true() , less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z)) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { minus^#(x, 0()) -> c_1(x) , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , quot^#(0(), s(y)) -> c_3() , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) , app^#(nil(), y) -> c_5(y) , app^#(add(n, x), y) -> c_6(n, app^#(x, y)) , reverse^#(nil()) -> c_7() , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil()))) , shuffle^#(nil()) -> c_9() , shuffle^#(add(n, x)) -> c_10(n, shuffle^#(reverse(x))) , concat^#(leaf(), y) -> c_11(y) , concat^#(cons(u, v), y) -> c_12(u, concat^#(v, y)) , less_leaves^#(x, leaf()) -> c_13() , less_leaves^#(leaf(), cons(w, z)) -> c_14() , less_leaves^#(cons(u, v), cons(w, z)) -> c_15(less_leaves^#(concat(u, v), concat(w, z))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { minus^#(x, 0()) -> c_1(x) , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , quot^#(0(), s(y)) -> c_3() , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) , app^#(nil(), y) -> c_5(y) , app^#(add(n, x), y) -> c_6(n, app^#(x, y)) , reverse^#(nil()) -> c_7() , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil()))) , shuffle^#(nil()) -> c_9() , shuffle^#(add(n, x)) -> c_10(n, shuffle^#(reverse(x))) , concat^#(leaf(), y) -> c_11(y) , concat^#(cons(u, v), y) -> c_12(u, concat^#(v, y)) , less_leaves^#(x, leaf()) -> c_13() , less_leaves^#(leaf(), cons(w, z)) -> c_14() , less_leaves^#(cons(u, v), cons(w, z)) -> c_15(less_leaves^#(concat(u, v), concat(w, z))) } Strict Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , quot(0(), s(y)) -> 0() , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) , shuffle(nil()) -> nil() , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) , concat(leaf(), y) -> y , concat(cons(u, v), y) -> cons(u, concat(v, y)) , less_leaves(x, leaf()) -> false() , less_leaves(leaf(), cons(w, z)) -> true() , less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z)) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {3,7,9,13,14} by applications of Pre({3,7,9,13,14}) = {1,4,5,6,10,11,12,15}. Here rules are labeled as follows: DPs: { 1: minus^#(x, 0()) -> c_1(x) , 2: minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , 3: quot^#(0(), s(y)) -> c_3() , 4: quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) , 5: app^#(nil(), y) -> c_5(y) , 6: app^#(add(n, x), y) -> c_6(n, app^#(x, y)) , 7: reverse^#(nil()) -> c_7() , 8: reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil()))) , 9: shuffle^#(nil()) -> c_9() , 10: shuffle^#(add(n, x)) -> c_10(n, shuffle^#(reverse(x))) , 11: concat^#(leaf(), y) -> c_11(y) , 12: concat^#(cons(u, v), y) -> c_12(u, concat^#(v, y)) , 13: less_leaves^#(x, leaf()) -> c_13() , 14: less_leaves^#(leaf(), cons(w, z)) -> c_14() , 15: less_leaves^#(cons(u, v), cons(w, z)) -> c_15(less_leaves^#(concat(u, v), concat(w, z))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { minus^#(x, 0()) -> c_1(x) , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) , app^#(nil(), y) -> c_5(y) , app^#(add(n, x), y) -> c_6(n, app^#(x, y)) , reverse^#(add(n, x)) -> c_8(app^#(reverse(x), add(n, nil()))) , shuffle^#(add(n, x)) -> c_10(n, shuffle^#(reverse(x))) , concat^#(leaf(), y) -> c_11(y) , concat^#(cons(u, v), y) -> c_12(u, concat^#(v, y)) , less_leaves^#(cons(u, v), cons(w, z)) -> c_15(less_leaves^#(concat(u, v), concat(w, z))) } Strict Trs: { minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) , quot(0(), s(y)) -> 0() , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , app(nil(), y) -> y , app(add(n, x), y) -> add(n, app(x, y)) , reverse(nil()) -> nil() , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) , shuffle(nil()) -> nil() , shuffle(add(n, x)) -> add(n, shuffle(reverse(x))) , concat(leaf(), y) -> y , concat(cons(u, v), y) -> cons(u, concat(v, y)) , less_leaves(x, leaf()) -> false() , less_leaves(leaf(), cons(w, z)) -> true() , less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z)) } Weak DPs: { quot^#(0(), s(y)) -> c_3() , reverse^#(nil()) -> c_7() , shuffle^#(nil()) -> c_9() , less_leaves^#(x, leaf()) -> c_13() , less_leaves^#(leaf(), cons(w, z)) -> c_14() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..