declare proc {Impl X Y} {FD.impl X Y 1} end %% only simple implications `~`=FD.nega % ~ is syntax for negation proc {Kibi Sol} K % Kibi's sex: 0 male, 1 female P1 % sex of 1st parent P2 % sex of 2nd parent KC % Kibi's claim: 0 for "I am a boy", 1 for "I am a girl" TK % truth of Kibi's claim T1 % truth of 1st statement T2 % truth of 2nd statement T3 ] % truth of 3rd statement NP2=~P2 in Sol = [K P1 P2 KC TK T1 T2 T3] Sol ::: 0#1 {Impl ~K TK} % if Kibi is male then his statement is true {FD.equi KC K} = TK % Kibi tells the truth iff his claim tells his sex T1 = ~KC % the 1st statement describes Kibi's claim K = T2 % the 2nd statement describes Kibi's sex T3 = ~TK % the 3rd statement describes the truth of Kibi's claim P1 = NP2 % P1 and P2 have opposite sexes {Impl ~P1 T1} % if P1 is male then T1 {Impl NP2 T2} % if P2 is male then T2 {Impl NP2 T3} % if P2 is male then T3 {Impl P2 {FD.exor T2 T3}} % if P2 is female then either T2 or T3 {FD.distribute naive Sol} end {ExploreAll Kibi}Thus Kibi is a girl, the first parent is her mother and the second her father, and she claimed to be a boy.
Output: (1|1|0|0|0|1|1|1|nil)|nil
The search tree has only two choice points and two failure nodes.