The cat does not like the lion. The lion visits the tiger. The mouse likes the tiger. The tiger does not need the lion. If the cat is rough and the cat needs the tiger then the cat likes the tiger. If someone visits the mouse and they are kind then they need the tiger. If the mouse visits the cat and the cat likes the tiger then the mouse needs the lion.
The cat does not like the lion.
("cat" "likes" "lion" "-")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
If the cat is rough and the cat needs the tiger then the cat likes the tiger.
((("cat" "is" "rough" "+") ("cat" "needs" "tiger" "+")) -> ("cat" "likes" "tiger" "+"))
If someone visits the mouse and they are kind then they need the tiger.
((("someone" "visits" "mouse" "+") ("someone" "is" "kind" "+")) -> ("someone" "needs" "tiger" "+"))
If the mouse visits the cat and the cat likes the tiger then the mouse needs the lion.
((("mouse" "visits" "cat" "+") ("cat" "likes" "tiger" "+")) -> ("mouse" "needs" "lion" "+"))
The lion visits the tiger.
True
1
proof
[(triple2)]
("lion" "visits" "tiger" "+")
triple2
The cat likes the lion.
False
1
inv-proof
[(triple1)]
("cat" "likes" "lion" "+")
triple1
The cat does not like the tiger.
Unknown
inv-rconc
[@1: The cat likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "tiger" "-")
The lion likes the cat.
Unknown
random
[@0: The lion likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cat" "+")
@0: The cat does not like the lion.[(triple1)] The lion visits the tiger.[(triple2)] The mouse likes the tiger.[(triple3)] The tiger does not need the lion.[(triple4)]
The cat does not like the lion.
("cat" "likes" "lion" "-")
triple1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple3
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
triple4