%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWX200+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% 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 : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 07:08:15 PM UTC 2026
% Result : Theorem 6.14s 6.37s
% Output : Proof 6.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX200+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.15/0.33 % Computer : n026.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 11:15:40 EDT 2026
% 0.15/0.33 % CPUTime :
% 6.14/6.37 % SZS status Theorem
% 6.14/6.37 % SZS output start Proof
% 6.14/6.37 tff(ord_type, type, (
% 6.14/6.37 ord: $i > $o)).
% 6.14/6.37 tff(merge_type, type, (
% 6.14/6.37 merge: ( $i * $i ) > $i)).
% 6.14/6.37 tff(cons_type, type, (
% 6.14/6.37 cons: ( $i * $i ) > $i)).
% 6.14/6.37 tff(nil_type, type, (
% 6.14/6.37 nil: $i)).
% 6.14/6.37 tff(z_type, type, (
% 6.14/6.37 z: $i)).
% 6.14/6.37 tff(s_type, type, (
% 6.14/6.37 s: $i > $i)).
% 6.14/6.37 tff(leqNat_type, type, (
% 6.14/6.37 leqNat: ( $i * $i ) > $o)).
% 6.14/6.37 tff(1,plain,
% 6.14/6.37 (^[Y: $i] : refl((merge(nil, Y) = Y) <=> (merge(nil, Y) = Y))),
% 6.14/6.37 inference(bind,[status(th)],[])).
% 6.14/6.37 tff(2,plain,
% 6.14/6.37 (![Y: $i] : (merge(nil, Y) = Y) <=> ![Y: $i] : (merge(nil, Y) = Y)),
% 6.14/6.37 inference(quant_intro,[status(thm)],[1])).
% 6.14/6.37 tff(3,plain,
% 6.14/6.37 (![Y: $i] : (merge(nil, Y) = Y) <=> ![Y: $i] : (merge(nil, Y) = Y)),
% 6.14/6.37 inference(rewrite,[status(thm)],[])).
% 6.14/6.37 tff(4,axiom,(![Y: $i] : (merge(nil, Y) = Y)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_009')).
% 6.14/6.37 tff(5,plain,
% 6.14/6.37 (![Y: $i] : (merge(nil, Y) = Y)),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[4, 3])).
% 6.14/6.37 tff(6,plain,(
% 6.14/6.37 ![Y: $i] : (merge(nil, Y) = Y)),
% 6.14/6.37 inference(skolemize,[status(sab)],[5])).
% 6.14/6.37 tff(7,plain,
% 6.14/6.37 (![Y: $i] : (merge(nil, Y) = Y)),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[6, 2])).
% 6.14/6.37 tff(8,plain,
% 6.14/6.37 ((~![Y: $i] : (merge(nil, Y) = Y)) | (merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))) = cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))),
% 6.14/6.37 inference(quant_inst,[status(thm)],[])).
% 6.14/6.37 tff(9,plain,
% 6.14/6.37 (merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))) = cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))),
% 6.14/6.37 inference(unit_resolution,[status(thm)],[8, 7])).
% 6.14/6.37 tff(10,plain,
% 6.14/6.37 (ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))) <=> ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))),
% 6.14/6.37 inference(monotonicity,[status(thm)],[9])).
% 6.14/6.37 tff(11,plain,
% 6.14/6.37 (ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))) <=> ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))))),
% 6.14/6.37 inference(symmetry,[status(thm)],[10])).
% 6.14/6.37 tff(12,plain,
% 6.14/6.37 ((~ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))) <=> (~ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))))),
% 6.14/6.37 inference(monotonicity,[status(thm)],[11])).
% 6.14/6.37 tff(13,plain,
% 6.14/6.37 (^[Z: $i] : refl((~leqNat(s(Z), z)) <=> (~leqNat(s(Z), z)))),
% 6.14/6.37 inference(bind,[status(th)],[])).
% 6.14/6.37 tff(14,plain,
% 6.14/6.37 (![Z: $i] : (~leqNat(s(Z), z)) <=> ![Z: $i] : (~leqNat(s(Z), z))),
% 6.14/6.37 inference(quant_intro,[status(thm)],[13])).
% 6.14/6.37 tff(15,plain,
% 6.14/6.37 (![Z: $i] : (~leqNat(s(Z), z)) <=> ![Z: $i] : (~leqNat(s(Z), z))),
% 6.14/6.37 inference(rewrite,[status(thm)],[])).
% 6.14/6.37 tff(16,axiom,(![Z: $i] : (~leqNat(s(Z), z))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_007')).
% 6.14/6.37 tff(17,plain,
% 6.14/6.37 (![Z: $i] : (~leqNat(s(Z), z))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[16, 15])).
% 6.14/6.37 tff(18,plain,(
% 6.14/6.37 ![Z: $i] : (~leqNat(s(Z), z))),
% 6.14/6.37 inference(skolemize,[status(sab)],[17])).
% 6.14/6.37 tff(19,plain,
% 6.14/6.37 (![Z: $i] : (~leqNat(s(Z), z))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[18, 14])).
% 6.14/6.37 tff(20,plain,
% 6.14/6.37 ((~![Z: $i] : (~leqNat(s(Z), z))) | (~leqNat(s(nil), z))),
% 6.14/6.37 inference(quant_inst,[status(thm)],[])).
% 6.14/6.37 tff(21,plain,
% 6.14/6.37 (~leqNat(s(nil), z)),
% 6.14/6.37 inference(unit_resolution,[status(thm)],[20, 19])).
% 6.14/6.37 tff(22,plain,
% 6.14/6.37 (^[Z: $i, Xs: $i, Y2: $i, Ys: $i] : refl((leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys)))) <=> (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys)))))),
% 6.14/6.37 inference(bind,[status(th)],[])).
% 6.14/6.37 tff(23,plain,
% 6.14/6.37 (![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys)))) <=> ![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys))))),
% 6.14/6.37 inference(quant_intro,[status(thm)],[22])).
% 6.14/6.37 tff(24,plain,
% 6.14/6.37 (![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys)))) <=> ![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys))))),
% 6.14/6.37 inference(rewrite,[status(thm)],[])).
% 6.14/6.37 tff(25,plain,
% 6.14/6.37 (^[Z: $i, Xs: $i, Y2: $i, Ys: $i] : rewrite(((~leqNat(Z, Y2)) => (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys)))) <=> (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys)))))),
% 6.14/6.37 inference(bind,[status(th)],[])).
% 6.14/6.37 tff(26,plain,
% 6.14/6.37 (![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) => (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys)))) <=> ![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys))))),
% 6.14/6.37 inference(quant_intro,[status(thm)],[25])).
% 6.14/6.37 tff(27,axiom,(![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) => (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_012')).
% 6.14/6.37 tff(28,plain,
% 6.14/6.37 (![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys))))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[27, 26])).
% 6.14/6.37 tff(29,plain,
% 6.14/6.37 (![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys))))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[28, 24])).
% 6.14/6.37 tff(30,plain,(
% 6.14/6.37 ![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys))))),
% 6.14/6.37 inference(skolemize,[status(sab)],[29])).
% 6.14/6.37 tff(31,plain,
% 6.14/6.37 (![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys))))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[30, 23])).
% 6.14/6.37 tff(32,plain,
% 6.14/6.37 (((~![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys))))) | (leqNat(s(nil), z) | (merge(cons(s(nil), nil), cons(z, cons(nil, nil))) = cons(z, merge(cons(s(nil), nil), cons(nil, nil)))))) <=> ((~![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys))))) | leqNat(s(nil), z) | (merge(cons(s(nil), nil), cons(z, cons(nil, nil))) = cons(z, merge(cons(s(nil), nil), cons(nil, nil)))))),
% 6.14/6.37 inference(rewrite,[status(thm)],[])).
% 6.14/6.37 tff(33,plain,
% 6.14/6.37 ((~![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys))))) | (leqNat(s(nil), z) | (merge(cons(s(nil), nil), cons(z, cons(nil, nil))) = cons(z, merge(cons(s(nil), nil), cons(nil, nil)))))),
% 6.14/6.37 inference(quant_inst,[status(thm)],[])).
% 6.14/6.37 tff(34,plain,
% 6.14/6.37 ((~![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Y2, merge(cons(Z, Xs), Ys))))) | leqNat(s(nil), z) | (merge(cons(s(nil), nil), cons(z, cons(nil, nil))) = cons(z, merge(cons(s(nil), nil), cons(nil, nil))))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[33, 32])).
% 6.14/6.37 tff(35,plain,
% 6.14/6.37 (merge(cons(s(nil), nil), cons(z, cons(nil, nil))) = cons(z, merge(cons(s(nil), nil), cons(nil, nil)))),
% 6.14/6.37 inference(unit_resolution,[status(thm)],[34, 31, 21])).
% 6.14/6.37 tff(36,plain,
% 6.14/6.37 (cons(z, merge(cons(s(nil), nil), cons(nil, nil))) = merge(cons(s(nil), nil), cons(z, cons(nil, nil)))),
% 6.14/6.37 inference(symmetry,[status(thm)],[35])).
% 6.14/6.37 tff(37,plain,
% 6.14/6.37 ((~![Y: $i] : (merge(nil, Y) = Y)) | (merge(nil, cons(nil, cons(nil, nil))) = cons(nil, cons(nil, nil)))),
% 6.14/6.37 inference(quant_inst,[status(thm)],[])).
% 6.14/6.37 tff(38,plain,
% 6.14/6.37 (merge(nil, cons(nil, cons(nil, nil))) = cons(nil, cons(nil, nil))),
% 6.14/6.37 inference(unit_resolution,[status(thm)],[37, 7])).
% 6.14/6.37 tff(39,plain,
% 6.14/6.37 (cons(nil, cons(nil, nil)) = merge(nil, cons(nil, cons(nil, nil)))),
% 6.14/6.37 inference(symmetry,[status(thm)],[38])).
% 6.14/6.37 tff(40,plain,
% 6.14/6.37 (cons(nil, cons(nil, cons(nil, nil))) = cons(nil, merge(nil, cons(nil, cons(nil, nil))))),
% 6.14/6.37 inference(monotonicity,[status(thm)],[39])).
% 6.14/6.37 tff(41,plain,
% 6.14/6.37 (cons(s(nil), cons(nil, cons(nil, cons(nil, nil)))) = cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))),
% 6.14/6.37 inference(monotonicity,[status(thm)],[40])).
% 6.14/6.37 tff(42,plain,
% 6.14/6.37 (cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))) = cons(s(nil), cons(nil, cons(nil, cons(nil, nil))))),
% 6.14/6.37 inference(symmetry,[status(thm)],[41])).
% 6.14/6.37 tff(43,plain,
% 6.14/6.37 ((~![Y: $i] : (merge(nil, Y) = Y)) | (merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) = cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))),
% 6.14/6.37 inference(quant_inst,[status(thm)],[])).
% 6.14/6.37 tff(44,plain,
% 6.14/6.37 (merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) = cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))),
% 6.14/6.37 inference(unit_resolution,[status(thm)],[43, 7])).
% 6.14/6.37 tff(45,plain,
% 6.14/6.37 (merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) = cons(s(nil), cons(nil, cons(nil, cons(nil, nil))))),
% 6.14/6.37 inference(transitivity,[status(thm)],[44, 42])).
% 6.14/6.37 tff(46,plain,
% 6.14/6.37 (ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))) <=> ord(cons(s(nil), cons(nil, cons(nil, cons(nil, nil)))))),
% 6.14/6.37 inference(monotonicity,[status(thm)],[45])).
% 6.14/6.37 tff(47,plain,
% 6.14/6.37 (ord(cons(s(nil), cons(nil, cons(nil, cons(nil, nil))))) <=> ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))))),
% 6.14/6.37 inference(symmetry,[status(thm)],[46])).
% 6.14/6.37 tff(48,plain,
% 6.14/6.37 ((~ord(cons(s(nil), cons(nil, cons(nil, cons(nil, nil)))))) <=> (~ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))))),
% 6.14/6.37 inference(monotonicity,[status(thm)],[47])).
% 6.14/6.37 tff(49,assumption,(~ord(cons(s(nil), cons(nil, cons(nil, cons(nil, nil)))))), introduced(assumption)).
% 6.14/6.37 tff(50,plain,
% 6.14/6.37 (~ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[49, 48])).
% 6.14/6.37 tff(51,plain,
% 6.14/6.37 (ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) <=> ord(cons(s(nil), cons(nil, cons(nil, cons(nil, nil)))))),
% 6.14/6.37 inference(monotonicity,[status(thm)],[42])).
% 6.14/6.37 tff(52,plain,
% 6.14/6.37 (ord(cons(s(nil), cons(nil, cons(nil, cons(nil, nil))))) <=> ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))),
% 6.14/6.37 inference(symmetry,[status(thm)],[51])).
% 6.14/6.37 tff(53,plain,
% 6.14/6.37 ((~ord(cons(s(nil), cons(nil, cons(nil, cons(nil, nil)))))) <=> (~ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))))),
% 6.14/6.37 inference(monotonicity,[status(thm)],[52])).
% 6.14/6.37 tff(54,plain,
% 6.14/6.37 (~ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[49, 53])).
% 6.14/6.37 tff(55,plain,
% 6.14/6.37 (^[Xs: $i, Ys: $i] : refl((ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs))) <=> (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs))))),
% 6.14/6.37 inference(bind,[status(th)],[])).
% 6.14/6.37 tff(56,plain,
% 6.14/6.37 (![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs))) <=> ![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))),
% 6.14/6.37 inference(quant_intro,[status(thm)],[55])).
% 6.14/6.37 tff(57,plain,
% 6.14/6.37 ((~?[Xs: $i, Ys: $i] : (~(ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs))))) <=> (~?[Xs: $i, Ys: $i] : (~(ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))))),
% 6.14/6.37 inference(rewrite,[status(thm)],[])).
% 6.14/6.37 tff(58,plain,
% 6.14/6.37 ((~?[Xs: $i, Ys: $i] : (~(ord(Xs) => ((~ord(Ys)) => ord(merge(Xs, Ys)))))) <=> (~?[Xs: $i, Ys: $i] : (~(ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))))),
% 6.14/6.37 inference(rewrite,[status(thm)],[])).
% 6.14/6.37 tff(59,axiom,(~?[Xs: $i, Ys: $i] : (~(ord(Xs) => ((~ord(Ys)) => ord(merge(Xs, Ys)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','goal_016')).
% 6.14/6.37 tff(60,plain,
% 6.14/6.37 (~?[Xs: $i, Ys: $i] : (~(ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs))))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[59, 58])).
% 6.14/6.37 tff(61,plain,
% 6.14/6.37 (~?[Xs: $i, Ys: $i] : (~(ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs))))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[60, 57])).
% 6.14/6.37 tff(62,plain,
% 6.14/6.37 (~?[Xs: $i, Ys: $i] : (~(ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs))))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[61, 57])).
% 6.14/6.37 tff(63,plain,
% 6.14/6.37 (~?[Xs: $i, Ys: $i] : (~(ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs))))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[62, 57])).
% 6.14/6.37 tff(64,plain,
% 6.14/6.37 (^[Xs: $i, Ys: $i] : refl($oeq((ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs))), (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))))),
% 6.14/6.37 inference(bind,[status(th)],[])).
% 6.14/6.37 tff(65,plain,(
% 6.14/6.37 ![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))),
% 6.14/6.37 inference(nnf-neg,[status(sab)],[63, 64])).
% 6.14/6.37 tff(66,plain,
% 6.14/6.37 (![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[65, 56])).
% 6.14/6.37 tff(67,plain,
% 6.14/6.37 (ord(nil) <=> ord(nil)),
% 6.14/6.37 inference(rewrite,[status(thm)],[])).
% 6.14/6.37 tff(68,axiom,(ord(nil)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_013')).
% 6.14/6.37 tff(69,plain,
% 6.14/6.37 (ord(nil)),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[68, 67])).
% 6.14/6.37 tff(70,plain,
% 6.14/6.37 (((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | (ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) | ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))) | (~ord(nil)))) <=> ((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) | ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))) | (~ord(nil)))),
% 6.14/6.37 inference(rewrite,[status(thm)],[])).
% 6.14/6.37 tff(71,plain,
% 6.14/6.37 ((ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))) | ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) | (~ord(nil))) <=> (ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) | ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))) | (~ord(nil)))),
% 6.14/6.37 inference(rewrite,[status(thm)],[])).
% 6.14/6.37 tff(72,plain,
% 6.14/6.37 (((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | (ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))) | ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) | (~ord(nil)))) <=> ((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | (ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) | ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))) | (~ord(nil))))),
% 6.14/6.37 inference(monotonicity,[status(thm)],[71])).
% 6.14/6.37 tff(73,plain,
% 6.14/6.37 (((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | (ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))) | ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) | (~ord(nil)))) <=> ((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) | ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))) | (~ord(nil)))),
% 6.14/6.37 inference(transitivity,[status(thm)],[72, 70])).
% 6.14/6.37 tff(74,plain,
% 6.14/6.37 ((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | (ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))) | ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) | (~ord(nil)))),
% 6.14/6.37 inference(quant_inst,[status(thm)],[])).
% 6.14/6.37 tff(75,plain,
% 6.14/6.37 ((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) | ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil))))))) | (~ord(nil))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[74, 73])).
% 6.14/6.37 tff(76,plain,
% 6.14/6.37 (ord(cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))) | ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))))),
% 6.14/6.37 inference(unit_resolution,[status(thm)],[75, 69, 66])).
% 6.14/6.37 tff(77,plain,
% 6.14/6.37 (ord(merge(nil, cons(s(nil), cons(nil, merge(nil, cons(nil, cons(nil, nil)))))))),
% 6.14/6.37 inference(unit_resolution,[status(thm)],[76, 54])).
% 6.14/6.37 tff(78,plain,
% 6.14/6.37 ($false),
% 6.14/6.37 inference(unit_resolution,[status(thm)],[77, 50])).
% 6.14/6.37 tff(79,plain,(ord(cons(s(nil), cons(nil, cons(nil, cons(nil, nil)))))), inference(lemma,lemma(discharge,[]))).
% 6.14/6.37 tff(80,plain,
% 6.14/6.37 (^[Y: $i, Y2: $i, Xs: $i] : refl((~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs))))) <=> (~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs))))))),
% 6.14/6.37 inference(bind,[status(th)],[])).
% 6.14/6.37 tff(81,plain,
% 6.14/6.37 (![Y: $i, Y2: $i, Xs: $i] : (~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs))))) <=> ![Y: $i, Y2: $i, Xs: $i] : (~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs)))))),
% 6.14/6.37 inference(quant_intro,[status(thm)],[80])).
% 6.14/6.37 tff(82,plain,
% 6.14/6.37 (^[Y: $i, Y2: $i, Xs: $i] : trans(trans(monotonicity(rewrite((leqNat(Y, Y2) & ord(cons(Y2, Xs))) <=> (~((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))))), ((ord(cons(Y, cons(Y2, Xs))) <=> (leqNat(Y, Y2) & ord(cons(Y2, Xs)))) <=> (ord(cons(Y, cons(Y2, Xs))) <=> (~((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))))))), rewrite((ord(cons(Y, cons(Y2, Xs))) <=> (~((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))))) <=> (~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs)))))), ((ord(cons(Y, cons(Y2, Xs))) <=> (leqNat(Y, Y2) & ord(cons(Y2, Xs)))) <=> (~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs))))))), rewrite((~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs))))) <=> (~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs)))))), ((ord(cons(Y, cons(Y2, Xs))) <=> (leqNat(Y, Y2) & ord(cons(Y2, Xs)))) <=> (~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs)))))))),
% 6.14/6.37 inference(bind,[status(th)],[])).
% 6.14/6.37 tff(83,plain,
% 6.14/6.37 (![Y: $i, Y2: $i, Xs: $i] : (ord(cons(Y, cons(Y2, Xs))) <=> (leqNat(Y, Y2) & ord(cons(Y2, Xs)))) <=> ![Y: $i, Y2: $i, Xs: $i] : (~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs)))))),
% 6.14/6.37 inference(quant_intro,[status(thm)],[82])).
% 6.14/6.37 tff(84,plain,
% 6.14/6.37 (![Y: $i, Y2: $i, Xs: $i] : (ord(cons(Y, cons(Y2, Xs))) <=> (leqNat(Y, Y2) & ord(cons(Y2, Xs)))) <=> ![Y: $i, Y2: $i, Xs: $i] : (ord(cons(Y, cons(Y2, Xs))) <=> (leqNat(Y, Y2) & ord(cons(Y2, Xs))))),
% 6.14/6.37 inference(rewrite,[status(thm)],[])).
% 6.14/6.37 tff(85,axiom,(![Y: $i, Y2: $i, Xs: $i] : (ord(cons(Y, cons(Y2, Xs))) <=> (leqNat(Y, Y2) & ord(cons(Y2, Xs))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_015')).
% 6.14/6.37 tff(86,plain,
% 6.14/6.37 (![Y: $i, Y2: $i, Xs: $i] : (ord(cons(Y, cons(Y2, Xs))) <=> (leqNat(Y, Y2) & ord(cons(Y2, Xs))))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[85, 84])).
% 6.14/6.37 tff(87,plain,(
% 6.14/6.37 ![Y: $i, Y2: $i, Xs: $i] : (ord(cons(Y, cons(Y2, Xs))) <=> (leqNat(Y, Y2) & ord(cons(Y2, Xs))))),
% 6.14/6.37 inference(skolemize,[status(sab)],[86])).
% 6.14/6.37 tff(88,plain,
% 6.14/6.37 (![Y: $i, Y2: $i, Xs: $i] : (~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs)))))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[87, 83])).
% 6.14/6.37 tff(89,plain,
% 6.14/6.37 (![Y: $i, Y2: $i, Xs: $i] : (~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs)))))),
% 6.14/6.37 inference(modus_ponens,[status(thm)],[88, 81])).
% 6.14/6.37 tff(90,plain,
% 6.14/6.37 ((~![Y: $i, Y2: $i, Xs: $i] : (~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs)))))) | (~(((~leqNat(s(nil), nil)) | (~ord(cons(nil, cons(nil, cons(nil, nil)))))) <=> ord(cons(s(nil), cons(nil, cons(nil, cons(nil, nil)))))))),
% 6.14/6.37 inference(quant_inst,[status(thm)],[])).
% 6.14/6.38 tff(91,plain,
% 6.14/6.38 (~(((~leqNat(s(nil), nil)) | (~ord(cons(nil, cons(nil, cons(nil, nil)))))) <=> ord(cons(s(nil), cons(nil, cons(nil, cons(nil, nil))))))),
% 6.14/6.38 inference(unit_resolution,[status(thm)],[90, 89])).
% 6.14/6.38 tff(92,plain,
% 6.14/6.38 ((((~leqNat(s(nil), nil)) | (~ord(cons(nil, cons(nil, cons(nil, nil)))))) <=> ord(cons(s(nil), cons(nil, cons(nil, cons(nil, nil)))))) | (~((~leqNat(s(nil), nil)) | (~ord(cons(nil, cons(nil, cons(nil, nil))))))) | (~ord(cons(s(nil), cons(nil, cons(nil, cons(nil, nil))))))),
% 6.14/6.38 inference(tautology,[status(thm)],[])).
% 6.14/6.38 tff(93,plain,
% 6.14/6.38 ((~((~leqNat(s(nil), nil)) | (~ord(cons(nil, cons(nil, cons(nil, nil))))))) | (~ord(cons(s(nil), cons(nil, cons(nil, cons(nil, nil))))))),
% 6.14/6.38 inference(unit_resolution,[status(thm)],[92, 91])).
% 6.14/6.38 tff(94,plain,
% 6.14/6.38 (~((~leqNat(s(nil), nil)) | (~ord(cons(nil, cons(nil, cons(nil, nil))))))),
% 6.14/6.38 inference(unit_resolution,[status(thm)],[93, 79])).
% 6.14/6.38 tff(95,plain,
% 6.14/6.38 (((~leqNat(s(nil), nil)) | (~ord(cons(nil, cons(nil, cons(nil, nil)))))) | leqNat(s(nil), nil)),
% 6.14/6.38 inference(tautology,[status(thm)],[])).
% 6.14/6.38 tff(96,plain,
% 6.14/6.38 (leqNat(s(nil), nil)),
% 6.14/6.38 inference(unit_resolution,[status(thm)],[95, 94])).
% 6.14/6.38 tff(97,plain,
% 6.14/6.38 (^[Z: $i, Xs: $i, Y2: $i, Ys: $i] : refl(((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys))))) <=> ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys))))))),
% 6.14/6.38 inference(bind,[status(th)],[])).
% 6.14/6.38 tff(98,plain,
% 6.14/6.38 (![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys))))) <=> ![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys)))))),
% 6.14/6.38 inference(quant_intro,[status(thm)],[97])).
% 6.14/6.38 tff(99,plain,
% 6.14/6.38 (![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys))))) <=> ![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys)))))),
% 6.14/6.38 inference(rewrite,[status(thm)],[])).
% 6.14/6.38 tff(100,plain,
% 6.14/6.38 (^[Z: $i, Xs: $i, Y2: $i, Ys: $i] : rewrite((leqNat(Z, Y2) => (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys))))) <=> ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys))))))),
% 6.14/6.38 inference(bind,[status(th)],[])).
% 6.14/6.38 tff(101,plain,
% 6.14/6.38 (![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) => (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys))))) <=> ![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys)))))),
% 6.14/6.38 inference(quant_intro,[status(thm)],[100])).
% 6.14/6.38 tff(102,axiom,(![Z: $i, Xs: $i, Y2: $i, Ys: $i] : (leqNat(Z, Y2) => (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_011')).
% 6.14/6.38 tff(103,plain,
% 6.14/6.38 (![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys)))))),
% 6.14/6.38 inference(modus_ponens,[status(thm)],[102, 101])).
% 6.14/6.38 tff(104,plain,
% 6.14/6.38 (![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys)))))),
% 6.14/6.38 inference(modus_ponens,[status(thm)],[103, 99])).
% 6.14/6.38 tff(105,plain,(
% 6.14/6.38 ![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys)))))),
% 6.14/6.38 inference(skolemize,[status(sab)],[104])).
% 6.14/6.38 tff(106,plain,
% 6.14/6.38 (![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys)))))),
% 6.14/6.38 inference(modus_ponens,[status(thm)],[105, 98])).
% 6.14/6.38 tff(107,plain,
% 6.14/6.38 (((~![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys)))))) | ((~leqNat(s(nil), nil)) | (merge(cons(s(nil), nil), cons(nil, nil)) = cons(s(nil), merge(nil, cons(nil, nil)))))) <=> ((~![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys)))))) | (~leqNat(s(nil), nil)) | (merge(cons(s(nil), nil), cons(nil, nil)) = cons(s(nil), merge(nil, cons(nil, nil)))))),
% 6.14/6.38 inference(rewrite,[status(thm)],[])).
% 6.14/6.38 tff(108,plain,
% 6.14/6.38 ((~![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys)))))) | ((~leqNat(s(nil), nil)) | (merge(cons(s(nil), nil), cons(nil, nil)) = cons(s(nil), merge(nil, cons(nil, nil)))))),
% 6.14/6.38 inference(quant_inst,[status(thm)],[])).
% 6.14/6.38 tff(109,plain,
% 6.14/6.38 ((~![Z: $i, Xs: $i, Y2: $i, Ys: $i] : ((~leqNat(Z, Y2)) | (merge(cons(Z, Xs), cons(Y2, Ys)) = cons(Z, merge(Xs, cons(Y2, Ys)))))) | (~leqNat(s(nil), nil)) | (merge(cons(s(nil), nil), cons(nil, nil)) = cons(s(nil), merge(nil, cons(nil, nil))))),
% 6.14/6.38 inference(modus_ponens,[status(thm)],[108, 107])).
% 6.14/6.38 tff(110,plain,
% 6.14/6.38 (merge(cons(s(nil), nil), cons(nil, nil)) = cons(s(nil), merge(nil, cons(nil, nil)))),
% 6.14/6.38 inference(unit_resolution,[status(thm)],[109, 106, 96])).
% 6.14/6.38 tff(111,plain,
% 6.14/6.38 (cons(s(nil), merge(nil, cons(nil, nil))) = merge(cons(s(nil), nil), cons(nil, nil))),
% 6.14/6.38 inference(symmetry,[status(thm)],[110])).
% 6.14/6.38 tff(112,plain,
% 6.14/6.38 ((~![Y: $i] : (merge(nil, Y) = Y)) | (merge(nil, cons(nil, nil)) = cons(nil, nil))),
% 6.14/6.38 inference(quant_inst,[status(thm)],[])).
% 6.14/6.38 tff(113,plain,
% 6.14/6.38 (merge(nil, cons(nil, nil)) = cons(nil, nil)),
% 6.14/6.38 inference(unit_resolution,[status(thm)],[112, 7])).
% 6.14/6.38 tff(114,plain,
% 6.14/6.38 (cons(s(nil), merge(nil, cons(nil, nil))) = cons(s(nil), cons(nil, nil))),
% 6.14/6.38 inference(monotonicity,[status(thm)],[113])).
% 6.14/6.38 tff(115,plain,
% 6.14/6.38 (cons(s(nil), cons(nil, nil)) = cons(s(nil), merge(nil, cons(nil, nil)))),
% 6.14/6.38 inference(symmetry,[status(thm)],[114])).
% 6.14/6.38 tff(116,plain,
% 6.14/6.38 (cons(s(nil), cons(nil, nil)) = merge(cons(s(nil), nil), cons(nil, nil))),
% 6.14/6.38 inference(transitivity,[status(thm)],[115, 111])).
% 6.14/6.38 tff(117,plain,
% 6.14/6.38 (cons(z, cons(s(nil), cons(nil, nil))) = cons(z, merge(cons(s(nil), nil), cons(nil, nil)))),
% 6.14/6.38 inference(monotonicity,[status(thm)],[116])).
% 6.14/6.38 tff(118,plain,
% 6.14/6.38 (cons(z, cons(s(nil), cons(nil, nil))) = merge(cons(s(nil), nil), cons(z, cons(nil, nil)))),
% 6.14/6.38 inference(transitivity,[status(thm)],[117, 36])).
% 6.14/6.38 tff(119,plain,
% 6.14/6.38 (cons(z, cons(z, cons(s(nil), cons(nil, nil)))) = cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))),
% 6.14/6.38 inference(monotonicity,[status(thm)],[118])).
% 6.14/6.38 tff(120,plain,
% 6.14/6.38 (cons(z, merge(cons(s(nil), nil), cons(nil, nil))) = cons(z, cons(s(nil), cons(nil, nil)))),
% 6.14/6.38 inference(symmetry,[status(thm)],[117])).
% 6.14/6.38 tff(121,plain,
% 6.14/6.38 (cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil)))) = cons(z, cons(z, cons(s(nil), cons(nil, nil))))),
% 6.14/6.38 inference(monotonicity,[status(thm)],[120])).
% 6.14/6.38 tff(122,plain,
% 6.14/6.38 (cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil)))) = cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))),
% 6.14/6.38 inference(transitivity,[status(thm)],[121, 119])).
% 6.14/6.38 tff(123,plain,
% 6.14/6.38 (cons(s(nil), cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil))))) = cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))),
% 6.14/6.38 inference(monotonicity,[status(thm)],[122])).
% 6.14/6.38 tff(124,plain,
% 6.14/6.38 (ord(cons(s(nil), cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil)))))) <=> ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))),
% 6.14/6.38 inference(monotonicity,[status(thm)],[123])).
% 6.14/6.38 tff(125,plain,
% 6.14/6.38 ((~ord(cons(s(nil), cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil))))))) <=> (~ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))))),
% 6.14/6.38 inference(monotonicity,[status(thm)],[124])).
% 6.14/6.38 tff(126,plain,
% 6.14/6.38 ((~![Y: $i, Y2: $i, Xs: $i] : (~(((~leqNat(Y, Y2)) | (~ord(cons(Y2, Xs)))) <=> ord(cons(Y, cons(Y2, Xs)))))) | (~(((~leqNat(s(nil), z)) | (~ord(cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil))))))) <=> ord(cons(s(nil), cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil))))))))),
% 6.14/6.38 inference(quant_inst,[status(thm)],[])).
% 6.14/6.38 tff(127,plain,
% 6.14/6.38 (~(((~leqNat(s(nil), z)) | (~ord(cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil))))))) <=> ord(cons(s(nil), cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil)))))))),
% 6.14/6.38 inference(unit_resolution,[status(thm)],[126, 89])).
% 6.14/6.38 tff(128,plain,
% 6.14/6.38 (((~leqNat(s(nil), z)) | (~ord(cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil))))))) | leqNat(s(nil), z)),
% 6.14/6.38 inference(tautology,[status(thm)],[])).
% 6.14/6.38 tff(129,plain,
% 6.14/6.38 ((~leqNat(s(nil), z)) | (~ord(cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil))))))),
% 6.14/6.38 inference(unit_resolution,[status(thm)],[128, 21])).
% 6.14/6.38 tff(130,plain,
% 6.14/6.38 ((((~leqNat(s(nil), z)) | (~ord(cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil))))))) <=> ord(cons(s(nil), cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil))))))) | (~((~leqNat(s(nil), z)) | (~ord(cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil)))))))) | (~ord(cons(s(nil), cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil)))))))),
% 6.14/6.38 inference(tautology,[status(thm)],[])).
% 6.14/6.38 tff(131,plain,
% 6.14/6.38 ((((~leqNat(s(nil), z)) | (~ord(cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil))))))) <=> ord(cons(s(nil), cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil))))))) | (~ord(cons(s(nil), cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil)))))))),
% 6.14/6.38 inference(unit_resolution,[status(thm)],[130, 129])).
% 6.14/6.38 tff(132,plain,
% 6.14/6.38 (~ord(cons(s(nil), cons(z, cons(z, merge(cons(s(nil), nil), cons(nil, nil))))))),
% 6.14/6.38 inference(unit_resolution,[status(thm)],[131, 127])).
% 6.14/6.38 tff(133,plain,
% 6.14/6.38 (~ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))),
% 6.14/6.38 inference(modus_ponens,[status(thm)],[132, 125])).
% 6.14/6.38 tff(134,plain,
% 6.14/6.38 (~ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))))),
% 6.14/6.38 inference(modus_ponens,[status(thm)],[133, 12])).
% 6.14/6.38 tff(135,plain,
% 6.14/6.38 (((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | ((~ord(nil)) | ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))) | ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))))) <=> ((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | (~ord(nil)) | ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))) | ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))))),
% 6.14/6.38 inference(rewrite,[status(thm)],[])).
% 6.14/6.38 tff(136,plain,
% 6.14/6.38 ((ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))) | ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))) | (~ord(nil))) <=> ((~ord(nil)) | ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))) | ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))))),
% 6.14/6.38 inference(rewrite,[status(thm)],[])).
% 6.14/6.38 tff(137,plain,
% 6.14/6.38 (((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | (ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))) | ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))) | (~ord(nil)))) <=> ((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | ((~ord(nil)) | ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))) | ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))))))),
% 6.14/6.38 inference(monotonicity,[status(thm)],[136])).
% 6.14/6.38 tff(138,plain,
% 6.14/6.38 (((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | (ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))) | ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))) | (~ord(nil)))) <=> ((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | (~ord(nil)) | ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))) | ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))))),
% 6.14/6.38 inference(transitivity,[status(thm)],[137, 135])).
% 6.14/6.38 tff(139,plain,
% 6.14/6.38 ((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | (ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil))))))) | ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))) | (~ord(nil)))),
% 6.14/6.38 inference(quant_inst,[status(thm)],[])).
% 6.14/6.38 tff(140,plain,
% 6.14/6.38 ((~![Xs: $i, Ys: $i] : (ord(merge(Xs, Ys)) | ord(Ys) | (~ord(Xs)))) | (~ord(nil)) | ord(cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))) | ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))))),
% 6.14/6.38 inference(modus_ponens,[status(thm)],[139, 138])).
% 6.14/6.38 tff(141,plain,
% 6.14/6.38 (ord(merge(nil, cons(s(nil), cons(z, merge(cons(s(nil), nil), cons(z, cons(nil, nil)))))))),
% 6.14/6.38 inference(unit_resolution,[status(thm)],[140, 69, 66, 133])).
% 6.14/6.38 tff(142,plain,
% 6.14/6.38 ($false),
% 6.14/6.38 inference(unit_resolution,[status(thm)],[141, 134])).
% 6.14/6.38 % SZS output end Proof
% 6.14/6.39 % E exiting
%------------------------------------------------------------------------------