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