twee-2.5: tests/union2.p

cnf(ifeq_axiom, axiom, ifeq4(A, A, B, C)=B).
cnf(ifeq_axiom, axiom, ifeq3(A, A, B, C)=B).
cnf(ifeq_axiom, axiom, ifeq2(A, A, B, C)=B).
cnf(ifeq_axiom, axiom, ifeq(A, A, B, C)=B).
cnf(elem_union_1, axiom, ifeq(notelem(X, union(A, B)), true, notelem(X, A), true)=true).
cnf(elem_union_2, axiom, ifeq(notelem(X, union(A, B)), true, notelem(X, B), true)=true).
cnf(elem_union_3, axiom, ifeq(notelem(X, B), true, ifeq(notelem(X, A), true, notelem(X, union(A, B)), true), true)=true).
cnf(elem_equals, axiom, ifeq2(notelem(sK1_elem_equals_X(A, B), B), true, ifeq2(notelem(sK1_elem_equals_X(A, B), A), true, A, B), B)=B).
%cnf(union_commutative, negated_conjecture, union(a, b)!=union(b, a)).
%cnf(elem_equals_1, axiom, ifeq3(choice(A, B), c1, notelem(sK1_elem_equals_X(A, B), A), true)=true).
%cnf(elem_equals_2, axiom, ifeq3(choice(A, B), c2, notelem(sK1_elem_equals_X(A, B), B), true)=true).
%cnf(elem_equals_3, axiom, ifeq4(choice(A, B), c3, A, B)=B).
cnf(elem_equals_1, axiom, select(c1, a, d, d) = d).
cnf(elem_equals_1, axiom, select(c2, d, b, d) = d).
cnf(elem_equals_1, axiom, select(c3, d, d, c) = d).
cnf(blah, conjecture, a=d | b=d | c=d).
cnf(select, axiom, select(C, X, X, X)=X).
cnf(select, axiom, select(c1, X, Y, Z)=X).
cnf(select, axiom, select(c2, X, Y, Z)=Y).
cnf(select, axiom, select(c3, X, Y, Z)=Z).

%select(C, X, Y, Z) = select(C, select(c1, X, Y, Z), select(c2, X, Y, Z), select(c3, X, Y, Z)).

%  d
%= select(