The lion needs the mouse. The mouse eats the tiger. The tiger eats the lion. If someone eats the lion then the lion does not visit the mouse. If someone visits the mouse then the mouse needs the tiger. If someone needs the mouse and they do not visit the mouse then they visit the tiger.
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
If someone eats the lion then the lion does not visit the mouse.
((("someone" "eats" "lion" "+")) -> ("lion" "visits" "mouse" "-"))
If someone visits the mouse then the mouse needs the tiger.
((("someone" "visits" "mouse" "+")) -> ("mouse" "needs" "tiger" "+"))
If someone needs the mouse and they do not visit the mouse then they visit the tiger.
((("someone" "needs" "mouse" "+") ("someone" "visits" "mouse" "~")) -> ("someone" "visits" "tiger" "+"))
The lion needs the mouse.
True
1
proof
[(triple1)]
("lion" "needs" "mouse" "+")
triple1
The lion does not need the mouse.
False
1
inv-proof
[(triple1)]
("lion" "needs" "mouse" "-")
triple1
The lion does not visit the mouse.
True
2
proof
[(((triple3) -> rule1))]
("lion" "visits" "mouse" "-")
((triple3) -> (rule1 % int1))
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
int1
The lion visits the mouse.
False
2
inv-proof
[(((triple3) -> rule1))]
("lion" "visits" "mouse" "+")
((triple3) -> (rule1 % int1))
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
int1
The lion visits the tiger.
True
4
proof
[(((triple1 ((triple3) -> rule1)) -> rule3))]
("lion" "visits" "tiger" "+")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
int2
The lion does not visit the tiger.
False
4
inv-proof
[(((triple1 ((triple3) -> rule1)) -> rule3))]
("lion" "visits" "tiger" "-")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
int2
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The mouse visits the tiger.
Unknown
rconc
[@1: The mouse visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "tiger" "+")
The mouse does not need the tiger.
Unknown
inv-rconc
[@1: The mouse needs the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "tiger" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The lion needs the mouse.[(triple1)] The mouse eats the tiger.[(triple2)] The tiger eats the lion.[(triple3)] @1: The lion does not visit the mouse.[(((triple3) -> rule1))] @2: The lion visits the tiger.[(((triple1 ((triple3) -> rule1)) -> rule3))]
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple2
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple3
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
((triple3) -> (rule1 % int1))
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
int2