The bear is rough. The bear needs the cow. The cow is cold. The cow is rough. The dog chases the lion. The dog likes the bear. The lion chases the dog. The lion is green. The lion is red. The lion likes the bear. If someone likes the dog then they like the bear. If someone is rough then they chase the bear. If someone needs the lion then the lion is rough.
The bear is rough.
("bear" "is" "rough" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is rough.
("cow" "is" "rough" "+")
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is red.
("lion" "is" "red" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
If someone likes the dog then they like the bear.
((("someone" "likes" "dog" "+")) -> ("someone" "likes" "bear" "+"))
If someone is rough then they chase the bear.
((("someone" "is" "rough" "+")) -> ("someone" "chases" "bear" "+"))
If someone needs the lion then the lion is rough.
((("someone" "needs" "lion" "+")) -> ("lion" "is" "rough" "+"))
The bear needs the cow.
True
1
proof
[(triple2)]
("bear" "needs" "cow" "+")
triple2
The cow is not rough.
False
1
inv-proof
[(triple4)]
("cow" "is" "rough" "-")
triple4
The cow chases the bear.
True
2
proof
[(((triple4) -> rule2))]
("cow" "chases" "bear" "+")
((triple4) -> (rule2 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow does not chase the bear.
False
2
inv-proof
[(((triple4) -> rule2))]
("cow" "chases" "bear" "-")
((triple4) -> (rule2 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The dog does not chase the bear.
Unknown
inv-rconc
[@1: The dog chases the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "bear" "-")
The cow likes the bear.
Unknown
rconc
[@1: The cow likes the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "bear" "+")
The lion does not like the cow.
Unknown
inv-random
[@0: The lion likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cow" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The bear is rough.[(triple1)] The bear needs the cow.[(triple2)] The cow is cold.[(triple3)] The cow is rough.[(triple4)] The dog chases the lion.[(triple5)] The dog likes the bear.[(triple6)] The lion chases the dog.[(triple7)] The lion is green.[(triple8)] The lion is red.[(triple9)] The lion likes the bear.[(triple10)] @1: The bear chases the bear.[(((triple1) -> rule2))] The cow chases the bear.[(((triple4) -> rule2))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear needs the cow.
("bear" "needs" "cow" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is rough.
("cow" "is" "rough" "+")
triple4
The dog chases the lion.
("dog" "chases" "lion" "+")
triple5
The dog likes the bear.
("dog" "likes" "bear" "+")
triple6
The lion chases the dog.
("lion" "chases" "dog" "+")
triple7
The lion is green.
("lion" "is" "green" "+")
triple8
The lion is red.
("lion" "is" "red" "+")
triple9
The lion likes the bear.
("lion" "likes" "bear" "+")
triple10
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple1) -> (rule2 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
((triple4) -> (rule2 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1