Metis---2.4.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : CAT001-2 : TPTP v8.1.0. Released v1.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n022.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:30 EDT 2022

% Result   : Satisfiable 1.35s 1.53s
% Output   : Saturation 1.37s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : CAT001-2 : TPTP v8.1.0. Released v1.0.0.
% 0.03/0.12  % Command  : metis --show proof --show saturation %s
% 0.12/0.33  % Computer : n022.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 600
% 0.12/0.34  % DateTime : Sun May 29 19:41:23 EDT 2022
% 0.12/0.34  % CPUTime  : 
% 0.12/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 1.35/1.53  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.35/1.53  
% 1.35/1.53  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.35/1.53  |- codomain (domain $X) = domain $X
% 1.35/1.53  |- domain (codomain $X) = codomain $X
% 1.35/1.53  |- compose (domain $X) $X = $X
% 1.35/1.53  |- compose $X (codomain $X) = $X
% 1.35/1.53  |- ~(codomain $X = domain $Y) \/ domain (compose $X $Y) = domain $X
% 1.35/1.53  |- ~(codomain $X = domain $Y) \/ codomain (compose $X $Y) = codomain $Y
% 1.35/1.53  |- ~(codomain $X = domain $Y) \/ ~(codomain $Y = domain $Z) \/
% 1.35/1.53     compose $X (compose $Y $Z) = compose (compose $X $Y) $Z
% 1.35/1.53  |- ~(codomain $X = domain a) \/ ~(codomain $Z = domain a) \/
% 1.35/1.53     ~(compose $Z (compose a b) = compose $X (compose a b)) \/ $X = $Z
% 1.35/1.53  |- codomain a = domain b
% 1.35/1.53  |- codomain a = domain h
% 1.35/1.53  |- codomain a = domain g
% 1.35/1.53  |- compose a h = compose a g
% 1.35/1.53  |- ~(codomain $Z = domain $Z) \/
% 1.35/1.53     compose $Z (compose $Z $Z) = compose (compose $Z $Z) $Z
% 1.35/1.53  |- ~(h = g)
% 1.35/1.53  |- compose (codomain a) b = b
% 1.35/1.53  |- compose (codomain $X) (codomain $X) = codomain $X
% 1.35/1.53  |- compose (codomain a) g = g
% 1.35/1.53  |- compose (codomain a) h = h
% 1.35/1.53  |- domain (domain $_2) = domain $_2
% 1.35/1.53  |- codomain (codomain $X) = codomain $X
% 1.35/1.53  |- compose (domain $X) (domain $X) = domain $X
% 1.35/1.53  |- ~(codomain b = codomain a) \/
% 1.35/1.53     compose b (compose b b) = compose (compose b b) b
% 1.35/1.53  |- ~(codomain g = codomain a) \/
% 1.35/1.53     compose g (compose g g) = compose (compose g g) g
% 1.35/1.53  |- ~(codomain g = codomain a) \/
% 1.35/1.53     compose h (compose h h) = compose (compose h h) h
% 1.35/1.53  |- ~(codomain $X = domain $_10) \/
% 1.35/1.53     domain (compose (codomain $X) $_10) = codomain $X
% 1.35/1.53  |- ~(domain $X = domain $_10) \/
% 1.35/1.53     domain (compose (domain $X) $_10) = domain $X
% 1.35/1.53  |- ~(codomain $_9 = codomain a) \/ domain (compose $_9 b) = domain $_9
% 1.35/1.53  |- ~(codomain $_9 = codomain $X) \/
% 1.35/1.53     domain (compose $_9 (codomain $X)) = domain $_9
% 1.35/1.53  |- ~(codomain $_9 = domain $_2) \/
% 1.35/1.53     domain (compose $_9 (domain $_2)) = domain $_9
% 1.35/1.53  |- ~(codomain $_9 = codomain a) \/ domain (compose $_9 g) = domain $_9
% 1.35/1.53  |- ~(codomain $_9 = codomain a) \/ domain (compose $_9 h) = domain $_9
% 1.35/1.53  |- domain (compose a b) = domain a
% 1.35/1.53  |- domain (compose a g) = domain a
% 1.35/1.53  |- ~(codomain $X = domain a) \/
% 1.35/1.53     domain (compose $X (compose a b)) = domain $X
% 1.35/1.53  |- ~(codomain b = domain a) \/
% 1.35/1.53     compose (compose a b) (compose (compose a b) (compose a b)) =
% 1.35/1.53     compose (compose (compose a b) (compose a b)) (compose a b)
% 1.35/1.53  |- compose (domain a) (compose a b) = compose a b
% 1.35/1.53  |- ~(codomain $X = domain a) \/
% 1.35/1.53     domain (compose $X (compose a g)) = domain $X
% 1.35/1.53  |- ~(codomain g = domain a) \/
% 1.35/1.53     compose (compose a g) (compose (compose a g) (compose a g)) =
% 1.35/1.53     compose (compose (compose a g) (compose a g)) (compose a g)
% 1.35/1.53  |- compose (domain a) (compose a g) = compose a g
% 1.35/1.53  |- ~(codomain $X = domain $_12) \/
% 1.35/1.53     codomain (compose (codomain $X) $_12) = codomain $_12
% 1.35/1.53  |- ~(domain $X = domain $_12) \/
% 1.35/1.53     codomain (compose (domain $X) $_12) = codomain $_12
% 1.35/1.53  |- ~(codomain $_11 = codomain a) \/ codomain (compose $_11 b) = codomain b
% 1.35/1.53  |- ~(codomain $_11 = codomain $X) \/
% 1.35/1.53     codomain (compose $_11 (codomain $X)) = codomain $X
% 1.35/1.53  |- ~(codomain $_11 = domain a) \/
% 1.35/1.53     codomain (compose $_11 (compose a b)) = codomain b
% 1.35/1.53  |- ~(codomain $_11 = domain a) \/
% 1.35/1.53     codomain (compose $_11 (compose a g)) = codomain g
% 1.35/1.53  |- ~(codomain $_11 = domain $_2) \/
% 1.35/1.53     codomain (compose $_11 (domain $_2)) = domain $_2
% 1.35/1.53  |- ~(codomain $_11 = codomain a) \/ codomain (compose $_11 g) = codomain g
% 1.35/1.53  |- ~(codomain $_11 = codomain a) \/ codomain (compose $_11 h) = codomain g
% 1.35/1.53  |- codomain (compose a b) = codomain b
% 1.35/1.53  |- codomain (compose a g) = codomain g
% 1.35/1.53  |- codomain g = codomain h
% 1.35/1.53  |- ~(codomain g = domain $Y) \/ codomain (compose h $Y) = codomain $Y
% 1.35/1.53  |- ~(codomain g = domain $Y) \/ domain (compose h $Y) = codomain a
% 1.35/1.53  |- compose h (codomain g) = h
% 1.35/1.53  |- ~(codomain b = domain $Y) \/
% 1.35/1.53     codomain (compose (compose a b) $Y) = codomain $Y
% 1.35/1.53  |- ~(codomain b = domain $Y) \/
% 1.35/1.53     domain (compose (compose a b) $Y) = domain a
% 1.35/1.53  |- compose (compose a b) (codomain b) = compose a b
% 1.35/1.53  |- ~(codomain g = domain $Y) \/
% 1.35/1.53     codomain (compose (compose a g) $Y) = codomain $Y
% 1.35/1.53  |- ~(codomain g = domain $Y) \/
% 1.35/1.53     domain (compose (compose a g) $Y) = domain a
% 1.35/1.53  |- compose (compose a g) (codomain g) = compose a g
% 1.35/1.53  |- ~(codomain $X = codomain a) \/
% 1.35/1.53     domain (compose (codomain $X) b) = codomain $X
% 1.35/1.53  |- ~(codomain b = codomain a) \/
% 1.35/1.53     domain (compose (compose a b) b) = domain a
% 1.35/1.53  |- ~(codomain g = codomain a) \/
% 1.35/1.53     domain (compose (compose a g) b) = domain a
% 1.35/1.53  |- ~(codomain g = codomain a) \/ domain (compose h b) = codomain a
% 1.35/1.53  |- ~(codomain $X = codomain a) \/
% 1.35/1.53     domain (compose (codomain $X) g) = codomain $X
% 1.35/1.53  |- ~(codomain b = codomain a) \/
% 1.35/1.53     domain (compose (compose a b) g) = domain a
% 1.35/1.53  |- ~(codomain g = codomain a) \/
% 1.35/1.53     domain (compose (compose a g) g) = domain a
% 1.35/1.53  |- ~(codomain g = codomain a) \/ domain (compose h g) = codomain a
% 1.35/1.53  |- ~(codomain $X = codomain a) \/
% 1.35/1.53     domain (compose (codomain $X) h) = codomain $X
% 1.35/1.53  |- ~(codomain b = codomain a) \/
% 1.35/1.53     domain (compose (compose a b) h) = domain a
% 1.35/1.53  |- ~(codomain g = codomain a) \/
% 1.35/1.53     domain (compose (compose a g) h) = domain a
% 1.35/1.53  |- ~(codomain g = codomain a) \/ domain (compose h h) = codomain a
% 1.35/1.53  |- ~(codomain $X = codomain a) \/
% 1.35/1.53     codomain (compose (codomain $X) b) = codomain b
% 1.35/1.53  |- ~(codomain b = codomain a) \/
% 1.35/1.53     codomain (compose (compose a b) b) = codomain a
% 1.35/1.53  |- ~(codomain g = codomain a) \/
% 1.35/1.53     codomain (compose (compose a g) b) = codomain b
% 1.35/1.53  |- ~(codomain g = codomain a) \/ codomain (compose h b) = codomain b
% 1.35/1.53  |- ~(codomain $X = codomain a) \/
% 1.35/1.53     codomain (compose (codomain $X) g) = codomain g
% 1.35/1.53  |- ~(codomain b = codomain a) \/
% 1.35/1.53     codomain (compose (compose a b) g) = codomain g
% 1.35/1.53  |- ~(codomain g = codomain a) \/
% 1.35/1.53     codomain (compose (compose a g) g) = codomain a
% 1.35/1.53  |- ~(codomain g = codomain a) \/ codomain (compose h g) = codomain a
% 1.35/1.53  |- ~(codomain $X = codomain a) \/
% 1.35/1.53     codomain (compose (codomain $X) h) = codomain g
% 1.35/1.53  |- ~(codomain b = codomain a) \/
% 1.35/1.53     codomain (compose (compose a b) h) = codomain g
% 1.35/1.53  |- ~(codomain g = codomain a) \/
% 1.35/1.53     codomain (compose (compose a g) h) = codomain a
% 1.35/1.53  |- ~(codomain g = codomain a) \/ codomain (compose h h) = codomain a
% 1.35/1.53  |- ~(codomain b = domain a) \/
% 1.35/1.53     codomain (compose (compose a b) (compose a b)) = codomain b
% 1.35/1.53  |- ~(codomain g = domain a) \/
% 1.35/1.53     codomain (compose (compose a g) (compose a b)) = codomain b
% 1.35/1.53  |- ~(codomain g = domain a) \/
% 1.35/1.53     codomain (compose h (compose a b)) = codomain b
% 1.35/1.53  |- ~(codomain b = domain a) \/
% 1.35/1.53     domain (compose (compose a b) (compose a b)) = codomain b
% 1.35/1.53  |- ~(codomain g = domain a) \/
% 1.35/1.53     domain (compose (compose a g) (compose a b)) = codomain g
% 1.35/1.54  |- ~(codomain g = domain a) \/
% 1.35/1.54     domain (compose h (compose a b)) = codomain a
% 1.35/1.54  |- ~(codomain b = domain a) \/
% 1.35/1.54     domain (compose (compose a b) (compose a g)) = codomain b
% 1.35/1.54  |- ~(codomain g = domain a) \/
% 1.35/1.54     domain (compose (compose a g) (compose a g)) = codomain g
% 1.35/1.54  |- ~(codomain g = domain a) \/
% 1.35/1.54     domain (compose h (compose a g)) = codomain a
% 1.35/1.54  |- ~(codomain g = codomain $X) \/
% 1.35/1.54     codomain (compose h (codomain $X)) = codomain $X
% 1.35/1.54  |- ~(codomain g = domain a) \/
% 1.35/1.54     codomain (compose h (compose a g)) = codomain g
% 1.35/1.54  |- ~(codomain g = codomain $X) \/
% 1.35/1.54     domain (compose h (codomain $X)) = codomain a
% 1.35/1.54  |- ~(codomain $X = domain a) \/
% 1.35/1.54     codomain (compose (codomain $X) (compose a g)) = codomain g
% 1.35/1.54  |- ~(codomain b = domain a) \/
% 1.35/1.54     codomain (compose (compose a b) (compose a g)) = codomain g
% 1.35/1.54  |- ~(codomain g = domain a) \/
% 1.35/1.54     codomain (compose (compose a g) (compose a g)) = codomain g
% 1.35/1.54  |- ~(domain $X = domain a) \/
% 1.35/1.54     codomain (compose (domain $X) (compose a g)) = codomain g
% 1.35/1.54  |- ~(codomain b = codomain $X) \/
% 1.35/1.54     codomain (compose (compose a b) (codomain $X)) = codomain $X
% 1.35/1.54  |- ~(codomain g = codomain $X) \/
% 1.35/1.54     codomain (compose (compose a g) (codomain $X)) = codomain $X
% 1.35/1.54  |- ~(codomain $_36 = domain a) \/
% 1.35/1.54     domain (compose (codomain $_36) (compose a b)) = codomain $_36
% 1.35/1.54  |- ~(codomain $_36 = domain a) \/
% 1.35/1.54     domain (compose (codomain $_36) (compose a g)) = codomain $_36
% 1.35/1.54  |- ~(domain $_38 = domain a) \/
% 1.35/1.54     domain (compose (domain $_38) (compose a b)) = domain $_38
% 1.35/1.54  |- ~(domain $_38 = domain a) \/
% 1.35/1.54     domain (compose (domain $_38) (compose a g)) = domain $_38
% 1.35/1.54  |- ~(codomain b = codomain $_42) \/
% 1.35/1.54     domain (compose (compose a b) (codomain $_42)) = domain a
% 1.35/1.54  |- ~(codomain g = codomain $_42) \/
% 1.35/1.54     domain (compose (compose a g) (codomain $_42)) = domain a
% 1.35/1.54  |- ~(codomain $X = domain $_44) \/
% 1.35/1.54     domain (compose (codomain $X) (domain $_44)) = codomain $X
% 1.35/1.54  |- ~(domain $X = domain $_44) \/
% 1.35/1.54     domain (compose (domain $X) (domain $_44)) = domain $X
% 1.35/1.54  |- ~(codomain $_55 = domain a) \/
% 1.35/1.54     codomain (compose (codomain $_55) (compose a b)) = codomain b
% 1.35/1.54  |- ~(domain $X = domain a) \/
% 1.35/1.54     codomain (compose (domain $X) (compose a b)) = codomain b
% 1.35/1.54  |- ~(domain $_59 = codomain $X) \/
% 1.35/1.54     codomain (compose (domain $_59) (codomain $X)) = codomain $X
% 1.35/1.54  |- ~(domain $_59 = domain $_2) \/
% 1.35/1.54     codomain (compose (domain $_59) (domain $_2)) = domain $_2
% 1.35/1.54  |- ~(codomain $X = codomain $_61) \/
% 1.35/1.54     codomain (compose (codomain $X) (codomain $_61)) = codomain $_61
% 1.35/1.54  |- ~(codomain $X = domain $_64) \/
% 1.35/1.54     codomain (compose (codomain $X) (domain $_64)) = domain $_64
% 1.35/1.54  |- ~(domain $_68 = codomain $X) \/
% 1.35/1.54     domain (compose (domain $_68) (codomain $X)) = domain $_68
% 1.35/1.54  |- ~(codomain $X = codomain $_70) \/
% 1.35/1.54     domain (compose (codomain $X) (codomain $_70)) = codomain $X
% 1.37/1.54  |- ~(codomain $X = domain $_87) \/ ~(codomain $_85 = codomain $X) \/
% 1.37/1.54     compose $_85 (compose (codomain $X) $_87) =
% 1.37/1.54     compose (compose $_85 (codomain $X)) $_87
% 1.37/1.54  |- ~(codomain $_85 = domain a) \/ ~(codomain b = domain $_87) \/
% 1.37/1.54     compose $_85 (compose (compose a b) $_87) =
% 1.37/1.54     compose (compose $_85 (compose a b)) $_87
% 1.37/1.54  |- ~(codomain $_85 = domain a) \/ ~(codomain g = domain $_87) \/
% 1.37/1.54     compose $_85 (compose (compose a g) $_87) =
% 1.37/1.54     compose (compose $_85 (compose a g)) $_87
% 1.37/1.54  |- ~(codomain $_85 = domain $X) \/ ~(domain $X = domain $_87) \/
% 1.37/1.54     compose $_85 (compose (domain $X) $_87) =
% 1.37/1.54     compose (compose $_85 (domain $X)) $_87
% 1.37/1.54  |- ~(codomain $_85 = codomain a) \/ ~(codomain g = domain $_87) \/
% 1.37/1.54     compose $_85 (compose h $_87) = compose (compose $_85 h) $_87
% 1.37/1.54  |- ~(codomain $_85 = domain $_86) \/ ~(codomain $_86 = codomain a) \/
% 1.37/1.54     compose $_85 (compose $_86 b) = compose (compose $_85 $_86) b
% 1.37/1.54  |- ~(codomain $_85 = domain $_86) \/ ~(codomain $_86 = codomain $X) \/
% 1.37/1.54     compose $_85 (compose $_86 (codomain $X)) =
% 1.37/1.54     compose (compose $_85 $_86) (codomain $X)
% 1.37/1.54  |- ~(codomain $_85 = domain $_86) \/ ~(codomain $_86 = domain a) \/
% 1.37/1.54     compose $_85 (compose $_86 (compose a b)) =
% 1.37/1.54     compose (compose $_85 $_86) (compose a b)
% 1.37/1.54  |- ~(codomain $_85 = domain $_86) \/ ~(codomain $_86 = domain a) \/
% 1.37/1.54     compose $_85 (compose $_86 (compose a g)) =
% 1.37/1.54     compose (compose $_85 $_86) (compose a g)
% 1.37/1.54  |- ~(codomain $_85 = domain $_86) \/ ~(codomain $_86 = domain $_2) \/
% 1.37/1.54     compose $_85 (compose $_86 (domain $_2)) =
% 1.37/1.54     compose (compose $_85 $_86) (domain $_2)
% 1.37/1.54  |- ~(codomain $_85 = domain $_86) \/ ~(codomain $_86 = codomain a) \/
% 1.37/1.54     compose $_85 (compose $_86 g) = compose (compose $_85 $_86) g
% 1.37/1.54  |- ~(codomain $_85 = domain $_86) \/ ~(codomain $_86 = codomain a) \/
% 1.37/1.54     compose $_85 (compose $_86 h) = compose (compose $_85 $_86) h
% 1.37/1.54  |- ~(codomain $X = domain $_86) \/ ~(codomain $_86 = domain $_87) \/
% 1.37/1.54     compose (codomain $X) (compose $_86 $_87) =
% 1.37/1.54     compose (compose (codomain $X) $_86) $_87
% 1.37/1.54  |- ~(codomain $_86 = domain $_87) \/ ~(codomain b = domain $_86) \/
% 1.37/1.54     compose (compose a b) (compose $_86 $_87) =
% 1.37/1.54     compose (compose (compose a b) $_86) $_87
% 1.37/1.54  |- ~(codomain $_86 = domain $_87) \/ ~(codomain g = domain $_86) \/
% 1.37/1.54     compose (compose a g) (compose $_86 $_87) =
% 1.37/1.54     compose (compose (compose a g) $_86) $_87
% 1.37/1.54  |- ~(codomain $_86 = domain $_87) \/ ~(domain $X = domain $_86) \/
% 1.37/1.54     compose (domain $X) (compose $_86 $_87) =
% 1.37/1.54     compose (compose (domain $X) $_86) $_87
% 1.37/1.54  |- ~(codomain $_86 = domain $_87) \/ ~(codomain g = domain $_86) \/
% 1.37/1.54     compose h (compose $_86 $_87) = compose (compose h $_86) $_87
% 1.37/1.54  |- ~(codomain $_85 = codomain a) \/ ~(codomain b = domain $_87) \/
% 1.37/1.54     compose $_85 (compose b $_87) = compose (compose $_85 b) $_87
% 1.37/1.54  |- ~(codomain $_85 = codomain a) \/ ~(codomain g = domain $_87) \/
% 1.37/1.54     compose $_85 (compose g $_87) = compose (compose $_85 g) $_87
% 1.37/1.54  |- ~(codomain $X = domain $_87) \/
% 1.37/1.54     compose $X (compose (codomain $X) $_87) = compose $X $_87
% 1.37/1.54  |- ~(codomain b = domain a) \/
% 1.37/1.54     compose b (compose (compose a b) a) =
% 1.37/1.54     compose (compose b (compose a b)) a
% 1.37/1.54  |- ~(codomain g = domain a) \/
% 1.37/1.54     compose g (compose (compose a g) a) =
% 1.37/1.54     compose (compose g (compose a g)) a
% 1.37/1.54  |- ~(codomain $_85 = domain $_87) \/
% 1.37/1.54     compose $_85 $_87 = compose (compose $_85 (domain $_87)) $_87
% 1.37/1.54  |- ~(codomain g = domain $_87) \/
% 1.37/1.54     compose a (compose h $_87) = compose (compose a g) $_87
% 1.37/1.54  |- ~(codomain $_85 = domain $X) \/
% 1.37/1.54     compose $_85 $X = compose (compose $_85 $X) (codomain $X)
% 1.37/1.54  |- ~(codomain a = domain a) \/
% 1.37/1.54     compose a (compose a (compose a b)) =
% 1.37/1.54     compose (compose a a) (compose a b)
% 1.37/1.54  |- ~(codomain a = domain a) \/
% 1.37/1.54     compose a (compose a (compose a g)) =
% 1.37/1.54     compose (compose a a) (compose a g)
% 1.37/1.54  |- ~(codomain $_87 = domain $_87) \/
% 1.37/1.54     compose (codomain $_87) (compose $_87 $_87) =
% 1.37/1.54     compose (compose (codomain $_87) $_87) $_87
% 1.37/1.54  |- ~(codomain b = codomain a) \/
% 1.37/1.54     compose (compose a b) (compose b b) =
% 1.37/1.54     compose (compose (compose a b) b) b
% 1.37/1.54  |- ~(codomain g = codomain a) \/
% 1.37/1.54     compose (compose a g) (compose g g) =
% 1.37/1.54     compose (compose (compose a g) g) g
% 1.37/1.54  |- ~(codomain $_86 = domain $_87) \/
% 1.37/1.54     compose (domain $_86) (compose $_86 $_87) = compose $_86 $_87
% 1.37/1.54  |- ~(codomain g = codomain a) \/
% 1.37/1.54     compose h (compose g g) = compose (compose h g) g
% 1.37/1.55  |- ~(codomain b = domain $_87) \/
% 1.37/1.55     compose a (compose b $_87) = compose (compose a b) $_87
% 1.37/1.55  |- ~(codomain g = domain $_87) \/
% 1.37/1.55     compose a (compose g $_87) = compose (compose a g) $_87
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose a (compose h b) = compose (compose a g) b
% 1.37/1.55  |- ~(codomain g = codomain $X) \/
% 1.37/1.55     compose a (compose h (codomain $X)) =
% 1.37/1.55     compose (compose a g) (codomain $X)
% 1.37/1.55  |- ~(codomain g = domain a) \/
% 1.37/1.55     compose a (compose h (compose a b)) =
% 1.37/1.55     compose (compose a g) (compose a b)
% 1.37/1.55  |- ~(codomain g = domain a) \/
% 1.37/1.55     compose a (compose h (compose a g)) =
% 1.37/1.55     compose (compose a g) (compose a g)
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose a (compose h g) = compose (compose a g) g
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose a (compose h h) = compose (compose a g) h
% 1.37/1.55  |- ~(codomain b = codomain a) \/
% 1.37/1.55     compose a (compose b b) = compose (compose a b) b
% 1.37/1.55  |- ~(codomain b = codomain $X) \/
% 1.37/1.55     compose a (compose b (codomain $X)) =
% 1.37/1.55     compose (compose a b) (codomain $X)
% 1.37/1.55  |- ~(codomain b = domain a) \/
% 1.37/1.55     compose a (compose b (compose a b)) =
% 1.37/1.55     compose (compose a b) (compose a b)
% 1.37/1.55  |- ~(codomain b = domain a) \/
% 1.37/1.55     compose a (compose b (compose a g)) =
% 1.37/1.55     compose (compose a b) (compose a g)
% 1.37/1.55  |- ~(codomain b = codomain a) \/
% 1.37/1.55     compose a (compose b g) = compose (compose a b) g
% 1.37/1.55  |- ~(codomain b = codomain a) \/
% 1.37/1.55     compose a (compose b h) = compose (compose a b) h
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose a (compose g b) = compose (compose a g) b
% 1.37/1.55  |- ~(codomain g = codomain $X) \/
% 1.37/1.55     compose a (compose g (codomain $X)) =
% 1.37/1.55     compose (compose a g) (codomain $X)
% 1.37/1.55  |- ~(codomain g = domain a) \/
% 1.37/1.55     compose a (compose g (compose a b)) =
% 1.37/1.55     compose (compose a g) (compose a b)
% 1.37/1.55  |- ~(codomain g = domain a) \/
% 1.37/1.55     compose a (compose g (compose a g)) =
% 1.37/1.55     compose (compose a g) (compose a g)
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose a (compose g g) = compose (compose a g) g
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose a (compose g h) = compose (compose a g) h
% 1.37/1.55  |- ~(codomain b = domain a) \/
% 1.37/1.55     compose (codomain b) (compose (compose a b) (compose a b)) =
% 1.37/1.55     compose (compose (codomain b) (compose a b)) (compose a b)
% 1.37/1.55  |- ~(codomain g = domain a) \/
% 1.37/1.55     compose (codomain g) (compose (compose a g) (compose a g)) =
% 1.37/1.55     compose (compose (codomain g) (compose a g)) (compose a g)
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose (codomain a) (compose h h) = compose h h
% 1.37/1.55  |- ~(codomain b = codomain a) \/
% 1.37/1.55     compose (codomain a) (compose b b) = compose b b
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose (codomain a) (compose g g) = compose g g
% 1.37/1.55  |- ~(codomain $X = domain $_93) \/
% 1.37/1.55     compose (codomain $X) (compose (codomain $X) $_93) =
% 1.37/1.55     compose (codomain $X) $_93
% 1.37/1.55  |- ~(codomain b = domain $_93) \/
% 1.37/1.55     compose (compose a b) (compose (codomain b) $_93) =
% 1.37/1.55     compose (compose a b) $_93
% 1.37/1.55  |- ~(codomain g = domain $_93) \/
% 1.37/1.55     compose (compose a g) (compose (codomain g) $_93) =
% 1.37/1.55     compose (compose a g) $_93
% 1.37/1.55  |- ~(domain $X = domain $_93) \/
% 1.37/1.55     compose (domain $X) (compose (domain $X) $_93) =
% 1.37/1.55     compose (domain $X) $_93
% 1.37/1.55  |- ~(codomain g = domain $_93) \/
% 1.37/1.55     compose h (compose (codomain g) $_93) = compose h $_93
% 1.37/1.55  |- ~(codomain $_92 = codomain a) \/
% 1.37/1.55     compose $_92 (compose (codomain $_92) b) = compose $_92 b
% 1.37/1.55  |- ~(codomain $_92 = codomain $X) \/
% 1.37/1.55     compose $_92 (compose (codomain $_92) (codomain $X)) =
% 1.37/1.55     compose $_92 (codomain $X)
% 1.37/1.55  |- ~(codomain $_92 = domain a) \/
% 1.37/1.55     compose $_92 (compose (codomain $_92) (compose a b)) =
% 1.37/1.55     compose $_92 (compose a b)
% 1.37/1.55  |- ~(codomain $_92 = domain a) \/
% 1.37/1.55     compose $_92 (compose (codomain $_92) (compose a g)) =
% 1.37/1.55     compose $_92 (compose a g)
% 1.37/1.55  |- ~(codomain $_92 = domain $_2) \/
% 1.37/1.55     compose $_92 (compose (codomain $_92) (domain $_2)) =
% 1.37/1.55     compose $_92 (domain $_2)
% 1.37/1.55  |- ~(codomain $_92 = codomain a) \/
% 1.37/1.55     compose $_92 (compose (codomain $_92) g) = compose $_92 g
% 1.37/1.55  |- ~(codomain $_92 = codomain a) \/
% 1.37/1.55     compose $_92 (compose (codomain $_92) h) = compose $_92 h
% 1.37/1.55  |- ~(codomain g = codomain $X) \/
% 1.37/1.55     compose h (compose (codomain g) (codomain $X)) = compose h (codomain $X)
% 1.37/1.55  |- ~(codomain g = domain a) \/
% 1.37/1.55     compose h (compose (codomain g) (compose a b)) = compose h (compose a b)
% 1.37/1.55  |- ~(codomain g = domain a) \/
% 1.37/1.55     compose h (compose (codomain g) (compose a g)) = compose h (compose a g)
% 1.37/1.55  |- ~(codomain $X = codomain a) \/
% 1.37/1.55     compose (codomain $X) (compose (codomain $X) b) =
% 1.37/1.55     compose (codomain $X) b
% 1.37/1.55  |- ~(codomain $X = codomain a) \/
% 1.37/1.55     compose (codomain $X) (compose (codomain $X) g) =
% 1.37/1.55     compose (codomain $X) g
% 1.37/1.55  |- ~(codomain $X = codomain a) \/
% 1.37/1.55     compose (codomain $X) (compose (codomain $X) h) =
% 1.37/1.55     compose (codomain $X) h
% 1.37/1.55  |- ~(codomain $X = domain $_99) \/
% 1.37/1.55     compose (codomain $X) $_99 =
% 1.37/1.55     compose (compose (codomain $X) (domain $_99)) $_99
% 1.37/1.55  |- ~(domain $X = domain $_99) \/
% 1.37/1.55     compose (domain $X) $_99 =
% 1.37/1.55     compose (compose (domain $X) (domain $_99)) $_99
% 1.37/1.55  |- ~(codomain $_98 = codomain a) \/
% 1.37/1.55     compose $_98 b = compose (compose $_98 (codomain a)) b
% 1.37/1.55  |- ~(codomain $_98 = codomain $X) \/
% 1.37/1.55     compose $_98 (codomain $X) =
% 1.37/1.55     compose (compose $_98 (codomain $X)) (codomain $X)
% 1.37/1.55  |- ~(codomain $_98 = domain a) \/
% 1.37/1.55     compose $_98 (compose a b) =
% 1.37/1.55     compose (compose $_98 (domain a)) (compose a b)
% 1.37/1.55  |- ~(codomain $_98 = domain a) \/
% 1.37/1.55     compose $_98 (compose a g) =
% 1.37/1.55     compose (compose $_98 (domain a)) (compose a g)
% 1.37/1.55  |- ~(codomain $_98 = domain $_2) \/
% 1.37/1.55     compose $_98 (domain $_2) =
% 1.37/1.55     compose (compose $_98 (domain $_2)) (domain $_2)
% 1.37/1.55  |- ~(codomain $_98 = codomain a) \/
% 1.37/1.55     compose $_98 g = compose (compose $_98 (codomain a)) g
% 1.37/1.55  |- ~(codomain $_98 = codomain a) \/
% 1.37/1.55     compose $_98 h = compose (compose $_98 (codomain a)) h
% 1.37/1.55  |- ~(codomain $X = codomain a) \/
% 1.37/1.55     compose (codomain $X) b = compose (compose (codomain $X) (codomain a)) b
% 1.37/1.55  |- ~(codomain b = codomain a) \/
% 1.37/1.55     compose (compose a b) b = compose (compose (compose a b) (codomain a)) b
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose (compose a g) b = compose (compose (compose a g) (codomain a)) b
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose h b = compose (compose h (codomain a)) b
% 1.37/1.55  |- ~(codomain $X = codomain a) \/
% 1.37/1.55     compose (codomain $X) g = compose (compose (codomain $X) (codomain a)) g
% 1.37/1.55  |- ~(codomain b = codomain a) \/
% 1.37/1.55     compose (compose a b) g = compose (compose (compose a b) (codomain a)) g
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose (compose a g) g = compose (compose (compose a g) (codomain a)) g
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose h g = compose (compose h (codomain a)) g
% 1.37/1.55  |- ~(codomain $X = codomain a) \/
% 1.37/1.55     compose (codomain $X) h = compose (compose (codomain $X) (codomain a)) h
% 1.37/1.55  |- ~(codomain b = codomain a) \/
% 1.37/1.55     compose (compose a b) h = compose (compose (compose a b) (codomain a)) h
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose (compose a g) h = compose (compose (compose a g) (codomain a)) h
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose h h = compose (compose h (codomain a)) h
% 1.37/1.55  |- ~(codomain $X = domain $_103) \/
% 1.37/1.55     compose (codomain $X) $_103 =
% 1.37/1.55     compose (compose (codomain $X) $_103) (codomain $_103)
% 1.37/1.55  |- ~(codomain b = domain $_103) \/
% 1.37/1.55     compose (compose a b) $_103 =
% 1.37/1.55     compose (compose (compose a b) $_103) (codomain $_103)
% 1.37/1.55  |- ~(codomain g = domain $_103) \/
% 1.37/1.55     compose (compose a g) $_103 =
% 1.37/1.55     compose (compose (compose a g) $_103) (codomain $_103)
% 1.37/1.55  |- ~(domain $X = domain $_103) \/
% 1.37/1.55     compose (domain $X) $_103 =
% 1.37/1.55     compose (compose (domain $X) $_103) (codomain $_103)
% 1.37/1.55  |- ~(codomain g = domain $_103) \/
% 1.37/1.55     compose h $_103 = compose (compose h $_103) (codomain $_103)
% 1.37/1.55  |- ~(codomain $_104 = codomain a) \/
% 1.37/1.55     compose $_104 b = compose (compose $_104 b) (codomain b)
% 1.37/1.55  |- ~(codomain $_104 = domain a) \/
% 1.37/1.55     compose $_104 (compose a b) =
% 1.37/1.55     compose (compose $_104 (compose a b)) (codomain b)
% 1.37/1.55  |- ~(codomain $_104 = domain a) \/
% 1.37/1.55     compose $_104 (compose a g) =
% 1.37/1.55     compose (compose $_104 (compose a g)) (codomain g)
% 1.37/1.55  |- ~(codomain $_104 = codomain a) \/
% 1.37/1.55     compose $_104 g = compose (compose $_104 g) (codomain g)
% 1.37/1.55  |- ~(codomain $_104 = codomain a) \/
% 1.37/1.55     compose $_104 h = compose (compose $_104 h) (codomain g)
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose h b = compose (compose h b) (codomain b)
% 1.37/1.55  |- ~(codomain g = codomain $X) \/
% 1.37/1.55     compose h (codomain $X) =
% 1.37/1.55     compose (compose h (codomain $X)) (codomain $X)
% 1.37/1.55  |- ~(codomain g = domain a) \/
% 1.37/1.55     compose h (compose a b) = compose (compose h (compose a b)) (codomain b)
% 1.37/1.55  |- ~(codomain g = domain a) \/
% 1.37/1.55     compose h (compose a g) = compose (compose h (compose a g)) (codomain g)
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose h g = compose (compose h g) (codomain a)
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose h h = compose (compose h h) (codomain a)
% 1.37/1.55  |- ~(codomain $X = codomain a) \/
% 1.37/1.55     compose (codomain $X) b = compose (compose (codomain $X) b) (codomain b)
% 1.37/1.55  |- ~(codomain b = codomain a) \/
% 1.37/1.55     compose (compose a b) b = compose (compose (compose a b) b) (codomain a)
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose (compose a g) b = compose (compose (compose a g) b) (codomain b)
% 1.37/1.55  |- ~(codomain $X = codomain a) \/
% 1.37/1.55     compose (codomain $X) g = compose (compose (codomain $X) g) (codomain g)
% 1.37/1.55  |- ~(codomain b = codomain a) \/
% 1.37/1.55     compose (compose a b) g = compose (compose (compose a b) g) (codomain g)
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose (compose a g) g = compose (compose (compose a g) g) (codomain a)
% 1.37/1.55  |- ~(codomain $X = codomain a) \/
% 1.37/1.55     compose (codomain $X) h = compose (compose (codomain $X) h) (codomain g)
% 1.37/1.55  |- ~(codomain b = codomain a) \/
% 1.37/1.55     compose (compose a b) h = compose (compose (compose a b) h) (codomain g)
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose (compose a g) h = compose (compose (compose a g) h) (codomain a)
% 1.37/1.55  |- ~(codomain b = domain $_110) \/
% 1.37/1.55     compose (domain a) (compose (compose a b) $_110) =
% 1.37/1.55     compose (compose a b) $_110
% 1.37/1.55  |- ~(codomain g = domain $_110) \/
% 1.37/1.55     compose (domain a) (compose (compose a g) $_110) =
% 1.37/1.55     compose (compose a g) $_110
% 1.37/1.55  |- ~(codomain g = domain $_110) \/
% 1.37/1.55     compose (codomain a) (compose h $_110) = compose h $_110
% 1.37/1.55  |- ~(codomain $_109 = codomain a) \/
% 1.37/1.55     compose (domain $_109) (compose $_109 b) = compose $_109 b
% 1.37/1.55  |- ~(codomain $_109 = codomain $X) \/
% 1.37/1.55     compose (domain $_109) (compose $_109 (codomain $X)) =
% 1.37/1.55     compose $_109 (codomain $X)
% 1.37/1.55  |- ~(codomain $_109 = domain a) \/
% 1.37/1.55     compose (domain $_109) (compose $_109 (compose a b)) =
% 1.37/1.55     compose $_109 (compose a b)
% 1.37/1.55  |- ~(codomain $_109 = domain a) \/
% 1.37/1.55     compose (domain $_109) (compose $_109 (compose a g)) =
% 1.37/1.55     compose $_109 (compose a g)
% 1.37/1.55  |- ~(codomain $_109 = domain $_2) \/
% 1.37/1.55     compose (domain $_109) (compose $_109 (domain $_2)) =
% 1.37/1.55     compose $_109 (domain $_2)
% 1.37/1.55  |- ~(codomain $_109 = codomain a) \/
% 1.37/1.55     compose (domain $_109) (compose $_109 g) = compose $_109 g
% 1.37/1.55  |- ~(codomain $_109 = codomain a) \/
% 1.37/1.55     compose (domain $_109) (compose $_109 h) = compose $_109 h
% 1.37/1.55  |- ~(codomain g = codomain a) \/
% 1.37/1.55     compose (codomain a) (compose h b) = compose h b
% 1.37/1.55  |- ~(codomain g = codomain $X) \/
% 1.37/1.55     compose (codomain a) (compose h (codomain $X)) = compose h (codomain $X)
% 1.37/1.55  |- ~(codomain g = domain a) \/
% 1.37/1.55     compose (codomain a) (compose h (compose a b)) = compose h (compose a b)
% 1.37/1.55  |- ~(codomain g = domain a) \/
% 1.37/1.55     compose (codomain a) (compose h (compose a g)) = compose h (compose a g)
% 1.37/1.56  |- ~(codomain g = codomain a) \/
% 1.37/1.56     compose (codomain a) (compose h g) = compose h g
% 1.37/1.56  |- ~(codomain b = codomain a) \/
% 1.37/1.56     compose (domain a) (compose (compose a b) b) = compose (compose a b) b
% 1.37/1.56  |- ~(codomain g = codomain a) \/
% 1.37/1.56     compose (domain a) (compose (compose a g) b) = compose (compose a g) b
% 1.37/1.56  |- ~(codomain b = codomain a) \/
% 1.37/1.56     compose (domain a) (compose (compose a b) g) = compose (compose a b) g
% 1.37/1.56  |- ~(codomain g = codomain a) \/
% 1.37/1.56     compose (domain a) (compose (compose a g) g) = compose (compose a g) g
% 1.37/1.56  |- ~(codomain b = codomain a) \/
% 1.37/1.56     compose (domain a) (compose (compose a b) h) = compose (compose a b) h
% 1.37/1.56  |- ~(codomain g = codomain a) \/
% 1.37/1.56     compose (domain a) (compose (compose a g) h) = compose (compose a g) h
% 1.37/1.56  |- ~(codomain b = domain a) \/
% 1.37/1.56     compose (codomain b) (compose (compose a b) (compose a b)) =
% 1.37/1.56     compose (compose a b) (compose a b)
% 1.37/1.56  |- ~(codomain g = domain a) \/
% 1.37/1.56     compose (codomain g) (compose (compose a g) (compose a b)) =
% 1.37/1.56     compose (compose a g) (compose a b)
% 1.37/1.56  |- ~(codomain b = domain a) \/
% 1.37/1.56     compose (codomain b) (compose (compose a b) (compose a g)) =
% 1.37/1.56     compose (compose a b) (compose a g)
% 1.37/1.56  |- ~(codomain g = domain a) \/
% 1.37/1.56     compose (codomain g) (compose (compose a g) (compose a g)) =
% 1.37/1.56     compose (compose a g) (compose a g)
% 1.37/1.56  |- ~(codomain $X = domain a) \/
% 1.37/1.56     compose (codomain $X) (compose a b) =
% 1.37/1.56     compose (compose (codomain $X) (domain a)) (compose a b)
% 1.37/1.56  |- ~(domain $X = domain a) \/
% 1.37/1.56     compose (domain $X) (compose a b) =
% 1.37/1.56     compose (compose (domain $X) (domain a)) (compose a b)
% 1.37/1.56  |- ~(codomain $X = domain a) \/
% 1.37/1.56     compose (codomain $X) (compose a g) =
% 1.37/1.56     compose (compose (codomain $X) (domain a)) (compose a g)
% 1.37/1.56  |- ~(domain $X = domain a) \/
% 1.37/1.56     compose (domain $X) (compose a g) =
% 1.37/1.56     compose (compose (domain $X) (domain a)) (compose a g)
% 1.37/1.56  |- ~(codomain b = codomain $X) \/
% 1.37/1.56     compose (compose a b) (compose (codomain b) (codomain $X)) =
% 1.37/1.56     compose (compose a b) (codomain $X)
% 1.37/1.56  |- ~(codomain b = domain a) \/
% 1.37/1.56     compose (compose a b) (compose (codomain b) (compose a b)) =
% 1.37/1.56     compose (compose a b) (compose a b)
% 1.37/1.56  |- ~(codomain b = domain a) \/
% 1.37/1.56     compose (compose a b) (compose (codomain b) (compose a g)) =
% 1.37/1.56     compose (compose a b) (compose a g)
% 1.37/1.56  |- ~(codomain g = codomain $X) \/
% 1.37/1.56     compose (compose a g) (compose (codomain g) (codomain $X)) =
% 1.37/1.56     compose (compose a g) (codomain $X)
% 1.37/1.56  |- ~(codomain g = domain a) \/
% 1.37/1.56     compose (compose a g) (compose (codomain g) (compose a b)) =
% 1.37/1.56     compose (compose a g) (compose a b)
% 1.37/1.56  |- ~(codomain g = domain a) \/
% 1.37/1.56     compose (compose a g) (compose (codomain g) (compose a g)) =
% 1.37/1.56     compose (compose a g) (compose a g)
% 1.37/1.56  |- ~(codomain $X = domain a) \/
% 1.37/1.56     compose (codomain $X) (compose (codomain $X) (compose a b)) =
% 1.37/1.56     compose (codomain $X) (compose a b)
% 1.37/1.56  |- ~(domain $X = domain a) \/
% 1.37/1.56     compose (domain $X) (compose (domain $X) (compose a b)) =
% 1.37/1.56     compose (domain $X) (compose a b)
% 1.37/1.56  |- ~(codomain $X = domain a) \/
% 1.37/1.56     compose (codomain $X) (compose (codomain $X) (compose a g)) =
% 1.37/1.56     compose (codomain $X) (compose a g)
% 1.37/1.56  |- ~(domain $X = domain a) \/
% 1.37/1.56     compose (domain $X) (compose (domain $X) (compose a g)) =
% 1.37/1.56     compose (domain $X) (compose a g)
% 1.37/1.56  |- ~(codomain b = codomain $X) \/
% 1.37/1.56     compose (compose a b) (codomain $X) =
% 1.37/1.56     compose (compose (compose a b) (codomain $X)) (codomain $X)
% 1.37/1.56  |- ~(codomain b = domain a) \/
% 1.37/1.56     compose (compose a b) (compose a b) =
% 1.37/1.56     compose (compose (compose a b) (compose a b)) (codomain b)
% 1.37/1.56  |- ~(codomain b = domain a) \/
% 1.37/1.56     compose (compose a b) (compose a g) =
% 1.37/1.56     compose (compose (compose a b) (compose a g)) (codomain g)
% 1.37/1.56  |- ~(codomain g = codomain $X) \/
% 1.37/1.56     compose (compose a g) (codomain $X) =
% 1.37/1.56     compose (compose (compose a g) (codomain $X)) (codomain $X)
% 1.37/1.56  |- ~(codomain g = domain a) \/
% 1.37/1.56     compose (compose a g) (compose a b) =
% 1.37/1.56     compose (compose (compose a g) (compose a b)) (codomain b)
% 1.37/1.56  |- ~(codomain g = domain a) \/
% 1.37/1.56     compose (compose a g) (compose a g) =
% 1.37/1.56     compose (compose (compose a g) (compose a g)) (codomain g)
% 1.37/1.56  |- ~(codomain $X = domain a) \/
% 1.37/1.56     compose (codomain $X) (compose a b) =
% 1.37/1.56     compose (compose (codomain $X) (compose a b)) (codomain b)
% 1.37/1.56  |- ~(domain $X = domain a) \/
% 1.37/1.56     compose (domain $X) (compose a b) =
% 1.37/1.56     compose (compose (domain $X) (compose a b)) (codomain b)
% 1.37/1.56  |- ~(codomain $X = domain a) \/
% 1.37/1.56     compose (codomain $X) (compose a g) =
% 1.37/1.56     compose (compose (codomain $X) (compose a g)) (codomain g)
% 1.37/1.56  |- ~(domain $X = domain a) \/
% 1.37/1.56     compose (domain $X) (compose a g) =
% 1.37/1.56     compose (compose (domain $X) (compose a g)) (codomain g)
% 1.37/1.56  |- ~(codomain b = codomain $X) \/
% 1.37/1.56     compose (domain a) (compose (compose a b) (codomain $X)) =
% 1.37/1.56     compose (compose a b) (codomain $X)
% 1.37/1.56  |- ~(codomain g = codomain $X) \/
% 1.37/1.56     compose (domain a) (compose (compose a g) (codomain $X)) =
% 1.37/1.56     compose (compose a g) (codomain $X)
% 1.37/1.56  |- ~(codomain b = codomain a) \/ b = compose b (codomain a)
% 1.37/1.56  |- ~(codomain g = codomain a) \/ g = compose g (codomain a)
% 1.37/1.56  |- ~(codomain g = codomain a) \/ h = compose h (codomain a)
% 1.37/1.56  |- ~(codomain $_162 = codomain $X) \/
% 1.37/1.56     compose (codomain $_162) (codomain $X) =
% 1.37/1.56     compose (compose (codomain $_162) (codomain $X)) (codomain $X)
% 1.37/1.56  |- ~(domain $_164 = codomain $X) \/
% 1.37/1.56     compose (domain $_164) (codomain $X) =
% 1.37/1.56     compose (compose (domain $_164) (codomain $X)) (codomain $X)
% 1.37/1.56  |- ~(domain $_164 = domain $_2) \/
% 1.37/1.56     compose (domain $_164) (domain $_2) =
% 1.37/1.56     compose (compose (domain $_164) (domain $_2)) (domain $_2)
% 1.37/1.56  |- ~(codomain $X = domain $_168) \/
% 1.37/1.56     compose (codomain $X) (domain $_168) =
% 1.37/1.56     compose (compose (codomain $X) (domain $_168)) (domain $_168)
% 1.37/1.56  |- ~(codomain $_170 = codomain $X) \/
% 1.37/1.56     compose (codomain $_170) (compose (codomain $_170) (codomain $X)) =
% 1.37/1.56     compose (codomain $_170) (codomain $X)
% 1.37/1.56  |- ~(domain $_172 = codomain $X) \/
% 1.37/1.56     compose (domain $_172) (compose (domain $_172) (codomain $X)) =
% 1.37/1.56     compose (domain $_172) (codomain $X)
% 1.37/1.56  |- ~(domain $_172 = domain $_2) \/
% 1.37/1.56     compose (domain $_172) (compose (domain $_172) (domain $_2)) =
% 1.37/1.56     compose (domain $_172) (domain $_2)
% 1.37/1.56  |- ~(codomain $X = domain $_176) \/
% 1.37/1.56     compose (codomain $X) (compose (codomain $X) (domain $_176)) =
% 1.37/1.56     compose (codomain $X) (domain $_176)
% 1.37/1.56  |- ~(codomain $_186 = domain a) \/
% 1.37/1.56     ~(compose a b = compose $_186 (compose a b)) \/ $_186 = domain a
% 1.37/1.56  |- ~(codomain $_209 = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.56     compose $_209 (compose h b) = compose (compose $_209 h) b
% 1.37/1.56  |- ~(codomain $_209 = codomain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.56     compose $_209 (compose h (codomain $X)) =
% 1.37/1.56     compose (compose $_209 h) (codomain $X)
% 1.37/1.56  |- ~(codomain $_209 = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.56     compose $_209 (compose h (compose a b)) =
% 1.37/1.56     compose (compose $_209 h) (compose a b)
% 1.37/1.56  |- ~(codomain $_209 = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.56     compose $_209 (compose h (compose a g)) =
% 1.37/1.56     compose (compose $_209 h) (compose a g)
% 1.37/1.56  |- ~(codomain $_209 = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.56     compose $_209 (compose h g) = compose (compose $_209 h) g
% 1.37/1.56  |- ~(codomain $_209 = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.56     compose $_209 (compose h h) = compose (compose $_209 h) h
% 1.37/1.56  |- ~(codomain $X = codomain a) \/ ~(codomain g = domain $_210) \/
% 1.37/1.56     compose (codomain $X) (compose h $_210) =
% 1.37/1.56     compose (compose (codomain $X) h) $_210
% 1.37/1.56  |- ~(codomain b = codomain a) \/ ~(codomain g = domain $_210) \/
% 1.37/1.56     compose (compose a b) (compose h $_210) =
% 1.37/1.56     compose (compose (compose a b) h) $_210
% 1.37/1.56  |- ~(codomain a = domain $_210) \/ ~(codomain g = codomain a) \/
% 1.37/1.56     compose (compose a g) (compose h $_210) =
% 1.37/1.56     compose (compose (compose a g) h) $_210
% 1.37/1.56  |- ~(codomain g = codomain a) \/
% 1.37/1.56     compose g (compose h b) = compose (compose g h) b
% 1.37/1.56  |- ~(codomain g = codomain a) \/
% 1.37/1.56     compose g (compose h (codomain a)) = compose (compose g h) (codomain a)
% 1.37/1.56  |- ~(codomain g = codomain a) \/
% 1.37/1.56     compose g (compose h g) = compose (compose g h) g
% 1.37/1.56  |- ~(codomain g = codomain a) \/
% 1.37/1.56     compose g (compose h h) = compose (compose g h) h
% 1.37/1.56  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.56     compose (codomain $X) (compose h b) =
% 1.37/1.56     compose (compose (codomain $X) h) b
% 1.37/1.56  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.56     compose (compose a b) (compose h b) =
% 1.37/1.56     compose (compose (compose a b) h) b
% 1.37/1.56  |- ~(codomain g = codomain a) \/
% 1.37/1.56     compose (compose a g) (compose h b) =
% 1.37/1.56     compose (compose (compose a g) h) b
% 1.37/1.56  |- ~(codomain g = codomain a) \/
% 1.37/1.56     compose h (compose h b) = compose (compose h h) b
% 1.37/1.56  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.56     compose (codomain $X) (compose h g) =
% 1.37/1.56     compose (compose (codomain $X) h) g
% 1.37/1.56  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.56     compose (compose a b) (compose h g) =
% 1.37/1.56     compose (compose (compose a b) h) g
% 1.37/1.56  |- ~(codomain g = codomain a) \/
% 1.37/1.56     compose (compose a g) (compose h g) =
% 1.37/1.56     compose (compose (compose a g) h) g
% 1.37/1.56  |- ~(codomain g = codomain a) \/
% 1.37/1.56     compose h (compose h g) = compose (compose h h) g
% 1.37/1.56  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.56     compose (codomain $X) (compose h h) =
% 1.37/1.56     compose (compose (codomain $X) h) h
% 1.37/1.56  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.56     compose (compose a b) (compose h h) =
% 1.37/1.56     compose (compose (compose a b) h) h
% 1.37/1.56  |- ~(codomain g = codomain a) \/
% 1.37/1.56     compose (compose a g) (compose h h) =
% 1.37/1.56     compose (compose (compose a g) h) h
% 1.37/1.56  |- ~(codomain $X = domain $_215) \/ ~(codomain $_215 = codomain a) \/
% 1.37/1.56     compose (codomain $X) (compose $_215 b) =
% 1.37/1.56     compose (compose (codomain $X) $_215) b
% 1.37/1.56  |- ~(codomain $_215 = codomain a) \/ ~(codomain b = domain $_215) \/
% 1.37/1.56     compose (compose a b) (compose $_215 b) =
% 1.37/1.56     compose (compose (compose a b) $_215) b
% 1.37/1.56  |- ~(codomain $_215 = codomain a) \/ ~(codomain g = domain $_215) \/
% 1.37/1.56     compose (compose a g) (compose $_215 b) =
% 1.37/1.56     compose (compose (compose a g) $_215) b
% 1.37/1.56  |- ~(codomain $_215 = codomain a) \/ ~(codomain g = domain $_215) \/
% 1.37/1.56     compose h (compose $_215 b) = compose (compose h $_215) b
% 1.37/1.56  |- ~(codomain $_214 = codomain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.56     compose $_214 (compose b b) = compose (compose $_214 b) b
% 1.37/1.56  |- ~(codomain $X = codomain a) \/ ~(codomain $_214 = codomain $X) \/
% 1.37/1.56     compose $_214 (compose (codomain $X) b) =
% 1.37/1.56     compose (compose $_214 (codomain $X)) b
% 1.37/1.56  |- ~(codomain $_214 = domain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.56     compose $_214 (compose (compose a b) b) =
% 1.37/1.56     compose (compose $_214 (compose a b)) b
% 1.37/1.57  |- ~(codomain $_214 = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose $_214 (compose (compose a g) b) =
% 1.37/1.57     compose (compose $_214 (compose a g)) b
% 1.37/1.57  |- ~(codomain $_214 = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose $_214 (compose g b) = compose (compose $_214 g) b
% 1.37/1.57  |- ~(codomain $X = codomain a) \/
% 1.37/1.57     compose a (compose (codomain $X) b) =
% 1.37/1.57     compose (compose a (codomain $X)) b
% 1.37/1.57  |- ~(codomain g = codomain a) \/
% 1.37/1.57     compose g (compose g b) = compose (compose g g) b
% 1.37/1.57  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose b b) = compose (compose h b) b
% 1.37/1.57  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.57     compose h (compose (codomain $X) b) =
% 1.37/1.57     compose (compose h (codomain $X)) b
% 1.37/1.57  |- ~(codomain b = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.57     compose h (compose (compose a b) b) =
% 1.37/1.57     compose (compose h (compose a b)) b
% 1.37/1.57  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose (compose a g) b) =
% 1.37/1.57     compose (compose h (compose a g)) b
% 1.37/1.57  |- ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose g b) = compose (compose h g) b
% 1.37/1.57  |- ~(codomain $X = codomain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.57     compose (codomain $X) (compose b b) =
% 1.37/1.57     compose (compose (codomain $X) b) b
% 1.37/1.57  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose (compose a g) (compose b b) =
% 1.37/1.57     compose (compose (compose a g) b) b
% 1.37/1.57  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose (codomain $X) (compose g b) =
% 1.37/1.57     compose (compose (codomain $X) g) b
% 1.37/1.57  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose (compose a b) (compose g b) =
% 1.37/1.57     compose (compose (compose a b) g) b
% 1.37/1.57  |- ~(codomain g = codomain a) \/
% 1.37/1.57     compose (compose a g) (compose g b) =
% 1.37/1.57     compose (compose (compose a g) g) b
% 1.37/1.57  |- ~(codomain g = codomain a) \/
% 1.37/1.57     compose (codomain a) (compose g b) = compose g b
% 1.37/1.57  |- ~(codomain $X = domain $_221) \/ ~(codomain $_221 = codomain a) \/
% 1.37/1.57     compose (codomain $X) (compose $_221 g) =
% 1.37/1.57     compose (compose (codomain $X) $_221) g
% 1.37/1.57  |- ~(codomain $_221 = codomain a) \/ ~(codomain b = domain $_221) \/
% 1.37/1.57     compose (compose a b) (compose $_221 g) =
% 1.37/1.57     compose (compose (compose a b) $_221) g
% 1.37/1.57  |- ~(codomain $_221 = codomain a) \/ ~(codomain g = domain $_221) \/
% 1.37/1.57     compose (compose a g) (compose $_221 g) =
% 1.37/1.57     compose (compose (compose a g) $_221) g
% 1.37/1.57  |- ~(codomain $_221 = codomain a) \/ ~(codomain g = domain $_221) \/
% 1.37/1.57     compose h (compose $_221 g) = compose (compose h $_221) g
% 1.37/1.57  |- ~(codomain $_220 = codomain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.57     compose $_220 (compose b g) = compose (compose $_220 b) g
% 1.37/1.57  |- ~(codomain $X = codomain a) \/ ~(codomain $_220 = codomain $X) \/
% 1.37/1.57     compose $_220 (compose (codomain $X) g) =
% 1.37/1.57     compose (compose $_220 (codomain $X)) g
% 1.37/1.57  |- ~(codomain $_220 = domain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.57     compose $_220 (compose (compose a b) g) =
% 1.37/1.57     compose (compose $_220 (compose a b)) g
% 1.37/1.57  |- ~(codomain $_220 = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose $_220 (compose (compose a g) g) =
% 1.37/1.57     compose (compose $_220 (compose a g)) g
% 1.37/1.57  |- ~(codomain $_220 = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose $_220 (compose g g) = compose (compose $_220 g) g
% 1.37/1.57  |- ~(codomain b = codomain a) \/
% 1.37/1.57     compose b (compose b g) = compose (compose b b) g
% 1.37/1.57  |- ~(codomain $X = codomain a) \/
% 1.37/1.57     compose a (compose (codomain $X) g) =
% 1.37/1.57     compose (compose a (codomain $X)) g
% 1.37/1.57  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose b g) = compose (compose h b) g
% 1.37/1.57  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.57     compose h (compose (codomain $X) g) =
% 1.37/1.57     compose (compose h (codomain $X)) g
% 1.37/1.57  |- ~(codomain b = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.57     compose h (compose (compose a b) g) =
% 1.37/1.57     compose (compose h (compose a b)) g
% 1.37/1.57  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose (compose a g) g) =
% 1.37/1.57     compose (compose h (compose a g)) g
% 1.37/1.57  |- ~(codomain $X = codomain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.57     compose (codomain $X) (compose b g) =
% 1.37/1.57     compose (compose (codomain $X) b) g
% 1.37/1.57  |- ~(codomain b = codomain a) \/
% 1.37/1.57     compose (compose a b) (compose b g) =
% 1.37/1.57     compose (compose (compose a b) b) g
% 1.37/1.57  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose (compose a g) (compose b g) =
% 1.37/1.57     compose (compose (compose a g) b) g
% 1.37/1.57  |- ~(codomain b = codomain a) \/
% 1.37/1.57     compose (codomain a) (compose b g) = compose b g
% 1.37/1.57  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose (codomain $X) (compose g g) =
% 1.37/1.57     compose (compose (codomain $X) g) g
% 1.37/1.57  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose (compose a b) (compose g g) =
% 1.37/1.57     compose (compose (compose a b) g) g
% 1.37/1.57  |- ~(codomain $X = domain $_227) \/ ~(codomain $_227 = codomain a) \/
% 1.37/1.57     compose (codomain $X) (compose $_227 h) =
% 1.37/1.57     compose (compose (codomain $X) $_227) h
% 1.37/1.57  |- ~(codomain $_227 = codomain a) \/ ~(codomain b = domain $_227) \/
% 1.37/1.57     compose (compose a b) (compose $_227 h) =
% 1.37/1.57     compose (compose (compose a b) $_227) h
% 1.37/1.57  |- ~(codomain $_227 = codomain a) \/ ~(codomain g = domain $_227) \/
% 1.37/1.57     compose (compose a g) (compose $_227 h) =
% 1.37/1.57     compose (compose (compose a g) $_227) h
% 1.37/1.57  |- ~(codomain $_227 = codomain a) \/ ~(codomain g = domain $_227) \/
% 1.37/1.57     compose h (compose $_227 h) = compose (compose h $_227) h
% 1.37/1.57  |- ~(codomain $_226 = codomain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.57     compose $_226 (compose b h) = compose (compose $_226 b) h
% 1.37/1.57  |- ~(codomain $X = codomain a) \/ ~(codomain $_226 = codomain $X) \/
% 1.37/1.57     compose $_226 (compose (codomain $X) h) =
% 1.37/1.57     compose (compose $_226 (codomain $X)) h
% 1.37/1.57  |- ~(codomain $_226 = domain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.57     compose $_226 (compose (compose a b) h) =
% 1.37/1.57     compose (compose $_226 (compose a b)) h
% 1.37/1.57  |- ~(codomain $_226 = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose $_226 (compose (compose a g) h) =
% 1.37/1.57     compose (compose $_226 (compose a g)) h
% 1.37/1.57  |- ~(codomain $_226 = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose $_226 (compose g h) = compose (compose $_226 g) h
% 1.37/1.57  |- ~(codomain b = codomain a) \/
% 1.37/1.57     compose b (compose b h) = compose (compose b b) h
% 1.37/1.57  |- ~(codomain $X = codomain a) \/
% 1.37/1.57     compose a (compose (codomain $X) h) =
% 1.37/1.57     compose (compose a (codomain $X)) h
% 1.37/1.57  |- ~(codomain g = codomain a) \/
% 1.37/1.57     compose g (compose g h) = compose (compose g g) h
% 1.37/1.57  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose b h) = compose (compose h b) h
% 1.37/1.57  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.57     compose h (compose (codomain $X) h) =
% 1.37/1.57     compose (compose h (codomain $X)) h
% 1.37/1.57  |- ~(codomain b = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.57     compose h (compose (compose a b) h) =
% 1.37/1.57     compose (compose h (compose a b)) h
% 1.37/1.57  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose (compose a g) h) =
% 1.37/1.57     compose (compose h (compose a g)) h
% 1.37/1.57  |- ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose g h) = compose (compose h g) h
% 1.37/1.57  |- ~(codomain $X = codomain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.57     compose (codomain $X) (compose b h) =
% 1.37/1.57     compose (compose (codomain $X) b) h
% 1.37/1.57  |- ~(codomain b = codomain a) \/
% 1.37/1.57     compose (compose a b) (compose b h) =
% 1.37/1.57     compose (compose (compose a b) b) h
% 1.37/1.57  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose (compose a g) (compose b h) =
% 1.37/1.57     compose (compose (compose a g) b) h
% 1.37/1.57  |- ~(codomain b = codomain a) \/
% 1.37/1.57     compose (codomain a) (compose b h) = compose b h
% 1.37/1.57  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose (codomain $X) (compose g h) =
% 1.37/1.57     compose (compose (codomain $X) g) h
% 1.37/1.57  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose (compose a b) (compose g h) =
% 1.37/1.57     compose (compose (compose a b) g) h
% 1.37/1.57  |- ~(codomain g = codomain a) \/
% 1.37/1.57     compose (compose a g) (compose g h) =
% 1.37/1.57     compose (compose (compose a g) g) h
% 1.37/1.57  |- ~(codomain g = codomain a) \/
% 1.37/1.57     compose (codomain a) (compose g h) = compose g h
% 1.37/1.57  |- ~(codomain b = domain $_233) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose b $_233) = compose (compose h b) $_233
% 1.37/1.57  |- ~(codomain $X = domain $_233) \/ ~(codomain g = codomain $X) \/
% 1.37/1.57     compose h (compose (codomain $X) $_233) =
% 1.37/1.57     compose (compose h (codomain $X)) $_233
% 1.37/1.57  |- ~(codomain b = domain $_233) \/ ~(codomain g = domain a) \/
% 1.37/1.57     compose h (compose (compose a b) $_233) =
% 1.37/1.57     compose (compose h (compose a b)) $_233
% 1.37/1.57  |- ~(codomain g = domain $_233) \/ ~(codomain g = domain a) \/
% 1.37/1.57     compose h (compose (compose a g) $_233) =
% 1.37/1.57     compose (compose h (compose a g)) $_233
% 1.37/1.57  |- ~(codomain a = domain $_233) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose g $_233) = compose (compose h g) $_233
% 1.37/1.57  |- ~(codomain a = domain $_233) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose h $_233) = compose (compose h h) $_233
% 1.37/1.57  |- ~(codomain $_232 = codomain $X) \/ ~(codomain g = domain $_232) \/
% 1.37/1.57     compose h (compose $_232 (codomain $X)) =
% 1.37/1.57     compose (compose h $_232) (codomain $X)
% 1.37/1.57  |- ~(codomain $_232 = domain a) \/ ~(codomain g = domain $_232) \/
% 1.37/1.57     compose h (compose $_232 (compose a b)) =
% 1.37/1.57     compose (compose h $_232) (compose a b)
% 1.37/1.57  |- ~(codomain $_232 = domain a) \/ ~(codomain g = domain $_232) \/
% 1.37/1.57     compose h (compose $_232 (compose a g)) =
% 1.37/1.57     compose (compose h $_232) (compose a g)
% 1.37/1.57  |- ~(codomain g = domain a) \/
% 1.37/1.57     compose h (compose (compose a g) a) =
% 1.37/1.57     compose (compose h (compose a g)) a
% 1.37/1.57  |- ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose g (codomain a)) = compose (compose h g) (codomain a)
% 1.37/1.57  |- ~(codomain b = codomain $X) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose b (codomain $X)) =
% 1.37/1.57     compose (compose h b) (codomain $X)
% 1.37/1.57  |- ~(codomain b = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose b (compose a b)) =
% 1.37/1.57     compose (compose h b) (compose a b)
% 1.37/1.57  |- ~(codomain b = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose b (compose a g)) =
% 1.37/1.57     compose (compose h b) (compose a g)
% 1.37/1.57  |- ~(codomain a = codomain $X) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose g (codomain $X)) =
% 1.37/1.57     compose (compose h g) (codomain $X)
% 1.37/1.57  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose g (compose a b)) =
% 1.37/1.57     compose (compose h g) (compose a b)
% 1.37/1.57  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose g (compose a g)) =
% 1.37/1.57     compose (compose h g) (compose a g)
% 1.37/1.57  |- ~(codomain a = codomain $X) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose h (codomain $X)) =
% 1.37/1.57     compose (compose h h) (codomain $X)
% 1.37/1.57  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose h (compose a b)) =
% 1.37/1.57     compose (compose h h) (compose a b)
% 1.37/1.57  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose h (compose a g)) =
% 1.37/1.57     compose (compose h h) (compose a g)
% 1.37/1.57  |- ~(codomain g = codomain a) \/
% 1.37/1.57     compose h (compose h (codomain a)) = compose (compose h h) (codomain a)
% 1.37/1.57  |- ~(codomain $_237 = codomain a) \/ ~(codomain b = codomain $X) \/
% 1.37/1.57     compose $_237 (compose b (codomain $X)) =
% 1.37/1.57     compose (compose $_237 b) (codomain $X)
% 1.37/1.57  |- ~(codomain $_237 = codomain a) \/ ~(codomain b = domain a) \/
% 1.37/1.57     compose $_237 (compose b (compose a b)) =
% 1.37/1.57     compose (compose $_237 b) (compose a b)
% 1.37/1.57  |- ~(codomain $_237 = codomain a) \/ ~(codomain b = domain a) \/
% 1.37/1.57     compose $_237 (compose b (compose a g)) =
% 1.37/1.57     compose (compose $_237 b) (compose a g)
% 1.37/1.57  |- ~(codomain $X = codomain a) \/ ~(codomain b = domain $_238) \/
% 1.37/1.57     compose (codomain $X) (compose b $_238) =
% 1.37/1.57     compose (compose (codomain $X) b) $_238
% 1.37/1.57  |- ~(codomain a = domain $_238) \/ ~(codomain b = codomain a) \/
% 1.37/1.57     compose (compose a b) (compose b $_238) =
% 1.37/1.57     compose (compose (compose a b) b) $_238
% 1.37/1.57  |- ~(codomain b = domain $_238) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose (compose a g) (compose b $_238) =
% 1.37/1.57     compose (compose (compose a g) b) $_238
% 1.37/1.57  |- ~(codomain b = codomain a) \/
% 1.37/1.57     compose b (compose b (codomain a)) = compose (compose b b) (codomain a)
% 1.37/1.57  |- ~(codomain b = domain $_238) \/
% 1.37/1.57     compose (codomain a) (compose b $_238) = compose b $_238
% 1.37/1.57  |- ~(codomain b = codomain $X) \/
% 1.37/1.57     compose (codomain a) (compose b (codomain $X)) = compose b (codomain $X)
% 1.37/1.57  |- ~(codomain b = domain a) \/
% 1.37/1.57     compose (codomain a) (compose b (compose a b)) = compose b (compose a b)
% 1.37/1.57  |- ~(codomain b = domain a) \/
% 1.37/1.57     compose (codomain a) (compose b (compose a g)) = compose b (compose a g)
% 1.37/1.57  |- ~(codomain $_241 = codomain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.57     compose $_241 (compose g (codomain $X)) =
% 1.37/1.57     compose (compose $_241 g) (codomain $X)
% 1.37/1.57  |- ~(codomain $_241 = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.57     compose $_241 (compose g (compose a b)) =
% 1.37/1.57     compose (compose $_241 g) (compose a b)
% 1.37/1.57  |- ~(codomain $_241 = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.57     compose $_241 (compose g (compose a g)) =
% 1.37/1.57     compose (compose $_241 g) (compose a g)
% 1.37/1.57  |- ~(codomain $X = codomain a) \/ ~(codomain g = domain $_242) \/
% 1.37/1.57     compose (codomain $X) (compose g $_242) =
% 1.37/1.57     compose (compose (codomain $X) g) $_242
% 1.37/1.57  |- ~(codomain b = codomain a) \/ ~(codomain g = domain $_242) \/
% 1.37/1.57     compose (compose a b) (compose g $_242) =
% 1.37/1.57     compose (compose (compose a b) g) $_242
% 1.37/1.57  |- ~(codomain a = domain $_242) \/ ~(codomain g = codomain a) \/
% 1.37/1.57     compose (compose a g) (compose g $_242) =
% 1.37/1.57     compose (compose (compose a g) g) $_242
% 1.37/1.57  |- ~(codomain g = codomain a) \/
% 1.37/1.57     compose g (compose g (codomain a)) = compose (compose g g) (codomain a)
% 1.37/1.57  |- ~(codomain g = domain $_242) \/
% 1.37/1.57     compose (codomain a) (compose g $_242) = compose g $_242
% 1.37/1.58  |- ~(codomain g = codomain $X) \/
% 1.37/1.58     compose (codomain a) (compose g (codomain $X)) = compose g (codomain $X)
% 1.37/1.58  |- ~(codomain g = domain a) \/
% 1.37/1.58     compose (codomain a) (compose g (compose a b)) = compose g (compose a b)
% 1.37/1.58  |- ~(codomain g = domain a) \/
% 1.37/1.58     compose (codomain a) (compose g (compose a g)) = compose g (compose a g)
% 1.37/1.58  |- ~(codomain $X = codomain a) \/ ~(codomain b = domain a) \/
% 1.37/1.58     compose (codomain $X) (compose b (compose a b)) =
% 1.37/1.58     compose (compose (codomain $X) b) (compose a b)
% 1.37/1.58  |- ~(codomain a = domain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.58     compose (compose a b) (compose b (compose a b)) =
% 1.37/1.58     compose (compose (compose a b) b) (compose a b)
% 1.37/1.58  |- ~(codomain b = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose b (compose a b)) =
% 1.37/1.58     compose (compose (compose a g) b) (compose a b)
% 1.37/1.58  |- ~(codomain $X = codomain a) \/ ~(codomain b = domain a) \/
% 1.37/1.58     compose (codomain $X) (compose b (compose a g)) =
% 1.37/1.58     compose (compose (codomain $X) b) (compose a g)
% 1.37/1.58  |- ~(codomain a = domain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.58     compose (compose a b) (compose b (compose a g)) =
% 1.37/1.58     compose (compose (compose a b) b) (compose a g)
% 1.37/1.58  |- ~(codomain b = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose b (compose a g)) =
% 1.37/1.58     compose (compose (compose a g) b) (compose a g)
% 1.37/1.58  |- ~(codomain a = codomain $X) \/ ~(codomain b = codomain a) \/
% 1.37/1.58     compose (compose a b) (compose b (codomain $X)) =
% 1.37/1.58     compose (compose (compose a b) b) (codomain $X)
% 1.37/1.58  |- ~(codomain b = codomain a) \/
% 1.37/1.58     compose (compose a b) (compose b (codomain a)) =
% 1.37/1.58     compose (compose (compose a b) b) (codomain a)
% 1.37/1.58  |- ~(codomain b = codomain $X) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose b (codomain $X)) =
% 1.37/1.58     compose (compose (compose a g) b) (codomain $X)
% 1.37/1.58  |- ~(codomain $X = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.58     compose (codomain $X) (compose g (compose a b)) =
% 1.37/1.58     compose (compose (codomain $X) g) (compose a b)
% 1.37/1.58  |- ~(codomain b = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.58     compose (compose a b) (compose g (compose a b)) =
% 1.37/1.58     compose (compose (compose a b) g) (compose a b)
% 1.37/1.58  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose g (compose a b)) =
% 1.37/1.58     compose (compose (compose a g) g) (compose a b)
% 1.37/1.58  |- ~(codomain $X = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.58     compose (codomain $X) (compose g (compose a g)) =
% 1.37/1.58     compose (compose (codomain $X) g) (compose a g)
% 1.37/1.58  |- ~(codomain b = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.58     compose (compose a b) (compose g (compose a g)) =
% 1.37/1.58     compose (compose (compose a b) g) (compose a g)
% 1.37/1.58  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose g (compose a g)) =
% 1.37/1.58     compose (compose (compose a g) g) (compose a g)
% 1.37/1.58  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.58     compose (compose a b) (compose g (codomain $X)) =
% 1.37/1.58     compose (compose (compose a b) g) (codomain $X)
% 1.37/1.58  |- ~(codomain a = codomain $X) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose g (codomain $X)) =
% 1.37/1.58     compose (compose (compose a g) g) (codomain $X)
% 1.37/1.58  |- ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose g (codomain a)) =
% 1.37/1.58     compose (compose (compose a g) g) (codomain a)
% 1.37/1.58  |- ~(codomain $X = codomain a) \/ ~(codomain b = codomain $X) \/
% 1.37/1.58     compose (compose a b) (compose (codomain $X) b) =
% 1.37/1.58     compose (compose (compose a b) (codomain $X)) b
% 1.37/1.58  |- ~(codomain a = domain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.58     compose (compose a b) (compose (compose a b) b) =
% 1.37/1.58     compose (compose (compose a b) (compose a b)) b
% 1.37/1.58  |- ~(codomain b = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a b) (compose (compose a g) b) =
% 1.37/1.58     compose (compose (compose a b) (compose a g)) b
% 1.37/1.58  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.58     compose (compose a g) (compose (codomain $X) b) =
% 1.37/1.58     compose (compose (compose a g) (codomain $X)) b
% 1.37/1.58  |- ~(codomain b = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.58     compose (compose a g) (compose (compose a b) b) =
% 1.37/1.58     compose (compose (compose a g) (compose a b)) b
% 1.37/1.58  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose (compose a g) b) =
% 1.37/1.58     compose (compose (compose a g) (compose a g)) b
% 1.37/1.58  |- ~(codomain $X = domain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.58     compose (codomain $X) (compose (compose a b) b) =
% 1.37/1.58     compose (compose (codomain $X) (compose a b)) b
% 1.37/1.58  |- ~(codomain b = codomain a) \/ ~(domain $X = domain a) \/
% 1.37/1.58     compose (domain $X) (compose (compose a b) b) =
% 1.37/1.58     compose (compose (domain $X) (compose a b)) b
% 1.37/1.58  |- ~(codomain $X = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (codomain $X) (compose (compose a g) b) =
% 1.37/1.58     compose (compose (codomain $X) (compose a g)) b
% 1.37/1.58  |- ~(codomain g = codomain a) \/ ~(domain $X = domain a) \/
% 1.37/1.58     compose (domain $X) (compose (compose a g) b) =
% 1.37/1.58     compose (compose (domain $X) (compose a g)) b
% 1.37/1.58  |- ~(codomain $X = codomain a) \/ ~(codomain b = codomain $X) \/
% 1.37/1.58     compose (compose a b) (compose (codomain $X) g) =
% 1.37/1.58     compose (compose (compose a b) (codomain $X)) g
% 1.37/1.58  |- ~(codomain a = domain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.58     compose (compose a b) (compose (compose a b) g) =
% 1.37/1.58     compose (compose (compose a b) (compose a b)) g
% 1.37/1.58  |- ~(codomain b = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a b) (compose (compose a g) g) =
% 1.37/1.58     compose (compose (compose a b) (compose a g)) g
% 1.37/1.58  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.58     compose (compose a g) (compose (codomain $X) g) =
% 1.37/1.58     compose (compose (compose a g) (codomain $X)) g
% 1.37/1.58  |- ~(codomain b = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.58     compose (compose a g) (compose (compose a b) g) =
% 1.37/1.58     compose (compose (compose a g) (compose a b)) g
% 1.37/1.58  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose (compose a g) g) =
% 1.37/1.58     compose (compose (compose a g) (compose a g)) g
% 1.37/1.58  |- ~(codomain $X = domain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.58     compose (codomain $X) (compose (compose a b) g) =
% 1.37/1.58     compose (compose (codomain $X) (compose a b)) g
% 1.37/1.58  |- ~(codomain b = codomain a) \/ ~(domain $X = domain a) \/
% 1.37/1.58     compose (domain $X) (compose (compose a b) g) =
% 1.37/1.58     compose (compose (domain $X) (compose a b)) g
% 1.37/1.58  |- ~(codomain $X = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (codomain $X) (compose (compose a g) g) =
% 1.37/1.58     compose (compose (codomain $X) (compose a g)) g
% 1.37/1.58  |- ~(codomain g = codomain a) \/ ~(domain $X = domain a) \/
% 1.37/1.58     compose (domain $X) (compose (compose a g) g) =
% 1.37/1.58     compose (compose (domain $X) (compose a g)) g
% 1.37/1.58  |- ~(codomain b = codomain $X) \/ ~(codomain g = domain a) \/
% 1.37/1.58     compose h (compose (compose a b) (codomain $X)) =
% 1.37/1.58     compose (compose h (compose a b)) (codomain $X)
% 1.37/1.58  |- ~(codomain b = domain a) \/ ~(codomain g = codomain b) \/
% 1.37/1.58     compose h (compose (compose a b) (compose a b)) =
% 1.37/1.58     compose (compose h (compose a b)) (compose a b)
% 1.37/1.58  |- ~(codomain b = domain a) \/ ~(codomain g = codomain b) \/
% 1.37/1.58     compose h (compose (compose a b) (compose a g)) =
% 1.37/1.58     compose (compose h (compose a b)) (compose a g)
% 1.37/1.58  |- ~(codomain g = codomain $X) \/ ~(codomain g = domain a) \/
% 1.37/1.58     compose h (compose (compose a g) (codomain $X)) =
% 1.37/1.58     compose (compose h (compose a g)) (codomain $X)
% 1.37/1.58  |- ~(codomain g = domain a) \/
% 1.37/1.58     compose h (compose (compose a g) (compose a b)) =
% 1.37/1.58     compose (compose h (compose a g)) (compose a b)
% 1.37/1.58  |- ~(codomain g = domain a) \/
% 1.37/1.58     compose h (compose (compose a g) (compose a g)) =
% 1.37/1.58     compose (compose h (compose a g)) (compose a g)
% 1.37/1.58  |- ~(codomain $X = domain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.58     compose h (compose (codomain $X) (compose a b)) =
% 1.37/1.58     compose (compose h (codomain $X)) (compose a b)
% 1.37/1.58  |- ~(codomain $X = domain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.58     compose h (compose (codomain $X) (compose a g)) =
% 1.37/1.58     compose (compose h (codomain $X)) (compose a g)
% 1.37/1.58  |- ~(codomain $X = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.58     compose (codomain $X) (compose h (compose a b)) =
% 1.37/1.58     compose (compose (codomain $X) h) (compose a b)
% 1.37/1.58  |- ~(codomain b = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.58     compose (compose a b) (compose h (compose a b)) =
% 1.37/1.58     compose (compose (compose a b) h) (compose a b)
% 1.37/1.58  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose h (compose a b)) =
% 1.37/1.58     compose (compose (compose a g) h) (compose a b)
% 1.37/1.58  |- ~(codomain $X = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.58     compose (codomain $X) (compose h (compose a g)) =
% 1.37/1.58     compose (compose (codomain $X) h) (compose a g)
% 1.37/1.58  |- ~(codomain b = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.58     compose (compose a b) (compose h (compose a g)) =
% 1.37/1.58     compose (compose (compose a b) h) (compose a g)
% 1.37/1.58  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose h (compose a g)) =
% 1.37/1.58     compose (compose (compose a g) h) (compose a g)
% 1.37/1.58  |- ~(codomain b = codomain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.58     compose (compose a b) (compose h (codomain $X)) =
% 1.37/1.58     compose (compose (compose a b) h) (codomain $X)
% 1.37/1.58  |- ~(codomain a = codomain $X) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose h (codomain $X)) =
% 1.37/1.58     compose (compose (compose a g) h) (codomain $X)
% 1.37/1.58  |- ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose h (codomain a)) =
% 1.37/1.58     compose (compose (compose a g) h) (codomain a)
% 1.37/1.58  |- ~(codomain $X = codomain a) \/ ~(codomain b = codomain $X) \/
% 1.37/1.58     compose (compose a b) (compose (codomain $X) h) =
% 1.37/1.58     compose (compose (compose a b) (codomain $X)) h
% 1.37/1.58  |- ~(codomain a = domain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.58     compose (compose a b) (compose (compose a b) h) =
% 1.37/1.58     compose (compose (compose a b) (compose a b)) h
% 1.37/1.58  |- ~(codomain b = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a b) (compose (compose a g) h) =
% 1.37/1.58     compose (compose (compose a b) (compose a g)) h
% 1.37/1.58  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.58     compose (compose a g) (compose (codomain $X) h) =
% 1.37/1.58     compose (compose (compose a g) (codomain $X)) h
% 1.37/1.58  |- ~(codomain b = codomain a) \/ ~(codomain g = domain a) \/
% 1.37/1.58     compose (compose a g) (compose (compose a b) h) =
% 1.37/1.58     compose (compose (compose a g) (compose a b)) h
% 1.37/1.58  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (compose a g) (compose (compose a g) h) =
% 1.37/1.58     compose (compose (compose a g) (compose a g)) h
% 1.37/1.58  |- ~(codomain $X = domain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.58     compose (codomain $X) (compose (compose a b) h) =
% 1.37/1.58     compose (compose (codomain $X) (compose a b)) h
% 1.37/1.58  |- ~(codomain b = codomain a) \/ ~(domain $X = domain a) \/
% 1.37/1.58     compose (domain $X) (compose (compose a b) h) =
% 1.37/1.58     compose (compose (domain $X) (compose a b)) h
% 1.37/1.58  |- ~(codomain $X = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.58     compose (codomain $X) (compose (compose a g) h) =
% 1.37/1.58     compose (compose (codomain $X) (compose a g)) h
% 1.37/1.58  |- ~(codomain g = codomain a) \/ ~(domain $X = domain a) \/
% 1.37/1.58     compose (domain $X) (compose (compose a g) h) =
% 1.37/1.58     compose (compose (domain $X) (compose a g)) h
% 1.37/1.58  |- ~(codomain $_284 = domain a) \/ ~(codomain b = codomain $X) \/
% 1.37/1.58     compose $_284 (compose (compose a b) (codomain $X)) =
% 1.37/1.58     compose (compose $_284 (compose a b)) (codomain $X)
% 1.37/1.58  |- ~(codomain $X = domain a) \/ ~(codomain b = domain $_285) \/
% 1.37/1.58     compose (codomain $X) (compose (compose a b) $_285) =
% 1.37/1.58     compose (compose (codomain $X) (compose a b)) $_285
% 1.37/1.58  |- ~(codomain b = domain $_285) \/ ~(domain $X = domain a) \/
% 1.37/1.58     compose (domain $X) (compose (compose a b) $_285) =
% 1.37/1.58     compose (compose (domain $X) (compose a b)) $_285
% 1.37/1.58  |- ~(codomain b = domain a) \/
% 1.37/1.58     compose b (compose (compose a b) (compose a b)) =
% 1.37/1.58     compose (compose b (compose a b)) (compose a b)
% 1.37/1.58  |- ~(codomain b = domain a) \/
% 1.37/1.58     compose b (compose (compose a b) (compose a g)) =
% 1.37/1.58     compose (compose b (compose a b)) (compose a g)
% 1.37/1.58  |- ~(codomain b = domain a) \/
% 1.37/1.58     compose (codomain b) (compose (compose a b) a) =
% 1.37/1.58     compose (compose (codomain b) (compose a b)) a
% 1.37/1.58  |- ~(codomain b = domain a) \/
% 1.37/1.58     compose (compose a b) (compose (compose a b) a) =
% 1.37/1.58     compose (compose (compose a b) (compose a b)) a
% 1.37/1.58  |- ~(codomain $_286 = domain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.58     compose $_286 (compose (compose a g) (codomain $X)) =
% 1.37/1.58     compose (compose $_286 (compose a g)) (codomain $X)
% 1.37/1.58  |- ~(codomain $X = domain a) \/ ~(codomain g = domain $_287) \/
% 1.37/1.58     compose (codomain $X) (compose (compose a g) $_287) =
% 1.37/1.58     compose (compose (codomain $X) (compose a g)) $_287
% 1.37/1.58  |- ~(codomain g = domain $_287) \/ ~(domain $X = domain a) \/
% 1.37/1.58     compose (domain $X) (compose (compose a g) $_287) =
% 1.37/1.58     compose (compose (domain $X) (compose a g)) $_287
% 1.37/1.58  |- ~(codomain g = domain a) \/
% 1.37/1.58     compose g (compose (compose a g) (compose a b)) =
% 1.37/1.58     compose (compose g (compose a g)) (compose a b)
% 1.37/1.58  |- ~(codomain g = domain a) \/
% 1.37/1.58     compose g (compose (compose a g) (compose a g)) =
% 1.37/1.58     compose (compose g (compose a g)) (compose a g)
% 1.37/1.58  |- ~(codomain g = domain a) \/
% 1.37/1.58     compose (codomain g) (compose (compose a g) a) =
% 1.37/1.58     compose (compose (codomain g) (compose a g)) a
% 1.37/1.58  |- ~(codomain g = domain a) \/
% 1.37/1.58     compose (compose a g) (compose (compose a g) a) =
% 1.37/1.58     compose (compose (compose a g) (compose a g)) a
% 1.37/1.58  |- ~(codomain $X = domain $_289) \/ ~(codomain $_289 = domain a) \/
% 1.37/1.58     compose (codomain $X) (compose $_289 (compose a b)) =
% 1.37/1.58     compose (compose (codomain $X) $_289) (compose a b)
% 1.37/1.58  |- ~(codomain $_289 = domain a) \/ ~(domain $X = domain $_289) \/
% 1.37/1.58     compose (domain $X) (compose $_289 (compose a b)) =
% 1.37/1.58     compose (compose (domain $X) $_289) (compose a b)
% 1.37/1.58  |- ~(codomain $X = domain a) \/ ~(codomain $_288 = codomain $X) \/
% 1.37/1.58     compose $_288 (compose (codomain $X) (compose a b)) =
% 1.37/1.58     compose (compose $_288 (codomain $X)) (compose a b)
% 1.37/1.58  |- ~(codomain $_288 = codomain b) \/ ~(codomain b = domain a) \/
% 1.37/1.58     compose $_288 (compose (compose a b) (compose a b)) =
% 1.37/1.58     compose (compose $_288 (compose a b)) (compose a b)
% 1.37/1.59  |- ~(codomain $_288 = codomain g) \/ ~(codomain g = domain a) \/
% 1.37/1.59     compose $_288 (compose (compose a g) (compose a b)) =
% 1.37/1.59     compose (compose $_288 (compose a g)) (compose a b)
% 1.37/1.59  |- ~(codomain a = domain a) \/
% 1.37/1.59     compose (codomain a) (compose a (compose a b)) =
% 1.37/1.59     compose (compose (codomain a) a) (compose a b)
% 1.37/1.59  |- ~(codomain $X = domain $_291) \/ ~(codomain $_291 = domain a) \/
% 1.37/1.59     compose (codomain $X) (compose $_291 (compose a g)) =
% 1.37/1.59     compose (compose (codomain $X) $_291) (compose a g)
% 1.37/1.59  |- ~(codomain $_291 = domain a) \/ ~(domain $X = domain $_291) \/
% 1.37/1.59     compose (domain $X) (compose $_291 (compose a g)) =
% 1.37/1.59     compose (compose (domain $X) $_291) (compose a g)
% 1.37/1.59  |- ~(codomain $X = domain a) \/ ~(codomain $_290 = codomain $X) \/
% 1.37/1.59     compose $_290 (compose (codomain $X) (compose a g)) =
% 1.37/1.59     compose (compose $_290 (codomain $X)) (compose a g)
% 1.37/1.59  |- ~(codomain $_290 = codomain b) \/ ~(codomain b = domain a) \/
% 1.37/1.59     compose $_290 (compose (compose a b) (compose a g)) =
% 1.37/1.59     compose (compose $_290 (compose a b)) (compose a g)
% 1.37/1.59  |- ~(codomain $_290 = codomain g) \/ ~(codomain g = domain a) \/
% 1.37/1.59     compose $_290 (compose (compose a g) (compose a g)) =
% 1.37/1.59     compose (compose $_290 (compose a g)) (compose a g)
% 1.37/1.59  |- ~(codomain a = domain a) \/
% 1.37/1.59     compose (codomain a) (compose a (compose a g)) =
% 1.37/1.59     compose (compose (codomain a) a) (compose a g)
% 1.37/1.59  |- ~(codomain $X = domain $_293) \/ ~(codomain b = codomain $X) \/
% 1.37/1.59     compose (compose a b) (compose (codomain $X) $_293) =
% 1.37/1.59     compose (compose (compose a b) (codomain $X)) $_293
% 1.37/1.59  |- ~(codomain b = domain $_293) \/ ~(codomain b = domain a) \/
% 1.37/1.59     compose (compose a b) (compose (compose a b) $_293) =
% 1.37/1.59     compose (compose (compose a b) (compose a b)) $_293
% 1.37/1.59  |- ~(codomain b = domain a) \/ ~(codomain g = domain $_293) \/
% 1.37/1.59     compose (compose a b) (compose (compose a g) $_293) =
% 1.37/1.59     compose (compose (compose a b) (compose a g)) $_293
% 1.37/1.59  |- ~(codomain $_292 = codomain $X) \/ ~(codomain b = domain $_292) \/
% 1.37/1.59     compose (compose a b) (compose $_292 (codomain $X)) =
% 1.37/1.59     compose (compose (compose a b) $_292) (codomain $X)
% 1.37/1.59  |- ~(codomain $_292 = domain a) \/ ~(codomain b = domain $_292) \/
% 1.37/1.59     compose (compose a b) (compose $_292 (compose a b)) =
% 1.37/1.59     compose (compose (compose a b) $_292) (compose a b)
% 1.37/1.59  |- ~(codomain $_292 = domain a) \/ ~(codomain b = domain $_292) \/
% 1.37/1.59     compose (compose a b) (compose $_292 (compose a g)) =
% 1.37/1.59     compose (compose (compose a b) $_292) (compose a g)
% 1.37/1.59  |- ~(codomain $_292 = domain $_2) \/ ~(codomain b = domain $_292) \/
% 1.37/1.59     compose (compose a b) (compose $_292 (domain $_2)) =
% 1.37/1.59     compose (compose (compose a b) $_292) (domain $_2)
% 1.37/1.59  |- ~(codomain $X = domain $_295) \/ ~(codomain g = codomain $X) \/
% 1.37/1.59     compose (compose a g) (compose (codomain $X) $_295) =
% 1.37/1.59     compose (compose (compose a g) (codomain $X)) $_295
% 1.37/1.59  |- ~(codomain b = domain $_295) \/ ~(codomain g = domain a) \/
% 1.37/1.59     compose (compose a g) (compose (compose a b) $_295) =
% 1.37/1.59     compose (compose (compose a g) (compose a b)) $_295
% 1.37/1.59  |- ~(codomain g = domain $_295) \/ ~(codomain g = domain a) \/
% 1.37/1.59     compose (compose a g) (compose (compose a g) $_295) =
% 1.37/1.59     compose (compose (compose a g) (compose a g)) $_295
% 1.37/1.59  |- ~(codomain $_294 = codomain $X) \/ ~(codomain g = domain $_294) \/
% 1.37/1.59     compose (compose a g) (compose $_294 (codomain $X)) =
% 1.37/1.59     compose (compose (compose a g) $_294) (codomain $X)
% 1.37/1.59  |- ~(codomain $_294 = domain a) \/ ~(codomain g = domain $_294) \/
% 1.37/1.59     compose (compose a g) (compose $_294 (compose a b)) =
% 1.37/1.59     compose (compose (compose a g) $_294) (compose a b)
% 1.37/1.59  |- ~(codomain $_294 = domain a) \/ ~(codomain g = domain $_294) \/
% 1.37/1.59     compose (compose a g) (compose $_294 (compose a g)) =
% 1.37/1.59     compose (compose (compose a g) $_294) (compose a g)
% 1.37/1.59  |- ~(codomain $_294 = domain $_2) \/ ~(codomain g = domain $_294) \/
% 1.37/1.59     compose (compose a g) (compose $_294 (domain $_2)) =
% 1.37/1.59     compose (compose (compose a g) $_294) (domain $_2)
% 1.37/1.59  |- ~(codomain b = codomain $X) \/ ~(codomain b = domain a) \/
% 1.37/1.59     compose (compose a b) (compose (compose a b) (codomain $X)) =
% 1.37/1.59     compose (compose (compose a b) (compose a b)) (codomain $X)
% 1.37/1.59  |- ~(codomain b = domain a) \/
% 1.37/1.59     compose (compose a b) (compose (compose a b) (compose a g)) =
% 1.37/1.59     compose (compose (compose a b) (compose a b)) (compose a g)
% 1.37/1.59  |- ~(codomain b = domain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.59     compose (compose a b) (compose (compose a g) (codomain $X)) =
% 1.37/1.59     compose (compose (compose a b) (compose a g)) (codomain $X)
% 1.37/1.59  |- ~(codomain b = domain a) \/ ~(codomain g = codomain b) \/
% 1.37/1.59     compose (compose a b) (compose (compose a g) (compose a b)) =
% 1.37/1.59     compose (compose (compose a b) (compose a g)) (compose a b)
% 1.37/1.59  |- ~(codomain b = domain a) \/ ~(codomain g = codomain b) \/
% 1.37/1.59     compose (compose a b) (compose (compose a g) (compose a g)) =
% 1.37/1.59     compose (compose (compose a b) (compose a g)) (compose a g)
% 1.37/1.59  |- ~(codomain $X = domain a) \/ ~(codomain b = codomain $X) \/
% 1.37/1.59     compose (compose a b) (compose (codomain $X) (compose a b)) =
% 1.37/1.59     compose (compose (compose a b) (codomain $X)) (compose a b)
% 1.37/1.59  |- ~(codomain $X = domain a) \/ ~(codomain b = codomain $X) \/
% 1.37/1.59     compose (compose a b) (compose (codomain $X) (compose a g)) =
% 1.37/1.59     compose (compose (compose a b) (codomain $X)) (compose a g)
% 1.37/1.59  |- ~(codomain b = codomain $X) \/ ~(codomain g = domain a) \/
% 1.37/1.59     compose (compose a g) (compose (compose a b) (codomain $X)) =
% 1.37/1.59     compose (compose (compose a g) (compose a b)) (codomain $X)
% 1.37/1.59  |- ~(codomain b = domain a) \/ ~(codomain g = codomain b) \/
% 1.37/1.59     compose (compose a g) (compose (compose a b) (compose a b)) =
% 1.37/1.59     compose (compose (compose a g) (compose a b)) (compose a b)
% 1.37/1.59  |- ~(codomain b = domain a) \/ ~(codomain g = codomain b) \/
% 1.37/1.59     compose (compose a g) (compose (compose a b) (compose a g)) =
% 1.37/1.59     compose (compose (compose a g) (compose a b)) (compose a g)
% 1.37/1.59  |- ~(codomain g = codomain $X) \/ ~(codomain g = domain a) \/
% 1.37/1.59     compose (compose a g) (compose (compose a g) (codomain $X)) =
% 1.37/1.59     compose (compose (compose a g) (compose a g)) (codomain $X)
% 1.37/1.59  |- ~(codomain g = domain a) \/
% 1.37/1.59     compose (compose a g) (compose (compose a g) (compose a b)) =
% 1.37/1.59     compose (compose (compose a g) (compose a g)) (compose a b)
% 1.37/1.59  |- ~(codomain $X = domain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.59     compose (compose a g) (compose (codomain $X) (compose a b)) =
% 1.37/1.59     compose (compose (compose a g) (codomain $X)) (compose a b)
% 1.37/1.59  |- ~(codomain $X = domain a) \/ ~(codomain g = codomain $X) \/
% 1.37/1.59     compose (compose a g) (compose (codomain $X) (compose a g)) =
% 1.37/1.59     compose (compose (compose a g) (codomain $X)) (compose a g)
% 1.37/1.59  |- ~(codomain $X = codomain b) \/ ~(codomain b = domain a) \/
% 1.37/1.59     compose (codomain $X) (compose (compose a b) (compose a b)) =
% 1.37/1.59     compose (compose (codomain $X) (compose a b)) (compose a b)
% 1.37/1.59  |- ~(codomain $X = codomain g) \/ ~(codomain g = domain a) \/
% 1.37/1.59     compose (codomain $X) (compose (compose a g) (compose a b)) =
% 1.37/1.59     compose (compose (codomain $X) (compose a g)) (compose a b)
% 1.37/1.59  |- ~(codomain g = domain a) \/
% 1.37/1.59     compose (codomain g) (compose (compose a g) (compose a b)) =
% 1.37/1.59     compose (compose (codomain g) (compose a g)) (compose a b)
% 1.37/1.59  |- ~(codomain $X = codomain b) \/ ~(codomain b = domain a) \/
% 1.37/1.59     compose (codomain $X) (compose (compose a b) (compose a g)) =
% 1.37/1.59     compose (compose (codomain $X) (compose a b)) (compose a g)
% 1.37/1.59  |- ~(codomain b = domain a) \/
% 1.37/1.59     compose (codomain b) (compose (compose a b) (compose a g)) =
% 1.37/1.59     compose (compose (codomain b) (compose a b)) (compose a g)
% 1.37/1.59  |- ~(codomain $X = codomain g) \/ ~(codomain g = domain a) \/
% 1.37/1.59     compose (codomain $X) (compose (compose a g) (compose a g)) =
% 1.37/1.59     compose (compose (codomain $X) (compose a g)) (compose a g)
% 1.37/1.59  |- ~(codomain a = domain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose b (compose a b)) = compose b (compose a b)
% 1.37/1.59  |- ~(codomain a = domain a) \/ ~(codomain b = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose b (compose a g)) = compose b (compose a g)
% 1.37/1.59  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose g (compose a b)) = compose g (compose a b)
% 1.37/1.59  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose g (compose a g)) = compose g (compose a g)
% 1.37/1.59  |- ~(codomain b = codomain g) \/ ~(codomain b = domain a) \/
% 1.37/1.59     compose (codomain b) (compose (compose a g) (compose a g)) =
% 1.37/1.59     compose (compose (codomain b) (compose a g)) (compose a g)
% 1.37/1.59  |- ~(codomain b = codomain g) \/ ~(codomain b = domain a) \/
% 1.37/1.59     compose h (compose a b) = compose (compose h (compose a b)) (codomain b)
% 1.37/1.59  |- ~(codomain b = domain a) \/ ~(codomain g = codomain b) \/
% 1.37/1.59     compose h (compose (compose a g) (codomain b)) =
% 1.37/1.59     compose (compose h (compose a g)) (codomain b)
% 1.37/1.59  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose h (compose a b)) = compose h (compose a b)
% 1.37/1.59  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose h (compose a g)) = compose h (compose a g)
% 1.37/1.59  |- ~(codomain b = domain a) \/ ~(codomain g = codomain b) \/
% 1.37/1.59     compose (compose a g) (compose (compose a g) (codomain b)) =
% 1.37/1.59     compose (compose (compose a g) (compose a g)) (codomain b)
% 1.37/1.59  |- ~(codomain b = codomain g) \/ ~(codomain b = domain a) \/
% 1.37/1.59     compose (codomain b) (compose (compose a g) (compose a b)) =
% 1.37/1.59     compose (compose (codomain b) (compose a g)) (compose a b)
% 1.37/1.59  |- ~(codomain $X = codomain $_356) \/ ~(codomain $_356 = domain $_358) \/
% 1.37/1.59     compose (codomain $X) (compose (codomain $_356) $_358) =
% 1.37/1.59     compose (compose (codomain $X) (codomain $_356)) $_358
% 1.37/1.59  |- ~(codomain $_356 = domain $X) \/
% 1.37/1.59     compose (domain $X) (compose (codomain $_356) $X) =
% 1.37/1.59     compose (compose (domain $X) (codomain $_356)) $X
% 1.37/1.59  |- ~(codomain $_356 = codomain $_357) \/
% 1.37/1.59     compose $_357 (compose (codomain $_356) (codomain $_357)) =
% 1.37/1.59     compose (compose $_357 (codomain $_356)) (codomain $_357)
% 1.37/1.59  |- ~(domain $X = domain $_359) \/
% 1.37/1.59     compose (domain $_359) (compose (domain $X) $_359) =
% 1.37/1.59     compose (compose (domain $_359) (domain $X)) $_359
% 1.37/1.59  |- ~(codomain $_360 = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose (codomain $_360) b) =
% 1.37/1.59     compose (compose (codomain a) (codomain $_360)) b
% 1.37/1.59  |- ~(codomain $_360 = domain a) \/
% 1.37/1.59     compose (domain a) (compose (codomain $_360) (compose a b)) =
% 1.37/1.59     compose (compose (domain a) (codomain $_360)) (compose a b)
% 1.37/1.59  |- ~(codomain $_360 = domain a) \/
% 1.37/1.59     compose (domain a) (compose (codomain $_360) (compose a g)) =
% 1.37/1.59     compose (compose (domain a) (codomain $_360)) (compose a g)
% 1.37/1.59  |- ~(codomain $_360 = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose (codomain $_360) g) =
% 1.37/1.59     compose (compose (codomain a) (codomain $_360)) g
% 1.37/1.59  |- ~(codomain $_360 = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose (codomain $_360) h) =
% 1.37/1.59     compose (compose (codomain a) (codomain $_360)) h
% 1.37/1.59  |- ~(domain $X = domain a) \/
% 1.37/1.59     compose (domain a) (compose (domain $X) (compose a b)) =
% 1.37/1.59     compose (compose (domain a) (domain $X)) (compose a b)
% 1.37/1.59  |- ~(domain $X = domain a) \/
% 1.37/1.59     compose (domain a) (compose (domain $X) (compose a g)) =
% 1.37/1.59     compose (compose (domain a) (domain $X)) (compose a g)
% 1.37/1.59  |- ~(domain $X = codomain $_369) \/
% 1.37/1.59     compose $_369 (compose (domain $X) (codomain $_369)) =
% 1.37/1.59     compose (compose $_369 (domain $X)) (codomain $_369)
% 1.37/1.59  |- ~(codomain $_368 = codomain $X) \/
% 1.37/1.59     compose (codomain $X) (compose (codomain $_368) (codomain $X)) =
% 1.37/1.59     compose (compose (codomain $X) (codomain $_368)) (codomain $X)
% 1.37/1.59  |- ~(codomain $_368 = codomain b) \/
% 1.37/1.59     compose (compose a b) (compose (codomain $_368) (codomain b)) =
% 1.37/1.59     compose (compose (compose a b) (codomain $_368)) (codomain b)
% 1.37/1.59  |- ~(codomain $_368 = codomain g) \/
% 1.37/1.59     compose (compose a g) (compose (codomain $_368) (codomain g)) =
% 1.37/1.59     compose (compose (compose a g) (codomain $_368)) (codomain g)
% 1.37/1.59  |- ~(codomain $_368 = domain $X) \/
% 1.37/1.59     compose (domain $X) (compose (codomain $_368) (domain $X)) =
% 1.37/1.59     compose (compose (domain $X) (codomain $_368)) (domain $X)
% 1.37/1.59  |- ~(codomain $_368 = codomain g) \/
% 1.37/1.59     compose h (compose (codomain $_368) (codomain g)) =
% 1.37/1.59     compose (compose h (codomain $_368)) (codomain g)
% 1.37/1.59  |- ~(domain $X = domain $_379) \/
% 1.37/1.59     compose (domain $_379) (compose (domain $X) (domain $_379)) =
% 1.37/1.59     compose (compose (domain $_379) (domain $X)) (domain $_379)
% 1.37/1.59  |- ~(domain $_381 = codomain $X) \/
% 1.37/1.59     compose (codomain $X) (compose (domain $_381) (codomain $X)) =
% 1.37/1.59     compose (compose (codomain $X) (domain $_381)) (codomain $X)
% 1.37/1.59  |- ~(codomain $_386 = domain $_385) \/ ~(domain $_385 = codomain $X) \/
% 1.37/1.59     compose $_386 (compose (domain $_385) (codomain $X)) =
% 1.37/1.59     compose (compose $_386 (domain $_385)) (codomain $X)
% 1.37/1.59  |- ~(codomain $_386 = domain $_385) \/ ~(domain $_385 = domain a) \/
% 1.37/1.59     compose $_386 (compose (domain $_385) (compose a b)) =
% 1.37/1.59     compose (compose $_386 (domain $_385)) (compose a b)
% 1.37/1.59  |- ~(codomain $_386 = domain $_385) \/ ~(domain $_385 = domain a) \/
% 1.37/1.59     compose $_386 (compose (domain $_385) (compose a g)) =
% 1.37/1.59     compose (compose $_386 (domain $_385)) (compose a g)
% 1.37/1.59  |- ~(codomain $_386 = domain $_385) \/ ~(domain $_385 = domain $_2) \/
% 1.37/1.59     compose $_386 (compose (domain $_385) (domain $_2)) =
% 1.37/1.59     compose (compose $_386 (domain $_385)) (domain $_2)
% 1.37/1.59  |- ~(codomain $X = domain $_385) \/ ~(domain $_385 = domain $_387) \/
% 1.37/1.59     compose (codomain $X) (compose (domain $_385) $_387) =
% 1.37/1.59     compose (compose (codomain $X) (domain $_385)) $_387
% 1.37/1.59  |- ~(domain $X = domain $_385) \/ ~(domain $_385 = domain $_387) \/
% 1.37/1.59     compose (domain $X) (compose (domain $_385) $_387) =
% 1.37/1.59     compose (compose (domain $X) (domain $_385)) $_387
% 1.37/1.59  |- ~(codomain $X = codomain $_388) \/ ~(codomain $_389 = codomain $X) \/
% 1.37/1.59     compose $_389 (compose (codomain $X) (codomain $_388)) =
% 1.37/1.59     compose (compose $_389 (codomain $X)) (codomain $_388)
% 1.37/1.59  |- ~(codomain $X = domain $_390) \/ ~(codomain $_390 = codomain $_388) \/
% 1.37/1.59     compose (codomain $X) (compose $_390 (codomain $_388)) =
% 1.37/1.59     compose (compose (codomain $X) $_390) (codomain $_388)
% 1.37/1.59  |- ~(codomain $X = domain $_391) \/ ~(codomain $_392 = codomain $X) \/
% 1.37/1.59     compose $_392 (compose (codomain $X) (domain $_391)) =
% 1.37/1.59     compose (compose $_392 (codomain $X)) (domain $_391)
% 1.37/1.59  |- ~(codomain $X = domain $_393) \/ ~(codomain $_393 = domain $_391) \/
% 1.37/1.59     compose (codomain $X) (compose $_393 (domain $_391)) =
% 1.37/1.59     compose (compose (codomain $X) $_393) (domain $_391)
% 1.37/1.59  |- ~(codomain $_393 = domain $_391) \/ ~(domain $X = domain $_393) \/
% 1.37/1.59     compose (domain $X) (compose $_393 (domain $_391)) =
% 1.37/1.59     compose (compose (domain $X) $_393) (domain $_391)
% 1.37/1.59  |- ~(codomain $_393 = domain $_391) \/ ~(codomain g = domain $_393) \/
% 1.37/1.59     compose h (compose $_393 (domain $_391)) =
% 1.37/1.59     compose (compose h $_393) (domain $_391)
% 1.37/1.59  |- ~(codomain a = domain a) \/ ~(codomain g = codomain a) \/
% 1.37/1.59     compose h (compose (compose a g) (codomain a)) =
% 1.37/1.59     compose (compose h (compose a g)) (codomain a)
% 1.37/1.59  |- ~(codomain $X = domain $_403) \/ ~(domain $_401 = codomain $X) \/
% 1.37/1.59     compose (domain $_401) (compose (codomain $X) $_403) =
% 1.37/1.59     compose (compose (domain $_401) (codomain $X)) $_403
% 1.37/1.59  |- ~(codomain $_402 = codomain a) \/ ~(domain $_401 = domain $_402) \/
% 1.37/1.59     compose (domain $_401) (compose $_402 b) =
% 1.37/1.59     compose (compose (domain $_401) $_402) b
% 1.37/1.59  |- ~(codomain $_402 = codomain $X) \/ ~(domain $_401 = domain $_402) \/
% 1.37/1.59     compose (domain $_401) (compose $_402 (codomain $X)) =
% 1.37/1.59     compose (compose (domain $_401) $_402) (codomain $X)
% 1.37/1.59  |- ~(codomain $_402 = codomain a) \/ ~(domain $_401 = domain $_402) \/
% 1.37/1.59     compose (domain $_401) (compose $_402 g) =
% 1.37/1.59     compose (compose (domain $_401) $_402) g
% 1.37/1.59  |- ~(codomain $_402 = codomain a) \/ ~(domain $_401 = domain $_402) \/
% 1.37/1.59     compose (domain $_401) (compose $_402 h) =
% 1.37/1.59     compose (compose (domain $_401) $_402) h
% 1.37/1.59  |- ~(codomain $X = codomain a) \/ ~(codomain b = codomain $_404) \/
% 1.37/1.59     compose (codomain $X) (compose b (codomain $_404)) =
% 1.37/1.59     compose (compose (codomain $X) b) (codomain $_404)
% 1.37/1.59  |- ~(codomain a = domain $_407) \/ ~(codomain b = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose b $_407) = compose b $_407
% 1.37/1.59  |- ~(codomain a = codomain $X) \/ ~(codomain b = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose b (codomain $X)) = compose b (codomain $X)
% 1.37/1.59  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain $_410) \/
% 1.37/1.59     compose (codomain $X) (compose g (codomain $_410)) =
% 1.37/1.59     compose (compose (codomain $X) g) (codomain $_410)
% 1.37/1.59  |- ~(codomain a = domain $_413) \/ ~(codomain g = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose g $_413) = compose g $_413
% 1.37/1.59  |- ~(codomain a = codomain $X) \/ ~(codomain g = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose g (codomain $X)) = compose g (codomain $X)
% 1.37/1.59  |- ~(codomain b = codomain g) \/ ~(codomain b = domain a) \/
% 1.37/1.59     compose (compose a g) (compose a b) =
% 1.37/1.59     compose (compose (compose a g) (compose a b)) (codomain b)
% 1.37/1.59  |- ~(codomain $X = codomain a) \/ ~(codomain $_427 = codomain $X) \/
% 1.37/1.59     compose (codomain $_427) (compose (codomain $X) b) =
% 1.37/1.59     compose (compose (codomain $_427) (codomain $X)) b
% 1.37/1.59  |- ~(codomain $X = codomain a) \/ ~(codomain $_431 = codomain $X) \/
% 1.37/1.59     compose (codomain $_431) (compose (codomain $X) g) =
% 1.37/1.59     compose (compose (codomain $_431) (codomain $X)) g
% 1.37/1.59  |- ~(codomain $X = codomain $_437) \/ ~(codomain g = codomain $X) \/
% 1.37/1.59     compose h (compose (codomain $X) (codomain $_437)) =
% 1.37/1.59     compose (compose h (codomain $X)) (codomain $_437)
% 1.37/1.59  |- ~(codomain $X = codomain a) \/ ~(codomain g = codomain $_439) \/
% 1.37/1.59     compose (codomain $X) (compose h (codomain $_439)) =
% 1.37/1.59     compose (compose (codomain $X) h) (codomain $_439)
% 1.37/1.59  |- ~(codomain a = domain $_442) \/ ~(codomain g = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose h $_442) = compose h $_442
% 1.37/1.59  |- ~(codomain a = codomain $X) \/ ~(codomain g = codomain a) \/
% 1.37/1.59     compose (codomain a) (compose h (codomain $X)) = compose h (codomain $X)
% 1.37/1.59  |- ~(codomain $X = codomain a) \/ ~(codomain $_445 = codomain $X) \/
% 1.37/1.59     compose (codomain $_445) (compose (codomain $X) h) =
% 1.37/1.59     compose (compose (codomain $_445) (codomain $X)) h
% 1.37/1.59  |- ~(codomain $_461 = codomain a) \/ ~(domain $X = codomain $_461) \/
% 1.37/1.59     compose (domain $X) (compose (codomain $_461) b) =
% 1.37/1.59     compose (compose (domain $X) (codomain $_461)) b
% 1.37/1.59  |- ~(codomain $_463 = codomain a) \/ ~(domain $X = codomain $_463) \/
% 1.37/1.59     compose (domain $X) (compose (codomain $_463) g) =
% 1.37/1.59     compose (compose (domain $X) (codomain $_463)) g
% 1.37/1.59  |- ~(codomain $_465 = domain $X) \/ ~(codomain g = codomain $_465) \/
% 1.37/1.59     compose h (compose (codomain $_465) (domain $X)) =
% 1.37/1.59     compose (compose h (codomain $_465)) (domain $X)
% 1.37/1.59  |- ~(codomain $_475 = codomain a) \/ ~(domain $X = codomain $_475) \/
% 1.37/1.59     compose (domain $X) (compose (codomain $_475) h) =
% 1.37/1.59     compose (compose (domain $X) (codomain $_475)) h
% 1.37/1.60  |- ~(codomain $_479 = codomain $X) \/ ~(codomain b = codomain $_479) \/
% 1.37/1.60     compose (compose a b) (compose (codomain $_479) (codomain $X)) =
% 1.37/1.60     compose (compose (compose a b) (codomain $_479)) (codomain $X)
% 1.37/1.60  |- ~(codomain $X = domain $_483) \/ ~(codomain b = codomain $X) \/
% 1.37/1.60     compose (compose a b) (compose (codomain $X) (domain $_483)) =
% 1.37/1.60     compose (compose (compose a b) (codomain $X)) (domain $_483)
% 1.37/1.60  |- ~(codomain $_485 = codomain $X) \/ ~(codomain g = codomain $_485) \/
% 1.37/1.60     compose (compose a g) (compose (codomain $_485) (codomain $X)) =
% 1.37/1.60     compose (compose (compose a g) (codomain $_485)) (codomain $X)
% 1.37/1.60  |- ~(codomain $X = domain $_489) \/ ~(codomain g = codomain $X) \/
% 1.37/1.60     compose (compose a g) (compose (codomain $X) (domain $_489)) =
% 1.37/1.60     compose (compose (compose a g) (codomain $X)) (domain $_489)
% 1.37/1.60  |- ~(codomain $X = domain a) \/ ~(domain $_493 = codomain $X) \/
% 1.37/1.60     compose (domain $_493) (compose (codomain $X) (compose a b)) =
% 1.37/1.60     compose (compose (domain $_493) (codomain $X)) (compose a b)
% 1.37/1.60  |- ~(domain $_2 = domain a) \/ ~(domain $_493 = domain $_2) \/
% 1.37/1.60     compose (domain $_493) (compose (domain $_2) (compose a b)) =
% 1.37/1.60     compose (compose (domain $_493) (domain $_2)) (compose a b)
% 1.37/1.60  |- ~(codomain $X = codomain $_495) \/ ~(codomain $_495 = domain a) \/
% 1.37/1.60     compose (codomain $X) (compose (codomain $_495) (compose a b)) =
% 1.37/1.60     compose (compose (codomain $X) (codomain $_495)) (compose a b)
% 1.37/1.60  |- ~(codomain $X = domain a) \/ ~(domain $_499 = codomain $X) \/
% 1.37/1.60     compose (domain $_499) (compose (codomain $X) (compose a g)) =
% 1.37/1.60     compose (compose (domain $_499) (codomain $X)) (compose a g)
% 1.37/1.60  |- ~(domain $_2 = domain a) \/ ~(domain $_499 = domain $_2) \/
% 1.37/1.60     compose (domain $_499) (compose (domain $_2) (compose a g)) =
% 1.37/1.60     compose (compose (domain $_499) (domain $_2)) (compose a g)
% 1.37/1.60  |- ~(codomain $X = codomain $_501) \/ ~(codomain $_501 = domain a) \/
% 1.37/1.60     compose (codomain $X) (compose (codomain $_501) (compose a g)) =
% 1.37/1.60     compose (compose (codomain $X) (codomain $_501)) (compose a g)
% 1.37/1.60  |- ~(codomain $X = domain a) \/ ~(codomain b = codomain $_503) \/
% 1.37/1.60     compose (codomain $X) (compose (compose a b) (codomain $_503)) =
% 1.37/1.60     compose (compose (codomain $X) (compose a b)) (codomain $_503)
% 1.37/1.60  |- ~(codomain b = codomain $X) \/ ~(domain $_507 = domain a) \/
% 1.37/1.60     compose (domain $_507) (compose (compose a b) (codomain $X)) =
% 1.37/1.60     compose (compose (domain $_507) (compose a b)) (codomain $X)
% 1.37/1.60  |- ~(codomain $X = domain a) \/ ~(codomain g = codomain $_509) \/
% 1.37/1.60     compose (codomain $X) (compose (compose a g) (codomain $_509)) =
% 1.37/1.60     compose (compose (codomain $X) (compose a g)) (codomain $_509)
% 1.37/1.60  |- ~(codomain g = codomain $X) \/ ~(domain $_513 = domain a) \/
% 1.37/1.60     compose (domain $_513) (compose (compose a g) (codomain $X)) =
% 1.37/1.60     compose (compose (domain $_513) (compose a g)) (codomain $X)
% 1.37/1.60  |- ~(codomain $X = domain $_534) \/ ~(domain $_534 = domain a) \/
% 1.37/1.60     compose (codomain $X) (compose (domain $_534) (compose a b)) =
% 1.37/1.60     compose (compose (codomain $X) (domain $_534)) (compose a b)
% 1.37/1.60  |- ~(codomain $X = domain $_541) \/ ~(domain $_541 = domain a) \/
% 1.37/1.60     compose (codomain $X) (compose (domain $_541) (compose a g)) =
% 1.37/1.60     compose (compose (codomain $X) (domain $_541)) (compose a g)
% 1.37/1.60  |- ~(codomain $X = domain $_557) \/ ~(domain $_557 = domain $_556) \/
% 1.37/1.60     compose (codomain $X) (compose (domain $_557) (domain $_556)) =
% 1.37/1.60     compose (compose (codomain $X) (domain $_557)) (domain $_556)
% 1.37/1.60  |- ~(domain $X = domain $_557) \/ ~(domain $_557 = domain $_556) \/
% 1.37/1.60     compose (domain $X) (compose (domain $_557) (domain $_556)) =
% 1.37/1.60     compose (compose (domain $X) (domain $_557)) (domain $_556)
% 1.37/1.60  |- ~(domain $_564 = domain $_565) \/ ~(domain $_565 = codomain $X) \/
% 1.37/1.60     compose (domain $_564) (compose (domain $_565) (codomain $X)) =
% 1.37/1.60     compose (compose (domain $_564) (domain $_565)) (codomain $X)
% 1.37/1.60  |- ~(codomain $X = codomain $_571) \/ ~(codomain $_571 = domain $_572) \/
% 1.37/1.60     compose (codomain $X) (compose (codomain $_571) (domain $_572)) =
% 1.37/1.60     compose (compose (codomain $X) (codomain $_571)) (domain $_572)
% 1.37/1.60  |- ~(codomain $X = domain $_584) \/ ~(domain $_583 = codomain $X) \/
% 1.37/1.60     compose (domain $_583) (compose (codomain $X) (domain $_584)) =
% 1.37/1.60     compose (compose (domain $_583) (codomain $X)) (domain $_584)
% 1.37/1.60  |- ~(codomain $X = codomain $_604) \/ ~(codomain $_604 = codomain $_605) \/
% 1.37/1.60     compose (codomain $X) (compose (codomain $_604) (codomain $_605)) =
% 1.37/1.60     compose (compose (codomain $X) (codomain $_604)) (codomain $_605)
% 1.37/1.60  |- ~(codomain $_604 = codomain $_605) \/ ~(domain $X = codomain $_604) \/
% 1.37/1.60     compose (domain $X) (compose (codomain $_604) (codomain $_605)) =
% 1.37/1.60     compose (compose (domain $X) (codomain $_604)) (codomain $_605)
% 1.37/1.60  |- ~(codomain $_607 = domain $X) \/ ~(domain $X = codomain $_608) \/
% 1.37/1.60     compose (codomain $_607) (compose (domain $X) (codomain $_608)) =
% 1.37/1.60     compose (compose (codomain $_607) (domain $X)) (codomain $_608)
% 1.37/1.60  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.37/1.60  
%------------------------------------------------------------------------------