%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : CAT001-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Jul 15 06:16:17 AM UTC 2025 % Result : Satisfiable 2.52s 2.74s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : CAT001-10 : TPTP v9.0.0. Released v7.5.0. % 0.03/0.11 % Command : run_Leo-III %s %d THM % 0.12/0.32 % Computer : n006.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Mon Jul 14 04:36:34 EDT 2025 % 0.12/0.32 % CPUTime : % 2.52/2.74 % SZS status Satisfiable % 2.52/2.74 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 2.52/2.74 2: domain(b) -> codomain(a) % 2.52/2.74 4: domain(h) -> codomain(a) % 2.52/2.74 6: domain(g) -> codomain(a) % 2.52/2.74 7: codomain(domain(X)) -> domain(X) % 2.52/2.74 8: domain(codomain(X)) -> codomain(X) % 2.52/2.74 9: compose(a, h) -> compose(a, g) % 2.52/2.74 10: domain(domain(X)) -> domain(X) % 2.52/2.74 11: codomain(codomain(X)) -> codomain(X) % 2.52/2.74 12: compose(domain(X), X) -> X % 2.52/2.74 13: compose(X, codomain(X)) -> X % 2.52/2.74 14: ifeq(X, X, Y, Z) -> Y % 2.52/2.74 15: compose(codomain(a), b) -> b % 2.52/2.74 16: compose(codomain(a), g) -> g % 2.52/2.74 17: compose(codomain(a), h) -> h % 2.52/2.74 18: compose(codomain(X), codomain(X)) -> codomain(X) % 2.52/2.74 19: compose(domain(X), domain(X)) -> domain(X) % 2.52/2.74 20: ifeq(codomain(X), domain(Y), codomain(compose(X, Y)), codomain(Y)) -> codomain(Y) % 2.52/2.74 21: codomain(h) -> codomain(compose(a, g)) % 2.52/2.74 22: compose(h, codomain(compose(a, g))) -> h % 2.52/2.74 23: ifeq(codomain(X), domain(Y), domain(compose(X, Y)), domain(X)) -> domain(X) % 2.52/2.74 24: domain(compose(a, g)) -> domain(a) % 2.52/2.74 25: compose(domain(a), compose(a, g)) -> compose(a, g) % 2.52/2.74 26: ifeq(codomain(X), codomain(a), domain(compose(X, b)), domain(X)) -> domain(X) % 2.52/2.74 27: domain(compose(a, b)) -> domain(a) % 2.52/2.74 28: compose(domain(a), compose(a, b)) -> compose(a, b) % 2.52/2.74 29: ifeq(codomain(X), codomain(a), domain(compose(X, h)), domain(X)) -> domain(X) % 2.52/2.74 30: ifeq(codomain(X), codomain(a), domain(compose(X, g)), domain(X)) -> domain(X) % 2.52/2.74 31: ifeq(codomain(b), domain(X), domain(compose(b, X)), codomain(a)) -> codomain(a) % 2.52/2.74 32: ifeq(codomain(g), domain(X), domain(compose(g, X)), codomain(a)) -> codomain(a) % 2.52/2.74 33: ifeq(codomain(X), codomain(a), codomain(compose(X, g)), codomain(g)) -> codomain(g) % 2.52/2.74 34: codomain(compose(a, g)) -> codomain(g) % 2.52/2.74 35: compose(h, codomain(g)) -> h % 2.52/2.74 36: compose(compose(a, g), codomain(g)) -> compose(a, g) % 2.52/2.74 37: ifeq(codomain(X), codomain(a), codomain(compose(X, h)), codomain(g)) -> codomain(g) % 2.52/2.74 38: ifeq(codomain(X), codomain(a), codomain(compose(X, b)), codomain(b)) -> codomain(b) % 2.52/2.74 39: codomain(compose(a, b)) -> codomain(b) % 2.52/2.74 40: compose(compose(a, b), codomain(b)) -> compose(a, b) % 2.52/2.74 41: ifeq(codomain(X), codomain(Y), codomain(compose(X, codomain(Y))), codomain(Y)) -> codomain(Y) % 2.52/2.74 42: ifeq(codomain(X), domain(Y), codomain(compose(X, domain(Y))), domain(Y)) -> domain(Y) % 2.52/2.74 43: ifeq(codomain(X), domain(Y), domain(compose(codomain(X), Y)), codomain(X)) -> codomain(X) % 2.52/2.74 44: ifeq(domain(X), domain(Y), codomain(compose(domain(X), Y)), codomain(Y)) -> codomain(Y) % 2.52/2.74 45: ifeq(domain(X), domain(Y), domain(compose(domain(X), Y)), domain(X)) -> domain(X) % 2.52/2.74 46: ifeq(codomain(X), codomain(Y), domain(compose(X, codomain(Y))), domain(X)) -> domain(X) % 2.52/2.74 47: ifeq(codomain(b), codomain(a), domain(compose(b, g)), codomain(a)) -> codomain(a) % 2.52/2.74 48: ifeq(codomain(b), codomain(a), domain(compose(b, b)), codomain(a)) -> codomain(a) % 2.52/2.74 49: ifeq(codomain(b), codomain(a), domain(compose(b, h)), codomain(a)) -> codomain(a) % 2.52/2.74 50: ifeq(codomain(g), codomain(a), domain(compose(g, g)), codomain(a)) -> codomain(a) % 2.52/2.74 51: ifeq(codomain(g), codomain(a), domain(compose(g, h)), codomain(a)) -> codomain(a) % 2.52/2.74 52: ifeq(codomain(g), codomain(a), domain(compose(g, b)), codomain(a)) -> codomain(a) % 2.52/2.74 53: ifeq(codomain(g), codomain(a), codomain(compose(h, h)), codomain(g)) -> codomain(g) % 2.52/2.74 54: ifeq(codomain(g), codomain(a), codomain(compose(h, b)), codomain(b)) -> codomain(b) % 2.52/2.74 55: ifeq(codomain(X), domain(Y), codomain(compose(codomain(X), Y)), codomain(Y)) -> codomain(Y) % 2.52/2.74 56: ifeq(codomain(X), domain(Y), domain(compose(X, domain(Y))), domain(X)) -> domain(X) % 2.52/2.74 57: ifeq(codomain(X), codomain(a), domain(compose(codomain(X), h)), codomain(X)) -> codomain(X) % 2.52/2.74 58: ifeq(codomain(g), domain(X), codomain(compose(h, domain(X))), domain(X)) -> domain(X) % 2.52/2.74 59: ifeq(codomain(X), codomain(a), domain(compose(codomain(X), b)), codomain(X)) -> codomain(X) % 2.52/2.74 60: ifeq(codomain(X), codomain(a), domain(compose(codomain(X), g)), codomain(X)) -> codomain(X) % 2.52/2.74 61: ifeq(domain(X), codomain(a), domain(compose(domain(X), h)), domain(X)) -> domain(X) % 2.52/2.74 62: ifeq(domain(X), codomain(a), domain(compose(domain(X), g)), domain(X)) -> domain(X) % 2.52/2.74 63: ifeq(domain(X), codomain(a), domain(compose(domain(X), b)), domain(X)) -> domain(X) % 2.52/2.74 64: ifeq(codomain(g), codomain(X), codomain(compose(h, codomain(X))), codomain(X)) -> codomain(X) % 2.52/2.74 65: ifeq(domain(X), codomain(a), codomain(compose(domain(X), g)), codomain(g)) -> codomain(g) % 2.52/2.74 66: ifeq(domain(X), codomain(a), codomain(compose(domain(X), h)), codomain(g)) -> codomain(g) % 2.52/2.74 67: ifeq(codomain(g), codomain(X), domain(compose(g, codomain(X))), codomain(a)) -> codomain(a) % 2.52/2.74 68: ifeq(codomain(b), codomain(X), domain(compose(b, codomain(X))), codomain(a)) -> codomain(a) % 2.52/2.74 69: ifeq(codomain(g), codomain(X), domain(compose(h, codomain(X))), codomain(a)) -> codomain(a) % 2.52/2.74 70: ifeq(domain(X), codomain(a), codomain(compose(domain(X), b)), codomain(b)) -> codomain(b) % 2.52/2.74 71: ifeq(codomain(X), codomain(a), codomain(compose(codomain(X), g)), codomain(g)) -> codomain(g) % 2.52/2.74 72: ifeq(codomain(X), codomain(a), codomain(compose(codomain(X), h)), codomain(g)) -> codomain(g) % 2.52/2.74 73: ifeq(codomain(g), domain(X), domain(compose(g, domain(X))), codomain(a)) -> codomain(a) % 2.52/2.74 74: ifeq(codomain(X), codomain(a), codomain(compose(codomain(X), b)), codomain(b)) -> codomain(b) % 2.52/2.74 75: ifeq(codomain(b), domain(X), domain(compose(b, domain(X))), codomain(a)) -> codomain(a) % 2.52/2.74 76: ifeq(codomain(g), domain(X), domain(compose(h, X)), codomain(a)) -> codomain(a) % 2.52/2.74 77: ifeq(codomain(g), codomain(a), domain(compose(h, b)), codomain(a)) -> codomain(a) % 2.52/2.74 78: ifeq(codomain(g), codomain(a), domain(compose(h, g)), codomain(a)) -> codomain(a) % 2.52/2.74 79: ifeq(codomain(g), codomain(a), domain(compose(h, h)), codomain(a)) -> codomain(a) % 2.52/2.74 80: ifeq(codomain(g), domain(X), domain(compose(h, domain(X))), codomain(a)) -> codomain(a) % 2.52/2.74 81: ifeq(codomain(X), domain(Y), codomain(compose(codomain(X), domain(Y))), domain(Y)) -> domain(Y) % 2.52/2.74 82: ifeq(codomain(X), domain(Y), domain(compose(codomain(X), domain(Y))), codomain(X)) -> codomain(X) % 2.52/2.74 83: ifeq(codomain(X), codomain(Y), domain(compose(codomain(X), codomain(Y))), codomain(X)) -> codomain(X) % 2.52/2.74 84: ifeq(domain(X), domain(Y), codomain(compose(domain(X), domain(Y))), domain(Y)) -> domain(Y) % 2.52/2.74 85: ifeq(domain(X), domain(Y), domain(compose(domain(X), domain(Y))), domain(X)) -> domain(X) % 2.52/2.74 86: ifeq(domain(X), codomain(Y), codomain(compose(domain(X), codomain(Y))), codomain(Y)) -> codomain(Y) % 2.52/2.74 87: ifeq(domain(X), codomain(Y), domain(compose(domain(X), codomain(Y))), domain(X)) -> domain(X) % 2.52/2.74 88: ifeq(codomain(X), codomain(Y), codomain(compose(codomain(X), codomain(Y))), codomain(Y)) -> codomain(Y) % 2.52/2.74 89: ifeq(codomain(g), domain(X), codomain(compose(h, X)), codomain(X)) -> codomain(X) % 2.52/2.74 90: ifeq(codomain(g), codomain(a), codomain(compose(h, g)), codomain(g)) -> codomain(g) % 2.52/2.74 91: ifeq(codomain(X), domain(a), domain(compose(X, compose(a, g))), domain(X)) -> domain(X) % 2.52/2.74 92: ifeq(codomain(b), domain(a), domain(compose(b, compose(a, g))), codomain(a)) -> codomain(a) % 2.52/2.74 93: ifeq(codomain(g), domain(a), domain(compose(g, compose(a, g))), codomain(a)) -> codomain(a) % 2.52/2.74 94: ifeq(codomain(g), domain(a), domain(compose(h, compose(a, g))), codomain(a)) -> codomain(a) % 2.52/2.74 95: ifeq(codomain(X), domain(a), domain(compose(X, compose(a, b))), domain(X)) -> domain(X) % 2.52/2.74 96: ifeq(codomain(g), domain(X), codomain(compose(compose(a, g), X)), codomain(X)) -> codomain(X) % 2.52/2.74 97: ifeq(codomain(b), domain(X), codomain(compose(compose(a, b), X)), codomain(X)) -> codomain(X) % 2.52/2.74 98: ifeq(codomain(X), domain(a), codomain(compose(X, compose(a, b))), codomain(b)) -> codomain(b) % 2.52/2.74 99: ifeq(codomain(b), domain(X), domain(compose(compose(a, b), X)), domain(a)) -> domain(a) % 2.52/2.74 100: ifeq(codomain(X), domain(a), codomain(compose(X, compose(a, g))), codomain(g)) -> codomain(g) % 2.52/2.74 101: ifeq(codomain(g), domain(X), domain(compose(compose(a, g), X)), domain(a)) -> domain(a) % 2.52/2.74 102: ifeq(codomain(X), domain(a), domain(compose(codomain(X), compose(a, g))), codomain(X)) -> codomain(X) % 2.52/2.74 103: ifeq(domain(X), domain(a), domain(compose(domain(X), compose(a, g))), domain(X)) -> domain(X) % 2.52/2.74 104: ifeq(codomain(g), domain(a), codomain(compose(h, compose(a, b))), codomain(b)) -> codomain(b) % 2.52/2.74 105: ifeq(codomain(g), domain(a), codomain(compose(h, compose(a, g))), codomain(g)) -> codomain(g) % 2.52/2.74 106: ifeq(codomain(g), codomain(a), codomain(compose(compose(a, g), b)), codomain(b)) -> codomain(b) % 2.52/2.74 107: ifeq(codomain(b), domain(a), domain(compose(b, compose(a, b))), codomain(a)) -> codomain(a) % 2.52/2.74 108: ifeq(codomain(b), codomain(a), domain(compose(compose(a, b), g)), domain(a)) -> domain(a) % 2.52/2.74 109: ifeq(codomain(g), codomain(a), domain(compose(compose(a, g), h)), domain(a)) -> domain(a) % 2.52/2.74 110: ifeq(codomain(g), codomain(a), domain(compose(compose(a, g), b)), domain(a)) -> domain(a) % 2.52/2.74 111: ifeq(codomain(g), codomain(a), codomain(compose(compose(a, g), g)), codomain(g)) -> codomain(g) % 2.52/2.74 112: ifeq(codomain(b), codomain(a), domain(compose(compose(a, b), h)), domain(a)) -> domain(a) % 2.52/2.74 113: ifeq(codomain(g), domain(a), domain(compose(h, compose(a, b))), codomain(a)) -> codomain(a) % 2.52/2.74 114: ifeq(codomain(g), codomain(a), domain(compose(compose(a, g), g)), domain(a)) -> domain(a) % 2.52/2.74 115: ifeq(codomain(g), codomain(a), codomain(compose(compose(a, g), h)), codomain(g)) -> codomain(g) % 2.52/2.74 116: ifeq(codomain(g), domain(a), domain(compose(g, compose(a, b))), codomain(a)) -> codomain(a) % 2.52/2.74 117: ifeq(codomain(b), codomain(a), domain(compose(compose(a, b), b)), domain(a)) -> domain(a) % 2.52/2.74 118: ifeq(codomain(b), codomain(a), codomain(compose(compose(a, b), h)), codomain(g)) -> codomain(g) % 2.52/2.74 119: ifeq(codomain(b), codomain(a), codomain(compose(compose(a, b), b)), codomain(b)) -> codomain(b) % 2.52/2.74 120: ifeq(codomain(b), codomain(a), codomain(compose(compose(a, b), g)), codomain(g)) -> codomain(g) % 2.52/2.74 121: ifeq(domain(X), domain(a), codomain(compose(domain(X), compose(a, g))), codomain(g)) -> codomain(g) % 2.52/2.74 122: ifeq(codomain(g), codomain(X), domain(compose(compose(a, g), codomain(X))), domain(a)) -> domain(a) % 2.52/2.74 123: ifeq(codomain(b), codomain(X), codomain(compose(compose(a, b), codomain(X))), codomain(X)) -> codomain(X) % 2.52/2.74 124: ifeq(codomain(g), codomain(X), codomain(compose(compose(a, g), codomain(X))), codomain(X)) -> codomain(X) % 2.52/2.74 125: ifeq(codomain(b), domain(X), codomain(compose(compose(a, b), domain(X))), domain(X)) -> domain(X) % 2.52/2.74 126: ifeq(codomain(X), domain(a), domain(compose(codomain(X), compose(a, b))), codomain(X)) -> codomain(X) % 2.52/2.74 127: ifeq(codomain(g), domain(X), codomain(compose(compose(a, g), domain(X))), domain(X)) -> domain(X) % 2.52/2.74 128: ifeq(domain(X), domain(a), domain(compose(domain(X), compose(a, b))), domain(X)) -> domain(X) % 2.52/2.74 129: ifeq(codomain(b), domain(X), domain(compose(compose(a, b), domain(X))), domain(a)) -> domain(a) % 2.52/2.74 130: ifeq(codomain(g), domain(X), domain(compose(compose(a, g), domain(X))), domain(a)) -> domain(a) % 2.52/2.74 131: ifeq(codomain(X), domain(a), codomain(compose(codomain(X), compose(a, g))), codomain(g)) -> codomain(g) % 2.52/2.74 132: ifeq(codomain(X), domain(a), codomain(compose(codomain(X), compose(a, b))), codomain(b)) -> codomain(b) % 2.52/2.74 133: ifeq(codomain(b), codomain(X), domain(compose(compose(a, b), codomain(X))), domain(a)) -> domain(a) % 2.52/2.74 134: ifeq(domain(X), domain(a), codomain(compose(domain(X), compose(a, b))), codomain(b)) -> codomain(b) % 2.52/2.74 135: ifeq(codomain(b), domain(a), domain(compose(compose(a, b), compose(a, g))), domain(a)) -> domain(a) % 2.52/2.74 136: ifeq(codomain(g), domain(a), domain(compose(compose(a, g), compose(a, g))), domain(a)) -> domain(a) % 2.52/2.74 137: ifeq(codomain(g), domain(a), codomain(compose(compose(a, g), compose(a, b))), codomain(b)) -> codomain(b) % 2.52/2.74 138: ifeq(codomain(g), domain(a), domain(compose(compose(a, g), compose(a, b))), domain(a)) -> domain(a) % 2.52/2.74 139: ifeq(codomain(b), domain(a), codomain(compose(compose(a, b), compose(a, g))), codomain(g)) -> codomain(g) % 2.52/2.74 140: ifeq(codomain(b), domain(a), codomain(compose(compose(a, b), compose(a, b))), codomain(b)) -> codomain(b) % 2.52/2.74 141: ifeq(codomain(g), domain(a), codomain(compose(compose(a, g), compose(a, g))), codomain(g)) -> codomain(g) % 2.52/2.74 142: ifeq(codomain(b), domain(a), domain(compose(compose(a, b), compose(a, b))), domain(a)) -> domain(a) % 2.52/2.74 143: ifeq(codomain(X), domain(Y), ifeq(codomain(Z), domain(X), compose(Z, compose(X, Y)), compose(compose(Z, X), Y)), compose(compose(Z, X), Y)) -> compose(compose(Z, X), Y) % 2.52/2.74 144: ifeq(codomain(X), domain(Y), compose(X, compose(codomain(X), Y)), compose(X, Y)) -> compose(X, Y) % 2.52/2.74 145: ifeq(codomain(X), domain(Y), compose(domain(X), compose(X, Y)), compose(X, Y)) -> compose(X, Y) % 2.52/2.74 146: ifeq(codomain(X), domain(Y), compose(X, Y), compose(compose(X, domain(Y)), Y)) -> compose(compose(X, domain(Y)), Y) % 2.52/2.74 147: ifeq(codomain(X), domain(Y), compose(X, Y), compose(compose(X, Y), codomain(Y))) -> compose(compose(X, Y), codomain(Y)) % 2.52/2.74 148: ifeq(codomain(X), codomain(a), compose(X, compose(codomain(X), b)), compose(X, b)) -> compose(X, b) % 2.52/2.74 149: ifeq(codomain(X), codomain(a), compose(X, compose(codomain(X), h)), compose(X, h)) -> compose(X, h) % 2.52/2.74 150: ifeq(codomain(X), codomain(a), compose(X, compose(codomain(X), g)), compose(X, g)) -> compose(X, g) % 2.52/2.74 151: ifeq(codomain(X), codomain(a), compose(domain(X), compose(X, g)), compose(X, g)) -> compose(X, g) % 2.52/2.74 152: ifeq(codomain(X), codomain(a), compose(domain(X), compose(X, h)), compose(X, h)) -> compose(X, h) % 2.52/2.74 153: ifeq(codomain(X), codomain(a), compose(domain(X), compose(X, b)), compose(X, b)) -> compose(X, b) % 2.52/2.74 154: ifeq(codomain(g), domain(X), compose(codomain(a), compose(h, X)), compose(h, X)) -> compose(h, X) % 2.52/2.74 155: ifeq(codomain(g), domain(X), compose(codomain(a), compose(g, X)), compose(g, X)) -> compose(g, X) % 2.52/2.74 156: ifeq(codomain(b), domain(X), compose(codomain(a), compose(b, X)), compose(b, X)) -> compose(b, X) % 2.52/2.74 157: ifeq(codomain(g), domain(X), compose(h, compose(codomain(g), X)), compose(h, X)) -> compose(h, X) % 2.52/2.74 158: ifeq(codomain(g), domain(X), compose(h, X), compose(compose(h, domain(X)), X)) -> compose(compose(h, domain(X)), X) % 2.52/2.74 159: ifeq(codomain(g), domain(X), compose(h, X), compose(compose(h, X), codomain(X))) -> compose(compose(h, X), codomain(X)) % 2.52/2.74 160: ifeq(codomain(X), codomain(a), compose(X, b), compose(compose(X, b), codomain(b))) -> compose(compose(X, b), codomain(b)) % 2.52/2.74 161: ifeq(codomain(X), codomain(a), compose(X, h), compose(compose(X, h), codomain(g))) -> compose(compose(X, h), codomain(g)) % 2.52/2.74 162: ifeq(codomain(X), codomain(a), compose(X, g), compose(compose(X, g), codomain(g))) -> compose(compose(X, g), codomain(g)) % 2.52/2.74 163: ifeq(codomain(X), codomain(a), compose(X, b), compose(compose(X, codomain(a)), b)) -> compose(compose(X, codomain(a)), b) % 2.52/2.74 164: ifeq(codomain(X), codomain(a), compose(X, g), compose(compose(X, codomain(a)), g)) -> compose(compose(X, codomain(a)), g) % 2.52/2.74 165: ifeq(codomain(X), codomain(a), compose(X, h), compose(compose(X, codomain(a)), h)) -> compose(compose(X, codomain(a)), h) % 2.52/2.74 166: ifeq(codomain(g), domain(X), compose(a, compose(h, X)), compose(compose(a, g), X)) -> compose(compose(a, g), X) % 2.52/2.74 167: ifeq(codomain(X), domain(a), compose(X, compose(a, g)), compose(compose(X, a), h)) -> compose(compose(X, a), h) % 2.52/2.74 168: ifeq(codomain(g), codomain(a), compose(h, compose(codomain(g), b)), compose(h, b)) -> compose(h, b) % 2.52/2.74 169: ifeq(codomain(g), codomain(a), compose(h, compose(codomain(g), h)), compose(h, h)) -> compose(h, h) % 2.52/2.74 170: ifeq(codomain(g), codomain(a), compose(h, compose(codomain(g), g)), compose(h, g)) -> compose(h, g) % 2.52/2.74 171: ifeq(codomain(g), codomain(a), compose(codomain(a), compose(h, g)), compose(h, g)) -> compose(h, g) % 2.52/2.74 172: ifeq(codomain(b), codomain(a), compose(codomain(a), compose(b, g)), compose(b, g)) -> compose(b, g) % 2.52/2.74 173: ifeq(codomain(b), codomain(a), compose(codomain(a), compose(b, h)), compose(b, h)) -> compose(b, h) % 2.52/2.74 174: ifeq(codomain(g), codomain(a), compose(codomain(a), compose(h, h)), compose(h, h)) -> compose(h, h) % 2.52/2.74 175: ifeq(codomain(g), codomain(a), compose(codomain(a), compose(g, h)), compose(g, h)) -> compose(g, h) % 2.52/2.74 176: ifeq(codomain(g), codomain(a), compose(codomain(a), compose(g, g)), compose(g, g)) -> compose(g, g) % 2.52/2.74 177: ifeq(codomain(b), codomain(a), compose(codomain(a), compose(b, b)), compose(b, b)) -> compose(b, b) % 2.52/2.74 178: ifeq(codomain(g), codomain(a), compose(codomain(a), compose(h, b)), compose(h, b)) -> compose(h, b) % 2.52/2.74 179: ifeq(codomain(g), codomain(a), compose(codomain(a), compose(g, b)), compose(g, b)) -> compose(g, b) % 2.52/2.74 180: ifeq(domain(X), domain(Y), compose(domain(X), compose(domain(X), Y)), compose(domain(X), Y)) -> compose(domain(X), Y) % 2.52/2.74 181: ifeq(codomain(X), domain(Y), compose(codomain(X), compose(codomain(X), Y)), compose(codomain(X), Y)) -> compose(codomain(X), Y) % 2.52/2.74 182: ifeq(codomain(X), codomain(Y), compose(X, compose(codomain(X), codomain(Y))), compose(X, codomain(Y))) -> compose(X, codomain(Y)) % 2.52/2.74 183: ifeq(codomain(X), codomain(Y), compose(domain(X), compose(X, codomain(Y))), compose(X, codomain(Y))) -> compose(X, codomain(Y)) % 2.52/2.74 184: ifeq(codomain(X), domain(Y), compose(X, compose(codomain(X), domain(Y))), compose(X, domain(Y))) -> compose(X, domain(Y)) % 2.52/2.74 185: ifeq(codomain(X), domain(Y), compose(domain(X), compose(X, domain(Y))), compose(X, domain(Y))) -> compose(X, domain(Y)) % 2.52/2.74 186: ifeq(codomain(g), codomain(a), compose(h, h), compose(compose(h, h), codomain(g))) -> compose(compose(h, h), codomain(g)) % 2.52/2.74 187: ifeq(codomain(g), codomain(a), compose(h, h), compose(compose(h, codomain(a)), h)) -> compose(compose(h, codomain(a)), h) % 2.52/2.74 188: ifeq(codomain(g), codomain(a), compose(h, b), compose(compose(h, codomain(a)), b)) -> compose(compose(h, codomain(a)), b) % 2.52/2.74 189: ifeq(codomain(g), codomain(a), compose(h, g), compose(compose(h, codomain(a)), g)) -> compose(compose(h, codomain(a)), g) % 2.52/2.74 190: ifeq(codomain(g), codomain(a), compose(h, g), compose(compose(h, g), codomain(g))) -> compose(compose(h, g), codomain(g)) % 2.52/2.74 191: ifeq(codomain(g), codomain(a), compose(h, b), compose(compose(h, b), codomain(b))) -> compose(compose(h, b), codomain(b)) % 2.52/2.74 192: ifeq(codomain(g), domain(a), compose(h, compose(a, g)), compose(compose(h, a), h)) -> compose(compose(h, a), h) % 2.52/2.74 193: ifeq(codomain(g), codomain(a), compose(a, compose(h, b)), compose(compose(a, g), b)) -> compose(compose(a, g), b) % 2.52/2.74 194: ifeq(codomain(g), codomain(a), compose(a, compose(h, g)), compose(compose(a, g), g)) -> compose(compose(a, g), g) % 2.52/2.74 195: ifeq(codomain(g), codomain(a), compose(a, compose(h, h)), compose(compose(a, g), h)) -> compose(compose(a, g), h) % 2.52/2.74 196: ifeq(domain(X), domain(Y), compose(domain(X), Y), compose(compose(domain(X), Y), codomain(Y))) -> compose(compose(domain(X), Y), codomain(Y)) % 2.52/2.74 197: ifeq(codomain(X), codomain(Y), compose(X, codomain(Y)), compose(compose(X, codomain(Y)), codomain(Y))) -> compose(compose(X, codomain(Y)), codomain(Y)) % 2.52/2.74 198: ifeq(codomain(X), domain(Y), compose(codomain(X), Y), compose(compose(codomain(X), domain(Y)), Y)) -> compose(compose(codomain(X), domain(Y)), Y) % 2.52/2.74 199: ifeq(codomain(X), domain(Y), compose(X, domain(Y)), compose(compose(X, domain(Y)), domain(Y))) -> compose(compose(X, domain(Y)), domain(Y)) % 2.52/2.74 200: ifeq(codomain(X), domain(Y), compose(codomain(X), Y), compose(compose(codomain(X), Y), codomain(Y))) -> compose(compose(codomain(X), Y), codomain(Y)) % 2.52/2.74 201: ifeq(domain(X), domain(Y), compose(domain(X), Y), compose(compose(domain(X), domain(Y)), Y)) -> compose(compose(domain(X), domain(Y)), Y) % 2.52/2.74 202: ifeq(codomain(X), codomain(a), compose(codomain(X), compose(codomain(X), g)), compose(codomain(X), g)) -> compose(codomain(X), g) % 2.52/2.74 203: ifeq(domain(X), codomain(a), compose(domain(X), compose(domain(X), g)), compose(domain(X), g)) -> compose(domain(X), g) % 2.52/2.74 204: ifeq(codomain(X), codomain(a), compose(codomain(X), compose(codomain(X), h)), compose(codomain(X), h)) -> compose(codomain(X), h) % 2.52/2.74 205: ifeq(domain(X), codomain(a), compose(domain(X), compose(domain(X), h)), compose(domain(X), h)) -> compose(domain(X), h) % 2.52/2.74 206: ifeq(domain(X), codomain(a), compose(domain(X), compose(domain(X), b)), compose(domain(X), b)) -> compose(domain(X), b) % 2.52/2.74 207: ifeq(codomain(X), codomain(a), compose(codomain(X), compose(codomain(X), b)), compose(codomain(X), b)) -> compose(codomain(X), b) % 2.52/2.74 208: ifeq(codomain(g), codomain(X), compose(h, compose(codomain(g), codomain(X))), compose(h, codomain(X))) -> compose(h, codomain(X)) % 2.52/2.74 209: ifeq(codomain(g), domain(X), compose(codomain(a), compose(h, domain(X))), compose(h, domain(X))) -> compose(h, domain(X)) % 2.52/2.74 210: ifeq(codomain(g), domain(X), compose(h, compose(codomain(g), domain(X))), compose(h, domain(X))) -> compose(h, domain(X)) % 2.52/2.74 211: ifeq(codomain(b), domain(X), compose(codomain(a), compose(b, domain(X))), compose(b, domain(X))) -> compose(b, domain(X)) % 2.52/2.74 212: ifeq(codomain(g), domain(X), compose(codomain(a), compose(g, domain(X))), compose(g, domain(X))) -> compose(g, domain(X)) % 2.52/2.74 213: ifeq(codomain(g), codomain(X), compose(codomain(a), compose(g, codomain(X))), compose(g, codomain(X))) -> compose(g, codomain(X)) % 2.52/2.74 214: ifeq(codomain(b), codomain(X), compose(codomain(a), compose(b, codomain(X))), compose(b, codomain(X))) -> compose(b, codomain(X)) % 2.52/2.74 215: ifeq(codomain(g), codomain(X), compose(codomain(a), compose(h, codomain(X))), compose(h, codomain(X))) -> compose(h, codomain(X)) % 2.52/2.74 216: ifeq(codomain(g), domain(X), compose(h, domain(X)), compose(compose(h, domain(X)), domain(X))) -> compose(compose(h, domain(X)), domain(X)) % 2.52/2.74 217: ifeq(codomain(g), codomain(X), compose(h, codomain(X)), compose(compose(h, codomain(X)), codomain(X))) -> compose(compose(h, codomain(X)), codomain(X)) % 2.52/2.74 218: ifeq(domain(X), codomain(a), compose(domain(X), g), compose(compose(domain(X), codomain(a)), g)) -> compose(compose(domain(X), codomain(a)), g) % 2.52/2.74 219: ifeq(domain(X), codomain(a), compose(domain(X), b), compose(compose(domain(X), b), codomain(b))) -> compose(compose(domain(X), b), codomain(b)) % 2.52/2.74 220: ifeq(domain(X), codomain(a), compose(domain(X), g), compose(compose(domain(X), g), codomain(g))) -> compose(compose(domain(X), g), codomain(g)) % 2.52/2.74 221: ifeq(codomain(X), codomain(a), compose(codomain(X), b), compose(compose(codomain(X), codomain(a)), b)) -> compose(compose(codomain(X), codomain(a)), b) % 2.52/2.74 222: ifeq(codomain(X), codomain(a), compose(codomain(X), h), compose(compose(codomain(X), h), codomain(g))) -> compose(compose(codomain(X), h), codomain(g)) % 2.52/2.74 223: ifeq(domain(X), codomain(a), compose(domain(X), h), compose(compose(domain(X), codomain(a)), h)) -> compose(compose(domain(X), codomain(a)), h) % 2.52/2.74 224: ifeq(domain(X), codomain(a), compose(domain(X), b), compose(compose(domain(X), codomain(a)), b)) -> compose(compose(domain(X), codomain(a)), b) % 2.52/2.74 225: ifeq(codomain(X), codomain(a), compose(codomain(X), h), compose(compose(codomain(X), codomain(a)), h)) -> compose(compose(codomain(X), codomain(a)), h) % 2.52/2.74 226: ifeq(codomain(X), codomain(a), compose(codomain(X), g), compose(compose(codomain(X), codomain(a)), g)) -> compose(compose(codomain(X), codomain(a)), g) % 2.52/2.74 227: ifeq(codomain(X), codomain(a), compose(codomain(X), b), compose(compose(codomain(X), b), codomain(b))) -> compose(compose(codomain(X), b), codomain(b)) % 2.52/2.74 228: ifeq(domain(X), codomain(a), compose(domain(X), h), compose(compose(domain(X), h), codomain(g))) -> compose(compose(domain(X), h), codomain(g)) % 2.52/2.74 229: ifeq(codomain(X), codomain(a), compose(codomain(X), g), compose(compose(codomain(X), g), codomain(g))) -> compose(compose(codomain(X), g), codomain(g)) % 2.52/2.74 230: ifeq(codomain(g), codomain(X), compose(a, compose(h, codomain(X))), compose(compose(a, g), codomain(X))) -> compose(compose(a, g), codomain(X)) % 2.52/2.74 231: ifeq(codomain(g), domain(X), compose(a, compose(h, domain(X))), compose(compose(a, g), domain(X))) -> compose(compose(a, g), domain(X)) % 2.52/2.74 232: ifeq(domain(X), domain(a), compose(domain(X), compose(a, g)), compose(compose(domain(X), a), h)) -> compose(compose(domain(X), a), h) % 2.52/2.74 233: ifeq(codomain(X), domain(a), compose(codomain(X), compose(a, g)), compose(compose(codomain(X), a), h)) -> compose(compose(codomain(X), a), h) % 2.52/2.74 234: ifeq(codomain(X), domain(a), compose(X, compose(codomain(X), compose(a, g))), compose(X, compose(a, g))) -> compose(X, compose(a, g)) % 2.52/2.74 235: ifeq(codomain(X), domain(a), compose(domain(X), compose(X, compose(a, g))), compose(X, compose(a, g))) -> compose(X, compose(a, g)) % 2.52/2.74 236: ifeq(domain(X), codomain(Y), compose(domain(X), compose(domain(X), codomain(Y))), compose(domain(X), codomain(Y))) -> compose(domain(X), codomain(Y)) % 2.52/2.74 237: ifeq(domain(X), domain(Y), compose(domain(X), compose(domain(X), domain(Y))), compose(domain(X), domain(Y))) -> compose(domain(X), domain(Y)) % 2.52/2.74 238: ifeq(codomain(X), codomain(Y), compose(codomain(X), compose(codomain(X), codomain(Y))), compose(codomain(X), codomain(Y))) -> compose(codomain(X), codomain(Y)) % 2.52/2.74 239: ifeq(codomain(X), domain(Y), compose(codomain(X), compose(codomain(X), domain(Y))), compose(codomain(X), domain(Y))) -> compose(codomain(X), domain(Y)) % 2.52/2.74 240: ifeq(codomain(g), domain(X), compose(domain(a), compose(compose(a, g), X)), compose(compose(a, g), X)) -> compose(compose(a, g), X) % 2.52/2.74 241: ifeq(codomain(X), domain(a), compose(domain(X), compose(X, compose(a, b))), compose(X, compose(a, b))) -> compose(X, compose(a, b)) % 2.52/2.74 242: ifeq(codomain(X), domain(a), compose(X, compose(codomain(X), compose(a, b))), compose(X, compose(a, b))) -> compose(X, compose(a, b)) % 2.52/2.74 243: ifeq(codomain(g), domain(X), compose(compose(a, g), compose(codomain(g), X)), compose(compose(a, g), X)) -> compose(compose(a, g), X) % 2.52/2.74 244: ifeq(codomain(b), domain(X), compose(compose(a, b), compose(codomain(b), X)), compose(compose(a, b), X)) -> compose(compose(a, b), X) % 2.52/2.74 245: ifeq(codomain(b), domain(X), compose(domain(a), compose(compose(a, b), X)), compose(compose(a, b), X)) -> compose(compose(a, b), X) % 2.52/2.74 246: ifeq(codomain(X), domain(Y), compose(codomain(X), domain(Y)), compose(compose(codomain(X), domain(Y)), domain(Y))) -> compose(compose(codomain(X), domain(Y)), domain(Y)) % 2.52/2.74 247: ifeq(codomain(X), codomain(Y), compose(codomain(X), codomain(Y)), compose(compose(codomain(X), codomain(Y)), codomain(Y))) -> compose(compose(codomain(X), codomain(Y)), codomain(Y)) % 2.52/2.74 248: ifeq(domain(X), domain(Y), compose(domain(X), domain(Y)), compose(compose(domain(X), domain(Y)), domain(Y))) -> compose(compose(domain(X), domain(Y)), domain(Y)) % 2.52/2.74 249: ifeq(domain(X), codomain(Y), compose(domain(X), codomain(Y)), compose(compose(domain(X), codomain(Y)), codomain(Y))) -> compose(compose(domain(X), codomain(Y)), codomain(Y)) % 2.52/2.74 250: ifeq(codomain(X), domain(a), compose(X, compose(a, g)), compose(compose(X, compose(a, g)), codomain(g))) -> compose(compose(X, compose(a, g)), codomain(g)) % 2.52/2.74 251: ifeq(codomain(X), domain(a), compose(X, compose(a, g)), compose(compose(X, domain(a)), compose(a, g))) -> compose(compose(X, domain(a)), compose(a, g)) % 2.52/2.74 252: ifeq(codomain(g), codomain(a), compose(domain(a), compose(compose(a, g), h)), compose(compose(a, g), h)) -> compose(compose(a, g), h) % 2.52/2.74 253: ifeq(codomain(g), codomain(a), compose(domain(a), compose(compose(a, g), g)), compose(compose(a, g), g)) -> compose(compose(a, g), g) % 2.52/2.74 254: ifeq(codomain(b), codomain(a), compose(domain(a), compose(compose(a, b), h)), compose(compose(a, b), h)) -> compose(compose(a, b), h) % 2.52/2.74 255: ifeq(codomain(b), codomain(a), compose(domain(a), compose(compose(a, b), g)), compose(compose(a, b), g)) -> compose(compose(a, b), g) % 2.52/2.74 256: ifeq(codomain(g), domain(a), compose(codomain(a), compose(h, compose(a, g))), compose(h, compose(a, g))) -> compose(h, compose(a, g)) % 2.52/2.74 257: ifeq(codomain(g), domain(a), compose(codomain(a), compose(h, compose(a, b))), compose(h, compose(a, b))) -> compose(h, compose(a, b)) % 2.52/2.74 258: ifeq(codomain(g), domain(a), compose(codomain(a), compose(g, compose(a, g))), compose(g, compose(a, g))) -> compose(g, compose(a, g)) % 2.52/2.74 259: ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(codomain(b), h)), compose(compose(a, b), h)) -> compose(compose(a, b), h) % 2.52/2.74 260: ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(codomain(g), h)), compose(compose(a, g), h)) -> compose(compose(a, g), h) % 2.52/2.74 261: ifeq(codomain(b), domain(a), compose(codomain(a), compose(b, compose(a, g))), compose(b, compose(a, g))) -> compose(b, compose(a, g)) % 2.52/2.74 262: ifeq(codomain(g), domain(a), compose(h, compose(codomain(g), compose(a, g))), compose(h, compose(a, g))) -> compose(h, compose(a, g)) % 2.52/2.74 263: ifeq(codomain(b), codomain(a), compose(domain(a), compose(compose(a, b), b)), compose(compose(a, b), b)) -> compose(compose(a, b), b) % 2.52/2.74 264: ifeq(codomain(g), codomain(a), compose(domain(a), compose(compose(a, g), b)), compose(compose(a, g), b)) -> compose(compose(a, g), b) % 2.52/2.74 265: ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(codomain(g), b)), compose(compose(a, g), b)) -> compose(compose(a, g), b) % 2.52/2.74 266: ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(codomain(g), g)), compose(compose(a, g), g)) -> compose(compose(a, g), g) % 2.52/2.74 267: ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(codomain(b), b)), compose(compose(a, b), b)) -> compose(compose(a, b), b) % 2.52/2.74 268: ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(codomain(b), g)), compose(compose(a, b), g)) -> compose(compose(a, b), g) % 2.52/2.74 269: ifeq(codomain(b), domain(a), compose(codomain(a), compose(b, compose(a, b))), compose(b, compose(a, b))) -> compose(b, compose(a, b)) % 2.52/2.74 270: ifeq(codomain(g), domain(a), compose(codomain(a), compose(g, compose(a, b))), compose(g, compose(a, b))) -> compose(g, compose(a, b)) % 2.52/2.74 271: ifeq(codomain(g), domain(a), compose(h, compose(codomain(g), compose(a, b))), compose(h, compose(a, b))) -> compose(h, compose(a, b)) % 2.52/2.74 272: ifeq(codomain(g), domain(X), compose(compose(a, g), X), compose(compose(compose(a, g), domain(X)), X)) -> compose(compose(compose(a, g), domain(X)), X) % 2.52/2.74 273: ifeq(codomain(b), domain(X), compose(compose(a, b), X), compose(compose(compose(a, b), X), codomain(X))) -> compose(compose(compose(a, b), X), codomain(X)) % 2.52/2.74 274: ifeq(codomain(g), domain(X), compose(compose(a, g), X), compose(compose(compose(a, g), X), codomain(X))) -> compose(compose(compose(a, g), X), codomain(X)) % 2.52/2.74 275: ifeq(codomain(b), domain(X), compose(compose(a, b), X), compose(compose(compose(a, b), domain(X)), X)) -> compose(compose(compose(a, b), domain(X)), X) % 2.52/2.74 276: ifeq(codomain(X), domain(a), compose(X, compose(a, b)), compose(compose(X, compose(a, b)), codomain(b))) -> compose(compose(X, compose(a, b)), codomain(b)) % 2.52/2.74 277: ifeq(codomain(X), domain(a), compose(X, compose(a, b)), compose(compose(X, domain(a)), compose(a, b))) -> compose(compose(X, domain(a)), compose(a, b)) % 2.52/2.74 278: ifeq(codomain(g), domain(a), compose(h, compose(a, b)), compose(compose(h, compose(a, b)), codomain(b))) -> compose(compose(h, compose(a, b)), codomain(b)) % 2.52/2.74 279: ifeq(codomain(g), domain(a), compose(h, compose(a, g)), compose(compose(h, compose(a, g)), codomain(g))) -> compose(compose(h, compose(a, g)), codomain(g)) % 2.52/2.74 280: ifeq(codomain(g), codomain(a), compose(compose(a, g), b), compose(compose(compose(a, g), b), codomain(b))) -> compose(compose(compose(a, g), b), codomain(b)) % 2.52/2.74 281: ifeq(codomain(g), codomain(a), compose(compose(a, g), h), compose(compose(compose(a, g), h), codomain(g))) -> compose(compose(compose(a, g), h), codomain(g)) % 2.52/2.74 282: ifeq(codomain(b), codomain(a), compose(compose(a, b), b), compose(compose(compose(a, b), b), codomain(b))) -> compose(compose(compose(a, b), b), codomain(b)) % 2.52/2.74 283: ifeq(codomain(g), codomain(a), compose(compose(a, g), b), compose(compose(compose(a, g), codomain(a)), b)) -> compose(compose(compose(a, g), codomain(a)), b) % 2.52/2.74 284: ifeq(codomain(b), codomain(a), compose(compose(a, b), b), compose(compose(compose(a, b), codomain(a)), b)) -> compose(compose(compose(a, b), codomain(a)), b) % 2.52/2.74 285: ifeq(codomain(g), domain(a), compose(h, compose(a, b)), compose(compose(h, domain(a)), compose(a, b))) -> compose(compose(h, domain(a)), compose(a, b)) % 2.52/2.74 286: ifeq(codomain(g), domain(a), compose(h, compose(a, g)), compose(compose(h, domain(a)), compose(a, g))) -> compose(compose(h, domain(a)), compose(a, g)) % 2.52/2.74 287: ifeq(codomain(g), codomain(a), compose(compose(a, g), g), compose(compose(compose(a, g), codomain(a)), g)) -> compose(compose(compose(a, g), codomain(a)), g) % 2.52/2.74 288: ifeq(codomain(b), codomain(a), compose(compose(a, b), h), compose(compose(compose(a, b), codomain(a)), h)) -> compose(compose(compose(a, b), codomain(a)), h) % 2.52/2.74 289: ifeq(codomain(b), codomain(a), compose(compose(a, b), g), compose(compose(compose(a, b), g), codomain(g))) -> compose(compose(compose(a, b), g), codomain(g)) % 2.52/2.74 290: ifeq(codomain(g), codomain(a), compose(compose(a, g), g), compose(compose(compose(a, g), g), codomain(g))) -> compose(compose(compose(a, g), g), codomain(g)) % 2.52/2.74 291: ifeq(codomain(b), codomain(a), compose(compose(a, b), g), compose(compose(compose(a, b), codomain(a)), g)) -> compose(compose(compose(a, b), codomain(a)), g) % 2.52/2.74 292: ifeq(codomain(g), codomain(a), compose(compose(a, g), h), compose(compose(compose(a, g), codomain(a)), h)) -> compose(compose(compose(a, g), codomain(a)), h) % 2.52/2.74 293: ifeq(codomain(b), codomain(a), compose(compose(a, b), h), compose(compose(compose(a, b), h), codomain(g))) -> compose(compose(compose(a, b), h), codomain(g)) % 2.52/2.74 294: ifeq(codomain(g), domain(a), compose(a, compose(h, compose(a, g))), compose(compose(a, g), compose(a, g))) -> compose(compose(a, g), compose(a, g)) % 2.52/2.74 295: ifeq(codomain(g), domain(a), compose(compose(a, g), compose(a, g)), compose(compose(compose(a, g), a), h)) -> compose(compose(compose(a, g), a), h) % 2.52/2.74 296: ifeq(codomain(b), domain(a), compose(compose(a, b), compose(a, g)), compose(compose(compose(a, b), a), h)) -> compose(compose(compose(a, b), a), h) % 2.52/2.74 297: ifeq(codomain(g), domain(a), compose(a, compose(h, compose(a, b))), compose(compose(a, g), compose(a, b))) -> compose(compose(a, g), compose(a, b)) % 2.52/2.74 298: ifeq(domain(X), domain(a), compose(domain(X), compose(domain(X), compose(a, g))), compose(domain(X), compose(a, g))) -> compose(domain(X), compose(a, g)) % 2.52/2.74 299: ifeq(codomain(X), domain(a), compose(codomain(X), compose(codomain(X), compose(a, g))), compose(codomain(X), compose(a, g))) -> compose(codomain(X), compose(a, g)) % 2.52/2.74 300: ifeq(codomain(X), domain(a), compose(codomain(X), compose(codomain(X), compose(a, b))), compose(codomain(X), compose(a, b))) -> compose(codomain(X), compose(a, b)) % 2.52/2.74 301: ifeq(domain(X), domain(a), compose(domain(X), compose(domain(X), compose(a, b))), compose(domain(X), compose(a, b))) -> compose(domain(X), compose(a, b)) % 2.52/2.74 302: ifeq(codomain(g), codomain(X), compose(compose(a, g), compose(codomain(g), codomain(X))), compose(compose(a, g), codomain(X))) -> compose(compose(a, g), codomain(X)) % 2.52/2.74 303: ifeq(codomain(b), domain(X), compose(compose(a, b), compose(codomain(b), domain(X))), compose(compose(a, b), domain(X))) -> compose(compose(a, b), domain(X)) % 2.52/2.74 304: ifeq(codomain(b), codomain(X), compose(compose(a, b), compose(codomain(b), codomain(X))), compose(compose(a, b), codomain(X))) -> compose(compose(a, b), codomain(X)) % 2.52/2.74 305: ifeq(codomain(b), domain(X), compose(domain(a), compose(compose(a, b), domain(X))), compose(compose(a, b), domain(X))) -> compose(compose(a, b), domain(X)) % 2.52/2.74 306: ifeq(codomain(g), domain(X), compose(domain(a), compose(compose(a, g), domain(X))), compose(compose(a, g), domain(X))) -> compose(compose(a, g), domain(X)) % 2.52/2.74 307: ifeq(codomain(b), codomain(X), compose(domain(a), compose(compose(a, b), codomain(X))), compose(compose(a, b), codomain(X))) -> compose(compose(a, b), codomain(X)) % 2.52/2.74 308: ifeq(codomain(g), codomain(X), compose(domain(a), compose(compose(a, g), codomain(X))), compose(compose(a, g), codomain(X))) -> compose(compose(a, g), codomain(X)) % 2.52/2.74 309: ifeq(codomain(g), domain(X), compose(compose(a, g), compose(codomain(g), domain(X))), compose(compose(a, g), domain(X))) -> compose(compose(a, g), domain(X)) % 2.52/2.74 310: ifeq(codomain(g), codomain(X), compose(compose(a, g), codomain(X)), compose(compose(compose(a, g), codomain(X)), codomain(X))) -> compose(compose(compose(a, g), codomain(X)), codomain(X)) % 2.52/2.74 311: ifeq(codomain(b), codomain(X), compose(compose(a, b), codomain(X)), compose(compose(compose(a, b), codomain(X)), codomain(X))) -> compose(compose(compose(a, b), codomain(X)), codomain(X)) % 2.52/2.74 312: ifeq(codomain(b), domain(X), compose(compose(a, b), domain(X)), compose(compose(compose(a, b), domain(X)), domain(X))) -> compose(compose(compose(a, b), domain(X)), domain(X)) % 2.52/2.74 313: ifeq(codomain(g), domain(X), compose(compose(a, g), domain(X)), compose(compose(compose(a, g), domain(X)), domain(X))) -> compose(compose(compose(a, g), domain(X)), domain(X)) % 2.52/2.74 314: ifeq(codomain(X), domain(a), compose(codomain(X), compose(a, b)), compose(compose(codomain(X), compose(a, b)), codomain(b))) -> compose(compose(codomain(X), compose(a, b)), codomain(b)) % 2.52/2.74 315: ifeq(domain(X), domain(a), compose(domain(X), compose(a, g)), compose(compose(domain(X), compose(a, g)), codomain(g))) -> compose(compose(domain(X), compose(a, g)), codomain(g)) % 2.52/2.74 316: ifeq(domain(X), domain(a), compose(domain(X), compose(a, b)), compose(compose(domain(X), domain(a)), compose(a, b))) -> compose(compose(domain(X), domain(a)), compose(a, b)) % 2.52/2.74 317: ifeq(domain(X), domain(a), compose(domain(X), compose(a, g)), compose(compose(domain(X), domain(a)), compose(a, g))) -> compose(compose(domain(X), domain(a)), compose(a, g)) % 2.52/2.74 318: ifeq(codomain(X), domain(a), compose(codomain(X), compose(a, g)), compose(compose(codomain(X), compose(a, g)), codomain(g))) -> compose(compose(codomain(X), compose(a, g)), codomain(g)) % 2.52/2.74 319: ifeq(domain(X), domain(a), compose(domain(X), compose(a, b)), compose(compose(domain(X), compose(a, b)), codomain(b))) -> compose(compose(domain(X), compose(a, b)), codomain(b)) % 2.52/2.74 320: ifeq(codomain(X), domain(a), compose(codomain(X), compose(a, g)), compose(compose(codomain(X), domain(a)), compose(a, g))) -> compose(compose(codomain(X), domain(a)), compose(a, g)) % 2.52/2.74 321: ifeq(codomain(X), domain(a), compose(codomain(X), compose(a, b)), compose(compose(codomain(X), domain(a)), compose(a, b))) -> compose(compose(codomain(X), domain(a)), compose(a, b)) % 2.52/2.74 322: ifeq(codomain(X), codomain(compose(Y, X)), ifeq(codomain(Y), domain(X), compose(Y, compose(X, codomain(compose(Y, X)))), compose(Y, X)), compose(Y, X)) -> compose(Y, X) % 2.52/2.74 323: ifeq(codomain(X), codomain(a), ifeq(codomain(Y), domain(X), compose(Y, compose(X, g)), compose(compose(Y, X), g)), compose(compose(Y, X), g)) -> compose(compose(Y, X), g) % 2.52/2.74 324: ifeq(codomain(X), domain(a), compose(X, compose(a, g)), compose(compose(X, a), g)) -> compose(compose(X, a), g) % 2.52/2.74 325: ifeq(codomain(g), domain(a), compose(h, compose(a, g)), compose(compose(h, a), g)) -> compose(compose(h, a), g) % 2.52/2.74 326: ifeq(codomain(X), domain(a), compose(codomain(X), compose(a, g)), compose(compose(codomain(X), a), g)) -> compose(compose(codomain(X), a), g) % 2.52/2.74 327: ifeq(domain(X), domain(a), compose(domain(X), compose(a, g)), compose(compose(domain(X), a), g)) -> compose(compose(domain(X), a), g) % 2.52/2.74 328: ifeq(codomain(g), domain(a), compose(compose(a, g), compose(a, g)), compose(compose(compose(a, g), a), g)) -> compose(compose(compose(a, g), a), g) % 2.52/2.74 329: ifeq(codomain(b), domain(a), compose(compose(a, b), compose(a, g)), compose(compose(compose(a, b), a), g)) -> compose(compose(compose(a, b), a), g) % 2.52/2.74 330: ifeq(codomain(g), domain(a), compose(domain(a), compose(compose(a, g), compose(a, b))), compose(compose(a, g), compose(a, b))) -> compose(compose(a, g), compose(a, b)) % 2.52/2.74 331: ifeq(codomain(b), domain(a), compose(compose(a, b), compose(codomain(b), compose(a, g))), compose(compose(a, b), compose(a, g))) -> compose(compose(a, b), compose(a, g)) % 2.52/2.74 332: ifeq(codomain(b), domain(a), compose(domain(a), compose(compose(a, b), compose(a, g))), compose(compose(a, b), compose(a, g))) -> compose(compose(a, b), compose(a, g)) % 2.52/2.74 333: ifeq(codomain(g), domain(a), compose(domain(a), compose(compose(a, g), compose(a, g))), compose(compose(a, g), compose(a, g))) -> compose(compose(a, g), compose(a, g)) % 2.52/2.74 334: ifeq(codomain(X), codomain(a), ifeq(codomain(Y), domain(X), compose(Y, compose(X, h)), compose(compose(Y, X), h)), compose(compose(Y, X), h)) -> compose(compose(Y, X), h) % 2.52/2.74 335: ifeq(codomain(X), codomain(a), ifeq(codomain(Y), domain(X), compose(Y, compose(X, b)), compose(compose(Y, X), b)), compose(compose(Y, X), b)) -> compose(compose(Y, X), b) % 2.52/2.74 336: ifeq(codomain(X), domain(a), compose(X, compose(a, b)), compose(compose(X, a), b)) -> compose(compose(X, a), b) % 2.52/2.74 337: ifeq(codomain(g), domain(a), compose(h, compose(a, b)), compose(compose(h, a), b)) -> compose(compose(h, a), b) % 2.52/2.74 338: ifeq(codomain(X), domain(a), compose(codomain(X), compose(a, b)), compose(compose(codomain(X), a), b)) -> compose(compose(codomain(X), a), b) % 2.52/2.74 339: ifeq(domain(X), domain(a), compose(domain(X), compose(a, b)), compose(compose(domain(X), a), b)) -> compose(compose(domain(X), a), b) % 2.52/2.74 340: ifeq(codomain(g), domain(a), compose(compose(a, g), compose(a, b)), compose(compose(compose(a, g), a), b)) -> compose(compose(compose(a, g), a), b) % 2.52/2.74 341: ifeq(codomain(b), domain(a), compose(compose(a, b), compose(a, b)), compose(compose(compose(a, b), a), b)) -> compose(compose(compose(a, b), a), b) % 2.52/2.74 342: ifeq(codomain(g), domain(a), compose(compose(a, g), compose(codomain(g), compose(a, g))), compose(compose(a, g), compose(a, g))) -> compose(compose(a, g), compose(a, g)) % 2.52/2.74 343: ifeq(codomain(g), domain(X), ifeq(codomain(Y), codomain(a), compose(Y, compose(h, X)), compose(compose(Y, h), X)), compose(compose(Y, h), X)) -> compose(compose(Y, h), X) % 2.52/2.74 344: ifeq(codomain(g), domain(X), ifeq(codomain(Y), codomain(a), compose(Y, compose(g, X)), compose(compose(Y, g), X)), compose(compose(Y, g), X)) -> compose(compose(Y, g), X) % 2.52/2.74 345: ifeq(codomain(g), domain(X), compose(a, compose(g, X)), compose(compose(a, g), X)) -> compose(compose(a, g), X) % 2.52/2.74 346: ifeq(codomain(g), codomain(a), compose(a, compose(g, b)), compose(compose(a, g), b)) -> compose(compose(a, g), b) % 2.52/2.74 347: ifeq(codomain(g), codomain(a), compose(a, compose(g, g)), compose(compose(a, g), g)) -> compose(compose(a, g), g) % 2.52/2.74 348: ifeq(codomain(g), codomain(a), compose(a, compose(g, h)), compose(compose(a, g), h)) -> compose(compose(a, g), h) % 2.52/2.74 349: ifeq(codomain(g), domain(X), compose(a, compose(g, domain(X))), compose(compose(a, g), domain(X))) -> compose(compose(a, g), domain(X)) % 2.52/2.74 350: ifeq(codomain(g), codomain(X), compose(a, compose(g, codomain(X))), compose(compose(a, g), codomain(X))) -> compose(compose(a, g), codomain(X)) % 2.52/2.74 351: ifeq(codomain(g), domain(a), compose(a, compose(g, compose(a, b))), compose(compose(a, g), compose(a, b))) -> compose(compose(a, g), compose(a, b)) % 2.52/2.74 352: ifeq(codomain(g), domain(a), compose(a, compose(g, compose(a, g))), compose(compose(a, g), compose(a, g))) -> compose(compose(a, g), compose(a, g)) % 2.52/2.74 353: ifeq(codomain(b), domain(X), ifeq(codomain(Y), codomain(a), compose(Y, compose(b, X)), compose(compose(Y, b), X)), compose(compose(Y, b), X)) -> compose(compose(Y, b), X) % 2.52/2.74 354: ifeq(codomain(b), domain(X), compose(a, compose(b, X)), compose(compose(a, b), X)) -> compose(compose(a, b), X) % 2.52/2.74 355: ifeq(codomain(b), codomain(a), compose(a, compose(b, b)), compose(compose(a, b), b)) -> compose(compose(a, b), b) % 2.52/2.74 356: ifeq(codomain(b), codomain(a), compose(a, compose(b, g)), compose(compose(a, b), g)) -> compose(compose(a, b), g) % 2.52/2.74 357: ifeq(codomain(b), codomain(a), compose(a, compose(b, h)), compose(compose(a, b), h)) -> compose(compose(a, b), h) % 2.52/2.74 358: ifeq(codomain(b), domain(X), compose(a, compose(b, domain(X))), compose(compose(a, b), domain(X))) -> compose(compose(a, b), domain(X)) % 2.52/2.74 359: ifeq(codomain(b), codomain(X), compose(a, compose(b, codomain(X))), compose(compose(a, b), codomain(X))) -> compose(compose(a, b), codomain(X)) % 2.52/2.74 360: ifeq(codomain(b), domain(a), compose(a, compose(b, compose(a, b))), compose(compose(a, b), compose(a, b))) -> compose(compose(a, b), compose(a, b)) % 2.52/2.74 361: ifeq(codomain(b), domain(a), compose(a, compose(b, compose(a, g))), compose(compose(a, b), compose(a, g))) -> compose(compose(a, b), compose(a, g)) % 2.52/2.74 362: ifeq(codomain(X), domain(Y), ifeq(codomain(g), domain(X), compose(h, compose(X, Y)), compose(compose(h, X), Y)), compose(compose(h, X), Y)) -> compose(compose(h, X), Y) % 2.52/2.74 363: ifeq(codomain(b), domain(a), compose(domain(a), compose(compose(a, b), compose(a, b))), compose(compose(a, b), compose(a, b))) -> compose(compose(a, b), compose(a, b)) % 2.52/2.74 364: ifeq(codomain(g), domain(a), compose(compose(a, g), compose(codomain(g), compose(a, b))), compose(compose(a, g), compose(a, b))) -> compose(compose(a, g), compose(a, b)) % 2.52/2.74 365: ifeq(codomain(b), domain(a), compose(compose(a, b), compose(codomain(b), compose(a, b))), compose(compose(a, b), compose(a, b))) -> compose(compose(a, b), compose(a, b)) % 2.52/2.74 366: ifeq(codomain(g), domain(a), compose(compose(a, g), compose(a, g)), compose(compose(compose(a, g), compose(a, g)), codomain(g))) -> compose(compose(compose(a, g), compose(a, g)), codomain(g)) % 2.52/2.74 367: ifeq(codomain(b), domain(a), compose(compose(a, b), compose(a, g)), compose(compose(compose(a, b), compose(a, g)), codomain(g))) -> compose(compose(compose(a, b), compose(a, g)), codomain(g)) % 2.52/2.74 368: ifeq(codomain(g), domain(a), compose(compose(a, g), compose(a, g)), compose(compose(compose(a, g), domain(a)), compose(a, g))) -> compose(compose(compose(a, g), domain(a)), compose(a, g)) % 2.52/2.74 369: ifeq(codomain(b), domain(a), compose(compose(a, b), compose(a, g)), compose(compose(compose(a, b), domain(a)), compose(a, g))) -> compose(compose(compose(a, b), domain(a)), compose(a, g)) % 2.52/2.74 370: ifeq(codomain(X), codomain(a), ifeq(codomain(g), domain(X), compose(h, compose(X, g)), compose(compose(h, X), g)), compose(compose(h, X), g)) -> compose(compose(h, X), g) % 2.52/2.74 371: ifeq(codomain(X), codomain(a), ifeq(codomain(g), domain(X), compose(h, compose(X, h)), compose(compose(h, X), h)), compose(compose(h, X), h)) -> compose(compose(h, X), h) % 2.52/2.74 372: ifeq(codomain(X), codomain(a), ifeq(codomain(g), domain(X), compose(h, compose(X, b)), compose(compose(h, X), b)), compose(compose(h, X), b)) -> compose(compose(h, X), b) % 2.52/2.74 373: ifeq(codomain(b), codomain(a), ifeq(codomain(X), codomain(a), compose(X, compose(b, b)), compose(compose(X, b), b)), compose(compose(X, b), b)) -> compose(compose(X, b), b) % 2.52/2.74 374: ifeq(codomain(g), codomain(a), ifeq(codomain(X), codomain(a), compose(X, compose(h, b)), compose(compose(X, h), b)), compose(compose(X, h), b)) -> compose(compose(X, h), b) % 2.52/2.74 375: ifeq(codomain(b), domain(a), compose(compose(a, b), compose(a, b)), compose(compose(compose(a, b), compose(a, b)), codomain(b))) -> compose(compose(compose(a, b), compose(a, b)), codomain(b)) % 2.52/2.74 376: ifeq(codomain(g), codomain(a), ifeq(codomain(X), codomain(a), compose(X, compose(g, b)), compose(compose(X, g), b)), compose(compose(X, g), b)) -> compose(compose(X, g), b) % 2.52/2.74 377: ifeq(codomain(g), codomain(a), ifeq(codomain(X), codomain(a), compose(X, compose(h, h)), compose(compose(X, h), h)), compose(compose(X, h), h)) -> compose(compose(X, h), h) % 2.52/2.74 378: ifeq(codomain(g), codomain(a), ifeq(codomain(X), codomain(a), compose(X, compose(g, h)), compose(compose(X, g), h)), compose(compose(X, g), h)) -> compose(compose(X, g), h) % 2.52/2.74 379: ifeq(codomain(b), codomain(a), ifeq(codomain(X), codomain(a), compose(X, compose(b, h)), compose(compose(X, b), h)), compose(compose(X, b), h)) -> compose(compose(X, b), h) % 2.52/2.74 380: ifeq(codomain(b), codomain(a), ifeq(codomain(X), codomain(a), compose(X, compose(b, g)), compose(compose(X, b), g)), compose(compose(X, b), g)) -> compose(compose(X, b), g) % 2.52/2.74 381: ifeq(codomain(g), codomain(a), ifeq(codomain(X), codomain(a), compose(X, compose(h, g)), compose(compose(X, h), g)), compose(compose(X, h), g)) -> compose(compose(X, h), g) % 2.52/2.74 382: ifeq(codomain(g), codomain(a), ifeq(codomain(X), codomain(a), compose(X, compose(g, g)), compose(compose(X, g), g)), compose(compose(X, g), g)) -> compose(compose(X, g), g) % 2.52/2.74 383: ifeq(codomain(g), domain(a), compose(compose(a, g), compose(a, b)), compose(compose(compose(a, g), compose(a, b)), codomain(b))) -> compose(compose(compose(a, g), compose(a, b)), codomain(b)) % 2.52/2.74 384: ifeq(codomain(b), domain(a), compose(compose(a, b), compose(a, b)), compose(compose(compose(a, b), domain(a)), compose(a, b))) -> compose(compose(compose(a, b), domain(a)), compose(a, b)) % 2.52/2.74 385: ifeq(codomain(g), domain(a), compose(compose(a, g), compose(a, b)), compose(compose(compose(a, g), domain(a)), compose(a, b))) -> compose(compose(compose(a, g), domain(a)), compose(a, b)) % 2.52/2.74 386: ifeq(codomain(b), domain(X), ifeq(codomain(g), codomain(a), compose(h, compose(b, X)), compose(compose(h, b), X)), compose(compose(h, b), X)) -> compose(compose(h, b), X) % 2.52/2.74 387: ifeq(codomain(g), domain(X), ifeq(codomain(g), codomain(a), compose(h, compose(g, X)), compose(compose(h, g), X)), compose(compose(h, g), X)) -> compose(compose(h, g), X) % 2.52/2.74 388: ifeq(codomain(g), domain(X), ifeq(codomain(g), codomain(a), compose(h, compose(h, X)), compose(compose(h, h), X)), compose(compose(h, h), X)) -> compose(compose(h, h), X) % 2.52/2.74 389: ifeq(codomain(X), codomain(compose(h, X)), ifeq(codomain(g), domain(X), compose(h, compose(X, codomain(compose(h, X)))), compose(h, X)), compose(h, X)) -> compose(h, X) % 2.52/2.74 390: ifeq(codomain(g), codomain(compose(X, h)), ifeq(codomain(X), codomain(a), compose(X, compose(h, codomain(compose(X, h)))), compose(X, h)), compose(X, h)) -> compose(X, h) % 2.52/2.74 391: ifeq(codomain(g), codomain(compose(X, g)), ifeq(codomain(X), codomain(a), compose(X, compose(g, codomain(compose(X, g)))), compose(X, g)), compose(X, g)) -> compose(X, g) % 2.52/2.74 392: ifeq(codomain(b), codomain(compose(X, b)), ifeq(codomain(X), codomain(a), compose(X, compose(b, codomain(compose(X, b)))), compose(X, b)), compose(X, b)) -> compose(X, b) % 2.52/2.74 393: ifeq(codomain(g), codomain(a), ifeq(codomain(g), codomain(a), compose(h, compose(g, g)), compose(compose(h, g), g)), compose(compose(h, g), g)) -> compose(compose(h, g), g) % 2.52/2.74 394: ifeq(codomain(b), codomain(a), ifeq(codomain(g), codomain(a), compose(h, compose(b, h)), compose(compose(h, b), h)), compose(compose(h, b), h)) -> compose(compose(h, b), h) % 2.52/2.74 395: ifeq(codomain(b), codomain(a), ifeq(codomain(g), codomain(a), compose(h, compose(b, g)), compose(compose(h, b), g)), compose(compose(h, b), g)) -> compose(compose(h, b), g) % 2.52/2.74 396: ifeq(codomain(g), codomain(a), ifeq(codomain(g), codomain(a), compose(h, compose(g, h)), compose(compose(h, g), h)), compose(compose(h, g), h)) -> compose(compose(h, g), h) % 2.52/2.74 397: ifeq(codomain(g), codomain(a), ifeq(codomain(g), codomain(a), compose(h, compose(h, h)), compose(compose(h, h), h)), compose(compose(h, h), h)) -> compose(compose(h, h), h) % 2.52/2.74 398: ifeq(codomain(g), codomain(a), ifeq(codomain(g), codomain(a), compose(h, compose(h, b)), compose(compose(h, h), b)), compose(compose(h, h), b)) -> compose(compose(h, h), b) % 2.52/2.74 399: ifeq(codomain(g), codomain(a), ifeq(codomain(g), codomain(a), compose(h, compose(h, g)), compose(compose(h, h), g)), compose(compose(h, h), g)) -> compose(compose(h, h), g) % 2.52/2.74 400: ifeq(codomain(b), codomain(a), ifeq(codomain(g), codomain(a), compose(h, compose(b, b)), compose(compose(h, b), b)), compose(compose(h, b), b)) -> compose(compose(h, b), b) % 2.52/2.74 401: ifeq(codomain(g), codomain(a), ifeq(codomain(g), codomain(a), compose(h, compose(g, b)), compose(compose(h, g), b)), compose(compose(h, g), b)) -> compose(compose(h, g), b) % 2.52/2.74 402: ifeq(codomain(X), codomain(Y), ifeq(codomain(Z), domain(X), compose(Z, compose(X, codomain(Y))), compose(compose(Z, X), codomain(Y))), compose(compose(Z, X), codomain(Y))) -> compose(compose(Z, X), codomain(Y)) % 2.52/2.74 403: ifeq(domain(X), domain(Y), ifeq(codomain(Z), domain(X), compose(Z, compose(domain(X), Y)), compose(compose(Z, domain(X)), Y)), compose(compose(Z, domain(X)), Y)) -> compose(compose(Z, domain(X)), Y) % 2.52/2.74 404: ifeq(codomain(X), domain(Y), ifeq(codomain(Z), codomain(X), compose(Z, compose(codomain(X), Y)), compose(compose(Z, codomain(X)), Y)), compose(compose(Z, codomain(X)), Y)) -> compose(compose(Z, codomain(X)), Y) % 2.52/2.74 405: ifeq(codomain(X), domain(Y), ifeq(domain(Z), domain(X), compose(domain(Z), compose(X, Y)), compose(compose(domain(Z), X), Y)), compose(compose(domain(Z), X), Y)) -> compose(compose(domain(Z), X), Y) % 2.52/2.74 406: ifeq(codomain(g), codomain(compose(h, g)), ifeq(codomain(g), codomain(a), compose(h, compose(g, codomain(compose(h, g)))), compose(h, g)), compose(h, g)) -> compose(h, g) % 2.52/2.74 407: ifeq(codomain(b), codomain(compose(h, b)), ifeq(codomain(g), codomain(a), compose(h, compose(b, codomain(compose(h, b)))), compose(h, b)), compose(h, b)) -> compose(h, b) % 2.52/2.74 408: ifeq(codomain(g), codomain(compose(h, h)), ifeq(codomain(g), codomain(a), compose(h, compose(h, codomain(compose(h, h)))), compose(h, h)), compose(h, h)) -> compose(h, h) % 2.52/2.74 409: ifeq(codomain(X), domain(Y), ifeq(codomain(Z), domain(X), compose(Z, compose(X, domain(Y))), compose(compose(Z, X), domain(Y))), compose(compose(Z, X), domain(Y))) -> compose(compose(Z, X), domain(Y)) % 2.52/2.74 410: ifeq(codomain(X), domain(Y), ifeq(codomain(Z), domain(X), compose(codomain(Z), compose(X, Y)), compose(compose(codomain(Z), X), Y)), compose(compose(codomain(Z), X), Y)) -> compose(compose(codomain(Z), X), Y) % 2.52/2.74 411: ifeq(domain(X), codomain(a), ifeq(codomain(Y), domain(X), compose(Y, compose(domain(X), h)), compose(compose(Y, domain(X)), h)), compose(compose(Y, domain(X)), h)) -> compose(compose(Y, domain(X)), h) % 2.52/2.74 412: ifeq(domain(X), codomain(a), ifeq(codomain(Y), domain(X), compose(Y, compose(domain(X), g)), compose(compose(Y, domain(X)), g)), compose(compose(Y, domain(X)), g)) -> compose(compose(Y, domain(X)), g) % 2.52/2.74 413: ifeq(domain(X), codomain(a), ifeq(codomain(Y), domain(X), compose(Y, compose(domain(X), b)), compose(compose(Y, domain(X)), b)), compose(compose(Y, domain(X)), b)) -> compose(compose(Y, domain(X)), b) % 2.52/2.74 414: ifeq(domain(X), domain(Y), ifeq(codomain(g), domain(X), compose(h, compose(domain(X), Y)), compose(compose(h, domain(X)), Y)), compose(compose(h, domain(X)), Y)) -> compose(compose(h, domain(X)), Y) % 2.52/2.74 415: ifeq(codomain(X), codomain(a), ifeq(codomain(Y), codomain(X), compose(Y, compose(codomain(X), g)), compose(compose(Y, codomain(X)), g)), compose(compose(Y, codomain(X)), g)) -> compose(compose(Y, codomain(X)), g) % 2.52/2.74 416: ifeq(codomain(X), codomain(a), ifeq(codomain(Y), codomain(X), compose(Y, compose(codomain(X), b)), compose(compose(Y, codomain(X)), b)), compose(compose(Y, codomain(X)), b)) -> compose(compose(Y, codomain(X)), b) % 2.52/2.74 417: ifeq(codomain(X), codomain(a), ifeq(domain(Y), domain(X), compose(domain(Y), compose(X, b)), compose(compose(domain(Y), X), b)), compose(compose(domain(Y), X), b)) -> compose(compose(domain(Y), X), b) % 2.52/2.74 418: ifeq(codomain(X), codomain(a), ifeq(codomain(Y), codomain(X), compose(Y, compose(codomain(X), h)), compose(compose(Y, codomain(X)), h)), compose(compose(Y, codomain(X)), h)) -> compose(compose(Y, codomain(X)), h) % 2.52/2.74 419: ifeq(codomain(X), domain(Y), ifeq(codomain(g), codomain(X), compose(h, compose(codomain(X), Y)), compose(compose(h, codomain(X)), Y)), compose(compose(h, codomain(X)), Y)) -> compose(compose(h, codomain(X)), Y) % 2.52/2.74 420: ifeq(codomain(X), codomain(a), ifeq(domain(Y), domain(X), compose(domain(Y), compose(X, h)), compose(compose(domain(Y), X), h)), compose(compose(domain(Y), X), h)) -> compose(compose(domain(Y), X), h) % 2.52/2.74 421: ifeq(codomain(X), codomain(a), ifeq(domain(Y), domain(X), compose(domain(Y), compose(X, g)), compose(compose(domain(Y), X), g)), compose(compose(domain(Y), X), g)) -> compose(compose(domain(Y), X), g) % 2.52/2.74 422: ifeq(codomain(X), codomain(a), ifeq(codomain(Y), domain(X), compose(codomain(Y), compose(X, b)), compose(compose(codomain(Y), X), b)), compose(compose(codomain(Y), X), b)) -> compose(compose(codomain(Y), X), b) % 2.52/2.74 423: ifeq(codomain(X), codomain(a), ifeq(codomain(Y), domain(X), compose(codomain(Y), compose(X, g)), compose(compose(codomain(Y), X), g)), compose(compose(codomain(Y), X), g)) -> compose(compose(codomain(Y), X), g) % 2.52/2.74 424: ifeq(codomain(X), codomain(a), ifeq(codomain(Y), domain(X), compose(codomain(Y), compose(X, h)), compose(compose(codomain(Y), X), h)), compose(compose(codomain(Y), X), h)) -> compose(compose(codomain(Y), X), h) % 2.52/2.74 425: ifeq(codomain(X), codomain(Y), ifeq(codomain(g), domain(X), compose(h, compose(X, codomain(Y))), compose(compose(h, X), codomain(Y))), compose(compose(h, X), codomain(Y))) -> compose(compose(h, X), codomain(Y)) % 2.52/2.74 426: ifeq(codomain(b), codomain(X), ifeq(codomain(Y), codomain(a), compose(Y, compose(b, codomain(X))), compose(compose(Y, b), codomain(X))), compose(compose(Y, b), codomain(X))) -> compose(compose(Y, b), codomain(X)) % 2.52/2.74 427: ifeq(codomain(g), codomain(X), ifeq(codomain(Y), codomain(a), compose(Y, compose(h, codomain(X))), compose(compose(Y, h), codomain(X))), compose(compose(Y, h), codomain(X))) -> compose(compose(Y, h), codomain(X)) % 2.52/2.74 428: ifeq(codomain(b), domain(X), ifeq(domain(Y), codomain(a), compose(domain(Y), compose(b, X)), compose(compose(domain(Y), b), X)), compose(compose(domain(Y), b), X)) -> compose(compose(domain(Y), b), X) % 2.52/2.74 429: ifeq(codomain(b), domain(X), ifeq(codomain(Y), codomain(a), compose(codomain(Y), compose(b, X)), compose(compose(codomain(Y), b), X)), compose(compose(codomain(Y), b), X)) -> compose(compose(codomain(Y), b), X) % 2.52/2.74 430: ifeq(codomain(g), domain(X), ifeq(codomain(Y), codomain(a), compose(Y, compose(g, domain(X))), compose(compose(Y, g), domain(X))), compose(compose(Y, g), domain(X))) -> compose(compose(Y, g), domain(X)) % 2.52/2.74 431: ifeq(codomain(g), domain(X), ifeq(domain(Y), codomain(a), compose(domain(Y), compose(g, X)), compose(compose(domain(Y), g), X)), compose(compose(domain(Y), g), X)) -> compose(compose(domain(Y), g), X) % 2.52/2.74 432: ifeq(codomain(g), domain(X), ifeq(codomain(Y), codomain(a), compose(codomain(Y), compose(g, X)), compose(compose(codomain(Y), g), X)), compose(compose(codomain(Y), g), X)) -> compose(compose(codomain(Y), g), X) % 2.52/2.74 433: ifeq(codomain(g), domain(X), ifeq(codomain(Y), codomain(a), compose(Y, compose(h, domain(X))), compose(compose(Y, h), domain(X))), compose(compose(Y, h), domain(X))) -> compose(compose(Y, h), domain(X)) % 2.52/2.74 434: ifeq(codomain(g), codomain(X), ifeq(codomain(Y), codomain(a), compose(Y, compose(g, codomain(X))), compose(compose(Y, g), codomain(X))), compose(compose(Y, g), codomain(X))) -> compose(compose(Y, g), codomain(X)) % 2.52/2.74 435: ifeq(codomain(g), domain(X), ifeq(domain(Y), codomain(a), compose(domain(Y), compose(h, X)), compose(compose(domain(Y), h), X)), compose(compose(domain(Y), h), X)) -> compose(compose(domain(Y), h), X) % 2.52/2.74 436: ifeq(codomain(b), domain(X), ifeq(codomain(Y), codomain(a), compose(Y, compose(b, domain(X))), compose(compose(Y, b), domain(X))), compose(compose(Y, b), domain(X))) -> compose(compose(Y, b), domain(X)) % 2.52/2.74 437: ifeq(codomain(g), domain(X), ifeq(codomain(Y), codomain(a), compose(codomain(Y), compose(h, X)), compose(compose(codomain(Y), h), X)), compose(compose(codomain(Y), h), X)) -> compose(compose(codomain(Y), h), X) % 2.52/2.74 438: ifeq(codomain(X), domain(Y), ifeq(codomain(g), domain(X), compose(h, compose(X, domain(Y))), compose(compose(h, X), domain(Y))), compose(compose(h, X), domain(Y))) -> compose(compose(h, X), domain(Y)) % 2.52/2.74 439: ifeq(domain(X), codomain(a), ifeq(codomain(g), domain(X), compose(h, compose(domain(X), h)), compose(compose(h, domain(X)), h)), compose(compose(h, domain(X)), h)) -> compose(compose(h, domain(X)), h) % 2.52/2.74 440: ifeq(codomain(X), codomain(a), ifeq(codomain(g), codomain(X), compose(h, compose(codomain(X), g)), compose(compose(h, codomain(X)), g)), compose(compose(h, codomain(X)), g)) -> compose(compose(h, codomain(X)), g) % 2.52/2.74 441: ifeq(codomain(X), codomain(a), ifeq(codomain(g), codomain(X), compose(h, compose(codomain(X), b)), compose(compose(h, codomain(X)), b)), compose(compose(h, codomain(X)), b)) -> compose(compose(h, codomain(X)), b) % 2.52/2.74 442: ifeq(codomain(X), codomain(a), ifeq(codomain(g), codomain(X), compose(h, compose(codomain(X), h)), compose(compose(h, codomain(X)), h)), compose(compose(h, codomain(X)), h)) -> compose(compose(h, codomain(X)), h) % 2.52/2.74 443: ifeq(domain(X), codomain(a), ifeq(codomain(g), domain(X), compose(h, compose(domain(X), b)), compose(compose(h, domain(X)), b)), compose(compose(h, domain(X)), b)) -> compose(compose(h, domain(X)), b) % 2.52/2.74 444: ifeq(domain(X), codomain(a), ifeq(codomain(g), domain(X), compose(h, compose(domain(X), g)), compose(compose(h, domain(X)), g)), compose(compose(h, domain(X)), g)) -> compose(compose(h, domain(X)), g) % 2.52/2.74 445: ifeq(codomain(b), domain(X), ifeq(codomain(g), codomain(a), compose(h, compose(b, domain(X))), compose(compose(h, b), domain(X))), compose(compose(h, b), domain(X))) -> compose(compose(h, b), domain(X)) % 2.52/2.74 446: ifeq(codomain(g), codomain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(h, g)), compose(compose(domain(X), h), g)), compose(compose(domain(X), h), g)) -> compose(compose(domain(X), h), g) % 2.52/2.74 447: ifeq(codomain(g), codomain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(h, g)), compose(compose(codomain(X), h), g)), compose(compose(codomain(X), h), g)) -> compose(compose(codomain(X), h), g) % 2.52/2.74 448: ifeq(codomain(g), codomain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(h, h)), compose(compose(codomain(X), h), h)), compose(compose(codomain(X), h), h)) -> compose(compose(codomain(X), h), h) % 2.52/2.74 449: ifeq(codomain(g), codomain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(h, b)), compose(compose(codomain(X), h), b)), compose(compose(codomain(X), h), b)) -> compose(compose(codomain(X), h), b) % 2.52/2.74 450: ifeq(codomain(b), codomain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(b, g)), compose(compose(codomain(X), b), g)), compose(compose(codomain(X), b), g)) -> compose(compose(codomain(X), b), g) % 2.52/2.74 451: ifeq(codomain(g), codomain(X), ifeq(codomain(g), codomain(a), compose(h, compose(g, codomain(X))), compose(compose(h, g), codomain(X))), compose(compose(h, g), codomain(X))) -> compose(compose(h, g), codomain(X)) % 2.52/2.74 452: ifeq(codomain(g), codomain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(g, b)), compose(compose(domain(X), g), b)), compose(compose(domain(X), g), b)) -> compose(compose(domain(X), g), b) % 2.52/2.74 453: ifeq(codomain(g), codomain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(g, b)), compose(compose(codomain(X), g), b)), compose(compose(codomain(X), g), b)) -> compose(compose(codomain(X), g), b) % 2.52/2.74 454: ifeq(codomain(g), codomain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(h, b)), compose(compose(domain(X), h), b)), compose(compose(domain(X), h), b)) -> compose(compose(domain(X), h), b) % 2.52/2.74 455: ifeq(codomain(b), codomain(X), ifeq(codomain(g), codomain(a), compose(h, compose(b, codomain(X))), compose(compose(h, b), codomain(X))), compose(compose(h, b), codomain(X))) -> compose(compose(h, b), codomain(X)) % 2.52/2.74 456: ifeq(codomain(g), codomain(X), ifeq(codomain(g), codomain(a), compose(h, compose(h, codomain(X))), compose(compose(h, h), codomain(X))), compose(compose(h, h), codomain(X))) -> compose(compose(h, h), codomain(X)) % 2.52/2.74 457: ifeq(codomain(b), codomain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(b, b)), compose(compose(domain(X), b), b)), compose(compose(domain(X), b), b)) -> compose(compose(domain(X), b), b) % 2.52/2.74 458: ifeq(codomain(g), codomain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(h, h)), compose(compose(domain(X), h), h)), compose(compose(domain(X), h), h)) -> compose(compose(domain(X), h), h) % 2.52/2.74 459: ifeq(codomain(b), codomain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(b, b)), compose(compose(codomain(X), b), b)), compose(compose(codomain(X), b), b)) -> compose(compose(codomain(X), b), b) % 2.52/2.74 460: ifeq(codomain(b), codomain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(b, g)), compose(compose(domain(X), b), g)), compose(compose(domain(X), b), g)) -> compose(compose(domain(X), b), g) % 2.52/2.74 461: ifeq(codomain(b), codomain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(b, h)), compose(compose(codomain(X), b), h)), compose(compose(codomain(X), b), h)) -> compose(compose(codomain(X), b), h) % 2.52/2.74 462: ifeq(codomain(g), codomain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(g, h)), compose(compose(codomain(X), g), h)), compose(compose(codomain(X), g), h)) -> compose(compose(codomain(X), g), h) % 2.52/2.74 463: ifeq(codomain(g), codomain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(g, g)), compose(compose(codomain(X), g), g)), compose(compose(codomain(X), g), g)) -> compose(compose(codomain(X), g), g) % 2.52/2.74 464: ifeq(codomain(g), codomain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(g, h)), compose(compose(domain(X), g), h)), compose(compose(domain(X), g), h)) -> compose(compose(domain(X), g), h) % 2.52/2.74 465: ifeq(codomain(g), codomain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(g, g)), compose(compose(domain(X), g), g)), compose(compose(domain(X), g), g)) -> compose(compose(domain(X), g), g) % 2.52/2.74 466: ifeq(codomain(b), codomain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(b, h)), compose(compose(domain(X), b), h)), compose(compose(domain(X), b), h)) -> compose(compose(domain(X), b), h) % 2.52/2.74 467: ifeq(codomain(g), domain(X), ifeq(codomain(g), codomain(a), compose(h, compose(g, domain(X))), compose(compose(h, g), domain(X))), compose(compose(h, g), domain(X))) -> compose(compose(h, g), domain(X)) % 2.52/2.74 468: ifeq(codomain(g), domain(X), ifeq(codomain(g), codomain(a), compose(h, compose(h, domain(X))), compose(compose(h, h), domain(X))), compose(compose(h, h), domain(X))) -> compose(compose(h, h), domain(X)) % 2.52/2.74 469: ifeq(codomain(X), codomain(compose(domain(Y), X)), ifeq(domain(Y), domain(X), compose(domain(Y), compose(X, codomain(compose(domain(Y), X)))), compose(domain(Y), X)), compose(domain(Y), X)) -> compose(domain(Y), X) % 2.52/2.74 470: ifeq(domain(X), codomain(compose(Y, domain(X))), ifeq(codomain(Y), domain(X), compose(Y, compose(domain(X), codomain(compose(Y, domain(X))))), compose(Y, domain(X))), compose(Y, domain(X))) -> compose(Y, domain(X)) % 2.52/2.74 471: ifeq(codomain(X), codomain(compose(Y, codomain(X))), ifeq(codomain(Y), codomain(X), compose(Y, compose(codomain(X), codomain(compose(Y, codomain(X))))), compose(Y, codomain(X))), compose(Y, codomain(X))) -> compose(Y, codomain(X)) % 2.52/2.74 472: ifeq(codomain(X), codomain(compose(codomain(Y), X)), ifeq(codomain(Y), domain(X), compose(codomain(Y), compose(X, codomain(compose(codomain(Y), X)))), compose(codomain(Y), X)), compose(codomain(Y), X)) -> compose(codomain(Y), X) % 2.52/2.74 473: ifeq(codomain(X), domain(Y), ifeq(domain(compose(X, Y)), domain(X), compose(X, Y), compose(compose(domain(compose(X, Y)), X), Y)), compose(compose(domain(compose(X, Y)), X), Y)) -> compose(compose(domain(compose(X, Y)), X), Y) % 2.52/2.74 475: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(X, compose(a, b)), Z, ifeq(compose(Y, compose(a, b)), Z, Y, X), X), X), X) -> X % 2.52/2.74 476: ifeq(codomain(X), domain(a), ifeq(compose(X, compose(a, b)), Y, ifeq(compose(a, b), Y, domain(a), X), X), X) -> X % 2.52/2.74 477: ifeq(compose(a, b), X, ifeq(compose(a, b), X, domain(a), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 478: ifeq(codomain(X), domain(a), ifeq(compose(a, b), compose(X, compose(a, b)), domain(a), X), X) -> X % 2.52/2.74 479: ifeq(codomain(X), domain(a), ifeq(compose(X, compose(a, b)), compose(a, b), domain(a), X), X) -> X % 2.52/2.74 480: ifeq(codomain(g), domain(a), ifeq(compose(h, compose(a, b)), compose(a, b), domain(a), h), h) -> h % 2.52/2.74 481: ifeq(codomain(g), domain(a), ifeq(compose(a, b), compose(h, compose(a, b)), domain(a), h), h) -> h % 2.52/2.74 482: ifeq(domain(X), domain(a), ifeq(compose(domain(X), compose(a, b)), compose(a, b), domain(a), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 483: ifeq(codomain(X), domain(a), ifeq(compose(codomain(X), compose(a, b)), compose(a, b), domain(a), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 484: ifeq(domain(X), domain(a), ifeq(compose(a, b), compose(domain(X), compose(a, b)), domain(a), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 485: ifeq(codomain(X), domain(a), ifeq(compose(a, b), compose(codomain(X), compose(a, b)), domain(a), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 486: ifeq(codomain(g), domain(a), ifeq(compose(h, compose(a, b)), X, ifeq(compose(a, b), X, domain(a), h), h), h) -> h % 2.52/2.74 487: ifeq(codomain(X), domain(a), ifeq(compose(a, b), Y, ifeq(compose(X, compose(a, b)), Y, X, domain(a)), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 488: ifeq(codomain(X), domain(a), ifeq(compose(X, compose(a, b)), compose(a, b), X, domain(a)), domain(a)) -> domain(a) % 2.52/2.74 489: ifeq(codomain(X), domain(a), ifeq(compose(a, b), compose(X, compose(a, b)), X, domain(a)), domain(a)) -> domain(a) % 2.52/2.74 490: ifeq(codomain(g), domain(a), ifeq(compose(a, b), compose(h, compose(a, b)), h, domain(a)), domain(a)) -> domain(a) % 2.52/2.74 491: ifeq(codomain(g), domain(a), ifeq(compose(h, compose(a, b)), compose(a, b), h, domain(a)), domain(a)) -> domain(a) % 2.52/2.74 492: ifeq(domain(X), domain(a), ifeq(compose(a, b), compose(domain(X), compose(a, b)), domain(X), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 493: ifeq(codomain(X), domain(a), ifeq(compose(a, b), compose(codomain(X), compose(a, b)), codomain(X), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 494: ifeq(domain(X), domain(a), ifeq(compose(domain(X), compose(a, b)), compose(a, b), domain(X), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 495: ifeq(codomain(X), domain(a), ifeq(compose(codomain(X), compose(a, b)), compose(a, b), codomain(X), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 496: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(Y, compose(a, b)), compose(X, compose(a, b)), Y, X), X), X) -> X % 2.52/2.74 497: ifeq(codomain(X), domain(a), ifeq(codomain(X), domain(a), X, X), X) -> X % 2.52/2.74 498: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), h, h), h) -> h % 2.52/2.74 499: ifeq(domain(X), domain(a), ifeq(domain(X), domain(a), domain(X), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 500: ifeq(codomain(X), domain(a), ifeq(codomain(X), domain(a), codomain(X), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 501: ifeq(codomain(b), domain(a), ifeq(codomain(b), domain(a), compose(a, b), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 502: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), compose(a, g), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 503: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(X, compose(a, b)), compose(Y, compose(a, b)), Y, X), X), X) -> X % 2.52/2.74 504: ifeq(codomain(b), domain(a), ifeq(compose(compose(a, b), compose(a, b)), compose(a, b), compose(a, b), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 505: ifeq(codomain(g), domain(a), ifeq(compose(compose(a, g), compose(a, b)), compose(a, b), compose(a, g), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 506: ifeq(codomain(b), domain(a), ifeq(compose(a, b), compose(compose(a, b), compose(a, b)), compose(a, b), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 507: ifeq(codomain(g), domain(a), ifeq(compose(a, b), compose(compose(a, g), compose(a, b)), compose(a, g), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 508: ifeq(codomain(g), domain(a), ifeq(compose(a, b), X, ifeq(compose(h, compose(a, b)), X, h, domain(a)), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 509: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(h, compose(a, b)), compose(X, compose(a, b)), h, X), X), X) -> X % 2.52/2.74 510: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(X, compose(a, b)), compose(h, compose(a, b)), h, X), X), X) -> X % 2.52/2.74 511: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(h, compose(a, b)), compose(X, compose(a, b)), X, h), h), h) -> h % 2.52/2.74 512: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(X, compose(a, b)), compose(h, compose(a, b)), X, h), h), h) -> h % 2.52/2.74 513: ifeq(codomain(b), domain(a), ifeq(compose(compose(a, b), compose(a, b)), compose(a, b), domain(a), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 514: ifeq(codomain(g), domain(a), ifeq(compose(compose(a, g), compose(a, b)), compose(a, b), domain(a), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 515: ifeq(codomain(b), domain(a), ifeq(compose(a, b), compose(compose(a, b), compose(a, b)), domain(a), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 516: ifeq(codomain(g), domain(a), ifeq(compose(a, b), compose(compose(a, g), compose(a, b)), domain(a), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 517: ifeq(codomain(X), domain(a), ifeq(compose(codomain(X), compose(a, b)), Y, ifeq(compose(a, b), Y, domain(a), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 518: ifeq(domain(X), domain(a), ifeq(compose(domain(X), compose(a, b)), Y, ifeq(compose(a, b), Y, domain(a), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 519: ifeq(domain(X), domain(a), ifeq(compose(a, b), Y, ifeq(compose(domain(X), compose(a, b)), Y, domain(X), domain(a)), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 520: ifeq(codomain(X), domain(a), ifeq(compose(a, b), Y, ifeq(compose(codomain(X), compose(a, b)), Y, codomain(X), domain(a)), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 521: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(X, compose(a, b)), compose(codomain(Y), compose(a, b)), codomain(Y), X), X), X) -> X % 2.52/2.74 522: ifeq(codomain(X), domain(a), ifeq(domain(Y), domain(a), ifeq(compose(domain(Y), compose(a, b)), compose(X, compose(a, b)), domain(Y), X), X), X) -> X % 2.52/2.74 523: ifeq(codomain(X), domain(a), ifeq(domain(Y), domain(a), ifeq(compose(X, compose(a, b)), compose(domain(Y), compose(a, b)), domain(Y), X), X), X) -> X % 2.52/2.74 524: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(codomain(Y), compose(a, b)), compose(X, compose(a, b)), codomain(Y), X), X), X) -> X % 2.52/2.74 525: ifeq(codomain(g), domain(a), ifeq(domain(X), domain(a), ifeq(compose(domain(X), compose(a, b)), compose(h, compose(a, b)), domain(X), h), h), h) -> h % 2.52/2.74 526: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(codomain(X), compose(a, b)), compose(h, compose(a, b)), codomain(X), h), h), h) -> h % 2.52/2.74 527: ifeq(codomain(g), domain(a), ifeq(domain(X), domain(a), ifeq(compose(h, compose(a, b)), compose(domain(X), compose(a, b)), domain(X), h), h), h) -> h % 2.52/2.74 528: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(h, compose(a, b)), compose(codomain(X), compose(a, b)), codomain(X), h), h), h) -> h % 2.52/2.74 529: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(X, compose(a, b)), Y, ifeq(compose(h, compose(a, b)), Y, h, X), X), X), X) -> X % 2.52/2.74 530: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(codomain(X), compose(a, b)), compose(Y, compose(a, b)), Y, codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 531: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(Y, compose(a, b)), compose(codomain(X), compose(a, b)), Y, codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 532: ifeq(domain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(domain(X), compose(a, b)), compose(Y, compose(a, b)), Y, domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 533: ifeq(domain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(Y, compose(a, b)), compose(domain(X), compose(a, b)), Y, domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 534: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(h, compose(a, b)), Y, ifeq(compose(X, compose(a, b)), Y, X, h), h), h), h) -> h % 2.52/2.74 535: ifeq(codomain(g), domain(a), ifeq(compose(a, b), X, ifeq(compose(compose(a, g), compose(a, b)), X, compose(a, g), domain(a)), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 536: ifeq(codomain(b), domain(a), ifeq(compose(a, b), X, ifeq(compose(compose(a, b), compose(a, b)), X, compose(a, b), domain(a)), domain(a)), domain(a)) -> domain(a) % 2.52/2.74 537: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(compose(a, g), compose(a, b)), compose(X, compose(a, b)), compose(a, g), X), X), X) -> X % 2.52/2.74 538: ifeq(codomain(X), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(compose(a, b), compose(a, b)), compose(X, compose(a, b)), compose(a, b), X), X), X) -> X % 2.52/2.74 539: ifeq(codomain(X), domain(a), ifeq(domain(Y), domain(a), ifeq(compose(X, compose(a, b)), Z, ifeq(compose(domain(Y), compose(a, b)), Z, domain(Y), X), X), X), X) -> X % 2.52/2.74 540: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(X, compose(a, b)), compose(compose(a, g), compose(a, b)), compose(a, g), X), X), X) -> X % 2.52/2.74 541: ifeq(codomain(X), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(X, compose(a, b)), compose(compose(a, b), compose(a, b)), compose(a, b), X), X), X) -> X % 2.52/2.74 542: ifeq(domain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(domain(X), compose(a, b)), compose(h, compose(a, b)), h, domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 543: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(codomain(X), compose(a, b)), compose(h, compose(a, b)), h, codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 544: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(h, compose(a, b)), compose(codomain(X), compose(a, b)), h, codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 545: ifeq(domain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(h, compose(a, b)), compose(domain(X), compose(a, b)), h, domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 546: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(h, compose(a, b)), X, ifeq(compose(h, compose(a, b)), X, h, h), h), h), h) -> h % 2.52/2.74 547: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(X, compose(a, b)), Z, ifeq(compose(codomain(Y), compose(a, b)), Z, codomain(Y), X), X), X), X) -> X % 2.52/2.74 548: ifeq(codomain(g), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(h, compose(a, b)), compose(compose(a, b), compose(a, b)), compose(a, b), h), h), h) -> h % 2.52/2.74 549: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(h, compose(a, b)), compose(compose(a, g), compose(a, b)), compose(a, g), h), h), h) -> h % 2.52/2.74 550: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(compose(a, g), compose(a, b)), compose(h, compose(a, b)), compose(a, g), h), h), h) -> h % 2.52/2.74 551: ifeq(codomain(g), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(compose(a, b), compose(a, b)), compose(h, compose(a, b)), compose(a, b), h), h), h) -> h % 2.52/2.74 552: ifeq(codomain(g), domain(a), ifeq(domain(X), domain(a), ifeq(compose(h, compose(a, b)), Y, ifeq(compose(domain(X), compose(a, b)), Y, domain(X), h), h), h), h) -> h % 2.52/2.74 553: ifeq(codomain(X), codomain(Y), ifeq(codomain(Z), codomain(X), compose(Z, compose(codomain(X), codomain(Y))), compose(compose(Z, codomain(X)), codomain(Y))), compose(compose(Z, codomain(X)), codomain(Y))) -> compose(compose(Z, codomain(X)), codomain(Y)) % 2.52/2.74 554: ifeq(domain(X), domain(Y), ifeq(domain(Z), domain(X), compose(domain(Z), compose(domain(X), Y)), compose(compose(domain(Z), domain(X)), Y)), compose(compose(domain(Z), domain(X)), Y)) -> compose(compose(domain(Z), domain(X)), Y) % 2.52/2.74 555: ifeq(codomain(X), domain(Y), ifeq(codomain(Z), codomain(X), compose(Z, compose(codomain(X), domain(Y))), compose(compose(Z, codomain(X)), domain(Y))), compose(compose(Z, codomain(X)), domain(Y))) -> compose(compose(Z, codomain(X)), domain(Y)) % 2.52/2.74 556: ifeq(domain(X), domain(Y), ifeq(codomain(Z), domain(X), compose(Z, compose(domain(X), domain(Y))), compose(compose(Z, domain(X)), domain(Y))), compose(compose(Z, domain(X)), domain(Y))) -> compose(compose(Z, domain(X)), domain(Y)) % 2.52/2.74 557: ifeq(domain(X), codomain(Y), ifeq(codomain(Z), domain(X), compose(Z, compose(domain(X), codomain(Y))), compose(compose(Z, domain(X)), codomain(Y))), compose(compose(Z, domain(X)), codomain(Y))) -> compose(compose(Z, domain(X)), codomain(Y)) % 2.52/2.74 558: ifeq(domain(X), domain(Y), ifeq(codomain(Z), domain(X), compose(codomain(Z), compose(domain(X), Y)), compose(compose(codomain(Z), domain(X)), Y)), compose(compose(codomain(Z), domain(X)), Y)) -> compose(compose(codomain(Z), domain(X)), Y) % 2.52/2.74 559: ifeq(codomain(X), domain(Y), ifeq(domain(Z), codomain(X), compose(domain(Z), compose(codomain(X), Y)), compose(compose(domain(Z), codomain(X)), Y)), compose(compose(domain(Z), codomain(X)), Y)) -> compose(compose(domain(Z), codomain(X)), Y) % 2.52/2.74 560: ifeq(codomain(X), codomain(Y), ifeq(codomain(Z), domain(X), compose(codomain(Z), compose(X, codomain(Y))), compose(compose(codomain(Z), X), codomain(Y))), compose(compose(codomain(Z), X), codomain(Y))) -> compose(compose(codomain(Z), X), codomain(Y)) % 2.52/2.74 561: ifeq(codomain(X), domain(Y), ifeq(codomain(Z), codomain(X), compose(codomain(Z), compose(codomain(X), Y)), compose(compose(codomain(Z), codomain(X)), Y)), compose(compose(codomain(Z), codomain(X)), Y)) -> compose(compose(codomain(Z), codomain(X)), Y) % 2.52/2.74 562: ifeq(codomain(X), domain(Y), ifeq(domain(Z), domain(X), compose(domain(Z), compose(X, domain(Y))), compose(compose(domain(Z), X), domain(Y))), compose(compose(domain(Z), X), domain(Y))) -> compose(compose(domain(Z), X), domain(Y)) % 2.52/2.74 563: ifeq(codomain(X), codomain(Y), ifeq(domain(Z), domain(X), compose(domain(Z), compose(X, codomain(Y))), compose(compose(domain(Z), X), codomain(Y))), compose(compose(domain(Z), X), codomain(Y))) -> compose(compose(domain(Z), X), codomain(Y)) % 2.52/2.74 564: ifeq(codomain(X), domain(a), ifeq(domain(Y), domain(a), ifeq(compose(domain(Y), compose(a, b)), compose(codomain(X), compose(a, b)), domain(Y), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 565: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(codomain(Y), compose(a, b)), compose(codomain(X), compose(a, b)), codomain(Y), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 566: ifeq(domain(X), domain(a), ifeq(domain(Y), domain(a), ifeq(compose(domain(X), compose(a, b)), compose(domain(Y), compose(a, b)), domain(Y), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 567: ifeq(codomain(X), domain(a), ifeq(domain(Y), domain(a), ifeq(compose(codomain(X), compose(a, b)), compose(domain(Y), compose(a, b)), domain(Y), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 568: ifeq(domain(X), domain(a), ifeq(domain(Y), domain(a), ifeq(compose(domain(Y), compose(a, b)), compose(domain(X), compose(a, b)), domain(Y), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 569: ifeq(domain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(codomain(Y), compose(a, b)), compose(domain(X), compose(a, b)), codomain(Y), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 570: ifeq(domain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(domain(X), compose(a, b)), compose(codomain(Y), compose(a, b)), codomain(Y), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 571: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(codomain(X), compose(a, b)), compose(codomain(Y), compose(a, b)), codomain(Y), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 572: ifeq(codomain(g), domain(a), ifeq(compose(compose(a, g), compose(a, b)), X, ifeq(compose(a, b), X, domain(a), compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 573: ifeq(codomain(b), domain(a), ifeq(compose(compose(a, b), compose(a, b)), X, ifeq(compose(a, b), X, domain(a), compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 574: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(h, compose(a, b)), Y, ifeq(compose(codomain(X), compose(a, b)), Y, codomain(X), h), h), h), h) -> h % 2.52/2.74 575: ifeq(codomain(X), domain(Y), ifeq(codomain(Z), domain(X), compose(codomain(Z), compose(X, domain(Y))), compose(compose(codomain(Z), X), domain(Y))), compose(compose(codomain(Z), X), domain(Y))) -> compose(compose(codomain(Z), X), domain(Y)) % 2.52/2.74 576: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(X), compose(Y, compose(X, compose(a, g))), compose(compose(Y, X), compose(a, g))), compose(compose(Y, X), compose(a, g))) -> compose(compose(Y, X), compose(a, g)) % 2.52/2.74 577: ifeq(domain(X), codomain(compose(h, domain(X))), ifeq(codomain(g), domain(X), compose(h, compose(domain(X), codomain(compose(h, domain(X))))), compose(h, domain(X))), compose(h, domain(X))) -> compose(h, domain(X)) % 2.52/2.74 578: ifeq(codomain(g), domain(X), ifeq(codomain(Y), domain(a), compose(Y, compose(compose(a, g), X)), compose(compose(Y, compose(a, g)), X)), compose(compose(Y, compose(a, g)), X)) -> compose(compose(Y, compose(a, g)), X) % 2.52/2.74 579: ifeq(codomain(X), codomain(compose(h, codomain(X))), ifeq(codomain(g), codomain(X), compose(h, compose(codomain(X), codomain(compose(h, codomain(X))))), compose(h, codomain(X))), compose(h, codomain(X))) -> compose(h, codomain(X)) % 2.52/2.74 580: ifeq(codomain(g), codomain(compose(codomain(X), g)), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(g, codomain(compose(codomain(X), g)))), compose(codomain(X), g)), compose(codomain(X), g)) -> compose(codomain(X), g) % 2.52/2.74 581: ifeq(codomain(g), codomain(compose(domain(X), h)), ifeq(domain(X), codomain(a), compose(domain(X), compose(h, codomain(compose(domain(X), h)))), compose(domain(X), h)), compose(domain(X), h)) -> compose(domain(X), h) % 2.52/2.74 582: ifeq(codomain(g), codomain(compose(domain(X), g)), ifeq(domain(X), codomain(a), compose(domain(X), compose(g, codomain(compose(domain(X), g)))), compose(domain(X), g)), compose(domain(X), g)) -> compose(domain(X), g) % 2.52/2.74 583: ifeq(codomain(b), codomain(compose(domain(X), b)), ifeq(domain(X), codomain(a), compose(domain(X), compose(b, codomain(compose(domain(X), b)))), compose(domain(X), b)), compose(domain(X), b)) -> compose(domain(X), b) % 2.52/2.74 584: ifeq(codomain(g), codomain(compose(codomain(X), h)), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(h, codomain(compose(codomain(X), h)))), compose(codomain(X), h)), compose(codomain(X), h)) -> compose(codomain(X), h) % 2.52/2.74 585: ifeq(codomain(b), codomain(compose(codomain(X), b)), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(b, codomain(compose(codomain(X), b)))), compose(codomain(X), b)), compose(codomain(X), b)) -> compose(codomain(X), b) % 2.52/2.74 586: ifeq(codomain(X), codomain(a), ifeq(domain(compose(X, h)), domain(X), compose(X, h), compose(compose(domain(compose(X, h)), X), h)), compose(compose(domain(compose(X, h)), X), h)) -> compose(compose(domain(compose(X, h)), X), h) % 2.52/2.74 587: ifeq(codomain(X), codomain(a), ifeq(domain(compose(X, g)), domain(X), compose(X, g), compose(compose(domain(compose(X, g)), X), g)), compose(compose(domain(compose(X, g)), X), g)) -> compose(compose(domain(compose(X, g)), X), g) % 2.52/2.74 588: ifeq(codomain(X), codomain(a), ifeq(domain(compose(X, b)), domain(X), compose(X, b), compose(compose(domain(compose(X, b)), X), b)), compose(compose(domain(compose(X, b)), X), b)) -> compose(compose(domain(compose(X, b)), X), b) % 2.52/2.74 589: ifeq(codomain(b), domain(X), ifeq(domain(compose(b, X)), codomain(a), compose(b, X), compose(compose(domain(compose(b, X)), b), X)), compose(compose(domain(compose(b, X)), b), X)) -> compose(compose(domain(compose(b, X)), b), X) % 2.52/2.74 590: ifeq(codomain(g), domain(X), ifeq(domain(compose(g, X)), codomain(a), compose(g, X), compose(compose(domain(compose(g, X)), g), X)), compose(compose(domain(compose(g, X)), g), X)) -> compose(compose(domain(compose(g, X)), g), X) % 2.52/2.74 591: ifeq(codomain(g), domain(X), ifeq(domain(compose(h, X)), codomain(a), compose(h, X), compose(compose(domain(compose(h, X)), h), X)), compose(compose(domain(compose(h, X)), h), X)) -> compose(compose(domain(compose(h, X)), h), X) % 2.52/2.74 592: ifeq(codomain(X), codomain(a), ifeq(domain(Y), codomain(X), compose(domain(Y), compose(codomain(X), b)), compose(compose(domain(Y), codomain(X)), b)), compose(compose(domain(Y), codomain(X)), b)) -> compose(compose(domain(Y), codomain(X)), b) % 2.52/2.74 593: ifeq(codomain(X), codomain(a), ifeq(domain(Y), codomain(X), compose(domain(Y), compose(codomain(X), h)), compose(compose(domain(Y), codomain(X)), h)), compose(compose(domain(Y), codomain(X)), h)) -> compose(compose(domain(Y), codomain(X)), h) % 2.52/2.74 594: ifeq(domain(X), domain(Y), ifeq(codomain(g), domain(X), compose(h, compose(domain(X), domain(Y))), compose(compose(h, domain(X)), domain(Y))), compose(compose(h, domain(X)), domain(Y))) -> compose(compose(h, domain(X)), domain(Y)) % 2.52/2.74 595: ifeq(domain(X), codomain(a), ifeq(codomain(Y), domain(X), compose(codomain(Y), compose(domain(X), h)), compose(compose(codomain(Y), domain(X)), h)), compose(compose(codomain(Y), domain(X)), h)) -> compose(compose(codomain(Y), domain(X)), h) % 2.52/2.74 596: ifeq(codomain(X), codomain(a), ifeq(codomain(Y), codomain(X), compose(codomain(Y), compose(codomain(X), h)), compose(compose(codomain(Y), codomain(X)), h)), compose(compose(codomain(Y), codomain(X)), h)) -> compose(compose(codomain(Y), codomain(X)), h) % 2.52/2.74 597: ifeq(domain(X), codomain(Y), ifeq(codomain(g), domain(X), compose(h, compose(domain(X), codomain(Y))), compose(compose(h, domain(X)), codomain(Y))), compose(compose(h, domain(X)), codomain(Y))) -> compose(compose(h, domain(X)), codomain(Y)) % 2.52/2.74 598: ifeq(codomain(X), codomain(Y), ifeq(codomain(g), codomain(X), compose(h, compose(codomain(X), codomain(Y))), compose(compose(h, codomain(X)), codomain(Y))), compose(compose(h, codomain(X)), codomain(Y))) -> compose(compose(h, codomain(X)), codomain(Y)) % 2.52/2.74 599: ifeq(domain(X), codomain(a), ifeq(domain(Y), domain(X), compose(domain(Y), compose(domain(X), b)), compose(compose(domain(Y), domain(X)), b)), compose(compose(domain(Y), domain(X)), b)) -> compose(compose(domain(Y), domain(X)), b) % 2.52/2.74 600: ifeq(domain(X), codomain(a), ifeq(codomain(Y), domain(X), compose(codomain(Y), compose(domain(X), g)), compose(compose(codomain(Y), domain(X)), g)), compose(compose(codomain(Y), domain(X)), g)) -> compose(compose(codomain(Y), domain(X)), g) % 2.52/2.74 601: ifeq(codomain(X), codomain(a), ifeq(codomain(Y), codomain(X), compose(codomain(Y), compose(codomain(X), g)), compose(compose(codomain(Y), codomain(X)), g)), compose(compose(codomain(Y), codomain(X)), g)) -> compose(compose(codomain(Y), codomain(X)), g) % 2.52/2.74 602: ifeq(codomain(X), domain(Y), ifeq(codomain(g), codomain(X), compose(h, compose(codomain(X), domain(Y))), compose(compose(h, codomain(X)), domain(Y))), compose(compose(h, codomain(X)), domain(Y))) -> compose(compose(h, codomain(X)), domain(Y)) % 2.52/2.74 603: ifeq(domain(X), codomain(a), ifeq(domain(Y), domain(X), compose(domain(Y), compose(domain(X), g)), compose(compose(domain(Y), domain(X)), g)), compose(compose(domain(Y), domain(X)), g)) -> compose(compose(domain(Y), domain(X)), g) % 2.52/2.74 604: ifeq(domain(X), codomain(a), ifeq(domain(Y), domain(X), compose(domain(Y), compose(domain(X), h)), compose(compose(domain(Y), domain(X)), h)), compose(compose(domain(Y), domain(X)), h)) -> compose(compose(domain(Y), domain(X)), h) % 2.52/2.74 605: ifeq(codomain(X), codomain(a), ifeq(codomain(Y), codomain(X), compose(codomain(Y), compose(codomain(X), b)), compose(compose(codomain(Y), codomain(X)), b)), compose(compose(codomain(Y), codomain(X)), b)) -> compose(compose(codomain(Y), codomain(X)), b) % 2.52/2.74 606: ifeq(domain(X), codomain(a), ifeq(codomain(Y), domain(X), compose(codomain(Y), compose(domain(X), b)), compose(compose(codomain(Y), domain(X)), b)), compose(compose(codomain(Y), domain(X)), b)) -> compose(compose(codomain(Y), domain(X)), b) % 2.52/2.74 607: ifeq(codomain(X), codomain(a), ifeq(domain(Y), codomain(X), compose(domain(Y), compose(codomain(X), g)), compose(compose(domain(Y), codomain(X)), g)), compose(compose(domain(Y), codomain(X)), g)) -> compose(compose(domain(Y), codomain(X)), g) % 2.52/2.74 608: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(X), compose(Y, compose(X, compose(a, b))), compose(compose(Y, X), compose(a, b))), compose(compose(Y, X), compose(a, b))) -> compose(compose(Y, X), compose(a, b)) % 2.52/2.74 609: ifeq(codomain(X), domain(Y), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(X, Y)), compose(compose(compose(a, g), X), Y)), compose(compose(compose(a, g), X), Y)) -> compose(compose(compose(a, g), X), Y) % 2.52/2.74 610: ifeq(codomain(X), domain(Y), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(X, Y)), compose(compose(compose(a, b), X), Y)), compose(compose(compose(a, b), X), Y)) -> compose(compose(compose(a, b), X), Y) % 2.52/2.74 611: ifeq(codomain(b), codomain(X), ifeq(domain(Y), codomain(a), compose(domain(Y), compose(b, codomain(X))), compose(compose(domain(Y), b), codomain(X))), compose(compose(domain(Y), b), codomain(X))) -> compose(compose(domain(Y), b), codomain(X)) % 2.52/2.74 612: ifeq(codomain(b), domain(X), ifeq(domain(Y), codomain(a), compose(domain(Y), compose(b, domain(X))), compose(compose(domain(Y), b), domain(X))), compose(compose(domain(Y), b), domain(X))) -> compose(compose(domain(Y), b), domain(X)) % 2.52/2.74 613: ifeq(codomain(g), domain(X), ifeq(codomain(Y), codomain(a), compose(codomain(Y), compose(g, domain(X))), compose(compose(codomain(Y), g), domain(X))), compose(compose(codomain(Y), g), domain(X))) -> compose(compose(codomain(Y), g), domain(X)) % 2.52/2.74 614: ifeq(codomain(g), codomain(X), ifeq(codomain(Y), codomain(a), compose(codomain(Y), compose(h, codomain(X))), compose(compose(codomain(Y), h), codomain(X))), compose(compose(codomain(Y), h), codomain(X))) -> compose(compose(codomain(Y), h), codomain(X)) % 2.52/2.74 615: ifeq(codomain(g), domain(X), ifeq(domain(Y), codomain(a), compose(domain(Y), compose(h, domain(X))), compose(compose(domain(Y), h), domain(X))), compose(compose(domain(Y), h), domain(X))) -> compose(compose(domain(Y), h), domain(X)) % 2.52/2.74 616: ifeq(codomain(g), domain(X), ifeq(domain(Y), codomain(a), compose(domain(Y), compose(g, domain(X))), compose(compose(domain(Y), g), domain(X))), compose(compose(domain(Y), g), domain(X))) -> compose(compose(domain(Y), g), domain(X)) % 2.52/2.74 617: ifeq(codomain(b), codomain(X), ifeq(codomain(Y), codomain(a), compose(codomain(Y), compose(b, codomain(X))), compose(compose(codomain(Y), b), codomain(X))), compose(compose(codomain(Y), b), codomain(X))) -> compose(compose(codomain(Y), b), codomain(X)) % 2.52/2.74 618: ifeq(codomain(b), domain(X), ifeq(codomain(Y), codomain(a), compose(codomain(Y), compose(b, domain(X))), compose(compose(codomain(Y), b), domain(X))), compose(compose(codomain(Y), b), domain(X))) -> compose(compose(codomain(Y), b), domain(X)) % 2.52/2.74 619: ifeq(codomain(g), codomain(X), ifeq(domain(Y), codomain(a), compose(domain(Y), compose(g, codomain(X))), compose(compose(domain(Y), g), codomain(X))), compose(compose(domain(Y), g), codomain(X))) -> compose(compose(domain(Y), g), codomain(X)) % 2.52/2.74 620: ifeq(codomain(g), domain(X), ifeq(codomain(Y), codomain(a), compose(codomain(Y), compose(h, domain(X))), compose(compose(codomain(Y), h), domain(X))), compose(compose(codomain(Y), h), domain(X))) -> compose(compose(codomain(Y), h), domain(X)) % 2.52/2.74 621: ifeq(codomain(g), codomain(X), ifeq(domain(Y), codomain(a), compose(domain(Y), compose(h, codomain(X))), compose(compose(domain(Y), h), codomain(X))), compose(compose(domain(Y), h), codomain(X))) -> compose(compose(domain(Y), h), codomain(X)) % 2.52/2.74 622: ifeq(codomain(b), domain(X), ifeq(codomain(Y), domain(a), compose(Y, compose(compose(a, b), X)), compose(compose(Y, compose(a, b)), X)), compose(compose(Y, compose(a, b)), X)) -> compose(compose(Y, compose(a, b)), X) % 2.52/2.74 623: ifeq(codomain(g), codomain(X), ifeq(codomain(Y), codomain(a), compose(codomain(Y), compose(g, codomain(X))), compose(compose(codomain(Y), g), codomain(X))), compose(compose(codomain(Y), g), codomain(X))) -> compose(compose(codomain(Y), g), codomain(X)) % 2.52/2.74 624: ifeq(codomain(g), codomain(a), ifeq(codomain(X), domain(a), compose(X, compose(compose(a, g), b)), compose(compose(X, compose(a, g)), b)), compose(compose(X, compose(a, g)), b)) -> compose(compose(X, compose(a, g)), b) % 2.52/2.74 625: ifeq(codomain(g), domain(a), ifeq(codomain(X), codomain(a), compose(X, compose(h, compose(a, g))), compose(compose(X, h), compose(a, g))), compose(compose(X, h), compose(a, g))) -> compose(compose(X, h), compose(a, g)) % 2.52/2.74 626: ifeq(codomain(b), domain(a), ifeq(codomain(X), codomain(a), compose(X, compose(b, compose(a, g))), compose(compose(X, b), compose(a, g))), compose(compose(X, b), compose(a, g))) -> compose(compose(X, b), compose(a, g)) % 2.52/2.74 627: ifeq(codomain(g), codomain(a), ifeq(codomain(X), domain(a), compose(X, compose(compose(a, g), h)), compose(compose(X, compose(a, g)), h)), compose(compose(X, compose(a, g)), h)) -> compose(compose(X, compose(a, g)), h) % 2.52/2.74 628: ifeq(codomain(g), codomain(a), ifeq(codomain(X), domain(a), compose(X, compose(compose(a, g), g)), compose(compose(X, compose(a, g)), g)), compose(compose(X, compose(a, g)), g)) -> compose(compose(X, compose(a, g)), g) % 2.52/2.74 629: ifeq(codomain(g), domain(a), ifeq(codomain(X), codomain(a), compose(X, compose(g, compose(a, g))), compose(compose(X, g), compose(a, g))), compose(compose(X, g), compose(a, g))) -> compose(compose(X, g), compose(a, g)) % 2.52/2.74 630: ifeq(domain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(domain(X), compose(a, b)), Z, ifeq(compose(Y, compose(a, b)), Z, Y, domain(X)), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 631: ifeq(codomain(X), codomain(a), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(X, g)), compose(compose(compose(a, b), X), g)), compose(compose(compose(a, b), X), g)) -> compose(compose(compose(a, b), X), g) % 2.52/2.74 632: ifeq(codomain(X), codomain(a), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(X, g)), compose(compose(compose(a, g), X), g)), compose(compose(compose(a, g), X), g)) -> compose(compose(compose(a, g), X), g) % 2.52/2.74 633: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(X), compose(h, compose(X, compose(a, g))), compose(compose(h, X), compose(a, g))), compose(compose(h, X), compose(a, g))) -> compose(compose(h, X), compose(a, g)) % 2.52/2.74 634: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(X), compose(h, compose(X, compose(a, b))), compose(compose(h, X), compose(a, b))), compose(compose(h, X), compose(a, b))) -> compose(compose(h, X), compose(a, b)) % 2.52/2.74 635: ifeq(codomain(X), codomain(a), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(X, h)), compose(compose(compose(a, b), X), h)), compose(compose(compose(a, b), X), h)) -> compose(compose(compose(a, b), X), h) % 2.52/2.74 636: ifeq(codomain(X), codomain(a), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(X, b)), compose(compose(compose(a, b), X), b)), compose(compose(compose(a, b), X), b)) -> compose(compose(compose(a, b), X), b) % 2.52/2.74 637: ifeq(codomain(X), codomain(a), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(X, h)), compose(compose(compose(a, g), X), h)), compose(compose(compose(a, g), X), h)) -> compose(compose(compose(a, g), X), h) % 2.52/2.74 638: ifeq(codomain(X), codomain(a), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(X, b)), compose(compose(compose(a, g), X), b)), compose(compose(compose(a, g), X), b)) -> compose(compose(compose(a, g), X), b) % 2.52/2.74 639: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(X, compose(a, b)), Y, ifeq(compose(compose(a, g), compose(a, b)), Y, compose(a, g), X), X), X), X) -> X % 2.52/2.74 640: ifeq(codomain(X), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(X, compose(a, b)), Y, ifeq(compose(compose(a, b), compose(a, b)), Y, compose(a, b), X), X), X), X) -> X % 2.52/2.74 641: ifeq(codomain(g), domain(X), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, g), X)), compose(compose(h, compose(a, g)), X)), compose(compose(h, compose(a, g)), X)) -> compose(compose(h, compose(a, g)), X) % 2.52/2.74 642: ifeq(codomain(g), domain(X), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(g, X)), compose(compose(compose(a, g), g), X)), compose(compose(compose(a, g), g), X)) -> compose(compose(compose(a, g), g), X) % 2.52/2.74 643: ifeq(codomain(g), domain(a), ifeq(codomain(X), codomain(a), compose(X, compose(g, compose(a, b))), compose(compose(X, g), compose(a, b))), compose(compose(X, g), compose(a, b))) -> compose(compose(X, g), compose(a, b)) % 2.52/2.74 644: ifeq(codomain(b), codomain(a), ifeq(codomain(X), domain(a), compose(X, compose(compose(a, b), h)), compose(compose(X, compose(a, b)), h)), compose(compose(X, compose(a, b)), h)) -> compose(compose(X, compose(a, b)), h) % 2.52/2.74 645: ifeq(codomain(g), domain(X), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(h, X)), compose(compose(compose(a, b), h), X)), compose(compose(compose(a, b), h), X)) -> compose(compose(compose(a, b), h), X) % 2.52/2.74 646: ifeq(codomain(g), domain(X), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(h, X)), compose(compose(compose(a, g), h), X)), compose(compose(compose(a, g), h), X)) -> compose(compose(compose(a, g), h), X) % 2.52/2.74 647: ifeq(codomain(b), codomain(a), ifeq(codomain(X), domain(a), compose(X, compose(compose(a, b), g)), compose(compose(X, compose(a, b)), g)), compose(compose(X, compose(a, b)), g)) -> compose(compose(X, compose(a, b)), g) % 2.52/2.74 648: ifeq(codomain(b), codomain(a), ifeq(codomain(X), domain(a), compose(X, compose(compose(a, b), b)), compose(compose(X, compose(a, b)), b)), compose(compose(X, compose(a, b)), b)) -> compose(compose(X, compose(a, b)), b) % 2.52/2.74 649: ifeq(codomain(b), domain(X), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, b), X)), compose(compose(h, compose(a, b)), X)), compose(compose(h, compose(a, b)), X)) -> compose(compose(h, compose(a, b)), X) % 2.52/2.74 650: ifeq(codomain(b), domain(X), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(b, X)), compose(compose(compose(a, b), b), X)), compose(compose(compose(a, b), b), X)) -> compose(compose(compose(a, b), b), X) % 2.52/2.74 651: ifeq(codomain(b), domain(X), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(b, X)), compose(compose(compose(a, g), b), X)), compose(compose(compose(a, g), b), X)) -> compose(compose(compose(a, g), b), X) % 2.52/2.74 652: ifeq(codomain(g), domain(X), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(g, X)), compose(compose(compose(a, b), g), X)), compose(compose(compose(a, b), g), X)) -> compose(compose(compose(a, b), g), X) % 2.52/2.74 653: ifeq(codomain(b), domain(a), ifeq(codomain(X), codomain(a), compose(X, compose(b, compose(a, b))), compose(compose(X, b), compose(a, b))), compose(compose(X, b), compose(a, b))) -> compose(compose(X, b), compose(a, b)) % 2.52/2.74 654: ifeq(codomain(g), domain(a), ifeq(codomain(X), codomain(a), compose(X, compose(h, compose(a, b))), compose(compose(X, h), compose(a, b))), compose(compose(X, h), compose(a, b))) -> compose(compose(X, h), compose(a, b)) % 2.52/2.74 655: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(codomain(X), compose(a, b)), Z, ifeq(compose(Y, compose(a, b)), Z, Y, codomain(X)), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 656: ifeq(codomain(b), codomain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(b, b)), compose(compose(compose(a, b), b), b)), compose(compose(compose(a, b), b), b)) -> compose(compose(compose(a, b), b), b) % 2.52/2.74 657: ifeq(codomain(g), domain(a), ifeq(codomain(g), codomain(a), compose(h, compose(h, compose(a, g))), compose(compose(h, h), compose(a, g))), compose(compose(h, h), compose(a, g))) -> compose(compose(h, h), compose(a, g)) % 2.52/2.74 658: ifeq(codomain(b), codomain(a), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, b), h)), compose(compose(h, compose(a, b)), h)), compose(compose(h, compose(a, b)), h)) -> compose(compose(h, compose(a, b)), h) % 2.52/2.74 659: ifeq(codomain(g), codomain(a), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, g), h)), compose(compose(h, compose(a, g)), h)), compose(compose(h, compose(a, g)), h)) -> compose(compose(h, compose(a, g)), h) % 2.52/2.74 660: ifeq(codomain(b), codomain(a), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, b), b)), compose(compose(h, compose(a, b)), b)), compose(compose(h, compose(a, b)), b)) -> compose(compose(h, compose(a, b)), b) % 2.52/2.74 661: ifeq(codomain(g), codomain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(g, g)), compose(compose(compose(a, b), g), g)), compose(compose(compose(a, b), g), g)) -> compose(compose(compose(a, b), g), g) % 2.52/2.74 662: ifeq(codomain(g), codomain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(g, g)), compose(compose(compose(a, g), g), g)), compose(compose(compose(a, g), g), g)) -> compose(compose(compose(a, g), g), g) % 2.52/2.74 663: ifeq(domain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(domain(X), compose(a, b)), Y, ifeq(compose(h, compose(a, b)), Y, h, domain(X)), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 664: ifeq(codomain(g), codomain(a), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, g), g)), compose(compose(h, compose(a, g)), g)), compose(compose(h, compose(a, g)), g)) -> compose(compose(h, compose(a, g)), g) % 2.52/2.74 665: ifeq(codomain(g), codomain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(g, b)), compose(compose(compose(a, g), g), b)), compose(compose(compose(a, g), g), b)) -> compose(compose(compose(a, g), g), b) % 2.52/2.74 666: ifeq(codomain(X), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(codomain(X), compose(a, b)), compose(compose(a, b), compose(a, b)), compose(a, b), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 667: ifeq(domain(X), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(compose(a, b), compose(a, b)), compose(domain(X), compose(a, b)), compose(a, b), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 668: ifeq(domain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(compose(a, g), compose(a, b)), compose(domain(X), compose(a, b)), compose(a, g), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 669: ifeq(domain(X), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(domain(X), compose(a, b)), compose(compose(a, b), compose(a, b)), compose(a, b), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 670: ifeq(domain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(domain(X), compose(a, b)), compose(compose(a, g), compose(a, b)), compose(a, g), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 671: ifeq(codomain(g), codomain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(g, b)), compose(compose(compose(a, b), g), b)), compose(compose(compose(a, b), g), b)) -> compose(compose(compose(a, b), g), b) % 2.52/2.74 672: ifeq(codomain(b), codomain(a), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, b), g)), compose(compose(h, compose(a, b)), g)), compose(compose(h, compose(a, b)), g)) -> compose(compose(h, compose(a, b)), g) % 2.52/2.74 673: ifeq(codomain(b), codomain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(b, b)), compose(compose(compose(a, g), b), b)), compose(compose(compose(a, g), b), b)) -> compose(compose(compose(a, g), b), b) % 2.52/2.74 674: ifeq(codomain(g), domain(a), ifeq(codomain(g), codomain(a), compose(h, compose(h, compose(a, b))), compose(compose(h, h), compose(a, b))), compose(compose(h, h), compose(a, b))) -> compose(compose(h, h), compose(a, b)) % 2.52/2.74 675: ifeq(codomain(b), codomain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(b, g)), compose(compose(compose(a, b), b), g)), compose(compose(compose(a, b), b), g)) -> compose(compose(compose(a, b), b), g) % 2.52/2.74 676: ifeq(codomain(X), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(compose(a, b), compose(a, b)), compose(codomain(X), compose(a, b)), compose(a, b), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 677: ifeq(codomain(g), domain(a), ifeq(codomain(g), codomain(a), compose(h, compose(g, compose(a, g))), compose(compose(h, g), compose(a, g))), compose(compose(h, g), compose(a, g))) -> compose(compose(h, g), compose(a, g)) % 2.52/2.74 678: ifeq(codomain(g), domain(a), ifeq(codomain(g), codomain(a), compose(h, compose(g, compose(a, b))), compose(compose(h, g), compose(a, b))), compose(compose(h, g), compose(a, b))) -> compose(compose(h, g), compose(a, b)) % 2.52/2.74 679: ifeq(codomain(g), codomain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(h, g)), compose(compose(compose(a, g), h), g)), compose(compose(compose(a, g), h), g)) -> compose(compose(compose(a, g), h), g) % 2.52/2.74 680: ifeq(codomain(g), codomain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(h, b)), compose(compose(compose(a, g), h), b)), compose(compose(compose(a, g), h), b)) -> compose(compose(compose(a, g), h), b) % 2.52/2.74 681: ifeq(codomain(g), codomain(a), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, g), b)), compose(compose(h, compose(a, g)), b)), compose(compose(h, compose(a, g)), b)) -> compose(compose(h, compose(a, g)), b) % 2.52/2.74 682: ifeq(codomain(g), codomain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(h, b)), compose(compose(compose(a, b), h), b)), compose(compose(compose(a, b), h), b)) -> compose(compose(compose(a, b), h), b) % 2.52/2.74 683: ifeq(codomain(g), codomain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(g, h)), compose(compose(compose(a, b), g), h)), compose(compose(compose(a, b), g), h)) -> compose(compose(compose(a, b), g), h) % 2.52/2.74 684: ifeq(codomain(b), codomain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(b, h)), compose(compose(compose(a, g), b), h)), compose(compose(compose(a, g), b), h)) -> compose(compose(compose(a, g), b), h) % 2.52/2.74 685: ifeq(codomain(g), codomain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(g, h)), compose(compose(compose(a, g), g), h)), compose(compose(compose(a, g), g), h)) -> compose(compose(compose(a, g), g), h) % 2.52/2.74 686: ifeq(codomain(g), codomain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(h, g)), compose(compose(compose(a, b), h), g)), compose(compose(compose(a, b), h), g)) -> compose(compose(compose(a, b), h), g) % 2.52/2.74 687: ifeq(codomain(b), codomain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(b, h)), compose(compose(compose(a, b), b), h)), compose(compose(compose(a, b), b), h)) -> compose(compose(compose(a, b), b), h) % 2.52/2.74 688: ifeq(codomain(b), codomain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(b, g)), compose(compose(compose(a, g), b), g)), compose(compose(compose(a, g), b), g)) -> compose(compose(compose(a, g), b), g) % 2.52/2.74 689: ifeq(codomain(g), codomain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(h, h)), compose(compose(compose(a, g), h), h)), compose(compose(compose(a, g), h), h)) -> compose(compose(compose(a, g), h), h) % 2.52/2.74 690: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(codomain(X), compose(a, b)), compose(compose(a, g), compose(a, b)), compose(a, g), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 691: ifeq(codomain(b), domain(a), ifeq(codomain(g), codomain(a), compose(h, compose(b, compose(a, g))), compose(compose(h, b), compose(a, g))), compose(compose(h, b), compose(a, g))) -> compose(compose(h, b), compose(a, g)) % 2.52/2.74 692: ifeq(codomain(b), domain(a), ifeq(codomain(g), codomain(a), compose(h, compose(b, compose(a, b))), compose(compose(h, b), compose(a, b))), compose(compose(h, b), compose(a, b))) -> compose(compose(h, b), compose(a, b)) % 2.52/2.74 693: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(compose(a, g), compose(a, b)), compose(codomain(X), compose(a, b)), compose(a, g), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 694: ifeq(codomain(g), codomain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(h, h)), compose(compose(compose(a, b), h), h)), compose(compose(compose(a, b), h), h)) -> compose(compose(compose(a, b), h), h) % 2.52/2.74 695: ifeq(codomain(g), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(h, compose(a, b)), X, ifeq(compose(compose(a, b), compose(a, b)), X, compose(a, b), h), h), h), h) -> h % 2.52/2.74 696: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(h, compose(a, b)), X, ifeq(compose(compose(a, g), compose(a, b)), X, compose(a, g), h), h), h), h) -> h % 2.52/2.74 697: ifeq(codomain(g), codomain(a), ifeq(domain(compose(h, h)), codomain(a), compose(h, h), compose(compose(domain(compose(h, h)), h), h)), compose(compose(domain(compose(h, h)), h), h)) -> compose(compose(domain(compose(h, h)), h), h) % 2.52/2.74 698: ifeq(codomain(g), codomain(a), ifeq(domain(compose(h, b)), codomain(a), compose(h, b), compose(compose(domain(compose(h, b)), h), b)), compose(compose(domain(compose(h, b)), h), b)) -> compose(compose(domain(compose(h, b)), h), b) % 2.52/2.74 699: ifeq(codomain(g), codomain(a), ifeq(domain(compose(g, b)), codomain(a), compose(g, b), compose(compose(domain(compose(g, b)), g), b)), compose(compose(domain(compose(g, b)), g), b)) -> compose(compose(domain(compose(g, b)), g), b) % 2.52/2.74 700: ifeq(codomain(g), codomain(a), ifeq(domain(compose(g, h)), codomain(a), compose(g, h), compose(compose(domain(compose(g, h)), g), h)), compose(compose(domain(compose(g, h)), g), h)) -> compose(compose(domain(compose(g, h)), g), h) % 2.52/2.74 701: ifeq(codomain(b), codomain(a), ifeq(domain(compose(b, h)), codomain(a), compose(b, h), compose(compose(domain(compose(b, h)), b), h)), compose(compose(domain(compose(b, h)), b), h)) -> compose(compose(domain(compose(b, h)), b), h) % 2.52/2.74 702: ifeq(codomain(g), codomain(a), ifeq(domain(compose(g, g)), codomain(a), compose(g, g), compose(compose(domain(compose(g, g)), g), g)), compose(compose(domain(compose(g, g)), g), g)) -> compose(compose(domain(compose(g, g)), g), g) % 2.52/2.74 703: ifeq(codomain(g), codomain(a), ifeq(domain(compose(h, g)), codomain(a), compose(h, g), compose(compose(domain(compose(h, g)), h), g)), compose(compose(domain(compose(h, g)), h), g)) -> compose(compose(domain(compose(h, g)), h), g) % 2.52/2.74 704: ifeq(codomain(b), codomain(a), ifeq(domain(compose(b, b)), codomain(a), compose(b, b), compose(compose(domain(compose(b, b)), b), b)), compose(compose(domain(compose(b, b)), b), b)) -> compose(compose(domain(compose(b, b)), b), b) % 2.52/2.74 705: ifeq(codomain(b), codomain(a), ifeq(domain(compose(b, g)), codomain(a), compose(b, g), compose(compose(domain(compose(b, g)), b), g)), compose(compose(domain(compose(b, g)), b), g)) -> compose(compose(domain(compose(b, g)), b), g) % 2.52/2.74 706: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(codomain(X), compose(a, b)), Y, ifeq(compose(h, compose(a, b)), Y, h, codomain(X)), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 707: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(X, compose(a, b)), compose(compose(a, g), compose(a, b)), X, compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 708: ifeq(codomain(b), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(compose(a, b), compose(a, b)), compose(X, compose(a, b)), X, compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 709: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(compose(a, g), compose(a, b)), compose(X, compose(a, b)), X, compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 710: ifeq(codomain(b), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(X, compose(a, b)), compose(compose(a, b), compose(a, b)), X, compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 711: ifeq(codomain(b), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(h, compose(a, b)), compose(compose(a, b), compose(a, b)), h, compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 712: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(compose(a, g), compose(a, b)), compose(h, compose(a, b)), h, compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 713: ifeq(codomain(b), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(compose(a, b), compose(a, b)), compose(h, compose(a, b)), h, compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 714: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(h, compose(a, b)), compose(compose(a, g), compose(a, b)), h, compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 715: ifeq(domain(X), domain(Y), ifeq(domain(Z), domain(X), compose(domain(Z), compose(domain(X), domain(Y))), compose(compose(domain(Z), domain(X)), domain(Y))), compose(compose(domain(Z), domain(X)), domain(Y))) -> compose(compose(domain(Z), domain(X)), domain(Y)) % 2.52/2.74 716: ifeq(domain(X), codomain(Y), ifeq(codomain(Z), domain(X), compose(codomain(Z), compose(domain(X), codomain(Y))), compose(compose(codomain(Z), domain(X)), codomain(Y))), compose(compose(codomain(Z), domain(X)), codomain(Y))) -> compose(compose(codomain(Z), domain(X)), codomain(Y)) % 2.52/2.74 717: ifeq(codomain(X), codomain(Y), ifeq(codomain(Z), codomain(X), compose(codomain(Z), compose(codomain(X), codomain(Y))), compose(compose(codomain(Z), codomain(X)), codomain(Y))), compose(compose(codomain(Z), codomain(X)), codomain(Y))) -> compose(compose(codomain(Z), codomain(X)), codomain(Y)) % 2.52/2.74 718: ifeq(domain(X), codomain(Y), ifeq(domain(Z), domain(X), compose(domain(Z), compose(domain(X), codomain(Y))), compose(compose(domain(Z), domain(X)), codomain(Y))), compose(compose(domain(Z), domain(X)), codomain(Y))) -> compose(compose(domain(Z), domain(X)), codomain(Y)) % 2.52/2.74 719: ifeq(codomain(X), codomain(Y), ifeq(domain(Z), codomain(X), compose(domain(Z), compose(codomain(X), codomain(Y))), compose(compose(domain(Z), codomain(X)), codomain(Y))), compose(compose(domain(Z), codomain(X)), codomain(Y))) -> compose(compose(domain(Z), codomain(X)), codomain(Y)) % 2.52/2.74 720: ifeq(codomain(X), domain(Y), ifeq(domain(Z), codomain(X), compose(domain(Z), compose(codomain(X), domain(Y))), compose(compose(domain(Z), codomain(X)), domain(Y))), compose(compose(domain(Z), codomain(X)), domain(Y))) -> compose(compose(domain(Z), codomain(X)), domain(Y)) % 2.52/2.74 721: ifeq(domain(X), domain(Y), ifeq(codomain(Z), domain(X), compose(codomain(Z), compose(domain(X), domain(Y))), compose(compose(codomain(Z), domain(X)), domain(Y))), compose(compose(codomain(Z), domain(X)), domain(Y))) -> compose(compose(codomain(Z), domain(X)), domain(Y)) % 2.52/2.74 722: ifeq(codomain(X), domain(Y), ifeq(codomain(Z), codomain(X), compose(codomain(Z), compose(codomain(X), domain(Y))), compose(compose(codomain(Z), codomain(X)), domain(Y))), compose(compose(codomain(Z), codomain(X)), domain(Y))) -> compose(compose(codomain(Z), codomain(X)), domain(Y)) % 2.52/2.74 723: ifeq(codomain(X), domain(a), ifeq(codomain(Y), codomain(X), compose(Y, compose(codomain(X), compose(a, g))), compose(compose(Y, codomain(X)), compose(a, g))), compose(compose(Y, codomain(X)), compose(a, g))) -> compose(compose(Y, codomain(X)), compose(a, g)) % 2.52/2.74 724: ifeq(codomain(X), domain(a), ifeq(domain(Y), domain(X), compose(domain(Y), compose(X, compose(a, g))), compose(compose(domain(Y), X), compose(a, g))), compose(compose(domain(Y), X), compose(a, g))) -> compose(compose(domain(Y), X), compose(a, g)) % 2.52/2.74 725: ifeq(domain(X), domain(a), ifeq(codomain(Y), domain(X), compose(Y, compose(domain(X), compose(a, g))), compose(compose(Y, domain(X)), compose(a, g))), compose(compose(Y, domain(X)), compose(a, g))) -> compose(compose(Y, domain(X)), compose(a, g)) % 2.52/2.74 726: ifeq(codomain(g), domain(X), ifeq(domain(Y), domain(a), compose(domain(Y), compose(compose(a, g), X)), compose(compose(domain(Y), compose(a, g)), X)), compose(compose(domain(Y), compose(a, g)), X)) -> compose(compose(domain(Y), compose(a, g)), X) % 2.52/2.74 727: ifeq(codomain(g), codomain(X), ifeq(codomain(Y), domain(a), compose(Y, compose(compose(a, g), codomain(X))), compose(compose(Y, compose(a, g)), codomain(X))), compose(compose(Y, compose(a, g)), codomain(X))) -> compose(compose(Y, compose(a, g)), codomain(X)) % 2.52/2.74 728: ifeq(domain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(domain(X), compose(a, b)), Z, ifeq(compose(codomain(Y), compose(a, b)), Z, codomain(Y), domain(X)), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 729: ifeq(domain(X), domain(a), ifeq(domain(Y), domain(a), ifeq(compose(domain(X), compose(a, b)), Z, ifeq(compose(domain(Y), compose(a, b)), Z, domain(Y), domain(X)), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 730: ifeq(codomain(X), domain(a), ifeq(domain(Y), domain(a), ifeq(compose(codomain(X), compose(a, b)), Z, ifeq(compose(domain(Y), compose(a, b)), Z, domain(Y), codomain(X)), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 731: ifeq(codomain(X), domain(a), ifeq(codomain(Y), codomain(X), compose(Y, compose(codomain(X), compose(a, b))), compose(compose(Y, codomain(X)), compose(a, b))), compose(compose(Y, codomain(X)), compose(a, b))) -> compose(compose(Y, codomain(X)), compose(a, b)) % 2.52/2.74 732: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(X), compose(codomain(Y), compose(X, compose(a, g))), compose(compose(codomain(Y), X), compose(a, g))), compose(compose(codomain(Y), X), compose(a, g))) -> compose(compose(codomain(Y), X), compose(a, g)) % 2.52/2.74 733: ifeq(codomain(X), domain(Y), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(X, domain(Y))), compose(compose(compose(a, b), X), domain(Y))), compose(compose(compose(a, b), X), domain(Y))) -> compose(compose(compose(a, b), X), domain(Y)) % 2.52/2.74 734: ifeq(codomain(X), domain(Y), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(X, domain(Y))), compose(compose(compose(a, g), X), domain(Y))), compose(compose(compose(a, g), X), domain(Y))) -> compose(compose(compose(a, g), X), domain(Y)) % 2.52/2.74 735: ifeq(codomain(X), domain(Y), ifeq(codomain(b), codomain(X), compose(compose(a, b), compose(codomain(X), Y)), compose(compose(compose(a, b), codomain(X)), Y)), compose(compose(compose(a, b), codomain(X)), Y)) -> compose(compose(compose(a, b), codomain(X)), Y) % 2.52/2.74 736: ifeq(domain(X), domain(Y), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(domain(X), Y)), compose(compose(compose(a, g), domain(X)), Y)), compose(compose(compose(a, g), domain(X)), Y)) -> compose(compose(compose(a, g), domain(X)), Y) % 2.52/2.74 737: ifeq(codomain(X), domain(Y), ifeq(codomain(g), codomain(X), compose(compose(a, g), compose(codomain(X), Y)), compose(compose(compose(a, g), codomain(X)), Y)), compose(compose(compose(a, g), codomain(X)), Y)) -> compose(compose(compose(a, g), codomain(X)), Y) % 2.52/2.74 738: ifeq(domain(X), domain(a), ifeq(codomain(Y), domain(X), compose(Y, compose(domain(X), compose(a, b))), compose(compose(Y, domain(X)), compose(a, b))), compose(compose(Y, domain(X)), compose(a, b))) -> compose(compose(Y, domain(X)), compose(a, b)) % 2.52/2.74 739: ifeq(codomain(X), codomain(Y), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(X, codomain(Y))), compose(compose(compose(a, g), X), codomain(Y))), compose(compose(compose(a, g), X), codomain(Y))) -> compose(compose(compose(a, g), X), codomain(Y)) % 2.52/2.74 740: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(X), compose(codomain(Y), compose(X, compose(a, b))), compose(compose(codomain(Y), X), compose(a, b))), compose(compose(codomain(Y), X), compose(a, b))) -> compose(compose(codomain(Y), X), compose(a, b)) % 2.52/2.74 741: ifeq(domain(X), domain(Y), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(domain(X), Y)), compose(compose(compose(a, b), domain(X)), Y)), compose(compose(compose(a, b), domain(X)), Y)) -> compose(compose(compose(a, b), domain(X)), Y) % 2.52/2.74 742: ifeq(codomain(X), domain(a), ifeq(domain(Y), domain(X), compose(domain(Y), compose(X, compose(a, b))), compose(compose(domain(Y), X), compose(a, b))), compose(compose(domain(Y), X), compose(a, b))) -> compose(compose(domain(Y), X), compose(a, b)) % 2.52/2.74 743: ifeq(codomain(X), codomain(Y), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(X, codomain(Y))), compose(compose(compose(a, b), X), codomain(Y))), compose(compose(compose(a, b), X), codomain(Y))) -> compose(compose(compose(a, b), X), codomain(Y)) % 2.52/2.74 744: ifeq(codomain(b), domain(X), ifeq(codomain(Y), domain(a), compose(Y, compose(compose(a, b), domain(X))), compose(compose(Y, compose(a, b)), domain(X))), compose(compose(Y, compose(a, b)), domain(X))) -> compose(compose(Y, compose(a, b)), domain(X)) % 2.52/2.74 745: ifeq(codomain(g), domain(X), ifeq(codomain(Y), domain(a), compose(Y, compose(compose(a, g), domain(X))), compose(compose(Y, compose(a, g)), domain(X))), compose(compose(Y, compose(a, g)), domain(X))) -> compose(compose(Y, compose(a, g)), domain(X)) % 2.52/2.74 746: ifeq(codomain(g), domain(X), ifeq(codomain(Y), domain(a), compose(codomain(Y), compose(compose(a, g), X)), compose(compose(codomain(Y), compose(a, g)), X)), compose(compose(codomain(Y), compose(a, g)), X)) -> compose(compose(codomain(Y), compose(a, g)), X) % 2.52/2.74 747: ifeq(codomain(b), domain(X), ifeq(domain(Y), domain(a), compose(domain(Y), compose(compose(a, b), X)), compose(compose(domain(Y), compose(a, b)), X)), compose(compose(domain(Y), compose(a, b)), X)) -> compose(compose(domain(Y), compose(a, b)), X) % 2.52/2.74 748: ifeq(codomain(b), codomain(X), ifeq(codomain(Y), domain(a), compose(Y, compose(compose(a, b), codomain(X))), compose(compose(Y, compose(a, b)), codomain(X))), compose(compose(Y, compose(a, b)), codomain(X))) -> compose(compose(Y, compose(a, b)), codomain(X)) % 2.52/2.74 749: ifeq(codomain(b), domain(X), ifeq(codomain(Y), domain(a), compose(codomain(Y), compose(compose(a, b), X)), compose(compose(codomain(Y), compose(a, b)), X)), compose(compose(codomain(Y), compose(a, b)), X)) -> compose(compose(codomain(Y), compose(a, b)), X) % 2.52/2.74 750: ifeq(codomain(X), domain(a), ifeq(codomain(Y), domain(a), ifeq(compose(codomain(X), compose(a, b)), Z, ifeq(compose(codomain(Y), compose(a, b)), Z, codomain(Y), codomain(X)), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 751: ifeq(domain(X), codomain(a), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(domain(X), g)), compose(compose(compose(a, g), domain(X)), g)), compose(compose(compose(a, g), domain(X)), g)) -> compose(compose(compose(a, g), domain(X)), g) % 2.52/2.74 752: ifeq(codomain(X), codomain(a), ifeq(codomain(g), codomain(X), compose(compose(a, g), compose(codomain(X), h)), compose(compose(compose(a, g), codomain(X)), h)), compose(compose(compose(a, g), codomain(X)), h)) -> compose(compose(compose(a, g), codomain(X)), h) % 2.52/2.74 753: ifeq(codomain(X), domain(a), ifeq(codomain(g), codomain(X), compose(h, compose(codomain(X), compose(a, g))), compose(compose(h, codomain(X)), compose(a, g))), compose(compose(h, codomain(X)), compose(a, g))) -> compose(compose(h, codomain(X)), compose(a, g)) % 2.52/2.74 754: ifeq(domain(X), codomain(a), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(domain(X), h)), compose(compose(compose(a, b), domain(X)), h)), compose(compose(compose(a, b), domain(X)), h)) -> compose(compose(compose(a, b), domain(X)), h) % 2.52/2.74 755: ifeq(domain(X), codomain(a), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(domain(X), h)), compose(compose(compose(a, g), domain(X)), h)), compose(compose(compose(a, g), domain(X)), h)) -> compose(compose(compose(a, g), domain(X)), h) % 2.52/2.74 756: ifeq(domain(X), domain(a), ifeq(codomain(g), domain(X), compose(h, compose(domain(X), compose(a, g))), compose(compose(h, domain(X)), compose(a, g))), compose(compose(h, domain(X)), compose(a, g))) -> compose(compose(h, domain(X)), compose(a, g)) % 2.52/2.74 757: ifeq(domain(X), codomain(a), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(domain(X), b)), compose(compose(compose(a, b), domain(X)), b)), compose(compose(compose(a, b), domain(X)), b)) -> compose(compose(compose(a, b), domain(X)), b) % 2.52/2.74 758: ifeq(codomain(X), domain(a), ifeq(codomain(g), codomain(X), compose(h, compose(codomain(X), compose(a, b))), compose(compose(h, codomain(X)), compose(a, b))), compose(compose(h, codomain(X)), compose(a, b))) -> compose(compose(h, codomain(X)), compose(a, b)) % 2.52/2.74 759: ifeq(codomain(X), codomain(a), ifeq(codomain(g), codomain(X), compose(compose(a, g), compose(codomain(X), b)), compose(compose(compose(a, g), codomain(X)), b)), compose(compose(compose(a, g), codomain(X)), b)) -> compose(compose(compose(a, g), codomain(X)), b) % 2.52/2.74 760: ifeq(codomain(X), codomain(a), ifeq(codomain(b), codomain(X), compose(compose(a, b), compose(codomain(X), b)), compose(compose(compose(a, b), codomain(X)), b)), compose(compose(compose(a, b), codomain(X)), b)) -> compose(compose(compose(a, b), codomain(X)), b) % 2.52/2.74 761: ifeq(codomain(X), codomain(a), ifeq(codomain(b), codomain(X), compose(compose(a, b), compose(codomain(X), g)), compose(compose(compose(a, b), codomain(X)), g)), compose(compose(compose(a, b), codomain(X)), g)) -> compose(compose(compose(a, b), codomain(X)), g) % 2.52/2.74 762: ifeq(codomain(X), codomain(a), ifeq(codomain(g), codomain(X), compose(compose(a, g), compose(codomain(X), g)), compose(compose(compose(a, g), codomain(X)), g)), compose(compose(compose(a, g), codomain(X)), g)) -> compose(compose(compose(a, g), codomain(X)), g) % 2.52/2.74 763: ifeq(domain(X), codomain(a), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(domain(X), g)), compose(compose(compose(a, b), domain(X)), g)), compose(compose(compose(a, b), domain(X)), g)) -> compose(compose(compose(a, b), domain(X)), g) % 2.52/2.74 764: ifeq(domain(X), codomain(a), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(domain(X), b)), compose(compose(compose(a, g), domain(X)), b)), compose(compose(compose(a, g), domain(X)), b)) -> compose(compose(compose(a, g), domain(X)), b) % 2.52/2.74 765: ifeq(codomain(X), codomain(a), ifeq(codomain(b), codomain(X), compose(compose(a, b), compose(codomain(X), h)), compose(compose(compose(a, b), codomain(X)), h)), compose(compose(compose(a, b), codomain(X)), h)) -> compose(compose(compose(a, b), codomain(X)), h) % 2.52/2.74 766: ifeq(domain(X), domain(a), ifeq(codomain(g), domain(X), compose(h, compose(domain(X), compose(a, b))), compose(compose(h, domain(X)), compose(a, b))), compose(compose(h, domain(X)), compose(a, b))) -> compose(compose(h, domain(X)), compose(a, b)) % 2.52/2.74 767: ifeq(domain(X), codomain(compose(codomain(Y), domain(X))), ifeq(codomain(Y), domain(X), compose(codomain(Y), compose(domain(X), codomain(compose(codomain(Y), domain(X))))), compose(codomain(Y), domain(X))), compose(codomain(Y), domain(X))) -> compose(codomain(Y), domain(X)) % 2.52/2.74 768: ifeq(codomain(X), codomain(compose(domain(Y), codomain(X))), ifeq(domain(Y), codomain(X), compose(domain(Y), compose(codomain(X), codomain(compose(domain(Y), codomain(X))))), compose(domain(Y), codomain(X))), compose(domain(Y), codomain(X))) -> compose(domain(Y), codomain(X)) % 2.52/2.74 769: ifeq(codomain(X), codomain(compose(codomain(Y), codomain(X))), ifeq(codomain(Y), codomain(X), compose(codomain(Y), compose(codomain(X), codomain(compose(codomain(Y), codomain(X))))), compose(codomain(Y), codomain(X))), compose(codomain(Y), codomain(X))) -> compose(codomain(Y), codomain(X)) % 2.52/2.74 770: ifeq(domain(X), codomain(compose(domain(Y), domain(X))), ifeq(domain(Y), domain(X), compose(domain(Y), compose(domain(X), codomain(compose(domain(Y), domain(X))))), compose(domain(Y), domain(X))), compose(domain(Y), domain(X))) -> compose(domain(Y), domain(X)) % 2.52/2.74 771: ifeq(codomain(g), domain(a), ifeq(domain(X), domain(a), ifeq(compose(domain(X), compose(a, b)), compose(compose(a, g), compose(a, b)), domain(X), compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 772: ifeq(codomain(b), domain(a), ifeq(domain(X), domain(a), ifeq(compose(compose(a, b), compose(a, b)), compose(domain(X), compose(a, b)), domain(X), compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 773: ifeq(codomain(g), domain(a), ifeq(domain(X), domain(a), ifeq(compose(compose(a, g), compose(a, b)), compose(domain(X), compose(a, b)), domain(X), compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 774: ifeq(codomain(b), domain(a), ifeq(domain(X), domain(a), ifeq(compose(domain(X), compose(a, b)), compose(compose(a, b), compose(a, b)), domain(X), compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 775: ifeq(codomain(b), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(compose(a, b), compose(a, b)), compose(codomain(X), compose(a, b)), codomain(X), compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 776: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(compose(a, g), compose(a, b)), compose(codomain(X), compose(a, b)), codomain(X), compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 777: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(codomain(X), compose(a, b)), compose(compose(a, g), compose(a, b)), codomain(X), compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 778: ifeq(codomain(b), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(codomain(X), compose(a, b)), compose(compose(a, b), compose(a, b)), codomain(X), compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 779: ifeq(codomain(g), codomain(a), ifeq(domain(X), domain(a), compose(domain(X), compose(compose(a, g), b)), compose(compose(domain(X), compose(a, g)), b)), compose(compose(domain(X), compose(a, g)), b)) -> compose(compose(domain(X), compose(a, g)), b) % 2.52/2.74 780: ifeq(codomain(g), codomain(a), ifeq(codomain(X), domain(a), compose(codomain(X), compose(compose(a, g), b)), compose(compose(codomain(X), compose(a, g)), b)), compose(compose(codomain(X), compose(a, g)), b)) -> compose(compose(codomain(X), compose(a, g)), b) % 2.52/2.74 781: ifeq(codomain(b), codomain(a), ifeq(domain(X), domain(a), compose(domain(X), compose(compose(a, b), b)), compose(compose(domain(X), compose(a, b)), b)), compose(compose(domain(X), compose(a, b)), b)) -> compose(compose(domain(X), compose(a, b)), b) % 2.52/2.74 782: ifeq(codomain(g), codomain(a), ifeq(domain(X), domain(a), compose(domain(X), compose(compose(a, g), g)), compose(compose(domain(X), compose(a, g)), g)), compose(compose(domain(X), compose(a, g)), g)) -> compose(compose(domain(X), compose(a, g)), g) % 2.52/2.74 783: ifeq(codomain(g), domain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(h, compose(a, g))), compose(compose(domain(X), h), compose(a, g))), compose(compose(domain(X), h), compose(a, g))) -> compose(compose(domain(X), h), compose(a, g)) % 2.52/2.74 784: ifeq(codomain(g), domain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(g, compose(a, g))), compose(compose(domain(X), g), compose(a, g))), compose(compose(domain(X), g), compose(a, g))) -> compose(compose(domain(X), g), compose(a, g)) % 2.52/2.74 785: ifeq(codomain(b), codomain(a), ifeq(codomain(X), domain(a), compose(codomain(X), compose(compose(a, b), b)), compose(compose(codomain(X), compose(a, b)), b)), compose(compose(codomain(X), compose(a, b)), b)) -> compose(compose(codomain(X), compose(a, b)), b) % 2.52/2.74 786: ifeq(codomain(g), codomain(a), ifeq(domain(X), domain(a), compose(domain(X), compose(compose(a, g), h)), compose(compose(domain(X), compose(a, g)), h)), compose(compose(domain(X), compose(a, g)), h)) -> compose(compose(domain(X), compose(a, g)), h) % 2.52/2.74 787: ifeq(codomain(b), codomain(X), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, b), codomain(X))), compose(compose(h, compose(a, b)), codomain(X))), compose(compose(h, compose(a, b)), codomain(X))) -> compose(compose(h, compose(a, b)), codomain(X)) % 2.52/2.74 788: ifeq(codomain(g), domain(X), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(g, domain(X))), compose(compose(compose(a, b), g), domain(X))), compose(compose(compose(a, b), g), domain(X))) -> compose(compose(compose(a, b), g), domain(X)) % 2.52/2.74 789: ifeq(codomain(b), codomain(a), ifeq(codomain(X), domain(a), compose(codomain(X), compose(compose(a, b), g)), compose(compose(codomain(X), compose(a, b)), g)), compose(compose(codomain(X), compose(a, b)), g)) -> compose(compose(codomain(X), compose(a, b)), g) % 2.52/2.74 790: ifeq(codomain(g), codomain(a), ifeq(codomain(X), domain(a), compose(codomain(X), compose(compose(a, g), g)), compose(compose(codomain(X), compose(a, g)), g)), compose(compose(codomain(X), compose(a, g)), g)) -> compose(compose(codomain(X), compose(a, g)), g) % 2.52/2.74 791: ifeq(codomain(g), domain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(g, compose(a, g))), compose(compose(codomain(X), g), compose(a, g))), compose(compose(codomain(X), g), compose(a, g))) -> compose(compose(codomain(X), g), compose(a, g)) % 2.52/2.74 792: ifeq(codomain(b), codomain(X), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(b, codomain(X))), compose(compose(compose(a, g), b), codomain(X))), compose(compose(compose(a, g), b), codomain(X))) -> compose(compose(compose(a, g), b), codomain(X)) % 2.52/2.74 793: ifeq(codomain(b), domain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(b, compose(a, b))), compose(compose(domain(X), b), compose(a, b))), compose(compose(domain(X), b), compose(a, b))) -> compose(compose(domain(X), b), compose(a, b)) % 2.52/2.74 794: ifeq(codomain(g), domain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(h, compose(a, g))), compose(compose(codomain(X), h), compose(a, g))), compose(compose(codomain(X), h), compose(a, g))) -> compose(compose(codomain(X), h), compose(a, g)) % 2.52/2.74 795: ifeq(codomain(b), codomain(a), ifeq(domain(X), domain(a), compose(domain(X), compose(compose(a, b), h)), compose(compose(domain(X), compose(a, b)), h)), compose(compose(domain(X), compose(a, b)), h)) -> compose(compose(domain(X), compose(a, b)), h) % 2.52/2.74 796: ifeq(codomain(b), domain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(b, compose(a, g))), compose(compose(domain(X), b), compose(a, g))), compose(compose(domain(X), b), compose(a, g))) -> compose(compose(domain(X), b), compose(a, g)) % 2.52/2.74 797: ifeq(codomain(g), codomain(X), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, g), codomain(X))), compose(compose(h, compose(a, g)), codomain(X))), compose(compose(h, compose(a, g)), codomain(X))) -> compose(compose(h, compose(a, g)), codomain(X)) % 2.52/2.74 798: ifeq(codomain(g), codomain(X), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(h, codomain(X))), compose(compose(compose(a, g), h), codomain(X))), compose(compose(compose(a, g), h), codomain(X))) -> compose(compose(compose(a, g), h), codomain(X)) % 2.52/2.74 799: ifeq(codomain(g), domain(X), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(h, domain(X))), compose(compose(compose(a, b), h), domain(X))), compose(compose(compose(a, b), h), domain(X))) -> compose(compose(compose(a, b), h), domain(X)) % 2.52/2.74 800: ifeq(codomain(g), domain(X), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(h, domain(X))), compose(compose(compose(a, g), h), domain(X))), compose(compose(compose(a, g), h), domain(X))) -> compose(compose(compose(a, g), h), domain(X)) % 2.52/2.74 801: ifeq(codomain(b), domain(X), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(b, domain(X))), compose(compose(compose(a, g), b), domain(X))), compose(compose(compose(a, g), b), domain(X))) -> compose(compose(compose(a, g), b), domain(X)) % 2.52/2.74 802: ifeq(codomain(b), domain(X), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(b, domain(X))), compose(compose(compose(a, b), b), domain(X))), compose(compose(compose(a, b), b), domain(X))) -> compose(compose(compose(a, b), b), domain(X)) % 2.52/2.74 803: ifeq(codomain(g), domain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(g, compose(a, b))), compose(compose(codomain(X), g), compose(a, b))), compose(compose(codomain(X), g), compose(a, b))) -> compose(compose(codomain(X), g), compose(a, b)) % 2.52/2.74 804: ifeq(codomain(g), domain(X), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(g, domain(X))), compose(compose(compose(a, g), g), domain(X))), compose(compose(compose(a, g), g), domain(X))) -> compose(compose(compose(a, g), g), domain(X)) % 2.52/2.74 805: ifeq(codomain(b), codomain(a), ifeq(domain(X), domain(a), compose(domain(X), compose(compose(a, b), g)), compose(compose(domain(X), compose(a, b)), g)), compose(compose(domain(X), compose(a, b)), g)) -> compose(compose(domain(X), compose(a, b)), g) % 2.52/2.74 806: ifeq(codomain(b), codomain(a), ifeq(codomain(X), domain(a), compose(codomain(X), compose(compose(a, b), h)), compose(compose(codomain(X), compose(a, b)), h)), compose(compose(codomain(X), compose(a, b)), h)) -> compose(compose(codomain(X), compose(a, b)), h) % 2.52/2.74 807: ifeq(codomain(g), codomain(a), ifeq(codomain(X), domain(a), compose(codomain(X), compose(compose(a, g), h)), compose(compose(codomain(X), compose(a, g)), h)), compose(compose(codomain(X), compose(a, g)), h)) -> compose(compose(codomain(X), compose(a, g)), h) % 2.52/2.74 808: ifeq(codomain(b), codomain(X), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(b, codomain(X))), compose(compose(compose(a, b), b), codomain(X))), compose(compose(compose(a, b), b), codomain(X))) -> compose(compose(compose(a, b), b), codomain(X)) % 2.52/2.74 809: ifeq(codomain(g), domain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(g, compose(a, b))), compose(compose(domain(X), g), compose(a, b))), compose(compose(domain(X), g), compose(a, b))) -> compose(compose(domain(X), g), compose(a, b)) % 2.52/2.74 810: ifeq(codomain(g), codomain(X), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(g, codomain(X))), compose(compose(compose(a, b), g), codomain(X))), compose(compose(compose(a, b), g), codomain(X))) -> compose(compose(compose(a, b), g), codomain(X)) % 2.52/2.74 811: ifeq(codomain(g), domain(a), ifeq(domain(X), codomain(a), compose(domain(X), compose(h, compose(a, b))), compose(compose(domain(X), h), compose(a, b))), compose(compose(domain(X), h), compose(a, b))) -> compose(compose(domain(X), h), compose(a, b)) % 2.52/2.74 812: ifeq(codomain(g), codomain(X), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(g, codomain(X))), compose(compose(compose(a, g), g), codomain(X))), compose(compose(compose(a, g), g), codomain(X))) -> compose(compose(compose(a, g), g), codomain(X)) % 2.52/2.74 813: ifeq(codomain(b), domain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(b, compose(a, g))), compose(compose(codomain(X), b), compose(a, g))), compose(compose(codomain(X), b), compose(a, g))) -> compose(compose(codomain(X), b), compose(a, g)) % 2.52/2.74 814: ifeq(codomain(b), domain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(b, compose(a, b))), compose(compose(codomain(X), b), compose(a, b))), compose(compose(codomain(X), b), compose(a, b))) -> compose(compose(codomain(X), b), compose(a, b)) % 2.52/2.74 815: ifeq(codomain(g), domain(a), ifeq(codomain(X), codomain(a), compose(codomain(X), compose(h, compose(a, b))), compose(compose(codomain(X), h), compose(a, b))), compose(compose(codomain(X), h), compose(a, b))) -> compose(compose(codomain(X), h), compose(a, b)) % 2.52/2.74 816: ifeq(codomain(g), codomain(X), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(h, codomain(X))), compose(compose(compose(a, b), h), codomain(X))), compose(compose(compose(a, b), h), codomain(X))) -> compose(compose(compose(a, b), h), codomain(X)) % 2.52/2.74 817: ifeq(codomain(g), codomain(compose(X, compose(a, g))), ifeq(codomain(X), domain(a), compose(X, compose(compose(a, g), codomain(compose(X, compose(a, g))))), compose(X, compose(a, g))), compose(X, compose(a, g))) -> compose(X, compose(a, g)) % 2.52/2.74 818: ifeq(codomain(g), domain(X), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, g), domain(X))), compose(compose(h, compose(a, g)), domain(X))), compose(compose(h, compose(a, g)), domain(X))) -> compose(compose(h, compose(a, g)), domain(X)) % 2.52/2.74 819: ifeq(codomain(b), domain(X), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, b), domain(X))), compose(compose(h, compose(a, b)), domain(X))), compose(compose(h, compose(a, b)), domain(X))) -> compose(compose(h, compose(a, b)), domain(X)) % 2.52/2.74 820: ifeq(codomain(X), codomain(compose(compose(a, g), X)), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(X, codomain(compose(compose(a, g), X)))), compose(compose(a, g), X)), compose(compose(a, g), X)) -> compose(compose(a, g), X) % 2.52/2.74 821: ifeq(codomain(X), codomain(compose(compose(a, b), X)), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(X, codomain(compose(compose(a, b), X)))), compose(compose(a, b), X)), compose(compose(a, b), X)) -> compose(compose(a, b), X) % 2.52/2.74 822: ifeq(codomain(b), codomain(compose(X, compose(a, b))), ifeq(codomain(X), domain(a), compose(X, compose(compose(a, b), codomain(compose(X, compose(a, b))))), compose(X, compose(a, b))), compose(X, compose(a, b))) -> compose(X, compose(a, b)) % 2.52/2.74 823: ifeq(codomain(X), codomain(Y), ifeq(domain(compose(X, codomain(Y))), domain(X), compose(X, codomain(Y)), compose(compose(domain(compose(X, codomain(Y))), X), codomain(Y))), compose(compose(domain(compose(X, codomain(Y))), X), codomain(Y))) -> compose(compose(domain(compose(X, codomain(Y))), X), codomain(Y)) % 2.52/2.74 824: ifeq(domain(X), domain(Y), ifeq(domain(compose(domain(X), Y)), domain(X), compose(domain(X), Y), compose(compose(domain(compose(domain(X), Y)), domain(X)), Y)), compose(compose(domain(compose(domain(X), Y)), domain(X)), Y)) -> compose(compose(domain(compose(domain(X), Y)), domain(X)), Y) % 2.52/2.74 825: ifeq(codomain(X), domain(Y), ifeq(domain(compose(codomain(X), Y)), codomain(X), compose(codomain(X), Y), compose(compose(domain(compose(codomain(X), Y)), codomain(X)), Y)), compose(compose(domain(compose(codomain(X), Y)), codomain(X)), Y)) -> compose(compose(domain(compose(codomain(X), Y)), codomain(X)), Y) % 2.52/2.74 826: ifeq(codomain(X), domain(Y), ifeq(domain(compose(X, domain(Y))), domain(X), compose(X, domain(Y)), compose(compose(domain(compose(X, domain(Y))), X), domain(Y))), compose(compose(domain(compose(X, domain(Y))), X), domain(Y))) -> compose(compose(domain(compose(X, domain(Y))), X), domain(Y)) % 2.52/2.74 827: ifeq(codomain(g), codomain(compose(compose(a, b), h)), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(h, codomain(compose(compose(a, b), h)))), compose(compose(a, b), h)), compose(compose(a, b), h)) -> compose(compose(a, b), h) % 2.52/2.74 828: ifeq(codomain(g), codomain(compose(compose(a, g), h)), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(h, codomain(compose(compose(a, g), h)))), compose(compose(a, g), h)), compose(compose(a, g), h)) -> compose(compose(a, g), h) % 2.52/2.74 829: ifeq(codomain(b), codomain(compose(compose(a, b), b)), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(b, codomain(compose(compose(a, b), b)))), compose(compose(a, b), b)), compose(compose(a, b), b)) -> compose(compose(a, b), b) % 2.52/2.74 830: ifeq(codomain(b), codomain(compose(h, compose(a, b))), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, b), codomain(compose(h, compose(a, b))))), compose(h, compose(a, b))), compose(h, compose(a, b))) -> compose(h, compose(a, b)) % 2.52/2.74 831: ifeq(codomain(g), codomain(compose(h, compose(a, g))), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, g), codomain(compose(h, compose(a, g))))), compose(h, compose(a, g))), compose(h, compose(a, g))) -> compose(h, compose(a, g)) % 2.52/2.74 832: ifeq(codomain(g), codomain(compose(compose(a, b), g)), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(g, codomain(compose(compose(a, b), g)))), compose(compose(a, b), g)), compose(compose(a, b), g)) -> compose(compose(a, b), g) % 2.52/2.74 833: ifeq(codomain(g), codomain(compose(compose(a, g), g)), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(g, codomain(compose(compose(a, g), g)))), compose(compose(a, g), g)), compose(compose(a, g), g)) -> compose(compose(a, g), g) % 2.52/2.74 834: ifeq(codomain(b), codomain(compose(compose(a, g), b)), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(b, codomain(compose(compose(a, g), b)))), compose(compose(a, g), b)), compose(compose(a, g), b)) -> compose(compose(a, g), b) % 2.52/2.74 835: ifeq(domain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(domain(X), compose(a, b)), Y, ifeq(compose(compose(a, g), compose(a, b)), Y, compose(a, g), domain(X)), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 836: ifeq(domain(X), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(domain(X), compose(a, b)), Y, ifeq(compose(compose(a, b), compose(a, b)), Y, compose(a, b), domain(X)), domain(X)), domain(X)), domain(X)) -> domain(X) % 2.52/2.74 837: ifeq(codomain(X), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(codomain(X), compose(a, b)), Y, ifeq(compose(compose(a, b), compose(a, b)), Y, compose(a, b), codomain(X)), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 838: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(codomain(X), compose(a, b)), Y, ifeq(compose(compose(a, g), compose(a, b)), Y, compose(a, g), codomain(X)), codomain(X)), codomain(X)), codomain(X)) -> codomain(X) % 2.52/2.74 839: ifeq(codomain(X), codomain(Y), ifeq(codomain(g), codomain(X), compose(compose(a, g), compose(codomain(X), codomain(Y))), compose(compose(compose(a, g), codomain(X)), codomain(Y))), compose(compose(compose(a, g), codomain(X)), codomain(Y))) -> compose(compose(compose(a, g), codomain(X)), codomain(Y)) % 2.52/2.74 840: ifeq(codomain(X), domain(a), ifeq(codomain(Y), codomain(X), compose(codomain(Y), compose(codomain(X), compose(a, b))), compose(compose(codomain(Y), codomain(X)), compose(a, b))), compose(compose(codomain(Y), codomain(X)), compose(a, b))) -> compose(compose(codomain(Y), codomain(X)), compose(a, b)) % 2.52/2.74 841: ifeq(codomain(X), domain(a), ifeq(codomain(Y), codomain(X), compose(codomain(Y), compose(codomain(X), compose(a, g))), compose(compose(codomain(Y), codomain(X)), compose(a, g))), compose(compose(codomain(Y), codomain(X)), compose(a, g))) -> compose(compose(codomain(Y), codomain(X)), compose(a, g)) % 2.52/2.74 842: ifeq(domain(X), domain(a), ifeq(domain(Y), domain(X), compose(domain(Y), compose(domain(X), compose(a, b))), compose(compose(domain(Y), domain(X)), compose(a, b))), compose(compose(domain(Y), domain(X)), compose(a, b))) -> compose(compose(domain(Y), domain(X)), compose(a, b)) % 2.52/2.74 843: ifeq(codomain(X), domain(Y), ifeq(codomain(g), codomain(X), compose(compose(a, g), compose(codomain(X), domain(Y))), compose(compose(compose(a, g), codomain(X)), domain(Y))), compose(compose(compose(a, g), codomain(X)), domain(Y))) -> compose(compose(compose(a, g), codomain(X)), domain(Y)) % 2.52/2.74 844: ifeq(codomain(X), domain(a), ifeq(domain(Y), codomain(X), compose(domain(Y), compose(codomain(X), compose(a, g))), compose(compose(domain(Y), codomain(X)), compose(a, g))), compose(compose(domain(Y), codomain(X)), compose(a, g))) -> compose(compose(domain(Y), codomain(X)), compose(a, g)) % 2.52/2.74 845: ifeq(domain(X), domain(a), ifeq(codomain(Y), domain(X), compose(codomain(Y), compose(domain(X), compose(a, g))), compose(compose(codomain(Y), domain(X)), compose(a, g))), compose(compose(codomain(Y), domain(X)), compose(a, g))) -> compose(compose(codomain(Y), domain(X)), compose(a, g)) % 2.52/2.74 846: ifeq(codomain(X), domain(Y), ifeq(codomain(b), codomain(X), compose(compose(a, b), compose(codomain(X), domain(Y))), compose(compose(compose(a, b), codomain(X)), domain(Y))), compose(compose(compose(a, b), codomain(X)), domain(Y))) -> compose(compose(compose(a, b), codomain(X)), domain(Y)) % 2.52/2.74 847: ifeq(codomain(X), domain(a), ifeq(domain(Y), codomain(X), compose(domain(Y), compose(codomain(X), compose(a, b))), compose(compose(domain(Y), codomain(X)), compose(a, b))), compose(compose(domain(Y), codomain(X)), compose(a, b))) -> compose(compose(domain(Y), codomain(X)), compose(a, b)) % 2.52/2.74 848: ifeq(domain(X), domain(a), ifeq(domain(Y), domain(X), compose(domain(Y), compose(domain(X), compose(a, g))), compose(compose(domain(Y), domain(X)), compose(a, g))), compose(compose(domain(Y), domain(X)), compose(a, g))) -> compose(compose(domain(Y), domain(X)), compose(a, g)) % 2.52/2.74 849: ifeq(codomain(X), codomain(Y), ifeq(codomain(b), codomain(X), compose(compose(a, b), compose(codomain(X), codomain(Y))), compose(compose(compose(a, b), codomain(X)), codomain(Y))), compose(compose(compose(a, b), codomain(X)), codomain(Y))) -> compose(compose(compose(a, b), codomain(X)), codomain(Y)) % 2.52/2.74 850: ifeq(domain(X), codomain(Y), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(domain(X), codomain(Y))), compose(compose(compose(a, b), domain(X)), codomain(Y))), compose(compose(compose(a, b), domain(X)), codomain(Y))) -> compose(compose(compose(a, b), domain(X)), codomain(Y)) % 2.52/2.74 851: ifeq(domain(X), codomain(Y), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(domain(X), codomain(Y))), compose(compose(compose(a, g), domain(X)), codomain(Y))), compose(compose(compose(a, g), domain(X)), codomain(Y))) -> compose(compose(compose(a, g), domain(X)), codomain(Y)) % 2.52/2.74 852: ifeq(domain(X), domain(Y), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(domain(X), domain(Y))), compose(compose(compose(a, b), domain(X)), domain(Y))), compose(compose(compose(a, b), domain(X)), domain(Y))) -> compose(compose(compose(a, b), domain(X)), domain(Y)) % 2.52/2.74 853: ifeq(domain(X), domain(Y), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(domain(X), domain(Y))), compose(compose(compose(a, g), domain(X)), domain(Y))), compose(compose(compose(a, g), domain(X)), domain(Y))) -> compose(compose(compose(a, g), domain(X)), domain(Y)) % 2.52/2.74 854: ifeq(domain(X), domain(a), ifeq(codomain(Y), domain(X), compose(codomain(Y), compose(domain(X), compose(a, b))), compose(compose(codomain(Y), domain(X)), compose(a, b))), compose(compose(codomain(Y), domain(X)), compose(a, b))) -> compose(compose(codomain(Y), domain(X)), compose(a, b)) % 2.52/2.74 855: ifeq(codomain(g), codomain(X), ifeq(codomain(Y), domain(a), compose(codomain(Y), compose(compose(a, g), codomain(X))), compose(compose(codomain(Y), compose(a, g)), codomain(X))), compose(compose(codomain(Y), compose(a, g)), codomain(X))) -> compose(compose(codomain(Y), compose(a, g)), codomain(X)) % 2.52/2.74 856: ifeq(codomain(b), codomain(X), ifeq(codomain(Y), domain(a), compose(codomain(Y), compose(compose(a, b), codomain(X))), compose(compose(codomain(Y), compose(a, b)), codomain(X))), compose(compose(codomain(Y), compose(a, b)), codomain(X))) -> compose(compose(codomain(Y), compose(a, b)), codomain(X)) % 2.52/2.74 857: ifeq(codomain(g), codomain(X), ifeq(domain(Y), domain(a), compose(domain(Y), compose(compose(a, g), codomain(X))), compose(compose(domain(Y), compose(a, g)), codomain(X))), compose(compose(domain(Y), compose(a, g)), codomain(X))) -> compose(compose(domain(Y), compose(a, g)), codomain(X)) % 2.52/2.74 858: ifeq(codomain(g), domain(X), ifeq(domain(Y), domain(a), compose(domain(Y), compose(compose(a, g), domain(X))), compose(compose(domain(Y), compose(a, g)), domain(X))), compose(compose(domain(Y), compose(a, g)), domain(X))) -> compose(compose(domain(Y), compose(a, g)), domain(X)) % 2.52/2.74 859: ifeq(codomain(b), domain(X), ifeq(domain(Y), domain(a), compose(domain(Y), compose(compose(a, b), domain(X))), compose(compose(domain(Y), compose(a, b)), domain(X))), compose(compose(domain(Y), compose(a, b)), domain(X))) -> compose(compose(domain(Y), compose(a, b)), domain(X)) % 2.52/2.74 860: ifeq(codomain(b), codomain(X), ifeq(domain(Y), domain(a), compose(domain(Y), compose(compose(a, b), codomain(X))), compose(compose(domain(Y), compose(a, b)), codomain(X))), compose(compose(domain(Y), compose(a, b)), codomain(X))) -> compose(compose(domain(Y), compose(a, b)), codomain(X)) % 2.52/2.74 861: ifeq(codomain(X), codomain(a), ifeq(domain(compose(codomain(X), h)), codomain(X), compose(codomain(X), h), compose(compose(domain(compose(codomain(X), h)), codomain(X)), h)), compose(compose(domain(compose(codomain(X), h)), codomain(X)), h)) -> compose(compose(domain(compose(codomain(X), h)), codomain(X)), h) % 2.52/2.74 862: ifeq(domain(X), codomain(a), ifeq(domain(compose(domain(X), h)), domain(X), compose(domain(X), h), compose(compose(domain(compose(domain(X), h)), domain(X)), h)), compose(compose(domain(compose(domain(X), h)), domain(X)), h)) -> compose(compose(domain(compose(domain(X), h)), domain(X)), h) % 2.52/2.74 863: ifeq(domain(X), codomain(a), ifeq(domain(compose(domain(X), g)), domain(X), compose(domain(X), g), compose(compose(domain(compose(domain(X), g)), domain(X)), g)), compose(compose(domain(compose(domain(X), g)), domain(X)), g)) -> compose(compose(domain(compose(domain(X), g)), domain(X)), g) % 2.52/2.74 864: ifeq(domain(X), codomain(a), ifeq(domain(compose(domain(X), b)), domain(X), compose(domain(X), b), compose(compose(domain(compose(domain(X), b)), domain(X)), b)), compose(compose(domain(compose(domain(X), b)), domain(X)), b)) -> compose(compose(domain(compose(domain(X), b)), domain(X)), b) % 2.52/2.74 865: ifeq(codomain(X), codomain(a), ifeq(domain(compose(codomain(X), g)), codomain(X), compose(codomain(X), g), compose(compose(domain(compose(codomain(X), g)), codomain(X)), g)), compose(compose(domain(compose(codomain(X), g)), codomain(X)), g)) -> compose(compose(domain(compose(codomain(X), g)), codomain(X)), g) % 2.52/2.74 866: ifeq(codomain(X), codomain(a), ifeq(domain(compose(codomain(X), b)), codomain(X), compose(codomain(X), b), compose(compose(domain(compose(codomain(X), b)), codomain(X)), b)), compose(compose(domain(compose(codomain(X), b)), codomain(X)), b)) -> compose(compose(domain(compose(codomain(X), b)), codomain(X)), b) % 2.52/2.74 867: ifeq(codomain(g), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(compose(a, b), compose(a, b)), compose(compose(a, g), compose(a, b)), compose(a, b), compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 868: ifeq(codomain(g), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(compose(a, g), compose(a, b)), compose(compose(a, b), compose(a, b)), compose(a, b), compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 869: ifeq(codomain(b), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(compose(a, g), compose(a, b)), compose(compose(a, b), compose(a, b)), compose(a, g), compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 870: ifeq(codomain(b), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(compose(a, b), compose(a, b)), compose(compose(a, g), compose(a, b)), compose(a, g), compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 871: ifeq(codomain(b), codomain(X), ifeq(domain(compose(b, codomain(X))), codomain(a), compose(b, codomain(X)), compose(compose(domain(compose(b, codomain(X))), b), codomain(X))), compose(compose(domain(compose(b, codomain(X))), b), codomain(X))) -> compose(compose(domain(compose(b, codomain(X))), b), codomain(X)) % 2.52/2.74 872: ifeq(codomain(g), codomain(X), ifeq(domain(compose(h, codomain(X))), codomain(a), compose(h, codomain(X)), compose(compose(domain(compose(h, codomain(X))), h), codomain(X))), compose(compose(domain(compose(h, codomain(X))), h), codomain(X))) -> compose(compose(domain(compose(h, codomain(X))), h), codomain(X)) % 2.52/2.74 873: ifeq(codomain(g), domain(X), ifeq(domain(compose(h, domain(X))), codomain(a), compose(h, domain(X)), compose(compose(domain(compose(h, domain(X))), h), domain(X))), compose(compose(domain(compose(h, domain(X))), h), domain(X))) -> compose(compose(domain(compose(h, domain(X))), h), domain(X)) % 2.52/2.74 874: ifeq(codomain(b), domain(X), ifeq(domain(compose(b, domain(X))), codomain(a), compose(b, domain(X)), compose(compose(domain(compose(b, domain(X))), b), domain(X))), compose(compose(domain(compose(b, domain(X))), b), domain(X))) -> compose(compose(domain(compose(b, domain(X))), b), domain(X)) % 2.52/2.74 875: ifeq(codomain(g), domain(X), ifeq(domain(compose(g, domain(X))), codomain(a), compose(g, domain(X)), compose(compose(domain(compose(g, domain(X))), g), domain(X))), compose(compose(domain(compose(g, domain(X))), g), domain(X))) -> compose(compose(domain(compose(g, domain(X))), g), domain(X)) % 2.52/2.74 876: ifeq(codomain(g), codomain(X), ifeq(domain(compose(g, codomain(X))), codomain(a), compose(g, codomain(X)), compose(compose(domain(compose(g, codomain(X))), g), codomain(X))), compose(compose(domain(compose(g, codomain(X))), g), codomain(X))) -> compose(compose(domain(compose(g, codomain(X))), g), codomain(X)) % 2.52/2.74 877: ifeq(codomain(X), domain(a), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(X, compose(a, g))), compose(compose(compose(a, b), X), compose(a, g))), compose(compose(compose(a, b), X), compose(a, g))) -> compose(compose(compose(a, b), X), compose(a, g)) % 2.52/2.74 878: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(X, compose(a, g))), compose(compose(compose(a, g), X), compose(a, g))), compose(compose(compose(a, g), X), compose(a, g))) -> compose(compose(compose(a, g), X), compose(a, g)) % 2.52/2.74 879: ifeq(codomain(g), domain(X), ifeq(codomain(Y), domain(a), compose(codomain(Y), compose(compose(a, g), domain(X))), compose(compose(codomain(Y), compose(a, g)), domain(X))), compose(compose(codomain(Y), compose(a, g)), domain(X))) -> compose(compose(codomain(Y), compose(a, g)), domain(X)) % 2.52/2.74 880: ifeq(codomain(b), domain(X), ifeq(codomain(Y), domain(a), compose(codomain(Y), compose(compose(a, b), domain(X))), compose(compose(codomain(Y), compose(a, b)), domain(X))), compose(compose(codomain(Y), compose(a, b)), domain(X))) -> compose(compose(codomain(Y), compose(a, b)), domain(X)) % 2.52/2.74 881: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), compose(X, compose(compose(a, g), compose(a, g))), compose(compose(X, compose(a, g)), compose(a, g))), compose(compose(X, compose(a, g)), compose(a, g))) -> compose(compose(X, compose(a, g)), compose(a, g)) % 2.52/2.74 882: ifeq(codomain(b), domain(a), ifeq(codomain(X), domain(a), compose(X, compose(compose(a, b), compose(a, g))), compose(compose(X, compose(a, b)), compose(a, g))), compose(compose(X, compose(a, b)), compose(a, g))) -> compose(compose(X, compose(a, b)), compose(a, g)) % 2.52/2.74 883: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), compose(X, compose(compose(a, g), compose(a, b))), compose(compose(X, compose(a, g)), compose(a, b))), compose(compose(X, compose(a, g)), compose(a, b))) -> compose(compose(X, compose(a, g)), compose(a, b)) % 2.52/2.74 884: ifeq(codomain(g), domain(X), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, g), X)), compose(compose(compose(a, b), compose(a, g)), X)), compose(compose(compose(a, b), compose(a, g)), X)) -> compose(compose(compose(a, b), compose(a, g)), X) % 2.52/2.74 885: ifeq(codomain(g), domain(X), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, g), X)), compose(compose(compose(a, g), compose(a, g)), X)), compose(compose(compose(a, g), compose(a, g)), X)) -> compose(compose(compose(a, g), compose(a, g)), X) % 2.52/2.74 886: ifeq(codomain(b), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(compose(a, b), compose(a, b)), Y, ifeq(compose(X, compose(a, b)), Y, X, compose(a, b)), compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 887: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(compose(a, g), compose(a, b)), Y, ifeq(compose(X, compose(a, b)), Y, X, compose(a, g)), compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 888: ifeq(codomain(X), domain(a), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(X, compose(a, b))), compose(compose(compose(a, g), X), compose(a, b))), compose(compose(compose(a, g), X), compose(a, b))) -> compose(compose(compose(a, g), X), compose(a, b)) % 2.52/2.74 889: ifeq(codomain(X), domain(a), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(X, compose(a, b))), compose(compose(compose(a, b), X), compose(a, b))), compose(compose(compose(a, b), X), compose(a, b))) -> compose(compose(compose(a, b), X), compose(a, b)) % 2.52/2.74 890: ifeq(codomain(b), domain(X), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, b), X)), compose(compose(compose(a, g), compose(a, b)), X)), compose(compose(compose(a, g), compose(a, b)), X)) -> compose(compose(compose(a, g), compose(a, b)), X) % 2.52/2.74 891: ifeq(codomain(b), domain(a), ifeq(codomain(X), domain(a), compose(X, compose(compose(a, b), compose(a, b))), compose(compose(X, compose(a, b)), compose(a, b))), compose(compose(X, compose(a, b)), compose(a, b))) -> compose(compose(X, compose(a, b)), compose(a, b)) % 2.52/2.74 892: ifeq(codomain(b), domain(X), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, b), X)), compose(compose(compose(a, b), compose(a, b)), X)), compose(compose(compose(a, b), compose(a, b)), X)) -> compose(compose(compose(a, b), compose(a, b)), X) % 2.52/2.74 893: ifeq(codomain(g), codomain(a), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, g), g)), compose(compose(compose(a, b), compose(a, g)), g)), compose(compose(compose(a, b), compose(a, g)), g)) -> compose(compose(compose(a, b), compose(a, g)), g) % 2.52/2.74 894: ifeq(codomain(g), codomain(a), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, g), h)), compose(compose(compose(a, b), compose(a, g)), h)), compose(compose(compose(a, b), compose(a, g)), h)) -> compose(compose(compose(a, b), compose(a, g)), h) % 2.52/2.74 895: ifeq(codomain(b), domain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(b, compose(a, g))), compose(compose(compose(a, g), b), compose(a, g))), compose(compose(compose(a, g), b), compose(a, g))) -> compose(compose(compose(a, g), b), compose(a, g)) % 2.52/2.74 896: ifeq(codomain(g), domain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(h, compose(a, g))), compose(compose(compose(a, g), h), compose(a, g))), compose(compose(compose(a, g), h), compose(a, g))) -> compose(compose(compose(a, g), h), compose(a, g)) % 2.52/2.74 897: ifeq(codomain(g), domain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(h, compose(a, g))), compose(compose(compose(a, b), h), compose(a, g))), compose(compose(compose(a, b), h), compose(a, g))) -> compose(compose(compose(a, b), h), compose(a, g)) % 2.52/2.74 898: ifeq(codomain(g), codomain(a), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, g), b)), compose(compose(compose(a, g), compose(a, g)), b)), compose(compose(compose(a, g), compose(a, g)), b)) -> compose(compose(compose(a, g), compose(a, g)), b) % 2.52/2.74 899: ifeq(codomain(g), codomain(a), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, g), h)), compose(compose(compose(a, g), compose(a, g)), h)), compose(compose(compose(a, g), compose(a, g)), h)) -> compose(compose(compose(a, g), compose(a, g)), h) % 2.52/2.74 900: ifeq(codomain(g), codomain(a), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, g), b)), compose(compose(compose(a, b), compose(a, g)), b)), compose(compose(compose(a, b), compose(a, g)), b)) -> compose(compose(compose(a, b), compose(a, g)), b) % 2.52/2.74 901: ifeq(codomain(b), domain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(b, compose(a, g))), compose(compose(compose(a, b), b), compose(a, g))), compose(compose(compose(a, b), b), compose(a, g))) -> compose(compose(compose(a, b), b), compose(a, g)) % 2.52/2.74 902: ifeq(codomain(g), codomain(a), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, g), g)), compose(compose(compose(a, g), compose(a, g)), g)), compose(compose(compose(a, g), compose(a, g)), g)) -> compose(compose(compose(a, g), compose(a, g)), g) % 2.52/2.74 903: ifeq(codomain(g), domain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(g, compose(a, g))), compose(compose(compose(a, b), g), compose(a, g))), compose(compose(compose(a, b), g), compose(a, g))) -> compose(compose(compose(a, b), g), compose(a, g)) % 2.52/2.74 904: ifeq(codomain(g), domain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(g, compose(a, g))), compose(compose(compose(a, g), g), compose(a, g))), compose(compose(compose(a, g), g), compose(a, g))) -> compose(compose(compose(a, g), g), compose(a, g)) % 2.52/2.74 905: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(compose(a, g), compose(a, b)), X, ifeq(compose(h, compose(a, b)), X, h, compose(a, g)), compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 906: ifeq(codomain(b), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(compose(a, b), compose(a, b)), X, ifeq(compose(h, compose(a, b)), X, h, compose(a, b)), compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 907: ifeq(codomain(b), codomain(a), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, b), b)), compose(compose(compose(a, g), compose(a, b)), b)), compose(compose(compose(a, g), compose(a, b)), b)) -> compose(compose(compose(a, g), compose(a, b)), b) % 2.52/2.74 908: ifeq(codomain(b), domain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(b, compose(a, b))), compose(compose(compose(a, b), b), compose(a, b))), compose(compose(compose(a, b), b), compose(a, b))) -> compose(compose(compose(a, b), b), compose(a, b)) % 2.52/2.74 909: ifeq(codomain(g), domain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(h, compose(a, b))), compose(compose(compose(a, b), h), compose(a, b))), compose(compose(compose(a, b), h), compose(a, b))) -> compose(compose(compose(a, b), h), compose(a, b)) % 2.52/2.74 910: ifeq(codomain(g), domain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(h, compose(a, b))), compose(compose(compose(a, g), h), compose(a, b))), compose(compose(compose(a, g), h), compose(a, b))) -> compose(compose(compose(a, g), h), compose(a, b)) % 2.52/2.74 911: ifeq(codomain(b), codomain(a), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, b), h)), compose(compose(compose(a, b), compose(a, b)), h)), compose(compose(compose(a, b), compose(a, b)), h)) -> compose(compose(compose(a, b), compose(a, b)), h) % 2.52/2.74 912: ifeq(codomain(g), domain(a), ifeq(codomain(b), codomain(a), compose(compose(a, b), compose(g, compose(a, b))), compose(compose(compose(a, b), g), compose(a, b))), compose(compose(compose(a, b), g), compose(a, b))) -> compose(compose(compose(a, b), g), compose(a, b)) % 2.52/2.74 913: ifeq(codomain(b), codomain(a), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, b), g)), compose(compose(compose(a, g), compose(a, b)), g)), compose(compose(compose(a, g), compose(a, b)), g)) -> compose(compose(compose(a, g), compose(a, b)), g) % 2.52/2.74 914: ifeq(codomain(b), codomain(a), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, b), g)), compose(compose(compose(a, b), compose(a, b)), g)), compose(compose(compose(a, b), compose(a, b)), g)) -> compose(compose(compose(a, b), compose(a, b)), g) % 2.52/2.74 915: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, g), compose(a, b))), compose(compose(h, compose(a, g)), compose(a, b))), compose(compose(h, compose(a, g)), compose(a, b))) -> compose(compose(h, compose(a, g)), compose(a, b)) % 2.52/2.74 916: ifeq(codomain(b), codomain(a), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, b), b)), compose(compose(compose(a, b), compose(a, b)), b)), compose(compose(compose(a, b), compose(a, b)), b)) -> compose(compose(compose(a, b), compose(a, b)), b) % 2.52/2.74 917: ifeq(codomain(g), domain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(g, compose(a, b))), compose(compose(compose(a, g), g), compose(a, b))), compose(compose(compose(a, g), g), compose(a, b))) -> compose(compose(compose(a, g), g), compose(a, b)) % 2.52/2.74 918: ifeq(codomain(b), codomain(a), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, b), h)), compose(compose(compose(a, g), compose(a, b)), h)), compose(compose(compose(a, g), compose(a, b)), h)) -> compose(compose(compose(a, g), compose(a, b)), h) % 2.52/2.74 919: ifeq(codomain(b), domain(a), ifeq(codomain(g), codomain(a), compose(compose(a, g), compose(b, compose(a, b))), compose(compose(compose(a, g), b), compose(a, b))), compose(compose(compose(a, g), b), compose(a, b))) -> compose(compose(compose(a, g), b), compose(a, b)) % 2.52/2.74 920: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, g), compose(a, g))), compose(compose(h, compose(a, g)), compose(a, g))), compose(compose(h, compose(a, g)), compose(a, g))) -> compose(compose(h, compose(a, g)), compose(a, g)) % 2.52/2.74 921: ifeq(codomain(b), domain(a), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, b), compose(a, b))), compose(compose(h, compose(a, b)), compose(a, b))), compose(compose(h, compose(a, b)), compose(a, b))) -> compose(compose(h, compose(a, b)), compose(a, b)) % 2.52/2.74 922: ifeq(codomain(b), domain(a), ifeq(codomain(g), domain(a), compose(h, compose(compose(a, b), compose(a, g))), compose(compose(h, compose(a, b)), compose(a, g))), compose(compose(h, compose(a, b)), compose(a, g))) -> compose(compose(h, compose(a, b)), compose(a, g)) % 2.52/2.74 923: ifeq(codomain(b), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(compose(a, b), compose(a, b)), Y, ifeq(compose(codomain(X), compose(a, b)), Y, codomain(X), compose(a, b)), compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 924: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), ifeq(compose(compose(a, g), compose(a, b)), Y, ifeq(compose(codomain(X), compose(a, b)), Y, codomain(X), compose(a, g)), compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 925: ifeq(codomain(b), domain(a), ifeq(domain(X), domain(a), ifeq(compose(compose(a, b), compose(a, b)), Y, ifeq(compose(domain(X), compose(a, b)), Y, domain(X), compose(a, b)), compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 926: ifeq(codomain(g), domain(a), ifeq(domain(X), domain(a), ifeq(compose(compose(a, g), compose(a, b)), Y, ifeq(compose(domain(X), compose(a, b)), Y, domain(X), compose(a, g)), compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 927: ifeq(codomain(X), codomain(compose(compose(a, g), codomain(X))), ifeq(codomain(g), codomain(X), compose(compose(a, g), compose(codomain(X), codomain(compose(compose(a, g), codomain(X))))), compose(compose(a, g), codomain(X))), compose(compose(a, g), codomain(X))) -> compose(compose(a, g), codomain(X)) % 2.52/2.74 928: ifeq(domain(X), codomain(compose(compose(a, b), domain(X))), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(domain(X), codomain(compose(compose(a, b), domain(X))))), compose(compose(a, b), domain(X))), compose(compose(a, b), domain(X))) -> compose(compose(a, b), domain(X)) % 2.52/2.74 929: ifeq(domain(X), codomain(compose(compose(a, g), domain(X))), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(domain(X), codomain(compose(compose(a, g), domain(X))))), compose(compose(a, g), domain(X))), compose(compose(a, g), domain(X))) -> compose(compose(a, g), domain(X)) % 2.52/2.74 930: ifeq(codomain(X), codomain(compose(compose(a, b), codomain(X))), ifeq(codomain(b), codomain(X), compose(compose(a, b), compose(codomain(X), codomain(compose(compose(a, b), codomain(X))))), compose(compose(a, b), codomain(X))), compose(compose(a, b), codomain(X))) -> compose(compose(a, b), codomain(X)) % 2.52/2.74 931: ifeq(codomain(g), codomain(compose(domain(X), compose(a, g))), ifeq(domain(X), domain(a), compose(domain(X), compose(compose(a, g), codomain(compose(domain(X), compose(a, g))))), compose(domain(X), compose(a, g))), compose(domain(X), compose(a, g))) -> compose(domain(X), compose(a, g)) % 2.52/2.74 932: ifeq(codomain(b), codomain(compose(codomain(X), compose(a, b))), ifeq(codomain(X), domain(a), compose(codomain(X), compose(compose(a, b), codomain(compose(codomain(X), compose(a, b))))), compose(codomain(X), compose(a, b))), compose(codomain(X), compose(a, b))) -> compose(codomain(X), compose(a, b)) % 2.52/2.74 933: ifeq(codomain(g), codomain(compose(codomain(X), compose(a, g))), ifeq(codomain(X), domain(a), compose(codomain(X), compose(compose(a, g), codomain(compose(codomain(X), compose(a, g))))), compose(codomain(X), compose(a, g))), compose(codomain(X), compose(a, g))) -> compose(codomain(X), compose(a, g)) % 2.52/2.74 934: ifeq(codomain(b), codomain(compose(domain(X), compose(a, b))), ifeq(domain(X), domain(a), compose(domain(X), compose(compose(a, b), codomain(compose(domain(X), compose(a, b))))), compose(domain(X), compose(a, b))), compose(domain(X), compose(a, b))) -> compose(domain(X), compose(a, b)) % 2.52/2.74 935: ifeq(codomain(X), domain(a), ifeq(codomain(g), codomain(X), compose(compose(a, g), compose(codomain(X), compose(a, g))), compose(compose(compose(a, g), codomain(X)), compose(a, g))), compose(compose(compose(a, g), codomain(X)), compose(a, g))) -> compose(compose(compose(a, g), codomain(X)), compose(a, g)) % 2.52/2.74 936: ifeq(domain(X), domain(a), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(domain(X), compose(a, g))), compose(compose(compose(a, b), domain(X)), compose(a, g))), compose(compose(compose(a, b), domain(X)), compose(a, g))) -> compose(compose(compose(a, b), domain(X)), compose(a, g)) % 2.52/2.74 937: ifeq(domain(X), domain(a), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(domain(X), compose(a, g))), compose(compose(compose(a, g), domain(X)), compose(a, g))), compose(compose(compose(a, g), domain(X)), compose(a, g))) -> compose(compose(compose(a, g), domain(X)), compose(a, g)) % 2.52/2.74 938: ifeq(codomain(X), domain(a), ifeq(codomain(b), codomain(X), compose(compose(a, b), compose(codomain(X), compose(a, g))), compose(compose(compose(a, b), codomain(X)), compose(a, g))), compose(compose(compose(a, b), codomain(X)), compose(a, g))) -> compose(compose(compose(a, b), codomain(X)), compose(a, g)) % 2.52/2.74 939: ifeq(codomain(g), domain(a), ifeq(domain(X), domain(a), compose(domain(X), compose(compose(a, g), compose(a, g))), compose(compose(domain(X), compose(a, g)), compose(a, g))), compose(compose(domain(X), compose(a, g)), compose(a, g))) -> compose(compose(domain(X), compose(a, g)), compose(a, g)) % 2.52/2.74 940: ifeq(codomain(b), domain(a), ifeq(domain(X), domain(a), compose(domain(X), compose(compose(a, b), compose(a, g))), compose(compose(domain(X), compose(a, b)), compose(a, g))), compose(compose(domain(X), compose(a, b)), compose(a, g))) -> compose(compose(domain(X), compose(a, b)), compose(a, g)) % 2.52/2.74 941: ifeq(codomain(g), codomain(X), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, g), codomain(X))), compose(compose(compose(a, b), compose(a, g)), codomain(X))), compose(compose(compose(a, b), compose(a, g)), codomain(X))) -> compose(compose(compose(a, b), compose(a, g)), codomain(X)) % 2.52/2.74 942: ifeq(codomain(g), domain(a), ifeq(domain(X), domain(a), compose(domain(X), compose(compose(a, g), compose(a, b))), compose(compose(domain(X), compose(a, g)), compose(a, b))), compose(compose(domain(X), compose(a, g)), compose(a, b))) -> compose(compose(domain(X), compose(a, g)), compose(a, b)) % 2.52/2.74 943: ifeq(codomain(g), codomain(X), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, g), codomain(X))), compose(compose(compose(a, g), compose(a, g)), codomain(X))), compose(compose(compose(a, g), compose(a, g)), codomain(X))) -> compose(compose(compose(a, g), compose(a, g)), codomain(X)) % 2.52/2.74 944: ifeq(domain(X), domain(a), ifeq(codomain(g), domain(X), compose(compose(a, g), compose(domain(X), compose(a, b))), compose(compose(compose(a, g), domain(X)), compose(a, b))), compose(compose(compose(a, g), domain(X)), compose(a, b))) -> compose(compose(compose(a, g), domain(X)), compose(a, b)) % 2.52/2.74 945: ifeq(codomain(X), domain(a), ifeq(codomain(b), codomain(X), compose(compose(a, b), compose(codomain(X), compose(a, b))), compose(compose(compose(a, b), codomain(X)), compose(a, b))), compose(compose(compose(a, b), codomain(X)), compose(a, b))) -> compose(compose(compose(a, b), codomain(X)), compose(a, b)) % 2.52/2.74 946: ifeq(codomain(X), domain(a), ifeq(codomain(g), codomain(X), compose(compose(a, g), compose(codomain(X), compose(a, b))), compose(compose(compose(a, g), codomain(X)), compose(a, b))), compose(compose(compose(a, g), codomain(X)), compose(a, b))) -> compose(compose(compose(a, g), codomain(X)), compose(a, b)) % 2.52/2.74 947: ifeq(domain(X), domain(a), ifeq(codomain(b), domain(X), compose(compose(a, b), compose(domain(X), compose(a, b))), compose(compose(compose(a, b), domain(X)), compose(a, b))), compose(compose(compose(a, b), domain(X)), compose(a, b))) -> compose(compose(compose(a, b), domain(X)), compose(a, b)) % 2.52/2.74 948: ifeq(codomain(b), codomain(X), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, b), codomain(X))), compose(compose(compose(a, b), compose(a, b)), codomain(X))), compose(compose(compose(a, b), compose(a, b)), codomain(X))) -> compose(compose(compose(a, b), compose(a, b)), codomain(X)) % 2.52/2.74 949: ifeq(codomain(b), codomain(X), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, b), codomain(X))), compose(compose(compose(a, g), compose(a, b)), codomain(X))), compose(compose(compose(a, g), compose(a, b)), codomain(X))) -> compose(compose(compose(a, g), compose(a, b)), codomain(X)) % 2.52/2.74 950: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), compose(codomain(X), compose(compose(a, g), compose(a, b))), compose(compose(codomain(X), compose(a, g)), compose(a, b))), compose(compose(codomain(X), compose(a, g)), compose(a, b))) -> compose(compose(codomain(X), compose(a, g)), compose(a, b)) % 2.52/2.74 951: ifeq(codomain(g), domain(a), ifeq(codomain(X), domain(a), compose(codomain(X), compose(compose(a, g), compose(a, g))), compose(compose(codomain(X), compose(a, g)), compose(a, g))), compose(compose(codomain(X), compose(a, g)), compose(a, g))) -> compose(compose(codomain(X), compose(a, g)), compose(a, g)) % 2.52/2.74 952: ifeq(codomain(b), domain(X), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, b), domain(X))), compose(compose(compose(a, g), compose(a, b)), domain(X))), compose(compose(compose(a, g), compose(a, b)), domain(X))) -> compose(compose(compose(a, g), compose(a, b)), domain(X)) % 2.52/2.74 953: ifeq(codomain(g), domain(X), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, g), domain(X))), compose(compose(compose(a, g), compose(a, g)), domain(X))), compose(compose(compose(a, g), compose(a, g)), domain(X))) -> compose(compose(compose(a, g), compose(a, g)), domain(X)) % 2.52/2.74 954: ifeq(codomain(g), domain(X), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, g), domain(X))), compose(compose(compose(a, b), compose(a, g)), domain(X))), compose(compose(compose(a, b), compose(a, g)), domain(X))) -> compose(compose(compose(a, b), compose(a, g)), domain(X)) % 2.52/2.74 955: ifeq(codomain(b), domain(X), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, b), domain(X))), compose(compose(compose(a, b), compose(a, b)), domain(X))), compose(compose(compose(a, b), compose(a, b)), domain(X))) -> compose(compose(compose(a, b), compose(a, b)), domain(X)) % 2.52/2.74 956: ifeq(codomain(b), domain(a), ifeq(codomain(X), domain(a), compose(codomain(X), compose(compose(a, b), compose(a, b))), compose(compose(codomain(X), compose(a, b)), compose(a, b))), compose(compose(codomain(X), compose(a, b)), compose(a, b))) -> compose(compose(codomain(X), compose(a, b)), compose(a, b)) % 2.52/2.74 957: ifeq(codomain(b), domain(a), ifeq(domain(X), domain(a), compose(domain(X), compose(compose(a, b), compose(a, b))), compose(compose(domain(X), compose(a, b)), compose(a, b))), compose(compose(domain(X), compose(a, b)), compose(a, b))) -> compose(compose(domain(X), compose(a, b)), compose(a, b)) % 2.52/2.74 958: ifeq(codomain(b), domain(a), ifeq(codomain(X), domain(a), compose(codomain(X), compose(compose(a, b), compose(a, g))), compose(compose(codomain(X), compose(a, b)), compose(a, g))), compose(compose(codomain(X), compose(a, b)), compose(a, g))) -> compose(compose(codomain(X), compose(a, b)), compose(a, g)) % 2.52/2.74 959: ifeq(domain(X), codomain(Y), ifeq(domain(compose(domain(X), codomain(Y))), domain(X), compose(domain(X), codomain(Y)), compose(compose(domain(compose(domain(X), codomain(Y))), domain(X)), codomain(Y))), compose(compose(domain(compose(domain(X), codomain(Y))), domain(X)), codomain(Y))) -> compose(compose(domain(compose(domain(X), codomain(Y))), domain(X)), codomain(Y)) % 2.52/2.74 960: ifeq(domain(X), domain(Y), ifeq(domain(compose(domain(X), domain(Y))), domain(X), compose(domain(X), domain(Y)), compose(compose(domain(compose(domain(X), domain(Y))), domain(X)), domain(Y))), compose(compose(domain(compose(domain(X), domain(Y))), domain(X)), domain(Y))) -> compose(compose(domain(compose(domain(X), domain(Y))), domain(X)), domain(Y)) % 2.52/2.74 961: ifeq(codomain(X), codomain(Y), ifeq(domain(compose(codomain(X), codomain(Y))), codomain(X), compose(codomain(X), codomain(Y)), compose(compose(domain(compose(codomain(X), codomain(Y))), codomain(X)), codomain(Y))), compose(compose(domain(compose(codomain(X), codomain(Y))), codomain(X)), codomain(Y))) -> compose(compose(domain(compose(codomain(X), codomain(Y))), codomain(X)), codomain(Y)) % 2.52/2.74 962: ifeq(codomain(X), domain(Y), ifeq(domain(compose(codomain(X), domain(Y))), codomain(X), compose(codomain(X), domain(Y)), compose(compose(domain(compose(codomain(X), domain(Y))), codomain(X)), domain(Y))), compose(compose(domain(compose(codomain(X), domain(Y))), codomain(X)), domain(Y))) -> compose(compose(domain(compose(codomain(X), domain(Y))), codomain(X)), domain(Y)) % 2.52/2.74 963: ifeq(codomain(b), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(compose(a, b), compose(a, b)), X, ifeq(compose(compose(a, g), compose(a, b)), X, compose(a, g), compose(a, b)), compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 964: ifeq(codomain(b), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(compose(a, b), compose(a, b)), X, ifeq(compose(compose(a, b), compose(a, b)), X, compose(a, b), compose(a, b)), compose(a, b)), compose(a, b)), compose(a, b)) -> compose(a, b) % 2.52/2.74 965: ifeq(codomain(g), domain(a), ifeq(codomain(b), domain(a), ifeq(compose(compose(a, g), compose(a, b)), X, ifeq(compose(compose(a, b), compose(a, b)), X, compose(a, b), compose(a, g)), compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 966: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), ifeq(compose(compose(a, g), compose(a, b)), X, ifeq(compose(compose(a, g), compose(a, b)), X, compose(a, g), compose(a, g)), compose(a, g)), compose(a, g)), compose(a, g)) -> compose(a, g) % 2.52/2.74 967: ifeq(codomain(X), domain(a), ifeq(domain(compose(X, compose(a, g))), domain(X), compose(X, compose(a, g)), compose(compose(domain(compose(X, compose(a, g))), X), compose(a, g))), compose(compose(domain(compose(X, compose(a, g))), X), compose(a, g))) -> compose(compose(domain(compose(X, compose(a, g))), X), compose(a, g)) % 2.52/2.74 968: ifeq(codomain(g), domain(X), ifeq(domain(compose(compose(a, g), X)), domain(a), compose(compose(a, g), X), compose(compose(domain(compose(compose(a, g), X)), compose(a, g)), X)), compose(compose(domain(compose(compose(a, g), X)), compose(a, g)), X)) -> compose(compose(domain(compose(compose(a, g), X)), compose(a, g)), X) % 2.52/2.74 969: ifeq(codomain(X), domain(a), ifeq(domain(compose(X, compose(a, b))), domain(X), compose(X, compose(a, b)), compose(compose(domain(compose(X, compose(a, b))), X), compose(a, b))), compose(compose(domain(compose(X, compose(a, b))), X), compose(a, b))) -> compose(compose(domain(compose(X, compose(a, b))), X), compose(a, b)) % 2.52/2.74 970: ifeq(codomain(b), domain(X), ifeq(domain(compose(compose(a, b), X)), domain(a), compose(compose(a, b), X), compose(compose(domain(compose(compose(a, b), X)), compose(a, b)), X)), compose(compose(domain(compose(compose(a, b), X)), compose(a, b)), X)) -> compose(compose(domain(compose(compose(a, b), X)), compose(a, b)), X) % 2.52/2.74 971: ifeq(codomain(b), codomain(a), ifeq(domain(compose(compose(a, b), g)), domain(a), compose(compose(a, b), g), compose(compose(domain(compose(compose(a, b), g)), compose(a, b)), g)), compose(compose(domain(compose(compose(a, b), g)), compose(a, b)), g)) -> compose(compose(domain(compose(compose(a, b), g)), compose(a, b)), g) % 2.52/2.74 972: ifeq(codomain(g), codomain(a), ifeq(domain(compose(compose(a, g), h)), domain(a), compose(compose(a, g), h), compose(compose(domain(compose(compose(a, g), h)), compose(a, g)), h)), compose(compose(domain(compose(compose(a, g), h)), compose(a, g)), h)) -> compose(compose(domain(compose(compose(a, g), h)), compose(a, g)), h) % 2.52/2.74 973: ifeq(codomain(g), codomain(a), ifeq(domain(compose(compose(a, g), g)), domain(a), compose(compose(a, g), g), compose(compose(domain(compose(compose(a, g), g)), compose(a, g)), g)), compose(compose(domain(compose(compose(a, g), g)), compose(a, g)), g)) -> compose(compose(domain(compose(compose(a, g), g)), compose(a, g)), g) % 2.52/2.74 974: ifeq(codomain(g), domain(a), ifeq(domain(compose(h, compose(a, g))), codomain(a), compose(h, compose(a, g)), compose(compose(domain(compose(h, compose(a, g))), h), compose(a, g))), compose(compose(domain(compose(h, compose(a, g))), h), compose(a, g))) -> compose(compose(domain(compose(h, compose(a, g))), h), compose(a, g)) % 2.52/2.74 975: ifeq(codomain(b), codomain(a), ifeq(domain(compose(compose(a, b), h)), domain(a), compose(compose(a, b), h), compose(compose(domain(compose(compose(a, b), h)), compose(a, b)), h)), compose(compose(domain(compose(compose(a, b), h)), compose(a, b)), h)) -> compose(compose(domain(compose(compose(a, b), h)), compose(a, b)), h) % 2.52/2.74 976: ifeq(codomain(b), domain(a), ifeq(domain(compose(b, compose(a, g))), codomain(a), compose(b, compose(a, g)), compose(compose(domain(compose(b, compose(a, g))), b), compose(a, g))), compose(compose(domain(compose(b, compose(a, g))), b), compose(a, g))) -> compose(compose(domain(compose(b, compose(a, g))), b), compose(a, g)) % 2.52/2.74 977: ifeq(codomain(g), codomain(a), ifeq(domain(compose(compose(a, g), b)), domain(a), compose(compose(a, g), b), compose(compose(domain(compose(compose(a, g), b)), compose(a, g)), b)), compose(compose(domain(compose(compose(a, g), b)), compose(a, g)), b)) -> compose(compose(domain(compose(compose(a, g), b)), compose(a, g)), b) % 2.52/2.74 978: ifeq(codomain(b), codomain(a), ifeq(domain(compose(compose(a, b), b)), domain(a), compose(compose(a, b), b), compose(compose(domain(compose(compose(a, b), b)), compose(a, b)), b)), compose(compose(domain(compose(compose(a, b), b)), compose(a, b)), b)) -> compose(compose(domain(compose(compose(a, b), b)), compose(a, b)), b) % 2.52/2.74 979: ifeq(codomain(g), domain(a), ifeq(domain(compose(h, compose(a, b))), codomain(a), compose(h, compose(a, b)), compose(compose(domain(compose(h, compose(a, b))), h), compose(a, b))), compose(compose(domain(compose(h, compose(a, b))), h), compose(a, b))) -> compose(compose(domain(compose(h, compose(a, b))), h), compose(a, b)) % 2.52/2.74 980: ifeq(codomain(g), domain(a), ifeq(domain(compose(g, compose(a, g))), codomain(a), compose(g, compose(a, g)), compose(compose(domain(compose(g, compose(a, g))), g), compose(a, g))), compose(compose(domain(compose(g, compose(a, g))), g), compose(a, g))) -> compose(compose(domain(compose(g, compose(a, g))), g), compose(a, g)) % 2.52/2.74 981: ifeq(codomain(b), domain(a), ifeq(domain(compose(b, compose(a, b))), codomain(a), compose(b, compose(a, b)), compose(compose(domain(compose(b, compose(a, b))), b), compose(a, b))), compose(compose(domain(compose(b, compose(a, b))), b), compose(a, b))) -> compose(compose(domain(compose(b, compose(a, b))), b), compose(a, b)) % 2.52/2.74 982: ifeq(codomain(g), domain(a), ifeq(domain(compose(g, compose(a, b))), codomain(a), compose(g, compose(a, b)), compose(compose(domain(compose(g, compose(a, b))), g), compose(a, b))), compose(compose(domain(compose(g, compose(a, b))), g), compose(a, b))) -> compose(compose(domain(compose(g, compose(a, b))), g), compose(a, b)) % 2.52/2.74 983: ifeq(codomain(b), domain(a), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, b), compose(a, g))), compose(compose(compose(a, b), compose(a, b)), compose(a, g))), compose(compose(compose(a, b), compose(a, b)), compose(a, g))) -> compose(compose(compose(a, b), compose(a, b)), compose(a, g)) % 2.52/2.74 984: ifeq(codomain(b), domain(a), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, b), compose(a, g))), compose(compose(compose(a, g), compose(a, b)), compose(a, g))), compose(compose(compose(a, g), compose(a, b)), compose(a, g))) -> compose(compose(compose(a, g), compose(a, b)), compose(a, g)) % 2.52/2.74 985: ifeq(codomain(g), domain(a), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, g), compose(a, b))), compose(compose(compose(a, b), compose(a, g)), compose(a, b))), compose(compose(compose(a, b), compose(a, g)), compose(a, b))) -> compose(compose(compose(a, b), compose(a, g)), compose(a, b)) % 2.52/2.74 986: ifeq(codomain(g), domain(a), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, g), compose(a, g))), compose(compose(compose(a, b), compose(a, g)), compose(a, g))), compose(compose(compose(a, b), compose(a, g)), compose(a, g))) -> compose(compose(compose(a, b), compose(a, g)), compose(a, g)) % 2.52/2.74 987: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, g), compose(a, g))), compose(compose(compose(a, g), compose(a, g)), compose(a, g))), compose(compose(compose(a, g), compose(a, g)), compose(a, g))) -> compose(compose(compose(a, g), compose(a, g)), compose(a, g)) % 2.52/2.74 988: ifeq(codomain(g), domain(a), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, g), compose(a, b))), compose(compose(compose(a, g), compose(a, g)), compose(a, b))), compose(compose(compose(a, g), compose(a, g)), compose(a, b))) -> compose(compose(compose(a, g), compose(a, g)), compose(a, b)) % 2.52/2.74 989: ifeq(codomain(b), domain(a), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, b), compose(a, b))), compose(compose(compose(a, b), compose(a, b)), compose(a, b))), compose(compose(compose(a, b), compose(a, b)), compose(a, b))) -> compose(compose(compose(a, b), compose(a, b)), compose(a, b)) % 2.52/2.74 990: ifeq(codomain(b), domain(a), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, b), compose(a, b))), compose(compose(compose(a, g), compose(a, b)), compose(a, b))), compose(compose(compose(a, g), compose(a, b)), compose(a, b))) -> compose(compose(compose(a, g), compose(a, b)), compose(a, b)) % 2.52/2.74 991: ifeq(codomain(g), codomain(compose(compose(a, b), compose(a, g))), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, g), codomain(compose(compose(a, b), compose(a, g))))), compose(compose(a, b), compose(a, g))), compose(compose(a, b), compose(a, g))) -> compose(compose(a, b), compose(a, g)) % 2.52/2.74 992: ifeq(codomain(g), codomain(compose(compose(a, g), compose(a, g))), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, g), codomain(compose(compose(a, g), compose(a, g))))), compose(compose(a, g), compose(a, g))), compose(compose(a, g), compose(a, g))) -> compose(compose(a, g), compose(a, g)) % 2.52/2.74 993: ifeq(codomain(b), codomain(compose(compose(a, b), compose(a, b))), ifeq(codomain(b), domain(a), compose(compose(a, b), compose(compose(a, b), codomain(compose(compose(a, b), compose(a, b))))), compose(compose(a, b), compose(a, b))), compose(compose(a, b), compose(a, b))) -> compose(compose(a, b), compose(a, b)) % 2.52/2.74 994: ifeq(codomain(b), codomain(compose(compose(a, g), compose(a, b))), ifeq(codomain(g), domain(a), compose(compose(a, g), compose(compose(a, b), codomain(compose(compose(a, g), compose(a, b))))), compose(compose(a, g), compose(a, b))), compose(compose(a, g), compose(a, b))) -> compose(compose(a, g), compose(a, b)) % 2.52/2.74 995: ifeq(domain(X), domain(a), ifeq(domain(compose(domain(X), compose(a, g))), domain(X), compose(domain(X), compose(a, g)), compose(compose(domain(compose(domain(X), compose(a, g))), domain(X)), compose(a, g))), compose(compose(domain(compose(domain(X), compose(a, g))), domain(X)), compose(a, g))) -> compose(compose(domain(compose(domain(X), compose(a, g))), domain(X)), compose(a, g)) % 2.52/2.74 996: ifeq(codomain(X), domain(a), ifeq(domain(compose(codomain(X), compose(a, g))), codomain(X), compose(codomain(X), compose(a, g)), compose(compose(domain(compose(codomain(X), compose(a, g))), codomain(X)), compose(a, g))), compose(compose(domain(compose(codomain(X), compose(a, g))), codomain(X)), compose(a, g))) -> compose(compose(domain(compose(codomain(X), compose(a, g))), codomain(X)), compose(a, g)) % 2.52/2.74 997: ifeq(codomain(X), domain(a), ifeq(domain(compose(codomain(X), compose(a, b))), codomain(X), compose(codomain(X), compose(a, b)), compose(compose(domain(compose(codomain(X), compose(a, b))), codomain(X)), compose(a, b))), compose(compose(domain(compose(codomain(X), compose(a, b))), codomain(X)), compose(a, b))) -> compose(compose(domain(compose(codomain(X), compose(a, b))), codomain(X)), compose(a, b)) % 2.52/2.74 998: ifeq(domain(X), domain(a), ifeq(domain(compose(domain(X), compose(a, b))), domain(X), compose(domain(X), compose(a, b)), compose(compose(domain(compose(domain(X), compose(a, b))), domain(X)), compose(a, b))), compose(compose(domain(compose(domain(X), compose(a, b))), domain(X)), compose(a, b))) -> compose(compose(domain(compose(domain(X), compose(a, b))), domain(X)), compose(a, b)) % 2.52/2.74 999: ifeq(codomain(g), domain(X), ifeq(domain(compose(compose(a, g), domain(X))), domain(a), compose(compose(a, g), domain(X)), compose(compose(domain(compose(compose(a, g), domain(X))), compose(a, g)), domain(X))), compose(compose(domain(compose(compose(a, g), domain(X))), compose(a, g)), domain(X))) -> compose(compose(domain(compose(compose(a, g), domain(X))), compose(a, g)), domain(X)) % 2.52/2.74 1000: ifeq(codomain(g), codomain(X), ifeq(domain(compose(compose(a, g), codomain(X))), domain(a), compose(compose(a, g), codomain(X)), compose(compose(domain(compose(compose(a, g), codomain(X))), compose(a, g)), codomain(X))), compose(compose(domain(compose(compose(a, g), codomain(X))), compose(a, g)), codomain(X))) -> compose(compose(domain(compose(compose(a, g), codomain(X))), compose(a, g)), codomain(X)) % 2.52/2.74 1001: ifeq(codomain(b), domain(X), ifeq(domain(compose(compose(a, b), domain(X))), domain(a), compose(compose(a, b), domain(X)), compose(compose(domain(compose(compose(a, b), domain(X))), compose(a, b)), domain(X))), compose(compose(domain(compose(compose(a, b), domain(X))), compose(a, b)), domain(X))) -> compose(compose(domain(compose(compose(a, b), domain(X))), compose(a, b)), domain(X)) % 2.52/2.74 1002: ifeq(codomain(b), codomain(X), ifeq(domain(compose(compose(a, b), codomain(X))), domain(a), compose(compose(a, b), codomain(X)), compose(compose(domain(compose(compose(a, b), codomain(X))), compose(a, b)), codomain(X))), compose(compose(domain(compose(compose(a, b), codomain(X))), compose(a, b)), codomain(X))) -> compose(compose(domain(compose(compose(a, b), codomain(X))), compose(a, b)), codomain(X)) % 2.52/2.74 1003: ifeq(codomain(g), domain(a), ifeq(domain(compose(compose(a, g), compose(a, g))), domain(a), compose(compose(a, g), compose(a, g)), compose(compose(domain(compose(compose(a, g), compose(a, g))), compose(a, g)), compose(a, g))), compose(compose(domain(compose(compose(a, g), compose(a, g))), compose(a, g)), compose(a, g))) -> compose(compose(domain(compose(compose(a, g), compose(a, g))), compose(a, g)), compose(a, g)) % 2.52/2.74 1004: ifeq(codomain(b), domain(a), ifeq(domain(compose(compose(a, b), compose(a, g))), domain(a), compose(compose(a, b), compose(a, g)), compose(compose(domain(compose(compose(a, b), compose(a, g))), compose(a, b)), compose(a, g))), compose(compose(domain(compose(compose(a, b), compose(a, g))), compose(a, b)), compose(a, g))) -> compose(compose(domain(compose(compose(a, b), compose(a, g))), compose(a, b)), compose(a, g)) % 2.52/2.74 1005: ifeq(codomain(g), domain(a), ifeq(domain(compose(compose(a, g), compose(a, b))), domain(a), compose(compose(a, g), compose(a, b)), compose(compose(domain(compose(compose(a, g), compose(a, b))), compose(a, g)), compose(a, b))), compose(compose(domain(compose(compose(a, g), compose(a, b))), compose(a, g)), compose(a, b))) -> compose(compose(domain(compose(compose(a, g), compose(a, b))), compose(a, g)), compose(a, b)) % 2.52/2.74 1006: ifeq(codomain(b), domain(a), ifeq(domain(compose(compose(a, b), compose(a, b))), domain(a), compose(compose(a, b), compose(a, b)), compose(compose(domain(compose(compose(a, b), compose(a, b))), compose(a, b)), compose(a, b))), compose(compose(domain(compose(compose(a, b), compose(a, b))), compose(a, b)), compose(a, b))) -> compose(compose(domain(compose(compose(a, b), compose(a, b))), compose(a, b)), compose(a, b)) % 2.52/2.74 %------------------------------------------------------------------------------