The lion sees the rabbit. The mouse is cold. The rabbit sees the lion. If someone sees the rabbit and the rabbit sees the mouse then the mouse sees the lion. If the lion sees the mouse then the mouse eats the lion. If someone sees the lion then the lion eats the rabbit. If someone eats the mouse then the mouse chases the rabbit. If someone chases the mouse and they are nice then they eat the rabbit. If someone eats the mouse then they chase the mouse.
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone sees the rabbit and the rabbit sees the mouse then the mouse sees the lion.
((("someone" "sees" "rabbit" "+") ("rabbit" "sees" "mouse" "+")) -> ("mouse" "sees" "lion" "+"))
If the lion sees the mouse then the mouse eats the lion.
((("lion" "sees" "mouse" "+")) -> ("mouse" "eats" "lion" "+"))
If someone sees the lion then the lion eats the rabbit.
((("someone" "sees" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
If someone eats the mouse then the mouse chases the rabbit.
((("someone" "eats" "mouse" "+")) -> ("mouse" "chases" "rabbit" "+"))
If someone chases the mouse and they are nice then they eat the rabbit.
((("someone" "chases" "mouse" "+") ("someone" "is" "nice" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone eats the mouse then they chase the mouse.
((("someone" "eats" "mouse" "+")) -> ("someone" "chases" "mouse" "+"))
The rabbit sees the lion.
True
1
proof
[(triple3)]
("rabbit" "sees" "lion" "+")
triple3
The mouse is not cold.
False
1
inv-proof
[(triple2)]
("mouse" "is" "cold" "-")
triple2
The lion eats the rabbit.
True
2
proof
[(((triple3) -> rule3))]
("lion" "eats" "rabbit" "+")
((triple3) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion does not eat the rabbit.
False
2
inv-proof
[(((triple3) -> rule3))]
("lion" "eats" "rabbit" "-")
((triple3) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The mouse does not eat the rabbit.
Unknown
inv-rconc
[@1: The mouse eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "eats" "rabbit" "-")
The rabbit chases the mouse.
Unknown
rconc
[@1: The rabbit chases the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "chases" "mouse" "+")
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 mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The lion sees the rabbit.[(triple1)] The mouse is cold.[(triple2)] The rabbit sees the lion.[(triple3)] @1: The lion eats the rabbit.[(((triple3) -> rule3))]
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple3
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
((triple3) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1