Anne is furry. Anne is quiet. Harry is quiet. All white people are cold. All kind people are cold. If someone is blue and white then they are kind. Round, cold people are white. Furry people are round. If someone is blue then they are furry. If Anne is round then Anne is cold. Quiet, kind people are furry.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
All kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is blue and white then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Round, cold people are white.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
Furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
If someone is blue then they are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If Anne is round then Anne is cold.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "cold" "+"))
Quiet, kind people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Harry is quiet.
True
1
proof
[(triple3)]
("Harry" "is" "quiet" "+")
triple3
Anne is not quiet.
False
1
inv-proof
[(triple2)]
("Anne" "is" "quiet" "-")
triple2
Anne is round.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "round" "+")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "round" "-")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Harry is not furry.
Unknown
inv-rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "kind" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Anne is furry.[(triple1)] Anne is quiet.[(triple2)] Harry is quiet.[(triple3)] @1: Anne is round.[(((triple1) -> rule5))] @2: Anne is cold.[(((((triple1) -> rule5)) -> rule7))] @3: Anne is white.[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule7)) -> rule4))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3