%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO631+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n023.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:05:42 EDT 2022
% Result : Theorem 194.71s 187.77s
% Output : Proof 194.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO631+1 : TPTP v8.1.0. Released v7.5.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n023.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 16:49:49 EDT 2022
% 0.12/0.33 % CPUTime :
% 194.71/187.77 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 194.71/187.77 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 194.71/187.78
% 194.71/187.78 %-----------------------------------------------------
% 194.71/187.78 fof(ruleD3, axiom, ! [_269279, _269282, _269285, _269288] : (coll(_269279, _269282, _269285) & coll(_269279, _269282, _269288) => coll(_269285, _269288, _269279)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD3)).
% 194.71/187.78 fof(ruleD1, axiom, ! [_269508, _269511, _269514] : (coll(_269508, _269511, _269514) => coll(_269508, _269514, _269511)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD1)).
% 194.71/187.78 fof(ruleD8, axiom, ! [_269681, _269684, _269687, _269690] : (perp(_269681, _269684, _269687, _269690) => perp(_269687, _269690, _269681, _269684)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD8)).
% 194.71/187.78 fof(ruleD17, axiom, ! [_269885, _269888, _269891, _269894, _269897] : (cyclic(_269885, _269888, _269891, _269894) & cyclic(_269885, _269888, _269891, _269897) => cyclic(_269888, _269891, _269894, _269897)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD17)).
% 194.71/187.78 fof(ruleD9, axiom, ! [_270140, _270143, _270146, _270149, _270152, _270155] : (perp(_270140, _270143, _270146, _270149) & perp(_270146, _270149, _270152, _270155) => para(_270140, _270143, _270152, _270155)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD9)).
% 194.71/187.78 fof(ruleD21, axiom, ! [_270407, _270410, _270413, _270416, _270419, _270422, _270425, _270428] : (eqangle(_270407, _270410, _270413, _270416, _270419, _270422, _270425, _270428) => eqangle(_270407, _270410, _270419, _270422, _270413, _270416, _270425, _270428)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD21)).
% 194.71/187.78 fof(ruleD2, axiom, ! [_270722, _270725, _270728] : (coll(_270722, _270725, _270728) => coll(_270725, _270722, _270728)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD2)).
% 194.71/187.78 fof(ruleD42a, axiom, ! [_270895, _270898, _270901, _270904] : (eqangle(_270901, _270895, _270901, _270898, _270904, _270895, _270904, _270898) & ~ coll(_270901, _270904, _270895) => cyclic(_270895, _270898, _270901, _270904)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD42a)).
% 194.71/187.78 fof(ruleD40, axiom, ! [_271161, _271164, _271167, _271170, _271173, _271176] : (para(_271161, _271164, _271167, _271170) => eqangle(_271161, _271164, _271173, _271176, _271167, _271170, _271173, _271176)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD40)).
% 194.71/187.78 fof(exemplo6GDDFULL8110994, conjecture, ! [_271412, _271415, _271418, _271421, _271424, _271427, _271430, _271433, _271436, _271439, _271442, _271445, _271448] : (circle(_271421, _271412, _271415, _271418) & circle(_271421, _271412, _271424, _271445) & circle(_271421, _271412, _271427, _271448) & perp(_271430, _271427, _271412, _271424) & coll(_271430, _271412, _271424) & perp(_271433, _271427, _271412, _271415) & coll(_271433, _271412, _271415) & perp(_271436, _271427, _271415, _271418) & coll(_271436, _271415, _271418) & perp(_271439, _271427, _271418, _271424) & coll(_271439, _271418, _271424) & coll(_271442, _271430, _271433) & coll(_271442, _271436, _271439) => cyclic(_271427, _271433, _271442, _271436)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL8110994)).
% 194.71/187.78 fof(ruleD7, axiom, ! [_272175, _272178, _272181, _272184] : (perp(_272175, _272178, _272181, _272184) => perp(_272175, _272178, _272184, _272181)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 194.71/187.78 fof(ruleD42b, axiom, ! [_272391, _272394, _272397, _272400] : (eqangle(_272397, _272391, _272397, _272394, _272400, _272391, _272400, _272394) & coll(_272397, _272400, _272394) => cyclic(_272391, _272394, _272397, _272400)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD42b)).
% 194.71/187.78
% 194.71/187.78 cnf(1, plain, [-(coll(_86129, _86191, _86002)), coll(_86002, _86066, _86129), coll(_86002, _86066, _86191)], clausify(ruleD3)).
% 194.71/187.78 cnf(2, plain, [coll(_85080, _85132, _85183), -(coll(_85080, _85183, _85132))], clausify(ruleD1)).
% 194.71/187.78 cnf(3, plain, [perp(_89566, _89625, _89683, _89740), -(perp(_89683, _89740, _89566, _89625))], clausify(ruleD8)).
% 194.71/187.78 cnf(4, plain, [-(cyclic(_96530, _96601, _96671, _96740)), cyclic(_96458, _96530, _96601, _96671), cyclic(_96458, _96530, _96601, _96740)], clausify(ruleD17)).
% 194.71/187.78 cnf(5, plain, [-(para(_90191, _90268, _90493, _90566)), perp(_90191, _90268, _90344, _90419), perp(_90344, _90419, _90493, _90566)], clausify(ruleD9)).
% 194.71/187.78 cnf(6, plain, [eqangle(_101597, _101684, _101770, _101855, _101939, _102022, _102104, _102185), -(eqangle(_101597, _101684, _101939, _102022, _101770, _101855, _102104, _102185))], clausify(ruleD21)).
% 194.71/187.78 cnf(7, plain, [coll(_85541, _85593, _85644), -(coll(_85593, _85541, _85644))], clausify(ruleD2)).
% 194.71/187.78 cnf(8, plain, [-(cyclic(_127883, _127955, _128026, _128096)), eqangle(_128026, _127883, _128026, _127955, _128096, _127883, _128096, _127955), -(coll(_128026, _128096, _127883))], clausify(ruleD42a)).
% 194.71/187.78 cnf(9, plain, [para(_126090, _126163, _126235, _126306), -(eqangle(_126090, _126163, _126376, _126445, _126235, _126306, _126376, _126445))], clausify(ruleD40)).
% 194.71/187.78 cnf(10, plain, [-(coll(31 ^ [], 27 ^ [], 28 ^ []))], clausify(exemplo6GDDFULL8110994)).
% 194.71/187.78 cnf(11, plain, [perp(_88941, _89000, _89058, _89115), -(perp(_88941, _89000, _89115, _89058))], clausify(ruleD7)).
% 194.71/187.78 cnf(12, plain, [-(coll(_63591, _63758, _63921)), coll(_63506, _63675, _63840), _63506 = _63591, _63675 = _63758, _63840 = _63921], theory(equality)).
% 194.71/187.78 cnf(13, plain, [-(cyclic(_128850, _128920, _128989, _129057)), eqangle(_128989, _128850, _128989, _128920, _129057, _128850, _129057, _128920), coll(_128989, _129057, _128920)], clausify(ruleD42b)).
% 194.71/187.78 cnf(14, plain, [cyclic(26 ^ [], 28 ^ [], 31 ^ [], 29 ^ [])], clausify(exemplo6GDDFULL8110994)).
% 194.71/187.78 cnf(15, plain, [-(_61104 = _61104)], theory(equality)).
% 194.71/187.78 cnf(16, plain, [-(perp(28 ^ [], 26 ^ [], 21 ^ [], 22 ^ []))], clausify(exemplo6GDDFULL8110994)).
% 194.71/187.78
% 194.71/187.78 cnf('1',plain,[cyclic(26 ^ [], 28 ^ [], 31 ^ [], 29 ^ [])],start(14)).
% 194.71/187.78 cnf('1.1',plain,[-(cyclic(26 ^ [], 28 ^ [], 31 ^ [], 29 ^ [])), cyclic(26 ^ [], 26 ^ [], 28 ^ [], 31 ^ []), cyclic(26 ^ [], 26 ^ [], 28 ^ [], 29 ^ [])],extension(4,bind([[_96671, _96458, _96530, _96601, _96740], [31 ^ [], 26 ^ [], 26 ^ [], 28 ^ [], 29 ^ []]]))).
% 194.71/187.78 cnf('1.1.1',plain,[-(cyclic(26 ^ [], 26 ^ [], 28 ^ [], 31 ^ [])), eqangle(28 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 31 ^ [], 26 ^ [], 31 ^ [], 26 ^ []), -(coll(28 ^ [], 31 ^ [], 26 ^ []))],extension(8,bind([[_127955, _128026, _128096, _127883], [26 ^ [], 28 ^ [], 31 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.1',plain,[-(eqangle(28 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 31 ^ [], 26 ^ [], 31 ^ [], 26 ^ [])), eqangle(28 ^ [], 26 ^ [], 31 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 31 ^ [], 26 ^ [])],extension(6,bind([[_101597, _101684, _101770, _101855, _101939, _102022, _102104, _102185], [28 ^ [], 26 ^ [], 31 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 31 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.1.1',plain,[-(eqangle(28 ^ [], 26 ^ [], 31 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 31 ^ [], 26 ^ [])), para(28 ^ [], 26 ^ [], 28 ^ [], 26 ^ [])],extension(9,bind([[_126376, _126445, _126090, _126163, _126235, _126306], [31 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 28 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.1.1.1',plain,[-(para(28 ^ [], 26 ^ [], 28 ^ [], 26 ^ [])), perp(28 ^ [], 26 ^ [], 22 ^ [], 21 ^ []), perp(22 ^ [], 21 ^ [], 28 ^ [], 26 ^ [])],extension(5,bind([[_90191, _90268, _90344, _90419, _90493, _90566], [28 ^ [], 26 ^ [], 22 ^ [], 21 ^ [], 28 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.1.1.1.1',plain,[-(perp(28 ^ [], 26 ^ [], 22 ^ [], 21 ^ [])), perp(28 ^ [], 26 ^ [], 21 ^ [], 22 ^ [])],extension(11,bind([[_88941, _89000, _89058, _89115], [28 ^ [], 26 ^ [], 21 ^ [], 22 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.1.1.1.1.1',plain,[-(perp(28 ^ [], 26 ^ [], 21 ^ [], 22 ^ []))],extension(16)).
% 194.71/187.78 cnf('1.1.1.1.1.1.2',plain,[-(perp(22 ^ [], 21 ^ [], 28 ^ [], 26 ^ [])), perp(28 ^ [], 26 ^ [], 22 ^ [], 21 ^ [])],extension(3,bind([[_89566, _89625, _89683, _89740], [28 ^ [], 26 ^ [], 22 ^ [], 21 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.1.1.1.2.1',plain,[-(perp(28 ^ [], 26 ^ [], 22 ^ [], 21 ^ []))],lemmata('1.1.1.1.1.1')).
% 194.71/187.78 cnf('1.1.1.2',plain,[coll(28 ^ [], 31 ^ [], 26 ^ []), -(coll(26 ^ [], 27 ^ [], 28 ^ [])), coll(28 ^ [], 31 ^ [], 27 ^ [])],extension(1,bind([[_86129, _86002, _86066, _86191], [26 ^ [], 28 ^ [], 31 ^ [], 27 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.2.1',plain,[coll(26 ^ [], 27 ^ [], 28 ^ []), -(coll(28 ^ [], 31 ^ [], 26 ^ [])), coll(26 ^ [], 27 ^ [], 31 ^ [])],extension(1,bind([[_86129, _86002, _86066, _86191], [28 ^ [], 26 ^ [], 27 ^ [], 31 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.2.1.1',plain,[coll(28 ^ [], 31 ^ [], 26 ^ []), -(coll(28 ^ [], 31 ^ [], 26 ^ [])), 28 ^ [] = 28 ^ [], 31 ^ [] = 31 ^ [], 26 ^ [] = 26 ^ []],extension(12,bind([[_63506, _63591, _63675, _63758, _63840, _63921], [28 ^ [], 28 ^ [], 31 ^ [], 31 ^ [], 26 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.2.1.1.1',plain,[coll(28 ^ [], 31 ^ [], 26 ^ []), -(cyclic(26 ^ [], 26 ^ [], 28 ^ [], 31 ^ [])), eqangle(28 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 31 ^ [], 26 ^ [], 31 ^ [], 26 ^ [])],extension(13,bind([[_128989, _128850, _129057, _128920], [28 ^ [], 26 ^ [], 31 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.2.1.1.1.1',plain,[cyclic(26 ^ [], 26 ^ [], 28 ^ [], 31 ^ [])],reduction('1.1')).
% 194.71/187.78 cnf('1.1.1.2.1.1.1.2',plain,[-(eqangle(28 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 31 ^ [], 26 ^ [], 31 ^ [], 26 ^ []))],lemmata('1.1.1')).
% 194.71/187.78 cnf('1.1.1.2.1.1.2',plain,[-(28 ^ [] = 28 ^ [])],extension(15,bind([[_61104], [28 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.2.1.1.3',plain,[-(31 ^ [] = 31 ^ [])],extension(15,bind([[_61104], [31 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.2.1.1.4',plain,[-(26 ^ [] = 26 ^ [])],extension(15,bind([[_61104], [26 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.2.1.2',plain,[-(coll(26 ^ [], 27 ^ [], 31 ^ [])), coll(31 ^ [], 28 ^ [], 26 ^ []), coll(31 ^ [], 28 ^ [], 27 ^ [])],extension(1,bind([[_86129, _86002, _86066, _86191], [26 ^ [], 31 ^ [], 28 ^ [], 27 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.2.1.2.1',plain,[-(coll(31 ^ [], 28 ^ [], 26 ^ [])), coll(28 ^ [], 31 ^ [], 26 ^ [])],extension(7,bind([[_85541, _85593, _85644], [28 ^ [], 31 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.2.1.2.1.1',plain,[-(coll(28 ^ [], 31 ^ [], 26 ^ []))],reduction('1.1.1')).
% 194.71/187.78 cnf('1.1.1.2.1.2.2',plain,[-(coll(31 ^ [], 28 ^ [], 27 ^ [])), coll(31 ^ [], 27 ^ [], 28 ^ [])],extension(2,bind([[_85080, _85132, _85183], [31 ^ [], 27 ^ [], 28 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.2.1.2.2.1',plain,[-(coll(31 ^ [], 27 ^ [], 28 ^ []))],extension(10)).
% 194.71/187.78 cnf('1.1.1.2.2',plain,[-(coll(28 ^ [], 31 ^ [], 27 ^ [])), coll(31 ^ [], 28 ^ [], 27 ^ [])],extension(7,bind([[_85541, _85593, _85644], [31 ^ [], 28 ^ [], 27 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.2.2.1',plain,[-(coll(31 ^ [], 28 ^ [], 27 ^ [])), coll(31 ^ [], 27 ^ [], 28 ^ [])],extension(2,bind([[_85080, _85132, _85183], [31 ^ [], 27 ^ [], 28 ^ []]]))).
% 194.71/187.78 cnf('1.1.1.2.2.1.1',plain,[-(coll(31 ^ [], 27 ^ [], 28 ^ []))],extension(10)).
% 194.71/187.78 cnf('1.1.2',plain,[-(cyclic(26 ^ [], 26 ^ [], 28 ^ [], 29 ^ [])), eqangle(28 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 29 ^ [], 26 ^ [], 29 ^ [], 26 ^ []), -(coll(28 ^ [], 29 ^ [], 26 ^ []))],extension(8,bind([[_127955, _128026, _128096, _127883], [26 ^ [], 28 ^ [], 29 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.1',plain,[-(eqangle(28 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 29 ^ [], 26 ^ [], 29 ^ [], 26 ^ [])), eqangle(28 ^ [], 26 ^ [], 29 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 29 ^ [], 26 ^ [])],extension(6,bind([[_101597, _101684, _101770, _101855, _101939, _102022, _102104, _102185], [28 ^ [], 26 ^ [], 29 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 29 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.1.1',plain,[-(eqangle(28 ^ [], 26 ^ [], 29 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 29 ^ [], 26 ^ [])), para(28 ^ [], 26 ^ [], 28 ^ [], 26 ^ [])],extension(9,bind([[_126376, _126445, _126090, _126163, _126235, _126306], [29 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 28 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.1.1.1',plain,[-(para(28 ^ [], 26 ^ [], 28 ^ [], 26 ^ [])), perp(28 ^ [], 26 ^ [], 22 ^ [], 21 ^ []), perp(22 ^ [], 21 ^ [], 28 ^ [], 26 ^ [])],extension(5,bind([[_90191, _90268, _90344, _90419, _90493, _90566], [28 ^ [], 26 ^ [], 22 ^ [], 21 ^ [], 28 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.1.1.1.1',plain,[-(perp(28 ^ [], 26 ^ [], 22 ^ [], 21 ^ [])), perp(28 ^ [], 26 ^ [], 21 ^ [], 22 ^ [])],extension(11,bind([[_88941, _89000, _89058, _89115], [28 ^ [], 26 ^ [], 21 ^ [], 22 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.1.1.1.1.1',plain,[-(perp(28 ^ [], 26 ^ [], 21 ^ [], 22 ^ []))],extension(16)).
% 194.71/187.78 cnf('1.1.2.1.1.1.2',plain,[-(perp(22 ^ [], 21 ^ [], 28 ^ [], 26 ^ [])), perp(28 ^ [], 26 ^ [], 22 ^ [], 21 ^ [])],extension(3,bind([[_89566, _89625, _89683, _89740], [28 ^ [], 26 ^ [], 22 ^ [], 21 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.1.1.1.2.1',plain,[-(perp(28 ^ [], 26 ^ [], 22 ^ [], 21 ^ []))],lemmata('1.1.2.1.1.1')).
% 194.71/187.78 cnf('1.1.2.2',plain,[coll(28 ^ [], 29 ^ [], 26 ^ []), -(coll(26 ^ [], 26 ^ [], 28 ^ [])), coll(28 ^ [], 29 ^ [], 26 ^ [])],extension(1,bind([[_86129, _86002, _86066, _86191], [26 ^ [], 28 ^ [], 29 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.2.1',plain,[coll(26 ^ [], 26 ^ [], 28 ^ []), -(coll(28 ^ [], 29 ^ [], 26 ^ [])), coll(26 ^ [], 26 ^ [], 29 ^ [])],extension(1,bind([[_86129, _86002, _86066, _86191], [28 ^ [], 26 ^ [], 26 ^ [], 29 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.2.1.1',plain,[coll(28 ^ [], 29 ^ [], 26 ^ []), -(coll(28 ^ [], 29 ^ [], 26 ^ [])), 28 ^ [] = 28 ^ [], 29 ^ [] = 29 ^ [], 26 ^ [] = 26 ^ []],extension(12,bind([[_63506, _63591, _63675, _63758, _63840, _63921], [28 ^ [], 28 ^ [], 29 ^ [], 29 ^ [], 26 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.2.1.1.1',plain,[coll(28 ^ [], 29 ^ [], 26 ^ []), -(cyclic(26 ^ [], 26 ^ [], 28 ^ [], 29 ^ [])), eqangle(28 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 29 ^ [], 26 ^ [], 29 ^ [], 26 ^ [])],extension(13,bind([[_128989, _128850, _129057, _128920], [28 ^ [], 26 ^ [], 29 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.2.1.1.1.1',plain,[cyclic(26 ^ [], 26 ^ [], 28 ^ [], 29 ^ [])],reduction('1.1')).
% 194.71/187.78 cnf('1.1.2.2.1.1.1.2',plain,[-(eqangle(28 ^ [], 26 ^ [], 28 ^ [], 26 ^ [], 29 ^ [], 26 ^ [], 29 ^ [], 26 ^ []))],lemmata('1.1.2')).
% 194.71/187.78 cnf('1.1.2.2.1.1.2',plain,[-(28 ^ [] = 28 ^ [])],extension(15,bind([[_61104], [28 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.2.1.1.3',plain,[-(29 ^ [] = 29 ^ [])],extension(15,bind([[_61104], [29 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.2.1.1.4',plain,[-(26 ^ [] = 26 ^ [])],extension(15,bind([[_61104], [26 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.2.1.2',plain,[-(coll(26 ^ [], 26 ^ [], 29 ^ [])), coll(29 ^ [], 28 ^ [], 26 ^ []), coll(29 ^ [], 28 ^ [], 26 ^ [])],extension(1,bind([[_86129, _86002, _86066, _86191], [26 ^ [], 29 ^ [], 28 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.2.1.2.1',plain,[-(coll(29 ^ [], 28 ^ [], 26 ^ [])), coll(28 ^ [], 29 ^ [], 26 ^ [])],extension(7,bind([[_85541, _85593, _85644], [28 ^ [], 29 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.2.1.2.1.1',plain,[-(coll(28 ^ [], 29 ^ [], 26 ^ []))],reduction('1.1.2')).
% 194.71/187.78 cnf('1.1.2.2.1.2.2',plain,[-(coll(29 ^ [], 28 ^ [], 26 ^ [])), coll(28 ^ [], 29 ^ [], 26 ^ [])],extension(7,bind([[_85541, _85593, _85644], [28 ^ [], 29 ^ [], 26 ^ []]]))).
% 194.71/187.78 cnf('1.1.2.2.1.2.2.1',plain,[-(coll(28 ^ [], 29 ^ [], 26 ^ []))],reduction('1.1.2')).
% 194.71/187.78 cnf('1.1.2.2.2',plain,[-(coll(28 ^ [], 29 ^ [], 26 ^ []))],reduction('1.1.2')).
% 194.71/187.78 %-----------------------------------------------------
% 194.71/187.78
% 194.71/187.78 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------