Don't Ask Alice - Part the Fifth

This is the fifth installment on Dodgson's unsolved sorites - for the previous four go here:
Don't ask Alice, I don't think she'll know [from Dodgson's Symbolic Logic, p. 186]
Don't ask Alice - Part the Second [from Dodgson's Symbolic Logic, p. 187]
Don't ask Alice - Part the Third [from Dodgson's Symbolic Logic, p. 188]
Don't ask Alice - Part the Fourth [from Dodgson's Symbolic Logic, p. 190]
Without further ado, here is the fifth of Dodgson's [hitherto] unsolved sorites:

Six friends, and their six wives, are staying in the same hotel; and they all walk out daily, in parties of various size and composition. To ensure variety in these daily walks, they have agree to observe the following Rules:---
(1) If Acres is with (i.e. is in the same party with) his wife, and Barry with his, and Eden with Mrs. Hall, Cole must be with Mrs. Dix;
(2) If Acres is with his wife, and Hall with his, and Barry with Mrs. Cole, Dix must not be with Mrs. Eden;
(3) If Cole and Dix and their wives are all in the same party, and Acres not with Mrs. Barry, Eden must not be with Mrs. Hall;
(4) If Acres is with his wife, and Dix with his, and Barry not with Mrs. Cole, Eden must be with Mrs. Hall;
(5) If Eden is with his wife, and Hall with his, and Cole with Mrs. Dix, Acres must not be with Mrs. Barry;
(6) If Barry and Cole and their wives are all in the same party, and Eden not with Mrs. Hall, Dix must be with Mrs. Eden.
The Problem is to prove that there must be, every day, at least one married couple who are not in the same party.

This problem is simplest by introducing the propositional functions g_J(I) = {U,U^~} representing the condition (true or false) that the individual I is in the same party as Mrs. J (this type of function was unknown to Dodgson). The universe of individuals is {A, B, C, D, E, H, MA, MB, MC, MD, ME, MH} representing Acres, Barry, Cole, Dix, Eden, Hall, and Mrs. Acres, etc. (the Mrs. don't enter into the problem except through the functions). Transcribing each of the premises and writing them as a conjunction:
ρ(g_A(A)^~g_B(B)^~g_H(E)^~g_D(C)) · ρ(g_A(A)^~g_H(H)^~g_C(B)^~g_E(D)^~) · ρ(g_C(C)^~g_D(D)^~g_B(A)g_H(E)^~) · ρ(g_A(A)^~g_D(D)^~g_C(B)g_H(E)) · ρ(g_E(E)^~g_H(H)^~g_D(C)^~g_B(A)^~) · ρ(g_B(B)^~g_C(C)^~g_H(E)g_E(D))
Applying the theorem, canceling those terms which appear both complemented and uncomplemented (shown underlined above), produces the conclusion:

ρ(g_A(A)^~g_B(B)^~g_C(C)^~g_D(D)^~g_E(E)^~g_H(H)^~),    or
¬(g_A(A) · g_B(B) · g_C(C) · g_D(D) · g_E(E) · g_H(H))

Hence, that all of the men are in groups with their wives must be false, or at least one married couple is not in the same party. Q.E.D.