%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEU228+3 : TPTP v9.2.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.qytigATidQ true
% Computer : n019.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:53:55 PM UTC 2025
% Result : Theorem 0.54s 0.97s
% Output : Refutation 0.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SEU228+3 : TPTP v9.2.0. Released v3.2.0.
% 0.03/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.qytigATidQ true
% 0.13/0.36 % Computer : n019.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Wed Oct 1 16:01:08 EDT 2025
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Running portfolio for 300 s
% 0.13/0.36 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.36 % Number of cores: 8
% 0.13/0.36 % Python version: Python 3.6.8
% 0.13/0.37 % Running in FO mode
% 0.52/0.64 % Total configuration time : 435
% 0.52/0.64 % Estimated wc time : 1092
% 0.52/0.64 % Estimated cpu time (7 cpus) : 156.0
% 0.52/0.72 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.52/0.74 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.52/0.75 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.52/0.75 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.52/0.75 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.52/0.75 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.52/0.75 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.54/0.97 % Solved by fo/fo4.sh.
% 0.54/0.97 % done 210 iterations in 0.170s
% 0.54/0.97 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.54/0.97 % SZS output start Refutation
% 0.54/0.97 thf(apply_type, type, apply: $i > $i > $i).
% 0.54/0.97 thf(relation_rng_type, type, relation_rng: $i > $i).
% 0.54/0.97 thf(function_type, type, function: $i > $o).
% 0.54/0.97 thf(subset_type, type, subset: $i > $i > $o).
% 0.54/0.97 thf(in_type, type, in: $i > $i > $o).
% 0.54/0.97 thf(relation_inverse_image_type, type, relation_inverse_image: $i > $i > $i).
% 0.54/0.97 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $i > $i > $o).
% 0.54/0.97 thf(sk__4_type, type, sk__4: $i > $i > $i).
% 0.54/0.97 thf(sk__7_type, type, sk__7: $i > $i > $i).
% 0.54/0.97 thf(relation_dom_type, type, relation_dom: $i > $i).
% 0.54/0.97 thf(relation_image_type, type, relation_image: $i > $i > $i).
% 0.54/0.97 thf(sk__13_type, type, sk__13: $i).
% 0.54/0.97 thf(relation_type, type, relation: $i > $o).
% 0.54/0.97 thf(sk__12_type, type, sk__12: $i).
% 0.54/0.97 thf(t145_funct_1, axiom,
% 0.54/0.97 (![A:$i,B:$i]:
% 0.54/0.97 ( ( ( relation @ B ) & ( function @ B ) ) =>
% 0.54/0.97 ( subset @
% 0.54/0.97 ( relation_image @ B @ ( relation_inverse_image @ B @ A ) ) @ A ) ))).
% 0.54/0.97 thf(zip_derived_cl41, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i]:
% 0.54/0.97 ( (subset @
% 0.54/0.97 (relation_image @ X0 @ (relation_inverse_image @ X0 @ X1)) @ X1)
% 0.54/0.97 | ~ (function @ X0)
% 0.54/0.97 | ~ (relation @ X0))),
% 0.54/0.97 inference('cnf', [status(esa)], [t145_funct_1])).
% 0.54/0.97 thf(d10_xboole_0, axiom,
% 0.54/0.97 (![A:$i,B:$i]:
% 0.54/0.97 ( ( ( A ) = ( B ) ) <=> ( ( subset @ A @ B ) & ( subset @ B @ A ) ) ))).
% 0.54/0.97 thf(zip_derived_cl4, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i]:
% 0.54/0.97 (((X1) = (X0)) | ~ (subset @ X0 @ X1) | ~ (subset @ X1 @ X0))),
% 0.54/0.97 inference('cnf', [status(esa)], [d10_xboole_0])).
% 0.54/0.97 thf(zip_derived_cl88, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i]:
% 0.54/0.97 (~ (relation @ X1)
% 0.54/0.97 | ~ (function @ X1)
% 0.54/0.97 | ~ (subset @ X0 @
% 0.54/0.97 (relation_image @ X1 @ (relation_inverse_image @ X1 @ X0)))
% 0.54/0.97 | ((X0) = (relation_image @ X1 @ (relation_inverse_image @ X1 @ X0))))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl41, zip_derived_cl4])).
% 0.54/0.97 thf(d3_tarski, axiom,
% 0.54/0.97 (![A:$i,B:$i]:
% 0.54/0.97 ( ( subset @ A @ B ) <=> ( ![C:$i]: ( ( in @ C @ A ) => ( in @ C @ B ) ) ) ))).
% 0.54/0.97 thf(zip_derived_cl20, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i]:
% 0.54/0.97 ( (subset @ X0 @ X1) | ~ (in @ (sk__4 @ X1 @ X0) @ X1))),
% 0.54/0.97 inference('cnf', [status(esa)], [d3_tarski])).
% 0.54/0.97 thf(t147_funct_1, conjecture,
% 0.54/0.97 (![A:$i,B:$i]:
% 0.54/0.97 ( ( ( relation @ B ) & ( function @ B ) ) =>
% 0.54/0.97 ( ( subset @ A @ ( relation_rng @ B ) ) =>
% 0.54/0.97 ( ( relation_image @ B @ ( relation_inverse_image @ B @ A ) ) = ( A ) ) ) ))).
% 0.54/0.97 thf(zf_stmt_0, negated_conjecture,
% 0.54/0.97 (~( ![A:$i,B:$i]:
% 0.54/0.97 ( ( ( relation @ B ) & ( function @ B ) ) =>
% 0.54/0.97 ( ( subset @ A @ ( relation_rng @ B ) ) =>
% 0.54/0.97 ( ( relation_image @ B @ ( relation_inverse_image @ B @ A ) ) =
% 0.54/0.97 ( A ) ) ) ) )),
% 0.54/0.97 inference('cnf.neg', [status(esa)], [t147_funct_1])).
% 0.54/0.97 thf(zip_derived_cl44, plain, ( (relation @ sk__13)),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.54/0.97 thf(zip_derived_cl47, plain, ( (subset @ sk__12 @ (relation_rng @ sk__13))),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.54/0.97 thf(zip_derived_cl21, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i]:
% 0.54/0.97 ( (subset @ X0 @ X1) | (in @ (sk__4 @ X1 @ X0) @ X0))),
% 0.54/0.97 inference('cnf', [status(esa)], [d3_tarski])).
% 0.54/0.97 thf(zip_derived_cl19, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.97 (~ (in @ X0 @ X1) | (in @ X0 @ X2) | ~ (subset @ X1 @ X2))),
% 0.54/0.97 inference('cnf', [status(esa)], [d3_tarski])).
% 0.54/0.97 thf(zip_derived_cl79, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.97 ( (subset @ X0 @ X1)
% 0.54/0.97 | ~ (subset @ X0 @ X2)
% 0.54/0.97 | (in @ (sk__4 @ X1 @ X0) @ X2))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl21, zip_derived_cl19])).
% 0.54/0.97 thf(zip_derived_cl86, plain,
% 0.54/0.97 (![X0 : $i]:
% 0.54/0.97 ( (in @ (sk__4 @ X0 @ sk__12) @ (relation_rng @ sk__13))
% 0.54/0.97 | (subset @ sk__12 @ X0))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl47, zip_derived_cl79])).
% 0.54/0.97 thf(d5_funct_1, axiom,
% 0.54/0.97 (![A:$i]:
% 0.54/0.97 ( ( ( relation @ A ) & ( function @ A ) ) =>
% 0.54/0.97 ( ![B:$i]:
% 0.54/0.97 ( ( ( B ) = ( relation_rng @ A ) ) <=>
% 0.54/0.97 ( ![C:$i]:
% 0.54/0.97 ( ( in @ C @ B ) <=>
% 0.54/0.97 ( ?[D:$i]:
% 0.54/0.97 ( ( ( C ) = ( apply @ A @ D ) ) &
% 0.54/0.97 ( in @ D @ ( relation_dom @ A ) ) ) ) ) ) ) ) ))).
% 0.54/0.97 thf(zip_derived_cl25, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.97 (((X1) != (relation_rng @ X0))
% 0.54/0.97 | ((X2) = (apply @ X0 @ (sk__7 @ X2 @ X0)))
% 0.54/0.97 | ~ (in @ X2 @ X1)
% 0.54/0.97 | ~ (function @ X0)
% 0.54/0.97 | ~ (relation @ X0))),
% 0.54/0.97 inference('cnf', [status(esa)], [d5_funct_1])).
% 0.54/0.97 thf(zip_derived_cl101, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i]:
% 0.54/0.97 ( (subset @ sk__12 @ X0)
% 0.54/0.97 | ~ (relation @ X1)
% 0.54/0.97 | ~ (function @ X1)
% 0.54/0.97 | ((sk__4 @ X0 @ sk__12)
% 0.54/0.97 = (apply @ X1 @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ X1)))
% 0.54/0.97 | ((relation_rng @ sk__13) != (relation_rng @ X1)))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl86, zip_derived_cl25])).
% 0.54/0.97 thf(zip_derived_cl227, plain,
% 0.54/0.97 (![X0 : $i]:
% 0.54/0.97 (((relation_rng @ sk__13) != (relation_rng @ sk__13))
% 0.54/0.97 | ((sk__4 @ X0 @ sk__12)
% 0.54/0.97 = (apply @ sk__13 @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13)))
% 0.54/0.97 | ~ (function @ sk__13)
% 0.54/0.97 | (subset @ sk__12 @ X0))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl44, zip_derived_cl101])).
% 0.54/0.97 thf(zip_derived_cl45, plain, ( (function @ sk__13)),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.54/0.97 thf(zip_derived_cl231, plain,
% 0.54/0.97 (![X0 : $i]:
% 0.54/0.97 (((relation_rng @ sk__13) != (relation_rng @ sk__13))
% 0.54/0.97 | ((sk__4 @ X0 @ sk__12)
% 0.54/0.97 = (apply @ sk__13 @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13)))
% 0.54/0.97 | (subset @ sk__12 @ X0))),
% 0.54/0.97 inference('demod', [status(thm)], [zip_derived_cl227, zip_derived_cl45])).
% 0.54/0.97 thf(zip_derived_cl232, plain,
% 0.54/0.97 (![X0 : $i]:
% 0.54/0.97 ( (subset @ sk__12 @ X0)
% 0.54/0.97 | ((sk__4 @ X0 @ sk__12)
% 0.54/0.97 = (apply @ sk__13 @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13))))),
% 0.54/0.97 inference('simplify', [status(thm)], [zip_derived_cl231])).
% 0.54/0.97 thf(zip_derived_cl21, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i]:
% 0.54/0.97 ( (subset @ X0 @ X1) | (in @ (sk__4 @ X1 @ X0) @ X0))),
% 0.54/0.97 inference('cnf', [status(esa)], [d3_tarski])).
% 0.54/0.97 thf(zip_derived_cl232, plain,
% 0.54/0.97 (![X0 : $i]:
% 0.54/0.97 ( (subset @ sk__12 @ X0)
% 0.54/0.97 | ((sk__4 @ X0 @ sk__12)
% 0.54/0.97 = (apply @ sk__13 @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13))))),
% 0.54/0.97 inference('simplify', [status(thm)], [zip_derived_cl231])).
% 0.54/0.97 thf(d13_funct_1, axiom,
% 0.54/0.97 (![A:$i]:
% 0.54/0.97 ( ( ( relation @ A ) & ( function @ A ) ) =>
% 0.54/0.97 ( ![B:$i,C:$i]:
% 0.54/0.97 ( ( ( C ) = ( relation_inverse_image @ A @ B ) ) <=>
% 0.54/0.97 ( ![D:$i]:
% 0.54/0.97 ( ( in @ D @ C ) <=>
% 0.54/0.97 ( ( in @ D @ ( relation_dom @ A ) ) &
% 0.54/0.97 ( in @ ( apply @ A @ D ) @ B ) ) ) ) ) ) ))).
% 0.54/0.97 thf(zip_derived_cl18, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.54/0.97 (((X2) != (relation_inverse_image @ X0 @ X1))
% 0.54/0.97 | (in @ X3 @ X2)
% 0.54/0.97 | ~ (in @ (apply @ X0 @ X3) @ X1)
% 0.54/0.97 | ~ (in @ X3 @ (relation_dom @ X0))
% 0.54/0.97 | ~ (function @ X0)
% 0.54/0.97 | ~ (relation @ X0))),
% 0.54/0.97 inference('cnf', [status(esa)], [d13_funct_1])).
% 0.54/0.97 thf(zip_derived_cl233, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.97 (~ (in @ (sk__4 @ X0 @ sk__12) @ X1)
% 0.54/0.97 | (subset @ sk__12 @ X0)
% 0.54/0.97 | ~ (relation @ sk__13)
% 0.54/0.97 | ~ (function @ sk__13)
% 0.54/0.97 | ~ (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @
% 0.54/0.97 (relation_dom @ sk__13))
% 0.54/0.97 | (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @ X2)
% 0.54/0.97 | ((X2) != (relation_inverse_image @ sk__13 @ X1)))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl232, zip_derived_cl18])).
% 0.54/0.97 thf(zip_derived_cl44, plain, ( (relation @ sk__13)),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.54/0.97 thf(zip_derived_cl45, plain, ( (function @ sk__13)),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.54/0.97 thf(zip_derived_cl236, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.97 (~ (in @ (sk__4 @ X0 @ sk__12) @ X1)
% 0.54/0.97 | (subset @ sk__12 @ X0)
% 0.54/0.97 | ~ (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @
% 0.54/0.97 (relation_dom @ sk__13))
% 0.54/0.97 | (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @ X2)
% 0.54/0.97 | ((X2) != (relation_inverse_image @ sk__13 @ X1)))),
% 0.54/0.97 inference('demod', [status(thm)],
% 0.54/0.97 [zip_derived_cl233, zip_derived_cl44, zip_derived_cl45])).
% 0.54/0.97 thf(zip_derived_cl44, plain, ( (relation @ sk__13)),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.54/0.97 thf(zip_derived_cl86, plain,
% 0.54/0.97 (![X0 : $i]:
% 0.54/0.97 ( (in @ (sk__4 @ X0 @ sk__12) @ (relation_rng @ sk__13))
% 0.54/0.97 | (subset @ sk__12 @ X0))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl47, zip_derived_cl79])).
% 0.54/0.97 thf(zip_derived_cl26, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.97 (((X1) != (relation_rng @ X0))
% 0.54/0.97 | (in @ (sk__7 @ X2 @ X0) @ (relation_dom @ X0))
% 0.54/0.97 | ~ (in @ X2 @ X1)
% 0.54/0.97 | ~ (function @ X0)
% 0.54/0.97 | ~ (relation @ X0))),
% 0.54/0.97 inference('cnf', [status(esa)], [d5_funct_1])).
% 0.54/0.97 thf(zip_derived_cl102, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i]:
% 0.54/0.97 ( (subset @ sk__12 @ X0)
% 0.54/0.97 | ~ (relation @ X1)
% 0.54/0.97 | ~ (function @ X1)
% 0.54/0.97 | (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ X1) @ (relation_dom @ X1))
% 0.54/0.97 | ((relation_rng @ sk__13) != (relation_rng @ X1)))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl86, zip_derived_cl26])).
% 0.54/0.97 thf(zip_derived_cl147, plain,
% 0.54/0.97 (![X0 : $i]:
% 0.54/0.97 (((relation_rng @ sk__13) != (relation_rng @ sk__13))
% 0.54/0.97 | (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @
% 0.54/0.97 (relation_dom @ sk__13))
% 0.54/0.97 | ~ (function @ sk__13)
% 0.54/0.97 | (subset @ sk__12 @ X0))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl44, zip_derived_cl102])).
% 0.54/0.97 thf(zip_derived_cl45, plain, ( (function @ sk__13)),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.54/0.97 thf(zip_derived_cl151, plain,
% 0.54/0.97 (![X0 : $i]:
% 0.54/0.97 (((relation_rng @ sk__13) != (relation_rng @ sk__13))
% 0.54/0.97 | (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @
% 0.54/0.97 (relation_dom @ sk__13))
% 0.54/0.97 | (subset @ sk__12 @ X0))),
% 0.54/0.97 inference('demod', [status(thm)], [zip_derived_cl147, zip_derived_cl45])).
% 0.54/0.97 thf(zip_derived_cl152, plain,
% 0.54/0.97 (![X0 : $i]:
% 0.54/0.97 ( (subset @ sk__12 @ X0)
% 0.54/0.97 | (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @
% 0.54/0.97 (relation_dom @ sk__13)))),
% 0.54/0.97 inference('simplify', [status(thm)], [zip_derived_cl151])).
% 0.54/0.97 thf(zip_derived_cl385, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.97 (((X2) != (relation_inverse_image @ sk__13 @ X1))
% 0.54/0.97 | (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @ X2)
% 0.54/0.97 | (subset @ sk__12 @ X0)
% 0.54/0.97 | ~ (in @ (sk__4 @ X0 @ sk__12) @ X1))),
% 0.54/0.97 inference('clc', [status(thm)], [zip_derived_cl236, zip_derived_cl152])).
% 0.54/0.97 thf(zip_derived_cl386, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i]:
% 0.54/0.97 ( (subset @ sk__12 @ X0)
% 0.54/0.97 | (subset @ sk__12 @ X0)
% 0.54/0.97 | (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @ X1)
% 0.54/0.97 | ((X1) != (relation_inverse_image @ sk__13 @ sk__12)))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl21, zip_derived_cl385])).
% 0.54/0.97 thf(zip_derived_cl389, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i]:
% 0.54/0.97 (((X1) != (relation_inverse_image @ sk__13 @ sk__12))
% 0.54/0.97 | (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @ X1)
% 0.54/0.97 | (subset @ sk__12 @ X0))),
% 0.54/0.97 inference('simplify', [status(thm)], [zip_derived_cl386])).
% 0.54/0.97 thf(zip_derived_cl392, plain,
% 0.54/0.97 (![X0 : $i]:
% 0.54/0.97 ( (subset @ sk__12 @ X0)
% 0.54/0.97 | (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @
% 0.54/0.97 (relation_inverse_image @ sk__13 @ sk__12)))),
% 0.54/0.97 inference('eq_res', [status(thm)], [zip_derived_cl389])).
% 0.54/0.97 thf(zip_derived_cl152, plain,
% 0.54/0.97 (![X0 : $i]:
% 0.54/0.97 ( (subset @ sk__12 @ X0)
% 0.54/0.97 | (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @
% 0.54/0.97 (relation_dom @ sk__13)))),
% 0.54/0.97 inference('simplify', [status(thm)], [zip_derived_cl151])).
% 0.54/0.97 thf(d12_funct_1, axiom,
% 0.54/0.97 (![A:$i]:
% 0.54/0.97 ( ( ( function @ A ) & ( relation @ A ) ) =>
% 0.54/0.97 ( ![B:$i,C:$i]:
% 0.54/0.97 ( ( ( C ) = ( relation_image @ A @ B ) ) <=>
% 0.54/0.97 ( ![D:$i]:
% 0.54/0.97 ( ( in @ D @ C ) <=>
% 0.54/0.97 ( ?[E:$i]:
% 0.54/0.97 ( ( in @ E @ ( relation_dom @ A ) ) & ( in @ E @ B ) &
% 0.54/0.97 ( ( D ) = ( apply @ A @ E ) ) ) ) ) ) ) ) ))).
% 0.54/0.97 thf(zf_stmt_1, axiom,
% 0.54/0.97 (![E:$i,D:$i,B:$i,A:$i]:
% 0.54/0.97 ( ( zip_tseitin_0 @ E @ D @ B @ A ) <=>
% 0.54/0.97 ( ( ( D ) = ( apply @ A @ E ) ) & ( in @ E @ B ) &
% 0.54/0.97 ( in @ E @ ( relation_dom @ A ) ) ) ))).
% 0.54/0.97 thf(zip_derived_cl8, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.54/0.97 ( (zip_tseitin_0 @ X0 @ X1 @ X2 @ X3)
% 0.54/0.97 | ~ (in @ X0 @ (relation_dom @ X3))
% 0.54/0.97 | ~ (in @ X0 @ X2)
% 0.54/0.97 | ((X1) != (apply @ X3 @ X0)))),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.54/0.97 thf(zf_stmt_2, type, zip_tseitin_0 : $i > $i > $i > $i > $o).
% 0.54/0.97 thf(zf_stmt_3, axiom,
% 0.54/0.97 (![A:$i]:
% 0.54/0.97 ( ( ( relation @ A ) & ( function @ A ) ) =>
% 0.54/0.97 ( ![B:$i,C:$i]:
% 0.54/0.97 ( ( ( C ) = ( relation_image @ A @ B ) ) <=>
% 0.54/0.97 ( ![D:$i]:
% 0.54/0.97 ( ( in @ D @ C ) <=>
% 0.54/0.97 ( ?[E:$i]: ( zip_tseitin_0 @ E @ D @ B @ A ) ) ) ) ) ) ))).
% 0.54/0.97 thf(zip_derived_cl12, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 0.54/0.97 (((X2) != (relation_image @ X0 @ X1))
% 0.54/0.97 | (in @ X3 @ X2)
% 0.54/0.97 | ~ (zip_tseitin_0 @ X4 @ X3 @ X1 @ X0)
% 0.54/0.97 | ~ (function @ X0)
% 0.54/0.97 | ~ (relation @ X0))),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.54/0.97 thf(zip_derived_cl111, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 0.54/0.97 (((X2) != (apply @ X0 @ X3))
% 0.54/0.97 | ~ (in @ X3 @ X1)
% 0.54/0.97 | ~ (in @ X3 @ (relation_dom @ X0))
% 0.54/0.97 | ~ (relation @ X0)
% 0.54/0.97 | ~ (function @ X0)
% 0.54/0.97 | (in @ X2 @ X4)
% 0.54/0.97 | ((X4) != (relation_image @ X0 @ X1)))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl8, zip_derived_cl12])).
% 0.54/0.97 thf(zip_derived_cl157, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.54/0.97 ( (subset @ sk__12 @ X0)
% 0.54/0.97 | ((X1) != (relation_image @ sk__13 @ X2))
% 0.54/0.97 | (in @ X3 @ X1)
% 0.54/0.97 | ~ (function @ sk__13)
% 0.54/0.97 | ~ (relation @ sk__13)
% 0.54/0.97 | ~ (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @ X2)
% 0.54/0.97 | ((X3)
% 0.54/0.97 != (apply @ sk__13 @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13))))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl152, zip_derived_cl111])).
% 0.54/0.97 thf(zip_derived_cl45, plain, ( (function @ sk__13)),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.54/0.97 thf(zip_derived_cl44, plain, ( (relation @ sk__13)),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.54/0.97 thf(zip_derived_cl159, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.54/0.97 ( (subset @ sk__12 @ X0)
% 0.54/0.97 | ((X1) != (relation_image @ sk__13 @ X2))
% 0.54/0.97 | (in @ X3 @ X1)
% 0.54/0.97 | ~ (in @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13) @ X2)
% 0.54/0.97 | ((X3)
% 0.54/0.97 != (apply @ sk__13 @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13))))),
% 0.54/0.97 inference('demod', [status(thm)],
% 0.54/0.97 [zip_derived_cl157, zip_derived_cl45, zip_derived_cl44])).
% 0.54/0.97 thf(zip_derived_cl402, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.97 ( (subset @ sk__12 @ X0)
% 0.54/0.97 | ((X1)
% 0.54/0.97 != (apply @ sk__13 @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13)))
% 0.54/0.97 | (in @ X1 @ X2)
% 0.54/0.97 | ((X2)
% 0.54/0.97 != (relation_image @ sk__13 @
% 0.54/0.97 (relation_inverse_image @ sk__13 @ sk__12)))
% 0.54/0.97 | (subset @ sk__12 @ X0))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl392, zip_derived_cl159])).
% 0.54/0.97 thf(zip_derived_cl407, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.97 (((X2)
% 0.54/0.97 != (relation_image @ sk__13 @
% 0.54/0.97 (relation_inverse_image @ sk__13 @ sk__12)))
% 0.54/0.97 | (in @ X1 @ X2)
% 0.54/0.97 | ((X1)
% 0.54/0.97 != (apply @ sk__13 @ (sk__7 @ (sk__4 @ X0 @ sk__12) @ sk__13)))
% 0.54/0.97 | (subset @ sk__12 @ X0))),
% 0.54/0.97 inference('simplify', [status(thm)], [zip_derived_cl402])).
% 0.54/0.97 thf(zip_derived_cl441, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.97 (((X1) != (sk__4 @ X0 @ sk__12))
% 0.54/0.97 | (subset @ sk__12 @ X0)
% 0.54/0.97 | (subset @ sk__12 @ X0)
% 0.54/0.97 | (in @ X1 @ X2)
% 0.54/0.97 | ((X2)
% 0.54/0.97 != (relation_image @ sk__13 @
% 0.54/0.97 (relation_inverse_image @ sk__13 @ sk__12))))),
% 0.54/0.97 inference('sup-', [status(thm)], [zip_derived_cl232, zip_derived_cl407])).
% 0.54/0.97 thf(zip_derived_cl443, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.97 (((X2)
% 0.54/0.97 != (relation_image @ sk__13 @
% 0.54/0.97 (relation_inverse_image @ sk__13 @ sk__12)))
% 0.54/0.97 | (in @ X1 @ X2)
% 0.54/0.97 | (subset @ sk__12 @ X0)
% 0.54/0.97 | ((X1) != (sk__4 @ X0 @ sk__12)))),
% 0.54/0.97 inference('simplify', [status(thm)], [zip_derived_cl441])).
% 0.54/0.97 thf(zip_derived_cl444, plain,
% 0.54/0.97 (![X0 : $i, X1 : $i]:
% 0.54/0.97 (((X0) != (sk__4 @ X1 @ sk__12))
% 0.54/0.97 | (subset @ sk__12 @ X1)
% 0.54/0.97 | (in @ X0 @
% 0.54/0.97 (relation_image @ sk__13 @
% 0.54/0.97 (relation_inverse_image @ sk__13 @ sk__12))))),
% 0.54/0.97 inference('eq_res', [status(thm)], [zip_derived_cl443])).
% 0.54/0.97 thf(zip_derived_cl447, plain,
% 0.54/0.97 (![X0 : $i]:
% 0.54/0.97 ( (in @ (sk__4 @ X0 @ sk__12) @
% 0.54/0.97 (relation_image @ sk__13 @
% 0.54/0.97 (relation_inverse_image @ sk__13 @ sk__12)))
% 0.54/0.97 | (subset @ sk__12 @ X0))),
% 0.54/0.97 inference('eq_res', [status(thm)], [zip_derived_cl444])).
% 0.54/0.97 thf(zip_derived_cl458, plain,
% 0.54/0.97 (( (subset @ sk__12 @
% 0.54/0.97 (relation_image @ sk__13 @ (relation_inverse_image @ sk__13 @ sk__12)))
% 0.54/0.97 | (subset @ sk__12 @
% 0.54/0.97 (relation_image @ sk__13 @
% 0.54/0.97 (relation_inverse_image @ sk__13 @ sk__12))))),
% 0.54/0.97 inference('sup+', [status(thm)], [zip_derived_cl20, zip_derived_cl447])).
% 0.54/0.97 thf(zip_derived_cl459, plain,
% 0.54/0.97 ( (subset @ sk__12 @
% 0.54/0.97 (relation_image @ sk__13 @ (relation_inverse_image @ sk__13 @ sk__12)))),
% 0.54/0.97 inference('simplify', [status(thm)], [zip_derived_cl458])).
% 0.54/0.97 thf(zip_derived_cl465, plain,
% 0.54/0.97 ((((sk__12)
% 0.54/0.97 = (relation_image @ sk__13 @
% 0.54/0.97 (relation_inverse_image @ sk__13 @ sk__12)))
% 0.54/0.97 | ~ (function @ sk__13)
% 0.54/0.97 | ~ (relation @ sk__13))),
% 0.54/0.97 inference('sup+', [status(thm)], [zip_derived_cl88, zip_derived_cl459])).
% 0.54/0.97 thf(zip_derived_cl45, plain, ( (function @ sk__13)),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.54/0.97 thf(zip_derived_cl44, plain, ( (relation @ sk__13)),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.54/0.97 thf(zip_derived_cl466, plain,
% 0.54/0.97 (((sk__12)
% 0.54/0.97 = (relation_image @ sk__13 @
% 0.54/0.97 (relation_inverse_image @ sk__13 @ sk__12)))),
% 0.54/0.97 inference('demod', [status(thm)],
% 0.54/0.97 [zip_derived_cl465, zip_derived_cl45, zip_derived_cl44])).
% 0.54/0.97 thf(zip_derived_cl46, plain,
% 0.54/0.97 (((relation_image @ sk__13 @ (relation_inverse_image @ sk__13 @ sk__12))
% 0.54/0.97 != (sk__12))),
% 0.54/0.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.54/0.97 thf(zip_derived_cl467, plain, ($false),
% 0.54/0.97 inference('simplify_reflect-', [status(thm)],
% 0.54/0.97 [zip_derived_cl466, zip_derived_cl46])).
% 0.54/0.97
% 0.54/0.97 % SZS output end Refutation
% 0.54/0.97
% 0.54/0.97
% 0.54/0.97 % Terminating...
% 1.61/1.10 % Runner terminated.
% 1.61/1.12 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------