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