%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SET020-6 : TPTP v9.0.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:24:51 AM UTC 2025
% Result : Unsatisfiable 1.31s 1.50s
% Output : Proof 1.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SET020-6 : TPTP v9.0.0. Bugfixed v2.1.0.
% 0.06/0.12 % Command : run_E %s %d THM
% 0.14/0.34 % Computer : n015.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Fri Jun 20 04:01:56 EDT 2025
% 0.14/0.34 % CPUTime :
% 1.31/1.50 % SZS status Unsatisfiable
% 1.31/1.50 % SZS output start Proof
% 1.31/1.50 tff(member_type, type, (
% 1.31/1.50 member: ( $i * $i ) > $o)).
% 1.31/1.50 tff(singleton_type, type, (
% 1.31/1.50 singleton: $i > $i)).
% 1.31/1.50 tff(first_type, type, (
% 1.31/1.50 first: $i > $i)).
% 1.31/1.50 tff(ordered_pair_type, type, (
% 1.31/1.50 ordered_pair: ( $i * $i ) > $i)).
% 1.31/1.50 tff(v_type, type, (
% 1.31/1.50 v: $i)).
% 1.31/1.50 tff(u_type, type, (
% 1.31/1.50 u: $i)).
% 1.31/1.50 tff(unordered_pair_type, type, (
% 1.31/1.50 unordered_pair: ( $i * $i ) > $i)).
% 1.31/1.50 tff(universal_class_type, type, (
% 1.31/1.50 universal_class: $i)).
% 1.31/1.50 tff(cross_product_type, type, (
% 1.31/1.50 cross_product: ( $i * $i ) > $i)).
% 1.31/1.50 tff(second_type, type, (
% 1.31/1.50 second: $i > $i)).
% 1.31/1.50 tff(complement_type, type, (
% 1.31/1.50 complement: $i > $i)).
% 1.31/1.50 tff(1,plain,
% 1.31/1.50 (^[X: $i] : refl((unordered_pair(X, X) = singleton(X)) <=> (unordered_pair(X, X) = singleton(X)))),
% 1.31/1.50 inference(bind,[status(th)],[])).
% 1.31/1.50 tff(2,plain,
% 1.31/1.50 (![X: $i] : (unordered_pair(X, X) = singleton(X)) <=> ![X: $i] : (unordered_pair(X, X) = singleton(X))),
% 1.31/1.50 inference(quant_intro,[status(thm)],[1])).
% 1.31/1.50 tff(3,plain,
% 1.31/1.50 (![X: $i] : (unordered_pair(X, X) = singleton(X)) <=> ![X: $i] : (unordered_pair(X, X) = singleton(X))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(4,axiom,(![X: $i] : (unordered_pair(X, X) = singleton(X))), file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax','singleton_set')).
% 1.31/1.50 tff(5,plain,
% 1.31/1.50 (![X: $i] : (unordered_pair(X, X) = singleton(X))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[4, 3])).
% 1.31/1.50 tff(6,plain,(
% 1.31/1.50 ![X: $i] : (unordered_pair(X, X) = singleton(X))),
% 1.31/1.50 inference(skolemize,[status(sab)],[5])).
% 1.31/1.50 tff(7,plain,
% 1.31/1.50 (![X: $i] : (unordered_pair(X, X) = singleton(X))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[6, 2])).
% 1.31/1.50 tff(8,plain,
% 1.31/1.50 ((~![X: $i] : (unordered_pair(X, X) = singleton(X))) | (unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))) = singleton(first(ordered_pair(u, v))))),
% 1.31/1.50 inference(quant_inst,[status(thm)],[])).
% 1.31/1.50 tff(9,plain,
% 1.31/1.50 (unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))) = singleton(first(ordered_pair(u, v)))),
% 1.31/1.50 inference(unit_resolution,[status(thm)],[8, 7])).
% 1.31/1.50 tff(10,plain,
% 1.31/1.50 (singleton(first(ordered_pair(u, v))) = unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v)))),
% 1.31/1.50 inference(symmetry,[status(thm)],[9])).
% 1.31/1.50 tff(11,plain,
% 1.31/1.50 (member(first(ordered_pair(u, v)), singleton(first(ordered_pair(u, v)))) <=> member(first(ordered_pair(u, v)), unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))))),
% 1.31/1.50 inference(monotonicity,[status(thm)],[10])).
% 1.31/1.50 tff(12,plain,
% 1.31/1.50 (member(first(ordered_pair(u, v)), unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v)))) <=> member(first(ordered_pair(u, v)), singleton(first(ordered_pair(u, v))))),
% 1.31/1.50 inference(symmetry,[status(thm)],[11])).
% 1.31/1.50 tff(13,plain,
% 1.31/1.50 (member(ordered_pair(u, v), cross_product(universal_class, universal_class)) <=> member(ordered_pair(u, v), cross_product(universal_class, universal_class))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(14,axiom,(member(ordered_pair(u, v), cross_product(universal_class, universal_class))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_unique_1st_and_2nd_in_pair_of_sets1_1')).
% 1.31/1.50 tff(15,plain,
% 1.31/1.50 (member(ordered_pair(u, v), cross_product(universal_class, universal_class))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[14, 13])).
% 1.31/1.50 tff(16,plain,
% 1.31/1.50 (^[Z: $i, Y: $i, X: $i] : refl(((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z)) <=> ((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z)))),
% 1.31/1.50 inference(bind,[status(th)],[])).
% 1.31/1.50 tff(17,plain,
% 1.31/1.50 (![Z: $i, Y: $i, X: $i] : ((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z)) <=> ![Z: $i, Y: $i, X: $i] : ((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z))),
% 1.31/1.50 inference(quant_intro,[status(thm)],[16])).
% 1.31/1.50 tff(18,plain,
% 1.31/1.50 (![Z: $i, Y: $i, X: $i] : ((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z)) <=> ![Z: $i, Y: $i, X: $i] : ((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(19,axiom,(![Z: $i, Y: $i, X: $i] : ((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z))), file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax','cartesian_product4')).
% 1.31/1.50 tff(20,plain,
% 1.31/1.50 (![Z: $i, Y: $i, X: $i] : ((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[19, 18])).
% 1.31/1.50 tff(21,plain,(
% 1.31/1.50 ![Z: $i, Y: $i, X: $i] : ((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z))),
% 1.31/1.50 inference(skolemize,[status(sab)],[20])).
% 1.31/1.50 tff(22,plain,
% 1.31/1.50 (![Z: $i, Y: $i, X: $i] : ((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[21, 17])).
% 1.31/1.50 tff(23,plain,
% 1.31/1.50 (((~![Z: $i, Y: $i, X: $i] : ((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z))) | ((~member(ordered_pair(u, v), cross_product(universal_class, universal_class))) | (ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))) = ordered_pair(u, v)))) <=> ((~![Z: $i, Y: $i, X: $i] : ((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z))) | (~member(ordered_pair(u, v), cross_product(universal_class, universal_class))) | (ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))) = ordered_pair(u, v)))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(24,plain,
% 1.31/1.50 ((~![Z: $i, Y: $i, X: $i] : ((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z))) | ((~member(ordered_pair(u, v), cross_product(universal_class, universal_class))) | (ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))) = ordered_pair(u, v)))),
% 1.31/1.50 inference(quant_inst,[status(thm)],[])).
% 1.31/1.50 tff(25,plain,
% 1.31/1.50 ((~![Z: $i, Y: $i, X: $i] : ((~member(Z, cross_product(X, Y))) | (ordered_pair(first(Z), second(Z)) = Z))) | (~member(ordered_pair(u, v), cross_product(universal_class, universal_class))) | (ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))) = ordered_pair(u, v))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[24, 23])).
% 1.31/1.50 tff(26,plain,
% 1.31/1.50 (ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))) = ordered_pair(u, v)),
% 1.31/1.50 inference(unit_resolution,[status(thm)],[25, 22, 15])).
% 1.31/1.50 tff(27,plain,
% 1.31/1.50 (member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(universal_class, universal_class)) <=> member(ordered_pair(u, v), cross_product(universal_class, universal_class))),
% 1.31/1.50 inference(monotonicity,[status(thm)],[26])).
% 1.31/1.50 tff(28,plain,
% 1.31/1.50 (member(ordered_pair(u, v), cross_product(universal_class, universal_class)) <=> member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(universal_class, universal_class))),
% 1.31/1.50 inference(symmetry,[status(thm)],[27])).
% 1.31/1.50 tff(29,plain,
% 1.31/1.50 (member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(universal_class, universal_class))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[15, 28])).
% 1.31/1.50 tff(30,plain,
% 1.31/1.50 (^[V: $i, Y: $i, U: $i, X: $i] : refl(((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X)) <=> ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X)))),
% 1.31/1.50 inference(bind,[status(th)],[])).
% 1.31/1.50 tff(31,plain,
% 1.31/1.50 (![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X)) <=> ![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))),
% 1.31/1.50 inference(quant_intro,[status(thm)],[30])).
% 1.31/1.50 tff(32,plain,
% 1.31/1.50 (![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X)) <=> ![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(33,axiom,(![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))), file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax','cartesian_product1')).
% 1.31/1.50 tff(34,plain,
% 1.31/1.50 (![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[33, 32])).
% 1.31/1.50 tff(35,plain,(
% 1.31/1.50 ![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))),
% 1.31/1.50 inference(skolemize,[status(sab)],[34])).
% 1.31/1.50 tff(36,plain,
% 1.31/1.50 (![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[35, 31])).
% 1.31/1.50 tff(37,plain,
% 1.31/1.50 (((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))) | ((~member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(universal_class, universal_class))) | member(first(ordered_pair(u, v)), universal_class))) <=> ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))) | (~member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(universal_class, universal_class))) | member(first(ordered_pair(u, v)), universal_class))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(38,plain,
% 1.31/1.50 ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))) | ((~member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(universal_class, universal_class))) | member(first(ordered_pair(u, v)), universal_class))),
% 1.31/1.50 inference(quant_inst,[status(thm)],[])).
% 1.31/1.50 tff(39,plain,
% 1.31/1.50 ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))) | (~member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(universal_class, universal_class))) | member(first(ordered_pair(u, v)), universal_class)),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[38, 37])).
% 1.31/1.50 tff(40,plain,
% 1.31/1.50 ((~member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(universal_class, universal_class))) | member(first(ordered_pair(u, v)), universal_class)),
% 1.31/1.50 inference(unit_resolution,[status(thm)],[39, 36])).
% 1.31/1.50 tff(41,plain,
% 1.31/1.50 (member(first(ordered_pair(u, v)), universal_class)),
% 1.31/1.50 inference(unit_resolution,[status(thm)],[40, 29])).
% 1.31/1.50 tff(42,plain,
% 1.31/1.50 (^[Y: $i, X: $i] : refl(((~member(X, universal_class)) | member(X, unordered_pair(X, Y))) <=> ((~member(X, universal_class)) | member(X, unordered_pair(X, Y))))),
% 1.31/1.50 inference(bind,[status(th)],[])).
% 1.31/1.50 tff(43,plain,
% 1.31/1.50 (![Y: $i, X: $i] : ((~member(X, universal_class)) | member(X, unordered_pair(X, Y))) <=> ![Y: $i, X: $i] : ((~member(X, universal_class)) | member(X, unordered_pair(X, Y)))),
% 1.31/1.50 inference(quant_intro,[status(thm)],[42])).
% 1.31/1.50 tff(44,plain,
% 1.31/1.50 (![Y: $i, X: $i] : ((~member(X, universal_class)) | member(X, unordered_pair(X, Y))) <=> ![Y: $i, X: $i] : ((~member(X, universal_class)) | member(X, unordered_pair(X, Y)))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(45,axiom,(![Y: $i, X: $i] : ((~member(X, universal_class)) | member(X, unordered_pair(X, Y)))), file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax','unordered_pair2')).
% 1.31/1.50 tff(46,plain,
% 1.31/1.50 (![Y: $i, X: $i] : ((~member(X, universal_class)) | member(X, unordered_pair(X, Y)))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[45, 44])).
% 1.31/1.50 tff(47,plain,(
% 1.31/1.50 ![Y: $i, X: $i] : ((~member(X, universal_class)) | member(X, unordered_pair(X, Y)))),
% 1.31/1.50 inference(skolemize,[status(sab)],[46])).
% 1.31/1.50 tff(48,plain,
% 1.31/1.50 (![Y: $i, X: $i] : ((~member(X, universal_class)) | member(X, unordered_pair(X, Y)))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[47, 43])).
% 1.31/1.50 tff(49,plain,
% 1.31/1.50 (((~![Y: $i, X: $i] : ((~member(X, universal_class)) | member(X, unordered_pair(X, Y)))) | ((~member(first(ordered_pair(u, v)), universal_class)) | member(first(ordered_pair(u, v)), unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v)))))) <=> ((~![Y: $i, X: $i] : ((~member(X, universal_class)) | member(X, unordered_pair(X, Y)))) | (~member(first(ordered_pair(u, v)), universal_class)) | member(first(ordered_pair(u, v)), unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v)))))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(50,plain,
% 1.31/1.50 ((~![Y: $i, X: $i] : ((~member(X, universal_class)) | member(X, unordered_pair(X, Y)))) | ((~member(first(ordered_pair(u, v)), universal_class)) | member(first(ordered_pair(u, v)), unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v)))))),
% 1.31/1.50 inference(quant_inst,[status(thm)],[])).
% 1.31/1.50 tff(51,plain,
% 1.31/1.50 ((~![Y: $i, X: $i] : ((~member(X, universal_class)) | member(X, unordered_pair(X, Y)))) | (~member(first(ordered_pair(u, v)), universal_class)) | member(first(ordered_pair(u, v)), unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[50, 49])).
% 1.31/1.50 tff(52,plain,
% 1.31/1.50 (member(first(ordered_pair(u, v)), unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))))),
% 1.31/1.50 inference(unit_resolution,[status(thm)],[51, 48, 41])).
% 1.31/1.50 tff(53,plain,
% 1.31/1.50 (member(first(ordered_pair(u, v)), singleton(first(ordered_pair(u, v))))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[52, 12])).
% 1.31/1.50 tff(54,plain,
% 1.31/1.50 (member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class)) <=> member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class))),
% 1.31/1.50 inference(monotonicity,[status(thm)],[26])).
% 1.31/1.50 tff(55,plain,
% 1.31/1.50 (member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class)) <=> member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class))),
% 1.31/1.50 inference(symmetry,[status(thm)],[54])).
% 1.31/1.50 tff(56,plain,
% 1.31/1.50 ((u = first(ordered_pair(u, v))) <=> (first(ordered_pair(u, v)) = u)),
% 1.31/1.50 inference(commutativity,[status(thm)],[])).
% 1.31/1.50 tff(57,plain,
% 1.31/1.50 ((first(ordered_pair(u, v)) = u) <=> (u = first(ordered_pair(u, v)))),
% 1.31/1.50 inference(symmetry,[status(thm)],[56])).
% 1.31/1.50 tff(58,plain,
% 1.31/1.50 ((~(first(ordered_pair(u, v)) = u)) <=> (~(u = first(ordered_pair(u, v))))),
% 1.31/1.50 inference(monotonicity,[status(thm)],[57])).
% 1.31/1.50 tff(59,plain,
% 1.31/1.50 ((~(first(ordered_pair(u, v)) = u)) <=> (~(first(ordered_pair(u, v)) = u))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(60,axiom,(~(first(ordered_pair(u, v)) = u)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_unique_1st_and_2nd_in_pair_of_sets1_2')).
% 1.31/1.50 tff(61,plain,
% 1.31/1.50 (~(first(ordered_pair(u, v)) = u)),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[60, 59])).
% 1.31/1.50 tff(62,plain,
% 1.31/1.50 (~(u = first(ordered_pair(u, v)))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[61, 58])).
% 1.31/1.50 tff(63,plain,
% 1.31/1.50 (member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v)))) <=> member(u, singleton(first(ordered_pair(u, v))))),
% 1.31/1.50 inference(monotonicity,[status(thm)],[9])).
% 1.31/1.50 tff(64,plain,
% 1.31/1.50 (member(u, singleton(first(ordered_pair(u, v)))) <=> member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))))),
% 1.31/1.50 inference(symmetry,[status(thm)],[63])).
% 1.31/1.50 tff(65,assumption,(member(u, singleton(first(ordered_pair(u, v))))), introduced(assumption)).
% 1.31/1.50 tff(66,plain,
% 1.31/1.50 (member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[65, 64])).
% 1.31/1.50 tff(67,plain,
% 1.31/1.50 (^[Y: $i, U: $i, X: $i] : refl(((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y)))) <=> ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y)))))),
% 1.31/1.50 inference(bind,[status(th)],[])).
% 1.31/1.50 tff(68,plain,
% 1.31/1.50 (![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y)))) <=> ![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))),
% 1.31/1.50 inference(quant_intro,[status(thm)],[67])).
% 1.31/1.50 tff(69,plain,
% 1.31/1.50 (![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y)))) <=> ![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(70,plain,
% 1.31/1.50 (^[Y: $i, U: $i, X: $i] : rewrite((((~member(U, unordered_pair(X, Y))) | (U = X)) | (U = Y)) <=> ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y)))))),
% 1.31/1.50 inference(bind,[status(th)],[])).
% 1.31/1.50 tff(71,plain,
% 1.31/1.50 (![Y: $i, U: $i, X: $i] : (((~member(U, unordered_pair(X, Y))) | (U = X)) | (U = Y)) <=> ![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))),
% 1.31/1.50 inference(quant_intro,[status(thm)],[70])).
% 1.31/1.50 tff(72,axiom,(![Y: $i, U: $i, X: $i] : (((~member(U, unordered_pair(X, Y))) | (U = X)) | (U = Y))), file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax','unordered_pair_member')).
% 1.31/1.50 tff(73,plain,
% 1.31/1.50 (![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[72, 71])).
% 1.31/1.50 tff(74,plain,
% 1.31/1.50 (![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[73, 69])).
% 1.31/1.50 tff(75,plain,(
% 1.31/1.50 ![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))),
% 1.31/1.50 inference(skolemize,[status(sab)],[74])).
% 1.31/1.50 tff(76,plain,
% 1.31/1.50 (![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[75, 68])).
% 1.31/1.50 tff(77,plain,
% 1.31/1.50 (((~![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))) | ((u = first(ordered_pair(u, v))) | (~member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))))))) <=> ((~![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))) | (u = first(ordered_pair(u, v))) | (~member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))))))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(78,plain,
% 1.31/1.50 (((u = first(ordered_pair(u, v))) | (u = first(ordered_pair(u, v))) | (~member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v)))))) <=> ((u = first(ordered_pair(u, v))) | (~member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))))))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(79,plain,
% 1.31/1.50 (((~![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))) | ((u = first(ordered_pair(u, v))) | (u = first(ordered_pair(u, v))) | (~member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))))))) <=> ((~![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))) | ((u = first(ordered_pair(u, v))) | (~member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v)))))))),
% 1.31/1.50 inference(monotonicity,[status(thm)],[78])).
% 1.31/1.50 tff(80,plain,
% 1.31/1.50 (((~![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))) | ((u = first(ordered_pair(u, v))) | (u = first(ordered_pair(u, v))) | (~member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))))))) <=> ((~![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))) | (u = first(ordered_pair(u, v))) | (~member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))))))),
% 1.31/1.50 inference(transitivity,[status(thm)],[79, 77])).
% 1.31/1.50 tff(81,plain,
% 1.31/1.50 ((~![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))) | ((u = first(ordered_pair(u, v))) | (u = first(ordered_pair(u, v))) | (~member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v))))))),
% 1.31/1.50 inference(quant_inst,[status(thm)],[])).
% 1.31/1.50 tff(82,plain,
% 1.31/1.50 ((~![Y: $i, U: $i, X: $i] : ((U = Y) | (U = X) | (~member(U, unordered_pair(X, Y))))) | (u = first(ordered_pair(u, v))) | (~member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v)))))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[81, 80])).
% 1.31/1.50 tff(83,plain,
% 1.31/1.50 ((u = first(ordered_pair(u, v))) | (~member(u, unordered_pair(first(ordered_pair(u, v)), first(ordered_pair(u, v)))))),
% 1.31/1.50 inference(unit_resolution,[status(thm)],[82, 76])).
% 1.31/1.50 tff(84,plain,
% 1.31/1.50 ($false),
% 1.31/1.50 inference(unit_resolution,[status(thm)],[83, 66, 62])).
% 1.31/1.50 tff(85,plain,(~member(u, singleton(first(ordered_pair(u, v))))), inference(lemma,lemma(discharge,[]))).
% 1.31/1.50 tff(86,assumption,(~member(u, complement(singleton(first(ordered_pair(u, v)))))), introduced(assumption)).
% 1.31/1.50 tff(87,plain,
% 1.31/1.50 (((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))) | ((~member(ordered_pair(u, v), cross_product(universal_class, universal_class))) | member(u, universal_class))) <=> ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))) | (~member(ordered_pair(u, v), cross_product(universal_class, universal_class))) | member(u, universal_class))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(88,plain,
% 1.31/1.50 ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))) | ((~member(ordered_pair(u, v), cross_product(universal_class, universal_class))) | member(u, universal_class))),
% 1.31/1.50 inference(quant_inst,[status(thm)],[])).
% 1.31/1.50 tff(89,plain,
% 1.31/1.50 ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))) | (~member(ordered_pair(u, v), cross_product(universal_class, universal_class))) | member(u, universal_class)),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[88, 87])).
% 1.31/1.50 tff(90,plain,
% 1.31/1.50 (member(u, universal_class)),
% 1.31/1.50 inference(unit_resolution,[status(thm)],[89, 36, 15])).
% 1.31/1.50 tff(91,plain,
% 1.31/1.50 (^[Z: $i, X: $i] : refl((member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X))) <=> (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X))))),
% 1.31/1.50 inference(bind,[status(th)],[])).
% 1.31/1.50 tff(92,plain,
% 1.31/1.50 (![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X))) <=> ![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))),
% 1.31/1.50 inference(quant_intro,[status(thm)],[91])).
% 1.31/1.50 tff(93,plain,
% 1.31/1.50 (![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X))) <=> ![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(94,plain,
% 1.31/1.50 (^[Z: $i, X: $i] : rewrite((((~member(Z, universal_class)) | member(Z, complement(X))) | member(Z, X)) <=> (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X))))),
% 1.31/1.50 inference(bind,[status(th)],[])).
% 1.31/1.50 tff(95,plain,
% 1.31/1.50 (![Z: $i, X: $i] : (((~member(Z, universal_class)) | member(Z, complement(X))) | member(Z, X)) <=> ![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))),
% 1.31/1.50 inference(quant_intro,[status(thm)],[94])).
% 1.31/1.50 tff(96,axiom,(![Z: $i, X: $i] : (((~member(Z, universal_class)) | member(Z, complement(X))) | member(Z, X))), file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax','complement2')).
% 1.31/1.50 tff(97,plain,
% 1.31/1.50 (![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[96, 95])).
% 1.31/1.50 tff(98,plain,
% 1.31/1.50 (![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[97, 93])).
% 1.31/1.50 tff(99,plain,(
% 1.31/1.50 ![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))),
% 1.31/1.50 inference(skolemize,[status(sab)],[98])).
% 1.31/1.50 tff(100,plain,
% 1.31/1.50 (![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[99, 92])).
% 1.31/1.50 tff(101,plain,
% 1.31/1.50 (((~![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))) | ((~member(u, universal_class)) | member(u, complement(singleton(first(ordered_pair(u, v))))) | member(u, singleton(first(ordered_pair(u, v)))))) <=> ((~![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))) | (~member(u, universal_class)) | member(u, complement(singleton(first(ordered_pair(u, v))))) | member(u, singleton(first(ordered_pair(u, v)))))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(102,plain,
% 1.31/1.50 ((member(u, singleton(first(ordered_pair(u, v)))) | (~member(u, universal_class)) | member(u, complement(singleton(first(ordered_pair(u, v)))))) <=> ((~member(u, universal_class)) | member(u, complement(singleton(first(ordered_pair(u, v))))) | member(u, singleton(first(ordered_pair(u, v)))))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(103,plain,
% 1.31/1.50 (((~![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))) | (member(u, singleton(first(ordered_pair(u, v)))) | (~member(u, universal_class)) | member(u, complement(singleton(first(ordered_pair(u, v))))))) <=> ((~![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))) | ((~member(u, universal_class)) | member(u, complement(singleton(first(ordered_pair(u, v))))) | member(u, singleton(first(ordered_pair(u, v))))))),
% 1.31/1.50 inference(monotonicity,[status(thm)],[102])).
% 1.31/1.50 tff(104,plain,
% 1.31/1.50 (((~![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))) | (member(u, singleton(first(ordered_pair(u, v)))) | (~member(u, universal_class)) | member(u, complement(singleton(first(ordered_pair(u, v))))))) <=> ((~![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))) | (~member(u, universal_class)) | member(u, complement(singleton(first(ordered_pair(u, v))))) | member(u, singleton(first(ordered_pair(u, v)))))),
% 1.31/1.50 inference(transitivity,[status(thm)],[103, 101])).
% 1.31/1.50 tff(105,plain,
% 1.31/1.50 ((~![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))) | (member(u, singleton(first(ordered_pair(u, v)))) | (~member(u, universal_class)) | member(u, complement(singleton(first(ordered_pair(u, v))))))),
% 1.31/1.50 inference(quant_inst,[status(thm)],[])).
% 1.31/1.50 tff(106,plain,
% 1.31/1.50 ((~![Z: $i, X: $i] : (member(Z, X) | (~member(Z, universal_class)) | member(Z, complement(X)))) | (~member(u, universal_class)) | member(u, complement(singleton(first(ordered_pair(u, v))))) | member(u, singleton(first(ordered_pair(u, v))))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[105, 104])).
% 1.31/1.50 tff(107,plain,
% 1.31/1.50 ($false),
% 1.31/1.50 inference(unit_resolution,[status(thm)],[106, 100, 90, 86, 85])).
% 1.31/1.50 tff(108,plain,(member(u, complement(singleton(first(ordered_pair(u, v)))))), inference(lemma,lemma(discharge,[]))).
% 1.31/1.50 tff(109,plain,
% 1.31/1.50 (^[V: $i, Y: $i, U: $i, X: $i] : refl(((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y)) <=> ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y)))),
% 1.31/1.50 inference(bind,[status(th)],[])).
% 1.31/1.50 tff(110,plain,
% 1.31/1.50 (![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y)) <=> ![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y))),
% 1.31/1.50 inference(quant_intro,[status(thm)],[109])).
% 1.31/1.50 tff(111,plain,
% 1.31/1.50 (![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y)) <=> ![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(112,axiom,(![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y))), file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax','cartesian_product2')).
% 1.31/1.50 tff(113,plain,
% 1.31/1.50 (![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[112, 111])).
% 1.31/1.50 tff(114,plain,(
% 1.31/1.50 ![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y))),
% 1.31/1.50 inference(skolemize,[status(sab)],[113])).
% 1.31/1.50 tff(115,plain,
% 1.31/1.50 (![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y))),
% 1.31/1.50 inference(modus_ponens,[status(thm)],[114, 110])).
% 1.31/1.50 tff(116,plain,
% 1.31/1.50 (((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y))) | ((~member(ordered_pair(u, v), cross_product(universal_class, universal_class))) | member(v, universal_class))) <=> ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y))) | (~member(ordered_pair(u, v), cross_product(universal_class, universal_class))) | member(v, universal_class))),
% 1.31/1.50 inference(rewrite,[status(thm)],[])).
% 1.31/1.50 tff(117,plain,
% 1.31/1.50 ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y))) | ((~member(ordered_pair(u, v), cross_product(universal_class, universal_class))) | member(v, universal_class))),
% 1.31/1.51 inference(quant_inst,[status(thm)],[])).
% 1.31/1.51 tff(118,plain,
% 1.31/1.51 ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(V, Y))) | (~member(ordered_pair(u, v), cross_product(universal_class, universal_class))) | member(v, universal_class)),
% 1.31/1.51 inference(modus_ponens,[status(thm)],[117, 116])).
% 1.31/1.51 tff(119,plain,
% 1.31/1.51 (member(v, universal_class)),
% 1.31/1.51 inference(unit_resolution,[status(thm)],[118, 115, 15])).
% 1.31/1.51 tff(120,plain,
% 1.31/1.51 (^[V: $i, Y: $i, U: $i, X: $i] : refl(((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y))) <=> ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y))))),
% 1.31/1.51 inference(bind,[status(th)],[])).
% 1.31/1.51 tff(121,plain,
% 1.31/1.51 (![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y))) <=> ![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))),
% 1.31/1.51 inference(quant_intro,[status(thm)],[120])).
% 1.31/1.51 tff(122,plain,
% 1.31/1.51 (![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y))) <=> ![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))),
% 1.31/1.51 inference(rewrite,[status(thm)],[])).
% 1.31/1.51 tff(123,plain,
% 1.31/1.51 (^[V: $i, Y: $i, U: $i, X: $i] : rewrite((((~member(U, X)) | (~member(V, Y))) | member(ordered_pair(U, V), cross_product(X, Y))) <=> ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y))))),
% 1.31/1.51 inference(bind,[status(th)],[])).
% 1.31/1.51 tff(124,plain,
% 1.31/1.51 (![V: $i, Y: $i, U: $i, X: $i] : (((~member(U, X)) | (~member(V, Y))) | member(ordered_pair(U, V), cross_product(X, Y))) <=> ![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))),
% 1.31/1.51 inference(quant_intro,[status(thm)],[123])).
% 1.31/1.51 tff(125,axiom,(![V: $i, Y: $i, U: $i, X: $i] : (((~member(U, X)) | (~member(V, Y))) | member(ordered_pair(U, V), cross_product(X, Y)))), file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax','cartesian_product3')).
% 1.31/1.51 tff(126,plain,
% 1.31/1.51 (![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))),
% 1.31/1.51 inference(modus_ponens,[status(thm)],[125, 124])).
% 1.31/1.51 tff(127,plain,
% 1.31/1.51 (![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))),
% 1.31/1.51 inference(modus_ponens,[status(thm)],[126, 122])).
% 1.31/1.51 tff(128,plain,(
% 1.31/1.51 ![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))),
% 1.31/1.51 inference(skolemize,[status(sab)],[127])).
% 1.31/1.51 tff(129,plain,
% 1.31/1.51 (![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))),
% 1.31/1.51 inference(modus_ponens,[status(thm)],[128, 121])).
% 1.31/1.51 tff(130,plain,
% 1.31/1.51 (((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))) | ((~member(v, universal_class)) | (~member(u, complement(singleton(first(ordered_pair(u, v)))))) | member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class)))) <=> ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))) | (~member(v, universal_class)) | (~member(u, complement(singleton(first(ordered_pair(u, v)))))) | member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class)))),
% 1.31/1.51 inference(rewrite,[status(thm)],[])).
% 1.31/1.51 tff(131,plain,
% 1.31/1.51 (((~member(u, complement(singleton(first(ordered_pair(u, v)))))) | member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class)) | (~member(v, universal_class))) <=> ((~member(v, universal_class)) | (~member(u, complement(singleton(first(ordered_pair(u, v)))))) | member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class)))),
% 1.31/1.51 inference(rewrite,[status(thm)],[])).
% 1.31/1.51 tff(132,plain,
% 1.31/1.51 (((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))) | ((~member(u, complement(singleton(first(ordered_pair(u, v)))))) | member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class)) | (~member(v, universal_class)))) <=> ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))) | ((~member(v, universal_class)) | (~member(u, complement(singleton(first(ordered_pair(u, v)))))) | member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class))))),
% 1.31/1.51 inference(monotonicity,[status(thm)],[131])).
% 1.31/1.51 tff(133,plain,
% 1.31/1.51 (((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))) | ((~member(u, complement(singleton(first(ordered_pair(u, v)))))) | member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class)) | (~member(v, universal_class)))) <=> ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))) | (~member(v, universal_class)) | (~member(u, complement(singleton(first(ordered_pair(u, v)))))) | member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class)))),
% 1.31/1.51 inference(transitivity,[status(thm)],[132, 130])).
% 1.31/1.51 tff(134,plain,
% 1.31/1.51 ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))) | ((~member(u, complement(singleton(first(ordered_pair(u, v)))))) | member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class)) | (~member(v, universal_class)))),
% 1.31/1.51 inference(quant_inst,[status(thm)],[])).
% 1.31/1.51 tff(135,plain,
% 1.31/1.51 ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(U, X)) | member(ordered_pair(U, V), cross_product(X, Y)) | (~member(V, Y)))) | (~member(v, universal_class)) | (~member(u, complement(singleton(first(ordered_pair(u, v)))))) | member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class))),
% 1.31/1.51 inference(modus_ponens,[status(thm)],[134, 133])).
% 1.31/1.51 tff(136,plain,
% 1.31/1.51 ((~member(u, complement(singleton(first(ordered_pair(u, v)))))) | member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class))),
% 1.31/1.51 inference(unit_resolution,[status(thm)],[135, 129, 119])).
% 1.31/1.51 tff(137,plain,
% 1.31/1.51 (member(ordered_pair(u, v), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class))),
% 1.31/1.51 inference(unit_resolution,[status(thm)],[136, 108])).
% 1.31/1.51 tff(138,plain,
% 1.31/1.51 (member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class))),
% 1.31/1.51 inference(modus_ponens,[status(thm)],[137, 55])).
% 1.31/1.51 tff(139,plain,
% 1.31/1.51 (((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))) | ((~member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class))) | member(first(ordered_pair(u, v)), complement(singleton(first(ordered_pair(u, v))))))) <=> ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))) | (~member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class))) | member(first(ordered_pair(u, v)), complement(singleton(first(ordered_pair(u, v))))))),
% 1.31/1.51 inference(rewrite,[status(thm)],[])).
% 1.31/1.51 tff(140,plain,
% 1.31/1.51 ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))) | ((~member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class))) | member(first(ordered_pair(u, v)), complement(singleton(first(ordered_pair(u, v))))))),
% 1.31/1.51 inference(quant_inst,[status(thm)],[])).
% 1.31/1.51 tff(141,plain,
% 1.31/1.51 ((~![V: $i, Y: $i, U: $i, X: $i] : ((~member(ordered_pair(U, V), cross_product(X, Y))) | member(U, X))) | (~member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class))) | member(first(ordered_pair(u, v)), complement(singleton(first(ordered_pair(u, v)))))),
% 1.31/1.51 inference(modus_ponens,[status(thm)],[140, 139])).
% 1.31/1.51 tff(142,plain,
% 1.31/1.51 ((~member(ordered_pair(first(ordered_pair(u, v)), second(ordered_pair(u, v))), cross_product(complement(singleton(first(ordered_pair(u, v)))), universal_class))) | member(first(ordered_pair(u, v)), complement(singleton(first(ordered_pair(u, v)))))),
% 1.31/1.51 inference(unit_resolution,[status(thm)],[141, 36])).
% 1.31/1.51 tff(143,plain,
% 1.31/1.51 (member(first(ordered_pair(u, v)), complement(singleton(first(ordered_pair(u, v)))))),
% 1.31/1.51 inference(unit_resolution,[status(thm)],[142, 138])).
% 1.31/1.51 tff(144,plain,
% 1.31/1.51 (^[Z: $i, X: $i] : refl(((~member(Z, X)) | (~member(Z, complement(X)))) <=> ((~member(Z, X)) | (~member(Z, complement(X)))))),
% 1.31/1.51 inference(bind,[status(th)],[])).
% 1.31/1.51 tff(145,plain,
% 1.31/1.51 (![Z: $i, X: $i] : ((~member(Z, X)) | (~member(Z, complement(X)))) <=> ![Z: $i, X: $i] : ((~member(Z, X)) | (~member(Z, complement(X))))),
% 1.31/1.51 inference(quant_intro,[status(thm)],[144])).
% 1.31/1.51 tff(146,plain,
% 1.31/1.51 (![Z: $i, X: $i] : ((~member(Z, X)) | (~member(Z, complement(X)))) <=> ![Z: $i, X: $i] : ((~member(Z, X)) | (~member(Z, complement(X))))),
% 1.31/1.51 inference(rewrite,[status(thm)],[])).
% 1.31/1.51 tff(147,plain,
% 1.31/1.51 (^[Z: $i, X: $i] : rewrite(((~member(Z, complement(X))) | (~member(Z, X))) <=> ((~member(Z, X)) | (~member(Z, complement(X)))))),
% 1.31/1.51 inference(bind,[status(th)],[])).
% 1.31/1.51 tff(148,plain,
% 1.31/1.51 (![Z: $i, X: $i] : ((~member(Z, complement(X))) | (~member(Z, X))) <=> ![Z: $i, X: $i] : ((~member(Z, X)) | (~member(Z, complement(X))))),
% 1.31/1.51 inference(quant_intro,[status(thm)],[147])).
% 1.31/1.51 tff(149,axiom,(![Z: $i, X: $i] : ((~member(Z, complement(X))) | (~member(Z, X)))), file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax','complement1')).
% 1.31/1.51 tff(150,plain,
% 1.31/1.51 (![Z: $i, X: $i] : ((~member(Z, X)) | (~member(Z, complement(X))))),
% 1.31/1.51 inference(modus_ponens,[status(thm)],[149, 148])).
% 1.31/1.51 tff(151,plain,
% 1.31/1.51 (![Z: $i, X: $i] : ((~member(Z, X)) | (~member(Z, complement(X))))),
% 1.31/1.51 inference(modus_ponens,[status(thm)],[150, 146])).
% 1.31/1.51 tff(152,plain,(
% 1.31/1.51 ![Z: $i, X: $i] : ((~member(Z, X)) | (~member(Z, complement(X))))),
% 1.31/1.51 inference(skolemize,[status(sab)],[151])).
% 1.31/1.51 tff(153,plain,
% 1.31/1.51 (![Z: $i, X: $i] : ((~member(Z, X)) | (~member(Z, complement(X))))),
% 1.31/1.51 inference(modus_ponens,[status(thm)],[152, 145])).
% 1.31/1.51 tff(154,plain,
% 1.31/1.51 (((~![Z: $i, X: $i] : ((~member(Z, X)) | (~member(Z, complement(X))))) | ((~member(first(ordered_pair(u, v)), singleton(first(ordered_pair(u, v))))) | (~member(first(ordered_pair(u, v)), complement(singleton(first(ordered_pair(u, v)))))))) <=> ((~![Z: $i, X: $i] : ((~member(Z, X)) | (~member(Z, complement(X))))) | (~member(first(ordered_pair(u, v)), singleton(first(ordered_pair(u, v))))) | (~member(first(ordered_pair(u, v)), complement(singleton(first(ordered_pair(u, v)))))))),
% 1.31/1.51 inference(rewrite,[status(thm)],[])).
% 1.31/1.51 tff(155,plain,
% 1.31/1.51 ((~![Z: $i, X: $i] : ((~member(Z, X)) | (~member(Z, complement(X))))) | ((~member(first(ordered_pair(u, v)), singleton(first(ordered_pair(u, v))))) | (~member(first(ordered_pair(u, v)), complement(singleton(first(ordered_pair(u, v)))))))),
% 1.31/1.51 inference(quant_inst,[status(thm)],[])).
% 1.31/1.51 tff(156,plain,
% 1.31/1.51 ((~![Z: $i, X: $i] : ((~member(Z, X)) | (~member(Z, complement(X))))) | (~member(first(ordered_pair(u, v)), singleton(first(ordered_pair(u, v))))) | (~member(first(ordered_pair(u, v)), complement(singleton(first(ordered_pair(u, v))))))),
% 1.31/1.51 inference(modus_ponens,[status(thm)],[155, 154])).
% 1.31/1.51 tff(157,plain,
% 1.31/1.51 ($false),
% 1.31/1.51 inference(unit_resolution,[status(thm)],[156, 153, 143, 53])).
% 1.31/1.51 % SZS output end Proof
% 1.31/1.52 % E exiting
%------------------------------------------------------------------------------