MAYBE 905.84/297.04 MAYBE 905.84/297.04 905.84/297.04 We are left with following problem, upon which TcT provides the 905.84/297.04 certificate MAYBE. 905.84/297.04 905.84/297.04 Strict Trs: 905.84/297.04 { not(not(x)) -> x 905.84/297.04 , not(or(x, y)) -> and(not(x), not(y)) 905.84/297.04 , not(and(x, y)) -> or(not(x), not(y)) 905.84/297.04 , and(x, or(y, z)) -> or(and(x, y), and(x, z)) 905.84/297.04 , and(or(y, z), x) -> or(and(x, y), and(x, z)) } 905.84/297.04 Obligation: 905.84/297.04 runtime complexity 905.84/297.04 Answer: 905.84/297.04 MAYBE 905.84/297.04 905.84/297.04 None of the processors succeeded. 905.84/297.04 905.84/297.04 Details of failed attempt(s): 905.84/297.04 ----------------------------- 905.84/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 905.84/297.04 following reason: 905.84/297.04 905.84/297.04 Computation stopped due to timeout after 297.0 seconds. 905.84/297.04 905.84/297.04 2) 'Best' failed due to the following reason: 905.84/297.04 905.84/297.04 None of the processors succeeded. 905.84/297.04 905.84/297.04 Details of failed attempt(s): 905.84/297.04 ----------------------------- 905.84/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 905.84/297.04 seconds)' failed due to the following reason: 905.84/297.04 905.84/297.04 None of the processors succeeded. 905.84/297.04 905.84/297.04 Details of failed attempt(s): 905.84/297.04 ----------------------------- 905.84/297.04 1) 'empty' failed due to the following reason: 905.84/297.04 905.84/297.04 Empty strict component of the problem is NOT empty. 905.84/297.04 905.84/297.04 2) 'With Problem ...' failed due to the following reason: 905.84/297.04 905.84/297.04 None of the processors succeeded. 905.84/297.04 905.84/297.04 Details of failed attempt(s): 905.84/297.04 ----------------------------- 905.84/297.04 1) 'empty' failed due to the following reason: 905.84/297.04 905.84/297.04 Empty strict component of the problem is NOT empty. 905.84/297.04 905.84/297.04 2) 'Fastest' failed due to the following reason: 905.84/297.04 905.84/297.04 None of the processors succeeded. 905.84/297.04 905.84/297.04 Details of failed attempt(s): 905.84/297.04 ----------------------------- 905.84/297.04 1) 'With Problem ...' failed due to the following reason: 905.84/297.04 905.84/297.04 None of the processors succeeded. 905.84/297.04 905.84/297.04 Details of failed attempt(s): 905.84/297.04 ----------------------------- 905.84/297.04 1) 'empty' failed due to the following reason: 905.84/297.04 905.84/297.04 Empty strict component of the problem is NOT empty. 905.84/297.04 905.84/297.04 2) 'With Problem ...' failed due to the following reason: 905.84/297.04 905.84/297.04 None of the processors succeeded. 905.84/297.04 905.84/297.04 Details of failed attempt(s): 905.84/297.04 ----------------------------- 905.84/297.04 1) 'empty' failed due to the following reason: 905.84/297.04 905.84/297.04 Empty strict component of the problem is NOT empty. 905.84/297.04 905.84/297.04 2) 'With Problem ...' failed due to the following reason: 905.84/297.04 905.84/297.04 None of the processors succeeded. 905.84/297.04 905.84/297.04 Details of failed attempt(s): 905.84/297.04 ----------------------------- 905.84/297.04 1) 'empty' failed due to the following reason: 905.84/297.04 905.84/297.04 Empty strict component of the problem is NOT empty. 905.84/297.04 905.84/297.04 2) 'With Problem ...' failed due to the following reason: 905.84/297.04 905.84/297.04 Empty strict component of the problem is NOT empty. 905.84/297.04 905.84/297.04 905.84/297.04 905.84/297.04 905.84/297.04 2) 'With Problem ...' failed due to the following reason: 905.84/297.04 905.84/297.04 None of the processors succeeded. 905.84/297.04 905.84/297.04 Details of failed attempt(s): 905.84/297.04 ----------------------------- 905.84/297.04 1) 'empty' failed due to the following reason: 905.84/297.04 905.84/297.04 Empty strict component of the problem is NOT empty. 905.84/297.04 905.84/297.04 2) 'With Problem ...' failed due to the following reason: 905.84/297.04 905.84/297.04 Empty strict component of the problem is NOT empty. 905.84/297.04 905.84/297.04 905.84/297.04 905.84/297.04 905.84/297.04 905.84/297.04 2) 'Best' failed due to the following reason: 905.84/297.04 905.84/297.04 None of the processors succeeded. 905.84/297.04 905.84/297.04 Details of failed attempt(s): 905.84/297.04 ----------------------------- 905.84/297.04 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 905.84/297.04 following reason: 905.84/297.04 905.84/297.04 The processor is inapplicable, reason: 905.84/297.04 Processor only applicable for innermost runtime complexity analysis 905.84/297.04 905.84/297.04 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 905.84/297.04 to the following reason: 905.84/297.04 905.84/297.04 The processor is inapplicable, reason: 905.84/297.04 Processor only applicable for innermost runtime complexity analysis 905.84/297.04 905.84/297.04 905.84/297.04 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 905.84/297.04 failed due to the following reason: 905.84/297.04 905.84/297.04 None of the processors succeeded. 905.84/297.04 905.84/297.04 Details of failed attempt(s): 905.84/297.04 ----------------------------- 905.84/297.04 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 905.84/297.04 failed due to the following reason: 905.84/297.04 905.84/297.04 match-boundness of the problem could not be verified. 905.84/297.04 905.84/297.04 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 905.84/297.04 failed due to the following reason: 905.84/297.04 905.84/297.04 match-boundness of the problem could not be verified. 905.84/297.05 905.84/297.05 905.84/297.05 905.84/297.05 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 905.84/297.05 the following reason: 905.84/297.05 905.84/297.05 We add the following weak dependency pairs: 905.84/297.05 905.84/297.05 Strict DPs: 905.84/297.05 { not^#(not(x)) -> c_1(x) 905.84/297.05 , not^#(or(x, y)) -> c_2(and^#(not(x), not(y))) 905.84/297.05 , not^#(and(x, y)) -> c_3(not^#(x), not^#(y)) 905.84/297.05 , and^#(x, or(y, z)) -> c_4(and^#(x, y), and^#(x, z)) 905.84/297.05 , and^#(or(y, z), x) -> c_5(and^#(x, y), and^#(x, z)) } 905.84/297.05 905.84/297.05 and mark the set of starting terms. 905.84/297.05 905.84/297.05 We are left with following problem, upon which TcT provides the 905.84/297.05 certificate MAYBE. 905.84/297.05 905.84/297.05 Strict DPs: 905.84/297.05 { not^#(not(x)) -> c_1(x) 905.84/297.05 , not^#(or(x, y)) -> c_2(and^#(not(x), not(y))) 905.84/297.05 , not^#(and(x, y)) -> c_3(not^#(x), not^#(y)) 905.84/297.05 , and^#(x, or(y, z)) -> c_4(and^#(x, y), and^#(x, z)) 905.84/297.05 , and^#(or(y, z), x) -> c_5(and^#(x, y), and^#(x, z)) } 905.84/297.05 Strict Trs: 905.84/297.05 { not(not(x)) -> x 905.84/297.05 , not(or(x, y)) -> and(not(x), not(y)) 905.84/297.05 , not(and(x, y)) -> or(not(x), not(y)) 905.84/297.05 , and(x, or(y, z)) -> or(and(x, y), and(x, z)) 905.84/297.05 , and(or(y, z), x) -> or(and(x, y), and(x, z)) } 905.84/297.05 Obligation: 905.84/297.05 runtime complexity 905.84/297.05 Answer: 905.84/297.05 MAYBE 905.84/297.05 905.84/297.05 Consider the dependency graph: 905.84/297.05 905.84/297.05 1: not^#(not(x)) -> c_1(x) 905.84/297.05 -->_1 and^#(or(y, z), x) -> c_5(and^#(x, y), and^#(x, z)) :5 905.84/297.05 -->_1 and^#(x, or(y, z)) -> c_4(and^#(x, y), and^#(x, z)) :4 905.84/297.05 -->_1 not^#(and(x, y)) -> c_3(not^#(x), not^#(y)) :3 905.84/297.05 -->_1 not^#(or(x, y)) -> c_2(and^#(not(x), not(y))) :2 905.84/297.05 -->_1 not^#(not(x)) -> c_1(x) :1 905.84/297.05 905.84/297.05 2: not^#(or(x, y)) -> c_2(and^#(not(x), not(y))) 905.84/297.05 -->_1 and^#(or(y, z), x) -> c_5(and^#(x, y), and^#(x, z)) :5 905.84/297.05 -->_1 and^#(x, or(y, z)) -> c_4(and^#(x, y), and^#(x, z)) :4 905.84/297.05 905.84/297.05 3: not^#(and(x, y)) -> c_3(not^#(x), not^#(y)) 905.84/297.05 -->_2 not^#(and(x, y)) -> c_3(not^#(x), not^#(y)) :3 905.84/297.05 -->_1 not^#(and(x, y)) -> c_3(not^#(x), not^#(y)) :3 905.84/297.05 -->_2 not^#(or(x, y)) -> c_2(and^#(not(x), not(y))) :2 905.84/297.05 -->_1 not^#(or(x, y)) -> c_2(and^#(not(x), not(y))) :2 905.84/297.05 -->_2 not^#(not(x)) -> c_1(x) :1 905.84/297.05 -->_1 not^#(not(x)) -> c_1(x) :1 905.84/297.05 905.84/297.05 4: and^#(x, or(y, z)) -> c_4(and^#(x, y), and^#(x, z)) 905.84/297.05 -->_2 and^#(or(y, z), x) -> c_5(and^#(x, y), and^#(x, z)) :5 905.84/297.05 -->_1 and^#(or(y, z), x) -> c_5(and^#(x, y), and^#(x, z)) :5 905.84/297.05 -->_2 and^#(x, or(y, z)) -> c_4(and^#(x, y), and^#(x, z)) :4 905.84/297.05 -->_1 and^#(x, or(y, z)) -> c_4(and^#(x, y), and^#(x, z)) :4 905.84/297.05 905.84/297.05 5: and^#(or(y, z), x) -> c_5(and^#(x, y), and^#(x, z)) 905.84/297.05 -->_2 and^#(or(y, z), x) -> c_5(and^#(x, y), and^#(x, z)) :5 905.84/297.05 -->_1 and^#(or(y, z), x) -> c_5(and^#(x, y), and^#(x, z)) :5 905.84/297.05 -->_2 and^#(x, or(y, z)) -> c_4(and^#(x, y), and^#(x, z)) :4 905.84/297.05 -->_1 and^#(x, or(y, z)) -> c_4(and^#(x, y), and^#(x, z)) :4 905.84/297.05 905.84/297.05 905.84/297.05 Only the nodes {2,5,4} are reachable from nodes {2,4,5} that start 905.84/297.05 derivation from marked basic terms. The nodes not reachable are 905.84/297.05 removed from the problem. 905.84/297.05 905.84/297.05 We are left with following problem, upon which TcT provides the 905.84/297.05 certificate MAYBE. 905.84/297.05 905.84/297.05 Strict DPs: 905.84/297.05 { not^#(or(x, y)) -> c_2(and^#(not(x), not(y))) 905.84/297.05 , and^#(x, or(y, z)) -> c_4(and^#(x, y), and^#(x, z)) 905.84/297.05 , and^#(or(y, z), x) -> c_5(and^#(x, y), and^#(x, z)) } 905.84/297.05 Strict Trs: 905.84/297.05 { not(not(x)) -> x 905.84/297.05 , not(or(x, y)) -> and(not(x), not(y)) 905.84/297.05 , not(and(x, y)) -> or(not(x), not(y)) 905.84/297.05 , and(x, or(y, z)) -> or(and(x, y), and(x, z)) 905.84/297.05 , and(or(y, z), x) -> or(and(x, y), and(x, z)) } 905.84/297.05 Obligation: 905.84/297.05 runtime complexity 905.84/297.05 Answer: 905.84/297.05 MAYBE 905.84/297.05 905.84/297.05 Empty strict component of the problem is NOT empty. 905.84/297.05 905.84/297.05 905.84/297.05 Arrrr.. 906.53/297.62 EOF