Anne is quiet. Erin is young. Gary is red. All red things are young. All kind things are furry. All quiet, kind things are furry. If something is red and not blue then it is not furry. All red things are not furry. If something is furry and not nice then it is quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is red.
("Gary" "is" "red" "+")
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
All quiet, kind things are furry.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If something is red and not blue then it is not furry.
((("something" "is" "red" "+") ("something" "is" "blue" "~")) -> ("something" "is" "furry" "-"))
All red things are not furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "-"))
If something is furry and not nice then it is quiet.
((("something" "is" "furry" "+") ("something" "is" "nice" "~")) -> ("something" "is" "quiet" "+"))
Gary is red.
True
1
proof
[(triple3)]
("Gary" "is" "red" "+")
triple3
Gary is not red.
False
1
inv-proof
[(triple3)]
("Gary" "is" "red" "-")
triple3
Gary is young.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "young" "+")
((triple3) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
False
2
inv-proof
[(((triple3) -> rule5))]
("Gary" "is" "furry" "+")
((triple3) -> (rule5 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "quiet" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Anne is quiet.[(triple1)] Erin is young.[(triple2)] Gary is red.[(triple3)] @1: Gary is not furry.[(((triple3) -> rule5))] Gary is young.[(((triple3) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Gary is not furry.
("Gary" "is" "furry" "-")
((triple3) -> (rule5 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple3) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1