The lion is young. The lion needs the mouse. The mouse is not nice. The mouse does not like the lion. The mouse likes the squirrel. The squirrel chases the mouse. The squirrel is nice. The squirrel is young. The squirrel likes the mouse. The squirrel needs the mouse. If something needs the lion and it is nice then the lion needs the squirrel. If something needs the lion then the lion chases the squirrel. If something likes the lion then it does not need the lion. If something needs the squirrel then it needs the lion. If something needs the mouse then the mouse needs the squirrel. If something chases the lion and it needs the squirrel then the squirrel likes the mouse. If something chases the mouse and it is cold then it chases the lion. If something likes the mouse then it is big.
The lion is young.
("lion" "is" "young" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse is not nice.
("mouse" "is" "nice" "-")
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If something needs the lion and it is nice then the lion needs the squirrel.
((("something" "needs" "lion" "+") ("something" "is" "nice" "+")) -> ("lion" "needs" "squirrel" "+"))
If something needs the lion then the lion chases the squirrel.
((("something" "needs" "lion" "+")) -> ("lion" "chases" "squirrel" "+"))
If something likes the lion then it does not need the lion.
((("something" "likes" "lion" "+")) -> ("something" "needs" "lion" "-"))
If something needs the squirrel then it needs the lion.
((("something" "needs" "squirrel" "+")) -> ("something" "needs" "lion" "+"))
If something needs the mouse then the mouse needs the squirrel.
((("something" "needs" "mouse" "+")) -> ("mouse" "needs" "squirrel" "+"))
If something chases the lion and it needs the squirrel then the squirrel likes the mouse.
((("something" "chases" "lion" "+") ("something" "needs" "squirrel" "+")) -> ("squirrel" "likes" "mouse" "+"))
If something chases the mouse and it is cold then it chases the lion.
((("something" "chases" "mouse" "+") ("something" "is" "cold" "+")) -> ("something" "chases" "lion" "+"))
If something likes the mouse then it is big.
((("something" "likes" "mouse" "+")) -> ("something" "is" "big" "+"))
The squirrel is young.
True
1
proof
[(triple8)]
("squirrel" "is" "young" "+")
triple8
The squirrel does not chase the mouse.
False
1
inv-proof
[(triple6)]
("squirrel" "chases" "mouse" "-")
triple6
The squirrel is big.
True
2
proof
[(((triple9) -> rule8))]
("squirrel" "is" "big" "+")
((triple9) -> (rule8 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is not big.
False
2
inv-proof
[(((triple9) -> rule8))]
("squirrel" "is" "big" "-")
((triple9) -> (rule8 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The mouse needs the lion.
True
3
proof
[(((((triple10) -> rule5)) -> rule4) OR ((((triple2) -> rule5)) -> rule4))]
("mouse" "needs" "lion" "+")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse does not need the lion.
False
3
inv-proof
[(((((triple10) -> rule5)) -> rule4) OR ((((triple2) -> rule5)) -> rule4))]
("mouse" "needs" "lion" "-")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The lion chases the squirrel.
True
4
proof
[(((((((triple10) -> rule5)) -> rule4)) -> rule2) OR ((((((triple2) -> rule5)) -> rule4)) -> rule2))]
("lion" "chases" "squirrel" "+")
((((((triple10) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The lion does not chase the squirrel.
False
4
inv-proof
[(((((((triple10) -> rule5)) -> rule4)) -> rule2) OR ((((((triple2) -> rule5)) -> rule4)) -> rule2))]
("lion" "chases" "squirrel" "-")
((((((triple10) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The mouse does not chase the lion.
Unknown
inv-rconc
[@1: The mouse chases the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "chases" "lion" "-")
The lion chases the lion.
Unknown
rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "chases" "lion" "+")
The squirrel does not need the lion.
Unknown
inv-rconc
[@1: The squirrel needs the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "lion" "-")
The lion needs the lion.
Unknown
rconc
[@2: The lion needs the lion.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("lion" "needs" "lion" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The lion is young.[(triple1)] The lion needs the mouse.[(triple2)] The mouse does not like the lion.[(triple4)] The mouse is not nice.[(triple3)] The mouse likes the squirrel.[(triple5)] The squirrel chases the mouse.[(triple6)] The squirrel is nice.[(triple7)] The squirrel is young.[(triple8)] The squirrel likes the mouse.[(triple9)] The squirrel needs the mouse.[(triple10)] @1: The mouse needs the squirrel.[(((triple10) -> rule5) OR ((triple2) -> rule5))] The squirrel is big.[(((triple9) -> rule8))] @2: The mouse needs the lion.[(((((triple10) -> rule5)) -> rule4) OR ((((triple2) -> rule5)) -> rule4))] @3: The lion chases the squirrel.[(((((((triple10) -> rule5)) -> rule4)) -> rule2) OR ((((((triple2) -> rule5)) -> rule4)) -> rule2))]
The lion is young.
("lion" "is" "young" "+")
triple1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple2
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
triple4
The mouse is not nice.
("mouse" "is" "nice" "-")
triple3
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple5
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple6
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple7
The squirrel is young.
("squirrel" "is" "young" "+")
triple8
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple9
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple10
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
((triple10) -> (rule5 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
((triple2) -> (rule5 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((triple9) -> (rule8 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
((((((triple10) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3