The rabbit is red. All blue things are red. Red, young things are cold. All young, red things are cold. All rough, red things are young. Cold things are rough. Cold things are young. If something is blue then it is young. If something is young and blue then it is red.
The rabbit is red.
("rabbit" "is" "red" "+")
All blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Red, young things are cold.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All young, red things are cold.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
All rough, red things are young.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is blue then it is young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is young and blue then it is red.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
The rabbit is red.
True
1
proof
[(triple1)]
("rabbit" "is" "red" "+")
triple1
The rabbit is not red.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "red" "-")
triple1
The rabbit is not cold.
Unknown
inv-rconc
[@5: The rabbit is cold.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule5 <- rule3 <- rule6 <- FAIL)]]
("rabbit" "is" "cold" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
@0: The rabbit is red.[(triple1)]
The rabbit is red.
("rabbit" "is" "red" "+")
triple1