%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : ITP023+1 : TPTP v8.1.0. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n027.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 : 600s
% DateTime : Sat Jul 16 23:40:41 EDT 2022
% Result : Theorem 0.42s 1.41s
% Output : Proof 0.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ITP023+1 : TPTP v8.1.0. Bugfixed v7.5.0.
% 0.12/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n027.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 : 600
% 0.13/0.34 % DateTime : Thu Jun 2 13:18:20 EDT 2022
% 0.19/0.34 % CPUTime :
% 0.42/1.41 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/1.42 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/1.43
% 0.42/1.43 %-----------------------------------------------------
% 0.42/1.43 fof(thm_2Ereal__topology_2EBOUNDED__BALL, conjecture, ! [_152332, _152335] : p(s(tyop_2Emin_2Ebool, c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, _152332), s(tyop_2Erealax_2Ereal, _152335)))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thm_2Ereal__topology_2EBOUNDED__BALL)).
% 0.42/1.43 fof(thm_2Ereal__topology_2EBALL__SUBSET__CBALL, axiom, ! [_152683, _152686] : p(s(tyop_2Emin_2Ebool, c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, _152683), s(tyop_2Erealax_2Ereal, _152686))))), s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, _152683), s(tyop_2Erealax_2Ereal, _152686)))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thm_2Ereal__topology_2EBALL__SUBSET__CBALL)).
% 0.42/1.43 fof(thm_2Ereal__topology_2EBOUNDED__SUBSET, axiom, ! [_153068, _153071] : (p(s(tyop_2Emin_2Ebool, c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), _153071)))) & p(s(tyop_2Emin_2Ebool, c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), _153068), s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), _153071)))) => p(s(tyop_2Emin_2Ebool, c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), _153068))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thm_2Ereal__topology_2EBOUNDED__SUBSET)).
% 0.42/1.43 fof(thm_2Ereal__topology_2EBOUNDED__CBALL, axiom, ! [_153431, _153434] : p(s(tyop_2Emin_2Ebool, c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, _153431), s(tyop_2Erealax_2Ereal, _153434)))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thm_2Ereal__topology_2EBOUNDED__CBALL)).
% 0.42/1.43
% 0.42/1.43 cnf(1, plain, [p(s(tyop_2Emin_2Ebool, c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, 6 ^ []), s(tyop_2Erealax_2Ereal, 7 ^ []))))))))], clausify(thm_2Ereal__topology_2EBOUNDED__BALL)).
% 0.42/1.43 cnf(2, plain, [-(p(s(tyop_2Emin_2Ebool, c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, _82944), s(tyop_2Erealax_2Ereal, _83022))))), s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, _82944), s(tyop_2Erealax_2Ereal, _83022)))))))))], clausify(thm_2Ereal__topology_2EBALL__SUBSET__CBALL)).
% 0.42/1.43 cnf(3, plain, [-(p(s(tyop_2Emin_2Ebool, c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), _83849))))), p(s(tyop_2Emin_2Ebool, c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), _83925)))), p(s(tyop_2Emin_2Ebool, c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), _83849), s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), _83925))))], clausify(thm_2Ereal__topology_2EBOUNDED__SUBSET)).
% 0.42/1.43 cnf(4, plain, [-(p(s(tyop_2Emin_2Ebool, c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, _84708), s(tyop_2Erealax_2Ereal, _84768)))))))))], clausify(thm_2Ereal__topology_2EBOUNDED__CBALL)).
% 0.42/1.43
% 0.42/1.43 cnf('1',plain,[p(s(tyop_2Emin_2Ebool, c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, 6 ^ []), s(tyop_2Erealax_2Ereal, 7 ^ []))))))))],start(1)).
% 0.42/1.43 cnf('1.1',plain,[-(p(s(tyop_2Emin_2Ebool, c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, 6 ^ []), s(tyop_2Erealax_2Ereal, 7 ^ []))))))))), p(s(tyop_2Emin_2Ebool, c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, 6 ^ []), s(tyop_2Erealax_2Ereal, 7 ^ [])))))))), p(s(tyop_2Emin_2Ebool, c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, 6 ^ []), s(tyop_2Erealax_2Ereal, 7 ^ []))))), s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, 6 ^ []), s(tyop_2Erealax_2Ereal, 7 ^ []))))))))],extension(3,bind([[_83849, _83925], [c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, 6 ^ []), s(tyop_2Erealax_2Ereal, 7 ^ [])))), c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, 6 ^ []), s(tyop_2Erealax_2Ereal, 7 ^ []))))]]))).
% 0.42/1.43 cnf('1.1.1',plain,[-(p(s(tyop_2Emin_2Ebool, c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, 6 ^ []), s(tyop_2Erealax_2Ereal, 7 ^ [])))))))))],extension(4,bind([[_84708, _84768], [6 ^ [], 7 ^ []]]))).
% 0.42/1.43 cnf('1.1.2',plain,[-(p(s(tyop_2Emin_2Ebool, c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, 6 ^ []), s(tyop_2Erealax_2Ereal, 7 ^ []))))), s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal, tyop_2Emin_2Ebool), c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal, tyop_2Erealax_2Ereal), c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal, 6 ^ []), s(tyop_2Erealax_2Ereal, 7 ^ [])))))))))],extension(2,bind([[_82944, _83022], [6 ^ [], 7 ^ []]]))).
% 0.42/1.43 %-----------------------------------------------------
% 0.42/1.43
% 0.42/1.43 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------