%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : HWV007-2 : TPTP v9.2.0. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.4syLSCoj9h true
% Computer : n009.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:37:28 PM UTC 2025
% Result : Unsatisfiable 0.58s 0.85s
% Output : Refutation 0.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.16 % Problem : HWV007-2 : TPTP v9.2.0. Bugfixed v2.7.0.
% 0.12/0.17 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.4syLSCoj9h true
% 0.14/0.38 % Computer : n009.cluster.edu
% 0.14/0.38 % Model : x86_64 x86_64
% 0.14/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.38 % Memory : 8042.1875MB
% 0.14/0.38 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.38 % CPULimit : 300
% 0.14/0.38 % WCLimit : 300
% 0.14/0.38 % DateTime : Wed Oct 1 11:18:08 EDT 2025
% 0.14/0.39 % CPUTime :
% 0.14/0.39 % Running portfolio for 300 s
% 0.14/0.39 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.39 % Number of cores: 8
% 0.14/0.39 % Python version: Python 3.6.8
% 0.14/0.39 % Running in FO mode
% 0.55/0.67 % Total configuration time : 435
% 0.55/0.67 % Estimated wc time : 1092
% 0.55/0.67 % Estimated cpu time (7 cpus) : 156.0
% 0.57/0.74 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.57/0.76 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.57/0.76 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.57/0.77 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.57/0.79 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.57/0.81 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.57/0.82 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.58/0.85 % Solved by fo/fo6_bce.sh.
% 0.58/0.85 % BCE start: 62
% 0.58/0.85 % BCE eliminated: 0
% 0.58/0.85 % PE start: 62
% 0.58/0.85 logic: neq
% 0.58/0.85 % PE eliminated: -103
% 0.58/0.85 % done 211 iterations in 0.079s
% 0.58/0.85 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.58/0.85 % SZS output start Refutation
% 0.58/0.85 thf(h2_type, type, h2: $i > $i).
% 0.58/0.85 thf(outs_type, type, outs: $i > $i).
% 0.58/0.85 thf(h1_type, type, h1: $i > $i).
% 0.58/0.85 thf(and1_type, type, and1: $i > $i).
% 0.58/0.85 thf(logic_or_type, type, logic_or: $i > $o).
% 0.58/0.85 thf(or1_type, type, or1: $i > $i).
% 0.58/0.85 thf(outc_type, type, outc: $i > $i).
% 0.58/0.85 thf(f_type, type, f: $i).
% 0.58/0.85 thf(not_ok_type, type, not_ok: $i > $o).
% 0.58/0.85 thf(abnormal_type, type, abnormal: $i > $o).
% 0.58/0.85 thf(logic_not_type, type, logic_not: $i > $o).
% 0.58/0.85 thf(or_ok_type, type, or_ok: $i > $o).
% 0.58/0.85 thf(and_ok_type, type, and_ok: $i > $o).
% 0.58/0.85 thf(inc_type, type, inc: $i > $i).
% 0.58/0.85 thf(connection_type, type, connection: $i > $i > $o).
% 0.58/0.85 thf(in2_type, type, in2: $i > $i).
% 0.58/0.85 thf(zero_type, type, zero: $i > $o).
% 0.58/0.85 thf(and2_type, type, and2: $i > $i).
% 0.58/0.85 thf(fulladder_type, type, fulladder: $i > $o).
% 0.58/0.85 thf(logic_and_type, type, logic_and: $i > $o).
% 0.58/0.85 thf(out1_type, type, out1: $i > $i).
% 0.58/0.85 thf(not1_type, type, not1: $i > $i).
% 0.58/0.85 thf(one_type, type, one: $i > $o).
% 0.58/0.85 thf(in1_type, type, in1: $i > $i).
% 0.58/0.85 thf(halfadder_type, type, halfadder: $i > $o).
% 0.58/0.85 thf(diagnosis_or1_or1h2, conjecture,
% 0.58/0.85 (~( ( ~( abnormal @ ( or1 @ ( h2 @ f ) ) ) ) |
% 0.58/0.85 ( ~( abnormal @ ( or1 @ f ) ) ) ))).
% 0.58/0.85 thf(zf_stmt_0, negated_conjecture,
% 0.58/0.85 (( ~( abnormal @ ( or1 @ ( h2 @ f ) ) ) ) | ( ~( abnormal @ ( or1 @ f ) ) )),
% 0.58/0.85 inference('cnf.neg', [status(esa)], [diagnosis_or1_or1h2])).
% 0.58/0.85 thf(zip_derived_cl61, plain,
% 0.58/0.85 ((~ (abnormal @ (or1 @ (h2 @ f))) | ~ (abnormal @ (or1 @ f)))),
% 0.58/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.58/0.85 thf(f_isa_fulladder, axiom, (fulladder @ f)).
% 0.58/0.85 thf(zip_derived_cl51, plain, ( (fulladder @ f)),
% 0.58/0.85 inference('cnf', [status(esa)], [f_isa_fulladder])).
% 0.58/0.85 thf(fulladder_or1, axiom,
% 0.58/0.85 (( ~( fulladder @ X ) ) | ( logic_or @ ( or1 @ X ) ))).
% 0.58/0.85 thf(zip_derived_cl42, plain,
% 0.58/0.85 (![X0 : $i]: (~ (fulladder @ X0) | (logic_or @ (or1 @ X0)))),
% 0.58/0.85 inference('cnf', [status(esa)], [fulladder_or1])).
% 0.58/0.85 thf(or_ok_or_abnormal, axiom,
% 0.58/0.85 (( ~( logic_or @ K ) ) | ( or_ok @ K ) | ( abnormal @ K ))).
% 0.58/0.85 thf(zip_derived_cl20, plain,
% 0.58/0.85 (![X0 : $i]: (~ (logic_or @ X0) | (or_ok @ X0) | (abnormal @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [or_ok_or_abnormal])).
% 0.58/0.85 thf(zip_derived_cl66, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (fulladder @ X0) | (abnormal @ (or1 @ X0)) | (or_ok @ (or1 @ X0)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl42, zip_derived_cl20])).
% 0.58/0.85 thf(zip_derived_cl110, plain,
% 0.58/0.85 (( (or_ok @ (or1 @ f)) | (abnormal @ (or1 @ f)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl66])).
% 0.58/0.85 thf(or_0_01, axiom,
% 0.58/0.85 (( ~( or_ok @ K ) ) | ( ~( zero @ ( out1 @ K ) ) ) | ( zero @ ( in2 @ K ) ))).
% 0.58/0.85 thf(zip_derived_cl18, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (or_ok @ X0) | ~ (zero @ (out1 @ X0)) | (zero @ (in2 @ X0)))),
% 0.58/0.85 inference('cnf', [status(esa)], [or_0_01])).
% 0.58/0.85 thf(zip_derived_cl123, plain,
% 0.58/0.85 (( (abnormal @ (or1 @ f))
% 0.58/0.85 | (zero @ (in2 @ (or1 @ f)))
% 0.58/0.85 | ~ (zero @ (out1 @ (or1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl110, zip_derived_cl18])).
% 0.58/0.85 thf(zip_derived_cl51, plain, ( (fulladder @ f)),
% 0.58/0.85 inference('cnf', [status(esa)], [f_isa_fulladder])).
% 0.58/0.85 thf(fulladder_connection_outc_out1or1, axiom,
% 0.58/0.85 (( ~( fulladder @ X ) ) |
% 0.58/0.85 ( connection @ ( outc @ X ) @ ( out1 @ ( or1 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl50, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (fulladder @ X0)
% 0.58/0.85 | (connection @ (outc @ X0) @ (out1 @ (or1 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [fulladder_connection_outc_out1or1])).
% 0.58/0.85 thf(zip_derived_cl109, plain,
% 0.58/0.85 ( (connection @ (outc @ f) @ (out1 @ (or1 @ f)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl50])).
% 0.58/0.85 thf(value_propagation_zero1, axiom,
% 0.58/0.85 (( ~( connection @ P1 @ P2 ) ) | ( ~( zero @ P1 ) ) | ( zero @ P2 ))).
% 0.58/0.85 thf(zip_derived_cl0, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (zero @ X0) | (zero @ X1))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_zero1])).
% 0.58/0.85 thf(zip_derived_cl291, plain,
% 0.58/0.85 (( (zero @ (out1 @ (or1 @ f))) | ~ (zero @ (outc @ f)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl109, zip_derived_cl0])).
% 0.58/0.85 thf(outc_0, axiom, (zero @ ( outc @ f ))).
% 0.58/0.85 thf(zip_derived_cl56, plain, ( (zero @ (outc @ f))),
% 0.58/0.85 inference('cnf', [status(esa)], [outc_0])).
% 0.58/0.85 thf(zip_derived_cl385, plain, ( (zero @ (out1 @ (or1 @ f)))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl291, zip_derived_cl56])).
% 0.58/0.85 thf(zip_derived_cl387, plain,
% 0.58/0.85 (( (abnormal @ (or1 @ f)) | (zero @ (in2 @ (or1 @ f))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl123, zip_derived_cl385])).
% 0.58/0.85 thf(zip_derived_cl51, plain, ( (fulladder @ f)),
% 0.58/0.85 inference('cnf', [status(esa)], [f_isa_fulladder])).
% 0.58/0.85 thf(fulladder_connection_outch1_in2or1, axiom,
% 0.58/0.85 (( ~( fulladder @ X ) ) |
% 0.58/0.85 ( connection @ ( outc @ ( h1 @ X ) ) @ ( in2 @ ( or1 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl44, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (fulladder @ X0)
% 0.58/0.85 | (connection @ (outc @ (h1 @ X0)) @ (in2 @ (or1 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [fulladder_connection_outch1_in2or1])).
% 0.58/0.85 thf(zip_derived_cl103, plain,
% 0.58/0.85 ( (connection @ (outc @ (h1 @ f)) @ (in2 @ (or1 @ f)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl44])).
% 0.58/0.85 thf(value_propagation_zero2, axiom,
% 0.58/0.85 (( ~( connection @ P1 @ P2 ) ) | ( ~( zero @ P2 ) ) | ( zero @ P1 ))).
% 0.58/0.85 thf(zip_derived_cl2, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (zero @ X1) | (zero @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_zero2])).
% 0.58/0.85 thf(zip_derived_cl269, plain,
% 0.58/0.85 (( (zero @ (outc @ (h1 @ f))) | ~ (zero @ (in2 @ (or1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl103, zip_derived_cl2])).
% 0.58/0.85 thf(zip_derived_cl395, plain,
% 0.58/0.85 (( (abnormal @ (or1 @ f)) | (zero @ (outc @ (h1 @ f))))),
% 0.58/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl387, zip_derived_cl269])).
% 0.58/0.85 thf(zip_derived_cl51, plain, ( (fulladder @ f)),
% 0.58/0.85 inference('cnf', [status(esa)], [f_isa_fulladder])).
% 0.58/0.85 thf(fulladder_halfadder1, axiom,
% 0.58/0.85 (( ~( fulladder @ X ) ) | ( halfadder @ ( h1 @ X ) ))).
% 0.58/0.85 thf(zip_derived_cl40, plain,
% 0.58/0.85 (![X0 : $i]: (~ (fulladder @ X0) | (halfadder @ (h1 @ X0)))),
% 0.58/0.85 inference('cnf', [status(esa)], [fulladder_halfadder1])).
% 0.58/0.85 thf(zip_derived_cl100, plain, ( (halfadder @ (h1 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl40])).
% 0.58/0.85 thf(halfadder_connection_outc_out1and2, axiom,
% 0.58/0.85 (( ~( halfadder @ X ) ) |
% 0.58/0.85 ( connection @ ( outc @ X ) @ ( out1 @ ( and2 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl36, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0)
% 0.58/0.85 | (connection @ (outc @ X0) @ (out1 @ (and2 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_connection_outc_out1and2])).
% 0.58/0.85 thf(zip_derived_cl198, plain,
% 0.58/0.85 ( (connection @ (outc @ (h1 @ f)) @ (out1 @ (and2 @ (h1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl100, zip_derived_cl36])).
% 0.58/0.85 thf(zip_derived_cl0, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (zero @ X0) | (zero @ X1))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_zero1])).
% 0.58/0.85 thf(zip_derived_cl315, plain,
% 0.58/0.85 (( (zero @ (out1 @ (and2 @ (h1 @ f)))) | ~ (zero @ (outc @ (h1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl198, zip_derived_cl0])).
% 0.58/0.85 thf(zip_derived_cl407, plain,
% 0.58/0.85 (( (abnormal @ (or1 @ f)) | (zero @ (out1 @ (and2 @ (h1 @ f)))))),
% 0.58/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl395, zip_derived_cl315])).
% 0.58/0.85 thf(unique_value, axiom, (( ~( zero @ P ) ) | ( ~( one @ P ) ))).
% 0.58/0.85 thf(zip_derived_cl4, plain, (![X0 : $i]: (~ (zero @ X0) | ~ (one @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [unique_value])).
% 0.58/0.85 thf(zip_derived_cl408, plain,
% 0.58/0.85 (( (abnormal @ (or1 @ f)) | ~ (one @ (out1 @ (and2 @ (h1 @ f)))))),
% 0.58/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl407, zip_derived_cl4])).
% 0.58/0.85 thf(zip_derived_cl100, plain, ( (halfadder @ (h1 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl40])).
% 0.58/0.85 thf(halfadder_and2, axiom,
% 0.58/0.85 (( ~( halfadder @ X ) ) | ( logic_and @ ( and2 @ X ) ))).
% 0.58/0.85 thf(zip_derived_cl28, plain,
% 0.58/0.85 (![X0 : $i]: (~ (halfadder @ X0) | (logic_and @ (and2 @ X0)))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_and2])).
% 0.58/0.85 thf(and_ok_or_abnormal, axiom,
% 0.58/0.85 (( ~( logic_and @ K ) ) | ( and_ok @ K ) | ( abnormal @ K ))).
% 0.58/0.85 thf(zip_derived_cl12, plain,
% 0.58/0.85 (![X0 : $i]: (~ (logic_and @ X0) | (and_ok @ X0) | (abnormal @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [and_ok_or_abnormal])).
% 0.58/0.85 thf(zip_derived_cl64, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0)
% 0.58/0.85 | (abnormal @ (and2 @ X0))
% 0.58/0.85 | (and_ok @ (and2 @ X0)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl28, zip_derived_cl12])).
% 0.58/0.85 thf(zip_derived_cl203, plain,
% 0.58/0.85 (( (and_ok @ (and2 @ (h1 @ f))) | (abnormal @ (and2 @ (h1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl100, zip_derived_cl64])).
% 0.58/0.85 thf(and_11_1, axiom,
% 0.58/0.85 (( ~( and_ok @ K ) ) | ( ~( one @ ( in1 @ K ) ) ) |
% 0.58/0.85 ( ~( one @ ( in2 @ K ) ) ) | ( one @ ( out1 @ K ) ))).
% 0.58/0.85 thf(zip_derived_cl7, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (and_ok @ X0)
% 0.58/0.85 | ~ (one @ (in1 @ X0))
% 0.58/0.85 | ~ (one @ (in2 @ X0))
% 0.58/0.85 | (one @ (out1 @ X0)))),
% 0.58/0.85 inference('cnf', [status(esa)], [and_11_1])).
% 0.58/0.85 thf(zip_derived_cl244, plain,
% 0.58/0.85 (( (abnormal @ (and2 @ (h1 @ f)))
% 0.58/0.85 | (one @ (out1 @ (and2 @ (h1 @ f))))
% 0.58/0.85 | ~ (one @ (in2 @ (and2 @ (h1 @ f))))
% 0.58/0.85 | ~ (one @ (in1 @ (and2 @ (h1 @ f)))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl203, zip_derived_cl7])).
% 0.58/0.85 thf(zip_derived_cl100, plain, ( (halfadder @ (h1 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl40])).
% 0.58/0.85 thf(halfadder_connection_in2_in2and2, axiom,
% 0.58/0.85 (( ~( halfadder @ X ) ) |
% 0.58/0.85 ( connection @ ( in2 @ X ) @ ( in2 @ ( and2 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl34, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0) | (connection @ (in2 @ X0) @ (in2 @ (and2 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_connection_in2_in2and2])).
% 0.58/0.85 thf(zip_derived_cl196, plain,
% 0.58/0.85 ( (connection @ (in2 @ (h1 @ f)) @ (in2 @ (and2 @ (h1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl100, zip_derived_cl34])).
% 0.58/0.85 thf(value_propagation_one1, axiom,
% 0.58/0.85 (( ~( connection @ P1 @ P2 ) ) | ( ~( one @ P1 ) ) | ( one @ P2 ))).
% 0.58/0.85 thf(zip_derived_cl1, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (one @ X0) | (one @ X1))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_one1])).
% 0.58/0.85 thf(zip_derived_cl308, plain,
% 0.58/0.85 (( (one @ (in2 @ (and2 @ (h1 @ f)))) | ~ (one @ (in2 @ (h1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl196, zip_derived_cl1])).
% 0.58/0.85 thf(zip_derived_cl51, plain, ( (fulladder @ f)),
% 0.58/0.85 inference('cnf', [status(esa)], [f_isa_fulladder])).
% 0.58/0.85 thf(fulladder_connection_inc_in2h1, axiom,
% 0.58/0.85 (( ~( fulladder @ X ) ) |
% 0.58/0.85 ( connection @ ( inc @ X ) @ ( in2 @ ( h1 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl48, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (fulladder @ X0) | (connection @ (inc @ X0) @ (in2 @ (h1 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [fulladder_connection_inc_in2h1])).
% 0.58/0.85 thf(zip_derived_cl107, plain, ( (connection @ (inc @ f) @ (in2 @ (h1 @ f)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl48])).
% 0.58/0.85 thf(zip_derived_cl1, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (one @ X0) | (one @ X1))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_one1])).
% 0.58/0.85 thf(zip_derived_cl284, plain,
% 0.58/0.85 (( (one @ (in2 @ (h1 @ f))) | ~ (one @ (inc @ f)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl107, zip_derived_cl1])).
% 0.58/0.85 thf(inc_1, axiom, (one @ ( inc @ f ))).
% 0.58/0.85 thf(zip_derived_cl54, plain, ( (one @ (inc @ f))),
% 0.58/0.85 inference('cnf', [status(esa)], [inc_1])).
% 0.58/0.85 thf(zip_derived_cl378, plain, ( (one @ (in2 @ (h1 @ f)))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl284, zip_derived_cl54])).
% 0.58/0.85 thf(zip_derived_cl406, plain, ( (one @ (in2 @ (and2 @ (h1 @ f))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl308, zip_derived_cl378])).
% 0.58/0.85 thf(zip_derived_cl100, plain, ( (halfadder @ (h1 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl40])).
% 0.58/0.85 thf(halfadder_connection_in1_in1and2, axiom,
% 0.58/0.85 (( ~( halfadder @ X ) ) |
% 0.58/0.85 ( connection @ ( in1 @ X ) @ ( in1 @ ( and2 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl33, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0) | (connection @ (in1 @ X0) @ (in1 @ (and2 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_connection_in1_in1and2])).
% 0.58/0.85 thf(zip_derived_cl195, plain,
% 0.58/0.85 ( (connection @ (in1 @ (h1 @ f)) @ (in1 @ (and2 @ (h1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl100, zip_derived_cl33])).
% 0.58/0.85 thf(zip_derived_cl1, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (one @ X0) | (one @ X1))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_one1])).
% 0.58/0.85 thf(zip_derived_cl304, plain,
% 0.58/0.85 (( (one @ (in1 @ (and2 @ (h1 @ f)))) | ~ (one @ (in1 @ (h1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl195, zip_derived_cl1])).
% 0.58/0.85 thf(zip_derived_cl51, plain, ( (fulladder @ f)),
% 0.58/0.85 inference('cnf', [status(esa)], [f_isa_fulladder])).
% 0.58/0.85 thf(fulladder_connection_in2_in1h1, axiom,
% 0.58/0.85 (( ~( fulladder @ X ) ) |
% 0.58/0.85 ( connection @ ( in2 @ X ) @ ( in1 @ ( h1 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl47, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (fulladder @ X0) | (connection @ (in2 @ X0) @ (in1 @ (h1 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [fulladder_connection_in2_in1h1])).
% 0.58/0.85 thf(zip_derived_cl106, plain, ( (connection @ (in2 @ f) @ (in1 @ (h1 @ f)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl47])).
% 0.58/0.85 thf(zip_derived_cl1, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (one @ X0) | (one @ X1))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_one1])).
% 0.58/0.85 thf(zip_derived_cl280, plain,
% 0.58/0.85 (( (one @ (in1 @ (h1 @ f))) | ~ (one @ (in2 @ f)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl106, zip_derived_cl1])).
% 0.58/0.85 thf(in2_0, axiom, (one @ ( in2 @ f ))).
% 0.58/0.85 thf(zip_derived_cl53, plain, ( (one @ (in2 @ f))),
% 0.58/0.85 inference('cnf', [status(esa)], [in2_0])).
% 0.58/0.85 thf(zip_derived_cl375, plain, ( (one @ (in1 @ (h1 @ f)))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl280, zip_derived_cl53])).
% 0.58/0.85 thf(zip_derived_cl403, plain, ( (one @ (in1 @ (and2 @ (h1 @ f))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl304, zip_derived_cl375])).
% 0.58/0.85 thf(zip_derived_cl435, plain,
% 0.58/0.85 (( (abnormal @ (and2 @ (h1 @ f))) | (one @ (out1 @ (and2 @ (h1 @ f)))))),
% 0.58/0.85 inference('demod', [status(thm)],
% 0.58/0.85 [zip_derived_cl244, zip_derived_cl406, zip_derived_cl403])).
% 0.58/0.85 thf(diagnosis_and2h1, conjecture, (abnormal @ ( and2 @ ( h1 @ f ) ))).
% 0.58/0.85 thf(zf_stmt_1, negated_conjecture, (~( abnormal @ ( and2 @ ( h1 @ f ) ) )),
% 0.58/0.85 inference('cnf.neg', [status(esa)], [diagnosis_and2h1])).
% 0.58/0.85 thf(zip_derived_cl57, plain, (~ (abnormal @ (and2 @ (h1 @ f)))),
% 0.58/0.85 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.58/0.85 thf(zip_derived_cl436, plain, ( (one @ (out1 @ (and2 @ (h1 @ f))))),
% 0.58/0.85 inference('clc', [status(thm)], [zip_derived_cl435, zip_derived_cl57])).
% 0.58/0.85 thf(zip_derived_cl439, plain, ( (abnormal @ (or1 @ f))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl408, zip_derived_cl436])).
% 0.58/0.85 thf(zip_derived_cl443, plain, (~ (abnormal @ (or1 @ (h2 @ f)))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl61, zip_derived_cl439])).
% 0.58/0.85 thf(zip_derived_cl51, plain, ( (fulladder @ f)),
% 0.58/0.85 inference('cnf', [status(esa)], [f_isa_fulladder])).
% 0.58/0.85 thf(fulladder_halfadder2, axiom,
% 0.58/0.85 (( ~( fulladder @ X ) ) | ( halfadder @ ( h2 @ X ) ))).
% 0.58/0.85 thf(zip_derived_cl41, plain,
% 0.58/0.85 (![X0 : $i]: (~ (fulladder @ X0) | (halfadder @ (h2 @ X0)))),
% 0.58/0.85 inference('cnf', [status(esa)], [fulladder_halfadder2])).
% 0.58/0.85 thf(zip_derived_cl101, plain, ( (halfadder @ (h2 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl41])).
% 0.58/0.85 thf(halfadder_or1, axiom,
% 0.58/0.85 (( ~( halfadder @ X ) ) | ( logic_or @ ( or1 @ X ) ))).
% 0.58/0.85 thf(zip_derived_cl30, plain,
% 0.58/0.85 (![X0 : $i]: (~ (halfadder @ X0) | (logic_or @ (or1 @ X0)))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_or1])).
% 0.58/0.85 thf(zip_derived_cl20, plain,
% 0.58/0.85 (![X0 : $i]: (~ (logic_or @ X0) | (or_ok @ X0) | (abnormal @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [or_ok_or_abnormal])).
% 0.58/0.85 thf(zip_derived_cl65, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0) | (abnormal @ (or1 @ X0)) | (or_ok @ (or1 @ X0)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl30, zip_derived_cl20])).
% 0.58/0.85 thf(or_1_11, axiom,
% 0.58/0.85 (( ~( or_ok @ K ) ) | ( ~( one @ ( out1 @ K ) ) ) |
% 0.58/0.85 ( one @ ( in1 @ K ) ) | ( one @ ( in2 @ K ) ))).
% 0.58/0.85 thf(zip_derived_cl16, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (or_ok @ X0)
% 0.58/0.85 | ~ (one @ (out1 @ X0))
% 0.58/0.85 | (one @ (in1 @ X0))
% 0.58/0.85 | (one @ (in2 @ X0)))),
% 0.58/0.85 inference('cnf', [status(esa)], [or_1_11])).
% 0.58/0.85 thf(zip_derived_cl114, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 ( (abnormal @ (or1 @ X0))
% 0.58/0.85 | ~ (halfadder @ X0)
% 0.58/0.85 | (one @ (in2 @ (or1 @ X0)))
% 0.58/0.85 | (one @ (in1 @ (or1 @ X0)))
% 0.58/0.85 | ~ (one @ (out1 @ (or1 @ X0))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl65, zip_derived_cl16])).
% 0.58/0.85 thf(zip_derived_cl232, plain,
% 0.58/0.85 ((~ (one @ (out1 @ (or1 @ (h2 @ f))))
% 0.58/0.85 | (one @ (in1 @ (or1 @ (h2 @ f))))
% 0.58/0.85 | (one @ (in2 @ (or1 @ (h2 @ f))))
% 0.58/0.85 | (abnormal @ (or1 @ (h2 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl101, zip_derived_cl114])).
% 0.58/0.85 thf(zip_derived_cl101, plain, ( (halfadder @ (h2 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl41])).
% 0.58/0.85 thf(halfadder_connection_in1_in1or1, axiom,
% 0.58/0.85 (( ~( halfadder @ X ) ) |
% 0.58/0.85 ( connection @ ( in1 @ X ) @ ( in1 @ ( or1 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl31, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0) | (connection @ (in1 @ X0) @ (in1 @ (or1 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_connection_in1_in1or1])).
% 0.58/0.85 thf(zip_derived_cl214, plain,
% 0.58/0.85 ( (connection @ (in1 @ (h2 @ f)) @ (in1 @ (or1 @ (h2 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl101, zip_derived_cl31])).
% 0.58/0.85 thf(zip_derived_cl0, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (zero @ X0) | (zero @ X1))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_zero1])).
% 0.58/0.85 thf(zip_derived_cl331, plain,
% 0.58/0.85 (( (zero @ (in1 @ (or1 @ (h2 @ f)))) | ~ (zero @ (in1 @ (h2 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl214, zip_derived_cl0])).
% 0.58/0.85 thf(zip_derived_cl51, plain, ( (fulladder @ f)),
% 0.58/0.85 inference('cnf', [status(esa)], [f_isa_fulladder])).
% 0.58/0.85 thf(fulladder_connection_in1_in1h2, axiom,
% 0.58/0.85 (( ~( fulladder @ X ) ) |
% 0.58/0.85 ( connection @ ( in1 @ X ) @ ( in1 @ ( h2 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl46, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (fulladder @ X0) | (connection @ (in1 @ X0) @ (in1 @ (h2 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [fulladder_connection_in1_in1h2])).
% 0.58/0.85 thf(zip_derived_cl105, plain, ( (connection @ (in1 @ f) @ (in1 @ (h2 @ f)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl46])).
% 0.58/0.85 thf(zip_derived_cl0, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (zero @ X0) | (zero @ X1))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_zero1])).
% 0.58/0.85 thf(zip_derived_cl275, plain,
% 0.58/0.85 (( (zero @ (in1 @ (h2 @ f))) | ~ (zero @ (in1 @ f)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl105, zip_derived_cl0])).
% 0.58/0.85 thf(in1_1, axiom, (zero @ ( in1 @ f ))).
% 0.58/0.85 thf(zip_derived_cl52, plain, ( (zero @ (in1 @ f))),
% 0.58/0.85 inference('cnf', [status(esa)], [in1_1])).
% 0.58/0.85 thf(zip_derived_cl369, plain, ( (zero @ (in1 @ (h2 @ f)))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl275, zip_derived_cl52])).
% 0.58/0.85 thf(zip_derived_cl411, plain, ( (zero @ (in1 @ (or1 @ (h2 @ f))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl331, zip_derived_cl369])).
% 0.58/0.85 thf(zip_derived_cl4, plain, (![X0 : $i]: (~ (zero @ X0) | ~ (one @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [unique_value])).
% 0.58/0.85 thf(zip_derived_cl412, plain, (~ (one @ (in1 @ (or1 @ (h2 @ f))))),
% 0.58/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl411, zip_derived_cl4])).
% 0.58/0.85 thf(zip_derived_cl417, plain,
% 0.58/0.85 ((~ (one @ (out1 @ (or1 @ (h2 @ f))))
% 0.58/0.85 | (one @ (in2 @ (or1 @ (h2 @ f))))
% 0.58/0.85 | (abnormal @ (or1 @ (h2 @ f))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl232, zip_derived_cl412])).
% 0.58/0.85 thf(zip_derived_cl101, plain, ( (halfadder @ (h2 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl41])).
% 0.58/0.85 thf(halfadder_connection_in2_in2or1, axiom,
% 0.58/0.85 (( ~( halfadder @ X ) ) |
% 0.58/0.85 ( connection @ ( in2 @ X ) @ ( in2 @ ( or1 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl32, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0) | (connection @ (in2 @ X0) @ (in2 @ (or1 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_connection_in2_in2or1])).
% 0.58/0.85 thf(zip_derived_cl215, plain,
% 0.58/0.85 ( (connection @ (in2 @ (h2 @ f)) @ (in2 @ (or1 @ (h2 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl101, zip_derived_cl32])).
% 0.58/0.85 thf(value_propagation_one2, axiom,
% 0.58/0.85 (( ~( connection @ P1 @ P2 ) ) | ( ~( one @ P2 ) ) | ( one @ P1 ))).
% 0.58/0.85 thf(zip_derived_cl3, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (one @ X1) | (one @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_one2])).
% 0.58/0.85 thf(zip_derived_cl338, plain,
% 0.58/0.85 (( (one @ (in2 @ (h2 @ f))) | ~ (one @ (in2 @ (or1 @ (h2 @ f)))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl215, zip_derived_cl3])).
% 0.58/0.85 thf(zip_derived_cl51, plain, ( (fulladder @ f)),
% 0.58/0.85 inference('cnf', [status(esa)], [f_isa_fulladder])).
% 0.58/0.85 thf(fulladder_connection_outsh1_in2h2, axiom,
% 0.58/0.85 (( ~( fulladder @ X ) ) |
% 0.58/0.85 ( connection @ ( outs @ ( h1 @ X ) ) @ ( in2 @ ( h2 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl43, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (fulladder @ X0)
% 0.58/0.85 | (connection @ (outs @ (h1 @ X0)) @ (in2 @ (h2 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [fulladder_connection_outsh1_in2h2])).
% 0.58/0.85 thf(zip_derived_cl102, plain,
% 0.58/0.85 ( (connection @ (outs @ (h1 @ f)) @ (in2 @ (h2 @ f)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl43])).
% 0.58/0.85 thf(zip_derived_cl0, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (zero @ X0) | (zero @ X1))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_zero1])).
% 0.58/0.85 thf(zip_derived_cl263, plain,
% 0.58/0.85 (( (zero @ (in2 @ (h2 @ f))) | ~ (zero @ (outs @ (h1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl102, zip_derived_cl0])).
% 0.58/0.85 thf(zip_derived_cl100, plain, ( (halfadder @ (h1 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl40])).
% 0.58/0.85 thf(halfadder_connection_outs_out1and1, axiom,
% 0.58/0.85 (( ~( halfadder @ X ) ) |
% 0.58/0.85 ( connection @ ( outs @ X ) @ ( out1 @ ( and1 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl35, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0)
% 0.58/0.85 | (connection @ (outs @ X0) @ (out1 @ (and1 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_connection_outs_out1and1])).
% 0.58/0.85 thf(zip_derived_cl197, plain,
% 0.58/0.85 ( (connection @ (outs @ (h1 @ f)) @ (out1 @ (and1 @ (h1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl100, zip_derived_cl35])).
% 0.58/0.85 thf(zip_derived_cl2, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (zero @ X1) | (zero @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_zero2])).
% 0.58/0.85 thf(zip_derived_cl313, plain,
% 0.58/0.85 (( (zero @ (outs @ (h1 @ f))) | ~ (zero @ (out1 @ (and1 @ (h1 @ f)))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl197, zip_derived_cl2])).
% 0.58/0.85 thf(zip_derived_cl100, plain, ( (halfadder @ (h1 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl40])).
% 0.58/0.85 thf(halfadder_and1, axiom,
% 0.58/0.85 (( ~( halfadder @ X ) ) | ( logic_and @ ( and1 @ X ) ))).
% 0.58/0.85 thf(zip_derived_cl27, plain,
% 0.58/0.85 (![X0 : $i]: (~ (halfadder @ X0) | (logic_and @ (and1 @ X0)))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_and1])).
% 0.58/0.85 thf(zip_derived_cl12, plain,
% 0.58/0.85 (![X0 : $i]: (~ (logic_and @ X0) | (and_ok @ X0) | (abnormal @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [and_ok_or_abnormal])).
% 0.58/0.85 thf(zip_derived_cl63, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0)
% 0.58/0.85 | (abnormal @ (and1 @ X0))
% 0.58/0.85 | (and_ok @ (and1 @ X0)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl27, zip_derived_cl12])).
% 0.58/0.85 thf(zip_derived_cl202, plain,
% 0.58/0.85 (( (and_ok @ (and1 @ (h1 @ f))) | (abnormal @ (and1 @ (h1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl100, zip_derived_cl63])).
% 0.58/0.85 thf(and_x0_0, axiom,
% 0.58/0.85 (( ~( and_ok @ K ) ) | ( ~( zero @ ( in2 @ K ) ) ) |
% 0.58/0.85 ( zero @ ( out1 @ K ) ))).
% 0.58/0.85 thf(zip_derived_cl6, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (and_ok @ X0) | ~ (zero @ (in2 @ X0)) | (zero @ (out1 @ X0)))),
% 0.58/0.85 inference('cnf', [status(esa)], [and_x0_0])).
% 0.58/0.85 thf(zip_derived_cl236, plain,
% 0.58/0.85 (( (abnormal @ (and1 @ (h1 @ f)))
% 0.58/0.85 | (zero @ (out1 @ (and1 @ (h1 @ f))))
% 0.58/0.85 | ~ (zero @ (in2 @ (and1 @ (h1 @ f)))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl202, zip_derived_cl6])).
% 0.58/0.85 thf(diagnosis_or1_and1h1, conjecture,
% 0.58/0.85 (~( ( ~( abnormal @ ( and1 @ ( h1 @ f ) ) ) ) |
% 0.58/0.85 ( ~( abnormal @ ( or1 @ f ) ) ) ))).
% 0.58/0.85 thf(zf_stmt_2, negated_conjecture,
% 0.58/0.85 (( ~( abnormal @ ( and1 @ ( h1 @ f ) ) ) ) |
% 0.58/0.85 ( ~( abnormal @ ( or1 @ f ) ) )),
% 0.58/0.85 inference('cnf.neg', [status(esa)], [diagnosis_or1_and1h1])).
% 0.58/0.85 thf(zip_derived_cl58, plain,
% 0.58/0.85 ((~ (abnormal @ (and1 @ (h1 @ f))) | ~ (abnormal @ (or1 @ f)))),
% 0.58/0.85 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.58/0.85 thf(zip_derived_cl439, plain, ( (abnormal @ (or1 @ f))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl408, zip_derived_cl436])).
% 0.58/0.85 thf(zip_derived_cl440, plain, (~ (abnormal @ (and1 @ (h1 @ f)))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl58, zip_derived_cl439])).
% 0.58/0.85 thf(zip_derived_cl444, plain,
% 0.58/0.85 (( (zero @ (out1 @ (and1 @ (h1 @ f))))
% 0.58/0.85 | ~ (zero @ (in2 @ (and1 @ (h1 @ f)))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl236, zip_derived_cl440])).
% 0.58/0.85 thf(zip_derived_cl100, plain, ( (halfadder @ (h1 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl40])).
% 0.58/0.85 thf(halfadder_connection_out1not1_in2and1, axiom,
% 0.58/0.85 (( ~( halfadder @ X ) ) |
% 0.58/0.85 ( connection @ ( out1 @ ( not1 @ X ) ) @ ( in2 @ ( and1 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl39, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0)
% 0.58/0.85 | (connection @ (out1 @ (not1 @ X0)) @ (in2 @ (and1 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_connection_out1not1_in2and1])).
% 0.58/0.85 thf(zip_derived_cl201, plain,
% 0.58/0.85 ( (connection @ (out1 @ (not1 @ (h1 @ f))) @ (in2 @ (and1 @ (h1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl100, zip_derived_cl39])).
% 0.58/0.85 thf(zip_derived_cl0, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (zero @ X0) | (zero @ X1))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_zero1])).
% 0.58/0.85 thf(zip_derived_cl327, plain,
% 0.58/0.85 (( (zero @ (in2 @ (and1 @ (h1 @ f))))
% 0.58/0.85 | ~ (zero @ (out1 @ (not1 @ (h1 @ f)))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl201, zip_derived_cl0])).
% 0.58/0.85 thf(zip_derived_cl100, plain, ( (halfadder @ (h1 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl40])).
% 0.58/0.85 thf(halfadder_not1, axiom,
% 0.58/0.85 (( ~( halfadder @ X ) ) | ( logic_not @ ( not1 @ X ) ))).
% 0.58/0.85 thf(zip_derived_cl29, plain,
% 0.58/0.85 (![X0 : $i]: (~ (halfadder @ X0) | (logic_not @ (not1 @ X0)))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_not1])).
% 0.58/0.85 thf(not_ok_or_abnormal, axiom,
% 0.58/0.85 (( ~( logic_not @ K ) ) | ( not_ok @ K ) | ( abnormal @ K ))).
% 0.58/0.85 thf(zip_derived_cl26, plain,
% 0.58/0.85 (![X0 : $i]: (~ (logic_not @ X0) | (not_ok @ X0) | (abnormal @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [not_ok_or_abnormal])).
% 0.58/0.85 thf(zip_derived_cl62, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0)
% 0.58/0.85 | (abnormal @ (not1 @ X0))
% 0.58/0.85 | (not_ok @ (not1 @ X0)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl29, zip_derived_cl26])).
% 0.58/0.85 thf(not_1_0_fw, axiom,
% 0.58/0.85 (( ~( not_ok @ K ) ) | ( ~( one @ ( in1 @ K ) ) ) | ( zero @ ( out1 @ K ) ))).
% 0.58/0.85 thf(zip_derived_cl22, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (not_ok @ X0) | ~ (one @ (in1 @ X0)) | (zero @ (out1 @ X0)))),
% 0.58/0.85 inference('cnf', [status(esa)], [not_1_0_fw])).
% 0.58/0.85 thf(zip_derived_cl68, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 ( (abnormal @ (not1 @ X0))
% 0.58/0.85 | ~ (halfadder @ X0)
% 0.58/0.85 | (zero @ (out1 @ (not1 @ X0)))
% 0.58/0.85 | ~ (one @ (in1 @ (not1 @ X0))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl62, zip_derived_cl22])).
% 0.58/0.85 thf(zip_derived_cl205, plain,
% 0.58/0.85 ((~ (one @ (in1 @ (not1 @ (h1 @ f))))
% 0.58/0.85 | (zero @ (out1 @ (not1 @ (h1 @ f))))
% 0.58/0.85 | (abnormal @ (not1 @ (h1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl100, zip_derived_cl68])).
% 0.58/0.85 thf(zip_derived_cl100, plain, ( (halfadder @ (h1 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl40])).
% 0.58/0.85 thf(halfadder_connection_out1and2_in1not1, axiom,
% 0.58/0.85 (( ~( halfadder @ X ) ) |
% 0.58/0.85 ( connection @ ( out1 @ ( and2 @ X ) ) @ ( in1 @ ( not1 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl38, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0)
% 0.58/0.85 | (connection @ (out1 @ (and2 @ X0)) @ (in1 @ (not1 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_connection_out1and2_in1not1])).
% 0.58/0.85 thf(zip_derived_cl200, plain,
% 0.58/0.85 ( (connection @ (out1 @ (and2 @ (h1 @ f))) @ (in1 @ (not1 @ (h1 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl100, zip_derived_cl38])).
% 0.58/0.85 thf(zip_derived_cl1, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (one @ X0) | (one @ X1))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_one1])).
% 0.58/0.85 thf(zip_derived_cl324, plain,
% 0.58/0.85 (( (one @ (in1 @ (not1 @ (h1 @ f))))
% 0.58/0.85 | ~ (one @ (out1 @ (and2 @ (h1 @ f)))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl200, zip_derived_cl1])).
% 0.58/0.85 thf(zip_derived_cl436, plain, ( (one @ (out1 @ (and2 @ (h1 @ f))))),
% 0.58/0.85 inference('clc', [status(thm)], [zip_derived_cl435, zip_derived_cl57])).
% 0.58/0.85 thf(zip_derived_cl438, plain, ( (one @ (in1 @ (not1 @ (h1 @ f))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl324, zip_derived_cl436])).
% 0.58/0.85 thf(zip_derived_cl452, plain,
% 0.58/0.85 (( (zero @ (out1 @ (not1 @ (h1 @ f)))) | (abnormal @ (not1 @ (h1 @ f))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl205, zip_derived_cl438])).
% 0.58/0.85 thf(diagnosis_or1_not1h1, conjecture,
% 0.58/0.85 (~( ( ~( abnormal @ ( not1 @ ( h1 @ f ) ) ) ) |
% 0.58/0.85 ( ~( abnormal @ ( or1 @ f ) ) ) ))).
% 0.58/0.85 thf(zf_stmt_3, negated_conjecture,
% 0.58/0.85 (( ~( abnormal @ ( not1 @ ( h1 @ f ) ) ) ) |
% 0.58/0.85 ( ~( abnormal @ ( or1 @ f ) ) )),
% 0.58/0.85 inference('cnf.neg', [status(esa)], [diagnosis_or1_not1h1])).
% 0.58/0.85 thf(zip_derived_cl59, plain,
% 0.58/0.85 ((~ (abnormal @ (not1 @ (h1 @ f))) | ~ (abnormal @ (or1 @ f)))),
% 0.58/0.85 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.58/0.85 thf(zip_derived_cl439, plain, ( (abnormal @ (or1 @ f))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl408, zip_derived_cl436])).
% 0.58/0.85 thf(zip_derived_cl441, plain, (~ (abnormal @ (not1 @ (h1 @ f)))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl59, zip_derived_cl439])).
% 0.58/0.85 thf(zip_derived_cl453, plain, ( (zero @ (out1 @ (not1 @ (h1 @ f))))),
% 0.58/0.85 inference('clc', [status(thm)], [zip_derived_cl452, zip_derived_cl441])).
% 0.58/0.85 thf(zip_derived_cl454, plain, ( (zero @ (in2 @ (and1 @ (h1 @ f))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl327, zip_derived_cl453])).
% 0.58/0.85 thf(zip_derived_cl469, plain, ( (zero @ (out1 @ (and1 @ (h1 @ f))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl444, zip_derived_cl454])).
% 0.58/0.85 thf(zip_derived_cl470, plain, ( (zero @ (outs @ (h1 @ f)))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl313, zip_derived_cl469])).
% 0.58/0.85 thf(zip_derived_cl472, plain, ( (zero @ (in2 @ (h2 @ f)))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl263, zip_derived_cl470])).
% 0.58/0.85 thf(zip_derived_cl4, plain, (![X0 : $i]: (~ (zero @ X0) | ~ (one @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [unique_value])).
% 0.58/0.85 thf(zip_derived_cl479, plain, (~ (one @ (in2 @ (h2 @ f)))),
% 0.58/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl472, zip_derived_cl4])).
% 0.58/0.85 thf(zip_derived_cl480, plain, (~ (one @ (in2 @ (or1 @ (h2 @ f))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl338, zip_derived_cl479])).
% 0.58/0.85 thf(zip_derived_cl485, plain,
% 0.58/0.85 ((~ (one @ (out1 @ (or1 @ (h2 @ f)))) | (abnormal @ (or1 @ (h2 @ f))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl417, zip_derived_cl480])).
% 0.58/0.85 thf(zip_derived_cl101, plain, ( (halfadder @ (h2 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl41])).
% 0.58/0.85 thf(halfadder_connection_out1or1_in1_and1, axiom,
% 0.58/0.85 (( ~( halfadder @ X ) ) |
% 0.58/0.85 ( connection @ ( out1 @ ( or1 @ X ) ) @ ( in1 @ ( and1 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl37, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0)
% 0.58/0.85 | (connection @ (out1 @ (or1 @ X0)) @ (in1 @ (and1 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_connection_out1or1_in1_and1])).
% 0.58/0.85 thf(zip_derived_cl220, plain,
% 0.58/0.85 ( (connection @ (out1 @ (or1 @ (h2 @ f))) @ (in1 @ (and1 @ (h2 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl101, zip_derived_cl37])).
% 0.58/0.85 thf(zip_derived_cl3, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (one @ X1) | (one @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_one2])).
% 0.58/0.85 thf(zip_derived_cl358, plain,
% 0.58/0.85 (( (one @ (out1 @ (or1 @ (h2 @ f))))
% 0.58/0.85 | ~ (one @ (in1 @ (and1 @ (h2 @ f)))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl220, zip_derived_cl3])).
% 0.58/0.85 thf(zip_derived_cl101, plain, ( (halfadder @ (h2 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl41])).
% 0.58/0.85 thf(zip_derived_cl63, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0)
% 0.58/0.85 | (abnormal @ (and1 @ X0))
% 0.58/0.85 | (and_ok @ (and1 @ X0)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl27, zip_derived_cl12])).
% 0.58/0.85 thf(zip_derived_cl223, plain,
% 0.58/0.85 (( (and_ok @ (and1 @ (h2 @ f))) | (abnormal @ (and1 @ (h2 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl101, zip_derived_cl63])).
% 0.58/0.85 thf(and_1_1x, axiom,
% 0.58/0.85 (( ~( and_ok @ K ) ) | ( ~( one @ ( out1 @ K ) ) ) | ( one @ ( in1 @ K ) ))).
% 0.58/0.85 thf(zip_derived_cl9, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (and_ok @ X0) | ~ (one @ (out1 @ X0)) | (one @ (in1 @ X0)))),
% 0.58/0.85 inference('cnf', [status(esa)], [and_1_1x])).
% 0.58/0.85 thf(zip_derived_cl253, plain,
% 0.58/0.85 (( (abnormal @ (and1 @ (h2 @ f)))
% 0.58/0.85 | (one @ (in1 @ (and1 @ (h2 @ f))))
% 0.58/0.85 | ~ (one @ (out1 @ (and1 @ (h2 @ f)))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl223, zip_derived_cl9])).
% 0.58/0.85 thf(zip_derived_cl101, plain, ( (halfadder @ (h2 @ f))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl41])).
% 0.58/0.85 thf(zip_derived_cl35, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (halfadder @ X0)
% 0.58/0.85 | (connection @ (outs @ X0) @ (out1 @ (and1 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [halfadder_connection_outs_out1and1])).
% 0.58/0.85 thf(zip_derived_cl218, plain,
% 0.58/0.85 ( (connection @ (outs @ (h2 @ f)) @ (out1 @ (and1 @ (h2 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl101, zip_derived_cl35])).
% 0.58/0.85 thf(zip_derived_cl1, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (one @ X0) | (one @ X1))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_one1])).
% 0.58/0.85 thf(zip_derived_cl348, plain,
% 0.58/0.85 (( (one @ (out1 @ (and1 @ (h2 @ f)))) | ~ (one @ (outs @ (h2 @ f))))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl218, zip_derived_cl1])).
% 0.58/0.85 thf(zip_derived_cl51, plain, ( (fulladder @ f)),
% 0.58/0.85 inference('cnf', [status(esa)], [f_isa_fulladder])).
% 0.58/0.85 thf(fulladder_connection_outs_outsh2, axiom,
% 0.58/0.85 (( ~( fulladder @ X ) ) |
% 0.58/0.85 ( connection @ ( outs @ X ) @ ( outs @ ( h2 @ X ) ) ))).
% 0.58/0.85 thf(zip_derived_cl49, plain,
% 0.58/0.85 (![X0 : $i]:
% 0.58/0.85 (~ (fulladder @ X0) | (connection @ (outs @ X0) @ (outs @ (h2 @ X0))))),
% 0.58/0.85 inference('cnf', [status(esa)], [fulladder_connection_outs_outsh2])).
% 0.58/0.85 thf(zip_derived_cl108, plain,
% 0.58/0.85 ( (connection @ (outs @ f) @ (outs @ (h2 @ f)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl51, zip_derived_cl49])).
% 0.58/0.85 thf(zip_derived_cl1, plain,
% 0.58/0.85 (![X0 : $i, X1 : $i]:
% 0.58/0.85 (~ (connection @ X0 @ X1) | ~ (one @ X0) | (one @ X1))),
% 0.58/0.85 inference('cnf', [status(esa)], [value_propagation_one1])).
% 0.58/0.85 thf(zip_derived_cl288, plain,
% 0.58/0.85 (( (one @ (outs @ (h2 @ f))) | ~ (one @ (outs @ f)))),
% 0.58/0.85 inference('dp-resolution', [status(thm)],
% 0.58/0.85 [zip_derived_cl108, zip_derived_cl1])).
% 0.58/0.85 thf(outs_1, axiom, (one @ ( outs @ f ))).
% 0.58/0.85 thf(zip_derived_cl55, plain, ( (one @ (outs @ f))),
% 0.58/0.85 inference('cnf', [status(esa)], [outs_1])).
% 0.58/0.85 thf(zip_derived_cl379, plain, ( (one @ (outs @ (h2 @ f)))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl288, zip_derived_cl55])).
% 0.58/0.85 thf(zip_derived_cl425, plain, ( (one @ (out1 @ (and1 @ (h2 @ f))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl348, zip_derived_cl379])).
% 0.58/0.85 thf(zip_derived_cl474, plain,
% 0.58/0.85 (( (abnormal @ (and1 @ (h2 @ f))) | (one @ (in1 @ (and1 @ (h2 @ f)))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl253, zip_derived_cl425])).
% 0.58/0.85 thf(diagnosis_or1_and1h2, conjecture,
% 0.58/0.85 (~( ( ~( abnormal @ ( and1 @ ( h2 @ f ) ) ) ) |
% 0.58/0.85 ( ~( abnormal @ ( or1 @ f ) ) ) ))).
% 0.58/0.85 thf(zf_stmt_4, negated_conjecture,
% 0.58/0.85 (( ~( abnormal @ ( and1 @ ( h2 @ f ) ) ) ) |
% 0.58/0.85 ( ~( abnormal @ ( or1 @ f ) ) )),
% 0.58/0.85 inference('cnf.neg', [status(esa)], [diagnosis_or1_and1h2])).
% 0.58/0.85 thf(zip_derived_cl60, plain,
% 0.58/0.85 ((~ (abnormal @ (and1 @ (h2 @ f))) | ~ (abnormal @ (or1 @ f)))),
% 0.58/0.85 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.58/0.85 thf(zip_derived_cl439, plain, ( (abnormal @ (or1 @ f))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl408, zip_derived_cl436])).
% 0.58/0.85 thf(zip_derived_cl442, plain, (~ (abnormal @ (and1 @ (h2 @ f)))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl60, zip_derived_cl439])).
% 0.58/0.85 thf(zip_derived_cl475, plain, ( (one @ (in1 @ (and1 @ (h2 @ f))))),
% 0.58/0.85 inference('clc', [status(thm)], [zip_derived_cl474, zip_derived_cl442])).
% 0.58/0.85 thf(zip_derived_cl476, plain, ( (one @ (out1 @ (or1 @ (h2 @ f))))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl358, zip_derived_cl475])).
% 0.58/0.85 thf(zip_derived_cl487, plain, ( (abnormal @ (or1 @ (h2 @ f)))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl485, zip_derived_cl476])).
% 0.58/0.85 thf(zip_derived_cl488, plain, ($false),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl443, zip_derived_cl487])).
% 0.58/0.85
% 0.58/0.85 % SZS output end Refutation
% 0.58/0.85
% 0.58/0.85
% 0.58/0.85 % Terminating...
% 1.46/0.90 % Runner terminated.
% 1.46/0.91 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------