The bear is cold. The bear does not need the tiger. The bear does not see the rabbit. The bear does not see the tiger. The rabbit eats the tiger. The rabbit is young. The rabbit needs the bear. The rabbit needs the tiger. The rabbit sees the tiger. The tiger eats the rabbit. The tiger needs the rabbit. The tiger does not see the rabbit. If the tiger eats the bear and the bear does not see the tiger then the tiger does not see the rabbit. If something eats the rabbit then it is round. If the bear is young then the bear does not need the rabbit. If something is round then it does not need the bear. If something needs the bear then it is kind. If the tiger does not see the rabbit then the rabbit eats the tiger.
The bear is cold.
("bear" "is" "cold" "+")
The bear does not need the tiger.
("bear" "needs" "tiger" "-")
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
If the tiger eats the bear and the bear does not see the tiger then the tiger does not see the rabbit.
((("tiger" "eats" "bear" "+") ("bear" "sees" "tiger" "~")) -> ("tiger" "sees" "rabbit" "-"))
If something eats the rabbit then it is round.
((("something" "eats" "rabbit" "+")) -> ("something" "is" "round" "+"))
If the bear is young then the bear does not need the rabbit.
((("bear" "is" "young" "+")) -> ("bear" "needs" "rabbit" "-"))
If something is round then it does not need the bear.
((("something" "is" "round" "+")) -> ("something" "needs" "bear" "-"))
If something needs the bear then it is kind.
((("something" "needs" "bear" "+")) -> ("something" "is" "kind" "+"))
If the tiger does not see the rabbit then the rabbit eats the tiger.
((("tiger" "sees" "rabbit" "~")) -> ("rabbit" "eats" "tiger" "+"))
The rabbit needs the tiger.
True
1
proof
[(triple8)]
("rabbit" "needs" "tiger" "+")
triple8
The bear needs the tiger.
False
1
inv-proof
[(triple2)]
("bear" "needs" "tiger" "+")
triple2
The tiger is round.
True
2
proof
[(((triple10) -> rule2))]
("tiger" "is" "round" "+")
((triple10) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The rabbit is not kind.
False
2
inv-proof
[(((triple7) -> rule5))]
("rabbit" "is" "kind" "-")
((triple7) -> (rule5 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The tiger does not need the bear.
True
3
proof
[(((((triple10) -> rule2)) -> rule4))]
("tiger" "needs" "bear" "-")
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The tiger does not need the bear.
("tiger" "needs" "bear" "-")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger needs the bear.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule4))]
("tiger" "needs" "bear" "+")
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The tiger does not need the bear.
("tiger" "needs" "bear" "-")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The bear is not round.
Unknown
inv-rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "round" "-")
The bear is kind.
Unknown
rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "kind" "+")
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "kind" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The bear does not eat the tiger.
Unknown
inv-random
[@0: The bear eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "tiger" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
@0: The bear does not need the tiger.[(triple2)] The bear does not see the rabbit.[(triple3)] The bear does not see the tiger.[(triple4)] The bear is cold.[(triple1)] The rabbit eats the tiger.[(triple5 OR ((triple12) -> rule6))] The rabbit is young.[(triple6)] The rabbit needs the bear.[(triple7)] The rabbit needs the tiger.[(triple8)] The rabbit sees the tiger.[(triple9)] The tiger does not see the rabbit.[(triple12)] The tiger eats the rabbit.[(triple10)] The tiger needs the rabbit.[(triple11)] @1: The rabbit is kind.[(((triple7) -> rule5))] The tiger is round.[(((triple10) -> rule2))] @2: The tiger does not need the bear.[(((((triple10) -> rule2)) -> rule4))]
The bear does not need the tiger.
("bear" "needs" "tiger" "-")
triple2
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
triple3
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
triple4
The bear is cold.
("bear" "is" "cold" "+")
triple1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple5
((triple12) -> (rule6 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
triple6
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple7
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple8
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple9
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
triple12
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple10
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple11
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple7) -> (rule5 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((triple10) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger does not need the bear.
("tiger" "needs" "bear" "-")
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The tiger does not need the bear.
("tiger" "needs" "bear" "-")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2