MAYBE 1107.31/297.13 MAYBE 1107.31/297.13 1107.31/297.13 We are left with following problem, upon which TcT provides the 1107.31/297.13 certificate MAYBE. 1107.31/297.13 1107.31/297.13 Strict Trs: 1107.31/297.13 { din(der(der(X))) -> u41(din(der(X)), X) 1107.31/297.13 , din(der(plus(X, Y))) -> u21(din(der(X)), X, Y) 1107.31/297.13 , din(der(times(X, Y))) -> u31(din(der(X)), X, Y) 1107.31/297.13 , u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX) 1107.31/297.13 , u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)) 1107.31/297.13 , u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX) 1107.31/297.13 , u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))) 1107.31/297.13 , u41(dout(DX), X) -> u42(din(der(DX)), X, DX) 1107.31/297.13 , u42(dout(DDX), X, DX) -> dout(DDX) } 1107.31/297.13 Obligation: 1107.31/297.13 runtime complexity 1107.31/297.13 Answer: 1107.31/297.13 MAYBE 1107.31/297.13 1107.31/297.13 None of the processors succeeded. 1107.31/297.13 1107.31/297.13 Details of failed attempt(s): 1107.31/297.13 ----------------------------- 1107.31/297.13 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1107.31/297.13 following reason: 1107.31/297.13 1107.31/297.13 Computation stopped due to timeout after 297.0 seconds. 1107.31/297.13 1107.31/297.13 2) 'Best' failed due to the following reason: 1107.31/297.13 1107.31/297.13 None of the processors succeeded. 1107.31/297.13 1107.31/297.13 Details of failed attempt(s): 1107.31/297.13 ----------------------------- 1107.31/297.13 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1107.31/297.13 seconds)' failed due to the following reason: 1107.31/297.13 1107.31/297.13 Computation stopped due to timeout after 148.0 seconds. 1107.31/297.13 1107.31/297.13 2) 'Best' failed due to the following reason: 1107.31/297.13 1107.31/297.13 None of the processors succeeded. 1107.31/297.13 1107.31/297.13 Details of failed attempt(s): 1107.31/297.13 ----------------------------- 1107.31/297.13 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1107.31/297.13 to the following reason: 1107.31/297.13 1107.31/297.13 The processor is inapplicable, reason: 1107.31/297.13 Processor only applicable for innermost runtime complexity analysis 1107.31/297.13 1107.31/297.13 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1107.31/297.13 following reason: 1107.31/297.13 1107.31/297.13 The processor is inapplicable, reason: 1107.31/297.13 Processor only applicable for innermost runtime complexity analysis 1107.31/297.13 1107.31/297.13 1107.31/297.13 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1107.31/297.13 failed due to the following reason: 1107.31/297.13 1107.31/297.13 None of the processors succeeded. 1107.31/297.13 1107.31/297.13 Details of failed attempt(s): 1107.31/297.13 ----------------------------- 1107.31/297.13 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1107.31/297.13 failed due to the following reason: 1107.31/297.13 1107.31/297.13 match-boundness of the problem could not be verified. 1107.31/297.13 1107.31/297.13 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 1107.31/297.13 failed due to the following reason: 1107.31/297.13 1107.31/297.13 match-boundness of the problem could not be verified. 1107.31/297.13 1107.31/297.13 1107.31/297.13 1107.31/297.13 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1107.31/297.13 the following reason: 1107.31/297.13 1107.31/297.13 We add the following weak dependency pairs: 1107.31/297.13 1107.31/297.13 Strict DPs: 1107.31/297.13 { din^#(der(der(X))) -> c_1(u41^#(din(der(X)), X)) 1107.31/297.13 , din^#(der(plus(X, Y))) -> c_2(u21^#(din(der(X)), X, Y)) 1107.31/297.13 , din^#(der(times(X, Y))) -> c_3(u31^#(din(der(X)), X, Y)) 1107.31/297.13 , u41^#(dout(DX), X) -> c_8(u42^#(din(der(DX)), X, DX)) 1107.31/297.13 , u21^#(dout(DX), X, Y) -> c_4(u22^#(din(der(Y)), X, Y, DX)) 1107.31/297.13 , u31^#(dout(DX), X, Y) -> c_6(u32^#(din(der(Y)), X, Y, DX)) 1107.31/297.13 , u22^#(dout(DY), X, Y, DX) -> c_5(DX, DY) 1107.31/297.13 , u32^#(dout(DY), X, Y, DX) -> c_7(X, DY, Y, DX) 1107.31/297.13 , u42^#(dout(DDX), X, DX) -> c_9(DDX) } 1107.31/297.13 1107.31/297.13 and mark the set of starting terms. 1107.31/297.13 1107.31/297.13 We are left with following problem, upon which TcT provides the 1107.31/297.13 certificate MAYBE. 1107.31/297.13 1107.31/297.13 Strict DPs: 1107.31/297.13 { din^#(der(der(X))) -> c_1(u41^#(din(der(X)), X)) 1107.31/297.13 , din^#(der(plus(X, Y))) -> c_2(u21^#(din(der(X)), X, Y)) 1107.31/297.13 , din^#(der(times(X, Y))) -> c_3(u31^#(din(der(X)), X, Y)) 1107.31/297.13 , u41^#(dout(DX), X) -> c_8(u42^#(din(der(DX)), X, DX)) 1107.31/297.13 , u21^#(dout(DX), X, Y) -> c_4(u22^#(din(der(Y)), X, Y, DX)) 1107.31/297.13 , u31^#(dout(DX), X, Y) -> c_6(u32^#(din(der(Y)), X, Y, DX)) 1107.31/297.13 , u22^#(dout(DY), X, Y, DX) -> c_5(DX, DY) 1107.31/297.13 , u32^#(dout(DY), X, Y, DX) -> c_7(X, DY, Y, DX) 1107.31/297.13 , u42^#(dout(DDX), X, DX) -> c_9(DDX) } 1107.31/297.13 Strict Trs: 1107.31/297.13 { din(der(der(X))) -> u41(din(der(X)), X) 1107.31/297.13 , din(der(plus(X, Y))) -> u21(din(der(X)), X, Y) 1107.31/297.13 , din(der(times(X, Y))) -> u31(din(der(X)), X, Y) 1107.31/297.13 , u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX) 1107.31/297.13 , u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)) 1107.31/297.13 , u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX) 1107.31/297.13 , u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))) 1107.31/297.13 , u41(dout(DX), X) -> u42(din(der(DX)), X, DX) 1107.31/297.13 , u42(dout(DDX), X, DX) -> dout(DDX) } 1107.31/297.13 Obligation: 1107.31/297.13 runtime complexity 1107.31/297.13 Answer: 1107.31/297.13 MAYBE 1107.31/297.13 1107.31/297.13 Empty strict component of the problem is NOT empty. 1107.31/297.13 1107.31/297.13 1107.31/297.13 Arrrr.. 1107.83/297.54 EOF