The bear does not chase the lion. The cat is rough. The lion does not eat the bear. If someone is red and big then they do not like the lion. If the cat does not like the bear then the cat is not kind. If someone chases the cat then the cat is not rough.
The bear does not chase the lion.
("bear" "chases" "lion" "-")
The cat is rough.
("cat" "is" "rough" "+")
The lion does not eat the bear.
("lion" "eats" "bear" "-")
If someone is red and big then they do not like the lion.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "likes" "lion" "-"))
If the cat does not like the bear then the cat is not kind.
((("cat" "likes" "bear" "~")) -> ("cat" "is" "kind" "-"))
If someone chases the cat then the cat is not rough.
((("someone" "chases" "cat" "+")) -> ("cat" "is" "rough" "-"))
The cat is rough.
True
1
proof
[(triple2)]
("cat" "is" "rough" "+")
triple2
The cat is not rough.
False
1
inv-proof
[(triple2)]
("cat" "is" "rough" "-")
triple2
The cat does not eat the bear.
Unknown
inv-random
[@0: The cat eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "bear" "-")
The lion chases the cat.
Unknown
random
[@0: The lion chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cat" "+")
@0: The bear does not chase the lion.[(triple1)] The cat is rough.[(triple2)] The lion does not eat the bear.[(triple3)]
The bear does not chase the lion.
("bear" "chases" "lion" "-")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The lion does not eat the bear.
("lion" "eats" "bear" "-")
triple3