The lion is big. The lion is kind. The lion likes the mouse. The lion likes the squirrel. The mouse chases the squirrel. The mouse is not big. The mouse is blue. The mouse is nice. The mouse does not see the lion. The squirrel chases the lion. The squirrel chases the mouse. The squirrel is kind. The squirrel is nice. The squirrel is rough. The squirrel likes the lion. The squirrel likes the mouse. If someone chases the squirrel and the squirrel sees the mouse then the squirrel sees the lion. If the lion sees the squirrel and the lion chases the mouse then the lion does not chase the squirrel. If the mouse does not like the squirrel then the squirrel is not rough. If the squirrel chases the lion then the squirrel is rough. If someone sees the mouse then they are big. If someone chases the mouse and they are not blue then they see the lion. If someone is blue and they chase the lion then the lion does not chase the mouse. If the squirrel does not like the lion then the squirrel chases the lion.
The lion is big.
("lion" "is" "big" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is not big.
("mouse" "is" "big" "-")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
If someone chases the squirrel and the squirrel sees the mouse then the squirrel sees the lion.
((("someone" "chases" "squirrel" "+") ("squirrel" "sees" "mouse" "+")) -> ("squirrel" "sees" "lion" "+"))
If the lion sees the squirrel and the lion chases the mouse then the lion does not chase the squirrel.
((("lion" "sees" "squirrel" "+") ("lion" "chases" "mouse" "+")) -> ("lion" "chases" "squirrel" "-"))
If the mouse does not like the squirrel then the squirrel is not rough.
((("mouse" "likes" "squirrel" "~")) -> ("squirrel" "is" "rough" "-"))
If the squirrel chases the lion then the squirrel is rough.
((("squirrel" "chases" "lion" "+")) -> ("squirrel" "is" "rough" "+"))
If someone sees the mouse then they are big.
((("someone" "sees" "mouse" "+")) -> ("someone" "is" "big" "+"))
If someone chases the mouse and they are not blue then they see the lion.
((("someone" "chases" "mouse" "+") ("someone" "is" "blue" "~")) -> ("someone" "sees" "lion" "+"))
If someone is blue and they chase the lion then the lion does not chase the mouse.
((("someone" "is" "blue" "+") ("someone" "chases" "lion" "+")) -> ("lion" "chases" "mouse" "-"))
If the squirrel does not like the lion then the squirrel chases the lion.
((("squirrel" "likes" "lion" "~")) -> ("squirrel" "chases" "lion" "+"))
The lion is kind.
True
1
proof
[(triple2)]
("lion" "is" "kind" "+")
triple2
The squirrel does not like the lion.
False
1
inv-proof
[(triple15)]
("squirrel" "likes" "lion" "-")
triple15
The squirrel does not see the lion.
Unknown
inv-rconc
[@1: The squirrel sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "lion" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The lion is big.[(triple1)] The lion is kind.[(triple2)] The lion likes the mouse.[(triple3)] The lion likes the squirrel.[(triple4)] The mouse chases the squirrel.[(triple5)] The mouse does not see the lion.[(triple9)] The mouse is blue.[(triple7)] The mouse is nice.[(triple8)] The mouse is not big.[(triple6)] The squirrel chases the lion.[(triple10)] The squirrel chases the mouse.[(triple11)] The squirrel is kind.[(triple12)] The squirrel is nice.[(triple13)] The squirrel is rough.[(triple14 OR ((triple10) -> rule4))] The squirrel likes the lion.[(triple15)] The squirrel likes the mouse.[(triple16)]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple3
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple4
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple5
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
triple9
The mouse is blue.
("mouse" "is" "blue" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse is not big.
("mouse" "is" "big" "-")
triple6
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple10
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple11
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple12
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple13
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple14
((triple10) -> (rule4 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple15
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple16