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