The cow does not visit the dog. The dog needs the cow. If something needs the cow then the cow is green. If the dog does not like the cow and the dog does not visit the cow then the cow needs the dog. If something is cold and it needs the cow then the cow needs the dog.
The cow does not visit the dog.
("cow" "visits" "dog" "-")
The dog needs the cow.
("dog" "needs" "cow" "+")
If something needs the cow then the cow is green.
((("something" "needs" "cow" "+")) -> ("cow" "is" "green" "+"))
If the dog does not like the cow and the dog does not visit the cow then the cow needs the dog.
((("dog" "likes" "cow" "~") ("dog" "visits" "cow" "~")) -> ("cow" "needs" "dog" "+"))
If something is cold and it needs the cow then the cow needs the dog.
((("something" "is" "cold" "+") ("something" "needs" "cow" "+")) -> ("cow" "needs" "dog" "+"))
The dog needs the cow.
True
1
proof
[(triple2)]
("dog" "needs" "cow" "+")
triple2
The dog does not need the cow.
False
1
inv-proof
[(triple2)]
("dog" "needs" "cow" "-")
triple2
The cow is green.
True
2
proof
[(((triple2) -> rule1))]
("cow" "is" "green" "+")
((triple2) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not green.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "is" "green" "-")
((triple2) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow does not need the dog.
Unknown
inv-rconc
[@1: The cow needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "dog" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The cow does not visit the dog.[(triple1)] The dog needs the cow.[(triple2)] @1: The cow is green.[(((triple2) -> rule1))]
The cow does not visit the dog.
("cow" "visits" "dog" "-")
triple1
The dog needs the cow.
("dog" "needs" "cow" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
((triple2) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1