The bear eats the rabbit. The bear is rough. The mouse eats the squirrel. The mouse needs the rabbit. The rabbit is cold. The rabbit needs the bear. The rabbit needs the mouse. The squirrel is big. The squirrel is nice. The squirrel is red. The squirrel needs the bear. The squirrel needs the mouse. If someone needs the squirrel and they like the rabbit then the rabbit is big. If someone likes the rabbit then the rabbit is red. If someone eats the squirrel then they need the bear. Red people are rough. If someone needs the bear and they eat the mouse then the mouse needs the bear. If someone is red and rough then they like the rabbit. If someone eats the bear and the bear needs the mouse then they like the squirrel. If someone likes the mouse and the mouse likes the bear then the mouse eats the bear. If the bear eats the rabbit then the bear needs the mouse.
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear is rough.
("bear" "is" "rough" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If someone needs the squirrel and they like the rabbit then the rabbit is big.
((("someone" "needs" "squirrel" "+") ("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
If someone likes the rabbit then the rabbit is red.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "red" "+"))
If someone eats the squirrel then they need the bear.
((("someone" "eats" "squirrel" "+")) -> ("someone" "needs" "bear" "+"))
Red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone needs the bear and they eat the mouse then the mouse needs the bear.
((("someone" "needs" "bear" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "needs" "bear" "+"))
If someone is red and rough then they like the rabbit.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone eats the bear and the bear needs the mouse then they like the squirrel.
((("someone" "eats" "bear" "+") ("bear" "needs" "mouse" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone likes the mouse and the mouse likes the bear then the mouse eats the bear.
((("someone" "likes" "mouse" "+") ("mouse" "likes" "bear" "+")) -> ("mouse" "eats" "bear" "+"))
If the bear eats the rabbit then the bear needs the mouse.
((("bear" "eats" "rabbit" "+")) -> ("bear" "needs" "mouse" "+"))
The squirrel is red.
True
1
proof
[(triple10)]
("squirrel" "is" "red" "+")
triple10
The squirrel does not need the mouse.
False
1
inv-proof
[(triple12)]
("squirrel" "needs" "mouse" "-")
triple12
The bear needs the mouse.
True
2
proof
[(((triple1) -> rule9))]
("bear" "needs" "mouse" "+")
((triple1) -> (rule9 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear does not need the mouse.
False
2
inv-proof
[(((triple1) -> rule9))]
("bear" "needs" "mouse" "-")
((triple1) -> (rule9 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The squirrel likes the rabbit.
True
4
proof
[(((triple10 ((triple10) -> rule4)) -> rule6))]
("squirrel" "likes" "rabbit" "+")
((triple10 ((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel does not like the rabbit.
False
4
inv-proof
[(((triple10 ((triple10) -> rule4)) -> rule6))]
("squirrel" "likes" "rabbit" "-")
((triple10 ((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The rabbit is red.
True
5
proof
[(((((triple10 ((triple10) -> rule4)) -> rule6)) -> rule2))]
("rabbit" "is" "red" "+")
((((triple10 ((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The rabbit is not red.
False
5
inv-proof
[(((((triple10 ((triple10) -> rule4)) -> rule6)) -> rule2))]
("rabbit" "is" "red" "-")
((((triple10 ((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The rabbit is rough.
True
6
proof
[(((((((triple10 ((triple10) -> rule4)) -> rule6)) -> rule2)) -> rule4))]
("rabbit" "is" "rough" "+")
((((((triple10 ((triple10) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The rabbit is not rough.
False
6
inv-proof
[(((((((triple10 ((triple10) -> rule4)) -> rule6)) -> rule2)) -> rule4))]
("rabbit" "is" "rough" "-")
((((((triple10 ((triple10) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The rabbit likes the rabbit.
True
12
proof
[(((((((triple10 ((triple10) -> rule4)) -> rule6)) -> rule2) ((((((triple10 ((triple10) -> rule4)) -> rule6)) -> rule2)) -> rule4)) -> rule6))]
("rabbit" "likes" "rabbit" "+")
((((((triple10 ((triple10) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule2 % int3)) ((((((triple10 ((triple10) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int4
The squirrel is rough.
("squirrel" "is" "rough" "+")
int5
The rabbit does not like the rabbit.
False
12
inv-proof
[(((((((triple10 ((triple10) -> rule4)) -> rule6)) -> rule2) ((((((triple10 ((triple10) -> rule4)) -> rule6)) -> rule2)) -> rule4)) -> rule6))]
("rabbit" "likes" "rabbit" "-")
((((((triple10 ((triple10) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule2 % int3)) ((((((triple10 ((triple10) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int4
The squirrel is rough.
("squirrel" "is" "rough" "+")
int5
The mouse does not like the rabbit.
Unknown
inv-rconc
[@1: The mouse likes the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "likes" "rabbit" "-")
The mouse likes the squirrel.
Unknown
rconc
[@2: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("mouse" "likes" "squirrel" "+")
The rabbit is not big.
Unknown
inv-rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "big" "-")
The bear likes the squirrel.
Unknown
rconc
[@1: The bear likes the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "likes" "squirrel" "+")
The bear does not like the rabbit.
Unknown
inv-rconc
[@1: The bear likes the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "likes" "rabbit" "-")
The squirrel likes the squirrel.
Unknown
rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "likes" "squirrel" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The rabbit likes the mouse.
Unknown
random
[@0: The rabbit likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "mouse" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
@0: The bear eats the rabbit.[(triple1)] The bear is rough.[(triple2)] The mouse eats the squirrel.[(triple3)] The mouse needs the rabbit.[(triple4)] The rabbit is cold.[(triple5)] The rabbit needs the bear.[(triple6)] The rabbit needs the mouse.[(triple7)] The squirrel is big.[(triple8)] The squirrel is nice.[(triple9)] The squirrel is red.[(triple10)] The squirrel needs the bear.[(triple11)] The squirrel needs the mouse.[(triple12)] @1: The bear needs the mouse.[(((triple1) -> rule9))] The mouse needs the bear.[(((triple3) -> rule3))] The squirrel is rough.[(((triple10) -> rule4))] @2: The squirrel likes the rabbit.[(((triple10 ((triple10) -> rule4)) -> rule6))] @3: The rabbit is red.[(((((triple10 ((triple10) -> rule4)) -> rule6)) -> rule2))] @4: The rabbit is rough.[(((((((triple10 ((triple10) -> rule4)) -> rule6)) -> rule2)) -> rule4))] @5: The rabbit likes the rabbit.[(((((((triple10 ((triple10) -> rule4)) -> rule6)) -> rule2) ((((((triple10 ((triple10) -> rule4)) -> rule6)) -> rule2)) -> rule4)) -> rule6))]
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple3
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple4
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple5
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple6
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
triple8
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple9
The squirrel is red.
("squirrel" "is" "red" "+")
triple10
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple11
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple12
The bear needs the mouse.
("bear" "needs" "mouse" "+")
((triple1) -> (rule9 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple3) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple10) -> (rule4 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
((triple10 ((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
((((triple10 ((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((((triple10 ((triple10) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((((triple10 ((triple10) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule2 % int3)) ((((((triple10 ((triple10) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int4
The squirrel is rough.
("squirrel" "is" "rough" "+")
int5