twee-2.5: tests/union.p

cnf(elem_union_1, axiom, notelem(X, A) | ~notelem(X, union(A, B))).
cnf(elem_union_2, axiom, notelem(X, B) | ~notelem(X, union(A, B))).
cnf(elem_union_3, axiom, notelem(X, union(A, B)) | ~notelem(X, A) | ~notelem(X, B)).
cnf(elem_equals, axiom, A=B | ~notelem(sK1_elem_equals_X(A, B), A) | ~notelem(sK1_elem_equals_X(A, B), B)).
cnf(union_commutative, negated_conjecture, union(a, b)!=union(b, a)).

cnf(elem_equals_1, axiom, choice(A,B) = c1 => notelem(sK1_elem_equals_X(A, B), A)).
cnf(elem_equals_2, axiom, choice(A,B) = c2 => notelem(sK1_elem_equals_X(A, B), B)).
cnf(elem_equals_3, axiom, choice(A,B) = c3 => A=B).