The lion needs the mouse. The mouse sees the lion. The rabbit sees the mouse. If something is red then it eats the lion. If something is red and it does not eat the mouse then the mouse needs the lion. If something sees the rabbit then it is not nice. If the lion needs the mouse then the mouse is rough. If something is nice then it needs the mouse. If something needs the mouse and the mouse does not need the lion then the mouse eats the lion. If something eats the lion then the lion eats the rabbit. If the lion is big then the lion eats the rabbit.
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If something is red then it eats the lion.
((("something" "is" "red" "+")) -> ("something" "eats" "lion" "+"))
If something is red and it does not eat the mouse then the mouse needs the lion.
((("something" "is" "red" "+") ("something" "eats" "mouse" "~")) -> ("mouse" "needs" "lion" "+"))
If something sees the rabbit then it is not nice.
((("something" "sees" "rabbit" "+")) -> ("something" "is" "nice" "-"))
If the lion needs the mouse then the mouse is rough.
((("lion" "needs" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If something is nice then it needs the mouse.
((("something" "is" "nice" "+")) -> ("something" "needs" "mouse" "+"))
If something needs the mouse and the mouse does not need the lion then the mouse eats the lion.
((("something" "needs" "mouse" "+") ("mouse" "needs" "lion" "~")) -> ("mouse" "eats" "lion" "+"))
If something eats the lion then the lion eats the rabbit.
((("something" "eats" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
If the lion is big then the lion eats the rabbit.
((("lion" "is" "big" "+")) -> ("lion" "eats" "rabbit" "+"))
The lion needs the mouse.
True
1
proof
[(triple1)]
("lion" "needs" "mouse" "+")
triple1
The rabbit does not see the mouse.
False
1
inv-proof
[(triple3)]
("rabbit" "sees" "mouse" "-")
triple3
The mouse is rough.
True
2
proof
[(((triple1) -> rule4))]
("mouse" "is" "rough" "+")
((triple1) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is not rough.
False
2
inv-proof
[(((triple1) -> rule4))]
("mouse" "is" "rough" "-")
((triple1) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The lion does not eat the rabbit.
Unknown
inv-rconc
[@2: The lion eats the rabbit.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("lion" "eats" "rabbit" "-")
The lion eats the lion.
Unknown
rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "lion" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
@0: The lion needs the mouse.[(triple1)] The mouse sees the lion.[(triple2)] The rabbit sees the mouse.[(triple3)] @1: The mouse is rough.[(((triple1) -> rule4))]
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
((triple1) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1