The lion is not green. The lion does not need the rabbit. The mouse is green. The mouse is red. The mouse likes the lion. The mouse likes the rabbit. The mouse needs the rabbit. The rabbit is blue. The rabbit needs the mouse. The rabbit sees the mouse. If the mouse is kind and the mouse is rough then the mouse needs the lion. If the rabbit is kind and the rabbit is green then the rabbit sees the mouse. If someone sees the rabbit then the rabbit likes the mouse. If someone likes the mouse and they like the lion then the mouse sees the lion. If someone sees the mouse then they do not see the lion. If someone sees the lion then the lion is kind. If the rabbit does not see the lion then the lion likes the rabbit. If someone needs the lion and the lion likes the rabbit then the rabbit needs the mouse.
The lion is not green.
("lion" "is" "green" "-")
The lion does not need the rabbit.
("lion" "needs" "rabbit" "-")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If the mouse is kind and the mouse is rough then the mouse needs the lion.
((("mouse" "is" "kind" "+") ("mouse" "is" "rough" "+")) -> ("mouse" "needs" "lion" "+"))
If the rabbit is kind and the rabbit is green then the rabbit sees the mouse.
((("rabbit" "is" "kind" "+") ("rabbit" "is" "green" "+")) -> ("rabbit" "sees" "mouse" "+"))
If someone sees the rabbit then the rabbit likes the mouse.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "likes" "mouse" "+"))
If someone likes the mouse and they like the lion then the mouse sees the lion.
((("someone" "likes" "mouse" "+") ("someone" "likes" "lion" "+")) -> ("mouse" "sees" "lion" "+"))
If someone sees the mouse then they do not see the lion.
((("someone" "sees" "mouse" "+")) -> ("someone" "sees" "lion" "-"))
If someone sees the lion then the lion is kind.
((("someone" "sees" "lion" "+")) -> ("lion" "is" "kind" "+"))
If the rabbit does not see the lion then the lion likes the rabbit.
((("rabbit" "sees" "lion" "~")) -> ("lion" "likes" "rabbit" "+"))
If someone needs the lion and the lion likes the rabbit then the rabbit needs the mouse.
((("someone" "needs" "lion" "+") ("lion" "likes" "rabbit" "+")) -> ("rabbit" "needs" "mouse" "+"))
The mouse is green.
True
1
proof
[(triple3)]
("mouse" "is" "green" "+")
triple3
The mouse does not need the rabbit.
False
1
inv-proof
[(triple7)]
("mouse" "needs" "rabbit" "-")
triple7
The rabbit does not see the lion.
True
2
proof
[(((triple10) -> rule5))]
("rabbit" "sees" "lion" "-")
((triple10) -> (rule5 % int1))
The rabbit does not see the lion.
("rabbit" "sees" "lion" "-")
int1
The rabbit sees the lion.
False
2
inv-proof
[(((triple10) -> rule5))]
("rabbit" "sees" "lion" "+")
((triple10) -> (rule5 % int1))
The rabbit does not see the lion.
("rabbit" "sees" "lion" "-")
int1
The lion likes the rabbit.
True
3
proof
[(((((triple10) -> rule5)) -> rule7))]
("lion" "likes" "rabbit" "+")
((((triple10) -> (rule5 % int2))) -> (rule7 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The rabbit does not see the lion.
("rabbit" "sees" "lion" "-")
int2
The lion does not like the rabbit.
False
3
inv-proof
[(((((triple10) -> rule5)) -> rule7))]
("lion" "likes" "rabbit" "-")
((((triple10) -> (rule5 % int2))) -> (rule7 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The rabbit does not see the lion.
("rabbit" "sees" "lion" "-")
int2
The lion is not kind.
Unknown
inv-rconc
[@2: The lion is kind.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("lion" "is" "kind" "-")
The mouse sees the lion.
Unknown
rconc
[@1: The mouse sees the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "lion" "+")
The mouse does not need the lion.
Unknown
inv-rconc
[@1: The mouse needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "lion" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The rabbit does not need the lion.
Unknown
inv-random
[@0: The rabbit needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "lion" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The lion does not need the rabbit.[(triple2)] The lion is not green.[(triple1)] The mouse is green.[(triple3)] The mouse is red.[(triple4)] The mouse likes the lion.[(triple5)] The mouse likes the rabbit.[(triple6)] The mouse needs the rabbit.[(triple7)] The rabbit is blue.[(triple8)] The rabbit needs the mouse.[(triple9)] The rabbit sees the mouse.[(triple10)] @1: The rabbit does not see the lion.[(((triple10) -> rule5))] @2: The lion likes the rabbit.[(((((triple10) -> rule5)) -> rule7))]
The lion does not need the rabbit.
("lion" "needs" "rabbit" "-")
triple2
The lion is not green.
("lion" "is" "green" "-")
triple1
The mouse is green.
("mouse" "is" "green" "+")
triple3
The mouse is red.
("mouse" "is" "red" "+")
triple4
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple5
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple6
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple7
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple8
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple9
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple10
The rabbit does not see the lion.
("rabbit" "sees" "lion" "-")
((triple10) -> (rule5 % int1))
The rabbit does not see the lion.
("rabbit" "sees" "lion" "-")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
((((triple10) -> (rule5 % int2))) -> (rule7 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The rabbit does not see the lion.
("rabbit" "sees" "lion" "-")
int2