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