%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWX217+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.vSKHNCR1cc true
% Computer : n020.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:51 PM UTC 2026
% Result : Theorem 7.83s 1.71s
% Output : Refutation 7.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 20
% Syntax : Number of formulae : 244 ( 168 unt; 0 typ; 0 def)
% Number of atoms : 326 ( 198 equ; 0 cnn)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 1582 ( 46 ~; 79 |; 0 &;1454 @)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 18 ( 16 usr; 5 con; 0-2 aty)
% Number of variables : 161 ( 0 ^; 157 !; 4 ?; 161 :)
% Comments :
%------------------------------------------------------------------------------
thf(nil_type,type,
nil: $i ).
thf(append_type,type,
append: $i > $i > $i ).
thf(rd_type,type,
rd: $i > $i ).
thf(evenNat_type,type,
evenNat: $i > $o ).
thf(x_type,type,
x: $i > $i > $i ).
thf(double_type,type,
double: $i > $i ).
thf(proj1Suc_type,type,
proj1Suc: $i > $i ).
thf(cons_type,type,
cons: $i > $i > $i ).
thf(i_type,type,
i: $i ).
thf(tail_type,type,
tail: $i > $i ).
thf(shw_type,type,
shw: $i > $i ).
thf(half_type,type,
half: $i > $i ).
thf(addNat_type,type,
addNat: $i > $i > $i ).
thf(zero_type,type,
zero: $i ).
thf(o_type,type,
o: $i ).
thf(suc_type,type,
suc: $i > $i ).
thf(axiom_017,axiom,
! [Y: $i] :
( ( addNat @ zero @ Y )
= Y ) ).
thf(zip_derived_cl17,plain,
! [X0: $i] :
( ( addNat @ zero @ X0 )
= X0 ),
inference(cnf,[status(esa)],[axiom_017]) ).
thf(axiom_019,axiom,
! [X: $i] :
( ( double @ X )
= ( addNat @ X @ X ) ) ).
thf(zip_derived_cl19,plain,
! [X0: $i] :
( ( double @ X0 )
= ( addNat @ X0 @ X0 ) ),
inference(cnf,[status(esa)],[axiom_019]) ).
thf(axiom_018,axiom,
! [Y: $i,Z: $i] :
( ( addNat @ ( suc @ Z ) @ Y )
= ( suc @ ( addNat @ Z @ Y ) ) ) ).
thf(zip_derived_cl18,plain,
! [X0: $i,X1: $i] :
( ( addNat @ ( suc @ X0 ) @ X1 )
= ( suc @ ( addNat @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[axiom_018]) ).
thf(zip_derived_cl28,plain,
! [X0: $i] :
( ( double @ ( suc @ X0 ) )
= ( suc @ ( addNat @ X0 @ ( suc @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl19,zip_derived_cl18]) ).
thf(zip_derived_cl58,plain,
( ( double @ ( suc @ zero ) )
= ( suc @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl28]) ).
thf(axiom_009,axiom,
! [N: $i] :
( ( half @ ( suc @ ( suc @ N ) ) )
= ( suc @ ( half @ N ) ) ) ).
thf(zip_derived_cl8,plain,
! [X0: $i] :
( ( half @ ( suc @ ( suc @ X0 ) ) )
= ( suc @ ( half @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_009]) ).
thf(zip_derived_cl76,plain,
( ( half @ ( suc @ ( double @ ( suc @ zero ) ) ) )
= ( suc @ ( half @ ( suc @ zero ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl58,zip_derived_cl8]) ).
thf(axiom_008,axiom,
( ( half @ ( suc @ zero ) )
= zero ) ).
thf(zip_derived_cl7,plain,
( ( half @ ( suc @ zero ) )
= zero ),
inference(cnf,[status(esa)],[axiom_008]) ).
thf(zip_derived_cl92,plain,
( ( half @ ( suc @ ( double @ ( suc @ zero ) ) ) )
= ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl76,zip_derived_cl7]) ).
thf(zip_derived_cl8_001,plain,
! [X0: $i] :
( ( half @ ( suc @ ( suc @ X0 ) ) )
= ( suc @ ( half @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_009]) ).
thf(axiom_014,axiom,
! [Y: $i] :
( ~ ( evenNat @ ( suc @ Y ) )
=> ( ( shw @ ( suc @ Y ) )
= ( cons @ i @ ( shw @ ( half @ ( suc @ Y ) ) ) ) ) ) ).
thf(zip_derived_cl14,plain,
! [X0: $i] :
( ( ( shw @ ( suc @ X0 ) )
= ( cons @ i @ ( shw @ ( half @ ( suc @ X0 ) ) ) ) )
| ( evenNat @ ( suc @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_014]) ).
thf(zip_derived_cl40,plain,
! [X0: $i] :
( ( ( shw @ ( suc @ ( suc @ X0 ) ) )
= ( cons @ i @ ( shw @ ( suc @ ( half @ X0 ) ) ) ) )
| ( evenNat @ ( suc @ ( suc @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl8,zip_derived_cl14]) ).
thf(zip_derived_cl227,plain,
( ( ( shw @ ( suc @ ( suc @ ( suc @ ( double @ ( suc @ zero ) ) ) ) ) )
= ( cons @ i @ ( shw @ ( suc @ ( suc @ zero ) ) ) ) )
| ( evenNat @ ( suc @ ( suc @ ( suc @ ( double @ ( suc @ zero ) ) ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl92,zip_derived_cl40]) ).
thf(zip_derived_cl58_002,plain,
( ( double @ ( suc @ zero ) )
= ( suc @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl28]) ).
thf(zip_derived_cl231,plain,
( ( ( shw @ ( suc @ ( suc @ ( suc @ ( double @ ( suc @ zero ) ) ) ) ) )
= ( cons @ i @ ( shw @ ( double @ ( suc @ zero ) ) ) ) )
| ( evenNat @ ( suc @ ( suc @ ( suc @ ( double @ ( suc @ zero ) ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl227,zip_derived_cl58]) ).
thf(zip_derived_cl58_003,plain,
( ( double @ ( suc @ zero ) )
= ( suc @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl28]) ).
thf(zip_derived_cl28_004,plain,
! [X0: $i] :
( ( double @ ( suc @ X0 ) )
= ( suc @ ( addNat @ X0 @ ( suc @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl19,zip_derived_cl18]) ).
thf(zip_derived_cl82,plain,
( ( double @ ( suc @ ( suc @ zero ) ) )
= ( suc @ ( addNat @ ( suc @ zero ) @ ( double @ ( suc @ zero ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl58,zip_derived_cl28]) ).
thf(zip_derived_cl58_005,plain,
( ( double @ ( suc @ zero ) )
= ( suc @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl28]) ).
thf(zip_derived_cl18_006,plain,
! [X0: $i,X1: $i] :
( ( addNat @ ( suc @ X0 ) @ X1 )
= ( suc @ ( addNat @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[axiom_018]) ).
thf(zip_derived_cl17_007,plain,
! [X0: $i] :
( ( addNat @ zero @ X0 )
= X0 ),
inference(cnf,[status(esa)],[axiom_017]) ).
thf(zip_derived_cl96,plain,
( ( double @ ( double @ ( suc @ zero ) ) )
= ( suc @ ( suc @ ( double @ ( suc @ zero ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl82,zip_derived_cl58,zip_derived_cl18,zip_derived_cl17]) ).
thf(axiom_004,axiom,
! [X: $i] :
( ( proj1Suc @ ( suc @ X ) )
= X ) ).
thf(zip_derived_cl3,plain,
! [X0: $i] :
( ( proj1Suc @ ( suc @ X0 ) )
= X0 ),
inference(cnf,[status(esa)],[axiom_004]) ).
thf(zip_derived_cl254,plain,
( ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) )
= ( suc @ ( double @ ( suc @ zero ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl96,zip_derived_cl3]) ).
thf(zip_derived_cl28_008,plain,
! [X0: $i] :
( ( double @ ( suc @ X0 ) )
= ( suc @ ( addNat @ X0 @ ( suc @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl19,zip_derived_cl18]) ).
thf(zip_derived_cl3_009,plain,
! [X0: $i] :
( ( proj1Suc @ ( suc @ X0 ) )
= X0 ),
inference(cnf,[status(esa)],[axiom_004]) ).
thf(zip_derived_cl46,plain,
! [X0: $i] :
( ( proj1Suc @ ( double @ ( suc @ X0 ) ) )
= ( addNat @ X0 @ ( suc @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl28,zip_derived_cl3]) ).
thf(zip_derived_cl28_010,plain,
! [X0: $i] :
( ( double @ ( suc @ X0 ) )
= ( suc @ ( addNat @ X0 @ ( suc @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl19,zip_derived_cl18]) ).
thf(zip_derived_cl571,plain,
! [X0: $i] :
( ( double @ ( suc @ X0 ) )
= ( suc @ ( proj1Suc @ ( double @ ( suc @ X0 ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl46,zip_derived_cl28]) ).
thf(zip_derived_cl571_011,plain,
! [X0: $i] :
( ( double @ ( suc @ X0 ) )
= ( suc @ ( proj1Suc @ ( double @ ( suc @ X0 ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl46,zip_derived_cl28]) ).
thf(zip_derived_cl669,plain,
! [X0: $i] :
( ( double @ ( suc @ ( proj1Suc @ ( double @ ( suc @ X0 ) ) ) ) )
= ( suc @ ( proj1Suc @ ( double @ ( double @ ( suc @ X0 ) ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl571,zip_derived_cl571]) ).
thf(zip_derived_cl571_012,plain,
! [X0: $i] :
( ( double @ ( suc @ X0 ) )
= ( suc @ ( proj1Suc @ ( double @ ( suc @ X0 ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl46,zip_derived_cl28]) ).
thf(zip_derived_cl675,plain,
! [X0: $i] :
( ( double @ ( double @ ( suc @ X0 ) ) )
= ( suc @ ( proj1Suc @ ( double @ ( double @ ( suc @ X0 ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl669,zip_derived_cl571]) ).
thf(zip_derived_cl254_013,plain,
( ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) )
= ( suc @ ( double @ ( suc @ zero ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl96,zip_derived_cl3]) ).
thf(zip_derived_cl675_014,plain,
! [X0: $i] :
( ( double @ ( double @ ( suc @ X0 ) ) )
= ( suc @ ( proj1Suc @ ( double @ ( double @ ( suc @ X0 ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl669,zip_derived_cl571]) ).
thf(zip_derived_cl5402,plain,
( ( ( shw @ ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) )
= ( cons @ i @ ( shw @ ( double @ ( suc @ zero ) ) ) ) )
| ( evenNat @ ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl231,zip_derived_cl254,zip_derived_cl675,zip_derived_cl254,zip_derived_cl675]) ).
thf(zip_derived_cl7_015,plain,
( ( half @ ( suc @ zero ) )
= zero ),
inference(cnf,[status(esa)],[axiom_008]) ).
thf(zip_derived_cl14_016,plain,
! [X0: $i] :
( ( ( shw @ ( suc @ X0 ) )
= ( cons @ i @ ( shw @ ( half @ ( suc @ X0 ) ) ) ) )
| ( evenNat @ ( suc @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_014]) ).
thf(zip_derived_cl41,plain,
( ( ( shw @ ( suc @ zero ) )
= ( cons @ i @ ( shw @ zero ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl7,zip_derived_cl14]) ).
thf(axiom_012,axiom,
( ( shw @ zero )
= nil ) ).
thf(zip_derived_cl12,plain,
( ( shw @ zero )
= nil ),
inference(cnf,[status(esa)],[axiom_012]) ).
thf(zip_derived_cl42,plain,
( ( ( shw @ ( suc @ zero ) )
= ( cons @ i @ nil ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl41,zip_derived_cl12]) ).
thf(zip_derived_cl58_017,plain,
( ( double @ ( suc @ zero ) )
= ( suc @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl28]) ).
thf(axiom_011,axiom,
! [N: $i] :
( ( evenNat @ ( suc @ N ) )
<=> ~ ( evenNat @ N ) ) ).
thf(zip_derived_cl11,plain,
! [X0: $i] :
( ( evenNat @ ( suc @ X0 ) )
| ( evenNat @ X0 ) ),
inference(cnf,[status(esa)],[axiom_011]) ).
thf(axiom_013,axiom,
! [Y: $i] :
( ( evenNat @ ( suc @ Y ) )
=> ( ( shw @ ( suc @ Y ) )
= ( cons @ o @ ( shw @ ( half @ ( suc @ Y ) ) ) ) ) ) ).
thf(zip_derived_cl13,plain,
! [X0: $i] :
( ( ( shw @ ( suc @ X0 ) )
= ( cons @ o @ ( shw @ ( half @ ( suc @ X0 ) ) ) ) )
| ~ ( evenNat @ ( suc @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_013]) ).
thf(zip_derived_cl27,plain,
! [X0: $i] :
( ( evenNat @ X0 )
| ( ( shw @ ( suc @ X0 ) )
= ( cons @ o @ ( shw @ ( half @ ( suc @ X0 ) ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl11,zip_derived_cl13]) ).
thf(zip_derived_cl122,plain,
( ( ( shw @ ( suc @ ( suc @ zero ) ) )
= ( cons @ o @ ( shw @ ( half @ ( double @ ( suc @ zero ) ) ) ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl58,zip_derived_cl27]) ).
thf(zip_derived_cl58_018,plain,
( ( double @ ( suc @ zero ) )
= ( suc @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl28]) ).
thf(zip_derived_cl58_019,plain,
( ( double @ ( suc @ zero ) )
= ( suc @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl28]) ).
thf(zip_derived_cl8_020,plain,
! [X0: $i] :
( ( half @ ( suc @ ( suc @ X0 ) ) )
= ( suc @ ( half @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_009]) ).
thf(zip_derived_cl91,plain,
( ( half @ ( double @ ( suc @ zero ) ) )
= ( suc @ ( half @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl58,zip_derived_cl8]) ).
thf(axiom_007,axiom,
( ( half @ zero )
= zero ) ).
thf(zip_derived_cl6,plain,
( ( half @ zero )
= zero ),
inference(cnf,[status(esa)],[axiom_007]) ).
thf(zip_derived_cl100,plain,
( ( half @ ( double @ ( suc @ zero ) ) )
= ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl91,zip_derived_cl6]) ).
thf(zip_derived_cl125,plain,
( ( ( shw @ ( double @ ( suc @ zero ) ) )
= ( cons @ o @ ( shw @ ( suc @ zero ) ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl122,zip_derived_cl58,zip_derived_cl100]) ).
thf(zip_derived_cl2323,plain,
( ( ( shw @ ( double @ ( suc @ zero ) ) )
= ( cons @ o @ ( cons @ i @ nil ) ) )
| ( evenNat @ ( suc @ zero ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl42,zip_derived_cl125]) ).
thf(zip_derived_cl2324,plain,
( ( evenNat @ ( suc @ zero ) )
| ( ( shw @ ( double @ ( suc @ zero ) ) )
= ( cons @ o @ ( cons @ i @ nil ) ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl2323]) ).
thf(axiom_022,axiom,
! [Xs: $i] :
( ( rd @ ( cons @ o @ Xs ) )
= ( double @ ( rd @ Xs ) ) ) ).
thf(zip_derived_cl22,plain,
! [X0: $i] :
( ( rd @ ( cons @ o @ X0 ) )
= ( double @ ( rd @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_022]) ).
thf(zip_derived_cl3692,plain,
( ( ( rd @ ( shw @ ( double @ ( suc @ zero ) ) ) )
= ( double @ ( rd @ ( cons @ i @ nil ) ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl2324,zip_derived_cl22]) ).
thf(axiom_021,axiom,
! [Xs: $i] :
( ( rd @ ( cons @ i @ Xs ) )
= ( suc @ ( double @ ( rd @ Xs ) ) ) ) ).
thf(zip_derived_cl21,plain,
! [X0: $i] :
( ( rd @ ( cons @ i @ X0 ) )
= ( suc @ ( double @ ( rd @ X0 ) ) ) ),
inference(cnf,[status(esa)],[axiom_021]) ).
thf(axiom_020,axiom,
( ( rd @ nil )
= zero ) ).
thf(zip_derived_cl20,plain,
( ( rd @ nil )
= zero ),
inference(cnf,[status(esa)],[axiom_020]) ).
thf(zip_derived_cl19_021,plain,
! [X0: $i] :
( ( double @ X0 )
= ( addNat @ X0 @ X0 ) ),
inference(cnf,[status(esa)],[axiom_019]) ).
thf(zip_derived_cl17_022,plain,
! [X0: $i] :
( ( addNat @ zero @ X0 )
= X0 ),
inference(cnf,[status(esa)],[axiom_017]) ).
thf(zip_derived_cl26,plain,
( ( double @ zero )
= zero ),
inference('sup+',[status(thm)],[zip_derived_cl19,zip_derived_cl17]) ).
thf(zip_derived_cl3694,plain,
( ( ( rd @ ( shw @ ( double @ ( suc @ zero ) ) ) )
= ( double @ ( suc @ zero ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3692,zip_derived_cl21,zip_derived_cl20,zip_derived_cl26]) ).
thf(zip_derived_cl12_023,plain,
( ( shw @ zero )
= nil ),
inference(cnf,[status(esa)],[axiom_012]) ).
thf(axiom_023,axiom,
! [X: $i,Y: $i] :
( ( x @ X @ Y )
= ( rd @ ( append @ ( shw @ X ) @ ( shw @ Y ) ) ) ) ).
thf(zip_derived_cl23,plain,
! [X0: $i,X1: $i] :
( ( x @ X0 @ X1 )
= ( rd @ ( append @ ( shw @ X0 ) @ ( shw @ X1 ) ) ) ),
inference(cnf,[status(esa)],[axiom_023]) ).
thf(zip_derived_cl30,plain,
! [X0: $i] :
( ( x @ zero @ X0 )
= ( rd @ ( append @ nil @ ( shw @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl12,zip_derived_cl23]) ).
thf(axiom_015,axiom,
! [Y: $i] :
( ( append @ nil @ Y )
= Y ) ).
thf(zip_derived_cl15,plain,
! [X0: $i] :
( ( append @ nil @ X0 )
= X0 ),
inference(cnf,[status(esa)],[axiom_015]) ).
thf(zip_derived_cl31,plain,
! [X0: $i] :
( ( x @ zero @ X0 )
= ( rd @ ( shw @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl30,zip_derived_cl15]) ).
thf(zip_derived_cl3785,plain,
( ( ( x @ zero @ ( double @ ( suc @ zero ) ) )
= ( double @ ( suc @ zero ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl3694,zip_derived_cl31]) ).
thf(zip_derived_cl254_024,plain,
( ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) )
= ( suc @ ( double @ ( suc @ zero ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl96,zip_derived_cl3]) ).
thf(zip_derived_cl28_025,plain,
! [X0: $i] :
( ( double @ ( suc @ X0 ) )
= ( suc @ ( addNat @ X0 @ ( suc @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl19,zip_derived_cl18]) ).
thf(zip_derived_cl8_026,plain,
! [X0: $i] :
( ( half @ ( suc @ ( suc @ X0 ) ) )
= ( suc @ ( half @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_009]) ).
thf(zip_derived_cl48,plain,
! [X0: $i] :
( ( half @ ( suc @ ( double @ ( suc @ X0 ) ) ) )
= ( suc @ ( half @ ( addNat @ X0 @ ( suc @ X0 ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl28,zip_derived_cl8]) ).
thf(zip_derived_cl10,plain,
! [X0: $i] :
( ~ ( evenNat @ X0 )
| ~ ( evenNat @ ( suc @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_011]) ).
thf(zip_derived_cl713,plain,
! [X0: $i] :
( ~ ( evenNat @ ( half @ ( suc @ ( double @ ( suc @ X0 ) ) ) ) )
| ~ ( evenNat @ ( half @ ( addNat @ X0 @ ( suc @ X0 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl48,zip_derived_cl10]) ).
thf(zip_derived_cl5061,plain,
( ~ ( evenNat @ ( half @ ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) ) )
| ~ ( evenNat @ ( half @ ( addNat @ zero @ ( suc @ zero ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl254,zip_derived_cl713]) ).
thf(zip_derived_cl92_027,plain,
( ( half @ ( suc @ ( double @ ( suc @ zero ) ) ) )
= ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl76,zip_derived_cl7]) ).
thf(zip_derived_cl254_028,plain,
( ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) )
= ( suc @ ( double @ ( suc @ zero ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl96,zip_derived_cl3]) ).
thf(zip_derived_cl315,plain,
( ( half @ ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) )
= ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl92,zip_derived_cl254]) ).
thf(zip_derived_cl17_029,plain,
! [X0: $i] :
( ( addNat @ zero @ X0 )
= X0 ),
inference(cnf,[status(esa)],[axiom_017]) ).
thf(zip_derived_cl7_030,plain,
( ( half @ ( suc @ zero ) )
= zero ),
inference(cnf,[status(esa)],[axiom_008]) ).
thf(axiom_010,axiom,
evenNat @ zero ).
thf(zip_derived_cl9,plain,
evenNat @ zero,
inference(cnf,[status(esa)],[axiom_010]) ).
thf(zip_derived_cl5077,plain,
~ ( evenNat @ ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl5061,zip_derived_cl315,zip_derived_cl17,zip_derived_cl7,zip_derived_cl9]) ).
thf(zip_derived_cl5181,plain,
( ( x @ zero @ ( double @ ( suc @ zero ) ) )
= ( double @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3785,zip_derived_cl5077]) ).
thf(zip_derived_cl42_031,plain,
( ( ( shw @ ( suc @ zero ) )
= ( cons @ i @ nil ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl41,zip_derived_cl12]) ).
thf(zip_derived_cl23_032,plain,
! [X0: $i,X1: $i] :
( ( x @ X0 @ X1 )
= ( rd @ ( append @ ( shw @ X0 ) @ ( shw @ X1 ) ) ) ),
inference(cnf,[status(esa)],[axiom_023]) ).
thf(zip_derived_cl103,plain,
! [X0: $i] :
( ( ( x @ ( suc @ zero ) @ X0 )
= ( rd @ ( append @ ( cons @ i @ nil ) @ ( shw @ X0 ) ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl42,zip_derived_cl23]) ).
thf(axiom_016,axiom,
! [Y: $i,Z: $i,Xs: $i] :
( ( append @ ( cons @ Z @ Xs ) @ Y )
= ( cons @ Z @ ( append @ Xs @ Y ) ) ) ).
thf(zip_derived_cl16,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( append @ ( cons @ X0 @ X1 ) @ X2 )
= ( cons @ X0 @ ( append @ X1 @ X2 ) ) ),
inference(cnf,[status(esa)],[axiom_016]) ).
thf(zip_derived_cl15_033,plain,
! [X0: $i] :
( ( append @ nil @ X0 )
= X0 ),
inference(cnf,[status(esa)],[axiom_015]) ).
thf(zip_derived_cl21_034,plain,
! [X0: $i] :
( ( rd @ ( cons @ i @ X0 ) )
= ( suc @ ( double @ ( rd @ X0 ) ) ) ),
inference(cnf,[status(esa)],[axiom_021]) ).
thf(zip_derived_cl31_035,plain,
! [X0: $i] :
( ( x @ zero @ X0 )
= ( rd @ ( shw @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl30,zip_derived_cl15]) ).
thf(zip_derived_cl109,plain,
! [X0: $i] :
( ( ( x @ ( suc @ zero ) @ X0 )
= ( suc @ ( double @ ( x @ zero @ X0 ) ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl103,zip_derived_cl16,zip_derived_cl15,zip_derived_cl21,zip_derived_cl31]) ).
thf(zip_derived_cl5077_036,plain,
~ ( evenNat @ ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl5061,zip_derived_cl315,zip_derived_cl17,zip_derived_cl7,zip_derived_cl9]) ).
thf(zip_derived_cl5120,plain,
! [X0: $i] :
( ( x @ ( suc @ zero ) @ X0 )
= ( suc @ ( double @ ( x @ zero @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl109,zip_derived_cl5077]) ).
thf(zip_derived_cl5938,plain,
( ( x @ ( suc @ zero ) @ ( double @ ( suc @ zero ) ) )
= ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl5181,zip_derived_cl5120]) ).
thf(zip_derived_cl5120_037,plain,
! [X0: $i] :
( ( x @ ( suc @ zero ) @ X0 )
= ( suc @ ( double @ ( x @ zero @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl109,zip_derived_cl5077]) ).
thf(zip_derived_cl10_038,plain,
! [X0: $i] :
( ~ ( evenNat @ X0 )
| ~ ( evenNat @ ( suc @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_011]) ).
thf(zip_derived_cl5771,plain,
! [X0: $i] :
( ~ ( evenNat @ ( x @ ( suc @ zero ) @ X0 ) )
| ~ ( evenNat @ ( double @ ( x @ zero @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl5120,zip_derived_cl10]) ).
thf(zip_derived_cl7085,plain,
( ~ ( evenNat @ ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) )
| ~ ( evenNat @ ( double @ ( x @ zero @ ( double @ ( suc @ zero ) ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl5938,zip_derived_cl5771]) ).
thf(zip_derived_cl5181_039,plain,
( ( x @ zero @ ( double @ ( suc @ zero ) ) )
= ( double @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3785,zip_derived_cl5077]) ).
thf(zip_derived_cl58_040,plain,
( ( double @ ( suc @ zero ) )
= ( suc @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl28]) ).
thf(zip_derived_cl11_041,plain,
! [X0: $i] :
( ( evenNat @ ( suc @ X0 ) )
| ( evenNat @ X0 ) ),
inference(cnf,[status(esa)],[axiom_011]) ).
thf(zip_derived_cl78,plain,
( ( evenNat @ ( double @ ( suc @ zero ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl58,zip_derived_cl11]) ).
thf(zip_derived_cl571_042,plain,
! [X0: $i] :
( ( double @ ( suc @ X0 ) )
= ( suc @ ( proj1Suc @ ( double @ ( suc @ X0 ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl46,zip_derived_cl28]) ).
thf(zip_derived_cl46_043,plain,
! [X0: $i] :
( ( proj1Suc @ ( double @ ( suc @ X0 ) ) )
= ( addNat @ X0 @ ( suc @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl28,zip_derived_cl3]) ).
thf(zip_derived_cl28_044,plain,
! [X0: $i] :
( ( double @ ( suc @ X0 ) )
= ( suc @ ( addNat @ X0 @ ( suc @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl19,zip_derived_cl18]) ).
thf(zip_derived_cl11_045,plain,
! [X0: $i] :
( ( evenNat @ ( suc @ X0 ) )
| ( evenNat @ X0 ) ),
inference(cnf,[status(esa)],[axiom_011]) ).
thf(zip_derived_cl50,plain,
! [X0: $i] :
( ( evenNat @ ( double @ ( suc @ X0 ) ) )
| ( evenNat @ ( addNat @ X0 @ ( suc @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl28,zip_derived_cl11]) ).
thf(zip_derived_cl572,plain,
! [X0: $i] :
( ( evenNat @ ( proj1Suc @ ( double @ ( suc @ X0 ) ) ) )
| ( evenNat @ ( double @ ( suc @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl46,zip_derived_cl50]) ).
thf(zip_derived_cl832,plain,
! [X0: $i] :
( ( evenNat @ ( proj1Suc @ ( double @ ( double @ ( suc @ X0 ) ) ) ) )
| ( evenNat @ ( double @ ( suc @ ( proj1Suc @ ( double @ ( suc @ X0 ) ) ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl571,zip_derived_cl572]) ).
thf(zip_derived_cl571_046,plain,
! [X0: $i] :
( ( double @ ( suc @ X0 ) )
= ( suc @ ( proj1Suc @ ( double @ ( suc @ X0 ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl46,zip_derived_cl28]) ).
thf(zip_derived_cl839,plain,
! [X0: $i] :
( ( evenNat @ ( proj1Suc @ ( double @ ( double @ ( suc @ X0 ) ) ) ) )
| ( evenNat @ ( double @ ( double @ ( suc @ X0 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl832,zip_derived_cl571]) ).
thf(zip_derived_cl254_047,plain,
( ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) )
= ( suc @ ( double @ ( suc @ zero ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl96,zip_derived_cl3]) ).
thf(zip_derived_cl10_048,plain,
! [X0: $i] :
( ~ ( evenNat @ X0 )
| ~ ( evenNat @ ( suc @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_011]) ).
thf(zip_derived_cl321,plain,
( ~ ( evenNat @ ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) )
| ~ ( evenNat @ ( double @ ( suc @ zero ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl254,zip_derived_cl10]) ).
thf(zip_derived_cl3208,plain,
( ( evenNat @ ( double @ ( double @ ( suc @ zero ) ) ) )
| ~ ( evenNat @ ( double @ ( suc @ zero ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl839,zip_derived_cl321]) ).
thf(zip_derived_cl4850,plain,
( ( evenNat @ ( suc @ zero ) )
| ( evenNat @ ( double @ ( double @ ( suc @ zero ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl78,zip_derived_cl3208]) ).
thf(zip_derived_cl5077_049,plain,
~ ( evenNat @ ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl5061,zip_derived_cl315,zip_derived_cl17,zip_derived_cl7,zip_derived_cl9]) ).
thf(zip_derived_cl5187,plain,
evenNat @ ( double @ ( double @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4850,zip_derived_cl5077]) ).
thf(zip_derived_cl7115,plain,
~ ( evenNat @ ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7085,zip_derived_cl5181,zip_derived_cl5187]) ).
thf(zip_derived_cl7130,plain,
( ( shw @ ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) )
= ( cons @ i @ ( shw @ ( double @ ( suc @ zero ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl5402,zip_derived_cl7115]) ).
thf(axiom_002,axiom,
! [X: $i,X2: $i] :
( ( tail @ ( cons @ X @ X2 ) )
= X2 ) ).
thf(zip_derived_cl1,plain,
! [X0: $i,X1: $i] :
( ( tail @ ( cons @ X1 @ X0 ) )
= X0 ),
inference(cnf,[status(esa)],[axiom_002]) ).
thf(zip_derived_cl7421,plain,
( ( tail @ ( shw @ ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) ) )
= ( shw @ ( double @ ( suc @ zero ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl7130,zip_derived_cl1]) ).
thf(zip_derived_cl14_050,plain,
! [X0: $i] :
( ( ( shw @ ( suc @ X0 ) )
= ( cons @ i @ ( shw @ ( half @ ( suc @ X0 ) ) ) ) )
| ( evenNat @ ( suc @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_014]) ).
thf(zip_derived_cl1_051,plain,
! [X0: $i,X1: $i] :
( ( tail @ ( cons @ X1 @ X0 ) )
= X0 ),
inference(cnf,[status(esa)],[axiom_002]) ).
thf(zip_derived_cl38,plain,
! [X0: $i] :
( ( ( tail @ ( shw @ ( suc @ X0 ) ) )
= ( shw @ ( half @ ( suc @ X0 ) ) ) )
| ( evenNat @ ( suc @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl14,zip_derived_cl1]) ).
thf(zip_derived_cl23_052,plain,
! [X0: $i,X1: $i] :
( ( x @ X0 @ X1 )
= ( rd @ ( append @ ( shw @ X0 ) @ ( shw @ X1 ) ) ) ),
inference(cnf,[status(esa)],[axiom_023]) ).
thf(zip_derived_cl149,plain,
! [X0: $i,X1: $i] :
( ( ( x @ ( half @ ( suc @ X0 ) ) @ X1 )
= ( rd @ ( append @ ( tail @ ( shw @ ( suc @ X0 ) ) ) @ ( shw @ X1 ) ) ) )
| ( evenNat @ ( suc @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl38,zip_derived_cl23]) ).
thf(zip_derived_cl7582,plain,
! [X0: $i] :
( ( ( x @ ( half @ ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) ) @ X0 )
= ( rd @ ( append @ ( shw @ ( double @ ( suc @ zero ) ) ) @ ( shw @ X0 ) ) ) )
| ( evenNat @ ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl7421,zip_derived_cl149]) ).
thf(zip_derived_cl96_053,plain,
( ( double @ ( double @ ( suc @ zero ) ) )
= ( suc @ ( suc @ ( double @ ( suc @ zero ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl82,zip_derived_cl58,zip_derived_cl18,zip_derived_cl17]) ).
thf(zip_derived_cl8_054,plain,
! [X0: $i] :
( ( half @ ( suc @ ( suc @ X0 ) ) )
= ( suc @ ( half @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_009]) ).
thf(zip_derived_cl256,plain,
( ( half @ ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) )
= ( suc @ ( half @ ( suc @ ( double @ ( suc @ zero ) ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl96,zip_derived_cl8]) ).
thf(zip_derived_cl92_055,plain,
( ( half @ ( suc @ ( double @ ( suc @ zero ) ) ) )
= ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl76,zip_derived_cl7]) ).
thf(zip_derived_cl58_056,plain,
( ( double @ ( suc @ zero ) )
= ( suc @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl28]) ).
thf(zip_derived_cl292,plain,
( ( half @ ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) )
= ( double @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl256,zip_derived_cl92,zip_derived_cl58]) ).
thf(zip_derived_cl125_057,plain,
( ( ( shw @ ( double @ ( suc @ zero ) ) )
= ( cons @ o @ ( shw @ ( suc @ zero ) ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl122,zip_derived_cl58,zip_derived_cl100]) ).
thf(zip_derived_cl5077_058,plain,
~ ( evenNat @ ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl5061,zip_derived_cl315,zip_derived_cl17,zip_derived_cl7,zip_derived_cl9]) ).
thf(zip_derived_cl5122,plain,
( ( shw @ ( double @ ( suc @ zero ) ) )
= ( cons @ o @ ( shw @ ( suc @ zero ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl125,zip_derived_cl5077]) ).
thf(zip_derived_cl42_059,plain,
( ( ( shw @ ( suc @ zero ) )
= ( cons @ i @ nil ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl41,zip_derived_cl12]) ).
thf(zip_derived_cl5077_060,plain,
~ ( evenNat @ ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl5061,zip_derived_cl315,zip_derived_cl17,zip_derived_cl7,zip_derived_cl9]) ).
thf(zip_derived_cl5117,plain,
( ( shw @ ( suc @ zero ) )
= ( cons @ i @ nil ) ),
inference(demod,[status(thm)],[zip_derived_cl42,zip_derived_cl5077]) ).
thf(zip_derived_cl6025,plain,
( ( shw @ ( double @ ( suc @ zero ) ) )
= ( cons @ o @ ( cons @ i @ nil ) ) ),
inference(demod,[status(thm)],[zip_derived_cl5122,zip_derived_cl5117]) ).
thf(zip_derived_cl16_061,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( append @ ( cons @ X0 @ X1 ) @ X2 )
= ( cons @ X0 @ ( append @ X1 @ X2 ) ) ),
inference(cnf,[status(esa)],[axiom_016]) ).
thf(zip_derived_cl6028,plain,
! [X0: $i] :
( ( append @ ( shw @ ( double @ ( suc @ zero ) ) ) @ X0 )
= ( cons @ o @ ( append @ ( cons @ i @ nil ) @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl6025,zip_derived_cl16]) ).
thf(zip_derived_cl42_062,plain,
( ( ( shw @ ( suc @ zero ) )
= ( cons @ i @ nil ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl41,zip_derived_cl12]) ).
thf(zip_derived_cl7_063,plain,
( ( half @ ( suc @ zero ) )
= zero ),
inference(cnf,[status(esa)],[axiom_008]) ).
thf(zip_derived_cl14_064,plain,
! [X0: $i] :
( ( ( shw @ ( suc @ X0 ) )
= ( cons @ i @ ( shw @ ( half @ ( suc @ X0 ) ) ) ) )
| ( evenNat @ ( suc @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_014]) ).
thf(zip_derived_cl16_065,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( append @ ( cons @ X0 @ X1 ) @ X2 )
= ( cons @ X0 @ ( append @ X1 @ X2 ) ) ),
inference(cnf,[status(esa)],[axiom_016]) ).
thf(zip_derived_cl69,plain,
! [X0: $i,X1: $i] :
( ( ( append @ ( shw @ ( suc @ X0 ) ) @ X1 )
= ( cons @ i @ ( append @ ( shw @ ( half @ ( suc @ X0 ) ) ) @ X1 ) ) )
| ( evenNat @ ( suc @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl14,zip_derived_cl16]) ).
thf(zip_derived_cl2095,plain,
! [X0: $i] :
( ( ( append @ ( shw @ ( suc @ zero ) ) @ X0 )
= ( cons @ i @ ( append @ ( shw @ zero ) @ X0 ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl7,zip_derived_cl69]) ).
thf(zip_derived_cl12_066,plain,
( ( shw @ zero )
= nil ),
inference(cnf,[status(esa)],[axiom_012]) ).
thf(zip_derived_cl15_067,plain,
! [X0: $i] :
( ( append @ nil @ X0 )
= X0 ),
inference(cnf,[status(esa)],[axiom_015]) ).
thf(zip_derived_cl2110,plain,
! [X0: $i] :
( ( ( append @ ( shw @ ( suc @ zero ) ) @ X0 )
= ( cons @ i @ X0 ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2095,zip_derived_cl12,zip_derived_cl15]) ).
thf(zip_derived_cl2285,plain,
! [X0: $i] :
( ( ( append @ ( cons @ i @ nil ) @ X0 )
= ( cons @ i @ X0 ) )
| ( evenNat @ ( suc @ zero ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl42,zip_derived_cl2110]) ).
thf(zip_derived_cl2286,plain,
! [X0: $i] :
( ( evenNat @ ( suc @ zero ) )
| ( ( append @ ( cons @ i @ nil ) @ X0 )
= ( cons @ i @ X0 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl2285]) ).
thf(zip_derived_cl5077_068,plain,
~ ( evenNat @ ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl5061,zip_derived_cl315,zip_derived_cl17,zip_derived_cl7,zip_derived_cl9]) ).
thf(zip_derived_cl5154,plain,
! [X0: $i] :
( ( append @ ( cons @ i @ nil ) @ X0 )
= ( cons @ i @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2286,zip_derived_cl5077]) ).
thf(zip_derived_cl6031,plain,
! [X0: $i] :
( ( append @ ( shw @ ( double @ ( suc @ zero ) ) ) @ X0 )
= ( cons @ o @ ( cons @ i @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6028,zip_derived_cl5154]) ).
thf(zip_derived_cl22_069,plain,
! [X0: $i] :
( ( rd @ ( cons @ o @ X0 ) )
= ( double @ ( rd @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_022]) ).
thf(zip_derived_cl2110_070,plain,
! [X0: $i] :
( ( ( append @ ( shw @ ( suc @ zero ) ) @ X0 )
= ( cons @ i @ X0 ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2095,zip_derived_cl12,zip_derived_cl15]) ).
thf(zip_derived_cl23_071,plain,
! [X0: $i,X1: $i] :
( ( x @ X0 @ X1 )
= ( rd @ ( append @ ( shw @ X0 ) @ ( shw @ X1 ) ) ) ),
inference(cnf,[status(esa)],[axiom_023]) ).
thf(zip_derived_cl2284,plain,
! [X0: $i] :
( ( ( x @ ( suc @ zero ) @ X0 )
= ( rd @ ( cons @ i @ ( shw @ X0 ) ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl2110,zip_derived_cl23]) ).
thf(zip_derived_cl5077_072,plain,
~ ( evenNat @ ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl5061,zip_derived_cl315,zip_derived_cl17,zip_derived_cl7,zip_derived_cl9]) ).
thf(zip_derived_cl5153,plain,
! [X0: $i] :
( ( x @ ( suc @ zero ) @ X0 )
= ( rd @ ( cons @ i @ ( shw @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2284,zip_derived_cl5077]) ).
thf(zip_derived_cl7115_073,plain,
~ ( evenNat @ ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7085,zip_derived_cl5181,zip_derived_cl5187]) ).
thf(zip_derived_cl7589,plain,
! [X0: $i] :
( ( x @ ( double @ ( suc @ zero ) ) @ X0 )
= ( double @ ( x @ ( suc @ zero ) @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7582,zip_derived_cl292,zip_derived_cl6031,zip_derived_cl22,zip_derived_cl5153,zip_derived_cl7115]) ).
thf(goal_024,conjecture,
? [X: $i,Y: $i] :
( ( x @ X @ Y )
!= ( x @ Y @ X ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ? [X: $i,Y: $i] :
( ( x @ X @ Y )
!= ( x @ Y @ X ) ),
inference('cnf.neg',[status(esa)],[goal_024]) ).
thf(zip_derived_cl24,plain,
! [X0: $i,X1: $i] :
( ( x @ X1 @ X0 )
= ( x @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl24_074,plain,
! [X0: $i,X1: $i] :
( ( x @ X1 @ X0 )
= ( x @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl109_075,plain,
! [X0: $i] :
( ( ( x @ ( suc @ zero ) @ X0 )
= ( suc @ ( double @ ( x @ zero @ X0 ) ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl103,zip_derived_cl16,zip_derived_cl15,zip_derived_cl21,zip_derived_cl31]) ).
thf(zip_derived_cl2072,plain,
! [X0: $i] :
( ( ( x @ ( suc @ zero ) @ X0 )
= ( suc @ ( double @ ( x @ X0 @ zero ) ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl24,zip_derived_cl109]) ).
thf(zip_derived_cl10_076,plain,
! [X0: $i] :
( ~ ( evenNat @ X0 )
| ~ ( evenNat @ ( suc @ X0 ) ) ),
inference(cnf,[status(esa)],[axiom_011]) ).
thf(zip_derived_cl2152,plain,
! [X0: $i] :
( ~ ( evenNat @ ( x @ ( suc @ zero ) @ X0 ) )
| ( evenNat @ ( suc @ zero ) )
| ~ ( evenNat @ ( double @ ( x @ X0 @ zero ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2072,zip_derived_cl10]) ).
thf(zip_derived_cl2379,plain,
! [X0: $i] :
( ~ ( evenNat @ ( x @ X0 @ ( suc @ zero ) ) )
| ~ ( evenNat @ ( double @ ( x @ X0 @ zero ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl24,zip_derived_cl2152]) ).
thf(zip_derived_cl5077_077,plain,
~ ( evenNat @ ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl5061,zip_derived_cl315,zip_derived_cl17,zip_derived_cl7,zip_derived_cl9]) ).
thf(zip_derived_cl5159,plain,
! [X0: $i] :
( ~ ( evenNat @ ( x @ X0 @ ( suc @ zero ) ) )
| ~ ( evenNat @ ( double @ ( x @ X0 @ zero ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2379,zip_derived_cl5077]) ).
thf(zip_derived_cl7630,plain,
( ~ ( evenNat @ ( double @ ( x @ ( suc @ zero ) @ ( suc @ zero ) ) ) )
| ~ ( evenNat @ ( double @ ( x @ ( double @ ( suc @ zero ) ) @ zero ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl7589,zip_derived_cl5159]) ).
thf(zip_derived_cl42_078,plain,
( ( ( shw @ ( suc @ zero ) )
= ( cons @ i @ nil ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl41,zip_derived_cl12]) ).
thf(zip_derived_cl12_079,plain,
( ( shw @ zero )
= nil ),
inference(cnf,[status(esa)],[axiom_012]) ).
thf(zip_derived_cl23_080,plain,
! [X0: $i,X1: $i] :
( ( x @ X0 @ X1 )
= ( rd @ ( append @ ( shw @ X0 ) @ ( shw @ X1 ) ) ) ),
inference(cnf,[status(esa)],[axiom_023]) ).
thf(zip_derived_cl29,plain,
! [X0: $i] :
( ( x @ X0 @ zero )
= ( rd @ ( append @ ( shw @ X0 ) @ nil ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl12,zip_derived_cl23]) ).
thf(zip_derived_cl104,plain,
( ( ( x @ ( suc @ zero ) @ zero )
= ( rd @ ( append @ ( cons @ i @ nil ) @ nil ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl42,zip_derived_cl29]) ).
thf(zip_derived_cl24_081,plain,
! [X0: $i,X1: $i] :
( ( x @ X1 @ X0 )
= ( x @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl16_082,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( append @ ( cons @ X0 @ X1 ) @ X2 )
= ( cons @ X0 @ ( append @ X1 @ X2 ) ) ),
inference(cnf,[status(esa)],[axiom_016]) ).
thf(zip_derived_cl15_083,plain,
! [X0: $i] :
( ( append @ nil @ X0 )
= X0 ),
inference(cnf,[status(esa)],[axiom_015]) ).
thf(zip_derived_cl21_084,plain,
! [X0: $i] :
( ( rd @ ( cons @ i @ X0 ) )
= ( suc @ ( double @ ( rd @ X0 ) ) ) ),
inference(cnf,[status(esa)],[axiom_021]) ).
thf(zip_derived_cl20_085,plain,
( ( rd @ nil )
= zero ),
inference(cnf,[status(esa)],[axiom_020]) ).
thf(zip_derived_cl26_086,plain,
( ( double @ zero )
= zero ),
inference('sup+',[status(thm)],[zip_derived_cl19,zip_derived_cl17]) ).
thf(zip_derived_cl110,plain,
( ( ( x @ zero @ ( suc @ zero ) )
= ( suc @ zero ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl104,zip_derived_cl24,zip_derived_cl16,zip_derived_cl15,zip_derived_cl21,zip_derived_cl20,zip_derived_cl26]) ).
thf(zip_derived_cl109_087,plain,
! [X0: $i] :
( ( ( x @ ( suc @ zero ) @ X0 )
= ( suc @ ( double @ ( x @ zero @ X0 ) ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl103,zip_derived_cl16,zip_derived_cl15,zip_derived_cl21,zip_derived_cl31]) ).
thf(zip_derived_cl2074,plain,
( ( ( x @ ( suc @ zero ) @ ( suc @ zero ) )
= ( suc @ ( double @ ( suc @ zero ) ) ) )
| ( evenNat @ ( suc @ zero ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl110,zip_derived_cl109]) ).
thf(zip_derived_cl254_088,plain,
( ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) )
= ( suc @ ( double @ ( suc @ zero ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl96,zip_derived_cl3]) ).
thf(zip_derived_cl2077,plain,
( ( ( x @ ( suc @ zero ) @ ( suc @ zero ) )
= ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) )
| ( evenNat @ ( suc @ zero ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2074,zip_derived_cl254]) ).
thf(zip_derived_cl2078,plain,
( ( evenNat @ ( suc @ zero ) )
| ( ( x @ ( suc @ zero ) @ ( suc @ zero ) )
= ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl2077]) ).
thf(zip_derived_cl5077_089,plain,
~ ( evenNat @ ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl5061,zip_derived_cl315,zip_derived_cl17,zip_derived_cl7,zip_derived_cl9]) ).
thf(zip_derived_cl5132,plain,
( ( x @ ( suc @ zero ) @ ( suc @ zero ) )
= ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2078,zip_derived_cl5077]) ).
thf(zip_derived_cl58_090,plain,
( ( double @ ( suc @ zero ) )
= ( suc @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl17,zip_derived_cl28]) ).
thf(zip_derived_cl18_091,plain,
! [X0: $i,X1: $i] :
( ( addNat @ ( suc @ X0 ) @ X1 )
= ( suc @ ( addNat @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[axiom_018]) ).
thf(zip_derived_cl81,plain,
! [X0: $i] :
( ( addNat @ ( double @ ( suc @ zero ) ) @ X0 )
= ( suc @ ( addNat @ ( suc @ zero ) @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl58,zip_derived_cl18]) ).
thf(zip_derived_cl18_092,plain,
! [X0: $i,X1: $i] :
( ( addNat @ ( suc @ X0 ) @ X1 )
= ( suc @ ( addNat @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[axiom_018]) ).
thf(zip_derived_cl17_093,plain,
! [X0: $i] :
( ( addNat @ zero @ X0 )
= X0 ),
inference(cnf,[status(esa)],[axiom_017]) ).
thf(zip_derived_cl95,plain,
! [X0: $i] :
( ( addNat @ ( double @ ( suc @ zero ) ) @ X0 )
= ( suc @ ( suc @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl81,zip_derived_cl18,zip_derived_cl17]) ).
thf(zip_derived_cl50_094,plain,
! [X0: $i] :
( ( evenNat @ ( double @ ( suc @ X0 ) ) )
| ( evenNat @ ( addNat @ X0 @ ( suc @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl28,zip_derived_cl11]) ).
thf(zip_derived_cl215,plain,
( ( evenNat @ ( suc @ ( suc @ ( suc @ ( double @ ( suc @ zero ) ) ) ) ) )
| ( evenNat @ ( double @ ( suc @ ( double @ ( suc @ zero ) ) ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl95,zip_derived_cl50]) ).
thf(zip_derived_cl254_095,plain,
( ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) )
= ( suc @ ( double @ ( suc @ zero ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl96,zip_derived_cl3]) ).
thf(zip_derived_cl675_096,plain,
! [X0: $i] :
( ( double @ ( double @ ( suc @ X0 ) ) )
= ( suc @ ( proj1Suc @ ( double @ ( double @ ( suc @ X0 ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl669,zip_derived_cl571]) ).
thf(zip_derived_cl254_097,plain,
( ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) )
= ( suc @ ( double @ ( suc @ zero ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl96,zip_derived_cl3]) ).
thf(zip_derived_cl4846,plain,
( ( evenNat @ ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) )
| ( evenNat @ ( double @ ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl215,zip_derived_cl254,zip_derived_cl675,zip_derived_cl254]) ).
thf(zip_derived_cl7115_098,plain,
~ ( evenNat @ ( suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7085,zip_derived_cl5181,zip_derived_cl5187]) ).
thf(zip_derived_cl7132,plain,
evenNat @ ( double @ ( proj1Suc @ ( double @ ( double @ ( suc @ zero ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl4846,zip_derived_cl7115]) ).
thf(zip_derived_cl7589_099,plain,
! [X0: $i] :
( ( x @ ( double @ ( suc @ zero ) ) @ X0 )
= ( double @ ( x @ ( suc @ zero ) @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7582,zip_derived_cl292,zip_derived_cl6031,zip_derived_cl22,zip_derived_cl5153,zip_derived_cl7115]) ).
thf(zip_derived_cl12_100,plain,
( ( shw @ zero )
= nil ),
inference(cnf,[status(esa)],[axiom_012]) ).
thf(zip_derived_cl31_101,plain,
! [X0: $i] :
( ( x @ zero @ X0 )
= ( rd @ ( shw @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl30,zip_derived_cl15]) ).
thf(zip_derived_cl32,plain,
( ( x @ zero @ zero )
= ( rd @ nil ) ),
inference('sup+',[status(thm)],[zip_derived_cl12,zip_derived_cl31]) ).
thf(zip_derived_cl20_102,plain,
( ( rd @ nil )
= zero ),
inference(cnf,[status(esa)],[axiom_020]) ).
thf(zip_derived_cl33,plain,
( ( x @ zero @ zero )
= zero ),
inference(demod,[status(thm)],[zip_derived_cl32,zip_derived_cl20]) ).
thf(zip_derived_cl109_103,plain,
! [X0: $i] :
( ( ( x @ ( suc @ zero ) @ X0 )
= ( suc @ ( double @ ( x @ zero @ X0 ) ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl103,zip_derived_cl16,zip_derived_cl15,zip_derived_cl21,zip_derived_cl31]) ).
thf(zip_derived_cl2076,plain,
( ( ( x @ ( suc @ zero ) @ zero )
= ( suc @ ( double @ zero ) ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl33,zip_derived_cl109]) ).
thf(zip_derived_cl26_104,plain,
( ( double @ zero )
= zero ),
inference('sup+',[status(thm)],[zip_derived_cl19,zip_derived_cl17]) ).
thf(zip_derived_cl2079,plain,
( ( ( x @ ( suc @ zero ) @ zero )
= ( suc @ zero ) )
| ( evenNat @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2076,zip_derived_cl26]) ).
thf(zip_derived_cl5077_105,plain,
~ ( evenNat @ ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl5061,zip_derived_cl315,zip_derived_cl17,zip_derived_cl7,zip_derived_cl9]) ).
thf(zip_derived_cl5133,plain,
( ( x @ ( suc @ zero ) @ zero )
= ( suc @ zero ) ),
inference(demod,[status(thm)],[zip_derived_cl2079,zip_derived_cl5077]) ).
thf(zip_derived_cl5187_106,plain,
evenNat @ ( double @ ( double @ ( suc @ zero ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4850,zip_derived_cl5077]) ).
thf(zip_derived_cl7658,plain,
$false,
inference(demod,[status(thm)],[zip_derived_cl7630,zip_derived_cl5132,zip_derived_cl7132,zip_derived_cl7589,zip_derived_cl5133,zip_derived_cl5187]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX217+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.vSKHNCR1cc true
% 0.17/0.34 % Computer : n020.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Tue May 5 12:15:49 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 % Running portfolio for 300 s
% 0.17/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.35 % Number of cores: 8
% 0.21/0.35 % Python version: Python 3.6.8
% 0.21/0.35 % Running in FO mode
% 0.55/0.65 % Total configuration time : 435
% 0.55/0.65 % Estimated wc time : 1092
% 0.55/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.56/0.72 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.56/0.74 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.56/0.74 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.56/0.75 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.56/0.76 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.56/0.76 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.56/0.77 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 7.83/1.71 % Solved by fo/fo5.sh.
% 7.83/1.71 % done 1284 iterations in 0.922s
% 7.83/1.71 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 7.83/1.71 % SZS output start Refutation
% See solution above
% 7.83/1.71
% 7.83/1.71
% 7.83/1.71 % Terminating...
% 7.83/1.76 % Runner terminated.
% 7.83/1.76 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------