The bear chases the dog. The bear likes the cow. The bear needs the cow. The bear does not need the dog. The cow chases the bear. The cow is kind. The cow likes the bear. The cow likes the dog. The dog does not chase the cow. The dog needs the cow. If someone likes the dog then they need the bear. If someone is kind and they do not chase the bear then the bear needs the cow. If someone is red then they are kind. If someone needs the bear then they do not need the cow. If someone is kind and they need the bear then they need the dog. If someone likes the dog and the dog does not chase the bear then the dog does not like the bear. If the bear likes the cow and the bear likes the dog then the cow chases the dog. If the cow needs the dog then the cow chases the dog.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear does not need the dog.
("bear" "needs" "dog" "-")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The dog does not chase the cow.
("dog" "chases" "cow" "-")
The dog needs the cow.
("dog" "needs" "cow" "+")
If someone likes the dog then they need the bear.
((("someone" "likes" "dog" "+")) -> ("someone" "needs" "bear" "+"))
If someone is kind and they do not chase the bear then the bear needs the cow.
((("someone" "is" "kind" "+") ("someone" "chases" "bear" "~")) -> ("bear" "needs" "cow" "+"))
If someone is red then they are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If someone needs the bear then they do not need the cow.
((("someone" "needs" "bear" "+")) -> ("someone" "needs" "cow" "-"))
If someone is kind and they need the bear then they need the dog.
((("someone" "is" "kind" "+") ("someone" "needs" "bear" "+")) -> ("someone" "needs" "dog" "+"))
If someone likes the dog and the dog does not chase the bear then the dog does not like the bear.
((("someone" "likes" "dog" "+") ("dog" "chases" "bear" "~")) -> ("dog" "likes" "bear" "-"))
If the bear likes the cow and the bear likes the dog then the cow chases the dog.
((("bear" "likes" "cow" "+") ("bear" "likes" "dog" "+")) -> ("cow" "chases" "dog" "+"))
If the cow needs the dog then the cow chases the dog.
((("cow" "needs" "dog" "+")) -> ("cow" "chases" "dog" "+"))
The bear chases the dog.
True
1
proof
[(triple1)]
("bear" "chases" "dog" "+")
triple1
The cow does not like the dog.
False
1
inv-proof
[(triple8)]
("cow" "likes" "dog" "-")
triple8
The cow needs the bear.
True
2
proof
[(((triple8) -> rule1))]
("cow" "needs" "bear" "+")
((triple8) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow does not need the bear.
False
2
inv-proof
[(((triple8) -> rule1))]
("cow" "needs" "bear" "-")
((triple8) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow does not need the cow.
True
3
proof
[(((((triple8) -> rule1)) -> rule4))]
("cow" "needs" "cow" "-")
((((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow does not need the dog.
False
4
inv-proof
[(((triple6 ((triple8) -> rule1)) -> rule5))]
("cow" "needs" "dog" "-")
((triple6 ((triple8) -> (rule1 % int2))) -> (rule5 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow chases the dog.
True
5
proof
[(((((triple6 ((triple8) -> rule1)) -> rule5)) -> rule8))]
("cow" "chases" "dog" "+")
((((triple6 ((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The cow needs the bear.
("cow" "needs" "bear" "+")
int3
The cow does not chase the dog.
False
5
inv-proof
[(((((triple6 ((triple8) -> rule1)) -> rule5)) -> rule8))]
("cow" "chases" "dog" "-")
((((triple6 ((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The cow needs the bear.
("cow" "needs" "bear" "+")
int3
The dog does not need the bear.
Unknown
inv-rconc
[@1: The dog needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "needs" "bear" "-")
The dog needs the dog.
Unknown
rconc
[@2: The dog needs the dog.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("dog" "needs" "dog" "+")
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "needs" "bear" "-")
The dog is kind.
Unknown
rconc
[@1: The dog is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "kind" "+")
The dog does not chase the bear.
Unknown
inv-random
[@0: The dog chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "bear" "-")
The bear likes the dog.
Unknown
random
[@0: The bear likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "dog" "+")
The dog does not like the cow.
Unknown
inv-random
[@0: The dog likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cow" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The bear chases the dog.[(triple1)] The bear does not need the dog.[(triple4)] The bear likes the cow.[(triple2)] The bear needs the cow.[(triple3)] The cow chases the bear.[(triple5)] The cow is kind.[(triple6)] The cow likes the bear.[(triple7)] The cow likes the dog.[(triple8)] The dog does not chase the cow.[(triple9)] The dog needs the cow.[(triple10)] @1: The cow needs the bear.[(((triple8) -> rule1))] @2: The cow does not need the cow.[(((((triple8) -> rule1)) -> rule4))] The cow needs the dog.[(((triple6 ((triple8) -> rule1)) -> rule5))] @3: The cow chases the dog.[(((((triple6 ((triple8) -> rule1)) -> rule5)) -> rule8))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The bear does not need the dog.
("bear" "needs" "dog" "-")
triple4
The bear likes the cow.
("bear" "likes" "cow" "+")
triple2
The bear needs the cow.
("bear" "needs" "cow" "+")
triple3
The cow chases the bear.
("cow" "chases" "bear" "+")
triple5
The cow is kind.
("cow" "is" "kind" "+")
triple6
The cow likes the bear.
("cow" "likes" "bear" "+")
triple7
The cow likes the dog.
("cow" "likes" "dog" "+")
triple8
The dog does not chase the cow.
("dog" "chases" "cow" "-")
triple9
The dog needs the cow.
("dog" "needs" "cow" "+")
triple10
The cow needs the bear.
("cow" "needs" "bear" "+")
((triple8) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow does not need the cow.
("cow" "needs" "cow" "-")
((((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow needs the dog.
("cow" "needs" "dog" "+")
((triple6 ((triple8) -> (rule1 % int2))) -> (rule5 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
((((triple6 ((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The cow needs the bear.
("cow" "needs" "bear" "+")
int3