Anne is blue. Bob is furry. Charlie is nice. Harry is furry. If something is round then it is smart. If Anne is red then Anne is furry. If Bob is not smart then Bob is furry. If Charlie is rough then Charlie is furry. Nice, furry things are rough. All furry things are not nice.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If something is round then it is smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If Anne is red then Anne is furry.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "furry" "+"))
If Bob is not smart then Bob is furry.
((("Bob" "is" "smart" "~")) -> ("Bob" "is" "furry" "+"))
If Charlie is rough then Charlie is furry.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "furry" "+"))
Nice, furry things are rough.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All furry things are not nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "-"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "smart" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is blue.[(triple1)] Bob is furry.[(triple2)] Charlie is nice.[(triple3)] Harry is furry.[(triple4)] @1: Bob is not nice.[(((triple2) -> rule6))] Harry is not nice.[(((triple4) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Bob is not nice.
("Bob" "is" "nice" "-")
((triple2) -> (rule6 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Harry is not nice.
("Harry" "is" "nice" "-")
((triple4) -> (rule6 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1