Erin is cold. Erin is furry. Erin is red. Erin is rough. Gary is cold. Gary is furry. Gary is rough. Kind things are cold. If something is kind and furry then it is blue. Cold things are furry. If something is cold and kind then it is nice. If something is kind and cold then it is rough. Nice things are rough. If Gary is kind then Gary is nice. If Gary is kind and Gary is red then Gary is rough.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something is kind and furry then it is blue.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is cold and kind then it is nice.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is kind and cold then it is rough.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If Gary is kind then Gary is nice.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "nice" "+"))
If Gary is kind and Gary is red then Gary is rough.
((("Gary" "is" "kind" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "rough" "+"))
Gary is furry.
True
1
proof
[(triple6 OR ((triple5) -> rule3))]
("Gary" "is" "furry" "+")
triple6
((triple5) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Erin is not red.
False
1
inv-proof
[(triple3)]
("Erin" "is" "red" "-")
triple3
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Erin is cold.[(triple1)] Erin is furry.[(triple2 OR ((triple1) -> rule3))] Erin is red.[(triple3)] Erin is rough.[(triple4)] Gary is cold.[(triple5)] Gary is furry.[(triple6 OR ((triple5) -> rule3))] Gary is rough.[(triple7)]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
((triple1) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
((triple5) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple7