MAYBE 1070.16/297.05 MAYBE 1070.16/297.05 1070.16/297.05 We are left with following problem, upon which TcT provides the 1070.16/297.05 certificate MAYBE. 1070.16/297.05 1070.16/297.05 Strict Trs: 1070.16/297.05 { head(Cons(x, xs)) -> x 1070.16/297.05 , factor(Cons(Plus(), xs)) -> xs 1070.16/297.05 , factor(Cons(LPar(), xs)) -> 1070.16/297.05 factor[Ite][True][Let](Cons(LPar(), xs), expr(Cons(LPar(), xs))) 1070.16/297.05 , factor(Cons(Minus(), xs)) -> xs 1070.16/297.05 , factor(Cons(Div(), xs)) -> xs 1070.16/297.05 , factor(Cons(Mul(), xs)) -> xs 1070.16/297.05 , factor(Cons(Val(int), xs)) -> xs 1070.16/297.05 , factor(Cons(RPar(), xs)) -> xs 1070.16/297.05 , atom(Cons(x, xs)) -> xs 1070.16/297.05 , atom(Nil()) -> Nil() 1070.16/297.05 , expr(xs) -> expr[Let](xs, term(xs)) 1070.16/297.05 , member(x', Cons(x, xs)) -> 1070.16/297.05 member[Ite][True][Ite](eqAlph(x, x'), x', Cons(x, xs)) 1070.16/297.05 , member(x, Nil()) -> False() 1070.16/297.05 , term(xs) -> term[Let](xs, factor(xs)) 1070.16/297.05 , eqAlph(Plus(), Plus()) -> True() 1070.16/297.05 , eqAlph(Plus(), LPar()) -> False() 1070.16/297.05 , eqAlph(Plus(), Minus()) -> False() 1070.16/297.05 , eqAlph(Plus(), Div()) -> False() 1070.16/297.05 , eqAlph(Plus(), Mul()) -> False() 1070.16/297.05 , eqAlph(Plus(), Val(int2)) -> False() 1070.16/297.05 , eqAlph(Plus(), RPar()) -> False() 1070.16/297.05 , eqAlph(LPar(), Plus()) -> False() 1070.16/297.05 , eqAlph(LPar(), LPar()) -> True() 1070.16/297.05 , eqAlph(LPar(), Minus()) -> False() 1070.16/297.05 , eqAlph(LPar(), Div()) -> False() 1070.16/297.05 , eqAlph(LPar(), Mul()) -> False() 1070.16/297.05 , eqAlph(LPar(), Val(int2)) -> False() 1070.16/297.05 , eqAlph(LPar(), RPar()) -> False() 1070.16/297.05 , eqAlph(Minus(), Plus()) -> False() 1070.16/297.05 , eqAlph(Minus(), LPar()) -> False() 1070.16/297.05 , eqAlph(Minus(), Minus()) -> True() 1070.16/297.05 , eqAlph(Minus(), Div()) -> False() 1070.16/297.05 , eqAlph(Minus(), Mul()) -> False() 1070.16/297.05 , eqAlph(Minus(), Val(int2)) -> False() 1070.16/297.05 , eqAlph(Minus(), RPar()) -> False() 1070.16/297.05 , eqAlph(Div(), Plus()) -> False() 1070.16/297.05 , eqAlph(Div(), LPar()) -> False() 1070.16/297.05 , eqAlph(Div(), Minus()) -> False() 1070.16/297.05 , eqAlph(Div(), Div()) -> True() 1070.16/297.05 , eqAlph(Div(), Mul()) -> False() 1070.16/297.05 , eqAlph(Div(), Val(int2)) -> False() 1070.16/297.05 , eqAlph(Div(), RPar()) -> False() 1070.16/297.05 , eqAlph(Mul(), Plus()) -> False() 1070.16/297.05 , eqAlph(Mul(), LPar()) -> False() 1070.16/297.05 , eqAlph(Mul(), Minus()) -> False() 1070.16/297.05 , eqAlph(Mul(), Div()) -> False() 1070.16/297.05 , eqAlph(Mul(), Mul()) -> True() 1070.16/297.05 , eqAlph(Mul(), Val(int2)) -> False() 1070.16/297.05 , eqAlph(Mul(), RPar()) -> False() 1070.16/297.05 , eqAlph(Val(int), Plus()) -> False() 1070.16/297.05 , eqAlph(Val(int), LPar()) -> False() 1070.16/297.05 , eqAlph(Val(int), Minus()) -> False() 1070.16/297.05 , eqAlph(Val(int), Div()) -> False() 1070.16/297.05 , eqAlph(Val(int), Mul()) -> False() 1070.16/297.05 , eqAlph(Val(int), Val(int2)) -> !EQ(int2, int) 1070.16/297.05 , eqAlph(Val(int), RPar()) -> False() 1070.16/297.05 , eqAlph(RPar(), Plus()) -> False() 1070.16/297.05 , eqAlph(RPar(), LPar()) -> False() 1070.16/297.05 , eqAlph(RPar(), Minus()) -> False() 1070.16/297.05 , eqAlph(RPar(), Div()) -> False() 1070.16/297.05 , eqAlph(RPar(), Mul()) -> False() 1070.16/297.05 , eqAlph(RPar(), Val(int2)) -> False() 1070.16/297.05 , eqAlph(RPar(), RPar()) -> True() 1070.16/297.05 , notEmpty(Cons(x, xs)) -> True() 1070.16/297.05 , notEmpty(Nil()) -> False() 1070.16/297.05 , parsexp(xs) -> expr(xs) } 1070.16/297.05 Weak Trs: 1070.16/297.05 { expr[Let](xs', Cons(x, xs)) -> 1070.16/297.05 expr[Let][Ite][False][Ite](member(x, 1070.16/297.05 Cons(Plus(), Cons(Minus(), Nil()))), 1070.16/297.05 xs', 1070.16/297.05 Cons(x, xs)) 1070.16/297.05 , expr[Let](xs, Nil()) -> Nil() 1070.16/297.05 , !EQ(S(x), S(y)) -> !EQ(x, y) 1070.16/297.05 , !EQ(S(x), 0()) -> False() 1070.16/297.05 , !EQ(0(), S(y)) -> False() 1070.16/297.05 , !EQ(0(), 0()) -> True() 1070.16/297.05 , factor[Ite][True][Let](xs', Cons(Plus(), xs)) -> 1070.16/297.05 factor[Ite][True][Let][Ite](False(), xs', Cons(Plus(), xs)) 1070.16/297.05 , factor[Ite][True][Let](xs', Cons(LPar(), xs)) -> 1070.16/297.05 factor[Ite][True][Let][Ite](False(), xs', Cons(LPar(), xs)) 1070.16/297.05 , factor[Ite][True][Let](xs', Cons(Minus(), xs)) -> 1070.16/297.05 factor[Ite][True][Let][Ite](False(), xs', Cons(Minus(), xs)) 1070.16/297.05 , factor[Ite][True][Let](xs', Cons(Div(), xs)) -> 1070.16/297.05 factor[Ite][True][Let][Ite](False(), xs', Cons(Div(), xs)) 1070.16/297.05 , factor[Ite][True][Let](xs', Cons(Mul(), xs)) -> 1070.16/297.05 factor[Ite][True][Let][Ite](False(), xs', Cons(Mul(), xs)) 1070.16/297.05 , factor[Ite][True][Let](xs', Cons(Val(int), xs)) -> 1070.16/297.05 factor[Ite][True][Let][Ite](False(), xs', Cons(Val(int), xs)) 1070.16/297.05 , factor[Ite][True][Let](xs', Cons(RPar(), xs)) -> 1070.16/297.05 factor[Ite][True][Let][Ite](True(), xs', Cons(RPar(), xs)) 1070.16/297.05 , factor[Ite][True][Let](xs, Nil()) -> 1070.16/297.05 factor[Ite][True][Let][Ite](and(False(), 1070.16/297.05 eqAlph(head(Nil()), RPar())), 1070.16/297.05 xs, 1070.16/297.05 Nil()) 1070.16/297.05 , member[Ite][True][Ite](True(), x, xs) -> True() 1070.16/297.05 , member[Ite][True][Ite](False(), x', Cons(x, xs)) -> 1070.16/297.05 member(x', xs) 1070.16/297.05 , and(True(), True()) -> True() 1070.16/297.05 , and(True(), False()) -> False() 1070.16/297.05 , and(False(), True()) -> False() 1070.16/297.05 , and(False(), False()) -> False() 1070.16/297.05 , term[Let](xs', Cons(x, xs)) -> 1070.16/297.05 term[Let][Ite][False][Ite](member(x, 1070.16/297.05 Cons(Mul(), Cons(Div(), Nil()))), 1070.16/297.05 xs', 1070.16/297.05 Cons(x, xs)) 1070.16/297.05 , term[Let](xs, Nil()) -> Nil() } 1070.16/297.05 Obligation: 1070.16/297.05 innermost runtime complexity 1070.16/297.05 Answer: 1070.16/297.05 MAYBE 1070.16/297.05 1070.16/297.05 None of the processors succeeded. 1070.16/297.05 1070.16/297.05 Details of failed attempt(s): 1070.16/297.05 ----------------------------- 1070.16/297.05 1) 'empty' failed due to the following reason: 1070.16/297.05 1070.16/297.05 Empty strict component of the problem is NOT empty. 1070.16/297.05 1070.16/297.05 2) 'Best' failed due to the following reason: 1070.16/297.05 1070.16/297.05 None of the processors succeeded. 1070.16/297.05 1070.16/297.05 Details of failed attempt(s): 1070.16/297.05 ----------------------------- 1070.16/297.05 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1070.16/297.05 following reason: 1070.16/297.05 1070.16/297.05 Computation stopped due to timeout after 297.0 seconds. 1070.16/297.05 1070.16/297.05 2) 'Best' failed due to the following reason: 1070.16/297.05 1070.16/297.05 None of the processors succeeded. 1070.16/297.05 1070.16/297.05 Details of failed attempt(s): 1070.16/297.05 ----------------------------- 1070.16/297.05 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1070.16/297.05 seconds)' failed due to the following reason: 1070.16/297.05 1070.16/297.05 Computation stopped due to timeout after 148.0 seconds. 1070.16/297.05 1070.16/297.05 2) 'Best' failed due to the following reason: 1070.16/297.05 1070.16/297.05 None of the processors succeeded. 1070.16/297.05 1070.16/297.05 Details of failed attempt(s): 1070.16/297.05 ----------------------------- 1070.16/297.05 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1070.16/297.05 following reason: 1070.16/297.05 1070.16/297.05 The input cannot be shown compatible 1070.16/297.05 1070.16/297.05 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1070.16/297.05 to the following reason: 1070.16/297.05 1070.16/297.05 The input cannot be shown compatible 1070.16/297.05 1070.16/297.05 1070.16/297.05 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1070.16/297.05 failed due to the following reason: 1070.16/297.05 1070.16/297.05 None of the processors succeeded. 1070.16/297.05 1070.16/297.05 Details of failed attempt(s): 1070.16/297.05 ----------------------------- 1070.16/297.05 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1070.16/297.05 failed due to the following reason: 1070.16/297.05 1070.16/297.05 match-boundness of the problem could not be verified. 1070.16/297.05 1070.16/297.05 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1070.16/297.05 failed due to the following reason: 1070.16/297.05 1070.16/297.05 match-boundness of the problem could not be verified. 1070.16/297.05 1070.16/297.05 1070.16/297.05 1070.16/297.05 1070.16/297.05 1070.16/297.05 Arrrr.. 1070.65/297.42 EOF