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