%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SYO068^4.020 : TPTP v9.2.0. Released v4.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.v2B2MSRgV8 true
% Computer : n010.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 05:06:23 PM UTC 2025
% Result : Theorem 3.13s 1.15s
% Output : Refutation 3.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYO068^4.020 : TPTP v9.2.0. Released v4.0.0.
% 0.13/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.v2B2MSRgV8 true
% 0.13/0.35 % Computer : n010.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Oct 1 18:09:08 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.13/0.35 % Running portfolio for 300 s
% 0.13/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.35 % Number of cores: 8
% 0.20/0.35 % Python version: Python 3.6.8
% 0.20/0.36 % Running in HO mode
% 0.56/0.66 % Total configuration time : 828
% 0.56/0.66 % Estimated wc time : 1656
% 0.56/0.66 % Estimated cpu time (8 cpus) : 207.0
% 0.57/0.73 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.57/0.78 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.57/0.78 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.57/0.78 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 0.57/0.81 % /export/starexec/sandbox/solver/bin/lams/40_noforms.sh running for 90s
% 0.57/0.81 % /export/starexec/sandbox/solver/bin/lams/40_b.comb.sh running for 70s
% 0.57/0.82 % /export/starexec/sandbox/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.57/0.82 % /export/starexec/sandbox/solver/bin/lams/30_sp5.sh running for 60s
% 0.59/0.84 % /export/starexec/sandbox/solver/bin/lams/30_b.l.sh running for 90s
% 0.59/0.84 % /export/starexec/sandbox/solver/bin/lams/35_full_unif.sh running for 56s
% 0.59/0.86 % /export/starexec/sandbox/solver/bin/lams/15_old_s4.sh running for 30s
% 0.59/0.87 % /export/starexec/sandbox/solver/bin/lams/15_lifting3.sh running for 30s
% 0.60/0.88 % /export/starexec/sandbox/solver/bin/lams/33_shallow_sine.sh running for 66s
% 0.60/0.94 % /export/starexec/sandbox/solver/bin/lams/40_e_lift.sh running for 80s
% 0.61/0.96 % /export/starexec/sandbox/solver/bin/lams/15_lifting1.sh running for 30s
% 0.61/0.98 % /export/starexec/sandbox/solver/bin/lams/8_new_cnf.sh running for 16s
% 3.13/1.08 % /export/starexec/sandbox/solver/bin/lams/10_e_short2.sh running for 20s
% 3.13/1.15 % Solved by lams/15_lifting1.sh.
% 3.13/1.15 % done 129 iterations in 0.140s
% 3.13/1.15 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 3.13/1.15 % SZS output start Refutation
% 3.13/1.15 thf(zip_tseitin_16_type, type, zip_tseitin_16: $i > $i > $o).
% 3.13/1.15 thf(iatom_type, type, iatom: ($i > $o) > $i > $o).
% 3.13/1.15 thf(p10_type, type, p10: $i > $o).
% 3.13/1.15 thf(sk__22_type, type, sk__22: $i > $i).
% 3.13/1.15 thf(p2_type, type, p2: $i > $o).
% 3.13/1.15 thf(ivalid_type, type, ivalid: ($i > $o) > $o).
% 3.13/1.15 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $o).
% 3.13/1.15 thf(sk__12_type, type, sk__12: $i > $i).
% 3.13/1.15 thf(sk__10_type, type, sk__10: $i > $i).
% 3.13/1.15 thf(p1_type, type, p1: $i > $o).
% 3.13/1.15 thf(sk__27_type, type, sk__27: $i > $i).
% 3.13/1.15 thf(irel_type, type, irel: $i > $i > $o).
% 3.13/1.15 thf(sk__37_type, type, sk__37: $i > $i).
% 3.13/1.15 thf(mor_type, type, mor: ($i > $o) > ($i > $o) > $i > $o).
% 3.13/1.15 thf(sk__30_type, type, sk__30: $i > $i).
% 3.13/1.15 thf(mimplies_type, type, mimplies: ($i > $o) > ($i > $o) > $i > $o).
% 3.13/1.15 thf(p18_type, type, p18: $i > $o).
% 3.13/1.15 thf(zip_tseitin_14_type, type, zip_tseitin_14: $i > $i > $o).
% 3.13/1.15 thf(sk__28_type, type, sk__28: $i > $i).
% 3.13/1.15 thf(p8_type, type, p8: $i > $o).
% 3.13/1.15 thf(sk__34_type, type, sk__34: $i > $i).
% 3.13/1.15 thf(sk__43_type, type, sk__43: $i > $i).
% 3.13/1.15 thf(sk__14_type, type, sk__14: $i > $i).
% 3.13/1.15 thf(sk__15_type, type, sk__15: $i > $i).
% 3.13/1.15 thf(zip_tseitin_11_type, type, zip_tseitin_11: $i > $i > $o).
% 3.13/1.15 thf(sk__7_type, type, sk__7: $i > $i).
% 3.13/1.15 thf(sk__18_type, type, sk__18: $i > $i).
% 3.13/1.15 thf(sk__42_type, type, sk__42: $i > $i).
% 3.13/1.15 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $i > $o).
% 3.13/1.15 thf(mbox_s4_type, type, mbox_s4: ($i > $o) > $i > $o).
% 3.13/1.15 thf(sk__35_type, type, sk__35: $i > $i).
% 3.13/1.15 thf(zip_tseitin_4_type, type, zip_tseitin_4: $i > $i > $o).
% 3.13/1.15 thf(p12_type, type, p12: $i > $o).
% 3.13/1.15 thf(sk__24_type, type, sk__24: $i > $i).
% 3.13/1.15 thf(p7_type, type, p7: $i > $o).
% 3.13/1.15 thf(iimplies_type, type, iimplies: ($i > $o) > ($i > $o) > $i > $o).
% 3.13/1.15 thf(p0_type, type, p0: $i > $o).
% 3.13/1.15 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > $o).
% 3.13/1.15 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $o).
% 3.13/1.15 thf(sk__11_type, type, sk__11: $i > $i).
% 3.13/1.15 thf(p14_type, type, p14: $i > $o).
% 3.13/1.15 thf(sk__29_type, type, sk__29: $i > $i).
% 3.13/1.15 thf(p16_type, type, p16: $i > $o).
% 3.13/1.15 thf(sk__32_type, type, sk__32: $i > $i).
% 3.13/1.15 thf(p13_type, type, p13: $i > $o).
% 3.13/1.15 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $o).
% 3.13/1.15 thf(p6_type, type, p6: $i > $o).
% 3.13/1.15 thf(zip_tseitin_15_type, type, zip_tseitin_15: $i > $i > $o).
% 3.13/1.15 thf(zip_tseitin_6_type, type, zip_tseitin_6: $i > $i > $o).
% 3.13/1.15 thf(sk__26_type, type, sk__26: $i > $i).
% 3.13/1.15 thf(mnot_type, type, mnot: ($i > $o) > $i > $o).
% 3.13/1.15 thf(zip_tseitin_18_type, type, zip_tseitin_18: $i > $i > $o).
% 3.13/1.15 thf(p15_type, type, p15: $i > $o).
% 3.13/1.15 thf(sk__20_type, type, sk__20: $i > $i).
% 3.13/1.15 thf(sk__17_type, type, sk__17: $i > $i).
% 3.13/1.15 thf(sk__38_type, type, sk__38: $i > $i).
% 3.13/1.15 thf(sk__31_type, type, sk__31: $i > $i).
% 3.13/1.15 thf(p17_type, type, p17: $i > $o).
% 3.13/1.15 thf(p11_type, type, p11: $i > $o).
% 3.13/1.15 thf(p20_type, type, p20: $i > $o).
% 3.13/1.15 thf(sk__33_type, type, sk__33: $i > $i).
% 3.13/1.15 thf(sk__6_type, type, sk__6: $i > $i).
% 3.13/1.15 thf(sk__8_type, type, sk__8: $i > $i).
% 3.13/1.15 thf(p9_type, type, p9: $i > $o).
% 3.13/1.15 thf(zip_tseitin_9_type, type, zip_tseitin_9: $i > $i > $o).
% 3.13/1.15 thf(sk__45_type, type, sk__45: $i).
% 3.13/1.15 thf(p19_type, type, p19: $i > $o).
% 3.13/1.15 thf(p5_type, type, p5: $i > $o).
% 3.13/1.15 thf(sk__16_type, type, sk__16: $i > $i).
% 3.13/1.15 thf(sk__13_type, type, sk__13: $i > $i).
% 3.13/1.15 thf(sk__25_type, type, sk__25: $i > $i).
% 3.13/1.15 thf(sk__5_type, type, sk__5: $i > $i).
% 3.13/1.15 thf(sk__40_type, type, sk__40: $i > $i).
% 3.13/1.15 thf(sk__9_type, type, sk__9: $i > $i).
% 3.13/1.15 thf(zip_tseitin_8_type, type, zip_tseitin_8: $i > $i > $o).
% 3.13/1.15 thf(sk__44_type, type, sk__44: $i > $i).
% 3.13/1.15 thf(zip_tseitin_10_type, type, zip_tseitin_10: $i > $i > $o).
% 3.13/1.15 thf(p4_type, type, p4: $i > $o).
% 3.13/1.15 thf(zip_tseitin_19_type, type, zip_tseitin_19: $i > $i > $o).
% 3.13/1.15 thf(p3_type, type, p3: $i > $o).
% 3.13/1.15 thf(zip_tseitin_13_type, type, zip_tseitin_13: $i > $i > $o).
% 3.13/1.15 thf(sk__36_type, type, sk__36: $i > $i).
% 3.13/1.15 thf(sk__19_type, type, sk__19: $i > $i).
% 3.13/1.15 thf(sk__39_type, type, sk__39: $i > $i).
% 3.13/1.15 thf(sk__41_type, type, sk__41: $i > $i).
% 3.13/1.15 thf(zip_tseitin_7_type, type, zip_tseitin_7: $i > $i > $o).
% 3.13/1.15 thf(sk__21_type, type, sk__21: $i > $i).
% 3.13/1.15 thf(zip_tseitin_12_type, type, zip_tseitin_12: $i > $i > $o).
% 3.13/1.15 thf(sk__23_type, type, sk__23: $i > $i).
% 3.13/1.15 thf(zip_tseitin_17_type, type, zip_tseitin_17: $i > $i > $o).
% 3.13/1.15 thf(ivalid, axiom,(( ivalid ) =
% 3.13/1.15 (^[Phi:( $i > $o )]: ( ![W:$i]: ( Phi @ W ) )))).
% 3.13/1.15 thf('0', plain,
% 3.13/1.15 (( ivalid ) = ( ^[Phi:( $i > $o )]: ( ![W:$i]: ( Phi @ W ) ) )),
% 3.13/1.15 inference('simplify_rw_rule', [status(thm)], [ivalid])).
% 3.13/1.15 thf('1', plain,
% 3.13/1.15 (( ivalid ) = ( ^[V_1:( $i > $o )]: ( ![X4:$i]: ( V_1 @ X4 ) ) )),
% 3.13/1.15 define([status(thm)])).
% 3.13/1.15 thf(iatom, axiom,(( iatom ) = (^[P:( $i > $o )]: ( P )))).
% 3.13/1.15 thf('2', plain, (( iatom ) = ( ^[P:( $i > $o )]: ( P ) )),
% 3.13/1.15 inference('simplify_rw_rule', [status(thm)], [iatom])).
% 3.13/1.15 thf('3', plain, (( iatom ) = ( ^[V_1:( $i > $o )]: ( V_1 ) )),
% 3.13/1.15 define([status(thm)])).thf(con, conjecture, (ivalid @ ( iatom @ p0 ))).
% 3.13/1.15 thf(zf_stmt_0, conjecture, (![X4:$i]: ( p0 @ X4 ))).
% 3.13/1.15 thf(zf_stmt_1, negated_conjecture, (~( ![X4:$i]: ( p0 @ X4 ) )),
% 3.13/1.15 inference('cnf.neg', [status(esa)], [zf_stmt_0])).
% 3.13/1.15 thf(zip_derived_cl63, plain, (~ (p0 @ sk__45)),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_1])).
% 3.13/1.15 thf(iimplies, axiom,(( iimplies ) =
% 3.13/1.15 (^[P:( $i > $o ),Q:( $i > $o )]:
% 3.13/1.15 ( mimplies @ ( mbox_s4 @ P ) @ ( mbox_s4 @ Q ) )))).
% 3.13/1.15 thf(mbox_s4, axiom,(( mbox_s4 ) =
% 3.13/1.15 (^[P:( $i > $o ),X:$i]: ( ![Y:$i]: ( ( irel @ X @ Y ) => ( P @ Y ) ) )))).
% 3.13/1.15 thf('4', plain,
% 3.13/1.15 (( mbox_s4 ) =
% 3.13/1.15 ( ^[P:( $i > $o ),X:$i]: ( ![Y:$i]: ( ( irel @ X @ Y ) => ( P @ Y ) ) ) )),
% 3.13/1.15 inference('simplify_rw_rule', [status(thm)], [mbox_s4])).
% 3.13/1.15 thf('5', plain,
% 3.13/1.15 (( mbox_s4 ) =
% 3.13/1.15 ( ^[V_1:( $i > $o ),V_2:$i]:
% 3.13/1.15 ( ![X4:$i]: ( ( irel @ V_2 @ X4 ) => ( V_1 @ X4 ) ) ) )),
% 3.13/1.15 define([status(thm)])).
% 3.13/1.15 thf(mimplies, axiom,(( mimplies ) =
% 3.13/1.15 (^[U:( $i > $o ),V:( $i > $o )]: ( mor @ ( mnot @ U ) @ V )))).
% 3.13/1.15 thf(mor, axiom,(( mor ) =
% 3.13/1.15 (^[X:( $i > $o ),Y:( $i > $o ),U:$i]: ( ( X @ U ) | ( Y @ U ) )))).
% 3.13/1.15 thf('6', plain,
% 3.13/1.15 (( mor ) =
% 3.13/1.15 ( ^[X:( $i > $o ),Y:( $i > $o ),U:$i]: ( ( X @ U ) | ( Y @ U ) ) )),
% 3.13/1.15 inference('simplify_rw_rule', [status(thm)], [mor])).
% 3.13/1.15 thf('7', plain,
% 3.13/1.15 (( mor ) =
% 3.13/1.15 ( ^[V_1:( $i > $o ),V_2:( $i > $o ),V_3:$i]:
% 3.13/1.15 ( ( V_1 @ V_3 ) | ( V_2 @ V_3 ) ) )),
% 3.13/1.15 define([status(thm)])).
% 3.13/1.15 thf(mnot, axiom,(( mnot ) = (^[X:( $i > $o ),U:$i]: ( ~( X @ U ) )))).
% 3.13/1.15 thf('8', plain, (( mnot ) = ( ^[X:( $i > $o ),U:$i]: ( ~( X @ U ) ) )),
% 3.13/1.15 inference('simplify_rw_rule', [status(thm)], [mnot])).
% 3.13/1.15 thf('9', plain,
% 3.13/1.15 (( mnot ) = ( ^[V_1:( $i > $o ),V_2:$i]: ( ~( V_1 @ V_2 ) ) )),
% 3.13/1.15 define([status(thm)])).
% 3.13/1.15 thf('10', plain,
% 3.13/1.15 (( mimplies ) =
% 3.13/1.15 ( ^[U:( $i > $o ),V:( $i > $o )]: ( mor @ ( mnot @ U ) @ V ) )),
% 3.13/1.15 inference('simplify_rw_rule', [status(thm)], [mimplies, '7', '9'])).
% 3.13/1.15 thf('11', plain,
% 3.13/1.15 (( mimplies ) =
% 3.13/1.15 ( ^[V_1:( $i > $o ),V_2:( $i > $o )]: ( mor @ ( mnot @ V_1 ) @ V_2 ) )),
% 3.13/1.15 define([status(thm)])).
% 3.13/1.15 thf('12', plain,
% 3.13/1.15 (( iimplies ) =
% 3.13/1.15 ( ^[P:( $i > $o ),Q:( $i > $o )]:
% 3.13/1.15 ( mimplies @ ( mbox_s4 @ P ) @ ( mbox_s4 @ Q ) ) )),
% 3.13/1.15 inference('simplify_rw_rule', [status(thm)], [iimplies, '5', '11'])).
% 3.13/1.15 thf('13', plain,
% 3.13/1.15 (( iimplies ) =
% 3.13/1.15 ( ^[V_1:( $i > $o ),V_2:( $i > $o )]:
% 3.13/1.15 ( mimplies @ ( mbox_s4 @ V_1 ) @ ( mbox_s4 @ V_2 ) ) )),
% 3.13/1.15 define([status(thm)])).
% 3.13/1.15 thf(axiom2, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p1 ) @ ( iimplies @ ( iatom @ p1 ) @ ( iatom @ p0 ) ) ))).
% 3.13/1.15 thf(zf_stmt_2, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p0 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p1 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p1 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_3, type, zip_tseitin_0 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_4, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p1 @ X10 ) ) => ( zip_tseitin_0 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_5, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_0 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_0 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p0 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl5, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_0 @ (sk__5 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_0 @ (sk__6 @ X1) @ X1)
% 3.13/1.15 | (p0 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_5])).
% 3.13/1.15 thf(zip_derived_cl3, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_0 @ X0 @ X1) | ~ (p1 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_4])).
% 3.13/1.15 thf(axiom3, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p2 ) @ ( iimplies @ ( iatom @ p2 ) @ ( iatom @ p1 ) ) ))).
% 3.13/1.15 thf(zf_stmt_6, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p1 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p2 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p2 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_7, type, zip_tseitin_1 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_8, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p2 @ X10 ) ) => ( zip_tseitin_1 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_9, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_1 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_1 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p1 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl8, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_1 @ (sk__7 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_1 @ (sk__8 @ X1) @ X1)
% 3.13/1.15 | (p1 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_9])).
% 3.13/1.15 thf(zip_derived_cl6, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_1 @ X0 @ X1) | ~ (p2 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_8])).
% 3.13/1.15 thf(axiom4, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p3 ) @ ( iimplies @ ( iatom @ p3 ) @ ( iatom @ p2 ) ) ))).
% 3.13/1.15 thf(zf_stmt_10, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p2 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p3 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p3 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_11, type, zip_tseitin_2 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_12, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p3 @ X10 ) ) => ( zip_tseitin_2 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_13, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_2 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_2 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p2 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl11, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_2 @ (sk__9 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_2 @ (sk__10 @ X1) @ X1)
% 3.13/1.15 | (p2 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_13])).
% 3.13/1.15 thf(zip_derived_cl9, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_2 @ X0 @ X1) | ~ (p3 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_12])).
% 3.13/1.15 thf(axiom5, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p4 ) @ ( iimplies @ ( iatom @ p4 ) @ ( iatom @ p3 ) ) ))).
% 3.13/1.15 thf(zf_stmt_14, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p3 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p4 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p4 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_15, type, zip_tseitin_3 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_16, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p4 @ X10 ) ) => ( zip_tseitin_3 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_17, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_3 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_3 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p3 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl14, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_3 @ (sk__11 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_3 @ (sk__12 @ X1) @ X1)
% 3.13/1.15 | (p3 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_17])).
% 3.13/1.15 thf(zip_derived_cl12, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_3 @ X0 @ X1) | ~ (p4 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_16])).
% 3.13/1.15 thf(axiom6, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p5 ) @ ( iimplies @ ( iatom @ p5 ) @ ( iatom @ p4 ) ) ))).
% 3.13/1.15 thf(zf_stmt_18, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p4 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p5 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p5 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_19, type, zip_tseitin_4 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_20, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p5 @ X10 ) ) => ( zip_tseitin_4 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_21, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_4 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_4 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p4 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl17, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_4 @ (sk__13 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_4 @ (sk__14 @ X1) @ X1)
% 3.13/1.15 | (p4 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_21])).
% 3.13/1.15 thf(zip_derived_cl15, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_4 @ X0 @ X1) | ~ (p5 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_20])).
% 3.13/1.15 thf(axiom7, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p6 ) @ ( iimplies @ ( iatom @ p6 ) @ ( iatom @ p5 ) ) ))).
% 3.13/1.15 thf(zf_stmt_22, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p5 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p6 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p6 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_23, type, zip_tseitin_5 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_24, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p6 @ X10 ) ) => ( zip_tseitin_5 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_25, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_5 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_5 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p5 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl20, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_5 @ (sk__15 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_5 @ (sk__16 @ X1) @ X1)
% 3.13/1.15 | (p5 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_25])).
% 3.13/1.15 thf(zip_derived_cl18, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_5 @ X0 @ X1) | ~ (p6 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_24])).
% 3.13/1.15 thf(axiom8, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p7 ) @ ( iimplies @ ( iatom @ p7 ) @ ( iatom @ p6 ) ) ))).
% 3.13/1.15 thf(zf_stmt_26, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p6 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p7 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p7 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_27, type, zip_tseitin_6 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_28, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p7 @ X10 ) ) => ( zip_tseitin_6 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_29, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_6 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_6 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p6 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl23, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_6 @ (sk__17 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_6 @ (sk__18 @ X1) @ X1)
% 3.13/1.15 | (p6 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_29])).
% 3.13/1.15 thf(zip_derived_cl21, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_6 @ X0 @ X1) | ~ (p7 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_28])).
% 3.13/1.15 thf(axiom9, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p8 ) @ ( iimplies @ ( iatom @ p8 ) @ ( iatom @ p7 ) ) ))).
% 3.13/1.15 thf(zf_stmt_30, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p7 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p8 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p8 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_31, type, zip_tseitin_7 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_32, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p8 @ X10 ) ) => ( zip_tseitin_7 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_33, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_7 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_7 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p7 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl26, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_7 @ (sk__19 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_7 @ (sk__20 @ X1) @ X1)
% 3.13/1.15 | (p7 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_33])).
% 3.13/1.15 thf(zip_derived_cl24, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_7 @ X0 @ X1) | ~ (p8 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_32])).
% 3.13/1.15 thf(axiom10, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p9 ) @ ( iimplies @ ( iatom @ p9 ) @ ( iatom @ p8 ) ) ))).
% 3.13/1.15 thf(zf_stmt_34, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p8 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p9 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p9 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_35, type, zip_tseitin_8 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_36, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p9 @ X10 ) ) => ( zip_tseitin_8 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_37, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_8 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_8 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p8 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl29, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_8 @ (sk__21 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_8 @ (sk__22 @ X1) @ X1)
% 3.13/1.15 | (p8 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_37])).
% 3.13/1.15 thf(zip_derived_cl27, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_8 @ X0 @ X1) | ~ (p9 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_36])).
% 3.13/1.15 thf(axiom11, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p10 ) @ ( iimplies @ ( iatom @ p10 ) @ ( iatom @ p9 ) ) ))).
% 3.13/1.15 thf(zf_stmt_38, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p9 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p10 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p10 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_39, type, zip_tseitin_9 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_40, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p10 @ X10 ) ) => ( zip_tseitin_9 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_41, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_9 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_9 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p9 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl32, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_9 @ (sk__23 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_9 @ (sk__24 @ X1) @ X1)
% 3.13/1.15 | (p9 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_41])).
% 3.13/1.15 thf(zip_derived_cl30, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_9 @ X0 @ X1) | ~ (p10 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_40])).
% 3.13/1.15 thf(axiom12, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p11 ) @ ( iimplies @ ( iatom @ p11 ) @ ( iatom @ p10 ) ) ))).
% 3.13/1.15 thf(zf_stmt_42, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p10 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p11 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p11 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_43, type, zip_tseitin_10 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_44, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p11 @ X10 ) ) =>
% 3.13/1.15 ( zip_tseitin_10 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_45, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_10 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_10 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p10 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl35, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_10 @ (sk__25 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_10 @ (sk__26 @ X1) @ X1)
% 3.13/1.15 | (p10 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_45])).
% 3.13/1.15 thf(zip_derived_cl33, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_10 @ X0 @ X1) | ~ (p11 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_44])).
% 3.13/1.15 thf(axiom13, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p12 ) @ ( iimplies @ ( iatom @ p12 ) @ ( iatom @ p11 ) ) ))).
% 3.13/1.15 thf(zf_stmt_46, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p11 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p12 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p12 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_47, type, zip_tseitin_11 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_48, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p12 @ X10 ) ) =>
% 3.13/1.15 ( zip_tseitin_11 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_49, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_11 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_11 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p11 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl38, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_11 @ (sk__27 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_11 @ (sk__28 @ X1) @ X1)
% 3.13/1.15 | (p11 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_49])).
% 3.13/1.15 thf(zip_derived_cl36, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_11 @ X0 @ X1) | ~ (p12 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_48])).
% 3.13/1.15 thf(axiom14, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p13 ) @ ( iimplies @ ( iatom @ p13 ) @ ( iatom @ p12 ) ) ))).
% 3.13/1.15 thf(zf_stmt_50, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p12 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p13 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p13 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_51, type, zip_tseitin_12 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_52, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p13 @ X10 ) ) =>
% 3.13/1.15 ( zip_tseitin_12 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_53, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_12 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_12 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p12 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl41, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_12 @ (sk__29 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_12 @ (sk__30 @ X1) @ X1)
% 3.13/1.15 | (p12 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_53])).
% 3.13/1.15 thf(zip_derived_cl39, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_12 @ X0 @ X1) | ~ (p13 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_52])).
% 3.13/1.15 thf(axiom15, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p14 ) @ ( iimplies @ ( iatom @ p14 ) @ ( iatom @ p13 ) ) ))).
% 3.13/1.15 thf(zf_stmt_54, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p13 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p14 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p14 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_55, type, zip_tseitin_13 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_56, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p14 @ X10 ) ) =>
% 3.13/1.15 ( zip_tseitin_13 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_57, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_13 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_13 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p13 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl44, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_13 @ (sk__31 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_13 @ (sk__32 @ X1) @ X1)
% 3.13/1.15 | (p13 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_57])).
% 3.13/1.15 thf(zip_derived_cl42, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_13 @ X0 @ X1) | ~ (p14 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_56])).
% 3.13/1.15 thf(axiom16, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p15 ) @ ( iimplies @ ( iatom @ p15 ) @ ( iatom @ p14 ) ) ))).
% 3.13/1.15 thf(zf_stmt_58, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p14 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p15 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p15 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_59, type, zip_tseitin_14 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_60, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p15 @ X10 ) ) =>
% 3.13/1.15 ( zip_tseitin_14 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_61, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_14 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_14 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p14 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl47, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_14 @ (sk__33 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_14 @ (sk__34 @ X1) @ X1)
% 3.13/1.15 | (p14 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_61])).
% 3.13/1.15 thf(zip_derived_cl45, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_14 @ X0 @ X1) | ~ (p15 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_60])).
% 3.13/1.15 thf(axiom17, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p16 ) @ ( iimplies @ ( iatom @ p16 ) @ ( iatom @ p15 ) ) ))).
% 3.13/1.15 thf(zf_stmt_62, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p15 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p16 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p16 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_63, type, zip_tseitin_15 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_64, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p16 @ X10 ) ) =>
% 3.13/1.15 ( zip_tseitin_15 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_65, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_15 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_15 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p15 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl50, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_15 @ (sk__35 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_15 @ (sk__36 @ X1) @ X1)
% 3.13/1.15 | (p15 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_65])).
% 3.13/1.15 thf(zip_derived_cl48, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_15 @ X0 @ X1) | ~ (p16 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_64])).
% 3.13/1.15 thf(axiom18, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p17 ) @ ( iimplies @ ( iatom @ p17 ) @ ( iatom @ p16 ) ) ))).
% 3.13/1.15 thf(zf_stmt_66, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p16 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p17 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p17 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_67, type, zip_tseitin_16 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_68, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p17 @ X10 ) ) =>
% 3.13/1.15 ( zip_tseitin_16 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_69, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_16 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_16 @ X10 @ X8 ) ) ) |
% 3.13/1.15 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p16 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.15 thf(zip_derived_cl53, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.15 (~ (zip_tseitin_16 @ (sk__37 @ X0) @ X0)
% 3.13/1.15 | ~ (irel @ X0 @ X1)
% 3.13/1.15 | ~ (zip_tseitin_16 @ (sk__38 @ X1) @ X1)
% 3.13/1.15 | (p16 @ X2)
% 3.13/1.15 | ~ (irel @ X1 @ X2))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_69])).
% 3.13/1.15 thf(zip_derived_cl51, plain,
% 3.13/1.15 (![X0 : $i, X1 : $i]: ( (zip_tseitin_16 @ X0 @ X1) | ~ (p17 @ X0))),
% 3.13/1.15 inference('cnf', [status(esa)], [zf_stmt_68])).
% 3.13/1.15 thf(axiom19, axiom,
% 3.13/1.15 (ivalid @
% 3.13/1.15 ( iimplies @
% 3.13/1.15 ( iatom @ p18 ) @ ( iimplies @ ( iatom @ p18 ) @ ( iatom @ p17 ) ) ))).
% 3.13/1.15 thf(zf_stmt_70, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p17 @ X12 ) ) ) |
% 3.13/1.15 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p18 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.15 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p18 @ X6 ) ) ) ) ))).
% 3.13/1.15 thf(zf_stmt_71, type, zip_tseitin_17 : $i > $i > $o).
% 3.13/1.15 thf(zf_stmt_72, axiom,
% 3.13/1.15 (![X10:$i,X8:$i]:
% 3.13/1.15 ( ( ( irel @ X8 @ X10 ) => ( p18 @ X10 ) ) =>
% 3.13/1.15 ( zip_tseitin_17 @ X10 @ X8 ) ))).
% 3.13/1.15 thf(zf_stmt_73, axiom,
% 3.13/1.15 (![X4:$i]:
% 3.13/1.15 ( ( ~( ![X6:$i]: ( zip_tseitin_17 @ X6 @ X4 ) ) ) |
% 3.13/1.15 ( ![X8:$i]:
% 3.13/1.15 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.15 ( ( ~( ![X10:$i]: ( zip_tseitin_17 @ X10 @ X8 ) ) ) |
% 3.13/1.16 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p17 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.16 thf(zip_derived_cl56, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (zip_tseitin_17 @ (sk__39 @ X0) @ X0)
% 3.13/1.16 | ~ (irel @ X0 @ X1)
% 3.13/1.16 | ~ (zip_tseitin_17 @ (sk__40 @ X1) @ X1)
% 3.13/1.16 | (p17 @ X2)
% 3.13/1.16 | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('cnf', [status(esa)], [zf_stmt_73])).
% 3.13/1.16 thf(zip_derived_cl54, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: ( (zip_tseitin_17 @ X0 @ X1) | ~ (p18 @ X0))),
% 3.13/1.16 inference('cnf', [status(esa)], [zf_stmt_72])).
% 3.13/1.16 thf(axiom20, axiom,
% 3.13/1.16 (ivalid @
% 3.13/1.16 ( iimplies @
% 3.13/1.16 ( iatom @ p19 ) @ ( iimplies @ ( iatom @ p19 ) @ ( iatom @ p18 ) ) ))).
% 3.13/1.16 thf(zf_stmt_74, axiom,
% 3.13/1.16 (![X4:$i]:
% 3.13/1.16 ( ( ![X8:$i]:
% 3.13/1.16 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.16 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p18 @ X12 ) ) ) |
% 3.13/1.16 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p19 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.16 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p19 @ X6 ) ) ) ) ))).
% 3.13/1.16 thf(zf_stmt_75, type, zip_tseitin_18 : $i > $i > $o).
% 3.13/1.16 thf(zf_stmt_76, axiom,
% 3.13/1.16 (![X10:$i,X8:$i]:
% 3.13/1.16 ( ( ( irel @ X8 @ X10 ) => ( p19 @ X10 ) ) =>
% 3.13/1.16 ( zip_tseitin_18 @ X10 @ X8 ) ))).
% 3.13/1.16 thf(zf_stmt_77, axiom,
% 3.13/1.16 (![X4:$i]:
% 3.13/1.16 ( ( ~( ![X6:$i]: ( zip_tseitin_18 @ X6 @ X4 ) ) ) |
% 3.13/1.16 ( ![X8:$i]:
% 3.13/1.16 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.16 ( ( ~( ![X10:$i]: ( zip_tseitin_18 @ X10 @ X8 ) ) ) |
% 3.13/1.16 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p18 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.16 thf(zip_derived_cl59, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (zip_tseitin_18 @ (sk__41 @ X0) @ X0)
% 3.13/1.16 | ~ (irel @ X0 @ X1)
% 3.13/1.16 | ~ (zip_tseitin_18 @ (sk__42 @ X1) @ X1)
% 3.13/1.16 | (p18 @ X2)
% 3.13/1.16 | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('cnf', [status(esa)], [zf_stmt_77])).
% 3.13/1.16 thf(zip_derived_cl57, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: ( (zip_tseitin_18 @ X0 @ X1) | ~ (p19 @ X0))),
% 3.13/1.16 inference('cnf', [status(esa)], [zf_stmt_76])).
% 3.13/1.16 thf(axiom21, axiom,
% 3.13/1.16 (ivalid @
% 3.13/1.16 ( iimplies @
% 3.13/1.16 ( iatom @ p20 ) @ ( iimplies @ ( iatom @ p20 ) @ ( iatom @ p19 ) ) ))).
% 3.13/1.16 thf(zf_stmt_78, axiom,
% 3.13/1.16 (![X4:$i]:
% 3.13/1.16 ( ( ![X8:$i]:
% 3.13/1.16 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.16 ( ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p19 @ X12 ) ) ) |
% 3.13/1.16 ( ~( ![X10:$i]: ( ( irel @ X8 @ X10 ) => ( p20 @ X10 ) ) ) ) ) ) ) |
% 3.13/1.16 ( ~( ![X6:$i]: ( ( irel @ X4 @ X6 ) => ( p20 @ X6 ) ) ) ) ))).
% 3.13/1.16 thf(zf_stmt_79, type, zip_tseitin_19 : $i > $i > $o).
% 3.13/1.16 thf(zf_stmt_80, axiom,
% 3.13/1.16 (![X10:$i,X8:$i]:
% 3.13/1.16 ( ( ( irel @ X8 @ X10 ) => ( p20 @ X10 ) ) =>
% 3.13/1.16 ( zip_tseitin_19 @ X10 @ X8 ) ))).
% 3.13/1.16 thf(zf_stmt_81, axiom,
% 3.13/1.16 (![X4:$i]:
% 3.13/1.16 ( ( ~( ![X6:$i]: ( zip_tseitin_19 @ X6 @ X4 ) ) ) |
% 3.13/1.16 ( ![X8:$i]:
% 3.13/1.16 ( ( irel @ X4 @ X8 ) =>
% 3.13/1.16 ( ( ~( ![X10:$i]: ( zip_tseitin_19 @ X10 @ X8 ) ) ) |
% 3.13/1.16 ( ![X12:$i]: ( ( irel @ X8 @ X12 ) => ( p19 @ X12 ) ) ) ) ) ) ))).
% 3.13/1.16 thf(zip_derived_cl62, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (zip_tseitin_19 @ (sk__43 @ X0) @ X0)
% 3.13/1.16 | ~ (irel @ X0 @ X1)
% 3.13/1.16 | ~ (zip_tseitin_19 @ (sk__44 @ X1) @ X1)
% 3.13/1.16 | (p19 @ X2)
% 3.13/1.16 | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('cnf', [status(esa)], [zf_stmt_81])).
% 3.13/1.16 thf(zip_derived_cl60, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: ( (zip_tseitin_19 @ X0 @ X1) | ~ (p20 @ X0))),
% 3.13/1.16 inference('cnf', [status(esa)], [zf_stmt_80])).
% 3.13/1.16 thf(axiom1, axiom, (ivalid @ ( iatom @ p20 ))).
% 3.13/1.16 thf(zf_stmt_82, axiom, (![X4:$i]: ( p20 @ X4 ))).
% 3.13/1.16 thf(zip_derived_cl2, plain, (![X0 : $i]: (p20 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [zf_stmt_82])).
% 3.13/1.16 thf(zip_derived_cl67, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_19 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl60, zip_derived_cl2])).
% 3.13/1.16 thf(zip_derived_cl67, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_19 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl60, zip_derived_cl2])).
% 3.13/1.16 thf(zip_derived_cl90, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p19 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl62, zip_derived_cl67, zip_derived_cl67])).
% 3.13/1.16 thf(zip_derived_cl92, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p19 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl90])).
% 3.13/1.16 thf(refl_axiom, axiom, (![X:$i]: ( irel @ X @ X ))).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl93, plain, (![X0 : $i]: (p19 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl92, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl94, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_18 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl57, zip_derived_cl93])).
% 3.13/1.16 thf(zip_derived_cl94, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_18 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl57, zip_derived_cl93])).
% 3.13/1.16 thf(zip_derived_cl95, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p18 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl59, zip_derived_cl94, zip_derived_cl94])).
% 3.13/1.16 thf(zip_derived_cl97, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p18 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl95])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl98, plain, (![X0 : $i]: (p18 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl97, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl99, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_17 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl54, zip_derived_cl98])).
% 3.13/1.16 thf(zip_derived_cl99, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_17 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl54, zip_derived_cl98])).
% 3.13/1.16 thf(zip_derived_cl100, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p17 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl56, zip_derived_cl99, zip_derived_cl99])).
% 3.13/1.16 thf(zip_derived_cl103, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p17 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl100])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl104, plain, (![X0 : $i]: (p17 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl103, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl105, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_16 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl51, zip_derived_cl104])).
% 3.13/1.16 thf(zip_derived_cl105, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_16 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl51, zip_derived_cl104])).
% 3.13/1.16 thf(zip_derived_cl106, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p16 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl53, zip_derived_cl105, zip_derived_cl105])).
% 3.13/1.16 thf(zip_derived_cl108, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p16 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl106])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl109, plain, (![X0 : $i]: (p16 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl108, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl110, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_15 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl48, zip_derived_cl109])).
% 3.13/1.16 thf(zip_derived_cl110, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_15 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl48, zip_derived_cl109])).
% 3.13/1.16 thf(zip_derived_cl111, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p15 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl50, zip_derived_cl110, zip_derived_cl110])).
% 3.13/1.16 thf(zip_derived_cl113, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p15 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl111])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl114, plain, (![X0 : $i]: (p15 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl113, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl115, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_14 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl45, zip_derived_cl114])).
% 3.13/1.16 thf(zip_derived_cl115, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_14 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl45, zip_derived_cl114])).
% 3.13/1.16 thf(zip_derived_cl116, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p14 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl47, zip_derived_cl115, zip_derived_cl115])).
% 3.13/1.16 thf(zip_derived_cl118, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p14 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl116])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl119, plain, (![X0 : $i]: (p14 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl118, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl121, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_13 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl42, zip_derived_cl119])).
% 3.13/1.16 thf(zip_derived_cl121, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_13 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl42, zip_derived_cl119])).
% 3.13/1.16 thf(zip_derived_cl122, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p13 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl44, zip_derived_cl121, zip_derived_cl121])).
% 3.13/1.16 thf(zip_derived_cl124, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p13 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl122])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl125, plain, (![X0 : $i]: (p13 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl124, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl126, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_12 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl39, zip_derived_cl125])).
% 3.13/1.16 thf(zip_derived_cl126, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_12 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl39, zip_derived_cl125])).
% 3.13/1.16 thf(zip_derived_cl127, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p12 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl41, zip_derived_cl126, zip_derived_cl126])).
% 3.13/1.16 thf(zip_derived_cl129, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p12 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl127])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl130, plain, (![X0 : $i]: (p12 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl129, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl131, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_11 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl36, zip_derived_cl130])).
% 3.13/1.16 thf(zip_derived_cl131, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_11 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl36, zip_derived_cl130])).
% 3.13/1.16 thf(zip_derived_cl132, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p11 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl38, zip_derived_cl131, zip_derived_cl131])).
% 3.13/1.16 thf(zip_derived_cl134, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p11 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl132])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl135, plain, (![X0 : $i]: (p11 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl134, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl136, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_10 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl33, zip_derived_cl135])).
% 3.13/1.16 thf(zip_derived_cl136, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_10 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl33, zip_derived_cl135])).
% 3.13/1.16 thf(zip_derived_cl138, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p10 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl35, zip_derived_cl136, zip_derived_cl136])).
% 3.13/1.16 thf(zip_derived_cl140, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p10 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl138])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl141, plain, (![X0 : $i]: (p10 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl140, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl142, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_9 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl30, zip_derived_cl141])).
% 3.13/1.16 thf(zip_derived_cl142, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_9 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl30, zip_derived_cl141])).
% 3.13/1.16 thf(zip_derived_cl143, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p9 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl32, zip_derived_cl142, zip_derived_cl142])).
% 3.13/1.16 thf(zip_derived_cl145, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p9 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl143])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl146, plain, (![X0 : $i]: (p9 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl145, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl147, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_8 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl27, zip_derived_cl146])).
% 3.13/1.16 thf(zip_derived_cl147, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_8 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl27, zip_derived_cl146])).
% 3.13/1.16 thf(zip_derived_cl148, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p8 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl29, zip_derived_cl147, zip_derived_cl147])).
% 3.13/1.16 thf(zip_derived_cl150, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p8 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl148])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl151, plain, (![X0 : $i]: (p8 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl150, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl152, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_7 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl24, zip_derived_cl151])).
% 3.13/1.16 thf(zip_derived_cl152, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_7 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl24, zip_derived_cl151])).
% 3.13/1.16 thf(zip_derived_cl153, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p7 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl26, zip_derived_cl152, zip_derived_cl152])).
% 3.13/1.16 thf(zip_derived_cl156, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p7 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl153])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl157, plain, (![X0 : $i]: (p7 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl156, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl158, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_6 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl21, zip_derived_cl157])).
% 3.13/1.16 thf(zip_derived_cl158, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_6 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl21, zip_derived_cl157])).
% 3.13/1.16 thf(zip_derived_cl159, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p6 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl23, zip_derived_cl158, zip_derived_cl158])).
% 3.13/1.16 thf(zip_derived_cl161, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p6 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl159])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl162, plain, (![X0 : $i]: (p6 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl161, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl163, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_5 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl18, zip_derived_cl162])).
% 3.13/1.16 thf(zip_derived_cl163, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_5 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl18, zip_derived_cl162])).
% 3.13/1.16 thf(zip_derived_cl164, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p5 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl20, zip_derived_cl163, zip_derived_cl163])).
% 3.13/1.16 thf(zip_derived_cl166, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p5 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl164])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl167, plain, (![X0 : $i]: (p5 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl166, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl168, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_4 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl15, zip_derived_cl167])).
% 3.13/1.16 thf(zip_derived_cl168, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_4 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl15, zip_derived_cl167])).
% 3.13/1.16 thf(zip_derived_cl169, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p4 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl17, zip_derived_cl168, zip_derived_cl168])).
% 3.13/1.16 thf(zip_derived_cl172, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p4 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl169])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl173, plain, (![X0 : $i]: (p4 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl172, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl176, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_3 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl12, zip_derived_cl173])).
% 3.13/1.16 thf(zip_derived_cl176, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_3 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl12, zip_derived_cl173])).
% 3.13/1.16 thf(zip_derived_cl177, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p3 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl14, zip_derived_cl176, zip_derived_cl176])).
% 3.13/1.16 thf(zip_derived_cl180, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p3 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl177])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl181, plain, (![X0 : $i]: (p3 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl180, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl182, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_2 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl9, zip_derived_cl181])).
% 3.13/1.16 thf(zip_derived_cl182, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_2 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl9, zip_derived_cl181])).
% 3.13/1.16 thf(zip_derived_cl183, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p2 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl11, zip_derived_cl182, zip_derived_cl182])).
% 3.13/1.16 thf(zip_derived_cl186, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p2 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl183])).
% 3.13/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.13/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.13/1.16 thf(zip_derived_cl187, plain, (![X0 : $i]: (p2 @ X0)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl186, zip_derived_cl0])).
% 3.13/1.16 thf(zip_derived_cl188, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_1 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl6, zip_derived_cl187])).
% 3.13/1.16 thf(zip_derived_cl188, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_1 @ X0 @ X1)),
% 3.13/1.16 inference('demod', [status(thm)], [zip_derived_cl6, zip_derived_cl187])).
% 3.13/1.16 thf(zip_derived_cl189, plain,
% 3.13/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.13/1.16 (~ (irel @ X0 @ X1) | (p1 @ X2) | ~ (irel @ X1 @ X2))),
% 3.13/1.16 inference('demod', [status(thm)],
% 3.13/1.16 [zip_derived_cl8, zip_derived_cl188, zip_derived_cl188])).
% 3.13/1.16 thf(zip_derived_cl192, plain,
% 3.13/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p1 @ X0))),
% 3.13/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl189])).
% 3.71/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.71/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.71/1.16 thf(zip_derived_cl193, plain, (![X0 : $i]: (p1 @ X0)),
% 3.71/1.16 inference('demod', [status(thm)], [zip_derived_cl192, zip_derived_cl0])).
% 3.71/1.16 thf(zip_derived_cl194, plain,
% 3.71/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_0 @ X0 @ X1)),
% 3.71/1.16 inference('demod', [status(thm)], [zip_derived_cl3, zip_derived_cl193])).
% 3.71/1.16 thf(zip_derived_cl194, plain,
% 3.71/1.16 (![X0 : $i, X1 : $i]: (zip_tseitin_0 @ X0 @ X1)),
% 3.71/1.16 inference('demod', [status(thm)], [zip_derived_cl3, zip_derived_cl193])).
% 3.71/1.16 thf(zip_derived_cl198, plain,
% 3.71/1.16 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.71/1.16 (~ (irel @ X0 @ X1) | (p0 @ X2) | ~ (irel @ X1 @ X2))),
% 3.71/1.16 inference('demod', [status(thm)],
% 3.71/1.16 [zip_derived_cl5, zip_derived_cl194, zip_derived_cl194])).
% 3.71/1.16 thf(zip_derived_cl201, plain,
% 3.71/1.16 (![X0 : $i]: (~ (irel @ X0 @ X0) | (p0 @ X0))),
% 3.71/1.16 inference('eq_fact', [status(thm)], [zip_derived_cl198])).
% 3.71/1.16 thf(zip_derived_cl0, plain, (![X0 : $i]: (irel @ X0 @ X0)),
% 3.71/1.16 inference('cnf', [status(esa)], [refl_axiom])).
% 3.71/1.16 thf(zip_derived_cl202, plain, (![X0 : $i]: (p0 @ X0)),
% 3.71/1.16 inference('demod', [status(thm)], [zip_derived_cl201, zip_derived_cl0])).
% 3.71/1.16 thf(zip_derived_cl203, plain, ($false),
% 3.71/1.16 inference('demod', [status(thm)], [zip_derived_cl63, zip_derived_cl202])).
% 3.71/1.16
% 3.71/1.16 % SZS output end Refutation
% 3.71/1.16
% 3.71/1.16
% 3.71/1.16 % Terminating...
% 3.73/1.24 % Runner terminated.
% 3.73/1.25 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------