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