Anne is furry. Anne is round. Anne is white. Round things are rough. Furry, red things are cold. If something is cold then it is white. If something is furry and cold then it is smart. If something is cold then it is smart. All white, red things are smart. If something is smart and round then it is cold. Cold things are red.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
Furry, red things are cold.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it is white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is furry and cold then it is smart.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
All white, red things are smart.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If something is smart and round then it is cold.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Anne is not white.
False
1
inv-proof
[(triple3)]
("Anne" "is" "white" "-")
triple3
@0: Anne is furry.[(triple1)] Anne is round.[(triple2)] Anne is white.[(triple3)] @1: Anne is rough.[(((triple2) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1