The cat is rough. The cat likes the dog. The cat likes the lion. The cat likes the rabbit. The cat sees the rabbit. The dog eats the rabbit. The dog sees the cat. The lion is nice. The lion likes the cat. The lion likes the dog. The lion sees the dog. The rabbit likes the dog. If someone likes the lion then they see the dog. If someone is green then they eat the lion. If the lion sees the rabbit then the rabbit sees the lion.
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
If someone likes the lion then they see the dog.
((("someone" "likes" "lion" "+")) -> ("someone" "sees" "dog" "+"))
If someone is green then they eat the lion.
((("someone" "is" "green" "+")) -> ("someone" "eats" "lion" "+"))
If the lion sees the rabbit then the rabbit sees the lion.
((("lion" "sees" "rabbit" "+")) -> ("rabbit" "sees" "lion" "+"))
The cat likes the dog.
True
1
proof
[(triple2)]
("cat" "likes" "dog" "+")
triple2
The cat does not see the rabbit.
False
1
inv-proof
[(triple5)]
("cat" "sees" "rabbit" "-")
triple5
The cat sees the dog.
True
2
proof
[(((triple3) -> rule1))]
("cat" "sees" "dog" "+")
((triple3) -> (rule1 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat does not see the dog.
False
2
inv-proof
[(((triple3) -> rule1))]
("cat" "sees" "dog" "-")
((triple3) -> (rule1 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "dog" "-")
The dog eats the lion.
Unknown
rconc
[@1: The dog eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "lion" "+")
The rabbit does not like the cat.
Unknown
inv-random
[@0: The rabbit likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cat" "-")
The lion eats the cat.
Unknown
random
[@0: The lion eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "cat" "+")
@0: The cat is rough.[(triple1)] The cat likes the dog.[(triple2)] The cat likes the lion.[(triple3)] The cat likes the rabbit.[(triple4)] The cat sees the rabbit.[(triple5)] The dog eats the rabbit.[(triple6)] The dog sees the cat.[(triple7)] The lion is nice.[(triple8)] The lion likes the cat.[(triple9)] The lion likes the dog.[(triple10)] The lion sees the dog.[(triple11)] The rabbit likes the dog.[(triple12)] @1: The cat sees the dog.[(((triple3) -> rule1))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The cat likes the dog.
("cat" "likes" "dog" "+")
triple2
The cat likes the lion.
("cat" "likes" "lion" "+")
triple3
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple4
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple5
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple6
The dog sees the cat.
("dog" "sees" "cat" "+")
triple7
The lion is nice.
("lion" "is" "nice" "+")
triple8
The lion likes the cat.
("lion" "likes" "cat" "+")
triple9
The lion likes the dog.
("lion" "likes" "dog" "+")
triple10
The lion sees the dog.
("lion" "sees" "dog" "+")
triple11
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple12
The cat sees the dog.
("cat" "sees" "dog" "+")
((triple3) -> (rule1 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1