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