MAYBE 985.11/297.04 MAYBE 985.11/297.04 985.11/297.04 We are left with following problem, upon which TcT provides the 985.11/297.04 certificate MAYBE. 985.11/297.04 985.11/297.04 Strict Trs: 985.11/297.04 { fstsplit(0(), x) -> nil() 985.11/297.04 , fstsplit(s(n), nil()) -> nil() 985.11/297.04 , fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t)) 985.11/297.04 , sndsplit(0(), x) -> x 985.11/297.04 , sndsplit(s(n), nil()) -> nil() 985.11/297.04 , sndsplit(s(n), cons(h, t)) -> sndsplit(n, t) 985.11/297.04 , empty(nil()) -> true() 985.11/297.04 , empty(cons(h, t)) -> false() 985.11/297.04 , leq(0(), m) -> true() 985.11/297.04 , leq(s(n), 0()) -> false() 985.11/297.04 , leq(s(n), s(m)) -> leq(n, m) 985.11/297.04 , length(nil()) -> 0() 985.11/297.04 , length(cons(h, t)) -> s(length(t)) 985.11/297.04 , app(nil(), x) -> x 985.11/297.04 , app(cons(h, t), x) -> cons(h, app(t, x)) 985.11/297.04 , map_f(pid, nil()) -> nil() 985.11/297.04 , map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t)) 985.11/297.04 , head(cons(h, t)) -> h 985.11/297.04 , tail(cons(h, t)) -> t 985.11/297.04 , ring(st_1, in_2, st_2, in_3, st_3, m) -> 985.11/297.04 if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1))) 985.11/297.04 , ring(st_1, in_2, st_2, in_3, st_3, m) -> 985.11/297.04 if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2))) 985.11/297.04 , ring(st_1, in_2, st_2, in_3, st_3, m) -> 985.11/297.04 if_5(st_1, 985.11/297.04 in_2, 985.11/297.04 st_2, 985.11/297.04 in_3, 985.11/297.04 st_3, 985.11/297.04 m, 985.11/297.04 empty(map_f(two(), head(in_2)))) 985.11/297.04 , ring(st_1, in_2, st_2, in_3, st_3, m) -> 985.11/297.04 if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3))) 985.11/297.04 , ring(st_1, in_2, st_2, in_3, st_3, m) -> 985.11/297.04 if_9(st_1, 985.11/297.04 in_2, 985.11/297.04 st_2, 985.11/297.04 in_3, 985.11/297.04 st_3, 985.11/297.04 m, 985.11/297.04 empty(map_f(three(), head(in_3)))) 985.11/297.04 , if_1(st_1, in_2, st_2, in_3, st_3, m, false()) -> 985.11/297.04 ring(sndsplit(m, st_1), 985.11/297.04 cons(fstsplit(m, st_1), in_2), 985.11/297.04 st_2, 985.11/297.04 in_3, 985.11/297.04 st_3, 985.11/297.04 m) 985.11/297.04 , if_2(st_1, in_2, st_2, in_3, st_3, m, true()) -> 985.11/297.04 if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2))) 985.11/297.04 , if_2(st_1, in_2, st_2, in_3, st_3, m, false()) -> 985.11/297.04 if_4(st_1, 985.11/297.04 in_2, 985.11/297.04 st_2, 985.11/297.04 in_3, 985.11/297.04 st_3, 985.11/297.04 m, 985.11/297.04 empty(fstsplit(m, app(map_f(two(), head(in_2)), st_2)))) 985.11/297.04 , if_3(st_1, in_2, st_2, in_3, st_3, m, false()) -> 985.11/297.04 ring(st_1, 985.11/297.04 in_2, 985.11/297.04 sndsplit(m, st_2), 985.11/297.04 cons(fstsplit(m, st_2), in_3), 985.11/297.04 st_3, 985.11/297.04 m) 985.11/297.04 , if_4(st_1, in_2, st_2, in_3, st_3, m, false()) -> 985.11/297.04 ring(st_1, 985.11/297.04 tail(in_2), 985.11/297.04 sndsplit(m, app(map_f(two(), head(in_2)), st_2)), 985.11/297.04 cons(fstsplit(m, app(map_f(two(), head(in_2)), st_2)), in_3), 985.11/297.04 st_3, 985.11/297.04 m) 985.11/297.04 , if_5(st_1, in_2, st_2, in_3, st_3, m, true()) -> 985.11/297.04 ring(st_1, tail(in_2), st_2, in_3, st_3, m) 985.11/297.04 , if_6(st_1, in_2, st_2, in_3, st_3, m, true()) -> 985.11/297.04 if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3))) 985.11/297.04 , if_6(st_1, in_2, st_2, in_3, st_3, m, false()) -> 985.11/297.04 if_8(st_1, 985.11/297.04 in_2, 985.11/297.04 st_2, 985.11/297.04 in_3, 985.11/297.04 st_3, 985.11/297.04 m, 985.11/297.04 empty(fstsplit(m, app(map_f(three(), head(in_3)), st_3)))) 985.11/297.04 , if_7(st_1, in_2, st_2, in_3, st_3, m, false()) -> 985.11/297.04 ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m) 985.11/297.04 , if_8(st_1, in_2, st_2, in_3, st_3, m, false()) -> 985.11/297.04 ring(st_1, 985.11/297.04 in_2, 985.11/297.04 st_2, 985.11/297.04 tail(in_3), 985.11/297.04 sndsplit(m, app(map_f(three(), head(in_3)), st_3)), 985.11/297.04 m) 985.11/297.04 , if_9(st_1, in_2, st_2, in_3, st_3, m, true()) -> 985.11/297.04 ring(st_1, in_2, st_2, tail(in_3), st_3, m) } 985.11/297.04 Obligation: 985.11/297.04 innermost runtime complexity 985.11/297.04 Answer: 985.11/297.04 MAYBE 985.11/297.04 985.11/297.04 None of the processors succeeded. 985.11/297.04 985.11/297.04 Details of failed attempt(s): 985.11/297.04 ----------------------------- 985.11/297.04 1) 'empty' failed due to the following reason: 985.11/297.04 985.11/297.04 Empty strict component of the problem is NOT empty. 985.11/297.04 985.11/297.04 2) 'Best' failed due to the following reason: 985.11/297.04 985.11/297.04 None of the processors succeeded. 985.11/297.04 985.11/297.04 Details of failed attempt(s): 985.11/297.04 ----------------------------- 985.11/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 985.11/297.04 following reason: 985.11/297.04 985.11/297.04 Computation stopped due to timeout after 297.0 seconds. 985.11/297.04 985.11/297.04 2) 'Best' failed due to the following reason: 985.11/297.04 985.11/297.04 None of the processors succeeded. 985.11/297.04 985.11/297.04 Details of failed attempt(s): 985.11/297.04 ----------------------------- 985.11/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 985.11/297.04 seconds)' failed due to the following reason: 985.11/297.04 985.11/297.04 Computation stopped due to timeout after 148.0 seconds. 985.11/297.04 985.11/297.04 2) 'Best' failed due to the following reason: 985.11/297.04 985.11/297.04 None of the processors succeeded. 985.11/297.04 985.11/297.04 Details of failed attempt(s): 985.11/297.04 ----------------------------- 985.11/297.04 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 985.11/297.04 following reason: 985.11/297.04 985.11/297.04 The input cannot be shown compatible 985.11/297.04 985.11/297.04 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 985.11/297.04 to the following reason: 985.11/297.04 985.11/297.04 The input cannot be shown compatible 985.11/297.04 985.11/297.04 985.11/297.04 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 985.11/297.04 failed due to the following reason: 985.11/297.04 985.11/297.04 None of the processors succeeded. 985.11/297.04 985.11/297.04 Details of failed attempt(s): 985.11/297.04 ----------------------------- 985.11/297.04 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 985.11/297.04 failed due to the following reason: 985.11/297.04 985.11/297.04 match-boundness of the problem could not be verified. 985.11/297.04 985.11/297.04 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 985.11/297.04 failed due to the following reason: 985.11/297.04 985.11/297.04 match-boundness of the problem could not be verified. 985.11/297.04 985.11/297.04 985.11/297.04 985.11/297.04 985.11/297.04 985.11/297.04 Arrrr.. 985.33/297.29 EOF