Charlie is big. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is not rough. Charlie is round. Charlie is not smart. If Charlie is rough and Charlie is round then Charlie is quiet. If someone is quiet and not red then they are not rough.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
If Charlie is rough and Charlie is round then Charlie is quiet.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "quiet" "+"))
If someone is quiet and not red then they are not rough.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "rough" "-"))
Charlie is not rough.
True
1
proof
[(triple5)]
("Charlie" "is" "rough" "-")
triple5
Charlie is not quiet.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "quiet" "-")
triple3
@0: Charlie is big.[(triple1)] Charlie is nice.[(triple2)] Charlie is not rough.[(triple5)] Charlie is not smart.[(triple7)] Charlie is quiet.[(triple3)] Charlie is red.[(triple4)] Charlie is round.[(triple6)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple5
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple6