%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SYO905^6 : TPTP v9.2.0. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.CSXoxSbglY true
% Computer : n007.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:08:32 PM UTC 2025
% Result : Theorem 10.17s 3.38s
% Output : Refutation 10.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 33
% Syntax : Number of formulae : 519 ( 446 unt; 0 typ; 0 def)
% Number of atoms : 1847 ( 18 equ; 0 cnn)
% Maximal formula atoms : 159 ( 3 avg)
% Number of connectives : 4323 ( 515 ~; 523 |; 69 &;2960 @)
% ( 0 <=>; 256 =>; 0 <=; 0 <~>)
% Maximal formula depth : 85 ( 8 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 24 ( 24 >; 0 *; 0 +; 0 <<)
% Number of symbols : 40 ( 37 usr; 3 con; 0-3 aty)
% Number of variables : 1684 ( 55 ^;1586 !; 43 ?;1684 :)
% Comments :
%------------------------------------------------------------------------------
thf(mworld_type,type,
mworld: $tType ).
thf(sk__12_type,type,
sk__12: mworld > mworld ).
thf(v20_type,type,
v20: mworld > $o ).
thf(sk__10_type,type,
sk__10: mworld > mworld ).
thf(v23_type,type,
v23: mworld > $o ).
thf(v24_type,type,
v24: mworld > $o ).
thf(v16_type,type,
v16: mworld > $o ).
thf(v8_type,type,
v8: mworld > $o ).
thf(mbox_type,type,
mbox: ( mworld > $o ) > mworld > $o ).
thf(v13_type,type,
v13: mworld > $o ).
thf(v22_type,type,
v22: mworld > $o ).
thf(v14_type,type,
v14: mworld > $o ).
thf(sk__6_type,type,
sk__6: mworld > mworld ).
thf(sk__36_type,type,
sk__36: mworld > mworld ).
thf(mactual_type,type,
mactual: mworld ).
thf(mand_type,type,
mand: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
thf(v25_type,type,
v25: mworld > $o ).
thf(mor_type,type,
mor: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
thf(v26_type,type,
v26: mworld > $o ).
thf(v21_type,type,
v21: mworld > $o ).
thf(sk__9_type,type,
sk__9: mworld > mworld ).
thf(mdia_type,type,
mdia: ( mworld > $o ) > mworld > $o ).
thf(mnot_type,type,
mnot: ( mworld > $o ) > mworld > $o ).
thf(v11_type,type,
v11: mworld > $o ).
thf(mlocal_type,type,
mlocal: ( mworld > $o ) > $o ).
thf(sk__20_type,type,
sk__20: mworld > mworld ).
thf(sk__35_type,type,
sk__35: mworld > mworld ).
thf(v7_type,type,
v7: mworld > $o ).
thf(v15_type,type,
v15: mworld > $o ).
thf(mrel_type,type,
mrel: mworld > mworld > $o ).
thf(sk__11_type,type,
sk__11: mworld > mworld ).
thf(sk__22_type,type,
sk__22: mworld > mworld ).
thf(v5_type,type,
v5: mworld > $o ).
thf(v12_type,type,
v12: mworld > $o ).
thf(v1_type,type,
v1: mworld > $o ).
thf(sk__8_type,type,
sk__8: mworld > mworld ).
thf(sk__25_type,type,
sk__25: mworld > mworld ).
thf(v6_type,type,
v6: mworld > $o ).
thf(mdia_def,axiom,
( mdia
= ( ^ [Phi: mworld > $o,W: mworld] :
? [V: mworld] :
( ( Phi @ V )
& ( mrel @ W @ V ) ) ) ) ).
thf('0',plain,
( mdia
= ( ^ [Phi: mworld > $o,W: mworld] :
? [V: mworld] :
( ( Phi @ V )
& ( mrel @ W @ V ) ) ) ),
inference(simplify_rw_rule,[status(thm)],[mdia_def]) ).
thf('1',plain,
( mdia
= ( ^ [V_1: mworld > $o,V_2: mworld] :
? [X4: mworld] :
( ( V_1 @ X4 )
& ( mrel @ V_2 @ X4 ) ) ) ),
define([status(thm)]) ).
thf(mbox_def,axiom,
( mbox
= ( ^ [Phi: mworld > $o,W: mworld] :
! [V: mworld] :
( ( mrel @ W @ V )
=> ( Phi @ V ) ) ) ) ).
thf('2',plain,
( mbox
= ( ^ [Phi: mworld > $o,W: mworld] :
! [V: mworld] :
( ( mrel @ W @ V )
=> ( Phi @ V ) ) ) ),
inference(simplify_rw_rule,[status(thm)],[mbox_def]) ).
thf('3',plain,
( mbox
= ( ^ [V_1: mworld > $o,V_2: mworld] :
! [X4: mworld] :
( ( mrel @ V_2 @ X4 )
=> ( V_1 @ X4 ) ) ) ),
define([status(thm)]) ).
thf(mand_def,axiom,
( mand
= ( ^ [A: mworld > $o,B: mworld > $o,W: mworld] :
( ( A @ W )
& ( B @ W ) ) ) ) ).
thf('4',plain,
( mand
= ( ^ [A: mworld > $o,B: mworld > $o,W: mworld] :
( ( A @ W )
& ( B @ W ) ) ) ),
inference(simplify_rw_rule,[status(thm)],[mand_def]) ).
thf('5',plain,
( mand
= ( ^ [V_1: mworld > $o,V_2: mworld > $o,V_3: mworld] :
( ( V_1 @ V_3 )
& ( V_2 @ V_3 ) ) ) ),
define([status(thm)]) ).
thf(mnot_def,axiom,
( mnot
= ( ^ [A: mworld > $o,W: mworld] :
~ ( A @ W ) ) ) ).
thf('6',plain,
( mnot
= ( ^ [A: mworld > $o,W: mworld] :
~ ( A @ W ) ) ),
inference(simplify_rw_rule,[status(thm)],[mnot_def]) ).
thf('7',plain,
( mnot
= ( ^ [V_1: mworld > $o,V_2: mworld] :
~ ( V_1 @ V_2 ) ) ),
define([status(thm)]) ).
thf(mlocal_def,axiom,
( mlocal
= ( ^ [Phi: mworld > $o] : ( Phi @ mactual ) ) ) ).
thf('8',plain,
( mlocal
= ( ^ [Phi: mworld > $o] : ( Phi @ mactual ) ) ),
inference(simplify_rw_rule,[status(thm)],[mlocal_def]) ).
thf('9',plain,
( mlocal
= ( ^ [V_1: mworld > $o] : ( V_1 @ mactual ) ) ),
define([status(thm)]) ).
thf(alt1,axiom,
( mlocal
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mand
@ ( mbox
@ ( mdia
@ ^ [W: mworld] : $true ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mand @ ( mdia @ v5 ) @ ( mdia @ ( mnot @ v5 ) ) ) ) )
@ ( mand @ ( mdia @ v6 ) @ ( mdia @ ( mnot @ v6 ) ) ) ) )
@ ( mand @ ( mdia @ v7 ) @ ( mdia @ ( mnot @ v7 ) ) ) ) )
@ ( mand @ ( mdia @ v8 ) @ ( mdia @ ( mnot @ v8 ) ) ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mand @ ( mdia @ v13 ) @ ( mdia @ ( mnot @ v13 ) ) ) ) )
@ ( mand @ ( mdia @ v14 ) @ ( mdia @ ( mnot @ v14 ) ) ) ) )
@ ( mand @ ( mdia @ v15 ) @ ( mdia @ ( mnot @ v15 ) ) ) ) )
@ ( mand @ ( mdia @ v16 ) @ ( mdia @ ( mnot @ v16 ) ) ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mand @ ( mdia @ v21 ) @ ( mdia @ ( mnot @ v21 ) ) ) ) )
@ ( mand @ ( mdia @ v22 ) @ ( mdia @ ( mnot @ v22 ) ) ) ) )
@ ( mand @ ( mdia @ v23 ) @ ( mdia @ ( mnot @ v23 ) ) ) ) )
@ ( mand @ ( mdia @ v24 ) @ ( mdia @ ( mnot @ v24 ) ) ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) )
@ ( mdia
@ ^ [W: mworld] : $true ) ) ) ).
thf(zf_stmt_0,axiom,
( ! [X4: mworld] :
( ( mrel @ mactual @ X4 )
=> ( ! [X6: mworld] :
( ( mrel @ X4 @ X6 )
=> ( ! [X8: mworld] :
( ( mrel @ X6 @ X8 )
=> ( ! [X10: mworld] :
( ( mrel @ X8 @ X10 )
=> ( ! [X12: mworld] :
( ( mrel @ X10 @ X12 )
=> ( ! [X14: mworld] :
( ( mrel @ X12 @ X14 )
=> ( ! [X16: mworld] :
( ( mrel @ X14 @ X16 )
=> ( ! [X18: mworld] :
( ( mrel @ X16 @ X18 )
=> ( ! [X20: mworld] :
( ( mrel @ X18 @ X20 )
=> ( ! [X22: mworld] :
( ( mrel @ X20 @ X22 )
=> ( ! [X24: mworld] :
( ( mrel @ X22 @ X24 )
=> ( ! [X26: mworld] :
( ( mrel @ X24 @ X26 )
=> ( ! [X28: mworld] :
( ( mrel @ X26 @ X28 )
=> ( ! [X30: mworld] :
( ( mrel @ X28 @ X30 )
=> ( ! [X32: mworld] :
( ( mrel @ X30 @ X32 )
=> ( ! [X34: mworld] :
( ( mrel @ X32 @ X34 )
=> ( ! [X36: mworld] :
( ( mrel @ X34 @ X36 )
=> ( ! [X38: mworld] :
( ( mrel @ X36 @ X38 )
=> ( ! [X40: mworld] :
( ( mrel @ X38 @ X40 )
=> ( ! [X42: mworld] :
( ( mrel @ X40 @ X42 )
=> ( ! [X44: mworld] :
( ( mrel @ X42 @ X44 )
=> ( ! [X46: mworld] :
( ( mrel @ X44 @ X46 )
=> ( ! [X48: mworld] :
( ( mrel @ X46 @ X48 )
=> ( ! [X50: mworld] :
( ( mrel @ X48 @ X50 )
=> ( ! [X52: mworld] :
( ( mrel @ X50 @ X52 )
=> ( ! [X54: mworld] :
( ( mrel @ X52 @ X54 )
=> ( ! [X56: mworld] :
( ( mrel @ X54 @ X56 )
=> ? [X58: mworld] : ( mrel @ X56 @ X58 ) )
& ? [X60: mworld] : ( mrel @ X54 @ X60 ) ) )
& ? [X62: mworld] : ( mrel @ X52 @ X62 ) ) )
& ? [X64: mworld] : ( mrel @ X50 @ X64 ) ) )
& ? [X66: mworld] :
( ( v5 @ X66 )
& ( mrel @ X48 @ X66 ) )
& ? [X68: mworld] :
( ~ ( v5 @ X68 )
& ( mrel @ X48 @ X68 ) ) ) )
& ? [X70: mworld] :
( ( v6 @ X70 )
& ( mrel @ X46 @ X70 ) )
& ? [X72: mworld] :
( ~ ( v6 @ X72 )
& ( mrel @ X46 @ X72 ) ) ) )
& ? [X74: mworld] :
( ( v7 @ X74 )
& ( mrel @ X44 @ X74 ) )
& ? [X76: mworld] :
( ~ ( v7 @ X76 )
& ( mrel @ X44 @ X76 ) ) ) )
& ? [X78: mworld] :
( ( v8 @ X78 )
& ( mrel @ X42 @ X78 ) )
& ? [X80: mworld] :
( ~ ( v8 @ X80 )
& ( mrel @ X42 @ X80 ) ) ) )
& ? [X82: mworld] : ( mrel @ X40 @ X82 ) ) )
& ? [X84: mworld] : ( mrel @ X38 @ X84 ) ) )
& ? [X86: mworld] : ( mrel @ X36 @ X86 ) ) )
& ? [X88: mworld] : ( mrel @ X34 @ X88 ) ) )
& ? [X90: mworld] :
( ( v13 @ X90 )
& ( mrel @ X32 @ X90 ) )
& ? [X92: mworld] :
( ~ ( v13 @ X92 )
& ( mrel @ X32 @ X92 ) ) ) )
& ? [X94: mworld] :
( ( v14 @ X94 )
& ( mrel @ X30 @ X94 ) )
& ? [X96: mworld] :
( ~ ( v14 @ X96 )
& ( mrel @ X30 @ X96 ) ) ) )
& ? [X98: mworld] :
( ( v15 @ X98 )
& ( mrel @ X28 @ X98 ) )
& ? [X100: mworld] :
( ~ ( v15 @ X100 )
& ( mrel @ X28 @ X100 ) ) ) )
& ? [X102: mworld] :
( ( v16 @ X102 )
& ( mrel @ X26 @ X102 ) )
& ? [X104: mworld] :
( ~ ( v16 @ X104 )
& ( mrel @ X26 @ X104 ) ) ) )
& ? [X106: mworld] : ( mrel @ X24 @ X106 ) ) )
& ? [X108: mworld] : ( mrel @ X22 @ X108 ) ) )
& ? [X110: mworld] : ( mrel @ X20 @ X110 ) ) )
& ? [X112: mworld] : ( mrel @ X18 @ X112 ) ) )
& ? [X114: mworld] :
( ( v21 @ X114 )
& ( mrel @ X16 @ X114 ) )
& ? [X116: mworld] :
( ~ ( v21 @ X116 )
& ( mrel @ X16 @ X116 ) ) ) )
& ? [X118: mworld] :
( ( v22 @ X118 )
& ( mrel @ X14 @ X118 ) )
& ? [X120: mworld] :
( ~ ( v22 @ X120 )
& ( mrel @ X14 @ X120 ) ) ) )
& ? [X122: mworld] :
( ( v23 @ X122 )
& ( mrel @ X12 @ X122 ) )
& ? [X124: mworld] :
( ~ ( v23 @ X124 )
& ( mrel @ X12 @ X124 ) ) ) )
& ? [X126: mworld] :
( ( v24 @ X126 )
& ( mrel @ X10 @ X126 ) )
& ? [X128: mworld] :
( ~ ( v24 @ X128 )
& ( mrel @ X10 @ X128 ) ) ) )
& ? [X130: mworld] : ( mrel @ X8 @ X130 ) ) )
& ? [X132: mworld] : ( mrel @ X6 @ X132 ) ) )
& ? [X134: mworld] : ( mrel @ X4 @ X134 ) ) )
& ? [X136: mworld] : ( mrel @ mactual @ X136 ) ) ).
thf(zip_derived_cl112,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( v23 @ ( sk__35 @ X4 ) )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(mrel_universal,axiom,
! [W: mworld,V: mworld] : ( mrel @ W @ V ) ).
thf(zip_derived_cl0,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_001,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_002,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_003,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_004,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl121,plain,
! [X4: mworld] :
~ ( v23 @ ( sk__35 @ X4 ) ),
inference(demod,[status(thm)],[zip_derived_cl112,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl79,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld,X20: mworld,X21: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ~ ( mrel @ X20 @ X21 )
| ( v6 @ ( sk__8 @ X21 ) )
| ~ ( mrel @ X19 @ X20 )
| ~ ( mrel @ X17 @ X18 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl0_005,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_006,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_007,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_008,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_009,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_010,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_011,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_012,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_013,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_014,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_015,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_016,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_017,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_018,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_019,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_020,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_021,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_022,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_023,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_024,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_025,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_026,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl198,plain,
! [X21: mworld] : ( v6 @ ( sk__8 @ X21 ) ),
inference(demod,[status(thm)],[zip_derived_cl79,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(mor_def,axiom,
( mor
= ( ^ [A: mworld > $o,B: mworld > $o,W: mworld] :
( ( A @ W )
| ( B @ W ) ) ) ) ).
thf('10',plain,
( mor
= ( ^ [A: mworld > $o,B: mworld > $o,W: mworld] :
( ( A @ W )
| ( B @ W ) ) ) ),
inference(simplify_rw_rule,[status(thm)],[mor_def]) ).
thf('11',plain,
( mor
= ( ^ [V_1: mworld > $o,V_2: mworld > $o,V_3: mworld] :
( ( V_1 @ V_3 )
| ( V_2 @ V_3 ) ) ) ),
define([status(thm)]) ).
thf(mod25,axiom,
mlocal @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v25 ) @ ( mbox @ ( mbox @ ( mor @ v23 @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v12 ) @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mnot @ v6 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zf_stmt_1,axiom,
! [X4: mworld] :
( ( mrel @ mactual @ X4 )
=> ! [X6: mworld] :
( ( mrel @ X4 @ X6 )
=> ! [X8: mworld] :
( ( mrel @ X6 @ X8 )
=> ! [X10: mworld] :
( ( mrel @ X8 @ X10 )
=> ( ~ ( v25 @ X10 )
| ! [X12: mworld] :
( ( mrel @ X10 @ X12 )
=> ! [X14: mworld] :
( ( mrel @ X12 @ X14 )
=> ( ( v23 @ X14 )
| ! [X16: mworld] :
( ( mrel @ X14 @ X16 )
=> ! [X18: mworld] :
( ( mrel @ X16 @ X18 )
=> ! [X20: mworld] :
( ( mrel @ X18 @ X20 )
=> ! [X22: mworld] :
( ( mrel @ X20 @ X22 )
=> ! [X24: mworld] :
( ( mrel @ X22 @ X24 )
=> ! [X26: mworld] :
( ( mrel @ X24 @ X26 )
=> ! [X28: mworld] :
( ( mrel @ X26 @ X28 )
=> ! [X30: mworld] :
( ( mrel @ X28 @ X30 )
=> ! [X32: mworld] :
( ( mrel @ X30 @ X32 )
=> ! [X34: mworld] :
( ( mrel @ X32 @ X34 )
=> ! [X36: mworld] :
( ( mrel @ X34 @ X36 )
=> ( ~ ( v12 @ X36 )
| ! [X38: mworld] :
( ( mrel @ X36 @ X38 )
=> ! [X40: mworld] :
( ( mrel @ X38 @ X40 )
=> ! [X42: mworld] :
( ( mrel @ X40 @ X42 )
=> ! [X44: mworld] :
( ( mrel @ X42 @ X44 )
=> ! [X46: mworld] :
( ( mrel @ X44 @ X46 )
=> ! [X48: mworld] :
( ( mrel @ X46 @ X48 )
=> ~ ( v6 @ X48 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl25,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld,X20: mworld,X21: mworld,X22: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( v25 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ( v23 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ~ ( mrel @ X20 @ X21 )
| ~ ( v6 @ X22 )
| ~ ( mrel @ X21 @ X22 )
| ~ ( mrel @ X19 @ X20 )
| ~ ( mrel @ X17 @ X18 )
| ~ ( v12 @ X16 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_1]) ).
thf(zip_derived_cl0_027,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_028,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_029,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_030,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_031,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_032,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_033,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_034,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_035,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_036,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_037,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_038,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_039,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_040,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_041,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_042,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_043,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_044,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_045,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_046,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_047,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_048,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_049,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl263,plain,
! [X3: mworld,X5: mworld,X16: mworld,X22: mworld] :
( ~ ( v25 @ X3 )
| ( v23 @ X5 )
| ~ ( v6 @ X22 )
| ~ ( v12 @ X16 ) ),
inference(demod,[status(thm)],[zip_derived_cl25,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl90,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld,X20: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ( v7 @ ( sk__10 @ X20 ) )
| ~ ( mrel @ X19 @ X20 )
| ~ ( mrel @ X17 @ X18 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl0_050,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_051,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_052,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_053,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_054,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_055,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_056,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_057,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_058,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_059,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_060,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_061,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_062,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_063,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_064,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_065,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_066,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_067,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_068,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_069,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_070,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl179,plain,
! [X20: mworld] : ( v7 @ ( sk__10 @ X20 ) ),
inference(demod,[status(thm)],[zip_derived_cl90,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl69,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ( v14 @ ( sk__20 @ X13 ) )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl0_071,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_072,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_073,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_074,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_075,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_076,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_077,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_078,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_079,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_080,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_081,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_082,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_083,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_084,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl152,plain,
! [X13: mworld] : ( v14 @ ( sk__20 @ X13 ) ),
inference(demod,[status(thm)],[zip_derived_cl69,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl75,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ( v8 @ ( sk__12 @ X19 ) )
| ~ ( mrel @ X17 @ X18 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl0_085,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_086,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_087,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_088,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_089,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_090,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_091,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_092,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_093,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_094,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_095,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_096,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_097,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_098,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_099,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_100,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_101,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_102,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_103,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_104,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl169,plain,
! [X19: mworld] : ( v8 @ ( sk__12 @ X19 ) ),
inference(demod,[status(thm)],[zip_derived_cl75,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(mod22,axiom,
mlocal @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ v25 @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ v20 @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v14 ) @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mnot @ v8 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zf_stmt_2,axiom,
! [X4: mworld] :
( ( mrel @ mactual @ X4 )
=> ! [X6: mworld] :
( ( mrel @ X4 @ X6 )
=> ! [X8: mworld] :
( ( mrel @ X6 @ X8 )
=> ! [X10: mworld] :
( ( mrel @ X8 @ X10 )
=> ( ( v25 @ X10 )
| ! [X12: mworld] :
( ( mrel @ X10 @ X12 )
=> ! [X14: mworld] :
( ( mrel @ X12 @ X14 )
=> ! [X16: mworld] :
( ( mrel @ X14 @ X16 )
=> ! [X18: mworld] :
( ( mrel @ X16 @ X18 )
=> ! [X20: mworld] :
( ( mrel @ X18 @ X20 )
=> ( ( v20 @ X20 )
| ! [X22: mworld] :
( ( mrel @ X20 @ X22 )
=> ! [X24: mworld] :
( ( mrel @ X22 @ X24 )
=> ! [X26: mworld] :
( ( mrel @ X24 @ X26 )
=> ! [X28: mworld] :
( ( mrel @ X26 @ X28 )
=> ! [X30: mworld] :
( ( mrel @ X28 @ X30 )
=> ! [X32: mworld] :
( ( mrel @ X30 @ X32 )
=> ( ~ ( v14 @ X32 )
| ! [X34: mworld] :
( ( mrel @ X32 @ X34 )
=> ! [X36: mworld] :
( ( mrel @ X34 @ X36 )
=> ! [X38: mworld] :
( ( mrel @ X36 @ X38 )
=> ! [X40: mworld] :
( ( mrel @ X38 @ X40 )
=> ! [X42: mworld] :
( ( mrel @ X40 @ X42 )
=> ! [X44: mworld] :
( ( mrel @ X42 @ X44 )
=> ~ ( v8 @ X44 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl22,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld,X20: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ( v25 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ~ ( v8 @ X20 )
| ~ ( mrel @ X19 @ X20 )
| ~ ( mrel @ X17 @ X18 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( v14 @ X14 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ( v20 @ X8 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_2]) ).
thf(zip_derived_cl0_105,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_106,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_107,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_108,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_109,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_110,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_111,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_112,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_113,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_114,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_115,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_116,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_117,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_118,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_119,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_120,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_121,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_122,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_123,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_124,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_125,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl219,plain,
! [X3: mworld,X8: mworld,X14: mworld,X20: mworld] :
( ( v25 @ X3 )
| ~ ( v8 @ X20 )
| ~ ( v14 @ X14 )
| ( v20 @ X8 ) ),
inference(demod,[status(thm)],[zip_derived_cl22,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl220,plain,
! [X1: mworld,X2: mworld,X3: mworld] :
( ( v20 @ X1 )
| ~ ( v14 @ X2 )
| ( v25 @ X3 ) ),
inference('sup-',[status(thm)],[zip_derived_cl169,zip_derived_cl219]) ).
thf(zip_derived_cl222,plain,
! [X1: mworld,X2: mworld] :
( ( v25 @ X1 )
| ( v20 @ X2 ) ),
inference('sup-',[status(thm)],[zip_derived_cl152,zip_derived_cl220]) ).
thf(zip_derived_cl55,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ( v24 @ ( sk__36 @ X3 ) )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl0_126,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_127,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_128,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_129,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl123,plain,
! [X3: mworld] : ( v24 @ ( sk__36 @ X3 ) ),
inference(demod,[status(thm)],[zip_derived_cl55,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl198_130,plain,
! [X21: mworld] : ( v6 @ ( sk__8 @ X21 ) ),
inference(demod,[status(thm)],[zip_derived_cl79,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(mod30,axiom,
mlocal @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v24 ) @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v20 ) @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v6 ) @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ v1 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zf_stmt_3,axiom,
! [X4: mworld] :
( ( mrel @ mactual @ X4 )
=> ! [X6: mworld] :
( ( mrel @ X4 @ X6 )
=> ! [X8: mworld] :
( ( mrel @ X6 @ X8 )
=> ! [X10: mworld] :
( ( mrel @ X8 @ X10 )
=> ! [X12: mworld] :
( ( mrel @ X10 @ X12 )
=> ( ~ ( v24 @ X12 )
| ! [X14: mworld] :
( ( mrel @ X12 @ X14 )
=> ! [X16: mworld] :
( ( mrel @ X14 @ X16 )
=> ! [X18: mworld] :
( ( mrel @ X16 @ X18 )
=> ! [X20: mworld] :
( ( mrel @ X18 @ X20 )
=> ( ~ ( v20 @ X20 )
| ! [X22: mworld] :
( ( mrel @ X20 @ X22 )
=> ! [X24: mworld] :
( ( mrel @ X22 @ X24 )
=> ! [X26: mworld] :
( ( mrel @ X24 @ X26 )
=> ! [X28: mworld] :
( ( mrel @ X26 @ X28 )
=> ! [X30: mworld] :
( ( mrel @ X28 @ X30 )
=> ! [X32: mworld] :
( ( mrel @ X30 @ X32 )
=> ! [X34: mworld] :
( ( mrel @ X32 @ X34 )
=> ! [X36: mworld] :
( ( mrel @ X34 @ X36 )
=> ! [X38: mworld] :
( ( mrel @ X36 @ X38 )
=> ! [X40: mworld] :
( ( mrel @ X38 @ X40 )
=> ! [X42: mworld] :
( ( mrel @ X40 @ X42 )
=> ! [X44: mworld] :
( ( mrel @ X42 @ X44 )
=> ! [X46: mworld] :
( ( mrel @ X44 @ X46 )
=> ! [X48: mworld] :
( ( mrel @ X46 @ X48 )
=> ( ~ ( v6 @ X48 )
| ! [X50: mworld] :
( ( mrel @ X48 @ X50 )
=> ! [X52: mworld] :
( ( mrel @ X50 @ X52 )
=> ! [X54: mworld] :
( ( mrel @ X52 @ X54 )
=> ! [X56: mworld] :
( ( mrel @ X54 @ X56 )
=> ! [X58: mworld] :
( ( mrel @ X56 @ X58 )
=> ( v1 @ X58 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl30,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld,X20: mworld,X21: mworld,X22: mworld,X23: mworld,X24: mworld,X25: mworld,X26: mworld,X27: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ~ ( mrel @ X20 @ X21 )
| ~ ( mrel @ X22 @ X23 )
| ~ ( mrel @ X24 @ X25 )
| ~ ( mrel @ X26 @ X27 )
| ( v1 @ X27 )
| ~ ( mrel @ X25 @ X26 )
| ~ ( mrel @ X23 @ X24 )
| ~ ( v6 @ X22 )
| ~ ( mrel @ X21 @ X22 )
| ~ ( mrel @ X19 @ X20 )
| ~ ( mrel @ X17 @ X18 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( v20 @ X8 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( v24 @ X4 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_3]) ).
thf(zip_derived_cl0_131,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_132,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_133,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_134,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_135,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_136,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_137,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_138,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_139,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_140,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_141,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_142,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_143,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_144,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_145,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_146,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_147,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_148,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_149,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_150,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_151,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_152,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_153,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_154,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_155,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_156,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_157,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_158,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl335,plain,
! [X4: mworld,X8: mworld,X22: mworld,X27: mworld] :
( ( v1 @ X27 )
| ~ ( v6 @ X22 )
| ~ ( v20 @ X8 )
| ~ ( v24 @ X4 ) ),
inference(demod,[status(thm)],[zip_derived_cl30,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl336,plain,
! [X1: mworld,X2: mworld,X3: mworld] :
( ~ ( v24 @ X1 )
| ~ ( v20 @ X2 )
| ( v1 @ X3 ) ),
inference('sup-',[status(thm)],[zip_derived_cl198,zip_derived_cl335]) ).
thf(zip_derived_cl345,plain,
! [X1: mworld,X2: mworld] :
( ( v1 @ X1 )
| ~ ( v20 @ X2 ) ),
inference('sup-',[status(thm)],[zip_derived_cl123,zip_derived_cl336]) ).
thf(zip_derived_cl347,plain,
! [X1: mworld,X2: mworld] :
( ( v25 @ X2 )
| ( v1 @ X1 ) ),
inference('sup-',[status(thm)],[zip_derived_cl222,zip_derived_cl345]) ).
thf(zip_derived_cl100,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ( v15 @ ( sk__22 @ X12 ) )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl0_159,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_160,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_161,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_162,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_163,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_164,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_165,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_166,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_167,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_168,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_169,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_170,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_171,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl148,plain,
! [X12: mworld] : ( v15 @ ( sk__22 @ X12 ) ),
inference(demod,[status(thm)],[zip_derived_cl100,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(mod45,axiom,
mlocal @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v15 ) @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v11 ) @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v7 ) @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zf_stmt_4,axiom,
! [X4: mworld] :
( ( mrel @ mactual @ X4 )
=> ! [X6: mworld] :
( ( mrel @ X4 @ X6 )
=> ! [X8: mworld] :
( ( mrel @ X6 @ X8 )
=> ! [X10: mworld] :
( ( mrel @ X8 @ X10 )
=> ! [X12: mworld] :
( ( mrel @ X10 @ X12 )
=> ! [X14: mworld] :
( ( mrel @ X12 @ X14 )
=> ! [X16: mworld] :
( ( mrel @ X14 @ X16 )
=> ! [X18: mworld] :
( ( mrel @ X16 @ X18 )
=> ! [X20: mworld] :
( ( mrel @ X18 @ X20 )
=> ! [X22: mworld] :
( ( mrel @ X20 @ X22 )
=> ! [X24: mworld] :
( ( mrel @ X22 @ X24 )
=> ! [X26: mworld] :
( ( mrel @ X24 @ X26 )
=> ! [X28: mworld] :
( ( mrel @ X26 @ X28 )
=> ! [X30: mworld] :
( ( mrel @ X28 @ X30 )
=> ( ~ ( v15 @ X30 )
| ! [X32: mworld] :
( ( mrel @ X30 @ X32 )
=> ! [X34: mworld] :
( ( mrel @ X32 @ X34 )
=> ! [X36: mworld] :
( ( mrel @ X34 @ X36 )
=> ! [X38: mworld] :
( ( mrel @ X36 @ X38 )
=> ( ~ ( v11 @ X38 )
| ! [X40: mworld] :
( ( mrel @ X38 @ X40 )
=> ! [X42: mworld] :
( ( mrel @ X40 @ X42 )
=> ! [X44: mworld] :
( ( mrel @ X42 @ X44 )
=> ! [X46: mworld] :
( ( mrel @ X44 @ X46 )
=> ( ~ ( v7 @ X46 )
| ! [X48: mworld] :
( ( mrel @ X46 @ X48 )
=> ! [X50: mworld] :
( ( mrel @ X48 @ X50 )
=> ! [X52: mworld] :
( ( mrel @ X50 @ X52 )
=> ! [X54: mworld] :
( ( mrel @ X52 @ X54 )
=> ! [X56: mworld] :
( ( mrel @ X54 @ X56 )
=> ! [X58: mworld] :
( ( mrel @ X56 @ X58 )
=> ~ ( v1 @ X58 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl45,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld,X20: mworld,X21: mworld,X22: mworld,X23: mworld,X24: mworld,X25: mworld,X26: mworld,X27: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( v15 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ~ ( v11 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ~ ( mrel @ X20 @ X21 )
| ~ ( v7 @ X21 )
| ~ ( mrel @ X22 @ X23 )
| ~ ( mrel @ X24 @ X25 )
| ~ ( mrel @ X26 @ X27 )
| ~ ( v1 @ X27 )
| ~ ( mrel @ X25 @ X26 )
| ~ ( mrel @ X23 @ X24 )
| ~ ( mrel @ X21 @ X22 )
| ~ ( mrel @ X19 @ X20 )
| ~ ( mrel @ X17 @ X18 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_4]) ).
thf(zip_derived_cl0_172,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_173,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_174,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_175,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_176,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_177,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_178,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_179,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_180,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_181,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_182,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_183,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_184,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_185,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_186,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_187,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_188,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_189,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_190,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_191,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_192,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_193,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_194,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_195,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_196,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_197,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_198,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_199,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl310,plain,
! [X13: mworld,X17: mworld,X21: mworld,X27: mworld] :
( ~ ( v15 @ X13 )
| ~ ( v11 @ X17 )
| ~ ( v7 @ X21 )
| ~ ( v1 @ X27 ) ),
inference(demod,[status(thm)],[zip_derived_cl45,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl311,plain,
! [X1: mworld,X2: mworld,X3: mworld] :
( ~ ( v1 @ X1 )
| ~ ( v7 @ X2 )
| ~ ( v11 @ X3 ) ),
inference('sup-',[status(thm)],[zip_derived_cl148,zip_derived_cl310]) ).
thf(zip_derived_cl414,plain,
! [X1: mworld,X2: mworld,X3: mworld] :
( ( v25 @ X3 )
| ~ ( v11 @ X1 )
| ~ ( v7 @ X2 ) ),
inference('sup-',[status(thm)],[zip_derived_cl347,zip_derived_cl311]) ).
thf(zip_derived_cl123_200,plain,
! [X3: mworld] : ( v24 @ ( sk__36 @ X3 ) ),
inference(demod,[status(thm)],[zip_derived_cl55,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(mod18,axiom,
mlocal @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ v25 @ ( mbox @ ( mor @ ( mnot @ v24 ) @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ v16 @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ v11 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zf_stmt_5,axiom,
! [X4: mworld] :
( ( mrel @ mactual @ X4 )
=> ! [X6: mworld] :
( ( mrel @ X4 @ X6 )
=> ! [X8: mworld] :
( ( mrel @ X6 @ X8 )
=> ! [X10: mworld] :
( ( mrel @ X8 @ X10 )
=> ( ( v25 @ X10 )
| ! [X12: mworld] :
( ( mrel @ X10 @ X12 )
=> ( ~ ( v24 @ X12 )
| ! [X14: mworld] :
( ( mrel @ X12 @ X14 )
=> ! [X16: mworld] :
( ( mrel @ X14 @ X16 )
=> ! [X18: mworld] :
( ( mrel @ X16 @ X18 )
=> ! [X20: mworld] :
( ( mrel @ X18 @ X20 )
=> ! [X22: mworld] :
( ( mrel @ X20 @ X22 )
=> ! [X24: mworld] :
( ( mrel @ X22 @ X24 )
=> ! [X26: mworld] :
( ( mrel @ X24 @ X26 )
=> ! [X28: mworld] :
( ( mrel @ X26 @ X28 )
=> ( ( v16 @ X28 )
| ! [X30: mworld] :
( ( mrel @ X28 @ X30 )
=> ! [X32: mworld] :
( ( mrel @ X30 @ X32 )
=> ! [X34: mworld] :
( ( mrel @ X32 @ X34 )
=> ! [X36: mworld] :
( ( mrel @ X34 @ X36 )
=> ! [X38: mworld] :
( ( mrel @ X36 @ X38 )
=> ( v11 @ X38 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl18,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ( v25 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ( v11 @ X17 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( mrel @ X13 @ X14 )
| ( v16 @ X12 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( v24 @ X4 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_5]) ).
thf(zip_derived_cl0_201,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_202,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_203,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_204,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_205,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_206,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_207,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_208,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_209,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_210,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_211,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_212,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_213,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_214,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_215,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_216,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_217,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_218,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl174,plain,
! [X3: mworld,X4: mworld,X12: mworld,X17: mworld] :
( ( v25 @ X3 )
| ( v11 @ X17 )
| ( v16 @ X12 )
| ~ ( v24 @ X4 ) ),
inference(demod,[status(thm)],[zip_derived_cl18,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl175,plain,
! [X1: mworld,X2: mworld,X3: mworld] :
( ( v16 @ X1 )
| ( v11 @ X2 )
| ( v25 @ X3 ) ),
inference('sup-',[status(thm)],[zip_derived_cl123,zip_derived_cl174]) ).
thf(zip_derived_cl63,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( v16 @ ( sk__25 @ X11 ) )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl0_219,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_220,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_221,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_222,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_223,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_224,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_225,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_226,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_227,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_228,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_229,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_230,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl142,plain,
! [X11: mworld] :
~ ( v16 @ ( sk__25 @ X11 ) ),
inference(demod,[status(thm)],[zip_derived_cl63,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl190,plain,
! [X1: mworld,X2: mworld] :
( ( v25 @ X1 )
| ( v11 @ X2 ) ),
inference('sup-',[status(thm)],[zip_derived_cl175,zip_derived_cl142]) ).
thf(zip_derived_cl429,plain,
! [X2: mworld,X3: mworld] :
( ~ ( v7 @ X2 )
| ( v25 @ X3 ) ),
inference(clc,[status(thm)],[zip_derived_cl414,zip_derived_cl190]) ).
thf(zip_derived_cl430,plain,
! [X1: mworld] : ( v25 @ X1 ),
inference('sup-',[status(thm)],[zip_derived_cl179,zip_derived_cl429]) ).
thf(zip_derived_cl435,plain,
! [X5: mworld,X16: mworld,X22: mworld] :
( ( v23 @ X5 )
| ~ ( v6 @ X22 )
| ~ ( v12 @ X16 ) ),
inference(demod,[status(thm)],[zip_derived_cl263,zip_derived_cl430]) ).
thf(zip_derived_cl456,plain,
! [X1: mworld,X2: mworld] :
( ~ ( v12 @ X1 )
| ( v23 @ X2 ) ),
inference('sup-',[status(thm)],[zip_derived_cl198,zip_derived_cl435]) ).
thf(zip_derived_cl179_231,plain,
! [X20: mworld] : ( v7 @ ( sk__10 @ X20 ) ),
inference(demod,[status(thm)],[zip_derived_cl90,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl169_232,plain,
! [X19: mworld] : ( v8 @ ( sk__12 @ X19 ) ),
inference(demod,[status(thm)],[zip_derived_cl75,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl152_233,plain,
! [X13: mworld] : ( v14 @ ( sk__20 @ X13 ) ),
inference(demod,[status(thm)],[zip_derived_cl69,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl86,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld,X20: mworld,X21: mworld,X22: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ~ ( mrel @ X20 @ X21 )
| ( v5 @ ( sk__6 @ X22 ) )
| ~ ( mrel @ X21 @ X22 )
| ~ ( mrel @ X19 @ X20 )
| ~ ( mrel @ X17 @ X18 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl0_234,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_235,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_236,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_237,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_238,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_239,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_240,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_241,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_242,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_243,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_244,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_245,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_246,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_247,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_248,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_249,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_250,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_251,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_252,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_253,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_254,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_255,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_256,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl216,plain,
! [X22: mworld] : ( v5 @ ( sk__6 @ X22 ) ),
inference(demod,[status(thm)],[zip_derived_cl86,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(mod11,axiom,
mlocal @ ( mbox @ ( mbox @ ( mbox @ ( mor @ v26 @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v14 ) @ ( mbox @ ( mbox @ ( mor @ v12 @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mnot @ v5 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zf_stmt_6,axiom,
! [X4: mworld] :
( ( mrel @ mactual @ X4 )
=> ! [X6: mworld] :
( ( mrel @ X4 @ X6 )
=> ! [X8: mworld] :
( ( mrel @ X6 @ X8 )
=> ( ( v26 @ X8 )
| ! [X10: mworld] :
( ( mrel @ X8 @ X10 )
=> ! [X12: mworld] :
( ( mrel @ X10 @ X12 )
=> ! [X14: mworld] :
( ( mrel @ X12 @ X14 )
=> ! [X16: mworld] :
( ( mrel @ X14 @ X16 )
=> ! [X18: mworld] :
( ( mrel @ X16 @ X18 )
=> ! [X20: mworld] :
( ( mrel @ X18 @ X20 )
=> ! [X22: mworld] :
( ( mrel @ X20 @ X22 )
=> ! [X24: mworld] :
( ( mrel @ X22 @ X24 )
=> ! [X26: mworld] :
( ( mrel @ X24 @ X26 )
=> ! [X28: mworld] :
( ( mrel @ X26 @ X28 )
=> ! [X30: mworld] :
( ( mrel @ X28 @ X30 )
=> ! [X32: mworld] :
( ( mrel @ X30 @ X32 )
=> ( ~ ( v14 @ X32 )
| ! [X34: mworld] :
( ( mrel @ X32 @ X34 )
=> ! [X36: mworld] :
( ( mrel @ X34 @ X36 )
=> ( ( v12 @ X36 )
| ! [X38: mworld] :
( ( mrel @ X36 @ X38 )
=> ! [X40: mworld] :
( ( mrel @ X38 @ X40 )
=> ! [X42: mworld] :
( ( mrel @ X40 @ X42 )
=> ! [X44: mworld] :
( ( mrel @ X42 @ X44 )
=> ! [X46: mworld] :
( ( mrel @ X44 @ X46 )
=> ! [X48: mworld] :
( ( mrel @ X46 @ X48 )
=> ! [X50: mworld] :
( ( mrel @ X48 @ X50 )
=> ~ ( v5 @ X50 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl11,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld,X20: mworld,X21: mworld,X22: mworld,X23: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ~ ( mrel @ X20 @ X21 )
| ~ ( mrel @ X22 @ X23 )
| ~ ( v5 @ X23 )
| ~ ( mrel @ X21 @ X22 )
| ~ ( mrel @ X19 @ X20 )
| ~ ( mrel @ X17 @ X18 )
| ( v12 @ X16 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( v14 @ X14 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ( v26 @ X2 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_6]) ).
thf(zip_derived_cl0_257,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_258,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_259,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_260,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_261,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_262,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_263,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_264,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_265,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_266,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_267,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_268,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_269,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_270,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_271,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_272,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_273,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_274,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_275,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_276,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_277,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_278,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_279,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_280,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl255,plain,
! [X2: mworld,X14: mworld,X16: mworld,X23: mworld] :
( ~ ( v5 @ X23 )
| ( v12 @ X16 )
| ~ ( v14 @ X14 )
| ( v26 @ X2 ) ),
inference(demod,[status(thm)],[zip_derived_cl11,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl256,plain,
! [X1: mworld,X2: mworld,X3: mworld] :
( ( v26 @ X1 )
| ~ ( v14 @ X2 )
| ( v12 @ X3 ) ),
inference('sup-',[status(thm)],[zip_derived_cl216,zip_derived_cl255]) ).
thf(zip_derived_cl279,plain,
! [X1: mworld,X2: mworld] :
( ( v12 @ X1 )
| ( v26 @ X2 ) ),
inference('sup-',[status(thm)],[zip_derived_cl152,zip_derived_cl256]) ).
thf(zip_derived_cl179_281,plain,
! [X20: mworld] : ( v7 @ ( sk__10 @ X20 ) ),
inference(demod,[status(thm)],[zip_derived_cl90,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(mod17,axiom,
mlocal @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v26 ) @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v8 ) @ ( mbox @ ( mor @ ( mnot @ v7 ) @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ v1 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zf_stmt_7,axiom,
! [X4: mworld] :
( ( mrel @ mactual @ X4 )
=> ! [X6: mworld] :
( ( mrel @ X4 @ X6 )
=> ! [X8: mworld] :
( ( mrel @ X6 @ X8 )
=> ( ~ ( v26 @ X8 )
| ! [X10: mworld] :
( ( mrel @ X8 @ X10 )
=> ! [X12: mworld] :
( ( mrel @ X10 @ X12 )
=> ! [X14: mworld] :
( ( mrel @ X12 @ X14 )
=> ! [X16: mworld] :
( ( mrel @ X14 @ X16 )
=> ! [X18: mworld] :
( ( mrel @ X16 @ X18 )
=> ! [X20: mworld] :
( ( mrel @ X18 @ X20 )
=> ! [X22: mworld] :
( ( mrel @ X20 @ X22 )
=> ! [X24: mworld] :
( ( mrel @ X22 @ X24 )
=> ! [X26: mworld] :
( ( mrel @ X24 @ X26 )
=> ! [X28: mworld] :
( ( mrel @ X26 @ X28 )
=> ! [X30: mworld] :
( ( mrel @ X28 @ X30 )
=> ! [X32: mworld] :
( ( mrel @ X30 @ X32 )
=> ! [X34: mworld] :
( ( mrel @ X32 @ X34 )
=> ! [X36: mworld] :
( ( mrel @ X34 @ X36 )
=> ! [X38: mworld] :
( ( mrel @ X36 @ X38 )
=> ! [X40: mworld] :
( ( mrel @ X38 @ X40 )
=> ! [X42: mworld] :
( ( mrel @ X40 @ X42 )
=> ! [X44: mworld] :
( ( mrel @ X42 @ X44 )
=> ( ~ ( v8 @ X44 )
| ! [X46: mworld] :
( ( mrel @ X44 @ X46 )
=> ( ~ ( v7 @ X46 )
| ! [X48: mworld] :
( ( mrel @ X46 @ X48 )
=> ! [X50: mworld] :
( ( mrel @ X48 @ X50 )
=> ! [X52: mworld] :
( ( mrel @ X50 @ X52 )
=> ! [X54: mworld] :
( ( mrel @ X52 @ X54 )
=> ! [X56: mworld] :
( ( mrel @ X54 @ X56 )
=> ! [X58: mworld] :
( ( mrel @ X56 @ X58 )
=> ( v1 @ X58 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl17,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld,X20: mworld,X21: mworld,X22: mworld,X23: mworld,X24: mworld,X25: mworld,X26: mworld,X27: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ~ ( mrel @ X20 @ X21 )
| ~ ( v7 @ X21 )
| ~ ( mrel @ X22 @ X23 )
| ~ ( mrel @ X24 @ X25 )
| ~ ( mrel @ X26 @ X27 )
| ( v1 @ X27 )
| ~ ( mrel @ X25 @ X26 )
| ~ ( mrel @ X23 @ X24 )
| ~ ( mrel @ X21 @ X22 )
| ~ ( v8 @ X20 )
| ~ ( mrel @ X19 @ X20 )
| ~ ( mrel @ X17 @ X18 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( v26 @ X2 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_7]) ).
thf(zip_derived_cl0_282,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_283,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_284,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_285,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_286,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_287,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_288,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_289,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_290,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_291,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_292,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_293,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_294,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_295,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_296,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_297,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_298,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_299,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_300,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_301,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_302,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_303,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_304,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_305,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_306,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_307,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_308,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_309,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl332,plain,
! [X2: mworld,X20: mworld,X21: mworld,X27: mworld] :
( ~ ( v7 @ X21 )
| ( v1 @ X27 )
| ~ ( v8 @ X20 )
| ~ ( v26 @ X2 ) ),
inference(demod,[status(thm)],[zip_derived_cl17,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl333,plain,
! [X1: mworld,X2: mworld,X3: mworld] :
( ~ ( v26 @ X1 )
| ~ ( v8 @ X2 )
| ( v1 @ X3 ) ),
inference('sup-',[status(thm)],[zip_derived_cl179,zip_derived_cl332]) ).
thf(zip_derived_cl389,plain,
! [X1: mworld,X2: mworld,X3: mworld] :
( ( v12 @ X3 )
| ( v1 @ X1 )
| ~ ( v8 @ X2 ) ),
inference('sup-',[status(thm)],[zip_derived_cl279,zip_derived_cl333]) ).
thf(zip_derived_cl403,plain,
! [X1: mworld,X2: mworld] :
( ( v1 @ X1 )
| ( v12 @ X2 ) ),
inference('sup-',[status(thm)],[zip_derived_cl169,zip_derived_cl389]) ).
thf(zip_derived_cl311_310,plain,
! [X1: mworld,X2: mworld,X3: mworld] :
( ~ ( v1 @ X1 )
| ~ ( v7 @ X2 )
| ~ ( v11 @ X3 ) ),
inference('sup-',[status(thm)],[zip_derived_cl148,zip_derived_cl310]) ).
thf(mod50,axiom,
mlocal @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ v11 @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ v7 @ ( mbox @ ( mor @ v6 @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ v1 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zf_stmt_8,axiom,
! [X4: mworld] :
( ( mrel @ mactual @ X4 )
=> ! [X6: mworld] :
( ( mrel @ X4 @ X6 )
=> ! [X8: mworld] :
( ( mrel @ X6 @ X8 )
=> ! [X10: mworld] :
( ( mrel @ X8 @ X10 )
=> ! [X12: mworld] :
( ( mrel @ X10 @ X12 )
=> ! [X14: mworld] :
( ( mrel @ X12 @ X14 )
=> ! [X16: mworld] :
( ( mrel @ X14 @ X16 )
=> ! [X18: mworld] :
( ( mrel @ X16 @ X18 )
=> ! [X20: mworld] :
( ( mrel @ X18 @ X20 )
=> ! [X22: mworld] :
( ( mrel @ X20 @ X22 )
=> ! [X24: mworld] :
( ( mrel @ X22 @ X24 )
=> ! [X26: mworld] :
( ( mrel @ X24 @ X26 )
=> ! [X28: mworld] :
( ( mrel @ X26 @ X28 )
=> ! [X30: mworld] :
( ( mrel @ X28 @ X30 )
=> ! [X32: mworld] :
( ( mrel @ X30 @ X32 )
=> ! [X34: mworld] :
( ( mrel @ X32 @ X34 )
=> ! [X36: mworld] :
( ( mrel @ X34 @ X36 )
=> ! [X38: mworld] :
( ( mrel @ X36 @ X38 )
=> ( ( v11 @ X38 )
| ! [X40: mworld] :
( ( mrel @ X38 @ X40 )
=> ! [X42: mworld] :
( ( mrel @ X40 @ X42 )
=> ! [X44: mworld] :
( ( mrel @ X42 @ X44 )
=> ! [X46: mworld] :
( ( mrel @ X44 @ X46 )
=> ( ( v7 @ X46 )
| ! [X48: mworld] :
( ( mrel @ X46 @ X48 )
=> ( ( v6 @ X48 )
| ! [X50: mworld] :
( ( mrel @ X48 @ X50 )
=> ! [X52: mworld] :
( ( mrel @ X50 @ X52 )
=> ! [X54: mworld] :
( ( mrel @ X52 @ X54 )
=> ! [X56: mworld] :
( ( mrel @ X54 @ X56 )
=> ! [X58: mworld] :
( ( mrel @ X56 @ X58 )
=> ( v1 @ X58 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl50,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld,X20: mworld,X21: mworld,X22: mworld,X23: mworld,X24: mworld,X25: mworld,X26: mworld,X27: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ( v11 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ~ ( mrel @ X20 @ X21 )
| ( v7 @ X21 )
| ~ ( mrel @ X22 @ X23 )
| ~ ( mrel @ X24 @ X25 )
| ~ ( mrel @ X26 @ X27 )
| ( v1 @ X27 )
| ~ ( mrel @ X25 @ X26 )
| ~ ( mrel @ X23 @ X24 )
| ( v6 @ X22 )
| ~ ( mrel @ X21 @ X22 )
| ~ ( mrel @ X19 @ X20 )
| ~ ( mrel @ X17 @ X18 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_8]) ).
thf(zip_derived_cl0_311,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_312,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_313,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_314,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_315,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_316,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_317,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_318,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_319,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_320,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_321,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_322,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_323,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_324,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_325,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_326,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_327,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_328,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_329,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_330,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_331,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_332,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_333,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_334,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_335,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_336,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_337,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_338,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl377,plain,
! [X17: mworld,X21: mworld,X22: mworld,X27: mworld] :
( ( v11 @ X17 )
| ( v7 @ X21 )
| ( v1 @ X27 )
| ( v6 @ X22 ) ),
inference(demod,[status(thm)],[zip_derived_cl50,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl169_339,plain,
! [X19: mworld] : ( v8 @ ( sk__12 @ X19 ) ),
inference(demod,[status(thm)],[zip_derived_cl75,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl216_340,plain,
! [X22: mworld] : ( v5 @ ( sk__6 @ X22 ) ),
inference(demod,[status(thm)],[zip_derived_cl86,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(mod49,axiom,
mlocal @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mor @ v11 @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v8 ) @ ( mbox @ ( mbox @ ( mbox @ ( mor @ ( mnot @ v5 ) @ ( mbox @ ( mbox @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zf_stmt_9,axiom,
! [X4: mworld] :
( ( mrel @ mactual @ X4 )
=> ! [X6: mworld] :
( ( mrel @ X4 @ X6 )
=> ! [X8: mworld] :
( ( mrel @ X6 @ X8 )
=> ! [X10: mworld] :
( ( mrel @ X8 @ X10 )
=> ! [X12: mworld] :
( ( mrel @ X10 @ X12 )
=> ! [X14: mworld] :
( ( mrel @ X12 @ X14 )
=> ! [X16: mworld] :
( ( mrel @ X14 @ X16 )
=> ! [X18: mworld] :
( ( mrel @ X16 @ X18 )
=> ! [X20: mworld] :
( ( mrel @ X18 @ X20 )
=> ! [X22: mworld] :
( ( mrel @ X20 @ X22 )
=> ! [X24: mworld] :
( ( mrel @ X22 @ X24 )
=> ! [X26: mworld] :
( ( mrel @ X24 @ X26 )
=> ! [X28: mworld] :
( ( mrel @ X26 @ X28 )
=> ! [X30: mworld] :
( ( mrel @ X28 @ X30 )
=> ! [X32: mworld] :
( ( mrel @ X30 @ X32 )
=> ! [X34: mworld] :
( ( mrel @ X32 @ X34 )
=> ! [X36: mworld] :
( ( mrel @ X34 @ X36 )
=> ! [X38: mworld] :
( ( mrel @ X36 @ X38 )
=> ( ( v11 @ X38 )
| ! [X40: mworld] :
( ( mrel @ X38 @ X40 )
=> ! [X42: mworld] :
( ( mrel @ X40 @ X42 )
=> ! [X44: mworld] :
( ( mrel @ X42 @ X44 )
=> ( ~ ( v8 @ X44 )
| ! [X46: mworld] :
( ( mrel @ X44 @ X46 )
=> ! [X48: mworld] :
( ( mrel @ X46 @ X48 )
=> ! [X50: mworld] :
( ( mrel @ X48 @ X50 )
=> ( ~ ( v5 @ X50 )
| ! [X52: mworld] :
( ( mrel @ X50 @ X52 )
=> ! [X54: mworld] :
( ( mrel @ X52 @ X54 )
=> ! [X56: mworld] :
( ( mrel @ X54 @ X56 )
=> ! [X58: mworld] :
( ( mrel @ X56 @ X58 )
=> ~ ( v1 @ X58 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl49,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld,X20: mworld,X21: mworld,X22: mworld,X23: mworld,X24: mworld,X25: mworld,X26: mworld,X27: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ( v11 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ~ ( mrel @ X20 @ X21 )
| ~ ( mrel @ X22 @ X23 )
| ~ ( v5 @ X23 )
| ~ ( mrel @ X24 @ X25 )
| ~ ( mrel @ X26 @ X27 )
| ~ ( v1 @ X27 )
| ~ ( mrel @ X25 @ X26 )
| ~ ( mrel @ X23 @ X24 )
| ~ ( mrel @ X21 @ X22 )
| ~ ( v8 @ X20 )
| ~ ( mrel @ X19 @ X20 )
| ~ ( mrel @ X17 @ X18 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_9]) ).
thf(zip_derived_cl0_341,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_342,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_343,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_344,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_345,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_346,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_347,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_348,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_349,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_350,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_351,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_352,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_353,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_354,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_355,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_356,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_357,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_358,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_359,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_360,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_361,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_362,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_363,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_364,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_365,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_366,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_367,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_368,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl341,plain,
! [X17: mworld,X20: mworld,X23: mworld,X27: mworld] :
( ( v11 @ X17 )
| ~ ( v5 @ X23 )
| ~ ( v1 @ X27 )
| ~ ( v8 @ X20 ) ),
inference(demod,[status(thm)],[zip_derived_cl49,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl342,plain,
! [X1: mworld,X2: mworld,X3: mworld] :
( ~ ( v8 @ X1 )
| ~ ( v1 @ X2 )
| ( v11 @ X3 ) ),
inference('sup-',[status(thm)],[zip_derived_cl216,zip_derived_cl341]) ).
thf(zip_derived_cl373,plain,
! [X1: mworld,X2: mworld] :
( ( v11 @ X1 )
| ~ ( v1 @ X2 ) ),
inference('sup-',[status(thm)],[zip_derived_cl169,zip_derived_cl342]) ).
thf(zip_derived_cl378,plain,
! [X17: mworld,X21: mworld,X22: mworld] :
( ( v6 @ X22 )
| ( v7 @ X21 )
| ( v11 @ X17 ) ),
inference(clc,[status(thm)],[zip_derived_cl377,zip_derived_cl373]) ).
thf(zip_derived_cl92,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld,X20: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ~ ( v7 @ ( sk__11 @ X20 ) )
| ~ ( mrel @ X19 @ X20 )
| ~ ( mrel @ X17 @ X18 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl0_369,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_370,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_371,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_372,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_373,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_374,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_375,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_376,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_377,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_378,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_379,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_380,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_381,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_382,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_383,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_384,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_385,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_386,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_387,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_388,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_389,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl165,plain,
! [X20: mworld] :
~ ( v7 @ ( sk__11 @ X20 ) ),
inference(demod,[status(thm)],[zip_derived_cl92,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl380,plain,
! [X1: mworld,X2: mworld] :
( ( v11 @ X1 )
| ( v6 @ X2 ) ),
inference('sup-',[status(thm)],[zip_derived_cl378,zip_derived_cl165]) ).
thf(zip_derived_cl77,plain,
! [X0: mworld,X1: mworld,X2: mworld,X3: mworld,X4: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld,X9: mworld,X10: mworld,X11: mworld,X12: mworld,X13: mworld,X14: mworld,X15: mworld,X16: mworld,X17: mworld,X18: mworld,X19: mworld,X20: mworld,X21: mworld] :
( ~ ( mrel @ X0 @ X1 )
| ~ ( mrel @ X2 @ X3 )
| ~ ( mrel @ X4 @ X5 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( mrel @ X8 @ X9 )
| ~ ( mrel @ X10 @ X11 )
| ~ ( mrel @ X12 @ X13 )
| ~ ( mrel @ X14 @ X15 )
| ~ ( mrel @ X16 @ X17 )
| ~ ( mrel @ X18 @ X19 )
| ~ ( mrel @ X20 @ X21 )
| ~ ( v6 @ ( sk__9 @ X21 ) )
| ~ ( mrel @ X19 @ X20 )
| ~ ( mrel @ X17 @ X18 )
| ~ ( mrel @ X15 @ X16 )
| ~ ( mrel @ X13 @ X14 )
| ~ ( mrel @ X11 @ X12 )
| ~ ( mrel @ X9 @ X10 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ X3 @ X4 )
| ~ ( mrel @ X1 @ X2 )
| ~ ( mrel @ mactual @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl0_390,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_391,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_392,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_393,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_394,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_395,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_396,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_397,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_398,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_399,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_400,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_401,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_402,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_403,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_404,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_405,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_406,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_407,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_408,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_409,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_410,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl0_411,plain,
! [X0: mworld,X1: mworld] : ( mrel @ X0 @ X1 ),
inference(cnf,[status(esa)],[mrel_universal]) ).
thf(zip_derived_cl177,plain,
! [X21: mworld] :
~ ( v6 @ ( sk__9 @ X21 ) ),
inference(demod,[status(thm)],[zip_derived_cl77,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0,zip_derived_cl0]) ).
thf(zip_derived_cl474,plain,
! [X1: mworld] : ( v11 @ X1 ),
inference('sup-',[status(thm)],[zip_derived_cl380,zip_derived_cl177]) ).
thf(zip_derived_cl479,plain,
! [X1: mworld,X2: mworld] :
( ~ ( v1 @ X1 )
| ~ ( v7 @ X2 ) ),
inference(demod,[status(thm)],[zip_derived_cl311,zip_derived_cl474]) ).
thf(zip_derived_cl486,plain,
! [X1: mworld,X2: mworld] :
( ( v12 @ X2 )
| ~ ( v7 @ X1 ) ),
inference('sup-',[status(thm)],[zip_derived_cl403,zip_derived_cl479]) ).
thf(zip_derived_cl497,plain,
! [X1: mworld] : ( v12 @ X1 ),
inference('sup-',[status(thm)],[zip_derived_cl179,zip_derived_cl486]) ).
thf(zip_derived_cl501,plain,
! [X2: mworld] : ( v23 @ X2 ),
inference(demod,[status(thm)],[zip_derived_cl456,zip_derived_cl497]) ).
thf(zip_derived_cl502,plain,
$false,
inference(demod,[status(thm)],[zip_derived_cl121,zip_derived_cl501]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.20 % Problem : SYO905^6 : TPTP v9.2.0. Released v8.1.0.
% 0.06/0.21 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.CSXoxSbglY true
% 0.12/0.44 % Computer : n007.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:13:08 EDT 2025
% 0.16/0.44 % CPUTime :
% 0.16/0.44 % Running portfolio for 300 s
% 0.16/0.44 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.45 % Number of cores: 8
% 0.16/0.45 % Python version: Python 3.6.8
% 0.16/0.45 % Running in HO mode
% 0.26/0.70 % Total configuration time : 828
% 0.26/0.70 % Estimated wc time : 1656
% 0.26/0.70 % Estimated cpu time (8 cpus) : 207.0
% 0.28/0.85 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.28/0.86 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.28/0.86 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 0.28/0.86 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.28/0.87 % /export/starexec/sandbox/solver/bin/lams/40_noforms.sh running for 90s
% 0.28/0.87 % /export/starexec/sandbox/solver/bin/lams/40_b.comb.sh running for 70s
% 0.28/0.87 % /export/starexec/sandbox/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.28/0.88 % /export/starexec/sandbox/solver/bin/lams/30_sp5.sh running for 60s
% 1.29/1.09 % /export/starexec/sandbox/solver/bin/lams/30_b.l.sh running for 90s
% 1.49/1.17 % /export/starexec/sandbox/solver/bin/lams/35_full_unif.sh running for 56s
% 1.49/1.22 % /export/starexec/sandbox/solver/bin/lams/15_old_s4.sh running for 30s
% 1.62/1.24 % /export/starexec/sandbox/solver/bin/lams/15_lifting3.sh running for 30s
% 1.62/1.25 % /export/starexec/sandbox/solver/bin/lams/33_shallow_sine.sh running for 66s
% 1.80/1.33 % /export/starexec/sandbox/solver/bin/lams/40_e_lift.sh running for 80s
% 2.07/1.45 % /export/starexec/sandbox/solver/bin/lams/15_lifting1.sh running for 30s
% 2.13/1.48 % /export/starexec/sandbox/solver/bin/lams/8_new_cnf.sh running for 16s
% 3.09/1.69 % /export/starexec/sandbox/solver/bin/lams/10_e_short2.sh running for 20s
% 10.17/3.38 % Solved by lams/40_noforms.sh.
% 10.17/3.38 % done 190 iterations in 2.340s
% 10.17/3.38 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 10.17/3.38 % SZS output start Refutation
% See solution above
% 10.17/3.39
% 10.17/3.39
% 10.17/3.39 % Terminating...
% 10.48/3.51 % Runner terminated.
% 10.48/3.51 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------