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