The lion is blue. The lion is cold. The lion likes the mouse. The lion needs the mouse. The lion sees the mouse. The mouse is rough. The mouse needs the lion. If someone likes the lion then they like the mouse. If someone sees the lion and they need the mouse then the lion sees the mouse. If someone is cold then they see the lion. If someone sees the lion then the lion likes the mouse. If someone likes the lion and the lion needs the mouse then the lion likes the mouse. If someone needs the mouse and the mouse likes the lion then they like the mouse.
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
If someone likes the lion then they like the mouse.
((("someone" "likes" "lion" "+")) -> ("someone" "likes" "mouse" "+"))
If someone sees the lion and they need the mouse then the lion sees the mouse.
((("someone" "sees" "lion" "+") ("someone" "needs" "mouse" "+")) -> ("lion" "sees" "mouse" "+"))
If someone is cold then they see the lion.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the lion then the lion likes the mouse.
((("someone" "sees" "lion" "+")) -> ("lion" "likes" "mouse" "+"))
If someone likes the lion and the lion needs the mouse then the lion likes the mouse.
((("someone" "likes" "lion" "+") ("lion" "needs" "mouse" "+")) -> ("lion" "likes" "mouse" "+"))
If someone needs the mouse and the mouse likes the lion then they like the mouse.
((("someone" "needs" "mouse" "+") ("mouse" "likes" "lion" "+")) -> ("someone" "likes" "mouse" "+"))
The lion is cold.
True
1
proof
[(triple2)]
("lion" "is" "cold" "+")
triple2
The lion is not blue.
False
1
inv-proof
[(triple1)]
("lion" "is" "blue" "-")
triple1
The lion sees the lion.
True
2
proof
[(((triple2) -> rule3))]
("lion" "sees" "lion" "+")
((triple2) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not see the lion.
False
2
inv-proof
[(((triple2) -> rule3))]
("lion" "sees" "lion" "-")
((triple2) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The mouse does not like the mouse.
Unknown
inv-rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse sees the lion.
Unknown
rconc
[@1: The mouse sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "lion" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The lion is blue.[(triple1)] The lion is cold.[(triple2)] The lion likes the mouse.[(triple3 OR ((((triple2) -> rule3)) -> rule4))] The lion needs the mouse.[(triple4)] The lion sees the mouse.[(triple5 OR ((((triple2) -> rule3) triple4) -> rule2))] The mouse is rough.[(triple6)] The mouse needs the lion.[(triple7)] @1: The lion sees the lion.[(((triple2) -> rule3))]
The lion is blue.
("lion" "is" "blue" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple3
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple4
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple5
((((triple2) -> (rule3 % int2)) triple4) -> (rule2 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
triple6
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple7
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple2) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1