The mouse does not see the tiger. The rabbit eats the mouse. The squirrel sees the rabbit. The tiger is young. If someone likes the rabbit then the rabbit eats the mouse. If someone is nice then they do not like the tiger. If someone eats the mouse then they are young. If someone eats the mouse and they are young then the mouse sees the squirrel. If the squirrel eats the tiger and the squirrel likes the mouse then the squirrel likes the rabbit. If someone sees the squirrel then the squirrel likes the mouse. If someone is young then they do not see the squirrel. If someone is blue and they do not like the mouse then the mouse eats the squirrel.
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The tiger is young.
("tiger" "is" "young" "+")
If someone likes the rabbit then the rabbit eats the mouse.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "eats" "mouse" "+"))
If someone is nice then they do not like the tiger.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "tiger" "-"))
If someone eats the mouse then they are young.
((("someone" "eats" "mouse" "+")) -> ("someone" "is" "young" "+"))
If someone eats the mouse and they are young then the mouse sees the squirrel.
((("someone" "eats" "mouse" "+") ("someone" "is" "young" "+")) -> ("mouse" "sees" "squirrel" "+"))
If the squirrel eats the tiger and the squirrel likes the mouse then the squirrel likes the rabbit.
((("squirrel" "eats" "tiger" "+") ("squirrel" "likes" "mouse" "+")) -> ("squirrel" "likes" "rabbit" "+"))
If someone sees the squirrel then the squirrel likes the mouse.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "likes" "mouse" "+"))
If someone is young then they do not see the squirrel.
((("someone" "is" "young" "+")) -> ("someone" "sees" "squirrel" "-"))
If someone is blue and they do not like the mouse then the mouse eats the squirrel.
((("someone" "is" "blue" "+") ("someone" "likes" "mouse" "~")) -> ("mouse" "eats" "squirrel" "+"))
The squirrel sees the rabbit.
True
1
proof
[(triple3)]
("squirrel" "sees" "rabbit" "+")
triple3
The rabbit does not eat the mouse.
False
1
inv-proof
[(triple2)]
("rabbit" "eats" "mouse" "-")
triple2
The tiger does not see the squirrel.
True
2
proof
[(((triple4) -> rule7))]
("tiger" "sees" "squirrel" "-")
((triple4) -> (rule7 % int1))
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int1
The tiger sees the squirrel.
False
2
inv-proof
[(((triple4) -> rule7))]
("tiger" "sees" "squirrel" "+")
((triple4) -> (rule7 % int1))
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int1
The rabbit does not see the squirrel.
True
3
proof
[(((((triple2) -> rule3)) -> rule7))]
("rabbit" "sees" "squirrel" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit does not see the squirrel.
("rabbit" "sees" "squirrel" "-")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The mouse does not see the squirrel.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule4))]
("mouse" "sees" "squirrel" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The squirrel likes the mouse.
True
5
proof
[(((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule6))]
("squirrel" "likes" "mouse" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The squirrel does not like the mouse.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule6))]
("squirrel" "likes" "mouse" "-")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The mouse does not eat the squirrel.
Unknown
inv-rconc
[@1: The mouse eats the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "eats" "squirrel" "-")
The squirrel is young.
Unknown
rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "young" "+")
The squirrel does not like the rabbit.
Unknown
inv-rconc
[@1: The squirrel likes the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "likes" "rabbit" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "young" "+")
The squirrel does not see the mouse.
Unknown
inv-random
[@0: The squirrel sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "mouse" "-")
The tiger eats the mouse.
Unknown
random
[@0: The tiger eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "mouse" "+")
The rabbit does not see the mouse.
Unknown
inv-random
[@0: The rabbit sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "mouse" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The mouse does not see the tiger.[(triple1)] The rabbit eats the mouse.[(triple2)] The squirrel sees the rabbit.[(triple3)] The tiger is young.[(triple4)] @1: The rabbit is young.[(((triple2) -> rule3))] The tiger does not see the squirrel.[(((triple4) -> rule7))] @2: The mouse sees the squirrel.[(((triple2 ((triple2) -> rule3)) -> rule4))] The rabbit does not see the squirrel.[(((((triple2) -> rule3)) -> rule7))] @3: The squirrel likes the mouse.[(((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule6))]
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
triple1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple3
The tiger is young.
("tiger" "is" "young" "+")
triple4
The rabbit is young.
("rabbit" "is" "young" "+")
((triple2) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
((triple4) -> (rule7 % int1))
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit does not see the squirrel.
("rabbit" "sees" "squirrel" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit does not see the squirrel.
("rabbit" "sees" "squirrel" "-")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3