EQUATIONS: 
app(nil(),y) = y
app(cons(x,y),z) = cons(x,app(y,z))
app(app(x,y),z) = app(x,app(y,z))
reviter(nil(),y) = y
reviter(cons(x,y),z) = reviter(y,cons(x,z))
rev(nil()) = nil()
rev(cons(x,y)) = app(rev(y),cons(x,nil()))
app(rev(x),y) = reviter(x,y)
rev(x) = reviter(x,nil())

COMPLETE TRS:
RULES:
app(nil(),y) -> y
app(cons(x,y),z) -> cons(x,app(y,z))
app(app(x,y),z) -> app(x,app(y,z))
reviter(nil(),y) -> y
reviter(cons(x,y),z) -> reviter(y,cons(x,z))
rev(x) -> reviter(x,nil())
app(reviter(x,y),z) -> reviter(x,app(y,z))

SUCCESS
MaxTRS: 14 
Search time: 15.11 seconds