%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO223+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n029.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:54 EDT 2022
% Result : Theorem 191.46s 184.95s
% Output : Proof 191.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO223+1 : TPTP v8.1.0. Released v3.3.0.
% 0.07/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n029.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Sat Jun 18 12:05:14 EDT 2022
% 0.12/0.34 % CPUTime :
% 191.46/184.95 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 191.46/184.96 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 191.46/184.97
% 191.46/184.97 %-----------------------------------------------------
% 191.46/184.97 fof(oac1, axiom, ! [_40157, _40160, _40163] : (convergent_lines(_40157, _40160) & unorthogonal_lines(_40157, _40160) => convergent_lines(_40157, _40163) & unorthogonal_lines(_40157, _40163) | convergent_lines(_40160, _40163) & unorthogonal_lines(_40160, _40163)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', oac1)).
% 191.46/184.97 fof(con, conjecture, ! [_40427, _40430] : ~ distinct_lines(parallel_through_point(_40430, _40427), orthogonal_through_point(orthogonal_through_point(_40430, _40427), _40427)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 191.46/184.97 fof(ooc1, axiom, ! [_40600, _40603] : ~ unorthogonal_lines(orthogonal_through_point(_40603, _40600), _40603), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', ooc1)).
% 191.46/184.97 fof(ax6, axiom, ! [_40753, _40756, _40759] : (convergent_lines(_40753, _40756) => convergent_lines(_40753, _40759) | convergent_lines(_40756, _40759)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ax6)).
% 191.46/184.97 fof(cp1, axiom, ! [_40938, _40941] : ~ convergent_lines(parallel_through_point(_40941, _40938), _40941), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+2.ax', cp1)).
% 191.46/184.97 fof(ooc2, axiom, ! [_41080, _41083] : ~ apart_point_and_line(_41080, orthogonal_through_point(_41083, _41080)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', ooc2)).
% 191.46/184.97 fof(ouo1, axiom, ! [_41232, _41235, _41238, _41241] : (distinct_lines(_41235, _41238) => apart_point_and_line(_41232, _41235) | apart_point_and_line(_41232, _41238) | unorthogonal_lines(_41235, _41241) | unorthogonal_lines(_41238, _41241)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', ouo1)).
% 191.46/184.97 fof(apart3, axiom, ! [_41496] : ~ convergent_lines(_41496, _41496), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', apart3)).
% 191.46/184.97 fof(cp2, axiom, ! [_41611, _41614] : ~ apart_point_and_line(_41611, parallel_through_point(_41614, _41611)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+2.ax', cp2)).
% 191.46/184.97 fof(occu1, axiom, ! [_41757, _41760] : (convergent_lines(_41757, _41760) | unorthogonal_lines(_41757, _41760)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', occu1)).
% 191.46/184.97
% 191.46/184.97 cnf(1, plain, [unorthogonal_lines(_15753, _15827), convergent_lines(_15753, _15827), -(unorthogonal_lines(_15753, _15900)), -(convergent_lines(_15827, _15900))], clausify(oac1)).
% 191.46/184.97 cnf(2, plain, [-(distinct_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ [])))], clausify(con)).
% 191.46/184.97 cnf(3, plain, [unorthogonal_lines(orthogonal_through_point(_16540, _16496), _16540)], clausify(ooc1)).
% 191.46/184.97 cnf(4, plain, [unorthogonal_lines(_15753, _15827), convergent_lines(_15753, _15827), -(unorthogonal_lines(_15753, _15900)), -(unorthogonal_lines(_15827, _15900))], clausify(oac1)).
% 191.46/184.97 cnf(5, plain, [convergent_lines(_9894, _9950), -(convergent_lines(_9894, _10005)), -(convergent_lines(_9950, _10005))], clausify(ax6)).
% 191.46/184.97 cnf(6, plain, [convergent_lines(parallel_through_point(_14334, _14290), _14334)], clausify(cp1)).
% 191.46/184.97 cnf(7, plain, [apart_point_and_line(_16783, orthogonal_through_point(_16827, _16783))], clausify(ooc2)).
% 191.46/184.97 cnf(8, plain, [unorthogonal_lines(_15753, _15827), convergent_lines(_15753, _15827), -(convergent_lines(_15753, _15900)), -(convergent_lines(_15827, _15900))], clausify(oac1)).
% 191.46/184.97 cnf(9, plain, [distinct_lines(_17133, _17205), -(apart_point_and_line(_17060, _17133)), -(apart_point_and_line(_17060, _17205)), -(unorthogonal_lines(_17133, _17276)), -(unorthogonal_lines(_17205, _17276))], clausify(ouo1)).
% 191.46/184.97 cnf(10, plain, [unorthogonal_lines(_15753, _15827), convergent_lines(_15753, _15827), -(convergent_lines(_15753, _15900)), -(unorthogonal_lines(_15827, _15900))], clausify(oac1)).
% 191.46/184.97 cnf(11, plain, [convergent_lines(_8768, _8768)], clausify(apart3)).
% 191.46/184.97 cnf(12, plain, [apart_point_and_line(_14577, parallel_through_point(_14621, _14577))], clausify(cp2)).
% 191.46/184.97 cnf(13, plain, [-(convergent_lines(_15443, _15488)), -(unorthogonal_lines(_15443, _15488))], clausify(occu1)).
% 191.46/184.97
% 191.46/184.97 cnf('1',plain,[unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ [])],start(3,bind([[_16496, _16540], [1 ^ [], 2 ^ []]]))).
% 191.46/184.97 cnf('1.1',plain,[-(unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ [])), unorthogonal_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])), convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])), -(convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []))],extension(10,bind([[_15827, _15753, _15900], [orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.1',plain,[-(unorthogonal_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []))), distinct_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ [])), -(apart_point_and_line(1 ^ [], parallel_through_point(2 ^ [], 1 ^ []))), -(apart_point_and_line(1 ^ [], orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []))), -(unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])))],extension(9,bind([[_17133, _17060, _17205, _17276], [parallel_through_point(2 ^ [], 1 ^ []), 1 ^ [], orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])]]))).
% 191.46/184.97 cnf('1.1.1.1',plain,[-(distinct_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ [])))],extension(2)).
% 191.46/184.97 cnf('1.1.1.2',plain,[apart_point_and_line(1 ^ [], parallel_through_point(2 ^ [], 1 ^ []))],extension(12,bind([[_14621, _14577], [2 ^ [], 1 ^ []]]))).
% 191.46/184.97 cnf('1.1.1.3',plain,[apart_point_and_line(1 ^ [], orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []))],extension(7,bind([[_16827, _16783], [orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []]]))).
% 191.46/184.97 cnf('1.1.1.4',plain,[unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []))],extension(3,bind([[_16496, _16540], [1 ^ [], orthogonal_through_point(2 ^ [], 1 ^ [])]]))).
% 191.46/184.97 cnf('1.1.2',plain,[-(convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []))), convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ [])), -(convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])))],extension(5,bind([[_9950, _9894, _10005], [parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])]]))).
% 191.46/184.97 cnf('1.1.2.1',plain,[-(convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ []))), convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ []), -(convergent_lines(2 ^ [], parallel_through_point(2 ^ [], 1 ^ [])))],extension(5,bind([[_9894, _9950, _10005], [orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ [], parallel_through_point(2 ^ [], 1 ^ [])]]))).
% 191.46/184.97 cnf('1.1.2.1.1',plain,[-(convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ [])), convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ []), -(convergent_lines(2 ^ [], 2 ^ []))],extension(5,bind([[_9894, _9950, _10005], [orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ [], 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.2.1.1.1',plain,[-(convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ [])), -(unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ []))],extension(13,bind([[_15443, _15488], [orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.2.1.1.1.1',plain,[unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ [])],extension(3,bind([[_16496, _16540], [1 ^ [], 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.2.1.1.2',plain,[convergent_lines(2 ^ [], 2 ^ [])],extension(11,bind([[_8768], [2 ^ []]]))).
% 191.46/184.97 cnf('1.1.2.1.2',plain,[convergent_lines(2 ^ [], parallel_through_point(2 ^ [], 1 ^ [])), -(convergent_lines(2 ^ [], 2 ^ [])), -(convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []))],extension(5,bind([[_9894, _9950, _10005], [2 ^ [], parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.2.1.2.1',plain,[convergent_lines(2 ^ [], 2 ^ [])],extension(11,bind([[_8768], [2 ^ []]]))).
% 191.46/184.97 cnf('1.1.2.1.2.2',plain,[convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ [])],extension(6,bind([[_14290, _14334], [1 ^ [], 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.2.2',plain,[convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])), -(convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ []))), -(convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ [])))],extension(5,bind([[_9894, _9950, _10005], [orthogonal_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ [])]]))).
% 191.46/184.97 cnf('1.1.2.2.1',plain,[convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ [])), -(convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []))), -(convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])))],extension(5,bind([[_9894, _9950, _10005], [orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])]]))).
% 191.46/184.97 cnf('1.1.2.2.1.1',plain,[convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []))],extension(11,bind([[_8768], [orthogonal_through_point(2 ^ [], 1 ^ [])]]))).
% 191.46/184.97 cnf('1.1.2.2.1.2',plain,[convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []))],reduction('1.1')).
% 191.46/184.97 cnf('1.1.2.2.2',plain,[convergent_lines(orthogonal_through_point(2 ^ [], 1 ^ []), parallel_through_point(2 ^ [], 1 ^ []))],lemmata('1.1.2.2')).
% 191.46/184.97 cnf('1.1.3',plain,[convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []), unorthogonal_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []), -(unorthogonal_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ [])), -(convergent_lines(2 ^ [], 2 ^ []))],extension(1,bind([[_15753, _15827, _15900], [parallel_through_point(2 ^ [], 1 ^ []), 2 ^ [], 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.3.1',plain,[-(unorthogonal_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ [])), unorthogonal_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])), convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])), -(unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ []))],extension(4,bind([[_15753, _15827, _15900], [parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.3.1.1',plain,[-(unorthogonal_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []))), distinct_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ [])), -(apart_point_and_line(1 ^ [], parallel_through_point(2 ^ [], 1 ^ []))), -(apart_point_and_line(1 ^ [], orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []))), -(unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])))],extension(9,bind([[_17133, _17060, _17205, _17276], [parallel_through_point(2 ^ [], 1 ^ []), 1 ^ [], orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])]]))).
% 191.46/184.97 cnf('1.1.3.1.1.1',plain,[-(distinct_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ [])))],extension(2)).
% 191.46/184.97 cnf('1.1.3.1.1.2',plain,[apart_point_and_line(1 ^ [], parallel_through_point(2 ^ [], 1 ^ []))],extension(12,bind([[_14621, _14577], [2 ^ [], 1 ^ []]]))).
% 191.46/184.97 cnf('1.1.3.1.1.3',plain,[apart_point_and_line(1 ^ [], orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []))],extension(7,bind([[_16827, _16783], [orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []]]))).
% 191.46/184.97 cnf('1.1.3.1.1.4',plain,[unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(2 ^ [], 1 ^ []), 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ []))],extension(3,bind([[_16496, _16540], [1 ^ [], orthogonal_through_point(2 ^ [], 1 ^ [])]]))).
% 191.46/184.97 cnf('1.1.3.1.2',plain,[-(convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), orthogonal_through_point(2 ^ [], 1 ^ [])))],lemmata('1.1')).
% 191.46/184.97 cnf('1.1.3.1.3',plain,[unorthogonal_lines(orthogonal_through_point(2 ^ [], 1 ^ []), 2 ^ [])],extension(3,bind([[_16496, _16540], [1 ^ [], 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.3.2',plain,[unorthogonal_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []), convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []), -(unorthogonal_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ [])), -(convergent_lines(2 ^ [], 2 ^ []))],extension(1,bind([[_15753, _15827, _15900], [parallel_through_point(2 ^ [], 1 ^ []), 2 ^ [], 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.3.2.1',plain,[-(convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []))],reduction('1.1')).
% 191.46/184.97 cnf('1.1.3.2.2',plain,[unorthogonal_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []), convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []), -(convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ [])), -(convergent_lines(2 ^ [], 2 ^ []))],extension(8,bind([[_15753, _15827, _15900], [parallel_through_point(2 ^ [], 1 ^ []), 2 ^ [], 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.3.2.2.1',plain,[-(convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ []))],lemmata('1.1.3.2')).
% 191.46/184.97 cnf('1.1.3.2.2.2',plain,[convergent_lines(parallel_through_point(2 ^ [], 1 ^ []), 2 ^ [])],extension(6,bind([[_14290, _14334], [1 ^ [], 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.3.2.2.3',plain,[convergent_lines(2 ^ [], 2 ^ [])],extension(11,bind([[_8768], [2 ^ []]]))).
% 191.46/184.97 cnf('1.1.3.2.3',plain,[convergent_lines(2 ^ [], 2 ^ [])],extension(11,bind([[_8768], [2 ^ []]]))).
% 191.46/184.97 cnf('1.1.3.3',plain,[convergent_lines(2 ^ [], 2 ^ []), -(convergent_lines(2 ^ [], parallel_through_point(2 ^ [], _27277))), -(convergent_lines(2 ^ [], parallel_through_point(2 ^ [], _27277)))],extension(5,bind([[_9894, _9950, _10005], [2 ^ [], 2 ^ [], parallel_through_point(2 ^ [], _27277)]]))).
% 191.46/184.97 cnf('1.1.3.3.1',plain,[convergent_lines(2 ^ [], parallel_through_point(2 ^ [], _27277)), -(convergent_lines(2 ^ [], 2 ^ [])), -(convergent_lines(parallel_through_point(2 ^ [], _27277), 2 ^ []))],extension(5,bind([[_9894, _9950, _10005], [2 ^ [], parallel_through_point(2 ^ [], _27277), 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.3.3.1.1',plain,[convergent_lines(2 ^ [], 2 ^ [])],extension(11,bind([[_8768], [2 ^ []]]))).
% 191.46/184.97 cnf('1.1.3.3.1.2',plain,[convergent_lines(parallel_through_point(2 ^ [], _27277), 2 ^ [])],extension(6,bind([[_14290, _14334], [_27277, 2 ^ []]]))).
% 191.46/184.97 cnf('1.1.3.3.2',plain,[convergent_lines(2 ^ [], parallel_through_point(2 ^ [], _27277))],lemmata('1.1.3.3')).
% 191.46/184.97 %-----------------------------------------------------
% 191.46/184.97
% 191.46/184.97 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------