%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEU291+1 : 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.33LsGsySEf true
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 04:54:07 PM UTC 2025
% Result : Theorem 0.60s 0.91s
% Output : Refutation 0.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SEU291+1 : TPTP v9.2.0. Released v3.3.0.
% 0.12/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.33LsGsySEf true
% 0.13/0.34 % Computer : n007.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 1 16:13:38 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % Running portfolio for 300 s
% 0.13/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.35 % Number of cores: 8
% 0.13/0.35 % Python version: Python 3.6.8
% 0.13/0.35 % Running in FO mode
% 0.56/0.64 % Total configuration time : 435
% 0.56/0.64 % Estimated wc time : 1092
% 0.56/0.64 % Estimated cpu time (7 cpus) : 156.0
% 0.58/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.58/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.59/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.59/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.59/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.59/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.59/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.60/0.88 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 0.60/0.91 % Solved by fo/fo3_bce.sh.
% 0.60/0.91 % BCE start: 91
% 0.60/0.91 % BCE eliminated: 6
% 0.60/0.91 % PE start: 85
% 0.60/0.91 logic: eq
% 0.60/0.91 % PE eliminated: 0
% 0.60/0.91 % done 259 iterations in 0.115s
% 0.60/0.91 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.60/0.91 % SZS output start Refutation
% 0.60/0.91 thf(empty_set_type, type, empty_set: $i).
% 0.60/0.91 thf(sk__18_type, type, sk__18: $i).
% 0.60/0.91 thf(function_type, type, function: $i > $o).
% 0.60/0.91 thf(sk__19_type, type, sk__19: $i).
% 0.60/0.91 thf(powerset_type, type, powerset: $i > $i).
% 0.60/0.91 thf(quasi_total_type, type, quasi_total: $i > $i > $i > $o).
% 0.60/0.91 thf(subset_type, type, subset: $i > $i > $o).
% 0.60/0.91 thf(element_type, type, element: $i > $i > $o).
% 0.60/0.91 thf(relation_of2_as_subset_type, type, relation_of2_as_subset: $i > $i > $i > $o).
% 0.60/0.91 thf(relation_dom_as_subset_type, type, relation_dom_as_subset: $i > $i > $i > $i).
% 0.60/0.91 thf(sk__20_type, type, sk__20: $i).
% 0.60/0.91 thf(relation_dom_type, type, relation_dom: $i > $i).
% 0.60/0.91 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $o).
% 0.60/0.91 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $i > $o).
% 0.60/0.91 thf(relation_of2_type, type, relation_of2: $i > $i > $i > $o).
% 0.60/0.91 thf(sk__17_type, type, sk__17: $i).
% 0.60/0.91 thf(t9_funct_2, conjecture,
% 0.60/0.91 (![A:$i,B:$i,C:$i,D:$i]:
% 0.60/0.91 ( ( ( function @ D ) & ( quasi_total @ D @ A @ B ) &
% 0.60/0.91 ( relation_of2_as_subset @ D @ A @ B ) ) =>
% 0.60/0.91 ( ( subset @ B @ C ) =>
% 0.60/0.91 ( ( ( ( B ) = ( empty_set ) ) & ( ( A ) != ( empty_set ) ) ) |
% 0.60/0.91 ( ( function @ D ) & ( quasi_total @ D @ A @ C ) &
% 0.60/0.91 ( relation_of2_as_subset @ D @ A @ C ) ) ) ) ))).
% 0.60/0.91 thf(zf_stmt_0, negated_conjecture,
% 0.60/0.91 (~( ![A:$i,B:$i,C:$i,D:$i]:
% 0.60/0.91 ( ( ( function @ D ) & ( quasi_total @ D @ A @ B ) &
% 0.60/0.91 ( relation_of2_as_subset @ D @ A @ B ) ) =>
% 0.60/0.91 ( ( subset @ B @ C ) =>
% 0.60/0.91 ( ( ( ( B ) = ( empty_set ) ) & ( ( A ) != ( empty_set ) ) ) |
% 0.60/0.91 ( ( function @ D ) & ( quasi_total @ D @ A @ C ) &
% 0.60/0.91 ( relation_of2_as_subset @ D @ A @ C ) ) ) ) ) )),
% 0.60/0.91 inference('cnf.neg', [status(esa)], [t9_funct_2])).
% 0.60/0.91 thf(zip_derived_cl86, plain,
% 0.60/0.91 ( (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__18)),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.60/0.91 thf(zip_derived_cl87, plain, ( (quasi_total @ sk__20 @ sk__17 @ sk__18)),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.60/0.91 thf(d1_funct_2, axiom,
% 0.60/0.91 (![A:$i,B:$i,C:$i]:
% 0.60/0.91 ( ( relation_of2_as_subset @ C @ A @ B ) =>
% 0.60/0.91 ( ( ( ( B ) = ( empty_set ) ) =>
% 0.60/0.91 ( ( ( quasi_total @ C @ A @ B ) <=> ( ( C ) = ( empty_set ) ) ) |
% 0.60/0.91 ( ( A ) = ( empty_set ) ) ) ) &
% 0.60/0.91 ( ( ( ( B ) = ( empty_set ) ) => ( ( A ) = ( empty_set ) ) ) =>
% 0.60/0.91 ( ( quasi_total @ C @ A @ B ) <=>
% 0.60/0.91 ( ( A ) = ( relation_dom_as_subset @ A @ B @ C ) ) ) ) ) ))).
% 0.60/0.91 thf(zf_stmt_1, axiom,
% 0.60/0.91 (![B:$i,A:$i]:
% 0.60/0.91 ( ( ( ( B ) = ( empty_set ) ) => ( ( A ) = ( empty_set ) ) ) =>
% 0.60/0.91 ( zip_tseitin_0 @ B @ A ) ))).
% 0.60/0.91 thf(zip_derived_cl8, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i]: ( (zip_tseitin_0 @ X0 @ X1) | ((X0) = (empty_set)))),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.60/0.91 thf(zf_stmt_2, type, zip_tseitin_1 : $i > $i > $i > $o).
% 0.60/0.91 thf(zf_stmt_3, axiom,
% 0.60/0.91 (![C:$i,B:$i,A:$i]:
% 0.60/0.91 ( ( zip_tseitin_1 @ C @ B @ A ) =>
% 0.60/0.91 ( ( quasi_total @ C @ A @ B ) <=>
% 0.60/0.91 ( ( A ) = ( relation_dom_as_subset @ A @ B @ C ) ) ) ))).
% 0.60/0.91 thf(zf_stmt_4, type, zip_tseitin_0 : $i > $i > $o).
% 0.60/0.91 thf(zf_stmt_5, axiom,
% 0.60/0.91 (![A:$i,B:$i,C:$i]:
% 0.60/0.91 ( ( relation_of2_as_subset @ C @ A @ B ) =>
% 0.60/0.91 ( ( ( zip_tseitin_0 @ B @ A ) => ( zip_tseitin_1 @ C @ B @ A ) ) &
% 0.60/0.91 ( ( ( B ) = ( empty_set ) ) =>
% 0.60/0.91 ( ( ( A ) = ( empty_set ) ) |
% 0.60/0.91 ( ( quasi_total @ C @ A @ B ) <=> ( ( C ) = ( empty_set ) ) ) ) ) ) ))).
% 0.60/0.91 thf(zip_derived_cl11, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (~ (zip_tseitin_0 @ X0 @ X1)
% 0.60/0.91 | (zip_tseitin_1 @ X2 @ X0 @ X1)
% 0.60/0.91 | ~ (relation_of2_as_subset @ X2 @ X1 @ X0))),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.60/0.91 thf(zip_derived_cl349, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (((X1) = (empty_set))
% 0.60/0.91 | ~ (relation_of2_as_subset @ X2 @ X0 @ X1)
% 0.60/0.91 | (zip_tseitin_1 @ X2 @ X1 @ X0))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl8, zip_derived_cl11])).
% 0.60/0.91 thf(zip_derived_cl10, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (~ (quasi_total @ X0 @ X1 @ X2)
% 0.60/0.91 | ((X1) = (relation_dom_as_subset @ X1 @ X2 @ X0))
% 0.60/0.91 | ~ (zip_tseitin_1 @ X0 @ X2 @ X1))),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.60/0.91 thf(zip_derived_cl353, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (~ (relation_of2_as_subset @ X2 @ X1 @ X0)
% 0.60/0.91 | ((X0) = (empty_set))
% 0.60/0.91 | ((X1) = (relation_dom_as_subset @ X1 @ X0 @ X2))
% 0.60/0.91 | ~ (quasi_total @ X2 @ X1 @ X0))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl349, zip_derived_cl10])).
% 0.60/0.91 thf(zip_derived_cl387, plain,
% 0.60/0.91 ((((sk__17) = (relation_dom_as_subset @ sk__17 @ sk__18 @ sk__20))
% 0.60/0.91 | ((sk__18) = (empty_set))
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__18))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl87, zip_derived_cl353])).
% 0.60/0.91 thf(zip_derived_cl86, plain,
% 0.60/0.91 ( (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__18)),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.60/0.91 thf(zip_derived_cl699, plain,
% 0.60/0.91 ((((sk__17) = (relation_dom_as_subset @ sk__17 @ sk__18 @ sk__20))
% 0.60/0.91 | ((sk__18) = (empty_set)))),
% 0.60/0.91 inference('demod', [status(thm)], [zip_derived_cl387, zip_derived_cl86])).
% 0.60/0.91 thf(redefinition_m2_relset_1, axiom,
% 0.60/0.91 (![A:$i,B:$i,C:$i]:
% 0.60/0.91 ( ( relation_of2_as_subset @ C @ A @ B ) <=> ( relation_of2 @ C @ A @ B ) ))).
% 0.60/0.91 thf(zip_derived_cl71, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 ( (relation_of2 @ X0 @ X1 @ X2)
% 0.60/0.91 | ~ (relation_of2_as_subset @ X0 @ X1 @ X2))),
% 0.60/0.91 inference('cnf', [status(esa)], [redefinition_m2_relset_1])).
% 0.60/0.91 thf(redefinition_k4_relset_1, axiom,
% 0.60/0.91 (![A:$i,B:$i,C:$i]:
% 0.60/0.91 ( ( relation_of2 @ C @ A @ B ) =>
% 0.60/0.91 ( ( relation_dom_as_subset @ A @ B @ C ) = ( relation_dom @ C ) ) ))).
% 0.60/0.91 thf(zip_derived_cl70, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (((relation_dom_as_subset @ X1 @ X2 @ X0) = (relation_dom @ X0))
% 0.60/0.91 | ~ (relation_of2 @ X0 @ X1 @ X2))),
% 0.60/0.91 inference('cnf', [status(esa)], [redefinition_k4_relset_1])).
% 0.60/0.91 thf(zip_derived_cl371, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (~ (relation_of2_as_subset @ X2 @ X1 @ X0)
% 0.60/0.91 | ((relation_dom_as_subset @ X1 @ X0 @ X2) = (relation_dom @ X2)))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl71, zip_derived_cl70])).
% 0.60/0.91 thf(zip_derived_cl701, plain,
% 0.60/0.91 ((((sk__17) = (relation_dom @ sk__20))
% 0.60/0.91 | ((sk__18) = (empty_set))
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__18))),
% 0.60/0.91 inference('sup+', [status(thm)], [zip_derived_cl699, zip_derived_cl371])).
% 0.60/0.91 thf(zip_derived_cl86, plain,
% 0.60/0.91 ( (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__18)),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.60/0.91 thf(zip_derived_cl703, plain,
% 0.60/0.91 ((((sk__17) = (relation_dom @ sk__20)) | ((sk__18) = (empty_set)))),
% 0.60/0.91 inference('demod', [status(thm)], [zip_derived_cl701, zip_derived_cl86])).
% 0.60/0.91 thf(zip_derived_cl90, plain, ( (subset @ sk__18 @ sk__19)),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.60/0.91 thf(t16_relset_1, axiom,
% 0.60/0.91 (![A:$i,B:$i,C:$i,D:$i]:
% 0.60/0.91 ( ( relation_of2_as_subset @ D @ C @ A ) =>
% 0.60/0.91 ( ( subset @ A @ B ) => ( relation_of2_as_subset @ D @ C @ B ) ) ))).
% 0.60/0.91 thf(zip_derived_cl74, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.60/0.91 (~ (subset @ X0 @ X1)
% 0.60/0.91 | ~ (relation_of2_as_subset @ X2 @ X3 @ X0)
% 0.60/0.91 | (relation_of2_as_subset @ X2 @ X3 @ X1))),
% 0.60/0.91 inference('cnf', [status(esa)], [t16_relset_1])).
% 0.60/0.91 thf(zip_derived_cl362, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i]:
% 0.60/0.91 ( (relation_of2_as_subset @ X1 @ X0 @ sk__19)
% 0.60/0.91 | ~ (relation_of2_as_subset @ X1 @ X0 @ sk__18))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl90, zip_derived_cl74])).
% 0.60/0.91 thf(zip_derived_cl371, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (~ (relation_of2_as_subset @ X2 @ X1 @ X0)
% 0.60/0.91 | ((relation_dom_as_subset @ X1 @ X0 @ X2) = (relation_dom @ X2)))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl71, zip_derived_cl70])).
% 0.60/0.91 thf(zip_derived_cl349, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (((X1) = (empty_set))
% 0.60/0.91 | ~ (relation_of2_as_subset @ X2 @ X0 @ X1)
% 0.60/0.91 | (zip_tseitin_1 @ X2 @ X1 @ X0))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl8, zip_derived_cl11])).
% 0.60/0.91 thf(zip_derived_cl9, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (((X0) != (relation_dom_as_subset @ X0 @ X1 @ X2))
% 0.60/0.91 | (quasi_total @ X2 @ X0 @ X1)
% 0.60/0.91 | ~ (zip_tseitin_1 @ X2 @ X1 @ X0))),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.60/0.91 thf(zip_derived_cl352, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (~ (relation_of2_as_subset @ X2 @ X1 @ X0)
% 0.60/0.91 | ((X0) = (empty_set))
% 0.60/0.91 | (quasi_total @ X2 @ X1 @ X0)
% 0.60/0.91 | ((X1) != (relation_dom_as_subset @ X1 @ X0 @ X2)))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl349, zip_derived_cl9])).
% 0.60/0.91 thf(zip_derived_cl85, plain,
% 0.60/0.91 ((~ (function @ sk__20)
% 0.60/0.91 | ~ (quasi_total @ sk__20 @ sk__17 @ sk__19)
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__19))),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.60/0.91 thf(zip_derived_cl393, plain,
% 0.60/0.91 ((((sk__17) != (relation_dom_as_subset @ sk__17 @ sk__19 @ sk__20))
% 0.60/0.91 | ((sk__19) = (empty_set))
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__19)
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__19)
% 0.60/0.91 | ~ (function @ sk__20))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl352, zip_derived_cl85])).
% 0.60/0.91 thf(zip_derived_cl725, plain,
% 0.60/0.91 ((~ (function @ sk__20)
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__19)
% 0.60/0.91 | ((sk__19) = (empty_set))
% 0.60/0.91 | ((sk__17) != (relation_dom_as_subset @ sk__17 @ sk__19 @ sk__20)))),
% 0.60/0.91 inference('simplify', [status(thm)], [zip_derived_cl393])).
% 0.60/0.91 thf(zip_derived_cl88, plain, ( (function @ sk__20)),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.60/0.91 thf(zip_derived_cl726, plain,
% 0.60/0.91 ((~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__19)
% 0.60/0.91 | ((sk__19) = (empty_set))
% 0.60/0.91 | ((sk__17) != (relation_dom_as_subset @ sk__17 @ sk__19 @ sk__20)))),
% 0.60/0.91 inference('demod', [status(thm)], [zip_derived_cl725, zip_derived_cl88])).
% 0.60/0.91 thf(zip_derived_cl727, plain,
% 0.60/0.91 ((((sk__17) != (relation_dom @ sk__20))
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__19)
% 0.60/0.91 | ((sk__19) = (empty_set))
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__19))),
% 0.60/0.91 inference('sup-', [status(thm)], [zip_derived_cl371, zip_derived_cl726])).
% 0.60/0.91 thf(zip_derived_cl728, plain,
% 0.60/0.91 ((((sk__19) = (empty_set))
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__19)
% 0.60/0.91 | ((sk__17) != (relation_dom @ sk__20)))),
% 0.60/0.91 inference('simplify', [status(thm)], [zip_derived_cl727])).
% 0.60/0.91 thf(zip_derived_cl777, plain,
% 0.60/0.91 ((~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__18)
% 0.60/0.91 | ((sk__17) != (relation_dom @ sk__20))
% 0.60/0.91 | ((sk__19) = (empty_set)))),
% 0.60/0.91 inference('sup-', [status(thm)], [zip_derived_cl362, zip_derived_cl728])).
% 0.60/0.91 thf(zip_derived_cl86, plain,
% 0.60/0.91 ( (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__18)),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.60/0.91 thf(zip_derived_cl778, plain,
% 0.60/0.91 ((((sk__17) != (relation_dom @ sk__20)) | ((sk__19) = (empty_set)))),
% 0.60/0.91 inference('demod', [status(thm)], [zip_derived_cl777, zip_derived_cl86])).
% 0.60/0.91 thf(zip_derived_cl781, plain,
% 0.60/0.91 ((((sk__17) != (sk__17))
% 0.60/0.91 | ((sk__18) = (empty_set))
% 0.60/0.91 | ((sk__19) = (empty_set)))),
% 0.60/0.91 inference('sup-', [status(thm)], [zip_derived_cl703, zip_derived_cl778])).
% 0.60/0.91 thf(zip_derived_cl782, plain,
% 0.60/0.91 ((((sk__19) = (empty_set)) | ((sk__18) = (empty_set)))),
% 0.60/0.91 inference('simplify', [status(thm)], [zip_derived_cl781])).
% 0.60/0.91 thf(zip_derived_cl90, plain, ( (subset @ sk__18 @ sk__19)),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.60/0.91 thf(t3_xboole_1, axiom,
% 0.60/0.91 (![A:$i]: ( ( subset @ A @ empty_set ) => ( ( A ) = ( empty_set ) ) ))).
% 0.60/0.91 thf(zip_derived_cl79, plain,
% 0.60/0.91 (![X0 : $i]: (((X0) = (empty_set)) | ~ (subset @ X0 @ empty_set))),
% 0.60/0.91 inference('cnf', [status(esa)], [t3_xboole_1])).
% 0.60/0.91 thf(zip_derived_cl366, plain,
% 0.60/0.91 (![X0 : $i]:
% 0.60/0.91 (((sk__18) != (X0)) | ((sk__19) != (empty_set)) | ((X0) = (empty_set)))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl90, zip_derived_cl79])).
% 0.60/0.91 thf(zip_derived_cl785, plain,
% 0.60/0.91 (![X0 : $i]:
% 0.60/0.91 (((empty_set) != (empty_set))
% 0.60/0.91 | ((sk__18) = (empty_set))
% 0.60/0.91 | ((X0) = (empty_set))
% 0.60/0.91 | ((sk__18) != (X0)))),
% 0.60/0.91 inference('sup-', [status(thm)], [zip_derived_cl782, zip_derived_cl366])).
% 0.60/0.91 thf(zip_derived_cl799, plain,
% 0.60/0.91 (![X0 : $i]:
% 0.60/0.91 (((sk__18) != (X0)) | ((X0) = (empty_set)) | ((sk__18) = (empty_set)))),
% 0.60/0.91 inference('simplify', [status(thm)], [zip_derived_cl785])).
% 0.60/0.91 thf(zip_derived_cl804, plain,
% 0.60/0.91 ((((sk__18) = (empty_set)) | ((sk__18) = (empty_set)))),
% 0.60/0.91 inference('eq_res', [status(thm)], [zip_derived_cl799])).
% 0.60/0.91 thf(zip_derived_cl805, plain, (((sk__18) = (empty_set))),
% 0.60/0.91 inference('simplify', [status(thm)], [zip_derived_cl804])).
% 0.60/0.91 thf(zip_derived_cl806, plain,
% 0.60/0.91 ( (relation_of2_as_subset @ sk__20 @ sk__17 @ empty_set)),
% 0.60/0.91 inference('demod', [status(thm)], [zip_derived_cl86, zip_derived_cl805])).
% 0.60/0.91 thf(zip_derived_cl89, plain,
% 0.60/0.91 ((((sk__18) != (empty_set)) | ((sk__17) = (empty_set)))),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.60/0.91 thf(zip_derived_cl805, plain, (((sk__18) = (empty_set))),
% 0.60/0.91 inference('simplify', [status(thm)], [zip_derived_cl804])).
% 0.60/0.91 thf(zip_derived_cl807, plain,
% 0.60/0.91 ((((empty_set) != (empty_set)) | ((sk__17) = (empty_set)))),
% 0.60/0.91 inference('demod', [status(thm)], [zip_derived_cl89, zip_derived_cl805])).
% 0.60/0.91 thf(zip_derived_cl808, plain, (((sk__17) = (empty_set))),
% 0.60/0.91 inference('simplify', [status(thm)], [zip_derived_cl807])).
% 0.60/0.91 thf(zip_derived_cl7, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i]:
% 0.60/0.91 ( (zip_tseitin_0 @ X0 @ X1) | ((X1) != (empty_set)))),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.60/0.91 thf(zip_derived_cl11, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (~ (zip_tseitin_0 @ X0 @ X1)
% 0.60/0.91 | (zip_tseitin_1 @ X2 @ X0 @ X1)
% 0.60/0.91 | ~ (relation_of2_as_subset @ X2 @ X1 @ X0))),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.60/0.91 thf(zip_derived_cl348, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (((X0) != (empty_set))
% 0.60/0.91 | ~ (relation_of2_as_subset @ X2 @ X0 @ X1)
% 0.60/0.91 | (zip_tseitin_1 @ X2 @ X1 @ X0))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl7, zip_derived_cl11])).
% 0.60/0.91 thf(zip_derived_cl9, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (((X0) != (relation_dom_as_subset @ X0 @ X1 @ X2))
% 0.60/0.91 | (quasi_total @ X2 @ X0 @ X1)
% 0.60/0.91 | ~ (zip_tseitin_1 @ X2 @ X1 @ X0))),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.60/0.91 thf(zip_derived_cl350, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (~ (relation_of2_as_subset @ X2 @ X0 @ X1)
% 0.60/0.91 | ((X0) != (empty_set))
% 0.60/0.91 | (quasi_total @ X2 @ X0 @ X1)
% 0.60/0.91 | ((X0) != (relation_dom_as_subset @ X0 @ X1 @ X2)))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl348, zip_derived_cl9])).
% 0.60/0.91 thf(zip_derived_cl85, plain,
% 0.60/0.91 ((~ (function @ sk__20)
% 0.60/0.91 | ~ (quasi_total @ sk__20 @ sk__17 @ sk__19)
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__19))),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.60/0.91 thf(zip_derived_cl389, plain,
% 0.60/0.91 ((((sk__17) != (relation_dom_as_subset @ sk__17 @ sk__19 @ sk__20))
% 0.60/0.91 | ((sk__17) != (empty_set))
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__19)
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__19)
% 0.60/0.91 | ~ (function @ sk__20))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl350, zip_derived_cl85])).
% 0.60/0.91 thf(zip_derived_cl681, plain,
% 0.60/0.91 ((~ (function @ sk__20)
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ sk__17 @ sk__19)
% 0.60/0.91 | ((sk__17) != (empty_set))
% 0.60/0.91 | ((sk__17) != (relation_dom_as_subset @ sk__17 @ sk__19 @ sk__20)))),
% 0.60/0.91 inference('simplify', [status(thm)], [zip_derived_cl389])).
% 0.60/0.91 thf(zip_derived_cl682, plain,
% 0.60/0.91 ((~ (function @ sk__20)
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ empty_set @ sk__19)
% 0.60/0.91 | ((sk__17) != (empty_set))
% 0.60/0.91 | ((empty_set)
% 0.60/0.91 != (relation_dom_as_subset @ empty_set @ sk__19 @ sk__20)))),
% 0.60/0.91 inference('local_rewriting', [status(thm)], [zip_derived_cl681])).
% 0.60/0.91 thf(zip_derived_cl88, plain, ( (function @ sk__20)),
% 0.60/0.91 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.60/0.91 thf(zip_derived_cl683, plain,
% 0.60/0.91 ((~ (relation_of2_as_subset @ sk__20 @ empty_set @ sk__19)
% 0.60/0.91 | ((sk__17) != (empty_set))
% 0.60/0.91 | ((empty_set)
% 0.60/0.91 != (relation_dom_as_subset @ empty_set @ sk__19 @ sk__20)))),
% 0.60/0.91 inference('demod', [status(thm)], [zip_derived_cl682, zip_derived_cl88])).
% 0.60/0.91 thf(zip_derived_cl71, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 ( (relation_of2 @ X0 @ X1 @ X2)
% 0.60/0.91 | ~ (relation_of2_as_subset @ X0 @ X1 @ X2))),
% 0.60/0.91 inference('cnf', [status(esa)], [redefinition_m2_relset_1])).
% 0.60/0.91 thf(dt_k4_relset_1, axiom,
% 0.60/0.91 (![A:$i,B:$i,C:$i]:
% 0.60/0.91 ( ( relation_of2 @ C @ A @ B ) =>
% 0.60/0.91 ( element @ ( relation_dom_as_subset @ A @ B @ C ) @ ( powerset @ A ) ) ))).
% 0.60/0.91 thf(zip_derived_cl18, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 ( (element @ (relation_dom_as_subset @ X0 @ X1 @ X2) @ (powerset @ X0))
% 0.60/0.91 | ~ (relation_of2 @ X2 @ X0 @ X1))),
% 0.60/0.91 inference('cnf', [status(esa)], [dt_k4_relset_1])).
% 0.60/0.91 thf(zip_derived_cl370, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.60/0.91 (~ (relation_of2_as_subset @ X2 @ X1 @ X0)
% 0.60/0.91 | (element @ (relation_dom_as_subset @ X1 @ X0 @ X2) @
% 0.60/0.91 (powerset @ X1)))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl71, zip_derived_cl18])).
% 0.60/0.91 thf(t3_subset, axiom,
% 0.60/0.91 (![A:$i,B:$i]:
% 0.60/0.91 ( ( element @ A @ ( powerset @ B ) ) <=> ( subset @ A @ B ) ))).
% 0.60/0.91 thf(zip_derived_cl77, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i]:
% 0.60/0.91 ( (subset @ X0 @ X1) | ~ (element @ X0 @ (powerset @ X1)))),
% 0.60/0.91 inference('cnf', [status(esa)], [t3_subset])).
% 0.60/0.91 thf(zip_derived_cl79, plain,
% 0.60/0.91 (![X0 : $i]: (((X0) = (empty_set)) | ~ (subset @ X0 @ empty_set))),
% 0.60/0.91 inference('cnf', [status(esa)], [t3_xboole_1])).
% 0.60/0.91 thf(zip_derived_cl361, plain,
% 0.60/0.91 (![X0 : $i]:
% 0.60/0.91 (~ (element @ X0 @ (powerset @ empty_set)) | ((X0) = (empty_set)))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl77, zip_derived_cl79])).
% 0.60/0.91 thf(zip_derived_cl543, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i]:
% 0.60/0.91 (~ (relation_of2_as_subset @ X0 @ empty_set @ X1)
% 0.60/0.91 | ((relation_dom_as_subset @ empty_set @ X1 @ X0) = (empty_set)))),
% 0.60/0.91 inference('sup-', [status(thm)], [zip_derived_cl370, zip_derived_cl361])).
% 0.60/0.91 thf(zip_derived_cl684, plain,
% 0.60/0.91 ((((sk__17) != (empty_set))
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ empty_set @ sk__19))),
% 0.60/0.91 inference('clc', [status(thm)], [zip_derived_cl683, zip_derived_cl543])).
% 0.60/0.91 thf(zip_derived_cl362, plain,
% 0.60/0.91 (![X0 : $i, X1 : $i]:
% 0.60/0.91 ( (relation_of2_as_subset @ X1 @ X0 @ sk__19)
% 0.60/0.91 | ~ (relation_of2_as_subset @ X1 @ X0 @ sk__18))),
% 0.60/0.91 inference('dp-resolution', [status(thm)],
% 0.60/0.91 [zip_derived_cl90, zip_derived_cl74])).
% 0.60/0.91 thf(zip_derived_cl685, plain,
% 0.60/0.91 ((((sk__17) != (empty_set))
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ empty_set @ sk__18))),
% 0.60/0.91 inference('sup+', [status(thm)], [zip_derived_cl684, zip_derived_cl362])).
% 0.60/0.91 thf(zip_derived_cl805, plain, (((sk__18) = (empty_set))),
% 0.60/0.91 inference('simplify', [status(thm)], [zip_derived_cl804])).
% 0.60/0.91 thf(zip_derived_cl826, plain,
% 0.60/0.91 ((((sk__17) != (empty_set))
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ empty_set @ empty_set))),
% 0.60/0.91 inference('demod', [status(thm)], [zip_derived_cl685, zip_derived_cl805])).
% 0.60/0.91 thf(zip_derived_cl808, plain, (((sk__17) = (empty_set))),
% 0.60/0.91 inference('simplify', [status(thm)], [zip_derived_cl807])).
% 0.60/0.91 thf(zip_derived_cl842, plain,
% 0.60/0.91 ((((empty_set) != (empty_set))
% 0.60/0.91 | ~ (relation_of2_as_subset @ sk__20 @ empty_set @ empty_set))),
% 0.60/0.91 inference('demod', [status(thm)], [zip_derived_cl826, zip_derived_cl808])).
% 0.60/0.91 thf(zip_derived_cl843, plain,
% 0.60/0.91 (~ (relation_of2_as_subset @ sk__20 @ empty_set @ empty_set)),
% 0.60/0.91 inference('simplify', [status(thm)], [zip_derived_cl842])).
% 0.60/0.91 thf(zip_derived_cl849, plain, ($false),
% 0.60/0.91 inference('demod', [status(thm)],
% 0.60/0.91 [zip_derived_cl806, zip_derived_cl808, zip_derived_cl843])).
% 0.60/0.91
% 0.60/0.91 % SZS output end Refutation
% 0.60/0.91
% 0.60/0.91
% 0.60/0.91 % Terminating...
% 0.62/1.00 % Runner terminated.
% 2.00/1.01 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------