%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SYN741^7 : TPTP v9.2.0. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.BU3o1V09ef true
% Computer : n006.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:05:40 PM UTC 2025
% Result : Theorem 12.25s 2.43s
% Output : Refutation 12.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 34
% Syntax : Number of formulae : 276 ( 53 unt; 0 typ; 0 def)
% Number of atoms : 2479 ( 15 equ; 504 cnn)
% Maximal formula atoms : 23 ( 8 avg)
% Number of connectives : 5861 (1135 ~;1235 |; 0 &;3189 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 11 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 21 ( 21 >; 0 *; 0 +; 0 <<)
% Number of symbols : 15 ( 10 usr; 4 con; 0-3 aty)
% ( 302 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 970 ( 329 ^; 641 !; 0 ?; 970 :)
% Comments :
%------------------------------------------------------------------------------
thf(v1_type,type,
v1: $i > $o ).
thf(v4_type,type,
v4: $i > $o ).
thf(rel_s4_type,type,
rel_s4: $i > $i > $o ).
thf(mreflexive_type,type,
mreflexive: ( $i > $i > $o ) > $o ).
thf(mnot_type,type,
mnot: ( $i > $o ) > $i > $o ).
thf(mor_type,type,
mor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(v2_type,type,
v2: $i > $o ).
thf(mbox_s4_type,type,
mbox_s4: ( $i > $o ) > $i > $o ).
thf(v3_type,type,
v3: $i > $o ).
thf(mvalid_type,type,
mvalid: ( $i > $o ) > $o ).
thf(mbox_s4,axiom,
( mbox_s4
= ( ^ [Phi: $i > $o,W: $i] :
! [V: $i] :
( ( Phi @ V )
| ~ ( rel_s4 @ W @ V ) ) ) ) ).
thf('0',plain,
( mbox_s4
= ( ^ [Phi: $i > $o,W: $i] :
! [V: $i] :
( ( Phi @ V )
| ~ ( rel_s4 @ W @ V ) ) ) ),
inference(simplify_rw_rule,[status(thm)],[mbox_s4]) ).
thf('1',plain,
( mbox_s4
= ( ^ [V_1: $i > $o,V_2: $i] :
! [X4: $i] :
( ( V_1 @ X4 )
| ~ ( rel_s4 @ V_2 @ X4 ) ) ) ),
define([status(thm)]) ).
thf(mvalid,axiom,
( mvalid
= ( ^ [Phi: $i > $o] :
! [W: $i] : ( Phi @ W ) ) ) ).
thf('2',plain,
( mvalid
= ( ^ [Phi: $i > $o] :
! [W: $i] : ( Phi @ W ) ) ),
inference(simplify_rw_rule,[status(thm)],[mvalid]) ).
thf('3',plain,
( mvalid
= ( ^ [V_1: $i > $o] :
! [X4: $i] : ( V_1 @ X4 ) ) ),
define([status(thm)]) ).
thf(mor,axiom,
( mor
= ( ^ [Phi: $i > $o,Psi: $i > $o,W: $i] :
( ( Phi @ W )
| ( Psi @ W ) ) ) ) ).
thf('4',plain,
( mor
= ( ^ [Phi: $i > $o,Psi: $i > $o,W: $i] :
( ( Phi @ W )
| ( Psi @ W ) ) ) ),
inference(simplify_rw_rule,[status(thm)],[mor]) ).
thf('5',plain,
( mor
= ( ^ [V_1: $i > $o,V_2: $i > $o,V_3: $i] :
( ( V_1 @ V_3 )
| ( V_2 @ V_3 ) ) ) ),
define([status(thm)]) ).
thf(mnot,axiom,
( mnot
= ( ^ [Phi: $i > $o,W: $i] :
~ ( Phi @ W ) ) ) ).
thf('6',plain,
( mnot
= ( ^ [Phi: $i > $o,W: $i] :
~ ( Phi @ W ) ) ),
inference(simplify_rw_rule,[status(thm)],[mnot]) ).
thf('7',plain,
( mnot
= ( ^ [V_1: $i > $o,V_2: $i] :
~ ( V_1 @ V_2 ) ) ),
define([status(thm)]) ).
thf(persat21,axiom,
mvalid @ ( mor @ v4 @ ( mor @ ( mnot @ v2 ) @ ( mor @ ( mbox_s4 @ ( mbox_s4 @ v3 ) ) @ ( mbox_s4 @ ( mbox_s4 @ ( mnot @ v1 ) ) ) ) ) ) ).
thf(zf_stmt_0,axiom,
! [X4: $i] :
( ! [X10: $i] :
( ~ ( rel_s4 @ X4 @ X10 )
| ! [X12: $i] :
( ~ ( rel_s4 @ X10 @ X12 )
| ~ ( v1 @ X12 ) ) )
| ! [X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ! [X8: $i] :
( ~ ( rel_s4 @ X6 @ X8 )
| ( v3 @ X8 ) ) )
| ~ ( v2 @ X4 )
| ( v4 @ X4 ) ) ).
thf(zip_derived_cl24,plain,
( !!
@ ^ [Y0: $i] :
( ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( (~) @ ( v1 @ Y2 ) ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( v3 @ Y2 ) ) ) ) )
| ( (~) @ ( v2 @ Y0 ) )
| ( v4 @ Y0 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl1157,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v3 @ Y1 ) ) ) ) )
| ( (~) @ ( v2 @ X2 ) )
| ( v4 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl24]) ).
thf(mreflexive,axiom,
( mreflexive
= ( ^ [R: $i > $i > $o] :
! [S: $i] : ( R @ S @ S ) ) ) ).
thf('8',plain,
( mreflexive
= ( ^ [R: $i > $i > $o] :
! [S: $i] : ( R @ S @ S ) ) ),
inference(simplify_rw_rule,[status(thm)],[mreflexive]) ).
thf('9',plain,
( mreflexive
= ( ^ [V_1: $i > $i > $o] :
! [X4: $i] : ( V_1 @ X4 @ X4 ) ) ),
define([status(thm)]) ).
thf(a1,axiom,
mreflexive @ rel_s4 ).
thf(zf_stmt_1,axiom,
! [X4: $i] : ( rel_s4 @ X4 @ X4 ) ).
thf(zip_derived_cl1,plain,
( !!
@ ^ [Y0: $i] : ( rel_s4 @ Y0 @ Y0 ) ),
inference(cnf,[status(esa)],[zf_stmt_1]) ).
thf(zip_derived_cl37,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(persat16,axiom,
mvalid @ ( mor @ v3 @ ( mor @ ( mbox_s4 @ v4 ) @ ( mor @ ( mbox_s4 @ ( mbox_s4 @ v2 ) ) @ ( mbox_s4 @ ( mbox_s4 @ v3 ) ) ) ) ) ).
thf(zf_stmt_2,axiom,
! [X4: $i] :
( ! [X12: $i] :
( ~ ( rel_s4 @ X4 @ X12 )
| ! [X14: $i] :
( ~ ( rel_s4 @ X12 @ X14 )
| ( v3 @ X14 ) ) )
| ! [X8: $i] :
( ~ ( rel_s4 @ X4 @ X8 )
| ! [X10: $i] :
( ~ ( rel_s4 @ X8 @ X10 )
| ( v2 @ X10 ) ) )
| ! [X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ( v4 @ X6 ) )
| ( v3 @ X4 ) ) ).
thf(zip_derived_cl19,plain,
( !!
@ ^ [Y0: $i] :
( ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( v3 @ Y2 ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( v2 @ Y2 ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v4 @ Y1 ) ) )
| ( v3 @ Y0 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_2]) ).
thf(zip_derived_cl869,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v3 @ Y1 ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v2 @ Y1 ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ( v3 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl19]) ).
thf(zip_derived_cl870,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v3 @ Y1 ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v2 @ Y1 ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl869]) ).
thf(zip_derived_cl871,plain,
! [X2: $i,X4: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X4 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( v3 @ Y0 ) ) )
| ( v3 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v2 @ Y1 ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl870]) ).
thf(zip_derived_cl872,plain,
! [X2: $i,X4: $i] :
( ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( v3 @ Y0 ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v2 @ Y1 ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl871]) ).
thf(zip_derived_cl873,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( (~) @ ( rel_s4 @ X4 @ X6 ) )
| ( v3 @ X6 )
| ( v3 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v2 @ Y1 ) ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl872]) ).
thf(zip_derived_cl874,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v2 @ Y1 ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl873]) ).
thf(zip_derived_cl875,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X8 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( v2 @ Y0 ) ) )
| ( v3 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ~ ( rel_s4 @ X2 @ X4 )
| ( v3 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl874]) ).
thf(zip_derived_cl876,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( rel_s4 @ X2 @ X8 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( v2 @ Y0 ) ) )
| ~ ( rel_s4 @ X4 @ X6 )
| ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl875]) ).
thf(zip_derived_cl877,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( (~) @ ( rel_s4 @ X8 @ X10 ) )
| ( v2 @ X10 )
| ( v3 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ~ ( rel_s4 @ X2 @ X4 )
| ( v3 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( rel_s4 @ X2 @ X8 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl876]) ).
thf(zip_derived_cl878,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( rel_s4 @ X8 @ X10 )
| ( v2 @ X10 )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl877]) ).
thf(zip_derived_cl879,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i,X12: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X12 ) )
| ( v4 @ X12 )
| ( v3 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( v3 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( rel_s4 @ X2 @ X8 )
| ( v2 @ X10 )
| ~ ( rel_s4 @ X8 @ X10 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl878]) ).
thf(zip_derived_cl880,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i,X12: $i] :
( ~ ( rel_s4 @ X2 @ X12 )
| ( v4 @ X12 )
| ~ ( rel_s4 @ X8 @ X10 )
| ( v2 @ X10 )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl879]) ).
thf(zip_derived_cl891,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( v3 @ X1 )
| ~ ( rel_s4 @ X1 @ X1 )
| ( v3 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( rel_s4 @ X1 @ X2 )
| ( v2 @ X3 )
| ~ ( rel_s4 @ X2 @ X3 )
| ( v4 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl880]) ).
thf(zip_derived_cl37_001,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl893,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( v3 @ X1 )
| ( v3 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( rel_s4 @ X1 @ X2 )
| ( v2 @ X3 )
| ~ ( rel_s4 @ X2 @ X3 )
| ( v4 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl891,zip_derived_cl37]) ).
thf(persat15,axiom,
mvalid @ ( mor @ v3 @ ( mor @ ( mnot @ v2 ) @ ( mor @ ( mbox_s4 @ ( mbox_s4 @ ( mnot @ v2 ) ) ) @ ( mbox_s4 @ ( mbox_s4 @ ( mnot @ v4 ) ) ) ) ) ) ).
thf(zf_stmt_3,axiom,
! [X4: $i] :
( ! [X10: $i] :
( ~ ( rel_s4 @ X4 @ X10 )
| ! [X12: $i] :
( ~ ( rel_s4 @ X10 @ X12 )
| ~ ( v4 @ X12 ) ) )
| ! [X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ! [X8: $i] :
( ~ ( rel_s4 @ X6 @ X8 )
| ~ ( v2 @ X8 ) ) )
| ~ ( v2 @ X4 )
| ( v3 @ X4 ) ) ).
thf(zip_derived_cl18,plain,
( !!
@ ^ [Y0: $i] :
( ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( (~) @ ( v4 @ Y2 ) ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( (~) @ ( v2 @ Y2 ) ) ) ) ) )
| ( (~) @ ( v2 @ Y0 ) )
| ( v3 @ Y0 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_3]) ).
thf(zip_derived_cl824,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v4 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v2 @ Y1 ) ) ) ) ) )
| ( (~) @ ( v2 @ X2 ) )
| ( v3 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl18]) ).
thf(zip_derived_cl825,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v4 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v2 @ Y1 ) ) ) ) ) )
| ~ ( v2 @ X2 )
| ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl824]) ).
thf(zip_derived_cl826,plain,
! [X2: $i,X4: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X4 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ( v3 @ X2 )
| ~ ( v2 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v2 @ Y1 ) ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl825]) ).
thf(zip_derived_cl827,plain,
! [X2: $i,X4: $i] :
( ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v2 @ Y1 ) ) ) ) ) )
| ~ ( v2 @ X2 )
| ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl826]) ).
thf(zip_derived_cl828,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( (~) @ ( rel_s4 @ X4 @ X6 ) )
| ( (~) @ ( v4 @ X6 ) )
| ( v3 @ X2 )
| ~ ( v2 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v2 @ Y1 ) ) ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl827]) ).
thf(zip_derived_cl829,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v2 @ Y1 ) ) ) ) ) )
| ~ ( v2 @ X2 )
| ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl828]) ).
thf(zip_derived_cl830,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X8 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( (~) @ ( v2 @ Y0 ) ) ) )
| ( v3 @ X2 )
| ~ ( v2 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl829]) ).
thf(zip_derived_cl831,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( rel_s4 @ X2 @ X8 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( (~) @ ( v2 @ Y0 ) ) ) )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v2 @ X2 )
| ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl830]) ).
thf(zip_derived_cl832,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( (~) @ ( rel_s4 @ X8 @ X10 ) )
| ( (~) @ ( v2 @ X10 ) )
| ( v3 @ X2 )
| ~ ( v2 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( rel_s4 @ X2 @ X8 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl831]) ).
thf(zip_derived_cl833,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( rel_s4 @ X8 @ X10 )
| ~ ( v2 @ X10 )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v2 @ X2 )
| ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl832]) ).
thf(zip_derived_cl842,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( v3 @ X0 )
| ~ ( v2 @ X0 )
| ~ ( rel_s4 @ X0 @ X1 )
| ~ ( v4 @ X2 )
| ~ ( rel_s4 @ X1 @ X2 )
| ~ ( rel_s4 @ X0 @ X0 )
| ~ ( v2 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl833]) ).
thf(zip_derived_cl845,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( rel_s4 @ X0 @ X0 )
| ~ ( rel_s4 @ X1 @ X2 )
| ~ ( v4 @ X2 )
| ~ ( rel_s4 @ X0 @ X1 )
| ~ ( v2 @ X0 )
| ( v3 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl842]) ).
thf(zip_derived_cl37_002,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl848,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( rel_s4 @ X1 @ X2 )
| ~ ( v4 @ X2 )
| ~ ( rel_s4 @ X0 @ X1 )
| ~ ( v2 @ X0 )
| ( v3 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl845,zip_derived_cl37]) ).
thf(zip_derived_cl857,plain,
! [X0: $i] :
( ( v3 @ X0 )
| ~ ( v2 @ X0 )
| ~ ( rel_s4 @ X0 @ X0 )
| ~ ( v4 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl848]) ).
thf(zip_derived_cl37_003,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl858,plain,
! [X0: $i] :
( ( v3 @ X0 )
| ~ ( v2 @ X0 )
| ~ ( v4 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl857,zip_derived_cl37]) ).
thf(zip_derived_cl37_004,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(persat10,axiom,
mvalid @ ( mor @ v2 @ ( mor @ ( mnot @ v4 ) @ ( mor @ ( mbox_s4 @ ( mnot @ v4 ) ) @ ( mbox_s4 @ ( mbox_s4 @ ( mnot @ v4 ) ) ) ) ) ) ).
thf(zf_stmt_4,axiom,
! [X4: $i] :
( ! [X8: $i] :
( ~ ( rel_s4 @ X4 @ X8 )
| ! [X10: $i] :
( ~ ( rel_s4 @ X8 @ X10 )
| ~ ( v4 @ X10 ) ) )
| ! [X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v4 @ X6 ) )
| ~ ( v4 @ X4 )
| ( v2 @ X4 ) ) ).
thf(zip_derived_cl13,plain,
( !!
@ ^ [Y0: $i] :
( ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( (~) @ ( v4 @ Y2 ) ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v4 @ Y1 ) ) ) )
| ( (~) @ ( v4 @ Y0 ) )
| ( v2 @ Y0 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_4]) ).
thf(zip_derived_cl540,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v4 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ( (~) @ ( v4 @ X2 ) )
| ( v2 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl13]) ).
thf(zip_derived_cl541,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v4 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ~ ( v4 @ X2 )
| ( v2 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl540]) ).
thf(zip_derived_cl542,plain,
! [X2: $i,X4: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X4 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ( v2 @ X2 )
| ~ ( v4 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl541]) ).
thf(zip_derived_cl543,plain,
! [X2: $i,X4: $i] :
( ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ~ ( v4 @ X2 )
| ( v2 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl542]) ).
thf(zip_derived_cl544,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( (~) @ ( rel_s4 @ X4 @ X6 ) )
| ( (~) @ ( v4 @ X6 ) )
| ( v2 @ X2 )
| ~ ( v4 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl543]) ).
thf(zip_derived_cl545,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ~ ( v4 @ X2 )
| ( v2 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl544]) ).
thf(zip_derived_cl546,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X8 ) )
| ( (~) @ ( v4 @ X8 ) )
| ( v2 @ X2 )
| ~ ( v4 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl545]) ).
thf(zip_derived_cl547,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( rel_s4 @ X2 @ X8 )
| ~ ( v4 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v4 @ X2 )
| ( v2 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl546]) ).
thf(zip_derived_cl555,plain,
! [X0: $i,X1: $i] :
( ( v2 @ X1 )
| ~ ( v4 @ X1 )
| ~ ( rel_s4 @ X1 @ X1 )
| ~ ( v4 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v4 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl547]) ).
thf(zip_derived_cl557,plain,
! [X0: $i,X1: $i] :
( ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v4 @ X0 )
| ~ ( rel_s4 @ X1 @ X1 )
| ~ ( v4 @ X1 )
| ( v2 @ X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl555]) ).
thf(zip_derived_cl37_005,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl558,plain,
! [X0: $i,X1: $i] :
( ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v4 @ X0 )
| ~ ( v4 @ X1 )
| ( v2 @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl557,zip_derived_cl37]) ).
thf(zip_derived_cl560,plain,
! [X0: $i] :
( ( v2 @ X0 )
| ~ ( v4 @ X0 )
| ~ ( v4 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl37,zip_derived_cl558]) ).
thf(zip_derived_cl567,plain,
! [X0: $i] :
( ~ ( v4 @ X0 )
| ( v2 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl560]) ).
thf(zip_derived_cl859,plain,
! [X0: $i] :
( ~ ( v4 @ X0 )
| ( v3 @ X0 ) ),
inference(clc,[status(thm)],[zip_derived_cl858,zip_derived_cl567]) ).
thf(zip_derived_cl956,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( rel_s4 @ X2 @ X3 )
| ( v2 @ X3 )
| ~ ( rel_s4 @ X1 @ X2 )
| ~ ( rel_s4 @ X1 @ X0 )
| ( v3 @ X0 )
| ( v3 @ X1 ) ),
inference(clc,[status(thm)],[zip_derived_cl893,zip_derived_cl859]) ).
thf(zip_derived_cl966,plain,
! [X0: $i,X1: $i] :
( ( v3 @ X1 )
| ( v3 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( rel_s4 @ X1 @ X1 )
| ( v2 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl956]) ).
thf(zip_derived_cl37_006,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl967,plain,
! [X0: $i,X1: $i] :
( ( v3 @ X1 )
| ( v3 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ( v2 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl966,zip_derived_cl37]) ).
thf(zip_derived_cl37_007,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(persat8,axiom,
mvalid @ ( mor @ v2 @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox_s4 @ ( mnot @ v3 ) ) @ ( mbox_s4 @ ( mbox_s4 @ ( mnot @ v3 ) ) ) ) ) ) ).
thf(zf_stmt_5,axiom,
! [X4: $i] :
( ! [X8: $i] :
( ~ ( rel_s4 @ X4 @ X8 )
| ! [X10: $i] :
( ~ ( rel_s4 @ X8 @ X10 )
| ~ ( v3 @ X10 ) ) )
| ! [X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v3 @ X6 ) )
| ~ ( v1 @ X4 )
| ( v2 @ X4 ) ) ).
thf(zip_derived_cl11,plain,
( !!
@ ^ [Y0: $i] :
( ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( (~) @ ( v3 @ Y2 ) ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v3 @ Y1 ) ) ) )
| ( (~) @ ( v1 @ Y0 ) )
| ( v2 @ Y0 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_5]) ).
thf(zip_derived_cl464,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v3 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( (~) @ ( v1 @ X2 ) )
| ( v2 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl11]) ).
thf(zip_derived_cl465,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v3 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ~ ( v1 @ X2 )
| ( v2 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl464]) ).
thf(zip_derived_cl466,plain,
! [X2: $i,X4: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X4 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( v2 @ X2 )
| ~ ( v1 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl465]) ).
thf(zip_derived_cl467,plain,
! [X2: $i,X4: $i] :
( ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ~ ( v1 @ X2 )
| ( v2 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl466]) ).
thf(zip_derived_cl468,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( (~) @ ( rel_s4 @ X4 @ X6 ) )
| ( (~) @ ( v3 @ X6 ) )
| ( v2 @ X2 )
| ~ ( v1 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl467]) ).
thf(zip_derived_cl469,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ~ ( v1 @ X2 )
| ( v2 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl468]) ).
thf(zip_derived_cl470,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X8 ) )
| ( (~) @ ( v3 @ X8 ) )
| ( v2 @ X2 )
| ~ ( v1 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl469]) ).
thf(zip_derived_cl471,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( rel_s4 @ X2 @ X8 )
| ~ ( v3 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v1 @ X2 )
| ( v2 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl470]) ).
thf(zip_derived_cl479,plain,
! [X0: $i,X1: $i] :
( ( v2 @ X1 )
| ~ ( v1 @ X1 )
| ~ ( rel_s4 @ X1 @ X1 )
| ~ ( v3 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v3 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl471]) ).
thf(zip_derived_cl481,plain,
! [X0: $i,X1: $i] :
( ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v3 @ X0 )
| ~ ( rel_s4 @ X1 @ X1 )
| ~ ( v1 @ X1 )
| ( v2 @ X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl479]) ).
thf(zip_derived_cl37_008,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl482,plain,
! [X0: $i,X1: $i] :
( ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v3 @ X0 )
| ~ ( v1 @ X1 )
| ( v2 @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl481,zip_derived_cl37]) ).
thf(zip_derived_cl483,plain,
! [X0: $i] :
( ( v2 @ X0 )
| ~ ( v1 @ X0 )
| ~ ( v3 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl37,zip_derived_cl482]) ).
thf(persat4,axiom,
mvalid @ ( mor @ v1 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox_s4 @ ( mbox_s4 @ v2 ) ) @ ( mbox_s4 @ ( mbox_s4 @ ( mnot @ v3 ) ) ) ) ) ) ).
thf(zf_stmt_6,axiom,
! [X4: $i] :
( ! [X10: $i] :
( ~ ( rel_s4 @ X4 @ X10 )
| ! [X12: $i] :
( ~ ( rel_s4 @ X10 @ X12 )
| ~ ( v3 @ X12 ) ) )
| ! [X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ! [X8: $i] :
( ~ ( rel_s4 @ X6 @ X8 )
| ( v2 @ X8 ) ) )
| ~ ( v3 @ X4 )
| ( v1 @ X4 ) ) ).
thf(zip_derived_cl7,plain,
( !!
@ ^ [Y0: $i] :
( ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( (~) @ ( v3 @ Y2 ) ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( v2 @ Y2 ) ) ) ) )
| ( (~) @ ( v3 @ Y0 ) )
| ( v1 @ Y0 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_6]) ).
thf(zip_derived_cl225,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v3 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v2 @ Y1 ) ) ) ) )
| ( (~) @ ( v3 @ X2 ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl7]) ).
thf(zip_derived_cl226,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v3 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v2 @ Y1 ) ) ) ) )
| ~ ( v3 @ X2 )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl225]) ).
thf(zip_derived_cl227,plain,
! [X2: $i,X4: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X4 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( v1 @ X2 )
| ~ ( v3 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v2 @ Y1 ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl226]) ).
thf(zip_derived_cl228,plain,
! [X2: $i,X4: $i] :
( ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v2 @ Y1 ) ) ) ) )
| ~ ( v3 @ X2 )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl227]) ).
thf(zip_derived_cl229,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( (~) @ ( rel_s4 @ X4 @ X6 ) )
| ( (~) @ ( v3 @ X6 ) )
| ( v1 @ X2 )
| ~ ( v3 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v2 @ Y1 ) ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl228]) ).
thf(zip_derived_cl230,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v2 @ Y1 ) ) ) ) )
| ~ ( v3 @ X2 )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl229]) ).
thf(zip_derived_cl231,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X8 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( v2 @ Y0 ) ) )
| ( v1 @ X2 )
| ~ ( v3 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl230]) ).
thf(zip_derived_cl232,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( rel_s4 @ X2 @ X8 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( v2 @ Y0 ) ) )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v3 @ X2 )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl231]) ).
thf(zip_derived_cl233,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( (~) @ ( rel_s4 @ X8 @ X10 ) )
| ( v2 @ X10 )
| ( v1 @ X2 )
| ~ ( v3 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( rel_s4 @ X2 @ X8 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl232]) ).
thf(zip_derived_cl234,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( rel_s4 @ X8 @ X10 )
| ( v2 @ X10 )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v3 @ X2 )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl233]) ).
thf(zip_derived_cl242,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( v1 @ X2 )
| ~ ( v3 @ X2 )
| ~ ( rel_s4 @ X2 @ X1 )
| ~ ( v3 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( rel_s4 @ X2 @ X1 )
| ( v2 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl234]) ).
thf(zip_derived_cl244,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( v2 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v3 @ X0 )
| ~ ( rel_s4 @ X2 @ X1 )
| ~ ( v3 @ X2 )
| ( v1 @ X2 ) ),
inference(simplify,[status(thm)],[zip_derived_cl242]) ).
thf(zip_derived_cl288,plain,
! [X0: $i] :
( ( v1 @ X0 )
| ~ ( v3 @ X0 )
| ~ ( rel_s4 @ X0 @ X0 )
| ~ ( v3 @ X0 )
| ( v2 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl244]) ).
thf(zip_derived_cl289,plain,
! [X0: $i] :
( ( v2 @ X0 )
| ~ ( rel_s4 @ X0 @ X0 )
| ~ ( v3 @ X0 )
| ( v1 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl288]) ).
thf(zip_derived_cl37_009,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl290,plain,
! [X0: $i] :
( ( v2 @ X0 )
| ~ ( v3 @ X0 )
| ( v1 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl289,zip_derived_cl37]) ).
thf(zip_derived_cl490,plain,
! [X0: $i] :
( ~ ( v3 @ X0 )
| ( v2 @ X0 ) ),
inference(clc,[status(thm)],[zip_derived_cl483,zip_derived_cl290]) ).
thf(zip_derived_cl996,plain,
! [X0: $i,X1: $i] :
( ( v2 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ( v3 @ X1 ) ),
inference(clc,[status(thm)],[zip_derived_cl967,zip_derived_cl490]) ).
thf(zip_derived_cl997,plain,
! [X0: $i] :
( ( v3 @ X0 )
| ( v2 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl37,zip_derived_cl996]) ).
thf(zip_derived_cl490_010,plain,
! [X0: $i] :
( ~ ( v3 @ X0 )
| ( v2 @ X0 ) ),
inference(clc,[status(thm)],[zip_derived_cl483,zip_derived_cl290]) ).
thf(zip_derived_cl1005,plain,
! [X0: $i] : ( v2 @ X0 ),
inference(clc,[status(thm)],[zip_derived_cl997,zip_derived_cl490]) ).
thf(zip_derived_cl1158,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v3 @ Y1 ) ) ) ) )
| ( (~) @ $true )
| ( v4 @ X2 ) ),
inference(demod,[status(thm)],[zip_derived_cl1157,zip_derived_cl1005]) ).
thf(zip_derived_cl1159,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) )
| ( v4 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v3 @ Y1 ) ) ) ) ) ),
inference('simplify boolean subterms',[status(thm)],[zip_derived_cl1158]) ).
thf(zip_derived_cl1160,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) )
| ( v4 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v3 @ Y1 ) ) ) ) ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1159]) ).
thf(zip_derived_cl1161,plain,
! [X2: $i,X4: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X4 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v3 @ Y1 ) ) ) ) )
| ( v4 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1160]) ).
thf(zip_derived_cl1162,plain,
! [X2: $i,X4: $i] :
( ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ( v4 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v3 @ Y1 ) ) ) ) ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1161]) ).
thf(zip_derived_cl1163,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( (~) @ ( rel_s4 @ X4 @ X6 ) )
| ( (~) @ ( v1 @ X6 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v3 @ Y1 ) ) ) ) )
| ( v4 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1162]) ).
thf(zip_derived_cl1164,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( v4 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v3 @ Y1 ) ) ) ) ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1163]) ).
thf(zip_derived_cl1165,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X8 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( v3 @ Y0 ) ) )
| ( v4 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1164]) ).
thf(zip_derived_cl1166,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( rel_s4 @ X2 @ X8 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( v3 @ Y0 ) ) )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( v4 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1165]) ).
thf(zip_derived_cl1167,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( (~) @ ( rel_s4 @ X8 @ X10 ) )
| ( v3 @ X10 )
| ( v4 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( rel_s4 @ X2 @ X8 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1166]) ).
thf(zip_derived_cl1168,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( rel_s4 @ X8 @ X10 )
| ( v3 @ X10 )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( v4 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1167]) ).
thf(zip_derived_cl1179,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( v4 @ X2 )
| ~ ( rel_s4 @ X2 @ X1 )
| ~ ( v1 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( rel_s4 @ X2 @ X1 )
| ( v3 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl1168]) ).
thf(zip_derived_cl1181,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( v3 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v1 @ X0 )
| ~ ( rel_s4 @ X2 @ X1 )
| ( v4 @ X2 ) ),
inference(simplify,[status(thm)],[zip_derived_cl1179]) ).
thf(zip_derived_cl37_011,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(persat25,axiom,
mvalid @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox_s4 @ ( mnot @ v1 ) ) @ ( mor @ ( mbox_s4 @ ( mnot @ v3 ) ) @ ( mbox_s4 @ ( mbox_s4 @ ( mnot @ v1 ) ) ) ) ) ) ).
thf(zf_stmt_7,axiom,
! [X4: $i] :
( ! [X10: $i] :
( ~ ( rel_s4 @ X4 @ X10 )
| ! [X12: $i] :
( ~ ( rel_s4 @ X10 @ X12 )
| ~ ( v1 @ X12 ) ) )
| ! [X8: $i] :
( ~ ( rel_s4 @ X4 @ X8 )
| ~ ( v3 @ X8 ) )
| ! [X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v1 @ X6 ) )
| ~ ( v1 @ X4 ) ) ).
thf(zip_derived_cl28,plain,
( !!
@ ^ [Y0: $i] :
( ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( (~) @ ( v1 @ Y2 ) ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v3 @ Y1 ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) )
| ( (~) @ ( v1 @ Y0 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_7]) ).
thf(zip_derived_cl1360,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ( (~) @ ( v1 @ X2 ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl28]) ).
thf(zip_derived_cl1361,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ~ ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1360]) ).
thf(zip_derived_cl1362,plain,
! [X2: $i,X4: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X4 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ~ ( v1 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1361]) ).
thf(zip_derived_cl1363,plain,
! [X2: $i,X4: $i] :
( ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ~ ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1362]) ).
thf(zip_derived_cl1364,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( (~) @ ( rel_s4 @ X4 @ X6 ) )
| ( (~) @ ( v1 @ X6 ) )
| ~ ( v1 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1363]) ).
thf(zip_derived_cl1365,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ~ ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1364]) ).
thf(zip_derived_cl37_012,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl37_013,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(persat7,axiom,
mvalid @ ( mor @ v1 @ ( mor @ ( mbox_s4 @ ( mnot @ v3 ) ) @ ( mor @ ( mbox_s4 @ ( mbox_s4 @ ( mnot @ v1 ) ) ) @ ( mbox_s4 @ ( mbox_s4 @ ( mnot @ v4 ) ) ) ) ) ) ).
thf(zf_stmt_8,axiom,
! [X4: $i] :
( ! [X12: $i] :
( ~ ( rel_s4 @ X4 @ X12 )
| ! [X14: $i] :
( ~ ( rel_s4 @ X12 @ X14 )
| ~ ( v4 @ X14 ) ) )
| ! [X8: $i] :
( ~ ( rel_s4 @ X4 @ X8 )
| ! [X10: $i] :
( ~ ( rel_s4 @ X8 @ X10 )
| ~ ( v1 @ X10 ) ) )
| ! [X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v3 @ X6 ) )
| ( v1 @ X4 ) ) ).
thf(zip_derived_cl10,plain,
( !!
@ ^ [Y0: $i] :
( ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( (~) @ ( v4 @ Y2 ) ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( (~) @ ( v1 @ Y2 ) ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v3 @ Y1 ) ) ) )
| ( v1 @ Y0 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_8]) ).
thf(zip_derived_cl406,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v4 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl10]) ).
thf(zip_derived_cl407,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v4 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl406]) ).
thf(zip_derived_cl408,plain,
! [X2: $i,X4: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X4 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ( v1 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl407]) ).
thf(zip_derived_cl409,plain,
! [X2: $i,X4: $i] :
( ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl408]) ).
thf(zip_derived_cl410,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( (~) @ ( rel_s4 @ X4 @ X6 ) )
| ( (~) @ ( v4 @ X6 ) )
| ( v1 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl409]) ).
thf(zip_derived_cl411,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl410]) ).
thf(zip_derived_cl412,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X8 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ( v1 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl411]) ).
thf(zip_derived_cl413,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( rel_s4 @ X2 @ X8 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl412]) ).
thf(zip_derived_cl414,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( (~) @ ( rel_s4 @ X8 @ X10 ) )
| ( (~) @ ( v1 @ X10 ) )
| ( v1 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( rel_s4 @ X2 @ X8 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl413]) ).
thf(zip_derived_cl415,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( rel_s4 @ X8 @ X10 )
| ~ ( v1 @ X10 )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl414]) ).
thf(zip_derived_cl416,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i,X12: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X12 ) )
| ( (~) @ ( v3 @ X12 ) )
| ( v1 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( v1 @ X10 )
| ~ ( rel_s4 @ X8 @ X10 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl415]) ).
thf(zip_derived_cl417,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i,X12: $i] :
( ~ ( rel_s4 @ X2 @ X12 )
| ~ ( v3 @ X12 )
| ~ ( rel_s4 @ X8 @ X10 )
| ~ ( v1 @ X10 )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v4 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl416]) ).
thf(zip_derived_cl418,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( v1 @ X0 )
| ~ ( rel_s4 @ X0 @ X1 )
| ~ ( v4 @ X2 )
| ~ ( rel_s4 @ X1 @ X2 )
| ~ ( rel_s4 @ X0 @ X3 )
| ~ ( v1 @ X4 )
| ~ ( rel_s4 @ X3 @ X4 )
| ~ ( v3 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl37,zip_derived_cl417]) ).
thf(zip_derived_cl718,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( v3 @ X1 )
| ~ ( rel_s4 @ X0 @ X2 )
| ~ ( v1 @ X2 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( rel_s4 @ X0 @ X3 )
| ~ ( v4 @ X3 )
| ( v1 @ X1 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl418]) ).
thf(zip_derived_cl848_014,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( rel_s4 @ X1 @ X2 )
| ~ ( v4 @ X2 )
| ~ ( rel_s4 @ X0 @ X1 )
| ~ ( v2 @ X0 )
| ( v3 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl845,zip_derived_cl37]) ).
thf(zip_derived_cl1005_015,plain,
! [X0: $i] : ( v2 @ X0 ),
inference(clc,[status(thm)],[zip_derived_cl997,zip_derived_cl490]) ).
thf(zip_derived_cl1018,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( rel_s4 @ X1 @ X2 )
| ~ ( v4 @ X2 )
| ~ ( rel_s4 @ X0 @ X1 )
| ( v3 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl848,zip_derived_cl1005]) ).
thf(zip_derived_cl1289,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( v1 @ X1 )
| ~ ( v4 @ X3 )
| ~ ( rel_s4 @ X0 @ X3 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v1 @ X2 )
| ~ ( rel_s4 @ X0 @ X2 ) ),
inference(clc,[status(thm)],[zip_derived_cl718,zip_derived_cl1018]) ).
thf(zip_derived_cl1290,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( rel_s4 @ X0 @ X1 )
| ~ ( v1 @ X1 )
| ~ ( rel_s4 @ X2 @ X0 )
| ~ ( v4 @ X0 )
| ( v1 @ X2 ) ),
inference('sup-',[status(thm)],[zip_derived_cl37,zip_derived_cl1289]) ).
thf(persat2,axiom,
mvalid @ ( mor @ v1 @ ( mor @ ( mnot @ v2 ) @ ( mor @ ( mbox_s4 @ ( mbox_s4 @ v4 ) ) @ ( mbox_s4 @ ( mbox_s4 @ ( mnot @ v1 ) ) ) ) ) ) ).
thf(zf_stmt_9,axiom,
! [X4: $i] :
( ! [X10: $i] :
( ~ ( rel_s4 @ X4 @ X10 )
| ! [X12: $i] :
( ~ ( rel_s4 @ X10 @ X12 )
| ~ ( v1 @ X12 ) ) )
| ! [X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ! [X8: $i] :
( ~ ( rel_s4 @ X6 @ X8 )
| ( v4 @ X8 ) ) )
| ~ ( v2 @ X4 )
| ( v1 @ X4 ) ) ).
thf(zip_derived_cl5,plain,
( !!
@ ^ [Y0: $i] :
( ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( (~) @ ( v1 @ Y2 ) ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( v4 @ Y2 ) ) ) ) )
| ( (~) @ ( v2 @ Y0 ) )
| ( v1 @ Y0 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_9]) ).
thf(zip_derived_cl124,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v4 @ Y1 ) ) ) ) )
| ( (~) @ ( v2 @ X2 ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl5]) ).
thf(zip_derived_cl125,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v1 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v4 @ Y1 ) ) ) ) )
| ~ ( v2 @ X2 )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl124]) ).
thf(zip_derived_cl126,plain,
! [X2: $i,X4: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X4 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ( v1 @ X2 )
| ~ ( v2 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v4 @ Y1 ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl125]) ).
thf(zip_derived_cl127,plain,
! [X2: $i,X4: $i] :
( ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v4 @ Y1 ) ) ) ) )
| ~ ( v2 @ X2 )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl126]) ).
thf(zip_derived_cl128,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( (~) @ ( rel_s4 @ X4 @ X6 ) )
| ( (~) @ ( v1 @ X6 ) )
| ( v1 @ X2 )
| ~ ( v2 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v4 @ Y1 ) ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl127]) ).
thf(zip_derived_cl129,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v4 @ Y1 ) ) ) ) )
| ~ ( v2 @ X2 )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl128]) ).
thf(zip_derived_cl130,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X8 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ( v1 @ X2 )
| ~ ( v2 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl129]) ).
thf(zip_derived_cl131,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( rel_s4 @ X2 @ X8 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v2 @ X2 )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl130]) ).
thf(zip_derived_cl132,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( (~) @ ( rel_s4 @ X8 @ X10 ) )
| ( v4 @ X10 )
| ( v1 @ X2 )
| ~ ( v2 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( rel_s4 @ X2 @ X8 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl131]) ).
thf(zip_derived_cl133,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( rel_s4 @ X8 @ X10 )
| ( v4 @ X10 )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v2 @ X2 )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl132]) ).
thf(zip_derived_cl141,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( v1 @ X1 )
| ~ ( v2 @ X1 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v1 @ X2 )
| ~ ( rel_s4 @ X0 @ X2 )
| ~ ( rel_s4 @ X1 @ X1 )
| ( v4 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl133]) ).
thf(zip_derived_cl37_016,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl143,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( v1 @ X1 )
| ~ ( v2 @ X1 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v1 @ X2 )
| ~ ( rel_s4 @ X0 @ X2 )
| ( v4 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl141,zip_derived_cl37]) ).
thf(zip_derived_cl1005_017,plain,
! [X0: $i] : ( v2 @ X0 ),
inference(clc,[status(thm)],[zip_derived_cl997,zip_derived_cl490]) ).
thf(zip_derived_cl1013,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( v1 @ X1 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v1 @ X2 )
| ~ ( rel_s4 @ X0 @ X2 )
| ( v4 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl143,zip_derived_cl1005]) ).
thf(zip_derived_cl1349,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( v1 @ X2 )
| ~ ( rel_s4 @ X2 @ X0 )
| ~ ( v1 @ X1 )
| ~ ( rel_s4 @ X0 @ X1 ) ),
inference(clc,[status(thm)],[zip_derived_cl1290,zip_derived_cl1013]) ).
thf(zip_derived_cl1366,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v1 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 ) ),
inference(clc,[status(thm)],[zip_derived_cl1365,zip_derived_cl1349]) ).
thf(zip_derived_cl1367,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X8 ) )
| ( (~) @ ( v1 @ X8 ) )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1366]) ).
thf(zip_derived_cl1368,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( rel_s4 @ X2 @ X8 )
| ~ ( v1 @ X8 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1367]) ).
thf(zip_derived_cl1369,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X10 ) )
| ( (~) @ ( v3 @ X10 ) )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v1 @ X8 )
| ~ ( rel_s4 @ X2 @ X8 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1368]) ).
thf(zip_derived_cl1370,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( rel_s4 @ X2 @ X10 )
| ~ ( v3 @ X10 )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( v1 @ X8 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v1 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1369]) ).
thf(zip_derived_cl1382,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v1 @ X0 )
| ~ ( rel_s4 @ X1 @ X1 )
| ~ ( v1 @ X2 )
| ~ ( rel_s4 @ X1 @ X2 )
| ~ ( v3 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl1370]) ).
thf(zip_derived_cl37_018,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl1383,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v1 @ X0 )
| ~ ( v1 @ X2 )
| ~ ( rel_s4 @ X1 @ X2 )
| ~ ( v3 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl1382,zip_derived_cl37]) ).
thf(zip_derived_cl1393,plain,
! [X0: $i,X1: $i] :
( ~ ( v3 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v1 @ X0 )
| ~ ( v1 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl1383]) ).
thf(zip_derived_cl1394,plain,
! [X0: $i,X1: $i] :
( ~ ( v1 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v3 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl1393]) ).
thf(zip_derived_cl1395,plain,
! [X0: $i] :
( ~ ( v3 @ X0 )
| ~ ( v1 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl37,zip_derived_cl1394]) ).
thf(persat5,axiom,
mvalid @ ( mor @ v1 @ ( mor @ ( mbox_s4 @ v1 ) @ ( mor @ ( mbox_s4 @ ( mbox_s4 @ v4 ) ) @ ( mbox_s4 @ ( mbox_s4 @ ( mnot @ v2 ) ) ) ) ) ) ).
thf(zf_stmt_10,axiom,
! [X4: $i] :
( ! [X12: $i] :
( ~ ( rel_s4 @ X4 @ X12 )
| ! [X14: $i] :
( ~ ( rel_s4 @ X12 @ X14 )
| ~ ( v2 @ X14 ) ) )
| ! [X8: $i] :
( ~ ( rel_s4 @ X4 @ X8 )
| ! [X10: $i] :
( ~ ( rel_s4 @ X8 @ X10 )
| ( v4 @ X10 ) ) )
| ! [X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ( v1 @ X6 ) )
| ( v1 @ X4 ) ) ).
thf(zip_derived_cl8,plain,
( !!
@ ^ [Y0: $i] :
( ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( (~) @ ( v2 @ Y2 ) ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( v4 @ Y2 ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v1 @ Y1 ) ) )
| ( v1 @ Y0 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_10]) ).
thf(zip_derived_cl291,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v2 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v4 @ Y1 ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v1 @ Y0 ) ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl8]) ).
thf(zip_derived_cl292,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v2 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v4 @ Y1 ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v1 @ Y0 ) ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl291]) ).
thf(zip_derived_cl293,plain,
! [X2: $i,X4: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X4 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v2 @ Y0 ) ) ) )
| ( v1 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v1 @ Y0 ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v4 @ Y1 ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl292]) ).
thf(zip_derived_cl294,plain,
! [X2: $i,X4: $i] :
( ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v2 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v4 @ Y1 ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v1 @ Y0 ) ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl293]) ).
thf(zip_derived_cl295,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( (~) @ ( rel_s4 @ X4 @ X6 ) )
| ( (~) @ ( v2 @ X6 ) )
| ( v1 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v1 @ Y0 ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v4 @ Y1 ) ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl294]) ).
thf(zip_derived_cl296,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v2 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( v4 @ Y1 ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v1 @ Y0 ) ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl295]) ).
thf(zip_derived_cl297,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X8 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ( v1 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v1 @ Y0 ) ) )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v2 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl296]) ).
thf(zip_derived_cl298,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( rel_s4 @ X2 @ X8 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X8 @ Y0 ) )
| ( v4 @ Y0 ) ) )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v2 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v1 @ Y0 ) ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl297]) ).
thf(zip_derived_cl299,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( (~) @ ( rel_s4 @ X8 @ X10 ) )
| ( v4 @ X10 )
| ( v1 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v1 @ Y0 ) ) )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v2 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( rel_s4 @ X2 @ X8 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl298]) ).
thf(zip_derived_cl300,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( rel_s4 @ X8 @ X10 )
| ( v4 @ X10 )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v2 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( v1 @ Y0 ) ) )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl299]) ).
thf(zip_derived_cl301,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i,X12: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X12 ) )
| ( v1 @ X12 )
| ( v1 @ X2 )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v2 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( rel_s4 @ X2 @ X8 )
| ( v4 @ X10 )
| ~ ( rel_s4 @ X8 @ X10 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl300]) ).
thf(zip_derived_cl302,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i,X12: $i] :
( ~ ( rel_s4 @ X2 @ X12 )
| ( v1 @ X12 )
| ~ ( rel_s4 @ X8 @ X10 )
| ( v4 @ X10 )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v2 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( v1 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl301]) ).
thf(zip_derived_cl312,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( v1 @ X1 )
| ~ ( rel_s4 @ X1 @ X1 )
| ~ ( v2 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( rel_s4 @ X1 @ X2 )
| ( v4 @ X3 )
| ~ ( rel_s4 @ X2 @ X3 )
| ( v1 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl302]) ).
thf(zip_derived_cl37_019,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl314,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( v1 @ X1 )
| ~ ( v2 @ X0 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( rel_s4 @ X1 @ X2 )
| ( v4 @ X3 )
| ~ ( rel_s4 @ X2 @ X3 )
| ( v1 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl312,zip_derived_cl37]) ).
thf(zip_derived_cl1005_020,plain,
! [X0: $i] : ( v2 @ X0 ),
inference(clc,[status(thm)],[zip_derived_cl997,zip_derived_cl490]) ).
thf(zip_derived_cl1785,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( v1 @ X1 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( rel_s4 @ X1 @ X2 )
| ( v4 @ X3 )
| ~ ( rel_s4 @ X2 @ X3 )
| ( v1 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl314,zip_derived_cl1005]) ).
thf(zip_derived_cl37_021,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(persat26,axiom,
mvalid @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox_s4 @ ( mnot @ v2 ) ) @ ( mor @ ( mbox_s4 @ ( mnot @ v4 ) ) @ ( mbox_s4 @ ( mbox_s4 @ ( mnot @ v3 ) ) ) ) ) ) ).
thf(zf_stmt_11,axiom,
! [X4: $i] :
( ! [X10: $i] :
( ~ ( rel_s4 @ X4 @ X10 )
| ! [X12: $i] :
( ~ ( rel_s4 @ X10 @ X12 )
| ~ ( v3 @ X12 ) ) )
| ! [X8: $i] :
( ~ ( rel_s4 @ X4 @ X8 )
| ~ ( v4 @ X8 ) )
| ! [X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v2 @ X6 ) )
| ~ ( v3 @ X4 ) ) ).
thf(zip_derived_cl29,plain,
( !!
@ ^ [Y0: $i] :
( ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( !!
@ ^ [Y2: $i] :
( ( (~) @ ( rel_s4 @ Y1 @ Y2 ) )
| ( (~) @ ( v3 @ Y2 ) ) ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v4 @ Y1 ) ) ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v2 @ Y1 ) ) ) )
| ( (~) @ ( v3 @ Y0 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_11]) ).
thf(zip_derived_cl1427,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v3 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v2 @ Y0 ) ) ) )
| ( (~) @ ( v3 @ X2 ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl29]) ).
thf(zip_derived_cl1428,plain,
! [X2: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( !!
@ ^ [Y1: $i] :
( ( (~) @ ( rel_s4 @ Y0 @ Y1 ) )
| ( (~) @ ( v3 @ Y1 ) ) ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v2 @ Y0 ) ) ) )
| ~ ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1427]) ).
thf(zip_derived_cl1429,plain,
! [X2: $i,X4: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X4 ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ~ ( v3 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v2 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1428]) ).
thf(zip_derived_cl1430,plain,
! [X2: $i,X4: $i] :
( ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X4 @ Y0 ) )
| ( (~) @ ( v3 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v2 @ Y0 ) ) ) )
| ~ ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1429]) ).
thf(zip_derived_cl1431,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( (~) @ ( rel_s4 @ X4 @ X6 ) )
| ( (~) @ ( v3 @ X6 ) )
| ~ ( v3 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v2 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1430]) ).
thf(zip_derived_cl1432,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v4 @ Y0 ) ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v2 @ Y0 ) ) ) )
| ~ ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1431]) ).
thf(zip_derived_cl1433,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X8 ) )
| ( (~) @ ( v4 @ X8 ) )
| ~ ( v3 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v2 @ Y0 ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1432]) ).
thf(zip_derived_cl1434,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( rel_s4 @ X2 @ X8 )
| ~ ( v4 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v2 @ Y0 ) ) ) )
| ~ ( v3 @ X2 ) ),
inference(lazy_cnf_or,[status(thm)],[zip_derived_cl1433]) ).
thf(zip_derived_cl37_022,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl848_023,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( rel_s4 @ X1 @ X2 )
| ~ ( v4 @ X2 )
| ~ ( rel_s4 @ X0 @ X1 )
| ~ ( v2 @ X0 )
| ( v3 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl845,zip_derived_cl37]) ).
thf(zip_derived_cl849,plain,
! [X0: $i,X1: $i] :
( ( v3 @ X1 )
| ~ ( v2 @ X1 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v4 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl37,zip_derived_cl848]) ).
thf(zip_derived_cl1005_024,plain,
! [X0: $i] : ( v2 @ X0 ),
inference(clc,[status(thm)],[zip_derived_cl997,zip_derived_cl490]) ).
thf(zip_derived_cl1019,plain,
! [X0: $i,X1: $i] :
( ( v3 @ X1 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v4 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl849,zip_derived_cl1005]) ).
thf(zip_derived_cl1435,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( !!
@ ^ [Y0: $i] :
( ( (~) @ ( rel_s4 @ X2 @ Y0 ) )
| ( (~) @ ( v2 @ Y0 ) ) ) )
| ~ ( rel_s4 @ X2 @ X4 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v4 @ X8 )
| ~ ( rel_s4 @ X2 @ X8 ) ),
inference(clc,[status(thm)],[zip_derived_cl1434,zip_derived_cl1019]) ).
thf(zip_derived_cl1436,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X10 ) )
| ( (~) @ ( v2 @ X10 ) )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( v4 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1435]) ).
thf(zip_derived_cl1005_025,plain,
! [X0: $i] : ( v2 @ X0 ),
inference(clc,[status(thm)],[zip_derived_cl997,zip_derived_cl490]) ).
thf(zip_derived_cl1437,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X10 ) )
| ( (~) @ $true )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( v4 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference(demod,[status(thm)],[zip_derived_cl1436,zip_derived_cl1005]) ).
thf(zip_derived_cl1438,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( (~) @ ( rel_s4 @ X2 @ X10 ) )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( v4 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference('simplify boolean subterms',[status(thm)],[zip_derived_cl1437]) ).
thf(zip_derived_cl1439,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( rel_s4 @ X2 @ X10 )
| ~ ( rel_s4 @ X2 @ X8 )
| ~ ( v4 @ X8 )
| ~ ( rel_s4 @ X4 @ X6 )
| ~ ( v3 @ X6 )
| ~ ( rel_s4 @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl1438]) ).
thf(zip_derived_cl1440,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( rel_s4 @ X1 @ X0 )
| ~ ( rel_s4 @ X1 @ X2 )
| ~ ( v4 @ X2 )
| ~ ( rel_s4 @ X0 @ X3 )
| ~ ( v3 @ X3 ) ),
inference(condensation,[status(thm)],[zip_derived_cl1439]) ).
thf(zip_derived_cl1451,plain,
! [X0: $i,X1: $i] :
( ~ ( v3 @ X0 )
| ~ ( rel_s4 @ X0 @ X0 )
| ~ ( v4 @ X1 )
| ~ ( rel_s4 @ X0 @ X1 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl1440]) ).
thf(zip_derived_cl37_026,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl1452,plain,
! [X0: $i,X1: $i] :
( ~ ( v3 @ X0 )
| ~ ( v4 @ X1 )
| ~ ( rel_s4 @ X0 @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl1451,zip_derived_cl37]) ).
thf(zip_derived_cl1019_027,plain,
! [X0: $i,X1: $i] :
( ( v3 @ X1 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v4 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl849,zip_derived_cl1005]) ).
thf(zip_derived_cl1453,plain,
! [X0: $i,X1: $i] :
( ~ ( rel_s4 @ X0 @ X1 )
| ~ ( v4 @ X1 ) ),
inference(clc,[status(thm)],[zip_derived_cl1452,zip_derived_cl1019]) ).
thf(zip_derived_cl1454,plain,
! [X0: $i] :
~ ( v4 @ X0 ),
inference('sup-',[status(thm)],[zip_derived_cl37,zip_derived_cl1453]) ).
thf(zip_derived_cl1786,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( v1 @ X0 )
| ~ ( rel_s4 @ X2 @ X3 )
| ~ ( rel_s4 @ X1 @ X2 )
| ~ ( rel_s4 @ X1 @ X0 )
| ( v1 @ X1 ) ),
inference(clc,[status(thm)],[zip_derived_cl1785,zip_derived_cl1454]) ).
thf(zip_derived_cl1289_028,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( v1 @ X1 )
| ~ ( v4 @ X3 )
| ~ ( rel_s4 @ X0 @ X3 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v1 @ X2 )
| ~ ( rel_s4 @ X0 @ X2 ) ),
inference(clc,[status(thm)],[zip_derived_cl718,zip_derived_cl1018]) ).
thf(zip_derived_cl1299,plain,
! [X0: $i,X1: $i] :
( ~ ( rel_s4 @ X0 @ X1 )
| ~ ( v1 @ X1 )
| ~ ( rel_s4 @ X0 @ X0 )
| ~ ( v4 @ X0 )
| ( v1 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl1289]) ).
thf(zip_derived_cl37_029,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl1301,plain,
! [X0: $i,X1: $i] :
( ~ ( rel_s4 @ X0 @ X1 )
| ~ ( v1 @ X1 )
| ~ ( v4 @ X0 )
| ( v1 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl1299,zip_derived_cl37]) ).
thf(zip_derived_cl37_030,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl143_031,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( v1 @ X1 )
| ~ ( v2 @ X1 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( v1 @ X2 )
| ~ ( rel_s4 @ X0 @ X2 )
| ( v4 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl141,zip_derived_cl37]) ).
thf(zip_derived_cl161,plain,
! [X0: $i,X1: $i] :
( ( v4 @ X0 )
| ~ ( rel_s4 @ X0 @ X1 )
| ~ ( v1 @ X1 )
| ~ ( v2 @ X0 )
| ( v1 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl37,zip_derived_cl143]) ).
thf(zip_derived_cl1005_032,plain,
! [X0: $i] : ( v2 @ X0 ),
inference(clc,[status(thm)],[zip_derived_cl997,zip_derived_cl490]) ).
thf(zip_derived_cl1016,plain,
! [X0: $i,X1: $i] :
( ( v4 @ X0 )
| ~ ( rel_s4 @ X0 @ X1 )
| ~ ( v1 @ X1 )
| ( v1 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl161,zip_derived_cl1005]) ).
thf(zip_derived_cl1329,plain,
! [X0: $i,X1: $i] :
( ( v1 @ X0 )
| ~ ( v1 @ X1 )
| ~ ( rel_s4 @ X0 @ X1 ) ),
inference(clc,[status(thm)],[zip_derived_cl1301,zip_derived_cl1016]) ).
thf(zip_derived_cl1787,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( v1 @ X1 )
| ~ ( rel_s4 @ X1 @ X0 )
| ~ ( rel_s4 @ X1 @ X2 )
| ~ ( rel_s4 @ X2 @ X3 ) ),
inference(clc,[status(thm)],[zip_derived_cl1786,zip_derived_cl1329]) ).
thf(zip_derived_cl1788,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( v1 @ X0 )
| ~ ( rel_s4 @ X2 @ X1 )
| ~ ( rel_s4 @ X0 @ X2 ) ),
inference(condensation,[status(thm)],[zip_derived_cl1787]) ).
thf(zip_derived_cl1799,plain,
! [X0: $i] :
( ~ ( rel_s4 @ X0 @ X0 )
| ( v1 @ X0 ) ),
inference(eq_fact,[status(thm)],[zip_derived_cl1788]) ).
thf(zip_derived_cl37_033,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl1800,plain,
! [X0: $i] : ( v1 @ X0 ),
inference(demod,[status(thm)],[zip_derived_cl1799,zip_derived_cl37]) ).
thf(zip_derived_cl1803,plain,
! [X0: $i] :
~ ( v3 @ X0 ),
inference(demod,[status(thm)],[zip_derived_cl1395,zip_derived_cl1800]) ).
thf(zip_derived_cl1800_034,plain,
! [X0: $i] : ( v1 @ X0 ),
inference(demod,[status(thm)],[zip_derived_cl1799,zip_derived_cl37]) ).
thf(zip_derived_cl1866,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( rel_s4 @ X1 @ X0 )
| ~ ( rel_s4 @ X2 @ X1 )
| ( v4 @ X2 ) ),
inference(demod,[status(thm)],[zip_derived_cl1181,zip_derived_cl1803,zip_derived_cl1800]) ).
thf(zip_derived_cl1454_035,plain,
! [X0: $i] :
~ ( v4 @ X0 ),
inference('sup-',[status(thm)],[zip_derived_cl37,zip_derived_cl1453]) ).
thf(zip_derived_cl1867,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( rel_s4 @ X2 @ X1 )
| ~ ( rel_s4 @ X1 @ X0 ) ),
inference(clc,[status(thm)],[zip_derived_cl1866,zip_derived_cl1454]) ).
thf(zip_derived_cl1878,plain,
! [X0: $i] :
~ ( rel_s4 @ X0 @ X0 ),
inference(eq_fact,[status(thm)],[zip_derived_cl1867]) ).
thf(zip_derived_cl37_036,plain,
! [X2: $i] : ( rel_s4 @ X2 @ X2 ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl1]) ).
thf(zip_derived_cl1879,plain,
$false,
inference(demod,[status(thm)],[zip_derived_cl1878,zip_derived_cl37]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : SYN741^7 : TPTP v9.2.0. Released v5.5.0.
% 0.00/0.09 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.BU3o1V09ef true
% 0.08/0.28 % Computer : n006.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Wed Oct 1 13:31:08 EDT 2025
% 0.08/0.28 % CPUTime :
% 0.08/0.28 % Running portfolio for 300 s
% 0.08/0.28 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.28 % Number of cores: 8
% 0.08/0.28 % Python version: Python 3.6.8
% 0.08/0.28 % Running in HO mode
% 0.38/0.54 % Total configuration time : 828
% 0.38/0.54 % Estimated wc time : 1656
% 0.38/0.54 % Estimated cpu time (8 cpus) : 207.0
% 0.44/0.64 % /export/starexec/sandbox2/solver/bin/lams/40_c.s.sh running for 80s
% 0.44/0.66 % /export/starexec/sandbox2/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.44/0.66 % /export/starexec/sandbox2/solver/bin/lams/15_e_short1.sh running for 30s
% 0.44/0.66 % /export/starexec/sandbox2/solver/bin/lams/40_c_ic.sh running for 80s
% 0.44/0.66 % /export/starexec/sandbox2/solver/bin/lams/40_noforms.sh running for 90s
% 0.44/0.69 % /export/starexec/sandbox2/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.53/0.69 % /export/starexec/sandbox2/solver/bin/lams/40_b.comb.sh running for 70s
% 0.53/0.72 % /export/starexec/sandbox2/solver/bin/lams/30_sp5.sh running for 60s
% 0.53/0.76 % /export/starexec/sandbox2/solver/bin/lams/30_b.l.sh running for 90s
% 0.53/0.77 % /export/starexec/sandbox2/solver/bin/lams/35_full_unif.sh running for 56s
% 0.53/0.79 % /export/starexec/sandbox2/solver/bin/lams/15_old_s4.sh running for 30s
% 0.55/1.02 % /export/starexec/sandbox2/solver/bin/lams/15_lifting3.sh running for 30s
% 5.79/1.49 % /export/starexec/sandbox2/solver/bin/lams/33_shallow_sine.sh running for 66s
% 7.56/1.69 % /export/starexec/sandbox2/solver/bin/lams/40_e_lift.sh running for 80s
% 12.25/2.43 % Solved by lams/15_lifting3.sh.
% 12.25/2.43 % done 409 iterations in 1.237s
% 12.25/2.43 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 12.25/2.43 % SZS output start Refutation
% See solution above
% 12.25/2.44
% 12.25/2.44
% 12.25/2.44 % Terminating...
% 12.68/2.58 % Runner terminated.
% 12.70/2.60 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------