YES

Problem:
 app(app(eq(),0()),0()) -> true()
 app(app(eq(),0()),app(s(),x)) -> false()
 app(app(eq(),app(s(),x)),0()) -> false()
 app(app(eq(),app(s(),x)),app(s(),y)) -> app(app(eq(),x),y)
 app(app(or(),true()),y) -> true()
 app(app(or(),false()),y) -> y
 app(app(union(),empty()),h) -> h
 app(app(union(),app(app(app(edge(),x),y),i)),h) -> app(app(app(edge(),x),y),app(app(union(),i),h))
 app(app(app(app(reach(),x),y),empty()),h) -> false()
 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(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(map(),f),nil()) -> nil()
 app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))
 app(app(filter(),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(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)

Proof:
 Uncurry Processor:
  eq2(0(),0()) -> true()
  eq2(0(),s1(x)) -> false()
  eq2(s1(x),0()) -> false()
  eq2(s1(x),s1(y)) -> eq2(x,y)
  or2(true(),y) -> true()
  or2(false(),y) -> y
  union2(empty(),h) -> h
  union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
  reach4(x,y,empty(),h) -> false()
  reach4(x,y,edge3(u,v,i),h) -> if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
  if_reach_15(true(),x,y,edge3(u,v,i),h) -> if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
  if_reach_15(false(),x,y,edge3(u,v,i),h) -> reach4(x,y,i,edge3(u,v,h))
  if_reach_25(true(),x,y,edge3(u,v,i),h) -> true()
  if_reach_25(false(),x,y,edge3(u,v,i),h) -> or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
  map2(f,nil()) -> nil()
  map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
  filter2(f,nil()) -> nil()
  filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
  filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
  filter24(false(),f,x,xs) -> filter2(f,xs)
  app(eq1(x11),x12) -> eq2(x11,x12)
  app(eq(),x12) -> eq1(x12)
  app(s(),x12) -> s1(x12)
  app(or1(x11),x12) -> or2(x11,x12)
  app(or(),x12) -> or1(x12)
  app(union1(x11),x12) -> union2(x11,x12)
  app(union(),x12) -> union1(x12)
  app(edge2(x11,x10),x12) -> edge3(x11,x10,x12)
  app(edge1(x11),x12) -> edge2(x11,x12)
  app(edge(),x12) -> edge1(x12)
  app(reach3(x11,x10,x9),x12) -> reach4(x11,x10,x9,x12)
  app(reach2(x11,x10),x12) -> reach3(x11,x10,x12)
  app(reach1(x11),x12) -> reach2(x11,x12)
  app(reach(),x12) -> reach1(x12)
  app(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_15(x11,x10,x9,x8,x12)
  app(if_reach_13(x11,x10,x9),x12) -> if_reach_14(x11,x10,x9,x12)
  app(if_reach_12(x11,x10),x12) -> if_reach_13(x11,x10,x12)
  app(if_reach_11(x11),x12) -> if_reach_12(x11,x12)
  app(if_reach_1(),x12) -> if_reach_11(x12)
  app(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_25(x11,x10,x9,x8,x12)
  app(if_reach_23(x11,x10,x9),x12) -> if_reach_24(x11,x10,x9,x12)
  app(if_reach_22(x11,x10),x12) -> if_reach_23(x11,x10,x12)
  app(if_reach_21(x11),x12) -> if_reach_22(x11,x12)
  app(if_reach_2(),x12) -> if_reach_21(x12)
  app(map1(x11),x12) -> map2(x11,x12)
  app(map(),x12) -> map1(x12)
  app(cons1(x11),x12) -> cons2(x11,x12)
  app(cons(),x12) -> cons1(x12)
  app(filter1(x11),x12) -> filter2(x11,x12)
  app(filter(),x12) -> filter1(x12)
  app(filter23(x11,x10,x9),x12) -> filter24(x11,x10,x9,x12)
  app(filter22(x11,x10),x12) -> filter23(x11,x10,x12)
  app(filter21(x11),x12) -> filter22(x11,x12)
  app(filter2(),x12) -> filter21(x12)
  DP Processor:
   DPs:
    eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y)
    union{2,#}(edge3(x,y,i),h) -> union{2,#}(i,h)
    reach{4,#}(x,y,edge3(u,v,i),h) -> eq{2,#}(x,u)
    reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h)
    if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> eq{2,#}(y,v)
    if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> if_reach_2{5,#}(eq2(y,v),x,y,edge3(u,v,i),h)
    if_reach_1{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,edge3(u,v,h))
    if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> union{2,#}(i,h)
    if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(v,y,union2(i,h),empty())
    if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,h)
    if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) ->
    or{2,#}(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
    map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
    map{2,#}(f,cons2(x,xs)) -> app#(f,x)
    filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
    filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
    filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
    filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
    app#(eq1(x11),x12) -> eq{2,#}(x11,x12)
    app#(or1(x11),x12) -> or{2,#}(x11,x12)
    app#(union1(x11),x12) -> union{2,#}(x11,x12)
    app#(reach3(x11,x10,x9),x12) -> reach{4,#}(x11,x10,x9,x12)
    app#(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_1{5,#}(x11,x10,x9,x8,x12)
    app#(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_2{5,#}(x11,x10,x9,x8,x12)
    app#(map1(x11),x12) -> map{2,#}(x11,x12)
    app#(filter1(x11),x12) -> filter{2,#}(x11,x12)
    app#(filter23(x11,x10,x9),x12) -> filter2{4,#}(x11,x10,x9,x12)
   TRS:
    eq2(0(),0()) -> true()
    eq2(0(),s1(x)) -> false()
    eq2(s1(x),0()) -> false()
    eq2(s1(x),s1(y)) -> eq2(x,y)
    or2(true(),y) -> true()
    or2(false(),y) -> y
    union2(empty(),h) -> h
    union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
    reach4(x,y,empty(),h) -> false()
    reach4(x,y,edge3(u,v,i),h) -> if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
    if_reach_15(true(),x,y,edge3(u,v,i),h) -> if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
    if_reach_15(false(),x,y,edge3(u,v,i),h) -> reach4(x,y,i,edge3(u,v,h))
    if_reach_25(true(),x,y,edge3(u,v,i),h) -> true()
    if_reach_25(false(),x,y,edge3(u,v,i),h) -> or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
    map2(f,nil()) -> nil()
    map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
    filter2(f,nil()) -> nil()
    filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
    filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
    filter24(false(),f,x,xs) -> filter2(f,xs)
    app(eq1(x11),x12) -> eq2(x11,x12)
    app(eq(),x12) -> eq1(x12)
    app(s(),x12) -> s1(x12)
    app(or1(x11),x12) -> or2(x11,x12)
    app(or(),x12) -> or1(x12)
    app(union1(x11),x12) -> union2(x11,x12)
    app(union(),x12) -> union1(x12)
    app(edge2(x11,x10),x12) -> edge3(x11,x10,x12)
    app(edge1(x11),x12) -> edge2(x11,x12)
    app(edge(),x12) -> edge1(x12)
    app(reach3(x11,x10,x9),x12) -> reach4(x11,x10,x9,x12)
    app(reach2(x11,x10),x12) -> reach3(x11,x10,x12)
    app(reach1(x11),x12) -> reach2(x11,x12)
    app(reach(),x12) -> reach1(x12)
    app(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_15(x11,x10,x9,x8,x12)
    app(if_reach_13(x11,x10,x9),x12) -> if_reach_14(x11,x10,x9,x12)
    app(if_reach_12(x11,x10),x12) -> if_reach_13(x11,x10,x12)
    app(if_reach_11(x11),x12) -> if_reach_12(x11,x12)
    app(if_reach_1(),x12) -> if_reach_11(x12)
    app(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_25(x11,x10,x9,x8,x12)
    app(if_reach_23(x11,x10,x9),x12) -> if_reach_24(x11,x10,x9,x12)
    app(if_reach_22(x11,x10),x12) -> if_reach_23(x11,x10,x12)
    app(if_reach_21(x11),x12) -> if_reach_22(x11,x12)
    app(if_reach_2(),x12) -> if_reach_21(x12)
    app(map1(x11),x12) -> map2(x11,x12)
    app(map(),x12) -> map1(x12)
    app(cons1(x11),x12) -> cons2(x11,x12)
    app(cons(),x12) -> cons1(x12)
    app(filter1(x11),x12) -> filter2(x11,x12)
    app(filter(),x12) -> filter1(x12)
    app(filter23(x11,x10,x9),x12) -> filter24(x11,x10,x9,x12)
    app(filter22(x11,x10),x12) -> filter23(x11,x10,x12)
    app(filter21(x11),x12) -> filter22(x11,x12)
    app(filter2(),x12) -> filter21(x12)
   TDG Processor:
    DPs:
     eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y)
     union{2,#}(edge3(x,y,i),h) -> union{2,#}(i,h)
     reach{4,#}(x,y,edge3(u,v,i),h) -> eq{2,#}(x,u)
     reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h)
     if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> eq{2,#}(y,v)
     if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> if_reach_2{5,#}(eq2(y,v),x,y,edge3(u,v,i),h)
     if_reach_1{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,edge3(u,v,h))
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> union{2,#}(i,h)
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(v,y,union2(i,h),empty())
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,h)
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) ->
     or{2,#}(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     app#(eq1(x11),x12) -> eq{2,#}(x11,x12)
     app#(or1(x11),x12) -> or{2,#}(x11,x12)
     app#(union1(x11),x12) -> union{2,#}(x11,x12)
     app#(reach3(x11,x10,x9),x12) -> reach{4,#}(x11,x10,x9,x12)
     app#(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_1{5,#}(x11,x10,x9,x8,x12)
     app#(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_2{5,#}(x11,x10,x9,x8,x12)
     app#(map1(x11),x12) -> map{2,#}(x11,x12)
     app#(filter1(x11),x12) -> filter{2,#}(x11,x12)
     app#(filter23(x11,x10,x9),x12) -> filter2{4,#}(x11,x10,x9,x12)
    TRS:
     eq2(0(),0()) -> true()
     eq2(0(),s1(x)) -> false()
     eq2(s1(x),0()) -> false()
     eq2(s1(x),s1(y)) -> eq2(x,y)
     or2(true(),y) -> true()
     or2(false(),y) -> y
     union2(empty(),h) -> h
     union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
     reach4(x,y,empty(),h) -> false()
     reach4(x,y,edge3(u,v,i),h) -> if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
     if_reach_15(true(),x,y,edge3(u,v,i),h) -> if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
     if_reach_15(false(),x,y,edge3(u,v,i),h) -> reach4(x,y,i,edge3(u,v,h))
     if_reach_25(true(),x,y,edge3(u,v,i),h) -> true()
     if_reach_25(false(),x,y,edge3(u,v,i),h) ->
     or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
     map2(f,nil()) -> nil()
     map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
     filter2(f,nil()) -> nil()
     filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
     filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
     filter24(false(),f,x,xs) -> filter2(f,xs)
     app(eq1(x11),x12) -> eq2(x11,x12)
     app(eq(),x12) -> eq1(x12)
     app(s(),x12) -> s1(x12)
     app(or1(x11),x12) -> or2(x11,x12)
     app(or(),x12) -> or1(x12)
     app(union1(x11),x12) -> union2(x11,x12)
     app(union(),x12) -> union1(x12)
     app(edge2(x11,x10),x12) -> edge3(x11,x10,x12)
     app(edge1(x11),x12) -> edge2(x11,x12)
     app(edge(),x12) -> edge1(x12)
     app(reach3(x11,x10,x9),x12) -> reach4(x11,x10,x9,x12)
     app(reach2(x11,x10),x12) -> reach3(x11,x10,x12)
     app(reach1(x11),x12) -> reach2(x11,x12)
     app(reach(),x12) -> reach1(x12)
     app(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_15(x11,x10,x9,x8,x12)
     app(if_reach_13(x11,x10,x9),x12) -> if_reach_14(x11,x10,x9,x12)
     app(if_reach_12(x11,x10),x12) -> if_reach_13(x11,x10,x12)
     app(if_reach_11(x11),x12) -> if_reach_12(x11,x12)
     app(if_reach_1(),x12) -> if_reach_11(x12)
     app(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_25(x11,x10,x9,x8,x12)
     app(if_reach_23(x11,x10,x9),x12) -> if_reach_24(x11,x10,x9,x12)
     app(if_reach_22(x11,x10),x12) -> if_reach_23(x11,x10,x12)
     app(if_reach_21(x11),x12) -> if_reach_22(x11,x12)
     app(if_reach_2(),x12) -> if_reach_21(x12)
     app(map1(x11),x12) -> map2(x11,x12)
     app(map(),x12) -> map1(x12)
     app(cons1(x11),x12) -> cons2(x11,x12)
     app(cons(),x12) -> cons1(x12)
     app(filter1(x11),x12) -> filter2(x11,x12)
     app(filter(),x12) -> filter1(x12)
     app(filter23(x11,x10,x9),x12) -> filter24(x11,x10,x9,x12)
     app(filter22(x11,x10),x12) -> filter23(x11,x10,x12)
     app(filter21(x11),x12) -> filter22(x11,x12)
     app(filter2(),x12) -> filter21(x12)
    graph:
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) ->
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) ->
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(filter23(x11,x10,x9),x12) -> filter2{4,#}(x11,x10,x9,x12)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(filter1(x11),x12) -> filter{2,#}(x11,x12)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(map1(x11),x12) -> map{2,#}(x11,x12)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_2{5,#}(x11,x10,x9,x8,x12)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_1{5,#}(x11,x10,x9,x8,x12)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(reach3(x11,x10,x9),x12) -> reach{4,#}(x11,x10,x9,x12)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(union1(x11),x12) -> union{2,#}(x11,x12)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(or1(x11),x12) -> or{2,#}(x11,x12)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(eq1(x11),x12) -> eq{2,#}(x11,x12)
     app#(filter23(x11,x10,x9),x12) -> filter2{4,#}(x11,x10,x9,x12) ->
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     app#(filter23(x11,x10,x9),x12) -> filter2{4,#}(x11,x10,x9,x12) ->
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     app#(filter1(x11),x12) -> filter{2,#}(x11,x12) ->
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
     app#(filter1(x11),x12) -> filter{2,#}(x11,x12) ->
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     app#(map1(x11),x12) -> map{2,#}(x11,x12) ->
     map{2,#}(f,cons2(x,xs)) -> app#(f,x)
     app#(map1(x11),x12) -> map{2,#}(x11,x12) ->
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
     app#(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_2{5,#}(x11,x10,x9,x8,x12) ->
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) ->
     or{2,#}(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
     app#(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_2{5,#}(x11,x10,x9,x8,x12) ->
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,h)
     app#(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_2{5,#}(x11,x10,x9,x8,x12) ->
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(v,y,union2(i,h),empty())
     app#(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_2{5,#}(x11,x10,x9,x8,x12) ->
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> union{2,#}(i,h)
     app#(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_1{5,#}(x11,x10,x9,x8,x12) ->
     if_reach_1{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,edge3(u,v,h))
     app#(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_1{5,#}(x11,x10,x9,x8,x12) ->
     if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> if_reach_2{5,#}(eq2(y,v),x,y,edge3(u,v,i),h)
     app#(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_1{5,#}(x11,x10,x9,x8,x12) ->
     if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> eq{2,#}(y,v)
     app#(reach3(x11,x10,x9),x12) -> reach{4,#}(x11,x10,x9,x12) ->
     reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h)
     app#(reach3(x11,x10,x9),x12) -> reach{4,#}(x11,x10,x9,x12) ->
     reach{4,#}(x,y,edge3(u,v,i),h) -> eq{2,#}(x,u)
     app#(union1(x11),x12) -> union{2,#}(x11,x12) ->
     union{2,#}(edge3(x,y,i),h) -> union{2,#}(i,h)
     app#(eq1(x11),x12) -> eq{2,#}(x11,x12) ->
     eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(filter23(x11,x10,x9),x12) -> filter2{4,#}(x11,x10,x9,x12)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(filter1(x11),x12) -> filter{2,#}(x11,x12)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(map1(x11),x12) -> map{2,#}(x11,x12)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_2{5,#}(x11,x10,x9,x8,x12)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_1{5,#}(x11,x10,x9,x8,x12)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(reach3(x11,x10,x9),x12) -> reach{4,#}(x11,x10,x9,x12)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(union1(x11),x12) -> union{2,#}(x11,x12)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(or1(x11),x12) -> or{2,#}(x11,x12)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(eq1(x11),x12) -> eq{2,#}(x11,x12)
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) ->
     map{2,#}(f,cons2(x,xs)) -> app#(f,x)
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) ->
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,h) ->
     reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h)
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,h) ->
     reach{4,#}(x,y,edge3(u,v,i),h) -> eq{2,#}(x,u)
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(v,y,union2(i,h),empty()) ->
     reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h)
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(v,y,union2(i,h),empty()) ->
     reach{4,#}(x,y,edge3(u,v,i),h) -> eq{2,#}(x,u)
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> union{2,#}(i,h) ->
     union{2,#}(edge3(x,y,i),h) -> union{2,#}(i,h)
     if_reach_1{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,edge3(u,v,h)) ->
     reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h)
     if_reach_1{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,edge3(u,v,h)) ->
     reach{4,#}(x,y,edge3(u,v,i),h) -> eq{2,#}(x,u)
     if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> if_reach_2{5,#}(eq2(y,v),x,y,edge3(u,v,i),h) ->
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) ->
     or{2,#}(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
     if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> if_reach_2{5,#}(eq2(y,v),x,y,edge3(u,v,i),h) ->
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,h)
     if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> if_reach_2{5,#}(eq2(y,v),x,y,edge3(u,v,i),h) ->
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(v,y,union2(i,h),empty())
     if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> if_reach_2{5,#}(eq2(y,v),x,y,edge3(u,v,i),h) ->
     if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> union{2,#}(i,h)
     if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> eq{2,#}(y,v) ->
     eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y)
     reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h) ->
     if_reach_1{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,edge3(u,v,h))
     reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h) ->
     if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> if_reach_2{5,#}(eq2(y,v),x,y,edge3(u,v,i),h)
     reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h) ->
     if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> eq{2,#}(y,v)
     reach{4,#}(x,y,edge3(u,v,i),h) -> eq{2,#}(x,u) ->
     eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y)
     union{2,#}(edge3(x,y,i),h) -> union{2,#}(i,h) ->
     union{2,#}(edge3(x,y,i),h) -> union{2,#}(i,h)
     eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y) -> eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y)
    SCC Processor:
     #sccs: 4
     #rules: 16
     #arcs: 61/676
     DPs:
      filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
      filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
      app#(map1(x11),x12) -> map{2,#}(x11,x12)
      map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
      map{2,#}(f,cons2(x,xs)) -> app#(f,x)
      app#(filter1(x11),x12) -> filter{2,#}(x11,x12)
      filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
      filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
      app#(filter23(x11,x10,x9),x12) -> filter2{4,#}(x11,x10,x9,x12)
     TRS:
      eq2(0(),0()) -> true()
      eq2(0(),s1(x)) -> false()
      eq2(s1(x),0()) -> false()
      eq2(s1(x),s1(y)) -> eq2(x,y)
      or2(true(),y) -> true()
      or2(false(),y) -> y
      union2(empty(),h) -> h
      union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
      reach4(x,y,empty(),h) -> false()
      reach4(x,y,edge3(u,v,i),h) -> if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
      if_reach_15(true(),x,y,edge3(u,v,i),h) -> if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
      if_reach_15(false(),x,y,edge3(u,v,i),h) -> reach4(x,y,i,edge3(u,v,h))
      if_reach_25(true(),x,y,edge3(u,v,i),h) -> true()
      if_reach_25(false(),x,y,edge3(u,v,i),h) ->
      or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app(eq1(x11),x12) -> eq2(x11,x12)
      app(eq(),x12) -> eq1(x12)
      app(s(),x12) -> s1(x12)
      app(or1(x11),x12) -> or2(x11,x12)
      app(or(),x12) -> or1(x12)
      app(union1(x11),x12) -> union2(x11,x12)
      app(union(),x12) -> union1(x12)
      app(edge2(x11,x10),x12) -> edge3(x11,x10,x12)
      app(edge1(x11),x12) -> edge2(x11,x12)
      app(edge(),x12) -> edge1(x12)
      app(reach3(x11,x10,x9),x12) -> reach4(x11,x10,x9,x12)
      app(reach2(x11,x10),x12) -> reach3(x11,x10,x12)
      app(reach1(x11),x12) -> reach2(x11,x12)
      app(reach(),x12) -> reach1(x12)
      app(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_15(x11,x10,x9,x8,x12)
      app(if_reach_13(x11,x10,x9),x12) -> if_reach_14(x11,x10,x9,x12)
      app(if_reach_12(x11,x10),x12) -> if_reach_13(x11,x10,x12)
      app(if_reach_11(x11),x12) -> if_reach_12(x11,x12)
      app(if_reach_1(),x12) -> if_reach_11(x12)
      app(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_25(x11,x10,x9,x8,x12)
      app(if_reach_23(x11,x10,x9),x12) -> if_reach_24(x11,x10,x9,x12)
      app(if_reach_22(x11,x10),x12) -> if_reach_23(x11,x10,x12)
      app(if_reach_21(x11),x12) -> if_reach_22(x11,x12)
      app(if_reach_2(),x12) -> if_reach_21(x12)
      app(map1(x11),x12) -> map2(x11,x12)
      app(map(),x12) -> map1(x12)
      app(cons1(x11),x12) -> cons2(x11,x12)
      app(cons(),x12) -> cons1(x12)
      app(filter1(x11),x12) -> filter2(x11,x12)
      app(filter(),x12) -> filter1(x12)
      app(filter23(x11,x10,x9),x12) -> filter24(x11,x10,x9,x12)
      app(filter22(x11,x10),x12) -> filter23(x11,x10,x12)
      app(filter21(x11),x12) -> filter22(x11,x12)
      app(filter2(),x12) -> filter21(x12)
     Subterm Criterion Processor:
      simple projection:
       pi(map{2,#}) = 1
       pi(app#) = 1
       pi(filter{2,#}) = 1
       pi(filter2{4,#}) = 3
      problem:
       DPs:
        filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
        app#(map1(x11),x12) -> map{2,#}(x11,x12)
        app#(filter1(x11),x12) -> filter{2,#}(x11,x12)
        filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
        app#(filter23(x11,x10,x9),x12) -> filter2{4,#}(x11,x10,x9,x12)
       TRS:
        eq2(0(),0()) -> true()
        eq2(0(),s1(x)) -> false()
        eq2(s1(x),0()) -> false()
        eq2(s1(x),s1(y)) -> eq2(x,y)
        or2(true(),y) -> true()
        or2(false(),y) -> y
        union2(empty(),h) -> h
        union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
        reach4(x,y,empty(),h) -> false()
        reach4(x,y,edge3(u,v,i),h) -> if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
        if_reach_15(true(),x,y,edge3(u,v,i),h) -> if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
        if_reach_15(false(),x,y,edge3(u,v,i),h) -> reach4(x,y,i,edge3(u,v,h))
        if_reach_25(true(),x,y,edge3(u,v,i),h) -> true()
        if_reach_25(false(),x,y,edge3(u,v,i),h) ->
        or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app(eq1(x11),x12) -> eq2(x11,x12)
        app(eq(),x12) -> eq1(x12)
        app(s(),x12) -> s1(x12)
        app(or1(x11),x12) -> or2(x11,x12)
        app(or(),x12) -> or1(x12)
        app(union1(x11),x12) -> union2(x11,x12)
        app(union(),x12) -> union1(x12)
        app(edge2(x11,x10),x12) -> edge3(x11,x10,x12)
        app(edge1(x11),x12) -> edge2(x11,x12)
        app(edge(),x12) -> edge1(x12)
        app(reach3(x11,x10,x9),x12) -> reach4(x11,x10,x9,x12)
        app(reach2(x11,x10),x12) -> reach3(x11,x10,x12)
        app(reach1(x11),x12) -> reach2(x11,x12)
        app(reach(),x12) -> reach1(x12)
        app(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_15(x11,x10,x9,x8,x12)
        app(if_reach_13(x11,x10,x9),x12) -> if_reach_14(x11,x10,x9,x12)
        app(if_reach_12(x11,x10),x12) -> if_reach_13(x11,x10,x12)
        app(if_reach_11(x11),x12) -> if_reach_12(x11,x12)
        app(if_reach_1(),x12) -> if_reach_11(x12)
        app(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_25(x11,x10,x9,x8,x12)
        app(if_reach_23(x11,x10,x9),x12) -> if_reach_24(x11,x10,x9,x12)
        app(if_reach_22(x11,x10),x12) -> if_reach_23(x11,x10,x12)
        app(if_reach_21(x11),x12) -> if_reach_22(x11,x12)
        app(if_reach_2(),x12) -> if_reach_21(x12)
        app(map1(x11),x12) -> map2(x11,x12)
        app(map(),x12) -> map1(x12)
        app(cons1(x11),x12) -> cons2(x11,x12)
        app(cons(),x12) -> cons1(x12)
        app(filter1(x11),x12) -> filter2(x11,x12)
        app(filter(),x12) -> filter1(x12)
        app(filter23(x11,x10,x9),x12) -> filter24(x11,x10,x9,x12)
        app(filter22(x11,x10),x12) -> filter23(x11,x10,x12)
        app(filter21(x11),x12) -> filter22(x11,x12)
        app(filter2(),x12) -> filter21(x12)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 20/25
       
     
     DPs:
      reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h)
      if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> if_reach_2{5,#}(eq2(y,v),x,y,edge3(u,v,i),h)
      if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(v,y,union2(i,h),empty())
      if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,h)
      if_reach_1{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,edge3(u,v,h))
     TRS:
      eq2(0(),0()) -> true()
      eq2(0(),s1(x)) -> false()
      eq2(s1(x),0()) -> false()
      eq2(s1(x),s1(y)) -> eq2(x,y)
      or2(true(),y) -> true()
      or2(false(),y) -> y
      union2(empty(),h) -> h
      union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
      reach4(x,y,empty(),h) -> false()
      reach4(x,y,edge3(u,v,i),h) -> if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
      if_reach_15(true(),x,y,edge3(u,v,i),h) -> if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
      if_reach_15(false(),x,y,edge3(u,v,i),h) -> reach4(x,y,i,edge3(u,v,h))
      if_reach_25(true(),x,y,edge3(u,v,i),h) -> true()
      if_reach_25(false(),x,y,edge3(u,v,i),h) ->
      or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app(eq1(x11),x12) -> eq2(x11,x12)
      app(eq(),x12) -> eq1(x12)
      app(s(),x12) -> s1(x12)
      app(or1(x11),x12) -> or2(x11,x12)
      app(or(),x12) -> or1(x12)
      app(union1(x11),x12) -> union2(x11,x12)
      app(union(),x12) -> union1(x12)
      app(edge2(x11,x10),x12) -> edge3(x11,x10,x12)
      app(edge1(x11),x12) -> edge2(x11,x12)
      app(edge(),x12) -> edge1(x12)
      app(reach3(x11,x10,x9),x12) -> reach4(x11,x10,x9,x12)
      app(reach2(x11,x10),x12) -> reach3(x11,x10,x12)
      app(reach1(x11),x12) -> reach2(x11,x12)
      app(reach(),x12) -> reach1(x12)
      app(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_15(x11,x10,x9,x8,x12)
      app(if_reach_13(x11,x10,x9),x12) -> if_reach_14(x11,x10,x9,x12)
      app(if_reach_12(x11,x10),x12) -> if_reach_13(x11,x10,x12)
      app(if_reach_11(x11),x12) -> if_reach_12(x11,x12)
      app(if_reach_1(),x12) -> if_reach_11(x12)
      app(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_25(x11,x10,x9,x8,x12)
      app(if_reach_23(x11,x10,x9),x12) -> if_reach_24(x11,x10,x9,x12)
      app(if_reach_22(x11,x10),x12) -> if_reach_23(x11,x10,x12)
      app(if_reach_21(x11),x12) -> if_reach_22(x11,x12)
      app(if_reach_2(),x12) -> if_reach_21(x12)
      app(map1(x11),x12) -> map2(x11,x12)
      app(map(),x12) -> map1(x12)
      app(cons1(x11),x12) -> cons2(x11,x12)
      app(cons(),x12) -> cons1(x12)
      app(filter1(x11),x12) -> filter2(x11,x12)
      app(filter(),x12) -> filter1(x12)
      app(filter23(x11,x10,x9),x12) -> filter24(x11,x10,x9,x12)
      app(filter22(x11,x10),x12) -> filter23(x11,x10,x12)
      app(filter21(x11),x12) -> filter22(x11,x12)
      app(filter2(),x12) -> filter21(x12)
     Usable Rule Processor:
      DPs:
       reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h)
       if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> if_reach_2{5,#}(eq2(y,v),x,y,edge3(u,v,i),h)
       if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(v,y,union2(i,h),empty())
       if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,h)
       if_reach_1{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,edge3(u,v,h))
      TRS:
       eq2(0(),0()) -> true()
       eq2(0(),s1(x)) -> false()
       eq2(s1(x),0()) -> false()
       eq2(s1(x),s1(y)) -> eq2(x,y)
       union2(empty(),h) -> h
       union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
      Matrix Interpretation Processor: dim=1
       
       usable rules:
        union2(empty(),h) -> h
        union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
       interpretation:
        [if_reach_2{5,#}](x0, x1, x2, x3, x4) = x3 + x4,
        
        [if_reach_1{5,#}](x0, x1, x2, x3, x4) = x3 + x4,
        
        [reach{4,#}](x0, x1, x2, x3) = x2 + x3,
        
        [edge3](x0, x1, x2) = 2x0 + x2 + 2,
        
        [union2](x0, x1) = x0 + x1,
        
        [s1](x0) = 0,
        
        [eq2](x0, x1) = 0,
        
        [empty] = 0,
        
        [false] = 0,
        
        [true] = 0,
        
        [0] = 0
       orientation:
        reach{4,#}(x,y,edge3(u,v,i),h) = h + i + 2u + 2 >= h + i + 2u + 2 = if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h)
        
        if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) = h + i + 2u + 2 >= h + i + 2u + 2 = if_reach_2{5,#}(eq2(y,v),x,y,edge3(u,v,i),h)
        
        if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) = h + i + 2u + 2 >= h + i = reach{4,#}(v,y,union2(i,h),empty())
        
        if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) = h + i + 2u + 2 >= h + i = reach{4,#}(x,y,i,h)
        
        if_reach_1{5,#}(false(),x,y,edge3(u,v,i),h) = h + i + 2u + 2 >= h + i + 2u + 2 = reach{4,#}(x,y,i,edge3(u,v,h))
        
        eq2(0(),0()) = 0 >= 0 = true()
        
        eq2(0(),s1(x)) = 0 >= 0 = false()
        
        eq2(s1(x),0()) = 0 >= 0 = false()
        
        eq2(s1(x),s1(y)) = 0 >= 0 = eq2(x,y)
        
        union2(empty(),h) = h >= h = h
        
        union2(edge3(x,y,i),h) = h + i + 2x + 2 >= h + i + 2x + 2 = edge3(x,y,union2(i,h))
       problem:
        DPs:
         reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h)
         if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> if_reach_2{5,#}(eq2(y,v),x,y,edge3(u,v,i),h)
         if_reach_1{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,edge3(u,v,h))
        TRS:
         eq2(0(),0()) -> true()
         eq2(0(),s1(x)) -> false()
         eq2(s1(x),0()) -> false()
         eq2(s1(x),s1(y)) -> eq2(x,y)
         union2(empty(),h) -> h
         union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
       Restore Modifier:
        DPs:
         reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h)
         if_reach_1{5,#}(true(),x,y,edge3(u,v,i),h) -> if_reach_2{5,#}(eq2(y,v),x,y,edge3(u,v,i),h)
         if_reach_1{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,edge3(u,v,h))
        TRS:
         eq2(0(),0()) -> true()
         eq2(0(),s1(x)) -> false()
         eq2(s1(x),0()) -> false()
         eq2(s1(x),s1(y)) -> eq2(x,y)
         or2(true(),y) -> true()
         or2(false(),y) -> y
         union2(empty(),h) -> h
         union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
         reach4(x,y,empty(),h) -> false()
         reach4(x,y,edge3(u,v,i),h) -> if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
         if_reach_15(true(),x,y,edge3(u,v,i),h) -> if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
         if_reach_15(false(),x,y,edge3(u,v,i),h) -> reach4(x,y,i,edge3(u,v,h))
         if_reach_25(true(),x,y,edge3(u,v,i),h) -> true()
         if_reach_25(false(),x,y,edge3(u,v,i),h) ->
         or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
         map2(f,nil()) -> nil()
         map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
         filter2(f,nil()) -> nil()
         filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
         filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
         filter24(false(),f,x,xs) -> filter2(f,xs)
         app(eq1(x11),x12) -> eq2(x11,x12)
         app(eq(),x12) -> eq1(x12)
         app(s(),x12) -> s1(x12)
         app(or1(x11),x12) -> or2(x11,x12)
         app(or(),x12) -> or1(x12)
         app(union1(x11),x12) -> union2(x11,x12)
         app(union(),x12) -> union1(x12)
         app(edge2(x11,x10),x12) -> edge3(x11,x10,x12)
         app(edge1(x11),x12) -> edge2(x11,x12)
         app(edge(),x12) -> edge1(x12)
         app(reach3(x11,x10,x9),x12) -> reach4(x11,x10,x9,x12)
         app(reach2(x11,x10),x12) -> reach3(x11,x10,x12)
         app(reach1(x11),x12) -> reach2(x11,x12)
         app(reach(),x12) -> reach1(x12)
         app(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_15(x11,x10,x9,x8,x12)
         app(if_reach_13(x11,x10,x9),x12) -> if_reach_14(x11,x10,x9,x12)
         app(if_reach_12(x11,x10),x12) -> if_reach_13(x11,x10,x12)
         app(if_reach_11(x11),x12) -> if_reach_12(x11,x12)
         app(if_reach_1(),x12) -> if_reach_11(x12)
         app(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_25(x11,x10,x9,x8,x12)
         app(if_reach_23(x11,x10,x9),x12) -> if_reach_24(x11,x10,x9,x12)
         app(if_reach_22(x11,x10),x12) -> if_reach_23(x11,x10,x12)
         app(if_reach_21(x11),x12) -> if_reach_22(x11,x12)
         app(if_reach_2(),x12) -> if_reach_21(x12)
         app(map1(x11),x12) -> map2(x11,x12)
         app(map(),x12) -> map1(x12)
         app(cons1(x11),x12) -> cons2(x11,x12)
         app(cons(),x12) -> cons1(x12)
         app(filter1(x11),x12) -> filter2(x11,x12)
         app(filter(),x12) -> filter1(x12)
         app(filter23(x11,x10,x9),x12) -> filter24(x11,x10,x9,x12)
         app(filter22(x11,x10),x12) -> filter23(x11,x10,x12)
         app(filter21(x11),x12) -> filter22(x11,x12)
         app(filter2(),x12) -> filter21(x12)
        SCC Processor:
         #sccs: 1
         #rules: 2
         #arcs: 7/9
         DPs:
          if_reach_1{5,#}(false(),x,y,edge3(u,v,i),h) -> reach{4,#}(x,y,i,edge3(u,v,h))
          reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h)
         TRS:
          eq2(0(),0()) -> true()
          eq2(0(),s1(x)) -> false()
          eq2(s1(x),0()) -> false()
          eq2(s1(x),s1(y)) -> eq2(x,y)
          or2(true(),y) -> true()
          or2(false(),y) -> y
          union2(empty(),h) -> h
          union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
          reach4(x,y,empty(),h) -> false()
          reach4(x,y,edge3(u,v,i),h) -> if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
          if_reach_15(true(),x,y,edge3(u,v,i),h) -> if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
          if_reach_15(false(),x,y,edge3(u,v,i),h) -> reach4(x,y,i,edge3(u,v,h))
          if_reach_25(true(),x,y,edge3(u,v,i),h) -> true()
          if_reach_25(false(),x,y,edge3(u,v,i),h) ->
          or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
          map2(f,nil()) -> nil()
          map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
          filter2(f,nil()) -> nil()
          filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
          filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
          filter24(false(),f,x,xs) -> filter2(f,xs)
          app(eq1(x11),x12) -> eq2(x11,x12)
          app(eq(),x12) -> eq1(x12)
          app(s(),x12) -> s1(x12)
          app(or1(x11),x12) -> or2(x11,x12)
          app(or(),x12) -> or1(x12)
          app(union1(x11),x12) -> union2(x11,x12)
          app(union(),x12) -> union1(x12)
          app(edge2(x11,x10),x12) -> edge3(x11,x10,x12)
          app(edge1(x11),x12) -> edge2(x11,x12)
          app(edge(),x12) -> edge1(x12)
          app(reach3(x11,x10,x9),x12) -> reach4(x11,x10,x9,x12)
          app(reach2(x11,x10),x12) -> reach3(x11,x10,x12)
          app(reach1(x11),x12) -> reach2(x11,x12)
          app(reach(),x12) -> reach1(x12)
          app(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_15(x11,x10,x9,x8,x12)
          app(if_reach_13(x11,x10,x9),x12) -> if_reach_14(x11,x10,x9,x12)
          app(if_reach_12(x11,x10),x12) -> if_reach_13(x11,x10,x12)
          app(if_reach_11(x11),x12) -> if_reach_12(x11,x12)
          app(if_reach_1(),x12) -> if_reach_11(x12)
          app(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_25(x11,x10,x9,x8,x12)
          app(if_reach_23(x11,x10,x9),x12) -> if_reach_24(x11,x10,x9,x12)
          app(if_reach_22(x11,x10),x12) -> if_reach_23(x11,x10,x12)
          app(if_reach_21(x11),x12) -> if_reach_22(x11,x12)
          app(if_reach_2(),x12) -> if_reach_21(x12)
          app(map1(x11),x12) -> map2(x11,x12)
          app(map(),x12) -> map1(x12)
          app(cons1(x11),x12) -> cons2(x11,x12)
          app(cons(),x12) -> cons1(x12)
          app(filter1(x11),x12) -> filter2(x11,x12)
          app(filter(),x12) -> filter1(x12)
          app(filter23(x11,x10,x9),x12) -> filter24(x11,x10,x9,x12)
          app(filter22(x11,x10),x12) -> filter23(x11,x10,x12)
          app(filter21(x11),x12) -> filter22(x11,x12)
          app(filter2(),x12) -> filter21(x12)
         Subterm Criterion Processor:
          simple projection:
           pi(reach{4,#}) = 2
           pi(if_reach_1{5,#}) = 3
          problem:
           DPs:
            reach{4,#}(x,y,edge3(u,v,i),h) -> if_reach_1{5,#}(eq2(x,u),x,y,edge3(u,v,i),h)
           TRS:
            eq2(0(),0()) -> true()
            eq2(0(),s1(x)) -> false()
            eq2(s1(x),0()) -> false()
            eq2(s1(x),s1(y)) -> eq2(x,y)
            or2(true(),y) -> true()
            or2(false(),y) -> y
            union2(empty(),h) -> h
            union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
            reach4(x,y,empty(),h) -> false()
            reach4(x,y,edge3(u,v,i),h) -> if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
            if_reach_15(true(),x,y,edge3(u,v,i),h) -> if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
            if_reach_15(false(),x,y,edge3(u,v,i),h) -> reach4(x,y,i,edge3(u,v,h))
            if_reach_25(true(),x,y,edge3(u,v,i),h) -> true()
            if_reach_25(false(),x,y,edge3(u,v,i),h) ->
            or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
            map2(f,nil()) -> nil()
            map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
            filter2(f,nil()) -> nil()
            filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
            filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
            filter24(false(),f,x,xs) -> filter2(f,xs)
            app(eq1(x11),x12) -> eq2(x11,x12)
            app(eq(),x12) -> eq1(x12)
            app(s(),x12) -> s1(x12)
            app(or1(x11),x12) -> or2(x11,x12)
            app(or(),x12) -> or1(x12)
            app(union1(x11),x12) -> union2(x11,x12)
            app(union(),x12) -> union1(x12)
            app(edge2(x11,x10),x12) -> edge3(x11,x10,x12)
            app(edge1(x11),x12) -> edge2(x11,x12)
            app(edge(),x12) -> edge1(x12)
            app(reach3(x11,x10,x9),x12) -> reach4(x11,x10,x9,x12)
            app(reach2(x11,x10),x12) -> reach3(x11,x10,x12)
            app(reach1(x11),x12) -> reach2(x11,x12)
            app(reach(),x12) -> reach1(x12)
            app(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_15(x11,x10,x9,x8,x12)
            app(if_reach_13(x11,x10,x9),x12) -> if_reach_14(x11,x10,x9,x12)
            app(if_reach_12(x11,x10),x12) -> if_reach_13(x11,x10,x12)
            app(if_reach_11(x11),x12) -> if_reach_12(x11,x12)
            app(if_reach_1(),x12) -> if_reach_11(x12)
            app(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_25(x11,x10,x9,x8,x12)
            app(if_reach_23(x11,x10,x9),x12) -> if_reach_24(x11,x10,x9,x12)
            app(if_reach_22(x11,x10),x12) -> if_reach_23(x11,x10,x12)
            app(if_reach_21(x11),x12) -> if_reach_22(x11,x12)
            app(if_reach_2(),x12) -> if_reach_21(x12)
            app(map1(x11),x12) -> map2(x11,x12)
            app(map(),x12) -> map1(x12)
            app(cons1(x11),x12) -> cons2(x11,x12)
            app(cons(),x12) -> cons1(x12)
            app(filter1(x11),x12) -> filter2(x11,x12)
            app(filter(),x12) -> filter1(x12)
            app(filter23(x11,x10,x9),x12) -> filter24(x11,x10,x9,x12)
            app(filter22(x11,x10),x12) -> filter23(x11,x10,x12)
            app(filter21(x11),x12) -> filter22(x11,x12)
            app(filter2(),x12) -> filter21(x12)
          SCC Processor:
           #sccs: 0
           #rules: 0
           #arcs: 2/1
           
     
     DPs:
      union{2,#}(edge3(x,y,i),h) -> union{2,#}(i,h)
     TRS:
      eq2(0(),0()) -> true()
      eq2(0(),s1(x)) -> false()
      eq2(s1(x),0()) -> false()
      eq2(s1(x),s1(y)) -> eq2(x,y)
      or2(true(),y) -> true()
      or2(false(),y) -> y
      union2(empty(),h) -> h
      union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
      reach4(x,y,empty(),h) -> false()
      reach4(x,y,edge3(u,v,i),h) -> if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
      if_reach_15(true(),x,y,edge3(u,v,i),h) -> if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
      if_reach_15(false(),x,y,edge3(u,v,i),h) -> reach4(x,y,i,edge3(u,v,h))
      if_reach_25(true(),x,y,edge3(u,v,i),h) -> true()
      if_reach_25(false(),x,y,edge3(u,v,i),h) ->
      or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app(eq1(x11),x12) -> eq2(x11,x12)
      app(eq(),x12) -> eq1(x12)
      app(s(),x12) -> s1(x12)
      app(or1(x11),x12) -> or2(x11,x12)
      app(or(),x12) -> or1(x12)
      app(union1(x11),x12) -> union2(x11,x12)
      app(union(),x12) -> union1(x12)
      app(edge2(x11,x10),x12) -> edge3(x11,x10,x12)
      app(edge1(x11),x12) -> edge2(x11,x12)
      app(edge(),x12) -> edge1(x12)
      app(reach3(x11,x10,x9),x12) -> reach4(x11,x10,x9,x12)
      app(reach2(x11,x10),x12) -> reach3(x11,x10,x12)
      app(reach1(x11),x12) -> reach2(x11,x12)
      app(reach(),x12) -> reach1(x12)
      app(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_15(x11,x10,x9,x8,x12)
      app(if_reach_13(x11,x10,x9),x12) -> if_reach_14(x11,x10,x9,x12)
      app(if_reach_12(x11,x10),x12) -> if_reach_13(x11,x10,x12)
      app(if_reach_11(x11),x12) -> if_reach_12(x11,x12)
      app(if_reach_1(),x12) -> if_reach_11(x12)
      app(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_25(x11,x10,x9,x8,x12)
      app(if_reach_23(x11,x10,x9),x12) -> if_reach_24(x11,x10,x9,x12)
      app(if_reach_22(x11,x10),x12) -> if_reach_23(x11,x10,x12)
      app(if_reach_21(x11),x12) -> if_reach_22(x11,x12)
      app(if_reach_2(),x12) -> if_reach_21(x12)
      app(map1(x11),x12) -> map2(x11,x12)
      app(map(),x12) -> map1(x12)
      app(cons1(x11),x12) -> cons2(x11,x12)
      app(cons(),x12) -> cons1(x12)
      app(filter1(x11),x12) -> filter2(x11,x12)
      app(filter(),x12) -> filter1(x12)
      app(filter23(x11,x10,x9),x12) -> filter24(x11,x10,x9,x12)
      app(filter22(x11,x10),x12) -> filter23(x11,x10,x12)
      app(filter21(x11),x12) -> filter22(x11,x12)
      app(filter2(),x12) -> filter21(x12)
     Subterm Criterion Processor:
      simple projection:
       pi(union{2,#}) = 0
      problem:
       DPs:
        
       TRS:
        eq2(0(),0()) -> true()
        eq2(0(),s1(x)) -> false()
        eq2(s1(x),0()) -> false()
        eq2(s1(x),s1(y)) -> eq2(x,y)
        or2(true(),y) -> true()
        or2(false(),y) -> y
        union2(empty(),h) -> h
        union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
        reach4(x,y,empty(),h) -> false()
        reach4(x,y,edge3(u,v,i),h) -> if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
        if_reach_15(true(),x,y,edge3(u,v,i),h) -> if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
        if_reach_15(false(),x,y,edge3(u,v,i),h) -> reach4(x,y,i,edge3(u,v,h))
        if_reach_25(true(),x,y,edge3(u,v,i),h) -> true()
        if_reach_25(false(),x,y,edge3(u,v,i),h) ->
        or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app(eq1(x11),x12) -> eq2(x11,x12)
        app(eq(),x12) -> eq1(x12)
        app(s(),x12) -> s1(x12)
        app(or1(x11),x12) -> or2(x11,x12)
        app(or(),x12) -> or1(x12)
        app(union1(x11),x12) -> union2(x11,x12)
        app(union(),x12) -> union1(x12)
        app(edge2(x11,x10),x12) -> edge3(x11,x10,x12)
        app(edge1(x11),x12) -> edge2(x11,x12)
        app(edge(),x12) -> edge1(x12)
        app(reach3(x11,x10,x9),x12) -> reach4(x11,x10,x9,x12)
        app(reach2(x11,x10),x12) -> reach3(x11,x10,x12)
        app(reach1(x11),x12) -> reach2(x11,x12)
        app(reach(),x12) -> reach1(x12)
        app(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_15(x11,x10,x9,x8,x12)
        app(if_reach_13(x11,x10,x9),x12) -> if_reach_14(x11,x10,x9,x12)
        app(if_reach_12(x11,x10),x12) -> if_reach_13(x11,x10,x12)
        app(if_reach_11(x11),x12) -> if_reach_12(x11,x12)
        app(if_reach_1(),x12) -> if_reach_11(x12)
        app(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_25(x11,x10,x9,x8,x12)
        app(if_reach_23(x11,x10,x9),x12) -> if_reach_24(x11,x10,x9,x12)
        app(if_reach_22(x11,x10),x12) -> if_reach_23(x11,x10,x12)
        app(if_reach_21(x11),x12) -> if_reach_22(x11,x12)
        app(if_reach_2(),x12) -> if_reach_21(x12)
        app(map1(x11),x12) -> map2(x11,x12)
        app(map(),x12) -> map1(x12)
        app(cons1(x11),x12) -> cons2(x11,x12)
        app(cons(),x12) -> cons1(x12)
        app(filter1(x11),x12) -> filter2(x11,x12)
        app(filter(),x12) -> filter1(x12)
        app(filter23(x11,x10,x9),x12) -> filter24(x11,x10,x9,x12)
        app(filter22(x11,x10),x12) -> filter23(x11,x10,x12)
        app(filter21(x11),x12) -> filter22(x11,x12)
        app(filter2(),x12) -> filter21(x12)
      Qed
     
     DPs:
      eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y)
     TRS:
      eq2(0(),0()) -> true()
      eq2(0(),s1(x)) -> false()
      eq2(s1(x),0()) -> false()
      eq2(s1(x),s1(y)) -> eq2(x,y)
      or2(true(),y) -> true()
      or2(false(),y) -> y
      union2(empty(),h) -> h
      union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
      reach4(x,y,empty(),h) -> false()
      reach4(x,y,edge3(u,v,i),h) -> if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
      if_reach_15(true(),x,y,edge3(u,v,i),h) -> if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
      if_reach_15(false(),x,y,edge3(u,v,i),h) -> reach4(x,y,i,edge3(u,v,h))
      if_reach_25(true(),x,y,edge3(u,v,i),h) -> true()
      if_reach_25(false(),x,y,edge3(u,v,i),h) ->
      or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app(eq1(x11),x12) -> eq2(x11,x12)
      app(eq(),x12) -> eq1(x12)
      app(s(),x12) -> s1(x12)
      app(or1(x11),x12) -> or2(x11,x12)
      app(or(),x12) -> or1(x12)
      app(union1(x11),x12) -> union2(x11,x12)
      app(union(),x12) -> union1(x12)
      app(edge2(x11,x10),x12) -> edge3(x11,x10,x12)
      app(edge1(x11),x12) -> edge2(x11,x12)
      app(edge(),x12) -> edge1(x12)
      app(reach3(x11,x10,x9),x12) -> reach4(x11,x10,x9,x12)
      app(reach2(x11,x10),x12) -> reach3(x11,x10,x12)
      app(reach1(x11),x12) -> reach2(x11,x12)
      app(reach(),x12) -> reach1(x12)
      app(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_15(x11,x10,x9,x8,x12)
      app(if_reach_13(x11,x10,x9),x12) -> if_reach_14(x11,x10,x9,x12)
      app(if_reach_12(x11,x10),x12) -> if_reach_13(x11,x10,x12)
      app(if_reach_11(x11),x12) -> if_reach_12(x11,x12)
      app(if_reach_1(),x12) -> if_reach_11(x12)
      app(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_25(x11,x10,x9,x8,x12)
      app(if_reach_23(x11,x10,x9),x12) -> if_reach_24(x11,x10,x9,x12)
      app(if_reach_22(x11,x10),x12) -> if_reach_23(x11,x10,x12)
      app(if_reach_21(x11),x12) -> if_reach_22(x11,x12)
      app(if_reach_2(),x12) -> if_reach_21(x12)
      app(map1(x11),x12) -> map2(x11,x12)
      app(map(),x12) -> map1(x12)
      app(cons1(x11),x12) -> cons2(x11,x12)
      app(cons(),x12) -> cons1(x12)
      app(filter1(x11),x12) -> filter2(x11,x12)
      app(filter(),x12) -> filter1(x12)
      app(filter23(x11,x10,x9),x12) -> filter24(x11,x10,x9,x12)
      app(filter22(x11,x10),x12) -> filter23(x11,x10,x12)
      app(filter21(x11),x12) -> filter22(x11,x12)
      app(filter2(),x12) -> filter21(x12)
     Subterm Criterion Processor:
      simple projection:
       pi(eq{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        eq2(0(),0()) -> true()
        eq2(0(),s1(x)) -> false()
        eq2(s1(x),0()) -> false()
        eq2(s1(x),s1(y)) -> eq2(x,y)
        or2(true(),y) -> true()
        or2(false(),y) -> y
        union2(empty(),h) -> h
        union2(edge3(x,y,i),h) -> edge3(x,y,union2(i,h))
        reach4(x,y,empty(),h) -> false()
        reach4(x,y,edge3(u,v,i),h) -> if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
        if_reach_15(true(),x,y,edge3(u,v,i),h) -> if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
        if_reach_15(false(),x,y,edge3(u,v,i),h) -> reach4(x,y,i,edge3(u,v,h))
        if_reach_25(true(),x,y,edge3(u,v,i),h) -> true()
        if_reach_25(false(),x,y,edge3(u,v,i),h) ->
        or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app(eq1(x11),x12) -> eq2(x11,x12)
        app(eq(),x12) -> eq1(x12)
        app(s(),x12) -> s1(x12)
        app(or1(x11),x12) -> or2(x11,x12)
        app(or(),x12) -> or1(x12)
        app(union1(x11),x12) -> union2(x11,x12)
        app(union(),x12) -> union1(x12)
        app(edge2(x11,x10),x12) -> edge3(x11,x10,x12)
        app(edge1(x11),x12) -> edge2(x11,x12)
        app(edge(),x12) -> edge1(x12)
        app(reach3(x11,x10,x9),x12) -> reach4(x11,x10,x9,x12)
        app(reach2(x11,x10),x12) -> reach3(x11,x10,x12)
        app(reach1(x11),x12) -> reach2(x11,x12)
        app(reach(),x12) -> reach1(x12)
        app(if_reach_14(x11,x10,x9,x8),x12) -> if_reach_15(x11,x10,x9,x8,x12)
        app(if_reach_13(x11,x10,x9),x12) -> if_reach_14(x11,x10,x9,x12)
        app(if_reach_12(x11,x10),x12) -> if_reach_13(x11,x10,x12)
        app(if_reach_11(x11),x12) -> if_reach_12(x11,x12)
        app(if_reach_1(),x12) -> if_reach_11(x12)
        app(if_reach_24(x11,x10,x9,x8),x12) -> if_reach_25(x11,x10,x9,x8,x12)
        app(if_reach_23(x11,x10,x9),x12) -> if_reach_24(x11,x10,x9,x12)
        app(if_reach_22(x11,x10),x12) -> if_reach_23(x11,x10,x12)
        app(if_reach_21(x11),x12) -> if_reach_22(x11,x12)
        app(if_reach_2(),x12) -> if_reach_21(x12)
        app(map1(x11),x12) -> map2(x11,x12)
        app(map(),x12) -> map1(x12)
        app(cons1(x11),x12) -> cons2(x11,x12)
        app(cons(),x12) -> cons1(x12)
        app(filter1(x11),x12) -> filter2(x11,x12)
        app(filter(),x12) -> filter1(x12)
        app(filter23(x11,x10,x9),x12) -> filter24(x11,x10,x9,x12)
        app(filter22(x11,x10),x12) -> filter23(x11,x10,x12)
        app(filter21(x11),x12) -> filter22(x11,x12)
        app(filter2(),x12) -> filter21(x12)
      Qed