The lion eats the mouse. The lion eats the rabbit. The lion visits the mouse. The lion visits the rabbit. The mouse sees the lion. The mouse visits the rabbit. The rabbit eats the mouse. If someone visits the mouse and they eat the mouse then the mouse is young. If someone is blue then they see the lion. If the mouse eats the lion then the mouse sees the lion.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
If someone visits the mouse and they eat the mouse then the mouse is young.
((("someone" "visits" "mouse" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If someone is blue then they see the lion.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "lion" "+"))
If the mouse eats the lion then the mouse sees the lion.
((("mouse" "eats" "lion" "+")) -> ("mouse" "sees" "lion" "+"))
The mouse visits the rabbit.
True
1
proof
[(triple6)]
("mouse" "visits" "rabbit" "+")
triple6
The lion does not eat the rabbit.
False
1
inv-proof
[(triple2)]
("lion" "eats" "rabbit" "-")
triple2
The mouse is young.
True
3
proof
[(((triple3 triple1) -> rule1))]
("mouse" "is" "young" "+")
((triple3 triple1) -> (rule1 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is not young.
False
3
inv-proof
[(((triple3 triple1) -> rule1))]
("mouse" "is" "young" "-")
((triple3 triple1) -> (rule1 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The rabbit does not see the lion.
Unknown
inv-rconc
[@1: The rabbit sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "lion" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "lion" "+")
The mouse does not eat the lion.
Unknown
inv-random
[@0: The mouse eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "lion" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The lion eats the mouse.[(triple1)] The lion eats the rabbit.[(triple2)] The lion visits the mouse.[(triple3)] The lion visits the rabbit.[(triple4)] The mouse sees the lion.[(triple5)] The mouse visits the rabbit.[(triple6)] The rabbit eats the mouse.[(triple7)] @1: The mouse is young.[(((triple3 triple1) -> rule1))]
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple3
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple4
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple5
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple6
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple7
The mouse is young.
("mouse" "is" "young" "+")
((triple3 triple1) -> (rule1 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1