%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO172+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:17:15 PM UTC 2026
% Result : Theorem 23.32s 3.34s
% Output : Proof 23.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO172+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.34 % Computer : n002.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Wed Sep 23 11:18:03 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 23.32/3.34 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.32/3.34 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.32/3.34 fof(sdef0, definition, (spl0 <=> (distinct_points(sk2,X0) | distinct_points(X0,X0))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 23.32/3.34 cnf(p239, plain, (distinct_points(sk2,X0) | distinct_points(X0,X0) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 23.32/3.34 fof(f0, axiom, ! [X] : ~ distinct_points(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart1)).
% 23.32/3.34 fof(f0_nnf, plain, ! [X] : (~(distinct_points(X,X))), inference(nnf_transformation, [status(thm)], [f0])).
% 23.32/3.34 fof(f0_sk, plain, ! [X] : (~(distinct_points(X,X))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 23.32/3.34 cnf(c0, plain, ~distinct_points(X0,X0), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 23.32/3.34 cnf(p262, plain, (distinct_points(sk2,X0) | ~spl0), inference(resolution, [status(thm)], [p239, c0])).
% 23.32/3.34 cnf(p263, plain, ($false | ~spl0), inference(resolution, [status(thm)], [p262, c0])).
% 23.32/3.34 cnf(sct0, plain, (~spl0), inference(avatar_contradiction_clause, [status(thm)], [p263])).
% 23.32/3.34 fof(sdef3, definition, (spl3 <=> (distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 23.32/3.34 cnf(p545, plain, (distinct_points(sk2,X0) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 23.32/3.34 cnf(p546, plain, ($false | ~spl3), inference(resolution, [status(thm)], [p545, c0])).
% 23.32/3.34 cnf(sct1, plain, (~spl3), inference(avatar_contradiction_clause, [status(thm)], [p546])).
% 23.32/3.34 fof(sdef4, definition, (spl4 <=> (distinct_points(intersection_point(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 23.32/3.34 cnf(p566, plain, (distinct_points(intersection_point(sk0,sk1),X0) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 23.32/3.34 cnf(p568, plain, ($false | ~spl4), inference(resolution, [status(thm)], [p566, c0])).
% 23.32/3.34 cnf(sct2, plain, (~spl4), inference(avatar_contradiction_clause, [status(thm)], [p568])).
% 23.32/3.34 fof(sdef6, definition, (spl6 <=> (apart_point_and_line(sk2,sk0))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 23.32/3.34 cnf(p1414, plain, (apart_point_and_line(sk2,sk0) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 23.32/3.34 fof(f12, conjecture, ! [X,Y,Z] : ( ( convergent_lines(X,Y) & ~ apart_point_and_line(Z,X) & ~ apart_point_and_line(Z,Y) ) => ~ distinct_points(Z,intersection_point(X,Y)) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 23.32/3.34 fof(f12_neg, negated_conjecture, ~(! [X,Y,Z] : ( ( convergent_lines(X,Y) & ~ apart_point_and_line(Z,X) & ~ apart_point_and_line(Z,Y) ) => ~ distinct_points(Z,intersection_point(X,Y)) )), inference(negated_conjecture, [status(cth)], [f12])).
% 23.32/3.34 fof(f12_nnf, plain, ? [X,Y,Z] : ((((convergent_lines(X,Y) & ~(apart_point_and_line(Z,X))) & ~(apart_point_and_line(Z,Y))) & distinct_points(Z,intersection_point(X,Y)))), inference(nnf_transformation, [status(thm)], [f12_neg])).
% 23.32/3.34 fof(f12_sk, plain, (((convergent_lines(sk0,sk1) & ~(apart_point_and_line(sk2,sk0))) & ~(apart_point_and_line(sk2,sk1))) & distinct_points(sk2,intersection_point(sk0,sk1))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2])], [f12_nnf])).
% 23.32/3.34 cnf(c15, plain, ~apart_point_and_line(sk2,sk0), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 23.32/3.34 cnf(p1636, plain, ($false | ~spl6), inference(resolution, [status(thm)], [p1414, c15])).
% 23.32/3.34 cnf(sct3, plain, (~spl6), inference(avatar_contradiction_clause, [status(thm)], [p1636])).
% 23.32/3.34 fof(sdef7, definition, (spl7 <=> (apart_point_and_line(sk2,sk1))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 23.32/3.34 cnf(p1415, plain, (apart_point_and_line(sk2,sk1) | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 23.32/3.34 cnf(c16, plain, ~apart_point_and_line(sk2,sk1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 23.32/3.34 cnf(p1637, plain, ($false | ~spl7), inference(resolution, [status(thm)], [p1415, c16])).
% 23.32/3.34 cnf(sct4, plain, (~spl7), inference(avatar_contradiction_clause, [status(thm)], [p1637])).
% 23.32/3.34 fof(sdef83, definition, (spl83 <=> (convergent_lines(sk0,sk0))), introduced(definition, [new_symbols(naming, [spl83])], [avatar_definition])).
% 23.32/3.34 cnf(p1651, plain, (convergent_lines(sk0,sk0) | ~spl83), inference(avatar_component_clause, [status(thm)], [sdef83])).
% 23.32/3.34 fof(f2, axiom, ! [X] : ~ convergent_lines(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart3)).
% 23.32/3.34 fof(f2_nnf, plain, ! [X] : (~(convergent_lines(X,X))), inference(nnf_transformation, [status(thm)], [f2])).
% 23.32/3.34 fof(f2_sk, plain, ! [X] : (~(convergent_lines(X,X))), inference(skolemisation, [status(esa)], [f2_nnf])).
% 23.32/3.34 cnf(c2, plain, ~convergent_lines(X0,X0), inference(cnf_transformation, [status(esa)], [f2_sk])).
% 23.32/3.34 cnf(p1657, plain, ($false | ~spl83), inference(resolution, [status(thm)], [p1651, c2])).
% 23.32/3.34 cnf(sct5, plain, (~spl83), inference(avatar_contradiction_clause, [status(thm)], [p1657])).
% 23.32/3.34 fof(sdef84, definition, (spl84 <=> (distinct_lines(sk0,sk0))), introduced(definition, [new_symbols(naming, [spl84])], [avatar_definition])).
% 23.32/3.34 cnf(p1654, plain, (distinct_lines(sk0,sk0) | ~spl84), inference(avatar_component_clause, [status(thm)], [sdef84])).
% 23.32/3.34 fof(f1, axiom, ! [X] : ~ distinct_lines(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart2)).
% 23.32/3.34 fof(f1_nnf, plain, ! [X] : (~(distinct_lines(X,X))), inference(nnf_transformation, [status(thm)], [f1])).
% 23.32/3.34 fof(f1_sk, plain, ! [X] : (~(distinct_lines(X,X))), inference(skolemisation, [status(esa)], [f1_nnf])).
% 23.32/3.34 cnf(c1, plain, ~distinct_lines(X0,X0), inference(cnf_transformation, [status(esa)], [f1_sk])).
% 23.32/3.34 cnf(p1864, plain, ($false | ~spl84), inference(resolution, [status(thm)], [p1654, c1])).
% 23.32/3.34 cnf(sct6, plain, (~spl84), inference(avatar_contradiction_clause, [status(thm)], [p1864])).
% 23.32/3.34 fof(sdef8, definition, (spl8 <=> (apart_point_and_line(intersection_point(sk0,sk1),sk0))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 23.32/3.34 cnf(p1416, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk0) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 23.32/3.34 fof(f7, axiom, ! [X,Y,Z] : ( convergent_lines(X,Y) => ( ( apart_point_and_line(Z,X) | apart_point_and_line(Z,Y) ) => distinct_points(Z,intersection_point(X,Y)) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con2)).
% 23.32/3.34 fof(f7_nnf, plain, ! [X,Y,Z] : ((~(convergent_lines(X,Y)) | ((~(apart_point_and_line(Z,X)) & ~(apart_point_and_line(Z,Y))) | distinct_points(Z,intersection_point(X,Y))))), inference(nnf_transformation, [status(thm)], [f7])).
% 23.32/3.34 fof(f7_sk, plain, ! [X,Y,Z] : ((~(convergent_lines(X,Y)) | ((~(apart_point_and_line(Z,X)) & ~(apart_point_and_line(Z,Y))) | distinct_points(Z,intersection_point(X,Y))))), inference(skolemisation, [status(esa)], [f7_nnf])).
% 23.32/3.34 cnf(c8, plain, ~convergent_lines(X0,X1) | ~apart_point_and_line(X2,X0) | distinct_points(X2,intersection_point(X0,X1)), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 23.32/3.34 cnf(c14, plain, convergent_lines(sk0,sk1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 23.32/3.34 cnf(p88, plain, ~apart_point_and_line(X0,sk0) | distinct_points(X0,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [c8, c14])).
% 23.32/3.34 cnf(p1638, plain, (distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)) | ~spl8), inference(resolution, [status(thm)], [p1416, p88])).
% 23.32/3.34 cnf(p1880, plain, ($false | ~spl8), inference(resolution, [status(thm)], [p1638, c0])).
% 23.32/3.34 cnf(sct7, plain, (~spl8), inference(avatar_contradiction_clause, [status(thm)], [p1880])).
% 23.32/3.34 fof(sdef9, definition, (spl9 <=> (apart_point_and_line(intersection_point(sk0,sk1),sk1))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 23.32/3.34 cnf(p1417, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk1) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 23.32/3.34 cnf(c9, plain, ~convergent_lines(X0,X1) | ~apart_point_and_line(X2,X1) | distinct_points(X2,intersection_point(X0,X1)), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 23.32/3.34 cnf(p109, plain, ~apart_point_and_line(X0,sk1) | distinct_points(X0,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [c9, c14])).
% 23.32/3.34 cnf(p1865, plain, (distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)) | ~spl9), inference(resolution, [status(thm)], [p1417, p109])).
% 23.32/3.34 cnf(p1881, plain, ($false | ~spl9), inference(resolution, [status(thm)], [p1865, c0])).
% 23.32/3.34 cnf(sct8, plain, (~spl9), inference(avatar_contradiction_clause, [status(thm)], [p1881])).
% 23.32/3.34 fof(f3, axiom, ! [X,Y,Z] : ( distinct_points(X,Y) => ( distinct_points(X,Z) | distinct_points(Y,Z) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart4)).
% 23.32/3.34 fof(f3_nnf, plain, ! [X,Y,Z] : ((~(distinct_points(X,Y)) | (distinct_points(X,Z) | distinct_points(Y,Z)))), inference(nnf_transformation, [status(thm)], [f3])).
% 23.32/3.34 fof(f3_sk, plain, ! [X,Y,Z] : ((~(distinct_points(X,Y)) | (distinct_points(X,Z) | distinct_points(Y,Z)))), inference(skolemisation, [status(esa)], [f3_nnf])).
% 23.32/3.34 cnf(c3, plain, ~distinct_points(X0,X1) | distinct_points(X0,X2) | distinct_points(X1,X2), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 23.32/3.34 cnf(c17, plain, distinct_points(sk2,intersection_point(sk0,sk1)), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 23.32/3.34 cnf(p19, plain, distinct_points(sk2,X0) | distinct_points(intersection_point(sk0,sk1),X0), inference(resolution, [status(thm)], [c3, c17])).
% 23.32/3.34 cnf(p20, plain, distinct_points(sk2,X0) | distinct_points(intersection_point(sk0,sk1),X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p19, c3])).
% 23.32/3.34 cnf(p24, plain, distinct_points(sk2,X0) | distinct_points(intersection_point(sk0,sk1),X1) | distinct_points(X0,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [p20, c3])).
% 23.32/3.34 cnf(p238, plain, distinct_points(sk2,X0) | distinct_points(intersection_point(sk0,sk1),sk2) | distinct_points(X0,X0), inference(factoring, [status(thm)], [p24])).
% 23.32/3.34 fof(sdef1, definition, (spl1 <=> (distinct_points(intersection_point(sk0,sk1),sk2))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 23.32/3.34 cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [p238, sdef0, sdef1])).
% 23.32/3.34 fof(f6, axiom, ! [X,Y,Z] : ( distinct_points(X,Y) => ( apart_point_and_line(Z,line_connecting(X,Y)) => ( distinct_points(Z,X) & distinct_points(Z,Y) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con1)).
% 23.32/3.34 fof(f6_nnf, plain, ! [X,Y,Z] : ((~(distinct_points(X,Y)) | (~(apart_point_and_line(Z,line_connecting(X,Y))) | (distinct_points(Z,X) & distinct_points(Z,Y))))), inference(nnf_transformation, [status(thm)], [f6])).
% 23.32/3.34 fof(f6_sk, plain, ! [X,Y,Z] : ((~(distinct_points(X,Y)) | (~(apart_point_and_line(Z,line_connecting(X,Y))) | (distinct_points(Z,X) & distinct_points(Z,Y))))), inference(skolemisation, [status(esa)], [f6_nnf])).
% 23.32/3.34 cnf(c6, plain, ~distinct_points(X0,X1) | ~apart_point_and_line(X2,line_connecting(X0,X1)) | distinct_points(X2,X0), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 23.32/3.34 cnf(p22, plain, distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X1,X0) | distinct_points(sk2,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [p20, c3])).
% 23.32/3.34 cnf(p55, plain, ~apart_point_and_line(X0,line_connecting(X1,X2)) | distinct_points(X0,X1) | distinct_points(intersection_point(sk0,sk1),X2) | distinct_points(sk2,X3) | distinct_points(X1,X3), inference(resolution, [status(thm)], [c6, p22])).
% 23.32/3.34 cnf(p543, plain, ~apart_point_and_line(X0,line_connecting(sk2,X1)) | distinct_points(X0,sk2) | distinct_points(intersection_point(sk0,sk1),X1) | distinct_points(sk2,X2), inference(factoring, [status(thm)], [p55])).
% 23.32/3.34 fof(sdef2, definition, (spl2 <=> (~apart_point_and_line(X0,line_connecting(sk2,X1)) | distinct_points(X0,sk2) | distinct_points(intersection_point(sk0,sk1),X1))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 23.32/3.34 cnf(ssp1, plain, (spl2 | spl3), inference(avatar_split_clause, [status(thm)], [p543, sdef2, sdef3])).
% 23.32/3.34 cnf(p56, plain, ~apart_point_and_line(X0,line_connecting(sk2,X1)) | distinct_points(X0,sk2) | distinct_points(intersection_point(sk0,sk1),X2) | distinct_points(X3,X2) | distinct_points(X3,X1), inference(resolution, [status(thm)], [c6, p22])).
% 23.32/3.34 cnf(p565, plain, ~apart_point_and_line(X0,line_connecting(sk2,X1)) | distinct_points(X0,sk2) | distinct_points(intersection_point(sk0,sk1),X2) | distinct_points(intersection_point(sk0,sk1),X1), inference(factoring, [status(thm)], [p56])).
% 23.32/3.34 cnf(ssp2, plain, (spl2 | spl4), inference(avatar_split_clause, [status(thm)], [p565, sdef2, sdef4])).
% 23.32/3.34 cnf(c7, plain, ~distinct_points(X0,X1) | ~apart_point_and_line(X2,line_connecting(X0,X1)) | distinct_points(X2,X1), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 23.32/3.34 cnf(p79, plain, ~apart_point_and_line(X0,line_connecting(X1,X2)) | distinct_points(X0,X2) | distinct_points(intersection_point(sk0,sk1),X2) | distinct_points(sk2,X3) | distinct_points(X1,X3), inference(resolution, [status(thm)], [c7, p22])).
% 23.32/3.34 cnf(p774, plain, ~apart_point_and_line(X0,line_connecting(sk2,X1)) | distinct_points(X0,X1) | distinct_points(intersection_point(sk0,sk1),X1) | distinct_points(sk2,X2), inference(factoring, [status(thm)], [p79])).
% 23.32/3.34 fof(sdef5, definition, (spl5 <=> (~apart_point_and_line(X0,line_connecting(sk2,X1)) | distinct_points(X0,X1) | distinct_points(intersection_point(sk0,sk1),X1))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 23.32/3.34 cnf(ssp3, plain, (spl3 | spl5), inference(avatar_split_clause, [status(thm)], [p774, sdef3, sdef5])).
% 23.32/3.34 cnf(p80, plain, ~apart_point_and_line(X0,line_connecting(sk2,X1)) | distinct_points(X0,X1) | distinct_points(intersection_point(sk0,sk1),X2) | distinct_points(X3,X2) | distinct_points(X3,X1), inference(resolution, [status(thm)], [c7, p22])).
% 23.32/3.34 cnf(p806, plain, ~apart_point_and_line(X0,line_connecting(sk2,X1)) | distinct_points(X0,X1) | distinct_points(intersection_point(sk0,sk1),X2) | distinct_points(intersection_point(sk0,sk1),X1), inference(factoring, [status(thm)], [p80])).
% 23.32/3.34 cnf(ssp4, plain, (spl4 | spl5), inference(avatar_split_clause, [status(thm)], [p806, sdef4, sdef5])).
% 23.32/3.34 fof(f8, axiom, ! [X,Y,U,V] : ( ( distinct_points(X,Y) & distinct_lines(U,V) ) => ( apart_point_and_line(X,U) | apart_point_and_line(X,V) | apart_point_and_line(Y,U) | apart_point_and_line(Y,V) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cu1)).
% 23.32/3.34 fof(f8_nnf, plain, ! [X,Y,U,V] : (((~(distinct_points(X,Y)) | ~(distinct_lines(U,V))) | (((apart_point_and_line(X,U) | apart_point_and_line(X,V)) | apart_point_and_line(Y,U)) | apart_point_and_line(Y,V)))), inference(nnf_transformation, [status(thm)], [f8])).
% 23.32/3.34 fof(f8_sk, plain, ! [X,Y,U,V] : (((~(distinct_points(X,Y)) | ~(distinct_lines(U,V))) | (((apart_point_and_line(X,U) | apart_point_and_line(X,V)) | apart_point_and_line(Y,U)) | apart_point_and_line(Y,V)))), inference(skolemisation, [status(esa)], [f8_nnf])).
% 23.32/3.34 cnf(c10, plain, ~distinct_points(X0,X1) | ~distinct_lines(X2,X3) | apart_point_and_line(X0,X2) | apart_point_and_line(X0,X3) | apart_point_and_line(X1,X2) | apart_point_and_line(X1,X3), inference(cnf_transformation, [status(esa)], [f8_sk])).
% 23.32/3.34 cnf(p139, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1), inference(resolution, [status(thm)], [c10, c17])).
% 23.32/3.34 fof(f11, axiom, ! [X,Y] : ( convergent_lines(X,Y) => distinct_lines(X,Y) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ceq3)).
% 23.32/3.34 fof(f11_nnf, plain, ! [X,Y] : ((~(convergent_lines(X,Y)) | distinct_lines(X,Y))), inference(nnf_transformation, [status(thm)], [f11])).
% 23.32/3.34 fof(f11_sk, plain, ! [X,Y] : ((~(convergent_lines(X,Y)) | distinct_lines(X,Y))), inference(skolemisation, [status(esa)], [f11_nnf])).
% 23.32/3.34 cnf(c13, plain, ~convergent_lines(X0,X1) | distinct_lines(X0,X1), inference(cnf_transformation, [status(esa)], [f11_sk])).
% 23.32/3.34 cnf(p18, plain, distinct_lines(sk0,sk1), inference(resolution, [status(thm)], [c13, c14])).
% 23.32/3.34 cnf(p1413, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,sk1) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),sk1), inference(resolution, [status(thm)], [p139, p18])).
% 23.32/3.34 cnf(ssp5, plain, (spl6 | spl7 | spl8 | spl9), inference(avatar_split_clause, [status(thm)], [p1413, sdef6, sdef7, sdef8, sdef9])).
% 23.32/3.34 fof(f4, axiom, ! [X,Y,Z] : ( distinct_lines(X,Y) => ( distinct_lines(X,Z) | distinct_lines(Y,Z) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart5)).
% 23.32/3.34 fof(f4_nnf, plain, ! [X,Y,Z] : ((~(distinct_lines(X,Y)) | (distinct_lines(X,Z) | distinct_lines(Y,Z)))), inference(nnf_transformation, [status(thm)], [f4])).
% 23.32/3.34 fof(f4_sk, plain, ! [X,Y,Z] : ((~(distinct_lines(X,Y)) | (distinct_lines(X,Z) | distinct_lines(Y,Z)))), inference(skolemisation, [status(esa)], [f4_nnf])).
% 23.32/3.34 cnf(c4, plain, ~distinct_lines(X0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 23.32/3.34 cnf(p32, plain, distinct_lines(sk0,X0) | distinct_lines(sk1,X0), inference(resolution, [status(thm)], [c4, p18])).
% 23.32/3.34 cnf(p1418, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X0), inference(resolution, [status(thm)], [p139, p32])).
% 23.32/3.34 fof(sdef10, definition, (spl10 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 23.32/3.34 cnf(ssp6, plain, (spl7 | spl9 | spl10), inference(avatar_split_clause, [status(thm)], [p1418, sdef7, sdef9, sdef10])).
% 23.32/3.34 cnf(p33, plain, distinct_lines(sk0,X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p32, c4])).
% 23.32/3.34 cnf(p1420, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p139, p33])).
% 23.32/3.34 fof(sdef11, definition, (spl11 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 23.32/3.34 cnf(ssp7, plain, (spl6 | spl8 | spl11), inference(avatar_split_clause, [status(thm)], [p1420, sdef6, sdef8, sdef11])).
% 23.32/3.34 cnf(p1422, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p139, p33])).
% 23.32/3.34 fof(sdef12, definition, (spl12 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 23.32/3.34 cnf(ssp8, plain, (spl7 | spl9 | spl12), inference(avatar_split_clause, [status(thm)], [p1422, sdef7, sdef9, sdef12])).
% 23.32/3.34 cnf(p1424, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk0,X0) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p139, p33])).
% 23.32/3.34 fof(sdef13, definition, (spl13 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X0))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 23.32/3.34 cnf(ssp9, plain, (spl10 | spl13), inference(avatar_split_clause, [status(thm)], [p1424, sdef10, sdef13])).
% 23.32/3.34 cnf(p34, plain, distinct_lines(sk0,X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p33, c1])).
% 23.32/3.34 cnf(p1426, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p139, p34])).
% 23.32/3.34 fof(sdef14, definition, (spl14 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,sk1))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 23.32/3.34 cnf(ssp10, plain, (spl6 | spl8 | spl14), inference(avatar_split_clause, [status(thm)], [p1426, sdef6, sdef8, sdef14])).
% 23.32/3.34 cnf(p38, plain, distinct_lines(X0,sk1) | distinct_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p34, c4])).
% 23.32/3.34 cnf(p1428, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | distinct_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p139, p38])).
% 23.32/3.34 fof(sdef15, definition, (spl15 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 23.32/3.34 cnf(ssp11, plain, (spl7 | spl9 | spl15), inference(avatar_split_clause, [status(thm)], [p1428, sdef7, sdef9, sdef15])).
% 23.32/3.34 cnf(p1430, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p139, p38])).
% 23.32/3.34 fof(sdef16, definition, (spl16 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 23.32/3.34 cnf(ssp12, plain, (spl6 | spl8 | spl16), inference(avatar_split_clause, [status(thm)], [p1430, sdef6, sdef8, sdef16])).
% 23.32/3.34 cnf(p1432, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p38])).
% 23.32/3.34 cnf(ssp13, plain, (spl10 | spl14), inference(avatar_split_clause, [status(thm)], [p1432, sdef10, sdef14])).
% 23.32/3.34 cnf(p39, plain, distinct_lines(X0,sk1) | distinct_lines(X0,sk0), inference(resolution, [status(thm)], [p38, c1])).
% 23.32/3.34 cnf(p1433, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | distinct_lines(X0,sk0), inference(resolution, [status(thm)], [p139, p39])).
% 23.32/3.34 fof(sdef17, definition, (spl17 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,sk0))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 23.32/3.34 cnf(ssp14, plain, (spl7 | spl9 | spl17), inference(avatar_split_clause, [status(thm)], [p1433, sdef7, sdef9, sdef17])).
% 23.32/3.34 cnf(p44, plain, distinct_lines(X0,sk0) | distinct_lines(X0,X1) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p39, c4])).
% 23.32/3.34 cnf(p1435, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk0) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p139, p44])).
% 23.32/3.34 cnf(ssp15, plain, (spl13 | spl17), inference(avatar_split_clause, [status(thm)], [p1435, sdef13, sdef17])).
% 23.32/3.34 cnf(p1436, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p139, p44])).
% 23.32/3.34 fof(sdef18, definition, (spl18 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 23.32/3.34 cnf(ssp16, plain, (spl7 | spl9 | spl18), inference(avatar_split_clause, [status(thm)], [p1436, sdef7, sdef9, sdef18])).
% 23.32/3.34 cnf(p58, plain, distinct_lines(X0,sk0) | distinct_lines(sk1,X0), inference(resolution, [status(thm)], [p44, c1])).
% 23.32/3.34 cnf(p1438, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | distinct_lines(sk1,X0), inference(resolution, [status(thm)], [p139, p58])).
% 23.32/3.34 cnf(ssp17, plain, (spl6 | spl8 | spl13), inference(avatar_split_clause, [status(thm)], [p1438, sdef6, sdef8, sdef13])).
% 23.32/3.34 cnf(p61, plain, distinct_lines(sk1,X0) | distinct_lines(X0,X1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p58, c4])).
% 23.32/3.34 cnf(p1439, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p139, p61])).
% 23.32/3.34 fof(sdef19, definition, (spl19 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 23.32/3.34 cnf(ssp18, plain, (spl6 | spl8 | spl19), inference(avatar_split_clause, [status(thm)], [p1439, sdef6, sdef8, sdef19])).
% 23.32/3.34 fof(f5, axiom, ! [X,Y,Z] : ( convergent_lines(X,Y) => ( convergent_lines(X,Z) | convergent_lines(Y,Z) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart6)).
% 23.32/3.34 fof(f5_nnf, plain, ! [X,Y,Z] : ((~(convergent_lines(X,Y)) | (convergent_lines(X,Z) | convergent_lines(Y,Z)))), inference(nnf_transformation, [status(thm)], [f5])).
% 23.32/3.34 fof(f5_sk, plain, ! [X,Y,Z] : ((~(convergent_lines(X,Y)) | (convergent_lines(X,Z) | convergent_lines(Y,Z)))), inference(skolemisation, [status(esa)], [f5_nnf])).
% 23.32/3.34 cnf(c5, plain, ~convergent_lines(X0,X1) | convergent_lines(X0,X2) | convergent_lines(X1,X2), inference(cnf_transformation, [status(esa)], [f5_sk])).
% 23.32/3.34 cnf(p42, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X0), inference(resolution, [status(thm)], [c5, c14])).
% 23.32/3.34 cnf(p46, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p42, c5])).
% 23.32/3.34 cnf(p65, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p46, c13])).
% 23.32/3.34 cnf(p1441, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk0,X0) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p139, p65])).
% 23.32/3.34 fof(sdef20, definition, (spl20 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 23.32/3.34 fof(sdef21, definition, (spl21 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X0))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 23.32/3.34 cnf(ssp19, plain, (spl20 | spl21), inference(avatar_split_clause, [status(thm)], [p1441, sdef20, sdef21])).
% 23.32/3.34 cnf(p45, plain, convergent_lines(sk0,X0) | distinct_lines(sk1,X0), inference(resolution, [status(thm)], [p42, c13])).
% 23.32/3.34 cnf(p47, plain, distinct_lines(sk1,X0) | convergent_lines(sk0,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p45, c5])).
% 23.32/3.34 cnf(p85, plain, distinct_lines(sk1,X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p47, c13])).
% 23.32/3.34 cnf(p1444, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p139, p85])).
% 23.32/3.34 fof(sdef22, definition, (spl22 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 23.32/3.34 cnf(ssp20, plain, (spl7 | spl9 | spl22), inference(avatar_split_clause, [status(thm)], [p1444, sdef7, sdef9, sdef22])).
% 23.32/3.34 cnf(p1446, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk1,X0) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p85])).
% 23.32/3.34 cnf(ssp21, plain, (spl13 | spl20), inference(avatar_split_clause, [status(thm)], [p1446, sdef13, sdef20])).
% 23.32/3.34 cnf(p63, plain, convergent_lines(sk1,X0) | convergent_lines(X1,X0) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p46, c13])).
% 23.32/3.34 cnf(p104, plain, convergent_lines(sk1,X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p63, c13])).
% 23.32/3.34 cnf(p1447, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p139, p104])).
% 23.32/3.34 fof(sdef23, definition, (spl23 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 23.32/3.34 cnf(ssp22, plain, (spl6 | spl8 | spl23), inference(avatar_split_clause, [status(thm)], [p1447, sdef6, sdef8, sdef23])).
% 23.32/3.34 cnf(p1449, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk1,X1) | distinct_lines(sk0,X0), inference(resolution, [status(thm)], [p139, p104])).
% 23.32/3.34 cnf(ssp23, plain, (spl10 | spl21), inference(avatar_split_clause, [status(thm)], [p1449, sdef10, sdef21])).
% 23.32/3.34 cnf(p64, plain, convergent_lines(sk0,X0) | convergent_lines(X0,X1) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p46, c13])).
% 23.32/3.34 cnf(p126, plain, convergent_lines(sk0,X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p64, c13])).
% 23.32/3.34 cnf(p1450, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p139, p126])).
% 23.32/3.34 fof(sdef24, definition, (spl24 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 23.32/3.34 cnf(ssp24, plain, (spl7 | spl9 | spl24), inference(avatar_split_clause, [status(thm)], [p1450, sdef7, sdef9, sdef24])).
% 23.32/3.34 cnf(p62, plain, convergent_lines(sk0,X0) | convergent_lines(X0,sk1), inference(resolution, [status(thm)], [p46, c2])).
% 23.32/3.34 cnf(p71, plain, convergent_lines(X0,sk1) | convergent_lines(sk0,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p62, c5])).
% 23.32/3.34 cnf(p150, plain, convergent_lines(X0,sk1) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p71, c13])).
% 23.32/3.34 cnf(p1452, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk1) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p150])).
% 23.32/3.34 fof(sdef25, definition, (spl25 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X0,sk1))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 23.32/3.34 cnf(ssp25, plain, (spl20 | spl25), inference(avatar_split_clause, [status(thm)], [p1452, sdef20, sdef25])).
% 23.32/3.34 cnf(p70, plain, convergent_lines(sk0,X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p62, c13])).
% 23.32/3.34 cnf(p82, plain, distinct_lines(X0,sk1) | convergent_lines(sk0,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p70, c5])).
% 23.32/3.34 cnf(p169, plain, distinct_lines(X0,sk1) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p82, c13])).
% 23.32/3.34 cnf(p1454, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk1) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p169])).
% 23.32/3.34 cnf(ssp26, plain, (spl14 | spl20), inference(avatar_split_clause, [status(thm)], [p1454, sdef14, sdef20])).
% 23.32/3.34 cnf(p149, plain, convergent_lines(X0,sk1) | convergent_lines(X0,X1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p71, c13])).
% 23.32/3.34 cnf(p209, plain, convergent_lines(X0,sk1) | distinct_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p149, c13])).
% 23.32/3.34 cnf(p1455, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p139, p209])).
% 23.32/3.34 fof(sdef26, definition, (spl26 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 23.32/3.34 cnf(ssp27, plain, (spl6 | spl8 | spl26), inference(avatar_split_clause, [status(thm)], [p1455, sdef6, sdef8, sdef26])).
% 23.32/3.34 cnf(p1457, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p209])).
% 23.32/3.34 cnf(ssp28, plain, (spl10 | spl25), inference(avatar_split_clause, [status(thm)], [p1457, sdef10, sdef25])).
% 23.32/3.34 cnf(p148, plain, convergent_lines(X0,sk1) | convergent_lines(X0,sk0), inference(resolution, [status(thm)], [p71, c2])).
% 23.32/3.34 cnf(p161, plain, convergent_lines(X0,sk0) | convergent_lines(X0,X1) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p148, c5])).
% 23.32/3.34 cnf(p228, plain, convergent_lines(X0,sk0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p161, c13])).
% 23.32/3.34 cnf(p1458, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk0) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p139, p228])).
% 23.32/3.34 fof(sdef27, definition, (spl27 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X0,sk0))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 23.32/3.34 cnf(ssp29, plain, (spl21 | spl27), inference(avatar_split_clause, [status(thm)], [p1458, sdef21, sdef27])).
% 23.32/3.34 cnf(p216, plain, convergent_lines(X0,sk1) | distinct_lines(X0,sk0), inference(resolution, [status(thm)], [p150, c2])).
% 23.32/3.34 cnf(p224, plain, distinct_lines(X0,sk0) | convergent_lines(X0,X1) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p216, c5])).
% 23.32/3.34 cnf(p307, plain, distinct_lines(X0,sk0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p224, c13])).
% 23.32/3.34 cnf(p1460, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk0) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p139, p307])).
% 23.32/3.34 cnf(ssp30, plain, (spl17 | spl21), inference(avatar_split_clause, [status(thm)], [p1460, sdef17, sdef21])).
% 23.32/3.34 cnf(p325, plain, convergent_lines(X0,sk0) | distinct_lines(X0,X1) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p228, c13])).
% 23.32/3.34 cnf(p1461, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk0) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p139, p325])).
% 23.32/3.34 cnf(ssp31, plain, (spl13 | spl27), inference(avatar_split_clause, [status(thm)], [p1461, sdef13, sdef27])).
% 23.32/3.34 cnf(p1462, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk0) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p139, p325])).
% 23.32/3.34 fof(sdef28, definition, (spl28 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk0) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 23.32/3.34 cnf(ssp32, plain, (spl7 | spl9 | spl28), inference(avatar_split_clause, [status(thm)], [p1462, sdef7, sdef9, sdef28])).
% 23.32/3.34 cnf(p227, plain, convergent_lines(X0,sk0) | convergent_lines(sk1,X0), inference(resolution, [status(thm)], [p161, c2])).
% 23.32/3.34 cnf(p256, plain, convergent_lines(sk1,X0) | convergent_lines(X0,X1) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p227, c5])).
% 23.32/3.34 cnf(p337, plain, convergent_lines(sk1,X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p256, c13])).
% 23.32/3.34 cnf(p378, plain, convergent_lines(sk1,X0) | distinct_lines(X0,X1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p337, c13])).
% 23.32/3.34 cnf(p1464, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p139, p378])).
% 23.32/3.34 fof(sdef29, definition, (spl29 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 23.32/3.34 cnf(ssp33, plain, (spl6 | spl8 | spl29), inference(avatar_split_clause, [status(thm)], [p1464, sdef6, sdef8, sdef29])).
% 23.32/3.34 cnf(p35, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p33, c4])).
% 23.32/3.34 cnf(p1466, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,X0) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p139, p35])).
% 23.32/3.34 fof(sdef30, definition, (spl30 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,X0) | distinct_lines(sk0,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 23.32/3.34 cnf(ssp34, plain, (spl7 | spl9 | spl30), inference(avatar_split_clause, [status(thm)], [p1466, sdef7, sdef9, sdef30])).
% 23.32/3.34 cnf(p1468, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk1,X1) | distinct_lines(sk0,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p139, p35])).
% 23.32/3.34 cnf(ssp35, plain, (spl13 | spl15), inference(avatar_split_clause, [status(thm)], [p1468, sdef13, sdef15])).
% 23.32/3.34 cnf(p1469, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X2,X1) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p139, p35])).
% 23.32/3.34 fof(sdef31, definition, (spl31 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X2,X1) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 23.32/3.34 cnf(ssp36, plain, (spl6 | spl8 | spl31), inference(avatar_split_clause, [status(thm)], [p1469, sdef6, sdef8, sdef31])).
% 23.32/3.34 cnf(p1471, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk1,X2) | distinct_lines(X0,X2) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p35])).
% 23.32/3.34 cnf(ssp37, plain, (spl10 | spl11), inference(avatar_split_clause, [status(thm)], [p1471, sdef10, sdef11])).
% 23.32/3.34 cnf(p36, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p33, c4])).
% 23.32/3.34 cnf(p1472, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p139, p36])).
% 23.32/3.34 fof(sdef32, definition, (spl32 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 23.32/3.34 cnf(ssp38, plain, (spl6 | spl8 | spl32), inference(avatar_split_clause, [status(thm)], [p1472, sdef6, sdef8, sdef32])).
% 23.32/3.34 cnf(p1474, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p139, p36])).
% 23.32/3.34 fof(sdef33, definition, (spl33 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 23.32/3.34 cnf(ssp39, plain, (spl7 | spl9 | spl33), inference(avatar_split_clause, [status(thm)], [p1474, sdef7, sdef9, sdef33])).
% 23.32/3.34 cnf(p1476, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk0,X2) | distinct_lines(X2,X0) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p139, p36])).
% 23.32/3.34 cnf(ssp40, plain, (spl12 | spl13), inference(avatar_split_clause, [status(thm)], [p1476, sdef12, sdef13])).
% 23.32/3.34 cnf(p444, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X1,sk1), inference(resolution, [status(thm)], [p36, c1])).
% 23.32/3.34 cnf(p1477, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | distinct_lines(X1,sk1), inference(resolution, [status(thm)], [p139, p444])).
% 23.32/3.34 fof(sdef34, definition, (spl34 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | distinct_lines(X1,sk1))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 23.32/3.34 cnf(ssp41, plain, (spl6 | spl8 | spl34), inference(avatar_split_clause, [status(thm)], [p1477, sdef6, sdef8, sdef34])).
% 23.32/3.34 cnf(p37, plain, distinct_lines(sk0,X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p33, c4])).
% 23.32/3.34 cnf(p1479, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p139, p37])).
% 23.32/3.34 fof(sdef35, definition, (spl35 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 23.32/3.34 cnf(ssp42, plain, (spl6 | spl8 | spl35), inference(avatar_split_clause, [status(thm)], [p1479, sdef6, sdef8, sdef35])).
% 23.32/3.34 cnf(p1481, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p139, p37])).
% 23.32/3.34 fof(sdef36, definition, (spl36 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 23.32/3.34 cnf(ssp43, plain, (spl7 | spl9 | spl36), inference(avatar_split_clause, [status(thm)], [p1481, sdef7, sdef9, sdef36])).
% 23.32/3.34 cnf(p1483, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk0,X0) | distinct_lines(sk1,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p37])).
% 23.32/3.34 cnf(ssp44, plain, (spl10 | spl19), inference(avatar_split_clause, [status(thm)], [p1483, sdef10, sdef19])).
% 23.32/3.34 cnf(p40, plain, distinct_lines(X0,sk1) | distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p38, c4])).
% 23.32/3.34 cnf(p1484, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p139, p40])).
% 23.32/3.34 fof(sdef37, definition, (spl37 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 23.32/3.34 cnf(ssp45, plain, (spl7 | spl9 | spl37), inference(avatar_split_clause, [status(thm)], [p1484, sdef7, sdef9, sdef37])).
% 23.32/3.34 cnf(p1486, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk1) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p139, p40])).
% 23.32/3.34 cnf(ssp46, plain, (spl14 | spl15), inference(avatar_split_clause, [status(thm)], [p1486, sdef14, sdef15])).
% 23.32/3.34 cnf(p1487, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p139, p40])).
% 23.32/3.34 fof(sdef38, definition, (spl38 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 23.32/3.34 cnf(ssp47, plain, (spl6 | spl8 | spl38), inference(avatar_split_clause, [status(thm)], [p1487, sdef6, sdef8, sdef38])).
% 23.32/3.34 cnf(p1489, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X2,sk1) | distinct_lines(X2,X0) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p40])).
% 23.32/3.34 cnf(ssp48, plain, (spl10 | spl16), inference(avatar_split_clause, [status(thm)], [p1489, sdef10, sdef16])).
% 23.32/3.34 cnf(p449, plain, distinct_lines(X0,sk1) | distinct_lines(X0,X1) | distinct_lines(X1,sk0), inference(resolution, [status(thm)], [p40, c1])).
% 23.32/3.34 cnf(p1490, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | distinct_lines(X0,X1) | distinct_lines(X1,sk0), inference(resolution, [status(thm)], [p139, p449])).
% 23.32/3.34 fof(sdef39, definition, (spl39 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | distinct_lines(X1,sk0))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 23.32/3.34 cnf(ssp49, plain, (spl7 | spl9 | spl39), inference(avatar_split_clause, [status(thm)], [p1490, sdef7, sdef9, sdef39])).
% 23.32/3.34 cnf(p1492, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk1) | distinct_lines(X1,sk0), inference(resolution, [status(thm)], [p139, p449])).
% 23.32/3.34 cnf(ssp50, plain, (spl14 | spl17), inference(avatar_split_clause, [status(thm)], [p1492, sdef14, sdef17])).
% 23.32/3.34 cnf(p41, plain, distinct_lines(X0,sk1) | distinct_lines(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p38, c4])).
% 23.32/3.34 cnf(p1493, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p139, p41])).
% 23.32/3.34 fof(sdef40, definition, (spl40 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 23.32/3.34 cnf(ssp51, plain, (spl6 | spl8 | spl40), inference(avatar_split_clause, [status(thm)], [p1493, sdef6, sdef8, sdef40])).
% 23.32/3.34 cnf(p1495, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk1) | distinct_lines(sk0,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p41])).
% 23.32/3.34 cnf(ssp52, plain, (spl12 | spl14), inference(avatar_split_clause, [status(thm)], [p1495, sdef12, sdef14])).
% 23.32/3.34 cnf(p59, plain, distinct_lines(X0,sk0) | distinct_lines(sk1,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p44, c4])).
% 23.32/3.34 cnf(p1496, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p139, p59])).
% 23.32/3.34 fof(sdef41, definition, (spl41 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 23.32/3.34 cnf(ssp53, plain, (spl7 | spl9 | spl41), inference(avatar_split_clause, [status(thm)], [p1496, sdef7, sdef9, sdef41])).
% 23.32/3.34 cnf(p1498, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk0) | distinct_lines(sk1,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p59])).
% 23.32/3.34 cnf(ssp54, plain, (spl17 | spl19), inference(avatar_split_clause, [status(thm)], [p1498, sdef17, sdef19])).
% 23.32/3.34 cnf(p1499, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X2,sk0) | distinct_lines(sk1,X0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p59])).
% 23.32/3.34 cnf(ssp55, plain, (spl13 | spl18), inference(avatar_split_clause, [status(thm)], [p1499, sdef13, sdef18])).
% 23.32/3.34 cnf(p60, plain, distinct_lines(X0,sk0) | distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p44, c4])).
% 23.32/3.34 cnf(p1500, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk0) | distinct_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p139, p60])).
% 23.32/3.34 cnf(ssp56, plain, (spl11 | spl17), inference(avatar_split_clause, [status(thm)], [p1500, sdef11, sdef17])).
% 23.32/3.34 cnf(p1501, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p139, p60])).
% 23.32/3.34 fof(sdef42, definition, (spl42 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 23.32/3.34 cnf(ssp57, plain, (spl7 | spl9 | spl42), inference(avatar_split_clause, [status(thm)], [p1501, sdef7, sdef9, sdef42])).
% 23.32/3.34 cnf(p67, plain, convergent_lines(sk0,X0) | convergent_lines(X0,X1) | convergent_lines(sk1,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p46, c5])).
% 23.32/3.34 cnf(p482, plain, convergent_lines(sk0,X0) | convergent_lines(X0,X1) | convergent_lines(X1,sk1), inference(resolution, [status(thm)], [p67, c2])).
% 23.32/3.34 cnf(p495, plain, convergent_lines(X0,X1) | convergent_lines(X1,sk1) | distinct_lines(sk0,X0), inference(resolution, [status(thm)], [p482, c13])).
% 23.32/3.34 cnf(p506, plain, convergent_lines(X0,sk1) | distinct_lines(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p495, c13])).
% 23.32/3.34 cnf(p1503, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p139, p506])).
% 23.32/3.34 fof(sdef43, definition, (spl43 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 23.32/3.34 cnf(ssp58, plain, (spl6 | spl8 | spl43), inference(avatar_split_clause, [status(thm)], [p1503, sdef6, sdef8, sdef43])).
% 23.32/3.34 cnf(p86, plain, distinct_lines(sk1,X0) | convergent_lines(X0,X1) | convergent_lines(sk0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p47, c5])).
% 23.32/3.34 cnf(p547, plain, distinct_lines(sk1,X0) | convergent_lines(X0,X1) | convergent_lines(X1,sk0), inference(resolution, [status(thm)], [p86, c2])).
% 23.32/3.34 cnf(p559, plain, distinct_lines(sk1,X0) | convergent_lines(X1,sk0) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p547, c13])).
% 23.32/3.34 cnf(p1505, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk0) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p139, p559])).
% 23.32/3.34 fof(sdef44, definition, (spl44 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk0) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 23.32/3.34 cnf(ssp59, plain, (spl7 | spl9 | spl44), inference(avatar_split_clause, [status(thm)], [p1505, sdef7, sdef9, sdef44])).
% 23.32/3.34 cnf(p101, plain, distinct_lines(sk1,X0) | distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p61, c4])).
% 23.32/3.34 cnf(p1507, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p139, p101])).
% 23.32/3.34 fof(sdef45, definition, (spl45 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 23.32/3.34 cnf(ssp60, plain, (spl6 | spl8 | spl45), inference(avatar_split_clause, [status(thm)], [p1507, sdef6, sdef8, sdef45])).
% 23.32/3.34 cnf(p132, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p65, c4])).
% 23.32/3.34 cnf(p1509, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk0,X0) | convergent_lines(sk1,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p132])).
% 23.32/3.34 cnf(ssp61, plain, (spl20 | spl29), inference(avatar_split_clause, [status(thm)], [p1509, sdef20, sdef29])).
% 23.32/3.34 cnf(p1510, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk0,X2) | convergent_lines(sk1,X0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p132])).
% 23.32/3.34 cnf(ssp62, plain, (spl21 | spl24), inference(avatar_split_clause, [status(thm)], [p1510, sdef21, sdef24])).
% 23.32/3.34 cnf(p133, plain, convergent_lines(sk1,X0) | distinct_lines(X1,X0) | convergent_lines(sk0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p65, c5])).
% 23.32/3.34 cnf(p1511, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk1,X1) | convergent_lines(sk0,X2) | convergent_lines(X0,X2), inference(resolution, [status(thm)], [p139, p133])).
% 23.32/3.34 fof(sdef46, definition, (spl46 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | convergent_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 23.32/3.34 cnf(ssp63, plain, (spl21 | spl46), inference(avatar_split_clause, [status(thm)], [p1511, sdef21, sdef46])).
% 23.32/3.34 cnf(p134, plain, convergent_lines(sk0,X0) | distinct_lines(X0,X1) | convergent_lines(sk1,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p65, c5])).
% 23.32/3.34 cnf(p1513, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk0,X0) | convergent_lines(sk1,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p139, p134])).
% 23.32/3.34 fof(sdef47, definition, (spl47 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | convergent_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 23.32/3.34 cnf(ssp64, plain, (spl20 | spl47), inference(avatar_split_clause, [status(thm)], [p1513, sdef20, sdef47])).
% 23.32/3.34 cnf(p151, plain, convergent_lines(X0,sk1) | convergent_lines(X0,X1) | convergent_lines(sk0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p71, c5])).
% 23.32/3.34 cnf(p646, plain, convergent_lines(X0,sk1) | convergent_lines(X0,X1) | convergent_lines(X1,sk0), inference(resolution, [status(thm)], [p151, c2])).
% 23.32/3.34 cnf(p662, plain, convergent_lines(X0,sk1) | convergent_lines(X1,sk0) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p646, c13])).
% 23.32/3.34 cnf(p1515, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk1) | convergent_lines(X1,sk0), inference(resolution, [status(thm)], [p139, p662])).
% 23.32/3.34 cnf(ssp65, plain, (spl25 | spl27), inference(avatar_split_clause, [status(thm)], [p1515, sdef25, sdef27])).
% 23.32/3.34 cnf(p661, plain, convergent_lines(X0,X1) | convergent_lines(X1,sk0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p646, c13])).
% 23.32/3.34 cnf(p672, plain, convergent_lines(X0,sk0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p661, c13])).
% 23.32/3.34 cnf(p1516, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X1,sk0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p139, p672])).
% 23.32/3.34 cnf(ssp66, plain, (spl14 | spl27), inference(avatar_split_clause, [status(thm)], [p1516, sdef14, sdef27])).
% 23.32/3.34 cnf(p679, plain, convergent_lines(X0,sk1) | distinct_lines(X0,X1) | distinct_lines(X1,sk0), inference(resolution, [status(thm)], [p662, c13])).
% 23.32/3.34 cnf(p1517, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk1) | distinct_lines(X1,sk0), inference(resolution, [status(thm)], [p139, p679])).
% 23.32/3.34 cnf(ssp67, plain, (spl17 | spl25), inference(avatar_split_clause, [status(thm)], [p1517, sdef17, sdef25])).
% 23.32/3.34 cnf(p179, plain, convergent_lines(sk0,X0) | distinct_lines(X1,X0) | distinct_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p85, c4])).
% 23.32/3.34 cnf(p1518, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk0,X1) | distinct_lines(sk1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p139, p179])).
% 23.32/3.34 cnf(ssp68, plain, (spl11 | spl20), inference(avatar_split_clause, [status(thm)], [p1518, sdef11, sdef20])).
% 23.32/3.34 cnf(p1519, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X2,X1) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p139, p179])).
% 23.32/3.34 fof(sdef48, definition, (spl48 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X2,X1) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 23.32/3.34 cnf(ssp69, plain, (spl7 | spl9 | spl48), inference(avatar_split_clause, [status(thm)], [p1519, sdef7, sdef9, sdef48])).
% 23.32/3.34 cnf(p1521, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk0,X2) | distinct_lines(X0,X2) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p139, p179])).
% 23.32/3.34 cnf(ssp70, plain, (spl13 | spl22), inference(avatar_split_clause, [status(thm)], [p1521, sdef13, sdef22])).
% 23.32/3.34 cnf(p180, plain, distinct_lines(sk1,X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p85, c4])).
% 23.32/3.34 cnf(p1522, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p139, p180])).
% 23.32/3.34 fof(sdef49, definition, (spl49 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 23.32/3.34 cnf(ssp71, plain, (spl7 | spl9 | spl49), inference(avatar_split_clause, [status(thm)], [p1522, sdef7, sdef9, sdef49])).
% 23.32/3.34 cnf(p1524, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk1,X0) | convergent_lines(sk0,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p180])).
% 23.32/3.34 cnf(ssp72, plain, (spl13 | spl24), inference(avatar_split_clause, [status(thm)], [p1524, sdef13, sdef24])).
% 23.32/3.34 cnf(p1525, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk1,X2) | convergent_lines(sk0,X0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p180])).
% 23.32/3.34 cnf(ssp73, plain, (spl19 | spl20), inference(avatar_split_clause, [status(thm)], [p1525, sdef19, sdef20])).
% 23.32/3.34 cnf(p181, plain, distinct_lines(sk1,X0) | distinct_lines(X0,X1) | convergent_lines(sk0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p85, c5])).
% 23.32/3.34 cnf(p1526, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | convergent_lines(sk0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p139, p181])).
% 23.32/3.34 fof(sdef50, definition, (spl50 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | convergent_lines(sk0,X2) | convergent_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 23.32/3.34 cnf(ssp74, plain, (spl7 | spl9 | spl50), inference(avatar_split_clause, [status(thm)], [p1526, sdef7, sdef9, sdef50])).
% 23.32/3.34 cnf(p1528, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk1,X0) | convergent_lines(sk0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p139, p181])).
% 23.32/3.34 cnf(ssp75, plain, (spl13 | spl46), inference(avatar_split_clause, [status(thm)], [p1528, sdef13, sdef46])).
% 23.32/3.34 cnf(p186, plain, convergent_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p104, c4])).
% 23.32/3.34 cnf(p1529, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk1,X1) | distinct_lines(sk0,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p139, p186])).
% 23.32/3.34 cnf(ssp76, plain, (spl15 | spl21), inference(avatar_split_clause, [status(thm)], [p1529, sdef15, sdef21])).
% 23.32/3.34 cnf(p1530, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X2,X1) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p139, p186])).
% 23.32/3.34 fof(sdef51, definition, (spl51 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X2,X1) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 23.32/3.34 cnf(ssp77, plain, (spl6 | spl8 | spl51), inference(avatar_split_clause, [status(thm)], [p1530, sdef6, sdef8, sdef51])).
% 23.32/3.34 cnf(p1532, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk1,X2) | distinct_lines(X0,X2) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p186])).
% 23.32/3.34 cnf(ssp78, plain, (spl10 | spl23), inference(avatar_split_clause, [status(thm)], [p1532, sdef10, sdef23])).
% 23.32/3.34 cnf(p187, plain, convergent_lines(sk1,X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p104, c4])).
% 23.32/3.34 cnf(p1533, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p139, p187])).
% 23.32/3.34 fof(sdef52, definition, (spl52 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 23.32/3.34 cnf(ssp79, plain, (spl6 | spl8 | spl52), inference(avatar_split_clause, [status(thm)], [p1533, sdef6, sdef8, sdef52])).
% 23.32/3.34 cnf(p1535, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk1,X2) | distinct_lines(sk0,X0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p187])).
% 23.32/3.34 cnf(ssp80, plain, (spl10 | spl29), inference(avatar_split_clause, [status(thm)], [p1535, sdef10, sdef29])).
% 23.32/3.34 cnf(p1536, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk1,X0) | distinct_lines(sk0,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p187])).
% 23.32/3.34 cnf(ssp81, plain, (spl12 | spl21), inference(avatar_split_clause, [status(thm)], [p1536, sdef12, sdef21])).
% 23.32/3.34 cnf(p188, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | convergent_lines(sk1,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p104, c5])).
% 23.32/3.34 cnf(p1537, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | convergent_lines(sk1,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p139, p188])).
% 23.32/3.34 fof(sdef53, definition, (spl53 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | convergent_lines(sk1,X2) | convergent_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 23.32/3.34 cnf(ssp82, plain, (spl6 | spl8 | spl53), inference(avatar_split_clause, [status(thm)], [p1537, sdef6, sdef8, sdef53])).
% 23.32/3.34 cnf(p1539, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk0,X0) | convergent_lines(sk1,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p139, p188])).
% 23.32/3.34 cnf(ssp83, plain, (spl10 | spl47), inference(avatar_split_clause, [status(thm)], [p1539, sdef10, sdef47])).
% 23.32/3.34 cnf(p191, plain, convergent_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p126, c4])).
% 23.32/3.34 cnf(p1540, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p139, p191])).
% 23.32/3.34 fof(sdef54, definition, (spl54 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 23.32/3.34 cnf(ssp84, plain, (spl7 | spl9 | spl54), inference(avatar_split_clause, [status(thm)], [p1540, sdef7, sdef9, sdef54])).
% 23.32/3.34 cnf(p192, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X0) | convergent_lines(sk0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p126, c5])).
% 23.32/3.34 cnf(p1542, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,X0) | convergent_lines(sk0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p139, p192])).
% 23.32/3.34 fof(sdef55, definition, (spl55 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,X0) | convergent_lines(sk0,X2) | convergent_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 23.32/3.34 cnf(ssp85, plain, (spl7 | spl9 | spl55), inference(avatar_split_clause, [status(thm)], [p1542, sdef7, sdef9, sdef55])).
% 23.32/3.34 cnf(p217, plain, convergent_lines(X0,sk1) | convergent_lines(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p150, c4])).
% 23.32/3.34 cnf(p1544, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk1) | convergent_lines(sk0,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p217])).
% 23.32/3.34 cnf(ssp86, plain, (spl24 | spl25), inference(avatar_split_clause, [status(thm)], [p1544, sdef24, sdef25])).
% 23.32/3.34 cnf(p1545, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X2,sk1) | convergent_lines(sk0,X0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p217])).
% 23.32/3.34 cnf(ssp87, plain, (spl20 | spl26), inference(avatar_split_clause, [status(thm)], [p1545, sdef20, sdef26])).
% 23.32/3.34 cnf(p219, plain, convergent_lines(X0,sk1) | distinct_lines(X0,X1) | convergent_lines(sk0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p150, c5])).
% 23.32/3.34 cnf(p1546, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk1) | convergent_lines(sk0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p139, p219])).
% 23.32/3.34 cnf(ssp88, plain, (spl25 | spl46), inference(avatar_split_clause, [status(thm)], [p1546, sdef25, sdef46])).
% 23.32/3.34 cnf(p298, plain, distinct_lines(X0,sk1) | convergent_lines(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p169, c4])).
% 23.32/3.34 cnf(p1547, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk1) | convergent_lines(sk0,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p298])).
% 23.32/3.34 cnf(ssp89, plain, (spl14 | spl24), inference(avatar_split_clause, [status(thm)], [p1547, sdef14, sdef24])).
% 23.32/3.34 cnf(p1548, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X2,sk1) | convergent_lines(sk0,X0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p298])).
% 23.32/3.34 cnf(ssp90, plain, (spl16 | spl20), inference(avatar_split_clause, [status(thm)], [p1548, sdef16, sdef20])).
% 23.32/3.34 cnf(p299, plain, distinct_lines(X0,sk1) | distinct_lines(X0,X1) | convergent_lines(sk0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p169, c5])).
% 23.32/3.34 cnf(p1549, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk1) | convergent_lines(sk0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p139, p299])).
% 23.32/3.34 cnf(ssp91, plain, (spl14 | spl46), inference(avatar_split_clause, [status(thm)], [p1549, sdef14, sdef46])).
% 23.32/3.34 cnf(p302, plain, convergent_lines(X0,sk1) | distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p209, c4])).
% 23.32/3.34 cnf(p1550, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk1) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p139, p302])).
% 23.32/3.34 cnf(ssp92, plain, (spl15 | spl25), inference(avatar_split_clause, [status(thm)], [p1550, sdef15, sdef25])).
% 23.32/3.34 cnf(p1551, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk1) | distinct_lines(X1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p139, p302])).
% 23.32/3.34 fof(sdef56, definition, (spl56 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk1) | distinct_lines(X1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 23.32/3.34 cnf(ssp93, plain, (spl6 | spl8 | spl56), inference(avatar_split_clause, [status(thm)], [p1551, sdef6, sdef8, sdef56])).
% 23.32/3.34 cnf(p1553, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X2,sk1) | distinct_lines(X2,X0) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p302])).
% 23.32/3.34 cnf(ssp94, plain, (spl10 | spl26), inference(avatar_split_clause, [status(thm)], [p1553, sdef10, sdef26])).
% 23.32/3.34 cnf(p303, plain, convergent_lines(X0,sk1) | distinct_lines(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p209, c4])).
% 23.32/3.34 cnf(p1554, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk1) | distinct_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p139, p303])).
% 23.32/3.34 fof(sdef57, definition, (spl57 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk1) | distinct_lines(X1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 23.32/3.34 cnf(ssp95, plain, (spl6 | spl8 | spl57), inference(avatar_split_clause, [status(thm)], [p1554, sdef6, sdef8, sdef57])).
% 23.32/3.34 cnf(p1556, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk1) | distinct_lines(sk0,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p303])).
% 23.32/3.34 cnf(ssp96, plain, (spl12 | spl25), inference(avatar_split_clause, [status(thm)], [p1556, sdef12, sdef25])).
% 23.32/3.34 cnf(p304, plain, distinct_lines(sk0,X0) | distinct_lines(X1,X0) | convergent_lines(X1,X2) | convergent_lines(sk1,X2), inference(resolution, [status(thm)], [p209, c5])).
% 23.32/3.34 cnf(p1557, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,X0) | convergent_lines(X1,X2) | convergent_lines(sk1,X2), inference(resolution, [status(thm)], [p139, p304])).
% 23.32/3.34 fof(sdef58, definition, (spl58 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,X0) | convergent_lines(X1,X2) | convergent_lines(sk1,X2))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 23.32/3.34 cnf(ssp97, plain, (spl6 | spl8 | spl58), inference(avatar_split_clause, [status(thm)], [p1557, sdef6, sdef8, sdef58])).
% 23.32/3.34 cnf(p326, plain, convergent_lines(X0,sk0) | convergent_lines(sk1,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p228, c4])).
% 23.32/3.34 cnf(p1559, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk0) | convergent_lines(sk1,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p326])).
% 23.32/3.34 cnf(ssp98, plain, (spl27 | spl29), inference(avatar_split_clause, [status(thm)], [p1559, sdef27, sdef29])).
% 23.32/3.34 cnf(p1560, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X2,sk0) | convergent_lines(sk1,X0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p326])).
% 23.32/3.34 cnf(ssp99, plain, (spl21 | spl28), inference(avatar_split_clause, [status(thm)], [p1560, sdef21, sdef28])).
% 23.32/3.34 cnf(p327, plain, convergent_lines(X0,sk0) | distinct_lines(X0,X1) | convergent_lines(sk1,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p228, c5])).
% 23.32/3.34 cnf(p1561, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk0) | convergent_lines(sk1,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p139, p327])).
% 23.32/3.34 cnf(ssp100, plain, (spl27 | spl47), inference(avatar_split_clause, [status(thm)], [p1561, sdef27, sdef47])).
% 23.32/3.34 cnf(p367, plain, distinct_lines(X0,sk0) | convergent_lines(sk1,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p307, c4])).
% 23.32/3.34 cnf(p1562, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk0) | convergent_lines(sk1,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p367])).
% 23.32/3.34 cnf(ssp101, plain, (spl17 | spl29), inference(avatar_split_clause, [status(thm)], [p1562, sdef17, sdef29])).
% 23.32/3.34 cnf(p1563, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X2,sk0) | convergent_lines(sk1,X0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p367])).
% 23.32/3.34 cnf(ssp102, plain, (spl18 | spl21), inference(avatar_split_clause, [status(thm)], [p1563, sdef18, sdef21])).
% 23.32/3.34 cnf(p368, plain, distinct_lines(X0,sk0) | distinct_lines(X0,X1) | convergent_lines(sk1,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p307, c5])).
% 23.32/3.34 cnf(p1564, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk0) | convergent_lines(sk1,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p139, p368])).
% 23.32/3.34 cnf(ssp103, plain, (spl17 | spl47), inference(avatar_split_clause, [status(thm)], [p1564, sdef17, sdef47])).
% 23.32/3.34 cnf(p374, plain, convergent_lines(X0,sk0) | distinct_lines(sk1,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p325, c4])).
% 23.32/3.34 cnf(p1565, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk0) | distinct_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p139, p374])).
% 23.32/3.34 fof(sdef59, definition, (spl59 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk0) | distinct_lines(X1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 23.32/3.34 cnf(ssp104, plain, (spl7 | spl9 | spl59), inference(avatar_split_clause, [status(thm)], [p1565, sdef7, sdef9, sdef59])).
% 23.32/3.34 cnf(p1567, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk0) | distinct_lines(sk1,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p374])).
% 23.32/3.34 cnf(ssp105, plain, (spl19 | spl27), inference(avatar_split_clause, [status(thm)], [p1567, sdef19, sdef27])).
% 23.32/3.34 cnf(p1568, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X2,sk0) | distinct_lines(sk1,X0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p374])).
% 23.32/3.34 cnf(ssp106, plain, (spl13 | spl28), inference(avatar_split_clause, [status(thm)], [p1568, sdef13, sdef28])).
% 23.32/3.34 cnf(p375, plain, convergent_lines(X0,sk0) | distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p325, c4])).
% 23.32/3.34 cnf(p1569, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk0) | distinct_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p139, p375])).
% 23.32/3.34 cnf(ssp107, plain, (spl11 | spl27), inference(avatar_split_clause, [status(thm)], [p1569, sdef11, sdef27])).
% 23.32/3.34 cnf(p1570, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk0) | distinct_lines(X1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p139, p375])).
% 23.32/3.34 fof(sdef60, definition, (spl60 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk0) | distinct_lines(X1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 23.32/3.34 cnf(ssp108, plain, (spl7 | spl9 | spl60), inference(avatar_split_clause, [status(thm)], [p1570, sdef7, sdef9, sdef60])).
% 23.32/3.34 cnf(p405, plain, convergent_lines(sk1,X0) | distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p378, c4])).
% 23.32/3.34 cnf(p1572, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p139, p405])).
% 23.32/3.34 fof(sdef61, definition, (spl61 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 23.32/3.34 cnf(ssp109, plain, (spl6 | spl8 | spl61), inference(avatar_split_clause, [status(thm)], [p1572, sdef6, sdef8, sdef61])).
% 23.32/3.34 cnf(p447, plain, distinct_lines(X0,X1) | distinct_lines(X1,sk1) | distinct_lines(sk0,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p444, c4])).
% 23.32/3.34 cnf(p1574, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,X2) | distinct_lines(X2,sk1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p139, p447])).
% 23.32/3.34 fof(sdef62, definition, (spl62 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,X2) | distinct_lines(X2,sk1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 23.32/3.34 cnf(ssp110, plain, (spl6 | spl8 | spl62), inference(avatar_split_clause, [status(thm)], [p1574, sdef6, sdef8, sdef62])).
% 23.32/3.34 cnf(p1576, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,X2) | distinct_lines(X2,sk1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p447])).
% 23.32/3.34 cnf(ssp111, plain, (spl10 | spl34), inference(avatar_split_clause, [status(thm)], [p1576, sdef10, sdef34])).
% 23.32/3.34 cnf(p453, plain, distinct_lines(X0,X1) | distinct_lines(X1,sk0) | distinct_lines(X0,X2) | distinct_lines(sk1,X2), inference(resolution, [status(thm)], [p449, c4])).
% 23.32/3.34 cnf(p1577, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,X2) | distinct_lines(X2,sk0) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p139, p453])).
% 23.32/3.34 cnf(ssp112, plain, (spl13 | spl39), inference(avatar_split_clause, [status(thm)], [p1577, sdef13, sdef39])).
% 23.32/3.34 cnf(p1578, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,X2) | distinct_lines(X2,sk0) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p139, p453])).
% 23.32/3.34 fof(sdef63, definition, (spl63 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,X2) | distinct_lines(X2,sk0) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 23.32/3.34 cnf(ssp113, plain, (spl7 | spl9 | spl63), inference(avatar_split_clause, [status(thm)], [p1578, sdef7, sdef9, sdef63])).
% 23.32/3.34 cnf(p454, plain, distinct_lines(X0,sk1) | distinct_lines(X1,sk0) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p449, c4])).
% 23.32/3.34 cnf(p1580, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk1) | distinct_lines(X2,sk0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p454])).
% 23.32/3.34 cnf(ssp114, plain, (spl14 | spl18), inference(avatar_split_clause, [status(thm)], [p1580, sdef14, sdef18])).
% 23.32/3.34 cnf(p1581, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X2,sk1) | distinct_lines(X0,sk0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p454])).
% 23.32/3.34 cnf(ssp115, plain, (spl16 | spl17), inference(avatar_split_clause, [status(thm)], [p1581, sdef16, sdef17])).
% 23.32/3.34 cnf(p484, plain, convergent_lines(sk0,X0) | convergent_lines(X0,X1) | convergent_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p67, c13])).
% 23.32/3.34 cnf(p1582, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk0,X2) | convergent_lines(X2,X0) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p139, p484])).
% 23.32/3.34 fof(sdef64, definition, (spl64 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | convergent_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 23.32/3.34 cnf(ssp116, plain, (spl21 | spl64), inference(avatar_split_clause, [status(thm)], [p1582, sdef21, sdef64])).
% 23.32/3.34 cnf(p523, plain, convergent_lines(X0,sk1) | distinct_lines(X1,X0) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p506, c4])).
% 23.32/3.34 cnf(p1584, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk1) | distinct_lines(X2,X1) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p139, p523])).
% 23.32/3.34 fof(sdef65, definition, (spl65 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk1) | distinct_lines(X2,X1) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 23.32/3.34 cnf(ssp117, plain, (spl6 | spl8 | spl65), inference(avatar_split_clause, [status(thm)], [p1584, sdef6, sdef8, sdef65])).
% 23.32/3.34 cnf(p1586, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X2,sk1) | distinct_lines(X0,X2) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p523])).
% 23.32/3.34 cnf(ssp118, plain, (spl10 | spl43), inference(avatar_split_clause, [status(thm)], [p1586, sdef10, sdef43])).
% 23.32/3.34 cnf(p68, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X1) | convergent_lines(X0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p46, c5])).
% 23.32/3.34 cnf(p531, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X1) | convergent_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p68, c13])).
% 23.32/3.34 cnf(p1587, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk0,X0) | convergent_lines(sk1,X2) | convergent_lines(X2,X1), inference(resolution, [status(thm)], [p139, p531])).
% 23.32/3.34 fof(sdef66, definition, (spl66 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | convergent_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 23.32/3.34 cnf(ssp119, plain, (spl20 | spl66), inference(avatar_split_clause, [status(thm)], [p1587, sdef20, sdef66])).
% 23.32/3.34 cnf(p549, plain, distinct_lines(sk1,X0) | convergent_lines(X0,X1) | convergent_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p86, c13])).
% 23.32/3.34 cnf(p1589, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk1,X2) | convergent_lines(X2,X0) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p549])).
% 23.32/3.34 fof(sdef67, definition, (spl67 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | convergent_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 23.32/3.34 cnf(ssp120, plain, (spl20 | spl67), inference(avatar_split_clause, [status(thm)], [p1589, sdef20, sdef67])).
% 23.32/3.34 cnf(p569, plain, convergent_lines(X0,sk0) | distinct_lines(X1,X0) | distinct_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p559, c4])).
% 23.32/3.34 cnf(p1591, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk0) | distinct_lines(X2,X1) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p139, p569])).
% 23.32/3.34 fof(sdef68, definition, (spl68 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk0) | distinct_lines(X2,X1) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 23.32/3.34 cnf(ssp121, plain, (spl7 | spl9 | spl68), inference(avatar_split_clause, [status(thm)], [p1591, sdef7, sdef9, sdef68])).
% 23.32/3.34 cnf(p1593, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X2,sk0) | distinct_lines(X0,X2) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p139, p569])).
% 23.32/3.34 cnf(ssp122, plain, (spl13 | spl44), inference(avatar_split_clause, [status(thm)], [p1593, sdef13, sdef44])).
% 23.32/3.34 cnf(p87, plain, distinct_lines(sk1,X0) | convergent_lines(sk0,X1) | convergent_lines(X0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p47, c5])).
% 23.32/3.34 cnf(p574, plain, distinct_lines(sk1,X0) | convergent_lines(sk0,X1) | convergent_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p87, c13])).
% 23.32/3.34 cnf(p1594, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | convergent_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p139, p574])).
% 23.32/3.34 fof(sdef69, definition, (spl69 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | convergent_lines(X1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 23.32/3.34 cnf(ssp123, plain, (spl7 | spl9 | spl69), inference(avatar_split_clause, [status(thm)], [p1594, sdef7, sdef9, sdef69])).
% 23.32/3.34 cnf(p1596, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk1,X0) | convergent_lines(sk0,X2) | convergent_lines(X2,X1), inference(resolution, [status(thm)], [p139, p574])).
% 23.32/3.34 cnf(ssp124, plain, (spl13 | spl64), inference(avatar_split_clause, [status(thm)], [p1596, sdef13, sdef64])).
% 23.32/3.34 cnf(p105, plain, convergent_lines(X0,X1) | distinct_lines(sk0,X0) | convergent_lines(sk1,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p63, c5])).
% 23.32/3.34 cnf(p586, plain, convergent_lines(X0,X1) | distinct_lines(sk0,X0) | convergent_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p105, c13])).
% 23.32/3.34 cnf(p1597, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X2,X0) | distinct_lines(sk0,X2) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p139, p586])).
% 23.32/3.34 fof(sdef70, definition, (spl70 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,X0) | distinct_lines(sk0,X1))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 23.32/3.34 cnf(ssp125, plain, (spl21 | spl70), inference(avatar_split_clause, [status(thm)], [p1597, sdef21, sdef70])).
% 23.32/3.34 cnf(p106, plain, convergent_lines(sk1,X0) | distinct_lines(sk0,X1) | convergent_lines(X1,X2) | convergent_lines(X0,X2), inference(resolution, [status(thm)], [p63, c5])).
% 23.32/3.34 cnf(p596, plain, convergent_lines(sk1,X0) | distinct_lines(sk0,X1) | convergent_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p106, c13])).
% 23.32/3.34 cnf(p1599, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | convergent_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p139, p596])).
% 23.32/3.34 fof(sdef71, definition, (spl71 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | convergent_lines(X1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 23.32/3.34 cnf(ssp126, plain, (spl6 | spl8 | spl71), inference(avatar_split_clause, [status(thm)], [p1599, sdef6, sdef8, sdef71])).
% 23.32/3.34 cnf(p1601, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk1,X2) | distinct_lines(sk0,X0) | convergent_lines(X2,X1), inference(resolution, [status(thm)], [p139, p596])).
% 23.32/3.34 cnf(ssp127, plain, (spl10 | spl66), inference(avatar_split_clause, [status(thm)], [p1601, sdef10, sdef66])).
% 23.32/3.34 cnf(p127, plain, convergent_lines(X0,X1) | distinct_lines(sk1,X1) | convergent_lines(sk0,X2) | convergent_lines(X0,X2), inference(resolution, [status(thm)], [p64, c5])).
% 23.32/3.34 cnf(p606, plain, convergent_lines(X0,X1) | distinct_lines(sk1,X1) | convergent_lines(sk0,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p127, c13])).
% 23.32/3.34 cnf(p1602, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,X2) | distinct_lines(sk1,X2) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p606])).
% 23.32/3.34 fof(sdef72, definition, (spl72 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X0,X1) | distinct_lines(sk1,X1))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 23.32/3.34 cnf(ssp128, plain, (spl20 | spl72), inference(avatar_split_clause, [status(thm)], [p1602, sdef20, sdef72])).
% 23.32/3.34 cnf(p625, plain, convergent_lines(sk1,X0) | distinct_lines(X1,X0) | convergent_lines(X1,X2) | distinct_lines(sk0,X2), inference(resolution, [status(thm)], [p133, c13])).
% 23.32/3.34 cnf(p1604, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk1,X1) | convergent_lines(X0,X2) | distinct_lines(sk0,X2), inference(resolution, [status(thm)], [p139, p625])).
% 23.32/3.34 fof(sdef73, definition, (spl73 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X0,X1) | distinct_lines(sk0,X1))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 23.32/3.34 cnf(ssp129, plain, (spl21 | spl73), inference(avatar_split_clause, [status(thm)], [p1604, sdef21, sdef73])).
% 23.32/3.34 cnf(p626, plain, convergent_lines(sk1,X0) | distinct_lines(X1,X0) | convergent_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p133, c13])).
% 23.32/3.34 cnf(p1606, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk1,X1) | convergent_lines(sk0,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p139, p626])).
% 23.32/3.34 cnf(ssp130, plain, (spl21 | spl22), inference(avatar_split_clause, [status(thm)], [p1606, sdef21, sdef22])).
% 23.32/3.34 cnf(p1607, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk1,X2) | distinct_lines(X0,X2) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p626])).
% 23.32/3.34 cnf(ssp131, plain, (spl20 | spl23), inference(avatar_split_clause, [status(thm)], [p1607, sdef20, sdef23])).
% 23.32/3.34 cnf(p648, plain, convergent_lines(X0,sk1) | convergent_lines(X0,X1) | convergent_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p151, c13])).
% 23.32/3.34 cnf(p1608, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X2,sk1) | convergent_lines(X2,X0) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p648])).
% 23.32/3.34 fof(sdef74, definition, (spl74 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X1,sk1) | convergent_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl74])], [avatar_definition])).
% 23.32/3.34 cnf(ssp132, plain, (spl20 | spl74), inference(avatar_split_clause, [status(thm)], [p1608, sdef20, sdef74])).
% 23.32/3.34 cnf(p680, plain, convergent_lines(X0,sk1) | convergent_lines(X1,sk0) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p662, c4])).
% 23.32/3.34 cnf(p1610, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk1) | convergent_lines(X2,sk0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p680])).
% 23.32/3.34 cnf(ssp133, plain, (spl25 | spl28), inference(avatar_split_clause, [status(thm)], [p1610, sdef25, sdef28])).
% 23.32/3.34 cnf(p1611, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X2,sk1) | convergent_lines(X0,sk0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p680])).
% 23.32/3.34 cnf(ssp134, plain, (spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p1611, sdef26, sdef27])).
% 23.32/3.34 cnf(p693, plain, convergent_lines(X0,sk0) | distinct_lines(X1,sk1) | distinct_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p672, c4])).
% 23.32/3.34 cnf(p1612, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X2,sk0) | distinct_lines(X0,sk1) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p693])).
% 23.32/3.34 cnf(ssp135, plain, (spl14 | spl28), inference(avatar_split_clause, [status(thm)], [p1612, sdef14, sdef28])).
% 23.32/3.34 cnf(p1613, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk0) | distinct_lines(X2,sk1) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p693])).
% 23.32/3.34 cnf(ssp136, plain, (spl16 | spl27), inference(avatar_split_clause, [status(thm)], [p1613, sdef16, sdef27])).
% 23.32/3.34 cnf(p699, plain, convergent_lines(X0,sk1) | distinct_lines(X1,sk0) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p679, c4])).
% 23.32/3.34 cnf(p1614, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk1) | distinct_lines(X2,sk0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p699])).
% 23.32/3.34 cnf(ssp137, plain, (spl18 | spl25), inference(avatar_split_clause, [status(thm)], [p1614, sdef18, sdef25])).
% 23.32/3.34 cnf(p1615, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X2,sk1) | distinct_lines(X0,sk0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p139, p699])).
% 23.32/3.34 cnf(ssp138, plain, (spl17 | spl26), inference(avatar_split_clause, [status(thm)], [p1615, sdef17, sdef26])).
% 23.32/3.34 cnf(p152, plain, convergent_lines(X0,sk1) | convergent_lines(sk0,X1) | convergent_lines(X0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p71, c5])).
% 23.32/3.34 cnf(p703, plain, convergent_lines(X0,sk1) | convergent_lines(sk0,X1) | convergent_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p152, c13])).
% 23.32/3.34 cnf(p1616, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk1) | convergent_lines(sk0,X2) | convergent_lines(X2,X1), inference(resolution, [status(thm)], [p139, p703])).
% 23.32/3.34 cnf(ssp139, plain, (spl25 | spl64), inference(avatar_split_clause, [status(thm)], [p1616, sdef25, sdef64])).
% 23.32/3.34 cnf(p170, plain, distinct_lines(X0,sk1) | convergent_lines(X0,X1) | convergent_lines(sk0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p82, c5])).
% 23.32/3.34 cnf(p715, plain, distinct_lines(X0,sk1) | convergent_lines(X0,X1) | convergent_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p170, c13])).
% 23.32/3.34 cnf(p1617, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X2,sk1) | convergent_lines(X2,X0) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p139, p715])).
% 23.32/3.34 fof(sdef75, definition, (spl75 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk1) | convergent_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl75])], [avatar_definition])).
% 23.32/3.34 cnf(ssp140, plain, (spl20 | spl75), inference(avatar_split_clause, [status(thm)], [p1617, sdef20, sdef75])).
% 23.32/3.34 cnf(p171, plain, distinct_lines(X0,sk1) | convergent_lines(sk0,X1) | convergent_lines(X0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p82, c5])).
% 23.32/3.34 cnf(p725, plain, distinct_lines(X0,sk1) | convergent_lines(sk0,X1) | convergent_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p171, c13])).
% 23.32/3.34 cnf(p1619, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk1) | convergent_lines(sk0,X2) | convergent_lines(X2,X1), inference(resolution, [status(thm)], [p139, p725])).
% 23.32/3.34 cnf(ssp141, plain, (spl14 | spl64), inference(avatar_split_clause, [status(thm)], [p1619, sdef14, sdef64])).
% 23.32/3.34 cnf(p84, plain, distinct_lines(sk1,X0) | convergent_lines(X0,X1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p47, c13])).
% 23.32/3.34 cnf(p176, plain, distinct_lines(sk1,X0) | distinct_lines(sk0,X1) | convergent_lines(X0,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p84, c5])).
% 23.32/3.34 cnf(p734, plain, distinct_lines(sk1,X0) | distinct_lines(sk0,X1) | convergent_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p176, c13])).
% 23.32/3.34 cnf(p1620, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X1) | convergent_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p139, p734])).
% 23.32/3.34 fof(sdef76, definition, (spl76 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X1) | convergent_lines(X1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl76])], [avatar_definition])).
% 23.32/3.34 cnf(ssp142, plain, (spl7 | spl9 | spl76), inference(avatar_split_clause, [status(thm)], [p1620, sdef7, sdef9, sdef76])).
% 23.32/3.34 cnf(p1622, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk1,X0) | distinct_lines(sk0,X2) | convergent_lines(X2,X1), inference(resolution, [status(thm)], [p139, p734])).
% 23.32/3.34 cnf(ssp143, plain, (spl13 | spl70), inference(avatar_split_clause, [status(thm)], [p1622, sdef13, sdef70])).
% 23.32/3.34 cnf(p735, plain, distinct_lines(sk1,X0) | distinct_lines(sk0,X1) | convergent_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p176, c13])).
% 23.32/3.34 cnf(p1623, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | convergent_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p139, p735])).
% 23.32/3.34 fof(sdef77, definition, (spl77 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | convergent_lines(X1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl77])], [avatar_definition])).
% 23.32/3.34 cnf(ssp144, plain, (spl6 | spl8 | spl77), inference(avatar_split_clause, [status(thm)], [p1623, sdef6, sdef8, sdef77])).
% 23.32/3.34 cnf(p1625, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk1,X2) | distinct_lines(sk0,X0) | convergent_lines(X2,X1), inference(resolution, [status(thm)], [p139, p735])).
% 23.32/3.34 cnf(ssp145, plain, (spl10 | spl67), inference(avatar_split_clause, [status(thm)], [p1625, sdef10, sdef67])).
% 23.32/3.34 cnf(p754, plain, distinct_lines(sk1,X0) | distinct_lines(X0,X1) | convergent_lines(X1,X2) | distinct_lines(sk0,X2), inference(resolution, [status(thm)], [p181, c13])).
% 23.32/3.34 cnf(p1626, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | convergent_lines(X1,X2) | distinct_lines(sk0,X2), inference(resolution, [status(thm)], [p139, p754])).
% 23.32/3.34 fof(sdef78, definition, (spl78 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | convergent_lines(X1,X2) | distinct_lines(sk0,X2))), introduced(definition, [new_symbols(naming, [spl78])], [avatar_definition])).
% 23.32/3.34 cnf(ssp146, plain, (spl7 | spl9 | spl78), inference(avatar_split_clause, [status(thm)], [p1626, sdef7, sdef9, sdef78])).
% 23.32/3.34 cnf(p1628, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk1,X0) | convergent_lines(X1,X2) | distinct_lines(sk0,X2), inference(resolution, [status(thm)], [p139, p754])).
% 23.32/3.34 cnf(ssp147, plain, (spl13 | spl73), inference(avatar_split_clause, [status(thm)], [p1628, sdef13, sdef73])).
% 23.32/3.34 cnf(p755, plain, distinct_lines(sk1,X0) | distinct_lines(X0,X1) | convergent_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p181, c13])).
% 23.32/3.34 cnf(p1629, plain, apart_point_and_line(sk2,sk1) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | convergent_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p139, p755])).
% 23.32/3.34 fof(sdef79, definition, (spl79 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | convergent_lines(sk0,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl79])], [avatar_definition])).
% 23.32/3.34 cnf(ssp148, plain, (spl7 | spl9 | spl79), inference(avatar_split_clause, [status(thm)], [p1629, sdef7, sdef9, sdef79])).
% 23.32/3.34 cnf(p776, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | convergent_lines(X1,X2) | distinct_lines(sk1,X2), inference(resolution, [status(thm)], [p188, c13])).
% 23.32/3.34 cnf(p1631, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | convergent_lines(X1,X2) | distinct_lines(sk1,X2), inference(resolution, [status(thm)], [p139, p776])).
% 23.32/3.34 fof(sdef80, definition, (spl80 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | convergent_lines(X1,X2) | distinct_lines(sk1,X2))), introduced(definition, [new_symbols(naming, [spl80])], [avatar_definition])).
% 23.32/3.34 cnf(ssp149, plain, (spl6 | spl8 | spl80), inference(avatar_split_clause, [status(thm)], [p1631, sdef6, sdef8, sdef80])).
% 23.32/3.34 cnf(p1633, plain, apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk0,X0) | convergent_lines(X1,X2) | distinct_lines(sk1,X2), inference(resolution, [status(thm)], [p139, p776])).
% 23.32/3.34 cnf(ssp150, plain, (spl10 | spl72), inference(avatar_split_clause, [status(thm)], [p1633, sdef10, sdef72])).
% 23.32/3.34 cnf(p777, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | convergent_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p188, c13])).
% 23.32/3.34 cnf(p1634, plain, apart_point_and_line(sk2,sk0) | apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | convergent_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p139, p777])).
% 23.32/3.34 fof(sdef81, definition, (spl81 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,X1) | convergent_lines(sk1,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl81])], [avatar_definition])).
% 23.32/3.34 cnf(ssp151, plain, (spl6 | spl8 | spl81), inference(avatar_split_clause, [status(thm)], [p1634, sdef6, sdef8, sdef81])).
% 23.32/3.34 cnf(p93, plain, ~apart_point_and_line(X0,X1) | distinct_points(X0,intersection_point(X1,X2)) | convergent_lines(sk0,X1) | convergent_lines(sk1,X2), inference(resolution, [status(thm)], [c8, p46])).
% 23.32/3.34 cnf(p1649, plain, (distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,X0)) | convergent_lines(sk0,sk0) | convergent_lines(sk1,X0) | ~spl8), inference(resolution, [status(thm)], [p1416, p93])).
% 23.32/3.34 fof(sdef82, definition, (spl82 <=> (distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,X0)) | convergent_lines(sk1,X0))), introduced(definition, [new_symbols(naming, [spl82])], [avatar_definition])).
% 23.32/3.34 cnf(ssp152, plain, (~spl8 | spl82 | spl83), inference(avatar_split_clause, [status(thm)], [p1649, sdef82, sdef83])).
% 23.32/3.34 cnf(p108, plain, convergent_lines(sk1,X0) | distinct_lines(sk0,X1) | ~apart_point_and_line(X2,X1) | distinct_points(X2,intersection_point(X1,X0)), inference(resolution, [status(thm)], [p63, c8])).
% 23.32/3.34 cnf(p1653, plain, (convergent_lines(sk1,X0) | distinct_lines(sk0,sk0) | distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,X0)) | ~spl8), inference(resolution, [status(thm)], [p1416, p108])).
% 23.32/3.34 cnf(ssp153, plain, (~spl8 | spl82 | spl84), inference(avatar_split_clause, [status(thm)], [p1653, sdef82, sdef84])).
% 23.32/3.34 cnf(p140, plain, ~distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(sk2,X2), inference(resolution, [status(thm)], [c10, p19])).
% 23.32/3.34 cnf(p1658, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,sk1) | distinct_points(sk2,X0), inference(resolution, [status(thm)], [p140, p18])).
% 23.32/3.34 fof(sdef85, definition, (spl85 <=> (apart_point_and_line(X0,sk0) | apart_point_and_line(X0,sk1) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl85])], [avatar_definition])).
% 23.32/3.34 cnf(ssp154, plain, (spl8 | spl9 | spl85), inference(avatar_split_clause, [status(thm)], [p1658, sdef8, sdef9, sdef85])).
% 23.32/3.34 cnf(p1660, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk0,X0), inference(resolution, [status(thm)], [p140, p32])).
% 23.32/3.34 fof(sdef86, definition, (spl86 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl86])], [avatar_definition])).
% 23.32/3.34 cnf(ssp155, plain, (spl9 | spl86), inference(avatar_split_clause, [status(thm)], [p1660, sdef9, sdef86])).
% 23.32/3.34 cnf(p1662, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p140, p33])).
% 23.32/3.34 fof(sdef87, definition, (spl87 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl87])], [avatar_definition])).
% 23.32/3.34 cnf(ssp156, plain, (spl8 | spl87), inference(avatar_split_clause, [status(thm)], [p1662, sdef8, sdef87])).
% 23.32/3.34 cnf(p1664, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk0,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p140, p33])).
% 23.32/3.34 fof(sdef88, definition, (spl88 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk0,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl88])], [avatar_definition])).
% 23.32/3.34 cnf(ssp157, plain, (spl9 | spl88), inference(avatar_split_clause, [status(thm)], [p1664, sdef9, sdef88])).
% 23.32/3.34 cnf(p1667, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p140, p34])).
% 23.32/3.34 fof(sdef89, definition, (spl89 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,sk1))), introduced(definition, [new_symbols(naming, [spl89])], [avatar_definition])).
% 23.32/3.34 cnf(ssp158, plain, (spl8 | spl89), inference(avatar_split_clause, [status(thm)], [p1667, sdef8, sdef89])).
% 23.32/3.34 cnf(p1669, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk1) | distinct_points(sk2,X1) | distinct_lines(sk0,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p140, p38])).
% 23.32/3.34 fof(sdef90, definition, (spl90 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk1) | distinct_points(sk2,X1) | distinct_lines(sk0,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl90])], [avatar_definition])).
% 23.32/3.34 cnf(ssp159, plain, (spl9 | spl90), inference(avatar_split_clause, [status(thm)], [p1669, sdef9, sdef90])).
% 23.32/3.34 cnf(p1671, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,sk1) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p140, p38])).
% 23.32/3.34 fof(sdef91, definition, (spl91 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,sk1) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl91])], [avatar_definition])).
% 23.32/3.34 cnf(ssp160, plain, (spl8 | spl91), inference(avatar_split_clause, [status(thm)], [p1671, sdef8, sdef91])).
% 23.32/3.34 cnf(p1674, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk1) | distinct_points(sk2,X1) | distinct_lines(X0,sk0), inference(resolution, [status(thm)], [p140, p39])).
% 23.32/3.34 fof(sdef92, definition, (spl92 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk1) | distinct_points(sk2,X1) | distinct_lines(X0,sk0))), introduced(definition, [new_symbols(naming, [spl92])], [avatar_definition])).
% 23.32/3.34 cnf(ssp161, plain, (spl9 | spl92), inference(avatar_split_clause, [status(thm)], [p1674, sdef9, sdef92])).
% 23.32/3.34 cnf(p1677, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,sk0) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p140, p44])).
% 23.32/3.34 fof(sdef93, definition, (spl93 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,sk0) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl93])], [avatar_definition])).
% 23.32/3.34 cnf(ssp162, plain, (spl9 | spl93), inference(avatar_split_clause, [status(thm)], [p1677, sdef9, sdef93])).
% 23.32/3.34 cnf(p1679, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk0) | distinct_points(sk2,X1) | distinct_lines(sk1,X0), inference(resolution, [status(thm)], [p140, p58])).
% 23.32/3.34 fof(sdef94, definition, (spl94 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk0) | distinct_points(sk2,X1) | distinct_lines(sk1,X0))), introduced(definition, [new_symbols(naming, [spl94])], [avatar_definition])).
% 23.32/3.34 cnf(ssp163, plain, (spl8 | spl94), inference(avatar_split_clause, [status(thm)], [p1679, sdef8, sdef94])).
% 23.32/3.34 cnf(p1681, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p140, p61])).
% 23.32/3.34 fof(sdef95, definition, (spl95 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl95])], [avatar_definition])).
% 23.32/3.34 cnf(ssp164, plain, (spl8 | spl95), inference(avatar_split_clause, [status(thm)], [p1681, sdef8, sdef95])).
% 23.32/3.34 cnf(p1684, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk0,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p140, p85])).
% 23.32/3.34 fof(sdef96, definition, (spl96 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk0,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl96])], [avatar_definition])).
% 23.32/3.34 cnf(ssp165, plain, (spl9 | spl96), inference(avatar_split_clause, [status(thm)], [p1684, sdef9, sdef96])).
% 23.32/3.34 cnf(p1687, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p140, p104])).
% 23.32/3.34 fof(sdef97, definition, (spl97 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl97])], [avatar_definition])).
% 23.32/3.34 cnf(ssp166, plain, (spl8 | spl97), inference(avatar_split_clause, [status(thm)], [p1687, sdef8, sdef97])).
% 23.32/3.34 cnf(p1690, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk0,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p140, p126])).
% 23.32/3.34 fof(sdef98, definition, (spl98 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk0,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl98])], [avatar_definition])).
% 23.32/3.34 cnf(ssp167, plain, (spl9 | spl98), inference(avatar_split_clause, [status(thm)], [p1690, sdef9, sdef98])).
% 23.32/3.34 cnf(p1694, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk1) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p140, p209])).
% 23.32/3.34 fof(sdef99, definition, (spl99 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk1) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl99])], [avatar_definition])).
% 23.32/3.34 cnf(ssp168, plain, (spl8 | spl99), inference(avatar_split_clause, [status(thm)], [p1694, sdef8, sdef99])).
% 23.32/3.34 cnf(p1700, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk0) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p140, p325])).
% 23.32/3.34 fof(sdef100, definition, (spl100 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk0) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl100])], [avatar_definition])).
% 23.32/3.34 cnf(ssp169, plain, (spl9 | spl100), inference(avatar_split_clause, [status(thm)], [p1700, sdef9, sdef100])).
% 23.32/3.34 cnf(p1702, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p140, p378])).
% 23.32/3.34 fof(sdef101, definition, (spl101 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl101])], [avatar_definition])).
% 23.32/3.34 cnf(ssp170, plain, (spl8 | spl101), inference(avatar_split_clause, [status(thm)], [p1702, sdef8, sdef101])).
% 23.32/3.34 cnf(p1704, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,X0) | distinct_lines(sk0,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p140, p35])).
% 23.32/3.34 fof(sdef102, definition, (spl102 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,X0) | distinct_lines(sk0,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl102])], [avatar_definition])).
% 23.32/3.34 cnf(ssp171, plain, (spl9 | spl102), inference(avatar_split_clause, [status(thm)], [p1704, sdef9, sdef102])).
% 23.32/3.34 cnf(p1707, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk1,X2) | distinct_lines(X3,X2) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p140, p35])).
% 23.32/3.34 fof(sdef103, definition, (spl103 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk1,X2) | distinct_lines(X3,X2) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl103])], [avatar_definition])).
% 23.32/3.34 cnf(ssp172, plain, (spl8 | spl103), inference(avatar_split_clause, [status(thm)], [p1707, sdef8, sdef103])).
% 23.32/3.34 cnf(p1710, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(sk1,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p140, p36])).
% 23.32/3.34 fof(sdef104, definition, (spl104 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(sk1,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl104])], [avatar_definition])).
% 23.32/3.34 cnf(ssp173, plain, (spl8 | spl104), inference(avatar_split_clause, [status(thm)], [p1710, sdef8, sdef104])).
% 23.32/3.34 cnf(p1712, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk0,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p140, p36])).
% 23.32/3.34 fof(sdef105, definition, (spl105 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk0,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl105])], [avatar_definition])).
% 23.32/3.34 cnf(ssp174, plain, (spl9 | spl105), inference(avatar_split_clause, [status(thm)], [p1712, sdef9, sdef105])).
% 23.32/3.34 cnf(p1715, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(X2,sk1), inference(resolution, [status(thm)], [p140, p444])).
% 23.32/3.34 fof(sdef106, definition, (spl106 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(X2,sk1))), introduced(definition, [new_symbols(naming, [spl106])], [avatar_definition])).
% 23.32/3.34 cnf(ssp175, plain, (spl8 | spl106), inference(avatar_split_clause, [status(thm)], [p1715, sdef8, sdef106])).
% 23.32/3.34 cnf(p1717, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk1,X2) | distinct_lines(X0,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p140, p37])).
% 23.32/3.34 fof(sdef107, definition, (spl107 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk1,X2) | distinct_lines(X0,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl107])], [avatar_definition])).
% 23.32/3.34 cnf(ssp176, plain, (spl8 | spl107), inference(avatar_split_clause, [status(thm)], [p1717, sdef8, sdef107])).
% 23.32/3.34 cnf(p1719, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk0,X2) | distinct_lines(X2,X3) | distinct_lines(X0,X3), inference(resolution, [status(thm)], [p140, p37])).
% 23.32/3.34 fof(sdef108, definition, (spl108 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk0,X2) | distinct_lines(X2,X3) | distinct_lines(X0,X3))), introduced(definition, [new_symbols(naming, [spl108])], [avatar_definition])).
% 23.32/3.34 cnf(ssp177, plain, (spl9 | spl108), inference(avatar_split_clause, [status(thm)], [p1719, sdef9, sdef108])).
% 23.32/3.34 cnf(p1722, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk1) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(sk0,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p140, p40])).
% 23.32/3.34 fof(sdef109, definition, (spl109 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk1) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(sk0,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl109])], [avatar_definition])).
% 23.32/3.34 cnf(ssp178, plain, (spl9 | spl109), inference(avatar_split_clause, [status(thm)], [p1722, sdef9, sdef109])).
% 23.32/3.34 cnf(p1725, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,sk1) | distinct_lines(X2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p140, p40])).
% 23.32/3.34 fof(sdef110, definition, (spl110 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,sk1) | distinct_lines(X2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl110])], [avatar_definition])).
% 23.32/3.34 cnf(ssp179, plain, (spl8 | spl110), inference(avatar_split_clause, [status(thm)], [p1725, sdef8, sdef110])).
% 23.32/3.34 cnf(p1728, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk1) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(X2,sk0), inference(resolution, [status(thm)], [p140, p449])).
% 23.32/3.34 fof(sdef111, definition, (spl111 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk1) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(X2,sk0))), introduced(definition, [new_symbols(naming, [spl111])], [avatar_definition])).
% 23.32/3.34 cnf(ssp180, plain, (spl9 | spl111), inference(avatar_split_clause, [status(thm)], [p1728, sdef9, sdef111])).
% 23.32/3.34 cnf(p1731, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,sk1) | distinct_lines(X2,X3) | distinct_lines(X0,X3), inference(resolution, [status(thm)], [p140, p41])).
% 23.32/3.34 fof(sdef112, definition, (spl112 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,sk1) | distinct_lines(X2,X3) | distinct_lines(X0,X3))), introduced(definition, [new_symbols(naming, [spl112])], [avatar_definition])).
% 23.32/3.34 cnf(ssp181, plain, (spl8 | spl112), inference(avatar_split_clause, [status(thm)], [p1731, sdef8, sdef112])).
% 23.32/3.34 cnf(p1734, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,sk0) | distinct_lines(X2,X3) | distinct_lines(X0,X3), inference(resolution, [status(thm)], [p140, p59])).
% 23.32/3.34 fof(sdef113, definition, (spl113 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,sk0) | distinct_lines(X2,X3) | distinct_lines(X0,X3))), introduced(definition, [new_symbols(naming, [spl113])], [avatar_definition])).
% 23.32/3.34 cnf(ssp182, plain, (spl9 | spl113), inference(avatar_split_clause, [status(thm)], [p1734, sdef9, sdef113])).
% 23.32/3.34 cnf(p1739, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,sk0) | distinct_lines(X2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p140, p60])).
% 23.32/3.34 fof(sdef114, definition, (spl114 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,sk0) | distinct_lines(X2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl114])], [avatar_definition])).
% 23.32/3.34 cnf(ssp183, plain, (spl9 | spl114), inference(avatar_split_clause, [status(thm)], [p1739, sdef9, sdef114])).
% 23.32/3.34 cnf(p1741, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk1) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p140, p506])).
% 23.32/3.34 fof(sdef115, definition, (spl115 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk1) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl115])], [avatar_definition])).
% 23.32/3.34 cnf(ssp184, plain, (spl8 | spl115), inference(avatar_split_clause, [status(thm)], [p1741, sdef8, sdef115])).
% 23.32/3.34 cnf(p1743, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk0) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p140, p559])).
% 23.32/3.34 fof(sdef116, definition, (spl116 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk0) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl116])], [avatar_definition])).
% 23.32/3.34 cnf(ssp185, plain, (spl9 | spl116), inference(avatar_split_clause, [status(thm)], [p1743, sdef9, sdef116])).
% 23.32/3.34 cnf(p1745, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk1,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p140, p101])).
% 23.32/3.34 fof(sdef117, definition, (spl117 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk1,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl117])], [avatar_definition])).
% 23.32/3.34 cnf(ssp186, plain, (spl8 | spl117), inference(avatar_split_clause, [status(thm)], [p1745, sdef8, sdef117])).
% 23.32/3.34 cnf(p1755, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk0,X2) | distinct_lines(X3,X2) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p140, p179])).
% 23.32/3.34 fof(sdef118, definition, (spl118 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk0,X2) | distinct_lines(X3,X2) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl118])], [avatar_definition])).
% 23.32/3.34 cnf(ssp187, plain, (spl9 | spl118), inference(avatar_split_clause, [status(thm)], [p1755, sdef9, sdef118])).
% 23.32/3.34 cnf(p1758, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk0,X2) | distinct_lines(X0,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p140, p180])).
% 23.32/3.34 fof(sdef119, definition, (spl119 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk0,X2) | distinct_lines(X0,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl119])], [avatar_definition])).
% 23.32/3.34 cnf(ssp188, plain, (spl9 | spl119), inference(avatar_split_clause, [status(thm)], [p1758, sdef9, sdef119])).
% 23.32/3.34 cnf(p1762, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | convergent_lines(sk0,X3) | convergent_lines(X2,X3), inference(resolution, [status(thm)], [p140, p181])).
% 23.32/3.34 fof(sdef120, definition, (spl120 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | convergent_lines(sk0,X3) | convergent_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl120])], [avatar_definition])).
% 23.32/3.34 cnf(ssp189, plain, (spl9 | spl120), inference(avatar_split_clause, [status(thm)], [p1762, sdef9, sdef120])).
% 23.32/3.34 cnf(p1766, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk1,X2) | distinct_lines(X3,X2) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p140, p186])).
% 23.32/3.34 fof(sdef121, definition, (spl121 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk1,X2) | distinct_lines(X3,X2) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl121])], [avatar_definition])).
% 23.32/3.34 cnf(ssp190, plain, (spl8 | spl121), inference(avatar_split_clause, [status(thm)], [p1766, sdef8, sdef121])).
% 23.32/3.34 cnf(p1769, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk1,X2) | distinct_lines(X0,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p140, p187])).
% 23.32/3.34 fof(sdef122, definition, (spl122 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk1,X2) | distinct_lines(X0,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl122])], [avatar_definition])).
% 23.32/3.34 cnf(ssp191, plain, (spl8 | spl122), inference(avatar_split_clause, [status(thm)], [p1769, sdef8, sdef122])).
% 23.32/3.34 cnf(p1773, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | convergent_lines(sk1,X3) | convergent_lines(X2,X3), inference(resolution, [status(thm)], [p140, p188])).
% 23.32/3.34 fof(sdef123, definition, (spl123 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | convergent_lines(sk1,X3) | convergent_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl123])], [avatar_definition])).
% 23.32/3.34 cnf(ssp192, plain, (spl8 | spl123), inference(avatar_split_clause, [status(thm)], [p1773, sdef8, sdef123])).
% 23.32/3.34 cnf(p1776, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk0,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p140, p191])).
% 23.32/3.34 fof(sdef124, definition, (spl124 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk0,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl124])], [avatar_definition])).
% 23.32/3.34 cnf(ssp193, plain, (spl9 | spl124), inference(avatar_split_clause, [status(thm)], [p1776, sdef9, sdef124])).
% 23.32/3.34 cnf(p1778, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,X0) | convergent_lines(sk0,X3) | convergent_lines(X2,X3), inference(resolution, [status(thm)], [p140, p192])).
% 23.32/3.34 fof(sdef125, definition, (spl125 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,X0) | convergent_lines(sk0,X3) | convergent_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl125])], [avatar_definition])).
% 23.32/3.34 cnf(ssp194, plain, (spl9 | spl125), inference(avatar_split_clause, [status(thm)], [p1778, sdef9, sdef125])).
% 23.32/3.34 cnf(p1787, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk1) | distinct_lines(X2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p140, p302])).
% 23.32/3.34 fof(sdef126, definition, (spl126 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk1) | distinct_lines(X2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl126])], [avatar_definition])).
% 23.32/3.34 cnf(ssp195, plain, (spl8 | spl126), inference(avatar_split_clause, [status(thm)], [p1787, sdef8, sdef126])).
% 23.32/3.34 cnf(p1790, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk1) | distinct_lines(X2,X3) | distinct_lines(X0,X3), inference(resolution, [status(thm)], [p140, p303])).
% 23.32/3.34 fof(sdef127, definition, (spl127 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk1) | distinct_lines(X2,X3) | distinct_lines(X0,X3))), introduced(definition, [new_symbols(naming, [spl127])], [avatar_definition])).
% 23.32/3.34 cnf(ssp196, plain, (spl8 | spl127), inference(avatar_split_clause, [status(thm)], [p1790, sdef8, sdef127])).
% 23.32/3.34 cnf(p1793, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,X0) | convergent_lines(X2,X3) | convergent_lines(sk1,X3), inference(resolution, [status(thm)], [p140, p304])).
% 23.32/3.34 fof(sdef128, definition, (spl128 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,X0) | convergent_lines(X2,X3) | convergent_lines(sk1,X3))), introduced(definition, [new_symbols(naming, [spl128])], [avatar_definition])).
% 23.32/3.34 cnf(ssp197, plain, (spl8 | spl128), inference(avatar_split_clause, [status(thm)], [p1793, sdef8, sdef128])).
% 23.32/3.34 cnf(p1801, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk0) | distinct_lines(X2,X3) | distinct_lines(X0,X3), inference(resolution, [status(thm)], [p140, p374])).
% 23.32/3.34 fof(sdef129, definition, (spl129 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk0) | distinct_lines(X2,X3) | distinct_lines(X0,X3))), introduced(definition, [new_symbols(naming, [spl129])], [avatar_definition])).
% 23.32/3.34 cnf(ssp198, plain, (spl9 | spl129), inference(avatar_split_clause, [status(thm)], [p1801, sdef9, sdef129])).
% 23.32/3.34 cnf(p1806, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk0) | distinct_lines(X2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p140, p375])).
% 23.32/3.34 fof(sdef130, definition, (spl130 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk0) | distinct_lines(X2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl130])], [avatar_definition])).
% 23.32/3.34 cnf(ssp199, plain, (spl9 | spl130), inference(avatar_split_clause, [status(thm)], [p1806, sdef9, sdef130])).
% 23.32/3.34 cnf(p1808, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk1,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p140, p405])).
% 23.32/3.34 fof(sdef131, definition, (spl131 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk1,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl131])], [avatar_definition])).
% 23.32/3.34 cnf(ssp200, plain, (spl8 | spl131), inference(avatar_split_clause, [status(thm)], [p1808, sdef8, sdef131])).
% 23.32/3.34 cnf(p1810, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,X3) | distinct_lines(X3,sk1) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p140, p447])).
% 23.32/3.34 fof(sdef132, definition, (spl132 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,X3) | distinct_lines(X3,sk1) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl132])], [avatar_definition])).
% 23.32/3.34 cnf(ssp201, plain, (spl8 | spl132), inference(avatar_split_clause, [status(thm)], [p1810, sdef8, sdef132])).
% 23.32/3.34 cnf(p1814, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,X3) | distinct_lines(X3,sk0) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p140, p453])).
% 23.32/3.34 fof(sdef133, definition, (spl133 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X2,X3) | distinct_lines(X3,sk0) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl133])], [avatar_definition])).
% 23.32/3.34 cnf(ssp202, plain, (spl9 | spl133), inference(avatar_split_clause, [status(thm)], [p1814, sdef9, sdef133])).
% 23.32/3.34 cnf(p1819, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk1) | distinct_lines(X3,X2) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p140, p523])).
% 23.32/3.34 fof(sdef134, definition, (spl134 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk1) | distinct_lines(X3,X2) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl134])], [avatar_definition])).
% 23.32/3.34 cnf(ssp203, plain, (spl8 | spl134), inference(avatar_split_clause, [status(thm)], [p1819, sdef8, sdef134])).
% 23.32/3.34 cnf(p1824, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk0) | distinct_lines(X3,X2) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p140, p569])).
% 23.32/3.34 fof(sdef135, definition, (spl135 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(X2,sk0) | distinct_lines(X3,X2) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl135])], [avatar_definition])).
% 23.32/3.34 cnf(ssp204, plain, (spl9 | spl135), inference(avatar_split_clause, [status(thm)], [p1824, sdef9, sdef135])).
% 23.32/3.34 cnf(p1827, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk0,X2) | convergent_lines(X2,X3) | distinct_lines(X0,X3), inference(resolution, [status(thm)], [p140, p574])).
% 23.32/3.34 fof(sdef136, definition, (spl136 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk0,X2) | convergent_lines(X2,X3) | distinct_lines(X0,X3))), introduced(definition, [new_symbols(naming, [spl136])], [avatar_definition])).
% 23.32/3.34 cnf(ssp205, plain, (spl9 | spl136), inference(avatar_split_clause, [status(thm)], [p1827, sdef9, sdef136])).
% 23.32/3.34 cnf(p1831, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk1,X2) | convergent_lines(X2,X3) | distinct_lines(X0,X3), inference(resolution, [status(thm)], [p140, p596])).
% 23.32/3.34 fof(sdef137, definition, (spl137 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | convergent_lines(sk1,X2) | convergent_lines(X2,X3) | distinct_lines(X0,X3))), introduced(definition, [new_symbols(naming, [spl137])], [avatar_definition])).
% 23.32/3.34 cnf(ssp206, plain, (spl8 | spl137), inference(avatar_split_clause, [status(thm)], [p1831, sdef8, sdef137])).
% 23.32/3.34 cnf(p1848, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk0,X2) | convergent_lines(X2,X3) | distinct_lines(X0,X3), inference(resolution, [status(thm)], [p140, p734])).
% 23.32/3.34 fof(sdef138, definition, (spl138 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk0,X2) | convergent_lines(X2,X3) | distinct_lines(X0,X3))), introduced(definition, [new_symbols(naming, [spl138])], [avatar_definition])).
% 23.32/3.34 cnf(ssp207, plain, (spl9 | spl138), inference(avatar_split_clause, [status(thm)], [p1848, sdef9, sdef138])).
% 23.32/3.34 cnf(p1851, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk1,X2) | convergent_lines(X2,X3) | distinct_lines(X0,X3), inference(resolution, [status(thm)], [p140, p735])).
% 23.32/3.34 fof(sdef139, definition, (spl139 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(sk1,X2) | convergent_lines(X2,X3) | distinct_lines(X0,X3))), introduced(definition, [new_symbols(naming, [spl139])], [avatar_definition])).
% 23.32/3.34 cnf(ssp208, plain, (spl8 | spl139), inference(avatar_split_clause, [status(thm)], [p1851, sdef8, sdef139])).
% 23.32/3.34 cnf(p1854, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | convergent_lines(X2,X3) | distinct_lines(sk0,X3), inference(resolution, [status(thm)], [p140, p754])).
% 23.32/3.34 fof(sdef140, definition, (spl140 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | convergent_lines(X2,X3) | distinct_lines(sk0,X3))), introduced(definition, [new_symbols(naming, [spl140])], [avatar_definition])).
% 23.32/3.34 cnf(ssp209, plain, (spl9 | spl140), inference(avatar_split_clause, [status(thm)], [p1854, sdef9, sdef140])).
% 23.32/3.34 cnf(p1857, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | convergent_lines(sk0,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p140, p755])).
% 23.32/3.34 fof(sdef141, definition, (spl141 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk1) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | convergent_lines(sk0,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl141])], [avatar_definition])).
% 23.32/3.34 cnf(ssp210, plain, (spl9 | spl141), inference(avatar_split_clause, [status(thm)], [p1857, sdef9, sdef141])).
% 23.32/3.34 cnf(p1859, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | convergent_lines(X2,X3) | distinct_lines(sk1,X3), inference(resolution, [status(thm)], [p140, p776])).
% 23.32/3.34 fof(sdef142, definition, (spl142 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | convergent_lines(X2,X3) | distinct_lines(sk1,X3))), introduced(definition, [new_symbols(naming, [spl142])], [avatar_definition])).
% 23.32/3.34 cnf(ssp211, plain, (spl8 | spl142), inference(avatar_split_clause, [status(thm)], [p1859, sdef8, sdef142])).
% 23.32/3.34 cnf(p1862, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | convergent_lines(sk1,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p140, p777])).
% 23.32/3.34 fof(sdef143, definition, (spl143 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X1,sk0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | distinct_lines(X0,X2) | convergent_lines(sk1,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl143])], [avatar_definition])).
% 23.32/3.34 cnf(ssp212, plain, (spl8 | spl143), inference(avatar_split_clause, [status(thm)], [p1862, sdef8, sdef143])).
% 23.32/3.34 cnf(sat_ref, plain, $false, inference(avatar_sat_refutation, [status(thm)], [ssp0, ssp1, ssp2, ssp3, ssp4, ssp5, ssp6, ssp7, ssp8, ssp9, ssp10, ssp11, ssp12, ssp13, ssp14, ssp15, ssp16, ssp17, ssp18, ssp19, ssp20, ssp21, ssp22, ssp23, ssp24, ssp25, ssp26, ssp27, ssp28, ssp29, ssp30, ssp31, ssp32, ssp33, ssp34, ssp35, ssp36, ssp37, ssp38, ssp39, ssp40, ssp41, ssp42, ssp43, ssp44, ssp45, ssp46, ssp47, ssp48, ssp49, ssp50, ssp51, ssp52, ssp53, ssp54, ssp55, ssp56, ssp57, ssp58, ssp59, ssp60, ssp61, ssp62, ssp63, ssp64, ssp65, ssp66, ssp67, ssp68, ssp69, ssp70, ssp71, ssp72, ssp73, ssp74, ssp75, ssp76, ssp77, ssp78, ssp79, ssp80, ssp81, ssp82, ssp83, ssp84, ssp85, ssp86, ssp87, ssp88, ssp89, ssp90, ssp91, ssp92, ssp93, ssp94, ssp95, ssp96, ssp97, ssp98, ssp99, ssp100, ssp101, ssp102, ssp103, ssp104, ssp105, ssp106, ssp107, ssp108, ssp109, ssp110, ssp111, ssp112, ssp113, ssp114, ssp115, ssp116, ssp117, ssp118, ssp119, ssp120, ssp121, ssp122, ssp123, ssp124, ssp125, ssp126, ssp127, ssp128, ssp129, ssp130, ssp131, ssp132, ssp133, ssp134, ssp135, ssp136, ssp137, ssp138, ssp139, ssp140, ssp141, ssp142, ssp143, ssp144, ssp145, ssp146, ssp147, ssp148, ssp149, ssp150, ssp151, ssp152, ssp153, ssp154, ssp155, ssp156, ssp157, ssp158, ssp159, ssp160, ssp161, ssp162, ssp163, ssp164, ssp165, ssp166, ssp167, ssp168, ssp169, ssp170, ssp171, ssp172, ssp173, ssp174, ssp175, ssp176, ssp177, ssp178, ssp179, ssp180, ssp181, ssp182, ssp183, ssp184, ssp185, ssp186, ssp187, ssp188, ssp189, ssp190, ssp191, ssp192, ssp193, ssp194, ssp195, ssp196, ssp197, ssp198, ssp199, ssp200, ssp201, ssp202, ssp203, ssp204, ssp205, ssp206, ssp207, ssp208, ssp209, ssp210, ssp211, ssp212, sct0, sct1, sct2, sct3, sct4, sct5, sct6, sct7, sct8])).
% 23.32/3.34 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------