The lion chases the rabbit. The lion sees the rabbit. The rabbit likes the lion. If something chases the rabbit then the rabbit sees the lion. If something sees the lion then it chases the lion. If something likes the rabbit and the rabbit chases the lion then the lion chases the rabbit.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
If something chases the rabbit then the rabbit sees the lion.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "sees" "lion" "+"))
If something sees the lion then it chases the lion.
((("something" "sees" "lion" "+")) -> ("something" "chases" "lion" "+"))
If something likes the rabbit and the rabbit chases the lion then the lion chases the rabbit.
((("something" "likes" "rabbit" "+") ("rabbit" "chases" "lion" "+")) -> ("lion" "chases" "rabbit" "+"))
The rabbit likes the lion.
True
1
proof
[(triple3)]
("rabbit" "likes" "lion" "+")
triple3
The rabbit does not like the lion.
False
1
inv-proof
[(triple3)]
("rabbit" "likes" "lion" "-")
triple3
The rabbit sees the lion.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "sees" "lion" "+")
((triple1) -> (rule1 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit does not see the lion.
False
2
inv-proof
[(((triple1) -> rule1))]
("rabbit" "sees" "lion" "-")
((triple1) -> (rule1 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit chases the lion.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("rabbit" "chases" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit does not chase the lion.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("rabbit" "chases" "lion" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The lion does not chase the lion.
Unknown
inv-rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "chases" "lion" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The lion chases the rabbit.[(triple1)] The lion sees the rabbit.[(triple2)] The rabbit likes the lion.[(triple3)] @1: The rabbit sees the lion.[(((triple1) -> rule1))] @2: The rabbit chases the lion.[(((((triple1) -> rule1)) -> rule2))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple2
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple3
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
((triple1) -> (rule1 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2