MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { r(x, y) -> r[Ite](e(x, y), x, y) , head(Cons(x, xs)) -> x , equal(B(), B()) -> True() , equal(B(), A()) -> False() , equal(B(), T()) -> False() , equal(B(), F()) -> False() , equal(A(), B()) -> False() , equal(A(), A()) -> True() , equal(A(), T()) -> False() , equal(A(), F()) -> False() , equal(T(), B()) -> False() , equal(T(), A()) -> False() , equal(T(), T()) -> True() , equal(T(), F()) -> False() , equal(F(), B()) -> False() , equal(F(), A()) -> False() , equal(F(), T()) -> False() , equal(F(), F()) -> True() , e(Cons(B(), Cons(x, xs)), b) -> False() , e(Cons(B(), Nil()), b) -> False() , e(Cons(A(), Cons(x, xs)), b) -> False() , e(Cons(A(), Nil()), b) -> e[Match][Cons][Ite][True][Match](A(), Nil(), b) , e(Cons(T(), Cons(x, xs)), b) -> False() , e(Cons(T(), Nil()), b) -> False() , e(Cons(F(), Cons(x, xs)), b) -> False() , e(Cons(F(), Nil()), b) -> False() , e(Nil(), b) -> False() , goal(x, y) -> q(x, y) , p(x, y) -> p[Ite](e(x, y), x, y) , t(x, y) -> t[Ite](e(x, y), x, y) , q(x, y) -> q[Ite](e(x, y), x, y) , notEmpty(Cons(x, xs)) -> True() , notEmpty(Nil()) -> False() } Weak Trs: { t[Ite](True(), x, y) -> True() , t[Ite](False(), x, y) -> True() , p[Ite](True(), x, y) -> True() , p[Ite](False(), x, Cons(B(), xs)) -> False() , p[Ite](False(), x, Cons(A(), xs)) -> False() , p[Ite](False(), x, Cons(T(), xs)) -> False() , p[Ite](False(), x', Cons(F(), xs)) -> and(r(x', Cons(F(), xs)), p(x', xs)) , q[Ite][False][Ite](True(), x', Cons(x, xs)) -> q[Ite][False][Ite][True][Ite](and(p(x', Cons(x, xs)), q(x', xs)), x', Cons(x, xs)) , q[Ite][False][Ite](False(), x, y) -> False() , q[Ite](True(), x, y) -> True() , q[Ite](False(), x, Cons(B(), Cons(B(), xs))) -> False() , q[Ite](False(), x, Cons(B(), Cons(A(), xs))) -> False() , q[Ite](False(), x, Cons(B(), Cons(T(), xs))) -> False() , q[Ite](False(), x, Cons(B(), Cons(F(), xs))) -> False() , q[Ite](False(), x', Cons(B(), Nil())) -> q[Ite][False][Ite](and(True(), and(False(), and(False(), equal(head(Nil()), F())))), x', Cons(B(), Nil())) , q[Ite](False(), x, Cons(A(), Cons(B(), xs))) -> False() , q[Ite](False(), x, Cons(A(), Cons(A(), xs))) -> False() , q[Ite](False(), x, Cons(A(), Cons(T(), xs))) -> False() , q[Ite](False(), x, Cons(A(), Cons(F(), xs))) -> False() , q[Ite](False(), x', Cons(A(), Nil())) -> q[Ite][False][Ite](and(True(), and(False(), and(False(), equal(head(Nil()), F())))), x', Cons(A(), Nil())) , q[Ite](False(), x, Cons(T(), Cons(B(), xs))) -> False() , q[Ite](False(), x, Cons(T(), Cons(A(), xs))) -> False() , q[Ite](False(), x, Cons(T(), Cons(T(), xs))) -> False() , q[Ite](False(), x, Cons(T(), Cons(F(), xs))) -> False() , q[Ite](False(), x', Cons(T(), Nil())) -> q[Ite][False][Ite](and(True(), and(False(), and(False(), equal(head(Nil()), F())))), x', Cons(T(), Nil())) , q[Ite](False(), x, Cons(F(), Cons(B(), xs))) -> False() , q[Ite](False(), x, Cons(F(), Cons(A(), xs))) -> False() , q[Ite](False(), x, Cons(F(), Cons(T(), xs))) -> False() , q[Ite](False(), x', Cons(F(), Cons(F(), xs))) -> q[Ite][False][Ite][True][Ite](and(p(x', Cons(F(), Cons(F(), xs))), q(x', Cons(F(), xs))), x', Cons(F(), Cons(F(), xs))) , q[Ite](False(), x', Cons(F(), Nil())) -> q[Ite][False][Ite](and(True(), and(True(), and(False(), equal(head(Nil()), F())))), x', Cons(F(), Nil())) , r[Ite](True(), x, y) -> True() , r[Ite](False(), x, Cons(B(), xs)) -> False() , r[Ite](False(), x, Cons(A(), xs)) -> False() , r[Ite](False(), x, Cons(T(), xs)) -> False() , r[Ite](False(), x', Cons(F(), xs)) -> r[Ite][False][Ite][True][Ite](and(q(x', xs), r(x', xs)), x', Cons(F(), xs)) , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Best' failed due to the following reason: 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) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 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. Arrrr..