Charlie is young. Dave is furry. Gary is big. Harry is big. If Dave is quiet and Dave is big then Dave is kind. If Dave is smart and Dave is furry then Dave is rough.
Charlie is young.
("Charlie" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
If Dave is quiet and Dave is big then Dave is kind.
((("Dave" "is" "quiet" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "kind" "+"))
If Dave is smart and Dave is furry then Dave is rough.
((("Dave" "is" "smart" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "rough" "+"))
Charlie is young.
True
1
proof
[(triple1)]
("Charlie" "is" "young" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple4)]
("Harry" "is" "big" "-")
triple4
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "rough" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is young.[(triple1)] Dave is furry.[(triple2)] Gary is big.[(triple3)] Harry is big.[(triple4)]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4