%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SYO228^5 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.rD0grtqTOB true
% Computer : n016.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 05:07:03 PM UTC 2025
% Result : Theorem 1.13s 1.10s
% Output : Refutation 1.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 76
% Number of leaves : 1
% Syntax : Number of formulae : 486 ( 56 unt; 0 typ; 0 def)
% Number of atoms : 1496 ( 152 equ; 0 cnn)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 5120 ( 710 ~;1006 |; 42 &;3336 @)
% ( 0 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 6 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 22 ( 22 >; 0 *; 0 +; 0 <<)
% Number of symbols : 17 ( 15 usr; 8 con; 0-2 aty)
% Number of variables : 216 ( 0 ^; 216 !; 0 ?; 216 :)
% Comments :
%------------------------------------------------------------------------------
thf(g_type,type,
g: $tType ).
thf(b_type,type,
b: $tType ).
thf(a_type,type,
a: $tType ).
thf(sk__12_type,type,
sk__12: g ).
thf(sk__13_type,type,
sk__13: g ).
thf(sk__type,type,
sk_: g > b ).
thf(sk__14_type,type,
sk__14: g ).
thf(sk__1_type,type,
sk__1: b > a ).
thf(sk__4_type,type,
sk__4: b > $o ).
thf(sk__9_type,type,
sk__9: g ).
thf(sk__11_type,type,
sk__11: a ).
thf(sk__8_type,type,
sk__8: g ).
thf(sk__7_type,type,
sk__7: a > a > a ).
thf(sk__5_type,type,
sk__5: b > b > b ).
thf(sk__6_type,type,
sk__6: a > $o ).
thf(sk__2_type,type,
sk__2: g > $o ).
thf(sk__10_type,type,
sk__10: a ).
thf(sk__3_type,type,
sk__3: g > g > g ).
thf(cTHM126_EXPANDED_pme,conjecture,
! [Xh1: g > b,Xh2: b > a,Xs1: g > $o,Xf1: g > g > g,Xs2: b > $o,Xf2: b > b > b,Xs3: a > $o,Xf3: a > a > a] :
( ( ! [Xx: g,Xy: g] :
( ( ( Xs1 @ Xx )
& ( Xs1 @ Xy ) )
=> ( Xs1 @ ( Xf1 @ Xx @ Xy ) ) )
& ! [Xx: b,Xy: b] :
( ( ( Xs2 @ Xx )
& ( Xs2 @ Xy ) )
=> ( Xs2 @ ( Xf2 @ Xx @ Xy ) ) )
& ! [Xx: g] :
( ( Xs1 @ Xx )
=> ( Xs2 @ ( Xh1 @ Xx ) ) )
& ! [Xx: g,Xy: g] :
( ( ( Xs1 @ Xx )
& ( Xs1 @ Xy ) )
=> ( ( Xh1 @ ( Xf1 @ Xx @ Xy ) )
= ( Xf2 @ ( Xh1 @ Xx ) @ ( Xh1 @ Xy ) ) ) )
& ! [Xx: b,Xy: b] :
( ( ( Xs2 @ Xx )
& ( Xs2 @ Xy ) )
=> ( Xs2 @ ( Xf2 @ Xx @ Xy ) ) )
& ! [Xx: a,Xy: a] :
( ( ( Xs3 @ Xx )
& ( Xs3 @ Xy ) )
=> ( Xs3 @ ( Xf3 @ Xx @ Xy ) ) )
& ! [Xx: b] :
( ( Xs2 @ Xx )
=> ( Xs3 @ ( Xh2 @ Xx ) ) )
& ! [Xx: b,Xy: b] :
( ( ( Xs2 @ Xx )
& ( Xs2 @ Xy ) )
=> ( ( Xh2 @ ( Xf2 @ Xx @ Xy ) )
= ( Xf3 @ ( Xh2 @ Xx ) @ ( Xh2 @ Xy ) ) ) ) )
=> ( ! [Xx: g,Xy: g] :
( ( ( Xs1 @ Xx )
& ( Xs1 @ Xy ) )
=> ( Xs1 @ ( Xf1 @ Xx @ Xy ) ) )
& ! [Xx: a,Xy: a] :
( ( ( Xs3 @ Xx )
& ( Xs3 @ Xy ) )
=> ( Xs3 @ ( Xf3 @ Xx @ Xy ) ) )
& ! [Xx: g] :
( ( Xs1 @ Xx )
=> ( Xs3 @ ( Xh2 @ ( Xh1 @ Xx ) ) ) )
& ! [Xx: g,Xy: g] :
( ( ( Xs1 @ Xx )
& ( Xs1 @ Xy )
& ( Xs1 @ Xx )
& ( Xs1 @ Xy ) )
=> ( ( Xh2 @ ( Xh1 @ ( Xf1 @ Xx @ Xy ) ) )
= ( Xf3 @ ( Xh2 @ ( Xh1 @ Xx ) ) @ ( Xh2 @ ( Xh1 @ Xy ) ) ) ) ) ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ! [Xh1: g > b,Xh2: b > a,Xs1: g > $o,Xf1: g > g > g,Xs2: b > $o,Xf2: b > b > b,Xs3: a > $o,Xf3: a > a > a] :
( ( ! [Xx: g,Xy: g] :
( ( ( Xs1 @ Xx )
& ( Xs1 @ Xy ) )
=> ( Xs1 @ ( Xf1 @ Xx @ Xy ) ) )
& ! [Xx: b,Xy: b] :
( ( ( Xs2 @ Xx )
& ( Xs2 @ Xy ) )
=> ( Xs2 @ ( Xf2 @ Xx @ Xy ) ) )
& ! [Xx: g] :
( ( Xs1 @ Xx )
=> ( Xs2 @ ( Xh1 @ Xx ) ) )
& ! [Xx: g,Xy: g] :
( ( ( Xs1 @ Xx )
& ( Xs1 @ Xy ) )
=> ( ( Xh1 @ ( Xf1 @ Xx @ Xy ) )
= ( Xf2 @ ( Xh1 @ Xx ) @ ( Xh1 @ Xy ) ) ) )
& ! [Xx: b,Xy: b] :
( ( ( Xs2 @ Xx )
& ( Xs2 @ Xy ) )
=> ( Xs2 @ ( Xf2 @ Xx @ Xy ) ) )
& ! [Xx: a,Xy: a] :
( ( ( Xs3 @ Xx )
& ( Xs3 @ Xy ) )
=> ( Xs3 @ ( Xf3 @ Xx @ Xy ) ) )
& ! [Xx: b] :
( ( Xs2 @ Xx )
=> ( Xs3 @ ( Xh2 @ Xx ) ) )
& ! [Xx: b,Xy: b] :
( ( ( Xs2 @ Xx )
& ( Xs2 @ Xy ) )
=> ( ( Xh2 @ ( Xf2 @ Xx @ Xy ) )
= ( Xf3 @ ( Xh2 @ Xx ) @ ( Xh2 @ Xy ) ) ) ) )
=> ( ! [Xx: g,Xy: g] :
( ( ( Xs1 @ Xx )
& ( Xs1 @ Xy ) )
=> ( Xs1 @ ( Xf1 @ Xx @ Xy ) ) )
& ! [Xx: a,Xy: a] :
( ( ( Xs3 @ Xx )
& ( Xs3 @ Xy ) )
=> ( Xs3 @ ( Xf3 @ Xx @ Xy ) ) )
& ! [Xx: g] :
( ( Xs1 @ Xx )
=> ( Xs3 @ ( Xh2 @ ( Xh1 @ Xx ) ) ) )
& ! [Xx: g,Xy: g] :
( ( ( Xs1 @ Xx )
& ( Xs1 @ Xy )
& ( Xs1 @ Xx )
& ( Xs1 @ Xy ) )
=> ( ( Xh2 @ ( Xh1 @ ( Xf1 @ Xx @ Xy ) ) )
= ( Xf3 @ ( Xh2 @ ( Xh1 @ Xx ) ) @ ( Xh2 @ ( Xh1 @ Xy ) ) ) ) ) ) ),
inference('cnf.neg',[status(esa)],[cTHM126_EXPANDED_pme]) ).
thf(zip_derived_cl95,plain,
! [X9: g,X10: g] :
( ~ ( sk__2 @ X9 )
| ~ ( sk__2 @ X10 )
| ( ( sk_ @ ( sk__3 @ X9 @ X10 ) )
= ( sk__5 @ ( sk_ @ X9 ) @ ( sk_ @ X10 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_001,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl90,plain,
! [X0: b,X1: b] :
( ~ ( sk__4 @ X0 )
| ~ ( sk__4 @ X1 )
| ( ( sk__1 @ ( sk__5 @ X0 @ X1 ) )
= ( sk__7 @ ( sk__1 @ X0 ) @ ( sk__1 @ X1 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_002,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl97,plain,
! [X13: b] :
( ( sk__6 @ ( sk__1 @ X13 ) )
| ~ ( sk__4 @ X13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl98,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl94_003,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_004,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl92,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl95_005,plain,
! [X9: g,X10: g] :
( ~ ( sk__2 @ X9 )
| ~ ( sk__2 @ X10 )
| ( ( sk_ @ ( sk__3 @ X9 @ X10 ) )
= ( sk__5 @ ( sk_ @ X9 ) @ ( sk_ @ X10 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl90_006,plain,
! [X0: b,X1: b] :
( ~ ( sk__4 @ X0 )
| ~ ( sk__4 @ X1 )
| ( ( sk__1 @ ( sk__5 @ X0 @ X1 ) )
= ( sk__7 @ ( sk__1 @ X0 ) @ ( sk__1 @ X1 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl84,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl524,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__10 )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl90,zip_derived_cl84]) ).
thf(zip_derived_cl655,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__13 )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl95,zip_derived_cl524]) ).
thf(zip_derived_cl62,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl91,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl257,plain,
( ( sk__2 @ sk__14 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 ) ),
inference('sup+',[status(thm)],[zip_derived_cl62,zip_derived_cl91]) ).
thf(zip_derived_cl98_007,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl92_008,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl72,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl292,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( sk__2 @ sk__14 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl72]) ).
thf(zip_derived_cl98_009,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl91_010,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl32,plain,
( ( sk__2 @ sk__9 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl214,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( sk__2 @ sk__14 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl32]) ).
thf(zip_derived_cl98_011,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl42,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl182,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl42]) ).
thf(zip_derived_cl91_012,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl37,plain,
( ( sk__2 @ sk__9 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl173,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl37]) ).
thf(zip_derived_cl47,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl175,plain,
( ( sk__2 @ sk__9 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 )
| ~ ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl173,zip_derived_cl47]) ).
thf(zip_derived_cl57,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl176,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl175,zip_derived_cl57]) ).
thf(zip_derived_cl184,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__14 ) ),
inference(clc,[status(thm)],[zip_derived_cl182,zip_derived_cl176]) ).
thf(zip_derived_cl216,plain,
( ( sk__2 @ sk__9 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 )
| ~ ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl214,zip_derived_cl184]) ).
thf(zip_derived_cl98_013,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl52,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl196,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl52]) ).
thf(zip_derived_cl176_014,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl175,zip_derived_cl57]) ).
thf(zip_derived_cl198,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__14 ) ),
inference(clc,[status(thm)],[zip_derived_cl196,zip_derived_cl176]) ).
thf(zip_derived_cl217,plain,
( ( sk__2 @ sk__14 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl216,zip_derived_cl198]) ).
thf(zip_derived_cl218,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 )
| ( sk__2 @ sk__14 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl217]) ).
thf(zip_derived_cl176_015,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl175,zip_derived_cl57]) ).
thf(zip_derived_cl220,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl218,zip_derived_cl176]) ).
thf(zip_derived_cl296,plain,
( ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl292,zip_derived_cl220]) ).
thf(zip_derived_cl98_016,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl22,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl91_017,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl2,plain,
( ( sk__2 @ sk__8 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl149,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( sk__2 @ sk__14 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl2]) ).
thf(zip_derived_cl98_018,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl12,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl142,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl12]) ).
thf(zip_derived_cl91_019,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl7,plain,
( ( sk__2 @ sk__8 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl123,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl7]) ).
thf(zip_derived_cl17,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl125,plain,
( ( sk__2 @ sk__8 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 )
| ~ ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl123,zip_derived_cl17]) ).
thf(zip_derived_cl27,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl126,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl125,zip_derived_cl27]) ).
thf(zip_derived_cl144,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__14 ) ),
inference(clc,[status(thm)],[zip_derived_cl142,zip_derived_cl126]) ).
thf(zip_derived_cl152,plain,
( ( sk__2 @ sk__8 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 )
| ~ ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl149,zip_derived_cl144]) ).
thf(zip_derived_cl162,plain,
( ( sk__2 @ sk__14 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl22,zip_derived_cl152]) ).
thf(zip_derived_cl163,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 )
| ( sk__2 @ sk__14 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl162]) ).
thf(zip_derived_cl126_020,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl125,zip_derived_cl27]) ).
thf(zip_derived_cl165,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl163,zip_derived_cl126]) ).
thf(zip_derived_cl297,plain,
( ( sk__2 @ sk__14 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__11 ) ),
inference(clc,[status(thm)],[zip_derived_cl296,zip_derived_cl165]) ).
thf(zip_derived_cl298,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__14 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl297]) ).
thf(zip_derived_cl91_021,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl92_022,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl67,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl243,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl67]) ).
thf(zip_derived_cl220_023,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl218,zip_derived_cl176]) ).
thf(zip_derived_cl247,plain,
( ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl243,zip_derived_cl220]) ).
thf(zip_derived_cl165_024,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl163,zip_derived_cl126]) ).
thf(zip_derived_cl248,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl247,zip_derived_cl165]) ).
thf(zip_derived_cl249,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl248]) ).
thf(zip_derived_cl92_025,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl77,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl205,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl77]) ).
thf(zip_derived_cl184_026,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__14 ) ),
inference(clc,[status(thm)],[zip_derived_cl182,zip_derived_cl176]) ).
thf(zip_derived_cl207,plain,
( ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl205,zip_derived_cl184]) ).
thf(zip_derived_cl165_027,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl163,zip_derived_cl126]) ).
thf(zip_derived_cl208,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__11 ) ),
inference(clc,[status(thm)],[zip_derived_cl207,zip_derived_cl165]) ).
thf(zip_derived_cl251,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ~ ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl249,zip_derived_cl208]) ).
thf(zip_derived_cl92_028,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl87,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl226,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl87]) ).
thf(zip_derived_cl220_029,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl218,zip_derived_cl176]) ).
thf(zip_derived_cl228,plain,
( ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl226,zip_derived_cl220]) ).
thf(zip_derived_cl165_030,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl163,zip_derived_cl126]) ).
thf(zip_derived_cl229,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl228,zip_derived_cl165]) ).
thf(zip_derived_cl252,plain,
( ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 ) ),
inference(clc,[status(thm)],[zip_derived_cl251,zip_derived_cl229]) ).
thf(zip_derived_cl300,plain,
( ( sk__2 @ sk__14 )
| ( sk__6 @ sk__11 ) ),
inference(clc,[status(thm)],[zip_derived_cl298,zip_derived_cl252]) ).
thf(zip_derived_cl352,plain,
( ~ ( sk__6 @ sk__10 )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 ) ),
inference(clc,[status(thm)],[zip_derived_cl257,zip_derived_cl300]) ).
thf(zip_derived_cl98_031,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl92_032,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl82,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl328,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( sk__2 @ sk__14 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl82]) ).
thf(zip_derived_cl220_033,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl218,zip_derived_cl176]) ).
thf(zip_derived_cl330,plain,
( ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl328,zip_derived_cl220]) ).
thf(zip_derived_cl165_034,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl163,zip_derived_cl126]) ).
thf(zip_derived_cl331,plain,
( ( sk__2 @ sk__14 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl330,zip_derived_cl165]) ).
thf(zip_derived_cl332,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__14 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl331]) ).
thf(zip_derived_cl252_035,plain,
( ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 ) ),
inference(clc,[status(thm)],[zip_derived_cl251,zip_derived_cl229]) ).
thf(zip_derived_cl334,plain,
( ( sk__2 @ sk__14 )
| ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl332,zip_derived_cl252]) ).
thf(zip_derived_cl353,plain,
( ( sk__2 @ sk__14 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl352,zip_derived_cl334]) ).
thf(zip_derived_cl92_036,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl354,plain,
( ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 ) ),
inference('sup+',[status(thm)],[zip_derived_cl353,zip_derived_cl92]) ).
thf(zip_derived_cl220_037,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl218,zip_derived_cl176]) ).
thf(zip_derived_cl358,plain,
( ~ ( sk__2 @ sk__8 )
| ( sk__2 @ sk__14 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl354,zip_derived_cl220]) ).
thf(zip_derived_cl165_038,plain,
( ( sk__2 @ sk__14 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl163,zip_derived_cl126]) ).
thf(zip_derived_cl359,plain,
( ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__14 ) ),
inference(clc,[status(thm)],[zip_derived_cl358,zip_derived_cl165]) ).
thf(zip_derived_cl98_039,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl360,plain,
( ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__12 ) ),
inference('sup+',[status(thm)],[zip_derived_cl359,zip_derived_cl98]) ).
thf(zip_derived_cl252_040,plain,
( ( sk__2 @ sk__12 )
| ( sk__2 @ sk__14 ) ),
inference(clc,[status(thm)],[zip_derived_cl251,zip_derived_cl229]) ).
thf(zip_derived_cl364,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl60,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl91_041,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl253,plain,
( ( sk__2 @ sk__13 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 ) ),
inference('sup+',[status(thm)],[zip_derived_cl60,zip_derived_cl91]) ).
thf(zip_derived_cl98_042,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl92_043,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl70,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl283,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( sk__2 @ sk__13 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl70]) ).
thf(zip_derived_cl98_044,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl50,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl91_045,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl30,plain,
( ( sk__2 @ sk__9 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl185,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( sk__2 @ sk__13 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl30]) ).
thf(zip_derived_cl98_046,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl40,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl178,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl40]) ).
thf(zip_derived_cl91_047,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl35,plain,
( ( sk__2 @ sk__9 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl168,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl35]) ).
thf(zip_derived_cl45,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl170,plain,
( ( sk__2 @ sk__9 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 )
| ~ ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl168,zip_derived_cl45]) ).
thf(zip_derived_cl55,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl171,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl170,zip_derived_cl55]) ).
thf(zip_derived_cl180,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__13 ) ),
inference(clc,[status(thm)],[zip_derived_cl178,zip_derived_cl171]) ).
thf(zip_derived_cl187,plain,
( ( sk__2 @ sk__9 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 )
| ~ ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl185,zip_derived_cl180]) ).
thf(zip_derived_cl190,plain,
( ( sk__2 @ sk__13 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl50,zip_derived_cl187]) ).
thf(zip_derived_cl191,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 )
| ( sk__2 @ sk__13 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl190]) ).
thf(zip_derived_cl171_048,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl170,zip_derived_cl55]) ).
thf(zip_derived_cl193,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl191,zip_derived_cl171]) ).
thf(zip_derived_cl285,plain,
( ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 )
| ~ ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl283,zip_derived_cl193]) ).
thf(zip_derived_cl98_049,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl20,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl98_050,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl10,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl128,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl10]) ).
thf(zip_derived_cl91_051,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl5,plain,
( ( sk__2 @ sk__8 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl108,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl5]) ).
thf(zip_derived_cl15,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl110,plain,
( ( sk__2 @ sk__8 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 )
| ~ ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl108,zip_derived_cl15]) ).
thf(zip_derived_cl25,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl111,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl110,zip_derived_cl25]) ).
thf(zip_derived_cl130,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__13 ) ),
inference(clc,[status(thm)],[zip_derived_cl128,zip_derived_cl111]) ).
thf(zip_derived_cl91_052,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl0,plain,
( ( sk__2 @ sk__8 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl102,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( sk__2 @ sk__13 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl0]) ).
thf(zip_derived_cl131,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__8 )
| ( sk__2 @ sk__8 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 )
| ~ ( sk__6 @ sk__10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl130,zip_derived_cl102]) ).
thf(zip_derived_cl133,plain,
( ~ ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__8 )
| ( sk__2 @ sk__13 ) ),
inference(simplify,[status(thm)],[zip_derived_cl131]) ).
thf(zip_derived_cl146,plain,
( ( sk__2 @ sk__13 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl20,zip_derived_cl133]) ).
thf(zip_derived_cl147,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 )
| ( sk__2 @ sk__13 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl146]) ).
thf(zip_derived_cl111_053,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl110,zip_derived_cl25]) ).
thf(zip_derived_cl151,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl147,zip_derived_cl111]) ).
thf(zip_derived_cl286,plain,
( ( sk__2 @ sk__13 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__11 ) ),
inference(clc,[status(thm)],[zip_derived_cl285,zip_derived_cl151]) ).
thf(zip_derived_cl287,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__13 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl286]) ).
thf(zip_derived_cl91_054,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl92_055,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl65,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl233,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl65]) ).
thf(zip_derived_cl193_056,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl191,zip_derived_cl171]) ).
thf(zip_derived_cl235,plain,
( ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 )
| ~ ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl233,zip_derived_cl193]) ).
thf(zip_derived_cl151_057,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl147,zip_derived_cl111]) ).
thf(zip_derived_cl236,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl235,zip_derived_cl151]) ).
thf(zip_derived_cl237,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl236]) ).
thf(zip_derived_cl92_058,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl75,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl200,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl75]) ).
thf(zip_derived_cl193_059,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl191,zip_derived_cl171]) ).
thf(zip_derived_cl202,plain,
( ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 )
| ~ ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl200,zip_derived_cl193]) ).
thf(zip_derived_cl151_060,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl147,zip_derived_cl111]) ).
thf(zip_derived_cl203,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__11 ) ),
inference(clc,[status(thm)],[zip_derived_cl202,zip_derived_cl151]) ).
thf(zip_derived_cl239,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ~ ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl237,zip_derived_cl203]) ).
thf(zip_derived_cl92_061,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl85,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl221,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl85]) ).
thf(zip_derived_cl193_062,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl191,zip_derived_cl171]) ).
thf(zip_derived_cl223,plain,
( ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 )
| ~ ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl221,zip_derived_cl193]) ).
thf(zip_derived_cl151_063,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl147,zip_derived_cl111]) ).
thf(zip_derived_cl224,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl223,zip_derived_cl151]) ).
thf(zip_derived_cl240,plain,
( ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 ) ),
inference(clc,[status(thm)],[zip_derived_cl239,zip_derived_cl224]) ).
thf(zip_derived_cl289,plain,
( ( sk__2 @ sk__13 )
| ( sk__6 @ sk__11 ) ),
inference(clc,[status(thm)],[zip_derived_cl287,zip_derived_cl240]) ).
thf(zip_derived_cl337,plain,
( ~ ( sk__6 @ sk__10 )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 ) ),
inference(clc,[status(thm)],[zip_derived_cl253,zip_derived_cl289]) ).
thf(zip_derived_cl98_064,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl92_065,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl80,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl303,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( sk__2 @ sk__13 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl80]) ).
thf(zip_derived_cl193_066,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl191,zip_derived_cl171]) ).
thf(zip_derived_cl321,plain,
( ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 )
| ~ ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl303,zip_derived_cl193]) ).
thf(zip_derived_cl151_067,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl147,zip_derived_cl111]) ).
thf(zip_derived_cl322,plain,
( ( sk__2 @ sk__13 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl321,zip_derived_cl151]) ).
thf(zip_derived_cl323,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__13 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl322]) ).
thf(zip_derived_cl240_068,plain,
( ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 ) ),
inference(clc,[status(thm)],[zip_derived_cl239,zip_derived_cl224]) ).
thf(zip_derived_cl325,plain,
( ( sk__2 @ sk__13 )
| ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl323,zip_derived_cl240]) ).
thf(zip_derived_cl338,plain,
( ( sk__2 @ sk__13 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl337,zip_derived_cl325]) ).
thf(zip_derived_cl92_069,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl339,plain,
( ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 )
| ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 ) ),
inference('sup+',[status(thm)],[zip_derived_cl338,zip_derived_cl92]) ).
thf(zip_derived_cl193_070,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl191,zip_derived_cl171]) ).
thf(zip_derived_cl345,plain,
( ~ ( sk__2 @ sk__8 )
| ( sk__2 @ sk__13 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl339,zip_derived_cl193]) ).
thf(zip_derived_cl151_071,plain,
( ( sk__2 @ sk__13 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl147,zip_derived_cl111]) ).
thf(zip_derived_cl346,plain,
( ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__2 @ sk__13 ) ),
inference(clc,[status(thm)],[zip_derived_cl345,zip_derived_cl151]) ).
thf(zip_derived_cl98_072,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl347,plain,
( ( sk__2 @ sk__13 )
| ~ ( sk__2 @ sk__12 ) ),
inference('sup+',[status(thm)],[zip_derived_cl346,zip_derived_cl98]) ).
thf(zip_derived_cl240_073,plain,
( ( sk__2 @ sk__12 )
| ( sk__2 @ sk__13 ) ),
inference(clc,[status(thm)],[zip_derived_cl239,zip_derived_cl224]) ).
thf(zip_derived_cl351,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl657,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl655,zip_derived_cl364,zip_derived_cl351]) ).
thf(zip_derived_cl658,plain,
( ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__10 )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl657]) ).
thf(zip_derived_cl682,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl658]) ).
thf(zip_derived_cl94_074,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_075,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl95_076,plain,
! [X9: g,X10: g] :
( ~ ( sk__2 @ X9 )
| ~ ( sk__2 @ X10 )
| ( ( sk_ @ ( sk__3 @ X9 @ X10 ) )
= ( sk__5 @ ( sk_ @ X9 ) @ ( sk_ @ X10 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl90_077,plain,
! [X0: b,X1: b] :
( ~ ( sk__4 @ X0 )
| ~ ( sk__4 @ X1 )
| ( ( sk__1 @ ( sk__5 @ X0 @ X1 ) )
= ( sk__7 @ ( sk__1 @ X0 ) @ ( sk__1 @ X1 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl98_078,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl24,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl343,plain,
( ~ ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl24]) ).
thf(zip_derived_cl94_079,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_080,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl95_081,plain,
! [X9: g,X10: g] :
( ~ ( sk__2 @ X9 )
| ~ ( sk__2 @ X10 )
| ( ( sk_ @ ( sk__3 @ X9 @ X10 ) )
= ( sk__5 @ ( sk_ @ X9 ) @ ( sk_ @ X10 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl90_082,plain,
! [X0: b,X1: b] :
( ~ ( sk__4 @ X0 )
| ~ ( sk__4 @ X1 )
| ( ( sk__1 @ ( sk__5 @ X0 @ X1 ) )
= ( sk__7 @ ( sk__1 @ X0 ) @ ( sk__1 @ X1 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl95_083,plain,
! [X9: g,X10: g] :
( ~ ( sk__2 @ X9 )
| ~ ( sk__2 @ X10 )
| ( ( sk_ @ ( sk__3 @ X9 @ X10 ) )
= ( sk__5 @ ( sk_ @ X9 ) @ ( sk_ @ X10 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_084,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_085,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl90_086,plain,
! [X0: b,X1: b] :
( ~ ( sk__4 @ X0 )
| ~ ( sk__4 @ X1 )
| ( ( sk__1 @ ( sk__5 @ X0 @ X1 ) )
= ( sk__7 @ ( sk__1 @ X0 ) @ ( sk__1 @ X1 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl49,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl92_087,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl79,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl393,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl79]) ).
thf(zip_derived_cl98_088,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl14,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl245,plain,
( ~ ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl14]) ).
thf(zip_derived_cl19,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl365,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl245,zip_derived_cl19]) ).
thf(zip_derived_cl395,plain,
( ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl393,zip_derived_cl365]) ).
thf(zip_derived_cl440,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__11 ) ),
inference(clc,[status(thm)],[zip_derived_cl49,zip_derived_cl395]) ).
thf(zip_derived_cl441,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 ) ),
inference('sup-',[status(thm)],[zip_derived_cl90,zip_derived_cl440]) ).
thf(zip_derived_cl450,plain,
( ~ ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__11 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl441]) ).
thf(zip_derived_cl364_089,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl452,plain,
( ( sk__2 @ sk__12 )
| ( sk__6 @ sk__11 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl450,zip_derived_cl364]) ).
thf(zip_derived_cl454,plain,
( ~ ( sk__2 @ sk__13 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl452]) ).
thf(zip_derived_cl351_090,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl456,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 ) ),
inference(demod,[status(thm)],[zip_derived_cl454,zip_derived_cl351]) ).
thf(zip_derived_cl458,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl95,zip_derived_cl456]) ).
thf(zip_derived_cl364_091,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl351_092,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl460,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__11 ) ),
inference(demod,[status(thm)],[zip_derived_cl458,zip_derived_cl364,zip_derived_cl351]) ).
thf(zip_derived_cl461,plain,
( ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 ) ),
inference(simplify,[status(thm)],[zip_derived_cl460]) ).
thf(zip_derived_cl91_093,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl69,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl98_094,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl92_095,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl64,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl405,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl64]) ).
thf(zip_derived_cl34,plain,
( ( sk__2 @ sk__9 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl407,plain,
( ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl405,zip_derived_cl34]) ).
thf(zip_derived_cl4,plain,
( ( sk__2 @ sk__8 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl408,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl407,zip_derived_cl4]) ).
thf(zip_derived_cl409,plain,
( ~ ( sk__2 @ sk__12 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl408]) ).
thf(zip_derived_cl480,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl69,zip_derived_cl409]) ).
thf(zip_derived_cl481,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl480]) ).
thf(zip_derived_cl493,plain,
( ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ~ ( sk__6 @ sk__10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl461,zip_derived_cl481]) ).
thf(zip_derived_cl95_096,plain,
! [X9: g,X10: g] :
( ~ ( sk__2 @ X9 )
| ~ ( sk__2 @ X10 )
| ( ( sk_ @ ( sk__3 @ X9 @ X10 ) )
= ( sk__5 @ ( sk_ @ X9 ) @ ( sk_ @ X10 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_097,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_098,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl90_099,plain,
! [X0: b,X1: b] :
( ~ ( sk__4 @ X0 )
| ~ ( sk__4 @ X1 )
| ( ( sk__1 @ ( sk__5 @ X0 @ X1 ) )
= ( sk__7 @ ( sk__1 @ X0 ) @ ( sk__1 @ X1 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl59,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl92_100,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl89,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl397,plain,
( ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl92,zip_derived_cl89]) ).
thf(zip_derived_cl29,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl91_101,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl9,plain,
( ( sk__2 @ sk__8 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl209,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl9]) ).
thf(zip_derived_cl365_102,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl245,zip_derived_cl19]) ).
thf(zip_derived_cl368,plain,
( ( sk__2 @ sk__8 )
| ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl209,zip_derived_cl365]) ).
thf(zip_derived_cl382,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl29,zip_derived_cl368]) ).
thf(zip_derived_cl399,plain,
( ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__9 ) ),
inference(clc,[status(thm)],[zip_derived_cl397,zip_derived_cl382]) ).
thf(zip_derived_cl469,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__10 ) ),
inference(clc,[status(thm)],[zip_derived_cl59,zip_derived_cl399]) ).
thf(zip_derived_cl470,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 ) ),
inference('sup-',[status(thm)],[zip_derived_cl90,zip_derived_cl469]) ).
thf(zip_derived_cl472,plain,
( ~ ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__10 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl470]) ).
thf(zip_derived_cl364_103,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl474,plain,
( ( sk__2 @ sk__12 )
| ( sk__6 @ sk__10 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl472,zip_derived_cl364]) ).
thf(zip_derived_cl476,plain,
( ~ ( sk__2 @ sk__13 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl474]) ).
thf(zip_derived_cl351_104,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl478,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 ) ),
inference(demod,[status(thm)],[zip_derived_cl476,zip_derived_cl351]) ).
thf(zip_derived_cl483,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl95,zip_derived_cl478]) ).
thf(zip_derived_cl364_105,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl351_106,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl485,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 )
| ( sk__6 @ sk__10 ) ),
inference(demod,[status(thm)],[zip_derived_cl483,zip_derived_cl364,zip_derived_cl351]) ).
thf(zip_derived_cl486,plain,
( ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 ) ),
inference(simplify,[status(thm)],[zip_derived_cl485]) ).
thf(zip_derived_cl516,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 ) ),
inference(clc,[status(thm)],[zip_derived_cl493,zip_derived_cl486]) ).
thf(zip_derived_cl517,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( sk__2 @ sk__12 )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl90,zip_derived_cl516]) ).
thf(zip_derived_cl526,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__13 )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__2 @ sk__12 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl95,zip_derived_cl517]) ).
thf(zip_derived_cl364_107,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl351_108,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl528,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__2 @ sk__12 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl526,zip_derived_cl364,zip_derived_cl351]) ).
thf(zip_derived_cl529,plain,
( ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( sk__2 @ sk__12 )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl528]) ).
thf(zip_derived_cl92_109,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl532,plain,
( ( sk__2 @ sk__12 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 ) ),
inference('sup+',[status(thm)],[zip_derived_cl529,zip_derived_cl92]) ).
thf(zip_derived_cl95_110,plain,
! [X9: g,X10: g] :
( ~ ( sk__2 @ X9 )
| ~ ( sk__2 @ X10 )
| ( ( sk_ @ ( sk__3 @ X9 @ X10 ) )
= ( sk__5 @ ( sk_ @ X9 ) @ ( sk_ @ X10 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_111,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_112,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl90_113,plain,
! [X0: b,X1: b] :
( ~ ( sk__4 @ X0 )
| ~ ( sk__4 @ X1 )
| ( ( sk__1 @ ( sk__5 @ X0 @ X1 ) )
= ( sk__7 @ ( sk__1 @ X0 ) @ ( sk__1 @ X1 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl486_114,plain,
( ( sk__6 @ sk__10 )
| ( sk__2 @ sk__12 ) ),
inference(simplify,[status(thm)],[zip_derived_cl485]) ).
thf(zip_derived_cl461_115,plain,
( ( sk__6 @ sk__11 )
| ( sk__2 @ sk__12 ) ),
inference(simplify,[status(thm)],[zip_derived_cl460]) ).
thf(zip_derived_cl91_116,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl39,plain,
( ( sk__2 @ sk__9 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl370,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl39]) ).
thf(zip_derived_cl464,plain,
( ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 )
| ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__6 @ sk__10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl461,zip_derived_cl370]) ).
thf(zip_derived_cl466,plain,
( ~ ( sk__6 @ sk__10 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__9 )
| ( sk__2 @ sk__12 ) ),
inference(simplify,[status(thm)],[zip_derived_cl464]) ).
thf(zip_derived_cl489,plain,
( ( sk__2 @ sk__12 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl486,zip_derived_cl466]) ).
thf(zip_derived_cl491,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__9 )
| ( sk__2 @ sk__12 ) ),
inference(simplify,[status(thm)],[zip_derived_cl489]) ).
thf(zip_derived_cl498,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl90,zip_derived_cl491]) ).
thf(zip_derived_cl500,plain,
( ~ ( sk__2 @ sk__14 )
| ( sk__2 @ sk__9 )
| ( sk__2 @ sk__12 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl498]) ).
thf(zip_derived_cl364_117,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl502,plain,
( ( sk__2 @ sk__9 )
| ( sk__2 @ sk__12 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl500,zip_derived_cl364]) ).
thf(zip_derived_cl504,plain,
( ~ ( sk__2 @ sk__13 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl502]) ).
thf(zip_derived_cl351_118,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl506,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 ) ),
inference(demod,[status(thm)],[zip_derived_cl504,zip_derived_cl351]) ).
thf(zip_derived_cl508,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__13 )
| ( sk__2 @ sk__9 )
| ( sk__2 @ sk__12 ) ),
inference('sup-',[status(thm)],[zip_derived_cl95,zip_derived_cl506]) ).
thf(zip_derived_cl364_119,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl351_120,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl510,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ( sk__2 @ sk__9 )
| ( sk__2 @ sk__12 ) ),
inference(demod,[status(thm)],[zip_derived_cl508,zip_derived_cl364,zip_derived_cl351]) ).
thf(zip_derived_cl511,plain,
( ( sk__2 @ sk__12 )
| ( sk__2 @ sk__9 ) ),
inference(simplify,[status(thm)],[zip_derived_cl510]) ).
thf(zip_derived_cl536,plain,
( ~ ( sk__2 @ sk__8 )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( sk__2 @ sk__12 ) ),
inference(clc,[status(thm)],[zip_derived_cl532,zip_derived_cl511]) ).
thf(zip_derived_cl95_121,plain,
! [X9: g,X10: g] :
( ~ ( sk__2 @ X9 )
| ~ ( sk__2 @ X10 )
| ( ( sk_ @ ( sk__3 @ X9 @ X10 ) )
= ( sk__5 @ ( sk_ @ X9 ) @ ( sk_ @ X10 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_122,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_123,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl90_124,plain,
! [X0: b,X1: b] :
( ~ ( sk__4 @ X0 )
| ~ ( sk__4 @ X1 )
| ( ( sk__1 @ ( sk__5 @ X0 @ X1 ) )
= ( sk__7 @ ( sk__1 @ X0 ) @ ( sk__1 @ X1 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl382_125,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 ) ),
inference(clc,[status(thm)],[zip_derived_cl29,zip_derived_cl368]) ).
thf(zip_derived_cl383,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( sk__2 @ sk__8 )
| ( sk__2 @ sk__12 ) ),
inference('sup-',[status(thm)],[zip_derived_cl90,zip_derived_cl382]) ).
thf(zip_derived_cl432,plain,
( ~ ( sk__2 @ sk__14 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl383]) ).
thf(zip_derived_cl364_126,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl434,plain,
( ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl432,zip_derived_cl364]) ).
thf(zip_derived_cl436,plain,
( ~ ( sk__2 @ sk__13 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__8 )
| ( sk__2 @ sk__12 ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl434]) ).
thf(zip_derived_cl351_127,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl438,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__8 )
| ( sk__2 @ sk__12 ) ),
inference(demod,[status(thm)],[zip_derived_cl436,zip_derived_cl351]) ).
thf(zip_derived_cl443,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl95,zip_derived_cl438]) ).
thf(zip_derived_cl364_128,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl351_129,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl445,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ( sk__2 @ sk__12 )
| ( sk__2 @ sk__8 ) ),
inference(demod,[status(thm)],[zip_derived_cl443,zip_derived_cl364,zip_derived_cl351]) ).
thf(zip_derived_cl446,plain,
( ( sk__2 @ sk__8 )
| ( sk__2 @ sk__12 ) ),
inference(simplify,[status(thm)],[zip_derived_cl445]) ).
thf(zip_derived_cl537,plain,
( ( sk__2 @ sk__12 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl536,zip_derived_cl446]) ).
thf(zip_derived_cl539,plain,
( ~ ( sk__2 @ sk__14 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( sk__2 @ sk__12 ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl537]) ).
thf(zip_derived_cl364_130,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl542,plain,
( ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( sk__2 @ sk__12 ) ),
inference(demod,[status(thm)],[zip_derived_cl539,zip_derived_cl364]) ).
thf(zip_derived_cl547,plain,
( ~ ( sk__2 @ sk__13 )
| ( sk__2 @ sk__12 ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl542]) ).
thf(zip_derived_cl351_131,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl550,plain,
sk__2 @ sk__12,
inference(demod,[status(thm)],[zip_derived_cl547,zip_derived_cl351]) ).
thf(zip_derived_cl554,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__8 ) ),
inference(demod,[status(thm)],[zip_derived_cl343,zip_derived_cl550]) ).
thf(zip_derived_cl95_132,plain,
! [X9: g,X10: g] :
( ~ ( sk__2 @ X9 )
| ~ ( sk__2 @ X10 )
| ( ( sk_ @ ( sk__3 @ X9 @ X10 ) )
= ( sk__5 @ ( sk_ @ X9 ) @ ( sk_ @ X10 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_133,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_134,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl90_135,plain,
! [X0: b,X1: b] :
( ~ ( sk__4 @ X0 )
| ~ ( sk__4 @ X1 )
| ( ( sk__1 @ ( sk__5 @ X0 @ X1 ) )
= ( sk__7 @ ( sk__1 @ X0 ) @ ( sk__1 @ X1 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl365_136,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl245,zip_derived_cl19]) ).
thf(zip_derived_cl366,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl90,zip_derived_cl365]) ).
thf(zip_derived_cl411,plain,
( ~ ( sk__2 @ sk__14 )
| ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl366]) ).
thf(zip_derived_cl364_137,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl413,plain,
( ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl411,zip_derived_cl364]) ).
thf(zip_derived_cl415,plain,
( ~ ( sk__2 @ sk__13 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl413]) ).
thf(zip_derived_cl351_138,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl417,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__8 ) ),
inference(demod,[status(thm)],[zip_derived_cl415,zip_derived_cl351]) ).
thf(zip_derived_cl419,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__13 )
| ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl95,zip_derived_cl417]) ).
thf(zip_derived_cl364_139,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl351_140,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl421,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ( sk__2 @ sk__8 )
| ( sk__6 @ sk__11 ) ),
inference(demod,[status(thm)],[zip_derived_cl419,zip_derived_cl364,zip_derived_cl351]) ).
thf(zip_derived_cl422,plain,
( ( sk__6 @ sk__11 )
| ( sk__2 @ sk__8 ) ),
inference(simplify,[status(thm)],[zip_derived_cl421]) ).
thf(zip_derived_cl91_141,plain,
! [X2: a,X3: a] :
( ~ ( sk__6 @ X2 )
| ~ ( sk__6 @ X3 )
| ( sk__6 @ ( sk__7 @ X2 @ X3 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl409_142,plain,
( ~ ( sk__2 @ sk__12 )
| ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl408]) ).
thf(zip_derived_cl550_143,plain,
sk__2 @ sk__12,
inference(demod,[status(thm)],[zip_derived_cl547,zip_derived_cl351]) ).
thf(zip_derived_cl557,plain,
( ~ ( sk__6 @ ( sk__7 @ sk__10 @ sk__11 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl409,zip_derived_cl550]) ).
thf(zip_derived_cl562,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl557]) ).
thf(zip_derived_cl564,plain,
( ( sk__2 @ sk__8 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__6 @ sk__10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl422,zip_derived_cl562]) ).
thf(zip_derived_cl578,plain,
( ( sk__2 @ sk__8 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl554,zip_derived_cl564]) ).
thf(zip_derived_cl579,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl90,zip_derived_cl578]) ).
thf(zip_derived_cl649,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__13 )
| ( sk__2 @ sk__8 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl95,zip_derived_cl579]) ).
thf(zip_derived_cl364_144,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl351_145,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl651,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ( sk__2 @ sk__8 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl649,zip_derived_cl364,zip_derived_cl351]) ).
thf(zip_derived_cl652,plain,
( ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( sk__2 @ sk__8 ) ),
inference(simplify,[status(thm)],[zip_derived_cl651]) ).
thf(zip_derived_cl662,plain,
( ~ ( sk__2 @ sk__14 )
| ( sk__2 @ sk__8 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl652]) ).
thf(zip_derived_cl364_146,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl665,plain,
( ( sk__2 @ sk__8 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl662,zip_derived_cl364]) ).
thf(zip_derived_cl670,plain,
( ~ ( sk__2 @ sk__13 )
| ( sk__2 @ sk__8 ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl665]) ).
thf(zip_derived_cl351_147,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl673,plain,
sk__2 @ sk__8,
inference(demod,[status(thm)],[zip_derived_cl670,zip_derived_cl351]) ).
thf(zip_derived_cl685,plain,
( ~ ( sk__2 @ sk__9 )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl682,zip_derived_cl673]) ).
thf(zip_derived_cl690,plain,
( ~ ( sk__2 @ sk__14 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__10 )
| ~ ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl685]) ).
thf(zip_derived_cl364_148,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl693,plain,
( ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__10 )
| ~ ( sk__2 @ sk__9 ) ),
inference(demod,[status(thm)],[zip_derived_cl690,zip_derived_cl364]) ).
thf(zip_derived_cl698,plain,
( ~ ( sk__2 @ sk__13 )
| ~ ( sk__2 @ sk__9 )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl693]) ).
thf(zip_derived_cl351_149,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl701,plain,
( ~ ( sk__2 @ sk__9 )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl698,zip_derived_cl351]) ).
thf(zip_derived_cl706,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__6 @ sk__10 )
| ~ ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl701]) ).
thf(zip_derived_cl550_150,plain,
sk__2 @ sk__12,
inference(demod,[status(thm)],[zip_derived_cl547,zip_derived_cl351]) ).
thf(zip_derived_cl709,plain,
( ( sk__6 @ sk__10 )
| ~ ( sk__2 @ sk__9 ) ),
inference(demod,[status(thm)],[zip_derived_cl706,zip_derived_cl550]) ).
thf(zip_derived_cl562_151,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl557]) ).
thf(zip_derived_cl98_152,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl94_153,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_154,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl95_155,plain,
! [X9: g,X10: g] :
( ~ ( sk__2 @ X9 )
| ~ ( sk__2 @ X10 )
| ( ( sk_ @ ( sk__3 @ X9 @ X10 ) )
= ( sk__5 @ ( sk_ @ X9 ) @ ( sk_ @ X10 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl90_156,plain,
! [X0: b,X1: b] :
( ~ ( sk__4 @ X0 )
| ~ ( sk__4 @ X1 )
| ( ( sk__1 @ ( sk__5 @ X0 @ X1 ) )
= ( sk__7 @ ( sk__1 @ X0 ) @ ( sk__1 @ X1 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl74,plain,
( ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl521,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__11 )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl90,zip_derived_cl74]) ).
thf(zip_derived_cl605,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__13 )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl95,zip_derived_cl521]) ).
thf(zip_derived_cl364_157,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl351_158,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl607,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) )
| ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl605,zip_derived_cl364,zip_derived_cl351]) ).
thf(zip_derived_cl608,plain,
( ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__11 )
| ~ ( sk__2 @ ( sk__3 @ sk__8 @ sk__9 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl607]) ).
thf(zip_derived_cl92_159,plain,
! [X4: g,X5: g] :
( ~ ( sk__2 @ X4 )
| ~ ( sk__2 @ X5 )
| ( sk__2 @ ( sk__3 @ X4 @ X5 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl611,plain,
( ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__2 @ sk__9 )
| ~ ( sk__2 @ sk__8 ) ),
inference('sup+',[status(thm)],[zip_derived_cl608,zip_derived_cl92]) ).
thf(zip_derived_cl95_160,plain,
! [X9: g,X10: g] :
( ~ ( sk__2 @ X9 )
| ~ ( sk__2 @ X10 )
| ( ( sk_ @ ( sk__3 @ X9 @ X10 ) )
= ( sk__5 @ ( sk_ @ X9 ) @ ( sk_ @ X10 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_161,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl94_162,plain,
! [X8: g] :
( ( sk__4 @ ( sk_ @ X8 ) )
| ~ ( sk__2 @ X8 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl90_163,plain,
! [X0: b,X1: b] :
( ~ ( sk__4 @ X0 )
| ~ ( sk__4 @ X1 )
| ( ( sk__1 @ ( sk__5 @ X0 @ X1 ) )
= ( sk__7 @ ( sk__1 @ X0 ) @ ( sk__1 @ X1 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl98_164,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl44,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl389,plain,
( ~ ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl44]) ).
thf(zip_derived_cl550_165,plain,
sk__2 @ sk__12,
inference(demod,[status(thm)],[zip_derived_cl547,zip_derived_cl351]) ).
thf(zip_derived_cl555,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__9 ) ),
inference(demod,[status(thm)],[zip_derived_cl389,zip_derived_cl550]) ).
thf(zip_derived_cl581,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl90,zip_derived_cl555]) ).
thf(zip_derived_cl583,plain,
( ~ ( sk__2 @ sk__14 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__9 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl581]) ).
thf(zip_derived_cl364_166,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl585,plain,
( ( sk__6 @ sk__11 )
| ( sk__2 @ sk__9 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl583,zip_derived_cl364]) ).
thf(zip_derived_cl587,plain,
( ~ ( sk__2 @ sk__13 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl585]) ).
thf(zip_derived_cl351_167,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl589,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 ) ),
inference(demod,[status(thm)],[zip_derived_cl587,zip_derived_cl351]) ).
thf(zip_derived_cl591,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__13 )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl95,zip_derived_cl589]) ).
thf(zip_derived_cl364_168,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl351_169,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl593,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ( sk__6 @ sk__11 )
| ( sk__2 @ sk__9 ) ),
inference(demod,[status(thm)],[zip_derived_cl591,zip_derived_cl364,zip_derived_cl351]) ).
thf(zip_derived_cl594,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 ) ),
inference(simplify,[status(thm)],[zip_derived_cl593]) ).
thf(zip_derived_cl615,plain,
( ~ ( sk__2 @ sk__8 )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__11 ) ),
inference(clc,[status(thm)],[zip_derived_cl611,zip_derived_cl594]) ).
thf(zip_derived_cl422_170,plain,
( ( sk__6 @ sk__11 )
| ( sk__2 @ sk__8 ) ),
inference(simplify,[status(thm)],[zip_derived_cl421]) ).
thf(zip_derived_cl616,plain,
( ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl615,zip_derived_cl422]) ).
thf(zip_derived_cl618,plain,
( ~ ( sk__2 @ sk__14 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl616]) ).
thf(zip_derived_cl364_171,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl621,plain,
( ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( sk__6 @ sk__11 ) ),
inference(demod,[status(thm)],[zip_derived_cl618,zip_derived_cl364]) ).
thf(zip_derived_cl626,plain,
( ~ ( sk__2 @ sk__13 )
| ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl621]) ).
thf(zip_derived_cl351_172,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl629,plain,
( ( sk__6 @ sk__11 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl626,zip_derived_cl351]) ).
thf(zip_derived_cl634,plain,
( ~ ( sk__2 @ sk__12 )
| ( sk__6 @ sk__11 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl629]) ).
thf(zip_derived_cl550_173,plain,
sk__2 @ sk__12,
inference(demod,[status(thm)],[zip_derived_cl547,zip_derived_cl351]) ).
thf(zip_derived_cl637,plain,
sk__6 @ sk__11,
inference(demod,[status(thm)],[zip_derived_cl634,zip_derived_cl550]) ).
thf(zip_derived_cl641,plain,
( ~ ( sk__6 @ sk__10 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl562,zip_derived_cl637]) ).
thf(zip_derived_cl713,plain,
( ~ ( sk__2 @ sk__9 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl709,zip_derived_cl641]) ).
thf(zip_derived_cl98_174,plain,
! [X0: g] :
( ~ ( sk__2 @ X0 )
| ( sk__6 @ ( sk__1 @ ( sk_ @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl97]) ).
thf(zip_derived_cl54,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__10 )
| ~ ( sk__6 @ ( sk__1 @ ( sk_ @ sk__12 ) ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl391,plain,
( ~ ( sk__2 @ sk__12 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__9 ) ),
inference('sup-',[status(thm)],[zip_derived_cl98,zip_derived_cl54]) ).
thf(zip_derived_cl550_175,plain,
sk__2 @ sk__12,
inference(demod,[status(thm)],[zip_derived_cl547,zip_derived_cl351]) ).
thf(zip_derived_cl556,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ( sk__6 @ sk__10 )
| ( sk__2 @ sk__9 ) ),
inference(demod,[status(thm)],[zip_derived_cl391,zip_derived_cl550]) ).
thf(zip_derived_cl594_176,plain,
( ( sk__2 @ sk__9 )
| ( sk__6 @ sk__11 ) ),
inference(simplify,[status(thm)],[zip_derived_cl593]) ).
thf(zip_derived_cl562_177,plain,
( ~ ( sk__6 @ sk__11 )
| ~ ( sk__6 @ sk__10 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl91,zip_derived_cl557]) ).
thf(zip_derived_cl597,plain,
( ( sk__2 @ sk__9 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__6 @ sk__10 ) ),
inference('sup-',[status(thm)],[zip_derived_cl594,zip_derived_cl562]) ).
thf(zip_derived_cl602,plain,
( ( sk__2 @ sk__9 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl556,zip_derived_cl597]) ).
thf(zip_derived_cl725,plain,
( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__7 @ ( sk__1 @ ( sk_ @ sk__13 ) ) @ ( sk__1 @ ( sk_ @ sk__14 ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl713,zip_derived_cl602]) ).
thf(zip_derived_cl726,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) )
| ~ ( sk__4 @ ( sk_ @ sk__14 ) )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl90,zip_derived_cl725]) ).
thf(zip_derived_cl737,plain,
( ~ ( sk__2 @ sk__14 )
| ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl726]) ).
thf(zip_derived_cl364_178,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl739,plain,
( ~ ( sk__4 @ ( sk_ @ sk__13 ) )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl737,zip_derived_cl364]) ).
thf(zip_derived_cl741,plain,
( ~ ( sk__2 @ sk__13 )
| ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl739]) ).
thf(zip_derived_cl351_179,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl743,plain,
( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk__5 @ ( sk_ @ sk__13 ) @ ( sk_ @ sk__14 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl741,zip_derived_cl351]) ).
thf(zip_derived_cl745,plain,
( ( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) )
| ~ ( sk__2 @ sk__14 )
| ~ ( sk__2 @ sk__13 ) ),
inference('sup-',[status(thm)],[zip_derived_cl95,zip_derived_cl743]) ).
thf(zip_derived_cl364_180,plain,
sk__2 @ sk__14,
inference(clc,[status(thm)],[zip_derived_cl360,zip_derived_cl252]) ).
thf(zip_derived_cl351_181,plain,
sk__2 @ sk__13,
inference(clc,[status(thm)],[zip_derived_cl347,zip_derived_cl240]) ).
thf(zip_derived_cl747,plain,
( ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) )
!= ( sk__1 @ ( sk_ @ ( sk__3 @ sk__13 @ sk__14 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl745,zip_derived_cl364,zip_derived_cl351]) ).
thf(zip_derived_cl748,plain,
$false,
inference(simplify,[status(thm)],[zip_derived_cl747]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.21 % Problem : SYO228^5 : TPTP v9.2.0. Released v4.0.0.
% 0.11/0.23 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.rD0grtqTOB true
% 0.12/0.44 % Computer : n016.cluster.edu
% 0.12/0.44 % Model : x86_64 x86_64
% 0.12/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.44 % Memory : 8042.1875MB
% 0.12/0.44 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.44 % CPULimit : 300
% 0.12/0.44 % WCLimit : 300
% 0.12/0.44 % DateTime : Wed Oct 1 18:14:08 EDT 2025
% 0.12/0.44 % CPUTime :
% 0.12/0.44 % Running portfolio for 300 s
% 0.12/0.44 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.44 % Number of cores: 8
% 0.12/0.44 % Python version: Python 3.6.8
% 0.12/0.44 % Running in HO mode
% 0.27/0.71 % Total configuration time : 828
% 0.27/0.71 % Estimated wc time : 1656
% 0.27/0.71 % Estimated cpu time (8 cpus) : 207.0
% 0.29/0.83 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.29/0.93 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.29/1.00 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.29/1.06 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 1.13/1.08 % /export/starexec/sandbox/solver/bin/lams/40_noforms.sh running for 90s
% 1.13/1.08 % /export/starexec/sandbox/solver/bin/lams/40_b.comb.sh running for 70s
% 1.13/1.08 % /export/starexec/sandbox/solver/bin/lams/30_sp5.sh running for 60s
% 1.13/1.08 % /export/starexec/sandbox/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 1.13/1.10 % Solved by lams/40_c.s.sh.
% 1.13/1.10 % done 315 iterations in 0.166s
% 1.13/1.10 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 1.13/1.10 % SZS output start Refutation
% See solution above
% 1.13/1.11
% 1.13/1.11
% 1.13/1.11 % Terminating...
% 1.21/1.23 % Runner terminated.
% 1.26/1.23 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------