%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : MSC010+1 : TPTP v9.2.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.KzsGUB7G3Q true
% Computer : n017.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:44:53 PM UTC 2025
% Result : Theorem 0.57s 0.89s
% Output : Refutation 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : MSC010+1 : TPTP v9.2.0. Released v3.1.0.
% 0.07/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.KzsGUB7G3Q true
% 0.14/0.34 % Computer : n017.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Oct 1 14:03:23 EDT 2025
% 0.14/0.35 % CPUTime :
% 0.14/0.35 % Running portfolio for 300 s
% 0.14/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.35 % Number of cores: 8
% 0.14/0.35 % Python version: Python 3.6.8
% 0.14/0.35 % Running in FO mode
% 0.55/0.68 % Total configuration time : 435
% 0.55/0.68 % Estimated wc time : 1092
% 0.55/0.68 % Estimated cpu time (7 cpus) : 156.0
% 0.56/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.56/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.56/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.56/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.56/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.56/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.56/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.57/0.89 % Solved by fo/fo1_av.sh.
% 0.57/0.89 % done 230 iterations in 0.057s
% 0.57/0.89 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.57/0.89 % SZS output start Refutation
% 0.57/0.89 thf(n998_type, type, n998: $i).
% 0.57/0.89 thf(zip_tseitin_7_type, type, zip_tseitin_7: $i > $i > $o).
% 0.57/0.89 thf(r_ds1_filter_init_type, type, r_ds1_filter_init: $i).
% 0.57/0.89 thf(sk__3_type, type, sk__3: $i).
% 0.57/0.89 thf(sk__type, type, sk_: $i > $i).
% 0.57/0.89 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $o).
% 0.57/0.89 thf(q_ds1_filter_init_type, type, q_ds1_filter_init: $i).
% 0.57/0.89 thf(zip_tseitin_19_type, type, zip_tseitin_19: $i > $i > $o).
% 0.57/0.89 thf(sk__21_type, type, sk__21: $i).
% 0.57/0.89 thf(sk__12_type, type, sk__12: $i).
% 0.57/0.89 thf(sk__6_type, type, sk__6: $i).
% 0.57/0.89 thf(zip_tseitin_8_type, type, zip_tseitin_8: $i > $i > $o).
% 0.57/0.89 thf(pv5_type, type, pv5: $i).
% 0.57/0.89 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $o).
% 0.57/0.89 thf(zip_tseitin_6_type, type, zip_tseitin_6: $i > $i > $o).
% 0.57/0.89 thf(sk__15_type, type, sk__15: $i).
% 0.57/0.89 thf(sk__9_type, type, sk__9: $i).
% 0.57/0.89 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $o).
% 0.57/0.89 thf(sk__1_type, type, sk__1: $i).
% 0.57/0.89 thf(sk__11_type, type, sk__11: $i).
% 0.57/0.89 thf(n5_type, type, n5: $i).
% 0.57/0.89 thf(sk__14_type, type, sk__14: $i).
% 0.57/0.89 thf(zip_tseitin_17_type, type, zip_tseitin_17: $i > $i > $o).
% 0.57/0.89 thf(n0_type, type, n0: $i).
% 0.57/0.89 thf(sk__2_type, type, sk__2: $i).
% 0.57/0.89 thf(n2_type, type, n2: $i).
% 0.57/0.89 thf(leq_type, type, leq: $i > $i > $o).
% 0.57/0.89 thf(phi_ds1_filter_init_type, type, phi_ds1_filter_init: $i).
% 0.57/0.89 thf(sk__16_type, type, sk__16: $i).
% 0.57/0.89 thf(xhatmin_ds1_filter_init_type, type, xhatmin_ds1_filter_init: $i).
% 0.57/0.89 thf(sk__4_type, type, sk__4: $i).
% 0.57/0.89 thf(init_type, type, init: $i).
% 0.57/0.89 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $i > $o).
% 0.57/0.89 thf(zip_tseitin_4_type, type, zip_tseitin_4: $i > $i > $o).
% 0.57/0.89 thf(pminus_ds1_filter_init_type, type, pminus_ds1_filter_init: $i).
% 0.57/0.89 thf(zip_tseitin_10_type, type, zip_tseitin_10: $i > $i > $o).
% 0.57/0.89 thf(zip_tseitin_14_type, type, zip_tseitin_14: $i > $i > $o).
% 0.57/0.89 thf(zip_tseitin_9_type, type, zip_tseitin_9: $i > $i > $o).
% 0.57/0.89 thf(sk__19_type, type, sk__19: $i).
% 0.57/0.89 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $o).
% 0.57/0.89 thf(zip_tseitin_13_type, type, zip_tseitin_13: $i > $i > $o).
% 0.57/0.89 thf(sk__20_type, type, sk__20: $i).
% 0.57/0.89 thf(sk__7_type, type, sk__7: $i).
% 0.57/0.89 thf(h_ds1_filter_init_type, type, h_ds1_filter_init: $i).
% 0.57/0.89 thf(pred_type, type, pred: $i > $i).
% 0.57/0.89 thf(sk__13_type, type, sk__13: $i).
% 0.57/0.89 thf(sk__8_type, type, sk__8: $i).
% 0.57/0.89 thf(sk__18_type, type, sk__18: $i).
% 0.57/0.89 thf(pv64_type, type, pv64: $i).
% 0.57/0.89 thf(a_select3_type, type, a_select3: $i > $i > $i > $i).
% 0.57/0.89 thf(zip_tseitin_15_type, type, zip_tseitin_15: $i > $i > $o).
% 0.57/0.89 thf(sk__17_type, type, sk__17: $i).
% 0.57/0.89 thf(pv63_type, type, pv63: $i).
% 0.57/0.89 thf(zip_tseitin_11_type, type, zip_tseitin_11: $i > $i > $o).
% 0.57/0.89 thf(id_ds1_filter_init_type, type, id_ds1_filter_init: $i).
% 0.57/0.89 thf(zip_tseitin_16_type, type, zip_tseitin_16: $i > $i > $o).
% 0.57/0.89 thf(sk__10_type, type, sk__10: $i).
% 0.57/0.89 thf(zip_tseitin_18_type, type, zip_tseitin_18: $i > $i > $o).
% 0.57/0.89 thf(dv_ds1_filter_init_type, type, dv_ds1_filter_init: $i).
% 0.57/0.89 thf(gt_type, type, gt: $i > $i > $o).
% 0.57/0.89 thf(zip_tseitin_12_type, type, zip_tseitin_12: $i > $i > $o).
% 0.57/0.89 thf(sk__5_type, type, sk__5: $i).
% 0.57/0.89 thf(n1, axiom,
% 0.57/0.89 (( ( ![X19:$i]:
% 0.57/0.89 ( ( ( leq @ X19 @ ( pred @ pv63 ) ) & ( leq @ n0 @ X19 ) ) =>
% 0.57/0.89 ( ![X20:$i]:
% 0.57/0.89 ( ( ( leq @ X20 @ n5 ) & ( leq @ n0 @ X20 ) ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X19 @ X20 ) = ( init ) ) ) ) ) ) &
% 0.57/0.89 ( ![X17:$i,X18:$i]:
% 0.57/0.89 ( ( ( leq @ X18 @ n5 ) & ( leq @ X17 @ n5 ) & ( leq @ n0 @ X18 ) &
% 0.57/0.89 ( leq @ n0 @ X17 ) ) =>
% 0.57/0.89 ( ( gt @ pv63 @ X17 ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X17 @ X18 ) = ( init ) ) ) ) ) &
% 0.57/0.89 ( ![X15:$i,X16:$i]:
% 0.57/0.89 ( ( ( leq @ X16 @ n5 ) & ( leq @ X15 @ n5 ) & ( leq @ n0 @ X16 ) &
% 0.57/0.89 ( leq @ n0 @ X15 ) ) =>
% 0.57/0.89 ( ( ( gt @ pv64 @ X16 ) & ( ( X15 ) = ( pv63 ) ) ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X15 @ X16 ) = ( init ) ) ) ) ) &
% 0.57/0.89 ( ![X13:$i,X14:$i]:
% 0.57/0.89 ( ( ( leq @ X14 @ n5 ) & ( leq @ X13 @ n5 ) & ( leq @ n0 @ X14 ) &
% 0.57/0.89 ( leq @ n0 @ X13 ) ) =>
% 0.57/0.89 ( ( a_select3 @ pminus_ds1_filter_init @ X13 @ X14 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X11:$i,X12:$i]:
% 0.57/0.89 ( ( ( leq @ X12 @ n0 ) & ( leq @ X11 @ n5 ) & ( leq @ n0 @ X12 ) &
% 0.57/0.89 ( leq @ n0 @ X11 ) ) =>
% 0.57/0.89 ( ( a_select3 @ xhatmin_ds1_filter_init @ X11 @ X12 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X9:$i,X10:$i]:
% 0.57/0.89 ( ( ( leq @ X10 @ n2 ) & ( leq @ X9 @ n2 ) & ( leq @ n0 @ X10 ) &
% 0.57/0.89 ( leq @ n0 @ X9 ) ) =>
% 0.57/0.89 ( ( a_select3 @ r_ds1_filter_init @ X9 @ X10 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X7:$i,X8:$i]:
% 0.57/0.89 ( ( ( leq @ X8 @ n5 ) & ( leq @ X7 @ n5 ) & ( leq @ n0 @ X8 ) &
% 0.57/0.89 ( leq @ n0 @ X7 ) ) =>
% 0.57/0.89 ( ( a_select3 @ q_ds1_filter_init @ X7 @ X8 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X5:$i,X6:$i]:
% 0.57/0.89 ( ( ( leq @ X6 @ n0 ) & ( leq @ X5 @ n5 ) & ( leq @ n0 @ X6 ) &
% 0.57/0.89 ( leq @ n0 @ X5 ) ) =>
% 0.57/0.89 ( ( a_select3 @ dv_ds1_filter_init @ X5 @ X6 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X3:$i,X4:$i]:
% 0.57/0.89 ( ( ( leq @ X4 @ n5 ) & ( leq @ X3 @ n5 ) & ( leq @ n0 @ X4 ) &
% 0.57/0.89 ( leq @ n0 @ X3 ) ) =>
% 0.57/0.89 ( ( a_select3 @ phi_ds1_filter_init @ X3 @ X4 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X1:$i,X2:$i]:
% 0.57/0.89 ( ( ( leq @ X2 @ n5 ) & ( leq @ X1 @ n2 ) & ( leq @ n0 @ X2 ) &
% 0.57/0.89 ( leq @ n0 @ X1 ) ) =>
% 0.57/0.89 ( ( a_select3 @ h_ds1_filter_init @ X1 @ X2 ) = ( init ) ) ) ) &
% 0.57/0.89 ( leq @ pv64 @ n5 ) & ( leq @ pv63 @ n5 ) & ( leq @ pv5 @ n998 ) &
% 0.57/0.89 ( leq @ n0 @ pv64 ) & ( leq @ n0 @ pv63 ) & ( leq @ n0 @ pv5 ) &
% 0.57/0.89 ( ( pv63 ) != ( pv64 ) ) ) =>
% 0.57/0.89 ( ![X21:$i,X22:$i]:
% 0.57/0.89 ( ( ( leq @ X22 @ n5 ) & ( leq @ X21 @ n5 ) & ( leq @ n0 @ X22 ) &
% 0.57/0.89 ( leq @ n0 @ X21 ) ) =>
% 0.57/0.89 ( ( ( leq @ X22 @ pv64 ) & ( ( X21 ) = ( pv63 ) ) &
% 0.57/0.89 ( ( pv64 ) != ( X22 ) ) ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X21 @ X22 ) = ( init ) ) ) ) ))).
% 0.57/0.89 thf(zf_stmt_0, axiom,
% 0.57/0.89 (![X2:$i,X1:$i]:
% 0.57/0.89 ( ( ( zip_tseitin_18 @ X2 @ X1 ) =>
% 0.57/0.89 ( ( a_select3 @ h_ds1_filter_init @ X1 @ X2 ) = ( init ) ) ) =>
% 0.57/0.89 ( zip_tseitin_19 @ X2 @ X1 ) ))).
% 0.57/0.89 thf(zip_derived_cl47, plain,
% 0.57/0.89 (![X0 : $i, X1 : $i]:
% 0.57/0.89 ( (zip_tseitin_19 @ X0 @ X1) | (zip_tseitin_18 @ X0 @ X1))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.57/0.89 thf(zf_stmt_1, type, zip_tseitin_19 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_2, type, zip_tseitin_18 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_3, axiom,
% 0.57/0.89 (![X2:$i,X1:$i]:
% 0.57/0.89 ( ( zip_tseitin_18 @ X2 @ X1 ) =>
% 0.57/0.89 ( ( leq @ n0 @ X1 ) & ( leq @ n0 @ X2 ) & ( leq @ X1 @ n2 ) &
% 0.57/0.89 ( leq @ X2 @ n5 ) ) ))).
% 0.57/0.89 thf(zf_stmt_4, type, zip_tseitin_17 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_5, axiom,
% 0.57/0.89 (![X4:$i,X3:$i]:
% 0.57/0.89 ( ( ( zip_tseitin_4 @ X4 @ X3 ) =>
% 0.57/0.89 ( ( a_select3 @ phi_ds1_filter_init @ X3 @ X4 ) = ( init ) ) ) =>
% 0.57/0.89 ( zip_tseitin_17 @ X4 @ X3 ) ))).
% 0.57/0.89 thf(zf_stmt_6, type, zip_tseitin_16 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_7, axiom,
% 0.57/0.89 (![X6:$i,X5:$i]:
% 0.57/0.89 ( ( ( zip_tseitin_11 @ X6 @ X5 ) =>
% 0.57/0.89 ( ( a_select3 @ dv_ds1_filter_init @ X5 @ X6 ) = ( init ) ) ) =>
% 0.57/0.89 ( zip_tseitin_16 @ X6 @ X5 ) ))).
% 0.57/0.89 thf(zf_stmt_8, type, zip_tseitin_15 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_9, axiom,
% 0.57/0.89 (![X8:$i,X7:$i]:
% 0.57/0.89 ( ( ( zip_tseitin_4 @ X8 @ X7 ) =>
% 0.57/0.89 ( ( a_select3 @ q_ds1_filter_init @ X7 @ X8 ) = ( init ) ) ) =>
% 0.57/0.89 ( zip_tseitin_15 @ X8 @ X7 ) ))).
% 0.57/0.89 thf(zf_stmt_10, type, zip_tseitin_14 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_11, axiom,
% 0.57/0.89 (![X10:$i,X9:$i]:
% 0.57/0.89 ( ( ( zip_tseitin_13 @ X10 @ X9 ) =>
% 0.57/0.89 ( ( a_select3 @ r_ds1_filter_init @ X9 @ X10 ) = ( init ) ) ) =>
% 0.57/0.89 ( zip_tseitin_14 @ X10 @ X9 ) ))).
% 0.57/0.89 thf(zf_stmt_12, type, zip_tseitin_13 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_13, axiom,
% 0.57/0.89 (![X10:$i,X9:$i]:
% 0.57/0.89 ( ( zip_tseitin_13 @ X10 @ X9 ) =>
% 0.57/0.89 ( ( leq @ n0 @ X9 ) & ( leq @ n0 @ X10 ) & ( leq @ X9 @ n2 ) &
% 0.57/0.89 ( leq @ X10 @ n2 ) ) ))).
% 0.57/0.89 thf(zf_stmt_14, type, zip_tseitin_12 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_15, axiom,
% 0.57/0.89 (![X12:$i,X11:$i]:
% 0.57/0.89 ( ( ( zip_tseitin_11 @ X12 @ X11 ) =>
% 0.57/0.89 ( ( a_select3 @ xhatmin_ds1_filter_init @ X11 @ X12 ) = ( init ) ) ) =>
% 0.57/0.89 ( zip_tseitin_12 @ X12 @ X11 ) ))).
% 0.57/0.89 thf(zf_stmt_16, type, zip_tseitin_11 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_17, axiom,
% 0.57/0.89 (![X12:$i,X11:$i]:
% 0.57/0.89 ( ( zip_tseitin_11 @ X12 @ X11 ) =>
% 0.57/0.89 ( ( leq @ n0 @ X11 ) & ( leq @ n0 @ X12 ) & ( leq @ X11 @ n5 ) &
% 0.57/0.89 ( leq @ X12 @ n0 ) ) ))).
% 0.57/0.89 thf(zf_stmt_18, type, zip_tseitin_10 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_19, axiom,
% 0.57/0.89 (![X14:$i,X13:$i]:
% 0.57/0.89 ( ( ( zip_tseitin_4 @ X14 @ X13 ) =>
% 0.57/0.89 ( ( a_select3 @ pminus_ds1_filter_init @ X13 @ X14 ) = ( init ) ) ) =>
% 0.57/0.89 ( zip_tseitin_10 @ X14 @ X13 ) ))).
% 0.57/0.89 thf(zf_stmt_20, type, zip_tseitin_9 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_21, axiom,
% 0.57/0.89 (![X16:$i,X15:$i]:
% 0.57/0.89 ( ( ( zip_tseitin_4 @ X16 @ X15 ) => ( zip_tseitin_8 @ X16 @ X15 ) ) =>
% 0.57/0.89 ( zip_tseitin_9 @ X16 @ X15 ) ))).
% 0.57/0.89 thf(zf_stmt_22, type, zip_tseitin_8 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_23, axiom,
% 0.57/0.89 (![X16:$i,X15:$i]:
% 0.57/0.89 ( ( ( zip_tseitin_7 @ X16 @ X15 ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X15 @ X16 ) = ( init ) ) ) =>
% 0.57/0.89 ( zip_tseitin_8 @ X16 @ X15 ) ))).
% 0.57/0.89 thf(zf_stmt_24, type, zip_tseitin_7 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_25, axiom,
% 0.57/0.89 (![X16:$i,X15:$i]:
% 0.57/0.89 ( ( zip_tseitin_7 @ X16 @ X15 ) =>
% 0.57/0.89 ( ( ( X15 ) = ( pv63 ) ) & ( gt @ pv64 @ X16 ) ) ))).
% 0.57/0.89 thf(zf_stmt_26, type, zip_tseitin_6 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_27, axiom,
% 0.57/0.89 (![X18:$i,X17:$i]:
% 0.57/0.89 ( ( ( zip_tseitin_4 @ X18 @ X17 ) => ( zip_tseitin_5 @ X18 @ X17 ) ) =>
% 0.57/0.89 ( zip_tseitin_6 @ X18 @ X17 ) ))).
% 0.57/0.89 thf(zf_stmt_28, type, zip_tseitin_5 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_29, axiom,
% 0.57/0.89 (![X18:$i,X17:$i]:
% 0.57/0.89 ( ( ( gt @ pv63 @ X17 ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X17 @ X18 ) = ( init ) ) ) =>
% 0.57/0.89 ( zip_tseitin_5 @ X18 @ X17 ) ))).
% 0.57/0.89 thf(zf_stmt_30, type, zip_tseitin_4 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_31, axiom,
% 0.57/0.89 (![X18:$i,X17:$i]:
% 0.57/0.89 ( ( zip_tseitin_4 @ X18 @ X17 ) =>
% 0.57/0.89 ( ( leq @ n0 @ X17 ) & ( leq @ n0 @ X18 ) & ( leq @ X17 @ n5 ) &
% 0.57/0.89 ( leq @ X18 @ n5 ) ) ))).
% 0.57/0.89 thf(zf_stmt_32, type, zip_tseitin_3 : $i > $o).
% 0.57/0.89 thf(zf_stmt_33, axiom,
% 0.57/0.89 (![X19:$i]:
% 0.57/0.89 ( ( ( zip_tseitin_0 @ X19 ) =>
% 0.57/0.89 ( ![X20:$i]: ( zip_tseitin_2 @ X20 @ X19 ) ) ) =>
% 0.57/0.89 ( zip_tseitin_3 @ X19 ) ))).
% 0.57/0.89 thf(zf_stmt_34, type, zip_tseitin_2 : $i > $i > $o).
% 0.57/0.89 thf(zf_stmt_35, axiom,
% 0.57/0.89 (![X20:$i,X19:$i]:
% 0.57/0.89 ( ( ( zip_tseitin_1 @ X20 ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X19 @ X20 ) = ( init ) ) ) =>
% 0.57/0.89 ( zip_tseitin_2 @ X20 @ X19 ) ))).
% 0.57/0.89 thf(zf_stmt_36, type, zip_tseitin_1 : $i > $o).
% 0.57/0.89 thf(zf_stmt_37, axiom,
% 0.57/0.89 (![X20:$i]:
% 0.57/0.89 ( ( zip_tseitin_1 @ X20 ) => ( ( leq @ n0 @ X20 ) & ( leq @ X20 @ n5 ) ) ))).
% 0.57/0.89 thf(zf_stmt_38, type, zip_tseitin_0 : $i > $o).
% 0.57/0.89 thf(zf_stmt_39, axiom,
% 0.57/0.89 (![X19:$i]:
% 0.57/0.89 ( ( zip_tseitin_0 @ X19 ) =>
% 0.57/0.89 ( ( leq @ n0 @ X19 ) & ( leq @ X19 @ ( pred @ pv63 ) ) ) ))).
% 0.57/0.89 thf(zf_stmt_40, axiom,
% 0.57/0.89 (( ( ( pv63 ) != ( pv64 ) ) & ( leq @ n0 @ pv5 ) & ( leq @ n0 @ pv63 ) &
% 0.57/0.89 ( leq @ n0 @ pv64 ) & ( leq @ pv5 @ n998 ) & ( leq @ pv63 @ n5 ) &
% 0.57/0.89 ( leq @ pv64 @ n5 ) &
% 0.57/0.89 ( ![X1:$i,X2:$i]: ( zip_tseitin_19 @ X2 @ X1 ) ) &
% 0.57/0.89 ( ![X3:$i,X4:$i]: ( zip_tseitin_17 @ X4 @ X3 ) ) &
% 0.57/0.89 ( ![X5:$i,X6:$i]: ( zip_tseitin_16 @ X6 @ X5 ) ) &
% 0.57/0.89 ( ![X7:$i,X8:$i]: ( zip_tseitin_15 @ X8 @ X7 ) ) &
% 0.57/0.89 ( ![X9:$i,X10:$i]: ( zip_tseitin_14 @ X10 @ X9 ) ) &
% 0.57/0.89 ( ![X11:$i,X12:$i]: ( zip_tseitin_12 @ X12 @ X11 ) ) &
% 0.57/0.89 ( ![X13:$i,X14:$i]: ( zip_tseitin_10 @ X14 @ X13 ) ) &
% 0.57/0.89 ( ![X15:$i,X16:$i]: ( zip_tseitin_9 @ X16 @ X15 ) ) &
% 0.57/0.89 ( ![X17:$i,X18:$i]: ( zip_tseitin_6 @ X18 @ X17 ) ) &
% 0.57/0.89 ( ![X19:$i]: ( zip_tseitin_3 @ X19 ) ) ) =>
% 0.57/0.89 ( ![X21:$i,X22:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X21 ) & ( leq @ n0 @ X22 ) & ( leq @ X21 @ n5 ) &
% 0.57/0.89 ( leq @ X22 @ n5 ) ) =>
% 0.57/0.89 ( ( ( ( pv64 ) != ( X22 ) ) & ( ( X21 ) = ( pv63 ) ) &
% 0.57/0.89 ( leq @ X22 @ pv64 ) ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X21 @ X22 ) = ( init ) ) ) ) ))).
% 0.57/0.89 thf(zip_derived_cl48, plain,
% 0.57/0.89 (![X0 : $i, X1 : $i]:
% 0.57/0.89 (((pv64) = (X0))
% 0.57/0.89 | ~ (leq @ X0 @ pv64)
% 0.57/0.89 | ((a_select3 @ id_ds1_filter_init @ X1 @ X0) = (init))
% 0.57/0.89 | ~ (leq @ X0 @ n5)
% 0.57/0.89 | ~ (leq @ n0 @ X0)
% 0.57/0.89 | ~ (leq @ n0 @ X1)
% 0.57/0.89 | ~ (leq @ X1 @ n5)
% 0.57/0.89 | ((X1) != (pv63))
% 0.57/0.89 | ~ (zip_tseitin_3 @ sk__1)
% 0.57/0.89 | ~ (zip_tseitin_6 @ sk__3 @ sk__2)
% 0.57/0.89 | ~ (zip_tseitin_9 @ sk__5 @ sk__4)
% 0.57/0.89 | ~ (zip_tseitin_10 @ sk__7 @ sk__6)
% 0.57/0.89 | ~ (zip_tseitin_12 @ sk__9 @ sk__8)
% 0.57/0.89 | ~ (zip_tseitin_14 @ sk__11 @ sk__10)
% 0.57/0.89 | ~ (zip_tseitin_15 @ sk__13 @ sk__12)
% 0.57/0.89 | ~ (zip_tseitin_16 @ sk__15 @ sk__14)
% 0.57/0.89 | ~ (zip_tseitin_17 @ sk__17 @ sk__16)
% 0.57/0.89 | ~ (zip_tseitin_19 @ sk__19 @ sk__18)
% 0.57/0.89 | ~ (leq @ pv64 @ n5)
% 0.57/0.89 | ~ (leq @ pv63 @ n5)
% 0.57/0.89 | ~ (leq @ pv5 @ n998)
% 0.57/0.89 | ~ (leq @ n0 @ pv64)
% 0.57/0.89 | ~ (leq @ n0 @ pv63)
% 0.57/0.89 | ~ (leq @ n0 @ pv5)
% 0.57/0.89 | ((pv63) = (pv64)))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_40])).
% 0.57/0.89 thf(zip_derived_cl81, plain,
% 0.57/0.89 ((~ (zip_tseitin_19 @ sk__19 @ sk__18))
% 0.57/0.89 <= (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)))),
% 0.57/0.89 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.89 thf(zip_derived_cl221, plain,
% 0.57/0.89 (( (zip_tseitin_18 @ sk__19 @ sk__18))
% 0.57/0.89 <= (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl47, zip_derived_cl81])).
% 0.57/0.89 thf(zip_derived_cl43, plain,
% 0.57/0.89 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_18 @ X0 @ X1))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.57/0.89 thf(zip_derived_cl235, plain,
% 0.57/0.89 (( (leq @ n0 @ sk__19)) <= (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl221, zip_derived_cl43])).
% 0.57/0.89 thf(n91, conjecture,
% 0.57/0.89 (( ( ( pv63 ) != ( pv64 ) ) & ( leq @ n0 @ pv5 ) & ( leq @ n0 @ pv63 ) &
% 0.57/0.89 ( leq @ n0 @ pv64 ) & ( leq @ pv5 @ n998 ) & ( leq @ pv63 @ n5 ) &
% 0.57/0.89 ( leq @ pv64 @ n5 ) &
% 0.57/0.89 ( ![X1:$i,X2:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X1 ) & ( leq @ n0 @ X2 ) & ( leq @ X1 @ n2 ) &
% 0.57/0.89 ( leq @ X2 @ n5 ) ) =>
% 0.57/0.89 ( ( a_select3 @ h_ds1_filter_init @ X1 @ X2 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X3:$i,X4:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X3 ) & ( leq @ n0 @ X4 ) & ( leq @ X3 @ n5 ) &
% 0.57/0.89 ( leq @ X4 @ n5 ) ) =>
% 0.57/0.89 ( ( a_select3 @ phi_ds1_filter_init @ X3 @ X4 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X5:$i,X6:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X5 ) & ( leq @ n0 @ X6 ) & ( leq @ X5 @ n5 ) &
% 0.57/0.89 ( leq @ X6 @ n0 ) ) =>
% 0.57/0.89 ( ( a_select3 @ dv_ds1_filter_init @ X5 @ X6 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X7:$i,X8:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X7 ) & ( leq @ n0 @ X8 ) & ( leq @ X7 @ n5 ) &
% 0.57/0.89 ( leq @ X8 @ n5 ) ) =>
% 0.57/0.89 ( ( a_select3 @ q_ds1_filter_init @ X7 @ X8 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X9:$i,X10:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X9 ) & ( leq @ n0 @ X10 ) & ( leq @ X9 @ n2 ) &
% 0.57/0.89 ( leq @ X10 @ n2 ) ) =>
% 0.57/0.89 ( ( a_select3 @ r_ds1_filter_init @ X9 @ X10 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X11:$i,X12:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X11 ) & ( leq @ n0 @ X12 ) & ( leq @ X11 @ n5 ) &
% 0.57/0.89 ( leq @ X12 @ n0 ) ) =>
% 0.57/0.89 ( ( a_select3 @ xhatmin_ds1_filter_init @ X11 @ X12 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X13:$i,X14:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X13 ) & ( leq @ n0 @ X14 ) & ( leq @ X13 @ n5 ) &
% 0.57/0.89 ( leq @ X14 @ n5 ) ) =>
% 0.57/0.89 ( ( a_select3 @ pminus_ds1_filter_init @ X13 @ X14 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X15:$i,X16:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X15 ) & ( leq @ n0 @ X16 ) & ( leq @ X15 @ n5 ) &
% 0.57/0.89 ( leq @ X16 @ n5 ) ) =>
% 0.57/0.89 ( ( ( ( X15 ) = ( pv63 ) ) & ( gt @ pv64 @ X16 ) ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X15 @ X16 ) = ( init ) ) ) ) ) &
% 0.57/0.89 ( ![X17:$i,X18:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X17 ) & ( leq @ n0 @ X18 ) & ( leq @ X17 @ n5 ) &
% 0.57/0.89 ( leq @ X18 @ n5 ) ) =>
% 0.57/0.89 ( ( gt @ pv63 @ X17 ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X17 @ X18 ) = ( init ) ) ) ) ) &
% 0.57/0.89 ( ![X19:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X19 ) & ( leq @ X19 @ ( pred @ pv63 ) ) ) =>
% 0.57/0.89 ( ![X20:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X20 ) & ( leq @ X20 @ n5 ) ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X19 @ X20 ) = ( init ) ) ) ) ) ) ) =>
% 0.57/0.89 ( ![X21:$i,X22:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X21 ) & ( leq @ n0 @ X22 ) & ( leq @ X21 @ n5 ) &
% 0.57/0.89 ( leq @ X22 @ n5 ) ) =>
% 0.57/0.89 ( ( ( ( pv64 ) != ( X22 ) ) & ( ( X21 ) = ( pv63 ) ) &
% 0.57/0.89 ( leq @ X22 @ pv64 ) ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X21 @ X22 ) = ( init ) ) ) ) ))).
% 0.57/0.89 thf(zf_stmt_41, negated_conjecture,
% 0.57/0.89 (~( ( ( ( pv63 ) != ( pv64 ) ) & ( leq @ n0 @ pv5 ) &
% 0.57/0.89 ( leq @ n0 @ pv63 ) & ( leq @ n0 @ pv64 ) & ( leq @ pv5 @ n998 ) &
% 0.57/0.89 ( leq @ pv63 @ n5 ) & ( leq @ pv64 @ n5 ) &
% 0.57/0.89 ( ![X1:$i,X2:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X1 ) & ( leq @ n0 @ X2 ) & ( leq @ X1 @ n2 ) &
% 0.57/0.89 ( leq @ X2 @ n5 ) ) =>
% 0.57/0.89 ( ( a_select3 @ h_ds1_filter_init @ X1 @ X2 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X3:$i,X4:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X3 ) & ( leq @ n0 @ X4 ) & ( leq @ X3 @ n5 ) &
% 0.57/0.89 ( leq @ X4 @ n5 ) ) =>
% 0.57/0.89 ( ( a_select3 @ phi_ds1_filter_init @ X3 @ X4 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X5:$i,X6:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X5 ) & ( leq @ n0 @ X6 ) & ( leq @ X5 @ n5 ) &
% 0.57/0.89 ( leq @ X6 @ n0 ) ) =>
% 0.57/0.89 ( ( a_select3 @ dv_ds1_filter_init @ X5 @ X6 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X7:$i,X8:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X7 ) & ( leq @ n0 @ X8 ) & ( leq @ X7 @ n5 ) &
% 0.57/0.89 ( leq @ X8 @ n5 ) ) =>
% 0.57/0.89 ( ( a_select3 @ q_ds1_filter_init @ X7 @ X8 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X9:$i,X10:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X9 ) & ( leq @ n0 @ X10 ) & ( leq @ X9 @ n2 ) &
% 0.57/0.89 ( leq @ X10 @ n2 ) ) =>
% 0.57/0.89 ( ( a_select3 @ r_ds1_filter_init @ X9 @ X10 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X11:$i,X12:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X11 ) & ( leq @ n0 @ X12 ) & ( leq @ X11 @ n5 ) &
% 0.57/0.89 ( leq @ X12 @ n0 ) ) =>
% 0.57/0.89 ( ( a_select3 @ xhatmin_ds1_filter_init @ X11 @ X12 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X13:$i,X14:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X13 ) & ( leq @ n0 @ X14 ) & ( leq @ X13 @ n5 ) &
% 0.57/0.89 ( leq @ X14 @ n5 ) ) =>
% 0.57/0.89 ( ( a_select3 @ pminus_ds1_filter_init @ X13 @ X14 ) = ( init ) ) ) ) &
% 0.57/0.89 ( ![X15:$i,X16:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X15 ) & ( leq @ n0 @ X16 ) & ( leq @ X15 @ n5 ) &
% 0.57/0.89 ( leq @ X16 @ n5 ) ) =>
% 0.57/0.89 ( ( ( ( X15 ) = ( pv63 ) ) & ( gt @ pv64 @ X16 ) ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X15 @ X16 ) = ( init ) ) ) ) ) &
% 0.57/0.89 ( ![X17:$i,X18:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X17 ) & ( leq @ n0 @ X18 ) & ( leq @ X17 @ n5 ) &
% 0.57/0.89 ( leq @ X18 @ n5 ) ) =>
% 0.57/0.89 ( ( gt @ pv63 @ X17 ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X17 @ X18 ) = ( init ) ) ) ) ) &
% 0.57/0.89 ( ![X19:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X19 ) & ( leq @ X19 @ ( pred @ pv63 ) ) ) =>
% 0.57/0.89 ( ![X20:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X20 ) & ( leq @ X20 @ n5 ) ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X19 @ X20 ) = ( init ) ) ) ) ) ) ) =>
% 0.57/0.89 ( ![X21:$i,X22:$i]:
% 0.57/0.89 ( ( ( leq @ n0 @ X21 ) & ( leq @ n0 @ X22 ) & ( leq @ X21 @ n5 ) &
% 0.57/0.89 ( leq @ X22 @ n5 ) ) =>
% 0.57/0.89 ( ( ( ( pv64 ) != ( X22 ) ) & ( ( X21 ) = ( pv63 ) ) &
% 0.57/0.89 ( leq @ X22 @ pv64 ) ) =>
% 0.57/0.89 ( ( a_select3 @ id_ds1_filter_init @ X21 @ X22 ) = ( init ) ) ) ) ) )),
% 0.57/0.89 inference('cnf.neg', [status(esa)], [n91])).
% 0.57/0.89 thf(zip_derived_cl56, plain,
% 0.57/0.89 (![X0 : $i, X1 : $i]:
% 0.57/0.89 (~ (leq @ X0 @ n2)
% 0.57/0.89 | ~ (leq @ n0 @ X0)
% 0.57/0.89 | ~ (leq @ n0 @ X1)
% 0.57/0.89 | ~ (leq @ X1 @ n5)
% 0.57/0.89 | ((a_select3 @ h_ds1_filter_init @ X0 @ X1) = (init)))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.89 thf(zip_derived_cl46, plain,
% 0.57/0.89 (![X0 : $i, X1 : $i]:
% 0.57/0.89 ( (zip_tseitin_19 @ X0 @ X1)
% 0.57/0.89 | ((a_select3 @ h_ds1_filter_init @ X1 @ X0) != (init)))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.57/0.89 thf(zip_derived_cl81, plain,
% 0.57/0.89 ((~ (zip_tseitin_19 @ sk__19 @ sk__18))
% 0.57/0.89 <= (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)))),
% 0.57/0.89 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.89 thf(zip_derived_cl209, plain,
% 0.57/0.89 ((((a_select3 @ h_ds1_filter_init @ sk__18 @ sk__19) != (init)))
% 0.57/0.89 <= (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl46, zip_derived_cl81])).
% 0.57/0.89 thf(zip_derived_cl223, plain,
% 0.57/0.89 (((~ (leq @ sk__19 @ n5)
% 0.57/0.89 | ~ (leq @ n0 @ sk__19)
% 0.57/0.89 | ~ (leq @ n0 @ sk__18)
% 0.57/0.89 | ~ (leq @ sk__18 @ n2)
% 0.57/0.89 | ((init) != (init)))) <= (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl56, zip_derived_cl209])).
% 0.57/0.89 thf(zip_derived_cl224, plain,
% 0.57/0.89 (((~ (leq @ sk__18 @ n2)
% 0.57/0.89 | ~ (leq @ n0 @ sk__18)
% 0.57/0.89 | ~ (leq @ n0 @ sk__19)
% 0.57/0.89 | ~ (leq @ sk__19 @ n5))) <= (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)))),
% 0.57/0.89 inference('simplify', [status(thm)], [zip_derived_cl223])).
% 0.57/0.89 thf(zip_derived_cl226, plain,
% 0.57/0.89 ((~ (leq @ n0 @ sk__19)) <= (~ ( (leq @ n0 @ sk__19)))),
% 0.57/0.89 inference('split', [status(esa)], [zip_derived_cl224])).
% 0.57/0.89 thf('0', plain,
% 0.57/0.89 (( (leq @ n0 @ sk__19)) | ( (zip_tseitin_19 @ sk__19 @ sk__18))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl235, zip_derived_cl226])).
% 0.57/0.89 thf(zip_derived_cl91, plain, ((((pv63) = (pv64))) <= ((((pv63) = (pv64))))),
% 0.57/0.89 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.89 thf(zip_derived_cl49, plain, (((pv63) != (pv64))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.89 thf('1', plain, (~ (((pv63) = (pv64)))),
% 0.57/0.89 inference('simplify_reflect-', [status(thm)],
% 0.57/0.89 [zip_derived_cl91, zip_derived_cl49])).
% 0.57/0.89 thf(zip_derived_cl53, plain, ( (leq @ pv5 @ n998)),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.89 thf(zip_derived_cl78, plain,
% 0.57/0.89 ((~ (leq @ pv5 @ n998)) <= (~ ( (leq @ pv5 @ n998)))),
% 0.57/0.89 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.89 thf('2', plain, (( (leq @ pv5 @ n998))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl78])).
% 0.57/0.89 thf(zip_derived_cl55, plain, ( (leq @ pv64 @ n5)),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.89 thf(zip_derived_cl80, plain,
% 0.57/0.89 ((~ (leq @ pv64 @ n5)) <= (~ ( (leq @ pv64 @ n5)))),
% 0.57/0.89 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.89 thf('3', plain, (( (leq @ pv64 @ n5))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl55, zip_derived_cl80])).
% 0.57/0.89 thf(zip_derived_cl20, plain,
% 0.57/0.89 (![X0 : $i, X1 : $i]:
% 0.57/0.89 ( (zip_tseitin_9 @ X0 @ X1) | ~ (zip_tseitin_8 @ X0 @ X1))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_21])).
% 0.57/0.89 thf(zip_derived_cl88, plain,
% 0.57/0.89 ((~ (zip_tseitin_9 @ sk__5 @ sk__4))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.89 thf(zip_derived_cl143, plain,
% 0.57/0.89 ((~ (zip_tseitin_8 @ sk__5 @ sk__4))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl88])).
% 0.57/0.89 thf(zip_derived_cl19, plain,
% 0.57/0.89 (![X0 : $i, X1 : $i]:
% 0.57/0.89 ( (zip_tseitin_8 @ X0 @ X1) | (zip_tseitin_7 @ X0 @ X1))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_23])).
% 0.57/0.89 thf(zip_derived_cl146, plain,
% 0.57/0.89 (( (zip_tseitin_7 @ sk__5 @ sk__4))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup+', [status(thm)], [zip_derived_cl143, zip_derived_cl19])).
% 0.57/0.89 thf(zip_derived_cl146, plain,
% 0.57/0.89 (( (zip_tseitin_7 @ sk__5 @ sk__4))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup+', [status(thm)], [zip_derived_cl143, zip_derived_cl19])).
% 0.57/0.89 thf(zip_derived_cl16, plain,
% 0.57/0.89 (![X0 : $i, X1 : $i]: (((X0) = (pv63)) | ~ (zip_tseitin_7 @ X1 @ X0))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_25])).
% 0.57/0.89 thf(zip_derived_cl151, plain,
% 0.57/0.89 ((((sk__4) = (pv63))) <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl146, zip_derived_cl16])).
% 0.57/0.89 thf(zip_derived_cl158, plain,
% 0.57/0.89 (( (zip_tseitin_7 @ sk__5 @ pv63))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('demod', [status(thm)], [zip_derived_cl146, zip_derived_cl151])).
% 0.57/0.89 thf(zip_derived_cl17, plain,
% 0.57/0.89 (![X0 : $i, X1 : $i]: ( (gt @ pv64 @ X0) | ~ (zip_tseitin_7 @ X0 @ X1))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_25])).
% 0.57/0.89 thf(zip_derived_cl172, plain,
% 0.57/0.89 (( (gt @ pv64 @ sk__5)) <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl158, zip_derived_cl17])).
% 0.57/0.89 thf(zip_derived_cl63, plain,
% 0.57/0.89 (![X14 : $i, X15 : $i]:
% 0.57/0.89 (((X14) != (pv63))
% 0.57/0.89 | ~ (leq @ X14 @ n5)
% 0.57/0.89 | ~ (leq @ n0 @ X14)
% 0.57/0.89 | ~ (leq @ n0 @ X15)
% 0.57/0.89 | ~ (leq @ X15 @ n5)
% 0.57/0.89 | ((a_select3 @ id_ds1_filter_init @ X14 @ X15) = (init))
% 0.57/0.89 | ~ (gt @ pv64 @ X15))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.89 thf(zip_derived_cl270, plain,
% 0.57/0.89 ((![X0 : $i]:
% 0.57/0.89 (((X0) != (pv63))
% 0.57/0.89 | ~ (leq @ X0 @ n5)
% 0.57/0.89 | ~ (leq @ n0 @ X0)
% 0.57/0.89 | ~ (leq @ n0 @ sk__5)
% 0.57/0.89 | ~ (leq @ sk__5 @ n5)
% 0.57/0.89 | ((a_select3 @ id_ds1_filter_init @ X0 @ sk__5) = (init))))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl172, zip_derived_cl63])).
% 0.57/0.89 thf(zip_derived_cl88, plain,
% 0.57/0.89 ((~ (zip_tseitin_9 @ sk__5 @ sk__4))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.89 thf(zip_derived_cl151, plain,
% 0.57/0.89 ((((sk__4) = (pv63))) <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl146, zip_derived_cl16])).
% 0.57/0.89 thf(zip_derived_cl155, plain,
% 0.57/0.89 ((~ (zip_tseitin_9 @ sk__5 @ pv63))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('demod', [status(thm)], [zip_derived_cl88, zip_derived_cl151])).
% 0.57/0.89 thf(zip_derived_cl21, plain,
% 0.57/0.89 (![X0 : $i, X1 : $i]:
% 0.57/0.89 ( (zip_tseitin_9 @ X0 @ X1) | (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_21])).
% 0.57/0.89 thf(zip_derived_cl160, plain,
% 0.57/0.89 (( (zip_tseitin_4 @ sk__5 @ pv63))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup+', [status(thm)], [zip_derived_cl155, zip_derived_cl21])).
% 0.57/0.89 thf(zip_derived_cl9, plain,
% 0.57/0.89 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.89 thf(zip_derived_cl175, plain,
% 0.57/0.89 (( (leq @ n0 @ sk__5)) <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl160, zip_derived_cl9])).
% 0.57/0.89 thf(zip_derived_cl160, plain,
% 0.57/0.89 (( (zip_tseitin_4 @ sk__5 @ pv63))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup+', [status(thm)], [zip_derived_cl155, zip_derived_cl21])).
% 0.57/0.89 thf(zip_derived_cl11, plain,
% 0.57/0.89 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n5) | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.89 thf(zip_derived_cl176, plain,
% 0.57/0.89 (( (leq @ sk__5 @ n5)) <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl160, zip_derived_cl11])).
% 0.57/0.89 thf(zip_derived_cl271, plain,
% 0.57/0.89 ((![X0 : $i]:
% 0.57/0.89 (((X0) != (pv63))
% 0.57/0.89 | ~ (leq @ X0 @ n5)
% 0.57/0.89 | ~ (leq @ n0 @ X0)
% 0.57/0.89 | ((a_select3 @ id_ds1_filter_init @ X0 @ sk__5) = (init))))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('demod', [status(thm)],
% 0.57/0.89 [zip_derived_cl270, zip_derived_cl175, zip_derived_cl176])).
% 0.57/0.89 thf(zip_derived_cl143, plain,
% 0.57/0.89 ((~ (zip_tseitin_8 @ sk__5 @ sk__4))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl88])).
% 0.57/0.89 thf(zip_derived_cl18, plain,
% 0.57/0.89 (![X0 : $i, X1 : $i]:
% 0.57/0.89 ( (zip_tseitin_8 @ X0 @ X1)
% 0.57/0.89 | ((a_select3 @ id_ds1_filter_init @ X1 @ X0) != (init)))),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_23])).
% 0.57/0.89 thf(zip_derived_cl145, plain,
% 0.57/0.89 ((((a_select3 @ id_ds1_filter_init @ sk__4 @ sk__5) != (init)))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup+', [status(thm)], [zip_derived_cl143, zip_derived_cl18])).
% 0.57/0.89 thf(zip_derived_cl151, plain,
% 0.57/0.89 ((((sk__4) = (pv63))) <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl146, zip_derived_cl16])).
% 0.57/0.89 thf(zip_derived_cl157, plain,
% 0.57/0.89 ((((a_select3 @ id_ds1_filter_init @ pv63 @ sk__5) != (init)))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('demod', [status(thm)], [zip_derived_cl145, zip_derived_cl151])).
% 0.57/0.89 thf(zip_derived_cl272, plain,
% 0.57/0.89 (((~ (leq @ n0 @ pv63)
% 0.57/0.89 | ~ (leq @ pv63 @ n5)
% 0.57/0.89 | ((pv63) != (pv63))
% 0.57/0.89 | ((init) != (init)))) <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.89 inference('s_sup-', [status(thm)], [zip_derived_cl271, zip_derived_cl157])).
% 0.57/0.89 thf(zip_derived_cl51, plain, ( (leq @ n0 @ pv63)),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.89 thf(zip_derived_cl54, plain, ( (leq @ pv63 @ n5)),
% 0.57/0.89 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.89 thf(zip_derived_cl273, plain,
% 0.57/0.89 (((((pv63) != (pv63)) | ((init) != (init))))
% 0.57/0.89 <= (~ ( (zip_tseitin_9 @ sk__5 @ sk__4)))),
% 0.57/0.90 inference('demod', [status(thm)],
% 0.57/0.90 [zip_derived_cl272, zip_derived_cl51, zip_derived_cl54])).
% 0.57/0.90 thf('4', plain, (( (zip_tseitin_9 @ sk__5 @ sk__4))),
% 0.57/0.90 inference('simplify', [status(thm)], [zip_derived_cl273])).
% 0.57/0.90 thf(zip_derived_cl62, plain,
% 0.57/0.90 (![X12 : $i, X13 : $i]:
% 0.57/0.90 (~ (leq @ X12 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ X12)
% 0.57/0.90 | ~ (leq @ n0 @ X13)
% 0.57/0.90 | ~ (leq @ X13 @ n5)
% 0.57/0.90 | ((a_select3 @ pminus_ds1_filter_init @ X12 @ X13) = (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl22, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_10 @ X0 @ X1)
% 0.57/0.90 | ((a_select3 @ pminus_ds1_filter_init @ X1 @ X0) != (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_19])).
% 0.57/0.90 thf(zip_derived_cl87, plain,
% 0.57/0.90 ((~ (zip_tseitin_10 @ sk__7 @ sk__6))
% 0.57/0.90 <= (~ ( (zip_tseitin_10 @ sk__7 @ sk__6)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl149, plain,
% 0.57/0.90 ((((a_select3 @ pminus_ds1_filter_init @ sk__6 @ sk__7) != (init)))
% 0.57/0.90 <= (~ ( (zip_tseitin_10 @ sk__7 @ sk__6)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl22, zip_derived_cl87])).
% 0.57/0.90 thf(zip_derived_cl267, plain,
% 0.57/0.90 (((~ (leq @ sk__7 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ sk__7)
% 0.57/0.90 | ~ (leq @ n0 @ sk__6)
% 0.57/0.90 | ~ (leq @ sk__6 @ n5)
% 0.57/0.90 | ((init) != (init)))) <= (~ ( (zip_tseitin_10 @ sk__7 @ sk__6)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl62, zip_derived_cl149])).
% 0.57/0.90 thf(zip_derived_cl23, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_10 @ X0 @ X1) | (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_19])).
% 0.57/0.90 thf(zip_derived_cl87, plain,
% 0.57/0.90 ((~ (zip_tseitin_10 @ sk__7 @ sk__6))
% 0.57/0.90 <= (~ ( (zip_tseitin_10 @ sk__7 @ sk__6)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl169, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__7 @ sk__6))
% 0.57/0.90 <= (~ ( (zip_tseitin_10 @ sk__7 @ sk__6)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl23, zip_derived_cl87])).
% 0.57/0.90 thf(zip_derived_cl11, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n5) | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl184, plain,
% 0.57/0.90 (( (leq @ sk__7 @ n5)) <= (~ ( (zip_tseitin_10 @ sk__7 @ sk__6)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl169, zip_derived_cl11])).
% 0.57/0.90 thf(zip_derived_cl169, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__7 @ sk__6))
% 0.57/0.90 <= (~ ( (zip_tseitin_10 @ sk__7 @ sk__6)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl23, zip_derived_cl87])).
% 0.57/0.90 thf(zip_derived_cl9, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl183, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__7)) <= (~ ( (zip_tseitin_10 @ sk__7 @ sk__6)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl169, zip_derived_cl9])).
% 0.57/0.90 thf(zip_derived_cl169, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__7 @ sk__6))
% 0.57/0.90 <= (~ ( (zip_tseitin_10 @ sk__7 @ sk__6)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl23, zip_derived_cl87])).
% 0.57/0.90 thf(zip_derived_cl8, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_4 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl181, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__6)) <= (~ ( (zip_tseitin_10 @ sk__7 @ sk__6)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl169, zip_derived_cl8])).
% 0.57/0.90 thf(zip_derived_cl169, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__7 @ sk__6))
% 0.57/0.90 <= (~ ( (zip_tseitin_10 @ sk__7 @ sk__6)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl23, zip_derived_cl87])).
% 0.57/0.90 thf(zip_derived_cl10, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n5) | ~ (zip_tseitin_4 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl182, plain,
% 0.57/0.90 (( (leq @ sk__6 @ n5)) <= (~ ( (zip_tseitin_10 @ sk__7 @ sk__6)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl169, zip_derived_cl10])).
% 0.57/0.90 thf(zip_derived_cl268, plain,
% 0.57/0.90 ((((init) != (init))) <= (~ ( (zip_tseitin_10 @ sk__7 @ sk__6)))),
% 0.57/0.90 inference('demod', [status(thm)],
% 0.57/0.90 [zip_derived_cl267, zip_derived_cl184, zip_derived_cl183,
% 0.57/0.90 zip_derived_cl181, zip_derived_cl182])).
% 0.57/0.90 thf('5', plain, (( (zip_tseitin_10 @ sk__7 @ sk__6))),
% 0.57/0.90 inference('simplify', [status(thm)], [zip_derived_cl268])).
% 0.57/0.90 thf(zip_derived_cl61, plain,
% 0.57/0.90 (![X10 : $i, X11 : $i]:
% 0.57/0.90 (~ (leq @ X10 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ X10)
% 0.57/0.90 | ~ (leq @ n0 @ X11)
% 0.57/0.90 | ~ (leq @ X11 @ n0)
% 0.57/0.90 | ((a_select3 @ xhatmin_ds1_filter_init @ X10 @ X11) = (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl28, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_12 @ X0 @ X1)
% 0.57/0.90 | ((a_select3 @ xhatmin_ds1_filter_init @ X1 @ X0) != (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_15])).
% 0.57/0.90 thf(zip_derived_cl86, plain,
% 0.57/0.90 ((~ (zip_tseitin_12 @ sk__9 @ sk__8))
% 0.57/0.90 <= (~ ( (zip_tseitin_12 @ sk__9 @ sk__8)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl167, plain,
% 0.57/0.90 ((((a_select3 @ xhatmin_ds1_filter_init @ sk__8 @ sk__9) != (init)))
% 0.57/0.90 <= (~ ( (zip_tseitin_12 @ sk__9 @ sk__8)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl28, zip_derived_cl86])).
% 0.57/0.90 thf(zip_derived_cl264, plain,
% 0.57/0.90 (((~ (leq @ sk__9 @ n0)
% 0.57/0.90 | ~ (leq @ n0 @ sk__9)
% 0.57/0.90 | ~ (leq @ n0 @ sk__8)
% 0.57/0.90 | ~ (leq @ sk__8 @ n5)
% 0.57/0.90 | ((init) != (init)))) <= (~ ( (zip_tseitin_12 @ sk__9 @ sk__8)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl61, zip_derived_cl167])).
% 0.57/0.90 thf(zip_derived_cl29, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_12 @ X0 @ X1) | (zip_tseitin_11 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_15])).
% 0.57/0.90 thf(zip_derived_cl86, plain,
% 0.57/0.90 ((~ (zip_tseitin_12 @ sk__9 @ sk__8))
% 0.57/0.90 <= (~ ( (zip_tseitin_12 @ sk__9 @ sk__8)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl179, plain,
% 0.57/0.90 (( (zip_tseitin_11 @ sk__9 @ sk__8))
% 0.57/0.90 <= (~ ( (zip_tseitin_12 @ sk__9 @ sk__8)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl29, zip_derived_cl86])).
% 0.57/0.90 thf(zip_derived_cl27, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n0) | ~ (zip_tseitin_11 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_17])).
% 0.57/0.90 thf(zip_derived_cl192, plain,
% 0.57/0.90 (( (leq @ sk__9 @ n0)) <= (~ ( (zip_tseitin_12 @ sk__9 @ sk__8)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl179, zip_derived_cl27])).
% 0.57/0.90 thf(zip_derived_cl179, plain,
% 0.57/0.90 (( (zip_tseitin_11 @ sk__9 @ sk__8))
% 0.57/0.90 <= (~ ( (zip_tseitin_12 @ sk__9 @ sk__8)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl29, zip_derived_cl86])).
% 0.57/0.90 thf(zip_derived_cl25, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_11 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_17])).
% 0.57/0.90 thf(zip_derived_cl191, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__9)) <= (~ ( (zip_tseitin_12 @ sk__9 @ sk__8)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl179, zip_derived_cl25])).
% 0.57/0.90 thf(zip_derived_cl179, plain,
% 0.57/0.90 (( (zip_tseitin_11 @ sk__9 @ sk__8))
% 0.57/0.90 <= (~ ( (zip_tseitin_12 @ sk__9 @ sk__8)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl29, zip_derived_cl86])).
% 0.57/0.90 thf(zip_derived_cl24, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_11 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_17])).
% 0.57/0.90 thf(zip_derived_cl189, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__8)) <= (~ ( (zip_tseitin_12 @ sk__9 @ sk__8)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl179, zip_derived_cl24])).
% 0.57/0.90 thf(zip_derived_cl179, plain,
% 0.57/0.90 (( (zip_tseitin_11 @ sk__9 @ sk__8))
% 0.57/0.90 <= (~ ( (zip_tseitin_12 @ sk__9 @ sk__8)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl29, zip_derived_cl86])).
% 0.57/0.90 thf(zip_derived_cl26, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n5) | ~ (zip_tseitin_11 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_17])).
% 0.57/0.90 thf(zip_derived_cl190, plain,
% 0.57/0.90 (( (leq @ sk__8 @ n5)) <= (~ ( (zip_tseitin_12 @ sk__9 @ sk__8)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl179, zip_derived_cl26])).
% 0.57/0.90 thf(zip_derived_cl265, plain,
% 0.57/0.90 ((((init) != (init))) <= (~ ( (zip_tseitin_12 @ sk__9 @ sk__8)))),
% 0.57/0.90 inference('demod', [status(thm)],
% 0.57/0.90 [zip_derived_cl264, zip_derived_cl192, zip_derived_cl191,
% 0.57/0.90 zip_derived_cl189, zip_derived_cl190])).
% 0.57/0.90 thf('6', plain, (( (zip_tseitin_12 @ sk__9 @ sk__8))),
% 0.57/0.90 inference('simplify', [status(thm)], [zip_derived_cl265])).
% 0.57/0.90 thf(zip_derived_cl7, plain,
% 0.57/0.90 (![X0 : $i]: ( (zip_tseitin_3 @ X0) | (zip_tseitin_0 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_33])).
% 0.57/0.90 thf(zip_derived_cl90, plain,
% 0.57/0.90 ((~ (zip_tseitin_3 @ sk__1)) <= (~ ( (zip_tseitin_3 @ sk__1)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl112, plain,
% 0.57/0.90 (( (zip_tseitin_0 @ sk__1)) <= (~ ( (zip_tseitin_3 @ sk__1)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl7, zip_derived_cl90])).
% 0.57/0.90 thf(zip_derived_cl1, plain,
% 0.57/0.90 (![X0 : $i]: ( (leq @ X0 @ (pred @ pv63)) | ~ (zip_tseitin_0 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_39])).
% 0.57/0.90 thf(zip_derived_cl65, plain,
% 0.57/0.90 (![X18 : $i, X19 : $i]:
% 0.57/0.90 (~ (leq @ n0 @ X18)
% 0.57/0.90 | ~ (leq @ X18 @ n5)
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ X19 @ X18) = (init))
% 0.57/0.90 | ~ (leq @ X19 @ (pred @ pv63))
% 0.57/0.90 | ~ (leq @ n0 @ X19))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl247, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 (~ (zip_tseitin_0 @ X0)
% 0.57/0.90 | ~ (leq @ n0 @ X1)
% 0.57/0.90 | ~ (leq @ X1 @ n5)
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ X0 @ X1) = (init))
% 0.57/0.90 | ~ (leq @ n0 @ X0))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl65])).
% 0.57/0.90 thf(zip_derived_cl0, plain,
% 0.57/0.90 (![X0 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_0 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_39])).
% 0.57/0.90 thf(zip_derived_cl248, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 (((a_select3 @ id_ds1_filter_init @ X0 @ X1) = (init))
% 0.57/0.90 | ~ (leq @ X1 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ X1)
% 0.57/0.90 | ~ (zip_tseitin_0 @ X0))),
% 0.57/0.90 inference('clc', [status(thm)], [zip_derived_cl247, zip_derived_cl0])).
% 0.57/0.90 thf(zip_derived_cl249, plain,
% 0.57/0.90 ((![X0 : $i]:
% 0.57/0.90 (((a_select3 @ id_ds1_filter_init @ sk__1 @ X0) = (init))
% 0.57/0.90 | ~ (leq @ X0 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ X0)))
% 0.57/0.90 <= (~ ( (zip_tseitin_3 @ sk__1)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl112, zip_derived_cl248])).
% 0.57/0.90 thf(zip_derived_cl4, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_2 @ X0 @ X1)
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ X1 @ X0) != (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_35])).
% 0.57/0.90 thf(zip_derived_cl6, plain,
% 0.57/0.90 (![X0 : $i]:
% 0.57/0.90 ( (zip_tseitin_3 @ X0) | ~ (zip_tseitin_2 @ (sk_ @ X0) @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_33])).
% 0.57/0.90 thf(zip_derived_cl110, plain,
% 0.57/0.90 (![X0 : $i]:
% 0.57/0.90 (((a_select3 @ id_ds1_filter_init @ X0 @ (sk_ @ X0)) != (init))
% 0.57/0.90 | (zip_tseitin_3 @ X0))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl4, zip_derived_cl6])).
% 0.57/0.90 thf(zip_derived_cl250, plain,
% 0.57/0.90 (((~ (leq @ n0 @ (sk_ @ sk__1))
% 0.57/0.90 | ~ (leq @ (sk_ @ sk__1) @ n5)
% 0.57/0.90 | ((init) != (init))
% 0.57/0.90 | (zip_tseitin_3 @ sk__1))) <= (~ ( (zip_tseitin_3 @ sk__1)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl249, zip_derived_cl110])).
% 0.57/0.90 thf(zip_derived_cl90, plain,
% 0.57/0.90 ((~ (zip_tseitin_3 @ sk__1)) <= (~ ( (zip_tseitin_3 @ sk__1)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl251, plain,
% 0.57/0.90 (((~ (leq @ n0 @ (sk_ @ sk__1))
% 0.57/0.90 | ~ (leq @ (sk_ @ sk__1) @ n5)
% 0.57/0.90 | ((init) != (init)))) <= (~ ( (zip_tseitin_3 @ sk__1)))),
% 0.57/0.90 inference('demod', [status(thm)], [zip_derived_cl250, zip_derived_cl90])).
% 0.57/0.90 thf(zip_derived_cl252, plain,
% 0.57/0.90 (((~ (leq @ (sk_ @ sk__1) @ n5) | ~ (leq @ n0 @ (sk_ @ sk__1))))
% 0.57/0.90 <= (~ ( (zip_tseitin_3 @ sk__1)))),
% 0.57/0.90 inference('simplify', [status(thm)], [zip_derived_cl251])).
% 0.57/0.90 thf('7', plain,
% 0.57/0.90 (( (zip_tseitin_3 @ sk__1)) | ~ ( (leq @ (sk_ @ sk__1) @ n5)) |
% 0.57/0.90 ~ ( (leq @ n0 @ (sk_ @ sk__1)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl252])).
% 0.57/0.90 thf(zip_derived_cl253, plain,
% 0.57/0.90 ((~ (leq @ n0 @ (sk_ @ sk__1))) <= (~ ( (leq @ n0 @ (sk_ @ sk__1))))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl252])).
% 0.57/0.90 thf(zip_derived_cl5, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_2 @ X0 @ X1) | (zip_tseitin_1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_35])).
% 0.57/0.90 thf(zip_derived_cl6, plain,
% 0.57/0.90 (![X0 : $i]:
% 0.57/0.90 ( (zip_tseitin_3 @ X0) | ~ (zip_tseitin_2 @ (sk_ @ X0) @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_33])).
% 0.57/0.90 thf(zip_derived_cl120, plain,
% 0.57/0.90 (![X0 : $i]: ( (zip_tseitin_1 @ (sk_ @ X0)) | (zip_tseitin_3 @ X0))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl6])).
% 0.57/0.90 thf(zip_derived_cl2, plain,
% 0.57/0.90 (![X0 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_37])).
% 0.57/0.90 thf(zip_derived_cl141, plain,
% 0.57/0.90 (![X0 : $i]: ( (zip_tseitin_3 @ X0) | (leq @ n0 @ (sk_ @ X0)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl120, zip_derived_cl2])).
% 0.57/0.90 thf(zip_derived_cl255, plain,
% 0.57/0.90 (( (zip_tseitin_3 @ sk__1)) <= (~ ( (leq @ n0 @ (sk_ @ sk__1))))),
% 0.57/0.90 inference('s_sup+', [status(thm)], [zip_derived_cl253, zip_derived_cl141])).
% 0.57/0.90 thf(zip_derived_cl90, plain,
% 0.57/0.90 ((~ (zip_tseitin_3 @ sk__1)) <= (~ ( (zip_tseitin_3 @ sk__1)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf('8', plain, (( (leq @ n0 @ (sk_ @ sk__1))) | ( (zip_tseitin_3 @ sk__1))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl255, zip_derived_cl90])).
% 0.57/0.90 thf(zip_derived_cl254, plain,
% 0.57/0.90 ((~ (leq @ (sk_ @ sk__1) @ n5)) <= (~ ( (leq @ (sk_ @ sk__1) @ n5)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl252])).
% 0.57/0.90 thf(zip_derived_cl120, plain,
% 0.57/0.90 (![X0 : $i]: ( (zip_tseitin_1 @ (sk_ @ X0)) | (zip_tseitin_3 @ X0))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl6])).
% 0.57/0.90 thf(zip_derived_cl3, plain,
% 0.57/0.90 (![X0 : $i]: ( (leq @ X0 @ n5) | ~ (zip_tseitin_1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_37])).
% 0.57/0.90 thf(zip_derived_cl142, plain,
% 0.57/0.90 (![X0 : $i]: ( (zip_tseitin_3 @ X0) | (leq @ (sk_ @ X0) @ n5))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl120, zip_derived_cl3])).
% 0.57/0.90 thf(zip_derived_cl257, plain,
% 0.57/0.90 (( (zip_tseitin_3 @ sk__1)) <= (~ ( (leq @ (sk_ @ sk__1) @ n5)))),
% 0.57/0.90 inference('s_sup+', [status(thm)], [zip_derived_cl254, zip_derived_cl142])).
% 0.57/0.90 thf(zip_derived_cl90, plain,
% 0.57/0.90 ((~ (zip_tseitin_3 @ sk__1)) <= (~ ( (zip_tseitin_3 @ sk__1)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf('9', plain, (( (leq @ (sk_ @ sk__1) @ n5)) | ( (zip_tseitin_3 @ sk__1))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl257, zip_derived_cl90])).
% 0.57/0.90 thf(zip_derived_cl60, plain,
% 0.57/0.90 (![X8 : $i, X9 : $i]:
% 0.57/0.90 (~ (leq @ X8 @ n2)
% 0.57/0.90 | ~ (leq @ n0 @ X8)
% 0.57/0.90 | ~ (leq @ n0 @ X9)
% 0.57/0.90 | ~ (leq @ X9 @ n2)
% 0.57/0.90 | ((a_select3 @ r_ds1_filter_init @ X8 @ X9) = (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl34, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_14 @ X0 @ X1)
% 0.57/0.90 | ((a_select3 @ r_ds1_filter_init @ X1 @ X0) != (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_11])).
% 0.57/0.90 thf(zip_derived_cl85, plain,
% 0.57/0.90 ((~ (zip_tseitin_14 @ sk__11 @ sk__10))
% 0.57/0.90 <= (~ ( (zip_tseitin_14 @ sk__11 @ sk__10)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl177, plain,
% 0.57/0.90 ((((a_select3 @ r_ds1_filter_init @ sk__10 @ sk__11) != (init)))
% 0.57/0.90 <= (~ ( (zip_tseitin_14 @ sk__11 @ sk__10)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl34, zip_derived_cl85])).
% 0.57/0.90 thf(zip_derived_cl260, plain,
% 0.57/0.90 (((~ (leq @ sk__11 @ n2)
% 0.57/0.90 | ~ (leq @ n0 @ sk__11)
% 0.57/0.90 | ~ (leq @ n0 @ sk__10)
% 0.57/0.90 | ~ (leq @ sk__10 @ n2)
% 0.57/0.90 | ((init) != (init)))) <= (~ ( (zip_tseitin_14 @ sk__11 @ sk__10)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl60, zip_derived_cl177])).
% 0.57/0.90 thf(zip_derived_cl35, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_14 @ X0 @ X1) | (zip_tseitin_13 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_11])).
% 0.57/0.90 thf(zip_derived_cl85, plain,
% 0.57/0.90 ((~ (zip_tseitin_14 @ sk__11 @ sk__10))
% 0.57/0.90 <= (~ ( (zip_tseitin_14 @ sk__11 @ sk__10)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl187, plain,
% 0.57/0.90 (( (zip_tseitin_13 @ sk__11 @ sk__10))
% 0.57/0.90 <= (~ ( (zip_tseitin_14 @ sk__11 @ sk__10)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl35, zip_derived_cl85])).
% 0.57/0.90 thf(zip_derived_cl33, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n2) | ~ (zip_tseitin_13 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_13])).
% 0.57/0.90 thf(zip_derived_cl200, plain,
% 0.57/0.90 (( (leq @ sk__11 @ n2)) <= (~ ( (zip_tseitin_14 @ sk__11 @ sk__10)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl187, zip_derived_cl33])).
% 0.57/0.90 thf(zip_derived_cl187, plain,
% 0.57/0.90 (( (zip_tseitin_13 @ sk__11 @ sk__10))
% 0.57/0.90 <= (~ ( (zip_tseitin_14 @ sk__11 @ sk__10)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl35, zip_derived_cl85])).
% 0.57/0.90 thf(zip_derived_cl31, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_13 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_13])).
% 0.57/0.90 thf(zip_derived_cl199, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__11)) <= (~ ( (zip_tseitin_14 @ sk__11 @ sk__10)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl187, zip_derived_cl31])).
% 0.57/0.90 thf(zip_derived_cl187, plain,
% 0.57/0.90 (( (zip_tseitin_13 @ sk__11 @ sk__10))
% 0.57/0.90 <= (~ ( (zip_tseitin_14 @ sk__11 @ sk__10)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl35, zip_derived_cl85])).
% 0.57/0.90 thf(zip_derived_cl30, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_13 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_13])).
% 0.57/0.90 thf(zip_derived_cl197, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__10)) <= (~ ( (zip_tseitin_14 @ sk__11 @ sk__10)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl187, zip_derived_cl30])).
% 0.57/0.90 thf(zip_derived_cl187, plain,
% 0.57/0.90 (( (zip_tseitin_13 @ sk__11 @ sk__10))
% 0.57/0.90 <= (~ ( (zip_tseitin_14 @ sk__11 @ sk__10)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl35, zip_derived_cl85])).
% 0.57/0.90 thf(zip_derived_cl32, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n2) | ~ (zip_tseitin_13 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_13])).
% 0.57/0.90 thf(zip_derived_cl198, plain,
% 0.57/0.90 (( (leq @ sk__10 @ n2)) <= (~ ( (zip_tseitin_14 @ sk__11 @ sk__10)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl187, zip_derived_cl32])).
% 0.57/0.90 thf(zip_derived_cl261, plain,
% 0.57/0.90 ((((init) != (init))) <= (~ ( (zip_tseitin_14 @ sk__11 @ sk__10)))),
% 0.57/0.90 inference('demod', [status(thm)],
% 0.57/0.90 [zip_derived_cl260, zip_derived_cl200, zip_derived_cl199,
% 0.57/0.90 zip_derived_cl197, zip_derived_cl198])).
% 0.57/0.90 thf('10', plain, (( (zip_tseitin_14 @ sk__11 @ sk__10))),
% 0.57/0.90 inference('simplify', [status(thm)], [zip_derived_cl261])).
% 0.57/0.90 thf(zip_derived_cl59, plain,
% 0.57/0.90 (![X6 : $i, X7 : $i]:
% 0.57/0.90 (~ (leq @ X6 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ X6)
% 0.57/0.90 | ~ (leq @ n0 @ X7)
% 0.57/0.90 | ~ (leq @ X7 @ n5)
% 0.57/0.90 | ((a_select3 @ q_ds1_filter_init @ X6 @ X7) = (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl36, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_15 @ X0 @ X1)
% 0.57/0.90 | ((a_select3 @ q_ds1_filter_init @ X1 @ X0) != (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_9])).
% 0.57/0.90 thf(zip_derived_cl84, plain,
% 0.57/0.90 ((~ (zip_tseitin_15 @ sk__13 @ sk__12))
% 0.57/0.90 <= (~ ( (zip_tseitin_15 @ sk__13 @ sk__12)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl185, plain,
% 0.57/0.90 ((((a_select3 @ q_ds1_filter_init @ sk__12 @ sk__13) != (init)))
% 0.57/0.90 <= (~ ( (zip_tseitin_15 @ sk__13 @ sk__12)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl36, zip_derived_cl84])).
% 0.57/0.90 thf(zip_derived_cl244, plain,
% 0.57/0.90 (((~ (leq @ sk__13 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ sk__13)
% 0.57/0.90 | ~ (leq @ n0 @ sk__12)
% 0.57/0.90 | ~ (leq @ sk__12 @ n5)
% 0.57/0.90 | ((init) != (init)))) <= (~ ( (zip_tseitin_15 @ sk__13 @ sk__12)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl59, zip_derived_cl185])).
% 0.57/0.90 thf(zip_derived_cl37, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_15 @ X0 @ X1) | (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_9])).
% 0.57/0.90 thf(zip_derived_cl84, plain,
% 0.57/0.90 ((~ (zip_tseitin_15 @ sk__13 @ sk__12))
% 0.57/0.90 <= (~ ( (zip_tseitin_15 @ sk__13 @ sk__12)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl195, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__13 @ sk__12))
% 0.57/0.90 <= (~ ( (zip_tseitin_15 @ sk__13 @ sk__12)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl37, zip_derived_cl84])).
% 0.57/0.90 thf(zip_derived_cl11, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n5) | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl204, plain,
% 0.57/0.90 (( (leq @ sk__13 @ n5)) <= (~ ( (zip_tseitin_15 @ sk__13 @ sk__12)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl195, zip_derived_cl11])).
% 0.57/0.90 thf(zip_derived_cl195, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__13 @ sk__12))
% 0.57/0.90 <= (~ ( (zip_tseitin_15 @ sk__13 @ sk__12)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl37, zip_derived_cl84])).
% 0.57/0.90 thf(zip_derived_cl9, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl203, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__13)) <= (~ ( (zip_tseitin_15 @ sk__13 @ sk__12)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl195, zip_derived_cl9])).
% 0.57/0.90 thf(zip_derived_cl195, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__13 @ sk__12))
% 0.57/0.90 <= (~ ( (zip_tseitin_15 @ sk__13 @ sk__12)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl37, zip_derived_cl84])).
% 0.57/0.90 thf(zip_derived_cl8, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_4 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl201, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__12)) <= (~ ( (zip_tseitin_15 @ sk__13 @ sk__12)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl195, zip_derived_cl8])).
% 0.57/0.90 thf(zip_derived_cl195, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__13 @ sk__12))
% 0.57/0.90 <= (~ ( (zip_tseitin_15 @ sk__13 @ sk__12)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl37, zip_derived_cl84])).
% 0.57/0.90 thf(zip_derived_cl10, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n5) | ~ (zip_tseitin_4 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl202, plain,
% 0.57/0.90 (( (leq @ sk__12 @ n5)) <= (~ ( (zip_tseitin_15 @ sk__13 @ sk__12)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl195, zip_derived_cl10])).
% 0.57/0.90 thf(zip_derived_cl245, plain,
% 0.57/0.90 ((((init) != (init))) <= (~ ( (zip_tseitin_15 @ sk__13 @ sk__12)))),
% 0.57/0.90 inference('demod', [status(thm)],
% 0.57/0.90 [zip_derived_cl244, zip_derived_cl204, zip_derived_cl203,
% 0.57/0.90 zip_derived_cl201, zip_derived_cl202])).
% 0.57/0.90 thf('11', plain, (( (zip_tseitin_15 @ sk__13 @ sk__12))),
% 0.57/0.90 inference('simplify', [status(thm)], [zip_derived_cl245])).
% 0.57/0.90 thf(zip_derived_cl58, plain,
% 0.57/0.90 (![X4 : $i, X5 : $i]:
% 0.57/0.90 (~ (leq @ X4 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ X4)
% 0.57/0.90 | ~ (leq @ n0 @ X5)
% 0.57/0.90 | ~ (leq @ X5 @ n0)
% 0.57/0.90 | ((a_select3 @ dv_ds1_filter_init @ X4 @ X5) = (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl38, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_16 @ X0 @ X1)
% 0.57/0.90 | ((a_select3 @ dv_ds1_filter_init @ X1 @ X0) != (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.57/0.90 thf(zip_derived_cl83, plain,
% 0.57/0.90 ((~ (zip_tseitin_16 @ sk__15 @ sk__14))
% 0.57/0.90 <= (~ ( (zip_tseitin_16 @ sk__15 @ sk__14)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl193, plain,
% 0.57/0.90 ((((a_select3 @ dv_ds1_filter_init @ sk__14 @ sk__15) != (init)))
% 0.57/0.90 <= (~ ( (zip_tseitin_16 @ sk__15 @ sk__14)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl38, zip_derived_cl83])).
% 0.57/0.90 thf(zip_derived_cl237, plain,
% 0.57/0.90 (((~ (leq @ sk__15 @ n0)
% 0.57/0.90 | ~ (leq @ n0 @ sk__15)
% 0.57/0.90 | ~ (leq @ n0 @ sk__14)
% 0.57/0.90 | ~ (leq @ sk__14 @ n5)
% 0.57/0.90 | ((init) != (init)))) <= (~ ( (zip_tseitin_16 @ sk__15 @ sk__14)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl58, zip_derived_cl193])).
% 0.57/0.90 thf(zip_derived_cl39, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_16 @ X0 @ X1) | (zip_tseitin_11 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.57/0.90 thf(zip_derived_cl83, plain,
% 0.57/0.90 ((~ (zip_tseitin_16 @ sk__15 @ sk__14))
% 0.57/0.90 <= (~ ( (zip_tseitin_16 @ sk__15 @ sk__14)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl207, plain,
% 0.57/0.90 (( (zip_tseitin_11 @ sk__15 @ sk__14))
% 0.57/0.90 <= (~ ( (zip_tseitin_16 @ sk__15 @ sk__14)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl39, zip_derived_cl83])).
% 0.57/0.90 thf(zip_derived_cl27, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n0) | ~ (zip_tseitin_11 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_17])).
% 0.57/0.90 thf(zip_derived_cl216, plain,
% 0.57/0.90 (( (leq @ sk__15 @ n0)) <= (~ ( (zip_tseitin_16 @ sk__15 @ sk__14)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl207, zip_derived_cl27])).
% 0.57/0.90 thf(zip_derived_cl207, plain,
% 0.57/0.90 (( (zip_tseitin_11 @ sk__15 @ sk__14))
% 0.57/0.90 <= (~ ( (zip_tseitin_16 @ sk__15 @ sk__14)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl39, zip_derived_cl83])).
% 0.57/0.90 thf(zip_derived_cl25, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_11 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_17])).
% 0.57/0.90 thf(zip_derived_cl215, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__15)) <= (~ ( (zip_tseitin_16 @ sk__15 @ sk__14)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl207, zip_derived_cl25])).
% 0.57/0.90 thf(zip_derived_cl207, plain,
% 0.57/0.90 (( (zip_tseitin_11 @ sk__15 @ sk__14))
% 0.57/0.90 <= (~ ( (zip_tseitin_16 @ sk__15 @ sk__14)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl39, zip_derived_cl83])).
% 0.57/0.90 thf(zip_derived_cl24, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_11 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_17])).
% 0.57/0.90 thf(zip_derived_cl213, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__14)) <= (~ ( (zip_tseitin_16 @ sk__15 @ sk__14)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl207, zip_derived_cl24])).
% 0.57/0.90 thf(zip_derived_cl207, plain,
% 0.57/0.90 (( (zip_tseitin_11 @ sk__15 @ sk__14))
% 0.57/0.90 <= (~ ( (zip_tseitin_16 @ sk__15 @ sk__14)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl39, zip_derived_cl83])).
% 0.57/0.90 thf(zip_derived_cl26, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n5) | ~ (zip_tseitin_11 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_17])).
% 0.57/0.90 thf(zip_derived_cl214, plain,
% 0.57/0.90 (( (leq @ sk__14 @ n5)) <= (~ ( (zip_tseitin_16 @ sk__15 @ sk__14)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl207, zip_derived_cl26])).
% 0.57/0.90 thf(zip_derived_cl238, plain,
% 0.57/0.90 ((((init) != (init))) <= (~ ( (zip_tseitin_16 @ sk__15 @ sk__14)))),
% 0.57/0.90 inference('demod', [status(thm)],
% 0.57/0.90 [zip_derived_cl237, zip_derived_cl216, zip_derived_cl215,
% 0.57/0.90 zip_derived_cl213, zip_derived_cl214])).
% 0.57/0.90 thf('12', plain, (( (zip_tseitin_16 @ sk__15 @ sk__14))),
% 0.57/0.90 inference('simplify', [status(thm)], [zip_derived_cl238])).
% 0.57/0.90 thf(zip_derived_cl57, plain,
% 0.57/0.90 (![X2 : $i, X3 : $i]:
% 0.57/0.90 (~ (leq @ X2 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ X2)
% 0.57/0.90 | ~ (leq @ n0 @ X3)
% 0.57/0.90 | ~ (leq @ X3 @ n5)
% 0.57/0.90 | ((a_select3 @ phi_ds1_filter_init @ X2 @ X3) = (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl40, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_17 @ X0 @ X1)
% 0.57/0.90 | ((a_select3 @ phi_ds1_filter_init @ X1 @ X0) != (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.57/0.90 thf(zip_derived_cl82, plain,
% 0.57/0.90 ((~ (zip_tseitin_17 @ sk__17 @ sk__16))
% 0.57/0.90 <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl205, plain,
% 0.57/0.90 ((((a_select3 @ phi_ds1_filter_init @ sk__16 @ sk__17) != (init)))
% 0.57/0.90 <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl40, zip_derived_cl82])).
% 0.57/0.90 thf(zip_derived_cl229, plain,
% 0.57/0.90 (((~ (leq @ sk__17 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ sk__17)
% 0.57/0.90 | ~ (leq @ n0 @ sk__16)
% 0.57/0.90 | ~ (leq @ sk__16 @ n5)
% 0.57/0.90 | ((init) != (init)))) <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl57, zip_derived_cl205])).
% 0.57/0.90 thf(zip_derived_cl41, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_17 @ X0 @ X1) | (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.57/0.90 thf(zip_derived_cl82, plain,
% 0.57/0.90 ((~ (zip_tseitin_17 @ sk__17 @ sk__16))
% 0.57/0.90 <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl211, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__17 @ sk__16))
% 0.57/0.90 <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl41, zip_derived_cl82])).
% 0.57/0.90 thf(zip_derived_cl8, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_4 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl217, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__16)) <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl211, zip_derived_cl8])).
% 0.57/0.90 thf(zip_derived_cl211, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__17 @ sk__16))
% 0.57/0.90 <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl41, zip_derived_cl82])).
% 0.57/0.90 thf(zip_derived_cl10, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n5) | ~ (zip_tseitin_4 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl218, plain,
% 0.57/0.90 (( (leq @ sk__16 @ n5)) <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl211, zip_derived_cl10])).
% 0.57/0.90 thf(zip_derived_cl230, plain,
% 0.57/0.90 (((~ (leq @ sk__17 @ n5) | ~ (leq @ n0 @ sk__17) | ((init) != (init))))
% 0.57/0.90 <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('demod', [status(thm)],
% 0.57/0.90 [zip_derived_cl229, zip_derived_cl217, zip_derived_cl218])).
% 0.57/0.90 thf(zip_derived_cl231, plain,
% 0.57/0.90 (((~ (leq @ n0 @ sk__17) | ~ (leq @ sk__17 @ n5)))
% 0.57/0.90 <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('simplify', [status(thm)], [zip_derived_cl230])).
% 0.57/0.90 thf(zip_derived_cl211, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__17 @ sk__16))
% 0.57/0.90 <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl41, zip_derived_cl82])).
% 0.57/0.90 thf(zip_derived_cl9, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl219, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__17)) <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl211, zip_derived_cl9])).
% 0.57/0.90 thf(zip_derived_cl211, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__17 @ sk__16))
% 0.57/0.90 <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl41, zip_derived_cl82])).
% 0.57/0.90 thf(zip_derived_cl11, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n5) | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl220, plain,
% 0.57/0.90 (( (leq @ sk__17 @ n5)) <= (~ ( (zip_tseitin_17 @ sk__17 @ sk__16)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl211, zip_derived_cl11])).
% 0.57/0.90 thf('13', plain, (( (zip_tseitin_17 @ sk__17 @ sk__16))),
% 0.57/0.90 inference('demod', [status(thm)],
% 0.57/0.90 [zip_derived_cl231, zip_derived_cl219, zip_derived_cl220])).
% 0.57/0.90 thf(zip_derived_cl70, plain, ( (leq @ sk__21 @ n5)),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl74, plain,
% 0.57/0.90 ((![X0 : $i, X1 : $i]:
% 0.57/0.90 (~ (leq @ n0 @ X0)
% 0.57/0.90 | ~ (leq @ X0 @ n5)
% 0.57/0.90 | ((X1) != (pv63))
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ X1 @ X0) = (init))
% 0.57/0.90 | ((pv64) = (X0))
% 0.57/0.90 | ~ (leq @ X0 @ pv64)
% 0.57/0.90 | ~ (leq @ n0 @ X1)
% 0.57/0.90 | ~ (leq @ X1 @ n5)))
% 0.57/0.90 <= ((![X0 : $i, X1 : $i]:
% 0.57/0.90 (~ (leq @ n0 @ X0)
% 0.57/0.90 | ~ (leq @ X0 @ n5)
% 0.57/0.90 | ((X1) != (pv63))
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ X1 @ X0) = (init))
% 0.57/0.90 | ((pv64) = (X0))
% 0.57/0.90 | ~ (leq @ X0 @ pv64)
% 0.57/0.90 | ~ (leq @ n0 @ X1)
% 0.57/0.90 | ~ (leq @ X1 @ n5))))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl71, plain,
% 0.57/0.90 (((a_select3 @ id_ds1_filter_init @ sk__20 @ sk__21) != (init))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl66, plain, (((sk__20) = (pv63))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl93, plain,
% 0.57/0.90 (((a_select3 @ id_ds1_filter_init @ pv63 @ sk__21) != (init))),
% 0.57/0.90 inference('demod', [status(thm)], [zip_derived_cl71, zip_derived_cl66])).
% 0.57/0.90 thf(zip_derived_cl96, plain,
% 0.57/0.90 (((~ (leq @ pv63 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ pv63)
% 0.57/0.90 | ~ (leq @ sk__21 @ pv64)
% 0.57/0.90 | ((pv64) = (sk__21))
% 0.57/0.90 | ((pv63) != (pv63))
% 0.57/0.90 | ~ (leq @ sk__21 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ sk__21)
% 0.57/0.90 | ((init) != (init))))
% 0.57/0.90 <= ((![X0 : $i, X1 : $i]:
% 0.57/0.90 (~ (leq @ n0 @ X0)
% 0.57/0.90 | ~ (leq @ X0 @ n5)
% 0.57/0.90 | ((X1) != (pv63))
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ X1 @ X0) = (init))
% 0.57/0.90 | ((pv64) = (X0))
% 0.57/0.90 | ~ (leq @ X0 @ pv64)
% 0.57/0.90 | ~ (leq @ n0 @ X1)
% 0.57/0.90 | ~ (leq @ X1 @ n5))))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl74, zip_derived_cl93])).
% 0.57/0.90 thf(zip_derived_cl97, plain,
% 0.57/0.90 (((~ (leq @ n0 @ sk__21)
% 0.57/0.90 | ~ (leq @ sk__21 @ n5)
% 0.57/0.90 | ((pv64) = (sk__21))
% 0.57/0.90 | ~ (leq @ sk__21 @ pv64)
% 0.57/0.90 | ~ (leq @ n0 @ pv63)
% 0.57/0.90 | ~ (leq @ pv63 @ n5)))
% 0.57/0.90 <= ((![X0 : $i, X1 : $i]:
% 0.57/0.90 (~ (leq @ n0 @ X0)
% 0.57/0.90 | ~ (leq @ X0 @ n5)
% 0.57/0.90 | ((X1) != (pv63))
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ X1 @ X0) = (init))
% 0.57/0.90 | ((pv64) = (X0))
% 0.57/0.90 | ~ (leq @ X0 @ pv64)
% 0.57/0.90 | ~ (leq @ n0 @ X1)
% 0.57/0.90 | ~ (leq @ X1 @ n5))))),
% 0.57/0.90 inference('simplify', [status(thm)], [zip_derived_cl96])).
% 0.57/0.90 thf(zip_derived_cl73, plain, (((pv64) != (sk__21))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl98, plain,
% 0.57/0.90 (((~ (leq @ n0 @ sk__21)
% 0.57/0.90 | ~ (leq @ sk__21 @ n5)
% 0.57/0.90 | ~ (leq @ sk__21 @ pv64)
% 0.57/0.90 | ~ (leq @ n0 @ pv63)
% 0.57/0.90 | ~ (leq @ pv63 @ n5)))
% 0.57/0.90 <= ((![X0 : $i, X1 : $i]:
% 0.57/0.90 (~ (leq @ n0 @ X0)
% 0.57/0.90 | ~ (leq @ X0 @ n5)
% 0.57/0.90 | ((X1) != (pv63))
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ X1 @ X0) = (init))
% 0.57/0.90 | ((pv64) = (X0))
% 0.57/0.90 | ~ (leq @ X0 @ pv64)
% 0.57/0.90 | ~ (leq @ n0 @ X1)
% 0.57/0.90 | ~ (leq @ X1 @ n5))))),
% 0.57/0.90 inference('simplify_reflect-', [status(thm)],
% 0.57/0.90 [zip_derived_cl97, zip_derived_cl73])).
% 0.57/0.90 thf(zip_derived_cl100, plain,
% 0.57/0.90 ((~ (leq @ sk__21 @ n5)) <= (~ ( (leq @ sk__21 @ n5)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl98])).
% 0.57/0.90 thf('14', plain, (( (leq @ sk__21 @ n5))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl70, zip_derived_cl100])).
% 0.57/0.90 thf(zip_derived_cl69, plain, ( (leq @ n0 @ sk__21)),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl101, plain,
% 0.57/0.90 ((~ (leq @ n0 @ sk__21)) <= (~ ( (leq @ n0 @ sk__21)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl98])).
% 0.57/0.90 thf('15', plain, (( (leq @ n0 @ sk__21))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl69, zip_derived_cl101])).
% 0.57/0.90 thf(zip_derived_cl72, plain, ( (leq @ sk__21 @ pv64)),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl99, plain,
% 0.57/0.90 ((~ (leq @ sk__21 @ pv64)) <= (~ ( (leq @ sk__21 @ pv64)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl98])).
% 0.57/0.90 thf('16', plain, (( (leq @ sk__21 @ pv64))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl72, zip_derived_cl99])).
% 0.57/0.90 thf('17', plain,
% 0.57/0.90 (~
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 (~ (leq @ n0 @ X0)
% 0.57/0.90 | ~ (leq @ X0 @ n5)
% 0.57/0.90 | ((X1) != (pv63))
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ X1 @ X0) = (init))
% 0.57/0.90 | ((pv64) = (X0))
% 0.57/0.90 | ~ (leq @ X0 @ pv64)
% 0.57/0.90 | ~ (leq @ n0 @ X1)
% 0.57/0.90 | ~ (leq @ X1 @ n5))) |
% 0.57/0.90 ~ ( (leq @ sk__21 @ pv64)) | ~ ( (leq @ pv63 @ n5)) |
% 0.57/0.90 ~ ( (leq @ n0 @ sk__21)) | ~ ( (leq @ sk__21 @ n5)) |
% 0.57/0.90 ~ ( (leq @ n0 @ pv63))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl98])).
% 0.57/0.90 thf(zip_derived_cl54, plain, ( (leq @ pv63 @ n5)),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl79, plain,
% 0.57/0.90 ((~ (leq @ pv63 @ n5)) <= (~ ( (leq @ pv63 @ n5)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf('18', plain, (( (leq @ pv63 @ n5))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl54, zip_derived_cl79])).
% 0.57/0.90 thf(zip_derived_cl52, plain, ( (leq @ n0 @ pv64)),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl77, plain,
% 0.57/0.90 ((~ (leq @ n0 @ pv64)) <= (~ ( (leq @ n0 @ pv64)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf('19', plain, (( (leq @ n0 @ pv64))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl52, zip_derived_cl77])).
% 0.57/0.90 thf(zip_derived_cl51, plain, ( (leq @ n0 @ pv63)),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl76, plain,
% 0.57/0.90 ((~ (leq @ n0 @ pv63)) <= (~ ( (leq @ n0 @ pv63)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf('20', plain, (( (leq @ n0 @ pv63))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl51, zip_derived_cl76])).
% 0.57/0.90 thf(zip_derived_cl50, plain, ( (leq @ n0 @ pv5)),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl75, plain,
% 0.57/0.90 ((~ (leq @ n0 @ pv5)) <= (~ ( (leq @ n0 @ pv5)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf('21', plain, (( (leq @ n0 @ pv5))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl75])).
% 0.57/0.90 thf(zip_derived_cl14, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_6 @ X0 @ X1) | ~ (zip_tseitin_5 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_27])).
% 0.57/0.90 thf(zip_derived_cl89, plain,
% 0.57/0.90 ((~ (zip_tseitin_6 @ sk__3 @ sk__2))
% 0.57/0.90 <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl129, plain,
% 0.57/0.90 ((~ (zip_tseitin_5 @ sk__3 @ sk__2))
% 0.57/0.90 <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl14, zip_derived_cl89])).
% 0.57/0.90 thf(zip_derived_cl13, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (zip_tseitin_5 @ X0 @ X1) | (gt @ pv63 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_29])).
% 0.57/0.90 thf(zip_derived_cl132, plain,
% 0.57/0.90 (( (gt @ pv63 @ sk__2)) <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup+', [status(thm)], [zip_derived_cl129, zip_derived_cl13])).
% 0.57/0.90 thf(zip_derived_cl64, plain,
% 0.57/0.90 (![X16 : $i, X17 : $i]:
% 0.57/0.90 (~ (gt @ pv63 @ X16)
% 0.57/0.90 | ~ (leq @ X16 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ X16)
% 0.57/0.90 | ~ (leq @ n0 @ X17)
% 0.57/0.90 | ~ (leq @ X17 @ n5)
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ X16 @ X17) = (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_41])).
% 0.57/0.90 thf(zip_derived_cl275, plain,
% 0.57/0.90 ((![X0 : $i]:
% 0.57/0.90 (~ (leq @ sk__2 @ n5)
% 0.57/0.90 | ~ (leq @ n0 @ sk__2)
% 0.57/0.90 | ~ (leq @ n0 @ X0)
% 0.57/0.90 | ~ (leq @ X0 @ n5)
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ sk__2 @ X0) = (init))))
% 0.57/0.90 <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl132, zip_derived_cl64])).
% 0.57/0.90 thf(zip_derived_cl15, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_6 @ X0 @ X1) | (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_27])).
% 0.57/0.90 thf(zip_derived_cl89, plain,
% 0.57/0.90 ((~ (zip_tseitin_6 @ sk__3 @ sk__2))
% 0.57/0.90 <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl135, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__3 @ sk__2))
% 0.57/0.90 <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl15, zip_derived_cl89])).
% 0.57/0.90 thf(zip_derived_cl10, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n5) | ~ (zip_tseitin_4 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl138, plain,
% 0.57/0.90 (( (leq @ sk__2 @ n5)) <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl135, zip_derived_cl10])).
% 0.57/0.90 thf(zip_derived_cl135, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__3 @ sk__2))
% 0.57/0.90 <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl15, zip_derived_cl89])).
% 0.57/0.90 thf(zip_derived_cl8, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_4 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl137, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__2)) <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl135, zip_derived_cl8])).
% 0.57/0.90 thf(zip_derived_cl276, plain,
% 0.57/0.90 ((![X0 : $i]:
% 0.57/0.90 (~ (leq @ n0 @ X0)
% 0.57/0.90 | ~ (leq @ X0 @ n5)
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ sk__2 @ X0) = (init))))
% 0.57/0.90 <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('demod', [status(thm)],
% 0.57/0.90 [zip_derived_cl275, zip_derived_cl138, zip_derived_cl137])).
% 0.57/0.90 thf(zip_derived_cl129, plain,
% 0.57/0.90 ((~ (zip_tseitin_5 @ sk__3 @ sk__2))
% 0.57/0.90 <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl14, zip_derived_cl89])).
% 0.57/0.90 thf(zip_derived_cl12, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 ( (zip_tseitin_5 @ X0 @ X1)
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ X1 @ X0) != (init)))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_29])).
% 0.57/0.90 thf(zip_derived_cl131, plain,
% 0.57/0.90 ((((a_select3 @ id_ds1_filter_init @ sk__2 @ sk__3) != (init)))
% 0.57/0.90 <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup+', [status(thm)], [zip_derived_cl129, zip_derived_cl12])).
% 0.57/0.90 thf(zip_derived_cl278, plain,
% 0.57/0.90 (((~ (leq @ sk__3 @ n5) | ~ (leq @ n0 @ sk__3) | ((init) != (init))))
% 0.57/0.90 <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl276, zip_derived_cl131])).
% 0.57/0.90 thf(zip_derived_cl135, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__3 @ sk__2))
% 0.57/0.90 <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl15, zip_derived_cl89])).
% 0.57/0.90 thf(zip_derived_cl11, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n5) | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl140, plain,
% 0.57/0.90 (( (leq @ sk__3 @ n5)) <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl135, zip_derived_cl11])).
% 0.57/0.90 thf(zip_derived_cl135, plain,
% 0.57/0.90 (( (zip_tseitin_4 @ sk__3 @ sk__2))
% 0.57/0.90 <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl15, zip_derived_cl89])).
% 0.57/0.90 thf(zip_derived_cl9, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_31])).
% 0.57/0.90 thf(zip_derived_cl139, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__3)) <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl135, zip_derived_cl9])).
% 0.57/0.90 thf(zip_derived_cl280, plain,
% 0.57/0.90 ((((init) != (init))) <= (~ ( (zip_tseitin_6 @ sk__3 @ sk__2)))),
% 0.57/0.90 inference('demod', [status(thm)],
% 0.57/0.90 [zip_derived_cl278, zip_derived_cl140, zip_derived_cl139])).
% 0.57/0.90 thf('22', plain, (( (zip_tseitin_6 @ sk__3 @ sk__2))),
% 0.57/0.90 inference('simplify', [status(thm)], [zip_derived_cl280])).
% 0.57/0.90 thf('23', plain,
% 0.57/0.90 (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)) |
% 0.57/0.90 ~ ( (zip_tseitin_6 @ sk__3 @ sk__2)) | ~ ( (leq @ n0 @ pv5)) |
% 0.57/0.90 ~ ( (leq @ n0 @ pv63)) | ~ ( (leq @ n0 @ pv64)) |
% 0.57/0.90 ~ ( (leq @ pv63 @ n5)) |
% 0.57/0.90 (![X0 : $i, X1 : $i]:
% 0.57/0.90 (~ (leq @ n0 @ X0)
% 0.57/0.90 | ~ (leq @ X0 @ n5)
% 0.57/0.90 | ((X1) != (pv63))
% 0.57/0.90 | ((a_select3 @ id_ds1_filter_init @ X1 @ X0) = (init))
% 0.57/0.90 | ((pv64) = (X0))
% 0.57/0.90 | ~ (leq @ X0 @ pv64)
% 0.57/0.90 | ~ (leq @ n0 @ X1)
% 0.57/0.90 | ~ (leq @ X1 @ n5))) |
% 0.57/0.90 ~ ( (zip_tseitin_17 @ sk__17 @ sk__16)) |
% 0.57/0.90 ~ ( (zip_tseitin_16 @ sk__15 @ sk__14)) |
% 0.57/0.90 ~ ( (zip_tseitin_15 @ sk__13 @ sk__12)) |
% 0.57/0.90 ~ ( (zip_tseitin_14 @ sk__11 @ sk__10)) |
% 0.57/0.90 ~ ( (zip_tseitin_3 @ sk__1)) | ~ ( (zip_tseitin_12 @ sk__9 @ sk__8)) |
% 0.57/0.90 ~ ( (zip_tseitin_10 @ sk__7 @ sk__6)) |
% 0.57/0.90 ~ ( (zip_tseitin_9 @ sk__5 @ sk__4)) | ~ ( (leq @ pv64 @ n5)) |
% 0.57/0.90 ~ ( (leq @ pv5 @ n998)) | (((pv63) = (pv64)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.57/0.90 thf(zip_derived_cl221, plain,
% 0.57/0.90 (( (zip_tseitin_18 @ sk__19 @ sk__18))
% 0.57/0.90 <= (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl47, zip_derived_cl81])).
% 0.57/0.90 thf(zip_derived_cl45, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n5) | ~ (zip_tseitin_18 @ X0 @ X1))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.57/0.90 thf(zip_derived_cl236, plain,
% 0.57/0.90 (( (leq @ sk__19 @ n5)) <= (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl221, zip_derived_cl45])).
% 0.57/0.90 thf(zip_derived_cl225, plain,
% 0.57/0.90 ((~ (leq @ sk__19 @ n5)) <= (~ ( (leq @ sk__19 @ n5)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl224])).
% 0.57/0.90 thf('24', plain,
% 0.57/0.90 (( (leq @ sk__19 @ n5)) | ( (zip_tseitin_19 @ sk__19 @ sk__18))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl236, zip_derived_cl225])).
% 0.57/0.90 thf(zip_derived_cl221, plain,
% 0.57/0.90 (( (zip_tseitin_18 @ sk__19 @ sk__18))
% 0.57/0.90 <= (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl47, zip_derived_cl81])).
% 0.57/0.90 thf(zip_derived_cl44, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ X0 @ n2) | ~ (zip_tseitin_18 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.57/0.90 thf(zip_derived_cl234, plain,
% 0.57/0.90 (( (leq @ sk__18 @ n2)) <= (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl221, zip_derived_cl44])).
% 0.57/0.90 thf(zip_derived_cl228, plain,
% 0.57/0.90 ((~ (leq @ sk__18 @ n2)) <= (~ ( (leq @ sk__18 @ n2)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl224])).
% 0.57/0.90 thf('25', plain,
% 0.57/0.90 (( (leq @ sk__18 @ n2)) | ( (zip_tseitin_19 @ sk__19 @ sk__18))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl234, zip_derived_cl228])).
% 0.57/0.90 thf(zip_derived_cl221, plain,
% 0.57/0.90 (( (zip_tseitin_18 @ sk__19 @ sk__18))
% 0.57/0.90 <= (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl47, zip_derived_cl81])).
% 0.57/0.90 thf(zip_derived_cl42, plain,
% 0.57/0.90 (![X0 : $i, X1 : $i]: ( (leq @ n0 @ X0) | ~ (zip_tseitin_18 @ X1 @ X0))),
% 0.57/0.90 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.57/0.90 thf(zip_derived_cl233, plain,
% 0.57/0.90 (( (leq @ n0 @ sk__18)) <= (~ ( (zip_tseitin_19 @ sk__19 @ sk__18)))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl221, zip_derived_cl42])).
% 0.57/0.90 thf(zip_derived_cl227, plain,
% 0.57/0.90 ((~ (leq @ n0 @ sk__18)) <= (~ ( (leq @ n0 @ sk__18)))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl224])).
% 0.57/0.90 thf('26', plain,
% 0.57/0.90 (( (leq @ n0 @ sk__18)) | ( (zip_tseitin_19 @ sk__19 @ sk__18))),
% 0.57/0.90 inference('s_sup-', [status(thm)], [zip_derived_cl233, zip_derived_cl227])).
% 0.57/0.90 thf('27', plain,
% 0.57/0.90 (( (zip_tseitin_19 @ sk__19 @ sk__18)) | ~ ( (leq @ n0 @ sk__18)) |
% 0.57/0.90 ~ ( (leq @ sk__19 @ n5)) | ~ ( (leq @ sk__18 @ n2)) |
% 0.57/0.90 ~ ( (leq @ n0 @ sk__19))),
% 0.57/0.90 inference('split', [status(esa)], [zip_derived_cl224])).
% 0.57/0.90 thf(zip_derived_cl282, plain, ($false),
% 0.57/0.90 inference('sat_resolution*', [status(thm)],
% 0.57/0.90 ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9', '10', '11',
% 0.57/0.90 '12', '13', '14', '15', '16', '17', '18', '19', '20', '21',
% 0.57/0.90 '22', '23', '24', '25', '26', '27'])).
% 0.57/0.90
% 0.57/0.90 % SZS output end Refutation
% 0.57/0.90
% 0.57/0.90
% 0.57/0.90 % Terminating...
% 1.45/1.09 % Runner terminated.
% 1.45/1.11 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------