MAYBE 994.23/297.44 MAYBE 994.23/297.44 994.23/297.44 We are left with following problem, upon which TcT provides the 994.23/297.44 certificate MAYBE. 994.23/297.44 994.23/297.44 Strict Trs: 994.23/297.44 { fstsplit(0(), x) -> nil() 994.23/297.44 , fstsplit(s(n), nil()) -> nil() 994.23/297.44 , fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t)) 994.23/297.44 , sndsplit(0(), x) -> x 994.23/297.44 , sndsplit(s(n), nil()) -> nil() 994.23/297.44 , sndsplit(s(n), cons(h, t)) -> sndsplit(n, t) 994.23/297.44 , empty(nil()) -> true() 994.23/297.44 , empty(cons(h, t)) -> false() 994.23/297.44 , leq(0(), m) -> true() 994.23/297.44 , leq(s(n), 0()) -> false() 994.23/297.44 , leq(s(n), s(m)) -> leq(n, m) 994.23/297.44 , length(nil()) -> 0() 994.23/297.44 , length(cons(h, t)) -> s(length(t)) 994.23/297.44 , app(nil(), x) -> x 994.23/297.44 , app(cons(h, t), x) -> cons(h, app(t, x)) 994.23/297.44 , map_f(pid, nil()) -> nil() 994.23/297.44 , map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t)) 994.23/297.44 , process(store, m) -> if1(store, m, leq(m, length(store))) 994.23/297.44 , if1(store, m, true()) -> if2(store, m, empty(fstsplit(m, store))) 994.23/297.44 , if1(store, m, false()) -> 994.23/297.44 if3(store, m, empty(fstsplit(m, app(map_f(self(), nil()), store)))) 994.23/297.44 , if2(store, m, false()) -> 994.23/297.44 process(app(map_f(self(), nil()), sndsplit(m, store)), m) 994.23/297.44 , if3(store, m, false()) -> 994.23/297.44 process(sndsplit(m, app(map_f(self(), nil()), store)), m) } 994.23/297.44 Obligation: 994.23/297.44 runtime complexity 994.23/297.44 Answer: 994.23/297.44 MAYBE 994.23/297.44 994.23/297.44 None of the processors succeeded. 994.23/297.44 994.23/297.44 Details of failed attempt(s): 994.23/297.44 ----------------------------- 994.23/297.44 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 994.23/297.44 following reason: 994.23/297.44 994.23/297.44 Computation stopped due to timeout after 297.0 seconds. 994.23/297.44 994.23/297.44 2) 'Best' failed due to the following reason: 994.23/297.44 994.23/297.44 None of the processors succeeded. 994.23/297.44 994.23/297.44 Details of failed attempt(s): 994.23/297.44 ----------------------------- 994.23/297.44 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 994.23/297.44 seconds)' failed due to the following reason: 994.23/297.44 994.23/297.44 Computation stopped due to timeout after 148.0 seconds. 994.23/297.44 994.23/297.44 2) 'Best' failed due to the following reason: 994.23/297.44 994.23/297.44 None of the processors succeeded. 994.23/297.44 994.23/297.44 Details of failed attempt(s): 994.23/297.44 ----------------------------- 994.23/297.44 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 994.23/297.44 following reason: 994.23/297.44 994.23/297.45 The processor is inapplicable, reason: 994.23/297.45 Processor only applicable for innermost runtime complexity analysis 994.23/297.45 994.23/297.45 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 994.23/297.45 to the following reason: 994.23/297.45 994.23/297.45 The processor is inapplicable, reason: 994.23/297.45 Processor only applicable for innermost runtime complexity analysis 994.23/297.45 994.23/297.45 994.23/297.45 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 994.23/297.45 failed due to the following reason: 994.23/297.45 994.23/297.45 None of the processors succeeded. 994.23/297.45 994.23/297.45 Details of failed attempt(s): 994.23/297.45 ----------------------------- 994.23/297.45 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 994.23/297.45 failed due to the following reason: 994.23/297.45 994.23/297.45 match-boundness of the problem could not be verified. 994.23/297.45 994.23/297.45 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 994.23/297.45 failed due to the following reason: 994.23/297.45 994.23/297.45 match-boundness of the problem could not be verified. 994.23/297.45 994.23/297.45 994.23/297.45 994.23/297.45 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 994.23/297.45 the following reason: 994.23/297.45 994.23/297.45 We add the following weak dependency pairs: 994.23/297.45 994.23/297.45 Strict DPs: 994.23/297.45 { fstsplit^#(0(), x) -> c_1() 994.23/297.45 , fstsplit^#(s(n), nil()) -> c_2() 994.23/297.45 , fstsplit^#(s(n), cons(h, t)) -> c_3(h, fstsplit^#(n, t)) 994.23/297.45 , sndsplit^#(0(), x) -> c_4(x) 994.23/297.45 , sndsplit^#(s(n), nil()) -> c_5() 994.23/297.45 , sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t)) 994.23/297.45 , empty^#(nil()) -> c_7() 994.23/297.45 , empty^#(cons(h, t)) -> c_8() 994.23/297.45 , leq^#(0(), m) -> c_9() 994.23/297.45 , leq^#(s(n), 0()) -> c_10() 994.23/297.45 , leq^#(s(n), s(m)) -> c_11(leq^#(n, m)) 994.23/297.45 , length^#(nil()) -> c_12() 994.23/297.45 , length^#(cons(h, t)) -> c_13(length^#(t)) 994.23/297.45 , app^#(nil(), x) -> c_14(x) 994.23/297.45 , app^#(cons(h, t), x) -> c_15(h, app^#(t, x)) 994.23/297.45 , map_f^#(pid, nil()) -> c_16() 994.23/297.45 , map_f^#(pid, cons(h, t)) -> c_17(app^#(f(pid, h), map_f(pid, t))) 994.23/297.45 , process^#(store, m) -> 994.23/297.45 c_18(if1^#(store, m, leq(m, length(store)))) 994.23/297.45 , if1^#(store, m, true()) -> 994.23/297.45 c_19(if2^#(store, m, empty(fstsplit(m, store)))) 994.23/297.45 , if1^#(store, m, false()) -> 994.23/297.45 c_20(if3^#(store, 994.23/297.45 m, 994.23/297.45 empty(fstsplit(m, app(map_f(self(), nil()), store))))) 994.23/297.45 , if2^#(store, m, false()) -> 994.23/297.45 c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m)) 994.23/297.45 , if3^#(store, m, false()) -> 994.23/297.45 c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m)) } 994.23/297.45 994.23/297.45 and mark the set of starting terms. 994.23/297.45 994.23/297.45 We are left with following problem, upon which TcT provides the 994.23/297.45 certificate MAYBE. 994.23/297.45 994.23/297.45 Strict DPs: 994.23/297.45 { fstsplit^#(0(), x) -> c_1() 994.23/297.45 , fstsplit^#(s(n), nil()) -> c_2() 994.23/297.45 , fstsplit^#(s(n), cons(h, t)) -> c_3(h, fstsplit^#(n, t)) 994.23/297.45 , sndsplit^#(0(), x) -> c_4(x) 994.23/297.45 , sndsplit^#(s(n), nil()) -> c_5() 994.23/297.45 , sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t)) 994.23/297.45 , empty^#(nil()) -> c_7() 994.23/297.45 , empty^#(cons(h, t)) -> c_8() 994.23/297.45 , leq^#(0(), m) -> c_9() 994.23/297.45 , leq^#(s(n), 0()) -> c_10() 994.23/297.45 , leq^#(s(n), s(m)) -> c_11(leq^#(n, m)) 994.23/297.45 , length^#(nil()) -> c_12() 994.23/297.45 , length^#(cons(h, t)) -> c_13(length^#(t)) 994.23/297.45 , app^#(nil(), x) -> c_14(x) 994.23/297.45 , app^#(cons(h, t), x) -> c_15(h, app^#(t, x)) 994.23/297.45 , map_f^#(pid, nil()) -> c_16() 994.23/297.45 , map_f^#(pid, cons(h, t)) -> c_17(app^#(f(pid, h), map_f(pid, t))) 994.23/297.45 , process^#(store, m) -> 994.23/297.45 c_18(if1^#(store, m, leq(m, length(store)))) 994.23/297.45 , if1^#(store, m, true()) -> 994.23/297.45 c_19(if2^#(store, m, empty(fstsplit(m, store)))) 994.23/297.45 , if1^#(store, m, false()) -> 994.23/297.45 c_20(if3^#(store, 994.23/297.45 m, 994.23/297.45 empty(fstsplit(m, app(map_f(self(), nil()), store))))) 994.23/297.45 , if2^#(store, m, false()) -> 994.23/297.45 c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m)) 994.23/297.45 , if3^#(store, m, false()) -> 994.23/297.45 c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m)) } 994.23/297.45 Strict Trs: 994.23/297.45 { fstsplit(0(), x) -> nil() 994.23/297.45 , fstsplit(s(n), nil()) -> nil() 994.23/297.45 , fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t)) 994.23/297.45 , sndsplit(0(), x) -> x 994.23/297.45 , sndsplit(s(n), nil()) -> nil() 994.23/297.45 , sndsplit(s(n), cons(h, t)) -> sndsplit(n, t) 994.23/297.45 , empty(nil()) -> true() 994.23/297.45 , empty(cons(h, t)) -> false() 994.23/297.45 , leq(0(), m) -> true() 994.23/297.45 , leq(s(n), 0()) -> false() 994.23/297.45 , leq(s(n), s(m)) -> leq(n, m) 994.23/297.45 , length(nil()) -> 0() 994.23/297.45 , length(cons(h, t)) -> s(length(t)) 994.23/297.45 , app(nil(), x) -> x 994.23/297.45 , app(cons(h, t), x) -> cons(h, app(t, x)) 994.23/297.45 , map_f(pid, nil()) -> nil() 994.23/297.45 , map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t)) 994.23/297.45 , process(store, m) -> if1(store, m, leq(m, length(store))) 994.23/297.45 , if1(store, m, true()) -> if2(store, m, empty(fstsplit(m, store))) 994.23/297.45 , if1(store, m, false()) -> 994.23/297.45 if3(store, m, empty(fstsplit(m, app(map_f(self(), nil()), store)))) 994.23/297.45 , if2(store, m, false()) -> 994.23/297.45 process(app(map_f(self(), nil()), sndsplit(m, store)), m) 994.23/297.45 , if3(store, m, false()) -> 994.23/297.45 process(sndsplit(m, app(map_f(self(), nil()), store)), m) } 994.23/297.45 Obligation: 994.23/297.45 runtime complexity 994.23/297.45 Answer: 994.23/297.45 MAYBE 994.23/297.45 994.23/297.45 We estimate the number of application of {1,2,5,7,8,9,10,12,16,17} 994.23/297.45 by applications of Pre({1,2,5,7,8,9,10,12,16,17}) = 994.23/297.45 {3,4,6,11,13,14,15}. Here rules are labeled as follows: 994.23/297.45 994.23/297.45 DPs: 994.23/297.45 { 1: fstsplit^#(0(), x) -> c_1() 994.23/297.45 , 2: fstsplit^#(s(n), nil()) -> c_2() 994.23/297.45 , 3: fstsplit^#(s(n), cons(h, t)) -> c_3(h, fstsplit^#(n, t)) 994.23/297.45 , 4: sndsplit^#(0(), x) -> c_4(x) 994.23/297.45 , 5: sndsplit^#(s(n), nil()) -> c_5() 994.23/297.45 , 6: sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t)) 994.23/297.45 , 7: empty^#(nil()) -> c_7() 994.23/297.45 , 8: empty^#(cons(h, t)) -> c_8() 994.23/297.45 , 9: leq^#(0(), m) -> c_9() 994.23/297.45 , 10: leq^#(s(n), 0()) -> c_10() 994.23/297.45 , 11: leq^#(s(n), s(m)) -> c_11(leq^#(n, m)) 994.23/297.45 , 12: length^#(nil()) -> c_12() 994.23/297.45 , 13: length^#(cons(h, t)) -> c_13(length^#(t)) 994.23/297.45 , 14: app^#(nil(), x) -> c_14(x) 994.23/297.45 , 15: app^#(cons(h, t), x) -> c_15(h, app^#(t, x)) 994.23/297.45 , 16: map_f^#(pid, nil()) -> c_16() 994.23/297.45 , 17: map_f^#(pid, cons(h, t)) -> 994.23/297.45 c_17(app^#(f(pid, h), map_f(pid, t))) 994.23/297.45 , 18: process^#(store, m) -> 994.23/297.45 c_18(if1^#(store, m, leq(m, length(store)))) 994.23/297.45 , 19: if1^#(store, m, true()) -> 994.23/297.45 c_19(if2^#(store, m, empty(fstsplit(m, store)))) 994.23/297.45 , 20: if1^#(store, m, false()) -> 994.23/297.45 c_20(if3^#(store, 994.23/297.45 m, 994.23/297.45 empty(fstsplit(m, app(map_f(self(), nil()), store))))) 994.23/297.45 , 21: if2^#(store, m, false()) -> 994.23/297.45 c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m)) 994.23/297.45 , 22: if3^#(store, m, false()) -> 994.23/297.45 c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m)) } 994.23/297.45 994.23/297.45 We are left with following problem, upon which TcT provides the 994.23/297.45 certificate MAYBE. 994.23/297.45 994.23/297.45 Strict DPs: 994.23/297.45 { fstsplit^#(s(n), cons(h, t)) -> c_3(h, fstsplit^#(n, t)) 994.23/297.45 , sndsplit^#(0(), x) -> c_4(x) 994.23/297.45 , sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t)) 994.23/297.45 , leq^#(s(n), s(m)) -> c_11(leq^#(n, m)) 994.23/297.45 , length^#(cons(h, t)) -> c_13(length^#(t)) 994.23/297.45 , app^#(nil(), x) -> c_14(x) 994.23/297.45 , app^#(cons(h, t), x) -> c_15(h, app^#(t, x)) 994.23/297.45 , process^#(store, m) -> 994.23/297.45 c_18(if1^#(store, m, leq(m, length(store)))) 994.23/297.45 , if1^#(store, m, true()) -> 994.23/297.45 c_19(if2^#(store, m, empty(fstsplit(m, store)))) 994.23/297.45 , if1^#(store, m, false()) -> 994.23/297.45 c_20(if3^#(store, 994.23/297.45 m, 994.23/297.45 empty(fstsplit(m, app(map_f(self(), nil()), store))))) 994.23/297.45 , if2^#(store, m, false()) -> 994.23/297.45 c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m)) 994.23/297.45 , if3^#(store, m, false()) -> 994.23/297.45 c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m)) } 994.23/297.45 Strict Trs: 994.23/297.45 { fstsplit(0(), x) -> nil() 994.23/297.45 , fstsplit(s(n), nil()) -> nil() 994.23/297.45 , fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t)) 994.23/297.45 , sndsplit(0(), x) -> x 994.23/297.45 , sndsplit(s(n), nil()) -> nil() 994.23/297.45 , sndsplit(s(n), cons(h, t)) -> sndsplit(n, t) 994.23/297.45 , empty(nil()) -> true() 994.23/297.45 , empty(cons(h, t)) -> false() 994.23/297.45 , leq(0(), m) -> true() 994.23/297.45 , leq(s(n), 0()) -> false() 994.23/297.45 , leq(s(n), s(m)) -> leq(n, m) 994.23/297.45 , length(nil()) -> 0() 994.23/297.45 , length(cons(h, t)) -> s(length(t)) 994.23/297.45 , app(nil(), x) -> x 994.23/297.45 , app(cons(h, t), x) -> cons(h, app(t, x)) 994.23/297.45 , map_f(pid, nil()) -> nil() 994.23/297.45 , map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t)) 994.23/297.45 , process(store, m) -> if1(store, m, leq(m, length(store))) 994.23/297.45 , if1(store, m, true()) -> if2(store, m, empty(fstsplit(m, store))) 994.23/297.45 , if1(store, m, false()) -> 994.23/297.45 if3(store, m, empty(fstsplit(m, app(map_f(self(), nil()), store)))) 994.23/297.45 , if2(store, m, false()) -> 994.23/297.45 process(app(map_f(self(), nil()), sndsplit(m, store)), m) 994.23/297.45 , if3(store, m, false()) -> 994.23/297.45 process(sndsplit(m, app(map_f(self(), nil()), store)), m) } 994.23/297.45 Weak DPs: 994.23/297.45 { fstsplit^#(0(), x) -> c_1() 994.23/297.45 , fstsplit^#(s(n), nil()) -> c_2() 994.23/297.45 , sndsplit^#(s(n), nil()) -> c_5() 994.23/297.45 , empty^#(nil()) -> c_7() 994.23/297.45 , empty^#(cons(h, t)) -> c_8() 994.23/297.45 , leq^#(0(), m) -> c_9() 994.23/297.45 , leq^#(s(n), 0()) -> c_10() 994.23/297.45 , length^#(nil()) -> c_12() 994.23/297.45 , map_f^#(pid, nil()) -> c_16() 994.23/297.45 , map_f^#(pid, cons(h, t)) -> 994.23/297.45 c_17(app^#(f(pid, h), map_f(pid, t))) } 994.23/297.45 Obligation: 994.23/297.45 runtime complexity 994.23/297.45 Answer: 994.23/297.45 MAYBE 994.23/297.45 994.23/297.45 Empty strict component of the problem is NOT empty. 994.23/297.45 994.23/297.45 994.23/297.45 Arrrr.. 994.66/297.73 EOF