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