The bear chases the lion. The bear eats the rabbit. The bear does not eat the squirrel. The lion chases the bear. The lion does not chase the squirrel. The rabbit chases the bear. The rabbit does not chase the lion. The rabbit is big. The rabbit does not see the squirrel. The squirrel eats the bear. If someone chases the bear then the bear sees the squirrel.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear does not eat the squirrel.
("bear" "eats" "squirrel" "-")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion does not chase the squirrel.
("lion" "chases" "squirrel" "-")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit does not see the squirrel.
("rabbit" "sees" "squirrel" "-")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
If someone chases the bear then the bear sees the squirrel.
((("someone" "chases" "bear" "+")) -> ("bear" "sees" "squirrel" "+"))
The rabbit chases the bear.
True
1
proof
[(triple6)]
("rabbit" "chases" "bear" "+")
triple6
The bear does not eat the rabbit.
False
1
inv-proof
[(triple2)]
("bear" "eats" "rabbit" "-")
triple2
The bear sees the squirrel.
True
2
proof
[(((triple4) -> rule1) OR ((triple6) -> rule1))]
("bear" "sees" "squirrel" "+")
((triple4) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
((triple6) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear does not see the squirrel.
False
2
inv-proof
[(((triple4) -> rule1) OR ((triple6) -> rule1))]
("bear" "sees" "squirrel" "-")
((triple4) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
((triple6) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear does not eat the lion.
Unknown
inv-random
[@0: The bear eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "lion" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The squirrel does not chase the rabbit.
Unknown
inv-random
[@0: The squirrel chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "rabbit" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear chases the lion.[(triple1)] The bear does not eat the squirrel.[(triple3)] The bear eats the rabbit.[(triple2)] The lion chases the bear.[(triple4)] The lion does not chase the squirrel.[(triple5)] The rabbit chases the bear.[(triple6)] The rabbit does not chase the lion.[(triple7)] The rabbit does not see the squirrel.[(triple9)] The rabbit is big.[(triple8)] The squirrel eats the bear.[(triple10)] @1: The bear sees the squirrel.[(((triple4) -> rule1) OR ((triple6) -> rule1))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear does not eat the squirrel.
("bear" "eats" "squirrel" "-")
triple3
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple2
The lion chases the bear.
("lion" "chases" "bear" "+")
triple4
The lion does not chase the squirrel.
("lion" "chases" "squirrel" "-")
triple5
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple6
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
triple7
The rabbit does not see the squirrel.
("rabbit" "sees" "squirrel" "-")
triple9
The rabbit is big.
("rabbit" "is" "big" "+")
triple8
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple10
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
((triple4) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
((triple6) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1