The lion likes the mouse. The mouse visits the lion. If someone is big then they need the lion. If someone visits the lion then they are red.
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If someone is big then they need the lion.
((("someone" "is" "big" "+")) -> ("someone" "needs" "lion" "+"))
If someone visits the lion then they are red.
((("someone" "visits" "lion" "+")) -> ("someone" "is" "red" "+"))
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 red.
True
2
proof
[(((triple2) -> rule2))]
("mouse" "is" "red" "+")
((triple2) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is not red.
False
2
inv-proof
[(((triple2) -> rule2))]
("mouse" "is" "red" "-")
((triple2) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse does not need the lion.
Unknown
inv-rconc
[@1: The mouse needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "lion" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "lion" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
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 likes the mouse.[(triple1)] The mouse visits the lion.[(triple2)] @1: The mouse is red.[(((triple2) -> rule2))]
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple2
The mouse is red.
("mouse" "is" "red" "+")
((triple2) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1