Charlie is blue. Charlie is green. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is rough. Charlie is white. If someone is white then they are rough. All white people are quiet.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If someone is white then they are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is quiet.
True
1
proof
[(triple5 OR ((triple7) -> rule2))]
("Charlie" "is" "quiet" "+")
triple5
((triple7) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not green.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "green" "-")
triple2
@0: Charlie is blue.[(triple1)] Charlie is green.[(triple2)] Charlie is kind.[(triple3)] Charlie is nice.[(triple4)] Charlie is quiet.[(triple5 OR ((triple7) -> rule2))] Charlie is rough.[(triple6 OR ((triple7) -> rule1))] Charlie is white.[(triple7)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
((triple7) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
((triple7) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple7