Bob is red. Charlie is kind. Charlie is quiet. Charlie is white. Dave is big. Dave is kind. Harry is quiet. If someone is smart then they are red. All round people are not red. All smart, big people are round. All big people are round. If someone is quiet then they are big. White people are kind. If someone is quiet and not red then they are kind. Smart, quiet people are kind. Kind people are white.
Dave is red.
@0: Bob is red.[(triple1)] Charlie is kind.[(triple2 OR ((triple4) -> rule6) OR ((triple3 ((((((triple3) -> rule5)) -> rule4)) -> rule2)) -> rule7))] Charlie is quiet.[(triple3)] Charlie is white.[(triple4 OR ((triple2) -> rule9) OR ((((triple3 ((((((triple3) -> rule5)) -> rule4)) -> rule2)) -> rule7)) -> rule9))] Dave is big.[(triple5)] Dave is kind.[(triple6)] Harry is quiet.[(triple7)] @1: Charlie is big.[(((triple3) -> rule5))] Dave is round.[(((triple5) -> rule4))] Dave is white.[(((triple6) -> rule9))] Harry is big.[(((triple7) -> rule5))] @2: Charlie is round.[(((((triple3) -> rule5)) -> rule4))] Dave is not red.[(((((triple5) -> rule4)) -> rule2))] Harry is round.[(((((triple7) -> rule5)) -> rule4))] @3: Charlie is not red.[(((((((triple3) -> rule5)) -> rule4)) -> rule2))] Harry is not red.[(((((((triple7) -> rule5)) -> rule4)) -> rule2))] @4: Harry is kind.[(((triple7 ((((((triple7) -> rule5)) -> rule4)) -> rule2)) -> rule7))] @5: Harry is white.[(((((triple7 ((((((triple7) -> rule5)) -> rule4)) -> rule2)) -> rule7)) -> rule9))]