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