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