The bear sees the cow. The bear sees the tiger. The cow does not chase the bear. The cow is big. The cow is nice. The cow is young. The cow sees the bear. The lion chases the bear. The lion needs the bear. The lion sees the cow. The tiger does not chase the lion. The tiger is rough. The tiger needs the bear. The tiger needs the lion. The tiger sees the bear. The tiger sees the cow. If someone chases the cow then they chase the tiger. If someone needs the tiger and they do not chase the bear then the tiger does not see the lion. If someone chases the tiger then the tiger sees the lion. If someone needs the lion and the lion needs the bear then the lion chases the cow. If someone needs the bear then the bear chases the cow. All young people are cold. If the bear is rough then the bear needs the cow. If someone sees the lion and the lion is big then they are not young.
The bear sees the cow.
("bear" "sees" "cow" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The cow does not chase the bear.
("cow" "chases" "bear" "-")
The cow is big.
("cow" "is" "big" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is young.
("cow" "is" "young" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If someone chases the cow then they chase the tiger.
((("someone" "chases" "cow" "+")) -> ("someone" "chases" "tiger" "+"))
If someone needs the tiger and they do not chase the bear then the tiger does not see the lion.
((("someone" "needs" "tiger" "+") ("someone" "chases" "bear" "~")) -> ("tiger" "sees" "lion" "-"))
If someone chases the tiger then the tiger sees the lion.
((("someone" "chases" "tiger" "+")) -> ("tiger" "sees" "lion" "+"))
If someone needs the lion and the lion needs the bear then the lion chases the cow.
((("someone" "needs" "lion" "+") ("lion" "needs" "bear" "+")) -> ("lion" "chases" "cow" "+"))
If someone needs the bear then the bear chases the cow.
((("someone" "needs" "bear" "+")) -> ("bear" "chases" "cow" "+"))
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If the bear is rough then the bear needs the cow.
((("bear" "is" "rough" "+")) -> ("bear" "needs" "cow" "+"))
If someone sees the lion and the lion is big then they are not young.
((("someone" "sees" "lion" "+") ("lion" "is" "big" "+")) -> ("someone" "is" "young" "-"))
The cow is big.
True
1
proof
[(triple4)]
("cow" "is" "big" "+")
triple4
The cow is not big.
False
1
inv-proof
[(triple4)]
("cow" "is" "big" "-")
triple4
The bear chases the cow.
True
2
proof
[(((triple13) -> rule5) OR ((triple9) -> rule5))]
("bear" "chases" "cow" "+")
((triple13) -> (rule5 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
((triple9) -> (rule5 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The lion does not chase the cow.
False
3
inv-proof
[(((triple14 triple9) -> rule4))]
("lion" "chases" "cow" "-")
((triple14 triple9) -> (rule4 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion chases the tiger.
True
4
proof
[(((((triple14 triple9) -> rule4)) -> rule1))]
("lion" "chases" "tiger" "+")
((((triple14 triple9) -> (rule4 % int2))) -> (rule1 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The bear does not chase the tiger.
False
3
inv-proof
[(((((triple13) -> rule5)) -> rule1) OR ((((triple9) -> rule5)) -> rule1))]
("bear" "chases" "tiger" "-")
((((triple13) -> (rule5 % int2))) -> (rule1 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
((((triple9) -> (rule5 % int2))) -> (rule1 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The tiger sees the lion.
True
4
proof
[(((((((triple13) -> rule5)) -> rule1)) -> rule3) OR ((((((triple9) -> rule5)) -> rule1)) -> rule3) OR ((((((triple14 triple9) -> rule4)) -> rule1)) -> rule3))]
("tiger" "sees" "lion" "+")
((((((triple13) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3
((((((triple9) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3
((((((triple14 triple9) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3
The tiger does not see the lion.
False
4
inv-proof
[(((((((triple13) -> rule5)) -> rule1)) -> rule3) OR ((((((triple9) -> rule5)) -> rule1)) -> rule3) OR ((((((triple14 triple9) -> rule4)) -> rule1)) -> rule3))]
("tiger" "sees" "lion" "-")
((((((triple13) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3
((((((triple9) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3
((((((triple14 triple9) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3
The cow does not chase the tiger.
Unknown
inv-rconc
[@1: The cow chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "tiger" "-")
The bear is cold.
Unknown
rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "cold" "+")
The bear does not need the cow.
Unknown
inv-rconc
[@1: The bear needs the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "needs" "cow" "-")
The tiger chases the tiger.
Unknown
rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "tiger" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The bear needs the tiger.
Unknown
random
[@0: The bear needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "tiger" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The bear sees the cow.[(triple1)] The bear sees the tiger.[(triple2)] The cow does not chase the bear.[(triple3)] The cow is big.[(triple4)] The cow is nice.[(triple5)] The cow is young.[(triple6)] The cow sees the bear.[(triple7)] The lion chases the bear.[(triple8)] The lion needs the bear.[(triple9)] The lion sees the cow.[(triple10)] The tiger does not chase the lion.[(triple11)] The tiger is rough.[(triple12)] The tiger needs the bear.[(triple13)] The tiger needs the lion.[(triple14)] The tiger sees the bear.[(triple15)] The tiger sees the cow.[(triple16)] @1: The bear chases the cow.[(((triple13) -> rule5) OR ((triple9) -> rule5))] The cow is cold.[(((triple6) -> rule6))] The lion chases the cow.[(((triple14 triple9) -> rule4))] @2: The bear chases the tiger.[(((((triple13) -> rule5)) -> rule1) OR ((((triple9) -> rule5)) -> rule1))] The lion chases the tiger.[(((((triple14 triple9) -> rule4)) -> rule1))] @3: The tiger sees the lion.[(((((((triple13) -> rule5)) -> rule1)) -> rule3) OR ((((((triple9) -> rule5)) -> rule1)) -> rule3) OR ((((((triple14 triple9) -> rule4)) -> rule1)) -> rule3))]
The bear sees the cow.
("bear" "sees" "cow" "+")
triple1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple2
The cow does not chase the bear.
("cow" "chases" "bear" "-")
triple3
The cow is big.
("cow" "is" "big" "+")
triple4
The cow is nice.
("cow" "is" "nice" "+")
triple5
The cow is young.
("cow" "is" "young" "+")
triple6
The cow sees the bear.
("cow" "sees" "bear" "+")
triple7
The lion chases the bear.
("lion" "chases" "bear" "+")
triple8
The lion needs the bear.
("lion" "needs" "bear" "+")
triple9
The lion sees the cow.
("lion" "sees" "cow" "+")
triple10
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple13
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple14
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple15
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple16
The bear chases the cow.
("bear" "chases" "cow" "+")
((triple13) -> (rule5 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
((triple9) -> (rule5 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((triple6) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
((triple14 triple9) -> (rule4 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
((((triple13) -> (rule5 % int2))) -> (rule1 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
((((triple9) -> (rule5 % int2))) -> (rule1 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
((((triple14 triple9) -> (rule4 % int2))) -> (rule1 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The tiger sees the lion.
("tiger" "sees" "lion" "+")
((((((triple13) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3
((((((triple9) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3
((((((triple14 triple9) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3