%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NUM583+3 : 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.uPrtPNyuYB true
% Computer : n031.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:47:31 PM UTC 2025
% Result : Theorem 3.20s 1.68s
% Output : Refutation 3.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.20 % Problem : NUM583+3 : TPTP v9.2.0. Released v4.0.0.
% 0.06/0.22 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.uPrtPNyuYB true
% 0.13/0.43 % Computer : n031.cluster.edu
% 0.13/0.43 % Model : x86_64 x86_64
% 0.13/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.43 % Memory : 8042.1875MB
% 0.13/0.43 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.43 % CPULimit : 300
% 0.13/0.43 % WCLimit : 300
% 0.13/0.43 % DateTime : Wed Oct 1 16:40:53 EDT 2025
% 0.13/0.44 % CPUTime :
% 0.13/0.44 % Running portfolio for 300 s
% 0.13/0.44 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.44 % Number of cores: 8
% 0.13/0.45 % Python version: Python 3.6.8
% 0.13/0.45 % Running in FO mode
% 0.29/0.71 % Total configuration time : 435
% 0.29/0.71 % Estimated wc time : 1092
% 0.29/0.71 % Estimated cpu time (7 cpus) : 156.0
% 0.31/0.84 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.31/0.92 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.31/1.02 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.31/1.03 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.31/1.03 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.31/1.04 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.31/1.06 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 3.20/1.68 % Solved by fo/fo5.sh.
% 3.20/1.68 % done 490 iterations in 0.505s
% 3.20/1.68 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 3.20/1.68 % SZS output start Refutation
% 3.20/1.68 thf(aSet0_type, type, aSet0: $i > $o).
% 3.20/1.68 thf(slbdtsldtrb0_type, type, slbdtsldtrb0: $i > $i > $i).
% 3.20/1.68 thf(xi_type, type, xi: $i).
% 3.20/1.68 thf(sdtlpdtrp0_type, type, sdtlpdtrp0: $i > $i > $i).
% 3.20/1.68 thf(aElement0_type, type, aElement0: $i > $o).
% 3.20/1.68 thf(sk__30_type, type, sk__30: $i).
% 3.20/1.68 thf(sbrdtbr0_type, type, sbrdtbr0: $i > $i).
% 3.20/1.68 thf(xS_type, type, xS: $i).
% 3.20/1.68 thf(sdtlseqdt0_type, type, sdtlseqdt0: $i > $i > $o).
% 3.20/1.68 thf(sdtmndt0_type, type, sdtmndt0: $i > $i > $i).
% 3.20/1.68 thf(szmzizndt0_type, type, szmzizndt0: $i > $i).
% 3.20/1.68 thf(aSubsetOf0_type, type, aSubsetOf0: $i > $i > $o).
% 3.20/1.68 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 3.20/1.68 thf(xk_type, type, xk: $i).
% 3.20/1.68 thf(zip_tseitin_24_type, type, zip_tseitin_24: $i > $o).
% 3.20/1.68 thf(xK_type, type, xK: $i).
% 3.20/1.68 thf(xN_type, type, xN: $i).
% 3.20/1.68 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 3.20/1.68 thf(xQ_type, type, xQ: $i).
% 3.20/1.68 thf(m__, conjecture,
% 3.20/1.68 (( ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) =>
% 3.20/1.68 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ W0 ) ) ) &
% 3.20/1.68 ( aElementOf0 @
% 3.20/1.68 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ ( sdtlpdtrp0 @ xN @ xi ) ) ) =>
% 3.20/1.68 ( ( ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @
% 3.20/1.68 W0 @
% 3.20/1.68 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) <=>
% 3.20/1.68 ( ( ( ( W0 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) |
% 3.20/1.68 ( aElementOf0 @ W0 @ xQ ) ) &
% 3.20/1.68 ( aElement0 @ W0 ) ) ) ) &
% 3.20/1.68 ( aSet0 @
% 3.20/1.68 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) =>
% 3.20/1.68 ( ( aSubsetOf0 @
% 3.20/1.68 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) @ xS ) |
% 3.20/1.68 ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @
% 3.20/1.68 W0 @
% 3.20/1.68 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) =>
% 3.20/1.68 ( aElementOf0 @ W0 @ xS ) ) ) ) ))).
% 3.20/1.68 thf(zf_stmt_0, type, zip_tseitin_24 : $i > $o).
% 3.20/1.68 thf(zf_stmt_1, axiom,
% 3.20/1.68 (![W0:$i]:
% 3.20/1.68 ( ( zip_tseitin_24 @ W0 ) <=>
% 3.20/1.68 ( ( aElement0 @ W0 ) &
% 3.20/1.68 ( ( aElementOf0 @ W0 @ xQ ) |
% 3.20/1.68 ( ( W0 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) ))).
% 3.20/1.68 thf(zf_stmt_2, conjecture,
% 3.20/1.68 (( ( aElementOf0 @
% 3.20/1.68 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ ( sdtlpdtrp0 @ xN @ xi ) ) &
% 3.20/1.68 ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) =>
% 3.20/1.68 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ W0 ) ) ) ) =>
% 3.20/1.68 ( ( ( aSet0 @
% 3.20/1.68 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) &
% 3.20/1.68 ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @
% 3.20/1.68 W0 @
% 3.20/1.68 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) <=>
% 3.20/1.68 ( zip_tseitin_24 @ W0 ) ) ) ) =>
% 3.20/1.68 ( ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @
% 3.20/1.68 W0 @
% 3.20/1.68 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) =>
% 3.20/1.68 ( aElementOf0 @ W0 @ xS ) ) ) |
% 3.20/1.68 ( aSubsetOf0 @
% 3.20/1.68 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) @ xS ) ) ))).
% 3.20/1.68 thf(zf_stmt_3, negated_conjecture,
% 3.20/1.68 (~( ( ( aElementOf0 @
% 3.20/1.68 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @
% 3.20/1.68 ( sdtlpdtrp0 @ xN @ xi ) ) &
% 3.20/1.68 ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) =>
% 3.20/1.68 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ W0 ) ) ) ) =>
% 3.20/1.68 ( ( ( aSet0 @
% 3.20/1.68 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) &
% 3.20/1.68 ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @
% 3.20/1.68 W0 @
% 3.20/1.68 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) <=>
% 3.20/1.68 ( zip_tseitin_24 @ W0 ) ) ) ) =>
% 3.20/1.68 ( ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @
% 3.20/1.68 W0 @
% 3.20/1.68 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) =>
% 3.20/1.68 ( aElementOf0 @ W0 @ xS ) ) ) |
% 3.20/1.68 ( aSubsetOf0 @
% 3.20/1.68 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) @
% 3.20/1.68 xS ) ) ) )),
% 3.20/1.68 inference('cnf.neg', [status(esa)], [zf_stmt_2])).
% 3.20/1.68 thf(zip_derived_cl274, plain, (~ (aElementOf0 @ sk__30 @ xS)),
% 3.20/1.68 inference('cnf', [status(esa)], [zf_stmt_3])).
% 3.20/1.68 thf(zip_derived_cl275, plain,
% 3.20/1.68 ( (aElementOf0 @ sk__30 @
% 3.20/1.68 (sdtpldt0 @ xQ @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi))))),
% 3.20/1.68 inference('cnf', [status(esa)], [zf_stmt_3])).
% 3.20/1.68 thf(m__4007, axiom,
% 3.20/1.68 (( ( sbrdtbr0 @
% 3.20/1.68 ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) =
% 3.20/1.68 ( xK ) ) &
% 3.20/1.68 ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @
% 3.20/1.68 W0 @ ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) <=>
% 3.20/1.68 ( ( aElement0 @ W0 ) &
% 3.20/1.68 ( ( aElementOf0 @ W0 @ xQ ) |
% 3.20/1.68 ( ( W0 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) ) ) &
% 3.20/1.68 ( aSet0 @ ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) &
% 3.20/1.68 ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) =>
% 3.20/1.68 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ W0 ) ) ) &
% 3.20/1.68 ( aElementOf0 @
% 3.20/1.68 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ ( sdtlpdtrp0 @ xN @ xi ) ))).
% 3.20/1.68 thf(zip_derived_cl263, plain,
% 3.20/1.68 (![X0 : $i]:
% 3.20/1.68 (((X0) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)))
% 3.20/1.68 | (aElementOf0 @ X0 @ xQ)
% 3.20/1.68 | ~ (aElementOf0 @ X0 @
% 3.20/1.68 (sdtpldt0 @ xQ @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)))))),
% 3.20/1.68 inference('cnf', [status(esa)], [m__4007])).
% 3.20/1.68 thf(zip_derived_cl1809, plain,
% 3.20/1.68 (( (aElementOf0 @ sk__30 @ xQ)
% 3.20/1.68 | ((sk__30) = (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi))))),
% 3.20/1.68 inference('sup-', [status(thm)], [zip_derived_cl275, zip_derived_cl263])).
% 3.20/1.68 thf(m__3989_02, axiom,
% 3.20/1.68 (( aElementOf0 @
% 3.20/1.68 xQ @
% 3.20/1.68 ( slbdtsldtrb0 @
% 3.20/1.68 ( sdtmndt0 @
% 3.20/1.68 ( sdtlpdtrp0 @ xN @ xi ) @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) @
% 3.20/1.68 xk ) ) &
% 3.20/1.68 ( ( sbrdtbr0 @ xQ ) = ( xk ) ) &
% 3.20/1.68 ( aSubsetOf0 @
% 3.20/1.68 xQ @
% 3.20/1.68 ( sdtmndt0 @
% 3.20/1.68 ( sdtlpdtrp0 @ xN @ xi ) @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) &
% 3.20/1.68 ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @ W0 @ xQ ) =>
% 3.20/1.68 ( aElementOf0 @
% 3.20/1.68 W0 @
% 3.20/1.68 ( sdtmndt0 @
% 3.20/1.68 ( sdtlpdtrp0 @ xN @ xi ) @
% 3.20/1.68 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) ) &
% 3.20/1.68 ( aSet0 @ xQ ) &
% 3.20/1.68 ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @
% 3.20/1.68 W0 @
% 3.20/1.68 ( sdtmndt0 @
% 3.20/1.68 ( sdtlpdtrp0 @ xN @ xi ) @
% 3.20/1.68 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) <=>
% 3.20/1.68 ( ( aElement0 @ W0 ) &
% 3.20/1.68 ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) &
% 3.20/1.68 ( ( W0 ) != ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) ) &
% 3.20/1.68 ( aSet0 @
% 3.20/1.68 ( sdtmndt0 @
% 3.20/1.68 ( sdtlpdtrp0 @ xN @ xi ) @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) &
% 3.20/1.68 ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) =>
% 3.20/1.68 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ W0 ) ) ) &
% 3.20/1.68 ( aElementOf0 @
% 3.20/1.68 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ ( sdtlpdtrp0 @ xN @ xi ) ))).
% 3.20/1.68 thf(zip_derived_cl245, plain,
% 3.20/1.68 ( (aElementOf0 @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)) @
% 3.20/1.68 (sdtlpdtrp0 @ xN @ xi))),
% 3.20/1.68 inference('cnf', [status(esa)], [m__3989_02])).
% 3.20/1.68 thf(m__4037, axiom,
% 3.20/1.68 (( aSubsetOf0 @ ( sdtlpdtrp0 @ xN @ xi ) @ xS ) &
% 3.20/1.68 ( ![W0:$i]:
% 3.20/1.68 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) =>
% 3.20/1.68 ( aElementOf0 @ W0 @ xS ) ) ))).
% 3.20/1.68 thf(zip_derived_cl265, plain,
% 3.20/1.68 (![X0 : $i]:
% 3.20/1.68 ( (aElementOf0 @ X0 @ xS)
% 3.20/1.68 | ~ (aElementOf0 @ X0 @ (sdtlpdtrp0 @ xN @ xi)))),
% 3.20/1.68 inference('cnf', [status(esa)], [m__4037])).
% 3.20/1.68 thf(zip_derived_cl519, plain,
% 3.20/1.68 ( (aElementOf0 @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)) @ xS)),
% 3.20/1.68 inference('sup-', [status(thm)], [zip_derived_cl245, zip_derived_cl265])).
% 3.20/1.68 thf(zip_derived_cl1838, plain,
% 3.20/1.68 (( (aElementOf0 @ sk__30 @ xS) | (aElementOf0 @ sk__30 @ xQ))),
% 3.20/1.68 inference('sup+', [status(thm)], [zip_derived_cl1809, zip_derived_cl519])).
% 3.20/1.68 thf(zip_derived_cl274, plain, (~ (aElementOf0 @ sk__30 @ xS)),
% 3.20/1.68 inference('cnf', [status(esa)], [zf_stmt_3])).
% 3.20/1.68 thf(zip_derived_cl1851, plain, ( (aElementOf0 @ sk__30 @ xQ)),
% 3.20/1.68 inference('demod', [status(thm)], [zip_derived_cl1838, zip_derived_cl274])).
% 3.20/1.68 thf(zip_derived_cl253, plain,
% 3.20/1.68 (![X0 : $i]:
% 3.20/1.68 ( (aElementOf0 @ X0 @
% 3.20/1.68 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xi) @
% 3.20/1.68 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi))))
% 3.20/1.68 | ~ (aElementOf0 @ X0 @ xQ))),
% 3.20/1.68 inference('cnf', [status(esa)], [m__3989_02])).
% 3.20/1.68 thf(zip_derived_cl1859, plain,
% 3.20/1.68 ( (aElementOf0 @ sk__30 @
% 3.20/1.68 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xi) @
% 3.20/1.68 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi))))),
% 3.20/1.68 inference('sup-', [status(thm)], [zip_derived_cl1851, zip_derived_cl253])).
% 3.20/1.68 thf(zip_derived_cl250, plain,
% 3.20/1.68 (![X0 : $i]:
% 3.20/1.68 ( (aElementOf0 @ X0 @ (sdtlpdtrp0 @ xN @ xi))
% 3.20/1.68 | ~ (aElementOf0 @ X0 @
% 3.20/1.68 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xi) @
% 3.20/1.68 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)))))),
% 3.20/1.68 inference('cnf', [status(esa)], [m__3989_02])).
% 3.20/1.68 thf(zip_derived_cl1983, plain,
% 3.20/1.68 ( (aElementOf0 @ sk__30 @ (sdtlpdtrp0 @ xN @ xi))),
% 3.20/1.68 inference('sup-', [status(thm)], [zip_derived_cl1859, zip_derived_cl250])).
% 3.20/1.68 thf(zip_derived_cl265, plain,
% 3.20/1.68 (![X0 : $i]:
% 3.20/1.68 ( (aElementOf0 @ X0 @ xS)
% 3.20/1.68 | ~ (aElementOf0 @ X0 @ (sdtlpdtrp0 @ xN @ xi)))),
% 3.20/1.68 inference('cnf', [status(esa)], [m__4037])).
% 3.20/1.68 thf(zip_derived_cl1999, plain, ( (aElementOf0 @ sk__30 @ xS)),
% 3.20/1.68 inference('sup-', [status(thm)], [zip_derived_cl1983, zip_derived_cl265])).
% 3.20/1.68 thf(zip_derived_cl2007, plain, ($false),
% 3.20/1.68 inference('demod', [status(thm)], [zip_derived_cl274, zip_derived_cl1999])).
% 3.20/1.68
% 3.20/1.68 % SZS output end Refutation
% 3.20/1.68
% 3.20/1.68
% 3.20/1.68 % Terminating...
% 3.20/1.83 % Runner terminated.
% 3.22/1.84 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------