The bear eats the mouse. The bear is kind. The bear likes the lion. The bear sees the mouse. The cat eats the lion. The cat eats the mouse. The cat is kind. The cat is young. The cat likes the bear. The cat likes the lion. The lion likes the mouse. The mouse eats the bear. The mouse eats the cat. The mouse is young. The mouse likes the lion. The mouse sees the bear. If someone eats the cat and they see the cat then they see the mouse. If someone sees the cat then they are green. If someone likes the bear then the bear sees the lion. If someone sees the bear then they are kind. If someone is young and they like the mouse then the mouse eats the lion. If someone sees the mouse and the mouse sees the cat then they see the cat.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
If someone eats the cat and they see the cat then they see the mouse.
((("someone" "eats" "cat" "+") ("someone" "sees" "cat" "+")) -> ("someone" "sees" "mouse" "+"))
If someone sees the cat then they are green.
((("someone" "sees" "cat" "+")) -> ("someone" "is" "green" "+"))
If someone likes the bear then the bear sees the lion.
((("someone" "likes" "bear" "+")) -> ("bear" "sees" "lion" "+"))
If someone sees the bear then they are kind.
((("someone" "sees" "bear" "+")) -> ("someone" "is" "kind" "+"))
If someone is young and they like the mouse then the mouse eats the lion.
((("someone" "is" "young" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "eats" "lion" "+"))
If someone sees the mouse and the mouse sees the cat then they see the cat.
((("someone" "sees" "mouse" "+") ("mouse" "sees" "cat" "+")) -> ("someone" "sees" "cat" "+"))
The mouse eats the cat.
True
1
proof
[(triple13)]
("mouse" "eats" "cat" "+")
triple13
The cat does not like the lion.
False
1
inv-proof
[(triple10)]
("cat" "likes" "lion" "-")
triple10
The bear sees the lion.
True
2
proof
[(((triple9) -> rule3))]
("bear" "sees" "lion" "+")
((triple9) -> (rule3 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The mouse is not kind.
False
2
inv-proof
[(((triple16) -> rule4))]
("mouse" "is" "kind" "-")
((triple16) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse does not eat the lion.
Unknown
inv-rconc
[@1: The mouse eats the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "eats" "lion" "-")
The lion is green.
Unknown
rconc
[@2: The lion is green.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("lion" "is" "green" "+")
The lion does not see the bear.
Unknown
inv-random
[@0: The lion sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bear" "-")
The lion likes the cat.
Unknown
random
[@0: The lion likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cat" "+")
@0: The bear eats the mouse.[(triple1)] The bear is kind.[(triple2)] The bear likes the lion.[(triple3)] The bear sees the mouse.[(triple4)] The cat eats the lion.[(triple5)] The cat eats the mouse.[(triple6)] The cat is kind.[(triple7)] The cat is young.[(triple8)] The cat likes the bear.[(triple9)] The cat likes the lion.[(triple10)] The lion likes the mouse.[(triple11)] The mouse eats the bear.[(triple12)] The mouse eats the cat.[(triple13)] The mouse is young.[(triple14)] The mouse likes the lion.[(triple15)] The mouse sees the bear.[(triple16)] @1: The bear sees the lion.[(((triple9) -> rule3))] The mouse is kind.[(((triple16) -> rule4))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear likes the lion.
("bear" "likes" "lion" "+")
triple3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple4
The cat eats the lion.
("cat" "eats" "lion" "+")
triple5
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple6
The cat is kind.
("cat" "is" "kind" "+")
triple7
The cat is young.
("cat" "is" "young" "+")
triple8
The cat likes the bear.
("cat" "likes" "bear" "+")
triple9
The cat likes the lion.
("cat" "likes" "lion" "+")
triple10
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple11
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple12
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple13
The mouse is young.
("mouse" "is" "young" "+")
triple14
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple15
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple16
The bear sees the lion.
("bear" "sees" "lion" "+")
((triple9) -> (rule3 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((triple16) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1