WORST_CASE(?,O(n^2))
* Step 1: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add0(C(x,y),y') -> add0(y,C(S(),y'))
            add0(Z(),y) -> y
            goal(xs,ys) -> mul0(xs,ys)
            isZero(C(x,y)) -> False()
            isZero(Z()) -> True()
            mul0(C(x,y),y') -> add0(mul0(y,y'),y')
            mul0(Z(),y) -> Z()
            second(C(x,y)) -> y
        - Signature:
            {add0/2,goal/2,isZero/1,mul0/2,second/1} / {C/2,False/0,S/0,True/0,Z/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add0,goal,isZero,mul0,second} and constructors {C,False,S
            ,True,Z}
    + Applied Processor:
        Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
    + Details:
        Signatures used:
        ----------------
          C :: [A(1) x A(1)] -(1)-> A(1)
          C :: [A(12) x A(12)] -(12)-> A(12)
          C :: [A(15) x A(15)] -(15)-> A(15)
          C :: [A(6) x A(6)] -(6)-> A(6)
          False :: [] -(0)-> A(14)
          S :: [] -(0)-> A(15)
          True :: [] -(0)-> A(14)
          Z :: [] -(0)-> A(1)
          Z :: [] -(0)-> A(12)
          Z :: [] -(0)-> A(15)
          Z :: [] -(0)-> A(7)
          add0 :: [A(1) x A(1)] -(15)-> A(1)
          goal :: [A(15) x A(15)] -(14)-> A(0)
          isZero :: [A(12)] -(3)-> A(0)
          mul0 :: [A(15) x A(1)] -(6)-> A(1)
          second :: [A(6)] -(5)-> A(0)
        
        
        Cost-free Signatures used:
        --------------------------
          C :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          S :: [] -(0)-> A_cf(0)
          Z :: [] -(0)-> A_cf(0)
          add0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          mul0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
        
        
        Base Constructor Signatures used:
        ---------------------------------
          C_A :: [A(1) x A(1)] -(1)-> A(1)
          False_A :: [] -(0)-> A(1)
          S_A :: [] -(0)-> A(1)
          True_A :: [] -(0)-> A(1)
          Z_A :: [] -(0)-> A(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          add0(Z(),y) -> y
        2. Weak:
          add0(C(x,y),y') -> add0(y,C(S(),y'))
          goal(xs,ys) -> mul0(xs,ys)
          isZero(C(x,y)) -> False()
          isZero(Z()) -> True()
          mul0(C(x,y),y') -> add0(mul0(y,y'),y')
          mul0(Z(),y) -> Z()
          second(C(x,y)) -> y
* Step 2: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add0(C(x,y),y') -> add0(y,C(S(),y'))
            goal(xs,ys) -> mul0(xs,ys)
            isZero(C(x,y)) -> False()
            isZero(Z()) -> True()
            mul0(C(x,y),y') -> add0(mul0(y,y'),y')
            mul0(Z(),y) -> Z()
            second(C(x,y)) -> y
        - Weak TRS:
            add0(Z(),y) -> y
        - Signature:
            {add0/2,goal/2,isZero/1,mul0/2,second/1} / {C/2,False/0,S/0,True/0,Z/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add0,goal,isZero,mul0,second} and constructors {C,False,S
            ,True,Z}
    + Applied Processor:
        Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
    + Details:
        Signatures used:
        ----------------
          C :: [A(11) x A(11)] -(11)-> A(11)
          C :: [A(6) x A(6)] -(6)-> A(6)
          C :: [A(12) x A(12)] -(12)-> A(12)
          False :: [] -(0)-> A(14)
          S :: [] -(0)-> A(13)
          True :: [] -(0)-> A(14)
          Z :: [] -(0)-> A(6)
          Z :: [] -(0)-> A(12)
          Z :: [] -(0)-> A(11)
          Z :: [] -(0)-> A(13)
          add0 :: [A(11) x A(11)] -(7)-> A(11)
          goal :: [A(14) x A(15)] -(15)-> A(4)
          isZero :: [A(6)] -(6)-> A(0)
          mul0 :: [A(12) x A(1)] -(13)-> A(11)
          second :: [A(6)] -(3)-> A(0)
        
        
        Cost-free Signatures used:
        --------------------------
          C :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          S :: [] -(0)-> A_cf(0)
          Z :: [] -(0)-> A_cf(0)
          add0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          mul0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
        
        
        Base Constructor Signatures used:
        ---------------------------------
          C_A :: [A(1) x A(1)] -(1)-> A(1)
          False_A :: [] -(0)-> A(1)
          S_A :: [] -(0)-> A(1)
          True_A :: [] -(0)-> A(1)
          Z_A :: [] -(0)-> A(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          isZero(C(x,y)) -> False()
        2. Weak:
          add0(C(x,y),y') -> add0(y,C(S(),y'))
          goal(xs,ys) -> mul0(xs,ys)
          isZero(Z()) -> True()
          mul0(C(x,y),y') -> add0(mul0(y,y'),y')
          mul0(Z(),y) -> Z()
          second(C(x,y)) -> y
