twee-0.1: tests/length2.p

cnf(a, axiom, '++'(Xs, '++'(Ys, Zs)) = '++'('++'(Xs, Ys), Zs)).
cnf(a, axiom, length('++'(Xs, Ys)) = length('++'(Ys, Xs))).
cnf(a, axiom, length('++'('++'(c,a),b)) != length('++'(a,'++'(b,c)))).