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