%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : KLE135+1 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n008.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:13:04 AM UTC 2025
% Result : Theorem 4.47s 4.63s
% Output : Proof 4.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : KLE135+1 : TPTP v9.0.0. Released v4.0.0.
% 0.13/0.14 % Command : run_E %s %d THM
% 0.13/0.35 % Computer : n008.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu Jun 19 19:03:03 EDT 2025
% 0.13/0.36 % CPUTime :
% 4.47/4.63 % SZS status Theorem
% 4.47/4.63 % SZS output start Proof
% 4.47/4.63 tff(addition_type, type, (
% 4.47/4.63 addition: ( $i * $i ) > $i)).
% 4.47/4.63 tff(domain_type, type, (
% 4.47/4.63 domain: $i > $i)).
% 4.47/4.63 tff(antidomain_type, type, (
% 4.47/4.63 antidomain: $i > $i)).
% 4.47/4.63 tff(tptp_fun_X0_0_type, type, (
% 4.47/4.63 tptp_fun_X0_0: $i)).
% 4.47/4.63 tff(forward_diamond_type, type, (
% 4.47/4.63 forward_diamond: ( $i * $i ) > $i)).
% 4.47/4.63 tff(one_type, type, (
% 4.47/4.63 one: $i)).
% 4.47/4.63 tff(multiplication_type, type, (
% 4.47/4.63 multiplication: ( $i * $i ) > $i)).
% 4.47/4.63 tff(zero_type, type, (
% 4.47/4.63 zero: $i)).
% 4.47/4.63 tff(divergence_type, type, (
% 4.47/4.63 divergence: $i > $i)).
% 4.47/4.63 tff(star_type, type, (
% 4.47/4.63 star: $i > $i)).
% 4.47/4.63 tff(1,plain,
% 4.47/4.63 (^[A: $i] : refl((multiplication(one, A) = A) <=> (multiplication(one, A) = A))),
% 4.47/4.63 inference(bind,[status(th)],[])).
% 4.47/4.63 tff(2,plain,
% 4.47/4.63 (![A: $i] : (multiplication(one, A) = A) <=> ![A: $i] : (multiplication(one, A) = A)),
% 4.47/4.63 inference(quant_intro,[status(thm)],[1])).
% 4.47/4.63 tff(3,plain,
% 4.47/4.63 (![A: $i] : (multiplication(one, A) = A) <=> ![A: $i] : (multiplication(one, A) = A)),
% 4.47/4.63 inference(rewrite,[status(thm)],[])).
% 4.47/4.63 tff(4,axiom,(![A: $i] : (multiplication(one, A) = A)), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax','multiplicative_left_identity')).
% 4.47/4.63 tff(5,plain,
% 4.47/4.63 (![A: $i] : (multiplication(one, A) = A)),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[4, 3])).
% 4.47/4.63 tff(6,plain,(
% 4.47/4.63 ![A: $i] : (multiplication(one, A) = A)),
% 4.47/4.63 inference(skolemize,[status(sab)],[5])).
% 4.47/4.63 tff(7,plain,
% 4.47/4.63 (![A: $i] : (multiplication(one, A) = A)),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[6, 2])).
% 4.47/4.63 tff(8,plain,
% 4.47/4.63 ((~![A: $i] : (multiplication(one, A) = A)) | (multiplication(one, antidomain(antidomain(X0!0))) = antidomain(antidomain(X0!0)))),
% 4.47/4.63 inference(quant_inst,[status(thm)],[])).
% 4.47/4.63 tff(9,plain,
% 4.47/4.63 (multiplication(one, antidomain(antidomain(X0!0))) = antidomain(antidomain(X0!0))),
% 4.47/4.63 inference(unit_resolution,[status(thm)],[8, 7])).
% 4.47/4.63 tff(10,plain,
% 4.47/4.63 (^[A: $i] : refl((addition(A, zero) = A) <=> (addition(A, zero) = A))),
% 4.47/4.63 inference(bind,[status(th)],[])).
% 4.47/4.63 tff(11,plain,
% 4.47/4.63 (![A: $i] : (addition(A, zero) = A) <=> ![A: $i] : (addition(A, zero) = A)),
% 4.47/4.63 inference(quant_intro,[status(thm)],[10])).
% 4.47/4.63 tff(12,plain,
% 4.47/4.63 (![A: $i] : (addition(A, zero) = A) <=> ![A: $i] : (addition(A, zero) = A)),
% 4.47/4.63 inference(rewrite,[status(thm)],[])).
% 4.47/4.63 tff(13,axiom,(![A: $i] : (addition(A, zero) = A)), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax','additive_identity')).
% 4.47/4.63 tff(14,plain,
% 4.47/4.63 (![A: $i] : (addition(A, zero) = A)),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[13, 12])).
% 4.47/4.63 tff(15,plain,(
% 4.47/4.63 ![A: $i] : (addition(A, zero) = A)),
% 4.47/4.63 inference(skolemize,[status(sab)],[14])).
% 4.47/4.63 tff(16,plain,
% 4.47/4.63 (![A: $i] : (addition(A, zero) = A)),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[15, 11])).
% 4.47/4.63 tff(17,plain,
% 4.47/4.63 ((~![A: $i] : (addition(A, zero) = A)) | (addition(antidomain(domain(multiplication(X0!0, domain(zero)))), zero) = antidomain(domain(multiplication(X0!0, domain(zero)))))),
% 4.47/4.63 inference(quant_inst,[status(thm)],[])).
% 4.47/4.63 tff(18,plain,
% 4.47/4.63 (addition(antidomain(domain(multiplication(X0!0, domain(zero)))), zero) = antidomain(domain(multiplication(X0!0, domain(zero))))),
% 4.47/4.63 inference(unit_resolution,[status(thm)],[17, 16])).
% 4.47/4.63 tff(19,plain,
% 4.47/4.63 (^[X0: $i] : refl((domain(X0) = antidomain(antidomain(X0))) <=> (domain(X0) = antidomain(antidomain(X0))))),
% 4.47/4.63 inference(bind,[status(th)],[])).
% 4.47/4.63 tff(20,plain,
% 4.47/4.63 (![X0: $i] : (domain(X0) = antidomain(antidomain(X0))) <=> ![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))),
% 4.47/4.63 inference(quant_intro,[status(thm)],[19])).
% 4.47/4.63 tff(21,plain,
% 4.47/4.63 (![X0: $i] : (domain(X0) = antidomain(antidomain(X0))) <=> ![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))),
% 4.47/4.63 inference(rewrite,[status(thm)],[])).
% 4.47/4.63 tff(22,axiom,(![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax','domain4')).
% 4.47/4.63 tff(23,plain,
% 4.47/4.63 (![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[22, 21])).
% 4.47/4.63 tff(24,plain,(
% 4.47/4.63 ![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))),
% 4.47/4.63 inference(skolemize,[status(sab)],[23])).
% 4.47/4.63 tff(25,plain,
% 4.47/4.63 (![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[24, 20])).
% 4.47/4.63 tff(26,plain,
% 4.47/4.63 ((~![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))) | (domain(multiplication(X0!0, domain(zero))) = antidomain(antidomain(multiplication(X0!0, domain(zero)))))),
% 4.47/4.63 inference(quant_inst,[status(thm)],[])).
% 4.47/4.63 tff(27,plain,
% 4.47/4.63 (domain(multiplication(X0!0, domain(zero))) = antidomain(antidomain(multiplication(X0!0, domain(zero))))),
% 4.47/4.63 inference(unit_resolution,[status(thm)],[26, 25])).
% 4.47/4.63 tff(28,plain,
% 4.47/4.63 (^[X0: $i, X1: $i] : refl((forward_diamond(X0, X1) = domain(multiplication(X0, domain(X1)))) <=> (forward_diamond(X0, X1) = domain(multiplication(X0, domain(X1)))))),
% 4.47/4.63 inference(bind,[status(th)],[])).
% 4.47/4.63 tff(29,plain,
% 4.47/4.63 (![X0: $i, X1: $i] : (forward_diamond(X0, X1) = domain(multiplication(X0, domain(X1)))) <=> ![X0: $i, X1: $i] : (forward_diamond(X0, X1) = domain(multiplication(X0, domain(X1))))),
% 4.47/4.63 inference(quant_intro,[status(thm)],[28])).
% 4.47/4.63 tff(30,plain,
% 4.47/4.63 (![X0: $i, X1: $i] : (forward_diamond(X0, X1) = domain(multiplication(X0, domain(X1)))) <=> ![X0: $i, X1: $i] : (forward_diamond(X0, X1) = domain(multiplication(X0, domain(X1))))),
% 4.47/4.63 inference(rewrite,[status(thm)],[])).
% 4.47/4.63 tff(31,axiom,(![X0: $i, X1: $i] : (forward_diamond(X0, X1) = domain(multiplication(X0, domain(X1))))), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+6.ax','forward_diamond')).
% 4.47/4.63 tff(32,plain,
% 4.47/4.63 (![X0: $i, X1: $i] : (forward_diamond(X0, X1) = domain(multiplication(X0, domain(X1))))),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[31, 30])).
% 4.47/4.63 tff(33,plain,(
% 4.47/4.63 ![X0: $i, X1: $i] : (forward_diamond(X0, X1) = domain(multiplication(X0, domain(X1))))),
% 4.47/4.63 inference(skolemize,[status(sab)],[32])).
% 4.47/4.63 tff(34,plain,
% 4.47/4.63 (![X0: $i, X1: $i] : (forward_diamond(X0, X1) = domain(multiplication(X0, domain(X1))))),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[33, 29])).
% 4.47/4.63 tff(35,plain,
% 4.47/4.63 ((~![X0: $i, X1: $i] : (forward_diamond(X0, X1) = domain(multiplication(X0, domain(X1))))) | (forward_diamond(X0!0, zero) = domain(multiplication(X0!0, domain(zero))))),
% 4.47/4.63 inference(quant_inst,[status(thm)],[])).
% 4.47/4.63 tff(36,plain,
% 4.47/4.63 (forward_diamond(X0!0, zero) = domain(multiplication(X0!0, domain(zero)))),
% 4.47/4.63 inference(unit_resolution,[status(thm)],[35, 34])).
% 4.47/4.63 tff(37,plain,
% 4.47/4.63 ((~![X0: $i] : ((~(divergence(X0) = zero)) | (forward_diamond(star(X0), antidomain(X0)) = one))) <=> (~![X0: $i] : ((~(divergence(X0) = zero)) | (forward_diamond(star(X0), antidomain(X0)) = one)))),
% 4.47/4.63 inference(rewrite,[status(thm)],[])).
% 4.47/4.63 tff(38,plain,
% 4.47/4.63 ((~![X0: $i] : ((divergence(X0) = zero) => (forward_diamond(star(X0), antidomain(X0)) = one))) <=> (~![X0: $i] : ((~(divergence(X0) = zero)) | (forward_diamond(star(X0), antidomain(X0)) = one)))),
% 4.47/4.63 inference(rewrite,[status(thm)],[])).
% 4.47/4.63 tff(39,axiom,(~![X0: $i] : ((divergence(X0) = zero) => (forward_diamond(star(X0), antidomain(X0)) = one))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','goals')).
% 4.47/4.63 tff(40,plain,
% 4.47/4.63 (~![X0: $i] : ((~(divergence(X0) = zero)) | (forward_diamond(star(X0), antidomain(X0)) = one))),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[39, 38])).
% 4.47/4.63 tff(41,plain,
% 4.47/4.63 (~![X0: $i] : ((~(divergence(X0) = zero)) | (forward_diamond(star(X0), antidomain(X0)) = one))),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[40, 37])).
% 4.47/4.63 tff(42,plain,
% 4.47/4.63 (~![X0: $i] : ((~(divergence(X0) = zero)) | (forward_diamond(star(X0), antidomain(X0)) = one))),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[41, 37])).
% 4.47/4.63 tff(43,plain,
% 4.47/4.63 (~![X0: $i] : ((~(divergence(X0) = zero)) | (forward_diamond(star(X0), antidomain(X0)) = one))),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[42, 37])).
% 4.47/4.63 tff(44,plain,(
% 4.47/4.63 ~((~(divergence(X0!0) = zero)) | (forward_diamond(star(X0!0), antidomain(X0!0)) = one))),
% 4.47/4.63 inference(skolemize,[status(sab)],[43])).
% 4.47/4.63 tff(45,plain,
% 4.47/4.63 (divergence(X0!0) = zero),
% 4.47/4.63 inference(or_elim,[status(thm)],[44])).
% 4.47/4.63 tff(46,plain,
% 4.47/4.63 (zero = divergence(X0!0)),
% 4.47/4.63 inference(symmetry,[status(thm)],[45])).
% 4.47/4.63 tff(47,plain,
% 4.47/4.63 (forward_diamond(X0!0, zero) = forward_diamond(X0!0, divergence(X0!0))),
% 4.47/4.63 inference(monotonicity,[status(thm)],[46])).
% 4.47/4.63 tff(48,plain,
% 4.47/4.63 (forward_diamond(X0!0, divergence(X0!0)) = forward_diamond(X0!0, zero)),
% 4.47/4.63 inference(symmetry,[status(thm)],[47])).
% 4.47/4.63 tff(49,plain,
% 4.47/4.63 (^[X0: $i] : refl((forward_diamond(X0, divergence(X0)) = divergence(X0)) <=> (forward_diamond(X0, divergence(X0)) = divergence(X0)))),
% 4.47/4.63 inference(bind,[status(th)],[])).
% 4.47/4.63 tff(50,plain,
% 4.47/4.63 (![X0: $i] : (forward_diamond(X0, divergence(X0)) = divergence(X0)) <=> ![X0: $i] : (forward_diamond(X0, divergence(X0)) = divergence(X0))),
% 4.47/4.63 inference(quant_intro,[status(thm)],[49])).
% 4.47/4.63 tff(51,plain,
% 4.47/4.63 (![X0: $i] : (forward_diamond(X0, divergence(X0)) = divergence(X0)) <=> ![X0: $i] : (forward_diamond(X0, divergence(X0)) = divergence(X0))),
% 4.47/4.63 inference(rewrite,[status(thm)],[])).
% 4.47/4.63 tff(52,axiom,(![X0: $i] : (forward_diamond(X0, divergence(X0)) = divergence(X0))), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+7.ax','divergence1')).
% 4.47/4.63 tff(53,plain,
% 4.47/4.63 (![X0: $i] : (forward_diamond(X0, divergence(X0)) = divergence(X0))),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[52, 51])).
% 4.47/4.63 tff(54,plain,(
% 4.47/4.63 ![X0: $i] : (forward_diamond(X0, divergence(X0)) = divergence(X0))),
% 4.47/4.63 inference(skolemize,[status(sab)],[53])).
% 4.47/4.63 tff(55,plain,
% 4.47/4.63 (![X0: $i] : (forward_diamond(X0, divergence(X0)) = divergence(X0))),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[54, 50])).
% 4.47/4.63 tff(56,plain,
% 4.47/4.63 ((~![X0: $i] : (forward_diamond(X0, divergence(X0)) = divergence(X0))) | (forward_diamond(X0!0, divergence(X0!0)) = divergence(X0!0))),
% 4.47/4.63 inference(quant_inst,[status(thm)],[])).
% 4.47/4.63 tff(57,plain,
% 4.47/4.63 (forward_diamond(X0!0, divergence(X0!0)) = divergence(X0!0)),
% 4.47/4.63 inference(unit_resolution,[status(thm)],[56, 55])).
% 4.47/4.63 tff(58,plain,
% 4.47/4.63 (divergence(X0!0) = forward_diamond(X0!0, divergence(X0!0))),
% 4.47/4.63 inference(symmetry,[status(thm)],[57])).
% 4.47/4.63 tff(59,plain,
% 4.47/4.63 (zero = antidomain(antidomain(multiplication(X0!0, domain(zero))))),
% 4.47/4.63 inference(transitivity,[status(thm)],[46, 58, 48, 36, 27])).
% 4.47/4.63 tff(60,plain,
% 4.47/4.63 (antidomain(antidomain(multiplication(X0!0, domain(zero)))) = domain(multiplication(X0!0, domain(zero)))),
% 4.47/4.63 inference(symmetry,[status(thm)],[27])).
% 4.47/4.63 tff(61,plain,
% 4.47/4.63 (antidomain(antidomain(antidomain(multiplication(X0!0, domain(zero))))) = antidomain(domain(multiplication(X0!0, domain(zero))))),
% 4.47/4.63 inference(monotonicity,[status(thm)],[60])).
% 4.47/4.63 tff(62,plain,
% 4.47/4.63 (antidomain(domain(multiplication(X0!0, domain(zero)))) = antidomain(antidomain(antidomain(multiplication(X0!0, domain(zero)))))),
% 4.47/4.63 inference(symmetry,[status(thm)],[61])).
% 4.47/4.63 tff(63,plain,
% 4.47/4.63 (addition(antidomain(domain(multiplication(X0!0, domain(zero)))), zero) = addition(antidomain(antidomain(antidomain(multiplication(X0!0, domain(zero))))), antidomain(antidomain(multiplication(X0!0, domain(zero)))))),
% 4.47/4.63 inference(monotonicity,[status(thm)],[62, 59])).
% 4.47/4.63 tff(64,plain,
% 4.47/4.63 (addition(antidomain(antidomain(antidomain(multiplication(X0!0, domain(zero))))), antidomain(antidomain(multiplication(X0!0, domain(zero))))) = addition(antidomain(domain(multiplication(X0!0, domain(zero)))), zero)),
% 4.47/4.63 inference(symmetry,[status(thm)],[63])).
% 4.47/4.63 tff(65,plain,
% 4.47/4.63 (^[X0: $i] : refl((addition(antidomain(antidomain(X0)), antidomain(X0)) = one) <=> (addition(antidomain(antidomain(X0)), antidomain(X0)) = one))),
% 4.47/4.63 inference(bind,[status(th)],[])).
% 4.47/4.63 tff(66,plain,
% 4.47/4.63 (![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one) <=> ![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one)),
% 4.47/4.63 inference(quant_intro,[status(thm)],[65])).
% 4.47/4.63 tff(67,plain,
% 4.47/4.63 (![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one) <=> ![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one)),
% 4.47/4.63 inference(rewrite,[status(thm)],[])).
% 4.47/4.63 tff(68,axiom,(![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one)), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax','domain3')).
% 4.47/4.63 tff(69,plain,
% 4.47/4.63 (![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one)),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[68, 67])).
% 4.47/4.63 tff(70,plain,(
% 4.47/4.63 ![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one)),
% 4.47/4.63 inference(skolemize,[status(sab)],[69])).
% 4.47/4.63 tff(71,plain,
% 4.47/4.63 (![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one)),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[70, 66])).
% 4.47/4.63 tff(72,plain,
% 4.47/4.63 ((~![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one)) | (addition(antidomain(antidomain(antidomain(multiplication(X0!0, domain(zero))))), antidomain(antidomain(multiplication(X0!0, domain(zero))))) = one)),
% 4.47/4.63 inference(quant_inst,[status(thm)],[])).
% 4.47/4.63 tff(73,plain,
% 4.47/4.63 (addition(antidomain(antidomain(antidomain(multiplication(X0!0, domain(zero))))), antidomain(antidomain(multiplication(X0!0, domain(zero))))) = one),
% 4.47/4.63 inference(unit_resolution,[status(thm)],[72, 71])).
% 4.47/4.63 tff(74,plain,
% 4.47/4.63 (one = addition(antidomain(antidomain(antidomain(multiplication(X0!0, domain(zero))))), antidomain(antidomain(multiplication(X0!0, domain(zero)))))),
% 4.47/4.63 inference(symmetry,[status(thm)],[73])).
% 4.47/4.63 tff(75,plain,
% 4.47/4.63 (one = antidomain(domain(multiplication(X0!0, domain(zero))))),
% 4.47/4.63 inference(transitivity,[status(thm)],[74, 64, 18])).
% 4.47/4.63 tff(76,plain,
% 4.47/4.63 (multiplication(one, antidomain(antidomain(X0!0))) = multiplication(antidomain(domain(multiplication(X0!0, domain(zero)))), antidomain(antidomain(X0!0)))),
% 4.47/4.63 inference(monotonicity,[status(thm)],[75])).
% 4.47/4.63 tff(77,plain,
% 4.47/4.63 (multiplication(antidomain(domain(multiplication(X0!0, domain(zero)))), antidomain(antidomain(X0!0))) = multiplication(one, antidomain(antidomain(X0!0)))),
% 4.47/4.63 inference(symmetry,[status(thm)],[76])).
% 4.47/4.63 tff(78,plain,
% 4.47/4.63 (^[A: $i, B: $i] : refl((addition(A, B) = addition(B, A)) <=> (addition(A, B) = addition(B, A)))),
% 4.47/4.63 inference(bind,[status(th)],[])).
% 4.47/4.63 tff(79,plain,
% 4.47/4.63 (![A: $i, B: $i] : (addition(A, B) = addition(B, A)) <=> ![A: $i, B: $i] : (addition(A, B) = addition(B, A))),
% 4.47/4.63 inference(quant_intro,[status(thm)],[78])).
% 4.47/4.63 tff(80,plain,
% 4.47/4.63 (![A: $i, B: $i] : (addition(A, B) = addition(B, A)) <=> ![A: $i, B: $i] : (addition(A, B) = addition(B, A))),
% 4.47/4.63 inference(rewrite,[status(thm)],[])).
% 4.47/4.63 tff(81,axiom,(![A: $i, B: $i] : (addition(A, B) = addition(B, A))), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax','additive_commutativity')).
% 4.47/4.63 tff(82,plain,
% 4.47/4.63 (![A: $i, B: $i] : (addition(A, B) = addition(B, A))),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[81, 80])).
% 4.47/4.63 tff(83,plain,(
% 4.47/4.63 ![A: $i, B: $i] : (addition(A, B) = addition(B, A))),
% 4.47/4.63 inference(skolemize,[status(sab)],[82])).
% 4.47/4.63 tff(84,plain,
% 4.47/4.63 (![A: $i, B: $i] : (addition(A, B) = addition(B, A))),
% 4.47/4.63 inference(modus_ponens,[status(thm)],[83, 79])).
% 4.47/4.63 tff(85,plain,
% 4.47/4.63 ((~![A: $i, B: $i] : (addition(A, B) = addition(B, A))) | (addition(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(antidomain(X0!0)))) = addition(antidomain(antidomain(antidomain(X0!0))), antidomain(domain(antidomain(X0!0)))))),
% 4.47/4.63 inference(quant_inst,[status(thm)],[])).
% 4.47/4.63 tff(86,plain,
% 4.47/4.63 (addition(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(antidomain(X0!0)))) = addition(antidomain(antidomain(antidomain(X0!0))), antidomain(domain(antidomain(X0!0))))),
% 4.47/4.63 inference(unit_resolution,[status(thm)],[85, 84])).
% 4.47/4.63 tff(87,plain,
% 4.47/4.63 ((~![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))) | (domain(antidomain(X0!0)) = antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.63 inference(quant_inst,[status(thm)],[])).
% 4.47/4.63 tff(88,plain,
% 4.47/4.63 (domain(antidomain(X0!0)) = antidomain(antidomain(antidomain(X0!0)))),
% 4.47/4.63 inference(unit_resolution,[status(thm)],[87, 25])).
% 4.47/4.63 tff(89,plain,
% 4.47/4.63 (antidomain(antidomain(antidomain(X0!0))) = domain(antidomain(X0!0))),
% 4.47/4.63 inference(symmetry,[status(thm)],[88])).
% 4.47/4.63 tff(90,plain,
% 4.47/4.63 (antidomain(antidomain(antidomain(antidomain(X0!0)))) = antidomain(domain(antidomain(X0!0)))),
% 4.47/4.63 inference(monotonicity,[status(thm)],[89])).
% 4.47/4.63 tff(91,plain,
% 4.47/4.63 (antidomain(domain(antidomain(X0!0))) = antidomain(antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.63 inference(symmetry,[status(thm)],[90])).
% 4.47/4.63 tff(92,plain,
% 4.47/4.63 (addition(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(antidomain(X0!0)))) = addition(antidomain(antidomain(antidomain(antidomain(X0!0)))), antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[91])).
% 4.47/4.64 tff(93,plain,
% 4.47/4.64 (addition(antidomain(antidomain(antidomain(antidomain(X0!0)))), antidomain(antidomain(antidomain(X0!0)))) = addition(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[92])).
% 4.47/4.64 tff(94,plain,
% 4.47/4.64 ((~![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one)) | (addition(antidomain(antidomain(antidomain(antidomain(X0!0)))), antidomain(antidomain(antidomain(X0!0)))) = one)),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(95,plain,
% 4.47/4.64 (addition(antidomain(antidomain(antidomain(antidomain(X0!0)))), antidomain(antidomain(antidomain(X0!0)))) = one),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[94, 71])).
% 4.47/4.64 tff(96,plain,
% 4.47/4.64 (one = addition(antidomain(antidomain(antidomain(antidomain(X0!0)))), antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[95])).
% 4.47/4.64 tff(97,plain,
% 4.47/4.64 (antidomain(domain(multiplication(X0!0, domain(zero)))) = addition(antidomain(domain(multiplication(X0!0, domain(zero)))), zero)),
% 4.47/4.64 inference(symmetry,[status(thm)],[18])).
% 4.47/4.64 tff(98,plain,
% 4.47/4.64 (antidomain(domain(multiplication(X0!0, domain(zero)))) = addition(antidomain(antidomain(antidomain(X0!0))), antidomain(domain(antidomain(X0!0))))),
% 4.47/4.64 inference(transitivity,[status(thm)],[97, 63, 73, 96, 93, 86])).
% 4.47/4.64 tff(99,plain,
% 4.47/4.64 (multiplication(antidomain(domain(multiplication(X0!0, domain(zero)))), antidomain(antidomain(X0!0))) = multiplication(addition(antidomain(antidomain(antidomain(X0!0))), antidomain(domain(antidomain(X0!0)))), antidomain(antidomain(X0!0)))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[98])).
% 4.47/4.64 tff(100,plain,
% 4.47/4.64 (multiplication(addition(antidomain(antidomain(antidomain(X0!0))), antidomain(domain(antidomain(X0!0)))), antidomain(antidomain(X0!0))) = multiplication(antidomain(domain(multiplication(X0!0, domain(zero)))), antidomain(antidomain(X0!0)))),
% 4.47/4.64 inference(symmetry,[status(thm)],[99])).
% 4.47/4.64 tff(101,plain,
% 4.47/4.64 (^[A: $i, B: $i, C: $i] : refl((multiplication(addition(A, B), C) = addition(multiplication(A, C), multiplication(B, C))) <=> (multiplication(addition(A, B), C) = addition(multiplication(A, C), multiplication(B, C))))),
% 4.47/4.64 inference(bind,[status(th)],[])).
% 4.47/4.64 tff(102,plain,
% 4.47/4.64 (![A: $i, B: $i, C: $i] : (multiplication(addition(A, B), C) = addition(multiplication(A, C), multiplication(B, C))) <=> ![A: $i, B: $i, C: $i] : (multiplication(addition(A, B), C) = addition(multiplication(A, C), multiplication(B, C)))),
% 4.47/4.64 inference(quant_intro,[status(thm)],[101])).
% 4.47/4.64 tff(103,plain,
% 4.47/4.64 (![A: $i, B: $i, C: $i] : (multiplication(addition(A, B), C) = addition(multiplication(A, C), multiplication(B, C))) <=> ![A: $i, B: $i, C: $i] : (multiplication(addition(A, B), C) = addition(multiplication(A, C), multiplication(B, C)))),
% 4.47/4.64 inference(rewrite,[status(thm)],[])).
% 4.47/4.64 tff(104,axiom,(![A: $i, B: $i, C: $i] : (multiplication(addition(A, B), C) = addition(multiplication(A, C), multiplication(B, C)))), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax','left_distributivity')).
% 4.47/4.64 tff(105,plain,
% 4.47/4.64 (![A: $i, B: $i, C: $i] : (multiplication(addition(A, B), C) = addition(multiplication(A, C), multiplication(B, C)))),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[104, 103])).
% 4.47/4.64 tff(106,plain,(
% 4.47/4.64 ![A: $i, B: $i, C: $i] : (multiplication(addition(A, B), C) = addition(multiplication(A, C), multiplication(B, C)))),
% 4.47/4.64 inference(skolemize,[status(sab)],[105])).
% 4.47/4.64 tff(107,plain,
% 4.47/4.64 (![A: $i, B: $i, C: $i] : (multiplication(addition(A, B), C) = addition(multiplication(A, C), multiplication(B, C)))),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[106, 102])).
% 4.47/4.64 tff(108,plain,
% 4.47/4.64 ((~![A: $i, B: $i, C: $i] : (multiplication(addition(A, B), C) = addition(multiplication(A, C), multiplication(B, C)))) | (multiplication(addition(antidomain(antidomain(antidomain(X0!0))), antidomain(domain(antidomain(X0!0)))), antidomain(antidomain(X0!0))) = addition(multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))), multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(X0!0)))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(109,plain,
% 4.47/4.64 (multiplication(addition(antidomain(antidomain(antidomain(X0!0))), antidomain(domain(antidomain(X0!0)))), antidomain(antidomain(X0!0))) = addition(multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))), multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[108, 107])).
% 4.47/4.64 tff(110,plain,
% 4.47/4.64 (addition(multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))), multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(X0!0)))) = multiplication(addition(antidomain(antidomain(antidomain(X0!0))), antidomain(domain(antidomain(X0!0)))), antidomain(antidomain(X0!0)))),
% 4.47/4.64 inference(symmetry,[status(thm)],[109])).
% 4.47/4.64 tff(111,plain,
% 4.47/4.64 (multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(antidomain(X0!0)))) = multiplication(antidomain(antidomain(antidomain(antidomain(X0!0)))), antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[91])).
% 4.47/4.64 tff(112,plain,
% 4.47/4.64 (multiplication(antidomain(antidomain(antidomain(antidomain(X0!0)))), antidomain(antidomain(antidomain(X0!0)))) = multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[111])).
% 4.47/4.64 tff(113,plain,
% 4.47/4.64 (^[X0: $i] : refl((multiplication(antidomain(X0), X0) = zero) <=> (multiplication(antidomain(X0), X0) = zero))),
% 4.47/4.64 inference(bind,[status(th)],[])).
% 4.47/4.64 tff(114,plain,
% 4.47/4.64 (![X0: $i] : (multiplication(antidomain(X0), X0) = zero) <=> ![X0: $i] : (multiplication(antidomain(X0), X0) = zero)),
% 4.47/4.64 inference(quant_intro,[status(thm)],[113])).
% 4.47/4.64 tff(115,plain,
% 4.47/4.64 (![X0: $i] : (multiplication(antidomain(X0), X0) = zero) <=> ![X0: $i] : (multiplication(antidomain(X0), X0) = zero)),
% 4.47/4.64 inference(rewrite,[status(thm)],[])).
% 4.47/4.64 tff(116,axiom,(![X0: $i] : (multiplication(antidomain(X0), X0) = zero)), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax','domain1')).
% 4.47/4.64 tff(117,plain,
% 4.47/4.64 (![X0: $i] : (multiplication(antidomain(X0), X0) = zero)),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[116, 115])).
% 4.47/4.64 tff(118,plain,(
% 4.47/4.64 ![X0: $i] : (multiplication(antidomain(X0), X0) = zero)),
% 4.47/4.64 inference(skolemize,[status(sab)],[117])).
% 4.47/4.64 tff(119,plain,
% 4.47/4.64 (![X0: $i] : (multiplication(antidomain(X0), X0) = zero)),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[118, 114])).
% 4.47/4.64 tff(120,plain,
% 4.47/4.64 ((~![X0: $i] : (multiplication(antidomain(X0), X0) = zero)) | (multiplication(antidomain(antidomain(antidomain(antidomain(X0!0)))), antidomain(antidomain(antidomain(X0!0)))) = zero)),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(121,plain,
% 4.47/4.64 (multiplication(antidomain(antidomain(antidomain(antidomain(X0!0)))), antidomain(antidomain(antidomain(X0!0)))) = zero),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[120, 119])).
% 4.47/4.64 tff(122,plain,
% 4.47/4.64 (zero = multiplication(antidomain(antidomain(antidomain(antidomain(X0!0)))), antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[121])).
% 4.47/4.64 tff(123,plain,
% 4.47/4.64 ((~![X0: $i] : (multiplication(antidomain(X0), X0) = zero)) | (multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))) = zero)),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(124,plain,
% 4.47/4.64 (multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))) = zero),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[123, 119])).
% 4.47/4.64 tff(125,plain,
% 4.47/4.64 (multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))) = multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(transitivity,[status(thm)],[124, 122, 112])).
% 4.47/4.64 tff(126,plain,
% 4.47/4.64 (addition(multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))), multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(X0!0)))) = addition(multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(antidomain(X0!0)))), multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[125])).
% 4.47/4.64 tff(127,plain,
% 4.47/4.64 (addition(multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(antidomain(X0!0)))), multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(X0!0)))) = addition(multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))), multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[126])).
% 4.47/4.64 tff(128,plain,
% 4.47/4.64 (^[A: $i, B: $i, C: $i] : refl((multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C))) <=> (multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C))))),
% 4.47/4.64 inference(bind,[status(th)],[])).
% 4.47/4.64 tff(129,plain,
% 4.47/4.64 (![A: $i, B: $i, C: $i] : (multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C))) <=> ![A: $i, B: $i, C: $i] : (multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C)))),
% 4.47/4.64 inference(quant_intro,[status(thm)],[128])).
% 4.47/4.64 tff(130,plain,
% 4.47/4.64 (![A: $i, B: $i, C: $i] : (multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C))) <=> ![A: $i, B: $i, C: $i] : (multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C)))),
% 4.47/4.64 inference(rewrite,[status(thm)],[])).
% 4.47/4.64 tff(131,axiom,(![A: $i, B: $i, C: $i] : (multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C)))), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax','right_distributivity')).
% 4.47/4.64 tff(132,plain,
% 4.47/4.64 (![A: $i, B: $i, C: $i] : (multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C)))),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[131, 130])).
% 4.47/4.64 tff(133,plain,(
% 4.47/4.64 ![A: $i, B: $i, C: $i] : (multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C)))),
% 4.47/4.64 inference(skolemize,[status(sab)],[132])).
% 4.47/4.64 tff(134,plain,
% 4.47/4.64 (![A: $i, B: $i, C: $i] : (multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C)))),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[133, 129])).
% 4.47/4.64 tff(135,plain,
% 4.47/4.64 ((~![A: $i, B: $i, C: $i] : (multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C)))) | (multiplication(antidomain(domain(antidomain(X0!0))), addition(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0)))) = addition(multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(antidomain(X0!0)))), multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(X0!0)))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(136,plain,
% 4.47/4.64 (multiplication(antidomain(domain(antidomain(X0!0))), addition(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0)))) = addition(multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(antidomain(X0!0)))), multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[135, 134])).
% 4.47/4.64 tff(137,plain,
% 4.47/4.64 (^[X0: $i, X1: $i] : refl((addition(antidomain(multiplication(X0, X1)), antidomain(multiplication(X0, antidomain(antidomain(X1))))) = antidomain(multiplication(X0, antidomain(antidomain(X1))))) <=> (addition(antidomain(multiplication(X0, X1)), antidomain(multiplication(X0, antidomain(antidomain(X1))))) = antidomain(multiplication(X0, antidomain(antidomain(X1))))))),
% 4.47/4.64 inference(bind,[status(th)],[])).
% 4.47/4.64 tff(138,plain,
% 4.47/4.64 (![X0: $i, X1: $i] : (addition(antidomain(multiplication(X0, X1)), antidomain(multiplication(X0, antidomain(antidomain(X1))))) = antidomain(multiplication(X0, antidomain(antidomain(X1))))) <=> ![X0: $i, X1: $i] : (addition(antidomain(multiplication(X0, X1)), antidomain(multiplication(X0, antidomain(antidomain(X1))))) = antidomain(multiplication(X0, antidomain(antidomain(X1)))))),
% 4.47/4.64 inference(quant_intro,[status(thm)],[137])).
% 4.47/4.64 tff(139,plain,
% 4.47/4.64 (![X0: $i, X1: $i] : (addition(antidomain(multiplication(X0, X1)), antidomain(multiplication(X0, antidomain(antidomain(X1))))) = antidomain(multiplication(X0, antidomain(antidomain(X1))))) <=> ![X0: $i, X1: $i] : (addition(antidomain(multiplication(X0, X1)), antidomain(multiplication(X0, antidomain(antidomain(X1))))) = antidomain(multiplication(X0, antidomain(antidomain(X1)))))),
% 4.47/4.64 inference(rewrite,[status(thm)],[])).
% 4.47/4.64 tff(140,axiom,(![X0: $i, X1: $i] : (addition(antidomain(multiplication(X0, X1)), antidomain(multiplication(X0, antidomain(antidomain(X1))))) = antidomain(multiplication(X0, antidomain(antidomain(X1)))))), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax','domain2')).
% 4.47/4.64 tff(141,plain,
% 4.47/4.64 (![X0: $i, X1: $i] : (addition(antidomain(multiplication(X0, X1)), antidomain(multiplication(X0, antidomain(antidomain(X1))))) = antidomain(multiplication(X0, antidomain(antidomain(X1)))))),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[140, 139])).
% 4.47/4.64 tff(142,plain,(
% 4.47/4.64 ![X0: $i, X1: $i] : (addition(antidomain(multiplication(X0, X1)), antidomain(multiplication(X0, antidomain(antidomain(X1))))) = antidomain(multiplication(X0, antidomain(antidomain(X1)))))),
% 4.47/4.64 inference(skolemize,[status(sab)],[141])).
% 4.47/4.64 tff(143,plain,
% 4.47/4.64 (![X0: $i, X1: $i] : (addition(antidomain(multiplication(X0, X1)), antidomain(multiplication(X0, antidomain(antidomain(X1))))) = antidomain(multiplication(X0, antidomain(antidomain(X1)))))),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[142, 138])).
% 4.47/4.64 tff(144,plain,
% 4.47/4.64 ((~![X0: $i, X1: $i] : (addition(antidomain(multiplication(X0, X1)), antidomain(multiplication(X0, antidomain(antidomain(X1))))) = antidomain(multiplication(X0, antidomain(antidomain(X1)))))) | (addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))) = antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(145,plain,
% 4.47/4.64 (addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))) = antidomain(multiplication(X0!0, antidomain(antidomain(zero))))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[144, 143])).
% 4.47/4.64 tff(146,plain,
% 4.47/4.64 (^[A: $i] : refl((multiplication(A, zero) = zero) <=> (multiplication(A, zero) = zero))),
% 4.47/4.64 inference(bind,[status(th)],[])).
% 4.47/4.64 tff(147,plain,
% 4.47/4.64 (![A: $i] : (multiplication(A, zero) = zero) <=> ![A: $i] : (multiplication(A, zero) = zero)),
% 4.47/4.64 inference(quant_intro,[status(thm)],[146])).
% 4.47/4.64 tff(148,plain,
% 4.47/4.64 (![A: $i] : (multiplication(A, zero) = zero) <=> ![A: $i] : (multiplication(A, zero) = zero)),
% 4.47/4.64 inference(rewrite,[status(thm)],[])).
% 4.47/4.64 tff(149,axiom,(![A: $i] : (multiplication(A, zero) = zero)), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax','right_annihilation')).
% 4.47/4.64 tff(150,plain,
% 4.47/4.64 (![A: $i] : (multiplication(A, zero) = zero)),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[149, 148])).
% 4.47/4.64 tff(151,plain,(
% 4.47/4.64 ![A: $i] : (multiplication(A, zero) = zero)),
% 4.47/4.64 inference(skolemize,[status(sab)],[150])).
% 4.47/4.64 tff(152,plain,
% 4.47/4.64 (![A: $i] : (multiplication(A, zero) = zero)),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[151, 147])).
% 4.47/4.64 tff(153,plain,
% 4.47/4.64 ((~![A: $i] : (multiplication(A, zero) = zero)) | (multiplication(X0!0, zero) = zero)),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(154,plain,
% 4.47/4.64 (multiplication(X0!0, zero) = zero),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[153, 152])).
% 4.47/4.64 tff(155,plain,
% 4.47/4.64 (multiplication(X0!0, zero) = domain(multiplication(X0!0, domain(zero)))),
% 4.47/4.64 inference(transitivity,[status(thm)],[154, 46, 58, 48, 36])).
% 4.47/4.64 tff(156,plain,
% 4.47/4.64 (antidomain(multiplication(X0!0, zero)) = antidomain(domain(multiplication(X0!0, domain(zero))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[155])).
% 4.47/4.64 tff(157,plain,
% 4.47/4.64 (addition(zero, antidomain(multiplication(X0!0, zero))) = addition(zero, antidomain(domain(multiplication(X0!0, domain(zero)))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[156])).
% 4.47/4.64 tff(158,plain,
% 4.47/4.64 (addition(zero, antidomain(domain(multiplication(X0!0, domain(zero))))) = addition(zero, antidomain(multiplication(X0!0, zero)))),
% 4.47/4.64 inference(symmetry,[status(thm)],[157])).
% 4.47/4.64 tff(159,plain,
% 4.47/4.64 ((~![A: $i, B: $i] : (addition(A, B) = addition(B, A))) | (addition(antidomain(domain(multiplication(X0!0, domain(zero)))), zero) = addition(zero, antidomain(domain(multiplication(X0!0, domain(zero))))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(160,plain,
% 4.47/4.64 (addition(antidomain(domain(multiplication(X0!0, domain(zero)))), zero) = addition(zero, antidomain(domain(multiplication(X0!0, domain(zero)))))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[159, 84])).
% 4.47/4.64 tff(161,plain,
% 4.47/4.64 (antidomain(multiplication(X0!0, zero)) = addition(zero, antidomain(multiplication(X0!0, zero)))),
% 4.47/4.64 inference(transitivity,[status(thm)],[156, 97, 160, 158])).
% 4.47/4.64 tff(162,plain,
% 4.47/4.64 (addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))) = addition(addition(zero, antidomain(multiplication(X0!0, zero))), antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[161])).
% 4.47/4.64 tff(163,plain,
% 4.47/4.64 (addition(addition(zero, antidomain(multiplication(X0!0, zero))), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))) = addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[162])).
% 4.47/4.64 tff(164,plain,
% 4.47/4.64 (^[C: $i, B: $i, A: $i] : refl((addition(A, addition(B, C)) = addition(addition(A, B), C)) <=> (addition(A, addition(B, C)) = addition(addition(A, B), C)))),
% 4.47/4.64 inference(bind,[status(th)],[])).
% 4.47/4.64 tff(165,plain,
% 4.47/4.64 (![C: $i, B: $i, A: $i] : (addition(A, addition(B, C)) = addition(addition(A, B), C)) <=> ![C: $i, B: $i, A: $i] : (addition(A, addition(B, C)) = addition(addition(A, B), C))),
% 4.47/4.64 inference(quant_intro,[status(thm)],[164])).
% 4.47/4.64 tff(166,plain,
% 4.47/4.64 (![C: $i, B: $i, A: $i] : (addition(A, addition(B, C)) = addition(addition(A, B), C)) <=> ![C: $i, B: $i, A: $i] : (addition(A, addition(B, C)) = addition(addition(A, B), C))),
% 4.47/4.64 inference(rewrite,[status(thm)],[])).
% 4.47/4.64 tff(167,axiom,(![C: $i, B: $i, A: $i] : (addition(A, addition(B, C)) = addition(addition(A, B), C))), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax','additive_associativity')).
% 4.47/4.64 tff(168,plain,
% 4.47/4.64 (![C: $i, B: $i, A: $i] : (addition(A, addition(B, C)) = addition(addition(A, B), C))),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[167, 166])).
% 4.47/4.64 tff(169,plain,(
% 4.47/4.64 ![C: $i, B: $i, A: $i] : (addition(A, addition(B, C)) = addition(addition(A, B), C))),
% 4.47/4.64 inference(skolemize,[status(sab)],[168])).
% 4.47/4.64 tff(170,plain,
% 4.47/4.64 (![C: $i, B: $i, A: $i] : (addition(A, addition(B, C)) = addition(addition(A, B), C))),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[169, 165])).
% 4.47/4.64 tff(171,plain,
% 4.47/4.64 ((~![C: $i, B: $i, A: $i] : (addition(A, addition(B, C)) = addition(addition(A, B), C))) | (addition(zero, addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))) = addition(addition(zero, antidomain(multiplication(X0!0, zero))), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(172,plain,
% 4.47/4.64 (addition(zero, addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))) = addition(addition(zero, antidomain(multiplication(X0!0, zero))), antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[171, 170])).
% 4.47/4.64 tff(173,plain,
% 4.47/4.64 ((~![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))) | (domain(zero) = antidomain(antidomain(zero)))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(174,plain,
% 4.47/4.64 (domain(zero) = antidomain(antidomain(zero))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[173, 25])).
% 4.47/4.64 tff(175,plain,
% 4.47/4.64 (antidomain(antidomain(zero)) = domain(zero)),
% 4.47/4.64 inference(symmetry,[status(thm)],[174])).
% 4.47/4.64 tff(176,plain,
% 4.47/4.64 (multiplication(X0!0, antidomain(antidomain(zero))) = multiplication(X0!0, domain(zero))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[175])).
% 4.47/4.64 tff(177,plain,
% 4.47/4.64 (multiplication(X0!0, domain(zero)) = multiplication(X0!0, antidomain(antidomain(zero)))),
% 4.47/4.64 inference(symmetry,[status(thm)],[176])).
% 4.47/4.64 tff(178,plain,
% 4.47/4.64 (antidomain(multiplication(X0!0, domain(zero))) = antidomain(multiplication(X0!0, antidomain(antidomain(zero))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[177])).
% 4.47/4.64 tff(179,plain,
% 4.47/4.64 (antidomain(multiplication(X0!0, antidomain(antidomain(zero)))) = antidomain(multiplication(X0!0, domain(zero)))),
% 4.47/4.64 inference(symmetry,[status(thm)],[178])).
% 4.47/4.64 tff(180,plain,
% 4.47/4.64 (addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))) = antidomain(multiplication(X0!0, domain(zero)))),
% 4.47/4.64 inference(transitivity,[status(thm)],[145, 179])).
% 4.47/4.64 tff(181,plain,
% 4.47/4.64 (addition(zero, addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))) = addition(antidomain(antidomain(multiplication(X0!0, domain(zero)))), antidomain(multiplication(X0!0, domain(zero))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[59, 180])).
% 4.47/4.64 tff(182,plain,
% 4.47/4.64 (addition(antidomain(antidomain(multiplication(X0!0, domain(zero)))), antidomain(multiplication(X0!0, domain(zero)))) = addition(zero, addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[181])).
% 4.47/4.64 tff(183,plain,
% 4.47/4.64 ((~![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one)) | (addition(antidomain(antidomain(multiplication(X0!0, domain(zero)))), antidomain(multiplication(X0!0, domain(zero)))) = one)),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(184,plain,
% 4.47/4.64 (addition(antidomain(antidomain(multiplication(X0!0, domain(zero)))), antidomain(multiplication(X0!0, domain(zero)))) = one),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[183, 71])).
% 4.47/4.64 tff(185,plain,
% 4.47/4.64 (one = addition(antidomain(antidomain(multiplication(X0!0, domain(zero)))), antidomain(multiplication(X0!0, domain(zero))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[184])).
% 4.47/4.64 tff(186,plain,
% 4.47/4.64 ((~![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one)) | (addition(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))) = one)),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(187,plain,
% 4.47/4.64 (addition(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))) = one),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[186, 71])).
% 4.47/4.64 tff(188,plain,
% 4.47/4.64 (addition(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))) = antidomain(multiplication(X0!0, antidomain(antidomain(zero))))),
% 4.47/4.64 inference(transitivity,[status(thm)],[187, 185, 182, 172, 163, 145])).
% 4.47/4.64 tff(189,plain,
% 4.47/4.64 (multiplication(antidomain(domain(antidomain(X0!0))), addition(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0)))) = multiplication(antidomain(domain(antidomain(X0!0))), antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[188])).
% 4.47/4.64 tff(190,plain,
% 4.47/4.64 (multiplication(antidomain(domain(antidomain(X0!0))), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))) = multiplication(antidomain(domain(antidomain(X0!0))), addition(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[189])).
% 4.47/4.64 tff(191,plain,
% 4.47/4.64 (addition(addition(zero, antidomain(multiplication(X0!0, zero))), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))) = addition(zero, addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[172])).
% 4.47/4.64 tff(192,plain,
% 4.47/4.64 (antidomain(multiplication(X0!0, antidomain(antidomain(zero)))) = addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[145])).
% 4.47/4.64 tff(193,plain,
% 4.47/4.64 (antidomain(multiplication(X0!0, antidomain(antidomain(zero)))) = one),
% 4.47/4.64 inference(transitivity,[status(thm)],[192, 162, 191, 181, 184])).
% 4.47/4.64 tff(194,plain,
% 4.47/4.64 (multiplication(antidomain(domain(antidomain(X0!0))), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))) = multiplication(antidomain(domain(antidomain(X0!0))), one)),
% 4.47/4.64 inference(monotonicity,[status(thm)],[193])).
% 4.47/4.64 tff(195,plain,
% 4.47/4.64 (multiplication(antidomain(domain(antidomain(X0!0))), one) = multiplication(antidomain(domain(antidomain(X0!0))), antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[194])).
% 4.47/4.64 tff(196,plain,
% 4.47/4.64 (^[A: $i] : refl((multiplication(A, one) = A) <=> (multiplication(A, one) = A))),
% 4.47/4.64 inference(bind,[status(th)],[])).
% 4.47/4.64 tff(197,plain,
% 4.47/4.64 (![A: $i] : (multiplication(A, one) = A) <=> ![A: $i] : (multiplication(A, one) = A)),
% 4.47/4.64 inference(quant_intro,[status(thm)],[196])).
% 4.47/4.64 tff(198,plain,
% 4.47/4.64 (![A: $i] : (multiplication(A, one) = A) <=> ![A: $i] : (multiplication(A, one) = A)),
% 4.47/4.64 inference(rewrite,[status(thm)],[])).
% 4.47/4.64 tff(199,axiom,(![A: $i] : (multiplication(A, one) = A)), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax','multiplicative_right_identity')).
% 4.47/4.64 tff(200,plain,
% 4.47/4.64 (![A: $i] : (multiplication(A, one) = A)),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[199, 198])).
% 4.47/4.64 tff(201,plain,(
% 4.47/4.64 ![A: $i] : (multiplication(A, one) = A)),
% 4.47/4.64 inference(skolemize,[status(sab)],[200])).
% 4.47/4.64 tff(202,plain,
% 4.47/4.64 (![A: $i] : (multiplication(A, one) = A)),
% 4.47/4.64 inference(modus_ponens,[status(thm)],[201, 197])).
% 4.47/4.64 tff(203,plain,
% 4.47/4.64 ((~![A: $i] : (multiplication(A, one) = A)) | (multiplication(antidomain(domain(antidomain(X0!0))), one) = antidomain(domain(antidomain(X0!0))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(204,plain,
% 4.47/4.64 (multiplication(antidomain(domain(antidomain(X0!0))), one) = antidomain(domain(antidomain(X0!0)))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[203, 202])).
% 4.47/4.64 tff(205,plain,
% 4.47/4.64 (antidomain(domain(antidomain(X0!0))) = multiplication(antidomain(domain(antidomain(X0!0))), one)),
% 4.47/4.64 inference(symmetry,[status(thm)],[204])).
% 4.47/4.64 tff(206,plain,
% 4.47/4.64 (antidomain(antidomain(antidomain(antidomain(X0!0)))) = antidomain(antidomain(X0!0))),
% 4.47/4.64 inference(transitivity,[status(thm)],[90, 205, 195, 190, 136, 127, 110, 100, 77, 9])).
% 4.47/4.64 tff(207,plain,
% 4.47/4.64 (antidomain(antidomain(antidomain(antidomain(antidomain(X0!0))))) = antidomain(antidomain(antidomain(X0!0)))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[206])).
% 4.47/4.64 tff(208,plain,
% 4.47/4.64 ((~![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))) | (domain(antidomain(antidomain(antidomain(X0!0)))) = antidomain(antidomain(antidomain(antidomain(antidomain(X0!0))))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(209,plain,
% 4.47/4.64 (domain(antidomain(antidomain(antidomain(X0!0)))) = antidomain(antidomain(antidomain(antidomain(antidomain(X0!0)))))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[208, 25])).
% 4.47/4.64 tff(210,plain,
% 4.47/4.64 (domain(antidomain(antidomain(antidomain(X0!0)))) = antidomain(antidomain(antidomain(X0!0)))),
% 4.47/4.64 inference(transitivity,[status(thm)],[209, 207])).
% 4.47/4.64 tff(211,plain,
% 4.47/4.64 (addition(multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(antidomain(X0!0)))), multiplication(antidomain(domain(antidomain(X0!0))), antidomain(antidomain(X0!0)))) = multiplication(antidomain(domain(antidomain(X0!0))), addition(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[136])).
% 4.47/4.64 tff(212,plain,
% 4.47/4.64 (antidomain(antidomain(X0!0)) = multiplication(one, antidomain(antidomain(X0!0)))),
% 4.47/4.64 inference(symmetry,[status(thm)],[9])).
% 4.47/4.64 tff(213,plain,
% 4.47/4.64 ((~![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))) | (domain(X0!0) = antidomain(antidomain(X0!0)))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(214,plain,
% 4.47/4.64 (domain(X0!0) = antidomain(antidomain(X0!0))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[213, 25])).
% 4.47/4.64 tff(215,plain,
% 4.47/4.64 ((~![A: $i] : (multiplication(A, one) = A)) | (multiplication(X0!0, one) = X0!0)),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(216,plain,
% 4.47/4.64 (multiplication(X0!0, one) = X0!0),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[215, 202])).
% 4.47/4.64 tff(217,plain,
% 4.47/4.64 (multiplication(X0!0, one) = multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[75])).
% 4.47/4.64 tff(218,plain,
% 4.47/4.64 (multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))) = multiplication(X0!0, one)),
% 4.47/4.64 inference(symmetry,[status(thm)],[217])).
% 4.47/4.64 tff(219,plain,
% 4.47/4.64 ((~![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))) | (domain(antidomain(multiplication(X0!0, domain(zero)))) = antidomain(antidomain(antidomain(multiplication(X0!0, domain(zero))))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(220,plain,
% 4.47/4.64 (domain(antidomain(multiplication(X0!0, domain(zero)))) = antidomain(antidomain(antidomain(multiplication(X0!0, domain(zero)))))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[219, 25])).
% 4.47/4.64 tff(221,plain,
% 4.47/4.64 (antidomain(domain(multiplication(X0!0, domain(zero)))) = antidomain(multiplication(X0!0, domain(zero)))),
% 4.47/4.64 inference(transitivity,[status(thm)],[97, 63, 73, 185, 182, 172, 163, 145, 179])).
% 4.47/4.64 tff(222,plain,
% 4.47/4.64 (domain(antidomain(domain(multiplication(X0!0, domain(zero))))) = domain(antidomain(multiplication(X0!0, domain(zero))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[221])).
% 4.47/4.64 tff(223,plain,
% 4.47/4.64 (domain(one) = domain(antidomain(domain(multiplication(X0!0, domain(zero)))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[75])).
% 4.47/4.64 tff(224,plain,
% 4.47/4.64 (domain(one) = antidomain(domain(multiplication(X0!0, domain(zero))))),
% 4.47/4.64 inference(transitivity,[status(thm)],[223, 222, 220, 61])).
% 4.47/4.64 tff(225,plain,
% 4.47/4.64 (multiplication(X0!0, domain(one)) = multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[224])).
% 4.47/4.64 tff(226,plain,
% 4.47/4.64 (multiplication(X0!0, domain(one)) = X0!0),
% 4.47/4.64 inference(transitivity,[status(thm)],[225, 218, 216])).
% 4.47/4.64 tff(227,plain,
% 4.47/4.64 (domain(multiplication(X0!0, domain(one))) = domain(X0!0)),
% 4.47/4.64 inference(monotonicity,[status(thm)],[226])).
% 4.47/4.64 tff(228,plain,
% 4.47/4.64 ((~![X0: $i, X1: $i] : (forward_diamond(X0, X1) = domain(multiplication(X0, domain(X1))))) | (forward_diamond(X0!0, one) = domain(multiplication(X0!0, domain(one))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(229,plain,
% 4.47/4.64 (forward_diamond(X0!0, one) = domain(multiplication(X0!0, domain(one)))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[228, 34])).
% 4.47/4.64 tff(230,plain,
% 4.47/4.64 (domain(one) = one),
% 4.47/4.64 inference(transitivity,[status(thm)],[223, 222, 220, 61, 97, 63, 73])).
% 4.47/4.64 tff(231,plain,
% 4.47/4.64 (multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))) = X0!0),
% 4.47/4.64 inference(transitivity,[status(thm)],[218, 216])).
% 4.47/4.64 tff(232,plain,
% 4.47/4.64 (forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)) = forward_diamond(X0!0, one)),
% 4.47/4.64 inference(monotonicity,[status(thm)],[231, 230])).
% 4.47/4.64 tff(233,plain,
% 4.47/4.64 (forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)) = antidomain(antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(transitivity,[status(thm)],[232, 229, 227, 214, 212, 76, 99, 109, 126, 211, 189, 194, 204, 91])).
% 4.47/4.64 tff(234,plain,
% 4.47/4.64 (addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0))))) = addition(antidomain(antidomain(antidomain(antidomain(X0!0)))), antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[233, 210])).
% 4.47/4.64 tff(235,plain,
% 4.47/4.64 (addition(antidomain(antidomain(antidomain(antidomain(X0!0)))), antidomain(antidomain(antidomain(X0!0)))) = addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0)))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[234])).
% 4.47/4.64 tff(236,plain,
% 4.47/4.64 (antidomain(multiplication(X0!0, zero)) = antidomain(multiplication(X0!0, antidomain(antidomain(zero))))),
% 4.47/4.64 inference(transitivity,[status(thm)],[156, 97, 63, 73, 185, 182, 172, 163, 145])).
% 4.47/4.64 tff(237,plain,
% 4.47/4.64 (addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, zero))) = addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[236])).
% 4.47/4.64 tff(238,plain,
% 4.47/4.64 (antidomain(domain(multiplication(X0!0, domain(zero)))) = antidomain(multiplication(X0!0, zero))),
% 4.47/4.64 inference(symmetry,[status(thm)],[156])).
% 4.47/4.64 tff(239,plain,
% 4.47/4.64 (addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0))))) = antidomain(multiplication(X0!0, zero))),
% 4.47/4.64 inference(transitivity,[status(thm)],[234, 95, 74, 64, 18, 238])).
% 4.47/4.64 tff(240,plain,
% 4.47/4.64 (domain(one) = antidomain(multiplication(X0!0, zero))),
% 4.47/4.64 inference(transitivity,[status(thm)],[223, 222, 220, 61, 238])).
% 4.47/4.64 tff(241,plain,
% 4.47/4.64 (addition(domain(one), addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0)))))) = addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, zero)))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[240, 239])).
% 4.47/4.64 tff(242,plain,
% 4.47/4.64 (addition(domain(one), addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0)))))) = addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0)))))),
% 4.47/4.64 inference(transitivity,[status(thm)],[241, 237, 162, 191, 181, 184, 96, 235])).
% 4.47/4.64 tff(243,plain,
% 4.47/4.64 ((one = forward_diamond(star(X0!0), antidomain(X0!0))) <=> (forward_diamond(star(X0!0), antidomain(X0!0)) = one)),
% 4.47/4.64 inference(commutativity,[status(thm)],[])).
% 4.47/4.64 tff(244,plain,
% 4.47/4.64 ((~![X0: $i, X1: $i] : (forward_diamond(X0, X1) = domain(multiplication(X0, domain(X1))))) | (forward_diamond(star(X0!0), antidomain(X0!0)) = domain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(245,plain,
% 4.47/4.64 (forward_diamond(star(X0!0), antidomain(X0!0)) = domain(multiplication(star(X0!0), domain(antidomain(X0!0))))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[244, 34])).
% 4.47/4.64 tff(246,plain,
% 4.47/4.64 (domain(multiplication(star(X0!0), domain(antidomain(X0!0)))) = forward_diamond(star(X0!0), antidomain(X0!0))),
% 4.47/4.64 inference(symmetry,[status(thm)],[245])).
% 4.47/4.64 tff(247,plain,
% 4.47/4.64 ((~![A: $i] : (multiplication(A, one) = A)) | (multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), one) = domain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(248,plain,
% 4.47/4.64 (multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), one) = domain(multiplication(star(X0!0), domain(antidomain(X0!0))))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[247, 202])).
% 4.47/4.64 tff(249,plain,
% 4.47/4.64 (multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))) = multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), one)),
% 4.47/4.64 inference(monotonicity,[status(thm)],[193])).
% 4.47/4.64 tff(250,plain,
% 4.47/4.64 ((~![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one)) | (addition(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))) = one)),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(251,plain,
% 4.47/4.64 (addition(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))) = one),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[250, 71])).
% 4.47/4.64 tff(252,plain,
% 4.47/4.64 (multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))) = multiplication(star(X0!0), domain(antidomain(X0!0)))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[89])).
% 4.47/4.64 tff(253,plain,
% 4.47/4.64 (multiplication(star(X0!0), domain(antidomain(X0!0))) = multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[252])).
% 4.47/4.64 tff(254,plain,
% 4.47/4.64 (antidomain(multiplication(star(X0!0), domain(antidomain(X0!0)))) = antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[253])).
% 4.47/4.64 tff(255,plain,
% 4.47/4.64 (antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))) = antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[254])).
% 4.47/4.64 tff(256,plain,
% 4.47/4.64 ((~![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))) | (domain(multiplication(star(X0!0), domain(antidomain(X0!0)))) = antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(257,plain,
% 4.47/4.64 (domain(multiplication(star(X0!0), domain(antidomain(X0!0)))) = antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[256, 25])).
% 4.47/4.64 tff(258,plain,
% 4.47/4.64 (addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))) = addition(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[257, 255])).
% 4.47/4.64 tff(259,plain,
% 4.47/4.64 ((~![A: $i, B: $i] : (addition(A, B) = addition(B, A))) | (addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))) = addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), domain(multiplication(star(X0!0), domain(antidomain(X0!0))))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(260,plain,
% 4.47/4.64 (addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))) = addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), domain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[259, 84])).
% 4.47/4.64 tff(261,plain,
% 4.47/4.64 (addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), domain(multiplication(star(X0!0), domain(antidomain(X0!0))))) = addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))),
% 4.47/4.64 inference(symmetry,[status(thm)],[260])).
% 4.47/4.64 tff(262,plain,
% 4.47/4.64 ((~![X0: $i, X1: $i] : (addition(antidomain(multiplication(X0, X1)), antidomain(multiplication(X0, antidomain(antidomain(X1))))) = antidomain(multiplication(X0, antidomain(antidomain(X1)))))) | (addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))) = antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))),
% 4.47/4.64 inference(quant_inst,[status(thm)],[])).
% 4.47/4.64 tff(263,plain,
% 4.47/4.64 (addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))) = antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))),
% 4.47/4.64 inference(unit_resolution,[status(thm)],[262, 143])).
% 4.47/4.64 tff(264,plain,
% 4.47/4.64 (addition(addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))), domain(multiplication(star(X0!0), domain(antidomain(X0!0))))) = addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), domain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.64 inference(monotonicity,[status(thm)],[263])).
% 4.47/4.64 tff(265,plain,
% 4.47/4.64 ((~![C: $i, B: $i, A: $i] : (addition(A, addition(B, C)) = addition(addition(A, B), C))) | (addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), domain(multiplication(star(X0!0), domain(antidomain(X0!0)))))) = addition(addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))), domain(multiplication(star(X0!0), domain(antidomain(X0!0))))))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(266,plain,
% 4.47/4.65 (addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), domain(multiplication(star(X0!0), domain(antidomain(X0!0)))))) = addition(addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))), domain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[265, 170])).
% 4.47/4.65 tff(267,plain,
% 4.47/4.65 (addition(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))) = addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))),
% 4.47/4.65 inference(symmetry,[status(thm)],[258])).
% 4.47/4.65 tff(268,plain,
% 4.47/4.65 (one = addition(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.65 inference(symmetry,[status(thm)],[251])).
% 4.47/4.65 tff(269,plain,
% 4.47/4.65 (one = addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), domain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[268, 267, 260])).
% 4.47/4.65 tff(270,plain,
% 4.47/4.65 (addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), one) = addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), domain(multiplication(star(X0!0), domain(antidomain(X0!0))))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[269])).
% 4.47/4.65 tff(271,plain,
% 4.47/4.65 (addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), one) = antidomain(multiplication(X0!0, antidomain(antidomain(zero))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[270, 266, 264, 261, 258, 251, 185, 182, 172, 163, 145])).
% 4.47/4.65 tff(272,plain,
% 4.47/4.65 (multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), one)) = multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[271])).
% 4.47/4.65 tff(273,plain,
% 4.47/4.65 ((~![A: $i, B: $i, C: $i] : (multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C)))) | (multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), one)) = addition(multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), one)))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(274,plain,
% 4.47/4.65 (multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), one)) = addition(multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), one))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[273, 134])).
% 4.47/4.65 tff(275,plain,
% 4.47/4.65 (addition(multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), one)) = multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), one))),
% 4.47/4.65 inference(symmetry,[status(thm)],[274])).
% 4.47/4.65 tff(276,plain,
% 4.47/4.65 (domain(multiplication(star(X0!0), domain(antidomain(X0!0)))) = multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), one)),
% 4.47/4.65 inference(symmetry,[status(thm)],[248])).
% 4.47/4.65 tff(277,plain,
% 4.47/4.65 ((~![A: $i] : (addition(A, zero) = A)) | (addition(multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), zero) = multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(278,plain,
% 4.47/4.65 (addition(multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), zero) = multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0))))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[277, 16])).
% 4.47/4.65 tff(279,plain,
% 4.47/4.65 (multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))) = multiplication(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[257, 255])).
% 4.47/4.65 tff(280,plain,
% 4.47/4.65 (multiplication(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))) = multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))),
% 4.47/4.65 inference(symmetry,[status(thm)],[279])).
% 4.47/4.65 tff(281,plain,
% 4.47/4.65 ((~![X0: $i] : (multiplication(antidomain(X0), X0) = zero)) | (multiplication(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))) = zero)),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(282,plain,
% 4.47/4.65 (multiplication(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))) = zero),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[281, 119])).
% 4.47/4.65 tff(283,plain,
% 4.47/4.65 (zero = multiplication(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.65 inference(symmetry,[status(thm)],[282])).
% 4.47/4.65 tff(284,plain,
% 4.47/4.65 (zero = multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[283, 280])).
% 4.47/4.65 tff(285,plain,
% 4.47/4.65 (addition(multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), zero) = addition(multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[284])).
% 4.47/4.65 tff(286,plain,
% 4.47/4.65 (addition(multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))) = addition(multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), zero)),
% 4.47/4.65 inference(symmetry,[status(thm)],[285])).
% 4.47/4.65 tff(287,plain,
% 4.47/4.65 ((~![A: $i, B: $i, C: $i] : (multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C)))) | (multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))) = addition(multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(288,plain,
% 4.47/4.65 (multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))) = addition(multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[287, 134])).
% 4.47/4.65 tff(289,plain,
% 4.47/4.65 (addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))) = antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[263, 255])).
% 4.47/4.65 tff(290,plain,
% 4.47/4.65 (multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))) = multiplication(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[257, 289])).
% 4.47/4.65 tff(291,plain,
% 4.47/4.65 (multiplication(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))) = multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))))),
% 4.47/4.65 inference(symmetry,[status(thm)],[290])).
% 4.47/4.65 tff(292,plain,
% 4.47/4.65 (domain(multiplication(X0!0, domain(zero))) = forward_diamond(X0!0, zero)),
% 4.47/4.65 inference(symmetry,[status(thm)],[36])).
% 4.47/4.65 tff(293,plain,
% 4.47/4.65 (domain(multiplication(X0!0, domain(zero))) = divergence(X0!0)),
% 4.47/4.65 inference(transitivity,[status(thm)],[292, 47, 57])).
% 4.47/4.65 tff(294,plain,
% 4.47/4.65 (forward_diamond(X0!0, domain(multiplication(X0!0, domain(zero)))) = forward_diamond(X0!0, divergence(X0!0))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[293])).
% 4.47/4.65 tff(295,plain,
% 4.47/4.65 (forward_diamond(X0!0, domain(multiplication(X0!0, domain(zero)))) = multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[294, 57, 45, 283, 291, 288, 286, 278])).
% 4.47/4.65 tff(296,plain,
% 4.47/4.65 (addition(forward_diamond(X0!0, domain(multiplication(X0!0, domain(zero)))), domain(multiplication(star(X0!0), domain(antidomain(X0!0))))) = addition(multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), multiplication(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), one))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[295, 276])).
% 4.47/4.65 tff(297,plain,
% 4.47/4.65 ((~![A: $i] : (multiplication(one, A) = A)) | (multiplication(one, antidomain(X0!0)) = antidomain(X0!0))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(298,plain,
% 4.47/4.65 (multiplication(one, antidomain(X0!0)) = antidomain(X0!0)),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[297, 7])).
% 4.47/4.65 tff(299,plain,
% 4.47/4.65 (multiplication(one, antidomain(X0!0)) = multiplication(antidomain(domain(multiplication(X0!0, domain(zero)))), antidomain(X0!0))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[75])).
% 4.47/4.65 tff(300,plain,
% 4.47/4.65 (multiplication(antidomain(domain(multiplication(X0!0, domain(zero)))), antidomain(X0!0)) = multiplication(one, antidomain(X0!0))),
% 4.47/4.65 inference(symmetry,[status(thm)],[299])).
% 4.47/4.65 tff(301,plain,
% 4.47/4.65 ((~![A: $i, B: $i] : (addition(A, B) = addition(B, A))) | (addition(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))) = addition(antidomain(antidomain(X0!0)), antidomain(antidomain(antidomain(X0!0)))))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(302,plain,
% 4.47/4.65 (addition(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))) = addition(antidomain(antidomain(X0!0)), antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[301, 84])).
% 4.47/4.65 tff(303,plain,
% 4.47/4.65 (one = addition(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0)))),
% 4.47/4.65 inference(symmetry,[status(thm)],[187])).
% 4.47/4.65 tff(304,plain,
% 4.47/4.65 (antidomain(domain(multiplication(X0!0, domain(zero)))) = addition(antidomain(antidomain(X0!0)), antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[97, 63, 73, 303, 302])).
% 4.47/4.65 tff(305,plain,
% 4.47/4.65 (multiplication(antidomain(domain(multiplication(X0!0, domain(zero)))), antidomain(X0!0)) = multiplication(addition(antidomain(antidomain(X0!0)), antidomain(antidomain(antidomain(X0!0)))), antidomain(X0!0))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[304])).
% 4.47/4.65 tff(306,plain,
% 4.47/4.65 (multiplication(addition(antidomain(antidomain(X0!0)), antidomain(antidomain(antidomain(X0!0)))), antidomain(X0!0)) = multiplication(antidomain(domain(multiplication(X0!0, domain(zero)))), antidomain(X0!0))),
% 4.47/4.65 inference(symmetry,[status(thm)],[305])).
% 4.47/4.65 tff(307,plain,
% 4.47/4.65 ((~![A: $i, B: $i, C: $i] : (multiplication(addition(A, B), C) = addition(multiplication(A, C), multiplication(B, C)))) | (multiplication(addition(antidomain(antidomain(X0!0)), antidomain(antidomain(antidomain(X0!0)))), antidomain(X0!0)) = addition(multiplication(antidomain(antidomain(X0!0)), antidomain(X0!0)), multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(X0!0))))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(308,plain,
% 4.47/4.65 (multiplication(addition(antidomain(antidomain(X0!0)), antidomain(antidomain(antidomain(X0!0)))), antidomain(X0!0)) = addition(multiplication(antidomain(antidomain(X0!0)), antidomain(X0!0)), multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(X0!0)))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[307, 107])).
% 4.47/4.65 tff(309,plain,
% 4.47/4.65 (addition(multiplication(antidomain(antidomain(X0!0)), antidomain(X0!0)), multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(X0!0))) = multiplication(addition(antidomain(antidomain(X0!0)), antidomain(antidomain(antidomain(X0!0)))), antidomain(X0!0))),
% 4.47/4.65 inference(symmetry,[status(thm)],[308])).
% 4.47/4.65 tff(310,plain,
% 4.47/4.65 (zero = multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0)))),
% 4.47/4.65 inference(symmetry,[status(thm)],[124])).
% 4.47/4.65 tff(311,plain,
% 4.47/4.65 ((~![X0: $i] : (multiplication(antidomain(X0), X0) = zero)) | (multiplication(antidomain(antidomain(X0!0)), antidomain(X0!0)) = zero)),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(312,plain,
% 4.47/4.65 (multiplication(antidomain(antidomain(X0!0)), antidomain(X0!0)) = zero),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[311, 119])).
% 4.47/4.65 tff(313,plain,
% 4.47/4.65 (multiplication(antidomain(antidomain(X0!0)), antidomain(X0!0)) = multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0)))),
% 4.47/4.65 inference(transitivity,[status(thm)],[312, 310])).
% 4.47/4.65 tff(314,plain,
% 4.47/4.65 (addition(multiplication(antidomain(antidomain(X0!0)), antidomain(X0!0)), multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(X0!0))) = addition(multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))), multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(X0!0)))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[313])).
% 4.47/4.65 tff(315,plain,
% 4.47/4.65 (addition(multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))), multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(X0!0))) = addition(multiplication(antidomain(antidomain(X0!0)), antidomain(X0!0)), multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(X0!0)))),
% 4.47/4.65 inference(symmetry,[status(thm)],[314])).
% 4.47/4.65 tff(316,plain,
% 4.47/4.65 ((~![A: $i, B: $i, C: $i] : (multiplication(A, addition(B, C)) = addition(multiplication(A, B), multiplication(A, C)))) | (multiplication(antidomain(antidomain(antidomain(X0!0))), addition(antidomain(antidomain(X0!0)), antidomain(X0!0))) = addition(multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))), multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(X0!0))))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(317,plain,
% 4.47/4.65 (multiplication(antidomain(antidomain(antidomain(X0!0))), addition(antidomain(antidomain(X0!0)), antidomain(X0!0))) = addition(multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))), multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(X0!0)))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[316, 134])).
% 4.47/4.65 tff(318,plain,
% 4.47/4.65 ((~![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one)) | (addition(antidomain(antidomain(X0!0)), antidomain(X0!0)) = one)),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(319,plain,
% 4.47/4.65 (addition(antidomain(antidomain(X0!0)), antidomain(X0!0)) = one),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[318, 71])).
% 4.47/4.65 tff(320,plain,
% 4.47/4.65 (addition(antidomain(antidomain(X0!0)), antidomain(X0!0)) = antidomain(multiplication(X0!0, antidomain(antidomain(zero))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[319, 185, 182, 172, 163, 145])).
% 4.47/4.65 tff(321,plain,
% 4.47/4.65 (multiplication(antidomain(antidomain(antidomain(X0!0))), addition(antidomain(antidomain(X0!0)), antidomain(X0!0))) = multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[320])).
% 4.47/4.65 tff(322,plain,
% 4.47/4.65 (multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))) = multiplication(antidomain(antidomain(antidomain(X0!0))), addition(antidomain(antidomain(X0!0)), antidomain(X0!0)))),
% 4.47/4.65 inference(symmetry,[status(thm)],[321])).
% 4.47/4.65 tff(323,plain,
% 4.47/4.65 (multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(multiplication(X0!0, antidomain(antidomain(zero))))) = multiplication(antidomain(antidomain(antidomain(X0!0))), one)),
% 4.47/4.65 inference(monotonicity,[status(thm)],[193])).
% 4.47/4.65 tff(324,plain,
% 4.47/4.65 (multiplication(antidomain(antidomain(antidomain(X0!0))), one) = multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(multiplication(X0!0, antidomain(antidomain(zero)))))),
% 4.47/4.65 inference(symmetry,[status(thm)],[323])).
% 4.47/4.65 tff(325,plain,
% 4.47/4.65 ((~![A: $i] : (multiplication(A, one) = A)) | (multiplication(antidomain(antidomain(antidomain(X0!0))), one) = antidomain(antidomain(antidomain(X0!0))))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(326,plain,
% 4.47/4.65 (multiplication(antidomain(antidomain(antidomain(X0!0))), one) = antidomain(antidomain(antidomain(X0!0)))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[325, 202])).
% 4.47/4.65 tff(327,plain,
% 4.47/4.65 (antidomain(antidomain(antidomain(X0!0))) = multiplication(antidomain(antidomain(antidomain(X0!0))), one)),
% 4.47/4.65 inference(symmetry,[status(thm)],[326])).
% 4.47/4.65 tff(328,plain,
% 4.47/4.65 (domain(antidomain(X0!0)) = antidomain(X0!0)),
% 4.47/4.65 inference(transitivity,[status(thm)],[88, 327, 324, 322, 317, 315, 309, 306, 300, 298])).
% 4.47/4.65 tff(329,plain,
% 4.47/4.65 (forward_diamond(star(X0!0), domain(antidomain(X0!0))) = forward_diamond(star(X0!0), antidomain(X0!0))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[328])).
% 4.47/4.65 tff(330,plain,
% 4.47/4.65 (domain(antidomain(antidomain(antidomain(X0!0)))) = domain(antidomain(X0!0))),
% 4.47/4.65 inference(transitivity,[status(thm)],[209, 207, 89])).
% 4.47/4.65 tff(331,plain,
% 4.47/4.65 (star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))) = star(X0!0)),
% 4.47/4.65 inference(monotonicity,[status(thm)],[231])).
% 4.47/4.65 tff(332,plain,
% 4.47/4.65 (forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))) = forward_diamond(star(X0!0), domain(antidomain(X0!0)))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[331, 330])).
% 4.47/4.65 tff(333,plain,
% 4.47/4.65 (forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))) = domain(multiplication(star(X0!0), domain(antidomain(X0!0))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[332, 329, 245])).
% 4.47/4.65 tff(334,plain,
% 4.47/4.65 (forward_diamond(X0!0, divergence(X0!0)) = forward_diamond(X0!0, domain(multiplication(X0!0, domain(zero))))),
% 4.47/4.65 inference(symmetry,[status(thm)],[294])).
% 4.47/4.65 tff(335,plain,
% 4.47/4.65 (divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))) = divergence(X0!0)),
% 4.47/4.65 inference(monotonicity,[status(thm)],[231])).
% 4.47/4.65 tff(336,plain,
% 4.47/4.65 (divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))) = forward_diamond(X0!0, domain(multiplication(X0!0, domain(zero))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[335, 58, 334])).
% 4.47/4.65 tff(337,plain,
% 4.47/4.65 (addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0)))))) = addition(forward_diamond(X0!0, domain(multiplication(X0!0, domain(zero)))), domain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[336, 333])).
% 4.47/4.65 tff(338,plain,
% 4.47/4.65 (addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0)))))) = forward_diamond(star(X0!0), antidomain(X0!0))),
% 4.47/4.65 inference(transitivity,[status(thm)],[337, 296, 275, 272, 249, 248, 246])).
% 4.47/4.65 tff(339,plain,
% 4.47/4.65 ((~![X0: $i] : (addition(antidomain(antidomain(X0)), antidomain(X0)) = one)) | (addition(antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))) = one)),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(340,plain,
% 4.47/4.65 (addition(antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))) = one),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[339, 71])).
% 4.47/4.65 tff(341,plain,
% 4.47/4.65 ((~![A: $i, B: $i] : (addition(A, B) = addition(B, A))) | (addition(antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))) = addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0))))))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(342,plain,
% 4.47/4.65 (addition(antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))) = addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0)))))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[341, 84])).
% 4.47/4.65 tff(343,plain,
% 4.47/4.65 (addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0))))) = addition(antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0))))),
% 4.47/4.65 inference(symmetry,[status(thm)],[342])).
% 4.47/4.65 tff(344,plain,
% 4.47/4.65 (addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0))))) = antidomain(multiplication(X0!0, zero))),
% 4.47/4.65 inference(transitivity,[status(thm)],[343, 340, 74, 64, 18, 238])).
% 4.47/4.65 tff(345,plain,
% 4.47/4.65 (one = antidomain(multiplication(X0!0, zero))),
% 4.47/4.65 inference(transitivity,[status(thm)],[74, 64, 18, 238])).
% 4.47/4.65 tff(346,plain,
% 4.47/4.65 (addition(one, addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0)))))) = addition(antidomain(multiplication(X0!0, zero)), antidomain(multiplication(X0!0, zero)))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[345, 344])).
% 4.47/4.65 tff(347,plain,
% 4.47/4.65 ((~![C: $i, B: $i, A: $i] : (addition(A, addition(B, C)) = addition(addition(A, B), C))) | (addition(one, addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0)))))) = addition(addition(one, antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0))))))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(348,plain,
% 4.47/4.65 (addition(one, addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0)))))) = addition(addition(one, antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0)))))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[347, 170])).
% 4.47/4.65 tff(349,plain,
% 4.47/4.65 (addition(addition(one, antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0))))) = addition(one, addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0))))))),
% 4.47/4.65 inference(symmetry,[status(thm)],[348])).
% 4.47/4.65 tff(350,plain,
% 4.47/4.65 ((~![C: $i, B: $i, A: $i] : (addition(A, addition(B, C)) = addition(addition(A, B), C))) | (addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))) = addition(addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(351,plain,
% 4.47/4.65 (addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))) = addition(addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[350, 170])).
% 4.47/4.65 tff(352,plain,
% 4.47/4.65 (addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))) = addition(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[257, 289])).
% 4.47/4.65 tff(353,plain,
% 4.47/4.65 (addition(antidomain(antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), domain(antidomain(X0!0))))) = addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))))),
% 4.47/4.65 inference(symmetry,[status(thm)],[352])).
% 4.47/4.65 tff(354,plain,
% 4.47/4.65 (one = addition(addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[268, 353, 351])).
% 4.47/4.65 tff(355,plain,
% 4.47/4.65 (addition(one, antidomain(multiplication(star(X0!0), antidomain(X0!0)))) = addition(addition(addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))), antidomain(multiplication(star(X0!0), antidomain(X0!0))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[354])).
% 4.47/4.65 tff(356,plain,
% 4.47/4.65 (addition(addition(addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))) = addition(one, antidomain(multiplication(star(X0!0), antidomain(X0!0))))),
% 4.47/4.65 inference(symmetry,[status(thm)],[355])).
% 4.47/4.65 tff(357,plain,
% 4.47/4.65 ((~![C: $i, B: $i, A: $i] : (addition(A, addition(B, C)) = addition(addition(A, B), C))) | (addition(addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), antidomain(X0!0))))) = addition(addition(addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(358,plain,
% 4.47/4.65 (addition(addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), antidomain(X0!0))))) = addition(addition(addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))), antidomain(multiplication(star(X0!0), antidomain(X0!0))))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[357, 170])).
% 4.47/4.65 tff(359,plain,
% 4.47/4.65 ((~![A: $i, B: $i] : (addition(A, B) = addition(B, A))) | (addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))) = addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(360,plain,
% 4.47/4.65 (addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))) = addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), antidomain(X0!0))))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[359, 84])).
% 4.47/4.65 tff(361,plain,
% 4.47/4.65 (addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))) = addition(antidomain(multiplication(star(X0!0), antidomain(X0!0))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))),
% 4.47/4.65 inference(symmetry,[status(thm)],[360])).
% 4.47/4.65 tff(362,plain,
% 4.47/4.65 (addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))) = antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[361, 263])).
% 4.47/4.65 tff(363,plain,
% 4.47/4.65 (addition(addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), antidomain(X0!0))))) = addition(addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[362])).
% 4.47/4.65 tff(364,plain,
% 4.47/4.65 (addition(addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0)))))) = addition(addition(domain(multiplication(star(X0!0), domain(antidomain(X0!0)))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))), addition(antidomain(multiplication(star(X0!0), antidomain(antidomain(antidomain(X0!0))))), antidomain(multiplication(star(X0!0), antidomain(X0!0)))))),
% 4.47/4.65 inference(symmetry,[status(thm)],[363])).
% 4.47/4.65 tff(365,plain,
% 4.47/4.65 (one = addition(one, antidomain(multiplication(star(X0!0), antidomain(X0!0))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[268, 353, 351, 364, 358, 356])).
% 4.47/4.65 tff(366,plain,
% 4.47/4.65 (addition(one, antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0))))) = addition(addition(one, antidomain(multiplication(star(X0!0), antidomain(X0!0)))), antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0)))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[365])).
% 4.47/4.65 tff(367,plain,
% 4.47/4.65 ((~![X0: $i] : (domain(X0) = antidomain(antidomain(X0)))) | (domain(multiplication(star(X0!0), antidomain(X0!0))) = antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0)))))),
% 4.47/4.65 inference(quant_inst,[status(thm)],[])).
% 4.47/4.65 tff(368,plain,
% 4.47/4.65 (domain(multiplication(star(X0!0), antidomain(X0!0))) = antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0))))),
% 4.47/4.65 inference(unit_resolution,[status(thm)],[367, 25])).
% 4.47/4.65 tff(369,plain,
% 4.47/4.65 (addition(multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(antidomain(X0!0))), multiplication(antidomain(antidomain(antidomain(X0!0))), antidomain(X0!0))) = multiplication(antidomain(antidomain(antidomain(X0!0))), addition(antidomain(antidomain(X0!0)), antidomain(X0!0)))),
% 4.47/4.65 inference(symmetry,[status(thm)],[317])).
% 4.47/4.65 tff(370,plain,
% 4.47/4.65 (antidomain(X0!0) = multiplication(one, antidomain(X0!0))),
% 4.47/4.65 inference(symmetry,[status(thm)],[298])).
% 4.47/4.65 tff(371,plain,
% 4.47/4.65 (antidomain(X0!0) = domain(antidomain(X0!0))),
% 4.47/4.65 inference(transitivity,[status(thm)],[370, 299, 305, 308, 314, 369, 321, 323, 326, 89])).
% 4.47/4.65 tff(372,plain,
% 4.47/4.65 (multiplication(star(X0!0), antidomain(X0!0)) = multiplication(star(X0!0), domain(antidomain(X0!0)))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[371])).
% 4.47/4.65 tff(373,plain,
% 4.47/4.65 (domain(multiplication(star(X0!0), antidomain(X0!0))) = domain(multiplication(star(X0!0), domain(antidomain(X0!0))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[372])).
% 4.47/4.65 tff(374,plain,
% 4.47/4.65 (domain(multiplication(star(X0!0), domain(antidomain(X0!0)))) = domain(multiplication(star(X0!0), antidomain(X0!0)))),
% 4.47/4.65 inference(symmetry,[status(thm)],[373])).
% 4.47/4.65 tff(375,plain,
% 4.47/4.65 (domain(multiplication(star(X0!0), domain(antidomain(X0!0)))) = antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[374, 368])).
% 4.47/4.65 tff(376,plain,
% 4.47/4.65 (addition(one, domain(multiplication(star(X0!0), domain(antidomain(X0!0))))) = addition(one, antidomain(antidomain(multiplication(star(X0!0), antidomain(X0!0)))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[375])).
% 4.47/4.65 tff(377,plain,
% 4.47/4.65 (addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0)))))) = domain(multiplication(star(X0!0), domain(antidomain(X0!0))))),
% 4.47/4.65 inference(transitivity,[status(thm)],[337, 296, 275, 272, 249, 248])).
% 4.47/4.65 tff(378,plain,
% 4.47/4.65 (addition(domain(one), addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) = addition(one, domain(multiplication(star(X0!0), domain(antidomain(X0!0)))))),
% 4.47/4.65 inference(monotonicity,[status(thm)],[230, 377])).
% 4.47/4.65 tff(379,plain,
% 4.47/4.65 (addition(domain(one), addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) = one),
% 4.47/4.65 inference(transitivity,[status(thm)],[378, 376, 366, 349, 346, 237, 162, 191, 181, 184])).
% 4.47/4.66 tff(380,plain,
% 4.47/4.66 ((addition(domain(one), addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) = addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) <=> (one = forward_diamond(star(X0!0), antidomain(X0!0)))),
% 4.47/4.66 inference(monotonicity,[status(thm)],[379, 338])).
% 4.47/4.66 tff(381,plain,
% 4.47/4.66 ((addition(domain(one), addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) = addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) <=> (forward_diamond(star(X0!0), antidomain(X0!0)) = one)),
% 4.47/4.66 inference(transitivity,[status(thm)],[380, 243])).
% 4.47/4.66 tff(382,plain,
% 4.47/4.66 ((forward_diamond(star(X0!0), antidomain(X0!0)) = one) <=> (addition(domain(one), addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) = addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0)))))))),
% 4.47/4.66 inference(symmetry,[status(thm)],[381])).
% 4.47/4.66 tff(383,plain,
% 4.47/4.66 ((~(forward_diamond(star(X0!0), antidomain(X0!0)) = one)) <=> (~(addition(domain(one), addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) = addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))))),
% 4.47/4.66 inference(monotonicity,[status(thm)],[382])).
% 4.47/4.66 tff(384,plain,
% 4.47/4.66 (~(forward_diamond(star(X0!0), antidomain(X0!0)) = one)),
% 4.47/4.66 inference(or_elim,[status(thm)],[44])).
% 4.47/4.66 tff(385,plain,
% 4.47/4.66 (~(addition(domain(one), addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) = addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0)))))))),
% 4.47/4.66 inference(modus_ponens,[status(thm)],[384, 383])).
% 4.47/4.66 tff(386,plain,
% 4.47/4.66 (^[X0: $i, X1: $i, X2: $i] : refl(((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2))))) <=> ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2))))))),
% 4.47/4.66 inference(bind,[status(th)],[])).
% 4.47/4.66 tff(387,plain,
% 4.47/4.66 (![X0: $i, X1: $i, X2: $i] : ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2))))) <=> ![X0: $i, X1: $i, X2: $i] : ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2)))))),
% 4.47/4.66 inference(quant_intro,[status(thm)],[386])).
% 4.47/4.66 tff(388,plain,
% 4.47/4.66 (![X0: $i, X1: $i, X2: $i] : ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2))))) <=> ![X0: $i, X1: $i, X2: $i] : ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2)))))),
% 4.47/4.66 inference(rewrite,[status(thm)],[])).
% 4.47/4.66 tff(389,plain,
% 4.47/4.66 (^[X0: $i, X1: $i, X2: $i] : rewrite(((addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2))) => (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2))))) <=> ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2))))))),
% 4.47/4.66 inference(bind,[status(th)],[])).
% 4.47/4.66 tff(390,plain,
% 4.47/4.66 (![X0: $i, X1: $i, X2: $i] : ((addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2))) => (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2))))) <=> ![X0: $i, X1: $i, X2: $i] : ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2)))))),
% 4.47/4.66 inference(quant_intro,[status(thm)],[389])).
% 4.47/4.66 tff(391,axiom,(![X0: $i, X1: $i, X2: $i] : ((addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2))) => (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2)))))), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+7.ax','divergence2')).
% 4.47/4.66 tff(392,plain,
% 4.47/4.66 (![X0: $i, X1: $i, X2: $i] : ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2)))))),
% 4.47/4.66 inference(modus_ponens,[status(thm)],[391, 390])).
% 4.47/4.66 tff(393,plain,
% 4.47/4.66 (![X0: $i, X1: $i, X2: $i] : ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2)))))),
% 4.47/4.66 inference(modus_ponens,[status(thm)],[392, 388])).
% 4.47/4.66 tff(394,plain,(
% 4.47/4.66 ![X0: $i, X1: $i, X2: $i] : ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2)))))),
% 4.47/4.66 inference(skolemize,[status(sab)],[393])).
% 4.47/4.66 tff(395,plain,
% 4.47/4.66 (![X0: $i, X1: $i, X2: $i] : ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2)))))),
% 4.47/4.66 inference(modus_ponens,[status(thm)],[394, 387])).
% 4.47/4.66 tff(396,plain,
% 4.47/4.66 (((~![X0: $i, X1: $i, X2: $i] : ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2)))))) | ((~(addition(domain(one), addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0)))))) = addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0))))))) | (addition(domain(one), addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) = addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))))) <=> ((~![X0: $i, X1: $i, X2: $i] : ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2)))))) | (~(addition(domain(one), addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0)))))) = addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0))))))) | (addition(domain(one), addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) = addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))))),
% 4.47/4.66 inference(rewrite,[status(thm)],[])).
% 4.47/4.66 tff(397,plain,
% 4.47/4.66 ((~![X0: $i, X1: $i, X2: $i] : ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2)))))) | ((~(addition(domain(one), addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0)))))) = addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0))))))) | (addition(domain(one), addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) = addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))))),
% 4.47/4.67 inference(quant_inst,[status(thm)],[])).
% 4.47/4.67 tff(398,plain,
% 4.47/4.67 ((~![X0: $i, X1: $i, X2: $i] : ((~(addition(domain(X0), addition(forward_diamond(X1, domain(X0)), domain(X2))) = addition(forward_diamond(X1, domain(X0)), domain(X2)))) | (addition(domain(X0), addition(divergence(X1), forward_diamond(star(X1), domain(X2)))) = addition(divergence(X1), forward_diamond(star(X1), domain(X2)))))) | (~(addition(domain(one), addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0)))))) = addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0))))))) | (addition(domain(one), addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) = addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0)))))))),
% 4.47/4.67 inference(modus_ponens,[status(thm)],[397, 396])).
% 4.47/4.67 tff(399,plain,
% 4.47/4.67 ((~(addition(domain(one), addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0)))))) = addition(forward_diamond(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero))))), domain(one)), domain(antidomain(antidomain(antidomain(X0!0))))))) | (addition(domain(one), addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0))))))) = addition(divergence(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), forward_diamond(star(multiplication(X0!0, antidomain(domain(multiplication(X0!0, domain(zero)))))), domain(antidomain(antidomain(antidomain(X0!0)))))))),
% 4.47/4.67 inference(unit_resolution,[status(thm)],[398, 395])).
% 4.47/4.67 tff(400,plain,
% 4.47/4.67 ($false),
% 4.47/4.67 inference(unit_resolution,[status(thm)],[399, 385, 242])).
% 4.47/4.67 % SZS output end Proof
% 4.47/4.68 % E exiting
%------------------------------------------------------------------------------