Anne is rough. Harry is rough. Nice people are furry. If someone is rough then they are furry. If someone is young then they are nice. All smart, nice people are rough. If someone is smart and not big then they are not young. If Anne is not nice then Anne is green.
Anne is rough.
("Anne" "is" "rough" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If someone is rough then they are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If someone is young then they are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
All smart, nice people are rough.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart and not big then they are not young.
((("someone" "is" "smart" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "young" "-"))
If Anne is not nice then Anne is green.
((("Anne" "is" "nice" "~")) -> ("Anne" "is" "green" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Harry is not rough.
False
1
inv-proof
[(triple2)]
("Harry" "is" "rough" "-")
triple2
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "nice" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Anne is rough.[(triple1)] Harry is rough.[(triple2)] @1: Anne is furry.[(((triple1) -> rule2))] Harry is furry.[(((triple2) -> rule2))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Harry is rough.
("Harry" "is" "rough" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1