The lion eats the mouse. The lion is cold. The lion is green. The lion is rough. The lion likes the mouse. The lion sees the mouse. The mouse eats the lion. The mouse is big. The mouse is cold. The mouse is rough. The mouse likes the lion. The mouse sees the lion. If something is rough and it likes the lion then the lion eats the mouse. If something likes the lion and the lion sees the mouse then the lion is red. If something eats the mouse and it eats the lion then the lion sees the mouse.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If something is rough and it likes the lion then the lion eats the mouse.
((("something" "is" "rough" "+") ("something" "likes" "lion" "+")) -> ("lion" "eats" "mouse" "+"))
If something likes the lion and the lion sees the mouse then the lion is red.
((("something" "likes" "lion" "+") ("lion" "sees" "mouse" "+")) -> ("lion" "is" "red" "+"))
If something eats the mouse and it eats the lion then the lion sees the mouse.
((("something" "eats" "mouse" "+") ("something" "eats" "lion" "+")) -> ("lion" "sees" "mouse" "+"))
The mouse eats the lion.
True
1
proof
[(triple7)]
("mouse" "eats" "lion" "+")
triple7
The mouse does not like the lion.
False
1
inv-proof
[(triple11)]
("mouse" "likes" "lion" "-")
triple11
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The lion eats the mouse.[(triple1 OR ((triple10 triple11) -> rule1))] The lion is cold.[(triple2)] The lion is green.[(triple3)] The lion is rough.[(triple4)] The lion likes the mouse.[(triple5)] The lion sees the mouse.[(triple6)] The mouse eats the lion.[(triple7)] The mouse is big.[(triple8)] The mouse is cold.[(triple9)] The mouse is rough.[(triple10)] The mouse likes the lion.[(triple11)] The mouse sees the lion.[(triple12)] @1: The lion is red.[(((triple11 triple6) -> rule2))]
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
((triple10 triple11) -> (rule1 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple5
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple6
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple7
The mouse is big.
("mouse" "is" "big" "+")
triple8
The mouse is cold.
("mouse" "is" "cold" "+")
triple9
The mouse is rough.
("mouse" "is" "rough" "+")
triple10
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple11
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple12
The lion is red.
("lion" "is" "red" "+")
((triple11 triple6) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1