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