The lion does not like the mouse. The mouse eats the lion. If someone likes the lion and the lion is rough then they see the mouse. If someone eats the lion then they see the mouse. If someone is rough and they eat the mouse then they are not blue. If someone sees the mouse then they like the lion. If someone is blue and they do not eat the lion then they are rough. If someone likes the lion then the lion is red.
The lion does not like the mouse.
("lion" "likes" "mouse" "-")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
If someone likes the lion and the lion is rough then they see the mouse.
((("someone" "likes" "lion" "+") ("lion" "is" "rough" "+")) -> ("someone" "sees" "mouse" "+"))
If someone eats the lion then they see the mouse.
((("someone" "eats" "lion" "+")) -> ("someone" "sees" "mouse" "+"))
If someone is rough and they eat the mouse then they are not blue.
((("someone" "is" "rough" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "is" "blue" "-"))
If someone sees the mouse then they like the lion.
((("someone" "sees" "mouse" "+")) -> ("someone" "likes" "lion" "+"))
If someone is blue and they do not eat the lion then they are rough.
((("someone" "is" "blue" "+") ("someone" "eats" "lion" "~")) -> ("someone" "is" "rough" "+"))
If someone likes the lion then the lion is red.
((("someone" "likes" "lion" "+")) -> ("lion" "is" "red" "+"))
The mouse eats the lion.
True
1
proof
[(triple2)]
("mouse" "eats" "lion" "+")
triple2
The mouse does not eat the lion.
False
1
inv-proof
[(triple2)]
("mouse" "eats" "lion" "-")
triple2
The mouse sees the mouse.
True
2
proof
[(((triple2) -> rule2))]
("mouse" "sees" "mouse" "+")
((triple2) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse does not see the mouse.
False
2
inv-proof
[(((triple2) -> rule2))]
("mouse" "sees" "mouse" "-")
((triple2) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse likes the lion.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("mouse" "likes" "lion" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse does not like the lion.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4))]
("mouse" "likes" "lion" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The lion is red.
True
4
proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule6))]
("lion" "is" "red" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
The lion is not red.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule6))]
("lion" "is" "red" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
The lion does not see the mouse.
Unknown
inv-rconc
[@2: The lion sees the mouse.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("lion" "sees" "mouse" "-")
The mouse is rough.
Unknown
rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "rough" "+")
The lion does not like the lion.
Unknown
inv-rconc
[@2: The lion likes the lion.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("lion" "likes" "lion" "-")
The lion is rough.
Unknown
rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "rough" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The lion does not like the mouse.[(triple1)] The mouse eats the lion.[(triple2)] @1: The mouse sees the mouse.[(((triple2) -> rule2))] @2: The mouse likes the lion.[(((((triple2) -> rule2)) -> rule4))] @3: The lion is red.[(((((((triple2) -> rule2)) -> rule4)) -> rule6))]
The lion does not like the mouse.
("lion" "likes" "mouse" "-")
triple1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple2) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The lion is red.
("lion" "is" "red" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3