The cow is red. The cow visits the dog. The dog visits the cow. If someone sees the cow and they see the dog then the dog visits the cow.
The cow is red.
("cow" "is" "red" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
If someone sees the cow and they see the dog then the dog visits the cow.
((("someone" "sees" "cow" "+") ("someone" "sees" "dog" "+")) -> ("dog" "visits" "cow" "+"))
The dog visits the cow.
True
1
proof
[(triple3)]
("dog" "visits" "cow" "+")
triple3
The cow is not red.
False
1
inv-proof
[(triple1)]
("cow" "is" "red" "-")
triple1
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow is red.[(triple1)] The cow visits the dog.[(triple2)] The dog visits the cow.[(triple3)]
The cow is red.
("cow" "is" "red" "+")
triple1
The cow visits the dog.
("cow" "visits" "dog" "+")
triple2
The dog visits the cow.
("dog" "visits" "cow" "+")
triple3