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