Bob is nice. Dave is green. Dave is kind. If someone is kind then they are not furry. All furry people are quiet. If someone is furry then they are not nice.
Bob is nice.
("Bob" "is" "nice" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
If someone is kind then they are not furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "-"))
All furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is furry then they are not nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "-"))
Dave is kind.
True
1
proof
[(triple3)]
("Dave" "is" "kind" "+")
triple3
Dave is not kind.
False
1
inv-proof
[(triple3)]
("Dave" "is" "kind" "-")
triple3
Dave is not furry.
True
2
proof
[(((triple3) -> rule1))]
("Dave" "is" "furry" "-")
((triple3) -> (rule1 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is furry.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Bob is nice.[(triple1)] Dave is green.[(triple2)] Dave is kind.[(triple3)] @1: Dave is not furry.[(((triple3) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is not furry.
("Dave" "is" "furry" "-")
((triple3) -> (rule1 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1