%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO198+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:25 PM UTC 2026
% Result : Theorem 25.57s 3.87s
% Output : Proof 25.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO198+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.07/0.35 % Computer : n006.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Wed Sep 23 11:26:17 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 25.57/3.87 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 25.57/3.87 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 25.57/3.87 fof(sdef0, definition, (spl0 <=> (distinct_points(intersection_point(sk0,sk2),intersection_point(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 25.57/3.87 cnf(p425, plain, (distinct_points(intersection_point(sk0,sk2),intersection_point(sk0,sk2)) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 25.57/3.87 fof(f0, axiom, ! [X] : ~ distinct_points(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart1)).
% 25.57/3.87 fof(f0_nnf, plain, ! [X] : (~(distinct_points(X,X))), inference(nnf_transformation, [status(thm)], [f0])).
% 25.57/3.87 fof(f0_sk, plain, ! [X] : (~(distinct_points(X,X))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 25.57/3.87 cnf(c0, plain, ~distinct_points(X0,X0), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 25.57/3.87 cnf(p427, plain, ($false | ~spl0), inference(resolution, [status(thm)], [p425, c0])).
% 25.57/3.87 cnf(sct0, plain, (~spl0), inference(avatar_contradiction_clause, [status(thm)], [p427])).
% 25.57/3.87 fof(sdef27, definition, (spl27 <=> (convergent_lines(sk0,sk0))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 25.57/3.87 cnf(p541, plain, (convergent_lines(sk0,sk0) | ~spl27), inference(avatar_component_clause, [status(thm)], [sdef27])).
% 25.57/3.87 fof(f2, axiom, ! [X] : ~ convergent_lines(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart3)).
% 25.57/3.87 fof(f2_nnf, plain, ! [X] : (~(convergent_lines(X,X))), inference(nnf_transformation, [status(thm)], [f2])).
% 25.57/3.87 fof(f2_sk, plain, ! [X] : (~(convergent_lines(X,X))), inference(skolemisation, [status(esa)], [f2_nnf])).
% 25.57/3.87 cnf(c2, plain, ~convergent_lines(X0,X0), inference(cnf_transformation, [status(esa)], [f2_sk])).
% 25.57/3.87 cnf(p543, plain, ($false | ~spl27), inference(resolution, [status(thm)], [p541, c2])).
% 25.57/3.87 cnf(sct1, plain, (~spl27), inference(avatar_contradiction_clause, [status(thm)], [p543])).
% 25.57/3.87 fof(sdef30, definition, (spl30 <=> (apart_point_and_line(intersection_point(sk0,sk1),sk2))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 25.57/3.87 cnf(p562, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk2) | ~spl30), inference(avatar_component_clause, [status(thm)], [sdef30])).
% 25.57/3.87 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(X,Z),Y) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 25.57/3.87 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(X,Z),Y) )), inference(negated_conjecture, [status(cth)], [f12])).
% 25.57/3.87 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(X,Z),Y))), inference(nnf_transformation, [status(thm)], [f12_neg])).
% 25.57/3.87 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(sk0,sk2),sk1)), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2])], [f12_nnf])).
% 25.57/3.87 cnf(c17, plain, ~apart_point_and_line(intersection_point(sk0,sk1),sk2), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 25.57/3.87 cnf(p630, plain, ($false | ~spl30), inference(resolution, [status(thm)], [p562, c17])).
% 25.57/3.87 cnf(sct2, plain, (~spl30), inference(avatar_contradiction_clause, [status(thm)], [p630])).
% 25.57/3.87 fof(sdef4, definition, (spl4 <=> (apart_point_and_line(intersection_point(sk0,sk2),sk2))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 25.57/3.87 cnf(p481, plain, (apart_point_and_line(intersection_point(sk0,sk2),sk2) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 25.57/3.87 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.57/3.87 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.57/3.87 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.57/3.87 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.57/3.87 cnf(c16, plain, convergent_lines(sk0,sk2), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 25.57/3.87 cnf(p56, plain, ~apart_point_and_line(X0,sk2) | distinct_points(X0,intersection_point(sk0,sk2)), inference(resolution, [status(thm)], [c9, c16])).
% 25.57/3.87 cnf(p544, plain, (distinct_points(intersection_point(sk0,sk2),intersection_point(sk0,sk2)) | ~spl4), inference(resolution, [status(thm)], [p481, p56])).
% 25.57/3.87 cnf(p637, plain, ($false | ~spl4), inference(resolution, [status(thm)], [p544, c0])).
% 25.57/3.87 cnf(sct3, plain, (~spl4), inference(avatar_contradiction_clause, [status(thm)], [p637])).
% 25.57/3.87 fof(sdef6, definition, (spl6 <=> (apart_point_and_line(intersection_point(sk1,sk2),sk2))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 25.57/3.87 cnf(p483, plain, (apart_point_and_line(intersection_point(sk1,sk2),sk2) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 25.57/3.87 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.57/3.87 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.57/3.87 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.57/3.87 cnf(c5, plain, ~convergent_lines(X0,X1) | convergent_lines(X0,X2) | convergent_lines(X1,X2), inference(cnf_transformation, [status(esa)], [f5_sk])).
% 25.57/3.87 cnf(c15, plain, convergent_lines(sk2,sk1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 25.57/3.87 cnf(p26, plain, convergent_lines(sk2,X0) | convergent_lines(sk1,X0), inference(resolution, [status(thm)], [c5, c15])).
% 25.57/3.87 cnf(p34, plain, convergent_lines(sk1,sk2), inference(resolution, [status(thm)], [p26, c2])).
% 25.57/3.87 cnf(p59, plain, ~apart_point_and_line(X0,sk2) | distinct_points(X0,intersection_point(sk1,sk2)), inference(resolution, [status(thm)], [c9, p34])).
% 25.57/3.87 cnf(p615, plain, (distinct_points(intersection_point(sk1,sk2),intersection_point(sk1,sk2)) | ~spl6), inference(resolution, [status(thm)], [p483, p59])).
% 25.57/3.87 cnf(p733, plain, ($false | ~spl6), inference(resolution, [status(thm)], [p615, c0])).
% 25.57/3.87 cnf(sct4, plain, (~spl6), inference(avatar_contradiction_clause, [status(thm)], [p733])).
% 25.57/3.87 fof(sdef3, definition, (spl3 <=> (apart_point_and_line(intersection_point(sk0,sk2),sk0))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 25.57/3.87 cnf(p480, plain, (apart_point_and_line(intersection_point(sk0,sk2),sk0) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 25.57/3.87 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.57/3.87 cnf(p46, plain, ~apart_point_and_line(X0,sk0) | distinct_points(X0,intersection_point(sk0,sk2)), inference(resolution, [status(thm)], [c8, c16])).
% 25.57/3.87 cnf(p534, plain, (distinct_points(intersection_point(sk0,sk2),intersection_point(sk0,sk2)) | ~spl3), inference(resolution, [status(thm)], [p480, p46])).
% 25.57/3.87 cnf(p751, plain, ($false | ~spl3), inference(resolution, [status(thm)], [p534, c0])).
% 25.57/3.87 cnf(sct5, plain, (~spl3), inference(avatar_contradiction_clause, [status(thm)], [p751])).
% 25.57/3.87 fof(sdef29, definition, (spl29 <=> (apart_point_and_line(intersection_point(sk0,sk1),sk0))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 25.57/3.87 cnf(p561, plain, (apart_point_and_line(intersection_point(sk0,sk1),sk0) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 25.57/3.87 cnf(c14, plain, convergent_lines(sk0,sk1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 25.57/3.87 cnf(p44, plain, ~apart_point_and_line(X0,sk0) | distinct_points(X0,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [c8, c14])).
% 25.57/3.87 cnf(p621, plain, (distinct_points(intersection_point(sk0,sk1),intersection_point(sk0,sk1)) | ~spl29), inference(resolution, [status(thm)], [p561, p44])).
% 25.57/3.87 cnf(p752, plain, ($false | ~spl29), inference(resolution, [status(thm)], [p621, c0])).
% 25.57/3.87 cnf(sct6, plain, (~spl29), inference(avatar_contradiction_clause, [status(thm)], [p752])).
% 25.57/3.87 cnf(p49, plain, ~apart_point_and_line(X0,sk1) | distinct_points(X0,intersection_point(sk1,sk2)), inference(resolution, [status(thm)], [c8, p34])).
% 25.57/3.87 cnf(c18, plain, apart_point_and_line(intersection_point(sk0,sk2),sk1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 25.57/3.87 cnf(p64, plain, distinct_points(intersection_point(sk0,sk2),intersection_point(sk1,sk2)), inference(resolution, [status(thm)], [p49, c18])).
% 25.57/3.87 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.57/3.87 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.57/3.87 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.57/3.87 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.57/3.87 cnf(p66, plain, ~apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk2),intersection_point(sk1,sk2))) | distinct_points(X0,intersection_point(sk0,sk2)), inference(resolution, [status(thm)], [p64, c6])).
% 25.57/3.87 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.57/3.87 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.57/3.87 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.57/3.87 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.57/3.87 cnf(p93, plain, distinct_lines(sk1,X0) | apart_point_and_line(intersection_point(sk0,sk2),X0), inference(resolution, [status(thm)], [c12, c18])).
% 25.57/3.87 cnf(p424, plain, distinct_points(intersection_point(sk0,sk2),intersection_point(sk0,sk2)) | distinct_lines(sk1,line_connecting(intersection_point(sk0,sk2),intersection_point(sk1,sk2))), inference(resolution, [status(thm)], [p66, p93])).
% 25.57/3.87 fof(sdef1, definition, (spl1 <=> (distinct_lines(sk1,line_connecting(intersection_point(sk0,sk2),intersection_point(sk1,sk2))))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 25.57/3.87 cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [p424, sdef0, sdef1])).
% 25.57/3.87 cnf(p54, plain, ~apart_point_and_line(X0,sk1) | distinct_points(X0,intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [c9, c14])).
% 25.57/3.87 cnf(p68, plain, distinct_points(intersection_point(sk0,sk2),intersection_point(sk0,sk1)), inference(resolution, [status(thm)], [p54, c18])).
% 25.57/3.87 cnf(p70, plain, ~apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk2),intersection_point(sk0,sk1))) | distinct_points(X0,intersection_point(sk0,sk2)), inference(resolution, [status(thm)], [p68, c6])).
% 25.57/3.87 cnf(p446, plain, distinct_points(intersection_point(sk0,sk2),intersection_point(sk0,sk2)) | distinct_lines(sk1,line_connecting(intersection_point(sk0,sk2),intersection_point(sk0,sk1))), inference(resolution, [status(thm)], [p70, p93])).
% 25.57/3.87 fof(sdef2, definition, (spl2 <=> (distinct_lines(sk1,line_connecting(intersection_point(sk0,sk2),intersection_point(sk0,sk1))))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 25.57/3.87 cnf(ssp1, plain, (spl0 | spl2), inference(avatar_split_clause, [status(thm)], [p446, sdef0, sdef2])).
% 25.57/3.87 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.57/3.87 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.57/3.87 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.57/3.87 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.57/3.87 cnf(p72, plain, ~distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1), inference(resolution, [status(thm)], [c10, p64])).
% 25.57/3.87 fof(f11, axiom, ! [X,Y] : ( convergent_lines(X,Y) => distinct_lines(X,Y) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ceq3)).
% 25.57/3.87 fof(f11_nnf, plain, ! [X,Y] : ((~(convergent_lines(X,Y)) | distinct_lines(X,Y))), inference(nnf_transformation, [status(thm)], [f11])).
% 25.57/3.87 fof(f11_sk, plain, ! [X,Y] : ((~(convergent_lines(X,Y)) | distinct_lines(X,Y))), inference(skolemisation, [status(esa)], [f11_nnf])).
% 25.57/3.87 cnf(c13, plain, ~convergent_lines(X0,X1) | distinct_lines(X0,X1), inference(cnf_transformation, [status(esa)], [f11_sk])).
% 25.57/3.87 cnf(p21, plain, distinct_lines(sk0,sk2), inference(resolution, [status(thm)], [c13, c16])).
% 25.57/3.87 cnf(p479, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),sk2), inference(resolution, [status(thm)], [p72, p21])).
% 25.57/3.87 fof(sdef5, definition, (spl5 <=> (apart_point_and_line(intersection_point(sk1,sk2),sk0))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 25.57/3.87 cnf(ssp2, plain, (spl3 | spl4 | spl5 | spl6), inference(avatar_split_clause, [status(thm)], [p479, sdef3, sdef4, sdef5, sdef6])).
% 25.57/3.87 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.57/3.87 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.57/3.87 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.57/3.87 cnf(c4, plain, ~distinct_lines(X0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 25.57/3.87 cnf(p24, plain, distinct_lines(sk0,X0) | distinct_lines(sk2,X0), inference(resolution, [status(thm)], [c4, p21])).
% 25.57/3.87 cnf(p484, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk2) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk0,X0), inference(resolution, [status(thm)], [p72, p24])).
% 25.57/3.87 fof(sdef7, definition, (spl7 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 25.57/3.87 cnf(ssp3, plain, (spl4 | spl6 | spl7), inference(avatar_split_clause, [status(thm)], [p484, sdef4, sdef6, sdef7])).
% 25.57/3.87 cnf(p19, plain, distinct_lines(sk0,sk1), inference(resolution, [status(thm)], [c13, c14])).
% 25.57/3.87 cnf(p22, plain, distinct_lines(sk0,X0) | distinct_lines(sk1,X0), inference(resolution, [status(thm)], [c4, p19])).
% 25.57/3.87 cnf(p28, plain, distinct_lines(sk0,X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p22, c4])).
% 25.57/3.87 cnf(p486, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p72, p28])).
% 25.57/3.87 fof(sdef8, definition, (spl8 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 25.57/3.87 cnf(ssp4, plain, (spl3 | spl5 | spl8), inference(avatar_split_clause, [status(thm)], [p486, sdef3, sdef5, sdef8])).
% 25.57/3.87 fof(f1, axiom, ! [X] : ~ distinct_lines(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart2)).
% 25.57/3.87 fof(f1_nnf, plain, ! [X] : (~(distinct_lines(X,X))), inference(nnf_transformation, [status(thm)], [f1])).
% 25.57/3.87 fof(f1_sk, plain, ! [X] : (~(distinct_lines(X,X))), inference(skolemisation, [status(esa)], [f1_nnf])).
% 25.57/3.87 cnf(c1, plain, ~distinct_lines(X0,X0), inference(cnf_transformation, [status(esa)], [f1_sk])).
% 25.57/3.87 cnf(p84, plain, distinct_lines(sk0,X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p28, c1])).
% 25.57/3.87 cnf(p488, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p72, p84])).
% 25.57/3.87 fof(sdef9, definition, (spl9 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X0,sk1))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 25.57/3.87 cnf(ssp5, plain, (spl3 | spl5 | spl9), inference(avatar_split_clause, [status(thm)], [p488, sdef3, sdef5, sdef9])).
% 25.57/3.87 cnf(p31, plain, distinct_lines(sk0,X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p24, c4])).
% 25.57/3.87 cnf(p490, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p72, p31])).
% 25.57/3.87 fof(sdef10, definition, (spl10 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 25.57/3.87 cnf(ssp6, plain, (spl3 | spl5 | spl10), inference(avatar_split_clause, [status(thm)], [p490, sdef3, sdef5, sdef10])).
% 25.57/3.87 cnf(p492, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk2) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p72, p31])).
% 25.57/3.87 fof(sdef11, definition, (spl11 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 25.57/3.87 cnf(ssp7, plain, (spl4 | spl6 | spl11), inference(avatar_split_clause, [status(thm)], [p492, sdef4, sdef6, sdef11])).
% 25.57/3.87 cnf(p494, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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(sk2,X1), inference(resolution, [status(thm)], [p72, p31])).
% 25.57/3.87 fof(sdef12, definition, (spl12 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 25.57/3.87 cnf(ssp8, plain, (spl7 | spl12), inference(avatar_split_clause, [status(thm)], [p494, sdef7, sdef12])).
% 25.57/3.87 cnf(p97, plain, distinct_lines(sk0,X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p31, c1])).
% 25.57/3.87 cnf(p496, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p72, p97])).
% 25.57/3.87 fof(sdef13, definition, (spl13 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X0,sk2))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 25.57/3.87 cnf(ssp9, plain, (spl3 | spl5 | spl13), inference(avatar_split_clause, [status(thm)], [p496, sdef3, sdef5, sdef13])).
% 25.57/3.87 cnf(p35, plain, convergent_lines(sk1,X0) | distinct_lines(sk2,X0), inference(resolution, [status(thm)], [p26, c13])).
% 25.57/3.87 cnf(p41, plain, distinct_lines(sk2,X0) | convergent_lines(sk1,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p35, c5])).
% 25.57/3.87 cnf(p191, plain, distinct_lines(sk2,X0) | convergent_lines(X0,sk1), inference(resolution, [status(thm)], [p41, c2])).
% 25.57/3.87 cnf(p200, plain, distinct_lines(sk2,X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p191, c13])).
% 25.57/3.87 cnf(p498, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk2) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p72, p200])).
% 25.57/3.87 cnf(ssp10, plain, (spl4 | spl6 | spl9), inference(avatar_split_clause, [status(thm)], [p498, sdef4, sdef6, sdef9])).
% 25.57/3.87 cnf(p27, plain, convergent_lines(sk0,X0) | convergent_lines(sk2,X0), inference(resolution, [status(thm)], [c5, c16])).
% 25.57/3.87 cnf(p37, plain, convergent_lines(sk0,X0) | distinct_lines(sk2,X0), inference(resolution, [status(thm)], [p27, c13])).
% 25.57/3.87 cnf(p43, plain, distinct_lines(sk2,X0) | convergent_lines(sk0,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p37, c5])).
% 25.57/3.87 cnf(p205, plain, distinct_lines(sk2,X0) | convergent_lines(X0,sk0), inference(resolution, [status(thm)], [p43, c2])).
% 25.57/3.87 cnf(p214, plain, distinct_lines(sk2,X0) | distinct_lines(X0,sk0), inference(resolution, [status(thm)], [p205, c13])).
% 25.57/3.87 cnf(p499, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk2) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X0,sk0), inference(resolution, [status(thm)], [p72, p214])).
% 25.57/3.87 fof(sdef14, definition, (spl14 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X0,sk0))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 25.57/3.87 cnf(ssp11, plain, (spl4 | spl6 | spl14), inference(avatar_split_clause, [status(thm)], [p499, sdef4, sdef6, sdef14])).
% 25.57/3.87 cnf(p501, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | distinct_lines(sk2,X0), inference(resolution, [status(thm)], [p72, p214])).
% 25.57/3.87 cnf(ssp12, plain, (spl3 | spl5 | spl12), inference(avatar_split_clause, [status(thm)], [p501, sdef3, sdef5, sdef12])).
% 25.57/3.87 cnf(p88, plain, distinct_lines(X0,sk1) | distinct_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p84, c4])).
% 25.57/3.87 cnf(p502, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p72, p88])).
% 25.57/3.87 fof(sdef15, definition, (spl15 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 25.57/3.87 cnf(ssp13, plain, (spl3 | spl5 | spl15), inference(avatar_split_clause, [status(thm)], [p502, sdef3, sdef5, sdef15])).
% 25.57/3.87 cnf(p504, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p72, p88])).
% 25.57/3.87 cnf(ssp14, plain, (spl7 | spl9), inference(avatar_split_clause, [status(thm)], [p504, sdef7, sdef9])).
% 25.57/3.87 cnf(p20, plain, distinct_lines(sk2,sk1), inference(resolution, [status(thm)], [c13, c15])).
% 25.57/3.87 cnf(p23, plain, distinct_lines(sk2,X0) | distinct_lines(sk1,X0), inference(resolution, [status(thm)], [c4, p20])).
% 25.57/3.87 cnf(p30, plain, distinct_lines(sk1,X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p23, c4])).
% 25.57/3.87 cnf(p89, plain, distinct_lines(sk1,X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p30, c1])).
% 25.57/3.87 cnf(p94, plain, distinct_lines(X0,sk2) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p89, c4])).
% 25.57/3.87 cnf(p505, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk2) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p72, p94])).
% 25.57/3.87 cnf(ssp15, plain, (spl4 | spl6 | spl8), inference(avatar_split_clause, [status(thm)], [p505, sdef4, sdef6, sdef8])).
% 25.57/3.87 cnf(p101, plain, distinct_lines(X0,sk2) | distinct_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p97, c4])).
% 25.57/3.87 cnf(p506, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk2) | distinct_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p72, p101])).
% 25.57/3.87 fof(sdef16, definition, (spl16 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 25.57/3.87 cnf(ssp16, plain, (spl4 | spl6 | spl16), inference(avatar_split_clause, [status(thm)], [p506, sdef4, sdef6, sdef16])).
% 25.57/3.87 cnf(p508, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p72, p101])).
% 25.57/3.87 fof(sdef17, definition, (spl17 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 25.57/3.87 cnf(ssp17, plain, (spl3 | spl5 | spl17), inference(avatar_split_clause, [status(thm)], [p508, sdef3, sdef5, sdef17])).
% 25.57/3.87 cnf(p510, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p72, p101])).
% 25.57/3.87 cnf(ssp18, plain, (spl7 | spl13), inference(avatar_split_clause, [status(thm)], [p510, sdef7, sdef13])).
% 25.57/3.87 cnf(p25, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X0), inference(resolution, [status(thm)], [c5, c14])).
% 25.57/3.87 cnf(p33, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p25, c5])).
% 25.57/3.87 cnf(p105, plain, convergent_lines(sk0,X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p33, c13])).
% 25.57/3.87 cnf(p511, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p72, p105])).
% 25.57/3.87 fof(sdef18, definition, (spl18 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 25.57/3.87 fof(sdef19, definition, (spl19 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(sk1,X0))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 25.57/3.87 cnf(ssp19, plain, (spl18 | spl19), inference(avatar_split_clause, [status(thm)], [p511, sdef18, sdef19])).
% 25.57/3.87 cnf(p36, plain, convergent_lines(sk1,X0) | convergent_lines(sk2,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p26, c5])).
% 25.57/3.87 cnf(p130, plain, convergent_lines(sk1,X0) | convergent_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p36, c13])).
% 25.57/3.87 cnf(p514, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p72, p130])).
% 25.57/3.87 fof(sdef20, definition, (spl20 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 25.57/3.87 cnf(ssp20, plain, (spl19 | spl20), inference(avatar_split_clause, [status(thm)], [p514, sdef19, sdef20])).
% 25.57/3.87 cnf(p38, plain, convergent_lines(sk0,X0) | convergent_lines(sk2,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p27, c5])).
% 25.57/3.87 cnf(p143, plain, convergent_lines(sk0,X0) | convergent_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p38, c13])).
% 25.57/3.87 cnf(p516, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p72, p143])).
% 25.57/3.87 cnf(ssp21, plain, (spl18 | spl20), inference(avatar_split_clause, [status(thm)], [p516, sdef18, sdef20])).
% 25.57/3.87 cnf(p193, plain, distinct_lines(sk2,X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p41, c13])).
% 25.57/3.87 cnf(p517, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk2) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p72, p193])).
% 25.57/3.87 fof(sdef21, definition, (spl21 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 25.57/3.87 cnf(ssp22, plain, (spl4 | spl6 | spl21), inference(avatar_split_clause, [status(thm)], [p517, sdef4, sdef6, sdef21])).
% 25.57/3.87 cnf(p519, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | distinct_lines(sk2,X0) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p72, p193])).
% 25.57/3.87 cnf(ssp23, plain, (spl12 | spl19), inference(avatar_split_clause, [status(thm)], [p519, sdef12, sdef19])).
% 25.57/3.87 cnf(p203, plain, distinct_lines(X0,sk1) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p200, c4])).
% 25.57/3.87 cnf(p520, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk2) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p72, p203])).
% 25.57/3.87 cnf(ssp24, plain, (spl4 | spl6 | spl15), inference(avatar_split_clause, [status(thm)], [p520, sdef4, sdef6, sdef15])).
% 25.57/3.87 cnf(p521, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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(sk2,X1), inference(resolution, [status(thm)], [p72, p203])).
% 25.57/3.87 cnf(ssp25, plain, (spl9 | spl12), inference(avatar_split_clause, [status(thm)], [p521, sdef9, sdef12])).
% 25.57/3.87 cnf(p207, plain, distinct_lines(sk2,X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p43, c13])).
% 25.57/3.87 cnf(p522, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk2) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p72, p207])).
% 25.57/3.87 fof(sdef22, definition, (spl22 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 25.57/3.87 cnf(ssp26, plain, (spl4 | spl6 | spl22), inference(avatar_split_clause, [status(thm)], [p522, sdef4, sdef6, sdef22])).
% 25.57/3.87 cnf(p524, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | distinct_lines(sk2,X0) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p72, p207])).
% 25.57/3.87 cnf(ssp27, plain, (spl12 | spl18), inference(avatar_split_clause, [status(thm)], [p524, sdef12, sdef18])).
% 25.57/3.87 cnf(p218, plain, distinct_lines(X0,sk0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p214, c4])).
% 25.57/3.87 cnf(p525, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk2) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p72, p218])).
% 25.57/3.87 fof(sdef23, definition, (spl23 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 25.57/3.87 cnf(ssp28, plain, (spl4 | spl6 | spl23), inference(avatar_split_clause, [status(thm)], [p525, sdef4, sdef6, sdef23])).
% 25.57/3.87 cnf(p527, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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(sk2,X1), inference(resolution, [status(thm)], [p72, p218])).
% 25.57/3.87 cnf(ssp29, plain, (spl12 | spl14), inference(avatar_split_clause, [status(thm)], [p527, sdef12, sdef14])).
% 25.57/3.87 cnf(p219, plain, distinct_lines(sk2,X0) | distinct_lines(X0,X1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p214, c4])).
% 25.57/3.87 cnf(p528, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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(X1,X0), inference(resolution, [status(thm)], [p72, p219])).
% 25.57/3.87 fof(sdef24, definition, (spl24 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | distinct_lines(sk2,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 25.57/3.87 cnf(ssp30, plain, (spl3 | spl5 | spl24), inference(avatar_split_clause, [status(thm)], [p528, sdef3, sdef5, sdef24])).
% 25.57/3.87 cnf(p103, plain, convergent_lines(sk1,X0) | convergent_lines(X1,X0) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p33, c13])).
% 25.57/3.87 cnf(p246, plain, convergent_lines(sk1,X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p103, c13])).
% 25.57/3.87 cnf(p530, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),sk0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p72, p246])).
% 25.57/3.87 cnf(ssp31, plain, (spl3 | spl5 | spl21), inference(avatar_split_clause, [status(thm)], [p530, sdef3, sdef5, sdef21])).
% 25.57/3.87 cnf(p531, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | convergent_lines(sk1,X1) | distinct_lines(sk0,X0), inference(resolution, [status(thm)], [p72, p246])).
% 25.57/3.87 cnf(ssp32, plain, (spl7 | spl19), inference(avatar_split_clause, [status(thm)], [p531, sdef7, sdef19])).
% 25.57/3.87 cnf(p102, plain, convergent_lines(sk0,X0) | convergent_lines(X0,sk1), inference(resolution, [status(thm)], [p33, c2])).
% 25.57/3.87 cnf(p117, plain, convergent_lines(X0,sk1) | convergent_lines(sk0,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p102, c5])).
% 25.57/3.87 cnf(p270, plain, convergent_lines(X0,sk1) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p117, c13])).
% 25.57/3.87 cnf(p532, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk1,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X1) | convergent_lines(X0,sk1) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p72, p270])).
% 25.57/3.87 fof(sdef25, definition, (spl25 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk1,sk2),X0) | convergent_lines(X0,sk1))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 25.57/3.87 cnf(ssp33, plain, (spl18 | spl25), inference(avatar_split_clause, [status(thm)], [p532, sdef18, sdef25])).
% 25.57/3.87 cnf(p60, 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.57/3.87 cnf(p539, plain, (distinct_points(intersection_point(sk0,sk2),intersection_point(sk2,sk0)) | convergent_lines(sk0,sk0) | ~spl3), inference(resolution, [status(thm)], [p480, p60])).
% 25.57/3.87 fof(sdef26, definition, (spl26 <=> (distinct_points(intersection_point(sk0,sk2),intersection_point(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 25.57/3.87 cnf(ssp34, plain, (~spl3 | spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p539, sdef26, sdef27])).
% 25.57/3.87 cnf(p482, plain, (apart_point_and_line(intersection_point(sk1,sk2),sk0) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 25.57/3.87 cnf(p557, plain, (distinct_points(intersection_point(sk1,sk2),intersection_point(sk2,sk0)) | convergent_lines(sk0,sk0) | ~spl5), inference(resolution, [status(thm)], [p482, p60])).
% 25.57/3.87 fof(sdef28, definition, (spl28 <=> (distinct_points(intersection_point(sk1,sk2),intersection_point(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 25.57/3.87 cnf(ssp35, plain, (~spl5 | spl27 | spl28), inference(avatar_split_clause, [status(thm)], [p557, sdef27, sdef28])).
% 25.57/3.87 cnf(p73, plain, ~distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1), inference(resolution, [status(thm)], [c10, p68])).
% 25.57/3.87 cnf(p560, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),sk2), inference(resolution, [status(thm)], [p73, p21])).
% 25.57/3.87 cnf(ssp36, plain, (spl3 | spl4 | spl29 | spl30), inference(avatar_split_clause, [status(thm)], [p560, sdef3, sdef4, sdef29, sdef30])).
% 25.57/3.87 cnf(p563, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X0), inference(resolution, [status(thm)], [p73, p24])).
% 25.57/3.87 fof(sdef31, definition, (spl31 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 25.57/3.87 cnf(ssp37, plain, (spl4 | spl30 | spl31), inference(avatar_split_clause, [status(thm)], [p563, sdef4, sdef30, sdef31])).
% 25.57/3.87 cnf(p565, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p73, p28])).
% 25.57/3.87 fof(sdef32, definition, (spl32 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 25.57/3.87 cnf(ssp38, plain, (spl3 | spl29 | spl32), inference(avatar_split_clause, [status(thm)], [p565, sdef3, sdef29, sdef32])).
% 25.57/3.87 cnf(p567, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p73, p84])).
% 25.57/3.87 fof(sdef33, definition, (spl33 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,sk1))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 25.57/3.87 cnf(ssp39, plain, (spl3 | spl29 | spl33), inference(avatar_split_clause, [status(thm)], [p567, sdef3, sdef29, sdef33])).
% 25.57/3.87 cnf(p569, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p73, p31])).
% 25.57/3.87 fof(sdef34, definition, (spl34 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 25.57/3.87 cnf(ssp40, plain, (spl3 | spl29 | spl34), inference(avatar_split_clause, [status(thm)], [p569, sdef3, sdef29, sdef34])).
% 25.57/3.87 cnf(p571, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p73, p31])).
% 25.57/3.87 fof(sdef35, definition, (spl35 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 25.57/3.87 cnf(ssp41, plain, (spl4 | spl30 | spl35), inference(avatar_split_clause, [status(thm)], [p571, sdef4, sdef30, sdef35])).
% 25.57/3.87 cnf(p573, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk0,X0) | distinct_lines(sk2,X1), inference(resolution, [status(thm)], [p73, p31])).
% 25.57/3.87 fof(sdef36, definition, (spl36 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 25.57/3.87 cnf(ssp42, plain, (spl31 | spl36), inference(avatar_split_clause, [status(thm)], [p573, sdef31, sdef36])).
% 25.57/3.87 cnf(p575, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p73, p97])).
% 25.57/3.87 fof(sdef37, definition, (spl37 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,sk2))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 25.57/3.87 cnf(ssp43, plain, (spl3 | spl29 | spl37), inference(avatar_split_clause, [status(thm)], [p575, sdef3, sdef29, sdef37])).
% 25.57/3.87 cnf(p577, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p73, p200])).
% 25.57/3.87 cnf(ssp44, plain, (spl4 | spl30 | spl33), inference(avatar_split_clause, [status(thm)], [p577, sdef4, sdef30, sdef33])).
% 25.57/3.87 cnf(p578, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,sk0), inference(resolution, [status(thm)], [p73, p214])).
% 25.57/3.87 fof(sdef38, definition, (spl38 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X0,sk0))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 25.57/3.87 cnf(ssp45, plain, (spl4 | spl30 | spl38), inference(avatar_split_clause, [status(thm)], [p578, sdef4, sdef30, sdef38])).
% 25.57/3.87 cnf(p580, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | distinct_lines(sk2,X0), inference(resolution, [status(thm)], [p73, p214])).
% 25.57/3.87 cnf(ssp46, plain, (spl3 | spl29 | spl36), inference(avatar_split_clause, [status(thm)], [p580, sdef3, sdef29, sdef36])).
% 25.57/3.87 cnf(p581, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p73, p88])).
% 25.57/3.87 fof(sdef39, definition, (spl39 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 25.57/3.87 cnf(ssp47, plain, (spl3 | spl29 | spl39), inference(avatar_split_clause, [status(thm)], [p581, sdef3, sdef29, sdef39])).
% 25.57/3.87 cnf(p583, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk1) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p73, p88])).
% 25.57/3.87 cnf(ssp48, plain, (spl31 | spl33), inference(avatar_split_clause, [status(thm)], [p583, sdef31, sdef33])).
% 25.57/3.87 cnf(p584, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk2) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p73, p94])).
% 25.57/3.87 cnf(ssp49, plain, (spl4 | spl30 | spl32), inference(avatar_split_clause, [status(thm)], [p584, sdef4, sdef30, sdef32])).
% 25.57/3.87 cnf(p585, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk2) | distinct_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p73, p101])).
% 25.57/3.87 fof(sdef40, definition, (spl40 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 25.57/3.87 cnf(ssp50, plain, (spl4 | spl30 | spl40), inference(avatar_split_clause, [status(thm)], [p585, sdef4, sdef30, sdef40])).
% 25.57/3.87 cnf(p587, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p73, p101])).
% 25.57/3.87 fof(sdef41, definition, (spl41 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 25.57/3.87 cnf(ssp51, plain, (spl3 | spl29 | spl41), inference(avatar_split_clause, [status(thm)], [p587, sdef3, sdef29, sdef41])).
% 25.57/3.87 cnf(p589, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk2) | distinct_lines(sk0,X1), inference(resolution, [status(thm)], [p73, p101])).
% 25.57/3.87 cnf(ssp52, plain, (spl31 | spl37), inference(avatar_split_clause, [status(thm)], [p589, sdef31, sdef37])).
% 25.57/3.87 cnf(p590, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk0,X0) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p73, p105])).
% 25.57/3.87 fof(sdef42, definition, (spl42 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 25.57/3.87 fof(sdef43, definition, (spl43 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X0))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 25.57/3.87 cnf(ssp53, plain, (spl42 | spl43), inference(avatar_split_clause, [status(thm)], [p590, sdef42, sdef43])).
% 25.57/3.87 cnf(p593, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk1,X0) | convergent_lines(sk2,X1), inference(resolution, [status(thm)], [p73, p130])).
% 25.57/3.87 fof(sdef44, definition, (spl44 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 25.57/3.87 cnf(ssp54, plain, (spl43 | spl44), inference(avatar_split_clause, [status(thm)], [p593, sdef43, sdef44])).
% 25.57/3.87 cnf(p595, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk0,X0) | convergent_lines(sk2,X1), inference(resolution, [status(thm)], [p73, p143])).
% 25.57/3.87 cnf(ssp55, plain, (spl42 | spl44), inference(avatar_split_clause, [status(thm)], [p595, sdef42, sdef44])).
% 25.57/3.87 cnf(p596, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p73, p193])).
% 25.57/3.87 fof(sdef45, definition, (spl45 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 25.57/3.87 cnf(ssp56, plain, (spl4 | spl30 | spl45), inference(avatar_split_clause, [status(thm)], [p596, sdef4, sdef30, sdef45])).
% 25.57/3.87 cnf(p598, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk2,X0) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p73, p193])).
% 25.57/3.87 cnf(ssp57, plain, (spl36 | spl43), inference(avatar_split_clause, [status(thm)], [p598, sdef36, sdef43])).
% 25.57/3.87 cnf(p599, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p73, p203])).
% 25.57/3.87 cnf(ssp58, plain, (spl4 | spl30 | spl39), inference(avatar_split_clause, [status(thm)], [p599, sdef4, sdef30, sdef39])).
% 25.57/3.87 cnf(p600, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk1) | distinct_lines(sk2,X1), inference(resolution, [status(thm)], [p73, p203])).
% 25.57/3.87 cnf(ssp59, plain, (spl33 | spl36), inference(avatar_split_clause, [status(thm)], [p600, sdef33, sdef36])).
% 25.57/3.87 cnf(p601, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p73, p207])).
% 25.57/3.87 fof(sdef46, definition, (spl46 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 25.57/3.87 cnf(ssp60, plain, (spl4 | spl30 | spl46), inference(avatar_split_clause, [status(thm)], [p601, sdef4, sdef30, sdef46])).
% 25.57/3.87 cnf(p603, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(sk2,X0) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p73, p207])).
% 25.57/3.87 cnf(ssp61, plain, (spl36 | spl42), inference(avatar_split_clause, [status(thm)], [p603, sdef36, sdef42])).
% 25.57/3.87 cnf(p604, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk2) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p73, p218])).
% 25.57/3.87 fof(sdef47, definition, (spl47 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 25.57/3.87 cnf(ssp62, plain, (spl4 | spl30 | spl47), inference(avatar_split_clause, [status(thm)], [p604, sdef4, sdef30, sdef47])).
% 25.57/3.87 cnf(p606, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | distinct_lines(X0,sk0) | distinct_lines(sk2,X1), inference(resolution, [status(thm)], [p73, p218])).
% 25.57/3.87 cnf(ssp63, plain, (spl36 | spl38), inference(avatar_split_clause, [status(thm)], [p606, sdef36, sdef38])).
% 25.57/3.87 cnf(p607, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk2,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p73, p219])).
% 25.57/3.87 fof(sdef48, definition, (spl48 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | distinct_lines(sk2,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 25.57/3.87 cnf(ssp64, plain, (spl3 | spl29 | spl48), inference(avatar_split_clause, [status(thm)], [p607, sdef3, sdef29, sdef48])).
% 25.57/3.87 cnf(p609, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),sk0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p73, p246])).
% 25.57/3.87 cnf(ssp65, plain, (spl3 | spl29 | spl45), inference(avatar_split_clause, [status(thm)], [p609, sdef3, sdef29, sdef45])).
% 25.57/3.87 cnf(p610, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(sk1,X1) | distinct_lines(sk0,X0), inference(resolution, [status(thm)], [p73, p246])).
% 25.57/3.87 cnf(ssp66, plain, (spl31 | spl43), inference(avatar_split_clause, [status(thm)], [p610, sdef31, sdef43])).
% 25.57/3.87 cnf(p611, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk0,sk1),X0) | apart_point_and_line(intersection_point(sk0,sk1),X1) | convergent_lines(X0,sk1) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p73, p270])).
% 25.57/3.87 fof(sdef49, definition, (spl49 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk1),X0) | convergent_lines(X0,sk1))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 25.57/3.87 cnf(ssp67, plain, (spl42 | spl49), inference(avatar_split_clause, [status(thm)], [p611, sdef42, sdef49])).
% 25.57/3.87 cnf(p627, plain, (distinct_points(intersection_point(sk0,sk1),intersection_point(sk2,sk0)) | convergent_lines(sk0,sk0) | ~spl29), inference(resolution, [status(thm)], [p561, p60])).
% 25.57/3.87 fof(sdef50, definition, (spl50 <=> (distinct_points(intersection_point(sk0,sk1),intersection_point(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 25.57/3.87 cnf(ssp68, plain, (~spl29 | spl27 | spl50), inference(avatar_split_clause, [status(thm)], [p627, sdef27, sdef50])).
% 25.57/3.87 cnf(p55, plain, ~apart_point_and_line(X0,sk1) | distinct_points(X0,intersection_point(sk2,sk1)), inference(resolution, [status(thm)], [c9, c15])).
% 25.57/3.87 cnf(p74, plain, distinct_points(intersection_point(sk0,sk2),intersection_point(sk2,sk1)), inference(resolution, [status(thm)], [p55, c18])).
% 25.57/3.87 cnf(p76, plain, ~apart_point_and_line(X0,line_connecting(intersection_point(sk0,sk2),intersection_point(sk2,sk1))) | distinct_points(X0,intersection_point(sk0,sk2)), inference(resolution, [status(thm)], [p74, c6])).
% 25.57/3.87 cnf(p635, plain, distinct_points(intersection_point(sk0,sk2),intersection_point(sk0,sk2)) | distinct_lines(sk1,line_connecting(intersection_point(sk0,sk2),intersection_point(sk2,sk1))), inference(resolution, [status(thm)], [p76, p93])).
% 25.57/3.87 fof(sdef51, definition, (spl51 <=> (distinct_lines(sk1,line_connecting(intersection_point(sk0,sk2),intersection_point(sk2,sk1))))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 25.57/3.87 cnf(ssp69, plain, (spl0 | spl51), inference(avatar_split_clause, [status(thm)], [p635, sdef0, sdef51])).
% 25.57/3.87 cnf(p78, plain, ~distinct_lines(X0,X1) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1), inference(resolution, [status(thm)], [p74, c10])).
% 25.57/3.87 cnf(p662, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),sk2), inference(resolution, [status(thm)], [p78, p21])).
% 25.57/3.87 fof(sdef52, definition, (spl52 <=> (apart_point_and_line(intersection_point(sk2,sk1),sk0))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 25.57/3.87 fof(sdef53, definition, (spl53 <=> (apart_point_and_line(intersection_point(sk2,sk1),sk2))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 25.57/3.87 cnf(ssp70, plain, (spl3 | spl4 | spl52 | spl53), inference(avatar_split_clause, [status(thm)], [p662, sdef3, sdef4, sdef52, sdef53])).
% 25.57/3.87 cnf(p665, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk2) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk0,X0), inference(resolution, [status(thm)], [p78, p24])).
% 25.57/3.87 fof(sdef54, definition, (spl54 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 25.57/3.87 cnf(ssp71, plain, (spl4 | spl53 | spl54), inference(avatar_split_clause, [status(thm)], [p665, sdef4, sdef53, sdef54])).
% 25.57/3.87 cnf(p667, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p78, p28])).
% 25.57/3.87 fof(sdef55, definition, (spl55 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk1,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 25.57/3.87 cnf(ssp72, plain, (spl3 | spl52 | spl55), inference(avatar_split_clause, [status(thm)], [p667, sdef3, sdef52, sdef55])).
% 25.57/3.87 cnf(p669, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p78, p84])).
% 25.57/3.87 fof(sdef56, definition, (spl56 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X0,sk1))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 25.57/3.87 cnf(ssp73, plain, (spl3 | spl52 | spl56), inference(avatar_split_clause, [status(thm)], [p669, sdef3, sdef52, sdef56])).
% 25.57/3.87 cnf(p671, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p78, p31])).
% 25.57/3.87 fof(sdef57, definition, (spl57 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 25.57/3.87 cnf(ssp74, plain, (spl3 | spl52 | spl57), inference(avatar_split_clause, [status(thm)], [p671, sdef3, sdef52, sdef57])).
% 25.57/3.87 cnf(p673, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk2) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p78, p31])).
% 25.57/3.87 fof(sdef58, definition, (spl58 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 25.57/3.87 cnf(ssp75, plain, (spl4 | spl53 | spl58), inference(avatar_split_clause, [status(thm)], [p673, sdef4, sdef53, sdef58])).
% 25.57/3.87 cnf(p675, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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(sk2,X1), inference(resolution, [status(thm)], [p78, p31])).
% 25.57/3.87 fof(sdef59, definition, (spl59 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 25.57/3.87 cnf(ssp76, plain, (spl54 | spl59), inference(avatar_split_clause, [status(thm)], [p675, sdef54, sdef59])).
% 25.57/3.87 cnf(p677, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p78, p97])).
% 25.57/3.87 fof(sdef60, definition, (spl60 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X0,sk2))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 25.57/3.87 cnf(ssp77, plain, (spl3 | spl52 | spl60), inference(avatar_split_clause, [status(thm)], [p677, sdef3, sdef52, sdef60])).
% 25.57/3.87 cnf(p679, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk2) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X0,sk1), inference(resolution, [status(thm)], [p78, p200])).
% 25.57/3.87 cnf(ssp78, plain, (spl4 | spl53 | spl56), inference(avatar_split_clause, [status(thm)], [p679, sdef4, sdef53, sdef56])).
% 25.57/3.87 cnf(p680, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk2) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X0,sk0), inference(resolution, [status(thm)], [p78, p214])).
% 25.57/3.87 fof(sdef61, definition, (spl61 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X0,sk0))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 25.57/3.87 cnf(ssp79, plain, (spl4 | spl53 | spl61), inference(avatar_split_clause, [status(thm)], [p680, sdef4, sdef53, sdef61])).
% 25.57/3.87 cnf(p682, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | distinct_lines(sk2,X0), inference(resolution, [status(thm)], [p78, p214])).
% 25.57/3.87 cnf(ssp80, plain, (spl3 | spl52 | spl59), inference(avatar_split_clause, [status(thm)], [p682, sdef3, sdef52, sdef59])).
% 25.57/3.87 cnf(p683, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p78, p88])).
% 25.57/3.87 fof(sdef62, definition, (spl62 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 25.57/3.87 cnf(ssp81, plain, (spl3 | spl52 | spl62), inference(avatar_split_clause, [status(thm)], [p683, sdef3, sdef52, sdef62])).
% 25.57/3.87 cnf(p685, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p78, p88])).
% 25.57/3.87 cnf(ssp82, plain, (spl54 | spl56), inference(avatar_split_clause, [status(thm)], [p685, sdef54, sdef56])).
% 25.57/3.87 cnf(p686, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk2) | distinct_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p78, p94])).
% 25.57/3.87 cnf(ssp83, plain, (spl4 | spl53 | spl55), inference(avatar_split_clause, [status(thm)], [p686, sdef4, sdef53, sdef55])).
% 25.57/3.87 cnf(p687, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk2) | distinct_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p78, p101])).
% 25.57/3.87 fof(sdef63, definition, (spl63 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 25.57/3.87 cnf(ssp84, plain, (spl4 | spl53 | spl63), inference(avatar_split_clause, [status(thm)], [p687, sdef4, sdef53, sdef63])).
% 25.57/3.87 cnf(p689, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p78, p101])).
% 25.57/3.87 fof(sdef64, definition, (spl64 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 25.57/3.87 cnf(ssp85, plain, (spl3 | spl52 | spl64), inference(avatar_split_clause, [status(thm)], [p689, sdef3, sdef52, sdef64])).
% 25.57/3.87 cnf(p691, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p78, p101])).
% 25.57/3.87 cnf(ssp86, plain, (spl54 | spl60), inference(avatar_split_clause, [status(thm)], [p691, sdef54, sdef60])).
% 25.57/3.87 cnf(p692, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p78, p105])).
% 25.57/3.87 fof(sdef65, definition, (spl65 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(sk0,X0))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 25.57/3.87 fof(sdef66, definition, (spl66 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(sk1,X0))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 25.57/3.87 cnf(ssp87, plain, (spl65 | spl66), inference(avatar_split_clause, [status(thm)], [p692, sdef65, sdef66])).
% 25.57/3.87 cnf(p695, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p78, p130])).
% 25.57/3.87 fof(sdef67, definition, (spl67 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 25.57/3.87 cnf(ssp88, plain, (spl66 | spl67), inference(avatar_split_clause, [status(thm)], [p695, sdef66, sdef67])).
% 25.57/3.87 cnf(p697, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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)], [p78, p143])).
% 25.57/3.87 cnf(ssp89, plain, (spl65 | spl67), inference(avatar_split_clause, [status(thm)], [p697, sdef65, sdef67])).
% 25.57/3.87 cnf(p698, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk2) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p78, p193])).
% 25.57/3.87 fof(sdef68, definition, (spl68 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 25.57/3.87 cnf(ssp90, plain, (spl4 | spl53 | spl68), inference(avatar_split_clause, [status(thm)], [p698, sdef4, sdef53, sdef68])).
% 25.57/3.87 cnf(p700, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | distinct_lines(sk2,X0) | convergent_lines(sk1,X1), inference(resolution, [status(thm)], [p78, p193])).
% 25.57/3.87 cnf(ssp91, plain, (spl59 | spl66), inference(avatar_split_clause, [status(thm)], [p700, sdef59, sdef66])).
% 25.57/3.87 cnf(p701, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk2) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X1,sk1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p78, p203])).
% 25.57/3.87 cnf(ssp92, plain, (spl4 | spl53 | spl62), inference(avatar_split_clause, [status(thm)], [p701, sdef4, sdef53, sdef62])).
% 25.57/3.87 cnf(p702, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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(sk2,X1), inference(resolution, [status(thm)], [p78, p203])).
% 25.57/3.87 cnf(ssp93, plain, (spl56 | spl59), inference(avatar_split_clause, [status(thm)], [p702, sdef56, sdef59])).
% 25.57/3.87 cnf(p703, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk2) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p78, p207])).
% 25.57/3.87 fof(sdef69, definition, (spl69 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(sk0,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 25.57/3.87 cnf(ssp94, plain, (spl4 | spl53 | spl69), inference(avatar_split_clause, [status(thm)], [p703, sdef4, sdef53, sdef69])).
% 25.57/3.87 cnf(p705, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | distinct_lines(sk2,X0) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p78, p207])).
% 25.57/3.87 cnf(ssp95, plain, (spl59 | spl65), inference(avatar_split_clause, [status(thm)], [p705, sdef59, sdef65])).
% 25.57/3.87 cnf(p706, plain, apart_point_and_line(intersection_point(sk0,sk2),sk2) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk2) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p78, p218])).
% 25.57/3.87 fof(sdef70, definition, (spl70 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(X1,sk0) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 25.57/3.87 cnf(ssp96, plain, (spl4 | spl53 | spl70), inference(avatar_split_clause, [status(thm)], [p706, sdef4, sdef53, sdef70])).
% 25.57/3.87 cnf(p708, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),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(sk2,X1), inference(resolution, [status(thm)], [p78, p218])).
% 25.57/3.87 cnf(ssp97, plain, (spl59 | spl61), inference(avatar_split_clause, [status(thm)], [p708, sdef59, sdef61])).
% 25.57/3.87 cnf(p709, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),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(X1,X0), inference(resolution, [status(thm)], [p78, p219])).
% 25.57/3.87 fof(sdef71, definition, (spl71 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | distinct_lines(sk2,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 25.57/3.87 cnf(ssp98, plain, (spl3 | spl52 | spl71), inference(avatar_split_clause, [status(thm)], [p709, sdef3, sdef52, sdef71])).
% 25.57/3.87 cnf(p711, plain, apart_point_and_line(intersection_point(sk0,sk2),sk0) | apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),sk0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(sk1,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p78, p246])).
% 25.57/3.87 cnf(ssp99, plain, (spl3 | spl52 | spl68), inference(avatar_split_clause, [status(thm)], [p711, sdef3, sdef52, sdef68])).
% 25.57/3.87 cnf(p712, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | convergent_lines(sk1,X1) | distinct_lines(sk0,X0), inference(resolution, [status(thm)], [p78, p246])).
% 25.57/3.87 cnf(ssp100, plain, (spl54 | spl66), inference(avatar_split_clause, [status(thm)], [p712, sdef54, sdef66])).
% 25.57/3.87 cnf(p713, plain, apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk0,sk2),X1) | apart_point_and_line(intersection_point(sk2,sk1),X0) | apart_point_and_line(intersection_point(sk2,sk1),X1) | convergent_lines(X0,sk1) | convergent_lines(sk0,X1), inference(resolution, [status(thm)], [p78, p270])).
% 25.57/3.87 fof(sdef72, definition, (spl72 <=> (apart_point_and_line(intersection_point(sk0,sk2),X0) | apart_point_and_line(intersection_point(sk2,sk1),X0) | convergent_lines(X0,sk1))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 25.57/3.87 cnf(ssp101, plain, (spl65 | spl72), inference(avatar_split_clause, [status(thm)], [p713, sdef65, sdef72])).
% 25.57/3.87 cnf(p663, plain, (apart_point_and_line(intersection_point(sk2,sk1),sk0) | ~spl52), inference(avatar_component_clause, [status(thm)], [sdef52])).
% 25.57/3.87 cnf(p722, plain, (distinct_points(intersection_point(sk2,sk1),intersection_point(sk2,sk0)) | convergent_lines(sk0,sk0) | ~spl52), inference(resolution, [status(thm)], [p663, p60])).
% 25.57/3.87 fof(sdef73, definition, (spl73 <=> (distinct_points(intersection_point(sk2,sk1),intersection_point(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 25.57/3.87 cnf(ssp102, plain, (~spl52 | spl27 | spl73), inference(avatar_split_clause, [status(thm)], [p722, sdef27, sdef73])).
% 25.57/3.87 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, sct0, sct1, sct2, sct3, sct4, sct5, sct6])).
% 25.57/3.87 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------