Anne is furry. Anne is red. Anne is round. Anne is white. Dave is cold. Dave is kind. Dave is young. If someone is round then they are cold. All red, young people are round. If someone is cold and furry then they are kind.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
All red, young people are round.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is cold and furry then they are kind.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Anne is round.
True
1
proof
[(triple3)]
("Anne" "is" "round" "+")
triple3
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Anne is cold.
True
2
proof
[(((triple3) -> rule1))]
("Anne" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple3) -> rule1))]
("Anne" "is" "cold" "-")
((triple3) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
True
4
proof
[(((((triple3) -> rule1) triple1) -> rule3))]
("Anne" "is" "kind" "+")
((((triple3) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not kind.
False
4
inv-proof
[(((((triple3) -> rule1) triple1) -> rule3))]
("Anne" "is" "kind" "-")
((((triple3) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is furry.[(triple1)] Anne is red.[(triple2)] Anne is round.[(triple3)] Anne is white.[(triple4)] Dave is cold.[(triple5)] Dave is kind.[(triple6)] Dave is young.[(triple7)] @1: Anne is cold.[(((triple3) -> rule1))] @2: Anne is kind.[(((((triple3) -> rule1) triple1) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Anne is cold.
("Anne" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple3) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2