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