%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : HAL002+1 : TPTP v9.0.0. Released v2.6.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:08:44 AM UTC 2025
% Result : Theorem 1.02s 1.22s
% Output : Proof 1.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.11 % Problem : HAL002+1 : TPTP v9.0.0. Released v2.6.0.
% 0.09/0.11 % Command : run_E %s %d THM
% 0.10/0.30 % Computer : n002.cluster.edu
% 0.10/0.30 % Model : x86_64 x86_64
% 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.30 % Memory : 8042.1875MB
% 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30 % CPULimit : 300
% 0.10/0.30 % WCLimit : 300
% 0.10/0.30 % DateTime : Thu Jun 19 17:11:46 EDT 2025
% 0.10/0.31 % CPUTime :
% 1.02/1.22 % SZS status Theorem
% 1.02/1.22 % SZS output start Proof
% 1.02/1.22 tff(tptp_fun_El2_0_type, type, (
% 1.02/1.22 tptp_fun_El2_0: ( $i * $i ) > $i)).
% 1.02/1.22 tff(x_type, type, (
% 1.02/1.22 x: $i)).
% 1.02/1.22 tff(any1_type, type, (
% 1.02/1.22 any1: $i)).
% 1.02/1.22 tff(tptp_fun_El1_1_type, type, (
% 1.02/1.22 tptp_fun_El1_1: ( $i * $i ) > $i)).
% 1.02/1.22 tff(subtract_type, type, (
% 1.02/1.22 subtract: ( $i * $i * $i ) > $i)).
% 1.02/1.22 tff(element_type, type, (
% 1.02/1.22 element: ( $i * $i ) > $o)).
% 1.02/1.22 tff(apply_type, type, (
% 1.02/1.22 apply: ( $i * $i ) > $i)).
% 1.02/1.22 tff(injection_type, type, (
% 1.02/1.22 injection: $i > $o)).
% 1.02/1.22 tff(injection_2_type, type, (
% 1.02/1.22 injection_2: $i > $o)).
% 1.02/1.22 tff(zero_type, type, (
% 1.02/1.22 zero: $i > $i)).
% 1.02/1.22 tff(tptp_fun_El_8_type, type, (
% 1.02/1.22 tptp_fun_El_8: ( $i * $i * $i ) > $i)).
% 1.02/1.22 tff(any2_type, type, (
% 1.02/1.22 any2: $i)).
% 1.02/1.22 tff(morphism_type, type, (
% 1.02/1.22 morphism: ( $i * $i * $i ) > $o)).
% 1.02/1.22 tff(1,plain,
% 1.02/1.22 (morphism(x, any1, any2) <=> morphism(x, any1, any2)),
% 1.02/1.22 inference(rewrite,[status(thm)],[])).
% 1.02/1.22 tff(2,axiom,(morphism(x, any1, any2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','x_morphism')).
% 1.02/1.22 tff(3,plain,
% 1.02/1.22 (morphism(x, any1, any2)),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[2, 1])).
% 1.02/1.22 tff(4,plain,
% 1.02/1.22 (^[Morphism: $i, Dom: $i, Cod: $i] : rewrite(((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod)))))) <=> ((~morphism(Morphism, Dom, Cod)) | (~((~(apply(Morphism, zero(Dom)) = zero(Cod))) | (~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)))))))),
% 1.02/1.22 inference(bind,[status(th)],[])).
% 1.02/1.22 tff(5,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod)))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~(apply(Morphism, zero(Dom)) = zero(Cod))) | (~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))))))),
% 1.02/1.22 inference(quant_intro,[status(thm)],[4])).
% 1.02/1.22 tff(6,plain,
% 1.02/1.22 (^[Morphism: $i, Dom: $i, Cod: $i] : refl(((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod)))))) <=> ((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod)))))))),
% 1.02/1.22 inference(bind,[status(th)],[])).
% 1.02/1.22 tff(7,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod)))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod))))))),
% 1.02/1.22 inference(quant_intro,[status(thm)],[6])).
% 1.02/1.22 tff(8,plain,
% 1.02/1.22 (^[Morphism: $i, Dom: $i, Cod: $i] : rewrite(((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod)))))) <=> ((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod)))))))),
% 1.02/1.22 inference(bind,[status(th)],[])).
% 1.02/1.22 tff(9,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod)))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod))))))),
% 1.02/1.22 inference(quant_intro,[status(thm)],[8])).
% 1.02/1.22 tff(10,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod)))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod))))))),
% 1.02/1.22 inference(transitivity,[status(thm)],[9, 7])).
% 1.02/1.22 tff(11,plain,
% 1.02/1.22 (^[Morphism: $i, Dom: $i, Cod: $i] : rewrite(((~morphism(Morphism, Dom, Cod)) | (![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod)))) <=> ((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod)))))))),
% 1.02/1.22 inference(bind,[status(th)],[])).
% 1.02/1.22 tff(12,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod)))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod))))))),
% 1.02/1.22 inference(quant_intro,[status(thm)],[11])).
% 1.02/1.22 tff(13,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod)))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod))))),
% 1.02/1.22 inference(rewrite,[status(thm)],[])).
% 1.02/1.22 tff(14,plain,
% 1.02/1.22 (^[Morphism: $i, Dom: $i, Cod: $i] : trans(monotonicity(rewrite((![El: $i] : (element(El, Dom) => element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod))) <=> (![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod)))), ((morphism(Morphism, Dom, Cod) => (![El: $i] : (element(El, Dom) => element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod)))) <=> (morphism(Morphism, Dom, Cod) => (![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod)))))), rewrite((morphism(Morphism, Dom, Cod) => (![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod)))) <=> ((~morphism(Morphism, Dom, Cod)) | (![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod))))), ((morphism(Morphism, Dom, Cod) => (![El: $i] : (element(El, Dom) => element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod)))) <=> ((~morphism(Morphism, Dom, Cod)) | (![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod))))))),
% 1.02/1.22 inference(bind,[status(th)],[])).
% 1.02/1.22 tff(15,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : (morphism(Morphism, Dom, Cod) => (![El: $i] : (element(El, Dom) => element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod)))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod))))),
% 1.02/1.22 inference(quant_intro,[status(thm)],[14])).
% 1.02/1.22 tff(16,axiom,(![Morphism: $i, Dom: $i, Cod: $i] : (morphism(Morphism, Dom, Cod) => (![El: $i] : (element(El, Dom) => element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod))))), file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax','morphism')).
% 1.02/1.22 tff(17,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod))))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[16, 15])).
% 1.02/1.22 tff(18,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod))))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[17, 13])).
% 1.02/1.22 tff(19,plain,(
% 1.02/1.22 ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod)) & (apply(Morphism, zero(Dom)) = zero(Cod))))),
% 1.02/1.22 inference(skolemize,[status(sab)],[18])).
% 1.02/1.22 tff(20,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod))))))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[19, 12])).
% 1.02/1.22 tff(21,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))) | (~(apply(Morphism, zero(Dom)) = zero(Cod))))))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[20, 10])).
% 1.02/1.22 tff(22,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~(apply(Morphism, zero(Dom)) = zero(Cod))) | (~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))))))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[21, 5])).
% 1.02/1.22 tff(23,plain,
% 1.02/1.22 (((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~(apply(Morphism, zero(Dom)) = zero(Cod))) | (~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))))))) | ((~morphism(x, any1, any2)) | (~((~(apply(x, zero(any1)) = zero(any2))) | (~![El: $i] : ((~element(El, any1)) | element(apply(x, El), any2))))))) <=> ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~(apply(Morphism, zero(Dom)) = zero(Cod))) | (~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))))))) | (~morphism(x, any1, any2)) | (~((~(apply(x, zero(any1)) = zero(any2))) | (~![El: $i] : ((~element(El, any1)) | element(apply(x, El), any2))))))),
% 1.02/1.22 inference(rewrite,[status(thm)],[])).
% 1.02/1.22 tff(24,plain,
% 1.02/1.22 ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~(apply(Morphism, zero(Dom)) = zero(Cod))) | (~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))))))) | ((~morphism(x, any1, any2)) | (~((~(apply(x, zero(any1)) = zero(any2))) | (~![El: $i] : ((~element(El, any1)) | element(apply(x, El), any2))))))),
% 1.02/1.22 inference(quant_inst,[status(thm)],[])).
% 1.02/1.22 tff(25,plain,
% 1.02/1.22 ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~((~(apply(Morphism, zero(Dom)) = zero(Cod))) | (~![El: $i] : ((~element(El, Dom)) | element(apply(Morphism, El), Cod))))))) | (~morphism(x, any1, any2)) | (~((~(apply(x, zero(any1)) = zero(any2))) | (~![El: $i] : ((~element(El, any1)) | element(apply(x, El), any2)))))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[24, 23])).
% 1.02/1.22 tff(26,plain,
% 1.02/1.22 (~((~(apply(x, zero(any1)) = zero(any2))) | (~![El: $i] : ((~element(El, any1)) | element(apply(x, El), any2))))),
% 1.02/1.22 inference(unit_resolution,[status(thm)],[25, 22, 3])).
% 1.02/1.22 tff(27,plain,
% 1.02/1.22 (((~(apply(x, zero(any1)) = zero(any2))) | (~![El: $i] : ((~element(El, any1)) | element(apply(x, El), any2)))) | (apply(x, zero(any1)) = zero(any2))),
% 1.02/1.22 inference(tautology,[status(thm)],[])).
% 1.02/1.22 tff(28,plain,
% 1.02/1.22 (apply(x, zero(any1)) = zero(any2)),
% 1.02/1.22 inference(unit_resolution,[status(thm)],[27, 26])).
% 1.02/1.22 tff(29,plain,
% 1.02/1.22 (zero(any2) = apply(x, zero(any1))),
% 1.02/1.22 inference(symmetry,[status(thm)],[28])).
% 1.02/1.22 tff(30,assumption,(~injection_2(x)), introduced(assumption)).
% 1.02/1.22 tff(31,plain,
% 1.02/1.22 (^[Morphism: $i, Dom: $i, Cod: $i] : refl((injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)) | (~element(tptp_fun_El_8(Cod, Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod)))))) <=> (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)) | (~element(tptp_fun_El_8(Cod, Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod)))))))),
% 1.02/1.22 inference(bind,[status(th)],[])).
% 1.02/1.22 tff(32,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)) | (~element(tptp_fun_El_8(Cod, Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod)))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)) | (~element(tptp_fun_El_8(Cod, Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod))))))),
% 1.02/1.22 inference(quant_intro,[status(thm)],[31])).
% 1.02/1.22 tff(33,plain,
% 1.02/1.22 (^[Morphism: $i, Dom: $i, Cod: $i] : rewrite((injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El_8(Cod, Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod)))) | (tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom))))) <=> (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)) | (~element(tptp_fun_El_8(Cod, Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod)))))))),
% 1.02/1.22 inference(bind,[status(th)],[])).
% 1.02/1.22 tff(34,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El_8(Cod, Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod)))) | (tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)) | (~element(tptp_fun_El_8(Cod, Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod))))))),
% 1.02/1.22 inference(quant_intro,[status(thm)],[33])).
% 1.02/1.22 tff(35,plain,
% 1.02/1.22 (^[Morphism: $i, Dom: $i, Cod: $i] : rewrite((injection_2(Morphism) | ((~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El_8(Cod, Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod)))) | (tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)))))) <=> (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El_8(Cod, Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod)))) | (tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom))))))),
% 1.02/1.22 inference(bind,[status(th)],[])).
% 1.02/1.22 tff(36,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | ((~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El_8(Cod, Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod)))) | (tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El_8(Cod, Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod)))) | (tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)))))),
% 1.02/1.22 inference(quant_intro,[status(thm)],[35])).
% 1.02/1.22 tff(37,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom)))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))))),
% 1.02/1.22 inference(rewrite,[status(thm)],[])).
% 1.02/1.22 tff(38,plain,
% 1.02/1.22 (^[Morphism: $i, Dom: $i, Cod: $i] : trans(monotonicity(rewrite((morphism(Morphism, Dom, Cod) & ![El: $i] : ((element(El, Dom) & (apply(Morphism, El) = zero(Cod))) => (El = zero(Dom)))) <=> (morphism(Morphism, Dom, Cod) & ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))), (((morphism(Morphism, Dom, Cod) & ![El: $i] : ((element(El, Dom) & (apply(Morphism, El) = zero(Cod))) => (El = zero(Dom)))) => injection_2(Morphism)) <=> ((morphism(Morphism, Dom, Cod) & ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom)))) => injection_2(Morphism)))), rewrite(((morphism(Morphism, Dom, Cod) & ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom)))) => injection_2(Morphism)) <=> (injection_2(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))))), (((morphism(Morphism, Dom, Cod) & ![El: $i] : ((element(El, Dom) & (apply(Morphism, El) = zero(Cod))) => (El = zero(Dom)))) => injection_2(Morphism)) <=> (injection_2(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))))))),
% 1.02/1.22 inference(bind,[status(th)],[])).
% 1.02/1.22 tff(39,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : ((morphism(Morphism, Dom, Cod) & ![El: $i] : ((element(El, Dom) & (apply(Morphism, El) = zero(Cod))) => (El = zero(Dom)))) => injection_2(Morphism)) <=> ![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))))),
% 1.02/1.22 inference(quant_intro,[status(thm)],[38])).
% 1.02/1.22 tff(40,axiom,(![Morphism: $i, Dom: $i, Cod: $i] : ((morphism(Morphism, Dom, Cod) & ![El: $i] : ((element(El, Dom) & (apply(Morphism, El) = zero(Cod))) => (El = zero(Dom)))) => injection_2(Morphism))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','properties_for_injection_2')).
% 1.02/1.22 tff(41,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[40, 39])).
% 1.02/1.22 tff(42,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[41, 37])).
% 1.02/1.22 tff(43,plain,(
% 1.02/1.22 ![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | ((~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El_8(Cod, Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod)))) | (tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom))))))),
% 1.02/1.22 inference(skolemize,[status(sab)],[42])).
% 1.02/1.22 tff(44,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El_8(Cod, Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod)))) | (tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)))))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[43, 36])).
% 1.02/1.22 tff(45,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)) | (~element(tptp_fun_El_8(Cod, Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod))))))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[44, 34])).
% 1.02/1.22 tff(46,plain,
% 1.02/1.22 (![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)) | (~element(tptp_fun_El_8(Cod, Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod))))))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[45, 32])).
% 1.02/1.22 tff(47,plain,
% 1.02/1.22 (((~![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)) | (~element(tptp_fun_El_8(Cod, Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod))))))) | (injection_2(x) | (~morphism(x, any1, any2)) | (~((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = zero(any2))))))) <=> ((~![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)) | (~element(tptp_fun_El_8(Cod, Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod))))))) | injection_2(x) | (~morphism(x, any1, any2)) | (~((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = zero(any2))))))),
% 1.02/1.22 inference(rewrite,[status(thm)],[])).
% 1.02/1.22 tff(48,plain,
% 1.02/1.22 ((~![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)) | (~element(tptp_fun_El_8(Cod, Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod))))))) | (injection_2(x) | (~morphism(x, any1, any2)) | (~((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = zero(any2))))))),
% 1.02/1.22 inference(quant_inst,[status(thm)],[])).
% 1.02/1.22 tff(49,plain,
% 1.02/1.22 ((~![Morphism: $i, Dom: $i, Cod: $i] : (injection_2(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El_8(Cod, Dom, Morphism) = zero(Dom)) | (~element(tptp_fun_El_8(Cod, Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El_8(Cod, Dom, Morphism)) = zero(Cod))))))) | injection_2(x) | (~morphism(x, any1, any2)) | (~((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = zero(any2)))))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[48, 47])).
% 1.02/1.22 tff(50,plain,
% 1.02/1.22 (injection_2(x) | (~((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = zero(any2)))))),
% 1.02/1.22 inference(unit_resolution,[status(thm)],[49, 46, 3])).
% 1.02/1.22 tff(51,plain,
% 1.02/1.22 (~((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = zero(any2))))),
% 1.02/1.22 inference(unit_resolution,[status(thm)],[50, 30])).
% 1.02/1.22 tff(52,plain,
% 1.02/1.22 (((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = zero(any2)))) | (apply(x, tptp_fun_El_8(any2, any1, x)) = zero(any2))),
% 1.02/1.22 inference(tautology,[status(thm)],[])).
% 1.02/1.22 tff(53,plain,
% 1.02/1.22 (apply(x, tptp_fun_El_8(any2, any1, x)) = zero(any2)),
% 1.02/1.22 inference(unit_resolution,[status(thm)],[52, 51])).
% 1.02/1.22 tff(54,plain,
% 1.02/1.22 (apply(x, tptp_fun_El_8(any2, any1, x)) = apply(x, zero(any1))),
% 1.02/1.22 inference(transitivity,[status(thm)],[53, 29])).
% 1.02/1.22 tff(55,plain,
% 1.02/1.22 (((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = zero(any2)))) | element(tptp_fun_El_8(any2, any1, x), any1)),
% 1.02/1.22 inference(tautology,[status(thm)],[])).
% 1.02/1.22 tff(56,plain,
% 1.02/1.22 (element(tptp_fun_El_8(any2, any1, x), any1)),
% 1.02/1.22 inference(unit_resolution,[status(thm)],[55, 51])).
% 1.02/1.22 tff(57,plain,
% 1.02/1.22 (^[Dom: $i, El: $i] : refl(((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom))) <=> ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom))))),
% 1.02/1.22 inference(bind,[status(th)],[])).
% 1.02/1.22 tff(58,plain,
% 1.02/1.22 (![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom))) <=> ![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))),
% 1.02/1.22 inference(quant_intro,[status(thm)],[57])).
% 1.02/1.22 tff(59,plain,
% 1.02/1.22 (![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom))) <=> ![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))),
% 1.02/1.22 inference(rewrite,[status(thm)],[])).
% 1.02/1.22 tff(60,plain,
% 1.02/1.22 (^[Dom: $i, El: $i] : rewrite((element(El, Dom) => (subtract(Dom, El, El) = zero(Dom))) <=> ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom))))),
% 1.02/1.22 inference(bind,[status(th)],[])).
% 1.02/1.22 tff(61,plain,
% 1.02/1.22 (![Dom: $i, El: $i] : (element(El, Dom) => (subtract(Dom, El, El) = zero(Dom))) <=> ![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))),
% 1.02/1.22 inference(quant_intro,[status(thm)],[60])).
% 1.02/1.22 tff(62,axiom,(![Dom: $i, El: $i] : (element(El, Dom) => (subtract(Dom, El, El) = zero(Dom)))), file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax','subtract_to_0')).
% 1.02/1.22 tff(63,plain,
% 1.02/1.22 (![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[62, 61])).
% 1.02/1.22 tff(64,plain,
% 1.02/1.22 (![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[63, 59])).
% 1.02/1.22 tff(65,plain,(
% 1.02/1.22 ![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))),
% 1.02/1.22 inference(skolemize,[status(sab)],[64])).
% 1.02/1.22 tff(66,plain,
% 1.02/1.22 (![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[65, 58])).
% 1.02/1.22 tff(67,plain,
% 1.02/1.22 (((~![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))) | ((~element(tptp_fun_El_8(any2, any1, x), any1)) | (subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)) = zero(any1)))) <=> ((~![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)) = zero(any1)))),
% 1.02/1.22 inference(rewrite,[status(thm)],[])).
% 1.02/1.22 tff(68,plain,
% 1.02/1.22 ((~![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))) | ((~element(tptp_fun_El_8(any2, any1, x), any1)) | (subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)) = zero(any1)))),
% 1.02/1.22 inference(quant_inst,[status(thm)],[])).
% 1.02/1.22 tff(69,plain,
% 1.02/1.22 ((~![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)) = zero(any1))),
% 1.02/1.22 inference(modus_ponens,[status(thm)],[68, 67])).
% 1.02/1.22 tff(70,plain,
% 1.02/1.22 (subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)) = zero(any1)),
% 1.02/1.22 inference(unit_resolution,[status(thm)],[69, 66, 56])).
% 1.02/1.22 tff(71,plain,
% 1.02/1.22 (element(subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)), any1) <=> element(zero(any1), any1)),
% 1.02/1.22 inference(monotonicity,[status(thm)],[70])).
% 1.02/1.22 tff(72,plain,
% 1.02/1.22 (^[Dom: $i, El1: $i, El2: $i] : refl((element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom))) <=> (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom))))),
% 1.02/1.22 inference(bind,[status(th)],[])).
% 1.02/1.22 tff(73,plain,
% 1.02/1.22 (![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom))) <=> ![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))),
% 1.02/1.22 inference(quant_intro,[status(thm)],[72])).
% 1.02/1.22 tff(74,plain,
% 1.02/1.22 (^[Dom: $i, El1: $i, El2: $i] : trans(monotonicity(trans(monotonicity(rewrite((element(El1, Dom) & element(El2, Dom)) <=> (~((~element(El2, Dom)) | (~element(El1, Dom))))), ((~(element(El1, Dom) & element(El2, Dom))) <=> (~(~((~element(El2, Dom)) | (~element(El1, Dom))))))), rewrite((~(~((~element(El2, Dom)) | (~element(El1, Dom))))) <=> ((~element(El2, Dom)) | (~element(El1, Dom)))), ((~(element(El1, Dom) & element(El2, Dom))) <=> ((~element(El2, Dom)) | (~element(El1, Dom))))), (((~(element(El1, Dom) & element(El2, Dom))) | element(subtract(Dom, El1, El2), Dom)) <=> (((~element(El2, Dom)) | (~element(El1, Dom))) | element(subtract(Dom, El1, El2), Dom)))), rewrite((((~element(El2, Dom)) | (~element(El1, Dom))) | element(subtract(Dom, El1, El2), Dom)) <=> (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))), (((~(element(El1, Dom) & element(El2, Dom))) | element(subtract(Dom, El1, El2), Dom)) <=> (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))))),
% 1.02/1.22 inference(bind,[status(th)],[])).
% 1.02/1.22 tff(75,plain,
% 1.02/1.22 (![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | element(subtract(Dom, El1, El2), Dom)) <=> ![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))),
% 1.02/1.22 inference(quant_intro,[status(thm)],[74])).
% 1.02/1.22 tff(76,plain,
% 1.02/1.22 (![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | element(subtract(Dom, El1, El2), Dom)) <=> ![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | element(subtract(Dom, El1, El2), Dom))),
% 1.02/1.22 inference(rewrite,[status(thm)],[])).
% 1.02/1.22 tff(77,plain,
% 1.02/1.22 (^[Dom: $i, El1: $i, El2: $i] : rewrite(((element(El1, Dom) & element(El2, Dom)) => element(subtract(Dom, El1, El2), Dom)) <=> ((~(element(El1, Dom) & element(El2, Dom))) | element(subtract(Dom, El1, El2), Dom)))),
% 1.02/1.23 inference(bind,[status(th)],[])).
% 1.02/1.23 tff(78,plain,
% 1.02/1.23 (![Dom: $i, El1: $i, El2: $i] : ((element(El1, Dom) & element(El2, Dom)) => element(subtract(Dom, El1, El2), Dom)) <=> ![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | element(subtract(Dom, El1, El2), Dom))),
% 1.02/1.23 inference(quant_intro,[status(thm)],[77])).
% 1.02/1.23 tff(79,axiom,(![Dom: $i, El1: $i, El2: $i] : ((element(El1, Dom) & element(El2, Dom)) => element(subtract(Dom, El1, El2), Dom))), file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax','subtract_in_domain')).
% 1.02/1.23 tff(80,plain,
% 1.02/1.23 (![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | element(subtract(Dom, El1, El2), Dom))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[79, 78])).
% 1.02/1.23 tff(81,plain,
% 1.02/1.23 (![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | element(subtract(Dom, El1, El2), Dom))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[80, 76])).
% 1.02/1.23 tff(82,plain,(
% 1.02/1.23 ![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | element(subtract(Dom, El1, El2), Dom))),
% 1.02/1.23 inference(skolemize,[status(sab)],[81])).
% 1.02/1.23 tff(83,plain,
% 1.02/1.23 (![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[82, 75])).
% 1.02/1.23 tff(84,plain,
% 1.02/1.23 (![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[83, 73])).
% 1.02/1.23 tff(85,plain,
% 1.02/1.23 (((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((~element(tptp_fun_El_8(any2, any1, x), any1)) | element(subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)), any1))) <=> ((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | element(subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)), any1))),
% 1.02/1.23 inference(rewrite,[status(thm)],[])).
% 1.02/1.23 tff(86,plain,
% 1.02/1.23 ((element(subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)), any1) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1))) <=> ((~element(tptp_fun_El_8(any2, any1, x), any1)) | element(subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)), any1))),
% 1.02/1.23 inference(rewrite,[status(thm)],[])).
% 1.02/1.23 tff(87,plain,
% 1.02/1.23 (((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (element(subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)), any1) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)))) <=> ((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((~element(tptp_fun_El_8(any2, any1, x), any1)) | element(subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)), any1)))),
% 1.02/1.23 inference(monotonicity,[status(thm)],[86])).
% 1.02/1.23 tff(88,plain,
% 1.02/1.23 (((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (element(subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)), any1) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)))) <=> ((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | element(subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)), any1))),
% 1.02/1.23 inference(transitivity,[status(thm)],[87, 85])).
% 1.02/1.23 tff(89,plain,
% 1.02/1.23 ((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (element(subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)), any1) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)))),
% 1.02/1.23 inference(quant_inst,[status(thm)],[])).
% 1.02/1.23 tff(90,plain,
% 1.02/1.23 ((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | element(subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)), any1)),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[89, 88])).
% 1.02/1.23 tff(91,plain,
% 1.02/1.23 (element(subtract(any1, tptp_fun_El_8(any2, any1, x), tptp_fun_El_8(any2, any1, x)), any1)),
% 1.02/1.23 inference(unit_resolution,[status(thm)],[90, 84, 56])).
% 1.02/1.23 tff(92,plain,
% 1.02/1.23 (element(zero(any1), any1)),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[91, 71])).
% 1.02/1.23 tff(93,plain,
% 1.02/1.23 ((~(injection(x) <=> injection_2(x))) <=> (~(injection(x) <=> injection_2(x)))),
% 1.02/1.23 inference(rewrite,[status(thm)],[])).
% 1.02/1.23 tff(94,axiom,(~(injection(x) <=> injection_2(x))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','my')).
% 1.02/1.23 tff(95,plain,
% 1.02/1.23 (~(injection(x) <=> injection_2(x))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[94, 93])).
% 1.02/1.23 tff(96,plain,
% 1.02/1.23 (~(injection(x) <=> injection_2(x))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[95, 93])).
% 1.02/1.23 tff(97,plain,
% 1.02/1.23 (~(injection(x) <=> injection_2(x))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[96, 93])).
% 1.02/1.23 tff(98,plain,
% 1.02/1.23 (~(injection(x) <=> injection_2(x))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[97, 93])).
% 1.02/1.23 tff(99,plain,
% 1.02/1.23 (~(injection(x) <=> injection_2(x))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[98, 93])).
% 1.02/1.23 tff(100,plain,
% 1.02/1.23 ((injection(x) <=> injection_2(x)) | injection(x) | injection_2(x)),
% 1.02/1.23 inference(tautology,[status(thm)],[])).
% 1.02/1.23 tff(101,plain,
% 1.02/1.23 (injection(x) | injection_2(x)),
% 1.02/1.23 inference(unit_resolution,[status(thm)],[100, 99])).
% 1.02/1.23 tff(102,plain,
% 1.02/1.23 (injection(x)),
% 1.02/1.23 inference(unit_resolution,[status(thm)],[101, 30])).
% 1.02/1.23 tff(103,plain,
% 1.02/1.23 (^[Morphism: $i, Dom: $i, Cod: $i] : refl(((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2))))) <=> ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2))))))),
% 1.02/1.23 inference(bind,[status(th)],[])).
% 1.02/1.23 tff(104,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))),
% 1.02/1.23 inference(quant_intro,[status(thm)],[103])).
% 1.02/1.23 tff(105,plain,
% 1.02/1.23 (^[Morphism: $i, Dom: $i, Cod: $i] : rewrite(((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2))))) <=> ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2))))))),
% 1.02/1.23 inference(bind,[status(th)],[])).
% 1.02/1.23 tff(106,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))),
% 1.02/1.23 inference(quant_intro,[status(thm)],[105])).
% 1.02/1.23 tff(107,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))),
% 1.02/1.23 inference(transitivity,[status(thm)],[106, 104])).
% 1.02/1.23 tff(108,plain,
% 1.02/1.23 (^[Morphism: $i, Dom: $i, Cod: $i] : trans(monotonicity(trans(monotonicity(rewrite((injection(Morphism) & morphism(Morphism, Dom, Cod)) <=> (~((~injection(Morphism)) | (~morphism(Morphism, Dom, Cod))))), ((~(injection(Morphism) & morphism(Morphism, Dom, Cod))) <=> (~(~((~injection(Morphism)) | (~morphism(Morphism, Dom, Cod))))))), rewrite((~(~((~injection(Morphism)) | (~morphism(Morphism, Dom, Cod))))) <=> ((~injection(Morphism)) | (~morphism(Morphism, Dom, Cod)))), ((~(injection(Morphism) & morphism(Morphism, Dom, Cod))) <=> ((~injection(Morphism)) | (~morphism(Morphism, Dom, Cod))))), quant_intro(proof_bind(^[El1: $i, El2: $i] : trans(monotonicity(trans(monotonicity(rewrite((element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2))) <=> (~((~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))), ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) <=> (~(~((~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))))), rewrite((~(~((~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))) <=> ((~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2))))), ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) <=> ((~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))), (((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)) <=> (((~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))), rewrite((((~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)) <=> ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2))))), (((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)) <=> ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2))))))), (![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)) <=> ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))), (((~(injection(Morphism) & morphism(Morphism, Dom, Cod))) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2))) <=> (((~injection(Morphism)) | (~morphism(Morphism, Dom, Cod))) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2))))))), rewrite((((~injection(Morphism)) | (~morphism(Morphism, Dom, Cod))) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2))))) <=> ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))), (((~(injection(Morphism) & morphism(Morphism, Dom, Cod))) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2))) <=> ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))))),
% 1.02/1.23 inference(bind,[status(th)],[])).
% 1.02/1.23 tff(109,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection(Morphism) & morphism(Morphism, Dom, Cod))) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))),
% 1.02/1.23 inference(quant_intro,[status(thm)],[108])).
% 1.02/1.23 tff(110,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection(Morphism) & morphism(Morphism, Dom, Cod))) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection(Morphism) & morphism(Morphism, Dom, Cod))) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))),
% 1.02/1.23 inference(rewrite,[status(thm)],[])).
% 1.02/1.23 tff(111,plain,
% 1.02/1.23 (^[Morphism: $i, Dom: $i, Cod: $i] : trans(monotonicity(quant_intro(proof_bind(^[El1: $i, El2: $i] : trans(monotonicity(rewrite(((element(El1, Dom) & element(El2, Dom)) & (apply(Morphism, El1) = apply(Morphism, El2))) <=> (element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))), ((((element(El1, Dom) & element(El2, Dom)) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2)) <=> ((element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2)))), rewrite(((element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2)) <=> ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2))), ((((element(El1, Dom) & element(El2, Dom)) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2)) <=> ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2))))), (![El1: $i, El2: $i] : (((element(El1, Dom) & element(El2, Dom)) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2)) <=> ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))), (((injection(Morphism) & morphism(Morphism, Dom, Cod)) => ![El1: $i, El2: $i] : (((element(El1, Dom) & element(El2, Dom)) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2))) <=> ((injection(Morphism) & morphism(Morphism, Dom, Cod)) => ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2))))), rewrite(((injection(Morphism) & morphism(Morphism, Dom, Cod)) => ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2))) <=> ((~(injection(Morphism) & morphism(Morphism, Dom, Cod))) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))), (((injection(Morphism) & morphism(Morphism, Dom, Cod)) => ![El1: $i, El2: $i] : (((element(El1, Dom) & element(El2, Dom)) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2))) <=> ((~(injection(Morphism) & morphism(Morphism, Dom, Cod))) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))))),
% 1.02/1.23 inference(bind,[status(th)],[])).
% 1.02/1.23 tff(112,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : ((injection(Morphism) & morphism(Morphism, Dom, Cod)) => ![El1: $i, El2: $i] : (((element(El1, Dom) & element(El2, Dom)) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection(Morphism) & morphism(Morphism, Dom, Cod))) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))),
% 1.02/1.23 inference(quant_intro,[status(thm)],[111])).
% 1.02/1.23 tff(113,axiom,(![Morphism: $i, Dom: $i, Cod: $i] : ((injection(Morphism) & morphism(Morphism, Dom, Cod)) => ![El1: $i, El2: $i] : (((element(El1, Dom) & element(El2, Dom)) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2)))), file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax','injection_properties')).
% 1.02/1.23 tff(114,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection(Morphism) & morphism(Morphism, Dom, Cod))) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[113, 112])).
% 1.02/1.23 tff(115,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection(Morphism) & morphism(Morphism, Dom, Cod))) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[114, 110])).
% 1.02/1.23 tff(116,plain,(
% 1.02/1.23 ![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection(Morphism) & morphism(Morphism, Dom, Cod))) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))),
% 1.02/1.23 inference(skolemize,[status(sab)],[115])).
% 1.02/1.23 tff(117,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[116, 109])).
% 1.02/1.23 tff(118,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[117, 107])).
% 1.02/1.23 tff(119,plain,
% 1.02/1.23 (((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))) | ((~injection(x)) | (~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2)))))) <=> ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))) | (~injection(x)) | (~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2)))))),
% 1.02/1.23 inference(rewrite,[status(thm)],[])).
% 1.02/1.23 tff(120,plain,
% 1.02/1.23 (((~morphism(x, any1, any2)) | (~injection(x)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))) <=> ((~injection(x)) | (~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2)))))),
% 1.02/1.23 inference(rewrite,[status(thm)],[])).
% 1.02/1.23 tff(121,plain,
% 1.02/1.23 (^[El1: $i, El2: $i] : rewrite(((El1 = El2) | (~element(El1, any1)) | (~element(El2, any1)) | (~(apply(x, El1) = apply(x, El2)))) <=> ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2)))))),
% 1.02/1.23 inference(bind,[status(th)],[])).
% 1.02/1.23 tff(122,plain,
% 1.02/1.23 (![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, any1)) | (~element(El2, any1)) | (~(apply(x, El1) = apply(x, El2)))) <=> ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))),
% 1.02/1.23 inference(quant_intro,[status(thm)],[121])).
% 1.02/1.23 tff(123,plain,
% 1.02/1.23 (((~morphism(x, any1, any2)) | (~injection(x)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, any1)) | (~element(El2, any1)) | (~(apply(x, El1) = apply(x, El2))))) <=> ((~morphism(x, any1, any2)) | (~injection(x)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2)))))),
% 1.02/1.23 inference(monotonicity,[status(thm)],[122])).
% 1.02/1.23 tff(124,plain,
% 1.02/1.23 (((~morphism(x, any1, any2)) | (~injection(x)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, any1)) | (~element(El2, any1)) | (~(apply(x, El1) = apply(x, El2))))) <=> ((~injection(x)) | (~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2)))))),
% 1.02/1.23 inference(transitivity,[status(thm)],[123, 120])).
% 1.02/1.23 tff(125,plain,
% 1.02/1.23 (((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))) | ((~morphism(x, any1, any2)) | (~injection(x)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, any1)) | (~element(El2, any1)) | (~(apply(x, El1) = apply(x, El2)))))) <=> ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))) | ((~injection(x)) | (~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))))),
% 1.02/1.23 inference(monotonicity,[status(thm)],[124])).
% 1.02/1.23 tff(126,plain,
% 1.02/1.23 (((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))) | ((~morphism(x, any1, any2)) | (~injection(x)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, any1)) | (~element(El2, any1)) | (~(apply(x, El1) = apply(x, El2)))))) <=> ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))) | (~injection(x)) | (~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2)))))),
% 1.02/1.23 inference(transitivity,[status(thm)],[125, 119])).
% 1.02/1.23 tff(127,plain,
% 1.02/1.23 ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))) | ((~morphism(x, any1, any2)) | (~injection(x)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, any1)) | (~element(El2, any1)) | (~(apply(x, El1) = apply(x, El2)))))),
% 1.02/1.23 inference(quant_inst,[status(thm)],[])).
% 1.02/1.23 tff(128,plain,
% 1.02/1.23 ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection(Morphism)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El1, Dom)) | (~element(El2, Dom)) | (~(apply(Morphism, El1) = apply(Morphism, El2)))))) | (~injection(x)) | (~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[127, 126])).
% 1.02/1.23 tff(129,plain,
% 1.02/1.23 ((~injection(x)) | ![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))),
% 1.02/1.23 inference(unit_resolution,[status(thm)],[128, 118, 3])).
% 1.02/1.23 tff(130,plain,
% 1.02/1.23 (![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))),
% 1.02/1.23 inference(unit_resolution,[status(thm)],[129, 102])).
% 1.02/1.23 tff(131,plain,
% 1.02/1.23 (((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = zero(any2)))) | (~(tptp_fun_El_8(any2, any1, x) = zero(any1)))),
% 1.02/1.23 inference(tautology,[status(thm)],[])).
% 1.02/1.23 tff(132,plain,
% 1.02/1.23 (~(tptp_fun_El_8(any2, any1, x) = zero(any1))),
% 1.02/1.23 inference(unit_resolution,[status(thm)],[131, 51])).
% 1.02/1.23 tff(133,plain,
% 1.02/1.23 (((~![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))) | ((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~element(zero(any1), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = apply(x, zero(any1)))))) <=> ((~![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))) | (tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~element(zero(any1), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = apply(x, zero(any1)))))),
% 1.02/1.23 inference(rewrite,[status(thm)],[])).
% 1.02/1.23 tff(134,plain,
% 1.02/1.23 (((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(zero(any1), any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = apply(x, zero(any1))))) <=> ((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~element(zero(any1), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = apply(x, zero(any1)))))),
% 1.02/1.23 inference(rewrite,[status(thm)],[])).
% 1.02/1.23 tff(135,plain,
% 1.02/1.23 (((~![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))) | ((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(zero(any1), any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = apply(x, zero(any1)))))) <=> ((~![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))) | ((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~element(zero(any1), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = apply(x, zero(any1))))))),
% 1.02/1.23 inference(monotonicity,[status(thm)],[134])).
% 1.02/1.23 tff(136,plain,
% 1.02/1.23 (((~![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))) | ((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(zero(any1), any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = apply(x, zero(any1)))))) <=> ((~![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))) | (tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~element(zero(any1), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = apply(x, zero(any1)))))),
% 1.02/1.23 inference(transitivity,[status(thm)],[135, 133])).
% 1.02/1.23 tff(137,plain,
% 1.02/1.23 ((~![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))) | ((tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(zero(any1), any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = apply(x, zero(any1)))))),
% 1.02/1.23 inference(quant_inst,[status(thm)],[])).
% 1.02/1.23 tff(138,plain,
% 1.02/1.23 ((~![El1: $i, El2: $i] : ((El1 = El2) | (~element(El2, any1)) | (~element(El1, any1)) | (~(apply(x, El1) = apply(x, El2))))) | (tptp_fun_El_8(any2, any1, x) = zero(any1)) | (~element(tptp_fun_El_8(any2, any1, x), any1)) | (~element(zero(any1), any1)) | (~(apply(x, tptp_fun_El_8(any2, any1, x)) = apply(x, zero(any1))))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[137, 136])).
% 1.02/1.23 tff(139,plain,
% 1.02/1.23 ($false),
% 1.02/1.23 inference(unit_resolution,[status(thm)],[138, 132, 56, 130, 92, 54])).
% 1.02/1.23 tff(140,plain,(injection_2(x)), inference(lemma,lemma(discharge,[]))).
% 1.02/1.23 tff(141,plain,
% 1.02/1.23 ((injection(x) <=> injection_2(x)) | (~injection(x)) | (~injection_2(x))),
% 1.02/1.23 inference(tautology,[status(thm)],[])).
% 1.02/1.23 tff(142,plain,
% 1.02/1.23 ((~injection(x)) | (~injection_2(x))),
% 1.02/1.23 inference(unit_resolution,[status(thm)],[141, 99])).
% 1.02/1.23 tff(143,plain,
% 1.02/1.23 (~injection(x)),
% 1.02/1.23 inference(unit_resolution,[status(thm)],[142, 140])).
% 1.02/1.23 tff(144,plain,
% 1.02/1.23 (^[Morphism: $i, Dom: $i, Cod: $i] : refl((injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)) | (~element(tptp_fun_El1_1(Dom, Morphism), Dom)) | (~element(tptp_fun_El2_0(Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism))))))) <=> (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)) | (~element(tptp_fun_El1_1(Dom, Morphism), Dom)) | (~element(tptp_fun_El2_0(Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism))))))))),
% 1.02/1.23 inference(bind,[status(th)],[])).
% 1.02/1.23 tff(145,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)) | (~element(tptp_fun_El1_1(Dom, Morphism), Dom)) | (~element(tptp_fun_El2_0(Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism))))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)) | (~element(tptp_fun_El1_1(Dom, Morphism), Dom)) | (~element(tptp_fun_El2_0(Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism)))))))),
% 1.02/1.23 inference(quant_intro,[status(thm)],[144])).
% 1.02/1.23 tff(146,plain,
% 1.02/1.23 (^[Morphism: $i, Dom: $i, Cod: $i] : rewrite((injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El1_1(Dom, Morphism), Dom) & element(tptp_fun_El2_0(Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism))))) | (tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism))))) <=> (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)) | (~element(tptp_fun_El1_1(Dom, Morphism), Dom)) | (~element(tptp_fun_El2_0(Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism))))))))),
% 1.02/1.23 inference(bind,[status(th)],[])).
% 1.02/1.23 tff(147,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El1_1(Dom, Morphism), Dom) & element(tptp_fun_El2_0(Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism))))) | (tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)) | (~element(tptp_fun_El1_1(Dom, Morphism), Dom)) | (~element(tptp_fun_El2_0(Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism)))))))),
% 1.02/1.23 inference(quant_intro,[status(thm)],[146])).
% 1.02/1.23 tff(148,plain,
% 1.02/1.23 (^[Morphism: $i, Dom: $i, Cod: $i] : rewrite((injection(Morphism) | ((~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El1_1(Dom, Morphism), Dom) & element(tptp_fun_El2_0(Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism))))) | (tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)))))) <=> (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El1_1(Dom, Morphism), Dom) & element(tptp_fun_El2_0(Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism))))) | (tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism))))))),
% 1.02/1.23 inference(bind,[status(th)],[])).
% 1.02/1.23 tff(149,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | ((~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El1_1(Dom, Morphism), Dom) & element(tptp_fun_El2_0(Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism))))) | (tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El1_1(Dom, Morphism), Dom) & element(tptp_fun_El2_0(Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism))))) | (tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)))))),
% 1.02/1.23 inference(quant_intro,[status(thm)],[148])).
% 1.02/1.23 tff(150,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))))),
% 1.02/1.23 inference(rewrite,[status(thm)],[])).
% 1.02/1.23 tff(151,plain,
% 1.02/1.23 (^[Morphism: $i, Dom: $i, Cod: $i] : trans(monotonicity(rewrite((morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : (((element(El1, Dom) & element(El2, Dom)) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2))) <=> (morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))), (((morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : (((element(El1, Dom) & element(El2, Dom)) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2))) => injection(Morphism)) <=> ((morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2))) => injection(Morphism)))), rewrite(((morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2))) => injection(Morphism)) <=> (injection(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))))), (((morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : (((element(El1, Dom) & element(El2, Dom)) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2))) => injection(Morphism)) <=> (injection(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))))))),
% 1.02/1.23 inference(bind,[status(th)],[])).
% 1.02/1.23 tff(152,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : ((morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : (((element(El1, Dom) & element(El2, Dom)) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2))) => injection(Morphism)) <=> ![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))))),
% 1.02/1.23 inference(quant_intro,[status(thm)],[151])).
% 1.02/1.23 tff(153,axiom,(![Morphism: $i, Dom: $i, Cod: $i] : ((morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : (((element(El1, Dom) & element(El2, Dom)) & (apply(Morphism, El1) = apply(Morphism, El2))) => (El1 = El2))) => injection(Morphism))), file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax','properties_for_injection')).
% 1.02/1.23 tff(154,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[153, 152])).
% 1.02/1.23 tff(155,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~(morphism(Morphism, Dom, Cod) & ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom) & (apply(Morphism, El1) = apply(Morphism, El2)))) | (El1 = El2)))))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[154, 150])).
% 1.02/1.23 tff(156,plain,(
% 1.02/1.23 ![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | ((~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El1_1(Dom, Morphism), Dom) & element(tptp_fun_El2_0(Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism))))) | (tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism))))))),
% 1.02/1.23 inference(skolemize,[status(sab)],[155])).
% 1.02/1.23 tff(157,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((~(element(tptp_fun_El1_1(Dom, Morphism), Dom) & element(tptp_fun_El2_0(Dom, Morphism), Dom) & (apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism))))) | (tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)))))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[156, 149])).
% 1.02/1.23 tff(158,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)) | (~element(tptp_fun_El1_1(Dom, Morphism), Dom)) | (~element(tptp_fun_El2_0(Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism)))))))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[157, 147])).
% 1.02/1.23 tff(159,plain,
% 1.02/1.23 (![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)) | (~element(tptp_fun_El1_1(Dom, Morphism), Dom)) | (~element(tptp_fun_El2_0(Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism)))))))),
% 1.02/1.23 inference(modus_ponens,[status(thm)],[158, 145])).
% 1.02/1.23 tff(160,plain,
% 1.02/1.23 (((~![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)) | (~element(tptp_fun_El1_1(Dom, Morphism), Dom)) | (~element(tptp_fun_El2_0(Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism)))))))) | (injection(x) | (~morphism(x, any1, any2)) | (~((tptp_fun_El1_1(any1, x) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~(apply(x, tptp_fun_El1_1(any1, x)) = apply(x, tptp_fun_El2_0(any1, x)))))))) <=> ((~![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)) | (~element(tptp_fun_El1_1(Dom, Morphism), Dom)) | (~element(tptp_fun_El2_0(Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism)))))))) | injection(x) | (~morphism(x, any1, any2)) | (~((tptp_fun_El1_1(any1, x) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~(apply(x, tptp_fun_El1_1(any1, x)) = apply(x, tptp_fun_El2_0(any1, x)))))))),
% 1.02/1.23 inference(rewrite,[status(thm)],[])).
% 1.02/1.23 tff(161,plain,
% 1.02/1.23 ((~![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)) | (~element(tptp_fun_El1_1(Dom, Morphism), Dom)) | (~element(tptp_fun_El2_0(Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism)))))))) | (injection(x) | (~morphism(x, any1, any2)) | (~((tptp_fun_El1_1(any1, x) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~(apply(x, tptp_fun_El1_1(any1, x)) = apply(x, tptp_fun_El2_0(any1, x)))))))),
% 1.02/1.23 inference(quant_inst,[status(thm)],[])).
% 1.02/1.23 tff(162,plain,
% 1.02/1.23 ((~![Morphism: $i, Dom: $i, Cod: $i] : (injection(Morphism) | (~morphism(Morphism, Dom, Cod)) | (~((tptp_fun_El1_1(Dom, Morphism) = tptp_fun_El2_0(Dom, Morphism)) | (~element(tptp_fun_El1_1(Dom, Morphism), Dom)) | (~element(tptp_fun_El2_0(Dom, Morphism), Dom)) | (~(apply(Morphism, tptp_fun_El1_1(Dom, Morphism)) = apply(Morphism, tptp_fun_El2_0(Dom, Morphism)))))))) | injection(x) | (~morphism(x, any1, any2)) | (~((tptp_fun_El1_1(any1, x) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~(apply(x, tptp_fun_El1_1(any1, x)) = apply(x, tptp_fun_El2_0(any1, x))))))),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[161, 160])).
% 1.02/1.24 tff(163,plain,
% 1.02/1.24 (injection(x) | (~((tptp_fun_El1_1(any1, x) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~(apply(x, tptp_fun_El1_1(any1, x)) = apply(x, tptp_fun_El2_0(any1, x))))))),
% 1.02/1.24 inference(unit_resolution,[status(thm)],[162, 159, 3])).
% 1.02/1.24 tff(164,plain,
% 1.02/1.24 (~((tptp_fun_El1_1(any1, x) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~(apply(x, tptp_fun_El1_1(any1, x)) = apply(x, tptp_fun_El2_0(any1, x)))))),
% 1.02/1.24 inference(unit_resolution,[status(thm)],[163, 143])).
% 1.02/1.24 tff(165,plain,
% 1.02/1.24 (((tptp_fun_El1_1(any1, x) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~(apply(x, tptp_fun_El1_1(any1, x)) = apply(x, tptp_fun_El2_0(any1, x))))) | element(tptp_fun_El2_0(any1, x), any1)),
% 1.02/1.24 inference(tautology,[status(thm)],[])).
% 1.02/1.24 tff(166,plain,
% 1.02/1.24 (element(tptp_fun_El2_0(any1, x), any1)),
% 1.02/1.24 inference(unit_resolution,[status(thm)],[165, 164])).
% 1.02/1.24 tff(167,plain,
% 1.02/1.24 (((tptp_fun_El1_1(any1, x) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~(apply(x, tptp_fun_El1_1(any1, x)) = apply(x, tptp_fun_El2_0(any1, x))))) | element(tptp_fun_El1_1(any1, x), any1)),
% 1.02/1.24 inference(tautology,[status(thm)],[])).
% 1.02/1.24 tff(168,plain,
% 1.02/1.24 (element(tptp_fun_El1_1(any1, x), any1)),
% 1.02/1.24 inference(unit_resolution,[status(thm)],[167, 164])).
% 1.02/1.24 tff(169,plain,
% 1.02/1.24 (^[Dom: $i, El1: $i, El2: $i] : refl(((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom))) <=> ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom))))),
% 1.02/1.24 inference(bind,[status(th)],[])).
% 1.02/1.24 tff(170,plain,
% 1.02/1.24 (![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom))) <=> ![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))),
% 1.02/1.24 inference(quant_intro,[status(thm)],[169])).
% 1.02/1.24 tff(171,plain,
% 1.02/1.24 (^[Dom: $i, El1: $i, El2: $i] : trans(monotonicity(trans(monotonicity(rewrite((element(El1, Dom) & element(El2, Dom)) <=> (~((~element(El2, Dom)) | (~element(El1, Dom))))), ((~(element(El1, Dom) & element(El2, Dom))) <=> (~(~((~element(El2, Dom)) | (~element(El1, Dom))))))), rewrite((~(~((~element(El2, Dom)) | (~element(El1, Dom))))) <=> ((~element(El2, Dom)) | (~element(El1, Dom)))), ((~(element(El1, Dom) & element(El2, Dom))) <=> ((~element(El2, Dom)) | (~element(El1, Dom))))), (((~(element(El1, Dom) & element(El2, Dom))) | (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2)) <=> (((~element(El2, Dom)) | (~element(El1, Dom))) | (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2)))), rewrite((((~element(El2, Dom)) | (~element(El1, Dom))) | (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2)) <=> ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))), (((~(element(El1, Dom) & element(El2, Dom))) | (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2)) <=> ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))))),
% 1.02/1.24 inference(bind,[status(th)],[])).
% 1.02/1.24 tff(172,plain,
% 1.02/1.24 (![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2)) <=> ![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))),
% 1.02/1.24 inference(quant_intro,[status(thm)],[171])).
% 1.02/1.24 tff(173,plain,
% 1.02/1.24 (![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2)) <=> ![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2))),
% 1.02/1.24 inference(rewrite,[status(thm)],[])).
% 1.02/1.24 tff(174,plain,
% 1.02/1.24 (^[Dom: $i, El1: $i, El2: $i] : rewrite(((element(El1, Dom) & element(El2, Dom)) => (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2)) <=> ((~(element(El1, Dom) & element(El2, Dom))) | (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2)))),
% 1.02/1.24 inference(bind,[status(th)],[])).
% 1.02/1.24 tff(175,plain,
% 1.02/1.24 (![Dom: $i, El1: $i, El2: $i] : ((element(El1, Dom) & element(El2, Dom)) => (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2)) <=> ![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2))),
% 1.02/1.24 inference(quant_intro,[status(thm)],[174])).
% 1.02/1.24 tff(176,axiom,(![Dom: $i, El1: $i, El2: $i] : ((element(El1, Dom) & element(El2, Dom)) => (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2))), file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax','subtract_cancellation')).
% 1.02/1.24 tff(177,plain,
% 1.02/1.24 (![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2))),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[176, 175])).
% 1.02/1.24 tff(178,plain,
% 1.02/1.24 (![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2))),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[177, 173])).
% 1.02/1.24 tff(179,plain,(
% 1.02/1.24 ![Dom: $i, El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (subtract(Dom, El1, subtract(Dom, El1, El2)) = El2))),
% 1.02/1.24 inference(skolemize,[status(sab)],[178])).
% 1.02/1.24 tff(180,plain,
% 1.02/1.24 (![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[179, 172])).
% 1.02/1.24 tff(181,plain,
% 1.02/1.24 (![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[180, 170])).
% 1.02/1.24 tff(182,plain,
% 1.02/1.24 (((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = tptp_fun_El2_0(any1, x)))) <=> ((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = tptp_fun_El2_0(any1, x)))),
% 1.02/1.24 inference(rewrite,[status(thm)],[])).
% 1.02/1.24 tff(183,plain,
% 1.02/1.24 (((subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~element(tptp_fun_El1_1(any1, x), any1))) <=> ((~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = tptp_fun_El2_0(any1, x)))),
% 1.02/1.24 inference(rewrite,[status(thm)],[])).
% 1.02/1.24 tff(184,plain,
% 1.02/1.24 (((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~element(tptp_fun_El1_1(any1, x), any1)))) <=> ((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = tptp_fun_El2_0(any1, x))))),
% 1.02/1.24 inference(monotonicity,[status(thm)],[183])).
% 1.02/1.24 tff(185,plain,
% 1.02/1.24 (((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~element(tptp_fun_El1_1(any1, x), any1)))) <=> ((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = tptp_fun_El2_0(any1, x)))),
% 1.02/1.24 inference(transitivity,[status(thm)],[184, 182])).
% 1.02/1.24 tff(186,plain,
% 1.02/1.24 ((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~element(tptp_fun_El1_1(any1, x), any1)))),
% 1.02/1.24 inference(quant_inst,[status(thm)],[])).
% 1.02/1.24 tff(187,plain,
% 1.02/1.24 ((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = tptp_fun_El2_0(any1, x))),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[186, 185])).
% 1.02/1.24 tff(188,plain,
% 1.02/1.24 (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = tptp_fun_El2_0(any1, x)),
% 1.02/1.24 inference(unit_resolution,[status(thm)],[187, 181, 168, 166])).
% 1.02/1.24 tff(189,plain,
% 1.02/1.24 (((~(apply(x, zero(any1)) = zero(any2))) | (~![El: $i] : ((~element(El, any1)) | element(apply(x, El), any2)))) | ![El: $i] : ((~element(El, any1)) | element(apply(x, El), any2))),
% 1.02/1.24 inference(tautology,[status(thm)],[])).
% 1.02/1.24 tff(190,plain,
% 1.02/1.24 (![El: $i] : ((~element(El, any1)) | element(apply(x, El), any2))),
% 1.02/1.24 inference(unit_resolution,[status(thm)],[189, 26])).
% 1.02/1.24 tff(191,plain,
% 1.02/1.24 (((~![El: $i] : ((~element(El, any1)) | element(apply(x, El), any2))) | ((~element(tptp_fun_El2_0(any1, x), any1)) | element(apply(x, tptp_fun_El2_0(any1, x)), any2))) <=> ((~![El: $i] : ((~element(El, any1)) | element(apply(x, El), any2))) | (~element(tptp_fun_El2_0(any1, x), any1)) | element(apply(x, tptp_fun_El2_0(any1, x)), any2))),
% 1.02/1.24 inference(rewrite,[status(thm)],[])).
% 1.02/1.24 tff(192,plain,
% 1.02/1.24 ((~![El: $i] : ((~element(El, any1)) | element(apply(x, El), any2))) | ((~element(tptp_fun_El2_0(any1, x), any1)) | element(apply(x, tptp_fun_El2_0(any1, x)), any2))),
% 1.02/1.24 inference(quant_inst,[status(thm)],[])).
% 1.02/1.24 tff(193,plain,
% 1.02/1.24 ((~![El: $i] : ((~element(El, any1)) | element(apply(x, El), any2))) | (~element(tptp_fun_El2_0(any1, x), any1)) | element(apply(x, tptp_fun_El2_0(any1, x)), any2)),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[192, 191])).
% 1.02/1.24 tff(194,plain,
% 1.02/1.24 (element(apply(x, tptp_fun_El2_0(any1, x)), any2)),
% 1.02/1.24 inference(unit_resolution,[status(thm)],[193, 166, 190])).
% 1.02/1.24 tff(195,plain,
% 1.02/1.24 (((~![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))) | ((~element(apply(x, tptp_fun_El2_0(any1, x)), any2)) | (subtract(any2, apply(x, tptp_fun_El2_0(any1, x)), apply(x, tptp_fun_El2_0(any1, x))) = zero(any2)))) <=> ((~![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))) | (~element(apply(x, tptp_fun_El2_0(any1, x)), any2)) | (subtract(any2, apply(x, tptp_fun_El2_0(any1, x)), apply(x, tptp_fun_El2_0(any1, x))) = zero(any2)))),
% 1.02/1.24 inference(rewrite,[status(thm)],[])).
% 1.02/1.24 tff(196,plain,
% 1.02/1.24 ((~![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))) | ((~element(apply(x, tptp_fun_El2_0(any1, x)), any2)) | (subtract(any2, apply(x, tptp_fun_El2_0(any1, x)), apply(x, tptp_fun_El2_0(any1, x))) = zero(any2)))),
% 1.02/1.24 inference(quant_inst,[status(thm)],[])).
% 1.02/1.24 tff(197,plain,
% 1.02/1.24 ((~![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))) | (~element(apply(x, tptp_fun_El2_0(any1, x)), any2)) | (subtract(any2, apply(x, tptp_fun_El2_0(any1, x)), apply(x, tptp_fun_El2_0(any1, x))) = zero(any2))),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[196, 195])).
% 1.02/1.24 tff(198,plain,
% 1.02/1.24 (subtract(any2, apply(x, tptp_fun_El2_0(any1, x)), apply(x, tptp_fun_El2_0(any1, x))) = zero(any2)),
% 1.02/1.24 inference(unit_resolution,[status(thm)],[197, 66, 194])).
% 1.02/1.24 tff(199,plain,
% 1.02/1.24 (((tptp_fun_El1_1(any1, x) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~(apply(x, tptp_fun_El1_1(any1, x)) = apply(x, tptp_fun_El2_0(any1, x))))) | (apply(x, tptp_fun_El1_1(any1, x)) = apply(x, tptp_fun_El2_0(any1, x)))),
% 1.02/1.24 inference(tautology,[status(thm)],[])).
% 1.02/1.24 tff(200,plain,
% 1.02/1.24 (apply(x, tptp_fun_El1_1(any1, x)) = apply(x, tptp_fun_El2_0(any1, x))),
% 1.02/1.24 inference(unit_resolution,[status(thm)],[199, 164])).
% 1.02/1.24 tff(201,plain,
% 1.02/1.24 (subtract(any2, apply(x, tptp_fun_El1_1(any1, x)), apply(x, tptp_fun_El2_0(any1, x))) = subtract(any2, apply(x, tptp_fun_El2_0(any1, x)), apply(x, tptp_fun_El2_0(any1, x)))),
% 1.02/1.24 inference(monotonicity,[status(thm)],[200])).
% 1.02/1.24 tff(202,plain,
% 1.02/1.24 (^[Morphism: $i, Dom: $i, Cod: $i] : refl(((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom)))) <=> ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom)))))),
% 1.02/1.24 inference(bind,[status(th)],[])).
% 1.02/1.24 tff(203,plain,
% 1.02/1.24 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom)))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))),
% 1.02/1.24 inference(quant_intro,[status(thm)],[202])).
% 1.02/1.24 tff(204,plain,
% 1.02/1.24 (^[Morphism: $i, Dom: $i, Cod: $i] : rewrite(((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom)))) <=> ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom)))))),
% 1.02/1.24 inference(bind,[status(th)],[])).
% 1.02/1.24 tff(205,plain,
% 1.02/1.24 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom)))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))),
% 1.02/1.24 inference(quant_intro,[status(thm)],[204])).
% 1.02/1.24 tff(206,plain,
% 1.02/1.24 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom)))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))),
% 1.02/1.24 inference(transitivity,[status(thm)],[205, 203])).
% 1.02/1.24 tff(207,plain,
% 1.02/1.24 (^[Morphism: $i, Dom: $i, Cod: $i] : rewrite(((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))))) <=> ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom)))))),
% 1.02/1.24 inference(bind,[status(th)],[])).
% 1.02/1.24 tff(208,plain,
% 1.02/1.24 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))),
% 1.02/1.24 inference(quant_intro,[status(thm)],[207])).
% 1.02/1.24 tff(209,plain,
% 1.02/1.24 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2)))))),
% 1.02/1.24 inference(rewrite,[status(thm)],[])).
% 1.02/1.24 tff(210,plain,
% 1.02/1.24 (^[Morphism: $i, Dom: $i, Cod: $i] : trans(monotonicity(quant_intro(proof_bind(^[El1: $i, El2: $i] : rewrite(((element(El1, Dom) & element(El2, Dom)) => (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2)))) <=> ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2)))))), (![El1: $i, El2: $i] : ((element(El1, Dom) & element(El2, Dom)) => (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2)))) <=> ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2)))))), ((morphism(Morphism, Dom, Cod) => ![El1: $i, El2: $i] : ((element(El1, Dom) & element(El2, Dom)) => (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))))) <=> (morphism(Morphism, Dom, Cod) => ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))))))), rewrite((morphism(Morphism, Dom, Cod) => ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))))) <=> ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2)))))), ((morphism(Morphism, Dom, Cod) => ![El1: $i, El2: $i] : ((element(El1, Dom) & element(El2, Dom)) => (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))))) <=> ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2)))))))),
% 1.02/1.24 inference(bind,[status(th)],[])).
% 1.02/1.24 tff(211,plain,
% 1.02/1.24 (![Morphism: $i, Dom: $i, Cod: $i] : (morphism(Morphism, Dom, Cod) => ![El1: $i, El2: $i] : ((element(El1, Dom) & element(El2, Dom)) => (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2)))))),
% 1.02/1.24 inference(quant_intro,[status(thm)],[210])).
% 1.02/1.24 tff(212,axiom,(![Morphism: $i, Dom: $i, Cod: $i] : (morphism(Morphism, Dom, Cod) => ![El1: $i, El2: $i] : ((element(El1, Dom) & element(El2, Dom)) => (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2)))))), file('/export/starexec/sandbox/benchmark/Axioms/HAL001+0.ax','subtract_distribution')).
% 1.02/1.24 tff(213,plain,
% 1.02/1.24 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2)))))),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[212, 211])).
% 1.02/1.24 tff(214,plain,
% 1.02/1.24 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2)))))),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[213, 209])).
% 1.02/1.24 tff(215,plain,(
% 1.02/1.24 ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((~(element(El1, Dom) & element(El2, Dom))) | (apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2)))))),
% 1.02/1.24 inference(skolemize,[status(sab)],[214])).
% 1.02/1.24 tff(216,plain,
% 1.02/1.24 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[215, 208])).
% 1.02/1.24 tff(217,plain,
% 1.02/1.24 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[216, 206])).
% 1.02/1.24 tff(218,plain,
% 1.02/1.24 (((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))) | ((~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1))))) <=> ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))) | (~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1))))),
% 1.02/1.24 inference(rewrite,[status(thm)],[])).
% 1.02/1.24 tff(219,plain,
% 1.02/1.24 (((~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)) | (~element(El2, any1)))) <=> ((~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1))))),
% 1.02/1.24 inference(rewrite,[status(thm)],[])).
% 1.02/1.24 tff(220,plain,
% 1.02/1.24 (((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))) | ((~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)) | (~element(El2, any1))))) <=> ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))) | ((~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)))))),
% 1.02/1.24 inference(monotonicity,[status(thm)],[219])).
% 1.02/1.24 tff(221,plain,
% 1.02/1.24 (((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))) | ((~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)) | (~element(El2, any1))))) <=> ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))) | (~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1))))),
% 1.02/1.24 inference(transitivity,[status(thm)],[220, 218])).
% 1.02/1.24 tff(222,plain,
% 1.02/1.24 ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))) | ((~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)) | (~element(El2, any1))))),
% 1.02/1.24 inference(quant_inst,[status(thm)],[])).
% 1.02/1.24 tff(223,plain,
% 1.02/1.24 ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | ![El1: $i, El2: $i] : ((apply(Morphism, subtract(Dom, El1, El2)) = subtract(Cod, apply(Morphism, El1), apply(Morphism, El2))) | (~element(El1, Dom)) | (~element(El2, Dom))))) | (~morphism(x, any1, any2)) | ![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)))),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[222, 221])).
% 1.02/1.24 tff(224,plain,
% 1.02/1.24 (![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)))),
% 1.02/1.24 inference(unit_resolution,[status(thm)],[223, 217, 3])).
% 1.02/1.24 tff(225,plain,
% 1.02/1.24 (((~![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)))) | ((~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = subtract(any2, apply(x, tptp_fun_El1_1(any1, x)), apply(x, tptp_fun_El2_0(any1, x)))))) <=> ((~![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = subtract(any2, apply(x, tptp_fun_El1_1(any1, x)), apply(x, tptp_fun_El2_0(any1, x)))))),
% 1.02/1.24 inference(rewrite,[status(thm)],[])).
% 1.02/1.24 tff(226,plain,
% 1.02/1.24 (((~element(tptp_fun_El2_0(any1, x), any1)) | (apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = subtract(any2, apply(x, tptp_fun_El1_1(any1, x)), apply(x, tptp_fun_El2_0(any1, x)))) | (~element(tptp_fun_El1_1(any1, x), any1))) <=> ((~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = subtract(any2, apply(x, tptp_fun_El1_1(any1, x)), apply(x, tptp_fun_El2_0(any1, x)))))),
% 1.02/1.24 inference(rewrite,[status(thm)],[])).
% 1.02/1.24 tff(227,plain,
% 1.02/1.24 (((~![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)))) | ((~element(tptp_fun_El2_0(any1, x), any1)) | (apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = subtract(any2, apply(x, tptp_fun_El1_1(any1, x)), apply(x, tptp_fun_El2_0(any1, x)))) | (~element(tptp_fun_El1_1(any1, x), any1)))) <=> ((~![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)))) | ((~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = subtract(any2, apply(x, tptp_fun_El1_1(any1, x)), apply(x, tptp_fun_El2_0(any1, x))))))),
% 1.02/1.24 inference(monotonicity,[status(thm)],[226])).
% 1.02/1.24 tff(228,plain,
% 1.02/1.24 (((~![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)))) | ((~element(tptp_fun_El2_0(any1, x), any1)) | (apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = subtract(any2, apply(x, tptp_fun_El1_1(any1, x)), apply(x, tptp_fun_El2_0(any1, x)))) | (~element(tptp_fun_El1_1(any1, x), any1)))) <=> ((~![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = subtract(any2, apply(x, tptp_fun_El1_1(any1, x)), apply(x, tptp_fun_El2_0(any1, x)))))),
% 1.02/1.24 inference(transitivity,[status(thm)],[227, 225])).
% 1.02/1.24 tff(229,plain,
% 1.02/1.24 ((~![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)))) | ((~element(tptp_fun_El2_0(any1, x), any1)) | (apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = subtract(any2, apply(x, tptp_fun_El1_1(any1, x)), apply(x, tptp_fun_El2_0(any1, x)))) | (~element(tptp_fun_El1_1(any1, x), any1)))),
% 1.02/1.24 inference(quant_inst,[status(thm)],[])).
% 1.02/1.24 tff(230,plain,
% 1.02/1.24 ((~![El1: $i, El2: $i] : ((~element(El2, any1)) | (apply(x, subtract(any1, El1, El2)) = subtract(any2, apply(x, El1), apply(x, El2))) | (~element(El1, any1)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = subtract(any2, apply(x, tptp_fun_El1_1(any1, x)), apply(x, tptp_fun_El2_0(any1, x))))),
% 1.02/1.24 inference(modus_ponens,[status(thm)],[229, 228])).
% 1.02/1.24 tff(231,plain,
% 1.02/1.24 (apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = subtract(any2, apply(x, tptp_fun_El1_1(any1, x)), apply(x, tptp_fun_El2_0(any1, x)))),
% 1.02/1.24 inference(unit_resolution,[status(thm)],[230, 224, 168, 166])).
% 1.02/1.24 tff(232,plain,
% 1.02/1.24 (apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = zero(any2)),
% 1.02/1.24 inference(transitivity,[status(thm)],[231, 201, 198])).
% 1.02/1.24 tff(233,plain,
% 1.02/1.24 (((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1))) <=> ((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1))),
% 1.02/1.24 inference(rewrite,[status(thm)],[])).
% 1.02/1.24 tff(234,plain,
% 1.02/1.24 ((element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~element(tptp_fun_El1_1(any1, x), any1))) <=> ((~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1))),
% 1.02/1.25 inference(rewrite,[status(thm)],[])).
% 1.02/1.25 tff(235,plain,
% 1.02/1.25 (((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~element(tptp_fun_El1_1(any1, x), any1)))) <=> ((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1)))),
% 1.02/1.25 inference(monotonicity,[status(thm)],[234])).
% 1.02/1.25 tff(236,plain,
% 1.02/1.25 (((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~element(tptp_fun_El1_1(any1, x), any1)))) <=> ((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1))),
% 1.02/1.25 inference(transitivity,[status(thm)],[235, 233])).
% 1.02/1.25 tff(237,plain,
% 1.02/1.25 ((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~element(tptp_fun_El1_1(any1, x), any1)))),
% 1.02/1.25 inference(quant_inst,[status(thm)],[])).
% 1.02/1.25 tff(238,plain,
% 1.02/1.25 ((~![Dom: $i, El1: $i, El2: $i] : (element(subtract(Dom, El1, El2), Dom) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1)),
% 1.02/1.25 inference(modus_ponens,[status(thm)],[237, 236])).
% 1.02/1.25 tff(239,plain,
% 1.02/1.25 (element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1)),
% 1.02/1.25 inference(unit_resolution,[status(thm)],[238, 84, 168, 166])).
% 1.02/1.25 tff(240,plain,
% 1.02/1.25 (^[Morphism: $i, Dom: $i, Cod: $i] : refl(((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod))))) <=> ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod))))))),
% 1.02/1.25 inference(bind,[status(th)],[])).
% 1.02/1.25 tff(241,plain,
% 1.02/1.25 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))),
% 1.02/1.25 inference(quant_intro,[status(thm)],[240])).
% 1.02/1.25 tff(242,plain,
% 1.02/1.25 (^[Morphism: $i, Dom: $i, Cod: $i] : rewrite(((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod))))) <=> ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod))))))),
% 1.02/1.25 inference(bind,[status(th)],[])).
% 1.02/1.25 tff(243,plain,
% 1.02/1.25 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))),
% 1.02/1.25 inference(quant_intro,[status(thm)],[242])).
% 1.02/1.25 tff(244,plain,
% 1.02/1.25 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod))))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))),
% 1.02/1.25 inference(transitivity,[status(thm)],[243, 241])).
% 1.02/1.25 tff(245,plain,
% 1.02/1.25 (^[Morphism: $i, Dom: $i, Cod: $i] : trans(monotonicity(trans(monotonicity(rewrite((injection_2(Morphism) & morphism(Morphism, Dom, Cod)) <=> (~((~injection_2(Morphism)) | (~morphism(Morphism, Dom, Cod))))), ((~(injection_2(Morphism) & morphism(Morphism, Dom, Cod))) <=> (~(~((~injection_2(Morphism)) | (~morphism(Morphism, Dom, Cod))))))), rewrite((~(~((~injection_2(Morphism)) | (~morphism(Morphism, Dom, Cod))))) <=> ((~injection_2(Morphism)) | (~morphism(Morphism, Dom, Cod)))), ((~(injection_2(Morphism) & morphism(Morphism, Dom, Cod))) <=> ((~injection_2(Morphism)) | (~morphism(Morphism, Dom, Cod))))), quant_intro(proof_bind(^[El: $i] : trans(monotonicity(trans(monotonicity(rewrite((element(El, Dom) & (apply(Morphism, El) = zero(Cod))) <=> (~((~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))), ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) <=> (~(~((~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))))), rewrite((~(~((~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))) <=> ((~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod))))), ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) <=> ((~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))), (((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))) <=> (((~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))), rewrite((((~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))) <=> ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod))))), (((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))) <=> ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod))))))), (![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))) <=> ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))), (((~(injection_2(Morphism) & morphism(Morphism, Dom, Cod))) | ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom)))) <=> (((~injection_2(Morphism)) | (~morphism(Morphism, Dom, Cod))) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod))))))), rewrite((((~injection_2(Morphism)) | (~morphism(Morphism, Dom, Cod))) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod))))) <=> ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))), (((~(injection_2(Morphism) & morphism(Morphism, Dom, Cod))) | ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom)))) <=> ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))))),
% 1.02/1.25 inference(bind,[status(th)],[])).
% 1.02/1.25 tff(246,plain,
% 1.02/1.25 (![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection_2(Morphism) & morphism(Morphism, Dom, Cod))) | ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom)))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))),
% 1.02/1.25 inference(quant_intro,[status(thm)],[245])).
% 1.02/1.25 tff(247,plain,
% 1.02/1.25 (![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection_2(Morphism) & morphism(Morphism, Dom, Cod))) | ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom)))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection_2(Morphism) & morphism(Morphism, Dom, Cod))) | ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))),
% 1.02/1.25 inference(rewrite,[status(thm)],[])).
% 1.02/1.25 tff(248,plain,
% 1.02/1.25 (^[Morphism: $i, Dom: $i, Cod: $i] : trans(monotonicity(quant_intro(proof_bind(^[El: $i] : rewrite(((element(El, Dom) & (apply(Morphism, El) = zero(Cod))) => (El = zero(Dom))) <=> ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))), (![El: $i] : ((element(El, Dom) & (apply(Morphism, El) = zero(Cod))) => (El = zero(Dom))) <=> ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))), (((injection_2(Morphism) & morphism(Morphism, Dom, Cod)) => ![El: $i] : ((element(El, Dom) & (apply(Morphism, El) = zero(Cod))) => (El = zero(Dom)))) <=> ((injection_2(Morphism) & morphism(Morphism, Dom, Cod)) => ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom)))))), rewrite(((injection_2(Morphism) & morphism(Morphism, Dom, Cod)) => ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom)))) <=> ((~(injection_2(Morphism) & morphism(Morphism, Dom, Cod))) | ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))), (((injection_2(Morphism) & morphism(Morphism, Dom, Cod)) => ![El: $i] : ((element(El, Dom) & (apply(Morphism, El) = zero(Cod))) => (El = zero(Dom)))) <=> ((~(injection_2(Morphism) & morphism(Morphism, Dom, Cod))) | ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))))),
% 1.02/1.25 inference(bind,[status(th)],[])).
% 1.02/1.25 tff(249,plain,
% 1.02/1.25 (![Morphism: $i, Dom: $i, Cod: $i] : ((injection_2(Morphism) & morphism(Morphism, Dom, Cod)) => ![El: $i] : ((element(El, Dom) & (apply(Morphism, El) = zero(Cod))) => (El = zero(Dom)))) <=> ![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection_2(Morphism) & morphism(Morphism, Dom, Cod))) | ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))),
% 1.02/1.25 inference(quant_intro,[status(thm)],[248])).
% 1.02/1.25 tff(250,axiom,(![Morphism: $i, Dom: $i, Cod: $i] : ((injection_2(Morphism) & morphism(Morphism, Dom, Cod)) => ![El: $i] : ((element(El, Dom) & (apply(Morphism, El) = zero(Cod))) => (El = zero(Dom))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','injection_properties_2')).
% 1.02/1.25 tff(251,plain,
% 1.02/1.25 (![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection_2(Morphism) & morphism(Morphism, Dom, Cod))) | ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))),
% 1.02/1.25 inference(modus_ponens,[status(thm)],[250, 249])).
% 1.02/1.25 tff(252,plain,
% 1.02/1.25 (![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection_2(Morphism) & morphism(Morphism, Dom, Cod))) | ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))),
% 1.02/1.25 inference(modus_ponens,[status(thm)],[251, 247])).
% 1.02/1.25 tff(253,plain,(
% 1.02/1.25 ![Morphism: $i, Dom: $i, Cod: $i] : ((~(injection_2(Morphism) & morphism(Morphism, Dom, Cod))) | ![El: $i] : ((~(element(El, Dom) & (apply(Morphism, El) = zero(Cod)))) | (El = zero(Dom))))),
% 1.02/1.25 inference(skolemize,[status(sab)],[252])).
% 1.02/1.25 tff(254,plain,
% 1.02/1.25 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))),
% 1.02/1.25 inference(modus_ponens,[status(thm)],[253, 246])).
% 1.02/1.25 tff(255,plain,
% 1.02/1.25 (![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))),
% 1.02/1.25 inference(modus_ponens,[status(thm)],[254, 244])).
% 1.02/1.25 tff(256,plain,
% 1.02/1.25 (((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))) | ((~injection_2(x)) | (~morphism(x, any1, any2)) | ![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2)))))) <=> ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))) | (~injection_2(x)) | (~morphism(x, any1, any2)) | ![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2)))))),
% 1.02/1.25 inference(rewrite,[status(thm)],[])).
% 1.02/1.25 tff(257,plain,
% 1.02/1.25 (((~morphism(x, any1, any2)) | (~injection_2(x)) | ![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2))))) <=> ((~injection_2(x)) | (~morphism(x, any1, any2)) | ![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2)))))),
% 1.02/1.25 inference(rewrite,[status(thm)],[])).
% 1.02/1.25 tff(258,plain,
% 1.02/1.25 (((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))) | ((~morphism(x, any1, any2)) | (~injection_2(x)) | ![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2)))))) <=> ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))) | ((~injection_2(x)) | (~morphism(x, any1, any2)) | ![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2))))))),
% 1.02/1.25 inference(monotonicity,[status(thm)],[257])).
% 1.02/1.25 tff(259,plain,
% 1.02/1.25 (((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))) | ((~morphism(x, any1, any2)) | (~injection_2(x)) | ![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2)))))) <=> ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))) | (~injection_2(x)) | (~morphism(x, any1, any2)) | ![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2)))))),
% 1.02/1.25 inference(transitivity,[status(thm)],[258, 256])).
% 1.02/1.25 tff(260,plain,
% 1.02/1.25 ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))) | ((~morphism(x, any1, any2)) | (~injection_2(x)) | ![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2)))))),
% 1.02/1.25 inference(quant_inst,[status(thm)],[])).
% 1.02/1.25 tff(261,plain,
% 1.02/1.25 ((~![Morphism: $i, Dom: $i, Cod: $i] : ((~morphism(Morphism, Dom, Cod)) | (~injection_2(Morphism)) | ![El: $i] : ((El = zero(Dom)) | (~element(El, Dom)) | (~(apply(Morphism, El) = zero(Cod)))))) | (~injection_2(x)) | (~morphism(x, any1, any2)) | ![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2))))),
% 1.02/1.25 inference(modus_ponens,[status(thm)],[260, 259])).
% 1.02/1.25 tff(262,plain,
% 1.02/1.25 ((~injection_2(x)) | ![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2))))),
% 1.02/1.25 inference(unit_resolution,[status(thm)],[261, 255, 3])).
% 1.02/1.25 tff(263,plain,
% 1.02/1.25 (![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2))))),
% 1.02/1.25 inference(unit_resolution,[status(thm)],[262, 140])).
% 1.02/1.25 tff(264,plain,
% 1.02/1.25 (((~![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2))))) | ((subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)) = zero(any1)) | (~element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1)) | (~(apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = zero(any2))))) <=> ((~![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2))))) | (subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)) = zero(any1)) | (~element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1)) | (~(apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = zero(any2))))),
% 1.02/1.25 inference(rewrite,[status(thm)],[])).
% 1.02/1.25 tff(265,plain,
% 1.02/1.25 ((~![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2))))) | ((subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)) = zero(any1)) | (~element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1)) | (~(apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = zero(any2))))),
% 1.02/1.25 inference(quant_inst,[status(thm)],[])).
% 1.02/1.25 tff(266,plain,
% 1.02/1.25 ((~![El: $i] : ((El = zero(any1)) | (~element(El, any1)) | (~(apply(x, El) = zero(any2))))) | (subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)) = zero(any1)) | (~element(subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)), any1)) | (~(apply(x, subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))) = zero(any2)))),
% 1.02/1.25 inference(modus_ponens,[status(thm)],[265, 264])).
% 1.02/1.25 tff(267,plain,
% 1.02/1.25 (subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)) = zero(any1)),
% 1.02/1.25 inference(unit_resolution,[status(thm)],[266, 263, 239, 232])).
% 1.02/1.25 tff(268,plain,
% 1.02/1.25 (zero(any1) = subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))),
% 1.02/1.25 inference(symmetry,[status(thm)],[267])).
% 1.02/1.25 tff(269,plain,
% 1.02/1.25 (((~![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))) | ((~element(tptp_fun_El1_1(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x)) = zero(any1)))) <=> ((~![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x)) = zero(any1)))),
% 1.02/1.25 inference(rewrite,[status(thm)],[])).
% 1.02/1.25 tff(270,plain,
% 1.02/1.25 ((~![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))) | ((~element(tptp_fun_El1_1(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x)) = zero(any1)))),
% 1.02/1.25 inference(quant_inst,[status(thm)],[])).
% 1.02/1.25 tff(271,plain,
% 1.02/1.25 ((~![Dom: $i, El: $i] : ((~element(El, Dom)) | (subtract(Dom, El, El) = zero(Dom)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x)) = zero(any1))),
% 1.02/1.25 inference(modus_ponens,[status(thm)],[270, 269])).
% 1.02/1.25 tff(272,plain,
% 1.02/1.25 (subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x)) = zero(any1)),
% 1.02/1.25 inference(unit_resolution,[status(thm)],[271, 66, 168])).
% 1.02/1.25 tff(273,plain,
% 1.02/1.25 (subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x)) = subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x))),
% 1.02/1.25 inference(transitivity,[status(thm)],[272, 268])).
% 1.02/1.25 tff(274,plain,
% 1.02/1.25 (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x))) = subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El2_0(any1, x)))),
% 1.02/1.25 inference(monotonicity,[status(thm)],[273])).
% 1.02/1.25 tff(275,plain,
% 1.02/1.25 (((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((~element(tptp_fun_El1_1(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x))) = tptp_fun_El1_1(any1, x)))) <=> ((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x))) = tptp_fun_El1_1(any1, x)))),
% 1.02/1.25 inference(rewrite,[status(thm)],[])).
% 1.02/1.25 tff(276,plain,
% 1.02/1.25 (((subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x))) = tptp_fun_El1_1(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El1_1(any1, x), any1))) <=> ((~element(tptp_fun_El1_1(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x))) = tptp_fun_El1_1(any1, x)))),
% 1.02/1.25 inference(rewrite,[status(thm)],[])).
% 1.02/1.25 tff(277,plain,
% 1.02/1.25 (((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x))) = tptp_fun_El1_1(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El1_1(any1, x), any1)))) <=> ((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((~element(tptp_fun_El1_1(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x))) = tptp_fun_El1_1(any1, x))))),
% 1.02/1.25 inference(monotonicity,[status(thm)],[276])).
% 1.02/1.25 tff(278,plain,
% 1.02/1.25 (((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x))) = tptp_fun_El1_1(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El1_1(any1, x), any1)))) <=> ((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x))) = tptp_fun_El1_1(any1, x)))),
% 1.02/1.25 inference(transitivity,[status(thm)],[277, 275])).
% 1.02/1.25 tff(279,plain,
% 1.02/1.25 ((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | ((subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x))) = tptp_fun_El1_1(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El1_1(any1, x), any1)))),
% 1.02/1.25 inference(quant_inst,[status(thm)],[])).
% 1.02/1.25 tff(280,plain,
% 1.02/1.25 ((~![Dom: $i, El1: $i, El2: $i] : ((subtract(Dom, El1, subtract(Dom, El1, El2)) = El2) | (~element(El2, Dom)) | (~element(El1, Dom)))) | (~element(tptp_fun_El1_1(any1, x), any1)) | (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x))) = tptp_fun_El1_1(any1, x))),
% 1.02/1.25 inference(modus_ponens,[status(thm)],[279, 278])).
% 1.02/1.25 tff(281,plain,
% 1.02/1.25 (subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x))) = tptp_fun_El1_1(any1, x)),
% 1.02/1.25 inference(unit_resolution,[status(thm)],[280, 181, 168])).
% 1.02/1.25 tff(282,plain,
% 1.02/1.25 (tptp_fun_El1_1(any1, x) = subtract(any1, tptp_fun_El1_1(any1, x), subtract(any1, tptp_fun_El1_1(any1, x), tptp_fun_El1_1(any1, x)))),
% 1.02/1.25 inference(symmetry,[status(thm)],[281])).
% 1.02/1.25 tff(283,plain,
% 1.02/1.25 (tptp_fun_El1_1(any1, x) = tptp_fun_El2_0(any1, x)),
% 1.02/1.25 inference(transitivity,[status(thm)],[282, 274, 188])).
% 1.02/1.25 tff(284,plain,
% 1.02/1.25 (((tptp_fun_El1_1(any1, x) = tptp_fun_El2_0(any1, x)) | (~element(tptp_fun_El1_1(any1, x), any1)) | (~element(tptp_fun_El2_0(any1, x), any1)) | (~(apply(x, tptp_fun_El1_1(any1, x)) = apply(x, tptp_fun_El2_0(any1, x))))) | (~(tptp_fun_El1_1(any1, x) = tptp_fun_El2_0(any1, x)))),
% 1.02/1.25 inference(tautology,[status(thm)],[])).
% 1.02/1.25 tff(285,plain,
% 1.02/1.25 (~(tptp_fun_El1_1(any1, x) = tptp_fun_El2_0(any1, x))),
% 1.02/1.25 inference(unit_resolution,[status(thm)],[284, 164])).
% 1.02/1.25 tff(286,plain,
% 1.02/1.25 ($false),
% 1.02/1.25 inference(unit_resolution,[status(thm)],[285, 283])).
% 1.02/1.25 % SZS output end Proof
% 1.02/1.25 % E exiting
%------------------------------------------------------------------------------