twee-0.1: tests/length3.p

cnf(a, axiom, length('++'(Xs, '++'(Ys, '++'(Zs, Ws)))) = length('++'(Ws, '++'(Xs, '++'(Ys, Zs))))).
cnf(a, axiom, length('++'(Xs, '++'(Xs, '++'(Ys, Zs)))) = length('++'(Xs, '++'(Ys, '++'(Zs, Xs))))).