* Step 3: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add0(C(x,y),y') -> add0(y,C(S(),y'))
            goal(xs,ys) -> mul0(xs,ys)
            isZero(Z()) -> True()
            mul0(C(x,y),y') -> add0(mul0(y,y'),y')
            mul0(Z(),y) -> Z()
            second(C(x,y)) -> y
        - Weak TRS:
            add0(Z(),y) -> y
            isZero(C(x,y)) -> False()
        - Signature:
            {add0/2,goal/2,isZero/1,mul0/2,second/1} / {C/2,False/0,S/0,True/0,Z/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add0,goal,isZero,mul0,second} and constructors {C,False,S
            ,True,Z}
    + Applied Processor:
        Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
    + Details:
        Signatures used:
        ----------------
          C :: [A(7) x A(7)] -(7)-> A(7)
          C :: [A(15) x A(15)] -(15)-> A(15)
          C :: [A(6) x A(6)] -(6)-> A(6)
          C :: [A(14) x A(14)] -(14)-> A(14)
          False :: [] -(0)-> A(14)
          S :: [] -(0)-> A(15)
          True :: [] -(0)-> A(14)
          Z :: [] -(0)-> A(14)
          Z :: [] -(0)-> A(15)
          Z :: [] -(0)-> A(7)
          Z :: [] -(0)-> A(13)
          add0 :: [A(7) x A(7)] -(7)-> A(7)
          goal :: [A(15) x A(15)] -(14)-> A(0)
          isZero :: [A(14)] -(1)-> A(0)
          mul0 :: [A(15) x A(1)] -(11)-> A(7)
          second :: [A(6)] -(5)-> A(0)
        
        
        Cost-free Signatures used:
        --------------------------
          C :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          S :: [] -(0)-> A_cf(0)
          Z :: [] -(0)-> A_cf(0)
          add0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          mul0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
        
        
        Base Constructor Signatures used:
        ---------------------------------
          C_A :: [A(1) x A(1)] -(1)-> A(1)
          False_A :: [] -(0)-> A(1)
          S_A :: [] -(0)-> A(1)
          True_A :: [] -(0)-> A(1)
          Z_A :: [] -(0)-> A(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          goal(xs,ys) -> mul0(xs,ys)
          isZero(Z()) -> True()
        2. Weak:
          add0(C(x,y),y') -> add0(y,C(S(),y'))
          mul0(C(x,y),y') -> add0(mul0(y,y'),y')
          mul0(Z(),y) -> Z()
          second(C(x,y)) -> y
* Step 4: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add0(C(x,y),y') -> add0(y,C(S(),y'))
            mul0(C(x,y),y') -> add0(mul0(y,y'),y')
            mul0(Z(),y) -> Z()
            second(C(x,y)) -> y
        - Weak TRS:
            add0(Z(),y) -> y
            goal(xs,ys) -> mul0(xs,ys)
            isZero(C(x,y)) -> False()
            isZero(Z()) -> True()
        - Signature:
            {add0/2,goal/2,isZero/1,mul0/2,second/1} / {C/2,False/0,S/0,True/0,Z/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add0,goal,isZero,mul0,second} and constructors {C,False,S
            ,True,Z}
    + Applied Processor:
        Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
    + Details:
        Signatures used:
        ----------------
          C :: [A(0) x A(0)] -(0)-> A(0)
          C :: [A(15) x A(15)] -(15)-> A(15)
          C :: [A(14) x A(14)] -(14)-> A(14)
          False :: [] -(0)-> A(14)
          S :: [] -(0)-> A(12)
          True :: [] -(0)-> A(14)
          Z :: [] -(0)-> A(15)
          Z :: [] -(0)-> A(0)
          Z :: [] -(0)-> A(14)
          Z :: [] -(0)-> A(7)
          add0 :: [A(0) x A(0)] -(12)-> A(0)
          goal :: [A(15) x A(15)] -(14)-> A(0)
          isZero :: [A(14)] -(15)-> A(0)
          mul0 :: [A(15) x A(1)] -(0)-> A(0)
          second :: [A(0)] -(12)-> A(0)
        
        
        Cost-free Signatures used:
        --------------------------
          C :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          S :: [] -(0)-> A_cf(0)
          Z :: [] -(0)-> A_cf(0)
          add0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          mul0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
        
        
        Base Constructor Signatures used:
        ---------------------------------
          C_A :: [A(1) x A(1)] -(1)-> A(1)
          False_A :: [] -(0)-> A(1)
          S_A :: [] -(0)-> A(1)
          True_A :: [] -(0)-> A(1)
          Z_A :: [] -(0)-> A(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          second(C(x,y)) -> y
        2. Weak:
          add0(C(x,y),y') -> add0(y,C(S(),y'))
          mul0(C(x,y),y') -> add0(mul0(y,y'),y')
          mul0(Z(),y) -> Z()
