TIMEOUT

We are left with following problem, upon which TcT provides the
certificate TIMEOUT.

Strict Trs:
  { #abs(#0()) -> #0()
  , #abs(#neg(@x)) -> #pos(@x)
  , #abs(#pos(@x)) -> #pos(@x)
  , #abs(#s(@x)) -> #pos(#s(@x))
  , #equal(@x, @y) -> #eq(@x, @y)
  , #greater(@x, @y) -> #ckgt(#compare(@x, @y))
  , #less(@x, @y) -> #cklt(#compare(@x, @y))
  , *(@x, @y) -> #mult(@x, @y)
  , +(@x, @y) -> #add(@x, @y)
  , -(@x, @y) -> #sub(@x, @y)
  , add(@b1, @b2) -> add'(@b1, @b2, #abs(#0()))
  , add'(@b1, @b2, @r) -> add'#1(@b1, @b2, @r)
  , add'#1(::(@x, @xs), @b2, @r) -> add'#2(@b2, @r, @x, @xs)
  , add'#1(nil(), @b2, @r) -> nil()
  , add'#2(::(@y, @ys), @r, @x, @xs) ->
    add'#3(sum(@x, @y, @r), @xs, @ys)
  , add'#2(nil(), @r, @x, @xs) -> nil()
  , sum(@x, @y, @r) -> sum#1(+(+(@x, @y), @r))
  , add'#3(tuple#2(@z, @r'), @xs, @ys) -> ::(@z, add'(@xs, @ys, @r'))
  , bitToInt(@b) -> bitToInt'(@b, #abs(#pos(#s(#0()))))
  , bitToInt'(@b, @n) -> bitToInt'#1(@b, @n)
  , bitToInt'#1(::(@x, @xs), @n) ->
    +(*(@x, @n), bitToInt'(@xs, *(@n, #pos(#s(#s(#0()))))))
  , bitToInt'#1(nil(), @n) -> #abs(#0())
  , compare(@b1, @b2) -> compare#1(@b1, @b2)
  , compare#1(::(@x, @xs), @b2) -> compare#2(@b2, @x, @xs)
  , compare#1(nil(), @b2) -> #abs(#0())
  , compare#2(::(@y, @ys), @x, @xs) ->
    compare#3(compare(@xs, @ys), @x, @y)
  , compare#2(nil(), @x, @xs) -> #abs(#0())
  , compare#3(@r, @x, @y) -> compare#4(#equal(@r, #0()), @r, @x, @y)
  , compare#4(#false(), @r, @x, @y) -> @r
  , compare#4(#true(), @r, @x, @y) ->
    compare#5(#less(@x, @y), @x, @y)
  , compare#5(#false(), @x, @y) -> compare#6(#greater(@x, @y))
  , compare#5(#true(), @x, @y) -> -(#0(), #pos(#s(#0())))
  , compare#6(#false()) -> #abs(#0())
  , compare#6(#true()) -> #abs(#pos(#s(#0())))
  , diff(@x, @y, @r) ->
    tuple#2(mod(+(+(@x, @y), @r), #pos(#s(#s(#0())))),
            diff#1(#less(-(-(@x, @y), @r), #0())))
  , mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
  , diff#1(#false()) -> #abs(#0())
  , diff#1(#true()) -> #abs(#pos(#s(#0())))
  , div(@x, @y) -> #div(@x, @y)
  , leq(@b1, @b2) -> #less(compare(@b1, @b2), #pos(#s(#0())))
  , mult(@b1, @b2) -> mult#1(@b1, @b2)
  , mult#1(::(@x, @xs), @b2) ->
    mult#2(::(#abs(#0()), mult(@xs, @b2)), @b2, @x)
  , mult#1(nil(), @b2) -> nil()
  , mult#2(@zs, @b2, @x) ->
    mult#3(#equal(@x, #pos(#s(#0()))), @b2, @zs)
  , mult#3(#false(), @b2, @zs) -> @zs
  , mult#3(#true(), @b2, @zs) -> add(@b2, @zs)
  , mult3(@b1, @b2, @b3) -> mult(mult(@b1, @b2), @b2)
  , sub(@b1, @b2) -> sub#1(sub'(@b1, @b2, #abs(#0())))
  , sub'(@b1, @b2, @r) -> sub'#1(@b1, @b2, @r)
  , sub#1(tuple#2(@b, @_@1)) -> @b
  , sub'#1(::(@x, @xs), @b2, @r) -> sub'#2(@b2, @r, @x, @xs)
  , sub'#1(nil(), @b2, @r) -> tuple#2(nil(), @r)
  , sub'#2(::(@y, @ys), @r, @x, @xs) ->
    sub'#3(diff(@x, @y, @r), @xs, @ys)
  , sub'#2(nil(), @r, @x, @xs) -> tuple#2(nil(), @r)
  , sub'#3(tuple#2(@z, @r'), @xs, @ys) ->
    sub'#4(sub'(@xs, @ys, @r'), @z)
  , sub'#4(tuple#2(@zs, @s), @z) ->
    tuple#2(sub'#5(#equal(@s, #pos(#s(#0()))), @z, @zs), @s)
  , sub'#5(#false(), @z, @zs) -> ::(@z, @zs)
  , sub'#5(#true(), @z, @zs) -> ::(#abs(#0()), @zs)
  , sum#1(@s) -> sum#2(#equal(@s, #0()), @s)
  , sum#2(#false(), @s) -> sum#3(#equal(@s, #pos(#s(#0()))), @s)
  , sum#2(#true(), @s) -> tuple#2(#abs(#0()), #abs(#0()))
  , sum#3(#false(), @s) -> sum#4(#equal(@s, #pos(#s(#s(#0())))))
  , sum#3(#true(), @s) -> tuple#2(#abs(#pos(#s(#0()))), #abs(#0()))
  , sum#4(#false()) ->
    tuple#2(#abs(#pos(#s(#0()))), #abs(#pos(#s(#0()))))
  , sum#4(#true()) -> tuple#2(#abs(#0()), #abs(#pos(#s(#0())))) }
Weak Trs:
  { #eq(#0(), #0()) -> #true()
  , #eq(#0(), #neg(@y)) -> #false()
  , #eq(#0(), #pos(@y)) -> #false()
  , #eq(#0(), #s(@y)) -> #false()
  , #eq(#neg(@x), #0()) -> #false()
  , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
  , #eq(#neg(@x), #pos(@y)) -> #false()
  , #eq(#pos(@x), #0()) -> #false()
  , #eq(#pos(@x), #neg(@y)) -> #false()
  , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
  , #eq(#s(@x), #0()) -> #false()
  , #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
  , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
    #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
  , #eq(::(@x_1, @x_2), nil()) -> #false()
  , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false()
  , #eq(nil(), ::(@y_1, @y_2)) -> #false()
  , #eq(nil(), nil()) -> #true()
  , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false()
  , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false()
  , #eq(tuple#2(@x_1, @x_2), nil()) -> #false()
  , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) ->
    #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #ckgt(#EQ()) -> #false()
  , #ckgt(#GT()) -> #true()
  , #ckgt(#LT()) -> #false()
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , #mult(#0(), #0()) -> #0()
  , #mult(#0(), #neg(@y)) -> #0()
  , #mult(#0(), #pos(@y)) -> #0()
  , #mult(#neg(@x), #0()) -> #0()
  , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
  , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
  , #mult(#pos(@x), #0()) -> #0()
  , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
  , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
  , #add(#0(), @y) -> @y
  , #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))
  , #sub(@x, #0()) -> @x
  , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
  , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
  , #div(#0(), #0()) -> #divByZero()
  , #div(#0(), #neg(@y)) -> #0()
  , #div(#0(), #pos(@y)) -> #0()
  , #div(#neg(@x), #0()) -> #divByZero()
  , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
  , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
  , #div(#pos(@x), #0()) -> #divByZero()
  , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
  , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
  , #pred(#0()) -> #neg(#s(#0()))
  , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
  , #pred(#pos(#s(#0()))) -> #0()
  , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
  , #succ(#0()) -> #pos(#s(#0()))
  , #succ(#neg(#s(#0()))) -> #0()
  , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
  , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
  , #and(#false(), #false()) -> #false()
  , #and(#false(), #true()) -> #false()
  , #and(#true(), #false()) -> #false()
  , #and(#true(), #true()) -> #true()
  , #natdiv(#0(), #0()) -> #divByZero()
  , #natdiv(#0(), #s(@y)) -> #0()
  , #natdiv(#s(@x), #0()) -> #divByZero()
  , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
  , #positive(#0()) -> #0()
  , #positive(#neg(@x)) -> #neg(@x)
  , #positive(#pos(@x)) -> #pos(@x)
  , #positive(#s(@x)) -> #pos(#s(@x))
  , #negative(#0()) -> #0()
  , #negative(#neg(@x)) -> #pos(@x)
  , #negative(#pos(@x)) -> #neg(@x)
  , #negative(#s(@x)) -> #neg(#s(@x))
  , #divsub(#0(), #0()) -> #0()
  , #divsub(#0(), #s(@y)) -> #underflow()
  , #divsub(#s(@x), #0()) -> #s(@x)
  , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
  , #natmult(#0(), @y) -> #0()
  , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
  , #natadd(#0(), @y) -> @y
  , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
  , #natdiv'(#0(), @y) -> #s(#0())
  , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
  , #natdiv'(#underflow(), @y) -> #0()
  , #natsub(@x, #0()) -> @x
  , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) }
Obligation:
  innermost runtime complexity
Answer:
  TIMEOUT

Computation stopped due to timeout after 300.0 seconds.

Arrrr..