The bear chases the lion. The bear does not chase the tiger. The bear is blue. The bear is red. The bear is round. The bear likes the lion. The bear sees the tiger. The lion chases the bear. The lion is young. The lion sees the bear. The tiger chases the bear. The tiger is young. The tiger likes the bear. The tiger likes the lion. The tiger sees the lion. If someone sees the tiger then they see the lion. All young people are round. If the lion is round and the lion sees the bear then the lion sees the tiger.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear does not chase the tiger.
("bear" "chases" "tiger" "-")
The bear is blue.
("bear" "is" "blue" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is round.
("bear" "is" "round" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone sees the tiger then they see the lion.
((("someone" "sees" "tiger" "+")) -> ("someone" "sees" "lion" "+"))
All young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If the lion is round and the lion sees the bear then the lion sees the tiger.
((("lion" "is" "round" "+") ("lion" "sees" "bear" "+")) -> ("lion" "sees" "tiger" "+"))
The lion chases the bear.
True
1
proof
[(triple8)]
("lion" "chases" "bear" "+")
triple8
The tiger does not see the lion.
False
1
inv-proof
[(triple15)]
("tiger" "sees" "lion" "-")
triple15
The tiger is round.
True
2
proof
[(((triple12) -> rule2))]
("tiger" "is" "round" "+")
((triple12) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The lion is not round.
False
2
inv-proof
[(((triple9) -> rule2))]
("lion" "is" "round" "-")
((triple9) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion sees the tiger.
True
4
proof
[(((((triple9) -> rule2) triple10) -> rule3))]
("lion" "sees" "tiger" "+")
((((triple9) -> (rule2 % int2)) triple10) -> (rule3 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion does not see the tiger.
False
4
inv-proof
[(((((triple9) -> rule2) triple10) -> rule3))]
("lion" "sees" "tiger" "-")
((((triple9) -> (rule2 % int2)) triple10) -> (rule3 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion sees the lion.
True
5
proof
[(((((((triple9) -> rule2) triple10) -> rule3)) -> rule1))]
("lion" "sees" "lion" "+")
((((((triple9) -> (rule2 % int3)) triple10) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion does not see the lion.
False
5
inv-proof
[(((((((triple9) -> rule2) triple10) -> rule3)) -> rule1))]
("lion" "sees" "lion" "-")
((((((triple9) -> (rule2 % int3)) triple10) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The tiger does not see the bear.
Unknown
inv-random
[@0: The tiger sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bear" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
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 likes the tiger.
Unknown
random
[@0: The lion likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "tiger" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The lion does not like the bear.
Unknown
inv-random
[@0: The lion likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "bear" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
@0: The bear chases the lion.[(triple1)] The bear does not chase the tiger.[(triple2)] The bear is blue.[(triple3)] The bear is red.[(triple4)] The bear is round.[(triple5)] The bear likes the lion.[(triple6)] The bear sees the tiger.[(triple7)] The lion chases the bear.[(triple8)] The lion is young.[(triple9)] The lion sees the bear.[(triple10)] The tiger chases the bear.[(triple11)] The tiger is young.[(triple12)] The tiger likes the bear.[(triple13)] The tiger likes the lion.[(triple14)] The tiger sees the lion.[(triple15)] @1: The bear sees the lion.[(((triple7) -> rule1))] The lion is round.[(((triple9) -> rule2))] The tiger is round.[(((triple12) -> rule2))] @2: The lion sees the tiger.[(((((triple9) -> rule2) triple10) -> rule3))] @3: The lion sees the lion.[(((((((triple9) -> rule2) triple10) -> rule3)) -> rule1))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear does not chase the tiger.
("bear" "chases" "tiger" "-")
triple2
The bear is blue.
("bear" "is" "blue" "+")
triple3
The bear is red.
("bear" "is" "red" "+")
triple4
The bear is round.
("bear" "is" "round" "+")
triple5
The bear likes the lion.
("bear" "likes" "lion" "+")
triple6
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple7
The lion chases the bear.
("lion" "chases" "bear" "+")
triple8
The lion is young.
("lion" "is" "young" "+")
triple9
The lion sees the bear.
("lion" "sees" "bear" "+")
triple10
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple11
The tiger is young.
("tiger" "is" "young" "+")
triple12
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple13
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple14
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple15
The bear sees the lion.
("bear" "sees" "lion" "+")
((triple7) -> (rule1 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((triple9) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((triple12) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((((triple9) -> (rule2 % int2)) triple10) -> (rule3 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
((((((triple9) -> (rule2 % int3)) triple10) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3