%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : MGT091+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n026.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:13 AM UTC 2026
% Result : Theorem 0.21s 0.46s
% Output : Proof 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT091+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.07/0.34 % Computer : n026.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:27:14 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.21/0.46 % SZS status Theorem
% 0.21/0.46 % SZS output start Proof
% 0.21/0.46 tff(in_closed_type, type, (
% 0.21/0.46 in_closed: ( $i * $i * $i ) > $o)).
% 0.21/0.46 tff(v600_type, type, (
% 0.21/0.46 v600: $i)).
% 0.21/0.46 tff(v0_type, type, (
% 0.21/0.46 v0: $i)).
% 0.21/0.46 tff(v400_type, type, (
% 0.21/0.46 v400: $i)).
% 0.21/0.46 tff(leq_type, type, (
% 0.21/0.46 leq: ( $i * $i ) > $o)).
% 0.21/0.46 tff(less_type, type, (
% 0.21/0.46 less: ( $i * $i ) > $o)).
% 0.21/0.46 tff(v800_type, type, (
% 0.21/0.46 v800: $i)).
% 0.21/0.46 tff(axis_subsumes_type, type, (
% 0.21/0.46 axis_subsumes: ( $i * $i * $i * $i ) > $o)).
% 0.21/0.46 tff(tptp_fun_X_1_type, type, (
% 0.21/0.46 tptp_fun_X_1: ( $i * $i * $i * $i ) > $i)).
% 0.21/0.46 tff(axis_compatible_type, type, (
% 0.21/0.46 axis_compatible: ( $i * $i * $i * $i ) > $o)).
% 0.21/0.46 tff(tptp_fun_X_0_type, type, (
% 0.21/0.46 tptp_fun_X_0: ( $i * $i * $i * $i ) > $i)).
% 0.21/0.46 tff(box2_compatible_type, type, (
% 0.21/0.46 box2_compatible: ( $i * $i * $i * $i * $i * $i * $i * $i ) > $o)).
% 0.21/0.46 tff(1,plain,
% 0.21/0.46 (less(v400, v600) <=> less(v400, v600)),
% 0.21/0.46 inference(rewrite,[status(thm)],[])).
% 0.21/0.46 tff(2,axiom,(less(v400, v600)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','ord_v400_v600')).
% 0.21/0.46 tff(3,plain,
% 0.21/0.46 (less(v400, v600)),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[2, 1])).
% 0.21/0.46 tff(4,plain,
% 0.21/0.46 (^[X: $i, Y: $i] : refl(((~less(X, Y)) | leq(X, Y)) <=> ((~less(X, Y)) | leq(X, Y)))),
% 0.21/0.46 inference(bind,[status(th)],[])).
% 0.21/0.46 tff(5,plain,
% 0.21/0.46 (![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y)) <=> ![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.21/0.46 inference(quant_intro,[status(thm)],[4])).
% 0.21/0.46 tff(6,plain,
% 0.21/0.46 (![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y)) <=> ![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.21/0.46 inference(rewrite,[status(thm)],[])).
% 0.21/0.46 tff(7,plain,
% 0.21/0.46 (^[X: $i, Y: $i] : rewrite((less(X, Y) => leq(X, Y)) <=> ((~less(X, Y)) | leq(X, Y)))),
% 0.21/0.46 inference(bind,[status(th)],[])).
% 0.21/0.46 tff(8,plain,
% 0.21/0.46 (![X: $i, Y: $i] : (less(X, Y) => leq(X, Y)) <=> ![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.21/0.46 inference(quant_intro,[status(thm)],[7])).
% 0.21/0.46 tff(9,axiom,(![X: $i, Y: $i] : (less(X, Y) => leq(X, Y))), file('/export/starexec/sandbox/benchmark/Axioms/MGT002+0.ax','less_implies_leq')).
% 0.21/0.46 tff(10,plain,
% 0.21/0.46 (![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[9, 8])).
% 0.21/0.46 tff(11,plain,
% 0.21/0.46 (![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[10, 6])).
% 0.21/0.46 tff(12,plain,(
% 0.21/0.46 ![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.21/0.46 inference(skolemize,[status(sab)],[11])).
% 0.21/0.46 tff(13,plain,
% 0.21/0.46 (![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[12, 5])).
% 0.21/0.46 tff(14,plain,
% 0.21/0.46 (((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | ((~less(v400, v600)) | leq(v400, v600))) <=> ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | (~less(v400, v600)) | leq(v400, v600))),
% 0.21/0.46 inference(rewrite,[status(thm)],[])).
% 0.21/0.46 tff(15,plain,
% 0.21/0.46 ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | ((~less(v400, v600)) | leq(v400, v600))),
% 0.21/0.46 inference(quant_inst,[status(thm)],[])).
% 0.21/0.46 tff(16,plain,
% 0.21/0.46 ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | (~less(v400, v600)) | leq(v400, v600)),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.21/0.46 tff(17,plain,
% 0.21/0.46 (leq(v400, v600)),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[16, 13, 3])).
% 0.21/0.46 tff(18,plain,
% 0.21/0.46 (less(v0, v400) <=> less(v0, v400)),
% 0.21/0.46 inference(rewrite,[status(thm)],[])).
% 0.21/0.46 tff(19,axiom,(less(v0, v400)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','ord_v0_v400')).
% 0.21/0.46 tff(20,plain,
% 0.21/0.46 (less(v0, v400)),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[19, 18])).
% 0.21/0.46 tff(21,plain,
% 0.21/0.46 (((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | ((~less(v0, v400)) | leq(v0, v400))) <=> ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | (~less(v0, v400)) | leq(v0, v400))),
% 0.21/0.46 inference(rewrite,[status(thm)],[])).
% 0.21/0.46 tff(22,plain,
% 0.21/0.46 ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | ((~less(v0, v400)) | leq(v0, v400))),
% 0.21/0.46 inference(quant_inst,[status(thm)],[])).
% 0.21/0.46 tff(23,plain,
% 0.21/0.46 ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | (~less(v0, v400)) | leq(v0, v400)),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[22, 21])).
% 0.21/0.46 tff(24,plain,
% 0.21/0.46 (leq(v0, v400)),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[23, 13, 20])).
% 0.21/0.46 tff(25,plain,
% 0.21/0.46 ((~((~leq(v0, v400)) | (~leq(v400, v600)))) | (~leq(v0, v400)) | (~leq(v400, v600))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(26,plain,
% 0.21/0.46 (~((~leq(v0, v400)) | (~leq(v400, v600)))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[25, 24, 17])).
% 0.21/0.46 tff(27,plain,
% 0.21/0.46 (^[X: $i, V: $i] : refl((in_closed(X, V, V) <=> (X = V)) <=> (in_closed(X, V, V) <=> (X = V)))),
% 0.21/0.46 inference(bind,[status(th)],[])).
% 0.21/0.46 tff(28,plain,
% 0.21/0.46 (![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V)) <=> ![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))),
% 0.21/0.46 inference(quant_intro,[status(thm)],[27])).
% 0.21/0.46 tff(29,plain,
% 0.21/0.46 (![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V)) <=> ![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))),
% 0.21/0.46 inference(rewrite,[status(thm)],[])).
% 0.21/0.46 tff(30,axiom,(![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))), file('/export/starexec/sandbox/benchmark/Axioms/MGT002+6.ax','shape_point')).
% 0.21/0.46 tff(31,plain,
% 0.21/0.46 (![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[30, 29])).
% 0.21/0.46 tff(32,plain,(
% 0.21/0.46 ![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))),
% 0.21/0.46 inference(skolemize,[status(sab)],[31])).
% 0.21/0.46 tff(33,plain,
% 0.21/0.46 (![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[32, 28])).
% 0.21/0.46 tff(34,plain,
% 0.21/0.46 ((~![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))) | (in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400) <=> (tptp_fun_X_1(v800, v400, v400, v400) = v400))),
% 0.21/0.46 inference(quant_inst,[status(thm)],[])).
% 0.21/0.46 tff(35,plain,
% 0.21/0.46 (in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400) <=> (tptp_fun_X_1(v800, v400, v400, v400) = v400)),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[34, 33])).
% 0.21/0.46 tff(36,assumption,(~((~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800))), introduced(assumption)).
% 0.21/0.46 tff(37,plain,
% 0.21/0.46 (((~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(38,plain,
% 0.21/0.46 (in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[37, 36])).
% 0.21/0.46 tff(39,plain,
% 0.21/0.46 ((~(in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400) <=> (tptp_fun_X_1(v800, v400, v400, v400) = v400))) | (~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | (tptp_fun_X_1(v800, v400, v400, v400) = v400)),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(40,plain,
% 0.21/0.46 ((~(in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400) <=> (tptp_fun_X_1(v800, v400, v400, v400) = v400))) | (tptp_fun_X_1(v800, v400, v400, v400) = v400)),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[39, 38])).
% 0.21/0.46 tff(41,plain,
% 0.21/0.46 (tptp_fun_X_1(v800, v400, v400, v400) = v400),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[40, 35])).
% 0.21/0.46 tff(42,plain,
% 0.21/0.46 (leq(tptp_fun_X_1(v800, v400, v400, v400), v800) <=> leq(v400, v800)),
% 0.21/0.46 inference(monotonicity,[status(thm)],[41])).
% 0.21/0.46 tff(43,plain,
% 0.21/0.46 (leq(v400, v800) <=> leq(tptp_fun_X_1(v800, v400, v400, v400), v800)),
% 0.21/0.46 inference(symmetry,[status(thm)],[42])).
% 0.21/0.46 tff(44,plain,
% 0.21/0.46 (less(v400, v800) <=> less(v400, v800)),
% 0.21/0.46 inference(rewrite,[status(thm)],[])).
% 0.21/0.46 tff(45,axiom,(less(v400, v800)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','ord_v400_v800')).
% 0.21/0.46 tff(46,plain,
% 0.21/0.46 (less(v400, v800)),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[45, 44])).
% 0.21/0.46 tff(47,plain,
% 0.21/0.46 (((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | ((~less(v400, v800)) | leq(v400, v800))) <=> ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | (~less(v400, v800)) | leq(v400, v800))),
% 0.21/0.46 inference(rewrite,[status(thm)],[])).
% 0.21/0.46 tff(48,plain,
% 0.21/0.46 ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | ((~less(v400, v800)) | leq(v400, v800))),
% 0.21/0.46 inference(quant_inst,[status(thm)],[])).
% 0.21/0.46 tff(49,plain,
% 0.21/0.46 ((~![X: $i, Y: $i] : ((~less(X, Y)) | leq(X, Y))) | (~less(v400, v800)) | leq(v400, v800)),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[48, 47])).
% 0.21/0.46 tff(50,plain,
% 0.21/0.46 (leq(v400, v800)),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[49, 13, 46])).
% 0.21/0.46 tff(51,plain,
% 0.21/0.46 (leq(tptp_fun_X_1(v800, v400, v400, v400), v800)),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[50, 43])).
% 0.21/0.46 tff(52,plain,
% 0.21/0.46 (^[X: $i, A: $i, B: $i] : refl((~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B))) <=> (~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B))))),
% 0.21/0.46 inference(bind,[status(th)],[])).
% 0.21/0.46 tff(53,plain,
% 0.21/0.46 (![X: $i, A: $i, B: $i] : (~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B))) <=> ![X: $i, A: $i, B: $i] : (~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B)))),
% 0.21/0.46 inference(quant_intro,[status(thm)],[52])).
% 0.21/0.46 tff(54,plain,
% 0.21/0.46 (^[X: $i, A: $i, B: $i] : trans(trans(monotonicity(rewrite((leq(A, X) & leq(X, B)) <=> (~((~leq(A, X)) | (~leq(X, B))))), ((in_closed(X, A, B) <=> (leq(A, X) & leq(X, B))) <=> (in_closed(X, A, B) <=> (~((~leq(A, X)) | (~leq(X, B))))))), rewrite((in_closed(X, A, B) <=> (~((~leq(A, X)) | (~leq(X, B))))) <=> (~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B)))), ((in_closed(X, A, B) <=> (leq(A, X) & leq(X, B))) <=> (~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B))))), rewrite((~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B))) <=> (~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B)))), ((in_closed(X, A, B) <=> (leq(A, X) & leq(X, B))) <=> (~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B)))))),
% 0.21/0.46 inference(bind,[status(th)],[])).
% 0.21/0.46 tff(55,plain,
% 0.21/0.46 (![X: $i, A: $i, B: $i] : (in_closed(X, A, B) <=> (leq(A, X) & leq(X, B))) <=> ![X: $i, A: $i, B: $i] : (~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B)))),
% 0.21/0.46 inference(quant_intro,[status(thm)],[54])).
% 0.21/0.46 tff(56,plain,
% 0.21/0.46 (![X: $i, A: $i, B: $i] : (in_closed(X, A, B) <=> (leq(A, X) & leq(X, B))) <=> ![X: $i, A: $i, B: $i] : (in_closed(X, A, B) <=> (leq(A, X) & leq(X, B)))),
% 0.21/0.46 inference(rewrite,[status(thm)],[])).
% 0.21/0.46 tff(57,axiom,(![X: $i, A: $i, B: $i] : (in_closed(X, A, B) <=> (leq(A, X) & leq(X, B)))), file('/export/starexec/sandbox/benchmark/Axioms/MGT002+2.ax','in_closed')).
% 0.21/0.46 tff(58,plain,
% 0.21/0.46 (![X: $i, A: $i, B: $i] : (in_closed(X, A, B) <=> (leq(A, X) & leq(X, B)))),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[57, 56])).
% 0.21/0.46 tff(59,plain,(
% 0.21/0.46 ![X: $i, A: $i, B: $i] : (in_closed(X, A, B) <=> (leq(A, X) & leq(X, B)))),
% 0.21/0.46 inference(skolemize,[status(sab)],[58])).
% 0.21/0.46 tff(60,plain,
% 0.21/0.46 (![X: $i, A: $i, B: $i] : (~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B)))),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[59, 55])).
% 0.21/0.46 tff(61,plain,
% 0.21/0.46 (![X: $i, A: $i, B: $i] : (~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B)))),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[60, 53])).
% 0.21/0.46 tff(62,plain,
% 0.21/0.46 ((~![X: $i, A: $i, B: $i] : (~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B)))) | (~(((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v800))) <=> in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)))),
% 0.21/0.46 inference(quant_inst,[status(thm)],[])).
% 0.21/0.46 tff(63,plain,
% 0.21/0.46 (~(((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v800))) <=> in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[62, 61])).
% 0.21/0.46 tff(64,plain,
% 0.21/0.46 (((~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)) | (~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(65,plain,
% 0.21/0.46 (~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[64, 36])).
% 0.21/0.46 tff(66,plain,
% 0.21/0.46 ((((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v800))) <=> in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)) | ((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v800))) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(67,plain,
% 0.21/0.46 ((((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v800))) <=> in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)) | ((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v800)))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[66, 65])).
% 0.21/0.46 tff(68,plain,
% 0.21/0.46 ((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v800))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[67, 63])).
% 0.21/0.46 tff(69,plain,
% 0.21/0.46 ((~![X: $i, A: $i, B: $i] : (~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B)))) | (~(((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v400))) <=> in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)))),
% 0.21/0.46 inference(quant_inst,[status(thm)],[])).
% 0.21/0.46 tff(70,plain,
% 0.21/0.46 (~(((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v400))) <=> in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[69, 61])).
% 0.21/0.46 tff(71,plain,
% 0.21/0.46 ((((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v400))) <=> in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | (~((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v400)))) | (~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(72,plain,
% 0.21/0.46 ((((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v400))) <=> in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | (~((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v400))))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[71, 38])).
% 0.21/0.46 tff(73,plain,
% 0.21/0.46 (~((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v400)))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[72, 70])).
% 0.21/0.46 tff(74,plain,
% 0.21/0.46 (((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v400))) | leq(v400, tptp_fun_X_1(v800, v400, v400, v400))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(75,plain,
% 0.21/0.46 (leq(v400, tptp_fun_X_1(v800, v400, v400, v400))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[74, 73])).
% 0.21/0.46 tff(76,plain,
% 0.21/0.46 ((~((~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v800)))) | (~leq(v400, tptp_fun_X_1(v800, v400, v400, v400))) | (~leq(tptp_fun_X_1(v800, v400, v400, v400), v800))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(77,plain,
% 0.21/0.46 (~leq(tptp_fun_X_1(v800, v400, v400, v400), v800)),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[76, 75, 68])).
% 0.21/0.46 tff(78,plain,
% 0.21/0.46 ($false),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[77, 51])).
% 0.21/0.46 tff(79,plain,((~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)), inference(lemma,lemma(discharge,[]))).
% 0.21/0.46 tff(80,plain,
% 0.21/0.46 (^[I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : refl((~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))))) <=> (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))))))),
% 0.21/0.46 inference(bind,[status(th)],[])).
% 0.21/0.46 tff(81,plain,
% 0.21/0.46 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))))),
% 0.21/0.47 inference(quant_intro,[status(thm)],[80])).
% 0.21/0.47 tff(82,plain,
% 0.21/0.47 (^[I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : rewrite((~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))))) <=> (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))))))),
% 0.21/0.47 inference(bind,[status(th)],[])).
% 0.21/0.47 tff(83,plain,
% 0.21/0.47 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))))),
% 0.21/0.47 inference(quant_intro,[status(thm)],[82])).
% 0.21/0.47 tff(84,plain,
% 0.21/0.47 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))))),
% 0.21/0.47 inference(transitivity,[status(thm)],[83, 81])).
% 0.21/0.47 tff(85,plain,
% 0.21/0.47 (^[I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : trans(monotonicity(rewrite(((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi))) <=> ((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))), rewrite((axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))) <=> (axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))), ((((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi))) & (axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))) <=> (((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi))) & (axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))))), rewrite((((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi))) & (axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))) <=> (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))))), ((((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi))) & (axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))) <=> (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))))))),
% 0.21/0.47 inference(bind,[status(th)],[])).
% 0.21/0.47 tff(86,plain,
% 0.21/0.47 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi))) & (axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))))),
% 0.21/0.47 inference(quant_intro,[status(thm)],[85])).
% 0.21/0.47 tff(87,plain,
% 0.21/0.47 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (axis_subsumes(I1lo, I1hi, I2lo, I2hi) <=> ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (axis_subsumes(I1lo, I1hi, I2lo, I2hi) <=> ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(88,plain,
% 0.21/0.47 (^[I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : rewrite((axis_subsumes(I1lo, I1hi, I2lo, I2hi) <=> ![X: $i] : (in_closed(X, I1lo, I1hi) => in_closed(X, I2lo, I2hi))) <=> (axis_subsumes(I1lo, I1hi, I2lo, I2hi) <=> ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi))))),
% 0.21/0.47 inference(bind,[status(th)],[])).
% 0.21/0.47 tff(89,plain,
% 0.21/0.47 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (axis_subsumes(I1lo, I1hi, I2lo, I2hi) <=> ![X: $i] : (in_closed(X, I1lo, I1hi) => in_closed(X, I2lo, I2hi))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (axis_subsumes(I1lo, I1hi, I2lo, I2hi) <=> ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))),
% 0.21/0.47 inference(quant_intro,[status(thm)],[88])).
% 0.21/0.47 tff(90,axiom,(![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (axis_subsumes(I1lo, I1hi, I2lo, I2hi) <=> ![X: $i] : (in_closed(X, I1lo, I1hi) => in_closed(X, I2lo, I2hi)))), file('/export/starexec/sandbox/benchmark/Axioms/MGT002+2.ax','axis_subsumes_def')).
% 0.21/0.47 tff(91,plain,
% 0.21/0.47 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (axis_subsumes(I1lo, I1hi, I2lo, I2hi) <=> ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))),
% 0.21/0.47 inference(modus_ponens,[status(thm)],[90, 89])).
% 0.21/0.47 tff(92,plain,
% 0.21/0.47 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (axis_subsumes(I1lo, I1hi, I2lo, I2hi) <=> ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))),
% 0.21/0.47 inference(modus_ponens,[status(thm)],[91, 87])).
% 0.21/0.47 tff(93,plain,(
% 0.21/0.47 ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi))) & (axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))),
% 0.21/0.47 inference(skolemize,[status(sab)],[92])).
% 0.21/0.47 tff(94,plain,
% 0.21/0.47 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))))),
% 0.21/0.47 inference(modus_ponens,[status(thm)],[93, 86])).
% 0.21/0.47 tff(95,plain,
% 0.21/0.47 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))))),
% 0.21/0.47 inference(modus_ponens,[status(thm)],[94, 84])).
% 0.21/0.47 tff(96,plain,
% 0.21/0.47 ((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_subsumes(I1lo, I1hi, I2lo, I2hi)) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | in_closed(X, I2lo, I2hi)))) | (~(axis_subsumes(I1lo, I1hi, I2lo, I2hi) | (~((~in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | in_closed(tptp_fun_X_1(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))))) | (~((~((~axis_subsumes(v400, v400, v400, v800)) | ![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800)))) | (~(axis_subsumes(v400, v400, v400, v800) | (~((~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)))))))),
% 0.21/0.47 inference(quant_inst,[status(thm)],[])).
% 0.21/0.47 tff(97,plain,
% 0.21/0.47 (~((~((~axis_subsumes(v400, v400, v400, v800)) | ![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800)))) | (~(axis_subsumes(v400, v400, v400, v800) | (~((~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800))))))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[96, 95])).
% 0.21/0.47 tff(98,plain,
% 0.21/0.47 (((~((~axis_subsumes(v400, v400, v400, v800)) | ![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800)))) | (~(axis_subsumes(v400, v400, v400, v800) | (~((~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)))))) | (axis_subsumes(v400, v400, v400, v800) | (~((~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800))))),
% 0.21/0.47 inference(tautology,[status(thm)],[])).
% 0.21/0.47 tff(99,plain,
% 0.21/0.47 (axis_subsumes(v400, v400, v400, v800) | (~((~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[98, 97])).
% 0.21/0.47 tff(100,plain,
% 0.21/0.47 ((~(axis_subsumes(v400, v400, v400, v800) | (~((~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800))))) | axis_subsumes(v400, v400, v400, v800) | (~((~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)))),
% 0.21/0.47 inference(tautology,[status(thm)],[])).
% 0.21/0.47 tff(101,plain,
% 0.21/0.47 (axis_subsumes(v400, v400, v400, v800) | (~((~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[100, 99])).
% 0.21/0.47 tff(102,plain,
% 0.21/0.47 (axis_subsumes(v400, v400, v400, v800)),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[101, 79])).
% 0.21/0.47 tff(103,plain,
% 0.21/0.47 (((~((~axis_subsumes(v400, v400, v400, v800)) | ![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800)))) | (~(axis_subsumes(v400, v400, v400, v800) | (~((~in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v400)) | in_closed(tptp_fun_X_1(v800, v400, v400, v400), v400, v800)))))) | ((~axis_subsumes(v400, v400, v400, v800)) | ![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800)))),
% 0.21/0.47 inference(tautology,[status(thm)],[])).
% 0.21/0.47 tff(104,plain,
% 0.21/0.47 ((~axis_subsumes(v400, v400, v400, v800)) | ![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[103, 97])).
% 0.21/0.47 tff(105,plain,
% 0.21/0.47 ((~((~axis_subsumes(v400, v400, v400, v800)) | ![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800)))) | (~axis_subsumes(v400, v400, v400, v800)) | ![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800))),
% 0.21/0.47 inference(tautology,[status(thm)],[])).
% 0.21/0.47 tff(106,plain,
% 0.21/0.47 ((~axis_subsumes(v400, v400, v400, v800)) | ![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[105, 104])).
% 0.21/0.47 tff(107,plain,
% 0.21/0.47 (![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[106, 102])).
% 0.21/0.47 tff(108,plain,
% 0.21/0.47 (((~![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))) | in_closed(v400, v400, v400)) <=> ((~![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))) | in_closed(v400, v400, v400))),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(109,plain,
% 0.21/0.47 ((in_closed(v400, v400, v400) <=> $true) <=> in_closed(v400, v400, v400)),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(110,plain,
% 0.21/0.47 ((v400 = v400) <=> $true),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(111,plain,
% 0.21/0.47 ((in_closed(v400, v400, v400) <=> (v400 = v400)) <=> (in_closed(v400, v400, v400) <=> $true)),
% 0.21/0.47 inference(monotonicity,[status(thm)],[110])).
% 0.21/0.47 tff(112,plain,
% 0.21/0.47 ((in_closed(v400, v400, v400) <=> (v400 = v400)) <=> in_closed(v400, v400, v400)),
% 0.21/0.47 inference(transitivity,[status(thm)],[111, 109])).
% 0.21/0.47 tff(113,plain,
% 0.21/0.47 (((~![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))) | (in_closed(v400, v400, v400) <=> (v400 = v400))) <=> ((~![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))) | in_closed(v400, v400, v400))),
% 0.21/0.47 inference(monotonicity,[status(thm)],[112])).
% 0.21/0.47 tff(114,plain,
% 0.21/0.47 (((~![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))) | (in_closed(v400, v400, v400) <=> (v400 = v400))) <=> ((~![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))) | in_closed(v400, v400, v400))),
% 0.21/0.47 inference(transitivity,[status(thm)],[113, 108])).
% 0.21/0.47 tff(115,plain,
% 0.21/0.47 ((~![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))) | (in_closed(v400, v400, v400) <=> (v400 = v400))),
% 0.21/0.47 inference(quant_inst,[status(thm)],[])).
% 0.21/0.47 tff(116,plain,
% 0.21/0.47 ((~![X: $i, V: $i] : (in_closed(X, V, V) <=> (X = V))) | in_closed(v400, v400, v400)),
% 0.21/0.47 inference(modus_ponens,[status(thm)],[115, 114])).
% 0.21/0.47 tff(117,plain,
% 0.21/0.47 (in_closed(v400, v400, v400)),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[116, 33])).
% 0.21/0.47 tff(118,plain,
% 0.21/0.47 (((~![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800))) | ((~in_closed(v400, v400, v400)) | in_closed(v400, v400, v800))) <=> ((~![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800))) | (~in_closed(v400, v400, v400)) | in_closed(v400, v400, v800))),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(119,plain,
% 0.21/0.47 ((~![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800))) | ((~in_closed(v400, v400, v400)) | in_closed(v400, v400, v800))),
% 0.21/0.47 inference(quant_inst,[status(thm)],[])).
% 0.21/0.47 tff(120,plain,
% 0.21/0.47 ((~![X: $i] : ((~in_closed(X, v400, v400)) | in_closed(X, v400, v800))) | (~in_closed(v400, v400, v400)) | in_closed(v400, v400, v800)),
% 0.21/0.47 inference(modus_ponens,[status(thm)],[119, 118])).
% 0.21/0.47 tff(121,plain,
% 0.21/0.47 (in_closed(v400, v400, v800)),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[120, 117, 107])).
% 0.21/0.47 tff(122,plain,
% 0.21/0.47 (^[I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : refl((~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))) <=> (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))))),
% 0.21/0.47 inference(bind,[status(th)],[])).
% 0.21/0.47 tff(123,plain,
% 0.21/0.47 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))),
% 0.21/0.47 inference(quant_intro,[status(thm)],[122])).
% 0.21/0.47 tff(124,plain,
% 0.21/0.47 (^[I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : rewrite((~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))) <=> (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))))),
% 0.21/0.47 inference(bind,[status(th)],[])).
% 0.21/0.47 tff(125,plain,
% 0.21/0.47 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))),
% 0.21/0.47 inference(quant_intro,[status(thm)],[124])).
% 0.21/0.47 tff(126,plain,
% 0.21/0.47 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))),
% 0.21/0.47 inference(transitivity,[status(thm)],[125, 123])).
% 0.21/0.47 tff(127,plain,
% 0.21/0.47 (^[I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : trans(monotonicity(rewrite(((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi) & in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))) <=> ((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))), rewrite((axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : (~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)))) <=> (axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))), ((((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi) & in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))) & (axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : (~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))))) <=> (((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))) & (axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))))), rewrite((((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))))) & (axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi))))) <=> (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))), ((((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi) & in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))) & (axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : (~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))))) <=> (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))))),
% 0.21/0.48 inference(bind,[status(th)],[])).
% 0.21/0.48 tff(128,plain,
% 0.21/0.48 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi) & in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))) & (axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : (~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))),
% 0.21/0.48 inference(quant_intro,[status(thm)],[127])).
% 0.21/0.48 tff(129,plain,
% 0.21/0.48 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (axis_compatible(I1lo, I1hi, I2lo, I2hi) <=> ?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi))) <=> ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (axis_compatible(I1lo, I1hi, I2lo, I2hi) <=> ?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)))),
% 0.21/0.48 inference(rewrite,[status(thm)],[])).
% 0.21/0.48 tff(130,axiom,(![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (axis_compatible(I1lo, I1hi, I2lo, I2hi) <=> ?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)))), file('/export/starexec/sandbox/benchmark/Axioms/MGT002+2.ax','axis_compatible_def')).
% 0.21/0.48 tff(131,plain,
% 0.21/0.48 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (axis_compatible(I1lo, I1hi, I2lo, I2hi) <=> ?[X: $i] : (in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)))),
% 0.21/0.48 inference(modus_ponens,[status(thm)],[130, 129])).
% 0.21/0.48 tff(132,plain,(
% 0.21/0.48 ![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi) & in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi))) & (axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : (~(in_closed(X, I1lo, I1hi) & in_closed(X, I2lo, I2hi)))))),
% 0.21/0.48 inference(skolemize,[status(sab)],[131])).
% 0.21/0.48 tff(133,plain,
% 0.21/0.48 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))),
% 0.21/0.48 inference(modus_ponens,[status(thm)],[132, 128])).
% 0.21/0.48 tff(134,plain,
% 0.21/0.48 (![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))),
% 0.21/0.48 inference(modus_ponens,[status(thm)],[133, 126])).
% 0.21/0.48 tff(135,plain,
% 0.21/0.48 (((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800))))) | (~((~axis_compatible(v0, v600, v400, v800)) | (~((~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v0, v600)) | (~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v400, v800))))))))) <=> ((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800))))) | (~((~axis_compatible(v0, v600, v400, v800)) | (~((~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v0, v600)) | (~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v400, v800)))))))))),
% 0.21/0.48 inference(rewrite,[status(thm)],[])).
% 0.21/0.48 tff(136,plain,
% 0.21/0.48 ((~((~((~axis_compatible(v0, v600, v400, v800)) | (~((~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v0, v600)) | (~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v400, v800)))))) | (~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800))))))) <=> (~((~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800))))) | (~((~axis_compatible(v0, v600, v400, v800)) | (~((~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v0, v600)) | (~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v400, v800))))))))),
% 0.21/0.48 inference(rewrite,[status(thm)],[])).
% 0.21/0.48 tff(137,plain,
% 0.21/0.48 (((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~((~axis_compatible(v0, v600, v400, v800)) | (~((~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v0, v600)) | (~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v400, v800)))))) | (~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800)))))))) <=> ((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800))))) | (~((~axis_compatible(v0, v600, v400, v800)) | (~((~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v0, v600)) | (~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v400, v800)))))))))),
% 0.21/0.48 inference(monotonicity,[status(thm)],[136])).
% 0.21/0.48 tff(138,plain,
% 0.21/0.48 (((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~((~axis_compatible(v0, v600, v400, v800)) | (~((~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v0, v600)) | (~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v400, v800)))))) | (~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800)))))))) <=> ((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800))))) | (~((~axis_compatible(v0, v600, v400, v800)) | (~((~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v0, v600)) | (~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v400, v800)))))))))),
% 0.21/0.48 inference(transitivity,[status(thm)],[137, 135])).
% 0.21/0.48 tff(139,plain,
% 0.21/0.48 ((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~((~axis_compatible(v0, v600, v400, v800)) | (~((~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v0, v600)) | (~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v400, v800)))))) | (~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800)))))))),
% 0.21/0.48 inference(quant_inst,[status(thm)],[])).
% 0.21/0.48 tff(140,plain,
% 0.21/0.48 ((~![I1lo: $i, I1hi: $i, I2lo: $i, I2hi: $i] : (~((~((~axis_compatible(I1lo, I1hi, I2lo, I2hi)) | (~((~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I1lo, I1hi)) | (~in_closed(tptp_fun_X_0(I2hi, I2lo, I1hi, I1lo), I2lo, I2hi)))))) | (~(axis_compatible(I1lo, I1hi, I2lo, I2hi) | ![X: $i] : ((~in_closed(X, I1lo, I1hi)) | (~in_closed(X, I2lo, I2hi)))))))) | (~((~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800))))) | (~((~axis_compatible(v0, v600, v400, v800)) | (~((~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v0, v600)) | (~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v400, v800))))))))),
% 0.21/0.48 inference(modus_ponens,[status(thm)],[139, 138])).
% 0.21/0.48 tff(141,plain,
% 0.21/0.48 (~((~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800))))) | (~((~axis_compatible(v0, v600, v400, v800)) | (~((~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v0, v600)) | (~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v400, v800)))))))),
% 0.21/0.48 inference(unit_resolution,[status(thm)],[140, 134])).
% 0.21/0.48 tff(142,plain,
% 0.21/0.48 (((~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800))))) | (~((~axis_compatible(v0, v600, v400, v800)) | (~((~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v0, v600)) | (~in_closed(tptp_fun_X_0(v800, v400, v600, v0), v400, v800))))))) | (axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800))))),
% 0.21/0.48 inference(tautology,[status(thm)],[])).
% 0.21/0.48 tff(143,plain,
% 0.21/0.48 (axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800)))),
% 0.21/0.48 inference(unit_resolution,[status(thm)],[142, 141])).
% 0.21/0.48 tff(144,plain,
% 0.21/0.48 (^[A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : refl((~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2))) <=> (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2))))),
% 0.21/0.48 inference(bind,[status(th)],[])).
% 0.21/0.48 tff(145,plain,
% 0.21/0.48 (![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2))) <=> ![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))),
% 0.21/0.48 inference(quant_intro,[status(thm)],[144])).
% 0.21/0.48 tff(146,plain,
% 0.21/0.48 (^[A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : trans(trans(monotonicity(rewrite((axis_compatible(A1, B1, C1, D1) & axis_compatible(A2, B2, C2, D2)) <=> (~((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))))), ((box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2) <=> (axis_compatible(A1, B1, C1, D1) & axis_compatible(A2, B2, C2, D2))) <=> (box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2) <=> (~((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))))))), rewrite((box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2) <=> (~((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))))) <=> (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))), ((box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2) <=> (axis_compatible(A1, B1, C1, D1) & axis_compatible(A2, B2, C2, D2))) <=> (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2))))), rewrite((~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2))) <=> (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))), ((box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2) <=> (axis_compatible(A1, B1, C1, D1) & axis_compatible(A2, B2, C2, D2))) <=> (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))))),
% 0.21/0.48 inference(bind,[status(th)],[])).
% 0.21/0.48 tff(147,plain,
% 0.21/0.48 (![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2) <=> (axis_compatible(A1, B1, C1, D1) & axis_compatible(A2, B2, C2, D2))) <=> ![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))),
% 0.21/0.48 inference(quant_intro,[status(thm)],[146])).
% 0.21/0.48 tff(148,plain,
% 0.21/0.48 (![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2) <=> (axis_compatible(A1, B1, C1, D1) & axis_compatible(A2, B2, C2, D2))) <=> ![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2) <=> (axis_compatible(A1, B1, C1, D1) & axis_compatible(A2, B2, C2, D2)))),
% 0.21/0.48 inference(rewrite,[status(thm)],[])).
% 0.21/0.48 tff(149,axiom,(![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2) <=> (axis_compatible(A1, B1, C1, D1) & axis_compatible(A2, B2, C2, D2)))), file('/export/starexec/sandbox/benchmark/Axioms/MGT002+6.ax','box2_overlap')).
% 0.21/0.48 tff(150,plain,
% 0.21/0.48 (![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2) <=> (axis_compatible(A1, B1, C1, D1) & axis_compatible(A2, B2, C2, D2)))),
% 0.21/0.48 inference(modus_ponens,[status(thm)],[149, 148])).
% 0.21/0.48 tff(151,plain,(
% 0.21/0.48 ![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2) <=> (axis_compatible(A1, B1, C1, D1) & axis_compatible(A2, B2, C2, D2)))),
% 0.21/0.48 inference(skolemize,[status(sab)],[150])).
% 0.21/0.48 tff(152,plain,
% 0.21/0.48 (![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))),
% 0.21/0.48 inference(modus_ponens,[status(thm)],[151, 147])).
% 0.21/0.48 tff(153,plain,
% 0.21/0.48 (![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))),
% 0.21/0.48 inference(modus_ponens,[status(thm)],[152, 145])).
% 0.21/0.48 tff(154,plain,
% 0.21/0.48 (((~![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))) | (axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800))) <=> ((~![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))) | (axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)))),
% 0.21/0.49 inference(rewrite,[status(thm)],[])).
% 0.21/0.49 tff(155,plain,
% 0.21/0.49 ((~(~(axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)))) <=> (axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800))),
% 0.21/0.49 inference(rewrite,[status(thm)],[])).
% 0.21/0.49 tff(156,plain,
% 0.21/0.49 ((~(axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800))) <=> (~(axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)))),
% 0.21/0.49 inference(rewrite,[status(thm)],[])).
% 0.21/0.49 tff(157,plain,
% 0.21/0.49 (((~axis_compatible(v0, v600, v400, v800)) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)) <=> (~(axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)))),
% 0.21/0.49 inference(rewrite,[status(thm)],[])).
% 0.21/0.49 tff(158,plain,
% 0.21/0.49 (((~axis_compatible(v0, v600, v400, v800)) | (~axis_compatible(v0, v600, v400, v800))) <=> (~axis_compatible(v0, v600, v400, v800))),
% 0.21/0.49 inference(rewrite,[status(thm)],[])).
% 0.21/0.49 tff(159,plain,
% 0.21/0.49 ((((~axis_compatible(v0, v600, v400, v800)) | (~axis_compatible(v0, v600, v400, v800))) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)) <=> ((~axis_compatible(v0, v600, v400, v800)) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800))),
% 0.21/0.49 inference(monotonicity,[status(thm)],[158])).
% 0.21/0.49 tff(160,plain,
% 0.21/0.49 ((((~axis_compatible(v0, v600, v400, v800)) | (~axis_compatible(v0, v600, v400, v800))) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)) <=> (~(axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)))),
% 0.21/0.49 inference(transitivity,[status(thm)],[159, 157])).
% 0.21/0.49 tff(161,plain,
% 0.21/0.49 ((((~axis_compatible(v0, v600, v400, v800)) | (~axis_compatible(v0, v600, v400, v800))) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)) <=> (~(axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)))),
% 0.21/0.49 inference(transitivity,[status(thm)],[160, 156])).
% 0.21/0.49 tff(162,plain,
% 0.21/0.49 ((~(((~axis_compatible(v0, v600, v400, v800)) | (~axis_compatible(v0, v600, v400, v800))) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800))) <=> (~(~(axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800))))),
% 0.21/0.49 inference(monotonicity,[status(thm)],[161])).
% 0.21/0.49 tff(163,plain,
% 0.21/0.49 ((~(((~axis_compatible(v0, v600, v400, v800)) | (~axis_compatible(v0, v600, v400, v800))) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800))) <=> (axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800))),
% 0.21/0.49 inference(transitivity,[status(thm)],[162, 155])).
% 0.21/0.49 tff(164,plain,
% 0.21/0.49 (((~![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))) | (~(((~axis_compatible(v0, v600, v400, v800)) | (~axis_compatible(v0, v600, v400, v800))) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)))) <=> ((~![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))) | (axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)))),
% 0.21/0.49 inference(monotonicity,[status(thm)],[163])).
% 0.21/0.49 tff(165,plain,
% 0.21/0.49 (((~![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))) | (~(((~axis_compatible(v0, v600, v400, v800)) | (~axis_compatible(v0, v600, v400, v800))) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)))) <=> ((~![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))) | (axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)))),
% 0.21/0.49 inference(transitivity,[status(thm)],[164, 154])).
% 0.21/0.49 tff(166,plain,
% 0.21/0.49 ((~![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))) | (~(((~axis_compatible(v0, v600, v400, v800)) | (~axis_compatible(v0, v600, v400, v800))) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)))),
% 0.21/0.49 inference(quant_inst,[status(thm)],[])).
% 0.21/0.49 tff(167,plain,
% 0.21/0.49 ((~![A1: $i, B1: $i, A2: $i, B2: $i, C1: $i, D1: $i, C2: $i, D2: $i] : (~(((~axis_compatible(A1, B1, C1, D1)) | (~axis_compatible(A2, B2, C2, D2))) <=> box2_compatible(A1, B1, A2, B2, C1, D1, C2, D2)))) | (axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800))),
% 0.21/0.49 inference(modus_ponens,[status(thm)],[166, 165])).
% 0.21/0.49 tff(168,plain,
% 0.21/0.49 (axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)),
% 0.21/0.49 inference(unit_resolution,[status(thm)],[167, 153])).
% 0.21/0.49 tff(169,plain,
% 0.21/0.49 ((~box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)) <=> (~box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800))),
% 0.21/0.49 inference(rewrite,[status(thm)],[])).
% 0.21/0.49 tff(170,axiom,(~box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','odrl624')).
% 0.21/0.49 tff(171,plain,
% 0.21/0.49 (~box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)),
% 0.21/0.49 inference(modus_ponens,[status(thm)],[170, 169])).
% 0.21/0.49 tff(172,plain,
% 0.21/0.49 ((~(axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800))) | (~axis_compatible(v0, v600, v400, v800)) | box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800)),
% 0.21/0.49 inference(tautology,[status(thm)],[])).
% 0.21/0.49 tff(173,plain,
% 0.21/0.49 ((~(axis_compatible(v0, v600, v400, v800) <=> box2_compatible(v0, v600, v0, v600, v400, v800, v400, v800))) | (~axis_compatible(v0, v600, v400, v800))),
% 0.21/0.49 inference(unit_resolution,[status(thm)],[172, 171])).
% 0.21/0.49 tff(174,plain,
% 0.21/0.49 (~axis_compatible(v0, v600, v400, v800)),
% 0.21/0.49 inference(unit_resolution,[status(thm)],[173, 168])).
% 0.21/0.49 tff(175,plain,
% 0.21/0.49 ((~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800))))) | axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800)))),
% 0.21/0.49 inference(tautology,[status(thm)],[])).
% 0.21/0.49 tff(176,plain,
% 0.21/0.49 ((~(axis_compatible(v0, v600, v400, v800) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800))))) | ![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800)))),
% 0.21/0.49 inference(unit_resolution,[status(thm)],[175, 174])).
% 0.21/0.49 tff(177,plain,
% 0.21/0.49 (![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800)))),
% 0.21/0.49 inference(unit_resolution,[status(thm)],[176, 143])).
% 0.21/0.49 tff(178,plain,
% 0.21/0.49 (((~![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800)))) | ((~in_closed(v400, v0, v600)) | (~in_closed(v400, v400, v800)))) <=> ((~![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800)))) | (~in_closed(v400, v0, v600)) | (~in_closed(v400, v400, v800)))),
% 0.21/0.49 inference(rewrite,[status(thm)],[])).
% 0.21/0.49 tff(179,plain,
% 0.21/0.49 ((~![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800)))) | ((~in_closed(v400, v0, v600)) | (~in_closed(v400, v400, v800)))),
% 0.21/0.49 inference(quant_inst,[status(thm)],[])).
% 0.21/0.50 tff(180,plain,
% 0.21/0.50 ((~![X: $i] : ((~in_closed(X, v0, v600)) | (~in_closed(X, v400, v800)))) | (~in_closed(v400, v0, v600)) | (~in_closed(v400, v400, v800))),
% 0.21/0.50 inference(modus_ponens,[status(thm)],[179, 178])).
% 0.21/0.50 tff(181,plain,
% 0.21/0.50 (~in_closed(v400, v0, v600)),
% 0.21/0.50 inference(unit_resolution,[status(thm)],[180, 177, 121])).
% 0.21/0.50 tff(182,plain,
% 0.21/0.50 ((((~leq(v0, v400)) | (~leq(v400, v600))) <=> in_closed(v400, v0, v600)) | ((~leq(v0, v400)) | (~leq(v400, v600))) | in_closed(v400, v0, v600)),
% 0.21/0.50 inference(tautology,[status(thm)],[])).
% 0.21/0.50 tff(183,plain,
% 0.21/0.50 (((~leq(v0, v400)) | (~leq(v400, v600))) <=> in_closed(v400, v0, v600)),
% 0.21/0.50 inference(unit_resolution,[status(thm)],[182, 181, 26])).
% 0.21/0.50 tff(184,plain,
% 0.21/0.50 ((~![X: $i, A: $i, B: $i] : (~(((~leq(A, X)) | (~leq(X, B))) <=> in_closed(X, A, B)))) | (~(((~leq(v0, v400)) | (~leq(v400, v600))) <=> in_closed(v400, v0, v600)))),
% 0.21/0.50 inference(quant_inst,[status(thm)],[])).
% 0.21/0.50 tff(185,plain,
% 0.21/0.50 ($false),
% 0.21/0.50 inference(unit_resolution,[status(thm)],[184, 61, 183])).
% 0.21/0.50 % SZS output end Proof
% 0.21/0.50 % E exiting
%------------------------------------------------------------------------------