Charlie is kind. Gary is blue. If something is cold then it is red. All rough, red things are blue. All kind, rough things are red. Cold, blue things are big. If something is cold and blue then it is rough. Cold, big things are furry.
Charlie is kind.
("Charlie" "is" "kind" "+")
Gary is blue.
("Gary" "is" "blue" "+")
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
All rough, red things are blue.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
All kind, rough things are red.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
Cold, blue things are big.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is cold and blue then it is rough.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Cold, big things are furry.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Gary is blue.
True
1
proof
[(triple2)]
("Gary" "is" "blue" "+")
triple2
Gary is not blue.
False
1
inv-proof
[(triple2)]
("Gary" "is" "blue" "-")
triple2
Charlie is not red.
Unknown
inv-rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Charlie" "is" "red" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Charlie is kind.[(triple1)] Gary is blue.[(triple2)]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2