The cat is round. The cat does not like the dog. The cat sees the dog. The cat visits the dog. The dog is rough. The dog sees the cat. The dog visits the cat. If something likes the cat then it does not visit the cat.
The cat is round.
("cat" "is" "round" "+")
The cat does not like the dog.
("cat" "likes" "dog" "-")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
If something likes the cat then it does not visit the cat.
((("something" "likes" "cat" "+")) -> ("something" "visits" "cat" "-"))
The dog is rough.
True
1
proof
[(triple5)]
("dog" "is" "rough" "+")
triple5
The cat does not visit the dog.
False
1
inv-proof
[(triple4)]
("cat" "visits" "dog" "-")
triple4
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
@0: The cat does not like the dog.[(triple2)] The cat is round.[(triple1)] The cat sees the dog.[(triple3)] The cat visits the dog.[(triple4)] The dog is rough.[(triple5)] The dog sees the cat.[(triple6)] The dog visits the cat.[(triple7)]
The cat does not like the dog.
("cat" "likes" "dog" "-")
triple2
The cat is round.
("cat" "is" "round" "+")
triple1
The cat sees the dog.
("cat" "sees" "dog" "+")
triple3
The cat visits the dog.
("cat" "visits" "dog" "+")
triple4
The dog is rough.
("dog" "is" "rough" "+")
triple5
The dog sees the cat.
("dog" "sees" "cat" "+")
triple6
The dog visits the cat.
("dog" "visits" "cat" "+")
triple7