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