%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : ITP011^1 : TPTP v9.2.0. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.YxafYnMZMy true
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 04:38:17 PM UTC 2025
% Result : Theorem 92.07s 12.24s
% Output : Refutation 92.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : ITP011^1 : TPTP v9.2.0. Bugfixed v7.5.0.
% 0.03/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.YxafYnMZMy true
% 0.13/0.36 % Computer : n007.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Wed Oct 1 15:25:38 EDT 2025
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Running portfolio for 300 s
% 0.13/0.36 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.36 % Number of cores: 8
% 0.21/0.36 % Python version: Python 3.6.8
% 0.21/0.36 % Running in HO mode
% 0.55/0.67 % Total configuration time : 828
% 0.55/0.67 % Estimated wc time : 1656
% 0.55/0.67 % Estimated cpu time (8 cpus) : 207.0
% 0.55/0.72 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.55/0.72 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.55/0.72 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.55/0.74 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 0.55/0.76 % /export/starexec/sandbox/solver/bin/lams/40_noforms.sh running for 90s
% 0.55/0.76 % /export/starexec/sandbox/solver/bin/lams/30_sp5.sh running for 60s
% 0.55/0.76 % /export/starexec/sandbox/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.57/0.76 % /export/starexec/sandbox/solver/bin/lams/40_b.comb.sh running for 70s
% 0.57/0.95 % /export/starexec/sandbox/solver/bin/lams/30_b.l.sh running for 90s
% 92.07/12.24 % Solved by lams/40_c_ic.sh.
% 92.07/12.24 % done 1220 iterations in 11.469s
% 92.07/12.24 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 92.07/12.24 % SZS output start Refutation
% 92.07/12.24 thf(du_type, type, du: $tType).
% 92.07/12.24 thf(d_type, type, d: $tType).
% 92.07/12.24 thf(u_type, type, u: $tType).
% 92.07/12.24 thf(sk__2_type, type, sk__2: u > u > u > d > d > u).
% 92.07/12.24 thf(c_2Eoption_2EIS__NONE_2E1_type, type, c_2Eoption_2EIS__NONE_2E1: du > u).
% 92.07/12.24 thf(tyop_2Emin_2Efun_type, type, tyop_2Emin_2Efun: d > d > d).
% 92.07/12.24 thf(j_mono_2Etyop_2Emin_2Ebool_type, type, j_mono_2Etyop_2Emin_2Ebool:
% 92.07/12.24 du > $o).
% 92.07/12.24 thf(mono_2Ec_2Ebool_2EF_type, type, mono_2Ec_2Ebool_2EF: $o).
% 92.07/12.24 thf(sk__4_type, type, sk__4: u).
% 92.07/12.24 thf(c_2Eoption_2EOPTREL_2E3_type, type, c_2Eoption_2EOPTREL_2E3: du > du > du > u).
% 92.07/12.24 thf(sk__5_type, type, sk__5: u).
% 92.07/12.24 thf(combin_i_2E0_type, type, combin_i_2E0: u).
% 92.07/12.24 thf(c_2Eoption_2Eoption__CASE_2E3_type, type, c_2Eoption_2Eoption__CASE_2E3:
% 92.07/12.24 du > du > du > u).
% 92.07/12.24 thf(c_2Eoption_2ESOME_2E0_type, type, c_2Eoption_2ESOME_2E0: u).
% 92.07/12.24 thf(sk__6_type, type, sk__6: u).
% 92.07/12.24 thf(s_type, type, s: d > u > du).
% 92.07/12.24 thf(app_2E2_type, type, app_2E2: du > du > u).
% 92.07/12.24 thf(zip_tseitin_0_type, type, zip_tseitin_0: u > u > u > u > u > d > d > $o).
% 92.07/12.24 thf(c_2Eoption_2EOPTION__MAP_2E2_type, type, c_2Eoption_2EOPTION__MAP_2E2:
% 92.07/12.24 du > du > u).
% 92.07/12.24 thf(c_2Eoption_2EOPTION__JOIN_2E1_type, type, c_2Eoption_2EOPTION__JOIN_2E1:
% 92.07/12.24 du > u).
% 92.07/12.24 thf(tyop_2Eoption_2Eoption_type, type, tyop_2Eoption_2Eoption: d > d).
% 92.07/12.24 thf(sk__1_type, type, sk__1: u > u > u > d > d > u).
% 92.07/12.24 thf(sk__3_type, type, sk__3: d).
% 92.07/12.24 thf(tyop_2Emin_2Ebool_type, type, tyop_2Emin_2Ebool: d).
% 92.07/12.24 thf(mono_2Ec_2Ebool_2ET_type, type, mono_2Ec_2Ebool_2ET: $o).
% 92.07/12.24 thf(c_2Eoption_2ENONE_2E0_type, type, c_2Eoption_2ENONE_2E0: u).
% 92.07/12.24 thf(c_2Eoption_2ETHE_2E1_type, type, c_2Eoption_2ETHE_2E1: du > u).
% 92.07/12.24 thf(c_2Eoption_2ESOME_2E1_type, type, c_2Eoption_2ESOME_2E1: du > u).
% 92.07/12.24 thf(c_2Eoption_2EIS__SOME_2E1_type, type, c_2Eoption_2EIS__SOME_2E1: du > u).
% 92.07/12.24 thf(zip_tseitin_1_type, type, zip_tseitin_1: u > u > d > d > $o).
% 92.07/12.24 thf(thm_2Eoption_2EOPTREL__def, axiom,
% 92.07/12.24 (![A_27a:d,A_27b:d,V0R_2E0:u,V1x_2E0:u,V2y_2E0:u]:
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V0R_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V1x_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27b ) @ V2y_2E0 ) ) ) ) <=>
% 92.07/12.24 ( ( ?[V3x0_2E0:u,V4y0_2E0:u]:
% 92.07/12.24 ( ( ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V1x_2E0 ) =
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V3x0_2E0 ) ) ) ) &
% 92.07/12.24 ( ( s @ ( tyop_2Eoption_2Eoption @ A_27b ) @ V2y_2E0 ) =
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27b ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27b @ V4y0_2E0 ) ) ) ) &
% 92.07/12.24 ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( app_2E2 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @
% 92.07/12.24 ( app_2E2 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @
% 92.07/12.24 ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V0R_2E0 ) @
% 92.07/12.24 ( s @ A_27a @ V3x0_2E0 ) ) ) @
% 92.07/12.24 ( s @ A_27b @ V4y0_2E0 ) ) ) ) ) ) |
% 92.07/12.24 ( ( ( s @ ( tyop_2Eoption_2Eoption @ A_27b ) @ V2y_2E0 ) =
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27b ) @ c_2Eoption_2ENONE_2E0 ) ) &
% 92.07/12.24 ( ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V1x_2E0 ) =
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) ) ) ) ))).
% 92.07/12.24 thf(zf_stmt_0, type, zip_tseitin_1 : u > u > d > d > $o).
% 92.07/12.24 thf(zf_stmt_1, axiom,
% 92.07/12.24 (![V2y_2E0:u,V1x_2E0:u,A_27b:d,A_27a:d]:
% 92.07/12.24 ( ( zip_tseitin_1 @ V2y_2E0 @ V1x_2E0 @ A_27b @ A_27a ) <=>
% 92.07/12.24 ( ( ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V1x_2E0 ) =
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) ) &
% 92.07/12.24 ( ( s @ ( tyop_2Eoption_2Eoption @ A_27b ) @ V2y_2E0 ) =
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27b ) @ c_2Eoption_2ENONE_2E0 ) ) ) ))).
% 92.07/12.24 thf(zf_stmt_2, type, zip_tseitin_0 : u > u > u > u > u > d > d > $o).
% 92.07/12.24 thf(zf_stmt_3, axiom,
% 92.07/12.24 (![V4y0_2E0:u,V3x0_2E0:u,V2y_2E0:u,V1x_2E0:u,V0R_2E0:u,A_27b:d,A_27a:d]:
% 92.07/12.24 ( ( zip_tseitin_0 @
% 92.07/12.24 V4y0_2E0 @ V3x0_2E0 @ V2y_2E0 @ V1x_2E0 @ V0R_2E0 @ A_27b @ A_27a ) <=>
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( app_2E2 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @
% 92.07/12.24 ( app_2E2 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V0R_2E0 ) @
% 92.07/12.24 ( s @ A_27a @ V3x0_2E0 ) ) ) @
% 92.07/12.24 ( s @ A_27b @ V4y0_2E0 ) ) ) ) &
% 92.07/12.24 ( ( s @ ( tyop_2Eoption_2Eoption @ A_27b ) @ V2y_2E0 ) =
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27b ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27b @ V4y0_2E0 ) ) ) ) &
% 92.07/12.24 ( ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V1x_2E0 ) =
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V3x0_2E0 ) ) ) ) ) ))).
% 92.07/12.24 thf(zf_stmt_4, axiom,
% 92.07/12.24 (![A_27a:d,A_27b:d,V0R_2E0:u,V1x_2E0:u,V2y_2E0:u]:
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V0R_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V1x_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27b ) @ V2y_2E0 ) ) ) ) <=>
% 92.07/12.24 ( ( zip_tseitin_1 @ V2y_2E0 @ V1x_2E0 @ A_27b @ A_27a ) |
% 92.07/12.24 ( ?[V3x0_2E0:u,V4y0_2E0:u]:
% 92.07/12.24 ( zip_tseitin_0 @
% 92.07/12.24 V4y0_2E0 @ V3x0_2E0 @ V2y_2E0 @ V1x_2E0 @ V0R_2E0 @ A_27b @ A_27a ) ) ) ))).
% 92.07/12.24 thf(zip_derived_cl90, plain,
% 92.07/12.24 (![X0 : d, X1 : d, X2 : u, X3 : u, X4 : u, X5 : u, X6 : u]:
% 92.07/12.24 ( (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ X0 @
% 92.07/12.24 (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 X2) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ X0) @ X3) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ X1) @ X4))))
% 92.07/12.24 | ~ (zip_tseitin_0 @ X5 @ X6 @ X4 @ X3 @ X2 @ X1 @ X0))),
% 92.07/12.24 inference('cnf', [status(esa)], [zf_stmt_4])).
% 92.07/12.24 thf(thm_2Equotient__option_2EOPTION__REL__def, conjecture,
% 92.07/12.24 (![A_27a:d,V0y_2E0:u,V1x_2E0:u,V2R_2E0:u]:
% 92.07/12.24 ( ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V2R_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V1x_2E0 ) ) ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V0y_2E0 ) ) ) ) ) ) <=>
% 92.07/12.24 ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( app_2E2 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @
% 92.07/12.24 ( app_2E2 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V2R_2E0 ) @
% 92.07/12.24 ( s @ A_27a @ V1x_2E0 ) ) ) @
% 92.07/12.24 ( s @ A_27a @ V0y_2E0 ) ) ) ) ) &
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V2R_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V0y_2E0 ) ) ) ) ) ) <=>
% 92.07/12.24 ( mono_2Ec_2Ebool_2EF ) ) &
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V2R_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V1x_2E0 ) ) ) @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) ) ) ) <=>
% 92.07/12.24 ( mono_2Ec_2Ebool_2EF ) ) &
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V2R_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) ) ) ) <=>
% 92.07/12.24 ( mono_2Ec_2Ebool_2ET ) ) ))).
% 92.07/12.24 thf(zf_stmt_5, negated_conjecture,
% 92.07/12.24 (~( ![A_27a:d,V0y_2E0:u,V1x_2E0:u,V2R_2E0:u]:
% 92.07/12.24 ( ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V2R_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V1x_2E0 ) ) ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V0y_2E0 ) ) ) ) ) ) <=>
% 92.07/12.24 ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( app_2E2 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @
% 92.07/12.24 ( app_2E2 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @
% 92.07/12.24 ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V2R_2E0 ) @
% 92.07/12.24 ( s @ A_27a @ V1x_2E0 ) ) ) @
% 92.07/12.24 ( s @ A_27a @ V0y_2E0 ) ) ) ) ) &
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V2R_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V0y_2E0 ) ) ) ) ) ) <=>
% 92.07/12.24 ( mono_2Ec_2Ebool_2EF ) ) &
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V2R_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V1x_2E0 ) ) ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) ) ) ) <=>
% 92.07/12.24 ( mono_2Ec_2Ebool_2EF ) ) &
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) ) @
% 92.07/12.24 V2R_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) ) ) ) <=>
% 92.07/12.24 ( mono_2Ec_2Ebool_2ET ) ) ) )),
% 92.07/12.24 inference('cnf.neg', [status(esa)],
% 92.07/12.24 [thm_2Equotient__option_2EOPTION__REL__def])).
% 92.07/12.24 thf(zip_derived_cl93, plain,
% 92.07/12.24 ((~ (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 sk__6) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ sk__3 @ sk__5))) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ sk__3 @ sk__4))))))
% 92.07/12.24 | ~ (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (app_2E2 @
% 92.07/12.24 (s @ (tyop_2Emin_2Efun @ sk__3 @ tyop_2Emin_2Ebool) @
% 92.07/12.24 (app_2E2 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 sk__6) @
% 92.07/12.24 (s @ sk__3 @ sk__5))) @
% 92.07/12.24 (s @ sk__3 @ sk__4))))
% 92.07/12.24 | (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 sk__6) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @ c_2Eoption_2ENONE_2E0) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ sk__3 @ sk__4))))))
% 92.07/12.24 | (mono_2Ec_2Ebool_2EF)
% 92.07/12.24 | (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 sk__6) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ sk__3 @ sk__5))) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @ c_2Eoption_2ENONE_2E0))))
% 92.07/12.24 | (mono_2Ec_2Ebool_2EF)
% 92.07/12.24 | ~ (mono_2Ec_2Ebool_2ET)
% 92.07/12.24 | ~ (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 sk__6) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @ c_2Eoption_2ENONE_2E0) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @ c_2Eoption_2ENONE_2E0)))))),
% 92.07/12.24 inference('cnf', [status(esa)], [zf_stmt_5])).
% 92.07/12.24 thf(zip_derived_cl81, plain,
% 92.07/12.24 (![X0 : d, X1 : d, X2 : u, X3 : u, X4 : u, X5 : u, X6 : u]:
% 92.07/12.24 ( (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (app_2E2 @
% 92.07/12.24 (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @
% 92.07/12.24 (app_2E2 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ X1 @
% 92.07/12.24 (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 X2) @
% 92.07/12.24 (s @ X1 @ X3))) @
% 92.07/12.24 (s @ X0 @ X4))))
% 92.07/12.24 | ~ (zip_tseitin_0 @ X4 @ X3 @ X5 @ X6 @ X2 @ X0 @ X1))),
% 92.07/12.24 inference('cnf', [status(esa)], [zf_stmt_3])).
% 92.07/12.24 thf(zip_derived_cl86, plain,
% 92.07/12.24 (![X0 : d, X1 : u, X2 : u, X3 : d]:
% 92.07/12.24 (((s @ (tyop_2Eoption_2Eoption @ X0) @ X1)
% 92.07/12.24 = (s @ (tyop_2Eoption_2Eoption @ X0) @ c_2Eoption_2ENONE_2E0))
% 92.07/12.24 | ~ (zip_tseitin_1 @ X1 @ X2 @ X0 @ X3))),
% 92.07/12.24 inference('cnf', [status(esa)], [zf_stmt_1])).
% 92.07/12.24 thf(reserved_2Eho_2Ei__thm, axiom,
% 92.07/12.24 (![A_27a:d,V0x_2E0:u]:
% 92.07/12.24 ( ( s @
% 92.07/12.24 A_27a @
% 92.07/12.24 ( app_2E2 @
% 92.07/12.24 ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27a ) @ combin_i_2E0 ) @
% 92.07/12.24 ( s @ A_27a @ V0x_2E0 ) ) ) =
% 92.07/12.24 ( s @ A_27a @ V0x_2E0 ) ))).
% 92.07/12.24 thf(zip_derived_cl1, plain,
% 92.07/12.24 (![X0 : d, X1 : u]:
% 92.07/12.24 ((s @ X0 @
% 92.07/12.24 (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ X0) @ combin_i_2E0) @
% 92.07/12.24 (s @ X0 @ X1)))
% 92.07/12.24 = (s @ X0 @ X1))),
% 92.07/12.24 inference('cnf', [status(esa)], [reserved_2Eho_2Ei__thm])).
% 92.07/12.24 thf(zip_derived_cl85, plain,
% 92.07/12.24 (![X0 : d, X1 : u, X2 : u, X3 : d]:
% 92.07/12.24 (((s @ (tyop_2Eoption_2Eoption @ X0) @ X1)
% 92.07/12.24 = (s @ (tyop_2Eoption_2Eoption @ X0) @ c_2Eoption_2ENONE_2E0))
% 92.07/12.24 | ~ (zip_tseitin_1 @ X2 @ X1 @ X3 @ X0))),
% 92.07/12.24 inference('cnf', [status(esa)], [zf_stmt_1])).
% 92.07/12.24 thf(thm_2Eoption_2Eoption__CLAUSES, axiom,
% 92.07/12.24 (![A_27a:d,A_27b:d,V0f_2E0:u,V1e_2E0:u,V2e_2E0:u]:
% 92.07/12.24 ( ( ![V25x_2E0:u]:
% 92.07/12.24 ( ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2EOPTION__JOIN_2E1 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ ( tyop_2Eoption_2Eoption @ A_27a ) ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V25x_2E0 ) ) ) ) ) =
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V25x_2E0 ) ) ) &
% 92.07/12.24 ( ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2EOPTION__JOIN_2E1 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ ( tyop_2Eoption_2Eoption @ A_27a ) ) @
% 92.07/12.24 c_2Eoption_2ENONE_2E0 ) ) ) =
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) ) &
% 92.07/12.24 ( ![V24f_2E0:u]:
% 92.07/12.24 ( ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27b ) @
% 92.07/12.24 ( c_2Eoption_2EOPTION__MAP_2E2 @
% 92.07/12.24 ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V24f_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) ) ) =
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27b ) @ c_2Eoption_2ENONE_2E0 ) ) ) &
% 92.07/12.24 ( ![V22f_2E0:u,V23x_2E0:u]:
% 92.07/12.24 ( ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27b ) @
% 92.07/12.24 ( c_2Eoption_2EOPTION__MAP_2E2 @
% 92.07/12.24 ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V22f_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V23x_2E0 ) ) ) ) ) =
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27b ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @
% 92.07/12.24 ( s @
% 92.07/12.24 A_27b @
% 92.07/12.24 ( app_2E2 @
% 92.07/12.24 ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V22f_2E0 ) @
% 92.07/12.24 ( s @ A_27a @ V23x_2E0 ) ) ) ) ) ) ) &
% 92.07/12.24 ( ![V19x_2E0:u,V20v_2E0:u,V21f_2E0:u]:
% 92.07/12.24 ( ( s @
% 92.07/12.24 A_27b @
% 92.07/12.24 ( c_2Eoption_2Eoption__CASE_2E3 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V19x_2E0 ) ) ) @
% 92.07/12.24 ( s @ A_27b @ V20v_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V21f_2E0 ) ) ) =
% 92.07/12.24 ( s @
% 92.07/12.24 A_27b @
% 92.07/12.24 ( app_2E2 @
% 92.07/12.24 ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V21f_2E0 ) @
% 92.07/12.24 ( s @ A_27a @ V19x_2E0 ) ) ) ) ) &
% 92.07/12.24 ( ![V17v_2E0:u,V18f_2E0:u]:
% 92.07/12.24 ( ( s @
% 92.07/12.24 A_27b @
% 92.07/12.24 ( c_2Eoption_2Eoption__CASE_2E3 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) @
% 92.07/12.24 ( s @ A_27b @ V17v_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V18f_2E0 ) ) ) =
% 92.07/12.24 ( s @ A_27b @ V17v_2E0 ) ) ) &
% 92.07/12.24 ( ![V16x_2E0:u]:
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EIS__SOME_2E1 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V16x_2E0 ) ) ) ) =>
% 92.07/12.24 ( ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2Eoption__CASE_2E3 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V16x_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V1e_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Eoption_2Eoption @ A_27a ) ) @
% 92.07/12.24 c_2Eoption_2ESOME_2E0 ) ) ) =
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V16x_2E0 ) ) ) ) &
% 92.07/12.24 ( ![V15x_2E0:u]:
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EIS__SOME_2E1 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V15x_2E0 ) ) ) ) =>
% 92.07/12.24 ( ( s @
% 92.07/12.24 A_27b @
% 92.07/12.24 ( c_2Eoption_2Eoption__CASE_2E3 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V15x_2E0 ) @
% 92.07/12.24 ( s @ A_27b @ V2e_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V0f_2E0 ) ) ) =
% 92.07/12.24 ( s @
% 92.07/12.24 A_27b @
% 92.07/12.24 ( app_2E2 @
% 92.07/12.24 ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V0f_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 A_27a @
% 92.07/12.24 ( c_2Eoption_2ETHE_2E1 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V15x_2E0 ) ) ) ) ) ) ) ) &
% 92.07/12.24 ( ![V14x_2E0:u]:
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EIS__NONE_2E1 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V14x_2E0 ) ) ) ) =>
% 92.07/12.24 ( ( s @
% 92.07/12.24 A_27b @
% 92.07/12.24 ( c_2Eoption_2Eoption__CASE_2E3 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V14x_2E0 ) @
% 92.07/12.24 ( s @ A_27b @ V2e_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V0f_2E0 ) ) ) =
% 92.07/12.24 ( s @ A_27b @ V2e_2E0 ) ) ) ) &
% 92.07/12.24 ( ![V13x_2E0:u]:
% 92.07/12.24 ( ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2Eoption__CASE_2E3 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V13x_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V13x_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Eoption_2Eoption @ A_27a ) ) @
% 92.07/12.24 c_2Eoption_2ESOME_2E0 ) ) ) =
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V13x_2E0 ) ) ) &
% 92.07/12.24 ( ![V12x_2E0:u]:
% 92.07/12.24 ( ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2Eoption__CASE_2E3 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V12x_2E0 ) @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Emin_2Efun @
% 92.07/12.24 A_27a @ ( tyop_2Eoption_2Eoption @ A_27a ) ) @
% 92.07/12.24 c_2Eoption_2ESOME_2E0 ) ) ) =
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V12x_2E0 ) ) ) &
% 92.07/12.24 ( ![V11x_2E0:u]:
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EIS__SOME_2E1 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V11x_2E0 ) ) ) ) =>
% 92.07/12.24 ( ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @
% 92.07/12.24 ( s @
% 92.07/12.24 A_27a @
% 92.07/12.24 ( c_2Eoption_2ETHE_2E1 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V11x_2E0 ) ) ) ) ) =
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V11x_2E0 ) ) ) ) &
% 92.07/12.24 ( ![V10x_2E0:u]:
% 92.07/12.24 ( ( ~( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EIS__SOME_2E1 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V10x_2E0 ) ) ) ) ) <=>
% 92.07/12.24 ( ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V10x_2E0 ) =
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) ) ) ) &
% 92.07/12.24 ( ![V9x_2E0:u]:
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EIS__NONE_2E1 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V9x_2E0 ) ) ) ) <=>
% 92.07/12.24 ( ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ V9x_2E0 ) =
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) ) ) ) &
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EIS__SOME_2E1 @
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) ) ) ) <=>
% 92.07/12.24 ( mono_2Ec_2Ebool_2EF ) ) &
% 92.07/12.24 ( ![V8x_2E0:u]:
% 92.07/12.24 ( ( j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 ( s @
% 92.07/12.24 tyop_2Emin_2Ebool @
% 92.07/12.24 ( c_2Eoption_2EIS__SOME_2E1 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V8x_2E0 ) ) ) ) ) ) <=>
% 92.07/12.24 ( mono_2Ec_2Ebool_2ET ) ) ) &
% 92.07/12.24 ( ![V7x_2E0:u]:
% 92.07/12.24 ( ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V7x_2E0 ) ) ) !=
% 92.07/12.24 ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) ) ) &
% 92.07/12.24 ( ![V6x_2E0:u]:
% 92.07/12.24 ( ( s @ ( tyop_2Eoption_2Eoption @ A_27a ) @ c_2Eoption_2ENONE_2E0 ) !=
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V6x_2E0 ) ) ) ) ) &
% 92.07/12.24 ( ![V5x_2E0:u]:
% 92.07/12.24 ( ( s @
% 92.07/12.24 A_27a @
% 92.07/12.24 ( c_2Eoption_2ETHE_2E1 @
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V5x_2E0 ) ) ) ) ) =
% 92.07/12.24 ( s @ A_27a @ V5x_2E0 ) ) ) &
% 92.07/12.24 ( ![V3x_2E0:u,V4y_2E0:u]:
% 92.07/12.24 ( ( ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V3x_2E0 ) ) ) =
% 92.07/12.24 ( s @
% 92.07/12.24 ( tyop_2Eoption_2Eoption @ A_27a ) @
% 92.07/12.24 ( c_2Eoption_2ESOME_2E1 @ ( s @ A_27a @ V4y_2E0 ) ) ) ) <=>
% 92.07/12.24 ( ( s @ A_27a @ V3x_2E0 ) = ( s @ A_27a @ V4y_2E0 ) ) ) ) ))).
% 92.07/12.24 thf(zip_derived_cl77, plain,
% 92.07/12.24 (![X0 : d, X1 : d, X2 : u, X3 : u]:
% 92.07/12.24 ((s @ (tyop_2Eoption_2Eoption @ X0) @
% 92.07/12.24 (c_2Eoption_2EOPTION__MAP_2E2 @
% 92.07/12.24 (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X2) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ X1) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ X1 @ X3)))))
% 92.07/12.24 = (s @ (tyop_2Eoption_2Eoption @ X0) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @
% 92.07/12.24 (s @ X0 @
% 92.07/12.24 (app_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X2) @
% 92.07/12.24 (s @ X1 @ X3))))))),
% 92.07/12.24 inference('cnf', [status(esa)], [thm_2Eoption_2Eoption__CLAUSES])).
% 92.07/12.24 thf(zip_derived_cl61, plain,
% 92.07/12.24 (![X0 : d, X1 : u]:
% 92.07/12.24 ((s @ (tyop_2Eoption_2Eoption @ X0) @ c_2Eoption_2ENONE_2E0)
% 92.07/12.24 != (s @ (tyop_2Eoption_2Eoption @ X0) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ X0 @ X1))))),
% 92.07/12.24 inference('cnf', [status(esa)], [thm_2Eoption_2Eoption__CLAUSES])).
% 92.07/12.24 thf(zip_derived_cl60, plain,
% 92.07/12.24 (![X0 : d, X1 : u]:
% 92.07/12.24 ((s @ X0 @
% 92.07/12.24 (c_2Eoption_2ETHE_2E1 @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ X0) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ X0 @ X1)))))
% 92.07/12.24 = (s @ X0 @ X1))),
% 92.07/12.24 inference('cnf', [status(esa)], [thm_2Eoption_2Eoption__CLAUSES])).
% 92.07/12.24 thf(zip_derived_cl84, plain,
% 92.07/12.24 (![X0 : u, X1 : u, X2 : u, X3 : u, X4 : u, X5 : d, X6 : d]:
% 92.07/12.24 ( (zip_tseitin_0 @ X0 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6)
% 92.07/12.24 | ((s @ (tyop_2Eoption_2Eoption @ X6) @ X3)
% 92.07/12.24 != (s @ (tyop_2Eoption_2Eoption @ X6) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ X6 @ X1))))
% 92.07/12.24 | ((s @ (tyop_2Eoption_2Eoption @ X5) @ X2)
% 92.07/12.24 != (s @ (tyop_2Eoption_2Eoption @ X5) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ X5 @ X0))))
% 92.07/12.24 | ~ (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (app_2E2 @
% 92.07/12.24 (s @ (tyop_2Emin_2Efun @ X5 @ tyop_2Emin_2Ebool) @
% 92.07/12.24 (app_2E2 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ X6 @
% 92.07/12.24 (tyop_2Emin_2Efun @ X5 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 X4) @
% 92.07/12.24 (s @ X6 @ X1))) @
% 92.07/12.24 (s @ X5 @ X0)))))),
% 92.07/12.24 inference('cnf', [status(esa)], [zf_stmt_3])).
% 92.07/12.24 thf(zip_derived_cl82, plain,
% 92.07/12.24 (![X0 : d, X1 : u, X2 : u, X3 : u, X4 : u, X5 : u, X6 : d]:
% 92.07/12.24 (((s @ (tyop_2Eoption_2Eoption @ X0) @ X2)
% 92.07/12.24 = (s @ (tyop_2Eoption_2Eoption @ X0) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ X0 @ X1))))
% 92.07/12.24 | ~ (zip_tseitin_0 @ X1 @ X3 @ X2 @ X4 @ X5 @ X0 @ X6))),
% 92.07/12.24 inference('cnf', [status(esa)], [zf_stmt_3])).
% 92.07/12.24 thf(zip_derived_cl78, plain,
% 92.07/12.24 (![X0 : d, X1 : d, X2 : u]:
% 92.07/12.24 ((s @ (tyop_2Eoption_2Eoption @ X0) @
% 92.07/12.24 (c_2Eoption_2EOPTION__MAP_2E2 @
% 92.07/12.24 (s @ (tyop_2Emin_2Efun @ X1 @ X0) @ X2) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ X1) @ c_2Eoption_2ENONE_2E0)))
% 92.07/12.24 = (s @ (tyop_2Eoption_2Eoption @ X0) @ c_2Eoption_2ENONE_2E0))),
% 92.07/12.24 inference('cnf', [status(esa)], [thm_2Eoption_2Eoption__CLAUSES])).
% 92.07/12.24 thf(thm_2Ebool_2EEQ__CLAUSES, axiom,
% 92.07/12.24 (![V0t:$o]:
% 92.07/12.24 ( ( ( ( V0t ) <=> ( mono_2Ec_2Ebool_2EF ) ) <=> ( ~( V0t ) ) ) &
% 92.07/12.24 ( ( ( mono_2Ec_2Ebool_2EF ) <=> ( V0t ) ) <=> ( ~( V0t ) ) ) &
% 92.07/12.24 ( ( ( V0t ) <=> ( mono_2Ec_2Ebool_2ET ) ) <=> ( V0t ) ) &
% 92.07/12.24 ( ( ( mono_2Ec_2Ebool_2ET ) <=> ( V0t ) ) <=> ( V0t ) ) ))).
% 92.07/12.24 thf(zip_derived_cl47, plain,
% 92.07/12.24 (![X0 : $o]: ( (X0) | (mono_2Ec_2Ebool_2ET) | (X0))),
% 92.07/12.24 inference('cnf', [status(esa)], [thm_2Ebool_2EEQ__CLAUSES])).
% 92.07/12.24 thf(zip_derived_cl88, plain,
% 92.07/12.24 (![X0 : u, X1 : u, X2 : u, X3 : d, X4 : d]:
% 92.07/12.24 ( (zip_tseitin_0 @ (sk__2 @ X0 @ X1 @ X2 @ X3 @ X4) @
% 92.07/12.24 (sk__1 @ X0 @ X1 @ X2 @ X3 @ X4) @ X0 @ X1 @ X2 @ X3 @ X4)
% 92.07/12.24 | (zip_tseitin_1 @ X0 @ X1 @ X3 @ X4)
% 92.07/12.24 | ~ (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ X4 @
% 92.07/12.24 (tyop_2Emin_2Efun @ X3 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 X2) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ X4) @ X1) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ X3) @ X0)))))),
% 92.07/12.24 inference('cnf', [status(esa)], [zf_stmt_4])).
% 92.07/12.24 thf(zip_derived_cl83, plain,
% 92.07/12.24 (![X0 : d, X1 : u, X2 : u, X3 : u, X4 : u, X5 : u, X6 : d]:
% 92.07/12.24 (((s @ (tyop_2Eoption_2Eoption @ X0) @ X2)
% 92.07/12.24 = (s @ (tyop_2Eoption_2Eoption @ X0) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ X0 @ X1))))
% 92.07/12.24 | ~ (zip_tseitin_0 @ X3 @ X1 @ X4 @ X2 @ X5 @ X6 @ X0))),
% 92.07/12.24 inference('cnf', [status(esa)], [zf_stmt_3])).
% 92.07/12.24 thf(zip_derived_cl87, plain,
% 92.07/12.24 (![X0 : u, X1 : u, X2 : d, X3 : d]:
% 92.07/12.24 ( (zip_tseitin_1 @ X0 @ X1 @ X2 @ X3)
% 92.07/12.24 | ((s @ (tyop_2Eoption_2Eoption @ X2) @ X0)
% 92.07/12.24 != (s @ (tyop_2Eoption_2Eoption @ X2) @ c_2Eoption_2ENONE_2E0))
% 92.07/12.24 | ((s @ (tyop_2Eoption_2Eoption @ X3) @ X1)
% 92.07/12.24 != (s @ (tyop_2Eoption_2Eoption @ X3) @ c_2Eoption_2ENONE_2E0)))),
% 92.07/12.24 inference('cnf', [status(esa)], [zf_stmt_1])).
% 92.07/12.24 thf(zip_derived_cl54, plain,
% 92.07/12.24 (![X0 : $o]: (~ (X0) | ~ (mono_2Ec_2Ebool_2EF) | ~ (X0))),
% 92.07/12.24 inference('cnf', [status(esa)], [thm_2Ebool_2EEQ__CLAUSES])).
% 92.07/12.24 thf(zip_derived_cl101, plain,
% 92.07/12.24 (( (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 sk__6) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ sk__3 @ sk__5))) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ sk__3 @ sk__4))))))
% 92.07/12.24 | (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (app_2E2 @
% 92.07/12.24 (s @ (tyop_2Emin_2Efun @ sk__3 @ tyop_2Emin_2Ebool) @
% 92.07/12.24 (app_2E2 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 sk__6) @
% 92.07/12.24 (s @ sk__3 @ sk__5))) @
% 92.07/12.24 (s @ sk__3 @ sk__4))))
% 92.07/12.24 | (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 sk__6) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @ c_2Eoption_2ENONE_2E0) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ sk__3 @ sk__4))))))
% 92.07/12.24 | (mono_2Ec_2Ebool_2EF)
% 92.07/12.24 | (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 sk__6) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @
% 92.07/12.24 (c_2Eoption_2ESOME_2E1 @ (s @ sk__3 @ sk__5))) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @ c_2Eoption_2ENONE_2E0))))
% 92.07/12.24 | (mono_2Ec_2Ebool_2EF)
% 92.07/12.24 | ~ (mono_2Ec_2Ebool_2ET)
% 92.07/12.24 | ~ (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @
% 92.07/12.24 (tyop_2Emin_2Efun @ sk__3 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 sk__6) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @ c_2Eoption_2ENONE_2E0) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ sk__3) @ c_2Eoption_2ENONE_2E0)))))),
% 92.07/12.24 inference('cnf', [status(esa)], [zf_stmt_5])).
% 92.07/12.24 thf(zip_derived_cl79, plain,
% 92.07/12.24 (![X0 : d]:
% 92.07/12.24 ((s @ (tyop_2Eoption_2Eoption @ X0) @
% 92.07/12.24 (c_2Eoption_2EOPTION__JOIN_2E1 @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ (tyop_2Eoption_2Eoption @ X0)) @
% 92.07/12.24 c_2Eoption_2ENONE_2E0)))
% 92.07/12.24 = (s @ (tyop_2Eoption_2Eoption @ X0) @ c_2Eoption_2ENONE_2E0))),
% 92.07/12.24 inference('cnf', [status(esa)], [thm_2Eoption_2Eoption__CLAUSES])).
% 92.07/12.24 thf(zip_derived_cl89, plain,
% 92.07/12.24 (![X0 : d, X1 : d, X2 : u, X3 : u, X4 : u]:
% 92.07/12.24 ( (j_mono_2Etyop_2Emin_2Ebool @
% 92.07/12.24 (s @ tyop_2Emin_2Ebool @
% 92.07/12.24 (c_2Eoption_2EOPTREL_2E3 @
% 92.07/12.24 (s @
% 92.07/12.24 (tyop_2Emin_2Efun @ X0 @
% 92.07/12.24 (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool)) @
% 92.07/12.24 X2) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ X0) @ X3) @
% 92.07/12.24 (s @ (tyop_2Eoption_2Eoption @ X1) @ X4))))
% 92.07/12.24 | ~ (zip_tseitin_1 @ X4 @ X3 @ X1 @ X0))),
% 92.07/12.24 inference('cnf', [status(esa)], [zf_stmt_4])).
% 92.07/12.24 thf(zip_derived_cl14836, plain, ($false),
% 92.07/12.24 inference('eprover', [status(thm)],
% 92.07/12.24 [zip_derived_cl90, zip_derived_cl93, zip_derived_cl81,
% 92.07/12.24 zip_derived_cl86, zip_derived_cl1, zip_derived_cl85,
% 92.07/12.24 zip_derived_cl77, zip_derived_cl61, zip_derived_cl60,
% 92.07/12.24 zip_derived_cl84, zip_derived_cl82, zip_derived_cl78,
% 92.07/12.24 zip_derived_cl47, zip_derived_cl88, zip_derived_cl83,
% 92.07/12.24 zip_derived_cl87, zip_derived_cl54, zip_derived_cl101,
% 92.07/12.24 zip_derived_cl79, zip_derived_cl89])).
% 92.07/12.24
% 92.07/12.24 % SZS output end Refutation
% 92.07/12.24
% 92.07/12.24
% 92.07/12.24 % Terminating...
% 92.20/12.36 % Runner terminated.
% 92.20/12.37 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------