MAYBE 370.82/297.13 MAYBE 370.82/297.13 370.82/297.13 We are left with following problem, upon which TcT provides the 370.82/297.13 certificate MAYBE. 370.82/297.13 370.82/297.13 Strict Trs: 370.82/297.13 { empty(nil()) -> true() 370.82/297.13 , empty(cons(x, l)) -> false() 370.82/297.13 , head(cons(x, l)) -> x 370.82/297.13 , tail(nil()) -> nil() 370.82/297.13 , tail(cons(x, l)) -> l 370.82/297.13 , rev(nil()) -> nil() 370.82/297.13 , rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) 370.82/297.13 , rev2(x, nil()) -> nil() 370.82/297.13 , rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) 370.82/297.13 , last(x, l) -> if(empty(l), x, l) 370.82/297.13 , if(true(), x, l) -> x 370.82/297.13 , if(false(), x, l) -> last(head(l), tail(l)) } 370.82/297.13 Obligation: 370.82/297.13 innermost runtime complexity 370.82/297.13 Answer: 370.82/297.13 MAYBE 370.82/297.13 370.82/297.13 None of the processors succeeded. 370.82/297.13 370.82/297.13 Details of failed attempt(s): 370.82/297.13 ----------------------------- 370.82/297.13 1) 'empty' failed due to the following reason: 370.82/297.13 370.82/297.13 Empty strict component of the problem is NOT empty. 370.82/297.13 370.82/297.13 2) 'Best' failed due to the following reason: 370.82/297.13 370.82/297.13 None of the processors succeeded. 370.82/297.13 370.82/297.13 Details of failed attempt(s): 370.82/297.13 ----------------------------- 370.82/297.13 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 370.82/297.13 following reason: 370.82/297.13 370.82/297.13 Computation stopped due to timeout after 297.0 seconds. 370.82/297.13 370.82/297.13 2) 'Best' failed due to the following reason: 370.82/297.13 370.82/297.13 None of the processors succeeded. 370.82/297.13 370.82/297.13 Details of failed attempt(s): 370.82/297.13 ----------------------------- 370.82/297.13 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 370.82/297.13 seconds)' failed due to the following reason: 370.82/297.13 370.82/297.13 None of the processors succeeded. 370.82/297.13 370.82/297.13 Details of failed attempt(s): 370.82/297.13 ----------------------------- 370.82/297.13 1) 'empty' failed due to the following reason: 370.82/297.13 370.82/297.13 Empty strict component of the problem is NOT empty. 370.82/297.13 370.82/297.13 2) 'With Problem ...' failed due to the following reason: 370.82/297.13 370.82/297.13 None of the processors succeeded. 370.82/297.13 370.82/297.13 Details of failed attempt(s): 370.82/297.13 ----------------------------- 370.82/297.13 1) 'empty' failed due to the following reason: 370.82/297.13 370.82/297.13 Empty strict component of the problem is NOT empty. 370.82/297.13 370.82/297.13 2) 'Fastest' failed due to the following reason: 370.82/297.13 370.82/297.13 None of the processors succeeded. 370.82/297.13 370.82/297.13 Details of failed attempt(s): 370.82/297.13 ----------------------------- 370.82/297.13 1) 'With Problem ...' failed due to the following reason: 370.82/297.13 370.82/297.13 None of the processors succeeded. 370.82/297.13 370.82/297.13 Details of failed attempt(s): 370.82/297.13 ----------------------------- 370.82/297.13 1) 'empty' failed due to the following reason: 370.82/297.13 370.82/297.13 Empty strict component of the problem is NOT empty. 370.82/297.13 370.82/297.13 2) 'With Problem ...' failed due to the following reason: 370.82/297.13 370.82/297.13 The weightgap principle applies (using the following nonconstant 370.82/297.13 growth matrix-interpretation) 370.82/297.13 370.82/297.13 The following argument positions are usable: 370.82/297.13 Uargs(cons) = {2}, Uargs(rev) = {1}, Uargs(last) = {1, 2}, 370.82/297.13 Uargs(if) = {1} 370.82/297.13 370.82/297.13 TcT has computed the following matrix interpretation satisfying 370.82/297.13 not(EDA) and not(IDA(1)). 370.82/297.13 370.82/297.13 [empty](x1) = [0] 370.82/297.13 [0] 370.82/297.13 370.82/297.13 [nil] = [0] 370.82/297.13 [0] 370.82/297.13 370.82/297.13 [true] = [0] 370.82/297.13 [0] 370.82/297.13 370.82/297.13 [cons](x1, x2) = [0 0] x1 + [1 0] x2 + [0] 370.82/297.13 [1 0] [0 0] [0] 370.82/297.13 370.82/297.13 [false] = [0] 370.82/297.13 [0] 370.82/297.13 370.82/297.13 [head](x1) = [0 1] x1 + [0] 370.82/297.13 [0 0] [0] 370.82/297.13 370.82/297.13 [tail](x1) = [1 0] x1 + [0] 370.82/297.13 [0 0] [0] 370.82/297.13 370.82/297.13 [rev](x1) = [1 0] x1 + [0] 370.82/297.13 [0 0] [0] 370.82/297.13 370.82/297.13 [rev1](x1, x2) = [0] 370.82/297.13 [0] 370.82/297.13 370.82/297.13 [rev2](x1, x2) = [0 0] x2 + [0] 370.82/297.13 [1 0] [0] 370.82/297.13 370.82/297.13 [last](x1, x2) = [1 0] x1 + [1 1] x2 + [4] 370.82/297.13 [0 0] [0 0] [4] 370.82/297.13 370.82/297.13 [if](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 1] x3 + [0] 370.82/297.13 [0 0] [0 0] [0 0] [0] 370.82/297.13 370.82/297.13 The order satisfies the following ordering constraints: 370.82/297.13 370.82/297.13 [empty(nil())] = [0] 370.82/297.13 [0] 370.82/297.13 >= [0] 370.82/297.13 [0] 370.82/297.13 = [true()] 370.82/297.13 370.82/297.13 [empty(cons(x, l))] = [0] 370.82/297.13 [0] 370.82/297.13 >= [0] 370.82/297.13 [0] 370.82/297.13 = [false()] 370.82/297.13 370.82/297.13 [head(cons(x, l))] = [1 0] x + [0] 370.82/297.13 [0 0] [0] 370.82/297.13 ? [1 0] x + [0] 370.82/297.13 [0 1] [0] 370.82/297.13 = [x] 370.82/297.13 370.82/297.13 [tail(nil())] = [0] 370.82/297.13 [0] 370.82/297.13 >= [0] 370.82/297.13 [0] 370.82/297.13 = [nil()] 370.82/297.13 370.82/297.13 [tail(cons(x, l))] = [1 0] l + [0] 370.82/297.13 [0 0] [0] 370.82/297.13 ? [1 0] l + [0] 370.82/297.13 [0 1] [0] 370.82/297.13 = [l] 370.82/297.13 370.82/297.13 [rev(nil())] = [0] 370.82/297.13 [0] 370.82/297.13 >= [0] 370.82/297.13 [0] 370.82/297.13 = [nil()] 370.82/297.13 370.82/297.13 [rev(cons(x, l))] = [1 0] l + [0] 370.82/297.13 [0 0] [0] 370.82/297.13 >= [0] 370.82/297.13 [0] 370.82/297.13 = [cons(rev1(x, l), rev2(x, l))] 370.82/297.13 370.82/297.13 [rev2(x, nil())] = [0] 370.82/297.13 [0] 370.82/297.13 >= [0] 370.82/297.13 [0] 370.82/297.13 = [nil()] 370.82/297.13 370.82/297.13 [rev2(x, cons(y, l))] = [0 0] l + [0] 370.82/297.13 [1 0] [0] 370.82/297.13 >= [0] 370.82/297.13 [0] 370.82/297.13 = [rev(cons(x, rev2(y, l)))] 370.82/297.13 370.82/297.13 [last(x, l)] = [1 0] x + [1 1] l + [4] 370.82/297.13 [0 0] [0 0] [4] 370.82/297.13 > [1 0] x + [1 1] l + [0] 370.82/297.13 [0 0] [0 0] [0] 370.82/297.13 = [if(empty(l), x, l)] 370.82/297.13 370.82/297.13 [if(true(), x, l)] = [1 0] x + [1 1] l + [0] 370.82/297.13 [0 0] [0 0] [0] 370.82/297.13 ? [1 0] x + [0] 370.82/297.13 [0 1] [0] 370.82/297.13 = [x] 370.82/297.13 370.82/297.13 [if(false(), x, l)] = [1 0] x + [1 1] l + [0] 370.82/297.13 [0 0] [0 0] [0] 370.82/297.13 ? [1 1] l + [4] 370.82/297.13 [0 0] [4] 370.82/297.13 = [last(head(l), tail(l))] 370.82/297.13 370.82/297.13 370.82/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 370.82/297.13 370.82/297.13 We are left with following problem, upon which TcT provides the 370.82/297.13 certificate MAYBE. 370.82/297.13 370.82/297.13 Strict Trs: 370.82/297.13 { empty(nil()) -> true() 370.82/297.13 , empty(cons(x, l)) -> false() 370.82/297.13 , head(cons(x, l)) -> x 370.82/297.13 , tail(nil()) -> nil() 370.82/297.13 , tail(cons(x, l)) -> l 370.82/297.13 , rev(nil()) -> nil() 370.82/297.13 , rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) 370.82/297.13 , rev2(x, nil()) -> nil() 370.82/297.13 , rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) 370.82/297.13 , if(true(), x, l) -> x 370.82/297.13 , if(false(), x, l) -> last(head(l), tail(l)) } 370.82/297.13 Weak Trs: { last(x, l) -> if(empty(l), x, l) } 370.82/297.13 Obligation: 370.82/297.13 innermost runtime complexity 370.82/297.13 Answer: 370.82/297.13 MAYBE 370.82/297.13 370.82/297.13 The weightgap principle applies (using the following nonconstant 370.82/297.13 growth matrix-interpretation) 370.82/297.13 370.82/297.13 The following argument positions are usable: 370.82/297.13 Uargs(cons) = {2}, Uargs(rev) = {1}, Uargs(last) = {1, 2}, 370.82/297.13 Uargs(if) = {1} 370.82/297.13 370.82/297.13 TcT has computed the following matrix interpretation satisfying 370.82/297.13 not(EDA) and not(IDA(1)). 370.82/297.13 370.82/297.13 [empty](x1) = [0] 370.82/297.13 [0] 370.82/297.13 370.82/297.13 [nil] = [0] 370.82/297.13 [0] 370.82/297.13 370.82/297.13 [true] = [0] 370.82/297.13 [0] 370.82/297.13 370.82/297.13 [cons](x1, x2) = [0 0] x1 + [1 0] x2 + [0] 370.82/297.13 [1 0] [0 0] [0] 370.82/297.13 370.82/297.13 [false] = [1] 370.82/297.13 [0] 370.82/297.13 370.82/297.13 [head](x1) = [0 1] x1 + [0] 370.82/297.13 [0 0] [0] 370.82/297.13 370.82/297.13 [tail](x1) = [1 0] x1 + [0] 370.82/297.13 [0 0] [0] 370.82/297.13 370.82/297.13 [rev](x1) = [1 0] x1 + [0] 370.82/297.13 [0 0] [0] 370.82/297.13 370.82/297.13 [rev1](x1, x2) = [0] 370.82/297.13 [0] 370.82/297.13 370.82/297.13 [rev2](x1, x2) = [0 0] x2 + [0] 370.82/297.13 [0 1] [0] 370.82/297.13 370.82/297.13 [last](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 370.82/297.13 [0 0] [0 0] [0] 370.82/297.13 370.82/297.13 [if](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 1] x3 + [0] 370.82/297.13 [0 0] [0 0] [0 0] [0] 370.82/297.13 370.82/297.13 The order satisfies the following ordering constraints: 370.82/297.13 370.82/297.13 [empty(nil())] = [0] 370.82/297.13 [0] 370.82/297.13 >= [0] 370.82/297.13 [0] 370.82/297.13 = [true()] 370.82/297.13 370.82/297.13 [empty(cons(x, l))] = [0] 370.82/297.13 [0] 370.82/297.13 ? [1] 370.82/297.13 [0] 370.82/297.13 = [false()] 370.82/297.13 370.82/297.13 [head(cons(x, l))] = [1 0] x + [0] 370.82/297.13 [0 0] [0] 370.82/297.13 ? [1 0] x + [0] 370.82/297.13 [0 1] [0] 370.82/297.13 = [x] 370.82/297.13 370.82/297.13 [tail(nil())] = [0] 370.82/297.13 [0] 370.82/297.13 >= [0] 370.82/297.13 [0] 370.82/297.13 = [nil()] 370.82/297.13 370.82/297.13 [tail(cons(x, l))] = [1 0] l + [0] 370.82/297.13 [0 0] [0] 370.82/297.13 ? [1 0] l + [0] 370.82/297.13 [0 1] [0] 370.82/297.13 = [l] 370.82/297.13 370.82/297.13 [rev(nil())] = [0] 370.82/297.13 [0] 370.82/297.13 >= [0] 370.82/297.13 [0] 370.82/297.13 = [nil()] 370.82/297.13 370.82/297.13 [rev(cons(x, l))] = [1 0] l + [0] 370.82/297.13 [0 0] [0] 370.82/297.13 >= [0] 370.82/297.13 [0] 370.82/297.13 = [cons(rev1(x, l), rev2(x, l))] 370.82/297.13 370.82/297.13 [rev2(x, nil())] = [0] 370.82/297.13 [0] 370.82/297.13 >= [0] 370.82/297.13 [0] 370.82/297.13 = [nil()] 370.82/297.13 370.82/297.13 [rev2(x, cons(y, l))] = [0 0] y + [0] 370.82/297.13 [1 0] [0] 370.82/297.13 >= [0] 370.82/297.13 [0] 370.82/297.13 = [rev(cons(x, rev2(y, l)))] 370.82/297.13 370.82/297.13 [last(x, l)] = [1 0] x + [1 1] l + [0] 370.82/297.13 [0 0] [0 0] [0] 370.82/297.13 >= [1 0] x + [1 1] l + [0] 370.82/297.13 [0 0] [0 0] [0] 370.82/297.13 = [if(empty(l), x, l)] 370.82/297.13 370.82/297.13 [if(true(), x, l)] = [1 0] x + [1 1] l + [0] 370.82/297.14 [0 0] [0 0] [0] 370.82/297.14 ? [1 0] x + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [x] 370.82/297.14 370.82/297.14 [if(false(), x, l)] = [1 0] x + [1 1] l + [1] 370.82/297.14 [0 0] [0 0] [0] 370.82/297.14 > [1 1] l + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 = [last(head(l), tail(l))] 370.82/297.14 370.82/297.14 370.82/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 370.82/297.14 370.82/297.14 We are left with following problem, upon which TcT provides the 370.82/297.14 certificate MAYBE. 370.82/297.14 370.82/297.14 Strict Trs: 370.82/297.14 { empty(nil()) -> true() 370.82/297.14 , empty(cons(x, l)) -> false() 370.82/297.14 , head(cons(x, l)) -> x 370.82/297.14 , tail(nil()) -> nil() 370.82/297.14 , tail(cons(x, l)) -> l 370.82/297.14 , rev(nil()) -> nil() 370.82/297.14 , rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) 370.82/297.14 , rev2(x, nil()) -> nil() 370.82/297.14 , rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) 370.82/297.14 , if(true(), x, l) -> x } 370.82/297.14 Weak Trs: 370.82/297.14 { last(x, l) -> if(empty(l), x, l) 370.82/297.14 , if(false(), x, l) -> last(head(l), tail(l)) } 370.82/297.14 Obligation: 370.82/297.14 innermost runtime complexity 370.82/297.14 Answer: 370.82/297.14 MAYBE 370.82/297.14 370.82/297.14 The weightgap principle applies (using the following nonconstant 370.82/297.14 growth matrix-interpretation) 370.82/297.14 370.82/297.14 The following argument positions are usable: 370.82/297.14 Uargs(cons) = {2}, Uargs(rev) = {1}, Uargs(last) = {1, 2}, 370.82/297.14 Uargs(if) = {1} 370.82/297.14 370.82/297.14 TcT has computed the following matrix interpretation satisfying 370.82/297.14 not(EDA) and not(IDA(1)). 370.82/297.14 370.82/297.14 [empty](x1) = [2] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [nil] = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [true] = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [cons](x1, x2) = [0 0] x1 + [1 0] x2 + [0] 370.82/297.14 [1 0] [0 0] [0] 370.82/297.14 370.82/297.14 [false] = [4] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [head](x1) = [0 1] x1 + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [tail](x1) = [1 0] x1 + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [rev](x1) = [1 0] x1 + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [rev1](x1, x2) = [1 0] x2 + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [rev2](x1, x2) = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [last](x1, x2) = [1 0] x1 + [1 1] x2 + [6] 370.82/297.14 [0 0] [0 0] [0] 370.82/297.14 370.82/297.14 [if](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 1] x3 + [4] 370.82/297.14 [0 0] [0 0] [0 0] [0] 370.82/297.14 370.82/297.14 The order satisfies the following ordering constraints: 370.82/297.14 370.82/297.14 [empty(nil())] = [2] 370.82/297.14 [0] 370.82/297.14 > [0] 370.82/297.14 [0] 370.82/297.14 = [true()] 370.82/297.14 370.82/297.14 [empty(cons(x, l))] = [2] 370.82/297.14 [0] 370.82/297.14 ? [4] 370.82/297.14 [0] 370.82/297.14 = [false()] 370.82/297.14 370.82/297.14 [head(cons(x, l))] = [1 0] x + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 ? [1 0] x + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [x] 370.82/297.14 370.82/297.14 [tail(nil())] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [tail(cons(x, l))] = [1 0] l + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 ? [1 0] l + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [l] 370.82/297.14 370.82/297.14 [rev(nil())] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [rev(cons(x, l))] = [1 0] l + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 ? [0 0] l + [0] 370.82/297.14 [1 0] [0] 370.82/297.14 = [cons(rev1(x, l), rev2(x, l))] 370.82/297.14 370.82/297.14 [rev2(x, nil())] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [rev2(x, cons(y, l))] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [rev(cons(x, rev2(y, l)))] 370.82/297.14 370.82/297.14 [last(x, l)] = [1 0] x + [1 1] l + [6] 370.82/297.14 [0 0] [0 0] [0] 370.82/297.14 >= [1 0] x + [1 1] l + [6] 370.82/297.14 [0 0] [0 0] [0] 370.82/297.14 = [if(empty(l), x, l)] 370.82/297.14 370.82/297.14 [if(true(), x, l)] = [1 0] x + [1 1] l + [4] 370.82/297.14 [0 0] [0 0] [0] 370.82/297.14 ? [1 0] x + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [x] 370.82/297.14 370.82/297.14 [if(false(), x, l)] = [1 0] x + [1 1] l + [8] 370.82/297.14 [0 0] [0 0] [0] 370.82/297.14 > [1 1] l + [6] 370.82/297.14 [0 0] [0] 370.82/297.14 = [last(head(l), tail(l))] 370.82/297.14 370.82/297.14 370.82/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 370.82/297.14 370.82/297.14 We are left with following problem, upon which TcT provides the 370.82/297.14 certificate MAYBE. 370.82/297.14 370.82/297.14 Strict Trs: 370.82/297.14 { empty(cons(x, l)) -> false() 370.82/297.14 , head(cons(x, l)) -> x 370.82/297.14 , tail(nil()) -> nil() 370.82/297.14 , tail(cons(x, l)) -> l 370.82/297.14 , rev(nil()) -> nil() 370.82/297.14 , rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) 370.82/297.14 , rev2(x, nil()) -> nil() 370.82/297.14 , rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) 370.82/297.14 , if(true(), x, l) -> x } 370.82/297.14 Weak Trs: 370.82/297.14 { empty(nil()) -> true() 370.82/297.14 , last(x, l) -> if(empty(l), x, l) 370.82/297.14 , if(false(), x, l) -> last(head(l), tail(l)) } 370.82/297.14 Obligation: 370.82/297.14 innermost runtime complexity 370.82/297.14 Answer: 370.82/297.14 MAYBE 370.82/297.14 370.82/297.14 The weightgap principle applies (using the following nonconstant 370.82/297.14 growth matrix-interpretation) 370.82/297.14 370.82/297.14 The following argument positions are usable: 370.82/297.14 Uargs(cons) = {2}, Uargs(rev) = {1}, Uargs(last) = {1, 2}, 370.82/297.14 Uargs(if) = {1} 370.82/297.14 370.82/297.14 TcT has computed the following matrix interpretation satisfying 370.82/297.14 not(EDA) and not(IDA(1)). 370.82/297.14 370.82/297.14 [empty](x1) = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [nil] = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [true] = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [cons](x1, x2) = [0 0] x1 + [1 0] x2 + [0] 370.82/297.14 [1 0] [0 0] [0] 370.82/297.14 370.82/297.14 [false] = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [head](x1) = [0 1] x1 + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [tail](x1) = [1 0] x1 + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [rev](x1) = [1 0] x1 + [4] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [rev1](x1, x2) = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [rev2](x1, x2) = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [last](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 370.82/297.14 [0 0] [0 0] [0] 370.82/297.14 370.82/297.14 [if](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 1] x3 + [0] 370.82/297.14 [0 0] [0 0] [0 0] [0] 370.82/297.14 370.82/297.14 The order satisfies the following ordering constraints: 370.82/297.14 370.82/297.14 [empty(nil())] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [true()] 370.82/297.14 370.82/297.14 [empty(cons(x, l))] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [false()] 370.82/297.14 370.82/297.14 [head(cons(x, l))] = [1 0] x + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 ? [1 0] x + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [x] 370.82/297.14 370.82/297.14 [tail(nil())] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [tail(cons(x, l))] = [1 0] l + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 ? [1 0] l + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [l] 370.82/297.14 370.82/297.14 [rev(nil())] = [4] 370.82/297.14 [0] 370.82/297.14 > [0] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [rev(cons(x, l))] = [1 0] l + [4] 370.82/297.14 [0 0] [0] 370.82/297.14 > [0] 370.82/297.14 [0] 370.82/297.14 = [cons(rev1(x, l), rev2(x, l))] 370.82/297.14 370.82/297.14 [rev2(x, nil())] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [rev2(x, cons(y, l))] = [0] 370.82/297.14 [0] 370.82/297.14 ? [4] 370.82/297.14 [0] 370.82/297.14 = [rev(cons(x, rev2(y, l)))] 370.82/297.14 370.82/297.14 [last(x, l)] = [1 0] x + [1 1] l + [0] 370.82/297.14 [0 0] [0 0] [0] 370.82/297.14 >= [1 0] x + [1 1] l + [0] 370.82/297.14 [0 0] [0 0] [0] 370.82/297.14 = [if(empty(l), x, l)] 370.82/297.14 370.82/297.14 [if(true(), x, l)] = [1 0] x + [1 1] l + [0] 370.82/297.14 [0 0] [0 0] [0] 370.82/297.14 ? [1 0] x + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [x] 370.82/297.14 370.82/297.14 [if(false(), x, l)] = [1 0] x + [1 1] l + [0] 370.82/297.14 [0 0] [0 0] [0] 370.82/297.14 >= [1 1] l + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 = [last(head(l), tail(l))] 370.82/297.14 370.82/297.14 370.82/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 370.82/297.14 370.82/297.14 We are left with following problem, upon which TcT provides the 370.82/297.14 certificate MAYBE. 370.82/297.14 370.82/297.14 Strict Trs: 370.82/297.14 { empty(cons(x, l)) -> false() 370.82/297.14 , head(cons(x, l)) -> x 370.82/297.14 , tail(nil()) -> nil() 370.82/297.14 , tail(cons(x, l)) -> l 370.82/297.14 , rev2(x, nil()) -> nil() 370.82/297.14 , rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) 370.82/297.14 , if(true(), x, l) -> x } 370.82/297.14 Weak Trs: 370.82/297.14 { empty(nil()) -> true() 370.82/297.14 , rev(nil()) -> nil() 370.82/297.14 , rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) 370.82/297.14 , last(x, l) -> if(empty(l), x, l) 370.82/297.14 , if(false(), x, l) -> last(head(l), tail(l)) } 370.82/297.14 Obligation: 370.82/297.14 innermost runtime complexity 370.82/297.14 Answer: 370.82/297.14 MAYBE 370.82/297.14 370.82/297.14 The weightgap principle applies (using the following nonconstant 370.82/297.14 growth matrix-interpretation) 370.82/297.14 370.82/297.14 The following argument positions are usable: 370.82/297.14 Uargs(cons) = {2}, Uargs(rev) = {1}, Uargs(last) = {1, 2}, 370.82/297.14 Uargs(if) = {1} 370.82/297.14 370.82/297.14 TcT has computed the following matrix interpretation satisfying 370.82/297.14 not(EDA) and not(IDA(1)). 370.82/297.14 370.82/297.14 [empty](x1) = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [nil] = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [true] = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [cons](x1, x2) = [0 0] x1 + [1 0] x2 + [0] 370.82/297.14 [1 0] [0 0] [0] 370.82/297.14 370.82/297.14 [false] = [4] 370.82/297.14 [6] 370.82/297.14 370.82/297.14 [head](x1) = [0 1] x1 + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [tail](x1) = [1 0] x1 + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [rev](x1) = [1 0] x1 + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [rev1](x1, x2) = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [rev2](x1, x2) = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [last](x1, x2) = [1 0] x1 + [1 1] x2 + [4] 370.82/297.14 [0 1] [0 0] [2] 370.82/297.14 370.82/297.14 [if](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 1] x3 + [4] 370.82/297.14 [0 1] [0 1] [0 0] [2] 370.82/297.14 370.82/297.14 The order satisfies the following ordering constraints: 370.82/297.14 370.82/297.14 [empty(nil())] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [true()] 370.82/297.14 370.82/297.14 [empty(cons(x, l))] = [0] 370.82/297.14 [0] 370.82/297.14 ? [4] 370.82/297.14 [6] 370.82/297.14 = [false()] 370.82/297.14 370.82/297.14 [head(cons(x, l))] = [1 0] x + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 ? [1 0] x + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [x] 370.82/297.14 370.82/297.14 [tail(nil())] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [tail(cons(x, l))] = [1 0] l + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 ? [1 0] l + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [l] 370.82/297.14 370.82/297.14 [rev(nil())] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [rev(cons(x, l))] = [1 0] l + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [cons(rev1(x, l), rev2(x, l))] 370.82/297.14 370.82/297.14 [rev2(x, nil())] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [rev2(x, cons(y, l))] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [rev(cons(x, rev2(y, l)))] 370.82/297.14 370.82/297.14 [last(x, l)] = [1 0] x + [1 1] l + [4] 370.82/297.14 [0 1] [0 0] [2] 370.82/297.14 >= [1 0] x + [1 1] l + [4] 370.82/297.14 [0 1] [0 0] [2] 370.82/297.14 = [if(empty(l), x, l)] 370.82/297.14 370.82/297.14 [if(true(), x, l)] = [1 0] x + [1 1] l + [4] 370.82/297.14 [0 1] [0 0] [2] 370.82/297.14 > [1 0] x + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [x] 370.82/297.14 370.82/297.14 [if(false(), x, l)] = [1 0] x + [1 1] l + [8] 370.82/297.14 [0 1] [0 0] [8] 370.82/297.14 > [1 1] l + [4] 370.82/297.14 [0 0] [2] 370.82/297.14 = [last(head(l), tail(l))] 370.82/297.14 370.82/297.14 370.82/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 370.82/297.14 370.82/297.14 We are left with following problem, upon which TcT provides the 370.82/297.14 certificate MAYBE. 370.82/297.14 370.82/297.14 Strict Trs: 370.82/297.14 { empty(cons(x, l)) -> false() 370.82/297.14 , head(cons(x, l)) -> x 370.82/297.14 , tail(nil()) -> nil() 370.82/297.14 , tail(cons(x, l)) -> l 370.82/297.14 , rev2(x, nil()) -> nil() 370.82/297.14 , rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) } 370.82/297.14 Weak Trs: 370.82/297.14 { empty(nil()) -> true() 370.82/297.14 , rev(nil()) -> nil() 370.82/297.14 , rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) 370.82/297.14 , last(x, l) -> if(empty(l), x, l) 370.82/297.14 , if(true(), x, l) -> x 370.82/297.14 , if(false(), x, l) -> last(head(l), tail(l)) } 370.82/297.14 Obligation: 370.82/297.14 innermost runtime complexity 370.82/297.14 Answer: 370.82/297.14 MAYBE 370.82/297.14 370.82/297.14 The weightgap principle applies (using the following nonconstant 370.82/297.14 growth matrix-interpretation) 370.82/297.14 370.82/297.14 The following argument positions are usable: 370.82/297.14 Uargs(cons) = {2}, Uargs(rev) = {1}, Uargs(last) = {1, 2}, 370.82/297.14 Uargs(if) = {1} 370.82/297.14 370.82/297.14 TcT has computed the following matrix interpretation satisfying 370.82/297.14 not(EDA) and not(IDA(1)). 370.82/297.14 370.82/297.14 [empty](x1) = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [nil] = [2] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [true] = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [cons](x1, x2) = [0 0] x1 + [1 0] x2 + [0] 370.82/297.14 [1 0] [0 0] [0] 370.82/297.14 370.82/297.14 [false] = [4] 370.82/297.14 [6] 370.82/297.14 370.82/297.14 [head](x1) = [0 1] x1 + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [tail](x1) = [1 0] x1 + [2] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [rev](x1) = [1 0] x1 + [4] 370.82/297.14 [0 0] [4] 370.82/297.14 370.82/297.14 [rev1](x1, x2) = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [rev2](x1, x2) = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [last](x1, x2) = [1 0] x1 + [1 1] x2 + [4] 370.82/297.14 [0 1] [0 0] [2] 370.82/297.14 370.82/297.14 [if](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 1] x3 + [4] 370.82/297.14 [0 1] [0 1] [0 0] [2] 370.82/297.14 370.82/297.14 The order satisfies the following ordering constraints: 370.82/297.14 370.82/297.14 [empty(nil())] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [true()] 370.82/297.14 370.82/297.14 [empty(cons(x, l))] = [0] 370.82/297.14 [0] 370.82/297.14 ? [4] 370.82/297.14 [6] 370.82/297.14 = [false()] 370.82/297.14 370.82/297.14 [head(cons(x, l))] = [1 0] x + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 ? [1 0] x + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [x] 370.82/297.14 370.82/297.14 [tail(nil())] = [4] 370.82/297.14 [0] 370.82/297.14 > [2] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [tail(cons(x, l))] = [1 0] l + [2] 370.82/297.14 [0 0] [0] 370.82/297.14 ? [1 0] l + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [l] 370.82/297.14 370.82/297.14 [rev(nil())] = [6] 370.82/297.14 [4] 370.82/297.14 > [2] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [rev(cons(x, l))] = [1 0] l + [4] 370.82/297.14 [0 0] [4] 370.82/297.14 > [0] 370.82/297.14 [0] 370.82/297.14 = [cons(rev1(x, l), rev2(x, l))] 370.82/297.14 370.82/297.14 [rev2(x, nil())] = [0] 370.82/297.14 [0] 370.82/297.14 ? [2] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [rev2(x, cons(y, l))] = [0] 370.82/297.14 [0] 370.82/297.14 ? [4] 370.82/297.14 [4] 370.82/297.14 = [rev(cons(x, rev2(y, l)))] 370.82/297.14 370.82/297.14 [last(x, l)] = [1 0] x + [1 1] l + [4] 370.82/297.14 [0 1] [0 0] [2] 370.82/297.14 >= [1 0] x + [1 1] l + [4] 370.82/297.14 [0 1] [0 0] [2] 370.82/297.14 = [if(empty(l), x, l)] 370.82/297.14 370.82/297.14 [if(true(), x, l)] = [1 0] x + [1 1] l + [4] 370.82/297.14 [0 1] [0 0] [2] 370.82/297.14 > [1 0] x + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [x] 370.82/297.14 370.82/297.14 [if(false(), x, l)] = [1 0] x + [1 1] l + [8] 370.82/297.14 [0 1] [0 0] [8] 370.82/297.14 > [1 1] l + [6] 370.82/297.14 [0 0] [2] 370.82/297.14 = [last(head(l), tail(l))] 370.82/297.14 370.82/297.14 370.82/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 370.82/297.14 370.82/297.14 We are left with following problem, upon which TcT provides the 370.82/297.14 certificate MAYBE. 370.82/297.14 370.82/297.14 Strict Trs: 370.82/297.14 { empty(cons(x, l)) -> false() 370.82/297.14 , head(cons(x, l)) -> x 370.82/297.14 , tail(cons(x, l)) -> l 370.82/297.14 , rev2(x, nil()) -> nil() 370.82/297.14 , rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) } 370.82/297.14 Weak Trs: 370.82/297.14 { empty(nil()) -> true() 370.82/297.14 , tail(nil()) -> nil() 370.82/297.14 , rev(nil()) -> nil() 370.82/297.14 , rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) 370.82/297.14 , last(x, l) -> if(empty(l), x, l) 370.82/297.14 , if(true(), x, l) -> x 370.82/297.14 , if(false(), x, l) -> last(head(l), tail(l)) } 370.82/297.14 Obligation: 370.82/297.14 innermost runtime complexity 370.82/297.14 Answer: 370.82/297.14 MAYBE 370.82/297.14 370.82/297.14 The weightgap principle applies (using the following nonconstant 370.82/297.14 growth matrix-interpretation) 370.82/297.14 370.82/297.14 The following argument positions are usable: 370.82/297.14 Uargs(cons) = {2}, Uargs(rev) = {1}, Uargs(last) = {1, 2}, 370.82/297.14 Uargs(if) = {1} 370.82/297.14 370.82/297.14 TcT has computed the following matrix interpretation satisfying 370.82/297.14 not(EDA) and not(IDA(1)). 370.82/297.14 370.82/297.14 [empty](x1) = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [nil] = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [true] = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [cons](x1, x2) = [0 0] x1 + [1 0] x2 + [2] 370.82/297.14 [1 0] [0 1] [2] 370.82/297.14 370.82/297.14 [false] = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [head](x1) = [0 1] x1 + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [tail](x1) = [1 0] x1 + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 370.82/297.14 [rev](x1) = [1 0] x1 + [5] 370.82/297.14 [0 1] [5] 370.82/297.14 370.82/297.14 [rev1](x1, x2) = [0] 370.82/297.14 [0] 370.82/297.14 370.82/297.14 [rev2](x1, x2) = [1] 370.82/297.14 [1] 370.82/297.14 370.82/297.14 [last](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 370.82/297.14 [0 1] [0 0] [0] 370.82/297.14 370.82/297.14 [if](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 1] x3 + [0] 370.82/297.14 [0 0] [0 1] [0 0] [0] 370.82/297.14 370.82/297.14 The order satisfies the following ordering constraints: 370.82/297.14 370.82/297.14 [empty(nil())] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [true()] 370.82/297.14 370.82/297.14 [empty(cons(x, l))] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [false()] 370.82/297.14 370.82/297.14 [head(cons(x, l))] = [1 0] x + [0 1] l + [2] 370.82/297.14 [0 0] [0 0] [0] 370.82/297.14 ? [1 0] x + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [x] 370.82/297.14 370.82/297.14 [tail(nil())] = [0] 370.82/297.14 [0] 370.82/297.14 >= [0] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [tail(cons(x, l))] = [1 0] l + [2] 370.82/297.14 [0 0] [0] 370.82/297.14 ? [1 0] l + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [l] 370.82/297.14 370.82/297.14 [rev(nil())] = [5] 370.82/297.14 [5] 370.82/297.14 > [0] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [rev(cons(x, l))] = [0 0] x + [1 0] l + [7] 370.82/297.14 [1 0] [0 1] [7] 370.82/297.14 > [3] 370.82/297.14 [3] 370.82/297.14 = [cons(rev1(x, l), rev2(x, l))] 370.82/297.14 370.82/297.14 [rev2(x, nil())] = [1] 370.82/297.14 [1] 370.82/297.14 > [0] 370.82/297.14 [0] 370.82/297.14 = [nil()] 370.82/297.14 370.82/297.14 [rev2(x, cons(y, l))] = [1] 370.82/297.14 [1] 370.82/297.14 ? [0 0] x + [8] 370.82/297.14 [1 0] [8] 370.82/297.14 = [rev(cons(x, rev2(y, l)))] 370.82/297.14 370.82/297.14 [last(x, l)] = [1 0] x + [1 1] l + [0] 370.82/297.14 [0 1] [0 0] [0] 370.82/297.14 >= [1 0] x + [1 1] l + [0] 370.82/297.14 [0 1] [0 0] [0] 370.82/297.14 = [if(empty(l), x, l)] 370.82/297.14 370.82/297.14 [if(true(), x, l)] = [1 0] x + [1 1] l + [0] 370.82/297.14 [0 1] [0 0] [0] 370.82/297.14 >= [1 0] x + [0] 370.82/297.14 [0 1] [0] 370.82/297.14 = [x] 370.82/297.14 370.82/297.14 [if(false(), x, l)] = [1 0] x + [1 1] l + [0] 370.82/297.14 [0 1] [0 0] [0] 370.82/297.14 >= [1 1] l + [0] 370.82/297.14 [0 0] [0] 370.82/297.14 = [last(head(l), tail(l))] 370.82/297.14 370.82/297.14 370.82/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 370.82/297.14 370.82/297.14 We are left with following problem, upon which TcT provides the 370.82/297.14 certificate MAYBE. 370.82/297.14 370.82/297.14 Strict Trs: 370.82/297.14 { empty(cons(x, l)) -> false() 370.82/297.14 , head(cons(x, l)) -> x 370.82/297.14 , tail(cons(x, l)) -> l 370.82/297.14 , rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) } 370.82/297.14 Weak Trs: 370.82/297.14 { empty(nil()) -> true() 370.82/297.14 , tail(nil()) -> nil() 370.82/297.14 , rev(nil()) -> nil() 370.82/297.14 , rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) 370.82/297.14 , rev2(x, nil()) -> nil() 370.82/297.14 , last(x, l) -> if(empty(l), x, l) 370.82/297.14 , if(true(), x, l) -> x 370.82/297.14 , if(false(), x, l) -> last(head(l), tail(l)) } 370.82/297.14 Obligation: 370.82/297.14 innermost runtime complexity 370.82/297.14 Answer: 370.82/297.14 MAYBE 370.82/297.14 370.82/297.14 None of the processors succeeded. 370.82/297.14 370.82/297.14 Details of failed attempt(s): 370.82/297.14 ----------------------------- 370.82/297.14 1) 'empty' failed due to the following reason: 370.82/297.14 370.82/297.14 Empty strict component of the problem is NOT empty. 370.82/297.14 370.82/297.14 2) 'With Problem ...' failed due to the following reason: 370.82/297.14 370.82/297.14 None of the processors succeeded. 370.82/297.14 370.82/297.14 Details of failed attempt(s): 370.82/297.14 ----------------------------- 370.82/297.14 1) 'empty' failed due to the following reason: 370.82/297.14 370.82/297.14 Empty strict component of the problem is NOT empty. 370.82/297.14 370.82/297.14 2) 'With Problem ...' failed due to the following reason: 370.82/297.14 370.82/297.14 Empty strict component of the problem is NOT empty. 370.82/297.14 370.82/297.14 370.82/297.14 370.82/297.14 370.82/297.14 2) 'With Problem ...' failed due to the following reason: 370.82/297.14 370.82/297.14 None of the processors succeeded. 370.82/297.14 370.82/297.14 Details of failed attempt(s): 370.82/297.14 ----------------------------- 370.82/297.14 1) 'empty' failed due to the following reason: 370.82/297.14 370.82/297.14 Empty strict component of the problem is NOT empty. 370.82/297.14 370.82/297.14 2) 'With Problem ...' failed due to the following reason: 370.82/297.14 370.82/297.14 Empty strict component of the problem is NOT empty. 370.82/297.14 370.82/297.14 370.82/297.14 370.82/297.14 370.82/297.14 370.82/297.14 2) 'Best' failed due to the following reason: 370.82/297.14 370.82/297.14 None of the processors succeeded. 370.82/297.14 370.82/297.14 Details of failed attempt(s): 370.82/297.14 ----------------------------- 370.82/297.14 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 370.82/297.14 following reason: 370.82/297.14 370.82/297.15 The input cannot be shown compatible 370.82/297.15 370.82/297.15 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 370.82/297.15 to the following reason: 370.82/297.15 370.82/297.15 The input cannot be shown compatible 370.82/297.15 370.82/297.15 370.82/297.15 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 370.82/297.15 failed due to the following reason: 370.82/297.15 370.82/297.15 None of the processors succeeded. 370.82/297.15 370.82/297.15 Details of failed attempt(s): 370.82/297.15 ----------------------------- 370.82/297.15 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 370.82/297.15 failed due to the following reason: 370.82/297.15 370.82/297.15 match-boundness of the problem could not be verified. 370.82/297.15 370.82/297.15 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 370.82/297.15 failed due to the following reason: 370.82/297.15 370.82/297.15 match-boundness of the problem could not be verified. 370.82/297.15 370.82/297.15 370.82/297.15 370.82/297.15 370.82/297.15 370.82/297.15 Arrrr.. 370.82/297.19 EOF