%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO089+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n018.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:35 EDT 2022
% Result : Theorem 23.03s 23.07s
% Output : Proof 23.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : GEO089+1 : TPTP v8.1.0. Released v2.4.0.
% 0.06/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.32 % Computer : n018.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 600
% 0.11/0.32 % DateTime : Fri Jun 17 19:55:02 EDT 2022
% 0.11/0.33 % CPUTime :
% 23.03/23.07 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.03/23.08 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.03/23.08
% 23.03/23.08 %-----------------------------------------------------
% 23.03/23.08 fof(corollary_2_11, conjecture, ! [_63022, _63025] : (? [_63033] : (part_of(_63033, _63022) & inner_point(_63025, _63033)) => inner_point(_63025, _63022)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', corollary_2_11)).
% 23.03/23.08 fof(part_of_defn, axiom, ! [_63314, _63317] : (part_of(_63317, _63314) <=> ! [_63335] : (incident_c(_63335, _63317) => incident_c(_63335, _63314))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax', part_of_defn)).
% 23.03/23.08 fof(sum_defn, axiom, ! [_63543, _63546, _63549] : (_63543 = sum(_63546, _63549) <=> ! [_63570] : (incident_c(_63570, _63543) <=> incident_c(_63570, _63546) | incident_c(_63570, _63549))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax', sum_defn)).
% 23.03/23.08 fof(end_point_defn, axiom, ! [_63813, _63816] : (end_point(_63813, _63816) <=> incident_c(_63813, _63816) & ! [_63844, _63847] : (part_of(_63844, _63816) & part_of(_63847, _63816) & incident_c(_63813, _63844) & incident_c(_63813, _63847) => part_of(_63844, _63847) | part_of(_63847, _63844))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax', end_point_defn)).
% 23.03/23.08 fof(inner_point_defn, axiom, ! [_64241, _64244] : (inner_point(_64241, _64244) <=> incident_c(_64241, _64244) & ~ end_point(_64241, _64244)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax', inner_point_defn)).
% 23.03/23.08
% 23.03/23.08 cnf(1, plain, [-(part_of(16 ^ [], 14 ^ []))], clausify(corollary_2_11)).
% 23.03/23.08 cnf(2, plain, [-(inner_point(15 ^ [], 16 ^ []))], clausify(corollary_2_11)).
% 23.03/23.08 cnf(3, plain, [inner_point(15 ^ [], 14 ^ [])], clausify(corollary_2_11)).
% 23.03/23.08 cnf(4, plain, [-(sum(_17348, _17481) = sum(_17415, _17546)), _17348 = _17415, _17481 = _17546], theory(equality)).
% 23.03/23.08 cnf(5, plain, [-(_12176 = _12176)], theory(equality)).
% 23.03/23.08 cnf(6, plain, [-(end_point(_13480, _13611)), end_point(_13413, _13546), _13413 = _13480, _13546 = _13611], theory(equality)).
% 23.03/23.08 cnf(7, plain, [-(incident_c(_14104, _14235)), incident_c(_14037, _14170), _14037 = _14104, _14170 = _14235], theory(equality)).
% 23.03/23.08 cnf(8, plain, [-(part_of(_16696, _16827)), part_of(_16629, _16762), _16629 = _16696, _16762 = _16827], theory(equality)).
% 23.03/23.08 cnf(9, plain, [-(part_of(_18064, _18008)), -(incident_c(1 ^ [_18064, _18008], _18064))], clausify(part_of_defn)).
% 23.03/23.08 cnf(10, plain, [-(part_of(_18064, _18008)), incident_c(1 ^ [_18064, _18008], _18008)], clausify(part_of_defn)).
% 23.03/23.08 cnf(11, plain, [part_of(_18064, _18008), incident_c(_18178, _18064), -(incident_c(_18178, _18008))], clausify(part_of_defn)).
% 23.03/23.08 cnf(12, plain, [_18469 = sum(_18539, _18608), -(incident_c(_18772, _18469)), incident_c(_18772, _18608)], clausify(sum_defn)).
% 23.03/23.08 cnf(13, plain, [_18469 = sum(_18539, _18608), incident_c(_18772, _18469), -(incident_c(_18772, _18539)), -(incident_c(_18772, _18608))], clausify(sum_defn)).
% 23.03/23.08 cnf(14, plain, [-(end_point(_19154, _19245)), incident_c(_19154, _19245), -(part_of(3 ^ [_19245, _19154], _19245))], clausify(end_point_defn)).
% 23.03/23.08 cnf(15, plain, [-(end_point(_19154, _19245)), incident_c(_19154, _19245), -(part_of(4 ^ [_19245, _19154], _19245))], clausify(end_point_defn)).
% 23.03/23.08 cnf(16, plain, [-(end_point(_19154, _19245)), incident_c(_19154, _19245), -(incident_c(_19154, 3 ^ [_19245, _19154]))], clausify(end_point_defn)).
% 23.03/23.08 cnf(17, plain, [-(end_point(_19154, _19245)), incident_c(_19154, _19245), -(incident_c(_19154, 4 ^ [_19245, _19154]))], clausify(end_point_defn)).
% 23.03/23.08 cnf(18, plain, [-(end_point(_19154, _19245)), incident_c(_19154, _19245), part_of(3 ^ [_19245, _19154], 4 ^ [_19245, _19154])], clausify(end_point_defn)).
% 23.03/23.08 cnf(19, plain, [-(end_point(_19154, _19245)), incident_c(_19154, _19245), part_of(4 ^ [_19245, _19154], 3 ^ [_19245, _19154])], clausify(end_point_defn)).
% 23.03/23.08 cnf(20, plain, [end_point(_19154, _19245), -(part_of(_19530, _19453)), -(part_of(_19453, _19530)), part_of(_19453, _19245), part_of(_19530, _19245), incident_c(_19154, _19453), incident_c(_19154, _19530)], clausify(end_point_defn)).
% 23.03/23.08 cnf(21, plain, [inner_point(_20167, _20220), -(incident_c(_20167, _20220))], clausify(inner_point_defn)).
% 23.03/23.08 cnf(22, plain, [inner_point(_20167, _20220), end_point(_20167, _20220)], clausify(inner_point_defn)).
% 23.03/23.08 cnf(23, plain, [-(inner_point(_20167, _20220)), incident_c(_20167, _20220), -(end_point(_20167, _20220))], clausify(inner_point_defn)).
% 23.03/23.08
% 23.03/23.08 cnf('1',plain,[inner_point(15 ^ [], 16 ^ []), end_point(15 ^ [], 16 ^ [])],start(22,bind([[_20167, _20220], [15 ^ [], 16 ^ []]]))).
% 23.03/23.08 cnf('1.1',plain,[-(inner_point(15 ^ [], 16 ^ []))],extension(2)).
% 23.03/23.08 cnf('1.2',plain,[-(end_point(15 ^ [], 16 ^ [])), incident_c(15 ^ [], 16 ^ []), -(incident_c(15 ^ [], 3 ^ [16 ^ [], 15 ^ []]))],extension(16,bind([[_19245, _19154], [16 ^ [], 15 ^ []]]))).
% 23.03/23.08 cnf('1.2.1',plain,[-(incident_c(15 ^ [], 16 ^ [])), incident_c(15 ^ [], 16 ^ []), 15 ^ [] = 15 ^ [], 16 ^ [] = 16 ^ []],extension(7,bind([[_14037, _14104, _14170, _14235], [15 ^ [], 15 ^ [], 16 ^ [], 16 ^ []]]))).
% 23.03/23.08 cnf('1.2.1.1',plain,[-(incident_c(15 ^ [], 16 ^ [])), incident_c(15 ^ [], 16 ^ []), 15 ^ [] = 15 ^ [], 16 ^ [] = 16 ^ []],extension(7,bind([[_14037, _14104, _14170, _14235], [15 ^ [], 15 ^ [], 16 ^ [], 16 ^ []]]))).
% 23.03/23.08 cnf('1.2.1.1.1',plain,[-(incident_c(15 ^ [], 16 ^ [])), incident_c(15 ^ [], 16 ^ []), 15 ^ [] = 15 ^ [], 16 ^ [] = 16 ^ []],extension(7,bind([[_14037, _14104, _14170, _14235], [15 ^ [], 15 ^ [], 16 ^ [], 16 ^ []]]))).
% 23.03/23.08 cnf('1.2.1.1.1.1',plain,[-(incident_c(15 ^ [], 16 ^ [])), incident_c(15 ^ [], 16 ^ []), 15 ^ [] = 15 ^ [], 16 ^ [] = 16 ^ []],extension(7,bind([[_14037, _14104, _14170, _14235], [15 ^ [], 15 ^ [], 16 ^ [], 16 ^ []]]))).
% 23.03/23.08 cnf('1.2.1.1.1.1.1',plain,[-(incident_c(15 ^ [], 16 ^ [])), inner_point(15 ^ [], 16 ^ [])],extension(21,bind([[_20167, _20220], [15 ^ [], 16 ^ []]]))).
% 23.03/23.08 cnf('1.2.1.1.1.1.1.1',plain,[-(inner_point(15 ^ [], 16 ^ []))],extension(2)).
% 23.03/23.08 cnf('1.2.1.1.1.1.2',plain,[-(15 ^ [] = 15 ^ [])],extension(5,bind([[_12176], [15 ^ []]]))).
% 23.03/23.08 cnf('1.2.1.1.1.1.3',plain,[-(16 ^ [] = 16 ^ [])],extension(5,bind([[_12176], [16 ^ []]]))).
% 23.03/23.08 cnf('1.2.1.1.1.2',plain,[-(15 ^ [] = 15 ^ [])],extension(5,bind([[_12176], [15 ^ []]]))).
% 23.03/23.08 cnf('1.2.1.1.1.3',plain,[-(16 ^ [] = 16 ^ [])],extension(5,bind([[_12176], [16 ^ []]]))).
% 23.03/23.08 cnf('1.2.1.1.2',plain,[-(15 ^ [] = 15 ^ [])],extension(5,bind([[_12176], [15 ^ []]]))).
% 23.03/23.08 cnf('1.2.1.1.3',plain,[-(16 ^ [] = 16 ^ [])],extension(5,bind([[_12176], [16 ^ []]]))).
% 23.03/23.08 cnf('1.2.1.2',plain,[-(15 ^ [] = 15 ^ [])],extension(5,bind([[_12176], [15 ^ []]]))).
% 23.03/23.08 cnf('1.2.1.3',plain,[-(16 ^ [] = 16 ^ [])],extension(5,bind([[_12176], [16 ^ []]]))).
% 23.03/23.08 cnf('1.2.2',plain,[incident_c(15 ^ [], 3 ^ [16 ^ [], 15 ^ []]), end_point(15 ^ [], 14 ^ []), -(part_of(4 ^ [16 ^ [], 15 ^ []], 3 ^ [16 ^ [], 15 ^ []])), -(part_of(3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []])), part_of(3 ^ [16 ^ [], 15 ^ []], 14 ^ []), part_of(4 ^ [16 ^ [], 15 ^ []], 14 ^ []), incident_c(15 ^ [], 4 ^ [16 ^ [], 15 ^ []])],extension(20,bind([[_19453, _19245, _19154, _19530], [3 ^ [16 ^ [], 15 ^ []], 14 ^ [], 15 ^ [], 4 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.1',plain,[-(end_point(15 ^ [], 14 ^ [])), end_point(15 ^ [], 14 ^ []), 15 ^ [] = 15 ^ [], 14 ^ [] = 14 ^ []],extension(6,bind([[_13413, _13480, _13546, _13611], [15 ^ [], 15 ^ [], 14 ^ [], 14 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.1.1',plain,[-(end_point(15 ^ [], 14 ^ [])), end_point(15 ^ [], 14 ^ []), 15 ^ [] = 15 ^ [], 14 ^ [] = 14 ^ []],extension(6,bind([[_13413, _13480, _13546, _13611], [15 ^ [], 15 ^ [], 14 ^ [], 14 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.1.1.1',plain,[-(end_point(15 ^ [], 14 ^ [])), -(inner_point(15 ^ [], 14 ^ [])), incident_c(15 ^ [], 14 ^ [])],extension(23,bind([[_20167, _20220], [15 ^ [], 14 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.1.1.1.1',plain,[inner_point(15 ^ [], 14 ^ [])],extension(3)).
% 23.03/23.08 cnf('1.2.2.1.1.1.2',plain,[-(incident_c(15 ^ [], 14 ^ [])), part_of(16 ^ [], 14 ^ []), incident_c(15 ^ [], 16 ^ [])],extension(11,bind([[_18008, _18178, _18064], [14 ^ [], 15 ^ [], 16 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.1.1.1.2.1',plain,[-(part_of(16 ^ [], 14 ^ []))],extension(1)).
% 23.03/23.08 cnf('1.2.2.1.1.1.2.2',plain,[-(incident_c(15 ^ [], 16 ^ []))],lemmata('1.2')).
% 23.03/23.08 cnf('1.2.2.1.1.2',plain,[-(15 ^ [] = 15 ^ [])],extension(5,bind([[_12176], [15 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.1.1.3',plain,[-(14 ^ [] = 14 ^ [])],extension(5,bind([[_12176], [14 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.1.2',plain,[-(15 ^ [] = 15 ^ [])],extension(5,bind([[_12176], [15 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.1.3',plain,[-(14 ^ [] = 14 ^ [])],extension(5,bind([[_12176], [14 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.2',plain,[part_of(4 ^ [16 ^ [], 15 ^ []], 3 ^ [16 ^ [], 15 ^ []]), -(end_point(15 ^ [], 16 ^ [])), incident_c(15 ^ [], 16 ^ [])],extension(19,bind([[_19154, _19245], [15 ^ [], 16 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.2.1',plain,[end_point(15 ^ [], 16 ^ [])],reduction('1')).
% 23.03/23.08 cnf('1.2.2.2.2',plain,[-(incident_c(15 ^ [], 16 ^ []))],lemmata('1.2')).
% 23.03/23.08 cnf('1.2.2.3',plain,[part_of(3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []]), -(part_of(3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []])), 3 ^ [16 ^ [], 15 ^ []] = 3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []] = 4 ^ [16 ^ [], 15 ^ []]],extension(8,bind([[_16629, _16696, _16762, _16827], [3 ^ [16 ^ [], 15 ^ []], 3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.3.1',plain,[part_of(3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []]), -(part_of(3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []])), 3 ^ [16 ^ [], 15 ^ []] = 3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []] = 4 ^ [16 ^ [], 15 ^ []]],extension(8,bind([[_16629, _16696, _16762, _16827], [3 ^ [16 ^ [], 15 ^ []], 3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.3.1.1',plain,[part_of(3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []]), -(part_of(3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []])), 3 ^ [16 ^ [], 15 ^ []] = 3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []] = 4 ^ [16 ^ [], 15 ^ []]],extension(8,bind([[_16629, _16696, _16762, _16827], [3 ^ [16 ^ [], 15 ^ []], 3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.3.1.1.1',plain,[part_of(3 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []]), -(end_point(15 ^ [], 16 ^ [])), incident_c(15 ^ [], 16 ^ [])],extension(18,bind([[_19154, _19245], [15 ^ [], 16 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.3.1.1.1.1',plain,[end_point(15 ^ [], 16 ^ [])],reduction('1')).
% 23.03/23.08 cnf('1.2.2.3.1.1.1.2',plain,[-(incident_c(15 ^ [], 16 ^ []))],lemmata('1.2')).
% 23.03/23.08 cnf('1.2.2.3.1.1.2',plain,[-(3 ^ [16 ^ [], 15 ^ []] = 3 ^ [16 ^ [], 15 ^ []])],extension(5,bind([[_12176], [3 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.3.1.1.3',plain,[-(4 ^ [16 ^ [], 15 ^ []] = 4 ^ [16 ^ [], 15 ^ []])],extension(5,bind([[_12176], [4 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.3.1.2',plain,[-(3 ^ [16 ^ [], 15 ^ []] = 3 ^ [16 ^ [], 15 ^ []])],extension(5,bind([[_12176], [3 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.3.1.3',plain,[-(4 ^ [16 ^ [], 15 ^ []] = 4 ^ [16 ^ [], 15 ^ []])],extension(5,bind([[_12176], [4 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.3.2',plain,[-(3 ^ [16 ^ [], 15 ^ []] = 3 ^ [16 ^ [], 15 ^ []])],extension(5,bind([[_12176], [3 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.3.3',plain,[-(4 ^ [16 ^ [], 15 ^ []] = 4 ^ [16 ^ [], 15 ^ []])],extension(5,bind([[_12176], [4 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.4',plain,[-(part_of(3 ^ [16 ^ [], 15 ^ []], 14 ^ [])), incident_c(1 ^ [3 ^ [16 ^ [], 15 ^ []], 14 ^ []], 14 ^ [])],extension(10,bind([[_18064, _18008], [3 ^ [16 ^ [], 15 ^ []], 14 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.4.1',plain,[-(incident_c(1 ^ [3 ^ [16 ^ [], 15 ^ []], 14 ^ []], 14 ^ [])), part_of(16 ^ [], 14 ^ []), incident_c(1 ^ [3 ^ [16 ^ [], 15 ^ []], 14 ^ []], 16 ^ [])],extension(11,bind([[_18008, _18178, _18064], [14 ^ [], 1 ^ [3 ^ [16 ^ [], 15 ^ []], 14 ^ []], 16 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.4.1.1',plain,[-(part_of(16 ^ [], 14 ^ []))],extension(1)).
% 23.03/23.08 cnf('1.2.2.4.1.2',plain,[-(incident_c(1 ^ [3 ^ [16 ^ [], 15 ^ []], 14 ^ []], 16 ^ [])), part_of(3 ^ [16 ^ [], 15 ^ []], 16 ^ []), incident_c(1 ^ [3 ^ [16 ^ [], 15 ^ []], 14 ^ []], 3 ^ [16 ^ [], 15 ^ []])],extension(11,bind([[_18008, _18178, _18064], [16 ^ [], 1 ^ [3 ^ [16 ^ [], 15 ^ []], 14 ^ []], 3 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.4.1.2.1',plain,[-(part_of(3 ^ [16 ^ [], 15 ^ []], 16 ^ [])), -(end_point(15 ^ [], 16 ^ [])), incident_c(15 ^ [], 16 ^ [])],extension(14,bind([[_19154, _19245], [15 ^ [], 16 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.4.1.2.1.1',plain,[end_point(15 ^ [], 16 ^ [])],reduction('1')).
% 23.03/23.08 cnf('1.2.2.4.1.2.1.2',plain,[-(incident_c(15 ^ [], 16 ^ []))],lemmata('1.2')).
% 23.03/23.08 cnf('1.2.2.4.1.2.2',plain,[-(incident_c(1 ^ [3 ^ [16 ^ [], 15 ^ []], 14 ^ []], 3 ^ [16 ^ [], 15 ^ []])), -(part_of(3 ^ [16 ^ [], 15 ^ []], 14 ^ []))],extension(9,bind([[_18064, _18008], [3 ^ [16 ^ [], 15 ^ []], 14 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.4.1.2.2.1',plain,[part_of(3 ^ [16 ^ [], 15 ^ []], 14 ^ [])],reduction('1.2.2')).
% 23.03/23.08 cnf('1.2.2.5',plain,[-(part_of(4 ^ [16 ^ [], 15 ^ []], 14 ^ [])), incident_c(1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 14 ^ [])],extension(10,bind([[_18064, _18008], [4 ^ [16 ^ [], 15 ^ []], 14 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.5.1',plain,[-(incident_c(1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 14 ^ [])), sum(14 ^ [], 4 ^ [16 ^ [], 15 ^ []]) = sum(14 ^ [], 4 ^ [16 ^ [], 15 ^ []]), incident_c(1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], sum(14 ^ [], 4 ^ [16 ^ [], 15 ^ []])), -(incident_c(1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 4 ^ [16 ^ [], 15 ^ []]))],extension(13,bind([[_18539, _18469, _18772, _18608], [14 ^ [], sum(14 ^ [], 4 ^ [16 ^ [], 15 ^ []]), 1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 4 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.5.1.1',plain,[-(sum(14 ^ [], 4 ^ [16 ^ [], 15 ^ []]) = sum(14 ^ [], 4 ^ [16 ^ [], 15 ^ []])), 14 ^ [] = 14 ^ [], 4 ^ [16 ^ [], 15 ^ []] = 4 ^ [16 ^ [], 15 ^ []]],extension(4,bind([[_17348, _17415, _17481, _17546], [14 ^ [], 14 ^ [], 4 ^ [16 ^ [], 15 ^ []], 4 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.5.1.1.1',plain,[-(14 ^ [] = 14 ^ [])],extension(5,bind([[_12176], [14 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.5.1.1.2',plain,[-(4 ^ [16 ^ [], 15 ^ []] = 4 ^ [16 ^ [], 15 ^ []])],extension(5,bind([[_12176], [4 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.5.1.2',plain,[-(incident_c(1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], sum(14 ^ [], 4 ^ [16 ^ [], 15 ^ []]))), sum(14 ^ [], 4 ^ [16 ^ [], 15 ^ []]) = sum(14 ^ [], 4 ^ [16 ^ [], 15 ^ []]), incident_c(1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 4 ^ [16 ^ [], 15 ^ []])],extension(12,bind([[_18469, _18539, _18772, _18608], [sum(14 ^ [], 4 ^ [16 ^ [], 15 ^ []]), 14 ^ [], 1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 4 ^ [16 ^ [], 15 ^ []]]]))).
% 23.03/23.08 cnf('1.2.2.5.1.2.1',plain,[-(sum(14 ^ [], 4 ^ [16 ^ [], 15 ^ []]) = sum(14 ^ [], 4 ^ [16 ^ [], 15 ^ []]))],extension(5,bind([[_12176], [sum(14 ^ [], 4 ^ [16 ^ [], 15 ^ []])]]))).
% 23.03/23.08 cnf('1.2.2.5.1.2.2',plain,[-(incident_c(1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 4 ^ [16 ^ [], 15 ^ []])), -(part_of(4 ^ [16 ^ [], 15 ^ []], 14 ^ []))],extension(9,bind([[_18064, _18008], [4 ^ [16 ^ [], 15 ^ []], 14 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.5.1.2.2.1',plain,[part_of(4 ^ [16 ^ [], 15 ^ []], 14 ^ [])],reduction('1.2.2')).
% 23.03/23.08 cnf('1.2.2.5.1.3',plain,[incident_c(1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 4 ^ [16 ^ [], 15 ^ []]), part_of(4 ^ [16 ^ [], 15 ^ []], 16 ^ []), -(incident_c(1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 16 ^ []))],extension(11,bind([[_18064, _18178, _18008], [4 ^ [16 ^ [], 15 ^ []], 1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 16 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.5.1.3.1',plain,[-(part_of(4 ^ [16 ^ [], 15 ^ []], 16 ^ [])), -(end_point(15 ^ [], 16 ^ [])), incident_c(15 ^ [], 16 ^ [])],extension(15,bind([[_19154, _19245], [15 ^ [], 16 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.5.1.3.1.1',plain,[end_point(15 ^ [], 16 ^ [])],reduction('1')).
% 23.03/23.08 cnf('1.2.2.5.1.3.1.2',plain,[-(incident_c(15 ^ [], 16 ^ []))],lemmata('1.2')).
% 23.03/23.08 cnf('1.2.2.5.1.3.2',plain,[incident_c(1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 16 ^ []), part_of(16 ^ [], 14 ^ []), -(incident_c(1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 14 ^ []))],extension(11,bind([[_18064, _18178, _18008], [16 ^ [], 1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 14 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.5.1.3.2.1',plain,[-(part_of(16 ^ [], 14 ^ []))],extension(1)).
% 23.03/23.08 cnf('1.2.2.5.1.3.2.2',plain,[incident_c(1 ^ [4 ^ [16 ^ [], 15 ^ []], 14 ^ []], 14 ^ [])],reduction('1.2.2.5')).
% 23.03/23.08 cnf('1.2.2.6',plain,[-(incident_c(15 ^ [], 4 ^ [16 ^ [], 15 ^ []])), -(end_point(15 ^ [], 16 ^ [])), incident_c(15 ^ [], 16 ^ [])],extension(17,bind([[_19154, _19245], [15 ^ [], 16 ^ []]]))).
% 23.03/23.08 cnf('1.2.2.6.1',plain,[end_point(15 ^ [], 16 ^ [])],reduction('1')).
% 23.03/23.08 cnf('1.2.2.6.2',plain,[-(incident_c(15 ^ [], 16 ^ []))],lemmata('1.2')).
% 23.03/23.08 %-----------------------------------------------------
% 23.03/23.09
% 23.03/23.09 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------