MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            *(x,0()) -> 0()
            *(x,s(y)) -> +(*(x,y),x)
            +(x,0()) -> x
            +(x,s(y)) -> s(+(x,y))
            1() -> s(0())
            fac(0()) -> 1()
            fac(0()) -> s(0())
            fac(s(x)) -> *(s(x),fac(x))
            floop(0(),y) -> y
            floop(s(x),y) -> floop(x,*(s(x),y))
        - Signature:
            {*/2,+/2,1/0,fac/1,floop/2} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*,+,1,fac,floop} and constructors {0,s}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          *#(x,0()) -> c_1()
          *#(x,s(y)) -> c_2(+#(*(x,y),x),*#(x,y))
          +#(x,0()) -> c_3()
          +#(x,s(y)) -> c_4(+#(x,y))
          1#() -> c_5()
          fac#(0()) -> c_6(1#())
          fac#(0()) -> c_7()
          fac#(s(x)) -> c_8(*#(s(x),fac(x)),fac#(x))
          floop#(0(),y) -> c_9()
          floop#(s(x),y) -> c_10(floop#(x,*(s(x),y)),*#(s(x),y))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            *#(x,0()) -> c_1()
            *#(x,s(y)) -> c_2(+#(*(x,y),x),*#(x,y))
            +#(x,0()) -> c_3()
            +#(x,s(y)) -> c_4(+#(x,y))
            1#() -> c_5()
            fac#(0()) -> c_6(1#())
            fac#(0()) -> c_7()
            fac#(s(x)) -> c_8(*#(s(x),fac(x)),fac#(x))
            floop#(0(),y) -> c_9()
            floop#(s(x),y) -> c_10(floop#(x,*(s(x),y)),*#(s(x),y))
        - Weak TRS:
            *(x,0()) -> 0()
            *(x,s(y)) -> +(*(x,y),x)
            +(x,0()) -> x
            +(x,s(y)) -> s(+(x,y))
            1() -> s(0())
            fac(0()) -> 1()
            fac(0()) -> s(0())
            fac(s(x)) -> *(s(x),fac(x))
            floop(0(),y) -> y
            floop(s(x),y) -> floop(x,*(s(x),y))
        - Signature:
            {*/2,+/2,1/0,fac/1,floop/2,*#/2,+#/2,1#/0,fac#/1,floop#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0,c_6/1
            ,c_7/0,c_8/2,c_9/0,c_10/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#,+#,1#,fac#,floop#} and constructors {0,s}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          *(x,0()) -> 0()
          *(x,s(y)) -> +(*(x,y),x)
          +(x,0()) -> x
          +(x,s(y)) -> s(+(x,y))
          1() -> s(0())
          fac(0()) -> 1()
          fac(0()) -> s(0())
          fac(s(x)) -> *(s(x),fac(x))
          *#(x,0()) -> c_1()
          *#(x,s(y)) -> c_2(+#(*(x,y),x),*#(x,y))
          +#(x,0()) -> c_3()
          +#(x,s(y)) -> c_4(+#(x,y))
          1#() -> c_5()
          fac#(0()) -> c_6(1#())
          fac#(0()) -> c_7()
          fac#(s(x)) -> c_8(*#(s(x),fac(x)),fac#(x))
          floop#(0(),y) -> c_9()
          floop#(s(x),y) -> c_10(floop#(x,*(s(x),y)),*#(s(x),y))
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            *#(x,0()) -> c_1()
            *#(x,s(y)) -> c_2(+#(*(x,y),x),*#(x,y))
            +#(x,0()) -> c_3()
            +#(x,s(y)) -> c_4(+#(x,y))
            1#() -> c_5()
            fac#(0()) -> c_6(1#())
            fac#(0()) -> c_7()
            fac#(s(x)) -> c_8(*#(s(x),fac(x)),fac#(x))
            floop#(0(),y) -> c_9()
            floop#(s(x),y) -> c_10(floop#(x,*(s(x),y)),*#(s(x),y))
        - Weak TRS:
            *(x,0()) -> 0()
            *(x,s(y)) -> +(*(x,y),x)
            +(x,0()) -> x
            +(x,s(y)) -> s(+(x,y))
            1() -> s(0())
            fac(0()) -> 1()
            fac(0()) -> s(0())
            fac(s(x)) -> *(s(x),fac(x))
        - Signature:
            {*/2,+/2,1/0,fac/1,floop/2,*#/2,+#/2,1#/0,fac#/1,floop#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0,c_6/1
            ,c_7/0,c_8/2,c_9/0,c_10/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#,+#,1#,fac#,floop#} and constructors {0,s}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,3,5,7,9}
        by application of
          Pre({1,3,5,7,9}) = {2,4,6,8,10}.
        Here rules are labelled as follows:
          1: *#(x,0()) -> c_1()
          2: *#(x,s(y)) -> c_2(+#(*(x,y),x),*#(x,y))
          3: +#(x,0()) -> c_3()
          4: +#(x,s(y)) -> c_4(+#(x,y))
          5: 1#() -> c_5()
          6: fac#(0()) -> c_6(1#())
          7: fac#(0()) -> c_7()
          8: fac#(s(x)) -> c_8(*#(s(x),fac(x)),fac#(x))
          9: floop#(0(),y) -> c_9()
          10: floop#(s(x),y) -> c_10(floop#(x,*(s(x),y)),*#(s(x),y))
* Step 4: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            *#(x,s(y)) -> c_2(+#(*(x,y),x),*#(x,y))
            +#(x,s(y)) -> c_4(+#(x,y))
            fac#(0()) -> c_6(1#())
            fac#(s(x)) -> c_8(*#(s(x),fac(x)),fac#(x))
            floop#(s(x),y) -> c_10(floop#(x,*(s(x),y)),*#(s(x),y))
        - Weak DPs:
            *#(x,0()) -> c_1()
            +#(x,0()) -> c_3()
            1#() -> c_5()
            fac#(0()) -> c_7()
            floop#(0(),y) -> c_9()
        - Weak TRS:
            *(x,0()) -> 0()
            *(x,s(y)) -> +(*(x,y),x)
            +(x,0()) -> x
            +(x,s(y)) -> s(+(x,y))
            1() -> s(0())
            fac(0()) -> 1()
            fac(0()) -> s(0())
            fac(s(x)) -> *(s(x),fac(x))
        - Signature:
            {*/2,+/2,1/0,fac/1,floop/2,*#/2,+#/2,1#/0,fac#/1,floop#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0,c_6/1
            ,c_7/0,c_8/2,c_9/0,c_10/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#,+#,1#,fac#,floop#} and constructors {0,s}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {3}
        by application of
          Pre({3}) = {4}.
        Here rules are labelled as follows:
          1: *#(x,s(y)) -> c_2(+#(*(x,y),x),*#(x,y))
          2: +#(x,s(y)) -> c_4(+#(x,y))
          3: fac#(0()) -> c_6(1#())
          4: fac#(s(x)) -> c_8(*#(s(x),fac(x)),fac#(x))
          5: floop#(s(x),y) -> c_10(floop#(x,*(s(x),y)),*#(s(x),y))
          6: *#(x,0()) -> c_1()
          7: +#(x,0()) -> c_3()
          8: 1#() -> c_5()
          9: fac#(0()) -> c_7()
          10: floop#(0(),y) -> c_9()
* Step 5: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            *#(x,s(y)) -> c_2(+#(*(x,y),x),*#(x,y))
            +#(x,s(y)) -> c_4(+#(x,y))
            fac#(s(x)) -> c_8(*#(s(x),fac(x)),fac#(x))
            floop#(s(x),y) -> c_10(floop#(x,*(s(x),y)),*#(s(x),y))
        - Weak DPs:
            *#(x,0()) -> c_1()
            +#(x,0()) -> c_3()
            1#() -> c_5()
            fac#(0()) -> c_6(1#())
            fac#(0()) -> c_7()
            floop#(0(),y) -> c_9()
        - Weak TRS:
            *(x,0()) -> 0()
            *(x,s(y)) -> +(*(x,y),x)
            +(x,0()) -> x
            +(x,s(y)) -> s(+(x,y))
            1() -> s(0())
            fac(0()) -> 1()
            fac(0()) -> s(0())
            fac(s(x)) -> *(s(x),fac(x))
        - Signature:
            {*/2,+/2,1/0,fac/1,floop/2,*#/2,+#/2,1#/0,fac#/1,floop#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0,c_6/1
            ,c_7/0,c_8/2,c_9/0,c_10/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*#,+#,1#,fac#,floop#} and constructors {0,s}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:*#(x,s(y)) -> c_2(+#(*(x,y),x),*#(x,y))
             -->_1 +#(x,s(y)) -> c_4(+#(x,y)):2
             -->_1 +#(x,0()) -> c_3():6
             -->_2 *#(x,0()) -> c_1():5
             -->_2 *#(x,s(y)) -> c_2(+#(*(x,y),x),*#(x,y)):1
          
          2:S:+#(x,s(y)) -> c_4(+#(x,y))
             -->_1 +#(x,0()) -> c_3():6
             -->_1 +#(x,s(y)) -> c_4(+#(x,y)):2
          
          3:S:fac#(s(x)) -> c_8(*#(s(x),fac(x)),fac#(x))
             -->_2 fac#(0()) -> c_6(1#()):8
             -->_2 fac#(0()) -> c_7():9
             -->_1 *#(x,0()) -> c_1():5
             -->_2 fac#(s(x)) -> c_8(*#(s(x),fac(x)),fac#(x)):3
             -->_1 *#(x,s(y)) -> c_2(+#(*(x,y),x),*#(x,y)):1
          
          4:S:floop#(s(x),y) -> c_10(floop#(x,*(s(x),y)),*#(s(x),y))
             -->_1 floop#(0(),y) -> c_9():10
             -->_2 *#(x,0()) -> c_1():5
             -->_1 floop#(s(x),y) -> c_10(floop#(x,*(s(x),y)),*#(s(x),y)):4
             -->_2 *#(x,s(y)) -> c_2(+#(*(x,y),x),*#(x,y)):1
          
          5:W:*#(x,0()) -> c_1()
             
          
          6:W:+#(x,0()) -> c_3()
             
          
          7:W:1#() -> c_5()
             
          
          8:W:fac#(0()) -> c_6(1#())
             -->_1 1#() -> c_5():7
          
          9:W:fac#(0()) -> c_7()
             
          
          10:W:floop#(0(),y) -> c_9()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          10: floop#(0(),y) -> c_9()
          9: fac#(0()) -> c_7()
          8: fac#(0()) -> c_6(1#())
          7: 1#() -> c_5()
          5: *#(x,0()) -> c_1()
          6: +#(x,0()) -> c_3()
* Step 6: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          *#(x,s(y)) -> c_2(+#(*(x,y),x),*#(x,y))
          +#(x,s(y)) -> c_4(+#(x,y))
          fac#(s(x)) -> c_8(*#(s(x),fac(x)),fac#(x))
          floop#(s(x),y) -> c_10(floop#(x,*(s(x),y)),*#(s(x),y))
      - Weak TRS:
          *(x,0()) -> 0()
          *(x,s(y)) -> +(*(x,y),x)
          +(x,0()) -> x
          +(x,s(y)) -> s(+(x,y))
          1() -> s(0())
          fac(0()) -> 1()
          fac(0()) -> s(0())
          fac(s(x)) -> *(s(x),fac(x))
      - Signature:
          {*/2,+/2,1/0,fac/1,floop/2,*#/2,+#/2,1#/0,fac#/1,floop#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0,c_6/1
          ,c_7/0,c_8/2,c_9/0,c_10/2}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {*#,+#,1#,fac#,floop#} and constructors {0,s}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE