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)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [if_reach_2{5,#}](x0, x1, x2, x3, x4) = x1 + 2x3 + 2x4,
       
       [if_reach_1{5,#}](x0, x1, x2, x3, x4) = x1 + 2x3 + 2x4,
       
       [reach{4,#}](x0, x1, x2, x3) = x0 + 2x2 + 2x3,
       
       [filter21](x0) = 3x0 + 3,
       
       [filter22](x0, x1) = 4x0 + 5x1 + 3,
       
       [filter24](x0, x1, x2, x3) = 4,
       
       [filter23](x0, x1, x2) = x0 + 4x2 + 4,
       
       [filter2](x0, x1) = 4,
       
       [filter1](x0) = 3,
       
       [cons2](x0, x1) = 2,
       
       [cons1](x0) = 4x0 + 2,
       
       [map2](x0, x1) = 4x1,
       
       [map1](x0) = 0,
       
       [if_reach_21](x0) = 4x0 + 1,
       
       [if_reach_22](x0, x1) = x0 + 5x1,
       
       [if_reach_23](x0, x1, x2) = 3x0 + 5x1 + 2x2,
       
       [if_reach_25](x0, x1, x2, x3, x4) = 2x3 + 2x4,
       
       [if_reach_24](x0, x1, x2, x3) = x0 + 4x1 + 6x2 + x3,
       
       [if_reach_11](x0) = 2x0 + 3,
       
       [if_reach_12](x0, x1) = 3x0 + 3x1 + 4,
       
       [if_reach_13](x0, x1, x2) = 2x1 + x2 + 1,
       
       [if_reach_15](x0, x1, x2, x3, x4) = 2x3 + 2x4 + 1,
       
       [if_reach_14](x0, x1, x2, x3) = x1 + 2x2 + 5x3 + 2,
       
       [reach1](x0) = x0 + 1,
       
       [reach2](x0, x1) = 3x0 + 2,
       
       [reach4](x0, x1, x2, x3) = 2x2 + 2x3 + 1,
       
       [reach3](x0, x1, x2) = x2 + 2,
       
       [edge1](x0) = x0 + 2,
       
       [edge3](x0, x1, x2) = x0 + 2x1 + x2 + 4,
       
       [edge2](x0, x1) = x0 + 2x1 + 3,
       
       [union2](x0, x1) = x0 + x1,
       
       [union1](x0) = 2x0,
       
       [or2](x0, x1) = x1 + 7,
       
       [or1](x0) = x0 + 3,
       
       [s1](x0) = 0,
       
       [eq2](x0, x1) = 0,
       
       [eq1](x0) = 3,
       
       [filter2] = 1,
       
       [filter] = 1,
       
       [cons] = 4,
       
       [nil] = 4,
       
       [map] = 0,
       
       [if_reach_2] = 4,
       
       [if_reach_1] = 1,
       
       [reach] = 2,
       
       [edge] = 7,
       
       [empty] = 0,
       
       [union] = 3,
       
       [or] = 6,
       
       [false] = 0,
       
       [s] = 0,
       
       [true] = 0,
       
       [app](x0, x1) = 3x0 + 5x1,
       
       [0] = 0,
       
       [eq] = 1
      orientation:
       reach{4,#}(x,y,edge3(u,v,i),h) = 2h + 2i + 2u + 4v + x + 8 >= 2h + 2i + 2u + 4v + x + 8 = 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) = 2h + 2i + 2u + 4v + x + 8 >= 2h + 2i + 2u + 4v + x + 8 = 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) = 2h + 2i + 2u + 4v + x + 8 >= 2h + 2i + v = reach{4,#}(v,y,union2(i,h),empty())
       
       if_reach_2{5,#}(false(),x,y,edge3(u,v,i),h) = 2h + 2i + 2u + 4v + x + 8 >= 2h + 2i + x = reach{4,#}(x,y,i,h)
       
       if_reach_1{5,#}(false(),x,y,edge3(u,v,i),h) = 2h + 2i + 2u + 4v + x + 8 >= 2h + 2i + 2u + 4v + x + 8 = 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)
       
       or2(true(),y) = y + 7 >= 0 = true()
       
       or2(false(),y) = y + 7 >= y = y
       
       union2(empty(),h) = h >= h = h
       
       union2(edge3(x,y,i),h) = h + i + x + 2y + 4 >= h + i + x + 2y + 4 = edge3(x,y,union2(i,h))
       
       reach4(x,y,empty(),h) = 2h + 1 >= 0 = false()
       
       reach4(x,y,edge3(u,v,i),h) = 2h + 2i + 2u + 4v + 9 >= 2h + 2i + 2u + 4v + 9 = if_reach_15(eq2(x,u),x,y,edge3(u,v,i),h)
       
       if_reach_15(true(),x,y,edge3(u,v,i),h) = 2h + 2i + 2u + 4v + 9 >= 2h + 2i + 2u + 4v + 8 = if_reach_25(eq2(y,v),x,y,edge3(u,v,i),h)
       
       if_reach_15(false(),x,y,edge3(u,v,i),h) = 2h + 2i + 2u + 4v + 9 >= 2h + 2i + 2u + 4v + 9 = reach4(x,y,i,edge3(u,v,h))
       
       if_reach_25(true(),x,y,edge3(u,v,i),h) = 2h + 2i + 2u + 4v + 8 >= 0 = true()
       
       if_reach_25(false(),x,y,edge3(u,v,i),h) = 2h + 2i + 2u + 4v + 8 >= 2h + 2i + 8 = or2(reach4(x,y,i,h),reach4(v,y,union2(i,h),empty()))
       
       map2(f,nil()) = 16 >= 4 = nil()
       
       map2(f,cons2(x,xs)) = 8 >= 2 = cons2(app(f,x),map2(f,xs))
       
       filter2(f,nil()) = 4 >= 4 = nil()
       
       filter2(f,cons2(x,xs)) = 4 >= 4 = filter24(app(f,x),f,x,xs)
       
       filter24(true(),f,x,xs) = 4 >= 2 = cons2(x,filter2(f,xs))
       
       filter24(false(),f,x,xs) = 4 >= 4 = filter2(f,xs)
       
       app(eq1(x11),x12) = 5x12 + 9 >= 0 = eq2(x11,x12)
       
       app(eq(),x12) = 5x12 + 3 >= 3 = eq1(x12)
       
       app(s(),x12) = 5x12 >= 0 = s1(x12)
       
       app(or1(x11),x12) = 3x11 + 5x12 + 9 >= x12 + 7 = or2(x11,x12)
       
       app(or(),x12) = 5x12 + 18 >= x12 + 3 = or1(x12)
       
       app(union1(x11),x12) = 6x11 + 5x12 >= x11 + x12 = union2(x11,x12)
       
       app(union(),x12) = 5x12 + 9 >= 2x12 = union1(x12)
       
       app(edge2(x11,x10),x12) = 6x10 + 3x11 + 5x12 + 9 >= 2x10 + x11 + x12 + 4 = edge3(x11,x10,x12)
       
       app(edge1(x11),x12) = 3x11 + 5x12 + 6 >= x11 + 2x12 + 3 = edge2(x11,x12)
       
       app(edge(),x12) = 5x12 + 21 >= x12 + 2 = edge1(x12)
       
       app(reach3(x11,x10,x9),x12) = 5x12 + 3x9 + 6 >= 2x12 + 2x9 + 1 = reach4(x11,x10,x9,x12)
       
       app(reach2(x11,x10),x12) = 9x11 + 5x12 + 6 >= x12 + 2 = reach3(x11,x10,x12)
       
       app(reach1(x11),x12) = 3x11 + 5x12 + 3 >= 3x11 + 2 = reach2(x11,x12)
       
       app(reach(),x12) = 5x12 + 6 >= x12 + 1 = reach1(x12)
       
       app(if_reach_14(x11,x10,x9,x8),x12) = 3x10 + 5x12 + 15x8 + 6x9 + 6 >= 2x12 + 2x8 + 1 = if_reach_15(x11,x10,x9,x8,x12)
       
       app(if_reach_13(x11,x10,x9),x12) = 6x10 + 5x12 + 3x9 + 3 >= x10 + 5x12 + 2x9 + 2 = if_reach_14(x11,x10,x9,x12)
       
       app(if_reach_12(x11,x10),x12) = 9x10 + 9x11 + 5x12 + 12 >= 2x10 + x12 + 1 = if_reach_13(x11,x10,x12)
       
       app(if_reach_11(x11),x12) = 6x11 + 5x12 + 9 >= 3x11 + 3x12 + 4 = if_reach_12(x11,x12)
       
       app(if_reach_1(),x12) = 5x12 + 3 >= 2x12 + 3 = if_reach_11(x12)
       
       app(if_reach_24(x11,x10,x9,x8),x12) = 12x10 + 3x11 + 5x12 + 3x8 + 18x9 >= 2x12 + 2x8 = if_reach_25(x11,x10,x9,x8,x12)
       
       app(if_reach_23(x11,x10,x9),x12) = 15x10 + 9x11 + 5x12 + 6x9 >= 4x10 + x11 + x12 + 6x9 = if_reach_24(x11,x10,x9,x12)
       
       app(if_reach_22(x11,x10),x12) = 15x10 + 3x11 + 5x12 >= 5x10 + 3x11 + 2x12 = if_reach_23(x11,x10,x12)
       
       app(if_reach_21(x11),x12) = 12x11 + 5x12 + 3 >= x11 + 5x12 = if_reach_22(x11,x12)
       
       app(if_reach_2(),x12) = 5x12 + 12 >= 4x12 + 1 = if_reach_21(x12)
       
       app(map1(x11),x12) = 5x12 >= 4x12 = map2(x11,x12)
       
       app(map(),x12) = 5x12 >= 0 = map1(x12)
       
       app(cons1(x11),x12) = 12x11 + 5x12 + 6 >= 2 = cons2(x11,x12)
       
       app(cons(),x12) = 5x12 + 12 >= 4x12 + 2 = cons1(x12)
       
       app(filter1(x11),x12) = 5x12 + 9 >= 4 = filter2(x11,x12)
       
       app(filter(),x12) = 5x12 + 3 >= 3 = filter1(x12)
       
       app(filter23(x11,x10,x9),x12) = 3x11 + 5x12 + 12x9 + 12 >= 4 = filter24(x11,x10,x9,x12)
       
       app(filter22(x11,x10),x12) = 15x10 + 12x11 + 5x12 + 9 >= x11 + 4x12 + 4 = filter23(x11,x10,x12)
       
       app(filter21(x11),x12) = 9x11 + 5x12 + 9 >= 4x11 + 5x12 + 3 = filter22(x11,x12)
       
       app(filter2(),x12) = 5x12 + 3 >= 3x12 + 3 = filter21(x12)
      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)
        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