MAYBE 1183.43/297.29 MAYBE 1183.43/297.29 1183.43/297.29 We are left with following problem, upon which TcT provides the 1183.43/297.29 certificate MAYBE. 1183.43/297.29 1183.43/297.29 Strict Trs: 1183.43/297.29 { colorrest(cs, ncs, colorednodes, Cons(x, xs)) -> 1183.43/297.29 colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs)) 1183.43/297.29 , colorrest(cs, ncs, colorednodes, Nil()) -> colorednodes 1183.43/297.29 , getNodeName(N(name, adjs)) -> name 1183.43/297.29 , getAdjs(N(n, ns)) -> ns 1183.43/297.29 , possible(color, Cons(x, xs), colorednodes) -> 1183.43/297.29 possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), 1183.43/297.29 color, 1183.43/297.29 Cons(x, xs), 1183.43/297.29 colorednodes) 1183.43/297.29 , possible(color, Nil(), colorednodes) -> True() 1183.43/297.29 , eqColor(NoColor(), b) -> False() 1183.43/297.29 , eqColor(Blue(), NoColor()) -> False() 1183.43/297.29 , eqColor(Blue(), Blue()) -> True() 1183.43/297.29 , eqColor(Blue(), Red()) -> False() 1183.43/297.29 , eqColor(Blue(), Yellow()) -> False() 1183.43/297.29 , eqColor(Red(), NoColor()) -> False() 1183.43/297.29 , eqColor(Red(), Blue()) -> False() 1183.43/297.29 , eqColor(Red(), Red()) -> True() 1183.43/297.29 , eqColor(Red(), Yellow()) -> False() 1183.43/297.29 , eqColor(Yellow(), NoColor()) -> False() 1183.43/297.30 , eqColor(Yellow(), Blue()) -> False() 1183.43/297.30 , eqColor(Yellow(), Red()) -> False() 1183.43/297.30 , eqColor(Yellow(), Yellow()) -> True() 1183.43/297.30 , colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) -> 1183.43/297.30 colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), 1183.43/297.30 cs, 1183.43/297.30 Cons(x, xs), 1183.43/297.30 N(n, ns), 1183.43/297.30 colorednodes, 1183.43/297.30 rest) 1183.43/297.30 , colorednoderest(cs, Nil(), node, colorednodes, rest) -> Nil() 1183.43/297.30 , reverse(xs) -> revapp(xs, Nil()) 1183.43/297.30 , colornode(Cons(x, xs), N(n, ns), colorednodes) -> 1183.43/297.30 colornode[Ite][True][Ite](possible(x, ns, colorednodes), 1183.43/297.30 Cons(x, xs), 1183.43/297.30 N(n, ns), 1183.43/297.30 colorednodes) 1183.43/297.30 , colornode(Nil(), node, colorednodes) -> NotPossible() 1183.43/297.30 , eqColorList(Cons(c1, cs1), Nil()) -> False() 1183.43/297.30 , eqColorList(Cons(NoColor(), cs1), Cons(b, cs2)) -> 1183.43/297.30 and(False(), eqColorList(cs1, cs2)) 1183.43/297.30 , eqColorList(Cons(Blue(), cs1), Cons(NoColor(), cs2)) -> 1183.43/297.30 and(False(), eqColorList(cs1, cs2)) 1183.43/297.30 , eqColorList(Cons(Blue(), cs1), Cons(Blue(), cs2)) -> 1183.43/297.30 and(True(), eqColorList(cs1, cs2)) 1183.43/297.30 , eqColorList(Cons(Blue(), cs1), Cons(Red(), cs2)) -> 1183.43/297.30 and(False(), eqColorList(cs1, cs2)) 1183.43/297.30 , eqColorList(Cons(Blue(), cs1), Cons(Yellow(), cs2)) -> 1183.43/297.30 and(False(), eqColorList(cs1, cs2)) 1183.43/297.30 , eqColorList(Cons(Red(), cs1), Cons(NoColor(), cs2)) -> 1183.43/297.30 and(False(), eqColorList(cs1, cs2)) 1183.43/297.30 , eqColorList(Cons(Red(), cs1), Cons(Blue(), cs2)) -> 1183.43/297.30 and(False(), eqColorList(cs1, cs2)) 1183.43/297.30 , eqColorList(Cons(Red(), cs1), Cons(Red(), cs2)) -> 1183.43/297.30 and(True(), eqColorList(cs1, cs2)) 1183.43/297.30 , eqColorList(Cons(Red(), cs1), Cons(Yellow(), cs2)) -> 1183.43/297.30 and(False(), eqColorList(cs1, cs2)) 1183.43/297.30 , eqColorList(Cons(Yellow(), cs1), Cons(NoColor(), cs2)) -> 1183.43/297.30 and(False(), eqColorList(cs1, cs2)) 1183.43/297.30 , eqColorList(Cons(Yellow(), cs1), Cons(Blue(), cs2)) -> 1183.43/297.30 and(False(), eqColorList(cs1, cs2)) 1183.43/297.30 , eqColorList(Cons(Yellow(), cs1), Cons(Red(), cs2)) -> 1183.43/297.30 and(False(), eqColorList(cs1, cs2)) 1183.43/297.30 , eqColorList(Cons(Yellow(), cs1), Cons(Yellow(), cs2)) -> 1183.43/297.30 and(True(), eqColorList(cs1, cs2)) 1183.43/297.30 , eqColorList(Nil(), Cons(c2, cs2)) -> False() 1183.43/297.30 , eqColorList(Nil(), Nil()) -> True() 1183.43/297.30 , graphcolour(Cons(x, xs), cs) -> 1183.43/297.30 reverse(colorrest(cs, 1183.43/297.30 cs, 1183.43/297.30 Cons(colornode(cs, x, Nil()), Nil()), 1183.43/297.30 xs)) 1183.43/297.30 , getNodeFromCN(CN(cl, n)) -> n 1183.43/297.30 , colorrestthetrick(cs1, cs, ncs, colorednodes, rest) -> 1183.43/297.30 colorrestthetrick[Ite](eqColorList(cs1, ncs), 1183.43/297.30 cs1, 1183.43/297.30 cs, 1183.43/297.30 ncs, 1183.43/297.30 colorednodes, 1183.43/297.30 rest) 1183.43/297.30 , colorof(node, Cons(CN(cl, N(name, adjs)), xs)) -> 1183.43/297.30 colorof[Ite][True][Ite](!EQ(name, node), 1183.43/297.30 node, 1183.43/297.30 Cons(CN(cl, N(name, adjs)), xs)) 1183.43/297.30 , colorof(node, Nil()) -> NoColor() 1183.43/297.30 , getColorListFromCN(CN(cl, n)) -> cl 1183.43/297.30 , notEmpty(Cons(x, xs)) -> True() 1183.43/297.30 , notEmpty(Nil()) -> False() 1183.43/297.30 , revapp(Cons(x, xs), rest) -> revapp(xs, Cons(x, rest)) 1183.43/297.30 , revapp(Nil(), rest) -> rest } 1183.43/297.30 Weak Trs: 1183.43/297.30 { colornode[Ite][True][Ite](True(), cs, node, colorednodes) -> 1183.43/297.30 CN(cs, node) 1183.43/297.30 , colornode[Ite][True][Ite](False(), 1183.43/297.30 Cons(x, xs), 1183.43/297.30 node, 1183.43/297.30 colorednodes) 1183.43/297.30 -> colornode(xs, node, colorednodes) 1183.43/297.30 , !EQ(S(x), S(y)) -> !EQ(x, y) 1183.43/297.30 , !EQ(S(x), 0()) -> False() 1183.43/297.30 , !EQ(0(), S(y)) -> False() 1183.43/297.30 , !EQ(0(), 0()) -> True() 1183.43/297.30 , possible[Ite][True][Ite](True(), color, adjs, colorednodes) -> 1183.43/297.30 False() 1183.43/297.30 , possible[Ite][True][Ite](False(), 1183.43/297.30 color, 1183.43/297.30 Cons(x, xs), 1183.43/297.30 colorednodes) 1183.43/297.30 -> possible(color, xs, colorednodes) 1183.43/297.30 , colorof[Ite][True][Ite](True(), 1183.43/297.30 node, 1183.43/297.30 Cons(CN(Cons(x, xs), n), xs')) 1183.43/297.30 -> x 1183.43/297.30 , colorof[Ite][True][Ite](False(), node, Cons(x, xs)) -> 1183.43/297.30 colorof(node, xs) 1183.43/297.30 , and(True(), True()) -> True() 1183.43/297.30 , and(True(), False()) -> False() 1183.43/297.30 , and(False(), True()) -> False() 1183.43/297.30 , and(False(), False()) -> False() 1183.43/297.30 , colorrestthetrick[Ite](True(), cs1, cs, ncs, colorednodes, rest) 1183.43/297.30 -> colorrest(cs, cs1, colorednodes, rest) 1183.43/297.30 , colorrestthetrick[Ite](False(), 1183.43/297.30 Cons(x, xs), 1183.43/297.30 cs, 1183.43/297.30 ncs, 1183.43/297.30 colorednodes, 1183.43/297.30 rest) 1183.43/297.30 -> colorrestthetrick(xs, cs, ncs, colorednodes, rest) 1183.43/297.30 , colorednoderest[Ite][True][Ite](True(), 1183.43/297.30 cs, 1183.43/297.30 ncs, 1183.43/297.30 node, 1183.43/297.30 colorednodes, 1183.43/297.30 Cons(x, xs)) 1183.43/297.30 -> 1183.43/297.30 colorednoderest[Ite][True][Ite][True][Let](cs, 1183.43/297.30 ncs, 1183.43/297.30 node, 1183.43/297.30 colorednodes, 1183.43/297.30 Cons(x, xs), 1183.43/297.30 colorrest(cs, 1183.43/297.30 cs, 1183.43/297.30 Cons(CN(ncs, node), colorednodes), 1183.43/297.30 xs)) 1183.43/297.30 , colorednoderest[Ite][True][Ite](False(), 1183.43/297.30 cs, 1183.43/297.30 Cons(x, xs), 1183.43/297.30 node, 1183.43/297.30 colorednodes, 1183.43/297.30 rest) 1183.43/297.30 -> colorednoderest(cs, xs, node, colorednodes, rest) } 1183.43/297.30 Obligation: 1183.43/297.30 innermost runtime complexity 1183.43/297.30 Answer: 1183.43/297.30 MAYBE 1183.43/297.30 1183.43/297.30 None of the processors succeeded. 1183.43/297.30 1183.43/297.30 Details of failed attempt(s): 1183.43/297.30 ----------------------------- 1183.43/297.30 1) 'empty' failed due to the following reason: 1183.43/297.30 1183.43/297.30 Empty strict component of the problem is NOT empty. 1183.43/297.30 1183.43/297.30 2) 'Best' failed due to the following reason: 1183.43/297.30 1183.43/297.30 None of the processors succeeded. 1183.43/297.30 1183.43/297.30 Details of failed attempt(s): 1183.43/297.30 ----------------------------- 1183.43/297.30 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1183.43/297.30 following reason: 1183.43/297.30 1183.43/297.30 Computation stopped due to timeout after 297.0 seconds. 1183.43/297.30 1183.43/297.30 2) 'Best' failed due to the following reason: 1183.43/297.30 1183.43/297.30 None of the processors succeeded. 1183.43/297.30 1183.43/297.30 Details of failed attempt(s): 1183.43/297.30 ----------------------------- 1183.43/297.30 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1183.43/297.30 seconds)' failed due to the following reason: 1183.43/297.30 1183.43/297.30 Computation stopped due to timeout after 148.0 seconds. 1183.43/297.30 1183.43/297.30 2) 'Best' failed due to the following reason: 1183.43/297.30 1183.43/297.30 None of the processors succeeded. 1183.43/297.30 1183.43/297.30 Details of failed attempt(s): 1183.43/297.30 ----------------------------- 1183.43/297.30 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1183.43/297.30 following reason: 1183.43/297.30 1183.43/297.30 The input cannot be shown compatible 1183.43/297.30 1183.43/297.30 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1183.43/297.30 to the following reason: 1183.43/297.30 1183.43/297.30 The input cannot be shown compatible 1183.43/297.30 1183.43/297.30 1183.43/297.30 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1183.43/297.30 failed due to the following reason: 1183.43/297.30 1183.43/297.30 None of the processors succeeded. 1183.43/297.30 1183.43/297.30 Details of failed attempt(s): 1183.43/297.30 ----------------------------- 1183.43/297.30 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1183.43/297.30 failed due to the following reason: 1183.43/297.30 1183.43/297.30 match-boundness of the problem could not be verified. 1183.43/297.30 1183.43/297.30 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1183.43/297.30 failed due to the following reason: 1183.43/297.30 1183.43/297.30 match-boundness of the problem could not be verified. 1183.43/297.30 1183.43/297.30 1183.43/297.30 1183.43/297.30 1183.43/297.30 1183.43/297.30 Arrrr.. 1184.24/297.75 EOF