The bear likes the squirrel. The bear sees the dog. The bear sees the squirrel. The dog is nice. The squirrel chases the bear. The squirrel chases the dog. The squirrel is big. The squirrel is green. The squirrel is round. The squirrel likes the dog. The squirrel sees the dog. The squirrel sees the tiger. The tiger chases the bear. The tiger chases the squirrel. The tiger is green. The tiger sees the squirrel. If something chases the bear and the bear is round then the bear chases the squirrel. If something chases the squirrel and it chases the dog then the dog is big. If the squirrel is kind and the squirrel sees the tiger then the squirrel is nice. If something is kind then it chases the squirrel. If something is kind then it likes the squirrel. All big things are kind. If something chases the tiger then it is big. If something chases the bear and the bear chases the dog then the dog chases the bear. If something chases the tiger then the tiger sees the dog.
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The dog is nice.
("dog" "is" "nice" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something chases the bear and the bear is round then the bear chases the squirrel.
((("something" "chases" "bear" "+") ("bear" "is" "round" "+")) -> ("bear" "chases" "squirrel" "+"))
If something chases the squirrel and it chases the dog then the dog is big.
((("something" "chases" "squirrel" "+") ("something" "chases" "dog" "+")) -> ("dog" "is" "big" "+"))
If the squirrel is kind and the squirrel sees the tiger then the squirrel is nice.
((("squirrel" "is" "kind" "+") ("squirrel" "sees" "tiger" "+")) -> ("squirrel" "is" "nice" "+"))
If something is kind then it chases the squirrel.
((("something" "is" "kind" "+")) -> ("something" "chases" "squirrel" "+"))
If something is kind then it likes the squirrel.
((("something" "is" "kind" "+")) -> ("something" "likes" "squirrel" "+"))
All big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something chases the tiger then it is big.
((("something" "chases" "tiger" "+")) -> ("something" "is" "big" "+"))
If something chases the bear and the bear chases the dog then the dog chases the bear.
((("something" "chases" "bear" "+") ("bear" "chases" "dog" "+")) -> ("dog" "chases" "bear" "+"))
If something chases the tiger then the tiger sees the dog.
((("something" "chases" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
The bear likes the squirrel.
True
1
proof
[(triple1)]
("bear" "likes" "squirrel" "+")
triple1
The bear does not see the dog.
False
1
inv-proof
[(triple2)]
("bear" "sees" "dog" "-")
triple2
The squirrel is kind.
True
2
proof
[(((triple7) -> rule6))]
("squirrel" "is" "kind" "+")
((triple7) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is not kind.
False
2
inv-proof
[(((triple7) -> rule6))]
("squirrel" "is" "kind" "-")
((triple7) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel likes the squirrel.
True
3
proof
[(((((triple7) -> rule6)) -> rule5))]
("squirrel" "likes" "squirrel" "+")
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is not nice.
False
4
inv-proof
[(((((triple7) -> rule6) triple12) -> rule3))]
("squirrel" "is" "nice" "-")
((((triple7) -> (rule6 % int2)) triple12) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The dog is big.
True
5
proof
[(((((((triple7) -> rule6)) -> rule4) triple6) -> rule2))]
("dog" "is" "big" "+")
((((((triple7) -> (rule6 % int3))) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
The dog is not big.
False
5
inv-proof
[(((((((triple7) -> rule6)) -> rule4) triple6) -> rule2))]
("dog" "is" "big" "-")
((((((triple7) -> (rule6 % int3))) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
The dog is kind.
True
6
proof
[(((((((((triple7) -> rule6)) -> rule4) triple6) -> rule2)) -> rule6))]
("dog" "is" "kind" "+")
((((((((triple7) -> (rule6 % int4))) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel is kind.
("squirrel" "is" "kind" "+")
int4
The dog is not kind.
False
6
inv-proof
[(((((((((triple7) -> rule6)) -> rule4) triple6) -> rule2)) -> rule6))]
("dog" "is" "kind" "-")
((((((((triple7) -> (rule6 % int4))) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel is kind.
("squirrel" "is" "kind" "+")
int4
The dog chases the squirrel.
True
7
proof
[(((((((((((triple7) -> rule6)) -> rule4) triple6) -> rule2)) -> rule6)) -> rule4))]
("dog" "chases" "squirrel" "+")
((((((((((triple7) -> (rule6 % int5))) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int4
The squirrel is kind.
("squirrel" "is" "kind" "+")
int5
The dog does not chase the squirrel.
False
7
inv-proof
[(((((((((((triple7) -> rule6)) -> rule4) triple6) -> rule2)) -> rule6)) -> rule4))]
("dog" "chases" "squirrel" "-")
((((((((((triple7) -> (rule6 % int5))) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int4
The squirrel is kind.
("squirrel" "is" "kind" "+")
int5
The bear is not kind.
Unknown
inv-rconc
[@2: The bear is kind.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("bear" "is" "kind" "-")
The bear chases the squirrel.
Unknown
rconc
[@3: The bear chases the squirrel.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule7 <- FAIL)]]
("bear" "chases" "squirrel" "+")
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "is" "big" "-")
The tiger is big.
Unknown
rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "is" "big" "+")
The tiger does not see the dog.
Unknown
inv-rconc
[@1: The tiger sees the dog.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("tiger" "sees" "dog" "-")
The tiger is kind.
Unknown
rconc
[@2: The tiger is kind.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("tiger" "is" "kind" "+")
The dog does not like the bear.
Unknown
inv-random
[@0: The dog likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "bear" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The dog does not chase the tiger.
Unknown
inv-random
[@0: The dog chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "tiger" "-")
The dog sees the squirrel.
Unknown
random
[@0: The dog sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "squirrel" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear likes the dog.
Unknown
random
[@0: The bear likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "dog" "+")
@0: The bear likes the squirrel.[(triple1)] The bear sees the dog.[(triple2)] The bear sees the squirrel.[(triple3)] The dog is nice.[(triple4)] The squirrel chases the bear.[(triple5)] The squirrel chases the dog.[(triple6)] The squirrel is big.[(triple7)] The squirrel is green.[(triple8)] The squirrel is round.[(triple9)] The squirrel likes the dog.[(triple10)] The squirrel sees the dog.[(triple11)] The squirrel sees the tiger.[(triple12)] The tiger chases the bear.[(triple13)] The tiger chases the squirrel.[(triple14)] The tiger is green.[(triple15)] The tiger sees the squirrel.[(triple16)] @1: The squirrel is kind.[(((triple7) -> rule6))] @2: The squirrel chases the squirrel.[(((((triple7) -> rule6)) -> rule4))] The squirrel is nice.[(((((triple7) -> rule6) triple12) -> rule3))] The squirrel likes the squirrel.[(((((triple7) -> rule6)) -> rule5))] @3: The dog is big.[(((((((triple7) -> rule6)) -> rule4) triple6) -> rule2))] @4: The dog is kind.[(((((((((triple7) -> rule6)) -> rule4) triple6) -> rule2)) -> rule6))] @5: The dog chases the squirrel.[(((((((((((triple7) -> rule6)) -> rule4) triple6) -> rule2)) -> rule6)) -> rule4))] The dog likes the squirrel.[(((((((((((triple7) -> rule6)) -> rule4) triple6) -> rule2)) -> rule6)) -> rule5))]
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple1
The bear sees the dog.
("bear" "sees" "dog" "+")
triple2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple3
The dog is nice.
("dog" "is" "nice" "+")
triple4
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple5
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple6
The squirrel is big.
("squirrel" "is" "big" "+")
triple7
The squirrel is green.
("squirrel" "is" "green" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple10
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple11
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple12
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple13
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple14
The tiger is green.
("tiger" "is" "green" "+")
triple15
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple16
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple7) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((triple7) -> (rule6 % int2)) triple12) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The dog is big.
("dog" "is" "big" "+")
((((((triple7) -> (rule6 % int3))) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
((((((((triple7) -> (rule6 % int4))) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule6 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel is kind.
("squirrel" "is" "kind" "+")
int4
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
((((((((((triple7) -> (rule6 % int5))) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int4
The squirrel is kind.
("squirrel" "is" "kind" "+")
int5
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
((((((((((triple7) -> (rule6 % int5))) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int4
The squirrel is kind.
("squirrel" "is" "kind" "+")
int5