The bear visits the rabbit. The cat is rough. The cat likes the cow. The cow is big. The cow likes the bear. The cow visits the bear. The rabbit is nice. The rabbit is round. The rabbit likes the bear. The rabbit sees the cat. The rabbit sees the cow. The rabbit visits the cow. If the cat likes the bear and the bear likes the cow then the cow likes the cat. If something is rough then it sees the rabbit. If something visits the cow and the cow likes the cat then the cat visits the rabbit. If the rabbit is young and the rabbit sees the cat then the rabbit likes the cat. If the cow visits the bear then the bear is rough. If something likes the bear and it sees the cat then the cat visits the rabbit.
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cow is big.
("cow" "is" "big" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If the cat likes the bear and the bear likes the cow then the cow likes the cat.
((("cat" "likes" "bear" "+") ("bear" "likes" "cow" "+")) -> ("cow" "likes" "cat" "+"))
If something is rough then it sees the rabbit.
((("something" "is" "rough" "+")) -> ("something" "sees" "rabbit" "+"))
If something visits the cow and the cow likes the cat then the cat visits the rabbit.
((("something" "visits" "cow" "+") ("cow" "likes" "cat" "+")) -> ("cat" "visits" "rabbit" "+"))
If the rabbit is young and the rabbit sees the cat then the rabbit likes the cat.
((("rabbit" "is" "young" "+") ("rabbit" "sees" "cat" "+")) -> ("rabbit" "likes" "cat" "+"))
If the cow visits the bear then the bear is rough.
((("cow" "visits" "bear" "+")) -> ("bear" "is" "rough" "+"))
If something likes the bear and it sees the cat then the cat visits the rabbit.
((("something" "likes" "bear" "+") ("something" "sees" "cat" "+")) -> ("cat" "visits" "rabbit" "+"))
The cow visits the bear.
True
1
proof
[(triple6)]
("cow" "visits" "bear" "+")
triple6
The rabbit does not see the cow.
False
1
inv-proof
[(triple11)]
("rabbit" "sees" "cow" "-")
triple11
The bear is rough.
True
2
proof
[(((triple6) -> rule5))]
("bear" "is" "rough" "+")
((triple6) -> (rule5 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The cat does not see the rabbit.
False
2
inv-proof
[(((triple2) -> rule2))]
("cat" "sees" "rabbit" "-")
((triple2) -> (rule2 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The bear sees the rabbit.
True
3
proof
[(((((triple6) -> rule5)) -> rule2))]
("bear" "sees" "rabbit" "+")
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear does not see the rabbit.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule2))]
("bear" "sees" "rabbit" "-")
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The cow does not like the cat.
Unknown
inv-rconc
[@1: The cow likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "cat" "-")
The cow sees the rabbit.
Unknown
rconc
[@1: The cow sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "rabbit" "+")
The rabbit does not like the cat.
Unknown
inv-rconc
[@1: The rabbit likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "likes" "cat" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The bear does not see the cow.
Unknown
inv-random
[@0: The bear sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "cow" "-")
The rabbit visits the bear.
Unknown
random
[@0: The rabbit visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "bear" "+")
@0: The bear visits the rabbit.[(triple1)] The cat is rough.[(triple2)] The cat likes the cow.[(triple3)] The cow is big.[(triple4)] The cow likes the bear.[(triple5)] The cow visits the bear.[(triple6)] The rabbit is nice.[(triple7)] The rabbit is round.[(triple8)] The rabbit likes the bear.[(triple9)] The rabbit sees the cat.[(triple10)] The rabbit sees the cow.[(triple11)] The rabbit visits the cow.[(triple12)] @1: The bear is rough.[(((triple6) -> rule5))] The cat sees the rabbit.[(((triple2) -> rule2))] The cat visits the rabbit.[(((triple9 triple10) -> rule6))] @2: The bear sees the rabbit.[(((((triple6) -> rule5)) -> rule2))]
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat likes the cow.
("cat" "likes" "cow" "+")
triple3
The cow is big.
("cow" "is" "big" "+")
triple4
The cow likes the bear.
("cow" "likes" "bear" "+")
triple5
The cow visits the bear.
("cow" "visits" "bear" "+")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple7
The rabbit is round.
("rabbit" "is" "round" "+")
triple8
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple9
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple10
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple11
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple12
The bear is rough.
("bear" "is" "rough" "+")
((triple6) -> (rule5 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
((triple2) -> (rule2 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((triple9 triple10) -> (rule6 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2