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