{
  (* Indices to add *)
  indices_passive = [
    subsumptionIndex;
    lightNormIndex;
  ];

  indices_active = [
    fwDemodIndex;
    bwDemodIndex;
  ];

  indices_immediate = [
    subsumptionIndex;
    fwDemodIndex;
    bwDemodIndex;
    lightNormIndex;
  ];

  indices_input = [
    subsumptionIndex;
    fwDemodIndex;
    bwDemodIndex;
    lightNormIndex;
  ];


  (* Light simplify, triggered before adding clauses to passive *)
  light_triv = [
    trivRules;
  ];

  light_fw = [
    lightNorm;
  ];

  light_bw = [
  ];


  (* Full simplify, triggered on given clause before adding to active *)
  full_triv = [

  ];

  full_fw = [
    fwDemodLoopTriv;
    fwSubsumptionStrict;
    fwSubsumptionRes;
  ];

  full_bw = [
    bwDemod;
    (* bwSubsumption; *)
    (* bwSubsumptionRes; *)
  ];


  (* Immediate simplify, triggered on conclusions of given clause (cleared every iteration) *)
  (* *_main are simplifications wrt whole set *)
  (* *_immed are simplifications wrt immediate set *)
  immed_triv = [
    trivRules
  ];

  immed_fw_main = [
    lightNorm;
    (* fwDemodLoopTriv; *)
    (* fwSubsumption; *)
    (* fwSubsumptionRes; *)
  ];

  immed_fw_immed = [
    lightNorm;
    fwDemodLoopTriv;
    fwSubsumption;
    fwSubsumptionRes;
  ];

  immed_bw_main = [

  ];

  immed_bw_immed = [
    bwDemod;
    bwSubsumption;
    bwSubsumptionRes;
  ];


  (* Input simplify, triggered on input clauses *)
  input_triv = [
    trivRules;
  ];

  input_fw = [
    lightNorm;
    fwDemodLoopTriv;
    fwSubsumption;
    fwSubsumptionRes;
  ];

  input_bw = [
    bwDemod;
    bwSubsumption;
    bwSubsumptionRes;
  ];
}