The dog chases the tiger. The dog is red. The mouse chases the dog. The mouse chases the tiger. The mouse is red. The mouse sees the dog. The mouse visits the rabbit. The rabbit visits the dog. The tiger is red. The tiger visits the dog. If the rabbit sees the dog and the tiger does not see the rabbit then the rabbit does not chase the mouse.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is red.
("dog" "is" "red" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If the rabbit sees the dog and the tiger does not see the rabbit then the rabbit does not chase the mouse.
((("rabbit" "sees" "dog" "+") ("tiger" "sees" "rabbit" "~")) -> ("rabbit" "chases" "mouse" "-"))
The dog chases the tiger.
True
1
proof
[(triple1)]
("dog" "chases" "tiger" "+")
triple1
The mouse does not chase the dog.
False
1
inv-proof
[(triple3)]
("mouse" "chases" "dog" "-")
triple3
The rabbit does not visit the mouse.
Unknown
inv-random
[@0: The rabbit visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "mouse" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
@0: The dog chases the tiger.[(triple1)] The dog is red.[(triple2)] The mouse chases the dog.[(triple3)] The mouse chases the tiger.[(triple4)] The mouse is red.[(triple5)] The mouse sees the dog.[(triple6)] The mouse visits the rabbit.[(triple7)] The rabbit visits the dog.[(triple8)] The tiger is red.[(triple9)] The tiger visits the dog.[(triple10)]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple3
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple4
The mouse is red.
("mouse" "is" "red" "+")
triple5
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple6
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple7
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple10