The lion likes the rabbit. The rabbit likes the lion. If the rabbit likes the lion then the rabbit needs the lion. If someone is green and they see the lion then the lion needs the rabbit. If someone needs the rabbit and the rabbit sees the lion then they are young. If someone needs the lion then the lion sees the rabbit. If someone likes the lion and they are not cold then they are not green. If someone is red then they like the lion. If someone sees the rabbit and the rabbit does not like the lion then they do not like the rabbit. If someone likes the rabbit then the rabbit is not nice.
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
If the rabbit likes the lion then the rabbit needs the lion.
((("rabbit" "likes" "lion" "+")) -> ("rabbit" "needs" "lion" "+"))
If someone is green and they see the lion then the lion needs the rabbit.
((("someone" "is" "green" "+") ("someone" "sees" "lion" "+")) -> ("lion" "needs" "rabbit" "+"))
If someone needs the rabbit and the rabbit sees the lion then they are young.
((("someone" "needs" "rabbit" "+") ("rabbit" "sees" "lion" "+")) -> ("someone" "is" "young" "+"))
If someone needs the lion then the lion sees the rabbit.
((("someone" "needs" "lion" "+")) -> ("lion" "sees" "rabbit" "+"))
If someone likes the lion and they are not cold then they are not green.
((("someone" "likes" "lion" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "green" "-"))
If someone is red then they like the lion.
((("someone" "is" "red" "+")) -> ("someone" "likes" "lion" "+"))
If someone sees the rabbit and the rabbit does not like the lion then they do not like the rabbit.
((("someone" "sees" "rabbit" "+") ("rabbit" "likes" "lion" "~")) -> ("someone" "likes" "rabbit" "-"))
If someone likes the rabbit then the rabbit is not nice.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "nice" "-"))
The rabbit likes the lion.
True
1
proof
[(triple2)]
("rabbit" "likes" "lion" "+")
triple2
The lion does not like the rabbit.
False
1
inv-proof
[(triple1)]
("lion" "likes" "rabbit" "-")
triple1
The rabbit needs the lion.
True
2
proof
[(((triple2) -> rule1))]
("rabbit" "needs" "lion" "+")
((triple2) -> (rule1 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit is nice.
False
2
inv-proof
[(((triple1) -> rule8))]
("rabbit" "is" "nice" "+")
((triple1) -> (rule8 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The lion sees the rabbit.
True
3
proof
[(((((triple2) -> rule1)) -> rule4))]
("lion" "sees" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The lion does not see the rabbit.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4))]
("lion" "sees" "rabbit" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The lion is not young.
Unknown
inv-rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "young" "-")
The lion likes the lion.
Unknown
rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "likes" "lion" "+")
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "young" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
The rabbit is not green.
Unknown
inv-random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
@0: The lion likes the rabbit.[(triple1)] The rabbit likes the lion.[(triple2)] @1: The rabbit is not nice.[(((triple1) -> rule8))] The rabbit needs the lion.[(((triple2) -> rule1))] @2: The lion sees the rabbit.[(((((triple2) -> rule1)) -> rule4))]
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple2
The rabbit is not nice.
("rabbit" "is" "nice" "-")
((triple1) -> (rule8 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
((triple2) -> (rule1 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2