The lion is kind. The lion is not nice. The lion likes the rabbit. The lion needs the rabbit. The lion visits the rabbit. The rabbit is not nice. The rabbit does not need the lion. If something visits the rabbit then it likes the lion. If something is kind and it likes the lion then it does not need the lion. If something needs the lion and it is not nice then it visits the lion.
The lion is kind.
("lion" "is" "kind" "+")
The lion is not nice.
("lion" "is" "nice" "-")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit is not nice.
("rabbit" "is" "nice" "-")
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
If something visits the rabbit then it likes the lion.
((("something" "visits" "rabbit" "+")) -> ("something" "likes" "lion" "+"))
If something is kind and it likes the lion then it does not need the lion.
((("something" "is" "kind" "+") ("something" "likes" "lion" "+")) -> ("something" "needs" "lion" "-"))
If something needs the lion and it is not nice then it visits the lion.
((("something" "needs" "lion" "+") ("something" "is" "nice" "~")) -> ("something" "visits" "lion" "+"))
The lion is kind.
True
1
proof
[(triple1)]
("lion" "is" "kind" "+")
triple1
The rabbit needs the lion.
False
1
inv-proof
[(triple7)]
("rabbit" "needs" "lion" "+")
triple7
The lion likes the lion.
True
2
proof
[(((triple5) -> rule1))]
("lion" "likes" "lion" "+")
((triple5) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion does not like the lion.
False
2
inv-proof
[(((triple5) -> rule1))]
("lion" "likes" "lion" "-")
((triple5) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion does not need the lion.
True
4
proof
[(((triple1 ((triple5) -> rule1)) -> rule2))]
("lion" "needs" "lion" "-")
((triple1 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The lion does not need the lion.
("lion" "needs" "lion" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion needs the lion.
False
4
inv-proof
[(((triple1 ((triple5) -> rule1)) -> rule2))]
("lion" "needs" "lion" "+")
((triple1 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The lion does not need the lion.
("lion" "needs" "lion" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The rabbit does not like the lion.
Unknown
inv-rconc
[@1: The rabbit likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "likes" "lion" "-")
The lion visits the lion.
Unknown
rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "visits" "lion" "+")
The rabbit does not visit the lion.
Unknown
inv-rconc
[@1: The rabbit visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "visits" "lion" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The lion is kind.[(triple1)] The lion is not nice.[(triple2)] The lion likes the rabbit.[(triple3)] The lion needs the rabbit.[(triple4)] The lion visits the rabbit.[(triple5)] The rabbit does not need the lion.[(triple7)] The rabbit is not nice.[(triple6)] @1: The lion likes the lion.[(((triple5) -> rule1))] @2: The lion does not need the lion.[(((triple1 ((triple5) -> rule1)) -> rule2))]
The lion is kind.
("lion" "is" "kind" "+")
triple1
The lion is not nice.
("lion" "is" "nice" "-")
triple2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple3
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple4
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple5
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
triple7
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple6
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple5) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion does not need the lion.
("lion" "needs" "lion" "-")
((triple1 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The lion does not need the lion.
("lion" "needs" "lion" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2