Anne is furry. All furry people are big. Furry people are round. If someone is round and red then they are smart. If someone is red and big then they are not rough. If someone is furry and round then they are not cold. Rough, smart people are not cold.
Anne is furry.
("Anne" "is" "furry" "+")
All furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
If someone is round and red then they are smart.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If someone is red and big then they are not rough.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "-"))
If someone is furry and round then they are not cold.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "-"))
Rough, smart people are not cold.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "-"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Anne is big.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "big" "+")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "big" "-")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not cold.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule5))]
("Anne" "is" "cold" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule5))]
("Anne" "is" "cold" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is furry.[(triple1)] @1: Anne is big.[(((triple1) -> rule1))] Anne is round.[(((triple1) -> rule2))] @2: Anne is not cold.[(((triple1 ((triple1) -> rule2)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not cold.
("Anne" "is" "cold" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is round.
("Anne" "is" "round" "+")
int2