%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWX059+1 : TPTP v9.2.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.vbbtXfdEmS true
% Computer : n006.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:03:37 PM UTC 2025
% Result : Theorem 214.74s 31.26s
% Output : Refutation 214.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : SWX059+1 : TPTP v9.2.0. Released v9.1.0.
% 0.07/0.11 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.vbbtXfdEmS true
% 0.11/0.30 % Computer : n006.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8042.1875MB
% 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.30 % CPULimit : 300
% 0.11/0.30 % WCLimit : 300
% 0.11/0.30 % DateTime : Wed Oct 1 10:41:23 EDT 2025
% 0.11/0.30 % CPUTime :
% 0.11/0.30 % Running portfolio for 300 s
% 0.11/0.30 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.30 % Number of cores: 8
% 0.11/0.31 % Python version: Python 3.6.8
% 0.11/0.31 % Running in FO mode
% 0.52/0.61 % Total configuration time : 435
% 0.52/0.61 % Estimated wc time : 1092
% 0.52/0.61 % Estimated cpu time (7 cpus) : 156.0
% 0.57/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.57/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.57/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.57/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.57/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.57/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.57/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 214.74/31.26 % Solved by fo/fo6_bce.sh.
% 214.74/31.26 % BCE start: 595
% 214.74/31.26 % BCE eliminated: 1
% 214.74/31.26 % PE start: 594
% 214.74/31.26 logic: eq
% 214.74/31.26 % PE eliminated: 38
% 214.74/31.26 % done 10363 iterations in 30.538s
% 214.74/31.26 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 214.74/31.26 % SZS output start Refutation
% 214.74/31.26 thf(zip_tseitin_30_type, type, zip_tseitin_30: $i > $i > $i > $i > $o).
% 214.74/31.26 thf(s_type, type, s: $i > $i).
% 214.74/31.26 thf(cons_type, type, cons: $i > $i > $i).
% 214.74/31.26 thf(permutation_succeeds_type, type, permutation_succeeds: $i > $i > $o).
% 214.74/31.26 thf(@<_succeeds_type, type, @<_succeeds: $i > $i > $o).
% 214.74/31.26 thf(sk__131_type, type, sk__131: $i).
% 214.74/31.26 thf(sk__133_type, type, sk__133: $i).
% 214.74/31.26 thf(occ_type, type, occ: $i > $i > $i).
% 214.74/31.26 thf(0_type, type, 0: $i).
% 214.74/31.26 thf(list_succeeds_type, type, list_succeeds: $i > $o).
% 214.74/31.26 thf(sk__132_type, type, sk__132: $i).
% 214.74/31.26 thf(sk__110_type, type, sk__110: $i > $i).
% 214.74/31.26 thf(sk__128_type, type, sk__128: $i > $i > $i).
% 214.74/31.26 thf(zip_tseitin_29_type, type, zip_tseitin_29: $i > $i > $i > $o).
% 214.74/31.26 thf('theorem-(permutation:cons)', conjecture,
% 214.74/31.26 (![Xx:$i,Xl1:$i,Xl2:$i]:
% 214.74/31.26 ( ( permutation_succeeds @ ( cons @ Xx @ Xl1 ) @ ( cons @ Xx @ Xl2 ) ) =>
% 214.74/31.26 ( permutation_succeeds @ Xl1 @ Xl2 ) ))).
% 214.74/31.26 thf(zf_stmt_0, negated_conjecture,
% 214.74/31.26 (~( ![Xx:$i,Xl1:$i,Xl2:$i]:
% 214.74/31.26 ( ( permutation_succeeds @ ( cons @ Xx @ Xl1 ) @ ( cons @ Xx @ Xl2 ) ) =>
% 214.74/31.26 ( permutation_succeeds @ Xl1 @ Xl2 ) ) )),
% 214.74/31.26 inference('cnf.neg', [status(esa)], [theorem-(permutation:cons)])).
% 214.74/31.26 thf(zip_derived_cl593, plain,
% 214.74/31.26 ( (permutation_succeeds @ (cons @ sk__131 @ sk__132) @
% 214.74/31.26 (cons @ sk__131 @ sk__133))),
% 214.74/31.26 inference('cnf', [status(esa)], [zf_stmt_0])).
% 214.74/31.26 thf('theorem-(permutation:occ)', axiom,
% 214.74/31.26 (![Xl1:$i,Xl2:$i]:
% 214.74/31.26 ( ( permutation_succeeds @ Xl1 @ Xl2 ) =>
% 214.74/31.26 ( ![Xx:$i]: ( ( occ @ Xx @ Xl1 ) = ( occ @ Xx @ Xl2 ) ) ) ))).
% 214.74/31.26 thf(zip_derived_cl573, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i, X2 : $i]:
% 214.74/31.26 (((occ @ X0 @ X2) = (occ @ X0 @ X1))
% 214.74/31.26 | ~ (permutation_succeeds @ X2 @ X1))),
% 214.74/31.26 inference('cnf', [status(esa)], [theorem-(permutation:occ)])).
% 214.74/31.26 thf(zip_derived_cl3890, plain,
% 214.74/31.26 (![X0 : $i]:
% 214.74/31.26 ((occ @ X0 @ (cons @ sk__131 @ sk__132))
% 214.74/31.26 = (occ @ X0 @ (cons @ sk__131 @ sk__133)))),
% 214.74/31.26 inference('s_sup-', [status(thm)], [zip_derived_cl593, zip_derived_cl573])).
% 214.74/31.26 thf('lemma-(occ:cons:diff)', axiom,
% 214.74/31.26 (![Xx:$i,Xy:$i,Xl:$i]:
% 214.74/31.26 ( ( ( list_succeeds @ Xl ) & ( ( Xx ) != ( Xy ) ) ) =>
% 214.74/31.26 ( ( occ @ Xx @ ( cons @ Xy @ Xl ) ) = ( occ @ Xx @ Xl ) ) ))).
% 214.74/31.26 thf(zip_derived_cl567, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i, X2 : $i]:
% 214.74/31.26 (((X1) = (X0))
% 214.74/31.26 | ~ (list_succeeds @ X2)
% 214.74/31.26 | ((occ @ X1 @ (cons @ X0 @ X2)) = (occ @ X1 @ X2)))),
% 214.74/31.26 inference('cnf', [status(esa)], [lemma-(occ:cons:diff)])).
% 214.74/31.26 thf(zip_derived_cl9627, plain,
% 214.74/31.26 (![X0 : $i]:
% 214.74/31.26 (((X0) = (sk__131))
% 214.74/31.26 | ~ (list_succeeds @ sk__133)
% 214.74/31.26 | ((occ @ X0 @ (cons @ sk__131 @ sk__132)) = (occ @ X0 @ sk__133)))),
% 214.74/31.26 inference('s_sup+', [status(thm)],
% 214.74/31.26 [zip_derived_cl3890, zip_derived_cl567])).
% 214.74/31.26 thf(zip_derived_cl593, plain,
% 214.74/31.26 ( (permutation_succeeds @ (cons @ sk__131 @ sk__132) @
% 214.74/31.26 (cons @ sk__131 @ sk__133))),
% 214.74/31.26 inference('cnf', [status(esa)], [zf_stmt_0])).
% 214.74/31.26 thf('lemma-(permutation:types)', axiom,
% 214.74/31.26 (![Xl1:$i,Xl2:$i]:
% 214.74/31.26 ( ( permutation_succeeds @ Xl1 @ Xl2 ) =>
% 214.74/31.26 ( ( list_succeeds @ Xl1 ) & ( list_succeeds @ Xl2 ) ) ))).
% 214.74/31.26 thf(zip_derived_cl553, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i]:
% 214.74/31.26 ( (list_succeeds @ X0) | ~ (permutation_succeeds @ X1 @ X0))),
% 214.74/31.26 inference('cnf', [status(esa)], [lemma-(permutation:types)])).
% 214.74/31.26 thf(zip_derived_cl3767, plain,
% 214.74/31.26 ( (list_succeeds @ (cons @ sk__131 @ sk__133))),
% 214.74/31.26 inference('s_sup-', [status(thm)], [zip_derived_cl593, zip_derived_cl553])).
% 214.74/31.26 thf('axiom-(list:cons)', axiom,
% 214.74/31.26 (![Xx:$i,Xl:$i]:
% 214.74/31.26 ( ( list_succeeds @ ( cons @ Xx @ Xl ) ) => ( list_succeeds @ Xl ) ))).
% 214.74/31.26 thf(zip_derived_cl450, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i]:
% 214.74/31.26 ( (list_succeeds @ X0) | ~ (list_succeeds @ (cons @ X1 @ X0)))),
% 214.74/31.26 inference('cnf', [status(esa)], [axiom-(list:cons)])).
% 214.74/31.26 thf(zip_derived_cl3836, plain, ( (list_succeeds @ sk__133)),
% 214.74/31.26 inference('s_sup-', [status(thm)],
% 214.74/31.26 [zip_derived_cl3767, zip_derived_cl450])).
% 214.74/31.26 thf(zip_derived_cl9648, plain,
% 214.74/31.26 (![X0 : $i]:
% 214.74/31.26 (((X0) = (sk__131))
% 214.74/31.26 | ((occ @ X0 @ (cons @ sk__131 @ sk__132)) = (occ @ X0 @ sk__133)))),
% 214.74/31.26 inference('demod', [status(thm)],
% 214.74/31.26 [zip_derived_cl9627, zip_derived_cl3836])).
% 214.74/31.26 thf(zip_derived_cl567, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i, X2 : $i]:
% 214.74/31.26 (((X1) = (X0))
% 214.74/31.26 | ~ (list_succeeds @ X2)
% 214.74/31.26 | ((occ @ X1 @ (cons @ X0 @ X2)) = (occ @ X1 @ X2)))),
% 214.74/31.26 inference('cnf', [status(esa)], [lemma-(occ:cons:diff)])).
% 214.74/31.26 thf(zip_derived_cl17063, plain,
% 214.74/31.26 (![X0 : $i]:
% 214.74/31.26 (((X0) = (sk__131))
% 214.74/31.26 | ((X0) = (sk__131))
% 214.74/31.26 | ~ (list_succeeds @ sk__132)
% 214.74/31.26 | ((occ @ X0 @ sk__133) = (occ @ X0 @ sk__132)))),
% 214.74/31.26 inference('s_sup+', [status(thm)],
% 214.74/31.26 [zip_derived_cl9648, zip_derived_cl567])).
% 214.74/31.26 thf(zip_derived_cl593, plain,
% 214.74/31.26 ( (permutation_succeeds @ (cons @ sk__131 @ sk__132) @
% 214.74/31.26 (cons @ sk__131 @ sk__133))),
% 214.74/31.26 inference('cnf', [status(esa)], [zf_stmt_0])).
% 214.74/31.26 thf(zip_derived_cl552, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i]:
% 214.74/31.26 ( (list_succeeds @ X0) | ~ (permutation_succeeds @ X0 @ X1))),
% 214.74/31.26 inference('cnf', [status(esa)], [lemma-(permutation:types)])).
% 214.74/31.26 thf(zip_derived_cl3766, plain,
% 214.74/31.26 ( (list_succeeds @ (cons @ sk__131 @ sk__132))),
% 214.74/31.26 inference('s_sup-', [status(thm)], [zip_derived_cl593, zip_derived_cl552])).
% 214.74/31.26 thf(zip_derived_cl450, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i]:
% 214.74/31.26 ( (list_succeeds @ X0) | ~ (list_succeeds @ (cons @ X1 @ X0)))),
% 214.74/31.26 inference('cnf', [status(esa)], [axiom-(list:cons)])).
% 214.74/31.26 thf(zip_derived_cl3835, plain, ( (list_succeeds @ sk__132)),
% 214.74/31.26 inference('s_sup-', [status(thm)],
% 214.74/31.26 [zip_derived_cl3766, zip_derived_cl450])).
% 214.74/31.26 thf(zip_derived_cl17085, plain,
% 214.74/31.26 (![X0 : $i]:
% 214.74/31.26 (((X0) = (sk__131))
% 214.74/31.26 | ((X0) = (sk__131))
% 214.74/31.26 | ((occ @ X0 @ sk__133) = (occ @ X0 @ sk__132)))),
% 214.74/31.26 inference('demod', [status(thm)],
% 214.74/31.26 [zip_derived_cl17063, zip_derived_cl3835])).
% 214.74/31.26 thf(zip_derived_cl17086, plain,
% 214.74/31.26 (![X0 : $i]:
% 214.74/31.26 (((occ @ X0 @ sk__133) = (occ @ X0 @ sk__132)) | ((X0) = (sk__131)))),
% 214.74/31.26 inference('simplify', [status(thm)], [zip_derived_cl17085])).
% 214.74/31.26 thf('lemma-(permutation:completeness)', axiom,
% 214.74/31.26 (![Xl2:$i]:
% 214.74/31.26 ( ( list_succeeds @ Xl2 ) =>
% 214.74/31.26 ( ![Xl1:$i]:
% 214.74/31.26 ( ( ( list_succeeds @ Xl1 ) &
% 214.74/31.26 ( ![Xx:$i]: ( ( occ @ Xx @ Xl1 ) = ( occ @ Xx @ Xl2 ) ) ) ) =>
% 214.74/31.26 ( permutation_succeeds @ Xl1 @ Xl2 ) ) ) ))).
% 214.74/31.26 thf(zip_derived_cl577, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i]:
% 214.74/31.26 (~ (list_succeeds @ X0)
% 214.74/31.26 | ((occ @ (sk__128 @ X0 @ X1) @ X0)
% 214.74/31.26 != (occ @ (sk__128 @ X0 @ X1) @ X1))
% 214.74/31.26 | (permutation_succeeds @ X0 @ X1)
% 214.74/31.26 | ~ (list_succeeds @ X1))),
% 214.74/31.26 inference('cnf', [status(esa)], [lemma-(permutation:completeness)])).
% 214.74/31.26 thf(zip_derived_cl23846, plain,
% 214.74/31.26 (![X0 : $i]:
% 214.74/31.26 (((sk__128 @ X0 @ sk__133) = (sk__131))
% 214.74/31.26 | ~ (list_succeeds @ X0)
% 214.74/31.26 | ((occ @ (sk__128 @ X0 @ sk__133) @ X0)
% 214.74/31.26 != (occ @ (sk__128 @ X0 @ sk__133) @ sk__132))
% 214.74/31.26 | (permutation_succeeds @ X0 @ sk__133)
% 214.74/31.26 | ~ (list_succeeds @ sk__133))),
% 214.74/31.26 inference('s_sup-', [status(thm)],
% 214.74/31.26 [zip_derived_cl17086, zip_derived_cl577])).
% 214.74/31.26 thf(zip_derived_cl3836, plain, ( (list_succeeds @ sk__133)),
% 214.74/31.26 inference('s_sup-', [status(thm)],
% 214.74/31.26 [zip_derived_cl3767, zip_derived_cl450])).
% 214.74/31.26 thf(zip_derived_cl23883, plain,
% 214.74/31.26 (![X0 : $i]:
% 214.74/31.26 (((sk__128 @ X0 @ sk__133) = (sk__131))
% 214.74/31.26 | ~ (list_succeeds @ X0)
% 214.74/31.26 | ((occ @ (sk__128 @ X0 @ sk__133) @ X0)
% 214.74/31.26 != (occ @ (sk__128 @ X0 @ sk__133) @ sk__132))
% 214.74/31.26 | (permutation_succeeds @ X0 @ sk__133))),
% 214.74/31.26 inference('demod', [status(thm)],
% 214.74/31.26 [zip_derived_cl23846, zip_derived_cl3836])).
% 214.74/31.26 thf(zip_derived_cl148045, plain,
% 214.74/31.26 (( (permutation_succeeds @ sk__132 @ sk__133)
% 214.74/31.26 | ~ (list_succeeds @ sk__132)
% 214.74/31.26 | ((sk__128 @ sk__132 @ sk__133) = (sk__131)))),
% 214.74/31.26 inference('eq_res', [status(thm)], [zip_derived_cl23883])).
% 214.74/31.26 thf(zip_derived_cl594, plain, (~ (permutation_succeeds @ sk__132 @ sk__133)),
% 214.74/31.26 inference('cnf', [status(esa)], [zf_stmt_0])).
% 214.74/31.26 thf(zip_derived_cl3835, plain, ( (list_succeeds @ sk__132)),
% 214.74/31.26 inference('s_sup-', [status(thm)],
% 214.74/31.26 [zip_derived_cl3766, zip_derived_cl450])).
% 214.74/31.26 thf(zip_derived_cl148046, plain,
% 214.74/31.26 (((sk__128 @ sk__132 @ sk__133) = (sk__131))),
% 214.74/31.26 inference('demod', [status(thm)],
% 214.74/31.26 [zip_derived_cl148045, zip_derived_cl594, zip_derived_cl3835])).
% 214.74/31.26 thf(zip_derived_cl577, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i]:
% 214.74/31.26 (~ (list_succeeds @ X0)
% 214.74/31.26 | ((occ @ (sk__128 @ X0 @ X1) @ X0)
% 214.74/31.26 != (occ @ (sk__128 @ X0 @ X1) @ X1))
% 214.74/31.26 | (permutation_succeeds @ X0 @ X1)
% 214.74/31.26 | ~ (list_succeeds @ X1))),
% 214.74/31.26 inference('cnf', [status(esa)], [lemma-(permutation:completeness)])).
% 214.74/31.26 thf(zip_derived_cl148072, plain,
% 214.74/31.26 ((~ (list_succeeds @ sk__132)
% 214.74/31.26 | ((occ @ sk__131 @ sk__132) != (occ @ sk__131 @ sk__133))
% 214.74/31.26 | (permutation_succeeds @ sk__132 @ sk__133)
% 214.74/31.26 | ~ (list_succeeds @ sk__133))),
% 214.74/31.26 inference('s_sup-', [status(thm)],
% 214.74/31.26 [zip_derived_cl148046, zip_derived_cl577])).
% 214.74/31.26 thf(zip_derived_cl3835, plain, ( (list_succeeds @ sk__132)),
% 214.74/31.26 inference('s_sup-', [status(thm)],
% 214.74/31.26 [zip_derived_cl3766, zip_derived_cl450])).
% 214.74/31.26 thf(zip_derived_cl3890, plain,
% 214.74/31.26 (![X0 : $i]:
% 214.74/31.26 ((occ @ X0 @ (cons @ sk__131 @ sk__132))
% 214.74/31.26 = (occ @ X0 @ (cons @ sk__131 @ sk__133)))),
% 214.74/31.26 inference('s_sup-', [status(thm)], [zip_derived_cl593, zip_derived_cl573])).
% 214.74/31.26 thf('lemma-(occ:cons:eq)', axiom,
% 214.74/31.26 (![Xx:$i,Xl:$i]:
% 214.74/31.26 ( ( list_succeeds @ Xl ) =>
% 214.74/31.26 ( ( occ @ Xx @ ( cons @ Xx @ Xl ) ) = ( s @ ( occ @ Xx @ Xl ) ) ) ))).
% 214.74/31.26 thf(zip_derived_cl568, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i]:
% 214.74/31.26 (((occ @ X0 @ (cons @ X0 @ X1)) = (s @ (occ @ X0 @ X1)))
% 214.74/31.26 | ~ (list_succeeds @ X1))),
% 214.74/31.26 inference('cnf', [status(esa)], [lemma-(occ:cons:eq)])).
% 214.74/31.26 thf(zip_derived_cl9541, plain,
% 214.74/31.26 ((((occ @ sk__131 @ (cons @ sk__131 @ sk__132))
% 214.74/31.26 = (s @ (occ @ sk__131 @ sk__133)))
% 214.74/31.26 | ~ (list_succeeds @ sk__133))),
% 214.74/31.26 inference('s_sup+', [status(thm)],
% 214.74/31.26 [zip_derived_cl3890, zip_derived_cl568])).
% 214.74/31.26 thf(zip_derived_cl3836, plain, ( (list_succeeds @ sk__133)),
% 214.74/31.26 inference('s_sup-', [status(thm)],
% 214.74/31.26 [zip_derived_cl3767, zip_derived_cl450])).
% 214.74/31.26 thf(zip_derived_cl9561, plain,
% 214.74/31.26 (((occ @ sk__131 @ (cons @ sk__131 @ sk__132))
% 214.74/31.26 = (s @ (occ @ sk__131 @ sk__133)))),
% 214.74/31.26 inference('demod', [status(thm)],
% 214.74/31.26 [zip_derived_cl9541, zip_derived_cl3836])).
% 214.74/31.26 thf(zip_derived_cl568, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i]:
% 214.74/31.26 (((occ @ X0 @ (cons @ X0 @ X1)) = (s @ (occ @ X0 @ X1)))
% 214.74/31.26 | ~ (list_succeeds @ X1))),
% 214.74/31.26 inference('cnf', [status(esa)], [lemma-(occ:cons:eq)])).
% 214.74/31.26 thf(zip_derived_cl9661, plain,
% 214.74/31.26 ((((s @ (occ @ sk__131 @ sk__133)) = (s @ (occ @ sk__131 @ sk__132)))
% 214.74/31.26 | ~ (list_succeeds @ sk__132))),
% 214.74/31.26 inference('s_sup+', [status(thm)],
% 214.74/31.26 [zip_derived_cl9561, zip_derived_cl568])).
% 214.74/31.26 thf(zip_derived_cl3835, plain, ( (list_succeeds @ sk__132)),
% 214.74/31.26 inference('s_sup-', [status(thm)],
% 214.74/31.26 [zip_derived_cl3766, zip_derived_cl450])).
% 214.74/31.26 thf(zip_derived_cl9667, plain,
% 214.74/31.26 (((s @ (occ @ sk__131 @ sk__133)) = (s @ (occ @ sk__131 @ sk__132)))),
% 214.74/31.26 inference('demod', [status(thm)],
% 214.74/31.26 [zip_derived_cl9661, zip_derived_cl3835])).
% 214.74/31.26 thf(id88, axiom,
% 214.74/31.26 (![Xx1:$i,Xx2:$i]:
% 214.74/31.26 ( ( @<_succeeds @ Xx1 @ Xx2 ) <=>
% 214.74/31.26 ( ( ?[Xx5:$i]: ( ( ( Xx1 ) = ( 0 ) ) & ( ( Xx2 ) = ( s @ Xx5 ) ) ) ) |
% 214.74/31.26 ( ?[Xx3:$i,Xx4:$i]:
% 214.74/31.26 ( ( ( Xx1 ) = ( s @ Xx3 ) ) & ( ( Xx2 ) = ( s @ Xx4 ) ) &
% 214.74/31.26 ( @<_succeeds @ Xx3 @ Xx4 ) ) ) ) ))).
% 214.74/31.26 thf(zf_stmt_1, axiom,
% 214.74/31.26 (![Xx5:$i,Xx2:$i,Xx1:$i]:
% 214.74/31.26 ( ( zip_tseitin_29 @ Xx5 @ Xx2 @ Xx1 ) <=>
% 214.74/31.26 ( ( ( Xx2 ) = ( s @ Xx5 ) ) & ( ( Xx1 ) = ( 0 ) ) ) ))).
% 214.74/31.26 thf(zip_derived_cl318, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i, X2 : $i]:
% 214.74/31.26 ( (zip_tseitin_29 @ X0 @ X1 @ X2) | ((X2) != (0)) | ((X1) != (s @ X0)))),
% 214.74/31.26 inference('cnf', [status(esa)], [zf_stmt_1])).
% 214.74/31.26 thf(zf_stmt_2, type, zip_tseitin_30 : $i > $i > $i > $i > $o).
% 214.74/31.26 thf(zf_stmt_3, axiom,
% 214.74/31.26 (![Xx4:$i,Xx3:$i,Xx2:$i,Xx1:$i]:
% 214.74/31.26 ( ( zip_tseitin_30 @ Xx4 @ Xx3 @ Xx2 @ Xx1 ) <=>
% 214.74/31.26 ( ( @<_succeeds @ Xx3 @ Xx4 ) & ( ( Xx2 ) = ( s @ Xx4 ) ) &
% 214.74/31.26 ( ( Xx1 ) = ( s @ Xx3 ) ) ) ))).
% 214.74/31.26 thf(zf_stmt_4, type, zip_tseitin_29 : $i > $i > $i > $o).
% 214.74/31.26 thf(zf_stmt_5, axiom,
% 214.74/31.26 (![Xx1:$i,Xx2:$i]:
% 214.74/31.26 ( ( @<_succeeds @ Xx1 @ Xx2 ) <=>
% 214.74/31.26 ( ( ?[Xx3:$i,Xx4:$i]: ( zip_tseitin_30 @ Xx4 @ Xx3 @ Xx2 @ Xx1 ) ) |
% 214.74/31.26 ( ?[Xx5:$i]: ( zip_tseitin_29 @ Xx5 @ Xx2 @ Xx1 ) ) ) ))).
% 214.74/31.26 thf(zip_derived_cl325, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i, X2 : $i]:
% 214.74/31.26 ( (@<_succeeds @ X0 @ X1) | ~ (zip_tseitin_29 @ X2 @ X1 @ X0))),
% 214.74/31.26 inference('cnf', [status(esa)], [zf_stmt_5])).
% 214.74/31.26 thf(zip_derived_cl3374, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i, X2 : $i]:
% 214.74/31.26 (((X1) != (s @ X2)) | ((X0) != (0)) | (@<_succeeds @ X0 @ X1))),
% 214.74/31.26 inference('dp-resolution', [status(thm)],
% 214.74/31.26 [zip_derived_cl318, zip_derived_cl325])).
% 214.74/31.26 thf(zip_derived_cl3819, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i]: ( (@<_succeeds @ 0 @ X0) | ((X0) != (s @ X1)))),
% 214.74/31.26 inference('eq_res', [status(thm)], [zip_derived_cl3374])).
% 214.74/31.26 thf(zip_derived_cl3820, plain, (![X0 : $i]: (@<_succeeds @ 0 @ (s @ X0))),
% 214.74/31.26 inference('eq_res', [status(thm)], [zip_derived_cl3819])).
% 214.74/31.26 thf('axiom-(less:successor)', axiom,
% 214.74/31.26 (![Xx:$i,Xy:$i]:
% 214.74/31.26 ( ( @<_succeeds @ Xx @ Xy ) => ( ?[Xz:$i]: ( ( Xy ) = ( s @ Xz ) ) ) ))).
% 214.74/31.26 thf(zip_derived_cl399, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i]:
% 214.74/31.26 (((X0) = (s @ (sk__110 @ X0))) | ~ (@<_succeeds @ X1 @ X0))),
% 214.74/31.26 inference('cnf', [status(esa)], [axiom-(less:successor)])).
% 214.74/31.26 thf(zip_derived_cl5401, plain,
% 214.74/31.26 (![X0 : $i]: ((s @ X0) = (s @ (sk__110 @ (s @ X0))))),
% 214.74/31.26 inference('s_sup-', [status(thm)],
% 214.74/31.26 [zip_derived_cl3820, zip_derived_cl399])).
% 214.74/31.26 thf(id6, axiom,
% 214.74/31.26 (![Xx9:$i,Xx10:$i]:
% 214.74/31.26 ( ( ( s @ Xx9 ) = ( s @ Xx10 ) ) => ( ( Xx9 ) = ( Xx10 ) ) ))).
% 214.74/31.26 thf(zip_derived_cl5, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i]: (((X1) = (X0)) | ((s @ X1) != (s @ X0)))),
% 214.74/31.26 inference('cnf', [status(esa)], [id6])).
% 214.74/31.26 thf(zip_derived_cl6204, plain,
% 214.74/31.26 (![X0 : $i, X1 : $i]:
% 214.74/31.26 (((X1) = (sk__110 @ (s @ X0))) | ((s @ X1) != (s @ X0)))),
% 214.74/31.26 inference('s_sup-', [status(thm)], [zip_derived_cl5401, zip_derived_cl5])).
% 214.74/31.26 thf(zip_derived_cl6460, plain, (![X0 : $i]: ((X0) = (sk__110 @ (s @ X0)))),
% 214.74/31.26 inference('eq_res', [status(thm)], [zip_derived_cl6204])).
% 214.74/31.26 thf(zip_derived_cl9972, plain,
% 214.74/31.26 (((occ @ sk__131 @ sk__133) = (sk__110 @ (s @ (occ @ sk__131 @ sk__132))))),
% 214.74/31.26 inference('s_sup+', [status(thm)],
% 214.74/31.26 [zip_derived_cl9667, zip_derived_cl6460])).
% 214.74/31.26 thf(zip_derived_cl6460, plain, (![X0 : $i]: ((X0) = (sk__110 @ (s @ X0)))),
% 214.74/31.26 inference('eq_res', [status(thm)], [zip_derived_cl6204])).
% 214.74/31.26 thf(zip_derived_cl10016, plain,
% 214.74/31.26 (((occ @ sk__131 @ sk__133) = (occ @ sk__131 @ sk__132))),
% 214.74/31.26 inference('demod', [status(thm)],
% 214.74/31.26 [zip_derived_cl9972, zip_derived_cl6460])).
% 214.74/31.26 thf(zip_derived_cl594, plain, (~ (permutation_succeeds @ sk__132 @ sk__133)),
% 214.74/31.26 inference('cnf', [status(esa)], [zf_stmt_0])).
% 214.74/31.26 thf(zip_derived_cl3836, plain, ( (list_succeeds @ sk__133)),
% 214.74/31.26 inference('s_sup-', [status(thm)],
% 214.74/31.26 [zip_derived_cl3767, zip_derived_cl450])).
% 214.74/31.26 thf(zip_derived_cl148075, plain,
% 214.74/31.26 (((occ @ sk__131 @ sk__132) != (occ @ sk__131 @ sk__132))),
% 214.74/31.26 inference('demod', [status(thm)],
% 214.74/31.26 [zip_derived_cl148072, zip_derived_cl3835,
% 214.74/31.26 zip_derived_cl10016, zip_derived_cl594, zip_derived_cl3836])).
% 214.74/31.26 thf(zip_derived_cl148076, plain, ($false),
% 214.74/31.26 inference('simplify', [status(thm)], [zip_derived_cl148075])).
% 214.74/31.26
% 214.74/31.26 % SZS output end Refutation
% 214.74/31.26
% 214.74/31.26
% 214.74/31.26 % Terminating...
% 214.74/31.34 % Runner terminated.
% 214.74/31.35 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------