Anne is not nice. Anne is red. Anne is young. Harry is kind. Harry is red. Harry is rough. Harry is not white. If Anne is nice and Anne is not white then Anne is not kind. If Anne is white then Anne is not young. If someone is red and not young then they are not kind. If someone is white and not nice then they are kind. If someone is red then they are kind. If someone is red and rough then they are cold. If someone is nice and not kind then they are rough. If someone is young and not kind then they are rough.
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not white.
("Harry" "is" "white" "-")
If Anne is nice and Anne is not white then Anne is not kind.
((("Anne" "is" "nice" "+") ("Anne" "is" "white" "~")) -> ("Anne" "is" "kind" "-"))
If Anne is white then Anne is not young.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "young" "-"))
If someone is red and not young then they are not kind.
((("someone" "is" "red" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "kind" "-"))
If someone is white and not nice then they are kind.
((("someone" "is" "white" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "kind" "+"))
If someone is red then they are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and rough then they are cold.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice and not kind then they are rough.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "rough" "+"))
If someone is young and not kind then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "rough" "+"))
Harry is rough.
True
1
proof
[(triple6)]
("Harry" "is" "rough" "+")
triple6
Harry is not rough.
False
1
inv-proof
[(triple6)]
("Harry" "is" "rough" "-")
triple6
Anne is not cold.
Unknown
inv-rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is not nice.[(triple1)] Anne is red.[(triple2)] Anne is young.[(triple3)] Harry is kind.[(triple4 OR ((triple5) -> rule5))] Harry is not white.[(triple7)] Harry is red.[(triple5)] Harry is rough.[(triple6)] @1: Anne is kind.[(((triple2) -> rule5))] Harry is cold.[(((triple5 triple6) -> rule6))]
Anne is not nice.
("Anne" "is" "nice" "-")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
((triple5) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
triple7
Harry is red.
("Harry" "is" "red" "+")
triple5
Harry is rough.
("Harry" "is" "rough" "+")
triple6
Anne is kind.
("Anne" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple5 triple6) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1