The bear needs the lion. The cat sees the lion. The lion chases the rabbit. The rabbit needs the cat. If something sees the lion then the lion needs the rabbit. If something chases the lion then the lion is rough.
The bear needs the lion.
("bear" "needs" "lion" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If something sees the lion then the lion needs the rabbit.
((("something" "sees" "lion" "+")) -> ("lion" "needs" "rabbit" "+"))
If something chases the lion then the lion is rough.
((("something" "chases" "lion" "+")) -> ("lion" "is" "rough" "+"))
The rabbit needs the cat.
True
1
proof
[(triple4)]
("rabbit" "needs" "cat" "+")
triple4
The bear does not need the lion.
False
1
inv-proof
[(triple1)]
("bear" "needs" "lion" "-")
triple1
The lion needs the rabbit.
True
2
proof
[(((triple2) -> rule1))]
("lion" "needs" "rabbit" "+")
((triple2) -> (rule1 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The lion does not need the rabbit.
False
2
inv-proof
[(((triple2) -> rule1))]
("lion" "needs" "rabbit" "-")
((triple2) -> (rule1 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The lion is not rough.
Unknown
inv-rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "rough" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The cat does not chase the bear.
Unknown
inv-random
[@0: The cat chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "bear" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
@0: The bear needs the lion.[(triple1)] The cat sees the lion.[(triple2)] The lion chases the rabbit.[(triple3)] The rabbit needs the cat.[(triple4)] @1: The lion needs the rabbit.[(((triple2) -> rule1))]
The bear needs the lion.
("bear" "needs" "lion" "+")
triple1
The cat sees the lion.
("cat" "sees" "lion" "+")
triple2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple3
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple4
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
((triple2) -> (rule1 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1