Bob is not big. Bob is cold. Bob is quiet. Bob is red. Bob is not round. Bob is smart. Charlie is big. Charlie is cold. Gary is cold. Gary is kind. Gary is quiet. Gary is round. Gary is smart. Harry is not cold. Harry is not kind. Harry is smart. If Charlie is round and Charlie is kind then Charlie is not quiet. If Bob is round then Bob is kind. If someone is big then they are red. Big people are smart. Red, quiet people are cold. If someone is big and not red then they are not cold.
Bob is not kind.
@0: Bob is cold.[(triple2 OR ((triple4 triple3) -> rule5))] Bob is not big.[(triple1)] Bob is not round.[(triple5)] Bob is quiet.[(triple3)] Bob is red.[(triple4)] Bob is smart.[(triple6)] Charlie is big.[(triple7)] Charlie is cold.[(triple8)] Gary is cold.[(triple9)] Gary is kind.[(triple10)] Gary is quiet.[(triple11)] Gary is round.[(triple12)] Gary is smart.[(triple13)] Harry is not cold.[(triple14)] Harry is not kind.[(triple15)] Harry is smart.[(triple16)] @1: Charlie is red.[(((triple7) -> rule3))] Charlie is smart.[(((triple7) -> rule4))]