%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : MGT085+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n031.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:24:12 AM UTC 2026
% Result : Theorem 0.12s 0.41s
% Output : Proof 0.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT085+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.07/0.34 % Computer : n031.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 7 14:22:43 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.12/0.41 % SZS status Theorem
% 0.12/0.41 % SZS output start Proof
% 0.12/0.41 tff(leq_type, type, (
% 0.12/0.41 leq: ( $i * $i ) > $o)).
% 0.12/0.41 tff(v200_type, type, (
% 0.12/0.41 v200: $i)).
% 0.12/0.41 tff(tptp_fun_Y_3_type, type, (
% 0.12/0.41 tptp_fun_Y_3: $i)).
% 0.12/0.41 tff(v100_type, type, (
% 0.12/0.41 v100: $i)).
% 0.12/0.41 tff(less_type, type, (
% 0.12/0.41 less: ( $i * $i ) > $o)).
% 0.12/0.41 tff(v0_type, type, (
% 0.12/0.41 v0: $i)).
% 0.12/0.41 tff(in_lopen_type, type, (
% 0.12/0.41 in_lopen: ( $i * $i * $i ) > $o)).
% 0.12/0.41 tff(tptp_fun_X_4_type, type, (
% 0.12/0.41 tptp_fun_X_4: $i)).
% 0.12/0.41 tff(v400_type, type, (
% 0.12/0.41 v400: $i)).
% 0.12/0.41 tff(tptp_fun_Z_2_type, type, (
% 0.12/0.41 tptp_fun_Z_2: $i)).
% 0.12/0.41 tff(v50_type, type, (
% 0.12/0.41 v50: $i)).
% 0.12/0.41 tff(1,plain,
% 0.12/0.41 (^[X: $i, A: $i, B: $i] : refl((~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B))) <=> (~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B))))),
% 0.12/0.41 inference(bind,[status(th)],[])).
% 0.12/0.41 tff(2,plain,
% 0.12/0.41 (![X: $i, A: $i, B: $i] : (~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B))) <=> ![X: $i, A: $i, B: $i] : (~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B)))),
% 0.12/0.41 inference(quant_intro,[status(thm)],[1])).
% 0.12/0.41 tff(3,plain,
% 0.12/0.41 (^[X: $i, A: $i, B: $i] : trans(trans(monotonicity(rewrite((less(A, X) & leq(X, B)) <=> (~((~leq(X, B)) | (~less(A, X))))), ((in_lopen(X, A, B) <=> (less(A, X) & leq(X, B))) <=> (in_lopen(X, A, B) <=> (~((~leq(X, B)) | (~less(A, X))))))), rewrite((in_lopen(X, A, B) <=> (~((~leq(X, B)) | (~less(A, X))))) <=> (~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B)))), ((in_lopen(X, A, B) <=> (less(A, X) & leq(X, B))) <=> (~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B))))), rewrite((~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B))) <=> (~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B)))), ((in_lopen(X, A, B) <=> (less(A, X) & leq(X, B))) <=> (~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B)))))),
% 0.12/0.41 inference(bind,[status(th)],[])).
% 0.12/0.41 tff(4,plain,
% 0.12/0.41 (![X: $i, A: $i, B: $i] : (in_lopen(X, A, B) <=> (less(A, X) & leq(X, B))) <=> ![X: $i, A: $i, B: $i] : (~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B)))),
% 0.12/0.41 inference(quant_intro,[status(thm)],[3])).
% 0.12/0.41 tff(5,plain,
% 0.12/0.41 (![X: $i, A: $i, B: $i] : (in_lopen(X, A, B) <=> (less(A, X) & leq(X, B))) <=> ![X: $i, A: $i, B: $i] : (in_lopen(X, A, B) <=> (less(A, X) & leq(X, B)))),
% 0.12/0.41 inference(rewrite,[status(thm)],[])).
% 0.12/0.41 tff(6,axiom,(![X: $i, A: $i, B: $i] : (in_lopen(X, A, B) <=> (less(A, X) & leq(X, B)))), file('/export/starexec/sandbox/benchmark/Axioms/MGT002+2.ax','in_lopen')).
% 0.12/0.41 tff(7,plain,
% 0.12/0.41 (![X: $i, A: $i, B: $i] : (in_lopen(X, A, B) <=> (less(A, X) & leq(X, B)))),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.12/0.41 tff(8,plain,(
% 0.12/0.41 ![X: $i, A: $i, B: $i] : (in_lopen(X, A, B) <=> (less(A, X) & leq(X, B)))),
% 0.12/0.41 inference(skolemize,[status(sab)],[7])).
% 0.12/0.41 tff(9,plain,
% 0.12/0.41 (![X: $i, A: $i, B: $i] : (~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B)))),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[8, 4])).
% 0.12/0.41 tff(10,plain,
% 0.12/0.41 (![X: $i, A: $i, B: $i] : (~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B)))),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[9, 2])).
% 0.12/0.41 tff(11,plain,
% 0.12/0.41 ((~![X: $i, A: $i, B: $i] : (~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B)))) | (~(((~leq(Y!3, v100)) | (~less(v0, Y!3))) <=> in_lopen(Y!3, v0, v100)))),
% 0.12/0.41 inference(quant_inst,[status(thm)],[])).
% 0.12/0.41 tff(12,plain,
% 0.12/0.41 (~(((~leq(Y!3, v100)) | (~less(v0, Y!3))) <=> in_lopen(Y!3, v0, v100))),
% 0.12/0.41 inference(unit_resolution,[status(thm)],[11, 10])).
% 0.12/0.41 tff(13,assumption,(((~leq(X!4, v200)) | (~less(v0, X!4))) <=> in_lopen(X!4, v0, v200)), introduced(assumption)).
% 0.12/0.41 tff(14,plain,
% 0.12/0.41 ((~![X: $i, A: $i, B: $i] : (~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B)))) | (~(((~leq(X!4, v200)) | (~less(v0, X!4))) <=> in_lopen(X!4, v0, v200)))),
% 0.12/0.41 inference(quant_inst,[status(thm)],[])).
% 0.12/0.41 tff(15,plain,
% 0.12/0.41 ($false),
% 0.12/0.41 inference(unit_resolution,[status(thm)],[14, 10, 13])).
% 0.12/0.41 tff(16,plain,(~(((~leq(X!4, v200)) | (~less(v0, X!4))) <=> in_lopen(X!4, v0, v200))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.41 tff(17,assumption,(leq(X!4, v200)), introduced(assumption)).
% 0.12/0.41 tff(18,plain,
% 0.12/0.41 (less(v200, v400) <=> less(v200, v400)),
% 0.12/0.41 inference(rewrite,[status(thm)],[])).
% 0.12/0.41 tff(19,axiom,(less(v200, v400)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','ord_v200_v400')).
% 0.12/0.42 tff(20,plain,
% 0.12/0.42 (less(v200, v400)),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[19, 18])).
% 0.12/0.42 tff(21,plain,
% 0.12/0.42 (^[X: $i, Y: $i] : refl(((~less(X, Y)) | leq(X, Y)) <=> ((~less(X, Y)) | leq(X, Y)))),
% 0.12/0.42 inference(bind,[status(th)],[])).
% 0.12/0.42 tff(22,plain,
% 0.12/0.42 (![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y)) <=> ![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.12/0.42 inference(quant_intro,[status(thm)],[21])).
% 0.12/0.42 tff(23,plain,
% 0.12/0.42 (![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y)) <=> ![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.12/0.42 inference(rewrite,[status(thm)],[])).
% 0.12/0.42 tff(24,plain,
% 0.12/0.42 (^[X: $i, Y: $i] : rewrite((less(X, Y) => leq(X, Y)) <=> ((~less(X, Y)) | leq(X, Y)))),
% 0.12/0.42 inference(bind,[status(th)],[])).
% 0.12/0.42 tff(25,plain,
% 0.12/0.42 (![X: $i, Y: $i] : (less(X, Y) => leq(X, Y)) <=> ![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.12/0.42 inference(quant_intro,[status(thm)],[24])).
% 0.12/0.42 tff(26,axiom,(![X: $i, Y: $i] : (less(X, Y) => leq(X, Y))), file('/export/starexec/sandbox/benchmark/Axioms/MGT002+0.ax','less_implies_leq')).
% 0.12/0.42 tff(27,plain,
% 0.12/0.42 (![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[26, 25])).
% 0.12/0.42 tff(28,plain,
% 0.12/0.42 (![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[27, 23])).
% 0.12/0.42 tff(29,plain,(
% 0.12/0.42 ![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.12/0.42 inference(skolemize,[status(sab)],[28])).
% 0.12/0.42 tff(30,plain,
% 0.12/0.42 (![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[29, 22])).
% 0.12/0.42 tff(31,plain,
% 0.12/0.42 (((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | ((~less(v200, v400)) | leq(v200, v400))) <=> ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | (~less(v200, v400)) | leq(v200, v400))),
% 0.12/0.42 inference(rewrite,[status(thm)],[])).
% 0.12/0.42 tff(32,plain,
% 0.12/0.42 ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | ((~less(v200, v400)) | leq(v200, v400))),
% 0.12/0.42 inference(quant_inst,[status(thm)],[])).
% 0.12/0.42 tff(33,plain,
% 0.12/0.42 ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | (~less(v200, v400)) | leq(v200, v400)),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[32, 31])).
% 0.12/0.42 tff(34,plain,
% 0.12/0.42 (leq(v200, v400)),
% 0.12/0.42 inference(unit_resolution,[status(thm)],[33, 30, 20])).
% 0.12/0.42 tff(35,plain,
% 0.12/0.42 (![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y))) <=> ![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))),
% 0.12/0.42 inference(rewrite,[status(thm)],[])).
% 0.12/0.42 tff(36,plain,
% 0.12/0.42 (^[X: $i, Y: $i, Z: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(X, Y) & leq(Y, Z)) <=> (~((~leq(Y, Z)) | (~leq(X, Y))))), ((~(leq(X, Y) & leq(Y, Z))) <=> (~(~((~leq(Y, Z)) | (~leq(X, Y))))))), rewrite((~(~((~leq(Y, Z)) | (~leq(X, Y))))) <=> ((~leq(Y, Z)) | (~leq(X, Y)))), ((~(leq(X, Y) & leq(Y, Z))) <=> ((~leq(Y, Z)) | (~leq(X, Y))))), (((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)) <=> (((~leq(Y, Z)) | (~leq(X, Y))) | leq(X, Z)))), rewrite((((~leq(Y, Z)) | (~leq(X, Y))) | leq(X, Z)) <=> (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))), (((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)) <=> (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))))),
% 0.12/0.42 inference(bind,[status(th)],[])).
% 0.12/0.42 tff(37,plain,
% 0.12/0.42 (![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))),
% 0.12/0.42 inference(quant_intro,[status(thm)],[36])).
% 0.12/0.42 tff(38,plain,
% 0.12/0.42 (![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 0.12/0.42 inference(rewrite,[status(thm)],[])).
% 0.12/0.42 tff(39,plain,
% 0.12/0.42 (^[X: $i, Y: $i, Z: $i] : rewrite(((leq(X, Y) & leq(Y, Z)) => leq(X, Z)) <=> ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)))),
% 0.12/0.42 inference(bind,[status(th)],[])).
% 0.12/0.42 tff(40,plain,
% 0.12/0.42 (![X: $i, Y: $i, Z: $i] : ((leq(X, Y) & leq(Y, Z)) => leq(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 0.12/0.42 inference(quant_intro,[status(thm)],[39])).
% 0.12/0.42 tff(41,axiom,(![X: $i, Y: $i, Z: $i] : ((leq(X, Y) & leq(Y, Z)) => leq(X, Z))), file('/export/starexec/sandbox/benchmark/Axioms/MGT002+0.ax','leq_trans')).
% 0.12/0.42 tff(42,plain,
% 0.12/0.42 (![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[41, 40])).
% 0.12/0.42 tff(43,plain,
% 0.12/0.42 (![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[42, 38])).
% 0.12/0.42 tff(44,plain,(
% 0.12/0.42 ![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 0.12/0.42 inference(skolemize,[status(sab)],[43])).
% 0.12/0.42 tff(45,plain,
% 0.12/0.42 (![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[44, 37])).
% 0.12/0.42 tff(46,plain,
% 0.12/0.42 (![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[45, 35])).
% 0.12/0.42 tff(47,plain,
% 0.12/0.42 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(v200, v400)) | (~leq(X!4, v200)) | leq(X!4, v400))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v200, v400)) | (~leq(X!4, v200)) | leq(X!4, v400))),
% 0.12/0.42 inference(rewrite,[status(thm)],[])).
% 0.12/0.42 tff(48,plain,
% 0.12/0.42 ((leq(X!4, v400) | (~leq(v200, v400)) | (~leq(X!4, v200))) <=> ((~leq(v200, v400)) | (~leq(X!4, v200)) | leq(X!4, v400))),
% 0.12/0.42 inference(rewrite,[status(thm)],[])).
% 0.12/0.42 tff(49,plain,
% 0.12/0.42 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(X!4, v400) | (~leq(v200, v400)) | (~leq(X!4, v200)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(v200, v400)) | (~leq(X!4, v200)) | leq(X!4, v400)))),
% 0.12/0.42 inference(monotonicity,[status(thm)],[48])).
% 0.12/0.42 tff(50,plain,
% 0.12/0.42 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(X!4, v400) | (~leq(v200, v400)) | (~leq(X!4, v200)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v200, v400)) | (~leq(X!4, v200)) | leq(X!4, v400))),
% 0.12/0.42 inference(transitivity,[status(thm)],[49, 47])).
% 0.12/0.42 tff(51,plain,
% 0.12/0.42 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(X!4, v400) | (~leq(v200, v400)) | (~leq(X!4, v200)))),
% 0.12/0.42 inference(quant_inst,[status(thm)],[])).
% 0.12/0.42 tff(52,plain,
% 0.12/0.42 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v200, v400)) | (~leq(X!4, v200)) | leq(X!4, v400)),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[51, 50])).
% 0.12/0.42 tff(53,plain,
% 0.12/0.42 (leq(X!4, v400)),
% 0.12/0.42 inference(unit_resolution,[status(thm)],[52, 46, 34, 17])).
% 0.12/0.42 tff(54,plain,
% 0.12/0.42 ((X!4 = v400) <=> (v400 = X!4)),
% 0.12/0.42 inference(commutativity,[status(thm)],[])).
% 0.12/0.42 tff(55,plain,
% 0.12/0.42 (((in_lopen(Z!2, v0, v50) | in_lopen(Y!3, v0, v100) | in_lopen(X!4, v0, v200)) & leq(v400, X!4) & leq(v200, Y!3) & leq(v100, Z!2)) <=> ((in_lopen(Z!2, v0, v50) | in_lopen(Y!3, v0, v100) | in_lopen(X!4, v0, v200)) & leq(v400, X!4) & leq(v200, Y!3) & leq(v100, Z!2))),
% 0.12/0.42 inference(rewrite,[status(thm)],[])).
% 0.12/0.42 tff(56,plain,
% 0.12/0.42 (?[X: $i, Y: $i, Z: $i] : ((in_lopen(Z, v0, v50) | in_lopen(Y, v0, v100) | in_lopen(X, v0, v200)) & leq(v400, X) & leq(v200, Y) & leq(v100, Z)) <=> ?[X: $i, Y: $i, Z: $i] : ((in_lopen(Z, v0, v50) | in_lopen(Y, v0, v100) | in_lopen(X, v0, v200)) & leq(v400, X) & leq(v200, Y) & leq(v100, Z))),
% 0.12/0.42 inference(rewrite,[status(thm)],[])).
% 0.12/0.42 tff(57,plain,
% 0.12/0.42 ((~(~?[X: $i, Y: $i, Z: $i] : ((in_lopen(Z, v0, v50) | in_lopen(Y, v0, v100) | in_lopen(X, v0, v200)) & leq(v400, X) & leq(v200, Y) & leq(v100, Z)))) <=> ?[X: $i, Y: $i, Z: $i] : ((in_lopen(Z, v0, v50) | in_lopen(Y, v0, v100) | in_lopen(X, v0, v200)) & leq(v400, X) & leq(v200, Y) & leq(v100, Z))),
% 0.12/0.42 inference(rewrite,[status(thm)],[])).
% 0.12/0.42 tff(58,plain,
% 0.12/0.42 ((~?[X: $i, Y: $i, Z: $i] : (((((in_lopen(X, v0, v200) | in_lopen(Y, v0, v100)) | in_lopen(Z, v0, v50)) & leq(v400, X)) & leq(v200, Y)) & leq(v100, Z))) <=> (~?[X: $i, Y: $i, Z: $i] : ((in_lopen(Z, v0, v50) | in_lopen(Y, v0, v100) | in_lopen(X, v0, v200)) & leq(v400, X) & leq(v200, Y) & leq(v100, Z)))),
% 0.12/0.42 inference(rewrite,[status(thm)],[])).
% 0.12/0.42 tff(59,plain,
% 0.12/0.42 ((~(~?[X: $i, Y: $i, Z: $i] : (((((in_lopen(X, v0, v200) | in_lopen(Y, v0, v100)) | in_lopen(Z, v0, v50)) & leq(v400, X)) & leq(v200, Y)) & leq(v100, Z)))) <=> (~(~?[X: $i, Y: $i, Z: $i] : ((in_lopen(Z, v0, v50) | in_lopen(Y, v0, v100) | in_lopen(X, v0, v200)) & leq(v400, X) & leq(v200, Y) & leq(v100, Z))))),
% 0.12/0.42 inference(monotonicity,[status(thm)],[58])).
% 0.12/0.42 tff(60,plain,
% 0.12/0.42 ((~(~?[X: $i, Y: $i, Z: $i] : (((((in_lopen(X, v0, v200) | in_lopen(Y, v0, v100)) | in_lopen(Z, v0, v50)) & leq(v400, X)) & leq(v200, Y)) & leq(v100, Z)))) <=> ?[X: $i, Y: $i, Z: $i] : ((in_lopen(Z, v0, v50) | in_lopen(Y, v0, v100) | in_lopen(X, v0, v200)) & leq(v400, X) & leq(v200, Y) & leq(v100, Z))),
% 0.12/0.42 inference(transitivity,[status(thm)],[59, 57])).
% 0.12/0.42 tff(61,axiom,(~(~?[X: $i, Y: $i, Z: $i] : (((((in_lopen(X, v0, v200) | in_lopen(Y, v0, v100)) | in_lopen(Z, v0, v50)) & leq(v400, X)) & leq(v200, Y)) & leq(v100, Z)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','odrl445')).
% 0.12/0.42 tff(62,plain,
% 0.12/0.42 (?[X: $i, Y: $i, Z: $i] : ((in_lopen(Z, v0, v50) | in_lopen(Y, v0, v100) | in_lopen(X, v0, v200)) & leq(v400, X) & leq(v200, Y) & leq(v100, Z))),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[61, 60])).
% 0.12/0.42 tff(63,plain,
% 0.12/0.42 (?[X: $i, Y: $i, Z: $i] : ((in_lopen(Z, v0, v50) | in_lopen(Y, v0, v100) | in_lopen(X, v0, v200)) & leq(v400, X) & leq(v200, Y) & leq(v100, Z))),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[62, 56])).
% 0.12/0.42 tff(64,plain,(
% 0.12/0.42 (in_lopen(Z!2, v0, v50) | in_lopen(Y!3, v0, v100) | in_lopen(X!4, v0, v200)) & leq(v400, X!4) & leq(v200, Y!3) & leq(v100, Z!2)),
% 0.12/0.42 inference(skolemize,[status(sab)],[63])).
% 0.12/0.42 tff(65,plain,
% 0.12/0.42 ((in_lopen(Z!2, v0, v50) | in_lopen(Y!3, v0, v100) | in_lopen(X!4, v0, v200)) & leq(v400, X!4) & leq(v200, Y!3) & leq(v100, Z!2)),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[64, 55])).
% 0.12/0.42 tff(66,plain,
% 0.12/0.42 (leq(v400, X!4)),
% 0.12/0.42 inference(and_elim,[status(thm)],[65])).
% 0.12/0.42 tff(67,plain,
% 0.12/0.42 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(v400, X!4)) | leq(v200, X!4) | (~leq(v200, v400)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v400, X!4)) | leq(v200, X!4) | (~leq(v200, v400)))),
% 0.12/0.42 inference(rewrite,[status(thm)],[])).
% 0.12/0.42 tff(68,plain,
% 0.12/0.42 ((leq(v200, X!4) | (~leq(v400, X!4)) | (~leq(v200, v400))) <=> ((~leq(v400, X!4)) | leq(v200, X!4) | (~leq(v200, v400)))),
% 0.12/0.42 inference(rewrite,[status(thm)],[])).
% 0.12/0.42 tff(69,plain,
% 0.12/0.42 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(v200, X!4) | (~leq(v400, X!4)) | (~leq(v200, v400)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(v400, X!4)) | leq(v200, X!4) | (~leq(v200, v400))))),
% 0.12/0.42 inference(monotonicity,[status(thm)],[68])).
% 0.12/0.42 tff(70,plain,
% 0.12/0.42 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(v200, X!4) | (~leq(v400, X!4)) | (~leq(v200, v400)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v400, X!4)) | leq(v200, X!4) | (~leq(v200, v400)))),
% 0.12/0.42 inference(transitivity,[status(thm)],[69, 67])).
% 0.12/0.42 tff(71,plain,
% 0.12/0.42 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(v200, X!4) | (~leq(v400, X!4)) | (~leq(v200, v400)))),
% 0.12/0.42 inference(quant_inst,[status(thm)],[])).
% 0.12/0.42 tff(72,plain,
% 0.12/0.42 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v400, X!4)) | leq(v200, X!4) | (~leq(v200, v400))),
% 0.12/0.42 inference(modus_ponens,[status(thm)],[71, 70])).
% 0.12/0.42 tff(73,plain,
% 0.12/0.42 (leq(v200, X!4)),
% 0.12/0.42 inference(unit_resolution,[status(thm)],[72, 46, 66, 34])).
% 0.12/0.42 tff(74,plain,
% 0.12/0.42 (![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X))) <=> ![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))),
% 0.12/0.42 inference(rewrite,[status(thm)],[])).
% 0.12/0.42 tff(75,plain,
% 0.12/0.42 (^[X: $i, Y: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(X, Y) & leq(Y, X)) <=> (~((~leq(X, Y)) | (~leq(Y, X))))), ((~(leq(X, Y) & leq(Y, X))) <=> (~(~((~leq(X, Y)) | (~leq(Y, X))))))), rewrite((~(~((~leq(X, Y)) | (~leq(Y, X))))) <=> ((~leq(X, Y)) | (~leq(Y, X)))), ((~(leq(X, Y) & leq(Y, X))) <=> ((~leq(X, Y)) | (~leq(Y, X))))), (((~(leq(X, Y) & leq(Y, X))) | (X = Y)) <=> (((~leq(X, Y)) | (~leq(Y, X))) | (X = Y)))), rewrite((((~leq(X, Y)) | (~leq(Y, X))) | (X = Y)) <=> ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))), (((~(leq(X, Y) & leq(Y, X))) | (X = Y)) <=> ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))))),
% 0.12/0.43 inference(bind,[status(th)],[])).
% 0.12/0.43 tff(76,plain,
% 0.12/0.43 (![X: $i, Y: $i] : ((~(leq(X, Y) & leq(Y, X))) | (X = Y)) <=> ![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))),
% 0.12/0.43 inference(quant_intro,[status(thm)],[75])).
% 0.12/0.43 tff(77,plain,
% 0.12/0.43 (![X: $i, Y: $i] : ((~(leq(X, Y) & leq(Y, X))) | (X = Y)) <=> ![X: $i, Y: $i] : ((~(leq(X, Y) & leq(Y, X))) | (X = Y))),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(78,plain,
% 0.12/0.43 (^[X: $i, Y: $i] : rewrite(((leq(X, Y) & leq(Y, X)) => (X = Y)) <=> ((~(leq(X, Y) & leq(Y, X))) | (X = Y)))),
% 0.12/0.43 inference(bind,[status(th)],[])).
% 0.12/0.43 tff(79,plain,
% 0.12/0.43 (![X: $i, Y: $i] : ((leq(X, Y) & leq(Y, X)) => (X = Y)) <=> ![X: $i, Y: $i] : ((~(leq(X, Y) & leq(Y, X))) | (X = Y))),
% 0.12/0.43 inference(quant_intro,[status(thm)],[78])).
% 0.12/0.43 tff(80,axiom,(![X: $i, Y: $i] : ((leq(X, Y) & leq(Y, X)) => (X = Y))), file('/export/starexec/sandbox/benchmark/Axioms/MGT002+0.ax','leq_antisym')).
% 0.12/0.43 tff(81,plain,
% 0.12/0.43 (![X: $i, Y: $i] : ((~(leq(X, Y) & leq(Y, X))) | (X = Y))),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[80, 79])).
% 0.12/0.43 tff(82,plain,
% 0.12/0.43 (![X: $i, Y: $i] : ((~(leq(X, Y) & leq(Y, X))) | (X = Y))),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[81, 77])).
% 0.12/0.43 tff(83,plain,(
% 0.12/0.43 ![X: $i, Y: $i] : ((~(leq(X, Y) & leq(Y, X))) | (X = Y))),
% 0.12/0.43 inference(skolemize,[status(sab)],[82])).
% 0.12/0.43 tff(84,plain,
% 0.12/0.43 (![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[83, 76])).
% 0.12/0.43 tff(85,plain,
% 0.12/0.43 (![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[84, 74])).
% 0.12/0.43 tff(86,plain,
% 0.12/0.43 (((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | ((v200 = X!4) | (~leq(v200, X!4)) | (~leq(X!4, v200)))) <=> ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | (v200 = X!4) | (~leq(v200, X!4)) | (~leq(X!4, v200)))),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(87,plain,
% 0.12/0.43 ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | ((v200 = X!4) | (~leq(v200, X!4)) | (~leq(X!4, v200)))),
% 0.12/0.43 inference(quant_inst,[status(thm)],[])).
% 0.12/0.43 tff(88,plain,
% 0.12/0.43 ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | (v200 = X!4) | (~leq(v200, X!4)) | (~leq(X!4, v200))),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[87, 86])).
% 0.12/0.43 tff(89,plain,
% 0.12/0.43 (v200 = X!4),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[88, 85, 73, 17])).
% 0.12/0.43 tff(90,plain,
% 0.12/0.43 ((v200 = v400) <=> (X!4 = v400)),
% 0.12/0.43 inference(monotonicity,[status(thm)],[89])).
% 0.12/0.43 tff(91,plain,
% 0.12/0.43 ((v200 = v400) <=> (v400 = X!4)),
% 0.12/0.43 inference(transitivity,[status(thm)],[90, 54])).
% 0.12/0.43 tff(92,plain,
% 0.12/0.43 ((~(v200 = v400)) <=> (~(v400 = X!4))),
% 0.12/0.43 inference(monotonicity,[status(thm)],[91])).
% 0.12/0.43 tff(93,plain,
% 0.12/0.43 ((~(v200 = v400)) <=> (~(v200 = v400))),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(94,axiom,((((((((((~(v0 = v50)) & (~(v0 = v100))) & (~(v0 = v200))) & (~(v0 = v400))) & (~(v50 = v100))) & (~(v50 = v200))) & (~(v50 = v400))) & (~(v100 = v200))) & (~(v100 = v400))) & (~(v200 = v400))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','distinct')).
% 0.12/0.43 tff(95,plain,
% 0.12/0.43 (~(v200 = v400)),
% 0.12/0.43 inference(and_elim,[status(thm)],[94])).
% 0.12/0.43 tff(96,plain,
% 0.12/0.43 (~(v200 = v400)),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[95, 93])).
% 0.12/0.43 tff(97,plain,
% 0.12/0.43 (~(v400 = X!4)),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[96, 92])).
% 0.12/0.43 tff(98,plain,
% 0.12/0.43 (((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | ((v400 = X!4) | (~leq(v400, X!4)) | (~leq(X!4, v400)))) <=> ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | (v400 = X!4) | (~leq(v400, X!4)) | (~leq(X!4, v400)))),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(99,plain,
% 0.12/0.43 ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | ((v400 = X!4) | (~leq(v400, X!4)) | (~leq(X!4, v400)))),
% 0.12/0.43 inference(quant_inst,[status(thm)],[])).
% 0.12/0.43 tff(100,plain,
% 0.12/0.43 ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | (v400 = X!4) | (~leq(v400, X!4)) | (~leq(X!4, v400))),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[99, 98])).
% 0.12/0.43 tff(101,plain,
% 0.12/0.43 ($false),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[100, 85, 66, 97, 53])).
% 0.12/0.43 tff(102,plain,(~leq(X!4, v200)), inference(lemma,lemma(discharge,[]))).
% 0.12/0.43 tff(103,plain,
% 0.12/0.43 (((~leq(X!4, v200)) | (~less(v0, X!4))) | leq(X!4, v200)),
% 0.12/0.43 inference(tautology,[status(thm)],[])).
% 0.12/0.43 tff(104,plain,
% 0.12/0.43 ((~leq(X!4, v200)) | (~less(v0, X!4))),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[103, 102])).
% 0.12/0.43 tff(105,plain,
% 0.12/0.43 ((((~leq(X!4, v200)) | (~less(v0, X!4))) <=> in_lopen(X!4, v0, v200)) | (~((~leq(X!4, v200)) | (~less(v0, X!4)))) | (~in_lopen(X!4, v0, v200))),
% 0.12/0.43 inference(tautology,[status(thm)],[])).
% 0.12/0.43 tff(106,plain,
% 0.12/0.43 ((((~leq(X!4, v200)) | (~less(v0, X!4))) <=> in_lopen(X!4, v0, v200)) | (~in_lopen(X!4, v0, v200))),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[105, 104])).
% 0.12/0.43 tff(107,plain,
% 0.12/0.43 (~in_lopen(X!4, v0, v200)),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[106, 16])).
% 0.12/0.43 tff(108,assumption,(((~leq(Z!2, v50)) | (~less(v0, Z!2))) <=> in_lopen(Z!2, v0, v50)), introduced(assumption)).
% 0.12/0.43 tff(109,plain,
% 0.12/0.43 ((~![X: $i, A: $i, B: $i] : (~(((~leq(X, B)) | (~less(A, X))) <=> in_lopen(X, A, B)))) | (~(((~leq(Z!2, v50)) | (~less(v0, Z!2))) <=> in_lopen(Z!2, v0, v50)))),
% 0.12/0.43 inference(quant_inst,[status(thm)],[])).
% 0.12/0.43 tff(110,plain,
% 0.12/0.43 ($false),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[109, 10, 108])).
% 0.12/0.43 tff(111,plain,(~(((~leq(Z!2, v50)) | (~less(v0, Z!2))) <=> in_lopen(Z!2, v0, v50))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.43 tff(112,assumption,(leq(Z!2, v50)), introduced(assumption)).
% 0.12/0.43 tff(113,plain,
% 0.12/0.43 (less(v50, v100) <=> less(v50, v100)),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(114,axiom,(less(v50, v100)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','ord_v50_v100')).
% 0.12/0.43 tff(115,plain,
% 0.12/0.43 (less(v50, v100)),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[114, 113])).
% 0.12/0.43 tff(116,plain,
% 0.12/0.43 (((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | ((~less(v50, v100)) | leq(v50, v100))) <=> ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | (~less(v50, v100)) | leq(v50, v100))),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(117,plain,
% 0.12/0.43 ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | ((~less(v50, v100)) | leq(v50, v100))),
% 0.12/0.43 inference(quant_inst,[status(thm)],[])).
% 0.12/0.43 tff(118,plain,
% 0.12/0.43 ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | (~less(v50, v100)) | leq(v50, v100)),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[117, 116])).
% 0.12/0.43 tff(119,plain,
% 0.12/0.43 (leq(v50, v100)),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[118, 30, 115])).
% 0.12/0.43 tff(120,plain,
% 0.12/0.43 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(v50, v100)) | (~leq(Z!2, v50)) | leq(Z!2, v100))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v50, v100)) | (~leq(Z!2, v50)) | leq(Z!2, v100))),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(121,plain,
% 0.12/0.43 ((leq(Z!2, v100) | (~leq(v50, v100)) | (~leq(Z!2, v50))) <=> ((~leq(v50, v100)) | (~leq(Z!2, v50)) | leq(Z!2, v100))),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(122,plain,
% 0.12/0.43 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(Z!2, v100) | (~leq(v50, v100)) | (~leq(Z!2, v50)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(v50, v100)) | (~leq(Z!2, v50)) | leq(Z!2, v100)))),
% 0.12/0.43 inference(monotonicity,[status(thm)],[121])).
% 0.12/0.43 tff(123,plain,
% 0.12/0.43 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(Z!2, v100) | (~leq(v50, v100)) | (~leq(Z!2, v50)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v50, v100)) | (~leq(Z!2, v50)) | leq(Z!2, v100))),
% 0.12/0.43 inference(transitivity,[status(thm)],[122, 120])).
% 0.12/0.43 tff(124,plain,
% 0.12/0.43 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(Z!2, v100) | (~leq(v50, v100)) | (~leq(Z!2, v50)))),
% 0.12/0.43 inference(quant_inst,[status(thm)],[])).
% 0.12/0.43 tff(125,plain,
% 0.12/0.43 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v50, v100)) | (~leq(Z!2, v50)) | leq(Z!2, v100)),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[124, 123])).
% 0.12/0.43 tff(126,plain,
% 0.12/0.43 (leq(Z!2, v100)),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[125, 46, 119, 112])).
% 0.12/0.43 tff(127,plain,
% 0.12/0.43 ((Z!2 = v100) <=> (v100 = Z!2)),
% 0.12/0.43 inference(commutativity,[status(thm)],[])).
% 0.12/0.43 tff(128,plain,
% 0.12/0.43 (leq(v100, Z!2)),
% 0.12/0.43 inference(and_elim,[status(thm)],[65])).
% 0.12/0.43 tff(129,plain,
% 0.12/0.43 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(v100, Z!2)) | leq(v50, Z!2) | (~leq(v50, v100)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v100, Z!2)) | leq(v50, Z!2) | (~leq(v50, v100)))),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(130,plain,
% 0.12/0.43 ((leq(v50, Z!2) | (~leq(v100, Z!2)) | (~leq(v50, v100))) <=> ((~leq(v100, Z!2)) | leq(v50, Z!2) | (~leq(v50, v100)))),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(131,plain,
% 0.12/0.43 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(v50, Z!2) | (~leq(v100, Z!2)) | (~leq(v50, v100)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(v100, Z!2)) | leq(v50, Z!2) | (~leq(v50, v100))))),
% 0.12/0.43 inference(monotonicity,[status(thm)],[130])).
% 0.12/0.43 tff(132,plain,
% 0.12/0.43 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(v50, Z!2) | (~leq(v100, Z!2)) | (~leq(v50, v100)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v100, Z!2)) | leq(v50, Z!2) | (~leq(v50, v100)))),
% 0.12/0.43 inference(transitivity,[status(thm)],[131, 129])).
% 0.12/0.43 tff(133,plain,
% 0.12/0.43 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(v50, Z!2) | (~leq(v100, Z!2)) | (~leq(v50, v100)))),
% 0.12/0.43 inference(quant_inst,[status(thm)],[])).
% 0.12/0.43 tff(134,plain,
% 0.12/0.43 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v100, Z!2)) | leq(v50, Z!2) | (~leq(v50, v100))),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[133, 132])).
% 0.12/0.43 tff(135,plain,
% 0.12/0.43 (leq(v50, Z!2)),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[134, 46, 128, 119])).
% 0.12/0.43 tff(136,plain,
% 0.12/0.43 (((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | ((v50 = Z!2) | (~leq(v50, Z!2)) | (~leq(Z!2, v50)))) <=> ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | (v50 = Z!2) | (~leq(v50, Z!2)) | (~leq(Z!2, v50)))),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(137,plain,
% 0.12/0.43 ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | ((v50 = Z!2) | (~leq(v50, Z!2)) | (~leq(Z!2, v50)))),
% 0.12/0.43 inference(quant_inst,[status(thm)],[])).
% 0.12/0.43 tff(138,plain,
% 0.12/0.43 ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | (v50 = Z!2) | (~leq(v50, Z!2)) | (~leq(Z!2, v50))),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[137, 136])).
% 0.12/0.43 tff(139,plain,
% 0.12/0.43 (v50 = Z!2),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[138, 85, 135, 112])).
% 0.12/0.43 tff(140,plain,
% 0.12/0.43 ((v50 = v100) <=> (Z!2 = v100)),
% 0.12/0.43 inference(monotonicity,[status(thm)],[139])).
% 0.12/0.43 tff(141,plain,
% 0.12/0.43 ((v50 = v100) <=> (v100 = Z!2)),
% 0.12/0.43 inference(transitivity,[status(thm)],[140, 127])).
% 0.12/0.43 tff(142,plain,
% 0.12/0.43 ((~(v50 = v100)) <=> (~(v100 = Z!2))),
% 0.12/0.43 inference(monotonicity,[status(thm)],[141])).
% 0.12/0.43 tff(143,plain,
% 0.12/0.43 ((~(v50 = v100)) <=> (~(v50 = v100))),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(144,plain,
% 0.12/0.43 (((((((((~(v0 = v50)) & (~(v0 = v100))) & (~(v0 = v200))) & (~(v0 = v400))) & (~(v50 = v100))) & (~(v50 = v200))) & (~(v50 = v400))) & (~(v100 = v200))) & (~(v100 = v400))),
% 0.12/0.43 inference(and_elim,[status(thm)],[94])).
% 0.12/0.43 tff(145,plain,
% 0.12/0.43 ((((((((~(v0 = v50)) & (~(v0 = v100))) & (~(v0 = v200))) & (~(v0 = v400))) & (~(v50 = v100))) & (~(v50 = v200))) & (~(v50 = v400))) & (~(v100 = v200))),
% 0.12/0.43 inference(and_elim,[status(thm)],[144])).
% 0.12/0.43 tff(146,plain,
% 0.12/0.43 (((((((~(v0 = v50)) & (~(v0 = v100))) & (~(v0 = v200))) & (~(v0 = v400))) & (~(v50 = v100))) & (~(v50 = v200))) & (~(v50 = v400))),
% 0.12/0.43 inference(and_elim,[status(thm)],[145])).
% 0.12/0.43 tff(147,plain,
% 0.12/0.43 ((((((~(v0 = v50)) & (~(v0 = v100))) & (~(v0 = v200))) & (~(v0 = v400))) & (~(v50 = v100))) & (~(v50 = v200))),
% 0.12/0.43 inference(and_elim,[status(thm)],[146])).
% 0.12/0.43 tff(148,plain,
% 0.12/0.43 (((((~(v0 = v50)) & (~(v0 = v100))) & (~(v0 = v200))) & (~(v0 = v400))) & (~(v50 = v100))),
% 0.12/0.43 inference(and_elim,[status(thm)],[147])).
% 0.12/0.43 tff(149,plain,
% 0.12/0.43 (~(v50 = v100)),
% 0.12/0.43 inference(and_elim,[status(thm)],[148])).
% 0.12/0.43 tff(150,plain,
% 0.12/0.43 (~(v50 = v100)),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[149, 143])).
% 0.12/0.43 tff(151,plain,
% 0.12/0.43 (~(v100 = Z!2)),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[150, 142])).
% 0.12/0.43 tff(152,plain,
% 0.12/0.43 (((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | ((v100 = Z!2) | (~leq(v100, Z!2)) | (~leq(Z!2, v100)))) <=> ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | (v100 = Z!2) | (~leq(v100, Z!2)) | (~leq(Z!2, v100)))),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(153,plain,
% 0.12/0.43 ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | ((v100 = Z!2) | (~leq(v100, Z!2)) | (~leq(Z!2, v100)))),
% 0.12/0.43 inference(quant_inst,[status(thm)],[])).
% 0.12/0.43 tff(154,plain,
% 0.12/0.43 ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | (v100 = Z!2) | (~leq(v100, Z!2)) | (~leq(Z!2, v100))),
% 0.12/0.43 inference(modus_ponens,[status(thm)],[153, 152])).
% 0.12/0.43 tff(155,plain,
% 0.12/0.43 ($false),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[154, 85, 128, 151, 126])).
% 0.12/0.43 tff(156,plain,(~leq(Z!2, v50)), inference(lemma,lemma(discharge,[]))).
% 0.12/0.43 tff(157,plain,
% 0.12/0.43 (((~leq(Z!2, v50)) | (~less(v0, Z!2))) | leq(Z!2, v50)),
% 0.12/0.43 inference(tautology,[status(thm)],[])).
% 0.12/0.43 tff(158,plain,
% 0.12/0.43 ((~leq(Z!2, v50)) | (~less(v0, Z!2))),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[157, 156])).
% 0.12/0.43 tff(159,plain,
% 0.12/0.43 ((((~leq(Z!2, v50)) | (~less(v0, Z!2))) <=> in_lopen(Z!2, v0, v50)) | (~((~leq(Z!2, v50)) | (~less(v0, Z!2)))) | (~in_lopen(Z!2, v0, v50))),
% 0.12/0.43 inference(tautology,[status(thm)],[])).
% 0.12/0.43 tff(160,plain,
% 0.12/0.43 ((((~leq(Z!2, v50)) | (~less(v0, Z!2))) <=> in_lopen(Z!2, v0, v50)) | (~in_lopen(Z!2, v0, v50))),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[159, 158])).
% 0.12/0.43 tff(161,plain,
% 0.12/0.43 (~in_lopen(Z!2, v0, v50)),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[160, 111])).
% 0.12/0.43 tff(162,plain,
% 0.12/0.43 (in_lopen(Z!2, v0, v50) | in_lopen(Y!3, v0, v100) | in_lopen(X!4, v0, v200)),
% 0.12/0.43 inference(and_elim,[status(thm)],[65])).
% 0.12/0.43 tff(163,plain,
% 0.12/0.43 (in_lopen(Y!3, v0, v100) | in_lopen(X!4, v0, v200)),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[162, 161])).
% 0.12/0.43 tff(164,plain,
% 0.12/0.43 (in_lopen(Y!3, v0, v100)),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[163, 107])).
% 0.12/0.43 tff(165,plain,
% 0.12/0.43 ((((~leq(Y!3, v100)) | (~less(v0, Y!3))) <=> in_lopen(Y!3, v0, v100)) | (~((~leq(Y!3, v100)) | (~less(v0, Y!3)))) | (~in_lopen(Y!3, v0, v100))),
% 0.12/0.43 inference(tautology,[status(thm)],[])).
% 0.12/0.43 tff(166,plain,
% 0.12/0.43 ((((~leq(Y!3, v100)) | (~less(v0, Y!3))) <=> in_lopen(Y!3, v0, v100)) | (~((~leq(Y!3, v100)) | (~less(v0, Y!3))))),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[165, 164])).
% 0.12/0.43 tff(167,plain,
% 0.12/0.43 (~((~leq(Y!3, v100)) | (~less(v0, Y!3)))),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[166, 12])).
% 0.12/0.43 tff(168,plain,
% 0.12/0.43 (((~leq(Y!3, v100)) | (~less(v0, Y!3))) | leq(Y!3, v100)),
% 0.12/0.43 inference(tautology,[status(thm)],[])).
% 0.12/0.43 tff(169,plain,
% 0.12/0.43 (leq(Y!3, v100)),
% 0.12/0.43 inference(unit_resolution,[status(thm)],[168, 167])).
% 0.12/0.43 tff(170,plain,
% 0.12/0.43 (less(v100, v200) <=> less(v100, v200)),
% 0.12/0.43 inference(rewrite,[status(thm)],[])).
% 0.12/0.43 tff(171,axiom,(less(v100, v200)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','ord_v100_v200')).
% 0.12/0.44 tff(172,plain,
% 0.12/0.44 (less(v100, v200)),
% 0.12/0.44 inference(modus_ponens,[status(thm)],[171, 170])).
% 0.12/0.44 tff(173,plain,
% 0.12/0.44 (((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | ((~less(v100, v200)) | leq(v100, v200))) <=> ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | (~less(v100, v200)) | leq(v100, v200))),
% 0.12/0.44 inference(rewrite,[status(thm)],[])).
% 0.12/0.44 tff(174,plain,
% 0.12/0.44 ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | ((~less(v100, v200)) | leq(v100, v200))),
% 0.12/0.44 inference(quant_inst,[status(thm)],[])).
% 0.12/0.44 tff(175,plain,
% 0.12/0.44 ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | (~less(v100, v200)) | leq(v100, v200)),
% 0.12/0.44 inference(modus_ponens,[status(thm)],[174, 173])).
% 0.12/0.44 tff(176,plain,
% 0.12/0.44 (leq(v100, v200)),
% 0.12/0.44 inference(unit_resolution,[status(thm)],[175, 30, 172])).
% 0.12/0.44 tff(177,plain,
% 0.12/0.44 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(v100, v200)) | (~leq(Y!3, v100)) | leq(Y!3, v200))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v100, v200)) | (~leq(Y!3, v100)) | leq(Y!3, v200))),
% 0.12/0.44 inference(rewrite,[status(thm)],[])).
% 0.12/0.44 tff(178,plain,
% 0.12/0.44 ((leq(Y!3, v200) | (~leq(v100, v200)) | (~leq(Y!3, v100))) <=> ((~leq(v100, v200)) | (~leq(Y!3, v100)) | leq(Y!3, v200))),
% 0.12/0.44 inference(rewrite,[status(thm)],[])).
% 0.12/0.44 tff(179,plain,
% 0.12/0.44 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(Y!3, v200) | (~leq(v100, v200)) | (~leq(Y!3, v100)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(v100, v200)) | (~leq(Y!3, v100)) | leq(Y!3, v200)))),
% 0.12/0.44 inference(monotonicity,[status(thm)],[178])).
% 0.12/0.44 tff(180,plain,
% 0.12/0.44 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(Y!3, v200) | (~leq(v100, v200)) | (~leq(Y!3, v100)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v100, v200)) | (~leq(Y!3, v100)) | leq(Y!3, v200))),
% 0.12/0.44 inference(transitivity,[status(thm)],[179, 177])).
% 0.12/0.44 tff(181,plain,
% 0.12/0.44 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(Y!3, v200) | (~leq(v100, v200)) | (~leq(Y!3, v100)))),
% 0.12/0.44 inference(quant_inst,[status(thm)],[])).
% 0.12/0.44 tff(182,plain,
% 0.12/0.44 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v100, v200)) | (~leq(Y!3, v100)) | leq(Y!3, v200)),
% 0.12/0.44 inference(modus_ponens,[status(thm)],[181, 180])).
% 0.12/0.44 tff(183,plain,
% 0.12/0.44 (leq(Y!3, v200)),
% 0.12/0.44 inference(unit_resolution,[status(thm)],[182, 46, 176, 169])).
% 0.12/0.44 tff(184,plain,
% 0.12/0.44 ((Y!3 = v200) <=> (v200 = Y!3)),
% 0.12/0.44 inference(commutativity,[status(thm)],[])).
% 0.12/0.44 tff(185,plain,
% 0.12/0.44 (leq(v200, Y!3)),
% 0.12/0.44 inference(and_elim,[status(thm)],[65])).
% 0.12/0.44 tff(186,plain,
% 0.12/0.44 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(v200, Y!3)) | leq(v100, Y!3) | (~leq(v100, v200)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v200, Y!3)) | leq(v100, Y!3) | (~leq(v100, v200)))),
% 0.12/0.44 inference(rewrite,[status(thm)],[])).
% 0.12/0.44 tff(187,plain,
% 0.12/0.44 ((leq(v100, Y!3) | (~leq(v200, Y!3)) | (~leq(v100, v200))) <=> ((~leq(v200, Y!3)) | leq(v100, Y!3) | (~leq(v100, v200)))),
% 0.12/0.44 inference(rewrite,[status(thm)],[])).
% 0.12/0.44 tff(188,plain,
% 0.12/0.44 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(v100, Y!3) | (~leq(v200, Y!3)) | (~leq(v100, v200)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(v200, Y!3)) | leq(v100, Y!3) | (~leq(v100, v200))))),
% 0.12/0.44 inference(monotonicity,[status(thm)],[187])).
% 0.12/0.44 tff(189,plain,
% 0.12/0.44 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(v100, Y!3) | (~leq(v200, Y!3)) | (~leq(v100, v200)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v200, Y!3)) | leq(v100, Y!3) | (~leq(v100, v200)))),
% 0.12/0.44 inference(transitivity,[status(thm)],[188, 186])).
% 0.12/0.44 tff(190,plain,
% 0.12/0.44 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(v100, Y!3) | (~leq(v200, Y!3)) | (~leq(v100, v200)))),
% 0.12/0.44 inference(quant_inst,[status(thm)],[])).
% 0.12/0.44 tff(191,plain,
% 0.12/0.44 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(v200, Y!3)) | leq(v100, Y!3) | (~leq(v100, v200))),
% 0.12/0.44 inference(modus_ponens,[status(thm)],[190, 189])).
% 0.12/0.44 tff(192,plain,
% 0.12/0.44 (leq(v100, Y!3)),
% 0.12/0.44 inference(unit_resolution,[status(thm)],[191, 46, 185, 176])).
% 0.12/0.44 tff(193,plain,
% 0.12/0.44 (((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | ((v100 = Y!3) | (~leq(v100, Y!3)) | (~leq(Y!3, v100)))) <=> ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | (v100 = Y!3) | (~leq(v100, Y!3)) | (~leq(Y!3, v100)))),
% 0.12/0.44 inference(rewrite,[status(thm)],[])).
% 0.12/0.44 tff(194,plain,
% 0.12/0.44 ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | ((v100 = Y!3) | (~leq(v100, Y!3)) | (~leq(Y!3, v100)))),
% 0.12/0.44 inference(quant_inst,[status(thm)],[])).
% 0.12/0.44 tff(195,plain,
% 0.12/0.44 ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | (v100 = Y!3) | (~leq(v100, Y!3)) | (~leq(Y!3, v100))),
% 0.12/0.44 inference(modus_ponens,[status(thm)],[194, 193])).
% 0.12/0.44 tff(196,plain,
% 0.12/0.44 (v100 = Y!3),
% 0.12/0.44 inference(unit_resolution,[status(thm)],[195, 85, 192, 169])).
% 0.12/0.44 tff(197,plain,
% 0.12/0.44 ((v100 = v200) <=> (Y!3 = v200)),
% 0.12/0.44 inference(monotonicity,[status(thm)],[196])).
% 0.12/0.44 tff(198,plain,
% 0.12/0.44 ((v100 = v200) <=> (v200 = Y!3)),
% 0.12/0.44 inference(transitivity,[status(thm)],[197, 184])).
% 0.12/0.44 tff(199,plain,
% 0.12/0.44 ((~(v100 = v200)) <=> (~(v200 = Y!3))),
% 0.12/0.44 inference(monotonicity,[status(thm)],[198])).
% 0.12/0.44 tff(200,plain,
% 0.12/0.44 ((~(v100 = v200)) <=> (~(v100 = v200))),
% 0.12/0.44 inference(rewrite,[status(thm)],[])).
% 0.12/0.44 tff(201,plain,
% 0.12/0.44 (~(v100 = v200)),
% 0.12/0.44 inference(and_elim,[status(thm)],[145])).
% 0.12/0.44 tff(202,plain,
% 0.12/0.44 (~(v100 = v200)),
% 0.12/0.44 inference(modus_ponens,[status(thm)],[201, 200])).
% 0.12/0.44 tff(203,plain,
% 0.12/0.44 (~(v200 = Y!3)),
% 0.12/0.44 inference(modus_ponens,[status(thm)],[202, 199])).
% 0.12/0.44 tff(204,plain,
% 0.12/0.44 (((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | ((v200 = Y!3) | (~leq(v200, Y!3)) | (~leq(Y!3, v200)))) <=> ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | (v200 = Y!3) | (~leq(v200, Y!3)) | (~leq(Y!3, v200)))),
% 0.12/0.44 inference(rewrite,[status(thm)],[])).
% 0.12/0.44 tff(205,plain,
% 0.12/0.44 ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | ((v200 = Y!3) | (~leq(v200, Y!3)) | (~leq(Y!3, v200)))),
% 0.12/0.44 inference(quant_inst,[status(thm)],[])).
% 0.12/0.44 tff(206,plain,
% 0.12/0.44 ((~![X: $i, Y: $i] : ((X = Y) | (~leq(X, Y)) | (~leq(Y, X)))) | (v200 = Y!3) | (~leq(v200, Y!3)) | (~leq(Y!3, v200))),
% 0.12/0.44 inference(modus_ponens,[status(thm)],[205, 204])).
% 0.12/0.44 tff(207,plain,
% 0.12/0.44 ($false),
% 0.12/0.44 inference(unit_resolution,[status(thm)],[206, 85, 185, 203, 183])).
% 0.12/0.44 % SZS output end Proof
% 0.12/0.44 % E exiting
%------------------------------------------------------------------------------