MAYBE 1034.36/297.42 MAYBE 1034.36/297.42 1034.36/297.42 We are left with following problem, upon which TcT provides the 1034.36/297.42 certificate MAYBE. 1034.36/297.42 1034.36/297.42 Strict Trs: 1034.36/297.42 { purge(nil()) -> nil() 1034.36/297.42 , purge(.(x, y)) -> .(x, purge(remove(x, y))) 1034.36/297.42 , remove(x, nil()) -> nil() 1034.36/297.42 , remove(x, .(y, z)) -> 1034.36/297.42 if(=(x, y), remove(x, z), .(y, remove(x, z))) } 1034.36/297.42 Obligation: 1034.36/297.42 runtime complexity 1034.36/297.42 Answer: 1034.36/297.42 MAYBE 1034.36/297.42 1034.36/297.42 None of the processors succeeded. 1034.36/297.42 1034.36/297.42 Details of failed attempt(s): 1034.36/297.42 ----------------------------- 1034.36/297.42 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1034.36/297.42 following reason: 1034.36/297.42 1034.36/297.42 Computation stopped due to timeout after 297.0 seconds. 1034.36/297.42 1034.36/297.42 2) 'Best' failed due to the following reason: 1034.36/297.42 1034.36/297.42 None of the processors succeeded. 1034.36/297.42 1034.36/297.42 Details of failed attempt(s): 1034.36/297.42 ----------------------------- 1034.36/297.42 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1034.36/297.42 seconds)' failed due to the following reason: 1034.36/297.42 1034.36/297.42 None of the processors succeeded. 1034.36/297.42 1034.36/297.42 Details of failed attempt(s): 1034.36/297.42 ----------------------------- 1034.36/297.42 1) 'empty' failed due to the following reason: 1034.36/297.42 1034.36/297.42 Empty strict component of the problem is NOT empty. 1034.36/297.42 1034.36/297.42 2) 'With Problem ...' failed due to the following reason: 1034.36/297.42 1034.36/297.42 None of the processors succeeded. 1034.36/297.42 1034.36/297.42 Details of failed attempt(s): 1034.36/297.42 ----------------------------- 1034.36/297.42 1) 'empty' failed due to the following reason: 1034.36/297.42 1034.36/297.42 Empty strict component of the problem is NOT empty. 1034.36/297.42 1034.36/297.42 2) 'Fastest' failed due to the following reason: 1034.36/297.42 1034.36/297.42 None of the processors succeeded. 1034.36/297.42 1034.36/297.42 Details of failed attempt(s): 1034.36/297.42 ----------------------------- 1034.36/297.42 1) 'With Problem ...' failed due to the following reason: 1034.36/297.42 1034.36/297.42 None of the processors succeeded. 1034.36/297.42 1034.36/297.42 Details of failed attempt(s): 1034.36/297.42 ----------------------------- 1034.36/297.42 1) 'empty' failed due to the following reason: 1034.36/297.42 1034.36/297.42 Empty strict component of the problem is NOT empty. 1034.36/297.42 1034.36/297.42 2) 'With Problem ...' failed due to the following reason: 1034.36/297.42 1034.36/297.42 None of the processors succeeded. 1034.36/297.42 1034.36/297.42 Details of failed attempt(s): 1034.36/297.42 ----------------------------- 1034.36/297.42 1) 'empty' failed due to the following reason: 1034.36/297.42 1034.36/297.42 Empty strict component of the problem is NOT empty. 1034.36/297.42 1034.36/297.42 2) 'With Problem ...' failed due to the following reason: 1034.36/297.42 1034.36/297.42 None of the processors succeeded. 1034.36/297.42 1034.36/297.42 Details of failed attempt(s): 1034.36/297.42 ----------------------------- 1034.36/297.42 1) 'empty' failed due to the following reason: 1034.36/297.42 1034.36/297.42 Empty strict component of the problem is NOT empty. 1034.36/297.42 1034.36/297.42 2) 'With Problem ...' failed due to the following reason: 1034.36/297.42 1034.36/297.43 Empty strict component of the problem is NOT empty. 1034.36/297.43 1034.36/297.43 1034.36/297.43 1034.36/297.43 1034.36/297.43 2) 'With Problem ...' failed due to the following reason: 1034.36/297.43 1034.36/297.43 None of the processors succeeded. 1034.36/297.43 1034.36/297.43 Details of failed attempt(s): 1034.36/297.43 ----------------------------- 1034.36/297.43 1) 'empty' failed due to the following reason: 1034.36/297.43 1034.36/297.43 Empty strict component of the problem is NOT empty. 1034.36/297.43 1034.36/297.43 2) 'With Problem ...' failed due to the following reason: 1034.36/297.43 1034.36/297.43 Empty strict component of the problem is NOT empty. 1034.36/297.43 1034.36/297.43 1034.36/297.43 1034.36/297.43 1034.36/297.43 1034.36/297.43 2) 'Best' failed due to the following reason: 1034.36/297.43 1034.36/297.43 None of the processors succeeded. 1034.36/297.43 1034.36/297.43 Details of failed attempt(s): 1034.36/297.43 ----------------------------- 1034.36/297.43 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1034.36/297.43 following reason: 1034.36/297.43 1034.36/297.43 The processor is inapplicable, reason: 1034.36/297.43 Processor only applicable for innermost runtime complexity analysis 1034.36/297.43 1034.36/297.43 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1034.36/297.43 to the following reason: 1034.36/297.43 1034.36/297.43 The processor is inapplicable, reason: 1034.36/297.43 Processor only applicable for innermost runtime complexity analysis 1034.36/297.43 1034.36/297.43 1034.36/297.43 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1034.36/297.43 failed due to the following reason: 1034.36/297.43 1034.36/297.43 None of the processors succeeded. 1034.36/297.43 1034.36/297.43 Details of failed attempt(s): 1034.36/297.43 ----------------------------- 1034.36/297.43 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1034.36/297.43 failed due to the following reason: 1034.36/297.43 1034.36/297.43 match-boundness of the problem could not be verified. 1034.36/297.43 1034.36/297.43 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1034.36/297.43 failed due to the following reason: 1034.36/297.43 1034.36/297.43 match-boundness of the problem could not be verified. 1034.36/297.43 1034.36/297.43 1034.36/297.43 1034.36/297.43 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1034.36/297.43 the following reason: 1034.36/297.43 1034.36/297.43 We add the following weak dependency pairs: 1034.36/297.43 1034.36/297.43 Strict DPs: 1034.36/297.43 { purge^#(nil()) -> c_1() 1034.36/297.43 , purge^#(.(x, y)) -> c_2(x, purge^#(remove(x, y))) 1034.36/297.43 , remove^#(x, nil()) -> c_3() 1034.36/297.43 , remove^#(x, .(y, z)) -> 1034.36/297.43 c_4(x, y, remove^#(x, z), y, remove^#(x, z)) } 1034.36/297.43 1034.36/297.43 and mark the set of starting terms. 1034.36/297.43 1034.36/297.43 We are left with following problem, upon which TcT provides the 1034.36/297.43 certificate MAYBE. 1034.36/297.43 1034.36/297.43 Strict DPs: 1034.36/297.43 { purge^#(nil()) -> c_1() 1034.36/297.43 , purge^#(.(x, y)) -> c_2(x, purge^#(remove(x, y))) 1034.36/297.43 , remove^#(x, nil()) -> c_3() 1034.36/297.43 , remove^#(x, .(y, z)) -> 1034.36/297.43 c_4(x, y, remove^#(x, z), y, remove^#(x, z)) } 1034.36/297.43 Strict Trs: 1034.36/297.43 { purge(nil()) -> nil() 1034.36/297.43 , purge(.(x, y)) -> .(x, purge(remove(x, y))) 1034.36/297.43 , remove(x, nil()) -> nil() 1034.36/297.43 , remove(x, .(y, z)) -> 1034.36/297.43 if(=(x, y), remove(x, z), .(y, remove(x, z))) } 1034.36/297.43 Obligation: 1034.36/297.43 runtime complexity 1034.36/297.43 Answer: 1034.36/297.43 MAYBE 1034.36/297.43 1034.36/297.43 We estimate the number of application of {1,3} by applications of 1034.36/297.43 Pre({1,3}) = {2,4}. Here rules are labeled as follows: 1034.36/297.43 1034.36/297.43 DPs: 1034.36/297.43 { 1: purge^#(nil()) -> c_1() 1034.36/297.43 , 2: purge^#(.(x, y)) -> c_2(x, purge^#(remove(x, y))) 1034.36/297.43 , 3: remove^#(x, nil()) -> c_3() 1034.36/297.43 , 4: remove^#(x, .(y, z)) -> 1034.36/297.43 c_4(x, y, remove^#(x, z), y, remove^#(x, z)) } 1034.36/297.43 1034.36/297.43 We are left with following problem, upon which TcT provides the 1034.36/297.43 certificate MAYBE. 1034.36/297.43 1034.36/297.43 Strict DPs: 1034.36/297.43 { purge^#(.(x, y)) -> c_2(x, purge^#(remove(x, y))) 1034.36/297.43 , remove^#(x, .(y, z)) -> 1034.36/297.43 c_4(x, y, remove^#(x, z), y, remove^#(x, z)) } 1034.36/297.43 Strict Trs: 1034.36/297.43 { purge(nil()) -> nil() 1034.36/297.43 , purge(.(x, y)) -> .(x, purge(remove(x, y))) 1034.36/297.43 , remove(x, nil()) -> nil() 1034.36/297.43 , remove(x, .(y, z)) -> 1034.36/297.43 if(=(x, y), remove(x, z), .(y, remove(x, z))) } 1034.36/297.43 Weak DPs: 1034.36/297.43 { purge^#(nil()) -> c_1() 1034.36/297.43 , remove^#(x, nil()) -> c_3() } 1034.36/297.43 Obligation: 1034.36/297.43 runtime complexity 1034.36/297.43 Answer: 1034.36/297.43 MAYBE 1034.36/297.43 1034.36/297.43 Empty strict component of the problem is NOT empty. 1034.36/297.43 1034.36/297.43 1034.36/297.43 Arrrr.. 1034.65/297.67 EOF