The lion chases the mouse. The lion eats the mouse. The lion is big. The lion is blue. The lion is rough. The lion is young. The lion sees the mouse. The mouse chases the lion. The mouse eats the lion. The mouse is big. The mouse is blue. The mouse is green. The mouse is rough. The mouse is young. The mouse sees the lion. If someone is big and they eat the mouse then the mouse is blue. If someone sees the lion then they eat the mouse. If someone chases the mouse then the mouse is young.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If someone is big and they eat the mouse then the mouse is blue.
((("someone" "is" "big" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
If someone sees the lion then they eat the mouse.
((("someone" "sees" "lion" "+")) -> ("someone" "eats" "mouse" "+"))
If someone chases the mouse then the mouse is young.
((("someone" "chases" "mouse" "+")) -> ("mouse" "is" "young" "+"))
The mouse chases the lion.
True
1
proof
[(triple8)]
("mouse" "chases" "lion" "+")
triple8
The mouse does not chase the lion.
False
1
inv-proof
[(triple8)]
("mouse" "chases" "lion" "-")
triple8
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 is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
@0: The lion chases the mouse.[(triple1)] The lion eats the mouse.[(triple2)] The lion is big.[(triple3)] The lion is blue.[(triple4)] The lion is rough.[(triple5)] The lion is young.[(triple6)] The lion sees the mouse.[(triple7)] The mouse chases the lion.[(triple8)] The mouse eats the lion.[(triple9)] The mouse is big.[(triple10)] The mouse is blue.[(triple11 OR ((triple3 triple2) -> rule1) OR ((triple10 ((triple15) -> rule2)) -> rule1))] The mouse is green.[(triple12)] The mouse is rough.[(triple13)] The mouse is young.[(triple14 OR ((triple1) -> rule3))] The mouse sees the lion.[(triple15)] @1: The mouse eats the mouse.[(((triple15) -> rule2))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple2
The lion is big.
("lion" "is" "big" "+")
triple3
The lion is blue.
("lion" "is" "blue" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple7
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple8
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple9
The mouse is big.
("mouse" "is" "big" "+")
triple10
The mouse is blue.
("mouse" "is" "blue" "+")
triple11
((triple3 triple2) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple10 ((triple15) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
triple12
The mouse is rough.
("mouse" "is" "rough" "+")
triple13
The mouse is young.
("mouse" "is" "young" "+")
triple14
((triple1) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple15
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple15) -> (rule2 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1