The dog is nice. The dog visits the tiger. The lion does not chase the tiger. The lion is rough. The lion is young. The rabbit is red. The rabbit likes the dog. The rabbit likes the lion. The tiger is rough. The tiger likes the lion. If something visits the rabbit and the rabbit visits the dog then the dog visits the rabbit. If the lion visits the tiger and the lion is not nice then the lion does not like the rabbit. If something visits the dog and it does not like the lion then the dog is rough. If something likes the rabbit then the rabbit chases the dog. If something visits the lion then the lion likes the dog. If the rabbit likes the lion and the lion visits the rabbit then the lion is rough. Rough things are not kind. If something visits the dog and the dog is kind then it is not red.
The dog is nice.
("dog" "is" "nice" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The lion does not chase the tiger.
("lion" "chases" "tiger" "-")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If something visits the rabbit and the rabbit visits the dog then the dog visits the rabbit.
((("something" "visits" "rabbit" "+") ("rabbit" "visits" "dog" "+")) -> ("dog" "visits" "rabbit" "+"))
If the lion visits the tiger and the lion is not nice then the lion does not like the rabbit.
((("lion" "visits" "tiger" "+") ("lion" "is" "nice" "~")) -> ("lion" "likes" "rabbit" "-"))
If something visits the dog and it does not like the lion then the dog is rough.
((("something" "visits" "dog" "+") ("something" "likes" "lion" "~")) -> ("dog" "is" "rough" "+"))
If something likes the rabbit then the rabbit chases the dog.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "chases" "dog" "+"))
If something visits the lion then the lion likes the dog.
((("something" "visits" "lion" "+")) -> ("lion" "likes" "dog" "+"))
If the rabbit likes the lion and the lion visits the rabbit then the lion is rough.
((("rabbit" "likes" "lion" "+") ("lion" "visits" "rabbit" "+")) -> ("lion" "is" "rough" "+"))
Rough things are not kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "-"))
If something visits the dog and the dog is kind then it is not red.
((("something" "visits" "dog" "+") ("dog" "is" "kind" "+")) -> ("something" "is" "red" "-"))
The lion is young.
True
1
proof
[(triple5)]
("lion" "is" "young" "+")
triple5
The rabbit is not red.
False
1
inv-proof
[(triple6)]
("rabbit" "is" "red" "-")
triple6
The rabbit does not chase the dog.
Unknown
inv-rconc
[@1: The rabbit chases the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "chases" "dog" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
@0: The dog is nice.[(triple1)] The dog visits the tiger.[(triple2)] The lion does not chase the tiger.[(triple3)] The lion is rough.[(triple4)] The lion is young.[(triple5)] The rabbit is red.[(triple6)] The rabbit likes the dog.[(triple7)] The rabbit likes the lion.[(triple8)] The tiger is rough.[(triple9)] The tiger likes the lion.[(triple10)] @1: The lion is not kind.[(((triple4) -> rule7))] The tiger is not kind.[(((triple9) -> rule7))]
The dog is nice.
("dog" "is" "nice" "+")
triple1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple2
The lion does not chase the tiger.
("lion" "chases" "tiger" "-")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The rabbit is red.
("rabbit" "is" "red" "+")
triple6
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple7
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple10
The lion is not kind.
("lion" "is" "kind" "-")
((triple4) -> (rule7 % int1))
The lion is not kind.
("lion" "is" "kind" "-")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
((triple9) -> (rule7 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1