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