%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWV406+1 : TPTP v9.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.VdjF8Ol1Of true
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 05:01:01 PM UTC 2025
% Result : Theorem 12.12s 2.38s
% Output : Refutation 12.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV406+1 : TPTP v9.2.0. Released v3.3.0.
% 0.07/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.VdjF8Ol1Of true
% 0.13/0.34 % Computer : n009.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 1 12:42:38 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.13/0.35 % Running portfolio for 300 s
% 0.13/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.35 % Number of cores: 8
% 0.13/0.35 % Python version: Python 3.6.8
% 0.13/0.35 % Running in FO mode
% 0.61/0.69 % Total configuration time : 435
% 0.61/0.69 % Estimated wc time : 1092
% 0.61/0.69 % Estimated cpu time (7 cpus) : 156.0
% 0.61/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.61/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.61/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.61/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.61/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.61/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.61/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 12.12/2.38 % Solved by fo/fo1_av.sh.
% 12.12/2.38 % done 1304 iterations in 1.577s
% 12.12/2.38 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 12.12/2.38 % SZS output start Refutation
% 12.12/2.38 thf(strictly_less_than_type, type, strictly_less_than: $i > $i > $o).
% 12.12/2.38 thf(sk__4_type, type, sk__4: $i).
% 12.12/2.38 thf(sk__3_type, type, sk__3: $i).
% 12.12/2.38 thf(sk__type, type, sk_: $i).
% 12.12/2.38 thf(check_cpq_type, type, check_cpq: $i > $o).
% 12.12/2.38 thf(sk__8_type, type, sk__8: $i).
% 12.12/2.38 thf(pair_type, type, pair: $i > $i > $i).
% 12.12/2.38 thf(sk__2_type, type, sk__2: $i).
% 12.12/2.38 thf(less_than_type, type, less_than: $i > $i > $o).
% 12.12/2.38 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $i > $o).
% 12.12/2.38 thf(pair_in_list_type, type, pair_in_list: $i > $i > $i > $o).
% 12.12/2.38 thf(sk__7_type, type, sk__7: $i).
% 12.12/2.38 thf(triple_type, type, triple: $i > $i > $i > $i).
% 12.12/2.38 thf(sk__6_type, type, sk__6: $i).
% 12.12/2.38 thf(sk__1_type, type, sk__1: $i).
% 12.12/2.38 thf(sk__5_type, type, sk__5: $i).
% 12.12/2.38 thf(insert_slb_type, type, insert_slb: $i > $i > $i).
% 12.12/2.38 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $i > $i > $i > $o).
% 12.12/2.38 thf(ax37, axiom,
% 12.12/2.38 (![U:$i,V:$i,W:$i,X:$i,Y:$i]:
% 12.12/2.38 ( ( less_than @ Y @ X ) =>
% 12.12/2.38 ( ( check_cpq @
% 12.12/2.38 ( triple @ U @ ( insert_slb @ V @ ( pair @ X @ Y ) ) @ W ) ) <=>
% 12.12/2.38 ( check_cpq @ ( triple @ U @ V @ W ) ) ) ))).
% 12.12/2.38 thf(zip_derived_cl31, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 12.12/2.38 (~ (check_cpq @ (triple @ X0 @ X1 @ X2))
% 12.12/2.38 | (check_cpq @
% 12.12/2.38 (triple @ X0 @ (insert_slb @ X1 @ (pair @ X3 @ X4)) @ X2))
% 12.12/2.38 | ~ (less_than @ X4 @ X3))),
% 12.12/2.38 inference('cnf', [status(esa)], [ax37])).
% 12.12/2.38 thf(l42_co, conjecture,
% 12.12/2.38 (![U:$i]:
% 12.12/2.38 ( ( ![V:$i,W:$i]:
% 12.12/2.38 ( ( check_cpq @ ( triple @ V @ U @ W ) ) <=>
% 12.12/2.38 ( ![X:$i,Y:$i]:
% 12.12/2.38 ( ( pair_in_list @ U @ X @ Y ) => ( less_than @ Y @ X ) ) ) ) ) =>
% 12.12/2.38 ( ![Z:$i,X1:$i,X2:$i,X3:$i]:
% 12.12/2.38 ( ( check_cpq @
% 12.12/2.38 ( triple @ Z @ ( insert_slb @ U @ ( pair @ X2 @ X3 ) ) @ X1 ) ) <=>
% 12.12/2.38 ( ![X4:$i,X5:$i]:
% 12.12/2.38 ( ( pair_in_list @
% 12.12/2.38 ( insert_slb @ U @ ( pair @ X2 @ X3 ) ) @ X4 @ X5 ) =>
% 12.12/2.38 ( less_than @ X5 @ X4 ) ) ) ) ) ))).
% 12.12/2.38 thf(zf_stmt_0, type, zip_tseitin_1 : $i > $i > $i > $i > $i > $o).
% 12.12/2.38 thf(zf_stmt_1, axiom,
% 12.12/2.38 (![X5:$i,X4:$i,X3:$i,X2:$i,U:$i]:
% 12.12/2.38 ( ( zip_tseitin_1 @ X5 @ X4 @ X3 @ X2 @ U ) <=>
% 12.12/2.38 ( ( pair_in_list @ ( insert_slb @ U @ ( pair @ X2 @ X3 ) ) @ X4 @ X5 ) =>
% 12.12/2.38 ( less_than @ X5 @ X4 ) ) ))).
% 12.12/2.38 thf(zf_stmt_2, type, zip_tseitin_0 : $i > $i > $i > $o).
% 12.12/2.38 thf(zf_stmt_3, axiom,
% 12.12/2.38 (![Y:$i,X:$i,U:$i]:
% 12.12/2.38 ( ( zip_tseitin_0 @ Y @ X @ U ) <=>
% 12.12/2.38 ( ( pair_in_list @ U @ X @ Y ) => ( less_than @ Y @ X ) ) ))).
% 12.12/2.38 thf(zf_stmt_4, conjecture,
% 12.12/2.38 (![U:$i]:
% 12.12/2.38 ( ( ![V:$i,W:$i]:
% 12.12/2.38 ( ( check_cpq @ ( triple @ V @ U @ W ) ) <=>
% 12.12/2.38 ( ![X:$i,Y:$i]: ( zip_tseitin_0 @ Y @ X @ U ) ) ) ) =>
% 12.12/2.38 ( ![Z:$i,X1:$i,X2:$i,X3:$i]:
% 12.12/2.38 ( ( check_cpq @
% 12.12/2.38 ( triple @ Z @ ( insert_slb @ U @ ( pair @ X2 @ X3 ) ) @ X1 ) ) <=>
% 12.12/2.38 ( ![X4:$i,X5:$i]: ( zip_tseitin_1 @ X5 @ X4 @ X3 @ X2 @ U ) ) ) ) ))).
% 12.12/2.38 thf(zf_stmt_5, negated_conjecture,
% 12.12/2.38 (~( ![U:$i]:
% 12.12/2.38 ( ( ![V:$i,W:$i]:
% 12.12/2.38 ( ( check_cpq @ ( triple @ V @ U @ W ) ) <=>
% 12.12/2.38 ( ![X:$i,Y:$i]: ( zip_tseitin_0 @ Y @ X @ U ) ) ) ) =>
% 12.12/2.38 ( ![Z:$i,X1:$i,X2:$i,X3:$i]:
% 12.12/2.38 ( ( check_cpq @
% 12.12/2.38 ( triple @ Z @ ( insert_slb @ U @ ( pair @ X2 @ X3 ) ) @ X1 ) ) <=>
% 12.12/2.38 ( ![X4:$i,X5:$i]: ( zip_tseitin_1 @ X5 @ X4 @ X3 @ X2 @ U ) ) ) ) ) )),
% 12.12/2.38 inference('cnf.neg', [status(esa)], [zf_stmt_4])).
% 12.12/2.38 thf(zip_derived_cl58, plain,
% 12.12/2.38 ((~ (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_)
% 12.12/2.38 | ~ (check_cpq @
% 12.12/2.38 (triple @ sk__1 @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @
% 12.12/2.38 sk__2)))),
% 12.12/2.38 inference('cnf', [status(esa)], [zf_stmt_5])).
% 12.12/2.38 thf(zip_derived_cl64, plain,
% 12.12/2.38 ((~ (check_cpq @
% 12.12/2.38 (triple @ sk__1 @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @
% 12.12/2.38 sk__2)))
% 12.12/2.38 <= (~
% 12.12/2.38 ( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl58])).
% 12.12/2.38 thf(zip_derived_cl1084, plain,
% 12.12/2.38 (((~ (less_than @ sk__4 @ sk__3)
% 12.12/2.38 | ~ (check_cpq @ (triple @ sk__1 @ sk_ @ sk__2))))
% 12.12/2.38 <= (~
% 12.12/2.38 ( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl31, zip_derived_cl64])).
% 12.12/2.38 thf(zip_derived_cl1089, plain,
% 12.12/2.38 ((~ (less_than @ sk__4 @ sk__3)) <= (~ ( (less_than @ sk__4 @ sk__3)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl1084])).
% 12.12/2.38 thf(stricly_smaller_definition, axiom,
% 12.12/2.38 (![U:$i,V:$i]:
% 12.12/2.38 ( ( strictly_less_than @ U @ V ) <=>
% 12.12/2.38 ( ( less_than @ U @ V ) & ( ~( less_than @ V @ U ) ) ) ))).
% 12.12/2.38 thf(zip_derived_cl5, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i]:
% 12.12/2.38 ( (strictly_less_than @ X0 @ X1)
% 12.12/2.38 | (less_than @ X1 @ X0)
% 12.12/2.38 | ~ (less_than @ X0 @ X1))),
% 12.12/2.38 inference('cnf', [status(esa)], [stricly_smaller_definition])).
% 12.12/2.38 thf(totality, axiom,
% 12.12/2.38 (![U:$i,V:$i]: ( ( less_than @ V @ U ) | ( less_than @ U @ V ) ))).
% 12.12/2.38 thf(zip_derived_cl1, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i]: ( (less_than @ X0 @ X1) | (less_than @ X1 @ X0))),
% 12.12/2.38 inference('cnf', [status(esa)], [totality])).
% 12.12/2.38 thf(zip_derived_cl96, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i]:
% 12.12/2.38 ( (less_than @ X1 @ X0) | (strictly_less_than @ X0 @ X1))),
% 12.12/2.38 inference('clc', [status(thm)], [zip_derived_cl5, zip_derived_cl1])).
% 12.12/2.38 thf(zip_derived_cl59, plain,
% 12.12/2.38 (![X5 : $i, X6 : $i]:
% 12.12/2.38 ( (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_)
% 12.12/2.38 | (check_cpq @
% 12.12/2.38 (triple @ sk__1 @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @
% 12.12/2.38 sk__2)))),
% 12.12/2.38 inference('cnf', [status(esa)], [zf_stmt_5])).
% 12.12/2.38 thf(zip_derived_cl67, plain,
% 12.12/2.38 (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2)))
% 12.12/2.38 <= (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl59])).
% 12.12/2.38 thf(ax38, axiom,
% 12.12/2.38 (![U:$i,V:$i,W:$i,X:$i,Y:$i]:
% 12.12/2.38 ( ( strictly_less_than @ X @ Y ) =>
% 12.12/2.38 ( ~( check_cpq @
% 12.12/2.38 ( triple @ U @ ( insert_slb @ V @ ( pair @ X @ Y ) ) @ W ) ) ) ))).
% 12.12/2.38 thf(zip_derived_cl33, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 12.12/2.38 (~ (check_cpq @
% 12.12/2.38 (triple @ X0 @ (insert_slb @ X1 @ (pair @ X2 @ X3)) @ X4))
% 12.12/2.38 | ~ (strictly_less_than @ X2 @ X3))),
% 12.12/2.38 inference('cnf', [status(esa)], [ax38])).
% 12.12/2.38 thf(zip_derived_cl82, plain,
% 12.12/2.38 ((~ (strictly_less_than @ sk__3 @ sk__4))
% 12.12/2.38 <= (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl67, zip_derived_cl33])).
% 12.12/2.38 thf(zip_derived_cl99, plain,
% 12.12/2.38 (( (less_than @ sk__4 @ sk__3))
% 12.12/2.38 <= (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl96, zip_derived_cl82])).
% 12.12/2.38 thf('0', plain,
% 12.12/2.38 (~
% 12.12/2.38 ( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))) |
% 12.12/2.38 ( (less_than @ sk__4 @ sk__3))),
% 12.12/2.38 inference('s_sup+', [status(thm)], [zip_derived_cl1089, zip_derived_cl99])).
% 12.12/2.38 thf(zip_derived_cl55, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 12.12/2.38 ( (zip_tseitin_1 @ X0 @ X1 @ X2 @ X3 @ X4)
% 12.12/2.38 | (pair_in_list @ (insert_slb @ X4 @ (pair @ X3 @ X2)) @ X1 @ X0))),
% 12.12/2.38 inference('cnf', [status(esa)], [zf_stmt_1])).
% 12.12/2.38 thf(zip_derived_cl65, plain,
% 12.12/2.38 ((~ (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_))
% 12.12/2.38 <= (~ ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl58])).
% 12.12/2.38 thf(zip_derived_cl3190, plain,
% 12.12/2.38 (( (pair_in_list @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__5 @
% 12.12/2.38 sk__6))
% 12.12/2.38 <= (~ ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl55, zip_derived_cl65])).
% 12.12/2.38 thf(ax23, axiom,
% 12.12/2.38 (![U:$i,V:$i,W:$i,X:$i,Y:$i]:
% 12.12/2.38 ( ( pair_in_list @ ( insert_slb @ U @ ( pair @ V @ X ) ) @ W @ Y ) <=>
% 12.12/2.38 ( ( pair_in_list @ U @ W @ Y ) |
% 12.12/2.38 ( ( ( V ) = ( W ) ) & ( ( X ) = ( Y ) ) ) ) ))).
% 12.12/2.38 thf(zip_derived_cl15, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 12.12/2.38 (((X1) = (X0))
% 12.12/2.38 | (pair_in_list @ X2 @ X3 @ X0)
% 12.12/2.38 | ~ (pair_in_list @ (insert_slb @ X2 @ (pair @ X4 @ X1)) @ X3 @ X0))),
% 12.12/2.38 inference('cnf', [status(esa)], [ax23])).
% 12.12/2.38 thf(zip_derived_cl11380, plain,
% 12.12/2.38 (((((sk__4) = (sk__6)) | (pair_in_list @ sk_ @ sk__5 @ sk__6)))
% 12.12/2.38 <= (~ ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl3190, zip_derived_cl15])).
% 12.12/2.38 thf('1', plain,
% 12.12/2.38 ((((sk__4) = (sk__6))) | ( (pair_in_list @ sk_ @ sk__5 @ sk__6)) |
% 12.12/2.38 ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl11380])).
% 12.12/2.38 thf(zip_derived_cl3190, plain,
% 12.12/2.38 (( (pair_in_list @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__5 @
% 12.12/2.38 sk__6))
% 12.12/2.38 <= (~ ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl55, zip_derived_cl65])).
% 12.12/2.38 thf(zip_derived_cl14, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 12.12/2.38 (((X1) = (X0))
% 12.12/2.38 | (pair_in_list @ X2 @ X0 @ X3)
% 12.12/2.38 | ~ (pair_in_list @ (insert_slb @ X2 @ (pair @ X1 @ X4)) @ X0 @ X3))),
% 12.12/2.38 inference('cnf', [status(esa)], [ax23])).
% 12.12/2.38 thf(zip_derived_cl11379, plain,
% 12.12/2.38 (((((sk__3) = (sk__5)) | (pair_in_list @ sk_ @ sk__5 @ sk__6)))
% 12.12/2.38 <= (~ ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl3190, zip_derived_cl14])).
% 12.12/2.38 thf('2', plain,
% 12.12/2.38 ((((sk__3) = (sk__5))) | ( (pair_in_list @ sk_ @ sk__5 @ sk__6)) |
% 12.12/2.38 ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl11379])).
% 12.12/2.38 thf(zip_derived_cl11382, plain,
% 12.12/2.38 (( (pair_in_list @ sk_ @ sk__5 @ sk__6))
% 12.12/2.38 <= (( (pair_in_list @ sk_ @ sk__5 @ sk__6)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl11379])).
% 12.12/2.38 thf(zip_derived_cl57, plain,
% 12.12/2.38 (![X0 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 12.12/2.38 ( (zip_tseitin_0 @ X2 @ X3 @ sk_)
% 12.12/2.38 | ~ (check_cpq @ (triple @ X0 @ sk_ @ X4)))),
% 12.12/2.38 inference('cnf', [status(esa)], [zf_stmt_5])).
% 12.12/2.38 thf(zip_derived_cl62, plain,
% 12.12/2.38 ((![X2 : $i, X3 : $i]: (zip_tseitin_0 @ X2 @ X3 @ sk_))
% 12.12/2.38 <= ((![X2 : $i, X3 : $i]: (zip_tseitin_0 @ X2 @ X3 @ sk_)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl57])).
% 12.12/2.38 thf(zip_derived_cl50, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i]:
% 12.12/2.38 (~ (pair_in_list @ X0 @ X1 @ X2)
% 12.12/2.38 | (less_than @ X2 @ X1)
% 12.12/2.38 | ~ (zip_tseitin_0 @ X2 @ X1 @ X0))),
% 12.12/2.38 inference('cnf', [status(esa)], [zf_stmt_3])).
% 12.12/2.38 thf(zip_derived_cl2790, plain,
% 12.12/2.38 ((![X0 : $i, X1 : $i]:
% 12.12/2.38 (~ (pair_in_list @ sk_ @ X0 @ X1) | (less_than @ X1 @ X0)))
% 12.12/2.38 <= ((![X2 : $i, X3 : $i]: (zip_tseitin_0 @ X2 @ X3 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl62, zip_derived_cl50])).
% 12.12/2.38 thf(zip_derived_cl11385, plain,
% 12.12/2.38 (( (less_than @ sk__6 @ sk__5))
% 12.12/2.38 <= ((![X2 : $i, X3 : $i]: (zip_tseitin_0 @ X2 @ X3 @ sk_)) &
% 12.12/2.38 ( (pair_in_list @ sk_ @ sk__5 @ sk__6)))),
% 12.12/2.38 inference('s_sup-', [status(thm)],
% 12.12/2.38 [zip_derived_cl11382, zip_derived_cl2790])).
% 12.12/2.38 thf(zip_derived_cl54, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 12.12/2.38 ( (zip_tseitin_1 @ X0 @ X1 @ X2 @ X3 @ X4) | ~ (less_than @ X0 @ X1))),
% 12.12/2.38 inference('cnf', [status(esa)], [zf_stmt_1])).
% 12.12/2.38 thf(zip_derived_cl65, plain,
% 12.12/2.38 ((~ (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_))
% 12.12/2.38 <= (~ ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl58])).
% 12.12/2.38 thf(zip_derived_cl3123, plain,
% 12.12/2.38 ((~ (less_than @ sk__6 @ sk__5))
% 12.12/2.38 <= (~ ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl54, zip_derived_cl65])).
% 12.12/2.38 thf('3', plain,
% 12.12/2.38 (~ ( (pair_in_list @ sk_ @ sk__5 @ sk__6)) |
% 12.12/2.38 ~ (![X2 : $i, X3 : $i]: (zip_tseitin_0 @ X2 @ X3 @ sk_)) |
% 12.12/2.38 ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_))),
% 12.12/2.38 inference('s_sup-', [status(thm)],
% 12.12/2.38 [zip_derived_cl11385, zip_derived_cl3123])).
% 12.12/2.38 thf('4', plain,
% 12.12/2.38 ((![X2 : $i, X3 : $i]: (zip_tseitin_0 @ X2 @ X3 @ sk_)) |
% 12.12/2.38 (![X0 : $i, X4 : $i]: ~ (check_cpq @ (triple @ X0 @ sk_ @ X4)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl57])).
% 12.12/2.38 thf(zip_derived_cl67, plain,
% 12.12/2.38 (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2)))
% 12.12/2.38 <= (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl59])).
% 12.12/2.38 thf(zip_derived_cl32, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 12.12/2.38 (~ (check_cpq @
% 12.12/2.38 (triple @ X0 @ (insert_slb @ X1 @ (pair @ X2 @ X3)) @ X4))
% 12.12/2.38 | (check_cpq @ (triple @ X0 @ X1 @ X4))
% 12.12/2.38 | ~ (less_than @ X3 @ X2))),
% 12.12/2.38 inference('cnf', [status(esa)], [ax37])).
% 12.12/2.38 thf(zip_derived_cl1158, plain,
% 12.12/2.38 ((( (check_cpq @ (triple @ sk__1 @ sk_ @ sk__2))
% 12.12/2.38 | ~ (less_than @ sk__4 @ sk__3)))
% 12.12/2.38 <= (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl67, zip_derived_cl32])).
% 12.12/2.38 thf(zip_derived_cl99, plain,
% 12.12/2.38 (( (less_than @ sk__4 @ sk__3))
% 12.12/2.38 <= (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl96, zip_derived_cl82])).
% 12.12/2.38 thf(zip_derived_cl1161, plain,
% 12.12/2.38 (( (check_cpq @ (triple @ sk__1 @ sk_ @ sk__2)))
% 12.12/2.38 <= (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('demod', [status(thm)], [zip_derived_cl1158, zip_derived_cl99])).
% 12.12/2.38 thf(zip_derived_cl63, plain,
% 12.12/2.38 ((![X0 : $i, X4 : $i]: ~ (check_cpq @ (triple @ X0 @ sk_ @ X4)))
% 12.12/2.38 <= ((![X0 : $i, X4 : $i]: ~ (check_cpq @ (triple @ X0 @ sk_ @ X4))))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl57])).
% 12.12/2.38 thf('5', plain,
% 12.12/2.38 (~ (![X0 : $i, X4 : $i]: ~ (check_cpq @ (triple @ X0 @ sk_ @ X4))) |
% 12.12/2.38 ~
% 12.12/2.38 ( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl1161, zip_derived_cl63])).
% 12.12/2.38 thf('6', plain,
% 12.12/2.38 (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))) |
% 12.12/2.38 ~ ( (check_cpq @ (triple @ sk__1 @ sk_ @ sk__2))) |
% 12.12/2.38 ~ ( (less_than @ sk__4 @ sk__3))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl1084])).
% 12.12/2.38 thf(zip_derived_cl56, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i]:
% 12.12/2.38 ( (check_cpq @ (triple @ X0 @ sk_ @ X1))
% 12.12/2.38 | ~ (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_))),
% 12.12/2.38 inference('cnf', [status(esa)], [zf_stmt_5])).
% 12.12/2.38 thf('7', plain,
% 12.12/2.38 ((![X0 : $i, X1 : $i]: (check_cpq @ (triple @ X0 @ sk_ @ X1))) |
% 12.12/2.38 ~ ( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl56])).
% 12.12/2.38 thf('8', plain,
% 12.12/2.38 (~ ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_)) |
% 12.12/2.38 ~
% 12.12/2.38 ( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl58])).
% 12.12/2.38 thf(zip_derived_cl66, plain,
% 12.12/2.38 ((![X5 : $i, X6 : $i]: (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_))
% 12.12/2.38 <= ((![X5 : $i, X6 : $i]:
% 12.12/2.38 (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl59])).
% 12.12/2.38 thf(zip_derived_cl53, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 12.12/2.38 (~ (pair_in_list @ (insert_slb @ X0 @ (pair @ X1 @ X2)) @ X3 @ X4)
% 12.12/2.38 | (less_than @ X4 @ X3)
% 12.12/2.38 | ~ (zip_tseitin_1 @ X4 @ X3 @ X2 @ X1 @ X0))),
% 12.12/2.38 inference('cnf', [status(esa)], [zf_stmt_1])).
% 12.12/2.38 thf(zip_derived_cl2985, plain,
% 12.12/2.38 ((![X0 : $i, X1 : $i]:
% 12.12/2.38 (~ (pair_in_list @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @
% 12.12/2.38 X0 @ X1)
% 12.12/2.38 | (less_than @ X1 @ X0)))
% 12.12/2.38 <= ((![X5 : $i, X6 : $i]:
% 12.12/2.38 (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl66, zip_derived_cl53])).
% 12.12/2.38 thf(zip_derived_cl16, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 12.12/2.38 ( (pair_in_list @ (insert_slb @ X0 @ (pair @ X1 @ X2)) @ X3 @ X4)
% 12.12/2.38 | ~ (pair_in_list @ X0 @ X3 @ X4))),
% 12.12/2.38 inference('cnf', [status(esa)], [ax23])).
% 12.12/2.38 thf(zip_derived_cl2990, plain,
% 12.12/2.38 ((![X0 : $i, X1 : $i]:
% 12.12/2.38 ( (less_than @ X0 @ X1) | ~ (pair_in_list @ sk_ @ X1 @ X0)))
% 12.12/2.38 <= ((![X5 : $i, X6 : $i]:
% 12.12/2.38 (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('s_sup+', [status(thm)], [zip_derived_cl2985, zip_derived_cl16])).
% 12.12/2.38 thf(zip_derived_cl52, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i]:
% 12.12/2.38 ( (zip_tseitin_0 @ X0 @ X1 @ X2) | (pair_in_list @ X2 @ X1 @ X0))),
% 12.12/2.38 inference('cnf', [status(esa)], [zf_stmt_3])).
% 12.12/2.38 thf(zip_derived_cl61, plain,
% 12.12/2.38 ((~ (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_))
% 12.12/2.38 <= (~ ( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl56])).
% 12.12/2.38 thf(zip_derived_cl2938, plain,
% 12.12/2.38 (( (pair_in_list @ sk_ @ sk__7 @ sk__8))
% 12.12/2.38 <= (~ ( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl52, zip_derived_cl61])).
% 12.12/2.38 thf(zip_derived_cl2994, plain,
% 12.12/2.38 (( (less_than @ sk__8 @ sk__7))
% 12.12/2.38 <= (~ ( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_)) &
% 12.12/2.38 (![X5 : $i, X6 : $i]:
% 12.12/2.38 (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('s_sup+', [status(thm)],
% 12.12/2.38 [zip_derived_cl2990, zip_derived_cl2938])).
% 12.12/2.38 thf(zip_derived_cl51, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i]:
% 12.12/2.38 ( (zip_tseitin_0 @ X0 @ X1 @ X2) | ~ (less_than @ X0 @ X1))),
% 12.12/2.38 inference('cnf', [status(esa)], [zf_stmt_3])).
% 12.12/2.38 thf(zip_derived_cl61, plain,
% 12.12/2.38 ((~ (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_))
% 12.12/2.38 <= (~ ( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl56])).
% 12.12/2.38 thf(zip_derived_cl83, plain,
% 12.12/2.38 ((~ (less_than @ sk__8 @ sk__7))
% 12.12/2.38 <= (~ ( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl51, zip_derived_cl61])).
% 12.12/2.38 thf('9', plain,
% 12.12/2.38 (( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_)) |
% 12.12/2.38 ~
% 12.12/2.38 (![X5 : $i, X6 : $i]: (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl2994, zip_derived_cl83])).
% 12.12/2.38 thf(zip_derived_cl66, plain,
% 12.12/2.38 ((![X5 : $i, X6 : $i]: (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_))
% 12.12/2.38 <= ((![X5 : $i, X6 : $i]:
% 12.12/2.38 (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl59])).
% 12.12/2.38 thf(zip_derived_cl65, plain,
% 12.12/2.38 ((~ (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_))
% 12.12/2.38 <= (~ ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl58])).
% 12.12/2.38 thf('10', plain,
% 12.12/2.38 (~
% 12.12/2.38 (![X5 : $i, X6 : $i]: (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_)) |
% 12.12/2.38 ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl66, zip_derived_cl65])).
% 12.12/2.38 thf(zip_derived_cl1088, plain,
% 12.12/2.38 ((~ (check_cpq @ (triple @ sk__1 @ sk_ @ sk__2)))
% 12.12/2.38 <= (~ ( (check_cpq @ (triple @ sk__1 @ sk_ @ sk__2))))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl1084])).
% 12.12/2.38 thf(zip_derived_cl60, plain,
% 12.12/2.38 ((![X0 : $i, X1 : $i]: (check_cpq @ (triple @ X0 @ sk_ @ X1)))
% 12.12/2.38 <= ((![X0 : $i, X1 : $i]: (check_cpq @ (triple @ X0 @ sk_ @ X1))))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl56])).
% 12.12/2.38 thf('11', plain,
% 12.12/2.38 (( (check_cpq @ (triple @ sk__1 @ sk_ @ sk__2))) |
% 12.12/2.38 ~ (![X0 : $i, X1 : $i]: (check_cpq @ (triple @ X0 @ sk_ @ X1)))),
% 12.12/2.38 inference('s_sup+', [status(thm)], [zip_derived_cl1088, zip_derived_cl60])).
% 12.12/2.38 thf(zip_derived_cl11468, plain,
% 12.12/2.38 ((((sk__4) = (sk__6))) <= ((((sk__4) = (sk__6))))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl11380])).
% 12.12/2.38 thf(zip_derived_cl11383, plain,
% 12.12/2.38 ((((sk__3) = (sk__5))) <= ((((sk__3) = (sk__5))))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl11379])).
% 12.12/2.38 thf(zip_derived_cl3123, plain,
% 12.12/2.38 ((~ (less_than @ sk__6 @ sk__5))
% 12.12/2.38 <= (~ ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl54, zip_derived_cl65])).
% 12.12/2.38 thf(zip_derived_cl11387, plain,
% 12.12/2.38 ((~ (less_than @ sk__6 @ sk__3))
% 12.12/2.38 <= (~ ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_)) &
% 12.12/2.38 (((sk__3) = (sk__5))))),
% 12.12/2.38 inference('s_sup-', [status(thm)],
% 12.12/2.38 [zip_derived_cl11383, zip_derived_cl3123])).
% 12.12/2.38 thf(zip_derived_cl11488, plain,
% 12.12/2.38 ((~ (less_than @ sk__4 @ sk__3))
% 12.12/2.38 <= (~ ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_)) &
% 12.12/2.38 (((sk__4) = (sk__6))) &
% 12.12/2.38 (((sk__3) = (sk__5))))),
% 12.12/2.38 inference('s_sup-', [status(thm)],
% 12.12/2.38 [zip_derived_cl11468, zip_derived_cl11387])).
% 12.12/2.38 thf(zip_derived_cl83, plain,
% 12.12/2.38 ((~ (less_than @ sk__8 @ sk__7))
% 12.12/2.38 <= (~ ( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl51, zip_derived_cl61])).
% 12.12/2.38 thf(zip_derived_cl1, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i]: ( (less_than @ X0 @ X1) | (less_than @ X1 @ X0))),
% 12.12/2.38 inference('cnf', [status(esa)], [totality])).
% 12.12/2.38 thf(zip_derived_cl85, plain,
% 12.12/2.38 (( (less_than @ sk__7 @ sk__8))
% 12.12/2.38 <= (~ ( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_)))),
% 12.12/2.38 inference('s_sup+', [status(thm)], [zip_derived_cl83, zip_derived_cl1])).
% 12.12/2.38 thf(transitivity, axiom,
% 12.12/2.38 (![U:$i,V:$i,W:$i]:
% 12.12/2.38 ( ( ( less_than @ U @ V ) & ( less_than @ V @ W ) ) =>
% 12.12/2.38 ( less_than @ U @ W ) ))).
% 12.12/2.38 thf(zip_derived_cl0, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i]:
% 12.12/2.38 (~ (less_than @ X0 @ X1)
% 12.12/2.38 | ~ (less_than @ X1 @ X2)
% 12.12/2.38 | (less_than @ X0 @ X2))),
% 12.12/2.38 inference('cnf', [status(esa)], [transitivity])).
% 12.12/2.38 thf(zip_derived_cl89, plain,
% 12.12/2.38 ((![X0 : $i]: (~ (less_than @ sk__8 @ X0) | (less_than @ sk__7 @ X0)))
% 12.12/2.38 <= (~ ( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl85, zip_derived_cl0])).
% 12.12/2.38 thf(zip_derived_cl1, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i]: ( (less_than @ X0 @ X1) | (less_than @ X1 @ X0))),
% 12.12/2.38 inference('cnf', [status(esa)], [totality])).
% 12.12/2.38 thf(zip_derived_cl90, plain,
% 12.12/2.38 ((![X0 : $i]: ( (less_than @ sk__7 @ X0) | (less_than @ X0 @ sk__8)))
% 12.12/2.38 <= (~ ( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_)))),
% 12.12/2.38 inference('s_sup+', [status(thm)], [zip_derived_cl89, zip_derived_cl1])).
% 12.12/2.38 thf(zip_derived_cl1, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i]: ( (less_than @ X0 @ X1) | (less_than @ X1 @ X0))),
% 12.12/2.38 inference('cnf', [status(esa)], [totality])).
% 12.12/2.38 thf(zip_derived_cl99, plain,
% 12.12/2.38 (( (less_than @ sk__4 @ sk__3))
% 12.12/2.38 <= (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl96, zip_derived_cl82])).
% 12.12/2.38 thf(zip_derived_cl0, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i]:
% 12.12/2.38 (~ (less_than @ X0 @ X1)
% 12.12/2.38 | ~ (less_than @ X1 @ X2)
% 12.12/2.38 | (less_than @ X0 @ X2))),
% 12.12/2.38 inference('cnf', [status(esa)], [transitivity])).
% 12.12/2.38 thf(zip_derived_cl100, plain,
% 12.12/2.38 ((![X0 : $i]: (~ (less_than @ sk__3 @ X0) | (less_than @ sk__4 @ X0)))
% 12.12/2.38 <= (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl99, zip_derived_cl0])).
% 12.12/2.38 thf(zip_derived_cl0, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i]:
% 12.12/2.38 (~ (less_than @ X0 @ X1)
% 12.12/2.38 | ~ (less_than @ X1 @ X2)
% 12.12/2.38 | (less_than @ X0 @ X2))),
% 12.12/2.38 inference('cnf', [status(esa)], [transitivity])).
% 12.12/2.38 thf(zip_derived_cl101, plain,
% 12.12/2.38 ((![X0 : $i, X1 : $i]:
% 12.12/2.38 (~ (less_than @ sk__3 @ X0)
% 12.12/2.38 | ~ (less_than @ X0 @ X1)
% 12.12/2.38 | (less_than @ sk__4 @ X1)))
% 12.12/2.38 <= (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl100, zip_derived_cl0])).
% 12.12/2.38 thf(zip_derived_cl102, plain,
% 12.12/2.38 ((![X0 : $i, X1 : $i]:
% 12.12/2.38 ( (less_than @ X0 @ sk__3)
% 12.12/2.38 | ~ (less_than @ X0 @ X1)
% 12.12/2.38 | (less_than @ sk__4 @ X1)))
% 12.12/2.38 <= (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl101])).
% 12.12/2.38 thf(zip_derived_cl117, plain,
% 12.12/2.38 ((![X0 : $i]:
% 12.12/2.38 ( (less_than @ sk__7 @ X0)
% 12.12/2.38 | (less_than @ X0 @ sk__3)
% 12.12/2.38 | (less_than @ sk__4 @ sk__8)))
% 12.12/2.38 <= (~ ( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_)) &
% 12.12/2.38 ( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl90, zip_derived_cl102])).
% 12.12/2.38 thf(zip_derived_cl156, plain,
% 12.12/2.38 ((![X0 : $i]: ( (less_than @ sk__7 @ X0) | (less_than @ X0 @ sk__3)))
% 12.12/2.38 <= ((![X0 : $i]:
% 12.12/2.38 ( (less_than @ sk__7 @ X0) | (less_than @ X0 @ sk__3))))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl117])).
% 12.12/2.38 thf(zip_derived_cl85, plain,
% 12.12/2.38 (( (less_than @ sk__7 @ sk__8))
% 12.12/2.38 <= (~ ( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_)))),
% 12.12/2.38 inference('s_sup+', [status(thm)], [zip_derived_cl83, zip_derived_cl1])).
% 12.12/2.38 thf(zip_derived_cl102, plain,
% 12.12/2.38 ((![X0 : $i, X1 : $i]:
% 12.12/2.38 ( (less_than @ X0 @ sk__3)
% 12.12/2.38 | ~ (less_than @ X0 @ X1)
% 12.12/2.38 | (less_than @ sk__4 @ X1)))
% 12.12/2.38 <= (( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl101])).
% 12.12/2.38 thf(zip_derived_cl122, plain,
% 12.12/2.38 ((( (less_than @ sk__7 @ sk__3) | (less_than @ sk__4 @ sk__8)))
% 12.12/2.38 <= (~ ( (zip_tseitin_0 @ sk__8 @ sk__7 @ sk_)) &
% 12.12/2.38 ( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @
% 12.12/2.38 (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2))))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl85, zip_derived_cl102])).
% 12.12/2.38 thf(zip_derived_cl140, plain,
% 12.12/2.38 (( (less_than @ sk__4 @ sk__8)) <= (( (less_than @ sk__4 @ sk__8)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl122])).
% 12.12/2.38 thf(zip_derived_cl0, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i]:
% 12.12/2.38 (~ (less_than @ X0 @ X1)
% 12.12/2.38 | ~ (less_than @ X1 @ X2)
% 12.12/2.38 | (less_than @ X0 @ X2))),
% 12.12/2.38 inference('cnf', [status(esa)], [transitivity])).
% 12.12/2.38 thf(zip_derived_cl142, plain,
% 12.12/2.38 ((![X0 : $i]: (~ (less_than @ sk__8 @ X0) | (less_than @ sk__4 @ X0)))
% 12.12/2.38 <= (( (less_than @ sk__4 @ sk__8)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl140, zip_derived_cl0])).
% 12.12/2.38 thf(zip_derived_cl175, plain,
% 12.12/2.38 ((( (less_than @ sk__7 @ sk__8) | (less_than @ sk__4 @ sk__3)))
% 12.12/2.38 <= (( (less_than @ sk__4 @ sk__8)) &
% 12.12/2.38 (![X0 : $i]:
% 12.12/2.38 ( (less_than @ sk__7 @ X0) | (less_than @ X0 @ sk__3))))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl156, zip_derived_cl142])).
% 12.12/2.38 thf(zip_derived_cl183, plain,
% 12.12/2.38 (( (less_than @ sk__4 @ sk__3)) <= (( (less_than @ sk__4 @ sk__3)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl175])).
% 12.12/2.38 thf('12', plain,
% 12.12/2.38 (~ (((sk__4) = (sk__6))) | ~ (((sk__3) = (sk__5))) |
% 12.12/2.38 ~ ( (less_than @ sk__4 @ sk__3)) |
% 12.12/2.38 ( (zip_tseitin_1 @ sk__6 @ sk__5 @ sk__4 @ sk__3 @ sk_))),
% 12.12/2.38 inference('s_sup+', [status(thm)],
% 12.12/2.38 [zip_derived_cl11488, zip_derived_cl183])).
% 12.12/2.38 thf(zip_derived_cl2985, plain,
% 12.12/2.38 ((![X0 : $i, X1 : $i]:
% 12.12/2.38 (~ (pair_in_list @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @
% 12.12/2.38 X0 @ X1)
% 12.12/2.38 | (less_than @ X1 @ X0)))
% 12.12/2.38 <= ((![X5 : $i, X6 : $i]:
% 12.12/2.38 (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)], [zip_derived_cl66, zip_derived_cl53])).
% 12.12/2.38 thf(zip_derived_cl17, plain,
% 12.12/2.38 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 12.12/2.38 ( (pair_in_list @ (insert_slb @ X0 @ (pair @ X1 @ X2)) @ X3 @ X4)
% 12.12/2.38 | ((X1) != (X3))
% 12.12/2.38 | ((X2) != (X4)))),
% 12.12/2.38 inference('cnf', [status(esa)], [ax23])).
% 12.12/2.38 thf(zip_derived_cl2991, plain,
% 12.12/2.38 ((![X0 : $i, X1 : $i]:
% 12.12/2.38 ( (less_than @ X0 @ X1) | ((sk__3) != (X1)) | ((sk__4) != (X0))))
% 12.12/2.38 <= ((![X5 : $i, X6 : $i]:
% 12.12/2.38 (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('s_sup+', [status(thm)], [zip_derived_cl2985, zip_derived_cl17])).
% 12.12/2.38 thf(zip_derived_cl1089, plain,
% 12.12/2.38 ((~ (less_than @ sk__4 @ sk__3)) <= (~ ( (less_than @ sk__4 @ sk__3)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl1084])).
% 12.12/2.38 thf(zip_derived_cl3035, plain,
% 12.12/2.38 (((((sk__4) != (sk__4)) | ((sk__3) != (sk__3))))
% 12.12/2.38 <= (~ ( (less_than @ sk__4 @ sk__3)) &
% 12.12/2.38 (![X5 : $i, X6 : $i]:
% 12.12/2.38 (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_)))),
% 12.12/2.38 inference('s_sup-', [status(thm)],
% 12.12/2.38 [zip_derived_cl2991, zip_derived_cl1089])).
% 12.12/2.38 thf('13', plain,
% 12.12/2.38 (~
% 12.12/2.38 (![X5 : $i, X6 : $i]: (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_)) |
% 12.12/2.38 ( (less_than @ sk__4 @ sk__3))),
% 12.12/2.38 inference('simplify', [status(thm)], [zip_derived_cl3035])).
% 12.12/2.38 thf('14', plain,
% 12.12/2.38 ((![X5 : $i, X6 : $i]: (zip_tseitin_1 @ X5 @ X6 @ sk__4 @ sk__3 @ sk_)) |
% 12.12/2.38 ( (check_cpq @
% 12.12/2.38 (triple @ sk__1 @ (insert_slb @ sk_ @ (pair @ sk__3 @ sk__4)) @ sk__2)))),
% 12.12/2.38 inference('split', [status(esa)], [zip_derived_cl59])).
% 12.12/2.38 thf(zip_derived_cl15542, plain, ($false),
% 12.12/2.38 inference('sat_resolution*', [status(thm)],
% 12.12/2.38 ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9', '10', '11',
% 12.12/2.38 '12', '13', '14'])).
% 12.12/2.38
% 12.12/2.38 % SZS output end Refutation
% 12.12/2.38
% 12.12/2.38
% 12.12/2.38 % Terminating...
% 12.81/2.50 % Runner terminated.
% 12.81/2.51 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------