Anne is cold. Anne is green. Anne is quiet. Young people are big. If someone is furry then they are young. All blue people are big. If someone is green then they are cold. All cold people are green. All quiet, furry people are blue.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is furry then they are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
All cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
All quiet, furry people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Anne is cold.
True
1
proof
[(triple1 OR ((triple2) -> rule4))]
("Anne" "is" "cold" "+")
triple1
((triple2) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not quiet.
False
1
inv-proof
[(triple3)]
("Anne" "is" "quiet" "-")
triple3
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is cold.[(triple1 OR ((triple2) -> rule4))] Anne is green.[(triple2 OR ((triple1) -> rule5))] Anne is quiet.[(triple3)]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((triple2) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3