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