%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWX203-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.ZwIQuyAXTh true
% Computer : n023.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:49 PM UTC 2026
% Result : Unsatisfiable 216.43s 31.59s
% Output : Refutation 216.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX203-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.ZwIQuyAXTh true
% 0.18/0.35 % Computer : n023.cluster.edu
% 0.18/0.35 % Model : x86_64 x86_64
% 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.35 % Memory : 8042.1875MB
% 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.35 % CPULimit : 300
% 0.18/0.35 % WCLimit : 300
% 0.18/0.35 % DateTime : Tue May 5 11:28:38 EDT 2026
% 0.18/0.35 % CPUTime :
% 0.18/0.35 % Running portfolio for 300 s
% 0.18/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.35 % Number of cores: 8
% 0.18/0.35 % Python version: Python 3.6.8
% 0.21/0.36 % Running in FO mode
% 0.55/0.63 % Total configuration time : 435
% 0.55/0.63 % Estimated wc time : 1092
% 0.55/0.63 % Estimated cpu time (7 cpus) : 156.0
% 0.55/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.55/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.55/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.55/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.55/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.55/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.55/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.55/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 216.43/31.59 % Solved by fo/fo5.sh.
% 216.43/31.59 % done 6219 iterations in 30.806s
% 216.43/31.59 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 216.43/31.59 % SZS output start Refutation
% 216.43/31.59 thf(orb_type, type, orb: $i > $i > $i).
% 216.43/31.59 thf(aux_type, type, aux: $i > $i > $i > $i).
% 216.43/31.59 thf(psorted_rev_type, type, psorted_rev: $i > $i).
% 216.43/31.59 thf(rev_type, type, rev: $i > $i).
% 216.43/31.59 thf(impl_type, type, impl: $i > $i > $i).
% 216.43/31.59 thf(eq_type, type, eq: $i > $i > $i).
% 216.43/31.59 thf(sorted_type, type, sorted: $i > $i).
% 216.43/31.59 thf(lengthNat_type, type, lengthNat: $i > $i).
% 216.43/31.59 thf(z_type, type, z: $i).
% 216.43/31.59 thf(andb_type, type, andb: $i > $i > $i).
% 216.43/31.59 thf(unique_type, type, unique: $i > $i).
% 216.43/31.59 thf(cons_type, type, cons: $i > $i > $i).
% 216.43/31.59 thf(append_type, type, append: $i > $i > $i).
% 216.43/31.59 thf(eq2_type, type, eq2: $i > $i > $i).
% 216.43/31.59 thf(nil_type, type, nil: $i).
% 216.43/31.59 thf(elemNat_type, type, elemNat: $i > $i > $i).
% 216.43/31.59 thf(btrue_type, type, btrue: $i).
% 216.43/31.59 thf(s_type, type, s: $i > $i).
% 216.43/31.59 thf(bfalse_type, type, bfalse: $i).
% 216.43/31.59 thf(leqNat_type, type, leqNat: $i > $i > $i).
% 216.43/31.59 thf(axiom_029, axiom, (( eq @ ( s @ X ) @ z ) = ( bfalse ))).
% 216.43/31.59 thf(zip_derived_cl29, plain, (![X0 : $i]: ((eq @ (s @ X0) @ z) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_029])).
% 216.43/31.59 thf(axiom_011, axiom, (( elemNat @ X @ nil ) = ( bfalse ))).
% 216.43/31.59 thf(zip_derived_cl11, plain, (![X0 : $i]: ((elemNat @ X0 @ nil) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_011])).
% 216.43/31.59 thf(axiom_027, axiom, (( eq @ ( s @ X ) @ ( s @ Y ) ) = ( eq @ X @ Y ))).
% 216.43/31.59 thf(zip_derived_cl27, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]: ((eq @ (s @ X0) @ (s @ X1)) = (eq @ X0 @ X1))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_027])).
% 216.43/31.59 thf(zip_derived_cl27, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]: ((eq @ (s @ X0) @ (s @ X1)) = (eq @ X0 @ X1))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_027])).
% 216.43/31.59 thf(axiom_012, axiom,
% 216.43/31.59 (( elemNat @ X @ ( cons @ Z @ Xs ) ) =
% 216.43/31.59 ( orb @ ( eq @ X @ Z ) @ ( elemNat @ X @ Xs ) ))).
% 216.43/31.59 thf(zip_derived_cl12, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ X0 @ (cons @ X1 @ X2))
% 216.43/31.59 = (orb @ (eq @ X0 @ X1) @ (elemNat @ X0 @ X2)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_012])).
% 216.43/31.59 thf(zip_derived_cl64, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ (s @ X1) @ (cons @ (s @ X0) @ X2))
% 216.43/31.59 = (orb @ (eq @ X1 @ X0) @ (elemNat @ (s @ X1) @ X2)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl27, zip_derived_cl12])).
% 216.43/31.59 thf(zip_derived_cl323, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ X1)) @ (cons @ (s @ (s @ X0)) @ X2))
% 216.43/31.59 = (orb @ (eq @ X1 @ X0) @ (elemNat @ (s @ (s @ X1)) @ X2)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl27, zip_derived_cl64])).
% 216.43/31.59 thf(zip_derived_cl2105, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ X0)) @ (cons @ (s @ (s @ X1)) @ nil))
% 216.43/31.59 = (orb @ (eq @ X0 @ X1) @ bfalse))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl11, zip_derived_cl323])).
% 216.43/31.59 thf(zip_derived_cl323, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ X1)) @ (cons @ (s @ (s @ X0)) @ X2))
% 216.43/31.59 = (orb @ (eq @ X1 @ X0) @ (elemNat @ (s @ (s @ X1)) @ X2)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl27, zip_derived_cl64])).
% 216.43/31.59 thf(zip_derived_cl2172, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ X1)) @
% 216.43/31.59 (cons @ (s @ (s @ X2)) @ (cons @ (s @ (s @ X0)) @ nil)))
% 216.43/31.59 = (orb @ (eq @ X1 @ X2) @ (orb @ (eq @ X1 @ X0) @ bfalse)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl2105, zip_derived_cl323])).
% 216.43/31.59 thf(zip_derived_cl73116, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ (s @ X0))) @
% 216.43/31.59 (cons @ (s @ (s @ X1)) @ (cons @ (s @ (s @ z)) @ nil)))
% 216.43/31.59 = (orb @ (eq @ (s @ X0) @ X1) @ (orb @ bfalse @ bfalse)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl29, zip_derived_cl2172])).
% 216.43/31.59 thf(axiom_003, axiom, (( orb @ bfalse @ Q ) = ( Q ))).
% 216.43/31.59 thf(zip_derived_cl3, plain, (![X0 : $i]: ((orb @ bfalse @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_003])).
% 216.43/31.59 thf(zip_derived_cl73134, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ (s @ X0))) @
% 216.43/31.59 (cons @ (s @ (s @ X1)) @ (cons @ (s @ (s @ z)) @ nil)))
% 216.43/31.59 = (orb @ (eq @ (s @ X0) @ X1) @ bfalse))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl73116, zip_derived_cl3])).
% 216.43/31.59 thf(zip_derived_cl29, plain, (![X0 : $i]: ((eq @ (s @ X0) @ z) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_029])).
% 216.43/31.59 thf(zip_derived_cl323, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ X1)) @ (cons @ (s @ (s @ X0)) @ X2))
% 216.43/31.59 = (orb @ (eq @ X1 @ X0) @ (elemNat @ (s @ (s @ X1)) @ X2)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl27, zip_derived_cl64])).
% 216.43/31.59 thf(zip_derived_cl2127, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ (s @ X1))) @ (cons @ (s @ (s @ z)) @ X0))
% 216.43/31.59 = (orb @ bfalse @ (elemNat @ (s @ (s @ (s @ X1))) @ X0)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl29, zip_derived_cl323])).
% 216.43/31.59 thf(zip_derived_cl3, plain, (![X0 : $i]: ((orb @ bfalse @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_003])).
% 216.43/31.59 thf(zip_derived_cl2135, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ (s @ X1))) @ (cons @ (s @ (s @ z)) @ X0))
% 216.43/31.59 = (elemNat @ (s @ (s @ (s @ X1))) @ X0))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl2127, zip_derived_cl3])).
% 216.43/31.59 thf(zip_derived_cl73253, plain,
% 216.43/31.59 (![X0 : $i]:
% 216.43/31.59 ((orb @ (eq @ (s @ X0) @ z) @ bfalse)
% 216.43/31.59 = (elemNat @ (s @ (s @ (s @ X0))) @ (cons @ (s @ (s @ z)) @ nil)))),
% 216.43/31.59 inference('sup+', [status(thm)],
% 216.43/31.59 [zip_derived_cl73134, zip_derived_cl2135])).
% 216.43/31.59 thf(zip_derived_cl29, plain, (![X0 : $i]: ((eq @ (s @ X0) @ z) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_029])).
% 216.43/31.59 thf(zip_derived_cl3, plain, (![X0 : $i]: ((orb @ bfalse @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_003])).
% 216.43/31.59 thf(zip_derived_cl73287, plain,
% 216.43/31.59 (![X0 : $i]:
% 216.43/31.59 ((bfalse)
% 216.43/31.59 = (elemNat @ (s @ (s @ (s @ X0))) @ (cons @ (s @ (s @ z)) @ nil)))),
% 216.43/31.59 inference('demod', [status(thm)],
% 216.43/31.59 [zip_derived_cl73253, zip_derived_cl29, zip_derived_cl3])).
% 216.43/31.59 thf(zip_derived_cl29, plain, (![X0 : $i]: ((eq @ (s @ X0) @ z) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_029])).
% 216.43/31.59 thf(zip_derived_cl29, plain, (![X0 : $i]: ((eq @ (s @ X0) @ z) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_029])).
% 216.43/31.59 thf(zip_derived_cl12, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ X0 @ (cons @ X1 @ X2))
% 216.43/31.59 = (orb @ (eq @ X0 @ X1) @ (elemNat @ X0 @ X2)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_012])).
% 216.43/31.59 thf(zip_derived_cl63, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ X1) @ (cons @ z @ X0))
% 216.43/31.59 = (orb @ bfalse @ (elemNat @ (s @ X1) @ X0)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl29, zip_derived_cl12])).
% 216.43/31.59 thf(zip_derived_cl3, plain, (![X0 : $i]: ((orb @ bfalse @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_003])).
% 216.43/31.59 thf(zip_derived_cl67, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ X1) @ (cons @ z @ X0)) = (elemNat @ (s @ X1) @ X0))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl63, zip_derived_cl3])).
% 216.43/31.59 thf(zip_derived_cl64, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ (s @ X1) @ (cons @ (s @ X0) @ X2))
% 216.43/31.59 = (orb @ (eq @ X1 @ X0) @ (elemNat @ (s @ X1) @ X2)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl27, zip_derived_cl12])).
% 216.43/31.59 thf(zip_derived_cl316, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ (s @ X1) @ (cons @ (s @ X2) @ (cons @ z @ X0)))
% 216.43/31.59 = (orb @ (eq @ X1 @ X2) @ (elemNat @ (s @ X1) @ X0)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl67, zip_derived_cl64])).
% 216.43/31.59 thf(zip_derived_cl952, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ X1)) @ (cons @ (s @ z) @ (cons @ z @ X0)))
% 216.43/31.59 = (orb @ bfalse @ (elemNat @ (s @ (s @ X1)) @ X0)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl29, zip_derived_cl316])).
% 216.43/31.59 thf(zip_derived_cl3, plain, (![X0 : $i]: ((orb @ bfalse @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_003])).
% 216.43/31.59 thf(zip_derived_cl958, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ X1)) @ (cons @ (s @ z) @ (cons @ z @ X0)))
% 216.43/31.59 = (elemNat @ (s @ (s @ X1)) @ X0))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl952, zip_derived_cl3])).
% 216.43/31.59 thf(zip_derived_cl12, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ X0 @ (cons @ X1 @ X2))
% 216.43/31.59 = (orb @ (eq @ X0 @ X1) @ (elemNat @ X0 @ X2)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_012])).
% 216.43/31.59 thf(axiom_014, axiom,
% 216.43/31.59 (( unique @ ( cons @ Y @ Xs ) ) = ( aux @ Y @ Xs @ ( elemNat @ Y @ Xs ) ))).
% 216.43/31.59 thf(zip_derived_cl14, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((unique @ (cons @ X0 @ X1)) = (aux @ X0 @ X1 @ (elemNat @ X0 @ X1)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_014])).
% 216.43/31.59 thf(zip_derived_cl57, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((unique @ (cons @ X1 @ (cons @ X2 @ X0)))
% 216.43/31.59 = (aux @ X1 @ (cons @ X2 @ X0) @
% 216.43/31.59 (orb @ (eq @ X1 @ X2) @ (elemNat @ X1 @ X0))))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl12, zip_derived_cl14])).
% 216.43/31.59 thf(zip_derived_cl1060, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((unique @
% 216.43/31.59 (cons @ (s @ (s @ X1)) @
% 216.43/31.59 (cons @ X2 @ (cons @ (s @ z) @ (cons @ z @ X0)))))
% 216.43/31.59 = (aux @ (s @ (s @ X1)) @
% 216.43/31.59 (cons @ X2 @ (cons @ (s @ z) @ (cons @ z @ X0))) @
% 216.43/31.59 (orb @ (eq @ (s @ (s @ X1)) @ X2) @
% 216.43/31.59 (elemNat @ (s @ (s @ X1)) @ X0))))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl958, zip_derived_cl57])).
% 216.43/31.59 thf(zip_derived_cl12, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ X0 @ (cons @ X1 @ X2))
% 216.43/31.59 = (orb @ (eq @ X0 @ X1) @ (elemNat @ X0 @ X2)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_012])).
% 216.43/31.59 thf(zip_derived_cl1074, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((unique @
% 216.43/31.59 (cons @ (s @ (s @ X1)) @
% 216.43/31.59 (cons @ X2 @ (cons @ (s @ z) @ (cons @ z @ X0)))))
% 216.43/31.59 = (aux @ (s @ (s @ X1)) @
% 216.43/31.59 (cons @ X2 @ (cons @ (s @ z) @ (cons @ z @ X0))) @
% 216.43/31.59 (elemNat @ (s @ (s @ X1)) @ (cons @ X2 @ X0))))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl1060, zip_derived_cl12])).
% 216.43/31.59 thf(zip_derived_cl73364, plain,
% 216.43/31.59 (![X0 : $i]:
% 216.43/31.59 ((unique @
% 216.43/31.59 (cons @ (s @ (s @ (s @ X0))) @
% 216.43/31.59 (cons @ (s @ (s @ z)) @ (cons @ (s @ z) @ (cons @ z @ nil)))))
% 216.43/31.59 = (aux @ (s @ (s @ (s @ X0))) @
% 216.43/31.59 (cons @ (s @ (s @ z)) @ (cons @ (s @ z) @ (cons @ z @ nil))) @
% 216.43/31.59 bfalse))),
% 216.43/31.59 inference('sup+', [status(thm)],
% 216.43/31.59 [zip_derived_cl73287, zip_derived_cl1074])).
% 216.43/31.59 thf(axiom_001, axiom, (( aux @ Y @ Xs @ bfalse ) = ( unique @ Xs ))).
% 216.43/31.59 thf(zip_derived_cl1, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]: ((aux @ X1 @ X0 @ bfalse) = (unique @ X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_001])).
% 216.43/31.59 thf(zip_derived_cl11, plain, (![X0 : $i]: ((elemNat @ X0 @ nil) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_011])).
% 216.43/31.59 thf(zip_derived_cl67, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ X1) @ (cons @ z @ X0)) = (elemNat @ (s @ X1) @ X0))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl63, zip_derived_cl3])).
% 216.43/31.59 thf(zip_derived_cl316, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ (s @ X1) @ (cons @ (s @ X2) @ (cons @ z @ X0)))
% 216.43/31.59 = (orb @ (eq @ X1 @ X2) @ (elemNat @ (s @ X1) @ X0)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl67, zip_derived_cl64])).
% 216.43/31.59 thf(zip_derived_cl942, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ (s @ X1) @
% 216.43/31.59 (cons @ (s @ X2) @ (cons @ z @ (cons @ z @ X0))))
% 216.43/31.59 = (orb @ (eq @ X1 @ X2) @ (elemNat @ (s @ X1) @ X0)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl67, zip_derived_cl316])).
% 216.43/31.59 thf(zip_derived_cl5027, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ X0) @
% 216.43/31.59 (cons @ (s @ X1) @ (cons @ z @ (cons @ z @ nil))))
% 216.43/31.59 = (orb @ (eq @ X0 @ X1) @ bfalse))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl11, zip_derived_cl942])).
% 216.43/31.59 thf(zip_derived_cl29, plain, (![X0 : $i]: ((eq @ (s @ X0) @ z) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_029])).
% 216.43/31.59 thf(zip_derived_cl64, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ (s @ X1) @ (cons @ (s @ X0) @ X2))
% 216.43/31.59 = (orb @ (eq @ X1 @ X0) @ (elemNat @ (s @ X1) @ X2)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl27, zip_derived_cl12])).
% 216.43/31.59 thf(zip_derived_cl322, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ X1)) @ (cons @ (s @ z) @ X0))
% 216.43/31.59 = (orb @ bfalse @ (elemNat @ (s @ (s @ X1)) @ X0)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl29, zip_derived_cl64])).
% 216.43/31.59 thf(zip_derived_cl3, plain, (![X0 : $i]: ((orb @ bfalse @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_003])).
% 216.43/31.59 thf(zip_derived_cl329, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ X1)) @ (cons @ (s @ z) @ X0))
% 216.43/31.59 = (elemNat @ (s @ (s @ X1)) @ X0))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl322, zip_derived_cl3])).
% 216.43/31.59 thf(zip_derived_cl5145, plain,
% 216.43/31.59 (![X0 : $i]:
% 216.43/31.59 ((orb @ (eq @ (s @ X0) @ z) @ bfalse)
% 216.43/31.59 = (elemNat @ (s @ (s @ X0)) @ (cons @ z @ (cons @ z @ nil))))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl5027, zip_derived_cl329])).
% 216.43/31.59 thf(zip_derived_cl29, plain, (![X0 : $i]: ((eq @ (s @ X0) @ z) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_029])).
% 216.43/31.59 thf(zip_derived_cl3, plain, (![X0 : $i]: ((orb @ bfalse @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_003])).
% 216.43/31.59 thf(zip_derived_cl5159, plain,
% 216.43/31.59 (![X0 : $i]:
% 216.43/31.59 ((bfalse) = (elemNat @ (s @ (s @ X0)) @ (cons @ z @ (cons @ z @ nil))))),
% 216.43/31.59 inference('demod', [status(thm)],
% 216.43/31.59 [zip_derived_cl5145, zip_derived_cl29, zip_derived_cl3])).
% 216.43/31.59 thf(zip_derived_cl67, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ X1) @ (cons @ z @ X0)) = (elemNat @ (s @ X1) @ X0))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl63, zip_derived_cl3])).
% 216.43/31.59 thf(zip_derived_cl5242, plain,
% 216.43/31.59 (![X0 : $i]: ((bfalse) = (elemNat @ (s @ (s @ X0)) @ (cons @ z @ nil)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl5159, zip_derived_cl67])).
% 216.43/31.59 thf(zip_derived_cl329, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ (s @ (s @ X1)) @ (cons @ (s @ z) @ X0))
% 216.43/31.59 = (elemNat @ (s @ (s @ X1)) @ X0))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl322, zip_derived_cl3])).
% 216.43/31.59 thf(zip_derived_cl14, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((unique @ (cons @ X0 @ X1)) = (aux @ X0 @ X1 @ (elemNat @ X0 @ X1)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_014])).
% 216.43/31.59 thf(zip_derived_cl344, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((unique @ (cons @ (s @ (s @ X1)) @ (cons @ (s @ z) @ X0)))
% 216.43/31.59 = (aux @ (s @ (s @ X1)) @ (cons @ (s @ z) @ X0) @
% 216.43/31.59 (elemNat @ (s @ (s @ X1)) @ X0)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl329, zip_derived_cl14])).
% 216.43/31.59 thf(zip_derived_cl6963, plain,
% 216.43/31.59 (![X0 : $i]:
% 216.43/31.59 ((unique @
% 216.43/31.59 (cons @ (s @ (s @ X0)) @ (cons @ (s @ z) @ (cons @ z @ nil))))
% 216.43/31.59 = (aux @ (s @ (s @ X0)) @ (cons @ (s @ z) @ (cons @ z @ nil)) @
% 216.43/31.59 bfalse))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl5242, zip_derived_cl344])).
% 216.43/31.59 thf(zip_derived_cl1, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]: ((aux @ X1 @ X0 @ bfalse) = (unique @ X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_001])).
% 216.43/31.59 thf(zip_derived_cl29, plain, (![X0 : $i]: ((eq @ (s @ X0) @ z) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_029])).
% 216.43/31.59 thf(zip_derived_cl11, plain, (![X0 : $i]: ((elemNat @ X0 @ nil) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_011])).
% 216.43/31.59 thf(zip_derived_cl12, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((elemNat @ X0 @ (cons @ X1 @ X2))
% 216.43/31.59 = (orb @ (eq @ X0 @ X1) @ (elemNat @ X0 @ X2)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_012])).
% 216.43/31.59 thf(zip_derived_cl59, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((elemNat @ X0 @ (cons @ X1 @ nil)) = (orb @ (eq @ X0 @ X1) @ bfalse))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl11, zip_derived_cl12])).
% 216.43/31.59 thf(zip_derived_cl14, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((unique @ (cons @ X0 @ X1)) = (aux @ X0 @ X1 @ (elemNat @ X0 @ X1)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_014])).
% 216.43/31.59 thf(zip_derived_cl176, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((unique @ (cons @ X1 @ (cons @ X0 @ nil)))
% 216.43/31.59 = (aux @ X1 @ (cons @ X0 @ nil) @ (orb @ (eq @ X1 @ X0) @ bfalse)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl59, zip_derived_cl14])).
% 216.43/31.59 thf(zip_derived_cl658, plain,
% 216.43/31.59 (![X0 : $i]:
% 216.43/31.59 ((unique @ (cons @ (s @ X0) @ (cons @ z @ nil)))
% 216.43/31.59 = (aux @ (s @ X0) @ (cons @ z @ nil) @ (orb @ bfalse @ bfalse)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl29, zip_derived_cl176])).
% 216.43/31.59 thf(zip_derived_cl3, plain, (![X0 : $i]: ((orb @ bfalse @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_003])).
% 216.43/31.59 thf(zip_derived_cl1, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]: ((aux @ X1 @ X0 @ bfalse) = (unique @ X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_001])).
% 216.43/31.59 thf(zip_derived_cl11, plain, (![X0 : $i]: ((elemNat @ X0 @ nil) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_011])).
% 216.43/31.59 thf(zip_derived_cl14, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((unique @ (cons @ X0 @ X1)) = (aux @ X0 @ X1 @ (elemNat @ X0 @ X1)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_014])).
% 216.43/31.59 thf(zip_derived_cl52, plain,
% 216.43/31.59 (![X0 : $i]: ((unique @ (cons @ X0 @ nil)) = (aux @ X0 @ nil @ bfalse))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl11, zip_derived_cl14])).
% 216.43/31.59 thf(zip_derived_cl1, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]: ((aux @ X1 @ X0 @ bfalse) = (unique @ X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_001])).
% 216.43/31.59 thf(axiom_013, axiom, (( unique @ nil ) = ( btrue ))).
% 216.43/31.59 thf(zip_derived_cl13, plain, (((unique @ nil) = (btrue))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_013])).
% 216.43/31.59 thf(zip_derived_cl53, plain,
% 216.43/31.59 (![X0 : $i]: ((unique @ (cons @ X0 @ nil)) = (btrue))),
% 216.43/31.59 inference('demod', [status(thm)],
% 216.43/31.59 [zip_derived_cl52, zip_derived_cl1, zip_derived_cl13])).
% 216.43/31.59 thf(zip_derived_cl665, plain,
% 216.43/31.59 (![X0 : $i]: ((unique @ (cons @ (s @ X0) @ (cons @ z @ nil))) = (btrue))),
% 216.43/31.59 inference('demod', [status(thm)],
% 216.43/31.59 [zip_derived_cl658, zip_derived_cl3, zip_derived_cl1,
% 216.43/31.59 zip_derived_cl53])).
% 216.43/31.59 thf(zip_derived_cl6977, plain,
% 216.43/31.59 (![X0 : $i]:
% 216.43/31.59 ((unique @
% 216.43/31.59 (cons @ (s @ (s @ X0)) @ (cons @ (s @ z) @ (cons @ z @ nil))))
% 216.43/31.59 = (btrue))),
% 216.43/31.59 inference('demod', [status(thm)],
% 216.43/31.59 [zip_derived_cl6963, zip_derived_cl1, zip_derived_cl665])).
% 216.43/31.59 thf(zip_derived_cl73415, plain,
% 216.43/31.59 (![X0 : $i]:
% 216.43/31.59 ((unique @
% 216.43/31.59 (cons @ (s @ (s @ (s @ X0))) @
% 216.43/31.59 (cons @ (s @ (s @ z)) @ (cons @ (s @ z) @ (cons @ z @ nil)))))
% 216.43/31.59 = (btrue))),
% 216.43/31.59 inference('demod', [status(thm)],
% 216.43/31.59 [zip_derived_cl73364, zip_derived_cl1, zip_derived_cl6977])).
% 216.43/31.59 thf(axiom_024, axiom,
% 216.43/31.59 (( psorted_rev @ X ) =
% 216.43/31.59 ( impl @
% 216.43/31.59 ( eq2 @ ( sorted @ ( rev @ X ) ) @ btrue ) @
% 216.43/31.59 ( impl @
% 216.43/31.59 ( eq2 @ ( unique @ X ) @ btrue ) @
% 216.43/31.59 ( eq2 @
% 216.43/31.59 ( leqNat @ ( lengthNat @ X ) @ ( s @ ( s @ ( s @ z ) ) ) ) @ btrue ) ) ))).
% 216.43/31.59 thf(zip_derived_cl24, plain,
% 216.43/31.59 (![X0 : $i]:
% 216.43/31.59 ((psorted_rev @ X0)
% 216.43/31.59 = (impl @ (eq2 @ (sorted @ (rev @ X0)) @ btrue) @
% 216.43/31.59 (impl @ (eq2 @ (unique @ X0) @ btrue) @
% 216.43/31.59 (eq2 @ (leqNat @ (lengthNat @ X0) @ (s @ (s @ (s @ z)))) @ btrue))))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_024])).
% 216.43/31.59 thf(zip_derived_cl73851, plain,
% 216.43/31.59 (![X0 : $i]:
% 216.43/31.59 ((psorted_rev @
% 216.43/31.59 (cons @ (s @ (s @ (s @ X0))) @
% 216.43/31.59 (cons @ (s @ (s @ z)) @ (cons @ (s @ z) @ (cons @ z @ nil)))))
% 216.43/31.59 = (impl @
% 216.43/31.59 (eq2 @
% 216.43/31.59 (sorted @
% 216.43/31.59 (rev @
% 216.43/31.59 (cons @ (s @ (s @ (s @ X0))) @
% 216.43/31.59 (cons @ (s @ (s @ z)) @ (cons @ (s @ z) @ (cons @ z @ nil)))))) @
% 216.43/31.59 btrue) @
% 216.43/31.59 (impl @ (eq2 @ btrue @ btrue) @
% 216.43/31.59 (eq2 @
% 216.43/31.59 (leqNat @
% 216.43/31.59 (lengthNat @
% 216.43/31.59 (cons @ (s @ (s @ (s @ X0))) @
% 216.43/31.59 (cons @ (s @ (s @ z)) @ (cons @ (s @ z) @ (cons @ z @ nil))))) @
% 216.43/31.59 (s @ (s @ (s @ z)))) @
% 216.43/31.59 btrue))))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl73415, zip_derived_cl24])).
% 216.43/31.59 thf(axiom_017, axiom, (( rev @ nil ) = ( nil ))).
% 216.43/31.59 thf(zip_derived_cl17, plain, (((rev @ nil) = (nil))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_017])).
% 216.43/31.59 thf(axiom_018, axiom,
% 216.43/31.59 (( rev @ ( cons @ Y @ Xs ) ) =
% 216.43/31.59 ( append @ ( rev @ Xs ) @ ( cons @ Y @ nil ) ))).
% 216.43/31.59 thf(zip_derived_cl18, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((rev @ (cons @ X1 @ X0)) = (append @ (rev @ X0) @ (cons @ X1 @ nil)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_018])).
% 216.43/31.59 thf(zip_derived_cl54, plain,
% 216.43/31.59 (![X0 : $i]:
% 216.43/31.59 ((rev @ (cons @ X0 @ nil)) = (append @ nil @ (cons @ X0 @ nil)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl17, zip_derived_cl18])).
% 216.43/31.59 thf(axiom_015, axiom, (( append @ nil @ Y ) = ( Y ))).
% 216.43/31.59 thf(zip_derived_cl15, plain, (![X0 : $i]: ((append @ nil @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_015])).
% 216.43/31.59 thf(zip_derived_cl55, plain,
% 216.43/31.59 (![X0 : $i]: ((rev @ (cons @ X0 @ nil)) = (cons @ X0 @ nil))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl54, zip_derived_cl15])).
% 216.43/31.59 thf(zip_derived_cl18, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((rev @ (cons @ X1 @ X0)) = (append @ (rev @ X0) @ (cons @ X1 @ nil)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_018])).
% 216.43/31.59 thf(zip_derived_cl128, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((rev @ (cons @ X1 @ (cons @ X0 @ nil)))
% 216.43/31.59 = (append @ (cons @ X0 @ nil) @ (cons @ X1 @ nil)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl55, zip_derived_cl18])).
% 216.43/31.59 thf(axiom_016, axiom,
% 216.43/31.59 (( append @ ( cons @ Z @ Xs ) @ Y ) = ( cons @ Z @ ( append @ Xs @ Y ) ))).
% 216.43/31.59 thf(zip_derived_cl16, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((append @ (cons @ X0 @ X1) @ X2) = (cons @ X0 @ (append @ X1 @ X2)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_016])).
% 216.43/31.59 thf(zip_derived_cl242, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((rev @ (cons @ X1 @ (cons @ X0 @ nil)))
% 216.43/31.59 = (cons @ X0 @ (append @ nil @ (cons @ X1 @ nil))))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl128, zip_derived_cl16])).
% 216.43/31.59 thf(zip_derived_cl15, plain, (![X0 : $i]: ((append @ nil @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_015])).
% 216.43/31.59 thf(zip_derived_cl243, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((rev @ (cons @ X1 @ (cons @ X0 @ nil)))
% 216.43/31.59 = (cons @ X0 @ (cons @ X1 @ nil)))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl242, zip_derived_cl15])).
% 216.43/31.59 thf(zip_derived_cl18, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((rev @ (cons @ X1 @ X0)) = (append @ (rev @ X0) @ (cons @ X1 @ nil)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_018])).
% 216.43/31.59 thf(zip_derived_cl245, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((rev @ (cons @ X2 @ (cons @ X0 @ (cons @ X1 @ nil))))
% 216.43/31.59 = (append @ (cons @ X1 @ (cons @ X0 @ nil)) @ (cons @ X2 @ nil)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl243, zip_derived_cl18])).
% 216.43/31.59 thf(zip_derived_cl16, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((append @ (cons @ X0 @ X1) @ X2) = (cons @ X0 @ (append @ X1 @ X2)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_016])).
% 216.43/31.59 thf(zip_derived_cl757, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((rev @ (cons @ X2 @ (cons @ X1 @ (cons @ X0 @ nil))))
% 216.43/31.59 = (cons @ X0 @ (append @ (cons @ X1 @ nil) @ (cons @ X2 @ nil))))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl245, zip_derived_cl16])).
% 216.43/31.59 thf(zip_derived_cl128, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((rev @ (cons @ X1 @ (cons @ X0 @ nil)))
% 216.43/31.59 = (append @ (cons @ X0 @ nil) @ (cons @ X1 @ nil)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl55, zip_derived_cl18])).
% 216.43/31.59 thf(zip_derived_cl243, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((rev @ (cons @ X1 @ (cons @ X0 @ nil)))
% 216.43/31.59 = (cons @ X0 @ (cons @ X1 @ nil)))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl242, zip_derived_cl15])).
% 216.43/31.59 thf(zip_derived_cl244, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((cons @ X0 @ (cons @ X1 @ nil))
% 216.43/31.59 = (append @ (cons @ X0 @ nil) @ (cons @ X1 @ nil)))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl128, zip_derived_cl243])).
% 216.43/31.59 thf(zip_derived_cl758, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((rev @ (cons @ X2 @ (cons @ X1 @ (cons @ X0 @ nil))))
% 216.43/31.59 = (cons @ X0 @ (cons @ X1 @ (cons @ X2 @ nil))))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl757, zip_derived_cl244])).
% 216.43/31.59 thf(zip_derived_cl18, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((rev @ (cons @ X1 @ X0)) = (append @ (rev @ X0) @ (cons @ X1 @ nil)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_018])).
% 216.43/31.59 thf(zip_derived_cl760, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 216.43/31.59 ((rev @ (cons @ X3 @ (cons @ X0 @ (cons @ X1 @ (cons @ X2 @ nil)))))
% 216.43/31.59 = (append @ (cons @ X2 @ (cons @ X1 @ (cons @ X0 @ nil))) @
% 216.43/31.59 (cons @ X3 @ nil)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl758, zip_derived_cl18])).
% 216.43/31.59 thf(zip_derived_cl16, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((append @ (cons @ X0 @ X1) @ X2) = (cons @ X0 @ (append @ X1 @ X2)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_016])).
% 216.43/31.59 thf(zip_derived_cl3116, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 216.43/31.59 ((rev @ (cons @ X3 @ (cons @ X2 @ (cons @ X1 @ (cons @ X0 @ nil)))))
% 216.43/31.59 = (cons @ X0 @
% 216.43/31.59 (append @ (cons @ X1 @ (cons @ X2 @ nil)) @ (cons @ X3 @ nil))))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl760, zip_derived_cl16])).
% 216.43/31.59 thf(zip_derived_cl16, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((append @ (cons @ X0 @ X1) @ X2) = (cons @ X0 @ (append @ X1 @ X2)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_016])).
% 216.43/31.59 thf(zip_derived_cl244, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((cons @ X0 @ (cons @ X1 @ nil))
% 216.43/31.59 = (append @ (cons @ X0 @ nil) @ (cons @ X1 @ nil)))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl128, zip_derived_cl243])).
% 216.43/31.59 thf(zip_derived_cl3117, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 216.43/31.59 ((rev @ (cons @ X3 @ (cons @ X2 @ (cons @ X1 @ (cons @ X0 @ nil)))))
% 216.43/31.59 = (cons @ X0 @ (cons @ X1 @ (cons @ X2 @ (cons @ X3 @ nil)))))),
% 216.43/31.59 inference('demod', [status(thm)],
% 216.43/31.59 [zip_derived_cl3116, zip_derived_cl16, zip_derived_cl244])).
% 216.43/31.59 thf(axiom_004, axiom, (( leqNat @ z @ Y ) = ( btrue ))).
% 216.43/31.59 thf(zip_derived_cl4, plain, (![X0 : $i]: ((leqNat @ z @ X0) = (btrue))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_004])).
% 216.43/31.59 thf(axiom_023, axiom,
% 216.43/31.59 (( sorted @ ( cons @ Y @ ( cons @ Y2 @ Xs ) ) ) =
% 216.43/31.59 ( andb @ ( leqNat @ Y @ Y2 ) @ ( sorted @ ( cons @ Y2 @ Xs ) ) ))).
% 216.43/31.59 thf(zip_derived_cl23, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((sorted @ (cons @ X0 @ (cons @ X1 @ X2)))
% 216.43/31.59 = (andb @ (leqNat @ X0 @ X1) @ (sorted @ (cons @ X1 @ X2))))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_023])).
% 216.43/31.59 thf(zip_derived_cl71, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((sorted @ (cons @ z @ (cons @ X1 @ X0)))
% 216.43/31.59 = (andb @ btrue @ (sorted @ (cons @ X1 @ X0))))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl4, zip_derived_cl23])).
% 216.43/31.59 thf(axiom_019, axiom, (( andb @ btrue @ Q ) = ( Q ))).
% 216.43/31.59 thf(zip_derived_cl19, plain, (![X0 : $i]: ((andb @ btrue @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_019])).
% 216.43/31.59 thf(zip_derived_cl74, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((sorted @ (cons @ z @ (cons @ X1 @ X0)))
% 216.43/31.59 = (sorted @ (cons @ X1 @ X0)))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl71, zip_derived_cl19])).
% 216.43/31.59 thf(zip_derived_cl4, plain, (![X0 : $i]: ((leqNat @ z @ X0) = (btrue))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_004])).
% 216.43/31.59 thf(axiom_022, axiom, (( sorted @ ( cons @ Y @ nil ) ) = ( btrue ))).
% 216.43/31.59 thf(zip_derived_cl22, plain,
% 216.43/31.59 (![X0 : $i]: ((sorted @ (cons @ X0 @ nil)) = (btrue))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_022])).
% 216.43/31.59 thf(zip_derived_cl23, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((sorted @ (cons @ X0 @ (cons @ X1 @ X2)))
% 216.43/31.59 = (andb @ (leqNat @ X0 @ X1) @ (sorted @ (cons @ X1 @ X2))))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_023])).
% 216.43/31.59 thf(zip_derived_cl69, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((sorted @ (cons @ X1 @ (cons @ X0 @ nil)))
% 216.43/31.59 = (andb @ (leqNat @ X1 @ X0) @ btrue))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl22, zip_derived_cl23])).
% 216.43/31.59 thf(axiom_006, axiom,
% 216.43/31.59 (( leqNat @ ( s @ Z ) @ ( s @ M ) ) = ( leqNat @ Z @ M ))).
% 216.43/31.59 thf(zip_derived_cl6, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((leqNat @ (s @ X0) @ (s @ X1)) = (leqNat @ X0 @ X1))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_006])).
% 216.43/31.59 thf(zip_derived_cl23, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((sorted @ (cons @ X0 @ (cons @ X1 @ X2)))
% 216.43/31.59 = (andb @ (leqNat @ X0 @ X1) @ (sorted @ (cons @ X1 @ X2))))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_023])).
% 216.43/31.59 thf(zip_derived_cl73, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((sorted @ (cons @ (s @ X1) @ (cons @ (s @ X0) @ X2)))
% 216.43/31.59 = (andb @ (leqNat @ X1 @ X0) @ (sorted @ (cons @ (s @ X0) @ X2))))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl6, zip_derived_cl23])).
% 216.43/31.59 thf(zip_derived_cl488, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i, X2 : $i]:
% 216.43/31.59 ((sorted @ (cons @ (s @ X2) @ (cons @ (s @ X1) @ (cons @ X0 @ nil))))
% 216.43/31.59 = (andb @ (leqNat @ X2 @ X1) @
% 216.43/31.59 (andb @ (leqNat @ (s @ X1) @ X0) @ btrue)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl69, zip_derived_cl73])).
% 216.43/31.59 thf(zip_derived_cl9797, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((sorted @ (cons @ (s @ z) @ (cons @ (s @ X1) @ (cons @ X0 @ nil))))
% 216.43/31.59 = (andb @ btrue @ (andb @ (leqNat @ (s @ X1) @ X0) @ btrue)))),
% 216.43/31.59 inference('sup+', [status(thm)], [zip_derived_cl4, zip_derived_cl488])).
% 216.43/31.59 thf(zip_derived_cl19, plain, (![X0 : $i]: ((andb @ btrue @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_019])).
% 216.43/31.59 thf(zip_derived_cl9808, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((sorted @ (cons @ (s @ z) @ (cons @ (s @ X1) @ (cons @ X0 @ nil))))
% 216.43/31.59 = (andb @ (leqNat @ (s @ X1) @ X0) @ btrue))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl9797, zip_derived_cl19])).
% 216.43/31.59 thf(zip_derived_cl6, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((leqNat @ (s @ X0) @ (s @ X1)) = (leqNat @ X0 @ X1))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_006])).
% 216.43/31.59 thf(zip_derived_cl6, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((leqNat @ (s @ X0) @ (s @ X1)) = (leqNat @ X0 @ X1))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_006])).
% 216.43/31.59 thf(zip_derived_cl4, plain, (![X0 : $i]: ((leqNat @ z @ X0) = (btrue))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_004])).
% 216.43/31.59 thf(zip_derived_cl19, plain, (![X0 : $i]: ((andb @ btrue @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_019])).
% 216.43/31.59 thf(axiom_031, axiom, (( eq2 @ X @ X ) = ( btrue ))).
% 216.43/31.59 thf(zip_derived_cl31, plain, (![X0 : $i]: ((eq2 @ X0 @ X0) = (btrue))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_031])).
% 216.43/31.59 thf(zip_derived_cl31, plain, (![X0 : $i]: ((eq2 @ X0 @ X0) = (btrue))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_031])).
% 216.43/31.59 thf(axiom_008, axiom,
% 216.43/31.59 (( lengthNat @ ( cons @ Y @ Xs ) ) = ( s @ ( lengthNat @ Xs ) ))).
% 216.43/31.59 thf(zip_derived_cl8, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((lengthNat @ (cons @ X1 @ X0)) = (s @ (lengthNat @ X0)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_008])).
% 216.43/31.59 thf(zip_derived_cl8, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((lengthNat @ (cons @ X1 @ X0)) = (s @ (lengthNat @ X0)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_008])).
% 216.43/31.59 thf(zip_derived_cl8, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((lengthNat @ (cons @ X1 @ X0)) = (s @ (lengthNat @ X0)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_008])).
% 216.43/31.59 thf(zip_derived_cl8, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((lengthNat @ (cons @ X1 @ X0)) = (s @ (lengthNat @ X0)))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_008])).
% 216.43/31.59 thf(axiom_007, axiom, (( lengthNat @ nil ) = ( z ))).
% 216.43/31.59 thf(zip_derived_cl7, plain, (((lengthNat @ nil) = (z))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_007])).
% 216.43/31.59 thf(zip_derived_cl6, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((leqNat @ (s @ X0) @ (s @ X1)) = (leqNat @ X0 @ X1))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_006])).
% 216.43/31.59 thf(zip_derived_cl6, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((leqNat @ (s @ X0) @ (s @ X1)) = (leqNat @ X0 @ X1))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_006])).
% 216.43/31.59 thf(zip_derived_cl6, plain,
% 216.43/31.59 (![X0 : $i, X1 : $i]:
% 216.43/31.59 ((leqNat @ (s @ X0) @ (s @ X1)) = (leqNat @ X0 @ X1))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_006])).
% 216.43/31.59 thf(axiom_005, axiom, (( leqNat @ ( s @ Z ) @ z ) = ( bfalse ))).
% 216.43/31.59 thf(zip_derived_cl5, plain,
% 216.43/31.59 (![X0 : $i]: ((leqNat @ (s @ X0) @ z) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_005])).
% 216.43/31.59 thf(axiom_025, axiom, (( eq2 @ bfalse @ btrue ) = ( bfalse ))).
% 216.43/31.59 thf(zip_derived_cl25, plain, (((eq2 @ bfalse @ btrue) = (bfalse))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_025])).
% 216.43/31.59 thf(axiom_009, axiom, (( impl @ btrue @ Q ) = ( Q ))).
% 216.43/31.59 thf(zip_derived_cl9, plain, (![X0 : $i]: ((impl @ btrue @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_009])).
% 216.43/31.59 thf(zip_derived_cl9, plain, (![X0 : $i]: ((impl @ btrue @ X0) = (X0))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_009])).
% 216.43/31.59 thf(zip_derived_cl73865, plain,
% 216.43/31.59 (![X0 : $i]:
% 216.43/31.59 ((psorted_rev @
% 216.43/31.59 (cons @ (s @ (s @ (s @ X0))) @
% 216.43/31.59 (cons @ (s @ (s @ z)) @ (cons @ (s @ z) @ (cons @ z @ nil)))))
% 216.43/31.59 = (bfalse))),
% 216.43/31.59 inference('demod', [status(thm)],
% 216.43/31.59 [zip_derived_cl73851, zip_derived_cl3117, zip_derived_cl74,
% 216.43/31.59 zip_derived_cl9808, zip_derived_cl6, zip_derived_cl6,
% 216.43/31.59 zip_derived_cl4, zip_derived_cl19, zip_derived_cl31,
% 216.43/31.59 zip_derived_cl31, zip_derived_cl8, zip_derived_cl8,
% 216.43/31.59 zip_derived_cl8, zip_derived_cl8, zip_derived_cl7,
% 216.43/31.59 zip_derived_cl6, zip_derived_cl6, zip_derived_cl6,
% 216.43/31.59 zip_derived_cl5, zip_derived_cl25, zip_derived_cl9,
% 216.43/31.59 zip_derived_cl9])).
% 216.43/31.59 thf(goal, conjecture, (( eq2 @ ( psorted_rev @ X ) @ bfalse ) = ( btrue ))).
% 216.43/31.59 thf(zf_stmt_0, negated_conjecture,
% 216.43/31.59 (( eq2 @ ( psorted_rev @ X ) @ bfalse ) != ( btrue )),
% 216.43/31.59 inference('cnf.neg', [status(esa)], [goal])).
% 216.43/31.59 thf(zip_derived_cl32, plain,
% 216.43/31.59 (![X0 : $i]: ((eq2 @ (psorted_rev @ X0) @ bfalse) != (btrue))),
% 216.43/31.59 inference('cnf', [status(esa)], [zf_stmt_0])).
% 216.43/31.59 thf(zip_derived_cl73907, plain, (((eq2 @ bfalse @ bfalse) != (btrue))),
% 216.43/31.59 inference('sup-', [status(thm)], [zip_derived_cl73865, zip_derived_cl32])).
% 216.43/31.59 thf(zip_derived_cl31, plain, (![X0 : $i]: ((eq2 @ X0 @ X0) = (btrue))),
% 216.43/31.59 inference('cnf', [status(esa)], [axiom_031])).
% 216.43/31.59 thf(zip_derived_cl73908, plain, (((btrue) != (btrue))),
% 216.43/31.59 inference('demod', [status(thm)], [zip_derived_cl73907, zip_derived_cl31])).
% 216.43/31.59 thf(zip_derived_cl73909, plain, ($false),
% 216.43/31.59 inference('simplify', [status(thm)], [zip_derived_cl73908])).
% 216.43/31.59
% 216.43/31.59 % SZS output end Refutation
% 216.43/31.59
% 216.43/31.59
% 216.43/31.59 % Terminating...
% 0.61/31.62 % Runner terminated.
% 0.61/31.63 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------