MAYBE
MAYBE
TRS:
 {
   app(
      app(
         app(app(app(if_reach_1(), true()), x), y),
         app(app(app(edge(), u), v), i)
      ), h
   )
  ->
  app(
     app(
        app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y),
        app(app(app(edge(), u), v), i)
     ), h
  ),
  app(
     app(
        app(app(app(if_reach_1(), false()), x), y),
        app(app(app(edge(), u), v), i)
     ), h
  ) -> app(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)),
   app(
      app(
         app(app(app(if_reach_2(), true()), x), y),
         app(app(app(edge(), u), v), i)
      ), h
   )
  -> true(),
  app(
     app(
        app(app(app(if_reach_2(), false()), x), y),
        app(app(app(edge(), u), v), i)
     ), h
  ) ->
  app(
     app(or(), app(app(app(app(reach(), x), y), i), h)),
     app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())
  ),
                                           app(
                                              app(
                                                 app(app(reach(), x), y),
                                                 app(
                                                    app(app(edge(), u), v), i
                                                 )
                                              ), h
                                           )
  ->
  app(
     app(
        app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y),
        app(app(app(edge(), u), v), i)
     ), h
  ),
                                                                  app
                                                                  (
                                                                  app
                                                                  (
                                                                  app
                                                                  (
                                                                  app
                                                                  (reach(), x
                                                                  ), 
                                                                  y), 
                                                                  empty()), 
                                                                  h)
  -> false(),
                                                                app(
                                                                   app
                                                                   (
                                                                   app
                                                                   (
                                                                   app
                                                                   (
                                                                   filter2(),
                                                                   true()), 
                                                                   f), 
                                                                   x), 
                                                                   xs
                                                                )
  -> app(app(cons(), x), app(app(filter(), f), xs)),
                                                               app(
                                                                  app
                                                                  (
                                                                  app
                                                                  (
                                                                  app
                                                                  (
                                                                  filter2(),
                                                                  false()), 
                                                                  f), 
                                                                  x), 
                                                                  xs
                                                               )
  -> app(app(filter(), f), xs),
                                                                       
  app(app(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y),
                                                                               
  app(app(eq(), app(s(), x)), 0()) -> false(),
                                                                               
  app(app(eq(), 0()), app(s(), x)) -> false(),
                                                                                       
  app(app(eq(), 0()), 0()) -> true(),
                                                                                      
  app(app(or(), true()), y) -> true(),
                                                                                     
  app(app(or(), false()), y) -> y,
                                                           app(
                                                              app(
                                                                 union(),
                                                                 app(
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    edge(), x
                                                                    ), 
                                                                    y), 
                                                                    i
                                                                 )
                                                              ), h
                                                           )
  -> app(app(app(edge(), x), y), app(app(union(), i), h)),
                                                                                  
  app(app(union(), empty()), h) -> h,
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    map(), f),
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    cons(), x
                                                                    ), 
                                                                    xs))
  -> app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                                                                      
  app(app(map(), f), nil()) -> nil(),
                                                                 app(
                                                                    app
                                                                    (
                                                                    filter(),
                                                                    f),
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    cons(), x
                                                                    ), 
                                                                    xs)
                                                                 )
  -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                                                                                   
  app(app(filter(), f), nil()) -> nil()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
     app(
        app(
           app(app(app(if_reach_1(), true()), x), y),
           app(app(app(edge(), u), v), i)
        ), h
     )
    ->
    app(
       app(
          app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y),
          app(app(app(edge(), u), v), i)
       ), h
    ),
    app(
       app(
          app(app(app(if_reach_1(), false()), x), y),
          app(app(app(edge(), u), v), i)
       ), h
    ) -> app(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)),
     app(
        app(
           app(app(app(if_reach_2(), true()), x), y),
           app(app(app(edge(), u), v), i)
        ), h
     )
    -> true(),
    app(
       app(
          app(app(app(if_reach_2(), false()), x), y),
          app(app(app(edge(), u), v), i)
       ), h
    ) ->
    app(
       app(or(), app(app(app(app(reach(), x), y), i), h)),
       app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())
    ),
                                             app(
                                                app(
                                                   app(app(reach(), x), y),
                                                   app(
                                                      app(app(edge(), u), v),
                                                      i
                                                   )
                                                ), h
                                             )
    ->
    app(
       app(
          app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y),
          app(app(app(edge(), u), v), i)
       ), h
    ),
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    reach(),
                                                                    x), 
                                                                    y),
                                                                    empty()),
                                                                    h)
    -> false(),
                                                                  app
                                                                  (
                                                                  app
                                                                  (
                                                                  app
                                                                  (
                                                                  app
                                                                  (
                                                                  filter2(),
                                                                  true()), 
                                                                  f), 
                                                                  x), 
                                                                  xs)
    -> app(app(cons(), x), app(app(filter(), f), xs)),
                                                                 app(
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    app
                                                                    (
                                                                    filter2(),
                                                                    false()),
                                                                    f), 
                                                                    x), 
                                                                    xs
                                                                 )
    -> app(app(filter(), f), xs),
                                                                         
    app(app(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y),
                                                                                 
    app(app(eq(), app(s(), x)), 0()) -> false(),
                                                                                 
    app(app(eq(), 0()), app(s(), x)) -> false(),
                                                                                         
    app(app(eq(), 0()), 0()) -> true(),
                                                                                        
    app(app(or(), true()), y) -> true(),
                                                                                       
    app(app(or(), false()), y) -> y,
                                                             app(
                                                                app(
                                                                   union(),
                                                                   app
                                                                   (
                                                                   app
                                                                   (
                                                                   app
                                                                   (edge(), x
                                                                   ), 
                                                                   y), 
                                                                   i)
                                                                ), h
                                                             )
    -> app(app(app(edge(), x), y), app(app(union(), i), h)),
                                                                                    
    app(app(union(), empty()), h) -> h,
                                                                      
    app(app(map(), f), app(app(cons(), x), xs)) ->
    app(app(cons(), app(f, x)), app(app(map(), f), xs)),
                                                                                        
    app(app(map(), f), nil()) -> nil(),
                                                                   app
                                                                   (
                                                                   app
                                                                   (
                                                                   filter(),
                                                                   f),
                                                                   app
                                                                   (
                                                                   app
                                                                   (cons(), x
                                                                   ), 
                                                                   xs))
    -> app(app(app(app(filter2(), app(f, x)), f), x), xs),
                                                                                     
    app(app(filter(), f), nil()) -> nil()
   }
  Fail