%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEV542+1 : TPTP v9.2.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.lsjtaMCc1o true
% Computer : n028.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 : Thu Oct 2 04:57:49 PM UTC 2025
% Result : Theorem 67.38s 10.22s
% Output : Refutation 67.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 12
% Syntax : Number of formulae : 178 ( 77 unt; 0 typ; 0 def)
% Number of atoms : 309 ( 64 equ; 0 cnn)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 1269 ( 108 ~; 117 |; 4 &;1030 @)
% ( 7 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 15 ( 13 usr; 2 con; 0-2 aty)
% Number of variables : 271 ( 0 ^; 268 !; 3 ?; 271 :)
% Comments :
%------------------------------------------------------------------------------
thf(mem_type,type,
mem: $i > $i > $o ).
thf(u_type,type,
u: $i > $i > $i ).
thf(subq_type,type,
subq: $i > $i > $o ).
thf(p_type,type,
p: $i > $i ).
thf(a_type,type,
a: $i > $i > $i ).
thf(atleast2p_type,type,
atleast2p: $i > $o ).
thf(sk__1_type,type,
sk__1: $i > $i > $i ).
thf(sk__type,type,
sk_: $i > $i > $i ).
thf(atleast3p_type,type,
atleast3p: $i > $o ).
thf(s_type,type,
s: $i > $i ).
thf(n_type,type,
n: $i > $i ).
thf(disj_type,type,
disj: $i > $i > $o ).
thf(e_type,type,
e: $i ).
thf(s_ax,axiom,
! [X: $i,Y: $i] :
( ( mem @ X @ ( s @ Y ) )
<=> ( X = Y ) ) ).
thf(zip_derived_cl9,plain,
! [X0: $i,X1: $i] :
( ( mem @ X0 @ ( s @ X1 ) )
| ( X0 != X1 ) ),
inference(cnf,[status(esa)],[s_ax]) ).
thf(zip_derived_cl110,plain,
! [X0: $i] : ( mem @ X0 @ ( s @ X0 ) ),
inference(eq_res,[status(thm)],[zip_derived_cl9]) ).
thf(a_def,axiom,
! [X: $i,Y: $i] :
( ( a @ X @ Y )
= ( u @ X @ ( s @ Y ) ) ) ).
thf(zip_derived_cl16,plain,
! [X0: $i,X1: $i] :
( ( a @ X0 @ X1 )
= ( u @ X0 @ ( s @ X1 ) ) ),
inference(cnf,[status(esa)],[a_def]) ).
thf(subq_def,axiom,
! [X: $i,Y: $i] :
( ( subq @ X @ Y )
<=> ! [Z: $i] :
( ( mem @ Z @ X )
=> ( mem @ Z @ Y ) ) ) ).
thf(zip_derived_cl2,plain,
! [X0: $i,X1: $i] :
( ( subq @ X0 @ X1 )
| ( mem @ ( sk_ @ X1 @ X0 ) @ X0 ) ),
inference(cnf,[status(esa)],[subq_def]) ).
thf(u_ax,axiom,
! [X: $i,Y: $i,Z: $i] :
( ( mem @ X @ ( u @ Y @ Z ) )
<=> ( ( mem @ X @ Y )
| ( mem @ X @ Z ) ) ) ).
thf(zip_derived_cl11,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( mem @ X0 @ ( u @ X1 @ X2 ) )
| ~ ( mem @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[u_ax]) ).
thf(zip_derived_cl168,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( subq @ X0 @ X1 )
| ( mem @ ( sk_ @ X1 @ X0 ) @ ( u @ X0 @ X2 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2,zip_derived_cl11]) ).
thf(zip_derived_cl1,plain,
! [X0: $i,X1: $i] :
( ( subq @ X0 @ X1 )
| ~ ( mem @ ( sk_ @ X1 @ X0 ) @ X1 ) ),
inference(cnf,[status(esa)],[subq_def]) ).
thf(zip_derived_cl2358,plain,
! [X0: $i,X1: $i] :
( ( subq @ X1 @ ( u @ X1 @ X0 ) )
| ( subq @ X1 @ ( u @ X1 @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl168,zip_derived_cl1]) ).
thf(zip_derived_cl2363,plain,
! [X0: $i,X1: $i] : ( subq @ X1 @ ( u @ X1 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl2358]) ).
thf(zip_derived_cl2505,plain,
! [X0: $i,X1: $i] : ( subq @ X1 @ ( a @ X1 @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl16,zip_derived_cl2363]) ).
thf(atleast3_81,conjecture,
atleast3p @ ( a @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) @ ( n @ ( s @ ( n @ e ) ) ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ( atleast3p @ ( a @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) @ ( n @ ( s @ ( n @ e ) ) ) ) ),
inference('cnf.neg',[status(esa)],[atleast3_81]) ).
thf(zip_derived_cl79,plain,
~ ( atleast3p @ ( a @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) @ ( n @ ( s @ ( n @ e ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(atleast3p_def,axiom,
! [X: $i] :
( ( atleast3p @ X )
<=> ? [Y: $i] :
( ~ ( subq @ X @ Y )
& ( atleast2p @ Y )
& ( subq @ Y @ X ) ) ) ).
thf(zip_derived_cl26,plain,
! [X0: $i,X1: $i] :
( ( atleast3p @ X0 )
| ~ ( subq @ X1 @ X0 )
| ~ ( atleast2p @ X1 )
| ( subq @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[atleast3p_def]) ).
thf(zip_derived_cl236,plain,
! [X0: $i] :
( ~ ( subq @ X0 @ ( a @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) @ ( n @ ( s @ ( n @ e ) ) ) ) )
| ~ ( atleast2p @ X0 )
| ( subq @ ( a @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) @ ( n @ ( s @ ( n @ e ) ) ) ) @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl79,zip_derived_cl26]) ).
thf(zip_derived_cl2540,plain,
( ~ ( atleast2p @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) )
| ( subq @ ( a @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) @ ( n @ ( s @ ( n @ e ) ) ) ) @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2505,zip_derived_cl236]) ).
thf(zip_derived_cl0,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( mem @ X0 @ X1 )
| ( mem @ X0 @ X2 )
| ~ ( subq @ X1 @ X2 ) ),
inference(cnf,[status(esa)],[subq_def]) ).
thf(zip_derived_cl2542,plain,
! [X0: $i] :
( ~ ( atleast2p @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) )
| ~ ( mem @ X0 @ ( a @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) @ ( n @ ( s @ ( n @ e ) ) ) ) )
| ( mem @ X0 @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2540,zip_derived_cl0]) ).
thf(zip_derived_cl110_001,plain,
! [X0: $i] : ( mem @ X0 @ ( s @ X0 ) ),
inference(eq_res,[status(thm)],[zip_derived_cl9]) ).
thf(zip_derived_cl12,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( mem @ X0 @ ( u @ X1 @ X2 ) )
| ~ ( mem @ X0 @ X2 ) ),
inference(cnf,[status(esa)],[u_ax]) ).
thf(zip_derived_cl201,plain,
! [X0: $i,X1: $i] : ( mem @ X0 @ ( u @ X1 @ ( s @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl110,zip_derived_cl12]) ).
thf(zip_derived_cl16_002,plain,
! [X0: $i,X1: $i] :
( ( a @ X0 @ X1 )
= ( u @ X0 @ ( s @ X1 ) ) ),
inference(cnf,[status(esa)],[a_def]) ).
thf(zip_derived_cl208,plain,
! [X0: $i,X1: $i] : ( mem @ X0 @ ( a @ X1 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl201,zip_derived_cl16]) ).
thf(zip_derived_cl2576,plain,
( ( mem @ ( n @ ( s @ ( n @ e ) ) ) @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) )
| ~ ( atleast2p @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2542,zip_derived_cl208]) ).
thf(p_ax,axiom,
! [X: $i,Y: $i] :
( ( mem @ X @ ( p @ Y ) )
<=> ( subq @ X @ Y ) ) ).
thf(zip_derived_cl18,plain,
! [X0: $i,X1: $i] :
( ( subq @ X0 @ X1 )
| ~ ( mem @ X0 @ ( p @ X1 ) ) ),
inference(cnf,[status(esa)],[p_ax]) ).
thf(zip_derived_cl2613,plain,
( ~ ( atleast2p @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) )
| ( subq @ ( n @ ( s @ ( n @ e ) ) ) @ ( s @ ( s @ ( n @ e ) ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2576,zip_derived_cl18]) ).
thf(setext,axiom,
! [X: $i,Y: $i] :
( ( subq @ X @ Y )
=> ( ( subq @ Y @ X )
=> ( X = Y ) ) ) ).
thf(zip_derived_cl3,plain,
! [X0: $i,X1: $i] :
( ~ ( subq @ X0 @ X1 )
| ( X1 = X0 )
| ~ ( subq @ X1 @ X0 ) ),
inference(cnf,[status(esa)],[setext]) ).
thf(zip_derived_cl2625,plain,
( ~ ( atleast2p @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) )
| ( ( s @ ( s @ ( n @ e ) ) )
= ( n @ ( s @ ( n @ e ) ) ) )
| ~ ( subq @ ( s @ ( s @ ( n @ e ) ) ) @ ( n @ ( s @ ( n @ e ) ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2613,zip_derived_cl3]) ).
thf(n_def,axiom,
! [X: $i] :
( ( n @ X )
= ( a @ X @ X ) ) ).
thf(zip_derived_cl17,plain,
! [X0: $i] :
( ( n @ X0 )
= ( a @ X0 @ X0 ) ),
inference(cnf,[status(esa)],[n_def]) ).
thf(zip_derived_cl16_003,plain,
! [X0: $i,X1: $i] :
( ( a @ X0 @ X1 )
= ( u @ X0 @ ( s @ X1 ) ) ),
inference(cnf,[status(esa)],[a_def]) ).
thf(zip_derived_cl2_004,plain,
! [X0: $i,X1: $i] :
( ( subq @ X0 @ X1 )
| ( mem @ ( sk_ @ X1 @ X0 ) @ X0 ) ),
inference(cnf,[status(esa)],[subq_def]) ).
thf(zip_derived_cl12_005,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( mem @ X0 @ ( u @ X1 @ X2 ) )
| ~ ( mem @ X0 @ X2 ) ),
inference(cnf,[status(esa)],[u_ax]) ).
thf(zip_derived_cl204,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( subq @ X0 @ X1 )
| ( mem @ ( sk_ @ X1 @ X0 ) @ ( u @ X2 @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2,zip_derived_cl12]) ).
thf(zip_derived_cl1_006,plain,
! [X0: $i,X1: $i] :
( ( subq @ X0 @ X1 )
| ~ ( mem @ ( sk_ @ X1 @ X0 ) @ X1 ) ),
inference(cnf,[status(esa)],[subq_def]) ).
thf(zip_derived_cl3712,plain,
! [X0: $i,X1: $i] :
( ( subq @ X0 @ ( u @ X1 @ X0 ) )
| ( subq @ X0 @ ( u @ X1 @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl204,zip_derived_cl1]) ).
thf(zip_derived_cl3718,plain,
! [X0: $i,X1: $i] : ( subq @ X0 @ ( u @ X1 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl3712]) ).
thf(zip_derived_cl3737,plain,
! [X0: $i,X1: $i] : ( subq @ ( s @ X0 ) @ ( a @ X1 @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl16,zip_derived_cl3718]) ).
thf(zip_derived_cl3809,plain,
! [X0: $i] : ( subq @ ( s @ X0 ) @ ( n @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl3737]) ).
thf(zip_derived_cl3968,plain,
( ~ ( atleast2p @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) )
| ( ( s @ ( s @ ( n @ e ) ) )
= ( n @ ( s @ ( n @ e ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2625,zip_derived_cl3809]) ).
thf(zip_derived_cl2_007,plain,
! [X0: $i,X1: $i] :
( ( subq @ X0 @ X1 )
| ( mem @ ( sk_ @ X1 @ X0 ) @ X0 ) ),
inference(cnf,[status(esa)],[subq_def]) ).
thf(e_ax,axiom,
! [X: $i] :
~ ( mem @ X @ e ) ).
thf(zip_derived_cl7,plain,
! [X0: $i] :
~ ( mem @ X0 @ e ),
inference(cnf,[status(esa)],[e_ax]) ).
thf(zip_derived_cl80,plain,
! [X0: $i] : ( subq @ e @ X0 ),
inference('s_sup-',[status(thm)],[zip_derived_cl2,zip_derived_cl7]) ).
thf(zip_derived_cl19,plain,
! [X0: $i,X1: $i] :
( ( mem @ X0 @ ( p @ X1 ) )
| ~ ( subq @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[p_ax]) ).
thf(zip_derived_cl221,plain,
! [X0: $i] : ( mem @ e @ ( p @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl80,zip_derived_cl19]) ).
thf(atleast2p_def,axiom,
! [X: $i] :
( ( atleast2p @ X )
<=> ? [Y: $i] :
( ~ ( subq @ X @ ( p @ Y ) )
& ( mem @ Y @ X ) ) ) ).
thf(zip_derived_cl22,plain,
! [X0: $i,X1: $i] :
( ( atleast2p @ X0 )
| ~ ( mem @ X1 @ X0 )
| ( subq @ X0 @ ( p @ X1 ) ) ),
inference(cnf,[status(esa)],[atleast2p_def]) ).
thf(zip_derived_cl264,plain,
! [X0: $i] :
( ( atleast2p @ ( p @ X0 ) )
| ( subq @ ( p @ X0 ) @ ( p @ e ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl221,zip_derived_cl22]) ).
thf(zip_derived_cl0_008,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( mem @ X0 @ X1 )
| ( mem @ X0 @ X2 )
| ~ ( subq @ X1 @ X2 ) ),
inference(cnf,[status(esa)],[subq_def]) ).
thf(zip_derived_cl1134,plain,
! [X0: $i,X1: $i] :
( ( atleast2p @ ( p @ X0 ) )
| ~ ( mem @ X1 @ ( p @ X0 ) )
| ( mem @ X1 @ ( p @ e ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl264,zip_derived_cl0]) ).
thf(zip_derived_cl39695,plain,
! [X0: $i] :
( ( ( s @ ( s @ ( n @ e ) ) )
= ( n @ ( s @ ( n @ e ) ) ) )
| ~ ( mem @ X0 @ ( p @ ( s @ ( s @ ( n @ e ) ) ) ) )
| ( mem @ X0 @ ( p @ e ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl3968,zip_derived_cl1134]) ).
thf(zip_derived_cl2_009,plain,
! [X0: $i,X1: $i] :
( ( subq @ X0 @ X1 )
| ( mem @ ( sk_ @ X1 @ X0 ) @ X0 ) ),
inference(cnf,[status(esa)],[subq_def]) ).
thf(zip_derived_cl1_010,plain,
! [X0: $i,X1: $i] :
( ( subq @ X0 @ X1 )
| ~ ( mem @ ( sk_ @ X1 @ X0 ) @ X1 ) ),
inference(cnf,[status(esa)],[subq_def]) ).
thf(zip_derived_cl82,plain,
! [X0: $i] :
( ( subq @ X0 @ X0 )
| ( subq @ X0 @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2,zip_derived_cl1]) ).
thf(zip_derived_cl83,plain,
! [X0: $i] : ( subq @ X0 @ X0 ),
inference(simplify,[status(thm)],[zip_derived_cl82]) ).
thf(zip_derived_cl19_011,plain,
! [X0: $i,X1: $i] :
( ( mem @ X0 @ ( p @ X1 ) )
| ~ ( subq @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[p_ax]) ).
thf(zip_derived_cl220,plain,
! [X0: $i] : ( mem @ X0 @ ( p @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl83,zip_derived_cl19]) ).
thf(zip_derived_cl40013,plain,
( ( mem @ ( s @ ( s @ ( n @ e ) ) ) @ ( p @ e ) )
| ( ( s @ ( s @ ( n @ e ) ) )
= ( n @ ( s @ ( n @ e ) ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl39695,zip_derived_cl220]) ).
thf(disj_def,axiom,
! [X: $i,Y: $i] :
( ( disj @ X @ Y )
<=> ~ ? [Z: $i] :
( ( mem @ Z @ Y )
& ( mem @ Z @ X ) ) ) ).
thf(zip_derived_cl5,plain,
! [X0: $i,X1: $i] :
( ( disj @ X0 @ X1 )
| ( mem @ ( sk__1 @ X1 @ X0 ) @ X1 ) ),
inference(cnf,[status(esa)],[disj_def]) ).
thf(zip_derived_cl18_012,plain,
! [X0: $i,X1: $i] :
( ( subq @ X0 @ X1 )
| ~ ( mem @ X0 @ ( p @ X1 ) ) ),
inference(cnf,[status(esa)],[p_ax]) ).
thf(zip_derived_cl213,plain,
! [X0: $i,X1: $i] :
( ( disj @ X1 @ ( p @ X0 ) )
| ( subq @ ( sk__1 @ ( p @ X0 ) @ X1 ) @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl5,zip_derived_cl18]) ).
thf(zip_derived_cl80_013,plain,
! [X0: $i] : ( subq @ e @ X0 ),
inference('s_sup-',[status(thm)],[zip_derived_cl2,zip_derived_cl7]) ).
thf(zip_derived_cl3_014,plain,
! [X0: $i,X1: $i] :
( ~ ( subq @ X0 @ X1 )
| ( X1 = X0 )
| ~ ( subq @ X1 @ X0 ) ),
inference(cnf,[status(esa)],[setext]) ).
thf(zip_derived_cl103,plain,
! [X0: $i] :
( ( X0 = e )
| ~ ( subq @ X0 @ e ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl80,zip_derived_cl3]) ).
thf(zip_derived_cl4225,plain,
! [X0: $i] :
( ( disj @ X0 @ ( p @ e ) )
| ( ( sk__1 @ ( p @ e ) @ X0 )
= e ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl213,zip_derived_cl103]) ).
thf(zip_derived_cl6,plain,
! [X0: $i,X1: $i] :
( ( disj @ X0 @ X1 )
| ( mem @ ( sk__1 @ X1 @ X0 ) @ X0 ) ),
inference(cnf,[status(esa)],[disj_def]) ).
thf(zip_derived_cl8,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ~ ( mem @ X1 @ ( s @ X0 ) ) ),
inference(cnf,[status(esa)],[s_ax]) ).
thf(zip_derived_cl113,plain,
! [X0: $i,X1: $i] :
( ( disj @ ( s @ X0 ) @ X1 )
| ( ( sk__1 @ X1 @ ( s @ X0 ) )
= X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl6,zip_derived_cl8]) ).
thf(zip_derived_cl4339,plain,
! [X0: $i] :
( ( disj @ ( s @ X0 ) @ ( p @ e ) )
| ( disj @ ( s @ X0 ) @ ( p @ e ) )
| ( e = X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl4225,zip_derived_cl113]) ).
thf(zip_derived_cl4354,plain,
! [X0: $i] :
( ( e = X0 )
| ( disj @ ( s @ X0 ) @ ( p @ e ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl4339]) ).
thf(zip_derived_cl110_015,plain,
! [X0: $i] : ( mem @ X0 @ ( s @ X0 ) ),
inference(eq_res,[status(thm)],[zip_derived_cl9]) ).
thf(zip_derived_cl4,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( mem @ X0 @ X1 )
| ~ ( mem @ X0 @ X2 )
| ~ ( disj @ X1 @ X2 ) ),
inference(cnf,[status(esa)],[disj_def]) ).
thf(zip_derived_cl162,plain,
! [X0: $i,X1: $i] :
( ~ ( mem @ X0 @ X1 )
| ~ ( disj @ ( s @ X0 ) @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl110,zip_derived_cl4]) ).
thf(zip_derived_cl4404,plain,
! [X0: $i] :
( ( e = X0 )
| ~ ( mem @ X0 @ ( p @ e ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl4354,zip_derived_cl162]) ).
thf(zip_derived_cl40121,plain,
( ( ( s @ ( s @ ( n @ e ) ) )
= ( n @ ( s @ ( n @ e ) ) ) )
| ( e
= ( s @ ( s @ ( n @ e ) ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl40013,zip_derived_cl4404]) ).
thf(zip_derived_cl113_016,plain,
! [X0: $i,X1: $i] :
( ( disj @ ( s @ X0 ) @ X1 )
| ( ( sk__1 @ X1 @ ( s @ X0 ) )
= X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl6,zip_derived_cl8]) ).
thf(zip_derived_cl5_017,plain,
! [X0: $i,X1: $i] :
( ( disj @ X0 @ X1 )
| ( mem @ ( sk__1 @ X1 @ X0 ) @ X1 ) ),
inference(cnf,[status(esa)],[disj_def]) ).
thf(zip_derived_cl8_018,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ~ ( mem @ X1 @ ( s @ X0 ) ) ),
inference(cnf,[status(esa)],[s_ax]) ).
thf(zip_derived_cl108,plain,
! [X0: $i,X1: $i] :
( ( disj @ X1 @ ( s @ X0 ) )
| ( ( sk__1 @ ( s @ X0 ) @ X1 )
= X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl5,zip_derived_cl8]) ).
thf(zip_derived_cl876,plain,
! [X0: $i,X1: $i] :
( ( disj @ ( s @ X0 ) @ ( s @ X1 ) )
| ( disj @ ( s @ X0 ) @ ( s @ X1 ) )
| ( X0 = X1 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl113,zip_derived_cl108]) ).
thf(zip_derived_cl882,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ( disj @ ( s @ X0 ) @ ( s @ X1 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl876]) ).
thf(zip_derived_cl17_019,plain,
! [X0: $i] :
( ( n @ X0 )
= ( a @ X0 @ X0 ) ),
inference(cnf,[status(esa)],[n_def]) ).
thf(zip_derived_cl110_020,plain,
! [X0: $i] : ( mem @ X0 @ ( s @ X0 ) ),
inference(eq_res,[status(thm)],[zip_derived_cl9]) ).
thf(zip_derived_cl17_021,plain,
! [X0: $i] :
( ( n @ X0 )
= ( a @ X0 @ X0 ) ),
inference(cnf,[status(esa)],[n_def]) ).
thf(zip_derived_cl16_022,plain,
! [X0: $i,X1: $i] :
( ( a @ X0 @ X1 )
= ( u @ X0 @ ( s @ X1 ) ) ),
inference(cnf,[status(esa)],[a_def]) ).
thf(zip_derived_cl16_023,plain,
! [X0: $i,X1: $i] :
( ( a @ X0 @ X1 )
= ( u @ X0 @ ( s @ X1 ) ) ),
inference(cnf,[status(esa)],[a_def]) ).
thf(zip_derived_cl110_024,plain,
! [X0: $i] : ( mem @ X0 @ ( s @ X0 ) ),
inference(eq_res,[status(thm)],[zip_derived_cl9]) ).
thf(zip_derived_cl11_025,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( mem @ X0 @ ( u @ X1 @ X2 ) )
| ~ ( mem @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[u_ax]) ).
thf(zip_derived_cl167,plain,
! [X0: $i,X1: $i] : ( mem @ X0 @ ( u @ ( s @ X0 ) @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl110,zip_derived_cl11]) ).
thf(zip_derived_cl175,plain,
! [X0: $i,X1: $i] : ( mem @ X1 @ ( a @ ( s @ X1 ) @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl16,zip_derived_cl167]) ).
thf(zip_derived_cl11_026,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( mem @ X0 @ ( u @ X1 @ X2 ) )
| ~ ( mem @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[u_ax]) ).
thf(zip_derived_cl198,plain,
! [X0: $i,X1: $i,X2: $i] : ( mem @ X1 @ ( u @ ( a @ ( s @ X1 ) @ X0 ) @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl175,zip_derived_cl11]) ).
thf(zip_derived_cl221_027,plain,
! [X0: $i] : ( mem @ e @ ( p @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl80,zip_derived_cl19]) ).
thf(zip_derived_cl4_028,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( mem @ X0 @ X1 )
| ~ ( mem @ X0 @ X2 )
| ~ ( disj @ X1 @ X2 ) ),
inference(cnf,[status(esa)],[disj_def]) ).
thf(zip_derived_cl261,plain,
! [X0: $i,X1: $i] :
( ~ ( mem @ e @ X1 )
| ~ ( disj @ ( p @ X0 ) @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl221,zip_derived_cl4]) ).
thf(zip_derived_cl3413,plain,
! [X0: $i,X1: $i,X2: $i] :
~ ( disj @ ( p @ X2 ) @ ( u @ ( a @ ( s @ e ) @ X1 ) @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl198,zip_derived_cl261]) ).
thf(zip_derived_cl8841,plain,
! [X0: $i,X1: $i,X2: $i] :
~ ( disj @ ( p @ X2 ) @ ( a @ ( a @ ( s @ e ) @ X1 ) @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl16,zip_derived_cl3413]) ).
thf(zip_derived_cl8847,plain,
! [X0: $i,X1: $i] :
~ ( disj @ ( p @ X1 ) @ ( n @ ( a @ ( s @ e ) @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl17,zip_derived_cl8841]) ).
thf(zip_derived_cl6_029,plain,
! [X0: $i,X1: $i] :
( ( disj @ X0 @ X1 )
| ( mem @ ( sk__1 @ X1 @ X0 ) @ X0 ) ),
inference(cnf,[status(esa)],[disj_def]) ).
thf(zip_derived_cl18_030,plain,
! [X0: $i,X1: $i] :
( ( subq @ X0 @ X1 )
| ~ ( mem @ X0 @ ( p @ X1 ) ) ),
inference(cnf,[status(esa)],[p_ax]) ).
thf(zip_derived_cl214,plain,
! [X0: $i,X1: $i] :
( ( disj @ ( p @ X0 ) @ X1 )
| ( subq @ ( sk__1 @ X1 @ ( p @ X0 ) ) @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl6,zip_derived_cl18]) ).
thf(zip_derived_cl103_031,plain,
! [X0: $i] :
( ( X0 = e )
| ~ ( subq @ X0 @ e ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl80,zip_derived_cl3]) ).
thf(zip_derived_cl4310,plain,
! [X0: $i] :
( ( disj @ ( p @ e ) @ X0 )
| ( ( sk__1 @ X0 @ ( p @ e ) )
= e ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl214,zip_derived_cl103]) ).
thf(zip_derived_cl5_032,plain,
! [X0: $i,X1: $i] :
( ( disj @ X0 @ X1 )
| ( mem @ ( sk__1 @ X1 @ X0 ) @ X1 ) ),
inference(cnf,[status(esa)],[disj_def]) ).
thf(zip_derived_cl5526,plain,
! [X0: $i] :
( ( disj @ ( p @ e ) @ X0 )
| ( disj @ ( p @ e ) @ X0 )
| ( mem @ e @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl4310,zip_derived_cl5]) ).
thf(zip_derived_cl5541,plain,
! [X0: $i] :
( ( mem @ e @ X0 )
| ( disj @ ( p @ e ) @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl5526]) ).
thf(zip_derived_cl8852,plain,
! [X0: $i] : ( mem @ e @ ( n @ ( a @ ( s @ e ) @ X0 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl8847,zip_derived_cl5541]) ).
thf(zip_derived_cl4_033,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( mem @ X0 @ X1 )
| ~ ( mem @ X0 @ X2 )
| ~ ( disj @ X1 @ X2 ) ),
inference(cnf,[status(esa)],[disj_def]) ).
thf(zip_derived_cl8855,plain,
! [X0: $i,X1: $i] :
( ~ ( mem @ e @ X1 )
| ~ ( disj @ ( n @ ( a @ ( s @ e ) @ X0 ) ) @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl8852,zip_derived_cl4]) ).
thf(zip_derived_cl8937,plain,
! [X0: $i] :
~ ( disj @ ( n @ ( a @ ( s @ e ) @ X0 ) ) @ ( s @ e ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl110,zip_derived_cl8855]) ).
thf(zip_derived_cl8997,plain,
~ ( disj @ ( n @ ( n @ ( s @ e ) ) ) @ ( s @ e ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl17,zip_derived_cl8937]) ).
thf(zip_derived_cl5_034,plain,
! [X0: $i,X1: $i] :
( ( disj @ X0 @ X1 )
| ( mem @ ( sk__1 @ X1 @ X0 ) @ X1 ) ),
inference(cnf,[status(esa)],[disj_def]) ).
thf(zip_derived_cl4_035,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( mem @ X0 @ X1 )
| ~ ( mem @ X0 @ X2 )
| ~ ( disj @ X1 @ X2 ) ),
inference(cnf,[status(esa)],[disj_def]) ).
thf(zip_derived_cl106,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( disj @ X1 @ X0 )
| ~ ( mem @ ( sk__1 @ X0 @ X1 ) @ X2 )
| ~ ( disj @ X0 @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl5,zip_derived_cl4]) ).
thf(zip_derived_cl8999,plain,
! [X0: $i] :
( ~ ( mem @ ( sk__1 @ ( s @ e ) @ ( n @ ( n @ ( s @ e ) ) ) ) @ X0 )
| ~ ( disj @ ( s @ e ) @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl8997,zip_derived_cl106]) ).
thf(zip_derived_cl9691,plain,
! [X0: $i] :
( ( e = X0 )
| ~ ( mem @ ( sk__1 @ ( s @ e ) @ ( n @ ( n @ ( s @ e ) ) ) ) @ ( s @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl882,zip_derived_cl8999]) ).
thf(zip_derived_cl9_036,plain,
! [X0: $i,X1: $i] :
( ( mem @ X0 @ ( s @ X1 ) )
| ( X0 != X1 ) ),
inference(cnf,[status(esa)],[s_ax]) ).
thf(zip_derived_cl9713,plain,
! [X0: $i] :
( ( e = X0 )
| ( ( sk__1 @ ( s @ e ) @ ( n @ ( n @ ( s @ e ) ) ) )
!= X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl9691,zip_derived_cl9]) ).
thf(zip_derived_cl110_037,plain,
! [X0: $i] : ( mem @ X0 @ ( s @ X0 ) ),
inference(eq_res,[status(thm)],[zip_derived_cl9]) ).
thf(zip_derived_cl9725,plain,
! [X0: $i] :
( ( ( sk__1 @ ( s @ e ) @ ( n @ ( n @ ( s @ e ) ) ) )
!= ( s @ X0 ) )
| ( mem @ X0 @ e ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl9713,zip_derived_cl110]) ).
thf(zip_derived_cl7_038,plain,
! [X0: $i] :
~ ( mem @ X0 @ e ),
inference(cnf,[status(esa)],[e_ax]) ).
thf(zip_derived_cl12441,plain,
! [X0: $i] :
( ( sk__1 @ ( s @ e ) @ ( n @ ( n @ ( s @ e ) ) ) )
!= ( s @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl9725,zip_derived_cl7]) ).
thf(zip_derived_cl9691_039,plain,
! [X0: $i] :
( ( e = X0 )
| ~ ( mem @ ( sk__1 @ ( s @ e ) @ ( n @ ( n @ ( s @ e ) ) ) ) @ ( s @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl882,zip_derived_cl8999]) ).
thf(zip_derived_cl110_040,plain,
! [X0: $i] : ( mem @ X0 @ ( s @ X0 ) ),
inference(eq_res,[status(thm)],[zip_derived_cl9]) ).
thf(zip_derived_cl9714,plain,
( e
= ( sk__1 @ ( s @ e ) @ ( n @ ( n @ ( s @ e ) ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl9691,zip_derived_cl110]) ).
thf(zip_derived_cl13326,plain,
! [X0: $i] :
( e
!= ( s @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl12441,zip_derived_cl9714]) ).
thf(zip_derived_cl40122,plain,
( ( s @ ( s @ ( n @ e ) ) )
= ( n @ ( s @ ( n @ e ) ) ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl40121,zip_derived_cl13326]) ).
thf(zip_derived_cl17_041,plain,
! [X0: $i] :
( ( n @ X0 )
= ( a @ X0 @ X0 ) ),
inference(cnf,[status(esa)],[n_def]) ).
thf(zip_derived_cl175_042,plain,
! [X0: $i,X1: $i] : ( mem @ X1 @ ( a @ ( s @ X1 ) @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl16,zip_derived_cl167]) ).
thf(zip_derived_cl199,plain,
! [X0: $i] : ( mem @ X0 @ ( n @ ( s @ X0 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl175]) ).
thf(zip_derived_cl4_043,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( mem @ X0 @ X1 )
| ~ ( mem @ X0 @ X2 )
| ~ ( disj @ X1 @ X2 ) ),
inference(cnf,[status(esa)],[disj_def]) ).
thf(zip_derived_cl209,plain,
! [X0: $i,X1: $i] :
( ~ ( mem @ X0 @ X1 )
| ~ ( disj @ ( n @ ( s @ X0 ) ) @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl199,zip_derived_cl4]) ).
thf(zip_derived_cl41411,plain,
! [X0: $i] :
( ~ ( mem @ ( n @ e ) @ X0 )
| ~ ( disj @ ( s @ ( s @ ( n @ e ) ) ) @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl40122,zip_derived_cl209]) ).
thf(zip_derived_cl41454,plain,
~ ( disj @ ( s @ ( s @ ( n @ e ) ) ) @ ( s @ ( n @ e ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl110,zip_derived_cl41411]) ).
thf(zip_derived_cl882_044,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ( disj @ ( s @ X0 ) @ ( s @ X1 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl876]) ).
thf(zip_derived_cl41535,plain,
( ( s @ ( n @ e ) )
= ( n @ e ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl41454,zip_derived_cl882]) ).
thf(zip_derived_cl4354_045,plain,
! [X0: $i] :
( ( e = X0 )
| ( disj @ ( s @ X0 ) @ ( p @ e ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl4339]) ).
thf(zip_derived_cl42015,plain,
( ( e
= ( n @ e ) )
| ( disj @ ( n @ e ) @ ( p @ e ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl41535,zip_derived_cl4354]) ).
thf(zip_derived_cl9713_046,plain,
! [X0: $i] :
( ( e = X0 )
| ( ( sk__1 @ ( s @ e ) @ ( n @ ( n @ ( s @ e ) ) ) )
!= X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl9691,zip_derived_cl9]) ).
thf(zip_derived_cl17_047,plain,
! [X0: $i] :
( ( n @ X0 )
= ( a @ X0 @ X0 ) ),
inference(cnf,[status(esa)],[n_def]) ).
thf(zip_derived_cl208_048,plain,
! [X0: $i,X1: $i] : ( mem @ X0 @ ( a @ X1 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl201,zip_derived_cl16]) ).
thf(zip_derived_cl500,plain,
! [X0: $i] : ( mem @ X0 @ ( n @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl208]) ).
thf(zip_derived_cl10343,plain,
! [X0: $i] :
( ( ( sk__1 @ ( s @ e ) @ ( n @ ( n @ ( s @ e ) ) ) )
!= ( n @ X0 ) )
| ( mem @ X0 @ e ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl9713,zip_derived_cl500]) ).
thf(zip_derived_cl7_049,plain,
! [X0: $i] :
~ ( mem @ X0 @ e ),
inference(cnf,[status(esa)],[e_ax]) ).
thf(zip_derived_cl12836,plain,
! [X0: $i] :
( ( sk__1 @ ( s @ e ) @ ( n @ ( n @ ( s @ e ) ) ) )
!= ( n @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl10343,zip_derived_cl7]) ).
thf(zip_derived_cl9714_050,plain,
( e
= ( sk__1 @ ( s @ e ) @ ( n @ ( n @ ( s @ e ) ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl9691,zip_derived_cl110]) ).
thf(zip_derived_cl13328,plain,
! [X0: $i] :
( e
!= ( n @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl12836,zip_derived_cl9714]) ).
thf(zip_derived_cl42041,plain,
disj @ ( n @ e ) @ ( p @ e ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl42015,zip_derived_cl13328]) ).
thf(zip_derived_cl17_051,plain,
! [X0: $i] :
( ( n @ X0 )
= ( a @ X0 @ X0 ) ),
inference(cnf,[status(esa)],[n_def]) ).
thf(zip_derived_cl16_052,plain,
! [X0: $i,X1: $i] :
( ( a @ X0 @ X1 )
= ( u @ X0 @ ( s @ X1 ) ) ),
inference(cnf,[status(esa)],[a_def]) ).
thf(zip_derived_cl500_053,plain,
! [X0: $i] : ( mem @ X0 @ ( n @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl208]) ).
thf(zip_derived_cl11_054,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( mem @ X0 @ ( u @ X1 @ X2 ) )
| ~ ( mem @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[u_ax]) ).
thf(zip_derived_cl541,plain,
! [X0: $i,X1: $i] : ( mem @ X0 @ ( u @ ( n @ X0 ) @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl500,zip_derived_cl11]) ).
thf(zip_derived_cl865,plain,
! [X0: $i,X1: $i] : ( mem @ X1 @ ( a @ ( n @ X1 ) @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl16,zip_derived_cl541]) ).
thf(zip_derived_cl261_055,plain,
! [X0: $i,X1: $i] :
( ~ ( mem @ e @ X1 )
| ~ ( disj @ ( p @ X0 ) @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl221,zip_derived_cl4]) ).
thf(zip_derived_cl930,plain,
! [X0: $i,X1: $i] :
~ ( disj @ ( p @ X1 ) @ ( a @ ( n @ e ) @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl865,zip_derived_cl261]) ).
thf(zip_derived_cl942,plain,
! [X0: $i] :
~ ( disj @ ( p @ X0 ) @ ( n @ ( n @ e ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl17,zip_derived_cl930]) ).
thf(zip_derived_cl6_056,plain,
! [X0: $i,X1: $i] :
( ( disj @ X0 @ X1 )
| ( mem @ ( sk__1 @ X1 @ X0 ) @ X0 ) ),
inference(cnf,[status(esa)],[disj_def]) ).
thf(zip_derived_cl106_057,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( disj @ X1 @ X0 )
| ~ ( mem @ ( sk__1 @ X0 @ X1 ) @ X2 )
| ~ ( disj @ X0 @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl5,zip_derived_cl4]) ).
thf(zip_derived_cl662,plain,
! [X0: $i,X1: $i] :
( ( disj @ X0 @ X1 )
| ( disj @ X0 @ X1 )
| ~ ( disj @ X1 @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl6,zip_derived_cl106]) ).
thf(zip_derived_cl664,plain,
! [X0: $i,X1: $i] :
( ~ ( disj @ X1 @ X0 )
| ( disj @ X0 @ X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl662]) ).
thf(zip_derived_cl19915,plain,
! [X0: $i] :
~ ( disj @ ( n @ ( n @ e ) ) @ ( p @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl942,zip_derived_cl664]) ).
thf(zip_derived_cl40122_058,plain,
( ( s @ ( s @ ( n @ e ) ) )
= ( n @ ( s @ ( n @ e ) ) ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl40121,zip_derived_cl13326]) ).
thf(zip_derived_cl41535_059,plain,
( ( s @ ( n @ e ) )
= ( n @ e ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl41454,zip_derived_cl882]) ).
thf(zip_derived_cl41535_060,plain,
( ( s @ ( n @ e ) )
= ( n @ e ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl41454,zip_derived_cl882]) ).
thf(zip_derived_cl41535_061,plain,
( ( s @ ( n @ e ) )
= ( n @ e ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl41454,zip_derived_cl882]) ).
thf(zip_derived_cl41958,plain,
( ( n @ e )
= ( n @ ( n @ e ) ) ),
inference(demod,[status(thm)],[zip_derived_cl40122,zip_derived_cl41535,zip_derived_cl41535,zip_derived_cl41535]) ).
thf(zip_derived_cl42118,plain,
! [X0: $i] :
~ ( disj @ ( n @ e ) @ ( p @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl19915,zip_derived_cl41958]) ).
thf(zip_derived_cl42281,plain,
$false,
inference('s_sup-',[status(thm)],[zip_derived_cl42041,zip_derived_cl42118]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SEV542+1 : TPTP v9.2.0. Released v9.1.0.
% 0.10/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.lsjtaMCc1o true
% 0.14/0.34 % Computer : n028.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 : Wed Oct 1 15:37:38 EDT 2025
% 0.14/0.34 % CPUTime :
% 0.14/0.34 % Running portfolio for 300 s
% 0.14/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.35 % Number of cores: 8
% 0.14/0.35 % Python version: Python 3.6.8
% 0.14/0.35 % Running in FO mode
% 0.51/0.63 % Total configuration time : 435
% 0.51/0.63 % Estimated wc time : 1092
% 0.51/0.63 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.70 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.54/0.70 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.55/0.73 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.55/0.75 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.55/0.75 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.55/0.75 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.55/0.75 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 67.38/10.22 % Solved by fo/fo13.sh.
% 67.38/10.22 % done 7019 iterations in 9.426s
% 67.38/10.22 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 67.38/10.22 % SZS output start Refutation
% See solution above
% 67.38/10.22
% 67.38/10.22
% 67.38/10.22 % Terminating...
% 67.65/10.27 % Runner terminated.
% 67.65/10.28 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------