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