%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SYO378^5 : TPTP v9.2.0. Bugfixed v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.zuzevPRtCj true
% Computer : n009.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 05:07:20 PM UTC 2025
% Result : Theorem 0.51s 0.71s
% Output : Refutation 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SYO378^5 : TPTP v9.2.0. Bugfixed v5.2.0.
% 0.08/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.zuzevPRtCj true
% 0.13/0.35 % Computer : n009.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Oct 1 18:04:53 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.13/0.35 % Running portfolio for 300 s
% 0.13/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.35 % Number of cores: 8
% 0.13/0.35 % Python version: Python 3.6.8
% 0.13/0.36 % Running in HO mode
% 0.49/0.64 % Total configuration time : 828
% 0.49/0.64 % Estimated wc time : 1656
% 0.49/0.64 % Estimated cpu time (8 cpus) : 207.0
% 0.49/0.67 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.49/0.68 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.49/0.68 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.49/0.68 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 0.49/0.68 % /export/starexec/sandbox/solver/bin/lams/40_noforms.sh running for 90s
% 0.49/0.68 % /export/starexec/sandbox/solver/bin/lams/40_b.comb.sh running for 70s
% 0.49/0.68 % /export/starexec/sandbox/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.51/0.71 % Solved by lams/40_b.comb.sh.
% 0.51/0.71 % done 2 iterations in 0.010s
% 0.51/0.71 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.51/0.71 % SZS output start Refutation
% 0.51/0.71 thf(c_type, type, c: $i).
% 0.51/0.71 thf(cQDP1_type, type, cQDP1: ($i > $o) > $o).
% 0.51/0.71 thf(cQDP2_type, type, cQDP2: (($i > $o) > $o) > $o).
% 0.51/0.71 thf(cQDP0_type, type, cQDP0: $i > $o).
% 0.51/0.71 thf(cQDTHM2, conjecture, (?[Xs:( ( $i > $o ) > $o )]: ( cQDP2 @ Xs ))).
% 0.51/0.71 thf(zf_stmt_0, negated_conjecture,
% 0.51/0.71 (~( ?[Xs:( ( $i > $o ) > $o )]: ( cQDP2 @ Xs ) )),
% 0.51/0.71 inference('cnf.neg', [status(esa)], [cQDTHM2])).
% 0.51/0.71 thf(zip_derived_cl0, plain,
% 0.51/0.71 (~ (((??) @ (^[Y0 : ($i > $o) > $o]: (cQDP2 @ Y0))))),
% 0.51/0.71 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.51/0.71 thf(zip_derived_cl1, plain, (~ (((??) @ cQDP2))),
% 0.51/0.71 inference('lams2combs', [status(thm)], [zip_derived_cl0])).
% 0.51/0.71 thf(zip_derived_cl2, plain, (![X2 : ($i > $o) > $o]: ~ (cQDP2 @ X2)),
% 0.51/0.71 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl1])).
% 0.51/0.71 thf(cQDP2_def, axiom, ~ (cQDP2 @ X0) =>
% 0.51/0.71 ((((((X0) = (cQDP1))) & (((??) @ (^[Y0 : $i > $o]: (X0 @ Y0)))))) !=
% 0.51/0.71 ($true))).
% 0.51/0.71 thf('0', plain,
% 0.51/0.71 (![X0:( ( $i > $o ) > $o )]:
% 0.51/0.71 ( ( ~( cQDP2 @ X0 ) ) <=>
% 0.51/0.71 ( ~( ( ( X0 ) = ( cQDP1 ) ) & ( ?[X5:( $i > $o )]: ( X0 @ X5 ) ) ) ) )),
% 0.51/0.71 inference('rw.lit', [status(esa)], [cQDP2_def])).
% 0.51/0.71 thf(zip_derived_cl3, plain,
% 0.51/0.71 (![X0 : ($i > $o) > $o]:
% 0.51/0.71 ~ (((((X0) = (cQDP1))) & (((??) @ (^[Y0 : $i > $o]: (X0 @ Y0))))))),
% 0.51/0.71 inference('rw_clause', [status(thm)], [zip_derived_cl2, '0'])).
% 0.51/0.71 thf(zip_derived_cl4, plain,
% 0.51/0.71 (![X0 : ($i > $o) > $o]: ~ (((((X0) = (cQDP1))) & (((??) @ X0))))),
% 0.51/0.71 inference('comb-normalize', [status(thm)], [zip_derived_cl3])).
% 0.51/0.71 thf(zip_derived_cl5, plain,
% 0.51/0.71 (![X0 : ($i > $o) > $o]: (~ (((X0) = (cQDP1))) | ~ (((??) @ X0)))),
% 0.51/0.71 inference('lazy_cnf_and', [status(thm)], [zip_derived_cl4])).
% 0.51/0.71 thf(zip_derived_cl6, plain,
% 0.51/0.71 (![X0 : ($i > $o) > $o]: (((X0) != (cQDP1)) | ~ (((??) @ X0)))),
% 0.51/0.71 inference('simplify nested equalities', [status(thm)], [zip_derived_cl5])).
% 0.51/0.71 thf(zip_derived_cl7, plain,
% 0.51/0.71 (![X0 : ($i > $o) > $o, X2 : $i > $o]: (~ (X0 @ X2) | ((X0) != (cQDP1)))),
% 0.51/0.71 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl6])).
% 0.51/0.71 thf(zip_derived_cl10, plain, (![X0 : $i > $o]: ~ (cQDP1 @ X0)),
% 0.51/0.71 inference('eq_res', [status(thm)], [zip_derived_cl7])).
% 0.51/0.71 thf(cQDP1_def, axiom, ~ (cQDP1 @ X0) =>
% 0.51/0.71 ((((((X0) = (cQDP0))) & (((??) @ (^[Y0 : $i]: (X0 @ Y0)))))) != ($true))).
% 0.51/0.71 thf('1', plain,
% 0.51/0.71 (![X0:( $i > $o )]:
% 0.51/0.71 ( ( ~( cQDP1 @ X0 ) ) <=>
% 0.51/0.71 ( ~( ( ( X0 ) = ( cQDP0 ) ) & ( ?[X5:$i]: ( X0 @ X5 ) ) ) ) )),
% 0.51/0.71 inference('rw.lit', [status(esa)], [cQDP1_def])).
% 0.51/0.71 thf(zip_derived_cl20, plain,
% 0.51/0.71 (![X0 : $i > $o]:
% 0.51/0.71 ~ (((((X0) = (cQDP0))) & (((??) @ (^[Y0 : $i]: (X0 @ Y0))))))),
% 0.51/0.71 inference('rw_clause', [status(thm)], [zip_derived_cl10, '1'])).
% 0.51/0.71 thf(zip_derived_cl21, plain,
% 0.51/0.71 (![X0 : $i > $o]: ~ (((((X0) = (cQDP0))) & (((??) @ X0))))),
% 0.51/0.71 inference('comb-normalize', [status(thm)], [zip_derived_cl20])).
% 0.51/0.71 thf(zip_derived_cl22, plain,
% 0.51/0.71 (![X0 : $i > $o]: (~ (((X0) = (cQDP0))) | ~ (((??) @ X0)))),
% 0.51/0.71 inference('lazy_cnf_and', [status(thm)], [zip_derived_cl21])).
% 0.51/0.71 thf(zip_derived_cl23, plain,
% 0.51/0.71 (![X0 : $i > $o]: (((X0) != (cQDP0)) | ~ (((??) @ X0)))),
% 0.51/0.71 inference('simplify nested equalities', [status(thm)], [zip_derived_cl22])).
% 0.51/0.71 thf(zip_derived_cl24, plain,
% 0.51/0.71 (![X0 : $i > $o, X2 : $i]: (~ (X0 @ X2) | ((X0) != (cQDP0)))),
% 0.51/0.71 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl23])).
% 0.51/0.71 thf(zip_derived_cl27, plain, (![X0 : $i]: ~ (cQDP0 @ X0)),
% 0.51/0.71 inference('eq_res', [status(thm)], [zip_derived_cl24])).
% 0.51/0.71 thf(cQDP0_def, axiom,(( cQDP0 @ (X0)) = ((((X0) = (c)))))).
% 0.51/0.71 thf('2', plain, (![X0:$i]: ( ( cQDP0 @ X0 ) = ( ( X0 ) = ( c ) ) )),
% 0.51/0.71 define([status(thm)])).
% 0.51/0.71 thf(zip_derived_cl36, plain, (![X0 : $i]: ~ (((X0) = (c)))),
% 0.51/0.71 inference('rw', [status(thm)], [zip_derived_cl27, '2'])).
% 0.51/0.71 thf(zip_derived_cl37, plain, (![X0 : $i]: ((X0) != (c))),
% 0.51/0.71 inference('simplify nested equalities', [status(thm)], [zip_derived_cl36])).
% 0.51/0.71 thf(zip_derived_cl40, plain, ($false),
% 0.51/0.71 inference('eq_res', [status(thm)], [zip_derived_cl37])).
% 0.51/0.71
% 0.51/0.71 % SZS output end Refutation
% 0.51/0.71
% 0.51/0.71
% 0.51/0.71 % Terminating...
% 0.51/0.74 % Runner terminated.
% 1.25/0.75 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------