The bear is rough. The bear is young. The bear needs the mouse. The bear sees the lion. The cat visits the bear. The cat visits the mouse. The lion needs the cat. The lion needs the mouse. The lion sees the cat. The lion sees the mouse. The mouse needs the lion. The mouse visits the cat. If the lion sees the cat and the lion needs the mouse then the lion is young.
The bear is rough.
("bear" "is" "rough" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If the lion sees the cat and the lion needs the mouse then the lion is young.
((("lion" "sees" "cat" "+") ("lion" "needs" "mouse" "+")) -> ("lion" "is" "young" "+"))
The lion needs the cat.
True
1
proof
[(triple7)]
("lion" "needs" "cat" "+")
triple7
The lion does not need the cat.
False
1
inv-proof
[(triple7)]
("lion" "needs" "cat" "-")
triple7
The lion is young.
True
3
proof
[(((triple9 triple8) -> rule1))]
("lion" "is" "young" "+")
((triple9 triple8) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is not young.
False
3
inv-proof
[(((triple9 triple8) -> rule1))]
("lion" "is" "young" "-")
((triple9 triple8) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The bear is rough.[(triple1)] The bear is young.[(triple2)] The bear needs the mouse.[(triple3)] The bear sees the lion.[(triple4)] The cat visits the bear.[(triple5)] The cat visits the mouse.[(triple6)] The lion needs the cat.[(triple7)] The lion needs the mouse.[(triple8)] The lion sees the cat.[(triple9)] The lion sees the mouse.[(triple10)] The mouse needs the lion.[(triple11)] The mouse visits the cat.[(triple12)] @1: The lion is young.[(((triple9 triple8) -> rule1))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple3
The bear sees the lion.
("bear" "sees" "lion" "+")
triple4
The cat visits the bear.
("cat" "visits" "bear" "+")
triple5
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple6
The lion needs the cat.
("lion" "needs" "cat" "+")
triple7
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple8
The lion sees the cat.
("lion" "sees" "cat" "+")
triple9
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple10
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple11
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple12
The lion is young.
("lion" "is" "young" "+")
((triple9 triple8) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1