The cat likes the mouse. The lion is rough. The mouse likes the lion. If the mouse is rough and the mouse is blue then the mouse sees the cat. If someone likes the lion then they like the mouse. If someone is round and they like the mouse then the mouse needs the lion.
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The lion is rough.
("lion" "is" "rough" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
If the mouse is rough and the mouse is blue then the mouse sees the cat.
((("mouse" "is" "rough" "+") ("mouse" "is" "blue" "+")) -> ("mouse" "sees" "cat" "+"))
If someone likes the lion then they like the mouse.
((("someone" "likes" "lion" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is round and they like the mouse then the mouse needs the lion.
((("someone" "is" "round" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "needs" "lion" "+"))
The cat likes the mouse.
True
1
proof
[(triple1)]
("cat" "likes" "mouse" "+")
triple1
The mouse does not like the lion.
False
1
inv-proof
[(triple3)]
("mouse" "likes" "lion" "-")
triple3
The mouse likes the mouse.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "likes" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not like the mouse.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "likes" "mouse" "-")
((triple3) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not see the cat.
Unknown
inv-rconc
[@1: The mouse sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "cat" "-")
The lion likes the mouse.
Unknown
rconc
[@1: The lion likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "likes" "mouse" "+")
The lion does not see the mouse.
Unknown
inv-random
[@0: The lion sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "mouse" "-")
The mouse needs the cat.
Unknown
random
[@0: The mouse needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cat" "+")
@0: The cat likes the mouse.[(triple1)] The lion is rough.[(triple2)] The mouse likes the lion.[(triple3)] @1: The mouse likes the mouse.[(((triple3) -> rule2))]
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple1
The lion is rough.
("lion" "is" "rough" "+")
triple2
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1