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