%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : GRP620+1 : TPTP v9.2.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.tLdGFXsznd true
% Computer : n011.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:36:48 PM UTC 2025
% Result : Theorem 5.08s 1.39s
% Output : Refutation 5.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP620+1 : TPTP v9.2.0. Released v3.4.0.
% 0.11/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.tLdGFXsznd true
% 0.12/0.34 % Computer : n011.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 1 14:13:08 EDT 2025
% 0.19/0.34 % CPUTime :
% 0.19/0.34 % Running portfolio for 300 s
% 0.19/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.34 % Number of cores: 8
% 0.19/0.34 % Python version: Python 3.6.8
% 0.19/0.35 % Running in FO mode
% 0.54/0.66 % Total configuration time : 435
% 0.54/0.66 % Estimated wc time : 1092
% 0.54/0.66 % Estimated cpu time (7 cpus) : 156.0
% 0.56/0.74 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.56/0.76 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.56/0.78 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.56/0.79 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.56/0.79 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.56/0.80 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.56/0.82 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.57/0.90 % /export/starexec/sandbox/solver/bin/fo/fo1_lcnf.sh running for 50s
% 5.08/1.39 % Solved by fo/fo3_bce.sh.
% 5.08/1.39 % BCE start: 133
% 5.08/1.39 % BCE eliminated: 1
% 5.08/1.39 % PE start: 132
% 5.08/1.39 logic: eq
% 5.08/1.39 % PE eliminated: -17
% 5.08/1.39 % done 614 iterations in 0.608s
% 5.08/1.39 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 5.08/1.39 % SZS output start Refutation
% 5.08/1.39 thf(v4_group_1_type, type, v4_group_1: $i > $o).
% 5.08/1.39 thf(v3_struct_0_type, type, v3_struct_0: $i > $o).
% 5.08/1.39 thf(v1_fraenkel_type, type, v1_fraenkel: $i > $o).
% 5.08/1.39 thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
% 5.08/1.39 thf(l1_struct_0_type, type, l1_struct_0: $i > $o).
% 5.08/1.39 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $o).
% 5.08/1.39 thf(m1_subset_1_type, type, m1_subset_1: $i > $i > $o).
% 5.08/1.39 thf(m2_relset_1_type, type, m2_relset_1: $i > $i > $i > $o).
% 5.08/1.39 thf(v3_group_6_type, type, v3_group_6: $i > $i > $i > $o).
% 5.08/1.39 thf(v1_group_6_type, type, v1_group_6: $i > $i > $i > $o).
% 5.08/1.39 thf(v2_funct_1_type, type, v2_funct_1: $i > $o).
% 5.08/1.39 thf(l1_group_1_type, type, l1_group_1: $i > $o).
% 5.08/1.39 thf(m2_fraenkel_type, type, m2_fraenkel: $i > $i > $i > $i > $o).
% 5.08/1.39 thf(k2_funct_1_type, type, k2_funct_1: $i > $i).
% 5.08/1.39 thf(v1_funct_2_type, type, v1_funct_2: $i > $i > $i > $o).
% 5.08/1.40 thf(v1_group_1_type, type, v1_group_1: $i > $o).
% 5.08/1.40 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > $i > $o).
% 5.08/1.40 thf(sk__22_type, type, sk__22: $i).
% 5.08/1.40 thf(m1_fraenkel_type, type, m1_fraenkel: $i > $i > $i > $o).
% 5.08/1.40 thf(k1_autgroup_type, type, k1_autgroup: $i > $i).
% 5.08/1.40 thf(v2_group_6_type, type, v2_group_6: $i > $i > $i > $o).
% 5.08/1.40 thf(r2_hidden_type, type, r2_hidden: $i > $i > $o).
% 5.08/1.40 thf(v4_group_6_type, type, v4_group_6: $i > $i > $i > $o).
% 5.08/1.40 thf(v1_funct_1_type, type, v1_funct_1: $i > $o).
% 5.08/1.40 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $i > $o).
% 5.08/1.40 thf(v3_group_1_type, type, v3_group_1: $i > $o).
% 5.08/1.40 thf(sk__23_type, type, sk__23: $i).
% 5.08/1.40 thf(u1_struct_0_type, type, u1_struct_0: $i > $i).
% 5.08/1.40 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $o).
% 5.08/1.40 thf(dt_k1_autgroup, axiom,
% 5.08/1.40 (![A:$i]:
% 5.08/1.40 ( ( ( ~( v3_struct_0 @ A ) ) & ( v1_group_1 @ A ) & ( v3_group_1 @ A ) &
% 5.08/1.40 ( v4_group_1 @ A ) & ( l1_group_1 @ A ) ) =>
% 5.08/1.40 ( m1_fraenkel @
% 5.08/1.40 ( k1_autgroup @ A ) @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) ))).
% 5.08/1.40 thf(zip_derived_cl45, plain,
% 5.08/1.40 (![X0 : $i]:
% 5.08/1.40 ( (m1_fraenkel @ (k1_autgroup @ X0) @ (u1_struct_0 @ X0) @
% 5.08/1.40 (u1_struct_0 @ X0))
% 5.08/1.40 | ~ (l1_group_1 @ X0)
% 5.08/1.40 | ~ (v4_group_1 @ X0)
% 5.08/1.40 | ~ (v3_group_1 @ X0)
% 5.08/1.40 | ~ (v1_group_1 @ X0)
% 5.08/1.40 | (v3_struct_0 @ X0))),
% 5.08/1.40 inference('cnf', [status(esa)], [dt_k1_autgroup])).
% 5.08/1.40 thf(dt_m1_fraenkel, axiom,
% 5.08/1.40 (![A:$i,B:$i,C:$i]:
% 5.08/1.40 ( ( m1_fraenkel @ C @ A @ B ) =>
% 5.08/1.40 ( ( ~( v1_xboole_0 @ C ) ) & ( v1_fraenkel @ C ) ) ))).
% 5.08/1.40 thf(zip_derived_cl49, plain,
% 5.08/1.40 (![X0 : $i, X1 : $i, X2 : $i]:
% 5.08/1.40 (~ (v1_xboole_0 @ X0) | ~ (m1_fraenkel @ X0 @ X1 @ X2))),
% 5.08/1.40 inference('cnf', [status(esa)], [dt_m1_fraenkel])).
% 5.08/1.40 thf(zip_derived_cl1483, plain,
% 5.08/1.40 (![X0 : $i]:
% 5.08/1.40 ( (v3_struct_0 @ X0)
% 5.08/1.40 | ~ (v1_group_1 @ X0)
% 5.08/1.40 | ~ (v3_group_1 @ X0)
% 5.08/1.40 | ~ (v4_group_1 @ X0)
% 5.08/1.40 | ~ (l1_group_1 @ X0)
% 5.08/1.40 | ~ (v1_xboole_0 @ (k1_autgroup @ X0)))),
% 5.08/1.40 inference('dp-resolution', [status(thm)],
% 5.08/1.40 [zip_derived_cl45, zip_derived_cl49])).
% 5.08/1.40 thf(t7_autgroup, conjecture,
% 5.08/1.40 (![A:$i]:
% 5.08/1.40 ( ( ( ~( v3_struct_0 @ A ) ) & ( v1_group_1 @ A ) & ( v3_group_1 @ A ) &
% 5.08/1.40 ( v4_group_1 @ A ) & ( l1_group_1 @ A ) ) =>
% 5.08/1.40 ( ![B:$i]:
% 5.08/1.40 ( ( m2_fraenkel @
% 5.08/1.40 B @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) @
% 5.08/1.40 ( k1_autgroup @ A ) ) =>
% 5.08/1.40 ( m2_fraenkel @
% 5.08/1.40 ( k2_funct_1 @ B ) @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) @
% 5.08/1.40 ( k1_autgroup @ A ) ) ) ) ))).
% 5.08/1.40 thf(zf_stmt_0, negated_conjecture,
% 5.08/1.40 (~( ![A:$i]:
% 5.08/1.40 ( ( ( ~( v3_struct_0 @ A ) ) & ( v1_group_1 @ A ) &
% 5.08/1.40 ( v3_group_1 @ A ) & ( v4_group_1 @ A ) & ( l1_group_1 @ A ) ) =>
% 5.08/1.40 ( ![B:$i]:
% 5.08/1.40 ( ( m2_fraenkel @
% 5.08/1.40 B @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) @
% 5.08/1.40 ( k1_autgroup @ A ) ) =>
% 5.08/1.40 ( m2_fraenkel @
% 5.08/1.40 ( k2_funct_1 @ B ) @ ( u1_struct_0 @ A ) @
% 5.08/1.40 ( u1_struct_0 @ A ) @ ( k1_autgroup @ A ) ) ) ) ) )),
% 5.08/1.40 inference('cnf.neg', [status(esa)], [t7_autgroup])).
% 5.08/1.40 thf(zip_derived_cl132, plain,
% 5.08/1.40 ( (m2_fraenkel @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.08/1.40 (u1_struct_0 @ sk__22) @ (k1_autgroup @ sk__22))),
% 5.08/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.08/1.40 thf(t6_autgroup, axiom,
% 5.08/1.40 (![A:$i]:
% 5.08/1.40 ( ( ( ~( v3_struct_0 @ A ) ) & ( v1_group_1 @ A ) & ( v3_group_1 @ A ) &
% 5.08/1.40 ( v4_group_1 @ A ) & ( l1_group_1 @ A ) ) =>
% 5.08/1.40 ( ![B:$i]:
% 5.08/1.40 ( ( m2_fraenkel @
% 5.08/1.40 B @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) @
% 5.08/1.40 ( k1_autgroup @ A ) ) =>
% 5.08/1.40 ( ( v1_funct_1 @ ( k2_funct_1 @ B ) ) &
% 5.08/1.40 ( v1_funct_2 @
% 5.08/1.40 ( k2_funct_1 @ B ) @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) &
% 5.08/1.40 ( v1_group_6 @ ( k2_funct_1 @ B ) @ A @ A ) &
% 5.08/1.40 ( m2_relset_1 @
% 5.08/1.40 ( k2_funct_1 @ B ) @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) ) ) ) ))).
% 5.08/1.40 thf(zip_derived_cl119, plain,
% 5.08/1.40 (![X0 : $i, X1 : $i]:
% 5.08/1.40 (~ (m2_fraenkel @ X0 @ (u1_struct_0 @ X1) @ (u1_struct_0 @ X1) @
% 5.08/1.40 (k1_autgroup @ X1))
% 5.08/1.40 | (m2_relset_1 @ (k2_funct_1 @ X0) @ (u1_struct_0 @ X1) @
% 5.08/1.40 (u1_struct_0 @ X1))
% 5.08/1.40 | ~ (l1_group_1 @ X1)
% 5.08/1.40 | ~ (v4_group_1 @ X1)
% 5.08/1.40 | ~ (v3_group_1 @ X1)
% 5.08/1.40 | ~ (v1_group_1 @ X1)
% 5.08/1.40 | (v3_struct_0 @ X1))),
% 5.08/1.40 inference('cnf', [status(esa)], [t6_autgroup])).
% 5.08/1.40 thf(zip_derived_cl2935, plain,
% 5.08/1.40 (( (v3_struct_0 @ sk__22)
% 5.08/1.40 | ~ (v1_group_1 @ sk__22)
% 5.08/1.40 | ~ (v3_group_1 @ sk__22)
% 5.08/1.40 | ~ (v4_group_1 @ sk__22)
% 5.08/1.40 | ~ (l1_group_1 @ sk__22)
% 5.08/1.40 | (m2_relset_1 @ (k2_funct_1 @ sk__23) @ (u1_struct_0 @ sk__22) @
% 5.08/1.40 (u1_struct_0 @ sk__22)))),
% 5.08/1.40 inference('sup-', [status(thm)], [zip_derived_cl132, zip_derived_cl119])).
% 5.08/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.08/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.08/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.08/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.08/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.08/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.08/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.08/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.08/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.08/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.08/1.40 thf(zip_derived_cl2936, plain,
% 5.08/1.40 ( (m2_relset_1 @ (k2_funct_1 @ sk__23) @ (u1_struct_0 @ sk__22) @
% 5.08/1.40 (u1_struct_0 @ sk__22))),
% 5.08/1.40 inference('demod', [status(thm)],
% 5.08/1.40 [zip_derived_cl2935, zip_derived_cl126, zip_derived_cl127,
% 5.08/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.08/1.40 thf(zip_derived_cl132, plain,
% 5.08/1.40 ( (m2_fraenkel @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.08/1.40 (u1_struct_0 @ sk__22) @ (k1_autgroup @ sk__22))),
% 5.08/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.08/1.40 thf(zip_derived_cl45, plain,
% 5.08/1.40 (![X0 : $i]:
% 5.08/1.40 ( (m1_fraenkel @ (k1_autgroup @ X0) @ (u1_struct_0 @ X0) @
% 5.08/1.40 (u1_struct_0 @ X0))
% 5.08/1.40 | ~ (l1_group_1 @ X0)
% 5.08/1.40 | ~ (v4_group_1 @ X0)
% 5.08/1.40 | ~ (v3_group_1 @ X0)
% 5.08/1.40 | ~ (v1_group_1 @ X0)
% 5.08/1.40 | (v3_struct_0 @ X0))),
% 5.08/1.40 inference('cnf', [status(esa)], [dt_k1_autgroup])).
% 5.08/1.40 thf(redefinition_m2_fraenkel, axiom,
% 5.08/1.40 (![A:$i,B:$i,C:$i]:
% 5.08/1.40 ( ( ( ~( v1_xboole_0 @ B ) ) & ( m1_fraenkel @ C @ A @ B ) ) =>
% 5.08/1.40 ( ![D:$i]:
% 5.08/1.40 ( ( m2_fraenkel @ D @ A @ B @ C ) <=> ( m1_subset_1 @ D @ C ) ) ) ))).
% 5.08/1.40 thf(zip_derived_cl107, plain,
% 5.08/1.40 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 5.08/1.40 ( (v1_xboole_0 @ X0)
% 5.08/1.40 | ~ (m1_fraenkel @ X1 @ X2 @ X0)
% 5.08/1.40 | (m1_subset_1 @ X3 @ X1)
% 5.08/1.40 | ~ (m2_fraenkel @ X3 @ X2 @ X0 @ X1))),
% 5.08/1.40 inference('cnf', [status(esa)], [redefinition_m2_fraenkel])).
% 5.08/1.40 thf(zip_derived_cl1488, plain,
% 5.08/1.40 (![X0 : $i, X1 : $i]:
% 5.08/1.40 ( (v3_struct_0 @ X0)
% 5.08/1.40 | ~ (v1_group_1 @ X0)
% 5.08/1.40 | ~ (v3_group_1 @ X0)
% 5.08/1.40 | ~ (v4_group_1 @ X0)
% 5.08/1.40 | ~ (l1_group_1 @ X0)
% 5.08/1.40 | ~ (m2_fraenkel @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0) @
% 5.08/1.40 (k1_autgroup @ X0))
% 5.08/1.40 | (m1_subset_1 @ X1 @ (k1_autgroup @ X0))
% 5.08/1.40 | (v1_xboole_0 @ (u1_struct_0 @ X0)))),
% 5.08/1.40 inference('dp-resolution', [status(thm)],
% 5.08/1.40 [zip_derived_cl45, zip_derived_cl107])).
% 5.08/1.40 thf(dt_l1_group_1, axiom,
% 5.08/1.40 (![A:$i]: ( ( l1_group_1 @ A ) => ( l1_struct_0 @ A ) ))).
% 5.08/1.40 thf(zip_derived_cl48, plain,
% 5.08/1.40 (![X0 : $i]: ( (l1_struct_0 @ X0) | ~ (l1_group_1 @ X0))),
% 5.08/1.40 inference('cnf', [status(esa)], [dt_l1_group_1])).
% 5.08/1.40 thf(fc1_struct_0, axiom,
% 5.08/1.40 (![A:$i]:
% 5.08/1.40 ( ( ( ~( v3_struct_0 @ A ) ) & ( l1_struct_0 @ A ) ) =>
% 5.08/1.40 ( ~( v1_xboole_0 @ ( u1_struct_0 @ A ) ) ) ))).
% 5.08/1.40 thf(zip_derived_cl67, plain,
% 5.08/1.40 (![X0 : $i]:
% 5.08/1.40 (~ (v1_xboole_0 @ (u1_struct_0 @ X0))
% 5.08/1.40 | ~ (l1_struct_0 @ X0)
% 5.08/1.40 | (v3_struct_0 @ X0))),
% 5.08/1.40 inference('cnf', [status(esa)], [fc1_struct_0])).
% 5.08/1.40 thf(zip_derived_cl1155, plain,
% 5.08/1.40 (![X0 : $i]:
% 5.08/1.40 (~ (l1_group_1 @ X0)
% 5.08/1.40 | (v3_struct_0 @ X0)
% 5.08/1.40 | ~ (v1_xboole_0 @ (u1_struct_0 @ X0)))),
% 5.08/1.40 inference('dp-resolution', [status(thm)],
% 5.08/1.40 [zip_derived_cl48, zip_derived_cl67])).
% 5.08/1.40 thf(zip_derived_cl3025, plain,
% 5.08/1.40 (![X0 : $i, X1 : $i]:
% 5.08/1.40 ( (m1_subset_1 @ X1 @ (k1_autgroup @ X0))
% 5.08/1.40 | ~ (m2_fraenkel @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0) @
% 5.08/1.40 (k1_autgroup @ X0))
% 5.08/1.40 | ~ (l1_group_1 @ X0)
% 5.08/1.40 | ~ (v4_group_1 @ X0)
% 5.08/1.40 | ~ (v3_group_1 @ X0)
% 5.08/1.40 | ~ (v1_group_1 @ X0)
% 5.08/1.40 | (v3_struct_0 @ X0))),
% 5.08/1.40 inference('clc', [status(thm)], [zip_derived_cl1488, zip_derived_cl1155])).
% 5.08/1.40 thf(zip_derived_cl3027, plain,
% 5.08/1.40 (( (v3_struct_0 @ sk__22)
% 5.08/1.40 | ~ (v1_group_1 @ sk__22)
% 5.08/1.40 | ~ (v3_group_1 @ sk__22)
% 5.08/1.40 | ~ (v4_group_1 @ sk__22)
% 5.08/1.40 | ~ (l1_group_1 @ sk__22)
% 5.08/1.40 | (m1_subset_1 @ sk__23 @ (k1_autgroup @ sk__22)))),
% 5.08/1.40 inference('sup-', [status(thm)], [zip_derived_cl132, zip_derived_cl3025])).
% 5.08/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.08/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.08/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.08/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.08/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.08/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.08/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.08/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.08/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.08/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.08/1.40 thf(zip_derived_cl3028, plain,
% 5.08/1.40 ( (m1_subset_1 @ sk__23 @ (k1_autgroup @ sk__22))),
% 5.08/1.40 inference('demod', [status(thm)],
% 5.08/1.40 [zip_derived_cl3027, zip_derived_cl126, zip_derived_cl127,
% 5.08/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.08/1.40 thf(t2_subset, axiom,
% 5.08/1.40 (![A:$i,B:$i]:
% 5.08/1.40 ( ( m1_subset_1 @ A @ B ) =>
% 5.08/1.40 ( ( v1_xboole_0 @ B ) | ( r2_hidden @ A @ B ) ) ))).
% 5.08/1.40 thf(zip_derived_cl112, plain,
% 5.08/1.40 (![X0 : $i, X1 : $i]:
% 5.08/1.40 ( (r2_hidden @ X0 @ X1)
% 5.08/1.40 | (v1_xboole_0 @ X1)
% 5.08/1.40 | ~ (m1_subset_1 @ X0 @ X1))),
% 5.08/1.40 inference('cnf', [status(esa)], [t2_subset])).
% 5.08/1.40 thf(zip_derived_cl3030, plain,
% 5.08/1.40 (( (v1_xboole_0 @ (k1_autgroup @ sk__22))
% 5.08/1.40 | (r2_hidden @ sk__23 @ (k1_autgroup @ sk__22)))),
% 5.08/1.40 inference('sup-', [status(thm)], [zip_derived_cl3028, zip_derived_cl112])).
% 5.08/1.40 thf(zip_derived_cl132, plain,
% 5.08/1.40 ( (m2_fraenkel @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.08/1.40 (u1_struct_0 @ sk__22) @ (k1_autgroup @ sk__22))),
% 5.08/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.08/1.40 thf(zip_derived_cl45, plain,
% 5.08/1.40 (![X0 : $i]:
% 5.08/1.40 ( (m1_fraenkel @ (k1_autgroup @ X0) @ (u1_struct_0 @ X0) @
% 5.08/1.40 (u1_struct_0 @ X0))
% 5.08/1.40 | ~ (l1_group_1 @ X0)
% 5.08/1.40 | ~ (v4_group_1 @ X0)
% 5.08/1.40 | ~ (v3_group_1 @ X0)
% 5.08/1.40 | ~ (v1_group_1 @ X0)
% 5.08/1.40 | (v3_struct_0 @ X0))),
% 5.08/1.40 inference('cnf', [status(esa)], [dt_k1_autgroup])).
% 5.08/1.40 thf(dt_m2_fraenkel, axiom,
% 5.08/1.40 (![A:$i,B:$i,C:$i]:
% 5.08/1.40 ( ( ( ~( v1_xboole_0 @ B ) ) & ( m1_fraenkel @ C @ A @ B ) ) =>
% 5.08/1.40 ( ![D:$i]:
% 5.08/1.40 ( ( m2_fraenkel @ D @ A @ B @ C ) =>
% 5.08/1.40 ( ( v1_funct_1 @ D ) & ( v1_funct_2 @ D @ A @ B ) &
% 5.08/1.40 ( m2_relset_1 @ D @ A @ B ) ) ) ) ))).
% 5.08/1.40 thf(zip_derived_cl53, plain,
% 5.08/1.40 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 5.08/1.40 ( (v1_xboole_0 @ X0)
% 5.08/1.40 | ~ (m1_fraenkel @ X1 @ X2 @ X0)
% 5.08/1.40 | (m2_relset_1 @ X3 @ X2 @ X0)
% 5.08/1.40 | ~ (m2_fraenkel @ X3 @ X2 @ X0 @ X1))),
% 5.08/1.40 inference('cnf', [status(esa)], [dt_m2_fraenkel])).
% 5.08/1.40 thf(zip_derived_cl1486, plain,
% 5.08/1.40 (![X0 : $i, X1 : $i]:
% 5.08/1.40 ( (v3_struct_0 @ X0)
% 5.08/1.40 | ~ (v1_group_1 @ X0)
% 5.08/1.40 | ~ (v3_group_1 @ X0)
% 5.08/1.40 | ~ (v4_group_1 @ X0)
% 5.08/1.40 | ~ (l1_group_1 @ X0)
% 5.08/1.40 | ~ (m2_fraenkel @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0) @
% 5.08/1.40 (k1_autgroup @ X0))
% 5.08/1.40 | (m2_relset_1 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.08/1.40 | (v1_xboole_0 @ (u1_struct_0 @ X0)))),
% 5.08/1.40 inference('dp-resolution', [status(thm)],
% 5.08/1.40 [zip_derived_cl45, zip_derived_cl53])).
% 5.08/1.40 thf(zip_derived_cl1155, plain,
% 5.08/1.40 (![X0 : $i]:
% 5.08/1.40 (~ (l1_group_1 @ X0)
% 5.08/1.40 | (v3_struct_0 @ X0)
% 5.08/1.40 | ~ (v1_xboole_0 @ (u1_struct_0 @ X0)))),
% 5.08/1.40 inference('dp-resolution', [status(thm)],
% 5.08/1.40 [zip_derived_cl48, zip_derived_cl67])).
% 5.08/1.40 thf(zip_derived_cl3162, plain,
% 5.08/1.40 (![X0 : $i, X1 : $i]:
% 5.08/1.40 ( (m2_relset_1 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.08/1.40 | ~ (m2_fraenkel @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0) @
% 5.08/1.40 (k1_autgroup @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0))),
% 5.54/1.40 inference('clc', [status(thm)], [zip_derived_cl1486, zip_derived_cl1155])).
% 5.54/1.40 thf(zip_derived_cl3166, plain,
% 5.54/1.40 (( (v3_struct_0 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | (m2_relset_1 @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22)))),
% 5.54/1.40 inference('sup-', [status(thm)], [zip_derived_cl132, zip_derived_cl3162])).
% 5.54/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl3168, plain,
% 5.54/1.40 ( (m2_relset_1 @ sk__23 @ (u1_struct_0 @ sk__22) @ (u1_struct_0 @ sk__22))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3166, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.54/1.40 thf(zip_derived_cl45, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 ( (m1_fraenkel @ (k1_autgroup @ X0) @ (u1_struct_0 @ X0) @
% 5.54/1.40 (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0))),
% 5.54/1.40 inference('cnf', [status(esa)], [dt_k1_autgroup])).
% 5.54/1.40 thf(d1_autgroup, axiom,
% 5.54/1.40 (![A:$i]:
% 5.54/1.40 ( ( ( l1_group_1 @ A ) & ( v4_group_1 @ A ) & ( v3_group_1 @ A ) &
% 5.54/1.40 ( v1_group_1 @ A ) & ( ~( v3_struct_0 @ A ) ) ) =>
% 5.54/1.40 ( ![B:$i]:
% 5.54/1.40 ( ( m1_fraenkel @ B @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) =>
% 5.54/1.40 ( ( ( B ) = ( k1_autgroup @ A ) ) <=>
% 5.54/1.40 ( ( ![C:$i]:
% 5.54/1.40 ( ( ( m2_relset_1 @
% 5.54/1.40 C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) &
% 5.54/1.40 ( v1_group_6 @ C @ A @ A ) &
% 5.54/1.40 ( v1_funct_2 @
% 5.54/1.40 C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) &
% 5.54/1.40 ( v1_funct_1 @ C ) ) =>
% 5.54/1.40 ( ( r2_hidden @ C @ B ) <=>
% 5.54/1.40 ( ( v3_group_6 @ C @ A @ A ) & ( v2_funct_1 @ C ) ) ) ) ) &
% 5.54/1.40 ( ![C:$i]:
% 5.54/1.40 ( ( m2_fraenkel @
% 5.54/1.40 C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) @ B ) =>
% 5.54/1.40 ( ( m2_relset_1 @
% 5.54/1.40 C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) &
% 5.54/1.40 ( v1_group_6 @ C @ A @ A ) &
% 5.54/1.40 ( v1_funct_2 @
% 5.54/1.40 C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) &
% 5.54/1.40 ( v1_funct_1 @ C ) ) ) ) ) ) ) ) ))).
% 5.54/1.40 thf(zf_stmt_1, axiom,
% 5.54/1.40 (![C:$i,A:$i]:
% 5.54/1.40 ( ( zip_tseitin_0 @ C @ A ) <=>
% 5.54/1.40 ( ( v1_funct_1 @ C ) &
% 5.54/1.40 ( v1_funct_2 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) &
% 5.54/1.40 ( v1_group_6 @ C @ A @ A ) &
% 5.54/1.40 ( m2_relset_1 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) ) ))).
% 5.54/1.40 thf(zip_derived_cl25, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 ( (zip_tseitin_0 @ X0 @ X1)
% 5.54/1.40 | ~ (m2_relset_1 @ X0 @ (u1_struct_0 @ X1) @ (u1_struct_0 @ X1))
% 5.54/1.40 | ~ (v1_group_6 @ X0 @ X1 @ X1)
% 5.54/1.40 | ~ (v1_funct_2 @ X0 @ (u1_struct_0 @ X1) @ (u1_struct_0 @ X1))
% 5.54/1.40 | ~ (v1_funct_1 @ X0))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_1])).
% 5.54/1.40 thf(zf_stmt_2, type, zip_tseitin_3 : $i > $i > $i > $o).
% 5.54/1.40 thf(zf_stmt_3, axiom,
% 5.54/1.40 (![C:$i,B:$i,A:$i]:
% 5.54/1.40 ( ( zip_tseitin_3 @ C @ B @ A ) <=>
% 5.54/1.40 ( ( m2_fraenkel @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) @ B ) =>
% 5.54/1.40 ( ( v1_funct_1 @ C ) &
% 5.54/1.40 ( v1_funct_2 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) &
% 5.54/1.40 ( v1_group_6 @ C @ A @ A ) &
% 5.54/1.40 ( m2_relset_1 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) ) ) ))).
% 5.54/1.40 thf(zf_stmt_4, type, zip_tseitin_2 : $i > $i > $i > $o).
% 5.54/1.40 thf(zf_stmt_5, axiom,
% 5.54/1.40 (![C:$i,B:$i,A:$i]:
% 5.54/1.40 ( ( zip_tseitin_2 @ C @ B @ A ) <=>
% 5.54/1.40 ( ( zip_tseitin_0 @ C @ A ) =>
% 5.54/1.40 ( ( r2_hidden @ C @ B ) <=> ( zip_tseitin_1 @ C @ A ) ) ) ))).
% 5.54/1.40 thf(zf_stmt_6, type, zip_tseitin_1 : $i > $i > $o).
% 5.54/1.40 thf(zf_stmt_7, axiom,
% 5.54/1.40 (![C:$i,A:$i]:
% 5.54/1.40 ( ( zip_tseitin_1 @ C @ A ) <=>
% 5.54/1.40 ( ( v2_funct_1 @ C ) & ( v3_group_6 @ C @ A @ A ) ) ))).
% 5.54/1.40 thf(zf_stmt_8, type, zip_tseitin_0 : $i > $i > $o).
% 5.54/1.40 thf(zf_stmt_9, axiom,
% 5.54/1.40 (![A:$i]:
% 5.54/1.40 ( ( ( ~( v3_struct_0 @ A ) ) & ( v1_group_1 @ A ) & ( v3_group_1 @ A ) &
% 5.54/1.40 ( v4_group_1 @ A ) & ( l1_group_1 @ A ) ) =>
% 5.54/1.40 ( ![B:$i]:
% 5.54/1.40 ( ( m1_fraenkel @ B @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) =>
% 5.54/1.40 ( ( ( B ) = ( k1_autgroup @ A ) ) <=>
% 5.54/1.40 ( ( ![C:$i]: ( zip_tseitin_3 @ C @ B @ A ) ) &
% 5.54/1.40 ( ![C:$i]: ( zip_tseitin_2 @ C @ B @ A ) ) ) ) ) ) ))).
% 5.54/1.40 thf(zip_derived_cl41, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i]:
% 5.54/1.40 (~ (m1_fraenkel @ X0 @ (u1_struct_0 @ X1) @ (u1_struct_0 @ X1))
% 5.54/1.40 | ((X0) != (k1_autgroup @ X1))
% 5.54/1.40 | (zip_tseitin_2 @ X2 @ X0 @ X1)
% 5.54/1.40 | ~ (l1_group_1 @ X1)
% 5.54/1.40 | ~ (v4_group_1 @ X1)
% 5.54/1.40 | ~ (v3_group_1 @ X1)
% 5.54/1.40 | ~ (v1_group_1 @ X1)
% 5.54/1.40 | (v3_struct_0 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_9])).
% 5.54/1.40 thf(zip_derived_cl29, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i]:
% 5.54/1.40 (~ (zip_tseitin_0 @ X0 @ X1)
% 5.54/1.40 | ~ (r2_hidden @ X0 @ X2)
% 5.54/1.40 | (zip_tseitin_1 @ X0 @ X1)
% 5.54/1.40 | ~ (zip_tseitin_2 @ X0 @ X2 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_5])).
% 5.54/1.40 thf(zip_derived_cl1164, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i]:
% 5.54/1.40 ( (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ((X1) != (k1_autgroup @ X0))
% 5.54/1.40 | ~ (m1_fraenkel @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | (zip_tseitin_1 @ X2 @ X0)
% 5.54/1.40 | ~ (r2_hidden @ X2 @ X1)
% 5.54/1.40 | ~ (zip_tseitin_0 @ X2 @ X0))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl41, zip_derived_cl29])).
% 5.54/1.40 thf(zip_derived_cl1173, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i]:
% 5.54/1.40 (~ (v1_funct_1 @ X1)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (r2_hidden @ X1 @ X2)
% 5.54/1.40 | (zip_tseitin_1 @ X1 @ X0)
% 5.54/1.40 | ~ (m1_fraenkel @ X2 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ((X2) != (k1_autgroup @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl25, zip_derived_cl1164])).
% 5.54/1.40 thf(zip_derived_cl1492, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 5.54/1.40 (((k1_autgroup @ X0) != (X3))
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ X2))
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ X2))
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X2)
% 5.54/1.40 | ~ (v1_group_1 @ X2)
% 5.54/1.40 | ~ (v3_group_1 @ X2)
% 5.54/1.40 | ~ (v4_group_1 @ X2)
% 5.54/1.40 | ~ (l1_group_1 @ X2)
% 5.54/1.40 | ((X3) != (k1_autgroup @ X2))
% 5.54/1.40 | (zip_tseitin_1 @ X1 @ X2)
% 5.54/1.40 | ~ (r2_hidden @ X1 @ X3)
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X2))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X2 @ X2)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X2))
% 5.54/1.40 | ~ (v1_funct_1 @ X1))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl45, zip_derived_cl1173])).
% 5.54/1.40 thf(zip_derived_cl3537, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 5.54/1.40 (~ (v1_funct_1 @ X1)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X2))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X2 @ X2)
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X2))
% 5.54/1.40 | ~ (r2_hidden @ X1 @ X3)
% 5.54/1.40 | (zip_tseitin_1 @ X1 @ X2)
% 5.54/1.40 | ((X3) != (k1_autgroup @ X2))
% 5.54/1.40 | ~ (l1_group_1 @ X2)
% 5.54/1.40 | ~ (v4_group_1 @ X2)
% 5.54/1.40 | ~ (v3_group_1 @ X2)
% 5.54/1.40 | ~ (v1_group_1 @ X2)
% 5.54/1.40 | (v3_struct_0 @ X2)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ X2))
% 5.54/1.40 | ((k1_autgroup @ X0) != (X3)))),
% 5.54/1.40 inference('simplify', [status(thm)], [zip_derived_cl1492])).
% 5.54/1.40 thf(zip_derived_cl3544, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 (((k1_autgroup @ X0) != (X1))
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ sk__22))
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | ((X1) != (k1_autgroup @ sk__22))
% 5.54/1.40 | (zip_tseitin_1 @ sk__23 @ sk__22)
% 5.54/1.40 | ~ (r2_hidden @ sk__23 @ X1)
% 5.54/1.40 | ~ (v1_group_6 @ sk__23 @ sk__22 @ sk__22)
% 5.54/1.40 | ~ (v1_funct_2 @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22))
% 5.54/1.40 | ~ (v1_funct_1 @ sk__23))),
% 5.54/1.40 inference('sup-', [status(thm)], [zip_derived_cl3168, zip_derived_cl3537])).
% 5.54/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl132, plain,
% 5.54/1.40 ( (m2_fraenkel @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22) @ (k1_autgroup @ sk__22))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl45, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 ( (m1_fraenkel @ (k1_autgroup @ X0) @ (u1_struct_0 @ X0) @
% 5.54/1.40 (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0))),
% 5.54/1.40 inference('cnf', [status(esa)], [dt_k1_autgroup])).
% 5.54/1.40 thf(zip_derived_cl52, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 5.54/1.40 ( (v1_xboole_0 @ X0)
% 5.54/1.40 | ~ (m1_fraenkel @ X1 @ X2 @ X0)
% 5.54/1.40 | (v1_funct_2 @ X3 @ X2 @ X0)
% 5.54/1.40 | ~ (m2_fraenkel @ X3 @ X2 @ X0 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [dt_m2_fraenkel])).
% 5.54/1.40 thf(zip_derived_cl1485, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 ( (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (m2_fraenkel @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0) @
% 5.54/1.40 (k1_autgroup @ X0))
% 5.54/1.40 | (v1_funct_2 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | (v1_xboole_0 @ (u1_struct_0 @ X0)))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl45, zip_derived_cl52])).
% 5.54/1.40 thf(zip_derived_cl1155, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 (~ (l1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_xboole_0 @ (u1_struct_0 @ X0)))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl48, zip_derived_cl67])).
% 5.54/1.40 thf(zip_derived_cl3116, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 ( (v1_funct_2 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (m2_fraenkel @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0) @
% 5.54/1.40 (k1_autgroup @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0))),
% 5.54/1.40 inference('clc', [status(thm)], [zip_derived_cl1485, zip_derived_cl1155])).
% 5.54/1.40 thf(zip_derived_cl3118, plain,
% 5.54/1.40 (( (v3_struct_0 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | (v1_funct_2 @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22)))),
% 5.54/1.40 inference('sup-', [status(thm)], [zip_derived_cl132, zip_derived_cl3116])).
% 5.54/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl3119, plain,
% 5.54/1.40 ( (v1_funct_2 @ sk__23 @ (u1_struct_0 @ sk__22) @ (u1_struct_0 @ sk__22))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3118, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.54/1.40 thf(zip_derived_cl132, plain,
% 5.54/1.40 ( (m2_fraenkel @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22) @ (k1_autgroup @ sk__22))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl45, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 ( (m1_fraenkel @ (k1_autgroup @ X0) @ (u1_struct_0 @ X0) @
% 5.54/1.40 (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0))),
% 5.54/1.40 inference('cnf', [status(esa)], [dt_k1_autgroup])).
% 5.54/1.40 thf(zip_derived_cl51, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 5.54/1.40 ( (v1_xboole_0 @ X0)
% 5.54/1.40 | ~ (m1_fraenkel @ X1 @ X2 @ X0)
% 5.54/1.40 | (v1_funct_1 @ X3)
% 5.54/1.40 | ~ (m2_fraenkel @ X3 @ X2 @ X0 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [dt_m2_fraenkel])).
% 5.54/1.40 thf(zip_derived_cl1484, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 ( (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (m2_fraenkel @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0) @
% 5.54/1.40 (k1_autgroup @ X0))
% 5.54/1.40 | (v1_funct_1 @ X1)
% 5.54/1.40 | (v1_xboole_0 @ (u1_struct_0 @ X0)))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl45, zip_derived_cl51])).
% 5.54/1.40 thf(zip_derived_cl1155, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 (~ (l1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_xboole_0 @ (u1_struct_0 @ X0)))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl48, zip_derived_cl67])).
% 5.54/1.40 thf(zip_derived_cl2909, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 ( (v1_funct_1 @ X1)
% 5.54/1.40 | ~ (m2_fraenkel @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0) @
% 5.54/1.40 (k1_autgroup @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0))),
% 5.54/1.40 inference('clc', [status(thm)], [zip_derived_cl1484, zip_derived_cl1155])).
% 5.54/1.40 thf(zip_derived_cl2911, plain,
% 5.54/1.40 (( (v3_struct_0 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | (v1_funct_1 @ sk__23))),
% 5.54/1.40 inference('sup-', [status(thm)], [zip_derived_cl132, zip_derived_cl2909])).
% 5.54/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl2912, plain, ( (v1_funct_1 @ sk__23)),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl2911, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.54/1.40 thf(zip_derived_cl3549, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 (((k1_autgroup @ X0) != (X1))
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ sk__22))
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ((X1) != (k1_autgroup @ sk__22))
% 5.54/1.40 | (zip_tseitin_1 @ sk__23 @ sk__22)
% 5.54/1.40 | ~ (r2_hidden @ sk__23 @ X1)
% 5.54/1.40 | ~ (v1_group_6 @ sk__23 @ sk__22 @ sk__22))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3544, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130,
% 5.54/1.40 zip_derived_cl3119, zip_derived_cl2912])).
% 5.54/1.40 thf(zip_derived_cl132, plain,
% 5.54/1.40 ( (m2_fraenkel @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22) @ (k1_autgroup @ sk__22))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl45, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 ( (m1_fraenkel @ (k1_autgroup @ X0) @ (u1_struct_0 @ X0) @
% 5.54/1.40 (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0))),
% 5.54/1.40 inference('cnf', [status(esa)], [dt_k1_autgroup])).
% 5.54/1.40 thf(zip_derived_cl40, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i]:
% 5.54/1.40 (~ (m1_fraenkel @ X0 @ (u1_struct_0 @ X1) @ (u1_struct_0 @ X1))
% 5.54/1.40 | ((X0) != (k1_autgroup @ X1))
% 5.54/1.40 | (zip_tseitin_3 @ X2 @ X0 @ X1)
% 5.54/1.40 | ~ (l1_group_1 @ X1)
% 5.54/1.40 | ~ (v4_group_1 @ X1)
% 5.54/1.40 | ~ (v3_group_1 @ X1)
% 5.54/1.40 | ~ (v1_group_1 @ X1)
% 5.54/1.40 | (v3_struct_0 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_9])).
% 5.54/1.40 thf(zip_derived_cl35, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i]:
% 5.54/1.40 (~ (m2_fraenkel @ X0 @ (u1_struct_0 @ X1) @ (u1_struct_0 @ X1) @ X2)
% 5.54/1.40 | (v1_group_6 @ X0 @ X1 @ X1)
% 5.54/1.40 | ~ (zip_tseitin_3 @ X0 @ X2 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_3])).
% 5.54/1.40 thf(zip_derived_cl1191, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i]:
% 5.54/1.40 ( (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ((X1) != (k1_autgroup @ X0))
% 5.54/1.40 | ~ (m1_fraenkel @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | (v1_group_6 @ X2 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_fraenkel @ X2 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0) @ X1))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl40, zip_derived_cl35])).
% 5.54/1.40 thf(zip_derived_cl1501, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 5.54/1.40 (((k1_autgroup @ X0) != (X2))
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ X1))
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ X1))
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (m2_fraenkel @ X3 @ (u1_struct_0 @ X1) @ (u1_struct_0 @ X1) @ X2)
% 5.54/1.40 | (v1_group_6 @ X3 @ X1 @ X1)
% 5.54/1.40 | ((X2) != (k1_autgroup @ X1))
% 5.54/1.40 | ~ (l1_group_1 @ X1)
% 5.54/1.40 | ~ (v4_group_1 @ X1)
% 5.54/1.40 | ~ (v3_group_1 @ X1)
% 5.54/1.40 | ~ (v1_group_1 @ X1)
% 5.54/1.40 | (v3_struct_0 @ X1))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl45, zip_derived_cl1191])).
% 5.54/1.40 thf(zip_derived_cl3636, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 5.54/1.40 ( (v3_struct_0 @ X1)
% 5.54/1.40 | ~ (v1_group_1 @ X1)
% 5.54/1.40 | ~ (v3_group_1 @ X1)
% 5.54/1.40 | ~ (v4_group_1 @ X1)
% 5.54/1.40 | ~ (l1_group_1 @ X1)
% 5.54/1.40 | ((X2) != (k1_autgroup @ X1))
% 5.54/1.40 | (v1_group_6 @ X3 @ X1 @ X1)
% 5.54/1.40 | ~ (m2_fraenkel @ X3 @ (u1_struct_0 @ X1) @ (u1_struct_0 @ X1) @ X2)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ X1))
% 5.54/1.40 | ((k1_autgroup @ X0) != (X2)))),
% 5.54/1.40 inference('simplify', [status(thm)], [zip_derived_cl1501])).
% 5.54/1.40 thf(zip_derived_cl3641, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 (((k1_autgroup @ X0) != (k1_autgroup @ sk__22))
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ sk__22))
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | (v1_group_6 @ sk__23 @ sk__22 @ sk__22)
% 5.54/1.40 | ((k1_autgroup @ sk__22) != (k1_autgroup @ sk__22))
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | (v3_struct_0 @ sk__22))),
% 5.54/1.40 inference('sup-', [status(thm)], [zip_derived_cl132, zip_derived_cl3636])).
% 5.54/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl3646, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 (((k1_autgroup @ X0) != (k1_autgroup @ sk__22))
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ sk__22))
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | (v1_group_6 @ sk__23 @ sk__22 @ sk__22)
% 5.54/1.40 | ((k1_autgroup @ sk__22) != (k1_autgroup @ sk__22)))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3641, zip_derived_cl130, zip_derived_cl129,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl127, zip_derived_cl126])).
% 5.54/1.40 thf(zip_derived_cl3647, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 ( (v1_group_6 @ sk__23 @ sk__22 @ sk__22)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ sk__22))
% 5.54/1.40 | ((k1_autgroup @ X0) != (k1_autgroup @ sk__22)))),
% 5.54/1.40 inference('simplify', [status(thm)], [zip_derived_cl3646])).
% 5.54/1.40 thf(zip_derived_cl3651, plain,
% 5.54/1.40 ((((u1_struct_0 @ sk__22) != (u1_struct_0 @ sk__22))
% 5.54/1.40 | (v3_struct_0 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | (v1_group_6 @ sk__23 @ sk__22 @ sk__22))),
% 5.54/1.40 inference('eq_res', [status(thm)], [zip_derived_cl3647])).
% 5.54/1.40 thf(zip_derived_cl3652, plain,
% 5.54/1.40 (( (v1_group_6 @ sk__23 @ sk__22 @ sk__22)
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | (v3_struct_0 @ sk__22))),
% 5.54/1.40 inference('simplify', [status(thm)], [zip_derived_cl3651])).
% 5.54/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl3653, plain, ( (v1_group_6 @ sk__23 @ sk__22 @ sk__22)),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3652, zip_derived_cl130, zip_derived_cl129,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl127, zip_derived_cl126])).
% 5.54/1.40 thf(zip_derived_cl3656, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 (((k1_autgroup @ X0) != (X1))
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ sk__22))
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ((X1) != (k1_autgroup @ sk__22))
% 5.54/1.40 | (zip_tseitin_1 @ sk__23 @ sk__22)
% 5.54/1.40 | ~ (r2_hidden @ sk__23 @ X1))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3549, zip_derived_cl3653])).
% 5.54/1.40 thf(zip_derived_cl3722, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 ( (v1_xboole_0 @ (k1_autgroup @ sk__22))
% 5.54/1.40 | (zip_tseitin_1 @ sk__23 @ sk__22)
% 5.54/1.40 | ((k1_autgroup @ sk__22) != (k1_autgroup @ sk__22))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ sk__22))
% 5.54/1.40 | ((k1_autgroup @ X0) != (k1_autgroup @ sk__22)))),
% 5.54/1.40 inference('sup-', [status(thm)], [zip_derived_cl3030, zip_derived_cl3656])).
% 5.54/1.40 thf(zip_derived_cl3727, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 (((k1_autgroup @ X0) != (k1_autgroup @ sk__22))
% 5.54/1.40 | ((u1_struct_0 @ X0) != (u1_struct_0 @ sk__22))
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | (zip_tseitin_1 @ sk__23 @ sk__22)
% 5.54/1.40 | (v1_xboole_0 @ (k1_autgroup @ sk__22)))),
% 5.54/1.40 inference('simplify', [status(thm)], [zip_derived_cl3722])).
% 5.54/1.40 thf(zip_derived_cl3737, plain,
% 5.54/1.40 (( (v1_xboole_0 @ (k1_autgroup @ sk__22))
% 5.54/1.40 | (zip_tseitin_1 @ sk__23 @ sk__22)
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | (v3_struct_0 @ sk__22)
% 5.54/1.40 | ((u1_struct_0 @ sk__22) != (u1_struct_0 @ sk__22)))),
% 5.54/1.40 inference('eq_res', [status(thm)], [zip_derived_cl3727])).
% 5.54/1.40 thf(zip_derived_cl3738, plain,
% 5.54/1.40 (( (v3_struct_0 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | (zip_tseitin_1 @ sk__23 @ sk__22)
% 5.54/1.40 | (v1_xboole_0 @ (k1_autgroup @ sk__22)))),
% 5.54/1.40 inference('simplify', [status(thm)], [zip_derived_cl3737])).
% 5.54/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl3739, plain,
% 5.54/1.40 (( (zip_tseitin_1 @ sk__23 @ sk__22)
% 5.54/1.40 | (v1_xboole_0 @ (k1_autgroup @ sk__22)))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3738, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.54/1.40 thf(zip_derived_cl26, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]: ( (v2_funct_1 @ X0) | ~ (zip_tseitin_1 @ X0 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_7])).
% 5.54/1.40 thf(d12_group_6, axiom,
% 5.54/1.40 (![A:$i]:
% 5.54/1.40 ( ( ( ~( v3_struct_0 @ A ) ) & ( v3_group_1 @ A ) & ( v4_group_1 @ A ) &
% 5.54/1.40 ( l1_group_1 @ A ) ) =>
% 5.54/1.40 ( ![B:$i]:
% 5.54/1.40 ( ( ( ~( v3_struct_0 @ B ) ) & ( v3_group_1 @ B ) &
% 5.54/1.40 ( v4_group_1 @ B ) & ( l1_group_1 @ B ) ) =>
% 5.54/1.40 ( ![C:$i]:
% 5.54/1.40 ( ( ( v1_funct_1 @ C ) &
% 5.54/1.40 ( v1_funct_2 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) ) &
% 5.54/1.40 ( v1_group_6 @ C @ A @ B ) &
% 5.54/1.40 ( m2_relset_1 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) ) ) =>
% 5.54/1.40 ( ( v2_group_6 @ C @ A @ B ) <=> ( v2_funct_1 @ C ) ) ) ) ) ) ))).
% 5.54/1.40 thf(zip_derived_cl16, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i]:
% 5.54/1.40 ( (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v2_funct_1 @ X1)
% 5.54/1.40 | (v2_group_6 @ X1 @ X2 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X2 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_funct_1 @ X1)
% 5.54/1.40 | ~ (l1_group_1 @ X2)
% 5.54/1.40 | ~ (v4_group_1 @ X2)
% 5.54/1.40 | ~ (v3_group_1 @ X2)
% 5.54/1.40 | (v3_struct_0 @ X2))),
% 5.54/1.40 inference('cnf', [status(esa)], [d12_group_6])).
% 5.54/1.40 thf(zip_derived_cl27, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 ( (v3_group_6 @ X0 @ X1 @ X1) | ~ (zip_tseitin_1 @ X0 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_7])).
% 5.54/1.40 thf(d14_group_6, axiom,
% 5.54/1.40 (![A:$i]:
% 5.54/1.40 ( ( ( ~( v3_struct_0 @ A ) ) & ( v3_group_1 @ A ) & ( v4_group_1 @ A ) &
% 5.54/1.40 ( l1_group_1 @ A ) ) =>
% 5.54/1.40 ( ![B:$i]:
% 5.54/1.40 ( ( ( ~( v3_struct_0 @ B ) ) & ( v3_group_1 @ B ) &
% 5.54/1.40 ( v4_group_1 @ B ) & ( l1_group_1 @ B ) ) =>
% 5.54/1.40 ( ![C:$i]:
% 5.54/1.40 ( ( ( v1_funct_1 @ C ) &
% 5.54/1.40 ( v1_funct_2 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) ) &
% 5.54/1.40 ( v1_group_6 @ C @ A @ B ) &
% 5.54/1.40 ( m2_relset_1 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) ) ) =>
% 5.54/1.40 ( ( v4_group_6 @ C @ A @ B ) <=>
% 5.54/1.40 ( ( v3_group_6 @ C @ A @ B ) & ( v2_group_6 @ C @ A @ B ) ) ) ) ) ) ) ))).
% 5.54/1.40 thf(zip_derived_cl18, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i]:
% 5.54/1.40 ( (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_6 @ X1 @ X2 @ X0)
% 5.54/1.40 | ~ (v2_group_6 @ X1 @ X2 @ X0)
% 5.54/1.40 | (v4_group_6 @ X1 @ X2 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X2 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_funct_1 @ X1)
% 5.54/1.40 | ~ (l1_group_1 @ X2)
% 5.54/1.40 | ~ (v4_group_1 @ X2)
% 5.54/1.40 | ~ (v3_group_1 @ X2)
% 5.54/1.40 | (v3_struct_0 @ X2))),
% 5.54/1.40 inference('cnf', [status(esa)], [d14_group_6])).
% 5.54/1.40 thf(zip_derived_cl1141, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 (~ (zip_tseitin_1 @ X1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v1_funct_1 @ X1)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | (v4_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (v2_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl27, zip_derived_cl18])).
% 5.54/1.40 thf(zip_derived_cl1146, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 ( (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v1_funct_1 @ X1)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v2_funct_1 @ X1)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | (v4_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_funct_1 @ X1)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (zip_tseitin_1 @ X1 @ X0))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl16, zip_derived_cl1141])).
% 5.54/1.40 thf(zip_derived_cl1180, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i]:
% 5.54/1.40 (~ (zip_tseitin_1 @ X0 @ X1)
% 5.54/1.40 | ~ (zip_tseitin_1 @ X0 @ X2)
% 5.54/1.40 | (v3_struct_0 @ X2)
% 5.54/1.40 | ~ (v3_group_1 @ X2)
% 5.54/1.40 | ~ (v4_group_1 @ X2)
% 5.54/1.40 | ~ (l1_group_1 @ X2)
% 5.54/1.40 | ~ (v1_funct_1 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ X0 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X2))
% 5.54/1.40 | ~ (v1_group_6 @ X0 @ X2 @ X2)
% 5.54/1.40 | ~ (m2_relset_1 @ X0 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X2))
% 5.54/1.40 | (v4_group_6 @ X0 @ X2 @ X2)
% 5.54/1.40 | ~ (l1_group_1 @ X2)
% 5.54/1.40 | ~ (v4_group_1 @ X2)
% 5.54/1.40 | ~ (v3_group_1 @ X2)
% 5.54/1.40 | (v3_struct_0 @ X2)
% 5.54/1.40 | (v3_struct_0 @ X2)
% 5.54/1.40 | ~ (v3_group_1 @ X2)
% 5.54/1.40 | ~ (v4_group_1 @ X2)
% 5.54/1.40 | ~ (l1_group_1 @ X2)
% 5.54/1.40 | ~ (m2_relset_1 @ X0 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X2))
% 5.54/1.40 | ~ (v1_group_6 @ X0 @ X2 @ X2)
% 5.54/1.40 | ~ (v1_funct_2 @ X0 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X2))
% 5.54/1.40 | ~ (v1_funct_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X2)
% 5.54/1.40 | ~ (v4_group_1 @ X2)
% 5.54/1.40 | ~ (v3_group_1 @ X2)
% 5.54/1.40 | (v3_struct_0 @ X2))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl26, zip_derived_cl1146])).
% 5.54/1.40 thf(zip_derived_cl3160, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i]:
% 5.54/1.40 ( (v4_group_6 @ X0 @ X2 @ X2)
% 5.54/1.40 | ~ (m2_relset_1 @ X0 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X2))
% 5.54/1.40 | ~ (v1_group_6 @ X0 @ X2 @ X2)
% 5.54/1.40 | ~ (v1_funct_2 @ X0 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X2))
% 5.54/1.40 | ~ (v1_funct_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X2)
% 5.54/1.40 | ~ (v4_group_1 @ X2)
% 5.54/1.40 | ~ (v3_group_1 @ X2)
% 5.54/1.40 | (v3_struct_0 @ X2)
% 5.54/1.40 | ~ (zip_tseitin_1 @ X0 @ X2)
% 5.54/1.40 | ~ (zip_tseitin_1 @ X0 @ X1))),
% 5.54/1.40 inference('simplify', [status(thm)], [zip_derived_cl1180])).
% 5.54/1.40 thf(zip_derived_cl3740, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 ( (v1_xboole_0 @ (k1_autgroup @ sk__22))
% 5.54/1.40 | ~ (zip_tseitin_1 @ sk__23 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v1_funct_1 @ sk__23)
% 5.54/1.40 | ~ (v1_funct_2 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ sk__23 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | (v4_group_6 @ sk__23 @ X0 @ X0))),
% 5.54/1.40 inference('sup-', [status(thm)], [zip_derived_cl3739, zip_derived_cl3160])).
% 5.54/1.40 thf(zip_derived_cl2912, plain, ( (v1_funct_1 @ sk__23)),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl2911, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.54/1.40 thf(zip_derived_cl3742, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 ( (v1_xboole_0 @ (k1_autgroup @ sk__22))
% 5.54/1.40 | ~ (zip_tseitin_1 @ sk__23 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ sk__23 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | (v4_group_6 @ sk__23 @ X0 @ X0))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3740, zip_derived_cl2912])).
% 5.54/1.40 thf(t73_group_6, axiom,
% 5.54/1.40 (![A:$i]:
% 5.54/1.40 ( ( ( ~( v3_struct_0 @ A ) ) & ( v3_group_1 @ A ) & ( v4_group_1 @ A ) &
% 5.54/1.40 ( l1_group_1 @ A ) ) =>
% 5.54/1.40 ( ![B:$i]:
% 5.54/1.40 ( ( ( ~( v3_struct_0 @ B ) ) & ( v3_group_1 @ B ) &
% 5.54/1.40 ( v4_group_1 @ B ) & ( l1_group_1 @ B ) ) =>
% 5.54/1.40 ( ![C:$i]:
% 5.54/1.40 ( ( ( v1_funct_1 @ C ) &
% 5.54/1.40 ( v1_funct_2 @ C @ ( u1_struct_0 @ B ) @ ( u1_struct_0 @ A ) ) &
% 5.54/1.40 ( v1_group_6 @ C @ B @ A ) &
% 5.54/1.40 ( m2_relset_1 @ C @ ( u1_struct_0 @ B ) @ ( u1_struct_0 @ A ) ) ) =>
% 5.54/1.40 ( ![D:$i]:
% 5.54/1.40 ( ( ( v1_funct_1 @ D ) &
% 5.54/1.40 ( v1_funct_2 @
% 5.54/1.40 D @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) ) &
% 5.54/1.40 ( v1_group_6 @ D @ A @ B ) &
% 5.54/1.40 ( m2_relset_1 @
% 5.54/1.40 D @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) ) ) =>
% 5.54/1.40 ( ( ( v4_group_6 @ C @ B @ A ) &
% 5.54/1.40 ( ( D ) = ( k2_funct_1 @ C ) ) ) =>
% 5.54/1.40 ( v4_group_6 @ D @ A @ B ) ) ) ) ) ) ) ) ))).
% 5.54/1.40 thf(zip_derived_cl123, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 5.54/1.40 ( (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v1_funct_1 @ X1)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X2 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X2) @ (u1_struct_0 @ X0))
% 5.54/1.40 | (v4_group_6 @ X1 @ X2 @ X0)
% 5.54/1.40 | ((X1) != (k2_funct_1 @ X3))
% 5.54/1.40 | ~ (v4_group_6 @ X3 @ X0 @ X2)
% 5.54/1.40 | ~ (m2_relset_1 @ X3 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X2))
% 5.54/1.40 | ~ (v1_group_6 @ X3 @ X0 @ X2)
% 5.54/1.40 | ~ (v1_funct_2 @ X3 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X2))
% 5.54/1.40 | ~ (v1_funct_1 @ X3)
% 5.54/1.40 | ~ (l1_group_1 @ X2)
% 5.54/1.40 | ~ (v4_group_1 @ X2)
% 5.54/1.40 | ~ (v3_group_1 @ X2)
% 5.54/1.40 | (v3_struct_0 @ X2))),
% 5.54/1.40 inference('cnf', [status(esa)], [t73_group_6])).
% 5.54/1.40 thf(zip_derived_cl3800, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 (~ (m2_relset_1 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ sk__23 @ X0 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (zip_tseitin_1 @ sk__23 @ X0)
% 5.54/1.40 | (v1_xboole_0 @ (k1_autgroup @ sk__22))
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v1_funct_1 @ sk__23)
% 5.54/1.40 | ~ (v1_funct_2 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ sk__23 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ((X1) != (k2_funct_1 @ sk__23))
% 5.54/1.40 | (v4_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_funct_1 @ X1)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0))),
% 5.54/1.40 inference('sup-', [status(thm)], [zip_derived_cl3742, zip_derived_cl123])).
% 5.54/1.40 thf(zip_derived_cl2912, plain, ( (v1_funct_1 @ sk__23)),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl2911, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.54/1.40 thf(zip_derived_cl3814, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 (~ (m2_relset_1 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ sk__23 @ X0 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (zip_tseitin_1 @ sk__23 @ X0)
% 5.54/1.40 | (v1_xboole_0 @ (k1_autgroup @ sk__22))
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ sk__23 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ((X1) != (k2_funct_1 @ sk__23))
% 5.54/1.40 | (v4_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_funct_1 @ X1)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3800, zip_derived_cl2912])).
% 5.54/1.40 thf(zip_derived_cl3815, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 (~ (v1_funct_1 @ X1)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | (v4_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ((X1) != (k2_funct_1 @ sk__23))
% 5.54/1.40 | (v1_xboole_0 @ (k1_autgroup @ sk__22))
% 5.54/1.40 | ~ (zip_tseitin_1 @ sk__23 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ sk__23 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0)))),
% 5.54/1.40 inference('simplify', [status(thm)], [zip_derived_cl3814])).
% 5.54/1.40 thf(t5_autgroup, axiom,
% 5.54/1.40 (![A:$i]:
% 5.54/1.40 ( ( ( ~( v3_struct_0 @ A ) ) & ( v1_group_1 @ A ) & ( v3_group_1 @ A ) &
% 5.54/1.40 ( v4_group_1 @ A ) & ( l1_group_1 @ A ) ) =>
% 5.54/1.40 ( ![B:$i]:
% 5.54/1.40 ( ( ( v1_funct_1 @ B ) &
% 5.54/1.40 ( v1_funct_2 @ B @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) &
% 5.54/1.40 ( v1_group_6 @ B @ A @ A ) &
% 5.54/1.40 ( m2_relset_1 @ B @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ A ) ) ) =>
% 5.54/1.40 ( ( r2_hidden @ B @ ( k1_autgroup @ A ) ) <=>
% 5.54/1.40 ( v4_group_6 @ B @ A @ A ) ) ) ) ))).
% 5.54/1.40 thf(zip_derived_cl116, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 (~ (v1_funct_1 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ X0 @ (u1_struct_0 @ X1) @ (u1_struct_0 @ X1))
% 5.54/1.40 | ~ (v1_group_6 @ X0 @ X1 @ X1)
% 5.54/1.40 | ~ (m2_relset_1 @ X0 @ (u1_struct_0 @ X1) @ (u1_struct_0 @ X1))
% 5.54/1.40 | ~ (v4_group_6 @ X0 @ X1 @ X1)
% 5.54/1.40 | (r2_hidden @ X0 @ (k1_autgroup @ X1))
% 5.54/1.40 | ~ (l1_group_1 @ X1)
% 5.54/1.40 | ~ (v4_group_1 @ X1)
% 5.54/1.40 | ~ (v3_group_1 @ X1)
% 5.54/1.40 | ~ (v1_group_1 @ X1)
% 5.54/1.40 | (v3_struct_0 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [t5_autgroup])).
% 5.54/1.40 thf(zip_derived_cl4039, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 (~ (m2_relset_1 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ sk__23 @ X0 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (zip_tseitin_1 @ sk__23 @ X0)
% 5.54/1.40 | (v1_xboole_0 @ (k1_autgroup @ sk__22))
% 5.54/1.40 | ((X1) != (k2_funct_1 @ sk__23))
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_funct_1 @ X1)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | (r2_hidden @ X1 @ (k1_autgroup @ X0))
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_funct_1 @ X1))),
% 5.54/1.40 inference('sup-', [status(thm)], [zip_derived_cl3815, zip_derived_cl116])).
% 5.54/1.40 thf(zip_derived_cl4057, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 ( (r2_hidden @ X1 @ (k1_autgroup @ X0))
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v1_funct_1 @ X1)
% 5.54/1.40 | ~ (v1_funct_2 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ X1 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ((X1) != (k2_funct_1 @ sk__23))
% 5.54/1.40 | (v1_xboole_0 @ (k1_autgroup @ sk__22))
% 5.54/1.40 | ~ (zip_tseitin_1 @ sk__23 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v1_funct_2 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (v1_group_6 @ sk__23 @ X0 @ X0)
% 5.54/1.40 | ~ (m2_relset_1 @ sk__23 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0)))),
% 5.54/1.40 inference('simplify', [status(thm)], [zip_derived_cl4039])).
% 5.54/1.40 thf(zip_derived_cl4364, plain,
% 5.54/1.40 ((~ (m2_relset_1 @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22))
% 5.54/1.40 | ~ (v1_group_6 @ sk__23 @ sk__22 @ sk__22)
% 5.54/1.40 | ~ (v1_funct_2 @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22))
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | (v3_struct_0 @ sk__22)
% 5.54/1.40 | ~ (zip_tseitin_1 @ sk__23 @ sk__22)
% 5.54/1.40 | (v1_xboole_0 @ (k1_autgroup @ sk__22))
% 5.54/1.40 | ((k2_funct_1 @ sk__23) != (k2_funct_1 @ sk__23))
% 5.54/1.40 | ~ (v1_group_6 @ (k2_funct_1 @ sk__23) @ sk__22 @ sk__22)
% 5.54/1.40 | ~ (v1_funct_2 @ (k2_funct_1 @ sk__23) @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22))
% 5.54/1.40 | ~ (v1_funct_1 @ (k2_funct_1 @ sk__23))
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | (r2_hidden @ (k2_funct_1 @ sk__23) @ (k1_autgroup @ sk__22)))),
% 5.54/1.40 inference('sup-', [status(thm)], [zip_derived_cl2936, zip_derived_cl4057])).
% 5.54/1.40 thf(zip_derived_cl3168, plain,
% 5.54/1.40 ( (m2_relset_1 @ sk__23 @ (u1_struct_0 @ sk__22) @ (u1_struct_0 @ sk__22))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3166, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.54/1.40 thf(zip_derived_cl3653, plain, ( (v1_group_6 @ sk__23 @ sk__22 @ sk__22)),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3652, zip_derived_cl130, zip_derived_cl129,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl127, zip_derived_cl126])).
% 5.54/1.40 thf(zip_derived_cl3119, plain,
% 5.54/1.40 ( (v1_funct_2 @ sk__23 @ (u1_struct_0 @ sk__22) @ (u1_struct_0 @ sk__22))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3118, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.54/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl132, plain,
% 5.54/1.40 ( (m2_fraenkel @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22) @ (k1_autgroup @ sk__22))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl120, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 (~ (m2_fraenkel @ X0 @ (u1_struct_0 @ X1) @ (u1_struct_0 @ X1) @
% 5.54/1.40 (k1_autgroup @ X1))
% 5.54/1.40 | (v1_group_6 @ (k2_funct_1 @ X0) @ X1 @ X1)
% 5.54/1.40 | ~ (l1_group_1 @ X1)
% 5.54/1.40 | ~ (v4_group_1 @ X1)
% 5.54/1.40 | ~ (v3_group_1 @ X1)
% 5.54/1.40 | ~ (v1_group_1 @ X1)
% 5.54/1.40 | (v3_struct_0 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [t6_autgroup])).
% 5.54/1.40 thf(zip_derived_cl2906, plain,
% 5.54/1.40 (( (v3_struct_0 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | (v1_group_6 @ (k2_funct_1 @ sk__23) @ sk__22 @ sk__22))),
% 5.54/1.40 inference('sup-', [status(thm)], [zip_derived_cl132, zip_derived_cl120])).
% 5.54/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl2907, plain,
% 5.54/1.40 ( (v1_group_6 @ (k2_funct_1 @ sk__23) @ sk__22 @ sk__22)),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl2906, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.54/1.40 thf(zip_derived_cl132, plain,
% 5.54/1.40 ( (m2_fraenkel @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22) @ (k1_autgroup @ sk__22))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl121, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 (~ (m2_fraenkel @ X0 @ (u1_struct_0 @ X1) @ (u1_struct_0 @ X1) @
% 5.54/1.40 (k1_autgroup @ X1))
% 5.54/1.40 | (v1_funct_2 @ (k2_funct_1 @ X0) @ (u1_struct_0 @ X1) @
% 5.54/1.40 (u1_struct_0 @ X1))
% 5.54/1.40 | ~ (l1_group_1 @ X1)
% 5.54/1.40 | ~ (v4_group_1 @ X1)
% 5.54/1.40 | ~ (v3_group_1 @ X1)
% 5.54/1.40 | ~ (v1_group_1 @ X1)
% 5.54/1.40 | (v3_struct_0 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [t6_autgroup])).
% 5.54/1.40 thf(zip_derived_cl3010, plain,
% 5.54/1.40 (( (v3_struct_0 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | (v1_funct_2 @ (k2_funct_1 @ sk__23) @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22)))),
% 5.54/1.40 inference('sup-', [status(thm)], [zip_derived_cl132, zip_derived_cl121])).
% 5.54/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl3011, plain,
% 5.54/1.40 ( (v1_funct_2 @ (k2_funct_1 @ sk__23) @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3010, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.54/1.40 thf(zip_derived_cl132, plain,
% 5.54/1.40 ( (m2_fraenkel @ sk__23 @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22) @ (k1_autgroup @ sk__22))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl122, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 (~ (m2_fraenkel @ X0 @ (u1_struct_0 @ X1) @ (u1_struct_0 @ X1) @
% 5.54/1.40 (k1_autgroup @ X1))
% 5.54/1.40 | (v1_funct_1 @ (k2_funct_1 @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X1)
% 5.54/1.40 | ~ (v4_group_1 @ X1)
% 5.54/1.40 | ~ (v3_group_1 @ X1)
% 5.54/1.40 | ~ (v1_group_1 @ X1)
% 5.54/1.40 | (v3_struct_0 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [t6_autgroup])).
% 5.54/1.40 thf(zip_derived_cl2898, plain,
% 5.54/1.40 (( (v3_struct_0 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | (v1_funct_1 @ (k2_funct_1 @ sk__23)))),
% 5.54/1.40 inference('sup-', [status(thm)], [zip_derived_cl132, zip_derived_cl122])).
% 5.54/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl2899, plain, ( (v1_funct_1 @ (k2_funct_1 @ sk__23))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl2898, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.54/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl131, plain,
% 5.54/1.40 (~ (m2_fraenkel @ (k2_funct_1 @ sk__23) @ (u1_struct_0 @ sk__22) @
% 5.54/1.40 (u1_struct_0 @ sk__22) @ (k1_autgroup @ sk__22))),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl45, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 ( (m1_fraenkel @ (k1_autgroup @ X0) @ (u1_struct_0 @ X0) @
% 5.54/1.40 (u1_struct_0 @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0))),
% 5.54/1.40 inference('cnf', [status(esa)], [dt_k1_autgroup])).
% 5.54/1.40 thf(zip_derived_cl108, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 5.54/1.40 ( (v1_xboole_0 @ X0)
% 5.54/1.40 | ~ (m1_fraenkel @ X1 @ X2 @ X0)
% 5.54/1.40 | (m2_fraenkel @ X3 @ X2 @ X0 @ X1)
% 5.54/1.40 | ~ (m1_subset_1 @ X3 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [redefinition_m2_fraenkel])).
% 5.54/1.40 thf(zip_derived_cl1489, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 ( (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (m1_subset_1 @ X1 @ (k1_autgroup @ X0))
% 5.54/1.40 | (m2_fraenkel @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0) @
% 5.54/1.40 (k1_autgroup @ X0))
% 5.54/1.40 | (v1_xboole_0 @ (u1_struct_0 @ X0)))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl45, zip_derived_cl108])).
% 5.54/1.40 thf(zip_derived_cl1155, plain,
% 5.54/1.40 (![X0 : $i]:
% 5.54/1.40 (~ (l1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0)
% 5.54/1.40 | ~ (v1_xboole_0 @ (u1_struct_0 @ X0)))),
% 5.54/1.40 inference('dp-resolution', [status(thm)],
% 5.54/1.40 [zip_derived_cl48, zip_derived_cl67])).
% 5.54/1.40 thf(zip_derived_cl3121, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 ( (m2_fraenkel @ X1 @ (u1_struct_0 @ X0) @ (u1_struct_0 @ X0) @
% 5.54/1.40 (k1_autgroup @ X0))
% 5.54/1.40 | ~ (m1_subset_1 @ X1 @ (k1_autgroup @ X0))
% 5.54/1.40 | ~ (l1_group_1 @ X0)
% 5.54/1.40 | ~ (v4_group_1 @ X0)
% 5.54/1.40 | ~ (v3_group_1 @ X0)
% 5.54/1.40 | ~ (v1_group_1 @ X0)
% 5.54/1.40 | (v3_struct_0 @ X0))),
% 5.54/1.40 inference('clc', [status(thm)], [zip_derived_cl1489, zip_derived_cl1155])).
% 5.54/1.40 thf(zip_derived_cl3138, plain,
% 5.54/1.40 (( (v3_struct_0 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (l1_group_1 @ sk__22)
% 5.54/1.40 | ~ (m1_subset_1 @ (k2_funct_1 @ sk__23) @ (k1_autgroup @ sk__22)))),
% 5.54/1.40 inference('sup+', [status(thm)], [zip_derived_cl131, zip_derived_cl3121])).
% 5.54/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl3146, plain,
% 5.54/1.40 (~ (m1_subset_1 @ (k2_funct_1 @ sk__23) @ (k1_autgroup @ sk__22))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3138, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.54/1.40 thf(t1_subset, axiom,
% 5.54/1.40 (![A:$i,B:$i]: ( ( r2_hidden @ A @ B ) => ( m1_subset_1 @ A @ B ) ))).
% 5.54/1.40 thf(zip_derived_cl111, plain,
% 5.54/1.40 (![X0 : $i, X1 : $i]:
% 5.54/1.40 ( (m1_subset_1 @ X0 @ X1) | ~ (r2_hidden @ X0 @ X1))),
% 5.54/1.40 inference('cnf', [status(esa)], [t1_subset])).
% 5.54/1.40 thf(zip_derived_cl3156, plain,
% 5.54/1.40 (~ (r2_hidden @ (k2_funct_1 @ sk__23) @ (k1_autgroup @ sk__22))),
% 5.54/1.40 inference('sup+', [status(thm)], [zip_derived_cl3146, zip_derived_cl111])).
% 5.54/1.40 thf(zip_derived_cl4375, plain,
% 5.54/1.40 ((~ (zip_tseitin_1 @ sk__23 @ sk__22)
% 5.54/1.40 | (v1_xboole_0 @ (k1_autgroup @ sk__22))
% 5.54/1.40 | ((k2_funct_1 @ sk__23) != (k2_funct_1 @ sk__23)))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl4364, zip_derived_cl3168, zip_derived_cl3653,
% 5.54/1.40 zip_derived_cl3119, zip_derived_cl130, zip_derived_cl129,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl126, zip_derived_cl2907,
% 5.54/1.40 zip_derived_cl3011, zip_derived_cl2899, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl3156])).
% 5.54/1.40 thf(zip_derived_cl4376, plain,
% 5.54/1.40 (( (v1_xboole_0 @ (k1_autgroup @ sk__22))
% 5.54/1.40 | ~ (zip_tseitin_1 @ sk__23 @ sk__22))),
% 5.54/1.40 inference('simplify', [status(thm)], [zip_derived_cl4375])).
% 5.54/1.40 thf(zip_derived_cl3739, plain,
% 5.54/1.40 (( (zip_tseitin_1 @ sk__23 @ sk__22)
% 5.54/1.40 | (v1_xboole_0 @ (k1_autgroup @ sk__22)))),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl3738, zip_derived_cl126, zip_derived_cl127,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl129, zip_derived_cl130])).
% 5.54/1.40 thf(zip_derived_cl4387, plain, ( (v1_xboole_0 @ (k1_autgroup @ sk__22))),
% 5.54/1.40 inference('clc', [status(thm)], [zip_derived_cl4376, zip_derived_cl3739])).
% 5.54/1.40 thf(zip_derived_cl4396, plain,
% 5.54/1.40 ((~ (l1_group_1 @ sk__22)
% 5.54/1.40 | ~ (v4_group_1 @ sk__22)
% 5.54/1.40 | ~ (v3_group_1 @ sk__22)
% 5.54/1.40 | ~ (v1_group_1 @ sk__22)
% 5.54/1.40 | (v3_struct_0 @ sk__22))),
% 5.54/1.40 inference('sup+', [status(thm)], [zip_derived_cl1483, zip_derived_cl4387])).
% 5.54/1.40 thf(zip_derived_cl130, plain, ( (l1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl129, plain, ( (v4_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl128, plain, ( (v3_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl127, plain, ( (v1_group_1 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl126, plain, (~ (v3_struct_0 @ sk__22)),
% 5.54/1.40 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.54/1.40 thf(zip_derived_cl4397, plain, ($false),
% 5.54/1.40 inference('demod', [status(thm)],
% 5.54/1.40 [zip_derived_cl4396, zip_derived_cl130, zip_derived_cl129,
% 5.54/1.40 zip_derived_cl128, zip_derived_cl127, zip_derived_cl126])).
% 5.54/1.40
% 5.54/1.40 % SZS output end Refutation
% 5.54/1.40
% 5.54/1.40
% 5.54/1.40 % Terminating...
% 5.54/1.48 % Runner terminated.
% 5.54/1.49 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------