The lion needs the rabbit. The rabbit is cold. The rabbit is rough. If someone eats the rabbit and the rabbit needs the lion then the lion needs the rabbit. If someone likes the lion and the lion likes the rabbit then the lion eats the rabbit. If someone is cold then they need the lion.
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
If someone eats the rabbit and the rabbit needs the lion then the lion needs the rabbit.
((("someone" "eats" "rabbit" "+") ("rabbit" "needs" "lion" "+")) -> ("lion" "needs" "rabbit" "+"))
If someone likes the lion and the lion likes the rabbit then the lion eats the rabbit.
((("someone" "likes" "lion" "+") ("lion" "likes" "rabbit" "+")) -> ("lion" "eats" "rabbit" "+"))
If someone is cold then they need the lion.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "lion" "+"))
The lion needs the rabbit.
True
1
proof
[(triple1)]
("lion" "needs" "rabbit" "+")
triple1
The rabbit is not cold.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "cold" "-")
triple2
The rabbit needs the lion.
True
2
proof
[(((triple2) -> rule3))]
("rabbit" "needs" "lion" "+")
((triple2) -> (rule3 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit does not need the lion.
False
2
inv-proof
[(((triple2) -> rule3))]
("rabbit" "needs" "lion" "-")
((triple2) -> (rule3 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The lion does not need the lion.
Unknown
inv-rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "needs" "lion" "-")
The lion eats the rabbit.
Unknown
rconc
[@1: The lion eats the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "eats" "rabbit" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The lion likes the rabbit.
Unknown
random
[@0: The lion likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "rabbit" "+")
@0: The lion needs the rabbit.[(triple1)] The rabbit is cold.[(triple2)] The rabbit is rough.[(triple3)] @1: The rabbit needs the lion.[(((triple2) -> rule3))]
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple1
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple2
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple3
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
((triple2) -> (rule3 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1