MAYBE 748.19/297.14 MAYBE 748.19/297.14 748.19/297.14 We are left with following problem, upon which TcT provides the 748.19/297.14 certificate MAYBE. 748.19/297.14 748.19/297.14 Strict Trs: 748.19/297.14 { active(dbl(X)) -> dbl(active(X)) 748.19/297.14 , active(dbl(0())) -> mark(0()) 748.19/297.14 , active(dbl(s(X))) -> mark(s(s(dbl(X)))) 748.19/297.14 , active(dbls(X)) -> dbls(active(X)) 748.19/297.14 , active(dbls(nil())) -> mark(nil()) 748.19/297.14 , active(dbls(cons(X, Y))) -> mark(cons(dbl(X), dbls(Y))) 748.19/297.14 , active(sel(X1, X2)) -> sel(X1, active(X2)) 748.19/297.14 , active(sel(X1, X2)) -> sel(active(X1), X2) 748.19/297.14 , active(sel(0(), cons(X, Y))) -> mark(X) 748.19/297.14 , active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)) 748.19/297.14 , active(indx(X1, X2)) -> indx(active(X1), X2) 748.19/297.14 , active(indx(nil(), X)) -> mark(nil()) 748.19/297.14 , active(indx(cons(X, Y), Z)) -> mark(cons(sel(X, Z), indx(Y, Z))) 748.19/297.14 , active(from(X)) -> mark(cons(X, from(s(X)))) 748.19/297.14 , active(dbl1(X)) -> dbl1(active(X)) 748.19/297.14 , active(dbl1(0())) -> mark(01()) 748.19/297.14 , active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) 748.19/297.14 , active(s1(X)) -> s1(active(X)) 748.19/297.14 , active(sel1(X1, X2)) -> sel1(X1, active(X2)) 748.19/297.14 , active(sel1(X1, X2)) -> sel1(active(X1), X2) 748.19/297.14 , active(sel1(0(), cons(X, Y))) -> mark(X) 748.19/297.14 , active(sel1(s(X), cons(Y, Z))) -> mark(sel1(X, Z)) 748.19/297.14 , active(quote(X)) -> quote(active(X)) 748.19/297.14 , active(quote(dbl(X))) -> mark(dbl1(X)) 748.19/297.14 , active(quote(0())) -> mark(01()) 748.19/297.14 , active(quote(s(X))) -> mark(s1(quote(X))) 748.19/297.14 , active(quote(sel(X, Y))) -> mark(sel1(X, Y)) 748.19/297.14 , dbl(mark(X)) -> mark(dbl(X)) 748.19/297.14 , dbl(ok(X)) -> ok(dbl(X)) 748.19/297.14 , s(ok(X)) -> ok(s(X)) 748.19/297.14 , dbls(mark(X)) -> mark(dbls(X)) 748.19/297.14 , dbls(ok(X)) -> ok(dbls(X)) 748.19/297.14 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 748.19/297.14 , sel(X1, mark(X2)) -> mark(sel(X1, X2)) 748.19/297.14 , sel(mark(X1), X2) -> mark(sel(X1, X2)) 748.19/297.14 , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) 748.19/297.14 , indx(mark(X1), X2) -> mark(indx(X1, X2)) 748.19/297.14 , indx(ok(X1), ok(X2)) -> ok(indx(X1, X2)) 748.19/297.14 , from(ok(X)) -> ok(from(X)) 748.19/297.14 , dbl1(mark(X)) -> mark(dbl1(X)) 748.19/297.14 , dbl1(ok(X)) -> ok(dbl1(X)) 748.19/297.14 , s1(mark(X)) -> mark(s1(X)) 748.19/297.14 , s1(ok(X)) -> ok(s1(X)) 748.19/297.14 , sel1(X1, mark(X2)) -> mark(sel1(X1, X2)) 748.19/297.14 , sel1(mark(X1), X2) -> mark(sel1(X1, X2)) 748.19/297.14 , sel1(ok(X1), ok(X2)) -> ok(sel1(X1, X2)) 748.19/297.14 , quote(mark(X)) -> mark(quote(X)) 748.19/297.14 , quote(ok(X)) -> ok(quote(X)) 748.19/297.14 , proper(dbl(X)) -> dbl(proper(X)) 748.19/297.14 , proper(0()) -> ok(0()) 748.19/297.14 , proper(s(X)) -> s(proper(X)) 748.19/297.14 , proper(dbls(X)) -> dbls(proper(X)) 748.19/297.14 , proper(nil()) -> ok(nil()) 748.19/297.14 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 748.19/297.14 , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) 748.19/297.14 , proper(indx(X1, X2)) -> indx(proper(X1), proper(X2)) 748.19/297.14 , proper(from(X)) -> from(proper(X)) 748.19/297.14 , proper(dbl1(X)) -> dbl1(proper(X)) 748.19/297.14 , proper(01()) -> ok(01()) 748.19/297.14 , proper(s1(X)) -> s1(proper(X)) 748.19/297.14 , proper(sel1(X1, X2)) -> sel1(proper(X1), proper(X2)) 748.19/297.14 , proper(quote(X)) -> quote(proper(X)) 748.19/297.14 , top(mark(X)) -> top(proper(X)) 748.19/297.14 , top(ok(X)) -> top(active(X)) } 748.19/297.14 Obligation: 748.19/297.14 innermost runtime complexity 748.19/297.14 Answer: 748.19/297.14 MAYBE 748.19/297.14 748.19/297.14 None of the processors succeeded. 748.19/297.14 748.19/297.14 Details of failed attempt(s): 748.19/297.14 ----------------------------- 748.19/297.14 1) 'empty' failed due to the following reason: 748.19/297.14 748.19/297.14 Empty strict component of the problem is NOT empty. 748.19/297.14 748.19/297.14 2) 'Best' failed due to the following reason: 748.19/297.14 748.19/297.14 None of the processors succeeded. 748.19/297.14 748.19/297.14 Details of failed attempt(s): 748.19/297.14 ----------------------------- 748.19/297.14 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 748.19/297.14 following reason: 748.19/297.14 748.19/297.14 Computation stopped due to timeout after 297.0 seconds. 748.19/297.14 748.19/297.14 2) 'Best' failed due to the following reason: 748.19/297.14 748.19/297.14 None of the processors succeeded. 748.19/297.14 748.19/297.14 Details of failed attempt(s): 748.19/297.14 ----------------------------- 748.19/297.14 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 748.19/297.14 seconds)' failed due to the following reason: 748.19/297.14 748.19/297.14 Computation stopped due to timeout after 148.0 seconds. 748.19/297.14 748.19/297.14 2) 'Best' failed due to the following reason: 748.19/297.14 748.19/297.14 None of the processors succeeded. 748.19/297.14 748.19/297.14 Details of failed attempt(s): 748.19/297.14 ----------------------------- 748.19/297.14 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 748.19/297.14 following reason: 748.19/297.14 748.19/297.14 The input cannot be shown compatible 748.19/297.14 748.19/297.14 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 748.19/297.14 to the following reason: 748.19/297.14 748.19/297.14 The input cannot be shown compatible 748.19/297.14 748.19/297.14 748.19/297.14 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 748.19/297.14 failed due to the following reason: 748.19/297.14 748.19/297.14 None of the processors succeeded. 748.19/297.14 748.19/297.14 Details of failed attempt(s): 748.19/297.14 ----------------------------- 748.19/297.14 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 748.19/297.14 failed due to the following reason: 748.19/297.14 748.19/297.14 match-boundness of the problem could not be verified. 748.19/297.14 748.19/297.14 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 748.19/297.14 failed due to the following reason: 748.19/297.14 748.19/297.14 match-boundness of the problem could not be verified. 748.19/297.14 748.19/297.14 748.19/297.14 748.19/297.14 748.19/297.14 748.19/297.14 Arrrr.. 748.50/297.47 EOF