The cow visits the dog. The dog is red. The dog visits the cow. If someone is red then they do not chase the cow. If someone is young then they like the dog. If someone is round then they like the dog. If someone likes the cow then they do not like the dog. If someone likes the cow and they are round then the cow is round. If the dog visits the cow and the dog likes the cow then the dog is young. If the cow chases the dog and the cow is not kind then the dog does not like the cow. If someone chases the cow and they are kind then they are not young.
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog is red.
("dog" "is" "red" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
If someone is red then they do not chase the cow.
((("someone" "is" "red" "+")) -> ("someone" "chases" "cow" "-"))
If someone is young then they like the dog.
((("someone" "is" "young" "+")) -> ("someone" "likes" "dog" "+"))
If someone is round then they like the dog.
((("someone" "is" "round" "+")) -> ("someone" "likes" "dog" "+"))
If someone likes the cow then they do not like the dog.
((("someone" "likes" "cow" "+")) -> ("someone" "likes" "dog" "-"))
If someone likes the cow and they are round then the cow is round.
((("someone" "likes" "cow" "+") ("someone" "is" "round" "+")) -> ("cow" "is" "round" "+"))
If the dog visits the cow and the dog likes the cow then the dog is young.
((("dog" "visits" "cow" "+") ("dog" "likes" "cow" "+")) -> ("dog" "is" "young" "+"))
If the cow chases the dog and the cow is not kind then the dog does not like the cow.
((("cow" "chases" "dog" "+") ("cow" "is" "kind" "~")) -> ("dog" "likes" "cow" "-"))
If someone chases the cow and they are kind then they are not young.
((("someone" "chases" "cow" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "-"))
The dog visits the cow.
True
1
proof
[(triple3)]
("dog" "visits" "cow" "+")
triple3
The cow does not visit the dog.
False
1
inv-proof
[(triple1)]
("cow" "visits" "dog" "-")
triple1
The dog does not chase the cow.
True
2
proof
[(((triple2) -> rule1))]
("dog" "chases" "cow" "-")
((triple2) -> (rule1 % int1))
The dog does not chase the cow.
("dog" "chases" "cow" "-")
int1
The dog chases the cow.
False
2
inv-proof
[(((triple2) -> rule1))]
("dog" "chases" "cow" "+")
((triple2) -> (rule1 % int1))
The dog does not chase the cow.
("dog" "chases" "cow" "-")
int1
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "young" "-")
The dog likes the dog.
Unknown
rconc
[@2: The dog likes the dog.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("dog" "likes" "dog" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The cow chases the dog.
Unknown
random
[@0: The cow chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "dog" "+")
@0: The cow visits the dog.[(triple1)] The dog is red.[(triple2)] The dog visits the cow.[(triple3)] @1: The dog does not chase the cow.[(((triple2) -> rule1))]
The cow visits the dog.
("cow" "visits" "dog" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The dog visits the cow.
("dog" "visits" "cow" "+")
triple3
The dog does not chase the cow.
("dog" "chases" "cow" "-")
((triple2) -> (rule1 % int1))
The dog does not chase the cow.
("dog" "chases" "cow" "-")
int1