1;
(l(x 2, a(v(x 1), v(x 2))), x 1, v(x 2));
subs(l(x 2, a(v(x 1), v(x 2))), x 1, v(x 2));
2;
(a(v(x 1), l(x 2, a(v(x 1), v(x 2)))), x 1, v(x 2));
subs(a(v(x 1), l(x 2, a(v(x 1), v(x 2)))), x 1, v(x 2));
3;
(a(v(x 1), l(x 2, a(v(x 1), v(x 2)))), x 1, v(x 3));
subs(a(v(x 1), l(x 2, a(v(x 1), v(x 2)))), x 1, v(x 3));
4;
(v(x 2), x 2, l(x 1, v(x 1)));
subs(v(x 2), x 2, l(x 1, v(x 1)));
5;
(v(x 1), x 1, v(x 3));
subs(v(x 1), x 1, v(x 3));
6;
(a(v(x 1), v(x 1)), x 1, l(x 1, v(x 1)));
subs(a(v(x 1), v(x 1)), x 1, l(x 1, v(x 1)));
7;
(l(x 2, l(x 3, a(v(x 2), a(a(v(x 1), v(x 2)), v(x 3))))), x 1, l(x 4, l(x 5, a(v(x 4), v(x 5)))));
subs(l(x 2, l(x 3, a(v(x 2), a(a(v(x 1), v(x 2)), v(x 3))))), x 1, l(x 4, l(x 5, a(v(x 4), v(x 5)))));