The lion is big. The lion is green. The lion is kind. The lion is nice. The lion is rough. The lion likes the mouse. The lion needs the mouse. The lion sees the mouse. The mouse is big. The mouse is green. The mouse is kind. The mouse is rough. The mouse likes the lion. The mouse needs the lion. The mouse sees the lion. If something likes the mouse then it sees the lion.
The lion is big.
("lion" "is" "big" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If something likes the mouse then it sees the lion.
((("something" "likes" "mouse" "+")) -> ("something" "sees" "lion" "+"))
The lion sees the mouse.
True
1
proof
[(triple8)]
("lion" "sees" "mouse" "+")
triple8
The mouse does not like the lion.
False
1
inv-proof
[(triple13)]
("mouse" "likes" "lion" "-")
triple13
The lion sees the lion.
True
2
proof
[(((triple6) -> rule1))]
("lion" "sees" "lion" "+")
((triple6) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not see the lion.
False
2
inv-proof
[(((triple6) -> rule1))]
("lion" "sees" "lion" "-")
((triple6) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The lion is big.[(triple1)] The lion is green.[(triple2)] The lion is kind.[(triple3)] The lion is nice.[(triple4)] The lion is rough.[(triple5)] The lion likes the mouse.[(triple6)] The lion needs the mouse.[(triple7)] The lion sees the mouse.[(triple8)] The mouse is big.[(triple9)] The mouse is green.[(triple10)] The mouse is kind.[(triple11)] The mouse is rough.[(triple12)] The mouse likes the lion.[(triple13)] The mouse needs the lion.[(triple14)] The mouse sees the lion.[(triple15)] @1: The lion sees the lion.[(((triple6) -> rule1))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple6
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple7
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple8
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse is green.
("mouse" "is" "green" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
triple11
The mouse is rough.
("mouse" "is" "rough" "+")
triple12
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple13
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple14
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple15
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple6) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1