The cow likes the lion. The lion is red. The tiger visits the lion. If something visits the cow and the cow does not eat the tiger then the tiger eats the cow. If the lion likes the cow and the lion does not like the tiger then the lion visits the cow. If something visits the tiger then the tiger likes the cow.
The cow likes the lion.
("cow" "likes" "lion" "+")
The lion is red.
("lion" "is" "red" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something visits the cow and the cow does not eat the tiger then the tiger eats the cow.
((("something" "visits" "cow" "+") ("cow" "eats" "tiger" "~")) -> ("tiger" "eats" "cow" "+"))
If the lion likes the cow and the lion does not like the tiger then the lion visits the cow.
((("lion" "likes" "cow" "+") ("lion" "likes" "tiger" "~")) -> ("lion" "visits" "cow" "+"))
If something visits the tiger then the tiger likes the cow.
((("something" "visits" "tiger" "+")) -> ("tiger" "likes" "cow" "+"))
The tiger visits the lion.
True
1
proof
[(triple3)]
("tiger" "visits" "lion" "+")
triple3
The cow does not like the lion.
False
1
inv-proof
[(triple1)]
("cow" "likes" "lion" "-")
triple1
The tiger does not like the cow.
Unknown
inv-rconc
[@1: The tiger likes the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "cow" "-")
The cow visits the tiger.
Unknown
random
[@0: The cow visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "tiger" "+")
@0: The cow likes the lion.[(triple1)] The lion is red.[(triple2)] The tiger visits the lion.[(triple3)]
The cow likes the lion.
("cow" "likes" "lion" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple3