The bear chases the cow. The cow is blue. The dog is rough. If the cow eats the dog then the cow is cold. If something is cold and it does not eat the bear then the bear chases the cow. If something is rough then it does not like the cow. If something is red then it chases the dog. If something likes the dog then the dog likes the cow. If something is cold and it does not eat the bear then it is not round. If something chases the cow and the cow is not blue then the cow does not like the dog. If something likes the cow and it is not round then the cow chases the bear.
The bear chases the cow.
("bear" "chases" "cow" "+")
The cow is blue.
("cow" "is" "blue" "+")
The dog is rough.
("dog" "is" "rough" "+")
If the cow eats the dog then the cow is cold.
((("cow" "eats" "dog" "+")) -> ("cow" "is" "cold" "+"))
If something is cold and it does not eat the bear then the bear chases the cow.
((("something" "is" "cold" "+") ("something" "eats" "bear" "~")) -> ("bear" "chases" "cow" "+"))
If something is rough then it does not like the cow.
((("something" "is" "rough" "+")) -> ("something" "likes" "cow" "-"))
If something is red then it chases the dog.
((("something" "is" "red" "+")) -> ("something" "chases" "dog" "+"))
If something likes the dog then the dog likes the cow.
((("something" "likes" "dog" "+")) -> ("dog" "likes" "cow" "+"))
If something is cold and it does not eat the bear then it is not round.
((("something" "is" "cold" "+") ("something" "eats" "bear" "~")) -> ("something" "is" "round" "-"))
If something chases the cow and the cow is not blue then the cow does not like the dog.
((("something" "chases" "cow" "+") ("cow" "is" "blue" "~")) -> ("cow" "likes" "dog" "-"))
If something likes the cow and it is not round then the cow chases the bear.
((("something" "likes" "cow" "+") ("something" "is" "round" "~")) -> ("cow" "chases" "bear" "+"))
The bear chases the cow.
True
1
proof
[(triple1)]
("bear" "chases" "cow" "+")
triple1
The dog is not rough.
False
1
inv-proof
[(triple3)]
("dog" "is" "rough" "-")
triple3
The dog does not like the cow.
True
2
proof
[(((triple3) -> rule3))]
("dog" "likes" "cow" "-")
((triple3) -> (rule3 % int1))
The dog does not like the cow.
("dog" "likes" "cow" "-")
int1
The dog likes the cow.
False
2
inv-proof
[(((triple3) -> rule3))]
("dog" "likes" "cow" "+")
((triple3) -> (rule3 % int1))
The dog does not like the cow.
("dog" "likes" "cow" "-")
int1
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "chases" "dog" "-")
The cow is cold.
Unknown
rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "cold" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The bear eats the cow.
Unknown
random
[@0: The bear eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "cow" "+")
@0: The bear chases the cow.[(triple1)] The cow is blue.[(triple2)] The dog is rough.[(triple3)] @1: The dog does not like the cow.[(((triple3) -> rule3))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The dog is rough.
("dog" "is" "rough" "+")
triple3
The dog does not like the cow.
("dog" "likes" "cow" "-")
((triple3) -> (rule3 % int1))
The dog does not like the cow.
("dog" "likes" "cow" "-")
int1