type
  Dir {forward, backward, off};
  State {sink, cp_off, source};
  Load_13 [0..13];
  Flow_15 [0..15];

variable
// All Powers and Sinks are boolean varables
  bool P1_powered, S16_powered, S22_powered, S2_powered, S11_powered, S17_powered, S5_powered, S8_powered, S20_powered, S4_powered, S12_powered, S3_powered, S19_powered, S21_powered, S10_powered, S13_powered, S14_powered, S7_powered, S15_powered, S6_powered, S1_powered, S18_powered, S9_powered;

// Connection points
  State C1_state;
  Flow_15 C1_flow;

// Lines
  Dir L12_dir, L13_dir, L3_dir, L24_dir, L6_dir, L17_dir, L10_dir, L9_dir, L21_dir, L22_dir, L15_dir, L16_dir, L1_dir, L19_dir, L8_dir, L18_dir, L2_dir, L23_dir, L7_dir, L20_dir, L4_dir, L14_dir, L25_dir, L5_dir, L11_dir, L26_dir;
  Load_13 L1_load, L2_load, L3_load, L4_load, L5_load, L6_load, L7_load, L8_load, L9_load, L10_load, L11_load, L12_load, L13_load, L14_load, L15_load, L16_load, L17_load, L18_load, L19_load, L20_load, L21_load, L22_load, L23_load, L24_load, L25_load, L26_load;

rule
//Line L12
  (L12_dir != off && (L13_dir == backward || L16_dir == backward) >> L12_dir == backward) &&
  (L12_dir == backward >> L12_dir != off && (L13_dir == backward || L16_dir == backward));
  (L12_dir != off && (L11_dir == forward) >> L12_dir == forward) &&
  (L12_dir == forward >> L12_dir != off && (L11_dir == forward));
  L12_dir == forward >> L12_load == L13_load + L16_load + ((S11_powered >> 1) && (!S11_powered >> 0));
  L12_dir == backward >> L12_load == L11_load + ((S10_powered >> 1) && (!S10_powered >> 0));
  L12_dir == off >> L12_load == 0;

//Line L13
  (L13_dir != off && (L14_dir == backward) >> L13_dir == backward) &&
  (L13_dir == backward >> L13_dir != off && (L14_dir == backward));
  (L13_dir != off && (L12_dir == forward || L16_dir == backward) >> L13_dir == forward) &&
  (L13_dir == forward >> L13_dir != off && (L12_dir == forward || L16_dir == backward));
  L13_dir == forward >> L13_load == L14_load + ((S12_powered >> 1) && (!S12_powered >> 0));
  L13_dir == backward >> L13_load == L12_load + L16_load + ((S11_powered >> 1) && (!S11_powered >> 0));
  L13_dir == off >> L13_load == 0;

//Line L3
  (L3_dir != off && (L4_dir == backward) >> L3_dir == backward) &&
  (L3_dir == backward >> L3_dir != off && (L4_dir == backward));
  (L3_dir != off && (L2_dir == forward) >> L3_dir == forward) &&
  (L3_dir == forward >> L3_dir != off && (L2_dir == forward));
  L3_dir == forward >> L3_load == L4_load + ((S3_powered >> 1) && (!S3_powered >> 0));
  L3_dir == backward >> L3_load == L2_load + ((S2_powered >> 1) && (!S2_powered >> 0));
  L3_dir == off >> L3_load == 0;

//Line L24
  P1_powered >> ( (L24_dir != backward) );
  !P1_powered >> (
  ((L24_dir != off && (L23_dir == forward) >> L24_dir == backward) &&
  (L24_dir == backward >> L24_dir != off && (L23_dir == forward))) &&
  ((L24_dir != off && (L1_dir == backward || L7_dir == backward || L15_dir == backward || L25_dir == backward) >> L24_dir == forward) &&
  (L24_dir == forward >> L24_dir != off && (L1_dir == backward || L7_dir == backward || L15_dir == backward || L25_dir == backward)))
  );
  L24_dir == forward >> L24_load == L23_load + ((S21_powered >> 1) && (!S21_powered >> 0));
  L24_dir == backward >> L24_load == L1_load + L7_load + L15_load + L25_load;
  L24_dir == off >> L24_load == 0;

//Line L6
  (L6_dir != off && (L7_dir == forward || L8_dir == backward) >> L6_dir == backward) &&
  (L6_dir == backward >> L6_dir != off && (L7_dir == forward || L8_dir == backward));
  (L6_dir != off && (L5_dir == forward) >> L6_dir == forward) &&
  (L6_dir == forward >> L6_dir != off && (L5_dir == forward));
  L6_dir == forward >> L6_load == L7_load + L8_load + ((S6_powered >> 1) && (!S6_powered >> 0));
  L6_dir == backward >> L6_load == L5_load + ((S5_powered >> 1) && (!S5_powered >> 0));
  L6_dir == off >> L6_load == 0;

