Dave is furry. Dave is kind. Gary is big. Gary is furry. Gary is kind. Gary is quiet. Gary is white. Quiet, big people are not nice. If someone is quiet and kind then they are big.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
Quiet, big people are not nice.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "-"))
If someone is quiet and kind then they are big.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Dave is kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "+")
triple2
Gary is not white.
False
1
inv-proof
[(triple7)]
("Gary" "is" "white" "-")
triple7
Gary is not nice.
True
3
proof
[(((triple6 triple3) -> rule1) OR ((triple6 ((triple6 triple5) -> rule2)) -> rule1))]
("Gary" "is" "nice" "-")
((triple6 triple3) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
((triple6 ((triple6 triple5) -> (rule2 % int2))) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
False
3
inv-proof
[(((triple6 triple3) -> rule1) OR ((triple6 ((triple6 triple5) -> rule2)) -> rule1))]
("Gary" "is" "nice" "+")
((triple6 triple3) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
((triple6 ((triple6 triple5) -> (rule2 % int2))) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Dave is furry.[(triple1)] Dave is kind.[(triple2)] Gary is big.[(triple3 OR ((triple6 triple5) -> rule2))] Gary is furry.[(triple4)] Gary is kind.[(triple5)] Gary is quiet.[(triple6)] Gary is white.[(triple7)] @1: Gary is not nice.[(((triple6 triple3) -> rule1) OR ((triple6 ((triple6 triple5) -> rule2)) -> rule1))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
((triple6 triple5) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Gary is kind.
("Gary" "is" "kind" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
Gary is not nice.
("Gary" "is" "nice" "-")
((triple6 triple3) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
((triple6 ((triple6 triple5) -> (rule2 % int2))) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2