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