let R be the TRS under consideration

f(_1,f(a,_2)) -> f(a,f(f(f(a,a),_2),_1)) is in elim_R(R)
let r0 be the right-hand side of this rule
p0 = 1.0 is a position in r0
we have r0|p0 = f(f(a,a),_2)
f(_3,f(a,_4)) -> f(a,f(f(f(a,a),_4),_3)) is in R
let l'0 be the left-hand side of this rule
theta0 = {_2/f(a,_4), _3/f(a,a)} is a mgu of r0|p0 and l'0

==> f(_1,f(a,f(a,_2))) -> f(a,f(f(a,f(f(f(a,a),_2),f(a,a))),_1)) is in EU_R^1
let r1 be the right-hand side of this rule
p1 = 1.0.1 is a position in r1
we have r1|p1 = f(f(f(a,a),_2),f(a,a))
f(_3,f(a,_4)) -> f(a,f(f(f(a,a),_4),_3)) is in R
let l'1 be the left-hand side of this rule
theta1 = {_3/f(f(a,a),_2), _4/a} is a mgu of r1|p1 and l'1

==> f(_1,f(a,f(a,_2))) -> f(a,f(f(a,f(a,f(f(f(a,a),a),f(f(a,a),_2)))),_1)) is in EU_R^2
let r2 be the right-hand side of this rule
p2 = 1.1 is a position in r2
we have r2|p2 = _1
f(_3,f(a,_4)) -> f(a,f(f(f(a,a),_4),_3)) is in R
let l'2 be the left-hand side of this rule
theta2 = {_1/f(_3,f(a,_4))} is a mgu of r2|p2 and l'2

==> f(f(_1,f(a,_2)),f(a,f(a,_3))) -> f(a,f(f(a,f(a,f(f(f(a,a),a),f(f(a,a),_3)))),f(a,f(f(f(a,a),_2),_1)))) is in EU_R^3
let r3 be the right-hand side of this rule
p3 = 1.1.1 is a position in r3
we have r3|p3 = f(f(f(a,a),_2),_1)
f(_4,f(a,_5)) -> f(a,f(f(f(a,a),_5),_4)) is in R
let l'3 be the left-hand side of this rule
theta3 = {_1/f(a,_5), _4/f(f(a,a),_2)} is a mgu of r3|p3 and l'3

==> f(f(f(a,_1),f(a,_2)),f(a,f(a,_3))) -> f(a,f(f(a,f(a,f(f(f(a,a),a),f(f(a,a),_3)))),f(a,f(a,f(f(f(a,a),_1),f(f(a,a),_2)))))) is in EU_R^4
let r4 be the right-hand side of this rule
p4 = 1 is a position in r4
we have r4|p4 = f(f(a,f(a,f(f(f(a,a),a),f(f(a,a),_3)))),f(a,f(a,f(f(f(a,a),_1),f(f(a,a),_2)))))
f(_4,f(a,_5)) -> f(a,f(f(f(a,a),_5),_4)) is in R
let l'4 be the left-hand side of this rule
theta4 = {_4/f(a,f(a,f(f(f(a,a),a),f(f(a,a),_3)))), _5/f(a,f(f(f(a,a),_1),f(f(a,a),_2)))} is a mgu of r4|p4 and l'4

==> f(f(f(a,_1),f(a,_2)),f(a,f(a,_3))) -> f(a,f(a,f(f(f(a,a),f(a,f(f(f(a,a),_1),f(f(a,a),_2)))),f(a,f(a,f(f(f(a,a),a),f(f(a,a),_3))))))) is in EU_R^5
let l be the left-hand side and r be the right-hand side of this rule
let p = 1.1
let theta = {}
let theta' = {_1/a, _2/f(f(f(a,a),_1),f(f(a,a),_2)), _3/f(f(f(a,a),a),f(f(a,a),_3))}
we have r|p = f(f(f(a,a),f(a,f(f(f(a,a),_1),f(f(a,a),_2)))),f(a,f(a,f(f(f(a,a),a),f(f(a,a),_3))))) and
theta'(theta(l)) = theta(r|p)
so, theta(l) = f(f(f(a,_1),f(a,_2)),f(a,f(a,_3))) is non-terminating w.r.t. R

Termination disproved by the forward process
proof stopped at iteration i=5, depth k=7
20 rule(s) generated