%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : RNG092+1 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.X8Dg1SCZCp true
% Computer : n001.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:30 PM UTC 2025
% Result : Theorem 0.54s 0.92s
% Output : Refutation 0.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : RNG092+1 : TPTP v9.2.0. Released v4.0.0.
% 0.10/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.X8Dg1SCZCp true
% 0.13/0.34 % Computer : n001.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 17:21:08 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % Running portfolio for 300 s
% 0.13/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.34 % Number of cores: 8
% 0.13/0.34 % Python version: Python 3.6.8
% 0.13/0.35 % Running in FO mode
% 0.52/0.62 % Total configuration time : 435
% 0.52/0.62 % Estimated wc time : 1092
% 0.52/0.62 % Estimated cpu time (7 cpus) : 156.0
% 0.52/0.67 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.53/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.53/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.53/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.53/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.53/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.53/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.54/0.92 % Solved by fo/fo13.sh.
% 0.54/0.92 % done 211 iterations in 0.170s
% 0.54/0.92 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.54/0.92 % SZS output start Refutation
% 0.54/0.92 thf(sdtasdt0_type, type, sdtasdt0: $i > $i > $i).
% 0.54/0.92 thf(aElement0_type, type, aElement0: $i > $o).
% 0.54/0.92 thf(sdtpldt1_type, type, sdtpldt1: $i > $i > $i).
% 0.54/0.92 thf(sk__9_type, type, sk__9: $i > $i).
% 0.54/0.92 thf(xI_type, type, xI: $i).
% 0.54/0.92 thf(xJ_type, type, xJ: $i).
% 0.54/0.92 thf(sz00_type, type, sz00: $i).
% 0.54/0.92 thf(sk__10_type, type, sk__10: $i > $i).
% 0.54/0.92 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 0.54/0.92 thf(aIdeal0_type, type, aIdeal0: $i > $o).
% 0.54/0.92 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $i > $i > $i > $o).
% 0.54/0.92 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 0.54/0.92 thf(sk__8_type, type, sk__8: $i > $i).
% 0.54/0.92 thf(aSet0_type, type, aSet0: $i > $o).
% 0.54/0.92 thf(mDefSSum, axiom,
% 0.54/0.92 (![W0:$i,W1:$i]:
% 0.54/0.92 ( ( ( aSet0 @ W1 ) & ( aSet0 @ W0 ) ) =>
% 0.54/0.92 ( ![W2:$i]:
% 0.54/0.92 ( ( ( W2 ) = ( sdtpldt1 @ W0 @ W1 ) ) <=>
% 0.54/0.92 ( ( ![W3:$i]:
% 0.54/0.92 ( ( aElementOf0 @ W3 @ W2 ) <=>
% 0.54/0.92 ( ?[W4:$i,W5:$i]:
% 0.54/0.92 ( ( aElementOf0 @ W4 @ W0 ) & ( aElementOf0 @ W5 @ W1 ) &
% 0.54/0.92 ( ( sdtpldt0 @ W4 @ W5 ) = ( W3 ) ) ) ) ) ) &
% 0.54/0.92 ( aSet0 @ W2 ) ) ) ) ))).
% 0.54/0.92 thf(zf_stmt_0, type, zip_tseitin_2 : $i > $i > $i > $i > $i > $o).
% 0.54/0.92 thf(zf_stmt_1, axiom,
% 0.54/0.92 (![W5:$i,W4:$i,W3:$i,W1:$i,W0:$i]:
% 0.54/0.92 ( ( zip_tseitin_2 @ W5 @ W4 @ W3 @ W1 @ W0 ) <=>
% 0.54/0.92 ( ( ( sdtpldt0 @ W4 @ W5 ) = ( W3 ) ) & ( aElementOf0 @ W5 @ W1 ) &
% 0.54/0.92 ( aElementOf0 @ W4 @ W0 ) ) ))).
% 0.54/0.92 thf(zf_stmt_2, axiom,
% 0.54/0.92 (![W0:$i,W1:$i]:
% 0.54/0.92 ( ( ( aSet0 @ W0 ) & ( aSet0 @ W1 ) ) =>
% 0.54/0.92 ( ![W2:$i]:
% 0.54/0.92 ( ( ( W2 ) = ( sdtpldt1 @ W0 @ W1 ) ) <=>
% 0.54/0.92 ( ( aSet0 @ W2 ) &
% 0.54/0.92 ( ![W3:$i]:
% 0.54/0.92 ( ( aElementOf0 @ W3 @ W2 ) <=>
% 0.54/0.92 ( ?[W4:$i,W5:$i]: ( zip_tseitin_2 @ W5 @ W4 @ W3 @ W1 @ W0 ) ) ) ) ) ) ) ))).
% 0.54/0.92 thf(zip_derived_cl35, plain,
% 0.54/0.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.92 (~ (aSet0 @ X0)
% 0.54/0.92 | ~ (aSet0 @ X1)
% 0.54/0.92 | (aSet0 @ X2)
% 0.54/0.92 | ((X2) != (sdtpldt1 @ X0 @ X1)))),
% 0.54/0.92 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.54/0.92 thf(zip_derived_cl166, plain,
% 0.54/0.92 (![X0 : $i, X1 : $i]:
% 0.54/0.92 ( (aSet0 @ (sdtpldt1 @ X1 @ X0)) | ~ (aSet0 @ X0) | ~ (aSet0 @ X1))),
% 0.54/0.92 inference('eq_res', [status(thm)], [zip_derived_cl35])).
% 0.54/0.92 thf(mDefIdeal, axiom,
% 0.54/0.92 (![W0:$i]:
% 0.54/0.92 ( ( aIdeal0 @ W0 ) <=>
% 0.54/0.92 ( ( aSet0 @ W0 ) &
% 0.54/0.92 ( ![W1:$i]:
% 0.54/0.92 ( ( aElementOf0 @ W1 @ W0 ) =>
% 0.54/0.92 ( ( ![W2:$i]:
% 0.54/0.92 ( ( aElementOf0 @ W2 @ W0 ) =>
% 0.54/0.92 ( aElementOf0 @ ( sdtpldt0 @ W1 @ W2 ) @ W0 ) ) ) &
% 0.54/0.92 ( ![W2:$i]:
% 0.54/0.92 ( ( aElement0 @ W2 ) =>
% 0.54/0.92 ( aElementOf0 @ ( sdtasdt0 @ W2 @ W1 ) @ W0 ) ) ) ) ) ) ) ))).
% 0.54/0.92 thf(zip_derived_cl50, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 ( (aIdeal0 @ X0) | (aElementOf0 @ (sk__8 @ X0) @ X0) | ~ (aSet0 @ X0))),
% 0.54/0.92 inference('cnf', [status(esa)], [mDefIdeal])).
% 0.54/0.92 thf(zip_derived_cl166, plain,
% 0.54/0.92 (![X0 : $i, X1 : $i]:
% 0.54/0.92 ( (aSet0 @ (sdtpldt1 @ X1 @ X0)) | ~ (aSet0 @ X0) | ~ (aSet0 @ X1))),
% 0.54/0.92 inference('eq_res', [status(thm)], [zip_derived_cl35])).
% 0.54/0.92 thf(zip_derived_cl54, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 ( (aIdeal0 @ X0)
% 0.54/0.92 | (aElement0 @ (sk__10 @ X0))
% 0.54/0.92 | (aElementOf0 @ (sk__9 @ X0) @ X0)
% 0.54/0.92 | ~ (aSet0 @ X0))),
% 0.54/0.92 inference('cnf', [status(esa)], [mDefIdeal])).
% 0.54/0.92 thf(zip_derived_cl166, plain,
% 0.54/0.92 (![X0 : $i, X1 : $i]:
% 0.54/0.92 ( (aSet0 @ (sdtpldt1 @ X1 @ X0)) | ~ (aSet0 @ X0) | ~ (aSet0 @ X1))),
% 0.54/0.92 inference('eq_res', [status(thm)], [zip_derived_cl35])).
% 0.54/0.92 thf(zip_derived_cl166, plain,
% 0.54/0.92 (![X0 : $i, X1 : $i]:
% 0.54/0.92 ( (aSet0 @ (sdtpldt1 @ X1 @ X0)) | ~ (aSet0 @ X0) | ~ (aSet0 @ X1))),
% 0.54/0.92 inference('eq_res', [status(thm)], [zip_derived_cl35])).
% 0.54/0.92 thf(zip_derived_cl50, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 ( (aIdeal0 @ X0) | (aElementOf0 @ (sk__8 @ X0) @ X0) | ~ (aSet0 @ X0))),
% 0.54/0.92 inference('cnf', [status(esa)], [mDefIdeal])).
% 0.54/0.92 thf(zip_derived_cl166, plain,
% 0.54/0.92 (![X0 : $i, X1 : $i]:
% 0.54/0.92 ( (aSet0 @ (sdtpldt1 @ X1 @ X0)) | ~ (aSet0 @ X0) | ~ (aSet0 @ X1))),
% 0.54/0.92 inference('eq_res', [status(thm)], [zip_derived_cl35])).
% 0.54/0.92 thf(zip_derived_cl166, plain,
% 0.54/0.92 (![X0 : $i, X1 : $i]:
% 0.54/0.92 ( (aSet0 @ (sdtpldt1 @ X1 @ X0)) | ~ (aSet0 @ X0) | ~ (aSet0 @ X1))),
% 0.54/0.92 inference('eq_res', [status(thm)], [zip_derived_cl35])).
% 0.54/0.92 thf(zip_derived_cl50, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 ( (aIdeal0 @ X0) | (aElementOf0 @ (sk__8 @ X0) @ X0) | ~ (aSet0 @ X0))),
% 0.54/0.92 inference('cnf', [status(esa)], [mDefIdeal])).
% 0.54/0.92 thf(m__, conjecture,
% 0.54/0.92 (( ![W0:$i,W1:$i,W2:$i]:
% 0.54/0.92 ( ( ( aElementOf0 @ W0 @ ( sdtpldt1 @ xI @ xJ ) ) &
% 0.54/0.92 ( aElementOf0 @ W1 @ ( sdtpldt1 @ xI @ xJ ) ) & ( aElement0 @ W2 ) ) =>
% 0.54/0.92 ( ?[W3:$i,W4:$i]:
% 0.54/0.92 ( ( ?[W5:$i,W6:$i]:
% 0.54/0.92 ( ( aElementOf0 @
% 0.54/0.92 ( sdtasdt0 @ W2 @ W0 ) @ ( sdtpldt1 @ xI @ xJ ) ) &
% 0.54/0.92 ( aElementOf0 @
% 0.54/0.92 ( sdtpldt0 @ W0 @ W1 ) @ ( sdtpldt1 @ xI @ xJ ) ) &
% 0.54/0.92 ( ( sdtpldt0 @ W0 @ W1 ) =
% 0.54/0.92 ( sdtpldt0 @ ( sdtpldt0 @ W3 @ W5 ) @ ( sdtpldt0 @ W4 @ W6 ) ) ) &
% 0.54/0.92 ( aElementOf0 @ ( sdtasdt0 @ W2 @ W4 ) @ xJ ) &
% 0.54/0.92 ( aElementOf0 @ ( sdtasdt0 @ W2 @ W3 ) @ xI ) &
% 0.54/0.92 ( aElementOf0 @ ( sdtpldt0 @ W4 @ W6 ) @ xJ ) &
% 0.54/0.92 ( aElementOf0 @ ( sdtpldt0 @ W3 @ W5 ) @ xI ) &
% 0.54/0.92 ( ( W1 ) = ( sdtpldt0 @ W5 @ W6 ) ) &
% 0.54/0.92 ( aElementOf0 @ W6 @ xJ ) & ( aElementOf0 @ W5 @ xI ) ) ) &
% 0.54/0.92 ( ( W0 ) = ( sdtpldt0 @ W3 @ W4 ) ) & ( aElementOf0 @ W4 @ xJ ) &
% 0.54/0.92 ( aElementOf0 @ W3 @ xI ) ) ) ) ) =>
% 0.54/0.92 ( aIdeal0 @ ( sdtpldt1 @ xI @ xJ ) ))).
% 0.54/0.92 thf(zf_stmt_3, negated_conjecture,
% 0.54/0.92 (~( ( ![W0:$i,W1:$i,W2:$i]:
% 0.54/0.92 ( ( ( aElementOf0 @ W0 @ ( sdtpldt1 @ xI @ xJ ) ) &
% 0.54/0.92 ( aElementOf0 @ W1 @ ( sdtpldt1 @ xI @ xJ ) ) &
% 0.54/0.92 ( aElement0 @ W2 ) ) =>
% 0.54/0.92 ( ?[W3:$i,W4:$i]:
% 0.54/0.92 ( ( ?[W5:$i,W6:$i]:
% 0.54/0.92 ( ( aElementOf0 @
% 0.54/0.92 ( sdtasdt0 @ W2 @ W0 ) @ ( sdtpldt1 @ xI @ xJ ) ) &
% 0.54/0.92 ( aElementOf0 @
% 0.54/0.92 ( sdtpldt0 @ W0 @ W1 ) @ ( sdtpldt1 @ xI @ xJ ) ) &
% 0.54/0.92 ( ( sdtpldt0 @ W0 @ W1 ) =
% 0.54/0.92 ( sdtpldt0 @
% 0.54/0.92 ( sdtpldt0 @ W3 @ W5 ) @ ( sdtpldt0 @ W4 @ W6 ) ) ) &
% 0.54/0.92 ( aElementOf0 @ ( sdtasdt0 @ W2 @ W4 ) @ xJ ) &
% 0.54/0.92 ( aElementOf0 @ ( sdtasdt0 @ W2 @ W3 ) @ xI ) &
% 0.54/0.92 ( aElementOf0 @ ( sdtpldt0 @ W4 @ W6 ) @ xJ ) &
% 0.54/0.92 ( aElementOf0 @ ( sdtpldt0 @ W3 @ W5 ) @ xI ) &
% 0.54/0.92 ( ( W1 ) = ( sdtpldt0 @ W5 @ W6 ) ) &
% 0.54/0.92 ( aElementOf0 @ W6 @ xJ ) & ( aElementOf0 @ W5 @ xI ) ) ) &
% 0.54/0.92 ( ( W0 ) = ( sdtpldt0 @ W3 @ W4 ) ) &
% 0.54/0.92 ( aElementOf0 @ W4 @ xJ ) & ( aElementOf0 @ W3 @ xI ) ) ) ) ) =>
% 0.54/0.92 ( aIdeal0 @ ( sdtpldt1 @ xI @ xJ ) ) )),
% 0.54/0.92 inference('cnf.neg', [status(esa)], [m__])).
% 0.54/0.92 thf(zip_derived_cl60, plain,
% 0.54/0.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.92 (~ (aElementOf0 @ X0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElementOf0 @ X1 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X2)
% 0.54/0.92 | (aElementOf0 @ (sdtasdt0 @ X2 @ X1) @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.54/0.92 thf(zip_derived_cl71, plain,
% 0.54/0.92 (![X0 : $i, X1 : $i]:
% 0.54/0.92 ( (aElementOf0 @ (sdtasdt0 @ X1 @ X0) @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElementOf0 @ X0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X1))),
% 0.54/0.92 inference('condensation', [status(thm)], [zip_derived_cl60])).
% 0.54/0.92 thf(zip_derived_cl429, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 (~ (aSet0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | (aIdeal0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | (aElementOf0 @ (sdtasdt0 @ X0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ))) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X0))),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl71])).
% 0.54/0.92 thf(zip_derived_cl70, plain, (~ (aIdeal0 @ (sdtpldt1 @ xI @ xJ))),
% 0.54/0.92 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.54/0.92 thf(zip_derived_cl438, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 (~ (aSet0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | (aElementOf0 @ (sdtasdt0 @ X0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ))) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X0))),
% 0.54/0.92 inference('demod', [status(thm)], [zip_derived_cl429, zip_derived_cl70])).
% 0.54/0.92 thf(zip_derived_cl472, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 (~ (aSet0 @ xI)
% 0.54/0.92 | ~ (aSet0 @ xJ)
% 0.54/0.92 | (aElementOf0 @ (sdtasdt0 @ X0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ))) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X0))),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl166, zip_derived_cl438])).
% 0.54/0.92 thf(m__870, axiom, (( aIdeal0 @ xJ ) & ( aIdeal0 @ xI ))).
% 0.54/0.92 thf(zip_derived_cl56, plain, ( (aIdeal0 @ xI)),
% 0.54/0.92 inference('cnf', [status(esa)], [m__870])).
% 0.54/0.92 thf(zip_derived_cl47, plain,
% 0.54/0.92 (![X0 : $i]: ( (aSet0 @ X0) | ~ (aIdeal0 @ X0))),
% 0.54/0.92 inference('cnf', [status(esa)], [mDefIdeal])).
% 0.54/0.92 thf(zip_derived_cl73, plain, ( (aSet0 @ xI)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl56, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl55, plain, ( (aIdeal0 @ xJ)),
% 0.54/0.92 inference('cnf', [status(esa)], [m__870])).
% 0.54/0.92 thf(zip_derived_cl47, plain,
% 0.54/0.92 (![X0 : $i]: ( (aSet0 @ X0) | ~ (aIdeal0 @ X0))),
% 0.54/0.92 inference('cnf', [status(esa)], [mDefIdeal])).
% 0.54/0.92 thf(zip_derived_cl72, plain, ( (aSet0 @ xJ)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl55, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl475, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 ( (aElementOf0 @ (sdtasdt0 @ X0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ))) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X0))),
% 0.54/0.92 inference('demod', [status(thm)],
% 0.54/0.92 [zip_derived_cl472, zip_derived_cl73, zip_derived_cl72])).
% 0.54/0.92 thf(zip_derived_cl51, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 ( (aIdeal0 @ X0)
% 0.54/0.92 | ~ (aElementOf0 @ (sdtasdt0 @ (sk__10 @ X0) @ (sk__8 @ X0)) @ X0)
% 0.54/0.92 | ~ (aElementOf0 @ (sdtpldt0 @ (sk__8 @ X0) @ (sk__9 @ X0)) @ X0)
% 0.54/0.92 | ~ (aSet0 @ X0))),
% 0.54/0.92 inference('cnf', [status(esa)], [mDefIdeal])).
% 0.54/0.92 thf(zip_derived_cl514, plain,
% 0.54/0.92 ((~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ)))
% 0.54/0.92 | (aIdeal0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElementOf0 @
% 0.54/0.92 (sdtpldt0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sk__9 @ (sdtpldt1 @ xI @ xJ))) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aSet0 @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl475, zip_derived_cl51])).
% 0.54/0.92 thf(zip_derived_cl70, plain, (~ (aIdeal0 @ (sdtpldt1 @ xI @ xJ))),
% 0.54/0.92 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.54/0.92 thf(zip_derived_cl528, plain,
% 0.54/0.92 ((~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ)))
% 0.54/0.92 | ~ (aElementOf0 @
% 0.54/0.92 (sdtpldt0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sk__9 @ (sdtpldt1 @ xI @ xJ))) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aSet0 @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('demod', [status(thm)], [zip_derived_cl514, zip_derived_cl70])).
% 0.54/0.92 thf(zip_derived_cl533, plain,
% 0.54/0.92 ((~ (aSet0 @ xI)
% 0.54/0.92 | ~ (aSet0 @ xJ)
% 0.54/0.92 | ~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ)))
% 0.54/0.92 | ~ (aElementOf0 @
% 0.54/0.92 (sdtpldt0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sk__9 @ (sdtpldt1 @ xI @ xJ))) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl166, zip_derived_cl528])).
% 0.54/0.92 thf(zip_derived_cl73, plain, ( (aSet0 @ xI)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl56, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl72, plain, ( (aSet0 @ xJ)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl55, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl534, plain,
% 0.54/0.92 ((~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ)))
% 0.54/0.92 | ~ (aElementOf0 @
% 0.54/0.92 (sdtpldt0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sk__9 @ (sdtpldt1 @ xI @ xJ))) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('demod', [status(thm)],
% 0.54/0.92 [zip_derived_cl533, zip_derived_cl73, zip_derived_cl72])).
% 0.54/0.92 thf(zip_derived_cl61, plain,
% 0.54/0.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.92 (~ (aElementOf0 @ X0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElementOf0 @ X1 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X2)
% 0.54/0.92 | (aElementOf0 @ (sdtpldt0 @ X1 @ X0) @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.54/0.92 thf(zip_derived_cl941, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 (~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ)))
% 0.54/0.92 | ~ (aElementOf0 @ (sk__9 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElementOf0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X0))),
% 0.54/0.92 inference('s_sup+', [status(thm)], [zip_derived_cl534, zip_derived_cl61])).
% 0.54/0.92 thf(zip_derived_cl986, plain,
% 0.54/0.92 ((~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ)))
% 0.54/0.92 | ~ (aElementOf0 @ (sk__9 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElementOf0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('condensation', [status(thm)], [zip_derived_cl941])).
% 0.54/0.92 thf(zip_derived_cl166, plain,
% 0.54/0.92 (![X0 : $i, X1 : $i]:
% 0.54/0.92 ( (aSet0 @ (sdtpldt1 @ X1 @ X0)) | ~ (aSet0 @ X0) | ~ (aSet0 @ X1))),
% 0.54/0.92 inference('eq_res', [status(thm)], [zip_derived_cl35])).
% 0.54/0.92 thf(zip_derived_cl475, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 ( (aElementOf0 @ (sdtasdt0 @ X0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ))) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X0))),
% 0.54/0.92 inference('demod', [status(thm)],
% 0.54/0.92 [zip_derived_cl472, zip_derived_cl73, zip_derived_cl72])).
% 0.54/0.92 thf(zip_derived_cl53, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 ( (aIdeal0 @ X0)
% 0.54/0.92 | ~ (aElementOf0 @ (sdtasdt0 @ (sk__10 @ X0) @ (sk__8 @ X0)) @ X0)
% 0.54/0.92 | (aElementOf0 @ (sk__9 @ X0) @ X0)
% 0.54/0.92 | ~ (aSet0 @ X0))),
% 0.54/0.92 inference('cnf', [status(esa)], [mDefIdeal])).
% 0.54/0.92 thf(zip_derived_cl515, plain,
% 0.54/0.92 ((~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ)))
% 0.54/0.92 | (aIdeal0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | (aElementOf0 @ (sk__9 @ (sdtpldt1 @ xI @ xJ)) @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aSet0 @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl475, zip_derived_cl53])).
% 0.54/0.92 thf(zip_derived_cl70, plain, (~ (aIdeal0 @ (sdtpldt1 @ xI @ xJ))),
% 0.54/0.92 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.54/0.92 thf(zip_derived_cl529, plain,
% 0.54/0.92 ((~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ)))
% 0.54/0.92 | (aElementOf0 @ (sk__9 @ (sdtpldt1 @ xI @ xJ)) @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aSet0 @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('demod', [status(thm)], [zip_derived_cl515, zip_derived_cl70])).
% 0.54/0.92 thf(zip_derived_cl731, plain,
% 0.54/0.92 ((~ (aSet0 @ xI)
% 0.54/0.92 | ~ (aSet0 @ xJ)
% 0.54/0.92 | ~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ)))
% 0.54/0.92 | (aElementOf0 @ (sk__9 @ (sdtpldt1 @ xI @ xJ)) @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl166, zip_derived_cl529])).
% 0.54/0.92 thf(zip_derived_cl73, plain, ( (aSet0 @ xI)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl56, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl72, plain, ( (aSet0 @ xJ)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl55, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl732, plain,
% 0.54/0.92 ((~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ)))
% 0.54/0.92 | (aElementOf0 @ (sk__9 @ (sdtpldt1 @ xI @ xJ)) @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('demod', [status(thm)],
% 0.54/0.92 [zip_derived_cl731, zip_derived_cl73, zip_derived_cl72])).
% 0.54/0.92 thf(zip_derived_cl987, plain,
% 0.54/0.92 ((~ (aElementOf0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ))))),
% 0.54/0.92 inference('clc', [status(thm)], [zip_derived_cl986, zip_derived_cl732])).
% 0.54/0.92 thf(zip_derived_cl997, plain,
% 0.54/0.92 ((~ (aSet0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | (aIdeal0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ))))),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl987])).
% 0.54/0.92 thf(zip_derived_cl70, plain, (~ (aIdeal0 @ (sdtpldt1 @ xI @ xJ))),
% 0.54/0.92 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.54/0.92 thf(zip_derived_cl999, plain,
% 0.54/0.92 ((~ (aSet0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ))))),
% 0.54/0.92 inference('demod', [status(thm)], [zip_derived_cl997, zip_derived_cl70])).
% 0.54/0.92 thf(zip_derived_cl1001, plain,
% 0.54/0.92 ((~ (aSet0 @ xI)
% 0.54/0.92 | ~ (aSet0 @ xJ)
% 0.54/0.92 | ~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ))))),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl166, zip_derived_cl999])).
% 0.54/0.92 thf(zip_derived_cl73, plain, ( (aSet0 @ xI)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl56, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl72, plain, ( (aSet0 @ xJ)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl55, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl1002, plain,
% 0.54/0.92 (~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('demod', [status(thm)],
% 0.54/0.92 [zip_derived_cl1001, zip_derived_cl73, zip_derived_cl72])).
% 0.54/0.92 thf(zip_derived_cl52, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 ( (aIdeal0 @ X0)
% 0.54/0.92 | (aElement0 @ (sk__10 @ X0))
% 0.54/0.92 | ~ (aElementOf0 @ (sdtpldt0 @ (sk__8 @ X0) @ (sk__9 @ X0)) @ X0)
% 0.54/0.92 | ~ (aSet0 @ X0))),
% 0.54/0.92 inference('cnf', [status(esa)], [mDefIdeal])).
% 0.54/0.92 thf(zip_derived_cl1004, plain,
% 0.54/0.92 (( (aIdeal0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElementOf0 @
% 0.54/0.92 (sdtpldt0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sk__9 @ (sdtpldt1 @ xI @ xJ))) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aSet0 @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('s_sup+', [status(thm)], [zip_derived_cl1002, zip_derived_cl52])).
% 0.54/0.92 thf(zip_derived_cl70, plain, (~ (aIdeal0 @ (sdtpldt1 @ xI @ xJ))),
% 0.54/0.92 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.54/0.92 thf(zip_derived_cl1005, plain,
% 0.54/0.92 ((~ (aElementOf0 @
% 0.54/0.92 (sdtpldt0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sk__9 @ (sdtpldt1 @ xI @ xJ))) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aSet0 @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('demod', [status(thm)], [zip_derived_cl1004, zip_derived_cl70])).
% 0.54/0.92 thf(zip_derived_cl1028, plain,
% 0.54/0.92 ((~ (aSet0 @ xI)
% 0.54/0.92 | ~ (aSet0 @ xJ)
% 0.54/0.92 | ~ (aElementOf0 @
% 0.54/0.92 (sdtpldt0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sk__9 @ (sdtpldt1 @ xI @ xJ))) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('s_sup-', [status(thm)],
% 0.54/0.92 [zip_derived_cl166, zip_derived_cl1005])).
% 0.54/0.92 thf(zip_derived_cl73, plain, ( (aSet0 @ xI)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl56, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl72, plain, ( (aSet0 @ xJ)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl55, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl1029, plain,
% 0.54/0.92 (~ (aElementOf0 @
% 0.54/0.92 (sdtpldt0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sk__9 @ (sdtpldt1 @ xI @ xJ))) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))),
% 0.54/0.92 inference('demod', [status(thm)],
% 0.54/0.92 [zip_derived_cl1028, zip_derived_cl73, zip_derived_cl72])).
% 0.54/0.92 thf(zip_derived_cl61, plain,
% 0.54/0.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.92 (~ (aElementOf0 @ X0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElementOf0 @ X1 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X2)
% 0.54/0.92 | (aElementOf0 @ (sdtpldt0 @ X1 @ X0) @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.54/0.92 thf(zip_derived_cl1038, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 (~ (aElementOf0 @ (sk__9 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElementOf0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X0))),
% 0.54/0.92 inference('s_sup+', [status(thm)], [zip_derived_cl1029, zip_derived_cl61])).
% 0.54/0.92 thf(zip_derived_cl1040, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 (~ (aSet0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ)))
% 0.54/0.92 | (aIdeal0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElementOf0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X0))),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl54, zip_derived_cl1038])).
% 0.54/0.92 thf(zip_derived_cl1002, plain,
% 0.54/0.92 (~ (aElement0 @ (sk__10 @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('demod', [status(thm)],
% 0.54/0.92 [zip_derived_cl1001, zip_derived_cl73, zip_derived_cl72])).
% 0.54/0.92 thf(zip_derived_cl70, plain, (~ (aIdeal0 @ (sdtpldt1 @ xI @ xJ))),
% 0.54/0.92 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.54/0.92 thf(zip_derived_cl1041, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 (~ (aSet0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElementOf0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X0))),
% 0.54/0.92 inference('demod', [status(thm)],
% 0.54/0.92 [zip_derived_cl1040, zip_derived_cl1002, zip_derived_cl70])).
% 0.54/0.92 thf(zip_derived_cl1042, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 (~ (aSet0 @ xI)
% 0.54/0.92 | ~ (aSet0 @ xJ)
% 0.54/0.92 | ~ (aElementOf0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X0))),
% 0.54/0.92 inference('s_sup-', [status(thm)],
% 0.54/0.92 [zip_derived_cl166, zip_derived_cl1041])).
% 0.54/0.92 thf(zip_derived_cl73, plain, ( (aSet0 @ xI)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl56, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl72, plain, ( (aSet0 @ xJ)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl55, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl1043, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 (~ (aElementOf0 @ (sk__8 @ (sdtpldt1 @ xI @ xJ)) @
% 0.54/0.92 (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X0))),
% 0.54/0.92 inference('demod', [status(thm)],
% 0.54/0.92 [zip_derived_cl1042, zip_derived_cl73, zip_derived_cl72])).
% 0.54/0.92 thf(zip_derived_cl1044, plain,
% 0.54/0.92 (![X0 : $i]:
% 0.54/0.92 (~ (aSet0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | (aIdeal0 @ (sdtpldt1 @ xI @ xJ))
% 0.54/0.92 | ~ (aElement0 @ X0))),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl1043])).
% 0.54/0.92 thf(zip_derived_cl70, plain, (~ (aIdeal0 @ (sdtpldt1 @ xI @ xJ))),
% 0.54/0.92 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.54/0.92 thf(zip_derived_cl1066, plain,
% 0.54/0.92 (![X0 : $i]: (~ (aElement0 @ X0) | ~ (aSet0 @ (sdtpldt1 @ xI @ xJ)))),
% 0.54/0.92 inference('clc', [status(thm)], [zip_derived_cl1044, zip_derived_cl70])).
% 0.54/0.92 thf(zip_derived_cl1067, plain,
% 0.54/0.92 (![X0 : $i]: (~ (aSet0 @ xI) | ~ (aSet0 @ xJ) | ~ (aElement0 @ X0))),
% 0.54/0.92 inference('s_sup-', [status(thm)],
% 0.54/0.92 [zip_derived_cl166, zip_derived_cl1066])).
% 0.54/0.92 thf(zip_derived_cl73, plain, ( (aSet0 @ xI)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl56, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl72, plain, ( (aSet0 @ xJ)),
% 0.54/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl55, zip_derived_cl47])).
% 0.54/0.92 thf(zip_derived_cl1068, plain, (![X0 : $i]: ~ (aElement0 @ X0)),
% 0.54/0.92 inference('demod', [status(thm)],
% 0.54/0.92 [zip_derived_cl1067, zip_derived_cl73, zip_derived_cl72])).
% 0.54/0.92 thf(mSortsC, axiom, (aElement0 @ sz00)).
% 0.54/0.92 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 0.54/0.92 inference('cnf', [status(esa)], [mSortsC])).
% 0.54/0.92 thf(zip_derived_cl1072, plain, ($false),
% 0.54/0.92 inference('s_sup+', [status(thm)], [zip_derived_cl1068, zip_derived_cl1])).
% 0.54/0.92
% 0.54/0.92 % SZS output end Refutation
% 0.54/0.92
% 0.54/0.92
% 0.54/0.92 % Terminating...
% 0.56/1.05 % Runner terminated.
% 0.56/1.06 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------