The cat likes the lion. The lion sees the tiger. The tiger likes the lion. If the tiger likes the lion and the tiger is red then the tiger sees the lion. If something sees the lion and the lion is young then it is young.
The cat likes the lion.
("cat" "likes" "lion" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If the tiger likes the lion and the tiger is red then the tiger sees the lion.
((("tiger" "likes" "lion" "+") ("tiger" "is" "red" "+")) -> ("tiger" "sees" "lion" "+"))
If something sees the lion and the lion is young then it is young.
((("something" "sees" "lion" "+") ("lion" "is" "young" "+")) -> ("something" "is" "young" "+"))
The cat likes the lion.
True
1
proof
[(triple1)]
("cat" "likes" "lion" "+")
triple1
The cat does not like the lion.
False
1
inv-proof
[(triple1)]
("cat" "likes" "lion" "-")
triple1
The tiger does not see the lion.
Unknown
inv-rconc
[@1: The tiger sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "lion" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
@0: The cat likes the lion.[(triple1)] The lion sees the tiger.[(triple2)] The tiger likes the lion.[(triple3)]
The cat likes the lion.
("cat" "likes" "lion" "+")
triple1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple2
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple3