The bald eagle sees the dog. The cat is red. The dog sees the cat. The tiger likes the dog. If something sees the cat then it likes the cat. If something visits the cat then it is not red. If something sees the tiger then the tiger is big.
The bald eagle sees the dog.
("bald eagle" "sees" "dog" "+")
The cat is red.
("cat" "is" "red" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
If something sees the cat then it likes the cat.
((("something" "sees" "cat" "+")) -> ("something" "likes" "cat" "+"))
If something visits the cat then it is not red.
((("something" "visits" "cat" "+")) -> ("something" "is" "red" "-"))
If something sees the tiger then the tiger is big.
((("something" "sees" "tiger" "+")) -> ("tiger" "is" "big" "+"))
The tiger likes the dog.
True
1
proof
[(triple4)]
("tiger" "likes" "dog" "+")
triple4
The bald eagle does not see the dog.
False
1
inv-proof
[(triple1)]
("bald eagle" "sees" "dog" "-")
triple1
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "cat" "-")
The dog sees the bald eagle.
Unknown
random
[@0: The dog sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bald eagle" "+")
@0: The bald eagle sees the dog.[(triple1)] The cat is red.[(triple2)] The dog sees the cat.[(triple3)] The tiger likes the dog.[(triple4)] @1: The dog likes the cat.[(((triple3) -> rule1))]
The bald eagle sees the dog.
("bald eagle" "sees" "dog" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The dog sees the cat.
("dog" "sees" "cat" "+")
triple3
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple4
The dog likes the cat.
("dog" "likes" "cat" "+")
((triple3) -> (rule1 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1