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