//Line L17
  (L17_dir != off && (L18_dir == backward) >> L17_dir == backward) &&
  (L17_dir == backward >> L17_dir != off && (L18_dir == backward));
  (L17_dir != off && (L16_dir == forward) >> L17_dir == forward) &&
  (L17_dir == forward >> L17_dir != off && (L16_dir == forward));
  L17_dir == forward >> L17_load == L18_load + ((S15_powered >> 1) && (!S15_powered >> 0));
  L17_dir == backward >> L17_load == L16_load + ((S14_powered >> 1) && (!S14_powered >> 0));
  L17_dir == off >> L17_load == 0;

//Line L10
  (L10_dir != off && (L11_dir == backward) >> L10_dir == backward) &&
  (L10_dir == backward >> L10_dir != off && (L11_dir == backward));
  (L10_dir != off && (L9_dir == forward) >> L10_dir == forward) &&
  (L10_dir == forward >> L10_dir != off && (L9_dir == forward));
  L10_dir == forward >> L10_load == L11_load + ((S9_powered >> 1) && (!S9_powered >> 0));
  L10_dir == backward >> L10_load == L9_load + ((S8_powered >> 1) && (!S8_powered >> 0));
  L10_dir == off >> L10_load == 0;

//Line L9
  (L9_dir != off && (L10_dir == backward) >> L9_dir == backward) &&
  (L9_dir == backward >> L9_dir != off && (L10_dir == backward));
  (L9_dir != off && (L8_dir == forward) >> L9_dir == forward) &&
  (L9_dir == forward >> L9_dir != off && (L8_dir == forward));
  L9_dir == forward >> L9_load == L10_load + ((S8_powered >> 1) && (!S8_powered >> 0));
  L9_dir == backward >> L9_load == L8_load + ((S7_powered >> 1) && (!S7_powered >> 0));
  L9_dir == off >> L9_load == 0;

//Line L21
  (L21_dir != off && (L22_dir == backward) >> L21_dir == backward) &&
  (L21_dir == backward >> L21_dir != off && (L22_dir == backward));
  (L21_dir != off && (L20_dir == forward) >> L21_dir == forward) &&
  (L21_dir == forward >> L21_dir != off && (L20_dir == forward));
  L21_dir == forward >> L21_load == L22_load + ((S19_powered >> 1) && (!S19_powered >> 0));
  L21_dir == backward >> L21_load == L20_load + ((S18_powered >> 1) && (!S18_powered >> 0));
  L21_dir == off >> L21_load == 0;

//Line L22
  (L22_dir != off && (L23_dir == backward) >> L22_dir == backward) &&
  (L22_dir == backward >> L22_dir != off && (L23_dir == backward));
  (L22_dir != off && (L21_dir == forward) >> L22_dir == forward) &&
  (L22_dir == forward >> L22_dir != off && (L21_dir == forward));
  L22_dir == forward >> L22_load == L23_load + ((S20_powered >> 1) && (!S20_powered >> 0));
  L22_dir == backward >> L22_load == L21_load + ((S19_powered >> 1) && (!S19_powered >> 0));
  L22_dir == off >> L22_load == 0;

//Line L15
  P1_powered >> ( (L15_dir != backward) );
  !P1_powered >> (
  ((L15_dir != off && (L14_dir == forward) >> L15_dir == backward) &&
  (L15_dir == backward >> L15_dir != off && (L14_dir == forward))) &&
  ((L15_dir != off && (L1_dir == backward || L7_dir == backward || L24_dir == backward || L25_dir == backward) >> L15_dir == forward) &&
  (L15_dir == forward >> L15_dir != off && (L1_dir == backward || L7_dir == backward || L24_dir == backward || L25_dir == backward)))
  );
  L15_dir == forward >> L15_load == L14_load + ((S13_powered >> 1) && (!S13_powered >> 0));
  L15_dir == backward >> L15_load == L1_load + L7_load + L24_load + L25_load;
  L15_dir == off >> L15_load == 0;

//Line L16
  (L16_dir != off && (L17_dir == backward) >> L16_dir == backward) &&
  (L16_dir == backward >> L16_dir != off && (L17_dir == backward));
  (L16_dir != off && (L12_dir == forward || L13_dir == backward) >> L16_dir == forward) &&
  (L16_dir == forward >> L16_dir != off && (L12_dir == forward || L13_dir == backward));
  L16_dir == forward >> L16_load == L17_load + ((S14_powered >> 1) && (!S14_powered >> 0));
  L16_dir == backward >> L16_load == L12_load + L13_load + ((S11_powered >> 1) && (!S11_powered >> 0));
  L16_dir == off >> L16_load == 0;

