%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SYN723+1 : TPTP v9.2.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.ZDIERoQRMU true
% Computer : n014.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:05:37 PM UTC 2025
% Result : Theorem 0.52s 0.85s
% Output : Refutation 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SYN723+1 : TPTP v9.2.0. Released v2.5.0.
% 0.08/0.15 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.ZDIERoQRMU true
% 0.14/0.36 % Computer : n014.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed Oct 1 13:31:23 EDT 2025
% 0.14/0.36 % CPUTime :
% 0.14/0.36 % Running portfolio for 300 s
% 0.14/0.36 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.36 % Number of cores: 8
% 0.14/0.36 % Python version: Python 3.6.8
% 0.14/0.36 % Running in FO mode
% 0.50/0.62 % Total configuration time : 435
% 0.50/0.62 % Estimated wc time : 1092
% 0.50/0.62 % Estimated cpu time (7 cpus) : 156.0
% 0.50/0.69 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.50/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.50/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.50/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.50/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.50/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.50/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.52/0.85 % Solved by fo/fo1_av.sh.
% 0.52/0.85 % done 294 iterations in 0.086s
% 0.52/0.85 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.52/0.85 % SZS output start Refutation
% 0.52/0.85 thf(sk__16_type, type, sk__16: $i).
% 0.52/0.85 thf(zip_tseitin_10_type, type, zip_tseitin_10: $o).
% 0.52/0.85 thf(zip_tseitin_11_type, type, zip_tseitin_11: $o).
% 0.52/0.85 thf(sk__4_type, type, sk__4: $i).
% 0.52/0.85 thf(zip_tseitin_4_type, type, zip_tseitin_4: $o).
% 0.52/0.85 thf(sk__type, type, sk_: $i).
% 0.52/0.85 thf(sk__8_type, type, sk__8: $i > $i).
% 0.52/0.85 thf(q_type, type, q: $i > $o).
% 0.52/0.85 thf(r_type, type, r: $i > $o).
% 0.52/0.85 thf(zip_tseitin_3_type, type, zip_tseitin_3: $o).
% 0.52/0.85 thf(sk__25_type, type, sk__25: $i).
% 0.52/0.85 thf(zip_tseitin_12_type, type, zip_tseitin_12: $o).
% 0.52/0.85 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $o).
% 0.52/0.85 thf(sk__17_type, type, sk__17: $i).
% 0.52/0.85 thf(sk__18_type, type, sk__18: $i).
% 0.52/0.85 thf(p_type, type, p: $i > $o).
% 0.52/0.85 thf(sk__20_type, type, sk__20: $i > $i).
% 0.52/0.85 thf(sk__26_type, type, sk__26: $i).
% 0.52/0.85 thf(zip_tseitin_13_type, type, zip_tseitin_13: $o).
% 0.52/0.85 thf(sk__1_type, type, sk__1: $i).
% 0.52/0.85 thf(zip_tseitin_7_type, type, zip_tseitin_7: $i > $i > $o).
% 0.52/0.85 thf(sk__3_type, type, sk__3: $i).
% 0.52/0.85 thf(zip_tseitin_9_type, type, zip_tseitin_9: $o).
% 0.52/0.85 thf(sk__2_type, type, sk__2: $i).
% 0.52/0.85 thf(sk__13_type, type, sk__13: $i).
% 0.52/0.85 thf(zip_tseitin_6_type, type, zip_tseitin_6: $o).
% 0.52/0.85 thf(sk__29_type, type, sk__29: $i).
% 0.52/0.85 thf(sk__7_type, type, sk__7: $i).
% 0.52/0.85 thf(sk__15_type, type, sk__15: $i).
% 0.52/0.85 thf(sk__11_type, type, sk__11: $i > $i).
% 0.52/0.85 thf(sk__12_type, type, sk__12: $i).
% 0.52/0.85 thf(zip_tseitin_1_type, type, zip_tseitin_1: $o).
% 0.52/0.85 thf(sk__23_type, type, sk__23: $i > $i).
% 0.52/0.85 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $i > $o).
% 0.52/0.85 thf(sk__22_type, type, sk__22: $i).
% 0.52/0.85 thf(sk__10_type, type, sk__10: $i).
% 0.52/0.85 thf(sk__21_type, type, sk__21: $i).
% 0.52/0.85 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $o).
% 0.52/0.85 thf(sk__6_type, type, sk__6: $i).
% 0.52/0.85 thf(sk__24_type, type, sk__24: $i > $i).
% 0.52/0.85 thf(sk__14_type, type, sk__14: $i).
% 0.52/0.85 thf(sk__9_type, type, sk__9: $i).
% 0.52/0.85 thf(s_type, type, s: $i > $o).
% 0.52/0.85 thf(sk__19_type, type, sk__19: $i).
% 0.52/0.85 thf(sk__5_type, type, sk__5: $i).
% 0.52/0.85 thf(zip_tseitin_8_type, type, zip_tseitin_8: $o).
% 0.52/0.85 thf(sk__27_type, type, sk__27: $i > $i).
% 0.52/0.85 thf(sk__28_type, type, sk__28: $i > $i).
% 0.52/0.85 thf(thm138, conjecture,
% 0.52/0.85 (( ?[X:$i]: ( ![Y:$i]: ( ( p @ X ) <=> ( p @ Y ) ) ) ) <=>
% 0.52/0.85 ( ( ( ?[X:$i]: ( q @ X ) ) <=> ( ![Y:$i]: ( r @ Y ) ) ) <=>
% 0.52/0.85 ( ( ( ?[X:$i]: ( ![Y:$i]: ( ( q @ X ) <=> ( q @ Y ) ) ) ) <=>
% 0.52/0.85 ( ( ?[X:$i]: ( r @ X ) ) <=> ( ![Y:$i]: ( s @ Y ) ) ) ) <=>
% 0.52/0.85 ( ( ?[X:$i]: ( ![Y:$i]: ( ( r @ X ) <=> ( r @ Y ) ) ) ) <=>
% 0.52/0.85 ( ( ( ?[X:$i]: ( s @ X ) ) <=> ( ![Y:$i]: ( p @ Y ) ) ) <=>
% 0.52/0.85 ( ( ?[X:$i]: ( ![Y:$i]: ( ( s @ X ) <=> ( s @ Y ) ) ) ) <=>
% 0.52/0.85 ( ( ?[X:$i]: ( p @ X ) ) <=> ( ![Y:$i]: ( q @ Y ) ) ) ) ) ) ) ))).
% 0.52/0.85 thf(zf_stmt_0, axiom,
% 0.52/0.85 (![Y:$i,X:$i]:
% 0.52/0.85 ( ( zip_tseitin_5 @ Y @ X ) <=> ( ( r @ X ) <=> ( r @ Y ) ) ))).
% 0.52/0.85 thf(zip_derived_cl23, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_5 @ X0 @ X1) | (r @ X0) | (r @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.52/0.85 thf(zf_stmt_1, axiom,
% 0.52/0.85 (( zip_tseitin_11 ) <=>
% 0.52/0.85 ( ( ?[X:$i]: ( ![Y:$i]: ( zip_tseitin_5 @ Y @ X ) ) ) <=>
% 0.52/0.85 ( zip_tseitin_10 ) ))).
% 0.52/0.85 thf(zip_derived_cl45, plain,
% 0.52/0.85 (![X0 : $i]:
% 0.52/0.85 (~ (zip_tseitin_5 @ (sk__27 @ X0) @ X0)
% 0.52/0.85 | (zip_tseitin_10)
% 0.52/0.85 | ~ (zip_tseitin_11))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.52/0.85 thf(zip_derived_cl145, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_5 @ (sk__27 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_5 @ (sk__27 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl45])).
% 0.52/0.85 thf(zip_derived_cl239, plain,
% 0.52/0.85 ((![X0 : $i]: ( (r @ X0) | (r @ (sk__27 @ X0))))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_5 @ (sk__27 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl23, zip_derived_cl145])).
% 0.52/0.85 thf(zf_stmt_2, axiom,
% 0.52/0.85 (( zip_tseitin_3 ) <=>
% 0.52/0.85 ( ( ?[X:$i]: ( r @ X ) ) <=> ( ![Y:$i]: ( s @ Y ) ) ))).
% 0.52/0.85 thf(zip_derived_cl13, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]: (~ (r @ X0) | (s @ X1) | ~ (zip_tseitin_3))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.52/0.85 thf(zip_derived_cl74, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (r @ X0)) <= ((![X0 : $i]: ~ (r @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf(zip_derived_cl409, plain,
% 0.52/0.85 ((![X0 : $i]: (r @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (r @ X0)) &
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_5 @ (sk__27 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl239, zip_derived_cl74])).
% 0.52/0.85 thf(zip_derived_cl74, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (r @ X0)) <= ((![X0 : $i]: ~ (r @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf('0', plain,
% 0.52/0.85 (~ (![X0 : $i]: ~ (r @ X0)) |
% 0.52/0.85 ~ (![X0 : $i]: ~ (zip_tseitin_5 @ (sk__27 @ X0) @ X0))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl409, zip_derived_cl74])).
% 0.52/0.85 thf(zf_stmt_3, axiom,
% 0.52/0.85 (( zip_tseitin_4 ) <=>
% 0.52/0.85 ( ( ?[X:$i]: ( ![Y:$i]: ( zip_tseitin_2 @ Y @ X ) ) ) <=>
% 0.52/0.85 ( zip_tseitin_3 ) ))).
% 0.52/0.85 thf(zip_derived_cl19, plain,
% 0.52/0.85 (![X0 : $i]:
% 0.52/0.85 ( (zip_tseitin_4) | (zip_tseitin_3) | (zip_tseitin_2 @ X0 @ sk__9))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.52/0.85 thf(zip_derived_cl91, plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__9))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__9)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl19])).
% 0.52/0.85 thf(zf_stmt_4, axiom,
% 0.52/0.85 (![Y:$i,X:$i]:
% 0.52/0.85 ( ( zip_tseitin_2 @ Y @ X ) <=> ( ( q @ X ) <=> ( q @ Y ) ) ))).
% 0.52/0.85 thf(zip_derived_cl9, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 (~ (q @ X0) | (q @ X1) | ~ (zip_tseitin_2 @ X1 @ X0))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.52/0.85 thf(zip_derived_cl326, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (q @ sk__9) | (q @ X0)))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__9)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl91, zip_derived_cl9])).
% 0.52/0.85 thf('1', plain,
% 0.52/0.85 ((![X1 : $i]: (q @ X1)) |
% 0.52/0.85 ~ (![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__9)) | ~ ( (q @ sk__9))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl326])).
% 0.52/0.85 thf('2', plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__9)) | ( (zip_tseitin_3)) |
% 0.52/0.85 ( (zip_tseitin_4))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl19])).
% 0.52/0.85 thf(zip_derived_cl16, plain,
% 0.52/0.85 (![X0 : $i]:
% 0.52/0.85 (~ (zip_tseitin_3)
% 0.52/0.85 | (zip_tseitin_2 @ X0 @ sk__10)
% 0.52/0.85 | ~ (zip_tseitin_4))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.52/0.85 thf(zip_derived_cl82, plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__10))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__10)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl16])).
% 0.52/0.85 thf(zip_derived_cl17, plain,
% 0.52/0.85 (![X0 : $i]:
% 0.52/0.85 (~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0)
% 0.52/0.85 | (zip_tseitin_3)
% 0.52/0.85 | ~ (zip_tseitin_4))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.52/0.85 thf(zip_derived_cl85, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl17])).
% 0.52/0.85 thf('3', plain,
% 0.52/0.85 (~ (![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0)) |
% 0.52/0.85 ~ (![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__10))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl82, zip_derived_cl85])).
% 0.52/0.85 thf(zf_stmt_5, axiom,
% 0.52/0.85 (( zip_tseitin_9 ) <=>
% 0.52/0.85 ( ( ?[X:$i]: ( ![Y:$i]: ( zip_tseitin_7 @ Y @ X ) ) ) <=>
% 0.52/0.85 ( zip_tseitin_8 ) ))).
% 0.52/0.85 thf(zip_derived_cl39, plain,
% 0.52/0.85 (![X0 : $i]:
% 0.52/0.85 ( (zip_tseitin_9) | (zip_tseitin_8) | (zip_tseitin_7 @ X0 @ sk__21))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.52/0.85 thf(zip_derived_cl127, plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl39])).
% 0.52/0.85 thf(zip_derived_cl37, plain,
% 0.52/0.85 (![X0 : $i]:
% 0.52/0.85 (~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0)
% 0.52/0.85 | (zip_tseitin_8)
% 0.52/0.85 | ~ (zip_tseitin_9))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.52/0.85 thf(zip_derived_cl121, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl37])).
% 0.52/0.85 thf('4', plain,
% 0.52/0.85 (~ (![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21)) |
% 0.52/0.85 ~ (![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl127, zip_derived_cl121])).
% 0.52/0.85 thf(zip_derived_cl127, plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl39])).
% 0.52/0.85 thf(zf_stmt_6, axiom,
% 0.52/0.85 (![Y:$i,X:$i]:
% 0.52/0.85 ( ( zip_tseitin_7 @ Y @ X ) <=> ( ( s @ X ) <=> ( s @ Y ) ) ))).
% 0.52/0.85 thf(zip_derived_cl29, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 (~ (s @ X0) | (s @ X1) | ~ (zip_tseitin_7 @ X1 @ X0))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.52/0.85 thf(zip_derived_cl340, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (s @ sk__21) | (s @ X0)))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl127, zip_derived_cl29])).
% 0.52/0.85 thf('5', plain,
% 0.52/0.85 (~ ( (s @ sk__21)) | ~ (![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21)) |
% 0.52/0.85 (![X1 : $i]: (s @ X1))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl340])).
% 0.52/0.85 thf(zip_derived_cl127, plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl39])).
% 0.52/0.85 thf(zip_derived_cl38, plain,
% 0.52/0.85 (![X0 : $i]:
% 0.52/0.85 ( (zip_tseitin_9)
% 0.52/0.85 | ~ (zip_tseitin_8)
% 0.52/0.85 | ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.52/0.85 thf(zip_derived_cl124, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl38])).
% 0.52/0.85 thf('6', plain,
% 0.52/0.85 (~ (![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0)) |
% 0.52/0.85 ~ (![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl127, zip_derived_cl124])).
% 0.52/0.85 thf(zip_derived_cl127, plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl39])).
% 0.52/0.85 thf(zip_derived_cl28, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 (~ (s @ X0) | (s @ X1) | ~ (zip_tseitin_7 @ X0 @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.52/0.85 thf(zip_derived_cl339, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (s @ X0) | (s @ sk__21)))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl127, zip_derived_cl28])).
% 0.52/0.85 thf('7', plain,
% 0.52/0.85 (~ (![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21)) |
% 0.52/0.85 (![X0 : $i]: ~ (s @ X0)) | ( (s @ sk__21))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl339])).
% 0.52/0.85 thf('8', plain,
% 0.52/0.85 (( (zip_tseitin_9)) | ( (zip_tseitin_8)) |
% 0.52/0.85 (![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__21))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl39])).
% 0.52/0.85 thf(zip_derived_cl12, plain,
% 0.52/0.85 ((~ (s @ sk__7) | (r @ sk__6) | ~ (zip_tseitin_3))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.52/0.85 thf(zip_derived_cl71, plain, (( (r @ sk__6)) <= (( (r @ sk__6)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl12])).
% 0.52/0.85 thf(zip_derived_cl74, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (r @ X0)) <= ((![X0 : $i]: ~ (r @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf('9', plain, (~ ( (r @ sk__6)) | ~ (![X0 : $i]: ~ (r @ X0))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl71, zip_derived_cl74])).
% 0.52/0.85 thf('10', plain, (~ ( (s @ sk__7)) | ( (r @ sk__6)) | ~ ( (zip_tseitin_3))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl12])).
% 0.52/0.85 thf(zip_derived_cl36, plain,
% 0.52/0.85 (![X0 : $i]:
% 0.52/0.85 (~ (zip_tseitin_8)
% 0.52/0.85 | (zip_tseitin_7 @ X0 @ sk__22)
% 0.52/0.85 | ~ (zip_tseitin_9))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.52/0.85 thf('11', plain,
% 0.52/0.85 (~ ( (zip_tseitin_8)) | ~ ( (zip_tseitin_9)) |
% 0.52/0.85 (![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__22))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl36])).
% 0.52/0.85 thf(zip_derived_cl15, plain,
% 0.52/0.85 (![X0 : $i]: ( (zip_tseitin_3) | (s @ X0) | (r @ sk__5))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.52/0.85 thf(zip_derived_cl80, plain, (( (r @ sk__5)) <= (( (r @ sk__5)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl15])).
% 0.52/0.85 thf(zip_derived_cl74, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (r @ X0)) <= ((![X0 : $i]: ~ (r @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf('12', plain, (~ (![X0 : $i]: ~ (r @ X0)) | ~ ( (r @ sk__5))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl80, zip_derived_cl74])).
% 0.52/0.85 thf(zip_derived_cl44, plain,
% 0.52/0.85 (![X0 : $i]:
% 0.52/0.85 (~ (zip_tseitin_10)
% 0.52/0.85 | (zip_tseitin_5 @ X0 @ sk__26)
% 0.52/0.85 | ~ (zip_tseitin_11))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.52/0.85 thf(zip_derived_cl142, plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__26))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__26)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl44])).
% 0.52/0.85 thf(zip_derived_cl20, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 (~ (r @ X0) | (r @ X1) | ~ (zip_tseitin_5 @ X0 @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.52/0.85 thf(zip_derived_cl359, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (r @ X0) | (r @ sk__26)))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__26)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl142, zip_derived_cl20])).
% 0.52/0.85 thf('13', plain,
% 0.52/0.85 (~ (![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__26)) |
% 0.52/0.85 (![X0 : $i]: ~ (r @ X0)) | ( (r @ sk__26))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl359])).
% 0.52/0.85 thf(zip_derived_cl142, plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__26))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__26)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl44])).
% 0.52/0.85 thf(zip_derived_cl21, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 (~ (r @ X0) | (r @ X1) | ~ (zip_tseitin_5 @ X1 @ X0))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.52/0.85 thf(zip_derived_cl360, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (r @ sk__26) | (r @ X0)))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__26)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl142, zip_derived_cl21])).
% 0.52/0.85 thf('14', plain,
% 0.52/0.85 (~ (![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__26)) | ~ ( (r @ sk__26)) |
% 0.52/0.85 (![X1 : $i]: (r @ X1))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl360])).
% 0.52/0.85 thf('15', plain,
% 0.52/0.85 (( (r @ sk__5)) | ( (zip_tseitin_3)) | (![X1 : $i]: (s @ X1))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl15])).
% 0.52/0.85 thf('16', plain,
% 0.52/0.85 (~ ( (zip_tseitin_10)) | (![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__26)) |
% 0.52/0.85 ~ ( (zip_tseitin_11))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl44])).
% 0.52/0.85 thf(zf_stmt_7, axiom,
% 0.52/0.85 (( zip_tseitin_6 ) <=>
% 0.52/0.85 ( ( ?[X:$i]: ( s @ X ) ) <=> ( ![Y:$i]: ( p @ Y ) ) ))).
% 0.52/0.85 thf(zip_derived_cl27, plain,
% 0.52/0.85 (![X0 : $i]: ( (zip_tseitin_6) | (p @ X0) | (s @ sk__13))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.52/0.85 thf('17', plain,
% 0.52/0.85 (( (s @ sk__13)) | (![X1 : $i]: (p @ X1)) | ( (zip_tseitin_6))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl27])).
% 0.52/0.85 thf(zip_derived_cl23, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_5 @ X0 @ X1) | (r @ X0) | (r @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.52/0.85 thf(zip_derived_cl46, plain,
% 0.52/0.85 (![X0 : $i]:
% 0.52/0.85 ( (zip_tseitin_11)
% 0.52/0.85 | ~ (zip_tseitin_10)
% 0.52/0.85 | ~ (zip_tseitin_5 @ (sk__24 @ X0) @ X0))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.52/0.85 thf(zip_derived_cl148, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_5 @ (sk__24 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_5 @ (sk__24 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl46])).
% 0.52/0.85 thf(zip_derived_cl238, plain,
% 0.52/0.85 ((![X0 : $i]: ( (r @ X0) | (r @ (sk__24 @ X0))))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_5 @ (sk__24 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl23, zip_derived_cl148])).
% 0.52/0.85 thf(zip_derived_cl74, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (r @ X0)) <= ((![X0 : $i]: ~ (r @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf(zip_derived_cl407, plain,
% 0.52/0.85 ((![X0 : $i]: (r @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (r @ X0)) &
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_5 @ (sk__24 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl238, zip_derived_cl74])).
% 0.52/0.85 thf(zip_derived_cl74, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (r @ X0)) <= ((![X0 : $i]: ~ (r @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf('18', plain,
% 0.52/0.85 (~ (![X0 : $i]: ~ (zip_tseitin_5 @ (sk__24 @ X0) @ X0)) |
% 0.52/0.85 ~ (![X0 : $i]: ~ (r @ X0))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl407, zip_derived_cl74])).
% 0.52/0.85 thf(zip_derived_cl24, plain,
% 0.52/0.85 ((~ (p @ sk__15) | (s @ sk__14) | ~ (zip_tseitin_6))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.52/0.85 thf('19', plain,
% 0.52/0.85 (~ ( (p @ sk__15)) | ~ ( (zip_tseitin_6)) | ( (s @ sk__14))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl24])).
% 0.52/0.85 thf(zip_derived_cl25, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]: (~ (s @ X0) | (p @ X1) | ~ (zip_tseitin_6))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.52/0.85 thf(zip_derived_cl97, plain,
% 0.52/0.85 ((![X1 : $i]: (p @ X1)) <= ((![X1 : $i]: (p @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl25])).
% 0.52/0.85 thf(zip_derived_cl96, plain, ((~ (p @ sk__15)) <= (~ ( (p @ sk__15)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl24])).
% 0.52/0.85 thf('20', plain, (~ (![X1 : $i]: (p @ X1)) | ( (p @ sk__15))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl97, zip_derived_cl96])).
% 0.52/0.85 thf('21', plain,
% 0.52/0.85 (~ ( (zip_tseitin_3)) | (![X0 : $i]: ~ (r @ X0)) |
% 0.52/0.85 (![X1 : $i]: (s @ X1))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf(zip_derived_cl31, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_7 @ X0 @ X1) | (s @ X0) | (s @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.52/0.85 thf(zip_derived_cl121, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl37])).
% 0.52/0.85 thf(zip_derived_cl300, plain,
% 0.52/0.85 ((![X0 : $i]: ( (s @ X0) | (s @ (sk__23 @ X0))))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl31, zip_derived_cl121])).
% 0.52/0.85 thf(zip_derived_cl98, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (s @ X0)) <= ((![X0 : $i]: ~ (s @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl25])).
% 0.52/0.85 thf(zip_derived_cl413, plain,
% 0.52/0.85 ((![X0 : $i]: (s @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (s @ X0)) &
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl300, zip_derived_cl98])).
% 0.52/0.85 thf(zip_derived_cl98, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (s @ X0)) <= ((![X0 : $i]: ~ (s @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl25])).
% 0.52/0.85 thf('22', plain,
% 0.52/0.85 (~ (![X0 : $i]: ~ (s @ X0)) |
% 0.52/0.85 ~ (![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl413, zip_derived_cl98])).
% 0.52/0.85 thf(zip_derived_cl31, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_7 @ X0 @ X1) | (s @ X0) | (s @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.52/0.85 thf(zip_derived_cl124, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl38])).
% 0.52/0.85 thf(zip_derived_cl299, plain,
% 0.52/0.85 ((![X0 : $i]: ( (s @ X0) | (s @ (sk__20 @ X0))))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl31, zip_derived_cl124])).
% 0.52/0.85 thf(zip_derived_cl98, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (s @ X0)) <= ((![X0 : $i]: ~ (s @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl25])).
% 0.52/0.85 thf(zip_derived_cl411, plain,
% 0.52/0.85 ((![X0 : $i]: (s @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (s @ X0)) &
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl299, zip_derived_cl98])).
% 0.52/0.85 thf(zip_derived_cl348, plain, ((~ (s @ sk__21)) <= (~ ( (s @ sk__21)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl340])).
% 0.52/0.85 thf('23', plain,
% 0.52/0.85 (~ (![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0)) |
% 0.52/0.85 ~ (![X0 : $i]: ~ (s @ X0)) | ( (s @ sk__21))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl411, zip_derived_cl348])).
% 0.52/0.85 thf(zip_derived_cl378, plain, (( (s @ sk__21)) <= (( (s @ sk__21)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl339])).
% 0.52/0.85 thf(zip_derived_cl98, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (s @ X0)) <= ((![X0 : $i]: ~ (s @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl25])).
% 0.52/0.85 thf('24', plain, (~ ( (s @ sk__21)) | ~ (![X0 : $i]: ~ (s @ X0))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl378, zip_derived_cl98])).
% 0.52/0.85 thf(zip_derived_cl104, plain, (( (s @ sk__13)) <= (( (s @ sk__13)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl27])).
% 0.52/0.85 thf(zip_derived_cl98, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (s @ X0)) <= ((![X0 : $i]: ~ (s @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl25])).
% 0.52/0.85 thf('25', plain, (~ (![X0 : $i]: ~ (s @ X0)) | ~ ( (s @ sk__13))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl104, zip_derived_cl98])).
% 0.52/0.85 thf(zip_derived_cl95, plain, (( (s @ sk__14)) <= (( (s @ sk__14)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl24])).
% 0.52/0.85 thf(zip_derived_cl98, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (s @ X0)) <= ((![X0 : $i]: ~ (s @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl25])).
% 0.52/0.85 thf('26', plain, (~ ( (s @ sk__14)) | ~ (![X0 : $i]: ~ (s @ X0))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl95, zip_derived_cl98])).
% 0.52/0.85 thf('27', plain,
% 0.52/0.85 (~ ( (zip_tseitin_4)) |
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0)) |
% 0.52/0.85 ( (zip_tseitin_3))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl17])).
% 0.52/0.85 thf(zf_stmt_8, axiom,
% 0.52/0.85 (( zip_tseitin_1 ) <=>
% 0.52/0.85 ( ( ?[X:$i]: ( q @ X ) ) <=> ( ![Y:$i]: ( r @ Y ) ) ))).
% 0.52/0.85 thf(zip_derived_cl7, plain,
% 0.52/0.85 (![X0 : $i]: ( (zip_tseitin_1) | (r @ X0) | (q @ sk__1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.52/0.85 thf('28', plain,
% 0.52/0.85 (( (q @ sk__1)) | ( (zip_tseitin_1)) | (![X1 : $i]: (r @ X1))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl7])).
% 0.52/0.85 thf(zip_derived_cl11, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_2 @ X0 @ X1) | (q @ X0) | (q @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.52/0.85 thf(zip_derived_cl85, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl17])).
% 0.52/0.85 thf(zip_derived_cl205, plain,
% 0.52/0.85 ((![X0 : $i]: ( (q @ X0) | (q @ (sk__11 @ X0))))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl11, zip_derived_cl85])).
% 0.52/0.85 thf(zip_derived_cl5, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]: (~ (q @ X0) | (r @ X1) | ~ (zip_tseitin_1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.52/0.85 thf(zip_derived_cl62, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (q @ X0)) <= ((![X0 : $i]: ~ (q @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.85 thf(zip_derived_cl389, plain,
% 0.52/0.85 ((![X0 : $i]: (q @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (q @ X0)) &
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl205, zip_derived_cl62])).
% 0.52/0.85 thf(zip_derived_cl62, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (q @ X0)) <= ((![X0 : $i]: ~ (q @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.85 thf('29', plain,
% 0.52/0.85 (~ (![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0)) |
% 0.52/0.85 ~ (![X0 : $i]: ~ (q @ X0))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl389, zip_derived_cl62])).
% 0.52/0.85 thf(zip_derived_cl68, plain, (( (q @ sk__1)) <= (( (q @ sk__1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl7])).
% 0.52/0.85 thf(zip_derived_cl62, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (q @ X0)) <= ((![X0 : $i]: ~ (q @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.85 thf('30', plain, (~ (![X0 : $i]: ~ (q @ X0)) | ~ ( (q @ sk__1))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl68, zip_derived_cl62])).
% 0.52/0.85 thf(zf_stmt_9, axiom,
% 0.52/0.85 (( zip_tseitin_12 ) <=> ( ( zip_tseitin_4 ) <=> ( zip_tseitin_11 ) ))).
% 0.52/0.85 thf(zip_derived_cl51, plain,
% 0.52/0.85 (( (zip_tseitin_12) | (zip_tseitin_11) | (zip_tseitin_4))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_9])).
% 0.52/0.85 thf('31', plain,
% 0.52/0.85 (( (zip_tseitin_12)) | ( (zip_tseitin_11)) | ( (zip_tseitin_4))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl51])).
% 0.52/0.85 thf(zf_stmt_10, axiom,
% 0.52/0.85 (( zip_tseitin_8 ) <=>
% 0.52/0.85 ( ( ?[X:$i]: ( p @ X ) ) <=> ( ![Y:$i]: ( q @ Y ) ) ))).
% 0.52/0.85 thf(zip_derived_cl32, plain,
% 0.52/0.85 ((~ (q @ sk__19) | (p @ sk__18) | ~ (zip_tseitin_8))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_10])).
% 0.52/0.85 thf(zip_derived_cl107, plain, (( (p @ sk__18)) <= (( (p @ sk__18)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl32])).
% 0.52/0.85 thf(zip_derived_cl33, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]: (~ (p @ X0) | (q @ X1) | ~ (zip_tseitin_8))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_10])).
% 0.52/0.85 thf(zip_derived_cl110, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (p @ X0)) <= ((![X0 : $i]: ~ (p @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl33])).
% 0.52/0.85 thf('32', plain, (~ (![X0 : $i]: ~ (p @ X0)) | ~ ( (p @ sk__18))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl107, zip_derived_cl110])).
% 0.52/0.85 thf(zf_stmt_11, axiom,
% 0.52/0.85 (( zip_tseitin_10 ) <=> ( ( zip_tseitin_6 ) <=> ( zip_tseitin_9 ) ))).
% 0.52/0.85 thf(zip_derived_cl43, plain,
% 0.52/0.85 (( (zip_tseitin_10) | (zip_tseitin_9) | (zip_tseitin_6))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_11])).
% 0.52/0.85 thf('33', plain,
% 0.52/0.85 (( (zip_tseitin_9)) | ( (zip_tseitin_6)) | ( (zip_tseitin_10))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl43])).
% 0.52/0.85 thf(zip_derived_cl42, plain,
% 0.52/0.85 (( (zip_tseitin_10) | ~ (zip_tseitin_9) | ~ (zip_tseitin_6))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_11])).
% 0.52/0.85 thf('34', plain,
% 0.52/0.85 (~ ( (zip_tseitin_6)) | ~ ( (zip_tseitin_9)) | ( (zip_tseitin_10))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl42])).
% 0.52/0.85 thf(zip_derived_cl49, plain,
% 0.52/0.85 ((~ (zip_tseitin_4) | (zip_tseitin_11) | ~ (zip_tseitin_12))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_9])).
% 0.52/0.85 thf('35', plain,
% 0.52/0.85 (~ ( (zip_tseitin_4)) | ( (zip_tseitin_11)) | ~ ( (zip_tseitin_12))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl49])).
% 0.52/0.85 thf(zip_derived_cl109, plain,
% 0.52/0.85 ((![X1 : $i]: (q @ X1)) <= ((![X1 : $i]: (q @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl33])).
% 0.52/0.85 thf(zip_derived_cl108, plain, ((~ (q @ sk__19)) <= (~ ( (q @ sk__19)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl32])).
% 0.52/0.85 thf('36', plain, (( (q @ sk__19)) | ~ (![X1 : $i]: (q @ X1))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl109, zip_derived_cl108])).
% 0.52/0.85 thf('37', plain,
% 0.52/0.85 (( (p @ sk__18)) | ~ ( (zip_tseitin_8)) | ~ ( (q @ sk__19))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl32])).
% 0.52/0.85 thf('38', plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_5 @ (sk__27 @ X0) @ X0)) |
% 0.52/0.85 ~ ( (zip_tseitin_11)) | ( (zip_tseitin_10))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl45])).
% 0.52/0.85 thf(zip_derived_cl18, plain,
% 0.52/0.85 (![X0 : $i]:
% 0.52/0.85 ( (zip_tseitin_4)
% 0.52/0.85 | ~ (zip_tseitin_3)
% 0.52/0.85 | ~ (zip_tseitin_2 @ (sk__8 @ X0) @ X0))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.52/0.85 thf(zip_derived_cl88, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__8 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__8 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl18])).
% 0.52/0.85 thf(zip_derived_cl11, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_2 @ X0 @ X1) | (q @ X0) | (q @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.52/0.85 thf(zip_derived_cl213, plain,
% 0.52/0.85 ((![X0 : $i]: ( (q @ (sk__8 @ X0)) | (q @ X0)))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__8 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup+', [status(thm)], [zip_derived_cl88, zip_derived_cl11])).
% 0.52/0.85 thf(zip_derived_cl62, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (q @ X0)) <= ((![X0 : $i]: ~ (q @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.85 thf(zip_derived_cl403, plain,
% 0.52/0.85 ((![X0 : $i]: (q @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (q @ X0)) &
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_2 @ (sk__8 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl213, zip_derived_cl62])).
% 0.52/0.85 thf(zip_derived_cl62, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (q @ X0)) <= ((![X0 : $i]: ~ (q @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.85 thf('39', plain,
% 0.52/0.85 (~ (![X0 : $i]: ~ (zip_tseitin_2 @ (sk__8 @ X0) @ X0)) |
% 0.52/0.85 ~ (![X0 : $i]: ~ (q @ X0))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl403, zip_derived_cl62])).
% 0.52/0.85 thf(zf_stmt_12, axiom,
% 0.52/0.85 (( zip_tseitin_13 ) <=> ( ( zip_tseitin_1 ) <=> ( zip_tseitin_12 ) ))).
% 0.52/0.85 thf(zip_derived_cl53, plain,
% 0.52/0.85 ((~ (zip_tseitin_1) | (zip_tseitin_12) | ~ (zip_tseitin_13))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_12])).
% 0.52/0.85 thf('40', plain,
% 0.52/0.85 (~ ( (zip_tseitin_1)) | ( (zip_tseitin_12)) | ~ ( (zip_tseitin_13))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl53])).
% 0.52/0.85 thf(zip_derived_cl4, plain,
% 0.52/0.85 ((~ (r @ sk__3) | (q @ sk__2) | ~ (zip_tseitin_1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.52/0.85 thf('41', plain, (~ ( (r @ sk__3)) | ~ ( (zip_tseitin_1)) | ( (q @ sk__2))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl4])).
% 0.52/0.85 thf(zip_derived_cl82, plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__10))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__10)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl16])).
% 0.52/0.85 thf(zip_derived_cl9, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 (~ (q @ X0) | (q @ X1) | ~ (zip_tseitin_2 @ X1 @ X0))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.52/0.85 thf(zip_derived_cl312, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (q @ sk__10) | (q @ X0)))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__10)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl82, zip_derived_cl9])).
% 0.52/0.85 thf('42', plain,
% 0.52/0.85 (~ (![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__10)) |
% 0.52/0.85 (![X1 : $i]: (q @ X1)) | ~ ( (q @ sk__10))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl312])).
% 0.52/0.85 thf(zip_derived_cl82, plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__10))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__10)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl16])).
% 0.52/0.85 thf(zip_derived_cl8, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 (~ (q @ X0) | (q @ X1) | ~ (zip_tseitin_2 @ X0 @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.52/0.85 thf(zip_derived_cl311, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (q @ X0) | (q @ sk__10)))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__10)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl82, zip_derived_cl8])).
% 0.52/0.85 thf('43', plain,
% 0.52/0.85 (~ (![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__10)) | ( (q @ sk__10)) |
% 0.52/0.85 (![X0 : $i]: ~ (q @ X0))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl311])).
% 0.52/0.85 thf(zip_derived_cl52, plain,
% 0.52/0.85 ((~ (zip_tseitin_12) | (zip_tseitin_1) | ~ (zip_tseitin_13))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_12])).
% 0.52/0.85 thf('44', plain,
% 0.52/0.85 (~ ( (zip_tseitin_13)) | ~ ( (zip_tseitin_12)) | ( (zip_tseitin_1))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl52])).
% 0.52/0.85 thf('45', plain,
% 0.52/0.85 (~ ( (zip_tseitin_3)) | (![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__10)) |
% 0.52/0.85 ~ ( (zip_tseitin_4))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl16])).
% 0.52/0.85 thf(zip_derived_cl59, plain, (( (q @ sk__2)) <= (( (q @ sk__2)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl4])).
% 0.52/0.85 thf(zip_derived_cl62, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (q @ X0)) <= ((![X0 : $i]: ~ (q @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.85 thf('46', plain, (~ ( (q @ sk__2)) | ~ (![X0 : $i]: ~ (q @ X0))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl59, zip_derived_cl62])).
% 0.52/0.85 thf(zf_stmt_13, type, zip_tseitin_13 : $o).
% 0.52/0.85 thf(zf_stmt_14, type, zip_tseitin_12 : $o).
% 0.52/0.85 thf(zf_stmt_15, type, zip_tseitin_11 : $o).
% 0.52/0.85 thf(zf_stmt_16, type, zip_tseitin_10 : $o).
% 0.52/0.85 thf(zf_stmt_17, type, zip_tseitin_9 : $o).
% 0.52/0.85 thf(zf_stmt_18, type, zip_tseitin_8 : $o).
% 0.52/0.85 thf(zf_stmt_19, type, zip_tseitin_7 : $i > $i > $o).
% 0.52/0.85 thf(zf_stmt_20, type, zip_tseitin_6 : $o).
% 0.52/0.85 thf(zf_stmt_21, type, zip_tseitin_5 : $i > $i > $o).
% 0.52/0.85 thf(zf_stmt_22, type, zip_tseitin_4 : $o).
% 0.52/0.85 thf(zf_stmt_23, type, zip_tseitin_3 : $o).
% 0.52/0.85 thf(zf_stmt_24, type, zip_tseitin_2 : $i > $i > $o).
% 0.52/0.85 thf(zf_stmt_25, type, zip_tseitin_1 : $o).
% 0.52/0.85 thf(zf_stmt_26, type, zip_tseitin_0 : $i > $i > $o).
% 0.52/0.85 thf(zf_stmt_27, axiom,
% 0.52/0.85 (![Y:$i,X:$i]:
% 0.52/0.85 ( ( zip_tseitin_0 @ Y @ X ) <=> ( ( p @ X ) <=> ( p @ Y ) ) ))).
% 0.52/0.85 thf(zf_stmt_28, conjecture,
% 0.52/0.85 (( ?[X:$i]: ( ![Y:$i]: ( zip_tseitin_0 @ Y @ X ) ) ) <=> ( zip_tseitin_13 ))).
% 0.52/0.85 thf(zf_stmt_29, negated_conjecture,
% 0.52/0.85 (~( ( ?[X:$i]: ( ![Y:$i]: ( zip_tseitin_0 @ Y @ X ) ) ) <=>
% 0.52/0.85 ( zip_tseitin_13 ) )),
% 0.52/0.85 inference('cnf.neg', [status(esa)], [zf_stmt_28])).
% 0.52/0.85 thf(zip_derived_cl56, plain,
% 0.52/0.85 (![X0 : $i]: ( (zip_tseitin_13) | (zip_tseitin_0 @ X0 @ sk__29))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_29])).
% 0.52/0.85 thf('47', plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_0 @ X0 @ sk__29)) | ( (zip_tseitin_13))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl56])).
% 0.52/0.85 thf(zip_derived_cl35, plain,
% 0.52/0.85 (![X0 : $i]: ( (zip_tseitin_8) | (q @ X0) | (p @ sk__17))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_10])).
% 0.52/0.85 thf(zip_derived_cl116, plain, (( (p @ sk__17)) <= (( (p @ sk__17)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl35])).
% 0.52/0.85 thf(zip_derived_cl110, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (p @ X0)) <= ((![X0 : $i]: ~ (p @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl33])).
% 0.52/0.85 thf('48', plain, (~ (![X0 : $i]: ~ (p @ X0)) | ~ ( (p @ sk__17))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl116, zip_derived_cl110])).
% 0.52/0.85 thf('49', plain,
% 0.52/0.85 (( (p @ sk__17)) | (![X1 : $i]: (q @ X1)) | ( (zip_tseitin_8))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl35])).
% 0.52/0.85 thf(zip_derived_cl97, plain,
% 0.52/0.85 ((![X1 : $i]: (p @ X1)) <= ((![X1 : $i]: (p @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl25])).
% 0.52/0.85 thf(zip_derived_cl26, plain,
% 0.52/0.85 (![X0 : $i]: ( (zip_tseitin_6) | ~ (p @ sk__12) | ~ (s @ X0))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.52/0.85 thf(zip_derived_cl101, plain, ((~ (p @ sk__12)) <= (~ ( (p @ sk__12)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl26])).
% 0.52/0.85 thf('50', plain, (~ (![X1 : $i]: (p @ X1)) | ( (p @ sk__12))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl97, zip_derived_cl101])).
% 0.52/0.85 thf('51', plain,
% 0.52/0.85 (~ ( (p @ sk__12)) | ( (zip_tseitin_6)) | (![X0 : $i]: ~ (s @ X0))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl26])).
% 0.52/0.85 thf('52', plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0)) |
% 0.52/0.85 ( (zip_tseitin_8)) | ~ ( (zip_tseitin_9))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl37])).
% 0.52/0.85 thf(zip_derived_cl97, plain,
% 0.52/0.85 ((![X1 : $i]: (p @ X1)) <= ((![X1 : $i]: (p @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl25])).
% 0.52/0.85 thf(zip_derived_cl110, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (p @ X0)) <= ((![X0 : $i]: ~ (p @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl33])).
% 0.52/0.85 thf('53', plain, (~ (![X0 : $i]: ~ (p @ X0)) | ~ (![X1 : $i]: (p @ X1))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl97, zip_derived_cl110])).
% 0.52/0.85 thf(zip_derived_cl41, plain,
% 0.52/0.85 ((~ (zip_tseitin_6) | (zip_tseitin_9) | ~ (zip_tseitin_10))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_11])).
% 0.52/0.85 thf('54', plain,
% 0.52/0.85 (~ ( (zip_tseitin_10)) | ~ ( (zip_tseitin_6)) | ( (zip_tseitin_9))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl41])).
% 0.52/0.85 thf('55', plain,
% 0.52/0.85 (~ ( (zip_tseitin_8)) | (![X1 : $i]: (q @ X1)) |
% 0.52/0.85 (![X0 : $i]: ~ (p @ X0))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl33])).
% 0.52/0.85 thf(zip_derived_cl178, plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_0 @ X0 @ sk__29))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_0 @ X0 @ sk__29)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl56])).
% 0.52/0.85 thf(zip_derived_cl0, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 (~ (p @ X0) | (p @ X1) | ~ (zip_tseitin_0 @ X0 @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_27])).
% 0.52/0.85 thf(zip_derived_cl385, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (p @ X0) | (p @ sk__29)))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_0 @ X0 @ sk__29)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl178, zip_derived_cl0])).
% 0.52/0.85 thf('56', plain,
% 0.52/0.85 (( (p @ sk__29)) | (![X0 : $i]: ~ (p @ X0)) |
% 0.52/0.85 ~ (![X0 : $i]: (zip_tseitin_0 @ X0 @ sk__29))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl385])).
% 0.52/0.85 thf(zip_derived_cl40, plain,
% 0.52/0.85 ((~ (zip_tseitin_9) | (zip_tseitin_6) | ~ (zip_tseitin_10))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_11])).
% 0.52/0.85 thf('57', plain,
% 0.52/0.85 (~ ( (zip_tseitin_10)) | ~ ( (zip_tseitin_9)) | ( (zip_tseitin_6))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl40])).
% 0.52/0.85 thf(zip_derived_cl34, plain,
% 0.52/0.85 (![X0 : $i]: ( (zip_tseitin_8) | ~ (q @ sk__16) | ~ (p @ X0))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_10])).
% 0.52/0.85 thf('58', plain,
% 0.52/0.85 (( (zip_tseitin_8)) | (![X0 : $i]: ~ (p @ X0)) | ~ ( (q @ sk__16))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl34])).
% 0.52/0.85 thf(zip_derived_cl57, plain,
% 0.52/0.85 (![X1 : $i]:
% 0.52/0.85 (~ (zip_tseitin_13) | ~ (zip_tseitin_0 @ (sk__28 @ X1) @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_29])).
% 0.52/0.85 thf(zip_derived_cl180, plain,
% 0.52/0.85 ((![X1 : $i]: ~ (zip_tseitin_0 @ (sk__28 @ X1) @ X1))
% 0.52/0.85 <= ((![X1 : $i]: ~ (zip_tseitin_0 @ (sk__28 @ X1) @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl57])).
% 0.52/0.85 thf(zip_derived_cl3, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_0 @ X0 @ X1) | (p @ X0) | (p @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_27])).
% 0.52/0.85 thf(zip_derived_cl232, plain,
% 0.52/0.85 ((![X0 : $i]: ( (p @ (sk__28 @ X0)) | (p @ X0)))
% 0.52/0.85 <= ((![X1 : $i]: ~ (zip_tseitin_0 @ (sk__28 @ X1) @ X1)))),
% 0.52/0.85 inference('s_sup+', [status(thm)], [zip_derived_cl180, zip_derived_cl3])).
% 0.52/0.85 thf(zip_derived_cl110, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (p @ X0)) <= ((![X0 : $i]: ~ (p @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl33])).
% 0.52/0.85 thf(zip_derived_cl405, plain,
% 0.52/0.85 ((![X0 : $i]: (p @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (p @ X0)) &
% 0.52/0.85 (![X1 : $i]: ~ (zip_tseitin_0 @ (sk__28 @ X1) @ X1)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl232, zip_derived_cl110])).
% 0.52/0.85 thf(zip_derived_cl110, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (p @ X0)) <= ((![X0 : $i]: ~ (p @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl33])).
% 0.52/0.85 thf('59', plain,
% 0.52/0.85 (~ (![X0 : $i]: ~ (p @ X0)) |
% 0.52/0.85 ~ (![X1 : $i]: ~ (zip_tseitin_0 @ (sk__28 @ X1) @ X1))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl405, zip_derived_cl110])).
% 0.52/0.85 thf(zip_derived_cl97, plain,
% 0.52/0.85 ((![X1 : $i]: (p @ X1)) <= ((![X1 : $i]: (p @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl25])).
% 0.52/0.85 thf(zip_derived_cl180, plain,
% 0.52/0.85 ((![X1 : $i]: ~ (zip_tseitin_0 @ (sk__28 @ X1) @ X1))
% 0.52/0.85 <= ((![X1 : $i]: ~ (zip_tseitin_0 @ (sk__28 @ X1) @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl57])).
% 0.52/0.85 thf(zip_derived_cl2, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_0 @ X0 @ X1) | ~ (p @ X0) | ~ (p @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_27])).
% 0.52/0.85 thf(zip_derived_cl231, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (p @ (sk__28 @ X0)) | ~ (p @ X0)))
% 0.52/0.85 <= ((![X1 : $i]: ~ (zip_tseitin_0 @ (sk__28 @ X1) @ X1)))),
% 0.52/0.85 inference('s_sup+', [status(thm)], [zip_derived_cl180, zip_derived_cl2])).
% 0.52/0.85 thf(zip_derived_cl278, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (p @ X0))
% 0.52/0.85 <= ((![X1 : $i]: (p @ X1)) &
% 0.52/0.85 (![X1 : $i]: ~ (zip_tseitin_0 @ (sk__28 @ X1) @ X1)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl97, zip_derived_cl231])).
% 0.52/0.85 thf(zip_derived_cl97, plain,
% 0.52/0.85 ((![X1 : $i]: (p @ X1)) <= ((![X1 : $i]: (p @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl25])).
% 0.52/0.85 thf('60', plain,
% 0.52/0.85 (~ (![X1 : $i]: (p @ X1)) |
% 0.52/0.85 ~ (![X1 : $i]: ~ (zip_tseitin_0 @ (sk__28 @ X1) @ X1))),
% 0.52/0.85 inference('demod', [status(thm)], [zip_derived_cl278, zip_derived_cl97])).
% 0.52/0.85 thf('61', plain,
% 0.52/0.85 (~ ( (zip_tseitin_13)) |
% 0.52/0.85 (![X1 : $i]: ~ (zip_tseitin_0 @ (sk__28 @ X1) @ X1))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl57])).
% 0.52/0.85 thf(zip_derived_cl54, plain,
% 0.52/0.85 (( (zip_tseitin_13) | ~ (zip_tseitin_12) | ~ (zip_tseitin_1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_12])).
% 0.52/0.85 thf('62', plain,
% 0.52/0.85 (~ ( (zip_tseitin_1)) | ~ ( (zip_tseitin_12)) | ( (zip_tseitin_13))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl54])).
% 0.52/0.85 thf(zip_derived_cl50, plain,
% 0.52/0.85 (( (zip_tseitin_12) | ~ (zip_tseitin_11) | ~ (zip_tseitin_4))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_9])).
% 0.52/0.85 thf('63', plain,
% 0.52/0.85 (~ ( (zip_tseitin_4)) | ~ ( (zip_tseitin_11)) | ( (zip_tseitin_12))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl50])).
% 0.52/0.85 thf('64', plain,
% 0.52/0.85 (~ ( (zip_tseitin_3)) |
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_2 @ (sk__8 @ X0) @ X0)) | ( (zip_tseitin_4))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl18])).
% 0.52/0.85 thf('65', plain,
% 0.52/0.85 (( (zip_tseitin_9)) | ~ ( (zip_tseitin_8)) |
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl38])).
% 0.52/0.85 thf('66', plain,
% 0.52/0.85 (~ ( (zip_tseitin_10)) |
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_5 @ (sk__24 @ X0) @ X0)) |
% 0.52/0.85 ( (zip_tseitin_11))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl46])).
% 0.52/0.85 thf(zip_derived_cl14, plain,
% 0.52/0.85 (![X0 : $i]: ( (zip_tseitin_3) | ~ (s @ sk__4) | ~ (r @ X0))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.52/0.85 thf('67', plain,
% 0.52/0.85 (~ ( (s @ sk__4)) | (![X0 : $i]: ~ (r @ X0)) | ( (zip_tseitin_3))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl14])).
% 0.52/0.85 thf(zip_derived_cl61, plain,
% 0.52/0.85 ((![X1 : $i]: (r @ X1)) <= ((![X1 : $i]: (r @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.85 thf(zip_derived_cl148, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_5 @ (sk__24 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_5 @ (sk__24 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl46])).
% 0.52/0.85 thf(zip_derived_cl22, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_5 @ X0 @ X1) | ~ (r @ X0) | ~ (r @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.52/0.85 thf(zip_derived_cl229, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (r @ (sk__24 @ X0)) | ~ (r @ X0)))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_5 @ (sk__24 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup+', [status(thm)], [zip_derived_cl148, zip_derived_cl22])).
% 0.52/0.85 thf(zip_derived_cl274, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (r @ X0))
% 0.52/0.85 <= ((![X1 : $i]: (r @ X1)) &
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_5 @ (sk__24 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl61, zip_derived_cl229])).
% 0.52/0.85 thf(zip_derived_cl61, plain,
% 0.52/0.85 ((![X1 : $i]: (r @ X1)) <= ((![X1 : $i]: (r @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.85 thf('68', plain,
% 0.52/0.85 (~ (![X0 : $i]: ~ (zip_tseitin_5 @ (sk__24 @ X0) @ X0)) |
% 0.52/0.85 ~ (![X1 : $i]: (r @ X1))),
% 0.52/0.85 inference('demod', [status(thm)], [zip_derived_cl274, zip_derived_cl61])).
% 0.52/0.85 thf(zip_derived_cl6, plain,
% 0.52/0.85 (![X0 : $i]: ( (zip_tseitin_1) | ~ (r @ sk_) | ~ (q @ X0))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.52/0.85 thf('69', plain,
% 0.52/0.85 (~ ( (r @ sk_)) | ( (zip_tseitin_1)) | (![X0 : $i]: ~ (q @ X0))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl6])).
% 0.52/0.85 thf(zip_derived_cl73, plain,
% 0.52/0.85 ((![X1 : $i]: (s @ X1)) <= ((![X1 : $i]: (s @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf(zip_derived_cl30, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_7 @ X0 @ X1) | ~ (s @ X0) | ~ (s @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.52/0.85 thf(zip_derived_cl121, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl37])).
% 0.52/0.85 thf(zip_derived_cl284, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (s @ X0) | ~ (s @ (sk__23 @ X0))))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl30, zip_derived_cl121])).
% 0.52/0.85 thf(zip_derived_cl294, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (s @ X0))
% 0.52/0.85 <= ((![X1 : $i]: (s @ X1)) &
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl73, zip_derived_cl284])).
% 0.52/0.85 thf(zip_derived_cl73, plain,
% 0.52/0.85 ((![X1 : $i]: (s @ X1)) <= ((![X1 : $i]: (s @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf('70', plain,
% 0.52/0.85 (~ (![X1 : $i]: (s @ X1)) |
% 0.52/0.85 ~ (![X0 : $i]: ~ (zip_tseitin_7 @ (sk__23 @ X0) @ X0))),
% 0.52/0.85 inference('demod', [status(thm)], [zip_derived_cl294, zip_derived_cl73])).
% 0.52/0.85 thf(zip_derived_cl73, plain,
% 0.52/0.85 ((![X1 : $i]: (s @ X1)) <= ((![X1 : $i]: (s @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf(zip_derived_cl30, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_7 @ X0 @ X1) | ~ (s @ X0) | ~ (s @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.52/0.85 thf(zip_derived_cl124, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl38])).
% 0.52/0.85 thf(zip_derived_cl283, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (s @ X0) | ~ (s @ (sk__20 @ X0))))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl30, zip_derived_cl124])).
% 0.52/0.85 thf(zip_derived_cl290, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (s @ X0))
% 0.52/0.85 <= ((![X1 : $i]: (s @ X1)) &
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl73, zip_derived_cl283])).
% 0.52/0.85 thf(zip_derived_cl73, plain,
% 0.52/0.85 ((![X1 : $i]: (s @ X1)) <= ((![X1 : $i]: (s @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf('71', plain,
% 0.52/0.85 (~ (![X0 : $i]: ~ (zip_tseitin_7 @ (sk__20 @ X0) @ X0)) |
% 0.52/0.85 ~ (![X1 : $i]: (s @ X1))),
% 0.52/0.85 inference('demod', [status(thm)], [zip_derived_cl290, zip_derived_cl73])).
% 0.52/0.85 thf(zip_derived_cl73, plain,
% 0.52/0.85 ((![X1 : $i]: (s @ X1)) <= ((![X1 : $i]: (s @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf(zip_derived_cl72, plain, ((~ (s @ sk__7)) <= (~ ( (s @ sk__7)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl12])).
% 0.52/0.85 thf('72', plain, (( (s @ sk__7)) | ~ (![X1 : $i]: (s @ X1))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl73, zip_derived_cl72])).
% 0.52/0.85 thf(zip_derived_cl73, plain,
% 0.52/0.85 ((![X1 : $i]: (s @ X1)) <= ((![X1 : $i]: (s @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf(zip_derived_cl77, plain, ((~ (s @ sk__4)) <= (~ ( (s @ sk__4)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl14])).
% 0.52/0.85 thf('73', plain, (~ (![X1 : $i]: (s @ X1)) | ( (s @ sk__4))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl73, zip_derived_cl77])).
% 0.52/0.85 thf(zip_derived_cl73, plain,
% 0.52/0.85 ((![X1 : $i]: (s @ X1)) <= ((![X1 : $i]: (s @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf(zip_derived_cl98, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (s @ X0)) <= ((![X0 : $i]: ~ (s @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl25])).
% 0.52/0.85 thf('74', plain, (~ (![X1 : $i]: (s @ X1)) | ~ (![X0 : $i]: ~ (s @ X0))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl73, zip_derived_cl98])).
% 0.52/0.85 thf('75', plain,
% 0.52/0.85 (~ ( (zip_tseitin_6)) | (![X1 : $i]: (p @ X1)) |
% 0.52/0.85 (![X0 : $i]: ~ (s @ X0))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl25])).
% 0.52/0.85 thf(zip_derived_cl61, plain,
% 0.52/0.85 ((![X1 : $i]: (r @ X1)) <= ((![X1 : $i]: (r @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.85 thf(zip_derived_cl145, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_5 @ (sk__27 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_5 @ (sk__27 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl45])).
% 0.52/0.85 thf(zip_derived_cl22, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_5 @ X0 @ X1) | ~ (r @ X0) | ~ (r @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.52/0.85 thf(zip_derived_cl227, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (r @ (sk__27 @ X0)) | ~ (r @ X0)))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_5 @ (sk__27 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup+', [status(thm)], [zip_derived_cl145, zip_derived_cl22])).
% 0.52/0.85 thf(zip_derived_cl269, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (r @ X0))
% 0.52/0.85 <= ((![X1 : $i]: (r @ X1)) &
% 0.52/0.85 (![X0 : $i]: ~ (zip_tseitin_5 @ (sk__27 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl61, zip_derived_cl227])).
% 0.52/0.85 thf(zip_derived_cl61, plain,
% 0.52/0.85 ((![X1 : $i]: (r @ X1)) <= ((![X1 : $i]: (r @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.85 thf('76', plain,
% 0.52/0.85 (~ (![X1 : $i]: (r @ X1)) |
% 0.52/0.85 ~ (![X0 : $i]: ~ (zip_tseitin_5 @ (sk__27 @ X0) @ X0))),
% 0.52/0.85 inference('demod', [status(thm)], [zip_derived_cl269, zip_derived_cl61])).
% 0.52/0.85 thf(zip_derived_cl61, plain,
% 0.52/0.85 ((![X1 : $i]: (r @ X1)) <= ((![X1 : $i]: (r @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.85 thf(zip_derived_cl60, plain, ((~ (r @ sk__3)) <= (~ ( (r @ sk__3)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl4])).
% 0.52/0.85 thf('77', plain, (~ (![X1 : $i]: (r @ X1)) | ( (r @ sk__3))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl61, zip_derived_cl60])).
% 0.52/0.85 thf(zip_derived_cl61, plain,
% 0.52/0.85 ((![X1 : $i]: (r @ X1)) <= ((![X1 : $i]: (r @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.85 thf(zip_derived_cl65, plain, ((~ (r @ sk_)) <= (~ ( (r @ sk_)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl6])).
% 0.52/0.85 thf('78', plain, (~ (![X1 : $i]: (r @ X1)) | ( (r @ sk_))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl61, zip_derived_cl65])).
% 0.52/0.85 thf(zip_derived_cl61, plain,
% 0.52/0.85 ((![X1 : $i]: (r @ X1)) <= ((![X1 : $i]: (r @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.85 thf(zip_derived_cl74, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (r @ X0)) <= ((![X0 : $i]: ~ (r @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl13])).
% 0.52/0.85 thf('79', plain, (~ (![X1 : $i]: (r @ X1)) | ~ (![X0 : $i]: ~ (r @ X0))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl61, zip_derived_cl74])).
% 0.52/0.85 thf(zip_derived_cl85, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl17])).
% 0.52/0.85 thf(zip_derived_cl10, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_2 @ X0 @ X1) | ~ (q @ X0) | ~ (q @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.52/0.85 thf(zip_derived_cl198, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (q @ (sk__11 @ X0)) | ~ (q @ X0)))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup+', [status(thm)], [zip_derived_cl85, zip_derived_cl10])).
% 0.52/0.85 thf(zip_derived_cl109, plain,
% 0.52/0.85 ((![X1 : $i]: (q @ X1)) <= ((![X1 : $i]: (q @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl33])).
% 0.52/0.85 thf(zip_derived_cl262, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (q @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0)) &
% 0.52/0.85 (![X1 : $i]: (q @ X1)))),
% 0.52/0.85 inference('s_sup+', [status(thm)], [zip_derived_cl198, zip_derived_cl109])).
% 0.52/0.85 thf(zip_derived_cl109, plain,
% 0.52/0.85 ((![X1 : $i]: (q @ X1)) <= ((![X1 : $i]: (q @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl33])).
% 0.52/0.85 thf('80', plain,
% 0.52/0.85 (~ (![X0 : $i]: ~ (zip_tseitin_2 @ (sk__11 @ X0) @ X0)) |
% 0.52/0.85 ~ (![X1 : $i]: (q @ X1))),
% 0.52/0.85 inference('demod', [status(thm)], [zip_derived_cl262, zip_derived_cl109])).
% 0.52/0.85 thf(zip_derived_cl88, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__8 @ X0) @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__8 @ X0) @ X0)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl18])).
% 0.52/0.85 thf(zip_derived_cl10, plain,
% 0.52/0.85 (![X0 : $i, X1 : $i]:
% 0.52/0.85 ( (zip_tseitin_2 @ X0 @ X1) | ~ (q @ X0) | ~ (q @ X1))),
% 0.52/0.85 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.52/0.85 thf(zip_derived_cl212, plain,
% 0.52/0.85 ((![X0 : $i]: (~ (q @ (sk__8 @ X0)) | ~ (q @ X0)))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__8 @ X0) @ X0)))),
% 0.52/0.85 inference('s_sup+', [status(thm)], [zip_derived_cl88, zip_derived_cl10])).
% 0.52/0.85 thf(zip_derived_cl109, plain,
% 0.52/0.85 ((![X1 : $i]: (q @ X1)) <= ((![X1 : $i]: (q @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl33])).
% 0.52/0.85 thf(zip_derived_cl261, plain,
% 0.52/0.85 ((![X0 : $i]: ~ (q @ X0))
% 0.52/0.85 <= ((![X0 : $i]: ~ (zip_tseitin_2 @ (sk__8 @ X0) @ X0)) &
% 0.52/0.85 (![X1 : $i]: (q @ X1)))),
% 0.52/0.85 inference('s_sup+', [status(thm)], [zip_derived_cl212, zip_derived_cl109])).
% 0.52/0.85 thf(zip_derived_cl109, plain,
% 0.52/0.85 ((![X1 : $i]: (q @ X1)) <= ((![X1 : $i]: (q @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl33])).
% 0.52/0.85 thf('81', plain,
% 0.52/0.85 (~ (![X0 : $i]: ~ (zip_tseitin_2 @ (sk__8 @ X0) @ X0)) |
% 0.52/0.85 ~ (![X1 : $i]: (q @ X1))),
% 0.52/0.85 inference('demod', [status(thm)], [zip_derived_cl261, zip_derived_cl109])).
% 0.52/0.85 thf(zip_derived_cl109, plain,
% 0.52/0.85 ((![X1 : $i]: (q @ X1)) <= ((![X1 : $i]: (q @ X1)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl33])).
% 0.52/0.85 thf(zip_derived_cl113, plain, ((~ (q @ sk__16)) <= (~ ( (q @ sk__16)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl34])).
% 0.52/0.85 thf('82', plain, (( (q @ sk__16)) | ~ (![X1 : $i]: (q @ X1))),
% 0.52/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl109, zip_derived_cl113])).
% 0.52/0.85 thf(zip_derived_cl91, plain,
% 0.52/0.85 ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__9))
% 0.52/0.85 <= ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__9)))),
% 0.52/0.85 inference('split', [status(esa)], [zip_derived_cl19])).
% 0.52/0.86 thf(zip_derived_cl8, plain,
% 0.52/0.86 (![X0 : $i, X1 : $i]:
% 0.52/0.86 (~ (q @ X0) | (q @ X1) | ~ (zip_tseitin_2 @ X0 @ X1))),
% 0.52/0.86 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.52/0.86 thf(zip_derived_cl325, plain,
% 0.52/0.86 ((![X0 : $i]: (~ (q @ X0) | (q @ sk__9)))
% 0.52/0.86 <= ((![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__9)))),
% 0.52/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl91, zip_derived_cl8])).
% 0.52/0.86 thf('83', plain,
% 0.52/0.86 (( (q @ sk__9)) | ~ (![X0 : $i]: (zip_tseitin_2 @ X0 @ sk__9)) |
% 0.52/0.86 (![X0 : $i]: ~ (q @ X0))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl325])).
% 0.52/0.86 thf(zip_derived_cl118, plain,
% 0.52/0.86 ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__22))
% 0.52/0.86 <= ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__22)))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl36])).
% 0.52/0.86 thf(zip_derived_cl28, plain,
% 0.52/0.86 (![X0 : $i, X1 : $i]:
% 0.52/0.86 (~ (s @ X0) | (s @ X1) | ~ (zip_tseitin_7 @ X0 @ X1))),
% 0.52/0.86 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.52/0.86 thf(zip_derived_cl333, plain,
% 0.52/0.86 ((![X0 : $i]: (~ (s @ X0) | (s @ sk__22)))
% 0.52/0.86 <= ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__22)))),
% 0.52/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl118, zip_derived_cl28])).
% 0.52/0.86 thf('84', plain,
% 0.52/0.86 (~ (![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__22)) |
% 0.52/0.86 (![X0 : $i]: ~ (s @ X0)) | ( (s @ sk__22))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl333])).
% 0.52/0.86 thf(zip_derived_cl118, plain,
% 0.52/0.86 ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__22))
% 0.52/0.86 <= ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__22)))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl36])).
% 0.52/0.86 thf(zip_derived_cl29, plain,
% 0.52/0.86 (![X0 : $i, X1 : $i]:
% 0.52/0.86 (~ (s @ X0) | (s @ X1) | ~ (zip_tseitin_7 @ X1 @ X0))),
% 0.52/0.86 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.52/0.86 thf(zip_derived_cl334, plain,
% 0.52/0.86 ((![X0 : $i]: (~ (s @ sk__22) | (s @ X0)))
% 0.52/0.86 <= ((![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__22)))),
% 0.52/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl118, zip_derived_cl29])).
% 0.52/0.86 thf('85', plain,
% 0.52/0.86 (~ ( (s @ sk__22)) | ~ (![X0 : $i]: (zip_tseitin_7 @ X0 @ sk__22)) |
% 0.52/0.86 (![X1 : $i]: (s @ X1))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl334])).
% 0.52/0.86 thf(zip_derived_cl178, plain,
% 0.52/0.86 ((![X0 : $i]: (zip_tseitin_0 @ X0 @ sk__29))
% 0.52/0.86 <= ((![X0 : $i]: (zip_tseitin_0 @ X0 @ sk__29)))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl56])).
% 0.52/0.86 thf(zip_derived_cl1, plain,
% 0.52/0.86 (![X0 : $i, X1 : $i]:
% 0.52/0.86 (~ (p @ X0) | (p @ X1) | ~ (zip_tseitin_0 @ X1 @ X0))),
% 0.52/0.86 inference('cnf', [status(esa)], [zf_stmt_27])).
% 0.52/0.86 thf(zip_derived_cl386, plain,
% 0.52/0.86 ((![X0 : $i]: (~ (p @ sk__29) | (p @ X0)))
% 0.52/0.86 <= ((![X0 : $i]: (zip_tseitin_0 @ X0 @ sk__29)))),
% 0.52/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl178, zip_derived_cl1])).
% 0.52/0.86 thf('86', plain,
% 0.52/0.86 (~ ( (p @ sk__29)) | (![X1 : $i]: (p @ X1)) |
% 0.52/0.86 ~ (![X0 : $i]: (zip_tseitin_0 @ X0 @ sk__29))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl386])).
% 0.52/0.86 thf(zip_derived_cl109, plain,
% 0.52/0.86 ((![X1 : $i]: (q @ X1)) <= ((![X1 : $i]: (q @ X1)))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl33])).
% 0.52/0.86 thf(zip_derived_cl62, plain,
% 0.52/0.86 ((![X0 : $i]: ~ (q @ X0)) <= ((![X0 : $i]: ~ (q @ X0)))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.86 thf('87', plain, (~ (![X0 : $i]: ~ (q @ X0)) | ~ (![X1 : $i]: (q @ X1))),
% 0.52/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl109, zip_derived_cl62])).
% 0.52/0.86 thf('88', plain,
% 0.52/0.86 (~ ( (zip_tseitin_1)) | (![X0 : $i]: ~ (q @ X0)) |
% 0.52/0.86 (![X1 : $i]: (r @ X1))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl5])).
% 0.52/0.86 thf(zip_derived_cl55, plain,
% 0.52/0.86 (( (zip_tseitin_13) | (zip_tseitin_12) | (zip_tseitin_1))),
% 0.52/0.86 inference('cnf', [status(esa)], [zf_stmt_12])).
% 0.52/0.86 thf('89', plain,
% 0.52/0.86 (( (zip_tseitin_12)) | ( (zip_tseitin_1)) | ( (zip_tseitin_13))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl55])).
% 0.52/0.86 thf(zip_derived_cl48, plain,
% 0.52/0.86 ((~ (zip_tseitin_11) | (zip_tseitin_4) | ~ (zip_tseitin_12))),
% 0.52/0.86 inference('cnf', [status(esa)], [zf_stmt_9])).
% 0.52/0.86 thf('90', plain,
% 0.52/0.86 (~ ( (zip_tseitin_11)) | ~ ( (zip_tseitin_12)) | ( (zip_tseitin_4))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl48])).
% 0.52/0.86 thf(zip_derived_cl47, plain,
% 0.52/0.86 (![X0 : $i]:
% 0.52/0.86 ( (zip_tseitin_11)
% 0.52/0.86 | (zip_tseitin_10)
% 0.52/0.86 | (zip_tseitin_5 @ X0 @ sk__25))),
% 0.52/0.86 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.52/0.86 thf('91', plain,
% 0.52/0.86 ((![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__25)) | ( (zip_tseitin_11)) |
% 0.52/0.86 ( (zip_tseitin_10))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl47])).
% 0.52/0.86 thf(zip_derived_cl151, plain,
% 0.52/0.86 ((![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__25))
% 0.52/0.86 <= ((![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__25)))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl47])).
% 0.52/0.86 thf(zip_derived_cl21, plain,
% 0.52/0.86 (![X0 : $i, X1 : $i]:
% 0.52/0.86 (~ (r @ X0) | (r @ X1) | ~ (zip_tseitin_5 @ X1 @ X0))),
% 0.52/0.86 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.52/0.86 thf(zip_derived_cl366, plain,
% 0.52/0.86 ((![X0 : $i]: (~ (r @ sk__25) | (r @ X0)))
% 0.52/0.86 <= ((![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__25)))),
% 0.52/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl151, zip_derived_cl21])).
% 0.52/0.86 thf('92', plain,
% 0.52/0.86 (~ ( (r @ sk__25)) | ~ (![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__25)) |
% 0.52/0.86 (![X1 : $i]: (r @ X1))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl366])).
% 0.52/0.86 thf(zip_derived_cl151, plain,
% 0.52/0.86 ((![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__25))
% 0.52/0.86 <= ((![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__25)))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl47])).
% 0.52/0.86 thf(zip_derived_cl20, plain,
% 0.52/0.86 (![X0 : $i, X1 : $i]:
% 0.52/0.86 (~ (r @ X0) | (r @ X1) | ~ (zip_tseitin_5 @ X0 @ X1))),
% 0.52/0.86 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.52/0.86 thf(zip_derived_cl365, plain,
% 0.52/0.86 ((![X0 : $i]: (~ (r @ X0) | (r @ sk__25)))
% 0.52/0.86 <= ((![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__25)))),
% 0.52/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl151, zip_derived_cl20])).
% 0.52/0.86 thf('93', plain,
% 0.52/0.86 (( (r @ sk__25)) | ~ (![X0 : $i]: (zip_tseitin_5 @ X0 @ sk__25)) |
% 0.52/0.86 (![X0 : $i]: ~ (r @ X0))),
% 0.52/0.86 inference('split', [status(esa)], [zip_derived_cl365])).
% 0.52/0.86 thf(zip_derived_cl475, plain, ($false),
% 0.52/0.86 inference('sat_resolution*', [status(thm)],
% 0.52/0.86 ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9', '10', '11',
% 0.52/0.86 '12', '13', '14', '15', '16', '17', '18', '19', '20', '21',
% 0.52/0.86 '22', '23', '24', '25', '26', '27', '28', '29', '30', '31',
% 0.52/0.86 '32', '33', '34', '35', '36', '37', '38', '39', '40', '41',
% 0.52/0.86 '42', '43', '44', '45', '46', '47', '48', '49', '50', '51',
% 0.52/0.86 '52', '53', '54', '55', '56', '57', '58', '59', '60', '61',
% 0.52/0.86 '62', '63', '64', '65', '66', '67', '68', '69', '70', '71',
% 0.52/0.86 '72', '73', '74', '75', '76', '77', '78', '79', '80', '81',
% 0.52/0.86 '82', '83', '84', '85', '86', '87', '88', '89', '90', '91',
% 0.52/0.86 '92', '93'])).
% 0.52/0.86
% 0.52/0.86 % SZS output end Refutation
% 0.52/0.86
% 0.52/0.86
% 0.52/0.86 % Terminating...
% 1.52/0.96 % Runner terminated.
% 1.52/0.98 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------