The bear chases the mouse. The bear likes the mouse. The bear does not like the squirrel. The bear sees the squirrel. The mouse is round. The mouse likes the squirrel. The mouse sees the bear. The mouse sees the squirrel. The squirrel does not chase the mouse. The squirrel is young. The squirrel sees the bear. The squirrel sees the mouse. If the squirrel sees the bear then the bear does not see the mouse. If something sees the bear then it is nice. If something is nice then it chases the bear. If something chases the squirrel then it is big. If the bear sees the squirrel and the squirrel does not like the mouse then the bear likes the mouse. If the squirrel likes the bear and the bear does not see the squirrel then the squirrel chases the mouse. If the squirrel sees the mouse then the mouse is nice. If something sees the bear then it sees the mouse.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear does not like the squirrel.
("bear" "likes" "squirrel" "-")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel does not chase the mouse.
("squirrel" "chases" "mouse" "-")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If the squirrel sees the bear then the bear does not see the mouse.
((("squirrel" "sees" "bear" "+")) -> ("bear" "sees" "mouse" "-"))
If something sees the bear then it is nice.
((("something" "sees" "bear" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it chases the bear.
((("something" "is" "nice" "+")) -> ("something" "chases" "bear" "+"))
If something chases the squirrel then it is big.
((("something" "chases" "squirrel" "+")) -> ("something" "is" "big" "+"))
If the bear sees the squirrel and the squirrel does not like the mouse then the bear likes the mouse.
((("bear" "sees" "squirrel" "+") ("squirrel" "likes" "mouse" "~")) -> ("bear" "likes" "mouse" "+"))
If the squirrel likes the bear and the bear does not see the squirrel then the squirrel chases the mouse.
((("squirrel" "likes" "bear" "+") ("bear" "sees" "squirrel" "~")) -> ("squirrel" "chases" "mouse" "+"))
If the squirrel sees the mouse then the mouse is nice.
((("squirrel" "sees" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
If something sees the bear then it sees the mouse.
((("something" "sees" "bear" "+")) -> ("something" "sees" "mouse" "+"))
The mouse sees the bear.
True
1
proof
[(triple7)]
("mouse" "sees" "bear" "+")
triple7
The bear does not see the squirrel.
False
1
inv-proof
[(triple4)]
("bear" "sees" "squirrel" "-")
triple4
The squirrel is nice.
True
2
proof
[(((triple11) -> rule2))]
("squirrel" "is" "nice" "+")
((triple11) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The mouse is not nice.
False
2
inv-proof
[(((triple12) -> rule7) OR ((triple7) -> rule2) OR ((((triple11) -> rule8)) -> rule7))]
("mouse" "is" "nice" "-")
((triple12) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
((triple7) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
((((triple11) -> (rule8 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int2
The mouse chases the bear.
True
3
proof
[(((((triple12) -> rule7)) -> rule3) OR ((((triple7) -> rule2)) -> rule3) OR ((((((triple11) -> rule8)) -> rule7)) -> rule3))]
("mouse" "chases" "bear" "+")
((((triple12) -> (rule7 % int2))) -> (rule3 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((((((triple11) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
The mouse does not chase the bear.
False
3
inv-proof
[(((((triple12) -> rule7)) -> rule3) OR ((((triple7) -> rule2)) -> rule3) OR ((((((triple11) -> rule8)) -> rule7)) -> rule3))]
("mouse" "chases" "bear" "-")
((((triple12) -> (rule7 % int2))) -> (rule3 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((((((triple11) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "big" "-")
The bear chases the bear.
Unknown
rconc
[@2: The bear chases the bear.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("bear" "chases" "bear" "+")
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "big" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The bear chases the mouse.[(triple1)] The bear does not like the squirrel.[(triple3)] The bear likes the mouse.[(triple2)] The bear sees the squirrel.[(triple4)] The mouse is round.[(triple5)] The mouse likes the squirrel.[(triple6)] The mouse sees the bear.[(triple7)] The mouse sees the squirrel.[(triple8)] The squirrel does not chase the mouse.[(triple9)] The squirrel is young.[(triple10)] The squirrel sees the bear.[(triple11)] The squirrel sees the mouse.[(triple12 OR ((triple11) -> rule8))] @1: The bear does not see the mouse.[(((triple11) -> rule1))] The mouse is nice.[(((triple12) -> rule7) OR ((triple7) -> rule2) OR ((((triple11) -> rule8)) -> rule7))] The mouse sees the mouse.[(((triple7) -> rule8))] The squirrel is nice.[(((triple11) -> rule2))] @2: The mouse chases the bear.[(((((triple12) -> rule7)) -> rule3) OR ((((triple7) -> rule2)) -> rule3) OR ((((((triple11) -> rule8)) -> rule7)) -> rule3))] The squirrel chases the bear.[(((((triple11) -> rule2)) -> rule3))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear does not like the squirrel.
("bear" "likes" "squirrel" "-")
triple3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple4
The mouse is round.
("mouse" "is" "round" "+")
triple5
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple6
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple7
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple8
The squirrel does not chase the mouse.
("squirrel" "chases" "mouse" "-")
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
((triple11) -> (rule8 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The bear does not see the mouse.
("bear" "sees" "mouse" "-")
((triple11) -> (rule1 % int1))
The bear does not see the mouse.
("bear" "sees" "mouse" "-")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
((triple12) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
((triple7) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
((((triple11) -> (rule8 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple7) -> (rule8 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple11) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
((((triple12) -> (rule7 % int2))) -> (rule3 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((((((triple11) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2