Anne is quiet. Bob is kind. Charlie is quiet. Kind things are not smart. Young things are smart. All smart things are not quiet. All kind things are furry. If something is young then it is nice. If Bob is not quiet and Bob is not kind then Bob is furry. If Charlie is nice and Charlie is not furry then Charlie is not quiet. If Charlie is not nice then Charlie is quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Kind things are not smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "-"))
Young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
All smart things are not quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "-"))
All kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If Bob is not quiet and Bob is not kind then Bob is furry.
((("Bob" "is" "quiet" "~") ("Bob" "is" "kind" "~")) -> ("Bob" "is" "furry" "+"))
If Charlie is nice and Charlie is not furry then Charlie is not quiet.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "furry" "~")) -> ("Charlie" "is" "quiet" "-"))
If Charlie is not nice then Charlie is quiet.
((("Charlie" "is" "nice" "~")) -> ("Charlie" "is" "quiet" "+"))
Charlie is quiet.
True
1
proof
[(triple3)]
("Charlie" "is" "quiet" "+")
triple3
Charlie is not quiet.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "quiet" "-")
triple3
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is quiet.[(triple1)] Bob is kind.[(triple2)] Charlie is quiet.[(triple3)] @1: Bob is furry.[(((triple2) -> rule4))] Bob is not smart.[(((triple2) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not smart.
("Bob" "is" "smart" "-")
((triple2) -> (rule1 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1