The bear chases the lion. The bear chases the squirrel. The bear likes the squirrel. The dog chases the lion. The lion sees the squirrel. The squirrel likes the bear. The squirrel sees the bear. If someone sees the squirrel then they chase the dog. If someone sees the dog then the dog sees the bear. If someone chases the lion then they see the lion. If someone sees the squirrel and they are round then the squirrel likes the dog. If the bear sees the squirrel and the squirrel sees the dog then the bear is big. If someone chases the dog then they are round. If someone sees the squirrel and the squirrel likes the bear then the bear is young. If the bear sees the dog and the dog sees the lion then the lion sees the squirrel.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The dog chases the lion.
("dog" "chases" "lion" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If someone sees the squirrel then they chase the dog.
((("someone" "sees" "squirrel" "+")) -> ("someone" "chases" "dog" "+"))
If someone sees the dog then the dog sees the bear.
((("someone" "sees" "dog" "+")) -> ("dog" "sees" "bear" "+"))
If someone chases the lion then they see the lion.
((("someone" "chases" "lion" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the squirrel and they are round then the squirrel likes the dog.
((("someone" "sees" "squirrel" "+") ("someone" "is" "round" "+")) -> ("squirrel" "likes" "dog" "+"))
If the bear sees the squirrel and the squirrel sees the dog then the bear is big.
((("bear" "sees" "squirrel" "+") ("squirrel" "sees" "dog" "+")) -> ("bear" "is" "big" "+"))
If someone chases the dog then they are round.
((("someone" "chases" "dog" "+")) -> ("someone" "is" "round" "+"))
If someone sees the squirrel and the squirrel likes the bear then the bear is young.
((("someone" "sees" "squirrel" "+") ("squirrel" "likes" "bear" "+")) -> ("bear" "is" "young" "+"))
If the bear sees the dog and the dog sees the lion then the lion sees the squirrel.
((("bear" "sees" "dog" "+") ("dog" "sees" "lion" "+")) -> ("lion" "sees" "squirrel" "+"))
The squirrel sees the bear.
True
1
proof
[(triple7)]
("squirrel" "sees" "bear" "+")
triple7
The dog does not chase the lion.
False
1
inv-proof
[(triple4)]
("dog" "chases" "lion" "-")
triple4
The dog sees the lion.
True
2
proof
[(((triple4) -> rule3))]
("dog" "sees" "lion" "+")
((triple4) -> (rule3 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog does not see the lion.
False
2
inv-proof
[(((triple4) -> rule3))]
("dog" "sees" "lion" "-")
((triple4) -> (rule3 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The lion is round.
True
3
proof
[(((((triple5) -> rule1)) -> rule6))]
("lion" "is" "round" "+")
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
The lion is not round.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule6))]
("lion" "is" "round" "-")
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
The squirrel likes the dog.
True
5
proof
[(((triple5 ((((triple5) -> rule1)) -> rule6)) -> rule4))]
("squirrel" "likes" "dog" "+")
((triple5 ((((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
The squirrel does not like the dog.
False
5
inv-proof
[(((triple5 ((((triple5) -> rule1)) -> rule6)) -> rule4))]
("squirrel" "likes" "dog" "-")
((triple5 ((((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "big" "-")
The squirrel is round.
Unknown
rconc
[@2: The squirrel is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("squirrel" "is" "round" "+")
The dog is not round.
Unknown
inv-rconc
[@2: The dog is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("dog" "is" "round" "-")
The squirrel chases the dog.
Unknown
rconc
[@1: The squirrel chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "dog" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The lion chases the bear.
Unknown
random
[@0: The lion chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "bear" "+")
The dog does not chase the squirrel.
Unknown
inv-random
[@0: The dog chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "squirrel" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
@0: The bear chases the lion.[(triple1)] The bear chases the squirrel.[(triple2)] The bear likes the squirrel.[(triple3)] The dog chases the lion.[(triple4)] The lion sees the squirrel.[(triple5)] The squirrel likes the bear.[(triple6)] The squirrel sees the bear.[(triple7)] @1: The bear is young.[(((triple5 triple6) -> rule7))] The bear sees the lion.[(((triple1) -> rule3))] The dog sees the lion.[(((triple4) -> rule3))] The lion chases the dog.[(((triple5) -> rule1))] @2: The lion is round.[(((((triple5) -> rule1)) -> rule6))] @3: The squirrel likes the dog.[(((triple5 ((((triple5) -> rule1)) -> rule6)) -> rule4))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple2
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple3
The dog chases the lion.
("dog" "chases" "lion" "+")
triple4
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple5
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple6
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple7
The bear is young.
("bear" "is" "young" "+")
((triple5 triple6) -> (rule7 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
((triple1) -> (rule3 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
((triple4) -> (rule3 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
((triple5) -> (rule1 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
((triple5 ((((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3