The bald eagle is green. The bear visits the squirrel. The mouse is young. The squirrel does not see the bear. If someone visits the squirrel and the squirrel does not like the bald eagle then they do not visit the mouse. If someone is green then they see the mouse. If someone sees the mouse then the mouse sees the bald eagle. If the bald eagle is young and the bald eagle is kind then the bald eagle does not like the squirrel. If someone sees the bear and they are young then they are red. If the squirrel is cold and the squirrel visits the bald eagle then the squirrel is green. If someone likes the bald eagle and the bald eagle does not visit the squirrel then the bald eagle likes the mouse. If the bald eagle is kind and the bald eagle does not like the squirrel then the squirrel likes the mouse.
The bald eagle is green.
("bald eagle" "is" "green" "+")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The mouse is young.
("mouse" "is" "young" "+")
The squirrel does not see the bear.
("squirrel" "sees" "bear" "-")
If someone visits the squirrel and the squirrel does not like the bald eagle then they do not visit the mouse.
((("someone" "visits" "squirrel" "+") ("squirrel" "likes" "bald eagle" "~")) -> ("someone" "visits" "mouse" "-"))
If someone is green then they see the mouse.
((("someone" "is" "green" "+")) -> ("someone" "sees" "mouse" "+"))
If someone sees the mouse then the mouse sees the bald eagle.
((("someone" "sees" "mouse" "+")) -> ("mouse" "sees" "bald eagle" "+"))
If the bald eagle is young and the bald eagle is kind then the bald eagle does not like the squirrel.
((("bald eagle" "is" "young" "+") ("bald eagle" "is" "kind" "+")) -> ("bald eagle" "likes" "squirrel" "-"))
If someone sees the bear and they are young then they are red.
((("someone" "sees" "bear" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If the squirrel is cold and the squirrel visits the bald eagle then the squirrel is green.
((("squirrel" "is" "cold" "+") ("squirrel" "visits" "bald eagle" "+")) -> ("squirrel" "is" "green" "+"))
If someone likes the bald eagle and the bald eagle does not visit the squirrel then the bald eagle likes the mouse.
((("someone" "likes" "bald eagle" "+") ("bald eagle" "visits" "squirrel" "~")) -> ("bald eagle" "likes" "mouse" "+"))
If the bald eagle is kind and the bald eagle does not like the squirrel then the squirrel likes the mouse.
((("bald eagle" "is" "kind" "+") ("bald eagle" "likes" "squirrel" "~")) -> ("squirrel" "likes" "mouse" "+"))
The mouse is young.
True
1
proof
[(triple3)]
("mouse" "is" "young" "+")
triple3
The bear does not visit the squirrel.
False
1
inv-proof
[(triple2)]
("bear" "visits" "squirrel" "-")
triple2
The bald eagle sees the mouse.
True
2
proof
[(((triple1) -> rule2))]
("bald eagle" "sees" "mouse" "+")
((triple1) -> (rule2 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The bald eagle does not see the mouse.
False
2
inv-proof
[(((triple1) -> rule2))]
("bald eagle" "sees" "mouse" "-")
((triple1) -> (rule2 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The mouse sees the bald eagle.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("mouse" "sees" "bald eagle" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
int1
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int2
The mouse does not see the bald eagle.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("mouse" "sees" "bald eagle" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
int1
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int2
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "red" "-")
The squirrel is green.
Unknown
rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "green" "+")
The bear does not see the mouse.
Unknown
inv-rconc
[@1: The bear sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "mouse" "-")
The squirrel visits the bald eagle.
Unknown
random
[@0: The squirrel visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "bald eagle" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
@0: The bald eagle is green.[(triple1)] The bear visits the squirrel.[(triple2)] The mouse is young.[(triple3)] The squirrel does not see the bear.[(triple4)] @1: The bald eagle sees the mouse.[(((triple1) -> rule2))] @2: The mouse sees the bald eagle.[(((((triple1) -> rule2)) -> rule3))]
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple2
The mouse is young.
("mouse" "is" "young" "+")
triple3
The squirrel does not see the bear.
("squirrel" "sees" "bear" "-")
triple4
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
((triple1) -> (rule2 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
int1
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int2