Charlie is big. Charlie is green. Charlie is quiet. Charlie is not red. Charlie is rough. Charlie is not round. Charlie is not smart. If Charlie is green then Charlie is not round.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Charlie is not smart.
("Charlie" "is" "smart" "-")
If Charlie is green then Charlie is not round.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "round" "-"))
Charlie is not smart.
True
1
proof
[(triple7)]
("Charlie" "is" "smart" "-")
triple7
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
@0: Charlie is big.[(triple1)] Charlie is green.[(triple2)] Charlie is not red.[(triple4)] Charlie is not round.[(triple6 OR ((triple2) -> rule1))] Charlie is not smart.[(triple7)] Charlie is quiet.[(triple3)] Charlie is rough.[(triple5)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is not red.
("Charlie" "is" "red" "-")
triple4
Charlie is not round.
("Charlie" "is" "round" "-")
triple6
((triple2) -> (rule1 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5