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