The cow needs the dog. The cow visits the dog. The dog needs the cow. If someone needs the cow and the cow needs the dog then they are blue. If the dog likes the cow and the cow likes the dog then the dog is kind.
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
If someone needs the cow and the cow needs the dog then they are blue.
((("someone" "needs" "cow" "+") ("cow" "needs" "dog" "+")) -> ("someone" "is" "blue" "+"))
If the dog likes the cow and the cow likes the dog then the dog is kind.
((("dog" "likes" "cow" "+") ("cow" "likes" "dog" "+")) -> ("dog" "is" "kind" "+"))
The dog needs the cow.
True
1
proof
[(triple3)]
("dog" "needs" "cow" "+")
triple3
The cow does not visit the dog.
False
1
inv-proof
[(triple2)]
("cow" "visits" "dog" "-")
triple2
The cow is not blue.
Unknown
inv-rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "blue" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
@0: The cow needs the dog.[(triple1)] The cow visits the dog.[(triple2)] The dog needs the cow.[(triple3)] @1: The dog is blue.[(((triple3 triple1) -> rule1))]
The cow needs the dog.
("cow" "needs" "dog" "+")
triple1
The cow visits the dog.
("cow" "visits" "dog" "+")
triple2
The dog needs the cow.
("dog" "needs" "cow" "+")
triple3
The dog is blue.
("dog" "is" "blue" "+")
((triple3 triple1) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1