%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : RNG086+1 : 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.Vl0HnRyGSN true
% Computer : n017.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:28 PM UTC 2025
% Result : Theorem 34.78s 7.99s
% Output : Refutation 34.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : RNG086+1 : TPTP v9.2.0. Released v4.0.0.
% 0.08/0.16 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.Vl0HnRyGSN true
% 0.16/0.37 % Computer : n017.cluster.edu
% 0.16/0.37 % Model : x86_64 x86_64
% 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.37 % Memory : 8042.1875MB
% 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.37 % CPULimit : 300
% 0.16/0.37 % WCLimit : 300
% 0.16/0.37 % DateTime : Wed Oct 1 17:20:38 EDT 2025
% 0.16/0.37 % CPUTime :
% 0.16/0.37 % Running portfolio for 300 s
% 0.16/0.37 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.38 % Number of cores: 8
% 0.16/0.38 % Python version: Python 3.6.8
% 0.16/0.38 % Running in FO mode
% 0.53/0.65 % Total configuration time : 435
% 0.53/0.65 % Estimated wc time : 1092
% 0.53/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.53/0.76 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.53/0.78 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.53/0.79 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.53/0.80 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.53/0.81 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.53/0.82 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.53/0.82 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 34.78/7.99 % Solved by fo/fo13.sh.
% 34.78/7.99 % done 1557 iterations in 7.081s
% 34.78/7.99 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 34.78/7.99 % SZS output start Refutation
% 34.78/7.99 thf(sdtasdt0_type, type, sdtasdt0: $i > $i > $i).
% 34.78/7.99 thf(aElement0_type, type, aElement0: $i > $o).
% 34.78/7.99 thf(xy_type, type, xy: $i).
% 34.78/7.99 thf(sdtpldt1_type, type, sdtpldt1: $i > $i > $i).
% 34.78/7.99 thf(xz_type, type, xz: $i).
% 34.78/7.99 thf(xI_type, type, xI: $i).
% 34.78/7.99 thf(xJ_type, type, xJ: $i).
% 34.78/7.99 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 34.78/7.99 thf(xx_type, type, xx: $i).
% 34.78/7.99 thf(aIdeal0_type, type, aIdeal0: $i > $o).
% 34.78/7.99 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $i > $i > $i > $o).
% 34.78/7.99 thf(sk__5_type, type, sk__5: $i > $i > $i > $i).
% 34.78/7.99 thf(sk__6_type, type, sk__6: $i > $i > $i > $i).
% 34.78/7.99 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 34.78/7.99 thf(aSet0_type, type, aSet0: $i > $o).
% 34.78/7.99 thf(m__901, axiom,
% 34.78/7.99 (( aElement0 @ xz ) & ( aElementOf0 @ xy @ ( sdtpldt1 @ xI @ xJ ) ) &
% 34.78/7.99 ( aElementOf0 @ xx @ ( sdtpldt1 @ xI @ xJ ) ))).
% 34.78/7.99 thf(zip_derived_cl59, plain, ( (aElementOf0 @ xx @ (sdtpldt1 @ xI @ xJ))),
% 34.78/7.99 inference('cnf', [status(esa)], [m__901])).
% 34.78/7.99 thf(mDefSSum, axiom,
% 34.78/7.99 (![W0:$i,W1:$i]:
% 34.78/7.99 ( ( ( aSet0 @ W1 ) & ( aSet0 @ W0 ) ) =>
% 34.78/7.99 ( ![W2:$i]:
% 34.78/7.99 ( ( ( W2 ) = ( sdtpldt1 @ W0 @ W1 ) ) <=>
% 34.78/7.99 ( ( ![W3:$i]:
% 34.78/7.99 ( ( aElementOf0 @ W3 @ W2 ) <=>
% 34.78/7.99 ( ?[W4:$i,W5:$i]:
% 34.78/7.99 ( ( aElementOf0 @ W4 @ W0 ) & ( aElementOf0 @ W5 @ W1 ) &
% 34.78/7.99 ( ( sdtpldt0 @ W4 @ W5 ) = ( W3 ) ) ) ) ) ) &
% 34.78/7.99 ( aSet0 @ W2 ) ) ) ) ))).
% 34.78/7.99 thf(zf_stmt_0, type, zip_tseitin_2 : $i > $i > $i > $i > $i > $o).
% 34.78/7.99 thf(zf_stmt_1, axiom,
% 34.78/7.99 (![W5:$i,W4:$i,W3:$i,W1:$i,W0:$i]:
% 34.78/7.99 ( ( zip_tseitin_2 @ W5 @ W4 @ W3 @ W1 @ W0 ) <=>
% 34.78/7.99 ( ( ( sdtpldt0 @ W4 @ W5 ) = ( W3 ) ) & ( aElementOf0 @ W5 @ W1 ) &
% 34.78/7.99 ( aElementOf0 @ W4 @ W0 ) ) ))).
% 34.78/7.99 thf(zf_stmt_2, axiom,
% 34.78/7.99 (![W0:$i,W1:$i]:
% 34.78/7.99 ( ( ( aSet0 @ W0 ) & ( aSet0 @ W1 ) ) =>
% 34.78/7.99 ( ![W2:$i]:
% 34.78/7.99 ( ( ( W2 ) = ( sdtpldt1 @ W0 @ W1 ) ) <=>
% 34.78/7.99 ( ( aSet0 @ W2 ) &
% 34.78/7.99 ( ![W3:$i]:
% 34.78/7.99 ( ( aElementOf0 @ W3 @ W2 ) <=>
% 34.78/7.99 ( ?[W4:$i,W5:$i]: ( zip_tseitin_2 @ W5 @ W4 @ W3 @ W1 @ W0 ) ) ) ) ) ) ) ))).
% 34.78/7.99 thf(zip_derived_cl36, plain,
% 34.78/7.99 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 34.78/7.99 (~ (aSet0 @ X0)
% 34.78/7.99 | ~ (aSet0 @ X1)
% 34.78/7.99 | ~ (aElementOf0 @ X2 @ X3)
% 34.78/7.99 | (zip_tseitin_2 @ (sk__6 @ X2 @ X1 @ X0) @
% 34.78/7.99 (sk__5 @ X2 @ X1 @ X0) @ X2 @ X1 @ X0)
% 34.78/7.99 | ((X3) != (sdtpldt1 @ X0 @ X1)))),
% 34.78/7.99 inference('cnf', [status(esa)], [zf_stmt_2])).
% 34.78/7.99 thf(zip_derived_cl458, plain,
% 34.78/7.99 (![X0 : $i, X1 : $i, X2 : $i]:
% 34.78/7.99 ( (zip_tseitin_2 @ (sk__6 @ X2 @ X1 @ X0) @ (sk__5 @ X2 @ X1 @ X0) @
% 34.78/7.99 X2 @ X1 @ X0)
% 34.78/7.99 | ~ (aElementOf0 @ X2 @ (sdtpldt1 @ X0 @ X1))
% 34.78/7.99 | ~ (aSet0 @ X1)
% 34.78/7.99 | ~ (aSet0 @ X0))),
% 34.78/7.99 inference('eq_res', [status(thm)], [zip_derived_cl36])).
% 34.78/7.99 thf(zip_derived_cl21602, plain,
% 34.78/7.99 (( (zip_tseitin_2 @ (sk__6 @ xx @ xJ @ xI) @ (sk__5 @ xx @ xJ @ xI) @
% 34.78/7.99 xx @ xJ @ xI)
% 34.78/7.99 | ~ (aSet0 @ xJ)
% 34.78/7.99 | ~ (aSet0 @ xI))),
% 34.78/7.99 inference('s_sup-', [status(thm)], [zip_derived_cl59, zip_derived_cl458])).
% 34.78/7.99 thf(m__870, axiom, (( aIdeal0 @ xJ ) & ( aIdeal0 @ xI ))).
% 34.78/7.99 thf(zip_derived_cl55, plain, ( (aIdeal0 @ xJ)),
% 34.78/7.99 inference('cnf', [status(esa)], [m__870])).
% 34.78/7.99 thf(mDefIdeal, axiom,
% 34.78/7.99 (![W0:$i]:
% 34.78/7.99 ( ( aIdeal0 @ W0 ) <=>
% 34.78/7.99 ( ( aSet0 @ W0 ) &
% 34.78/7.99 ( ![W1:$i]:
% 34.78/7.99 ( ( aElementOf0 @ W1 @ W0 ) =>
% 34.78/7.99 ( ( ![W2:$i]:
% 34.78/7.99 ( ( aElementOf0 @ W2 @ W0 ) =>
% 34.78/7.99 ( aElementOf0 @ ( sdtpldt0 @ W1 @ W2 ) @ W0 ) ) ) &
% 34.78/7.99 ( ![W2:$i]:
% 34.78/7.99 ( ( aElement0 @ W2 ) =>
% 34.78/7.99 ( aElementOf0 @ ( sdtasdt0 @ W2 @ W1 ) @ W0 ) ) ) ) ) ) ) ))).
% 34.78/7.99 thf(zip_derived_cl47, plain,
% 34.78/7.99 (![X0 : $i]: ( (aSet0 @ X0) | ~ (aIdeal0 @ X0))),
% 34.78/7.99 inference('cnf', [status(esa)], [mDefIdeal])).
% 34.78/7.99 thf(zip_derived_cl61, plain, ( (aSet0 @ xJ)),
% 34.78/7.99 inference('s_sup-', [status(thm)], [zip_derived_cl55, zip_derived_cl47])).
% 34.78/7.99 thf(zip_derived_cl56, plain, ( (aIdeal0 @ xI)),
% 34.78/7.99 inference('cnf', [status(esa)], [m__870])).
% 34.78/7.99 thf(zip_derived_cl47, plain,
% 34.78/7.99 (![X0 : $i]: ( (aSet0 @ X0) | ~ (aIdeal0 @ X0))),
% 34.78/7.99 inference('cnf', [status(esa)], [mDefIdeal])).
% 34.78/7.99 thf(zip_derived_cl62, plain, ( (aSet0 @ xI)),
% 34.78/7.99 inference('s_sup-', [status(thm)], [zip_derived_cl56, zip_derived_cl47])).
% 34.78/7.99 thf(zip_derived_cl21617, plain,
% 34.78/7.99 ( (zip_tseitin_2 @ (sk__6 @ xx @ xJ @ xI) @ (sk__5 @ xx @ xJ @ xI) @
% 34.78/7.99 xx @ xJ @ xI)),
% 34.78/7.99 inference('demod', [status(thm)],
% 34.78/7.99 [zip_derived_cl21602, zip_derived_cl61, zip_derived_cl62])).
% 34.78/7.99 thf(zip_derived_cl31, plain,
% 34.78/7.99 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 34.78/7.99 (((sdtpldt0 @ X1 @ X2) = (X0))
% 34.78/7.99 | ~ (zip_tseitin_2 @ X2 @ X1 @ X0 @ X3 @ X4))),
% 34.78/7.99 inference('cnf', [status(esa)], [zf_stmt_1])).
% 34.78/7.99 thf(zip_derived_cl21625, plain,
% 34.78/7.99 (((sdtpldt0 @ (sk__5 @ xx @ xJ @ xI) @ (sk__6 @ xx @ xJ @ xI)) = (xx))),
% 34.78/7.99 inference('s_sup-', [status(thm)],
% 34.78/7.99 [zip_derived_cl21617, zip_derived_cl31])).
% 34.78/7.99 thf(zip_derived_cl21617, plain,
% 34.78/7.99 ( (zip_tseitin_2 @ (sk__6 @ xx @ xJ @ xI) @ (sk__5 @ xx @ xJ @ xI) @
% 34.78/7.99 xx @ xJ @ xI)),
% 34.78/7.99 inference('demod', [status(thm)],
% 34.78/7.99 [zip_derived_cl21602, zip_derived_cl61, zip_derived_cl62])).
% 34.78/7.99 thf(zip_derived_cl32, plain,
% 34.78/7.99 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 34.78/7.99 ( (aElementOf0 @ X0 @ X1) | ~ (zip_tseitin_2 @ X0 @ X2 @ X3 @ X1 @ X4))),
% 34.78/7.99 inference('cnf', [status(esa)], [zf_stmt_1])).
% 34.78/7.99 thf(zip_derived_cl21626, plain,
% 34.78/7.99 ( (aElementOf0 @ (sk__6 @ xx @ xJ @ xI) @ xJ)),
% 34.78/7.99 inference('s_sup-', [status(thm)],
% 34.78/7.99 [zip_derived_cl21617, zip_derived_cl32])).
% 34.78/7.99 thf(zip_derived_cl21617, plain,
% 34.78/7.99 ( (zip_tseitin_2 @ (sk__6 @ xx @ xJ @ xI) @ (sk__5 @ xx @ xJ @ xI) @
% 34.78/7.99 xx @ xJ @ xI)),
% 34.78/7.99 inference('demod', [status(thm)],
% 34.78/7.99 [zip_derived_cl21602, zip_derived_cl61, zip_derived_cl62])).
% 34.78/7.99 thf(zip_derived_cl33, plain,
% 34.78/7.99 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 34.78/7.99 ( (aElementOf0 @ X0 @ X1) | ~ (zip_tseitin_2 @ X2 @ X0 @ X3 @ X4 @ X1))),
% 34.78/7.99 inference('cnf', [status(esa)], [zf_stmt_1])).
% 34.78/7.99 thf(zip_derived_cl21627, plain,
% 34.78/7.99 ( (aElementOf0 @ (sk__5 @ xx @ xJ @ xI) @ xI)),
% 34.78/7.99 inference('s_sup-', [status(thm)],
% 34.78/7.99 [zip_derived_cl21617, zip_derived_cl33])).
% 34.78/7.99 thf(m__, conjecture,
% 34.78/7.99 (?[W0:$i,W1:$i]:
% 34.78/7.99 ( ( ( xx ) = ( sdtpldt0 @ W0 @ W1 ) ) & ( aElementOf0 @ W1 @ xJ ) &
% 34.78/7.99 ( aElementOf0 @ W0 @ xI ) ))).
% 34.78/7.99 thf(zf_stmt_3, negated_conjecture,
% 34.78/7.99 (~( ?[W0:$i,W1:$i]:
% 34.78/7.99 ( ( ( xx ) = ( sdtpldt0 @ W0 @ W1 ) ) & ( aElementOf0 @ W1 @ xJ ) &
% 34.78/7.99 ( aElementOf0 @ W0 @ xI ) ) )),
% 34.78/7.99 inference('cnf.neg', [status(esa)], [m__])).
% 34.78/7.99 thf(zip_derived_cl60, plain,
% 34.78/7.99 (![X0 : $i, X1 : $i]:
% 34.78/7.99 (~ (aElementOf0 @ X0 @ xI)
% 34.78/7.99 | ~ (aElementOf0 @ X1 @ xJ)
% 34.78/7.99 | ((xx) != (sdtpldt0 @ X0 @ X1)))),
% 34.78/7.99 inference('cnf', [status(esa)], [zf_stmt_3])).
% 34.78/7.99 thf(zip_derived_cl21673, plain,
% 34.78/7.99 (![X0 : $i]:
% 34.78/7.99 (~ (aElementOf0 @ X0 @ xJ)
% 34.78/7.99 | ((xx) != (sdtpldt0 @ (sk__5 @ xx @ xJ @ xI) @ X0)))),
% 34.78/7.99 inference('s_sup-', [status(thm)],
% 34.78/7.99 [zip_derived_cl21627, zip_derived_cl60])).
% 34.78/7.99 thf(zip_derived_cl21687, plain,
% 34.78/7.99 (((xx) != (sdtpldt0 @ (sk__5 @ xx @ xJ @ xI) @ (sk__6 @ xx @ xJ @ xI)))),
% 34.78/7.99 inference('s_sup-', [status(thm)],
% 34.78/7.99 [zip_derived_cl21626, zip_derived_cl21673])).
% 34.78/7.99 thf(zip_derived_cl21713, plain, ($false),
% 34.78/7.99 inference('simplify_reflect-', [status(thm)],
% 34.78/7.99 [zip_derived_cl21625, zip_derived_cl21687])).
% 34.78/7.99
% 34.78/7.99 % SZS output end Refutation
% 34.78/7.99
% 34.78/7.99
% 34.78/7.99 % Terminating...
% 35.22/8.19 % Runner terminated.
% 35.22/8.23 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------