Anne is furry. Anne is red. Dave is red. Dave is not young. Erin is not green. Erin is smart. Harry is not furry. All blue things are not green. Red things are not smart. All young, green things are blue.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not young.
("Dave" "is" "young" "-")
Erin is not green.
("Erin" "is" "green" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
All blue things are not green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "-"))
Red things are not smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "-"))
All young, green things are blue.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Erin is smart.
True
1
proof
[(triple6)]
("Erin" "is" "smart" "+")
triple6
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is furry.[(triple1)] Anne is red.[(triple2)] Dave is not young.[(triple4)] Dave is red.[(triple3)] Erin is not green.[(triple5)] Erin is smart.[(triple6)] Harry is not furry.[(triple7)] @1: Anne is not smart.[(((triple2) -> rule2))] Dave is not smart.[(((triple3) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Dave is not young.
("Dave" "is" "young" "-")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple3
Erin is not green.
("Erin" "is" "green" "-")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Harry is not furry.
("Harry" "is" "furry" "-")
triple7
Anne is not smart.
("Anne" "is" "smart" "-")
((triple2) -> (rule2 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Dave is not smart.
("Dave" "is" "smart" "-")
((triple3) -> (rule2 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1