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