//Line L1
  P1_powered >> ( (L1_dir != backward) );
  !P1_powered >> (
  ((L1_dir != off && (L2_dir == backward) >> L1_dir == backward) &&
  (L1_dir == backward >> L1_dir != off && (L2_dir == backward))) &&
  ((L1_dir != off && (L7_dir == backward || L15_dir == backward || L24_dir == backward || L25_dir == backward) >> L1_dir == forward) &&
  (L1_dir == forward >> L1_dir != off && (L7_dir == backward || L15_dir == backward || L24_dir == backward || L25_dir == backward)))
  );
  L1_dir == forward >> L1_load == L2_load + ((S1_powered >> 1) && (!S1_powered >> 0));
  L1_dir == backward >> L1_load == L7_load + L15_load + L24_load + L25_load;
  L1_dir == off >> L1_load == 0;

//Line L19
  (L19_dir != off && (L20_dir == backward) >> L19_dir == backward) &&
  (L19_dir == backward >> L19_dir != off && (L20_dir == backward));
  (L19_dir != off && (L18_dir == forward) >> L19_dir == forward) &&
  (L19_dir == forward >> L19_dir != off && (L18_dir == forward));
  L19_dir == forward >> L19_load == L20_load + ((S17_powered >> 1) && (!S17_powered >> 0));
  L19_dir == backward >> L19_load == L18_load + ((S16_powered >> 1) && (!S16_powered >> 0));
  L19_dir == off >> L19_load == 0;

//Line L8
  (L8_dir != off && (L9_dir == backward) >> L8_dir == backward) &&
  (L8_dir == backward >> L8_dir != off && (L9_dir == backward));
  (L8_dir != off && (L6_dir == forward || L7_dir == forward) >> L8_dir == forward) &&
  (L8_dir == forward >> L8_dir != off && (L6_dir == forward || L7_dir == forward));
  L8_dir == forward >> L8_load == L9_load + ((S7_powered >> 1) && (!S7_powered >> 0));
  L8_dir == backward >> L8_load == L6_load + L7_load + ((S6_powered >> 1) && (!S6_powered >> 0));
  L8_dir == off >> L8_load == 0;

//Line L18
  (L18_dir != off && (L19_dir == backward) >> L18_dir == backward) &&
  (L18_dir == backward >> L18_dir != off && (L19_dir == backward));
  (L18_dir != off && (L17_dir == forward) >> L18_dir == forward) &&
  (L18_dir == forward >> L18_dir != off && (L17_dir == forward));
  L18_dir == forward >> L18_load == L19_load + ((S16_powered >> 1) && (!S16_powered >> 0));
  L18_dir == backward >> L18_load == L17_load + ((S15_powered >> 1) && (!S15_powered >> 0));
  L18_dir == off >> L18_load == 0;

//Line L2
  (L2_dir != off && (L3_dir == backward) >> L2_dir == backward) &&
  (L2_dir == backward >> L2_dir != off && (L3_dir == backward));
  (L2_dir != off && (L1_dir == forward) >> L2_dir == forward) &&
  (L2_dir == forward >> L2_dir != off && (L1_dir == forward));
  L2_dir == forward >> L2_load == L3_load + ((S2_powered >> 1) && (!S2_powered >> 0));
  L2_dir == backward >> L2_load == L1_load + ((S1_powered >> 1) && (!S1_powered >> 0));
  L2_dir == off >> L2_load == 0;

//Line L23
  (L23_dir != off && (L24_dir == forward) >> L23_dir == backward) &&
  (L23_dir == backward >> L23_dir != off && (L24_dir == forward));
  (L23_dir != off && (L22_dir == forward) >> L23_dir == forward) &&
  (L23_dir == forward >> L23_dir != off && (L22_dir == forward));
  L23_dir == forward >> L23_load == L24_load + ((S21_powered >> 1) && (!S21_powered >> 0));
  L23_dir == backward >> L23_load == L22_load + ((S20_powered >> 1) && (!S20_powered >> 0));
  L23_dir == off >> L23_load == 0;

//Line L7
  P1_powered >> ( (L7_dir != backward) );
  !P1_powered >> (
  ((L7_dir != off && (L6_dir == forward || L8_dir == backward) >> L7_dir == backward) &&
  (L7_dir == backward >> L7_dir != off && (L6_dir == forward || L8_dir == backward))) &&
  ((L7_dir != off && (L1_dir == backward || L15_dir == backward || L24_dir == backward || L25_dir == backward) >> L7_dir == forward) &&
  (L7_dir == forward >> L7_dir != off && (L1_dir == backward || L15_dir == backward || L24_dir == backward || L25_dir == backward)))
  );
  L7_dir == forward >> L7_load == L6_load + L8_load + ((S6_powered >> 1) && (!S6_powered >> 0));
  L7_dir == backward >> L7_load == L1_load + L15_load + L24_load + L25_load;
  L7_dir == off >> L7_load == 0;

