%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO187+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 : n004.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:21 PM UTC 2026
% Result : Theorem 19.29s 3.00s
% Output : Proof 19.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO187+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n004.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 11:21:35 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 19.29/3.00 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.29/3.00 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.29/3.00 fof(sdef10, definition, (spl10 <=> (distinct_points(sk2,sk2))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 19.29/3.00 cnf(p692, plain, (distinct_points(sk2,sk2) | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 19.29/3.00 fof(f0, axiom, ! [X] : ~ distinct_points(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart1)).
% 19.29/3.00 fof(f0_nnf, plain, ! [X] : (~(distinct_points(X,X))), inference(nnf_transformation, [status(thm)], [f0])).
% 19.29/3.00 fof(f0_sk, plain, ! [X] : (~(distinct_points(X,X))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 19.29/3.00 cnf(c0, plain, ~distinct_points(X0,X0), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 19.29/3.00 cnf(p705, plain, ($false | ~spl10), inference(resolution, [status(thm)], [p692, c0])).
% 19.29/3.00 cnf(sct0, plain, (~spl10), inference(avatar_contradiction_clause, [status(thm)], [p705])).
% 19.29/3.00 fof(sdef2, definition, (spl2 <=> (distinct_points(sk2,X0) | distinct_points(X0,sk2))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 19.29/3.00 cnf(p675, plain, (distinct_points(sk2,X0) | distinct_points(X0,sk2) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 19.29/3.00 cnf(p706, plain, (distinct_points(sk2,sk2) | ~spl2), inference(factoring, [status(thm)], [p675])).
% 19.29/3.00 cnf(p715, plain, ($false | ~spl2), inference(resolution, [status(thm)], [p706, c0])).
% 19.29/3.00 cnf(sct1, plain, (~spl2), inference(avatar_contradiction_clause, [status(thm)], [p715])).
% 19.29/3.00 fof(sdef21, definition, (spl21 <=> (distinct_points(sk3,X0) | distinct_points(X0,sk3))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 19.29/3.00 cnf(p865, plain, (distinct_points(sk3,X0) | distinct_points(X0,sk3) | ~spl21), inference(avatar_component_clause, [status(thm)], [sdef21])).
% 19.29/3.00 cnf(p893, plain, (distinct_points(sk3,sk3) | ~spl21), inference(factoring, [status(thm)], [p865])).
% 19.29/3.00 cnf(p902, plain, ($false | ~spl21), inference(resolution, [status(thm)], [p893, c0])).
% 19.29/3.00 cnf(sct2, plain, (~spl21), inference(avatar_contradiction_clause, [status(thm)], [p902])).
% 19.29/3.00 fof(sdef31, definition, (spl31 <=> (apart_point_and_line(sk0,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 19.29/3.00 cnf(p917, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | ~spl31), inference(avatar_component_clause, [status(thm)], [sdef31])).
% 19.29/3.00 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)).
% 19.29/3.00 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])).
% 19.29/3.00 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])).
% 19.29/3.00 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])).
% 19.29/3.00 fof(f12, conjecture, ! [X,Y,U,V] : ( ( distinct_points(X,Y) & distinct_points(U,V) & ~ apart_point_and_line(X,line_connecting(U,V)) & ~ apart_point_and_line(Y,line_connecting(U,V)) ) => ( ~ apart_point_and_line(U,line_connecting(X,Y)) & ~ apart_point_and_line(V,line_connecting(X,Y)) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 19.29/3.00 fof(f12_neg, negated_conjecture, ~(! [X,Y,U,V] : ( ( distinct_points(X,Y) & distinct_points(U,V) & ~ apart_point_and_line(X,line_connecting(U,V)) & ~ apart_point_and_line(Y,line_connecting(U,V)) ) => ( ~ apart_point_and_line(U,line_connecting(X,Y)) & ~ apart_point_and_line(V,line_connecting(X,Y)) ) )), inference(negated_conjecture, [status(cth)], [f12])).
% 19.29/3.00 fof(f12_nnf, plain, ? [X,Y,U,V] : (((((distinct_points(X,Y) & distinct_points(U,V)) & ~(apart_point_and_line(X,line_connecting(U,V)))) & ~(apart_point_and_line(Y,line_connecting(U,V)))) & (apart_point_and_line(U,line_connecting(X,Y)) | apart_point_and_line(V,line_connecting(X,Y))))), inference(nnf_transformation, [status(thm)], [f12_neg])).
% 19.29/3.00 fof(f12_sk, plain, ((((distinct_points(sk0,sk1) & distinct_points(sk2,sk3)) & ~(apart_point_and_line(sk0,line_connecting(sk2,sk3)))) & ~(apart_point_and_line(sk1,line_connecting(sk2,sk3)))) & (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk3,line_connecting(sk0,sk1)))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2,sk3])], [f12_nnf])).
% 19.29/3.00 cnf(c14, plain, distinct_points(sk0,sk1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 19.29/3.00 cnf(p45, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c6, c14])).
% 19.29/3.00 cnf(p986, plain, (distinct_points(sk0,sk0) | ~spl31), inference(resolution, [status(thm)], [p917, p45])).
% 19.29/3.00 cnf(p989, plain, ($false | ~spl31), inference(resolution, [status(thm)], [p986, c0])).
% 19.29/3.00 cnf(sct3, plain, (~spl31), inference(avatar_contradiction_clause, [status(thm)], [p989])).
% 19.29/3.00 fof(sdef33, definition, (spl33 <=> (apart_point_and_line(sk1,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 19.29/3.00 cnf(p919, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | ~spl33), inference(avatar_component_clause, [status(thm)], [sdef33])).
% 19.29/3.00 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])).
% 19.29/3.00 cnf(p78, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [c7, c14])).
% 19.29/3.00 cnf(p990, plain, (distinct_points(sk1,sk1) | ~spl33), inference(resolution, [status(thm)], [p919, p78])).
% 19.29/3.00 cnf(p993, plain, ($false | ~spl33), inference(resolution, [status(thm)], [p990, c0])).
% 19.29/3.00 cnf(sct4, plain, (~spl33), inference(avatar_contradiction_clause, [status(thm)], [p993])).
% 19.29/3.00 fof(sdef35, definition, (spl35 <=> (apart_point_and_line(sk0,line_connecting(sk2,sk3)))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 19.29/3.00 cnf(p923, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk3)) | ~spl35), inference(avatar_component_clause, [status(thm)], [sdef35])).
% 19.29/3.00 cnf(c16, plain, ~apart_point_and_line(sk0,line_connecting(sk2,sk3)), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 19.29/3.00 cnf(p1013, plain, ($false | ~spl35), inference(resolution, [status(thm)], [p923, c16])).
% 19.29/3.00 cnf(sct5, plain, (~spl35), inference(avatar_contradiction_clause, [status(thm)], [p1013])).
% 19.29/3.00 fof(sdef36, definition, (spl36 <=> (apart_point_and_line(sk1,line_connecting(sk2,sk3)))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 19.29/3.00 cnf(p924, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk3)) | ~spl36), inference(avatar_component_clause, [status(thm)], [sdef36])).
% 19.29/3.00 cnf(c17, plain, ~apart_point_and_line(sk1,line_connecting(sk2,sk3)), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 19.29/3.00 cnf(p1014, plain, ($false | ~spl36), inference(resolution, [status(thm)], [p924, c17])).
% 19.29/3.00 cnf(sct6, plain, (~spl36), inference(avatar_contradiction_clause, [status(thm)], [p1014])).
% 19.29/3.00 cnf(c18, plain, apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk3,line_connecting(sk0,sk1)), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 19.29/3.00 fof(sdef0, definition, (spl0 <=> (apart_point_and_line(sk2,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 19.29/3.00 fof(sdef1, definition, (spl1 <=> (apart_point_and_line(sk3,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 19.29/3.00 cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [c18, sdef0, sdef1])).
% 19.29/3.00 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)).
% 19.29/3.00 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])).
% 19.29/3.00 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])).
% 19.29/3.00 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])).
% 19.29/3.00 cnf(p19, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 19.29/3.00 cnf(p161, plain, (distinct_points(sk2,X0) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | ~spl0), inference(resolution, [status(thm)], [c11, p19])).
% 19.29/3.00 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)).
% 19.29/3.00 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])).
% 19.29/3.00 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])).
% 19.29/3.00 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])).
% 19.29/3.00 cnf(p199, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | apart_point_and_line(X0,X1) | ~spl0), inference(resolution, [status(thm)], [p161, c12])).
% 19.29/3.00 cnf(c15, plain, distinct_points(sk2,sk3), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 19.29/3.00 cnf(p46, plain, ~apart_point_and_line(X0,line_connecting(sk2,sk3)) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [c6, c15])).
% 19.29/3.00 cnf(p674, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk3)) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p199, p46])).
% 19.29/3.00 fof(sdef3, definition, (spl3 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk3)))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 19.29/3.00 cnf(ssp1, plain, (~spl0 | spl2 | spl3), inference(avatar_split_clause, [status(thm)], [p674, sdef2, sdef3])).
% 19.29/3.00 cnf(p69, plain, (distinct_points(sk2,sk0) | ~spl0), inference(resolution, [status(thm)], [p45, p19])).
% 19.29/3.00 cnf(p72, plain, (~apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p69, c6])).
% 19.29/3.00 cnf(p677, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk0)) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p199, p72])).
% 19.29/3.00 fof(sdef4, definition, (spl4 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 19.29/3.00 cnf(ssp2, plain, (~spl0 | spl2 | spl4), inference(avatar_split_clause, [status(thm)], [p677, sdef2, sdef4])).
% 19.29/3.00 fof(f3, axiom, ! [X,Y,Z] : ( distinct_points(X,Y) => ( distinct_points(X,Z) | distinct_points(Y,Z) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart4)).
% 19.29/3.00 fof(f3_nnf, plain, ! [X,Y,Z] : ((~(distinct_points(X,Y)) | (distinct_points(X,Z) | distinct_points(Y,Z)))), inference(nnf_transformation, [status(thm)], [f3])).
% 19.29/3.00 fof(f3_sk, plain, ! [X,Y,Z] : ((~(distinct_points(X,Y)) | (distinct_points(X,Z) | distinct_points(Y,Z)))), inference(skolemisation, [status(esa)], [f3_nnf])).
% 19.29/3.00 cnf(c3, plain, ~distinct_points(X0,X1) | distinct_points(X0,X2) | distinct_points(X1,X2), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 19.29/3.00 cnf(p22, plain, distinct_points(sk2,X0) | distinct_points(sk3,X0), inference(resolution, [status(thm)], [c3, c15])).
% 19.29/3.00 cnf(p24, plain, distinct_points(sk2,X0) | distinct_points(sk3,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p22, c3])).
% 19.29/3.00 cnf(p30, plain, distinct_points(sk2,X0) | distinct_points(X0,sk3), inference(resolution, [status(thm)], [p24, c0])).
% 19.29/3.00 cnf(p34, plain, distinct_points(X0,sk3) | distinct_points(sk2,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p30, c3])).
% 19.29/3.00 cnf(p40, plain, distinct_points(X0,sk3) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p34, c0])).
% 19.29/3.00 cnf(p43, plain, distinct_points(sk3,sk2), inference(resolution, [status(thm)], [p40, c0])).
% 19.29/3.00 cnf(p101, plain, ~apart_point_and_line(X0,line_connecting(sk3,sk2)) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [c7, p43])).
% 19.29/3.00 cnf(p679, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk2)) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p199, p101])).
% 19.29/3.00 fof(sdef5, definition, (spl5 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk2)))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 19.29/3.00 cnf(ssp3, plain, (~spl0 | spl2 | spl5), inference(avatar_split_clause, [status(thm)], [p679, sdef2, sdef5])).
% 19.29/3.00 cnf(p71, plain, (distinct_points(sk2,X0) | distinct_points(sk0,X0) | ~spl0), inference(resolution, [status(thm)], [p69, c3])).
% 19.29/3.00 cnf(p75, plain, (distinct_points(sk0,sk2) | ~spl0), inference(resolution, [status(thm)], [p71, c0])).
% 19.29/3.00 cnf(p106, plain, (~apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p75, c7])).
% 19.29/3.00 cnf(p682, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p199, p106])).
% 19.29/3.00 fof(sdef6, definition, (spl6 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 19.29/3.00 cnf(ssp4, plain, (~spl0 | spl2 | spl6), inference(avatar_split_clause, [status(thm)], [p682, sdef2, sdef6])).
% 19.29/3.00 cnf(p113, plain, (distinct_points(sk2,sk1) | ~spl0), inference(resolution, [status(thm)], [p78, p19])).
% 19.29/3.00 cnf(p116, plain, (~apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p113, c6])).
% 19.29/3.00 cnf(p684, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk1)) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p199, p116])).
% 19.29/3.00 fof(sdef7, definition, (spl7 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 19.29/3.00 cnf(ssp5, plain, (~spl0 | spl2 | spl7), inference(avatar_split_clause, [status(thm)], [p684, sdef2, sdef7])).
% 19.29/3.00 cnf(p115, plain, (distinct_points(sk2,X0) | distinct_points(sk1,X0) | ~spl0), inference(resolution, [status(thm)], [p113, c3])).
% 19.29/3.00 cnf(p121, plain, (distinct_points(sk1,sk2) | ~spl0), inference(resolution, [status(thm)], [p115, c0])).
% 19.29/3.00 cnf(p153, plain, (~apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p121, c7])).
% 19.29/3.00 cnf(p686, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk2)) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p199, p153])).
% 19.29/3.00 fof(sdef8, definition, (spl8 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 19.29/3.00 cnf(ssp6, plain, (~spl0 | spl2 | spl8), inference(avatar_split_clause, [status(thm)], [p686, sdef2, sdef8])).
% 19.29/3.00 cnf(p57, plain, ~apart_point_and_line(X0,line_connecting(sk2,X1)) | distinct_points(X0,sk2) | distinct_points(X1,sk3), inference(resolution, [status(thm)], [c6, p30])).
% 19.29/3.00 cnf(p688, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X1)) | distinct_points(X0,sk2) | distinct_points(X1,sk3) | ~spl0), inference(resolution, [status(thm)], [p199, p57])).
% 19.29/3.00 fof(sdef9, definition, (spl9 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X0,sk3))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 19.29/3.00 cnf(ssp7, plain, (~spl0 | spl2 | spl9), inference(avatar_split_clause, [status(thm)], [p688, sdef2, sdef9])).
% 19.29/3.00 cnf(p58, plain, ~apart_point_and_line(X0,line_connecting(X1,sk3)) | distinct_points(X0,X1) | distinct_points(sk2,X1), inference(resolution, [status(thm)], [c6, p30])).
% 19.29/3.00 cnf(p636, plain, ~apart_point_and_line(sk2,line_connecting(X0,sk3)) | distinct_points(sk2,X0), inference(factoring, [status(thm)], [p58])).
% 19.29/3.00 cnf(p691, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(sk2,X0) | ~spl0), inference(resolution, [status(thm)], [p199, p636])).
% 19.29/3.00 fof(sdef11, definition, (spl11 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 19.29/3.00 cnf(ssp8, plain, (~spl0 | spl10 | spl11), inference(avatar_split_clause, [status(thm)], [p691, sdef10, sdef11])).
% 19.29/3.00 cnf(p77, plain, (distinct_points(sk0,X0) | ~apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(X1,sk2) | ~spl0), inference(resolution, [status(thm)], [p71, c6])).
% 19.29/3.00 cnf(p695, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X1)) | distinct_points(sk0,X1) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p199, p77])).
% 19.29/3.00 fof(sdef12, definition, (spl12 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 19.29/3.00 cnf(ssp9, plain, (~spl0 | spl2 | spl12), inference(avatar_split_clause, [status(thm)], [p695, sdef2, sdef12])).
% 19.29/3.00 cnf(p81, plain, ~apart_point_and_line(X0,line_connecting(sk3,X1)) | distinct_points(X0,X1) | distinct_points(sk2,X1), inference(resolution, [status(thm)], [c7, p22])).
% 19.29/3.00 cnf(p639, plain, ~apart_point_and_line(sk2,line_connecting(sk3,X0)) | distinct_points(sk2,X0), inference(factoring, [status(thm)], [p81])).
% 19.29/3.00 cnf(p698, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk2,X0) | ~spl0), inference(resolution, [status(thm)], [p199, p639])).
% 19.29/3.00 fof(sdef13, definition, (spl13 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 19.29/3.00 cnf(ssp10, plain, (~spl0 | spl10 | spl13), inference(avatar_split_clause, [status(thm)], [p698, sdef10, sdef13])).
% 19.29/3.00 cnf(p54, plain, ~apart_point_and_line(X0,line_connecting(sk2,X1)) | distinct_points(X0,sk2) | distinct_points(sk3,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [c6, p24])).
% 19.29/3.00 cnf(p700, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X1)) | distinct_points(X0,sk2) | distinct_points(sk3,X2) | distinct_points(X1,X2) | ~spl0), inference(resolution, [status(thm)], [p199, p54])).
% 19.29/3.00 fof(sdef14, definition, (spl14 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk3,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 19.29/3.00 cnf(ssp11, plain, (~spl0 | spl2 | spl14), inference(avatar_split_clause, [status(thm)], [p700, sdef2, sdef14])).
% 19.29/3.00 cnf(p123, plain, (distinct_points(sk1,X0) | ~apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(X1,sk2) | ~spl0), inference(resolution, [status(thm)], [p115, c6])).
% 19.29/3.00 cnf(p703, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X1)) | distinct_points(sk1,X1) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p199, p123])).
% 19.29/3.00 fof(sdef15, definition, (spl15 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 19.29/3.00 cnf(ssp12, plain, (~spl0 | spl2 | spl15), inference(avatar_split_clause, [status(thm)], [p703, sdef2, sdef15])).
% 19.29/3.00 cnf(p65, plain, ~apart_point_and_line(X0,line_connecting(sk2,X1)) | distinct_points(X0,sk2) | distinct_points(X2,sk3) | distinct_points(X2,X1), inference(resolution, [status(thm)], [c6, p34])).
% 19.29/3.00 cnf(p722, plain, (distinct_points(X0,sk2) | distinct_points(X1,sk3) | distinct_points(X1,X2) | distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X2)) | ~spl0), inference(resolution, [status(thm)], [p65, p199])).
% 19.29/3.00 fof(sdef16, definition, (spl16 <=> (distinct_points(X0,sk3) | distinct_points(X0,X1) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X1)))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 19.29/3.00 cnf(ssp13, plain, (~spl0 | spl2 | spl16), inference(avatar_split_clause, [status(thm)], [p722, sdef2, sdef16])).
% 19.29/3.00 cnf(p196, plain, (distinct_points(sk2,X0) | distinct_points(X0,sk0) | ~spl0), inference(resolution, [status(thm)], [p161, p45])).
% 19.29/3.00 cnf(p202, plain, (distinct_points(X0,sk0) | ~apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(X1,sk2) | ~spl0), inference(resolution, [status(thm)], [p196, c6])).
% 19.29/3.00 cnf(p739, plain, (distinct_points(X0,sk0) | distinct_points(X1,sk2) | distinct_points(sk2,X1) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | ~spl0), inference(resolution, [status(thm)], [p202, p199])).
% 19.29/3.00 fof(sdef17, definition, (spl17 <=> (distinct_points(X0,sk0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 19.29/3.00 cnf(ssp14, plain, (~spl0 | spl2 | spl17), inference(avatar_split_clause, [status(thm)], [p739, sdef2, sdef17])).
% 19.29/3.00 cnf(p203, plain, (distinct_points(sk2,X0) | ~apart_point_and_line(X1,line_connecting(X0,sk0)) | distinct_points(X1,X0) | ~spl0), inference(resolution, [status(thm)], [p196, c6])).
% 19.29/3.00 cnf(p742, plain, (distinct_points(sk2,X0) | ~apart_point_and_line(sk2,line_connecting(X0,sk0)) | ~spl0), inference(factoring, [status(thm)], [p203])).
% 19.29/3.00 cnf(p744, plain, (distinct_points(sk2,X0) | distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk0)) | ~spl0), inference(resolution, [status(thm)], [p742, p199])).
% 19.29/3.00 fof(sdef18, definition, (spl18 <=> (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk0)))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 19.29/3.00 cnf(ssp15, plain, (~spl0 | spl10 | spl18), inference(avatar_split_clause, [status(thm)], [p744, sdef10, sdef18])).
% 19.29/3.00 cnf(p197, plain, (distinct_points(sk2,X0) | distinct_points(X0,sk1) | ~spl0), inference(resolution, [status(thm)], [p161, p78])).
% 19.29/3.00 cnf(p210, plain, (distinct_points(X0,sk1) | ~apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(X1,sk2) | ~spl0), inference(resolution, [status(thm)], [p197, c6])).
% 19.29/3.00 cnf(p748, plain, (distinct_points(X0,sk1) | distinct_points(X1,sk2) | distinct_points(sk2,X1) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | ~spl0), inference(resolution, [status(thm)], [p210, p199])).
% 19.29/3.00 fof(sdef19, definition, (spl19 <=> (distinct_points(X0,sk1) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 19.29/3.00 cnf(ssp16, plain, (~spl0 | spl2 | spl19), inference(avatar_split_clause, [status(thm)], [p748, sdef2, sdef19])).
% 19.29/3.00 cnf(p211, plain, (distinct_points(sk2,X0) | ~apart_point_and_line(X1,line_connecting(X0,sk1)) | distinct_points(X1,X0) | ~spl0), inference(resolution, [status(thm)], [p197, c6])).
% 19.29/3.00 cnf(p753, plain, (distinct_points(sk2,X0) | ~apart_point_and_line(sk2,line_connecting(X0,sk1)) | ~spl0), inference(factoring, [status(thm)], [p211])).
% 19.29/3.00 cnf(p755, plain, (distinct_points(sk2,X0) | distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk1)) | ~spl0), inference(resolution, [status(thm)], [p753, p199])).
% 19.29/3.00 fof(sdef20, definition, (spl20 <=> (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk1)))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 19.29/3.00 cnf(ssp17, plain, (~spl0 | spl10 | spl20), inference(avatar_split_clause, [status(thm)], [p755, sdef10, sdef20])).
% 19.29/3.00 cnf(p20, plain, (apart_point_and_line(sk3,line_connecting(sk0,sk1)) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 19.29/3.00 cnf(p162, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | ~spl1), inference(resolution, [status(thm)], [c11, p20])).
% 19.29/3.00 cnf(p219, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | apart_point_and_line(X0,X1) | ~spl1), inference(resolution, [status(thm)], [p162, c12])).
% 19.29/3.00 cnf(p68, plain, ~apart_point_and_line(X0,line_connecting(sk3,sk2)) | distinct_points(X0,sk3), inference(resolution, [status(thm)], [c6, p43])).
% 19.29/3.00 cnf(p864, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk2)) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p219, p68])).
% 19.29/3.00 cnf(ssp18, plain, (~spl1 | spl5 | spl21), inference(avatar_split_clause, [status(thm)], [p864, sdef5, sdef21])).
% 19.29/3.00 cnf(p70, plain, (distinct_points(sk3,sk0) | ~spl1), inference(resolution, [status(thm)], [p45, p20])).
% 19.29/3.00 cnf(p74, plain, (~apart_point_and_line(X0,line_connecting(sk3,sk0)) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p70, c6])).
% 19.29/3.00 cnf(p866, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk0)) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p219, p74])).
% 19.29/3.00 fof(sdef22, definition, (spl22 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk0)))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 19.29/3.00 cnf(ssp19, plain, (~spl1 | spl21 | spl22), inference(avatar_split_clause, [status(thm)], [p866, sdef21, sdef22])).
% 19.29/3.00 cnf(p79, plain, ~apart_point_and_line(X0,line_connecting(sk2,sk3)) | distinct_points(X0,sk3), inference(resolution, [status(thm)], [c7, c15])).
% 19.29/3.00 cnf(p868, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk3)) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p219, p79])).
% 19.29/3.00 cnf(ssp20, plain, (~spl1 | spl3 | spl21), inference(avatar_split_clause, [status(thm)], [p868, sdef3, sdef21])).
% 19.29/3.00 cnf(p73, plain, (distinct_points(sk3,X0) | distinct_points(sk0,X0) | ~spl1), inference(resolution, [status(thm)], [p70, c3])).
% 19.29/3.00 cnf(p107, plain, (distinct_points(sk0,sk3) | ~spl1), inference(resolution, [status(thm)], [p73, c0])).
% 19.29/3.00 cnf(p112, plain, (~apart_point_and_line(X0,line_connecting(sk0,sk3)) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p107, c7])).
% 19.29/3.00 cnf(p870, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk3)) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p219, p112])).
% 19.29/3.00 fof(sdef23, definition, (spl23 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk3)))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 19.29/3.00 cnf(ssp21, plain, (~spl1 | spl21 | spl23), inference(avatar_split_clause, [status(thm)], [p870, sdef21, sdef23])).
% 19.29/3.00 cnf(p114, plain, (distinct_points(sk3,sk1) | ~spl1), inference(resolution, [status(thm)], [p78, p20])).
% 19.29/3.00 cnf(p119, plain, (~apart_point_and_line(X0,line_connecting(sk3,sk1)) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p114, c6])).
% 19.29/3.00 cnf(p872, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk1)) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p219, p119])).
% 19.29/3.00 fof(sdef24, definition, (spl24 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk1)))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 19.29/3.00 cnf(ssp22, plain, (~spl1 | spl21 | spl24), inference(avatar_split_clause, [status(thm)], [p872, sdef21, sdef24])).
% 19.29/3.00 cnf(p118, plain, (distinct_points(sk3,X0) | distinct_points(sk1,X0) | ~spl1), inference(resolution, [status(thm)], [p114, c3])).
% 19.29/3.00 cnf(p154, plain, (distinct_points(sk1,sk3) | ~spl1), inference(resolution, [status(thm)], [p118, c0])).
% 19.29/3.00 cnf(p160, plain, (~apart_point_and_line(X0,line_connecting(sk1,sk3)) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p154, c7])).
% 19.29/3.00 cnf(p874, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk3)) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p219, p160])).
% 19.29/3.00 fof(sdef25, definition, (spl25 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk3)))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 19.29/3.00 cnf(ssp23, plain, (~spl1 | spl21 | spl25), inference(avatar_split_clause, [status(thm)], [p874, sdef21, sdef25])).
% 19.29/3.00 cnf(p48, plain, ~apart_point_and_line(X0,line_connecting(sk3,X1)) | distinct_points(X0,sk3) | distinct_points(sk2,X1), inference(resolution, [status(thm)], [c6, p22])).
% 19.29/3.00 cnf(p876, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X1)) | distinct_points(X0,sk3) | distinct_points(sk2,X1) | ~spl1), inference(resolution, [status(thm)], [p219, p48])).
% 19.29/3.00 cnf(ssp24, plain, (~spl1 | spl13 | spl21), inference(avatar_split_clause, [status(thm)], [p876, sdef13, sdef21])).
% 19.29/3.00 cnf(p91, plain, ~apart_point_and_line(X0,line_connecting(X1,sk3)) | distinct_points(X0,sk3) | distinct_points(sk2,X1), inference(resolution, [status(thm)], [c7, p30])).
% 19.29/3.00 cnf(p879, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X1,sk3)) | distinct_points(X0,sk3) | distinct_points(sk2,X1) | ~spl1), inference(resolution, [status(thm)], [p219, p91])).
% 19.29/3.00 cnf(ssp25, plain, (~spl1 | spl11 | spl21), inference(avatar_split_clause, [status(thm)], [p879, sdef11, sdef21])).
% 19.29/3.00 cnf(p55, plain, ~apart_point_and_line(X0,line_connecting(sk3,X1)) | distinct_points(X0,sk3) | distinct_points(sk2,X2) | distinct_points(X2,X1), inference(resolution, [status(thm)], [c6, p24])).
% 19.29/3.00 cnf(p880, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X1)) | distinct_points(X0,sk3) | distinct_points(sk2,X2) | distinct_points(X2,X1) | ~spl1), inference(resolution, [status(thm)], [p219, p55])).
% 19.29/3.00 fof(sdef26, definition, (spl26 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk2,X1) | distinct_points(X1,X0))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 19.29/3.00 cnf(ssp26, plain, (~spl1 | spl21 | spl26), inference(avatar_split_clause, [status(thm)], [p880, sdef21, sdef26])).
% 19.29/3.00 cnf(p100, plain, ~apart_point_and_line(X0,line_connecting(X1,sk3)) | distinct_points(X0,sk3) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [c7, p40])).
% 19.29/3.00 cnf(p882, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X1,sk3)) | distinct_points(X0,sk3) | distinct_points(X1,sk2) | ~spl1), inference(resolution, [status(thm)], [p219, p100])).
% 19.29/3.00 fof(sdef27, definition, (spl27 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(X0,sk2))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 19.29/3.00 cnf(ssp27, plain, (~spl1 | spl21 | spl27), inference(avatar_split_clause, [status(thm)], [p882, sdef21, sdef27])).
% 19.29/3.00 cnf(p109, plain, (distinct_points(sk0,X0) | ~apart_point_and_line(X1,line_connecting(sk3,X0)) | distinct_points(X1,sk3) | ~spl1), inference(resolution, [status(thm)], [p73, c6])).
% 19.29/3.00 cnf(p884, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X1)) | distinct_points(sk0,X1) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p219, p109])).
% 19.29/3.00 fof(sdef28, definition, (spl28 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 19.29/3.00 cnf(ssp28, plain, (~spl1 | spl21 | spl28), inference(avatar_split_clause, [status(thm)], [p884, sdef21, sdef28])).
% 19.29/3.00 cnf(p156, plain, (distinct_points(sk1,X0) | ~apart_point_and_line(X1,line_connecting(sk3,X0)) | distinct_points(X1,sk3) | ~spl1), inference(resolution, [status(thm)], [p118, c6])).
% 19.29/3.00 cnf(p886, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X1)) | distinct_points(sk1,X1) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p219, p156])).
% 19.29/3.00 fof(sdef29, definition, (spl29 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 19.29/3.00 cnf(ssp29, plain, (~spl1 | spl21 | spl29), inference(avatar_split_clause, [status(thm)], [p886, sdef21, sdef29])).
% 19.29/3.00 cnf(p97, plain, ~apart_point_and_line(X0,line_connecting(X1,sk3)) | distinct_points(X0,sk3) | distinct_points(sk2,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [c7, p34])).
% 19.29/3.00 cnf(p891, plain, (distinct_points(X0,sk3) | distinct_points(sk2,X1) | distinct_points(X2,X1) | distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X2,sk3)) | ~spl1), inference(resolution, [status(thm)], [p97, p219])).
% 19.29/3.00 fof(sdef30, definition, (spl30 <=> (distinct_points(sk2,X0) | distinct_points(X1,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X1,sk3)))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 19.29/3.00 cnf(ssp30, plain, (~spl1 | spl21 | spl30), inference(avatar_split_clause, [status(thm)], [p891, sdef21, sdef30])).
% 19.29/3.00 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)).
% 19.29/3.00 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])).
% 19.29/3.00 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])).
% 19.29/3.00 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])).
% 19.29/3.00 cnf(p125, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1), inference(resolution, [status(thm)], [c10, c14])).
% 19.29/3.00 cnf(p163, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | apart_point_and_line(sk2,X0) | ~spl0), inference(resolution, [status(thm)], [c12, p19])).
% 19.29/3.00 cnf(p916, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | ~spl0), inference(resolution, [status(thm)], [p125, p163])).
% 19.29/3.00 fof(sdef32, definition, (spl32 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 19.29/3.00 cnf(ssp31, plain, (~spl0 | spl31 | spl32 | spl33), inference(avatar_split_clause, [status(thm)], [p916, sdef31, sdef32, sdef33])).
% 19.29/3.00 cnf(p920, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | distinct_points(sk2,X1) | apart_point_and_line(X1,X0) | ~spl0), inference(resolution, [status(thm)], [p125, p199])).
% 19.29/3.00 fof(sdef34, definition, (spl34 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_points(sk2,X1) | apart_point_and_line(X1,X0))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 19.29/3.00 cnf(ssp32, plain, (~spl0 | spl31 | spl33 | spl34), inference(avatar_split_clause, [status(thm)], [p920, sdef31, sdef33, sdef34])).
% 19.29/3.00 cnf(p676, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk3)) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 19.29/3.00 cnf(p922, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk3)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk3)) | ~spl3), inference(resolution, [status(thm)], [p125, p676])).
% 19.29/3.00 cnf(ssp33, plain, (~spl3 | spl31 | spl33 | spl35 | spl36), inference(avatar_split_clause, [status(thm)], [p922, sdef31, sdef33, sdef35, sdef36])).
% 19.29/3.00 cnf(p678, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk0)) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 19.29/3.00 cnf(p925, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | ~spl4), inference(resolution, [status(thm)], [p125, p678])).
% 19.29/3.00 fof(sdef37, definition, (spl37 <=> (apart_point_and_line(sk0,line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 19.29/3.00 fof(sdef38, definition, (spl38 <=> (apart_point_and_line(sk1,line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 19.29/3.00 cnf(ssp34, plain, (~spl4 | spl31 | spl33 | spl37 | spl38), inference(avatar_split_clause, [status(thm)], [p925, sdef31, sdef33, sdef37, sdef38])).
% 19.29/3.00 cnf(p680, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk2)) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 19.29/3.00 cnf(p928, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk3,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk3,sk2)) | ~spl5), inference(resolution, [status(thm)], [p125, p680])).
% 19.29/3.00 fof(sdef39, definition, (spl39 <=> (apart_point_and_line(sk0,line_connecting(sk3,sk2)))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 19.29/3.00 fof(sdef40, definition, (spl40 <=> (apart_point_and_line(sk1,line_connecting(sk3,sk2)))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 19.29/3.00 cnf(ssp35, plain, (~spl5 | spl31 | spl33 | spl39 | spl40), inference(avatar_split_clause, [status(thm)], [p928, sdef31, sdef33, sdef39, sdef40])).
% 19.29/3.00 cnf(p683, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 19.29/3.00 cnf(p931, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | ~spl6), inference(resolution, [status(thm)], [p125, p683])).
% 19.29/3.00 fof(sdef41, definition, (spl41 <=> (apart_point_and_line(sk0,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 19.29/3.00 fof(sdef42, definition, (spl42 <=> (apart_point_and_line(sk1,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 19.29/3.00 cnf(ssp36, plain, (~spl6 | spl31 | spl33 | spl41 | spl42), inference(avatar_split_clause, [status(thm)], [p931, sdef31, sdef33, sdef41, sdef42])).
% 19.29/3.00 cnf(p685, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk1)) | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 19.29/3.00 cnf(p934, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | ~spl7), inference(resolution, [status(thm)], [p125, p685])).
% 19.29/3.00 fof(sdef43, definition, (spl43 <=> (apart_point_and_line(sk0,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 19.29/3.00 fof(sdef44, definition, (spl44 <=> (apart_point_and_line(sk1,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 19.29/3.00 cnf(ssp37, plain, (~spl7 | spl31 | spl33 | spl43 | spl44), inference(avatar_split_clause, [status(thm)], [p934, sdef31, sdef33, sdef43, sdef44])).
% 19.29/3.00 cnf(p687, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk2)) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 19.29/3.00 cnf(p937, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk1,sk2)) | ~spl8), inference(resolution, [status(thm)], [p125, p687])).
% 19.29/3.00 fof(sdef45, definition, (spl45 <=> (apart_point_and_line(sk0,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 19.29/3.00 fof(sdef46, definition, (spl46 <=> (apart_point_and_line(sk1,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 19.29/3.00 cnf(ssp38, plain, (~spl8 | spl31 | spl33 | spl45 | spl46), inference(avatar_split_clause, [status(thm)], [p937, sdef31, sdef33, sdef45, sdef46])).
% 19.29/3.00 cnf(p689, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X0,sk3) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 19.29/3.00 cnf(p940, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(X0,sk3) | ~spl9), inference(resolution, [status(thm)], [p125, p689])).
% 19.29/3.00 fof(sdef47, definition, (spl47 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(X0,sk3))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 19.29/3.00 cnf(ssp39, plain, (~spl9 | spl31 | spl33 | spl47), inference(avatar_split_clause, [status(thm)], [p940, sdef31, sdef33, sdef47])).
% 19.29/3.00 cnf(p693, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(sk2,X0) | ~spl11), inference(avatar_component_clause, [status(thm)], [sdef11])).
% 19.29/3.00 cnf(p942, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk3)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk3)) | distinct_points(sk2,X0) | ~spl11), inference(resolution, [status(thm)], [p125, p693])).
% 19.29/3.00 fof(sdef48, definition, (spl48 <=> (apart_point_and_line(sk0,line_connecting(X0,sk3)) | apart_point_and_line(sk1,line_connecting(X0,sk3)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 19.29/3.00 cnf(ssp40, plain, (~spl11 | spl31 | spl33 | spl48), inference(avatar_split_clause, [status(thm)], [p942, sdef31, sdef33, sdef48])).
% 19.29/3.00 cnf(p696, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk0,X0) | ~spl12), inference(avatar_component_clause, [status(thm)], [sdef12])).
% 19.29/3.00 cnf(p944, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(sk0,X0) | ~spl12), inference(resolution, [status(thm)], [p125, p696])).
% 19.29/3.00 fof(sdef49, definition, (spl49 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 19.29/3.00 cnf(ssp41, plain, (~spl12 | spl31 | spl33 | spl49), inference(avatar_split_clause, [status(thm)], [p944, sdef31, sdef33, sdef49])).
% 19.29/3.00 cnf(p699, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk2,X0) | ~spl13), inference(avatar_component_clause, [status(thm)], [sdef13])).
% 19.29/3.00 cnf(p946, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk3,X0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk3,X0)) | distinct_points(sk2,X0) | ~spl13), inference(resolution, [status(thm)], [p125, p699])).
% 19.29/3.00 fof(sdef50, definition, (spl50 <=> (apart_point_and_line(sk0,line_connecting(sk3,X0)) | apart_point_and_line(sk1,line_connecting(sk3,X0)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 19.29/3.00 cnf(ssp42, plain, (~spl13 | spl31 | spl33 | spl50), inference(avatar_split_clause, [status(thm)], [p946, sdef31, sdef33, sdef50])).
% 19.29/3.00 cnf(p704, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk1,X0) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 19.29/3.00 cnf(p948, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(sk1,X0) | ~spl15), inference(resolution, [status(thm)], [p125, p704])).
% 19.29/3.00 fof(sdef51, definition, (spl51 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 19.29/3.00 cnf(ssp43, plain, (~spl15 | spl31 | spl33 | spl51), inference(avatar_split_clause, [status(thm)], [p948, sdef31, sdef33, sdef51])).
% 19.29/3.00 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)).
% 19.29/3.00 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])).
% 19.29/3.00 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])).
% 19.29/3.00 cnf(c4, plain, ~distinct_lines(X0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 19.29/3.00 cnf(p716, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk3),X0) | ~spl3), inference(resolution, [status(thm)], [p676, c4])).
% 19.29/3.00 cnf(p950, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk3)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk3)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl3), inference(resolution, [status(thm)], [p125, p716])).
% 19.29/3.00 fof(sdef52, definition, (spl52 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 19.29/3.00 cnf(ssp44, plain, (~spl3 | spl35 | spl36 | spl52), inference(avatar_split_clause, [status(thm)], [p950, sdef35, sdef36, sdef52])).
% 19.29/3.00 cnf(p718, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk0),X0) | ~spl4), inference(resolution, [status(thm)], [p678, c4])).
% 19.29/3.00 cnf(p952, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl4), inference(resolution, [status(thm)], [p125, p718])).
% 19.29/3.00 cnf(ssp45, plain, (~spl4 | spl37 | spl38 | spl52), inference(avatar_split_clause, [status(thm)], [p952, sdef37, sdef38, sdef52])).
% 19.29/3.00 cnf(p719, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk3,sk2),X0) | ~spl5), inference(resolution, [status(thm)], [p680, c4])).
% 19.29/3.00 cnf(p953, plain, (apart_point_and_line(sk0,line_connecting(sk3,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk3,sk2)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl5), inference(resolution, [status(thm)], [p125, p719])).
% 19.29/3.00 cnf(ssp46, plain, (~spl5 | spl39 | spl40 | spl52), inference(avatar_split_clause, [status(thm)], [p953, sdef39, sdef40, sdef52])).
% 19.29/3.00 cnf(p720, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl6), inference(resolution, [status(thm)], [p683, c4])).
% 19.29/3.00 cnf(p954, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl6), inference(resolution, [status(thm)], [p125, p720])).
% 19.29/3.00 cnf(ssp47, plain, (~spl6 | spl41 | spl42 | spl52), inference(avatar_split_clause, [status(thm)], [p954, sdef41, sdef42, sdef52])).
% 19.29/3.00 cnf(p721, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk1),X0) | ~spl7), inference(resolution, [status(thm)], [p685, c4])).
% 19.29/3.00 cnf(p955, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl7), inference(resolution, [status(thm)], [p125, p721])).
% 19.29/3.00 cnf(ssp48, plain, (~spl7 | spl43 | spl44 | spl52), inference(avatar_split_clause, [status(thm)], [p955, sdef43, sdef44, sdef52])).
% 19.29/3.00 cnf(p724, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk1,sk2),X0) | ~spl8), inference(resolution, [status(thm)], [p687, c4])).
% 19.29/3.00 cnf(p956, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk1,sk2)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl8), inference(resolution, [status(thm)], [p125, p724])).
% 19.29/3.00 cnf(ssp49, plain, (~spl8 | spl45 | spl46 | spl52), inference(avatar_split_clause, [status(thm)], [p956, sdef45, sdef46, sdef52])).
% 19.29/3.00 cnf(p740, plain, (distinct_points(X0,sk0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 19.29/3.00 cnf(p957, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(X0,sk0) | ~spl17), inference(resolution, [status(thm)], [p125, p740])).
% 19.29/3.00 fof(sdef53, definition, (spl53 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 19.29/3.00 cnf(ssp50, plain, (~spl17 | spl31 | spl33 | spl53), inference(avatar_split_clause, [status(thm)], [p957, sdef31, sdef33, sdef53])).
% 19.29/3.00 cnf(p745, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk0)) | ~spl18), inference(avatar_component_clause, [status(thm)], [sdef18])).
% 19.29/3.00 cnf(p959, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk0)) | distinct_points(sk2,X0) | ~spl18), inference(resolution, [status(thm)], [p125, p745])).
% 19.29/3.00 fof(sdef54, definition, (spl54 <=> (apart_point_and_line(sk0,line_connecting(X0,sk0)) | apart_point_and_line(sk1,line_connecting(X0,sk0)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 19.29/3.00 cnf(ssp51, plain, (~spl18 | spl31 | spl33 | spl54), inference(avatar_split_clause, [status(thm)], [p959, sdef31, sdef33, sdef54])).
% 19.29/3.00 cnf(p749, plain, (distinct_points(X0,sk1) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | ~spl19), inference(avatar_component_clause, [status(thm)], [sdef19])).
% 19.29/3.00 cnf(p961, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(X0,sk1) | ~spl19), inference(resolution, [status(thm)], [p125, p749])).
% 19.29/3.00 fof(sdef55, definition, (spl55 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 19.29/3.00 cnf(ssp52, plain, (~spl19 | spl31 | spl33 | spl55), inference(avatar_split_clause, [status(thm)], [p961, sdef31, sdef33, sdef55])).
% 19.29/3.00 cnf(p756, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk1)) | ~spl20), inference(avatar_component_clause, [status(thm)], [sdef20])).
% 19.29/3.00 cnf(p963, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk1)) | distinct_points(sk2,X0) | ~spl20), inference(resolution, [status(thm)], [p125, p756])).
% 19.29/3.00 fof(sdef56, definition, (spl56 <=> (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk1)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 19.29/3.00 cnf(ssp53, plain, (~spl20 | spl31 | spl33 | spl56), inference(avatar_split_clause, [status(thm)], [p963, sdef31, sdef33, sdef56])).
% 19.29/3.00 cnf(p867, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk0)) | ~spl22), inference(avatar_component_clause, [status(thm)], [sdef22])).
% 19.29/3.00 cnf(p965, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk3,sk0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk3,sk0)) | ~spl22), inference(resolution, [status(thm)], [p125, p867])).
% 19.29/3.00 fof(sdef57, definition, (spl57 <=> (apart_point_and_line(sk0,line_connecting(sk3,sk0)))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 19.29/3.00 fof(sdef58, definition, (spl58 <=> (apart_point_and_line(sk1,line_connecting(sk3,sk0)))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 19.29/3.00 cnf(ssp54, plain, (~spl22 | spl31 | spl33 | spl57 | spl58), inference(avatar_split_clause, [status(thm)], [p965, sdef31, sdef33, sdef57, sdef58])).
% 19.29/3.00 cnf(p871, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk3)) | ~spl23), inference(avatar_component_clause, [status(thm)], [sdef23])).
% 19.29/3.00 cnf(p968, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk3)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk3)) | ~spl23), inference(resolution, [status(thm)], [p125, p871])).
% 19.29/3.00 fof(sdef59, definition, (spl59 <=> (apart_point_and_line(sk0,line_connecting(sk0,sk3)))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 19.29/3.00 fof(sdef60, definition, (spl60 <=> (apart_point_and_line(sk1,line_connecting(sk0,sk3)))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 19.29/3.00 cnf(ssp55, plain, (~spl23 | spl31 | spl33 | spl59 | spl60), inference(avatar_split_clause, [status(thm)], [p968, sdef31, sdef33, sdef59, sdef60])).
% 19.29/3.00 cnf(p873, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk1)) | ~spl24), inference(avatar_component_clause, [status(thm)], [sdef24])).
% 19.29/3.00 cnf(p971, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk3,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk3,sk1)) | ~spl24), inference(resolution, [status(thm)], [p125, p873])).
% 19.29/3.00 fof(sdef61, definition, (spl61 <=> (apart_point_and_line(sk0,line_connecting(sk3,sk1)))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 19.29/3.00 fof(sdef62, definition, (spl62 <=> (apart_point_and_line(sk1,line_connecting(sk3,sk1)))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 19.29/3.00 cnf(ssp56, plain, (~spl24 | spl31 | spl33 | spl61 | spl62), inference(avatar_split_clause, [status(thm)], [p971, sdef31, sdef33, sdef61, sdef62])).
% 19.29/3.00 cnf(p875, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk3)) | ~spl25), inference(avatar_component_clause, [status(thm)], [sdef25])).
% 19.29/3.00 cnf(p974, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk1,sk3)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk1,sk3)) | ~spl25), inference(resolution, [status(thm)], [p125, p875])).
% 19.29/3.00 fof(sdef63, definition, (spl63 <=> (apart_point_and_line(sk0,line_connecting(sk1,sk3)))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 19.29/3.00 fof(sdef64, definition, (spl64 <=> (apart_point_and_line(sk1,line_connecting(sk1,sk3)))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 19.29/3.00 cnf(ssp57, plain, (~spl25 | spl31 | spl33 | spl63 | spl64), inference(avatar_split_clause, [status(thm)], [p974, sdef31, sdef33, sdef63, sdef64])).
% 19.29/3.00 cnf(p883, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(X0,sk2) | ~spl27), inference(avatar_component_clause, [status(thm)], [sdef27])).
% 19.29/3.00 cnf(p977, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk3)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk3)) | distinct_points(X0,sk2) | ~spl27), inference(resolution, [status(thm)], [p125, p883])).
% 19.29/3.00 fof(sdef65, definition, (spl65 <=> (apart_point_and_line(sk0,line_connecting(X0,sk3)) | apart_point_and_line(sk1,line_connecting(X0,sk3)) | distinct_points(X0,sk2))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 19.29/3.00 cnf(ssp58, plain, (~spl27 | spl31 | spl33 | spl65), inference(avatar_split_clause, [status(thm)], [p977, sdef31, sdef33, sdef65])).
% 19.29/3.00 cnf(p885, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk0,X0) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 19.29/3.00 cnf(p979, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk3,X0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk3,X0)) | distinct_points(sk0,X0) | ~spl28), inference(resolution, [status(thm)], [p125, p885])).
% 19.29/3.00 fof(sdef66, definition, (spl66 <=> (apart_point_and_line(sk0,line_connecting(sk3,X0)) | apart_point_and_line(sk1,line_connecting(sk3,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 19.29/3.00 cnf(ssp59, plain, (~spl28 | spl31 | spl33 | spl66), inference(avatar_split_clause, [status(thm)], [p979, sdef31, sdef33, sdef66])).
% 19.29/3.00 cnf(p887, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk1,X0) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 19.29/3.00 cnf(p981, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk3,X0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk3,X0)) | distinct_points(sk1,X0) | ~spl29), inference(resolution, [status(thm)], [p125, p887])).
% 19.29/3.00 fof(sdef67, definition, (spl67 <=> (apart_point_and_line(sk0,line_connecting(sk3,X0)) | apart_point_and_line(sk1,line_connecting(sk3,X0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 19.29/3.00 cnf(ssp60, plain, (~spl29 | spl31 | spl33 | spl67), inference(avatar_split_clause, [status(thm)], [p981, sdef31, sdef33, sdef67])).
% 19.29/3.00 cnf(p903, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk3,sk0),X0) | ~spl22), inference(resolution, [status(thm)], [p867, c4])).
% 19.29/3.00 cnf(p983, plain, (apart_point_and_line(sk0,line_connecting(sk3,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk3,sk0)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl22), inference(resolution, [status(thm)], [p125, p903])).
% 19.29/3.00 cnf(ssp61, plain, (~spl22 | spl52 | spl57 | spl58), inference(avatar_split_clause, [status(thm)], [p983, sdef52, sdef57, sdef58])).
% 19.29/3.00 cnf(p904, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk0,sk3),X0) | ~spl23), inference(resolution, [status(thm)], [p871, c4])).
% 19.29/3.00 cnf(p984, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk3)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk3)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl23), inference(resolution, [status(thm)], [p125, p904])).
% 19.29/3.00 cnf(ssp62, plain, (~spl23 | spl52 | spl59 | spl60), inference(avatar_split_clause, [status(thm)], [p984, sdef52, sdef59, sdef60])).
% 19.29/3.00 cnf(p906, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk3,sk1),X0) | ~spl24), inference(resolution, [status(thm)], [p873, c4])).
% 19.29/3.00 cnf(p985, plain, (apart_point_and_line(sk0,line_connecting(sk3,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk3,sk1)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl24), inference(resolution, [status(thm)], [p125, p906])).
% 19.29/3.00 cnf(ssp63, plain, (~spl24 | spl52 | spl61 | spl62), inference(avatar_split_clause, [status(thm)], [p985, sdef52, sdef61, sdef62])).
% 19.29/3.00 cnf(p126, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(sk3,X0) | apart_point_and_line(sk3,X1), inference(resolution, [status(thm)], [c10, c15])).
% 19.29/3.00 cnf(p994, plain, (apart_point_and_line(sk2,line_connecting(sk2,sk3)) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk3,line_connecting(sk2,sk3)) | apart_point_and_line(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl3), inference(resolution, [status(thm)], [p126, p716])).
% 19.29/3.00 fof(sdef68, definition, (spl68 <=> (apart_point_and_line(sk2,line_connecting(sk2,sk3)))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 19.29/3.00 fof(sdef69, definition, (spl69 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 19.29/3.00 fof(sdef70, definition, (spl70 <=> (apart_point_and_line(sk3,line_connecting(sk2,sk3)))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 19.29/3.00 cnf(ssp64, plain, (~spl3 | spl68 | spl69 | spl70), inference(avatar_split_clause, [status(thm)], [p994, sdef68, sdef69, sdef70])).
% 19.29/3.00 cnf(p998, plain, (apart_point_and_line(sk2,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk3,line_connecting(sk2,sk0)) | apart_point_and_line(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl4), inference(resolution, [status(thm)], [p126, p718])).
% 19.29/3.00 fof(sdef71, definition, (spl71 <=> (apart_point_and_line(sk2,line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 19.29/3.00 fof(sdef72, definition, (spl72 <=> (apart_point_and_line(sk3,line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 19.29/3.00 cnf(ssp65, plain, (~spl4 | spl69 | spl71 | spl72), inference(avatar_split_clause, [status(thm)], [p998, sdef69, sdef71, sdef72])).
% 19.29/3.00 cnf(p1001, plain, (apart_point_and_line(sk2,line_connecting(sk3,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk3,line_connecting(sk3,sk2)) | apart_point_and_line(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl5), inference(resolution, [status(thm)], [p126, p719])).
% 19.29/3.00 fof(sdef73, definition, (spl73 <=> (apart_point_and_line(sk2,line_connecting(sk3,sk2)))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 19.29/3.00 fof(sdef74, definition, (spl74 <=> (apart_point_and_line(sk3,line_connecting(sk3,sk2)))), introduced(definition, [new_symbols(naming, [spl74])], [avatar_definition])).
% 19.29/3.00 cnf(ssp66, plain, (~spl5 | spl69 | spl73 | spl74), inference(avatar_split_clause, [status(thm)], [p1001, sdef69, sdef73, sdef74])).
% 19.29/3.00 cnf(p1004, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk3,line_connecting(sk0,sk2)) | apart_point_and_line(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl6), inference(resolution, [status(thm)], [p126, p720])).
% 19.29/3.00 fof(sdef75, definition, (spl75 <=> (apart_point_and_line(sk2,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl75])], [avatar_definition])).
% 19.29/3.00 fof(sdef76, definition, (spl76 <=> (apart_point_and_line(sk3,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl76])], [avatar_definition])).
% 19.29/3.00 cnf(ssp67, plain, (~spl6 | spl69 | spl75 | spl76), inference(avatar_split_clause, [status(thm)], [p1004, sdef69, sdef75, sdef76])).
% 19.29/3.00 cnf(p1007, plain, (apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk3,line_connecting(sk2,sk1)) | apart_point_and_line(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl7), inference(resolution, [status(thm)], [p126, p721])).
% 19.29/3.00 fof(sdef77, definition, (spl77 <=> (apart_point_and_line(sk2,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl77])], [avatar_definition])).
% 19.29/3.00 fof(sdef78, definition, (spl78 <=> (apart_point_and_line(sk3,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl78])], [avatar_definition])).
% 19.29/3.00 cnf(ssp68, plain, (~spl7 | spl69 | spl77 | spl78), inference(avatar_split_clause, [status(thm)], [p1007, sdef69, sdef77, sdef78])).
% 19.29/3.00 cnf(p1010, plain, (apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk3,line_connecting(sk1,sk2)) | apart_point_and_line(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl8), inference(resolution, [status(thm)], [p126, p724])).
% 19.29/3.00 fof(sdef79, definition, (spl79 <=> (apart_point_and_line(sk2,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl79])], [avatar_definition])).
% 19.29/3.00 fof(sdef80, definition, (spl80 <=> (apart_point_and_line(sk3,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl80])], [avatar_definition])).
% 19.29/3.00 cnf(ssp69, plain, (~spl8 | spl69 | spl79 | spl80), inference(avatar_split_clause, [status(thm)], [p1010, sdef69, sdef79, sdef80])).
% 19.29/3.00 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, sct0, sct1, sct2, sct3, sct4, sct5, sct6])).
% 19.29/3.00 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------