The bear chases the rabbit. The bear likes the cow. The cow is cold. The cow is red. The cow is rough. The rabbit is rough. The tiger chases the bear. If someone chases the rabbit then they are red. If someone is cold and they need the rabbit then the rabbit needs the tiger. If the rabbit likes the tiger then the rabbit likes the bear. If someone chases the rabbit then the rabbit is rough. If someone chases the cow then the cow chases the rabbit. If someone chases the tiger and they like the rabbit then they chase the cow.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
If someone chases the rabbit then they are red.
((("someone" "chases" "rabbit" "+")) -> ("someone" "is" "red" "+"))
If someone is cold and they need the rabbit then the rabbit needs the tiger.
((("someone" "is" "cold" "+") ("someone" "needs" "rabbit" "+")) -> ("rabbit" "needs" "tiger" "+"))
If the rabbit likes the tiger then the rabbit likes the bear.
((("rabbit" "likes" "tiger" "+")) -> ("rabbit" "likes" "bear" "+"))
If someone chases the rabbit then the rabbit is rough.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
If someone chases the cow then the cow chases the rabbit.
((("someone" "chases" "cow" "+")) -> ("cow" "chases" "rabbit" "+"))
If someone chases the tiger and they like the rabbit then they chase the cow.
((("someone" "chases" "tiger" "+") ("someone" "likes" "rabbit" "+")) -> ("someone" "chases" "cow" "+"))
The tiger chases the bear.
True
1
proof
[(triple7)]
("tiger" "chases" "bear" "+")
triple7
The rabbit is not rough.
False
1
inv-proof
[(triple6 OR ((triple1) -> rule4))]
("rabbit" "is" "rough" "-")
triple6
((triple1) -> (rule4 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The bear is red.
True
2
proof
[(((triple1) -> rule1))]
("bear" "is" "red" "+")
((triple1) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is not red.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "is" "red" "-")
((triple1) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "red" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "chases" "cow" "+")
The cow does not chase the bear.
Unknown
inv-random
[@0: The cow chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "bear" "-")
The cow needs the rabbit.
Unknown
random
[@0: The cow needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "rabbit" "+")
@0: The bear chases the rabbit.[(triple1)] The bear likes the cow.[(triple2)] The cow is cold.[(triple3)] The cow is red.[(triple4)] The cow is rough.[(triple5)] The rabbit is rough.[(triple6 OR ((triple1) -> rule4))] The tiger chases the bear.[(triple7)] @1: The bear is red.[(((triple1) -> rule1))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear likes the cow.
("bear" "likes" "cow" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow is rough.
("cow" "is" "rough" "+")
triple5
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple6
((triple1) -> (rule4 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple7
The bear is red.
("bear" "is" "red" "+")
((triple1) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1