MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { m1(@x) -> ::(::(#abs(#pos(#s(#0()))), ::(#abs(#pos(#s(#s(#0())))), ::(#abs(#pos(#s(#s(#s(#0()))))), nil()))), ::(::(#abs(#pos(#s(#s(#0())))), ::(#abs(#pos(#s(#s(#s(#0()))))), ::(#abs(#pos(#s(#s(#s(#s(#0())))))), nil()))), nil())) , matrixMultList(@acc, @mm) -> matrixMultList#1(@mm, @acc) , m4(@x) -> ::(::(#abs(#pos(#s(#0()))), nil()), ::(::(#abs(#pos(#s(#s(#0())))), nil()), ::(::(#abs(#pos(#s(#s(#s(#0()))))), nil()), ::(::(#abs(#pos(#s(#s(#s(#s(#0())))))), nil()), nil())))) , attach(@line, @m) -> attach#1(@line, @m) , split(@m) -> split#1(@m) , matrixMult3(@m1, @m2, @m3) -> matrixMult(matrixMult(@m1, @m2), @m3) , mult#2(nil(), @x, @xs) -> #abs(#0()) , mult#2(::(@y, @ys), @x, @xs) -> +(*(@x, @y), mult(@xs, @ys)) , transpose'(@m) -> transAcc(@m, makeBase(@m)) , split#1(nil()) -> tuple#2(nil(), nil()) , split#1(::(@l, @ls)) -> split#2(@l, @ls) , transpose(@m) -> transpose#1(@m, @m) , m2(@x) -> ::(::(#abs(#pos(#s(#0()))), ::(#abs(#pos(#s(#s(#0())))), nil())), ::(::(#abs(#pos(#s(#s(#0())))), ::(#abs(#pos(#s(#s(#s(#0()))))), nil())), ::(::(#abs(#pos(#s(#s(#s(#s(#0())))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))), nil())), nil()))) , matrixMult'(@m1, @m2) -> matrixMult'#1(@m1, @m2) , transAcc(@m, @base) -> transAcc#1(@m, @base) , mult(@l1, @l2) -> mult#1(@l1, @l2) , +(@x, @y) -> #add(@x, @y) , transAcc#1(nil(), @base) -> @base , transAcc#1(::(@l, @m'), @base) -> attach(@l, transAcc(@m', @base)) , matrixMultList#1(nil(), @acc) -> @acc , matrixMultList#1(::(@m, @ms), @acc) -> matrixMultList(matrixMult(@acc, @m), @ms) , *(@x, @y) -> #mult(@x, @y) , mkBase#1(nil()) -> nil() , mkBase#1(::(@l, @m')) -> ::(nil(), mkBase(@m')) , transpose#3(nil(), @l) -> nil() , transpose#3(::(@y, @ys), @l) -> ::(@l, transpose(::(@y, @ys))) , attach#1(nil(), @m) -> nil() , attach#1(::(@x, @xs), @m) -> attach#2(@m, @x, @xs) , transpose#2(tuple#2(@l, @m')) -> transpose#3(@m', @l) , matrixMult'#1(nil(), @m2) -> nil() , matrixMult'#1(::(@l, @ls), @m2) -> ::(lineMult(@l, @m2), matrixMult'(@ls, @m2)) , matrixMultOld(@m1, @m2) -> matrixMult'(@m1, transpose(@m2)) , split#2(nil(), @ls) -> tuple#2(nil(), nil()) , split#2(::(@x, @xs), @ls) -> split#3(split(@ls), @x, @xs) , mkBase(@m) -> mkBase#1(@m) , makeBase(@m) -> makeBase#1(@m) , mult#1(nil(), @l2) -> #abs(#0()) , mult#1(::(@x, @xs), @l2) -> mult#2(@l2, @x, @xs) , lineMult#1(nil(), @l) -> nil() , lineMult#1(::(@x, @xs), @l) -> ::(mult(@l, @x), lineMult(@l, @xs)) , attach#2(nil(), @x, @xs) -> nil() , attach#2(::(@l, @ls), @x, @xs) -> ::(::(@x, @l), attach(@xs, @ls)) , makeBase#1(nil()) -> nil() , makeBase#1(::(@l, @m')) -> mkBase(@l) , m3(@x) -> ::(::(#abs(#pos(#s(#0()))), ::(#abs(#pos(#s(#s(#0())))), ::(#abs(#pos(#s(#s(#s(#0()))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))), nil())))), ::(::(#abs(#pos(#s(#s(#0())))), ::(#abs(#pos(#s(#s(#s(#0()))))), ::(#abs(#pos(#s(#s(#s(#s(#0())))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0()))))))), nil())))), nil())) , matrixMult(@m1, @m2) -> matrixMult'(@m1, transAcc(@m2, makeBase(@m2))) , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#0()) -> #0() , #abs(#s(@x)) -> #pos(#s(@x)) , lineMult(@l, @m2) -> lineMult#1(@m2, @l) , transpose#1(nil(), @m) -> nil() , transpose#1(::(@xs, @xss), @m) -> transpose#2(split(@m)) , split#3(tuple#2(@ys, @m'), @x, @xs) -> tuple#2(::(@x, @ys), ::(@xs, @m')) } Weak Trs: { #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #add(#0(), @y) -> @y , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#neg(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#0(), #0()) -> #0() , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #succ(#0()) -> #pos(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #pred(#0()) -> #neg(#s(#0())) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..