%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : MGT115+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% 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 : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:24:15 AM UTC 2026
% Result : Theorem 0.16s 0.48s
% Output : Proof 0.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : MGT115+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : run_E %s %d THM
% 0.16/0.40 % Computer : n008.cluster.edu
% 0.16/0.40 % Model : x86_64 x86_64
% 0.16/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.40 % Memory : 8046.5625MB
% 0.16/0.40 % OS : Linux 6.8.0-71-generic
% 0.16/0.40 % CPULimit : 300
% 0.16/0.40 % WCLimit : 300
% 0.16/0.40 % DateTime : Mon Sep 7 14:09:25 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.16/0.48 % SZS status Theorem
% 0.16/0.48 % SZS output start Proof
% 0.16/0.48 tff(pi2_type, type, (
% 0.16/0.48 pi2: $i)).
% 0.16/0.48 tff(pi1_type, type, (
% 0.16/0.48 pi1: $i)).
% 0.16/0.48 tff(inj_0_type, type, (
% 0.16/0.48 inj_0: $i > $i)).
% 0.16/0.48 tff(issue_type, type, (
% 0.16/0.48 issue: $i > $i)).
% 0.16/0.48 tff(1,plain,
% 0.16/0.48 (![Xk!0: $i] : (inj_0(issue(Xk!0)) = Xk!0) <=> ![Xk!0: $i] : (inj_0(issue(Xk!0)) = Xk!0)),
% 0.16/0.48 inference(rewrite,[status(thm)],[])).
% 0.16/0.48 tff(2,plain,
% 0.16/0.48 (![A: $i, B: $i] : ((~(issue(A) = issue(B))) | (A = B)) <=> ![Xk!0: $i] : (inj_0(issue(Xk!0)) = Xk!0)),
% 0.16/0.48 inference(rewrite,[status(thm)],[])).
% 0.16/0.48 tff(3,plain,
% 0.16/0.48 (![A: $i, B: $i] : ((~(issue(A) = issue(B))) | (A = B)) <=> ![A: $i, B: $i] : ((~(issue(A) = issue(B))) | (A = B))),
% 0.16/0.48 inference(rewrite,[status(thm)],[])).
% 0.16/0.48 tff(4,plain,
% 0.16/0.48 (^[A: $i, B: $i] : rewrite(((issue(A) = issue(B)) => (A = B)) <=> ((~(issue(A) = issue(B))) | (A = B)))),
% 0.16/0.48 inference(bind,[status(th)],[])).
% 0.16/0.48 tff(5,plain,
% 0.16/0.48 (![A: $i, B: $i] : ((issue(A) = issue(B)) => (A = B)) <=> ![A: $i, B: $i] : ((~(issue(A) = issue(B))) | (A = B))),
% 0.16/0.48 inference(quant_intro,[status(thm)],[4])).
% 0.16/0.48 tff(6,axiom,(![A: $i, B: $i] : ((issue(A) = issue(B)) => (A = B))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','issue_injective')).
% 0.16/0.48 tff(7,plain,
% 0.16/0.48 (![A: $i, B: $i] : ((~(issue(A) = issue(B))) | (A = B))),
% 0.16/0.48 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.16/0.48 tff(8,plain,
% 0.16/0.48 (![A: $i, B: $i] : ((~(issue(A) = issue(B))) | (A = B))),
% 0.16/0.48 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.16/0.48 tff(9,plain,(
% 0.16/0.48 ![A: $i, B: $i] : ((~(issue(A) = issue(B))) | (A = B))),
% 0.16/0.48 inference(skolemize,[status(sab)],[8])).
% 0.16/0.48 tff(10,plain,
% 0.16/0.48 (![Xk!0: $i] : (inj_0(issue(Xk!0)) = Xk!0)),
% 0.16/0.48 inference(modus_ponens,[status(thm)],[9, 2])).
% 0.16/0.48 tff(11,plain,
% 0.16/0.48 (![Xk!0: $i] : (inj_0(issue(Xk!0)) = Xk!0)),
% 0.16/0.48 inference(modus_ponens,[status(thm)],[10, 1])).
% 0.16/0.48 tff(12,plain,
% 0.16/0.48 ((~![Xk!0: $i] : (inj_0(issue(Xk!0)) = Xk!0)) | (inj_0(issue(pi2)) = pi2)),
% 0.16/0.48 inference(quant_inst,[status(thm)],[])).
% 0.16/0.48 tff(13,plain,
% 0.16/0.48 (inj_0(issue(pi2)) = pi2),
% 0.16/0.48 inference(unit_resolution,[status(thm)],[12, 11])).
% 0.16/0.48 tff(14,plain,
% 0.16/0.48 ((issue(pi1) = issue(pi2)) <=> (issue(pi1) = issue(pi2))),
% 0.16/0.48 inference(rewrite,[status(thm)],[])).
% 0.16/0.48 tff(15,plain,
% 0.16/0.48 ((~(~(issue(pi1) = issue(pi2)))) <=> (issue(pi1) = issue(pi2))),
% 0.16/0.48 inference(rewrite,[status(thm)],[])).
% 0.16/0.48 tff(16,axiom,(~(~(issue(pi1) = issue(pi2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','conjecture')).
% 0.16/0.48 tff(17,plain,
% 0.16/0.48 (issue(pi1) = issue(pi2)),
% 0.16/0.48 inference(modus_ponens,[status(thm)],[16, 15])).
% 0.16/0.48 tff(18,plain,
% 0.16/0.48 (issue(pi1) = issue(pi2)),
% 0.16/0.48 inference(modus_ponens,[status(thm)],[17, 14])).
% 0.16/0.48 tff(19,plain,
% 0.16/0.48 (issue(pi2) = issue(pi1)),
% 0.16/0.48 inference(symmetry,[status(thm)],[18])).
% 0.16/0.48 tff(20,plain,
% 0.16/0.48 (inj_0(issue(pi2)) = inj_0(issue(pi1))),
% 0.16/0.48 inference(monotonicity,[status(thm)],[19])).
% 0.16/0.48 tff(21,plain,
% 0.16/0.48 (inj_0(issue(pi1)) = inj_0(issue(pi2))),
% 0.16/0.48 inference(symmetry,[status(thm)],[20])).
% 0.16/0.48 tff(22,plain,
% 0.16/0.48 ((~![Xk!0: $i] : (inj_0(issue(Xk!0)) = Xk!0)) | (inj_0(issue(pi1)) = pi1)),
% 0.16/0.48 inference(quant_inst,[status(thm)],[])).
% 0.16/0.48 tff(23,plain,
% 0.16/0.48 (inj_0(issue(pi1)) = pi1),
% 0.16/0.48 inference(unit_resolution,[status(thm)],[22, 11])).
% 0.16/0.48 tff(24,plain,
% 0.16/0.48 (pi1 = inj_0(issue(pi1))),
% 0.16/0.48 inference(symmetry,[status(thm)],[23])).
% 0.16/0.48 tff(25,plain,
% 0.16/0.48 (pi1 = pi2),
% 0.16/0.48 inference(transitivity,[status(thm)],[24, 21, 13])).
% 0.16/0.48 tff(26,plain,
% 0.16/0.48 ((~(pi1 = pi2)) <=> (~(pi1 = pi2))),
% 0.16/0.48 inference(rewrite,[status(thm)],[])).
% 0.16/0.48 tff(27,axiom,(~(pi1 = pi2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pi1_neq_pi2')).
% 0.16/0.48 tff(28,plain,
% 0.16/0.48 (~(pi1 = pi2)),
% 0.16/0.48 inference(modus_ponens,[status(thm)],[27, 26])).
% 0.16/0.48 tff(29,plain,
% 0.16/0.48 ($false),
% 0.16/0.48 inference(unit_resolution,[status(thm)],[28, 25])).
% 0.16/0.48 % SZS output end Proof
% 0.16/0.48 % E exiting
%------------------------------------------------------------------------------