MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { colorrest(cs, ncs, colorednodes, Cons(x, xs)) -> colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs)) , colorrest(cs, ncs, colorednodes, Nil()) -> colorednodes , getNodeName(N(name, adjs)) -> name , getAdjs(N(n, ns)) -> ns , possible(color, Cons(x, xs), colorednodes) -> possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes) , possible(color, Nil(), colorednodes) -> True() , eqColor(NoColor(), b) -> False() , eqColor(Blue(), NoColor()) -> False() , eqColor(Blue(), Blue()) -> True() , eqColor(Blue(), Red()) -> False() , eqColor(Blue(), Yellow()) -> False() , eqColor(Red(), NoColor()) -> False() , eqColor(Red(), Blue()) -> False() , eqColor(Red(), Red()) -> True() , eqColor(Red(), Yellow()) -> False() , eqColor(Yellow(), NoColor()) -> False() , eqColor(Yellow(), Blue()) -> False() , eqColor(Yellow(), Red()) -> False() , eqColor(Yellow(), Yellow()) -> True() , colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) -> colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest) , colorednoderest(cs, Nil(), node, colorednodes, rest) -> Nil() , reverse(xs) -> revapp(xs, Nil()) , colornode(Cons(x, xs), N(n, ns), colorednodes) -> colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes) , colornode(Nil(), node, colorednodes) -> NotPossible() , eqColorList(Cons(c1, cs1), Nil()) -> False() , eqColorList(Cons(NoColor(), cs1), Cons(b, cs2)) -> and(False(), eqColorList(cs1, cs2)) , eqColorList(Cons(Blue(), cs1), Cons(NoColor(), cs2)) -> and(False(), eqColorList(cs1, cs2)) , eqColorList(Cons(Blue(), cs1), Cons(Blue(), cs2)) -> and(True(), eqColorList(cs1, cs2)) , eqColorList(Cons(Blue(), cs1), Cons(Red(), cs2)) -> and(False(), eqColorList(cs1, cs2)) , eqColorList(Cons(Blue(), cs1), Cons(Yellow(), cs2)) -> and(False(), eqColorList(cs1, cs2)) , eqColorList(Cons(Red(), cs1), Cons(NoColor(), cs2)) -> and(False(), eqColorList(cs1, cs2)) , eqColorList(Cons(Red(), cs1), Cons(Blue(), cs2)) -> and(False(), eqColorList(cs1, cs2)) , eqColorList(Cons(Red(), cs1), Cons(Red(), cs2)) -> and(True(), eqColorList(cs1, cs2)) , eqColorList(Cons(Red(), cs1), Cons(Yellow(), cs2)) -> and(False(), eqColorList(cs1, cs2)) , eqColorList(Cons(Yellow(), cs1), Cons(NoColor(), cs2)) -> and(False(), eqColorList(cs1, cs2)) , eqColorList(Cons(Yellow(), cs1), Cons(Blue(), cs2)) -> and(False(), eqColorList(cs1, cs2)) , eqColorList(Cons(Yellow(), cs1), Cons(Red(), cs2)) -> and(False(), eqColorList(cs1, cs2)) , eqColorList(Cons(Yellow(), cs1), Cons(Yellow(), cs2)) -> and(True(), eqColorList(cs1, cs2)) , eqColorList(Nil(), Cons(c2, cs2)) -> False() , eqColorList(Nil(), Nil()) -> True() , graphcolour(Cons(x, xs), cs) -> reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil()), Nil()), xs)) , getNodeFromCN(CN(cl, n)) -> n , colorrestthetrick(cs1, cs, ncs, colorednodes, rest) -> colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest) , colorof(node, Cons(CN(cl, N(name, adjs)), xs)) -> colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs)) , colorof(node, Nil()) -> NoColor() , getColorListFromCN(CN(cl, n)) -> cl , notEmpty(Cons(x, xs)) -> True() , notEmpty(Nil()) -> False() , revapp(Cons(x, xs), rest) -> revapp(xs, Cons(x, rest)) , revapp(Nil(), rest) -> rest } Weak Trs: { colornode[Ite][True][Ite](True(), cs, node, colorednodes) -> CN(cs, node) , colornode[Ite][True][Ite](False(), Cons(x, xs), node, colorednodes) -> colornode(xs, node, colorednodes) , !EQ(S(x), S(y)) -> !EQ(x, y) , !EQ(S(x), 0()) -> False() , !EQ(0(), S(y)) -> False() , !EQ(0(), 0()) -> True() , possible[Ite][True][Ite](True(), color, adjs, colorednodes) -> False() , possible[Ite][True][Ite](False(), color, Cons(x, xs), colorednodes) -> possible(color, xs, colorednodes) , colorof[Ite][True][Ite](True(), node, Cons(CN(Cons(x, xs), n), xs')) -> x , colorof[Ite][True][Ite](False(), node, Cons(x, xs)) -> colorof(node, xs) , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() , colorrestthetrick[Ite](True(), cs1, cs, ncs, colorednodes, rest) -> colorrest(cs, ncs, colorednodes, rest) , colorrestthetrick[Ite](False(), Cons(x, xs), cs, ncs, colorednodes, rest) -> colorrestthetrick(xs, cs, ncs, colorednodes, rest) , colorednoderest[Ite][True][Ite](True(), cs, ncs, node, colorednodes, Cons(x, xs)) -> colorednoderest[Ite][True][Ite][True][Let](cs, ncs, node, colorednodes, Cons(x, xs), colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs)) , colorednoderest[Ite][True][Ite](False(), cs, Cons(x, xs), node, colorednodes, rest) -> colorednoderest(cs, xs, node, colorednodes, rest) } 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) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'bsearch-popstar (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 minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..