%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : ALG206+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.DZsW5sjX61 true
% Computer : n001.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:28:17 PM UTC 2025
% Result : Theorem 0.85s 1.16s
% Output : Refutation 0.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 4
% Syntax : Number of formulae : 394 ( 180 unt; 0 typ; 0 def)
% Number of atoms : 1238 (1230 equ; 0 cnn)
% Maximal formula atoms : 210 ( 3 avg)
% Number of connectives : 3710 ( 126 ~; 269 |; 395 &;2740 @)
% ( 0 <=>; 2 =>; 178 <=; 0 <~>)
% Maximal formula depth : 115 ( 3 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 20 ( 18 usr; 15 con; 0-2 aty)
% Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
thf(e16_type,type,
e16: $i ).
thf(e24_type,type,
e24: $i ).
thf(e15_type,type,
e15: $i ).
thf(j_type,type,
j: $i > $i ).
thf(e20_type,type,
e20: $i ).
thf(e14_type,type,
e14: $i ).
thf(e23_type,type,
e23: $i ).
thf(e22_type,type,
e22: $i ).
thf(e13_type,type,
e13: $i ).
thf(e12_type,type,
e12: $i ).
thf(e11_type,type,
e11: $i ).
thf(e10_type,type,
e10: $i ).
thf(h_type,type,
h: $i > $i ).
thf(e26_type,type,
e26: $i ).
thf(e25_type,type,
e25: $i ).
thf(e21_type,type,
e21: $i ).
thf(op2_type,type,
op2: $i > $i > $i ).
thf(op1_type,type,
op1: $i > $i > $i ).
thf(co1,conjecture,
( ( ( ( ( h @ e10 )
= e20 )
| ( ( h @ e10 )
= e21 )
| ( ( h @ e10 )
= e22 )
| ( ( h @ e10 )
= e23 )
| ( ( h @ e10 )
= e24 )
| ( ( h @ e10 )
= e25 )
| ( ( h @ e10 )
= e26 ) )
& ( ( ( h @ e11 )
= e20 )
| ( ( h @ e11 )
= e21 )
| ( ( h @ e11 )
= e22 )
| ( ( h @ e11 )
= e23 )
| ( ( h @ e11 )
= e24 )
| ( ( h @ e11 )
= e25 )
| ( ( h @ e11 )
= e26 ) )
& ( ( ( h @ e12 )
= e20 )
| ( ( h @ e12 )
= e21 )
| ( ( h @ e12 )
= e22 )
| ( ( h @ e12 )
= e23 )
| ( ( h @ e12 )
= e24 )
| ( ( h @ e12 )
= e25 )
| ( ( h @ e12 )
= e26 ) )
& ( ( ( h @ e13 )
= e20 )
| ( ( h @ e13 )
= e21 )
| ( ( h @ e13 )
= e22 )
| ( ( h @ e13 )
= e23 )
| ( ( h @ e13 )
= e24 )
| ( ( h @ e13 )
= e25 )
| ( ( h @ e13 )
= e26 ) )
& ( ( ( h @ e14 )
= e20 )
| ( ( h @ e14 )
= e21 )
| ( ( h @ e14 )
= e22 )
| ( ( h @ e14 )
= e23 )
| ( ( h @ e14 )
= e24 )
| ( ( h @ e14 )
= e25 )
| ( ( h @ e14 )
= e26 ) )
& ( ( ( h @ e15 )
= e20 )
| ( ( h @ e15 )
= e21 )
| ( ( h @ e15 )
= e22 )
| ( ( h @ e15 )
= e23 )
| ( ( h @ e15 )
= e24 )
| ( ( h @ e15 )
= e25 )
| ( ( h @ e15 )
= e26 ) )
& ( ( ( h @ e16 )
= e20 )
| ( ( h @ e16 )
= e21 )
| ( ( h @ e16 )
= e22 )
| ( ( h @ e16 )
= e23 )
| ( ( h @ e16 )
= e24 )
| ( ( h @ e16 )
= e25 )
| ( ( h @ e16 )
= e26 ) )
& ( ( ( j @ e20 )
= e10 )
| ( ( j @ e20 )
= e11 )
| ( ( j @ e20 )
= e12 )
| ( ( j @ e20 )
= e13 )
| ( ( j @ e20 )
= e14 )
| ( ( j @ e20 )
= e15 )
| ( ( j @ e20 )
= e16 ) )
& ( ( ( j @ e21 )
= e10 )
| ( ( j @ e21 )
= e11 )
| ( ( j @ e21 )
= e12 )
| ( ( j @ e21 )
= e13 )
| ( ( j @ e21 )
= e14 )
| ( ( j @ e21 )
= e15 )
| ( ( j @ e21 )
= e16 ) )
& ( ( ( j @ e22 )
= e10 )
| ( ( j @ e22 )
= e11 )
| ( ( j @ e22 )
= e12 )
| ( ( j @ e22 )
= e13 )
| ( ( j @ e22 )
= e14 )
| ( ( j @ e22 )
= e15 )
| ( ( j @ e22 )
= e16 ) )
& ( ( ( j @ e23 )
= e10 )
| ( ( j @ e23 )
= e11 )
| ( ( j @ e23 )
= e12 )
| ( ( j @ e23 )
= e13 )
| ( ( j @ e23 )
= e14 )
| ( ( j @ e23 )
= e15 )
| ( ( j @ e23 )
= e16 ) )
& ( ( ( j @ e24 )
= e10 )
| ( ( j @ e24 )
= e11 )
| ( ( j @ e24 )
= e12 )
| ( ( j @ e24 )
= e13 )
| ( ( j @ e24 )
= e14 )
| ( ( j @ e24 )
= e15 )
| ( ( j @ e24 )
= e16 ) )
& ( ( ( j @ e25 )
= e10 )
| ( ( j @ e25 )
= e11 )
| ( ( j @ e25 )
= e12 )
| ( ( j @ e25 )
= e13 )
| ( ( j @ e25 )
= e14 )
| ( ( j @ e25 )
= e15 )
| ( ( j @ e25 )
= e16 ) )
& ( ( ( j @ e26 )
= e10 )
| ( ( j @ e26 )
= e11 )
| ( ( j @ e26 )
= e12 )
| ( ( j @ e26 )
= e13 )
| ( ( j @ e26 )
= e14 )
| ( ( j @ e26 )
= e15 )
| ( ( j @ e26 )
= e16 ) ) )
=> ~ ( ( ( h @ ( op1 @ e10 @ e10 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e10 @ e11 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e10 @ e12 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e10 @ e13 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e10 @ e14 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e10 @ e15 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e10 @ e16 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e16 ) ) )
& ( ( h @ ( op1 @ e11 @ e10 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e11 @ e11 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e11 @ e12 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e11 @ e13 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e11 @ e14 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e11 @ e15 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e11 @ e16 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e16 ) ) )
& ( ( h @ ( op1 @ e12 @ e10 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e12 @ e11 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e12 @ e12 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e12 @ e13 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e12 @ e14 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e12 @ e15 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e12 @ e16 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e16 ) ) )
& ( ( h @ ( op1 @ e13 @ e10 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e13 @ e11 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e13 @ e12 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e13 @ e13 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e13 @ e14 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e13 @ e15 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e13 @ e16 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e16 ) ) )
& ( ( h @ ( op1 @ e14 @ e10 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e14 @ e11 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e14 @ e12 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e14 @ e13 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e14 @ e14 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e14 @ e15 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e14 @ e16 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e16 ) ) )
& ( ( h @ ( op1 @ e15 @ e10 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e15 @ e11 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e15 @ e12 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e15 @ e13 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e15 @ e14 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e15 @ e15 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e15 @ e16 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e16 ) ) )
& ( ( h @ ( op1 @ e16 @ e10 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e16 @ e11 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e16 @ e12 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e16 @ e13 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e16 @ e14 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e16 @ e15 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e16 @ e16 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e16 ) ) )
& ( ( j @ ( op2 @ e20 @ e20 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e20 @ e21 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e20 @ e22 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e20 @ e23 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e20 @ e24 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e20 @ e25 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e20 @ e26 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e26 ) ) )
& ( ( j @ ( op2 @ e21 @ e20 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e21 @ e21 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e21 @ e22 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e21 @ e23 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e21 @ e24 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e21 @ e25 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e21 @ e26 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e26 ) ) )
& ( ( j @ ( op2 @ e22 @ e20 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e22 @ e21 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e22 @ e22 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e22 @ e23 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e22 @ e24 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e22 @ e25 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e22 @ e26 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e26 ) ) )
& ( ( j @ ( op2 @ e23 @ e20 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e23 @ e21 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e23 @ e22 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e23 @ e23 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e23 @ e24 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e23 @ e25 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e23 @ e26 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e26 ) ) )
& ( ( j @ ( op2 @ e24 @ e20 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e24 @ e21 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e24 @ e22 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e24 @ e23 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e24 @ e24 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e24 @ e25 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e24 @ e26 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e26 ) ) )
& ( ( j @ ( op2 @ e25 @ e20 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e25 @ e21 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e25 @ e22 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e25 @ e23 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e25 @ e24 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e25 @ e25 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e25 @ e26 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e26 ) ) )
& ( ( j @ ( op2 @ e26 @ e20 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e26 @ e21 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e26 @ e22 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e26 @ e23 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e26 @ e24 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e26 @ e25 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e26 @ e26 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e26 ) ) )
& ( ( h @ ( j @ e20 ) )
= e20 )
& ( ( h @ ( j @ e21 ) )
= e21 )
& ( ( h @ ( j @ e22 ) )
= e22 )
& ( ( h @ ( j @ e23 ) )
= e23 )
& ( ( h @ ( j @ e24 ) )
= e24 )
& ( ( h @ ( j @ e25 ) )
= e25 )
& ( ( h @ ( j @ e26 ) )
= e26 )
& ( ( j @ ( h @ e10 ) )
= e10 )
& ( ( j @ ( h @ e11 ) )
= e11 )
& ( ( j @ ( h @ e12 ) )
= e12 )
& ( ( j @ ( h @ e13 ) )
= e13 )
& ( ( j @ ( h @ e14 ) )
= e14 )
& ( ( j @ ( h @ e15 ) )
= e15 )
& ( ( j @ ( h @ e16 ) )
= e16 ) ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ( ( ( ( ( h @ e10 )
= e20 )
| ( ( h @ e10 )
= e21 )
| ( ( h @ e10 )
= e22 )
| ( ( h @ e10 )
= e23 )
| ( ( h @ e10 )
= e24 )
| ( ( h @ e10 )
= e25 )
| ( ( h @ e10 )
= e26 ) )
& ( ( ( h @ e11 )
= e20 )
| ( ( h @ e11 )
= e21 )
| ( ( h @ e11 )
= e22 )
| ( ( h @ e11 )
= e23 )
| ( ( h @ e11 )
= e24 )
| ( ( h @ e11 )
= e25 )
| ( ( h @ e11 )
= e26 ) )
& ( ( ( h @ e12 )
= e20 )
| ( ( h @ e12 )
= e21 )
| ( ( h @ e12 )
= e22 )
| ( ( h @ e12 )
= e23 )
| ( ( h @ e12 )
= e24 )
| ( ( h @ e12 )
= e25 )
| ( ( h @ e12 )
= e26 ) )
& ( ( ( h @ e13 )
= e20 )
| ( ( h @ e13 )
= e21 )
| ( ( h @ e13 )
= e22 )
| ( ( h @ e13 )
= e23 )
| ( ( h @ e13 )
= e24 )
| ( ( h @ e13 )
= e25 )
| ( ( h @ e13 )
= e26 ) )
& ( ( ( h @ e14 )
= e20 )
| ( ( h @ e14 )
= e21 )
| ( ( h @ e14 )
= e22 )
| ( ( h @ e14 )
= e23 )
| ( ( h @ e14 )
= e24 )
| ( ( h @ e14 )
= e25 )
| ( ( h @ e14 )
= e26 ) )
& ( ( ( h @ e15 )
= e20 )
| ( ( h @ e15 )
= e21 )
| ( ( h @ e15 )
= e22 )
| ( ( h @ e15 )
= e23 )
| ( ( h @ e15 )
= e24 )
| ( ( h @ e15 )
= e25 )
| ( ( h @ e15 )
= e26 ) )
& ( ( ( h @ e16 )
= e20 )
| ( ( h @ e16 )
= e21 )
| ( ( h @ e16 )
= e22 )
| ( ( h @ e16 )
= e23 )
| ( ( h @ e16 )
= e24 )
| ( ( h @ e16 )
= e25 )
| ( ( h @ e16 )
= e26 ) )
& ( ( ( j @ e20 )
= e10 )
| ( ( j @ e20 )
= e11 )
| ( ( j @ e20 )
= e12 )
| ( ( j @ e20 )
= e13 )
| ( ( j @ e20 )
= e14 )
| ( ( j @ e20 )
= e15 )
| ( ( j @ e20 )
= e16 ) )
& ( ( ( j @ e21 )
= e10 )
| ( ( j @ e21 )
= e11 )
| ( ( j @ e21 )
= e12 )
| ( ( j @ e21 )
= e13 )
| ( ( j @ e21 )
= e14 )
| ( ( j @ e21 )
= e15 )
| ( ( j @ e21 )
= e16 ) )
& ( ( ( j @ e22 )
= e10 )
| ( ( j @ e22 )
= e11 )
| ( ( j @ e22 )
= e12 )
| ( ( j @ e22 )
= e13 )
| ( ( j @ e22 )
= e14 )
| ( ( j @ e22 )
= e15 )
| ( ( j @ e22 )
= e16 ) )
& ( ( ( j @ e23 )
= e10 )
| ( ( j @ e23 )
= e11 )
| ( ( j @ e23 )
= e12 )
| ( ( j @ e23 )
= e13 )
| ( ( j @ e23 )
= e14 )
| ( ( j @ e23 )
= e15 )
| ( ( j @ e23 )
= e16 ) )
& ( ( ( j @ e24 )
= e10 )
| ( ( j @ e24 )
= e11 )
| ( ( j @ e24 )
= e12 )
| ( ( j @ e24 )
= e13 )
| ( ( j @ e24 )
= e14 )
| ( ( j @ e24 )
= e15 )
| ( ( j @ e24 )
= e16 ) )
& ( ( ( j @ e25 )
= e10 )
| ( ( j @ e25 )
= e11 )
| ( ( j @ e25 )
= e12 )
| ( ( j @ e25 )
= e13 )
| ( ( j @ e25 )
= e14 )
| ( ( j @ e25 )
= e15 )
| ( ( j @ e25 )
= e16 ) )
& ( ( ( j @ e26 )
= e10 )
| ( ( j @ e26 )
= e11 )
| ( ( j @ e26 )
= e12 )
| ( ( j @ e26 )
= e13 )
| ( ( j @ e26 )
= e14 )
| ( ( j @ e26 )
= e15 )
| ( ( j @ e26 )
= e16 ) ) )
=> ~ ( ( ( h @ ( op1 @ e10 @ e10 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e10 @ e11 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e10 @ e12 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e10 @ e13 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e10 @ e14 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e10 @ e15 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e10 @ e16 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e16 ) ) )
& ( ( h @ ( op1 @ e11 @ e10 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e11 @ e11 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e11 @ e12 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e11 @ e13 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e11 @ e14 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e11 @ e15 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e11 @ e16 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e16 ) ) )
& ( ( h @ ( op1 @ e12 @ e10 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e12 @ e11 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e12 @ e12 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e12 @ e13 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e12 @ e14 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e12 @ e15 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e12 @ e16 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e16 ) ) )
& ( ( h @ ( op1 @ e13 @ e10 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e13 @ e11 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e13 @ e12 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e13 @ e13 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e13 @ e14 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e13 @ e15 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e13 @ e16 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e16 ) ) )
& ( ( h @ ( op1 @ e14 @ e10 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e14 @ e11 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e14 @ e12 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e14 @ e13 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e14 @ e14 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e14 @ e15 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e14 @ e16 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e16 ) ) )
& ( ( h @ ( op1 @ e15 @ e10 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e15 @ e11 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e15 @ e12 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e15 @ e13 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e15 @ e14 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e15 @ e15 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e15 @ e16 ) )
= ( op2 @ ( h @ e15 ) @ ( h @ e16 ) ) )
& ( ( h @ ( op1 @ e16 @ e10 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e10 ) ) )
& ( ( h @ ( op1 @ e16 @ e11 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e11 ) ) )
& ( ( h @ ( op1 @ e16 @ e12 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e12 ) ) )
& ( ( h @ ( op1 @ e16 @ e13 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e13 ) ) )
& ( ( h @ ( op1 @ e16 @ e14 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e14 ) ) )
& ( ( h @ ( op1 @ e16 @ e15 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e15 ) ) )
& ( ( h @ ( op1 @ e16 @ e16 ) )
= ( op2 @ ( h @ e16 ) @ ( h @ e16 ) ) )
& ( ( j @ ( op2 @ e20 @ e20 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e20 @ e21 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e20 @ e22 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e20 @ e23 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e20 @ e24 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e20 @ e25 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e20 @ e26 ) )
= ( op1 @ ( j @ e20 ) @ ( j @ e26 ) ) )
& ( ( j @ ( op2 @ e21 @ e20 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e21 @ e21 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e21 @ e22 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e21 @ e23 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e21 @ e24 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e21 @ e25 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e21 @ e26 ) )
= ( op1 @ ( j @ e21 ) @ ( j @ e26 ) ) )
& ( ( j @ ( op2 @ e22 @ e20 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e22 @ e21 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e22 @ e22 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e22 @ e23 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e22 @ e24 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e22 @ e25 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e22 @ e26 ) )
= ( op1 @ ( j @ e22 ) @ ( j @ e26 ) ) )
& ( ( j @ ( op2 @ e23 @ e20 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e23 @ e21 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e23 @ e22 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e23 @ e23 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e23 @ e24 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e23 @ e25 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e23 @ e26 ) )
= ( op1 @ ( j @ e23 ) @ ( j @ e26 ) ) )
& ( ( j @ ( op2 @ e24 @ e20 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e24 @ e21 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e24 @ e22 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e24 @ e23 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e24 @ e24 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e24 @ e25 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e24 @ e26 ) )
= ( op1 @ ( j @ e24 ) @ ( j @ e26 ) ) )
& ( ( j @ ( op2 @ e25 @ e20 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e25 @ e21 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e25 @ e22 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e25 @ e23 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e25 @ e24 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e25 @ e25 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e25 @ e26 ) )
= ( op1 @ ( j @ e25 ) @ ( j @ e26 ) ) )
& ( ( j @ ( op2 @ e26 @ e20 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e20 ) ) )
& ( ( j @ ( op2 @ e26 @ e21 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e21 ) ) )
& ( ( j @ ( op2 @ e26 @ e22 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e22 ) ) )
& ( ( j @ ( op2 @ e26 @ e23 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e23 ) ) )
& ( ( j @ ( op2 @ e26 @ e24 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e24 ) ) )
& ( ( j @ ( op2 @ e26 @ e25 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e25 ) ) )
& ( ( j @ ( op2 @ e26 @ e26 ) )
= ( op1 @ ( j @ e26 ) @ ( j @ e26 ) ) )
& ( ( h @ ( j @ e20 ) )
= e20 )
& ( ( h @ ( j @ e21 ) )
= e21 )
& ( ( h @ ( j @ e22 ) )
= e22 )
& ( ( h @ ( j @ e23 ) )
= e23 )
& ( ( h @ ( j @ e24 ) )
= e24 )
& ( ( h @ ( j @ e25 ) )
= e25 )
& ( ( h @ ( j @ e26 ) )
= e26 )
& ( ( j @ ( h @ e10 ) )
= e10 )
& ( ( j @ ( h @ e11 ) )
= e11 )
& ( ( j @ ( h @ e12 ) )
= e12 )
& ( ( j @ ( h @ e13 ) )
= e13 )
& ( ( j @ ( h @ e14 ) )
= e14 )
& ( ( j @ ( h @ e15 ) )
= e15 )
& ( ( j @ ( h @ e16 ) )
= e16 ) ) ),
inference('cnf.neg',[status(esa)],[co1]) ).
thf(zip_derived_cl189,plain,
( ( ( h @ e10 )
= e20 )
| ( ( h @ e10 )
= e21 )
| ( ( h @ e10 )
= e22 )
| ( ( h @ e10 )
= e23 )
| ( ( h @ e10 )
= e24 )
| ( ( h @ e10 )
= e25 )
| ( ( h @ e10 )
= e26 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl319,plain,
( ( ( h @ e10 )
= e24 )
<= ( ( h @ e10 )
= e24 ) ),
inference(split,[status(esa)],[zip_derived_cl189]) ).
thf(zip_derived_cl316,plain,
( ( ( h @ e10 )
= e21 )
<= ( ( h @ e10 )
= e21 ) ),
inference(split,[status(esa)],[zip_derived_cl189]) ).
thf(zip_derived_cl203,plain,
( ( h @ ( op1 @ e10 @ e10 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e10 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(ax4,axiom,
( ( ( op1 @ e16 @ e16 )
= e16 )
& ( ( op1 @ e16 @ e15 )
= e12 )
& ( ( op1 @ e16 @ e14 )
= e13 )
& ( ( op1 @ e16 @ e13 )
= e11 )
& ( ( op1 @ e16 @ e12 )
= e10 )
& ( ( op1 @ e16 @ e11 )
= e14 )
& ( ( op1 @ e16 @ e10 )
= e15 )
& ( ( op1 @ e15 @ e16 )
= e12 )
& ( ( op1 @ e15 @ e15 )
= e15 )
& ( ( op1 @ e15 @ e14 )
= e11 )
& ( ( op1 @ e15 @ e13 )
= e16 )
& ( ( op1 @ e15 @ e12 )
= e13 )
& ( ( op1 @ e15 @ e11 )
= e10 )
& ( ( op1 @ e15 @ e10 )
= e14 )
& ( ( op1 @ e14 @ e16 )
= e13 )
& ( ( op1 @ e14 @ e15 )
= e11 )
& ( ( op1 @ e14 @ e14 )
= e14 )
& ( ( op1 @ e14 @ e13 )
= e10 )
& ( ( op1 @ e14 @ e12 )
= e15 )
& ( ( op1 @ e14 @ e11 )
= e12 )
& ( ( op1 @ e14 @ e10 )
= e16 )
& ( ( op1 @ e13 @ e16 )
= e11 )
& ( ( op1 @ e13 @ e15 )
= e16 )
& ( ( op1 @ e13 @ e14 )
= e10 )
& ( ( op1 @ e13 @ e13 )
= e13 )
& ( ( op1 @ e13 @ e12 )
= e14 )
& ( ( op1 @ e13 @ e11 )
= e15 )
& ( ( op1 @ e13 @ e10 )
= e12 )
& ( ( op1 @ e12 @ e16 )
= e10 )
& ( ( op1 @ e12 @ e15 )
= e13 )
& ( ( op1 @ e12 @ e14 )
= e15 )
& ( ( op1 @ e12 @ e13 )
= e14 )
& ( ( op1 @ e12 @ e12 )
= e12 )
& ( ( op1 @ e12 @ e11 )
= e16 )
& ( ( op1 @ e12 @ e10 )
= e11 )
& ( ( op1 @ e11 @ e16 )
= e14 )
& ( ( op1 @ e11 @ e15 )
= e10 )
& ( ( op1 @ e11 @ e14 )
= e12 )
& ( ( op1 @ e11 @ e13 )
= e15 )
& ( ( op1 @ e11 @ e12 )
= e16 )
& ( ( op1 @ e11 @ e11 )
= e11 )
& ( ( op1 @ e11 @ e10 )
= e13 )
& ( ( op1 @ e10 @ e16 )
= e15 )
& ( ( op1 @ e10 @ e15 )
= e14 )
& ( ( op1 @ e10 @ e14 )
= e16 )
& ( ( op1 @ e10 @ e13 )
= e12 )
& ( ( op1 @ e10 @ e12 )
= e11 )
& ( ( op1 @ e10 @ e11 )
= e13 )
& ( ( op1 @ e10 @ e10 )
= e10 ) ) ).
thf(zip_derived_cl139,plain,
( ( op1 @ e10 @ e10 )
= e10 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl1448,plain,
( ( h @ e10 )
= ( op2 @ ( h @ e10 ) @ ( h @ e10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl203,zip_derived_cl139]) ).
thf(zip_derived_cl1450,plain,
( ( e21
= ( op2 @ e21 @ e21 ) )
<= ( ( h @ e10 )
= e21 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl316,zip_derived_cl1448]) ).
thf(ax5,axiom,
( ( ( op2 @ e26 @ e26 )
= e25 )
& ( ( op2 @ e26 @ e25 )
= e20 )
& ( ( op2 @ e26 @ e24 )
= e21 )
& ( ( op2 @ e26 @ e23 )
= e24 )
& ( ( op2 @ e26 @ e22 )
= e22 )
& ( ( op2 @ e26 @ e21 )
= e23 )
& ( ( op2 @ e26 @ e20 )
= e26 )
& ( ( op2 @ e25 @ e26 )
= e20 )
& ( ( op2 @ e25 @ e25 )
= e21 )
& ( ( op2 @ e25 @ e24 )
= e26 )
& ( ( op2 @ e25 @ e23 )
= e23 )
& ( ( op2 @ e25 @ e22 )
= e25 )
& ( ( op2 @ e25 @ e21 )
= e22 )
& ( ( op2 @ e25 @ e20 )
= e24 )
& ( ( op2 @ e24 @ e26 )
= e21 )
& ( ( op2 @ e24 @ e25 )
= e26 )
& ( ( op2 @ e24 @ e24 )
= e24 )
& ( ( op2 @ e24 @ e23 )
= e22 )
& ( ( op2 @ e24 @ e22 )
= e20 )
& ( ( op2 @ e24 @ e21 )
= e25 )
& ( ( op2 @ e24 @ e20 )
= e23 )
& ( ( op2 @ e23 @ e26 )
= e24 )
& ( ( op2 @ e23 @ e25 )
= e23 )
& ( ( op2 @ e23 @ e24 )
= e22 )
& ( ( op2 @ e23 @ e23 )
= e20 )
& ( ( op2 @ e23 @ e22 )
= e26 )
& ( ( op2 @ e23 @ e21 )
= e21 )
& ( ( op2 @ e23 @ e20 )
= e25 )
& ( ( op2 @ e22 @ e26 )
= e22 )
& ( ( op2 @ e22 @ e25 )
= e25 )
& ( ( op2 @ e22 @ e24 )
= e20 )
& ( ( op2 @ e22 @ e23 )
= e26 )
& ( ( op2 @ e22 @ e22 )
= e23 )
& ( ( op2 @ e22 @ e21 )
= e24 )
& ( ( op2 @ e22 @ e20 )
= e21 )
& ( ( op2 @ e21 @ e26 )
= e23 )
& ( ( op2 @ e21 @ e25 )
= e22 )
& ( ( op2 @ e21 @ e24 )
= e25 )
& ( ( op2 @ e21 @ e23 )
= e21 )
& ( ( op2 @ e21 @ e22 )
= e24 )
& ( ( op2 @ e21 @ e21 )
= e26 )
& ( ( op2 @ e21 @ e20 )
= e20 )
& ( ( op2 @ e20 @ e26 )
= e26 )
& ( ( op2 @ e20 @ e25 )
= e24 )
& ( ( op2 @ e20 @ e24 )
= e23 )
& ( ( op2 @ e20 @ e23 )
= e25 )
& ( ( op2 @ e20 @ e22 )
= e21 )
& ( ( op2 @ e20 @ e21 )
= e20 )
& ( ( op2 @ e20 @ e20 )
= e22 ) ) ).
thf(zip_derived_cl180,plain,
( ( op2 @ e21 @ e21 )
= e26 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1579,plain,
( ( e21 = e26 )
<= ( ( h @ e10 )
= e21 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1450,zip_derived_cl180]) ).
thf(ax2,axiom,
( ( e25 != e26 )
& ( e24 != e26 )
& ( e24 != e25 )
& ( e23 != e26 )
& ( e23 != e25 )
& ( e23 != e24 )
& ( e22 != e26 )
& ( e22 != e25 )
& ( e22 != e24 )
& ( e22 != e23 )
& ( e21 != e26 )
& ( e21 != e25 )
& ( e21 != e24 )
& ( e21 != e23 )
& ( e21 != e22 )
& ( e20 != e26 )
& ( e20 != e25 )
& ( e20 != e24 )
& ( e20 != e23 )
& ( e20 != e22 )
& ( e20 != e21 ) ) ).
thf(zip_derived_cl31,plain,
e21 != e26,
inference(cnf,[status(esa)],[ax2]) ).
thf('0',plain,
( ( h @ e10 )
!= e21 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1579,zip_derived_cl31]) ).
thf(zip_derived_cl318,plain,
( ( ( h @ e10 )
= e23 )
<= ( ( h @ e10 )
= e23 ) ),
inference(split,[status(esa)],[zip_derived_cl189]) ).
thf(zip_derived_cl1448_001,plain,
( ( h @ e10 )
= ( op2 @ ( h @ e10 ) @ ( h @ e10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl203,zip_derived_cl139]) ).
thf(zip_derived_cl1452,plain,
( ( e23
= ( op2 @ e23 @ e23 ) )
<= ( ( h @ e10 )
= e23 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl318,zip_derived_cl1448]) ).
thf(zip_derived_cl164,plain,
( ( op2 @ e23 @ e23 )
= e20 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1465,plain,
( ( e23 = e20 )
<= ( ( h @ e10 )
= e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1452,zip_derived_cl164]) ).
thf(zip_derived_cl39,plain,
e20 != e23,
inference(cnf,[status(esa)],[ax2]) ).
thf('1',plain,
( ( h @ e10 )
!= e23 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1465,zip_derived_cl39]) ).
thf(zip_derived_cl315,plain,
( ( ( h @ e10 )
= e20 )
<= ( ( h @ e10 )
= e20 ) ),
inference(split,[status(esa)],[zip_derived_cl189]) ).
thf(zip_derived_cl1448_002,plain,
( ( h @ e10 )
= ( op2 @ ( h @ e10 ) @ ( h @ e10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl203,zip_derived_cl139]) ).
thf(zip_derived_cl1449,plain,
( ( e20
= ( op2 @ e20 @ e20 ) )
<= ( ( h @ e10 )
= e20 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl315,zip_derived_cl1448]) ).
thf(zip_derived_cl188,plain,
( ( op2 @ e20 @ e20 )
= e22 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1577,plain,
( ( e20 = e22 )
<= ( ( h @ e10 )
= e20 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1449,zip_derived_cl188]) ).
thf(zip_derived_cl40,plain,
e20 != e22,
inference(cnf,[status(esa)],[ax2]) ).
thf('2',plain,
( ( h @ e10 )
!= e20 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1577,zip_derived_cl40]) ).
thf(zip_derived_cl321,plain,
( ( ( h @ e10 )
= e26 )
<= ( ( h @ e10 )
= e26 ) ),
inference(split,[status(esa)],[zip_derived_cl189]) ).
thf(zip_derived_cl1448_003,plain,
( ( h @ e10 )
= ( op2 @ ( h @ e10 ) @ ( h @ e10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl203,zip_derived_cl139]) ).
thf(zip_derived_cl1455,plain,
( ( e26
= ( op2 @ e26 @ e26 ) )
<= ( ( h @ e10 )
= e26 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl321,zip_derived_cl1448]) ).
thf(zip_derived_cl140,plain,
( ( op2 @ e26 @ e26 )
= e25 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1469,plain,
( ( e26 = e25 )
<= ( ( h @ e10 )
= e26 ) ),
inference(demod,[status(thm)],[zip_derived_cl1455,zip_derived_cl140]) ).
thf(zip_derived_cl21,plain,
e25 != e26,
inference(cnf,[status(esa)],[ax2]) ).
thf('3',plain,
( ( h @ e10 )
!= e26 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1469,zip_derived_cl21]) ).
thf(zip_derived_cl320,plain,
( ( ( h @ e10 )
= e25 )
<= ( ( h @ e10 )
= e25 ) ),
inference(split,[status(esa)],[zip_derived_cl189]) ).
thf(zip_derived_cl1448_004,plain,
( ( h @ e10 )
= ( op2 @ ( h @ e10 ) @ ( h @ e10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl203,zip_derived_cl139]) ).
thf(zip_derived_cl1454,plain,
( ( e25
= ( op2 @ e25 @ e25 ) )
<= ( ( h @ e10 )
= e25 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl320,zip_derived_cl1448]) ).
thf(zip_derived_cl148,plain,
( ( op2 @ e25 @ e25 )
= e21 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1467,plain,
( ( e25 = e21 )
<= ( ( h @ e10 )
= e25 ) ),
inference(demod,[status(thm)],[zip_derived_cl1454,zip_derived_cl148]) ).
thf(zip_derived_cl32,plain,
e21 != e25,
inference(cnf,[status(esa)],[ax2]) ).
thf('4',plain,
( ( h @ e10 )
!= e25 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1467,zip_derived_cl32]) ).
thf(zip_derived_cl317,plain,
( ( ( h @ e10 )
= e22 )
<= ( ( h @ e10 )
= e22 ) ),
inference(split,[status(esa)],[zip_derived_cl189]) ).
thf(zip_derived_cl1448_005,plain,
( ( h @ e10 )
= ( op2 @ ( h @ e10 ) @ ( h @ e10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl203,zip_derived_cl139]) ).
thf(zip_derived_cl1451,plain,
( ( e22
= ( op2 @ e22 @ e22 ) )
<= ( ( h @ e10 )
= e22 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl317,zip_derived_cl1448]) ).
thf(zip_derived_cl172,plain,
( ( op2 @ e22 @ e22 )
= e23 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1594,plain,
( ( e22 = e23 )
<= ( ( h @ e10 )
= e22 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1451,zip_derived_cl172]) ).
thf(zip_derived_cl30,plain,
e22 != e23,
inference(cnf,[status(esa)],[ax2]) ).
thf('5',plain,
( ( h @ e10 )
!= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1594,zip_derived_cl30]) ).
thf('6',plain,
( ( ( h @ e10 )
= e24 )
| ( ( h @ e10 )
= e22 )
| ( ( h @ e10 )
= e25 )
| ( ( h @ e10 )
= e26 )
| ( ( h @ e10 )
= e20 )
| ( ( h @ e10 )
= e23 )
| ( ( h @ e10 )
= e21 ) ),
inference(split,[status(esa)],[zip_derived_cl189]) ).
thf('7',plain,
( ( h @ e10 )
= e24 ),
inference('sat_resolution*',[status(thm)],['0','1','2','3','4','5','6']) ).
thf(zip_derived_cl1597,plain,
( ( h @ e10 )
= e24 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl319,'7']) ).
thf(zip_derived_cl190,plain,
( ( ( h @ e11 )
= e20 )
| ( ( h @ e11 )
= e21 )
| ( ( h @ e11 )
= e22 )
| ( ( h @ e11 )
= e23 )
| ( ( h @ e11 )
= e24 )
| ( ( h @ e11 )
= e25 )
| ( ( h @ e11 )
= e26 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl326,plain,
( ( ( h @ e11 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(split,[status(esa)],[zip_derived_cl190]) ).
thf(zip_derived_cl204,plain,
( ( h @ ( op1 @ e10 @ e11 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e11 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl138,plain,
( ( op1 @ e10 @ e11 )
= e13 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl1477,plain,
( ( h @ e13 )
= ( op2 @ ( h @ e10 ) @ ( h @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl204,zip_derived_cl138]) ).
thf(zip_derived_cl1482,plain,
( ( ( h @ e13 )
= ( op2 @ ( h @ e10 ) @ e24 ) )
<= ( ( h @ e11 )
= e24 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl326,zip_derived_cl1477]) ).
thf(zip_derived_cl1666,plain,
( ( ( h @ e13 )
= ( op2 @ e24 @ e24 ) )
<= ( ( h @ e11 )
= e24 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1597,zip_derived_cl1482]) ).
thf(zip_derived_cl156,plain,
( ( op2 @ e24 @ e24 )
= e24 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1682,plain,
( ( ( h @ e13 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl1666,zip_derived_cl156]) ).
thf(zip_derived_cl220,plain,
( ( h @ ( op1 @ e12 @ e13 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e13 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl122,plain,
( ( op1 @ e12 @ e13 )
= e14 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl2128,plain,
( ( h @ e14 )
= ( op2 @ ( h @ e12 ) @ ( h @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl220,zip_derived_cl122]) ).
thf(zip_derived_cl2139,plain,
( ( ( h @ e14 )
= ( op2 @ ( h @ e12 ) @ e24 ) )
<= ( ( h @ e11 )
= e24 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1682,zip_derived_cl2128]) ).
thf(zip_derived_cl217,plain,
( ( h @ ( op1 @ e12 @ e10 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e10 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl125,plain,
( ( op1 @ e12 @ e10 )
= e11 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl1597_006,plain,
( ( h @ e10 )
= e24 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl319,'7']) ).
thf(zip_derived_cl1987,plain,
( ( h @ e11 )
= ( op2 @ ( h @ e12 ) @ e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl217,zip_derived_cl125,zip_derived_cl1597]) ).
thf(zip_derived_cl326_007,plain,
( ( ( h @ e11 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(split,[status(esa)],[zip_derived_cl190]) ).
thf(zip_derived_cl2144,plain,
( ( ( h @ e14 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl2139,zip_derived_cl1987,zip_derived_cl326]) ).
thf(zip_derived_cl193,plain,
( ( ( h @ e14 )
= e20 )
| ( ( h @ e14 )
= e21 )
| ( ( h @ e14 )
= e22 )
| ( ( h @ e14 )
= e23 )
| ( ( h @ e14 )
= e24 )
| ( ( h @ e14 )
= e25 )
| ( ( h @ e14 )
= e26 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl343,plain,
( ( ( h @ e14 )
= e20 )
<= ( ( h @ e14 )
= e20 ) ),
inference(split,[status(esa)],[zip_derived_cl193]) ).
thf(zip_derived_cl2526,plain,
( ( e24 = e20 )
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e14 )
= e20 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2144,zip_derived_cl343]) ).
thf(zip_derived_cl38,plain,
e20 != e24,
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl2536,plain,
( $false
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e14 )
= e20 ) ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2526,zip_derived_cl38]) ).
thf(zip_derived_cl1597_008,plain,
( ( h @ e10 )
= e24 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl319,'7']) ).
thf(zip_derived_cl322,plain,
( ( ( h @ e11 )
= e20 )
<= ( ( h @ e11 )
= e20 ) ),
inference(split,[status(esa)],[zip_derived_cl190]) ).
thf(zip_derived_cl1477_009,plain,
( ( h @ e13 )
= ( op2 @ ( h @ e10 ) @ ( h @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl204,zip_derived_cl138]) ).
thf(zip_derived_cl1478,plain,
( ( ( h @ e13 )
= ( op2 @ ( h @ e10 ) @ e20 ) )
<= ( ( h @ e11 )
= e20 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl322,zip_derived_cl1477]) ).
thf(zip_derived_cl1662,plain,
( ( ( h @ e13 )
= ( op2 @ e24 @ e20 ) )
<= ( ( h @ e11 )
= e20 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1597,zip_derived_cl1478]) ).
thf(zip_derived_cl160,plain,
( ( op2 @ e24 @ e20 )
= e23 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1678,plain,
( ( ( h @ e13 )
= e23 )
<= ( ( h @ e11 )
= e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1662,zip_derived_cl160]) ).
thf(zip_derived_cl227,plain,
( ( h @ ( op1 @ e13 @ e13 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e13 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl115,plain,
( ( op1 @ e13 @ e13 )
= e13 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl2397,plain,
( ( h @ e13 )
= ( op2 @ ( h @ e13 ) @ ( h @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl227,zip_derived_cl115]) ).
thf(zip_derived_cl2405,plain,
( ( e23
= ( op2 @ e23 @ e23 ) )
<= ( ( h @ e11 )
= e20 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1678,zip_derived_cl2397]) ).
thf(zip_derived_cl164_010,plain,
( ( op2 @ e23 @ e23 )
= e20 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl2426,plain,
( ( e23 = e20 )
<= ( ( h @ e11 )
= e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl2405,zip_derived_cl164]) ).
thf(zip_derived_cl39_011,plain,
e20 != e23,
inference(cnf,[status(esa)],[ax2]) ).
thf('8',plain,
( ( h @ e11 )
!= e20 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2426,zip_derived_cl39]) ).
thf(zip_derived_cl325,plain,
( ( ( h @ e11 )
= e23 )
<= ( ( h @ e11 )
= e23 ) ),
inference(split,[status(esa)],[zip_derived_cl190]) ).
thf(zip_derived_cl211,plain,
( ( h @ ( op1 @ e11 @ e11 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e11 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl131,plain,
( ( op1 @ e11 @ e11 )
= e11 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl1707,plain,
( ( h @ e11 )
= ( op2 @ ( h @ e11 ) @ ( h @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl211,zip_derived_cl131]) ).
thf(zip_derived_cl1711,plain,
( ( e23
= ( op2 @ e23 @ e23 ) )
<= ( ( h @ e11 )
= e23 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl325,zip_derived_cl1707]) ).
thf(zip_derived_cl164_012,plain,
( ( op2 @ e23 @ e23 )
= e20 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1724,plain,
( ( e23 = e20 )
<= ( ( h @ e11 )
= e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl1711,zip_derived_cl164]) ).
thf(zip_derived_cl39_013,plain,
e20 != e23,
inference(cnf,[status(esa)],[ax2]) ).
thf('9',plain,
( ( h @ e11 )
!= e23 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1724,zip_derived_cl39]) ).
thf(zip_derived_cl1597_014,plain,
( ( h @ e10 )
= e24 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl319,'7']) ).
thf(zip_derived_cl323,plain,
( ( ( h @ e11 )
= e21 )
<= ( ( h @ e11 )
= e21 ) ),
inference(split,[status(esa)],[zip_derived_cl190]) ).
thf(zip_derived_cl1477_015,plain,
( ( h @ e13 )
= ( op2 @ ( h @ e10 ) @ ( h @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl204,zip_derived_cl138]) ).
thf(zip_derived_cl1479,plain,
( ( ( h @ e13 )
= ( op2 @ ( h @ e10 ) @ e21 ) )
<= ( ( h @ e11 )
= e21 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl323,zip_derived_cl1477]) ).
thf(zip_derived_cl1663,plain,
( ( ( h @ e13 )
= ( op2 @ e24 @ e21 ) )
<= ( ( h @ e11 )
= e21 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1597,zip_derived_cl1479]) ).
thf(zip_derived_cl159,plain,
( ( op2 @ e24 @ e21 )
= e25 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1679,plain,
( ( ( h @ e13 )
= e25 )
<= ( ( h @ e11 )
= e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1663,zip_derived_cl159]) ).
thf(zip_derived_cl2397_016,plain,
( ( h @ e13 )
= ( op2 @ ( h @ e13 ) @ ( h @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl227,zip_derived_cl115]) ).
thf(zip_derived_cl2406,plain,
( ( e25
= ( op2 @ e25 @ e25 ) )
<= ( ( h @ e11 )
= e21 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1679,zip_derived_cl2397]) ).
thf(zip_derived_cl148_017,plain,
( ( op2 @ e25 @ e25 )
= e21 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl2428,plain,
( ( e25 = e21 )
<= ( ( h @ e11 )
= e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl2406,zip_derived_cl148]) ).
thf(zip_derived_cl32_018,plain,
e21 != e25,
inference(cnf,[status(esa)],[ax2]) ).
thf('10',plain,
( ( h @ e11 )
!= e21 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2428,zip_derived_cl32]) ).
thf(zip_derived_cl328,plain,
( ( ( h @ e11 )
= e26 )
<= ( ( h @ e11 )
= e26 ) ),
inference(split,[status(esa)],[zip_derived_cl190]) ).
thf(zip_derived_cl1707_019,plain,
( ( h @ e11 )
= ( op2 @ ( h @ e11 ) @ ( h @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl211,zip_derived_cl131]) ).
thf(zip_derived_cl1714,plain,
( ( e26
= ( op2 @ e26 @ e26 ) )
<= ( ( h @ e11 )
= e26 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl328,zip_derived_cl1707]) ).
thf(zip_derived_cl140_020,plain,
( ( op2 @ e26 @ e26 )
= e25 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1728,plain,
( ( e26 = e25 )
<= ( ( h @ e11 )
= e26 ) ),
inference(demod,[status(thm)],[zip_derived_cl1714,zip_derived_cl140]) ).
thf(zip_derived_cl21_021,plain,
e25 != e26,
inference(cnf,[status(esa)],[ax2]) ).
thf('11',plain,
( ( h @ e11 )
!= e26 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1728,zip_derived_cl21]) ).
thf(zip_derived_cl327,plain,
( ( ( h @ e11 )
= e25 )
<= ( ( h @ e11 )
= e25 ) ),
inference(split,[status(esa)],[zip_derived_cl190]) ).
thf(zip_derived_cl1707_022,plain,
( ( h @ e11 )
= ( op2 @ ( h @ e11 ) @ ( h @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl211,zip_derived_cl131]) ).
thf(zip_derived_cl1713,plain,
( ( e25
= ( op2 @ e25 @ e25 ) )
<= ( ( h @ e11 )
= e25 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl327,zip_derived_cl1707]) ).
thf(zip_derived_cl148_023,plain,
( ( op2 @ e25 @ e25 )
= e21 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1726,plain,
( ( e25 = e21 )
<= ( ( h @ e11 )
= e25 ) ),
inference(demod,[status(thm)],[zip_derived_cl1713,zip_derived_cl148]) ).
thf(zip_derived_cl32_024,plain,
e21 != e25,
inference(cnf,[status(esa)],[ax2]) ).
thf('12',plain,
( ( h @ e11 )
!= e25 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1726,zip_derived_cl32]) ).
thf(zip_derived_cl1597_025,plain,
( ( h @ e10 )
= e24 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl319,'7']) ).
thf(zip_derived_cl324,plain,
( ( ( h @ e11 )
= e22 )
<= ( ( h @ e11 )
= e22 ) ),
inference(split,[status(esa)],[zip_derived_cl190]) ).
thf(zip_derived_cl1477_026,plain,
( ( h @ e13 )
= ( op2 @ ( h @ e10 ) @ ( h @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl204,zip_derived_cl138]) ).
thf(zip_derived_cl1480,plain,
( ( ( h @ e13 )
= ( op2 @ ( h @ e10 ) @ e22 ) )
<= ( ( h @ e11 )
= e22 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl324,zip_derived_cl1477]) ).
thf(zip_derived_cl1664,plain,
( ( ( h @ e13 )
= ( op2 @ e24 @ e22 ) )
<= ( ( h @ e11 )
= e22 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1597,zip_derived_cl1480]) ).
thf(zip_derived_cl158,plain,
( ( op2 @ e24 @ e22 )
= e20 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1680,plain,
( ( ( h @ e13 )
= e20 )
<= ( ( h @ e11 )
= e22 ) ),
inference(demod,[status(thm)],[zip_derived_cl1664,zip_derived_cl158]) ).
thf(zip_derived_cl224,plain,
( ( h @ ( op1 @ e13 @ e10 ) )
= ( op2 @ ( h @ e13 ) @ ( h @ e10 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl118,plain,
( ( op1 @ e13 @ e10 )
= e12 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl1597_027,plain,
( ( h @ e10 )
= e24 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl319,'7']) ).
thf(zip_derived_cl2288,plain,
( ( h @ e12 )
= ( op2 @ ( h @ e13 ) @ e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl224,zip_derived_cl118,zip_derived_cl1597]) ).
thf(zip_derived_cl2298,plain,
( ( ( h @ e12 )
= ( op2 @ e20 @ e24 ) )
<= ( ( h @ e11 )
= e22 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1680,zip_derived_cl2288]) ).
thf(zip_derived_cl184,plain,
( ( op2 @ e20 @ e24 )
= e23 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl2310,plain,
( ( ( h @ e12 )
= e23 )
<= ( ( h @ e11 )
= e22 ) ),
inference(demod,[status(thm)],[zip_derived_cl2298,zip_derived_cl184]) ).
thf(zip_derived_cl219,plain,
( ( h @ ( op1 @ e12 @ e12 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e12 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl123,plain,
( ( op1 @ e12 @ e12 )
= e12 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl2111,plain,
( ( h @ e12 )
= ( op2 @ ( h @ e12 ) @ ( h @ e12 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl219,zip_derived_cl123]) ).
thf(zip_derived_cl2699,plain,
( ( e23
= ( op2 @ e23 @ e23 ) )
<= ( ( h @ e11 )
= e22 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2310,zip_derived_cl2111]) ).
thf(zip_derived_cl164_028,plain,
( ( op2 @ e23 @ e23 )
= e20 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl2714,plain,
( ( e23 = e20 )
<= ( ( h @ e11 )
= e22 ) ),
inference(demod,[status(thm)],[zip_derived_cl2699,zip_derived_cl164]) ).
thf(zip_derived_cl39_029,plain,
e20 != e23,
inference(cnf,[status(esa)],[ax2]) ).
thf('13',plain,
( ( h @ e11 )
!= e22 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2714,zip_derived_cl39]) ).
thf('14',plain,
( ( ( h @ e11 )
= e24 )
| ( ( h @ e11 )
= e22 )
| ( ( h @ e11 )
= e25 )
| ( ( h @ e11 )
= e26 )
| ( ( h @ e11 )
= e21 )
| ( ( h @ e11 )
= e23 )
| ( ( h @ e11 )
= e20 ) ),
inference(split,[status(esa)],[zip_derived_cl190]) ).
thf('15',plain,
( ( h @ e11 )
= e24 ),
inference('sat_resolution*',[status(thm)],['8','9','10','11','12','13','14']) ).
thf(zip_derived_cl196,plain,
( ( ( j @ e20 )
= e10 )
| ( ( j @ e20 )
= e11 )
| ( ( j @ e20 )
= e12 )
| ( ( j @ e20 )
= e13 )
| ( ( j @ e20 )
= e14 )
| ( ( j @ e20 )
= e15 )
| ( ( j @ e20 )
= e16 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl368,plain,
( ( ( j @ e20 )
= e14 )
<= ( ( j @ e20 )
= e14 ) ),
inference(split,[status(esa)],[zip_derived_cl196]) ).
thf(zip_derived_cl301,plain,
( ( h @ ( j @ e20 ) )
= e20 ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl1433,plain,
( ( ( h @ e14 )
= e20 )
<= ( ( j @ e20 )
= e14 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl368,zip_derived_cl301]) ).
thf(zip_derived_cl347,plain,
( ( ( h @ e14 )
= e24 )
<= ( ( h @ e14 )
= e24 ) ),
inference(split,[status(esa)],[zip_derived_cl193]) ).
thf(zip_derived_cl1530,plain,
( ( e20 = e24 )
<= ( ( ( h @ e14 )
= e24 )
& ( ( j @ e20 )
= e14 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1433,zip_derived_cl347]) ).
thf(zip_derived_cl38_030,plain,
e20 != e24,
inference(cnf,[status(esa)],[ax2]) ).
thf('16',plain,
( ( ( h @ e14 )
!= e24 )
| ( ( j @ e20 )
!= e14 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1530,zip_derived_cl38]) ).
thf(zip_derived_cl348,plain,
( ( ( h @ e14 )
= e25 )
<= ( ( h @ e14 )
= e25 ) ),
inference(split,[status(esa)],[zip_derived_cl193]) ).
thf(zip_derived_cl235,plain,
( ( h @ ( op1 @ e14 @ e14 ) )
= ( op2 @ ( h @ e14 ) @ ( h @ e14 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl107,plain,
( ( op1 @ e14 @ e14 )
= e14 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl2726,plain,
( ( h @ e14 )
= ( op2 @ ( h @ e14 ) @ ( h @ e14 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl235,zip_derived_cl107]) ).
thf(zip_derived_cl2743,plain,
( ( e25
= ( op2 @ e25 @ e25 ) )
<= ( ( h @ e14 )
= e25 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl348,zip_derived_cl2726]) ).
thf(zip_derived_cl148_031,plain,
( ( op2 @ e25 @ e25 )
= e21 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl2756,plain,
( ( e25 = e21 )
<= ( ( h @ e14 )
= e25 ) ),
inference(demod,[status(thm)],[zip_derived_cl2743,zip_derived_cl148]) ).
thf(zip_derived_cl32_032,plain,
e21 != e25,
inference(cnf,[status(esa)],[ax2]) ).
thf('17',plain,
( ( h @ e14 )
!= e25 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2756,zip_derived_cl32]) ).
thf(zip_derived_cl346,plain,
( ( ( h @ e14 )
= e23 )
<= ( ( h @ e14 )
= e23 ) ),
inference(split,[status(esa)],[zip_derived_cl193]) ).
thf(zip_derived_cl2726_033,plain,
( ( h @ e14 )
= ( op2 @ ( h @ e14 ) @ ( h @ e14 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl235,zip_derived_cl107]) ).
thf(zip_derived_cl2741,plain,
( ( e23
= ( op2 @ e23 @ e23 ) )
<= ( ( h @ e14 )
= e23 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl346,zip_derived_cl2726]) ).
thf(zip_derived_cl164_034,plain,
( ( op2 @ e23 @ e23 )
= e20 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl2754,plain,
( ( e23 = e20 )
<= ( ( h @ e14 )
= e23 ) ),
inference(demod,[status(thm)],[zip_derived_cl2741,zip_derived_cl164]) ).
thf(zip_derived_cl39_035,plain,
e20 != e23,
inference(cnf,[status(esa)],[ax2]) ).
thf('18',plain,
( ( h @ e14 )
!= e23 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2754,zip_derived_cl39]) ).
thf(zip_derived_cl1433_036,plain,
( ( ( h @ e14 )
= e20 )
<= ( ( j @ e20 )
= e14 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl368,zip_derived_cl301]) ).
thf(zip_derived_cl344,plain,
( ( ( h @ e14 )
= e21 )
<= ( ( h @ e14 )
= e21 ) ),
inference(split,[status(esa)],[zip_derived_cl193]) ).
thf(zip_derived_cl1527,plain,
( ( e20 = e21 )
<= ( ( ( h @ e14 )
= e21 )
& ( ( j @ e20 )
= e14 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1433,zip_derived_cl344]) ).
thf(zip_derived_cl41,plain,
e20 != e21,
inference(cnf,[status(esa)],[ax2]) ).
thf('19',plain,
( ( ( h @ e14 )
!= e21 )
| ( ( j @ e20 )
!= e14 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1527,zip_derived_cl41]) ).
thf(zip_derived_cl349,plain,
( ( ( h @ e14 )
= e26 )
<= ( ( h @ e14 )
= e26 ) ),
inference(split,[status(esa)],[zip_derived_cl193]) ).
thf(zip_derived_cl2726_037,plain,
( ( h @ e14 )
= ( op2 @ ( h @ e14 ) @ ( h @ e14 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl235,zip_derived_cl107]) ).
thf(zip_derived_cl2744,plain,
( ( e26
= ( op2 @ e26 @ e26 ) )
<= ( ( h @ e14 )
= e26 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl349,zip_derived_cl2726]) ).
thf(zip_derived_cl140_038,plain,
( ( op2 @ e26 @ e26 )
= e25 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl2758,plain,
( ( e26 = e25 )
<= ( ( h @ e14 )
= e26 ) ),
inference(demod,[status(thm)],[zip_derived_cl2744,zip_derived_cl140]) ).
thf(zip_derived_cl21_039,plain,
e25 != e26,
inference(cnf,[status(esa)],[ax2]) ).
thf('20',plain,
( ( h @ e14 )
!= e26 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2758,zip_derived_cl21]) ).
thf(zip_derived_cl1597_040,plain,
( ( h @ e10 )
= e24 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl319,'7']) ).
thf(zip_derived_cl365,plain,
( ( ( j @ e20 )
= e11 )
<= ( ( j @ e20 )
= e11 ) ),
inference(split,[status(esa)],[zip_derived_cl196]) ).
thf(zip_derived_cl301_041,plain,
( ( h @ ( j @ e20 ) )
= e20 ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl1430,plain,
( ( ( h @ e11 )
= e20 )
<= ( ( j @ e20 )
= e11 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl365,zip_derived_cl301]) ).
thf(zip_derived_cl1477_042,plain,
( ( h @ e13 )
= ( op2 @ ( h @ e10 ) @ ( h @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl204,zip_derived_cl138]) ).
thf(zip_derived_cl1496,plain,
( ( ( h @ e13 )
= ( op2 @ ( h @ e10 ) @ e20 ) )
<= ( ( j @ e20 )
= e11 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1430,zip_derived_cl1477]) ).
thf(zip_derived_cl1669,plain,
( ( ( h @ e13 )
= ( op2 @ e24 @ e20 ) )
<= ( ( j @ e20 )
= e11 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1597,zip_derived_cl1496]) ).
thf(zip_derived_cl160_043,plain,
( ( op2 @ e24 @ e20 )
= e23 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1685,plain,
( ( ( h @ e13 )
= e23 )
<= ( ( j @ e20 )
= e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl1669,zip_derived_cl160]) ).
thf(zip_derived_cl2397_044,plain,
( ( h @ e13 )
= ( op2 @ ( h @ e13 ) @ ( h @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl227,zip_derived_cl115]) ).
thf(zip_derived_cl2409,plain,
( ( e23
= ( op2 @ e23 @ e23 ) )
<= ( ( j @ e20 )
= e11 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1685,zip_derived_cl2397]) ).
thf(zip_derived_cl164_045,plain,
( ( op2 @ e23 @ e23 )
= e20 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl2430,plain,
( ( e23 = e20 )
<= ( ( j @ e20 )
= e11 ) ),
inference(demod,[status(thm)],[zip_derived_cl2409,zip_derived_cl164]) ).
thf(zip_derived_cl39_046,plain,
e20 != e23,
inference(cnf,[status(esa)],[ax2]) ).
thf('21',plain,
( ( j @ e20 )
!= e11 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2430,zip_derived_cl39]) ).
thf(zip_derived_cl1682_047,plain,
( ( ( h @ e13 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl1666,zip_derived_cl156]) ).
thf(zip_derived_cl213,plain,
( ( h @ ( op1 @ e11 @ e13 ) )
= ( op2 @ ( h @ e11 ) @ ( h @ e13 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl129,plain,
( ( op1 @ e11 @ e13 )
= e15 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl1802,plain,
( ( h @ e15 )
= ( op2 @ ( h @ e11 ) @ ( h @ e13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl213,zip_derived_cl129]) ).
thf(zip_derived_cl1858,plain,
( ( ( h @ e15 )
= ( op2 @ ( h @ e11 ) @ e24 ) )
<= ( ( h @ e11 )
= e24 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1682,zip_derived_cl1802]) ).
thf(zip_derived_cl326_048,plain,
( ( ( h @ e11 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(split,[status(esa)],[zip_derived_cl190]) ).
thf(zip_derived_cl156_049,plain,
( ( op2 @ e24 @ e24 )
= e24 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1871,plain,
( ( ( h @ e15 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl1858,zip_derived_cl326,zip_derived_cl156]) ).
thf(zip_derived_cl369,plain,
( ( ( j @ e20 )
= e15 )
<= ( ( j @ e20 )
= e15 ) ),
inference(split,[status(esa)],[zip_derived_cl196]) ).
thf(zip_derived_cl301_050,plain,
( ( h @ ( j @ e20 ) )
= e20 ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl1434,plain,
( ( ( h @ e15 )
= e20 )
<= ( ( j @ e20 )
= e15 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl369,zip_derived_cl301]) ).
thf(zip_derived_cl2235,plain,
( ( e24 = e20 )
<= ( ( ( h @ e11 )
= e24 )
& ( ( j @ e20 )
= e15 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1871,zip_derived_cl1434]) ).
thf(zip_derived_cl38_051,plain,
e20 != e24,
inference(cnf,[status(esa)],[ax2]) ).
thf('22',plain,
( ( ( j @ e20 )
!= e15 )
| ( ( h @ e11 )
!= e24 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2235,zip_derived_cl38]) ).
thf(zip_derived_cl192,plain,
( ( ( h @ e13 )
= e20 )
| ( ( h @ e13 )
= e21 )
| ( ( h @ e13 )
= e22 )
| ( ( h @ e13 )
= e23 )
| ( ( h @ e13 )
= e24 )
| ( ( h @ e13 )
= e25 )
| ( ( h @ e13 )
= e26 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl336,plain,
( ( ( h @ e13 )
= e20 )
<= ( ( h @ e13 )
= e20 ) ),
inference(split,[status(esa)],[zip_derived_cl192]) ).
thf(zip_derived_cl2288_052,plain,
( ( h @ e12 )
= ( op2 @ ( h @ e13 ) @ e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl224,zip_derived_cl118,zip_derived_cl1597]) ).
thf(zip_derived_cl2289,plain,
( ( ( h @ e12 )
= ( op2 @ e20 @ e24 ) )
<= ( ( h @ e13 )
= e20 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl336,zip_derived_cl2288]) ).
thf(zip_derived_cl184_053,plain,
( ( op2 @ e20 @ e24 )
= e23 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl2301,plain,
( ( ( h @ e12 )
= e23 )
<= ( ( h @ e13 )
= e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl2289,zip_derived_cl184]) ).
thf(zip_derived_cl2111_054,plain,
( ( h @ e12 )
= ( op2 @ ( h @ e12 ) @ ( h @ e12 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl219,zip_derived_cl123]) ).
thf(zip_derived_cl2570,plain,
( ( e23
= ( op2 @ e23 @ e23 ) )
<= ( ( h @ e13 )
= e20 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2301,zip_derived_cl2111]) ).
thf(zip_derived_cl164_055,plain,
( ( op2 @ e23 @ e23 )
= e20 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl2580,plain,
( ( e23 = e20 )
<= ( ( h @ e13 )
= e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl2570,zip_derived_cl164]) ).
thf(zip_derived_cl39_056,plain,
e20 != e23,
inference(cnf,[status(esa)],[ax2]) ).
thf('23',plain,
( ( h @ e13 )
!= e20 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2580,zip_derived_cl39]) ).
thf(zip_derived_cl367,plain,
( ( ( j @ e20 )
= e13 )
<= ( ( j @ e20 )
= e13 ) ),
inference(split,[status(esa)],[zip_derived_cl196]) ).
thf(zip_derived_cl301_057,plain,
( ( h @ ( j @ e20 ) )
= e20 ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl1432,plain,
( ( ( h @ e13 )
= e20 )
<= ( ( j @ e20 )
= e13 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl367,zip_derived_cl301]) ).
thf(zip_derived_cl342,plain,
( ( ( h @ e13 )
= e26 )
<= ( ( h @ e13 )
= e26 ) ),
inference(split,[status(esa)],[zip_derived_cl192]) ).
thf(zip_derived_cl1520,plain,
( ( e20 = e26 )
<= ( ( ( h @ e13 )
= e26 )
& ( ( j @ e20 )
= e13 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1432,zip_derived_cl342]) ).
thf(zip_derived_cl36,plain,
e20 != e26,
inference(cnf,[status(esa)],[ax2]) ).
thf('24',plain,
( ( ( j @ e20 )
!= e13 )
| ( ( h @ e13 )
!= e26 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1520,zip_derived_cl36]) ).
thf(zip_derived_cl1432_058,plain,
( ( ( h @ e13 )
= e20 )
<= ( ( j @ e20 )
= e13 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl367,zip_derived_cl301]) ).
thf(zip_derived_cl341,plain,
( ( ( h @ e13 )
= e25 )
<= ( ( h @ e13 )
= e25 ) ),
inference(split,[status(esa)],[zip_derived_cl192]) ).
thf(zip_derived_cl1519,plain,
( ( e20 = e25 )
<= ( ( ( h @ e13 )
= e25 )
& ( ( j @ e20 )
= e13 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1432,zip_derived_cl341]) ).
thf(zip_derived_cl37,plain,
e20 != e25,
inference(cnf,[status(esa)],[ax2]) ).
thf('25',plain,
( ( ( h @ e13 )
!= e25 )
| ( ( j @ e20 )
!= e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1519,zip_derived_cl37]) ).
thf(zip_derived_cl1432_059,plain,
( ( ( h @ e13 )
= e20 )
<= ( ( j @ e20 )
= e13 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl367,zip_derived_cl301]) ).
thf(zip_derived_cl340,plain,
( ( ( h @ e13 )
= e24 )
<= ( ( h @ e13 )
= e24 ) ),
inference(split,[status(esa)],[zip_derived_cl192]) ).
thf(zip_derived_cl1518,plain,
( ( e20 = e24 )
<= ( ( ( h @ e13 )
= e24 )
& ( ( j @ e20 )
= e13 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1432,zip_derived_cl340]) ).
thf(zip_derived_cl38_060,plain,
e20 != e24,
inference(cnf,[status(esa)],[ax2]) ).
thf('26',plain,
( ( ( j @ e20 )
!= e13 )
| ( ( h @ e13 )
!= e24 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1518,zip_derived_cl38]) ).
thf(zip_derived_cl1432_061,plain,
( ( ( h @ e13 )
= e20 )
<= ( ( j @ e20 )
= e13 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl367,zip_derived_cl301]) ).
thf(zip_derived_cl339,plain,
( ( ( h @ e13 )
= e23 )
<= ( ( h @ e13 )
= e23 ) ),
inference(split,[status(esa)],[zip_derived_cl192]) ).
thf(zip_derived_cl1517,plain,
( ( e20 = e23 )
<= ( ( ( h @ e13 )
= e23 )
& ( ( j @ e20 )
= e13 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1432,zip_derived_cl339]) ).
thf(zip_derived_cl39_062,plain,
e20 != e23,
inference(cnf,[status(esa)],[ax2]) ).
thf('27',plain,
( ( ( h @ e13 )
!= e23 )
| ( ( j @ e20 )
!= e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1517,zip_derived_cl39]) ).
thf(zip_derived_cl1432_063,plain,
( ( ( h @ e13 )
= e20 )
<= ( ( j @ e20 )
= e13 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl367,zip_derived_cl301]) ).
thf(zip_derived_cl338,plain,
( ( ( h @ e13 )
= e22 )
<= ( ( h @ e13 )
= e22 ) ),
inference(split,[status(esa)],[zip_derived_cl192]) ).
thf(zip_derived_cl1516,plain,
( ( e20 = e22 )
<= ( ( ( h @ e13 )
= e22 )
& ( ( j @ e20 )
= e13 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1432,zip_derived_cl338]) ).
thf(zip_derived_cl40_064,plain,
e20 != e22,
inference(cnf,[status(esa)],[ax2]) ).
thf('28',plain,
( ( ( h @ e13 )
!= e22 )
| ( ( j @ e20 )
!= e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1516,zip_derived_cl40]) ).
thf(zip_derived_cl1432_065,plain,
( ( ( h @ e13 )
= e20 )
<= ( ( j @ e20 )
= e13 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl367,zip_derived_cl301]) ).
thf(zip_derived_cl337,plain,
( ( ( h @ e13 )
= e21 )
<= ( ( h @ e13 )
= e21 ) ),
inference(split,[status(esa)],[zip_derived_cl192]) ).
thf(zip_derived_cl1515,plain,
( ( e20 = e21 )
<= ( ( ( h @ e13 )
= e21 )
& ( ( j @ e20 )
= e13 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1432,zip_derived_cl337]) ).
thf(zip_derived_cl41_066,plain,
e20 != e21,
inference(cnf,[status(esa)],[ax2]) ).
thf('29',plain,
( ( ( h @ e13 )
!= e21 )
| ( ( j @ e20 )
!= e13 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1515,zip_derived_cl41]) ).
thf('30',plain,
( ( ( h @ e13 )
= e24 )
| ( ( h @ e13 )
= e22 )
| ( ( h @ e13 )
= e26 )
| ( ( h @ e13 )
= e20 )
| ( ( h @ e13 )
= e21 )
| ( ( h @ e13 )
= e23 )
| ( ( h @ e13 )
= e25 ) ),
inference(split,[status(esa)],[zip_derived_cl192]) ).
thf(zip_derived_cl1597_067,plain,
( ( h @ e10 )
= e24 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl319,'7']) ).
thf(zip_derived_cl191,plain,
( ( ( h @ e12 )
= e20 )
| ( ( h @ e12 )
= e21 )
| ( ( h @ e12 )
= e22 )
| ( ( h @ e12 )
= e23 )
| ( ( h @ e12 )
= e24 )
| ( ( h @ e12 )
= e25 )
| ( ( h @ e12 )
= e26 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl329,plain,
( ( ( h @ e12 )
= e20 )
<= ( ( h @ e12 )
= e20 ) ),
inference(split,[status(esa)],[zip_derived_cl191]) ).
thf(zip_derived_cl205,plain,
( ( h @ ( op1 @ e10 @ e12 ) )
= ( op2 @ ( h @ e10 ) @ ( h @ e12 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl137,plain,
( ( op1 @ e10 @ e12 )
= e11 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl1551,plain,
( ( h @ e11 )
= ( op2 @ ( h @ e10 ) @ ( h @ e12 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl205,zip_derived_cl137]) ).
thf(zip_derived_cl1552,plain,
( ( ( h @ e11 )
= ( op2 @ ( h @ e10 ) @ e20 ) )
<= ( ( h @ e12 )
= e20 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl329,zip_derived_cl1551]) ).
thf(zip_derived_cl1670,plain,
( ( ( h @ e11 )
= ( op2 @ e24 @ e20 ) )
<= ( ( h @ e12 )
= e20 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1597,zip_derived_cl1552]) ).
thf(zip_derived_cl160_068,plain,
( ( op2 @ e24 @ e20 )
= e23 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1686,plain,
( ( ( h @ e11 )
= e23 )
<= ( ( h @ e12 )
= e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1670,zip_derived_cl160]) ).
thf(zip_derived_cl1707_069,plain,
( ( h @ e11 )
= ( op2 @ ( h @ e11 ) @ ( h @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl211,zip_derived_cl131]) ).
thf(zip_derived_cl1932,plain,
( ( e23
= ( op2 @ e23 @ e23 ) )
<= ( ( h @ e12 )
= e20 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1686,zip_derived_cl1707]) ).
thf(zip_derived_cl164_070,plain,
( ( op2 @ e23 @ e23 )
= e20 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1943,plain,
( ( e23 = e20 )
<= ( ( h @ e12 )
= e20 ) ),
inference(demod,[status(thm)],[zip_derived_cl1932,zip_derived_cl164]) ).
thf(zip_derived_cl39_071,plain,
e20 != e23,
inference(cnf,[status(esa)],[ax2]) ).
thf('31',plain,
( ( h @ e12 )
!= e20 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1943,zip_derived_cl39]) ).
thf(zip_derived_cl1597_072,plain,
( ( h @ e10 )
= e24 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl319,'7']) ).
thf(zip_derived_cl330,plain,
( ( ( h @ e12 )
= e21 )
<= ( ( h @ e12 )
= e21 ) ),
inference(split,[status(esa)],[zip_derived_cl191]) ).
thf(zip_derived_cl1551_073,plain,
( ( h @ e11 )
= ( op2 @ ( h @ e10 ) @ ( h @ e12 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl205,zip_derived_cl137]) ).
thf(zip_derived_cl1553,plain,
( ( ( h @ e11 )
= ( op2 @ ( h @ e10 ) @ e21 ) )
<= ( ( h @ e12 )
= e21 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl1551]) ).
thf(zip_derived_cl1671,plain,
( ( ( h @ e11 )
= ( op2 @ e24 @ e21 ) )
<= ( ( h @ e12 )
= e21 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1597,zip_derived_cl1553]) ).
thf(zip_derived_cl159_074,plain,
( ( op2 @ e24 @ e21 )
= e25 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1687,plain,
( ( ( h @ e11 )
= e25 )
<= ( ( h @ e12 )
= e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1671,zip_derived_cl159]) ).
thf(zip_derived_cl1707_075,plain,
( ( h @ e11 )
= ( op2 @ ( h @ e11 ) @ ( h @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl211,zip_derived_cl131]) ).
thf(zip_derived_cl1969,plain,
( ( e25
= ( op2 @ e25 @ e25 ) )
<= ( ( h @ e12 )
= e21 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1687,zip_derived_cl1707]) ).
thf(zip_derived_cl148_076,plain,
( ( op2 @ e25 @ e25 )
= e21 ),
inference(cnf,[status(esa)],[ax5]) ).
thf(zip_derived_cl1981,plain,
( ( e25 = e21 )
<= ( ( h @ e12 )
= e21 ) ),
inference(demod,[status(thm)],[zip_derived_cl1969,zip_derived_cl148]) ).
thf(zip_derived_cl32_077,plain,
e21 != e25,
inference(cnf,[status(esa)],[ax2]) ).
thf('32',plain,
( ( h @ e12 )
!= e21 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1981,zip_derived_cl32]) ).
thf(zip_derived_cl366,plain,
( ( ( j @ e20 )
= e12 )
<= ( ( j @ e20 )
= e12 ) ),
inference(split,[status(esa)],[zip_derived_cl196]) ).
thf(zip_derived_cl301_078,plain,
( ( h @ ( j @ e20 ) )
= e20 ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl1431,plain,
( ( ( h @ e12 )
= e20 )
<= ( ( j @ e20 )
= e12 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl366,zip_derived_cl301]) ).
thf(zip_derived_cl335,plain,
( ( ( h @ e12 )
= e26 )
<= ( ( h @ e12 )
= e26 ) ),
inference(split,[status(esa)],[zip_derived_cl191]) ).
thf(zip_derived_cl1508,plain,
( ( e20 = e26 )
<= ( ( ( h @ e12 )
= e26 )
& ( ( j @ e20 )
= e12 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1431,zip_derived_cl335]) ).
thf(zip_derived_cl36_079,plain,
e20 != e26,
inference(cnf,[status(esa)],[ax2]) ).
thf('33',plain,
( ( ( j @ e20 )
!= e12 )
| ( ( h @ e12 )
!= e26 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1508,zip_derived_cl36]) ).
thf(zip_derived_cl1431_080,plain,
( ( ( h @ e12 )
= e20 )
<= ( ( j @ e20 )
= e12 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl366,zip_derived_cl301]) ).
thf(zip_derived_cl334,plain,
( ( ( h @ e12 )
= e25 )
<= ( ( h @ e12 )
= e25 ) ),
inference(split,[status(esa)],[zip_derived_cl191]) ).
thf(zip_derived_cl1507,plain,
( ( e20 = e25 )
<= ( ( ( h @ e12 )
= e25 )
& ( ( j @ e20 )
= e12 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1431,zip_derived_cl334]) ).
thf(zip_derived_cl37_081,plain,
e20 != e25,
inference(cnf,[status(esa)],[ax2]) ).
thf('34',plain,
( ( ( h @ e12 )
!= e25 )
| ( ( j @ e20 )
!= e12 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1507,zip_derived_cl37]) ).
thf(zip_derived_cl1431_082,plain,
( ( ( h @ e12 )
= e20 )
<= ( ( j @ e20 )
= e12 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl366,zip_derived_cl301]) ).
thf(zip_derived_cl333,plain,
( ( ( h @ e12 )
= e24 )
<= ( ( h @ e12 )
= e24 ) ),
inference(split,[status(esa)],[zip_derived_cl191]) ).
thf(zip_derived_cl1506,plain,
( ( e20 = e24 )
<= ( ( ( h @ e12 )
= e24 )
& ( ( j @ e20 )
= e12 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1431,zip_derived_cl333]) ).
thf(zip_derived_cl38_083,plain,
e20 != e24,
inference(cnf,[status(esa)],[ax2]) ).
thf('35',plain,
( ( ( j @ e20 )
!= e12 )
| ( ( h @ e12 )
!= e24 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1506,zip_derived_cl38]) ).
thf(zip_derived_cl1431_084,plain,
( ( ( h @ e12 )
= e20 )
<= ( ( j @ e20 )
= e12 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl366,zip_derived_cl301]) ).
thf(zip_derived_cl332,plain,
( ( ( h @ e12 )
= e23 )
<= ( ( h @ e12 )
= e23 ) ),
inference(split,[status(esa)],[zip_derived_cl191]) ).
thf(zip_derived_cl1505,plain,
( ( e20 = e23 )
<= ( ( ( h @ e12 )
= e23 )
& ( ( j @ e20 )
= e12 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1431,zip_derived_cl332]) ).
thf(zip_derived_cl39_085,plain,
e20 != e23,
inference(cnf,[status(esa)],[ax2]) ).
thf('36',plain,
( ( ( h @ e12 )
!= e23 )
| ( ( j @ e20 )
!= e12 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1505,zip_derived_cl39]) ).
thf(zip_derived_cl1431_086,plain,
( ( ( h @ e12 )
= e20 )
<= ( ( j @ e20 )
= e12 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl366,zip_derived_cl301]) ).
thf(zip_derived_cl331,plain,
( ( ( h @ e12 )
= e22 )
<= ( ( h @ e12 )
= e22 ) ),
inference(split,[status(esa)],[zip_derived_cl191]) ).
thf(zip_derived_cl1504,plain,
( ( e20 = e22 )
<= ( ( ( h @ e12 )
= e22 )
& ( ( j @ e20 )
= e12 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1431,zip_derived_cl331]) ).
thf(zip_derived_cl40_087,plain,
e20 != e22,
inference(cnf,[status(esa)],[ax2]) ).
thf('37',plain,
( ( ( j @ e20 )
!= e12 )
| ( ( h @ e12 )
!= e22 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1504,zip_derived_cl40]) ).
thf('38',plain,
( ( ( h @ e12 )
= e24 )
| ( ( h @ e12 )
= e22 )
| ( ( h @ e12 )
= e20 )
| ( ( h @ e12 )
= e21 )
| ( ( h @ e12 )
= e25 )
| ( ( h @ e12 )
= e23 )
| ( ( h @ e12 )
= e26 ) ),
inference(split,[status(esa)],[zip_derived_cl191]) ).
thf(zip_derived_cl364,plain,
( ( ( j @ e20 )
= e10 )
<= ( ( j @ e20 )
= e10 ) ),
inference(split,[status(esa)],[zip_derived_cl196]) ).
thf(zip_derived_cl301_088,plain,
( ( h @ ( j @ e20 ) )
= e20 ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl1429,plain,
( ( ( h @ e10 )
= e20 )
<= ( ( j @ e20 )
= e10 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl364,zip_derived_cl301]) ).
thf(zip_derived_cl319_089,plain,
( ( ( h @ e10 )
= e24 )
<= ( ( h @ e10 )
= e24 ) ),
inference(split,[status(esa)],[zip_derived_cl189]) ).
thf(zip_derived_cl1439,plain,
( ( e20 = e24 )
<= ( ( ( h @ e10 )
= e24 )
& ( ( j @ e20 )
= e10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1429,zip_derived_cl319]) ).
thf(zip_derived_cl38_090,plain,
e20 != e24,
inference(cnf,[status(esa)],[ax2]) ).
thf('39',plain,
( ( ( j @ e20 )
!= e10 )
| ( ( h @ e10 )
!= e24 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1439,zip_derived_cl38]) ).
thf(zip_derived_cl326_091,plain,
( ( ( h @ e11 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(split,[status(esa)],[zip_derived_cl190]) ).
thf(zip_derived_cl218,plain,
( ( h @ ( op1 @ e12 @ e11 ) )
= ( op2 @ ( h @ e12 ) @ ( h @ e11 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl124,plain,
( ( op1 @ e12 @ e11 )
= e16 ),
inference(cnf,[status(esa)],[ax4]) ).
thf(zip_derived_cl2036,plain,
( ( h @ e16 )
= ( op2 @ ( h @ e12 ) @ ( h @ e11 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl218,zip_derived_cl124]) ).
thf(zip_derived_cl2041,plain,
( ( ( h @ e16 )
= ( op2 @ ( h @ e12 ) @ e24 ) )
<= ( ( h @ e11 )
= e24 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl326,zip_derived_cl2036]) ).
thf(zip_derived_cl1987_092,plain,
( ( h @ e11 )
= ( op2 @ ( h @ e12 ) @ e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl217,zip_derived_cl125,zip_derived_cl1597]) ).
thf(zip_derived_cl326_093,plain,
( ( ( h @ e11 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(split,[status(esa)],[zip_derived_cl190]) ).
thf(zip_derived_cl2050,plain,
( ( ( h @ e16 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl2041,zip_derived_cl1987,zip_derived_cl326]) ).
thf(zip_derived_cl195,plain,
( ( ( h @ e16 )
= e20 )
| ( ( h @ e16 )
= e21 )
| ( ( h @ e16 )
= e22 )
| ( ( h @ e16 )
= e23 )
| ( ( h @ e16 )
= e24 )
| ( ( h @ e16 )
= e25 )
| ( ( h @ e16 )
= e26 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl362,plain,
( ( ( h @ e16 )
= e25 )
<= ( ( h @ e16 )
= e25 ) ),
inference(split,[status(esa)],[zip_derived_cl195]) ).
thf(zip_derived_cl2382,plain,
( ( e24 = e25 )
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e16 )
= e25 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2050,zip_derived_cl362]) ).
thf(zip_derived_cl23,plain,
e24 != e25,
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl2392,plain,
( $false
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e16 )
= e25 ) ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2382,zip_derived_cl23]) ).
thf('40',plain,
( ( h @ e11 )
= e24 ),
inference('sat_resolution*',[status(thm)],['8','9','10','11','12','13','14']) ).
thf('41',plain,
( ( h @ e16 )
!= e25 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl2392,'40']) ).
thf(zip_derived_cl2050_094,plain,
( ( ( h @ e16 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl2041,zip_derived_cl1987,zip_derived_cl326]) ).
thf(zip_derived_cl358,plain,
( ( ( h @ e16 )
= e21 )
<= ( ( h @ e16 )
= e21 ) ),
inference(split,[status(esa)],[zip_derived_cl195]) ).
thf(zip_derived_cl2379,plain,
( ( e24 = e21 )
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e16 )
= e21 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2050,zip_derived_cl358]) ).
thf(zip_derived_cl33,plain,
e21 != e24,
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl2389,plain,
( $false
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e16 )
= e21 ) ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2379,zip_derived_cl33]) ).
thf('42',plain,
( ( h @ e11 )
= e24 ),
inference('sat_resolution*',[status(thm)],['8','9','10','11','12','13','14']) ).
thf('43',plain,
( ( h @ e16 )
!= e21 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl2389,'42']) ).
thf(zip_derived_cl2050_095,plain,
( ( ( h @ e16 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl2041,zip_derived_cl1987,zip_derived_cl326]) ).
thf(zip_derived_cl360,plain,
( ( ( h @ e16 )
= e23 )
<= ( ( h @ e16 )
= e23 ) ),
inference(split,[status(esa)],[zip_derived_cl195]) ).
thf(zip_derived_cl2381,plain,
( ( e24 = e23 )
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e16 )
= e23 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2050,zip_derived_cl360]) ).
thf(zip_derived_cl26,plain,
e23 != e24,
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl2391,plain,
( $false
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e16 )
= e23 ) ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2381,zip_derived_cl26]) ).
thf('44',plain,
( ( h @ e11 )
= e24 ),
inference('sat_resolution*',[status(thm)],['8','9','10','11','12','13','14']) ).
thf('45',plain,
( ( h @ e16 )
!= e23 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl2391,'44']) ).
thf(zip_derived_cl2050_096,plain,
( ( ( h @ e16 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl2041,zip_derived_cl1987,zip_derived_cl326]) ).
thf(zip_derived_cl359,plain,
( ( ( h @ e16 )
= e22 )
<= ( ( h @ e16 )
= e22 ) ),
inference(split,[status(esa)],[zip_derived_cl195]) ).
thf(zip_derived_cl2380,plain,
( ( e24 = e22 )
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e16 )
= e22 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2050,zip_derived_cl359]) ).
thf(zip_derived_cl29,plain,
e22 != e24,
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl2390,plain,
( $false
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e16 )
= e22 ) ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2380,zip_derived_cl29]) ).
thf('46',plain,
( ( h @ e11 )
= e24 ),
inference('sat_resolution*',[status(thm)],['8','9','10','11','12','13','14']) ).
thf('47',plain,
( ( h @ e16 )
!= e22 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl2390,'46']) ).
thf(zip_derived_cl2050_097,plain,
( ( ( h @ e16 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl2041,zip_derived_cl1987,zip_derived_cl326]) ).
thf(zip_derived_cl357,plain,
( ( ( h @ e16 )
= e20 )
<= ( ( h @ e16 )
= e20 ) ),
inference(split,[status(esa)],[zip_derived_cl195]) ).
thf(zip_derived_cl2378,plain,
( ( e24 = e20 )
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e16 )
= e20 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2050,zip_derived_cl357]) ).
thf(zip_derived_cl38_098,plain,
e20 != e24,
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl2388,plain,
( $false
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e16 )
= e20 ) ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2378,zip_derived_cl38]) ).
thf('48',plain,
( ( h @ e11 )
= e24 ),
inference('sat_resolution*',[status(thm)],['8','9','10','11','12','13','14']) ).
thf('49',plain,
( ( h @ e16 )
!= e20 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl2388,'48']) ).
thf(zip_derived_cl2050_099,plain,
( ( ( h @ e16 )
= e24 )
<= ( ( h @ e11 )
= e24 ) ),
inference(demod,[status(thm)],[zip_derived_cl2041,zip_derived_cl1987,zip_derived_cl326]) ).
thf(zip_derived_cl363,plain,
( ( ( h @ e16 )
= e26 )
<= ( ( h @ e16 )
= e26 ) ),
inference(split,[status(esa)],[zip_derived_cl195]) ).
thf(zip_derived_cl2383,plain,
( ( e24 = e26 )
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e16 )
= e26 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2050,zip_derived_cl363]) ).
thf(zip_derived_cl22,plain,
e24 != e26,
inference(cnf,[status(esa)],[ax2]) ).
thf(zip_derived_cl2393,plain,
( $false
<= ( ( ( h @ e11 )
= e24 )
& ( ( h @ e16 )
= e26 ) ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl2383,zip_derived_cl22]) ).
thf('50',plain,
( ( h @ e11 )
= e24 ),
inference('sat_resolution*',[status(thm)],['8','9','10','11','12','13','14']) ).
thf('51',plain,
( ( h @ e16 )
!= e26 ),
inference(simpl_trail,[status(thm)],[zip_derived_cl2393,'50']) ).
thf('52',plain,
( ( ( h @ e16 )
= e24 )
| ( ( h @ e16 )
= e26 )
| ( ( h @ e16 )
= e20 )
| ( ( h @ e16 )
= e22 )
| ( ( h @ e16 )
= e23 )
| ( ( h @ e16 )
= e21 )
| ( ( h @ e16 )
= e25 ) ),
inference(split,[status(esa)],[zip_derived_cl195]) ).
thf(zip_derived_cl370,plain,
( ( ( j @ e20 )
= e16 )
<= ( ( j @ e20 )
= e16 ) ),
inference(split,[status(esa)],[zip_derived_cl196]) ).
thf(zip_derived_cl301_100,plain,
( ( h @ ( j @ e20 ) )
= e20 ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl1435,plain,
( ( ( h @ e16 )
= e20 )
<= ( ( j @ e20 )
= e16 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl370,zip_derived_cl301]) ).
thf(zip_derived_cl361,plain,
( ( ( h @ e16 )
= e24 )
<= ( ( h @ e16 )
= e24 ) ),
inference(split,[status(esa)],[zip_derived_cl195]) ).
thf(zip_derived_cl1568,plain,
( ( e20 = e24 )
<= ( ( ( h @ e16 )
= e24 )
& ( ( j @ e20 )
= e16 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1435,zip_derived_cl361]) ).
thf(zip_derived_cl38_101,plain,
e20 != e24,
inference(cnf,[status(esa)],[ax2]) ).
thf('53',plain,
( ( ( j @ e20 )
!= e16 )
| ( ( h @ e16 )
!= e24 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1568,zip_derived_cl38]) ).
thf('54',plain,
( ( ( j @ e20 )
= e14 )
| ( ( j @ e20 )
= e16 )
| ( ( j @ e20 )
= e10 )
| ( ( j @ e20 )
= e12 )
| ( ( j @ e20 )
= e13 )
| ( ( j @ e20 )
= e15 )
| ( ( j @ e20 )
= e11 ) ),
inference(split,[status(esa)],[zip_derived_cl196]) ).
thf(zip_derived_cl1433_102,plain,
( ( ( h @ e14 )
= e20 )
<= ( ( j @ e20 )
= e14 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl368,zip_derived_cl301]) ).
thf(zip_derived_cl345,plain,
( ( ( h @ e14 )
= e22 )
<= ( ( h @ e14 )
= e22 ) ),
inference(split,[status(esa)],[zip_derived_cl193]) ).
thf(zip_derived_cl1528,plain,
( ( e20 = e22 )
<= ( ( ( h @ e14 )
= e22 )
& ( ( j @ e20 )
= e14 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1433,zip_derived_cl345]) ).
thf(zip_derived_cl40_103,plain,
e20 != e22,
inference(cnf,[status(esa)],[ax2]) ).
thf('55',plain,
( ( ( h @ e14 )
!= e22 )
| ( ( j @ e20 )
!= e14 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1528,zip_derived_cl40]) ).
thf('56',plain,
( ( ( h @ e14 )
= e20 )
| ( ( h @ e14 )
= e22 )
| ( ( h @ e14 )
= e26 )
| ( ( h @ e14 )
= e21 )
| ( ( h @ e14 )
= e23 )
| ( ( h @ e14 )
= e25 )
| ( ( h @ e14 )
= e24 ) ),
inference(split,[status(esa)],[zip_derived_cl193]) ).
thf('57',plain,
( ( h @ e14 )
= e20 ),
inference('sat_resolution*',[status(thm)],['16','17','18','19','20','21','8','9','10','11','12','13','14','22','23','24','25','26','27','28','29','30','31','32','33','34','35','36','37','38','0','1','2','3','4','5','6','39','41','43','45','47','49','51','52','53','54','55','56']) ).
thf(zip_derived_cl2810,plain,
$false,
inference(simpl_trail,[status(thm)],[zip_derived_cl2536,'15','57']) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : ALG206+1 : TPTP v9.2.0. Released v2.7.0.
% 0.10/0.11 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.DZsW5sjX61 true
% 0.11/0.32 % Computer : n001.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Wed Oct 1 16:59:08 EDT 2025
% 0.11/0.32 % CPUTime :
% 0.11/0.32 % Running portfolio for 300 s
% 0.11/0.32 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.32 % Number of cores: 8
% 0.11/0.32 % Python version: Python 3.6.8
% 0.11/0.33 % Running in FO mode
% 0.52/0.60 % Total configuration time : 435
% 0.52/0.60 % Estimated wc time : 1092
% 0.52/0.60 % Estimated cpu time (7 cpus) : 156.0
% 0.61/0.70 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.61/0.71 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.61/0.71 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.61/0.71 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.61/0.71 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.85/0.71 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.85/0.72 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.85/1.16 % Solved by fo/fo1_av.sh.
% 0.85/1.16 % done 1148 iterations in 0.394s
% 0.85/1.16 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.85/1.16 % SZS output start Refutation
% See solution above
% 0.85/1.16
% 0.85/1.16
% 0.85/1.16 % Terminating...
% 4.40/1.23 % Runner terminated.
% 4.40/1.26 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------