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