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