Erin is green. Gary is kind. All smart, rough things are kind. If something is furry then it is green. If Gary is smart and Gary is furry then Gary is kind. If something is kind and smart then it is green. Red things are smart. If Erin is smart then Erin is cold. All red things are rough. Kind things are green.
Erin is green.
("Erin" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
All smart, rough things are kind.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is furry then it is green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If Gary is smart and Gary is furry then Gary is kind.
((("Gary" "is" "smart" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "kind" "+"))
If something is kind and smart then it is green.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Erin is smart then Erin is cold.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "cold" "+"))
All red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Gary is kind.
True
1
proof
[(triple2)]
("Gary" "is" "kind" "+")
triple2
Gary is not kind.
False
1
inv-proof
[(triple2)]
("Gary" "is" "kind" "-")
triple2
Gary is green.
True
2
proof
[(((triple2) -> rule8))]
("Gary" "is" "green" "+")
((triple2) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple2) -> rule8))]
("Gary" "is" "green" "-")
((triple2) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is cold.
Unknown
rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Erin" "is" "cold" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Erin is green.[(triple1)] Gary is kind.[(triple2)] @1: Gary is green.[(((triple2) -> rule8))]
Erin is green.
("Erin" "is" "green" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
((triple2) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1