The bald eagle does not chase the dog. The bald eagle chases the mouse. The cow chases the dog. The dog chases the cow. The dog likes the mouse. The dog sees the cow. The mouse sees the cow. If someone chases the dog and they do not see the dog then they do not see the mouse. If someone sees the cow then they chase the cow.
The bald eagle does not chase the dog.
("bald eagle" "chases" "dog" "-")
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
The cow chases the dog.
("cow" "chases" "dog" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If someone chases the dog and they do not see the dog then they do not see the mouse.
((("someone" "chases" "dog" "+") ("someone" "sees" "dog" "~")) -> ("someone" "sees" "mouse" "-"))
If someone sees the cow then they chase the cow.
((("someone" "sees" "cow" "+")) -> ("someone" "chases" "cow" "+"))
The cow chases the dog.
True
1
proof
[(triple3)]
("cow" "chases" "dog" "+")
triple3
The dog does not chase the cow.
False
1
inv-proof
[(triple4 OR ((triple6) -> rule2))]
("dog" "chases" "cow" "-")
triple4
((triple6) -> (rule2 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The mouse chases the cow.
True
2
proof
[(((triple7) -> rule2))]
("mouse" "chases" "cow" "+")
((triple7) -> (rule2 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The mouse does not chase the cow.
False
2
inv-proof
[(((triple7) -> rule2))]
("mouse" "chases" "cow" "-")
((triple7) -> (rule2 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The bald eagle does not chase the cow.
Unknown
inv-rconc
[@1: The bald eagle chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "chases" "cow" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "chases" "cow" "+")
The bald eagle does not see the cow.
Unknown
inv-random
[@0: The bald eagle sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "cow" "-")
The bald eagle is blue.
Unknown
random
[@0: The bald eagle is blue.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "blue" "+")
@0: The bald eagle chases the mouse.[(triple2)] The bald eagle does not chase the dog.[(triple1)] The cow chases the dog.[(triple3)] The dog chases the cow.[(triple4 OR ((triple6) -> rule2))] The dog likes the mouse.[(triple5)] The dog sees the cow.[(triple6)] The mouse sees the cow.[(triple7)] @1: The mouse chases the cow.[(((triple7) -> rule2))]
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
triple2
The bald eagle does not chase the dog.
("bald eagle" "chases" "dog" "-")
triple1
The cow chases the dog.
("cow" "chases" "dog" "+")
triple3
The dog chases the cow.
("dog" "chases" "cow" "+")
triple4
((triple6) -> (rule2 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple5
The dog sees the cow.
("dog" "sees" "cow" "+")
triple6
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple7
The mouse chases the cow.
("mouse" "chases" "cow" "+")
((triple7) -> (rule2 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1