* Step 5: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add0(C(x,y),y') -> add0(y,C(S(),y'))
            mul0(C(x,y),y') -> add0(mul0(y,y'),y')
            mul0(Z(),y) -> Z()
        - Weak TRS:
            add0(Z(),y) -> y
            goal(xs,ys) -> mul0(xs,ys)
            isZero(C(x,y)) -> False()
            isZero(Z()) -> True()
            second(C(x,y)) -> y
        - Signature:
            {add0/2,goal/2,isZero/1,mul0/2,second/1} / {C/2,False/0,S/0,True/0,Z/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add0,goal,isZero,mul0,second} and constructors {C,False,S
            ,True,Z}
    + Applied Processor:
        Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
    + Details:
        Signatures used:
        ----------------
          C :: [A(3) x A(3)] -(3)-> A(3)
          C :: [A(15) x A(15)] -(15)-> A(15)
          C :: [A(14) x A(14)] -(14)-> A(14)
          C :: [A(10) x A(10)] -(10)-> A(10)
          False :: [] -(0)-> A(14)
          S :: [] -(0)-> A(13)
          True :: [] -(0)-> A(14)
          Z :: [] -(0)-> A(15)
          Z :: [] -(0)-> A(3)
          Z :: [] -(0)-> A(14)
          Z :: [] -(0)-> A(5)
          add0 :: [A(3) x A(3)] -(10)-> A(3)
          goal :: [A(15) x A(15)] -(14)-> A(0)
          isZero :: [A(14)] -(15)-> A(0)
          mul0 :: [A(15) x A(1)] -(8)-> A(3)
          second :: [A(10)] -(0)-> A(4)
        
        
        Cost-free Signatures used:
        --------------------------
          C :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          S :: [] -(0)-> A_cf(0)
          Z :: [] -(0)-> A_cf(0)
          add0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          mul0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
        
        
        Base Constructor Signatures used:
        ---------------------------------
          C_A :: [A(1) x A(1)] -(1)-> A(1)
          False_A :: [] -(0)-> A(1)
          S_A :: [] -(0)-> A(1)
          True_A :: [] -(0)-> A(1)
          Z_A :: [] -(0)-> A(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          mul0(Z(),y) -> Z()
        2. Weak:
          add0(C(x,y),y') -> add0(y,C(S(),y'))
          mul0(C(x,y),y') -> add0(mul0(y,y'),y')
* Step 6: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add0(C(x,y),y') -> add0(y,C(S(),y'))
            mul0(C(x,y),y') -> add0(mul0(y,y'),y')
        - Weak TRS:
            add0(Z(),y) -> y
            goal(xs,ys) -> mul0(xs,ys)
            isZero(C(x,y)) -> False()
            isZero(Z()) -> True()
            mul0(Z(),y) -> Z()
            second(C(x,y)) -> y
        - Signature:
            {add0/2,goal/2,isZero/1,mul0/2,second/1} / {C/2,False/0,S/0,True/0,Z/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add0,goal,isZero,mul0,second} and constructors {C,False,S
            ,True,Z}
    + Applied Processor:
        Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
    + Details:
        Signatures used:
        ----------------
          C :: [A(9) x A(9)] -(9)-> A(9)
          C :: [A(13) x A(13)] -(13)-> A(13)
          C :: [A(14) x A(14)] -(14)-> A(14)
          False :: [] -(0)-> A(14)
          S :: [] -(0)-> A(15)
          True :: [] -(0)-> A(14)
          Z :: [] -(0)-> A(9)
          Z :: [] -(0)-> A(14)
          Z :: [] -(0)-> A(13)
          Z :: [] -(0)-> A(15)
          add0 :: [A(9) x A(9)] -(7)-> A(9)
          goal :: [A(15) x A(15)] -(8)-> A(2)
          isZero :: [A(14)] -(15)-> A(0)
          mul0 :: [A(13) x A(1)] -(6)-> A(9)
          second :: [A(14)] -(0)-> A(0)
        
        
        Cost-free Signatures used:
        --------------------------
          C :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          S :: [] -(0)-> A_cf(0)
          Z :: [] -(0)-> A_cf(0)
          add0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
          mul0 :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
        
        
        Base Constructor Signatures used:
        ---------------------------------
          C_A :: [A(1) x A(1)] -(1)-> A(1)
          False_A :: [] -(0)-> A(1)
          S_A :: [] -(0)-> A(1)
          True_A :: [] -(0)-> A(1)
          Z_A :: [] -(0)-> A(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          mul0(C(x,y),y') -> add0(mul0(y,y'),y')
        2. Weak:
          add0(C(x,y),y') -> add0(y,C(S(),y'))
* Step 7: Ara WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add0(C(x,y),y') -> add0(y,C(S(),y'))
        - Weak TRS:
            add0(Z(),y) -> y
            goal(xs,ys) -> mul0(xs,ys)
            isZero(C(x,y)) -> False()
            isZero(Z()) -> True()
            mul0(C(x,y),y') -> add0(mul0(y,y'),y')
            mul0(Z(),y) -> Z()
            second(C(x,y)) -> y
        - Signature:
            {add0/2,goal/2,isZero/1,mul0/2,second/1} / {C/2,False/0,S/0,True/0,Z/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add0,goal,isZero,mul0,second} and constructors {C,False,S
            ,True,Z}
    + Applied Processor:
        Ara {heuristics_ = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 15, araFindStrictRules = Just 1}
    + Details:
        Signatures used:
        ----------------
          C :: [A(0, 0) x A(14, 0)] -(14)-> A(14, 0)
          C :: [A(0, 14) x A(14, 14)] -(14)-> A(0, 14)
          C :: [A(0, 13) x A(13, 13)] -(13)-> A(0, 13)
          C :: [A(0, 0) x A(7, 0)] -(7)-> A(7, 0)
          C :: [A(0, 0) x A(1, 0)] -(1)-> A(1, 0)
          False :: [] -(0)-> A(14, 14)
          S :: [] -(0)-> A(7, 13)
          True :: [] -(0)-> A(14, 14)
          Z :: [] -(0)-> A(14, 0)
          Z :: [] -(0)-> A(0, 14)
          Z :: [] -(0)-> A(0, 13)
          Z :: [] -(0)-> A(7, 7)
          add0 :: [A(14, 0) x A(1, 0)] -(4)-> A(1, 0)
          goal :: [A(14, 15) x A(14, 14)] -(10)-> A(0, 0)
          isZero :: [A(0, 14)] -(15)-> A(0, 0)
          mul0 :: [A(0, 13) x A(0, 0)] -(4)-> A(1, 0)
          second :: [A(7, 0)] -(0)-> A(0, 0)
        
        
        Cost-free Signatures used:
        --------------------------
          C :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
          C :: [A_cf(0, 0) x A_cf(13, 0)] -(13)-> A_cf(13, 0)
          S :: [] -(0)-> A_cf(11, 11)
          S :: [] -(0)-> A_cf(15, 11)
          Z :: [] -(0)-> A_cf(0, 0)
          Z :: [] -(0)-> A_cf(13, 0)
          Z :: [] -(0)-> A_cf(15, 2)
          add0 :: [A_cf(0, 0) x A_cf(0, 0)] -(2)-> A_cf(0, 0)
          add0 :: [A_cf(13, 0) x A_cf(13, 0)] -(0)-> A_cf(13, 0)
          mul0 :: [A_cf(13, 0) x A_cf(0, 0)] -(0)-> A_cf(13, 0)
        
        
        Base Constructor Signatures used:
        ---------------------------------
          C_A :: [A(0, 0) x A(1, 0)] -(1)-> A(1, 0)
          C_A :: [A(0, 1) x A(1, 1)] -(1)-> A(0, 1)
          False_A :: [] -(0)-> A(1, 0)
          False_A :: [] -(0)-> A(0, 1)
          S_A :: [] -(0)-> A(1, 0)
          S_A :: [] -(0)-> A(0, 1)
          True_A :: [] -(0)-> A(1, 0)
          True_A :: [] -(0)-> A(0, 1)
          Z_A :: [] -(0)-> A(1, 0)
          Z_A :: [] -(0)-> A(0, 1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          add0(C(x,y),y') -> add0(y,C(S(),y'))
        2. Weak:
          
* Step 8: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            add0(C(x,y),y') -> add0(y,C(S(),y'))
            add0(Z(),y) -> y
            goal(xs,ys) -> mul0(xs,ys)
            isZero(C(x,y)) -> False()
            isZero(Z()) -> True()
            mul0(C(x,y),y') -> add0(mul0(y,y'),y')
            mul0(Z(),y) -> Z()
            second(C(x,y)) -> y
        - Signature:
            {add0/2,goal/2,isZero/1,mul0/2,second/1} / {C/2,False/0,S/0,True/0,Z/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {add0,goal,isZero,mul0,second} and constructors {C,False,S
            ,True,Z}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))