Anne is kind. If someone is round then they are rough. If someone is cold and white then they are kind. All kind people are green.
Anne is kind.
("Anne" "is" "kind" "+")
If someone is round then they are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold and white then they are kind.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
All kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Anne is green.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "green" "+")
((triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "green" "-")
((triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is kind.[(triple1)] @1: Anne is green.[(((triple1) -> rule3))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1