MAYBE
Time: 0.764

Problem:
 Equations:
  plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
  plusAC(x4,x5) -> plusAC(x5,x4)
  appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
  appAC(x4,x5) -> appAC(x5,x4)
  plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
  plusAC(x5,x4) -> plusAC(x4,x5)
  appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
  appAC(x5,x4) -> appAC(x4,x5)
 TRS:
  if(true(),x,y) -> x
  if(false(),x,y) -> y
  eq(0(),0()) -> true()
  eq(0(),s(x)) -> false()
  eq(s(x),s(y)) -> eq(x,y)
  plusAC(empty(),x) -> x
  appAC(x,empty()) -> empty()
  appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
  appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
  appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
  appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())

Proof:
 DP Processor:
  Equations#:
   plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6))
   plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4)
   app{AC,#}(appAC(x4,x5),x6) -> app{AC,#}(x4,appAC(x5,x6))
   app{AC,#}(x4,x5) -> app{AC,#}(x5,x4)
   plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6)
   plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5)
   app{AC,#}(x4,appAC(x5,x6)) -> app{AC,#}(appAC(x4,x5),x6)
   app{AC,#}(x5,x4) -> app{AC,#}(x4,x5)
  DPs:
   eq#(s(x),s(y)) -> eq#(x,y)
   app{AC,#}(x,plusAC(y,z)) -> app{AC,#}(x,z)
   app{AC,#}(x,plusAC(y,z)) -> app{AC,#}(x,y)
   app{AC,#}(x,plusAC(y,z)) -> plus{AC,#}(appAC(x,y),appAC(x,z))
   app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(x,z)
   app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(x,y)
   app{AC,#}(x,appAC(plusAC(y,z),t)) -> plus{AC,#}(appAC(x,y),appAC(x,z))
   app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(plusAC(appAC(x,y),appAC(x,z)),t)
   app{AC,#}(singl(x),singl(y)) -> eq#(x,y)
   app{AC,#}(singl(x),singl(y)) -> if#(eq(x,y),singl(x),empty())
   plus{AC,#}(x7,plusAC(empty(),x)) -> plus{AC,#}(x7,x)
   app{AC,#}(x8,appAC(x,empty())) -> app{AC,#}(x8,empty())
   app{AC,#}(x9,appAC(x,appAC(empty(),z))) -> app{AC,#}(x9,appAC(empty(),z))
   app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x,z)
   app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x,y)
   app{AC,#}(x10,appAC(x,plusAC(y,z))) -> plus{AC,#}(appAC(x,y),appAC(x,z))
   app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x10,plusAC(appAC(x,y),appAC(x,z)))
   app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(x,z)
   app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(x,y)
   app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> plus{AC,#}(appAC(x,y),appAC(x,z))
   app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(plusAC(appAC(x,y),appAC(x,z)),t)
   app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) ->
   app{AC,#}(x11,appAC(plusAC(appAC(x,y),appAC(x,z)),t))
   app{AC,#}(x12,appAC(singl(x),singl(y))) -> eq#(x,y)
   app{AC,#}(x12,appAC(singl(x),singl(y))) -> if#(eq(x,y),singl(x),empty())
   app{AC,#}(x12,appAC(singl(x),singl(y))) -> app{AC,#}(x12,if(eq(x,y),singl(x),empty()))
  Equations:
   plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
   plusAC(x4,x5) -> plusAC(x5,x4)
   appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
   appAC(x4,x5) -> appAC(x5,x4)
   plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
   plusAC(x5,x4) -> plusAC(x4,x5)
   appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
   appAC(x5,x4) -> appAC(x4,x5)
  TRS:
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   eq(0(),0()) -> true()
   eq(0(),s(x)) -> false()
   eq(s(x),s(y)) -> eq(x,y)
   plusAC(empty(),x) -> x
   appAC(x,empty()) -> empty()
   appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
   appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
   appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
   appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())
  S:
   plus{AC,#}(plusAC(x13,x14),x15) -> plus{AC,#}(x13,x14)
   plus{AC,#}(x13,plusAC(x14,x15)) -> plus{AC,#}(x14,x15)
   app{AC,#}(appAC(x13,x14),x15) -> app{AC,#}(x13,x14)
   app{AC,#}(x13,appAC(x14,x15)) -> app{AC,#}(x14,x15)
  AC-EDG Processor:
   Equations#:
    plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6))
    plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4)
    app{AC,#}(appAC(x4,x5),x6) -> app{AC,#}(x4,appAC(x5,x6))
    app{AC,#}(x4,x5) -> app{AC,#}(x5,x4)
    plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6)
    plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5)
    app{AC,#}(x4,appAC(x5,x6)) -> app{AC,#}(appAC(x4,x5),x6)
    app{AC,#}(x5,x4) -> app{AC,#}(x4,x5)
   DPs:
    eq#(s(x),s(y)) -> eq#(x,y)
    app{AC,#}(x,plusAC(y,z)) -> app{AC,#}(x,z)
    app{AC,#}(x,plusAC(y,z)) -> app{AC,#}(x,y)
    app{AC,#}(x,plusAC(y,z)) -> plus{AC,#}(appAC(x,y),appAC(x,z))
    app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(x,z)
    app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(x,y)
    app{AC,#}(x,appAC(plusAC(y,z),t)) -> plus{AC,#}(appAC(x,y),appAC(x,z))
    app{AC,#}(x,appAC(plusAC(y,z),t)) -> app{AC,#}(plusAC(appAC(x,y),appAC(x,z)),t)
    app{AC,#}(singl(x),singl(y)) -> eq#(x,y)
    app{AC,#}(singl(x),singl(y)) -> if#(eq(x,y),singl(x),empty())
    plus{AC,#}(x7,plusAC(empty(),x)) -> plus{AC,#}(x7,x)
    app{AC,#}(x8,appAC(x,empty())) -> app{AC,#}(x8,empty())
    app{AC,#}(x9,appAC(x,appAC(empty(),z))) -> app{AC,#}(x9,appAC(empty(),z))
    app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x,z)
    app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x,y)
    app{AC,#}(x10,appAC(x,plusAC(y,z))) -> plus{AC,#}(appAC(x,y),appAC(x,z))
    app{AC,#}(x10,appAC(x,plusAC(y,z))) -> app{AC,#}(x10,plusAC(appAC(x,y),appAC(x,z)))
    app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(x,z)
    app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(x,y)
    app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> plus{AC,#}(appAC(x,y),appAC(x,z))
    app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) -> app{AC,#}(plusAC(appAC(x,y),appAC(x,z)),t)
    app{AC,#}(x11,appAC(x,appAC(plusAC(y,z),t))) ->
    app{AC,#}(x11,appAC(plusAC(appAC(x,y),appAC(x,z)),t))
    app{AC,#}(x12,appAC(singl(x),singl(y))) -> eq#(x,y)
    app{AC,#}(x12,appAC(singl(x),singl(y))) -> if#(eq(x,y),singl(x),empty())
    app{AC,#}(x12,appAC(singl(x),singl(y))) -> app{AC,#}(x12,if(eq(x,y),singl(x),empty()))
   Equations:
    plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
    plusAC(x4,x5) -> plusAC(x5,x4)
    appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
    appAC(x4,x5) -> appAC(x5,x4)
    plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
    plusAC(x5,x4) -> plusAC(x4,x5)
    appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
    appAC(x5,x4) -> appAC(x4,x5)
   TRS:
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    eq(0(),0()) -> true()
    eq(0(),s(x)) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    plusAC(empty(),x) -> x
    appAC(x,empty()) -> empty()
    appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
    appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
    appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
    appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())
   S:
    plus{AC,#}(plusAC(x13,x14),x15) -> plus{AC,#}(x13,x14)
    plus{AC,#}(x13,plusAC(x14,x15)) -> plus{AC,#}(x14,x15)
    app{AC,#}(appAC(x13,x14),x15) -> app{AC,#}(x13,x14)
    app{AC,#}(x13,appAC(x14,x15)) -> app{AC,#}(x14,x15)
   Open