The cat eats the lion. The cat likes the dog. The cow likes the lion. The dog needs the cow. The lion eats the cat. The lion likes the dog. The lion needs the cat. If someone eats the cat then they eat the lion.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
If someone eats the cat then they eat the lion.
((("someone" "eats" "cat" "+")) -> ("someone" "eats" "lion" "+"))
The dog needs the cow.
True
1
proof
[(triple4)]
("dog" "needs" "cow" "+")
triple4
The cow does not like the lion.
False
1
inv-proof
[(triple3)]
("cow" "likes" "lion" "-")
triple3
The dog does not eat the lion.
Unknown
inv-rconc
[@1: The dog eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "eats" "lion" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
@0: The cat eats the lion.[(triple1)] The cat likes the dog.[(triple2)] The cow likes the lion.[(triple3)] The dog needs the cow.[(triple4)] The lion eats the cat.[(triple5)] The lion likes the dog.[(triple6)] The lion needs the cat.[(triple7)] @1: The lion eats the lion.[(((triple5) -> rule1))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat likes the dog.
("cat" "likes" "dog" "+")
triple2
The cow likes the lion.
("cow" "likes" "lion" "+")
triple3
The dog needs the cow.
("dog" "needs" "cow" "+")
triple4
The lion eats the cat.
("lion" "eats" "cat" "+")
triple5
The lion likes the dog.
("lion" "likes" "dog" "+")
triple6
The lion needs the cat.
("lion" "needs" "cat" "+")
triple7
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple5) -> (rule1 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1