Gary is cold. Gary is kind. Gary is quiet. Gary is red. Gary is round. Gary is smart. Gary is white. Cold people are kind. If someone is smart then they are kind. If someone is cold then they are smart.
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If someone is cold then they are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Gary is smart.
True
1
proof
[(triple6 OR ((triple1) -> rule3))]
("Gary" "is" "smart" "+")
triple6
((triple1) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not red.
False
1
inv-proof
[(triple4)]
("Gary" "is" "red" "-")
triple4
@0: Gary is cold.[(triple1)] Gary is kind.[(triple2 OR ((triple1) -> rule1) OR ((triple6) -> rule2) OR ((((triple1) -> rule3)) -> rule2))] Gary is quiet.[(triple3)] Gary is red.[(triple4)] Gary is round.[(triple5)] Gary is smart.[(triple6 OR ((triple1) -> rule3))] Gary is white.[(triple7)]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
((triple1) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple6) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
((triple1) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple7