%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : LCL039-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.GFzKbcLY1k true
% Computer : n008.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 : Mon Sep 7 01:35:04 PM UTC 2026
% Result : Unsatisfiable 37.25s 6.00s
% Output : Refutation 37.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL039-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.GFzKbcLY1k true
% 0.09/0.36 % Computer : n008.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 00:14:08 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Running portfolio for 300 s
% 0.09/0.37 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Number of cores: 8
% 0.09/0.37 % Python version: Python 3.12.3
% 0.09/0.37 % Running in FO mode
% 0.33/0.60 % Total configuration time : 435
% 0.33/0.60 % Estimated wc time : 1092
% 0.33/0.60 % Estimated cpu time (7 cpus) : 156.0
% 0.40/0.67 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.40/0.73 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.40/0.73 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.40/0.73 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.40/0.74 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.40/0.74 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.40/0.74 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 37.25/6.00 % Solved by fo/fo1_av.sh.
% 37.25/6.00 % done 4301 iterations in 5.230s
% 37.25/6.00 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 37.25/6.00 % SZS output start Refutation
% 37.25/6.00 thf(not_type, type, not: $i > $i).
% 37.25/6.00 thf(is_a_theorem_type, type, is_a_theorem: $i > $o).
% 37.25/6.00 thf(implies_type, type, implies: $i > $i > $i).
% 37.25/6.00 thf(necessary_type, type, necessary: $i > $i).
% 37.25/6.00 thf(a_type, type, a: $i).
% 37.25/6.00 thf(necessitation2, axiom,
% 37.25/6.00 (is_a_theorem @ ( implies @ ( necessary @ X ) @ X ))).
% 37.25/6.00 thf(zip_derived_cl5, plain,
% 37.25/6.00 (![X0 : $i]: (is_a_theorem @ (implies @ (necessary @ X0) @ X0))),
% 37.25/6.00 inference('cnf', [status(esa)], [necessitation2])).
% 37.25/6.00 thf(cn_35, axiom,
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 ( implies @
% 37.25/6.00 ( implies @ X @ ( implies @ Y @ Z ) ) @
% 37.25/6.00 ( implies @ ( implies @ X @ Y ) @ ( implies @ X @ Z ) ) ))).
% 37.25/6.00 thf(zip_derived_cl2, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 (implies @ (implies @ X0 @ (implies @ X1 @ X2)) @
% 37.25/6.00 (implies @ (implies @ X0 @ X1) @ (implies @ X0 @ X2))))),
% 37.25/6.00 inference('cnf', [status(esa)], [cn_35])).
% 37.25/6.00 thf(condensed_detachment, axiom,
% 37.25/6.00 (( ~( is_a_theorem @ ( implies @ X @ Y ) ) ) | ( ~( is_a_theorem @ X ) ) |
% 37.25/6.00 ( is_a_theorem @ Y ))).
% 37.25/6.00 thf(zip_derived_cl0, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X0 @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ X0)
% 37.25/6.00 | (is_a_theorem @ X1))),
% 37.25/6.00 inference('cnf', [status(esa)], [condensed_detachment])).
% 37.25/6.00 thf(zip_derived_cl27, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ (implies @ X2 @ X0)))
% 37.25/6.00 | (is_a_theorem @
% 37.25/6.00 (implies @ (implies @ X1 @ X2) @ (implies @ X1 @ X0))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl2, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl0, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X0 @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ X0)
% 37.25/6.00 | (is_a_theorem @ X1))),
% 37.25/6.00 inference('cnf', [status(esa)], [condensed_detachment])).
% 37.25/6.00 thf(zip_derived_cl115, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ (implies @ X2 @ X0)))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X1 @ X2))
% 37.25/6.00 | (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl27, zip_derived_cl0])).
% 37.25/6.00 thf(cn_18, axiom, (is_a_theorem @ ( implies @ X @ ( implies @ Y @ X ) ))).
% 37.25/6.00 thf(zip_derived_cl1, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ X0 @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [cn_18])).
% 37.25/6.00 thf(zip_derived_cl0, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X0 @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ X0)
% 37.25/6.00 | (is_a_theorem @ X1))),
% 37.25/6.00 inference('cnf', [status(esa)], [condensed_detachment])).
% 37.25/6.00 thf(zip_derived_cl11, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ X0) | (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl216, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ X2 @ X0))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X2 @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl115, zip_derived_cl11])).
% 37.25/6.00 thf(zip_derived_cl334, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ (necessary @ X0) @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X0 @ X1)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl216])).
% 37.25/6.00 thf(prove_this, conjecture,
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 ( implies @ ( necessary @ a ) @ ( not @ ( necessary @ ( not @ a ) ) ) ))).
% 37.25/6.00 thf(zf_stmt_0, negated_conjecture,
% 37.25/6.00 (~( is_a_theorem @
% 37.25/6.00 ( implies @ ( necessary @ a ) @ ( not @ ( necessary @ ( not @ a ) ) ) ) )),
% 37.25/6.00 inference('cnf.neg', [status(esa)], [prove_this])).
% 37.25/6.00 thf(zip_derived_cl7, plain,
% 37.25/6.00 (~ (is_a_theorem @
% 37.25/6.00 (implies @ (necessary @ a) @ (not @ (necessary @ (not @ a)))))),
% 37.25/6.00 inference('cnf', [status(esa)], [zf_stmt_0])).
% 37.25/6.00 thf(zip_derived_cl586, plain,
% 37.25/6.00 (~ (is_a_theorem @ (implies @ a @ (not @ (necessary @ (not @ a)))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl334, zip_derived_cl7])).
% 37.25/6.00 thf(zip_derived_cl11, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ X0) | (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl115, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ (implies @ X2 @ X0)))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X1 @ X2))
% 37.25/6.00 | (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl27, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl1, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ X0 @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [cn_18])).
% 37.25/6.00 thf(zip_derived_cl217, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ X0 @ X0))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X0 @ X1)))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl115, zip_derived_cl1])).
% 37.25/6.00 thf(zip_derived_cl232, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ X0) | (is_a_theorem @ (implies @ X1 @ X1)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl11, zip_derived_cl217])).
% 37.25/6.00 thf(zip_derived_cl244, plain,
% 37.25/6.00 ((![X1 : $i]: (is_a_theorem @ (implies @ X1 @ X1)))
% 37.25/6.00 <= ((![X1 : $i]: (is_a_theorem @ (implies @ X1 @ X1))))),
% 37.25/6.00 inference('split', [status(esa)], [zip_derived_cl232])).
% 37.25/6.00 thf(cn_49, axiom,
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 ( implies @ ( implies @ ( not @ X ) @ ( not @ Y ) ) @ ( implies @ Y @ X ) ))).
% 37.25/6.00 thf(zip_derived_cl3, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 (implies @ (implies @ (not @ X0) @ (not @ X1)) @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [cn_49])).
% 37.25/6.00 thf(zip_derived_cl0, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X0 @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ X0)
% 37.25/6.00 | (is_a_theorem @ X1))),
% 37.25/6.00 inference('cnf', [status(esa)], [condensed_detachment])).
% 37.25/6.00 thf(zip_derived_cl14, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ (not @ X0) @ (not @ X1)))
% 37.25/6.00 | (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl3, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl251, plain,
% 37.25/6.00 ((![X0 : $i]: (is_a_theorem @ (implies @ X0 @ X0)))
% 37.25/6.00 <= ((![X1 : $i]: (is_a_theorem @ (implies @ X1 @ X1))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl244, zip_derived_cl14])).
% 37.25/6.00 thf(zip_derived_cl245, plain,
% 37.25/6.00 ((![X0 : $i]: ~ (is_a_theorem @ X0))
% 37.25/6.00 <= ((![X0 : $i]: ~ (is_a_theorem @ X0)))),
% 37.25/6.00 inference('split', [status(esa)], [zip_derived_cl232])).
% 37.25/6.00 thf(zip_derived_cl1, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ X0 @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [cn_18])).
% 37.25/6.00 thf('0', plain, (~ (![X0 : $i]: ~ (is_a_theorem @ X0))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl245, zip_derived_cl1])).
% 37.25/6.00 thf('1', plain,
% 37.25/6.00 ((![X1 : $i]: (is_a_theorem @ (implies @ X1 @ X1))) |
% 37.25/6.00 (![X0 : $i]: ~ (is_a_theorem @ X0))),
% 37.25/6.00 inference('split', [status(esa)], [zip_derived_cl232])).
% 37.25/6.00 thf('2', plain, ((![X1 : $i]: (is_a_theorem @ (implies @ X1 @ X1)))),
% 37.25/6.00 inference('sat_resolution*', [status(thm)], ['0', '1'])).
% 37.25/6.00 thf(zip_derived_cl291, plain,
% 37.25/6.00 (![X0 : $i]: (is_a_theorem @ (implies @ X0 @ X0))),
% 37.25/6.00 inference('simpl_trail', [status(thm)], [zip_derived_cl251, '2'])).
% 37.25/6.00 thf(zip_derived_cl3, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 (implies @ (implies @ (not @ X0) @ (not @ X1)) @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [cn_49])).
% 37.25/6.00 thf(necessitation1, axiom,
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 ( implies @
% 37.25/6.00 ( necessary @ ( implies @ X @ Y ) ) @
% 37.25/6.00 ( implies @ ( necessary @ X ) @ ( necessary @ Y ) ) ))).
% 37.25/6.00 thf(zip_derived_cl4, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 (implies @ (necessary @ (implies @ X0 @ X1)) @
% 37.25/6.00 (implies @ (necessary @ X0) @ (necessary @ X1))))),
% 37.25/6.00 inference('cnf', [status(esa)], [necessitation1])).
% 37.25/6.00 thf(zip_derived_cl0, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X0 @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ X0)
% 37.25/6.00 | (is_a_theorem @ X1))),
% 37.25/6.00 inference('cnf', [status(esa)], [condensed_detachment])).
% 37.25/6.00 thf(zip_derived_cl17, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (necessary @ (implies @ X1 @ X0)))
% 37.25/6.00 | (is_a_theorem @ (implies @ (necessary @ X1) @ (necessary @ X0))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl4, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl0, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X0 @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ X0)
% 37.25/6.00 | (is_a_theorem @ X1))),
% 37.25/6.00 inference('cnf', [status(esa)], [condensed_detachment])).
% 37.25/6.00 thf(zip_derived_cl18, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (necessary @ (implies @ X1 @ X0)))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ X1))
% 37.25/6.00 | (is_a_theorem @ (necessary @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl17, zip_derived_cl0])).
% 37.25/6.00 thf(axiom_of_necessitation, axiom,
% 37.25/6.00 (( ~( is_a_theorem @ X ) ) | ( is_a_theorem @ ( necessary @ X ) ))).
% 37.25/6.00 thf(zip_derived_cl6, plain,
% 37.25/6.00 (![X0 : $i]: (~ (is_a_theorem @ X0) | (is_a_theorem @ (necessary @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [axiom_of_necessitation])).
% 37.25/6.00 thf(zip_derived_cl19, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (necessary @ X0))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl18, zip_derived_cl6])).
% 37.25/6.00 thf(zip_derived_cl23, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (necessary @ (implies @ X1 @ X0)))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ (implies @ (not @ X0) @ (not @ X1)))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl3, zip_derived_cl19])).
% 37.25/6.00 thf(zip_derived_cl6, plain,
% 37.25/6.00 (![X0 : $i]: (~ (is_a_theorem @ X0) | (is_a_theorem @ (necessary @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [axiom_of_necessitation])).
% 37.25/6.00 thf(zip_derived_cl34, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (necessary @ (implies @ X0 @ X1)))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ (not @ X1) @ (not @ X0))))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl23, zip_derived_cl6])).
% 37.25/6.00 thf(zip_derived_cl297, plain,
% 37.25/6.00 (![X0 : $i]: (is_a_theorem @ (necessary @ (implies @ X0 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl291, zip_derived_cl34])).
% 37.25/6.00 thf(zip_derived_cl1, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ X0 @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [cn_18])).
% 37.25/6.00 thf(zip_derived_cl19, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (necessary @ X0))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl18, zip_derived_cl6])).
% 37.25/6.00 thf(zip_derived_cl22, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (necessary @ (implies @ X1 @ X0)))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl19])).
% 37.25/6.00 thf(zip_derived_cl5, plain,
% 37.25/6.00 (![X0 : $i]: (is_a_theorem @ (implies @ (necessary @ X0) @ X0))),
% 37.25/6.00 inference('cnf', [status(esa)], [necessitation2])).
% 37.25/6.00 thf(zip_derived_cl0, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X0 @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ X0)
% 37.25/6.00 | (is_a_theorem @ X1))),
% 37.25/6.00 inference('cnf', [status(esa)], [condensed_detachment])).
% 37.25/6.00 thf(zip_derived_cl8, plain,
% 37.25/6.00 (![X0 : $i]: (~ (is_a_theorem @ (necessary @ X0)) | (is_a_theorem @ X0))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl30, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (necessary @ X0))
% 37.25/6.00 | (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl22, zip_derived_cl8])).
% 37.25/6.00 thf(zip_derived_cl303, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ X1 @ (implies @ X0 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl297, zip_derived_cl30])).
% 37.25/6.00 thf(zip_derived_cl6, plain,
% 37.25/6.00 (![X0 : $i]: (~ (is_a_theorem @ X0) | (is_a_theorem @ (necessary @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [axiom_of_necessitation])).
% 37.25/6.00 thf(zip_derived_cl17, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (necessary @ (implies @ X1 @ X0)))
% 37.25/6.00 | (is_a_theorem @ (implies @ (necessary @ X1) @ (necessary @ X0))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl4, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl19, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (necessary @ X0))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl18, zip_derived_cl6])).
% 37.25/6.00 thf(zip_derived_cl26, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (necessary @ (implies @ X1 @ X0)))
% 37.25/6.00 | (is_a_theorem @ (necessary @ (necessary @ X0)))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ (necessary @ X1))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl17, zip_derived_cl19])).
% 37.25/6.00 thf(zip_derived_cl71, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ X0))
% 37.25/6.00 | (is_a_theorem @ (necessary @ (necessary @ X0)))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ (necessary @ X1))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl6, zip_derived_cl26])).
% 37.25/6.00 thf(zip_derived_cl309, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (necessary @ (necessary @ (implies @ X0 @ X0))))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ (necessary @ X1))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl303, zip_derived_cl71])).
% 37.25/6.00 thf(zip_derived_cl355, plain,
% 37.25/6.00 ((![X0 : $i]:
% 37.25/6.00 (is_a_theorem @ (necessary @ (necessary @ (implies @ X0 @ X0)))))
% 37.25/6.00 <= ((![X0 : $i]:
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 (necessary @ (necessary @ (implies @ X0 @ X0))))))),
% 37.25/6.00 inference('split', [status(esa)], [zip_derived_cl309])).
% 37.25/6.00 thf(zip_derived_cl30, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (necessary @ X0))
% 37.25/6.00 | (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl22, zip_derived_cl8])).
% 37.25/6.00 thf(zip_derived_cl357, plain,
% 37.25/6.00 ((![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ X1 @ (necessary @ (implies @ X0 @ X0)))))
% 37.25/6.00 <= ((![X0 : $i]:
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 (necessary @ (necessary @ (implies @ X0 @ X0))))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl355, zip_derived_cl30])).
% 37.25/6.00 thf(zip_derived_cl11, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ X0) | (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl71, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ X0))
% 37.25/6.00 | (is_a_theorem @ (necessary @ (necessary @ X0)))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ (necessary @ X1))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl6, zip_derived_cl26])).
% 37.25/6.00 thf(zip_derived_cl126, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ X0)
% 37.25/6.00 | (is_a_theorem @ (necessary @ (necessary @ X0)))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ (necessary @ X1))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl11, zip_derived_cl71])).
% 37.25/6.00 thf(zip_derived_cl134, plain,
% 37.25/6.00 ((![X1 : $i]: ~ (is_a_theorem @ (necessary @ (necessary @ X1))))
% 37.25/6.00 <= ((![X1 : $i]: ~ (is_a_theorem @ (necessary @ (necessary @ X1)))))),
% 37.25/6.00 inference('split', [status(esa)], [zip_derived_cl126])).
% 37.25/6.00 thf(zip_derived_cl6, plain,
% 37.25/6.00 (![X0 : $i]: (~ (is_a_theorem @ X0) | (is_a_theorem @ (necessary @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [axiom_of_necessitation])).
% 37.25/6.00 thf(zip_derived_cl136, plain,
% 37.25/6.00 ((![X0 : $i]: ~ (is_a_theorem @ (necessary @ X0)))
% 37.25/6.00 <= ((![X1 : $i]: ~ (is_a_theorem @ (necessary @ (necessary @ X1)))))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl134, zip_derived_cl6])).
% 37.25/6.00 thf(zip_derived_cl6, plain,
% 37.25/6.00 (![X0 : $i]: (~ (is_a_theorem @ X0) | (is_a_theorem @ (necessary @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [axiom_of_necessitation])).
% 37.25/6.00 thf(zip_derived_cl138, plain,
% 37.25/6.00 ((![X0 : $i]: ~ (is_a_theorem @ X0))
% 37.25/6.00 <= ((![X1 : $i]: ~ (is_a_theorem @ (necessary @ (necessary @ X1)))))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl136, zip_derived_cl6])).
% 37.25/6.00 thf(zip_derived_cl1, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ X0 @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [cn_18])).
% 37.25/6.00 thf('3', plain,
% 37.25/6.00 (~ (![X1 : $i]: ~ (is_a_theorem @ (necessary @ (necessary @ X1))))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl138, zip_derived_cl1])).
% 37.25/6.00 thf('4', plain,
% 37.25/6.00 ((![X0 : $i]:
% 37.25/6.00 (is_a_theorem @ (necessary @ (necessary @ (implies @ X0 @ X0))))) |
% 37.25/6.00 (![X1 : $i]: ~ (is_a_theorem @ (necessary @ (necessary @ X1))))),
% 37.25/6.00 inference('split', [status(esa)], [zip_derived_cl309])).
% 37.25/6.00 thf('5', plain,
% 37.25/6.00 ((![X0 : $i]:
% 37.25/6.00 (is_a_theorem @ (necessary @ (necessary @ (implies @ X0 @ X0)))))),
% 37.25/6.00 inference('sat_resolution*', [status(thm)], ['3', '4'])).
% 37.25/6.00 thf(zip_derived_cl361, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ X1 @ (necessary @ (implies @ X0 @ X0))))),
% 37.25/6.00 inference('simpl_trail', [status(thm)], [zip_derived_cl357, '5'])).
% 37.25/6.00 thf(zip_derived_cl71, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ X0))
% 37.25/6.00 | (is_a_theorem @ (necessary @ (necessary @ X0)))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ (necessary @ X1))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl6, zip_derived_cl26])).
% 37.25/6.00 thf(zip_derived_cl480, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @
% 37.25/6.00 (necessary @ (necessary @ (necessary @ (implies @ X0 @ X0)))))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ (necessary @ X1))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl361, zip_derived_cl71])).
% 37.25/6.00 thf(zip_derived_cl489, plain,
% 37.25/6.00 ((![X0 : $i]:
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 (necessary @ (necessary @ (necessary @ (implies @ X0 @ X0))))))
% 37.25/6.00 <= ((![X0 : $i]:
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 (necessary @ (necessary @ (necessary @ (implies @ X0 @ X0)))))))),
% 37.25/6.00 inference('split', [status(esa)], [zip_derived_cl480])).
% 37.25/6.00 thf('6', plain,
% 37.25/6.00 ((![X0 : $i]:
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 (necessary @ (necessary @ (necessary @ (implies @ X0 @ X0)))))) |
% 37.25/6.00 (![X1 : $i]: ~ (is_a_theorem @ (necessary @ (necessary @ X1))))),
% 37.25/6.00 inference('split', [status(esa)], [zip_derived_cl480])).
% 37.25/6.00 thf('7', plain,
% 37.25/6.00 ((![X0 : $i]:
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 (necessary @ (necessary @ (necessary @ (implies @ X0 @ X0))))))),
% 37.25/6.00 inference('sat_resolution*', [status(thm)], ['3', '6'])).
% 37.25/6.00 thf(zip_derived_cl498, plain,
% 37.25/6.00 (![X0 : $i]:
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 (necessary @ (necessary @ (necessary @ (implies @ X0 @ X0)))))),
% 37.25/6.00 inference('simpl_trail', [status(thm)], [zip_derived_cl489, '7'])).
% 37.25/6.00 thf(zip_derived_cl334, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ (necessary @ X0) @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X0 @ X1)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl216])).
% 37.25/6.00 thf(zip_derived_cl334, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ (necessary @ X0) @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X0 @ X1)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl216])).
% 37.25/6.00 thf(zip_derived_cl334, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ (necessary @ X0) @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X0 @ X1)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl216])).
% 37.25/6.00 thf(zip_derived_cl0, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X0 @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ X0)
% 37.25/6.00 | (is_a_theorem @ X1))),
% 37.25/6.00 inference('cnf', [status(esa)], [condensed_detachment])).
% 37.25/6.00 thf(zip_derived_cl576, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ X0))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ X1))
% 37.25/6.00 | (is_a_theorem @ X0))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl334, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl626, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ X0))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ (necessary @ X1)))
% 37.25/6.00 | (is_a_theorem @ X0))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl334, zip_derived_cl576])).
% 37.25/6.00 thf(zip_derived_cl691, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ X0))
% 37.25/6.00 | ~ (is_a_theorem @ (necessary @ (necessary @ (necessary @ X1))))
% 37.25/6.00 | (is_a_theorem @ X0))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl334, zip_derived_cl626])).
% 37.25/6.00 thf(zip_derived_cl784, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ (implies @ X0 @ X0) @ X1))
% 37.25/6.00 | (is_a_theorem @ X1))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl498, zip_derived_cl691])).
% 37.25/6.00 thf(zip_derived_cl27, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ (implies @ X2 @ X0)))
% 37.25/6.00 | (is_a_theorem @
% 37.25/6.00 (implies @ (implies @ X1 @ X2) @ (implies @ X1 @ X0))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl2, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl798, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ X1 @ X0))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X1 @ (implies @ X1 @ X0))))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl784, zip_derived_cl27])).
% 37.25/6.00 thf(zip_derived_cl334, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ (necessary @ X0) @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X0 @ X1)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl216])).
% 37.25/6.00 thf(zip_derived_cl974, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ (necessary @ X1) @ X0))
% 37.25/6.00 | ~ (is_a_theorem @
% 37.25/6.00 (implies @ X1 @ (implies @ (necessary @ X1) @ X0))))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl798, zip_derived_cl334])).
% 37.25/6.00 thf(zip_derived_cl1, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ X0 @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [cn_18])).
% 37.25/6.00 thf(zip_derived_cl216, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ X2 @ X0))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X2 @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl115, zip_derived_cl11])).
% 37.25/6.00 thf(zip_derived_cl325, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ X0 @ X2))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ (implies @ X1 @ X0) @ X2)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl216])).
% 37.25/6.00 thf(zip_derived_cl1, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ X0 @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [cn_18])).
% 37.25/6.00 thf(zip_derived_cl373, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ X0 @ (implies @ X2 @ (implies @ X1 @ X0))))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl325, zip_derived_cl1])).
% 37.25/6.00 thf(zip_derived_cl9699, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ (necessary @ X0) @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl974, zip_derived_cl373])).
% 37.25/6.00 thf(zip_derived_cl325, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ X0 @ X2))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ (implies @ X1 @ X0) @ X2)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl216])).
% 37.25/6.00 thf(zip_derived_cl27, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ (implies @ X2 @ X0)))
% 37.25/6.00 | (is_a_theorem @
% 37.25/6.00 (implies @ (implies @ X1 @ X2) @ (implies @ X1 @ X0))))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl2, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl381, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ X2 @ (implies @ X1 @ X0)))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X1 @ (implies @ X2 @ X0))))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl325, zip_derived_cl27])).
% 37.25/6.00 thf(zip_derived_cl12555, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ X1 @ (implies @ (necessary @ X0) @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)],
% 37.25/6.00 [zip_derived_cl9699, zip_derived_cl381])).
% 37.25/6.00 thf(zip_derived_cl115, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ (implies @ X2 @ X0)))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X1 @ X2))
% 37.25/6.00 | (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl27, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl13065, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ (necessary @ X0)))
% 37.25/6.00 | (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)],
% 37.25/6.00 [zip_derived_cl12555, zip_derived_cl115])).
% 37.25/6.00 thf(zip_derived_cl11, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ X0) | (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl115, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ X1 @ (implies @ X2 @ X0)))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X1 @ X2))
% 37.25/6.00 | (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl27, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl3, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 (implies @ (implies @ (not @ X0) @ (not @ X1)) @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [cn_49])).
% 37.25/6.00 thf(zip_derived_cl220, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ (implies @ (not @ X0) @ (not @ X1)) @ X0))
% 37.25/6.00 | ~ (is_a_theorem @
% 37.25/6.00 (implies @ (implies @ (not @ X0) @ (not @ X1)) @ X1)))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl115, zip_derived_cl3])).
% 37.25/6.00 thf(zip_derived_cl769, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ X0)
% 37.25/6.00 | (is_a_theorem @
% 37.25/6.00 (implies @ (implies @ (not @ X1) @ (not @ X0)) @ X1)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl11, zip_derived_cl220])).
% 37.25/6.00 thf(zip_derived_cl325, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ X0 @ X2))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ (implies @ X1 @ X0) @ X2)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl216])).
% 37.25/6.00 thf(zip_derived_cl3, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @
% 37.25/6.00 (implies @ (implies @ (not @ X0) @ (not @ X1)) @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('cnf', [status(esa)], [cn_49])).
% 37.25/6.00 thf(zip_derived_cl380, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ (not @ X1) @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl325, zip_derived_cl3])).
% 37.25/6.00 thf(zip_derived_cl216, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ X2 @ X0))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X2 @ X1))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup+', [status(thm)], [zip_derived_cl115, zip_derived_cl11])).
% 37.25/6.00 thf(zip_derived_cl760, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i, X2 : $i]:
% 37.25/6.00 ( (is_a_theorem @ (implies @ (not @ X1) @ X2))
% 37.25/6.00 | ~ (is_a_theorem @ (implies @ (implies @ X1 @ X0) @ X2)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl380, zip_derived_cl216])).
% 37.25/6.00 thf(zip_derived_cl6746, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ X1)
% 37.25/6.00 | (is_a_theorem @ (implies @ (not @ (not @ X0)) @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl769, zip_derived_cl760])).
% 37.25/6.00 thf(zip_derived_cl6761, plain,
% 37.25/6.00 ((![X0 : $i]: (is_a_theorem @ (implies @ (not @ (not @ X0)) @ X0)))
% 37.25/6.00 <= ((![X0 : $i]: (is_a_theorem @ (implies @ (not @ (not @ X0)) @ X0))))),
% 37.25/6.00 inference('split', [status(esa)], [zip_derived_cl6746])).
% 37.25/6.00 thf('8', plain,
% 37.25/6.00 ((![X0 : $i]: (is_a_theorem @ (implies @ (not @ (not @ X0)) @ X0))) |
% 37.25/6.00 (![X0 : $i]: ~ (is_a_theorem @ X0))),
% 37.25/6.00 inference('split', [status(esa)], [zip_derived_cl6746])).
% 37.25/6.00 thf('9', plain,
% 37.25/6.00 ((![X0 : $i]: (is_a_theorem @ (implies @ (not @ (not @ X0)) @ X0)))),
% 37.25/6.00 inference('sat_resolution*', [status(thm)], ['0', '8'])).
% 37.25/6.00 thf(zip_derived_cl6826, plain,
% 37.25/6.00 (![X0 : $i]: (is_a_theorem @ (implies @ (not @ (not @ X0)) @ X0))),
% 37.25/6.00 inference('simpl_trail', [status(thm)], [zip_derived_cl6761, '9'])).
% 37.25/6.00 thf(zip_derived_cl13249, plain,
% 37.25/6.00 (![X0 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ (not @ (not @ (necessary @ X0))) @ X0))),
% 37.25/6.00 inference('s_sup+', [status(thm)],
% 37.25/6.00 [zip_derived_cl13065, zip_derived_cl6826])).
% 37.25/6.00 thf(zip_derived_cl14, plain,
% 37.25/6.00 (![X0 : $i, X1 : $i]:
% 37.25/6.00 (~ (is_a_theorem @ (implies @ (not @ X0) @ (not @ X1)))
% 37.25/6.00 | (is_a_theorem @ (implies @ X1 @ X0)))),
% 37.25/6.00 inference('s_sup-', [status(thm)], [zip_derived_cl3, zip_derived_cl0])).
% 37.25/6.00 thf(zip_derived_cl13394, plain,
% 37.25/6.00 (![X0 : $i]:
% 37.25/6.00 (is_a_theorem @ (implies @ X0 @ (not @ (necessary @ (not @ X0)))))),
% 37.25/6.00 inference('s_sup-', [status(thm)],
% 37.25/6.00 [zip_derived_cl13249, zip_derived_cl14])).
% 37.25/6.00 thf(zip_derived_cl14302, plain, ($false),
% 37.25/6.00 inference('demod', [status(thm)],
% 37.25/6.00 [zip_derived_cl586, zip_derived_cl13394])).
% 37.25/6.00
% 37.25/6.00 % SZS output end Refutation
% 37.25/6.00
% 37.25/6.00
% 37.25/6.01 % Terminating...
% 38.26/6.05 % Runner terminated.
% 38.26/6.07 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------