%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] Gamma_1: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] Gamma_2: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] Gamma_3: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] Gamma_4: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] Gamma_5: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] Gamma_6: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) Gamma_7: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) Gamma_8: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) Gamma_9: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) Gamma_10: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) Gamma_11: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) Gamma_12: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) Gamma_13: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) Gamma_14: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) Gamma_15: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) Gamma_16: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) Gamma_17: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) 17: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), ~(well_founded_relation(esk3_0)), [well_ordering( esk3_0)], ~(relation(esk3_0)) Gamma_18: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) 17: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), ~(well_founded_relation(esk3_0)), [well_ordering( esk3_0)], ~(relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_19: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) 17: [~(well_ordering(esk3_0))] 18: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), ~(well_founded_relation(esk3_0)), [well_ordering( esk3_0)], ~(relation(esk3_0)) Gamma_20: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) 17: [~(well_ordering(esk3_0))] 18: [~(reflexive(esk3_0))], ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), ~(well_founded_relation(esk3_0)), ~(relation(esk3_0)) Gamma_21: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) 17: [~(well_ordering(esk3_0))] 18: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) Gamma_22: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 17: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) 18: [~(well_ordering(esk3_0))] Gamma_23: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 17: [~(epred1_2(esk3_0,esk2_0))], ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), ~(well_founded_relation(esk2_0)), ~( relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_24: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 17: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), [~(well_founded_relation(esk2_0))], ~( relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_25: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), [~(well_founded_relation(esk2_0))], ~( relation(esk3_0)) 16: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 17: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_26: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), [~(well_founded_relation(esk2_0))], ~( relation(esk3_0)) 16: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk2_0)) 17: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_27: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), [~(well_founded_relation(esk2_0))], ~( relation(esk3_0)) 16: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 17: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_28: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), [~(well_founded_relation(esk2_0))], ~( relation(esk3_0)) 17: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_29: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 15: [~(epred1_2(esk3_0,esk2_0))], ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk2_0)), ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 16: [~(well_ordering(esk3_0))] Gamma_30: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 16: [~(well_ordering(esk3_0))] Gamma_31: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 14: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 16: [~(well_ordering(esk3_0))] Gamma_32: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(well_ordering(esk2_0))], ~(relation(esk3_0)), ~( relation(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 16: [~(well_ordering(esk3_0))] Gamma_33: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 16: [~(well_ordering(esk3_0))] Gamma_34: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 16: [~(well_ordering(esk3_0))] Gamma_35: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 13: [~(epred1_2(esk3_0,esk2_0))], ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk2_0)), ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 14: [~(well_ordering(esk3_0))] Gamma_36: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 14: [~(well_ordering(esk3_0))] Gamma_37: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 12: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 14: [~(well_ordering(esk3_0))] Gamma_38: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( well_ordering(esk2_0))], ~(relation(esk3_0)), ~(relation(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 14: [~(well_ordering(esk3_0))] Gamma_39: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 14: [~(well_ordering(esk3_0))] Gamma_40: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 14: [~(well_ordering(esk3_0))] Gamma_41: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 11: [~(epred1_2(esk3_0,esk2_0))], ~(reflexive(esk3_0)), ~(transitive(esk2_0)), ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 12: [~(well_ordering(esk3_0))] Gamma_42: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk2_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 12: [~(well_ordering(esk3_0))] Gamma_43: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk2_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 10: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 12: [~(well_ordering(esk3_0))] Gamma_44: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk2_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 12: [~(well_ordering(esk3_0))] Gamma_45: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk2_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 12: [~(well_ordering(esk3_0))] Gamma_46: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk2_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 12: [~(well_ordering(esk3_0))] Gamma_47: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 9: [~(epred1_2(esk3_0,esk2_0))], ~(reflexive(esk2_0)), ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 10: [~(well_ordering(esk3_0))] Gamma_48: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 10: [~(well_ordering(esk3_0))] Gamma_49: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 8: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 10: [~(well_ordering(esk3_0))] Gamma_50: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [~(well_ordering(esk2_0))], ~(relation(esk3_0)), ~( relation(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 10: [~(well_ordering(esk3_0))] Gamma_51: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 8: [~(epred1_2(esk3_0,esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 10: [~(well_ordering(esk3_0))] Gamma_52: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: [~(epred1_2(esk3_0,esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 7: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 10: [~(well_ordering(esk3_0))] Gamma_53: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: [~(epred1_2(esk3_0,esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 7: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 8: [~(well_ordering(esk3_0))] Gamma_54: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: [~(epred1_2(esk3_0,esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 7: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 8: [~(well_ordering(esk3_0))] Gamma_55: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 6: [well_ordering(esk2_0)] 7: [~(epred1_2(esk3_0,esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 8: [~(well_ordering(esk3_0))] Gamma_56: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 6: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))], ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 7: [~(well_ordering(esk3_0))] Gamma_57: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)), [~(function(esk4_0))] 7: [~(well_ordering(esk3_0))] Gamma_58: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)), [~(function(esk4_0))] 5: [function(esk4_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 7: [~(well_ordering(esk3_0))] Gamma_59: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)), [~(function(esk4_0))] 5: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))], ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)) 6: [~(well_ordering(esk3_0))] Gamma_60: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)), [~(function(esk4_0))] 5: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), [~( relation(esk4_0))], ~(relation(esk2_0)) 6: [~(well_ordering(esk3_0))] Gamma_61: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), [~( relation(esk4_0))], ~(relation(esk2_0)) 4: [relation(esk4_0)] 5: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)), [~(function(esk4_0))] 6: [~(well_ordering(esk3_0))] Gamma_62: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), [~( relation(esk4_0))], ~(relation(esk2_0)) 4: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))], ~(relation(esk3_0)), ~( relation(esk2_0)) 5: [~(well_ordering(esk3_0))] Gamma_63: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), [~( relation(esk4_0))], ~(relation(esk2_0)) 4: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk3_0))], ~( relation(esk2_0)) 5: [~(well_ordering(esk3_0))] Gamma_64: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk3_0))], ~( relation(esk2_0)) 3: [relation(esk3_0)] 4: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), [~( relation(esk4_0))], ~(relation(esk2_0)) 5: [~(well_ordering(esk3_0))] Gamma_65: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk3_0))], ~( relation(esk2_0)) 3: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))], ~(relation(esk2_0)) 4: [~(well_ordering(esk3_0))] Gamma_66: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk3_0))], ~( relation(esk2_0)) 3: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk2_0))] 4: [~(well_ordering(esk3_0))] Gamma_67: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk2_0))] 2: [relation(esk2_0)] 3: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk3_0))], ~( relation(esk2_0)) 4: [~(well_ordering(esk3_0))] Gamma_68: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk2_0))] 2: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))] 3: [~(well_ordering(esk3_0))] Gamma_69: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk2_0))] 2: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))] 3: [~(well_ordering(esk3_0))] Gamma_70: (move) 0: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))] 1: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 2: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk2_0))] 3: [~(well_ordering(esk3_0))] Gamma_71: (resolve) 0: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))] 1: [] 2: [~(well_ordering(esk3_0))] SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] Gamma_1: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] Gamma_2: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] Gamma_3: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] Gamma_4: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] Gamma_5: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] Gamma_6: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) Gamma_7: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) Gamma_8: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) Gamma_9: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) Gamma_10: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) Gamma_11: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) Gamma_12: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) Gamma_13: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) Gamma_14: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) Gamma_15: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) Gamma_16: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) Gamma_17: (extend-no-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) 17: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), ~(well_founded_relation(esk3_0)), [well_ordering( esk3_0)], ~(relation(esk3_0)) Gamma_18: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) 17: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), ~(well_founded_relation(esk3_0)), [well_ordering( esk3_0)], ~(relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_19: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) 17: [~(well_ordering(esk3_0))] 18: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), ~(well_founded_relation(esk3_0)), [well_ordering( esk3_0)], ~(relation(esk3_0)) Gamma_20: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) 17: [~(well_ordering(esk3_0))] 18: [~(reflexive(esk3_0))], ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), ~(well_founded_relation(esk3_0)), ~(relation(esk3_0)) Gamma_21: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) 17: [~(well_ordering(esk3_0))] 18: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) Gamma_22: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 17: ~(epred1_2(esk3_0,esk2_0)), [well_founded_relation(esk3_0)], ~( well_founded_relation(esk2_0)) 18: [~(well_ordering(esk3_0))] Gamma_23: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 17: [~(epred1_2(esk3_0,esk2_0))], ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), ~(well_founded_relation(esk2_0)), ~( relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_24: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 16: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 17: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), [~(well_founded_relation(esk2_0))], ~( relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_25: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), [~(well_founded_relation(esk2_0))], ~( relation(esk3_0)) 16: [well_founded_relation(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 17: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_26: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), [~(well_founded_relation(esk2_0))], ~( relation(esk3_0)) 16: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk2_0)) 17: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_27: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), [~(well_founded_relation(esk2_0))], ~( relation(esk3_0)) 16: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 17: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_28: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), [connected(esk3_0)], ~(connected(esk2_0)) 16: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk3_0)), [~(well_founded_relation(esk2_0))], ~( relation(esk3_0)) 17: ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~(antisymmetric(esk3_0)), ~( connected(esk3_0)), [~(well_founded_relation(esk3_0))], ~(relation(esk3_0)) 18: [~(well_ordering(esk3_0))] Gamma_29: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 15: [~(epred1_2(esk3_0,esk2_0))], ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), ~(connected(esk2_0)), ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 16: [~(well_ordering(esk3_0))] Gamma_30: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 16: [~(well_ordering(esk3_0))] Gamma_31: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 14: [connected(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 16: [~(well_ordering(esk3_0))] Gamma_32: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(well_ordering(esk2_0))], ~(relation(esk3_0)), ~( relation(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 16: [~(well_ordering(esk3_0))] Gamma_33: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 16: [~(well_ordering(esk3_0))] Gamma_34: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), [antisymmetric(esk3_0)], ~(antisymmetric(esk2_0)) 14: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 15: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk3_0)), [~(connected(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 16: [~(well_ordering(esk3_0))] Gamma_35: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 13: [~(epred1_2(esk3_0,esk2_0))], ~(reflexive(esk3_0)), ~(transitive(esk3_0)), ~( antisymmetric(esk2_0)), ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 14: [~(well_ordering(esk3_0))] Gamma_36: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 14: [~(well_ordering(esk3_0))] Gamma_37: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 12: [antisymmetric(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 14: [~(well_ordering(esk3_0))] Gamma_38: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( well_ordering(esk2_0))], ~(relation(esk3_0)), ~(relation(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 14: [~(well_ordering(esk3_0))] Gamma_39: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 14: [~(well_ordering(esk3_0))] Gamma_40: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), [transitive(esk3_0)], ~(transitive(esk2_0)) 12: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 13: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), ~(transitive(esk3_0)), [~( antisymmetric(esk3_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 14: [~(well_ordering(esk3_0))] Gamma_41: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 11: [~(epred1_2(esk3_0,esk2_0))], ~(reflexive(esk3_0)), ~(transitive(esk2_0)), ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 12: [~(well_ordering(esk3_0))] Gamma_42: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk2_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 12: [~(well_ordering(esk3_0))] Gamma_43: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk2_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 10: [transitive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 12: [~(well_ordering(esk3_0))] Gamma_44: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk2_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 12: [~(well_ordering(esk3_0))] Gamma_45: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk2_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 12: [~(well_ordering(esk3_0))] Gamma_46: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), [reflexive(esk3_0)], ~(reflexive(esk2_0)) 10: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk2_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 11: ~(epred1_2(esk3_0,esk2_0)), ~(reflexive(esk3_0)), [~(transitive(esk3_0))], ~( well_ordering(esk2_0)), ~(relation(esk3_0)), ~(relation(esk2_0)) 12: [~(well_ordering(esk3_0))] Gamma_47: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 9: [~(epred1_2(esk3_0,esk2_0))], ~(reflexive(esk2_0)), ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 10: [~(well_ordering(esk3_0))] Gamma_48: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 10: [~(well_ordering(esk3_0))] Gamma_49: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 8: [reflexive(esk2_0)], ~(well_ordering(esk2_0)), ~(relation(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 10: [~(well_ordering(esk3_0))] Gamma_50: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [~(well_ordering(esk2_0))], ~(relation(esk3_0)), ~( relation(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 10: [~(well_ordering(esk3_0))] Gamma_51: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 7: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 8: [~(epred1_2(esk3_0,esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 10: [~(well_ordering(esk3_0))] Gamma_52: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: [~(epred1_2(esk3_0,esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 7: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [epred1_2(esk3_0, esk2_0)], ~(relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~( function(esk4_0)) 8: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk2_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 9: ~(epred1_2(esk3_0,esk2_0)), [~(reflexive(esk3_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk2_0)) 10: [~(well_ordering(esk3_0))] Gamma_53: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: [~(epred1_2(esk3_0,esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 7: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))], ~(well_ordering(esk2_0)), ~( relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 8: [~(well_ordering(esk3_0))] Gamma_54: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: [well_ordering(esk2_0)] 6: [~(epred1_2(esk3_0,esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 7: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 8: [~(well_ordering(esk3_0))] Gamma_55: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 6: [well_ordering(esk2_0)] 7: [~(epred1_2(esk3_0,esk2_0))], ~(well_ordering(esk2_0)), ~(relation(esk3_0)), ~( relation(esk2_0)) 8: [~(well_ordering(esk3_0))] Gamma_56: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 6: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))], ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 7: [~(well_ordering(esk3_0))] Gamma_57: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: [function(esk4_0)] 5: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)), [~(function(esk4_0))] 7: [~(well_ordering(esk3_0))] Gamma_58: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)), [~(function(esk4_0))] 5: [function(esk4_0)] 6: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(well_ordering(esk2_0))], ~( relation(esk3_0)), ~(relation(esk4_0)), ~(relation(esk2_0)), ~(function(esk4_0)) 7: [~(well_ordering(esk3_0))] Gamma_59: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)), [~(function(esk4_0))] 5: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))], ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)) 6: [~(well_ordering(esk3_0))] Gamma_60: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: [relation(esk4_0)] 4: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)), [~(function(esk4_0))] 5: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), [~( relation(esk4_0))], ~(relation(esk2_0)) 6: [~(well_ordering(esk3_0))] Gamma_61: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), [~( relation(esk4_0))], ~(relation(esk2_0)) 4: [relation(esk4_0)] 5: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), ~( relation(esk4_0)), ~(relation(esk2_0)), [~(function(esk4_0))] 6: [~(well_ordering(esk3_0))] Gamma_62: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), [~( relation(esk4_0))], ~(relation(esk2_0)) 4: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))], ~(relation(esk3_0)), ~( relation(esk2_0)) 5: [~(well_ordering(esk3_0))] Gamma_63: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: [relation(esk3_0)] 3: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), [~( relation(esk4_0))], ~(relation(esk2_0)) 4: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk3_0))], ~( relation(esk2_0)) 5: [~(well_ordering(esk3_0))] Gamma_64: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk3_0))], ~( relation(esk2_0)) 3: [relation(esk3_0)] 4: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), ~(relation(esk3_0)), [~( relation(esk4_0))], ~(relation(esk2_0)) 5: [~(well_ordering(esk3_0))] Gamma_65: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: [relation(esk2_0)] 2: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk3_0))], ~( relation(esk2_0)) 3: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))], ~(relation(esk2_0)) 4: [~(well_ordering(esk3_0))] Gamma_66: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: [relation(esk2_0)] 2: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk3_0))], ~( relation(esk2_0)) 3: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk2_0))] 4: [~(well_ordering(esk3_0))] Gamma_67: (move) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk2_0))] 2: [relation(esk2_0)] 3: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk3_0))], ~( relation(esk2_0)) 4: [~(well_ordering(esk3_0))] Gamma_68: (resolve) 0: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 1: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk2_0))] 2: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))] 3: [~(well_ordering(esk3_0))] Gamma_69: (extend-conflict) 0: [relation_isomorphism(esk2_0,esk3_0, esk4_0)] 1: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk2_0))] 2: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))] 3: [~(well_ordering(esk3_0))] Gamma_70: (move) 0: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))] 1: [relation_isomorphism(esk2_0,esk3_0,esk4_0)] 2: ~(relation_isomorphism(esk2_0,esk3_0,esk4_0)), [~(relation(esk2_0))] 3: [~(well_ordering(esk3_0))] Gamma_71: (resolve) 0: [~(relation_isomorphism(esk2_0,esk3_0,esk4_0))] 1: [] 2: [~(well_ordering(esk3_0))] SZS status Unsatisfiable