The bear eats the lion. The bear eats the mouse. The bear likes the lion. The bear likes the mouse. The bear does not like the tiger. The bear does not need the tiger. The lion eats the mouse. The lion likes the bear. The lion needs the mouse. The mouse does not need the bear. The tiger eats the bear. The tiger needs the lion. If someone needs the tiger then they are cold. If the lion does not like the mouse then the mouse is round. If someone needs the lion then they need the tiger. If someone eats the mouse then the mouse needs the lion. If someone eats the tiger then they are not nice. If the mouse does not need the tiger then the tiger does not need the bear.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear does not like the tiger.
("bear" "likes" "tiger" "-")
The bear does not need the tiger.
("bear" "needs" "tiger" "-")
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If someone needs the tiger then they are cold.
((("someone" "needs" "tiger" "+")) -> ("someone" "is" "cold" "+"))
If the lion does not like the mouse then the mouse is round.
((("lion" "likes" "mouse" "~")) -> ("mouse" "is" "round" "+"))
If someone needs the lion then they need the tiger.
((("someone" "needs" "lion" "+")) -> ("someone" "needs" "tiger" "+"))
If someone eats the mouse then the mouse needs the lion.
((("someone" "eats" "mouse" "+")) -> ("mouse" "needs" "lion" "+"))
If someone eats the tiger then they are not nice.
((("someone" "eats" "tiger" "+")) -> ("someone" "is" "nice" "-"))
If the mouse does not need the tiger then the tiger does not need the bear.
((("mouse" "needs" "tiger" "~")) -> ("tiger" "needs" "bear" "-"))
The bear eats the mouse.
True
1
proof
[(triple2)]
("bear" "eats" "mouse" "+")
triple2
The mouse needs the bear.
False
1
inv-proof
[(triple10)]
("mouse" "needs" "bear" "+")
triple10
The mouse needs the lion.
True
2
proof
[(((triple2) -> rule4) OR ((triple7) -> rule4))]
("mouse" "needs" "lion" "+")
((triple2) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
((triple7) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse does not need the lion.
False
2
inv-proof
[(((triple2) -> rule4) OR ((triple7) -> rule4))]
("mouse" "needs" "lion" "-")
((triple2) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
((triple7) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse needs the tiger.
True
3
proof
[(((((triple2) -> rule4)) -> rule3) OR ((((triple7) -> rule4)) -> rule3))]
("mouse" "needs" "tiger" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The mouse does not need the tiger.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3) OR ((((triple7) -> rule4)) -> rule3))]
("mouse" "needs" "tiger" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The mouse is cold.
True
4
proof
[(((((((triple2) -> rule4)) -> rule3)) -> rule1) OR ((((((triple7) -> rule4)) -> rule3)) -> rule1))]
("mouse" "is" "cold" "+")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int3
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int3
The mouse is not cold.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule3)) -> rule1) OR ((((((triple7) -> rule4)) -> rule3)) -> rule1))]
("mouse" "is" "cold" "-")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int3
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int3
The lion is not cold.
Unknown
inv-rconc
[@2: The lion is cold.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("lion" "is" "cold" "-")
The bear is cold.
Unknown
rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "cold" "+")
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "round" "-")
The lion needs the tiger.
Unknown
rconc
[@1: The lion needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "needs" "tiger" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The mouse likes the tiger.
Unknown
random
[@0: The mouse likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "tiger" "+")
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 bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear does not like the tiger.[(triple5)] The bear does not need the tiger.[(triple6)] The bear eats the lion.[(triple1)] The bear eats the mouse.[(triple2)] The bear likes the lion.[(triple3)] The bear likes the mouse.[(triple4)] The lion eats the mouse.[(triple7)] The lion likes the bear.[(triple8)] The lion needs the mouse.[(triple9)] The mouse does not need the bear.[(triple10)] The tiger eats the bear.[(triple11)] The tiger needs the lion.[(triple12)] @1: The mouse needs the lion.[(((triple2) -> rule4) OR ((triple7) -> rule4))] The tiger needs the tiger.[(((triple12) -> rule3))] @2: The mouse needs the tiger.[(((((triple2) -> rule4)) -> rule3) OR ((((triple7) -> rule4)) -> rule3))] The tiger is cold.[(((((triple12) -> rule3)) -> rule1))] @3: The mouse is cold.[(((((((triple2) -> rule4)) -> rule3)) -> rule1) OR ((((((triple7) -> rule4)) -> rule3)) -> rule1))]
The bear does not like the tiger.
("bear" "likes" "tiger" "-")
triple5
The bear does not need the tiger.
("bear" "needs" "tiger" "-")
triple6
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple2
The bear likes the lion.
("bear" "likes" "lion" "+")
triple3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple4
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple7
The lion likes the bear.
("lion" "likes" "bear" "+")
triple8
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple9
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
triple10
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple11
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple12
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((triple2) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
((triple7) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple12) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
((((triple12) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int3
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int3