The cat likes the mouse. The mouse does not need the tiger. The tiger eats the cat. If something is nice then it likes the mouse. If the tiger likes the cat and the tiger does not like the mouse then the mouse eats the cat.
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The mouse does not need the tiger.
("mouse" "needs" "tiger" "-")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
If something is nice then it likes the mouse.
((("something" "is" "nice" "+")) -> ("something" "likes" "mouse" "+"))
If the tiger likes the cat and the tiger does not like the mouse then the mouse eats the cat.
((("tiger" "likes" "cat" "+") ("tiger" "likes" "mouse" "~")) -> ("mouse" "eats" "cat" "+"))
The cat likes the mouse.
True
1
proof
[(triple1)]
("cat" "likes" "mouse" "+")
triple1
The mouse needs the tiger.
False
1
inv-proof
[(triple2)]
("mouse" "needs" "tiger" "+")
triple2
The tiger does not like the mouse.
Unknown
inv-rconc
[@1: The tiger likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "likes" "mouse" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat likes the mouse.[(triple1)] The mouse does not need the tiger.[(triple2)] The tiger eats the cat.[(triple3)]
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple1
The mouse does not need the tiger.
("mouse" "needs" "tiger" "-")
triple2
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple3