MAYBE 971.06/297.05 MAYBE 971.06/297.05 971.06/297.05 We are left with following problem, upon which TcT provides the 971.06/297.05 certificate MAYBE. 971.06/297.05 971.06/297.05 Strict Trs: 971.06/297.05 { r(x, y) -> r[Ite](e(x, y), x, y) 971.06/297.05 , head(Cons(x, xs)) -> x 971.06/297.05 , equal(B(), B()) -> True() 971.06/297.05 , equal(B(), A()) -> False() 971.06/297.05 , equal(B(), T()) -> False() 971.06/297.05 , equal(B(), F()) -> False() 971.06/297.05 , equal(A(), B()) -> False() 971.06/297.05 , equal(A(), A()) -> True() 971.06/297.05 , equal(A(), T()) -> False() 971.06/297.05 , equal(A(), F()) -> False() 971.06/297.05 , equal(T(), B()) -> False() 971.06/297.05 , equal(T(), A()) -> False() 971.06/297.05 , equal(T(), T()) -> True() 971.06/297.05 , equal(T(), F()) -> False() 971.06/297.05 , equal(F(), B()) -> False() 971.06/297.05 , equal(F(), A()) -> False() 971.06/297.05 , equal(F(), T()) -> False() 971.06/297.05 , equal(F(), F()) -> True() 971.06/297.05 , e(Cons(B(), Cons(x, xs)), b) -> False() 971.06/297.05 , e(Cons(B(), Nil()), b) -> False() 971.06/297.05 , e(Cons(A(), Cons(x, xs)), b) -> False() 971.06/297.05 , e(Cons(A(), Nil()), b) -> 971.06/297.05 e[Match][Cons][Ite][True][Match](A(), Nil(), b) 971.06/297.05 , e(Cons(T(), Cons(x, xs)), b) -> False() 971.06/297.05 , e(Cons(T(), Nil()), b) -> False() 971.06/297.05 , e(Cons(F(), Cons(x, xs)), b) -> False() 971.06/297.05 , e(Cons(F(), Nil()), b) -> False() 971.06/297.05 , e(Nil(), b) -> False() 971.06/297.05 , goal(x, y) -> q(x, y) 971.06/297.05 , p(x, y) -> p[Ite](e(x, y), x, y) 971.06/297.05 , t(x, y) -> t[Ite](e(x, y), x, y) 971.06/297.05 , q(x, y) -> q[Ite](e(x, y), x, y) 971.06/297.05 , notEmpty(Cons(x, xs)) -> True() 971.06/297.05 , notEmpty(Nil()) -> False() } 971.06/297.05 Weak Trs: 971.06/297.05 { t[Ite](True(), x, y) -> True() 971.06/297.05 , t[Ite](False(), x, y) -> True() 971.06/297.05 , p[Ite](True(), x, y) -> True() 971.06/297.05 , p[Ite](False(), x, Cons(B(), xs)) -> False() 971.06/297.05 , p[Ite](False(), x, Cons(A(), xs)) -> False() 971.06/297.05 , p[Ite](False(), x, Cons(T(), xs)) -> False() 971.06/297.05 , p[Ite](False(), x', Cons(F(), xs)) -> 971.06/297.05 and(r(x', Cons(F(), xs)), p(x', xs)) 971.06/297.05 , q[Ite][False][Ite](True(), x', Cons(x, xs)) -> 971.06/297.05 q[Ite][False][Ite][True][Ite](and(p(x', Cons(x, xs)), q(x', xs)), 971.06/297.05 x', 971.06/297.05 Cons(x, xs)) 971.06/297.05 , q[Ite][False][Ite](False(), x, y) -> False() 971.06/297.05 , q[Ite](True(), x, y) -> True() 971.06/297.05 , q[Ite](False(), x, Cons(B(), Cons(B(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x, Cons(B(), Cons(A(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x, Cons(B(), Cons(T(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x, Cons(B(), Cons(F(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x', Cons(B(), Nil())) -> 971.06/297.05 q[Ite][False][Ite](and(True(), 971.06/297.05 and(False(), and(False(), equal(head(Nil()), F())))), 971.06/297.05 x', 971.06/297.05 Cons(B(), Nil())) 971.06/297.05 , q[Ite](False(), x, Cons(A(), Cons(B(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x, Cons(A(), Cons(A(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x, Cons(A(), Cons(T(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x, Cons(A(), Cons(F(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x', Cons(A(), Nil())) -> 971.06/297.05 q[Ite][False][Ite](and(True(), 971.06/297.05 and(False(), and(False(), equal(head(Nil()), F())))), 971.06/297.05 x', 971.06/297.05 Cons(A(), Nil())) 971.06/297.05 , q[Ite](False(), x, Cons(T(), Cons(B(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x, Cons(T(), Cons(A(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x, Cons(T(), Cons(T(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x, Cons(T(), Cons(F(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x', Cons(T(), Nil())) -> 971.06/297.05 q[Ite][False][Ite](and(True(), 971.06/297.05 and(False(), and(False(), equal(head(Nil()), F())))), 971.06/297.05 x', 971.06/297.05 Cons(T(), Nil())) 971.06/297.05 , q[Ite](False(), x, Cons(F(), Cons(B(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x, Cons(F(), Cons(A(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x, Cons(F(), Cons(T(), xs))) -> False() 971.06/297.05 , q[Ite](False(), x', Cons(F(), Cons(F(), xs))) -> 971.06/297.05 q[Ite][False][Ite][True][Ite](and(p(x', Cons(F(), Cons(F(), xs))), 971.06/297.05 q(x', Cons(F(), xs))), 971.06/297.05 x', 971.06/297.05 Cons(F(), Cons(F(), xs))) 971.06/297.05 , q[Ite](False(), x', Cons(F(), Nil())) -> 971.06/297.05 q[Ite][False][Ite](and(True(), 971.06/297.05 and(True(), and(False(), equal(head(Nil()), F())))), 971.06/297.05 x', 971.06/297.05 Cons(F(), Nil())) 971.06/297.05 , r[Ite](True(), x, y) -> True() 971.06/297.05 , r[Ite](False(), x, Cons(B(), xs)) -> False() 971.06/297.05 , r[Ite](False(), x, Cons(A(), xs)) -> False() 971.06/297.05 , r[Ite](False(), x, Cons(T(), xs)) -> False() 971.06/297.05 , r[Ite](False(), x', Cons(F(), xs)) -> 971.06/297.05 r[Ite][False][Ite][True][Ite](and(q(x', xs), r(x', xs)), 971.06/297.05 x', 971.06/297.05 Cons(F(), xs)) 971.06/297.05 , and(True(), True()) -> True() 971.06/297.05 , and(True(), False()) -> False() 971.06/297.05 , and(False(), True()) -> False() 971.06/297.05 , and(False(), False()) -> False() } 971.06/297.05 Obligation: 971.06/297.05 innermost runtime complexity 971.06/297.05 Answer: 971.06/297.05 MAYBE 971.06/297.05 971.06/297.05 None of the processors succeeded. 971.06/297.05 971.06/297.05 Details of failed attempt(s): 971.06/297.05 ----------------------------- 971.06/297.05 1) 'empty' failed due to the following reason: 971.06/297.05 971.06/297.05 Empty strict component of the problem is NOT empty. 971.06/297.05 971.06/297.05 2) 'Best' failed due to the following reason: 971.06/297.05 971.06/297.05 None of the processors succeeded. 971.06/297.05 971.06/297.05 Details of failed attempt(s): 971.06/297.05 ----------------------------- 971.06/297.05 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 971.06/297.05 following reason: 971.06/297.05 971.06/297.05 Computation stopped due to timeout after 297.0 seconds. 971.06/297.05 971.06/297.05 2) 'Best' failed due to the following reason: 971.06/297.05 971.06/297.05 None of the processors succeeded. 971.06/297.05 971.06/297.05 Details of failed attempt(s): 971.06/297.05 ----------------------------- 971.06/297.05 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 971.06/297.05 seconds)' failed due to the following reason: 971.06/297.05 971.06/297.05 Computation stopped due to timeout after 148.0 seconds. 971.06/297.05 971.06/297.05 2) 'Best' failed due to the following reason: 971.06/297.05 971.06/297.05 None of the processors succeeded. 971.06/297.05 971.06/297.05 Details of failed attempt(s): 971.06/297.05 ----------------------------- 971.06/297.05 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 971.06/297.05 following reason: 971.06/297.05 971.06/297.05 The input cannot be shown compatible 971.06/297.05 971.06/297.05 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 971.06/297.05 to the following reason: 971.06/297.05 971.06/297.05 The input cannot be shown compatible 971.06/297.05 971.06/297.05 971.06/297.05 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 971.06/297.05 failed due to the following reason: 971.06/297.05 971.06/297.05 None of the processors succeeded. 971.06/297.05 971.06/297.05 Details of failed attempt(s): 971.06/297.05 ----------------------------- 971.06/297.05 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 971.06/297.05 failed due to the following reason: 971.06/297.05 971.06/297.05 match-boundness of the problem could not be verified. 971.06/297.05 971.06/297.05 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 971.06/297.05 failed due to the following reason: 971.06/297.05 971.06/297.05 match-boundness of the problem could not be verified. 971.06/297.05 971.06/297.05 971.06/297.05 971.06/297.05 971.06/297.05 971.06/297.05 Arrrr.. 971.21/297.18 EOF