Charlie is blue. Charlie is kind. Charlie is nice. Charlie is not quiet. Charlie is red. Charlie is round. Charlie is not white. All white, round people are blue. Blue people are nice. All round people are nice. If someone is white then they are red. Nice people are kind. If Charlie is not red then Charlie is nice.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
All white, round people are blue.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
All round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is white then they are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is not red then Charlie is nice.
((("Charlie" "is" "red" "~")) -> ("Charlie" "is" "nice" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Charlie is not nice.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule2) OR ((triple6) -> rule3))]
("Charlie" "is" "nice" "-")
triple3
((triple1) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple6) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
@0: Charlie is blue.[(triple1)] Charlie is kind.[(triple2 OR ((triple3) -> rule5) OR ((((triple1) -> rule2)) -> rule5) OR ((((triple6) -> rule3)) -> rule5))] Charlie is nice.[(triple3 OR ((triple1) -> rule2) OR ((triple6) -> rule3))] Charlie is not quiet.[(triple4)] Charlie is not white.[(triple7)] Charlie is red.[(triple5)] Charlie is round.[(triple6)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
((triple3) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
((triple1) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple6) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple4
Charlie is not white.
("Charlie" "is" "white" "-")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6