The bear is big. The bear is nice. The bear likes the lion. The bear needs the mouse. The lion chases the bear. The lion is green. The lion is young. The lion likes the bear. The mouse chases the bear. The mouse chases the lion. The mouse is nice. The mouse needs the lion. If someone chases the bear then the bear needs the lion. If someone needs the mouse and the mouse likes the bear then the mouse is young. If someone likes the mouse and they are green then they like the lion. If someone is big then they need the bear. If someone likes the bear then they are big. If someone chases the lion then they like the bear.
The bear is big.
("bear" "is" "big" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
If someone chases the bear then the bear needs the lion.
((("someone" "chases" "bear" "+")) -> ("bear" "needs" "lion" "+"))
If someone needs the mouse and the mouse likes the bear then the mouse is young.
((("someone" "needs" "mouse" "+") ("mouse" "likes" "bear" "+")) -> ("mouse" "is" "young" "+"))
If someone likes the mouse and they are green then they like the lion.
((("someone" "likes" "mouse" "+") ("someone" "is" "green" "+")) -> ("someone" "likes" "lion" "+"))
If someone is big then they need the bear.
((("someone" "is" "big" "+")) -> ("someone" "needs" "bear" "+"))
If someone likes the bear then they are big.
((("someone" "likes" "bear" "+")) -> ("someone" "is" "big" "+"))
If someone chases the lion then they like the bear.
((("someone" "chases" "lion" "+")) -> ("someone" "likes" "bear" "+"))
The lion chases the bear.
True
1
proof
[(triple5)]
("lion" "chases" "bear" "+")
triple5
The lion does not like the bear.
False
1
inv-proof
[(triple8)]
("lion" "likes" "bear" "-")
triple8
The lion is big.
True
2
proof
[(((triple8) -> rule5))]
("lion" "is" "big" "+")
((triple8) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is not big.
False
2
inv-proof
[(((triple8) -> rule5))]
("lion" "is" "big" "-")
((triple8) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion needs the bear.
True
3
proof
[(((((triple8) -> rule5)) -> rule4))]
("lion" "needs" "bear" "+")
((((triple8) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The mouse is not young.
False
4
inv-proof
[(((triple4 ((triple10) -> rule6)) -> rule2))]
("mouse" "is" "young" "-")
((triple4 ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int2
The mouse needs the bear.
True
4
proof
[(((((((triple10) -> rule6)) -> rule5)) -> rule4))]
("mouse" "needs" "bear" "+")
((((((triple10) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int3
The mouse does not need the bear.
False
4
inv-proof
[(((((((triple10) -> rule6)) -> rule5)) -> rule4))]
("mouse" "needs" "bear" "-")
((((((triple10) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int3
The bear does not like the bear.
Unknown
inv-rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "likes" "bear" "-")
The mouse likes the lion.
Unknown
rconc
[@1: The mouse likes the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "likes" "lion" "+")
The lion does not like the lion.
Unknown
inv-rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "likes" "lion" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
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 mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The bear is big.[(triple1)] The bear is nice.[(triple2)] The bear likes the lion.[(triple3)] The bear needs the mouse.[(triple4)] The lion chases the bear.[(triple5)] The lion is green.[(triple6)] The lion is young.[(triple7)] The lion likes the bear.[(triple8)] The mouse chases the bear.[(triple9)] The mouse chases the lion.[(triple10)] The mouse is nice.[(triple11)] The mouse needs the lion.[(triple12)] @1: The bear needs the bear.[(((triple1) -> rule4))] The bear needs the lion.[(((triple5) -> rule1) OR ((triple9) -> rule1))] The lion is big.[(((triple8) -> rule5))] The mouse likes the bear.[(((triple10) -> rule6))] @2: The lion needs the bear.[(((((triple8) -> rule5)) -> rule4))] The mouse is big.[(((((triple10) -> rule6)) -> rule5))] The mouse is young.[(((triple4 ((triple10) -> rule6)) -> rule2))] @3: The mouse needs the bear.[(((((((triple10) -> rule6)) -> rule5)) -> rule4))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear likes the lion.
("bear" "likes" "lion" "+")
triple3
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple4
The lion chases the bear.
("lion" "chases" "bear" "+")
triple5
The lion is green.
("lion" "is" "green" "+")
triple6
The lion is young.
("lion" "is" "young" "+")
triple7
The lion likes the bear.
("lion" "likes" "bear" "+")
triple8
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple9
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple10
The mouse is nice.
("mouse" "is" "nice" "+")
triple11
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple12
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple1) -> (rule4 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
((triple5) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
((triple9) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((triple8) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
((triple10) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
((((triple8) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
((((triple10) -> (rule6 % int2))) -> (rule5 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
((triple4 ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((((((triple10) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int3