Anne is red. If something is furry then it is nice. If Anne is nice then Anne is white. All red things are not smart. If something is furry then it is smart. If something is furry and not round then it is young. If something is red and not smart then it is not young.
Anne is red.
("Anne" "is" "red" "+")
If something is furry then it is nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If Anne is nice then Anne is white.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "white" "+"))
All red things are not smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "-"))
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is furry and not round then it is young.
((("something" "is" "furry" "+") ("something" "is" "round" "~")) -> ("something" "is" "young" "+"))
If something is red and not smart then it is not young.
((("something" "is" "red" "+") ("something" "is" "smart" "~")) -> ("something" "is" "young" "-"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Anne is not red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Anne is not smart.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "smart" "-")
((triple1) -> (rule3 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is smart.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is not young.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule6))]
("Anne" "is" "young" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is not smart.
("Anne" "is" "smart" "-")
int2
Anne is young.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule6))]
("Anne" "is" "young" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is not smart.
("Anne" "is" "smart" "-")
int2
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is white.
Unknown
rconc
[@2: Anne is white.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (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 red.[(triple1)] @1: Anne is not smart.[(((triple1) -> rule3))] @2: Anne is not young.[(((triple1 ((triple1) -> rule3)) -> rule6))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is not smart.
("Anne" "is" "smart" "-")
((triple1) -> (rule3 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is not young.
("Anne" "is" "young" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is not smart.
("Anne" "is" "smart" "-")
int2