Anne is big. Anne is blue. Anne is quiet. Bob is furry. Bob is not green. Bob is not rough. Erin is blue. All big things are blue. If something is quiet then it is furry. If something is quiet and not rough then it is big.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is not rough.
("Bob" "is" "rough" "-")
Erin is blue.
("Erin" "is" "blue" "+")
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is quiet then it is furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If something is quiet and not rough then it is big.
((("something" "is" "quiet" "+") ("something" "is" "rough" "~")) -> ("something" "is" "big" "+"))
Bob is not green.
True
1
proof
[(triple5)]
("Bob" "is" "green" "-")
triple5
Anne is not blue.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule1))]
("Anne" "is" "blue" "-")
triple2
((triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is not blue.
Unknown
inv-rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Bob" "is" "blue" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple1) -> rule1))] Anne is quiet.[(triple3)] Bob is furry.[(triple4)] Bob is not green.[(triple5)] Bob is not rough.[(triple6)] Erin is blue.[(triple7)] @1: Anne is furry.[(((triple3) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is not green.
("Bob" "is" "green" "-")
triple5
Bob is not rough.
("Bob" "is" "rough" "-")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Anne is furry.
("Anne" "is" "furry" "+")
((triple3) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1