MCK, version 0.2.0, Jun, 2004.
(C)opyright 2002 - 2004 University of New South Wales.

>> Spec holds:
rus.mck:121: spec_spr_xn =
(X (X a_announce ==> ((((((Knows B (a_hand[0]) \/ Knows B (neg a_hand[0])) /\ (Knows B (a_hand[1]) \/ Knows B (neg a_hand[1]))) /\ (Knows B (a_hand[2]) \/ Knows B (neg a_hand[2]))) /\ (Knows B (a_hand[3]) \/ Knows B (neg a_hand[3]))) /\ (Knows B (a_hand[4]) \/ Knows B (neg a_hand[4]))) /\ (Knows B (a_hand[5]) \/ Knows B (neg a_hand[5]))) /\ (Knows B (a_hand[6]) \/ Knows B (neg a_hand[6]))))
>> Spec fails:
rus.mck:135: spec_spr_xn =
(X (X a_announce ==> ((((((Knows A (b_hand[0]) \/ Knows A (neg b_hand[0])) /\ (Knows A (b_hand[1]) \/ Knows A (neg b_hand[1]))) /\ (Knows A (b_hand[2]) \/ Knows A (neg b_hand[2]))) /\ (Knows A (b_hand[3]) \/ Knows A (neg b_hand[3]))) /\ (Knows A (b_hand[4]) \/ Knows A (neg b_hand[4]))) /\ (Knows A (b_hand[5]) \/ Knows A (neg b_hand[5]))) /\ (Knows A (b_hand[6]) \/ Knows A (neg b_hand[6]))))
>> Spec holds:
rus.mck:148: spec_spr_xn =
(X (X a_announce ==> (((((neg (Knows C (a_hand[0]) \/ Knows C (b_hand[0])) /\ neg (Knows C (a_hand[1]) \/ Knows C (b_hand[1]))) /\ neg (Knows C (a_hand[2]) \/ Knows C (b_hand[2]))) /\ neg (Knows C (a_hand[3]) \/ Knows C (b_hand[3]))) /\ neg (Knows C (a_hand[4]) \/ Knows C (b_hand[4]))) /\ neg (Knows C (a_hand[5]) \/ Knows C (b_hand[5]))) /\ neg (Knows C (a_hand[6]) \/ Knows C (b_hand[6]))))
>> Spec holds:
rus.mck:160: spec_spr_xn =
(X (X (X a_announce /\ b_announce ==> ((((((Knows A (b_hand[0]) \/ Knows A (neg b_hand[0])) /\ (Knows A (b_hand[1]) \/ Knows A (neg b_hand[1]))) /\ (Knows A (b_hand[2]) \/ Knows A (neg b_hand[2]))) /\ (Knows A (b_hand[3]) \/ Knows A (neg b_hand[3]))) /\ (Knows A (b_hand[4]) \/ Knows A (neg b_hand[4]))) /\ (Knows A (b_hand[5]) \/ Knows A (neg b_hand[5]))) /\ (Knows A (b_hand[6]) \/ Knows A (neg b_hand[6])))))
>> Spec holds:
rus.mck:172: spec_spr_xn =
(X (X (X a_announce /\ b_announce ==> (((((neg (Knows C (a_hand[0]) \/ Knows C (b_hand[0])) /\ neg (Knows C (a_hand[1]) \/ Knows C (b_hand[1]))) /\ neg (Knows C (a_hand[2]) \/ Knows C (b_hand[2]))) /\ neg (Knows C (a_hand[3]) \/ Knows C (b_hand[3]))) /\ neg (Knows C (a_hand[4]) \/ Knows C (b_hand[4]))) /\ neg (Knows C (a_hand[5]) \/ Knows C (b_hand[5]))) /\ neg (Knows C (a_hand[6]) \/ Knows C (b_hand[6])))))