//Line L20
  (L20_dir != off && (L21_dir == backward) >> L20_dir == backward) &&
  (L20_dir == backward >> L20_dir != off && (L21_dir == backward));
  (L20_dir != off && (L19_dir == forward) >> L20_dir == forward) &&
  (L20_dir == forward >> L20_dir != off && (L19_dir == forward));
  L20_dir == forward >> L20_load == L21_load + ((S18_powered >> 1) && (!S18_powered >> 0));
  L20_dir == backward >> L20_load == L19_load + ((S17_powered >> 1) && (!S17_powered >> 0));
  L20_dir == off >> L20_load == 0;

//Line L4
  (L4_dir != off && (L5_dir == backward) >> L4_dir == backward) &&
  (L4_dir == backward >> L4_dir != off && (L5_dir == backward));
  (L4_dir != off && (L3_dir == forward) >> L4_dir == forward) &&
  (L4_dir == forward >> L4_dir != off && (L3_dir == forward));
  L4_dir == forward >> L4_load == L5_load + ((S4_powered >> 1) && (!S4_powered >> 0));
  L4_dir == backward >> L4_load == L3_load + ((S3_powered >> 1) && (!S3_powered >> 0));
  L4_dir == off >> L4_load == 0;

//Line L14
  (L14_dir != off && (L15_dir == forward) >> L14_dir == backward) &&
  (L14_dir == backward >> L14_dir != off && (L15_dir == forward));
  (L14_dir != off && (L13_dir == forward) >> L14_dir == forward) &&
  (L14_dir == forward >> L14_dir != off && (L13_dir == forward));
  L14_dir == forward >> L14_load == L15_load + ((S13_powered >> 1) && (!S13_powered >> 0));
  L14_dir == backward >> L14_load == L13_load + ((S12_powered >> 1) && (!S12_powered >> 0));
  L14_dir == off >> L14_load == 0;

//Line L25
  P1_powered >> ( (L25_dir != backward) );
  !P1_powered >> (
  ((L25_dir != off && (L26_dir == backward) >> L25_dir == backward) &&
  (L25_dir == backward >> L25_dir != off && (L26_dir == backward))) &&
  ((L25_dir != off && (L1_dir == backward || L7_dir == backward || L15_dir == backward || L24_dir == backward) >> L25_dir == forward) &&
  (L25_dir == forward >> L25_dir != off && (L1_dir == backward || L7_dir == backward || L15_dir == backward || L24_dir == backward)))
  );
  L25_dir == forward >> L25_load == L26_load + ((S22_powered >> 1) && (!S22_powered >> 0));
  L25_dir == backward >> L25_load == L1_load + L7_load + L15_load + L24_load;
  L25_dir == off >> L25_load == 0;

//Line L5
  (L5_dir != off && (L6_dir == backward) >> L5_dir == backward) &&
  (L5_dir == backward >> L5_dir != off && (L6_dir == backward));
  (L5_dir != off && (L4_dir == forward) >> L5_dir == forward) &&
  (L5_dir == forward >> L5_dir != off && (L4_dir == forward));
  L5_dir == forward >> L5_load == L6_load + ((S5_powered >> 1) && (!S5_powered >> 0));
  L5_dir == backward >> L5_load == L4_load + ((S4_powered >> 1) && (!S4_powered >> 0));
  L5_dir == off >> L5_load == 0;

//Line L11
  (L11_dir != off && (L12_dir == backward) >> L11_dir == backward) &&
  (L11_dir == backward >> L11_dir != off && (L12_dir == backward));
  (L11_dir != off && (L10_dir == forward) >> L11_dir == forward) &&
  (L11_dir == forward >> L11_dir != off && (L10_dir == forward));
  L11_dir == forward >> L11_load == L12_load + ((S10_powered >> 1) && (!S10_powered >> 0));
  L11_dir == backward >> L11_load == L10_load + ((S9_powered >> 1) && (!S9_powered >> 0));
  L11_dir == off >> L11_load == 0;

//Line L26
  ((L26_dir == forward >> C1_state == sink) &&
 (C1_state == sink >> L26_dir == forward)) &&
  ((L26_dir == backward >> C1_state == source) &&
   (C1_state == source >> L26_dir == backward)) &&
  ((L26_dir == off >> C1_state == cp_off) &&
   (C1_state == cp_off >> L26_dir == off)) &&
  (C1_state == cp_off >> C1_flow == 0);
  (L26_dir != off && (L25_dir == forward) >> L26_dir == forward) &&
  (L26_dir == forward >> L26_dir != off && (L25_dir == forward));
  L26_dir == forward >> L26_load == C1_flow;
  L26_dir == backward >> L26_load == L25_load + ((S22_powered >> 1) && (!S22_powered >> 0));
  L26_dir == off >> L26_load == 0;