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