The bald eagle likes the dog. The cat likes the dog. The dog eats the bald eagle. The lion likes the bald eagle. If something is green then it likes the lion. If something sees the bald eagle and the bald eagle sees the lion then it eats the bald eagle. If something likes the bald eagle then it eats the cat. If something sees the cat then it eats the lion. If something eats the bald eagle then it likes the dog. If the dog is round then the dog sees the bald eagle.
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
The lion likes the bald eagle.
("lion" "likes" "bald eagle" "+")
If something is green then it likes the lion.
((("something" "is" "green" "+")) -> ("something" "likes" "lion" "+"))
If something sees the bald eagle and the bald eagle sees the lion then it eats the bald eagle.
((("something" "sees" "bald eagle" "+") ("bald eagle" "sees" "lion" "+")) -> ("something" "eats" "bald eagle" "+"))
If something likes the bald eagle then it eats the cat.
((("something" "likes" "bald eagle" "+")) -> ("something" "eats" "cat" "+"))
If something sees the cat then it eats the lion.
((("something" "sees" "cat" "+")) -> ("something" "eats" "lion" "+"))
If something eats the bald eagle then it likes the dog.
((("something" "eats" "bald eagle" "+")) -> ("something" "likes" "dog" "+"))
If the dog is round then the dog sees the bald eagle.
((("dog" "is" "round" "+")) -> ("dog" "sees" "bald eagle" "+"))
The lion likes the bald eagle.
True
1
proof
[(triple4)]
("lion" "likes" "bald eagle" "+")
triple4
The dog does not eat the bald eagle.
False
1
inv-proof
[(triple3)]
("dog" "eats" "bald eagle" "-")
triple3
The lion eats the cat.
True
2
proof
[(((triple4) -> rule3))]
("lion" "eats" "cat" "+")
((triple4) -> (rule3 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The dog does not like the dog.
False
2
inv-proof
[(((triple3) -> rule5))]
("dog" "likes" "dog" "-")
((triple3) -> (rule5 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog does not eat the cat.
Unknown
inv-rconc
[@1: The dog eats the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "eats" "cat" "-")
The cat eats the cat.
Unknown
rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "eats" "cat" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The cat eats the dog.
Unknown
random
[@0: The cat eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "dog" "+")
@0: The bald eagle likes the dog.[(triple1)] The cat likes the dog.[(triple2)] The dog eats the bald eagle.[(triple3)] The lion likes the bald eagle.[(triple4)] @1: The dog likes the dog.[(((triple3) -> rule5))] The lion eats the cat.[(((triple4) -> rule3))]
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
triple1
The cat likes the dog.
("cat" "likes" "dog" "+")
triple2
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
triple3
The lion likes the bald eagle.
("lion" "likes" "bald eagle" "+")
triple4
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple3) -> (rule5 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
((triple4) -> (rule3 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1