%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWV384+1 : TPTP v9.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.IdtrfEk6Y9 true
% Computer : n002.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:00:58 PM UTC 2025
% Result : Theorem 0.50s 0.86s
% Output : Refutation 0.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWV384+1 : TPTP v9.2.0. Released v3.3.0.
% 0.07/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.IdtrfEk6Y9 true
% 0.11/0.35 % Computer : n002.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8042.1875MB
% 0.11/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Wed Oct 1 12:50:38 EDT 2025
% 0.11/0.35 % CPUTime :
% 0.11/0.35 % Running portfolio for 300 s
% 0.11/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.35 % Number of cores: 8
% 0.11/0.35 % Python version: Python 3.6.8
% 0.11/0.35 % Running in FO mode
% 0.47/0.65 % Total configuration time : 435
% 0.47/0.65 % Estimated wc time : 1092
% 0.47/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.48/0.74 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.48/0.74 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.48/0.74 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.48/0.74 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.48/0.74 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.48/0.75 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.48/0.75 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.50/0.80 % /export/starexec/sandbox/solver/bin/fo/fo1_lcnf.sh running for 50s
% 0.50/0.86 % Solved by fo/fo1_av.sh.
% 0.50/0.86 % done 112 iterations in 0.068s
% 0.50/0.86 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.50/0.86 % SZS output start Refutation
% 0.50/0.86 thf(succ_cpq_type, type, succ_cpq: $i > $i > $o).
% 0.50/0.86 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $i > $i > $i > $i > $o).
% 0.50/0.86 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $i > $o).
% 0.50/0.86 thf(im_succ_cpq_type, type, im_succ_cpq: $i > $i).
% 0.50/0.86 thf(sk__5_type, type, sk__5: $i).
% 0.50/0.86 thf(check_cpq_type, type, check_cpq: $i > $o).
% 0.50/0.86 thf(sk__9_type, type, sk__9: $i).
% 0.50/0.86 thf(sk__2_type, type, sk__2: $i).
% 0.50/0.86 thf(sk__type, type, sk_: $i).
% 0.50/0.86 thf(bad_type, type, bad: $i).
% 0.50/0.86 thf(sk__4_type, type, sk__4: $i).
% 0.50/0.86 thf(sk__7_type, type, sk__7: $i).
% 0.50/0.86 thf(sk__3_type, type, sk__3: $i).
% 0.50/0.86 thf(sk__11_type, type, sk__11: $i).
% 0.50/0.86 thf(ok_type, type, ok: $i > $o).
% 0.50/0.86 thf(triple_type, type, triple: $i > $i > $i > $i).
% 0.50/0.86 thf(sk__1_type, type, sk__1: $i).
% 0.50/0.86 thf(sk__6_type, type, sk__6: $i).
% 0.50/0.86 thf(sk__10_type, type, sk__10: $i).
% 0.50/0.86 thf(sk__8_type, type, sk__8: $i).
% 0.50/0.86 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > $i > $o).
% 0.50/0.86 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $i > $o).
% 0.50/0.86 thf(l20_induction, axiom,
% 0.50/0.86 (( ![U:$i,V:$i,W:$i,X:$i,Y:$i,Z:$i]:
% 0.50/0.86 ( ( succ_cpq @ ( triple @ U @ V @ W ) @ ( triple @ X @ Y @ Z ) ) =>
% 0.50/0.86 ( ( ( ~( ok @ ( triple @ X @ Y @ Z ) ) ) |
% 0.50/0.86 ( ~( check_cpq @ ( triple @ X @ Y @ Z ) ) ) ) =>
% 0.50/0.86 ( ( ~( ok @ ( im_succ_cpq @ ( triple @ X @ Y @ Z ) ) ) ) |
% 0.50/0.86 ( ~( check_cpq @ ( im_succ_cpq @ ( triple @ X @ Y @ Z ) ) ) ) ) ) ) ) =>
% 0.50/0.86 ( ![X1:$i,X2:$i,X3:$i]:
% 0.50/0.86 ( ( ( ~( ok @ ( triple @ X1 @ X2 @ X3 ) ) ) |
% 0.50/0.86 ( ~( check_cpq @ ( triple @ X1 @ X2 @ X3 ) ) ) ) =>
% 0.50/0.86 ( ![X4:$i,X5:$i,X6:$i]:
% 0.50/0.86 ( ( succ_cpq @ ( triple @ X1 @ X2 @ X3 ) @ ( triple @ X4 @ X5 @ X6 ) ) =>
% 0.50/0.86 ( ( ~( check_cpq @ ( triple @ X4 @ X5 @ X6 ) ) ) |
% 0.50/0.86 ( ~( ok @ ( triple @ X4 @ X5 @ X6 ) ) ) ) ) ) ) ))).
% 0.50/0.86 thf(zf_stmt_0, axiom,
% 0.50/0.86 (![Z:$i,Y:$i,X:$i,W:$i,V:$i,U:$i]:
% 0.50/0.86 ( ( ( succ_cpq @ ( triple @ U @ V @ W ) @ ( triple @ X @ Y @ Z ) ) =>
% 0.50/0.86 ( zip_tseitin_1 @ Z @ Y @ X ) ) =>
% 0.50/0.86 ( zip_tseitin_2 @ Z @ Y @ X @ W @ V @ U ) ))).
% 0.50/0.86 thf(zip_derived_cl54, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.50/0.86 ( (zip_tseitin_2 @ X0 @ X1 @ X2 @ X3 @ X4 @ X5)
% 0.50/0.86 | ~ (zip_tseitin_1 @ X0 @ X1 @ X2))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.50/0.86 thf(zf_stmt_1, type, zip_tseitin_3 : $i > $i > $i > $o).
% 0.50/0.86 thf(zf_stmt_2, axiom,
% 0.50/0.86 (![X3:$i,X2:$i,X1:$i]:
% 0.50/0.86 ( ( ( ~( check_cpq @ ( triple @ X1 @ X2 @ X3 ) ) ) |
% 0.50/0.86 ( ~( ok @ ( triple @ X1 @ X2 @ X3 ) ) ) ) =>
% 0.50/0.86 ( zip_tseitin_3 @ X3 @ X2 @ X1 ) ))).
% 0.50/0.86 thf(zf_stmt_3, type, zip_tseitin_2 : $i > $i > $i > $i > $i > $i > $o).
% 0.50/0.86 thf(zf_stmt_4, type, zip_tseitin_1 : $i > $i > $i > $o).
% 0.50/0.86 thf(zf_stmt_5, axiom,
% 0.50/0.86 (![Z:$i,Y:$i,X:$i]:
% 0.50/0.86 ( ( ( ( ~( check_cpq @ ( triple @ X @ Y @ Z ) ) ) |
% 0.50/0.86 ( ~( ok @ ( triple @ X @ Y @ Z ) ) ) ) =>
% 0.50/0.86 ( zip_tseitin_0 @ Z @ Y @ X ) ) =>
% 0.50/0.86 ( zip_tseitin_1 @ Z @ Y @ X ) ))).
% 0.50/0.86 thf(zf_stmt_6, type, zip_tseitin_0 : $i > $i > $i > $o).
% 0.50/0.86 thf(zf_stmt_7, axiom,
% 0.50/0.86 (![Z:$i,Y:$i,X:$i]:
% 0.50/0.86 ( ( ( ~( check_cpq @ ( im_succ_cpq @ ( triple @ X @ Y @ Z ) ) ) ) |
% 0.50/0.86 ( ~( ok @ ( im_succ_cpq @ ( triple @ X @ Y @ Z ) ) ) ) ) =>
% 0.50/0.86 ( zip_tseitin_0 @ Z @ Y @ X ) ))).
% 0.50/0.86 thf(zf_stmt_8, axiom,
% 0.50/0.86 (( ![U:$i,V:$i,W:$i,X:$i,Y:$i,Z:$i]:
% 0.50/0.86 ( zip_tseitin_2 @ Z @ Y @ X @ W @ V @ U ) ) =>
% 0.50/0.86 ( ![X1:$i,X2:$i,X3:$i]:
% 0.50/0.86 ( ( zip_tseitin_3 @ X3 @ X2 @ X1 ) =>
% 0.50/0.86 ( ![X4:$i,X5:$i,X6:$i]:
% 0.50/0.86 ( ( succ_cpq @ ( triple @ X1 @ X2 @ X3 ) @ ( triple @ X4 @ X5 @ X6 ) ) =>
% 0.50/0.86 ( ( ~( ok @ ( triple @ X4 @ X5 @ X6 ) ) ) |
% 0.50/0.86 ( ~( check_cpq @ ( triple @ X4 @ X5 @ X6 ) ) ) ) ) ) ) ))).
% 0.50/0.86 thf(zip_derived_cl58, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.50/0.86 (~ (zip_tseitin_3 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (ok @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (succ_cpq @ (triple @ X2 @ X1 @ X0) @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (zip_tseitin_2 @ sk__5 @ sk__4 @ sk__3 @ sk__2 @ sk__1 @ sk_))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.50/0.86 thf(zip_derived_cl66, plain,
% 0.50/0.86 ((~ (zip_tseitin_2 @ sk__5 @ sk__4 @ sk__3 @ sk__2 @ sk__1 @ sk_))
% 0.50/0.86 <= (~ ( (zip_tseitin_2 @ sk__5 @ sk__4 @ sk__3 @ sk__2 @ sk__1 @ sk_)))),
% 0.50/0.86 inference('split', [status(esa)], [zip_derived_cl58])).
% 0.50/0.86 thf(zip_derived_cl57, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 ( (zip_tseitin_3 @ X0 @ X1 @ X2) | (ok @ (triple @ X2 @ X1 @ X0)))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.50/0.86 thf(ax41, axiom,
% 0.50/0.86 (![U:$i,V:$i,W:$i]:
% 0.50/0.86 ( ( ~( ok @ ( triple @ U @ V @ W ) ) ) => ( ( W ) = ( bad ) ) ))).
% 0.50/0.86 thf(zip_derived_cl37, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 (((X0) = (bad)) | (ok @ (triple @ X1 @ X2 @ X0)))),
% 0.50/0.86 inference('cnf', [status(esa)], [ax41])).
% 0.50/0.86 thf(l20_co, conjecture,
% 0.50/0.86 (![U:$i,V:$i,W:$i]:
% 0.50/0.86 ( ( ( ~( check_cpq @ ( triple @ U @ V @ W ) ) ) |
% 0.50/0.86 ( ~( ok @ ( triple @ U @ V @ W ) ) ) ) =>
% 0.50/0.86 ( ![X:$i,Y:$i,Z:$i]:
% 0.50/0.86 ( ( succ_cpq @ ( triple @ U @ V @ W ) @ ( triple @ X @ Y @ Z ) ) =>
% 0.50/0.86 ( ( ~( ok @ ( triple @ X @ Y @ Z ) ) ) |
% 0.50/0.86 ( ~( check_cpq @ ( triple @ X @ Y @ Z ) ) ) ) ) ) ))).
% 0.50/0.86 thf(zf_stmt_9, negated_conjecture,
% 0.50/0.86 (~( ![U:$i,V:$i,W:$i]:
% 0.50/0.86 ( ( ( ~( check_cpq @ ( triple @ U @ V @ W ) ) ) |
% 0.50/0.86 ( ~( ok @ ( triple @ U @ V @ W ) ) ) ) =>
% 0.50/0.86 ( ![X:$i,Y:$i,Z:$i]:
% 0.50/0.86 ( ( succ_cpq @ ( triple @ U @ V @ W ) @ ( triple @ X @ Y @ Z ) ) =>
% 0.50/0.86 ( ( ~( ok @ ( triple @ X @ Y @ Z ) ) ) |
% 0.50/0.86 ( ~( check_cpq @ ( triple @ X @ Y @ Z ) ) ) ) ) ) ) )),
% 0.50/0.86 inference('cnf.neg', [status(esa)], [l20_co])).
% 0.50/0.86 thf(zip_derived_cl61, plain,
% 0.50/0.86 ((~ (check_cpq @ (triple @ sk__6 @ sk__7 @ sk__8))
% 0.50/0.86 | ~ (ok @ (triple @ sk__6 @ sk__7 @ sk__8)))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_9])).
% 0.50/0.86 thf(zip_derived_cl67, plain,
% 0.50/0.86 ((~ (ok @ (triple @ sk__6 @ sk__7 @ sk__8)))
% 0.50/0.86 <= (~ ( (ok @ (triple @ sk__6 @ sk__7 @ sk__8))))),
% 0.50/0.86 inference('split', [status(esa)], [zip_derived_cl61])).
% 0.50/0.86 thf(zip_derived_cl80, plain,
% 0.50/0.86 ((((sk__8) = (bad))) <= (~ ( (ok @ (triple @ sk__6 @ sk__7 @ sk__8))))),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl37, zip_derived_cl67])).
% 0.50/0.86 thf(zip_derived_cl64, plain,
% 0.50/0.86 ( (succ_cpq @ (triple @ sk__6 @ sk__7 @ sk__8) @
% 0.50/0.86 (triple @ sk__9 @ sk__10 @ sk__11))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_9])).
% 0.50/0.86 thf(zip_derived_cl65, plain,
% 0.50/0.86 ((![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.50/0.86 (~ (zip_tseitin_3 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (ok @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (succ_cpq @ (triple @ X2 @ X1 @ X0) @ (triple @ X3 @ X4 @ X5))))
% 0.50/0.86 <= ((![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.50/0.86 (~ (zip_tseitin_3 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (ok @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (succ_cpq @ (triple @ X2 @ X1 @ X0) @
% 0.50/0.86 (triple @ X3 @ X4 @ X5)))))),
% 0.50/0.86 inference('split', [status(esa)], [zip_derived_cl58])).
% 0.50/0.86 thf(zip_derived_cl103, plain,
% 0.50/0.86 (((~ (zip_tseitin_3 @ sk__8 @ sk__7 @ sk__6)
% 0.50/0.86 | ~ (check_cpq @ (triple @ sk__9 @ sk__10 @ sk__11))
% 0.50/0.86 | ~ (ok @ (triple @ sk__9 @ sk__10 @ sk__11))))
% 0.50/0.86 <= ((![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.50/0.86 (~ (zip_tseitin_3 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (ok @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (succ_cpq @ (triple @ X2 @ X1 @ X0) @
% 0.50/0.86 (triple @ X3 @ X4 @ X5)))))),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl64, zip_derived_cl65])).
% 0.50/0.86 thf(zip_derived_cl62, plain,
% 0.50/0.86 ( (check_cpq @ (triple @ sk__9 @ sk__10 @ sk__11))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_9])).
% 0.50/0.86 thf(zip_derived_cl63, plain, ( (ok @ (triple @ sk__9 @ sk__10 @ sk__11))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_9])).
% 0.50/0.86 thf(zip_derived_cl105, plain,
% 0.50/0.86 ((~ (zip_tseitin_3 @ sk__8 @ sk__7 @ sk__6))
% 0.50/0.86 <= ((![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.50/0.86 (~ (zip_tseitin_3 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (ok @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (succ_cpq @ (triple @ X2 @ X1 @ X0) @
% 0.50/0.86 (triple @ X3 @ X4 @ X5)))))),
% 0.50/0.86 inference('demod', [status(thm)],
% 0.50/0.86 [zip_derived_cl103, zip_derived_cl62, zip_derived_cl63])).
% 0.50/0.86 thf(zip_derived_cl106, plain,
% 0.50/0.86 ((~ (zip_tseitin_3 @ bad @ sk__7 @ sk__6))
% 0.50/0.86 <= (~ ( (ok @ (triple @ sk__6 @ sk__7 @ sk__8))) &
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.50/0.86 (~ (zip_tseitin_3 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (ok @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (succ_cpq @ (triple @ X2 @ X1 @ X0) @
% 0.50/0.86 (triple @ X3 @ X4 @ X5)))))),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl80, zip_derived_cl105])).
% 0.50/0.86 thf(zip_derived_cl125, plain,
% 0.50/0.86 (( (ok @ (triple @ sk__6 @ sk__7 @ bad)))
% 0.50/0.86 <= (~ ( (ok @ (triple @ sk__6 @ sk__7 @ sk__8))) &
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.50/0.86 (~ (zip_tseitin_3 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (ok @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (succ_cpq @ (triple @ X2 @ X1 @ X0) @
% 0.50/0.86 (triple @ X3 @ X4 @ X5)))))),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl57, zip_derived_cl106])).
% 0.50/0.86 thf(ax40, axiom, (![U:$i,V:$i]: ( ~( ok @ ( triple @ U @ V @ bad ) ) ))).
% 0.50/0.86 thf(zip_derived_cl36, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i]: ~ (ok @ (triple @ X0 @ X1 @ bad))),
% 0.50/0.86 inference('cnf', [status(esa)], [ax40])).
% 0.50/0.86 thf('0', plain,
% 0.50/0.86 (( (ok @ (triple @ sk__6 @ sk__7 @ sk__8))) |
% 0.50/0.86 ~
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.50/0.86 (~ (zip_tseitin_3 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (ok @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (succ_cpq @ (triple @ X2 @ X1 @ X0) @ (triple @ X3 @ X4 @ X5))))),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl125, zip_derived_cl36])).
% 0.50/0.86 thf(zip_derived_cl56, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 ( (zip_tseitin_3 @ X0 @ X1 @ X2)
% 0.50/0.86 | (check_cpq @ (triple @ X2 @ X1 @ X0)))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.50/0.86 thf(zip_derived_cl105, plain,
% 0.50/0.86 ((~ (zip_tseitin_3 @ sk__8 @ sk__7 @ sk__6))
% 0.50/0.86 <= ((![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.50/0.86 (~ (zip_tseitin_3 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (ok @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (succ_cpq @ (triple @ X2 @ X1 @ X0) @
% 0.50/0.86 (triple @ X3 @ X4 @ X5)))))),
% 0.50/0.86 inference('demod', [status(thm)],
% 0.50/0.86 [zip_derived_cl103, zip_derived_cl62, zip_derived_cl63])).
% 0.50/0.86 thf(zip_derived_cl116, plain,
% 0.50/0.86 (( (check_cpq @ (triple @ sk__6 @ sk__7 @ sk__8)))
% 0.50/0.86 <= ((![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.50/0.86 (~ (zip_tseitin_3 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (ok @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (succ_cpq @ (triple @ X2 @ X1 @ X0) @
% 0.50/0.86 (triple @ X3 @ X4 @ X5)))))),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl56, zip_derived_cl105])).
% 0.50/0.86 thf(zip_derived_cl68, plain,
% 0.50/0.86 ((~ (check_cpq @ (triple @ sk__6 @ sk__7 @ sk__8)))
% 0.50/0.86 <= (~ ( (check_cpq @ (triple @ sk__6 @ sk__7 @ sk__8))))),
% 0.50/0.86 inference('split', [status(esa)], [zip_derived_cl61])).
% 0.50/0.86 thf('1', plain,
% 0.50/0.86 (~
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.50/0.86 (~ (zip_tseitin_3 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (ok @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (succ_cpq @ (triple @ X2 @ X1 @ X0) @ (triple @ X3 @ X4 @ X5)))) |
% 0.50/0.86 ( (check_cpq @ (triple @ sk__6 @ sk__7 @ sk__8)))),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl116, zip_derived_cl68])).
% 0.50/0.86 thf('2', plain,
% 0.50/0.86 (~ ( (check_cpq @ (triple @ sk__6 @ sk__7 @ sk__8))) |
% 0.50/0.86 ~ ( (ok @ (triple @ sk__6 @ sk__7 @ sk__8)))),
% 0.50/0.86 inference('split', [status(esa)], [zip_derived_cl61])).
% 0.50/0.86 thf('3', plain,
% 0.50/0.86 (~ ( (zip_tseitin_2 @ sk__5 @ sk__4 @ sk__3 @ sk__2 @ sk__1 @ sk_)) |
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.50/0.86 (~ (zip_tseitin_3 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (ok @ (triple @ X3 @ X4 @ X5))
% 0.50/0.86 | ~ (succ_cpq @ (triple @ X2 @ X1 @ X0) @ (triple @ X3 @ X4 @ X5))))),
% 0.50/0.86 inference('split', [status(esa)], [zip_derived_cl58])).
% 0.50/0.86 thf('4', plain,
% 0.50/0.86 (~ ( (zip_tseitin_2 @ sk__5 @ sk__4 @ sk__3 @ sk__2 @ sk__1 @ sk_))),
% 0.50/0.86 inference('sat_resolution*', [status(thm)], ['0', '1', '2', '3'])).
% 0.50/0.86 thf(zip_derived_cl131, plain,
% 0.50/0.86 (~ (zip_tseitin_2 @ sk__5 @ sk__4 @ sk__3 @ sk__2 @ sk__1 @ sk_)),
% 0.50/0.86 inference('simpl_trail', [status(thm)], [zip_derived_cl66, '4'])).
% 0.50/0.86 thf(zip_derived_cl133, plain, (~ (zip_tseitin_1 @ sk__5 @ sk__4 @ sk__3)),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl54, zip_derived_cl131])).
% 0.50/0.86 thf(zip_derived_cl53, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 ( (zip_tseitin_1 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (triple @ X2 @ X1 @ X0))
% 0.50/0.86 | ~ (ok @ (triple @ X2 @ X1 @ X0)))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.50/0.86 thf(zip_derived_cl136, plain,
% 0.50/0.86 ((~ (check_cpq @ (triple @ sk__3 @ sk__4 @ sk__5))
% 0.50/0.86 | ~ (ok @ (triple @ sk__3 @ sk__4 @ sk__5)))),
% 0.50/0.86 inference('s_sup+', [status(thm)], [zip_derived_cl133, zip_derived_cl53])).
% 0.50/0.86 thf(zip_derived_cl140, plain,
% 0.50/0.86 ((~ (check_cpq @ (triple @ sk__3 @ sk__4 @ sk__5)))
% 0.50/0.86 <= (~ ( (check_cpq @ (triple @ sk__3 @ sk__4 @ sk__5))))),
% 0.50/0.86 inference('split', [status(esa)], [zip_derived_cl136])).
% 0.50/0.86 thf(zip_derived_cl51, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 ( (zip_tseitin_0 @ X0 @ X1 @ X2)
% 0.50/0.86 | (ok @ (im_succ_cpq @ (triple @ X2 @ X1 @ X0))))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.50/0.86 thf(l12_l13, axiom,
% 0.50/0.86 (![U:$i,V:$i,W:$i]:
% 0.50/0.86 ( ( ( ~( check_cpq @ ( triple @ U @ V @ W ) ) ) |
% 0.50/0.86 ( ~( ok @ ( triple @ U @ V @ W ) ) ) ) =>
% 0.50/0.86 ( ( ~( check_cpq @ ( im_succ_cpq @ ( triple @ U @ V @ W ) ) ) ) |
% 0.50/0.86 ( ~( ok @ ( im_succ_cpq @ ( triple @ U @ V @ W ) ) ) ) ) ))).
% 0.50/0.86 thf(zip_derived_cl59, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 (~ (ok @ (im_succ_cpq @ (triple @ X0 @ X1 @ X2)))
% 0.50/0.86 | ~ (check_cpq @ (im_succ_cpq @ (triple @ X0 @ X1 @ X2)))
% 0.50/0.86 | (ok @ (triple @ X0 @ X1 @ X2)))),
% 0.50/0.86 inference('cnf', [status(esa)], [l12_l13])).
% 0.50/0.86 thf(zip_derived_cl159, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 ( (zip_tseitin_0 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (im_succ_cpq @ (triple @ X2 @ X1 @ X0)))
% 0.50/0.86 | (ok @ (triple @ X2 @ X1 @ X0)))),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl51, zip_derived_cl59])).
% 0.50/0.86 thf(zip_derived_cl50, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 ( (zip_tseitin_0 @ X0 @ X1 @ X2)
% 0.50/0.86 | (check_cpq @ (im_succ_cpq @ (triple @ X2 @ X1 @ X0))))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.50/0.86 thf(zip_derived_cl168, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 ( (ok @ (triple @ X2 @ X1 @ X0)) | (zip_tseitin_0 @ X0 @ X1 @ X2))),
% 0.50/0.86 inference('clc', [status(thm)], [zip_derived_cl159, zip_derived_cl50])).
% 0.50/0.86 thf(zip_derived_cl139, plain,
% 0.50/0.86 ((~ (ok @ (triple @ sk__3 @ sk__4 @ sk__5)))
% 0.50/0.86 <= (~ ( (ok @ (triple @ sk__3 @ sk__4 @ sk__5))))),
% 0.50/0.86 inference('split', [status(esa)], [zip_derived_cl136])).
% 0.50/0.86 thf(zip_derived_cl37, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 (((X0) = (bad)) | (ok @ (triple @ X1 @ X2 @ X0)))),
% 0.50/0.86 inference('cnf', [status(esa)], [ax41])).
% 0.50/0.86 thf(zip_derived_cl141, plain,
% 0.50/0.86 ((((sk__5) = (bad))) <= (~ ( (ok @ (triple @ sk__3 @ sk__4 @ sk__5))))),
% 0.50/0.86 inference('s_sup+', [status(thm)], [zip_derived_cl139, zip_derived_cl37])).
% 0.50/0.86 thf(zip_derived_cl133, plain, (~ (zip_tseitin_1 @ sk__5 @ sk__4 @ sk__3)),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl54, zip_derived_cl131])).
% 0.50/0.86 thf(zip_derived_cl52, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 ( (zip_tseitin_1 @ X0 @ X1 @ X2) | ~ (zip_tseitin_0 @ X0 @ X1 @ X2))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.50/0.86 thf(zip_derived_cl135, plain, (~ (zip_tseitin_0 @ sk__5 @ sk__4 @ sk__3)),
% 0.50/0.86 inference('s_sup+', [status(thm)], [zip_derived_cl133, zip_derived_cl52])).
% 0.50/0.86 thf(zip_derived_cl146, plain,
% 0.50/0.86 ((~ (zip_tseitin_0 @ bad @ sk__4 @ sk__3))
% 0.50/0.86 <= (~ ( (ok @ (triple @ sk__3 @ sk__4 @ sk__5))))),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl141, zip_derived_cl135])).
% 0.50/0.86 thf(zip_derived_cl169, plain,
% 0.50/0.86 (( (ok @ (triple @ sk__3 @ sk__4 @ bad)))
% 0.50/0.86 <= (~ ( (ok @ (triple @ sk__3 @ sk__4 @ sk__5))))),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl168, zip_derived_cl146])).
% 0.50/0.86 thf(zip_derived_cl36, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i]: ~ (ok @ (triple @ X0 @ X1 @ bad))),
% 0.50/0.86 inference('cnf', [status(esa)], [ax40])).
% 0.50/0.86 thf('5', plain, (( (ok @ (triple @ sk__3 @ sk__4 @ sk__5)))),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl169, zip_derived_cl36])).
% 0.50/0.86 thf('6', plain,
% 0.50/0.86 (~ ( (check_cpq @ (triple @ sk__3 @ sk__4 @ sk__5))) |
% 0.50/0.86 ~ ( (ok @ (triple @ sk__3 @ sk__4 @ sk__5)))),
% 0.50/0.86 inference('split', [status(esa)], [zip_derived_cl136])).
% 0.50/0.86 thf('7', plain, (~ ( (check_cpq @ (triple @ sk__3 @ sk__4 @ sk__5)))),
% 0.50/0.86 inference('sat_resolution*', [status(thm)], ['5', '6'])).
% 0.50/0.86 thf(zip_derived_cl174, plain,
% 0.50/0.86 (~ (check_cpq @ (triple @ sk__3 @ sk__4 @ sk__5))),
% 0.50/0.86 inference('simpl_trail', [status(thm)], [zip_derived_cl140, '7'])).
% 0.50/0.86 thf(zip_derived_cl51, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 ( (zip_tseitin_0 @ X0 @ X1 @ X2)
% 0.50/0.86 | (ok @ (im_succ_cpq @ (triple @ X2 @ X1 @ X0))))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.50/0.86 thf(zip_derived_cl60, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 (~ (ok @ (im_succ_cpq @ (triple @ X0 @ X1 @ X2)))
% 0.50/0.86 | ~ (check_cpq @ (im_succ_cpq @ (triple @ X0 @ X1 @ X2)))
% 0.50/0.86 | (check_cpq @ (triple @ X0 @ X1 @ X2)))),
% 0.50/0.86 inference('cnf', [status(esa)], [l12_l13])).
% 0.50/0.86 thf(zip_derived_cl160, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 ( (zip_tseitin_0 @ X0 @ X1 @ X2)
% 0.50/0.86 | ~ (check_cpq @ (im_succ_cpq @ (triple @ X2 @ X1 @ X0)))
% 0.50/0.86 | (check_cpq @ (triple @ X2 @ X1 @ X0)))),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl51, zip_derived_cl60])).
% 0.50/0.86 thf(zip_derived_cl50, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 ( (zip_tseitin_0 @ X0 @ X1 @ X2)
% 0.50/0.86 | (check_cpq @ (im_succ_cpq @ (triple @ X2 @ X1 @ X0))))),
% 0.50/0.86 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.50/0.86 thf(zip_derived_cl176, plain,
% 0.50/0.86 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.50/0.86 ( (check_cpq @ (triple @ X2 @ X1 @ X0))
% 0.50/0.86 | (zip_tseitin_0 @ X0 @ X1 @ X2))),
% 0.50/0.86 inference('clc', [status(thm)], [zip_derived_cl160, zip_derived_cl50])).
% 0.50/0.86 thf(zip_derived_cl135, plain, (~ (zip_tseitin_0 @ sk__5 @ sk__4 @ sk__3)),
% 0.50/0.86 inference('s_sup+', [status(thm)], [zip_derived_cl133, zip_derived_cl52])).
% 0.50/0.86 thf(zip_derived_cl177, plain,
% 0.50/0.86 ( (check_cpq @ (triple @ sk__3 @ sk__4 @ sk__5))),
% 0.50/0.86 inference('s_sup-', [status(thm)], [zip_derived_cl176, zip_derived_cl135])).
% 0.50/0.86 thf(zip_derived_cl178, plain, ($false),
% 0.50/0.86 inference('demod', [status(thm)], [zip_derived_cl174, zip_derived_cl177])).
% 0.50/0.86
% 0.50/0.86 % SZS output end Refutation
% 0.50/0.86
% 0.50/0.86
% 0.50/0.86 % Terminating...
% 1.50/1.04 % Runner terminated.
% 1.50/1.06 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------