Gary is blue. Gary is green. Gary is kind. Gary is red. Gary is rough. Gary is smart. Gary is white. All kind, green people are red. All green, red people are kind. All smart people are white.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
All kind, green people are red.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
All green, red people are kind.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Gary is white.
True
1
proof
[(triple7 OR ((triple6) -> rule3))]
("Gary" "is" "white" "+")
triple7
((triple6) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not smart.
False
1
inv-proof
[(triple6)]
("Gary" "is" "smart" "-")
triple6
@0: Gary is blue.[(triple1)] Gary is green.[(triple2)] Gary is kind.[(triple3 OR ((triple2 triple4) -> rule2))] Gary is red.[(triple4 OR ((triple3 triple2) -> rule1))] Gary is rough.[(triple5)] Gary is smart.[(triple6)] Gary is white.[(triple7 OR ((triple6) -> rule3))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
Gary is green.
("Gary" "is" "green" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
((triple2 triple4) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple4
((triple3 triple2) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
((triple6) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1