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