%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : ALG016+1 : TPTP v9.2.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.xD06X814j8 true
% Computer : n021.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:18 PM UTC 2025
% Result : Theorem 5.24s 1.34s
% Output : Refutation 5.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 11
% Syntax : Number of formulae : 334 ( 316 unt; 0 typ; 0 def)
% Number of atoms : 993 ( 992 equ; 0 cnn)
% Maximal formula atoms : 128 ( 2 avg)
% Number of connectives : 4728 ( 157 ~; 247 |; 412 &;3912 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 64 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 16 ( 14 usr; 9 con; 0-2 aty)
% Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
thf(e13_type,type,
e13: $i ).
thf(e21_type,type,
e21: $i ).
thf(e12_type,type,
e12: $i ).
thf(e11_type,type,
e11: $i ).
thf(h1_type,type,
h1: $i > $i ).
thf(e23_type,type,
e23: $i ).
thf(e10_type,type,
e10: $i ).
thf(h4_type,type,
h4: $i > $i ).
thf(op1_type,type,
op1: $i > $i > $i ).
thf(e20_type,type,
e20: $i ).
thf(e22_type,type,
e22: $i ).
thf(op2_type,type,
op2: $i > $i > $i ).
thf(h3_type,type,
h3: $i > $i ).
thf(h2_type,type,
h2: $i > $i ).
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_cl678,plain,
( ( ( h2 @ e13 )
!= e23 )
| ( ( h2 @ e11 )
!= e22 )
| ( ( h2 @ e12 )
!= e21 )
| ( ( 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 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(ax27,axiom,
( ( ( h2 @ e13 )
= ( op2 @ e21 @ e21 ) )
& ( ( h2 @ e11 )
= ( op2 @ e21 @ ( op2 @ e21 @ e21 ) ) )
& ( ( h2 @ e10 )
= ( op2 @ ( op2 @ e21 @ ( op2 @ e21 @ e21 ) ) @ e21 ) )
& ( ( h2 @ e12 )
= e21 ) ) ).
thf(zip_derived_cl390,plain,
( ( h2 @ e13 )
= ( op2 @ e21 @ e21 ) ),
inference(cnf,[status(esa)],[ax27]) ).
thf(ax6,axiom,
( ( ( op2 @ ( op2 @ e23 @ e23 ) @ e23 )
= ( op2 @ e23 @ ( op2 @ e23 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e23 ) @ e22 )
= ( op2 @ e23 @ ( op2 @ e23 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e23 ) @ e21 )
= ( op2 @ e23 @ ( op2 @ e23 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e23 ) @ e20 )
= ( op2 @ e23 @ ( op2 @ e23 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e22 ) @ e23 )
= ( op2 @ e23 @ ( op2 @ e22 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e22 ) @ e22 )
= ( op2 @ e23 @ ( op2 @ e22 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e22 ) @ e21 )
= ( op2 @ e23 @ ( op2 @ e22 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e22 ) @ e20 )
= ( op2 @ e23 @ ( op2 @ e22 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e21 ) @ e23 )
= ( op2 @ e23 @ ( op2 @ e21 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e21 ) @ e22 )
= ( op2 @ e23 @ ( op2 @ e21 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e21 ) @ e21 )
= ( op2 @ e23 @ ( op2 @ e21 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e21 ) @ e20 )
= ( op2 @ e23 @ ( op2 @ e21 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e20 ) @ e23 )
= ( op2 @ e23 @ ( op2 @ e20 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e20 ) @ e22 )
= ( op2 @ e23 @ ( op2 @ e20 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e20 ) @ e21 )
= ( op2 @ e23 @ ( op2 @ e20 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e23 @ e20 ) @ e20 )
= ( op2 @ e23 @ ( op2 @ e20 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e23 ) @ e23 )
= ( op2 @ e22 @ ( op2 @ e23 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e23 ) @ e22 )
= ( op2 @ e22 @ ( op2 @ e23 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e23 ) @ e21 )
= ( op2 @ e22 @ ( op2 @ e23 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e23 ) @ e20 )
= ( op2 @ e22 @ ( op2 @ e23 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e22 ) @ e23 )
= ( op2 @ e22 @ ( op2 @ e22 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e22 ) @ e22 )
= ( op2 @ e22 @ ( op2 @ e22 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e22 ) @ e21 )
= ( op2 @ e22 @ ( op2 @ e22 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e22 ) @ e20 )
= ( op2 @ e22 @ ( op2 @ e22 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e21 ) @ e23 )
= ( op2 @ e22 @ ( op2 @ e21 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e21 ) @ e22 )
= ( op2 @ e22 @ ( op2 @ e21 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e21 ) @ e21 )
= ( op2 @ e22 @ ( op2 @ e21 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e21 ) @ e20 )
= ( op2 @ e22 @ ( op2 @ e21 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e20 ) @ e23 )
= ( op2 @ e22 @ ( op2 @ e20 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e20 ) @ e22 )
= ( op2 @ e22 @ ( op2 @ e20 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e20 ) @ e21 )
= ( op2 @ e22 @ ( op2 @ e20 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e22 @ e20 ) @ e20 )
= ( op2 @ e22 @ ( op2 @ e20 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e23 ) @ e23 )
= ( op2 @ e21 @ ( op2 @ e23 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e23 ) @ e22 )
= ( op2 @ e21 @ ( op2 @ e23 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e23 ) @ e21 )
= ( op2 @ e21 @ ( op2 @ e23 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e23 ) @ e20 )
= ( op2 @ e21 @ ( op2 @ e23 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e22 ) @ e23 )
= ( op2 @ e21 @ ( op2 @ e22 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e22 ) @ e22 )
= ( op2 @ e21 @ ( op2 @ e22 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e22 ) @ e21 )
= ( op2 @ e21 @ ( op2 @ e22 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e22 ) @ e20 )
= ( op2 @ e21 @ ( op2 @ e22 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e21 ) @ e23 )
= ( op2 @ e21 @ ( op2 @ e21 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e21 ) @ e22 )
= ( op2 @ e21 @ ( op2 @ e21 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e21 ) @ e21 )
= ( op2 @ e21 @ ( op2 @ e21 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e21 ) @ e20 )
= ( op2 @ e21 @ ( op2 @ e21 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e20 ) @ e23 )
= ( op2 @ e21 @ ( op2 @ e20 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e20 ) @ e22 )
= ( op2 @ e21 @ ( op2 @ e20 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e20 ) @ e21 )
= ( op2 @ e21 @ ( op2 @ e20 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e21 @ e20 ) @ e20 )
= ( op2 @ e21 @ ( op2 @ e20 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e23 ) @ e23 )
= ( op2 @ e20 @ ( op2 @ e23 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e23 ) @ e22 )
= ( op2 @ e20 @ ( op2 @ e23 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e23 ) @ e21 )
= ( op2 @ e20 @ ( op2 @ e23 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e23 ) @ e20 )
= ( op2 @ e20 @ ( op2 @ e23 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e22 ) @ e23 )
= ( op2 @ e20 @ ( op2 @ e22 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e22 ) @ e22 )
= ( op2 @ e20 @ ( op2 @ e22 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e22 ) @ e21 )
= ( op2 @ e20 @ ( op2 @ e22 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e22 ) @ e20 )
= ( op2 @ e20 @ ( op2 @ e22 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e21 ) @ e23 )
= ( op2 @ e20 @ ( op2 @ e21 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e21 ) @ e22 )
= ( op2 @ e20 @ ( op2 @ e21 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e21 ) @ e21 )
= ( op2 @ e20 @ ( op2 @ e21 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e21 ) @ e20 )
= ( op2 @ e20 @ ( op2 @ e21 @ e20 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e20 ) @ e23 )
= ( op2 @ e20 @ ( op2 @ e20 @ e23 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e20 ) @ e22 )
= ( op2 @ e20 @ ( op2 @ e20 @ e22 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e20 ) @ e21 )
= ( op2 @ e20 @ ( op2 @ e20 @ e21 ) ) )
& ( ( op2 @ ( op2 @ e20 @ e20 ) @ e20 )
= ( op2 @ e20 @ ( op2 @ e20 @ e20 ) ) ) ) ).
thf(zip_derived_cl123,plain,
( ( op2 @ ( op2 @ e23 @ e22 ) @ e21 )
= ( op2 @ e23 @ ( op2 @ e22 @ e21 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(ax29,axiom,
( ( ( h4 @ e13 )
= ( op2 @ e23 @ e23 ) )
& ( ( h4 @ e11 )
= ( op2 @ e23 @ ( op2 @ e23 @ e23 ) ) )
& ( ( h4 @ e10 )
= ( op2 @ ( op2 @ e23 @ ( op2 @ e23 @ e23 ) ) @ e23 ) )
& ( ( h4 @ e12 )
= e23 ) ) ).
thf(zip_derived_cl399,plain,
( ( h4 @ e11 )
= ( op2 @ e23 @ ( op2 @ e23 @ e23 ) ) ),
inference(cnf,[status(esa)],[ax29]) ).
thf(zip_derived_cl137,plain,
( ( op2 @ ( op2 @ e22 @ e22 ) @ e23 )
= ( op2 @ e22 @ ( op2 @ e22 @ e23 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(ax25,axiom,
( ( e23
= ( op2 @ e22 @ e22 ) )
& ( e21
= ( op2 @ e22 @ ( op2 @ e22 @ e22 ) ) )
& ( e20
= ( op2 @ ( op2 @ e22 @ ( op2 @ e22 @ e22 ) ) @ e22 ) ) ) ).
thf(zip_derived_cl383,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax25]) ).
thf(zip_derived_cl384,plain,
( e21
= ( op2 @ e22 @ ( op2 @ e22 @ e22 ) ) ),
inference(cnf,[status(esa)],[ax25]) ).
thf(zip_derived_cl383_001,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax25]) ).
thf(zip_derived_cl1451,plain,
( e21
= ( op2 @ e22 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl384,zip_derived_cl383]) ).
thf(zip_derived_cl1671,plain,
( ( op2 @ e23 @ e23 )
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl137,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1681,plain,
( ( h4 @ e11 )
= ( op2 @ e23 @ ( op2 @ e22 @ e21 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl399,zip_derived_cl1671]) ).
thf(zip_derived_cl1689,plain,
( ( op2 @ ( op2 @ e23 @ e22 ) @ e21 )
= ( h4 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl123,zip_derived_cl1681]) ).
thf(zip_derived_cl138,plain,
( ( op2 @ ( op2 @ e22 @ e22 ) @ e22 )
= ( op2 @ e22 @ ( op2 @ e22 @ e22 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl383_002,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax25]) ).
thf(zip_derived_cl383_003,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax25]) ).
thf(zip_derived_cl1451_004,plain,
( e21
= ( op2 @ e22 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl384,zip_derived_cl383]) ).
thf(zip_derived_cl1690,plain,
( ( op2 @ e23 @ e22 )
= e21 ),
inference(demod,[status(thm)],[zip_derived_cl138,zip_derived_cl383,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1701,plain,
( ( op2 @ e21 @ e21 )
= ( h4 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1689,zip_derived_cl1690]) ).
thf(zip_derived_cl117,plain,
( ( op2 @ ( op2 @ e23 @ e23 ) @ e23 )
= ( op2 @ e23 @ ( op2 @ e23 @ e23 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl399_005,plain,
( ( h4 @ e11 )
= ( op2 @ e23 @ ( op2 @ e23 @ e23 ) ) ),
inference(cnf,[status(esa)],[ax29]) ).
thf(zip_derived_cl1663,plain,
( ( op2 @ ( op2 @ e23 @ e23 ) @ e23 )
= ( h4 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl117,zip_derived_cl399]) ).
thf(zip_derived_cl1671_006,plain,
( ( op2 @ e23 @ e23 )
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl137,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1684,plain,
( ( op2 @ ( op2 @ e22 @ e21 ) @ e23 )
= ( h4 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1663,zip_derived_cl1671]) ).
thf(zip_derived_cl134,plain,
( ( op2 @ ( op2 @ e22 @ e23 ) @ e22 )
= ( op2 @ e22 @ ( op2 @ e23 @ e22 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1451_007,plain,
( e21
= ( op2 @ e22 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl384,zip_derived_cl383]) ).
thf(zip_derived_cl385,plain,
( e20
= ( op2 @ ( op2 @ e22 @ ( op2 @ e22 @ e22 ) ) @ e22 ) ),
inference(cnf,[status(esa)],[ax25]) ).
thf(zip_derived_cl383_008,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax25]) ).
thf(zip_derived_cl1451_009,plain,
( e21
= ( op2 @ e22 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl384,zip_derived_cl383]) ).
thf(zip_derived_cl1478,plain,
( e20
= ( op2 @ e21 @ e22 ) ),
inference(demod,[status(thm)],[zip_derived_cl385,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1668,plain,
( e20
= ( op2 @ e22 @ ( op2 @ e23 @ e22 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl134,zip_derived_cl1451,zip_derived_cl1478]) ).
thf(zip_derived_cl1690_010,plain,
( ( op2 @ e23 @ e22 )
= e21 ),
inference(demod,[status(thm)],[zip_derived_cl138,zip_derived_cl383,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1698,plain,
( e20
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1668,zip_derived_cl1690]) ).
thf(zip_derived_cl1714,plain,
( ( op2 @ e20 @ e23 )
= ( h4 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1684,zip_derived_cl1698]) ).
thf(zip_derived_cl1732,plain,
( ( op2 @ e21 @ e21 )
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1701,zip_derived_cl1714]) ).
thf(zip_derived_cl1750,plain,
( ( h2 @ e13 )
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl390,zip_derived_cl1732]) ).
thf(zip_derived_cl126,plain,
( ( op2 @ ( op2 @ e23 @ e21 ) @ e22 )
= ( op2 @ e23 @ ( op2 @ e21 @ e22 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1478_011,plain,
( e20
= ( op2 @ e21 @ e22 ) ),
inference(demod,[status(thm)],[zip_derived_cl385,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1666,plain,
( ( op2 @ ( op2 @ e23 @ e21 ) @ e22 )
= ( op2 @ e23 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl126,zip_derived_cl1478]) ).
thf(zip_derived_cl1681_012,plain,
( ( h4 @ e11 )
= ( op2 @ e23 @ ( op2 @ e22 @ e21 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl399,zip_derived_cl1671]) ).
thf(zip_derived_cl1698_013,plain,
( e20
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1668,zip_derived_cl1690]) ).
thf(zip_derived_cl1713,plain,
( ( h4 @ e11 )
= ( op2 @ e23 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1681,zip_derived_cl1698]) ).
thf(zip_derived_cl1701_014,plain,
( ( op2 @ e21 @ e21 )
= ( h4 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1689,zip_derived_cl1690]) ).
thf(zip_derived_cl1719,plain,
( ( op2 @ e21 @ e21 )
= ( op2 @ e23 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1713,zip_derived_cl1701]) ).
thf(zip_derived_cl1728,plain,
( ( op2 @ ( op2 @ e23 @ e21 ) @ e22 )
= ( op2 @ e21 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1666,zip_derived_cl1719]) ).
thf(zip_derived_cl121,plain,
( ( op2 @ ( op2 @ e23 @ e22 ) @ e23 )
= ( op2 @ e23 @ ( op2 @ e22 @ e23 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1451_015,plain,
( e21
= ( op2 @ e22 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl384,zip_derived_cl383]) ).
thf(zip_derived_cl1664,plain,
( ( op2 @ ( op2 @ e23 @ e22 ) @ e23 )
= ( op2 @ e23 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl121,zip_derived_cl1451]) ).
thf(zip_derived_cl1690_016,plain,
( ( op2 @ e23 @ e22 )
= e21 ),
inference(demod,[status(thm)],[zip_derived_cl138,zip_derived_cl383,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1697,plain,
( ( op2 @ e21 @ e23 )
= ( op2 @ e23 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1664,zip_derived_cl1690]) ).
thf(zip_derived_cl1732_017,plain,
( ( op2 @ e21 @ e21 )
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1701,zip_derived_cl1714]) ).
thf(zip_derived_cl1761,plain,
( ( op2 @ ( op2 @ e21 @ e23 ) @ e22 )
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1728,zip_derived_cl1697,zip_derived_cl1732]) ).
thf(zip_derived_cl142,plain,
( ( op2 @ ( op2 @ e22 @ e21 ) @ e22 )
= ( op2 @ e22 @ ( op2 @ e21 @ e22 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1698_018,plain,
( e20
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1668,zip_derived_cl1690]) ).
thf(zip_derived_cl1478_019,plain,
( e20
= ( op2 @ e21 @ e22 ) ),
inference(demod,[status(thm)],[zip_derived_cl385,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl133,plain,
( ( op2 @ ( op2 @ e22 @ e23 ) @ e23 )
= ( op2 @ e22 @ ( op2 @ e23 @ e23 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1451_020,plain,
( e21
= ( op2 @ e22 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl384,zip_derived_cl383]) ).
thf(zip_derived_cl1667,plain,
( ( op2 @ e21 @ e23 )
= ( op2 @ e22 @ ( op2 @ e23 @ e23 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl133,zip_derived_cl1451]) ).
thf(zip_derived_cl1671_021,plain,
( ( op2 @ e23 @ e23 )
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl137,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1686,plain,
( ( op2 @ e21 @ e23 )
= ( op2 @ e22 @ ( op2 @ e22 @ e21 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1667,zip_derived_cl1671]) ).
thf(zip_derived_cl1698_022,plain,
( e20
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1668,zip_derived_cl1690]) ).
thf(zip_derived_cl1715,plain,
( ( op2 @ e21 @ e23 )
= ( op2 @ e22 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1686,zip_derived_cl1698]) ).
thf(zip_derived_cl1767,plain,
( ( op2 @ e20 @ e22 )
= ( op2 @ e21 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl142,zip_derived_cl1698,zip_derived_cl1478,zip_derived_cl1715]) ).
thf(zip_derived_cl1778,plain,
( ( op2 @ ( op2 @ e20 @ e22 ) @ e22 )
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1761,zip_derived_cl1767]) ).
thf(ax5,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_cl114,plain,
( ( ( op2 @ e20 @ e22 )
= e23 )
| ( ( op2 @ e20 @ e22 )
= e22 )
| ( ( op2 @ e20 @ e22 )
= e21 )
| ( ( op2 @ e20 @ e22 )
= e20 ) ),
inference(cnf,[status(esa)],[ax5]) ).
thf(ax18,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_cl331,plain,
( ( op2 @ e20 @ e22 )
!= ( op2 @ e21 @ e22 ) ),
inference(cnf,[status(esa)],[ax18]) ).
thf(zip_derived_cl1478_023,plain,
( e20
= ( op2 @ e21 @ e22 ) ),
inference(demod,[status(thm)],[zip_derived_cl385,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1483,plain,
( ( op2 @ e20 @ e22 )
!= e20 ),
inference(demod,[status(thm)],[zip_derived_cl331,zip_derived_cl1478]) ).
thf(zip_derived_cl329,plain,
( ( op2 @ e20 @ e22 )
!= ( op2 @ e23 @ e22 ) ),
inference(cnf,[status(esa)],[ax18]) ).
thf(zip_derived_cl1690_024,plain,
( ( op2 @ e23 @ e22 )
= e21 ),
inference(demod,[status(thm)],[zip_derived_cl138,zip_derived_cl383,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1694,plain,
( ( op2 @ e20 @ e22 )
!= e21 ),
inference(demod,[status(thm)],[zip_derived_cl329,zip_derived_cl1690]) ).
thf(zip_derived_cl330,plain,
( ( op2 @ e20 @ e22 )
!= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax18]) ).
thf(zip_derived_cl383_025,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax25]) ).
thf(zip_derived_cl1443,plain,
( ( op2 @ e20 @ e22 )
!= e23 ),
inference(demod,[status(thm)],[zip_derived_cl330,zip_derived_cl383]) ).
thf(zip_derived_cl1854,plain,
( ( op2 @ e20 @ e22 )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl114,zip_derived_cl1483,zip_derived_cl1694,zip_derived_cl1443]) ).
thf(zip_derived_cl383_026,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax25]) ).
thf(zip_derived_cl1864,plain,
( e23
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1778,zip_derived_cl1854,zip_derived_cl383]) ).
thf(zip_derived_cl1887,plain,
( ( h2 @ e13 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1750,zip_derived_cl1864]) ).
thf(zip_derived_cl148,plain,
( ( op2 @ ( op2 @ e22 @ e20 ) @ e20 )
= ( op2 @ e22 @ ( op2 @ e20 @ e20 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1715_027,plain,
( ( op2 @ e21 @ e23 )
= ( op2 @ e22 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1686,zip_derived_cl1698]) ).
thf(zip_derived_cl1767_028,plain,
( ( op2 @ e20 @ e22 )
= ( op2 @ e21 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl142,zip_derived_cl1698,zip_derived_cl1478,zip_derived_cl1715]) ).
thf(zip_derived_cl1773,plain,
( ( op2 @ e20 @ e22 )
= ( op2 @ e22 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1715,zip_derived_cl1767]) ).
thf(zip_derived_cl1793,plain,
( ( op2 @ ( op2 @ e20 @ e22 ) @ e20 )
= ( op2 @ e22 @ ( op2 @ e20 @ e20 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl148,zip_derived_cl1773]) ).
thf(zip_derived_cl152,plain,
( ( op2 @ ( op2 @ e21 @ e23 ) @ e20 )
= ( op2 @ e21 @ ( op2 @ e23 @ e20 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1767_029,plain,
( ( op2 @ e20 @ e22 )
= ( op2 @ e21 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl142,zip_derived_cl1698,zip_derived_cl1478,zip_derived_cl1715]) ).
thf(zip_derived_cl1793_030,plain,
( ( op2 @ ( op2 @ e20 @ e22 ) @ e20 )
= ( op2 @ e22 @ ( op2 @ e20 @ e20 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl148,zip_derived_cl1773]) ).
thf(zip_derived_cl1719_031,plain,
( ( op2 @ e21 @ e21 )
= ( op2 @ e23 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1713,zip_derived_cl1701]) ).
thf(zip_derived_cl1732_032,plain,
( ( op2 @ e21 @ e21 )
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1701,zip_derived_cl1714]) ).
thf(zip_derived_cl1753,plain,
( ( op2 @ e20 @ e23 )
= ( op2 @ e23 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1719,zip_derived_cl1732]) ).
thf(zip_derived_cl391,plain,
( ( h2 @ e11 )
= ( op2 @ e21 @ ( op2 @ e21 @ e21 ) ) ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl1732_033,plain,
( ( op2 @ e21 @ e21 )
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1701,zip_derived_cl1714]) ).
thf(zip_derived_cl1751,plain,
( ( h2 @ e11 )
= ( op2 @ e21 @ ( op2 @ e20 @ e23 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl391,zip_derived_cl1732]) ).
thf(zip_derived_cl1797,plain,
( ( op2 @ e22 @ ( op2 @ e20 @ e20 ) )
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl152,zip_derived_cl1767,zip_derived_cl1793,zip_derived_cl1753,zip_derived_cl1751]) ).
thf(zip_derived_cl1798,plain,
( ( op2 @ ( op2 @ e20 @ e22 ) @ e20 )
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1793,zip_derived_cl1797]) ).
thf(zip_derived_cl1854_034,plain,
( ( op2 @ e20 @ e22 )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl114,zip_derived_cl1483,zip_derived_cl1694,zip_derived_cl1443]) ).
thf(zip_derived_cl1773_035,plain,
( ( op2 @ e20 @ e22 )
= ( op2 @ e22 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1715,zip_derived_cl1767]) ).
thf(zip_derived_cl1854_036,plain,
( ( op2 @ e20 @ e22 )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl114,zip_derived_cl1483,zip_derived_cl1694,zip_derived_cl1443]) ).
thf(zip_derived_cl1870,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl393,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl392,plain,
( ( h2 @ e10 )
= ( op2 @ ( op2 @ e21 @ ( op2 @ e21 @ e21 ) ) @ e21 ) ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl1732_037,plain,
( ( op2 @ e21 @ e21 )
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1701,zip_derived_cl1714]) ).
thf(zip_derived_cl1751_038,plain,
( ( h2 @ e11 )
= ( op2 @ e21 @ ( op2 @ e20 @ e23 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl391,zip_derived_cl1732]) ).
thf(zip_derived_cl1831,plain,
( ( h2 @ e10 )
= ( op2 @ ( h2 @ e11 ) @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl392,zip_derived_cl1732,zip_derived_cl1751]) ).
thf(zip_derived_cl1870_039,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl1698_040,plain,
( e20
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1668,zip_derived_cl1690]) ).
thf(zip_derived_cl1877,plain,
( ( h2 @ e10 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1831,zip_derived_cl1870,zip_derived_cl1698]) ).
thf(ax2,axiom,
( ( ( op1 @ ( op1 @ e13 @ e13 ) @ e13 )
= ( op1 @ e13 @ ( op1 @ e13 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e13 ) @ e12 )
= ( op1 @ e13 @ ( op1 @ e13 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e13 ) @ e11 )
= ( op1 @ e13 @ ( op1 @ e13 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e13 ) @ e10 )
= ( op1 @ e13 @ ( op1 @ e13 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e12 ) @ e13 )
= ( op1 @ e13 @ ( op1 @ e12 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e12 ) @ e12 )
= ( op1 @ e13 @ ( op1 @ e12 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e12 ) @ e11 )
= ( op1 @ e13 @ ( op1 @ e12 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e12 ) @ e10 )
= ( op1 @ e13 @ ( op1 @ e12 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e11 ) @ e13 )
= ( op1 @ e13 @ ( op1 @ e11 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e11 ) @ e12 )
= ( op1 @ e13 @ ( op1 @ e11 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e11 ) @ e11 )
= ( op1 @ e13 @ ( op1 @ e11 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e11 ) @ e10 )
= ( op1 @ e13 @ ( op1 @ e11 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e10 ) @ e13 )
= ( op1 @ e13 @ ( op1 @ e10 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e10 ) @ e12 )
= ( op1 @ e13 @ ( op1 @ e10 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e10 ) @ e11 )
= ( op1 @ e13 @ ( op1 @ e10 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e13 @ e10 ) @ e10 )
= ( op1 @ e13 @ ( op1 @ e10 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e13 ) @ e13 )
= ( op1 @ e12 @ ( op1 @ e13 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e13 ) @ e12 )
= ( op1 @ e12 @ ( op1 @ e13 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e13 ) @ e11 )
= ( op1 @ e12 @ ( op1 @ e13 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e13 ) @ e10 )
= ( op1 @ e12 @ ( op1 @ e13 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e12 ) @ e13 )
= ( op1 @ e12 @ ( op1 @ e12 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e12 ) @ e12 )
= ( op1 @ e12 @ ( op1 @ e12 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e12 ) @ e11 )
= ( op1 @ e12 @ ( op1 @ e12 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e12 ) @ e10 )
= ( op1 @ e12 @ ( op1 @ e12 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e11 ) @ e13 )
= ( op1 @ e12 @ ( op1 @ e11 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e11 ) @ e12 )
= ( op1 @ e12 @ ( op1 @ e11 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e11 ) @ e11 )
= ( op1 @ e12 @ ( op1 @ e11 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e11 ) @ e10 )
= ( op1 @ e12 @ ( op1 @ e11 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e10 ) @ e13 )
= ( op1 @ e12 @ ( op1 @ e10 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e10 ) @ e12 )
= ( op1 @ e12 @ ( op1 @ e10 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e10 ) @ e11 )
= ( op1 @ e12 @ ( op1 @ e10 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e12 @ e10 ) @ e10 )
= ( op1 @ e12 @ ( op1 @ e10 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e13 ) @ e13 )
= ( op1 @ e11 @ ( op1 @ e13 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e13 ) @ e12 )
= ( op1 @ e11 @ ( op1 @ e13 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e13 ) @ e11 )
= ( op1 @ e11 @ ( op1 @ e13 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e13 ) @ e10 )
= ( op1 @ e11 @ ( op1 @ e13 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e12 ) @ e13 )
= ( op1 @ e11 @ ( op1 @ e12 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e12 ) @ e12 )
= ( op1 @ e11 @ ( op1 @ e12 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e12 ) @ e11 )
= ( op1 @ e11 @ ( op1 @ e12 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e12 ) @ e10 )
= ( op1 @ e11 @ ( op1 @ e12 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e11 ) @ e13 )
= ( op1 @ e11 @ ( op1 @ e11 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e11 ) @ e12 )
= ( op1 @ e11 @ ( op1 @ e11 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e11 ) @ e11 )
= ( op1 @ e11 @ ( op1 @ e11 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e11 ) @ e10 )
= ( op1 @ e11 @ ( op1 @ e11 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e10 ) @ e13 )
= ( op1 @ e11 @ ( op1 @ e10 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e10 ) @ e12 )
= ( op1 @ e11 @ ( op1 @ e10 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e10 ) @ e11 )
= ( op1 @ e11 @ ( op1 @ e10 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e11 @ e10 ) @ e10 )
= ( op1 @ e11 @ ( op1 @ e10 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e13 ) @ e13 )
= ( op1 @ e10 @ ( op1 @ e13 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e13 ) @ e12 )
= ( op1 @ e10 @ ( op1 @ e13 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e13 ) @ e11 )
= ( op1 @ e10 @ ( op1 @ e13 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e13 ) @ e10 )
= ( op1 @ e10 @ ( op1 @ e13 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e12 ) @ e13 )
= ( op1 @ e10 @ ( op1 @ e12 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e12 ) @ e12 )
= ( op1 @ e10 @ ( op1 @ e12 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e12 ) @ e11 )
= ( op1 @ e10 @ ( op1 @ e12 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e12 ) @ e10 )
= ( op1 @ e10 @ ( op1 @ e12 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e11 ) @ e13 )
= ( op1 @ e10 @ ( op1 @ e11 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e11 ) @ e12 )
= ( op1 @ e10 @ ( op1 @ e11 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e11 ) @ e11 )
= ( op1 @ e10 @ ( op1 @ e11 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e11 ) @ e10 )
= ( op1 @ e10 @ ( op1 @ e11 @ e10 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e10 ) @ e13 )
= ( op1 @ e10 @ ( op1 @ e10 @ e13 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e10 ) @ e12 )
= ( op1 @ e10 @ ( op1 @ e10 @ e12 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e10 ) @ e11 )
= ( op1 @ e10 @ ( op1 @ e10 @ e11 ) ) )
& ( ( op1 @ ( op1 @ e10 @ e10 ) @ e10 )
= ( op1 @ e10 @ ( op1 @ e10 @ e10 ) ) ) ) ).
thf(zip_derived_cl36,plain,
( ( op1 @ ( op1 @ e12 @ e12 ) @ e13 )
= ( op1 @ e12 @ ( op1 @ e12 @ e13 ) ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(ax24,axiom,
( ( e13
= ( op1 @ e12 @ e12 ) )
& ( e11
= ( op1 @ e12 @ ( op1 @ e12 @ e12 ) ) )
& ( e10
= ( op1 @ ( op1 @ e12 @ ( op1 @ e12 @ e12 ) ) @ e12 ) ) ) ).
thf(zip_derived_cl380,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax24]) ).
thf(zip_derived_cl381,plain,
( e11
= ( op1 @ e12 @ ( op1 @ e12 @ e12 ) ) ),
inference(cnf,[status(esa)],[ax24]) ).
thf(zip_derived_cl380_041,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax24]) ).
thf(zip_derived_cl1444,plain,
( e11
= ( op1 @ e12 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl381,zip_derived_cl380]) ).
thf(zip_derived_cl1490,plain,
( ( op1 @ e13 @ e13 )
= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl36,zip_derived_cl380,zip_derived_cl1444]) ).
thf(zip_derived_cl33,plain,
( ( op1 @ ( op1 @ e12 @ e13 ) @ e12 )
= ( op1 @ e12 @ ( op1 @ e13 @ e12 ) ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl1444_042,plain,
( e11
= ( op1 @ e12 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl381,zip_derived_cl380]) ).
thf(zip_derived_cl382,plain,
( e10
= ( op1 @ ( op1 @ e12 @ ( op1 @ e12 @ e12 ) ) @ e12 ) ),
inference(cnf,[status(esa)],[ax24]) ).
thf(zip_derived_cl380_043,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax24]) ).
thf(zip_derived_cl1444_044,plain,
( e11
= ( op1 @ e12 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl381,zip_derived_cl380]) ).
thf(zip_derived_cl1470,plain,
( e10
= ( op1 @ e11 @ e12 ) ),
inference(demod,[status(thm)],[zip_derived_cl382,zip_derived_cl380,zip_derived_cl1444]) ).
thf(zip_derived_cl1487,plain,
( e10
= ( op1 @ e12 @ ( op1 @ e13 @ e12 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl33,zip_derived_cl1444,zip_derived_cl1470]) ).
thf(zip_derived_cl37,plain,
( ( op1 @ ( op1 @ e12 @ e12 ) @ e12 )
= ( op1 @ e12 @ ( op1 @ e12 @ e12 ) ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl380_045,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax24]) ).
thf(zip_derived_cl380_046,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax24]) ).
thf(zip_derived_cl1444_047,plain,
( e11
= ( op1 @ e12 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl381,zip_derived_cl380]) ).
thf(zip_derived_cl1505,plain,
( ( op1 @ e13 @ e12 )
= e11 ),
inference(demod,[status(thm)],[zip_derived_cl37,zip_derived_cl380,zip_derived_cl380,zip_derived_cl1444]) ).
thf(zip_derived_cl1514,plain,
( e10
= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1487,zip_derived_cl1505]) ).
thf(zip_derived_cl1521,plain,
( ( op1 @ e13 @ e13 )
= e10 ),
inference(demod,[status(thm)],[zip_derived_cl1490,zip_derived_cl1514]) ).
thf(zip_derived_cl1877_048,plain,
( ( h2 @ e10 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1831,zip_derived_cl1870,zip_derived_cl1698]) ).
thf(zip_derived_cl1887_049,plain,
( ( h2 @ e13 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1750,zip_derived_cl1864]) ).
thf(zip_derived_cl1887_050,plain,
( ( h2 @ e13 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1750,zip_derived_cl1864]) ).
thf(zip_derived_cl1671_051,plain,
( ( op2 @ e23 @ e23 )
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl137,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1698_052,plain,
( e20
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1668,zip_derived_cl1690]) ).
thf(zip_derived_cl1708,plain,
( ( op2 @ e23 @ e23 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1671,zip_derived_cl1698]) ).
thf(zip_derived_cl1505_053,plain,
( ( op1 @ e13 @ e12 )
= e11 ),
inference(demod,[status(thm)],[zip_derived_cl37,zip_derived_cl380,zip_derived_cl380,zip_derived_cl1444]) ).
thf(zip_derived_cl1870_054,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl1887_055,plain,
( ( h2 @ e13 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1750,zip_derived_cl1864]) ).
thf(zip_derived_cl393_056,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl1697_057,plain,
( ( op2 @ e21 @ e23 )
= ( op2 @ e23 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1664,zip_derived_cl1690]) ).
thf(zip_derived_cl1767_058,plain,
( ( op2 @ e20 @ e22 )
= ( op2 @ e21 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl142,zip_derived_cl1698,zip_derived_cl1478,zip_derived_cl1715]) ).
thf(zip_derived_cl1772,plain,
( ( op2 @ e20 @ e22 )
= ( op2 @ e23 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1697,zip_derived_cl1767]) ).
thf(zip_derived_cl1854_059,plain,
( ( op2 @ e20 @ e22 )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl114,zip_derived_cl1483,zip_derived_cl1694,zip_derived_cl1443]) ).
thf(zip_derived_cl1862,plain,
( e22
= ( op2 @ e23 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1772,zip_derived_cl1854]) ).
thf(zip_derived_cl20,plain,
( ( op1 @ ( op1 @ e13 @ e12 ) @ e13 )
= ( op1 @ e13 @ ( op1 @ e12 @ e13 ) ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl1444_060,plain,
( e11
= ( op1 @ e12 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl381,zip_derived_cl380]) ).
thf(zip_derived_cl1469,plain,
( ( op1 @ ( op1 @ e13 @ e12 ) @ e13 )
= ( op1 @ e13 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl20,zip_derived_cl1444]) ).
thf(zip_derived_cl1505_061,plain,
( ( op1 @ e13 @ e12 )
= e11 ),
inference(demod,[status(thm)],[zip_derived_cl37,zip_derived_cl380,zip_derived_cl380,zip_derived_cl1444]) ).
thf(zip_derived_cl1512,plain,
( ( op1 @ e11 @ e13 )
= ( op1 @ e13 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1469,zip_derived_cl1505]) ).
thf(zip_derived_cl38,plain,
( ( op1 @ ( op1 @ e12 @ e12 ) @ e11 )
= ( op1 @ e12 @ ( op1 @ e12 @ e11 ) ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl380_062,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax24]) ).
thf(zip_derived_cl1514_063,plain,
( e10
= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1487,zip_derived_cl1505]) ).
thf(zip_derived_cl1523,plain,
( ( op1 @ e13 @ e11 )
= ( op1 @ e12 @ e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl38,zip_derived_cl380,zip_derived_cl1514]) ).
thf(zip_derived_cl1512_064,plain,
( ( op1 @ e11 @ e13 )
= ( op1 @ e13 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1469,zip_derived_cl1505]) ).
thf(zip_derived_cl1541,plain,
( ( op1 @ e11 @ e13 )
= ( op1 @ e12 @ e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl1523,zip_derived_cl1512]) ).
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_cl7,plain,
( ( ( op1 @ e12 @ e10 )
= e13 )
| ( ( op1 @ e12 @ e10 )
= e12 )
| ( ( op1 @ e12 @ e10 )
= e11 )
| ( ( op1 @ e12 @ e10 )
= e10 ) ),
inference(cnf,[status(esa)],[ax1]) ).
thf(ax17,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_cl258,plain,
( ( op1 @ e12 @ e10 )
!= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl380_065,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax24]) ).
thf(zip_derived_cl1429,plain,
( ( op1 @ e12 @ e10 )
!= e13 ),
inference(demod,[status(thm)],[zip_derived_cl258,zip_derived_cl380]) ).
thf(zip_derived_cl1432,plain,
( ( ( op1 @ e12 @ e10 )
= e12 )
| ( ( op1 @ e12 @ e10 )
= e11 )
| ( ( op1 @ e12 @ e10 )
= e10 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl7,zip_derived_cl1429]) ).
thf(zip_derived_cl259,plain,
( ( op1 @ e12 @ e10 )
!= ( op1 @ e12 @ e11 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl1514_066,plain,
( e10
= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1487,zip_derived_cl1505]) ).
thf(zip_derived_cl1515,plain,
( ( op1 @ e12 @ e10 )
!= e10 ),
inference(demod,[status(thm)],[zip_derived_cl259,zip_derived_cl1514]) ).
thf(zip_derived_cl257,plain,
( ( op1 @ e12 @ e10 )
!= ( op1 @ e12 @ e13 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl1444_067,plain,
( e11
= ( op1 @ e12 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl381,zip_derived_cl380]) ).
thf(zip_derived_cl1446,plain,
( ( op1 @ e12 @ e10 )
!= e11 ),
inference(demod,[status(thm)],[zip_derived_cl257,zip_derived_cl1444]) ).
thf(zip_derived_cl1546,plain,
( ( op1 @ e12 @ e10 )
= e12 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1432,zip_derived_cl1515,zip_derived_cl1446]) ).
thf(zip_derived_cl1553,plain,
( ( op1 @ e11 @ e13 )
= e12 ),
inference(demod,[status(thm)],[zip_derived_cl1541,zip_derived_cl1546]) ).
thf(zip_derived_cl1559,plain,
( e12
= ( op1 @ e13 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1512,zip_derived_cl1553]) ).
thf(zip_derived_cl393_068,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl1887_069,plain,
( ( h2 @ e13 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1750,zip_derived_cl1864]) ).
thf(zip_derived_cl1870_070,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl1690_071,plain,
( ( op2 @ e23 @ e22 )
= e21 ),
inference(demod,[status(thm)],[zip_derived_cl138,zip_derived_cl383,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl3,plain,
( ( ( op1 @ e13 @ e10 )
= e13 )
| ( ( op1 @ e13 @ e10 )
= e12 )
| ( ( op1 @ e13 @ e10 )
= e11 )
| ( ( op1 @ e13 @ e10 )
= e10 ) ),
inference(cnf,[status(esa)],[ax1]) ).
thf(zip_derived_cl251,plain,
( ( op1 @ e13 @ e10 )
!= ( op1 @ e13 @ e13 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl1490_072,plain,
( ( op1 @ e13 @ e13 )
= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl36,zip_derived_cl380,zip_derived_cl1444]) ).
thf(zip_derived_cl1498,plain,
( ( op1 @ e13 @ e10 )
!= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl251,zip_derived_cl1490]) ).
thf(zip_derived_cl1514_073,plain,
( e10
= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1487,zip_derived_cl1505]) ).
thf(zip_derived_cl1537,plain,
( ( op1 @ e13 @ e10 )
!= e10 ),
inference(demod,[status(thm)],[zip_derived_cl1498,zip_derived_cl1514]) ).
thf(zip_derived_cl252,plain,
( ( op1 @ e13 @ e10 )
!= ( op1 @ e13 @ e12 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl1505_074,plain,
( ( op1 @ e13 @ e12 )
= e11 ),
inference(demod,[status(thm)],[zip_derived_cl37,zip_derived_cl380,zip_derived_cl380,zip_derived_cl1444]) ).
thf(zip_derived_cl1509,plain,
( ( op1 @ e13 @ e10 )
!= e11 ),
inference(demod,[status(thm)],[zip_derived_cl252,zip_derived_cl1505]) ).
thf(zip_derived_cl290,plain,
( ( op1 @ e12 @ e10 )
!= ( op1 @ e13 @ e10 ) ),
inference(cnf,[status(esa)],[ax17]) ).
thf(zip_derived_cl1541_075,plain,
( ( op1 @ e11 @ e13 )
= ( op1 @ e12 @ e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl1523,zip_derived_cl1512]) ).
thf(zip_derived_cl1542,plain,
( ( op1 @ e11 @ e13 )
!= ( op1 @ e13 @ e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl290,zip_derived_cl1541]) ).
thf(zip_derived_cl1553_076,plain,
( ( op1 @ e11 @ e13 )
= e12 ),
inference(demod,[status(thm)],[zip_derived_cl1541,zip_derived_cl1546]) ).
thf(zip_derived_cl1560,plain,
( e12
!= ( op1 @ e13 @ e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl1542,zip_derived_cl1553]) ).
thf(zip_derived_cl1587,plain,
( ( op1 @ e13 @ e10 )
= e13 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3,zip_derived_cl1537,zip_derived_cl1509,zip_derived_cl1560]) ).
thf(zip_derived_cl1887_077,plain,
( ( h2 @ e13 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1750,zip_derived_cl1864]) ).
thf(zip_derived_cl1887_078,plain,
( ( h2 @ e13 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1750,zip_derived_cl1864]) ).
thf(zip_derived_cl1877_079,plain,
( ( h2 @ e10 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1831,zip_derived_cl1870,zip_derived_cl1698]) ).
thf(zip_derived_cl1753_080,plain,
( ( op2 @ e20 @ e23 )
= ( op2 @ e23 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1719,zip_derived_cl1732]) ).
thf(zip_derived_cl1864_081,plain,
( e23
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1778,zip_derived_cl1854,zip_derived_cl383]) ).
thf(zip_derived_cl1888,plain,
( e23
= ( op2 @ e23 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1753,zip_derived_cl1864]) ).
thf(zip_derived_cl1444_082,plain,
( e11
= ( op1 @ e12 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl381,zip_derived_cl380]) ).
thf(zip_derived_cl1870_083,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl393_084,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl1887_085,plain,
( ( h2 @ e13 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1750,zip_derived_cl1864]) ).
thf(zip_derived_cl1767_086,plain,
( ( op2 @ e20 @ e22 )
= ( op2 @ e21 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl142,zip_derived_cl1698,zip_derived_cl1478,zip_derived_cl1715]) ).
thf(zip_derived_cl1854_087,plain,
( ( op2 @ e20 @ e22 )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl114,zip_derived_cl1483,zip_derived_cl1694,zip_derived_cl1443]) ).
thf(zip_derived_cl1861,plain,
( e22
= ( op2 @ e21 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1767,zip_derived_cl1854]) ).
thf(zip_derived_cl380_088,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax24]) ).
thf(zip_derived_cl1887_089,plain,
( ( h2 @ e13 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1750,zip_derived_cl1864]) ).
thf(zip_derived_cl393_090,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl393_091,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl1732_092,plain,
( ( op2 @ e21 @ e21 )
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1701,zip_derived_cl1714]) ).
thf(zip_derived_cl1864_093,plain,
( e23
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1778,zip_derived_cl1854,zip_derived_cl383]) ).
thf(zip_derived_cl1886,plain,
( ( op2 @ e21 @ e21 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1732,zip_derived_cl1864]) ).
thf(zip_derived_cl1514_094,plain,
( e10
= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1487,zip_derived_cl1505]) ).
thf(zip_derived_cl1877_095,plain,
( ( h2 @ e10 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1831,zip_derived_cl1870,zip_derived_cl1698]) ).
thf(zip_derived_cl393_096,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl1870_097,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl1478_098,plain,
( e20
= ( op2 @ e21 @ e22 ) ),
inference(demod,[status(thm)],[zip_derived_cl385,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1546_099,plain,
( ( op1 @ e12 @ e10 )
= e12 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1432,zip_derived_cl1515,zip_derived_cl1446]) ).
thf(zip_derived_cl393_100,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl393_101,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl1877_102,plain,
( ( h2 @ e10 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1831,zip_derived_cl1870,zip_derived_cl1698]) ).
thf(zip_derived_cl143,plain,
( ( op2 @ ( op2 @ e22 @ e21 ) @ e21 )
= ( op2 @ e22 @ ( op2 @ e21 @ e21 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1698_103,plain,
( e20
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1668,zip_derived_cl1690]) ).
thf(zip_derived_cl1732_104,plain,
( ( op2 @ e21 @ e21 )
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1701,zip_derived_cl1714]) ).
thf(zip_derived_cl136,plain,
( ( op2 @ ( op2 @ e22 @ e23 ) @ e20 )
= ( op2 @ e22 @ ( op2 @ e23 @ e20 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1451_105,plain,
( e21
= ( op2 @ e22 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl384,zip_derived_cl383]) ).
thf(zip_derived_cl1670,plain,
( ( op2 @ e21 @ e20 )
= ( op2 @ e22 @ ( op2 @ e23 @ e20 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl136,zip_derived_cl1451]) ).
thf(zip_derived_cl1719_106,plain,
( ( op2 @ e21 @ e21 )
= ( op2 @ e23 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1713,zip_derived_cl1701]) ).
thf(zip_derived_cl1729,plain,
( ( op2 @ e21 @ e20 )
= ( op2 @ e22 @ ( op2 @ e21 @ e21 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1670,zip_derived_cl1719]) ).
thf(zip_derived_cl1732_107,plain,
( ( op2 @ e21 @ e21 )
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1701,zip_derived_cl1714]) ).
thf(zip_derived_cl1762,plain,
( ( op2 @ e21 @ e20 )
= ( op2 @ e22 @ ( op2 @ e20 @ e23 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1729,zip_derived_cl1732]) ).
thf(zip_derived_cl1782,plain,
( ( op2 @ e20 @ e21 )
= ( op2 @ e21 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl143,zip_derived_cl1698,zip_derived_cl1732,zip_derived_cl1762]) ).
thf(zip_derived_cl124,plain,
( ( op2 @ ( op2 @ e23 @ e22 ) @ e20 )
= ( op2 @ e23 @ ( op2 @ e22 @ e20 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1690_108,plain,
( ( op2 @ e23 @ e22 )
= e21 ),
inference(demod,[status(thm)],[zip_derived_cl138,zip_derived_cl383,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1691,plain,
( ( op2 @ e21 @ e20 )
= ( op2 @ e23 @ ( op2 @ e22 @ e20 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl124,zip_derived_cl1690]) ).
thf(zip_derived_cl1715_109,plain,
( ( op2 @ e21 @ e23 )
= ( op2 @ e22 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1686,zip_derived_cl1698]) ).
thf(zip_derived_cl1760,plain,
( ( op2 @ e21 @ e20 )
= ( op2 @ e23 @ ( op2 @ e21 @ e23 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1691,zip_derived_cl1715]) ).
thf(zip_derived_cl1767_110,plain,
( ( op2 @ e20 @ e22 )
= ( op2 @ e21 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl142,zip_derived_cl1698,zip_derived_cl1478,zip_derived_cl1715]) ).
thf(zip_derived_cl1777,plain,
( ( op2 @ e21 @ e20 )
= ( op2 @ e23 @ ( op2 @ e20 @ e22 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1760,zip_derived_cl1767]) ).
thf(zip_derived_cl1782_111,plain,
( ( op2 @ e20 @ e21 )
= ( op2 @ e21 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl143,zip_derived_cl1698,zip_derived_cl1732,zip_derived_cl1762]) ).
thf(zip_derived_cl1788,plain,
( ( op2 @ e20 @ e21 )
= ( op2 @ e23 @ ( op2 @ e20 @ e22 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1777,zip_derived_cl1782]) ).
thf(zip_derived_cl1854_112,plain,
( ( op2 @ e20 @ e22 )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl114,zip_derived_cl1483,zip_derived_cl1694,zip_derived_cl1443]) ).
thf(zip_derived_cl1690_113,plain,
( ( op2 @ e23 @ e22 )
= e21 ),
inference(demod,[status(thm)],[zip_derived_cl138,zip_derived_cl383,zip_derived_cl383,zip_derived_cl1451]) ).
thf(zip_derived_cl1866,plain,
( ( op2 @ e20 @ e21 )
= e21 ),
inference(demod,[status(thm)],[zip_derived_cl1788,zip_derived_cl1854,zip_derived_cl1690]) ).
thf(zip_derived_cl1902,plain,
( e21
= ( op2 @ e21 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1782,zip_derived_cl1866]) ).
thf(zip_derived_cl1553_114,plain,
( ( op1 @ e11 @ e13 )
= e12 ),
inference(demod,[status(thm)],[zip_derived_cl1541,zip_derived_cl1546]) ).
thf(zip_derived_cl393_115,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl1870_116,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl1887_117,plain,
( ( h2 @ e13 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1750,zip_derived_cl1864]) ).
thf(zip_derived_cl1451_118,plain,
( e21
= ( op2 @ e22 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl384,zip_derived_cl383]) ).
thf(zip_derived_cl1470_119,plain,
( e10
= ( op1 @ e11 @ e12 ) ),
inference(demod,[status(thm)],[zip_derived_cl382,zip_derived_cl380,zip_derived_cl1444]) ).
thf(zip_derived_cl1877_120,plain,
( ( h2 @ e10 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1831,zip_derived_cl1870,zip_derived_cl1698]) ).
thf(zip_derived_cl1870_121,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl393_122,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl1698_123,plain,
( e20
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1668,zip_derived_cl1690]) ).
thf(zip_derived_cl22,plain,
( ( op1 @ ( op1 @ e13 @ e12 ) @ e11 )
= ( op1 @ e13 @ ( op1 @ e12 @ e11 ) ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl1505_124,plain,
( ( op1 @ e13 @ e12 )
= e11 ),
inference(demod,[status(thm)],[zip_derived_cl37,zip_derived_cl380,zip_derived_cl380,zip_derived_cl1444]) ).
thf(zip_derived_cl1506,plain,
( ( op1 @ e11 @ e11 )
= ( op1 @ e13 @ ( op1 @ e12 @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl22,zip_derived_cl1505]) ).
thf(zip_derived_cl1514_125,plain,
( e10
= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1487,zip_derived_cl1505]) ).
thf(zip_derived_cl1586,plain,
( ( op1 @ e11 @ e11 )
= ( op1 @ e13 @ e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl1506,zip_derived_cl1514]) ).
thf(zip_derived_cl1587_126,plain,
( ( op1 @ e13 @ e10 )
= e13 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3,zip_derived_cl1537,zip_derived_cl1509,zip_derived_cl1560]) ).
thf(zip_derived_cl1599,plain,
( ( op1 @ e11 @ e11 )
= e13 ),
inference(demod,[status(thm)],[zip_derived_cl1586,zip_derived_cl1587]) ).
thf(zip_derived_cl1887_127,plain,
( ( h2 @ e13 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1750,zip_derived_cl1864]) ).
thf(zip_derived_cl1870_128,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl1870_129,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl383_130,plain,
( e23
= ( op2 @ e22 @ e22 ) ),
inference(cnf,[status(esa)],[ax25]) ).
thf(zip_derived_cl35,plain,
( ( op1 @ ( op1 @ e12 @ e13 ) @ e10 )
= ( op1 @ e12 @ ( op1 @ e13 @ e10 ) ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl1444_131,plain,
( e11
= ( op1 @ e12 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl381,zip_derived_cl380]) ).
thf(zip_derived_cl1489,plain,
( ( op1 @ e11 @ e10 )
= ( op1 @ e12 @ ( op1 @ e13 @ e10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl35,zip_derived_cl1444]) ).
thf(zip_derived_cl1586_132,plain,
( ( op1 @ e11 @ e11 )
= ( op1 @ e13 @ e10 ) ),
inference(demod,[status(thm)],[zip_derived_cl1506,zip_derived_cl1514]) ).
thf(zip_derived_cl42,plain,
( ( op1 @ ( op1 @ e12 @ e11 ) @ e11 )
= ( op1 @ e12 @ ( op1 @ e11 @ e11 ) ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl1514_133,plain,
( e10
= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1487,zip_derived_cl1505]) ).
thf(zip_derived_cl1573,plain,
( ( op1 @ e10 @ e11 )
= ( op1 @ e12 @ ( op1 @ e11 @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl42,zip_derived_cl1514]) ).
thf(zip_derived_cl1592,plain,
( ( op1 @ e11 @ e10 )
= ( op1 @ e10 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1489,zip_derived_cl1586,zip_derived_cl1573]) ).
thf(zip_derived_cl1573_134,plain,
( ( op1 @ e10 @ e11 )
= ( op1 @ e12 @ ( op1 @ e11 @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl42,zip_derived_cl1514]) ).
thf(zip_derived_cl1599_135,plain,
( ( op1 @ e11 @ e11 )
= e13 ),
inference(demod,[status(thm)],[zip_derived_cl1586,zip_derived_cl1587]) ).
thf(zip_derived_cl1444_136,plain,
( e11
= ( op1 @ e12 @ e13 ) ),
inference(demod,[status(thm)],[zip_derived_cl381,zip_derived_cl380]) ).
thf(zip_derived_cl1604,plain,
( ( op1 @ e10 @ e11 )
= e11 ),
inference(demod,[status(thm)],[zip_derived_cl1573,zip_derived_cl1599,zip_derived_cl1444]) ).
thf(zip_derived_cl1613,plain,
( ( op1 @ e11 @ e10 )
= e11 ),
inference(demod,[status(thm)],[zip_derived_cl1592,zip_derived_cl1604]) ).
thf(zip_derived_cl1870_137,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl1870_138,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl1877_139,plain,
( ( h2 @ e10 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1831,zip_derived_cl1870,zip_derived_cl1698]) ).
thf(zip_derived_cl1773_140,plain,
( ( op2 @ e20 @ e22 )
= ( op2 @ e22 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1715,zip_derived_cl1767]) ).
thf(zip_derived_cl1854_141,plain,
( ( op2 @ e20 @ e22 )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl114,zip_derived_cl1483,zip_derived_cl1694,zip_derived_cl1443]) ).
thf(zip_derived_cl1863,plain,
( e22
= ( op2 @ e22 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl40,plain,
( ( op1 @ ( op1 @ e12 @ e11 ) @ e13 )
= ( op1 @ e12 @ ( op1 @ e11 @ e13 ) ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl1514_142,plain,
( e10
= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1487,zip_derived_cl1505]) ).
thf(zip_derived_cl1552,plain,
( ( op1 @ e10 @ e13 )
= ( op1 @ e12 @ ( op1 @ e11 @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl40,zip_derived_cl1514]) ).
thf(zip_derived_cl1553_143,plain,
( ( op1 @ e11 @ e13 )
= e12 ),
inference(demod,[status(thm)],[zip_derived_cl1541,zip_derived_cl1546]) ).
thf(zip_derived_cl380_144,plain,
( e13
= ( op1 @ e12 @ e12 ) ),
inference(cnf,[status(esa)],[ax24]) ).
thf(zip_derived_cl1564,plain,
( ( op1 @ e10 @ e13 )
= e13 ),
inference(demod,[status(thm)],[zip_derived_cl1552,zip_derived_cl1553,zip_derived_cl380]) ).
thf(zip_derived_cl1887_145,plain,
( ( h2 @ e13 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1750,zip_derived_cl1864]) ).
thf(zip_derived_cl1877_146,plain,
( ( h2 @ e10 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1831,zip_derived_cl1870,zip_derived_cl1698]) ).
thf(zip_derived_cl1887_147,plain,
( ( h2 @ e13 )
= e23 ),
inference(demod,[status(thm)],[zip_derived_cl1750,zip_derived_cl1864]) ).
thf(zip_derived_cl1864_148,plain,
( e23
= ( op2 @ e20 @ e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1778,zip_derived_cl1854,zip_derived_cl383]) ).
thf(zip_derived_cl41,plain,
( ( op1 @ ( op1 @ e12 @ e11 ) @ e12 )
= ( op1 @ e12 @ ( op1 @ e11 @ e12 ) ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl1514_149,plain,
( e10
= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1487,zip_derived_cl1505]) ).
thf(zip_derived_cl1470_150,plain,
( e10
= ( op1 @ e11 @ e12 ) ),
inference(demod,[status(thm)],[zip_derived_cl382,zip_derived_cl380,zip_derived_cl1444]) ).
thf(zip_derived_cl1546_151,plain,
( ( op1 @ e12 @ e10 )
= e12 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1432,zip_derived_cl1515,zip_derived_cl1446]) ).
thf(zip_derived_cl1565,plain,
( ( op1 @ e10 @ e12 )
= e12 ),
inference(demod,[status(thm)],[zip_derived_cl41,zip_derived_cl1514,zip_derived_cl1470,zip_derived_cl1546]) ).
thf(zip_derived_cl393_152,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl1877_153,plain,
( ( h2 @ e10 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1831,zip_derived_cl1870,zip_derived_cl1698]) ).
thf(zip_derived_cl393_154,plain,
( ( h2 @ e12 )
= e21 ),
inference(cnf,[status(esa)],[ax27]) ).
thf(zip_derived_cl1866_155,plain,
( ( op2 @ e20 @ e21 )
= e21 ),
inference(demod,[status(thm)],[zip_derived_cl1788,zip_derived_cl1854,zip_derived_cl1690]) ).
thf(zip_derived_cl1604_156,plain,
( ( op1 @ e10 @ e11 )
= e11 ),
inference(demod,[status(thm)],[zip_derived_cl1573,zip_derived_cl1599,zip_derived_cl1444]) ).
thf(zip_derived_cl1870_157,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl1877_158,plain,
( ( h2 @ e10 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1831,zip_derived_cl1870,zip_derived_cl1698]) ).
thf(zip_derived_cl1870_159,plain,
( e22
= ( h2 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1798,zip_derived_cl1854,zip_derived_cl1773,zip_derived_cl1854]) ).
thf(zip_derived_cl1854_160,plain,
( ( op2 @ e20 @ e22 )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl114,zip_derived_cl1483,zip_derived_cl1694,zip_derived_cl1443]) ).
thf(zip_derived_cl43,plain,
( ( op1 @ ( op1 @ e12 @ e11 ) @ e10 )
= ( op1 @ e12 @ ( op1 @ e11 @ e10 ) ) ),
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl1514_161,plain,
( e10
= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1487,zip_derived_cl1505]) ).
thf(zip_derived_cl1580,plain,
( ( op1 @ e10 @ e10 )
= ( op1 @ e12 @ ( op1 @ e11 @ e10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl43,zip_derived_cl1514]) ).
thf(zip_derived_cl1613_162,plain,
( ( op1 @ e11 @ e10 )
= e11 ),
inference(demod,[status(thm)],[zip_derived_cl1592,zip_derived_cl1604]) ).
thf(zip_derived_cl1514_163,plain,
( e10
= ( op1 @ e12 @ e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1487,zip_derived_cl1505]) ).
thf(zip_derived_cl1617,plain,
( ( op1 @ e10 @ e10 )
= e10 ),
inference(demod,[status(thm)],[zip_derived_cl1580,zip_derived_cl1613,zip_derived_cl1514]) ).
thf(zip_derived_cl1877_164,plain,
( ( h2 @ e10 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1831,zip_derived_cl1870,zip_derived_cl1698]) ).
thf(zip_derived_cl1877_165,plain,
( ( h2 @ e10 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1831,zip_derived_cl1870,zip_derived_cl1698]) ).
thf(zip_derived_cl1877_166,plain,
( ( h2 @ e10 )
= e20 ),
inference(demod,[status(thm)],[zip_derived_cl1831,zip_derived_cl1870,zip_derived_cl1698]) ).
thf(zip_derived_cl147,plain,
( ( op2 @ ( op2 @ e22 @ e20 ) @ e21 )
= ( op2 @ e22 @ ( op2 @ e20 @ e21 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1773_167,plain,
( ( op2 @ e20 @ e22 )
= ( op2 @ e22 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1715,zip_derived_cl1767]) ).
thf(zip_derived_cl144,plain,
( ( op2 @ ( op2 @ e22 @ e21 ) @ e20 )
= ( op2 @ e22 @ ( op2 @ e21 @ e20 ) ) ),
inference(cnf,[status(esa)],[ax6]) ).
thf(zip_derived_cl1698_168,plain,
( e20
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1668,zip_derived_cl1690]) ).
thf(zip_derived_cl1782_169,plain,
( ( op2 @ e20 @ e21 )
= ( op2 @ e21 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl143,zip_derived_cl1698,zip_derived_cl1732,zip_derived_cl1762]) ).
thf(zip_derived_cl1789,plain,
( ( op2 @ e20 @ e20 )
= ( op2 @ e22 @ ( op2 @ e20 @ e21 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl144,zip_derived_cl1698,zip_derived_cl1782]) ).
thf(zip_derived_cl1792,plain,
( ( op2 @ ( op2 @ e20 @ e22 ) @ e21 )
= ( op2 @ e20 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl147,zip_derived_cl1773,zip_derived_cl1789]) ).
thf(zip_derived_cl1854_170,plain,
( ( op2 @ e20 @ e22 )
= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl114,zip_derived_cl1483,zip_derived_cl1694,zip_derived_cl1443]) ).
thf(zip_derived_cl1698_171,plain,
( e20
= ( op2 @ e22 @ e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1668,zip_derived_cl1690]) ).
thf(zip_derived_cl1868,plain,
( e20
= ( op2 @ e20 @ e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1792,zip_derived_cl1854,zip_derived_cl1698]) ).
thf(zip_derived_cl3018,plain,
( ( e23 != e23 )
| ( e22 != e22 )
| ( e21 != e21 )
| ( e20 != e20 )
| ( e20 != e20 )
| ( e22 != e22 )
| ( e21 != e21 )
| ( e23 != e23 )
| ( e22 != e22 )
| ( e23 != e23 )
| ( e20 != e20 )
| ( e21 != e21 )
| ( e21 != e21 )
| ( e20 != e20 )
| ( e23 != e23 )
| ( e22 != e22 )
| ( e23 != e23 )
| ( e21 != e21 )
| ( e22 != e22 )
| ( e20 != e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl678,zip_derived_cl1887,zip_derived_cl1870,zip_derived_cl393,zip_derived_cl1877,zip_derived_cl1521,zip_derived_cl1877,zip_derived_cl1887,zip_derived_cl1887,zip_derived_cl1708,zip_derived_cl1505,zip_derived_cl1870,zip_derived_cl1887,zip_derived_cl393,zip_derived_cl1862,zip_derived_cl1559,zip_derived_cl393,zip_derived_cl1887,zip_derived_cl1870,zip_derived_cl1690,zip_derived_cl1587,zip_derived_cl1887,zip_derived_cl1887,zip_derived_cl1877,zip_derived_cl1888,zip_derived_cl1444,zip_derived_cl1870,zip_derived_cl393,zip_derived_cl1887,zip_derived_cl1861,zip_derived_cl380,zip_derived_cl1887,zip_derived_cl393,zip_derived_cl393,zip_derived_cl1886,zip_derived_cl1514,zip_derived_cl1877,zip_derived_cl393,zip_derived_cl1870,zip_derived_cl1478,zip_derived_cl1546,zip_derived_cl393,zip_derived_cl393,zip_derived_cl1877,zip_derived_cl1902,zip_derived_cl1553,zip_derived_cl393,zip_derived_cl1870,zip_derived_cl1887,zip_derived_cl1451,zip_derived_cl1470,zip_derived_cl1877,zip_derived_cl1870,zip_derived_cl393,zip_derived_cl1698,zip_derived_cl1599,zip_derived_cl1887,zip_derived_cl1870,zip_derived_cl1870,zip_derived_cl383,zip_derived_cl1613,zip_derived_cl1870,zip_derived_cl1870,zip_derived_cl1877,zip_derived_cl1863,zip_derived_cl1564,zip_derived_cl1887,zip_derived_cl1877,zip_derived_cl1887,zip_derived_cl1864,zip_derived_cl1565,zip_derived_cl393,zip_derived_cl1877,zip_derived_cl393,zip_derived_cl1866,zip_derived_cl1604,zip_derived_cl1870,zip_derived_cl1877,zip_derived_cl1870,zip_derived_cl1854,zip_derived_cl1617,zip_derived_cl1877,zip_derived_cl1877,zip_derived_cl1877,zip_derived_cl1868]) ).
thf(zip_derived_cl3019,plain,
$false,
inference(simplify,[status(thm)],[zip_derived_cl3018]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : ALG016+1 : TPTP v9.2.0. Released v2.7.0.
% 0.12/0.14 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.xD06X814j8 true
% 0.14/0.35 % Computer : n021.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Oct 1 17:05:53 EDT 2025
% 0.14/0.35 % CPUTime :
% 0.14/0.35 % Running portfolio for 300 s
% 0.14/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.35 % Number of cores: 8
% 0.14/0.36 % Python version: Python 3.6.8
% 0.14/0.36 % Running in FO mode
% 0.55/0.64 % Total configuration time : 435
% 0.55/0.64 % Estimated wc time : 1092
% 0.55/0.64 % Estimated cpu time (7 cpus) : 156.0
% 0.56/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.56/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.56/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.56/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.56/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.56/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.56/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 5.24/1.34 % Solved by fo/fo13.sh.
% 5.24/1.34 % done 0 iterations in 0.545s
% 5.24/1.34 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 5.24/1.34 % SZS output start Refutation
% See solution above
% 5.24/1.34
% 5.24/1.34
% 5.24/1.34 % Terminating...
% 5.70/1.45 % Runner terminated.
% 5.70/1.46 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------