The lion chases the rabbit. The mouse visits the lion. The rabbit does not visit the mouse. If someone is kind then they eat the rabbit. If the lion is round then the lion chases the rabbit. If someone is big then they chase the lion. If someone is big then they visit the mouse. If the rabbit visits the mouse and the rabbit does not chase the lion then the lion chases the mouse. If someone eats the mouse and they are not round then they do not visit the rabbit. If someone chases the rabbit then they do not visit the rabbit. If someone eats the rabbit and the rabbit does not visit the mouse then they chase the rabbit.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
If someone is kind then they eat the rabbit.
((("someone" "is" "kind" "+")) -> ("someone" "eats" "rabbit" "+"))
If the lion is round then the lion chases the rabbit.
((("lion" "is" "round" "+")) -> ("lion" "chases" "rabbit" "+"))
If someone is big then they chase the lion.
((("someone" "is" "big" "+")) -> ("someone" "chases" "lion" "+"))
If someone is big then they visit the mouse.
((("someone" "is" "big" "+")) -> ("someone" "visits" "mouse" "+"))
If the rabbit visits the mouse and the rabbit does not chase the lion then the lion chases the mouse.
((("rabbit" "visits" "mouse" "+") ("rabbit" "chases" "lion" "~")) -> ("lion" "chases" "mouse" "+"))
If someone eats the mouse and they are not round then they do not visit the rabbit.
((("someone" "eats" "mouse" "+") ("someone" "is" "round" "~")) -> ("someone" "visits" "rabbit" "-"))
If someone chases the rabbit then they do not visit the rabbit.
((("someone" "chases" "rabbit" "+")) -> ("someone" "visits" "rabbit" "-"))
If someone eats the rabbit and the rabbit does not visit the mouse then they chase the rabbit.
((("someone" "eats" "rabbit" "+") ("rabbit" "visits" "mouse" "~")) -> ("someone" "chases" "rabbit" "+"))
The lion chases the rabbit.
True
1
proof
[(triple1)]
("lion" "chases" "rabbit" "+")
triple1
The mouse does not visit the lion.
False
1
inv-proof
[(triple2)]
("mouse" "visits" "lion" "-")
triple2
The lion does not visit the rabbit.
True
2
proof
[(((triple1) -> rule7))]
("lion" "visits" "rabbit" "-")
((triple1) -> (rule7 % int1))
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
int1
The lion visits the rabbit.
False
2
inv-proof
[(((triple1) -> rule7))]
("lion" "visits" "rabbit" "+")
((triple1) -> (rule7 % int1))
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
int1
The lion does not chase the lion.
Unknown
inv-rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "chases" "lion" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The mouse does not visit the rabbit.
Unknown
inv-random
[@0: The mouse visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "rabbit" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The lion chases the rabbit.[(triple1)] The mouse visits the lion.[(triple2)] The rabbit does not visit the mouse.[(triple3)] @1: The lion does not visit the rabbit.[(((triple1) -> rule7))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple2
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
triple3
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
((triple1) -> (rule7 % int1))
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
int1