%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : NUM858+1 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n006.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:22:15 AM UTC 2025
% Result : Theorem 0.18s 0.37s
% Output : Proof 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : NUM858+1 : TPTP v9.0.0. Released v4.1.0.
% 0.10/0.11 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n006.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri Jun 20 02:02:05 EDT 2025
% 0.11/0.32 % CPUTime :
% 0.18/0.37 % SZS status Theorem
% 0.18/0.37 % SZS output start Proof
% 0.18/0.37 tff(max_type, type, (
% 0.18/0.37 max: ( $i * $i ) > $i)).
% 0.18/0.37 tff(tptp_fun_Y_3_type, type, (
% 0.18/0.37 tptp_fun_Y_3: $i)).
% 0.18/0.37 tff(tptp_fun_X_4_type, type, (
% 0.18/0.37 tptp_fun_X_4: $i)).
% 0.18/0.37 tff(tptp_fun_Z_2_type, type, (
% 0.18/0.37 tptp_fun_Z_2: $i)).
% 0.18/0.37 tff(lesseq_type, type, (
% 0.18/0.37 lesseq: ( $i * $i ) > $o)).
% 0.18/0.37 tff(tptp_fun_Z_0_type, type, (
% 0.18/0.37 tptp_fun_Z_0: ( $i * $i * $i ) > $i)).
% 0.18/0.37 tff(model_max_type, type, (
% 0.18/0.37 model_max: ( $i * $i * $i ) > $o)).
% 0.18/0.37 tff(minsol_model_max_type, type, (
% 0.18/0.37 minsol_model_max: ( $i * $i * $i ) > $o)).
% 0.18/0.37 tff(minsol_model_ub_type, type, (
% 0.18/0.37 minsol_model_ub: ( $i * $i * $i ) > $o)).
% 0.18/0.37 tff(ub_type, type, (
% 0.18/0.37 ub: ( $i * $i * $i ) > $o)).
% 0.18/0.37 tff(model_ub_type, type, (
% 0.18/0.37 model_ub: ( $i * $i * $i ) > $o)).
% 0.18/0.37 tff(tptp_fun_Z_1_type, type, (
% 0.18/0.37 tptp_fun_Z_1: ( $i * $i * $i ) > $i)).
% 0.18/0.37 tff(1,assumption,(Z!2 = max(X!4, Y!3)), introduced(assumption)).
% 0.18/0.37 tff(2,plain,
% 0.18/0.37 (max(X!4, Y!3) = Z!2),
% 0.18/0.37 inference(symmetry,[status(thm)],[1])).
% 0.18/0.37 tff(3,plain,
% 0.18/0.37 (^[X: $i, Y: $i, N: $i] : refl((model_max(X, Y, N) <=> (N = max(X, Y))) <=> (model_max(X, Y, N) <=> (N = max(X, Y))))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(4,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (model_max(X, Y, N) <=> (N = max(X, Y))) <=> ![X: $i, Y: $i, N: $i] : (model_max(X, Y, N) <=> (N = max(X, Y)))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[3])).
% 0.18/0.37 tff(5,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (model_max(X, Y, N) <=> (N = max(X, Y))) <=> ![X: $i, Y: $i, N: $i] : (model_max(X, Y, N) <=> (N = max(X, Y)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(6,axiom,(![X: $i, Y: $i, N: $i] : (model_max(X, Y, N) <=> (N = max(X, Y)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','model_max_1')).
% 0.18/0.37 tff(7,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (model_max(X, Y, N) <=> (N = max(X, Y)))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.18/0.37 tff(8,plain,(
% 0.18/0.37 ![X: $i, Y: $i, N: $i] : (model_max(X, Y, N) <=> (N = max(X, Y)))),
% 0.18/0.37 inference(skolemize,[status(sab)],[7])).
% 0.18/0.37 tff(9,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (model_max(X, Y, N) <=> (N = max(X, Y)))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[8, 4])).
% 0.18/0.37 tff(10,plain,
% 0.18/0.37 ((~![X: $i, Y: $i, N: $i] : (model_max(X, Y, N) <=> (N = max(X, Y)))) | (model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4)) <=> (tptp_fun_Z_0(Z!2, Y!3, X!4) = max(X!4, Y!3)))),
% 0.18/0.37 inference(quant_inst,[status(thm)],[])).
% 0.18/0.37 tff(11,plain,
% 0.18/0.37 (model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4)) <=> (tptp_fun_Z_0(Z!2, Y!3, X!4) = max(X!4, Y!3))),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[10, 9])).
% 0.18/0.37 tff(12,assumption,(~(model_max(X!4, Y!3, Z!2) <=> (Z!2 = max(X!4, Y!3)))), introduced(assumption)).
% 0.18/0.37 tff(13,plain,
% 0.18/0.37 ((~![X: $i, Y: $i, N: $i] : (model_max(X, Y, N) <=> (N = max(X, Y)))) | (model_max(X!4, Y!3, Z!2) <=> (Z!2 = max(X!4, Y!3)))),
% 0.18/0.37 inference(quant_inst,[status(thm)],[])).
% 0.18/0.37 tff(14,plain,
% 0.18/0.37 ($false),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[13, 9, 12])).
% 0.18/0.37 tff(15,plain,(model_max(X!4, Y!3, Z!2) <=> (Z!2 = max(X!4, Y!3))), inference(lemma,lemma(discharge,[]))).
% 0.18/0.37 tff(16,plain,
% 0.18/0.37 ((~(model_max(X!4, Y!3, Z!2) <=> (Z!2 = max(X!4, Y!3)))) | model_max(X!4, Y!3, Z!2) | (~(Z!2 = max(X!4, Y!3)))),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(17,plain,
% 0.18/0.37 (model_max(X!4, Y!3, Z!2)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[16, 1, 15])).
% 0.18/0.37 tff(18,plain,
% 0.18/0.37 (model_max(X!4, Y!3, Z!2) <=> (Z!2 = max(X!4, Y!3))),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[13, 9])).
% 0.18/0.37 tff(19,assumption,(~minsol_model_ub(X!4, Y!3, Z!2)), introduced(assumption)).
% 0.18/0.37 tff(20,plain,
% 0.18/0.37 ((~(minsol_model_ub(X!4, Y!3, Z!2) <=> minsol_model_max(X!4, Y!3, Z!2))) <=> (~(minsol_model_ub(X!4, Y!3, Z!2) <=> minsol_model_max(X!4, Y!3, Z!2)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(21,plain,
% 0.18/0.37 ((~![X: $i, Y: $i, Z: $i] : (minsol_model_ub(X, Y, Z) <=> minsol_model_max(X, Y, Z))) <=> (~![X: $i, Y: $i, Z: $i] : (minsol_model_ub(X, Y, Z) <=> minsol_model_max(X, Y, Z)))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(22,axiom,(~![X: $i, Y: $i, Z: $i] : (minsol_model_ub(X, Y, Z) <=> minsol_model_max(X, Y, Z))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','max_is_ub_1')).
% 0.18/0.37 tff(23,plain,
% 0.18/0.37 (~![X: $i, Y: $i, Z: $i] : (minsol_model_ub(X, Y, Z) <=> minsol_model_max(X, Y, Z))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[22, 21])).
% 0.18/0.37 tff(24,plain,
% 0.18/0.37 (~![X: $i, Y: $i, Z: $i] : (minsol_model_ub(X, Y, Z) <=> minsol_model_max(X, Y, Z))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[23, 21])).
% 0.18/0.37 tff(25,plain,
% 0.18/0.37 (~![X: $i, Y: $i, Z: $i] : (minsol_model_ub(X, Y, Z) <=> minsol_model_max(X, Y, Z))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[24, 21])).
% 0.18/0.37 tff(26,plain,
% 0.18/0.37 (~![X: $i, Y: $i, Z: $i] : (minsol_model_ub(X, Y, Z) <=> minsol_model_max(X, Y, Z))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[25, 21])).
% 0.18/0.37 tff(27,plain,(
% 0.18/0.37 ~(minsol_model_ub(X!4, Y!3, Z!2) <=> minsol_model_max(X!4, Y!3, Z!2))),
% 0.18/0.37 inference(skolemize,[status(sab)],[26])).
% 0.18/0.37 tff(28,plain,
% 0.18/0.37 (~(minsol_model_ub(X!4, Y!3, Z!2) <=> minsol_model_max(X!4, Y!3, Z!2))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[27, 20])).
% 0.18/0.37 tff(29,plain,
% 0.18/0.37 ((minsol_model_ub(X!4, Y!3, Z!2) <=> minsol_model_max(X!4, Y!3, Z!2)) | minsol_model_ub(X!4, Y!3, Z!2) | minsol_model_max(X!4, Y!3, Z!2)),
% 0.18/0.37 inference(tautology,[status(thm)],[])).
% 0.18/0.37 tff(30,plain,
% 0.18/0.37 (minsol_model_ub(X!4, Y!3, Z!2) | minsol_model_max(X!4, Y!3, Z!2)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[29, 28])).
% 0.18/0.37 tff(31,plain,
% 0.18/0.37 (minsol_model_max(X!4, Y!3, Z!2)),
% 0.18/0.37 inference(unit_resolution,[status(thm)],[30, 19])).
% 0.18/0.37 tff(32,plain,
% 0.18/0.37 (^[X: $i, Y: $i, N: $i] : rewrite((~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))))) <=> (~((~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))) | (~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))))))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(33,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))))) <=> ![X: $i, Y: $i, N: $i] : (~((~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))) | (~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))))))))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[32])).
% 0.18/0.37 tff(34,plain,
% 0.18/0.37 (^[X: $i, Y: $i, N: $i] : refl((~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))))) <=> (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))))))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(35,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))))) <=> ![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X))))))))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[34])).
% 0.18/0.37 tff(36,plain,
% 0.18/0.37 (^[X: $i, Y: $i, N: $i] : rewrite((~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))))) <=> (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))))))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(37,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))))) <=> ![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X))))))))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[36])).
% 0.18/0.37 tff(38,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))))) <=> ![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X))))))))),
% 0.18/0.37 inference(transitivity,[status(thm)],[37, 35])).
% 0.18/0.37 tff(39,plain,
% 0.18/0.37 (^[X: $i, Y: $i, N: $i] : trans(monotonicity(rewrite(((~minsol_model_max(X, Y, N)) | (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))) <=> ((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))), rewrite((minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X))))) <=> (minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))), ((((~minsol_model_max(X, Y, N)) | (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))) <=> (((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))))) & (minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))))), rewrite((((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))))) & (minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))) <=> (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X))))))))), ((((~minsol_model_max(X, Y, N)) | (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))) <=> (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X))))))))))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(40,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (((~minsol_model_max(X, Y, N)) | (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))) <=> ![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X))))))))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[39])).
% 0.18/0.37 tff(41,plain,
% 0.18/0.37 (^[X: $i, Y: $i, N: $i] : rewrite((((~minsol_model_max(X, Y, N)) | (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_max(X, Y, N) | ((~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X))))))) <=> (((~minsol_model_max(X, Y, N)) | (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(42,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (((~minsol_model_max(X, Y, N)) | (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_max(X, Y, N) | ((~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X))))))) <=> ![X: $i, Y: $i, N: $i] : (((~minsol_model_max(X, Y, N)) | (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X))))))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[41])).
% 0.18/0.37 tff(43,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (minsol_model_max(X, Y, N) <=> (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))) <=> ![X: $i, Y: $i, N: $i] : (minsol_model_max(X, Y, N) <=> (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))),
% 0.18/0.37 inference(rewrite,[status(thm)],[])).
% 0.18/0.37 tff(44,plain,
% 0.18/0.37 (^[X: $i, Y: $i, N: $i] : rewrite((minsol_model_max(X, Y, N) <=> (model_max(X, Y, N) & ![Z: $i] : (model_max(X, Y, Z) => lesseq(N, Z)))) <=> (minsol_model_max(X, Y, N) <=> (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))))),
% 0.18/0.37 inference(bind,[status(th)],[])).
% 0.18/0.37 tff(45,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (minsol_model_max(X, Y, N) <=> (model_max(X, Y, N) & ![Z: $i] : (model_max(X, Y, Z) => lesseq(N, Z)))) <=> ![X: $i, Y: $i, N: $i] : (minsol_model_max(X, Y, N) <=> (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))),
% 0.18/0.37 inference(quant_intro,[status(thm)],[44])).
% 0.18/0.37 tff(46,axiom,(![X: $i, Y: $i, N: $i] : (minsol_model_max(X, Y, N) <=> (model_max(X, Y, N) & ![Z: $i] : (model_max(X, Y, Z) => lesseq(N, Z))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','minsol_model_max')).
% 0.18/0.37 tff(47,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (minsol_model_max(X, Y, N) <=> (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[46, 45])).
% 0.18/0.37 tff(48,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (minsol_model_max(X, Y, N) <=> (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[47, 43])).
% 0.18/0.37 tff(49,plain,(
% 0.18/0.37 ![X: $i, Y: $i, N: $i] : (((~minsol_model_max(X, Y, N)) | (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_max(X, Y, N) | ((~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))))),
% 0.18/0.37 inference(skolemize,[status(sab)],[48])).
% 0.18/0.37 tff(50,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (((~minsol_model_max(X, Y, N)) | (model_max(X, Y, N) & ![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X))))))),
% 0.18/0.37 inference(modus_ponens,[status(thm)],[49, 42])).
% 0.18/0.37 tff(51,plain,
% 0.18/0.37 (![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X))))))))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[50, 40])).
% 0.18/0.38 tff(52,plain,
% 0.18/0.38 (![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X))))))))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[51, 38])).
% 0.18/0.38 tff(53,plain,
% 0.18/0.38 (![X: $i, Y: $i, N: $i] : (~((~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))) | (~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))))))))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[52, 33])).
% 0.18/0.38 tff(54,plain,
% 0.18/0.38 ((~![X: $i, Y: $i, N: $i] : (~((~(minsol_model_max(X, Y, N) | (~model_max(X, Y, N)) | (~((~model_max(X, Y, tptp_fun_Z_0(N, Y, X))) | lesseq(N, tptp_fun_Z_0(N, Y, X)))))) | (~((~minsol_model_max(X, Y, N)) | (~((~model_max(X, Y, N)) | (~![Z: $i] : ((~model_max(X, Y, Z)) | lesseq(N, Z)))))))))) | (~((~(minsol_model_max(X!4, Y!3, Z!2) | (~model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4)))))) | (~((~minsol_model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z)))))))))),
% 0.18/0.38 inference(quant_inst,[status(thm)],[])).
% 0.18/0.38 tff(55,plain,
% 0.18/0.38 (~((~(minsol_model_max(X!4, Y!3, Z!2) | (~model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4)))))) | (~((~minsol_model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z))))))))),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[54, 53])).
% 0.18/0.38 tff(56,plain,
% 0.18/0.38 (((~(minsol_model_max(X!4, Y!3, Z!2) | (~model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4)))))) | (~((~minsol_model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z)))))))) | ((~minsol_model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z))))))),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(57,plain,
% 0.18/0.38 ((~minsol_model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z)))))),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[56, 55])).
% 0.18/0.38 tff(58,plain,
% 0.18/0.38 ((~((~minsol_model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z))))))) | (~minsol_model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z)))))),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(59,plain,
% 0.18/0.38 ((~minsol_model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z)))))),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[58, 57])).
% 0.18/0.38 tff(60,plain,
% 0.18/0.38 (~((~model_max(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z))))),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[59, 31])).
% 0.18/0.38 tff(61,plain,
% 0.18/0.38 (((~model_max(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z)))) | model_max(X!4, Y!3, Z!2)),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(62,plain,
% 0.18/0.38 (model_max(X!4, Y!3, Z!2)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[61, 60])).
% 0.18/0.38 tff(63,plain,
% 0.18/0.38 ((~(model_max(X!4, Y!3, Z!2) <=> (Z!2 = max(X!4, Y!3)))) | (~model_max(X!4, Y!3, Z!2)) | (Z!2 = max(X!4, Y!3))),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(64,plain,
% 0.18/0.38 ((~(model_max(X!4, Y!3, Z!2) <=> (Z!2 = max(X!4, Y!3)))) | (Z!2 = max(X!4, Y!3))),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[63, 62])).
% 0.18/0.38 tff(65,plain,
% 0.18/0.38 (Z!2 = max(X!4, Y!3)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[64, 18])).
% 0.18/0.38 tff(66,plain,
% 0.18/0.38 (((~model_max(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z)))) | ![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z))),
% 0.18/0.38 inference(tautology,[status(thm)],[])).
% 0.18/0.38 tff(67,plain,
% 0.18/0.38 (![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z))),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[66, 60])).
% 0.18/0.38 tff(68,plain,
% 0.18/0.38 (((~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | ((~model_max(X!4, Y!3, Z!2)) | lesseq(Z!2, Z!2))) <=> ((~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | (~model_max(X!4, Y!3, Z!2)) | lesseq(Z!2, Z!2))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(69,plain,
% 0.18/0.38 ((~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | ((~model_max(X!4, Y!3, Z!2)) | lesseq(Z!2, Z!2))),
% 0.18/0.38 inference(quant_inst,[status(thm)],[])).
% 0.18/0.38 tff(70,plain,
% 0.18/0.38 ((~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | (~model_max(X!4, Y!3, Z!2)) | lesseq(Z!2, Z!2)),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[69, 68])).
% 0.18/0.38 tff(71,plain,
% 0.18/0.38 (lesseq(Z!2, Z!2)),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[70, 62, 67])).
% 0.18/0.38 tff(72,plain,
% 0.18/0.38 (^[X: $i, Y: $i, Z: $i] : refl((~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z))) <=> (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z))))),
% 0.18/0.38 inference(bind,[status(th)],[])).
% 0.18/0.38 tff(73,plain,
% 0.18/0.38 (![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z))) <=> ![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))),
% 0.18/0.38 inference(quant_intro,[status(thm)],[72])).
% 0.18/0.38 tff(74,plain,
% 0.18/0.38 (^[X: $i, Y: $i, Z: $i] : trans(trans(monotonicity(rewrite((lesseq(X, Z) & lesseq(Y, Z)) <=> (~((~lesseq(Y, Z)) | (~lesseq(X, Z))))), ((ub(X, Y, Z) <=> (lesseq(X, Z) & lesseq(Y, Z))) <=> (ub(X, Y, Z) <=> (~((~lesseq(Y, Z)) | (~lesseq(X, Z))))))), rewrite((ub(X, Y, Z) <=> (~((~lesseq(Y, Z)) | (~lesseq(X, Z))))) <=> (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))), ((ub(X, Y, Z) <=> (lesseq(X, Z) & lesseq(Y, Z))) <=> (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z))))), rewrite((~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z))) <=> (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))), ((ub(X, Y, Z) <=> (lesseq(X, Z) & lesseq(Y, Z))) <=> (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))))),
% 0.18/0.38 inference(bind,[status(th)],[])).
% 0.18/0.38 tff(75,plain,
% 0.18/0.38 (![X: $i, Y: $i, Z: $i] : (ub(X, Y, Z) <=> (lesseq(X, Z) & lesseq(Y, Z))) <=> ![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))),
% 0.18/0.38 inference(quant_intro,[status(thm)],[74])).
% 0.18/0.38 tff(76,plain,
% 0.18/0.38 (![X: $i, Y: $i, Z: $i] : (ub(X, Y, Z) <=> (lesseq(X, Z) & lesseq(Y, Z))) <=> ![X: $i, Y: $i, Z: $i] : (ub(X, Y, Z) <=> (lesseq(X, Z) & lesseq(Y, Z)))),
% 0.18/0.38 inference(rewrite,[status(thm)],[])).
% 0.18/0.38 tff(77,axiom,(![X: $i, Y: $i, Z: $i] : (ub(X, Y, Z) <=> (lesseq(X, Z) & lesseq(Y, Z)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','ub')).
% 0.18/0.38 tff(78,plain,
% 0.18/0.38 (![X: $i, Y: $i, Z: $i] : (ub(X, Y, Z) <=> (lesseq(X, Z) & lesseq(Y, Z)))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[77, 76])).
% 0.18/0.38 tff(79,plain,(
% 0.18/0.38 ![X: $i, Y: $i, Z: $i] : (ub(X, Y, Z) <=> (lesseq(X, Z) & lesseq(Y, Z)))),
% 0.18/0.38 inference(skolemize,[status(sab)],[78])).
% 0.18/0.38 tff(80,plain,
% 0.18/0.38 (![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[79, 75])).
% 0.18/0.38 tff(81,plain,
% 0.18/0.38 (![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))),
% 0.18/0.38 inference(modus_ponens,[status(thm)],[80, 73])).
% 0.18/0.38 tff(82,plain,
% 0.18/0.38 ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3)))) <=> ub(X!4, Y!3, max(X!4, Y!3))))),
% 0.18/0.38 inference(quant_inst,[status(thm)],[])).
% 0.18/0.38 tff(83,plain,
% 0.18/0.38 (~(((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3)))) <=> ub(X!4, Y!3, max(X!4, Y!3)))),
% 0.18/0.38 inference(unit_resolution,[status(thm)],[82, 81])).
% 0.18/0.38 tff(84,plain,
% 0.18/0.38 (^[X: $i, Y: $i, N: $i] : refl((model_ub(X, Y, N) <=> ub(X, Y, N)) <=> (model_ub(X, Y, N) <=> ub(X, Y, N)))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(85,plain,
% 0.18/0.39 (![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N)) <=> ![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[84])).
% 0.18/0.39 tff(86,plain,
% 0.18/0.39 (![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N)) <=> ![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(87,axiom,(![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','model_ub_1')).
% 0.18/0.39 tff(88,plain,
% 0.18/0.39 (![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[87, 86])).
% 0.18/0.39 tff(89,plain,(
% 0.18/0.39 ![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))),
% 0.18/0.39 inference(skolemize,[status(sab)],[88])).
% 0.18/0.39 tff(90,plain,
% 0.18/0.39 (![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[89, 85])).
% 0.18/0.39 tff(91,plain,
% 0.18/0.39 ((~![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))) | (model_ub(X!4, Y!3, max(X!4, Y!3)) <=> ub(X!4, Y!3, max(X!4, Y!3)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(92,plain,
% 0.18/0.39 (model_ub(X!4, Y!3, max(X!4, Y!3)) <=> ub(X!4, Y!3, max(X!4, Y!3))),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[91, 90])).
% 0.18/0.39 tff(93,plain,
% 0.18/0.39 (max(X!4, Y!3) = Z!2),
% 0.18/0.39 inference(symmetry,[status(thm)],[65])).
% 0.18/0.39 tff(94,plain,
% 0.18/0.39 (model_ub(X!4, Y!3, max(X!4, Y!3)) <=> model_ub(X!4, Y!3, Z!2)),
% 0.18/0.39 inference(monotonicity,[status(thm)],[93])).
% 0.18/0.39 tff(95,plain,
% 0.18/0.39 (model_ub(X!4, Y!3, Z!2) <=> model_ub(X!4, Y!3, max(X!4, Y!3))),
% 0.18/0.39 inference(symmetry,[status(thm)],[94])).
% 0.18/0.39 tff(96,plain,
% 0.18/0.39 ((~model_ub(X!4, Y!3, Z!2)) <=> (~model_ub(X!4, Y!3, max(X!4, Y!3)))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[95])).
% 0.18/0.39 tff(97,plain,
% 0.18/0.39 (lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)) <=> lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[93])).
% 0.18/0.39 tff(98,plain,
% 0.18/0.39 (((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))))) <=> ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(99,plain,
% 0.18/0.39 ((~(((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> (~(((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(100,plain,
% 0.18/0.39 ((((~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))) <=> (((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(101,plain,
% 0.18/0.39 ((~(((~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> (~(((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[100])).
% 0.18/0.39 tff(102,plain,
% 0.18/0.39 ((~(((~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> (~(((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))))),
% 0.18/0.39 inference(transitivity,[status(thm)],[101, 99])).
% 0.18/0.39 tff(103,plain,
% 0.18/0.39 (((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))))) <=> ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[102])).
% 0.18/0.39 tff(104,plain,
% 0.18/0.39 (((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))))) <=> ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))))),
% 0.18/0.39 inference(transitivity,[status(thm)],[103, 98])).
% 0.18/0.39 tff(105,plain,
% 0.18/0.39 ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(106,plain,
% 0.18/0.39 ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[105, 104])).
% 0.18/0.39 tff(107,plain,
% 0.18/0.39 (~(((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[106, 81])).
% 0.18/0.39 tff(108,plain,
% 0.18/0.39 ((~![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))) | (model_ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(109,plain,
% 0.18/0.39 (model_ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[108, 90])).
% 0.18/0.39 tff(110,assumption,(~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))), introduced(assumption)).
% 0.18/0.39 tff(111,plain,
% 0.18/0.39 ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(max(X!4, Y!3), max(X!4, Y!3)))) <=> ub(max(X!4, Y!3), Y!3, max(X!4, Y!3))))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(112,plain,
% 0.18/0.39 (~(((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(max(X!4, Y!3), max(X!4, Y!3)))) <=> ub(max(X!4, Y!3), Y!3, max(X!4, Y!3)))),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[111, 81])).
% 0.18/0.39 tff(113,plain,
% 0.18/0.39 ((~![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))) | (model_ub(max(X!4, Y!3), Y!3, max(X!4, Y!3)) <=> ub(max(X!4, Y!3), Y!3, max(X!4, Y!3)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(114,plain,
% 0.18/0.39 (model_ub(max(X!4, Y!3), Y!3, max(X!4, Y!3)) <=> ub(max(X!4, Y!3), Y!3, max(X!4, Y!3))),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[113, 90])).
% 0.18/0.39 tff(115,assumption,(lesseq(Y!3, X!4)), introduced(assumption)).
% 0.18/0.39 tff(116,plain,
% 0.18/0.39 (^[X: $i, Y: $i] : refl(((~lesseq(Y, X)) | (max(X, Y) = X)) <=> ((~lesseq(Y, X)) | (max(X, Y) = X)))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(117,plain,
% 0.18/0.39 (![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X)) <=> ![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[116])).
% 0.18/0.39 tff(118,plain,
% 0.18/0.39 (![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X)) <=> ![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(119,plain,
% 0.18/0.39 (^[X: $i, Y: $i] : rewrite(((max(X, Y) = X) | (~lesseq(Y, X))) <=> ((~lesseq(Y, X)) | (max(X, Y) = X)))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(120,plain,
% 0.18/0.39 (![X: $i, Y: $i] : ((max(X, Y) = X) | (~lesseq(Y, X))) <=> ![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))),
% 0.18/0.39 inference(quant_intro,[status(thm)],[119])).
% 0.18/0.39 tff(121,axiom,(![X: $i, Y: $i] : ((max(X, Y) = X) | (~lesseq(Y, X)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','max_1')).
% 0.18/0.39 tff(122,plain,
% 0.18/0.39 (![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[121, 120])).
% 0.18/0.39 tff(123,plain,
% 0.18/0.39 (![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[122, 118])).
% 0.18/0.39 tff(124,plain,(
% 0.18/0.39 ![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))),
% 0.18/0.39 inference(skolemize,[status(sab)],[123])).
% 0.18/0.39 tff(125,plain,
% 0.18/0.39 (![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[124, 117])).
% 0.18/0.39 tff(126,plain,
% 0.18/0.39 (((~![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))) | ((~lesseq(Y!3, X!4)) | (max(X!4, Y!3) = X!4))) <=> ((~![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))) | (~lesseq(Y!3, X!4)) | (max(X!4, Y!3) = X!4))),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(127,plain,
% 0.18/0.39 ((~![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))) | ((~lesseq(Y!3, X!4)) | (max(X!4, Y!3) = X!4))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(128,plain,
% 0.18/0.39 ((~![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))) | (~lesseq(Y!3, X!4)) | (max(X!4, Y!3) = X!4)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[127, 126])).
% 0.18/0.39 tff(129,plain,
% 0.18/0.39 ((~lesseq(Y!3, X!4)) | (max(X!4, Y!3) = X!4)),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[128, 125])).
% 0.18/0.39 tff(130,plain,
% 0.18/0.39 (max(X!4, Y!3) = X!4),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[129, 115])).
% 0.18/0.39 tff(131,plain,
% 0.18/0.39 (model_ub(max(X!4, Y!3), Y!3, max(X!4, Y!3)) <=> model_ub(X!4, Y!3, Z!2)),
% 0.18/0.39 inference(monotonicity,[status(thm)],[130, 93])).
% 0.18/0.39 tff(132,plain,
% 0.18/0.39 (model_ub(X!4, Y!3, Z!2) <=> model_ub(max(X!4, Y!3), Y!3, max(X!4, Y!3))),
% 0.18/0.39 inference(symmetry,[status(thm)],[131])).
% 0.18/0.39 tff(133,plain,
% 0.18/0.39 ((~model_ub(X!4, Y!3, Z!2)) <=> (~model_ub(max(X!4, Y!3), Y!3, max(X!4, Y!3)))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[132])).
% 0.18/0.39 tff(134,plain,
% 0.18/0.39 ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(135,plain,
% 0.18/0.39 (~(((~lesseq(Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4)))),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[134, 81])).
% 0.18/0.39 tff(136,plain,
% 0.18/0.39 ((~![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))) | (model_ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4)) <=> ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(137,plain,
% 0.18/0.39 (model_ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4)) <=> ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[136, 90])).
% 0.18/0.39 tff(138,assumption,(max(X!4, Y!3) = X!4), introduced(assumption)).
% 0.18/0.39 tff(139,plain,
% 0.18/0.39 (model_ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4)) <=> model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.18/0.39 inference(monotonicity,[status(thm)],[138])).
% 0.18/0.39 tff(140,plain,
% 0.18/0.39 (model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4)) <=> model_ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.18/0.39 inference(symmetry,[status(thm)],[139])).
% 0.18/0.39 tff(141,assumption,(model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))), introduced(assumption)).
% 0.18/0.39 tff(142,plain,
% 0.18/0.39 (model_ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[141, 140])).
% 0.18/0.39 tff(143,plain,
% 0.18/0.39 ((~(model_ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4)) <=> ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4)))) | (~model_ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(144,plain,
% 0.18/0.40 (ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[143, 142, 137])).
% 0.18/0.40 tff(145,plain,
% 0.18/0.40 (((~lesseq(Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) | lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(146,plain,
% 0.18/0.40 ((~lesseq(Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[145, 110])).
% 0.18/0.40 tff(147,plain,
% 0.18/0.40 ((((~lesseq(Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~((~lesseq(Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))))) | (~ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4)))),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(148,plain,
% 0.18/0.40 ((((~lesseq(Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~ub(max(X!4, Y!3), Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4)))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[147, 146])).
% 0.18/0.40 tff(149,plain,
% 0.18/0.40 ($false),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[148, 144, 135])).
% 0.18/0.40 tff(150,plain,((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)) | (~(max(X!4, Y!3) = X!4))), inference(lemma,lemma(discharge,[]))).
% 0.18/0.40 tff(151,plain,
% 0.18/0.40 (~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[150, 130, 110])).
% 0.18/0.40 tff(152,plain,
% 0.18/0.40 (((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4))) | model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(153,plain,
% 0.18/0.40 ((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[152, 151])).
% 0.18/0.40 tff(154,plain,
% 0.18/0.40 (^[X: $i, Y: $i, N: $i] : rewrite((~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))))) <=> (~((~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))) | (~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(155,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))))) <=> ![X: $i, Y: $i, N: $i] : (~((~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))) | (~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))))))))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[154])).
% 0.18/0.40 tff(156,plain,
% 0.18/0.40 (^[X: $i, Y: $i, N: $i] : refl((~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))))) <=> (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(157,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))))) <=> ![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X))))))))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[156])).
% 0.18/0.40 tff(158,plain,
% 0.18/0.40 (^[X: $i, Y: $i, N: $i] : rewrite((~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))))) <=> (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(159,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))))) <=> ![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X))))))))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[158])).
% 0.18/0.40 tff(160,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))))) <=> ![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X))))))))),
% 0.18/0.40 inference(transitivity,[status(thm)],[159, 157])).
% 0.18/0.40 tff(161,plain,
% 0.18/0.40 (^[X: $i, Y: $i, N: $i] : trans(monotonicity(rewrite(((~minsol_model_ub(X, Y, N)) | (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))) <=> ((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))), rewrite((minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X))))) <=> (minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))), ((((~minsol_model_ub(X, Y, N)) | (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))) <=> (((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))))) & (minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))))), rewrite((((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))))) & (minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))) <=> (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X))))))))), ((((~minsol_model_ub(X, Y, N)) | (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))) <=> (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X))))))))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(162,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (((~minsol_model_ub(X, Y, N)) | (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))) <=> ![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X))))))))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[161])).
% 0.18/0.40 tff(163,plain,
% 0.18/0.40 (^[X: $i, Y: $i, N: $i] : rewrite((((~minsol_model_ub(X, Y, N)) | (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_ub(X, Y, N) | ((~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X))))))) <=> (((~minsol_model_ub(X, Y, N)) | (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(164,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (((~minsol_model_ub(X, Y, N)) | (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_ub(X, Y, N) | ((~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X))))))) <=> ![X: $i, Y: $i, N: $i] : (((~minsol_model_ub(X, Y, N)) | (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X))))))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[163])).
% 0.18/0.40 tff(165,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (minsol_model_ub(X, Y, N) <=> (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))) <=> ![X: $i, Y: $i, N: $i] : (minsol_model_ub(X, Y, N) <=> (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(166,plain,
% 0.18/0.40 (^[X: $i, Y: $i, N: $i] : rewrite((minsol_model_ub(X, Y, N) <=> (model_ub(X, Y, N) & ![Z: $i] : (model_ub(X, Y, Z) => lesseq(N, Z)))) <=> (minsol_model_ub(X, Y, N) <=> (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(167,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (minsol_model_ub(X, Y, N) <=> (model_ub(X, Y, N) & ![Z: $i] : (model_ub(X, Y, Z) => lesseq(N, Z)))) <=> ![X: $i, Y: $i, N: $i] : (minsol_model_ub(X, Y, N) <=> (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[166])).
% 0.18/0.40 tff(168,axiom,(![X: $i, Y: $i, N: $i] : (minsol_model_ub(X, Y, N) <=> (model_ub(X, Y, N) & ![Z: $i] : (model_ub(X, Y, Z) => lesseq(N, Z))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','minsol_model_ub')).
% 0.18/0.40 tff(169,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (minsol_model_ub(X, Y, N) <=> (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[168, 167])).
% 0.18/0.40 tff(170,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (minsol_model_ub(X, Y, N) <=> (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[169, 165])).
% 0.18/0.40 tff(171,plain,(
% 0.18/0.40 ![X: $i, Y: $i, N: $i] : (((~minsol_model_ub(X, Y, N)) | (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_ub(X, Y, N) | ((~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))))),
% 0.18/0.40 inference(skolemize,[status(sab)],[170])).
% 0.18/0.40 tff(172,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (((~minsol_model_ub(X, Y, N)) | (model_ub(X, Y, N) & ![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))) & (minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X))))))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[171, 164])).
% 0.18/0.40 tff(173,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X))))))))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[172, 162])).
% 0.18/0.40 tff(174,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (~((~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z))))))) | (~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X))))))))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[173, 160])).
% 0.18/0.40 tff(175,plain,
% 0.18/0.40 (![X: $i, Y: $i, N: $i] : (~((~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))) | (~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))))))))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[174, 155])).
% 0.18/0.40 tff(176,plain,
% 0.18/0.40 ((~![X: $i, Y: $i, N: $i] : (~((~(minsol_model_ub(X, Y, N) | (~model_ub(X, Y, N)) | (~((~model_ub(X, Y, tptp_fun_Z_1(N, Y, X))) | lesseq(N, tptp_fun_Z_1(N, Y, X)))))) | (~((~minsol_model_ub(X, Y, N)) | (~((~model_ub(X, Y, N)) | (~![Z: $i] : ((~model_ub(X, Y, Z)) | lesseq(N, Z)))))))))) | (~((~(minsol_model_ub(X!4, Y!3, Z!2) | (~model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4)))))) | (~((~minsol_model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z)))))))))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(177,plain,
% 0.18/0.40 (~((~(minsol_model_ub(X!4, Y!3, Z!2) | (~model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4)))))) | (~((~minsol_model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))))))))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[176, 175])).
% 0.18/0.40 tff(178,plain,
% 0.18/0.40 (((~(minsol_model_ub(X!4, Y!3, Z!2) | (~model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4)))))) | (~((~minsol_model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z)))))))) | (minsol_model_ub(X!4, Y!3, Z!2) | (~model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4)))))),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(179,plain,
% 0.18/0.40 (minsol_model_ub(X!4, Y!3, Z!2) | (~model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4))))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[178, 177])).
% 0.18/0.40 tff(180,plain,
% 0.18/0.40 ((~(minsol_model_ub(X!4, Y!3, Z!2) | (~model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4)))))) | minsol_model_ub(X!4, Y!3, Z!2) | (~model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4))))),
% 0.18/0.40 inference(tautology,[status(thm)],[])).
% 0.18/0.40 tff(181,plain,
% 0.18/0.40 (minsol_model_ub(X!4, Y!3, Z!2) | (~model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4))))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[180, 179])).
% 0.18/0.40 tff(182,plain,
% 0.18/0.40 (~model_ub(X!4, Y!3, Z!2)),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[181, 153, 19])).
% 0.19/0.41 tff(183,plain,
% 0.19/0.41 (~model_ub(max(X!4, Y!3), Y!3, max(X!4, Y!3))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[182, 133])).
% 0.19/0.41 tff(184,plain,
% 0.19/0.41 ((~(model_ub(max(X!4, Y!3), Y!3, max(X!4, Y!3)) <=> ub(max(X!4, Y!3), Y!3, max(X!4, Y!3)))) | model_ub(max(X!4, Y!3), Y!3, max(X!4, Y!3)) | (~ub(max(X!4, Y!3), Y!3, max(X!4, Y!3)))),
% 0.19/0.41 inference(tautology,[status(thm)],[])).
% 0.19/0.41 tff(185,plain,
% 0.19/0.41 (~ub(max(X!4, Y!3), Y!3, max(X!4, Y!3))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[184, 183, 114])).
% 0.19/0.41 tff(186,plain,
% 0.19/0.41 (lesseq(Y!3, max(X!4, Y!3)) <=> lesseq(Y!3, X!4)),
% 0.19/0.41 inference(monotonicity,[status(thm)],[130])).
% 0.19/0.41 tff(187,plain,
% 0.19/0.41 (lesseq(Y!3, X!4) <=> lesseq(Y!3, max(X!4, Y!3))),
% 0.19/0.41 inference(symmetry,[status(thm)],[186])).
% 0.19/0.41 tff(188,plain,
% 0.19/0.41 (lesseq(Y!3, max(X!4, Y!3))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[115, 187])).
% 0.19/0.41 tff(189,plain,
% 0.19/0.41 (lesseq(max(X!4, Y!3), max(X!4, Y!3)) <=> lesseq(Z!2, Z!2)),
% 0.19/0.41 inference(monotonicity,[status(thm)],[93, 93])).
% 0.19/0.41 tff(190,plain,
% 0.19/0.41 (lesseq(Z!2, Z!2) <=> lesseq(max(X!4, Y!3), max(X!4, Y!3))),
% 0.19/0.41 inference(symmetry,[status(thm)],[189])).
% 0.19/0.41 tff(191,plain,
% 0.19/0.41 (lesseq(max(X!4, Y!3), max(X!4, Y!3))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[71, 190])).
% 0.19/0.41 tff(192,plain,
% 0.19/0.41 ((~((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(max(X!4, Y!3), max(X!4, Y!3))))) | (~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(max(X!4, Y!3), max(X!4, Y!3)))),
% 0.19/0.41 inference(tautology,[status(thm)],[])).
% 0.19/0.41 tff(193,plain,
% 0.19/0.41 (~((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(max(X!4, Y!3), max(X!4, Y!3))))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[192, 191, 188])).
% 0.19/0.41 tff(194,plain,
% 0.19/0.41 ((((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(max(X!4, Y!3), max(X!4, Y!3)))) <=> ub(max(X!4, Y!3), Y!3, max(X!4, Y!3))) | ((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(max(X!4, Y!3), max(X!4, Y!3)))) | ub(max(X!4, Y!3), Y!3, max(X!4, Y!3))),
% 0.19/0.41 inference(tautology,[status(thm)],[])).
% 0.19/0.41 tff(195,plain,
% 0.19/0.41 ((((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(max(X!4, Y!3), max(X!4, Y!3)))) <=> ub(max(X!4, Y!3), Y!3, max(X!4, Y!3))) | ub(max(X!4, Y!3), Y!3, max(X!4, Y!3))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[194, 193])).
% 0.19/0.41 tff(196,plain,
% 0.19/0.41 ($false),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[195, 185, 112])).
% 0.19/0.41 tff(197,plain,((~lesseq(Y!3, X!4)) | minsol_model_ub(X!4, Y!3, Z!2) | lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.41 tff(198,plain,
% 0.19/0.41 (~lesseq(Y!3, X!4)),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[197, 110, 19])).
% 0.19/0.41 tff(199,plain,
% 0.19/0.41 (^[X: $i, Y: $i] : refl((lesseq(X, Y) | lesseq(Y, X)) <=> (lesseq(X, Y) | lesseq(Y, X)))),
% 0.19/0.41 inference(bind,[status(th)],[])).
% 0.19/0.41 tff(200,plain,
% 0.19/0.41 (![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X)) <=> ![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))),
% 0.19/0.41 inference(quant_intro,[status(thm)],[199])).
% 0.19/0.41 tff(201,plain,
% 0.19/0.41 (![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X)) <=> ![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(202,axiom,(![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','lesseq_total')).
% 0.19/0.41 tff(203,plain,
% 0.19/0.41 (![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[202, 201])).
% 0.19/0.41 tff(204,plain,(
% 0.19/0.41 ![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))),
% 0.19/0.41 inference(skolemize,[status(sab)],[203])).
% 0.19/0.41 tff(205,plain,
% 0.19/0.41 (![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[204, 200])).
% 0.19/0.41 tff(206,plain,
% 0.19/0.41 (((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | (lesseq(X!4, Y!3) | lesseq(Y!3, X!4))) <=> ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(X!4, Y!3) | lesseq(Y!3, X!4))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(207,plain,
% 0.19/0.41 ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | (lesseq(X!4, Y!3) | lesseq(Y!3, X!4))),
% 0.19/0.41 inference(quant_inst,[status(thm)],[])).
% 0.19/0.41 tff(208,plain,
% 0.19/0.41 ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(X!4, Y!3) | lesseq(Y!3, X!4)),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[207, 206])).
% 0.19/0.41 tff(209,plain,
% 0.19/0.41 (lesseq(X!4, Y!3)),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[208, 205, 198])).
% 0.19/0.41 tff(210,plain,
% 0.19/0.41 (^[X: $i, Y: $i] : refl(((~lesseq(X, Y)) | (max(X, Y) = Y)) <=> ((~lesseq(X, Y)) | (max(X, Y) = Y)))),
% 0.19/0.41 inference(bind,[status(th)],[])).
% 0.19/0.41 tff(211,plain,
% 0.19/0.41 (![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y)) <=> ![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))),
% 0.19/0.41 inference(quant_intro,[status(thm)],[210])).
% 0.19/0.41 tff(212,plain,
% 0.19/0.41 (![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y)) <=> ![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(213,plain,
% 0.19/0.41 (^[X: $i, Y: $i] : rewrite(((max(X, Y) = Y) | (~lesseq(X, Y))) <=> ((~lesseq(X, Y)) | (max(X, Y) = Y)))),
% 0.19/0.41 inference(bind,[status(th)],[])).
% 0.19/0.41 tff(214,plain,
% 0.19/0.41 (![X: $i, Y: $i] : ((max(X, Y) = Y) | (~lesseq(X, Y))) <=> ![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))),
% 0.19/0.41 inference(quant_intro,[status(thm)],[213])).
% 0.19/0.41 tff(215,axiom,(![X: $i, Y: $i] : ((max(X, Y) = Y) | (~lesseq(X, Y)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','max_2')).
% 0.19/0.41 tff(216,plain,
% 0.19/0.41 (![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[215, 214])).
% 0.19/0.41 tff(217,plain,
% 0.19/0.41 (![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[216, 212])).
% 0.19/0.41 tff(218,plain,(
% 0.19/0.41 ![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))),
% 0.19/0.41 inference(skolemize,[status(sab)],[217])).
% 0.19/0.41 tff(219,plain,
% 0.19/0.41 (![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[218, 211])).
% 0.19/0.41 tff(220,plain,
% 0.19/0.41 (((~![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))) | ((~lesseq(X!4, Y!3)) | (max(X!4, Y!3) = Y!3))) <=> ((~![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))) | (~lesseq(X!4, Y!3)) | (max(X!4, Y!3) = Y!3))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(221,plain,
% 0.19/0.41 ((~![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))) | ((~lesseq(X!4, Y!3)) | (max(X!4, Y!3) = Y!3))),
% 0.19/0.41 inference(quant_inst,[status(thm)],[])).
% 0.19/0.41 tff(222,plain,
% 0.19/0.41 ((~![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))) | (~lesseq(X!4, Y!3)) | (max(X!4, Y!3) = Y!3)),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[221, 220])).
% 0.19/0.41 tff(223,plain,
% 0.19/0.41 ((~lesseq(X!4, Y!3)) | (max(X!4, Y!3) = Y!3)),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[222, 219])).
% 0.19/0.41 tff(224,plain,
% 0.19/0.41 (max(X!4, Y!3) = Y!3),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[223, 209])).
% 0.19/0.41 tff(225,plain,
% 0.19/0.41 (model_ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)) <=> model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.19/0.41 inference(monotonicity,[status(thm)],[224])).
% 0.19/0.41 tff(226,plain,
% 0.19/0.41 (model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4)) <=> model_ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.19/0.41 inference(symmetry,[status(thm)],[225])).
% 0.19/0.41 tff(227,plain,
% 0.19/0.41 (lesseq(X!4, max(X!4, Y!3)) <=> lesseq(X!4, Y!3)),
% 0.19/0.41 inference(monotonicity,[status(thm)],[224])).
% 0.19/0.41 tff(228,plain,
% 0.19/0.41 (lesseq(X!4, Y!3) <=> lesseq(X!4, max(X!4, Y!3))),
% 0.19/0.41 inference(symmetry,[status(thm)],[227])).
% 0.19/0.41 tff(229,plain,
% 0.19/0.41 (lesseq(X!4, max(X!4, Y!3))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[209, 228])).
% 0.19/0.41 tff(230,plain,
% 0.19/0.41 ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(max(X!4, Y!3), max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3)))) <=> ub(X!4, max(X!4, Y!3), max(X!4, Y!3))))),
% 0.19/0.41 inference(quant_inst,[status(thm)],[])).
% 0.19/0.41 tff(231,plain,
% 0.19/0.41 (~(((~lesseq(max(X!4, Y!3), max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3)))) <=> ub(X!4, max(X!4, Y!3), max(X!4, Y!3)))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[230, 81])).
% 0.19/0.41 tff(232,plain,
% 0.19/0.41 ((~![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))) | (model_ub(X!4, max(X!4, Y!3), max(X!4, Y!3)) <=> ub(X!4, max(X!4, Y!3), max(X!4, Y!3)))),
% 0.19/0.41 inference(quant_inst,[status(thm)],[])).
% 0.19/0.41 tff(233,plain,
% 0.19/0.41 (model_ub(X!4, max(X!4, Y!3), max(X!4, Y!3)) <=> ub(X!4, max(X!4, Y!3), max(X!4, Y!3))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[232, 90])).
% 0.19/0.41 tff(234,assumption,(max(X!4, Y!3) = Y!3), introduced(assumption)).
% 0.19/0.41 tff(235,plain,
% 0.19/0.41 (model_ub(X!4, max(X!4, Y!3), max(X!4, Y!3)) <=> model_ub(X!4, Y!3, Z!2)),
% 0.19/0.41 inference(monotonicity,[status(thm)],[234, 2])).
% 0.19/0.41 tff(236,plain,
% 0.19/0.41 (model_ub(X!4, Y!3, Z!2) <=> model_ub(X!4, max(X!4, Y!3), max(X!4, Y!3))),
% 0.19/0.41 inference(symmetry,[status(thm)],[235])).
% 0.19/0.41 tff(237,plain,
% 0.19/0.41 ((~model_ub(X!4, Y!3, Z!2)) <=> (~model_ub(X!4, max(X!4, Y!3), max(X!4, Y!3)))),
% 0.19/0.41 inference(monotonicity,[status(thm)],[236])).
% 0.19/0.41 tff(238,assumption,(~model_ub(X!4, Y!3, Z!2)), introduced(assumption)).
% 0.19/0.41 tff(239,plain,
% 0.19/0.41 (~model_ub(X!4, max(X!4, Y!3), max(X!4, Y!3))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[238, 237])).
% 0.19/0.41 tff(240,plain,
% 0.19/0.41 ((~(model_ub(X!4, max(X!4, Y!3), max(X!4, Y!3)) <=> ub(X!4, max(X!4, Y!3), max(X!4, Y!3)))) | model_ub(X!4, max(X!4, Y!3), max(X!4, Y!3)) | (~ub(X!4, max(X!4, Y!3), max(X!4, Y!3)))),
% 0.19/0.41 inference(tautology,[status(thm)],[])).
% 0.19/0.41 tff(241,plain,
% 0.19/0.41 (~ub(X!4, max(X!4, Y!3), max(X!4, Y!3))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[240, 239, 233])).
% 0.19/0.41 tff(242,assumption,(lesseq(X!4, max(X!4, Y!3))), introduced(assumption)).
% 0.19/0.41 tff(243,assumption,(lesseq(max(X!4, Y!3), max(X!4, Y!3))), introduced(assumption)).
% 0.19/0.41 tff(244,plain,
% 0.19/0.41 ((~((~lesseq(max(X!4, Y!3), max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3))))) | (~lesseq(max(X!4, Y!3), max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3)))),
% 0.19/0.41 inference(tautology,[status(thm)],[])).
% 0.19/0.41 tff(245,plain,
% 0.19/0.41 (~((~lesseq(max(X!4, Y!3), max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3))))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[244, 243, 242])).
% 0.19/0.41 tff(246,plain,
% 0.19/0.41 ((((~lesseq(max(X!4, Y!3), max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3)))) <=> ub(X!4, max(X!4, Y!3), max(X!4, Y!3))) | ((~lesseq(max(X!4, Y!3), max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3)))) | ub(X!4, max(X!4, Y!3), max(X!4, Y!3))),
% 0.19/0.41 inference(tautology,[status(thm)],[])).
% 0.19/0.41 tff(247,plain,
% 0.19/0.41 ((((~lesseq(max(X!4, Y!3), max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3)))) <=> ub(X!4, max(X!4, Y!3), max(X!4, Y!3))) | ub(X!4, max(X!4, Y!3), max(X!4, Y!3))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[246, 245])).
% 0.19/0.41 tff(248,plain,
% 0.19/0.41 ($false),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[247, 241, 231])).
% 0.19/0.41 tff(249,plain,(model_ub(X!4, Y!3, Z!2) | (~lesseq(max(X!4, Y!3), max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3))) | (~(Z!2 = max(X!4, Y!3))) | (~(max(X!4, Y!3) = Y!3))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.41 tff(250,plain,
% 0.19/0.41 (model_ub(X!4, Y!3, Z!2)),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[249, 229, 191, 65, 224])).
% 0.19/0.41 tff(251,plain,
% 0.19/0.41 (~((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4)))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[181, 250, 19])).
% 0.19/0.41 tff(252,plain,
% 0.19/0.41 (model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[152, 251])).
% 0.19/0.41 tff(253,plain,
% 0.19/0.41 (model_ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[252, 226])).
% 0.19/0.41 tff(254,plain,
% 0.19/0.41 ((~(model_ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) | (~model_ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))) | ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.19/0.41 inference(tautology,[status(thm)],[])).
% 0.19/0.41 tff(255,plain,
% 0.19/0.41 (ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[254, 253, 109])).
% 0.19/0.41 tff(256,plain,
% 0.19/0.41 (((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) | lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.19/0.41 inference(tautology,[status(thm)],[])).
% 0.19/0.41 tff(257,plain,
% 0.19/0.41 ((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[256, 110])).
% 0.19/0.41 tff(258,plain,
% 0.19/0.41 ((((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))))) | (~ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(259,plain,
% 0.19/0.42 ((((~lesseq(X!4, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))) <=> ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~ub(X!4, max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[258, 257])).
% 0.19/0.42 tff(260,plain,
% 0.19/0.42 ($false),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[259, 255, 107])).
% 0.19/0.42 tff(261,plain,(lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4)) | minsol_model_ub(X!4, Y!3, Z!2)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.42 tff(262,plain,
% 0.19/0.42 (lesseq(max(X!4, Y!3), tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[261, 19])).
% 0.19/0.42 tff(263,plain,
% 0.19/0.42 (lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[262, 97])).
% 0.19/0.42 tff(264,plain,
% 0.19/0.42 (((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4))) | (~lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4)))),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(265,plain,
% 0.19/0.42 ((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[264, 263])).
% 0.19/0.42 tff(266,plain,
% 0.19/0.42 (~model_ub(X!4, Y!3, Z!2)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[181, 265, 19])).
% 0.19/0.42 tff(267,plain,
% 0.19/0.42 (~model_ub(X!4, Y!3, max(X!4, Y!3))),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[266, 96])).
% 0.19/0.42 tff(268,plain,
% 0.19/0.42 ((~(model_ub(X!4, Y!3, max(X!4, Y!3)) <=> ub(X!4, Y!3, max(X!4, Y!3)))) | model_ub(X!4, Y!3, max(X!4, Y!3)) | (~ub(X!4, Y!3, max(X!4, Y!3)))),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(269,plain,
% 0.19/0.42 (~ub(X!4, Y!3, max(X!4, Y!3))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[268, 267, 92])).
% 0.19/0.42 tff(270,plain,
% 0.19/0.42 ((((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3)))) <=> ub(X!4, Y!3, max(X!4, Y!3))) | ((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3)))) | ub(X!4, Y!3, max(X!4, Y!3))),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(271,plain,
% 0.19/0.42 ((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3)))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[270, 269, 83])).
% 0.19/0.42 tff(272,assumption,((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3)))), introduced(assumption)).
% 0.19/0.42 tff(273,plain,
% 0.19/0.42 (X!4 = max(X!4, Y!3)),
% 0.19/0.42 inference(symmetry,[status(thm)],[130])).
% 0.19/0.42 tff(274,plain,
% 0.19/0.42 (lesseq(Y!3, X!4) <=> lesseq(Y!3, max(X!4, Y!3))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[273])).
% 0.19/0.42 tff(275,plain,
% 0.19/0.42 (lesseq(Y!3, max(X!4, Y!3))),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[115, 274])).
% 0.19/0.42 tff(276,plain,
% 0.19/0.42 (X!4 = Z!2),
% 0.19/0.42 inference(transitivity,[status(thm)],[273, 2])).
% 0.19/0.42 tff(277,plain,
% 0.19/0.42 (lesseq(X!4, max(X!4, Y!3)) <=> lesseq(Z!2, Z!2)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[276, 2])).
% 0.19/0.42 tff(278,plain,
% 0.19/0.42 (lesseq(Z!2, Z!2) <=> lesseq(X!4, max(X!4, Y!3))),
% 0.19/0.42 inference(symmetry,[status(thm)],[277])).
% 0.19/0.42 tff(279,assumption,(lesseq(Z!2, Z!2)), introduced(assumption)).
% 0.19/0.42 tff(280,plain,
% 0.19/0.42 (lesseq(X!4, max(X!4, Y!3))),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[279, 278])).
% 0.19/0.42 tff(281,plain,
% 0.19/0.42 ((~((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3))))) | (~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3)))),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(282,plain,
% 0.19/0.42 ($false),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[281, 280, 275, 272])).
% 0.19/0.42 tff(283,plain,((~lesseq(Y!3, X!4)) | (~((~lesseq(Y!3, max(X!4, Y!3))) | (~lesseq(X!4, max(X!4, Y!3))))) | (~lesseq(Z!2, Z!2)) | (~(Z!2 = max(X!4, Y!3)))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.42 tff(284,plain,
% 0.19/0.42 (~lesseq(Y!3, X!4)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[283, 271, 71, 65])).
% 0.19/0.42 tff(285,plain,
% 0.19/0.42 (lesseq(X!4, Y!3)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[208, 205, 284])).
% 0.19/0.42 tff(286,plain,
% 0.19/0.42 (max(X!4, Y!3) = Y!3),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[223, 285])).
% 0.19/0.42 tff(287,plain,
% 0.19/0.42 (Y!3 = max(X!4, Y!3)),
% 0.19/0.42 inference(symmetry,[status(thm)],[286])).
% 0.19/0.42 tff(288,plain,
% 0.19/0.42 (lesseq(X!4, Y!3) <=> lesseq(X!4, max(X!4, Y!3))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[287])).
% 0.19/0.42 tff(289,plain,
% 0.19/0.42 (lesseq(X!4, max(X!4, Y!3)) <=> lesseq(X!4, Y!3)),
% 0.19/0.42 inference(symmetry,[status(thm)],[288])).
% 0.19/0.42 tff(290,plain,
% 0.19/0.42 ((~lesseq(X!4, max(X!4, Y!3))) <=> (~lesseq(X!4, Y!3))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[289])).
% 0.19/0.42 tff(291,plain,
% 0.19/0.42 (~lesseq(X!4, max(X!4, Y!3))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[249, 286, 266, 65, 191])).
% 0.19/0.42 tff(292,plain,
% 0.19/0.42 (~lesseq(X!4, Y!3)),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[291, 290])).
% 0.19/0.42 tff(293,plain,
% 0.19/0.42 ($false),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[285, 292])).
% 0.19/0.42 tff(294,plain,(minsol_model_ub(X!4, Y!3, Z!2)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.42 tff(295,plain,
% 0.19/0.42 ((minsol_model_ub(X!4, Y!3, Z!2) <=> minsol_model_max(X!4, Y!3, Z!2)) | (~minsol_model_ub(X!4, Y!3, Z!2)) | (~minsol_model_max(X!4, Y!3, Z!2))),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(296,plain,
% 0.19/0.42 ((~minsol_model_ub(X!4, Y!3, Z!2)) | (~minsol_model_max(X!4, Y!3, Z!2))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[295, 28])).
% 0.19/0.42 tff(297,plain,
% 0.19/0.42 (~minsol_model_max(X!4, Y!3, Z!2)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[296, 294])).
% 0.19/0.42 tff(298,plain,
% 0.19/0.42 (((~(minsol_model_max(X!4, Y!3, Z!2) | (~model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4)))))) | (~((~minsol_model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_max(X!4, Y!3, Z)) | lesseq(Z!2, Z)))))))) | (minsol_model_max(X!4, Y!3, Z!2) | (~model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4)))))),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(299,plain,
% 0.19/0.42 (minsol_model_max(X!4, Y!3, Z!2) | (~model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4))))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[298, 55])).
% 0.19/0.42 tff(300,plain,
% 0.19/0.42 ((~(minsol_model_max(X!4, Y!3, Z!2) | (~model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4)))))) | minsol_model_max(X!4, Y!3, Z!2) | (~model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4))))),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(301,plain,
% 0.19/0.42 (minsol_model_max(X!4, Y!3, Z!2) | (~model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4))))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[300, 299])).
% 0.19/0.42 tff(302,plain,
% 0.19/0.42 ((~model_max(X!4, Y!3, Z!2)) | (~((~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4))))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[301, 297])).
% 0.19/0.42 tff(303,plain,
% 0.19/0.42 (~((~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4)))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[302, 17])).
% 0.19/0.42 tff(304,plain,
% 0.19/0.42 (((~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4))) | model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(305,plain,
% 0.19/0.42 (model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[304, 303])).
% 0.19/0.42 tff(306,plain,
% 0.19/0.42 ((~(model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4)) <=> (tptp_fun_Z_0(Z!2, Y!3, X!4) = max(X!4, Y!3)))) | (~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | (tptp_fun_Z_0(Z!2, Y!3, X!4) = max(X!4, Y!3))),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(307,plain,
% 0.19/0.42 ((~(model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4)) <=> (tptp_fun_Z_0(Z!2, Y!3, X!4) = max(X!4, Y!3)))) | (tptp_fun_Z_0(Z!2, Y!3, X!4) = max(X!4, Y!3))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[306, 305])).
% 0.19/0.42 tff(308,plain,
% 0.19/0.42 (tptp_fun_Z_0(Z!2, Y!3, X!4) = max(X!4, Y!3)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[307, 11])).
% 0.19/0.42 tff(309,plain,
% 0.19/0.42 (tptp_fun_Z_0(Z!2, Y!3, X!4) = Z!2),
% 0.19/0.42 inference(transitivity,[status(thm)],[308, 2])).
% 0.19/0.42 tff(310,plain,
% 0.19/0.42 (lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4)) <=> lesseq(Z!2, Z!2)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[309])).
% 0.19/0.42 tff(311,plain,
% 0.19/0.42 (lesseq(Z!2, Z!2) <=> lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4))),
% 0.19/0.42 inference(symmetry,[status(thm)],[310])).
% 0.19/0.42 tff(312,plain,
% 0.19/0.42 (((~(minsol_model_ub(X!4, Y!3, Z!2) | (~model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, tptp_fun_Z_1(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_1(Z!2, Y!3, X!4)))))) | (~((~minsol_model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z)))))))) | ((~minsol_model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))))))),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(313,plain,
% 0.19/0.42 ((~minsol_model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z)))))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[312, 177])).
% 0.19/0.42 tff(314,plain,
% 0.19/0.42 ((~((~minsol_model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))))))) | (~minsol_model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z)))))),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(315,plain,
% 0.19/0.42 ((~minsol_model_ub(X!4, Y!3, Z!2)) | (~((~model_ub(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z)))))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[314, 313])).
% 0.19/0.42 tff(316,plain,
% 0.19/0.42 (~((~model_ub(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[315, 294])).
% 0.19/0.42 tff(317,plain,
% 0.19/0.42 (((~model_ub(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z)))) | ![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(318,plain,
% 0.19/0.42 (![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[317, 316])).
% 0.19/0.42 tff(319,plain,
% 0.19/0.42 (((~model_ub(X!4, Y!3, Z!2)) | (~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z)))) | model_ub(X!4, Y!3, Z!2)),
% 0.19/0.42 inference(tautology,[status(thm)],[])).
% 0.19/0.42 tff(320,plain,
% 0.19/0.42 (model_ub(X!4, Y!3, Z!2)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[319, 316])).
% 0.19/0.42 tff(321,plain,
% 0.19/0.42 (((~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | ((~model_ub(X!4, Y!3, Z!2)) | lesseq(Z!2, Z!2))) <=> ((~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | (~model_ub(X!4, Y!3, Z!2)) | lesseq(Z!2, Z!2))),
% 0.19/0.42 inference(rewrite,[status(thm)],[])).
% 0.19/0.42 tff(322,plain,
% 0.19/0.42 ((~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | ((~model_ub(X!4, Y!3, Z!2)) | lesseq(Z!2, Z!2))),
% 0.19/0.42 inference(quant_inst,[status(thm)],[])).
% 0.19/0.42 tff(323,plain,
% 0.19/0.42 ((~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | (~model_ub(X!4, Y!3, Z!2)) | lesseq(Z!2, Z!2)),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[322, 321])).
% 0.19/0.42 tff(324,plain,
% 0.19/0.42 (lesseq(Z!2, Z!2)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[323, 320, 318])).
% 0.19/0.42 tff(325,plain,
% 0.19/0.42 (lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4))),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[324, 311])).
% 0.19/0.42 tff(326,plain,
% 0.19/0.43 (((~model_max(X!4, Y!3, tptp_fun_Z_0(Z!2, Y!3, X!4))) | lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4))) | (~lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4)))),
% 0.19/0.43 inference(tautology,[status(thm)],[])).
% 0.19/0.43 tff(327,plain,
% 0.19/0.43 (~lesseq(Z!2, tptp_fun_Z_0(Z!2, Y!3, X!4))),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[326, 303])).
% 0.19/0.43 tff(328,plain,
% 0.19/0.43 ($false),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[327, 325])).
% 0.19/0.43 tff(329,plain,(~(Z!2 = max(X!4, Y!3))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.43 tff(330,assumption,(~(model_ub(X!4, Y!3, Y!3) <=> ub(X!4, Y!3, Y!3))), introduced(assumption)).
% 0.19/0.43 tff(331,plain,
% 0.19/0.43 ((~![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))) | (model_ub(X!4, Y!3, Y!3) <=> ub(X!4, Y!3, Y!3))),
% 0.19/0.43 inference(quant_inst,[status(thm)],[])).
% 0.19/0.43 tff(332,plain,
% 0.19/0.43 ($false),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[331, 90, 330])).
% 0.19/0.43 tff(333,plain,(model_ub(X!4, Y!3, Y!3) <=> ub(X!4, Y!3, Y!3)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.43 tff(334,assumption,(((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) <=> ub(X!4, Y!3, Y!3)), introduced(assumption)).
% 0.19/0.43 tff(335,plain,
% 0.19/0.43 (((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) <=> ub(X!4, Y!3, Y!3)))) <=> ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) <=> ub(X!4, Y!3, Y!3))))),
% 0.19/0.43 inference(rewrite,[status(thm)],[])).
% 0.19/0.43 tff(336,plain,
% 0.19/0.43 ((~(((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) <=> ub(X!4, Y!3, Y!3))) <=> (~(((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) <=> ub(X!4, Y!3, Y!3)))),
% 0.19/0.43 inference(rewrite,[status(thm)],[])).
% 0.19/0.43 tff(337,plain,
% 0.19/0.43 ((((~lesseq(Y!3, Y!3)) | (~lesseq(X!4, Y!3))) <=> ub(X!4, Y!3, Y!3)) <=> (((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) <=> ub(X!4, Y!3, Y!3))),
% 0.19/0.43 inference(rewrite,[status(thm)],[])).
% 0.19/0.43 tff(338,plain,
% 0.19/0.43 ((~(((~lesseq(Y!3, Y!3)) | (~lesseq(X!4, Y!3))) <=> ub(X!4, Y!3, Y!3))) <=> (~(((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) <=> ub(X!4, Y!3, Y!3)))),
% 0.19/0.43 inference(monotonicity,[status(thm)],[337])).
% 0.19/0.43 tff(339,plain,
% 0.19/0.43 ((~(((~lesseq(Y!3, Y!3)) | (~lesseq(X!4, Y!3))) <=> ub(X!4, Y!3, Y!3))) <=> (~(((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) <=> ub(X!4, Y!3, Y!3)))),
% 0.19/0.43 inference(transitivity,[status(thm)],[338, 336])).
% 0.19/0.43 tff(340,plain,
% 0.19/0.43 (((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(Y!3, Y!3)) | (~lesseq(X!4, Y!3))) <=> ub(X!4, Y!3, Y!3)))) <=> ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) <=> ub(X!4, Y!3, Y!3))))),
% 0.19/0.43 inference(monotonicity,[status(thm)],[339])).
% 0.19/0.43 tff(341,plain,
% 0.19/0.43 (((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(Y!3, Y!3)) | (~lesseq(X!4, Y!3))) <=> ub(X!4, Y!3, Y!3)))) <=> ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) <=> ub(X!4, Y!3, Y!3))))),
% 0.19/0.43 inference(transitivity,[status(thm)],[340, 335])).
% 0.19/0.43 tff(342,plain,
% 0.19/0.43 ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(Y!3, Y!3)) | (~lesseq(X!4, Y!3))) <=> ub(X!4, Y!3, Y!3)))),
% 0.19/0.43 inference(quant_inst,[status(thm)],[])).
% 0.19/0.43 tff(343,plain,
% 0.19/0.43 ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) <=> ub(X!4, Y!3, Y!3)))),
% 0.19/0.43 inference(modus_ponens,[status(thm)],[342, 341])).
% 0.19/0.43 tff(344,plain,
% 0.19/0.43 ($false),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[343, 81, 334])).
% 0.19/0.43 tff(345,plain,(~(((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) <=> ub(X!4, Y!3, Y!3))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.43 tff(346,assumption,(lesseq(X!4, Y!3)), introduced(assumption)).
% 0.19/0.43 tff(347,assumption,(~lesseq(Y!3, Y!3)), introduced(assumption)).
% 0.19/0.43 tff(348,plain,
% 0.19/0.43 (((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(Y!3, Y!3)) <=> ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(Y!3, Y!3))),
% 0.19/0.43 inference(rewrite,[status(thm)],[])).
% 0.19/0.43 tff(349,plain,
% 0.19/0.43 ((lesseq(Y!3, Y!3) | lesseq(Y!3, Y!3)) <=> lesseq(Y!3, Y!3)),
% 0.19/0.43 inference(rewrite,[status(thm)],[])).
% 0.19/0.43 tff(350,plain,
% 0.19/0.43 (((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | (lesseq(Y!3, Y!3) | lesseq(Y!3, Y!3))) <=> ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(Y!3, Y!3))),
% 0.19/0.43 inference(monotonicity,[status(thm)],[349])).
% 0.19/0.43 tff(351,plain,
% 0.19/0.43 (((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | (lesseq(Y!3, Y!3) | lesseq(Y!3, Y!3))) <=> ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(Y!3, Y!3))),
% 0.19/0.43 inference(transitivity,[status(thm)],[350, 348])).
% 0.19/0.43 tff(352,plain,
% 0.19/0.43 ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | (lesseq(Y!3, Y!3) | lesseq(Y!3, Y!3))),
% 0.19/0.43 inference(quant_inst,[status(thm)],[])).
% 0.19/0.43 tff(353,plain,
% 0.19/0.43 ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(Y!3, Y!3)),
% 0.19/0.43 inference(modus_ponens,[status(thm)],[352, 351])).
% 0.19/0.43 tff(354,plain,
% 0.19/0.43 ($false),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[353, 205, 347])).
% 0.19/0.43 tff(355,plain,(lesseq(Y!3, Y!3)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.43 tff(356,plain,
% 0.19/0.43 ((~((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3)))) | (~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))),
% 0.19/0.43 inference(tautology,[status(thm)],[])).
% 0.19/0.43 tff(357,plain,
% 0.19/0.43 ((~((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3)))) | (~lesseq(X!4, Y!3))),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[356, 355])).
% 0.19/0.43 tff(358,plain,
% 0.19/0.43 (~((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3)))),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[357, 346])).
% 0.19/0.43 tff(359,plain,
% 0.19/0.43 ((((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) <=> ub(X!4, Y!3, Y!3)) | ((~lesseq(X!4, Y!3)) | (~lesseq(Y!3, Y!3))) | ub(X!4, Y!3, Y!3)),
% 0.19/0.43 inference(tautology,[status(thm)],[])).
% 0.19/0.43 tff(360,plain,
% 0.19/0.43 (ub(X!4, Y!3, Y!3)),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[359, 358, 345])).
% 0.19/0.43 tff(361,plain,
% 0.19/0.43 ((~(model_ub(X!4, Y!3, Y!3) <=> ub(X!4, Y!3, Y!3))) | model_ub(X!4, Y!3, Y!3) | (~ub(X!4, Y!3, Y!3))),
% 0.19/0.43 inference(tautology,[status(thm)],[])).
% 0.19/0.43 tff(362,plain,
% 0.19/0.43 (model_ub(X!4, Y!3, Y!3)),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[361, 360, 333])).
% 0.19/0.43 tff(363,plain,
% 0.19/0.43 (max(X!4, Y!3) = Y!3),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[223, 346])).
% 0.19/0.43 tff(364,plain,
% 0.19/0.43 ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(Y!3, Z!2)) | (~lesseq(X!4, Z!2))) <=> ub(X!4, Y!3, Z!2)))),
% 0.19/0.43 inference(quant_inst,[status(thm)],[])).
% 0.19/0.43 tff(365,plain,
% 0.19/0.43 (~(((~lesseq(Y!3, Z!2)) | (~lesseq(X!4, Z!2))) <=> ub(X!4, Y!3, Z!2))),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[364, 81])).
% 0.19/0.43 tff(366,plain,
% 0.19/0.43 ((~![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))) | (model_ub(X!4, Y!3, Z!2) <=> ub(X!4, Y!3, Z!2))),
% 0.19/0.43 inference(quant_inst,[status(thm)],[])).
% 0.19/0.43 tff(367,plain,
% 0.19/0.43 (model_ub(X!4, Y!3, Z!2) <=> ub(X!4, Y!3, Z!2)),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[366, 90])).
% 0.19/0.43 tff(368,plain,
% 0.19/0.43 ((~(model_ub(X!4, Y!3, Z!2) <=> ub(X!4, Y!3, Z!2))) | (~model_ub(X!4, Y!3, Z!2)) | ub(X!4, Y!3, Z!2)),
% 0.19/0.43 inference(tautology,[status(thm)],[])).
% 0.19/0.43 tff(369,plain,
% 0.19/0.43 ((~(model_ub(X!4, Y!3, Z!2) <=> ub(X!4, Y!3, Z!2))) | ub(X!4, Y!3, Z!2)),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[368, 320])).
% 0.19/0.43 tff(370,plain,
% 0.19/0.43 (ub(X!4, Y!3, Z!2)),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[369, 367])).
% 0.19/0.43 tff(371,plain,
% 0.19/0.43 ((((~lesseq(Y!3, Z!2)) | (~lesseq(X!4, Z!2))) <=> ub(X!4, Y!3, Z!2)) | (~((~lesseq(Y!3, Z!2)) | (~lesseq(X!4, Z!2)))) | (~ub(X!4, Y!3, Z!2))),
% 0.19/0.43 inference(tautology,[status(thm)],[])).
% 0.19/0.43 tff(372,plain,
% 0.19/0.43 ((((~lesseq(Y!3, Z!2)) | (~lesseq(X!4, Z!2))) <=> ub(X!4, Y!3, Z!2)) | (~((~lesseq(Y!3, Z!2)) | (~lesseq(X!4, Z!2))))),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[371, 370])).
% 0.19/0.43 tff(373,plain,
% 0.19/0.43 (~((~lesseq(Y!3, Z!2)) | (~lesseq(X!4, Z!2)))),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[372, 365])).
% 0.19/0.43 tff(374,plain,
% 0.19/0.43 (((~lesseq(Y!3, Z!2)) | (~lesseq(X!4, Z!2))) | lesseq(Y!3, Z!2)),
% 0.19/0.43 inference(tautology,[status(thm)],[])).
% 0.19/0.43 tff(375,plain,
% 0.19/0.43 (lesseq(Y!3, Z!2)),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[374, 373])).
% 0.19/0.43 tff(376,plain,
% 0.19/0.43 (((~![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))) | ((~lesseq(Y!3, Z!2)) | (max(Y!3, Z!2) = Z!2))) <=> ((~![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))) | (~lesseq(Y!3, Z!2)) | (max(Y!3, Z!2) = Z!2))),
% 0.19/0.43 inference(rewrite,[status(thm)],[])).
% 0.19/0.43 tff(377,plain,
% 0.19/0.43 ((~![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))) | ((~lesseq(Y!3, Z!2)) | (max(Y!3, Z!2) = Z!2))),
% 0.19/0.43 inference(quant_inst,[status(thm)],[])).
% 0.19/0.43 tff(378,plain,
% 0.19/0.43 ((~![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))) | (~lesseq(Y!3, Z!2)) | (max(Y!3, Z!2) = Z!2)),
% 0.19/0.43 inference(modus_ponens,[status(thm)],[377, 376])).
% 0.19/0.43 tff(379,plain,
% 0.19/0.43 (max(Y!3, Z!2) = Z!2),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[378, 219, 375])).
% 0.19/0.43 tff(380,plain,
% 0.19/0.43 (Z!2 = max(Y!3, Z!2)),
% 0.19/0.43 inference(symmetry,[status(thm)],[379])).
% 0.19/0.43 tff(381,plain,
% 0.19/0.43 ((Z!2 = max(X!4, Y!3)) <=> (max(Y!3, Z!2) = Y!3)),
% 0.19/0.43 inference(monotonicity,[status(thm)],[380, 363])).
% 0.19/0.43 tff(382,plain,
% 0.19/0.43 ((~(Z!2 = max(X!4, Y!3))) <=> (~(max(Y!3, Z!2) = Y!3))),
% 0.19/0.43 inference(monotonicity,[status(thm)],[381])).
% 0.19/0.44 tff(383,assumption,(~(Z!2 = max(X!4, Y!3))), introduced(assumption)).
% 0.19/0.44 tff(384,plain,
% 0.19/0.44 (~(max(Y!3, Z!2) = Y!3)),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[383, 382])).
% 0.19/0.44 tff(385,plain,
% 0.19/0.44 (((~![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))) | ((~lesseq(Z!2, Y!3)) | (max(Y!3, Z!2) = Y!3))) <=> ((~![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))) | (~lesseq(Z!2, Y!3)) | (max(Y!3, Z!2) = Y!3))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(386,plain,
% 0.19/0.44 ((~![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))) | ((~lesseq(Z!2, Y!3)) | (max(Y!3, Z!2) = Y!3))),
% 0.19/0.44 inference(quant_inst,[status(thm)],[])).
% 0.19/0.44 tff(387,plain,
% 0.19/0.44 ((~![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))) | (~lesseq(Z!2, Y!3)) | (max(Y!3, Z!2) = Y!3)),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[386, 385])).
% 0.19/0.44 tff(388,plain,
% 0.19/0.44 ((~lesseq(Z!2, Y!3)) | (max(Y!3, Z!2) = Y!3)),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[387, 125])).
% 0.19/0.44 tff(389,plain,
% 0.19/0.44 (~lesseq(Z!2, Y!3)),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[388, 384])).
% 0.19/0.44 tff(390,plain,
% 0.19/0.44 (((~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | ((~model_ub(X!4, Y!3, Y!3)) | lesseq(Z!2, Y!3))) <=> ((~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | (~model_ub(X!4, Y!3, Y!3)) | lesseq(Z!2, Y!3))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(391,plain,
% 0.19/0.44 ((~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | ((~model_ub(X!4, Y!3, Y!3)) | lesseq(Z!2, Y!3))),
% 0.19/0.44 inference(quant_inst,[status(thm)],[])).
% 0.19/0.44 tff(392,plain,
% 0.19/0.44 ((~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | (~model_ub(X!4, Y!3, Y!3)) | lesseq(Z!2, Y!3)),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[391, 390])).
% 0.19/0.44 tff(393,plain,
% 0.19/0.44 ($false),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[392, 318, 389, 362])).
% 0.19/0.44 tff(394,plain,((~lesseq(X!4, Y!3)) | (Z!2 = max(X!4, Y!3))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.44 tff(395,plain,
% 0.19/0.44 (~lesseq(X!4, Y!3)),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[394, 329])).
% 0.19/0.44 tff(396,assumption,(~lesseq(X!4, Y!3)), introduced(assumption)).
% 0.19/0.44 tff(397,plain,
% 0.19/0.44 (((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | (lesseq(Y!3, X!4) | lesseq(X!4, Y!3))) <=> ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(Y!3, X!4) | lesseq(X!4, Y!3))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(398,plain,
% 0.19/0.44 ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | (lesseq(Y!3, X!4) | lesseq(X!4, Y!3))),
% 0.19/0.44 inference(quant_inst,[status(thm)],[])).
% 0.19/0.44 tff(399,plain,
% 0.19/0.44 ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(Y!3, X!4) | lesseq(X!4, Y!3)),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[398, 397])).
% 0.19/0.44 tff(400,plain,
% 0.19/0.44 (lesseq(Y!3, X!4)),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[399, 205, 396])).
% 0.19/0.44 tff(401,assumption,(~lesseq(X!4, X!4)), introduced(assumption)).
% 0.19/0.44 tff(402,plain,
% 0.19/0.44 (((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(X!4, X!4)) <=> ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(X!4, X!4))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(403,plain,
% 0.19/0.44 ((lesseq(X!4, X!4) | lesseq(X!4, X!4)) <=> lesseq(X!4, X!4)),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(404,plain,
% 0.19/0.44 (((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | (lesseq(X!4, X!4) | lesseq(X!4, X!4))) <=> ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(X!4, X!4))),
% 0.19/0.44 inference(monotonicity,[status(thm)],[403])).
% 0.19/0.44 tff(405,plain,
% 0.19/0.44 (((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | (lesseq(X!4, X!4) | lesseq(X!4, X!4))) <=> ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(X!4, X!4))),
% 0.19/0.44 inference(transitivity,[status(thm)],[404, 402])).
% 0.19/0.44 tff(406,plain,
% 0.19/0.44 ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | (lesseq(X!4, X!4) | lesseq(X!4, X!4))),
% 0.19/0.44 inference(quant_inst,[status(thm)],[])).
% 0.19/0.44 tff(407,plain,
% 0.19/0.44 ((~![X: $i, Y: $i] : (lesseq(X, Y) | lesseq(Y, X))) | lesseq(X!4, X!4)),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[406, 405])).
% 0.19/0.44 tff(408,plain,
% 0.19/0.44 ($false),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[407, 205, 401])).
% 0.19/0.44 tff(409,plain,(lesseq(X!4, X!4)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.44 tff(410,plain,
% 0.19/0.44 ((~((~lesseq(Y!3, X!4)) | (~lesseq(X!4, X!4)))) | (~lesseq(Y!3, X!4)) | (~lesseq(X!4, X!4))),
% 0.19/0.44 inference(tautology,[status(thm)],[])).
% 0.19/0.44 tff(411,plain,
% 0.19/0.44 ((~((~lesseq(Y!3, X!4)) | (~lesseq(X!4, X!4)))) | (~lesseq(Y!3, X!4))),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[410, 409])).
% 0.19/0.44 tff(412,plain,
% 0.19/0.44 (~((~lesseq(Y!3, X!4)) | (~lesseq(X!4, X!4)))),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[411, 400])).
% 0.19/0.44 tff(413,assumption,(((~lesseq(Y!3, X!4)) | (~lesseq(X!4, X!4))) <=> ub(X!4, Y!3, X!4)), introduced(assumption)).
% 0.19/0.44 tff(414,plain,
% 0.19/0.44 ((~![X: $i, Y: $i, Z: $i] : (~(((~lesseq(Y, Z)) | (~lesseq(X, Z))) <=> ub(X, Y, Z)))) | (~(((~lesseq(Y!3, X!4)) | (~lesseq(X!4, X!4))) <=> ub(X!4, Y!3, X!4)))),
% 0.19/0.44 inference(quant_inst,[status(thm)],[])).
% 0.19/0.44 tff(415,plain,
% 0.19/0.44 ($false),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[414, 81, 413])).
% 0.19/0.44 tff(416,plain,(~(((~lesseq(Y!3, X!4)) | (~lesseq(X!4, X!4))) <=> ub(X!4, Y!3, X!4))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.44 tff(417,plain,
% 0.19/0.44 ((((~lesseq(Y!3, X!4)) | (~lesseq(X!4, X!4))) <=> ub(X!4, Y!3, X!4)) | ((~lesseq(Y!3, X!4)) | (~lesseq(X!4, X!4))) | ub(X!4, Y!3, X!4)),
% 0.19/0.44 inference(tautology,[status(thm)],[])).
% 0.19/0.44 tff(418,plain,
% 0.19/0.44 (((~lesseq(Y!3, X!4)) | (~lesseq(X!4, X!4))) | ub(X!4, Y!3, X!4)),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[417, 416])).
% 0.19/0.44 tff(419,plain,
% 0.19/0.44 (ub(X!4, Y!3, X!4)),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[418, 412])).
% 0.19/0.44 tff(420,assumption,(~(model_ub(X!4, Y!3, X!4) <=> ub(X!4, Y!3, X!4))), introduced(assumption)).
% 0.19/0.44 tff(421,plain,
% 0.19/0.44 ((~![X: $i, Y: $i, N: $i] : (model_ub(X, Y, N) <=> ub(X, Y, N))) | (model_ub(X!4, Y!3, X!4) <=> ub(X!4, Y!3, X!4))),
% 0.19/0.44 inference(quant_inst,[status(thm)],[])).
% 0.19/0.44 tff(422,plain,
% 0.19/0.44 ($false),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[421, 90, 420])).
% 0.19/0.44 tff(423,plain,(model_ub(X!4, Y!3, X!4) <=> ub(X!4, Y!3, X!4)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.44 tff(424,plain,
% 0.19/0.44 ((~(model_ub(X!4, Y!3, X!4) <=> ub(X!4, Y!3, X!4))) | model_ub(X!4, Y!3, X!4) | (~ub(X!4, Y!3, X!4))),
% 0.19/0.44 inference(tautology,[status(thm)],[])).
% 0.19/0.44 tff(425,plain,
% 0.19/0.44 (model_ub(X!4, Y!3, X!4) | (~ub(X!4, Y!3, X!4))),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[424, 423])).
% 0.19/0.44 tff(426,plain,
% 0.19/0.44 (model_ub(X!4, Y!3, X!4)),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[425, 419])).
% 0.19/0.44 tff(427,plain,
% 0.19/0.44 (max(X!4, Y!3) = X!4),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[129, 400])).
% 0.19/0.44 tff(428,plain,
% 0.19/0.44 (((~lesseq(Y!3, Z!2)) | (~lesseq(X!4, Z!2))) | lesseq(X!4, Z!2)),
% 0.19/0.44 inference(tautology,[status(thm)],[])).
% 0.19/0.44 tff(429,plain,
% 0.19/0.44 (lesseq(X!4, Z!2)),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[428, 373])).
% 0.19/0.44 tff(430,plain,
% 0.19/0.44 (((~![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))) | ((~lesseq(X!4, Z!2)) | (max(X!4, Z!2) = Z!2))) <=> ((~![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))) | (~lesseq(X!4, Z!2)) | (max(X!4, Z!2) = Z!2))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(431,plain,
% 0.19/0.44 ((~![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))) | ((~lesseq(X!4, Z!2)) | (max(X!4, Z!2) = Z!2))),
% 0.19/0.44 inference(quant_inst,[status(thm)],[])).
% 0.19/0.44 tff(432,plain,
% 0.19/0.44 ((~![X: $i, Y: $i] : ((~lesseq(X, Y)) | (max(X, Y) = Y))) | (~lesseq(X!4, Z!2)) | (max(X!4, Z!2) = Z!2)),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[431, 430])).
% 0.19/0.44 tff(433,plain,
% 0.19/0.44 (max(X!4, Z!2) = Z!2),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[432, 219, 429])).
% 0.19/0.44 tff(434,plain,
% 0.19/0.44 (Z!2 = max(X!4, Z!2)),
% 0.19/0.44 inference(symmetry,[status(thm)],[433])).
% 0.19/0.44 tff(435,plain,
% 0.19/0.44 ((Z!2 = max(X!4, Y!3)) <=> (max(X!4, Z!2) = X!4)),
% 0.19/0.44 inference(monotonicity,[status(thm)],[434, 427])).
% 0.19/0.44 tff(436,plain,
% 0.19/0.44 ((~(Z!2 = max(X!4, Y!3))) <=> (~(max(X!4, Z!2) = X!4))),
% 0.19/0.44 inference(monotonicity,[status(thm)],[435])).
% 0.19/0.44 tff(437,plain,
% 0.19/0.44 (~(max(X!4, Z!2) = X!4)),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[383, 436])).
% 0.19/0.44 tff(438,plain,
% 0.19/0.44 (((~![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))) | ((~lesseq(Z!2, X!4)) | (max(X!4, Z!2) = X!4))) <=> ((~![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))) | (~lesseq(Z!2, X!4)) | (max(X!4, Z!2) = X!4))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(439,plain,
% 0.19/0.44 ((~![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))) | ((~lesseq(Z!2, X!4)) | (max(X!4, Z!2) = X!4))),
% 0.19/0.44 inference(quant_inst,[status(thm)],[])).
% 0.19/0.44 tff(440,plain,
% 0.19/0.44 ((~![X: $i, Y: $i] : ((~lesseq(Y, X)) | (max(X, Y) = X))) | (~lesseq(Z!2, X!4)) | (max(X!4, Z!2) = X!4)),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[439, 438])).
% 0.19/0.44 tff(441,plain,
% 0.19/0.44 ((~lesseq(Z!2, X!4)) | (max(X!4, Z!2) = X!4)),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[440, 125])).
% 0.19/0.44 tff(442,plain,
% 0.19/0.44 (~lesseq(Z!2, X!4)),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[441, 437])).
% 0.19/0.44 tff(443,plain,
% 0.19/0.44 (((~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | ((~model_ub(X!4, Y!3, X!4)) | lesseq(Z!2, X!4))) <=> ((~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | (~model_ub(X!4, Y!3, X!4)) | lesseq(Z!2, X!4))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(444,plain,
% 0.19/0.44 ((~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | ((~model_ub(X!4, Y!3, X!4)) | lesseq(Z!2, X!4))),
% 0.19/0.44 inference(quant_inst,[status(thm)],[])).
% 0.19/0.44 tff(445,plain,
% 0.19/0.44 ((~![Z: $i] : ((~model_ub(X!4, Y!3, Z)) | lesseq(Z!2, Z))) | (~model_ub(X!4, Y!3, X!4)) | lesseq(Z!2, X!4)),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[444, 443])).
% 0.19/0.44 tff(446,plain,
% 0.19/0.44 ($false),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[445, 318, 442, 426])).
% 0.19/0.44 tff(447,plain,((Z!2 = max(X!4, Y!3)) | lesseq(X!4, Y!3)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.44 tff(448,plain,
% 0.19/0.44 ($false),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[447, 395, 329])).
% 0.19/0.44 % SZS output end Proof
% 0.19/0.44 % E exiting
%------------------------------------------------------------------------------