The dog eats the tiger. The lion eats the dog. The lion eats the tiger. The lion is red. The tiger eats the lion. The tiger likes the dog. The tiger likes the lion. If the tiger is red then the tiger is nice. If the lion eats the tiger then the tiger likes the lion. If something eats the lion then the lion likes the tiger. If something is big and it eats the dog then it eats the lion. If something chases the dog and it eats the lion then the dog is red. If something eats the dog then it is rough.
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is red.
("lion" "is" "red" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If the tiger is red then the tiger is nice.
((("tiger" "is" "red" "+")) -> ("tiger" "is" "nice" "+"))
If the lion eats the tiger then the tiger likes the lion.
((("lion" "eats" "tiger" "+")) -> ("tiger" "likes" "lion" "+"))
If something eats the lion then the lion likes the tiger.
((("something" "eats" "lion" "+")) -> ("lion" "likes" "tiger" "+"))
If something is big and it eats the dog then it eats the lion.
((("something" "is" "big" "+") ("something" "eats" "dog" "+")) -> ("something" "eats" "lion" "+"))
If something chases the dog and it eats the lion then the dog is red.
((("something" "chases" "dog" "+") ("something" "eats" "lion" "+")) -> ("dog" "is" "red" "+"))
If something eats the dog then it is rough.
((("something" "eats" "dog" "+")) -> ("something" "is" "rough" "+"))
The tiger eats the lion.
True
1
proof
[(triple5)]
("tiger" "eats" "lion" "+")
triple5
The lion does not eat the dog.
False
1
inv-proof
[(triple2)]
("lion" "eats" "dog" "-")
triple2
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "eats" "lion" "-")
The dog likes the tiger.
Unknown
random
[@0: The dog likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "tiger" "+")
@0: The dog eats the tiger.[(triple1)] The lion eats the dog.[(triple2)] The lion eats the tiger.[(triple3)] The lion is red.[(triple4)] The tiger eats the lion.[(triple5)] The tiger likes the dog.[(triple6)] The tiger likes the lion.[(triple7 OR ((triple3) -> rule2))] @1: The lion is rough.[(((triple2) -> rule6))] The lion likes the tiger.[(((triple5) -> rule3))]
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple1
The lion eats the dog.
("lion" "eats" "dog" "+")
triple2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple3
The lion is red.
("lion" "is" "red" "+")
triple4
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple5
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple6
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple7
((triple3) -> (rule2 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((triple2) -> (rule6 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
((triple5) -> (rule3 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1