Anne is furry. Dave is furry. Erin is young. Gary is nice. Cold people are kind. If Anne is furry then Anne is young. If someone is white then they are furry. White, nice people are not furry. All young people are white. If someone is big and not kind then they are nice. If someone is cold and big then they are nice. If someone is white and young then they are not nice.
Anne is furry.
("Anne" "is" "furry" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If Anne is furry then Anne is young.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "young" "+"))
If someone is white then they are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
White, nice people are not furry.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "-"))
All young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If someone is big and not kind then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "nice" "+"))
If someone is cold and big then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is white and young then they are not nice.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "-"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Dave is not furry.
False
1
inv-proof
[(triple2)]
("Dave" "is" "furry" "-")
triple2
Erin is white.
True
2
proof
[(((triple3) -> rule5))]
("Erin" "is" "white" "+")
((triple3) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "young" "-")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is furry.
True
3
proof
[(((((triple3) -> rule5)) -> rule3))]
("Erin" "is" "furry" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
False
4
inv-proof
[(((((triple3) -> rule5) triple3) -> rule8))]
("Erin" "is" "nice" "+")
((((triple3) -> (rule5 % int2)) triple3) -> (rule8 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Anne is not nice.
True
6
proof
[(((((((triple1) -> rule2)) -> rule5) ((triple1) -> rule2)) -> rule8))]
("Anne" "is" "nice" "-")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule2 % int3))) -> (rule8 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is nice.
False
6
inv-proof
[(((((((triple1) -> rule2)) -> rule5) ((triple1) -> rule2)) -> rule8))]
("Anne" "is" "nice" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule2 % int3))) -> (rule8 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "white" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "kind" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "nice" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Anne is furry.[(triple1)] Dave is furry.[(triple2)] Erin is young.[(triple3)] Gary is nice.[(triple4)] @1: Anne is young.[(((triple1) -> rule2))] Erin is white.[(((triple3) -> rule5))] @2: Anne is white.[(((((triple1) -> rule2)) -> rule5))] Erin is furry.[(((((triple3) -> rule5)) -> rule3))] Erin is not nice.[(((((triple3) -> rule5) triple3) -> rule8))] @3: Anne is not nice.[(((((((triple1) -> rule2)) -> rule5) ((triple1) -> rule2)) -> rule8))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not nice.
("Erin" "is" "nice" "-")
((((triple3) -> (rule5 % int2)) triple3) -> (rule8 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Anne is not nice.
("Anne" "is" "nice" "-")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule2 % int3))) -> (rule8 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3