The bald eagle visits the cow. The cat sees the cow. The cow chases the cat. The mouse sees the cat. If someone sees the bald eagle then they are red. If someone visits the mouse then the mouse visits the cat. If the bald eagle sees the cow then the bald eagle visits the cow.
The bald eagle visits the cow.
("bald eagle" "visits" "cow" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If someone sees the bald eagle then they are red.
((("someone" "sees" "bald eagle" "+")) -> ("someone" "is" "red" "+"))
If someone visits the mouse then the mouse visits the cat.
((("someone" "visits" "mouse" "+")) -> ("mouse" "visits" "cat" "+"))
If the bald eagle sees the cow then the bald eagle visits the cow.
((("bald eagle" "sees" "cow" "+")) -> ("bald eagle" "visits" "cow" "+"))
The mouse sees the cat.
True
1
proof
[(triple4)]
("mouse" "sees" "cat" "+")
triple4
The cow does not chase the cat.
False
1
inv-proof
[(triple3)]
("cow" "chases" "cat" "-")
triple3
The bald eagle is not red.
Unknown
inv-rconc
[@1: The bald eagle is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "red" "-")
The cat chases the bald eagle.
Unknown
random
[@0: The cat chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "bald eagle" "+")
@0: The bald eagle visits the cow.[(triple1)] The cat sees the cow.[(triple2)] The cow chases the cat.[(triple3)] The mouse sees the cat.[(triple4)]
The bald eagle visits the cow.
("bald eagle" "visits" "cow" "+")
triple1
The cat sees the cow.
("cat" "sees" "cow" "+")
triple2
The cow chases the cat.
("cow" "chases" "cat" "+")
triple3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple4