Anne is round. If something is kind and not blue then it is white. If something is round and white then it is smart. Green things are smart. If Anne is rough then Anne is not green. Green things are not kind. If Anne is round then Anne is smart. If something is green and blue then it is rough. White things are round.
Anne is round.
("Anne" "is" "round" "+")
If something is kind and not blue then it is white.
((("something" "is" "kind" "+") ("something" "is" "blue" "~")) -> ("something" "is" "white" "+"))
If something is round and white then it is smart.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If Anne is rough then Anne is not green.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "green" "-"))
Green things are not kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "-"))
If Anne is round then Anne is smart.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "smart" "+"))
If something is green and blue then it is rough.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Anne is round.
True
1
proof
[(triple1)]
("Anne" "is" "round" "+")
triple1
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Anne is smart.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "smart" "-")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is round.[(triple1)] @1: Anne is smart.[(((triple1) -> rule6))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1