The bear sees the squirrel. The mouse chases the squirrel. The squirrel sees the bear. If someone chases the squirrel then the squirrel chases the mouse. If someone chases the squirrel and they chase the mouse then the mouse eats the squirrel. If the bear chases the squirrel and the bear is green then the squirrel eats the mouse. If someone is round then they eat the mouse. If someone eats the mouse and they see the squirrel then the mouse eats the bear. If someone chases the mouse then the mouse sees the bear.
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If someone chases the squirrel then the squirrel chases the mouse.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "chases" "mouse" "+"))
If someone chases the squirrel and they chase the mouse then the mouse eats the squirrel.
((("someone" "chases" "squirrel" "+") ("someone" "chases" "mouse" "+")) -> ("mouse" "eats" "squirrel" "+"))
If the bear chases the squirrel and the bear is green then the squirrel eats the mouse.
((("bear" "chases" "squirrel" "+") ("bear" "is" "green" "+")) -> ("squirrel" "eats" "mouse" "+"))
If someone is round then they eat the mouse.
((("someone" "is" "round" "+")) -> ("someone" "eats" "mouse" "+"))
If someone eats the mouse and they see the squirrel then the mouse eats the bear.
((("someone" "eats" "mouse" "+") ("someone" "sees" "squirrel" "+")) -> ("mouse" "eats" "bear" "+"))
If someone chases the mouse then the mouse sees the bear.
((("someone" "chases" "mouse" "+")) -> ("mouse" "sees" "bear" "+"))
The squirrel sees the bear.
True
1
proof
[(triple3)]
("squirrel" "sees" "bear" "+")
triple3
The bear does not see the squirrel.
False
1
inv-proof
[(triple1)]
("bear" "sees" "squirrel" "-")
triple1
The squirrel chases the mouse.
True
2
proof
[(((triple2) -> rule1))]
("squirrel" "chases" "mouse" "+")
((triple2) -> (rule1 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel does not chase the mouse.
False
2
inv-proof
[(((triple2) -> rule1))]
("squirrel" "chases" "mouse" "-")
((triple2) -> (rule1 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The mouse sees the bear.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("mouse" "sees" "bear" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The mouse does not see the bear.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("mouse" "sees" "bear" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The bear does not eat the mouse.
Unknown
inv-rconc
[@1: The bear eats the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "eats" "mouse" "-")
The mouse eats the squirrel.
Unknown
rconc
[@1: The mouse eats the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "eats" "squirrel" "+")
The mouse does not eat the bear.
Unknown
inv-rconc
[@2: The mouse eats the bear.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("mouse" "eats" "bear" "-")
The bear sees the mouse.
Unknown
random
[@0: The bear sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "mouse" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
@0: The bear sees the squirrel.[(triple1)] The mouse chases the squirrel.[(triple2)] The squirrel sees the bear.[(triple3)] @1: The squirrel chases the mouse.[(((triple2) -> rule1))] @2: The mouse sees the bear.[(((((triple2) -> rule1)) -> rule6))]
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple1
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple2
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple3
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
((triple2) -> (rule1 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2