%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------%

------ Parsing...successful


------ Proving...
use I-

Gamma_0: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]

Gamma_1: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]

Gamma_2: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]

Gamma_3: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]

Gamma_4: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]

Gamma_5: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]

Gamma_6: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]

Gamma_7: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]

Gamma_8: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]

Gamma_9: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]

Gamma_10: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]

Gamma_11: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]

Gamma_12: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]

Gamma_13: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))

Gamma_14: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))

Gamma_15: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), [greater(
sk1(sk12,sk3),sk1(sk11,sk2))], ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))

Gamma_16: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), [greater(
sk1(sk12,sk3),sk1(sk11,sk2))], ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))
  16: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [greater(
sk8,sk7)], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))

Gamma_17: (extend-no-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), [greater(
sk1(sk12,sk3),sk1(sk11,sk2))], ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))
  16: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [greater(
sk8,sk7)], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))
  17: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [greater(
sk6,sk5)], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))

Gamma_18: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), [greater(
sk1(sk12,sk3),sk1(sk11,sk2))], ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))
  16: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [greater(
sk8,sk7)], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))
  17: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [greater(
sk6,sk5)], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))
  18: ~(greater(sk8,sk7)), [~(greater(sk6,sk5))]

Gamma_19: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), [greater(
sk1(sk12,sk3),sk1(sk11,sk2))], ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))
  16: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [greater(
sk8,sk7)], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))
  17: ~(greater(sk8,sk7)), [~(greater(sk6,sk5))]
  18: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [greater(
sk6,sk5)], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))

Gamma_20: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), [greater(
sk1(sk12,sk3),sk1(sk11,sk2))], ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))
  16: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [greater(
sk8,sk7)], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))
  17: ~(greater(sk8,sk7)), [~(greater(sk6,sk5))]
  18: [~(reproducibility(sk3,sk1(sk12,sk3),sk12))], ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), ~(
greater(sk8,sk7)), ~(organization(sk3,sk12)), ~(organization(sk2,sk11))

Gamma_21: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), [greater(
sk1(sk12,sk3),sk1(sk11,sk2))], ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))
  16: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [greater(
sk8,sk7)], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))
  17: ~(greater(sk8,sk7)), [~(greater(sk6,sk5))]
  18: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [~(
greater(sk8,sk7))], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))

Gamma_22: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), [greater(
sk1(sk12,sk3),sk1(sk11,sk2))], ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))
  16: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [~(
greater(sk8,sk7))], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))
  17: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [greater(
sk8,sk7)], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))
  18: ~(greater(sk8,sk7)), [~(greater(sk6,sk5))]

Gamma_23: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), [greater(
sk1(sk12,sk3),sk1(sk11,sk2))], ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))
  16: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [~(
greater(sk8,sk7))], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))
  17: [~(reproducibility(sk3,sk1(sk12,sk3),sk12))], ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), ~(
organization(sk3,sk12)), ~(organization(sk2,sk11))

Gamma_24: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), [greater(
sk1(sk12,sk3),sk1(sk11,sk2))], ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))
  16: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [~(
greater(sk8,sk7))], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))
  17: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), [~(greater(sk1(sk12,sk3),sk1(sk11,sk2)))], ~(
organization(sk3,sk12)), ~(organization(sk2,sk11))

Gamma_25: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), [~(greater(sk1(sk12,sk3),sk1(sk11,sk2)))], ~(
organization(sk3,sk12)), ~(organization(sk2,sk11))
  16: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), [greater(
sk1(sk12,sk3),sk1(sk11,sk2))], ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))
  17: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), ~(greater(sk1(sk12,sk3),sk1(sk11,sk2))), [~(
greater(sk8,sk7))], ~(organization(sk3,sk12)), ~(organization(sk2,sk11))

Gamma_26: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), [~(greater(sk1(sk12,sk3),sk1(sk11,sk2)))], ~(
organization(sk3,sk12)), ~(organization(sk2,sk11))
  16: [~(reproducibility(sk3,sk1(sk12,sk3),sk12))], ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))

Gamma_27: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), [~(greater(sk1(sk12,sk3),sk1(sk11,sk2)))], ~(
organization(sk3,sk12)), ~(organization(sk2,sk11))
  16: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), [~(reproducibility(sk2,sk1(sk11,sk2),sk11))], ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))

