Dave is kind. Dave is red. Dave is smart. If Dave is not green and Dave is not furry then Dave is nice. If Dave is smart then Dave is nice.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If Dave is not green and Dave is not furry then Dave is nice.
((("Dave" "is" "green" "~") ("Dave" "is" "furry" "~")) -> ("Dave" "is" "nice" "+"))
If Dave is smart then Dave is nice.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "nice" "+"))
Dave is smart.
True
1
proof
[(triple3)]
("Dave" "is" "smart" "+")
triple3
Dave is not red.
False
1
inv-proof
[(triple2)]
("Dave" "is" "red" "-")
triple2
Dave is nice.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "nice" "-")
((triple3) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Dave is kind.[(triple1)] Dave is red.[(triple2)] Dave is smart.[(triple3)] @1: Dave is nice.[(((triple3) -> rule2))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1