MAYBE 1169.01/297.05 MAYBE 1169.01/297.05 1169.01/297.05 We are left with following problem, upon which TcT provides the 1169.01/297.05 certificate MAYBE. 1169.01/297.05 1169.01/297.05 Strict Trs: 1169.01/297.05 { 0(#()) -> #() 1169.01/297.05 , +(x, #()) -> x 1169.01/297.05 , +(0(x), 0(y)) -> 0(+(x, y)) 1169.01/297.05 , +(0(x), 1(y)) -> 1(+(x, y)) 1169.01/297.05 , +(#(), x) -> x 1169.01/297.05 , +(+(x, y), z) -> +(x, +(y, z)) 1169.01/297.05 , +(1(x), 0(y)) -> 1(+(x, y)) 1169.01/297.05 , +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))) 1169.01/297.05 , -(x, #()) -> x 1169.01/297.05 , -(0(x), 0(y)) -> 0(-(x, y)) 1169.01/297.05 , -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))) 1169.01/297.05 , -(#(), x) -> #() 1169.01/297.05 , -(1(x), 0(y)) -> 1(-(x, y)) 1169.01/297.05 , -(1(x), 1(y)) -> 0(-(x, y)) 1169.01/297.05 , not(true()) -> false() 1169.01/297.05 , not(false()) -> true() 1169.01/297.05 , if(true(), x, y) -> x 1169.01/297.05 , if(false(), x, y) -> y 1169.01/297.05 , eq(0(x), 0(y)) -> eq(x, y) 1169.01/297.05 , eq(0(x), #()) -> eq(x, #()) 1169.01/297.05 , eq(0(x), 1(y)) -> false() 1169.01/297.05 , eq(#(), 0(y)) -> eq(#(), y) 1169.01/297.05 , eq(#(), #()) -> true() 1169.01/297.05 , eq(#(), 1(y)) -> false() 1169.01/297.05 , eq(1(x), 0(y)) -> false() 1169.01/297.05 , eq(1(x), #()) -> false() 1169.01/297.05 , eq(1(x), 1(y)) -> eq(x, y) 1169.01/297.05 , ge(x, #()) -> true() 1169.01/297.05 , ge(0(x), 0(y)) -> ge(x, y) 1169.01/297.05 , ge(0(x), 1(y)) -> not(ge(y, x)) 1169.01/297.05 , ge(#(), 0(x)) -> ge(#(), x) 1169.01/297.05 , ge(#(), 1(x)) -> false() 1169.01/297.05 , ge(1(x), 0(y)) -> ge(x, y) 1169.01/297.05 , ge(1(x), 1(y)) -> ge(x, y) 1169.01/297.05 , log(x) -> -(log'(x), 1(#())) 1169.01/297.05 , log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()) 1169.01/297.05 , log'(#()) -> #() 1169.01/297.05 , log'(1(x)) -> +(log'(x), 1(#())) 1169.01/297.05 , *(x, +(y, z)) -> +(*(x, y), *(x, z)) 1169.01/297.05 , *(0(x), y) -> 0(*(x, y)) 1169.01/297.05 , *(#(), x) -> #() 1169.01/297.05 , *(1(x), y) -> +(0(*(x, y)), y) 1169.01/297.05 , *(*(x, y), z) -> *(x, *(y, z)) 1169.01/297.05 , app(nil(), l) -> l 1169.01/297.05 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 1169.01/297.05 , sum(app(l1, l2)) -> +(sum(l1), sum(l2)) 1169.01/297.05 , sum(nil()) -> 0(#()) 1169.01/297.05 , sum(cons(x, l)) -> +(x, sum(l)) 1169.01/297.05 , prod(app(l1, l2)) -> *(prod(l1), prod(l2)) 1169.01/297.05 , prod(nil()) -> 1(#()) 1169.01/297.05 , prod(cons(x, l)) -> *(x, prod(l)) 1169.01/297.05 , mem(x, nil()) -> false() 1169.01/297.05 , mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)) 1169.01/297.05 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 1169.01/297.05 , inter(x, nil()) -> nil() 1169.01/297.05 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 1169.01/297.05 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 1169.01/297.05 , inter(nil(), x) -> nil() 1169.01/297.05 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) 1169.01/297.05 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 1169.01/297.05 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 1169.01/297.05 Obligation: 1169.01/297.05 innermost runtime complexity 1169.01/297.05 Answer: 1169.01/297.05 MAYBE 1169.01/297.05 1169.01/297.05 None of the processors succeeded. 1169.01/297.05 1169.01/297.05 Details of failed attempt(s): 1169.01/297.05 ----------------------------- 1169.01/297.05 1) 'empty' failed due to the following reason: 1169.01/297.05 1169.01/297.05 Empty strict component of the problem is NOT empty. 1169.01/297.05 1169.01/297.05 2) 'Best' failed due to the following reason: 1169.01/297.05 1169.01/297.05 None of the processors succeeded. 1169.01/297.05 1169.01/297.05 Details of failed attempt(s): 1169.01/297.05 ----------------------------- 1169.01/297.05 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1169.01/297.05 following reason: 1169.01/297.05 1169.01/297.05 Computation stopped due to timeout after 297.0 seconds. 1169.01/297.05 1169.01/297.05 2) 'Best' failed due to the following reason: 1169.01/297.05 1169.01/297.05 None of the processors succeeded. 1169.01/297.05 1169.01/297.05 Details of failed attempt(s): 1169.01/297.05 ----------------------------- 1169.01/297.05 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1169.01/297.05 seconds)' failed due to the following reason: 1169.01/297.05 1169.01/297.05 Computation stopped due to timeout after 148.0 seconds. 1169.01/297.05 1169.01/297.05 2) 'Best' failed due to the following reason: 1169.01/297.05 1169.01/297.05 None of the processors succeeded. 1169.01/297.05 1169.01/297.05 Details of failed attempt(s): 1169.01/297.05 ----------------------------- 1169.01/297.05 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1169.01/297.05 to the following reason: 1169.01/297.05 1169.01/297.05 The input cannot be shown compatible 1169.01/297.05 1169.01/297.05 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1169.01/297.05 following reason: 1169.01/297.05 1169.01/297.05 The input cannot be shown compatible 1169.01/297.05 1169.01/297.05 1169.01/297.05 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1169.01/297.05 failed due to the following reason: 1169.01/297.05 1169.01/297.05 None of the processors succeeded. 1169.01/297.05 1169.01/297.05 Details of failed attempt(s): 1169.01/297.05 ----------------------------- 1169.01/297.05 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1169.01/297.05 failed due to the following reason: 1169.01/297.05 1169.01/297.05 match-boundness of the problem could not be verified. 1169.01/297.05 1169.01/297.05 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1169.01/297.05 failed due to the following reason: 1169.01/297.05 1169.01/297.05 match-boundness of the problem could not be verified. 1169.01/297.05 1169.01/297.05 1169.01/297.05 1169.01/297.05 1169.01/297.05 1169.01/297.05 Arrrr.. 1169.65/297.50 EOF