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