The bear eats the mouse. The bear is nice. The mouse eats the bear. The mouse is cold. The mouse needs the bear. The tiger is round. The tiger likes the bear. If someone needs the bear then they eat the mouse. If someone likes the tiger and they are big then they eat the tiger. If someone is nice then they eat the bear. If someone needs the tiger and they are nice then they are big. If someone eats the tiger and the tiger likes the bear then the tiger is young. If the mouse is big then the mouse is nice. If someone needs the mouse and the mouse is cold then the mouse eats the tiger. If someone eats the mouse and they eat the bear then they need the tiger.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is nice.
("bear" "is" "nice" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
If someone needs the bear then they eat the mouse.
((("someone" "needs" "bear" "+")) -> ("someone" "eats" "mouse" "+"))
If someone likes the tiger and they are big then they eat the tiger.
((("someone" "likes" "tiger" "+") ("someone" "is" "big" "+")) -> ("someone" "eats" "tiger" "+"))
If someone is nice then they eat the bear.
((("someone" "is" "nice" "+")) -> ("someone" "eats" "bear" "+"))
If someone needs the tiger and they are nice then they are big.
((("someone" "needs" "tiger" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone eats the tiger and the tiger likes the bear then the tiger is young.
((("someone" "eats" "tiger" "+") ("tiger" "likes" "bear" "+")) -> ("tiger" "is" "young" "+"))
If the mouse is big then the mouse is nice.
((("mouse" "is" "big" "+")) -> ("mouse" "is" "nice" "+"))
If someone needs the mouse and the mouse is cold then the mouse eats the tiger.
((("someone" "needs" "mouse" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "eats" "tiger" "+"))
If someone eats the mouse and they eat the bear then they need the tiger.
((("someone" "eats" "mouse" "+") ("someone" "eats" "bear" "+")) -> ("someone" "needs" "tiger" "+"))
The tiger likes the bear.
True
1
proof
[(triple7)]
("tiger" "likes" "bear" "+")
triple7
The bear does not eat the mouse.
False
1
inv-proof
[(triple1)]
("bear" "eats" "mouse" "-")
triple1
The mouse eats the mouse.
True
2
proof
[(((triple5) -> rule1))]
("mouse" "eats" "mouse" "+")
((triple5) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse does not eat the mouse.
False
2
inv-proof
[(((triple5) -> rule1))]
("mouse" "eats" "mouse" "-")
((triple5) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse needs the tiger.
True
4
proof
[(((((triple5) -> rule1) triple3) -> rule8))]
("mouse" "needs" "tiger" "+")
((((triple5) -> (rule1 % int2)) triple3) -> (rule8 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse does not need the tiger.
False
4
inv-proof
[(((((triple5) -> rule1) triple3) -> rule8))]
("mouse" "needs" "tiger" "-")
((((triple5) -> (rule1 % int2)) triple3) -> (rule8 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The bear is big.
True
6
proof
[(((((triple1 ((triple2) -> rule3)) -> rule8) triple2) -> rule4))]
("bear" "is" "big" "+")
((((triple1 ((triple2) -> (rule3 % int3))) -> (rule8 % int2)) triple2) -> (rule4 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear is not big.
False
6
inv-proof
[(((((triple1 ((triple2) -> rule3)) -> rule8) triple2) -> rule4))]
("bear" "is" "big" "-")
((((triple1 ((triple2) -> (rule3 % int3))) -> (rule8 % int2)) triple2) -> (rule4 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The tiger does not need the tiger.
Unknown
inv-rconc
[@2: The tiger needs the tiger.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The mouse is big.
Unknown
rconc
[@2: The mouse is big.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("mouse" "is" "big" "+")
The tiger does not eat the tiger.
Unknown
inv-rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The bear eats the tiger.
Unknown
rconc
[@1: The bear eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "tiger" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The bear eats the mouse.[(triple1)] The bear is nice.[(triple2)] The mouse eats the bear.[(triple3)] The mouse is cold.[(triple4)] The mouse needs the bear.[(triple5)] The tiger is round.[(triple6)] The tiger likes the bear.[(triple7)] @1: The bear eats the bear.[(((triple2) -> rule3))] The mouse eats the mouse.[(((triple5) -> rule1))] @2: The bear needs the tiger.[(((triple1 ((triple2) -> rule3)) -> rule8))] The mouse needs the tiger.[(((((triple5) -> rule1) triple3) -> rule8))] @3: The bear is big.[(((((triple1 ((triple2) -> rule3)) -> rule8) triple2) -> rule4))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple3
The mouse is cold.
("mouse" "is" "cold" "+")
triple4
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple5
The tiger is round.
("tiger" "is" "round" "+")
triple6
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple7
The bear eats the bear.
("bear" "eats" "bear" "+")
((triple2) -> (rule3 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple5) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((triple1 ((triple2) -> (rule3 % int2))) -> (rule8 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
((((triple5) -> (rule1 % int2)) triple3) -> (rule8 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The bear is big.
("bear" "is" "big" "+")
((((triple1 ((triple2) -> (rule3 % int3))) -> (rule8 % int2)) triple2) -> (rule4 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3