%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : ALG110+1 : TPTP v9.2.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.9Eecay6lfW true
% Computer : n029.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:27:42 PM UTC 2025
% Result : Theorem 20.07s 3.69s
% Output : Refutation 20.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 50
% Syntax : Number of formulae : 682 ( 400 unt; 0 typ; 0 def)
% Number of atoms : 2006 (1714 equ; 0 cnn)
% Maximal formula atoms : 128 ( 2 avg)
% Number of connectives : 6078 ( 494 ~; 855 |; 437 &;4260 @)
% ( 0 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 48 ( 46 usr; 41 con; 0-2 aty)
% Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
thf(e23_type,type,
e23: $i ).
thf(h2_type,type,
h2: $i > $i ).
thf(zip_tseitin_18_type,type,
zip_tseitin_18: $o ).
thf(zip_tseitin_26_type,type,
zip_tseitin_26: $o ).
thf(zip_tseitin_19_type,type,
zip_tseitin_19: $o ).
thf(zip_tseitin_22_type,type,
zip_tseitin_22: $o ).
thf(zip_tseitin_12_type,type,
zip_tseitin_12: $o ).
thf(h3_type,type,
h3: $i > $i ).
thf(zip_tseitin_25_type,type,
zip_tseitin_25: $o ).
thf(e13_type,type,
e13: $i ).
thf(zip_tseitin_5_type,type,
zip_tseitin_5: $o ).
thf(zip_tseitin_11_type,type,
zip_tseitin_11: $o ).
thf(zip_tseitin_20_type,type,
zip_tseitin_20: $o ).
thf(op2_type,type,
op2: $i > $i > $i ).
thf(zip_tseitin_10_type,type,
zip_tseitin_10: $o ).
thf(e12_type,type,
e12: $i ).
thf(e22_type,type,
e22: $i ).
thf(zip_tseitin_21_type,type,
zip_tseitin_21: $o ).
thf(e21_type,type,
e21: $i ).
thf(e11_type,type,
e11: $i ).
thf(zip_tseitin_28_type,type,
zip_tseitin_28: $o ).
thf(zip_tseitin_0_type,type,
zip_tseitin_0: $o ).
thf(zip_tseitin_15_type,type,
zip_tseitin_15: $o ).
thf(zip_tseitin_24_type,type,
zip_tseitin_24: $o ).
thf(zip_tseitin_30_type,type,
zip_tseitin_30: $o ).
thf(zip_tseitin_17_type,type,
zip_tseitin_17: $o ).
thf(zip_tseitin_29_type,type,
zip_tseitin_29: $o ).
thf(zip_tseitin_14_type,type,
zip_tseitin_14: $o ).
thf(e10_type,type,
e10: $i ).
thf(zip_tseitin_31_type,type,
zip_tseitin_31: $o ).
thf(zip_tseitin_9_type,type,
zip_tseitin_9: $o ).
thf(op1_type,type,
op1: $i > $i > $i ).
thf(zip_tseitin_4_type,type,
zip_tseitin_4: $o ).
thf(zip_tseitin_13_type,type,
zip_tseitin_13: $o ).
thf(zip_tseitin_7_type,type,
zip_tseitin_7: $o ).
thf(h1_type,type,
h1: $i > $i ).
thf(zip_tseitin_27_type,type,
zip_tseitin_27: $o ).
thf(zip_tseitin_23_type,type,
zip_tseitin_23: $o ).
thf(zip_tseitin_1_type,type,
zip_tseitin_1: $o ).
thf(zip_tseitin_2_type,type,
zip_tseitin_2: $o ).
thf(zip_tseitin_8_type,type,
zip_tseitin_8: $o ).
thf(e20_type,type,
e20: $i ).
thf(zip_tseitin_16_type,type,
zip_tseitin_16: $o ).
thf(zip_tseitin_6_type,type,
zip_tseitin_6: $o ).
thf(h4_type,type,
h4: $i > $i ).
thf(zip_tseitin_3_type,type,
zip_tseitin_3: $o ).
thf(co1,conjecture,
( ( ( ( ( h4 @ e13 )
= e23 )
| ( ( h4 @ e12 )
= e23 )
| ( ( h4 @ e11 )
= e23 )
| ( ( h4 @ e10 )
= e23 ) )
& ( ( ( h4 @ e13 )
= e22 )
| ( ( h4 @ e12 )
= e22 )
| ( ( h4 @ e11 )
= e22 )
| ( ( h4 @ e10 )
= e22 ) )
& ( ( ( h4 @ e13 )
= e21 )
| ( ( h4 @ e12 )
= e21 )
| ( ( h4 @ e11 )
= e21 )
| ( ( h4 @ e10 )
= e21 ) )
& ( ( ( h4 @ e13 )
= e20 )
| ( ( h4 @ e12 )
= e20 )
| ( ( h4 @ e11 )
= e20 )
| ( ( h4 @ e10 )
= e20 ) )
& ( ( h4 @ ( op1 @ e13 @ e13 ) )
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e13 ) ) )
& ( ( h4 @ ( op1 @ e13 @ e12 ) )
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e12 ) ) )
& ( ( h4 @ ( op1 @ e13 @ e11 ) )
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e11 ) ) )
& ( ( h4 @ ( op1 @ e13 @ e10 ) )
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e10 ) ) )
& ( ( h4 @ ( op1 @ e12 @ e13 ) )
= ( op2 @ ( h4 @ e12 ) @ ( h4 @ e13 ) ) )
& ( ( h4 @ ( op1 @ e12 @ e12 ) )
= ( op2 @ ( h4 @ e12 ) @ ( h4 @ e12 ) ) )
& ( ( h4 @ ( op1 @ e12 @ e11 ) )
= ( op2 @ ( h4 @ e12 ) @ ( h4 @ e11 ) ) )
& ( ( h4 @ ( op1 @ e12 @ e10 ) )
= ( op2 @ ( h4 @ e12 ) @ ( h4 @ e10 ) ) )
& ( ( h4 @ ( op1 @ e11 @ e13 ) )
= ( op2 @ ( h4 @ e11 ) @ ( h4 @ e13 ) ) )
& ( ( h4 @ ( op1 @ e11 @ e12 ) )
= ( op2 @ ( h4 @ e11 ) @ ( h4 @ e12 ) ) )
& ( ( h4 @ ( op1 @ e11 @ e11 ) )
= ( op2 @ ( h4 @ e11 ) @ ( h4 @ e11 ) ) )
& ( ( h4 @ ( op1 @ e11 @ e10 ) )
= ( op2 @ ( h4 @ e11 ) @ ( h4 @ e10 ) ) )
& ( ( h4 @ ( op1 @ e10 @ e13 ) )
= ( op2 @ ( h4 @ e10 ) @ ( h4 @ e13 ) ) )
& ( ( h4 @ ( op1 @ e10 @ e12 ) )
= ( op2 @ ( h4 @ e10 ) @ ( h4 @ e12 ) ) )
& ( ( h4 @ ( op1 @ e10 @ e11 ) )
= ( op2 @ ( h4 @ e10 ) @ ( h4 @ e11 ) ) )
& ( ( h4 @ ( op1 @ e10 @ e10 ) )
= ( op2 @ ( h4 @ e10 ) @ ( h4 @ e10 ) ) ) )
| ( ( ( ( h3 @ e13 )
= e23 )
| ( ( h3 @ e12 )
= e23 )
| ( ( h3 @ e11 )
= e23 )
| ( ( h3 @ e10 )
= e23 ) )
& ( ( ( h3 @ e13 )
= e22 )
| ( ( h3 @ e12 )
= e22 )
| ( ( h3 @ e11 )
= e22 )
| ( ( h3 @ e10 )
= e22 ) )
& ( ( ( h3 @ e13 )
= e21 )
| ( ( h3 @ e12 )
= e21 )
| ( ( h3 @ e11 )
= e21 )
| ( ( h3 @ e10 )
= e21 ) )
& ( ( ( h3 @ e13 )
= e20 )
| ( ( h3 @ e12 )
= e20 )
| ( ( h3 @ e11 )
= e20 )
| ( ( h3 @ e10 )
= e20 ) )
& ( ( h3 @ ( op1 @ e13 @ e13 ) )
= ( op2 @ ( h3 @ e13 ) @ ( h3 @ e13 ) ) )
& ( ( h3 @ ( op1 @ e13 @ e12 ) )
= ( op2 @ ( h3 @ e13 ) @ ( h3 @ e12 ) ) )
& ( ( h3 @ ( op1 @ e13 @ e11 ) )
= ( op2 @ ( h3 @ e13 ) @ ( h3 @ e11 ) ) )
& ( ( h3 @ ( op1 @ e13 @ e10 ) )
= ( op2 @ ( h3 @ e13 ) @ ( h3 @ e10 ) ) )
& ( ( h3 @ ( op1 @ e12 @ e13 ) )
= ( op2 @ ( h3 @ e12 ) @ ( h3 @ e13 ) ) )
& ( ( h3 @ ( op1 @ e12 @ e12 ) )
= ( op2 @ ( h3 @ e12 ) @ ( h3 @ e12 ) ) )
& ( ( h3 @ ( op1 @ e12 @ e11 ) )
= ( op2 @ ( h3 @ e12 ) @ ( h3 @ e11 ) ) )
& ( ( h3 @ ( op1 @ e12 @ e10 ) )
= ( op2 @ ( h3 @ e12 ) @ ( h3 @ e10 ) ) )
& ( ( h3 @ ( op1 @ e11 @ e13 ) )
= ( op2 @ ( h3 @ e11 ) @ ( h3 @ e13 ) ) )
& ( ( h3 @ ( op1 @ e11 @ e12 ) )
= ( op2 @ ( h3 @ e11 ) @ ( h3 @ e12 ) ) )
& ( ( h3 @ ( op1 @ e11 @ e11 ) )
= ( op2 @ ( h3 @ e11 ) @ ( h3 @ e11 ) ) )
& ( ( h3 @ ( op1 @ e11 @ e10 ) )
= ( op2 @ ( h3 @ e11 ) @ ( h3 @ e10 ) ) )
& ( ( h3 @ ( op1 @ e10 @ e13 ) )
= ( op2 @ ( h3 @ e10 ) @ ( h3 @ e13 ) ) )
& ( ( h3 @ ( op1 @ e10 @ e12 ) )
= ( op2 @ ( h3 @ e10 ) @ ( h3 @ e12 ) ) )
& ( ( h3 @ ( op1 @ e10 @ e11 ) )
= ( op2 @ ( h3 @ e10 ) @ ( h3 @ e11 ) ) )
& ( ( h3 @ ( op1 @ e10 @ e10 ) )
= ( op2 @ ( h3 @ e10 ) @ ( h3 @ e10 ) ) ) )
| ( ( ( ( h2 @ e13 )
= e23 )
| ( ( h2 @ e12 )
= e23 )
| ( ( h2 @ e11 )
= e23 )
| ( ( h2 @ e10 )
= e23 ) )
& ( ( ( h2 @ e13 )
= e22 )
| ( ( h2 @ e12 )
= e22 )
| ( ( h2 @ e11 )
= e22 )
| ( ( h2 @ e10 )
= e22 ) )
& ( ( ( h2 @ e13 )
= e21 )
| ( ( h2 @ e12 )
= e21 )
| ( ( h2 @ e11 )
= e21 )
| ( ( h2 @ e10 )
= e21 ) )
& ( ( ( h2 @ e13 )
= e20 )
| ( ( h2 @ e12 )
= e20 )
| ( ( h2 @ e11 )
= e20 )
| ( ( h2 @ e10 )
= e20 ) )
& ( ( h2 @ ( op1 @ e13 @ e13 ) )
= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e13 ) ) )
& ( ( h2 @ ( op1 @ e13 @ e12 ) )
= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e12 ) ) )
& ( ( h2 @ ( op1 @ e13 @ e11 ) )
= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e11 ) ) )
& ( ( h2 @ ( op1 @ e13 @ e10 ) )
= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e10 ) ) )
& ( ( h2 @ ( op1 @ e12 @ e13 ) )
= ( op2 @ ( h2 @ e12 ) @ ( h2 @ e13 ) ) )
& ( ( h2 @ ( op1 @ e12 @ e12 ) )
= ( op2 @ ( h2 @ e12 ) @ ( h2 @ e12 ) ) )
& ( ( h2 @ ( op1 @ e12 @ e11 ) )
= ( op2 @ ( h2 @ e12 ) @ ( h2 @ e11 ) ) )
& ( ( h2 @ ( op1 @ e12 @ e10 ) )
= ( op2 @ ( h2 @ e12 ) @ ( h2 @ e10 ) ) )
& ( ( h2 @ ( op1 @ e11 @ e13 ) )
= ( op2 @ ( h2 @ e11 ) @ ( h2 @ e13 ) ) )
& ( ( h2 @ ( op1 @ e11 @ e12 ) )
= ( op2 @ ( h2 @ e11 ) @ ( h2 @ e12 ) ) )
& ( ( h2 @ ( op1 @ e11 @ e11 ) )
= ( op2 @ ( h2 @ e11 ) @ ( h2 @ e11 ) ) )
& ( ( h2 @ ( op1 @ e11 @ e10 ) )
= ( op2 @ ( h2 @ e11 ) @ ( h2 @ e10 ) ) )
& ( ( h2 @ ( op1 @ e10 @ e13 ) )
= ( op2 @ ( h2 @ e10 ) @ ( h2 @ e13 ) ) )
& ( ( h2 @ ( op1 @ e10 @ e12 ) )
= ( op2 @ ( h2 @ e10 ) @ ( h2 @ e12 ) ) )
& ( ( h2 @ ( op1 @ e10 @ e11 ) )
= ( op2 @ ( h2 @ e10 ) @ ( h2 @ e11 ) ) )
& ( ( h2 @ ( op1 @ e10 @ e10 ) )
= ( op2 @ ( h2 @ e10 ) @ ( h2 @ e10 ) ) ) )
| ( ( ( ( h1 @ e13 )
= e23 )
| ( ( h1 @ e12 )
= e23 )
| ( ( h1 @ e11 )
= e23 )
| ( ( h1 @ e10 )
= e23 ) )
& ( ( ( h1 @ e13 )
= e22 )
| ( ( h1 @ e12 )
= e22 )
| ( ( h1 @ e11 )
= e22 )
| ( ( h1 @ e10 )
= e22 ) )
& ( ( ( h1 @ e13 )
= e21 )
| ( ( h1 @ e12 )
= e21 )
| ( ( h1 @ e11 )
= e21 )
| ( ( h1 @ e10 )
= e21 ) )
& ( ( ( h1 @ e13 )
= e20 )
| ( ( h1 @ e12 )
= e20 )
| ( ( h1 @ e11 )
= e20 )
| ( ( h1 @ e10 )
= e20 ) )
& ( ( h1 @ ( op1 @ e13 @ e13 ) )
= ( op2 @ ( h1 @ e13 ) @ ( h1 @ e13 ) ) )
& ( ( h1 @ ( op1 @ e13 @ e12 ) )
= ( op2 @ ( h1 @ e13 ) @ ( h1 @ e12 ) ) )
& ( ( h1 @ ( op1 @ e13 @ e11 ) )
= ( op2 @ ( h1 @ e13 ) @ ( h1 @ e11 ) ) )
& ( ( h1 @ ( op1 @ e13 @ e10 ) )
= ( op2 @ ( h1 @ e13 ) @ ( h1 @ e10 ) ) )
& ( ( h1 @ ( op1 @ e12 @ e13 ) )
= ( op2 @ ( h1 @ e12 ) @ ( h1 @ e13 ) ) )
& ( ( h1 @ ( op1 @ e12 @ e12 ) )
= ( op2 @ ( h1 @ e12 ) @ ( h1 @ e12 ) ) )
& ( ( h1 @ ( op1 @ e12 @ e11 ) )
= ( op2 @ ( h1 @ e12 ) @ ( h1 @ e11 ) ) )
& ( ( h1 @ ( op1 @ e12 @ e10 ) )
= ( op2 @ ( h1 @ e12 ) @ ( h1 @ e10 ) ) )
& ( ( h1 @ ( op1 @ e11 @ e13 ) )
= ( op2 @ ( h1 @ e11 ) @ ( h1 @ e13 ) ) )
& ( ( h1 @ ( op1 @ e11 @ e12 ) )
= ( op2 @ ( h1 @ e11 ) @ ( h1 @ e12 ) ) )
& ( ( h1 @ ( op1 @ e11 @ e11 ) )
= ( op2 @ ( h1 @ e11 ) @ ( h1 @ e11 ) ) )
& ( ( h1 @ ( op1 @ e11 @ e10 ) )
= ( op2 @ ( h1 @ e11 ) @ ( h1 @ e10 ) ) )
& ( ( h1 @ ( op1 @ e10 @ e13 ) )
= ( op2 @ ( h1 @ e10 ) @ ( h1 @ e13 ) ) )
& ( ( h1 @ ( op1 @ e10 @ e12 ) )
= ( op2 @ ( h1 @ e10 ) @ ( h1 @ e12 ) ) )
& ( ( h1 @ ( op1 @ e10 @ e11 ) )
= ( op2 @ ( h1 @ e10 ) @ ( h1 @ e11 ) ) )
& ( ( h1 @ ( op1 @ e10 @ e10 ) )
= ( op2 @ ( h1 @ e10 ) @ ( h1 @ e10 ) ) ) ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ( ( ( ( ( h4 @ e13 )
= e23 )
| ( ( h4 @ e12 )
= e23 )
| ( ( h4 @ e11 )
= e23 )
| ( ( h4 @ e10 )
= e23 ) )
& ( ( ( h4 @ e13 )
= e22 )
| ( ( h4 @ e12 )
= e22 )
| ( ( h4 @ e11 )
= e22 )
| ( ( h4 @ e10 )
= e22 ) )
& ( ( ( h4 @ e13 )
= e21 )
| ( ( h4 @ e12 )
= e21 )
| ( ( h4 @ e11 )
= e21 )
| ( ( h4 @ e10 )
= e21 ) )
& ( ( ( h4 @ e13 )
= e20 )
| ( ( h4 @ e12 )
= e20 )
| ( ( h4 @ e11 )
= e20 )
| ( ( h4 @ e10 )
= e20 ) )
& ( ( h4 @ ( op1 @ e13 @ e13 ) )
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e13 ) ) )
& ( ( h4 @ ( op1 @ e13 @ e12 ) )
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e12 ) ) )
& ( ( h4 @ ( op1 @ e13 @ e11 ) )
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e11 ) ) )
& ( ( h4 @ ( op1 @ e13 @ e10 ) )
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e10 ) ) )
& ( ( h4 @ ( op1 @ e12 @ e13 ) )
= ( op2 @ ( h4 @ e12 ) @ ( h4 @ e13 ) ) )
& ( ( h4 @ ( op1 @ e12 @ e12 ) )
= ( op2 @ ( h4 @ e12 ) @ ( h4 @ e12 ) ) )
& ( ( h4 @ ( op1 @ e12 @ e11 ) )
= ( op2 @ ( h4 @ e12 ) @ ( h4 @ e11 ) ) )
& ( ( h4 @ ( op1 @ e12 @ e10 ) )
= ( op2 @ ( h4 @ e12 ) @ ( h4 @ e10 ) ) )
& ( ( h4 @ ( op1 @ e11 @ e13 ) )
= ( op2 @ ( h4 @ e11 ) @ ( h4 @ e13 ) ) )
& ( ( h4 @ ( op1 @ e11 @ e12 ) )
= ( op2 @ ( h4 @ e11 ) @ ( h4 @ e12 ) ) )
& ( ( h4 @ ( op1 @ e11 @ e11 ) )
= ( op2 @ ( h4 @ e11 ) @ ( h4 @ e11 ) ) )
& ( ( h4 @ ( op1 @ e11 @ e10 ) )
= ( op2 @ ( h4 @ e11 ) @ ( h4 @ e10 ) ) )
& ( ( h4 @ ( op1 @ e10 @ e13 ) )
= ( op2 @ ( h4 @ e10 ) @ ( h4 @ e13 ) ) )
& ( ( h4 @ ( op1 @ e10 @ e12 ) )
= ( op2 @ ( h4 @ e10 ) @ ( h4 @ e12 ) ) )
& ( ( h4 @ ( op1 @ e10 @ e11 ) )
= ( op2 @ ( h4 @ e10 ) @ ( h4 @ e11 ) ) )
& ( ( h4 @ ( op1 @ e10 @ e10 ) )
= ( op2 @ ( h4 @ e10 ) @ ( h4 @ e10 ) ) ) )
| ( ( ( ( h3 @ e13 )
= e23 )
| ( ( h3 @ e12 )
= e23 )
| ( ( h3 @ e11 )
= e23 )
| ( ( h3 @ e10 )
= e23 ) )
& ( ( ( h3 @ e13 )
= e22 )
| ( ( h3 @ e12 )
= e22 )
| ( ( h3 @ e11 )
= e22 )
| ( ( h3 @ e10 )
= e22 ) )
& ( ( ( h3 @ e13 )
= e21 )
| ( ( h3 @ e12 )
= e21 )
| ( ( h3 @ e11 )
= e21 )
| ( ( h3 @ e10 )
= e21 ) )
& ( ( ( h3 @ e13 )
= e20 )
| ( ( h3 @ e12 )
= e20 )
| ( ( h3 @ e11 )
= e20 )
| ( ( h3 @ e10 )
= e20 ) )
& ( ( h3 @ ( op1 @ e13 @ e13 ) )
= ( op2 @ ( h3 @ e13 ) @ ( h3 @ e13 ) ) )
& ( ( h3 @ ( op1 @ e13 @ e12 ) )
= ( op2 @ ( h3 @ e13 ) @ ( h3 @ e12 ) ) )
& ( ( h3 @ ( op1 @ e13 @ e11 ) )
= ( op2 @ ( h3 @ e13 ) @ ( h3 @ e11 ) ) )
& ( ( h3 @ ( op1 @ e13 @ e10 ) )
= ( op2 @ ( h3 @ e13 ) @ ( h3 @ e10 ) ) )
& ( ( h3 @ ( op1 @ e12 @ e13 ) )
= ( op2 @ ( h3 @ e12 ) @ ( h3 @ e13 ) ) )
& ( ( h3 @ ( op1 @ e12 @ e12 ) )
= ( op2 @ ( h3 @ e12 ) @ ( h3 @ e12 ) ) )
& ( ( h3 @ ( op1 @ e12 @ e11 ) )
= ( op2 @ ( h3 @ e12 ) @ ( h3 @ e11 ) ) )
& ( ( h3 @ ( op1 @ e12 @ e10 ) )
= ( op2 @ ( h3 @ e12 ) @ ( h3 @ e10 ) ) )
& ( ( h3 @ ( op1 @ e11 @ e13 ) )
= ( op2 @ ( h3 @ e11 ) @ ( h3 @ e13 ) ) )
& ( ( h3 @ ( op1 @ e11 @ e12 ) )
= ( op2 @ ( h3 @ e11 ) @ ( h3 @ e12 ) ) )
& ( ( h3 @ ( op1 @ e11 @ e11 ) )
= ( op2 @ ( h3 @ e11 ) @ ( h3 @ e11 ) ) )
& ( ( h3 @ ( op1 @ e11 @ e10 ) )
= ( op2 @ ( h3 @ e11 ) @ ( h3 @ e10 ) ) )
& ( ( h3 @ ( op1 @ e10 @ e13 ) )
= ( op2 @ ( h3 @ e10 ) @ ( h3 @ e13 ) ) )
& ( ( h3 @ ( op1 @ e10 @ e12 ) )
= ( op2 @ ( h3 @ e10 ) @ ( h3 @ e12 ) ) )
& ( ( h3 @ ( op1 @ e10 @ e11 ) )
= ( op2 @ ( h3 @ e10 ) @ ( h3 @ e11 ) ) )
& ( ( h3 @ ( op1 @ e10 @ e10 ) )
= ( op2 @ ( h3 @ e10 ) @ ( h3 @ e10 ) ) ) )
| ( ( ( ( h2 @ e13 )
= e23 )
| ( ( h2 @ e12 )
= e23 )
| ( ( h2 @ e11 )
= e23 )
| ( ( h2 @ e10 )
= e23 ) )
& ( ( ( h2 @ e13 )
= e22 )
| ( ( h2 @ e12 )
= e22 )
| ( ( h2 @ e11 )
= e22 )
| ( ( h2 @ e10 )
= e22 ) )
& ( ( ( h2 @ e13 )
= e21 )
| ( ( h2 @ e12 )
= e21 )
| ( ( h2 @ e11 )
= e21 )
| ( ( h2 @ e10 )
= e21 ) )
& ( ( ( h2 @ e13 )
= e20 )
| ( ( h2 @ e12 )
= e20 )
| ( ( h2 @ e11 )
= e20 )
| ( ( h2 @ e10 )
= e20 ) )
& ( ( h2 @ ( op1 @ e13 @ e13 ) )
= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e13 ) ) )
& ( ( h2 @ ( op1 @ e13 @ e12 ) )
= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e12 ) ) )
& ( ( h2 @ ( op1 @ e13 @ e11 ) )
= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e11 ) ) )
& ( ( h2 @ ( op1 @ e13 @ e10 ) )
= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e10 ) ) )
& ( ( h2 @ ( op1 @ e12 @ e13 ) )
= ( op2 @ ( h2 @ e12 ) @ ( h2 @ e13 ) ) )
& ( ( h2 @ ( op1 @ e12 @ e12 ) )
= ( op2 @ ( h2 @ e12 ) @ ( h2 @ e12 ) ) )
& ( ( h2 @ ( op1 @ e12 @ e11 ) )
= ( op2 @ ( h2 @ e12 ) @ ( h2 @ e11 ) ) )
& ( ( h2 @ ( op1 @ e12 @ e10 ) )
= ( op2 @ ( h2 @ e12 ) @ ( h2 @ e10 ) ) )
& ( ( h2 @ ( op1 @ e11 @ e13 ) )
= ( op2 @ ( h2 @ e11 ) @ ( h2 @ e13 ) ) )
& ( ( h2 @ ( op1 @ e11 @ e12 ) )
= ( op2 @ ( h2 @ e11 ) @ ( h2 @ e12 ) ) )
& ( ( h2 @ ( op1 @ e11 @ e11 ) )
= ( op2 @ ( h2 @ e11 ) @ ( h2 @ e11 ) ) )
& ( ( h2 @ ( op1 @ e11 @ e10 ) )
= ( op2 @ ( h2 @ e11 ) @ ( h2 @ e10 ) ) )
& ( ( h2 @ ( op1 @ e10 @ e13 ) )
= ( op2 @ ( h2 @ e10 ) @ ( h2 @ e13 ) ) )
& ( ( h2 @ ( op1 @ e10 @ e12 ) )
= ( op2 @ ( h2 @ e10 ) @ ( h2 @ e12 ) ) )
& ( ( h2 @ ( op1 @ e10 @ e11 ) )
= ( op2 @ ( h2 @ e10 ) @ ( h2 @ e11 ) ) )
& ( ( h2 @ ( op1 @ e10 @ e10 ) )
= ( op2 @ ( h2 @ e10 ) @ ( h2 @ e10 ) ) ) )
| ( ( ( ( h1 @ e13 )
= e23 )
| ( ( h1 @ e12 )
= e23 )
| ( ( h1 @ e11 )
= e23 )
| ( ( h1 @ e10 )
= e23 ) )
& ( ( ( h1 @ e13 )
= e22 )
| ( ( h1 @ e12 )
= e22 )
| ( ( h1 @ e11 )
= e22 )
| ( ( h1 @ e10 )
= e22 ) )
& ( ( ( h1 @ e13 )
= e21 )
| ( ( h1 @ e12 )
= e21 )
| ( ( h1 @ e11 )
= e21 )
| ( ( h1 @ e10 )
= e21 ) )
& ( ( ( h1 @ e13 )
= e20 )
| ( ( h1 @ e12 )
= e20 )
| ( ( h1 @ e11 )
= e20 )
| ( ( h1 @ e10 )
= e20 ) )
& ( ( h1 @ ( op1 @ e13 @ e13 ) )
= ( op2 @ ( h1 @ e13 ) @ ( h1 @ e13 ) ) )
& ( ( h1 @ ( op1 @ e13 @ e12 ) )
= ( op2 @ ( h1 @ e13 ) @ ( h1 @ e12 ) ) )
& ( ( h1 @ ( op1 @ e13 @ e11 ) )
= ( op2 @ ( h1 @ e13 ) @ ( h1 @ e11 ) ) )
& ( ( h1 @ ( op1 @ e13 @ e10 ) )
= ( op2 @ ( h1 @ e13 ) @ ( h1 @ e10 ) ) )
& ( ( h1 @ ( op1 @ e12 @ e13 ) )
= ( op2 @ ( h1 @ e12 ) @ ( h1 @ e13 ) ) )
& ( ( h1 @ ( op1 @ e12 @ e12 ) )
= ( op2 @ ( h1 @ e12 ) @ ( h1 @ e12 ) ) )
& ( ( h1 @ ( op1 @ e12 @ e11 ) )
= ( op2 @ ( h1 @ e12 ) @ ( h1 @ e11 ) ) )
& ( ( h1 @ ( op1 @ e12 @ e10 ) )
= ( op2 @ ( h1 @ e12 ) @ ( h1 @ e10 ) ) )
& ( ( h1 @ ( op1 @ e11 @ e13 ) )
= ( op2 @ ( h1 @ e11 ) @ ( h1 @ e13 ) ) )
& ( ( h1 @ ( op1 @ e11 @ e12 ) )
= ( op2 @ ( h1 @ e11 ) @ ( h1 @ e12 ) ) )
& ( ( h1 @ ( op1 @ e11 @ e11 ) )
= ( op2 @ ( h1 @ e11 ) @ ( h1 @ e11 ) ) )
& ( ( h1 @ ( op1 @ e11 @ e10 ) )
= ( op2 @ ( h1 @ e11 ) @ ( h1 @ e10 ) ) )
& ( ( h1 @ ( op1 @ e10 @ e13 ) )
= ( op2 @ ( h1 @ e10 ) @ ( h1 @ e13 ) ) )
& ( ( h1 @ ( op1 @ e10 @ e12 ) )
= ( op2 @ ( h1 @ e10 ) @ ( h1 @ e12 ) ) )
& ( ( h1 @ ( op1 @ e10 @ e11 ) )
= ( op2 @ ( h1 @ e10 ) @ ( h1 @ e11 ) ) )
& ( ( h1 @ ( op1 @ e10 @ e10 ) )
= ( op2 @ ( h1 @ e10 ) @ ( h1 @ e10 ) ) ) ) ),
inference('cnf.neg',[status(esa)],[co1]) ).
thf(zip_derived_cl785,plain,
( ( ( h2 @ e10 )
!= e23 )
| ( ( h2 @ e11 )
!= e22 )
| ( ( h2 @ e12 )
!= e21 )
| ( ( h2 @ e13 )
!= e20 )
| ( ( h2 @ ( op1 @ e13 @ e13 ) )
!= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e13 ) ) )
| ( ( h2 @ ( op1 @ e13 @ e12 ) )
!= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e12 ) ) )
| ( ( h2 @ ( op1 @ e13 @ e11 ) )
!= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e11 ) ) )
| ( ( h2 @ ( op1 @ e13 @ e10 ) )
!= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e10 ) ) )
| ( ( h2 @ ( op1 @ e12 @ e13 ) )
!= ( op2 @ ( h2 @ e12 ) @ ( h2 @ e13 ) ) )
| ( ( h2 @ ( op1 @ e12 @ e12 ) )
!= ( op2 @ ( h2 @ e12 ) @ ( h2 @ e12 ) ) )
| ( ( h2 @ ( op1 @ e12 @ e11 ) )
!= ( op2 @ ( h2 @ e12 ) @ ( h2 @ e11 ) ) )
| ( ( h2 @ ( op1 @ e12 @ e10 ) )
!= ( op2 @ ( h2 @ e12 ) @ ( h2 @ e10 ) ) )
| ( ( h2 @ ( op1 @ e11 @ e13 ) )
!= ( op2 @ ( h2 @ e11 ) @ ( h2 @ e13 ) ) )
| ( ( h2 @ ( op1 @ e11 @ e12 ) )
!= ( op2 @ ( h2 @ e11 ) @ ( h2 @ e12 ) ) )
| ( ( h2 @ ( op1 @ e11 @ e11 ) )
!= ( op2 @ ( h2 @ e11 ) @ ( h2 @ e11 ) ) )
| ( ( h2 @ ( op1 @ e11 @ e10 ) )
!= ( op2 @ ( h2 @ e11 ) @ ( h2 @ e10 ) ) )
| ( ( h2 @ ( op1 @ e10 @ e13 ) )
!= ( op2 @ ( h2 @ e10 ) @ ( h2 @ e13 ) ) )
| ( ( h2 @ ( op1 @ e10 @ e12 ) )
!= ( op2 @ ( h2 @ e10 ) @ ( h2 @ e12 ) ) )
| ( ( h2 @ ( op1 @ e10 @ e11 ) )
!= ( op2 @ ( h2 @ e10 ) @ ( h2 @ e11 ) ) )
| ( ( h2 @ ( op1 @ e10 @ e10 ) )
!= ( op2 @ ( h2 @ e10 ) @ ( h2 @ e10 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(ax15,axiom,
( ( ( h2 @ e13 )
= ( op2 @ e21 @ e21 ) )
& ( ( h2 @ e11 )
= ( op2 @ ( op2 @ ( op2 @ e21 @ e21 ) @ ( op2 @ e21 @ e21 ) ) @ ( op2 @ e21 @ e21 ) ) )
& ( ( h2 @ e10 )
= ( op2 @ ( op2 @ e21 @ e21 ) @ ( op2 @ e21 @ e21 ) ) )
& ( ( h2 @ e12 )
= e21 ) ) ).
thf(zip_derived_cl304,plain,
( ( h2 @ e10 )
= ( op2 @ ( op2 @ e21 @ e21 ) @ ( op2 @ e21 @ e21 ) ) ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl302,plain,
( ( h2 @ e13 )
= ( op2 @ e21 @ e21 ) ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl302_001,plain,
( ( h2 @ e13 )
= ( op2 @ e21 @ e21 ) ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl2002,plain,
( ( h2 @ e10 )
= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl304,zip_derived_cl302,zip_derived_cl302]) ).
thf(ax4,axiom,
( ( ( ( op2 @ e23 @ e23 )
= e23 )
| ( ( op2 @ e22 @ e23 )
= e23 )
| ( ( op2 @ e21 @ e23 )
= e23 )
| ( ( op2 @ e20 @ e23 )
= e23 ) )
& ( ( ( op2 @ e23 @ e23 )
= e23 )
| ( ( op2 @ e23 @ e22 )
= e23 )
| ( ( op2 @ e23 @ e21 )
= e23 )
| ( ( op2 @ e23 @ e20 )
= e23 ) )
& ( ( ( op2 @ e23 @ e23 )
= e22 )
| ( ( op2 @ e22 @ e23 )
= e22 )
| ( ( op2 @ e21 @ e23 )
= e22 )
| ( ( op2 @ e20 @ e23 )
= e22 ) )
& ( ( ( op2 @ e23 @ e23 )
= e22 )
| ( ( op2 @ e23 @ e22 )
= e22 )
| ( ( op2 @ e23 @ e21 )
= e22 )
| ( ( op2 @ e23 @ e20 )
= e22 ) )
& ( ( ( op2 @ e23 @ e23 )
= e21 )
| ( ( op2 @ e22 @ e23 )
= e21 )
| ( ( op2 @ e21 @ e23 )
= e21 )
| ( ( op2 @ e20 @ e23 )
= e21 ) )
& ( ( ( op2 @ e23 @ e23 )
= e21 )
| ( ( op2 @ e23 @ e22 )
= e21 )
| ( ( op2 @ e23 @ e21 )
= e21 )
| ( ( op2 @ e23 @ e20 )
= e21 ) )
& ( ( ( op2 @ e23 @ e23 )
= e20 )
| ( ( op2 @ e22 @ e23 )
= e20 )
| ( ( op2 @ e21 @ e23 )
= e20 )
| ( ( op2 @ e20 @ e23 )
= e20 ) )
& ( ( ( op2 @ e23 @ e23 )
= e20 )
| ( ( op2 @ e23 @ e22 )
= e20 )
| ( ( op2 @ e23 @ e21 )
= e20 )
| ( ( op2 @ e23 @ e20 )
= e20 ) )
& ( ( ( op2 @ e23 @ e22 )
= e23 )
| ( ( op2 @ e22 @ e22 )
= e23 )
| ( ( op2 @ e21 @ e22 )
= e23 )
| ( ( op2 @ e20 @ e22 )
= e23 ) )
& ( ( ( op2 @ e22 @ e23 )
= e23 )
| ( ( op2 @ e22 @ e22 )
= e23 )
| ( ( op2 @ e22 @ e21 )
= e23 )
| ( ( op2 @ e22 @ e20 )
= e23 ) )
& ( ( ( op2 @ e23 @ e22 )
= e22 )
| ( ( op2 @ e22 @ e22 )
= e22 )
| ( ( op2 @ e21 @ e22 )
= e22 )
| ( ( op2 @ e20 @ e22 )
= e22 ) )
& ( ( ( op2 @ e22 @ e23 )
= e22 )
| ( ( op2 @ e22 @ e22 )
= e22 )
| ( ( op2 @ e22 @ e21 )
= e22 )
| ( ( op2 @ e22 @ e20 )
= e22 ) )
& ( ( ( op2 @ e23 @ e22 )
= e21 )
| ( ( op2 @ e22 @ e22 )
= e21 )
| ( ( op2 @ e21 @ e22 )
= e21 )
| ( ( op2 @ e20 @ e22 )
= e21 ) )
& ( ( ( op2 @ e22 @ e23 )
= e21 )
| ( ( op2 @ e22 @ e22 )
= e21 )
| ( ( op2 @ e22 @ e21 )
= e21 )
| ( ( op2 @ e22 @ e20 )
= e21 ) )
& ( ( ( op2 @ e23 @ e22 )
= e20 )
| ( ( op2 @ e22 @ e22 )
= e20 )
| ( ( op2 @ e21 @ e22 )
= e20 )
| ( ( op2 @ e20 @ e22 )
= e20 ) )
& ( ( ( op2 @ e22 @ e23 )
= e20 )
| ( ( op2 @ e22 @ e22 )
= e20 )
| ( ( op2 @ e22 @ e21 )
= e20 )
| ( ( op2 @ e22 @ e20 )
= e20 ) )
& ( ( ( op2 @ e23 @ e21 )
= e23 )
| ( ( op2 @ e22 @ e21 )
= e23 )
| ( ( op2 @ e21 @ e21 )
= e23 )
| ( ( op2 @ e20 @ e21 )
= e23 ) )
& ( ( ( op2 @ e21 @ e23 )
= e23 )
| ( ( op2 @ e21 @ e22 )
= e23 )
| ( ( op2 @ e21 @ e21 )
= e23 )
| ( ( op2 @ e21 @ e20 )
= e23 ) )
& ( ( ( op2 @ e23 @ e21 )
= e22 )
| ( ( op2 @ e22 @ e21 )
= e22 )
| ( ( op2 @ e21 @ e21 )
= e22 )
| ( ( op2 @ e20 @ e21 )
= e22 ) )
& ( ( ( op2 @ e21 @ e23 )
= e22 )
| ( ( op2 @ e21 @ e22 )
= e22 )
| ( ( op2 @ e21 @ e21 )
= e22 )
| ( ( op2 @ e21 @ e20 )
= e22 ) )
& ( ( ( op2 @ e23 @ e21 )
= e21 )
| ( ( op2 @ e22 @ e21 )
= e21 )
| ( ( op2 @ e21 @ e21 )
= e21 )
| ( ( op2 @ e20 @ e21 )
= e21 ) )
& ( ( ( op2 @ e21 @ e23 )
= e21 )
| ( ( op2 @ e21 @ e22 )
= e21 )
| ( ( op2 @ e21 @ e21 )
= e21 )
| ( ( op2 @ e21 @ e20 )
= e21 ) )
& ( ( ( op2 @ e23 @ e21 )
= e20 )
| ( ( op2 @ e22 @ e21 )
= e20 )
| ( ( op2 @ e21 @ e21 )
= e20 )
| ( ( op2 @ e20 @ e21 )
= e20 ) )
& ( ( ( op2 @ e21 @ e23 )
= e20 )
| ( ( op2 @ e21 @ e22 )
= e20 )
| ( ( op2 @ e21 @ e21 )
= e20 )
| ( ( op2 @ e21 @ e20 )
= e20 ) )
& ( ( ( op2 @ e23 @ e20 )
= e23 )
| ( ( op2 @ e22 @ e20 )
= e23 )
| ( ( op2 @ e21 @ e20 )
= e23 )
| ( ( op2 @ e20 @ e20 )
= e23 ) )
& ( ( ( op2 @ e20 @ e23 )
= e23 )
| ( ( op2 @ e20 @ e22 )
= e23 )
| ( ( op2 @ e20 @ e21 )
= e23 )
| ( ( op2 @ e20 @ e20 )
= e23 ) )
& ( ( ( op2 @ e23 @ e20 )
= e22 )
| ( ( op2 @ e22 @ e20 )
= e22 )
| ( ( op2 @ e21 @ e20 )
= e22 )
| ( ( op2 @ e20 @ e20 )
= e22 ) )
& ( ( ( op2 @ e20 @ e23 )
= e22 )
| ( ( op2 @ e20 @ e22 )
= e22 )
| ( ( op2 @ e20 @ e21 )
= e22 )
| ( ( op2 @ e20 @ e20 )
= e22 ) )
& ( ( ( op2 @ e23 @ e20 )
= e21 )
| ( ( op2 @ e22 @ e20 )
= e21 )
| ( ( op2 @ e21 @ e20 )
= e21 )
| ( ( op2 @ e20 @ e20 )
= e21 ) )
& ( ( ( op2 @ e20 @ e23 )
= e21 )
| ( ( op2 @ e20 @ e22 )
= e21 )
| ( ( op2 @ e20 @ e21 )
= e21 )
| ( ( op2 @ e20 @ e20 )
= e21 ) )
& ( ( ( op2 @ e23 @ e20 )
= e20 )
| ( ( op2 @ e22 @ e20 )
= e20 )
| ( ( op2 @ e21 @ e20 )
= e20 )
| ( ( op2 @ e20 @ e20 )
= e20 ) )
& ( ( ( op2 @ e20 @ e23 )
= e20 )
| ( ( op2 @ e20 @ e22 )
= e20 )
| ( ( op2 @ e20 @ e21 )
= e20 )
| ( ( op2 @ e20 @ e20 )
= e20 ) ) ) ).
thf(zip_derived_cl86,plain,
( ( ( op2 @ e23 @ e21 )
= e20 )
| ( ( op2 @ e22 @ e21 )
= e20 )
| ( ( op2 @ e21 @ e21 )
= e20 )
| ( ( op2 @ e20 @ e21 )
= e20 ) ),
inference(cnf,[status(esa)],[ax4]) ).
thf(ax13,axiom,
( ( e23
= ( op2 @ e22 @ e22 ) )
& ( e21
= ( op2 @ ( op2 @ ( op2 @ e22 @ e22 ) @ ( op2 @ e22 @ e22 ) ) @ ( op2 @ e22 @ e22 ) ) )
& ( e20
= ( op2 @ ( op2 @ e22 @ e22 ) @ ( op2 @ e22 @ e22 ) ) ) ) ).
thf(zip_derived_cl297,plain,
( e20
= ( op2 @ ( op2 @ e22 @ e22 ) @ ( op2 @ e22 @ e22 ) ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl295,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl295_002,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(ax17,axiom,
( ( ( h4 @ e13 )
= ( op2 @ e23 @ e23 ) )
& ( ( h4 @ e11 )
= ( op2 @ ( op2 @ ( op2 @ e23 @ e23 ) @ ( op2 @ e23 @ e23 ) ) @ ( op2 @ e23 @ e23 ) ) )
& ( ( h4 @ e10 )
= ( op2 @ ( op2 @ e23 @ e23 ) @ ( op2 @ e23 @ e23 ) ) )
& ( ( h4 @ e12 )
= e23 ) ) ).
thf(zip_derived_cl310,plain,
( ( h4 @ e13 )
= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl1756,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_003,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl302_004,plain,
( ( h2 @ e13 )
= ( op2 @ e21 @ e21 ) ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl1756_005,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_006,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_007,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl2858,plain,
( ( ( op2 @ e23 @ e21 )
= ( h4 @ e13 ) )
| ( ( op2 @ e22 @ e21 )
= ( h4 @ e13 ) )
| ( ( h2 @ e13 )
= ( h4 @ e13 ) )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl86,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl302,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl1756]) ).
thf(ax6,axiom,
( ( ( op2 @ e23 @ e22 )
!= ( op2 @ e23 @ e23 ) )
& ( ( op2 @ e23 @ e21 )
!= ( op2 @ e23 @ e23 ) )
& ( ( op2 @ e23 @ e21 )
!= ( op2 @ e23 @ e22 ) )
& ( ( op2 @ e23 @ e20 )
!= ( op2 @ e23 @ e23 ) )
& ( ( op2 @ e23 @ e20 )
!= ( op2 @ e23 @ e22 ) )
& ( ( op2 @ e23 @ e20 )
!= ( op2 @ e23 @ e21 ) )
& ( ( op2 @ e22 @ e22 )
!= ( op2 @ e22 @ e23 ) )
& ( ( op2 @ e22 @ e21 )
!= ( op2 @ e22 @ e23 ) )
& ( ( op2 @ e22 @ e21 )
!= ( op2 @ e22 @ e22 ) )
& ( ( op2 @ e22 @ e20 )
!= ( op2 @ e22 @ e23 ) )
& ( ( op2 @ e22 @ e20 )
!= ( op2 @ e22 @ e22 ) )
& ( ( op2 @ e22 @ e20 )
!= ( op2 @ e22 @ e21 ) )
& ( ( op2 @ e21 @ e22 )
!= ( op2 @ e21 @ e23 ) )
& ( ( op2 @ e21 @ e21 )
!= ( op2 @ e21 @ e23 ) )
& ( ( op2 @ e21 @ e21 )
!= ( op2 @ e21 @ e22 ) )
& ( ( op2 @ e21 @ e20 )
!= ( op2 @ e21 @ e23 ) )
& ( ( op2 @ e21 @ e20 )
!= ( op2 @ e21 @ e22 ) )
& ( ( op2 @ e21 @ e20 )
!= ( op2 @ e21 @ e21 ) )
& ( ( op2 @ e20 @ e22 )
!= ( op2 @ e20 @ e23 ) )
& ( ( op2 @ e20 @ e21 )
!= ( op2 @ e20 @ e23 ) )
& ( ( op2 @ e20 @ e21 )
!= ( op2 @ e20 @ e22 ) )
& ( ( op2 @ e20 @ e20 )
!= ( op2 @ e20 @ e23 ) )
& ( ( op2 @ e20 @ e20 )
!= ( op2 @ e20 @ e22 ) )
& ( ( op2 @ e20 @ e20 )
!= ( op2 @ e20 @ e21 ) )
& ( ( op2 @ e22 @ e23 )
!= ( op2 @ e23 @ e23 ) )
& ( ( op2 @ e21 @ e23 )
!= ( op2 @ e23 @ e23 ) )
& ( ( op2 @ e21 @ e23 )
!= ( op2 @ e22 @ e23 ) )
& ( ( op2 @ e20 @ e23 )
!= ( op2 @ e23 @ e23 ) )
& ( ( op2 @ e20 @ e23 )
!= ( op2 @ e22 @ e23 ) )
& ( ( op2 @ e20 @ e23 )
!= ( op2 @ e21 @ e23 ) )
& ( ( op2 @ e22 @ e22 )
!= ( op2 @ e23 @ e22 ) )
& ( ( op2 @ e21 @ e22 )
!= ( op2 @ e23 @ e22 ) )
& ( ( op2 @ e21 @ e22 )
!= ( op2 @ e22 @ e22 ) )
& ( ( op2 @ e20 @ e22 )
!= ( op2 @ e23 @ e22 ) )
& ( ( op2 @ e20 @ e22 )
!= ( op2 @ e22 @ e22 ) )
& ( ( op2 @ e20 @ e22 )
!= ( op2 @ e21 @ e22 ) )
& ( ( op2 @ e22 @ e21 )
!= ( op2 @ e23 @ e21 ) )
& ( ( op2 @ e21 @ e21 )
!= ( op2 @ e23 @ e21 ) )
& ( ( op2 @ e21 @ e21 )
!= ( op2 @ e22 @ e21 ) )
& ( ( op2 @ e20 @ e21 )
!= ( op2 @ e23 @ e21 ) )
& ( ( op2 @ e20 @ e21 )
!= ( op2 @ e22 @ e21 ) )
& ( ( op2 @ e20 @ e21 )
!= ( op2 @ e21 @ e21 ) )
& ( ( op2 @ e22 @ e20 )
!= ( op2 @ e23 @ e20 ) )
& ( ( op2 @ e21 @ e20 )
!= ( op2 @ e23 @ e20 ) )
& ( ( op2 @ e21 @ e20 )
!= ( op2 @ e22 @ e20 ) )
& ( ( op2 @ e20 @ e20 )
!= ( op2 @ e23 @ e20 ) )
& ( ( op2 @ e20 @ e20 )
!= ( op2 @ e22 @ e20 ) )
& ( ( op2 @ e20 @ e20 )
!= ( op2 @ e21 @ e20 ) ) ) ).
thf(zip_derived_cl145,plain,
( ( op2 @ e23 @ e21 )
!= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl310_008,plain,
( ( h4 @ e13 )
= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl1668,plain,
( ( op2 @ e23 @ e21 )
!= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl145,zip_derived_cl310]) ).
thf(zip_derived_cl2859,plain,
( ( ( op2 @ e22 @ e21 )
= ( h4 @ e13 ) )
| ( ( h2 @ e13 )
= ( h4 @ e13 ) )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= ( h4 @ e13 ) ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2858,zip_derived_cl1668]) ).
thf(zip_derived_cl77,plain,
( ( ( op2 @ e22 @ e23 )
= e21 )
| ( ( op2 @ e22 @ e22 )
= e21 )
| ( ( op2 @ e22 @ e21 )
= e21 )
| ( ( op2 @ e22 @ e20 )
= e21 ) ),
inference(cnf,[status(esa)],[ax4]) ).
thf(ax3,axiom,
( ( ( ( op2 @ e23 @ e23 )
= e23 )
| ( ( op2 @ e23 @ e23 )
= e22 )
| ( ( op2 @ e23 @ e23 )
= e21 )
| ( ( op2 @ e23 @ e23 )
= e20 ) )
& ( ( ( op2 @ e23 @ e22 )
= e23 )
| ( ( op2 @ e23 @ e22 )
= e22 )
| ( ( op2 @ e23 @ e22 )
= e21 )
| ( ( op2 @ e23 @ e22 )
= e20 ) )
& ( ( ( op2 @ e23 @ e21 )
= e23 )
| ( ( op2 @ e23 @ e21 )
= e22 )
| ( ( op2 @ e23 @ e21 )
= e21 )
| ( ( op2 @ e23 @ e21 )
= e20 ) )
& ( ( ( op2 @ e23 @ e20 )
= e23 )
| ( ( op2 @ e23 @ e20 )
= e22 )
| ( ( op2 @ e23 @ e20 )
= e21 )
| ( ( op2 @ e23 @ e20 )
= e20 ) )
& ( ( ( op2 @ e22 @ e23 )
= e23 )
| ( ( op2 @ e22 @ e23 )
= e22 )
| ( ( op2 @ e22 @ e23 )
= e21 )
| ( ( op2 @ e22 @ e23 )
= e20 ) )
& ( ( ( op2 @ e22 @ e22 )
= e23 )
| ( ( op2 @ e22 @ e22 )
= e22 )
| ( ( op2 @ e22 @ e22 )
= e21 )
| ( ( op2 @ e22 @ e22 )
= e20 ) )
& ( ( ( op2 @ e22 @ e21 )
= e23 )
| ( ( op2 @ e22 @ e21 )
= e22 )
| ( ( op2 @ e22 @ e21 )
= e21 )
| ( ( op2 @ e22 @ e21 )
= e20 ) )
& ( ( ( op2 @ e22 @ e20 )
= e23 )
| ( ( op2 @ e22 @ e20 )
= e22 )
| ( ( op2 @ e22 @ e20 )
= e21 )
| ( ( op2 @ e22 @ e20 )
= e20 ) )
& ( ( ( op2 @ e21 @ e23 )
= e23 )
| ( ( op2 @ e21 @ e23 )
= e22 )
| ( ( op2 @ e21 @ e23 )
= e21 )
| ( ( op2 @ e21 @ e23 )
= e20 ) )
& ( ( ( op2 @ e21 @ e22 )
= e23 )
| ( ( op2 @ e21 @ e22 )
= e22 )
| ( ( op2 @ e21 @ e22 )
= e21 )
| ( ( op2 @ e21 @ e22 )
= e20 ) )
& ( ( ( op2 @ e21 @ e21 )
= e23 )
| ( ( op2 @ e21 @ e21 )
= e22 )
| ( ( op2 @ e21 @ e21 )
= e21 )
| ( ( op2 @ e21 @ e21 )
= e20 ) )
& ( ( ( op2 @ e21 @ e20 )
= e23 )
| ( ( op2 @ e21 @ e20 )
= e22 )
| ( ( op2 @ e21 @ e20 )
= e21 )
| ( ( op2 @ e21 @ e20 )
= e20 ) )
& ( ( ( op2 @ e20 @ e23 )
= e23 )
| ( ( op2 @ e20 @ e23 )
= e22 )
| ( ( op2 @ e20 @ e23 )
= e21 )
| ( ( op2 @ e20 @ e23 )
= e20 ) )
& ( ( ( op2 @ e20 @ e22 )
= e23 )
| ( ( op2 @ e20 @ e22 )
= e22 )
| ( ( op2 @ e20 @ e22 )
= e21 )
| ( ( op2 @ e20 @ e22 )
= e20 ) )
& ( ( ( op2 @ e20 @ e21 )
= e23 )
| ( ( op2 @ e20 @ e21 )
= e22 )
| ( ( op2 @ e20 @ e21 )
= e21 )
| ( ( op2 @ e20 @ e21 )
= e20 ) )
& ( ( ( op2 @ e20 @ e20 )
= e23 )
| ( ( op2 @ e20 @ e20 )
= e22 )
| ( ( op2 @ e20 @ e20 )
= e21 )
| ( ( op2 @ e20 @ e20 )
= e20 ) ) ) ).
thf(zip_derived_cl52,plain,
( ( ( op2 @ e22 @ e23 )
= e23 )
| ( ( op2 @ e22 @ e23 )
= e22 )
| ( ( op2 @ e22 @ e23 )
= e21 )
| ( ( op2 @ e22 @ e23 )
= e20 ) ),
inference(cnf,[status(esa)],[ax3]) ).
thf(zip_derived_cl1756_009,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl2414,plain,
( ( ( op2 @ e22 @ e23 )
= e23 )
| ( ( op2 @ e22 @ e23 )
= e22 )
| ( ( op2 @ e22 @ e23 )
= e21 )
| ( ( op2 @ e22 @ e23 )
= ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl52,zip_derived_cl1756]) ).
thf(zip_derived_cl168,plain,
( ( op2 @ e22 @ e23 )
!= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl310_010,plain,
( ( h4 @ e13 )
= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl1670,plain,
( ( op2 @ e22 @ e23 )
!= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl168,zip_derived_cl310]) ).
thf(zip_derived_cl150,plain,
( ( op2 @ e22 @ e22 )
!= ( op2 @ e22 @ e23 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl295_011,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl1493,plain,
( e23
!= ( op2 @ e22 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl150,zip_derived_cl295]) ).
thf(zip_derived_cl2415,plain,
( ( ( op2 @ e22 @ e23 )
= e22 )
| ( ( op2 @ e22 @ e23 )
= e21 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2414,zip_derived_cl1670,zip_derived_cl1493]) ).
thf(ax11,axiom,
( ( ( ( ( op2 @ e20 @ e20 )
= e20 )
& ( ( op2 @ e20 @ e20 )
!= e20 ) )
| ( ( ( op2 @ e21 @ e20 )
= e21 )
& ( ( op2 @ e20 @ e21 )
!= e20 ) )
| ( ( ( op2 @ e22 @ e20 )
= e22 )
& ( ( op2 @ e20 @ e22 )
!= e20 ) )
| ( ( ( op2 @ e23 @ e20 )
= e23 )
& ( ( op2 @ e20 @ e23 )
!= e20 ) ) )
& ( ( ( ( op2 @ e20 @ e21 )
= e20 )
& ( ( op2 @ e21 @ e20 )
!= e21 ) )
| ( ( ( op2 @ e21 @ e21 )
= e21 )
& ( ( op2 @ e21 @ e21 )
!= e21 ) )
| ( ( ( op2 @ e22 @ e21 )
= e22 )
& ( ( op2 @ e21 @ e22 )
!= e21 ) )
| ( ( ( op2 @ e23 @ e21 )
= e23 )
& ( ( op2 @ e21 @ e23 )
!= e21 ) ) )
& ( ( ( ( op2 @ e20 @ e22 )
= e20 )
& ( ( op2 @ e22 @ e20 )
!= e22 ) )
| ( ( ( op2 @ e21 @ e22 )
= e21 )
& ( ( op2 @ e22 @ e21 )
!= e22 ) )
| ( ( ( op2 @ e22 @ e22 )
= e22 )
& ( ( op2 @ e22 @ e22 )
!= e22 ) )
| ( ( ( op2 @ e23 @ e22 )
= e23 )
& ( ( op2 @ e22 @ e23 )
!= e22 ) ) )
& ( ( ( ( op2 @ e20 @ e23 )
= e20 )
& ( ( op2 @ e23 @ e20 )
!= e23 ) )
| ( ( ( op2 @ e21 @ e23 )
= e21 )
& ( ( op2 @ e23 @ e21 )
!= e23 ) )
| ( ( ( op2 @ e22 @ e23 )
= e22 )
& ( ( op2 @ e23 @ e22 )
!= e23 ) )
| ( ( ( op2 @ e23 @ e23 )
= e23 )
& ( ( op2 @ e23 @ e23 )
!= e23 ) ) ) ) ).
thf(zf_stmt_1,type,
zip_tseitin_31: $o ).
thf(zf_stmt_2,axiom,
( zip_tseitin_31
=> ( ( ( op2 @ e23 @ e23 )
!= e23 )
& ( ( op2 @ e23 @ e23 )
= e23 ) ) ) ).
thf(zf_stmt_3,type,
zip_tseitin_30: $o ).
thf(zf_stmt_4,axiom,
( zip_tseitin_30
=> ( ( ( op2 @ e23 @ e22 )
!= e23 )
& ( ( op2 @ e22 @ e23 )
= e22 ) ) ) ).
thf(zf_stmt_5,type,
zip_tseitin_29: $o ).
thf(zf_stmt_6,axiom,
( zip_tseitin_29
=> ( ( ( op2 @ e23 @ e21 )
!= e23 )
& ( ( op2 @ e21 @ e23 )
= e21 ) ) ) ).
thf(zf_stmt_7,type,
zip_tseitin_28: $o ).
thf(zf_stmt_8,axiom,
( zip_tseitin_28
=> ( ( ( op2 @ e23 @ e20 )
!= e23 )
& ( ( op2 @ e20 @ e23 )
= e20 ) ) ) ).
thf(zf_stmt_9,type,
zip_tseitin_27: $o ).
thf(zf_stmt_10,axiom,
( zip_tseitin_27
=> ( ( ( op2 @ e22 @ e23 )
!= e22 )
& ( ( op2 @ e23 @ e22 )
= e23 ) ) ) ).
thf(zf_stmt_11,type,
zip_tseitin_26: $o ).
thf(zf_stmt_12,axiom,
( zip_tseitin_26
=> ( ( ( op2 @ e22 @ e22 )
!= e22 )
& ( ( op2 @ e22 @ e22 )
= e22 ) ) ) ).
thf(zf_stmt_13,type,
zip_tseitin_25: $o ).
thf(zf_stmt_14,axiom,
( zip_tseitin_25
=> ( ( ( op2 @ e22 @ e21 )
!= e22 )
& ( ( op2 @ e21 @ e22 )
= e21 ) ) ) ).
thf(zf_stmt_15,type,
zip_tseitin_24: $o ).
thf(zf_stmt_16,axiom,
( zip_tseitin_24
=> ( ( ( op2 @ e22 @ e20 )
!= e22 )
& ( ( op2 @ e20 @ e22 )
= e20 ) ) ) ).
thf(zf_stmt_17,type,
zip_tseitin_23: $o ).
thf(zf_stmt_18,axiom,
( zip_tseitin_23
=> ( ( ( op2 @ e21 @ e23 )
!= e21 )
& ( ( op2 @ e23 @ e21 )
= e23 ) ) ) ).
thf(zf_stmt_19,type,
zip_tseitin_22: $o ).
thf(zf_stmt_20,axiom,
( zip_tseitin_22
=> ( ( ( op2 @ e21 @ e22 )
!= e21 )
& ( ( op2 @ e22 @ e21 )
= e22 ) ) ) ).
thf(zf_stmt_21,type,
zip_tseitin_21: $o ).
thf(zf_stmt_22,axiom,
( zip_tseitin_21
=> ( ( ( op2 @ e21 @ e21 )
!= e21 )
& ( ( op2 @ e21 @ e21 )
= e21 ) ) ) ).
thf(zf_stmt_23,type,
zip_tseitin_20: $o ).
thf(zf_stmt_24,axiom,
( zip_tseitin_20
=> ( ( ( op2 @ e21 @ e20 )
!= e21 )
& ( ( op2 @ e20 @ e21 )
= e20 ) ) ) ).
thf(zf_stmt_25,type,
zip_tseitin_19: $o ).
thf(zf_stmt_26,axiom,
( zip_tseitin_19
=> ( ( ( op2 @ e20 @ e23 )
!= e20 )
& ( ( op2 @ e23 @ e20 )
= e23 ) ) ) ).
thf(zf_stmt_27,type,
zip_tseitin_18: $o ).
thf(zf_stmt_28,axiom,
( zip_tseitin_18
=> ( ( ( op2 @ e20 @ e22 )
!= e20 )
& ( ( op2 @ e22 @ e20 )
= e22 ) ) ) ).
thf(zf_stmt_29,type,
zip_tseitin_17: $o ).
thf(zf_stmt_30,axiom,
( zip_tseitin_17
=> ( ( ( op2 @ e20 @ e21 )
!= e20 )
& ( ( op2 @ e21 @ e20 )
= e21 ) ) ) ).
thf(zf_stmt_31,type,
zip_tseitin_16: $o ).
thf(zf_stmt_32,axiom,
( zip_tseitin_16
=> ( ( ( op2 @ e20 @ e20 )
!= e20 )
& ( ( op2 @ e20 @ e20 )
= e20 ) ) ) ).
thf(zf_stmt_33,axiom,
( ( zip_tseitin_31
| zip_tseitin_30
| zip_tseitin_29
| zip_tseitin_28 )
& ( zip_tseitin_27
| zip_tseitin_26
| zip_tseitin_25
| zip_tseitin_24 )
& ( zip_tseitin_23
| zip_tseitin_22
| zip_tseitin_21
| zip_tseitin_20 )
& ( zip_tseitin_19
| zip_tseitin_18
| zip_tseitin_17
| zip_tseitin_16 ) ) ).
thf(zip_derived_cl288,plain,
( zip_tseitin_31
| zip_tseitin_30
| zip_tseitin_29
| zip_tseitin_28 ),
inference(cnf,[status(esa)],[zf_stmt_33]) ).
thf(zip_derived_cl287,plain,
( ( ( op2 @ e23 @ e23 )
= e23 )
| ~ zip_tseitin_31 ),
inference(cnf,[status(esa)],[zf_stmt_2]) ).
thf(zip_derived_cl286,plain,
( ( ( op2 @ e23 @ e23 )
!= e23 )
| ~ zip_tseitin_31 ),
inference(cnf,[status(esa)],[zf_stmt_2]) ).
thf(zip_derived_cl1603,plain,
~ zip_tseitin_31,
inference(clc,[status(thm)],[zip_derived_cl287,zip_derived_cl286]) ).
thf(zip_derived_cl1604,plain,
( zip_tseitin_30
| zip_tseitin_29
| zip_tseitin_28 ),
inference(demod,[status(thm)],[zip_derived_cl288,zip_derived_cl1603]) ).
thf(zip_derived_cl281,plain,
( ( ( op2 @ e20 @ e23 )
= e20 )
| ~ zip_tseitin_28 ),
inference(cnf,[status(esa)],[zf_stmt_8]) ).
thf(zip_derived_cl171,plain,
( ( op2 @ e20 @ e23 )
!= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1575,plain,
( ( e20
!= ( op2 @ e23 @ e23 ) )
| ~ zip_tseitin_28 ),
inference('sup-',[status(thm)],[zip_derived_cl281,zip_derived_cl171]) ).
thf(zip_derived_cl310_012,plain,
( ( h4 @ e13 )
= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl1675,plain,
( ( e20
!= ( h4 @ e13 ) )
| ~ zip_tseitin_28 ),
inference(demod,[status(thm)],[zip_derived_cl1575,zip_derived_cl310]) ).
thf(zip_derived_cl1682,plain,
( zip_tseitin_29
| zip_tseitin_30
| ( e20
!= ( h4 @ e13 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl1604,zip_derived_cl1675]) ).
thf(zip_derived_cl1756_013,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1845,plain,
( zip_tseitin_29
| zip_tseitin_30
| ( ( h4 @ e13 )
!= ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1682,zip_derived_cl1756]) ).
thf(zip_derived_cl1846,plain,
( zip_tseitin_30
| zip_tseitin_29 ),
inference(simplify,[status(thm)],[zip_derived_cl1845]) ).
thf(zip_derived_cl283,plain,
( ( ( op2 @ e21 @ e23 )
= e21 )
| ~ zip_tseitin_29 ),
inference(cnf,[status(esa)],[zf_stmt_6]) ).
thf(zip_derived_cl170,plain,
( ( op2 @ e21 @ e23 )
!= ( op2 @ e22 @ e23 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1601,plain,
( ( e21
!= ( op2 @ e22 @ e23 ) )
| ~ zip_tseitin_29 ),
inference('sup-',[status(thm)],[zip_derived_cl283,zip_derived_cl170]) ).
thf(zip_derived_cl1865,plain,
( zip_tseitin_30
| ( e21
!= ( op2 @ e22 @ e23 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl1846,zip_derived_cl1601]) ).
thf(zip_derived_cl2420,plain,
( ( e21 != e21 )
| ( ( op2 @ e22 @ e23 )
= e22 )
| zip_tseitin_30 ),
inference('sup-',[status(thm)],[zip_derived_cl2415,zip_derived_cl1865]) ).
thf(zip_derived_cl2423,plain,
( zip_tseitin_30
| ( ( op2 @ e22 @ e23 )
= e22 ) ),
inference(simplify,[status(thm)],[zip_derived_cl2420]) ).
thf(zip_derived_cl285,plain,
( ( ( op2 @ e22 @ e23 )
= e22 )
| ~ zip_tseitin_30 ),
inference(cnf,[status(esa)],[zf_stmt_4]) ).
thf(zip_derived_cl2476,plain,
( ( op2 @ e22 @ e23 )
= e22 ),
inference(clc,[status(thm)],[zip_derived_cl2423,zip_derived_cl285]) ).
thf(zip_derived_cl295_014,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl1756_015,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl2717,plain,
( ( e22 = e21 )
| ( e23 = e21 )
| ( ( op2 @ e22 @ e21 )
= e21 )
| ( ( op2 @ e22 @ ( h4 @ e13 ) )
= e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl77,zip_derived_cl2476,zip_derived_cl295,zip_derived_cl1756]) ).
thf(ax8,axiom,
( ( e22 != e23 )
& ( e21 != e23 )
& ( e21 != e22 )
& ( e20 != e23 )
& ( e20 != e22 )
& ( e20 != e21 ) ) ).
thf(zip_derived_cl199,plain,
e21 != e23,
inference(cnf,[status(esa)],[ax8]) ).
thf(zip_derived_cl200,plain,
e21 != e22,
inference(cnf,[status(esa)],[ax8]) ).
thf(zip_derived_cl2718,plain,
( ( ( op2 @ e22 @ e21 )
= e21 )
| ( ( op2 @ e22 @ ( h4 @ e13 ) )
= e21 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2717,zip_derived_cl199,zip_derived_cl200]) ).
thf(zip_derived_cl291,plain,
( zip_tseitin_19
| zip_tseitin_18
| zip_tseitin_17
| zip_tseitin_16 ),
inference(cnf,[status(esa)],[zf_stmt_33]) ).
thf(zip_derived_cl257,plain,
( ( ( op2 @ e20 @ e20 )
= e20 )
| ~ zip_tseitin_16 ),
inference(cnf,[status(esa)],[zf_stmt_32]) ).
thf(zip_derived_cl256,plain,
( ( ( op2 @ e20 @ e20 )
!= e20 )
| ~ zip_tseitin_16 ),
inference(cnf,[status(esa)],[zf_stmt_32]) ).
thf(zip_derived_cl1508,plain,
~ zip_tseitin_16,
inference(clc,[status(thm)],[zip_derived_cl257,zip_derived_cl256]) ).
thf(zip_derived_cl1517,plain,
( zip_tseitin_17
| zip_tseitin_18
| zip_tseitin_19 ),
inference(clc,[status(thm)],[zip_derived_cl291,zip_derived_cl1508]) ).
thf(zip_derived_cl261,plain,
( ( ( op2 @ e22 @ e20 )
= e22 )
| ~ zip_tseitin_18 ),
inference(cnf,[status(esa)],[zf_stmt_28]) ).
thf(zip_derived_cl153,plain,
( ( op2 @ e22 @ e20 )
!= ( op2 @ e22 @ e23 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1524,plain,
( ( e22
!= ( op2 @ e22 @ e23 ) )
| ~ zip_tseitin_18 ),
inference('sup-',[status(thm)],[zip_derived_cl261,zip_derived_cl153]) ).
thf(zip_derived_cl2476_016,plain,
( ( op2 @ e22 @ e23 )
= e22 ),
inference(clc,[status(thm)],[zip_derived_cl2423,zip_derived_cl285]) ).
thf(zip_derived_cl2480,plain,
( ( e22 != e22 )
| ~ zip_tseitin_18 ),
inference(demod,[status(thm)],[zip_derived_cl1524,zip_derived_cl2476]) ).
thf(zip_derived_cl2481,plain,
~ zip_tseitin_18,
inference(simplify,[status(thm)],[zip_derived_cl2480]) ).
thf(zip_derived_cl2491,plain,
( zip_tseitin_17
| zip_tseitin_19 ),
inference(demod,[status(thm)],[zip_derived_cl1517,zip_derived_cl2481]) ).
thf(zip_derived_cl259,plain,
( ( ( op2 @ e21 @ e20 )
= e21 )
| ~ zip_tseitin_17 ),
inference(cnf,[status(esa)],[zf_stmt_30]) ).
thf(zip_derived_cl188,plain,
( ( op2 @ e21 @ e20 )
!= ( op2 @ e22 @ e20 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1513,plain,
( ( e21
!= ( op2 @ e22 @ e20 ) )
| ~ zip_tseitin_17 ),
inference('sup-',[status(thm)],[zip_derived_cl259,zip_derived_cl188]) ).
thf(zip_derived_cl1756_017,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1799,plain,
( ( e21
!= ( op2 @ e22 @ ( h4 @ e13 ) ) )
| ~ zip_tseitin_17 ),
inference(demod,[status(thm)],[zip_derived_cl1513,zip_derived_cl1756]) ).
thf(zip_derived_cl2587,plain,
( zip_tseitin_19
| ( e21
!= ( op2 @ e22 @ ( h4 @ e13 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2491,zip_derived_cl1799]) ).
thf(zip_derived_cl263,plain,
( ( ( op2 @ e23 @ e20 )
= e23 )
| ~ zip_tseitin_19 ),
inference(cnf,[status(esa)],[zf_stmt_26]) ).
thf(zip_derived_cl149,plain,
( ( op2 @ e23 @ e20 )
!= ( op2 @ e23 @ e21 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1529,plain,
( ( e23
!= ( op2 @ e23 @ e21 ) )
| ~ zip_tseitin_19 ),
inference('sup-',[status(thm)],[zip_derived_cl263,zip_derived_cl149]) ).
thf(zip_derived_cl271,plain,
( ( ( op2 @ e23 @ e21 )
= e23 )
| ~ zip_tseitin_23 ),
inference(cnf,[status(esa)],[zf_stmt_18]) ).
thf(zip_derived_cl290,plain,
( zip_tseitin_23
| zip_tseitin_22
| zip_tseitin_21
| zip_tseitin_20 ),
inference(cnf,[status(esa)],[zf_stmt_33]) ).
thf(zip_derived_cl267,plain,
( ( ( op2 @ e21 @ e21 )
= e21 )
| ~ zip_tseitin_21 ),
inference(cnf,[status(esa)],[zf_stmt_22]) ).
thf(zip_derived_cl266,plain,
( ( ( op2 @ e21 @ e21 )
!= e21 )
| ~ zip_tseitin_21 ),
inference(cnf,[status(esa)],[zf_stmt_22]) ).
thf(zip_derived_cl1536,plain,
~ zip_tseitin_21,
inference(clc,[status(thm)],[zip_derived_cl267,zip_derived_cl266]) ).
thf(zip_derived_cl1537,plain,
( zip_tseitin_23
| zip_tseitin_22
| zip_tseitin_20 ),
inference(demod,[status(thm)],[zip_derived_cl290,zip_derived_cl1536]) ).
thf(zip_derived_cl269,plain,
( ( ( op2 @ e22 @ e21 )
= e22 )
| ~ zip_tseitin_22 ),
inference(cnf,[status(esa)],[zf_stmt_20]) ).
thf(zip_derived_cl151,plain,
( ( op2 @ e22 @ e21 )
!= ( op2 @ e22 @ e23 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1539,plain,
( ( e22
!= ( op2 @ e22 @ e23 ) )
| ~ zip_tseitin_22 ),
inference('sup-',[status(thm)],[zip_derived_cl269,zip_derived_cl151]) ).
thf(zip_derived_cl2476_018,plain,
( ( op2 @ e22 @ e23 )
= e22 ),
inference(clc,[status(thm)],[zip_derived_cl2423,zip_derived_cl285]) ).
thf(zip_derived_cl2482,plain,
( ( e22 != e22 )
| ~ zip_tseitin_22 ),
inference(demod,[status(thm)],[zip_derived_cl1539,zip_derived_cl2476]) ).
thf(zip_derived_cl2483,plain,
~ zip_tseitin_22,
inference(simplify,[status(thm)],[zip_derived_cl2482]) ).
thf(zip_derived_cl2497,plain,
( zip_tseitin_23
| zip_tseitin_20 ),
inference(demod,[status(thm)],[zip_derived_cl1537,zip_derived_cl2483]) ).
thf(zip_derived_cl89,plain,
( ( ( op2 @ e20 @ e23 )
= e23 )
| ( ( op2 @ e20 @ e22 )
= e23 )
| ( ( op2 @ e20 @ e21 )
= e23 )
| ( ( op2 @ e20 @ e20 )
= e23 ) ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl1756_019,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_020,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_021,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_022,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_023,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(ax14,axiom,
( ( ( h1 @ e13 )
= ( op2 @ e20 @ e20 ) )
& ( ( h1 @ e11 )
= ( op2 @ ( op2 @ ( op2 @ e20 @ e20 ) @ ( op2 @ e20 @ e20 ) ) @ ( op2 @ e20 @ e20 ) ) )
& ( ( h1 @ e10 )
= ( op2 @ ( op2 @ e20 @ e20 ) @ ( op2 @ e20 @ e20 ) ) )
& ( ( h1 @ e12 )
= e20 ) ) ).
thf(zip_derived_cl298,plain,
( ( h1 @ e13 )
= ( op2 @ e20 @ e20 ) ),
inference(cnf,[status(esa)],[ax14]) ).
thf(zip_derived_cl1756_024,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_025,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1794,plain,
( ( h1 @ e13 )
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl298,zip_derived_cl1756,zip_derived_cl1756]) ).
thf(zip_derived_cl312,plain,
( ( h4 @ e10 )
= ( op2 @ ( op2 @ e23 @ e23 ) @ ( op2 @ e23 @ e23 ) ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl310_026,plain,
( ( h4 @ e13 )
= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl310_027,plain,
( ( h4 @ e13 )
= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl1794_028,plain,
( ( h1 @ e13 )
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl298,zip_derived_cl1756,zip_derived_cl1756]) ).
thf(zip_derived_cl2004,plain,
( ( h4 @ e10 )
= ( h1 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl312,zip_derived_cl310,zip_derived_cl310,zip_derived_cl1794]) ).
thf(zip_derived_cl2009,plain,
( ( h4 @ e10 )
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1794,zip_derived_cl2004]) ).
thf(zip_derived_cl2919,plain,
( ( ( op2 @ ( h4 @ e13 ) @ e23 )
= e23 )
| ( ( op2 @ ( h4 @ e13 ) @ e22 )
= e23 )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e23 )
| ( ( h4 @ e10 )
= e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl89,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl2009]) ).
thf(zip_derived_cl178,plain,
( ( op2 @ e20 @ e22 )
!= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl295_029,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl1498,plain,
( ( op2 @ e20 @ e22 )
!= e23 ),
inference(demod,[status(thm)],[zip_derived_cl178,zip_derived_cl295]) ).
thf(zip_derived_cl1756_030,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1797,plain,
( ( op2 @ ( h4 @ e13 ) @ e22 )
!= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1498,zip_derived_cl1756]) ).
thf(zip_derived_cl2920,plain,
( ( ( op2 @ ( h4 @ e13 ) @ e23 )
= e23 )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e23 )
| ( ( h4 @ e10 )
= e23 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2919,zip_derived_cl1797]) ).
thf(zip_derived_cl296,plain,
( e21
= ( op2 @ ( op2 @ ( op2 @ e22 @ e22 ) @ ( op2 @ e22 @ e22 ) ) @ ( op2 @ e22 @ e22 ) ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl295_031,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl295_032,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl310_033,plain,
( ( h4 @ e13 )
= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl295_034,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl3106,plain,
( e21
= ( op2 @ ( h4 @ e13 ) @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl296,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310,zip_derived_cl295]) ).
thf(zip_derived_cl3113,plain,
( ( e21 = e23 )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e23 )
| ( ( h4 @ e10 )
= e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl2920,zip_derived_cl3106]) ).
thf(zip_derived_cl199_035,plain,
e21 != e23,
inference(cnf,[status(esa)],[ax8]) ).
thf(zip_derived_cl3114,plain,
( ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e23 )
| ( ( h4 @ e10 )
= e23 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3113,zip_derived_cl199]) ).
thf(zip_derived_cl265,plain,
( ( ( op2 @ e20 @ e21 )
= e20 )
| ~ zip_tseitin_20 ),
inference(cnf,[status(esa)],[zf_stmt_24]) ).
thf(zip_derived_cl1756_036,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_037,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1789,plain,
( ( ( op2 @ ( h4 @ e13 ) @ e21 )
= ( h4 @ e13 ) )
| ~ zip_tseitin_20 ),
inference(demod,[status(thm)],[zip_derived_cl265,zip_derived_cl1756,zip_derived_cl1756]) ).
thf(zip_derived_cl3204,plain,
( ( e23
= ( h4 @ e13 ) )
| ( ( h4 @ e10 )
= e23 )
| ~ zip_tseitin_20 ),
inference('sup+',[status(thm)],[zip_derived_cl3114,zip_derived_cl1789]) ).
thf(zip_derived_cl201,plain,
e20 != e23,
inference(cnf,[status(esa)],[ax8]) ).
thf(zip_derived_cl1756_038,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1775,plain,
( ( h4 @ e13 )
!= e23 ),
inference(demod,[status(thm)],[zip_derived_cl201,zip_derived_cl1756]) ).
thf(zip_derived_cl3215,plain,
( ( ( h4 @ e10 )
= e23 )
| ~ zip_tseitin_20 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3204,zip_derived_cl1775]) ).
thf(zip_derived_cl1789_039,plain,
( ( ( op2 @ ( h4 @ e13 ) @ e21 )
= ( h4 @ e13 ) )
| ~ zip_tseitin_20 ),
inference(demod,[status(thm)],[zip_derived_cl265,zip_derived_cl1756,zip_derived_cl1756]) ).
thf(zip_derived_cl1517_040,plain,
( zip_tseitin_17
| zip_tseitin_18
| zip_tseitin_19 ),
inference(clc,[status(thm)],[zip_derived_cl291,zip_derived_cl1508]) ).
thf(zip_derived_cl258,plain,
( ( ( op2 @ e20 @ e21 )
!= e20 )
| ~ zip_tseitin_17 ),
inference(cnf,[status(esa)],[zf_stmt_30]) ).
thf(zip_derived_cl1518,plain,
( zip_tseitin_19
| zip_tseitin_18
| ( ( op2 @ e20 @ e21 )
!= e20 ) ),
inference('sup-',[status(thm)],[zip_derived_cl1517,zip_derived_cl258]) ).
thf(zip_derived_cl1756_041,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_042,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1800,plain,
( zip_tseitin_19
| zip_tseitin_18
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
!= ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1518,zip_derived_cl1756,zip_derived_cl1756]) ).
thf(zip_derived_cl2481_043,plain,
~ zip_tseitin_18,
inference(simplify,[status(thm)],[zip_derived_cl2480]) ).
thf(zip_derived_cl2494,plain,
( zip_tseitin_19
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
!= ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1800,zip_derived_cl2481]) ).
thf(zip_derived_cl2908,plain,
( ( ( h4 @ e13 )
!= ( h4 @ e13 ) )
| ~ zip_tseitin_20
| zip_tseitin_19 ),
inference('sup-',[status(thm)],[zip_derived_cl1789,zip_derived_cl2494]) ).
thf(zip_derived_cl2914,plain,
( zip_tseitin_19
| ~ zip_tseitin_20 ),
inference(simplify,[status(thm)],[zip_derived_cl2908]) ).
thf(zip_derived_cl263_044,plain,
( ( ( op2 @ e23 @ e20 )
= e23 )
| ~ zip_tseitin_19 ),
inference(cnf,[status(esa)],[zf_stmt_26]) ).
thf(zip_derived_cl189,plain,
( ( op2 @ e20 @ e20 )
!= ( op2 @ e23 @ e20 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl298_045,plain,
( ( h1 @ e13 )
= ( op2 @ e20 @ e20 ) ),
inference(cnf,[status(esa)],[ax14]) ).
thf(zip_derived_cl1613,plain,
( ( h1 @ e13 )
!= ( op2 @ e23 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl189,zip_derived_cl298]) ).
thf(zip_derived_cl1620,plain,
( ( ( h1 @ e13 )
!= e23 )
| ~ zip_tseitin_19 ),
inference('sup-',[status(thm)],[zip_derived_cl263,zip_derived_cl1613]) ).
thf(zip_derived_cl2004_046,plain,
( ( h4 @ e10 )
= ( h1 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl312,zip_derived_cl310,zip_derived_cl310,zip_derived_cl1794]) ).
thf(zip_derived_cl2005,plain,
( ( ( h4 @ e10 )
!= e23 )
| ~ zip_tseitin_19 ),
inference(demod,[status(thm)],[zip_derived_cl1620,zip_derived_cl2004]) ).
thf(zip_derived_cl2918,plain,
( ~ zip_tseitin_20
| ( ( h4 @ e10 )
!= e23 ) ),
inference('sup-',[status(thm)],[zip_derived_cl2914,zip_derived_cl2005]) ).
thf(zip_derived_cl3253,plain,
~ zip_tseitin_20,
inference(clc,[status(thm)],[zip_derived_cl3215,zip_derived_cl2918]) ).
thf(zip_derived_cl3254,plain,
zip_tseitin_23,
inference('sup-',[status(thm)],[zip_derived_cl2497,zip_derived_cl3253]) ).
thf(zip_derived_cl3255,plain,
( ( op2 @ e23 @ e21 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl271,zip_derived_cl3254]) ).
thf(zip_derived_cl3315,plain,
( ( e23 != e23 )
| ~ zip_tseitin_19 ),
inference(demod,[status(thm)],[zip_derived_cl1529,zip_derived_cl3255]) ).
thf(zip_derived_cl3316,plain,
~ zip_tseitin_19,
inference(simplify,[status(thm)],[zip_derived_cl3315]) ).
thf(zip_derived_cl3356,plain,
( e21
!= ( op2 @ e22 @ ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2587,zip_derived_cl3316]) ).
thf(zip_derived_cl3391,plain,
( ( e21 != e21 )
| ( ( op2 @ e22 @ e21 )
= e21 ) ),
inference('sup-',[status(thm)],[zip_derived_cl2718,zip_derived_cl3356]) ).
thf(zip_derived_cl3394,plain,
( ( op2 @ e22 @ e21 )
= e21 ),
inference(simplify,[status(thm)],[zip_derived_cl3391]) ).
thf(zip_derived_cl3469,plain,
( ( e21
= ( h4 @ e13 ) )
| ( ( h2 @ e13 )
= ( h4 @ e13 ) )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2859,zip_derived_cl3394]) ).
thf(zip_derived_cl2494_047,plain,
( zip_tseitin_19
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
!= ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1800,zip_derived_cl2481]) ).
thf(zip_derived_cl3316_048,plain,
~ zip_tseitin_19,
inference(simplify,[status(thm)],[zip_derived_cl3315]) ).
thf(zip_derived_cl3354,plain,
( ( op2 @ ( h4 @ e13 ) @ e21 )
!= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl2494,zip_derived_cl3316]) ).
thf(zip_derived_cl203,plain,
e20 != e21,
inference(cnf,[status(esa)],[ax8]) ).
thf(zip_derived_cl1756_049,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1777,plain,
( ( h4 @ e13 )
!= e21 ),
inference(demod,[status(thm)],[zip_derived_cl203,zip_derived_cl1756]) ).
thf(zip_derived_cl3470,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl3470_050,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl3503,plain,
( ( h2 @ e10 )
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2002,zip_derived_cl3470,zip_derived_cl3470]) ).
thf(zip_derived_cl2009_051,plain,
( ( h4 @ e10 )
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1794,zip_derived_cl2004]) ).
thf(zip_derived_cl3114_052,plain,
( ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e23 )
| ( ( h4 @ e10 )
= e23 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3113,zip_derived_cl199]) ).
thf(zip_derived_cl183,plain,
( ( op2 @ e20 @ e21 )
!= ( op2 @ e23 @ e21 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1756_053,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1770,plain,
( ( op2 @ ( h4 @ e13 ) @ e21 )
!= ( op2 @ e23 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl183,zip_derived_cl1756]) ).
thf(zip_derived_cl3202,plain,
( ( e23
!= ( op2 @ e23 @ e21 ) )
| ( ( h4 @ e10 )
= e23 ) ),
inference('sup-',[status(thm)],[zip_derived_cl3114,zip_derived_cl1770]) ).
thf(zip_derived_cl3255_054,plain,
( ( op2 @ e23 @ e21 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl271,zip_derived_cl3254]) ).
thf(zip_derived_cl3335,plain,
( ( e23 != e23 )
| ( ( h4 @ e10 )
= e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl3202,zip_derived_cl3255]) ).
thf(zip_derived_cl3336,plain,
( ( h4 @ e10 )
= e23 ),
inference(simplify,[status(thm)],[zip_derived_cl3335]) ).
thf(zip_derived_cl3417,plain,
( e23
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2009,zip_derived_cl3336]) ).
thf(zip_derived_cl3737,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl303,plain,
( ( h2 @ e11 )
= ( op2 @ ( op2 @ ( op2 @ e21 @ e21 ) @ ( op2 @ e21 @ e21 ) ) @ ( op2 @ e21 @ e21 ) ) ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl302_055,plain,
( ( h2 @ e13 )
= ( op2 @ e21 @ e21 ) ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl302_056,plain,
( ( h2 @ e13 )
= ( op2 @ e21 @ e21 ) ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl2002_057,plain,
( ( h2 @ e10 )
= ( op2 @ ( h2 @ e13 ) @ ( h2 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl304,zip_derived_cl302,zip_derived_cl302]) ).
thf(zip_derived_cl302_058,plain,
( ( h2 @ e13 )
= ( op2 @ e21 @ e21 ) ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl3266,plain,
( ( h2 @ e11 )
= ( op2 @ ( h2 @ e10 ) @ ( h2 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl303,zip_derived_cl302,zip_derived_cl302,zip_derived_cl2002,zip_derived_cl302]) ).
thf(zip_derived_cl3470_059,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl3505,plain,
( ( h2 @ e11 )
= ( op2 @ ( h2 @ e10 ) @ ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3266,zip_derived_cl3470]) ).
thf(zip_derived_cl3737_060,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl51,plain,
( ( ( op2 @ e23 @ e20 )
= e23 )
| ( ( op2 @ e23 @ e20 )
= e22 )
| ( ( op2 @ e23 @ e20 )
= e21 )
| ( ( op2 @ e23 @ e20 )
= e20 ) ),
inference(cnf,[status(esa)],[ax3]) ).
thf(zip_derived_cl1756_061,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_062,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_063,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_064,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_065,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl2401,plain,
( ( ( op2 @ e23 @ ( h4 @ e13 ) )
= e23 )
| ( ( op2 @ e23 @ ( h4 @ e13 ) )
= e22 )
| ( ( op2 @ e23 @ ( h4 @ e13 ) )
= e21 )
| ( ( op2 @ e23 @ ( h4 @ e13 ) )
= ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl51,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl1756]) ).
thf(zip_derived_cl147,plain,
( ( op2 @ e23 @ e20 )
!= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl310_066,plain,
( ( h4 @ e13 )
= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl1669,plain,
( ( op2 @ e23 @ e20 )
!= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl147,zip_derived_cl310]) ).
thf(zip_derived_cl1756_067,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1841,plain,
( ( op2 @ e23 @ ( h4 @ e13 ) )
!= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl1669,zip_derived_cl1756]) ).
thf(zip_derived_cl2402,plain,
( ( ( op2 @ e23 @ ( h4 @ e13 ) )
= e23 )
| ( ( op2 @ e23 @ ( h4 @ e13 ) )
= e22 )
| ( ( op2 @ e23 @ ( h4 @ e13 ) )
= e21 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2401,zip_derived_cl1841]) ).
thf(zip_derived_cl1517_068,plain,
( zip_tseitin_17
| zip_tseitin_18
| zip_tseitin_19 ),
inference(clc,[status(thm)],[zip_derived_cl291,zip_derived_cl1508]) ).
thf(zip_derived_cl259_069,plain,
( ( ( op2 @ e21 @ e20 )
= e21 )
| ~ zip_tseitin_17 ),
inference(cnf,[status(esa)],[zf_stmt_30]) ).
thf(zip_derived_cl187,plain,
( ( op2 @ e21 @ e20 )
!= ( op2 @ e23 @ e20 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1512,plain,
( ( e21
!= ( op2 @ e23 @ e20 ) )
| ~ zip_tseitin_17 ),
inference('sup-',[status(thm)],[zip_derived_cl259,zip_derived_cl187]) ).
thf(zip_derived_cl1522,plain,
( zip_tseitin_19
| zip_tseitin_18
| ( e21
!= ( op2 @ e23 @ e20 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl1517,zip_derived_cl1512]) ).
thf(zip_derived_cl1756_070,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1801,plain,
( zip_tseitin_19
| zip_tseitin_18
| ( e21
!= ( op2 @ e23 @ ( h4 @ e13 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1522,zip_derived_cl1756]) ).
thf(zip_derived_cl2481_071,plain,
~ zip_tseitin_18,
inference(simplify,[status(thm)],[zip_derived_cl2480]) ).
thf(zip_derived_cl2495,plain,
( zip_tseitin_19
| ( e21
!= ( op2 @ e23 @ ( h4 @ e13 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1801,zip_derived_cl2481]) ).
thf(zip_derived_cl3316_072,plain,
~ zip_tseitin_19,
inference(simplify,[status(thm)],[zip_derived_cl3315]) ).
thf(zip_derived_cl3355,plain,
( e21
!= ( op2 @ e23 @ ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2495,zip_derived_cl3316]) ).
thf(zip_derived_cl3387,plain,
( ( e21 != e21 )
| ( ( op2 @ e23 @ ( h4 @ e13 ) )
= e22 )
| ( ( op2 @ e23 @ ( h4 @ e13 ) )
= e23 ) ),
inference('sup-',[status(thm)],[zip_derived_cl2402,zip_derived_cl3355]) ).
thf(zip_derived_cl3388,plain,
( ( ( op2 @ e23 @ ( h4 @ e13 ) )
= e23 )
| ( ( op2 @ e23 @ ( h4 @ e13 ) )
= e22 ) ),
inference(simplify,[status(thm)],[zip_derived_cl3387]) ).
thf(zip_derived_cl149_073,plain,
( ( op2 @ e23 @ e20 )
!= ( op2 @ e23 @ e21 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1756_074,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1758,plain,
( ( op2 @ e23 @ ( h4 @ e13 ) )
!= ( op2 @ e23 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl149,zip_derived_cl1756]) ).
thf(zip_derived_cl3255_075,plain,
( ( op2 @ e23 @ e21 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl271,zip_derived_cl3254]) ).
thf(zip_derived_cl3319,plain,
( ( op2 @ e23 @ ( h4 @ e13 ) )
!= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1758,zip_derived_cl3255]) ).
thf(zip_derived_cl3389,plain,
( ( op2 @ e23 @ ( h4 @ e13 ) )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3388,zip_derived_cl3319]) ).
thf(zip_derived_cl3738,plain,
( ( h2 @ e11 )
= e22 ),
inference(demod,[status(thm)],[zip_derived_cl3505,zip_derived_cl3737,zip_derived_cl3389]) ).
thf(zip_derived_cl305,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl3470_076,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl1756_077,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(ax12,axiom,
( ( e13
= ( op1 @ e12 @ e12 ) )
& ( e11
= ( op1 @ ( op1 @ ( op1 @ e12 @ e12 ) @ ( op1 @ e12 @ e12 ) ) @ ( op1 @ e12 @ e12 ) ) )
& ( e10
= ( op1 @ ( op1 @ e12 @ e12 ) @ ( op1 @ e12 @ e12 ) ) ) ) ).
thf(zip_derived_cl294,plain,
( e10
= ( op1 @ ( op1 @ e12 @ e12 ) @ ( op1 @ e12 @ e12 ) ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl292,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl292_078,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl1697,plain,
( e10
= ( op1 @ e13 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl294,zip_derived_cl292,zip_derived_cl292]) ).
thf(zip_derived_cl3737_079,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl3470_080,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl3470_081,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl3417_082,plain,
( e23
= ( op2 @ ( h4 @ e13 ) @ ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2009,zip_derived_cl3336]) ).
thf(ax2,axiom,
( ( ( ( op1 @ e13 @ e13 )
= e13 )
| ( ( op1 @ e12 @ e13 )
= e13 )
| ( ( op1 @ e11 @ e13 )
= e13 )
| ( ( op1 @ e10 @ e13 )
= e13 ) )
& ( ( ( op1 @ e13 @ e13 )
= e13 )
| ( ( op1 @ e13 @ e12 )
= e13 )
| ( ( op1 @ e13 @ e11 )
= e13 )
| ( ( op1 @ e13 @ e10 )
= e13 ) )
& ( ( ( op1 @ e13 @ e13 )
= e12 )
| ( ( op1 @ e12 @ e13 )
= e12 )
| ( ( op1 @ e11 @ e13 )
= e12 )
| ( ( op1 @ e10 @ e13 )
= e12 ) )
& ( ( ( op1 @ e13 @ e13 )
= e12 )
| ( ( op1 @ e13 @ e12 )
= e12 )
| ( ( op1 @ e13 @ e11 )
= e12 )
| ( ( op1 @ e13 @ e10 )
= e12 ) )
& ( ( ( op1 @ e13 @ e13 )
= e11 )
| ( ( op1 @ e12 @ e13 )
= e11 )
| ( ( op1 @ e11 @ e13 )
= e11 )
| ( ( op1 @ e10 @ e13 )
= e11 ) )
& ( ( ( op1 @ e13 @ e13 )
= e11 )
| ( ( op1 @ e13 @ e12 )
= e11 )
| ( ( op1 @ e13 @ e11 )
= e11 )
| ( ( op1 @ e13 @ e10 )
= e11 ) )
& ( ( ( op1 @ e13 @ e13 )
= e10 )
| ( ( op1 @ e12 @ e13 )
= e10 )
| ( ( op1 @ e11 @ e13 )
= e10 )
| ( ( op1 @ e10 @ e13 )
= e10 ) )
& ( ( ( op1 @ e13 @ e13 )
= e10 )
| ( ( op1 @ e13 @ e12 )
= e10 )
| ( ( op1 @ e13 @ e11 )
= e10 )
| ( ( op1 @ e13 @ e10 )
= e10 ) )
& ( ( ( op1 @ e13 @ e12 )
= e13 )
| ( ( op1 @ e12 @ e12 )
= e13 )
| ( ( op1 @ e11 @ e12 )
= e13 )
| ( ( op1 @ e10 @ e12 )
= e13 ) )
& ( ( ( op1 @ e12 @ e13 )
= e13 )
| ( ( op1 @ e12 @ e12 )
= e13 )
| ( ( op1 @ e12 @ e11 )
= e13 )
| ( ( op1 @ e12 @ e10 )
= e13 ) )
& ( ( ( op1 @ e13 @ e12 )
= e12 )
| ( ( op1 @ e12 @ e12 )
= e12 )
| ( ( op1 @ e11 @ e12 )
= e12 )
| ( ( op1 @ e10 @ e12 )
= e12 ) )
& ( ( ( op1 @ e12 @ e13 )
= e12 )
| ( ( op1 @ e12 @ e12 )
= e12 )
| ( ( op1 @ e12 @ e11 )
= e12 )
| ( ( op1 @ e12 @ e10 )
= e12 ) )
& ( ( ( op1 @ e13 @ e12 )
= e11 )
| ( ( op1 @ e12 @ e12 )
= e11 )
| ( ( op1 @ e11 @ e12 )
= e11 )
| ( ( op1 @ e10 @ e12 )
= e11 ) )
& ( ( ( op1 @ e12 @ e13 )
= e11 )
| ( ( op1 @ e12 @ e12 )
= e11 )
| ( ( op1 @ e12 @ e11 )
= e11 )
| ( ( op1 @ e12 @ e10 )
= e11 ) )
& ( ( ( op1 @ e13 @ e12 )
= e10 )
| ( ( op1 @ e12 @ e12 )
= e10 )
| ( ( op1 @ e11 @ e12 )
= e10 )
| ( ( op1 @ e10 @ e12 )
= e10 ) )
& ( ( ( op1 @ e12 @ e13 )
= e10 )
| ( ( op1 @ e12 @ e12 )
= e10 )
| ( ( op1 @ e12 @ e11 )
= e10 )
| ( ( op1 @ e12 @ e10 )
= e10 ) )
& ( ( ( op1 @ e13 @ e11 )
= e13 )
| ( ( op1 @ e12 @ e11 )
= e13 )
| ( ( op1 @ e11 @ e11 )
= e13 )
| ( ( op1 @ e10 @ e11 )
= e13 ) )
& ( ( ( op1 @ e11 @ e13 )
= e13 )
| ( ( op1 @ e11 @ e12 )
= e13 )
| ( ( op1 @ e11 @ e11 )
= e13 )
| ( ( op1 @ e11 @ e10 )
= e13 ) )
& ( ( ( op1 @ e13 @ e11 )
= e12 )
| ( ( op1 @ e12 @ e11 )
= e12 )
| ( ( op1 @ e11 @ e11 )
= e12 )
| ( ( op1 @ e10 @ e11 )
= e12 ) )
& ( ( ( op1 @ e11 @ e13 )
= e12 )
| ( ( op1 @ e11 @ e12 )
= e12 )
| ( ( op1 @ e11 @ e11 )
= e12 )
| ( ( op1 @ e11 @ e10 )
= e12 ) )
& ( ( ( op1 @ e13 @ e11 )
= e11 )
| ( ( op1 @ e12 @ e11 )
= e11 )
| ( ( op1 @ e11 @ e11 )
= e11 )
| ( ( op1 @ e10 @ e11 )
= e11 ) )
& ( ( ( op1 @ e11 @ e13 )
= e11 )
| ( ( op1 @ e11 @ e12 )
= e11 )
| ( ( op1 @ e11 @ e11 )
= e11 )
| ( ( op1 @ e11 @ e10 )
= e11 ) )
& ( ( ( op1 @ e13 @ e11 )
= e10 )
| ( ( op1 @ e12 @ e11 )
= e10 )
| ( ( op1 @ e11 @ e11 )
= e10 )
| ( ( op1 @ e10 @ e11 )
= e10 ) )
& ( ( ( op1 @ e11 @ e13 )
= e10 )
| ( ( op1 @ e11 @ e12 )
= e10 )
| ( ( op1 @ e11 @ e11 )
= e10 )
| ( ( op1 @ e11 @ e10 )
= e10 ) )
& ( ( ( op1 @ e13 @ e10 )
= e13 )
| ( ( op1 @ e12 @ e10 )
= e13 )
| ( ( op1 @ e11 @ e10 )
= e13 )
| ( ( op1 @ e10 @ e10 )
= e13 ) )
& ( ( ( op1 @ e10 @ e13 )
= e13 )
| ( ( op1 @ e10 @ e12 )
= e13 )
| ( ( op1 @ e10 @ e11 )
= e13 )
| ( ( op1 @ e10 @ e10 )
= e13 ) )
& ( ( ( op1 @ e13 @ e10 )
= e12 )
| ( ( op1 @ e12 @ e10 )
= e12 )
| ( ( op1 @ e11 @ e10 )
= e12 )
| ( ( op1 @ e10 @ e10 )
= e12 ) )
& ( ( ( op1 @ e10 @ e13 )
= e12 )
| ( ( op1 @ e10 @ e12 )
= e12 )
| ( ( op1 @ e10 @ e11 )
= e12 )
| ( ( op1 @ e10 @ e10 )
= e12 ) )
& ( ( ( op1 @ e13 @ e10 )
= e11 )
| ( ( op1 @ e12 @ e10 )
= e11 )
| ( ( op1 @ e11 @ e10 )
= e11 )
| ( ( op1 @ e10 @ e10 )
= e11 ) )
& ( ( ( op1 @ e10 @ e13 )
= e11 )
| ( ( op1 @ e10 @ e12 )
= e11 )
| ( ( op1 @ e10 @ e11 )
= e11 )
| ( ( op1 @ e10 @ e10 )
= e11 ) )
& ( ( ( op1 @ e13 @ e10 )
= e10 )
| ( ( op1 @ e12 @ e10 )
= e10 )
| ( ( op1 @ e11 @ e10 )
= e10 )
| ( ( op1 @ e10 @ e10 )
= e10 ) )
& ( ( ( op1 @ e10 @ e13 )
= e10 )
| ( ( op1 @ e10 @ e12 )
= e10 )
| ( ( op1 @ e10 @ e11 )
= e10 )
| ( ( op1 @ e10 @ e10 )
= e10 ) ) ) ).
thf(zip_derived_cl28,plain,
( ( ( op1 @ e13 @ e12 )
= e11 )
| ( ( op1 @ e12 @ e12 )
= e11 )
| ( ( op1 @ e11 @ e12 )
= e11 )
| ( ( op1 @ e10 @ e12 )
= e11 ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl292_083,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl2071,plain,
( ( ( op1 @ e13 @ e12 )
= e11 )
| ( e13 = e11 )
| ( ( op1 @ e11 @ e12 )
= e11 )
| ( ( op1 @ e10 @ e12 )
= e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl28,zip_derived_cl292]) ).
thf(ax7,axiom,
( ( e12 != e13 )
& ( e11 != e13 )
& ( e11 != e12 )
& ( e10 != e13 )
& ( e10 != e12 )
& ( e10 != e11 ) ) ).
thf(zip_derived_cl193,plain,
e11 != e13,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl2072,plain,
( ( ( op1 @ e13 @ e12 )
= e11 )
| ( ( op1 @ e11 @ e12 )
= e11 )
| ( ( op1 @ e10 @ e12 )
= e11 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2071,zip_derived_cl193]) ).
thf(ax5,axiom,
( ( ( op1 @ e13 @ e12 )
!= ( op1 @ e13 @ e13 ) )
& ( ( op1 @ e13 @ e11 )
!= ( op1 @ e13 @ e13 ) )
& ( ( op1 @ e13 @ e11 )
!= ( op1 @ e13 @ e12 ) )
& ( ( op1 @ e13 @ e10 )
!= ( op1 @ e13 @ e13 ) )
& ( ( op1 @ e13 @ e10 )
!= ( op1 @ e13 @ e12 ) )
& ( ( op1 @ e13 @ e10 )
!= ( op1 @ e13 @ e11 ) )
& ( ( op1 @ e12 @ e12 )
!= ( op1 @ e12 @ e13 ) )
& ( ( op1 @ e12 @ e11 )
!= ( op1 @ e12 @ e13 ) )
& ( ( op1 @ e12 @ e11 )
!= ( op1 @ e12 @ e12 ) )
& ( ( op1 @ e12 @ e10 )
!= ( op1 @ e12 @ e13 ) )
& ( ( op1 @ e12 @ e10 )
!= ( op1 @ e12 @ e12 ) )
& ( ( op1 @ e12 @ e10 )
!= ( op1 @ e12 @ e11 ) )
& ( ( op1 @ e11 @ e12 )
!= ( op1 @ e11 @ e13 ) )
& ( ( op1 @ e11 @ e11 )
!= ( op1 @ e11 @ e13 ) )
& ( ( op1 @ e11 @ e11 )
!= ( op1 @ e11 @ e12 ) )
& ( ( op1 @ e11 @ e10 )
!= ( op1 @ e11 @ e13 ) )
& ( ( op1 @ e11 @ e10 )
!= ( op1 @ e11 @ e12 ) )
& ( ( op1 @ e11 @ e10 )
!= ( op1 @ e11 @ e11 ) )
& ( ( op1 @ e10 @ e12 )
!= ( op1 @ e10 @ e13 ) )
& ( ( op1 @ e10 @ e11 )
!= ( op1 @ e10 @ e13 ) )
& ( ( op1 @ e10 @ e11 )
!= ( op1 @ e10 @ e12 ) )
& ( ( op1 @ e10 @ e10 )
!= ( op1 @ e10 @ e13 ) )
& ( ( op1 @ e10 @ e10 )
!= ( op1 @ e10 @ e12 ) )
& ( ( op1 @ e10 @ e10 )
!= ( op1 @ e10 @ e11 ) )
& ( ( op1 @ e12 @ e13 )
!= ( op1 @ e13 @ e13 ) )
& ( ( op1 @ e11 @ e13 )
!= ( op1 @ e13 @ e13 ) )
& ( ( op1 @ e11 @ e13 )
!= ( op1 @ e12 @ e13 ) )
& ( ( op1 @ e10 @ e13 )
!= ( op1 @ e13 @ e13 ) )
& ( ( op1 @ e10 @ e13 )
!= ( op1 @ e12 @ e13 ) )
& ( ( op1 @ e10 @ e13 )
!= ( op1 @ e11 @ e13 ) )
& ( ( op1 @ e12 @ e12 )
!= ( op1 @ e13 @ e12 ) )
& ( ( op1 @ e11 @ e12 )
!= ( op1 @ e13 @ e12 ) )
& ( ( op1 @ e11 @ e12 )
!= ( op1 @ e12 @ e12 ) )
& ( ( op1 @ e10 @ e12 )
!= ( op1 @ e13 @ e12 ) )
& ( ( op1 @ e10 @ e12 )
!= ( op1 @ e12 @ e12 ) )
& ( ( op1 @ e10 @ e12 )
!= ( op1 @ e11 @ e12 ) )
& ( ( op1 @ e12 @ e11 )
!= ( op1 @ e13 @ e11 ) )
& ( ( op1 @ e11 @ e11 )
!= ( op1 @ e13 @ e11 ) )
& ( ( op1 @ e11 @ e11 )
!= ( op1 @ e12 @ e11 ) )
& ( ( op1 @ e10 @ e11 )
!= ( op1 @ e13 @ e11 ) )
& ( ( op1 @ e10 @ e11 )
!= ( op1 @ e12 @ e11 ) )
& ( ( op1 @ e10 @ e11 )
!= ( op1 @ e11 @ e11 ) )
& ( ( op1 @ e12 @ e10 )
!= ( op1 @ e13 @ e10 ) )
& ( ( op1 @ e11 @ e10 )
!= ( op1 @ e13 @ e10 ) )
& ( ( op1 @ e11 @ e10 )
!= ( op1 @ e12 @ e10 ) )
& ( ( op1 @ e10 @ e10 )
!= ( op1 @ e13 @ e10 ) )
& ( ( op1 @ e10 @ e10 )
!= ( op1 @ e12 @ e10 ) )
& ( ( op1 @ e10 @ e10 )
!= ( op1 @ e11 @ e10 ) ) ) ).
thf(zip_derived_cl114,plain,
( ( op1 @ e10 @ e12 )
!= ( op1 @ e10 @ e13 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl293,plain,
( e11
= ( op1 @ ( op1 @ ( op1 @ e12 @ e12 ) @ ( op1 @ e12 @ e12 ) ) @ ( op1 @ e12 @ e12 ) ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl292_084,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl292_085,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl1697_086,plain,
( e10
= ( op1 @ e13 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl294,zip_derived_cl292,zip_derived_cl292]) ).
thf(zip_derived_cl292_087,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl3088,plain,
( e11
= ( op1 @ e10 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl293,zip_derived_cl292,zip_derived_cl292,zip_derived_cl1697,zip_derived_cl292]) ).
thf(zip_derived_cl3091,plain,
( ( op1 @ e10 @ e12 )
!= e11 ),
inference(demod,[status(thm)],[zip_derived_cl114,zip_derived_cl3088]) ).
thf(zip_derived_cl3121,plain,
( ( e11 != e11 )
| ( ( op1 @ e11 @ e12 )
= e11 )
| ( ( op1 @ e13 @ e12 )
= e11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl2072,zip_derived_cl3091]) ).
thf(zip_derived_cl3124,plain,
( ( ( op1 @ e13 @ e12 )
= e11 )
| ( ( op1 @ e11 @ e12 )
= e11 ) ),
inference(simplify,[status(thm)],[zip_derived_cl3121]) ).
thf(zip_derived_cl112,plain,
( ( op1 @ e11 @ e10 )
!= ( op1 @ e11 @ e12 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(ax10,axiom,
( ( ( ( ( op1 @ e10 @ e10 )
= e10 )
& ( ( op1 @ e10 @ e10 )
!= e10 ) )
| ( ( ( op1 @ e11 @ e10 )
= e11 )
& ( ( op1 @ e10 @ e11 )
!= e10 ) )
| ( ( ( op1 @ e12 @ e10 )
= e12 )
& ( ( op1 @ e10 @ e12 )
!= e10 ) )
| ( ( ( op1 @ e13 @ e10 )
= e13 )
& ( ( op1 @ e10 @ e13 )
!= e10 ) ) )
& ( ( ( ( op1 @ e10 @ e11 )
= e10 )
& ( ( op1 @ e11 @ e10 )
!= e11 ) )
| ( ( ( op1 @ e11 @ e11 )
= e11 )
& ( ( op1 @ e11 @ e11 )
!= e11 ) )
| ( ( ( op1 @ e12 @ e11 )
= e12 )
& ( ( op1 @ e11 @ e12 )
!= e11 ) )
| ( ( ( op1 @ e13 @ e11 )
= e13 )
& ( ( op1 @ e11 @ e13 )
!= e11 ) ) )
& ( ( ( ( op1 @ e10 @ e12 )
= e10 )
& ( ( op1 @ e12 @ e10 )
!= e12 ) )
| ( ( ( op1 @ e11 @ e12 )
= e11 )
& ( ( op1 @ e12 @ e11 )
!= e12 ) )
| ( ( ( op1 @ e12 @ e12 )
= e12 )
& ( ( op1 @ e12 @ e12 )
!= e12 ) )
| ( ( ( op1 @ e13 @ e12 )
= e13 )
& ( ( op1 @ e12 @ e13 )
!= e12 ) ) )
& ( ( ( ( op1 @ e10 @ e13 )
= e10 )
& ( ( op1 @ e13 @ e10 )
!= e13 ) )
| ( ( ( op1 @ e11 @ e13 )
= e11 )
& ( ( op1 @ e13 @ e11 )
!= e13 ) )
| ( ( ( op1 @ e12 @ e13 )
= e12 )
& ( ( op1 @ e13 @ e12 )
!= e13 ) )
| ( ( ( op1 @ e13 @ e13 )
= e13 )
& ( ( op1 @ e13 @ e13 )
!= e13 ) ) ) ) ).
thf(zf_stmt_34,axiom,
( zip_tseitin_3
=> ( ( ( op1 @ e10 @ e13 )
!= e10 )
& ( ( op1 @ e13 @ e10 )
= e13 ) ) ) ).
thf(zip_derived_cl227,plain,
( ( ( op1 @ e13 @ e10 )
= e13 )
| ~ zip_tseitin_3 ),
inference(cnf,[status(esa)],[zf_stmt_34]) ).
thf(zf_stmt_35,type,
zip_tseitin_15: $o ).
thf(zf_stmt_36,axiom,
( zip_tseitin_15
=> ( ( ( op1 @ e13 @ e13 )
!= e13 )
& ( ( op1 @ e13 @ e13 )
= e13 ) ) ) ).
thf(zf_stmt_37,type,
zip_tseitin_14: $o ).
thf(zf_stmt_38,axiom,
( zip_tseitin_14
=> ( ( ( op1 @ e13 @ e12 )
!= e13 )
& ( ( op1 @ e12 @ e13 )
= e12 ) ) ) ).
thf(zf_stmt_39,type,
zip_tseitin_13: $o ).
thf(zf_stmt_40,axiom,
( zip_tseitin_13
=> ( ( ( op1 @ e13 @ e11 )
!= e13 )
& ( ( op1 @ e11 @ e13 )
= e11 ) ) ) ).
thf(zf_stmt_41,type,
zip_tseitin_12: $o ).
thf(zf_stmt_42,axiom,
( zip_tseitin_12
=> ( ( ( op1 @ e13 @ e10 )
!= e13 )
& ( ( op1 @ e10 @ e13 )
= e10 ) ) ) ).
thf(zf_stmt_43,type,
zip_tseitin_11: $o ).
thf(zf_stmt_44,axiom,
( zip_tseitin_11
=> ( ( ( op1 @ e12 @ e13 )
!= e12 )
& ( ( op1 @ e13 @ e12 )
= e13 ) ) ) ).
thf(zf_stmt_45,type,
zip_tseitin_10: $o ).
thf(zf_stmt_46,axiom,
( zip_tseitin_10
=> ( ( ( op1 @ e12 @ e12 )
!= e12 )
& ( ( op1 @ e12 @ e12 )
= e12 ) ) ) ).
thf(zf_stmt_47,type,
zip_tseitin_9: $o ).
thf(zf_stmt_48,axiom,
( zip_tseitin_9
=> ( ( ( op1 @ e12 @ e11 )
!= e12 )
& ( ( op1 @ e11 @ e12 )
= e11 ) ) ) ).
thf(zf_stmt_49,type,
zip_tseitin_8: $o ).
thf(zf_stmt_50,axiom,
( zip_tseitin_8
=> ( ( ( op1 @ e12 @ e10 )
!= e12 )
& ( ( op1 @ e10 @ e12 )
= e10 ) ) ) ).
thf(zf_stmt_51,type,
zip_tseitin_7: $o ).
thf(zf_stmt_52,axiom,
( zip_tseitin_7
=> ( ( ( op1 @ e11 @ e13 )
!= e11 )
& ( ( op1 @ e13 @ e11 )
= e13 ) ) ) ).
thf(zf_stmt_53,type,
zip_tseitin_6: $o ).
thf(zf_stmt_54,axiom,
( zip_tseitin_6
=> ( ( ( op1 @ e11 @ e12 )
!= e11 )
& ( ( op1 @ e12 @ e11 )
= e12 ) ) ) ).
thf(zf_stmt_55,type,
zip_tseitin_5: $o ).
thf(zf_stmt_56,axiom,
( zip_tseitin_5
=> ( ( ( op1 @ e11 @ e11 )
!= e11 )
& ( ( op1 @ e11 @ e11 )
= e11 ) ) ) ).
thf(zf_stmt_57,type,
zip_tseitin_4: $o ).
thf(zf_stmt_58,axiom,
( zip_tseitin_4
=> ( ( ( op1 @ e11 @ e10 )
!= e11 )
& ( ( op1 @ e10 @ e11 )
= e10 ) ) ) ).
thf(zf_stmt_59,type,
zip_tseitin_3: $o ).
thf(zf_stmt_60,type,
zip_tseitin_2: $o ).
thf(zf_stmt_61,axiom,
( zip_tseitin_2
=> ( ( ( op1 @ e10 @ e12 )
!= e10 )
& ( ( op1 @ e12 @ e10 )
= e12 ) ) ) ).
thf(zf_stmt_62,type,
zip_tseitin_1: $o ).
thf(zf_stmt_63,axiom,
( zip_tseitin_1
=> ( ( ( op1 @ e10 @ e11 )
!= e10 )
& ( ( op1 @ e11 @ e10 )
= e11 ) ) ) ).
thf(zf_stmt_64,type,
zip_tseitin_0: $o ).
thf(zf_stmt_65,axiom,
( zip_tseitin_0
=> ( ( ( op1 @ e10 @ e10 )
!= e10 )
& ( ( op1 @ e10 @ e10 )
= e10 ) ) ) ).
thf(zf_stmt_66,axiom,
( ( zip_tseitin_15
| zip_tseitin_14
| zip_tseitin_13
| zip_tseitin_12 )
& ( zip_tseitin_11
| zip_tseitin_10
| zip_tseitin_9
| zip_tseitin_8 )
& ( zip_tseitin_7
| zip_tseitin_6
| zip_tseitin_5
| zip_tseitin_4 )
& ( zip_tseitin_3
| zip_tseitin_2
| zip_tseitin_1
| zip_tseitin_0 ) ) ).
thf(zip_derived_cl255,plain,
( zip_tseitin_3
| zip_tseitin_2
| zip_tseitin_1
| zip_tseitin_0 ),
inference(cnf,[status(esa)],[zf_stmt_66]) ).
thf(zip_derived_cl221,plain,
( ( ( op1 @ e10 @ e10 )
= e10 )
| ~ zip_tseitin_0 ),
inference(cnf,[status(esa)],[zf_stmt_65]) ).
thf(zip_derived_cl220,plain,
( ( ( op1 @ e10 @ e10 )
!= e10 )
| ~ zip_tseitin_0 ),
inference(cnf,[status(esa)],[zf_stmt_65]) ).
thf(zip_derived_cl1426,plain,
~ zip_tseitin_0,
inference(clc,[status(thm)],[zip_derived_cl221,zip_derived_cl220]) ).
thf(zip_derived_cl1486,plain,
( zip_tseitin_1
| zip_tseitin_2
| zip_tseitin_3 ),
inference(clc,[status(thm)],[zip_derived_cl255,zip_derived_cl1426]) ).
thf(zip_derived_cl223,plain,
( ( ( op1 @ e11 @ e10 )
= e11 )
| ~ zip_tseitin_1 ),
inference(cnf,[status(esa)],[zf_stmt_63]) ).
thf(zip_derived_cl1488,plain,
( zip_tseitin_3
| zip_tseitin_2
| ( ( op1 @ e11 @ e10 )
= e11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl1486,zip_derived_cl223]) ).
thf(zip_derived_cl225,plain,
( ( ( op1 @ e12 @ e10 )
= e12 )
| ~ zip_tseitin_2 ),
inference(cnf,[status(esa)],[zf_stmt_61]) ).
thf(zip_derived_cl2377,plain,
( ( ( op1 @ e11 @ e10 )
= e11 )
| zip_tseitin_3
| ( ( op1 @ e12 @ e10 )
= e12 ) ),
inference('sup-',[status(thm)],[zip_derived_cl1488,zip_derived_cl225]) ).
thf(zip_derived_cl105,plain,
( ( op1 @ e12 @ e10 )
!= ( op1 @ e12 @ e13 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl249,plain,
( ( ( op1 @ e12 @ e13 )
= e12 )
| ~ zip_tseitin_14 ),
inference(cnf,[status(esa)],[zf_stmt_38]) ).
thf(zip_derived_cl252,plain,
( zip_tseitin_15
| zip_tseitin_14
| zip_tseitin_13
| zip_tseitin_12 ),
inference(cnf,[status(esa)],[zf_stmt_66]) ).
thf(zip_derived_cl251,plain,
( ( ( op1 @ e13 @ e13 )
= e13 )
| ~ zip_tseitin_15 ),
inference(cnf,[status(esa)],[zf_stmt_36]) ).
thf(zip_derived_cl250,plain,
( ( ( op1 @ e13 @ e13 )
!= e13 )
| ~ zip_tseitin_15 ),
inference(cnf,[status(esa)],[zf_stmt_36]) ).
thf(zip_derived_cl1460,plain,
~ zip_tseitin_15,
inference(clc,[status(thm)],[zip_derived_cl251,zip_derived_cl250]) ).
thf(zip_derived_cl1474,plain,
( zip_tseitin_14
| zip_tseitin_13
| zip_tseitin_12 ),
inference(demod,[status(thm)],[zip_derived_cl252,zip_derived_cl1460]) ).
thf(zip_derived_cl245,plain,
( ( ( op1 @ e10 @ e13 )
= e10 )
| ~ zip_tseitin_12 ),
inference(cnf,[status(esa)],[zf_stmt_42]) ).
thf(zip_derived_cl1476,plain,
( zip_tseitin_13
| zip_tseitin_14
| ( ( op1 @ e10 @ e13 )
= e10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl1474,zip_derived_cl245]) ).
thf(zip_derived_cl123,plain,
( ( op1 @ e10 @ e13 )
!= ( op1 @ e13 @ e13 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1697_088,plain,
( e10
= ( op1 @ e13 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl294,zip_derived_cl292,zip_derived_cl292]) ).
thf(zip_derived_cl1703,plain,
( ( op1 @ e10 @ e13 )
!= e10 ),
inference(demod,[status(thm)],[zip_derived_cl123,zip_derived_cl1697]) ).
thf(zip_derived_cl2242,plain,
( zip_tseitin_13
| zip_tseitin_14 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1476,zip_derived_cl1703]) ).
thf(zip_derived_cl247,plain,
( ( ( op1 @ e11 @ e13 )
= e11 )
| ~ zip_tseitin_13 ),
inference(cnf,[status(esa)],[zf_stmt_40]) ).
thf(zip_derived_cl2244,plain,
( zip_tseitin_14
| ( ( op1 @ e11 @ e13 )
= e11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl2242,zip_derived_cl247]) ).
thf(zip_derived_cl3088_089,plain,
( e11
= ( op1 @ e10 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl293,zip_derived_cl292,zip_derived_cl292,zip_derived_cl1697,zip_derived_cl292]) ).
thf(zip_derived_cl16,plain,
( ( ( op1 @ e13 @ e13 )
= e13 )
| ( ( op1 @ e12 @ e13 )
= e13 )
| ( ( op1 @ e11 @ e13 )
= e13 )
| ( ( op1 @ e10 @ e13 )
= e13 ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl1697_090,plain,
( e10
= ( op1 @ e13 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl294,zip_derived_cl292,zip_derived_cl292]) ).
thf(zip_derived_cl1732,plain,
( ( e10 = e13 )
| ( ( op1 @ e12 @ e13 )
= e13 )
| ( ( op1 @ e11 @ e13 )
= e13 )
| ( ( op1 @ e10 @ e13 )
= e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl16,zip_derived_cl1697]) ).
thf(zip_derived_cl102,plain,
( ( op1 @ e12 @ e12 )
!= ( op1 @ e12 @ e13 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl292_091,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl1434,plain,
( e13
!= ( op1 @ e12 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl102,zip_derived_cl292]) ).
thf(zip_derived_cl195,plain,
e10 != e13,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl1733,plain,
( ( ( op1 @ e11 @ e13 )
= e13 )
| ( ( op1 @ e10 @ e13 )
= e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1732,zip_derived_cl1434,zip_derived_cl195]) ).
thf(zip_derived_cl3101,plain,
( ( e11 = e13 )
| ( ( op1 @ e11 @ e13 )
= e13 ) ),
inference('sup+',[status(thm)],[zip_derived_cl3088,zip_derived_cl1733]) ).
thf(zip_derived_cl193_092,plain,
e11 != e13,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl3103,plain,
( ( op1 @ e11 @ e13 )
= e13 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3101,zip_derived_cl193]) ).
thf(zip_derived_cl3158,plain,
( zip_tseitin_14
| ( e13 = e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl2244,zip_derived_cl3103]) ).
thf(zip_derived_cl193_093,plain,
e11 != e13,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl3159,plain,
zip_tseitin_14,
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3158,zip_derived_cl193]) ).
thf(zip_derived_cl3241,plain,
( ( op1 @ e12 @ e13 )
= e12 ),
inference(demod,[status(thm)],[zip_derived_cl249,zip_derived_cl3159]) ).
thf(zip_derived_cl3294,plain,
( ( op1 @ e12 @ e10 )
!= e12 ),
inference(demod,[status(thm)],[zip_derived_cl105,zip_derived_cl3241]) ).
thf(zip_derived_cl4159,plain,
( ( ( op1 @ e11 @ e10 )
= e11 )
| zip_tseitin_3 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2377,zip_derived_cl3294]) ).
thf(zip_derived_cl4161,plain,
( ( ( op1 @ e13 @ e10 )
= e13 )
| ( ( op1 @ e11 @ e10 )
= e11 ) ),
inference('sup+',[status(thm)],[zip_derived_cl227,zip_derived_cl4159]) ).
thf(zip_derived_cl101,plain,
( ( op1 @ e13 @ e10 )
!= ( op1 @ e13 @ e11 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl254,plain,
( zip_tseitin_7
| zip_tseitin_6
| zip_tseitin_5
| zip_tseitin_4 ),
inference(cnf,[status(esa)],[zf_stmt_66]) ).
thf(zip_derived_cl231,plain,
( ( ( op1 @ e11 @ e11 )
= e11 )
| ~ zip_tseitin_5 ),
inference(cnf,[status(esa)],[zf_stmt_56]) ).
thf(zip_derived_cl230,plain,
( ( ( op1 @ e11 @ e11 )
!= e11 )
| ~ zip_tseitin_5 ),
inference(cnf,[status(esa)],[zf_stmt_56]) ).
thf(zip_derived_cl1432,plain,
~ zip_tseitin_5,
inference(clc,[status(thm)],[zip_derived_cl231,zip_derived_cl230]) ).
thf(zip_derived_cl1482,plain,
( zip_tseitin_7
| zip_tseitin_6
| zip_tseitin_4 ),
inference(demod,[status(thm)],[zip_derived_cl254,zip_derived_cl1432]) ).
thf(zip_derived_cl229,plain,
( ( ( op1 @ e10 @ e11 )
= e10 )
| ~ zip_tseitin_4 ),
inference(cnf,[status(esa)],[zf_stmt_58]) ).
thf(zip_derived_cl1484,plain,
( zip_tseitin_6
| zip_tseitin_7
| ( ( op1 @ e10 @ e11 )
= e10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl1482,zip_derived_cl229]) ).
thf(zip_derived_cl233,plain,
( ( ( op1 @ e12 @ e11 )
= e12 )
| ~ zip_tseitin_6 ),
inference(cnf,[status(esa)],[zf_stmt_54]) ).
thf(zip_derived_cl2374,plain,
( ( ( op1 @ e10 @ e11 )
= e10 )
| zip_tseitin_7
| ( ( op1 @ e12 @ e11 )
= e12 ) ),
inference('sup-',[status(thm)],[zip_derived_cl1484,zip_derived_cl233]) ).
thf(zip_derived_cl103,plain,
( ( op1 @ e12 @ e11 )
!= ( op1 @ e12 @ e13 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl3241_094,plain,
( ( op1 @ e12 @ e13 )
= e12 ),
inference(demod,[status(thm)],[zip_derived_cl249,zip_derived_cl3159]) ).
thf(zip_derived_cl3293,plain,
( ( op1 @ e12 @ e11 )
!= e12 ),
inference(demod,[status(thm)],[zip_derived_cl103,zip_derived_cl3241]) ).
thf(zip_derived_cl3910,plain,
( ( ( op1 @ e10 @ e11 )
= e10 )
| zip_tseitin_7 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2374,zip_derived_cl3293]) ).
thf(zip_derived_cl235,plain,
( ( ( op1 @ e13 @ e11 )
= e13 )
| ~ zip_tseitin_7 ),
inference(cnf,[status(esa)],[zf_stmt_52]) ).
thf(zip_derived_cl3911,plain,
( ( ( op1 @ e10 @ e11 )
= e10 )
| ( ( op1 @ e13 @ e11 )
= e13 ) ),
inference('sup-',[status(thm)],[zip_derived_cl3910,zip_derived_cl235]) ).
thf(zip_derived_cl32,plain,
( ( ( op1 @ e13 @ e11 )
= e13 )
| ( ( op1 @ e12 @ e11 )
= e13 )
| ( ( op1 @ e11 @ e11 )
= e13 )
| ( ( op1 @ e10 @ e11 )
= e13 ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl104,plain,
( ( op1 @ e12 @ e11 )
!= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl292_095,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl1435,plain,
( ( op1 @ e12 @ e11 )
!= e13 ),
inference(demod,[status(thm)],[zip_derived_cl104,zip_derived_cl292]) ).
thf(zip_derived_cl2112,plain,
( ( ( op1 @ e13 @ e11 )
= e13 )
| ( ( op1 @ e11 @ e11 )
= e13 )
| ( ( op1 @ e10 @ e11 )
= e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl32,zip_derived_cl1435]) ).
thf(zip_derived_cl3920,plain,
( ( e10 = e13 )
| ( ( op1 @ e13 @ e11 )
= e13 )
| ( ( op1 @ e11 @ e11 )
= e13 )
| ( ( op1 @ e13 @ e11 )
= e13 ) ),
inference('sup+',[status(thm)],[zip_derived_cl3911,zip_derived_cl2112]) ).
thf(zip_derived_cl3926,plain,
( ( ( op1 @ e11 @ e11 )
= e13 )
| ( ( op1 @ e13 @ e11 )
= e13 )
| ( e10 = e13 ) ),
inference(simplify,[status(thm)],[zip_derived_cl3920]) ).
thf(zip_derived_cl195_096,plain,
e10 != e13,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl109,plain,
( ( op1 @ e11 @ e11 )
!= ( op1 @ e11 @ e13 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl3103_097,plain,
( ( op1 @ e11 @ e13 )
= e13 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3101,zip_derived_cl193]) ).
thf(zip_derived_cl3149,plain,
( ( op1 @ e11 @ e11 )
!= e13 ),
inference(demod,[status(thm)],[zip_derived_cl109,zip_derived_cl3103]) ).
thf(zip_derived_cl3927,plain,
( ( op1 @ e13 @ e11 )
= e13 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3926,zip_derived_cl195,zip_derived_cl3149]) ).
thf(zip_derived_cl3934,plain,
( ( op1 @ e13 @ e10 )
!= e13 ),
inference(demod,[status(thm)],[zip_derived_cl101,zip_derived_cl3927]) ).
thf(zip_derived_cl4162,plain,
( ( op1 @ e11 @ e10 )
= e11 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl4161,zip_derived_cl3934]) ).
thf(zip_derived_cl4166,plain,
( e11
!= ( op1 @ e11 @ e12 ) ),
inference(demod,[status(thm)],[zip_derived_cl112,zip_derived_cl4162]) ).
thf(zip_derived_cl4183,plain,
( ( e11 != e11 )
| ( ( op1 @ e13 @ e12 )
= e11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl3124,zip_derived_cl4166]) ).
thf(zip_derived_cl4187,plain,
( ( op1 @ e13 @ e12 )
= e11 ),
inference(simplify,[status(thm)],[zip_derived_cl4183]) ).
thf(zip_derived_cl3738_098,plain,
( ( h2 @ e11 )
= e22 ),
inference(demod,[status(thm)],[zip_derived_cl3505,zip_derived_cl3737,zip_derived_cl3389]) ).
thf(zip_derived_cl3470_099,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl305_100,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl62,plain,
( ( ( op2 @ e20 @ e21 )
= e23 )
| ( ( op2 @ e20 @ e21 )
= e22 )
| ( ( op2 @ e20 @ e21 )
= e21 )
| ( ( op2 @ e20 @ e21 )
= e20 ) ),
inference(cnf,[status(esa)],[ax3]) ).
thf(zip_derived_cl1756_101,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_102,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_103,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_104,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_105,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl2544,plain,
( ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e23 )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e22 )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e21 )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl62,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl1756]) ).
thf(zip_derived_cl3354_106,plain,
( ( op2 @ ( h4 @ e13 ) @ e21 )
!= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl2494,zip_derived_cl3316]) ).
thf(zip_derived_cl3438,plain,
( ( ( h4 @ e13 )
!= ( h4 @ e13 ) )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e21 )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e22 )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e23 ) ),
inference('sup-',[status(thm)],[zip_derived_cl2544,zip_derived_cl3354]) ).
thf(zip_derived_cl3440,plain,
( ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e23 )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e22 )
| ( ( op2 @ ( h4 @ e13 ) @ e21 )
= e21 ) ),
inference(simplify,[status(thm)],[zip_derived_cl3438]) ).
thf(zip_derived_cl163,plain,
( ( op2 @ e20 @ e21 )
!= ( op2 @ e20 @ e23 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1756_107,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_108,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1764,plain,
( ( op2 @ ( h4 @ e13 ) @ e21 )
!= ( op2 @ ( h4 @ e13 ) @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl163,zip_derived_cl1756,zip_derived_cl1756]) ).
thf(zip_derived_cl3106_109,plain,
( e21
= ( op2 @ ( h4 @ e13 ) @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl296,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310,zip_derived_cl295]) ).
thf(zip_derived_cl3108,plain,
( ( op2 @ ( h4 @ e13 ) @ e21 )
!= e21 ),
inference(demod,[status(thm)],[zip_derived_cl1764,zip_derived_cl3106]) ).
thf(zip_derived_cl1770_110,plain,
( ( op2 @ ( h4 @ e13 ) @ e21 )
!= ( op2 @ e23 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl183,zip_derived_cl1756]) ).
thf(zip_derived_cl3255_111,plain,
( ( op2 @ e23 @ e21 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl271,zip_derived_cl3254]) ).
thf(zip_derived_cl3320,plain,
( ( op2 @ ( h4 @ e13 ) @ e21 )
!= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1770,zip_derived_cl3255]) ).
thf(zip_derived_cl3441,plain,
( ( op2 @ ( h4 @ e13 ) @ e21 )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3440,zip_derived_cl3108,zip_derived_cl3320]) ).
thf(zip_derived_cl3927_112,plain,
( ( op1 @ e13 @ e11 )
= e13 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3926,zip_derived_cl195,zip_derived_cl3149]) ).
thf(zip_derived_cl3470_113,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl3470_114,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl3738_115,plain,
( ( h2 @ e11 )
= e22 ),
inference(demod,[status(thm)],[zip_derived_cl3505,zip_derived_cl3737,zip_derived_cl3389]) ).
thf(zip_derived_cl273,plain,
( ( ( op2 @ e20 @ e22 )
= e20 )
| ~ zip_tseitin_24 ),
inference(cnf,[status(esa)],[zf_stmt_16]) ).
thf(zip_derived_cl1756_116,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_117,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1791,plain,
( ( ( op2 @ ( h4 @ e13 ) @ e22 )
= ( h4 @ e13 ) )
| ~ zip_tseitin_24 ),
inference(demod,[status(thm)],[zip_derived_cl273,zip_derived_cl1756,zip_derived_cl1756]) ).
thf(zip_derived_cl289,plain,
( zip_tseitin_27
| zip_tseitin_26
| zip_tseitin_25
| zip_tseitin_24 ),
inference(cnf,[status(esa)],[zf_stmt_33]) ).
thf(zip_derived_cl279,plain,
( ( ( op2 @ e23 @ e22 )
= e23 )
| ~ zip_tseitin_27 ),
inference(cnf,[status(esa)],[zf_stmt_10]) ).
thf(zip_derived_cl174,plain,
( ( op2 @ e22 @ e22 )
!= ( op2 @ e23 @ e22 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl295_118,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl1496,plain,
( e23
!= ( op2 @ e23 @ e22 ) ),
inference(demod,[status(thm)],[zip_derived_cl174,zip_derived_cl295]) ).
thf(zip_derived_cl1571,plain,
~ zip_tseitin_27,
inference('simplify_reflect-',[status(thm)],[zip_derived_cl279,zip_derived_cl1496]) ).
thf(zip_derived_cl1572,plain,
( zip_tseitin_26
| zip_tseitin_25
| zip_tseitin_24 ),
inference(demod,[status(thm)],[zip_derived_cl289,zip_derived_cl1571]) ).
thf(zip_derived_cl295_119,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl277,plain,
( ( ( op2 @ e22 @ e22 )
= e22 )
| ~ zip_tseitin_26 ),
inference(cnf,[status(esa)],[zf_stmt_12]) ).
thf(zip_derived_cl1569,plain,
( ( e23 = e22 )
| ~ zip_tseitin_26 ),
inference('sup+',[status(thm)],[zip_derived_cl295,zip_derived_cl277]) ).
thf(zip_derived_cl198,plain,
e22 != e23,
inference(cnf,[status(esa)],[ax8]) ).
thf(zip_derived_cl1570,plain,
~ zip_tseitin_26,
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1569,zip_derived_cl198]) ).
thf(zip_derived_cl1578,plain,
( zip_tseitin_25
| zip_tseitin_24 ),
inference(demod,[status(thm)],[zip_derived_cl1572,zip_derived_cl1570]) ).
thf(zip_derived_cl275,plain,
( ( ( op2 @ e21 @ e22 )
= e21 )
| ~ zip_tseitin_25 ),
inference(cnf,[status(esa)],[zf_stmt_14]) ).
thf(zip_derived_cl1517_120,plain,
( zip_tseitin_17
| zip_tseitin_18
| zip_tseitin_19 ),
inference(clc,[status(thm)],[zip_derived_cl291,zip_derived_cl1508]) ).
thf(zip_derived_cl259_121,plain,
( ( ( op2 @ e21 @ e20 )
= e21 )
| ~ zip_tseitin_17 ),
inference(cnf,[status(esa)],[zf_stmt_30]) ).
thf(zip_derived_cl160,plain,
( ( op2 @ e21 @ e20 )
!= ( op2 @ e21 @ e22 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1510,plain,
( ( e21
!= ( op2 @ e21 @ e22 ) )
| ~ zip_tseitin_17 ),
inference('sup-',[status(thm)],[zip_derived_cl259,zip_derived_cl160]) ).
thf(zip_derived_cl1520,plain,
( zip_tseitin_19
| zip_tseitin_18
| ( e21
!= ( op2 @ e21 @ e22 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl1517,zip_derived_cl1510]) ).
thf(zip_derived_cl2481_122,plain,
~ zip_tseitin_18,
inference(simplify,[status(thm)],[zip_derived_cl2480]) ).
thf(zip_derived_cl2493,plain,
( zip_tseitin_19
| ( e21
!= ( op2 @ e21 @ e22 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1520,zip_derived_cl2481]) ).
thf(zip_derived_cl2680,plain,
( ( e21 != e21 )
| ~ zip_tseitin_25
| zip_tseitin_19 ),
inference('sup-',[status(thm)],[zip_derived_cl275,zip_derived_cl2493]) ).
thf(zip_derived_cl2682,plain,
( zip_tseitin_19
| ~ zip_tseitin_25 ),
inference(simplify,[status(thm)],[zip_derived_cl2680]) ).
thf(zip_derived_cl1529_123,plain,
( ( e23
!= ( op2 @ e23 @ e21 ) )
| ~ zip_tseitin_19 ),
inference('sup-',[status(thm)],[zip_derived_cl263,zip_derived_cl149]) ).
thf(zip_derived_cl2755,plain,
( ~ zip_tseitin_25
| ( e23
!= ( op2 @ e23 @ e21 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2682,zip_derived_cl1529]) ).
thf(zip_derived_cl3255_124,plain,
( ( op2 @ e23 @ e21 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl271,zip_derived_cl3254]) ).
thf(zip_derived_cl3327,plain,
( ~ zip_tseitin_25
| ( e23 != e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl2755,zip_derived_cl3255]) ).
thf(zip_derived_cl3328,plain,
~ zip_tseitin_25,
inference(simplify,[status(thm)],[zip_derived_cl3327]) ).
thf(zip_derived_cl3359,plain,
zip_tseitin_24,
inference(demod,[status(thm)],[zip_derived_cl1578,zip_derived_cl3328]) ).
thf(zip_derived_cl3369,plain,
( ( op2 @ ( h4 @ e13 ) @ e22 )
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl1791,zip_derived_cl3359]) ).
thf(zip_derived_cl19,plain,
( ( ( op1 @ e13 @ e13 )
= e12 )
| ( ( op1 @ e13 @ e12 )
= e12 )
| ( ( op1 @ e13 @ e11 )
= e12 )
| ( ( op1 @ e13 @ e10 )
= e12 ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl1697_125,plain,
( e10
= ( op1 @ e13 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl294,zip_derived_cl292,zip_derived_cl292]) ).
thf(zip_derived_cl1899,plain,
( ( e10 = e12 )
| ( ( op1 @ e13 @ e12 )
= e12 )
| ( ( op1 @ e13 @ e11 )
= e12 )
| ( ( op1 @ e13 @ e10 )
= e12 ) ),
inference(demod,[status(thm)],[zip_derived_cl19,zip_derived_cl1697]) ).
thf(zip_derived_cl196,plain,
e10 != e12,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl1900,plain,
( ( ( op1 @ e13 @ e12 )
= e12 )
| ( ( op1 @ e13 @ e11 )
= e12 )
| ( ( op1 @ e13 @ e10 )
= e12 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1899,zip_derived_cl196]) ).
thf(zip_derived_cl3927_126,plain,
( ( op1 @ e13 @ e11 )
= e13 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3926,zip_derived_cl195,zip_derived_cl3149]) ).
thf(zip_derived_cl3939,plain,
( ( ( op1 @ e13 @ e12 )
= e12 )
| ( e13 = e12 )
| ( ( op1 @ e13 @ e10 )
= e12 ) ),
inference(demod,[status(thm)],[zip_derived_cl1900,zip_derived_cl3927]) ).
thf(zip_derived_cl192,plain,
e12 != e13,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl3940,plain,
( ( ( op1 @ e13 @ e12 )
= e12 )
| ( ( op1 @ e13 @ e10 )
= e12 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3939,zip_derived_cl192]) ).
thf(zip_derived_cl4187_127,plain,
( ( op1 @ e13 @ e12 )
= e11 ),
inference(simplify,[status(thm)],[zip_derived_cl4183]) ).
thf(zip_derived_cl4246,plain,
( ( e11 = e12 )
| ( ( op1 @ e13 @ e10 )
= e12 ) ),
inference(demod,[status(thm)],[zip_derived_cl3940,zip_derived_cl4187]) ).
thf(zip_derived_cl194,plain,
e11 != e12,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl4247,plain,
( ( op1 @ e13 @ e10 )
= e12 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl4246,zip_derived_cl194]) ).
thf(zip_derived_cl305_128,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl3470_129,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl3737_130,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl3106_131,plain,
( e21
= ( op2 @ ( h4 @ e13 ) @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl296,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310,zip_derived_cl295]) ).
thf(zip_derived_cl3241_132,plain,
( ( op1 @ e12 @ e13 )
= e12 ),
inference(demod,[status(thm)],[zip_derived_cl249,zip_derived_cl3159]) ).
thf(zip_derived_cl305_133,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl305_134,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl3470_135,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl259_136,plain,
( ( ( op2 @ e21 @ e20 )
= e21 )
| ~ zip_tseitin_17 ),
inference(cnf,[status(esa)],[zf_stmt_30]) ).
thf(zip_derived_cl1756_137,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1783,plain,
( ( ( op2 @ e21 @ ( h4 @ e13 ) )
= e21 )
| ~ zip_tseitin_17 ),
inference(demod,[status(thm)],[zip_derived_cl259,zip_derived_cl1756]) ).
thf(zip_derived_cl2491_138,plain,
( zip_tseitin_17
| zip_tseitin_19 ),
inference(demod,[status(thm)],[zip_derived_cl1517,zip_derived_cl2481]) ).
thf(zip_derived_cl3316_139,plain,
~ zip_tseitin_19,
inference(simplify,[status(thm)],[zip_derived_cl3315]) ).
thf(zip_derived_cl3352,plain,
zip_tseitin_17,
inference(demod,[status(thm)],[zip_derived_cl2491,zip_derived_cl3316]) ).
thf(zip_derived_cl3366,plain,
( ( op2 @ e21 @ ( h4 @ e13 ) )
= e21 ),
inference(demod,[status(thm)],[zip_derived_cl1783,zip_derived_cl3352]) ).
thf(zip_derived_cl292_140,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl3470_141,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl305_142,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl305_143,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl302_144,plain,
( ( h2 @ e13 )
= ( op2 @ e21 @ e21 ) ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl3470_145,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl3500,plain,
( ( h4 @ e13 )
= ( op2 @ e21 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl302,zip_derived_cl3470]) ).
thf(zip_derived_cl36,plain,
( ( ( op1 @ e13 @ e11 )
= e11 )
| ( ( op1 @ e12 @ e11 )
= e11 )
| ( ( op1 @ e11 @ e11 )
= e11 )
| ( ( op1 @ e10 @ e11 )
= e11 ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl3927_146,plain,
( ( op1 @ e13 @ e11 )
= e13 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3926,zip_derived_cl195,zip_derived_cl3149]) ).
thf(zip_derived_cl3931,plain,
( ( e13 = e11 )
| ( ( op1 @ e12 @ e11 )
= e11 )
| ( ( op1 @ e11 @ e11 )
= e11 )
| ( ( op1 @ e10 @ e11 )
= e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl36,zip_derived_cl3927]) ).
thf(zip_derived_cl115,plain,
( ( op1 @ e10 @ e11 )
!= ( op1 @ e10 @ e13 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl3088_147,plain,
( e11
= ( op1 @ e10 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl293,zip_derived_cl292,zip_derived_cl292,zip_derived_cl1697,zip_derived_cl292]) ).
thf(zip_derived_cl3092,plain,
( ( op1 @ e10 @ e11 )
!= e11 ),
inference(demod,[status(thm)],[zip_derived_cl115,zip_derived_cl3088]) ).
thf(zip_derived_cl193_148,plain,
e11 != e13,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl3932,plain,
( ( ( op1 @ e12 @ e11 )
= e11 )
| ( ( op1 @ e11 @ e11 )
= e11 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3931,zip_derived_cl3092,zip_derived_cl193]) ).
thf(zip_derived_cl113,plain,
( ( op1 @ e11 @ e10 )
!= ( op1 @ e11 @ e11 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl4162_149,plain,
( ( op1 @ e11 @ e10 )
= e11 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl4161,zip_derived_cl3934]) ).
thf(zip_derived_cl4167,plain,
( e11
!= ( op1 @ e11 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl113,zip_derived_cl4162]) ).
thf(zip_derived_cl4190,plain,
( ( e11 != e11 )
| ( ( op1 @ e12 @ e11 )
= e11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl3932,zip_derived_cl4167]) ).
thf(zip_derived_cl4193,plain,
( ( op1 @ e12 @ e11 )
= e11 ),
inference(simplify,[status(thm)],[zip_derived_cl4190]) ).
thf(zip_derived_cl3738_150,plain,
( ( h2 @ e11 )
= e22 ),
inference(demod,[status(thm)],[zip_derived_cl3505,zip_derived_cl3737,zip_derived_cl3389]) ).
thf(zip_derived_cl305_151,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl3738_152,plain,
( ( h2 @ e11 )
= e22 ),
inference(demod,[status(thm)],[zip_derived_cl3505,zip_derived_cl3737,zip_derived_cl3389]) ).
thf(zip_derived_cl57,plain,
( ( ( op2 @ e21 @ e22 )
= e23 )
| ( ( op2 @ e21 @ e22 )
= e22 )
| ( ( op2 @ e21 @ e22 )
= e21 )
| ( ( op2 @ e21 @ e22 )
= e20 ) ),
inference(cnf,[status(esa)],[ax3]) ).
thf(zip_derived_cl1756_153,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl2461,plain,
( ( ( op2 @ e21 @ e22 )
= e23 )
| ( ( op2 @ e21 @ e22 )
= e22 )
| ( ( op2 @ e21 @ e22 )
= e21 )
| ( ( op2 @ e21 @ e22 )
= ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl57,zip_derived_cl1756]) ).
thf(zip_derived_cl176,plain,
( ( op2 @ e21 @ e22 )
!= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl295_154,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl1497,plain,
( ( op2 @ e21 @ e22 )
!= e23 ),
inference(demod,[status(thm)],[zip_derived_cl176,zip_derived_cl295]) ).
thf(zip_derived_cl2462,plain,
( ( ( op2 @ e21 @ e22 )
= e22 )
| ( ( op2 @ e21 @ e22 )
= e21 )
| ( ( op2 @ e21 @ e22 )
= ( h4 @ e13 ) ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2461,zip_derived_cl1497]) ).
thf(zip_derived_cl1578_155,plain,
( zip_tseitin_25
| zip_tseitin_24 ),
inference(demod,[status(thm)],[zip_derived_cl1572,zip_derived_cl1570]) ).
thf(zip_derived_cl273_156,plain,
( ( ( op2 @ e20 @ e22 )
= e20 )
| ~ zip_tseitin_24 ),
inference(cnf,[status(esa)],[zf_stmt_16]) ).
thf(zip_derived_cl179,plain,
( ( op2 @ e20 @ e22 )
!= ( op2 @ e21 @ e22 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1565,plain,
( ( e20
!= ( op2 @ e21 @ e22 ) )
| ~ zip_tseitin_24 ),
inference('sup-',[status(thm)],[zip_derived_cl273,zip_derived_cl179]) ).
thf(zip_derived_cl1596,plain,
( zip_tseitin_25
| ( e20
!= ( op2 @ e21 @ e22 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl1578,zip_derived_cl1565]) ).
thf(zip_derived_cl1756_157,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1819,plain,
( zip_tseitin_25
| ( ( h4 @ e13 )
!= ( op2 @ e21 @ e22 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1596,zip_derived_cl1756]) ).
thf(zip_derived_cl3328_158,plain,
~ zip_tseitin_25,
inference(simplify,[status(thm)],[zip_derived_cl3327]) ).
thf(zip_derived_cl3360,plain,
( ( h4 @ e13 )
!= ( op2 @ e21 @ e22 ) ),
inference(demod,[status(thm)],[zip_derived_cl1819,zip_derived_cl3328]) ).
thf(zip_derived_cl3409,plain,
( ( ( h4 @ e13 )
!= ( h4 @ e13 ) )
| ( ( op2 @ e21 @ e22 )
= e21 )
| ( ( op2 @ e21 @ e22 )
= e22 ) ),
inference('sup-',[status(thm)],[zip_derived_cl2462,zip_derived_cl3360]) ).
thf(zip_derived_cl3410,plain,
( ( ( op2 @ e21 @ e22 )
= e22 )
| ( ( op2 @ e21 @ e22 )
= e21 ) ),
inference(simplify,[status(thm)],[zip_derived_cl3409]) ).
thf(zip_derived_cl2493_159,plain,
( zip_tseitin_19
| ( e21
!= ( op2 @ e21 @ e22 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1520,zip_derived_cl2481]) ).
thf(zip_derived_cl3316_160,plain,
~ zip_tseitin_19,
inference(simplify,[status(thm)],[zip_derived_cl3315]) ).
thf(zip_derived_cl3353,plain,
( e21
!= ( op2 @ e21 @ e22 ) ),
inference(demod,[status(thm)],[zip_derived_cl2493,zip_derived_cl3316]) ).
thf(zip_derived_cl3411,plain,
( ( op2 @ e21 @ e22 )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3410,zip_derived_cl3353]) ).
thf(zip_derived_cl31,plain,
( ( ( op1 @ e12 @ e13 )
= e10 )
| ( ( op1 @ e12 @ e12 )
= e10 )
| ( ( op1 @ e12 @ e11 )
= e10 )
| ( ( op1 @ e12 @ e10 )
= e10 ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl292_161,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl2100,plain,
( ( ( op1 @ e12 @ e13 )
= e10 )
| ( e13 = e10 )
| ( ( op1 @ e12 @ e11 )
= e10 )
| ( ( op1 @ e12 @ e10 )
= e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl31,zip_derived_cl292]) ).
thf(zip_derived_cl195_162,plain,
e10 != e13,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl120,plain,
( ( op1 @ e12 @ e13 )
!= ( op1 @ e13 @ e13 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1697_163,plain,
( e10
= ( op1 @ e13 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl294,zip_derived_cl292,zip_derived_cl292]) ).
thf(zip_derived_cl1701,plain,
( ( op1 @ e12 @ e13 )
!= e10 ),
inference(demod,[status(thm)],[zip_derived_cl120,zip_derived_cl1697]) ).
thf(zip_derived_cl2101,plain,
( ( ( op1 @ e12 @ e11 )
= e10 )
| ( ( op1 @ e12 @ e10 )
= e10 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2100,zip_derived_cl195,zip_derived_cl1701]) ).
thf(zip_derived_cl4193_164,plain,
( ( op1 @ e12 @ e11 )
= e11 ),
inference(simplify,[status(thm)],[zip_derived_cl4190]) ).
thf(zip_derived_cl4298,plain,
( ( e11 = e10 )
| ( ( op1 @ e12 @ e10 )
= e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl2101,zip_derived_cl4193]) ).
thf(zip_derived_cl197,plain,
e10 != e11,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl4299,plain,
( ( op1 @ e12 @ e10 )
= e10 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl4298,zip_derived_cl197]) ).
thf(zip_derived_cl3737_165,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl305_166,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl3737_167,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl3106_168,plain,
( e21
= ( op2 @ ( h4 @ e13 ) @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl296,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310,zip_derived_cl295]) ).
thf(zip_derived_cl64,plain,
( ( ( op2 @ e23 @ e23 )
= e23 )
| ( ( op2 @ e22 @ e23 )
= e23 )
| ( ( op2 @ e21 @ e23 )
= e23 )
| ( ( op2 @ e20 @ e23 )
= e23 ) ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl310_169,plain,
( ( h4 @ e13 )
= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl2476_170,plain,
( ( op2 @ e22 @ e23 )
= e22 ),
inference(clc,[status(thm)],[zip_derived_cl2423,zip_derived_cl285]) ).
thf(zip_derived_cl1756_171,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl2568,plain,
( ( ( h4 @ e13 )
= e23 )
| ( e22 = e23 )
| ( ( op2 @ e21 @ e23 )
= e23 )
| ( ( op2 @ ( h4 @ e13 ) @ e23 )
= e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl64,zip_derived_cl310,zip_derived_cl2476,zip_derived_cl1756]) ).
thf(zip_derived_cl198_172,plain,
e22 != e23,
inference(cnf,[status(esa)],[ax8]) ).
thf(zip_derived_cl1775_173,plain,
( ( h4 @ e13 )
!= e23 ),
inference(demod,[status(thm)],[zip_derived_cl201,zip_derived_cl1756]) ).
thf(zip_derived_cl2569,plain,
( ( ( op2 @ e21 @ e23 )
= e23 )
| ( ( op2 @ ( h4 @ e13 ) @ e23 )
= e23 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2568,zip_derived_cl198,zip_derived_cl1775]) ).
thf(zip_derived_cl3115,plain,
( ( e21 = e23 )
| ( ( op2 @ e21 @ e23 )
= e23 ) ),
inference('sup+',[status(thm)],[zip_derived_cl3106,zip_derived_cl2569]) ).
thf(zip_derived_cl199_174,plain,
e21 != e23,
inference(cnf,[status(esa)],[ax8]) ).
thf(zip_derived_cl3116,plain,
( ( op2 @ e21 @ e23 )
= e23 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3115,zip_derived_cl199]) ).
thf(zip_derived_cl3103_175,plain,
( ( op1 @ e11 @ e13 )
= e13 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3101,zip_derived_cl193]) ).
thf(zip_derived_cl3470_176,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl3738_177,plain,
( ( h2 @ e11 )
= e22 ),
inference(demod,[status(thm)],[zip_derived_cl3505,zip_derived_cl3737,zip_derived_cl3389]) ).
thf(zip_derived_cl3470_178,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl79,plain,
( ( ( op2 @ e22 @ e23 )
= e20 )
| ( ( op2 @ e22 @ e22 )
= e20 )
| ( ( op2 @ e22 @ e21 )
= e20 )
| ( ( op2 @ e22 @ e20 )
= e20 ) ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl2476_179,plain,
( ( op2 @ e22 @ e23 )
= e22 ),
inference(clc,[status(thm)],[zip_derived_cl2423,zip_derived_cl285]) ).
thf(zip_derived_cl1756_180,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl295_181,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl1756_182,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_183,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_184,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_185,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl2735,plain,
( ( e22
= ( h4 @ e13 ) )
| ( e23
= ( h4 @ e13 ) )
| ( ( op2 @ e22 @ e21 )
= ( h4 @ e13 ) )
| ( ( op2 @ e22 @ ( h4 @ e13 ) )
= ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl79,zip_derived_cl2476,zip_derived_cl1756,zip_derived_cl295,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl1756,zip_derived_cl1756]) ).
thf(zip_derived_cl1775_186,plain,
( ( h4 @ e13 )
!= e23 ),
inference(demod,[status(thm)],[zip_derived_cl201,zip_derived_cl1756]) ).
thf(zip_derived_cl202,plain,
e20 != e22,
inference(cnf,[status(esa)],[ax8]) ).
thf(zip_derived_cl1756_187,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1776,plain,
( ( h4 @ e13 )
!= e22 ),
inference(demod,[status(thm)],[zip_derived_cl202,zip_derived_cl1756]) ).
thf(zip_derived_cl2736,plain,
( ( ( op2 @ e22 @ e21 )
= ( h4 @ e13 ) )
| ( ( op2 @ e22 @ ( h4 @ e13 ) )
= ( h4 @ e13 ) ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2735,zip_derived_cl1775,zip_derived_cl1776]) ).
thf(zip_derived_cl3394_188,plain,
( ( op2 @ e22 @ e21 )
= e21 ),
inference(simplify,[status(thm)],[zip_derived_cl3391]) ).
thf(zip_derived_cl3467,plain,
( ( e21
= ( h4 @ e13 ) )
| ( ( op2 @ e22 @ ( h4 @ e13 ) )
= ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2736,zip_derived_cl3394]) ).
thf(zip_derived_cl1777_189,plain,
( ( h4 @ e13 )
!= e21 ),
inference(demod,[status(thm)],[zip_derived_cl203,zip_derived_cl1756]) ).
thf(zip_derived_cl3468,plain,
( ( op2 @ e22 @ ( h4 @ e13 ) )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3467,zip_derived_cl1777]) ).
thf(ax1,axiom,
( ( ( ( op1 @ e13 @ e13 )
= e13 )
| ( ( op1 @ e13 @ e13 )
= e12 )
| ( ( op1 @ e13 @ e13 )
= e11 )
| ( ( op1 @ e13 @ e13 )
= e10 ) )
& ( ( ( op1 @ e13 @ e12 )
= e13 )
| ( ( op1 @ e13 @ e12 )
= e12 )
| ( ( op1 @ e13 @ e12 )
= e11 )
| ( ( op1 @ e13 @ e12 )
= e10 ) )
& ( ( ( op1 @ e13 @ e11 )
= e13 )
| ( ( op1 @ e13 @ e11 )
= e12 )
| ( ( op1 @ e13 @ e11 )
= e11 )
| ( ( op1 @ e13 @ e11 )
= e10 ) )
& ( ( ( op1 @ e13 @ e10 )
= e13 )
| ( ( op1 @ e13 @ e10 )
= e12 )
| ( ( op1 @ e13 @ e10 )
= e11 )
| ( ( op1 @ e13 @ e10 )
= e10 ) )
& ( ( ( op1 @ e12 @ e13 )
= e13 )
| ( ( op1 @ e12 @ e13 )
= e12 )
| ( ( op1 @ e12 @ e13 )
= e11 )
| ( ( op1 @ e12 @ e13 )
= e10 ) )
& ( ( ( op1 @ e12 @ e12 )
= e13 )
| ( ( op1 @ e12 @ e12 )
= e12 )
| ( ( op1 @ e12 @ e12 )
= e11 )
| ( ( op1 @ e12 @ e12 )
= e10 ) )
& ( ( ( op1 @ e12 @ e11 )
= e13 )
| ( ( op1 @ e12 @ e11 )
= e12 )
| ( ( op1 @ e12 @ e11 )
= e11 )
| ( ( op1 @ e12 @ e11 )
= e10 ) )
& ( ( ( op1 @ e12 @ e10 )
= e13 )
| ( ( op1 @ e12 @ e10 )
= e12 )
| ( ( op1 @ e12 @ e10 )
= e11 )
| ( ( op1 @ e12 @ e10 )
= e10 ) )
& ( ( ( op1 @ e11 @ e13 )
= e13 )
| ( ( op1 @ e11 @ e13 )
= e12 )
| ( ( op1 @ e11 @ e13 )
= e11 )
| ( ( op1 @ e11 @ e13 )
= e10 ) )
& ( ( ( op1 @ e11 @ e12 )
= e13 )
| ( ( op1 @ e11 @ e12 )
= e12 )
| ( ( op1 @ e11 @ e12 )
= e11 )
| ( ( op1 @ e11 @ e12 )
= e10 ) )
& ( ( ( op1 @ e11 @ e11 )
= e13 )
| ( ( op1 @ e11 @ e11 )
= e12 )
| ( ( op1 @ e11 @ e11 )
= e11 )
| ( ( op1 @ e11 @ e11 )
= e10 ) )
& ( ( ( op1 @ e11 @ e10 )
= e13 )
| ( ( op1 @ e11 @ e10 )
= e12 )
| ( ( op1 @ e11 @ e10 )
= e11 )
| ( ( op1 @ e11 @ e10 )
= e10 ) )
& ( ( ( op1 @ e10 @ e13 )
= e13 )
| ( ( op1 @ e10 @ e13 )
= e12 )
| ( ( op1 @ e10 @ e13 )
= e11 )
| ( ( op1 @ e10 @ e13 )
= e10 ) )
& ( ( ( op1 @ e10 @ e12 )
= e13 )
| ( ( op1 @ e10 @ e12 )
= e12 )
| ( ( op1 @ e10 @ e12 )
= e11 )
| ( ( op1 @ e10 @ e12 )
= e10 ) )
& ( ( ( op1 @ e10 @ e11 )
= e13 )
| ( ( op1 @ e10 @ e11 )
= e12 )
| ( ( op1 @ e10 @ e11 )
= e11 )
| ( ( op1 @ e10 @ e11 )
= e10 ) )
& ( ( ( op1 @ e10 @ e10 )
= e13 )
| ( ( op1 @ e10 @ e10 )
= e12 )
| ( ( op1 @ e10 @ e10 )
= e11 )
| ( ( op1 @ e10 @ e10 )
= e10 ) ) ) ).
thf(zip_derived_cl9,plain,
( ( ( op1 @ e11 @ e12 )
= e13 )
| ( ( op1 @ e11 @ e12 )
= e12 )
| ( ( op1 @ e11 @ e12 )
= e11 )
| ( ( op1 @ e11 @ e12 )
= e10 ) ),
inference(cnf,[status(esa)],[ax1]) ).
thf(zip_derived_cl253,plain,
( zip_tseitin_11
| zip_tseitin_10
| zip_tseitin_9
| zip_tseitin_8 ),
inference(cnf,[status(esa)],[zf_stmt_66]) ).
thf(zip_derived_cl241,plain,
( ( ( op1 @ e12 @ e12 )
= e12 )
| ~ zip_tseitin_10 ),
inference(cnf,[status(esa)],[zf_stmt_46]) ).
thf(zip_derived_cl240,plain,
( ( ( op1 @ e12 @ e12 )
!= e12 )
| ~ zip_tseitin_10 ),
inference(cnf,[status(esa)],[zf_stmt_46]) ).
thf(zip_derived_cl1433,plain,
~ zip_tseitin_10,
inference(clc,[status(thm)],[zip_derived_cl241,zip_derived_cl240]) ).
thf(zip_derived_cl1478,plain,
( zip_tseitin_11
| zip_tseitin_9
| zip_tseitin_8 ),
inference(demod,[status(thm)],[zip_derived_cl253,zip_derived_cl1433]) ).
thf(zip_derived_cl237,plain,
( ( ( op1 @ e10 @ e12 )
= e10 )
| ~ zip_tseitin_8 ),
inference(cnf,[status(esa)],[zf_stmt_50]) ).
thf(zip_derived_cl1480,plain,
( zip_tseitin_9
| zip_tseitin_11
| ( ( op1 @ e10 @ e12 )
= e10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl1478,zip_derived_cl237]) ).
thf(zip_derived_cl242,plain,
( ( ( op1 @ e12 @ e13 )
!= e12 )
| ~ zip_tseitin_11 ),
inference(cnf,[status(esa)],[zf_stmt_44]) ).
thf(zip_derived_cl3241_190,plain,
( ( op1 @ e12 @ e13 )
= e12 ),
inference(demod,[status(thm)],[zip_derived_cl249,zip_derived_cl3159]) ).
thf(zip_derived_cl3295,plain,
( ( e12 != e12 )
| ~ zip_tseitin_11 ),
inference(demod,[status(thm)],[zip_derived_cl242,zip_derived_cl3241]) ).
thf(zip_derived_cl3296,plain,
~ zip_tseitin_11,
inference(simplify,[status(thm)],[zip_derived_cl3295]) ).
thf(zip_derived_cl3304,plain,
( zip_tseitin_9
| ( ( op1 @ e10 @ e12 )
= e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl1480,zip_derived_cl3296]) ).
thf(zip_derived_cl239,plain,
( ( ( op1 @ e11 @ e12 )
= e11 )
| ~ zip_tseitin_9 ),
inference(cnf,[status(esa)],[zf_stmt_48]) ).
thf(zip_derived_cl3543,plain,
( ( ( op1 @ e10 @ e12 )
= e10 )
| ( ( op1 @ e11 @ e12 )
= e11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl3304,zip_derived_cl239]) ).
thf(zip_derived_cl131,plain,
( ( op1 @ e10 @ e12 )
!= ( op1 @ e11 @ e12 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl3824,plain,
( ( e10
!= ( op1 @ e11 @ e12 ) )
| ( ( op1 @ e11 @ e12 )
= e11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl3543,zip_derived_cl131]) ).
thf(zip_derived_cl3848,plain,
( ( e10 != e10 )
| ( ( op1 @ e11 @ e12 )
= e11 )
| ( ( op1 @ e11 @ e12 )
= e12 )
| ( ( op1 @ e11 @ e12 )
= e13 )
| ( ( op1 @ e11 @ e12 )
= e11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl9,zip_derived_cl3824]) ).
thf(zip_derived_cl3850,plain,
( ( ( op1 @ e11 @ e12 )
= e13 )
| ( ( op1 @ e11 @ e12 )
= e12 )
| ( ( op1 @ e11 @ e12 )
= e11 ) ),
inference(simplify,[status(thm)],[zip_derived_cl3848]) ).
thf(zip_derived_cl128,plain,
( ( op1 @ e11 @ e12 )
!= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl292_191,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl1438,plain,
( ( op1 @ e11 @ e12 )
!= e13 ),
inference(demod,[status(thm)],[zip_derived_cl128,zip_derived_cl292]) ).
thf(zip_derived_cl3851,plain,
( ( ( op1 @ e11 @ e12 )
= e12 )
| ( ( op1 @ e11 @ e12 )
= e11 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3850,zip_derived_cl1438]) ).
thf(zip_derived_cl4166_192,plain,
( e11
!= ( op1 @ e11 @ e12 ) ),
inference(demod,[status(thm)],[zip_derived_cl112,zip_derived_cl4162]) ).
thf(zip_derived_cl4184,plain,
( ( e11 != e11 )
| ( ( op1 @ e11 @ e12 )
= e12 ) ),
inference('sup-',[status(thm)],[zip_derived_cl3851,zip_derived_cl4166]) ).
thf(zip_derived_cl4188,plain,
( ( op1 @ e11 @ e12 )
= e12 ),
inference(simplify,[status(thm)],[zip_derived_cl4184]) ).
thf(zip_derived_cl305_193,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl3738_194,plain,
( ( h2 @ e11 )
= e22 ),
inference(demod,[status(thm)],[zip_derived_cl3505,zip_derived_cl3737,zip_derived_cl3389]) ).
thf(zip_derived_cl305_195,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl3394_196,plain,
( ( op2 @ e22 @ e21 )
= e21 ),
inference(simplify,[status(thm)],[zip_derived_cl3391]) ).
thf(zip_derived_cl39,plain,
( ( ( op1 @ e11 @ e13 )
= e10 )
| ( ( op1 @ e11 @ e12 )
= e10 )
| ( ( op1 @ e11 @ e11 )
= e10 )
| ( ( op1 @ e11 @ e10 )
= e10 ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl121,plain,
( ( op1 @ e11 @ e13 )
!= ( op1 @ e13 @ e13 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1697_197,plain,
( e10
= ( op1 @ e13 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl294,zip_derived_cl292,zip_derived_cl292]) ).
thf(zip_derived_cl1702,plain,
( ( op1 @ e11 @ e13 )
!= e10 ),
inference(demod,[status(thm)],[zip_derived_cl121,zip_derived_cl1697]) ).
thf(zip_derived_cl2202,plain,
( ( ( op1 @ e11 @ e12 )
= e10 )
| ( ( op1 @ e11 @ e11 )
= e10 )
| ( ( op1 @ e11 @ e10 )
= e10 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl39,zip_derived_cl1702]) ).
thf(zip_derived_cl4162_198,plain,
( ( op1 @ e11 @ e10 )
= e11 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl4161,zip_derived_cl3934]) ).
thf(zip_derived_cl4175,plain,
( ( ( op1 @ e11 @ e12 )
= e10 )
| ( ( op1 @ e11 @ e11 )
= e10 )
| ( e11 = e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl2202,zip_derived_cl4162]) ).
thf(zip_derived_cl197_199,plain,
e10 != e11,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl4176,plain,
( ( ( op1 @ e11 @ e12 )
= e10 )
| ( ( op1 @ e11 @ e11 )
= e10 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl4175,zip_derived_cl197]) ).
thf(zip_derived_cl4188_200,plain,
( ( op1 @ e11 @ e12 )
= e12 ),
inference(simplify,[status(thm)],[zip_derived_cl4184]) ).
thf(zip_derived_cl4386,plain,
( ( e12 = e10 )
| ( ( op1 @ e11 @ e11 )
= e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl4176,zip_derived_cl4188]) ).
thf(zip_derived_cl196_201,plain,
e10 != e12,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl4387,plain,
( ( op1 @ e11 @ e11 )
= e10 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl4386,zip_derived_cl196]) ).
thf(zip_derived_cl3737_202,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl3738_203,plain,
( ( h2 @ e11 )
= e22 ),
inference(demod,[status(thm)],[zip_derived_cl3505,zip_derived_cl3737,zip_derived_cl3389]) ).
thf(zip_derived_cl3738_204,plain,
( ( h2 @ e11 )
= e22 ),
inference(demod,[status(thm)],[zip_derived_cl3505,zip_derived_cl3737,zip_derived_cl3389]) ).
thf(zip_derived_cl295_205,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl4162_206,plain,
( ( op1 @ e11 @ e10 )
= e11 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl4161,zip_derived_cl3934]) ).
thf(zip_derived_cl3738_207,plain,
( ( h2 @ e11 )
= e22 ),
inference(demod,[status(thm)],[zip_derived_cl3505,zip_derived_cl3737,zip_derived_cl3389]) ).
thf(zip_derived_cl3738_208,plain,
( ( h2 @ e11 )
= e22 ),
inference(demod,[status(thm)],[zip_derived_cl3505,zip_derived_cl3737,zip_derived_cl3389]) ).
thf(zip_derived_cl3737_209,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl2476_210,plain,
( ( op2 @ e22 @ e23 )
= e22 ),
inference(clc,[status(thm)],[zip_derived_cl2423,zip_derived_cl285]) ).
thf(zip_derived_cl3088_211,plain,
( e11
= ( op1 @ e10 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl293,zip_derived_cl292,zip_derived_cl292,zip_derived_cl1697,zip_derived_cl292]) ).
thf(zip_derived_cl3738_212,plain,
( ( h2 @ e11 )
= e22 ),
inference(demod,[status(thm)],[zip_derived_cl3505,zip_derived_cl3737,zip_derived_cl3389]) ).
thf(zip_derived_cl3737_213,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl3470_214,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl3389_215,plain,
( ( op2 @ e23 @ ( h4 @ e13 ) )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3388,zip_derived_cl3319]) ).
thf(zip_derived_cl30,plain,
( ( ( op1 @ e13 @ e12 )
= e10 )
| ( ( op1 @ e12 @ e12 )
= e10 )
| ( ( op1 @ e11 @ e12 )
= e10 )
| ( ( op1 @ e10 @ e12 )
= e10 ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl292_216,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl2091,plain,
( ( ( op1 @ e13 @ e12 )
= e10 )
| ( e13 = e10 )
| ( ( op1 @ e11 @ e12 )
= e10 )
| ( ( op1 @ e10 @ e12 )
= e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl30,zip_derived_cl292]) ).
thf(zip_derived_cl195_217,plain,
e10 != e13,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl96,plain,
( ( op1 @ e13 @ e12 )
!= ( op1 @ e13 @ e13 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1697_218,plain,
( e10
= ( op1 @ e13 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl294,zip_derived_cl292,zip_derived_cl292]) ).
thf(zip_derived_cl1698,plain,
( ( op1 @ e13 @ e12 )
!= e10 ),
inference(demod,[status(thm)],[zip_derived_cl96,zip_derived_cl1697]) ).
thf(zip_derived_cl2092,plain,
( ( ( op1 @ e11 @ e12 )
= e10 )
| ( ( op1 @ e10 @ e12 )
= e10 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2091,zip_derived_cl195,zip_derived_cl1698]) ).
thf(zip_derived_cl4188_219,plain,
( ( op1 @ e11 @ e12 )
= e12 ),
inference(simplify,[status(thm)],[zip_derived_cl4184]) ).
thf(zip_derived_cl4277,plain,
( ( e12 = e10 )
| ( ( op1 @ e10 @ e12 )
= e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl2092,zip_derived_cl4188]) ).
thf(zip_derived_cl196_220,plain,
e10 != e12,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl4278,plain,
( ( op1 @ e10 @ e12 )
= e10 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl4277,zip_derived_cl196]) ).
thf(zip_derived_cl3737_221,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl3737_222,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl305_223,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl3255_224,plain,
( ( op2 @ e23 @ e21 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl271,zip_derived_cl3254]) ).
thf(zip_derived_cl14,plain,
( ( ( op1 @ e10 @ e11 )
= e13 )
| ( ( op1 @ e10 @ e11 )
= e12 )
| ( ( op1 @ e10 @ e11 )
= e11 )
| ( ( op1 @ e10 @ e11 )
= e10 ) ),
inference(cnf,[status(esa)],[ax1]) ).
thf(zip_derived_cl116,plain,
( ( op1 @ e10 @ e11 )
!= ( op1 @ e10 @ e12 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl4278_225,plain,
( ( op1 @ e10 @ e12 )
= e10 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl4277,zip_derived_cl196]) ).
thf(zip_derived_cl4327,plain,
( ( op1 @ e10 @ e11 )
!= e10 ),
inference(demod,[status(thm)],[zip_derived_cl116,zip_derived_cl4278]) ).
thf(zip_derived_cl4349,plain,
( ( e10 != e10 )
| ( ( op1 @ e10 @ e11 )
= e11 )
| ( ( op1 @ e10 @ e11 )
= e12 )
| ( ( op1 @ e10 @ e11 )
= e13 ) ),
inference('sup-',[status(thm)],[zip_derived_cl14,zip_derived_cl4327]) ).
thf(zip_derived_cl4351,plain,
( ( ( op1 @ e10 @ e11 )
= e13 )
| ( ( op1 @ e10 @ e11 )
= e12 )
| ( ( op1 @ e10 @ e11 )
= e11 ) ),
inference(simplify,[status(thm)],[zip_derived_cl4349]) ).
thf(zip_derived_cl3092_226,plain,
( ( op1 @ e10 @ e11 )
!= e11 ),
inference(demod,[status(thm)],[zip_derived_cl115,zip_derived_cl3088]) ).
thf(zip_derived_cl135,plain,
( ( op1 @ e10 @ e11 )
!= ( op1 @ e13 @ e11 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl3927_227,plain,
( ( op1 @ e13 @ e11 )
= e13 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3926,zip_derived_cl195,zip_derived_cl3149]) ).
thf(zip_derived_cl3937,plain,
( ( op1 @ e10 @ e11 )
!= e13 ),
inference(demod,[status(thm)],[zip_derived_cl135,zip_derived_cl3927]) ).
thf(zip_derived_cl4352,plain,
( ( op1 @ e10 @ e11 )
= e12 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl4351,zip_derived_cl3092,zip_derived_cl3937]) ).
thf(zip_derived_cl305_228,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax15]) ).
thf(zip_derived_cl3737_229,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl3738_230,plain,
( ( h2 @ e11 )
= e22 ),
inference(demod,[status(thm)],[zip_derived_cl3505,zip_derived_cl3737,zip_derived_cl3389]) ).
thf(zip_derived_cl76,plain,
( ( ( op2 @ e23 @ e22 )
= e21 )
| ( ( op2 @ e22 @ e22 )
= e21 )
| ( ( op2 @ e21 @ e22 )
= e21 )
| ( ( op2 @ e20 @ e22 )
= e21 ) ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl295_231,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax13]) ).
thf(zip_derived_cl1756_232,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl2705,plain,
( ( ( op2 @ e23 @ e22 )
= e21 )
| ( e23 = e21 )
| ( ( op2 @ e21 @ e22 )
= e21 )
| ( ( op2 @ ( h4 @ e13 ) @ e22 )
= e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl76,zip_derived_cl295,zip_derived_cl1756]) ).
thf(zip_derived_cl199_233,plain,
e21 != e23,
inference(cnf,[status(esa)],[ax8]) ).
thf(zip_derived_cl2706,plain,
( ( ( op2 @ e23 @ e22 )
= e21 )
| ( ( op2 @ e21 @ e22 )
= e21 )
| ( ( op2 @ ( h4 @ e13 ) @ e22 )
= e21 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2705,zip_derived_cl199]) ).
thf(zip_derived_cl3411_234,plain,
( ( op2 @ e21 @ e22 )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3410,zip_derived_cl3353]) ).
thf(zip_derived_cl3476,plain,
( ( ( op2 @ e23 @ e22 )
= e21 )
| ( e22 = e21 )
| ( ( op2 @ ( h4 @ e13 ) @ e22 )
= e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl2706,zip_derived_cl3411]) ).
thf(zip_derived_cl162,plain,
( ( op2 @ e20 @ e22 )
!= ( op2 @ e20 @ e23 ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1756_235,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1756_236,plain,
( e20
= ( h4 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl297,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310]) ).
thf(zip_derived_cl1763,plain,
( ( op2 @ ( h4 @ e13 ) @ e22 )
!= ( op2 @ ( h4 @ e13 ) @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl162,zip_derived_cl1756,zip_derived_cl1756]) ).
thf(zip_derived_cl3106_237,plain,
( e21
= ( op2 @ ( h4 @ e13 ) @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl296,zip_derived_cl295,zip_derived_cl295,zip_derived_cl310,zip_derived_cl295]) ).
thf(zip_derived_cl3107,plain,
( ( op2 @ ( h4 @ e13 ) @ e22 )
!= e21 ),
inference(demod,[status(thm)],[zip_derived_cl1763,zip_derived_cl3106]) ).
thf(zip_derived_cl200_238,plain,
e21 != e22,
inference(cnf,[status(esa)],[ax8]) ).
thf(zip_derived_cl3477,plain,
( ( op2 @ e23 @ e22 )
= e21 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3476,zip_derived_cl3107,zip_derived_cl200]) ).
thf(zip_derived_cl40,plain,
( ( ( op1 @ e13 @ e10 )
= e13 )
| ( ( op1 @ e12 @ e10 )
= e13 )
| ( ( op1 @ e11 @ e10 )
= e13 )
| ( ( op1 @ e10 @ e10 )
= e13 ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl106,plain,
( ( op1 @ e12 @ e10 )
!= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl292_239,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax12]) ).
thf(zip_derived_cl1436,plain,
( ( op1 @ e12 @ e10 )
!= e13 ),
inference(demod,[status(thm)],[zip_derived_cl106,zip_derived_cl292]) ).
thf(zip_derived_cl2215,plain,
( ( ( op1 @ e13 @ e10 )
= e13 )
| ( ( op1 @ e11 @ e10 )
= e13 )
| ( ( op1 @ e10 @ e10 )
= e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl40,zip_derived_cl1436]) ).
thf(zip_derived_cl4162_240,plain,
( ( op1 @ e11 @ e10 )
= e11 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl4161,zip_derived_cl3934]) ).
thf(zip_derived_cl4177,plain,
( ( ( op1 @ e13 @ e10 )
= e13 )
| ( e11 = e13 )
| ( ( op1 @ e10 @ e10 )
= e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl2215,zip_derived_cl4162]) ).
thf(zip_derived_cl193_241,plain,
e11 != e13,
inference(cnf,[status(esa)],[ax7]) ).
thf(zip_derived_cl3934_242,plain,
( ( op1 @ e13 @ e10 )
!= e13 ),
inference(demod,[status(thm)],[zip_derived_cl101,zip_derived_cl3927]) ).
thf(zip_derived_cl4178,plain,
( ( op1 @ e10 @ e10 )
= e13 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl4177,zip_derived_cl193,zip_derived_cl3934]) ).
thf(zip_derived_cl3470_243,plain,
( ( h2 @ e13 )
= ( h4 @ e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3469,zip_derived_cl3354,zip_derived_cl1777]) ).
thf(zip_derived_cl3737_244,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl3737_245,plain,
( ( h2 @ e10 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl3503,zip_derived_cl3417]) ).
thf(zip_derived_cl310_246,plain,
( ( h4 @ e13 )
= ( op2 @ e23 @ e23 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl6346,plain,
( ( e23 != e23 )
| ( e22 != e22 )
| ( e21 != e21 )
| ( ( h4 @ e13 )
!= ( h4 @ e13 ) )
| ( e23 != e23 )
| ( e22 != e22 )
| ( ( h4 @ e13 )
!= ( h4 @ e13 ) )
| ( e21 != e21 )
| ( e21 != e21 )
| ( ( h4 @ e13 )
!= ( h4 @ e13 ) )
| ( e22 != e22 )
| ( e23 != e23 )
| ( ( h4 @ e13 )
!= ( h4 @ e13 ) )
| ( e21 != e21 )
| ( e23 != e23 )
| ( e22 != e22 )
| ( e22 != e22 )
| ( e23 != e23 )
| ( e21 != e21 )
| ( ( h4 @ e13 )
!= ( h4 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl785,zip_derived_cl3737,zip_derived_cl3738,zip_derived_cl305,zip_derived_cl3470,zip_derived_cl1756,zip_derived_cl1697,zip_derived_cl3737,zip_derived_cl3470,zip_derived_cl3470,zip_derived_cl3417,zip_derived_cl4187,zip_derived_cl3738,zip_derived_cl3470,zip_derived_cl305,zip_derived_cl3441,zip_derived_cl3927,zip_derived_cl3470,zip_derived_cl3470,zip_derived_cl3738,zip_derived_cl3369,zip_derived_cl4247,zip_derived_cl305,zip_derived_cl3470,zip_derived_cl3737,zip_derived_cl3106,zip_derived_cl3241,zip_derived_cl305,zip_derived_cl305,zip_derived_cl3470,zip_derived_cl3366,zip_derived_cl292,zip_derived_cl3470,zip_derived_cl305,zip_derived_cl305,zip_derived_cl3500,zip_derived_cl4193,zip_derived_cl3738,zip_derived_cl305,zip_derived_cl3738,zip_derived_cl3411,zip_derived_cl4299,zip_derived_cl3737,zip_derived_cl305,zip_derived_cl3737,zip_derived_cl3116,zip_derived_cl3103,zip_derived_cl3470,zip_derived_cl3738,zip_derived_cl3470,zip_derived_cl3468,zip_derived_cl4188,zip_derived_cl305,zip_derived_cl3738,zip_derived_cl305,zip_derived_cl3394,zip_derived_cl4387,zip_derived_cl3737,zip_derived_cl3738,zip_derived_cl3738,zip_derived_cl295,zip_derived_cl4162,zip_derived_cl3738,zip_derived_cl3738,zip_derived_cl3737,zip_derived_cl2476,zip_derived_cl3088,zip_derived_cl3738,zip_derived_cl3737,zip_derived_cl3470,zip_derived_cl3389,zip_derived_cl4278,zip_derived_cl3737,zip_derived_cl3737,zip_derived_cl305,zip_derived_cl3255,zip_derived_cl4352,zip_derived_cl305,zip_derived_cl3737,zip_derived_cl3738,zip_derived_cl3477,zip_derived_cl4178,zip_derived_cl3470,zip_derived_cl3737,zip_derived_cl3737,zip_derived_cl310]) ).
thf(zip_derived_cl6347,plain,
$false,
inference(simplify,[status(thm)],[zip_derived_cl6346]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.11 % Problem : ALG110+1 : TPTP v9.2.0. Released v2.7.0.
% 0.02/0.11 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.9Eecay6lfW true
% 0.10/0.32 % Computer : n029.cluster.edu
% 0.10/0.32 % Model : x86_64 x86_64
% 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.32 % Memory : 8042.1875MB
% 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.32 % CPULimit : 300
% 0.10/0.32 % WCLimit : 300
% 0.10/0.32 % DateTime : Wed Oct 1 17:01:53 EDT 2025
% 0.10/0.32 % CPUTime :
% 0.10/0.32 % Running portfolio for 300 s
% 0.10/0.32 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.33 % Number of cores: 8
% 0.10/0.33 % Python version: Python 3.6.8
% 0.10/0.34 % Running in FO mode
% 0.48/0.65 % Total configuration time : 435
% 0.48/0.65 % Estimated wc time : 1092
% 0.48/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.49/0.73 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.49/0.73 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.49/0.73 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.49/0.74 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.49/0.74 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.49/0.74 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.50/0.78 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 20.07/3.69 % Solved by fo/fo4.sh.
% 20.07/3.69 % done 2192 iterations in 2.742s
% 20.07/3.69 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 20.07/3.69 % SZS output start Refutation
% See solution above
% 20.07/3.70
% 20.07/3.70
% 20.07/3.70 % Terminating...
% 20.74/3.88 % Runner terminated.
% 20.74/3.90 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------