Erin is blue. Gary is kind. Gary is white. Quiet things are smart. If something is blue then it is green. All kind, white things are not quiet. Smart things are quiet. If something is green and not blue then it is quiet. If Erin is kind and Erin is not white then Erin is smart. If Gary is kind and Gary is rough then Gary is smart. If Gary is quiet and Gary is blue then Gary is white.
Erin is blue.
("Erin" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is white.
("Gary" "is" "white" "+")
Quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
All kind, white things are not quiet.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "-"))
Smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is green and not blue then it is quiet.
((("something" "is" "green" "+") ("something" "is" "blue" "~")) -> ("something" "is" "quiet" "+"))
If Erin is kind and Erin is not white then Erin is smart.
((("Erin" "is" "kind" "+") ("Erin" "is" "white" "~")) -> ("Erin" "is" "smart" "+"))
If Gary is kind and Gary is rough then Gary is smart.
((("Gary" "is" "kind" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "smart" "+"))
If Gary is quiet and Gary is blue then Gary is white.
((("Gary" "is" "quiet" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "white" "+"))
Gary is kind.
True
1
proof
[(triple2)]
("Gary" "is" "kind" "+")
triple2
Gary is not white.
False
1
inv-proof
[(triple3)]
("Gary" "is" "white" "-")
triple3
Gary is not quiet.
True
3
proof
[(((triple2 triple3) -> rule3))]
("Gary" "is" "quiet" "-")
((triple2 triple3) -> (rule3 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is quiet.
False
3
inv-proof
[(((triple2 triple3) -> rule3))]
("Gary" "is" "quiet" "+")
((triple2 triple3) -> (rule3 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "green" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Erin is blue.[(triple1)] Gary is kind.[(triple2)] Gary is white.[(triple3)] @1: Erin is green.[(((triple1) -> rule2))] Gary is not quiet.[(((triple2 triple3) -> rule3))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
((triple1) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
((triple2 triple3) -> (rule3 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1