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