The lion visits the mouse. The mouse eats the lion. If the mouse likes the lion then the mouse is green. If the lion visits the mouse then the mouse likes the lion. If someone eats the mouse and they are young then the mouse likes the lion. If the mouse does not visit the lion then the mouse likes the lion. If the lion eats the mouse then the mouse does not like the lion. If someone likes the lion and they are young then the lion is green.
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
If the mouse likes the lion then the mouse is green.
((("mouse" "likes" "lion" "+")) -> ("mouse" "is" "green" "+"))
If the lion visits the mouse then the mouse likes the lion.
((("lion" "visits" "mouse" "+")) -> ("mouse" "likes" "lion" "+"))
If someone eats the mouse and they are young then the mouse likes the lion.
((("someone" "eats" "mouse" "+") ("someone" "is" "young" "+")) -> ("mouse" "likes" "lion" "+"))
If the mouse does not visit the lion then the mouse likes the lion.
((("mouse" "visits" "lion" "~")) -> ("mouse" "likes" "lion" "+"))
If the lion eats the mouse then the mouse does not like the lion.
((("lion" "eats" "mouse" "+")) -> ("mouse" "likes" "lion" "-"))
If someone likes the lion and they are young then the lion is green.
((("someone" "likes" "lion" "+") ("someone" "is" "young" "+")) -> ("lion" "is" "green" "+"))
The mouse eats the lion.
True
1
proof
[(triple2)]
("mouse" "eats" "lion" "+")
triple2
The mouse does not eat the lion.
False
1
inv-proof
[(triple2)]
("mouse" "eats" "lion" "-")
triple2
The mouse likes the lion.
True
2
proof
[(((triple1) -> rule2))]
("mouse" "likes" "lion" "+")
((triple1) -> (rule2 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse does not like the lion.
False
2
inv-proof
[(((triple1) -> rule2))]
("mouse" "likes" "lion" "-")
((triple1) -> (rule2 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse is green.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("mouse" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The mouse is not green.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("mouse" "is" "green" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The lion is not green.
Unknown
inv-rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "green" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
@0: The lion visits the mouse.[(triple1)] The mouse eats the lion.[(triple2)] @1: The mouse likes the lion.[(((triple1) -> rule2))] @2: The mouse is green.[(((((triple1) -> rule2)) -> rule1))]
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple2
The mouse likes the lion.
("mouse" "likes" "lion" "+")
((triple1) -> (rule2 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2