Gamma_28: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), [~(reproducibility(sk2,sk1(sk11,sk2),sk11))], ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))
  15: [reproducibility(sk2,sk1(sk11,sk2),sk11)], ~(organization(sk2,sk11))
  16: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(reproducibility(sk2,sk1(sk11,sk2),sk11)), ~(
accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(
reliability(sk2,sk5,sk11)), [~(greater(sk1(sk12,sk3),sk1(sk11,sk2)))], ~(
organization(sk3,sk12)), ~(organization(sk2,sk11))

Gamma_29: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), [~(reproducibility(sk2,sk1(sk11,sk2),sk11))], ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), ~(size(sk3,sk10,sk12)), ~(
size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(
reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), ~(
greater(sk10,sk9)), ~(organization(sk3,sk12)), [~(organization(sk2,sk11))]

Gamma_30: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  14: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), [~(reproducibility(sk2,sk1(sk11,sk2),sk11))], ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))
  15: [~(reproducibility(sk3,sk1(sk12,sk3),sk12))], ~(size(sk3,sk10,sk12)), ~(
size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(
reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), ~(
greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(organization(sk2,sk11))

Gamma_31: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [~(reproducibility(sk3,sk1(sk12,sk3),sk12))], ~(size(sk3,sk10,sk12)), ~(
size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(
reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), ~(
greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(organization(sk2,sk11))
  14: [reproducibility(sk3,sk1(sk12,sk3),sk12)], ~(organization(sk3,sk12))
  15: ~(reproducibility(sk3,sk1(sk12,sk3),sk12)), [~(reproducibility(sk2,sk1(sk11,sk2),sk11))], ~(
size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(
organization(sk2,sk11))

Gamma_32: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [~(reproducibility(sk3,sk1(sk12,sk3),sk12))], ~(size(sk3,sk10,sk12)), ~(
size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(
reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), ~(
greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(organization(sk2,sk11))
  14: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), [~(organization(sk3,sk12))], ~(
organization(sk2,sk11))

Gamma_33: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: [organization(sk2,sk11)]
  13: [~(reproducibility(sk3,sk1(sk12,sk3),sk12))], ~(size(sk3,sk10,sk12)), ~(
size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(
reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), ~(
greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(organization(sk2,sk11))
  14: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), [~(
organization(sk2,sk11))]

Gamma_34: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), [~(
organization(sk2,sk11))]
  13: [organization(sk2,sk11)]
  14: [~(reproducibility(sk3,sk1(sk12,sk3),sk12))], ~(size(sk3,sk10,sk12)), ~(
size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(accountability(sk2,sk7,sk11)), ~(
reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(class(sk3,sk4,sk12)), ~(
class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(reorganization_free(sk2,sk11,sk11)), ~(
greater(sk10,sk9)), ~(organization(sk3,sk12)), ~(organization(sk2,sk11))

Gamma_35: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), [~(
organization(sk2,sk11))]
  13: [~(size(sk3,sk10,sk12))], ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), ~(organization(sk3,sk12))

Gamma_36: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: [organization(sk3,sk12)]
  12: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), [~(
organization(sk2,sk11))]
  13: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), [~(organization(sk3,sk12))]

Gamma_37: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), [~(organization(sk3,sk12))]
  12: [organization(sk3,sk12)]
  13: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), ~(organization(sk3,sk12)), [~(
organization(sk2,sk11))]

Gamma_38: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), [~(organization(sk3,sk12))]
  12: [~(size(sk3,sk10,sk12))], ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9))

Gamma_39: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: [greater(sk10,sk9)]
  11: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), [~(organization(sk3,sk12))]
  12: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), [~(greater(sk10,sk9))]

Gamma_40: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), [~(greater(sk10,sk9))]
  11: [greater(sk10,sk9)]
  12: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), ~(greater(sk10,sk9)), [~(organization(sk3,sk12))]

Gamma_41: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), [~(greater(sk10,sk9))]
  11: [~(size(sk3,sk10,sk12))], ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11))

Gamma_42: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: [reorganization_free(sk2,sk11,sk11)]
  10: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), [~(greater(sk10,sk9))]
  11: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), [~(
reorganization_free(sk2,sk11,sk11))]

Gamma_43: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), [~(
reorganization_free(sk2,sk11,sk11))]
  10: [reorganization_free(sk2,sk11,sk11)]
  11: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), ~(
reorganization_free(sk2,sk11,sk11)), [~(greater(sk10,sk9))]

Gamma_44: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), [~(
reorganization_free(sk2,sk11,sk11))]
  10: [~(size(sk3,sk10,sk12))], ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12))

Gamma_45: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: [reorganization_free(sk3,sk12,sk12)]
  9: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), [~(
reorganization_free(sk2,sk11,sk11))]
  10: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), [~(reorganization_free(sk3,sk12,sk12))]

Gamma_46: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), [~(reorganization_free(sk3,sk12,sk12))]
  9: [reorganization_free(sk3,sk12,sk12)]
  10: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), ~(reorganization_free(sk3,sk12,sk12)), [~(
reorganization_free(sk2,sk11,sk11))]

Gamma_47: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), [~(reorganization_free(sk3,sk12,sk12))]
  9: [~(size(sk3,sk10,sk12))], ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11))

Gamma_48: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: [class(sk2,sk4,sk11)]
  8: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), [~(reorganization_free(sk3,sk12,sk12))]
  9: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), [~(class(sk2,sk4,sk11))]

