%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO223+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n021.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:03:55 EDT 2022
% Result : Theorem 30.74s 30.30s
% Output : Proof 30.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.10 % Problem : GEO223+3 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.11 % Command : leancop_casc.sh %s %d
% 0.10/0.31 % Computer : n021.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 600
% 0.10/0.31 % DateTime : Sat Jun 18 18:28:32 EDT 2022
% 0.10/0.31 % CPUTime :
% 30.74/30.30 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 30.74/30.30 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 30.74/30.31
% 30.74/30.31 %-----------------------------------------------------
% 30.74/30.31 fof(cotno1, axiom, ! [_69516, _69519, _69522] : ((~ convergent_lines(_69516, _69519) | ~ unorthogonal_lines(_69516, _69519)) & (~ convergent_lines(_69516, _69522) | ~ unorthogonal_lines(_69516, _69522)) => ~ convergent_lines(_69519, _69522) | ~ unorthogonal_lines(_69519, _69522)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+4.ax', cotno1)).
% 30.74/30.31 fof(oac1, axiom, ! [_69850, _69853, _69856] : (convergent_lines(_69850, _69853) & unorthogonal_lines(_69850, _69853) => convergent_lines(_69850, _69856) & unorthogonal_lines(_69850, _69856) | convergent_lines(_69853, _69856) & unorthogonal_lines(_69853, _69856)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+3.ax', oac1)).
% 30.74/30.31 fof(con, conjecture, ! [_70155, _70158] : equal_lines(parallel_through_point(_70158, _70155), orthogonal_through_point(orthogonal_through_point(_70158, _70155), _70155)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 30.74/30.31 fof(apart2, axiom, ! [_70322] : ~ distinct_lines(_70322, _70322), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', apart2)).
% 30.74/30.31 fof(apart3, axiom, ! [_70436] : ~ convergent_lines(_70436, _70436), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', apart3)).
% 30.74/30.31 fof(apart5, axiom, ! [_70551, _70554, _70557] : (distinct_lines(_70551, _70554) => distinct_lines(_70551, _70557) | distinct_lines(_70554, _70557)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', apart5)).
% 30.74/30.31 fof(ax6, axiom, ! [_70736, _70739, _70742] : (convergent_lines(_70736, _70739) => convergent_lines(_70736, _70742) | convergent_lines(_70739, _70742)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ax6)).
% 30.74/30.31 fof(ci3, axiom, ! [_70923, _70926] : (convergent_lines(_70923, _70926) => ~ apart_point_and_line(intersection_point(_70923, _70926), _70923)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ci3)).
% 30.74/30.31 fof(ci4, axiom, ! [_71092, _71095] : (convergent_lines(_71092, _71095) => ~ apart_point_and_line(intersection_point(_71092, _71095), _71095)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ci4)).
% 30.74/30.31 fof(p1, axiom, ! [_71265, _71268] : (distinct_lines(_71265, _71268) => convergent_lines(_71265, _71268)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+1.ax', p1)).
% 30.74/30.31 fof(cp1, axiom, ! [_71411, _71414] : ~ convergent_lines(parallel_through_point(_71414, _71411), _71414), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+2.ax', cp1)).
% 30.74/30.31 fof(occu1, axiom, ! [_71554, _71557] : (convergent_lines(_71554, _71557) | unorthogonal_lines(_71554, _71557)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+3.ax', occu1)).
% 30.74/30.31 fof(ooc1, axiom, ! [_71712, _71715] : ~ unorthogonal_lines(orthogonal_through_point(_71715, _71712), _71715), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+3.ax', ooc1)).
% 30.74/30.31 fof(ouo1, axiom, ! [_71854, _71857, _71860, _71863] : (distinct_lines(_71857, _71860) => apart_point_and_line(_71854, _71857) | apart_point_and_line(_71854, _71860) | unorthogonal_lines(_71857, _71863) | unorthogonal_lines(_71860, _71863)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+3.ax', ouo1)).
% 30.74/30.31 fof(ax2, axiom, ! [_72126, _72129] : (equal_lines(_72126, _72129) <=> ~ distinct_lines(_72126, _72129)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+6.ax', ax2)).
% 30.74/30.31
% 30.74/30.31 cnf(1, plain, [-(4 ^ [_22512, _22427, _22341]), -(unorthogonal_lines(_22341, _22512))], clausify(cotno1)).
% 30.74/30.31 cnf(2, plain, [-(4 ^ [_22512, _22427, _22341]), -(convergent_lines(_22341, _22512))], clausify(cotno1)).
% 30.74/30.31 cnf(3, plain, [-(3 ^ [_22512, _22427, _22341]), -(convergent_lines(_22341, _22427))], clausify(cotno1)).
% 30.74/30.31 cnf(4, plain, [-(2 ^ [_19998, _19925, _19851]), -(unorthogonal_lines(_19925, _19998))], clausify(oac1)).
% 30.74/30.31 cnf(5, plain, [-(2 ^ [_19998, _19925, _19851]), -(convergent_lines(_19925, _19998))], clausify(oac1)).
% 30.74/30.31 cnf(6, plain, [-(1 ^ [_19998, _19925, _19851]), -(unorthogonal_lines(_19851, _19998))], clausify(oac1)).
% 30.74/30.31 cnf(7, plain, [-(1 ^ [_19998, _19925, _19851]), -(convergent_lines(_19851, _19998))], clausify(oac1)).
% 30.74/30.31 cnf(8, plain, [equal_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))], clausify(con)).
% 30.74/30.31 cnf(9, plain, [distinct_lines(_12354, _12354)], clausify(apart2)).
% 30.74/30.31 cnf(10, plain, [convergent_lines(_12546, _12546)], clausify(apart3)).
% 30.74/30.31 cnf(11, plain, [distinct_lines(_13205, _13261), -(distinct_lines(_13205, _13316)), -(distinct_lines(_13261, _13316))], clausify(apart5)).
% 30.74/30.31 cnf(12, plain, [convergent_lines(_13672, _13728), -(convergent_lines(_13672, _13783)), -(convergent_lines(_13728, _13783))], clausify(ax6)).
% 30.74/30.31 cnf(13, plain, [convergent_lines(_14885, _14935), apart_point_and_line(intersection_point(_14885, _14935), _14885)], clausify(ci3)).
% 30.74/30.31 cnf(14, plain, [convergent_lines(_15258, _15308), apart_point_and_line(intersection_point(_15258, _15308), _15308)], clausify(ci4)).
% 30.74/30.31 cnf(15, plain, [distinct_lines(_18058, _18103), -(convergent_lines(_18058, _18103))], clausify(p1)).
% 30.74/30.31 cnf(16, plain, [convergent_lines(parallel_through_point(_18422, _18378), _18422)], clausify(cp1)).
% 30.74/30.31 cnf(17, plain, [-(convergent_lines(_19541, _19586)), -(unorthogonal_lines(_19541, _19586))], clausify(occu1)).
% 30.74/30.31 cnf(18, plain, [unorthogonal_lines(_19851, _19925), convergent_lines(_19851, _19925), 1 ^ [_19998, _19925, _19851], 2 ^ [_19998, _19925, _19851]], clausify(oac1)).
% 30.74/30.31 cnf(19, plain, [unorthogonal_lines(orthogonal_through_point(_20638, _20594), _20638)], clausify(ooc1)).
% 30.74/30.31 cnf(20, plain, [distinct_lines(_21231, _21303), -(apart_point_and_line(_21158, _21231)), -(apart_point_and_line(_21158, _21303)), -(unorthogonal_lines(_21231, _21374)), -(unorthogonal_lines(_21303, _21374))], clausify(ouo1)).
% 30.74/30.31 cnf(21, plain, [4 ^ [_22512, _22427, _22341], 3 ^ [_22512, _22427, _22341], convergent_lines(_22427, _22512), unorthogonal_lines(_22427, _22512)], clausify(cotno1)).
% 30.74/30.31 cnf(22, plain, [-(equal_lines(_25796, _25843)), -(distinct_lines(_25796, _25843))], clausify(ax2)).
% 30.74/30.31
% 30.74/30.31 cnf('1',plain,[equal_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))],start(8)).
% 30.74/30.31 cnf('1.1',plain,[-(equal_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))), -(distinct_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])))],extension(22,bind([[_25796, _25843], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1',plain,[distinct_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])), -(distinct_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), -(distinct_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(11,bind([[_13205, _13261, _13316], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.1',plain,[distinct_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],extension(9,bind([[_12354], [parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2',plain,[distinct_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), -(apart_point_and_line(intersection_point(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))), -(apart_point_and_line(intersection_point(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), parallel_through_point(6 ^ [], 5 ^ []))), -(unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []))), -(unorthogonal_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])))],extension(20,bind([[_21158, _21231, _21303, _21374], [intersection_point(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1',plain,[apart_point_and_line(intersection_point(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])), convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],extension(13,bind([[_14885, _14935], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1',plain,[-(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), -(3 ^ [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])])],extension(3,bind([[_22512, _22427, _22341], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1',plain,[3 ^ [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])], 4 ^ [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])], convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])), unorthogonal_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))],extension(21,bind([[_22341, _22427, _22512], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.1',plain,[-(4 ^ [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]), -(unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])))],extension(1,bind([[_22427, _22341, _22512], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.1.1',plain,[unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])), convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])), 1 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])], 2 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]],extension(18,bind([[_19998, _19925, _19851], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.1.1.1',plain,[-(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))), -(4 ^ [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])])],extension(2,bind([[_22512, _22427, _22341], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.1.1.1.1',plain,[4 ^ [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]],reduction('1.1.1.2.1.1.1')).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.1.1.2',plain,[-(1 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]), -(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(7,bind([[_19925, _19851, _19998], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.1.1.2.1',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],reduction('1.1.1.2.1')).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.1.1.3',plain,[-(2 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]), -(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(5,bind([[_19851, _19925, _19998], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.1.1.3.1',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],reduction('1.1.1.2.1')).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.2',plain,[-(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))), convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), -(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])))],extension(12,bind([[_13728, _13672, _13783], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.2.1',plain,[-(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(12,bind([[_13672, _13728, _13783], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.2.1.1',plain,[-(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), distinct_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],extension(15,bind([[_18058, _18103], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.2.1.1.1',plain,[-(distinct_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],reduction('1.1.1')).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.2.1.2',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],extension(10,bind([[_12546], [parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.2.2',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))],extension(10,bind([[_12546], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.3',plain,[-(unorthogonal_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])))],extension(17,bind([[_19541, _19586], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.3.1',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), -(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(12,bind([[_13672, _13728, _13783], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.3.1.1',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],extension(10,bind([[_12546], [parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.1.1.1.3.1.2',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],reduction('1.1.1.2.1')).
% 30.74/30.31 cnf('1.1.1.2.2',plain,[apart_point_and_line(intersection_point(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), parallel_through_point(6 ^ [], 5 ^ [])), convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],extension(14,bind([[_15258, _15308], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1',plain,[-(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), -(3 ^ [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])])],extension(3,bind([[_22512, _22427, _22341], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1.1',plain,[3 ^ [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])], 4 ^ [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])], convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])), unorthogonal_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))],extension(21,bind([[_22341, _22427, _22512], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.1',plain,[-(4 ^ [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]), -(unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])))],extension(1,bind([[_22427, _22341, _22512], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.1.1',plain,[unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])), convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])), 1 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])], 2 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]],extension(18,bind([[_19998, _19925, _19851], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.1.1.1',plain,[-(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))), -(4 ^ [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])])],extension(2,bind([[_22512, _22427, _22341], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.1.1.1.1',plain,[4 ^ [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]],reduction('1.1.1.2.2.1.1')).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.1.1.2',plain,[-(1 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]), -(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(7,bind([[_19925, _19851, _19998], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.1.1.2.1',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],reduction('1.1.1.2.2')).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.1.1.3',plain,[-(2 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]), -(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(5,bind([[_19851, _19925, _19998], [orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.1.1.3.1',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],reduction('1.1.1.2.2')).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.2',plain,[-(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))), convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])))],extension(12,bind([[_13672, _13728, _13783], [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.2.1',plain,[-(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])), -(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(12,bind([[_13672, _13728, _13783], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.2.1.1',plain,[-(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))), distinct_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))],extension(15,bind([[_18058, _18103], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.2.1.1.1',plain,[-(distinct_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])))],reduction('1.1')).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.2.1.2',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],reduction('1.1.1.2.2')).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.2.2',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))],reduction('1.1.1.2.2.1.1')).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.3',plain,[-(unorthogonal_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []))), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])))],extension(17,bind([[_19541, _19586], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.3.1',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ [])), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), -(convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(12,bind([[_13672, _13728, _13783], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.3.1.1',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],extension(10,bind([[_12546], [parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.2.1.1.3.1.2',plain,[convergent_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],reduction('1.1.1.2.2')).
% 30.74/30.31 cnf('1.1.1.2.3',plain,[unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(6 ^ [], 5 ^ []), 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []))],extension(19,bind([[_20594, _20638], [5 ^ [], orthogonal_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4',plain,[unorthogonal_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])), convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])), 1 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])], 2 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]],extension(18,bind([[_19998, _19925, _19851], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1',plain,[-(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []))), -(3 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])])],extension(3,bind([[_22512, _22427, _22341], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1',plain,[3 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])], 4 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])], convergent_lines(orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), unorthogonal_lines(orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],extension(21,bind([[_22341, _22427, _22512], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.1',plain,[-(4 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]), -(unorthogonal_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(1,bind([[_22427, _22341, _22512], [orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.1.1',plain,[unorthogonal_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), 1 ^ [orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])], 2 ^ [orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]],extension(18,bind([[_19998, _19925, _19851], [orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.1.1.1',plain,[-(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), -(4 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])])],extension(2,bind([[_22512, _22427, _22341], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.1.1.1.1',plain,[4 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]],reduction('1.1.1.2.4.1.1')).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.1.1.2',plain,[-(1 ^ [orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])))],extension(7,bind([[_19925, _19851, _19998], [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.1.1.2.1',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []))],reduction('1.1.1.2.4')).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.1.1.3',plain,[-(2 ^ [orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])))],extension(5,bind([[_19851, _19925, _19998], [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.1.1.3.1',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []))],reduction('1.1.1.2.4')).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.2',plain,[-(convergent_lines(orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), convergent_lines(orthogonal_through_point(6 ^ [], 5 ^ []), 6 ^ []), -(convergent_lines(6 ^ [], parallel_through_point(6 ^ [], 5 ^ [])))],extension(12,bind([[_13672, _13728, _13783], [orthogonal_through_point(6 ^ [], 5 ^ []), 6 ^ [], parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.2.1',plain,[-(convergent_lines(orthogonal_through_point(6 ^ [], 5 ^ []), 6 ^ [])), -(unorthogonal_lines(orthogonal_through_point(6 ^ [], 5 ^ []), 6 ^ []))],extension(17,bind([[_19541, _19586], [orthogonal_through_point(6 ^ [], 5 ^ []), 6 ^ []]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.2.1.1',plain,[unorthogonal_lines(orthogonal_through_point(6 ^ [], 5 ^ []), 6 ^ [])],extension(19,bind([[_20594, _20638], [5 ^ [], 6 ^ []]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.2.2',plain,[convergent_lines(6 ^ [], parallel_through_point(6 ^ [], 5 ^ [])), -(convergent_lines(6 ^ [], 6 ^ [])), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), 6 ^ []))],extension(12,bind([[_13672, _13728, _13783], [6 ^ [], parallel_through_point(6 ^ [], 5 ^ []), 6 ^ []]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.2.2.1',plain,[convergent_lines(6 ^ [], 6 ^ [])],extension(10,bind([[_12546], [6 ^ []]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.2.2.2',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), 6 ^ [])],extension(16,bind([[_18378, _18422], [5 ^ [], 6 ^ []]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.3',plain,[-(unorthogonal_lines(orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), -(convergent_lines(orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(17,bind([[_19541, _19586], [orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.3.1',plain,[convergent_lines(orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), -(convergent_lines(orthogonal_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []))), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])))],extension(12,bind([[_13672, _13728, _13783], [orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.3.1.1',plain,[convergent_lines(orthogonal_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []))],extension(10,bind([[_12546], [orthogonal_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.1.1.3.1.2',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []))],reduction('1.1.1.2.4')).
% 30.74/30.31 cnf('1.1.1.2.4.2',plain,[-(1 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]), -(unorthogonal_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(6,bind([[_19925, _19851, _19998], [orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.2.1',plain,[unorthogonal_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), 1 ^ [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])], 2 ^ [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]],extension(18,bind([[_19998, _19925, _19851], [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.2.1.1',plain,[-(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), -(4 ^ [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])])],extension(2,bind([[_22512, _22427, _22341], [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.2.1.1.1',plain,[4 ^ [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])], 3 ^ [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])], convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), unorthogonal_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],extension(21,bind([[_22341, _22427, _22512], [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.2.1.1.1.1',plain,[-(3 ^ [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(3,bind([[_22512, _22341, _22427], [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.2.1.1.1.1.1',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],extension(10,bind([[_12546], [parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.2.1.1.1.2',plain,[-(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), -(1 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])])],extension(7,bind([[_19998, _19925, _19851], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.2.1.1.1.2.1',plain,[1 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]],reduction('1.1.1.2.4')).
% 30.74/30.31 cnf('1.1.1.2.4.2.1.1.1.3',plain,[-(unorthogonal_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],reduction('1.1.1.2.4.2')).
% 30.74/30.31 cnf('1.1.1.2.4.2.1.2',plain,[-(1 ^ [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(7,bind([[_19925, _19851, _19998], [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.2.1.2.1',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],extension(10,bind([[_12546], [parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.2.1.3',plain,[-(2 ^ [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(5,bind([[_19851, _19925, _19998], [parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.2.1.3.1',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))],extension(10,bind([[_12546], [parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.3',plain,[-(2 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]), -(unorthogonal_lines(orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])))],extension(4,bind([[_19851, _19925, _19998], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.3.1',plain,[unorthogonal_lines(orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), convergent_lines(orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])), 1 ^ [6 ^ [], parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])], 2 ^ [6 ^ [], parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])]],extension(18,bind([[_19998, _19925, _19851], [6 ^ [], parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.3.1.1',plain,[-(convergent_lines(orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []))), -(2 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])])],extension(5,bind([[_19998, _19925, _19851], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]]))).
% 30.74/30.31 cnf('1.1.1.2.4.3.1.1.1',plain,[2 ^ [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ [])]],reduction('1.1.1.2.4')).
% 30.74/30.31 cnf('1.1.1.2.4.3.1.2',plain,[-(1 ^ [6 ^ [], parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])]), -(unorthogonal_lines(orthogonal_through_point(6 ^ [], 5 ^ []), 6 ^ []))],extension(6,bind([[_19925, _19851, _19998], [parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ []), 6 ^ []]]))).
% 30.74/30.31 cnf('1.1.1.2.4.3.1.2.1',plain,[unorthogonal_lines(orthogonal_through_point(6 ^ [], 5 ^ []), 6 ^ [])],extension(19,bind([[_20594, _20638], [5 ^ [], 6 ^ []]]))).
% 30.74/30.31 cnf('1.1.1.2.4.3.1.3',plain,[-(2 ^ [6 ^ [], parallel_through_point(6 ^ [], 5 ^ []), orthogonal_through_point(6 ^ [], 5 ^ [])]), -(convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), 6 ^ []))],extension(5,bind([[_19851, _19925, _19998], [orthogonal_through_point(6 ^ [], 5 ^ []), parallel_through_point(6 ^ [], 5 ^ []), 6 ^ []]]))).
% 30.74/30.31 cnf('1.1.1.2.4.3.1.3.1',plain,[convergent_lines(parallel_through_point(6 ^ [], 5 ^ []), 6 ^ [])],extension(16,bind([[_18378, _18422], [5 ^ [], 6 ^ []]]))).
% 30.74/30.31 %-----------------------------------------------------
% 30.74/30.31
% 30.74/30.32 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------