MAYBE

Problem:
 app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y)
 app(app(lt(),0()),app(s(),y)) -> true()
 app(app(lt(),y),0()) -> false()
 app(app(eq(),x),x) -> true()
 app(app(eq(),app(s(),x)),0()) -> false()
 app(app(eq(),0()),app(s(),x)) -> false()
 app(app(member(),w),null()) -> false()
 app(app(member(),w),app(app(app(fork(),x),y),z)) ->
 app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app
                                                                  (app(if(),app(app(eq(),w),y)),
                                                                   true
                                                                   ()),
                                                                  app(app(member(),w),z)))

Proof:
 DP Processor:
  DPs:
   app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(lt(),x)
   app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(app(lt(),x),y)
   app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),z)
   app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(eq(),w)
   app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(eq(),w),y)
   app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(eq(),w),y))
   app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(if(),app(app(eq(),w),y)),true())
   app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
   app#(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z))
   app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),x)
   app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(lt(),w)
   app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(lt(),w),y)
   app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(lt(),w),y))
   app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
   app#(app(if(),app(app(lt(),w),y)),app(app(member(),w),x))
   app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
   app#(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(
                                                                    app
                                                                    (
                                                                    app(if(),app(app(eq(),w),y)),
                                                                    true
                                                                    ()),
                                                                    app(app(member(),w),z)))
  TRS:
   app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y)
   app(app(lt(),0()),app(s(),y)) -> true()
   app(app(lt(),y),0()) -> false()
   app(app(eq(),x),x) -> true()
   app(app(eq(),app(s(),x)),0()) -> false()
   app(app(eq(),0()),app(s(),x)) -> false()
   app(app(member(),w),null()) -> false()
   app(app(member(),w),app(app(app(fork(),x),y),z)) ->
   app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app
                                                                    (
                                                                    app(if(),app(app(eq(),w),y)),
                                                                    true
                                                                    ()),
                                                                    app(app(member(),w),z)))
  Restore Modifier:
   DPs:
    app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(lt(),x)
    app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(app(lt(),x),y)
    app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),z)
    app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(eq(),w)
    app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(eq(),w),y)
    app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(eq(),w),y))
    app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(if(),app(app(eq(),w),y)),true())
    app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
    app#(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z))
    app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),x)
    app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(lt(),w)
    app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(lt(),w),y)
    app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(lt(),w),y))
    app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
    app#(app(if(),app(app(lt(),w),y)),app(app(member(),w),x))
    app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
    app#(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app
                                                                  (app
                                                                   (app(if(),app(app(eq(),w),y)),
                                                                    true
                                                                    ()),
                                                                   app(app(member(),w),z)))
   TRS:
    app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y)
    app(app(lt(),0()),app(s(),y)) -> true()
    app(app(lt(),y),0()) -> false()
    app(app(eq(),x),x) -> true()
    app(app(eq(),app(s(),x)),0()) -> false()
    app(app(eq(),0()),app(s(),x)) -> false()
    app(app(member(),w),null()) -> false()
    app(app(member(),w),app(app(app(fork(),x),y),z)) ->
    app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(
                                                                    app
                                                                    (
                                                                    app(if(),app(app(eq(),w),y)),
                                                                    true
                                                                    ()),
                                                                    app(app(member(),w),z)))
   SCC Processor:
    #sccs: 1
    #rules: 14
    #arcs: 196/196
    DPs:
     app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(lt(),x)
     app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(app(lt(),x),y)
     app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),z)
     app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(eq(),w)
     app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(eq(),w),y)
     app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(eq(),w),y))
     app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(if(),app(app(eq(),w),y)),true())
     app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
     app#(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z))
     app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),x)
     app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(lt(),w)
     app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(lt(),w),y)
     app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(lt(),w),y))
     app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
     app#(app(if(),app(app(lt(),w),y)),app(app(member(),w),x))
     app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
     app#(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app
                                                                   (app
                                                                    (
                                                                    app(if(),app(app(eq(),w),y)),
                                                                    true
                                                                    ()),
                                                                    app(app(member(),w),z)))
    TRS:
     app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y)
     app(app(lt(),0()),app(s(),y)) -> true()
     app(app(lt(),y),0()) -> false()
     app(app(eq(),x),x) -> true()
     app(app(eq(),app(s(),x)),0()) -> false()
     app(app(eq(),0()),app(s(),x)) -> false()
     app(app(member(),w),null()) -> false()
     app(app(member(),w),app(app(app(fork(),x),y),z)) ->
     app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app
                                                                  (app
                                                                   (app(if(),app(app(eq(),w),y)),
                                                                    true
                                                                    ()),
                                                                   app(app(member(),w),z)))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [app#](x0, x1) = x0,
      
      [if] = 1,
      
      [fork] = 0,
      
      [null] = 0,
      
      [member] = 1,
      
      [eq] = 1,
      
      [false] = 0,
      
      [true] = 0,
      
      [0] = 0,
      
      [app](x0, x1) = x0,
      
      [s] = 1,
      
      [lt] = 0
     orientation:
      app#(app(lt(),app(s(),x)),app(s(),y)) = 0 >= 0 = app#(lt(),x)
      
      app#(app(lt(),app(s(),x)),app(s(),y)) = 0 >= 0 = app#(app(lt(),x),y)
      
      app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(app(member(),w),z)
      
      app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(eq(),w)
      
      app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(app(eq(),w),y)
      
      app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(if(),app(app(eq(),w),y))
      
      app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(app(if(),app(app(eq(),w),y)),true())
      
      app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z))
      
      app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(app(member(),w),x)
      
      app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 0 = app#(lt(),w)
      
      app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 0 = app#(app(lt(),w),y)
      
      app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(if(),app(app(lt(),w),y))
      
      app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(app(if(),app(app(lt(),w),y)),app(app(member(),w),x))
      
      app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app
                                                                  (app
                                                                   (if(),
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    eq(),w),
                                                                    y)),
                                                                   true
                                                                   ()),
                                                                  app
                                                                  (app
                                                                   (member(),
                                                                    w),
                                                                   z)))
      
      app(app(lt(),app(s(),x)),app(s(),y)) = 0 >= 0 = app(app(lt(),x),y)
      
      app(app(lt(),0()),app(s(),y)) = 0 >= 0 = true()
      
      app(app(lt(),y),0()) = 0 >= 0 = false()
      
      app(app(eq(),x),x) = 1 >= 0 = true()
      
      app(app(eq(),app(s(),x)),0()) = 1 >= 0 = false()
      
      app(app(eq(),0()),app(s(),x)) = 1 >= 0 = false()
      
      app(app(member(),w),null()) = 1 >= 0 = false()
      
      app(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app(
                                                                    app
                                                                    (
                                                                    if(),
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    eq(),w),
                                                                    y)),
                                                                    true
                                                                    ()),
                                                                 app(
                                                                    app
                                                                    (
                                                                    member(),
                                                                    w),
                                                                    z)))
     problem:
      DPs:
       app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(lt(),x)
       app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(app(lt(),x),y)
       app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),z)
       app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(eq(),w)
       app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(eq(),w),y)
       app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(eq(),w),y))
       app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
       app#(app(if(),app(app(eq(),w),y)),true())
       app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
       app#(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z))
       app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),x)
       app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(lt(),w),y))
       app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
       app#(app(if(),app(app(lt(),w),y)),app(app(member(),w),x))
       app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
       app#(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),
            app(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z)))
      TRS:
       app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y)
       app(app(lt(),0()),app(s(),y)) -> true()
       app(app(lt(),y),0()) -> false()
       app(app(eq(),x),x) -> true()
       app(app(eq(),app(s(),x)),0()) -> false()
       app(app(eq(),0()),app(s(),x)) -> false()
       app(app(member(),w),null()) -> false()
       app(app(member(),w),app(app(app(fork(),x),y),z)) ->
       app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app
                                                                    (
                                                                    app
                                                                    (
                                                                    app(if(),app(app(eq(),w),y)),
                                                                    true
                                                                    ()),
                                                                    app(app(member(),w),z)))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [app#](x0, x1) = x0,
       
       [if] = 0,
       
       [fork] = 0,
       
       [null] = 0,
       
       [member] = 1,
       
       [eq] = 1,
       
       [false] = 0,
       
       [true] = 0,
       
       [0] = 0,
       
       [app](x0, x1) = x0 + 1,
       
       [s] = 0,
       
       [lt] = 1
      orientation:
       app#(app(lt(),app(s(),x)),app(s(),y)) = 2 >= 1 = app#(lt(),x)
       
       app#(app(lt(),app(s(),x)),app(s(),y)) = 2 >= 2 = app#(app(lt(),x),y)
       
       app#(app(member(),w),app(app(app(fork(),x),y),z)) = 2 >= 2 = app#(app(member(),w),z)
       
       app#(app(member(),w),app(app(app(fork(),x),y),z)) = 2 >= 1 = app#(eq(),w)
       
       app#(app(member(),w),app(app(app(fork(),x),y),z)) = 2 >= 2 = app#(app(eq(),w),y)
       
       app#(app(member(),w),app(app(app(fork(),x),y),z)) = 2 >= 0 = app#(if(),app(app(eq(),w),y))
       
       app#(app(member(),w),app(app(app(fork(),x),y),z)) = 2 >= 1 = app#(app(if(),app(app(eq(),w),y)),true())
       
       app#(app(member(),w),app(app(app(fork(),x),y),z)) = 2 >= 2 = app#(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z))
       
       app#(app(member(),w),app(app(app(fork(),x),y),z)) = 2 >= 2 = app#(app(member(),w),x)
       
       app#(app(member(),w),app(app(app(fork(),x),y),z)) = 2 >= 0 = app#(if(),app(app(lt(),w),y))
       
       app#(app(member(),w),app(app(app(fork(),x),y),z)) = 2 >= 1 = app#(app(if(),app(app(lt(),w),y)),app(app(member(),w),x))
       
       app#(app(member(),w),app(app(app(fork(),x),y),z)) = 2 >= 2 = app#(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app
                                                                  (app
                                                                   (if(),
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    eq(),w),
                                                                    y)),
                                                                   true
                                                                   ()),
                                                                  app
                                                                  (app
                                                                   (member(),
                                                                    w),
                                                                   z)))
       
       app(app(lt(),app(s(),x)),app(s(),y)) = 3 >= 3 = app(app(lt(),x),y)
       
       app(app(lt(),0()),app(s(),y)) = 3 >= 0 = true()
       
       app(app(lt(),y),0()) = 3 >= 0 = false()
       
       app(app(eq(),x),x) = 3 >= 0 = true()
       
       app(app(eq(),app(s(),x)),0()) = 3 >= 0 = false()
       
       app(app(eq(),0()),app(s(),x)) = 3 >= 0 = false()
       
       app(app(member(),w),null()) = 3 >= 0 = false()
       
       app(app(member(),w),app(app(app(fork(),x),y),z)) = 3 >= 3 = app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app(
                                                                    app
                                                                    (
                                                                    if(),
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    eq(),w),
                                                                    y)),
                                                                    true
                                                                    ()),
                                                                 app(
                                                                    app
                                                                    (
                                                                    member(),
                                                                    w),
                                                                    z)))
      problem:
       DPs:
        app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(app(lt(),x),y)
        app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),z)
        app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(eq(),w),y)
        app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
        app#(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z))
        app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),x)
        app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
        app#(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),
             app(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z)))
       TRS:
        app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y)
        app(app(lt(),0()),app(s(),y)) -> true()
        app(app(lt(),y),0()) -> false()
        app(app(eq(),x),x) -> true()
        app(app(eq(),app(s(),x)),0()) -> false()
        app(app(eq(),0()),app(s(),x)) -> false()
        app(app(member(),w),null()) -> false()
        app(app(member(),w),app(app(app(fork(),x),y),z)) ->
        app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),
            app(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [app#](x0, x1) = x0,
        
        [if] = 1,
        
        [fork] = 1,
        
        [null] = 0,
        
        [member] = 1,
        
        [eq] = 0,
        
        [false] = 0,
        
        [true] = 0,
        
        [0] = 0,
        
        [app](x0, x1) = x0,
        
        [s] = 0,
        
        [lt] = 0
       orientation:
        app#(app(lt(),app(s(),x)),app(s(),y)) = 0 >= 0 = app#(app(lt(),x),y)
        
        app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(app(member(),w),z)
        
        app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 0 = app#(app(eq(),w),y)
        
        app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z))
        
        app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(app(member(),w),x)
        
        app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app
                                                                  (app
                                                                   (if(),
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    eq(),w),
                                                                    y)),
                                                                   true
                                                                   ()),
                                                                  app
                                                                  (app
                                                                   (member(),
                                                                    w),
                                                                   z)))
        
        app(app(lt(),app(s(),x)),app(s(),y)) = 0 >= 0 = app(app(lt(),x),y)
        
        app(app(lt(),0()),app(s(),y)) = 0 >= 0 = true()
        
        app(app(lt(),y),0()) = 0 >= 0 = false()
        
        app(app(eq(),x),x) = 0 >= 0 = true()
        
        app(app(eq(),app(s(),x)),0()) = 0 >= 0 = false()
        
        app(app(eq(),0()),app(s(),x)) = 0 >= 0 = false()
        
        app(app(member(),w),null()) = 1 >= 0 = false()
        
        app(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app(
                                                                    app
                                                                    (
                                                                    if(),
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    eq(),w),
                                                                    y)),
                                                                    true
                                                                    ()),
                                                                 app(
                                                                    app
                                                                    (
                                                                    member(),
                                                                    w),
                                                                    z)))
       problem:
        DPs:
         app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(app(lt(),x),y)
         app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),z)
         app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
         app#(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z))
         app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),x)
         app#(app(member(),w),app(app(app(fork(),x),y),z)) ->
         app#(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),
              app(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z)))
        TRS:
         app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y)
         app(app(lt(),0()),app(s(),y)) -> true()
         app(app(lt(),y),0()) -> false()
         app(app(eq(),x),x) -> true()
         app(app(eq(),app(s(),x)),0()) -> false()
         app(app(eq(),0()),app(s(),x)) -> false()
         app(app(member(),w),null()) -> false()
         app(app(member(),w),app(app(app(fork(),x),y),z)) ->
         app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),
             app(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z)))
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [app#](x0, x1) = x0,
         
         [if] = 0,
         
         [fork] = 0,
         
         [null] = 0,
         
         [member] = 1,
         
         [eq] = 0,
         
         [false] = 0,
         
         [true] = 0,
         
         [0] = 0,
         
         [app](x0, x1) = x0,
         
         [s] = 1,
         
         [lt] = 0
        orientation:
         app#(app(lt(),app(s(),x)),app(s(),y)) = 0 >= 0 = app#(app(lt(),x),y)
         
         app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(app(member(),w),z)
         
         app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 0 = app#(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z))
         
         app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 1 = app#(app(member(),w),x)
         
         app#(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 0 = app#(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app
                                                                  (app
                                                                   (if(),
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    eq(),w),
                                                                    y)),
                                                                   true
                                                                   ()),
                                                                  app
                                                                  (app
                                                                   (member(),
                                                                    w),
                                                                   z)))
         
         app(app(lt(),app(s(),x)),app(s(),y)) = 0 >= 0 = app(app(lt(),x),y)
         
         app(app(lt(),0()),app(s(),y)) = 0 >= 0 = true()
         
         app(app(lt(),y),0()) = 0 >= 0 = false()
         
         app(app(eq(),x),x) = 0 >= 0 = true()
         
         app(app(eq(),app(s(),x)),0()) = 0 >= 0 = false()
         
         app(app(eq(),0()),app(s(),x)) = 0 >= 0 = false()
         
         app(app(member(),w),null()) = 1 >= 0 = false()
         
         app(app(member(),w),app(app(app(fork(),x),y),z)) = 1 >= 0 = app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app(
                                                                    app
                                                                    (
                                                                    if(),
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    eq(),w),
                                                                    y)),
                                                                    true
                                                                    ()),
                                                                 app(
                                                                    app
                                                                    (
                                                                    member(),
                                                                    w),
                                                                    z)))
        problem:
         DPs:
          app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(app(lt(),x),y)
          app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),z)
          app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),x)
         TRS:
          app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y)
          app(app(lt(),0()),app(s(),y)) -> true()
          app(app(lt(),y),0()) -> false()
          app(app(eq(),x),x) -> true()
          app(app(eq(),app(s(),x)),0()) -> false()
          app(app(eq(),0()),app(s(),x)) -> false()
          app(app(member(),w),null()) -> false()
          app(app(member(),w),app(app(app(fork(),x),y),z)) ->
          app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),
              app(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z)))
        Open