The dog is rough. The lion does not visit the dog. The rabbit visits the lion. If something visits the lion then it does not like the rabbit. If something likes the lion and it is nice then the lion does not like the rabbit. If something is nice and it visits the rabbit then it likes the dog.
The dog is rough.
("dog" "is" "rough" "+")
The lion does not visit the dog.
("lion" "visits" "dog" "-")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If something visits the lion then it does not like the rabbit.
((("something" "visits" "lion" "+")) -> ("something" "likes" "rabbit" "-"))
If something likes the lion and it is nice then the lion does not like the rabbit.
((("something" "likes" "lion" "+") ("something" "is" "nice" "+")) -> ("lion" "likes" "rabbit" "-"))
If something is nice and it visits the rabbit then it likes the dog.
((("something" "is" "nice" "+") ("something" "visits" "rabbit" "+")) -> ("something" "likes" "dog" "+"))
The dog is rough.
True
1
proof
[(triple1)]
("dog" "is" "rough" "+")
triple1
The lion visits the dog.
False
1
inv-proof
[(triple2)]
("lion" "visits" "dog" "+")
triple2
The rabbit does not like the rabbit.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "likes" "rabbit" "-")
((triple3) -> (rule1 % int1))
The rabbit does not like the rabbit.
("rabbit" "likes" "rabbit" "-")
int1
The rabbit likes the rabbit.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "likes" "rabbit" "+")
((triple3) -> (rule1 % int1))
The rabbit does not like the rabbit.
("rabbit" "likes" "rabbit" "-")
int1
The rabbit does not like the dog.
Unknown
inv-rconc
[@1: The rabbit likes the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "dog" "-")
The lion likes the dog.
Unknown
rconc
[@1: The lion likes the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "likes" "dog" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The dog likes the rabbit.
Unknown
random
[@0: The dog likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "rabbit" "+")
@0: The dog is rough.[(triple1)] The lion does not visit the dog.[(triple2)] The rabbit visits the lion.[(triple3)] @1: The rabbit does not like the rabbit.[(((triple3) -> rule1))]
The dog is rough.
("dog" "is" "rough" "+")
triple1
The lion does not visit the dog.
("lion" "visits" "dog" "-")
triple2
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple3
The rabbit does not like the rabbit.
("rabbit" "likes" "rabbit" "-")
((triple3) -> (rule1 % int1))
The rabbit does not like the rabbit.
("rabbit" "likes" "rabbit" "-")
int1