%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO094+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n010.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 05:02:37 EDT 2022
% Result : Theorem 163.18s 157.08s
% Output : Proof 163.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : GEO094+1 : TPTP v8.1.0. Released v2.4.0.
% 0.10/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n010.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Fri Jun 17 15:59:53 EDT 2022
% 0.12/0.34 % CPUTime :
% 163.18/157.08 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 163.18/157.09 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 163.26/157.09
% 163.26/157.09 %-----------------------------------------------------
% 163.26/157.09 fof(proposition_2_14_3, conjecture, ! [_49864, _49867, _49870, _49873] : (meet(_49873, _49867, _49870) & part_of(_49867, _49864) & part_of(_49870, _49864) => ~ end_point(_49873, _49864)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', proposition_2_14_3)).
% 163.26/157.09 fof(part_of_defn, axiom, ! [_50170, _50173] : (part_of(_50173, _50170) <=> ! [_50191] : (incident_c(_50191, _50173) => incident_c(_50191, _50170))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax', part_of_defn)).
% 163.26/157.09 fof(end_point_defn, axiom, ! [_50387, _50390] : (end_point(_50387, _50390) <=> incident_c(_50387, _50390) & ! [_50418, _50421] : (part_of(_50418, _50390) & part_of(_50421, _50390) & incident_c(_50387, _50418) & incident_c(_50387, _50421) => part_of(_50418, _50421) | part_of(_50421, _50418))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax', end_point_defn)).
% 163.26/157.09 fof(inner_point_defn, axiom, ! [_50742, _50745] : (inner_point(_50742, _50745) <=> incident_c(_50742, _50745) & ~ end_point(_50742, _50745)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax', inner_point_defn)).
% 163.26/157.09 fof(meet_defn, axiom, ! [_50936, _50939, _50942] : (meet(_50936, _50939, _50942) <=> incident_c(_50936, _50939) & incident_c(_50936, _50942) & ! [_50983] : (incident_c(_50983, _50939) & incident_c(_50983, _50942) => end_point(_50983, _50939) & end_point(_50983, _50942))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax', meet_defn)).
% 163.26/157.09 fof(c3, axiom, ! [_51315] : ? [_51323] : inner_point(_51323, _51315), file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax', c3)).
% 163.26/157.09
% 163.26/157.09 cnf(1, plain, [-(meet(17 ^ [], 15 ^ [], 16 ^ []))], clausify(proposition_2_14_3)).
% 163.26/157.09 cnf(2, plain, [-(part_of(15 ^ [], 14 ^ []))], clausify(proposition_2_14_3)).
% 163.26/157.09 cnf(3, plain, [-(part_of(16 ^ [], 14 ^ []))], clausify(proposition_2_14_3)).
% 163.26/157.09 cnf(4, plain, [-(end_point(17 ^ [], 14 ^ []))], clausify(proposition_2_14_3)).
% 163.26/157.09 cnf(5, plain, [-(_12306 = _12306)], theory(equality)).
% 163.26/157.09 cnf(6, plain, [-(inner_point(_14858, _14989)), inner_point(_14791, _14924), _14791 = _14858, _14924 = _14989], theory(equality)).
% 163.26/157.09 cnf(7, plain, [part_of(_18194, _18138), incident_c(_18308, _18194), -(incident_c(_18308, _18138))], clausify(part_of_defn)).
% 163.26/157.09 cnf(8, plain, [end_point(_19284, _19375), -(part_of(_19660, _19583)), -(part_of(_19583, _19660)), part_of(_19583, _19375), part_of(_19660, _19375), incident_c(_19284, _19583), incident_c(_19284, _19660)], clausify(end_point_defn)).
% 163.26/157.09 cnf(9, plain, [inner_point(_20297, _20350), -(incident_c(_20297, _20350))], clausify(inner_point_defn)).
% 163.26/157.09 cnf(10, plain, [inner_point(_20297, _20350), end_point(_20297, _20350)], clausify(inner_point_defn)).
% 163.26/157.09 cnf(11, plain, [meet(_20713, _20799, _20884), -(incident_c(_20713, _20799))], clausify(meet_defn)).
% 163.26/157.09 cnf(12, plain, [meet(_20713, _20799, _20884), -(incident_c(_20713, _20884))], clausify(meet_defn)).
% 163.26/157.09 cnf(13, plain, [meet(_20713, _20799, _20884), -(end_point(_21185, _20799)), incident_c(_21185, _20799), incident_c(_21185, _20884)], clausify(meet_defn)).
% 163.26/157.09 cnf(14, plain, [meet(_20713, _20799, _20884), -(end_point(_21185, _20884)), incident_c(_21185, _20799), incident_c(_21185, _20884)], clausify(meet_defn)).
% 163.26/157.09 cnf(15, plain, [-(inner_point(8 ^ [_24173], _24173))], clausify(c3)).
% 163.26/157.09
% 163.26/157.09 cnf('1',plain,[-(part_of(15 ^ [], 14 ^ []))],start(2)).
% 163.26/157.09 cnf('1.1',plain,[part_of(15 ^ [], 14 ^ []), end_point(17 ^ [], 14 ^ []), -(part_of(15 ^ [], 16 ^ [])), -(part_of(16 ^ [], 15 ^ [])), part_of(16 ^ [], 14 ^ []), incident_c(17 ^ [], 16 ^ []), incident_c(17 ^ [], 15 ^ [])],extension(8,bind([[_19375, _19583, _19284, _19660], [14 ^ [], 16 ^ [], 17 ^ [], 15 ^ []]]))).
% 163.26/157.09 cnf('1.1.1',plain,[-(end_point(17 ^ [], 14 ^ []))],extension(4)).
% 163.26/157.09 cnf('1.1.2',plain,[part_of(15 ^ [], 16 ^ []), incident_c(8 ^ [15 ^ []], 15 ^ []), -(incident_c(8 ^ [15 ^ []], 16 ^ []))],extension(7,bind([[_18194, _18308, _18138], [15 ^ [], 8 ^ [15 ^ []], 16 ^ []]]))).
% 163.26/157.09 cnf('1.1.2.1',plain,[-(incident_c(8 ^ [15 ^ []], 15 ^ [])), inner_point(8 ^ [15 ^ []], 15 ^ [])],extension(9,bind([[_20297, _20350], [8 ^ [15 ^ []], 15 ^ []]]))).
% 163.26/157.09 cnf('1.1.2.1.1',plain,[-(inner_point(8 ^ [15 ^ []], 15 ^ [])), inner_point(8 ^ [15 ^ []], 15 ^ []), 8 ^ [15 ^ []] = 8 ^ [15 ^ []], 15 ^ [] = 15 ^ []],extension(6,bind([[_14791, _14858, _14924, _14989], [8 ^ [15 ^ []], 8 ^ [15 ^ []], 15 ^ [], 15 ^ []]]))).
% 163.26/157.09 cnf('1.1.2.1.1.1',plain,[-(inner_point(8 ^ [15 ^ []], 15 ^ []))],extension(15,bind([[_24173], [15 ^ []]]))).
% 163.26/157.09 cnf('1.1.2.1.1.2',plain,[-(8 ^ [15 ^ []] = 8 ^ [15 ^ []])],extension(5,bind([[_12306], [8 ^ [15 ^ []]]]))).
% 163.26/157.09 cnf('1.1.2.1.1.3',plain,[-(15 ^ [] = 15 ^ [])],extension(5,bind([[_12306], [15 ^ []]]))).
% 163.26/157.09 cnf('1.1.2.2',plain,[incident_c(8 ^ [15 ^ []], 16 ^ []), meet(17 ^ [], 15 ^ [], 16 ^ []), -(end_point(8 ^ [15 ^ []], 15 ^ [])), incident_c(8 ^ [15 ^ []], 15 ^ [])],extension(13,bind([[_20713, _20884, _21185, _20799], [17 ^ [], 16 ^ [], 8 ^ [15 ^ []], 15 ^ []]]))).
% 163.26/157.09 cnf('1.1.2.2.1',plain,[-(meet(17 ^ [], 15 ^ [], 16 ^ []))],extension(1)).
% 163.26/157.09 cnf('1.1.2.2.2',plain,[end_point(8 ^ [15 ^ []], 15 ^ []), inner_point(8 ^ [15 ^ []], 15 ^ [])],extension(10,bind([[_20297, _20350], [8 ^ [15 ^ []], 15 ^ []]]))).
% 163.26/157.09 cnf('1.1.2.2.2.1',plain,[-(inner_point(8 ^ [15 ^ []], 15 ^ []))],extension(15,bind([[_24173], [15 ^ []]]))).
% 163.26/157.09 cnf('1.1.2.2.3',plain,[-(incident_c(8 ^ [15 ^ []], 15 ^ []))],lemmata('1.1.2')).
% 163.26/157.09 cnf('1.1.3',plain,[part_of(16 ^ [], 15 ^ []), incident_c(8 ^ [16 ^ []], 16 ^ []), -(incident_c(8 ^ [16 ^ []], 15 ^ []))],extension(7,bind([[_18194, _18308, _18138], [16 ^ [], 8 ^ [16 ^ []], 15 ^ []]]))).
% 163.26/157.09 cnf('1.1.3.1',plain,[-(incident_c(8 ^ [16 ^ []], 16 ^ [])), inner_point(8 ^ [16 ^ []], 16 ^ [])],extension(9,bind([[_20297, _20350], [8 ^ [16 ^ []], 16 ^ []]]))).
% 163.26/157.09 cnf('1.1.3.1.1',plain,[-(inner_point(8 ^ [16 ^ []], 16 ^ [])), inner_point(8 ^ [16 ^ []], 16 ^ []), 8 ^ [16 ^ []] = 8 ^ [16 ^ []], 16 ^ [] = 16 ^ []],extension(6,bind([[_14791, _14858, _14924, _14989], [8 ^ [16 ^ []], 8 ^ [16 ^ []], 16 ^ [], 16 ^ []]]))).
% 163.26/157.09 cnf('1.1.3.1.1.1',plain,[-(inner_point(8 ^ [16 ^ []], 16 ^ []))],extension(15,bind([[_24173], [16 ^ []]]))).
% 163.26/157.09 cnf('1.1.3.1.1.2',plain,[-(8 ^ [16 ^ []] = 8 ^ [16 ^ []])],extension(5,bind([[_12306], [8 ^ [16 ^ []]]]))).
% 163.26/157.09 cnf('1.1.3.1.1.3',plain,[-(16 ^ [] = 16 ^ [])],extension(5,bind([[_12306], [16 ^ []]]))).
% 163.26/157.09 cnf('1.1.3.2',plain,[incident_c(8 ^ [16 ^ []], 15 ^ []), meet(17 ^ [], 15 ^ [], 16 ^ []), -(end_point(8 ^ [16 ^ []], 16 ^ [])), incident_c(8 ^ [16 ^ []], 16 ^ [])],extension(14,bind([[_20713, _20799, _21185, _20884], [17 ^ [], 15 ^ [], 8 ^ [16 ^ []], 16 ^ []]]))).
% 163.26/157.09 cnf('1.1.3.2.1',plain,[-(meet(17 ^ [], 15 ^ [], 16 ^ []))],extension(1)).
% 163.26/157.09 cnf('1.1.3.2.2',plain,[end_point(8 ^ [16 ^ []], 16 ^ []), inner_point(8 ^ [16 ^ []], 16 ^ [])],extension(10,bind([[_20297, _20350], [8 ^ [16 ^ []], 16 ^ []]]))).
% 163.26/157.09 cnf('1.1.3.2.2.1',plain,[-(inner_point(8 ^ [16 ^ []], 16 ^ []))],extension(15,bind([[_24173], [16 ^ []]]))).
% 163.26/157.09 cnf('1.1.3.2.3',plain,[-(incident_c(8 ^ [16 ^ []], 16 ^ []))],lemmata('1.1.3')).
% 163.26/157.09 cnf('1.1.4',plain,[-(part_of(16 ^ [], 14 ^ []))],extension(3)).
% 163.26/157.09 cnf('1.1.5',plain,[-(incident_c(17 ^ [], 16 ^ [])), meet(17 ^ [], 15 ^ [], 16 ^ [])],extension(12,bind([[_20713, _20799, _20884], [17 ^ [], 15 ^ [], 16 ^ []]]))).
% 163.26/157.09 cnf('1.1.5.1',plain,[-(meet(17 ^ [], 15 ^ [], 16 ^ []))],extension(1)).
% 163.26/157.09 cnf('1.1.6',plain,[-(incident_c(17 ^ [], 15 ^ [])), meet(17 ^ [], 15 ^ [], 16 ^ [])],extension(11,bind([[_20713, _20799, _20884], [17 ^ [], 15 ^ [], 16 ^ []]]))).
% 163.26/157.09 cnf('1.1.6.1',plain,[-(meet(17 ^ [], 15 ^ [], 16 ^ []))],extension(1)).
% 163.26/157.09 %-----------------------------------------------------
% 163.26/157.10
% 163.26/157.10 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------