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