The bald eagle visits the cat. The cat eats the cow. The cow needs the bald eagle. The mouse eats the cat. If someone eats the cow and the cow does not need the mouse then they eat the cat. If someone eats the cow then they eat the bald eagle. If someone eats the bald eagle then the bald eagle eats the cow.
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
The cat eats the cow.
("cat" "eats" "cow" "+")
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
If someone eats the cow and the cow does not need the mouse then they eat the cat.
((("someone" "eats" "cow" "+") ("cow" "needs" "mouse" "~")) -> ("someone" "eats" "cat" "+"))
If someone eats the cow then they eat the bald eagle.
((("someone" "eats" "cow" "+")) -> ("someone" "eats" "bald eagle" "+"))
If someone eats the bald eagle then the bald eagle eats the cow.
((("someone" "eats" "bald eagle" "+")) -> ("bald eagle" "eats" "cow" "+"))
The bald eagle visits the cat.
True
1
proof
[(triple1)]
("bald eagle" "visits" "cat" "+")
triple1
The mouse does not eat the cat.
False
1
inv-proof
[(triple4)]
("mouse" "eats" "cat" "-")
triple4
The cat eats the bald eagle.
True
2
proof
[(((triple2) -> rule2))]
("cat" "eats" "bald eagle" "+")
((triple2) -> (rule2 % int1))
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int1
The cat does not eat the bald eagle.
False
2
inv-proof
[(((triple2) -> rule2))]
("cat" "eats" "bald eagle" "-")
((triple2) -> (rule2 % int1))
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int1
The bald eagle eats the cow.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("bald eagle" "eats" "cow" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
int1
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int2
The bald eagle does not eat the cow.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("bald eagle" "eats" "cow" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
int1
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int2
The bald eagle eats the bald eagle.
True
4
proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule2))]
("bald eagle" "eats" "bald eagle" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bald eagle eats the bald eagle.
("bald eagle" "eats" "bald eagle" "+")
int1
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
int2
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int3
The bald eagle does not eat the bald eagle.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule2))]
("bald eagle" "eats" "bald eagle" "-")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bald eagle eats the bald eagle.
("bald eagle" "eats" "bald eagle" "+")
int1
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
int2
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int3
The cow does not eat the cat.
Unknown
inv-rconc
[@1: The cow eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "eats" "cat" "-")
The mouse eats the bald eagle.
Unknown
rconc
[@1: The mouse eats the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "eats" "bald eagle" "+")
The bald eagle does not eat the cat.
Unknown
inv-rconc
[@1: The bald eagle eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "eats" "cat" "-")
The cat eats the cat.
Unknown
rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "cat" "+")
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
The cat does not visit the mouse.
Unknown
inv-random
[@0: The cat visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "mouse" "-")
The mouse eats the cow.
Unknown
random
[@0: The mouse eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cow" "+")
@0: The bald eagle visits the cat.[(triple1)] The cat eats the cow.[(triple2)] The cow needs the bald eagle.[(triple3)] The mouse eats the cat.[(triple4)] @1: The cat eats the bald eagle.[(((triple2) -> rule2))] @2: The bald eagle eats the cow.[(((((triple2) -> rule2)) -> rule3))] @3: The bald eagle eats the bald eagle.[(((((((triple2) -> rule2)) -> rule3)) -> rule2))]
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
triple1
The cat eats the cow.
("cat" "eats" "cow" "+")
triple2
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
triple3
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple4
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
((triple2) -> (rule2 % int1))
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int1
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
int1
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int2
The bald eagle eats the bald eagle.
("bald eagle" "eats" "bald eagle" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bald eagle eats the bald eagle.
("bald eagle" "eats" "bald eagle" "+")
int1
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
int2
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int3