Anne is nice. Dave is nice. Harry is white. If someone is white and not big then they are rough. Nice people are rough. If someone is red and not blue then they are nice. All red people are nice. If someone is big then they are not cold. Rough, cold people are white.
Anne is nice.
("Anne" "is" "nice" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is white and not big then they are rough.
((("someone" "is" "white" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "rough" "+"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is red and not blue then they are nice.
((("someone" "is" "red" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "nice" "+"))
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is big then they are not cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "-"))
Rough, cold people are white.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Dave is nice.
True
1
proof
[(triple2)]
("Dave" "is" "nice" "+")
triple2
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "white" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is nice.[(triple1)] Dave is nice.[(triple2)] Harry is white.[(triple3)] @1: Anne is rough.[(((triple1) -> rule2))] Dave is rough.[(((triple2) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1