%------------------------------------------------------------------------------
% File : Lash---1.13
% Problem : ITP193^1 : TPTP v9.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : lash -P picomus -M modes -p tstp -t %d %s
% Computer : n028.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 9 01:45:24 PM UTC 2025
% Result : Theorem 83.45s 82.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : ITP193^1 : TPTP v9.2.0. Released v7.5.0.
% 0.08/0.13 % Command : lash -P picomus -M modes -p tstp -t %d %s
% 0.13/0.35 % Computer : n028.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 8 18:17:53 EDT 2025
% 0.13/0.35 % CPUTime :
% 83.45/82.93 % SZS status Theorem
% 83.45/82.93 % Mode: cade22sinegrackle2x1406
% 83.45/82.93 % Steps: 24082
% 83.45/82.93 % SZS output start Proof
% 83.45/82.93 thf(ty_real, type, real : $tType).
% 83.45/82.93 thf(ty_set_real, type, set_real : $tType).
% 83.45/82.93 thf(ty_finite_finite_real, type, finite_finite_real : (set_real>$o)).
% 83.45/82.93 thf(ty_ord_less_real, type, ord_less_real : (real>real>$o)).
% 83.45/82.93 thf(ty_ord_less_eq_set_real, type, ord_less_eq_set_real : (set_real>set_real>$o)).
% 83.45/82.93 thf(ty_b, type, b : real).
% 83.45/82.93 thf(ty_a, type, a : real).
% 83.45/82.93 thf(ty_p, type, p : poly_real).
% 83.45/82.93 thf(ty_poly_real2, type, poly_real2 : (poly_real>real>real)).
% 83.45/82.93 thf(ty_collect_real, type, collect_real : ((real>$o)>set_real)).
% 83.45/82.93 thf(ty_zero_zero_real, type, zero_zero_real : real).
% 83.45/82.93 thf(sP1,plain,sP1 <=> (![X1:set_real]:(![X2:set_real]:(((ord_less_eq_set_real @ X1) @ X2) => ((~((finite_finite_real @ X1))) => (~((finite_finite_real @ X2))))))),introduced(definition,[new_symbols(definition,[sP1])])).
% 83.45/82.93 thf(sP2,plain,sP2 <=> (((~(((~(((((poly_real2 @ p) @ (@+[X1:real]:(~(((~(((~(((((poly_real2 @ p) @ X1) = zero_zero_real) => (~(((ord_less_real @ a) @ X1)))))) => (~(((ord_less_real @ X1) @ b)))))) => (((poly_real2 @ p) @ X1) = zero_zero_real)))))) = zero_zero_real) => (~(((ord_less_real @ a) @ (@+[X1:real]:(~(((~(((~(((((poly_real2 @ p) @ X1) = zero_zero_real) => (~(((ord_less_real @ a) @ X1)))))) => (~(((ord_less_real @ X1) @ b)))))) => (((poly_real2 @ p) @ X1) = zero_zero_real))))))))))) => (~(((ord_less_real @ (@+[X1:real]:(~(((~(((~(((((poly_real2 @ p) @ X1) = zero_zero_real) => (~(((ord_less_real @ a) @ X1)))))) => (~(((ord_less_real @ X1) @ b)))))) => (((poly_real2 @ p) @ X1) = zero_zero_real)))))) @ b)))))) => (((poly_real2 @ p) @ (@+[X1:real]:(~(((~(((~(((((poly_real2 @ p) @ X1) = zero_zero_real) => (~(((ord_less_real @ a) @ X1)))))) => (~(((ord_less_real @ X1) @ b)))))) => (((poly_real2 @ p) @ X1) = zero_zero_real)))))) = zero_zero_real)) => ((ord_less_eq_set_real @ (collect_real @ (^[X1:real]:(~(((~(((((poly_real2 @ p) @ X1) = zero_zero_real) => (~(((ord_less_real @ a) @ X1)))))) => (~(((ord_less_real @ X1) @ b))))))))) @ (collect_real @ (^[X1:real]:(((poly_real2 @ p) @ X1) = zero_zero_real))))),introduced(definition,[new_symbols(definition,[sP2])])).
% 83.45/82.93 thf(sP3,plain,sP3 <=> (![X1:real>$o]:(((~(((~(((((poly_real2 @ p) @ (@+[X2:real]:(~(((~(((~(((((poly_real2 @ p) @ X2) = zero_zero_real) => (~(((ord_less_real @ a) @ X2)))))) => (~(((ord_less_real @ X2) @ b)))))) => (X1 @ X2)))))) = zero_zero_real) => (~(((ord_less_real @ a) @ (@+[X2:real]:(~(((~(((~(((((poly_real2 @ p) @ X2) = zero_zero_real) => (~(((ord_less_real @ a) @ X2)))))) => (~(((ord_less_real @ X2) @ b)))))) => (X1 @ X2))))))))))) => (~(((ord_less_real @ (@+[X2:real]:(~(((~(((~(((((poly_real2 @ p) @ X2) = zero_zero_real) => (~(((ord_less_real @ a) @ X2)))))) => (~(((ord_less_real @ X2) @ b)))))) => (X1 @ X2)))))) @ b)))))) => (X1 @ (@+[X2:real]:(~(((~(((~(((((poly_real2 @ p) @ X2) = zero_zero_real) => (~(((ord_less_real @ a) @ X2)))))) => (~(((ord_less_real @ X2) @ b)))))) => (X1 @ X2))))))) => ((ord_less_eq_set_real @ (collect_real @ (^[X2:real]:(~(((~(((((poly_real2 @ p) @ X2) = zero_zero_real) => (~(((ord_less_real @ a) @ X2)))))) => (~(((ord_less_real @ X2) @ b))))))))) @ (collect_real @ X1)))),introduced(definition,[new_symbols(definition,[sP3])])).
% 83.45/82.93 thf(sP4,plain,sP4 <=> ((((poly_real2 @ p) @ (@+[X1:real]:(~(((~(((~(((((poly_real2 @ p) @ X1) = zero_zero_real) => (~(((ord_less_real @ a) @ X1)))))) => (~(((ord_less_real @ X1) @ b)))))) => (((poly_real2 @ p) @ X1) = zero_zero_real)))))) = zero_zero_real) => (~(((ord_less_real @ a) @ (@+[X1:real]:(~(((~(((~(((((poly_real2 @ p) @ X1) = zero_zero_real) => (~(((ord_less_real @ a) @ X1)))))) => (~(((ord_less_real @ X1) @ b)))))) => (((poly_real2 @ p) @ X1) = zero_zero_real))))))))),introduced(definition,[new_symbols(definition,[sP4])])).
% 83.45/82.93 thf(sP5,plain,sP5 <=> ((~(sP4)) => (~(((ord_less_real @ (@+[X1:real]:(~(((~(((~(((((poly_real2 @ p) @ X1) = zero_zero_real) => (~(((ord_less_real @ a) @ X1)))))) => (~(((ord_less_real @ X1) @ b)))))) => (((poly_real2 @ p) @ X1) = zero_zero_real)))))) @ b)))),introduced(definition,[new_symbols(definition,[sP5])])).
% 83.45/82.93 thf(sP6,plain,sP6 <=> (((poly_real2 @ p) @ (@+[X1:real]:(~(((~(((~(((((poly_real2 @ p) @ X1) = zero_zero_real) => (~(((ord_less_real @ a) @ X1)))))) => (~(((ord_less_real @ X1) @ b)))))) => (((poly_real2 @ p) @ X1) = zero_zero_real)))))) = zero_zero_real),introduced(definition,[new_symbols(definition,[sP6])])).
% 83.45/82.93 thf(sP7,plain,sP7 <=> (![X1:set_real]:(((ord_less_eq_set_real @ (collect_real @ (^[X2:real]:(~(((~(((((poly_real2 @ p) @ X2) = zero_zero_real) => (~(((ord_less_real @ a) @ X2)))))) => (~(((ord_less_real @ X2) @ b))))))))) @ X1) => ((~((finite_finite_real @ (collect_real @ (^[X2:real]:(~(((~(((((poly_real2 @ p) @ X2) = zero_zero_real) => (~(((ord_less_real @ a) @ X2)))))) => (~(((ord_less_real @ X2) @ b))))))))))) => (~((finite_finite_real @ X1)))))),introduced(definition,[new_symbols(definition,[sP7])])).
% 83.45/82.93 thf(sP8,plain,sP8 <=> ((ord_less_eq_set_real @ (collect_real @ (^[X1:real]:(~(((~(((((poly_real2 @ p) @ X1) = zero_zero_real) => (~(((ord_less_real @ a) @ X1)))))) => (~(((ord_less_real @ X1) @ b))))))))) @ (collect_real @ (^[X1:real]:(((poly_real2 @ p) @ X1) = zero_zero_real)))),introduced(definition,[new_symbols(definition,[sP8])])).
% 83.45/82.93 thf(sP9,plain,sP9 <=> (sP8 => ((~((finite_finite_real @ (collect_real @ (^[X1:real]:(~(((~(((((poly_real2 @ p) @ X1) = zero_zero_real) => (~(((ord_less_real @ a) @ X1)))))) => (~(((ord_less_real @ X1) @ b))))))))))) => (~((finite_finite_real @ (collect_real @ (^[X1:real]:(((poly_real2 @ p) @ X1) = zero_zero_real)))))))),introduced(definition,[new_symbols(definition,[sP9])])).
% 83.45/82.93 thf(sP10,plain,sP10 <=> (finite_finite_real @ (collect_real @ (^[X1:real]:(((poly_real2 @ p) @ X1) = zero_zero_real)))),introduced(definition,[new_symbols(definition,[sP10])])).
% 83.45/82.93 thf(sP11,plain,sP11 <=> ((~((finite_finite_real @ (collect_real @ (^[X1:real]:(~(((~(((((poly_real2 @ p) @ X1) = zero_zero_real) => (~(((ord_less_real @ a) @ X1)))))) => (~(((ord_less_real @ X1) @ b))))))))))) => (~(sP10))),introduced(definition,[new_symbols(definition,[sP11])])).
% 83.45/82.93 thf(sP12,plain,sP12 <=> ((~(sP5)) => sP6),introduced(definition,[new_symbols(definition,[sP12])])).
% 83.45/82.93 thf(sP13,plain,sP13 <=> (finite_finite_real @ (collect_real @ (^[X1:real]:(~(((~(((((poly_real2 @ p) @ X1) = zero_zero_real) => (~(((ord_less_real @ a) @ X1)))))) => (~(((ord_less_real @ X1) @ b))))))))),introduced(definition,[new_symbols(definition,[sP13])])).
% 83.45/82.93 thf(sP14,plain,sP14 <=> (![X1:real>$o]:(![X2:real>$o]:(((X1 @ (@+[X3:real]:(~(((X1 @ X3) => (X2 @ X3)))))) => (X2 @ (@+[X3:real]:(~(((X1 @ X3) => (X2 @ X3))))))) => ((ord_less_eq_set_real @ (collect_real @ X1)) @ (collect_real @ X2))))),introduced(definition,[new_symbols(definition,[sP14])])).
% 83.45/82.93 thf(conj_0,conjecture,sP13).
% 83.45/82.93 thf(h0,negated_conjecture,(~(sP13)),inference(assume_negation,[status(cth)],[conj_0])).
% 83.45/82.93 thf(1,plain,(sP4 | sP6),inference(prop_rule,[status(thm)],[])).
% 83.45/82.93 thf(2,plain,(sP5 | ~(sP4)),inference(prop_rule,[status(thm)],[])).
% 83.45/82.93 thf(3,plain,((~(sP11) | sP13) | ~(sP10)),inference(prop_rule,[status(thm)],[])).
% 83.45/82.93 thf(4,plain,(sP12 | ~(sP6)),inference(prop_rule,[status(thm)],[])).
% 83.45/82.93 thf(5,plain,(sP12 | ~(sP5)),inference(prop_rule,[status(thm)],[])).
% 83.45/82.93 thf(6,plain,((~(sP2) | ~(sP12)) | sP8),inference(prop_rule,[status(thm)],[])).
% 83.45/82.93 thf(7,plain,((~(sP9) | ~(sP8)) | sP11),inference(prop_rule,[status(thm)],[])).
% 83.45/82.93 thf(8,plain,(~(sP3) | sP2),inference(all_rule,[status(thm)],[])).
% 83.45/82.93 thf(9,plain,(~(sP7) | sP9),inference(all_rule,[status(thm)],[])).
% 83.45/82.93 thf(10,plain,(~(sP14) | sP3),inference(all_rule,[status(thm)],[])).
% 83.45/82.93 thf(11,plain,(~(sP1) | sP7),inference(all_rule,[status(thm)],[])).
% 83.45/82.93 1:1129: Could not find hyp name
% 83.45/82.93 s = Pi:real>$o (\_:real>$o.Pi:real>$o (\_:real>$o.imp (imp (^1 (Sepsilon:real (\_:real.imp (imp (^2 ^0) (^1 ^0)) False))) (^0 (Sepsilon:real (\_:real.imp (imp (^2 ^0) (^1 ^0)) False)))) (ord_less_eq_set_real (collect_real ^1) (collect_real ^0))))
% 83.45/82.93 hyp:
% 83.45/82.93 [1110] h0: imp (finite_finite_real (collect_real (\_:real.imp (imp (imp (imp (eq:real (poly_real2 p ^0) zero_zero_real) (imp (ord_less_real a ^0) False)) False) (imp (ord_less_real ^0 b) False)) False))) False
% 83.45/82.93 % SZS status Error
% 83.45/82.93 Exception: Failure("Could not find hyp name")
%------------------------------------------------------------------------------