The bear is nice. The bear visits the dog. The dog is young. The dog likes the lion. The dog visits the bear. The lion is cold. The lion is green. The lion is nice. The lion is rough. The lion is young. The lion needs the bear. The lion visits the bear. If someone visits the bear and they are cold then they visit the lion. If someone likes the lion then the lion is cold. If someone needs the bear and they visit the lion then the bear visits the lion.
The bear is nice.
("bear" "is" "nice" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
If someone visits the bear and they are cold then they visit the lion.
((("someone" "visits" "bear" "+") ("someone" "is" "cold" "+")) -> ("someone" "visits" "lion" "+"))
If someone likes the lion then the lion is cold.
((("someone" "likes" "lion" "+")) -> ("lion" "is" "cold" "+"))
If someone needs the bear and they visit the lion then the bear visits the lion.
((("someone" "needs" "bear" "+") ("someone" "visits" "lion" "+")) -> ("bear" "visits" "lion" "+"))
The lion is cold.
True
1
proof
[(triple6 OR ((triple4) -> rule2))]
("lion" "is" "cold" "+")
triple6
((triple4) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is not green.
False
1
inv-proof
[(triple7)]
("lion" "is" "green" "-")
triple7
The lion visits the lion.
True
3
proof
[(((triple12 triple6) -> rule1) OR ((triple12 ((triple4) -> rule2)) -> rule1))]
("lion" "visits" "lion" "+")
((triple12 triple6) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
((triple12 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion does not visit the lion.
False
3
inv-proof
[(((triple12 triple6) -> rule1) OR ((triple12 ((triple4) -> rule2)) -> rule1))]
("lion" "visits" "lion" "-")
((triple12 triple6) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
((triple12 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The bear visits the lion.
True
5
proof
[(((triple11 ((triple12 triple6) -> rule1)) -> rule3) OR ((triple11 ((triple12 ((triple4) -> rule2)) -> rule1)) -> rule3))]
("bear" "visits" "lion" "+")
((triple11 ((triple12 triple6) -> (rule1 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
((triple11 ((triple12 ((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The bear does not visit the lion.
False
5
inv-proof
[(((triple11 ((triple12 triple6) -> rule1)) -> rule3) OR ((triple11 ((triple12 ((triple4) -> rule2)) -> rule1)) -> rule3))]
("bear" "visits" "lion" "-")
((triple11 ((triple12 triple6) -> (rule1 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
((triple11 ((triple12 ((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The dog does not visit the lion.
Unknown
inv-rconc
[@1: The dog visits the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "lion" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The lion does not like the bear.
Unknown
inv-random
[@0: The lion likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "bear" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
@0: The bear is nice.[(triple1)] The bear visits the dog.[(triple2)] The dog is young.[(triple3)] The dog likes the lion.[(triple4)] The dog visits the bear.[(triple5)] The lion is cold.[(triple6 OR ((triple4) -> rule2))] The lion is green.[(triple7)] The lion is nice.[(triple8)] The lion is rough.[(triple9)] The lion is young.[(triple10)] The lion needs the bear.[(triple11)] The lion visits the bear.[(triple12)] @1: The lion visits the lion.[(((triple12 triple6) -> rule1) OR ((triple12 ((triple4) -> rule2)) -> rule1))] @2: The bear visits the lion.[(((triple11 ((triple12 triple6) -> rule1)) -> rule3) OR ((triple11 ((triple12 ((triple4) -> rule2)) -> rule1)) -> rule3))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The bear visits the dog.
("bear" "visits" "dog" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
The dog likes the lion.
("dog" "likes" "lion" "+")
triple4
The dog visits the bear.
("dog" "visits" "bear" "+")
triple5
The lion is cold.
("lion" "is" "cold" "+")
triple6
((triple4) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is green.
("lion" "is" "green" "+")
triple7
The lion is nice.
("lion" "is" "nice" "+")
triple8
The lion is rough.
("lion" "is" "rough" "+")
triple9
The lion is young.
("lion" "is" "young" "+")
triple10
The lion needs the bear.
("lion" "needs" "bear" "+")
triple11
The lion visits the bear.
("lion" "visits" "bear" "+")
triple12
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple12 triple6) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
((triple12 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The bear visits the lion.
("bear" "visits" "lion" "+")
((triple11 ((triple12 triple6) -> (rule1 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
((triple11 ((triple12 ((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3