The dog chases the rabbit. The dog does not eat the rabbit. The dog is big. The dog is cold. The dog is green. The dog is red. The dog is round. The dog needs the rabbit. The rabbit chases the dog. The rabbit eats the dog. The rabbit is big. The rabbit is not cold. The rabbit is green. The rabbit is red. The rabbit needs the dog. If the dog chases the rabbit and the dog is not red then the dog needs the rabbit. If someone is cold and not red then they do not eat the dog. If someone needs the dog and the dog chases the rabbit then the rabbit needs the dog.
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog does not eat the rabbit.
("dog" "eats" "rabbit" "-")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is not cold.
("rabbit" "is" "cold" "-")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
If the dog chases the rabbit and the dog is not red then the dog needs the rabbit.
((("dog" "chases" "rabbit" "+") ("dog" "is" "red" "~")) -> ("dog" "needs" "rabbit" "+"))
If someone is cold and not red then they do not eat the dog.
((("someone" "is" "cold" "+") ("someone" "is" "red" "~")) -> ("someone" "eats" "dog" "-"))
If someone needs the dog and the dog chases the rabbit then the rabbit needs the dog.
((("someone" "needs" "dog" "+") ("dog" "chases" "rabbit" "+")) -> ("rabbit" "needs" "dog" "+"))
The dog needs the rabbit.
True
1
proof
[(triple8)]
("dog" "needs" "rabbit" "+")
triple8
The rabbit is not green.
False
1
inv-proof
[(triple13)]
("rabbit" "is" "green" "-")
triple13
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The dog chases the rabbit.[(triple1)] The dog does not eat the rabbit.[(triple2)] The dog is big.[(triple3)] The dog is cold.[(triple4)] The dog is green.[(triple5)] The dog is red.[(triple6)] The dog is round.[(triple7)] The dog needs the rabbit.[(triple8)] The rabbit chases the dog.[(triple9)] The rabbit eats the dog.[(triple10)] The rabbit is big.[(triple11)] The rabbit is green.[(triple13)] The rabbit is not cold.[(triple12)] The rabbit is red.[(triple14)] The rabbit needs the dog.[(triple15)]
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple1
The dog does not eat the rabbit.
("dog" "eats" "rabbit" "-")
triple2
The dog is big.
("dog" "is" "big" "+")
triple3
The dog is cold.
("dog" "is" "cold" "+")
triple4
The dog is green.
("dog" "is" "green" "+")
triple5
The dog is red.
("dog" "is" "red" "+")
triple6
The dog is round.
("dog" "is" "round" "+")
triple7
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple8
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple9
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple10
The rabbit is big.
("rabbit" "is" "big" "+")
triple11
The rabbit is green.
("rabbit" "is" "green" "+")
triple13
The rabbit is not cold.
("rabbit" "is" "cold" "-")
triple12
The rabbit is red.
("rabbit" "is" "red" "+")
triple14
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple15