%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : RNG126+4 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.0BFoD6xzKL true
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 04:50:37 PM UTC 2025
% Result : Theorem 96.93s 14.52s
% Output : Refutation 96.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.11 % Problem : RNG126+4 : TPTP v9.2.0. Released v4.0.0.
% 0.09/0.12 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.0BFoD6xzKL true
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Oct 1 17:22:23 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.33 % Running portfolio for 300 s
% 0.12/0.33 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.33 % Number of cores: 8
% 0.12/0.34 % Python version: Python 3.6.8
% 0.12/0.34 % Running in FO mode
% 0.42/0.60 % Total configuration time : 435
% 0.42/0.60 % Estimated wc time : 1092
% 0.42/0.60 % Estimated cpu time (7 cpus) : 156.0
% 0.52/0.70 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.52/0.72 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.52/0.72 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.52/0.72 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.52/0.73 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.52/0.73 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.52/0.73 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 96.93/14.52 % Solved by fo/fo3_bce.sh.
% 96.93/14.52 % BCE start: 186
% 96.93/14.52 % BCE eliminated: 1
% 96.93/14.52 % PE start: 185
% 96.93/14.52 logic: eq
% 96.93/14.52 % PE eliminated: -4
% 96.93/14.52 % done 6792 iterations in 13.763s
% 96.93/14.52 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 96.93/14.52 % SZS output start Refutation
% 96.93/14.52 thf(sdtasdt0_type, type, sdtasdt0: $i > $i > $i).
% 96.93/14.52 thf(aElement0_type, type, aElement0: $i > $o).
% 96.93/14.52 thf(zip_tseitin_7_type, type, zip_tseitin_7: $i > $o).
% 96.93/14.52 thf(sdtpldt1_type, type, sdtpldt1: $i > $i > $i).
% 96.93/14.52 thf(xI_type, type, xI: $i).
% 96.93/14.52 thf(aDivisorOf0_type, type, aDivisorOf0: $i > $i > $o).
% 96.93/14.52 thf(zip_tseitin_10_type, type, zip_tseitin_10: $i > $i > $o).
% 96.93/14.52 thf(sbrdtbr0_type, type, sbrdtbr0: $i > $i).
% 96.93/14.52 thf(xa_type, type, xa: $i).
% 96.93/14.52 thf(sz00_type, type, sz00: $i).
% 96.93/14.52 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 96.93/14.52 thf(slsdtgt0_type, type, slsdtgt0: $i > $i).
% 96.93/14.52 thf(aIdeal0_type, type, aIdeal0: $i > $o).
% 96.93/14.52 thf(sk__20_type, type, sk__20: $i > $i).
% 96.93/14.52 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $o).
% 96.93/14.52 thf(xu_type, type, xu: $i).
% 96.93/14.52 thf(aGcdOfAnd0_type, type, aGcdOfAnd0: $i > $i > $i > $o).
% 96.93/14.52 thf(iLess0_type, type, iLess0: $i > $i > $o).
% 96.93/14.52 thf(xc_type, type, xc: $i).
% 96.93/14.52 thf(zip_tseitin_9_type, type, zip_tseitin_9: $i > $o).
% 96.93/14.52 thf(doDivides0_type, type, doDivides0: $i > $i > $o).
% 96.93/14.52 thf(zip_tseitin_11_type, type, zip_tseitin_11: $i > $i > $o).
% 96.93/14.52 thf(zip_tseitin_6_type, type, zip_tseitin_6: $i > $o).
% 96.93/14.52 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 96.93/14.52 thf(zip_tseitin_8_type, type, zip_tseitin_8: $i > $i > $o).
% 96.93/14.52 thf(aSet0_type, type, aSet0: $i > $o).
% 96.93/14.52 thf(xb_type, type, xb: $i).
% 96.93/14.52 thf(m__2373, axiom,
% 96.93/14.52 (( aDivisorOf0 @ xu @ xb ) & ( doDivides0 @ xu @ xb ) &
% 96.93/14.52 ( ?[W0:$i]: ( ( ( sdtasdt0 @ xu @ W0 ) = ( xb ) ) & ( aElement0 @ W0 ) ) ) &
% 96.93/14.52 ( aDivisorOf0 @ xu @ xa ) & ( doDivides0 @ xu @ xa ) &
% 96.93/14.52 ( ?[W0:$i]: ( ( ( sdtasdt0 @ xu @ W0 ) = ( xa ) ) & ( aElement0 @ W0 ) ) ))).
% 96.93/14.52 thf(zip_derived_cl167, plain, ( (aDivisorOf0 @ xu @ xa)),
% 96.93/14.52 inference('cnf', [status(esa)], [m__2373])).
% 96.93/14.52 thf(m__2129, axiom,
% 96.93/14.52 (( aElement0 @ xc ) &
% 96.93/14.52 ( ?[W0:$i]: ( ( aElement0 @ W0 ) & ( ( sdtasdt0 @ xc @ W0 ) = ( xa ) ) ) ) &
% 96.93/14.52 ( doDivides0 @ xc @ xa ) & ( aDivisorOf0 @ xc @ xa ) &
% 96.93/14.52 ( aElement0 @ xc ) &
% 96.93/14.52 ( ?[W0:$i]: ( ( aElement0 @ W0 ) & ( ( sdtasdt0 @ xc @ W0 ) = ( xb ) ) ) ) &
% 96.93/14.52 ( doDivides0 @ xc @ xb ) & ( aDivisorOf0 @ xc @ xb ) &
% 96.93/14.52 ( ![W0:$i]:
% 96.93/14.52 ( ( ( ( aDivisorOf0 @ W0 @ xb ) | ( doDivides0 @ W0 @ xb ) |
% 96.93/14.52 ( ?[W1:$i]:
% 96.93/14.52 ( ( aElement0 @ W1 ) & ( ( sdtasdt0 @ W0 @ W1 ) = ( xb ) ) ) ) ) &
% 96.93/14.52 ( ( aDivisorOf0 @ W0 @ xa ) |
% 96.93/14.52 ( ( ( doDivides0 @ W0 @ xa ) |
% 96.93/14.52 ( ?[W1:$i]:
% 96.93/14.52 ( ( aElement0 @ W1 ) & ( ( sdtasdt0 @ W0 @ W1 ) = ( xa ) ) ) ) ) &
% 96.93/14.52 ( aElement0 @ W0 ) ) ) ) =>
% 96.93/14.52 ( ( doDivides0 @ W0 @ xc ) &
% 96.93/14.52 ( ?[W1:$i]:
% 96.93/14.52 ( ( aElement0 @ W1 ) & ( ( sdtasdt0 @ W0 @ W1 ) = ( xc ) ) ) ) ) ) ) &
% 96.93/14.52 ( aGcdOfAnd0 @ xc @ xa @ xb ))).
% 96.93/14.52 thf(zf_stmt_0, axiom,
% 96.93/14.52 (![W0:$i]:
% 96.93/14.52 ( ( ( ?[W1:$i]:
% 96.93/14.52 ( ( ( sdtasdt0 @ W0 @ W1 ) = ( xb ) ) & ( aElement0 @ W1 ) ) ) |
% 96.93/14.52 ( doDivides0 @ W0 @ xb ) | ( aDivisorOf0 @ W0 @ xb ) ) =>
% 96.93/14.52 ( zip_tseitin_5 @ W0 ) ))).
% 96.93/14.52 thf(zip_derived_cl98, plain,
% 96.93/14.52 (![X0 : $i]: ( (zip_tseitin_5 @ X0) | ~ (doDivides0 @ X0 @ xb))),
% 96.93/14.52 inference('cnf', [status(esa)], [zf_stmt_0])).
% 96.93/14.52 thf(zf_stmt_1, axiom,
% 96.93/14.52 (![W0:$i]:
% 96.93/14.52 ( ( ( ( aElement0 @ W0 ) & ( zip_tseitin_6 @ W0 ) ) |
% 96.93/14.52 ( aDivisorOf0 @ W0 @ xa ) ) =>
% 96.93/14.52 ( zip_tseitin_7 @ W0 ) ))).
% 96.93/14.52 thf(zip_derived_cl103, plain,
% 96.93/14.52 (![X0 : $i]: ( (zip_tseitin_7 @ X0) | ~ (aDivisorOf0 @ X0 @ xa))),
% 96.93/14.52 inference('cnf', [status(esa)], [zf_stmt_1])).
% 96.93/14.52 thf(zf_stmt_2, type, zip_tseitin_9 : $i > $o).
% 96.93/14.52 thf(zf_stmt_3, axiom,
% 96.93/14.52 (![W0:$i]:
% 96.93/14.52 ( ( zip_tseitin_9 @ W0 ) =>
% 96.93/14.52 ( ( ?[W1:$i]: ( zip_tseitin_8 @ W1 @ W0 ) ) & ( doDivides0 @ W0 @ xc ) ) ))).
% 96.93/14.52 thf(zf_stmt_4, type, zip_tseitin_8 : $i > $i > $o).
% 96.93/14.52 thf(zf_stmt_5, axiom,
% 96.93/14.52 (![W1:$i,W0:$i]:
% 96.93/14.52 ( ( zip_tseitin_8 @ W1 @ W0 ) =>
% 96.93/14.52 ( ( ( sdtasdt0 @ W0 @ W1 ) = ( xc ) ) & ( aElement0 @ W1 ) ) ))).
% 96.93/14.52 thf(zf_stmt_6, type, zip_tseitin_7 : $i > $o).
% 96.93/14.52 thf(zf_stmt_7, type, zip_tseitin_6 : $i > $o).
% 96.93/14.52 thf(zf_stmt_8, axiom,
% 96.93/14.52 (![W0:$i]:
% 96.93/14.52 ( ( ( ?[W1:$i]:
% 96.93/14.52 ( ( ( sdtasdt0 @ W0 @ W1 ) = ( xa ) ) & ( aElement0 @ W1 ) ) ) |
% 96.93/14.52 ( doDivides0 @ W0 @ xa ) ) =>
% 96.93/14.52 ( zip_tseitin_6 @ W0 ) ))).
% 96.93/14.52 thf(zf_stmt_9, type, zip_tseitin_5 : $i > $o).
% 96.93/14.52 thf(zf_stmt_10, axiom,
% 96.93/14.52 (( ?[W0:$i]: ( ( ( sdtasdt0 @ xc @ W0 ) = ( xb ) ) & ( aElement0 @ W0 ) ) ) &
% 96.93/14.52 ( aGcdOfAnd0 @ xc @ xa @ xb ) &
% 96.93/14.52 ( ![W0:$i]:
% 96.93/14.52 ( ( ( zip_tseitin_7 @ W0 ) & ( zip_tseitin_5 @ W0 ) ) =>
% 96.93/14.52 ( zip_tseitin_9 @ W0 ) ) ) &
% 96.93/14.52 ( aDivisorOf0 @ xc @ xa ) & ( aElement0 @ xc ) &
% 96.93/14.52 ( ?[W0:$i]: ( ( ( sdtasdt0 @ xc @ W0 ) = ( xa ) ) & ( aElement0 @ W0 ) ) ) &
% 96.93/14.52 ( doDivides0 @ xc @ xb ) & ( aDivisorOf0 @ xc @ xb ) &
% 96.93/14.52 ( doDivides0 @ xc @ xa ))).
% 96.93/14.52 thf(zip_derived_cl115, plain,
% 96.93/14.52 (![X0 : $i]:
% 96.93/14.52 ( (zip_tseitin_9 @ X0)
% 96.93/14.52 | ~ (zip_tseitin_5 @ X0)
% 96.93/14.52 | ~ (zip_tseitin_7 @ X0))),
% 96.93/14.52 inference('cnf', [status(esa)], [zf_stmt_10])).
% 96.93/14.52 thf(zip_derived_cl997, plain,
% 96.93/14.52 (![X0 : $i]:
% 96.93/14.52 (~ (aDivisorOf0 @ X0 @ xa)
% 96.93/14.52 | ~ (zip_tseitin_5 @ X0)
% 96.93/14.52 | (zip_tseitin_9 @ X0))),
% 96.93/14.52 inference('dp-resolution', [status(thm)],
% 96.93/14.52 [zip_derived_cl103, zip_derived_cl115])).
% 96.93/14.52 thf(zip_derived_cl106, plain,
% 96.93/14.52 (![X0 : $i]:
% 96.93/14.52 ( (zip_tseitin_8 @ (sk__20 @ X0) @ X0) | ~ (zip_tseitin_9 @ X0))),
% 96.93/14.52 inference('cnf', [status(esa)], [zf_stmt_3])).
% 96.93/14.52 thf(zip_derived_cl104, plain,
% 96.93/14.52 (![X0 : $i, X1 : $i]:
% 96.93/14.52 (((sdtasdt0 @ X0 @ X1) = (xc)) | ~ (zip_tseitin_8 @ X1 @ X0))),
% 96.93/14.52 inference('cnf', [status(esa)], [zf_stmt_5])).
% 96.93/14.52 thf(zip_derived_cl994, plain,
% 96.93/14.52 (![X0 : $i]:
% 96.93/14.52 (~ (zip_tseitin_9 @ X0) | ((sdtasdt0 @ X0 @ (sk__20 @ X0)) = (xc)))),
% 96.93/14.52 inference('dp-resolution', [status(thm)],
% 96.93/14.52 [zip_derived_cl106, zip_derived_cl104])).
% 96.93/14.52 thf(zip_derived_cl1030, plain,
% 96.93/14.52 (![X0 : $i]:
% 96.93/14.52 (~ (zip_tseitin_5 @ X0)
% 96.93/14.52 | ~ (aDivisorOf0 @ X0 @ xa)
% 96.93/14.52 | ((sdtasdt0 @ X0 @ (sk__20 @ X0)) = (xc)))),
% 96.93/14.52 inference('dp-resolution', [status(thm)],
% 96.93/14.52 [zip_derived_cl997, zip_derived_cl994])).
% 96.93/14.52 thf(zip_derived_cl1068, plain,
% 96.93/14.52 (![X0 : $i]:
% 96.93/14.52 (~ (doDivides0 @ X0 @ xb)
% 96.93/14.52 | ((sdtasdt0 @ X0 @ (sk__20 @ X0)) = (xc))
% 96.93/14.52 | ~ (aDivisorOf0 @ X0 @ xa))),
% 96.93/14.52 inference('dp-resolution', [status(thm)],
% 96.93/14.52 [zip_derived_cl98, zip_derived_cl1030])).
% 96.93/14.52 thf(zip_derived_cl5655, plain,
% 96.93/14.52 ((((sdtasdt0 @ xu @ (sk__20 @ xu)) = (xc)) | ~ (doDivides0 @ xu @ xb))),
% 96.93/14.52 inference('sup-', [status(thm)], [zip_derived_cl167, zip_derived_cl1068])).
% 96.93/14.52 thf(zip_derived_cl170, plain, ( (doDivides0 @ xu @ xb)),
% 96.93/14.52 inference('cnf', [status(esa)], [m__2373])).
% 96.93/14.52 thf(zip_derived_cl5658, plain, (((sdtasdt0 @ xu @ (sk__20 @ xu)) = (xc))),
% 96.93/14.52 inference('demod', [status(thm)], [zip_derived_cl5655, zip_derived_cl170])).
% 96.93/14.52 thf(mMulComm, axiom,
% 96.93/14.52 (![W0:$i,W1:$i]:
% 96.93/14.52 ( ( ( aElement0 @ W0 ) & ( aElement0 @ W1 ) ) =>
% 96.93/14.52 ( ( sdtasdt0 @ W0 @ W1 ) = ( sdtasdt0 @ W1 @ W0 ) ) ))).
% 96.93/14.52 thf(zip_derived_cl12, plain,
% 96.93/14.52 (![X0 : $i, X1 : $i]:
% 96.93/14.52 (~ (aElement0 @ X0)
% 96.93/14.52 | ~ (aElement0 @ X1)
% 96.93/14.52 | ((sdtasdt0 @ X0 @ X1) = (sdtasdt0 @ X1 @ X0)))),
% 96.93/14.52 inference('cnf', [status(esa)], [mMulComm])).
% 96.93/14.52 thf(m__2174, axiom,
% 96.93/14.52 (( ( xI ) = ( sdtpldt1 @ ( slsdtgt0 @ xa ) @ ( slsdtgt0 @ xb ) ) ) &
% 96.93/14.52 ( ![W0:$i]:
% 96.93/14.52 ( ( aElementOf0 @ W0 @ xI ) <=>
% 96.93/14.52 ( ?[W1:$i,W2:$i]:
% 96.93/14.52 ( ( ( sdtpldt0 @ W1 @ W2 ) = ( W0 ) ) &
% 96.93/14.52 ( aElementOf0 @ W2 @ ( slsdtgt0 @ xb ) ) &
% 96.93/14.52 ( aElementOf0 @ W1 @ ( slsdtgt0 @ xa ) ) ) ) ) ) &
% 96.93/14.52 ( ![W0:$i]:
% 96.93/14.52 ( ( aElementOf0 @ W0 @ ( slsdtgt0 @ xb ) ) <=>
% 96.93/14.52 ( ?[W1:$i]:
% 96.93/14.52 ( ( ( sdtasdt0 @ xb @ W1 ) = ( W0 ) ) & ( aElement0 @ W1 ) ) ) ) ) &
% 96.93/14.52 ( ![W0:$i]:
% 96.93/14.52 ( ( aElementOf0 @ W0 @ ( slsdtgt0 @ xa ) ) <=>
% 96.93/14.52 ( ?[W1:$i]:
% 96.93/14.52 ( ( ( sdtasdt0 @ xa @ W1 ) = ( W0 ) ) & ( aElement0 @ W1 ) ) ) ) ) &
% 96.93/14.52 ( aIdeal0 @ xI ) &
% 96.93/14.52 ( ![W0:$i]:
% 96.93/14.52 ( ( aElementOf0 @ W0 @ xI ) =>
% 96.93/14.52 ( ( ![W1:$i]:
% 96.93/14.52 ( ( aElementOf0 @ W1 @ xI ) =>
% 96.93/14.52 ( aElementOf0 @ ( sdtpldt0 @ W0 @ W1 ) @ xI ) ) ) &
% 96.93/14.52 ( ![W1:$i]:
% 96.93/14.52 ( ( aElement0 @ W1 ) =>
% 96.93/14.52 ( aElementOf0 @ ( sdtasdt0 @ W1 @ W0 ) @ xI ) ) ) ) ) ) &
% 96.93/14.52 ( aSet0 @ xI ))).
% 96.93/14.52 thf(zip_derived_cl121, plain,
% 96.93/14.52 (![X0 : $i, X1 : $i]:
% 96.93/14.52 (~ (aElement0 @ X0)
% 96.93/14.52 | (aElementOf0 @ (sdtasdt0 @ X0 @ X1) @ xI)
% 96.93/14.52 | ~ (aElementOf0 @ X1 @ xI))),
% 96.93/14.52 inference('cnf', [status(esa)], [m__2174])).
% 96.93/14.52 thf(zip_derived_cl2744, plain,
% 96.93/14.52 (![X0 : $i, X1 : $i]:
% 96.93/14.52 ( (aElementOf0 @ (sdtasdt0 @ X1 @ X0) @ xI)
% 96.93/14.52 | ~ (aElement0 @ X1)
% 96.93/14.52 | ~ (aElement0 @ X0)
% 96.93/14.52 | ~ (aElementOf0 @ X1 @ xI)
% 96.93/14.52 | ~ (aElement0 @ X0))),
% 96.93/14.52 inference('sup+', [status(thm)], [zip_derived_cl12, zip_derived_cl121])).
% 96.93/14.52 thf(zip_derived_cl2777, plain,
% 96.93/14.52 (![X0 : $i, X1 : $i]:
% 96.93/14.52 (~ (aElementOf0 @ X1 @ xI)
% 96.93/14.52 | ~ (aElement0 @ X0)
% 96.93/14.52 | ~ (aElement0 @ X1)
% 96.93/14.52 | (aElementOf0 @ (sdtasdt0 @ X1 @ X0) @ xI))),
% 96.93/14.52 inference('simplify', [status(thm)], [zip_derived_cl2744])).
% 96.93/14.52 thf(zip_derived_cl80247, plain,
% 96.93/14.52 (( (aElementOf0 @ xc @ xI)
% 96.93/14.52 | ~ (aElement0 @ xu)
% 96.93/14.52 | ~ (aElement0 @ (sk__20 @ xu))
% 96.93/14.52 | ~ (aElementOf0 @ xu @ xI))),
% 96.93/14.52 inference('sup+', [status(thm)], [zip_derived_cl5658, zip_derived_cl2777])).
% 96.93/14.52 thf(m__, conjecture,
% 96.93/14.52 (( ![W0:$i]:
% 96.93/14.52 ( ( aElementOf0 @ W0 @ ( slsdtgt0 @ xa ) ) <=>
% 96.93/14.52 ( ?[W1:$i]:
% 96.93/14.52 ( ( aElement0 @ W1 ) & ( ( sdtasdt0 @ xa @ W1 ) = ( W0 ) ) ) ) ) ) =>
% 96.93/14.52 ( ( ![W0:$i]:
% 96.93/14.52 ( ( aElementOf0 @ W0 @ ( slsdtgt0 @ xb ) ) <=>
% 96.93/14.52 ( ?[W1:$i]:
% 96.93/14.52 ( ( aElement0 @ W1 ) & ( ( sdtasdt0 @ xb @ W1 ) = ( W0 ) ) ) ) ) ) =>
% 96.93/14.52 ( ( aElementOf0 @
% 96.93/14.52 xc @ ( sdtpldt1 @ ( slsdtgt0 @ xa ) @ ( slsdtgt0 @ xb ) ) ) |
% 96.93/14.52 ( ?[W0:$i,W1:$i]:
% 96.93/14.52 ( ( aElementOf0 @ W0 @ ( slsdtgt0 @ xa ) ) &
% 96.93/14.52 ( aElementOf0 @ W1 @ ( slsdtgt0 @ xb ) ) &
% 96.93/14.52 ( ( sdtpldt0 @ W0 @ W1 ) = ( xc ) ) ) ) ) ))).
% 96.93/14.52 thf(zf_stmt_11, type, zip_tseitin_11 : $i > $i > $o).
% 96.93/14.52 thf(zf_stmt_12, axiom,
% 96.93/14.52 (![W1:$i,W0:$i]:
% 96.93/14.52 ( ( zip_tseitin_11 @ W1 @ W0 ) <=>
% 96.93/14.52 ( ( ( sdtasdt0 @ xb @ W1 ) = ( W0 ) ) & ( aElement0 @ W1 ) ) ))).
% 96.93/14.52 thf(zf_stmt_13, type, zip_tseitin_10 : $i > $i > $o).
% 96.93/14.52 thf(zf_stmt_14, axiom,
% 96.93/14.52 (![W1:$i,W0:$i]:
% 96.93/14.52 ( ( zip_tseitin_10 @ W1 @ W0 ) <=>
% 96.93/14.52 ( ( ( sdtasdt0 @ xa @ W1 ) = ( W0 ) ) & ( aElement0 @ W1 ) ) ))).
% 96.93/14.52 thf(zf_stmt_15, conjecture,
% 96.93/14.52 (( ![W0:$i]:
% 96.93/14.52 ( ( aElementOf0 @ W0 @ ( slsdtgt0 @ xa ) ) <=>
% 96.93/14.52 ( ?[W1:$i]: ( zip_tseitin_10 @ W1 @ W0 ) ) ) ) =>
% 96.93/14.52 ( ( ![W0:$i]:
% 96.93/14.52 ( ( aElementOf0 @ W0 @ ( slsdtgt0 @ xb ) ) <=>
% 96.93/14.52 ( ?[W1:$i]: ( zip_tseitin_11 @ W1 @ W0 ) ) ) ) =>
% 96.93/14.52 ( ( ?[W0:$i,W1:$i]:
% 96.93/14.52 ( ( ( sdtpldt0 @ W0 @ W1 ) = ( xc ) ) &
% 96.93/14.52 ( aElementOf0 @ W1 @ ( slsdtgt0 @ xb ) ) &
% 96.93/14.52 ( aElementOf0 @ W0 @ ( slsdtgt0 @ xa ) ) ) ) |
% 96.93/14.52 ( aElementOf0 @
% 96.93/14.52 xc @ ( sdtpldt1 @ ( slsdtgt0 @ xa ) @ ( slsdtgt0 @ xb ) ) ) ) ))).
% 96.93/14.52 thf(zf_stmt_16, negated_conjecture,
% 96.93/14.52 (~( ( ![W0:$i]:
% 96.93/14.52 ( ( aElementOf0 @ W0 @ ( slsdtgt0 @ xa ) ) <=>
% 96.93/14.52 ( ?[W1:$i]: ( zip_tseitin_10 @ W1 @ W0 ) ) ) ) =>
% 96.93/14.52 ( ( ![W0:$i]:
% 96.93/14.52 ( ( aElementOf0 @ W0 @ ( slsdtgt0 @ xb ) ) <=>
% 96.93/14.52 ( ?[W1:$i]: ( zip_tseitin_11 @ W1 @ W0 ) ) ) ) =>
% 96.93/14.52 ( ( ?[W0:$i,W1:$i]:
% 96.93/14.52 ( ( ( sdtpldt0 @ W0 @ W1 ) = ( xc ) ) &
% 96.93/14.52 ( aElementOf0 @ W1 @ ( slsdtgt0 @ xb ) ) &
% 96.93/14.52 ( aElementOf0 @ W0 @ ( slsdtgt0 @ xa ) ) ) ) |
% 96.93/14.52 ( aElementOf0 @
% 96.93/14.52 xc @ ( sdtpldt1 @ ( slsdtgt0 @ xa ) @ ( slsdtgt0 @ xb ) ) ) ) ) )),
% 96.93/14.52 inference('cnf.neg', [status(esa)], [zf_stmt_15])).
% 96.93/14.52 thf(zip_derived_cl182, plain,
% 96.93/14.52 (~ (aElementOf0 @ xc @ (sdtpldt1 @ (slsdtgt0 @ xa) @ (slsdtgt0 @ xb)))),
% 96.93/14.52 inference('cnf', [status(esa)], [zf_stmt_16])).
% 96.93/14.52 thf(zip_derived_cl133, plain,
% 96.93/14.52 (((xI) = (sdtpldt1 @ (slsdtgt0 @ xa) @ (slsdtgt0 @ xb)))),
% 96.93/14.52 inference('cnf', [status(esa)], [m__2174])).
% 96.93/14.52 thf(zip_derived_cl1087, plain, (~ (aElementOf0 @ xc @ xI)),
% 96.93/14.52 inference('demod', [status(thm)], [zip_derived_cl182, zip_derived_cl133])).
% 96.93/14.52 thf(mEOfElem, axiom,
% 96.93/14.52 (![W0:$i]:
% 96.93/14.52 ( ( aSet0 @ W0 ) =>
% 96.93/14.52 ( ![W1:$i]: ( ( aElementOf0 @ W1 @ W0 ) => ( aElement0 @ W1 ) ) ) ))).
% 96.93/14.52 thf(zip_derived_cl25, plain,
% 96.93/14.52 (![X0 : $i, X1 : $i]:
% 96.93/14.52 (~ (aElementOf0 @ X0 @ X1) | (aElement0 @ X0) | ~ (aSet0 @ X1))),
% 96.93/14.52 inference('cnf', [status(esa)], [mEOfElem])).
% 96.93/14.52 thf(m__2273, axiom,
% 96.93/14.52 (( ![W0:$i]:
% 96.93/14.52 ( ( ( ( ?[W1:$i,W2:$i]:
% 96.93/14.52 ( ( ( sdtpldt0 @ W1 @ W2 ) = ( W0 ) ) &
% 96.93/14.52 ( aElementOf0 @ W2 @ ( slsdtgt0 @ xb ) ) &
% 96.93/14.52 ( aElementOf0 @ W1 @ ( slsdtgt0 @ xa ) ) ) ) |
% 96.93/14.52 ( aElementOf0 @ W0 @ xI ) ) &
% 96.93/14.52 ( ( W0 ) != ( sz00 ) ) ) =>
% 96.93/14.52 ( ~( iLess0 @ ( sbrdtbr0 @ W0 ) @ ( sbrdtbr0 @ xu ) ) ) ) ) &
% 96.93/14.52 ( ( xu ) != ( sz00 ) ) & ( aElementOf0 @ xu @ xI ) &
% 96.93/14.52 ( ?[W0:$i,W1:$i]:
% 96.93/14.52 ( ( ( sdtpldt0 @ W0 @ W1 ) = ( xu ) ) &
% 96.93/14.52 ( aElementOf0 @ W1 @ ( slsdtgt0 @ xb ) ) &
% 96.93/14.52 ( aElementOf0 @ W0 @ ( slsdtgt0 @ xa ) ) ) ))).
% 96.93/14.52 thf(zip_derived_cl160, plain, ( (aElementOf0 @ xu @ xI)),
% 96.93/14.52 inference('cnf', [status(esa)], [m__2273])).
% 96.93/14.52 thf(zip_derived_cl1105, plain, ((~ (aSet0 @ xI) | (aElement0 @ xu))),
% 96.93/14.52 inference('sup+', [status(thm)], [zip_derived_cl25, zip_derived_cl160])).
% 96.93/14.52 thf(zip_derived_cl119, plain, ( (aSet0 @ xI)),
% 96.93/14.52 inference('cnf', [status(esa)], [m__2174])).
% 96.93/14.52 thf(zip_derived_cl1106, plain, ( (aElement0 @ xu)),
% 96.93/14.52 inference('demod', [status(thm)], [zip_derived_cl1105, zip_derived_cl119])).
% 96.93/14.52 thf(zip_derived_cl167, plain, ( (aDivisorOf0 @ xu @ xa)),
% 96.93/14.52 inference('cnf', [status(esa)], [m__2373])).
% 96.93/14.52 thf(zip_derived_cl98, plain,
% 96.93/14.52 (![X0 : $i]: ( (zip_tseitin_5 @ X0) | ~ (doDivides0 @ X0 @ xb))),
% 96.93/14.52 inference('cnf', [status(esa)], [zf_stmt_0])).
% 96.93/14.52 thf(zip_derived_cl997, plain,
% 96.93/14.52 (![X0 : $i]:
% 96.93/14.52 (~ (aDivisorOf0 @ X0 @ xa)
% 96.93/14.52 | ~ (zip_tseitin_5 @ X0)
% 96.93/14.52 | (zip_tseitin_9 @ X0))),
% 96.93/14.52 inference('dp-resolution', [status(thm)],
% 96.93/14.52 [zip_derived_cl103, zip_derived_cl115])).
% 96.93/14.52 thf(zip_derived_cl106, plain,
% 96.93/14.52 (![X0 : $i]:
% 96.93/14.52 ( (zip_tseitin_8 @ (sk__20 @ X0) @ X0) | ~ (zip_tseitin_9 @ X0))),
% 96.93/14.52 inference('cnf', [status(esa)], [zf_stmt_3])).
% 96.93/14.52 thf(zip_derived_cl105, plain,
% 96.93/14.52 (![X0 : $i, X1 : $i]: ( (aElement0 @ X0) | ~ (zip_tseitin_8 @ X0 @ X1))),
% 96.93/14.52 inference('cnf', [status(esa)], [zf_stmt_5])).
% 96.93/14.52 thf(zip_derived_cl995, plain,
% 96.93/14.52 (![X0 : $i]: (~ (zip_tseitin_9 @ X0) | (aElement0 @ (sk__20 @ X0)))),
% 96.93/14.52 inference('dp-resolution', [status(thm)],
% 96.93/14.52 [zip_derived_cl106, zip_derived_cl105])).
% 96.93/14.52 thf(zip_derived_cl1031, plain,
% 96.93/14.52 (![X0 : $i]:
% 96.93/14.52 (~ (zip_tseitin_5 @ X0)
% 96.93/14.52 | ~ (aDivisorOf0 @ X0 @ xa)
% 96.93/14.52 | (aElement0 @ (sk__20 @ X0)))),
% 96.93/14.52 inference('dp-resolution', [status(thm)],
% 96.93/14.52 [zip_derived_cl997, zip_derived_cl995])).
% 96.93/14.52 thf(zip_derived_cl1069, plain,
% 96.93/14.52 (![X0 : $i]:
% 96.93/14.52 (~ (doDivides0 @ X0 @ xb)
% 96.93/14.52 | (aElement0 @ (sk__20 @ X0))
% 96.93/14.52 | ~ (aDivisorOf0 @ X0 @ xa))),
% 96.93/14.52 inference('dp-resolution', [status(thm)],
% 96.93/14.52 [zip_derived_cl98, zip_derived_cl1031])).
% 96.93/14.52 thf(zip_derived_cl1380, plain,
% 96.93/14.52 (( (aElement0 @ (sk__20 @ xu)) | ~ (doDivides0 @ xu @ xb))),
% 96.93/14.52 inference('sup-', [status(thm)], [zip_derived_cl167, zip_derived_cl1069])).
% 96.93/14.52 thf(zip_derived_cl170, plain, ( (doDivides0 @ xu @ xb)),
% 96.93/14.52 inference('cnf', [status(esa)], [m__2373])).
% 96.93/14.52 thf(zip_derived_cl1382, plain, ( (aElement0 @ (sk__20 @ xu))),
% 96.93/14.52 inference('demod', [status(thm)], [zip_derived_cl1380, zip_derived_cl170])).
% 96.93/14.52 thf(zip_derived_cl160, plain, ( (aElementOf0 @ xu @ xI)),
% 96.93/14.52 inference('cnf', [status(esa)], [m__2273])).
% 96.93/14.52 thf(zip_derived_cl80479, plain, ($false),
% 96.93/14.52 inference('demod', [status(thm)],
% 96.93/14.52 [zip_derived_cl80247, zip_derived_cl1087, zip_derived_cl1106,
% 96.93/14.52 zip_derived_cl1382, zip_derived_cl160])).
% 96.93/14.52
% 96.93/14.52 % SZS output end Refutation
% 96.93/14.52
% 96.93/14.52
% 96.93/14.52 % Terminating...
% 96.93/14.60 % Runner terminated.
% 96.93/14.60 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------