MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { head(Cons(x, xs)) -> x , factor(Cons(Plus(), xs)) -> xs , factor(Cons(LPar(), xs)) -> factor[Ite][True][Let](Cons(LPar(), xs), expr(Cons(LPar(), xs))) , factor(Cons(Minus(), xs)) -> xs , factor(Cons(Div(), xs)) -> xs , factor(Cons(Mul(), xs)) -> xs , factor(Cons(Val(int), xs)) -> xs , factor(Cons(RPar(), xs)) -> xs , atom(Cons(x, xs)) -> xs , atom(Nil()) -> Nil() , expr(xs) -> expr[Let](xs, term(xs)) , member(x', Cons(x, xs)) -> member[Ite][True][Ite](eqAlph(x, x'), x', Cons(x, xs)) , member(x, Nil()) -> False() , term(xs) -> term[Let](xs, factor(xs)) , eqAlph(Plus(), Plus()) -> True() , eqAlph(Plus(), LPar()) -> False() , eqAlph(Plus(), Minus()) -> False() , eqAlph(Plus(), Div()) -> False() , eqAlph(Plus(), Mul()) -> False() , eqAlph(Plus(), Val(int2)) -> False() , eqAlph(Plus(), RPar()) -> False() , eqAlph(LPar(), Plus()) -> False() , eqAlph(LPar(), LPar()) -> True() , eqAlph(LPar(), Minus()) -> False() , eqAlph(LPar(), Div()) -> False() , eqAlph(LPar(), Mul()) -> False() , eqAlph(LPar(), Val(int2)) -> False() , eqAlph(LPar(), RPar()) -> False() , eqAlph(Minus(), Plus()) -> False() , eqAlph(Minus(), LPar()) -> False() , eqAlph(Minus(), Minus()) -> True() , eqAlph(Minus(), Div()) -> False() , eqAlph(Minus(), Mul()) -> False() , eqAlph(Minus(), Val(int2)) -> False() , eqAlph(Minus(), RPar()) -> False() , eqAlph(Div(), Plus()) -> False() , eqAlph(Div(), LPar()) -> False() , eqAlph(Div(), Minus()) -> False() , eqAlph(Div(), Div()) -> True() , eqAlph(Div(), Mul()) -> False() , eqAlph(Div(), Val(int2)) -> False() , eqAlph(Div(), RPar()) -> False() , eqAlph(Mul(), Plus()) -> False() , eqAlph(Mul(), LPar()) -> False() , eqAlph(Mul(), Minus()) -> False() , eqAlph(Mul(), Div()) -> False() , eqAlph(Mul(), Mul()) -> True() , eqAlph(Mul(), Val(int2)) -> False() , eqAlph(Mul(), RPar()) -> False() , eqAlph(Val(int), Plus()) -> False() , eqAlph(Val(int), LPar()) -> False() , eqAlph(Val(int), Minus()) -> False() , eqAlph(Val(int), Div()) -> False() , eqAlph(Val(int), Mul()) -> False() , eqAlph(Val(int), Val(int2)) -> !EQ(int2, int) , eqAlph(Val(int), RPar()) -> False() , eqAlph(RPar(), Plus()) -> False() , eqAlph(RPar(), LPar()) -> False() , eqAlph(RPar(), Minus()) -> False() , eqAlph(RPar(), Div()) -> False() , eqAlph(RPar(), Mul()) -> False() , eqAlph(RPar(), Val(int2)) -> False() , eqAlph(RPar(), RPar()) -> True() , notEmpty(Cons(x, xs)) -> True() , notEmpty(Nil()) -> False() , parsexp(xs) -> expr(xs) } Weak Trs: { expr[Let](xs', Cons(x, xs)) -> expr[Let][Ite][False][Ite](member(x, Cons(Plus(), Cons(Minus(), Nil()))), xs', Cons(x, xs)) , expr[Let](xs, Nil()) -> Nil() , !EQ(S(x), S(y)) -> !EQ(x, y) , !EQ(S(x), 0()) -> False() , !EQ(0(), S(y)) -> False() , !EQ(0(), 0()) -> True() , factor[Ite][True][Let](xs', Cons(Plus(), xs)) -> factor[Ite][True][Let][Ite](False(), xs', Cons(Plus(), xs)) , factor[Ite][True][Let](xs', Cons(LPar(), xs)) -> factor[Ite][True][Let][Ite](False(), xs', Cons(LPar(), xs)) , factor[Ite][True][Let](xs', Cons(Minus(), xs)) -> factor[Ite][True][Let][Ite](False(), xs', Cons(Minus(), xs)) , factor[Ite][True][Let](xs', Cons(Div(), xs)) -> factor[Ite][True][Let][Ite](False(), xs', Cons(Div(), xs)) , factor[Ite][True][Let](xs', Cons(Mul(), xs)) -> factor[Ite][True][Let][Ite](False(), xs', Cons(Mul(), xs)) , factor[Ite][True][Let](xs', Cons(Val(int), xs)) -> factor[Ite][True][Let][Ite](False(), xs', Cons(Val(int), xs)) , factor[Ite][True][Let](xs', Cons(RPar(), xs)) -> factor[Ite][True][Let][Ite](True(), xs', Cons(RPar(), xs)) , factor[Ite][True][Let](xs, Nil()) -> factor[Ite][True][Let][Ite](and(False(), eqAlph(head(Nil()), RPar())), xs, Nil()) , member[Ite][True][Ite](True(), x, xs) -> True() , member[Ite][True][Ite](False(), x', Cons(x, xs)) -> member(x', xs) , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() , term[Let](xs', Cons(x, xs)) -> term[Let][Ite][False][Ite](member(x, Cons(Mul(), Cons(Div(), Nil()))), xs', Cons(x, xs)) , term[Let](xs, Nil()) -> Nil() } 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 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..