The bear chases the tiger. The bear is green. The bear sees the tiger. The cow chases the bear. The cow needs the bear. The cow needs the lion. The cow sees the lion. The lion chases the bear. The lion chases the tiger. The lion is big. The lion is kind. The lion sees the tiger. The tiger chases the bear. The tiger is kind. The tiger sees the bear. The tiger sees the lion. If something needs the lion then the lion needs the bear. If something chases the lion and the lion chases the cow then it chases the bear. If something needs the cow then it sees the tiger. If something needs the cow and the cow chases the lion then the lion needs the tiger. If the cow chases the tiger then the tiger chases the cow. If the cow is kind then the cow is big. If something chases the cow then it needs the cow. If something needs the bear and it sees the bear then the bear chases the lion.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is green.
("bear" "is" "green" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If something needs the lion then the lion needs the bear.
((("something" "needs" "lion" "+")) -> ("lion" "needs" "bear" "+"))
If something chases the lion and the lion chases the cow then it chases the bear.
((("something" "chases" "lion" "+") ("lion" "chases" "cow" "+")) -> ("something" "chases" "bear" "+"))
If something needs the cow then it sees the tiger.
((("something" "needs" "cow" "+")) -> ("something" "sees" "tiger" "+"))
If something needs the cow and the cow chases the lion then the lion needs the tiger.
((("something" "needs" "cow" "+") ("cow" "chases" "lion" "+")) -> ("lion" "needs" "tiger" "+"))
If the cow chases the tiger then the tiger chases the cow.
((("cow" "chases" "tiger" "+")) -> ("tiger" "chases" "cow" "+"))
If the cow is kind then the cow is big.
((("cow" "is" "kind" "+")) -> ("cow" "is" "big" "+"))
If something chases the cow then it needs the cow.
((("something" "chases" "cow" "+")) -> ("something" "needs" "cow" "+"))
If something needs the bear and it sees the bear then the bear chases the lion.
((("something" "needs" "bear" "+") ("something" "sees" "bear" "+")) -> ("bear" "chases" "lion" "+"))
The bear chases the tiger.
True
1
proof
[(triple1)]
("bear" "chases" "tiger" "+")
triple1
The lion does not chase the bear.
False
1
inv-proof
[(triple8)]
("lion" "chases" "bear" "-")
triple8
The lion needs the bear.
True
2
proof
[(((triple6) -> rule1))]
("lion" "needs" "bear" "+")
((triple6) -> (rule1 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion does not need the bear.
False
2
inv-proof
[(((triple6) -> rule1))]
("lion" "needs" "bear" "-")
((triple6) -> (rule1 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
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 cow needs the cow.
Unknown
rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "needs" "cow" "+")
The lion does not see the bear.
Unknown
inv-random
[@0: The lion sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bear" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear chases the tiger.[(triple1)] The bear is green.[(triple2)] The bear sees the tiger.[(triple3)] The cow chases the bear.[(triple4)] The cow needs the bear.[(triple5)] The cow needs the lion.[(triple6)] The cow sees the lion.[(triple7)] The lion chases the bear.[(triple8)] The lion chases the tiger.[(triple9)] The lion is big.[(triple10)] The lion is kind.[(triple11)] The lion sees the tiger.[(triple12)] The tiger chases the bear.[(triple13)] The tiger is kind.[(triple14)] The tiger sees the bear.[(triple15)] The tiger sees the lion.[(triple16)] @1: The lion needs the bear.[(((triple6) -> rule1))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
triple2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple3
The cow chases the bear.
("cow" "chases" "bear" "+")
triple4
The cow needs the bear.
("cow" "needs" "bear" "+")
triple5
The cow needs the lion.
("cow" "needs" "lion" "+")
triple6
The cow sees the lion.
("cow" "sees" "lion" "+")
triple7
The lion chases the bear.
("lion" "chases" "bear" "+")
triple8
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple9
The lion is big.
("lion" "is" "big" "+")
triple10
The lion is kind.
("lion" "is" "kind" "+")
triple11
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple12
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple13
The tiger is kind.
("tiger" "is" "kind" "+")
triple14
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple15
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple16
The lion needs the bear.
("lion" "needs" "bear" "+")
((triple6) -> (rule1 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1