%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : ANA126^1 : TPTP v9.2.0. Released v7.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.8HCfMj2eGr 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 04:29:01 PM UTC 2025
% Result : Theorem 3.39s 1.11s
% Output : Refutation 3.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.14 % Problem : ANA126^1 : TPTP v9.2.0. Released v7.0.0.
% 0.07/0.15 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.8HCfMj2eGr true
% 0.14/0.36 % Computer : n009.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed Oct 1 15:23:53 EDT 2025
% 0.14/0.36 % CPUTime :
% 0.14/0.36 % Running portfolio for 300 s
% 0.14/0.36 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.36 % Number of cores: 8
% 0.14/0.36 % Python version: Python 3.6.8
% 0.14/0.36 % Running in HO mode
% 0.39/0.73 % Total configuration time : 828
% 0.39/0.73 % Estimated wc time : 1656
% 0.39/0.73 % Estimated cpu time (8 cpus) : 207.0
% 0.40/0.79 % /export/starexec/sandbox2/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.40/0.79 % /export/starexec/sandbox2/solver/bin/lams/40_c.s.sh running for 80s
% 0.40/0.80 % /export/starexec/sandbox2/solver/bin/lams/40_c_ic.sh running for 80s
% 0.40/0.81 % /export/starexec/sandbox2/solver/bin/lams/15_e_short1.sh running for 30s
% 0.40/0.82 % /export/starexec/sandbox2/solver/bin/lams/40_noforms.sh running for 90s
% 0.40/0.83 % /export/starexec/sandbox2/solver/bin/lams/40_b.comb.sh running for 70s
% 0.40/0.84 % /export/starexec/sandbox2/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.40/0.84 % /export/starexec/sandbox2/solver/bin/lams/30_sp5.sh running for 60s
% 3.39/1.11 % Solved by lams/35_full_unif4.sh.
% 3.39/1.11 % done 89 iterations in 0.291s
% 3.39/1.11 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 3.39/1.11 % SZS output start Refutation
% 3.39/1.11 thf('type/realax/real_type', type, 'type/realax/real': $tType).
% 3.39/1.11 thf('type/nums/num_type', type, 'type/nums/num': $tType).
% 3.39/1.11 thf('const/realax/real_mul_type', type, 'const/realax/real_mul': 'type/realax/real' >
% 3.39/1.11 'type/realax/real' > 'type/realax/real').
% 3.39/1.11 thf('#sk43_type', type, '#sk43': ('type/realax/real' > 'type/realax/real') >
% 3.39/1.11 'type/realax/real' > 'type/realax/real').
% 3.39/1.11 thf('const/iterate/polynomial_function_type', type, 'const/iterate/polynomial_function':
% 3.39/1.11 ('type/realax/real' > 'type/realax/real') > $o).
% 3.39/1.11 thf('#sk418_type', type, '#sk418': 'type/realax/real' > 'type/realax/real').
% 3.39/1.11 thf('const/realax/real_of_num_type', type, 'const/realax/real_of_num':
% 3.39/1.11 'type/nums/num' > 'type/realax/real').
% 3.39/1.11 thf('const/nums/BIT1_type', type, 'const/nums/BIT1': 'type/nums/num' > 'type/nums/num').
% 3.39/1.11 thf('#sk1_type', type, '#sk1': 'type/realax/real' > 'type/realax/real').
% 3.39/1.11 thf('const/nums/_0_type', type, 'const/nums/_0': 'type/nums/num').
% 3.39/1.11 thf('const/nums/NUMERAL_type', type, 'const/nums/NUMERAL': 'type/nums/num' > 'type/nums/num').
% 3.39/1.11 thf('const/realax/real_neg_type', type, 'const/realax/real_neg': 'type/realax/real' > 'type/realax/real').
% 3.39/1.11 thf('thm/realax/REAL_MUL_LID_', axiom,
% 3.39/1.11 (![A:'type/realax/real']:
% 3.39/1.11 ( ( 'const/realax/real_mul' @
% 3.39/1.11 ( 'const/realax/real_of_num' @
% 3.39/1.11 ( 'const/nums/NUMERAL' @ ( 'const/nums/BIT1' @ 'const/nums/_0' ) ) ) @
% 3.39/1.11 A ) =
% 3.39/1.11 ( A ) ))).
% 3.39/1.11 thf(zip_derived_cl0, plain,
% 3.39/1.11 ( (((!!) @ (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ((('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @
% 3.39/1.11 ('const/nums/BIT1' @ 'const/nums/_0'))) @
% 3.39/1.11 Y0) = (Y0))))))),
% 3.39/1.11 inference('cnf', [status(esa)], [thm/realax/REAL_MUL_LID_])).
% 3.39/1.11 thf(zip_derived_cl48, plain,
% 3.39/1.11 (![X2 : 'type/realax/real']:
% 3.39/1.11 ((('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @ ('const/nums/BIT1' @ 'const/nums/_0'))) @
% 3.39/1.11 X2) = (X2)))),
% 3.39/1.11 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl0])).
% 3.39/1.11 thf(zip_derived_cl49, plain,
% 3.39/1.11 (![X2 : 'type/realax/real']:
% 3.39/1.11 (('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @ ('const/nums/BIT1' @ 'const/nums/_0'))) @
% 3.39/1.11 X2) = (X2))),
% 3.39/1.11 inference('simplify nested equalities', [status(thm)], [zip_derived_cl48])).
% 3.39/1.11 thf('thm/calc_int/REAL_MUL_LNEG_', axiom,
% 3.39/1.11 (![A:'type/realax/real',A0:'type/realax/real']:
% 3.39/1.11 ( ( 'const/realax/real_mul' @ ( 'const/realax/real_neg' @ A ) @ A0 ) =
% 3.39/1.11 ( 'const/realax/real_neg' @ ( 'const/realax/real_mul' @ A @ A0 ) ) ))).
% 3.39/1.11 thf(zip_derived_cl1, plain,
% 3.39/1.11 ( (((!!) @ (^[Y0 : 'type/realax/real']:
% 3.39/1.11 (((!!) @ (^[Y1 : 'type/realax/real']:
% 3.39/1.11 ((('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @ Y0) @ Y1) =
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_mul' @ Y0 @ Y1))))))))))),
% 3.39/1.11 inference('cnf', [status(esa)], [thm/calc_int/REAL_MUL_LNEG_])).
% 3.39/1.11 thf(zip_derived_cl50, plain,
% 3.39/1.11 (![X2 : 'type/realax/real']:
% 3.39/1.11 (((!!) @ (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ((('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @ X2) @ Y0) =
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_mul' @ X2 @ Y0)))))))),
% 3.39/1.11 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl1])).
% 3.39/1.11 thf(zip_derived_cl51, plain,
% 3.39/1.11 (![X2 : 'type/realax/real', X4 : 'type/realax/real']:
% 3.39/1.11 ((('const/realax/real_mul' @ ('const/realax/real_neg' @ X2) @ X4) =
% 3.39/1.11 ('const/realax/real_neg' @ ('const/realax/real_mul' @ X2 @ X4))))),
% 3.39/1.11 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl50])).
% 3.39/1.11 thf(zip_derived_cl52, plain,
% 3.39/1.11 (![X2 : 'type/realax/real', X4 : 'type/realax/real']:
% 3.39/1.11 (('const/realax/real_mul' @ ('const/realax/real_neg' @ X2) @ X4)
% 3.39/1.11 = ('const/realax/real_neg' @ ('const/realax/real_mul' @ X2 @ X4)))),
% 3.39/1.11 inference('simplify nested equalities', [status(thm)], [zip_derived_cl51])).
% 3.39/1.11 thf(zip_derived_cl49, plain,
% 3.39/1.11 (![X2 : 'type/realax/real']:
% 3.39/1.11 (('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @ ('const/nums/BIT1' @ 'const/nums/_0'))) @
% 3.39/1.11 X2) = (X2))),
% 3.39/1.11 inference('simplify nested equalities', [status(thm)], [zip_derived_cl48])).
% 3.39/1.11 thf(zip_derived_cl49, plain,
% 3.39/1.11 (![X2 : 'type/realax/real']:
% 3.39/1.11 (('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @ ('const/nums/BIT1' @ 'const/nums/_0'))) @
% 3.39/1.11 X2) = (X2))),
% 3.39/1.11 inference('simplify nested equalities', [status(thm)], [zip_derived_cl48])).
% 3.39/1.11 thf('thm/iterate/POLYNOMIAL_FUNCTION_NEG_', conjecture,
% 3.39/1.11 (![A:( 'type/realax/real' > 'type/realax/real' )]:
% 3.39/1.11 ( ( 'const/iterate/polynomial_function' @
% 3.39/1.11 ( ^[A0:'type/realax/real']: ( 'const/realax/real_neg' @ ( A @ A0 ) ) ) ) =
% 3.39/1.11 ( 'const/iterate/polynomial_function' @ A ) ))).
% 3.39/1.11 thf(zf_stmt_0, negated_conjecture,
% 3.39/1.11 (~( ![A:( 'type/realax/real' > 'type/realax/real' )]:
% 3.39/1.11 ( ( 'const/iterate/polynomial_function' @
% 3.39/1.11 ( ^[A0:'type/realax/real']:
% 3.39/1.11 ( 'const/realax/real_neg' @ ( A @ A0 ) ) ) ) =
% 3.39/1.11 ( 'const/iterate/polynomial_function' @ A ) ) )),
% 3.39/1.11 inference('cnf.neg', [status(esa)], [thm/iterate/POLYNOMIAL_FUNCTION_NEG_])).
% 3.39/1.11 thf(zip_derived_cl4, plain,
% 3.39/1.11 (~ (((!!) @ (^[Y0 : 'type/realax/real' > 'type/realax/real']:
% 3.39/1.11 ((('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y1 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ (Y0 @ Y1)))) =
% 3.39/1.11 ('const/iterate/polynomial_function' @ Y0))))))),
% 3.39/1.11 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.39/1.11 thf(zip_derived_cl11, plain,
% 3.39/1.11 (~ ((('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))) =
% 3.39/1.11 ('const/iterate/polynomial_function' @ '#sk1')))),
% 3.39/1.11 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl4])).
% 3.39/1.11 thf(zip_derived_cl12, plain,
% 3.39/1.11 ((('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']: ('const/realax/real_neg' @ ('#sk1' @ Y0))))
% 3.39/1.11 != ('const/iterate/polynomial_function' @ '#sk1'))),
% 3.39/1.11 inference('simplify nested equalities', [status(thm)], [zip_derived_cl11])).
% 3.39/1.11 thf(zip_derived_cl13, plain,
% 3.39/1.11 (( ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0))))
% 3.39/1.11 | ('const/iterate/polynomial_function' @ '#sk1'))),
% 3.39/1.11 inference('eq_elim', [status(thm)], [zip_derived_cl12])).
% 3.39/1.11 thf('thm/iterate/POLYNOMIAL_FUNCTION_LMUL_', axiom,
% 3.39/1.11 (![A:( 'type/realax/real' > 'type/realax/real' ),A0:'type/realax/real']:
% 3.39/1.11 ( ( 'const/iterate/polynomial_function' @ A ) =>
% 3.39/1.11 ( 'const/iterate/polynomial_function' @
% 3.39/1.11 ( ^[A1:'type/realax/real']:
% 3.39/1.11 ( 'const/realax/real_mul' @ A0 @ ( A @ A1 ) ) ) ) ))).
% 3.39/1.11 thf(zip_derived_cl2, plain,
% 3.39/1.11 ( (((!!) @ (^[Y0 : 'type/realax/real' > 'type/realax/real']:
% 3.39/1.11 (((!!) @ (^[Y1 : 'type/realax/real']:
% 3.39/1.11 ((('const/iterate/polynomial_function' @ Y0) =>
% 3.39/1.11 ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y2 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ Y1 @ (Y0 @ Y2))))))))))))),
% 3.39/1.11 inference('cnf', [status(esa)], [thm/iterate/POLYNOMIAL_FUNCTION_LMUL_])).
% 3.39/1.11 thf(zip_derived_cl57, plain,
% 3.39/1.11 (![X2 : 'type/realax/real' > 'type/realax/real']:
% 3.39/1.11 (((!!) @ (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ((('const/iterate/polynomial_function' @ X2) =>
% 3.39/1.11 ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y1 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ Y0 @ (X2 @ Y1)))))))))),
% 3.39/1.11 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl2])).
% 3.39/1.11 thf(zip_derived_cl58, plain,
% 3.39/1.11 (![X2 : 'type/realax/real' > 'type/realax/real', X4 : 'type/realax/real']:
% 3.39/1.11 ((('const/iterate/polynomial_function' @ X2) =>
% 3.39/1.11 ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ X4 @ (X2 @ Y0))))))),
% 3.39/1.11 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl57])).
% 3.39/1.11 thf(zip_derived_cl59, plain,
% 3.39/1.11 (![X2 : 'type/realax/real' > 'type/realax/real', X4 : 'type/realax/real']:
% 3.39/1.11 (~ ('const/iterate/polynomial_function' @ X2)
% 3.39/1.11 | ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ X4 @ (X2 @ Y0)))))),
% 3.39/1.11 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl58])).
% 3.39/1.11 thf(zip_derived_cl68, plain,
% 3.39/1.11 (![X0 : 'type/realax/real']:
% 3.39/1.11 ( ('const/iterate/polynomial_function' @ '#sk1')
% 3.39/1.11 | ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ X0 @
% 3.39/1.11 ((^[Y1 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y1))) @
% 3.39/1.11 Y0)))))),
% 3.39/1.11 inference('sup-', [status(thm)], [zip_derived_cl13, zip_derived_cl59])).
% 3.39/1.11 thf(zip_derived_cl69, plain,
% 3.39/1.11 (![X0 : 'type/realax/real']:
% 3.39/1.11 ( ('const/iterate/polynomial_function' @ '#sk1')
% 3.39/1.11 | ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ X0 @
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0))))))),
% 3.39/1.11 inference('ho_norm', [status(thm)], [zip_derived_cl68])).
% 3.39/1.11 thf(zip_derived_cl52, plain,
% 3.39/1.11 (![X2 : 'type/realax/real', X4 : 'type/realax/real']:
% 3.39/1.11 (('const/realax/real_mul' @ ('const/realax/real_neg' @ X2) @ X4)
% 3.39/1.11 = ('const/realax/real_neg' @ ('const/realax/real_mul' @ X2 @ X4)))),
% 3.39/1.11 inference('simplify nested equalities', [status(thm)], [zip_derived_cl51])).
% 3.39/1.11 thf(zip_derived_cl13, plain,
% 3.39/1.11 (( ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0))))
% 3.39/1.11 | ('const/iterate/polynomial_function' @ '#sk1'))),
% 3.39/1.11 inference('eq_elim', [status(thm)], [zip_derived_cl12])).
% 3.39/1.11 thf(zip_derived_cl59, plain,
% 3.39/1.11 (![X2 : 'type/realax/real' > 'type/realax/real', X4 : 'type/realax/real']:
% 3.39/1.11 (~ ('const/iterate/polynomial_function' @ X2)
% 3.39/1.11 | ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ X4 @ (X2 @ Y0)))))),
% 3.39/1.11 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl58])).
% 3.39/1.11 thf(zip_derived_cl12, plain,
% 3.39/1.11 ((('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']: ('const/realax/real_neg' @ ('#sk1' @ Y0))))
% 3.39/1.11 != ('const/iterate/polynomial_function' @ '#sk1'))),
% 3.39/1.11 inference('simplify nested equalities', [status(thm)], [zip_derived_cl11])).
% 3.39/1.11 thf(zip_derived_cl14, plain,
% 3.39/1.11 ((~ ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0))))
% 3.39/1.11 | ~ ('const/iterate/polynomial_function' @ '#sk1'))),
% 3.39/1.11 inference('eq_elim', [status(thm)], [zip_derived_cl12])).
% 3.39/1.11 thf(zip_derived_cl66, plain,
% 3.39/1.11 (![X0 : 'type/realax/real' > 'type/realax/real', X1 : 'type/realax/real']:
% 3.39/1.11 ((((^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ X1 @ (X0 @ Y0))))
% 3.39/1.11 != ((^[Y0 : 'type/realax/real']: ('#sk1' @ Y0))))
% 3.39/1.11 | ~ ('const/iterate/polynomial_function' @ X0)
% 3.39/1.11 | ~ ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))))),
% 3.39/1.11 inference('ext_sup', [status(thm)], [zip_derived_cl59, zip_derived_cl14])).
% 3.39/1.11 thf(zip_derived_cl70, plain,
% 3.39/1.11 (![X0 : 'type/realax/real' > 'type/realax/real', X1 : 'type/realax/real']:
% 3.39/1.11 ((((^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ X1 @ (X0 @ Y0))))
% 3.39/1.11 != ('#sk1'))
% 3.39/1.11 | ~ ('const/iterate/polynomial_function' @ X0)
% 3.39/1.11 | ~ ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))))),
% 3.39/1.11 inference('ho_norm', [status(thm)], [zip_derived_cl66])).
% 3.39/1.11 thf(zip_derived_cl77, plain,
% 3.39/1.11 (![X0 : 'type/realax/real' > 'type/realax/real', X1 : 'type/realax/real']:
% 3.39/1.11 ( ('const/iterate/polynomial_function' @ '#sk1')
% 3.39/1.11 | ~ ('const/iterate/polynomial_function' @ X0)
% 3.39/1.11 | (((^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ X1 @ (X0 @ Y0))))
% 3.39/1.11 != ('#sk1')))),
% 3.39/1.11 inference('sup-', [status(thm)], [zip_derived_cl13, zip_derived_cl70])).
% 3.39/1.11 thf(zip_derived_cl78, plain,
% 3.39/1.11 (![X0 : 'type/realax/real' > 'type/realax/real', X1 : 'type/realax/real']:
% 3.39/1.11 ( ('const/iterate/polynomial_function' @ '#sk1')
% 3.39/1.11 | ~ ('const/iterate/polynomial_function' @ X0)
% 3.39/1.11 | (('const/realax/real_mul' @ X1 @ (X0 @ ('#sk43' @ X0 @ X1)))
% 3.39/1.11 != ('#sk1' @ ('#sk43' @ X0 @ X1))))),
% 3.39/1.11 inference('neg_ext', [status(thm)], [zip_derived_cl77])).
% 3.39/1.11 thf(zip_derived_cl86, plain,
% 3.39/1.11 (![X0 : 'type/realax/real' > 'type/realax/real',
% 3.39/1.11 X1 : 'type/realax/real', X2 : 'type/realax/real' > 'type/realax/real']:
% 3.39/1.11 ((('const/realax/real_mul' @ X1 @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 (X2 @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @ (X2 @ Y0)) @ (X0 @ Y0))) @
% 3.39/1.11 X1)) @
% 3.39/1.11 (X0 @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @ (X2 @ Y0)) @ (X0 @ Y0))) @
% 3.39/1.11 X1)))))
% 3.39/1.11 != ('#sk1' @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ((^[Y1 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ (X2 @ Y1))) @
% 3.39/1.11 Y0) @
% 3.39/1.11 (X0 @ Y0))) @
% 3.39/1.11 X1)))
% 3.39/1.11 | ~ ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ((^[Y1 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ (X2 @ Y1))) @
% 3.39/1.11 Y0) @
% 3.39/1.11 (X0 @ Y0))))
% 3.39/1.11 | ('const/iterate/polynomial_function' @ '#sk1'))),
% 3.39/1.11 inference('sup-', [status(thm)], [zip_derived_cl52, zip_derived_cl78])).
% 3.39/1.11 thf(zip_derived_cl89, plain,
% 3.39/1.11 (![X0 : 'type/realax/real' > 'type/realax/real',
% 3.39/1.11 X1 : 'type/realax/real', X2 : 'type/realax/real' > 'type/realax/real']:
% 3.39/1.11 ((('const/realax/real_mul' @ X1 @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 (X2 @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @ (X2 @ Y0)) @ (X0 @ Y0))) @
% 3.39/1.11 X1)) @
% 3.39/1.11 (X0 @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @ (X2 @ Y0)) @ (X0 @ Y0))) @
% 3.39/1.11 X1)))))
% 3.39/1.11 != ('#sk1' @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @ (X2 @ Y0)) @ (X0 @ Y0))) @
% 3.39/1.11 X1)))
% 3.39/1.11 | ~ ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @ (X2 @ Y0)) @ (X0 @ Y0))))
% 3.39/1.11 | ('const/iterate/polynomial_function' @ '#sk1'))),
% 3.39/1.11 inference('ho_norm', [status(thm)], [zip_derived_cl86])).
% 3.39/1.11 thf(zip_derived_cl371, plain,
% 3.39/1.11 (![X0 : 'type/realax/real', X1 : 'type/realax/real']:
% 3.39/1.11 ( ('const/iterate/polynomial_function' @ '#sk1')
% 3.39/1.11 | ('const/iterate/polynomial_function' @ '#sk1')
% 3.39/1.11 | (('const/realax/real_mul' @ X1 @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ((^[Y0 : 'type/realax/real']: (X0)) @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ((^[Y1 : 'type/realax/real']: (X0)) @ Y0)) @
% 3.39/1.11 ((^[Y1 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y1))) @
% 3.39/1.11 Y0))) @
% 3.39/1.11 X1)) @
% 3.39/1.11 ((^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0))) @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ((^[Y1 : 'type/realax/real']: (X0)) @ Y0)) @
% 3.39/1.11 ((^[Y1 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y1))) @
% 3.39/1.11 Y0))) @
% 3.39/1.11 X1)))))
% 3.39/1.11 != ('#sk1' @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ((^[Y1 : 'type/realax/real']: (X0)) @ Y0)) @
% 3.39/1.11 ((^[Y1 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y1))) @
% 3.39/1.11 Y0))) @
% 3.39/1.11 X1))))),
% 3.39/1.11 inference('sup-', [status(thm)], [zip_derived_cl69, zip_derived_cl89])).
% 3.39/1.11 thf(zip_derived_cl398, plain,
% 3.39/1.11 (![X0 : 'type/realax/real', X1 : 'type/realax/real']:
% 3.39/1.11 ( ('const/iterate/polynomial_function' @ '#sk1')
% 3.39/1.11 | ('const/iterate/polynomial_function' @ '#sk1')
% 3.39/1.11 | (('const/realax/real_mul' @ X1 @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_mul' @ X0 @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('#sk1' @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @ X0) @
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))) @
% 3.39/1.11 X1))))))
% 3.39/1.11 != ('#sk1' @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @ X0) @
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))) @
% 3.39/1.11 X1))))),
% 3.39/1.11 inference('ho_norm', [status(thm)], [zip_derived_cl371])).
% 3.39/1.11 thf(zip_derived_cl399, plain,
% 3.39/1.11 (![X0 : 'type/realax/real', X1 : 'type/realax/real']:
% 3.39/1.11 ((('const/realax/real_mul' @ X1 @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_mul' @ X0 @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('#sk1' @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @ X0) @
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))) @
% 3.39/1.11 X1))))))
% 3.39/1.11 != ('#sk1' @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @ X0) @
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))) @
% 3.39/1.11 X1)))
% 3.39/1.11 | ('const/iterate/polynomial_function' @ '#sk1'))),
% 3.39/1.11 inference('simplify', [status(thm)], [zip_derived_cl398])).
% 3.39/1.11 thf(zip_derived_cl422, plain,
% 3.39/1.11 (![X0 : 'type/realax/real']:
% 3.39/1.11 ((('const/realax/real_mul' @ X0 @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('#sk1' @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @
% 3.39/1.11 ('const/nums/BIT1' @ 'const/nums/_0')))) @
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))) @
% 3.39/1.11 X0)))))
% 3.39/1.11 != ('#sk1' @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @
% 3.39/1.11 ('const/nums/BIT1' @ 'const/nums/_0')))) @
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))) @
% 3.39/1.11 X0)))
% 3.39/1.11 | ('const/iterate/polynomial_function' @ '#sk1'))),
% 3.39/1.11 inference('sup-', [status(thm)], [zip_derived_cl49, zip_derived_cl399])).
% 3.39/1.11 thf('thm/calc_int/REAL_NEG_NEG_', axiom,
% 3.39/1.11 (![A:'type/realax/real']:
% 3.39/1.11 ( ( 'const/realax/real_neg' @ ( 'const/realax/real_neg' @ A ) ) = ( A ) ))).
% 3.39/1.11 thf(zip_derived_cl3, plain,
% 3.39/1.11 ( (((!!) @ (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ((('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_neg' @ Y0)) = (Y0))))))),
% 3.39/1.11 inference('cnf', [status(esa)], [thm/calc_int/REAL_NEG_NEG_])).
% 3.39/1.11 thf(zip_derived_cl5, plain,
% 3.39/1.11 (![X2 : 'type/realax/real']:
% 3.39/1.11 ((('const/realax/real_neg' @ ('const/realax/real_neg' @ X2)) = (X2)))),
% 3.39/1.11 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl3])).
% 3.39/1.11 thf(zip_derived_cl6, plain,
% 3.39/1.11 (![X2 : 'type/realax/real']:
% 3.39/1.11 (('const/realax/real_neg' @ ('const/realax/real_neg' @ X2)) = (X2))),
% 3.39/1.11 inference('simplify nested equalities', [status(thm)], [zip_derived_cl5])).
% 3.39/1.11 thf(zip_derived_cl426, plain,
% 3.39/1.11 (![X0 : 'type/realax/real']:
% 3.39/1.11 ((('const/realax/real_mul' @ X0 @
% 3.39/1.11 ('#sk1' @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @
% 3.39/1.11 ('const/nums/BIT1' @ 'const/nums/_0')))) @
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))) @
% 3.39/1.11 X0)))
% 3.39/1.11 != ('#sk1' @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @
% 3.39/1.11 ('const/nums/BIT1' @ 'const/nums/_0')))) @
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))) @
% 3.39/1.11 X0)))
% 3.39/1.11 | ('const/iterate/polynomial_function' @ '#sk1'))),
% 3.39/1.11 inference('demod', [status(thm)], [zip_derived_cl422, zip_derived_cl6])).
% 3.39/1.11 thf(zip_derived_cl432, plain,
% 3.39/1.11 (((('#sk1' @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @ ('const/nums/BIT1' @ 'const/nums/_0')))) @
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))) @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @ ('const/nums/BIT1' @ 'const/nums/_0')))))
% 3.39/1.11 != ('#sk1' @
% 3.39/1.11 ('#sk43' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @
% 3.39/1.11 ('const/nums/BIT1' @ 'const/nums/_0')))) @
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))) @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @ ('const/nums/BIT1' @ 'const/nums/_0'))))))
% 3.39/1.11 | ('const/iterate/polynomial_function' @ '#sk1'))),
% 3.39/1.11 inference('sup-', [status(thm)], [zip_derived_cl49, zip_derived_cl426])).
% 3.39/1.11 thf(zip_derived_cl433, plain,
% 3.39/1.11 ( ('const/iterate/polynomial_function' @ '#sk1')),
% 3.39/1.11 inference('simplify', [status(thm)], [zip_derived_cl432])).
% 3.39/1.11 thf(zip_derived_cl59, plain,
% 3.39/1.11 (![X2 : 'type/realax/real' > 'type/realax/real', X4 : 'type/realax/real']:
% 3.39/1.11 (~ ('const/iterate/polynomial_function' @ X2)
% 3.39/1.11 | ('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ X4 @ (X2 @ Y0)))))),
% 3.39/1.11 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl58])).
% 3.39/1.11 thf(zip_derived_cl12, plain,
% 3.39/1.11 ((('const/iterate/polynomial_function' @
% 3.39/1.11 (^[Y0 : 'type/realax/real']: ('const/realax/real_neg' @ ('#sk1' @ Y0))))
% 3.39/1.11 != ('const/iterate/polynomial_function' @ '#sk1'))),
% 3.39/1.11 inference('simplify nested equalities', [status(thm)], [zip_derived_cl11])).
% 3.39/1.11 thf(zip_derived_cl63, plain,
% 3.39/1.11 (![X0 : 'type/realax/real' > 'type/realax/real', X1 : 'type/realax/real']:
% 3.39/1.11 ((((^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ X1 @ (X0 @ Y0))))
% 3.39/1.11 != ((^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))))
% 3.39/1.11 | ~ ('const/iterate/polynomial_function' @ X0)
% 3.39/1.11 | ~ ('const/iterate/polynomial_function' @ '#sk1'))),
% 3.39/1.11 inference('ext_sup', [status(thm)], [zip_derived_cl59, zip_derived_cl12])).
% 3.39/1.11 thf(zip_derived_cl433, plain,
% 3.39/1.11 ( ('const/iterate/polynomial_function' @ '#sk1')),
% 3.39/1.11 inference('simplify', [status(thm)], [zip_derived_cl432])).
% 3.39/1.11 thf(zip_derived_cl436, plain,
% 3.39/1.11 (![X0 : 'type/realax/real' > 'type/realax/real', X1 : 'type/realax/real']:
% 3.39/1.11 ((((^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ X1 @ (X0 @ Y0))))
% 3.39/1.11 != ((^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))))
% 3.39/1.11 | ~ ('const/iterate/polynomial_function' @ X0))),
% 3.39/1.11 inference('demod', [status(thm)], [zip_derived_cl63, zip_derived_cl433])).
% 3.39/1.11 thf(zip_derived_cl451, plain,
% 3.39/1.11 (![X0 : 'type/realax/real']:
% 3.39/1.11 (((^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_mul' @ X0 @ ('#sk1' @ Y0))))
% 3.39/1.11 != ((^[Y0 : 'type/realax/real']:
% 3.39/1.11 ('const/realax/real_neg' @ ('#sk1' @ Y0)))))),
% 3.39/1.11 inference('sup-', [status(thm)], [zip_derived_cl433, zip_derived_cl436])).
% 3.39/1.11 thf(zip_derived_cl461, plain,
% 3.39/1.11 (![X0 : 'type/realax/real']:
% 3.39/1.11 (('const/realax/real_mul' @ X0 @ ('#sk1' @ ('#sk418' @ X0)))
% 3.39/1.11 != ('const/realax/real_neg' @ ('#sk1' @ ('#sk418' @ X0))))),
% 3.39/1.11 inference('neg_ext', [status(thm)], [zip_derived_cl451])).
% 3.39/1.11 thf(zip_derived_cl462, plain,
% 3.39/1.11 (![X0 : 'type/realax/real']:
% 3.39/1.11 (('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_mul' @ X0 @
% 3.39/1.11 ('#sk1' @ ('#sk418' @ ('const/realax/real_neg' @ X0)))))
% 3.39/1.11 != ('const/realax/real_neg' @
% 3.39/1.11 ('#sk1' @ ('#sk418' @ ('const/realax/real_neg' @ X0)))))),
% 3.39/1.11 inference('sup-', [status(thm)], [zip_derived_cl52, zip_derived_cl461])).
% 3.39/1.11 thf(zip_derived_cl468, plain,
% 3.39/1.11 ((('const/realax/real_neg' @
% 3.39/1.11 ('#sk1' @
% 3.39/1.11 ('#sk418' @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @ ('const/nums/BIT1' @ 'const/nums/_0')))))))
% 3.39/1.11 != ('const/realax/real_neg' @
% 3.39/1.11 ('#sk1' @
% 3.39/1.11 ('#sk418' @
% 3.39/1.11 ('const/realax/real_neg' @
% 3.39/1.11 ('const/realax/real_of_num' @
% 3.39/1.11 ('const/nums/NUMERAL' @ ('const/nums/BIT1' @ 'const/nums/_0'))))))))),
% 3.39/1.11 inference('sup-', [status(thm)], [zip_derived_cl49, zip_derived_cl462])).
% 3.39/1.11 thf(zip_derived_cl474, plain, ($false),
% 3.39/1.11 inference('simplify', [status(thm)], [zip_derived_cl468])).
% 3.39/1.11
% 3.39/1.11 % SZS output end Refutation
% 3.39/1.11
% 3.39/1.11
% 3.39/1.11 % Terminating...
% 4.09/1.24 % Runner terminated.
% 4.09/1.25 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------