The lion is green. The rabbit likes the lion. If the lion is green then the lion likes the rabbit. If something likes the rabbit then it is not kind.
The lion is green.
("lion" "is" "green" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
If the lion is green then the lion likes the rabbit.
((("lion" "is" "green" "+")) -> ("lion" "likes" "rabbit" "+"))
If something likes the rabbit then it is not kind.
((("something" "likes" "rabbit" "+")) -> ("something" "is" "kind" "-"))
The rabbit likes the lion.
True
1
proof
[(triple2)]
("rabbit" "likes" "lion" "+")
triple2
The rabbit does not like the lion.
False
1
inv-proof
[(triple2)]
("rabbit" "likes" "lion" "-")
triple2
The lion likes the rabbit.
True
2
proof
[(((triple1) -> rule1))]
("lion" "likes" "rabbit" "+")
((triple1) -> (rule1 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The lion does not like the rabbit.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "likes" "rabbit" "-")
((triple1) -> (rule1 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The lion is not kind.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("lion" "is" "kind" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion is not kind.
("lion" "is" "kind" "-")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2
The lion is kind.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("lion" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion is not kind.
("lion" "is" "kind" "-")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The lion visits the rabbit.
Unknown
random
[@0: The lion visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "rabbit" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The lion is green.[(triple1)] The rabbit likes the lion.[(triple2)] @1: The lion likes the rabbit.[(((triple1) -> rule1))] @2: The lion is not kind.[(((((triple1) -> rule1)) -> rule2))]
The lion is green.
("lion" "is" "green" "+")
triple1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
((triple1) -> (rule1 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The lion is not kind.
("lion" "is" "kind" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion is not kind.
("lion" "is" "kind" "-")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2