The bald eagle is green. The cow likes the mouse. The mouse likes the bald eagle. The squirrel is green. All red people are kind. If the bald eagle is kind then the bald eagle sees the cow. If the squirrel is green then the squirrel likes the bald eagle. If someone likes the squirrel then they are nice. If someone sees the mouse and they are red then they are green. If someone needs the cow then they like the bald eagle.
The bald eagle is green.
("bald eagle" "is" "green" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If the bald eagle is kind then the bald eagle sees the cow.
((("bald eagle" "is" "kind" "+")) -> ("bald eagle" "sees" "cow" "+"))
If the squirrel is green then the squirrel likes the bald eagle.
((("squirrel" "is" "green" "+")) -> ("squirrel" "likes" "bald eagle" "+"))
If someone likes the squirrel then they are nice.
((("someone" "likes" "squirrel" "+")) -> ("someone" "is" "nice" "+"))
If someone sees the mouse and they are red then they are green.
((("someone" "sees" "mouse" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone needs the cow then they like the bald eagle.
((("someone" "needs" "cow" "+")) -> ("someone" "likes" "bald eagle" "+"))
The cow likes the mouse.
True
1
proof
[(triple2)]
("cow" "likes" "mouse" "+")
triple2
The mouse does not like the bald eagle.
False
1
inv-proof
[(triple3)]
("mouse" "likes" "bald eagle" "-")
triple3
The squirrel likes the bald eagle.
True
2
proof
[(((triple4) -> rule3))]
("squirrel" "likes" "bald eagle" "+")
((triple4) -> (rule3 % int1))
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int1
The squirrel does not like the bald eagle.
False
2
inv-proof
[(((triple4) -> rule3))]
("squirrel" "likes" "bald eagle" "-")
((triple4) -> (rule3 % int1))
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int1
The cow is not kind.
Unknown
inv-rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "kind" "-")
The bald eagle is kind.
Unknown
rconc
[@1: The bald eagle is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "kind" "+")
The cow does not see the squirrel.
Unknown
inv-random
[@0: The cow sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The bald eagle is green.[(triple1)] The cow likes the mouse.[(triple2)] The mouse likes the bald eagle.[(triple3)] The squirrel is green.[(triple4)] @1: The squirrel likes the bald eagle.[(((triple4) -> rule3))]
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple2
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
triple3
The squirrel is green.
("squirrel" "is" "green" "+")
triple4
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
((triple4) -> (rule3 % int1))
The squirrel likes the bald eagle.
("squirrel" "likes" "bald eagle" "+")
int1