twee-2.3: tests/REL038-1.p

cnf(maddux1_join_commutativity_1, axiom, join(A, B)=join(B, A)).
cnf(maddux2_join_associativity_2, axiom, join(A, join(B, C))=join(join(A, B), C)).
cnf(maddux3_a_kind_of_de_Morgan_3, axiom, A=join(complement(join(complement(A), complement(B))), complement(join(complement(A), B)))).
cnf(maddux4_definiton_of_meet_4, axiom, meet(A, B)=complement(join(complement(A), complement(B)))).
cnf(composition_associativity_5, axiom, composition(A, composition(B, C))=composition(composition(A, B), C)).
cnf(composition_identity_6, axiom, composition(A, one)=A).
cnf(composition_distributivity_7, axiom, composition(join(A, B), C)=join(composition(A, C), composition(B, C))).
cnf(converse_idempotence_8, axiom, converse(converse(A))=A).
cnf(converse_additivity_9, axiom, converse(join(A, B))=join(converse(A), converse(B))).
cnf(converse_multiplicativity_10, axiom, converse(composition(A, B))=composition(converse(B), converse(A))).
cnf(converse_cancellativity_11, axiom, join(composition(converse(A), complement(composition(A, B))), complement(B))=complement(B)).
cnf(def_top_12, axiom, top=join(A, complement(A))).
cnf(def_zero_13, axiom, zero=meet(A, complement(A))).
cnf(goals_14, negated_conjecture, join(meet(composition(sk1, sk2), sk3), meet(composition(sk1, meet(sk2, composition(converse(sk1), sk3))), sk3))!=meet(composition(sk1, meet(sk2, composition(converse(sk1), sk3))), sk3)).