The cow chases the squirrel. The squirrel chases the cow. The tiger visits the squirrel. If the squirrel visits the tiger and the squirrel sees the cow then the tiger is big. If something is big and it chases the squirrel then the squirrel sees the cow. If something chases the tiger then the tiger sees the cow.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If the squirrel visits the tiger and the squirrel sees the cow then the tiger is big.
((("squirrel" "visits" "tiger" "+") ("squirrel" "sees" "cow" "+")) -> ("tiger" "is" "big" "+"))
If something is big and it chases the squirrel then the squirrel sees the cow.
((("something" "is" "big" "+") ("something" "chases" "squirrel" "+")) -> ("squirrel" "sees" "cow" "+"))
If something chases the tiger then the tiger sees the cow.
((("something" "chases" "tiger" "+")) -> ("tiger" "sees" "cow" "+"))
The squirrel chases the cow.
True
1
proof
[(triple2)]
("squirrel" "chases" "cow" "+")
triple2
The cow does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("cow" "chases" "squirrel" "-")
triple1
The tiger does not see the cow.
Unknown
inv-rconc
[@1: The tiger sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "sees" "cow" "-")
The cow chases the tiger.
Unknown
random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "tiger" "+")
@0: The cow chases the squirrel.[(triple1)] The squirrel chases the cow.[(triple2)] The tiger visits the squirrel.[(triple3)]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple3