%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : MGT071+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n001.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:11 AM UTC 2026
% Result : Theorem 0.14s 0.43s
% Output : Proof 0.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT071+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 7 14:00:24 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.43 % SZS status Theorem
% 0.14/0.43 % SZS output start Proof
% 0.14/0.43 tff(in_closed_type, type, (
% 0.14/0.43 in_closed: ( $i * $i * $i ) > $o)).
% 0.14/0.43 tff(n15_type, type, (
% 0.14/0.43 n15: $i)).
% 0.14/0.43 tff(n10_type, type, (
% 0.14/0.43 n10: $i)).
% 0.14/0.43 tff(n5_type, type, (
% 0.14/0.43 n5: $i)).
% 0.14/0.43 tff(n0_type, type, (
% 0.14/0.43 n0: $i)).
% 0.14/0.43 tff(axis_conflict_type, type, (
% 0.14/0.43 axis_conflict: ( $i * $i * $i * $i ) > $o)).
% 0.14/0.43 tff(tptp_fun_X_0_type, type, (
% 0.14/0.43 tptp_fun_X_0: ( $i * $i * $i * $i ) > $i)).
% 0.14/0.43 tff(tptp_fun_X_2_type, type, (
% 0.14/0.43 tptp_fun_X_2: $i)).
% 0.14/0.43 tff(1,plain,
% 0.14/0.43 (^[I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : refl((~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))) <=> (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))))),
% 0.14/0.43 inference(bind,[status(th)],[])).
% 0.14/0.43 tff(2,plain,
% 0.14/0.43 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))),
% 0.14/0.43 inference(quant_intro,[status(thm)],[1])).
% 0.14/0.43 tff(3,plain,
% 0.14/0.43 (^[I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : rewrite((~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))) <=> (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))))),
% 0.14/0.43 inference(bind,[status(th)],[])).
% 0.14/0.43 tff(4,plain,
% 0.14/0.43 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))),
% 0.14/0.43 inference(quant_intro,[status(thm)],[3])).
% 0.14/0.43 tff(5,plain,
% 0.14/0.43 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))),
% 0.14/0.43 inference(transitivity,[status(thm)],[4, 2])).
% 0.14/0.43 tff(6,plain,
% 0.14/0.43 (^[I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : trans(monotonicity(rewrite(((in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi) & in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)) | axis_conflict(I1lo, I1hi, I2lo, I2hi)) <=> ((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))), trans(monotonicity(quant_intro(proof_bind(^[X: $i] : trans(monotonicity(rewrite((in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)) <=> (~((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))), ((~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))) <=> (~(~((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))), rewrite((~(~((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))) <=> ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))), ((~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))) <=> ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))), (![X: $i] : (~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))) <=> ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))), ((![X: $i] : (~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))) | (~axis_conflict(I1lo, I1hi, I2lo, I2hi))) <=> (![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))) | (~axis_conflict(I1lo, I1hi, I2lo, I2hi))))), rewrite((![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))) | (~axis_conflict(I1lo, I1hi, I2lo, I2hi))) <=> ((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))), ((![X: $i] : (~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))) | (~axis_conflict(I1lo, I1hi, I2lo, I2hi))) <=> ((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))), ((((in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi) & in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)) | axis_conflict(I1lo, I1hi, I2lo, I2hi)) & (![X: $i] : (~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))) | (~axis_conflict(I1lo, I1hi, I2lo, I2hi)))) <=> (((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi)) & ((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))), rewrite((((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi)) & ((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))) <=> (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))), ((((in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi) & in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)) | axis_conflict(I1lo, I1hi, I2lo, I2hi)) & (![X: $i] : (~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))) | (~axis_conflict(I1lo, I1hi, I2lo, I2hi)))) <=> (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))))),
% 0.14/0.43 inference(bind,[status(th)],[])).
% 0.14/0.43 tff(7,plain,
% 0.14/0.43 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (((in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi) & in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)) | axis_conflict(I1lo, I1hi, I2lo, I2hi)) & (![X: $i] : (~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))) | (~axis_conflict(I1lo, I1hi, I2lo, I2hi)))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))),
% 0.14/0.43 inference(quant_intro,[status(thm)],[6])).
% 0.14/0.43 tff(8,plain,
% 0.14/0.43 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~(?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)) <=> axis_conflict(I1lo, I1hi, I2lo, I2hi))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~(?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)) <=> axis_conflict(I1lo, I1hi, I2lo, I2hi)))),
% 0.14/0.43 inference(rewrite,[status(thm)],[])).
% 0.14/0.43 tff(9,plain,
% 0.14/0.43 (^[I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : trans(trans(monotonicity(rewrite((~?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))) <=> (~?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)))), ((axis_conflict(I1lo, I1hi, I2lo, I2hi) <=> (~?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)))) <=> (axis_conflict(I1lo, I1hi, I2lo, I2hi) <=> (~?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)))))), rewrite((axis_conflict(I1lo, I1hi, I2lo, I2hi) <=> (~?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)))) <=> (~(?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)) <=> axis_conflict(I1lo, I1hi, I2lo, I2hi)))), ((axis_conflict(I1lo, I1hi, I2lo, I2hi) <=> (~?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)))) <=> (~(?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)) <=> axis_conflict(I1lo, I1hi, I2lo, I2hi))))), rewrite((~(?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)) <=> axis_conflict(I1lo, I1hi, I2lo, I2hi))) <=> (~(?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)) <=> axis_conflict(I1lo, I1hi, I2lo, I2hi)))), ((axis_conflict(I1lo, I1hi, I2lo, I2hi) <=> (~?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)))) <=> (~(?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)) <=> axis_conflict(I1lo, I1hi, I2lo, I2hi)))))),
% 0.14/0.43 inference(bind,[status(th)],[])).
% 0.14/0.43 tff(10,plain,
% 0.14/0.43 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (axis_conflict(I1lo, I1hi, I2lo, I2hi) <=> (~?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~(?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)) <=> axis_conflict(I1lo, I1hi, I2lo, I2hi)))),
% 0.14/0.43 inference(quant_intro,[status(thm)],[9])).
% 0.14/0.43 tff(11,axiom,(![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (axis_conflict(I1lo, I1hi, I2lo, I2hi) <=> (~?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))))), file('/export/starexec/sandbox/benchmark/Axioms/MGT002+2.ax','axis_conflict_def')).
% 0.14/0.43 tff(12,plain,
% 0.14/0.43 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~(?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)) <=> axis_conflict(I1lo, I1hi, I2lo, I2hi)))),
% 0.14/0.43 inference(modus_ponens,[status(thm)],[11, 10])).
% 0.14/0.43 tff(13,plain,
% 0.14/0.43 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~(?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)) <=> axis_conflict(I1lo, I1hi, I2lo, I2hi)))),
% 0.14/0.43 inference(modus_ponens,[status(thm)],[12, 8])).
% 0.14/0.43 tff(14,plain,(
% 0.14/0.43 ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (((in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi) & in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)) | axis_conflict(I1lo, I1hi, I2lo, I2hi)) & (![X: $i] : (~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))) | (~axis_conflict(I1lo, I1hi, I2lo, I2hi))))),
% 0.14/0.43 inference(skolemize,[status(sab)],[13])).
% 0.14/0.43 tff(15,plain,
% 0.14/0.43 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))),
% 0.14/0.43 inference(modus_ponens,[status(thm)],[14, 7])).
% 0.14/0.43 tff(16,plain,
% 0.14/0.43 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))),
% 0.14/0.43 inference(modus_ponens,[status(thm)],[15, 5])).
% 0.14/0.43 tff(17,plain,
% 0.14/0.43 (((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15))))) | (~((~((~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n0, n5)) | (~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n10, n15)))) | axis_conflict(n0, n5, n10, n15)))))) <=> ((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15))))) | (~((~((~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n0, n5)) | (~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n10, n15)))) | axis_conflict(n0, n5, n10, n15))))))),
% 0.14/0.43 inference(rewrite,[status(thm)],[])).
% 0.14/0.43 tff(18,plain,
% 0.14/0.43 ((~((~((~((~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n0, n5)) | (~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n10, n15)))) | axis_conflict(n0, n5, n10, n15))) | (~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15))))))) <=> (~((~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15))))) | (~((~((~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n0, n5)) | (~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n10, n15)))) | axis_conflict(n0, n5, n10, n15)))))),
% 0.14/0.43 inference(rewrite,[status(thm)],[])).
% 0.14/0.43 tff(19,plain,
% 0.14/0.43 (((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~((~((~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n0, n5)) | (~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n10, n15)))) | axis_conflict(n0, n5, n10, n15))) | (~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15)))))))) <=> ((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15))))) | (~((~((~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n0, n5)) | (~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n10, n15)))) | axis_conflict(n0, n5, n10, n15))))))),
% 0.14/0.43 inference(monotonicity,[status(thm)],[18])).
% 0.14/0.43 tff(20,plain,
% 0.14/0.43 (((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~((~((~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n0, n5)) | (~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n10, n15)))) | axis_conflict(n0, n5, n10, n15))) | (~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15)))))))) <=> ((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15))))) | (~((~((~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n0, n5)) | (~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n10, n15)))) | axis_conflict(n0, n5, n10, n15))))))),
% 0.14/0.44 inference(transitivity,[status(thm)],[19, 17])).
% 0.14/0.44 tff(21,plain,
% 0.14/0.44 ((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~((~((~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n0, n5)) | (~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n10, n15)))) | axis_conflict(n0, n5, n10, n15))) | (~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15)))))))),
% 0.14/0.44 inference(quant_inst,[status(thm)],[])).
% 0.14/0.44 tff(22,plain,
% 0.14/0.44 ((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) | axis_conflict(I1lo, I1hi, I2lo, I2hi))) | (~((~axis_conflict(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15))))) | (~((~((~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n0, n5)) | (~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n10, n15)))) | axis_conflict(n0, n5, n10, n15)))))),
% 0.14/0.44 inference(modus_ponens,[status(thm)],[21, 20])).
% 0.14/0.44 tff(23,plain,
% 0.14/0.44 (~((~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15))))) | (~((~((~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n0, n5)) | (~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n10, n15)))) | axis_conflict(n0, n5, n10, n15))))),
% 0.14/0.44 inference(unit_resolution,[status(thm)],[22, 16])).
% 0.14/0.44 tff(24,plain,
% 0.14/0.44 (((~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15))))) | (~((~((~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n0, n5)) | (~in_closed(tptp_fun_X_0(n15, n10, n5, n0), n10, n15)))) | axis_conflict(n0, n5, n10, n15)))) | ((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15))))),
% 0.14/0.44 inference(tautology,[status(thm)],[])).
% 0.14/0.44 tff(25,plain,
% 0.14/0.44 ((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15)))),
% 0.14/0.44 inference(unit_resolution,[status(thm)],[24, 23])).
% 0.14/0.44 tff(26,plain,
% 0.14/0.44 (axis_conflict(n0, n5, n10, n15) <=> axis_conflict(n0, n5, n10, n15)),
% 0.14/0.44 inference(rewrite,[status(thm)],[])).
% 0.14/0.44 tff(27,axiom,(axis_conflict(n0, n5, n10, n15)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','conflict_hyp')).
% 0.14/0.44 tff(28,plain,
% 0.14/0.44 (axis_conflict(n0, n5, n10, n15)),
% 0.14/0.44 inference(modus_ponens,[status(thm)],[27, 26])).
% 0.14/0.44 tff(29,plain,
% 0.14/0.44 ((~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15))))) | (~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15)))),
% 0.14/0.44 inference(tautology,[status(thm)],[])).
% 0.14/0.44 tff(30,plain,
% 0.14/0.44 ((~((~axis_conflict(n0, n5, n10, n15)) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15))))) | ![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15)))),
% 0.14/0.44 inference(unit_resolution,[status(thm)],[29, 28])).
% 0.14/0.44 tff(31,plain,
% 0.14/0.44 (![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15)))),
% 0.14/0.44 inference(unit_resolution,[status(thm)],[30, 25])).
% 0.14/0.44 tff(32,plain,
% 0.14/0.44 (?[X: $i] : (in_closed(X, n0, n5) & in_closed(X, n10, n15)) <=> ?[X: $i] : (in_closed(X, n0, n5) & in_closed(X, n10, n15))),
% 0.14/0.44 inference(rewrite,[status(thm)],[])).
% 0.14/0.44 tff(33,plain,
% 0.14/0.44 ((~(~?[X: $i] : (in_closed(X, n0, n5) & in_closed(X, n10, n15)))) <=> ?[X: $i] : (in_closed(X, n0, n5) & in_closed(X, n10, n15))),
% 0.14/0.44 inference(rewrite,[status(thm)],[])).
% 0.14/0.44 tff(34,plain,
% 0.14/0.44 ((~?[X: $i] : (in_closed(X, n0, n5) & in_closed(X, n10, n15))) <=> (~?[X: $i] : (in_closed(X, n0, n5) & in_closed(X, n10, n15)))),
% 0.14/0.44 inference(rewrite,[status(thm)],[])).
% 0.14/0.44 tff(35,plain,
% 0.14/0.44 ((~(~?[X: $i] : (in_closed(X, n0, n5) & in_closed(X, n10, n15)))) <=> (~(~?[X: $i] : (in_closed(X, n0, n5) & in_closed(X, n10, n15))))),
% 0.14/0.44 inference(monotonicity,[status(thm)],[34])).
% 0.14/0.44 tff(36,plain,
% 0.14/0.44 ((~(~?[X: $i] : (in_closed(X, n0, n5) & in_closed(X, n10, n15)))) <=> ?[X: $i] : (in_closed(X, n0, n5) & in_closed(X, n10, n15))),
% 0.14/0.44 inference(transitivity,[status(thm)],[35, 33])).
% 0.14/0.44 tff(37,axiom,(~(~?[X: $i] : (in_closed(X, n0, n5) & in_closed(X, n10, n15)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','no_false_conflict')).
% 0.14/0.44 tff(38,plain,
% 0.14/0.44 (?[X: $i] : (in_closed(X, n0, n5) & in_closed(X, n10, n15))),
% 0.14/0.44 inference(modus_ponens,[status(thm)],[37, 36])).
% 0.14/0.44 tff(39,plain,
% 0.14/0.44 (?[X: $i] : (in_closed(X, n0, n5) & in_closed(X, n10, n15))),
% 0.14/0.44 inference(modus_ponens,[status(thm)],[38, 32])).
% 0.14/0.44 tff(40,plain,(
% 0.14/0.44 in_closed(X!2, n0, n5) & in_closed(X!2, n10, n15)),
% 0.14/0.44 inference(skolemize,[status(sab)],[39])).
% 0.14/0.44 tff(41,plain,
% 0.14/0.44 (in_closed(X!2, n10, n15)),
% 0.14/0.44 inference(and_elim,[status(thm)],[40])).
% 0.14/0.44 tff(42,plain,
% 0.14/0.44 (in_closed(X!2, n0, n5)),
% 0.14/0.44 inference(and_elim,[status(thm)],[40])).
% 0.14/0.44 tff(43,plain,
% 0.14/0.44 (((~![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15)))) | ((~in_closed(X!2, n0, n5)) | (~in_closed(X!2, n10, n15)))) <=> ((~![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15)))) | (~in_closed(X!2, n0, n5)) | (~in_closed(X!2, n10, n15)))),
% 0.14/0.44 inference(rewrite,[status(thm)],[])).
% 0.14/0.44 tff(44,plain,
% 0.14/0.44 ((~![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15)))) | ((~in_closed(X!2, n0, n5)) | (~in_closed(X!2, n10, n15)))),
% 0.14/0.44 inference(quant_inst,[status(thm)],[])).
% 0.14/0.44 tff(45,plain,
% 0.14/0.44 ((~![X: $i] : ((~in_closed(X, n0, n5)) | (~in_closed(X, n10, n15)))) | (~in_closed(X!2, n0, n5)) | (~in_closed(X!2, n10, n15))),
% 0.14/0.44 inference(modus_ponens,[status(thm)],[44, 43])).
% 0.14/0.44 tff(46,plain,
% 0.14/0.44 ($false),
% 0.14/0.44 inference(unit_resolution,[status(thm)],[45, 42, 41, 31])).
% 0.14/0.44 % SZS output end Proof
% 0.14/0.44 % E exiting
%------------------------------------------------------------------------------