%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEV231^5 : 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.T83kmkMCNU true
% Computer : n011.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:57:25 PM UTC 2025
% Result : Theorem 0.59s 0.86s
% Output : Refutation 0.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEV231^5 : TPTP v9.2.0. Released v4.0.0.
% 0.03/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.T83kmkMCNU true
% 0.13/0.34 % Computer : n011.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 15:40: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.35 % Number of cores: 8
% 0.13/0.35 % Python version: Python 3.6.8
% 0.13/0.35 % Running in HO mode
% 0.57/0.68 % Total configuration time : 828
% 0.57/0.68 % Estimated wc time : 1656
% 0.57/0.68 % Estimated cpu time (8 cpus) : 207.0
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.57/0.80 % /export/starexec/sandbox2/solver/bin/lams/40_c.s.sh running for 80s
% 0.57/0.80 % /export/starexec/sandbox2/solver/bin/lams/15_e_short1.sh running for 30s
% 0.57/0.80 % /export/starexec/sandbox2/solver/bin/lams/40_c_ic.sh running for 80s
% 0.57/0.80 % /export/starexec/sandbox2/solver/bin/lams/40_noforms.sh running for 90s
% 0.57/0.81 % /export/starexec/sandbox2/solver/bin/lams/40_b.comb.sh running for 70s
% 0.57/0.81 % /export/starexec/sandbox2/solver/bin/lams/30_sp5.sh running for 60s
% 0.57/0.82 % /export/starexec/sandbox2/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.59/0.86 % Solved by lams/35_full_unif4.sh.
% 0.59/0.86 % done 31 iterations in 0.062s
% 0.59/0.86 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.59/0.86 % SZS output start Refutation
% 0.59/0.86 thf(a_type, type, a: $tType).
% 0.59/0.86 thf('#sk2_type', type, '#sk2': a > $o).
% 0.59/0.86 thf('#form9_type', type, '#form9': $o).
% 0.59/0.86 thf(x_type, type, x: a > $o).
% 0.59/0.86 thf('#sk1_type', type, '#sk1': a).
% 0.59/0.86 thf('#form24_type', type, '#form24': $o).
% 0.59/0.86 thf(y_type, type, y: a > $o).
% 0.59/0.86 thf(cX5201_pme, conjecture,
% 0.59/0.86 (( ^[Xx0:a]: ( ( y @ Xx0 ) & ( x @ Xx0 ) ) ) =
% 0.59/0.86 ( ^[Xx0:a]:
% 0.59/0.86 ( ![S:( a > $o )]:
% 0.59/0.86 ( ( ( ( S ) = ( y ) ) | ( ( S ) = ( x ) ) ) => ( S @ Xx0 ) ) ) ))).
% 0.59/0.86 thf(zf_stmt_0, negated_conjecture,
% 0.59/0.86 (( ^[Xx0:a]: ( ( y @ Xx0 ) & ( x @ Xx0 ) ) ) !=
% 0.59/0.86 ( ^[Xx0:a]:
% 0.59/0.86 ( ![S:( a > $o )]:
% 0.59/0.86 ( ( ( ( S ) = ( y ) ) | ( ( S ) = ( x ) ) ) => ( S @ Xx0 ) ) ) )),
% 0.59/0.86 inference('cnf.neg', [status(esa)], [cX5201_pme])).
% 0.59/0.86 thf(zip_derived_cl0, plain,
% 0.59/0.86 ((((^[Y0 : a]: (((y @ Y0) & (x @ Y0)))))
% 0.59/0.86 != ((^[Y0 : a]:
% 0.59/0.86 (((!!) @ (^[Y1 : a > $o]:
% 0.59/0.86 (((((((Y1) = (y))) | (((Y1) = (x))))) => (Y1 @ Y0)))))))))),
% 0.59/0.86 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.59/0.86 thf(zip_derived_cl1, plain,
% 0.59/0.86 (((((y @ '#sk1') & (x @ '#sk1')))
% 0.59/0.86 != (((!!) @ (^[Y0 : a > $o]:
% 0.59/0.86 ((((((((^[Y1 : a]: (Y0 @ Y1))) =
% 0.59/0.86 ((^[Y1 : a]: (y @ Y1))))) |
% 0.59/0.86 ((((^[Y1 : a]: (Y0 @ Y1))) =
% 0.59/0.86 ((^[Y1 : a]: (x @ Y1))))))) =>
% 0.59/0.86 (Y0 @ '#sk1')))))))),
% 0.59/0.86 inference('neg_ext', [status(thm)], [zip_derived_cl0])).
% 0.59/0.86 thf(zip_derived_cl2, plain,
% 0.59/0.86 (((((y @ '#sk1') & (x @ '#sk1')))
% 0.59/0.86 != (((!!) @ (^[Y0 : a > $o]:
% 0.59/0.86 (((((((Y0) = (y))) | (((Y0) = (x))))) => (Y0 @ '#sk1')))))))),
% 0.59/0.86 inference('ho_norm', [status(thm)], [zip_derived_cl1])).
% 0.59/0.86 thf(zip_derived_cl7, plain,
% 0.59/0.86 (((((y @ '#sk1') & (x @ '#sk1')))
% 0.59/0.86 != ((^[Y0 : a > $o]:
% 0.59/0.86 ((((((((^[Y1 : a]: (Y0 @ Y1))) = ((^[Y1 : a]: (y @ Y1))))) |
% 0.59/0.86 ((((^[Y1 : a]: (Y0 @ Y1))) = ((^[Y1 : a]: (x @ Y1))))))) =>
% 0.59/0.86 (Y0 @ '#sk1')))) @
% 0.59/0.86 '#sk2'))),
% 0.59/0.86 inference('quantifier_rw', [status(thm)], [zip_derived_cl2])).
% 0.59/0.86 thf(zip_derived_cl8, plain,
% 0.59/0.86 (((((y @ '#sk1') & (x @ '#sk1')))
% 0.59/0.86 != ((((((('#sk2') = (y))) | ((('#sk2') = (x))))) => ('#sk2' @ '#sk1'))))),
% 0.59/0.86 inference('ho_norm', [status(thm)], [zip_derived_cl7])).
% 0.59/0.86 thf(zip_derived_cl2, plain,
% 0.59/0.86 (((((y @ '#sk1') & (x @ '#sk1')))
% 0.59/0.86 != (((!!) @ (^[Y0 : a > $o]:
% 0.59/0.86 (((((((Y0) = (y))) | (((Y0) = (x))))) => (Y0 @ '#sk1')))))))),
% 0.59/0.86 inference('ho_norm', [status(thm)], [zip_derived_cl1])).
% 0.59/0.86 thf(zip_derived_cl3, plain,
% 0.59/0.86 (![X-81 : a > $o]:
% 0.59/0.86 ( ((^[Y0 : a > $o]:
% 0.59/0.86 (((((((Y0) = (y))) | (((Y0) = (x))))) => (Y0 @ '#sk1')))) @
% 0.59/0.86 X-81)
% 0.59/0.86 | (((y @ '#sk1') & (x @ '#sk1'))))),
% 0.59/0.86 inference('forall_hoist', [status(thm)], [zip_derived_cl2])).
% 0.59/0.86 thf(zip_derived_cl9, plain,
% 0.59/0.86 (![X-81 : a > $o]:
% 0.59/0.86 ( (((((((X-81) = (y))) | (((X-81) = (x))))) => (X-81 @ '#sk1')))
% 0.59/0.86 | (((y @ '#sk1') & (x @ '#sk1'))))),
% 0.59/0.86 inference('ho_norm', [status(thm)], [zip_derived_cl3])).
% 0.59/0.86 thf(zip_derived_cl10, plain,
% 0.59/0.86 (![X0 : a > $o]:
% 0.59/0.86 ( (((((((X0) = (y))) | (((X0) = (x))))) => (X0 @ '#sk1')))
% 0.59/0.86 | (((y @ '#sk1') & (x @ '#sk1'))))),
% 0.59/0.86 inference('cannonize vars', [status(thm)], [zip_derived_cl9])).
% 0.59/0.86 thf(zip_derived_cl11, plain,
% 0.59/0.86 (![X0 : a > $o]:
% 0.59/0.86 (~ (((((X0) = (y))) | (((X0) = (x)))))
% 0.59/0.86 | (X0 @ '#sk1')
% 0.59/0.86 | (((y @ '#sk1') & (x @ '#sk1'))))),
% 0.59/0.86 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl10])).
% 0.59/0.86 thf(zip_derived_cl11, plain,
% 0.59/0.86 (![X0 : a > $o]:
% 0.59/0.86 (~ (((((X0) = (y))) | (((X0) = (x)))))
% 0.59/0.86 | (X0 @ '#sk1')
% 0.59/0.86 | (((y @ '#sk1') & (x @ '#sk1'))))),
% 0.59/0.86 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl10])).
% 0.59/0.86 thf(zip_derived_cl12, plain,
% 0.59/0.86 ((~ ('#form9') | (((y @ '#sk1') & (x @ '#sk1'))))),
% 0.59/0.86 define([status(thm)])).
% 0.59/0.86 thf(zip_derived_cl15, plain,
% 0.59/0.86 (![X0 : a > $o]:
% 0.59/0.86 ( ('#form9') | (X0 @ '#sk1') | ~ (((((X0) = (y))) | (((X0) = (x))))))),
% 0.59/0.86 inference('renaming', [status(thm)], [zip_derived_cl11, zip_derived_cl12])).
% 0.59/0.86 thf(zip_derived_cl16, plain,
% 0.59/0.86 (![X0 : a > $o]: (~ (((X0) = (y))) | (X0 @ '#sk1') | ('#form9'))),
% 0.59/0.86 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl15])).
% 0.59/0.86 thf(zip_derived_cl18, plain,
% 0.59/0.86 (![X0 : a > $o]: (((X0) != (y)) | (X0 @ '#sk1') | ('#form9'))),
% 0.59/0.86 inference('simplify nested equalities', [status(thm)], [zip_derived_cl16])).
% 0.59/0.86 thf(zip_derived_cl29, plain, (( ('#form9') | (y @ '#sk1'))),
% 0.59/0.86 inference('eq_res', [status(thm)], [zip_derived_cl18])).
% 0.59/0.86 thf(zip_derived_cl12, plain,
% 0.59/0.86 ((~ ('#form9') | (((y @ '#sk1') & (x @ '#sk1'))))),
% 0.59/0.86 define([status(thm)])).
% 0.59/0.86 thf(zip_derived_cl13, plain, (( (y @ '#sk1') | ~ ('#form9'))),
% 0.59/0.86 inference('lazy_cnf_and', [status(thm)], [zip_derived_cl12])).
% 0.59/0.86 thf(zip_derived_cl31, plain, ( (y @ '#sk1')),
% 0.59/0.86 inference('clc', [status(thm)], [zip_derived_cl29, zip_derived_cl13])).
% 0.59/0.86 thf(zip_derived_cl32, plain,
% 0.59/0.86 ((((($true) & (x @ '#sk1')))
% 0.59/0.86 != ((((((('#sk2') = (y))) | ((('#sk2') = (x))))) => ('#sk2' @ '#sk1'))))),
% 0.59/0.86 inference('demod', [status(thm)], [zip_derived_cl8, zip_derived_cl31])).
% 0.59/0.86 thf(zip_derived_cl33, plain,
% 0.59/0.86 (((x @ '#sk1')
% 0.59/0.86 != ((((((('#sk2') = (y))) | ((('#sk2') = (x))))) => ('#sk2' @ '#sk1'))))),
% 0.59/0.86 inference('simplify boolean subterms', [status(thm)], [zip_derived_cl32])).
% 0.59/0.86 thf(zip_derived_cl36, plain,
% 0.59/0.86 ((~ (x @ '#sk1')
% 0.59/0.86 | ~ ((((((('#sk2') = (y))) | ((('#sk2') = (x))))) => ('#sk2' @ '#sk1'))))),
% 0.59/0.86 inference('eq_elim', [status(thm)], [zip_derived_cl33])).
% 0.59/0.86 thf(zip_derived_cl40, plain,
% 0.59/0.86 (( ('#form24')
% 0.59/0.86 | ~ ((((((('#sk2') = (y))) | ((('#sk2') = (x))))) => ('#sk2' @ '#sk1'))))),
% 0.59/0.86 define([status(thm)])).
% 0.59/0.86 thf(zip_derived_cl42, plain, ((~ ('#sk2' @ '#sk1') | ('#form24'))),
% 0.59/0.86 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl40])).
% 0.59/0.86 thf(zip_derived_cl36, plain,
% 0.59/0.86 ((~ (x @ '#sk1')
% 0.59/0.86 | ~ ((((((('#sk2') = (y))) | ((('#sk2') = (x))))) => ('#sk2' @ '#sk1'))))),
% 0.59/0.86 inference('eq_elim', [status(thm)], [zip_derived_cl33])).
% 0.59/0.86 thf(zip_derived_cl40, plain,
% 0.59/0.86 (( ('#form24')
% 0.59/0.86 | ~ ((((((('#sk2') = (y))) | ((('#sk2') = (x))))) => ('#sk2' @ '#sk1'))))),
% 0.59/0.86 define([status(thm)])).
% 0.59/0.86 thf(zip_derived_cl43, plain, ((~ ('#form24') | ~ (x @ '#sk1'))),
% 0.59/0.86 inference('renaming', [status(thm)], [zip_derived_cl36, zip_derived_cl40])).
% 0.59/0.86 thf(zip_derived_cl17, plain,
% 0.59/0.86 (![X0 : a > $o]: (~ (((X0) = (x))) | (X0 @ '#sk1') | ('#form9'))),
% 0.59/0.86 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl15])).
% 0.59/0.86 thf(zip_derived_cl19, plain,
% 0.59/0.86 (![X0 : a > $o]: (((X0) != (x)) | (X0 @ '#sk1') | ('#form9'))),
% 0.59/0.86 inference('simplify nested equalities', [status(thm)], [zip_derived_cl17])).
% 0.59/0.86 thf(zip_derived_cl87, plain, (( ('#form9') | (x @ '#sk1'))),
% 0.59/0.86 inference('eq_res', [status(thm)], [zip_derived_cl19])).
% 0.59/0.86 thf(zip_derived_cl14, plain, (( (x @ '#sk1') | ~ ('#form9'))),
% 0.59/0.86 inference('lazy_cnf_and', [status(thm)], [zip_derived_cl12])).
% 0.59/0.86 thf(zip_derived_cl89, plain, ( (x @ '#sk1')),
% 0.59/0.86 inference('clc', [status(thm)], [zip_derived_cl87, zip_derived_cl14])).
% 0.59/0.86 thf(zip_derived_cl91, plain, (~ ('#form24')),
% 0.59/0.86 inference('demod', [status(thm)], [zip_derived_cl43, zip_derived_cl89])).
% 0.59/0.86 thf(zip_derived_cl92, plain, (~ ('#sk2' @ '#sk1')),
% 0.59/0.86 inference('demod', [status(thm)], [zip_derived_cl42, zip_derived_cl91])).
% 0.59/0.86 thf(zip_derived_cl33, plain,
% 0.59/0.86 (((x @ '#sk1')
% 0.59/0.86 != ((((((('#sk2') = (y))) | ((('#sk2') = (x))))) => ('#sk2' @ '#sk1'))))),
% 0.59/0.86 inference('simplify boolean subterms', [status(thm)], [zip_derived_cl32])).
% 0.59/0.86 thf(zip_derived_cl89, plain, ( (x @ '#sk1')),
% 0.59/0.86 inference('clc', [status(thm)], [zip_derived_cl87, zip_derived_cl14])).
% 0.59/0.86 thf(zip_derived_cl90, plain,
% 0.59/0.86 (~ ((((((('#sk2') = (y))) | ((('#sk2') = (x))))) => ('#sk2' @ '#sk1')))),
% 0.59/0.86 inference('demod', [status(thm)], [zip_derived_cl33, zip_derived_cl89])).
% 0.59/0.86 thf(zip_derived_cl92, plain, (~ ('#sk2' @ '#sk1')),
% 0.59/0.86 inference('demod', [status(thm)], [zip_derived_cl42, zip_derived_cl91])).
% 0.59/0.86 thf(zip_derived_cl94, plain,
% 0.59/0.86 (~ ((((((('#sk2') = (y))) | ((('#sk2') = (x))))) => ($false)))),
% 0.59/0.86 inference('demod', [status(thm)], [zip_derived_cl90, zip_derived_cl92])).
% 0.59/0.86 thf(zip_derived_cl95, plain,
% 0.59/0.86 (~ (((~) @ ((((('#sk2') = (y))) | ((('#sk2') = (x)))))))),
% 0.59/0.86 inference('simplify boolean subterms', [status(thm)], [zip_derived_cl94])).
% 0.59/0.86 thf(zip_derived_cl96, plain, ( ((((('#sk2') = (y))) | ((('#sk2') = (x)))))),
% 0.59/0.86 inference('simplify nested equalities', [status(thm)], [zip_derived_cl95])).
% 0.59/0.86 thf(zip_derived_cl97, plain, (( ((('#sk2') = (y))) | ((('#sk2') = (x))))),
% 0.59/0.86 inference('lazy_cnf_or', [status(thm)], [zip_derived_cl96])).
% 0.59/0.86 thf(zip_derived_cl98, plain, (((('#sk2') = (y)) | (('#sk2') = (x)))),
% 0.59/0.86 inference('simplify nested equalities', [status(thm)], [zip_derived_cl97])).
% 0.59/0.86 thf(zip_derived_cl100, plain,
% 0.59/0.86 (![X1 : a]: ((('#sk2' @ X1) = (x @ X1)) | (('#sk2') = (y)))),
% 0.59/0.86 inference('ho_complete_eq', [status(thm)], [zip_derived_cl98])).
% 0.59/0.86 thf(zip_derived_cl89, plain, ( (x @ '#sk1')),
% 0.59/0.86 inference('clc', [status(thm)], [zip_derived_cl87, zip_derived_cl14])).
% 0.59/0.86 thf(zip_derived_cl106, plain, (( ('#sk2' @ '#sk1') | (('#sk2') = (y)))),
% 0.59/0.86 inference('sup+', [status(thm)], [zip_derived_cl100, zip_derived_cl89])).
% 0.59/0.86 thf(zip_derived_cl92, plain, (~ ('#sk2' @ '#sk1')),
% 0.59/0.86 inference('demod', [status(thm)], [zip_derived_cl42, zip_derived_cl91])).
% 0.59/0.86 thf(zip_derived_cl113, plain, ((('#sk2') = (y))),
% 0.59/0.86 inference('demod', [status(thm)], [zip_derived_cl106, zip_derived_cl92])).
% 0.59/0.86 thf(zip_derived_cl117, plain, (![X1 : a]: (('#sk2' @ X1) = (y @ X1))),
% 0.59/0.86 inference('ho_complete_eq', [status(thm)], [zip_derived_cl113])).
% 0.59/0.86 thf(zip_derived_cl31, plain, ( (y @ '#sk1')),
% 0.59/0.86 inference('clc', [status(thm)], [zip_derived_cl29, zip_derived_cl13])).
% 0.59/0.86 thf(zip_derived_cl119, plain, ( ('#sk2' @ '#sk1')),
% 0.59/0.86 inference('sup+', [status(thm)], [zip_derived_cl117, zip_derived_cl31])).
% 0.59/0.86 thf(zip_derived_cl125, plain, ($false),
% 0.59/0.86 inference('demod', [status(thm)], [zip_derived_cl92, zip_derived_cl119])).
% 0.59/0.86
% 0.59/0.86 % SZS output end Refutation
% 0.59/0.86
% 0.59/0.86
% 0.59/0.86 % Terminating...
% 0.60/0.91 % Runner terminated.
% 0.60/0.93 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------