%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : MGT042-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.ZgvcvE8kQq true
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:25:14 AM UTC 2026
% Result : Unsatisfiable 0.43s 1.03s
% Output : Refutation 0.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT042-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.04 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.ZgvcvE8kQq true
% 0.10/0.36 % Computer : n028.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 7 13:07:47 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Running portfolio for 300 s
% 0.10/0.36 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Number of cores: 8
% 0.10/0.37 % Python version: Python 3.12.3
% 0.10/0.37 % Running in FO mode
% 0.38/0.58 % Total configuration time : 435
% 0.38/0.58 % Estimated wc time : 1092
% 0.38/0.58 % Estimated cpu time (7 cpus) : 156.0
% 0.40/0.65 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.40/0.72 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.40/0.72 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.40/0.72 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.40/0.72 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.40/0.72 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.40/0.72 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.43/1.03 % Solved by fo/fo3_bce.sh.
% 0.43/1.03 % BCE start: 38
% 0.43/1.03 % BCE eliminated: 0
% 0.43/1.03 % PE start: 38
% 0.43/1.03 logic: eq
% 0.43/1.03 % PE eliminated: -12
% 0.43/1.03 % done 301 iterations in 0.270s
% 0.43/1.03 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.43/1.03 % SZS output start Refutation
% 0.43/1.03 thf(greater_or_equal_type, type, greater_or_equal: $i > $i > $o).
% 0.43/1.03 thf(sk2_type, type, sk2: $i).
% 0.43/1.03 thf(smaller_type, type, smaller: $i > $i > $o).
% 0.43/1.03 thf(sk1_type, type, sk1: $i).
% 0.43/1.03 thf(has_immunity_type, type, has_immunity: $i > $i > $o).
% 0.43/1.03 thf(hazard_of_mortality_type, type, hazard_of_mortality: $i > $i > $i).
% 0.43/1.03 thf(organization_type, type, organization: $i > $o).
% 0.43/1.03 thf(capability_type, type, capability: $i > $i > $i).
% 0.43/1.03 thf(sk3_type, type, sk3: $i).
% 0.43/1.03 thf(smaller_or_equal_type, type, smaller_or_equal: $i > $i > $o).
% 0.43/1.03 thf(internal_friction_type, type, internal_friction: $i > $i > $i).
% 0.43/1.03 thf(position_type, type, position: $i > $i > $i).
% 0.43/1.03 thf(external_ties_type, type, external_ties: $i > $i > $i).
% 0.43/1.03 thf(greater_type, type, greater: $i > $i > $o).
% 0.43/1.03 thf(stock_of_knowledge_type, type, stock_of_knowledge: $i > $i > $i).
% 0.43/1.03 thf(definition_greater_or_equal_6, axiom,
% 0.43/1.03 (( ( A ) != ( B ) ) | ( greater_or_equal @ A @ B ))).
% 0.43/1.03 thf(zip_derived_cl5, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]: (((X1) != (X0)) | (greater_or_equal @ X1 @ X0))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_greater_or_equal_6])).
% 0.43/1.03 thf(lemma_1_51, conjecture,
% 0.43/1.03 (~( ( greater @
% 0.43/1.03 ( external_ties @ sk1 @ sk3 ) @ ( external_ties @ sk1 @ sk2 ) ) |
% 0.43/1.03 ( greater @
% 0.43/1.03 ( stock_of_knowledge @ sk1 @ sk3 ) @
% 0.43/1.03 ( stock_of_knowledge @ sk1 @ sk2 ) ) ))).
% 0.43/1.03 thf(zf_stmt_0, negated_conjecture,
% 0.43/1.03 (( greater @ ( external_ties @ sk1 @ sk3 ) @ ( external_ties @ sk1 @ sk2 ) ) |
% 0.43/1.03 ( greater @
% 0.43/1.03 ( stock_of_knowledge @ sk1 @ sk3 ) @ ( stock_of_knowledge @ sk1 @ sk2 ) )),
% 0.43/1.03 inference('cnf.neg', [status(esa)], [lemma_1_51])).
% 0.43/1.03 thf(zip_derived_cl24, plain,
% 0.43/1.03 (( (greater @ (external_ties @ sk1 @ sk3) @ (external_ties @ sk1 @ sk2))
% 0.43/1.03 | (greater @ (stock_of_knowledge @ sk1 @ sk3) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ sk2)))),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.43/1.03 thf(lemma_1_46, conjecture, (~( organization @ sk1 ))).
% 0.43/1.03 thf(zf_stmt_1, negated_conjecture, (organization @ sk1),
% 0.43/1.03 inference('cnf.neg', [status(esa)], [lemma_1_46])).
% 0.43/1.03 thf(zip_derived_cl19, plain, ( (organization @ sk1)),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.43/1.03 thf(assumption_6_44, axiom,
% 0.43/1.03 (( ~( organization @ A ) ) |
% 0.43/1.03 ( ~( greater @ ( external_ties @ A @ B ) @ ( external_ties @ A @ C ) ) ) |
% 0.43/1.03 ( greater @ ( position @ A @ B ) @ ( position @ A @ C ) ))).
% 0.43/1.03 thf(zip_derived_cl17, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.43/1.03 (~ (organization @ X0)
% 0.43/1.03 | ~ (greater @ (external_ties @ X0 @ X1) @ (external_ties @ X0 @ X2))
% 0.43/1.03 | (greater @ (position @ X0 @ X1) @ (position @ X0 @ X2)))),
% 0.43/1.03 inference('cnf', [status(esa)], [assumption_6_44])).
% 0.43/1.03 thf(zip_derived_cl212, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 ( (greater @ (position @ sk1 @ X1) @ (position @ sk1 @ X0))
% 0.43/1.03 | ~ (greater @ (external_ties @ sk1 @ X1) @
% 0.43/1.03 (external_ties @ sk1 @ X0)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl19, zip_derived_cl17])).
% 0.43/1.03 thf(zip_derived_cl314, plain,
% 0.43/1.03 (( (greater @ (stock_of_knowledge @ sk1 @ sk3) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ sk2))
% 0.43/1.03 | (greater @ (position @ sk1 @ sk3) @ (position @ sk1 @ sk2)))),
% 0.43/1.03 inference('sup-', [status(thm)], [zip_derived_cl24, zip_derived_cl212])).
% 0.43/1.03 thf(definition_greater_or_equal_4, axiom,
% 0.43/1.03 (( ~( greater_or_equal @ A @ B ) ) | ( greater @ A @ B ) |
% 0.43/1.03 ( ( A ) = ( B ) ))).
% 0.43/1.03 thf(zip_derived_cl3, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (~ (greater_or_equal @ X0 @ X1) | (greater @ X0 @ X1) | ((X0) = (X1)))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_greater_or_equal_4])).
% 0.43/1.03 thf(lemma_1_54, conjecture,
% 0.43/1.03 (~( smaller_or_equal @
% 0.43/1.03 ( internal_friction @ sk1 @ sk3 ) @ ( internal_friction @ sk1 @ sk2 ) ))).
% 0.43/1.03 thf(zf_stmt_2, negated_conjecture,
% 0.43/1.03 (smaller_or_equal @
% 0.43/1.03 ( internal_friction @ sk1 @ sk3 ) @ ( internal_friction @ sk1 @ sk2 )),
% 0.43/1.03 inference('cnf.neg', [status(esa)], [lemma_1_54])).
% 0.43/1.03 thf(zip_derived_cl27, plain,
% 0.43/1.03 ( (smaller_or_equal @ (internal_friction @ sk1 @ sk3) @
% 0.43/1.03 (internal_friction @ sk1 @ sk2))),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.43/1.03 thf(definition_smaller_or_equal_1, axiom,
% 0.43/1.03 (( ~( smaller_or_equal @ A @ B ) ) | ( smaller @ A @ B ) |
% 0.43/1.03 ( ( A ) = ( B ) ))).
% 0.43/1.03 thf(zip_derived_cl0, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (~ (smaller_or_equal @ X0 @ X1) | (smaller @ X0 @ X1) | ((X0) = (X1)))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_smaller_or_equal_1])).
% 0.43/1.03 thf(zip_derived_cl234, plain,
% 0.43/1.03 ((((internal_friction @ sk1 @ sk3) = (internal_friction @ sk1 @ sk2))
% 0.43/1.03 | (smaller @ (internal_friction @ sk1 @ sk3) @
% 0.43/1.03 (internal_friction @ sk1 @ sk2)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl27, zip_derived_cl0])).
% 0.43/1.03 thf(definition_smaller_or_equal_2, axiom,
% 0.43/1.03 (( ~( smaller @ A @ B ) ) | ( smaller_or_equal @ A @ B ))).
% 0.43/1.03 thf(zip_derived_cl1, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (~ (smaller @ X0 @ X1) | (smaller_or_equal @ X0 @ X1))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_smaller_or_equal_2])).
% 0.43/1.03 thf(zip_derived_cl19, plain, ( (organization @ sk1)),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.43/1.03 thf(assumption_5_41, axiom,
% 0.43/1.03 (( ~( organization @ A ) ) |
% 0.43/1.03 ( ~( greater @
% 0.43/1.03 ( stock_of_knowledge @ A @ B ) @ ( stock_of_knowledge @ A @ C ) ) ) |
% 0.43/1.03 ( ~( smaller_or_equal @
% 0.43/1.03 ( internal_friction @ A @ B ) @ ( internal_friction @ A @ C ) ) ) |
% 0.43/1.03 ( greater @ ( capability @ A @ B ) @ ( capability @ A @ C ) ))).
% 0.43/1.03 thf(zip_derived_cl14, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.43/1.03 (~ (organization @ X0)
% 0.43/1.03 | ~ (greater @ (stock_of_knowledge @ X0 @ X1) @
% 0.43/1.03 (stock_of_knowledge @ X0 @ X2))
% 0.43/1.03 | ~ (smaller_or_equal @ (internal_friction @ X0 @ X1) @
% 0.43/1.03 (internal_friction @ X0 @ X2))
% 0.43/1.03 | (greater @ (capability @ X0 @ X1) @ (capability @ X0 @ X2)))),
% 0.43/1.03 inference('cnf', [status(esa)], [assumption_5_41])).
% 0.43/1.03 thf(zip_derived_cl209, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 ( (greater @ (capability @ sk1 @ X1) @ (capability @ sk1 @ X0))
% 0.43/1.03 | ~ (smaller_or_equal @ (internal_friction @ sk1 @ X1) @
% 0.43/1.03 (internal_friction @ sk1 @ X0))
% 0.43/1.03 | ~ (greater @ (stock_of_knowledge @ sk1 @ X1) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ X0)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl19, zip_derived_cl14])).
% 0.43/1.03 thf(zip_derived_cl215, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (~ (smaller @ (internal_friction @ sk1 @ X1) @
% 0.43/1.03 (internal_friction @ sk1 @ X0))
% 0.43/1.03 | ~ (greater @ (stock_of_knowledge @ sk1 @ X1) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ X0))
% 0.43/1.03 | (greater @ (capability @ sk1 @ X1) @ (capability @ sk1 @ X0)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl1, zip_derived_cl209])).
% 0.43/1.03 thf(zip_derived_cl372, plain,
% 0.43/1.03 ((((internal_friction @ sk1 @ sk3) = (internal_friction @ sk1 @ sk2))
% 0.43/1.03 | (greater @ (capability @ sk1 @ sk3) @ (capability @ sk1 @ sk2))
% 0.43/1.03 | ~ (greater @ (stock_of_knowledge @ sk1 @ sk3) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ sk2)))),
% 0.43/1.03 inference('sup-', [status(thm)], [zip_derived_cl234, zip_derived_cl215])).
% 0.43/1.03 thf(definition_smaller_or_equal_3, axiom,
% 0.43/1.03 (( ( A ) != ( B ) ) | ( smaller_or_equal @ A @ B ))).
% 0.43/1.03 thf(zip_derived_cl2, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]: (((X1) != (X0)) | (smaller_or_equal @ X1 @ X0))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_smaller_or_equal_3])).
% 0.43/1.03 thf(zip_derived_cl209, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 ( (greater @ (capability @ sk1 @ X1) @ (capability @ sk1 @ X0))
% 0.43/1.03 | ~ (smaller_or_equal @ (internal_friction @ sk1 @ X1) @
% 0.43/1.03 (internal_friction @ sk1 @ X0))
% 0.43/1.03 | ~ (greater @ (stock_of_knowledge @ sk1 @ X1) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ X0)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl19, zip_derived_cl14])).
% 0.43/1.03 thf(zip_derived_cl218, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (((internal_friction @ sk1 @ X0) != (internal_friction @ sk1 @ X1))
% 0.43/1.03 | ~ (greater @ (stock_of_knowledge @ sk1 @ X0) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ X1))
% 0.43/1.03 | (greater @ (capability @ sk1 @ X0) @ (capability @ sk1 @ X1)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl2, zip_derived_cl209])).
% 0.43/1.03 thf(zip_derived_cl548, plain,
% 0.43/1.03 ((~ (greater @ (stock_of_knowledge @ sk1 @ sk3) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ sk2))
% 0.43/1.03 | (greater @ (capability @ sk1 @ sk3) @ (capability @ sk1 @ sk2)))),
% 0.43/1.03 inference('clc', [status(thm)], [zip_derived_cl372, zip_derived_cl218])).
% 0.43/1.03 thf(zip_derived_cl553, plain,
% 0.43/1.03 ((((stock_of_knowledge @ sk1 @ sk3) = (stock_of_knowledge @ sk1 @ sk2))
% 0.43/1.03 | ~ (greater_or_equal @ (stock_of_knowledge @ sk1 @ sk3) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ sk2))
% 0.43/1.03 | (greater @ (capability @ sk1 @ sk3) @ (capability @ sk1 @ sk2)))),
% 0.43/1.03 inference('sup-', [status(thm)], [zip_derived_cl3, zip_derived_cl548])).
% 0.43/1.03 thf(lemma_1_49, conjecture,
% 0.43/1.03 (~( ( greater_or_equal @
% 0.43/1.03 ( stock_of_knowledge @ sk1 @ sk3 ) @
% 0.43/1.03 ( stock_of_knowledge @ sk1 @ sk2 ) ) |
% 0.43/1.03 ( greater @
% 0.43/1.03 ( stock_of_knowledge @ sk1 @ sk3 ) @
% 0.43/1.03 ( stock_of_knowledge @ sk1 @ sk2 ) ) ))).
% 0.43/1.03 thf(zf_stmt_3, negated_conjecture,
% 0.43/1.03 (( greater_or_equal @
% 0.43/1.03 ( stock_of_knowledge @ sk1 @ sk3 ) @ ( stock_of_knowledge @ sk1 @ sk2 ) ) |
% 0.43/1.03 ( greater @
% 0.43/1.03 ( stock_of_knowledge @ sk1 @ sk3 ) @ ( stock_of_knowledge @ sk1 @ sk2 ) )),
% 0.43/1.03 inference('cnf.neg', [status(esa)], [lemma_1_49])).
% 0.43/1.03 thf(zip_derived_cl22, plain,
% 0.43/1.03 (( (greater_or_equal @ (stock_of_knowledge @ sk1 @ sk3) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ sk2))
% 0.43/1.03 | (greater @ (stock_of_knowledge @ sk1 @ sk3) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ sk2)))),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.43/1.03 thf(definition_greater_or_equal_5, axiom,
% 0.43/1.03 (( ~( greater @ A @ B ) ) | ( greater_or_equal @ A @ B ))).
% 0.43/1.03 thf(zip_derived_cl4, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (~ (greater @ X0 @ X1) | (greater_or_equal @ X0 @ X1))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_greater_or_equal_5])).
% 0.43/1.03 thf(zip_derived_cl309, plain,
% 0.43/1.03 ( (greater_or_equal @ (stock_of_knowledge @ sk1 @ sk3) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ sk2))),
% 0.43/1.03 inference('clc', [status(thm)], [zip_derived_cl22, zip_derived_cl4])).
% 0.43/1.03 thf(zip_derived_cl557, plain,
% 0.43/1.03 ((((stock_of_knowledge @ sk1 @ sk3) = (stock_of_knowledge @ sk1 @ sk2))
% 0.43/1.03 | (greater @ (capability @ sk1 @ sk3) @ (capability @ sk1 @ sk2)))),
% 0.43/1.03 inference('demod', [status(thm)], [zip_derived_cl553, zip_derived_cl309])).
% 0.43/1.03 thf(definition_smaller_8, axiom,
% 0.43/1.03 (( ~( greater @ A @ B ) ) | ( smaller @ B @ A ))).
% 0.43/1.03 thf(zip_derived_cl7, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]: (~ (greater @ X0 @ X1) | (smaller @ X1 @ X0))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_smaller_8])).
% 0.43/1.03 thf(zip_derived_cl3, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (~ (greater_or_equal @ X0 @ X1) | (greater @ X0 @ X1) | ((X0) = (X1)))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_greater_or_equal_4])).
% 0.43/1.03 thf(zip_derived_cl274, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 ( (smaller @ X0 @ X1) | ((X1) = (X0)) | ~ (greater_or_equal @ X1 @ X0))),
% 0.43/1.03 inference('sup+', [status(thm)], [zip_derived_cl7, zip_derived_cl3])).
% 0.43/1.03 thf(lemma_1_57, conjecture,
% 0.43/1.03 (~( ( greater @
% 0.43/1.03 ( external_ties @ sk1 @ sk3 ) @ ( external_ties @ sk1 @ sk2 ) ) |
% 0.43/1.03 ( greater_or_equal @
% 0.43/1.03 ( external_ties @ sk1 @ sk3 ) @ ( external_ties @ sk1 @ sk2 ) ) ))).
% 0.43/1.03 thf(zf_stmt_4, negated_conjecture,
% 0.43/1.03 (( greater @ ( external_ties @ sk1 @ sk3 ) @ ( external_ties @ sk1 @ sk2 ) ) |
% 0.43/1.03 ( greater_or_equal @
% 0.43/1.03 ( external_ties @ sk1 @ sk3 ) @ ( external_ties @ sk1 @ sk2 ) )),
% 0.43/1.03 inference('cnf.neg', [status(esa)], [lemma_1_57])).
% 0.43/1.03 thf(zip_derived_cl30, plain,
% 0.43/1.03 (( (greater @ (external_ties @ sk1 @ sk3) @ (external_ties @ sk1 @ sk2))
% 0.43/1.03 | (greater_or_equal @ (external_ties @ sk1 @ sk3) @
% 0.43/1.03 (external_ties @ sk1 @ sk2)))),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.43/1.03 thf(zip_derived_cl4, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (~ (greater @ X0 @ X1) | (greater_or_equal @ X0 @ X1))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_greater_or_equal_5])).
% 0.43/1.03 thf(zip_derived_cl328, plain,
% 0.43/1.03 ( (greater_or_equal @ (external_ties @ sk1 @ sk3) @
% 0.43/1.03 (external_ties @ sk1 @ sk2))),
% 0.43/1.03 inference('clc', [status(thm)], [zip_derived_cl30, zip_derived_cl4])).
% 0.43/1.03 thf(zip_derived_cl367, plain,
% 0.43/1.03 ((((external_ties @ sk1 @ sk3) = (external_ties @ sk1 @ sk2))
% 0.43/1.03 | (smaller @ (external_ties @ sk1 @ sk2) @ (external_ties @ sk1 @ sk3)))),
% 0.43/1.03 inference('sup+', [status(thm)], [zip_derived_cl274, zip_derived_cl328])).
% 0.43/1.03 thf(zip_derived_cl212, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 ( (greater @ (position @ sk1 @ X1) @ (position @ sk1 @ X0))
% 0.43/1.03 | ~ (greater @ (external_ties @ sk1 @ X1) @
% 0.43/1.03 (external_ties @ sk1 @ X0)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl19, zip_derived_cl17])).
% 0.43/1.03 thf(definition_smaller_7, axiom,
% 0.43/1.03 (( ~( smaller @ A @ B ) ) | ( greater @ B @ A ))).
% 0.43/1.03 thf(zip_derived_cl6, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]: (~ (smaller @ X0 @ X1) | (greater @ X1 @ X0))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_smaller_7])).
% 0.43/1.03 thf(zip_derived_cl301, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 ( (greater @ (position @ sk1 @ X1) @ (position @ sk1 @ X0))
% 0.43/1.03 | ~ (smaller @ (external_ties @ sk1 @ X0) @
% 0.43/1.03 (external_ties @ sk1 @ X1)))),
% 0.43/1.03 inference('sup+', [status(thm)], [zip_derived_cl212, zip_derived_cl6])).
% 0.43/1.03 thf(zip_derived_cl381, plain,
% 0.43/1.03 ((((external_ties @ sk1 @ sk3) = (external_ties @ sk1 @ sk2))
% 0.43/1.03 | (greater @ (position @ sk1 @ sk3) @ (position @ sk1 @ sk2)))),
% 0.43/1.03 inference('sup-', [status(thm)], [zip_derived_cl367, zip_derived_cl301])).
% 0.43/1.03 thf(zip_derived_cl19, plain, ( (organization @ sk1)),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.43/1.03 thf(assumption_6_45, axiom,
% 0.43/1.03 (( ~( organization @ A ) ) |
% 0.43/1.03 ( ( external_ties @ A @ B ) != ( external_ties @ A @ C ) ) |
% 0.43/1.03 ( ( position @ A @ B ) = ( position @ A @ C ) ))).
% 0.43/1.03 thf(zip_derived_cl18, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.43/1.03 (~ (organization @ X0)
% 0.43/1.03 | ((external_ties @ X0 @ X2) != (external_ties @ X0 @ X1))
% 0.43/1.03 | ((position @ X0 @ X2) = (position @ X0 @ X1)))),
% 0.43/1.03 inference('cnf', [status(esa)], [assumption_6_45])).
% 0.43/1.03 thf(zip_derived_cl213, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (((position @ sk1 @ X0) = (position @ sk1 @ X1))
% 0.43/1.03 | ((external_ties @ sk1 @ X0) != (external_ties @ sk1 @ X1)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl19, zip_derived_cl18])).
% 0.43/1.03 thf(zip_derived_cl385, plain,
% 0.43/1.03 (![X0 : $i]:
% 0.43/1.03 (((external_ties @ sk1 @ sk2) != (external_ties @ sk1 @ X0))
% 0.43/1.03 | (greater @ (position @ sk1 @ sk3) @ (position @ sk1 @ sk2))
% 0.43/1.03 | ((position @ sk1 @ sk3) = (position @ sk1 @ X0)))),
% 0.43/1.03 inference('sup-', [status(thm)], [zip_derived_cl381, zip_derived_cl213])).
% 0.43/1.03 thf(zip_derived_cl767, plain,
% 0.43/1.03 ((((position @ sk1 @ sk3) = (position @ sk1 @ sk2))
% 0.43/1.03 | (greater @ (position @ sk1 @ sk3) @ (position @ sk1 @ sk2)))),
% 0.43/1.03 inference('eq_res', [status(thm)], [zip_derived_cl385])).
% 0.43/1.03 thf(zip_derived_cl4, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (~ (greater @ X0 @ X1) | (greater_or_equal @ X0 @ X1))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_greater_or_equal_5])).
% 0.43/1.03 thf(zip_derived_cl776, plain,
% 0.43/1.03 ((((position @ sk1 @ sk3) = (position @ sk1 @ sk2))
% 0.43/1.03 | (greater_or_equal @ (position @ sk1 @ sk3) @ (position @ sk1 @ sk2)))),
% 0.43/1.03 inference('sup-', [status(thm)], [zip_derived_cl767, zip_derived_cl4])).
% 0.43/1.03 thf(zip_derived_cl5, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]: (((X1) != (X0)) | (greater_or_equal @ X1 @ X0))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_greater_or_equal_6])).
% 0.43/1.03 thf(zip_derived_cl800, plain,
% 0.43/1.03 ( (greater_or_equal @ (position @ sk1 @ sk3) @ (position @ sk1 @ sk2))),
% 0.43/1.03 inference('clc', [status(thm)], [zip_derived_cl776, zip_derived_cl5])).
% 0.43/1.03 thf(zip_derived_cl19, plain, ( (organization @ sk1)),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.43/1.03 thf(assumption_4_38, axiom,
% 0.43/1.03 (( ~( organization @ A ) ) | ( has_immunity @ A @ B ) |
% 0.43/1.03 ( has_immunity @ A @ C ) |
% 0.43/1.03 ( ~( greater @ ( capability @ A @ C ) @ ( capability @ A @ B ) ) ) |
% 0.43/1.03 ( ~( greater_or_equal @ ( position @ A @ C ) @ ( position @ A @ B ) ) ) |
% 0.43/1.03 ( smaller @
% 0.43/1.03 ( hazard_of_mortality @ A @ C ) @ ( hazard_of_mortality @ A @ B ) ))).
% 0.43/1.03 thf(zip_derived_cl11, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.43/1.03 (~ (organization @ X0)
% 0.43/1.03 | (has_immunity @ X0 @ X1)
% 0.43/1.03 | (has_immunity @ X0 @ X2)
% 0.43/1.03 | ~ (greater @ (capability @ X0 @ X2) @ (capability @ X0 @ X1))
% 0.43/1.03 | ~ (greater_or_equal @ (position @ X0 @ X2) @ (position @ X0 @ X1))
% 0.43/1.03 | (smaller @ (hazard_of_mortality @ X0 @ X2) @
% 0.43/1.03 (hazard_of_mortality @ X0 @ X1)))),
% 0.43/1.03 inference('cnf', [status(esa)], [assumption_4_38])).
% 0.43/1.03 thf(zip_derived_cl206, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 ( (smaller @ (hazard_of_mortality @ sk1 @ X1) @
% 0.43/1.03 (hazard_of_mortality @ sk1 @ X0))
% 0.43/1.03 | ~ (greater_or_equal @ (position @ sk1 @ X1) @ (position @ sk1 @ X0))
% 0.43/1.03 | ~ (greater @ (capability @ sk1 @ X1) @ (capability @ sk1 @ X0))
% 0.43/1.03 | (has_immunity @ sk1 @ X1)
% 0.43/1.03 | (has_immunity @ sk1 @ X0))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl19, zip_derived_cl11])).
% 0.43/1.03 thf(zip_derived_cl804, plain,
% 0.43/1.03 (( (has_immunity @ sk1 @ sk2)
% 0.43/1.03 | (has_immunity @ sk1 @ sk3)
% 0.43/1.03 | ~ (greater @ (capability @ sk1 @ sk3) @ (capability @ sk1 @ sk2))
% 0.43/1.03 | (smaller @ (hazard_of_mortality @ sk1 @ sk3) @
% 0.43/1.03 (hazard_of_mortality @ sk1 @ sk2)))),
% 0.43/1.03 inference('sup-', [status(thm)], [zip_derived_cl800, zip_derived_cl206])).
% 0.43/1.03 thf(lemma_1_47, conjecture, (has_immunity @ sk1 @ sk2)).
% 0.43/1.03 thf(zf_stmt_5, negated_conjecture, (~( has_immunity @ sk1 @ sk2 )),
% 0.43/1.03 inference('cnf.neg', [status(esa)], [lemma_1_47])).
% 0.43/1.03 thf(zip_derived_cl20, plain, (~ (has_immunity @ sk1 @ sk2)),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.43/1.03 thf(lemma_1_48, conjecture, (has_immunity @ sk1 @ sk3)).
% 0.43/1.03 thf(zf_stmt_6, negated_conjecture, (~( has_immunity @ sk1 @ sk3 )),
% 0.43/1.03 inference('cnf.neg', [status(esa)], [lemma_1_48])).
% 0.43/1.03 thf(zip_derived_cl21, plain, (~ (has_immunity @ sk1 @ sk3)),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.43/1.03 thf(zip_derived_cl807, plain,
% 0.43/1.03 ((~ (greater @ (capability @ sk1 @ sk3) @ (capability @ sk1 @ sk2))
% 0.43/1.03 | (smaller @ (hazard_of_mortality @ sk1 @ sk3) @
% 0.43/1.03 (hazard_of_mortality @ sk1 @ sk2)))),
% 0.43/1.03 inference('demod', [status(thm)],
% 0.43/1.03 [zip_derived_cl804, zip_derived_cl20, zip_derived_cl21])).
% 0.43/1.03 thf(lemma_1_64, conjecture,
% 0.43/1.03 (smaller @
% 0.43/1.03 ( hazard_of_mortality @ sk1 @ sk3 ) @ ( hazard_of_mortality @ sk1 @ sk2 ))).
% 0.43/1.03 thf(zf_stmt_7, negated_conjecture,
% 0.43/1.03 (~( smaller @
% 0.43/1.03 ( hazard_of_mortality @ sk1 @ sk3 ) @
% 0.43/1.03 ( hazard_of_mortality @ sk1 @ sk2 ) )),
% 0.43/1.03 inference('cnf.neg', [status(esa)], [lemma_1_64])).
% 0.43/1.03 thf(zip_derived_cl37, plain,
% 0.43/1.03 (~ (smaller @ (hazard_of_mortality @ sk1 @ sk3) @
% 0.43/1.03 (hazard_of_mortality @ sk1 @ sk2))),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.43/1.03 thf(zip_derived_cl808, plain,
% 0.43/1.03 (~ (greater @ (capability @ sk1 @ sk3) @ (capability @ sk1 @ sk2))),
% 0.43/1.03 inference('clc', [status(thm)], [zip_derived_cl807, zip_derived_cl37])).
% 0.43/1.03 thf(zip_derived_cl811, plain,
% 0.43/1.03 (((stock_of_knowledge @ sk1 @ sk3) = (stock_of_knowledge @ sk1 @ sk2))),
% 0.43/1.03 inference('demod', [status(thm)], [zip_derived_cl557, zip_derived_cl808])).
% 0.43/1.03 thf(meaning_postulate_greater_strict_9, axiom,
% 0.43/1.03 (( ~( greater @ A @ B ) ) | ( ~( greater @ B @ A ) ))).
% 0.43/1.03 thf(zip_derived_cl8, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]: (~ (greater @ X0 @ X1) | ~ (greater @ X1 @ X0))),
% 0.43/1.03 inference('cnf', [status(esa)], [meaning_postulate_greater_strict_9])).
% 0.43/1.03 thf(zip_derived_cl271, plain, (![X0 : $i]: ~ (greater @ X0 @ X0)),
% 0.43/1.03 inference('eq_fact', [status(thm)], [zip_derived_cl8])).
% 0.43/1.03 thf(zip_derived_cl824, plain,
% 0.43/1.03 ( (greater @ (position @ sk1 @ sk3) @ (position @ sk1 @ sk2))),
% 0.43/1.03 inference('demod', [status(thm)],
% 0.43/1.03 [zip_derived_cl314, zip_derived_cl811, zip_derived_cl271])).
% 0.43/1.03 thf(zip_derived_cl19, plain, ( (organization @ sk1)),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.43/1.03 thf(assumption_4_39, axiom,
% 0.43/1.03 (( ~( organization @ A ) ) | ( has_immunity @ A @ B ) |
% 0.43/1.03 ( has_immunity @ A @ C ) |
% 0.43/1.03 ( ~( greater_or_equal @ ( capability @ A @ C ) @ ( capability @ A @ B ) ) ) |
% 0.43/1.03 ( ~( greater @ ( position @ A @ C ) @ ( position @ A @ B ) ) ) |
% 0.43/1.03 ( smaller @
% 0.43/1.03 ( hazard_of_mortality @ A @ C ) @ ( hazard_of_mortality @ A @ B ) ))).
% 0.43/1.03 thf(zip_derived_cl12, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.43/1.03 (~ (organization @ X0)
% 0.43/1.03 | (has_immunity @ X0 @ X1)
% 0.43/1.03 | (has_immunity @ X0 @ X2)
% 0.43/1.03 | ~ (greater_or_equal @ (capability @ X0 @ X2) @
% 0.43/1.03 (capability @ X0 @ X1))
% 0.43/1.03 | ~ (greater @ (position @ X0 @ X2) @ (position @ X0 @ X1))
% 0.43/1.03 | (smaller @ (hazard_of_mortality @ X0 @ X2) @
% 0.43/1.03 (hazard_of_mortality @ X0 @ X1)))),
% 0.43/1.03 inference('cnf', [status(esa)], [assumption_4_39])).
% 0.43/1.03 thf(zip_derived_cl207, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 ( (smaller @ (hazard_of_mortality @ sk1 @ X1) @
% 0.43/1.03 (hazard_of_mortality @ sk1 @ X0))
% 0.43/1.03 | ~ (greater @ (position @ sk1 @ X1) @ (position @ sk1 @ X0))
% 0.43/1.03 | ~ (greater_or_equal @ (capability @ sk1 @ X1) @
% 0.43/1.03 (capability @ sk1 @ X0))
% 0.43/1.03 | (has_immunity @ sk1 @ X1)
% 0.43/1.03 | (has_immunity @ sk1 @ X0))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl19, zip_derived_cl12])).
% 0.43/1.03 thf(zip_derived_cl983, plain,
% 0.43/1.03 (( (has_immunity @ sk1 @ sk2)
% 0.43/1.03 | (has_immunity @ sk1 @ sk3)
% 0.43/1.03 | ~ (greater_or_equal @ (capability @ sk1 @ sk3) @
% 0.43/1.03 (capability @ sk1 @ sk2))
% 0.43/1.03 | (smaller @ (hazard_of_mortality @ sk1 @ sk3) @
% 0.43/1.03 (hazard_of_mortality @ sk1 @ sk2)))),
% 0.43/1.03 inference('sup-', [status(thm)], [zip_derived_cl824, zip_derived_cl207])).
% 0.43/1.03 thf(zip_derived_cl20, plain, (~ (has_immunity @ sk1 @ sk2)),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.43/1.03 thf(zip_derived_cl21, plain, (~ (has_immunity @ sk1 @ sk3)),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.43/1.03 thf(zip_derived_cl988, plain,
% 0.43/1.03 ((~ (greater_or_equal @ (capability @ sk1 @ sk3) @
% 0.43/1.03 (capability @ sk1 @ sk2))
% 0.43/1.03 | (smaller @ (hazard_of_mortality @ sk1 @ sk3) @
% 0.43/1.03 (hazard_of_mortality @ sk1 @ sk2)))),
% 0.43/1.03 inference('demod', [status(thm)],
% 0.43/1.03 [zip_derived_cl983, zip_derived_cl20, zip_derived_cl21])).
% 0.43/1.03 thf(zip_derived_cl274, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 ( (smaller @ X0 @ X1) | ((X1) = (X0)) | ~ (greater_or_equal @ X1 @ X0))),
% 0.43/1.03 inference('sup+', [status(thm)], [zip_derived_cl7, zip_derived_cl3])).
% 0.43/1.03 thf(zip_derived_cl309, plain,
% 0.43/1.03 ( (greater_or_equal @ (stock_of_knowledge @ sk1 @ sk3) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ sk2))),
% 0.43/1.03 inference('clc', [status(thm)], [zip_derived_cl22, zip_derived_cl4])).
% 0.43/1.03 thf(zip_derived_cl366, plain,
% 0.43/1.03 ((((stock_of_knowledge @ sk1 @ sk3) = (stock_of_knowledge @ sk1 @ sk2))
% 0.43/1.03 | (smaller @ (stock_of_knowledge @ sk1 @ sk2) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ sk3)))),
% 0.43/1.03 inference('sup+', [status(thm)], [zip_derived_cl274, zip_derived_cl309])).
% 0.43/1.03 thf(zip_derived_cl1, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (~ (smaller @ X0 @ X1) | (smaller_or_equal @ X0 @ X1))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_smaller_or_equal_2])).
% 0.43/1.03 thf(zip_derived_cl19, plain, ( (organization @ sk1)),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.43/1.03 thf(assumption_5_42, axiom,
% 0.43/1.03 (( ~( organization @ A ) ) |
% 0.43/1.03 ( ~( smaller_or_equal @
% 0.43/1.03 ( stock_of_knowledge @ A @ B ) @ ( stock_of_knowledge @ A @ C ) ) ) |
% 0.43/1.03 ( ~( greater @
% 0.43/1.03 ( internal_friction @ A @ B ) @ ( internal_friction @ A @ C ) ) ) |
% 0.43/1.03 ( smaller @ ( capability @ A @ B ) @ ( capability @ A @ C ) ))).
% 0.43/1.03 thf(zip_derived_cl15, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.43/1.03 (~ (organization @ X0)
% 0.43/1.03 | ~ (smaller_or_equal @ (stock_of_knowledge @ X0 @ X1) @
% 0.43/1.03 (stock_of_knowledge @ X0 @ X2))
% 0.43/1.03 | ~ (greater @ (internal_friction @ X0 @ X1) @
% 0.43/1.03 (internal_friction @ X0 @ X2))
% 0.43/1.03 | (smaller @ (capability @ X0 @ X1) @ (capability @ X0 @ X2)))),
% 0.43/1.03 inference('cnf', [status(esa)], [assumption_5_42])).
% 0.43/1.03 thf(zip_derived_cl210, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 ( (smaller @ (capability @ sk1 @ X1) @ (capability @ sk1 @ X0))
% 0.43/1.03 | ~ (greater @ (internal_friction @ sk1 @ X1) @
% 0.43/1.03 (internal_friction @ sk1 @ X0))
% 0.43/1.03 | ~ (smaller_or_equal @ (stock_of_knowledge @ sk1 @ X1) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ X0)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl19, zip_derived_cl15])).
% 0.43/1.03 thf(zip_derived_cl216, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (~ (smaller @ (stock_of_knowledge @ sk1 @ X1) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ X0))
% 0.43/1.03 | ~ (greater @ (internal_friction @ sk1 @ X1) @
% 0.43/1.03 (internal_friction @ sk1 @ X0))
% 0.43/1.03 | (smaller @ (capability @ sk1 @ X1) @ (capability @ sk1 @ X0)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl1, zip_derived_cl210])).
% 0.43/1.03 thf(zip_derived_cl6, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]: (~ (smaller @ X0 @ X1) | (greater @ X1 @ X0))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_smaller_7])).
% 0.43/1.03 thf(zip_derived_cl375, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 ( (smaller @ (capability @ sk1 @ X1) @ (capability @ sk1 @ X0))
% 0.43/1.03 | ~ (smaller @ (stock_of_knowledge @ sk1 @ X1) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ X0))
% 0.43/1.03 | ~ (smaller @ (internal_friction @ sk1 @ X0) @
% 0.43/1.03 (internal_friction @ sk1 @ X1)))),
% 0.43/1.03 inference('sup+', [status(thm)], [zip_derived_cl216, zip_derived_cl6])).
% 0.43/1.03 thf(zip_derived_cl379, plain,
% 0.43/1.03 ((((stock_of_knowledge @ sk1 @ sk3) = (stock_of_knowledge @ sk1 @ sk2))
% 0.43/1.03 | ~ (smaller @ (internal_friction @ sk1 @ sk3) @
% 0.43/1.03 (internal_friction @ sk1 @ sk2))
% 0.43/1.03 | (smaller @ (capability @ sk1 @ sk2) @ (capability @ sk1 @ sk3)))),
% 0.43/1.03 inference('sup-', [status(thm)], [zip_derived_cl366, zip_derived_cl375])).
% 0.43/1.03 thf(zip_derived_cl2, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]: (((X1) != (X0)) | (smaller_or_equal @ X1 @ X0))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_smaller_or_equal_3])).
% 0.43/1.03 thf(zip_derived_cl210, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 ( (smaller @ (capability @ sk1 @ X1) @ (capability @ sk1 @ X0))
% 0.43/1.03 | ~ (greater @ (internal_friction @ sk1 @ X1) @
% 0.43/1.03 (internal_friction @ sk1 @ X0))
% 0.43/1.03 | ~ (smaller_or_equal @ (stock_of_knowledge @ sk1 @ X1) @
% 0.43/1.03 (stock_of_knowledge @ sk1 @ X0)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl19, zip_derived_cl15])).
% 0.43/1.03 thf(zip_derived_cl219, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (((stock_of_knowledge @ sk1 @ X0) != (stock_of_knowledge @ sk1 @ X1))
% 0.43/1.03 | ~ (greater @ (internal_friction @ sk1 @ X0) @
% 0.43/1.03 (internal_friction @ sk1 @ X1))
% 0.43/1.03 | (smaller @ (capability @ sk1 @ X0) @ (capability @ sk1 @ X1)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl2, zip_derived_cl210])).
% 0.43/1.03 thf(zip_derived_cl6, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]: (~ (smaller @ X0 @ X1) | (greater @ X1 @ X0))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_smaller_7])).
% 0.43/1.03 thf(zip_derived_cl353, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 ( (smaller @ (capability @ sk1 @ X1) @ (capability @ sk1 @ X0))
% 0.43/1.03 | ((stock_of_knowledge @ sk1 @ X1) != (stock_of_knowledge @ sk1 @ X0))
% 0.43/1.03 | ~ (smaller @ (internal_friction @ sk1 @ X0) @
% 0.43/1.03 (internal_friction @ sk1 @ X1)))),
% 0.43/1.03 inference('sup+', [status(thm)], [zip_derived_cl219, zip_derived_cl6])).
% 0.43/1.03 thf(zip_derived_cl592, plain,
% 0.43/1.03 (( (smaller @ (capability @ sk1 @ sk2) @ (capability @ sk1 @ sk3))
% 0.43/1.03 | ~ (smaller @ (internal_friction @ sk1 @ sk3) @
% 0.43/1.03 (internal_friction @ sk1 @ sk2)))),
% 0.43/1.03 inference('clc', [status(thm)], [zip_derived_cl379, zip_derived_cl353])).
% 0.43/1.03 thf(zip_derived_cl234, plain,
% 0.43/1.03 ((((internal_friction @ sk1 @ sk3) = (internal_friction @ sk1 @ sk2))
% 0.43/1.03 | (smaller @ (internal_friction @ sk1 @ sk3) @
% 0.43/1.03 (internal_friction @ sk1 @ sk2)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl27, zip_derived_cl0])).
% 0.43/1.03 thf(zip_derived_cl593, plain,
% 0.43/1.03 (( (smaller @ (capability @ sk1 @ sk2) @ (capability @ sk1 @ sk3))
% 0.43/1.03 | ((internal_friction @ sk1 @ sk3) = (internal_friction @ sk1 @ sk2)))),
% 0.43/1.03 inference('sup+', [status(thm)], [zip_derived_cl592, zip_derived_cl234])).
% 0.43/1.03 thf(zip_derived_cl808, plain,
% 0.43/1.03 (~ (greater @ (capability @ sk1 @ sk3) @ (capability @ sk1 @ sk2))),
% 0.43/1.03 inference('clc', [status(thm)], [zip_derived_cl807, zip_derived_cl37])).
% 0.43/1.03 thf(zip_derived_cl6, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]: (~ (smaller @ X0 @ X1) | (greater @ X1 @ X0))),
% 0.43/1.03 inference('cnf', [status(esa)], [definition_smaller_7])).
% 0.43/1.03 thf(zip_derived_cl815, plain,
% 0.43/1.03 (~ (smaller @ (capability @ sk1 @ sk2) @ (capability @ sk1 @ sk3))),
% 0.43/1.03 inference('sup+', [status(thm)], [zip_derived_cl808, zip_derived_cl6])).
% 0.43/1.03 thf(zip_derived_cl868, plain,
% 0.43/1.03 (((internal_friction @ sk1 @ sk3) = (internal_friction @ sk1 @ sk2))),
% 0.43/1.03 inference('demod', [status(thm)], [zip_derived_cl593, zip_derived_cl815])).
% 0.43/1.03 thf(zip_derived_cl19, plain, ( (organization @ sk1)),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.43/1.03 thf(assumption_5_43, axiom,
% 0.43/1.03 (( ~( organization @ A ) ) |
% 0.43/1.03 ( ( stock_of_knowledge @ A @ B ) != ( stock_of_knowledge @ A @ C ) ) |
% 0.43/1.03 ( ( internal_friction @ A @ B ) != ( internal_friction @ A @ C ) ) |
% 0.43/1.03 ( ( capability @ A @ B ) = ( capability @ A @ C ) ))).
% 0.43/1.03 thf(zip_derived_cl16, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.43/1.03 (~ (organization @ X0)
% 0.43/1.03 | ((stock_of_knowledge @ X0 @ X2) != (stock_of_knowledge @ X0 @ X1))
% 0.43/1.03 | ((internal_friction @ X0 @ X2) != (internal_friction @ X0 @ X1))
% 0.43/1.03 | ((capability @ X0 @ X2) = (capability @ X0 @ X1)))),
% 0.43/1.03 inference('cnf', [status(esa)], [assumption_5_43])).
% 0.43/1.03 thf(zip_derived_cl211, plain,
% 0.43/1.03 (![X0 : $i, X1 : $i]:
% 0.43/1.03 (((capability @ sk1 @ X0) = (capability @ sk1 @ X1))
% 0.43/1.03 | ((internal_friction @ sk1 @ X0) != (internal_friction @ sk1 @ X1))
% 0.43/1.03 | ((stock_of_knowledge @ sk1 @ X0) != (stock_of_knowledge @ sk1 @ X1)))),
% 0.43/1.03 inference('dp-resolution', [status(thm)],
% 0.43/1.03 [zip_derived_cl19, zip_derived_cl16])).
% 0.43/1.03 thf(zip_derived_cl879, plain,
% 0.43/1.03 (![X0 : $i]:
% 0.43/1.03 (((internal_friction @ sk1 @ sk2) != (internal_friction @ sk1 @ X0))
% 0.43/1.03 | ((stock_of_knowledge @ sk1 @ sk3)
% 0.43/1.03 != (stock_of_knowledge @ sk1 @ X0))
% 0.43/1.03 | ((capability @ sk1 @ sk3) = (capability @ sk1 @ X0)))),
% 0.43/1.03 inference('sup-', [status(thm)], [zip_derived_cl868, zip_derived_cl211])).
% 0.43/1.03 thf(zip_derived_cl811, plain,
% 0.43/1.03 (((stock_of_knowledge @ sk1 @ sk3) = (stock_of_knowledge @ sk1 @ sk2))),
% 0.43/1.03 inference('demod', [status(thm)], [zip_derived_cl557, zip_derived_cl808])).
% 0.43/1.03 thf(zip_derived_cl889, plain,
% 0.43/1.03 (![X0 : $i]:
% 0.43/1.03 (((internal_friction @ sk1 @ sk2) != (internal_friction @ sk1 @ X0))
% 0.43/1.03 | ((stock_of_knowledge @ sk1 @ sk2)
% 0.43/1.03 != (stock_of_knowledge @ sk1 @ X0))
% 0.43/1.03 | ((capability @ sk1 @ sk3) = (capability @ sk1 @ X0)))),
% 0.43/1.03 inference('demod', [status(thm)], [zip_derived_cl879, zip_derived_cl811])).
% 0.43/1.03 thf(zip_derived_cl1045, plain,
% 0.43/1.03 ((((capability @ sk1 @ sk3) = (capability @ sk1 @ sk2))
% 0.43/1.03 | ((stock_of_knowledge @ sk1 @ sk2) != (stock_of_knowledge @ sk1 @ sk2)))),
% 0.43/1.03 inference('eq_res', [status(thm)], [zip_derived_cl889])).
% 0.43/1.03 thf(zip_derived_cl1046, plain,
% 0.43/1.03 (((capability @ sk1 @ sk3) = (capability @ sk1 @ sk2))),
% 0.43/1.03 inference('simplify', [status(thm)], [zip_derived_cl1045])).
% 0.43/1.03 thf(zip_derived_cl1095, plain,
% 0.43/1.03 ((~ (greater_or_equal @ (capability @ sk1 @ sk2) @
% 0.43/1.03 (capability @ sk1 @ sk2))
% 0.43/1.03 | (smaller @ (hazard_of_mortality @ sk1 @ sk3) @
% 0.43/1.03 (hazard_of_mortality @ sk1 @ sk2)))),
% 0.43/1.03 inference('demod', [status(thm)], [zip_derived_cl988, zip_derived_cl1046])).
% 0.43/1.03 thf(zip_derived_cl37, plain,
% 0.43/1.03 (~ (smaller @ (hazard_of_mortality @ sk1 @ sk3) @
% 0.43/1.03 (hazard_of_mortality @ sk1 @ sk2))),
% 0.43/1.03 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.43/1.03 thf(zip_derived_cl1096, plain,
% 0.43/1.03 (~ (greater_or_equal @ (capability @ sk1 @ sk2) @
% 0.43/1.03 (capability @ sk1 @ sk2))),
% 0.43/1.03 inference('clc', [status(thm)], [zip_derived_cl1095, zip_derived_cl37])).
% 0.43/1.03 thf(zip_derived_cl1100, plain,
% 0.43/1.03 (((capability @ sk1 @ sk2) != (capability @ sk1 @ sk2))),
% 0.43/1.03 inference('sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl1096])).
% 0.43/1.03 thf(zip_derived_cl1103, plain, ($false),
% 0.43/1.03 inference('simplify', [status(thm)], [zip_derived_cl1100])).
% 0.43/1.03
% 0.43/1.03 % SZS output end Refutation
% 0.43/1.03
% 0.43/1.03
% 0.43/1.03 % Terminating...
% 3.43/1.08 % Runner terminated.
% 3.43/1.10 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------