The mouse is kind. All green, red things are young. If something is kind and blue then it is green. All red things are kind. All red things are young. All red things are blue. Blue things are young.
The mouse is kind.
("mouse" "is" "kind" "+")
All green, red things are young.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is kind and blue then it is green.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
The mouse is kind.
True
1
proof
[(triple1)]
("mouse" "is" "kind" "+")
triple1
The mouse is not kind.
False
1
inv-proof
[(triple1)]
("mouse" "is" "kind" "-")
triple1
The mouse is not blue.
Unknown
inv-rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "blue" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The mouse is kind.[(triple1)]
The mouse is kind.
("mouse" "is" "kind" "+")
triple1