MAYBE 592.23/297.05 MAYBE 592.23/297.05 592.23/297.05 We are left with following problem, upon which TcT provides the 592.23/297.05 certificate MAYBE. 592.23/297.05 592.23/297.05 Strict Trs: 592.23/297.05 { a__h(X) -> a__g(mark(X), X) 592.23/297.05 , a__h(X) -> h(X) 592.23/297.05 , a__g(X1, X2) -> g(X1, X2) 592.23/297.05 , a__g(a(), X) -> a__f(b(), X) 592.23/297.05 , mark(a()) -> a__a() 592.23/297.05 , mark(b()) -> b() 592.23/297.05 , mark(h(X)) -> a__h(mark(X)) 592.23/297.05 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 592.23/297.05 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 592.23/297.05 , a__f(X, X) -> a__h(a__a()) 592.23/297.05 , a__f(X1, X2) -> f(X1, X2) 592.23/297.05 , a__a() -> a() 592.23/297.05 , a__a() -> b() } 592.23/297.05 Obligation: 592.23/297.05 runtime complexity 592.23/297.05 Answer: 592.23/297.05 MAYBE 592.23/297.05 592.23/297.05 None of the processors succeeded. 592.23/297.05 592.23/297.05 Details of failed attempt(s): 592.23/297.05 ----------------------------- 592.23/297.05 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 592.23/297.05 following reason: 592.23/297.05 592.23/297.05 Computation stopped due to timeout after 297.0 seconds. 592.23/297.05 592.23/297.05 2) 'Best' failed due to the following reason: 592.23/297.05 592.23/297.05 None of the processors succeeded. 592.23/297.05 592.23/297.05 Details of failed attempt(s): 592.23/297.05 ----------------------------- 592.23/297.05 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 592.23/297.05 seconds)' failed due to the following reason: 592.23/297.05 592.23/297.05 None of the processors succeeded. 592.23/297.05 592.23/297.05 Details of failed attempt(s): 592.23/297.05 ----------------------------- 592.23/297.05 1) 'empty' failed due to the following reason: 592.23/297.05 592.23/297.05 Empty strict component of the problem is NOT empty. 592.23/297.05 592.23/297.05 2) 'With Problem ...' failed due to the following reason: 592.23/297.05 592.23/297.05 None of the processors succeeded. 592.23/297.05 592.23/297.05 Details of failed attempt(s): 592.23/297.05 ----------------------------- 592.23/297.05 1) 'empty' failed due to the following reason: 592.23/297.05 592.23/297.05 Empty strict component of the problem is NOT empty. 592.23/297.05 592.23/297.05 2) 'Fastest' failed due to the following reason: 592.23/297.05 592.23/297.05 None of the processors succeeded. 592.23/297.05 592.23/297.05 Details of failed attempt(s): 592.23/297.05 ----------------------------- 592.23/297.05 1) 'With Problem ...' failed due to the following reason: 592.23/297.05 592.23/297.05 None of the processors succeeded. 592.23/297.05 592.23/297.05 Details of failed attempt(s): 592.23/297.05 ----------------------------- 592.23/297.05 1) 'empty' failed due to the following reason: 592.23/297.05 592.23/297.05 Empty strict component of the problem is NOT empty. 592.23/297.05 592.23/297.05 2) 'With Problem ...' failed due to the following reason: 592.23/297.05 592.23/297.05 None of the processors succeeded. 592.23/297.05 592.23/297.05 Details of failed attempt(s): 592.23/297.05 ----------------------------- 592.23/297.05 1) 'empty' failed due to the following reason: 592.23/297.05 592.23/297.05 Empty strict component of the problem is NOT empty. 592.23/297.05 592.23/297.05 2) 'With Problem ...' failed due to the following reason: 592.23/297.05 592.23/297.05 None of the processors succeeded. 592.23/297.05 592.23/297.05 Details of failed attempt(s): 592.23/297.05 ----------------------------- 592.23/297.05 1) 'empty' failed due to the following reason: 592.23/297.05 592.23/297.05 Empty strict component of the problem is NOT empty. 592.23/297.05 592.23/297.05 2) 'With Problem ...' failed due to the following reason: 592.23/297.05 592.23/297.05 Empty strict component of the problem is NOT empty. 592.23/297.05 592.23/297.05 592.23/297.05 592.23/297.05 592.23/297.05 2) 'With Problem ...' failed due to the following reason: 592.23/297.05 592.23/297.05 None of the processors succeeded. 592.23/297.05 592.23/297.05 Details of failed attempt(s): 592.23/297.05 ----------------------------- 592.23/297.05 1) 'empty' failed due to the following reason: 592.23/297.05 592.23/297.05 Empty strict component of the problem is NOT empty. 592.23/297.05 592.23/297.05 2) 'With Problem ...' failed due to the following reason: 592.23/297.05 592.23/297.05 Empty strict component of the problem is NOT empty. 592.23/297.05 592.23/297.05 592.23/297.05 592.23/297.05 592.23/297.05 592.23/297.05 2) 'Best' failed due to the following reason: 592.23/297.05 592.23/297.05 None of the processors succeeded. 592.23/297.05 592.23/297.05 Details of failed attempt(s): 592.23/297.05 ----------------------------- 592.23/297.05 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 592.23/297.05 following reason: 592.23/297.05 592.23/297.05 The processor is inapplicable, reason: 592.23/297.05 Processor only applicable for innermost runtime complexity analysis 592.23/297.05 592.23/297.05 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 592.23/297.05 to the following reason: 592.23/297.05 592.23/297.05 The processor is inapplicable, reason: 592.23/297.05 Processor only applicable for innermost runtime complexity analysis 592.23/297.05 592.23/297.05 592.23/297.05 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 592.23/297.05 failed due to the following reason: 592.23/297.05 592.23/297.05 None of the processors succeeded. 592.23/297.05 592.23/297.05 Details of failed attempt(s): 592.23/297.05 ----------------------------- 592.23/297.05 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 592.23/297.05 failed due to the following reason: 592.23/297.05 592.23/297.05 match-boundness of the problem could not be verified. 592.23/297.05 592.23/297.05 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 592.23/297.05 failed due to the following reason: 592.23/297.05 592.23/297.05 match-boundness of the problem could not be verified. 592.23/297.05 592.23/297.05 592.23/297.05 592.23/297.05 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 592.23/297.05 the following reason: 592.23/297.05 592.23/297.05 We add the following weak dependency pairs: 592.23/297.05 592.23/297.05 Strict DPs: 592.23/297.05 { a__h^#(X) -> c_1(a__g^#(mark(X), X)) 592.23/297.05 , a__h^#(X) -> c_2(X) 592.23/297.05 , a__g^#(X1, X2) -> c_3(X1, X2) 592.23/297.05 , a__g^#(a(), X) -> c_4(a__f^#(b(), X)) 592.23/297.05 , a__f^#(X, X) -> c_10(a__h^#(a__a())) 592.23/297.05 , a__f^#(X1, X2) -> c_11(X1, X2) 592.23/297.05 , mark^#(a()) -> c_5(a__a^#()) 592.23/297.05 , mark^#(b()) -> c_6() 592.23/297.05 , mark^#(h(X)) -> c_7(a__h^#(mark(X))) 592.23/297.05 , mark^#(g(X1, X2)) -> c_8(a__g^#(mark(X1), X2)) 592.23/297.05 , mark^#(f(X1, X2)) -> c_9(a__f^#(mark(X1), X2)) 592.23/297.05 , a__a^#() -> c_12() 592.23/297.05 , a__a^#() -> c_13() } 592.23/297.05 592.23/297.05 and mark the set of starting terms. 592.23/297.05 592.23/297.05 We are left with following problem, upon which TcT provides the 592.23/297.05 certificate MAYBE. 592.23/297.05 592.23/297.05 Strict DPs: 592.23/297.05 { a__h^#(X) -> c_1(a__g^#(mark(X), X)) 592.23/297.05 , a__h^#(X) -> c_2(X) 592.23/297.05 , a__g^#(X1, X2) -> c_3(X1, X2) 592.23/297.05 , a__g^#(a(), X) -> c_4(a__f^#(b(), X)) 592.23/297.05 , a__f^#(X, X) -> c_10(a__h^#(a__a())) 592.23/297.05 , a__f^#(X1, X2) -> c_11(X1, X2) 592.23/297.05 , mark^#(a()) -> c_5(a__a^#()) 592.23/297.05 , mark^#(b()) -> c_6() 592.23/297.05 , mark^#(h(X)) -> c_7(a__h^#(mark(X))) 592.23/297.05 , mark^#(g(X1, X2)) -> c_8(a__g^#(mark(X1), X2)) 592.23/297.05 , mark^#(f(X1, X2)) -> c_9(a__f^#(mark(X1), X2)) 592.23/297.05 , a__a^#() -> c_12() 592.23/297.05 , a__a^#() -> c_13() } 592.23/297.05 Strict Trs: 592.23/297.05 { a__h(X) -> a__g(mark(X), X) 592.23/297.05 , a__h(X) -> h(X) 592.23/297.05 , a__g(X1, X2) -> g(X1, X2) 592.23/297.05 , a__g(a(), X) -> a__f(b(), X) 592.23/297.05 , mark(a()) -> a__a() 592.23/297.05 , mark(b()) -> b() 592.23/297.05 , mark(h(X)) -> a__h(mark(X)) 592.23/297.05 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 592.23/297.05 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 592.23/297.05 , a__f(X, X) -> a__h(a__a()) 592.23/297.05 , a__f(X1, X2) -> f(X1, X2) 592.23/297.05 , a__a() -> a() 592.23/297.05 , a__a() -> b() } 592.23/297.05 Obligation: 592.23/297.05 runtime complexity 592.23/297.05 Answer: 592.23/297.05 MAYBE 592.23/297.05 592.23/297.05 We estimate the number of application of {8,12,13} by applications 592.23/297.05 of Pre({8,12,13}) = {2,3,6,7}. Here rules are labeled as follows: 592.23/297.05 592.23/297.05 DPs: 592.23/297.05 { 1: a__h^#(X) -> c_1(a__g^#(mark(X), X)) 592.23/297.05 , 2: a__h^#(X) -> c_2(X) 592.23/297.05 , 3: a__g^#(X1, X2) -> c_3(X1, X2) 592.23/297.05 , 4: a__g^#(a(), X) -> c_4(a__f^#(b(), X)) 592.23/297.05 , 5: a__f^#(X, X) -> c_10(a__h^#(a__a())) 592.23/297.05 , 6: a__f^#(X1, X2) -> c_11(X1, X2) 592.23/297.05 , 7: mark^#(a()) -> c_5(a__a^#()) 592.23/297.05 , 8: mark^#(b()) -> c_6() 592.23/297.05 , 9: mark^#(h(X)) -> c_7(a__h^#(mark(X))) 592.23/297.05 , 10: mark^#(g(X1, X2)) -> c_8(a__g^#(mark(X1), X2)) 592.23/297.05 , 11: mark^#(f(X1, X2)) -> c_9(a__f^#(mark(X1), X2)) 592.23/297.05 , 12: a__a^#() -> c_12() 592.23/297.05 , 13: a__a^#() -> c_13() } 592.23/297.05 592.23/297.05 We are left with following problem, upon which TcT provides the 592.23/297.05 certificate MAYBE. 592.23/297.05 592.23/297.05 Strict DPs: 592.23/297.05 { a__h^#(X) -> c_1(a__g^#(mark(X), X)) 592.23/297.05 , a__h^#(X) -> c_2(X) 592.23/297.05 , a__g^#(X1, X2) -> c_3(X1, X2) 592.23/297.06 , a__g^#(a(), X) -> c_4(a__f^#(b(), X)) 592.23/297.06 , a__f^#(X, X) -> c_10(a__h^#(a__a())) 592.23/297.06 , a__f^#(X1, X2) -> c_11(X1, X2) 592.23/297.06 , mark^#(a()) -> c_5(a__a^#()) 592.23/297.06 , mark^#(h(X)) -> c_7(a__h^#(mark(X))) 592.23/297.06 , mark^#(g(X1, X2)) -> c_8(a__g^#(mark(X1), X2)) 592.23/297.06 , mark^#(f(X1, X2)) -> c_9(a__f^#(mark(X1), X2)) } 592.23/297.06 Strict Trs: 592.23/297.06 { a__h(X) -> a__g(mark(X), X) 592.23/297.06 , a__h(X) -> h(X) 592.23/297.06 , a__g(X1, X2) -> g(X1, X2) 592.23/297.06 , a__g(a(), X) -> a__f(b(), X) 592.23/297.06 , mark(a()) -> a__a() 592.23/297.06 , mark(b()) -> b() 592.23/297.06 , mark(h(X)) -> a__h(mark(X)) 592.23/297.06 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 592.23/297.06 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 592.23/297.06 , a__f(X, X) -> a__h(a__a()) 592.23/297.06 , a__f(X1, X2) -> f(X1, X2) 592.23/297.06 , a__a() -> a() 592.23/297.06 , a__a() -> b() } 592.23/297.06 Weak DPs: 592.23/297.06 { mark^#(b()) -> c_6() 592.23/297.06 , a__a^#() -> c_12() 592.23/297.06 , a__a^#() -> c_13() } 592.23/297.06 Obligation: 592.23/297.06 runtime complexity 592.23/297.06 Answer: 592.23/297.06 MAYBE 592.23/297.06 592.23/297.06 We estimate the number of application of {7} by applications of 592.23/297.06 Pre({7}) = {2,3,6}. Here rules are labeled as follows: 592.23/297.06 592.23/297.06 DPs: 592.23/297.06 { 1: a__h^#(X) -> c_1(a__g^#(mark(X), X)) 592.23/297.06 , 2: a__h^#(X) -> c_2(X) 592.23/297.06 , 3: a__g^#(X1, X2) -> c_3(X1, X2) 592.23/297.06 , 4: a__g^#(a(), X) -> c_4(a__f^#(b(), X)) 592.23/297.06 , 5: a__f^#(X, X) -> c_10(a__h^#(a__a())) 592.23/297.06 , 6: a__f^#(X1, X2) -> c_11(X1, X2) 592.23/297.06 , 7: mark^#(a()) -> c_5(a__a^#()) 592.23/297.06 , 8: mark^#(h(X)) -> c_7(a__h^#(mark(X))) 592.23/297.06 , 9: mark^#(g(X1, X2)) -> c_8(a__g^#(mark(X1), X2)) 592.23/297.06 , 10: mark^#(f(X1, X2)) -> c_9(a__f^#(mark(X1), X2)) 592.23/297.06 , 11: mark^#(b()) -> c_6() 592.23/297.06 , 12: a__a^#() -> c_12() 592.23/297.06 , 13: a__a^#() -> c_13() } 592.23/297.06 592.23/297.06 We are left with following problem, upon which TcT provides the 592.23/297.06 certificate MAYBE. 592.23/297.06 592.23/297.06 Strict DPs: 592.23/297.06 { a__h^#(X) -> c_1(a__g^#(mark(X), X)) 592.23/297.06 , a__h^#(X) -> c_2(X) 592.23/297.06 , a__g^#(X1, X2) -> c_3(X1, X2) 592.23/297.06 , a__g^#(a(), X) -> c_4(a__f^#(b(), X)) 592.23/297.06 , a__f^#(X, X) -> c_10(a__h^#(a__a())) 592.23/297.06 , a__f^#(X1, X2) -> c_11(X1, X2) 592.23/297.06 , mark^#(h(X)) -> c_7(a__h^#(mark(X))) 592.23/297.06 , mark^#(g(X1, X2)) -> c_8(a__g^#(mark(X1), X2)) 592.23/297.06 , mark^#(f(X1, X2)) -> c_9(a__f^#(mark(X1), X2)) } 592.23/297.06 Strict Trs: 592.23/297.06 { a__h(X) -> a__g(mark(X), X) 592.23/297.06 , a__h(X) -> h(X) 592.23/297.06 , a__g(X1, X2) -> g(X1, X2) 592.23/297.06 , a__g(a(), X) -> a__f(b(), X) 592.23/297.06 , mark(a()) -> a__a() 592.23/297.06 , mark(b()) -> b() 592.23/297.06 , mark(h(X)) -> a__h(mark(X)) 592.23/297.06 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 592.23/297.06 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 592.23/297.06 , a__f(X, X) -> a__h(a__a()) 592.23/297.06 , a__f(X1, X2) -> f(X1, X2) 592.23/297.06 , a__a() -> a() 592.23/297.06 , a__a() -> b() } 592.23/297.06 Weak DPs: 592.23/297.06 { mark^#(a()) -> c_5(a__a^#()) 592.23/297.06 , mark^#(b()) -> c_6() 592.23/297.06 , a__a^#() -> c_12() 592.23/297.06 , a__a^#() -> c_13() } 592.23/297.06 Obligation: 592.23/297.06 runtime complexity 592.23/297.06 Answer: 592.23/297.06 MAYBE 592.23/297.06 592.23/297.06 Empty strict component of the problem is NOT empty. 592.23/297.06 592.23/297.06 592.23/297.06 Arrrr.. 592.56/297.36 EOF