%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : CAT001-4 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n021.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 : 600s % DateTime : Fri Jul 15 00:04:43 EDT 2022 % Result : Unsatisfiable 19.58s 19.30s % Output : Proof 19.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : CAT001-4 : TPTP v8.1.0. Released v1.0.0. % 0.11/0.13 % Command : moca.sh %s % 0.13/0.34 % Computer : n021.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sun May 29 17:34:28 EDT 2022 % 0.13/0.34 % CPUTime : % 19.58/19.30 % SZS status Unsatisfiable % 19.58/19.30 % SZS output start Proof % 19.58/19.30 The input problem is unsatisfiable because % 19.58/19.30 % 19.58/19.30 [1] the following set of Horn clauses is unsatisfiable: % 19.58/19.30 % 19.58/19.30 equivalent(X, Y) ==> there_exists(X) % 19.58/19.30 equivalent(X, Y) ==> X = Y % 19.58/19.30 there_exists(X) & X = Y ==> equivalent(X, Y) % 19.58/19.30 there_exists(domain(X)) ==> there_exists(X) % 19.58/19.30 there_exists(codomain(X)) ==> there_exists(X) % 19.58/19.30 there_exists(compose(X, Y)) ==> there_exists(domain(X)) % 19.58/19.30 there_exists(compose(X, Y)) ==> domain(X) = codomain(Y) % 19.58/19.30 there_exists(domain(X)) & domain(X) = codomain(Y) ==> there_exists(compose(X, Y)) % 19.58/19.30 compose(X, compose(Y, Z)) = compose(compose(X, Y), Z) % 19.58/19.30 compose(X, domain(X)) = X % 19.58/19.30 compose(codomain(X), X) = X % 19.58/19.30 there_exists(compose(a, b)) % 19.58/19.30 compose(compose(a, b), X) = Y & compose(compose(a, b), Z) = Y ==> X = Z % 19.58/19.30 there_exists(compose(b, h)) % 19.58/19.30 compose(b, h) = compose(b, g) % 19.58/19.30 h = g ==> \bottom % 19.58/19.30 % 19.58/19.30 This holds because % 19.58/19.30 % 19.58/19.30 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 19.58/19.30 % 19.58/19.30 E: % 19.58/19.30 compose(X, compose(Y, Z)) = compose(compose(X, Y), Z) % 19.58/19.30 compose(X, domain(X)) = X % 19.58/19.30 compose(b, h) = compose(b, g) % 19.58/19.30 compose(codomain(X), X) = X % 19.58/19.30 f1(equivalent(X, Y), X) = true__ % 19.58/19.30 f1(true__, X) = there_exists(X) % 19.58/19.30 f10(codomain(Y), Y, X) = f9(there_exists(domain(X)), X, Y) % 19.58/19.30 f10(domain(X), Y, X) = true__ % 19.58/19.30 f11(Y, Y, X, Z) = X % 19.58/19.30 f12(Y, Y, X, Z) = f11(compose(compose(a, b), X), Y, X, Z) % 19.58/19.30 f12(compose(compose(a, b), Z), Y, X, Z) = Z % 19.58/19.30 f13(g) = false__ % 19.58/19.30 f13(h) = true__ % 19.58/19.30 f2(equivalent(X, Y), X, Y) = Y % 19.58/19.30 f2(true__, X, Y) = X % 19.58/19.30 f3(true__, X, Y) = equivalent(X, Y) % 19.58/19.30 f4(X, Y, X) = true__ % 19.58/19.30 f4(Y, Y, X) = f3(there_exists(X), X, Y) % 19.58/19.30 f5(there_exists(domain(X)), X) = true__ % 19.58/19.30 f5(true__, X) = there_exists(X) % 19.58/19.30 f6(there_exists(codomain(X)), X) = true__ % 19.58/19.30 f6(true__, X) = there_exists(X) % 19.58/19.30 f7(there_exists(compose(X, Y)), X) = true__ % 19.58/19.30 f7(true__, X) = there_exists(domain(X)) % 19.58/19.30 f8(there_exists(compose(X, Y)), X, Y) = codomain(Y) % 19.58/19.30 f8(true__, X, Y) = domain(X) % 19.58/19.30 f9(true__, X, Y) = there_exists(compose(X, Y)) % 19.58/19.30 there_exists(compose(a, b)) = true__ % 19.58/19.30 there_exists(compose(b, h)) = true__ % 19.58/19.30 G: % 19.58/19.30 true__ = false__ % 19.58/19.30 % 19.58/19.30 This holds because % 19.58/19.30 % 19.58/19.30 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 19.58/19.30 % 19.58/19.30 domain(domain(f8(f6(true__, compose(X0, a)), X0, a))) = f8(f6(true__, compose(true__, a)), true__, a) % 19.58/19.30 f8(f6(true__, Y1), f8(f6(true__, compose(X0, Y1)), X0, Y1), Y1) = f8(f6(true__, compose(true__, Y1)), true__, Y1) % 19.58/19.30 f8(f6(true__, compose(X0, compose(X1, Y1))), compose(X0, X1), Y1) = f8(f6(true__, compose(Y2, Y1)), Y2, Y1) % 19.58/19.30 f8(f6(true__, compose(X0, compose(X1, Y1))), compose(X0, X1), Y1) = f8(f6(true__, compose(true__, Y1)), true__, Y1) % 19.58/19.30 f8(f6(true__, compose(X1, Y0)), X1, Y0) = f8(f6(true__, compose(Y1, Y0)), Y1, Y0) % 19.58/19.30 f8(f6(true__, compose(Y0, Y1)), compose(Y0, Y1), domain(Y1)) = f8(f6(true__, compose(true__, domain(Y1))), true__, domain(Y1)) % 19.58/19.30 f8(f6(true__, compose(Y0, compose(Y1, X1))), compose(Y0, Y1), compose(domain(Y1), X1)) = f8(f6(true__, compose(true__, compose(domain(Y1), X1))), true__, compose(domain(Y1), X1)) % 19.58/19.30 f8(there_exists(compose(X, Y)), X, Y) = codomain(Y) % 19.58/19.30 compose(X, domain(X)) -> X % 19.58/19.30 compose(X0, compose(X1, compose(Y1, domain(compose(X0, compose(X1, Y1)))))) -> compose(X0, compose(X1, Y1)) % 19.58/19.30 compose(X0, compose(X1, compose(Y1, domain(compose(domain(compose(X0, X1)), Y1))))) -> compose(X0, compose(X1, Y1)) % 19.58/19.30 compose(X0, compose(X1, compose(Y1, domain(domain(compose(X0, compose(X1, Y1))))))) -> compose(X0, compose(X1, Y1)) % 19.58/19.30 compose(X0, compose(X1, compose(domain(domain(compose(X0, X1))), Y1))) -> compose(X0, compose(X1, Y1)) % 19.58/19.30 compose(X0, compose(X1, compose(domain(domain(domain(compose(X0, X1)))), Y1))) -> compose(X0, compose(X1, Y1)) % 19.58/19.30 compose(Y0, compose(X0, compose(X1, domain(compose(domain(Y0), compose(X0, X1)))))) -> compose(Y0, compose(X0, X1)) % 19.58/19.30 compose(Y0, compose(X1, compose(domain(compose(Y0, X1)), domain(compose(Y0, X1))))) -> compose(Y0, X1) % 19.58/19.30 compose(Y0, compose(X1, compose(domain(compose(domain(Y0), X1)), Y2))) -> compose(Y0, compose(X1, Y2)) % 19.58/19.30 compose(Y0, compose(X1, domain(compose(domain(Y0), X1)))) -> compose(Y0, X1) % 19.58/19.30 compose(Y0, compose(X1, domain(compose(domain(domain(Y0)), X1)))) -> compose(Y0, X1) % 19.58/19.30 compose(Y0, compose(X1, domain(compose(domain(domain(domain(Y0))), X1)))) -> compose(Y0, X1) % 19.58/19.30 compose(Y0, compose(X1, domain(domain(compose(domain(Y0), X1))))) -> compose(Y0, X1) % 19.58/19.30 compose(Y0, compose(Y1, compose(domain(compose(Y0, Y1)), X1))) -> compose(Y0, compose(Y1, X1)) % 19.58/19.30 compose(Y0, compose(Y1, domain(compose(Y0, Y1)))) -> compose(Y0, Y1) % 19.58/19.30 compose(Y0, compose(Y1, domain(domain(compose(Y0, Y1))))) -> compose(Y0, Y1) % 19.58/19.30 compose(Y0, compose(Y1, domain(domain(domain(compose(Y0, Y1)))))) -> compose(Y0, Y1) % 19.58/19.30 compose(Y0, compose(Y1, domain(domain(domain(domain(compose(Y0, Y1))))))) -> compose(Y0, Y1) % 19.58/19.30 compose(Y0, compose(domain(Y0), Y2)) -> compose(Y0, Y2) % 19.58/19.30 compose(Y0, compose(domain(domain(Y0)), X1)) -> compose(Y0, X1) % 19.58/19.30 compose(Y0, compose(domain(domain(domain(Y0))), X1)) -> compose(Y0, X1) % 19.58/19.30 compose(Y0, compose(domain(domain(domain(Y0))), domain(domain(Y0)))) -> compose(Y0, domain(domain(domain(Y0)))) % 19.58/19.30 compose(Y0, compose(domain(domain(domain(domain(Y0)))), Y2)) -> compose(Y0, Y2) % 19.58/19.30 compose(Y0, compose(domain(domain(domain(domain(Y0)))), domain(Y0))) -> Y0 % 19.58/19.30 compose(Y0, compose(domain(domain(domain(domain(Y0)))), domain(domain(Y0)))) -> Y0 % 19.58/19.30 compose(Y0, compose(domain(domain(domain(domain(domain(Y0))))), X1)) -> compose(Y0, X1) % 19.58/19.30 compose(Y0, compose(domain(domain(domain(domain(domain(Y0))))), domain(domain(Y0)))) -> compose(Y0, domain(domain(domain(domain(domain(Y0)))))) % 19.58/19.30 compose(Y0, domain(compose(domain(Y0), domain(Y0)))) -> Y0 % 19.58/19.30 compose(Y0, domain(domain(Y0))) -> Y0 % 19.58/19.30 compose(Y0, domain(domain(domain(Y0)))) -> Y0 % 19.58/19.30 compose(Y0, domain(domain(domain(domain(Y0))))) -> Y0 % 19.58/19.30 compose(Y0, domain(domain(domain(domain(domain(Y0)))))) -> Y0 % 19.58/19.30 compose(Y0, domain(domain(domain(domain(domain(domain(Y0))))))) -> Y0 % 19.58/19.30 compose(Y0, domain(domain(domain(domain(domain(domain(domain(Y0)))))))) -> Y0 % 19.58/19.30 compose(b, compose(g, Y2)) -> compose(b, compose(h, Y2)) % 19.58/19.30 compose(b, compose(h, compose(X0, domain(compose(b, compose(h, X0)))))) -> compose(b, compose(h, X0)) % 19.58/19.30 compose(b, compose(h, compose(X0, domain(domain(compose(b, compose(h, X0))))))) -> compose(b, compose(h, X0)) % 19.58/19.30 compose(b, compose(h, compose(X1, domain(compose(g, X1))))) -> compose(b, compose(h, X1)) % 19.58/19.30 compose(b, compose(h, compose(domain(domain(g)), X1))) -> compose(b, compose(h, X1)) % 19.58/19.30 compose(b, compose(h, compose(domain(g), X1))) -> compose(b, compose(h, X1)) % 19.58/19.30 compose(b, compose(h, domain(domain(domain(domain(domain(h))))))) -> compose(b, h) % 19.58/19.30 compose(b, compose(h, domain(domain(domain(g))))) -> compose(b, h) % 19.58/19.30 compose(b, compose(h, domain(domain(g)))) -> compose(b, h) % 19.58/19.30 compose(b, compose(h, domain(g))) -> compose(b, h) % 19.58/19.30 compose(b, g) -> compose(b, h) % 19.58/19.30 compose(codomain(X), X) -> X % 19.58/19.30 compose(compose(X, Y), Z) -> compose(X, compose(Y, Z)) % 19.58/19.30 compose(domain(a), b) -> b % 19.58/19.30 compose(domain(a), compose(b, Y2)) -> compose(b, Y2) % 19.58/19.30 compose(domain(a), compose(domain(a), Y1)) -> compose(domain(a), Y1) % 19.58/19.30 compose(domain(a), domain(a)) -> domain(a) % 19.58/19.30 compose(domain(b), compose(domain(b), Y1)) -> compose(domain(b), Y1) % 19.58/19.30 compose(domain(b), compose(g, Y2)) -> compose(g, Y2) % 19.58/19.30 compose(domain(b), compose(h, Y2)) -> compose(h, Y2) % 19.58/19.30 compose(domain(b), compose(h, domain(g))) -> compose(h, domain(g)) % 19.58/19.30 compose(domain(b), domain(b)) -> domain(b) % 19.58/19.30 compose(domain(b), g) -> g % 19.58/19.30 compose(domain(b), h) -> h % 19.58/19.30 compose(domain(compose(a, b)), domain(compose(a, b))) -> domain(compose(a, b)) % 19.58/19.30 compose(domain(compose(b, h)), domain(compose(b, h))) -> domain(compose(b, h)) % 19.58/19.30 compose(domain(domain(a)), b) -> b % 19.58/19.30 compose(domain(domain(a)), compose(b, Y2)) -> compose(b, Y2) % 19.58/19.30 compose(domain(domain(a)), domain(domain(a))) -> domain(domain(a)) % 19.58/19.30 compose(domain(domain(b)), compose(g, Y2)) -> compose(g, Y2) % 19.58/19.30 compose(domain(domain(b)), compose(h, Y2)) -> compose(h, Y2) % 19.58/19.30 compose(domain(domain(b)), domain(domain(b))) -> domain(domain(b)) % 19.58/19.30 compose(domain(domain(b)), g) -> g % 19.58/19.30 compose(domain(domain(b)), h) -> h % 19.58/19.30 compose(domain(domain(compose(a, b))), domain(domain(compose(a, b)))) -> domain(domain(compose(a, b))) % 19.58/19.30 compose(domain(domain(compose(b, h))), domain(domain(compose(b, h)))) -> domain(domain(compose(b, h))) % 19.58/19.30 compose(domain(domain(domain(a))), domain(domain(domain(a)))) -> domain(domain(domain(a))) % 19.58/19.30 compose(domain(domain(domain(b))), domain(domain(domain(b)))) -> domain(domain(domain(b))) % 19.58/19.30 compose(domain(domain(domain(compose(a, b)))), domain(domain(domain(compose(a, b))))) -> domain(domain(domain(compose(a, b)))) % 19.58/19.30 compose(domain(domain(domain(compose(b, h)))), domain(domain(domain(compose(b, h))))) -> domain(domain(domain(compose(b, h)))) % 19.58/19.30 compose(domain(domain(f8(f6(true__, compose(true__, a)), true__, a))), a) -> a % 19.58/19.30 compose(domain(domain(h)), compose(domain(domain(h)), Y1)) -> compose(domain(domain(h)), Y1) % 19.58/19.30 compose(domain(domain(h)), domain(domain(h))) -> domain(domain(h)) % 19.58/19.30 compose(domain(domain(h)), domain(h)) -> domain(h) % 19.58/19.30 compose(domain(f8(f6(true__, compose(X0, a)), X0, a)), compose(a, Y2)) -> compose(a, Y2) % 19.58/19.30 compose(domain(f8(f6(true__, compose(X0, compose(X1, a))), compose(X0, X1), a)), a) -> a % 19.58/19.30 compose(domain(f8(f6(true__, compose(Y1, a)), Y1, a)), a) -> a % 19.58/19.30 compose(domain(g), domain(g)) -> domain(g) % 19.58/19.30 compose(domain(h), compose(domain(h), Y2)) -> compose(domain(h), Y2) % 19.58/19.30 compose(domain(h), domain(h)) -> domain(h) % 19.58/19.30 compose(f8(f6(true__, Y0), Y0, domain(Y0)), compose(domain(Y0), Y2)) -> compose(domain(Y0), Y2) % 19.58/19.30 compose(f8(f6(true__, Y0), Y0, domain(Y0)), domain(Y0)) -> domain(Y0) % 19.58/19.30 compose(f8(f6(true__, Y0), Y0, domain(domain(Y0))), compose(domain(domain(Y0)), Y2)) -> compose(domain(domain(Y0)), Y2) % 19.58/19.30 compose(f8(f6(true__, Y0), Y0, domain(domain(Y0))), domain(domain(Y0))) -> domain(domain(Y0)) % 19.58/19.30 compose(f8(f6(true__, Y0), Y0, domain(domain(domain(Y0)))), domain(domain(domain(Y0)))) -> domain(domain(domain(Y0))) % 19.58/19.30 compose(f8(f6(true__, Y0), Y0, domain(domain(domain(domain(Y0))))), domain(domain(domain(domain(Y0))))) -> domain(domain(domain(domain(Y0)))) % 19.58/19.30 compose(f8(f6(true__, Y1), f8(f6(true__, compose(X0, Y1)), X0, Y1), Y1), Y1) -> Y1 % 19.58/19.30 compose(f8(f6(true__, compose(X0, Y1)), X0, Y1), compose(Y1, Y2)) -> compose(Y1, Y2) % 19.58/19.30 compose(f8(f6(true__, compose(X0, compose(X1, Y1))), compose(X0, X1), Y1), Y1) -> Y1 % 19.58/19.30 compose(f8(f6(true__, compose(X1, Y0)), X1, Y0), Y0) -> Y0 % 19.58/19.30 compose(f8(f6(true__, compose(Y0, X1)), Y0, compose(X1, domain(compose(Y0, X1)))), compose(X1, domain(compose(Y0, X1)))) -> compose(X1, domain(compose(Y0, X1))) % 19.58/19.30 compose(f8(f6(true__, compose(Y0, X1)), Y0, compose(domain(Y0), X1)), compose(domain(Y0), X1)) -> compose(domain(Y0), X1) % 19.58/19.30 compose(f8(f6(true__, compose(Y0, X1)), Y0, compose(domain(domain(Y0)), X1)), compose(domain(domain(Y0)), X1)) -> compose(domain(domain(Y0)), X1) % 19.58/19.30 compose(f8(f6(true__, compose(Y0, Y1)), compose(Y0, Y1), domain(Y1)), domain(Y1)) -> domain(Y1) % 19.58/19.30 compose(f8(f6(true__, compose(Y0, Y1)), compose(Y0, Y1), domain(domain(Y1))), domain(domain(Y1))) -> domain(domain(Y1)) % 19.58/19.30 compose(f8(f6(true__, compose(Y0, b)), compose(Y0, domain(a)), b), b) -> b % 19.58/19.30 compose(f8(f6(true__, compose(Y0, f8(f6(true__, compose(true__, Y2)), true__, Y2))), Y0, f8(f6(true__, compose(true__, Y2)), true__, Y2)), Y2) -> Y2 % 19.58/19.30 compose(f8(f6(true__, compose(Y0, g)), compose(Y0, domain(b)), g), g) -> g % 19.58/19.30 compose(f8(f6(true__, compose(Y0, h)), compose(Y0, domain(b)), h), h) -> h % 19.58/19.30 compose(f8(f6(true__, compose(b, X0)), domain(a), compose(b, X0)), compose(b, X0)) -> compose(b, X0) % 19.58/19.30 compose(f8(f6(true__, compose(b, compose(h, X0))), b, compose(g, X0)), compose(g, X0)) -> compose(g, X0) % 19.58/19.30 compose(f8(f6(true__, compose(domain(a), compose(b, Y2))), b, Y2), Y2) -> Y2 % 19.58/19.30 compose(f8(f6(true__, compose(domain(b), compose(g, Y2))), g, Y2), Y2) -> Y2 % 19.58/19.30 compose(f8(f6(true__, compose(domain(b), compose(h, Y2))), h, Y2), Y2) -> Y2 % 19.58/19.30 compose(f8(f6(true__, compose(h, X0)), domain(b), compose(h, X0)), compose(h, X0)) -> compose(h, X0) % 19.58/19.30 compose(f8(f6(true__, compose(true__, X1)), true__, compose(domain(true__), X1)), compose(domain(true__), compose(X1, Y1))) -> compose(domain(true__), compose(X1, Y1)) % 19.58/19.30 compose(f8(f6(true__, compose(true__, Y1)), true__, Y1), compose(Y1, Y2)) -> compose(Y1, Y2) % 19.58/19.30 compose(f8(f6(true__, compose(true__, compose(X0, X1))), true__, compose(X0, X1)), compose(X0, compose(X1, Y1))) -> compose(X0, compose(X1, Y1)) % 19.58/19.30 compose(f8(f6(true__, compose(true__, f8(f6(true__, compose(true__, Y1)), true__, Y1))), true__, f8(f6(true__, compose(true__, Y1)), true__, Y1)), Y1) -> Y1 % 19.58/19.30 compose(f8(f6(true__, domain(Y1)), f8(f6(true__, Y1), Y1, domain(Y1)), domain(Y1)), domain(Y1)) -> domain(Y1) % 19.58/19.30 compose(f8(f6(true__, true__), true__, domain(domain(true__))), compose(domain(domain(true__)), Y1)) -> compose(domain(domain(true__)), Y1) % 19.58/19.30 compose(f8(f6(true__, true__), true__, domain(true__)), compose(domain(true__), Y1)) -> compose(domain(true__), Y1) % 19.58/19.30 domain(domain(a)) -> domain(a) % 19.58/19.30 domain(domain(b)) -> domain(b) % 19.58/19.30 domain(domain(compose(a, b))) -> domain(compose(a, b)) % 19.58/19.30 domain(domain(compose(b, h))) -> domain(compose(b, h)) % 19.58/19.30 domain(domain(domain(h))) -> domain(domain(h)) % 19.58/19.30 domain(domain(h)) -> domain(h) % 19.58/19.30 domain(f8(f6(true__, compose(true__, compose(a, b))), true__, compose(a, b))) -> f8(f6(true__, compose(true__, compose(a, b))), true__, compose(a, b)) % 19.58/19.30 domain(f8(f6(true__, compose(true__, compose(b, h))), true__, compose(b, h))) -> f8(f6(true__, compose(true__, compose(b, h))), true__, compose(b, h)) % 19.58/19.30 domain(f8(f6(true__, compose(true__, domain(a))), true__, domain(a))) -> f8(f6(true__, compose(true__, domain(a))), true__, domain(a)) % 19.58/19.30 domain(f8(f6(true__, compose(true__, domain(b))), true__, domain(b))) -> f8(f6(true__, compose(true__, domain(b))), true__, domain(b)) % 19.58/19.30 equivalent(X, Y) -> f3(true__, X, Y) % 19.58/19.30 f1(equivalent(X, Y), X) -> true__ % 19.58/19.30 f1(f3(true__, Y0, Y1), Y0) -> true__ % 19.58/19.30 f1(true__, X) -> there_exists(X) % 19.58/19.30 f10(codomain(Y), Y, X) -> f9(there_exists(domain(X)), X, Y) % 19.58/19.30 f10(domain(X), Y, X) -> true__ % 19.58/19.30 f10(domain(a), Y1, domain(a)) -> true__ % 19.58/19.30 f10(domain(a), b, Y2) -> f9(f6(true__, domain(Y2)), Y2, b) % 19.58/19.30 f10(domain(b), Y1, domain(b)) -> true__ % 19.58/19.30 f10(domain(b), g, Y2) -> f9(f6(true__, domain(Y2)), Y2, g) % 19.58/19.30 f10(domain(b), h, Y2) -> f9(f6(true__, domain(Y2)), Y2, h) % 19.58/19.30 f10(f8(f6(true__, Y0), Y0, domain(Y0)), domain(Y0), Y2) -> f9(f6(true__, domain(Y2)), Y2, domain(Y0)) % 19.58/19.30 f10(f8(f6(true__, compose(X0, compose(X1, Y1))), compose(X0, X1), Y1), Y1, Y2) -> f9(f6(true__, domain(Y2)), Y2, Y1) % 19.58/19.30 f10(f8(f6(true__, compose(X1, Y0)), X1, Y0), Y0, Y1) -> f9(f6(true__, domain(Y1)), Y1, Y0) % 19.58/19.30 f10(f8(f6(true__, compose(Y0, X1)), Y0, compose(domain(Y0), X1)), compose(domain(Y0), X1), Y2) -> f9(f6(true__, domain(Y2)), Y2, compose(domain(Y0), X1)) % 19.58/19.30 f11(Y, Y, X, Z) -> X % 19.58/19.30 f11(compose(a, b), compose(a, compose(b, X1)), domain(b), compose(domain(b), X1)) -> compose(domain(b), X1) % 19.58/19.30 f11(compose(a, b), compose(a, compose(b, Y1)), domain(b), Y1) -> Y1 % 19.58/19.30 f11(compose(a, b), compose(a, compose(b, Y1)), domain(domain(b)), Y1) -> Y1 % 19.58/19.30 f11(compose(a, b), compose(a, compose(b, h)), domain(b), g) -> g % 19.58/19.30 f11(compose(a, compose(b, X1)), compose(a, compose(b, Y1)), compose(domain(b), X1), Y1) -> Y1 % 19.58/19.30 f11(compose(a, compose(b, Y0)), compose(a, b), Y0, domain(b)) -> domain(b) % 19.58/19.30 f11(compose(a, compose(b, Y0)), compose(a, b), Y0, domain(domain(b))) -> domain(domain(b)) % 19.58/19.30 f11(compose(a, compose(b, Y0)), compose(a, compose(b, X1)), Y0, compose(domain(b), X1)) -> compose(domain(b), X1) % 19.58/19.30 f11(compose(a, compose(b, Y0)), compose(a, compose(b, compose(h, X0))), Y0, compose(g, X0)) -> compose(g, X0) % 19.58/19.30 f11(compose(a, compose(b, Y0)), compose(a, compose(b, h)), Y0, g) -> g % 19.58/19.30 f11(compose(a, compose(b, Y1)), compose(a, compose(b, Y2)), Y1, Y2) -> Y2 % 19.58/19.30 f11(compose(a, compose(b, compose(h, X0))), compose(a, compose(b, Y1)), compose(g, X0), Y1) -> Y1 % 19.58/19.30 f11(compose(a, compose(b, h)), compose(a, b), g, domain(b)) -> domain(b) % 19.58/19.30 f11(compose(a, compose(b, h)), compose(a, compose(b, Y1)), g, Y1) -> Y1 % 19.58/19.30 f12(Y, Y, X, Z) -> f11(compose(compose(a, b), X), Y, X, Z) % 19.58/19.30 f12(compose(a, b), Y1, Y2, compose(domain(b), domain(b))) -> compose(domain(b), domain(b)) % 19.58/19.30 f12(compose(a, b), Y1, Y2, domain(b)) -> domain(b) % 19.58/19.30 f12(compose(a, b), Y1, Y2, domain(compose(a, b))) -> domain(compose(a, b)) % 19.58/19.30 f12(compose(a, b), Y1, Y2, domain(domain(b))) -> domain(domain(b)) % 19.58/19.30 f12(compose(a, b), Y1, Y2, domain(domain(compose(a, b)))) -> domain(domain(compose(a, b))) % 19.58/19.30 f12(compose(a, b), Y1, Y2, domain(domain(domain(compose(a, b))))) -> domain(domain(domain(compose(a, b)))) % 19.58/19.30 f12(compose(a, b), Y1, Y2, domain(domain(domain(domain(compose(a, b)))))) -> domain(domain(domain(domain(compose(a, b))))) % 19.58/19.30 f12(compose(a, compose(b, X1)), Y1, Y2, compose(X1, domain(compose(a, compose(b, X1))))) -> compose(X1, domain(compose(a, compose(b, X1)))) % 19.58/19.30 f12(compose(a, compose(b, X1)), Y1, Y2, compose(X1, domain(compose(b, X1)))) -> compose(X1, domain(compose(b, X1))) % 19.58/19.30 f12(compose(a, compose(b, X1)), Y1, Y2, compose(X1, domain(compose(domain(b), X1)))) -> compose(X1, domain(compose(domain(b), X1))) % 19.58/19.30 f12(compose(a, compose(b, X1)), Y1, Y2, compose(X1, domain(compose(domain(compose(a, b)), X1)))) -> compose(X1, domain(compose(domain(compose(a, b)), X1))) % 19.58/19.30 f12(compose(a, compose(b, X1)), Y1, Y2, compose(X1, domain(domain(compose(a, compose(b, X1)))))) -> compose(X1, domain(domain(compose(a, compose(b, X1))))) % 19.58/19.30 f12(compose(a, compose(b, X1)), Y1, Y2, compose(X1, domain(domain(compose(b, X1))))) -> compose(X1, domain(domain(compose(b, X1)))) % 19.58/19.30 f12(compose(a, compose(b, X1)), Y1, Y2, compose(domain(b), X1)) -> compose(domain(b), X1) % 19.58/19.30 f12(compose(a, compose(b, X1)), Y1, Y2, compose(domain(compose(a, b)), X1)) -> compose(domain(compose(a, b)), X1) % 19.58/19.30 f12(compose(a, compose(b, X1)), Y1, Y2, compose(domain(domain(compose(a, b))), X1)) -> compose(domain(domain(compose(a, b))), X1) % 19.58/19.30 f12(compose(a, compose(b, X1)), Y1, Y2, compose(domain(domain(domain(compose(a, b)))), X1)) -> compose(domain(domain(domain(compose(a, b)))), X1) % 19.58/19.30 f12(compose(a, compose(b, Y0)), Y1, Y2, Y0) -> Y0 % 19.58/19.30 f12(compose(a, compose(b, compose(h, X0))), Y1, Y2, compose(g, X0)) -> compose(g, X0) % 19.58/19.30 f12(compose(a, compose(b, h)), Y1, Y2, compose(g, domain(h))) -> compose(g, domain(h)) % 19.58/19.30 f12(compose(a, compose(b, h)), Y1, Y2, compose(h, domain(g))) -> compose(h, domain(g)) % 19.58/19.30 f12(compose(a, compose(b, h)), Y1, Y2, g) -> g % 19.58/19.30 f12(compose(compose(a, b), Z), Y, X, Z) -> Z % 19.58/19.30 f13(g) -> false__ % 19.58/19.30 f13(h) -> true__ % 19.58/19.30 f2(equivalent(X, Y), X, Y) -> Y % 19.58/19.30 f2(f3(true__, Y0, Y1), Y0, Y1) -> Y1 % 19.58/19.30 f2(true__, X, Y) -> X % 19.58/19.30 f3(f6(true__, Y1), Y1, Y1) -> true__ % 19.58/19.30 f3(true__, a, a) -> true__ % 19.58/19.30 f3(true__, b, b) -> true__ % 19.58/19.30 f3(true__, compose(a, b), compose(a, b)) -> true__ % 19.58/19.30 f3(true__, compose(b, h), compose(b, h)) -> true__ % 19.58/19.30 f3(true__, domain(a), domain(a)) -> true__ % 19.58/19.30 f3(true__, domain(b), domain(b)) -> true__ % 19.58/19.30 f3(true__, domain(compose(a, b)), domain(compose(a, b))) -> true__ % 19.58/19.30 f3(true__, domain(compose(b, h)), domain(compose(b, h))) -> true__ % 19.58/19.30 f3(true__, domain(domain(a)), domain(domain(a))) -> true__ % 19.58/19.30 f3(true__, domain(domain(b)), domain(domain(b))) -> true__ % 19.58/19.30 f3(true__, domain(domain(compose(a, b))), domain(domain(compose(a, b)))) -> true__ % 19.58/19.30 f3(true__, domain(domain(compose(b, h))), domain(domain(compose(b, h)))) -> true__ % 19.58/19.30 f3(true__, domain(f8(f6(true__, compose(X0, a)), X0, a)), domain(f8(f6(true__, compose(X0, a)), X0, a))) -> true__ % 19.58/19.30 f3(true__, domain(f8(f6(true__, compose(true__, a)), true__, a)), domain(f8(f6(true__, compose(true__, a)), true__, a))) -> true__ % 19.58/19.30 f3(true__, domain(h), domain(h)) -> true__ % 19.58/19.30 f3(true__, g, g) -> true__ % 19.58/19.30 f3(true__, h, h) -> true__ % 19.58/19.30 f4(X, Y, X) -> true__ % 19.58/19.30 f4(Y, Y, X) -> f3(there_exists(X), X, Y) % 19.58/19.30 f5(f6(true__, domain(Y0)), Y0) -> true__ % 19.58/19.30 f5(there_exists(domain(X)), X) -> true__ % 19.58/19.30 f5(true__, X) -> there_exists(X) % 19.58/19.30 f6(f6(true__, domain(domain(domain(a)))), domain(domain(domain(a)))) -> true__ % 19.58/19.30 f6(f6(true__, domain(domain(domain(b)))), domain(domain(domain(b)))) -> true__ % 19.58/19.30 f6(f6(true__, domain(domain(domain(compose(a, b))))), domain(domain(domain(compose(a, b))))) -> true__ % 19.58/19.30 f6(f6(true__, domain(domain(domain(compose(b, h))))), domain(domain(domain(compose(b, h))))) -> true__ % 19.58/19.30 f6(f6(true__, domain(domain(h))), domain(domain(domain(h)))) -> true__ % 19.58/19.30 f6(f6(true__, domain(domain(h))), domain(domain(h))) -> true__ % 19.58/19.30 f6(f6(true__, domain(domain(h))), domain(h)) -> true__ % 19.58/19.30 f6(f6(true__, domain(g)), domain(g)) -> true__ % 19.58/19.30 f6(f6(true__, domain(h)), domain(h)) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, Y0), Y0, domain(Y0))), domain(Y0)) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, Y0), Y0, domain(domain(Y0)))), domain(domain(Y0))) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, Y0), Y0, domain(domain(domain(Y0))))), domain(domain(domain(Y0)))) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, Y0), Y0, domain(domain(domain(domain(Y0)))))), domain(domain(domain(domain(Y0))))) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, Y1), f8(f6(true__, compose(X0, Y1)), X0, Y1), Y1)), Y1) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, compose(X0, compose(X1, Y1))), compose(X0, X1), Y1)), Y1) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, compose(X1, Y0)), X1, Y0)), Y0) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, compose(Y0, X1)), Y0, compose(X1, domain(compose(Y0, X1))))), compose(X1, domain(compose(Y0, X1)))) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, compose(Y0, X1)), Y0, compose(domain(Y0), X1))), compose(domain(Y0), X1)) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, compose(b, compose(h, X0))), b, compose(g, X0))), compose(g, X0)) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, compose(h, X0)), domain(b), compose(h, X0))), compose(h, X0)) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, compose(true__, X1)), true__, compose(X1, domain(compose(true__, X1))))), compose(X1, domain(compose(true__, X1)))) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, compose(true__, X1)), true__, compose(domain(true__), X1))), compose(domain(true__), X1)) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, compose(true__, Y0)), true__, Y0)), Y0) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, true__), true__, domain(domain(domain(domain(true__)))))), domain(domain(domain(domain(true__))))) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, true__), true__, domain(domain(domain(true__))))), domain(domain(domain(true__)))) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, true__), true__, domain(domain(true__)))), domain(domain(true__))) -> true__ % 19.58/19.30 f6(f6(true__, f8(f6(true__, true__), true__, domain(true__))), domain(true__)) -> true__ % 19.58/19.30 f6(there_exists(codomain(X)), X) -> true__ % 19.58/19.30 f6(true__, a) -> true__ % 19.58/19.30 f6(true__, b) -> true__ % 19.58/19.30 f6(true__, compose(a, b)) -> true__ % 19.58/19.30 f6(true__, compose(b, h)) -> true__ % 19.58/19.30 f6(true__, domain(a)) -> true__ % 19.58/19.30 f6(true__, domain(b)) -> true__ % 19.58/19.30 f6(true__, domain(compose(a, b))) -> true__ % 19.58/19.30 f6(true__, domain(compose(b, h))) -> true__ % 19.58/19.30 f6(true__, domain(domain(a))) -> true__ % 19.58/19.30 f6(true__, domain(domain(b))) -> true__ % 19.58/19.30 f6(true__, domain(domain(compose(a, b)))) -> true__ % 19.58/19.30 f6(true__, domain(domain(compose(b, h)))) -> true__ % 19.58/19.30 f6(true__, domain(domain(domain(a)))) -> true__ % 19.58/19.30 f6(true__, domain(domain(domain(b)))) -> true__ % 19.58/19.30 f6(true__, domain(domain(domain(compose(a, b))))) -> true__ % 19.58/19.30 f6(true__, domain(domain(domain(compose(b, h))))) -> true__ % 19.58/19.30 f6(true__, domain(domain(domain(h)))) -> true__ % 19.58/19.30 f6(true__, domain(domain(f8(f6(true__, compose(X0, a)), X0, a)))) -> true__ % 19.58/19.30 f6(true__, domain(domain(f8(f6(true__, compose(true__, a)), true__, a)))) -> true__ % 19.58/19.30 f6(true__, domain(domain(h))) -> true__ % 19.58/19.30 f6(true__, domain(f8(f6(true__, compose(X0, b)), compose(X0, domain(a)), b))) -> true__ % 19.58/19.30 f6(true__, domain(f8(f6(true__, compose(X0, compose(X1, a))), compose(X0, X1), a))) -> true__ % 19.58/19.30 f6(true__, domain(f8(f6(true__, compose(X0, h)), compose(X0, domain(b)), h))) -> true__ % 19.58/19.30 f6(true__, domain(f8(f6(true__, compose(Y1, a)), Y1, a))) -> true__ % 19.58/19.30 f6(true__, domain(f8(f6(true__, compose(Y1, compose(a, b))), Y1, compose(a, b)))) -> true__ % 19.58/19.30 f6(true__, domain(f8(f6(true__, compose(Y1, compose(b, h))), Y1, compose(b, h)))) -> true__ % 19.58/19.30 f6(true__, domain(f8(f6(true__, compose(true__, a)), true__, a))) -> true__ % 19.58/19.30 f6(true__, domain(f8(f6(true__, compose(true__, compose(a, b))), true__, compose(a, b)))) -> true__ % 19.58/19.30 f6(true__, domain(f8(f6(true__, compose(true__, compose(b, h))), true__, compose(b, h)))) -> true__ % 19.58/19.30 f6(true__, domain(f8(f6(true__, compose(true__, domain(a))), true__, domain(a)))) -> true__ % 19.58/19.30 f6(true__, domain(f8(f6(true__, compose(true__, domain(b))), true__, domain(b)))) -> true__ % 19.58/19.30 f6(true__, domain(g)) -> true__ % 19.58/19.30 f6(true__, domain(h)) -> true__ % 19.58/19.30 f6(true__, f8(f6(true__, compose(X0, a)), X0, a)) -> true__ % 19.58/19.30 f6(true__, f8(f6(true__, compose(true__, a)), true__, a)) -> true__ % 19.58/19.30 f6(true__, g) -> true__ % 19.58/19.30 f6(true__, h) -> true__ % 19.58/19.30 f7(f6(true__, Y0), Y0) -> true__ % 19.58/19.30 f7(f6(true__, Y0), compose(Y0, f8(f6(true__, Y0), Y0, domain(Y0)))) -> true__ % 19.58/19.30 f7(f6(true__, Y1), f8(f6(true__, compose(X0, Y1)), X0, Y1)) -> true__ % 19.58/19.30 f7(f6(true__, Y1), f8(f6(true__, compose(true__, Y1)), true__, Y1)) -> true__ % 19.58/19.30 f7(f6(true__, Y1), f8(f6(true__, compose(true__, f8(f6(true__, compose(true__, Y1)), true__, Y1))), true__, f8(f6(true__, compose(true__, Y1)), true__, Y1))) -> true__ % 19.58/19.30 f7(f6(true__, compose(X0, X1)), f8(f6(true__, compose(true__, X0)), true__, X0)) -> true__ % 19.58/19.30 f7(f6(true__, compose(X0, compose(X1, Y1))), compose(X0, X1)) -> true__ % 19.58/19.30 f7(f6(true__, compose(X0, compose(X1, b))), compose(X0, compose(X1, domain(a)))) -> true__ % 19.58/19.30 f7(f6(true__, compose(X0, compose(X1, compose(Y1, Y2)))), compose(X0, compose(X1, Y1))) -> true__ % 19.58/19.30 f7(f6(true__, compose(X0, compose(X1, h))), compose(X0, compose(X1, domain(b)))) -> true__ % 19.58/19.30 f7(f6(true__, compose(X1, domain(compose(true__, X1)))), f8(f6(true__, compose(true__, X1)), true__, compose(X1, domain(compose(true__, X1))))) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y0, Y1)), Y0) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y0, Y2)), compose(Y0, f8(f6(true__, compose(X0, Y2)), X0, Y2))) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y0, Y2)), compose(Y0, f8(f6(true__, compose(true__, Y2)), true__, Y2))) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y0, b)), compose(Y0, domain(a))) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y0, compose(Y1, Y3))), compose(Y0, compose(Y1, f8(f6(true__, compose(true__, Y3)), true__, Y3)))) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y0, compose(Y2, Y3))), compose(Y0, compose(f8(f6(true__, compose(true__, compose(Y2, Y3))), true__, compose(Y2, Y3)), Y2))) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y0, compose(b, X0))), compose(Y0, domain(a))) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y0, compose(h, X0))), compose(Y0, domain(b))) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y0, domain(true__))), compose(Y0, f8(f6(true__, true__), true__, domain(true__)))) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y0, g)), compose(Y0, domain(b))) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y0, h)), compose(Y0, domain(b))) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y1, Y2)), compose(f8(f6(true__, compose(X0, compose(Y1, Y2))), X0, compose(Y1, Y2)), Y1)) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y1, Y2)), compose(f8(f6(true__, compose(true__, compose(Y1, Y2))), true__, compose(Y1, Y2)), Y1)) -> true__ % 19.58/19.30 f7(f6(true__, compose(Y1, compose(Y2, Y3))), compose(f8(f6(true__, compose(true__, compose(Y1, compose(Y2, Y3)))), true__, compose(Y1, compose(Y2, Y3))), compose(Y1, Y2))) -> true__ % 19.58/19.30 f7(f6(true__, compose(b, X0)), domain(a)) -> true__ % 19.58/19.30 f7(f6(true__, compose(b, compose(h, Y1))), compose(b, compose(h, f8(f6(true__, compose(true__, Y1)), true__, Y1)))) -> true__ % 19.58/19.30 f7(f6(true__, compose(b, compose(h, b))), compose(b, compose(h, domain(a)))) -> true__ % 19.58/19.30 f7(f6(true__, compose(b, compose(h, compose(X0, Y2)))), compose(b, compose(h, X0))) -> true__ % 19.58/19.30 f7(f6(true__, compose(b, compose(h, h))), compose(b, compose(h, domain(b)))) -> true__ % 19.58/19.30 f7(f6(true__, compose(domain(Y1), X1)), f8(f6(true__, compose(Y1, X1)), Y1, compose(domain(Y1), X1))) -> true__ % 19.58/19.30 f7(f6(true__, compose(domain(a), compose(b, Y2))), b) -> true__ % 19.58/19.30 f7(f6(true__, compose(domain(b), compose(g, Y2))), g) -> true__ % 19.58/19.30 f7(f6(true__, compose(domain(b), compose(h, Y2))), h) -> true__ % 19.58/19.30 f7(f6(true__, compose(domain(domain(true__)), Y1)), f8(f6(true__, true__), true__, domain(domain(true__)))) -> true__ % 19.58/19.30 f7(f6(true__, compose(domain(true__), X1)), f8(f6(true__, compose(true__, X1)), true__, compose(domain(true__), X1))) -> true__ % 19.58/19.30 f7(f6(true__, compose(domain(true__), Y1)), f8(f6(true__, true__), true__, domain(true__))) -> true__ % 19.58/19.30 f7(f6(true__, compose(f8(f6(true__, compose(X0, Y1)), X0, Y1), compose(Y1, Y2))), Y1) -> true__ % 19.58/19.30 f7(f6(true__, compose(h, X0)), domain(b)) -> true__ % 19.58/19.30 f7(f6(true__, domain(Y1)), f8(f6(true__, Y1), Y1, domain(Y1))) -> true__ % 19.58/19.30 f7(f6(true__, domain(domain(Y1))), f8(f6(true__, Y1), Y1, domain(domain(Y1)))) -> true__ % 19.58/19.30 f7(f6(true__, domain(domain(domain(Y1)))), f8(f6(true__, Y1), Y1, domain(domain(domain(Y1))))) -> true__ % 19.58/19.30 f7(f6(true__, domain(domain(domain(domain(Y1))))), f8(f6(true__, Y1), Y1, domain(domain(domain(domain(Y1)))))) -> true__ % 19.58/19.30 f7(f6(true__, domain(domain(domain(domain(true__))))), f8(f6(true__, true__), true__, domain(domain(domain(domain(true__)))))) -> true__ % 19.58/19.30 f7(f6(true__, domain(domain(domain(h)))), domain(domain(h))) -> true__ % 19.58/19.30 f7(f6(true__, domain(domain(domain(true__)))), f8(f6(true__, true__), true__, domain(domain(domain(true__))))) -> true__ % 19.58/19.30 f7(f6(true__, domain(domain(h))), domain(h)) -> true__ % 19.58/19.30 f7(f6(true__, domain(domain(true__))), f8(f6(true__, true__), true__, domain(domain(true__)))) -> true__ % 19.58/19.30 f7(f6(true__, domain(true__)), f8(f6(true__, true__), true__, domain(true__))) -> true__ % 19.58/19.30 f7(there_exists(compose(X, Y)), X) -> true__ % 19.58/19.30 f7(true__, X) -> there_exists(domain(X)) % 19.58/19.30 f8(f6(true__, Y1), f8(f6(true__, compose(true__, Y1)), true__, Y1), Y1) -> f8(f6(true__, compose(true__, Y1)), true__, Y1) % 19.58/19.30 f8(f6(true__, compose(X0, compose(X1, b))), compose(X0, X1), b) -> domain(a) % 19.58/19.30 f8(f6(true__, compose(X0, compose(X1, g))), compose(X0, X1), g) -> domain(b) % 19.58/19.30 f8(f6(true__, compose(X0, compose(X1, h))), compose(X0, X1), h) -> domain(b) % 19.58/19.30 f8(f6(true__, compose(Y0, Y2)), compose(Y0, f8(f6(true__, compose(true__, Y2)), true__, Y2)), Y2) -> f8(f6(true__, compose(true__, Y2)), true__, Y2) % 19.58/19.30 f8(f6(true__, compose(Y0, b)), compose(Y0, domain(a)), b) -> domain(a) % 19.58/19.30 f8(f6(true__, compose(Y0, compose(b, h))), compose(Y0, b), g) -> f8(f6(true__, compose(true__, g)), true__, g) % 19.58/19.30 f8(f6(true__, compose(Y0, h)), compose(Y0, domain(b)), h) -> domain(b) % 19.58/19.30 f8(f6(true__, compose(Y1, Y2)), compose(f8(f6(true__, compose(true__, compose(Y1, Y2))), true__, compose(Y1, Y2)), Y1), Y2) -> f8(f6(true__, compose(true__, Y2)), true__, Y2) % 19.58/19.30 f8(f6(true__, compose(Y1, compose(Y2, domain(true__)))), compose(Y1, Y2), domain(true__)) -> f8(f6(true__, true__), true__, domain(true__)) % 19.58/19.30 f8(f6(true__, compose(Y2, b)), Y2, b) -> domain(a) % 19.58/19.30 f8(f6(true__, compose(Y2, compose(domain(Y0), X1))), Y2, compose(domain(Y0), X1)) -> f8(f6(true__, compose(Y0, X1)), Y0, compose(domain(Y0), X1)) % 19.58/19.30 f8(f6(true__, compose(Y2, domain(Y0))), Y2, domain(Y0)) -> f8(f6(true__, Y0), Y0, domain(Y0)) % 19.58/19.30 f8(f6(true__, compose(Y2, g)), Y2, g) -> domain(b) % 19.58/19.30 f8(f6(true__, compose(Y2, h)), Y2, h) -> domain(b) % 19.58/19.30 f8(f6(true__, domain(true__)), f8(f6(true__, true__), true__, domain(true__)), domain(true__)) -> f8(f6(true__, true__), true__, domain(true__)) % 19.58/19.30 f8(true__, X, Y) -> domain(X) % 19.58/19.30 f9(true__, X, Y) -> there_exists(compose(X, Y)) % 19.58/19.30 false__ -> true__ % 19.58/19.30 g -> h % 19.58/19.30 there_exists(X) -> f6(true__, X) % 19.58/19.30 there_exists(compose(a, b)) -> true__ % 19.58/19.30 there_exists(compose(b, h)) -> true__ % 19.58/19.30 with the LPO induced by % 19.58/19.30 codomain > f10 > f9 > f2 > f12 > compose > f5 > f1 > f13 > g > h > a > f11 > b > f4 > equivalent > f7 > there_exists > f6 > f3 > f8 > domain > false__ > true__ % 19.58/19.30 % 19.58/19.30 % SZS output end Proof % 19.58/19.30 %------------------------------------------------------------------------------