The cow chases the dog. The cow is blue. The cow is not cold. The cow is nice. The cow is round. The cow is young. The cow likes the dog. The cow visits the dog. The dog chases the cow. The dog is blue. The dog is cold. The dog is not nice. The dog is round. The dog is not young. The dog likes the cow. The dog does not visit the cow. If the dog likes the cow and the dog does not visit the cow then the cow visits the dog. If someone likes the cow then the cow chases the dog. If the cow is round then the cow is young. If someone likes the dog then the dog chases the cow. If someone is young and they visit the cow then the cow does not like the dog. If the cow does not chase the dog then the cow does not like the dog.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is not cold.
("cow" "is" "cold" "-")
The cow is nice.
("cow" "is" "nice" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is not nice.
("dog" "is" "nice" "-")
The dog is round.
("dog" "is" "round" "+")
The dog is not young.
("dog" "is" "young" "-")
The dog likes the cow.
("dog" "likes" "cow" "+")
The dog does not visit the cow.
("dog" "visits" "cow" "-")
If the dog likes the cow and the dog does not visit the cow then the cow visits the dog.
((("dog" "likes" "cow" "+") ("dog" "visits" "cow" "~")) -> ("cow" "visits" "dog" "+"))
If someone likes the cow then the cow chases the dog.
((("someone" "likes" "cow" "+")) -> ("cow" "chases" "dog" "+"))
If the cow is round then the cow is young.
((("cow" "is" "round" "+")) -> ("cow" "is" "young" "+"))
If someone likes the dog then the dog chases the cow.
((("someone" "likes" "dog" "+")) -> ("dog" "chases" "cow" "+"))
If someone is young and they visit the cow then the cow does not like the dog.
((("someone" "is" "young" "+") ("someone" "visits" "cow" "+")) -> ("cow" "likes" "dog" "-"))
If the cow does not chase the dog then the cow does not like the dog.
((("cow" "chases" "dog" "~")) -> ("cow" "likes" "dog" "-"))
The cow is nice.
True
1
proof
[(triple4)]
("cow" "is" "nice" "+")
triple4
The cow does not visit the dog.
False
1
inv-proof
[(triple8 OR ((triple15 triple16) -> rule1))]
("cow" "visits" "dog" "-")
triple8
((triple15 triple16) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow chases the dog.[(triple1 OR ((triple15) -> rule2))] The cow is blue.[(triple2)] The cow is nice.[(triple4)] The cow is not cold.[(triple3)] The cow is round.[(triple5)] The cow is young.[(triple6 OR ((triple5) -> rule3))] The cow likes the dog.[(triple7)] The cow visits the dog.[(triple8 OR ((triple15 triple16) -> rule1))] The dog chases the cow.[(triple9 OR ((triple7) -> rule4))] The dog does not visit the cow.[(triple16)] The dog is blue.[(triple10)] The dog is cold.[(triple11)] The dog is not nice.[(triple12)] The dog is not young.[(triple14)] The dog is round.[(triple13)] The dog likes the cow.[(triple15)]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
((triple15) -> (rule2 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow is not cold.
("cow" "is" "cold" "-")
triple3
The cow is round.
("cow" "is" "round" "+")
triple5
The cow is young.
("cow" "is" "young" "+")
triple6
((triple5) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
triple7
The cow visits the dog.
("cow" "visits" "dog" "+")
triple8
((triple15 triple16) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
triple9
((triple7) -> (rule4 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog does not visit the cow.
("dog" "visits" "cow" "-")
triple16
The dog is blue.
("dog" "is" "blue" "+")
triple10
The dog is cold.
("dog" "is" "cold" "+")
triple11
The dog is not nice.
("dog" "is" "nice" "-")
triple12
The dog is not young.
("dog" "is" "young" "-")
triple14
The dog is round.
("dog" "is" "round" "+")
triple13
The dog likes the cow.
("dog" "likes" "cow" "+")
triple15