The cat likes the mouse. The lion chases the mouse. The mouse likes the cat. The squirrel likes the cat. If someone likes the mouse then the mouse chases the squirrel.
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
If someone likes the mouse then the mouse chases the squirrel.
((("someone" "likes" "mouse" "+")) -> ("mouse" "chases" "squirrel" "+"))
The mouse likes the cat.
True
1
proof
[(triple3)]
("mouse" "likes" "cat" "+")
triple3
The cat does not like the mouse.
False
1
inv-proof
[(triple1)]
("cat" "likes" "mouse" "-")
triple1
The mouse chases the squirrel.
True
2
proof
[(((triple1) -> rule1))]
("mouse" "chases" "squirrel" "+")
((triple1) -> (rule1 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The mouse does not chase the squirrel.
False
2
inv-proof
[(((triple1) -> rule1))]
("mouse" "chases" "squirrel" "-")
((triple1) -> (rule1 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The squirrel does not chase the mouse.
Unknown
inv-random
[@0: The squirrel chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "mouse" "-")
The cat needs the mouse.
Unknown
random
[@0: The cat needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "mouse" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The mouse chases the cat.
Unknown
random
[@0: The mouse chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cat" "+")
@0: The cat likes the mouse.[(triple1)] The lion chases the mouse.[(triple2)] The mouse likes the cat.[(triple3)] The squirrel likes the cat.[(triple4)] @1: The mouse chases the squirrel.[(((triple1) -> rule1))]
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple3
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple4
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
((triple1) -> (rule1 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1