The bear sees the lion. The bear visits the lion. The dog sees the bear. The dog visits the bear. The dog visits the lion. The lion is nice. The lion needs the bear. If the bear sees the lion then the bear needs the lion. If someone needs the lion and the lion visits the dog then the dog sees the bear. If someone visits the lion and the lion sees the dog then they need the bear.
The bear sees the lion.
("bear" "sees" "lion" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
If the bear sees the lion then the bear needs the lion.
((("bear" "sees" "lion" "+")) -> ("bear" "needs" "lion" "+"))
If someone needs the lion and the lion visits the dog then the dog sees the bear.
((("someone" "needs" "lion" "+") ("lion" "visits" "dog" "+")) -> ("dog" "sees" "bear" "+"))
If someone visits the lion and the lion sees the dog then they need the bear.
((("someone" "visits" "lion" "+") ("lion" "sees" "dog" "+")) -> ("someone" "needs" "bear" "+"))
The dog visits the bear.
True
1
proof
[(triple4)]
("dog" "visits" "bear" "+")
triple4
The bear does not visit the lion.
False
1
inv-proof
[(triple2)]
("bear" "visits" "lion" "-")
triple2
The bear needs the lion.
True
2
proof
[(((triple1) -> rule1))]
("bear" "needs" "lion" "+")
((triple1) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear does not need the lion.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "needs" "lion" "-")
((triple1) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The dog does not need the bear.
Unknown
inv-rconc
[@1: The dog needs the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "bear" "-")
The bear needs the bear.
Unknown
rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "bear" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
@0: The bear sees the lion.[(triple1)] The bear visits the lion.[(triple2)] The dog sees the bear.[(triple3)] The dog visits the bear.[(triple4)] The dog visits the lion.[(triple5)] The lion is nice.[(triple6)] The lion needs the bear.[(triple7)] @1: The bear needs the lion.[(((triple1) -> rule1))]
The bear sees the lion.
("bear" "sees" "lion" "+")
triple1
The bear visits the lion.
("bear" "visits" "lion" "+")
triple2
The dog sees the bear.
("dog" "sees" "bear" "+")
triple3
The dog visits the bear.
("dog" "visits" "bear" "+")
triple4
The dog visits the lion.
("dog" "visits" "lion" "+")
triple5
The lion is nice.
("lion" "is" "nice" "+")
triple6
The lion needs the bear.
("lion" "needs" "bear" "+")
triple7
The bear needs the lion.
("bear" "needs" "lion" "+")
((triple1) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1