%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO195+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 : n006.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:24 PM UTC 2026
% Result : Theorem 25.60s 3.79s
% Output : Proof 25.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO195+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.06/0.33 % Computer : n006.cluster.edu
% 0.06/0.33 % Model : x86_64 x86_64
% 0.06/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.33 % Memory : 8046.5625MB
% 0.06/0.33 % OS : Linux 6.8.0-71-generic
% 0.06/0.33 % CPULimit : 300
% 0.06/0.33 % WCLimit : 300
% 0.06/0.33 % DateTime : Wed Sep 23 11:23:56 UTC 2026
% 0.06/0.33 % CPUTime :
% 0.06/0.33 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 25.60/3.79 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 25.60/3.79 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 25.60/3.79 fof(sdef0, definition, (spl0 <=> (distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 25.60/3.79 cnf(p312, plain, (distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 25.60/3.79 fof(f0, axiom, ! [X] : ~ distinct_points(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart1)).
% 25.60/3.79 fof(f0_nnf, plain, ! [X] : (~(distinct_points(X,X))), inference(nnf_transformation, [status(thm)], [f0])).
% 25.60/3.79 fof(f0_sk, plain, ! [X] : (~(distinct_points(X,X))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 25.60/3.79 cnf(c0, plain, ~distinct_points(X0,X0), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.60/3.79 cnf(p314, plain, ($false | ~spl0), inference(resolution, [status(thm)], [p312, c0])).
% 25.60/3.79 cnf(sct0, plain, (~spl0), inference(avatar_contradiction_clause, [status(thm)], [p314])).
% 25.60/3.79 fof(sdef24, definition, (spl24 <=> (convergent_lines(sk0,sk0))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 25.60/3.79 cnf(p513, plain, (convergent_lines(sk0,sk0) | ~spl24), inference(avatar_component_clause, [status(thm)], [sdef24])).
% 25.60/3.79 fof(f2, axiom, ! [X] : ~ convergent_lines(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart3)).
% 25.60/3.79 fof(f2_nnf, plain, ! [X] : (~(convergent_lines(X,X))), inference(nnf_transformation, [status(thm)], [f2])).
% 25.60/3.79 fof(f2_sk, plain, ! [X] : (~(convergent_lines(X,X))), inference(skolemisation, [status(esa)], [f2_nnf])).
% 25.60/3.79 cnf(c2, plain, ~convergent_lines(X0,X0), inference(cnf_transformation, [status(esa)], [f2_sk])).
% 25.60/3.79 cnf(p515, plain, ($false | ~spl24), inference(resolution, [status(thm)], [p513, c2])).
% 25.60/3.79 cnf(sct1, plain, (~spl24), inference(avatar_contradiction_clause, [status(thm)], [p515])).
% 25.60/3.79 fof(sdef2, definition, (spl2 <=> (apart_point_and_line(intersection_point(sk0,sk1),sk0))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 25.60/3.79 cnf(p445, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk0) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 25.60/3.79 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)).
% 25.60/3.79 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])).
% 25.60/3.79 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])).
% 25.60/3.79 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])).
% 25.60/3.79 fof(f12, conjecture, ! [X,Y,Z] : ( ( convergent_lines(X,Y) & convergent_lines(Z,Y) & convergent_lines(X,Z) ) => ( apart_point_and_line(intersection_point(X,Y),Z) => apart_point_and_line(intersection_point(Y,X),Z) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 25.60/3.79 fof(f12_neg, negated_conjecture, ~(! [X,Y,Z] : ( ( convergent_lines(X,Y) & convergent_lines(Z,Y) & convergent_lines(X,Z) ) => ( apart_point_and_line(intersection_point(X,Y),Z) => apart_point_and_line(intersection_point(Y,X),Z) ) )), inference(negated_conjecture, [status(cth)], [f12])).
% 25.60/3.79 fof(f12_nnf, plain, ? [X,Y,Z] : ((((convergent_lines(X,Y) & convergent_lines(Z,Y)) & convergent_lines(X,Z)) & (apart_point_and_line(intersection_point(X,Y),Z) & ~(apart_point_and_line(intersection_point(Y,X),Z))))), inference(nnf_transformation, [status(thm)], [f12_neg])).
% 25.60/3.79 fof(f12_sk, plain, (((convergent_lines(sk0,sk1) & convergent_lines(sk2,sk1)) & convergent_lines(sk0,sk2)) & (apart_point_and_line(intersection_point(sk0,sk1),sk2) & ~(apart_point_and_line(intersection_point(sk1,sk0),sk2)))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2])], [f12_nnf])).
% 25.60/3.79 cnf(c14, plain, convergent_lines(sk0,sk1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 25.60/3.79 cnf(p44, plain, ~apart_point_and_line(X0,sk0) | distinct_points(X0,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [c8, c14])).
% 25.60/3.79 cnf(p492, plain, (distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)) | ~spl2), inference(resolution, [status(thm)], [p445, p44])).
% 25.60/3.79 cnf(p526, plain, ($false | ~spl2), inference(resolution, [status(thm)], [p492, c0])).
% 25.60/3.79 cnf(sct2, plain, (~spl2), inference(avatar_contradiction_clause, [status(thm)], [p526])).
% 25.60/3.79 fof(sdef3, definition, (spl3 <=> (apart_point_and_line(intersection_point(sk0,sk1),sk1))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 25.60/3.79 cnf(p446, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk1) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 25.60/3.79 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])).
% 25.60/3.79 cnf(p58, plain, ~apart_point_and_line(X0,sk1) | distinct_points(X0,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [c9, c14])).
% 25.60/3.79 cnf(p498, plain, (distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)) | ~spl3), inference(resolution, [status(thm)], [p446, p58])).
% 25.60/3.79 cnf(p527, plain, ($false | ~spl3), inference(resolution, [status(thm)], [p498, c0])).
% 25.60/3.79 cnf(sct3, plain, (~spl3), inference(avatar_contradiction_clause, [status(thm)], [p527])).
% 25.60/3.79 fof(sdef5, definition, (spl5 <=> (apart_point_and_line(intersection_point(sk2,sk1),sk1))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 25.60/3.79 cnf(p448, plain, (apart_point_and_line(intersection_point(sk2,sk1),sk1) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 25.60/3.79 cnf(c15, plain, convergent_lines(sk2,sk1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 25.60/3.79 cnf(p59, plain, ~apart_point_and_line(X0,sk1) | distinct_points(X0,intersection_point(sk2,sk1)), inference(resolution, [status(thm)], [c9, c15])).
% 25.60/3.79 cnf(p520, plain, (distinct_points(intersection_point(sk2,sk1),intersection_point(sk2,sk1)) | ~spl5), inference(resolution, [status(thm)], [p448, p59])).
% 25.60/3.79 cnf(p618, plain, ($false | ~spl5), inference(resolution, [status(thm)], [p520, c0])).
% 25.60/3.79 cnf(sct4, plain, (~spl5), inference(avatar_contradiction_clause, [status(thm)], [p618])).
% 25.60/3.79 fof(sdef26, definition, (spl26 <=> (apart_point_and_line(intersection_point(sk0,sk2),sk0))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 25.60/3.79 cnf(p543, plain, (apart_point_and_line(intersection_point(sk0,sk2),sk0) | ~spl26), inference(avatar_component_clause, [status(thm)], [sdef26])).
% 25.60/3.79 cnf(c16, plain, convergent_lines(sk0,sk2), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 25.60/3.79 cnf(p46, plain, ~apart_point_and_line(X0,sk0) | distinct_points(X0,intersection_point(sk0,sk2)), inference(resolution, [status(thm)], [c8, c16])).
% 25.60/3.79 cnf(p589, plain, (distinct_points(intersection_point(sk0,sk2),intersection_point(sk0,sk2)) | ~spl26), inference(resolution, [status(thm)], [p543, p46])).
% 25.60/3.79 cnf(p621, plain, ($false | ~spl26), inference(resolution, [status(thm)], [p589, c0])).
% 25.60/3.79 cnf(sct5, plain, (~spl26), inference(avatar_contradiction_clause, [status(thm)], [p621])).
% 25.60/3.79 fof(sdef48, definition, (spl48 <=> (apart_point_and_line(intersection_point(sk1,sk2),sk1))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 25.60/3.79 cnf(p638, plain, (apart_point_and_line(intersection_point(sk1,sk2),sk1) | ~spl48), inference(avatar_component_clause, [status(thm)], [sdef48])).
% 25.60/3.79 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)).
% 25.60/3.79 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])).
% 25.60/3.79 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])).
% 25.60/3.79 cnf(c5, plain, ~convergent_lines(X0,X1) | convergent_lines(X0,X2) | convergent_lines(X1,X2), inference(cnf_transformation, [status(esa)], [f5_sk])).
% 25.60/3.79 cnf(p26, plain, convergent_lines(sk2,X0) | convergent_lines(sk1,X0), inference(resolution, [status(thm)], [c5, c15])).
% 25.60/3.79 cnf(p34, plain, convergent_lines(sk1,sk2), inference(resolution, [status(thm)], [p26, c2])).
% 25.60/3.79 cnf(p49, plain, ~apart_point_and_line(X0,sk1) | distinct_points(X0,intersection_point(sk1,sk2)), inference(resolution, [status(thm)], [c8, p34])).
% 25.60/3.79 cnf(p692, plain, (distinct_points(intersection_point(sk1,sk2),intersection_point(sk1,sk2)) | ~spl48), inference(resolution, [status(thm)], [p638, p49])).
% 25.60/3.79 cnf(p742, plain, ($false | ~spl48), inference(resolution, [status(thm)], [p692, c0])).
% 25.60/3.79 cnf(sct6, plain, (~spl48), inference(avatar_contradiction_clause, [status(thm)], [p742])).
% 25.60/3.79 fof(sdef69, definition, (spl69 <=> (distinct_points(intersection_point(sk2,sk1),intersection_point(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 25.60/3.79 cnf(p751, plain, (distinct_points(intersection_point(sk2,sk1),intersection_point(sk2,sk1)) | ~spl69), inference(avatar_component_clause, [status(thm)], [sdef69])).
% 25.60/3.79 cnf(p757, plain, ($false | ~spl69), inference(resolution, [status(thm)], [p751, c0])).
% 25.60/3.79 cnf(sct7, plain, (~spl69), inference(avatar_contradiction_clause, [status(thm)], [p757])).
% 25.60/3.79 fof(sdef73, definition, (spl73 <=> (distinct_points(intersection_point(sk0,sk2),intersection_point(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 25.60/3.79 cnf(p774, plain, (distinct_points(intersection_point(sk0,sk2),intersection_point(sk0,sk2)) | ~spl73), inference(avatar_component_clause, [status(thm)], [sdef73])).
% 25.60/3.79 cnf(p821, plain, ($false | ~spl73), inference(resolution, [status(thm)], [p774, c0])).
% 25.60/3.79 cnf(sct8, plain, (~spl73), inference(avatar_contradiction_clause, [status(thm)], [p821])).
% 25.60/3.79 fof(sdef93, definition, (spl93 <=> (distinct_points(intersection_point(sk1,sk2),intersection_point(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl93])], [avatar_definition])).
% 25.60/3.79 cnf(p834, plain, (distinct_points(intersection_point(sk1,sk2),intersection_point(sk1,sk2)) | ~spl93), inference(avatar_component_clause, [status(thm)], [sdef93])).
% 25.60/3.79 cnf(p874, plain, ($false | ~spl93), inference(resolution, [status(thm)], [p834, c0])).
% 25.60/3.79 cnf(sct9, plain, (~spl93), inference(avatar_contradiction_clause, [status(thm)], [p874])).
% 25.60/3.79 fof(sdef176, definition, (spl176 <=> (distinct_lines(sk2,sk2))), introduced(definition, [new_symbols(naming, [spl176])], [avatar_definition])).
% 25.60/3.79 cnf(p1130, plain, (distinct_lines(sk2,sk2) | ~spl176), inference(avatar_component_clause, [status(thm)], [sdef176])).
% 25.60/3.79 fof(f1, axiom, ! [X] : ~ distinct_lines(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart2)).
% 25.60/3.79 fof(f1_nnf, plain, ! [X] : (~(distinct_lines(X,X))), inference(nnf_transformation, [status(thm)], [f1])).
% 25.60/3.79 fof(f1_sk, plain, ! [X] : (~(distinct_lines(X,X))), inference(skolemisation, [status(esa)], [f1_nnf])).
% 25.60/3.79 cnf(c1, plain, ~distinct_lines(X0,X0), inference(cnf_transformation, [status(esa)], [f1_sk])).
% 25.60/3.79 cnf(p1160, plain, ($false | ~spl176), inference(resolution, [status(thm)], [p1130, c1])).
% 25.60/3.79 cnf(sct10, plain, (~spl176), inference(avatar_contradiction_clause, [status(thm)], [p1160])).
% 25.60/3.79 fof(sdef200, definition, (spl200 <=> (convergent_lines(sk1,sk1))), introduced(definition, [new_symbols(naming, [spl200])], [avatar_definition])).
% 25.60/3.79 cnf(p1497, plain, (convergent_lines(sk1,sk1) | ~spl200), inference(avatar_component_clause, [status(thm)], [sdef200])).
% 25.60/3.79 cnf(p1501, plain, ($false | ~spl200), inference(resolution, [status(thm)], [p1497, c2])).
% 25.60/3.79 cnf(sct11, plain, (~spl200), inference(avatar_contradiction_clause, [status(thm)], [p1501])).
% 25.60/3.79 fof(sdef195, definition, (spl195 <=> (apart_point_and_line(intersection_point(sk1,sk0),sk0))), introduced(definition, [new_symbols(naming, [spl195])], [avatar_definition])).
% 25.60/3.79 cnf(p1461, plain, (apart_point_and_line(intersection_point(sk1,sk0),sk0) | ~spl195), inference(avatar_component_clause, [status(thm)], [sdef195])).
% 25.60/3.79 cnf(p25, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X0), inference(resolution, [status(thm)], [c5, c14])).
% 25.60/3.79 cnf(p33, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p25, c5])).
% 25.60/3.79 cnf(p102, plain, convergent_lines(sk0,X0) | convergent_lines(X0,sk1), inference(resolution, [status(thm)], [p33, c2])).
% 25.60/3.79 cnf(p117, plain, convergent_lines(X0,sk1) | convergent_lines(sk0,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p102, c5])).
% 25.60/3.79 cnf(p266, plain, convergent_lines(X0,sk1) | convergent_lines(X0,sk0), inference(resolution, [status(thm)], [p117, c2])).
% 25.60/3.79 cnf(p277, plain, convergent_lines(sk1,sk0), inference(resolution, [status(thm)], [p266, c2])).
% 25.60/3.79 cnf(p283, plain, ~apart_point_and_line(X0,sk0) | distinct_points(X0,intersection_point(sk1,sk0)), inference(resolution, [status(thm)], [p277, c9])).
% 25.60/3.79 cnf(p1476, plain, (distinct_points(intersection_point(sk1,sk0),intersection_point(sk1,sk0)) | ~spl195), inference(resolution, [status(thm)], [p1461, p283])).
% 25.60/3.79 cnf(p1506, plain, ($false | ~spl195), inference(resolution, [status(thm)], [p1476, c0])).
% 25.60/3.79 cnf(sct12, plain, (~spl195), inference(avatar_contradiction_clause, [status(thm)], [p1506])).
% 25.60/3.79 fof(sdef196, definition, (spl196 <=> (apart_point_and_line(intersection_point(sk1,sk0),sk1))), introduced(definition, [new_symbols(naming, [spl196])], [avatar_definition])).
% 25.60/3.79 cnf(p1462, plain, (apart_point_and_line(intersection_point(sk1,sk0),sk1) | ~spl196), inference(avatar_component_clause, [status(thm)], [sdef196])).
% 25.60/3.79 cnf(p282, plain, ~apart_point_and_line(X0,sk1) | distinct_points(X0,intersection_point(sk1,sk0)), inference(resolution, [status(thm)], [p277, c8])).
% 25.60/3.79 cnf(p1491, plain, (distinct_points(intersection_point(sk1,sk0),intersection_point(sk1,sk0)) | ~spl196), inference(resolution, [status(thm)], [p1462, p282])).
% 25.60/3.79 cnf(p1523, plain, ($false | ~spl196), inference(resolution, [status(thm)], [p1491, c0])).
% 25.60/3.79 cnf(sct13, plain, (~spl196), inference(avatar_contradiction_clause, [status(thm)], [p1523])).
% 25.60/3.79 cnf(p45, plain, ~apart_point_and_line(X0,sk2) | distinct_points(X0,intersection_point(sk2,sk1)), inference(resolution, [status(thm)], [c8, c15])).
% 25.60/3.79 cnf(c17, plain, apart_point_and_line(intersection_point(sk0,sk1),sk2), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 25.60/3.79 cnf(p54, plain, distinct_points(intersection_point(sk0,sk1),intersection_point(sk2,sk1)), inference(resolution, [status(thm)], [p45, c17])).
% 25.60/3.79 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)).
% 25.60/3.79 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])).
% 25.60/3.79 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])).
% 25.60/3.79 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])).
% 25.60/3.79 cnf(p56, plain, ~apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | distinct_points(X0,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [p54, c6])).
% 25.60/3.79 fof(f10, axiom, ! [X,Y,Z] : ( apart_point_and_line(X,Y) => ( distinct_lines(Y,Z) | apart_point_and_line(X,Z) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ceq2)).
% 25.60/3.79 fof(f10_nnf, plain, ! [X,Y,Z] : ((~(apart_point_and_line(X,Y)) | (distinct_lines(Y,Z) | apart_point_and_line(X,Z)))), inference(nnf_transformation, [status(thm)], [f10])).
% 25.60/3.79 fof(f10_sk, plain, ! [X,Y,Z] : ((~(apart_point_and_line(X,Y)) | (distinct_lines(Y,Z) | apart_point_and_line(X,Z)))), inference(skolemisation, [status(esa)], [f10_nnf])).
% 25.60/3.79 cnf(c12, plain, ~apart_point_and_line(X0,X1) | distinct_lines(X1,X2) | apart_point_and_line(X0,X2), inference(cnf_transformation, [status(esa)], [f10_sk])).
% 25.60/3.79 cnf(p93, plain, distinct_lines(sk2,X0) | apart_point_and_line(intersection_point(sk0,sk1),X0), inference(resolution, [status(thm)], [c12, c17])).
% 25.60/3.79 cnf(p311, plain, distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)) | distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))), inference(resolution, [status(thm)], [p56, p93])).
% 25.60/3.79 fof(sdef1, definition, (spl1 <=> (distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 25.60/3.79 cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [p311, sdef0, sdef1])).
% 25.60/3.79 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)).
% 25.60/3.79 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])).
% 25.60/3.79 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])).
% 25.60/3.79 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])).
% 25.60/3.79 cnf(p68, 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(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [c10, p54])).
% 25.60/3.79 fof(f11, axiom, ! [X,Y] : ( convergent_lines(X,Y) => distinct_lines(X,Y) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ceq3)).
% 25.60/3.79 fof(f11_nnf, plain, ! [X,Y] : ((~(convergent_lines(X,Y)) | distinct_lines(X,Y))), inference(nnf_transformation, [status(thm)], [f11])).
% 25.60/3.79 fof(f11_sk, plain, ! [X,Y] : ((~(convergent_lines(X,Y)) | distinct_lines(X,Y))), inference(skolemisation, [status(esa)], [f11_nnf])).
% 25.60/3.79 cnf(c13, plain, ~convergent_lines(X0,X1) | distinct_lines(X0,X1), inference(cnf_transformation, [status(esa)], [f11_sk])).
% 25.60/3.79 cnf(p19, plain, distinct_lines(sk0,sk1), inference(resolution, [status(thm)], [c13, c14])).
% 25.60/3.79 cnf(p444, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),sk1), inference(resolution, [status(thm)], [p68, p19])).
% 25.60/3.79 fof(sdef4, definition, (spl4 <=> (apart_point_and_line(intersection_point(sk2,sk1),sk0))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 25.60/3.79 cnf(ssp1, plain, (spl2 | spl3 | spl4 | spl5), inference(avatar_split_clause, [status(thm)], [p444, sdef2, sdef3, sdef4, sdef5])).
% 25.60/3.79 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)).
% 25.60/3.79 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])).
% 25.60/3.79 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])).
% 25.60/3.79 cnf(c4, plain, ~distinct_lines(X0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 25.60/3.79 cnf(p22, plain, distinct_lines(sk0,X0) | distinct_lines(sk1,X0), inference(resolution, [status(thm)], [c4, p19])).
% 25.60/3.79 cnf(p449, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk0,X0), inference(resolution, [status(thm)], [p68, p22])).
% 25.60/3.79 fof(sdef6, definition, (spl6 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 25.60/3.79 cnf(ssp2, plain, (spl3 | spl5 | spl6), inference(avatar_split_clause, [status(thm)], [p449, sdef3, sdef5, sdef6])).
% 25.60/3.79 cnf(p28, plain, distinct_lines(sk0,X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p22, c4])).
% 25.60/3.79 cnf(p451, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p68, p28])).
% 25.60/3.79 fof(sdef7, definition, (spl7 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 25.60/3.79 cnf(ssp3, plain, (spl2 | spl4 | spl7), inference(avatar_split_clause, [status(thm)], [p451, sdef2, sdef4, sdef7])).
% 25.60/3.79 cnf(p453, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p68, p28])).
% 25.60/3.79 fof(sdef8, definition, (spl8 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 25.60/3.79 cnf(ssp4, plain, (spl3 | spl5 | spl8), inference(avatar_split_clause, [status(thm)], [p453, sdef3, sdef5, sdef8])).
% 25.60/3.79 cnf(p455, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | distinct_lines(sk0,X0) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p68, p28])).
% 25.60/3.79 fof(sdef9, definition, (spl9 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk1,X0))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 25.60/3.79 cnf(ssp5, plain, (spl6 | spl9), inference(avatar_split_clause, [status(thm)], [p455, sdef6, sdef9])).
% 25.60/3.79 cnf(p84, plain, distinct_lines(sk0,X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p28, c1])).
% 25.60/3.79 cnf(p457, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p68, p84])).
% 25.60/3.79 fof(sdef10, definition, (spl10 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X0,sk1))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 25.60/3.79 cnf(ssp6, plain, (spl2 | spl4 | spl10), inference(avatar_split_clause, [status(thm)], [p457, sdef2, sdef4, sdef10])).
% 25.60/3.79 cnf(p20, plain, distinct_lines(sk2,sk1), inference(resolution, [status(thm)], [c13, c15])).
% 25.60/3.79 cnf(p23, plain, distinct_lines(sk2,X0) | distinct_lines(sk1,X0), inference(resolution, [status(thm)], [c4, p20])).
% 25.60/3.79 cnf(p30, plain, distinct_lines(sk1,X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p23, c4])).
% 25.60/3.79 cnf(p459, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p68, p30])).
% 25.60/3.79 fof(sdef11, definition, (spl11 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 25.60/3.79 cnf(ssp7, plain, (spl3 | spl5 | spl11), inference(avatar_split_clause, [status(thm)], [p459, sdef3, sdef5, sdef11])).
% 25.60/3.79 cnf(p89, plain, distinct_lines(sk1,X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p30, c1])).
% 25.60/3.79 cnf(p461, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p68, p89])).
% 25.60/3.79 fof(sdef12, definition, (spl12 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X0,sk2))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 25.60/3.79 cnf(ssp8, plain, (spl3 | spl5 | spl12), inference(avatar_split_clause, [status(thm)], [p461, sdef3, sdef5, sdef12])).
% 25.60/3.79 cnf(p21, plain, distinct_lines(sk0,sk2), inference(resolution, [status(thm)], [c13, c16])).
% 25.60/3.79 cnf(p24, plain, distinct_lines(sk0,X0) | distinct_lines(sk2,X0), inference(resolution, [status(thm)], [c4, p21])).
% 25.60/3.79 cnf(p31, plain, distinct_lines(sk0,X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p24, c4])).
% 25.60/3.79 cnf(p463, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p68, p31])).
% 25.60/3.79 cnf(ssp9, plain, (spl2 | spl4 | spl11), inference(avatar_split_clause, [status(thm)], [p463, sdef2, sdef4, sdef11])).
% 25.60/3.79 cnf(p97, plain, distinct_lines(sk0,X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p31, c1])).
% 25.60/3.79 cnf(p464, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p68, p97])).
% 25.60/3.79 cnf(ssp10, plain, (spl2 | spl4 | spl12), inference(avatar_split_clause, [status(thm)], [p464, sdef2, sdef4, sdef12])).
% 25.60/3.79 cnf(p32, plain, convergent_lines(sk0,X0) | distinct_lines(sk1,X0), inference(resolution, [status(thm)], [p25, c13])).
% 25.60/3.79 cnf(p40, plain, distinct_lines(sk1,X0) | convergent_lines(sk0,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p32, c5])).
% 25.60/3.79 cnf(p172, plain, distinct_lines(sk1,X0) | convergent_lines(X0,sk0), inference(resolution, [status(thm)], [p40, c2])).
% 25.60/3.79 cnf(p186, plain, distinct_lines(sk1,X0) | distinct_lines(X0,sk0), inference(resolution, [status(thm)], [p172, c13])).
% 25.60/3.79 cnf(p465, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X0,sk0), inference(resolution, [status(thm)], [p68, p186])).
% 25.60/3.79 fof(sdef13, definition, (spl13 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X0,sk0))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 25.60/3.79 cnf(ssp11, plain, (spl3 | spl5 | spl13), inference(avatar_split_clause, [status(thm)], [p465, sdef3, sdef5, sdef13])).
% 25.60/3.79 cnf(p467, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | distinct_lines(sk1,X0), inference(resolution, [status(thm)], [p68, p186])).
% 25.60/3.79 cnf(ssp12, plain, (spl2 | spl4 | spl9), inference(avatar_split_clause, [status(thm)], [p467, sdef2, sdef4, sdef9])).
% 25.60/3.79 cnf(p88, plain, distinct_lines(X0,sk1) | distinct_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p84, c4])).
% 25.60/3.79 cnf(p468, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | distinct_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p68, p88])).
% 25.60/3.79 fof(sdef14, definition, (spl14 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 25.60/3.79 cnf(ssp13, plain, (spl3 | spl5 | spl14), inference(avatar_split_clause, [status(thm)], [p468, sdef3, sdef5, sdef14])).
% 25.60/3.79 cnf(p470, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p68, p88])).
% 25.60/3.79 fof(sdef15, definition, (spl15 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 25.60/3.79 cnf(ssp14, plain, (spl2 | spl4 | spl15), inference(avatar_split_clause, [status(thm)], [p470, sdef2, sdef4, sdef15])).
% 25.60/3.79 cnf(p472, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | distinct_lines(X0,sk1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p68, p88])).
% 25.60/3.79 cnf(ssp15, plain, (spl6 | spl10), inference(avatar_split_clause, [status(thm)], [p472, sdef6, sdef10])).
% 25.60/3.79 cnf(p94, plain, distinct_lines(X0,sk2) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p89, c4])).
% 25.60/3.79 cnf(p473, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p68, p94])).
% 25.60/3.79 fof(sdef16, definition, (spl16 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 25.60/3.79 cnf(ssp16, plain, (spl3 | spl5 | spl16), inference(avatar_split_clause, [status(thm)], [p473, sdef3, sdef5, sdef16])).
% 25.60/3.79 cnf(p475, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | distinct_lines(X0,sk2) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p68, p94])).
% 25.60/3.79 cnf(ssp17, plain, (spl9 | spl12), inference(avatar_split_clause, [status(thm)], [p475, sdef9, sdef12])).
% 25.60/3.79 cnf(p101, plain, distinct_lines(X0,sk2) | distinct_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p97, c4])).
% 25.60/3.79 cnf(p476, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p68, p101])).
% 25.60/3.79 cnf(ssp18, plain, (spl2 | spl4 | spl16), inference(avatar_split_clause, [status(thm)], [p476, sdef2, sdef4, sdef16])).
% 25.60/3.79 cnf(p477, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | distinct_lines(X0,sk2) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p68, p101])).
% 25.60/3.79 cnf(ssp19, plain, (spl6 | spl12), inference(avatar_split_clause, [status(thm)], [p477, sdef6, sdef12])).
% 25.60/3.79 cnf(p105, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p33, c13])).
% 25.60/3.79 cnf(p478, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | convergent_lines(sk0,X0) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p68, p105])).
% 25.60/3.79 fof(sdef17, definition, (spl17 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 25.60/3.79 fof(sdef18, definition, (spl18 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(sk1,X0))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 25.60/3.79 cnf(ssp20, plain, (spl17 | spl18), inference(avatar_split_clause, [status(thm)], [p478, sdef17, sdef18])).
% 25.60/3.79 cnf(p36, plain, convergent_lines(sk1,X0) | convergent_lines(sk2,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p26, c5])).
% 25.60/3.79 cnf(p130, plain, convergent_lines(sk1,X0) | convergent_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p36, c13])).
% 25.60/3.79 cnf(p481, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | convergent_lines(sk1,X0) | convergent_lines(sk2,X1), inference(resolution, [status(thm)], [p68, p130])).
% 25.60/3.79 fof(sdef19, definition, (spl19 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 25.60/3.79 cnf(ssp21, plain, (spl18 | spl19), inference(avatar_split_clause, [status(thm)], [p481, sdef18, sdef19])).
% 25.60/3.79 cnf(p27, plain, convergent_lines(sk0,X0) | convergent_lines(sk2,X0), inference(resolution, [status(thm)], [c5, c16])).
% 25.60/3.79 cnf(p38, plain, convergent_lines(sk0,X0) | convergent_lines(sk2,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p27, c5])).
% 25.60/3.79 cnf(p143, plain, convergent_lines(sk0,X0) | convergent_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p38, c13])).
% 25.60/3.79 cnf(p483, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | convergent_lines(sk0,X0) | convergent_lines(sk2,X1), inference(resolution, [status(thm)], [p68, p143])).
% 25.60/3.79 cnf(ssp22, plain, (spl17 | spl19), inference(avatar_split_clause, [status(thm)], [p483, sdef17, sdef19])).
% 25.60/3.79 cnf(p174, plain, distinct_lines(sk1,X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p40, c13])).
% 25.60/3.79 cnf(p484, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p68, p174])).
% 25.60/3.79 fof(sdef20, definition, (spl20 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 25.60/3.79 cnf(ssp23, plain, (spl3 | spl5 | spl20), inference(avatar_split_clause, [status(thm)], [p484, sdef3, sdef5, sdef20])).
% 25.60/3.79 cnf(p486, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | distinct_lines(sk1,X0) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p68, p174])).
% 25.60/3.79 cnf(ssp24, plain, (spl9 | spl17), inference(avatar_split_clause, [status(thm)], [p486, sdef9, sdef17])).
% 25.60/3.79 cnf(p189, plain, distinct_lines(X0,sk0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p186, c4])).
% 25.60/3.79 cnf(p487, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p68, p189])).
% 25.60/3.79 fof(sdef21, definition, (spl21 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 25.60/3.79 cnf(ssp25, plain, (spl3 | spl5 | spl21), inference(avatar_split_clause, [status(thm)], [p487, sdef3, sdef5, sdef21])).
% 25.60/3.79 cnf(p489, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | distinct_lines(X0,sk0) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p68, p189])).
% 25.60/3.79 cnf(ssp26, plain, (spl9 | spl13), inference(avatar_split_clause, [status(thm)], [p489, sdef9, sdef13])).
% 25.60/3.79 cnf(p190, plain, distinct_lines(sk1,X0) | distinct_lines(X0,X1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p186, c4])).
% 25.60/3.79 cnf(p490, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p68, p190])).
% 25.60/3.79 fof(sdef22, definition, (spl22 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 25.60/3.79 cnf(ssp27, plain, (spl2 | spl4 | spl22), inference(avatar_split_clause, [status(thm)], [p490, sdef2, sdef4, sdef22])).
% 25.60/3.79 cnf(p447, plain, (apart_point_and_line(intersection_point(sk2,sk1),sk0) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 25.60/3.79 cnf(p64, plain, ~apart_point_and_line(X0,X1) | distinct_points(X0,intersection_point(sk2,X1)) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [c9, p27])).
% 25.60/3.79 cnf(p511, plain, (distinct_points(intersection_point(sk2,sk1),intersection_point(sk2,sk0)) | convergent_lines(sk0,sk0) | ~spl4), inference(resolution, [status(thm)], [p447, p64])).
% 25.60/3.79 fof(sdef23, definition, (spl23 <=> (distinct_points(intersection_point(sk2,sk1),intersection_point(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 25.60/3.79 cnf(ssp28, plain, (~spl4 | spl23 | spl24), inference(avatar_split_clause, [status(thm)], [p511, sdef23, sdef24])).
% 25.60/3.79 cnf(p60, plain, ~apart_point_and_line(X0,sk2) | distinct_points(X0,intersection_point(sk0,sk2)), inference(resolution, [status(thm)], [c9, c16])).
% 25.60/3.79 cnf(p69, plain, distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk2)), inference(resolution, [status(thm)], [p60, c17])).
% 25.60/3.79 cnf(p71, plain, ~apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | distinct_points(X0,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [p69, c6])).
% 25.60/3.79 cnf(p516, plain, distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)) | distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))), inference(resolution, [status(thm)], [p71, p93])).
% 25.60/3.79 fof(sdef25, definition, (spl25 <=> (distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 25.60/3.79 cnf(ssp29, plain, (spl0 | spl25), inference(avatar_split_clause, [status(thm)], [p516, sdef0, sdef25])).
% 25.60/3.79 cnf(p73, 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(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p69, c10])).
% 25.60/3.79 cnf(p542, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),sk1), inference(resolution, [status(thm)], [p73, p19])).
% 25.60/3.79 fof(sdef27, definition, (spl27 <=> (apart_point_and_line(intersection_point(sk0,sk2),sk1))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 25.60/3.79 cnf(ssp30, plain, (spl2 | spl3 | spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p542, sdef2, sdef3, sdef26, sdef27])).
% 25.60/3.79 cnf(p545, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(sk0,X0), inference(resolution, [status(thm)], [p73, p22])).
% 25.60/3.79 fof(sdef28, definition, (spl28 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 25.60/3.79 cnf(ssp31, plain, (spl3 | spl27 | spl28), inference(avatar_split_clause, [status(thm)], [p545, sdef3, sdef27, sdef28])).
% 25.60/3.79 cnf(p547, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p73, p28])).
% 25.60/3.79 fof(sdef29, definition, (spl29 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 25.60/3.79 cnf(ssp32, plain, (spl2 | spl26 | spl29), inference(avatar_split_clause, [status(thm)], [p547, sdef2, sdef26, sdef29])).
% 25.60/3.79 cnf(p549, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p73, p28])).
% 25.60/3.79 fof(sdef30, definition, (spl30 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 25.60/3.79 cnf(ssp33, plain, (spl3 | spl27 | spl30), inference(avatar_split_clause, [status(thm)], [p549, sdef3, sdef27, sdef30])).
% 25.60/3.79 cnf(p551, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | distinct_lines(sk0,X0) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p73, p28])).
% 25.60/3.79 fof(sdef31, definition, (spl31 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(sk1,X0))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 25.60/3.79 cnf(ssp34, plain, (spl28 | spl31), inference(avatar_split_clause, [status(thm)], [p551, sdef28, sdef31])).
% 25.60/3.79 cnf(p553, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p73, p84])).
% 25.60/3.79 fof(sdef32, definition, (spl32 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X0,sk1))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 25.60/3.79 cnf(ssp35, plain, (spl2 | spl26 | spl32), inference(avatar_split_clause, [status(thm)], [p553, sdef2, sdef26, sdef32])).
% 25.60/3.79 cnf(p555, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p73, p30])).
% 25.60/3.79 fof(sdef33, definition, (spl33 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 25.60/3.79 cnf(ssp36, plain, (spl3 | spl27 | spl33), inference(avatar_split_clause, [status(thm)], [p555, sdef3, sdef27, sdef33])).
% 25.60/3.79 cnf(p557, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p73, p89])).
% 25.60/3.79 fof(sdef34, definition, (spl34 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X0,sk2))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 25.60/3.79 cnf(ssp37, plain, (spl3 | spl27 | spl34), inference(avatar_split_clause, [status(thm)], [p557, sdef3, sdef27, sdef34])).
% 25.60/3.79 cnf(p559, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p73, p31])).
% 25.60/3.79 cnf(ssp38, plain, (spl2 | spl26 | spl33), inference(avatar_split_clause, [status(thm)], [p559, sdef2, sdef26, sdef33])).
% 25.60/3.79 cnf(p560, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p73, p97])).
% 25.60/3.79 cnf(ssp39, plain, (spl2 | spl26 | spl34), inference(avatar_split_clause, [status(thm)], [p560, sdef2, sdef26, sdef34])).
% 25.60/3.79 cnf(p561, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X0,sk0), inference(resolution, [status(thm)], [p73, p186])).
% 25.60/3.79 fof(sdef35, definition, (spl35 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X0,sk0))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 25.60/3.79 cnf(ssp40, plain, (spl3 | spl27 | spl35), inference(avatar_split_clause, [status(thm)], [p561, sdef3, sdef27, sdef35])).
% 25.60/3.79 cnf(p563, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | distinct_lines(sk1,X0), inference(resolution, [status(thm)], [p73, p186])).
% 25.60/3.79 cnf(ssp41, plain, (spl2 | spl26 | spl31), inference(avatar_split_clause, [status(thm)], [p563, sdef2, sdef26, sdef31])).
% 25.60/3.79 cnf(p564, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | distinct_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p73, p88])).
% 25.60/3.79 fof(sdef36, definition, (spl36 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 25.60/3.79 cnf(ssp42, plain, (spl3 | spl27 | spl36), inference(avatar_split_clause, [status(thm)], [p564, sdef3, sdef27, sdef36])).
% 25.60/3.79 cnf(p566, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p73, p88])).
% 25.60/3.79 fof(sdef37, definition, (spl37 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 25.60/3.79 cnf(ssp43, plain, (spl2 | spl26 | spl37), inference(avatar_split_clause, [status(thm)], [p566, sdef2, sdef26, sdef37])).
% 25.60/3.79 cnf(p568, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | distinct_lines(X0,sk1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p73, p88])).
% 25.60/3.79 cnf(ssp44, plain, (spl28 | spl32), inference(avatar_split_clause, [status(thm)], [p568, sdef28, sdef32])).
% 25.60/3.79 cnf(p569, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p73, p94])).
% 25.60/3.79 fof(sdef38, definition, (spl38 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 25.60/3.79 cnf(ssp45, plain, (spl3 | spl27 | spl38), inference(avatar_split_clause, [status(thm)], [p569, sdef3, sdef27, sdef38])).
% 25.60/3.79 cnf(p571, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | distinct_lines(X0,sk2) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p73, p94])).
% 25.60/3.79 cnf(ssp46, plain, (spl31 | spl34), inference(avatar_split_clause, [status(thm)], [p571, sdef31, sdef34])).
% 25.60/3.79 cnf(p572, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p73, p101])).
% 25.60/3.79 cnf(ssp47, plain, (spl2 | spl26 | spl38), inference(avatar_split_clause, [status(thm)], [p572, sdef2, sdef26, sdef38])).
% 25.60/3.79 cnf(p573, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | distinct_lines(X0,sk2) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p73, p101])).
% 25.60/3.79 cnf(ssp48, plain, (spl28 | spl34), inference(avatar_split_clause, [status(thm)], [p573, sdef28, sdef34])).
% 25.60/3.79 cnf(p574, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | convergent_lines(sk0,X0) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p73, p105])).
% 25.60/3.79 fof(sdef39, definition, (spl39 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | convergent_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 25.60/3.79 fof(sdef40, definition, (spl40 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | convergent_lines(sk1,X0))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 25.60/3.79 cnf(ssp49, plain, (spl39 | spl40), inference(avatar_split_clause, [status(thm)], [p574, sdef39, sdef40])).
% 25.60/3.79 cnf(p577, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | convergent_lines(sk1,X0) | convergent_lines(sk2,X1), inference(resolution, [status(thm)], [p73, p130])).
% 25.60/3.79 fof(sdef41, definition, (spl41 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | convergent_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 25.60/3.79 cnf(ssp50, plain, (spl40 | spl41), inference(avatar_split_clause, [status(thm)], [p577, sdef40, sdef41])).
% 25.60/3.79 cnf(p579, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | convergent_lines(sk0,X0) | convergent_lines(sk2,X1), inference(resolution, [status(thm)], [p73, p143])).
% 25.60/3.79 cnf(ssp51, plain, (spl39 | spl41), inference(avatar_split_clause, [status(thm)], [p579, sdef39, sdef41])).
% 25.60/3.79 cnf(p580, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p73, p174])).
% 25.60/3.79 fof(sdef42, definition, (spl42 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 25.60/3.79 cnf(ssp52, plain, (spl3 | spl27 | spl42), inference(avatar_split_clause, [status(thm)], [p580, sdef3, sdef27, sdef42])).
% 25.60/3.79 cnf(p582, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | distinct_lines(sk1,X0) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p73, p174])).
% 25.60/3.79 cnf(ssp53, plain, (spl31 | spl39), inference(avatar_split_clause, [status(thm)], [p582, sdef31, sdef39])).
% 25.60/3.79 cnf(p583, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p73, p189])).
% 25.60/3.79 fof(sdef43, definition, (spl43 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 25.60/3.79 cnf(ssp54, plain, (spl3 | spl27 | spl43), inference(avatar_split_clause, [status(thm)], [p583, sdef3, sdef27, sdef43])).
% 25.60/3.79 cnf(p585, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | distinct_lines(X0,sk0) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p73, p189])).
% 25.60/3.79 cnf(ssp55, plain, (spl31 | spl35), inference(avatar_split_clause, [status(thm)], [p585, sdef31, sdef35])).
% 25.60/3.79 cnf(p586, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p73, p190])).
% 25.60/3.79 fof(sdef44, definition, (spl44 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 25.60/3.79 cnf(ssp56, plain, (spl2 | spl26 | spl44), inference(avatar_split_clause, [status(thm)], [p586, sdef2, sdef26, sdef44])).
% 25.60/3.79 cnf(p595, plain, (distinct_points(intersection_point(sk0,sk2),intersection_point(sk2,sk0)) | convergent_lines(sk0,sk0) | ~spl26), inference(resolution, [status(thm)], [p543, p64])).
% 25.60/3.79 fof(sdef45, definition, (spl45 <=> (distinct_points(intersection_point(sk0,sk2),intersection_point(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 25.60/3.79 cnf(ssp57, plain, (~spl26 | spl24 | spl45), inference(avatar_split_clause, [status(thm)], [p595, sdef24, sdef45])).
% 25.60/3.79 cnf(p63, plain, ~apart_point_and_line(X0,sk2) | distinct_points(X0,intersection_point(sk1,sk2)), inference(resolution, [status(thm)], [c9, p34])).
% 25.60/3.79 cnf(p74, plain, distinct_points(intersection_point(sk0,sk1),intersection_point(sk1,sk2)), inference(resolution, [status(thm)], [p63, c17])).
% 25.60/3.79 cnf(p76, plain, ~apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | distinct_points(X0,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [p74, c6])).
% 25.60/3.79 cnf(p614, plain, distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)) | distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))), inference(resolution, [status(thm)], [p76, p93])).
% 25.60/3.79 fof(sdef46, definition, (spl46 <=> (distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 25.60/3.79 cnf(ssp58, plain, (spl0 | spl46), inference(avatar_split_clause, [status(thm)], [p614, sdef0, sdef46])).
% 25.60/3.79 cnf(p78, 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(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p74, c10])).
% 25.60/3.79 cnf(p636, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),sk1), inference(resolution, [status(thm)], [p78, p19])).
% 25.60/3.79 fof(sdef47, definition, (spl47 <=> (apart_point_and_line(intersection_point(sk1,sk2),sk0))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 25.60/3.79 cnf(ssp59, plain, (spl2 | spl3 | spl47 | spl48), inference(avatar_split_clause, [status(thm)], [p636, sdef2, sdef3, sdef47, sdef48])).
% 25.60/3.79 cnf(p639, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk0,X0), inference(resolution, [status(thm)], [p78, p22])).
% 25.60/3.79 fof(sdef49, definition, (spl49 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 25.60/3.79 cnf(ssp60, plain, (spl3 | spl48 | spl49), inference(avatar_split_clause, [status(thm)], [p639, sdef3, sdef48, sdef49])).
% 25.60/3.79 cnf(p641, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p78, p28])).
% 25.60/3.79 fof(sdef50, definition, (spl50 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 25.60/3.79 cnf(ssp61, plain, (spl2 | spl47 | spl50), inference(avatar_split_clause, [status(thm)], [p641, sdef2, sdef47, sdef50])).
% 25.60/3.79 cnf(p643, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p78, p28])).
% 25.60/3.79 fof(sdef51, definition, (spl51 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 25.60/3.79 cnf(ssp62, plain, (spl3 | spl48 | spl51), inference(avatar_split_clause, [status(thm)], [p643, sdef3, sdef48, sdef51])).
% 25.60/3.79 cnf(p645, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | distinct_lines(sk0,X0) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p78, p28])).
% 25.60/3.79 fof(sdef52, definition, (spl52 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk1,X0))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 25.60/3.79 cnf(ssp63, plain, (spl49 | spl52), inference(avatar_split_clause, [status(thm)], [p645, sdef49, sdef52])).
% 25.60/3.79 cnf(p647, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p78, p84])).
% 25.60/3.79 fof(sdef53, definition, (spl53 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X0,sk1))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 25.60/3.79 cnf(ssp64, plain, (spl2 | spl47 | spl53), inference(avatar_split_clause, [status(thm)], [p647, sdef2, sdef47, sdef53])).
% 25.60/3.79 cnf(p649, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p78, p30])).
% 25.60/3.79 fof(sdef54, definition, (spl54 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 25.60/3.79 cnf(ssp65, plain, (spl3 | spl48 | spl54), inference(avatar_split_clause, [status(thm)], [p649, sdef3, sdef48, sdef54])).
% 25.60/3.79 cnf(p651, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p78, p89])).
% 25.60/3.79 fof(sdef55, definition, (spl55 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X0,sk2))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 25.60/3.79 cnf(ssp66, plain, (spl3 | spl48 | spl55), inference(avatar_split_clause, [status(thm)], [p651, sdef3, sdef48, sdef55])).
% 25.60/3.79 cnf(p653, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p78, p31])).
% 25.60/3.79 cnf(ssp67, plain, (spl2 | spl47 | spl54), inference(avatar_split_clause, [status(thm)], [p653, sdef2, sdef47, sdef54])).
% 25.60/3.79 cnf(p654, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p78, p97])).
% 25.60/3.79 cnf(ssp68, plain, (spl2 | spl47 | spl55), inference(avatar_split_clause, [status(thm)], [p654, sdef2, sdef47, sdef55])).
% 25.60/3.79 cnf(p655, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X0,sk0), inference(resolution, [status(thm)], [p78, p186])).
% 25.60/3.79 fof(sdef56, definition, (spl56 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X0,sk0))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 25.60/3.79 cnf(ssp69, plain, (spl3 | spl48 | spl56), inference(avatar_split_clause, [status(thm)], [p655, sdef3, sdef48, sdef56])).
% 25.60/3.79 cnf(p657, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | distinct_lines(sk1,X0), inference(resolution, [status(thm)], [p78, p186])).
% 25.60/3.79 cnf(ssp70, plain, (spl2 | spl47 | spl52), inference(avatar_split_clause, [status(thm)], [p657, sdef2, sdef47, sdef52])).
% 25.60/3.79 cnf(p658, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | distinct_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p78, p88])).
% 25.60/3.79 fof(sdef57, definition, (spl57 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 25.60/3.79 cnf(ssp71, plain, (spl3 | spl48 | spl57), inference(avatar_split_clause, [status(thm)], [p658, sdef3, sdef48, sdef57])).
% 25.60/3.79 cnf(p660, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p78, p88])).
% 25.60/3.79 fof(sdef58, definition, (spl58 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 25.60/3.79 cnf(ssp72, plain, (spl2 | spl47 | spl58), inference(avatar_split_clause, [status(thm)], [p660, sdef2, sdef47, sdef58])).
% 25.60/3.79 cnf(p662, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | distinct_lines(X0,sk1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p78, p88])).
% 25.60/3.79 cnf(ssp73, plain, (spl49 | spl53), inference(avatar_split_clause, [status(thm)], [p662, sdef49, sdef53])).
% 25.60/3.79 cnf(p663, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p78, p94])).
% 25.60/3.79 fof(sdef59, definition, (spl59 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 25.60/3.79 cnf(ssp74, plain, (spl3 | spl48 | spl59), inference(avatar_split_clause, [status(thm)], [p663, sdef3, sdef48, sdef59])).
% 25.60/3.79 cnf(p665, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | distinct_lines(X0,sk2) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p78, p94])).
% 25.60/3.79 cnf(ssp75, plain, (spl52 | spl55), inference(avatar_split_clause, [status(thm)], [p665, sdef52, sdef55])).
% 25.60/3.79 cnf(p666, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p78, p101])).
% 25.60/3.79 cnf(ssp76, plain, (spl2 | spl47 | spl59), inference(avatar_split_clause, [status(thm)], [p666, sdef2, sdef47, sdef59])).
% 25.60/3.79 cnf(p667, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | distinct_lines(X0,sk2) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p78, p101])).
% 25.60/3.79 cnf(ssp77, plain, (spl49 | spl55), inference(avatar_split_clause, [status(thm)], [p667, sdef49, sdef55])).
% 25.60/3.79 cnf(p668, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | convergent_lines(sk0,X0) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p78, p105])).
% 25.60/3.79 fof(sdef60, definition, (spl60 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 25.60/3.79 fof(sdef61, definition, (spl61 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(sk1,X0))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 25.60/3.79 cnf(ssp78, plain, (spl60 | spl61), inference(avatar_split_clause, [status(thm)], [p668, sdef60, sdef61])).
% 25.60/3.79 cnf(p671, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | convergent_lines(sk1,X0) | convergent_lines(sk2,X1), inference(resolution, [status(thm)], [p78, p130])).
% 25.60/3.79 fof(sdef62, definition, (spl62 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 25.60/3.79 cnf(ssp79, plain, (spl61 | spl62), inference(avatar_split_clause, [status(thm)], [p671, sdef61, sdef62])).
% 25.60/3.79 cnf(p673, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | convergent_lines(sk0,X0) | convergent_lines(sk2,X1), inference(resolution, [status(thm)], [p78, p143])).
% 25.60/3.79 cnf(ssp80, plain, (spl60 | spl62), inference(avatar_split_clause, [status(thm)], [p673, sdef60, sdef62])).
% 25.60/3.79 cnf(p674, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p78, p174])).
% 25.60/3.79 fof(sdef63, definition, (spl63 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 25.60/3.79 cnf(ssp81, plain, (spl3 | spl48 | spl63), inference(avatar_split_clause, [status(thm)], [p674, sdef3, sdef48, sdef63])).
% 25.60/3.79 cnf(p676, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | distinct_lines(sk1,X0) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p78, p174])).
% 25.60/3.79 cnf(ssp82, plain, (spl52 | spl60), inference(avatar_split_clause, [status(thm)], [p676, sdef52, sdef60])).
% 25.60/3.79 cnf(p677, plain, apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p78, p189])).
% 25.60/3.79 fof(sdef64, definition, (spl64 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 25.60/3.79 cnf(ssp83, plain, (spl3 | spl48 | spl64), inference(avatar_split_clause, [status(thm)], [p677, sdef3, sdef48, sdef64])).
% 25.60/3.79 cnf(p679, plain, apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | distinct_lines(X0,sk0) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p78, p189])).
% 25.60/3.79 cnf(ssp84, plain, (spl52 | spl56), inference(avatar_split_clause, [status(thm)], [p679, sdef52, sdef56])).
% 25.60/3.79 cnf(p680, plain, apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p78, p190])).
% 25.60/3.79 fof(sdef65, definition, (spl65 <=> (apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 25.60/3.79 cnf(ssp85, plain, (spl2 | spl47 | spl65), inference(avatar_split_clause, [status(thm)], [p680, sdef2, sdef47, sdef65])).
% 25.60/3.79 cnf(p637, plain, (apart_point_and_line(intersection_point(sk1,sk2),sk0) | ~spl47), inference(avatar_component_clause, [status(thm)], [sdef47])).
% 25.60/3.79 cnf(p689, plain, (distinct_points(intersection_point(sk1,sk2),intersection_point(sk2,sk0)) | convergent_lines(sk0,sk0) | ~spl47), inference(resolution, [status(thm)], [p637, p64])).
% 25.60/3.79 fof(sdef66, definition, (spl66 <=> (distinct_points(intersection_point(sk1,sk2),intersection_point(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 25.60/3.79 cnf(ssp86, plain, (~spl47 | spl24 | spl66), inference(avatar_split_clause, [status(thm)], [p689, sdef24, sdef66])).
% 25.60/3.79 fof(f9, axiom, ! [X,Y,Z] : ( apart_point_and_line(X,Y) => ( distinct_points(X,Z) | apart_point_and_line(Z,Y) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ceq1)).
% 25.60/3.79 fof(f9_nnf, plain, ! [X,Y,Z] : ((~(apart_point_and_line(X,Y)) | (distinct_points(X,Z) | apart_point_and_line(Z,Y)))), inference(nnf_transformation, [status(thm)], [f9])).
% 25.60/3.79 fof(f9_sk, plain, ! [X,Y,Z] : ((~(apart_point_and_line(X,Y)) | (distinct_points(X,Z) | apart_point_and_line(Z,Y)))), inference(skolemisation, [status(esa)], [f9_nnf])).
% 25.60/3.79 cnf(c11, plain, ~apart_point_and_line(X0,X1) | distinct_points(X0,X2) | apart_point_and_line(X2,X1), inference(cnf_transformation, [status(esa)], [f9_sk])).
% 25.60/3.79 cnf(p79, plain, distinct_points(intersection_point(sk0,sk1),X0) | apart_point_and_line(X0,sk2), inference(resolution, [status(thm)], [c11, c17])).
% 25.60/3.79 cnf(p81, plain, apart_point_and_line(X0,sk2) | ~apart_point_and_line(X1,line_connecting(intersection_point(sk0,sk1),X0)) | distinct_points(X1,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [p79, c6])).
% 25.60/3.79 cnf(p740, plain, apart_point_and_line(X0,sk2) | distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)) | distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),X0)), inference(resolution, [status(thm)], [p81, p93])).
% 25.60/3.79 fof(sdef67, definition, (spl67 <=> (apart_point_and_line(X0,sk2) | distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),X0)))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 25.60/3.79 cnf(ssp87, plain, (spl0 | spl67), inference(avatar_split_clause, [status(thm)], [p740, sdef0, sdef67])).
% 25.60/3.79 cnf(p507, plain, (distinct_lines(sk0,X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | ~spl4), inference(resolution, [status(thm)], [p447, c12])).
% 25.60/3.79 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])).
% 25.60/3.79 cnf(p57, plain, ~apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | distinct_points(X0,intersection_point(sk2,sk1)), inference(resolution, [status(thm)], [p54, c7])).
% 25.60/3.79 cnf(p749, plain, (distinct_lines(sk0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | distinct_points(intersection_point(sk2,sk1),intersection_point(sk2,sk1)) | ~spl4), inference(resolution, [status(thm)], [p507, p57])).
% 25.60/3.79 fof(sdef68, definition, (spl68 <=> (distinct_lines(sk0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 25.60/3.79 cnf(ssp88, plain, (~spl4 | spl68 | spl69), inference(avatar_split_clause, [status(thm)], [p749, sdef68, sdef69])).
% 25.60/3.79 cnf(p77, plain, ~apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | distinct_points(X0,intersection_point(sk1,sk2)), inference(resolution, [status(thm)], [p74, c7])).
% 25.60/3.79 cnf(p754, plain, (distinct_lines(sk0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | distinct_points(intersection_point(sk2,sk1),intersection_point(sk1,sk2)) | ~spl4), inference(resolution, [status(thm)], [p507, p77])).
% 25.60/3.79 fof(sdef70, definition, (spl70 <=> (distinct_lines(sk0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 25.60/3.79 fof(sdef71, definition, (spl71 <=> (distinct_points(intersection_point(sk2,sk1),intersection_point(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 25.60/3.79 cnf(ssp89, plain, (~spl4 | spl70 | spl71), inference(avatar_split_clause, [status(thm)], [p754, sdef70, sdef71])).
% 25.60/3.79 cnf(p544, plain, (apart_point_and_line(intersection_point(sk0,sk2),sk1) | ~spl27), inference(avatar_component_clause, [status(thm)], [sdef27])).
% 25.60/3.79 cnf(p602, plain, (distinct_lines(sk1,X0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | ~spl27), inference(resolution, [status(thm)], [p544, c12])).
% 25.60/3.79 cnf(p72, plain, ~apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | distinct_points(X0,intersection_point(sk0,sk2)), inference(resolution, [status(thm)], [p69, c7])).
% 25.60/3.79 cnf(p772, plain, (distinct_lines(sk1,line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | distinct_points(intersection_point(sk0,sk2),intersection_point(sk0,sk2)) | ~spl27), inference(resolution, [status(thm)], [p602, p72])).
% 25.60/3.79 fof(sdef72, definition, (spl72 <=> (distinct_lines(sk1,line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 25.60/3.79 cnf(ssp90, plain, (~spl27 | spl72 | spl73), inference(avatar_split_clause, [status(thm)], [p772, sdef72, sdef73])).
% 25.60/3.79 cnf(p83, plain, apart_point_and_line(X0,sk2) | ~distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(X0,X1) | apart_point_and_line(X0,X2), inference(resolution, [status(thm)], [p79, c10])).
% 25.60/3.79 cnf(p776, plain, apart_point_and_line(X0,sk2) | 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), inference(resolution, [status(thm)], [p83, p19])).
% 25.60/3.79 fof(sdef74, definition, (spl74 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,sk1))), introduced(definition, [new_symbols(naming, [spl74])], [avatar_definition])).
% 25.60/3.79 cnf(ssp91, plain, (spl2 | spl3 | spl74), inference(avatar_split_clause, [status(thm)], [p776, sdef2, sdef3, sdef74])).
% 25.60/3.79 cnf(p778, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p83, p22])).
% 25.60/3.79 fof(sdef75, definition, (spl75 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(sk0,X1))), introduced(definition, [new_symbols(naming, [spl75])], [avatar_definition])).
% 25.60/3.79 cnf(ssp92, plain, (spl3 | spl75), inference(avatar_split_clause, [status(thm)], [p778, sdef3, sdef75])).
% 25.60/3.79 cnf(p780, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p83, p28])).
% 25.60/3.79 fof(sdef76, definition, (spl76 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl76])], [avatar_definition])).
% 25.60/3.79 cnf(ssp93, plain, (spl2 | spl76), inference(avatar_split_clause, [status(thm)], [p780, sdef2, sdef76])).
% 25.60/3.79 cnf(p782, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p83, p28])).
% 25.60/3.79 fof(sdef77, definition, (spl77 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X2,X1))), introduced(definition, [new_symbols(naming, [spl77])], [avatar_definition])).
% 25.60/3.79 cnf(ssp94, plain, (spl3 | spl77), inference(avatar_split_clause, [status(thm)], [p782, sdef3, sdef77])).
% 25.60/3.79 cnf(p785, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(X1,sk1), inference(resolution, [status(thm)], [p83, p84])).
% 25.60/3.79 fof(sdef78, definition, (spl78 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(X1,sk1))), introduced(definition, [new_symbols(naming, [spl78])], [avatar_definition])).
% 25.60/3.79 cnf(ssp95, plain, (spl2 | spl78), inference(avatar_split_clause, [status(thm)], [p785, sdef2, sdef78])).
% 25.60/3.79 cnf(p787, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p83, p30])).
% 25.60/3.79 fof(sdef79, definition, (spl79 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl79])], [avatar_definition])).
% 25.60/3.79 cnf(ssp96, plain, (spl3 | spl79), inference(avatar_split_clause, [status(thm)], [p787, sdef3, sdef79])).
% 25.60/3.79 cnf(p789, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(X1,sk2), inference(resolution, [status(thm)], [p83, p89])).
% 25.60/3.79 fof(sdef80, definition, (spl80 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(X1,sk2))), introduced(definition, [new_symbols(naming, [spl80])], [avatar_definition])).
% 25.60/3.79 cnf(ssp97, plain, (spl3 | spl80), inference(avatar_split_clause, [status(thm)], [p789, sdef3, sdef80])).
% 25.60/3.79 cnf(p791, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p83, p31])).
% 25.60/3.79 fof(sdef81, definition, (spl81 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl81])], [avatar_definition])).
% 25.60/3.79 cnf(ssp98, plain, (spl2 | spl81), inference(avatar_split_clause, [status(thm)], [p791, sdef2, sdef81])).
% 25.60/3.79 cnf(p793, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(X1,sk2), inference(resolution, [status(thm)], [p83, p97])).
% 25.60/3.79 fof(sdef82, definition, (spl82 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(X1,sk2))), introduced(definition, [new_symbols(naming, [spl82])], [avatar_definition])).
% 25.60/3.79 cnf(ssp99, plain, (spl2 | spl82), inference(avatar_split_clause, [status(thm)], [p793, sdef2, sdef82])).
% 25.60/3.79 cnf(p795, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(X1,sk0), inference(resolution, [status(thm)], [p83, p186])).
% 25.60/3.79 fof(sdef83, definition, (spl83 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(X1,sk0))), introduced(definition, [new_symbols(naming, [spl83])], [avatar_definition])).
% 25.60/3.79 cnf(ssp100, plain, (spl3 | spl83), inference(avatar_split_clause, [status(thm)], [p795, sdef3, sdef83])).
% 25.60/3.79 cnf(p797, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(X0,X1) | apart_point_and_line(X0,sk0) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p83, p186])).
% 25.60/3.79 fof(sdef84, definition, (spl84 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,X1) | apart_point_and_line(X0,sk0) | distinct_lines(sk1,X1))), introduced(definition, [new_symbols(naming, [spl84])], [avatar_definition])).
% 25.60/3.79 cnf(ssp101, plain, (spl2 | spl84), inference(avatar_split_clause, [status(thm)], [p797, sdef2, sdef84])).
% 25.60/3.79 cnf(p799, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(X0,X1) | apart_point_and_line(X0,sk1) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p83, p88])).
% 25.60/3.79 fof(sdef85, definition, (spl85 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,X1) | apart_point_and_line(X0,sk1) | distinct_lines(sk0,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl85])], [avatar_definition])).
% 25.60/3.79 cnf(ssp102, plain, (spl3 | spl85), inference(avatar_split_clause, [status(thm)], [p799, sdef3, sdef85])).
% 25.60/3.79 cnf(p801, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(X2,sk1) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p83, p88])).
% 25.60/3.79 fof(sdef86, definition, (spl86 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(X2,sk1) | distinct_lines(X2,X1))), introduced(definition, [new_symbols(naming, [spl86])], [avatar_definition])).
% 25.60/3.79 cnf(ssp103, plain, (spl2 | spl86), inference(avatar_split_clause, [status(thm)], [p801, sdef2, sdef86])).
% 25.60/3.79 cnf(p804, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(X2,sk2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p83, p94])).
% 25.60/3.79 fof(sdef87, definition, (spl87 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(X2,sk2) | distinct_lines(X2,X1))), introduced(definition, [new_symbols(naming, [spl87])], [avatar_definition])).
% 25.60/3.79 cnf(ssp104, plain, (spl3 | spl87), inference(avatar_split_clause, [status(thm)], [p804, sdef3, sdef87])).
% 25.60/3.79 cnf(p807, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(X2,sk2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p83, p101])).
% 25.60/3.79 fof(sdef88, definition, (spl88 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(X2,sk2) | distinct_lines(X2,X1))), introduced(definition, [new_symbols(naming, [spl88])], [avatar_definition])).
% 25.60/3.79 cnf(ssp105, plain, (spl2 | spl88), inference(avatar_split_clause, [status(thm)], [p807, sdef2, sdef88])).
% 25.60/3.79 cnf(p813, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | convergent_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p83, p174])).
% 25.60/3.79 fof(sdef89, definition, (spl89 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | convergent_lines(sk0,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl89])], [avatar_definition])).
% 25.60/3.79 cnf(ssp106, plain, (spl3 | spl89), inference(avatar_split_clause, [status(thm)], [p813, sdef3, sdef89])).
% 25.60/3.79 cnf(p816, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(X2,sk0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p83, p189])).
% 25.60/3.79 fof(sdef90, definition, (spl90 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,X1) | distinct_lines(X2,sk0) | distinct_lines(X2,X1))), introduced(definition, [new_symbols(naming, [spl90])], [avatar_definition])).
% 25.60/3.79 cnf(ssp107, plain, (spl3 | spl90), inference(avatar_split_clause, [status(thm)], [p816, sdef3, sdef90])).
% 25.60/3.79 cnf(p819, plain, apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p83, p190])).
% 25.60/3.79 fof(sdef91, definition, (spl91 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X2,X1))), introduced(definition, [new_symbols(naming, [spl91])], [avatar_definition])).
% 25.60/3.79 cnf(ssp108, plain, (spl2 | spl91), inference(avatar_split_clause, [status(thm)], [p819, sdef2, sdef91])).
% 25.60/3.79 cnf(p685, plain, (distinct_lines(sk0,X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | ~spl47), inference(resolution, [status(thm)], [p637, c12])).
% 25.60/3.79 cnf(p829, plain, (distinct_lines(sk0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | distinct_points(intersection_point(sk1,sk2),intersection_point(sk2,sk1)) | ~spl47), inference(resolution, [status(thm)], [p685, p57])).
% 25.60/3.79 fof(sdef92, definition, (spl92 <=> (distinct_points(intersection_point(sk1,sk2),intersection_point(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl92])], [avatar_definition])).
% 25.60/3.79 cnf(ssp109, plain, (~spl47 | spl68 | spl92), inference(avatar_split_clause, [status(thm)], [p829, sdef68, sdef92])).
% 25.60/3.79 cnf(p833, plain, (distinct_lines(sk0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | distinct_points(intersection_point(sk1,sk2),intersection_point(sk1,sk2)) | ~spl47), inference(resolution, [status(thm)], [p685, p77])).
% 25.60/3.79 cnf(ssp110, plain, (~spl47 | spl70 | spl93), inference(avatar_split_clause, [status(thm)], [p833, sdef70, sdef93])).
% 25.60/3.79 cnf(p85, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p28, c4])).
% 25.60/3.79 cnf(p840, plain, distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p85, p68])).
% 25.60/3.79 fof(sdef94, definition, (spl94 <=> (distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X1))), introduced(definition, [new_symbols(naming, [spl94])], [avatar_definition])).
% 25.60/3.79 cnf(ssp111, plain, (spl3 | spl5 | spl94), inference(avatar_split_clause, [status(thm)], [p840, sdef3, sdef5, sdef94])).
% 25.60/3.79 cnf(p842, plain, distinct_lines(sk1,X0) | distinct_lines(sk0,X1) | distinct_lines(X2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),X0), inference(resolution, [status(thm)], [p85, p68])).
% 25.60/3.79 fof(sdef95, definition, (spl95 <=> (distinct_lines(sk0,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X1))), introduced(definition, [new_symbols(naming, [spl95])], [avatar_definition])).
% 25.60/3.79 cnf(ssp112, plain, (spl9 | spl95), inference(avatar_split_clause, [status(thm)], [p842, sdef9, sdef95])).
% 25.60/3.79 cnf(p844, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X2), inference(resolution, [status(thm)], [p85, p68])).
% 25.60/3.79 fof(sdef96, definition, (spl96 <=> (distinct_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),X2))), introduced(definition, [new_symbols(naming, [spl96])], [avatar_definition])).
% 25.60/3.79 cnf(ssp113, plain, (spl2 | spl4 | spl96), inference(avatar_split_clause, [status(thm)], [p844, sdef2, sdef4, sdef96])).
% 25.60/3.79 cnf(p846, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(sk0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X2), inference(resolution, [status(thm)], [p85, p68])).
% 25.60/3.79 fof(sdef97, definition, (spl97 <=> (distinct_lines(sk1,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X1))), introduced(definition, [new_symbols(naming, [spl97])], [avatar_definition])).
% 25.60/3.79 cnf(ssp114, plain, (spl6 | spl97), inference(avatar_split_clause, [status(thm)], [p846, sdef6, sdef97])).
% 25.60/3.79 cnf(p848, plain, distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p85, p73])).
% 25.60/3.79 fof(sdef98, definition, (spl98 <=> (distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X1))), introduced(definition, [new_symbols(naming, [spl98])], [avatar_definition])).
% 25.60/3.79 cnf(ssp115, plain, (spl3 | spl27 | spl98), inference(avatar_split_clause, [status(thm)], [p848, sdef3, sdef27, sdef98])).
% 25.60/3.79 cnf(p850, plain, distinct_lines(sk1,X0) | distinct_lines(sk0,X1) | distinct_lines(X2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X2) | apart_point_and_line(intersection_point(sk0,sk2),X0), inference(resolution, [status(thm)], [p85, p73])).
% 25.60/3.79 fof(sdef99, definition, (spl99 <=> (distinct_lines(sk0,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X1))), introduced(definition, [new_symbols(naming, [spl99])], [avatar_definition])).
% 25.60/3.79 cnf(ssp116, plain, (spl31 | spl99), inference(avatar_split_clause, [status(thm)], [p850, sdef31, sdef99])).
% 25.60/3.79 cnf(p852, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X2), inference(resolution, [status(thm)], [p85, p73])).
% 25.60/3.79 fof(sdef100, definition, (spl100 <=> (distinct_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk2),X2))), introduced(definition, [new_symbols(naming, [spl100])], [avatar_definition])).
% 25.60/3.79 cnf(ssp117, plain, (spl2 | spl26 | spl100), inference(avatar_split_clause, [status(thm)], [p852, sdef2, sdef26, sdef100])).
% 25.60/3.79 cnf(p854, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(sk0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk2),X2), inference(resolution, [status(thm)], [p85, p73])).
% 25.60/3.79 fof(sdef101, definition, (spl101 <=> (distinct_lines(sk1,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X1))), introduced(definition, [new_symbols(naming, [spl101])], [avatar_definition])).
% 25.60/3.79 cnf(ssp118, plain, (spl28 | spl101), inference(avatar_split_clause, [status(thm)], [p854, sdef28, sdef101])).
% 25.60/3.79 cnf(p856, plain, distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p85, p78])).
% 25.60/3.79 fof(sdef102, definition, (spl102 <=> (distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X1))), introduced(definition, [new_symbols(naming, [spl102])], [avatar_definition])).
% 25.60/3.79 cnf(ssp119, plain, (spl3 | spl48 | spl102), inference(avatar_split_clause, [status(thm)], [p856, sdef3, sdef48, sdef102])).
% 25.60/3.79 cnf(p858, plain, distinct_lines(sk1,X0) | distinct_lines(sk0,X1) | distinct_lines(X2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X2) | apart_point_and_line(intersection_point(sk1,sk2),X0), inference(resolution, [status(thm)], [p85, p78])).
% 25.60/3.79 fof(sdef103, definition, (spl103 <=> (distinct_lines(sk0,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X1))), introduced(definition, [new_symbols(naming, [spl103])], [avatar_definition])).
% 25.60/3.79 cnf(ssp120, plain, (spl52 | spl103), inference(avatar_split_clause, [status(thm)], [p858, sdef52, sdef103])).
% 25.60/3.79 cnf(p860, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X2), inference(resolution, [status(thm)], [p85, p78])).
% 25.60/3.79 fof(sdef104, definition, (spl104 <=> (distinct_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk1,sk2),X2))), introduced(definition, [new_symbols(naming, [spl104])], [avatar_definition])).
% 25.60/3.79 cnf(ssp121, plain, (spl2 | spl47 | spl104), inference(avatar_split_clause, [status(thm)], [p860, sdef2, sdef47, sdef104])).
% 25.60/3.79 cnf(p862, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(sk0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk1,sk2),X1) | apart_point_and_line(intersection_point(sk1,sk2),X2), inference(resolution, [status(thm)], [p85, p78])).
% 25.60/3.79 fof(sdef105, definition, (spl105 <=> (distinct_lines(sk1,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X1))), introduced(definition, [new_symbols(naming, [spl105])], [avatar_definition])).
% 25.60/3.79 cnf(ssp122, plain, (spl49 | spl105), inference(avatar_split_clause, [status(thm)], [p862, sdef49, sdef105])).
% 25.60/3.79 cnf(p864, plain, distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X0,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X3,sk1) | apart_point_and_line(X3,X1), inference(resolution, [status(thm)], [p85, p83])).
% 25.60/3.79 fof(sdef106, definition, (spl106 <=> (distinct_lines(X0,X1) | distinct_lines(sk0,X2) | distinct_lines(X0,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X3,sk1) | apart_point_and_line(X3,X1))), introduced(definition, [new_symbols(naming, [spl106])], [avatar_definition])).
% 25.60/3.79 cnf(ssp123, plain, (spl3 | spl106), inference(avatar_split_clause, [status(thm)], [p864, sdef3, sdef106])).
% 25.60/3.79 cnf(p867, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(X3,sk0) | apart_point_and_line(X3,X2), inference(resolution, [status(thm)], [p85, p83])).
% 25.60/3.79 fof(sdef107, definition, (spl107 <=> (distinct_lines(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(X3,sk0) | apart_point_and_line(X3,X2))), introduced(definition, [new_symbols(naming, [spl107])], [avatar_definition])).
% 25.60/3.79 cnf(ssp124, plain, (spl2 | spl107), inference(avatar_split_clause, [status(thm)], [p867, sdef2, sdef107])).
% 25.60/3.79 cnf(p750, plain, (distinct_lines(sk0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | ~spl68), inference(avatar_component_clause, [status(thm)], [sdef68])).
% 25.60/3.79 cnf(p878, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | ~spl68), inference(resolution, [status(thm)], [p750, p68])).
% 25.60/3.79 fof(sdef108, definition, (spl108 <=> (apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))))), introduced(definition, [new_symbols(naming, [spl108])], [avatar_definition])).
% 25.60/3.79 fof(sdef109, definition, (spl109 <=> (apart_point_and_line(intersection_point(sk2,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))))), introduced(definition, [new_symbols(naming, [spl109])], [avatar_definition])).
% 25.60/3.79 cnf(ssp125, plain, (~spl68 | spl2 | spl4 | spl108 | spl109), inference(avatar_split_clause, [status(thm)], [p878, sdef2, sdef4, sdef108, sdef109])).
% 25.60/3.79 cnf(p881, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | ~spl68), inference(resolution, [status(thm)], [p750, p73])).
% 25.60/3.79 fof(sdef110, definition, (spl110 <=> (apart_point_and_line(intersection_point(sk0,sk2),line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))))), introduced(definition, [new_symbols(naming, [spl110])], [avatar_definition])).
% 25.60/3.79 cnf(ssp126, plain, (~spl68 | spl2 | spl26 | spl108 | spl110), inference(avatar_split_clause, [status(thm)], [p881, sdef2, sdef26, sdef108, sdef110])).
% 25.60/3.79 cnf(p883, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | ~spl68), inference(resolution, [status(thm)], [p750, p78])).
% 25.60/3.79 fof(sdef111, definition, (spl111 <=> (apart_point_and_line(intersection_point(sk1,sk2),line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))))), introduced(definition, [new_symbols(naming, [spl111])], [avatar_definition])).
% 25.60/3.79 cnf(ssp127, plain, (~spl68 | spl2 | spl47 | spl108 | spl111), inference(avatar_split_clause, [status(thm)], [p883, sdef2, sdef47, sdef108, sdef111])).
% 25.60/3.79 cnf(p885, plain, (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | ~spl68), inference(resolution, [status(thm)], [p750, p83])).
% 25.60/3.79 fof(sdef112, definition, (spl112 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))))), introduced(definition, [new_symbols(naming, [spl112])], [avatar_definition])).
% 25.60/3.79 cnf(ssp128, plain, (~spl68 | spl2 | spl108 | spl112), inference(avatar_split_clause, [status(thm)], [p885, sdef2, sdef108, sdef112])).
% 25.60/3.79 cnf(p86, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p28, c4])).
% 25.60/3.79 cnf(p890, plain, distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X0), inference(resolution, [status(thm)], [p86, p68])).
% 25.60/3.79 fof(sdef113, definition, (spl113 <=> (distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0))), introduced(definition, [new_symbols(naming, [spl113])], [avatar_definition])).
% 25.60/3.79 cnf(ssp129, plain, (spl2 | spl4 | spl113), inference(avatar_split_clause, [status(thm)], [p890, sdef2, sdef4, sdef113])).
% 25.60/3.79 cnf(p892, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X2), inference(resolution, [status(thm)], [p86, p68])).
% 25.60/3.79 fof(sdef114, definition, (spl114 <=> (distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),X2))), introduced(definition, [new_symbols(naming, [spl114])], [avatar_definition])).
% 25.60/3.79 cnf(ssp130, plain, (spl3 | spl5 | spl114), inference(avatar_split_clause, [status(thm)], [p892, sdef3, sdef5, sdef114])).
% 25.60/3.79 cnf(p894, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(sk1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X2), inference(resolution, [status(thm)], [p86, p68])).
% 25.60/3.79 fof(sdef115, definition, (spl115 <=> (distinct_lines(sk0,X0) | distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X1))), introduced(definition, [new_symbols(naming, [spl115])], [avatar_definition])).
% 25.60/3.79 cnf(ssp131, plain, (spl9 | spl115), inference(avatar_split_clause, [status(thm)], [p894, sdef9, sdef115])).
% 25.60/3.79 cnf(p896, plain, distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0), inference(resolution, [status(thm)], [p86, p73])).
% 25.60/3.79 fof(sdef116, definition, (spl116 <=> (distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0))), introduced(definition, [new_symbols(naming, [spl116])], [avatar_definition])).
% 25.60/3.79 cnf(ssp132, plain, (spl2 | spl26 | spl116), inference(avatar_split_clause, [status(thm)], [p896, sdef2, sdef26, sdef116])).
% 25.60/3.79 cnf(p898, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X2), inference(resolution, [status(thm)], [p86, p73])).
% 25.60/3.79 fof(sdef117, definition, (spl117 <=> (distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk2),X2))), introduced(definition, [new_symbols(naming, [spl117])], [avatar_definition])).
% 25.60/3.79 cnf(ssp133, plain, (spl3 | spl27 | spl117), inference(avatar_split_clause, [status(thm)], [p898, sdef3, sdef27, sdef117])).
% 25.60/3.79 cnf(p900, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(sk1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk2),X2), inference(resolution, [status(thm)], [p86, p73])).
% 25.60/3.79 fof(sdef118, definition, (spl118 <=> (distinct_lines(sk0,X0) | distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X1))), introduced(definition, [new_symbols(naming, [spl118])], [avatar_definition])).
% 25.60/3.79 cnf(ssp134, plain, (spl31 | spl118), inference(avatar_split_clause, [status(thm)], [p900, sdef31, sdef118])).
% 25.60/3.79 cnf(p902, plain, distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X0), inference(resolution, [status(thm)], [p86, p78])).
% 25.60/3.79 fof(sdef119, definition, (spl119 <=> (distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0))), introduced(definition, [new_symbols(naming, [spl119])], [avatar_definition])).
% 25.60/3.79 cnf(ssp135, plain, (spl2 | spl47 | spl119), inference(avatar_split_clause, [status(thm)], [p902, sdef2, sdef47, sdef119])).
% 25.60/3.79 cnf(p904, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X2), inference(resolution, [status(thm)], [p86, p78])).
% 25.60/3.79 fof(sdef120, definition, (spl120 <=> (distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk1,sk2),X2))), introduced(definition, [new_symbols(naming, [spl120])], [avatar_definition])).
% 25.60/3.79 cnf(ssp136, plain, (spl3 | spl48 | spl120), inference(avatar_split_clause, [status(thm)], [p904, sdef3, sdef48, sdef120])).
% 25.60/3.79 cnf(p906, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(sk1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk1,sk2),X1) | apart_point_and_line(intersection_point(sk1,sk2),X2), inference(resolution, [status(thm)], [p86, p78])).
% 25.60/3.79 fof(sdef121, definition, (spl121 <=> (distinct_lines(sk0,X0) | distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X1))), introduced(definition, [new_symbols(naming, [spl121])], [avatar_definition])).
% 25.60/3.79 cnf(ssp137, plain, (spl52 | spl121), inference(avatar_split_clause, [status(thm)], [p906, sdef52, sdef121])).
% 25.60/3.79 cnf(p908, plain, distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X3,sk0) | apart_point_and_line(X3,X0), inference(resolution, [status(thm)], [p86, p83])).
% 25.60/3.79 fof(sdef122, definition, (spl122 <=> (distinct_lines(X0,X1) | distinct_lines(sk1,X2) | distinct_lines(X1,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X3,sk0) | apart_point_and_line(X3,X0))), introduced(definition, [new_symbols(naming, [spl122])], [avatar_definition])).
% 25.60/3.79 cnf(ssp138, plain, (spl2 | spl122), inference(avatar_split_clause, [status(thm)], [p908, sdef2, sdef122])).
% 25.60/3.79 cnf(p910, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X1,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(X3,sk1) | apart_point_and_line(X3,X2), inference(resolution, [status(thm)], [p86, p83])).
% 25.60/3.79 fof(sdef123, definition, (spl123 <=> (distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X1,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(X3,sk1) | apart_point_and_line(X3,X2))), introduced(definition, [new_symbols(naming, [spl123])], [avatar_definition])).
% 25.60/3.79 cnf(ssp139, plain, (spl3 | spl123), inference(avatar_split_clause, [status(thm)], [p910, sdef3, sdef123])).
% 25.60/3.79 cnf(p755, plain, (distinct_lines(sk0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | ~spl70), inference(avatar_component_clause, [status(thm)], [sdef70])).
% 25.60/3.79 cnf(p914, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | ~spl70), inference(resolution, [status(thm)], [p755, p68])).
% 25.60/3.79 fof(sdef124, definition, (spl124 <=> (apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))))), introduced(definition, [new_symbols(naming, [spl124])], [avatar_definition])).
% 25.60/3.79 fof(sdef125, definition, (spl125 <=> (apart_point_and_line(intersection_point(sk2,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))))), introduced(definition, [new_symbols(naming, [spl125])], [avatar_definition])).
% 25.60/3.79 cnf(ssp140, plain, (~spl70 | spl2 | spl4 | spl124 | spl125), inference(avatar_split_clause, [status(thm)], [p914, sdef2, sdef4, sdef124, sdef125])).
% 25.60/3.79 cnf(p917, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | ~spl70), inference(resolution, [status(thm)], [p755, p73])).
% 25.60/3.79 fof(sdef126, definition, (spl126 <=> (apart_point_and_line(intersection_point(sk0,sk2),line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))))), introduced(definition, [new_symbols(naming, [spl126])], [avatar_definition])).
% 25.60/3.79 cnf(ssp141, plain, (~spl70 | spl2 | spl26 | spl124 | spl126), inference(avatar_split_clause, [status(thm)], [p917, sdef2, sdef26, sdef124, sdef126])).
% 25.60/3.79 cnf(p919, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | ~spl70), inference(resolution, [status(thm)], [p755, p78])).
% 25.60/3.79 fof(sdef127, definition, (spl127 <=> (apart_point_and_line(intersection_point(sk1,sk2),line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))))), introduced(definition, [new_symbols(naming, [spl127])], [avatar_definition])).
% 25.60/3.79 cnf(ssp142, plain, (~spl70 | spl2 | spl47 | spl124 | spl127), inference(avatar_split_clause, [status(thm)], [p919, sdef2, sdef47, sdef124, sdef127])).
% 25.60/3.79 cnf(p921, plain, (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | ~spl70), inference(resolution, [status(thm)], [p755, p83])).
% 25.60/3.79 fof(sdef128, definition, (spl128 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))))), introduced(definition, [new_symbols(naming, [spl128])], [avatar_definition])).
% 25.60/3.79 cnf(ssp143, plain, (~spl70 | spl2 | spl124 | spl128), inference(avatar_split_clause, [status(thm)], [p921, sdef2, sdef124, sdef128])).
% 25.60/3.79 cnf(p773, plain, (distinct_lines(sk1,line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | ~spl72), inference(avatar_component_clause, [status(thm)], [sdef72])).
% 25.60/3.79 cnf(p924, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | ~spl72), inference(resolution, [status(thm)], [p773, p68])).
% 25.60/3.79 fof(sdef129, definition, (spl129 <=> (apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))))), introduced(definition, [new_symbols(naming, [spl129])], [avatar_definition])).
% 25.60/3.79 fof(sdef130, definition, (spl130 <=> (apart_point_and_line(intersection_point(sk2,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))))), introduced(definition, [new_symbols(naming, [spl130])], [avatar_definition])).
% 25.60/3.79 cnf(ssp144, plain, (~spl72 | spl3 | spl5 | spl129 | spl130), inference(avatar_split_clause, [status(thm)], [p924, sdef3, sdef5, sdef129, sdef130])).
% 25.60/3.79 cnf(p927, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | ~spl72), inference(resolution, [status(thm)], [p773, p73])).
% 25.60/3.79 fof(sdef131, definition, (spl131 <=> (apart_point_and_line(intersection_point(sk0,sk2),line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))))), introduced(definition, [new_symbols(naming, [spl131])], [avatar_definition])).
% 25.60/3.79 cnf(ssp145, plain, (~spl72 | spl3 | spl27 | spl129 | spl131), inference(avatar_split_clause, [status(thm)], [p927, sdef3, sdef27, sdef129, sdef131])).
% 25.60/3.79 cnf(p929, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | ~spl72), inference(resolution, [status(thm)], [p773, p78])).
% 25.60/3.79 fof(sdef132, definition, (spl132 <=> (apart_point_and_line(intersection_point(sk1,sk2),line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))))), introduced(definition, [new_symbols(naming, [spl132])], [avatar_definition])).
% 25.60/3.79 cnf(ssp146, plain, (~spl72 | spl3 | spl48 | spl129 | spl132), inference(avatar_split_clause, [status(thm)], [p929, sdef3, sdef48, sdef129, sdef132])).
% 25.60/3.79 cnf(p931, plain, (apart_point_and_line(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | ~spl72), inference(resolution, [status(thm)], [p773, p83])).
% 25.60/3.79 fof(sdef133, definition, (spl133 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(X0,sk1) | apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))))), introduced(definition, [new_symbols(naming, [spl133])], [avatar_definition])).
% 25.60/3.79 cnf(ssp147, plain, (~spl72 | spl3 | spl129 | spl133), inference(avatar_split_clause, [status(thm)], [p931, sdef3, sdef129, sdef133])).
% 25.60/3.79 cnf(p87, plain, distinct_lines(sk0,X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p28, c4])).
% 25.60/3.79 cnf(p940, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p87, p68])).
% 25.60/3.79 fof(sdef134, definition, (spl134 <=> (distinct_lines(sk1,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X1))), introduced(definition, [new_symbols(naming, [spl134])], [avatar_definition])).
% 25.60/3.79 cnf(ssp148, plain, (spl2 | spl4 | spl134), inference(avatar_split_clause, [status(thm)], [p940, sdef2, sdef4, sdef134])).
% 25.60/3.79 cnf(p942, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X2,X1) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X2), inference(resolution, [status(thm)], [p87, p68])).
% 25.60/3.79 fof(sdef135, definition, (spl135 <=> (distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),X2))), introduced(definition, [new_symbols(naming, [spl135])], [avatar_definition])).
% 25.60/3.79 cnf(ssp149, plain, (spl3 | spl5 | spl135), inference(avatar_split_clause, [status(thm)], [p942, sdef3, sdef5, sdef135])).
% 25.60/3.79 cnf(p944, plain, distinct_lines(sk0,X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X2), inference(resolution, [status(thm)], [p87, p68])).
% 25.60/3.79 fof(sdef136, definition, (spl136 <=> (distinct_lines(sk1,X0) | distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X1))), introduced(definition, [new_symbols(naming, [spl136])], [avatar_definition])).
% 25.60/3.79 cnf(ssp150, plain, (spl6 | spl136), inference(avatar_split_clause, [status(thm)], [p944, sdef6, sdef136])).
% 25.60/3.79 cnf(p946, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p87, p73])).
% 25.60/3.79 fof(sdef137, definition, (spl137 <=> (distinct_lines(sk1,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X1))), introduced(definition, [new_symbols(naming, [spl137])], [avatar_definition])).
% 25.60/3.79 cnf(ssp151, plain, (spl2 | spl26 | spl137), inference(avatar_split_clause, [status(thm)], [p946, sdef2, sdef26, sdef137])).
% 25.60/3.79 cnf(p948, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X2,X1) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X2), inference(resolution, [status(thm)], [p87, p73])).
% 25.60/3.79 fof(sdef138, definition, (spl138 <=> (distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk2),X2))), introduced(definition, [new_symbols(naming, [spl138])], [avatar_definition])).
% 25.60/3.79 cnf(ssp152, plain, (spl3 | spl27 | spl138), inference(avatar_split_clause, [status(thm)], [p948, sdef3, sdef27, sdef138])).
% 25.60/3.79 cnf(p950, plain, distinct_lines(sk0,X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X2), inference(resolution, [status(thm)], [p87, p73])).
% 25.60/3.79 fof(sdef139, definition, (spl139 <=> (distinct_lines(sk1,X0) | distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X1))), introduced(definition, [new_symbols(naming, [spl139])], [avatar_definition])).
% 25.60/3.79 cnf(ssp153, plain, (spl28 | spl139), inference(avatar_split_clause, [status(thm)], [p950, sdef28, sdef139])).
% 25.60/3.79 cnf(p952, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p87, p78])).
% 25.60/3.79 fof(sdef140, definition, (spl140 <=> (distinct_lines(sk1,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X1))), introduced(definition, [new_symbols(naming, [spl140])], [avatar_definition])).
% 25.60/3.79 cnf(ssp154, plain, (spl2 | spl47 | spl140), inference(avatar_split_clause, [status(thm)], [p952, sdef2, sdef47, sdef140])).
% 25.60/3.79 cnf(p954, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X2,X1) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X2), inference(resolution, [status(thm)], [p87, p78])).
% 25.60/3.80 fof(sdef141, definition, (spl141 <=> (distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X2,X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk1,sk2),X2))), introduced(definition, [new_symbols(naming, [spl141])], [avatar_definition])).
% 25.60/3.80 cnf(ssp155, plain, (spl3 | spl48 | spl141), inference(avatar_split_clause, [status(thm)], [p954, sdef3, sdef48, sdef141])).
% 25.60/3.80 cnf(p956, plain, distinct_lines(sk0,X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X2), inference(resolution, [status(thm)], [p87, p78])).
% 25.60/3.80 fof(sdef142, definition, (spl142 <=> (distinct_lines(sk1,X0) | distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X1))), introduced(definition, [new_symbols(naming, [spl142])], [avatar_definition])).
% 25.60/3.80 cnf(ssp156, plain, (spl49 | spl142), inference(avatar_split_clause, [status(thm)], [p956, sdef49, sdef142])).
% 25.60/3.80 cnf(p958, plain, distinct_lines(sk1,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X3,sk0) | apart_point_and_line(X3,X1), inference(resolution, [status(thm)], [p87, p83])).
% 25.60/3.80 fof(sdef143, definition, (spl143 <=> (distinct_lines(sk1,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X3,sk0) | apart_point_and_line(X3,X1))), introduced(definition, [new_symbols(naming, [spl143])], [avatar_definition])).
% 25.60/3.80 cnf(ssp157, plain, (spl2 | spl143), inference(avatar_split_clause, [status(thm)], [p958, sdef2, sdef143])).
% 25.60/3.80 cnf(p960, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X2,X1) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(X3,sk1) | apart_point_and_line(X3,X2), inference(resolution, [status(thm)], [p87, p83])).
% 25.60/3.80 fof(sdef144, definition, (spl144 <=> (distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(X2,X1) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(X3,sk1) | apart_point_and_line(X3,X2))), introduced(definition, [new_symbols(naming, [spl144])], [avatar_definition])).
% 25.60/3.80 cnf(ssp158, plain, (spl3 | spl144), inference(avatar_split_clause, [status(thm)], [p960, sdef3, sdef144])).
% 25.60/3.80 cnf(p103, plain, convergent_lines(sk1,X0) | convergent_lines(X1,X0) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p33, c13])).
% 25.60/3.80 cnf(p244, plain, convergent_lines(sk1,X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p103, c13])).
% 25.60/3.80 cnf(p968, plain, convergent_lines(sk1,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p244, p68])).
% 25.60/3.80 fof(sdef145, definition, (spl145 <=> (convergent_lines(sk1,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X1))), introduced(definition, [new_symbols(naming, [spl145])], [avatar_definition])).
% 25.60/3.80 cnf(ssp159, plain, (spl2 | spl4 | spl145), inference(avatar_split_clause, [status(thm)], [p968, sdef2, sdef4, sdef145])).
% 25.60/3.80 cnf(p970, plain, convergent_lines(sk1,X0) | distinct_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0), inference(resolution, [status(thm)], [p244, p68])).
% 25.60/3.80 cnf(ssp160, plain, (spl6 | spl18), inference(avatar_split_clause, [status(thm)], [p970, sdef6, sdef18])).
% 25.60/3.80 cnf(p971, plain, convergent_lines(sk1,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p244, p73])).
% 25.60/3.80 fof(sdef146, definition, (spl146 <=> (convergent_lines(sk1,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X1))), introduced(definition, [new_symbols(naming, [spl146])], [avatar_definition])).
% 25.60/3.80 cnf(ssp161, plain, (spl2 | spl26 | spl146), inference(avatar_split_clause, [status(thm)], [p971, sdef2, sdef26, sdef146])).
% 25.60/3.80 cnf(p973, plain, convergent_lines(sk1,X0) | distinct_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0), inference(resolution, [status(thm)], [p244, p73])).
% 25.60/3.80 cnf(ssp162, plain, (spl28 | spl40), inference(avatar_split_clause, [status(thm)], [p973, sdef28, sdef40])).
% 25.60/3.80 cnf(p974, plain, convergent_lines(sk1,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p244, p78])).
% 25.60/3.80 fof(sdef147, definition, (spl147 <=> (convergent_lines(sk1,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X1))), introduced(definition, [new_symbols(naming, [spl147])], [avatar_definition])).
% 25.60/3.80 cnf(ssp163, plain, (spl2 | spl47 | spl147), inference(avatar_split_clause, [status(thm)], [p974, sdef2, sdef47, sdef147])).
% 25.60/3.80 cnf(p976, plain, convergent_lines(sk1,X0) | distinct_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0), inference(resolution, [status(thm)], [p244, p78])).
% 25.60/3.80 cnf(ssp164, plain, (spl49 | spl61), inference(avatar_split_clause, [status(thm)], [p976, sdef49, sdef61])).
% 25.60/3.80 cnf(p977, plain, convergent_lines(sk1,X0) | distinct_lines(X1,X0) | apart_point_and_line(X2,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X2,sk0) | apart_point_and_line(X2,X1), inference(resolution, [status(thm)], [p244, p83])).
% 25.60/3.80 fof(sdef148, definition, (spl148 <=> (convergent_lines(sk1,X0) | distinct_lines(X1,X0) | apart_point_and_line(X2,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X2,sk0) | apart_point_and_line(X2,X1))), introduced(definition, [new_symbols(naming, [spl148])], [avatar_definition])).
% 25.60/3.80 cnf(ssp165, plain, (spl2 | spl148), inference(avatar_split_clause, [status(thm)], [p977, sdef2, sdef148])).
% 25.60/3.80 cnf(p104, plain, convergent_lines(sk0,X0) | convergent_lines(X0,X1) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p33, c13])).
% 25.60/3.80 cnf(p253, plain, convergent_lines(sk0,X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p104, c13])).
% 25.60/3.80 cnf(p984, plain, convergent_lines(sk0,X0) | distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p253, p68])).
% 25.60/3.80 fof(sdef149, definition, (spl149 <=> (convergent_lines(sk0,X0) | distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X1))), introduced(definition, [new_symbols(naming, [spl149])], [avatar_definition])).
% 25.60/3.80 cnf(ssp166, plain, (spl3 | spl5 | spl149), inference(avatar_split_clause, [status(thm)], [p984, sdef3, sdef5, sdef149])).
% 25.60/3.80 cnf(p986, plain, convergent_lines(sk0,X0) | distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p253, p73])).
% 25.60/3.80 fof(sdef150, definition, (spl150 <=> (convergent_lines(sk0,X0) | distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X1))), introduced(definition, [new_symbols(naming, [spl150])], [avatar_definition])).
% 25.60/3.80 cnf(ssp167, plain, (spl3 | spl27 | spl150), inference(avatar_split_clause, [status(thm)], [p986, sdef3, sdef27, sdef150])).
% 25.60/3.80 cnf(p988, plain, convergent_lines(sk0,X0) | distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p253, p78])).
% 25.60/3.80 fof(sdef151, definition, (spl151 <=> (convergent_lines(sk0,X0) | distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X1))), introduced(definition, [new_symbols(naming, [spl151])], [avatar_definition])).
% 25.60/3.80 cnf(ssp168, plain, (spl3 | spl48 | spl151), inference(avatar_split_clause, [status(thm)], [p988, sdef3, sdef48, sdef151])).
% 25.60/3.80 cnf(p990, plain, convergent_lines(sk0,X0) | distinct_lines(X0,X1) | apart_point_and_line(X2,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X2,sk1) | apart_point_and_line(X2,X1), inference(resolution, [status(thm)], [p253, p83])).
% 25.60/3.80 fof(sdef152, definition, (spl152 <=> (convergent_lines(sk0,X0) | distinct_lines(X0,X1) | apart_point_and_line(X2,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X2,sk1) | apart_point_and_line(X2,X1))), introduced(definition, [new_symbols(naming, [spl152])], [avatar_definition])).
% 25.60/3.80 cnf(ssp169, plain, (spl3 | spl152), inference(avatar_split_clause, [status(thm)], [p990, sdef3, sdef152])).
% 25.60/3.80 cnf(p268, plain, convergent_lines(X0,sk1) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p117, c13])).
% 25.60/3.80 cnf(p1007, plain, convergent_lines(X0,sk1) | convergent_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p268, p68])).
% 25.60/3.80 fof(sdef153, definition, (spl153 <=> (convergent_lines(X0,sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0))), introduced(definition, [new_symbols(naming, [spl153])], [avatar_definition])).
% 25.60/3.80 cnf(ssp170, plain, (spl17 | spl153), inference(avatar_split_clause, [status(thm)], [p1007, sdef17, sdef153])).
% 25.60/3.80 cnf(p1009, plain, convergent_lines(X0,sk1) | convergent_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p268, p73])).
% 25.60/3.80 fof(sdef154, definition, (spl154 <=> (convergent_lines(X0,sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0))), introduced(definition, [new_symbols(naming, [spl154])], [avatar_definition])).
% 25.60/3.80 cnf(ssp171, plain, (spl39 | spl154), inference(avatar_split_clause, [status(thm)], [p1009, sdef39, sdef154])).
% 25.60/3.80 cnf(p1011, plain, convergent_lines(X0,sk1) | convergent_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p268, p78])).
% 25.60/3.80 fof(sdef155, definition, (spl155 <=> (convergent_lines(X0,sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0))), introduced(definition, [new_symbols(naming, [spl155])], [avatar_definition])).
% 25.60/3.80 cnf(ssp172, plain, (spl60 | spl155), inference(avatar_split_clause, [status(thm)], [p1011, sdef60, sdef155])).
% 25.60/3.80 cnf(p90, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(sk1,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p30, c4])).
% 25.60/3.80 cnf(p1018, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X2), inference(resolution, [status(thm)], [p90, p68])).
% 25.60/3.80 fof(sdef156, definition, (spl156 <=> (distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),X2))), introduced(definition, [new_symbols(naming, [spl156])], [avatar_definition])).
% 25.60/3.80 cnf(ssp173, plain, (spl3 | spl5 | spl156), inference(avatar_split_clause, [status(thm)], [p1018, sdef3, sdef5, sdef156])).
% 25.60/3.80 cnf(p1020, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(sk1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X2), inference(resolution, [status(thm)], [p90, p68])).
% 25.60/3.80 fof(sdef157, definition, (spl157 <=> (distinct_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X1))), introduced(definition, [new_symbols(naming, [spl157])], [avatar_definition])).
% 25.60/3.80 cnf(ssp174, plain, (spl9 | spl157), inference(avatar_split_clause, [status(thm)], [p1020, sdef9, sdef157])).
% 25.60/3.80 cnf(p1022, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X2), inference(resolution, [status(thm)], [p90, p73])).
% 25.60/3.80 fof(sdef158, definition, (spl158 <=> (distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk2),X2))), introduced(definition, [new_symbols(naming, [spl158])], [avatar_definition])).
% 25.60/3.80 cnf(ssp175, plain, (spl3 | spl27 | spl158), inference(avatar_split_clause, [status(thm)], [p1022, sdef3, sdef27, sdef158])).
% 25.60/3.80 cnf(p1024, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(sk1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk2),X2), inference(resolution, [status(thm)], [p90, p73])).
% 25.60/3.80 fof(sdef159, definition, (spl159 <=> (distinct_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X1))), introduced(definition, [new_symbols(naming, [spl159])], [avatar_definition])).
% 25.60/3.80 cnf(ssp176, plain, (spl31 | spl159), inference(avatar_split_clause, [status(thm)], [p1024, sdef31, sdef159])).
% 25.60/3.80 cnf(p1026, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X2), inference(resolution, [status(thm)], [p90, p78])).
% 25.60/3.80 fof(sdef160, definition, (spl160 <=> (distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk1,sk2),X2))), introduced(definition, [new_symbols(naming, [spl160])], [avatar_definition])).
% 25.60/3.80 cnf(ssp177, plain, (spl3 | spl48 | spl160), inference(avatar_split_clause, [status(thm)], [p1026, sdef3, sdef48, sdef160])).
% 25.60/3.80 cnf(p1028, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(sk1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk1,sk2),X1) | apart_point_and_line(intersection_point(sk1,sk2),X2), inference(resolution, [status(thm)], [p90, p78])).
% 25.60/3.80 fof(sdef161, definition, (spl161 <=> (distinct_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X1))), introduced(definition, [new_symbols(naming, [spl161])], [avatar_definition])).
% 25.60/3.80 cnf(ssp178, plain, (spl52 | spl161), inference(avatar_split_clause, [status(thm)], [p1028, sdef52, sdef161])).
% 25.60/3.80 cnf(p1030, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(X3,sk1) | apart_point_and_line(X3,X2), inference(resolution, [status(thm)], [p90, p83])).
% 25.60/3.80 fof(sdef162, definition, (spl162 <=> (distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(X1,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(X3,sk1) | apart_point_and_line(X3,X2))), introduced(definition, [new_symbols(naming, [spl162])], [avatar_definition])).
% 25.60/3.80 cnf(ssp179, plain, (spl3 | spl162), inference(avatar_split_clause, [status(thm)], [p1030, sdef3, sdef162])).
% 25.60/3.80 cnf(p91, plain, distinct_lines(sk1,X0) | distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p30, c4])).
% 25.60/3.80 cnf(p1058, plain, distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X0), inference(resolution, [status(thm)], [p91, p68])).
% 25.60/3.80 fof(sdef163, definition, (spl163 <=> (distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0))), introduced(definition, [new_symbols(naming, [spl163])], [avatar_definition])).
% 25.60/3.80 cnf(ssp180, plain, (spl3 | spl5 | spl163), inference(avatar_split_clause, [status(thm)], [p1058, sdef3, sdef5, sdef163])).
% 25.60/3.80 cnf(p1060, plain, distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X0), inference(resolution, [status(thm)], [p91, p73])).
% 25.60/3.80 fof(sdef164, definition, (spl164 <=> (distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0))), introduced(definition, [new_symbols(naming, [spl164])], [avatar_definition])).
% 25.60/3.80 cnf(ssp181, plain, (spl3 | spl27 | spl164), inference(avatar_split_clause, [status(thm)], [p1060, sdef3, sdef27, sdef164])).
% 25.60/3.80 cnf(p1062, plain, distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X0), inference(resolution, [status(thm)], [p91, p78])).
% 25.60/3.80 fof(sdef165, definition, (spl165 <=> (distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0))), introduced(definition, [new_symbols(naming, [spl165])], [avatar_definition])).
% 25.60/3.80 cnf(ssp182, plain, (spl3 | spl48 | spl165), inference(avatar_split_clause, [status(thm)], [p1062, sdef3, sdef48, sdef165])).
% 25.60/3.80 cnf(p1064, plain, distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X3,sk1) | apart_point_and_line(X3,X0), inference(resolution, [status(thm)], [p91, p83])).
% 25.60/3.80 fof(sdef166, definition, (spl166 <=> (distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X3,sk1) | apart_point_and_line(X3,X0))), introduced(definition, [new_symbols(naming, [spl166])], [avatar_definition])).
% 25.60/3.80 cnf(ssp183, plain, (spl3 | spl166), inference(avatar_split_clause, [status(thm)], [p1064, sdef3, sdef166])).
% 25.60/3.80 cnf(p116, plain, convergent_lines(sk0,X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p102, c13])).
% 25.60/3.80 cnf(p124, plain, distinct_lines(X0,sk1) | convergent_lines(sk0,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p116, c5])).
% 25.60/3.80 cnf(p287, plain, distinct_lines(X0,sk1) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p124, c13])).
% 25.60/3.80 cnf(p1073, plain, distinct_lines(X0,sk1) | convergent_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p287, p68])).
% 25.60/3.80 cnf(ssp184, plain, (spl10 | spl17), inference(avatar_split_clause, [status(thm)], [p1073, sdef10, sdef17])).
% 25.60/3.80 cnf(p1074, plain, distinct_lines(X0,sk1) | convergent_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p287, p73])).
% 25.60/3.80 cnf(ssp185, plain, (spl32 | spl39), inference(avatar_split_clause, [status(thm)], [p1074, sdef32, sdef39])).
% 25.60/3.80 cnf(p1075, plain, distinct_lines(X0,sk1) | convergent_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p287, p78])).
% 25.60/3.80 cnf(ssp186, plain, (spl53 | spl60), inference(avatar_split_clause, [status(thm)], [p1075, sdef53, sdef60])).
% 25.60/3.80 cnf(p128, plain, convergent_lines(sk2,X0) | convergent_lines(X1,X0) | distinct_lines(sk1,X1), inference(resolution, [status(thm)], [p36, c13])).
% 25.60/3.80 cnf(p296, plain, convergent_lines(sk2,X0) | distinct_lines(sk1,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p128, c13])).
% 25.60/3.80 cnf(p1084, plain, convergent_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p296, p68])).
% 25.60/3.80 fof(sdef167, definition, (spl167 <=> (convergent_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X1))), introduced(definition, [new_symbols(naming, [spl167])], [avatar_definition])).
% 25.60/3.80 cnf(ssp187, plain, (spl3 | spl5 | spl167), inference(avatar_split_clause, [status(thm)], [p1084, sdef3, sdef5, sdef167])).
% 25.60/3.80 cnf(p1086, plain, convergent_lines(sk2,X0) | distinct_lines(sk1,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0), inference(resolution, [status(thm)], [p296, p68])).
% 25.60/3.80 cnf(ssp188, plain, (spl9 | spl19), inference(avatar_split_clause, [status(thm)], [p1086, sdef9, sdef19])).
% 25.60/3.80 cnf(p1087, plain, convergent_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p296, p73])).
% 25.60/3.80 fof(sdef168, definition, (spl168 <=> (convergent_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X1))), introduced(definition, [new_symbols(naming, [spl168])], [avatar_definition])).
% 25.60/3.80 cnf(ssp189, plain, (spl3 | spl27 | spl168), inference(avatar_split_clause, [status(thm)], [p1087, sdef3, sdef27, sdef168])).
% 25.60/3.80 cnf(p1089, plain, convergent_lines(sk2,X0) | distinct_lines(sk1,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0), inference(resolution, [status(thm)], [p296, p73])).
% 25.60/3.80 cnf(ssp190, plain, (spl31 | spl41), inference(avatar_split_clause, [status(thm)], [p1089, sdef31, sdef41])).
% 25.60/3.80 cnf(p1090, plain, convergent_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p296, p78])).
% 25.60/3.80 fof(sdef169, definition, (spl169 <=> (convergent_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X1))), introduced(definition, [new_symbols(naming, [spl169])], [avatar_definition])).
% 25.60/3.80 cnf(ssp191, plain, (spl3 | spl48 | spl169), inference(avatar_split_clause, [status(thm)], [p1090, sdef3, sdef48, sdef169])).
% 25.60/3.80 cnf(p1092, plain, convergent_lines(sk2,X0) | distinct_lines(sk1,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0), inference(resolution, [status(thm)], [p296, p78])).
% 25.60/3.80 cnf(ssp192, plain, (spl52 | spl62), inference(avatar_split_clause, [status(thm)], [p1092, sdef52, sdef62])).
% 25.60/3.80 cnf(p1093, plain, convergent_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(X2,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X2,sk1) | apart_point_and_line(X2,X1), inference(resolution, [status(thm)], [p296, p83])).
% 25.60/3.80 fof(sdef170, definition, (spl170 <=> (convergent_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(X2,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X2,sk1) | apart_point_and_line(X2,X1))), introduced(definition, [new_symbols(naming, [spl170])], [avatar_definition])).
% 25.60/3.80 cnf(ssp193, plain, (spl3 | spl170), inference(avatar_split_clause, [status(thm)], [p1093, sdef3, sdef170])).
% 25.60/3.80 cnf(p92, plain, distinct_lines(sk1,X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p30, c4])).
% 25.60/3.80 cnf(p1097, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),sk1) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p92, p68])).
% 25.60/3.80 fof(sdef171, definition, (spl171 <=> (distinct_lines(sk2,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X1))), introduced(definition, [new_symbols(naming, [spl171])], [avatar_definition])).
% 25.60/3.80 cnf(ssp194, plain, (spl3 | spl5 | spl171), inference(avatar_split_clause, [status(thm)], [p1097, sdef3, sdef5, sdef171])).
% 25.60/3.80 cnf(p1099, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),sk1) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p92, p73])).
% 25.60/3.80 fof(sdef172, definition, (spl172 <=> (distinct_lines(sk2,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X1))), introduced(definition, [new_symbols(naming, [spl172])], [avatar_definition])).
% 25.60/3.80 cnf(ssp195, plain, (spl3 | spl27 | spl172), inference(avatar_split_clause, [status(thm)], [p1099, sdef3, sdef27, sdef172])).
% 25.60/3.80 cnf(p1101, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),sk1) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p92, p78])).
% 25.60/3.80 fof(sdef173, definition, (spl173 <=> (distinct_lines(sk2,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X1))), introduced(definition, [new_symbols(naming, [spl173])], [avatar_definition])).
% 25.60/3.80 cnf(ssp196, plain, (spl3 | spl48 | spl173), inference(avatar_split_clause, [status(thm)], [p1101, sdef3, sdef48, sdef173])).
% 25.60/3.80 cnf(p1103, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X3,sk1) | apart_point_and_line(X3,X1), inference(resolution, [status(thm)], [p92, p83])).
% 25.60/3.80 fof(sdef174, definition, (spl174 <=> (distinct_lines(sk2,X0) | distinct_lines(X1,X2) | distinct_lines(X0,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X3,sk1) | apart_point_and_line(X3,X1))), introduced(definition, [new_symbols(naming, [spl174])], [avatar_definition])).
% 25.60/3.80 cnf(ssp197, plain, (spl3 | spl174), inference(avatar_split_clause, [status(thm)], [p1103, sdef3, sdef174])).
% 25.60/3.80 cnf(p141, plain, convergent_lines(sk2,X0) | convergent_lines(X1,X0) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p38, c13])).
% 25.60/3.80 cnf(p325, plain, convergent_lines(sk2,X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p141, c13])).
% 25.60/3.80 cnf(p1116, plain, convergent_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p325, p68])).
% 25.60/3.80 cnf(ssp198, plain, (spl2 | spl4 | spl167), inference(avatar_split_clause, [status(thm)], [p1116, sdef2, sdef4, sdef167])).
% 25.60/3.80 cnf(p1117, plain, convergent_lines(sk2,X0) | distinct_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0), inference(resolution, [status(thm)], [p325, p68])).
% 25.60/3.80 cnf(ssp199, plain, (spl6 | spl19), inference(avatar_split_clause, [status(thm)], [p1117, sdef6, sdef19])).
% 25.60/3.80 cnf(p1118, plain, convergent_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p325, p73])).
% 25.60/3.80 cnf(ssp200, plain, (spl2 | spl26 | spl168), inference(avatar_split_clause, [status(thm)], [p1118, sdef2, sdef26, sdef168])).
% 25.60/3.80 cnf(p1119, plain, convergent_lines(sk2,X0) | distinct_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0), inference(resolution, [status(thm)], [p325, p73])).
% 25.60/3.80 cnf(ssp201, plain, (spl28 | spl41), inference(avatar_split_clause, [status(thm)], [p1119, sdef28, sdef41])).
% 25.60/3.80 cnf(p1120, plain, convergent_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p325, p78])).
% 25.60/3.80 cnf(ssp202, plain, (spl2 | spl47 | spl169), inference(avatar_split_clause, [status(thm)], [p1120, sdef2, sdef47, sdef169])).
% 25.60/3.80 cnf(p1121, plain, convergent_lines(sk2,X0) | distinct_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0), inference(resolution, [status(thm)], [p325, p78])).
% 25.60/3.80 cnf(ssp203, plain, (spl49 | spl62), inference(avatar_split_clause, [status(thm)], [p1121, sdef49, sdef62])).
% 25.60/3.80 cnf(p1122, plain, convergent_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(X2,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X2,sk0) | apart_point_and_line(X2,X1), inference(resolution, [status(thm)], [p325, p83])).
% 25.60/3.80 fof(sdef175, definition, (spl175 <=> (convergent_lines(sk2,X0) | distinct_lines(X1,X0) | apart_point_and_line(X2,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(X2,sk0) | apart_point_and_line(X2,X1))), introduced(definition, [new_symbols(naming, [spl175])], [avatar_definition])).
% 25.60/3.80 cnf(ssp204, plain, (spl2 | spl175), inference(avatar_split_clause, [status(thm)], [p1122, sdef2, sdef175])).
% 25.60/3.80 cnf(p95, plain, distinct_lines(sk2,X0) | distinct_points(intersection_point(sk0,sk1),X1) | apart_point_and_line(X1,X0), inference(resolution, [status(thm)], [p93, c11])).
% 25.60/3.80 cnf(c18, plain, ~apart_point_and_line(intersection_point(sk1,sk0),sk2), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 25.60/3.80 cnf(p1129, plain, distinct_lines(sk2,sk2) | distinct_points(intersection_point(sk0,sk1),intersection_point(sk1,sk0)), inference(resolution, [status(thm)], [p95, c18])).
% 25.60/3.80 fof(sdef177, definition, (spl177 <=> (distinct_points(intersection_point(sk0,sk1),intersection_point(sk1,sk0)))), introduced(definition, [new_symbols(naming, [spl177])], [avatar_definition])).
% 25.60/3.80 cnf(ssp205, plain, (spl176 | spl177), inference(avatar_split_clause, [status(thm)], [p1129, sdef176, sdef177])).
% 25.60/3.80 cnf(p1134, plain, distinct_lines(sk2,sk2) | distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk2,sk1)), inference(resolution, [status(thm)], [p95, p45])).
% 25.60/3.80 fof(sdef178, definition, (spl178 <=> (distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl178])], [avatar_definition])).
% 25.60/3.80 cnf(ssp206, plain, (spl176 | spl178), inference(avatar_split_clause, [status(thm)], [p1134, sdef176, sdef178])).
% 25.60/3.80 cnf(p1137, plain, distinct_lines(sk2,sk2) | distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk0,sk2)), inference(resolution, [status(thm)], [p95, p60])).
% 25.60/3.80 fof(sdef179, definition, (spl179 <=> (distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl179])], [avatar_definition])).
% 25.60/3.80 cnf(ssp207, plain, (spl176 | spl179), inference(avatar_split_clause, [status(thm)], [p1137, sdef176, sdef179])).
% 25.60/3.80 cnf(p1139, plain, distinct_lines(sk2,sk2) | distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk1,sk2)), inference(resolution, [status(thm)], [p95, p63])).
% 25.60/3.80 fof(sdef180, definition, (spl180 <=> (distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl180])], [avatar_definition])).
% 25.60/3.80 cnf(ssp208, plain, (spl176 | spl180), inference(avatar_split_clause, [status(thm)], [p1139, sdef176, sdef180])).
% 25.60/3.80 cnf(p48, plain, ~apart_point_and_line(X0,sk2) | distinct_points(X0,intersection_point(sk2,X1)) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [c8, p26])).
% 25.60/3.80 cnf(p1143, plain, distinct_lines(sk2,sk2) | distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk2,X1)) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p95, p48])).
% 25.60/3.80 fof(sdef181, definition, (spl181 <=> (distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk2,X1)) | convergent_lines(sk1,X1))), introduced(definition, [new_symbols(naming, [spl181])], [avatar_definition])).
% 25.60/3.80 cnf(ssp209, plain, (spl176 | spl181), inference(avatar_split_clause, [status(thm)], [p1143, sdef176, sdef181])).
% 25.60/3.80 cnf(p50, plain, ~apart_point_and_line(X0,sk2) | distinct_points(X0,intersection_point(sk2,X1)) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [c8, p27])).
% 25.60/3.80 cnf(p1145, plain, distinct_lines(sk2,sk2) | distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk2,X1)) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p95, p50])).
% 25.60/3.80 fof(sdef182, definition, (spl182 <=> (distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk2,X1)) | convergent_lines(sk0,X1))), introduced(definition, [new_symbols(naming, [spl182])], [avatar_definition])).
% 25.60/3.80 cnf(ssp210, plain, (spl176 | spl182), inference(avatar_split_clause, [status(thm)], [p1145, sdef176, sdef182])).
% 25.60/3.80 cnf(p1147, plain, distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [p95, p56])).
% 25.60/3.80 fof(sdef183, definition, (spl183 <=> (distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl183])], [avatar_definition])).
% 25.60/3.80 cnf(ssp211, plain, (spl1 | spl183), inference(avatar_split_clause, [status(thm)], [p1147, sdef1, sdef183])).
% 25.60/3.80 cnf(p1149, plain, distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk2,sk1)), inference(resolution, [status(thm)], [p95, p57])).
% 25.60/3.80 cnf(ssp212, plain, (spl1 | spl178), inference(avatar_split_clause, [status(thm)], [p1149, sdef1, sdef178])).
% 25.60/3.80 cnf(p140, plain, convergent_lines(sk0,X0) | convergent_lines(X0,sk2), inference(resolution, [status(thm)], [p38, c2])).
% 25.60/3.80 cnf(p162, plain, convergent_lines(X0,sk2) | convergent_lines(sk0,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p140, c5])).
% 25.60/3.80 cnf(p364, plain, convergent_lines(X0,sk2) | convergent_lines(X0,sk0), inference(resolution, [status(thm)], [p162, c2])).
% 25.60/3.80 cnf(p375, plain, convergent_lines(sk2,sk0), inference(resolution, [status(thm)], [p364, c2])).
% 25.60/3.80 cnf(p380, plain, ~apart_point_and_line(X0,sk2) | distinct_points(X0,intersection_point(sk2,sk0)), inference(resolution, [status(thm)], [p375, c8])).
% 25.60/3.80 cnf(p1150, plain, distinct_lines(sk2,sk2) | distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk2,sk0)), inference(resolution, [status(thm)], [p95, p380])).
% 25.60/3.80 fof(sdef184, definition, (spl184 <=> (distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl184])], [avatar_definition])).
% 25.60/3.80 cnf(ssp213, plain, (spl176 | spl184), inference(avatar_split_clause, [status(thm)], [p1150, sdef176, sdef184])).
% 25.60/3.80 cnf(p1154, plain, distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [p95, p71])).
% 25.60/3.80 cnf(ssp214, plain, (spl25 | spl183), inference(avatar_split_clause, [status(thm)], [p1154, sdef25, sdef183])).
% 25.60/3.80 cnf(p1155, plain, distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk0,sk2)), inference(resolution, [status(thm)], [p95, p72])).
% 25.60/3.80 cnf(ssp215, plain, (spl25 | spl179), inference(avatar_split_clause, [status(thm)], [p1155, sdef25, sdef179])).
% 25.60/3.80 cnf(p1156, plain, distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [p95, p76])).
% 25.60/3.80 cnf(ssp216, plain, (spl46 | spl183), inference(avatar_split_clause, [status(thm)], [p1156, sdef46, sdef183])).
% 25.60/3.80 cnf(p1157, plain, distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | distinct_points(intersection_point(sk0,sk1),X0) | distinct_points(X0,intersection_point(sk1,sk2)), inference(resolution, [status(thm)], [p95, p77])).
% 25.60/3.80 cnf(ssp217, plain, (spl46 | spl180), inference(avatar_split_clause, [status(thm)], [p1157, sdef46, sdef180])).
% 25.60/3.80 cnf(p1158, plain, distinct_lines(sk2,line_connecting(intersection_point(sk0,sk1),X0)) | distinct_points(intersection_point(sk0,sk1),X1) | apart_point_and_line(X0,sk2) | distinct_points(X1,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [p95, p81])).
% 25.60/3.80 cnf(ssp218, plain, (spl67 | spl183), inference(avatar_split_clause, [status(thm)], [p1158, sdef67, sdef183])).
% 25.60/3.80 cnf(p127, plain, convergent_lines(sk1,X0) | convergent_lines(X0,sk2), inference(resolution, [status(thm)], [p36, c2])).
% 25.60/3.80 cnf(p155, plain, convergent_lines(X0,sk2) | convergent_lines(sk1,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p127, c5])).
% 25.60/3.80 cnf(p349, plain, convergent_lines(X0,sk2) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p155, c13])).
% 25.60/3.80 cnf(p1179, plain, convergent_lines(X0,sk2) | convergent_lines(sk1,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p349, p68])).
% 25.60/3.80 fof(sdef185, definition, (spl185 <=> (convergent_lines(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0))), introduced(definition, [new_symbols(naming, [spl185])], [avatar_definition])).
% 25.60/3.80 cnf(ssp219, plain, (spl18 | spl185), inference(avatar_split_clause, [status(thm)], [p1179, sdef18, sdef185])).
% 25.60/3.80 cnf(p1181, plain, convergent_lines(X0,sk2) | convergent_lines(sk1,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p349, p73])).
% 25.60/3.80 fof(sdef186, definition, (spl186 <=> (convergent_lines(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),X0))), introduced(definition, [new_symbols(naming, [spl186])], [avatar_definition])).
% 25.60/3.80 cnf(ssp220, plain, (spl40 | spl186), inference(avatar_split_clause, [status(thm)], [p1181, sdef40, sdef186])).
% 25.60/3.80 cnf(p1183, plain, convergent_lines(X0,sk2) | convergent_lines(sk1,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p349, p78])).
% 25.60/3.80 fof(sdef187, definition, (spl187 <=> (convergent_lines(X0,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0))), introduced(definition, [new_symbols(naming, [spl187])], [avatar_definition])).
% 25.60/3.80 cnf(ssp221, plain, (spl61 | spl187), inference(avatar_split_clause, [status(thm)], [p1183, sdef61, sdef187])).
% 25.60/3.80 cnf(p96, plain, distinct_lines(sk2,X0) | distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X1), inference(resolution, [status(thm)], [p93, c12])).
% 25.60/3.80 cnf(p1189, plain, distinct_lines(sk2,X0) | distinct_lines(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))) | distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [p96, p56])).
% 25.60/3.80 fof(sdef188, definition, (spl188 <=> (distinct_lines(sk2,X0) | distinct_lines(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk2,sk1))))), introduced(definition, [new_symbols(naming, [spl188])], [avatar_definition])).
% 25.60/3.80 cnf(ssp222, plain, (spl0 | spl188), inference(avatar_split_clause, [status(thm)], [p1189, sdef0, sdef188])).
% 25.60/3.80 cnf(p1193, plain, distinct_lines(sk2,X0) | distinct_lines(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))) | distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [p96, p71])).
% 25.60/3.80 fof(sdef189, definition, (spl189 <=> (distinct_lines(sk2,X0) | distinct_lines(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk0,sk2))))), introduced(definition, [new_symbols(naming, [spl189])], [avatar_definition])).
% 25.60/3.80 cnf(ssp223, plain, (spl0 | spl189), inference(avatar_split_clause, [status(thm)], [p1193, sdef0, sdef189])).
% 25.60/3.80 cnf(p1195, plain, distinct_lines(sk2,X0) | distinct_lines(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))) | distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [p96, p76])).
% 25.60/3.80 fof(sdef190, definition, (spl190 <=> (distinct_lines(sk2,X0) | distinct_lines(X0,line_connecting(intersection_point(sk0,sk1),intersection_point(sk1,sk2))))), introduced(definition, [new_symbols(naming, [spl190])], [avatar_definition])).
% 25.60/3.80 cnf(ssp224, plain, (spl0 | spl190), inference(avatar_split_clause, [status(thm)], [p1195, sdef0, sdef190])).
% 25.60/3.80 cnf(p1197, plain, distinct_lines(sk2,X0) | distinct_lines(X0,line_connecting(intersection_point(sk0,sk1),X1)) | apart_point_and_line(X1,sk2) | distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [p96, p81])).
% 25.60/3.80 fof(sdef191, definition, (spl191 <=> (distinct_lines(sk2,X0) | distinct_lines(X0,line_connecting(intersection_point(sk0,sk1),X1)) | apart_point_and_line(X1,sk2))), introduced(definition, [new_symbols(naming, [spl191])], [avatar_definition])).
% 25.60/3.80 cnf(ssp225, plain, (spl0 | spl191), inference(avatar_split_clause, [status(thm)], [p1197, sdef0, sdef191])).
% 25.60/3.80 cnf(p98, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(sk0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p31, c4])).
% 25.60/3.80 cnf(p1225, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(sk0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk2,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X2), inference(resolution, [status(thm)], [p98, p68])).
% 25.60/3.80 cnf(ssp226, plain, (spl6 | spl157), inference(avatar_split_clause, [status(thm)], [p1225, sdef6, sdef157])).
% 25.60/3.80 cnf(p1226, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(sk0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk2),X2), inference(resolution, [status(thm)], [p98, p73])).
% 25.60/3.80 cnf(ssp227, plain, (spl28 | spl159), inference(avatar_split_clause, [status(thm)], [p1226, sdef28, sdef159])).
% 25.60/3.80 cnf(p1227, plain, distinct_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(sk0,X2) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk1),X2) | apart_point_and_line(intersection_point(sk1,sk2),X1) | apart_point_and_line(intersection_point(sk1,sk2),X2), inference(resolution, [status(thm)], [p98, p78])).
% 25.60/3.80 cnf(ssp228, plain, (spl49 | spl161), inference(avatar_split_clause, [status(thm)], [p1227, sdef49, sdef161])).
% 25.60/3.80 cnf(p366, plain, convergent_lines(X0,sk2) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p162, c13])).
% 25.60/3.80 cnf(p1244, plain, convergent_lines(X0,sk2) | convergent_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p366, p68])).
% 25.60/3.80 cnf(ssp229, plain, (spl17 | spl185), inference(avatar_split_clause, [status(thm)], [p1244, sdef17, sdef185])).
% 25.60/3.80 cnf(p1245, plain, convergent_lines(X0,sk2) | convergent_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p366, p73])).
% 25.60/3.80 cnf(ssp230, plain, (spl39 | spl186), inference(avatar_split_clause, [status(thm)], [p1245, sdef39, sdef186])).
% 25.60/3.80 cnf(p1246, plain, convergent_lines(X0,sk2) | convergent_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p366, p78])).
% 25.60/3.80 cnf(ssp231, plain, (spl60 | spl187), inference(avatar_split_clause, [status(thm)], [p1246, sdef60, sdef187])).
% 25.60/3.80 cnf(p99, plain, distinct_lines(sk0,X0) | distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p31, c4])).
% 25.60/3.80 cnf(p1265, plain, distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X0), inference(resolution, [status(thm)], [p99, p68])).
% 25.60/3.80 cnf(ssp232, plain, (spl2 | spl4 | spl163), inference(avatar_split_clause, [status(thm)], [p1265, sdef2, sdef4, sdef163])).
% 25.60/3.80 cnf(p1266, plain, distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0), inference(resolution, [status(thm)], [p99, p73])).
% 25.60/3.80 cnf(ssp233, plain, (spl2 | spl26 | spl164), inference(avatar_split_clause, [status(thm)], [p1266, sdef2, sdef26, sdef164])).
% 25.60/3.80 cnf(p1267, plain, distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X0), inference(resolution, [status(thm)], [p99, p78])).
% 25.60/3.80 cnf(ssp234, plain, (spl2 | spl47 | spl165), inference(avatar_split_clause, [status(thm)], [p1267, sdef2, sdef47, sdef165])).
% 25.60/3.80 cnf(p1268, plain, distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X3,sk0) | apart_point_and_line(X3,X0), inference(resolution, [status(thm)], [p99, p83])).
% 25.60/3.80 fof(sdef192, definition, (spl192 <=> (distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2) | apart_point_and_line(X3,sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(X3,sk0) | apart_point_and_line(X3,X0))), introduced(definition, [new_symbols(naming, [spl192])], [avatar_definition])).
% 25.60/3.80 cnf(ssp235, plain, (spl2 | spl192), inference(avatar_split_clause, [status(thm)], [p1268, sdef2, sdef192])).
% 25.60/3.80 cnf(p154, plain, convergent_lines(sk1,X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p127, c13])).
% 25.60/3.80 cnf(p169, plain, distinct_lines(X0,sk2) | convergent_lines(sk1,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p154, c5])).
% 25.60/3.80 cnf(p390, plain, distinct_lines(X0,sk2) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p169, c13])).
% 25.60/3.80 cnf(p1290, plain, distinct_lines(X0,sk2) | convergent_lines(sk1,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p390, p68])).
% 25.60/3.80 cnf(ssp236, plain, (spl12 | spl18), inference(avatar_split_clause, [status(thm)], [p1290, sdef12, sdef18])).
% 25.60/3.80 cnf(p1291, plain, distinct_lines(X0,sk2) | convergent_lines(sk1,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p390, p73])).
% 25.60/3.80 cnf(ssp237, plain, (spl34 | spl40), inference(avatar_split_clause, [status(thm)], [p1291, sdef34, sdef40])).
% 25.60/3.80 cnf(p1292, plain, distinct_lines(X0,sk2) | convergent_lines(sk1,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p390, p78])).
% 25.60/3.80 cnf(ssp238, plain, (spl55 | spl61), inference(avatar_split_clause, [status(thm)], [p1292, sdef55, sdef61])).
% 25.60/3.80 cnf(p161, plain, convergent_lines(sk0,X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p140, c13])).
% 25.60/3.80 cnf(p183, plain, distinct_lines(X0,sk2) | convergent_lines(sk0,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p161, c5])).
% 25.60/3.80 cnf(p406, plain, distinct_lines(X0,sk2) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p183, c13])).
% 25.60/3.80 cnf(p1301, plain, distinct_lines(X0,sk2) | convergent_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p406, p68])).
% 25.60/3.80 cnf(ssp239, plain, (spl12 | spl17), inference(avatar_split_clause, [status(thm)], [p1301, sdef12, sdef17])).
% 25.60/3.80 cnf(p1302, plain, distinct_lines(X0,sk2) | convergent_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1), inference(resolution, [status(thm)], [p406, p73])).
% 25.60/3.80 cnf(ssp240, plain, (spl34 | spl39), inference(avatar_split_clause, [status(thm)], [p1302, sdef34, sdef39])).
% 25.60/3.80 cnf(p1303, plain, distinct_lines(X0,sk2) | convergent_lines(sk0,X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [p406, p78])).
% 25.60/3.80 cnf(ssp241, plain, (spl55 | spl60), inference(avatar_split_clause, [status(thm)], [p1303, sdef55, sdef60])).
% 25.60/3.80 cnf(p111, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X1) | ~apart_point_and_line(X2,X0) | distinct_points(X2,intersection_point(X0,X1)), inference(resolution, [status(thm)], [p33, c8])).
% 25.60/3.80 cnf(p1425, plain, (convergent_lines(sk0,sk0) | convergent_lines(sk1,X0) | distinct_points(intersection_point(sk2,sk1),intersection_point(sk0,X0)) | ~spl4), inference(resolution, [status(thm)], [p111, p447])).
% 25.60/3.80 fof(sdef193, definition, (spl193 <=> (convergent_lines(sk1,X0) | distinct_points(intersection_point(sk2,sk1),intersection_point(sk0,X0)))), introduced(definition, [new_symbols(naming, [spl193])], [avatar_definition])).
% 25.60/3.80 cnf(ssp242, plain, (~spl4 | spl24 | spl193), inference(avatar_split_clause, [status(thm)], [p1425, sdef24, sdef193])).
% 25.60/3.80 cnf(p1427, plain, (convergent_lines(sk0,sk0) | convergent_lines(sk1,X0) | distinct_points(intersection_point(sk1,sk2),intersection_point(sk0,X0)) | ~spl47), inference(resolution, [status(thm)], [p111, p637])).
% 25.60/3.80 fof(sdef194, definition, (spl194 <=> (convergent_lines(sk1,X0) | distinct_points(intersection_point(sk1,sk2),intersection_point(sk0,X0)))), introduced(definition, [new_symbols(naming, [spl194])], [avatar_definition])).
% 25.60/3.80 cnf(ssp243, plain, (~spl47 | spl24 | spl194), inference(avatar_split_clause, [status(thm)], [p1427, sdef24, sdef194])).
% 25.60/3.80 cnf(p777, plain, (apart_point_and_line(X0,sk2) | apart_point_and_line(X0,sk0) | apart_point_and_line(X0,sk1) | ~spl74), inference(avatar_component_clause, [status(thm)], [sdef74])).
% 25.60/3.80 cnf(p1460, plain, (apart_point_and_line(intersection_point(sk1,sk0),sk0) | apart_point_and_line(intersection_point(sk1,sk0),sk1) | ~spl74), inference(resolution, [status(thm)], [p777, c18])).
% 25.60/3.80 cnf(ssp244, plain, (~spl74 | spl195 | spl196), inference(avatar_split_clause, [status(thm)], [p1460, sdef195, sdef196])).
% 25.60/3.80 cnf(p1478, plain, (distinct_points(intersection_point(sk1,sk0),intersection_point(sk2,sk0)) | convergent_lines(sk0,sk0) | ~spl195), inference(resolution, [status(thm)], [p1461, p64])).
% 25.60/3.80 fof(sdef197, definition, (spl197 <=> (distinct_points(intersection_point(sk1,sk0),intersection_point(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl197])], [avatar_definition])).
% 25.60/3.80 cnf(ssp245, plain, (~spl195 | spl24 | spl197), inference(avatar_split_clause, [status(thm)], [p1478, sdef24, sdef197])).
% 25.60/3.80 cnf(p1482, plain, (convergent_lines(sk0,sk0) | convergent_lines(sk1,X0) | distinct_points(intersection_point(sk1,sk0),intersection_point(sk0,X0)) | ~spl195), inference(resolution, [status(thm)], [p1461, p111])).
% 25.60/3.80 fof(sdef198, definition, (spl198 <=> (convergent_lines(sk1,X0) | distinct_points(intersection_point(sk1,sk0),intersection_point(sk0,X0)))), introduced(definition, [new_symbols(naming, [spl198])], [avatar_definition])).
% 25.60/3.80 cnf(ssp246, plain, (~spl195 | spl24 | spl198), inference(avatar_split_clause, [status(thm)], [p1482, sdef24, sdef198])).
% 25.60/3.80 cnf(p114, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X1) | ~apart_point_and_line(X2,X1) | distinct_points(X2,intersection_point(X0,X1)), inference(resolution, [status(thm)], [p33, c9])).
% 25.60/3.80 cnf(p1495, plain, (convergent_lines(sk0,X0) | convergent_lines(sk1,sk1) | distinct_points(intersection_point(sk0,sk2),intersection_point(X0,sk1)) | ~spl27), inference(resolution, [status(thm)], [p114, p544])).
% 25.60/3.80 fof(sdef199, definition, (spl199 <=> (convergent_lines(sk0,X0) | distinct_points(intersection_point(sk0,sk2),intersection_point(X0,sk1)))), introduced(definition, [new_symbols(naming, [spl199])], [avatar_definition])).
% 25.60/3.80 cnf(ssp247, plain, (~spl27 | spl199 | spl200), inference(avatar_split_clause, [status(thm)], [p1495, sdef199, sdef200])).
% 25.60/3.80 cnf(p1499, plain, (convergent_lines(sk0,X0) | convergent_lines(sk1,sk1) | distinct_points(intersection_point(sk1,sk0),intersection_point(X0,sk1)) | ~spl196), inference(resolution, [status(thm)], [p114, p1462])).
% 25.60/3.80 fof(sdef201, definition, (spl201 <=> (convergent_lines(sk0,X0) | distinct_points(intersection_point(sk1,sk0),intersection_point(X0,sk1)))), introduced(definition, [new_symbols(naming, [spl201])], [avatar_definition])).
% 25.60/3.80 cnf(ssp248, plain, (~spl196 | spl200 | spl201), inference(avatar_split_clause, [status(thm)], [p1499, sdef200, sdef201])).
% 25.60/3.80 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, ssp213, ssp214, ssp215, ssp216, ssp217, ssp218, ssp219, ssp220, ssp221, ssp222, ssp223, ssp224, ssp225, ssp226, ssp227, ssp228, ssp229, ssp230, ssp231, ssp232, ssp233, ssp234, ssp235, ssp236, ssp237, ssp238, ssp239, ssp240, ssp241, ssp242, ssp243, ssp244, ssp245, ssp246, ssp247, ssp248, sct0, sct1, sct2, sct3, sct4, sct5, sct6, sct7, sct8, sct9, sct10, sct11, sct12, sct13])).
% 25.60/3.80 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------