Gary is cold. Gary is kind. Gary is white. All rough things are kind. All cold, kind things are white. If Gary is white then Gary is red. All smart things are kind. All quiet, red things are smart. All quiet things are white.
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is white.
("Gary" "is" "white" "+")
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All cold, kind things are white.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If Gary is white then Gary is red.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "red" "+"))
All smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
All quiet, red things are smart.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Gary is white.
True
1
proof
[(triple3 OR ((triple1 triple2) -> rule2))]
("Gary" "is" "white" "+")
triple3
((triple1 triple2) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
1
inv-proof
[(triple3 OR ((triple1 triple2) -> rule2))]
("Gary" "is" "white" "-")
triple3
((triple1 triple2) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Gary is cold.[(triple1)] Gary is kind.[(triple2)] Gary is white.[(triple3 OR ((triple1 triple2) -> rule2))] @1: Gary is red.[(((triple3) -> rule3) OR ((((triple1 triple2) -> rule2)) -> rule3))]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
((triple1 triple2) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2