Dave is green. Dave is kind. Dave is nice. If someone is big then they are not kind. Green people are young. If someone is cold and nice then they are green. If someone is green and cold then they are nice. Kind people are nice. If Dave is not furry then Dave is nice.
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
If someone is big then they are not kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "-"))
Green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is cold and nice then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is green and cold then they are nice.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
Kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If Dave is not furry then Dave is nice.
((("Dave" "is" "furry" "~")) -> ("Dave" "is" "nice" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Dave is not nice.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule5))]
("Dave" "is" "nice" "-")
triple3
((triple2) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is green.[(triple1)] Dave is kind.[(triple2)] Dave is nice.[(triple3 OR ((triple2) -> rule5))] @1: Dave is young.[(((triple1) -> rule2))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple2) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple1) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1