Anne is rough. Anne is smart. Anne is young. If something is young then it is white. Round, blue things are furry. Round things are smart. Rough, blue things are white. All blue things are white. White things are rough.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
If something is young then it is white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Round, blue things are furry.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Rough, blue things are white.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
All blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
White things are rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
Anne is young.
True
1
proof
[(triple3)]
("Anne" "is" "young" "+")
triple3
Anne is not rough.
False
1
inv-proof
[(triple1 OR ((((triple3) -> rule1)) -> rule6))]
("Anne" "is" "rough" "-")
triple1
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is rough.[(triple1 OR ((((triple3) -> rule1)) -> rule6))] Anne is smart.[(triple2)] Anne is young.[(triple3)] @1: Anne is white.[(((triple3) -> rule1))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
((triple3) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1