Anne is blue. Anne is not cold. Anne is kind. Anne is red. Anne is rough. Gary is blue. Gary is not cold. Gary is red. Gary is smart. Gary is young. Smart things are young. If something is kind and not blue then it is young. All red things are kind. If something is cold and not red then it is smart. If something is cold and not young then it is rough. If something is red and not kind then it is rough.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If something is kind and not blue then it is young.
((("something" "is" "kind" "+") ("something" "is" "blue" "~")) -> ("something" "is" "young" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is cold and not red then it is smart.
((("something" "is" "cold" "+") ("something" "is" "red" "~")) -> ("something" "is" "smart" "+"))
If something is cold and not young then it is rough.
((("something" "is" "cold" "+") ("something" "is" "young" "~")) -> ("something" "is" "rough" "+"))
If something is red and not kind then it is rough.
((("something" "is" "red" "+") ("something" "is" "kind" "~")) -> ("something" "is" "rough" "+"))
Gary is smart.
True
1
proof
[(triple9)]
("Gary" "is" "smart" "+")
triple9
Gary is not young.
False
1
inv-proof
[(triple10 OR ((triple9) -> rule1))]
("Gary" "is" "young" "-")
triple10
((triple9) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
@0: Anne is blue.[(triple1)] Anne is kind.[(triple3 OR ((triple4) -> rule3))] Anne is not cold.[(triple2)] Anne is red.[(triple4)] Anne is rough.[(triple5)] Gary is blue.[(triple6)] Gary is not cold.[(triple7)] Gary is red.[(triple8)] Gary is smart.[(triple9)] Gary is young.[(triple10 OR ((triple9) -> rule1))] @1: Gary is kind.[(((triple8) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple4) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not cold.
("Anne" "is" "cold" "-")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is not cold.
("Gary" "is" "cold" "-")
triple7
Gary is red.
("Gary" "is" "red" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
((triple9) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple8) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1