The mouse is kind. The mouse is nice. The rabbit likes the mouse. If something visits the mouse and the mouse is red then the mouse likes the rabbit. If the mouse eats the rabbit and the rabbit eats the mouse then the rabbit is nice.
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
If something visits the mouse and the mouse is red then the mouse likes the rabbit.
((("something" "visits" "mouse" "+") ("mouse" "is" "red" "+")) -> ("mouse" "likes" "rabbit" "+"))
If the mouse eats the rabbit and the rabbit eats the mouse then the rabbit is nice.
((("mouse" "eats" "rabbit" "+") ("rabbit" "eats" "mouse" "+")) -> ("rabbit" "is" "nice" "+"))
The rabbit likes the mouse.
True
1
proof
[(triple3)]
("rabbit" "likes" "mouse" "+")
triple3
The rabbit does not like the mouse.
False
1
inv-proof
[(triple3)]
("rabbit" "likes" "mouse" "-")
triple3
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "nice" "-")
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 nice.[(triple2)] The rabbit likes the mouse.[(triple3)]
The mouse is kind.
("mouse" "is" "kind" "+")
triple1
The mouse is nice.
("mouse" "is" "nice" "+")
triple2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple3