The lion chases the mouse. The lion is not big. The lion is blue. The lion is nice. The lion is rough. The lion is round. The lion likes the mouse. The lion sees the mouse. The mouse chases the lion. The mouse is big. The mouse is blue. The mouse is nice. The mouse is rough. The mouse is round. The mouse likes the lion. The mouse sees the lion. If something chases the mouse then it is rough.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is not big.
("lion" "is" "big" "-")
The lion is blue.
("lion" "is" "blue" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "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 nice.
("mouse" "is" "nice" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If something chases the mouse then it is rough.
((("something" "chases" "mouse" "+")) -> ("something" "is" "rough" "+"))
The lion sees the mouse.
True
1
proof
[(triple8)]
("lion" "sees" "mouse" "+")
triple8
The lion is not blue.
False
1
inv-proof
[(triple3)]
("lion" "is" "blue" "-")
triple3
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
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 is blue.[(triple3)] The lion is nice.[(triple4)] The lion is not big.[(triple2)] The lion is rough.[(triple5 OR ((triple1) -> rule1))] The lion is round.[(triple6)] The lion likes the mouse.[(triple7)] The lion sees the mouse.[(triple8)] The mouse chases the lion.[(triple9)] The mouse is big.[(triple10)] The mouse is blue.[(triple11)] The mouse is nice.[(triple12)] The mouse is rough.[(triple13)] The mouse is round.[(triple14)] The mouse likes the lion.[(triple15)] The mouse sees the lion.[(triple16)]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is not big.
("lion" "is" "big" "-")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple5
((triple1) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is round.
("lion" "is" "round" "+")
triple6
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple7
The lion sees the mouse.
("lion" "sees" "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 nice.
("mouse" "is" "nice" "+")
triple12
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 sees the lion.
("mouse" "sees" "lion" "+")
triple16