The bear is rough. The bear does not need the cow. The cow likes the bear. The cow does not need the tiger. The rabbit is young. The rabbit likes the bear. The rabbit needs the cow. The rabbit sees the tiger. The tiger is rough. The tiger does not like the bear. The tiger needs the bear. The tiger does not need the rabbit. If someone needs the tiger then they are round. If the bear likes the tiger then the tiger likes the bear. If someone is kind and they do not need the bear then they do not need the tiger. If someone needs the cow then they need the tiger. If someone needs the rabbit then they do not see the tiger. If the bear does not need the cow then the cow is young. If the cow likes the bear and the cow is not young then the bear is not nice. If someone is nice and kind then they see the rabbit.
The bear is rough.
("bear" "is" "rough" "+")
The bear does not need the cow.
("bear" "needs" "cow" "-")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow does not need the tiger.
("cow" "needs" "tiger" "-")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger does not like the bear.
("tiger" "likes" "bear" "-")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
If someone needs the tiger then they are round.
((("someone" "needs" "tiger" "+")) -> ("someone" "is" "round" "+"))
If the bear likes the tiger then the tiger likes the bear.
((("bear" "likes" "tiger" "+")) -> ("tiger" "likes" "bear" "+"))
If someone is kind and they do not need the bear then they do not need the tiger.
((("someone" "is" "kind" "+") ("someone" "needs" "bear" "~")) -> ("someone" "needs" "tiger" "-"))
If someone needs the cow then they need the tiger.
((("someone" "needs" "cow" "+")) -> ("someone" "needs" "tiger" "+"))
If someone needs the rabbit then they do not see the tiger.
((("someone" "needs" "rabbit" "+")) -> ("someone" "sees" "tiger" "-"))
If the bear does not need the cow then the cow is young.
((("bear" "needs" "cow" "~")) -> ("cow" "is" "young" "+"))
If the cow likes the bear and the cow is not young then the bear is not nice.
((("cow" "likes" "bear" "+") ("cow" "is" "young" "~")) -> ("bear" "is" "nice" "-"))
If someone is nice and kind then they see the rabbit.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "sees" "rabbit" "+"))
The rabbit needs the cow.
True
1
proof
[(triple7)]
("rabbit" "needs" "cow" "+")
triple7
The tiger likes the bear.
False
1
inv-proof
[(triple10)]
("tiger" "likes" "bear" "+")
triple10
The rabbit needs the tiger.
True
2
proof
[(((triple7) -> rule4))]
("rabbit" "needs" "tiger" "+")
((triple7) -> (rule4 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The rabbit does not need the tiger.
False
2
inv-proof
[(((triple7) -> rule4))]
("rabbit" "needs" "tiger" "-")
((triple7) -> (rule4 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "round" "-")
The cow sees the rabbit.
Unknown
rconc
[@1: The cow sees the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "sees" "rabbit" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The cow needs the bear.
Unknown
random
[@0: The cow needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "bear" "+")
@0: The bear does not need the cow.[(triple2)] The bear is rough.[(triple1)] The cow does not need the tiger.[(triple4)] The cow likes the bear.[(triple3)] The rabbit is young.[(triple5)] The rabbit likes the bear.[(triple6)] The rabbit needs the cow.[(triple7)] The rabbit sees the tiger.[(triple8)] The tiger does not like the bear.[(triple10)] The tiger does not need the rabbit.[(triple12)] The tiger is rough.[(triple9)] The tiger needs the bear.[(triple11)] @1: The cow is young.[(((triple2) -> rule6))] The rabbit needs the tiger.[(((triple7) -> rule4))] @2: The rabbit is round.[(((((triple7) -> rule4)) -> rule1))]
The bear does not need the cow.
("bear" "needs" "cow" "-")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple1
The cow does not need the tiger.
("cow" "needs" "tiger" "-")
triple4
The cow likes the bear.
("cow" "likes" "bear" "+")
triple3
The rabbit is young.
("rabbit" "is" "young" "+")
triple5
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple6
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple7
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple8
The tiger does not like the bear.
("tiger" "likes" "bear" "-")
triple10
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
triple12
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple11
The cow is young.
("cow" "is" "young" "+")
((triple2) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
((triple7) -> (rule4 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int2