The bald eagle eats the rabbit. The cow is green. The mouse likes the bald eagle. The rabbit needs the mouse. If something eats the bald eagle then it needs the mouse. If something is green then it eats the bald eagle. If the cow eats the rabbit and the cow eats the mouse then the cow needs the bald eagle. If something needs the bald eagle and the bald eagle is round then it is kind. If something likes the bald eagle then it eats the bald eagle. All round things are young.
The bald eagle eats the rabbit.
("bald eagle" "eats" "rabbit" "+")
The cow is green.
("cow" "is" "green" "+")
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If something eats the bald eagle then it needs the mouse.
((("something" "eats" "bald eagle" "+")) -> ("something" "needs" "mouse" "+"))
If something is green then it eats the bald eagle.
((("something" "is" "green" "+")) -> ("something" "eats" "bald eagle" "+"))
If the cow eats the rabbit and the cow eats the mouse then the cow needs the bald eagle.
((("cow" "eats" "rabbit" "+") ("cow" "eats" "mouse" "+")) -> ("cow" "needs" "bald eagle" "+"))
If something needs the bald eagle and the bald eagle is round then it is kind.
((("something" "needs" "bald eagle" "+") ("bald eagle" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something likes the bald eagle then it eats the bald eagle.
((("something" "likes" "bald eagle" "+")) -> ("something" "eats" "bald eagle" "+"))
All round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
The bald eagle eats the rabbit.
True
1
proof
[(triple1)]
("bald eagle" "eats" "rabbit" "+")
triple1
The rabbit does not need the mouse.
False
1
inv-proof
[(triple4)]
("rabbit" "needs" "mouse" "-")
triple4
The mouse eats the bald eagle.
True
2
proof
[(((triple3) -> rule5))]
("mouse" "eats" "bald eagle" "+")
((triple3) -> (rule5 % int1))
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
int1
The mouse does not eat the bald eagle.
False
2
inv-proof
[(((triple3) -> rule5))]
("mouse" "eats" "bald eagle" "-")
((triple3) -> (rule5 % int1))
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
int1
The mouse needs the mouse.
True
3
proof
[(((((triple3) -> rule5)) -> rule1))]
("mouse" "needs" "mouse" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
int2
The cow does not need the mouse.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("cow" "needs" "mouse" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
int2
The bald eagle is not young.
Unknown
inv-rconc
[@1: The bald eagle is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "is" "young" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "young" "+")
The bald eagle is not kind.
Unknown
inv-rconc
[@1: The bald eagle is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "is" "kind" "-")
The mouse needs the bald eagle.
Unknown
random
[@0: The mouse needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bald eagle" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit likes the mouse.
Unknown
random
[@0: The rabbit likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "mouse" "+")
@0: The bald eagle eats the rabbit.[(triple1)] The cow is green.[(triple2)] The mouse likes the bald eagle.[(triple3)] The rabbit needs the mouse.[(triple4)] @1: The cow eats the bald eagle.[(((triple2) -> rule2))] The mouse eats the bald eagle.[(((triple3) -> rule5))] @2: The cow needs the mouse.[(((((triple2) -> rule2)) -> rule1))] The mouse needs the mouse.[(((((triple3) -> rule5)) -> rule1))]
The bald eagle eats the rabbit.
("bald eagle" "eats" "rabbit" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
triple3
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple4
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
((triple2) -> (rule2 % int1))
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
int1
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
((triple3) -> (rule5 % int1))
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
int2