The bear does not see the lion. The bear does not visit the tiger. The lion needs the bear. The lion sees the tiger. The lion visits the bear. The rabbit needs the bear. The rabbit visits the lion. The tiger does not need the bear. The tiger sees the lion. The tiger sees the rabbit. The tiger visits the bear. The tiger visits the lion. If something visits the lion then the lion is rough. If the lion needs the bear then the bear is kind. If something is kind and it visits the lion then it sees the lion.
The bear does not see the lion.
("bear" "sees" "lion" "-")
The bear does not visit the tiger.
("bear" "visits" "tiger" "-")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
The tiger does not need the bear.
("tiger" "needs" "bear" "-")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something visits the lion then the lion is rough.
((("something" "visits" "lion" "+")) -> ("lion" "is" "rough" "+"))
If the lion needs the bear then the bear is kind.
((("lion" "needs" "bear" "+")) -> ("bear" "is" "kind" "+"))
If something is kind and it visits the lion then it sees the lion.
((("something" "is" "kind" "+") ("something" "visits" "lion" "+")) -> ("something" "sees" "lion" "+"))
The tiger visits the lion.
True
1
proof
[(triple12)]
("tiger" "visits" "lion" "+")
triple12
The bear visits the tiger.
False
1
inv-proof
[(triple2)]
("bear" "visits" "tiger" "+")
triple2
The bear is kind.
True
2
proof
[(((triple3) -> rule2))]
("bear" "is" "kind" "+")
((triple3) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The lion is not rough.
False
2
inv-proof
[(((triple12) -> rule1) OR ((triple7) -> rule1))]
("lion" "is" "rough" "-")
((triple12) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((triple7) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The rabbit does not see the lion.
Unknown
inv-rconc
[@1: The rabbit sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "sees" "lion" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "sees" "lion" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The tiger needs the rabbit.
Unknown
random
[@0: The tiger needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "rabbit" "+")
@0: The bear does not see the lion.[(triple1)] The bear does not visit the tiger.[(triple2)] The lion needs the bear.[(triple3)] The lion sees the tiger.[(triple4)] The lion visits the bear.[(triple5)] The rabbit needs the bear.[(triple6)] The rabbit visits the lion.[(triple7)] The tiger does not need the bear.[(triple8)] The tiger sees the lion.[(triple9)] The tiger sees the rabbit.[(triple10)] The tiger visits the bear.[(triple11)] The tiger visits the lion.[(triple12)] @1: The bear is kind.[(((triple3) -> rule2))] The lion is rough.[(((triple12) -> rule1) OR ((triple7) -> rule1))]
The bear does not see the lion.
("bear" "sees" "lion" "-")
triple1
The bear does not visit the tiger.
("bear" "visits" "tiger" "-")
triple2
The lion needs the bear.
("lion" "needs" "bear" "+")
triple3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple4
The lion visits the bear.
("lion" "visits" "bear" "+")
triple5
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple6
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple7
The tiger does not need the bear.
("tiger" "needs" "bear" "-")
triple8
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple9
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple10
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple11
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple12
The bear is kind.
("bear" "is" "kind" "+")
((triple3) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((triple12) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((triple7) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1