The bear eats the mouse. The bear is cold. The bear is nice. The bear is round. The bear likes the squirrel. The bear sees the mouse. The mouse is cold. The mouse likes the bear. The mouse sees the bear. The squirrel is young. The squirrel sees the bear. The squirrel sees the mouse. Round people are nice. If someone sees the bear then the bear likes the mouse. If someone is young and they eat the squirrel then they like the mouse. If someone sees the bear and the bear eats the mouse then the mouse is round. If someone likes the mouse and the mouse is cold then they see the squirrel. If the squirrel sees the mouse and the squirrel eats the mouse then the mouse eats the squirrel.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is round.
("bear" "is" "round" "+")
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone sees the bear then the bear likes the mouse.
((("someone" "sees" "bear" "+")) -> ("bear" "likes" "mouse" "+"))
If someone is young and they eat the squirrel then they like the mouse.
((("someone" "is" "young" "+") ("someone" "eats" "squirrel" "+")) -> ("someone" "likes" "mouse" "+"))
If someone sees the bear and the bear eats the mouse then the mouse is round.
((("someone" "sees" "bear" "+") ("bear" "eats" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If someone likes the mouse and the mouse is cold then they see the squirrel.
((("someone" "likes" "mouse" "+") ("mouse" "is" "cold" "+")) -> ("someone" "sees" "squirrel" "+"))
If the squirrel sees the mouse and the squirrel eats the mouse then the mouse eats the squirrel.
((("squirrel" "sees" "mouse" "+") ("squirrel" "eats" "mouse" "+")) -> ("mouse" "eats" "squirrel" "+"))
The bear is cold.
True
1
proof
[(triple2)]
("bear" "is" "cold" "+")
triple2
The mouse does not like the bear.
False
1
inv-proof
[(triple8)]
("mouse" "likes" "bear" "-")
triple8
The mouse is round.
True
3
proof
[(((triple11 triple1) -> rule4) OR ((triple9 triple1) -> rule4))]
("mouse" "is" "round" "+")
((triple11 triple1) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((triple9 triple1) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is not round.
False
3
inv-proof
[(((triple11 triple1) -> rule4) OR ((triple9 triple1) -> rule4))]
("mouse" "is" "round" "-")
((triple11 triple1) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((triple9 triple1) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The bear sees the squirrel.
True
4
proof
[(((((triple11) -> rule2) triple7) -> rule5) OR ((((triple9) -> rule2) triple7) -> rule5))]
("bear" "sees" "squirrel" "+")
((((triple11) -> (rule2 % int2)) triple7) -> (rule5 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
((((triple9) -> (rule2 % int2)) triple7) -> (rule5 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The bear does not see the squirrel.
False
4
inv-proof
[(((((triple11) -> rule2) triple7) -> rule5) OR ((((triple9) -> rule2) triple7) -> rule5))]
("bear" "sees" "squirrel" "-")
((((triple11) -> (rule2 % int2)) triple7) -> (rule5 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
((((triple9) -> (rule2 % int2)) triple7) -> (rule5 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The squirrel does not like the mouse.
Unknown
inv-rconc
[@1: The squirrel likes the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "likes" "mouse" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The squirrel is not nice.
Unknown
inv-rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "nice" "-")
The bear eats the squirrel.
Unknown
random
[@0: The bear eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "squirrel" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The bear eats the mouse.[(triple1)] The bear is cold.[(triple2)] The bear is nice.[(triple3 OR ((triple4) -> rule1))] The bear is round.[(triple4)] The bear likes the squirrel.[(triple5)] The bear sees the mouse.[(triple6)] The mouse is cold.[(triple7)] The mouse likes the bear.[(triple8)] The mouse sees the bear.[(triple9)] The squirrel is young.[(triple10)] The squirrel sees the bear.[(triple11)] The squirrel sees the mouse.[(triple12)] @1: The bear likes the mouse.[(((triple11) -> rule2) OR ((triple9) -> rule2))] The mouse is round.[(((triple11 triple1) -> rule4) OR ((triple9 triple1) -> rule4))] @2: The bear sees the squirrel.[(((((triple11) -> rule2) triple7) -> rule5) OR ((((triple9) -> rule2) triple7) -> rule5))] The mouse is nice.[(((((triple11 triple1) -> rule4)) -> rule1) OR ((((triple9 triple1) -> rule4)) -> rule1))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple3
((triple4) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is round.
("bear" "is" "round" "+")
triple4
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple5
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple6
The mouse is cold.
("mouse" "is" "cold" "+")
triple7
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple8
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple9
The squirrel is young.
("squirrel" "is" "young" "+")
triple10
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple11
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple12
The bear likes the mouse.
("bear" "likes" "mouse" "+")
((triple11) -> (rule2 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
((triple9) -> (rule2 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple11 triple1) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((triple9 triple1) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
((((triple11) -> (rule2 % int2)) triple7) -> (rule5 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
((((triple9) -> (rule2 % int2)) triple7) -> (rule5 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
((((triple11 triple1) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
((((triple9 triple1) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2