%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : LCL489+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.caIxLZeWRu true
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 01:36:04 PM UTC 2026
% Result : Theorem 235.84s 39.94s
% Output : Refutation 235.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 24
% Syntax : Number of formulae : 299 ( 209 unt; 0 typ; 0 def)
% Number of atoms : 417 ( 139 equ; 0 cnn)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 1931 ( 107 ~; 103 |; 1 &;1706 @)
% ( 7 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 22 ( 20 usr; 15 con; 0-2 aty)
% Number of variables : 519 ( 0 ^; 519 !; 0 ?; 519 :)
% Comments :
%------------------------------------------------------------------------------
thf(op_or_type,type,
op_or: $o ).
thf(op_and_type,type,
op_and: $o ).
thf(and_type,type,
and: $i > $i > $i ).
thf(is_a_theorem_type,type,
is_a_theorem: $i > $o ).
thf(r2_type,type,
r2: $o ).
thf(sk__18_type,type,
sk__18: $i ).
thf(op_equiv_type,type,
op_equiv: $o ).
thf(r1_type,type,
r1: $o ).
thf(op_implies_and_type,type,
op_implies_and: $o ).
thf(or_type,type,
or: $i > $i > $i ).
thf(op_implies_or_type,type,
op_implies_or: $o ).
thf(r3_type,type,
r3: $o ).
thf(equiv_type,type,
equiv: $i > $i > $i ).
thf(and_3_type,type,
and_3: $o ).
thf(modus_ponens_type,type,
modus_ponens: $o ).
thf(r4_type,type,
r4: $o ).
thf(sk__17_type,type,
sk__17: $i ).
thf(implies_type,type,
implies: $i > $i > $i ).
thf(substitution_of_equivalents_type,type,
substitution_of_equivalents: $o ).
thf(not_type,type,
not: $i > $i ).
thf(and_3,axiom,
( and_3
<=> ! [X: $i,Y: $i] : ( is_a_theorem @ ( implies @ X @ ( implies @ Y @ ( and @ X @ Y ) ) ) ) ) ).
thf(zip_derived_cl20,plain,
( and_3
| ~ ( is_a_theorem @ ( implies @ sk__17 @ ( implies @ sk__18 @ ( and @ sk__17 @ sk__18 ) ) ) ) ),
inference(cnf,[status(esa)],[and_3]) ).
thf(hilbert_and_3,conjecture,
and_3 ).
thf(zf_stmt_0,negated_conjecture,
~ and_3,
inference('cnf.neg',[status(esa)],[hilbert_and_3]) ).
thf(zip_derived_cl73,plain,
~ and_3,
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl111,plain,
~ ( is_a_theorem @ ( implies @ sk__17 @ ( implies @ sk__18 @ ( and @ sk__17 @ sk__18 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl20,zip_derived_cl73]) ).
thf(op_implies_or,axiom,
( op_implies_or
=> ! [X: $i,Y: $i] :
( ( implies @ X @ Y )
= ( or @ ( not @ X ) @ Y ) ) ) ).
thf(zip_derived_cl58,plain,
! [X0: $i,X1: $i] :
( ( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) )
| ~ op_implies_or ),
inference(cnf,[status(esa)],[op_implies_or]) ).
thf(principia_op_implies_or,axiom,
op_implies_or ).
thf(zip_derived_cl60,plain,
op_implies_or,
inference(cnf,[status(esa)],[principia_op_implies_or]) ).
thf(zip_derived_cl88,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(r2,axiom,
( r2
<=> ! [P: $i,Q: $i] : ( is_a_theorem @ ( implies @ Q @ ( or @ P @ Q ) ) ) ) ).
thf(zip_derived_cl47,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ ( implies @ X0 @ ( or @ X1 @ X0 ) ) )
| ~ r2 ),
inference(cnf,[status(esa)],[r2]) ).
thf(principia_r2,axiom,
r2 ).
thf(zip_derived_cl65,plain,
r2,
inference(cnf,[status(esa)],[principia_r2]) ).
thf(zip_derived_cl85,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ X0 @ ( or @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl47,zip_derived_cl65]) ).
thf(modus_ponens,axiom,
( modus_ponens
<=> ! [X: $i,Y: $i] :
( ( ( is_a_theorem @ X )
& ( is_a_theorem @ ( implies @ X @ Y ) ) )
=> ( is_a_theorem @ Y ) ) ) ).
thf(zip_derived_cl0,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ X0 )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ~ ( is_a_theorem @ X1 )
| ~ modus_ponens ),
inference(cnf,[status(esa)],[modus_ponens]) ).
thf(principia_modus_ponens,axiom,
modus_ponens ).
thf(zip_derived_cl63,plain,
modus_ponens,
inference(cnf,[status(esa)],[principia_modus_ponens]) ).
thf(zip_derived_cl74,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ X0 )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ~ ( is_a_theorem @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl0,zip_derived_cl63]) ).
thf(zip_derived_cl87,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ X0 )
| ( is_a_theorem @ ( or @ X1 @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl85,zip_derived_cl74]) ).
thf(zip_derived_cl99,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ~ ( is_a_theorem @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl88,zip_derived_cl87]) ).
thf(zip_derived_cl99_001,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ~ ( is_a_theorem @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl88,zip_derived_cl87]) ).
thf(op_equiv,axiom,
( op_equiv
=> ! [X: $i,Y: $i] :
( ( equiv @ X @ Y )
= ( and @ ( implies @ X @ Y ) @ ( implies @ Y @ X ) ) ) ) ).
thf(zip_derived_cl59,plain,
! [X0: $i,X1: $i] :
( ( ( equiv @ X0 @ X1 )
= ( and @ ( implies @ X0 @ X1 ) @ ( implies @ X1 @ X0 ) ) )
| ~ op_equiv ),
inference(cnf,[status(esa)],[op_equiv]) ).
thf(principia_op_equiv,axiom,
op_equiv ).
thf(zip_derived_cl62,plain,
op_equiv,
inference(cnf,[status(esa)],[principia_op_equiv]) ).
thf(zip_derived_cl176,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ X1 )
= ( and @ ( implies @ X0 @ X1 ) @ ( implies @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl59,zip_derived_cl62]) ).
thf(zip_derived_cl88_002,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(r1,axiom,
( r1
<=> ! [P: $i] : ( is_a_theorem @ ( implies @ ( or @ P @ P ) @ P ) ) ) ).
thf(zip_derived_cl45,plain,
! [X0: $i] :
( ( is_a_theorem @ ( implies @ ( or @ X0 @ X0 ) @ X0 ) )
| ~ r1 ),
inference(cnf,[status(esa)],[r1]) ).
thf(principia_r1,axiom,
r1 ).
thf(zip_derived_cl64,plain,
r1,
inference(cnf,[status(esa)],[principia_r1]) ).
thf(zip_derived_cl83,plain,
! [X0: $i] : ( is_a_theorem @ ( implies @ ( or @ X0 @ X0 ) @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl45,zip_derived_cl64]) ).
thf(zip_derived_cl90,plain,
! [X0: $i] : ( is_a_theorem @ ( implies @ ( implies @ X0 @ ( not @ X0 ) ) @ ( not @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl88,zip_derived_cl83]) ).
thf(zip_derived_cl88_003,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(r3,axiom,
( r3
<=> ! [P: $i,Q: $i] : ( is_a_theorem @ ( implies @ ( or @ P @ Q ) @ ( or @ Q @ P ) ) ) ) ).
thf(zip_derived_cl49,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ ( implies @ ( or @ X0 @ X1 ) @ ( or @ X1 @ X0 ) ) )
| ~ r3 ),
inference(cnf,[status(esa)],[r3]) ).
thf(principia_r3,axiom,
r3 ).
thf(zip_derived_cl66,plain,
r3,
inference(cnf,[status(esa)],[principia_r3]) ).
thf(zip_derived_cl123,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ ( or @ X0 @ X1 ) @ ( or @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl49,zip_derived_cl66]) ).
thf(zip_derived_cl74_004,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ X0 )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ~ ( is_a_theorem @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl0,zip_derived_cl63]) ).
thf(zip_derived_cl124,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( or @ X0 @ X1 ) )
| ( is_a_theorem @ ( or @ X1 @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl123,zip_derived_cl74]) ).
thf(zip_derived_cl211,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ( is_a_theorem @ ( or @ X0 @ ( not @ X1 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl88,zip_derived_cl124]) ).
thf(zip_derived_cl314,plain,
! [X0: $i] : ( is_a_theorem @ ( or @ ( not @ X0 ) @ ( not @ ( implies @ X0 @ ( not @ X0 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl90,zip_derived_cl211]) ).
thf(op_and,axiom,
( op_and
=> ! [X: $i,Y: $i] :
( ( and @ X @ Y )
= ( not @ ( or @ ( not @ X ) @ ( not @ Y ) ) ) ) ) ).
thf(zip_derived_cl56,plain,
! [X0: $i,X1: $i] :
( ( ( and @ X0 @ X1 )
= ( not @ ( or @ ( not @ X0 ) @ ( not @ X1 ) ) ) )
| ~ op_and ),
inference(cnf,[status(esa)],[op_and]) ).
thf(zip_derived_cl88_005,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(principia_op_and,axiom,
op_and ).
thf(zip_derived_cl61,plain,
op_and,
inference(cnf,[status(esa)],[principia_op_and]) ).
thf(zip_derived_cl142,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( not @ ( implies @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56,zip_derived_cl88,zip_derived_cl61]) ).
thf(zip_derived_cl88_006,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl319,plain,
! [X0: $i] : ( is_a_theorem @ ( implies @ X0 @ ( and @ X0 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl314,zip_derived_cl142,zip_derived_cl88]) ).
thf(zip_derived_cl74_007,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ X0 )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ~ ( is_a_theorem @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl0,zip_derived_cl63]) ).
thf(zip_derived_cl321,plain,
! [X0: $i] :
( ~ ( is_a_theorem @ X0 )
| ( is_a_theorem @ ( and @ X0 @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl319,zip_derived_cl74]) ).
thf(zip_derived_cl142_008,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( not @ ( implies @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56,zip_derived_cl88,zip_derived_cl61]) ).
thf(zip_derived_cl88_009,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl85_010,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ X0 @ ( or @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl47,zip_derived_cl65]) ).
thf(zip_derived_cl89,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ X0 @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl88,zip_derived_cl85]) ).
thf(zip_derived_cl211_011,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ( is_a_theorem @ ( or @ X0 @ ( not @ X1 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl88,zip_derived_cl124]) ).
thf(zip_derived_cl311,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( or @ ( implies @ X1 @ X0 ) @ ( not @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl89,zip_derived_cl211]) ).
thf(op_or,axiom,
( op_or
=> ! [X: $i,Y: $i] :
( ( or @ X @ Y )
= ( not @ ( and @ ( not @ X ) @ ( not @ Y ) ) ) ) ) ).
thf(zip_derived_cl55,plain,
! [X0: $i,X1: $i] :
( ( ( or @ X0 @ X1 )
= ( not @ ( and @ ( not @ X0 ) @ ( not @ X1 ) ) ) )
| ~ op_or ),
inference(cnf,[status(esa)],[op_or]) ).
thf(hilbert_op_or,axiom,
op_or ).
thf(zip_derived_cl70,plain,
op_or,
inference(cnf,[status(esa)],[hilbert_op_or]) ).
thf(zip_derived_cl127,plain,
! [X0: $i,X1: $i] :
( ( or @ X0 @ X1 )
= ( not @ ( and @ ( not @ X0 ) @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl55,zip_derived_cl70]) ).
thf(op_implies_and,axiom,
( op_implies_and
=> ! [X: $i,Y: $i] :
( ( implies @ X @ Y )
= ( not @ ( and @ X @ ( not @ Y ) ) ) ) ) ).
thf(zip_derived_cl57,plain,
! [X0: $i,X1: $i] :
( ( ( implies @ X0 @ X1 )
= ( not @ ( and @ X0 @ ( not @ X1 ) ) ) )
| ~ op_implies_and ),
inference(cnf,[status(esa)],[op_implies_and]) ).
thf(hilbert_op_implies_and,axiom,
op_implies_and ).
thf(zip_derived_cl71,plain,
op_implies_and,
inference(cnf,[status(esa)],[hilbert_op_implies_and]) ).
thf(zip_derived_cl91,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( not @ ( and @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl57,zip_derived_cl71]) ).
thf(zip_derived_cl133,plain,
! [X0: $i,X1: $i] :
( ( implies @ ( not @ X1 ) @ X0 )
= ( or @ X1 @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl127,zip_derived_cl91]) ).
thf(zip_derived_cl74_012,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ X0 )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ~ ( is_a_theorem @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl0,zip_derived_cl63]) ).
thf(zip_derived_cl160,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( or @ X1 @ X0 ) )
| ~ ( is_a_theorem @ ( not @ X1 ) )
| ( is_a_theorem @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl133,zip_derived_cl74]) ).
thf(zip_derived_cl336,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ ( not @ X0 ) )
| ~ ( is_a_theorem @ ( not @ ( implies @ X1 @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl311,zip_derived_cl160]) ).
thf(zip_derived_cl379,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( and @ X1 @ X0 ) )
| ( is_a_theorem @ ( not @ ( not @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl142,zip_derived_cl336]) ).
thf(zip_derived_cl384,plain,
! [X0: $i] :
( ~ ( is_a_theorem @ X0 )
| ( is_a_theorem @ ( not @ ( not @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl321,zip_derived_cl379]) ).
thf(zip_derived_cl88_013,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(r4,axiom,
( r4
<=> ! [P: $i,Q: $i,R: $i] : ( is_a_theorem @ ( implies @ ( or @ P @ ( or @ Q @ R ) ) @ ( or @ Q @ ( or @ P @ R ) ) ) ) ) ).
thf(zip_derived_cl51,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( is_a_theorem @ ( implies @ ( or @ X0 @ ( or @ X1 @ X2 ) ) @ ( or @ X1 @ ( or @ X0 @ X2 ) ) ) )
| ~ r4 ),
inference(cnf,[status(esa)],[r4]) ).
thf(principia_r4,axiom,
r4 ).
thf(zip_derived_cl67,plain,
r4,
inference(cnf,[status(esa)],[principia_r4]) ).
thf(zip_derived_cl219,plain,
! [X0: $i,X1: $i,X2: $i] : ( is_a_theorem @ ( implies @ ( or @ X0 @ ( or @ X1 @ X2 ) ) @ ( or @ X1 @ ( or @ X0 @ X2 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl51,zip_derived_cl67]) ).
thf(zip_derived_cl222,plain,
! [X0: $i,X1: $i,X2: $i] : ( is_a_theorem @ ( implies @ ( or @ ( not @ X1 ) @ ( or @ X2 @ X0 ) ) @ ( or @ X2 @ ( implies @ X1 @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl88,zip_derived_cl219]) ).
thf(zip_derived_cl88_014,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl226,plain,
! [X0: $i,X1: $i,X2: $i] : ( is_a_theorem @ ( implies @ ( implies @ X1 @ ( or @ X2 @ X0 ) ) @ ( or @ X2 @ ( implies @ X1 @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl222,zip_derived_cl88]) ).
thf(zip_derived_cl176_015,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ X1 )
= ( and @ ( implies @ X0 @ X1 ) @ ( implies @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl59,zip_derived_cl62]) ).
thf(zip_derived_cl321_016,plain,
! [X0: $i] :
( ~ ( is_a_theorem @ X0 )
| ( is_a_theorem @ ( and @ X0 @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl319,zip_derived_cl74]) ).
thf(zip_derived_cl328,plain,
! [X0: $i] :
( ( is_a_theorem @ ( equiv @ X0 @ X0 ) )
| ~ ( is_a_theorem @ ( implies @ X0 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl176,zip_derived_cl321]) ).
thf(zip_derived_cl133_017,plain,
! [X0: $i,X1: $i] :
( ( implies @ ( not @ X1 ) @ X0 )
= ( or @ X1 @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl127,zip_derived_cl91]) ).
thf(zip_derived_cl85_018,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ X0 @ ( or @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl47,zip_derived_cl65]) ).
thf(zip_derived_cl166,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( or @ X0 @ ( or @ X1 @ ( not @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl133,zip_derived_cl85]) ).
thf(zip_derived_cl219_019,plain,
! [X0: $i,X1: $i,X2: $i] : ( is_a_theorem @ ( implies @ ( or @ X0 @ ( or @ X1 @ X2 ) ) @ ( or @ X1 @ ( or @ X0 @ X2 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl51,zip_derived_cl67]) ).
thf(zip_derived_cl74_020,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ X0 )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ~ ( is_a_theorem @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl0,zip_derived_cl63]) ).
thf(zip_derived_cl220,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( is_a_theorem @ ( or @ X1 @ ( or @ X2 @ X0 ) ) )
| ( is_a_theorem @ ( or @ X2 @ ( or @ X1 @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl219,zip_derived_cl74]) ).
thf(zip_derived_cl7360,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( or @ X1 @ ( or @ X0 @ ( not @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl166,zip_derived_cl220]) ).
thf(zip_derived_cl83_021,plain,
! [X0: $i] : ( is_a_theorem @ ( implies @ ( or @ X0 @ X0 ) @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl45,zip_derived_cl64]) ).
thf(zip_derived_cl74_022,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ X0 )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ~ ( is_a_theorem @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl0,zip_derived_cl63]) ).
thf(zip_derived_cl84,plain,
! [X0: $i] :
( ~ ( is_a_theorem @ ( or @ X0 @ X0 ) )
| ( is_a_theorem @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl83,zip_derived_cl74]) ).
thf(zip_derived_cl7415,plain,
! [X0: $i] : ( is_a_theorem @ ( or @ X0 @ ( not @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl7360,zip_derived_cl84]) ).
thf(zip_derived_cl88_023,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl123_024,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ ( or @ X0 @ X1 ) @ ( or @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl49,zip_derived_cl66]) ).
thf(zip_derived_cl125,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ ( or @ X0 @ ( not @ X1 ) ) @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl88,zip_derived_cl123]) ).
thf(zip_derived_cl74_025,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ X0 )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ~ ( is_a_theorem @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl0,zip_derived_cl63]) ).
thf(zip_derived_cl723,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( or @ X0 @ ( not @ X1 ) ) )
| ( is_a_theorem @ ( implies @ X1 @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl125,zip_derived_cl74]) ).
thf(zip_derived_cl7471,plain,
! [X0: $i] : ( is_a_theorem @ ( implies @ X0 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl7415,zip_derived_cl723]) ).
thf(zip_derived_cl7505,plain,
! [X0: $i] : ( is_a_theorem @ ( equiv @ X0 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl328,zip_derived_cl7471]) ).
thf(zip_derived_cl176_026,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ X1 )
= ( and @ ( implies @ X0 @ X1 ) @ ( implies @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl59,zip_derived_cl62]) ).
thf(zip_derived_cl379_027,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( and @ X1 @ X0 ) )
| ( is_a_theorem @ ( not @ ( not @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl142,zip_derived_cl336]) ).
thf(zip_derived_cl385,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( equiv @ X1 @ X0 ) )
| ( is_a_theorem @ ( not @ ( not @ ( implies @ X0 @ X1 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl176,zip_derived_cl379]) ).
thf(zip_derived_cl7586,plain,
! [X0: $i] : ( is_a_theorem @ ( not @ ( not @ ( implies @ X0 @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl7505,zip_derived_cl385]) ).
thf(zip_derived_cl88_028,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl160_029,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( or @ X1 @ X0 ) )
| ~ ( is_a_theorem @ ( not @ X1 ) )
| ( is_a_theorem @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl133,zip_derived_cl74]) ).
thf(zip_derived_cl208,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ( is_a_theorem @ X0 )
| ~ ( is_a_theorem @ ( not @ ( not @ X1 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl88,zip_derived_cl160]) ).
thf(zip_derived_cl8000,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ X1 )
| ~ ( is_a_theorem @ ( implies @ ( implies @ X0 @ X0 ) @ X1 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl7586,zip_derived_cl208]) ).
thf(zip_derived_cl8163,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( or @ X1 @ ( implies @ ( or @ X1 @ X0 ) @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl226,zip_derived_cl8000]) ).
thf(zip_derived_cl160_030,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( or @ X1 @ X0 ) )
| ~ ( is_a_theorem @ ( not @ X1 ) )
| ( is_a_theorem @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl133,zip_derived_cl74]) ).
thf(zip_derived_cl14128,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ ( implies @ ( or @ X1 @ X0 ) @ X0 ) )
| ~ ( is_a_theorem @ ( not @ X1 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl8163,zip_derived_cl160]) ).
thf(zip_derived_cl14183,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ X0 )
| ( is_a_theorem @ ( implies @ ( or @ ( not @ X0 ) @ X1 ) @ X1 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl384,zip_derived_cl14128]) ).
thf(zip_derived_cl88_031,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl14212,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ X0 )
| ( is_a_theorem @ ( implies @ ( implies @ X0 @ X1 ) @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl14183,zip_derived_cl88]) ).
thf(zip_derived_cl88_032,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl723_033,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( or @ X0 @ ( not @ X1 ) ) )
| ( is_a_theorem @ ( implies @ X1 @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl125,zip_derived_cl74]) ).
thf(zip_derived_cl753,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( implies @ X1 @ ( not @ X0 ) ) )
| ( is_a_theorem @ ( implies @ X0 @ ( not @ X1 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl88,zip_derived_cl723]) ).
thf(zip_derived_cl18500,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ X1 )
| ( is_a_theorem @ ( implies @ X0 @ ( not @ ( implies @ X1 @ ( not @ X0 ) ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl14212,zip_derived_cl753]) ).
thf(zip_derived_cl142_034,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( not @ ( implies @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56,zip_derived_cl88,zip_derived_cl61]) ).
thf(zip_derived_cl18521,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ X1 )
| ( is_a_theorem @ ( implies @ X0 @ ( and @ X1 @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl18500,zip_derived_cl142]) ).
thf(zip_derived_cl74_035,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ X0 )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ~ ( is_a_theorem @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl0,zip_derived_cl63]) ).
thf(zip_derived_cl18858,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ X1 )
| ~ ( is_a_theorem @ X0 )
| ( is_a_theorem @ ( and @ X1 @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl18521,zip_derived_cl74]) ).
thf(zip_derived_cl19452,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ ( equiv @ X1 @ X0 ) )
| ~ ( is_a_theorem @ ( implies @ X0 @ X1 ) )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl176,zip_derived_cl18858]) ).
thf(zip_derived_cl30726,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ X0 )
| ~ ( is_a_theorem @ ( implies @ X0 @ X1 ) )
| ( is_a_theorem @ ( equiv @ X0 @ X1 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl99,zip_derived_cl19452]) ).
thf(zip_derived_cl30858,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ X0 )
| ( is_a_theorem @ ( equiv @ X1 @ X0 ) )
| ~ ( is_a_theorem @ X1 ) ),
inference('sup-',[status(thm)],[zip_derived_cl99,zip_derived_cl30726]) ).
thf(substitution_of_equivalents,axiom,
( substitution_of_equivalents
<=> ! [X: $i,Y: $i] :
( ( is_a_theorem @ ( equiv @ X @ Y ) )
=> ( X = Y ) ) ) ).
thf(zip_derived_cl4,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( equiv @ X0 @ X1 ) )
| ( X0 = X1 )
| ~ substitution_of_equivalents ),
inference(cnf,[status(esa)],[substitution_of_equivalents]) ).
thf(use_substitution_of_equivalents,axiom,
substitution_of_equivalents ).
thf(zip_derived_cl69,plain,
substitution_of_equivalents,
inference(cnf,[status(esa)],[use_substitution_of_equivalents]) ).
thf(zip_derived_cl78,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( equiv @ X0 @ X1 ) )
| ( X0 = X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl4,zip_derived_cl69]) ).
thf(zip_derived_cl30946,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ X1 )
| ~ ( is_a_theorem @ X0 )
| ( X1 = X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl30858,zip_derived_cl78]) ).
thf(zip_derived_cl7505_036,plain,
! [X0: $i] : ( is_a_theorem @ ( equiv @ X0 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl328,zip_derived_cl7471]) ).
thf(zip_derived_cl32402,plain,
! [X0: $i,X1: $i] :
( ( ( equiv @ X0 @ X0 )
= X1 )
| ~ ( is_a_theorem @ X1 ) ),
inference('sup+',[status(thm)],[zip_derived_cl30946,zip_derived_cl7505]) ).
thf(zip_derived_cl89_037,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ X0 @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl88,zip_derived_cl85]) ).
thf(zip_derived_cl40770,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( equiv @ X2 @ X2 )
= ( implies @ X0 @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl32402,zip_derived_cl89]) ).
thf(zip_derived_cl142_038,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( not @ ( implies @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56,zip_derived_cl88,zip_derived_cl61]) ).
thf(zip_derived_cl88_039,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl143,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( implies @ ( implies @ X1 @ ( not @ X0 ) ) @ X2 )
= ( or @ ( and @ X1 @ X0 ) @ X2 ) ),
inference('sup+',[status(thm)],[zip_derived_cl142,zip_derived_cl88]) ).
thf(zip_derived_cl176_040,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ X1 )
= ( and @ ( implies @ X0 @ X1 ) @ ( implies @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl59,zip_derived_cl62]) ).
thf(zip_derived_cl2099,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( equiv @ X0 @ ( implies @ X2 @ ( not @ X1 ) ) )
= ( and @ ( implies @ X0 @ ( implies @ X2 @ ( not @ X1 ) ) ) @ ( or @ ( and @ X2 @ X1 ) @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl143,zip_derived_cl176]) ).
thf(zip_derived_cl62609,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( equiv @ ( not @ X1 ) @ ( implies @ X2 @ ( not @ X1 ) ) )
= ( and @ ( equiv @ X0 @ X0 ) @ ( or @ ( and @ X2 @ X1 ) @ ( not @ X1 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl40770,zip_derived_cl2099]) ).
thf(zip_derived_cl88_041,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl7415_042,plain,
! [X0: $i] : ( is_a_theorem @ ( or @ X0 @ ( not @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl7360,zip_derived_cl84]) ).
thf(zip_derived_cl7476,plain,
! [X0: $i] : ( is_a_theorem @ ( implies @ X0 @ ( not @ ( not @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl88,zip_derived_cl7415]) ).
thf(zip_derived_cl19452_043,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ ( equiv @ X1 @ X0 ) )
| ~ ( is_a_theorem @ ( implies @ X0 @ X1 ) )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl176,zip_derived_cl18858]) ).
thf(zip_derived_cl30749,plain,
! [X0: $i] :
( ~ ( is_a_theorem @ ( implies @ ( not @ ( not @ X0 ) ) @ X0 ) )
| ( is_a_theorem @ ( equiv @ ( not @ ( not @ X0 ) ) @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl7476,zip_derived_cl19452]) ).
thf(zip_derived_cl133_044,plain,
! [X0: $i,X1: $i] :
( ( implies @ ( not @ X1 ) @ X0 )
= ( or @ X1 @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl127,zip_derived_cl91]) ).
thf(zip_derived_cl88_045,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl7471_046,plain,
! [X0: $i] : ( is_a_theorem @ ( implies @ X0 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl7415,zip_derived_cl723]) ).
thf(zip_derived_cl30825,plain,
! [X0: $i] : ( is_a_theorem @ ( equiv @ ( not @ ( not @ X0 ) ) @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl30749,zip_derived_cl133,zip_derived_cl88,zip_derived_cl7471]) ).
thf(zip_derived_cl78_047,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( equiv @ X0 @ X1 ) )
| ( X0 = X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl4,zip_derived_cl69]) ).
thf(zip_derived_cl30977,plain,
! [X0: $i] :
( ( not @ ( not @ X0 ) )
= X0 ),
inference('sup-',[status(thm)],[zip_derived_cl30825,zip_derived_cl78]) ).
thf(zip_derived_cl142_048,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( not @ ( implies @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56,zip_derived_cl88,zip_derived_cl61]) ).
thf(zip_derived_cl127_049,plain,
! [X0: $i,X1: $i] :
( ( or @ X0 @ X1 )
= ( not @ ( and @ ( not @ X0 ) @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl55,zip_derived_cl70]) ).
thf(zip_derived_cl145,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( or @ ( implies @ X1 @ ( not @ X0 ) ) @ X2 )
= ( not @ ( and @ ( and @ X1 @ X0 ) @ ( not @ X2 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl142,zip_derived_cl127]) ).
thf(zip_derived_cl91_050,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( not @ ( and @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl57,zip_derived_cl71]) ).
thf(zip_derived_cl153,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( or @ ( implies @ X1 @ ( not @ X0 ) ) @ X2 )
= ( implies @ ( and @ X1 @ X0 ) @ X2 ) ),
inference(demod,[status(thm)],[zip_derived_cl145,zip_derived_cl91]) ).
thf(zip_derived_cl125_051,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ ( or @ X0 @ ( not @ X1 ) ) @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl88,zip_derived_cl123]) ).
thf(zip_derived_cl211_052,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ( is_a_theorem @ ( or @ X0 @ ( not @ X1 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl88,zip_derived_cl124]) ).
thf(zip_derived_cl724,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( or @ ( implies @ X1 @ X0 ) @ ( not @ ( or @ X0 @ ( not @ X1 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl125,zip_derived_cl211]) ).
thf(zip_derived_cl133_053,plain,
! [X0: $i,X1: $i] :
( ( implies @ ( not @ X1 ) @ X0 )
= ( or @ X1 @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl127,zip_derived_cl91]) ).
thf(zip_derived_cl142_054,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( not @ ( implies @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56,zip_derived_cl88,zip_derived_cl61]) ).
thf(zip_derived_cl165,plain,
! [X0: $i,X1: $i] :
( ( and @ ( not @ X1 ) @ X0 )
= ( not @ ( or @ X1 @ ( not @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl133,zip_derived_cl142]) ).
thf(zip_derived_cl736,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( or @ ( implies @ X1 @ X0 ) @ ( and @ ( not @ X0 ) @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl724,zip_derived_cl165]) ).
thf(zip_derived_cl4500,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ ( and @ X0 @ X1 ) @ ( and @ ( not @ ( not @ X1 ) ) @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl153,zip_derived_cl736]) ).
thf(zip_derived_cl88_055,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl165_056,plain,
! [X0: $i,X1: $i] :
( ( and @ ( not @ X1 ) @ X0 )
= ( not @ ( or @ X1 @ ( not @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl133,zip_derived_cl142]) ).
thf(zip_derived_cl198,plain,
! [X0: $i,X1: $i] :
( ( and @ ( not @ ( not @ X1 ) ) @ X0 )
= ( not @ ( implies @ X1 @ ( not @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl88,zip_derived_cl165]) ).
thf(zip_derived_cl142_057,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( not @ ( implies @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56,zip_derived_cl88,zip_derived_cl61]) ).
thf(zip_derived_cl203,plain,
! [X0: $i,X1: $i] :
( ( and @ ( not @ ( not @ X1 ) ) @ X0 )
= ( and @ X1 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl198,zip_derived_cl142]) ).
thf(zip_derived_cl4520,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ ( and @ X0 @ X1 ) @ ( and @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4500,zip_derived_cl203]) ).
thf(zip_derived_cl19452_058,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ ( equiv @ X1 @ X0 ) )
| ~ ( is_a_theorem @ ( implies @ X0 @ X1 ) )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl176,zip_derived_cl18858]) ).
thf(zip_derived_cl30787,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( implies @ ( and @ X1 @ X0 ) @ ( and @ X0 @ X1 ) ) )
| ( is_a_theorem @ ( equiv @ ( and @ X1 @ X0 ) @ ( and @ X0 @ X1 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl4520,zip_derived_cl19452]) ).
thf(zip_derived_cl4520_059,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ ( and @ X0 @ X1 ) @ ( and @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4500,zip_derived_cl203]) ).
thf(zip_derived_cl30844,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( equiv @ ( and @ X1 @ X0 ) @ ( and @ X0 @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl30787,zip_derived_cl4520]) ).
thf(zip_derived_cl78_060,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( equiv @ X0 @ X1 ) )
| ( X0 = X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl4,zip_derived_cl69]) ).
thf(zip_derived_cl45803,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( and @ X1 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl30844,zip_derived_cl78]) ).
thf(zip_derived_cl165_061,plain,
! [X0: $i,X1: $i] :
( ( and @ ( not @ X1 ) @ X0 )
= ( not @ ( or @ X1 @ ( not @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl133,zip_derived_cl142]) ).
thf(zip_derived_cl30977_062,plain,
! [X0: $i] :
( ( not @ ( not @ X0 ) )
= X0 ),
inference('sup-',[status(thm)],[zip_derived_cl30825,zip_derived_cl78]) ).
thf(zip_derived_cl31432,plain,
! [X0: $i,X1: $i] :
( ( not @ ( and @ ( not @ X1 ) @ X0 ) )
= ( or @ X1 @ ( not @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl165,zip_derived_cl30977]) ).
thf(zip_derived_cl46193,plain,
! [X0: $i,X1: $i] :
( ( not @ ( and @ X1 @ ( not @ X0 ) ) )
= ( or @ X0 @ ( not @ X1 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl45803,zip_derived_cl31432]) ).
thf(zip_derived_cl30977_063,plain,
! [X0: $i] :
( ( not @ ( not @ X0 ) )
= X0 ),
inference('sup-',[status(thm)],[zip_derived_cl30825,zip_derived_cl78]) ).
thf(zip_derived_cl142_064,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( not @ ( implies @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56,zip_derived_cl88,zip_derived_cl61]) ).
thf(zip_derived_cl31343,plain,
! [X0: $i,X1: $i] :
( ( and @ X1 @ ( not @ X0 ) )
= ( not @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl30977,zip_derived_cl142]) ).
thf(zip_derived_cl30977_065,plain,
! [X0: $i] :
( ( not @ ( not @ X0 ) )
= X0 ),
inference('sup-',[status(thm)],[zip_derived_cl30825,zip_derived_cl78]) ).
thf(zip_derived_cl46328,plain,
! [X0: $i,X1: $i] :
( ( implies @ X1 @ X0 )
= ( or @ X0 @ ( not @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl46193,zip_derived_cl31343,zip_derived_cl30977]) ).
thf(zip_derived_cl133_066,plain,
! [X0: $i,X1: $i] :
( ( implies @ ( not @ X1 ) @ X0 )
= ( or @ X1 @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl127,zip_derived_cl91]) ).
thf(zip_derived_cl176_067,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ X1 )
= ( and @ ( implies @ X0 @ X1 ) @ ( implies @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl59,zip_derived_cl62]) ).
thf(zip_derived_cl177,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ ( not @ X1 ) )
= ( and @ ( implies @ X0 @ ( not @ X1 ) ) @ ( or @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl133,zip_derived_cl176]) ).
thf(zip_derived_cl46601,plain,
! [X0: $i,X1: $i] :
( ( equiv @ ( not @ X1 ) @ ( not @ X0 ) )
= ( and @ ( implies @ ( not @ X1 ) @ ( not @ X0 ) ) @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl46328,zip_derived_cl177]) ).
thf(zip_derived_cl133_068,plain,
! [X0: $i,X1: $i] :
( ( implies @ ( not @ X1 ) @ X0 )
= ( or @ X1 @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl127,zip_derived_cl91]) ).
thf(zip_derived_cl46328_069,plain,
! [X0: $i,X1: $i] :
( ( implies @ X1 @ X0 )
= ( or @ X0 @ ( not @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl46193,zip_derived_cl31343,zip_derived_cl30977]) ).
thf(zip_derived_cl176_070,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ X1 )
= ( and @ ( implies @ X0 @ X1 ) @ ( implies @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl59,zip_derived_cl62]) ).
thf(zip_derived_cl46673,plain,
! [X0: $i,X1: $i] :
( ( equiv @ ( not @ X1 ) @ ( not @ X0 ) )
= ( equiv @ X0 @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl46601,zip_derived_cl133,zip_derived_cl46328,zip_derived_cl176]) ).
thf(zip_derived_cl176_071,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ X1 )
= ( and @ ( implies @ X0 @ X1 ) @ ( implies @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl59,zip_derived_cl62]) ).
thf(zip_derived_cl4520_072,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ ( and @ X0 @ X1 ) @ ( and @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4500,zip_derived_cl203]) ).
thf(zip_derived_cl4659,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ ( and @ ( implies @ X0 @ X1 ) @ ( implies @ X1 @ X0 ) ) @ ( equiv @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl176,zip_derived_cl4520]) ).
thf(zip_derived_cl176_073,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ X1 )
= ( and @ ( implies @ X0 @ X1 ) @ ( implies @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl59,zip_derived_cl62]) ).
thf(zip_derived_cl4678,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ ( equiv @ X0 @ X1 ) @ ( equiv @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4659,zip_derived_cl176]) ).
thf(zip_derived_cl19452_074,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ ( equiv @ X1 @ X0 ) )
| ~ ( is_a_theorem @ ( implies @ X0 @ X1 ) )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl176,zip_derived_cl18858]) ).
thf(zip_derived_cl30780,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( implies @ ( equiv @ X1 @ X0 ) @ ( equiv @ X0 @ X1 ) ) )
| ( is_a_theorem @ ( equiv @ ( equiv @ X1 @ X0 ) @ ( equiv @ X0 @ X1 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl4678,zip_derived_cl19452]) ).
thf(zip_derived_cl4678_075,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ ( equiv @ X0 @ X1 ) @ ( equiv @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4659,zip_derived_cl176]) ).
thf(zip_derived_cl30840,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( equiv @ ( equiv @ X1 @ X0 ) @ ( equiv @ X0 @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl30780,zip_derived_cl4678]) ).
thf(zip_derived_cl78_076,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( equiv @ X0 @ X1 ) )
| ( X0 = X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl4,zip_derived_cl69]) ).
thf(zip_derived_cl45491,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ X1 )
= ( equiv @ X1 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl30840,zip_derived_cl78]) ).
thf(zip_derived_cl48655,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X1 @ X0 )
= ( equiv @ ( not @ X1 ) @ ( not @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl46673,zip_derived_cl45491]) ).
thf(zip_derived_cl49142,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X1 @ ( not @ X0 ) )
= ( equiv @ ( not @ X1 ) @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl30977,zip_derived_cl48655]) ).
thf(zip_derived_cl142_077,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( not @ ( implies @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56,zip_derived_cl88,zip_derived_cl61]) ).
thf(zip_derived_cl46328_078,plain,
! [X0: $i,X1: $i] :
( ( implies @ X1 @ X0 )
= ( or @ X0 @ ( not @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl46193,zip_derived_cl31343,zip_derived_cl30977]) ).
thf(zip_derived_cl7586_079,plain,
! [X0: $i] : ( is_a_theorem @ ( not @ ( not @ ( implies @ X0 @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl7505,zip_derived_cl385]) ).
thf(zip_derived_cl203_080,plain,
! [X0: $i,X1: $i] :
( ( and @ ( not @ ( not @ X1 ) ) @ X0 )
= ( and @ X1 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl198,zip_derived_cl142]) ).
thf(zip_derived_cl18521_081,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ X1 )
| ( is_a_theorem @ ( implies @ X0 @ ( and @ X1 @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl18500,zip_derived_cl142]) ).
thf(zip_derived_cl18901,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ ( implies @ X0 @ ( and @ X1 @ X0 ) ) )
| ~ ( is_a_theorem @ ( not @ ( not @ X1 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl203,zip_derived_cl18521]) ).
thf(zip_derived_cl21241,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ X1 @ ( and @ ( implies @ X0 @ X0 ) @ X1 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl7586,zip_derived_cl18901]) ).
thf(zip_derived_cl19452_082,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ ( equiv @ X1 @ X0 ) )
| ~ ( is_a_theorem @ ( implies @ X0 @ X1 ) )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl176,zip_derived_cl18858]) ).
thf(zip_derived_cl30756,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( implies @ ( and @ ( implies @ X1 @ X1 ) @ X0 ) @ X0 ) )
| ( is_a_theorem @ ( equiv @ ( and @ ( implies @ X1 @ X1 ) @ X0 ) @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl21241,zip_derived_cl19452]) ).
thf(zip_derived_cl133_083,plain,
! [X0: $i,X1: $i] :
( ( implies @ ( not @ X1 ) @ X0 )
= ( or @ X1 @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl127,zip_derived_cl91]) ).
thf(zip_derived_cl89_084,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ X0 @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl88,zip_derived_cl85]) ).
thf(zip_derived_cl163,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( or @ X0 @ ( implies @ X1 @ ( not @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl133,zip_derived_cl89]) ).
thf(zip_derived_cl124_085,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( or @ X0 @ X1 ) )
| ( is_a_theorem @ ( or @ X1 @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl123,zip_derived_cl74]) ).
thf(zip_derived_cl210,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( or @ ( implies @ X1 @ ( not @ X0 ) ) @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl163,zip_derived_cl124]) ).
thf(zip_derived_cl133_086,plain,
! [X0: $i,X1: $i] :
( ( implies @ ( not @ X1 ) @ X0 )
= ( or @ X1 @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl127,zip_derived_cl91]) ).
thf(zip_derived_cl211_087,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) )
| ( is_a_theorem @ ( or @ X0 @ ( not @ X1 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl88,zip_derived_cl124]) ).
thf(zip_derived_cl318,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( or @ X1 @ X0 ) )
| ( is_a_theorem @ ( or @ X0 @ ( not @ ( not @ X1 ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl133,zip_derived_cl211]) ).
thf(zip_derived_cl666,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( or @ X0 @ ( not @ ( not @ ( implies @ X1 @ ( not @ X0 ) ) ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl210,zip_derived_cl318]) ).
thf(zip_derived_cl142_088,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( not @ ( implies @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56,zip_derived_cl88,zip_derived_cl61]) ).
thf(zip_derived_cl673,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( or @ X0 @ ( not @ ( and @ X1 @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl666,zip_derived_cl142]) ).
thf(zip_derived_cl124_089,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( or @ X0 @ X1 ) )
| ( is_a_theorem @ ( or @ X1 @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl123,zip_derived_cl74]) ).
thf(zip_derived_cl702,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( or @ ( not @ ( and @ X1 @ X0 ) ) @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl673,zip_derived_cl124]) ).
thf(zip_derived_cl88_090,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl713,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ ( and @ X1 @ X0 ) @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl702,zip_derived_cl88]) ).
thf(zip_derived_cl30831,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( equiv @ ( and @ ( implies @ X1 @ X1 ) @ X0 ) @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl30756,zip_derived_cl713]) ).
thf(zip_derived_cl319_091,plain,
! [X0: $i] : ( is_a_theorem @ ( implies @ X0 @ ( and @ X0 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl314,zip_derived_cl142,zip_derived_cl88]) ).
thf(zip_derived_cl19452_092,plain,
! [X0: $i,X1: $i] :
( ( is_a_theorem @ ( equiv @ X1 @ X0 ) )
| ~ ( is_a_theorem @ ( implies @ X0 @ X1 ) )
| ~ ( is_a_theorem @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl176,zip_derived_cl18858]) ).
thf(zip_derived_cl30751,plain,
! [X0: $i] :
( ~ ( is_a_theorem @ ( implies @ ( and @ X0 @ X0 ) @ X0 ) )
| ( is_a_theorem @ ( equiv @ ( and @ X0 @ X0 ) @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl319,zip_derived_cl19452]) ).
thf(zip_derived_cl713_093,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ ( and @ X1 @ X0 ) @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl702,zip_derived_cl88]) ).
thf(zip_derived_cl30827,plain,
! [X0: $i] : ( is_a_theorem @ ( equiv @ ( and @ X0 @ X0 ) @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl30751,zip_derived_cl713]) ).
thf(zip_derived_cl78_094,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( equiv @ X0 @ X1 ) )
| ( X0 = X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl4,zip_derived_cl69]) ).
thf(zip_derived_cl31682,plain,
! [X0: $i] :
( ( and @ X0 @ X0 )
= X0 ),
inference('sup-',[status(thm)],[zip_derived_cl30827,zip_derived_cl78]) ).
thf(zip_derived_cl176_095,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ X1 )
= ( and @ ( implies @ X0 @ X1 ) @ ( implies @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl59,zip_derived_cl62]) ).
thf(zip_derived_cl31879,plain,
! [X0: $i] :
( ( equiv @ X0 @ X0 )
= ( implies @ X0 @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl31682,zip_derived_cl176]) ).
thf(zip_derived_cl44001,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( equiv @ ( and @ ( equiv @ X1 @ X1 ) @ X0 ) @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl30831,zip_derived_cl31879]) ).
thf(zip_derived_cl78_096,plain,
! [X0: $i,X1: $i] :
( ~ ( is_a_theorem @ ( equiv @ X0 @ X1 ) )
| ( X0 = X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl4,zip_derived_cl69]) ).
thf(zip_derived_cl44005,plain,
! [X0: $i,X1: $i] :
( ( and @ ( equiv @ X1 @ X1 ) @ X0 )
= X0 ),
inference('sup-',[status(thm)],[zip_derived_cl44001,zip_derived_cl78]) ).
thf(zip_derived_cl62698,plain,
! [X1: $i,X2: $i] :
( ( equiv @ X1 @ ( and @ X2 @ X1 ) )
= ( implies @ X1 @ ( and @ X2 @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl62609,zip_derived_cl49142,zip_derived_cl142,zip_derived_cl46328,zip_derived_cl44005]) ).
thf(zip_derived_cl91341,plain,
~ ( is_a_theorem @ ( implies @ sk__17 @ ( equiv @ sk__18 @ ( and @ sk__17 @ sk__18 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl111,zip_derived_cl62698]) ).
thf(zip_derived_cl31682_097,plain,
! [X0: $i] :
( ( and @ X0 @ X0 )
= X0 ),
inference('sup-',[status(thm)],[zip_derived_cl30827,zip_derived_cl78]) ).
thf(zip_derived_cl142_098,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( not @ ( implies @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56,zip_derived_cl88,zip_derived_cl61]) ).
thf(zip_derived_cl91_099,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( not @ ( and @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl57,zip_derived_cl71]) ).
thf(zip_derived_cl146,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( implies @ X2 @ ( implies @ X1 @ ( not @ X0 ) ) )
= ( not @ ( and @ X2 @ ( and @ X1 @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl142,zip_derived_cl91]) ).
thf(zip_derived_cl31742,plain,
! [X0: $i,X1: $i] :
( ( implies @ X1 @ ( implies @ X0 @ ( not @ X0 ) ) )
= ( not @ ( and @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl31682,zip_derived_cl146]) ).
thf(zip_derived_cl31682_100,plain,
! [X0: $i] :
( ( and @ X0 @ X0 )
= X0 ),
inference('sup-',[status(thm)],[zip_derived_cl30827,zip_derived_cl78]) ).
thf(zip_derived_cl127_101,plain,
! [X0: $i,X1: $i] :
( ( or @ X0 @ X1 )
= ( not @ ( and @ ( not @ X0 ) @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl55,zip_derived_cl70]) ).
thf(zip_derived_cl31918,plain,
! [X0: $i] :
( ( or @ X0 @ X0 )
= ( not @ ( not @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl31682,zip_derived_cl127]) ).
thf(zip_derived_cl30977_102,plain,
! [X0: $i] :
( ( not @ ( not @ X0 ) )
= X0 ),
inference('sup-',[status(thm)],[zip_derived_cl30825,zip_derived_cl78]) ).
thf(zip_derived_cl32028,plain,
! [X0: $i] :
( ( or @ X0 @ X0 )
= X0 ),
inference(demod,[status(thm)],[zip_derived_cl31918,zip_derived_cl30977]) ).
thf(zip_derived_cl88_103,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl32298,plain,
! [X0: $i] :
( ( implies @ X0 @ ( not @ X0 ) )
= ( not @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl32028,zip_derived_cl88]) ).
thf(zip_derived_cl45803_104,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( and @ X1 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl30844,zip_derived_cl78]) ).
thf(zip_derived_cl30977_105,plain,
! [X0: $i] :
( ( not @ ( not @ X0 ) )
= X0 ),
inference('sup-',[status(thm)],[zip_derived_cl30825,zip_derived_cl78]) ).
thf(zip_derived_cl91_106,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( not @ ( and @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl57,zip_derived_cl71]) ).
thf(zip_derived_cl31334,plain,
! [X0: $i,X1: $i] :
( ( implies @ X1 @ ( not @ X0 ) )
= ( not @ ( and @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl30977,zip_derived_cl91]) ).
thf(zip_derived_cl46143,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ ( not @ X1 ) )
= ( not @ ( and @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl45803,zip_derived_cl31334]) ).
thf(zip_derived_cl50818,plain,
! [X0: $i,X1: $i] :
( ( implies @ X1 @ ( not @ X0 ) )
= ( implies @ X0 @ ( not @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl31742,zip_derived_cl32298,zip_derived_cl46143]) ).
thf(zip_derived_cl88_107,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl8163_108,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( or @ X1 @ ( implies @ ( or @ X1 @ X0 ) @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl226,zip_derived_cl8000]) ).
thf(zip_derived_cl14144,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ X1 @ ( implies @ ( or @ ( not @ X1 ) @ X0 ) @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl88,zip_derived_cl8163]) ).
thf(zip_derived_cl88_109,plain,
! [X0: $i,X1: $i] :
( ( implies @ X0 @ X1 )
= ( or @ ( not @ X0 ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl58,zip_derived_cl60]) ).
thf(zip_derived_cl14164,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ X1 @ ( implies @ ( implies @ X1 @ X0 ) @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl14144,zip_derived_cl88]) ).
thf(zip_derived_cl50841,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ X0 @ ( implies @ ( implies @ X1 @ ( not @ X0 ) ) @ ( not @ X1 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl50818,zip_derived_cl14164]) ).
thf(zip_derived_cl143_110,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( implies @ ( implies @ X1 @ ( not @ X0 ) ) @ X2 )
= ( or @ ( and @ X1 @ X0 ) @ X2 ) ),
inference('sup+',[status(thm)],[zip_derived_cl142,zip_derived_cl88]) ).
thf(zip_derived_cl46328_111,plain,
! [X0: $i,X1: $i] :
( ( implies @ X1 @ X0 )
= ( or @ X0 @ ( not @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl46193,zip_derived_cl31343,zip_derived_cl30977]) ).
thf(zip_derived_cl51072,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ X0 @ ( implies @ X1 @ ( and @ X1 @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl50841,zip_derived_cl143,zip_derived_cl46328]) ).
thf(zip_derived_cl50818_112,plain,
! [X0: $i,X1: $i] :
( ( implies @ X1 @ ( not @ X0 ) )
= ( implies @ X0 @ ( not @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl31742,zip_derived_cl32298,zip_derived_cl46143]) ).
thf(zip_derived_cl40770_113,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( equiv @ X2 @ X2 )
= ( implies @ X0 @ ( implies @ X1 @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl32402,zip_derived_cl89]) ).
thf(zip_derived_cl45803_114,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( and @ X1 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl30844,zip_derived_cl78]) ).
thf(zip_derived_cl44005_115,plain,
! [X0: $i,X1: $i] :
( ( and @ ( equiv @ X1 @ X1 ) @ X0 )
= X0 ),
inference('sup-',[status(thm)],[zip_derived_cl44001,zip_derived_cl78]) ).
thf(zip_derived_cl46168,plain,
! [X0: $i,X1: $i] :
( ( and @ X1 @ ( equiv @ X0 @ X0 ) )
= X1 ),
inference('sup+',[status(thm)],[zip_derived_cl45803,zip_derived_cl44005]) ).
thf(zip_derived_cl51958,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( and @ X2 @ ( implies @ X0 @ ( implies @ X1 @ X0 ) ) )
= X2 ),
inference('sup+',[status(thm)],[zip_derived_cl40770,zip_derived_cl46168]) ).
thf(zip_derived_cl176_116,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ X1 )
= ( and @ ( implies @ X0 @ X1 ) @ ( implies @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl59,zip_derived_cl62]) ).
thf(zip_derived_cl59735,plain,
! [X0: $i,X1: $i] :
( ( equiv @ ( implies @ X1 @ X0 ) @ X0 )
= ( implies @ ( implies @ X1 @ X0 ) @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl51958,zip_derived_cl176]) ).
thf(zip_derived_cl45491_117,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ X1 )
= ( equiv @ X1 @ X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl30840,zip_derived_cl78]) ).
thf(zip_derived_cl59811,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X0 @ ( implies @ X1 @ X0 ) )
= ( implies @ ( implies @ X1 @ X0 ) @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl59735,zip_derived_cl45491]) ).
thf(zip_derived_cl68261,plain,
! [X0: $i,X1: $i] :
( ( equiv @ ( not @ X1 ) @ ( implies @ X0 @ ( not @ X1 ) ) )
= ( implies @ ( implies @ X1 @ ( not @ X0 ) ) @ ( not @ X1 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl50818,zip_derived_cl59811]) ).
thf(zip_derived_cl49142_118,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X1 @ ( not @ X0 ) )
= ( equiv @ ( not @ X1 ) @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl30977,zip_derived_cl48655]) ).
thf(zip_derived_cl142_119,plain,
! [X0: $i,X1: $i] :
( ( and @ X0 @ X1 )
= ( not @ ( implies @ X0 @ ( not @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56,zip_derived_cl88,zip_derived_cl61]) ).
thf(zip_derived_cl143_120,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( implies @ ( implies @ X1 @ ( not @ X0 ) ) @ X2 )
= ( or @ ( and @ X1 @ X0 ) @ X2 ) ),
inference('sup+',[status(thm)],[zip_derived_cl142,zip_derived_cl88]) ).
thf(zip_derived_cl46328_121,plain,
! [X0: $i,X1: $i] :
( ( implies @ X1 @ X0 )
= ( or @ X0 @ ( not @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl46193,zip_derived_cl31343,zip_derived_cl30977]) ).
thf(zip_derived_cl68287,plain,
! [X0: $i,X1: $i] :
( ( equiv @ X1 @ ( and @ X0 @ X1 ) )
= ( implies @ X1 @ ( and @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl68261,zip_derived_cl49142,zip_derived_cl142,zip_derived_cl143,zip_derived_cl46328]) ).
thf(zip_derived_cl143498,plain,
! [X0: $i,X1: $i] : ( is_a_theorem @ ( implies @ X0 @ ( equiv @ X1 @ ( and @ X0 @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl51072,zip_derived_cl68287]) ).
thf(zip_derived_cl143499,plain,
$false,
inference(demod,[status(thm)],[zip_derived_cl91341,zip_derived_cl143498]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL489+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.05 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.caIxLZeWRu true
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 4 22:58:26 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Running portfolio for 300 s
% 0.09/0.36 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Number of cores: 8
% 0.09/0.37 % Python version: Python 3.12.3
% 0.09/0.37 % Running in FO mode
% 0.46/0.65 % Total configuration time : 435
% 0.46/0.65 % Estimated wc time : 1092
% 0.46/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.46/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.46/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.46/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.48/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.48/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.48/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.48/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.48/0.83 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 235.84/39.94 % Solved by fo/fo5.sh.
% 235.84/39.94 % done 17450 iterations in 39.060s
% 235.84/39.94 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 235.84/39.94 % SZS output start Refutation
% See solution above
% 235.84/39.95
% 235.84/39.95
% 235.84/39.95 % Terminating...
% 235.84/39.99 % Runner terminated.
% 235.84/40.02 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------