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