The bear chases the squirrel. The mouse is rough. The rabbit sees the squirrel. The squirrel chases the bear. If someone sees the squirrel then the squirrel chases the rabbit. If someone visits the mouse then the mouse sees the squirrel.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
If someone sees the squirrel then the squirrel chases the rabbit.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "chases" "rabbit" "+"))
If someone visits the mouse then the mouse sees the squirrel.
((("someone" "visits" "mouse" "+")) -> ("mouse" "sees" "squirrel" "+"))
The mouse is rough.
True
1
proof
[(triple2)]
("mouse" "is" "rough" "+")
triple2
The rabbit does not see the squirrel.
False
1
inv-proof
[(triple3)]
("rabbit" "sees" "squirrel" "-")
triple3
The squirrel chases the rabbit.
True
2
proof
[(((triple3) -> rule1))]
("squirrel" "chases" "rabbit" "+")
((triple3) -> (rule1 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The squirrel does not chase the rabbit.
False
2
inv-proof
[(((triple3) -> rule1))]
("squirrel" "chases" "rabbit" "-")
((triple3) -> (rule1 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The mouse does not see the squirrel.
Unknown
inv-rconc
[@1: The mouse sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "squirrel" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The bear chases the squirrel.[(triple1)] The mouse is rough.[(triple2)] The rabbit sees the squirrel.[(triple3)] The squirrel chases the bear.[(triple4)] @1: The squirrel chases the rabbit.[(((triple3) -> rule1))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The mouse is rough.
("mouse" "is" "rough" "+")
triple2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple3
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple4
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
((triple3) -> (rule1 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1