The mouse is kind. If something is red then it is blue. If something is rough then it is blue. Round things are blue. All rough things are red. If the mouse is blue then the mouse is rough. If the mouse is blue then the mouse is not kind. If the mouse is not rough and the mouse is not red then the mouse is not kind. If the mouse is rough and the mouse is round then the mouse is not kind.
The mouse is kind.
("mouse" "is" "kind" "+")
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If something is rough then it is blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If the mouse is blue then the mouse is rough.
((("mouse" "is" "blue" "+")) -> ("mouse" "is" "rough" "+"))
If the mouse is blue then the mouse is not kind.
((("mouse" "is" "blue" "+")) -> ("mouse" "is" "kind" "-"))
If the mouse is not rough and the mouse is not red then the mouse is not kind.
((("mouse" "is" "rough" "~") ("mouse" "is" "red" "~")) -> ("mouse" "is" "kind" "-"))
If the mouse is rough and the mouse is round then the mouse is not kind.
((("mouse" "is" "rough" "+") ("mouse" "is" "round" "+")) -> ("mouse" "is" "kind" "-"))
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 rough.
Unknown
inv-rconc
[@3: The mouse is rough.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule4 <- FAIL)]]
("mouse" "is" "rough" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
@0: The mouse is kind.[(triple1)]
The mouse is kind.
("mouse" "is" "kind" "+")
triple1