MAYBE
Time: 0.014

Problem:
 Equations:
  
 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:
 Open