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