Anne is kind. If Anne is smart and Anne is furry then Anne is cold. If Anne is smart and Anne is cold then Anne is young. Young things are furry. Furry things are blue. Kind things are furry. If something is kind and smart then it is quiet. If Anne is blue and Anne is young then Anne is quiet. If something is smart and kind then it is quiet.
Anne is kind.
("Anne" "is" "kind" "+")
If Anne is smart and Anne is furry then Anne is cold.
((("Anne" "is" "smart" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "cold" "+"))
If Anne is smart and Anne is cold then Anne is young.
((("Anne" "is" "smart" "+") ("Anne" "is" "cold" "+")) -> ("Anne" "is" "young" "+"))
Young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If something is kind and smart then it is quiet.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If Anne is blue and Anne is young then Anne is quiet.
((("Anne" "is" "blue" "+") ("Anne" "is" "young" "+")) -> ("Anne" "is" "quiet" "+"))
If something is smart and kind then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
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 furry.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "furry" "-")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is quiet.
Unknown
rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "young" "-")
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 furry.[(((triple1) -> rule5))] @2: Anne is blue.[(((((triple1) -> rule5)) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2