Charlie is big. Charlie is cold. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is rough. Charlie is smart. Dave is big. Dave is cold. Dave is nice. Dave is quiet. Dave is red. Dave is rough. Dave is smart. Smart people are red. Big people are quiet.
Charlie is not red.
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple2)] Charlie is nice.[(triple3)] Charlie is quiet.[(triple4 OR ((triple1) -> rule2))] Charlie is red.[(triple5 OR ((triple7) -> rule1))] Charlie is rough.[(triple6)] Charlie is smart.[(triple7)] Dave is big.[(triple8)] Dave is cold.[(triple9)] Dave is nice.[(triple10)] Dave is quiet.[(triple11 OR ((triple8) -> rule2))] Dave is red.[(triple12 OR ((triple14) -> rule1))] Dave is rough.[(triple13)] Dave is smart.[(triple14)]