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