The cat chases the lion. The cat is red. The cat likes the lion. The dog chases the cat. The dog chases the lion. The dog eats the lion. The dog is young. The dog likes the cat. The lion chases the rabbit. The lion eats the cat. The lion eats the dog. The lion likes the rabbit. The rabbit chases the cat. The rabbit is young. The rabbit likes the cat. The rabbit likes the dog. If something likes the rabbit and the rabbit eats the lion then the lion eats the cat. If something eats the lion and the lion chases the rabbit then it eats the cat.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
If something likes the rabbit and the rabbit eats the lion then the lion eats the cat.
((("something" "likes" "rabbit" "+") ("rabbit" "eats" "lion" "+")) -> ("lion" "eats" "cat" "+"))
If something eats the lion and the lion chases the rabbit then it eats the cat.
((("something" "eats" "lion" "+") ("lion" "chases" "rabbit" "+")) -> ("something" "eats" "cat" "+"))
The lion eats the cat.
True
1
proof
[(triple10)]
("lion" "eats" "cat" "+")
triple10
The dog does not chase the cat.
False
1
inv-proof
[(triple4)]
("dog" "chases" "cat" "-")
triple4
The rabbit does not eat the cat.
Unknown
inv-rconc
[@1: The rabbit eats the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "eats" "cat" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The cat chases the lion.[(triple1)] The cat is red.[(triple2)] The cat likes the lion.[(triple3)] The dog chases the cat.[(triple4)] The dog chases the lion.[(triple5)] The dog eats the lion.[(triple6)] The dog is young.[(triple7)] The dog likes the cat.[(triple8)] The lion chases the rabbit.[(triple9)] The lion eats the cat.[(triple10)] The lion eats the dog.[(triple11)] The lion likes the rabbit.[(triple12)] The rabbit chases the cat.[(triple13)] The rabbit is young.[(triple14)] The rabbit likes the cat.[(triple15)] The rabbit likes the dog.[(triple16)] @1: The dog eats the cat.[(((triple6 triple9) -> rule2))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cat likes the lion.
("cat" "likes" "lion" "+")
triple3
The dog chases the cat.
("dog" "chases" "cat" "+")
triple4
The dog chases the lion.
("dog" "chases" "lion" "+")
triple5
The dog eats the lion.
("dog" "eats" "lion" "+")
triple6
The dog is young.
("dog" "is" "young" "+")
triple7
The dog likes the cat.
("dog" "likes" "cat" "+")
triple8
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple9
The lion eats the cat.
("lion" "eats" "cat" "+")
triple10
The lion eats the dog.
("lion" "eats" "dog" "+")
triple11
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple12
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple13
The rabbit is young.
("rabbit" "is" "young" "+")
triple14
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple15
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple16
The dog eats the cat.
("dog" "eats" "cat" "+")
((triple6 triple9) -> (rule2 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1