The bear is young. The lion is not cold. The lion likes the mouse. The lion does not need the bear. The lion does not see the mouse. The mouse is kind. The mouse is rough. The mouse likes the bear. The mouse needs the lion. The mouse sees the bear. If the lion needs the bear then the bear is young. If someone sees the bear and the bear likes the lion then the lion is young. If someone likes the lion and they see the mouse then the lion does not need the bear. If the lion needs the mouse then the lion likes the mouse. If someone is young then they like the lion. If someone needs the lion and the lion likes the bear then they do not like the lion. If someone likes the lion and they need the mouse then the mouse does not see the bear. If someone is rough then they like the mouse.
The bear is young.
("bear" "is" "young" "+")
The lion is not cold.
("lion" "is" "cold" "-")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion does not need the bear.
("lion" "needs" "bear" "-")
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
If the lion needs the bear then the bear is young.
((("lion" "needs" "bear" "+")) -> ("bear" "is" "young" "+"))
If someone sees the bear and the bear likes the lion then the lion is young.
((("someone" "sees" "bear" "+") ("bear" "likes" "lion" "+")) -> ("lion" "is" "young" "+"))
If someone likes the lion and they see the mouse then the lion does not need the bear.
((("someone" "likes" "lion" "+") ("someone" "sees" "mouse" "+")) -> ("lion" "needs" "bear" "-"))
If the lion needs the mouse then the lion likes the mouse.
((("lion" "needs" "mouse" "+")) -> ("lion" "likes" "mouse" "+"))
If someone is young then they like the lion.
((("someone" "is" "young" "+")) -> ("someone" "likes" "lion" "+"))
If someone needs the lion and the lion likes the bear then they do not like the lion.
((("someone" "needs" "lion" "+") ("lion" "likes" "bear" "+")) -> ("someone" "likes" "lion" "-"))
If someone likes the lion and they need the mouse then the mouse does not see the bear.
((("someone" "likes" "lion" "+") ("someone" "needs" "mouse" "+")) -> ("mouse" "sees" "bear" "-"))
If someone is rough then they like the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "mouse" "+"))
The bear is young.
True
1
proof
[(triple1)]
("bear" "is" "young" "+")
triple1
The mouse does not like the bear.
False
1
inv-proof
[(triple8)]
("mouse" "likes" "bear" "-")
triple8
The bear likes the lion.
True
2
proof
[(((triple1) -> rule5))]
("bear" "likes" "lion" "+")
((triple1) -> (rule5 % int1))
The bear likes the lion.
("bear" "likes" "lion" "+")
int1
The bear does not like the lion.
False
2
inv-proof
[(((triple1) -> rule5))]
("bear" "likes" "lion" "-")
((triple1) -> (rule5 % int1))
The bear likes the lion.
("bear" "likes" "lion" "+")
int1
The lion is young.
True
4
proof
[(((triple10 ((triple1) -> rule5)) -> rule2))]
("lion" "is" "young" "+")
((triple10 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The bear likes the lion.
("bear" "likes" "lion" "+")
int2
The lion is not young.
False
4
inv-proof
[(((triple10 ((triple1) -> rule5)) -> rule2))]
("lion" "is" "young" "-")
((triple10 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The bear likes the lion.
("bear" "likes" "lion" "+")
int2
The lion likes the lion.
True
5
proof
[(((((triple10 ((triple1) -> rule5)) -> rule2)) -> rule5))]
("lion" "likes" "lion" "+")
((((triple10 ((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The bear likes the lion.
("bear" "likes" "lion" "+")
int3
The lion does not like the lion.
False
5
inv-proof
[(((((triple10 ((triple1) -> rule5)) -> rule2)) -> rule5))]
("lion" "likes" "lion" "-")
((((triple10 ((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The bear likes the lion.
("bear" "likes" "lion" "+")
int3
The mouse does not like the lion.
Unknown
inv-rconc
[@1: The mouse likes the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "likes" "lion" "-")
The bear likes the mouse.
Unknown
rconc
[@1: The bear likes the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "likes" "mouse" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The bear is young.[(triple1)] The lion does not need the bear.[(triple4)] The lion does not see the mouse.[(triple5)] The lion is not cold.[(triple2)] The lion likes the mouse.[(triple3)] The mouse is kind.[(triple6)] The mouse is rough.[(triple7)] The mouse likes the bear.[(triple8)] The mouse needs the lion.[(triple9)] The mouse sees the bear.[(triple10)] @1: The bear likes the lion.[(((triple1) -> rule5))] The mouse likes the mouse.[(((triple7) -> rule8))] @2: The lion is young.[(((triple10 ((triple1) -> rule5)) -> rule2))] @3: The lion likes the lion.[(((((triple10 ((triple1) -> rule5)) -> rule2)) -> rule5))]
The bear is young.
("bear" "is" "young" "+")
triple1
The lion does not need the bear.
("lion" "needs" "bear" "-")
triple4
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
triple5
The lion is not cold.
("lion" "is" "cold" "-")
triple2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple3
The mouse is kind.
("mouse" "is" "kind" "+")
triple6
The mouse is rough.
("mouse" "is" "rough" "+")
triple7
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple8
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple9
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple10
The bear likes the lion.
("bear" "likes" "lion" "+")
((triple1) -> (rule5 % int1))
The bear likes the lion.
("bear" "likes" "lion" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple7) -> (rule8 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The lion is young.
("lion" "is" "young" "+")
((triple10 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The bear likes the lion.
("bear" "likes" "lion" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
((((triple10 ((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The bear likes the lion.
("bear" "likes" "lion" "+")
int3