% EXPECT: sat
% Preamble  --------------
DATATYPE UNIT = Unit END;
DATATYPE BOOL = Truth | Falsity END;

% Decls     --------------
node$type: TYPE;
value$type: TYPE;
Nodes$elem$type: TYPE = node$type;
Nodes$t$type: TYPE;
node_pair_set$type: TYPE = ARRAY node$type OF ARRAY node$type OF BOOL;
failure_pattern$type: TYPE = node_pair_set$type;
is_faulty:(node$type, failure_pattern$type) -> BOOL = (LAMBDA (p: node$type, 
                                                               deliver: failure_pattern$type): 
                                                      (IF (EXISTS (q: node$type): 
                                                          (NOT ((((deliver)[
                                                                 (p)])[
                                                                (q)]) = 
                                                               (Truth)))) THEN 
                                                      (Truth) ELSE (Falsity) ENDIF));

CHECKSAT;