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