Gamma_49: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), [~(class(sk2,sk4,sk11))]
  8: [class(sk2,sk4,sk11)]
  9: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), ~(class(sk2,sk4,sk11)), [~(reorganization_free(sk3,sk12,sk12))]

Gamma_50: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), [~(class(sk2,sk4,sk11))]
  8: [~(size(sk3,sk10,sk12))], ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12))

Gamma_51: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: [class(sk3,sk4,sk12)]
  7: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), [~(class(sk2,sk4,sk11))]
  8: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), [~(
class(sk3,sk4,sk12))]

Gamma_52: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), [~(
class(sk3,sk4,sk12))]
  7: [class(sk3,sk4,sk12)]
  8: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), ~(
class(sk3,sk4,sk12)), [~(class(sk2,sk4,sk11))]

Gamma_53: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), [~(
class(sk3,sk4,sk12))]
  7: [~(size(sk3,sk10,sk12))], ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11))

Gamma_54: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: [reliability(sk2,sk5,sk11)]
  6: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), [~(
class(sk3,sk4,sk12))]
  7: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), [~(reliability(sk2,sk5,sk11))]

Gamma_55: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), [~(reliability(sk2,sk5,sk11))]
  6: [reliability(sk2,sk5,sk11)]
  7: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), ~(reliability(sk2,sk5,sk11)), [~(
class(sk3,sk4,sk12))]

Gamma_56: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), [~(reliability(sk2,sk5,sk11))]
  6: [~(size(sk3,sk10,sk12))], ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12))

Gamma_57: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: [reliability(sk3,sk6,sk12)]
  5: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), [~(reliability(sk2,sk5,sk11))]
  6: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), [~(reliability(sk3,sk6,sk12))]

Gamma_58: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), [~(reliability(sk3,sk6,sk12))]
  5: [reliability(sk3,sk6,sk12)]
  6: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), ~(reliability(sk3,sk6,sk12)), [~(reliability(sk2,sk5,sk11))]

Gamma_59: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), [~(reliability(sk3,sk6,sk12))]
  5: [~(size(sk3,sk10,sk12))], ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11))

Gamma_60: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: [accountability(sk2,sk7,sk11)]
  4: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), [~(reliability(sk3,sk6,sk12))]
  5: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), [~(
accountability(sk2,sk7,sk11))]

Gamma_61: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), [~(
accountability(sk2,sk7,sk11))]
  4: [accountability(sk2,sk7,sk11)]
  5: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), ~(
accountability(sk2,sk7,sk11)), [~(reliability(sk3,sk6,sk12))]

Gamma_62: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), [~(
accountability(sk2,sk7,sk11))]
  4: [~(size(sk3,sk10,sk12))], ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12))

Gamma_63: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: [accountability(sk3,sk8,sk12)]
  3: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), [~(
accountability(sk2,sk7,sk11))]
  4: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), [~(accountability(sk3,sk8,sk12))]

Gamma_64: (move)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), [~(accountability(sk3,sk8,sk12))]
  3: [accountability(sk3,sk8,sk12)]
  4: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), ~(accountability(sk3,sk8,sk12)), [~(
accountability(sk2,sk7,sk11))]

Gamma_65: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), [~(accountability(sk3,sk8,sk12))]
  3: [~(size(sk3,sk10,sk12))], ~(size(sk2,sk9,sk11))

Gamma_66: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: [size(sk2,sk9,sk11)]
  2: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), [~(accountability(sk3,sk8,sk12))]
  3: ~(size(sk3,sk10,sk12)), [~(size(sk2,sk9,sk11))]

Gamma_67: (move)
  0: [size(sk3,sk10,sk12)]
  1: ~(size(sk3,sk10,sk12)), [~(size(sk2,sk9,sk11))]
  2: [size(sk2,sk9,sk11)]
  3: ~(size(sk3,sk10,sk12)), ~(size(sk2,sk9,sk11)), [~(accountability(sk3,sk8,sk12))]

Gamma_68: (resolve)
  0: [size(sk3,sk10,sk12)]
  1: ~(size(sk3,sk10,sk12)), [~(size(sk2,sk9,sk11))]
  2: [~(size(sk3,sk10,sk12))]

Gamma_69: (extend-conflict)
  0: [size(sk3,sk10,sk12)]
  1: ~(size(sk3,sk10,sk12)), [~(size(sk2,sk9,sk11))]
  2: [~(size(sk3,sk10,sk12))]

Gamma_70: (move)
  0: [~(size(sk3,sk10,sk12))]
  1: [size(sk3,sk10,sk12)]
  2: ~(size(sk3,sk10,sk12)), [~(size(sk2,sk9,sk11))]

Gamma_71: (resolve)
  0: [~(size(sk3,sk10,sk12))]
  1: []

SZS status Unsatisfiable