The bear chases the rabbit. The bear is young. The bear sees the dog. The bear does not see the rabbit. The dog does not chase the bear. The dog chases the rabbit. The dog is nice. The rabbit chases the bear. The rabbit chases the dog. The rabbit likes the dog. The rabbit does not see the bear. The rabbit sees the dog. If someone chases the rabbit and they are not cold then the rabbit does not chase the dog. If the rabbit is young then the rabbit sees the bear. If the rabbit likes the dog then the dog does not like the rabbit.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is young.
("bear" "is" "young" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
The dog does not chase the bear.
("dog" "chases" "bear" "-")
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog is nice.
("dog" "is" "nice" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If someone chases the rabbit and they are not cold then the rabbit does not chase the dog.
((("someone" "chases" "rabbit" "+") ("someone" "is" "cold" "~")) -> ("rabbit" "chases" "dog" "-"))
If the rabbit is young then the rabbit sees the bear.
((("rabbit" "is" "young" "+")) -> ("rabbit" "sees" "bear" "+"))
If the rabbit likes the dog then the dog does not like the rabbit.
((("rabbit" "likes" "dog" "+")) -> ("dog" "likes" "rabbit" "-"))
The dog chases the rabbit.
True
1
proof
[(triple6)]
("dog" "chases" "rabbit" "+")
triple6
The rabbit sees the bear.
False
1
inv-proof
[(triple11)]
("rabbit" "sees" "bear" "+")
triple11
The dog does not like the rabbit.
True
2
proof
[(((triple10) -> rule3))]
("dog" "likes" "rabbit" "-")
((triple10) -> (rule3 % int1))
The dog does not like the rabbit.
("dog" "likes" "rabbit" "-")
int1
The dog likes the rabbit.
False
2
inv-proof
[(((triple10) -> rule3))]
("dog" "likes" "rabbit" "+")
((triple10) -> (rule3 % int1))
The dog does not like the rabbit.
("dog" "likes" "rabbit" "-")
int1
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The bear chases the dog.
Unknown
random
[@0: The bear chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "dog" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear likes the rabbit.
Unknown
random
[@0: The bear likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "rabbit" "+")
@0: The bear chases the rabbit.[(triple1)] The bear does not see the rabbit.[(triple4)] The bear is young.[(triple2)] The bear sees the dog.[(triple3)] The dog chases the rabbit.[(triple6)] The dog does not chase the bear.[(triple5)] The dog is nice.[(triple7)] The rabbit chases the bear.[(triple8)] The rabbit chases the dog.[(triple9)] The rabbit does not see the bear.[(triple11)] The rabbit likes the dog.[(triple10)] The rabbit sees the dog.[(triple12)] @1: The dog does not like the rabbit.[(((triple10) -> rule3))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
triple4
The bear is young.
("bear" "is" "young" "+")
triple2
The bear sees the dog.
("bear" "sees" "dog" "+")
triple3
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple6
The dog does not chase the bear.
("dog" "chases" "bear" "-")
triple5
The dog is nice.
("dog" "is" "nice" "+")
triple7
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple8
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple9
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
triple11
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple10
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple12
The dog does not like the rabbit.
("dog" "likes" "rabbit" "-")
((triple10) -> (rule3 % int1))
The dog does not like the rabbit.
("dog" "likes" "rabbit" "-")
int1