The cow chases the squirrel. The cow is blue. The rabbit chases the tiger. The rabbit is kind. The rabbit needs the tiger. The rabbit visits the squirrel. The squirrel does not chase the rabbit. The tiger chases the squirrel. The tiger needs the squirrel. The tiger visits the cow. If someone chases the rabbit and the rabbit chases the cow then the cow does not chase the tiger. If the rabbit needs the tiger then the rabbit visits the squirrel.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow is blue.
("cow" "is" "blue" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel does not chase the rabbit.
("squirrel" "chases" "rabbit" "-")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If someone chases the rabbit and the rabbit chases the cow then the cow does not chase the tiger.
((("someone" "chases" "rabbit" "+") ("rabbit" "chases" "cow" "+")) -> ("cow" "chases" "tiger" "-"))
If the rabbit needs the tiger then the rabbit visits the squirrel.
((("rabbit" "needs" "tiger" "+")) -> ("rabbit" "visits" "squirrel" "+"))
The tiger needs the squirrel.
True
1
proof
[(triple9)]
("tiger" "needs" "squirrel" "+")
triple9
The squirrel chases the rabbit.
False
1
inv-proof
[(triple7)]
("squirrel" "chases" "rabbit" "+")
triple7
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The cow needs the rabbit.
Unknown
random
[@0: The cow needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "rabbit" "+")
@0: The cow chases the squirrel.[(triple1)] The cow is blue.[(triple2)] The rabbit chases the tiger.[(triple3)] The rabbit is kind.[(triple4)] The rabbit needs the tiger.[(triple5)] The rabbit visits the squirrel.[(triple6 OR ((triple5) -> rule2))] The squirrel does not chase the rabbit.[(triple7)] The tiger chases the squirrel.[(triple8)] The tiger needs the squirrel.[(triple9)] The tiger visits the cow.[(triple10)]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple3
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple4
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple5
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple6
((triple5) -> (rule2 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The squirrel does not chase the rabbit.
("squirrel" "chases" "rabbit" "-")
triple7
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple8
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple9
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple10