%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEU356+2 : TPTP v9.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.LlMXmk8ao3 true
% Computer : n029.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:54:21 PM UTC 2025
% Result : Theorem 52.90s 8.14s
% Output : Refutation 53.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.10 % Problem : SEU356+2 : TPTP v9.2.0. Released v3.3.0.
% 0.05/0.11 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.LlMXmk8ao3 true
% 0.12/0.32 % Computer : n029.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Wed Oct 1 16:07:08 EDT 2025
% 0.12/0.32 % CPUTime :
% 0.12/0.32 % Running portfolio for 300 s
% 0.12/0.32 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.32 % Number of cores: 8
% 0.12/0.32 % Python version: Python 3.6.8
% 0.12/0.32 % Running in FO mode
% 0.45/0.58 % Total configuration time : 435
% 0.45/0.58 % Estimated wc time : 1092
% 0.45/0.58 % Estimated cpu time (7 cpus) : 156.0
% 0.49/0.67 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.49/0.67 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.50/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.50/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.50/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.50/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.50/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 52.90/8.14 % Solved by fo/fo4.sh.
% 52.90/8.14 % done 2927 iterations in 7.410s
% 52.90/8.14 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 52.90/8.14 % SZS output start Refutation
% 52.90/8.14 thf(sk__12_type, type, sk__12: $i).
% 52.90/8.14 thf(rel_str_type, type, rel_str: $i > $o).
% 52.90/8.14 thf(relstr_set_smaller_type, type, relstr_set_smaller: $i > $i > $i > $o).
% 52.90/8.14 thf(antisymmetric_relstr_type, type, antisymmetric_relstr: $i > $o).
% 52.90/8.14 thf(sk__9_type, type, sk__9: $i).
% 52.90/8.14 thf(zip_tseitin_4_type, type, zip_tseitin_4: $i > $i > $i > $i > $o).
% 52.90/8.14 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $i > $i > $o).
% 52.90/8.14 thf(element_type, type, element: $i > $i > $o).
% 52.90/8.14 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $i > $i > $o).
% 52.90/8.14 thf(sk__1_type, type, sk__1: $i > $i > $i > $i).
% 52.90/8.14 thf(sk__2_type, type, sk__2: $i > $i > $i > $i).
% 52.90/8.14 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $i > $o).
% 52.90/8.14 thf(sk__3_type, type, sk__3: $i > $i > $i).
% 52.90/8.14 thf(sk__10_type, type, sk__10: $i).
% 52.90/8.14 thf(ex_sup_of_relstr_set_type, type, ex_sup_of_relstr_set: $i > $i > $o).
% 52.90/8.14 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > $i > $i > $o).
% 52.90/8.14 thf(related_type, type, related: $i > $i > $i > $o).
% 52.90/8.14 thf(the_carrier_type, type, the_carrier: $i > $i).
% 52.90/8.14 thf(sk__11_type, type, sk__11: $i > $i).
% 52.90/8.14 thf(d7_yellow_0, axiom,
% 52.90/8.14 (![A:$i]:
% 52.90/8.14 ( ( rel_str @ A ) =>
% 52.90/8.14 ( ![B:$i]:
% 52.90/8.14 ( ( ex_sup_of_relstr_set @ A @ B ) <=>
% 52.90/8.14 ( ?[C:$i]:
% 52.90/8.14 ( ( element @ C @ ( the_carrier @ A ) ) &
% 52.90/8.14 ( relstr_set_smaller @ A @ B @ C ) &
% 52.90/8.14 ( ![D:$i]:
% 52.90/8.14 ( ( element @ D @ ( the_carrier @ A ) ) =>
% 52.90/8.14 ( ( relstr_set_smaller @ A @ B @ D ) =>
% 52.90/8.14 ( related @ A @ C @ D ) ) ) ) &
% 52.90/8.14 ( ![D:$i]:
% 52.90/8.14 ( ( element @ D @ ( the_carrier @ A ) ) =>
% 52.90/8.14 ( ( ( ![E:$i]:
% 52.90/8.14 ( ( element @ E @ ( the_carrier @ A ) ) =>
% 52.90/8.14 ( ( relstr_set_smaller @ A @ B @ E ) =>
% 52.90/8.14 ( related @ A @ D @ E ) ) ) ) &
% 52.90/8.14 ( relstr_set_smaller @ A @ B @ D ) ) =>
% 52.90/8.14 ( ( D ) = ( C ) ) ) ) ) ) ) ) ) ))).
% 52.90/8.14 thf(zf_stmt_0, type, zip_tseitin_4 : $i > $i > $i > $i > $o).
% 52.90/8.14 thf(zf_stmt_1, axiom,
% 52.90/8.14 (![D:$i,C:$i,B:$i,A:$i]:
% 52.90/8.14 ( ( zip_tseitin_4 @ D @ C @ B @ A ) <=>
% 52.90/8.14 ( ( element @ D @ ( the_carrier @ A ) ) =>
% 52.90/8.14 ( zip_tseitin_3 @ D @ C @ B @ A ) ) ))).
% 52.90/8.14 thf(zf_stmt_2, type, zip_tseitin_3 : $i > $i > $i > $i > $o).
% 52.90/8.14 thf(zf_stmt_3, axiom,
% 52.90/8.14 (![D:$i,C:$i,B:$i,A:$i]:
% 52.90/8.14 ( ( zip_tseitin_3 @ D @ C @ B @ A ) <=>
% 52.90/8.14 ( ( zip_tseitin_2 @ D @ B @ A ) => ( ( D ) = ( C ) ) ) ))).
% 52.90/8.14 thf(zf_stmt_4, type, zip_tseitin_2 : $i > $i > $i > $o).
% 52.90/8.14 thf(zf_stmt_5, axiom,
% 52.90/8.14 (![D:$i,B:$i,A:$i]:
% 52.90/8.14 ( ( zip_tseitin_2 @ D @ B @ A ) <=>
% 52.90/8.14 ( ( relstr_set_smaller @ A @ B @ D ) &
% 52.90/8.14 ( ![E:$i]:
% 52.90/8.14 ( ( element @ E @ ( the_carrier @ A ) ) =>
% 52.90/8.14 ( ( relstr_set_smaller @ A @ B @ E ) => ( related @ A @ D @ E ) ) ) ) ) ))).
% 52.90/8.14 thf(zf_stmt_6, type, zip_tseitin_1 : $i > $i > $i > $i > $o).
% 52.90/8.14 thf(zf_stmt_7, axiom,
% 52.90/8.14 (![D:$i,C:$i,B:$i,A:$i]:
% 52.90/8.14 ( ( zip_tseitin_1 @ D @ C @ B @ A ) <=>
% 52.90/8.14 ( ( element @ D @ ( the_carrier @ A ) ) =>
% 52.90/8.14 ( zip_tseitin_0 @ D @ C @ B @ A ) ) ))).
% 52.90/8.14 thf(zf_stmt_8, type, zip_tseitin_0 : $i > $i > $i > $i > $o).
% 52.90/8.14 thf(zf_stmt_9, axiom,
% 52.90/8.14 (![D:$i,C:$i,B:$i,A:$i]:
% 52.90/8.14 ( ( zip_tseitin_0 @ D @ C @ B @ A ) <=>
% 52.90/8.14 ( ( relstr_set_smaller @ A @ B @ D ) => ( related @ A @ C @ D ) ) ))).
% 52.90/8.14 thf(zf_stmt_10, axiom,
% 52.90/8.14 (![A:$i]:
% 52.90/8.14 ( ( rel_str @ A ) =>
% 52.90/8.14 ( ![B:$i]:
% 52.90/8.14 ( ( ex_sup_of_relstr_set @ A @ B ) <=>
% 52.90/8.14 ( ?[C:$i]:
% 52.90/8.14 ( ( ![D:$i]: ( zip_tseitin_4 @ D @ C @ B @ A ) ) &
% 52.90/8.14 ( ![D:$i]: ( zip_tseitin_1 @ D @ C @ B @ A ) ) &
% 52.90/8.14 ( relstr_set_smaller @ A @ B @ C ) &
% 52.90/8.14 ( element @ C @ ( the_carrier @ A ) ) ) ) ) ) ))).
% 52.90/8.14 thf(zip_derived_cl19, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i]:
% 52.90/8.14 (~ (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | (relstr_set_smaller @ X0 @ X1 @ (sk__3 @ X1 @ X0))
% 52.90/8.14 | ~ (rel_str @ X0))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_10])).
% 52.90/8.14 thf(zip_derived_cl18, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i]:
% 52.90/8.14 (~ (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | (element @ (sk__3 @ X1 @ X0) @ (the_carrier @ X0))
% 52.90/8.14 | ~ (rel_str @ X0))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_10])).
% 52.90/8.14 thf(t15_yellow_0, conjecture,
% 52.90/8.14 (![A:$i]:
% 52.90/8.14 ( ( ( antisymmetric_relstr @ A ) & ( rel_str @ A ) ) =>
% 52.90/8.14 ( ![B:$i]:
% 52.90/8.14 ( ( ex_sup_of_relstr_set @ A @ B ) <=>
% 52.90/8.14 ( ?[C:$i]:
% 52.90/8.14 ( ( ![D:$i]:
% 52.90/8.14 ( ( element @ D @ ( the_carrier @ A ) ) =>
% 52.90/8.14 ( ( relstr_set_smaller @ A @ B @ D ) =>
% 52.90/8.14 ( related @ A @ C @ D ) ) ) ) &
% 52.90/8.14 ( relstr_set_smaller @ A @ B @ C ) &
% 52.90/8.14 ( element @ C @ ( the_carrier @ A ) ) ) ) ) ) ))).
% 52.90/8.14 thf(zf_stmt_11, negated_conjecture,
% 52.90/8.14 (~( ![A:$i]:
% 52.90/8.14 ( ( ( antisymmetric_relstr @ A ) & ( rel_str @ A ) ) =>
% 52.90/8.14 ( ![B:$i]:
% 52.90/8.14 ( ( ex_sup_of_relstr_set @ A @ B ) <=>
% 52.90/8.14 ( ?[C:$i]:
% 52.90/8.14 ( ( ![D:$i]:
% 52.90/8.14 ( ( element @ D @ ( the_carrier @ A ) ) =>
% 52.90/8.14 ( ( relstr_set_smaller @ A @ B @ D ) =>
% 52.90/8.14 ( related @ A @ C @ D ) ) ) ) &
% 52.90/8.14 ( relstr_set_smaller @ A @ B @ C ) &
% 52.90/8.14 ( element @ C @ ( the_carrier @ A ) ) ) ) ) ) ) )),
% 52.90/8.14 inference('cnf.neg', [status(esa)], [t15_yellow_0])).
% 52.90/8.14 thf(zip_derived_cl71, plain,
% 52.90/8.14 (![X0 : $i]:
% 52.90/8.14 (~ (element @ X0 @ (the_carrier @ sk__9))
% 52.90/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ X0)
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__11 @ X0))
% 52.90/8.14 | ~ (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl75, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl2, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (zip_tseitin_0 @ X0 @ X1 @ X2 @ X3)
% 52.90/8.14 | (relstr_set_smaller @ X3 @ X2 @ X0))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_9])).
% 52.90/8.14 thf(zip_derived_cl4, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (zip_tseitin_1 @ X0 @ X1 @ X2 @ X3)
% 52.90/8.14 | ~ (zip_tseitin_0 @ X0 @ X1 @ X2 @ X3))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_7])).
% 52.90/8.14 thf(zip_derived_cl112, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (relstr_set_smaller @ X0 @ X1 @ X3)
% 52.90/8.14 | (zip_tseitin_1 @ X3 @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl2, zip_derived_cl4])).
% 52.90/8.14 thf(zip_derived_cl13, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (zip_tseitin_3 @ X0 @ X1 @ X2 @ X3)
% 52.90/8.14 | (zip_tseitin_2 @ X0 @ X2 @ X3))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_3])).
% 52.90/8.14 thf(zip_derived_cl15, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (zip_tseitin_4 @ X0 @ X1 @ X2 @ X3)
% 52.90/8.14 | ~ (zip_tseitin_3 @ X0 @ X1 @ X2 @ X3))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_1])).
% 52.90/8.14 thf(zip_derived_cl150, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (zip_tseitin_2 @ X3 @ X1 @ X0)
% 52.90/8.14 | (zip_tseitin_4 @ X3 @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl13, zip_derived_cl15])).
% 52.90/8.14 thf(zip_derived_cl17, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 (~ (zip_tseitin_4 @ (sk__1 @ X0 @ X1 @ X2) @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (zip_tseitin_1 @ (sk__2 @ X0 @ X1 @ X2) @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (relstr_set_smaller @ X2 @ X1 @ X0)
% 52.90/8.14 | ~ (element @ X0 @ (the_carrier @ X2))
% 52.90/8.14 | (ex_sup_of_relstr_set @ X2 @ X1)
% 52.90/8.14 | ~ (rel_str @ X2))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_10])).
% 52.90/8.14 thf(zip_derived_cl214, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 ( (zip_tseitin_2 @ (sk__1 @ X2 @ X1 @ X0) @ X1 @ X0)
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (zip_tseitin_1 @ (sk__2 @ X2 @ X1 @ X0) @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl150, zip_derived_cl17])).
% 52.90/8.14 thf(zip_derived_cl2551, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 ( (relstr_set_smaller @ X0 @ X1 @ (sk__2 @ X2 @ X1 @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | (zip_tseitin_2 @ (sk__1 @ X2 @ X1 @ X0) @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl112, zip_derived_cl214])).
% 52.90/8.14 thf(zip_derived_cl19308, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 52.90/8.14 | ~ (rel_str @ sk__9)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl75, zip_derived_cl2551])).
% 52.90/8.14 thf(zip_derived_cl70, plain, ( (rel_str @ sk__9)),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl19394, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('demod', [status(thm)], [zip_derived_cl19308, zip_derived_cl70])).
% 52.90/8.14 thf(zip_derived_cl19395, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl19394])).
% 52.90/8.14 thf(zip_derived_cl76, plain,
% 52.90/8.14 (( (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl19475, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl19395, zip_derived_cl76])).
% 52.90/8.14 thf(zip_derived_cl76, plain,
% 52.90/8.14 (( (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl7, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 (~ (element @ X0 @ (the_carrier @ X1))
% 52.90/8.14 | (related @ X1 @ X2 @ X0)
% 52.90/8.14 | ~ (relstr_set_smaller @ X1 @ X3 @ X0)
% 52.90/8.14 | ~ (zip_tseitin_2 @ X2 @ X3 @ X1))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_5])).
% 52.90/8.14 thf(zip_derived_cl87, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i]:
% 52.90/8.14 ( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (zip_tseitin_2 @ X1 @ X0 @ sk__9)
% 52.90/8.14 | ~ (relstr_set_smaller @ sk__9 @ X0 @ sk__12)
% 52.90/8.14 | (related @ sk__9 @ X1 @ sk__12))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl76, zip_derived_cl7])).
% 52.90/8.14 thf(zip_derived_cl19478, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12)
% 52.90/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl19475, zip_derived_cl87])).
% 52.90/8.14 thf(zip_derived_cl19485, plain,
% 52.90/8.14 ((~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl19478])).
% 52.90/8.14 thf(zip_derived_cl75, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl19526, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl19485, zip_derived_cl75])).
% 52.90/8.14 thf(zip_derived_cl75, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl112, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (relstr_set_smaller @ X0 @ X1 @ X3)
% 52.90/8.14 | (zip_tseitin_1 @ X3 @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl2, zip_derived_cl4])).
% 52.90/8.14 thf(zip_derived_cl16, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (zip_tseitin_4 @ X0 @ X1 @ X2 @ X3)
% 52.90/8.14 | (element @ X0 @ (the_carrier @ X3)))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_1])).
% 52.90/8.14 thf(zip_derived_cl17, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 (~ (zip_tseitin_4 @ (sk__1 @ X0 @ X1 @ X2) @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (zip_tseitin_1 @ (sk__2 @ X0 @ X1 @ X2) @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (relstr_set_smaller @ X2 @ X1 @ X0)
% 52.90/8.14 | ~ (element @ X0 @ (the_carrier @ X2))
% 52.90/8.14 | (ex_sup_of_relstr_set @ X2 @ X1)
% 52.90/8.14 | ~ (rel_str @ X2))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_10])).
% 52.90/8.14 thf(zip_derived_cl178, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 ( (element @ (sk__1 @ X2 @ X1 @ X0) @ (the_carrier @ X0))
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (zip_tseitin_1 @ (sk__2 @ X2 @ X1 @ X0) @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl16, zip_derived_cl17])).
% 52.90/8.14 thf(zip_derived_cl1792, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 ( (relstr_set_smaller @ X0 @ X1 @ (sk__2 @ X2 @ X1 @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | (element @ (sk__1 @ X2 @ X1 @ X0) @ (the_carrier @ X0)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl112, zip_derived_cl178])).
% 52.90/8.14 thf(zip_derived_cl6909, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | ~ (rel_str @ sk__9)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl75, zip_derived_cl1792])).
% 52.90/8.14 thf(zip_derived_cl70, plain, ( (rel_str @ sk__9)),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl6939, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('demod', [status(thm)], [zip_derived_cl6909, zip_derived_cl70])).
% 52.90/8.14 thf(zip_derived_cl6940, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl6939])).
% 52.90/8.14 thf(zip_derived_cl76, plain,
% 52.90/8.14 (( (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl7064, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl6940, zip_derived_cl76])).
% 52.90/8.14 thf(zip_derived_cl75, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl5, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (zip_tseitin_1 @ X0 @ X1 @ X2 @ X3)
% 52.90/8.14 | (element @ X0 @ (the_carrier @ X3)))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_7])).
% 52.90/8.14 thf(zip_derived_cl214, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 ( (zip_tseitin_2 @ (sk__1 @ X2 @ X1 @ X0) @ X1 @ X0)
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (zip_tseitin_1 @ (sk__2 @ X2 @ X1 @ X0) @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl150, zip_derived_cl17])).
% 52.90/8.14 thf(zip_derived_cl2549, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 ( (element @ (sk__2 @ X2 @ X1 @ X0) @ (the_carrier @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | (zip_tseitin_2 @ (sk__1 @ X2 @ X1 @ X0) @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl214])).
% 52.90/8.14 thf(zip_derived_cl15222, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 52.90/8.14 | ~ (rel_str @ sk__9)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl75, zip_derived_cl2549])).
% 52.90/8.14 thf(zip_derived_cl70, plain, ( (rel_str @ sk__9)),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl15303, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('demod', [status(thm)], [zip_derived_cl15222, zip_derived_cl70])).
% 52.90/8.14 thf(zip_derived_cl15304, plain,
% 52.90/8.14 (( (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl15303])).
% 52.90/8.14 thf(zip_derived_cl76, plain,
% 52.90/8.14 (( (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl15493, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl15304, zip_derived_cl76])).
% 52.90/8.14 thf(zip_derived_cl87, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i]:
% 52.90/8.14 ( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (zip_tseitin_2 @ X1 @ X0 @ sk__9)
% 52.90/8.14 | ~ (relstr_set_smaller @ sk__9 @ X0 @ sk__12)
% 52.90/8.14 | (related @ sk__9 @ X1 @ sk__12))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl76, zip_derived_cl7])).
% 52.90/8.14 thf(zip_derived_cl15496, plain,
% 52.90/8.14 (( (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12)
% 52.90/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl15493, zip_derived_cl87])).
% 52.90/8.14 thf(zip_derived_cl15503, plain,
% 52.90/8.14 ((~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl15496])).
% 52.90/8.14 thf(zip_derived_cl75, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl15535, plain,
% 52.90/8.14 (( (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl15503, zip_derived_cl75])).
% 52.90/8.14 thf(zip_derived_cl15493, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl15304, zip_derived_cl76])).
% 52.90/8.14 thf(zip_derived_cl6, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 ( (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (zip_tseitin_2 @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_5])).
% 52.90/8.14 thf(zip_derived_cl15494, plain,
% 52.90/8.14 (( (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__1 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl15493, zip_derived_cl6])).
% 52.90/8.14 thf(zip_derived_cl75, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl5, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (zip_tseitin_1 @ X0 @ X1 @ X2 @ X3)
% 52.90/8.14 | (element @ X0 @ (the_carrier @ X3)))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_7])).
% 52.90/8.14 thf(zip_derived_cl178, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 ( (element @ (sk__1 @ X2 @ X1 @ X0) @ (the_carrier @ X0))
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (zip_tseitin_1 @ (sk__2 @ X2 @ X1 @ X0) @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl16, zip_derived_cl17])).
% 52.90/8.14 thf(zip_derived_cl1790, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 ( (element @ (sk__2 @ X2 @ X1 @ X0) @ (the_carrier @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | (element @ (sk__1 @ X2 @ X1 @ X0) @ (the_carrier @ X0)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl178])).
% 52.90/8.14 thf(zip_derived_cl5753, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | ~ (rel_str @ sk__9)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl75, zip_derived_cl1790])).
% 52.90/8.14 thf(zip_derived_cl70, plain, ( (rel_str @ sk__9)),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl5780, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('demod', [status(thm)], [zip_derived_cl5753, zip_derived_cl70])).
% 52.90/8.14 thf(zip_derived_cl5781, plain,
% 52.90/8.14 (( (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl5780])).
% 52.90/8.14 thf(zip_derived_cl76, plain,
% 52.90/8.14 (( (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl5918, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl5781, zip_derived_cl76])).
% 52.90/8.14 thf(zip_derived_cl74, plain,
% 52.90/8.14 (![X1 : $i]:
% 52.90/8.14 (~ (element @ X1 @ (the_carrier @ sk__9))
% 52.90/8.14 | (related @ sk__9 @ sk__12 @ X1)
% 52.90/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ X1)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl5933, plain,
% 52.90/8.14 (( (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl5918, zip_derived_cl74])).
% 52.90/8.14 thf(zip_derived_cl5952, plain,
% 52.90/8.14 (( (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl5933])).
% 52.90/8.14 thf(zip_derived_cl15516, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('sup-', [status(thm)],
% 52.90/8.14 [zip_derived_cl15494, zip_derived_cl5952])).
% 52.90/8.14 thf(zip_derived_cl15532, plain,
% 52.90/8.14 (( (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl15516])).
% 52.90/8.14 thf(zip_derived_cl5918, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl5781, zip_derived_cl76])).
% 52.90/8.14 thf(zip_derived_cl76, plain,
% 52.90/8.14 (( (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(t25_orders_2, axiom,
% 52.90/8.14 (![A:$i]:
% 52.90/8.14 ( ( ( antisymmetric_relstr @ A ) & ( rel_str @ A ) ) =>
% 52.90/8.14 ( ![B:$i]:
% 52.90/8.14 ( ( element @ B @ ( the_carrier @ A ) ) =>
% 52.90/8.14 ( ![C:$i]:
% 52.90/8.14 ( ( element @ C @ ( the_carrier @ A ) ) =>
% 52.90/8.14 ( ( ( related @ A @ B @ C ) & ( related @ A @ C @ B ) ) =>
% 52.90/8.14 ( ( B ) = ( C ) ) ) ) ) ) ) ))).
% 52.90/8.14 thf(zip_derived_cl60, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 (~ (element @ X0 @ (the_carrier @ X1))
% 52.90/8.14 | ~ (related @ X1 @ X0 @ X2)
% 52.90/8.14 | ~ (related @ X1 @ X2 @ X0)
% 52.90/8.14 | ((X0) = (X2))
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X1))
% 52.90/8.14 | ~ (rel_str @ X1)
% 52.90/8.14 | ~ (antisymmetric_relstr @ X1))),
% 52.90/8.14 inference('cnf', [status(esa)], [t25_orders_2])).
% 52.90/8.14 thf(zip_derived_cl92, plain,
% 52.90/8.14 (![X0 : $i]:
% 52.90/8.14 ( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (antisymmetric_relstr @ sk__9)
% 52.90/8.14 | ~ (rel_str @ sk__9)
% 52.90/8.14 | ~ (element @ X0 @ (the_carrier @ sk__9))
% 52.90/8.14 | ((sk__12) = (X0))
% 52.90/8.14 | ~ (related @ sk__9 @ X0 @ sk__12)
% 52.90/8.14 | ~ (related @ sk__9 @ sk__12 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl76, zip_derived_cl60])).
% 52.90/8.14 thf(zip_derived_cl69, plain, ( (antisymmetric_relstr @ sk__9)),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl70, plain, ( (rel_str @ sk__9)),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl94, plain,
% 52.90/8.14 (![X0 : $i]:
% 52.90/8.14 ( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ X0 @ (the_carrier @ sk__9))
% 52.90/8.14 | ((sk__12) = (X0))
% 52.90/8.14 | ~ (related @ sk__9 @ X0 @ sk__12)
% 52.90/8.14 | ~ (related @ sk__9 @ sk__12 @ X0))),
% 52.90/8.14 inference('demod', [status(thm)],
% 52.90/8.14 [zip_derived_cl92, zip_derived_cl69, zip_derived_cl70])).
% 52.90/8.14 thf(zip_derived_cl5930, plain,
% 52.90/8.14 (( (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | ~ (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12)
% 52.90/8.14 | ((sk__12) = (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl5918, zip_derived_cl94])).
% 52.90/8.14 thf(zip_derived_cl5949, plain,
% 52.90/8.14 ((((sk__12) = (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | ~ (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12)
% 52.90/8.14 | ~ (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl5930])).
% 52.90/8.14 thf(zip_derived_cl75, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl5, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (zip_tseitin_1 @ X0 @ X1 @ X2 @ X3)
% 52.90/8.14 | (element @ X0 @ (the_carrier @ X3)))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_7])).
% 52.90/8.14 thf(zip_derived_cl12, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (zip_tseitin_3 @ X0 @ X1 @ X2 @ X3) | ((X0) != (X1)))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_3])).
% 52.90/8.14 thf(zip_derived_cl15, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (zip_tseitin_4 @ X0 @ X1 @ X2 @ X3)
% 52.90/8.14 | ~ (zip_tseitin_3 @ X0 @ X1 @ X2 @ X3))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_1])).
% 52.90/8.14 thf(zip_derived_cl80, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 (((X3) != (X2)) | (zip_tseitin_4 @ X3 @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl12, zip_derived_cl15])).
% 52.90/8.14 thf(zip_derived_cl17, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 (~ (zip_tseitin_4 @ (sk__1 @ X0 @ X1 @ X2) @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (zip_tseitin_1 @ (sk__2 @ X0 @ X1 @ X2) @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (relstr_set_smaller @ X2 @ X1 @ X0)
% 52.90/8.14 | ~ (element @ X0 @ (the_carrier @ X2))
% 52.90/8.14 | (ex_sup_of_relstr_set @ X2 @ X1)
% 52.90/8.14 | ~ (rel_str @ X2))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_10])).
% 52.90/8.14 thf(zip_derived_cl179, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 (((sk__1 @ X2 @ X1 @ X0) != (X2))
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (zip_tseitin_1 @ (sk__2 @ X2 @ X1 @ X0) @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl80, zip_derived_cl17])).
% 52.90/8.14 thf(zip_derived_cl878, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 ( (element @ (sk__2 @ X2 @ X1 @ X0) @ (the_carrier @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | ((sk__1 @ X2 @ X1 @ X0) != (X2)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl179])).
% 52.90/8.14 thf(zip_derived_cl1077, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ((sk__1 @ sk__12 @ sk__10 @ sk__9) != (sk__12))
% 52.90/8.14 | ~ (rel_str @ sk__9)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl75, zip_derived_cl878])).
% 52.90/8.14 thf(zip_derived_cl70, plain, ( (rel_str @ sk__9)),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl1088, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ((sk__1 @ sk__12 @ sk__10 @ sk__9) != (sk__12))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('demod', [status(thm)], [zip_derived_cl1077, zip_derived_cl70])).
% 52.90/8.14 thf(zip_derived_cl1089, plain,
% 52.90/8.14 (( (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | ((sk__1 @ sk__12 @ sk__10 @ sk__9) != (sk__12))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl1088])).
% 52.90/8.14 thf(zip_derived_cl76, plain,
% 52.90/8.14 (( (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl1093, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ((sk__1 @ sk__12 @ sk__10 @ sk__9) != (sk__12))
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl1089, zip_derived_cl76])).
% 52.90/8.14 thf(zip_derived_cl6146, plain,
% 52.90/8.14 (( (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | ~ (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl5949, zip_derived_cl1093])).
% 52.90/8.14 thf(zip_derived_cl15533, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | ~ (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('sup-', [status(thm)],
% 52.90/8.14 [zip_derived_cl15532, zip_derived_cl6146])).
% 52.90/8.14 thf(zip_derived_cl15534, plain,
% 52.90/8.14 ((~ (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12)
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl15533])).
% 52.90/8.14 thf(zip_derived_cl15536, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__2 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('clc', [status(thm)],
% 52.90/8.14 [zip_derived_cl15535, zip_derived_cl15534])).
% 52.90/8.14 thf(zip_derived_cl74, plain,
% 52.90/8.14 (![X1 : $i]:
% 52.90/8.14 (~ (element @ X1 @ (the_carrier @ sk__9))
% 52.90/8.14 | (related @ sk__9 @ sk__12 @ X1)
% 52.90/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ X1)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl15553, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (related @ sk__9 @ sk__12 @ (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl15536, zip_derived_cl74])).
% 52.90/8.14 thf(zip_derived_cl15574, plain,
% 52.90/8.14 (( (related @ sk__9 @ sk__12 @ (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl15553])).
% 52.90/8.14 thf(zip_derived_cl15579, plain,
% 52.90/8.14 (( (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (related @ sk__9 @ sk__12 @ (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('sup-', [status(thm)],
% 52.90/8.14 [zip_derived_cl7064, zip_derived_cl15574])).
% 52.90/8.14 thf(zip_derived_cl15580, plain,
% 52.90/8.14 (( (related @ sk__9 @ sk__12 @ (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl15579])).
% 52.90/8.14 thf(zip_derived_cl1, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (zip_tseitin_0 @ X0 @ X1 @ X2 @ X3) | ~ (related @ X3 @ X1 @ X0))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_9])).
% 52.90/8.14 thf(zip_derived_cl4, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (zip_tseitin_1 @ X0 @ X1 @ X2 @ X3)
% 52.90/8.14 | ~ (zip_tseitin_0 @ X0 @ X1 @ X2 @ X3))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_7])).
% 52.90/8.14 thf(zip_derived_cl83, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 (~ (related @ X0 @ X2 @ X3) | (zip_tseitin_1 @ X3 @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl4])).
% 52.90/8.14 thf(zip_derived_cl178, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 ( (element @ (sk__1 @ X2 @ X1 @ X0) @ (the_carrier @ X0))
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (zip_tseitin_1 @ (sk__2 @ X2 @ X1 @ X0) @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl16, zip_derived_cl17])).
% 52.90/8.14 thf(zip_derived_cl1791, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 (~ (related @ X0 @ X2 @ (sk__2 @ X2 @ X1 @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | (element @ (sk__1 @ X2 @ X1 @ X0) @ (the_carrier @ X0)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl83, zip_derived_cl178])).
% 52.90/8.14 thf(zip_derived_cl15687, plain,
% 52.90/8.14 (( (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | ~ (rel_str @ sk__9)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12))),
% 52.90/8.14 inference('sup-', [status(thm)],
% 52.90/8.14 [zip_derived_cl15580, zip_derived_cl1791])).
% 52.90/8.14 thf(zip_derived_cl70, plain, ( (rel_str @ sk__9)),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl15692, plain,
% 52.90/8.14 (( (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12))),
% 52.90/8.14 inference('demod', [status(thm)], [zip_derived_cl15687, zip_derived_cl70])).
% 52.90/8.14 thf(zip_derived_cl15693, plain,
% 52.90/8.14 ((~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl15692])).
% 52.90/8.14 thf(zip_derived_cl75, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl15697, plain,
% 52.90/8.14 (( (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl15693, zip_derived_cl75])).
% 52.90/8.14 thf(zip_derived_cl76, plain,
% 52.90/8.14 (( (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl15698, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl15697, zip_derived_cl76])).
% 52.90/8.14 thf(zip_derived_cl94, plain,
% 52.90/8.14 (![X0 : $i]:
% 52.90/8.14 ( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ X0 @ (the_carrier @ sk__9))
% 52.90/8.14 | ((sk__12) = (X0))
% 52.90/8.14 | ~ (related @ sk__9 @ X0 @ sk__12)
% 52.90/8.14 | ~ (related @ sk__9 @ sk__12 @ X0))),
% 52.90/8.14 inference('demod', [status(thm)],
% 52.90/8.14 [zip_derived_cl92, zip_derived_cl69, zip_derived_cl70])).
% 52.90/8.14 thf(zip_derived_cl15712, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | ~ (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12)
% 52.90/8.14 | ((sk__12) = (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl15698, zip_derived_cl94])).
% 52.90/8.14 thf(zip_derived_cl15736, plain,
% 52.90/8.14 ((((sk__12) = (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | ~ (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12)
% 52.90/8.14 | ~ (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl15712])).
% 52.90/8.14 thf(zip_derived_cl19527, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | ((sk__12) = (sk__1 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('sup-', [status(thm)],
% 52.90/8.14 [zip_derived_cl19526, zip_derived_cl15736])).
% 52.90/8.14 thf(zip_derived_cl19528, plain,
% 52.90/8.14 ((((sk__12) = (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | ~ (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl19527])).
% 52.90/8.14 thf(zip_derived_cl75, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl112, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 52.90/8.14 ( (relstr_set_smaller @ X0 @ X1 @ X3)
% 52.90/8.14 | (zip_tseitin_1 @ X3 @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl2, zip_derived_cl4])).
% 52.90/8.14 thf(zip_derived_cl179, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 (((sk__1 @ X2 @ X1 @ X0) != (X2))
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (zip_tseitin_1 @ (sk__2 @ X2 @ X1 @ X0) @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl80, zip_derived_cl17])).
% 52.90/8.14 thf(zip_derived_cl880, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 ( (relstr_set_smaller @ X0 @ X1 @ (sk__2 @ X2 @ X1 @ X0))
% 52.90/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 52.90/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 52.90/8.14 | ~ (rel_str @ X0)
% 52.90/8.14 | ((sk__1 @ X2 @ X1 @ X0) != (X2)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl112, zip_derived_cl179])).
% 52.90/8.14 thf(zip_derived_cl1219, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ((sk__1 @ sk__12 @ sk__10 @ sk__9) != (sk__12))
% 52.90/8.14 | ~ (rel_str @ sk__9)
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('sup-', [status(thm)], [zip_derived_cl75, zip_derived_cl880])).
% 52.90/8.14 thf(zip_derived_cl70, plain, ( (rel_str @ sk__9)),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl1234, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ((sk__1 @ sk__12 @ sk__10 @ sk__9) != (sk__12))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('demod', [status(thm)], [zip_derived_cl1219, zip_derived_cl70])).
% 52.90/8.14 thf(zip_derived_cl1235, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | ((sk__1 @ sk__12 @ sk__10 @ sk__9) != (sk__12))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('simplify', [status(thm)], [zip_derived_cl1234])).
% 52.90/8.14 thf(zip_derived_cl76, plain,
% 52.90/8.14 (( (element @ sk__12 @ (the_carrier @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 52.90/8.14 thf(zip_derived_cl1316, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | ((sk__1 @ sk__12 @ sk__10 @ sk__9) != (sk__12))
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl1235, zip_derived_cl76])).
% 52.90/8.14 thf(zip_derived_cl19662, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | ~ (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl19528, zip_derived_cl1316])).
% 52.90/8.14 thf(zip_derived_cl19475, plain,
% 52.90/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 52.90/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 52.90/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 52.90/8.14 inference('clc', [status(thm)], [zip_derived_cl19395, zip_derived_cl76])).
% 52.90/8.14 thf(zip_derived_cl6, plain,
% 52.90/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 52.90/8.14 ( (relstr_set_smaller @ X0 @ X1 @ X2)
% 52.90/8.14 | ~ (zip_tseitin_2 @ X2 @ X1 @ X0))),
% 52.90/8.14 inference('cnf', [status(esa)], [zf_stmt_5])).
% 52.90/8.14 thf(zip_derived_cl19476, plain,
% 52.90/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @
% 52.90/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 52.90/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 53.06/8.14 (sk__1 @ sk__12 @ sk__10 @ sk__9)))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl19475, zip_derived_cl6])).
% 53.06/8.14 thf(zip_derived_cl15698, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (element @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 53.06/8.14 inference('clc', [status(thm)], [zip_derived_cl15697, zip_derived_cl76])).
% 53.06/8.14 thf(zip_derived_cl74, plain,
% 53.06/8.14 (![X1 : $i]:
% 53.06/8.14 (~ (element @ X1 @ (the_carrier @ sk__9))
% 53.06/8.14 | (related @ sk__9 @ sk__12 @ X1)
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ X1)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 53.06/8.14 thf(zip_derived_cl15717, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @
% 53.06/8.14 (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9)))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl15698, zip_derived_cl74])).
% 53.06/8.14 thf(zip_derived_cl15740, plain,
% 53.06/8.14 (( (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @
% 53.06/8.14 (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl15717])).
% 53.06/8.14 thf(zip_derived_cl19502, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 53.06/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9)))),
% 53.06/8.14 inference('sup-', [status(thm)],
% 53.06/8.14 [zip_derived_cl19476, zip_derived_cl15740])).
% 53.06/8.14 thf(zip_derived_cl19523, plain,
% 53.06/8.14 (( (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 53.06/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl19502])).
% 53.06/8.14 thf(zip_derived_cl19663, plain,
% 53.06/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @
% 53.06/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('clc', [status(thm)],
% 53.06/8.14 [zip_derived_cl19662, zip_derived_cl19523])).
% 53.06/8.14 thf(zip_derived_cl15574, plain,
% 53.06/8.14 (( (related @ sk__9 @ sk__12 @ (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @
% 53.06/8.14 (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl15553])).
% 53.06/8.14 thf(zip_derived_cl19680, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (related @ sk__9 @ sk__12 @ (sk__2 @ sk__12 @ sk__10 @ sk__9)))),
% 53.06/8.14 inference('sup-', [status(thm)],
% 53.06/8.14 [zip_derived_cl19663, zip_derived_cl15574])).
% 53.06/8.14 thf(zip_derived_cl19701, plain,
% 53.06/8.14 (( (related @ sk__9 @ sk__12 @ (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl19680])).
% 53.06/8.14 thf(zip_derived_cl83, plain,
% 53.06/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 53.06/8.14 (~ (related @ X0 @ X2 @ X3) | (zip_tseitin_1 @ X3 @ X2 @ X1 @ X0))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl4])).
% 53.06/8.14 thf(zip_derived_cl214, plain,
% 53.06/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 53.06/8.14 ( (zip_tseitin_2 @ (sk__1 @ X2 @ X1 @ X0) @ X1 @ X0)
% 53.06/8.14 | ~ (rel_str @ X0)
% 53.06/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 53.06/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 53.06/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 53.06/8.14 | ~ (zip_tseitin_1 @ (sk__2 @ X2 @ X1 @ X0) @ X2 @ X1 @ X0))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl150, zip_derived_cl17])).
% 53.06/8.14 thf(zip_derived_cl2550, plain,
% 53.06/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 53.06/8.14 (~ (related @ X0 @ X2 @ (sk__2 @ X2 @ X1 @ X0))
% 53.06/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 53.06/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 53.06/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 53.06/8.14 | ~ (rel_str @ X0)
% 53.06/8.14 | (zip_tseitin_2 @ (sk__1 @ X2 @ X1 @ X0) @ X1 @ X0))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl83, zip_derived_cl214])).
% 53.06/8.14 thf(zip_derived_cl19704, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 53.06/8.14 | ~ (rel_str @ sk__9)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12))),
% 53.06/8.14 inference('sup-', [status(thm)],
% 53.06/8.14 [zip_derived_cl19701, zip_derived_cl2550])).
% 53.06/8.14 thf(zip_derived_cl70, plain, ( (rel_str @ sk__9)),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 53.06/8.14 thf(zip_derived_cl19710, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12))),
% 53.06/8.14 inference('demod', [status(thm)], [zip_derived_cl19704, zip_derived_cl70])).
% 53.06/8.14 thf(zip_derived_cl19711, plain,
% 53.06/8.14 ((~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 53.06/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 53.06/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl19710])).
% 53.06/8.14 thf(zip_derived_cl75, plain,
% 53.06/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 53.06/8.14 thf(zip_derived_cl19876, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 53.06/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9)))),
% 53.06/8.14 inference('clc', [status(thm)], [zip_derived_cl19711, zip_derived_cl75])).
% 53.06/8.14 thf(zip_derived_cl76, plain,
% 53.06/8.14 (( (element @ sk__12 @ (the_carrier @ sk__9))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 53.06/8.14 thf(zip_derived_cl19877, plain,
% 53.06/8.14 (( (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('clc', [status(thm)], [zip_derived_cl19876, zip_derived_cl76])).
% 53.06/8.14 thf(zip_derived_cl6, plain,
% 53.06/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 53.06/8.14 ( (relstr_set_smaller @ X0 @ X1 @ X2)
% 53.06/8.14 | ~ (zip_tseitin_2 @ X2 @ X1 @ X0))),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_5])).
% 53.06/8.14 thf(zip_derived_cl19878, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @
% 53.06/8.14 (sk__1 @ sk__12 @ sk__10 @ sk__9)))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl19877, zip_derived_cl6])).
% 53.06/8.14 thf(zip_derived_cl15740, plain,
% 53.06/8.14 (( (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @
% 53.06/8.14 (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl15717])).
% 53.06/8.14 thf(zip_derived_cl19910, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9)))),
% 53.06/8.14 inference('sup-', [status(thm)],
% 53.06/8.14 [zip_derived_cl19878, zip_derived_cl15740])).
% 53.06/8.14 thf(zip_derived_cl19931, plain,
% 53.06/8.14 (( (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl19910])).
% 53.06/8.14 thf(zip_derived_cl19877, plain,
% 53.06/8.14 (( (zip_tseitin_2 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__10 @ sk__9)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('clc', [status(thm)], [zip_derived_cl19876, zip_derived_cl76])).
% 53.06/8.14 thf(zip_derived_cl87, plain,
% 53.06/8.14 (![X0 : $i, X1 : $i]:
% 53.06/8.14 ( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | ~ (zip_tseitin_2 @ X1 @ X0 @ sk__9)
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ X0 @ sk__12)
% 53.06/8.14 | (related @ sk__9 @ X1 @ sk__12))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl76, zip_derived_cl7])).
% 53.06/8.14 thf(zip_derived_cl19880, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12)
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl19877, zip_derived_cl87])).
% 53.06/8.14 thf(zip_derived_cl19888, plain,
% 53.06/8.14 ((~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 53.06/8.14 | (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl19880])).
% 53.06/8.14 thf(zip_derived_cl75, plain,
% 53.06/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 53.06/8.14 thf(zip_derived_cl19890, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12))),
% 53.06/8.14 inference('clc', [status(thm)], [zip_derived_cl19888, zip_derived_cl75])).
% 53.06/8.14 thf(zip_derived_cl15736, plain,
% 53.06/8.14 ((((sk__12) = (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | ~ (related @ sk__9 @ (sk__1 @ sk__12 @ sk__10 @ sk__9) @ sk__12)
% 53.06/8.14 | ~ (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl15712])).
% 53.06/8.14 thf(zip_derived_cl19891, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | ~ (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | ((sk__12) = (sk__1 @ sk__12 @ sk__10 @ sk__9)))),
% 53.06/8.14 inference('sup-', [status(thm)],
% 53.06/8.14 [zip_derived_cl19890, zip_derived_cl15736])).
% 53.06/8.14 thf(zip_derived_cl19892, plain,
% 53.06/8.14 ((((sk__12) = (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | ~ (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl19891])).
% 53.06/8.14 thf(zip_derived_cl19701, plain,
% 53.06/8.14 (( (related @ sk__9 @ sk__12 @ (sk__2 @ sk__12 @ sk__10 @ sk__9))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl19680])).
% 53.06/8.14 thf(zip_derived_cl83, plain,
% 53.06/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 53.06/8.14 (~ (related @ X0 @ X2 @ X3) | (zip_tseitin_1 @ X3 @ X2 @ X1 @ X0))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl4])).
% 53.06/8.14 thf(zip_derived_cl179, plain,
% 53.06/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 53.06/8.14 (((sk__1 @ X2 @ X1 @ X0) != (X2))
% 53.06/8.14 | ~ (rel_str @ X0)
% 53.06/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 53.06/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 53.06/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 53.06/8.14 | ~ (zip_tseitin_1 @ (sk__2 @ X2 @ X1 @ X0) @ X2 @ X1 @ X0))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl80, zip_derived_cl17])).
% 53.06/8.14 thf(zip_derived_cl879, plain,
% 53.06/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 53.06/8.14 (~ (related @ X0 @ X2 @ (sk__2 @ X2 @ X1 @ X0))
% 53.06/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 53.06/8.14 | ~ (element @ X2 @ (the_carrier @ X0))
% 53.06/8.14 | (ex_sup_of_relstr_set @ X0 @ X1)
% 53.06/8.14 | ~ (rel_str @ X0)
% 53.06/8.14 | ((sk__1 @ X2 @ X1 @ X0) != (X2)))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl83, zip_derived_cl179])).
% 53.06/8.14 thf(zip_derived_cl19702, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | ((sk__1 @ sk__12 @ sk__10 @ sk__9) != (sk__12))
% 53.06/8.14 | ~ (rel_str @ sk__9)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl19701, zip_derived_cl879])).
% 53.06/8.14 thf(zip_derived_cl70, plain, ( (rel_str @ sk__9)),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 53.06/8.14 thf(zip_derived_cl19706, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | ((sk__1 @ sk__12 @ sk__10 @ sk__9) != (sk__12))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12))),
% 53.06/8.14 inference('demod', [status(thm)], [zip_derived_cl19702, zip_derived_cl70])).
% 53.06/8.14 thf(zip_derived_cl19707, plain,
% 53.06/8.14 ((~ (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 53.06/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9))
% 53.06/8.14 | ((sk__1 @ sk__12 @ sk__10 @ sk__9) != (sk__12))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl19706])).
% 53.06/8.14 thf(zip_derived_cl75, plain,
% 53.06/8.14 (( (relstr_set_smaller @ sk__9 @ sk__10 @ sk__12)
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 53.06/8.14 thf(zip_derived_cl19713, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | ((sk__1 @ sk__12 @ sk__10 @ sk__9) != (sk__12))
% 53.06/8.14 | ~ (element @ sk__12 @ (the_carrier @ sk__9)))),
% 53.06/8.14 inference('clc', [status(thm)], [zip_derived_cl19707, zip_derived_cl75])).
% 53.06/8.14 thf(zip_derived_cl76, plain,
% 53.06/8.14 (( (element @ sk__12 @ (the_carrier @ sk__9))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 53.06/8.14 thf(zip_derived_cl19714, plain,
% 53.06/8.14 ((((sk__1 @ sk__12 @ sk__10 @ sk__9) != (sk__12))
% 53.06/8.14 | (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('clc', [status(thm)], [zip_derived_cl19713, zip_derived_cl76])).
% 53.06/8.14 thf(zip_derived_cl19893, plain,
% 53.06/8.14 (( (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | ~ (related @ sk__9 @ sk__12 @ (sk__1 @ sk__12 @ sk__10 @ sk__9)))),
% 53.06/8.14 inference('clc', [status(thm)],
% 53.06/8.14 [zip_derived_cl19892, zip_derived_cl19714])).
% 53.06/8.14 thf(zip_derived_cl19932, plain, ( (ex_sup_of_relstr_set @ sk__9 @ sk__10)),
% 53.06/8.14 inference('clc', [status(thm)],
% 53.06/8.14 [zip_derived_cl19931, zip_derived_cl19893])).
% 53.06/8.14 thf(zip_derived_cl19933, plain,
% 53.06/8.14 (![X0 : $i]:
% 53.06/8.14 (~ (element @ X0 @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ X0)
% 53.06/8.14 | (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__11 @ X0)))),
% 53.06/8.14 inference('demod', [status(thm)], [zip_derived_cl71, zip_derived_cl19932])).
% 53.06/8.14 thf(zip_derived_cl73, plain,
% 53.06/8.14 (![X0 : $i]:
% 53.06/8.14 (~ (element @ X0 @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ X0)
% 53.06/8.14 | (element @ (sk__11 @ X0) @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 53.06/8.14 thf(zip_derived_cl19932, plain, ( (ex_sup_of_relstr_set @ sk__9 @ sk__10)),
% 53.06/8.14 inference('clc', [status(thm)],
% 53.06/8.14 [zip_derived_cl19931, zip_derived_cl19893])).
% 53.06/8.14 thf(zip_derived_cl19935, plain,
% 53.06/8.14 (![X0 : $i]:
% 53.06/8.14 (~ (element @ X0 @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ X0)
% 53.06/8.14 | (element @ (sk__11 @ X0) @ (the_carrier @ sk__9)))),
% 53.06/8.14 inference('demod', [status(thm)], [zip_derived_cl73, zip_derived_cl19932])).
% 53.06/8.14 thf(zip_derived_cl20, plain,
% 53.06/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 53.06/8.14 (~ (ex_sup_of_relstr_set @ X0 @ X1)
% 53.06/8.14 | (zip_tseitin_1 @ X2 @ (sk__3 @ X1 @ X0) @ X1 @ X0)
% 53.06/8.14 | ~ (rel_str @ X0))),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_10])).
% 53.06/8.14 thf(zip_derived_cl3, plain,
% 53.06/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 53.06/8.14 (~ (element @ X0 @ (the_carrier @ X1))
% 53.06/8.14 | (zip_tseitin_0 @ X0 @ X2 @ X3 @ X1)
% 53.06/8.14 | ~ (zip_tseitin_1 @ X0 @ X2 @ X3 @ X1))),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_7])).
% 53.06/8.14 thf(zip_derived_cl0, plain,
% 53.06/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 53.06/8.14 (~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 53.06/8.14 | (related @ X0 @ X3 @ X2)
% 53.06/8.14 | ~ (zip_tseitin_0 @ X2 @ X3 @ X1 @ X0))),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_9])).
% 53.06/8.14 thf(zip_derived_cl143, plain,
% 53.06/8.14 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 53.06/8.14 (~ (zip_tseitin_1 @ X3 @ X2 @ X1 @ X0)
% 53.06/8.14 | ~ (element @ X3 @ (the_carrier @ X0))
% 53.06/8.14 | (related @ X0 @ X2 @ X3)
% 53.06/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X3))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl3, zip_derived_cl0])).
% 53.06/8.14 thf(zip_derived_cl236, plain,
% 53.06/8.14 (![X0 : $i, X1 : $i, X2 : $i]:
% 53.06/8.14 (~ (rel_str @ X0)
% 53.06/8.14 | ~ (ex_sup_of_relstr_set @ X0 @ X1)
% 53.06/8.14 | ~ (relstr_set_smaller @ X0 @ X1 @ X2)
% 53.06/8.14 | (related @ X0 @ (sk__3 @ X1 @ X0) @ X2)
% 53.06/8.14 | ~ (element @ X2 @ (the_carrier @ X0)))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl143])).
% 53.06/8.14 thf(zip_derived_cl72, plain,
% 53.06/8.14 (![X0 : $i]:
% 53.06/8.14 (~ (element @ X0 @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ X0)
% 53.06/8.14 | ~ (related @ sk__9 @ X0 @ (sk__11 @ X0))
% 53.06/8.14 | ~ (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 53.06/8.14 thf(zip_derived_cl19932, plain, ( (ex_sup_of_relstr_set @ sk__9 @ sk__10)),
% 53.06/8.14 inference('clc', [status(thm)],
% 53.06/8.14 [zip_derived_cl19931, zip_derived_cl19893])).
% 53.06/8.14 thf(zip_derived_cl19934, plain,
% 53.06/8.14 (![X0 : $i]:
% 53.06/8.14 (~ (element @ X0 @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ X0)
% 53.06/8.14 | ~ (related @ sk__9 @ X0 @ (sk__11 @ X0)))),
% 53.06/8.14 inference('demod', [status(thm)], [zip_derived_cl72, zip_derived_cl19932])).
% 53.06/8.14 thf(zip_derived_cl20053, plain,
% 53.06/8.14 (![X0 : $i]:
% 53.06/8.14 (~ (element @ (sk__11 @ (sk__3 @ X0 @ sk__9)) @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ X0 @
% 53.06/8.14 (sk__11 @ (sk__3 @ X0 @ sk__9)))
% 53.06/8.14 | ~ (ex_sup_of_relstr_set @ sk__9 @ X0)
% 53.06/8.14 | ~ (rel_str @ sk__9)
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__3 @ X0 @ sk__9))
% 53.06/8.14 | ~ (element @ (sk__3 @ X0 @ sk__9) @ (the_carrier @ sk__9)))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl236, zip_derived_cl19934])).
% 53.06/8.14 thf(zip_derived_cl70, plain, ( (rel_str @ sk__9)),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 53.06/8.14 thf(zip_derived_cl20059, plain,
% 53.06/8.14 (![X0 : $i]:
% 53.06/8.14 (~ (element @ (sk__11 @ (sk__3 @ X0 @ sk__9)) @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ X0 @
% 53.06/8.14 (sk__11 @ (sk__3 @ X0 @ sk__9)))
% 53.06/8.14 | ~ (ex_sup_of_relstr_set @ sk__9 @ X0)
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__3 @ X0 @ sk__9))
% 53.06/8.14 | ~ (element @ (sk__3 @ X0 @ sk__9) @ (the_carrier @ sk__9)))),
% 53.06/8.14 inference('demod', [status(thm)], [zip_derived_cl20053, zip_derived_cl70])).
% 53.06/8.14 thf(zip_derived_cl20130, plain,
% 53.06/8.14 (![X0 : $i]:
% 53.06/8.14 (~ (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__3 @ X0 @ sk__9))
% 53.06/8.14 | ~ (element @ (sk__3 @ X0 @ sk__9) @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (element @ (sk__3 @ X0 @ sk__9) @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__3 @ X0 @ sk__9))
% 53.06/8.14 | ~ (ex_sup_of_relstr_set @ sk__9 @ X0)
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ X0 @
% 53.06/8.14 (sk__11 @ (sk__3 @ X0 @ sk__9))))),
% 53.06/8.14 inference('sup-', [status(thm)],
% 53.06/8.14 [zip_derived_cl19935, zip_derived_cl20059])).
% 53.06/8.14 thf(zip_derived_cl20149, plain,
% 53.06/8.14 (![X0 : $i]:
% 53.06/8.14 (~ (relstr_set_smaller @ sk__9 @ X0 @ (sk__11 @ (sk__3 @ X0 @ sk__9)))
% 53.06/8.14 | ~ (ex_sup_of_relstr_set @ sk__9 @ X0)
% 53.06/8.14 | ~ (element @ (sk__3 @ X0 @ sk__9) @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__3 @ X0 @ sk__9)))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl20130])).
% 53.06/8.14 thf(zip_derived_cl20527, plain,
% 53.06/8.14 ((~ (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__3 @ sk__10 @ sk__9))
% 53.06/8.14 | ~ (element @ (sk__3 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__3 @ sk__10 @ sk__9))
% 53.06/8.14 | ~ (element @ (sk__3 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('sup-', [status(thm)],
% 53.06/8.14 [zip_derived_cl19933, zip_derived_cl20149])).
% 53.06/8.14 thf(zip_derived_cl19932, plain, ( (ex_sup_of_relstr_set @ sk__9 @ sk__10)),
% 53.06/8.14 inference('clc', [status(thm)],
% 53.06/8.14 [zip_derived_cl19931, zip_derived_cl19893])).
% 53.06/8.14 thf(zip_derived_cl20532, plain,
% 53.06/8.14 ((~ (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__3 @ sk__10 @ sk__9))
% 53.06/8.14 | ~ (element @ (sk__3 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__3 @ sk__10 @ sk__9))
% 53.06/8.14 | ~ (element @ (sk__3 @ sk__10 @ sk__9) @ (the_carrier @ sk__9)))),
% 53.06/8.14 inference('demod', [status(thm)],
% 53.06/8.14 [zip_derived_cl20527, zip_derived_cl19932])).
% 53.06/8.14 thf(zip_derived_cl20533, plain,
% 53.06/8.14 ((~ (element @ (sk__3 @ sk__10 @ sk__9) @ (the_carrier @ sk__9))
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__3 @ sk__10 @ sk__9)))),
% 53.06/8.14 inference('simplify', [status(thm)], [zip_derived_cl20532])).
% 53.06/8.14 thf(zip_derived_cl20536, plain,
% 53.06/8.14 ((~ (rel_str @ sk__9)
% 53.06/8.14 | ~ (ex_sup_of_relstr_set @ sk__9 @ sk__10)
% 53.06/8.14 | ~ (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__3 @ sk__10 @ sk__9)))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl18, zip_derived_cl20533])).
% 53.06/8.14 thf(zip_derived_cl70, plain, ( (rel_str @ sk__9)),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 53.06/8.14 thf(zip_derived_cl19932, plain, ( (ex_sup_of_relstr_set @ sk__9 @ sk__10)),
% 53.06/8.14 inference('clc', [status(thm)],
% 53.06/8.14 [zip_derived_cl19931, zip_derived_cl19893])).
% 53.06/8.14 thf(zip_derived_cl20537, plain,
% 53.06/8.14 (~ (relstr_set_smaller @ sk__9 @ sk__10 @ (sk__3 @ sk__10 @ sk__9))),
% 53.06/8.14 inference('demod', [status(thm)],
% 53.06/8.14 [zip_derived_cl20536, zip_derived_cl70, zip_derived_cl19932])).
% 53.06/8.14 thf(zip_derived_cl20538, plain,
% 53.06/8.14 ((~ (rel_str @ sk__9) | ~ (ex_sup_of_relstr_set @ sk__9 @ sk__10))),
% 53.06/8.14 inference('sup-', [status(thm)], [zip_derived_cl19, zip_derived_cl20537])).
% 53.06/8.14 thf(zip_derived_cl70, plain, ( (rel_str @ sk__9)),
% 53.06/8.14 inference('cnf', [status(esa)], [zf_stmt_11])).
% 53.06/8.14 thf(zip_derived_cl19932, plain, ( (ex_sup_of_relstr_set @ sk__9 @ sk__10)),
% 53.06/8.14 inference('clc', [status(thm)],
% 53.06/8.14 [zip_derived_cl19931, zip_derived_cl19893])).
% 53.06/8.14 thf(zip_derived_cl20539, plain, ($false),
% 53.06/8.14 inference('demod', [status(thm)],
% 53.06/8.14 [zip_derived_cl20538, zip_derived_cl70, zip_derived_cl19932])).
% 53.06/8.14
% 53.06/8.14 % SZS output end Refutation
% 53.06/8.14
% 53.06/8.14
% 53.06/8.14 % Terminating...
% 53.06/8.22 % Runner terminated.
% 53.06/8.23 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------