The bear is blue. The bear is cold. The bear is red. The bear is young. The bear needs the lion. The bear sees the lion. The bear visits the lion. The lion is blue. The lion is cold. The lion is green. The lion is red. The lion is young. The lion needs the bear. The lion sees the bear. The lion visits the bear. If someone visits the lion then the lion visits the bear. If someone needs the lion then they visit the lion.
The bear is blue.
("bear" "is" "blue" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
If someone visits the lion then the lion visits the bear.
((("someone" "visits" "lion" "+")) -> ("lion" "visits" "bear" "+"))
If someone needs the lion then they visit the lion.
((("someone" "needs" "lion" "+")) -> ("someone" "visits" "lion" "+"))
The lion visits the bear.
True
1
proof
[(triple15 OR ((triple7) -> rule1) OR ((((triple5) -> rule2)) -> rule1))]
("lion" "visits" "bear" "+")
triple15
((triple7) -> (rule1 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The lion is not red.
False
1
inv-proof
[(triple11)]
("lion" "is" "red" "-")
triple11
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "lion" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear is blue.[(triple1)] The bear is cold.[(triple2)] The bear is red.[(triple3)] The bear is young.[(triple4)] The bear needs the lion.[(triple5)] The bear sees the lion.[(triple6)] The bear visits the lion.[(triple7 OR ((triple5) -> rule2))] The lion is blue.[(triple8)] The lion is cold.[(triple9)] The lion is green.[(triple10)] The lion is red.[(triple11)] The lion is young.[(triple12)] The lion needs the bear.[(triple13)] The lion sees the bear.[(triple14)] The lion visits the bear.[(triple15 OR ((triple7) -> rule1) OR ((((triple5) -> rule2)) -> rule1))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
The bear is young.
("bear" "is" "young" "+")
triple4
The bear needs the lion.
("bear" "needs" "lion" "+")
triple5
The bear sees the lion.
("bear" "sees" "lion" "+")
triple6
The bear visits the lion.
("bear" "visits" "lion" "+")
triple7
((triple5) -> (rule2 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
triple8
The lion is cold.
("lion" "is" "cold" "+")
triple9
The lion is green.
("lion" "is" "green" "+")
triple10
The lion is red.
("lion" "is" "red" "+")
triple11
The lion is young.
("lion" "is" "young" "+")
triple12
The lion needs the bear.
("lion" "needs" "bear" "+")
triple13
The lion sees the bear.
("lion" "sees" "bear" "+")
triple14
The lion visits the bear.
("lion" "visits" "bear" "+")
triple15
((triple7) -> (rule1 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2