Charlie is big. Charlie is blue. Charlie is furry. Charlie is nice. Charlie is red. Charlie is smart. Charlie is not young. Harry is big. Harry is blue. Harry is furry. Harry is red. Harry is smart. Smart things are blue. If something is red then it is blue. All blue things are nice. All furry, blue things are smart. If something is smart and not big then it is red. All big, young things are not furry.
Charlie is red.
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2 OR ((triple5) -> rule2) OR ((triple6) -> rule1))] Charlie is furry.[(triple3)] Charlie is nice.[(triple4 OR ((triple2) -> rule3) OR ((((triple5) -> rule2)) -> rule3) OR ((((triple6) -> rule1)) -> rule3))] Charlie is not young.[(triple7)] Charlie is red.[(triple5)] Charlie is smart.[(triple6 OR ((triple3 triple2) -> rule4) OR ((triple3 ((triple5) -> rule2)) -> rule4))] Harry is big.[(triple8)] Harry is blue.[(triple9 OR ((triple11) -> rule2) OR ((triple12) -> rule1))] Harry is furry.[(triple10)] Harry is red.[(triple11)] Harry is smart.[(triple12 OR ((triple10 triple9) -> rule4) OR ((triple10 ((triple11) -> rule2)) -> rule4))] @1: Harry is nice.[(((triple9) -> rule3) OR ((((triple11) -> rule2)) -> rule3) OR ((((triple12) -> rule1)) -> rule3))]