The bald eagle is rough. The bald eagle likes the bear. The bear is kind. The bear is young. The bear likes the mouse. The bear visits the bald eagle. The bear visits the squirrel. The mouse eats the bear. The mouse eats the squirrel. The mouse is big. The mouse is kind. The mouse is young. The mouse visits the bald eagle. The mouse visits the bear. The squirrel likes the mouse. If something likes the mouse then the mouse eats the squirrel. If something eats the bald eagle then it is rough. If the mouse eats the squirrel then the squirrel eats the mouse.
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear visits the bald eagle.
("bear" "visits" "bald eagle" "+")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
If something likes the mouse then the mouse eats the squirrel.
((("something" "likes" "mouse" "+")) -> ("mouse" "eats" "squirrel" "+"))
If something eats the bald eagle then it is rough.
((("something" "eats" "bald eagle" "+")) -> ("something" "is" "rough" "+"))
If the mouse eats the squirrel then the squirrel eats the mouse.
((("mouse" "eats" "squirrel" "+")) -> ("squirrel" "eats" "mouse" "+"))
The mouse visits the bear.
True
1
proof
[(triple14)]
("mouse" "visits" "bear" "+")
triple14
The mouse does not eat the bear.
False
1
inv-proof
[(triple8)]
("mouse" "eats" "bear" "-")
triple8
The squirrel eats the mouse.
True
2
proof
[(((triple9) -> rule3) OR ((((triple15) -> rule1)) -> rule3) OR ((((triple5) -> rule1)) -> rule3))]
("squirrel" "eats" "mouse" "+")
((triple9) -> (rule3 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
((((triple15) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The squirrel does not eat the mouse.
False
2
inv-proof
[(((triple9) -> rule3) OR ((((triple15) -> rule1)) -> rule3) OR ((((triple5) -> rule1)) -> rule3))]
("squirrel" "eats" "mouse" "-")
((triple9) -> (rule3 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
((((triple15) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The bear is not rough.
Unknown
inv-rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "rough" "-")
The squirrel is rough.
Unknown
rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "rough" "+")
The bear does not eat the bald eagle.
Unknown
inv-random
[@0: The bear eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bald eagle" "-")
The bear likes the squirrel.
Unknown
random
[@0: The bear likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "squirrel" "+")
@0: The bald eagle is rough.[(triple1)] The bald eagle likes the bear.[(triple2)] The bear is kind.[(triple3)] The bear is young.[(triple4)] The bear likes the mouse.[(triple5)] The bear visits the bald eagle.[(triple6)] The bear visits the squirrel.[(triple7)] The mouse eats the bear.[(triple8)] The mouse eats the squirrel.[(triple9 OR ((triple15) -> rule1) OR ((triple5) -> rule1))] The mouse is big.[(triple10)] The mouse is kind.[(triple11)] The mouse is young.[(triple12)] The mouse visits the bald eagle.[(triple13)] The mouse visits the bear.[(triple14)] The squirrel likes the mouse.[(triple15)] @1: The squirrel eats the mouse.[(((triple9) -> rule3) OR ((((triple15) -> rule1)) -> rule3) OR ((((triple5) -> rule1)) -> rule3))]
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple1
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
triple2
The bear is kind.
("bear" "is" "kind" "+")
triple3
The bear is young.
("bear" "is" "young" "+")
triple4
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple5
The bear visits the bald eagle.
("bear" "visits" "bald eagle" "+")
triple6
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple7
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple8
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple9
((triple15) -> (rule1 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
((triple5) -> (rule1 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
triple11
The mouse is young.
("mouse" "is" "young" "+")
triple12
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
triple13
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple14
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple15
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
((triple9) -> (rule3 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
((((triple15) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2