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