The dog eats the lion. The dog eats the mouse. The dog eats the rabbit. The dog is rough. The dog likes the lion. The dog likes the mouse. The dog likes the rabbit. The dog sees the rabbit. The lion is big. The lion likes the rabbit. The lion sees the mouse. The mouse is big. The mouse likes the dog. The mouse likes the lion. The mouse sees the rabbit. The rabbit sees the mouse. If someone eats the rabbit then the rabbit eats the lion.
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If someone eats the rabbit then the rabbit eats the lion.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "eats" "lion" "+"))
The rabbit sees the mouse.
True
1
proof
[(triple16)]
("rabbit" "sees" "mouse" "+")
triple16
The lion is not big.
False
1
inv-proof
[(triple9)]
("lion" "is" "big" "-")
triple9
The rabbit eats the lion.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "eats" "lion" "+")
((triple3) -> (rule1 % int1))
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int1
The rabbit does not eat the lion.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "eats" "lion" "-")
((triple3) -> (rule1 % int1))
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int1
The dog does not see the mouse.
Unknown
inv-random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The dog eats the lion.[(triple1)] The dog eats the mouse.[(triple2)] The dog eats the rabbit.[(triple3)] The dog is rough.[(triple4)] The dog likes the lion.[(triple5)] The dog likes the mouse.[(triple6)] The dog likes the rabbit.[(triple7)] The dog sees the rabbit.[(triple8)] The lion is big.[(triple9)] The lion likes the rabbit.[(triple10)] The lion sees the mouse.[(triple11)] The mouse is big.[(triple12)] The mouse likes the dog.[(triple13)] The mouse likes the lion.[(triple14)] The mouse sees the rabbit.[(triple15)] The rabbit sees the mouse.[(triple16)] @1: The rabbit eats the lion.[(((triple3) -> rule1))]
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple4
The dog likes the lion.
("dog" "likes" "lion" "+")
triple5
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple6
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple7
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple8
The lion is big.
("lion" "is" "big" "+")
triple9
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple10
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple11
The mouse is big.
("mouse" "is" "big" "+")
triple12
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple13
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple14
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple15
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple16
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
((triple3) -> (rule1 % int1))
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int1