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