The cat is big. The cow sees the tiger. The squirrel chases the cat. The tiger chases the cat. If something sees the squirrel and the squirrel chases the cat then the cat is big.
The cat is big.
("cat" "is" "big" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
If something sees the squirrel and the squirrel chases the cat then the cat is big.
((("something" "sees" "squirrel" "+") ("squirrel" "chases" "cat" "+")) -> ("cat" "is" "big" "+"))
The cow sees the tiger.
True
1
proof
[(triple2)]
("cow" "sees" "tiger" "+")
triple2
The cat is not big.
False
1
inv-proof
[(triple1)]
("cat" "is" "big" "-")
triple1
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The cat chases the cow.
Unknown
random
[@0: The cat chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cow" "+")
@0: The cat is big.[(triple1)] The cow sees the tiger.[(triple2)] The squirrel chases the cat.[(triple3)] The tiger chases the cat.[(triple4)]
The cat is big.
("cat" "is" "big" "+")
triple1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple4