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