%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO188+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 : n007.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 26.23s 14.03s
% Output : Proof 26.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO188+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/10.40 % Computer : n007.cluster.edu
% 0.11/10.40 % Model : x86_64 x86_64
% 0.11/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.40 % Memory : 8046.5625MB
% 0.11/10.40 % OS : Linux 6.8.0-71-generic
% 0.11/10.40 % CPULimit : 300
% 0.11/10.40 % WCLimit : 300
% 0.11/10.40 % DateTime : Wed Sep 23 11:20:02 UTC 2026
% 0.11/10.40 % CPUTime :
% 0.11/10.40 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 26.23/14.03 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.23/14.03 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.23/14.03 fof(sdef7, definition, (spl7 <=> (distinct_points(sk0,sk0))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 26.23/14.03 cnf(p458, plain, (distinct_points(sk0,sk0) | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 26.23/14.03 fof(f0, axiom, ! [X] : ~ distinct_points(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart1)).
% 26.23/14.03 fof(f0_nnf, plain, ! [X] : (~(distinct_points(X,X))), inference(nnf_transformation, [status(thm)], [f0])).
% 26.23/14.03 fof(f0_sk, plain, ! [X] : (~(distinct_points(X,X))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 26.23/14.03 cnf(c0, plain, ~distinct_points(X0,X0), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 26.23/14.03 cnf(p480, plain, ($false | ~spl7), inference(resolution, [status(thm)], [p458, c0])).
% 26.23/14.03 cnf(sct0, plain, (~spl7), inference(avatar_contradiction_clause, [status(thm)], [p480])).
% 26.23/14.03 fof(sdef1, definition, (spl1 <=> (distinct_points(sk0,X0) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 26.23/14.03 cnf(p445, plain, (distinct_points(sk0,X0) | distinct_points(X0,sk0) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 26.23/14.03 cnf(p482, plain, (distinct_points(sk0,sk0) | ~spl1), inference(factoring, [status(thm)], [p445])).
% 26.23/14.03 cnf(p491, plain, ($false | ~spl1), inference(resolution, [status(thm)], [p482, c0])).
% 26.23/14.03 cnf(sct1, plain, (~spl1), inference(avatar_contradiction_clause, [status(thm)], [p491])).
% 26.23/14.03 fof(sdef30, definition, (spl30 <=> (distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 26.23/14.03 cnf(p870, plain, (distinct_points(sk1,X0) | ~spl30), inference(avatar_component_clause, [status(thm)], [sdef30])).
% 26.23/14.03 cnf(p882, plain, ($false | ~spl30), inference(resolution, [status(thm)], [p870, c0])).
% 26.23/14.03 cnf(sct2, plain, (~spl30), inference(avatar_contradiction_clause, [status(thm)], [p882])).
% 26.23/14.03 fof(sdef31, definition, (spl31 <=> (distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 26.23/14.03 cnf(p890, plain, (distinct_points(sk2,X0) | ~spl31), inference(avatar_component_clause, [status(thm)], [sdef31])).
% 26.23/14.03 cnf(p902, plain, ($false | ~spl31), inference(resolution, [status(thm)], [p890, c0])).
% 26.23/14.03 cnf(sct3, plain, (~spl31), inference(avatar_contradiction_clause, [status(thm)], [p902])).
% 26.23/14.03 fof(sdef36, definition, (spl36 <=> (distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 26.23/14.03 cnf(p1007, plain, (distinct_points(X0,sk1) | ~spl36), inference(avatar_component_clause, [status(thm)], [sdef36])).
% 26.23/14.03 cnf(p1019, plain, ($false | ~spl36), inference(resolution, [status(thm)], [p1007, c0])).
% 26.23/14.03 cnf(sct4, plain, (~spl36), inference(avatar_contradiction_clause, [status(thm)], [p1019])).
% 26.23/14.03 fof(sdef37, definition, (spl37 <=> (apart_point_and_line(sk1,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 26.23/14.03 cnf(p1047, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | ~spl37), inference(avatar_component_clause, [status(thm)], [sdef37])).
% 26.23/14.03 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)).
% 26.23/14.03 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])).
% 26.23/14.03 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])).
% 26.23/14.03 cnf(c3, plain, ~distinct_points(X0,X1) | distinct_points(X0,X2) | distinct_points(X1,X2), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 26.23/14.03 fof(f12, conjecture, ! [X,Y,Z] : ( ( distinct_points(X,Y) & distinct_points(X,Z) & distinct_points(Y,Z) & ~ apart_point_and_line(Z,line_connecting(X,Y)) ) => ~ apart_point_and_line(X,line_connecting(Z,Y)) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 26.23/14.03 fof(f12_neg, negated_conjecture, ~(! [X,Y,Z] : ( ( distinct_points(X,Y) & distinct_points(X,Z) & distinct_points(Y,Z) & ~ apart_point_and_line(Z,line_connecting(X,Y)) ) => ~ apart_point_and_line(X,line_connecting(Z,Y)) )), inference(negated_conjecture, [status(cth)], [f12])).
% 26.23/14.03 fof(f12_nnf, plain, ? [X,Y,Z] : (((((distinct_points(X,Y) & distinct_points(X,Z)) & distinct_points(Y,Z)) & ~(apart_point_and_line(Z,line_connecting(X,Y)))) & apart_point_and_line(X,line_connecting(Z,Y)))), inference(nnf_transformation, [status(thm)], [f12_neg])).
% 26.23/14.03 fof(f12_sk, plain, ((((distinct_points(sk0,sk1) & distinct_points(sk0,sk2)) & distinct_points(sk1,sk2)) & ~(apart_point_and_line(sk2,line_connecting(sk0,sk1)))) & apart_point_and_line(sk0,line_connecting(sk2,sk1))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2])], [f12_nnf])).
% 26.23/14.03 cnf(c16, plain, distinct_points(sk1,sk2), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 26.23/14.03 cnf(p21, plain, distinct_points(sk1,X0) | distinct_points(sk2,X0), inference(resolution, [status(thm)], [c3, c16])).
% 26.23/14.03 cnf(p24, plain, distinct_points(sk1,X0) | distinct_points(sk2,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p21, c3])).
% 26.23/14.03 cnf(p35, plain, distinct_points(sk1,X0) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p24, c0])).
% 26.23/14.03 cnf(p39, plain, distinct_points(X0,sk2) | distinct_points(sk1,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p35, c3])).
% 26.23/14.03 cnf(p112, plain, distinct_points(X0,sk2) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [p39, c0])).
% 26.23/14.03 cnf(p121, plain, distinct_points(sk2,sk1), inference(resolution, [status(thm)], [p112, c0])).
% 26.23/14.03 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)).
% 26.23/14.03 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])).
% 26.23/14.03 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])).
% 26.23/14.03 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])).
% 26.23/14.03 cnf(p126, plain, ~apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [p121, c7])).
% 26.23/14.03 cnf(p1192, plain, (distinct_points(sk1,sk1) | ~spl37), inference(resolution, [status(thm)], [p1047, p126])).
% 26.23/14.03 cnf(p1195, plain, ($false | ~spl37), inference(resolution, [status(thm)], [p1192, c0])).
% 26.23/14.03 cnf(sct5, plain, (~spl37), inference(avatar_contradiction_clause, [status(thm)], [p1195])).
% 26.23/14.03 fof(sdef39, definition, (spl39 <=> (apart_point_and_line(sk2,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 26.23/14.03 cnf(p1049, plain, (apart_point_and_line(sk2,line_connecting(sk2,sk1)) | ~spl39), inference(avatar_component_clause, [status(thm)], [sdef39])).
% 26.23/14.03 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])).
% 26.23/14.03 cnf(p125, plain, ~apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p121, c6])).
% 26.23/14.03 cnf(p1196, plain, (distinct_points(sk2,sk2) | ~spl39), inference(resolution, [status(thm)], [p1049, p125])).
% 26.23/14.03 cnf(p1199, plain, ($false | ~spl39), inference(resolution, [status(thm)], [p1196, c0])).
% 26.23/14.03 cnf(sct6, plain, (~spl39), inference(avatar_contradiction_clause, [status(thm)], [p1199])).
% 26.23/14.03 fof(sdef41, definition, (spl41 <=> (apart_point_and_line(sk1,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 26.23/14.03 cnf(p1053, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | ~spl41), inference(avatar_component_clause, [status(thm)], [sdef41])).
% 26.23/14.03 cnf(c14, plain, distinct_points(sk0,sk1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 26.23/14.03 cnf(p71, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [c7, c14])).
% 26.23/14.03 cnf(p1212, plain, (distinct_points(sk1,sk1) | ~spl41), inference(resolution, [status(thm)], [p1053, p71])).
% 26.23/14.03 cnf(p1215, plain, ($false | ~spl41), inference(resolution, [status(thm)], [p1212, c0])).
% 26.23/14.03 cnf(sct7, plain, (~spl41), inference(avatar_contradiction_clause, [status(thm)], [p1215])).
% 26.23/14.03 fof(sdef42, definition, (spl42 <=> (apart_point_and_line(sk2,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 26.23/14.03 cnf(p1054, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | ~spl42), inference(avatar_component_clause, [status(thm)], [sdef42])).
% 26.23/14.03 cnf(c17, plain, ~apart_point_and_line(sk2,line_connecting(sk0,sk1)), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 26.23/14.03 cnf(p1216, plain, ($false | ~spl42), inference(resolution, [status(thm)], [p1054, c17])).
% 26.23/14.03 cnf(sct8, plain, (~spl42), inference(avatar_contradiction_clause, [status(thm)], [p1216])).
% 26.23/14.03 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)).
% 26.23/14.03 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])).
% 26.23/14.03 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])).
% 26.23/14.03 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])).
% 26.23/14.03 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)).
% 26.23/14.03 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])).
% 26.23/14.03 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])).
% 26.23/14.03 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])).
% 26.23/14.03 cnf(c18, plain, apart_point_and_line(sk0,line_connecting(sk2,sk1)), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 26.23/14.03 cnf(p174, plain, distinct_points(sk0,X0) | apart_point_and_line(X0,line_connecting(sk2,sk1)), inference(resolution, [status(thm)], [c11, c18])).
% 26.23/14.03 cnf(p205, plain, distinct_lines(line_connecting(sk2,sk1),X0) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [c12, p174])).
% 26.23/14.03 cnf(p45, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c6, c14])).
% 26.23/14.03 cnf(p443, plain, distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,sk1)) | distinct_points(sk0,X0) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [p205, p45])).
% 26.23/14.03 fof(sdef0, definition, (spl0 <=> (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 26.23/14.03 cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [p443, sdef0, sdef1])).
% 26.23/14.03 cnf(c15, plain, distinct_points(sk0,sk2), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 26.23/14.03 cnf(p46, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c6, c15])).
% 26.23/14.03 cnf(p446, plain, distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,sk2)) | distinct_points(sk0,X0) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [p205, p46])).
% 26.23/14.03 fof(sdef2, definition, (spl2 <=> (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 26.23/14.03 cnf(ssp1, plain, (spl1 | spl2), inference(avatar_split_clause, [status(thm)], [p446, sdef1, sdef2])).
% 26.23/14.03 cnf(p19, plain, distinct_points(sk0,X0) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [c3, c14])).
% 26.23/14.03 cnf(p22, plain, distinct_points(sk0,X0) | distinct_points(sk1,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p19, c3])).
% 26.23/14.03 cnf(p25, plain, distinct_points(sk0,X0) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [p22, c0])).
% 26.23/14.03 cnf(p29, plain, distinct_points(X0,sk1) | distinct_points(sk0,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p25, c3])).
% 26.23/14.03 cnf(p40, plain, distinct_points(X0,sk1) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [p29, c0])).
% 26.23/14.03 cnf(p43, plain, distinct_points(sk1,sk0), inference(resolution, [status(thm)], [p40, c0])).
% 26.23/14.03 cnf(p96, plain, ~apart_point_and_line(X0,line_connecting(sk1,sk0)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c7, p43])).
% 26.23/14.03 cnf(p448, plain, distinct_lines(line_connecting(sk2,sk1),line_connecting(sk1,sk0)) | distinct_points(sk0,X0) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [p205, p96])).
% 26.23/14.03 fof(sdef3, definition, (spl3 <=> (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk1,sk0)))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 26.23/14.03 cnf(ssp2, plain, (spl1 | spl3), inference(avatar_split_clause, [status(thm)], [p448, sdef1, sdef3])).
% 26.23/14.03 cnf(p20, plain, distinct_points(sk0,X0) | distinct_points(sk2,X0), inference(resolution, [status(thm)], [c3, c15])).
% 26.23/14.03 cnf(p23, plain, distinct_points(sk0,X0) | distinct_points(sk2,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p20, c3])).
% 26.23/14.03 cnf(p30, plain, distinct_points(sk0,X0) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p23, c0])).
% 26.23/14.03 cnf(p34, plain, distinct_points(X0,sk2) | distinct_points(sk0,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p30, c3])).
% 26.23/14.03 cnf(p97, plain, distinct_points(X0,sk2) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [p34, c0])).
% 26.23/14.03 cnf(p106, plain, distinct_points(sk2,sk0), inference(resolution, [status(thm)], [p97, c0])).
% 26.23/14.03 cnf(p111, plain, ~apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [p106, c7])).
% 26.23/14.03 cnf(p450, plain, distinct_lines(line_connecting(sk2,sk1),line_connecting(sk2,sk0)) | distinct_points(sk0,X0) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [p205, p111])).
% 26.23/14.03 fof(sdef4, definition, (spl4 <=> (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 26.23/14.03 cnf(ssp3, plain, (spl1 | spl4), inference(avatar_split_clause, [status(thm)], [p450, sdef1, sdef4])).
% 26.23/14.03 cnf(p54, plain, ~apart_point_and_line(X0,line_connecting(sk0,X1)) | distinct_points(X0,sk0) | distinct_points(X1,sk1), inference(resolution, [status(thm)], [c6, p25])).
% 26.23/14.03 cnf(p453, plain, distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | distinct_points(sk0,X1) | distinct_points(X1,sk0) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [p205, p54])).
% 26.23/14.03 fof(sdef5, definition, (spl5 <=> (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 26.23/14.03 cnf(ssp4, plain, (spl1 | spl5), inference(avatar_split_clause, [status(thm)], [p453, sdef1, sdef5])).
% 26.23/14.03 cnf(p55, plain, ~apart_point_and_line(X0,line_connecting(X1,sk1)) | distinct_points(X0,X1) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [c6, p25])).
% 26.23/14.03 cnf(p275, plain, ~apart_point_and_line(sk0,line_connecting(X0,sk1)) | distinct_points(sk0,X0), inference(factoring, [status(thm)], [p55])).
% 26.23/14.03 cnf(p456, plain, distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,sk1)) | distinct_points(sk0,sk0) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p205, p275])).
% 26.23/14.03 fof(sdef6, definition, (spl6 <=> (distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,sk1)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 26.23/14.03 cnf(ssp5, plain, (spl6 | spl7), inference(avatar_split_clause, [status(thm)], [p456, sdef6, sdef7])).
% 26.23/14.03 cnf(p59, plain, ~apart_point_and_line(X0,line_connecting(sk0,X1)) | distinct_points(X0,sk0) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [c6, p30])).
% 26.23/14.03 cnf(p459, plain, distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | distinct_points(sk0,X1) | distinct_points(X1,sk0) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p205, p59])).
% 26.23/14.03 fof(sdef8, definition, (spl8 <=> (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | distinct_points(X0,sk2))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 26.23/14.03 cnf(ssp6, plain, (spl1 | spl8), inference(avatar_split_clause, [status(thm)], [p459, sdef1, sdef8])).
% 26.23/14.03 cnf(p60, plain, ~apart_point_and_line(X0,line_connecting(X1,sk2)) | distinct_points(X0,X1) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [c6, p30])).
% 26.23/14.03 cnf(p288, plain, ~apart_point_and_line(sk0,line_connecting(X0,sk2)) | distinct_points(sk0,X0), inference(factoring, [status(thm)], [p60])).
% 26.23/14.03 cnf(p462, plain, distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,sk2)) | distinct_points(sk0,sk0) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p205, p288])).
% 26.23/14.03 fof(sdef9, definition, (spl9 <=> (distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,sk2)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 26.23/14.03 cnf(ssp7, plain, (spl7 | spl9), inference(avatar_split_clause, [status(thm)], [p462, sdef7, sdef9])).
% 26.23/14.03 cnf(p74, plain, ~apart_point_and_line(X0,line_connecting(sk1,X1)) | distinct_points(X0,X1) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [c7, p19])).
% 26.23/14.03 cnf(p306, plain, ~apart_point_and_line(sk0,line_connecting(sk1,X0)) | distinct_points(sk0,X0), inference(factoring, [status(thm)], [p74])).
% 26.23/14.03 cnf(p466, plain, distinct_lines(line_connecting(sk2,sk1),line_connecting(sk1,X0)) | distinct_points(sk0,sk0) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p205, p306])).
% 26.23/14.03 fof(sdef10, definition, (spl10 <=> (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk1,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 26.23/14.03 cnf(ssp8, plain, (spl7 | spl10), inference(avatar_split_clause, [status(thm)], [p466, sdef7, sdef10])).
% 26.23/14.03 cnf(p75, plain, ~apart_point_and_line(X0,line_connecting(sk2,X1)) | distinct_points(X0,X1) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [c7, p20])).
% 26.23/14.03 cnf(p329, plain, ~apart_point_and_line(sk0,line_connecting(sk2,X0)) | distinct_points(sk0,X0), inference(factoring, [status(thm)], [p75])).
% 26.23/14.03 cnf(p469, plain, distinct_lines(line_connecting(sk2,sk1),line_connecting(sk2,X0)) | distinct_points(sk0,sk0) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p205, p329])).
% 26.23/14.03 fof(sdef11, definition, (spl11 <=> (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk2,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 26.23/14.03 cnf(ssp9, plain, (spl7 | spl11), inference(avatar_split_clause, [status(thm)], [p469, sdef7, sdef11])).
% 26.23/14.03 cnf(p44, plain, distinct_points(X0,sk0) | distinct_points(X0,X1) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [p40, c3])).
% 26.23/14.03 cnf(p157, plain, distinct_points(X0,sk0) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p44, c0])).
% 26.23/14.03 cnf(p171, plain, distinct_points(sk1,X0) | ~apart_point_and_line(X1,line_connecting(X0,sk0)) | distinct_points(X1,sk0), inference(resolution, [status(thm)], [p157, c7])).
% 26.23/14.03 cnf(p472, plain, distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,sk0)) | distinct_points(sk0,X1) | distinct_points(sk1,X0) | distinct_points(X1,sk0), inference(resolution, [status(thm)], [p205, p171])).
% 26.23/14.03 fof(sdef12, definition, (spl12 <=> (distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,sk0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 26.23/14.03 cnf(ssp10, plain, (spl1 | spl12), inference(avatar_split_clause, [status(thm)], [p472, sdef1, sdef12])).
% 26.23/14.03 cnf(p51, plain, ~apart_point_and_line(X0,line_connecting(sk0,X1)) | distinct_points(X0,sk0) | distinct_points(sk1,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [c6, p22])).
% 26.23/14.03 cnf(p475, plain, distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | distinct_points(sk0,X1) | distinct_points(X1,sk0) | distinct_points(sk1,X2) | distinct_points(X0,X2), inference(resolution, [status(thm)], [p205, p51])).
% 26.23/14.03 fof(sdef13, definition, (spl13 <=> (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | distinct_points(sk1,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 26.23/14.03 cnf(ssp11, plain, (spl1 | spl13), inference(avatar_split_clause, [status(thm)], [p475, sdef1, sdef13])).
% 26.23/14.03 cnf(p107, plain, distinct_points(X0,sk0) | distinct_points(X0,X1) | distinct_points(sk2,X1), inference(resolution, [status(thm)], [p97, c3])).
% 26.23/14.03 cnf(p176, plain, distinct_points(X0,sk0) | distinct_points(sk2,X0), inference(resolution, [status(thm)], [p107, c0])).
% 26.23/14.03 cnf(p190, plain, distinct_points(sk2,X0) | ~apart_point_and_line(X1,line_connecting(X0,sk0)) | distinct_points(X1,sk0), inference(resolution, [status(thm)], [p176, c7])).
% 26.23/14.03 cnf(p477, plain, distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,sk0)) | distinct_points(sk0,X1) | distinct_points(sk2,X0) | distinct_points(X1,sk0), inference(resolution, [status(thm)], [p205, p190])).
% 26.23/14.03 fof(sdef14, definition, (spl14 <=> (distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,sk0)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 26.23/14.03 cnf(ssp12, plain, (spl1 | spl14), inference(avatar_split_clause, [status(thm)], [p477, sdef1, sdef14])).
% 26.23/14.03 cnf(p56, plain, ~apart_point_and_line(X0,line_connecting(sk0,X1)) | distinct_points(X0,sk0) | distinct_points(sk2,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [c6, p23])).
% 26.23/14.03 cnf(p499, plain, distinct_points(X0,sk0) | distinct_points(sk2,X1) | distinct_points(X2,X1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X2)) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p56, p205])).
% 26.23/14.03 fof(sdef15, definition, (spl15 <=> (distinct_points(sk2,X0) | distinct_points(X1,X0) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X1)))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 26.23/14.03 cnf(ssp13, plain, (spl1 | spl15), inference(avatar_split_clause, [status(thm)], [p499, sdef1, sdef15])).
% 26.23/14.03 cnf(p204, plain, distinct_lines(line_connecting(sk2,sk1),X0) | apart_point_and_line(sk0,X0), inference(resolution, [status(thm)], [c12, c18])).
% 26.23/14.03 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)).
% 26.23/14.03 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])).
% 26.23/14.03 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])).
% 26.23/14.03 cnf(c4, plain, ~distinct_lines(X0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 26.23/14.03 cnf(p212, plain, apart_point_and_line(sk0,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p204, c4])).
% 26.23/14.03 cnf(p521, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,sk1),X0) | distinct_points(sk0,sk0), inference(resolution, [status(thm)], [p212, p45])).
% 26.23/14.03 fof(sdef16, definition, (spl16 <=> (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 26.23/14.03 cnf(ssp14, plain, (spl7 | spl16), inference(avatar_split_clause, [status(thm)], [p521, sdef7, sdef16])).
% 26.23/14.03 cnf(p523, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X0) | distinct_points(sk0,sk0), inference(resolution, [status(thm)], [p212, p46])).
% 26.23/14.03 fof(sdef17, definition, (spl17 <=> (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X0))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 26.23/14.03 cnf(ssp15, plain, (spl7 | spl17), inference(avatar_split_clause, [status(thm)], [p523, sdef7, sdef17])).
% 26.23/14.03 cnf(p525, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk1,sk0),X0) | distinct_points(sk0,sk0), inference(resolution, [status(thm)], [p212, p96])).
% 26.23/14.03 fof(sdef18, definition, (spl18 <=> (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk1,sk0),X0))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 26.23/14.03 cnf(ssp16, plain, (spl7 | spl18), inference(avatar_split_clause, [status(thm)], [p525, sdef7, sdef18])).
% 26.23/14.03 cnf(p527, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk2,sk0),X0) | distinct_points(sk0,sk0), inference(resolution, [status(thm)], [p212, p111])).
% 26.23/14.03 fof(sdef19, definition, (spl19 <=> (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk2,sk0),X0))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 26.23/14.03 cnf(ssp17, plain, (spl7 | spl19), inference(avatar_split_clause, [status(thm)], [p527, sdef7, sdef19])).
% 26.23/14.03 cnf(p530, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,X1),X0) | distinct_points(sk0,sk0) | distinct_points(X1,sk1), inference(resolution, [status(thm)], [p212, p54])).
% 26.23/14.03 fof(sdef20, definition, (spl20 <=> (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,X1),X0) | distinct_points(X1,sk1))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 26.23/14.03 cnf(ssp18, plain, (spl7 | spl20), inference(avatar_split_clause, [status(thm)], [p530, sdef7, sdef20])).
% 26.23/14.03 cnf(p534, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,X1),X0) | distinct_points(sk0,sk0) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p212, p59])).
% 26.23/14.03 fof(sdef21, definition, (spl21 <=> (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,X1),X0) | distinct_points(X1,sk2))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 26.23/14.03 cnf(ssp19, plain, (spl7 | spl21), inference(avatar_split_clause, [status(thm)], [p534, sdef7, sdef21])).
% 26.23/14.03 cnf(p542, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(X1,sk0),X0) | distinct_points(sk1,X1) | distinct_points(sk0,sk0), inference(resolution, [status(thm)], [p212, p171])).
% 26.23/14.03 fof(sdef22, definition, (spl22 <=> (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(X1,sk0),X0) | distinct_points(sk1,X1))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 26.23/14.03 cnf(ssp20, plain, (spl7 | spl22), inference(avatar_split_clause, [status(thm)], [p542, sdef7, sdef22])).
% 26.23/14.03 cnf(p544, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,X1),X0) | distinct_points(sk0,sk0) | distinct_points(sk1,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [p212, p51])).
% 26.23/14.03 fof(sdef23, definition, (spl23 <=> (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,X1),X0) | distinct_points(sk1,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 26.23/14.03 cnf(ssp21, plain, (spl7 | spl23), inference(avatar_split_clause, [status(thm)], [p544, sdef7, sdef23])).
% 26.23/14.03 cnf(p546, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(X1,sk0),X0) | distinct_points(sk2,X1) | distinct_points(sk0,sk0), inference(resolution, [status(thm)], [p212, p190])).
% 26.23/14.03 fof(sdef24, definition, (spl24 <=> (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(X1,sk0),X0) | distinct_points(sk2,X1))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 26.23/14.03 cnf(ssp22, plain, (spl7 | spl24), inference(avatar_split_clause, [status(thm)], [p546, sdef7, sdef24])).
% 26.23/14.03 cnf(p549, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,X1),X0) | distinct_points(sk0,sk0) | distinct_points(sk2,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [p212, p56])).
% 26.23/14.03 fof(sdef25, definition, (spl25 <=> (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,X1),X0) | distinct_points(sk2,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 26.23/14.03 cnf(ssp23, plain, (spl7 | spl25), inference(avatar_split_clause, [status(thm)], [p549, sdef7, sdef25])).
% 26.23/14.03 cnf(p67, plain, ~apart_point_and_line(X0,line_connecting(sk0,X1)) | distinct_points(X0,sk0) | distinct_points(X2,sk1) | distinct_points(X2,X1), inference(resolution, [status(thm)], [c6, p29])).
% 26.23/14.03 cnf(p562, plain, distinct_points(X0,sk0) | distinct_points(X1,sk1) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X2)) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p67, p205])).
% 26.23/14.03 fof(sdef26, definition, (spl26 <=> (distinct_points(X0,sk1) | distinct_points(X0,X1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X1)))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 26.23/14.03 cnf(ssp24, plain, (spl1 | spl26), inference(avatar_split_clause, [status(thm)], [p562, sdef1, sdef26])).
% 26.23/14.03 cnf(p564, plain, distinct_points(sk0,sk0) | distinct_points(X0,sk1) | distinct_points(X0,X1) | distinct_lines(line_connecting(sk2,sk1),X2) | distinct_lines(line_connecting(sk0,X1),X2), inference(resolution, [status(thm)], [p67, p212])).
% 26.23/14.03 fof(sdef27, definition, (spl27 <=> (distinct_points(X0,sk1) | distinct_points(X0,X1) | distinct_lines(line_connecting(sk2,sk1),X2) | distinct_lines(line_connecting(sk0,X1),X2))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 26.23/14.03 cnf(ssp25, plain, (spl7 | spl27), inference(avatar_split_clause, [status(thm)], [p564, sdef7, sdef27])).
% 26.23/14.03 cnf(p53, plain, ~apart_point_and_line(X0,line_connecting(X1,X2)) | distinct_points(X0,X1) | distinct_points(sk0,X1) | distinct_points(sk1,X2), inference(resolution, [status(thm)], [c6, p22])).
% 26.23/14.03 cnf(p493, plain, ~apart_point_and_line(sk0,line_connecting(X0,X1)) | distinct_points(sk0,X0) | distinct_points(sk1,X1), inference(factoring, [status(thm)], [p53])).
% 26.23/14.03 cnf(p566, plain, distinct_points(sk0,X0) | distinct_points(sk1,X1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,X1)) | distinct_points(sk0,sk0), inference(resolution, [status(thm)], [p493, p205])).
% 26.23/14.03 fof(sdef28, definition, (spl28 <=> (distinct_points(sk0,X0) | distinct_points(sk1,X1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,X1)))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 26.23/14.03 cnf(ssp26, plain, (spl7 | spl28), inference(avatar_split_clause, [status(thm)], [p566, sdef7, sdef28])).
% 26.23/14.03 cnf(p58, plain, ~apart_point_and_line(X0,line_connecting(X1,X2)) | distinct_points(X0,X1) | distinct_points(sk0,X1) | distinct_points(sk2,X2), inference(resolution, [status(thm)], [c6, p23])).
% 26.23/14.03 cnf(p509, plain, ~apart_point_and_line(sk0,line_connecting(X0,X1)) | distinct_points(sk0,X0) | distinct_points(sk2,X1), inference(factoring, [status(thm)], [p58])).
% 26.23/14.03 cnf(p569, plain, distinct_points(sk0,X0) | distinct_points(sk2,X1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,X1)) | distinct_points(sk0,sk0), inference(resolution, [status(thm)], [p509, p205])).
% 26.23/14.03 fof(sdef29, definition, (spl29 <=> (distinct_points(sk0,X0) | distinct_points(sk2,X1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,X1)))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 26.23/14.03 cnf(ssp27, plain, (spl7 | spl29), inference(avatar_split_clause, [status(thm)], [p569, sdef7, sdef29])).
% 26.23/14.03 cnf(p476, plain, (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl13), inference(avatar_component_clause, [status(thm)], [sdef13])).
% 26.23/14.03 cnf(p869, plain, (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,sk1)) | distinct_points(sk1,X0) | ~spl13), inference(factoring, [status(thm)], [p476])).
% 26.23/14.03 cnf(ssp28, plain, (~spl13 | spl0 | spl30), inference(avatar_split_clause, [status(thm)], [p869, sdef0, sdef30])).
% 26.23/14.03 cnf(p500, plain, (distinct_points(sk2,X0) | distinct_points(X1,X0) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X1)) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 26.23/14.03 cnf(p889, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,sk2)) | ~spl15), inference(factoring, [status(thm)], [p500])).
% 26.23/14.03 cnf(ssp29, plain, (~spl15 | spl2 | spl31), inference(avatar_split_clause, [status(thm)], [p889, sdef2, sdef31])).
% 26.23/14.03 cnf(p94, plain, ~apart_point_and_line(X0,line_connecting(X1,X2)) | distinct_points(X0,X2) | distinct_points(X1,sk1) | distinct_points(sk0,X2), inference(resolution, [status(thm)], [c7, p29])).
% 26.23/14.03 cnf(p904, plain, ~apart_point_and_line(sk0,line_connecting(X0,X1)) | distinct_points(sk0,X1) | distinct_points(X0,sk1), inference(factoring, [status(thm)], [p94])).
% 26.23/14.03 cnf(p908, plain, distinct_points(sk0,X0) | distinct_points(X1,sk1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(X1,X0)) | distinct_points(sk0,sk0), inference(resolution, [status(thm)], [p904, p205])).
% 26.23/14.03 fof(sdef32, definition, (spl32 <=> (distinct_points(sk0,X0) | distinct_points(X1,sk1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(X1,X0)))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 26.23/14.03 cnf(ssp30, plain, (spl7 | spl32), inference(avatar_split_clause, [status(thm)], [p908, sdef7, sdef32])).
% 26.23/14.03 cnf(p101, plain, distinct_points(X0,sk2) | distinct_points(X0,X1) | ~apart_point_and_line(X2,line_connecting(sk0,X1)) | distinct_points(X2,sk0), inference(resolution, [status(thm)], [p34, c6])).
% 26.23/14.03 cnf(p921, plain, distinct_points(X0,sk2) | distinct_points(X0,X1) | distinct_points(X2,sk0) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X1)) | distinct_points(sk0,X2), inference(resolution, [status(thm)], [p101, p205])).
% 26.23/14.03 fof(sdef33, definition, (spl33 <=> (distinct_points(X0,sk2) | distinct_points(X0,X1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X1)))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 26.23/14.03 cnf(ssp31, plain, (spl1 | spl33), inference(avatar_split_clause, [status(thm)], [p921, sdef1, sdef33])).
% 26.23/14.03 cnf(p923, plain, distinct_points(X0,sk2) | distinct_points(X0,X1) | distinct_points(sk0,sk0) | distinct_lines(line_connecting(sk2,sk1),X2) | distinct_lines(line_connecting(sk0,X1),X2), inference(resolution, [status(thm)], [p101, p212])).
% 26.23/14.03 fof(sdef34, definition, (spl34 <=> (distinct_points(X0,sk2) | distinct_points(X0,X1) | distinct_lines(line_connecting(sk2,sk1),X2) | distinct_lines(line_connecting(sk0,X1),X2))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 26.23/14.03 cnf(ssp32, plain, (spl7 | spl34), inference(avatar_split_clause, [status(thm)], [p923, sdef7, sdef34])).
% 26.23/14.03 cnf(p105, plain, distinct_points(X0,sk2) | distinct_points(sk0,X1) | ~apart_point_and_line(X2,line_connecting(X0,X1)) | distinct_points(X2,X1), inference(resolution, [status(thm)], [p34, c7])).
% 26.23/14.03 cnf(p958, plain, distinct_points(X0,sk2) | distinct_points(sk0,X1) | ~apart_point_and_line(sk0,line_connecting(X0,X1)), inference(factoring, [status(thm)], [p105])).
% 26.23/14.03 cnf(p961, plain, distinct_points(X0,sk2) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,X1)) | distinct_points(sk0,sk0), inference(resolution, [status(thm)], [p958, p205])).
% 26.23/14.03 fof(sdef35, definition, (spl35 <=> (distinct_points(X0,sk2) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,X1)))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 26.23/14.03 cnf(ssp33, plain, (spl7 | spl35), inference(avatar_split_clause, [status(thm)], [p961, sdef7, sdef35])).
% 26.23/14.03 cnf(p563, plain, (distinct_points(X0,sk1) | distinct_points(X0,X1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X1)) | ~spl26), inference(avatar_component_clause, [status(thm)], [sdef26])).
% 26.23/14.03 cnf(p1006, plain, (distinct_points(X0,sk1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,sk1)) | ~spl26), inference(factoring, [status(thm)], [p563])).
% 26.23/14.03 cnf(ssp34, plain, (~spl26 | spl0 | spl36), inference(avatar_split_clause, [status(thm)], [p1006, sdef0, sdef36])).
% 26.23/14.03 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)).
% 26.23/14.03 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])).
% 26.23/14.03 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])).
% 26.23/14.03 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])).
% 26.23/14.03 cnf(p129, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1), inference(resolution, [status(thm)], [c10, c16])).
% 26.23/14.03 cnf(p1046, plain, apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk0,X0), inference(resolution, [status(thm)], [p129, p204])).
% 26.23/14.03 fof(sdef38, definition, (spl38 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk0,X0))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 26.23/14.03 cnf(ssp35, plain, (spl37 | spl38 | spl39), inference(avatar_split_clause, [status(thm)], [p1046, sdef37, sdef38, sdef39])).
% 26.23/14.03 cnf(p1050, plain, apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [p129, p205])).
% 26.23/14.03 fof(sdef40, definition, (spl40 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 26.23/14.03 cnf(ssp36, plain, (spl37 | spl39 | spl40), inference(avatar_split_clause, [status(thm)], [p1050, sdef37, sdef39, sdef40])).
% 26.23/14.03 cnf(p444, plain, (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,sk1)) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 26.23/14.03 cnf(p1052, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | ~spl0), inference(resolution, [status(thm)], [p129, p444])).
% 26.23/14.03 cnf(ssp37, plain, (~spl0 | spl37 | spl39 | spl41 | spl42), inference(avatar_split_clause, [status(thm)], [p1052, sdef37, sdef39, sdef41, sdef42])).
% 26.23/14.03 cnf(p447, plain, (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,sk2)) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 26.23/14.03 cnf(p1055, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | ~spl2), inference(resolution, [status(thm)], [p129, p447])).
% 26.23/14.03 fof(sdef43, definition, (spl43 <=> (apart_point_and_line(sk1,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 26.23/14.03 fof(sdef44, definition, (spl44 <=> (apart_point_and_line(sk2,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 26.23/14.03 cnf(ssp38, plain, (~spl2 | spl37 | spl39 | spl43 | spl44), inference(avatar_split_clause, [status(thm)], [p1055, sdef37, sdef39, sdef43, sdef44])).
% 26.23/14.03 cnf(p449, plain, (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk1,sk0)) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 26.23/14.03 cnf(p1058, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | ~spl3), inference(resolution, [status(thm)], [p129, p449])).
% 26.23/14.03 fof(sdef45, definition, (spl45 <=> (apart_point_and_line(sk1,line_connecting(sk1,sk0)))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 26.23/14.03 fof(sdef46, definition, (spl46 <=> (apart_point_and_line(sk2,line_connecting(sk1,sk0)))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 26.23/14.03 cnf(ssp39, plain, (~spl3 | spl37 | spl39 | spl45 | spl46), inference(avatar_split_clause, [status(thm)], [p1058, sdef37, sdef39, sdef45, sdef46])).
% 26.23/14.03 cnf(p451, plain, (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk2,sk0)) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 26.23/14.03 cnf(p1061, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk2,sk0)) | ~spl4), inference(resolution, [status(thm)], [p129, p451])).
% 26.23/14.03 fof(sdef47, definition, (spl47 <=> (apart_point_and_line(sk1,line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 26.23/14.03 fof(sdef48, definition, (spl48 <=> (apart_point_and_line(sk2,line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 26.23/14.03 cnf(ssp40, plain, (~spl4 | spl37 | spl39 | spl47 | spl48), inference(avatar_split_clause, [status(thm)], [p1061, sdef37, sdef39, sdef47, sdef48])).
% 26.23/14.03 cnf(p454, plain, (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | distinct_points(X0,sk1) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 26.23/14.03 cnf(p1064, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(X0,sk1) | ~spl5), inference(resolution, [status(thm)], [p129, p454])).
% 26.23/14.03 fof(sdef49, definition, (spl49 <=> (apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 26.23/14.03 cnf(ssp41, plain, (~spl5 | spl37 | spl39 | spl49), inference(avatar_split_clause, [status(thm)], [p1064, sdef37, sdef39, sdef49])).
% 26.23/14.03 cnf(p460, plain, (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | distinct_points(X0,sk2) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 26.23/14.03 cnf(p1066, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(X0,sk2) | ~spl8), inference(resolution, [status(thm)], [p129, p460])).
% 26.23/14.03 fof(sdef50, definition, (spl50 <=> (apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(X0,sk2))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 26.23/14.03 cnf(ssp42, plain, (~spl8 | spl37 | spl39 | spl50), inference(avatar_split_clause, [status(thm)], [p1066, sdef37, sdef39, sdef50])).
% 26.23/14.03 cnf(p473, plain, (distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,sk0)) | distinct_points(sk1,X0) | ~spl12), inference(avatar_component_clause, [status(thm)], [sdef12])).
% 26.23/14.03 cnf(p1068, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(X0,sk0)) | distinct_points(sk1,X0) | ~spl12), inference(resolution, [status(thm)], [p129, p473])).
% 26.23/14.03 fof(sdef51, definition, (spl51 <=> (apart_point_and_line(sk1,line_connecting(X0,sk0)) | apart_point_and_line(sk2,line_connecting(X0,sk0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 26.23/14.03 cnf(ssp43, plain, (~spl12 | spl37 | spl39 | spl51), inference(avatar_split_clause, [status(thm)], [p1068, sdef37, sdef39, sdef51])).
% 26.23/14.03 cnf(p478, plain, (distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,sk0)) | distinct_points(sk2,X0) | ~spl14), inference(avatar_component_clause, [status(thm)], [sdef14])).
% 26.23/14.03 cnf(p1070, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(X0,sk0)) | distinct_points(sk2,X0) | ~spl14), inference(resolution, [status(thm)], [p129, p478])).
% 26.23/14.03 fof(sdef52, definition, (spl52 <=> (apart_point_and_line(sk1,line_connecting(X0,sk0)) | apart_point_and_line(sk2,line_connecting(X0,sk0)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 26.23/14.03 cnf(ssp44, plain, (~spl14 | spl37 | spl39 | spl52), inference(avatar_split_clause, [status(thm)], [p1070, sdef37, sdef39, sdef52])).
% 26.23/14.03 cnf(p481, plain, (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl0), inference(resolution, [status(thm)], [p444, c4])).
% 26.23/14.03 cnf(p1072, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl0), inference(resolution, [status(thm)], [p129, p481])).
% 26.23/14.03 fof(sdef53, definition, (spl53 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 26.23/14.03 cnf(ssp45, plain, (~spl0 | spl37 | spl39 | spl53), inference(avatar_split_clause, [status(thm)], [p1072, sdef37, sdef39, sdef53])).
% 26.23/14.03 cnf(p492, plain, (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl2), inference(resolution, [status(thm)], [p447, c4])).
% 26.23/14.03 cnf(p1074, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl2), inference(resolution, [status(thm)], [p129, p492])).
% 26.23/14.03 fof(sdef54, definition, (spl54 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X0))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 26.23/14.03 cnf(ssp46, plain, (~spl2 | spl37 | spl39 | spl54), inference(avatar_split_clause, [status(thm)], [p1074, sdef37, sdef39, sdef54])).
% 26.23/14.03 cnf(p495, plain, (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk1,sk0),X0) | ~spl3), inference(resolution, [status(thm)], [p449, c4])).
% 26.23/14.03 cnf(p1076, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk0),X0) | ~spl3), inference(resolution, [status(thm)], [p129, p495])).
% 26.23/14.03 fof(sdef55, definition, (spl55 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk0),X0))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 26.23/14.03 cnf(ssp47, plain, (~spl3 | spl37 | spl39 | spl55), inference(avatar_split_clause, [status(thm)], [p1076, sdef37, sdef39, sdef55])).
% 26.23/14.03 cnf(p496, plain, (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk2,sk0),X0) | ~spl4), inference(resolution, [status(thm)], [p451, c4])).
% 26.23/14.03 cnf(p1078, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk0),X0) | ~spl4), inference(resolution, [status(thm)], [p129, p496])).
% 26.23/14.03 fof(sdef56, definition, (spl56 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk0),X0))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 26.23/14.03 cnf(ssp48, plain, (~spl4 | spl37 | spl39 | spl56), inference(avatar_split_clause, [status(thm)], [p1078, sdef37, sdef39, sdef56])).
% 26.23/14.03 cnf(p1080, plain, apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk0,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p129, p212])).
% 26.23/14.03 fof(sdef57, definition, (spl57 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk0,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 26.23/14.03 cnf(ssp49, plain, (spl37 | spl39 | spl57), inference(avatar_split_clause, [status(thm)], [p1080, sdef37, sdef39, sdef57])).
% 26.23/14.03 cnf(p1082, plain, apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(sk0,X0) | distinct_lines(line_connecting(sk2,sk1),X1), inference(resolution, [status(thm)], [p129, p212])).
% 26.23/14.03 fof(sdef58, definition, (spl58 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X0))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 26.23/14.03 cnf(ssp50, plain, (spl38 | spl58), inference(avatar_split_clause, [status(thm)], [p1082, sdef38, sdef58])).
% 26.23/14.03 cnf(p522, plain, (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl16), inference(avatar_component_clause, [status(thm)], [sdef16])).
% 26.23/14.03 cnf(p1084, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl16), inference(resolution, [status(thm)], [p129, p522])).
% 26.23/14.03 cnf(ssp51, plain, (~spl16 | spl37 | spl39 | spl53), inference(avatar_split_clause, [status(thm)], [p1084, sdef37, sdef39, sdef53])).
% 26.23/14.03 fof(f1, axiom, ! [X] : ~ distinct_lines(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart2)).
% 26.23/14.03 fof(f1_nnf, plain, ! [X] : (~(distinct_lines(X,X))), inference(nnf_transformation, [status(thm)], [f1])).
% 26.23/14.03 fof(f1_sk, plain, ! [X] : (~(distinct_lines(X,X))), inference(skolemisation, [status(esa)], [f1_nnf])).
% 26.23/14.03 cnf(c1, plain, ~distinct_lines(X0,X0), inference(cnf_transformation, [status(esa)], [f1_sk])).
% 26.23/14.03 cnf(p553, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk1)) | ~spl16), inference(resolution, [status(thm)], [p522, c1])).
% 26.23/14.03 cnf(p1085, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | ~spl16), inference(resolution, [status(thm)], [p129, p553])).
% 26.23/14.03 cnf(ssp52, plain, (~spl16 | spl37 | spl39 | spl41 | spl42), inference(avatar_split_clause, [status(thm)], [p1085, sdef37, sdef39, sdef41, sdef42])).
% 26.23/14.03 cnf(p524, plain, (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 26.23/14.03 cnf(p1086, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl17), inference(resolution, [status(thm)], [p129, p524])).
% 26.23/14.03 cnf(ssp53, plain, (~spl17 | spl37 | spl39 | spl54), inference(avatar_split_clause, [status(thm)], [p1086, sdef37, sdef39, sdef54])).
% 26.23/14.03 cnf(p555, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk2,sk1)) | ~spl17), inference(resolution, [status(thm)], [p524, c1])).
% 26.23/14.03 cnf(p1087, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | ~spl17), inference(resolution, [status(thm)], [p129, p555])).
% 26.23/14.03 cnf(ssp54, plain, (~spl17 | spl37 | spl39 | spl43 | spl44), inference(avatar_split_clause, [status(thm)], [p1087, sdef37, sdef39, sdef43, sdef44])).
% 26.23/14.03 cnf(p526, plain, (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk1,sk0),X0) | ~spl18), inference(avatar_component_clause, [status(thm)], [sdef18])).
% 26.23/14.03 cnf(p1088, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk0),X0) | ~spl18), inference(resolution, [status(thm)], [p129, p526])).
% 26.23/14.03 cnf(ssp55, plain, (~spl18 | spl37 | spl39 | spl55), inference(avatar_split_clause, [status(thm)], [p1088, sdef37, sdef39, sdef55])).
% 26.23/14.03 cnf(p558, plain, (distinct_lines(line_connecting(sk1,sk0),line_connecting(sk2,sk1)) | ~spl18), inference(resolution, [status(thm)], [p526, c1])).
% 26.23/14.03 cnf(p1089, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | ~spl18), inference(resolution, [status(thm)], [p129, p558])).
% 26.23/14.03 cnf(ssp56, plain, (~spl18 | spl37 | spl39 | spl45 | spl46), inference(avatar_split_clause, [status(thm)], [p1089, sdef37, sdef39, sdef45, sdef46])).
% 26.23/14.03 cnf(p528, plain, (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk2,sk0),X0) | ~spl19), inference(avatar_component_clause, [status(thm)], [sdef19])).
% 26.23/14.03 cnf(p1090, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk0),X0) | ~spl19), inference(resolution, [status(thm)], [p129, p528])).
% 26.23/14.03 cnf(ssp57, plain, (~spl19 | spl37 | spl39 | spl56), inference(avatar_split_clause, [status(thm)], [p1090, sdef37, sdef39, sdef56])).
% 26.23/14.03 cnf(p560, plain, (distinct_lines(line_connecting(sk2,sk0),line_connecting(sk2,sk1)) | ~spl19), inference(resolution, [status(thm)], [p528, c1])).
% 26.23/14.03 cnf(p1091, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | ~spl19), inference(resolution, [status(thm)], [p129, p560])).
% 26.23/14.03 cnf(ssp58, plain, (~spl19 | spl37 | spl39 | spl47 | spl48), inference(avatar_split_clause, [status(thm)], [p1091, sdef37, sdef39, sdef47, sdef48])).
% 26.23/14.03 cnf(p1092, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl13), inference(resolution, [status(thm)], [p129, p476])).
% 26.23/14.03 fof(sdef59, definition, (spl59 <=> (apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(sk1,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 26.23/14.03 cnf(ssp59, plain, (~spl13 | spl37 | spl39 | spl59), inference(avatar_split_clause, [status(thm)], [p1092, sdef37, sdef39, sdef59])).
% 26.23/14.03 cnf(p871, plain, (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | distinct_points(X0,sk1) | ~spl13), inference(resolution, [status(thm)], [p476, c0])).
% 26.23/14.03 cnf(p1094, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(X0,sk1) | ~spl13), inference(resolution, [status(thm)], [p129, p871])).
% 26.23/14.03 cnf(ssp60, plain, (~spl13 | spl37 | spl39 | spl49), inference(avatar_split_clause, [status(thm)], [p1094, sdef37, sdef39, sdef49])).
% 26.23/14.03 cnf(p872, plain, (distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | distinct_points(sk1,X0) | ~spl13), inference(resolution, [status(thm)], [p476, c0])).
% 26.23/14.03 cnf(p1095, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(sk1,X0) | ~spl13), inference(resolution, [status(thm)], [p129, p872])).
% 26.23/14.03 fof(sdef60, definition, (spl60 <=> (apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 26.23/14.03 cnf(ssp61, plain, (~spl13 | spl37 | spl39 | spl60), inference(avatar_split_clause, [status(thm)], [p1095, sdef37, sdef39, sdef60])).
% 26.23/14.03 cnf(p497, plain, (distinct_points(X0,sk1) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(line_connecting(sk0,X0),X1) | ~spl5), inference(resolution, [status(thm)], [p454, c4])).
% 26.23/14.03 cnf(p1097, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_points(X1,sk1) | distinct_lines(line_connecting(sk0,X1),X0) | ~spl5), inference(resolution, [status(thm)], [p129, p497])).
% 26.23/14.03 fof(sdef61, definition, (spl61 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_points(X1,sk1) | distinct_lines(line_connecting(sk0,X1),X0))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 26.23/14.03 cnf(ssp62, plain, (~spl5 | spl37 | spl39 | spl61), inference(avatar_split_clause, [status(thm)], [p1097, sdef37, sdef39, sdef61])).
% 26.23/14.03 cnf(p1099, plain, (apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | apart_point_and_line(sk2,X1) | distinct_points(X0,sk1) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl5), inference(resolution, [status(thm)], [p129, p497])).
% 26.23/14.03 cnf(ssp63, plain, (~spl5 | spl49 | spl58), inference(avatar_split_clause, [status(thm)], [p1099, sdef49, sdef58])).
% 26.23/14.03 cnf(p1100, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(sk2,X1) | distinct_points(X0,X1) | ~spl15), inference(resolution, [status(thm)], [p129, p500])).
% 26.23/14.03 fof(sdef62, definition, (spl62 <=> (apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(sk2,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 26.23/14.03 cnf(ssp64, plain, (~spl15 | spl37 | spl39 | spl62), inference(avatar_split_clause, [status(thm)], [p1100, sdef37, sdef39, sdef62])).
% 26.23/14.03 cnf(p891, plain, (distinct_points(X0,sk2) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | ~spl15), inference(resolution, [status(thm)], [p500, c0])).
% 26.23/14.03 cnf(p1102, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(X0,sk2) | ~spl15), inference(resolution, [status(thm)], [p129, p891])).
% 26.23/14.03 cnf(ssp65, plain, (~spl15 | spl37 | spl39 | spl50), inference(avatar_split_clause, [status(thm)], [p1102, sdef37, sdef39, sdef50])).
% 26.23/14.03 cnf(p892, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | ~spl15), inference(resolution, [status(thm)], [p500, c0])).
% 26.23/14.03 cnf(p1103, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(sk2,X0) | ~spl15), inference(resolution, [status(thm)], [p129, p892])).
% 26.23/14.03 fof(sdef63, definition, (spl63 <=> (apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 26.23/14.03 cnf(ssp66, plain, (~spl15 | spl37 | spl39 | spl63), inference(avatar_split_clause, [status(thm)], [p1103, sdef37, sdef39, sdef63])).
% 26.23/14.03 cnf(p501, plain, (distinct_points(X0,sk2) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(line_connecting(sk0,X0),X1) | ~spl8), inference(resolution, [status(thm)], [p460, c4])).
% 26.23/14.03 cnf(p1105, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_points(X1,sk2) | distinct_lines(line_connecting(sk0,X1),X0) | ~spl8), inference(resolution, [status(thm)], [p129, p501])).
% 26.23/14.03 fof(sdef64, definition, (spl64 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_points(X1,sk2) | distinct_lines(line_connecting(sk0,X1),X0))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 26.23/14.03 cnf(ssp67, plain, (~spl8 | spl37 | spl39 | spl64), inference(avatar_split_clause, [status(thm)], [p1105, sdef37, sdef39, sdef64])).
% 26.23/14.03 cnf(p1107, plain, (apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | apart_point_and_line(sk2,X1) | distinct_points(X0,sk2) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl8), inference(resolution, [status(thm)], [p129, p501])).
% 26.23/14.03 cnf(ssp68, plain, (~spl8 | spl50 | spl58), inference(avatar_split_clause, [status(thm)], [p1107, sdef50, sdef58])).
% 26.23/14.03 cnf(p505, plain, (distinct_points(sk1,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(line_connecting(X0,sk0),X1) | ~spl12), inference(resolution, [status(thm)], [p473, c4])).
% 26.23/14.03 cnf(p1108, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_points(sk1,X1) | distinct_lines(line_connecting(X1,sk0),X0) | ~spl12), inference(resolution, [status(thm)], [p129, p505])).
% 26.23/14.03 fof(sdef65, definition, (spl65 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_points(sk1,X1) | distinct_lines(line_connecting(X1,sk0),X0))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 26.23/14.03 cnf(ssp69, plain, (~spl12 | spl37 | spl39 | spl65), inference(avatar_split_clause, [status(thm)], [p1108, sdef37, sdef39, sdef65])).
% 26.23/14.03 cnf(p1110, plain, (apart_point_and_line(sk1,line_connecting(X0,sk0)) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,line_connecting(X0,sk0)) | apart_point_and_line(sk2,X1) | distinct_points(sk1,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl12), inference(resolution, [status(thm)], [p129, p505])).
% 26.23/14.03 cnf(ssp70, plain, (~spl12 | spl51 | spl58), inference(avatar_split_clause, [status(thm)], [p1110, sdef51, sdef58])).
% 26.23/14.03 cnf(p506, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(line_connecting(X0,sk0),X1) | ~spl14), inference(resolution, [status(thm)], [p478, c4])).
% 26.23/14.03 cnf(p1111, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_points(sk2,X1) | distinct_lines(line_connecting(X1,sk0),X0) | ~spl14), inference(resolution, [status(thm)], [p129, p506])).
% 26.23/14.03 fof(sdef66, definition, (spl66 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_points(sk2,X1) | distinct_lines(line_connecting(X1,sk0),X0))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 26.23/14.03 cnf(ssp71, plain, (~spl14 | spl37 | spl39 | spl66), inference(avatar_split_clause, [status(thm)], [p1111, sdef37, sdef39, sdef66])).
% 26.23/14.03 cnf(p1113, plain, (apart_point_and_line(sk1,line_connecting(X0,sk0)) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,line_connecting(X0,sk0)) | apart_point_and_line(sk2,X1) | distinct_points(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl14), inference(resolution, [status(thm)], [p129, p506])).
% 26.23/14.03 cnf(ssp72, plain, (~spl14 | spl52 | spl58), inference(avatar_split_clause, [status(thm)], [p1113, sdef52, sdef58])).
% 26.23/14.03 cnf(p508, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl0), inference(resolution, [status(thm)], [p481, c4])).
% 26.23/14.03 cnf(p1114, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl0), inference(resolution, [status(thm)], [p129, p508])).
% 26.23/14.03 fof(sdef67, definition, (spl67 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 26.23/14.03 cnf(ssp73, plain, (~spl0 | spl41 | spl42 | spl67), inference(avatar_split_clause, [status(thm)], [p1114, sdef41, sdef42, sdef67])).
% 26.23/14.03 cnf(p1116, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X1,X0) | ~spl0), inference(resolution, [status(thm)], [p129, p508])).
% 26.23/14.03 fof(sdef68, definition, (spl68 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 26.23/14.03 cnf(ssp74, plain, (~spl0 | spl37 | spl39 | spl68), inference(avatar_split_clause, [status(thm)], [p1116, sdef37, sdef39, sdef68])).
% 26.23/14.03 cnf(p1118, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl0), inference(resolution, [status(thm)], [p129, p508])).
% 26.23/14.03 cnf(ssp75, plain, (~spl0 | spl53 | spl58), inference(avatar_split_clause, [status(thm)], [p1118, sdef53, sdef58])).
% 26.23/14.03 cnf(p925, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl0), inference(resolution, [status(thm)], [p508, c1])).
% 26.23/14.03 cnf(p1119, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl0), inference(resolution, [status(thm)], [p129, p925])).
% 26.23/14.03 fof(sdef69, definition, (spl69 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 26.23/14.03 cnf(ssp76, plain, (~spl0 | spl41 | spl42 | spl69), inference(avatar_split_clause, [status(thm)], [p1119, sdef41, sdef42, sdef69])).
% 26.23/14.03 cnf(p512, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl2), inference(resolution, [status(thm)], [p492, c4])).
% 26.23/14.03 cnf(p1121, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl2), inference(resolution, [status(thm)], [p129, p512])).
% 26.23/14.03 cnf(ssp77, plain, (~spl2 | spl43 | spl44 | spl67), inference(avatar_split_clause, [status(thm)], [p1121, sdef43, sdef44, sdef67])).
% 26.23/14.03 cnf(p1122, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl2), inference(resolution, [status(thm)], [p129, p512])).
% 26.23/14.03 fof(sdef70, definition, (spl70 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 26.23/14.03 cnf(ssp78, plain, (~spl2 | spl37 | spl39 | spl70), inference(avatar_split_clause, [status(thm)], [p1122, sdef37, sdef39, sdef70])).
% 26.23/14.03 cnf(p1124, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl2), inference(resolution, [status(thm)], [p129, p512])).
% 26.23/14.03 cnf(ssp79, plain, (~spl2 | spl54 | spl58), inference(avatar_split_clause, [status(thm)], [p1124, sdef54, sdef58])).
% 26.23/14.03 cnf(p930, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl2), inference(resolution, [status(thm)], [p512, c1])).
% 26.23/14.03 cnf(p1125, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl2), inference(resolution, [status(thm)], [p129, p930])).
% 26.23/14.03 cnf(ssp80, plain, (~spl2 | spl43 | spl44 | spl69), inference(avatar_split_clause, [status(thm)], [p1125, sdef43, sdef44, sdef69])).
% 26.23/14.03 cnf(p514, plain, (distinct_lines(line_connecting(sk1,sk0),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl3), inference(resolution, [status(thm)], [p495, c4])).
% 26.23/14.03 cnf(p1126, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl3), inference(resolution, [status(thm)], [p129, p514])).
% 26.23/14.03 cnf(ssp81, plain, (~spl3 | spl45 | spl46 | spl67), inference(avatar_split_clause, [status(thm)], [p1126, sdef45, sdef46, sdef67])).
% 26.23/14.03 cnf(p1127, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk0),X1) | distinct_lines(X1,X0) | ~spl3), inference(resolution, [status(thm)], [p129, p514])).
% 26.23/14.03 fof(sdef71, definition, (spl71 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk0),X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 26.23/14.03 cnf(ssp82, plain, (~spl3 | spl37 | spl39 | spl71), inference(avatar_split_clause, [status(thm)], [p1127, sdef37, sdef39, sdef71])).
% 26.23/14.03 cnf(p1129, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk1,sk0),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl3), inference(resolution, [status(thm)], [p129, p514])).
% 26.23/14.03 cnf(ssp83, plain, (~spl3 | spl55 | spl58), inference(avatar_split_clause, [status(thm)], [p1129, sdef55, sdef58])).
% 26.23/14.03 cnf(p935, plain, (distinct_lines(line_connecting(sk1,sk0),X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl3), inference(resolution, [status(thm)], [p514, c1])).
% 26.23/14.03 cnf(p1130, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl3), inference(resolution, [status(thm)], [p129, p935])).
% 26.23/14.03 cnf(ssp84, plain, (~spl3 | spl45 | spl46 | spl69), inference(avatar_split_clause, [status(thm)], [p1130, sdef45, sdef46, sdef69])).
% 26.23/14.03 cnf(p516, plain, (distinct_lines(line_connecting(sk2,sk0),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl4), inference(resolution, [status(thm)], [p496, c4])).
% 26.23/14.03 cnf(p1131, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl4), inference(resolution, [status(thm)], [p129, p516])).
% 26.23/14.03 cnf(ssp85, plain, (~spl4 | spl47 | spl48 | spl67), inference(avatar_split_clause, [status(thm)], [p1131, sdef47, sdef48, sdef67])).
% 26.23/14.03 cnf(p1132, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk0),X1) | distinct_lines(X1,X0) | ~spl4), inference(resolution, [status(thm)], [p129, p516])).
% 26.23/14.03 fof(sdef72, definition, (spl72 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk0),X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 26.23/14.03 cnf(ssp86, plain, (~spl4 | spl37 | spl39 | spl72), inference(avatar_split_clause, [status(thm)], [p1132, sdef37, sdef39, sdef72])).
% 26.23/14.03 cnf(p1134, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk2,sk0),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl4), inference(resolution, [status(thm)], [p129, p516])).
% 26.23/14.03 cnf(ssp87, plain, (~spl4 | spl56 | spl58), inference(avatar_split_clause, [status(thm)], [p1134, sdef56, sdef58])).
% 26.23/14.03 cnf(p940, plain, (distinct_lines(line_connecting(sk2,sk0),X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl4), inference(resolution, [status(thm)], [p516, c1])).
% 26.23/14.03 cnf(p1135, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl4), inference(resolution, [status(thm)], [p129, p940])).
% 26.23/14.03 cnf(ssp88, plain, (~spl4 | spl47 | spl48 | spl69), inference(avatar_split_clause, [status(thm)], [p1135, sdef47, sdef48, sdef69])).
% 26.23/14.03 cnf(p531, plain, (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,X1),X0) | distinct_points(X1,sk1) | ~spl20), inference(avatar_component_clause, [status(thm)], [sdef20])).
% 26.23/14.03 cnf(p1136, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,X1),X0) | distinct_points(X1,sk1) | ~spl20), inference(resolution, [status(thm)], [p129, p531])).
% 26.23/14.03 cnf(ssp89, plain, (~spl20 | spl37 | spl39 | spl61), inference(avatar_split_clause, [status(thm)], [p1136, sdef37, sdef39, sdef61])).
% 26.23/14.03 cnf(p1137, plain, (apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_points(X0,sk1) | ~spl20), inference(resolution, [status(thm)], [p129, p531])).
% 26.23/14.03 cnf(ssp90, plain, (~spl20 | spl49 | spl58), inference(avatar_split_clause, [status(thm)], [p1137, sdef49, sdef58])).
% 26.23/14.03 cnf(p945, plain, (distinct_lines(line_connecting(sk0,X0),line_connecting(sk2,sk1)) | distinct_points(X0,sk1) | ~spl20), inference(resolution, [status(thm)], [p531, c1])).
% 26.23/14.03 cnf(p1138, plain, (apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | distinct_points(X0,sk1) | ~spl20), inference(resolution, [status(thm)], [p129, p945])).
% 26.23/14.03 cnf(ssp91, plain, (~spl20 | spl37 | spl39 | spl49), inference(avatar_split_clause, [status(thm)], [p1138, sdef37, sdef39, sdef49])).
% 26.23/14.03 cnf(p533, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [p212, p275])).
% 26.23/14.03 cnf(p1139, plain, apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [p129, p533])).
% 26.23/14.03 fof(sdef73, definition, (spl73 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(sk0,X1))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 26.23/14.03 cnf(ssp92, plain, (spl37 | spl39 | spl73), inference(avatar_split_clause, [status(thm)], [p1139, sdef37, sdef39, sdef73])).
% 26.23/14.03 cnf(p1141, plain, apart_point_and_line(sk1,line_connecting(X0,sk1)) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p129, p533])).
% 26.23/14.03 fof(sdef74, definition, (spl74 <=> (apart_point_and_line(sk1,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl74])], [avatar_definition])).
% 26.23/14.03 cnf(ssp93, plain, (spl58 | spl74), inference(avatar_split_clause, [status(thm)], [p1141, sdef58, sdef74])).
% 26.23/14.03 cnf(p949, plain, distinct_lines(line_connecting(X0,sk1),line_connecting(sk2,sk1)) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p533, c1])).
% 26.23/14.03 cnf(p1143, plain, apart_point_and_line(sk1,line_connecting(X0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p129, p949])).
% 26.23/14.03 cnf(ssp94, plain, (spl37 | spl39 | spl74), inference(avatar_split_clause, [status(thm)], [p1143, sdef37, sdef39, sdef74])).
% 26.23/14.03 cnf(p535, plain, (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk0,X1),X0) | distinct_points(X1,sk2) | ~spl21), inference(avatar_component_clause, [status(thm)], [sdef21])).
% 26.23/14.03 cnf(p1144, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,X1),X0) | distinct_points(X1,sk2) | ~spl21), inference(resolution, [status(thm)], [p129, p535])).
% 26.23/14.03 cnf(ssp95, plain, (~spl21 | spl37 | spl39 | spl64), inference(avatar_split_clause, [status(thm)], [p1144, sdef37, sdef39, sdef64])).
% 26.23/14.03 cnf(p1145, plain, (apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_points(X0,sk2) | ~spl21), inference(resolution, [status(thm)], [p129, p535])).
% 26.23/14.03 cnf(ssp96, plain, (~spl21 | spl50 | spl58), inference(avatar_split_clause, [status(thm)], [p1145, sdef50, sdef58])).
% 26.23/14.03 cnf(p954, plain, (distinct_lines(line_connecting(sk0,X0),line_connecting(sk2,sk1)) | distinct_points(X0,sk2) | ~spl21), inference(resolution, [status(thm)], [p535, c1])).
% 26.23/14.03 cnf(p1146, plain, (apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | distinct_points(X0,sk2) | ~spl21), inference(resolution, [status(thm)], [p129, p954])).
% 26.23/14.03 cnf(ssp97, plain, (~spl21 | spl37 | spl39 | spl50), inference(avatar_split_clause, [status(thm)], [p1146, sdef37, sdef39, sdef50])).
% 26.23/14.03 cnf(p537, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(X1,sk2),X0) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [p212, p288])).
% 26.23/14.03 cnf(p1147, plain, apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(X1,sk2),X0) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [p129, p537])).
% 26.23/14.03 fof(sdef75, definition, (spl75 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(X1,sk2),X0) | distinct_points(sk0,X1))), introduced(definition, [new_symbols(naming, [spl75])], [avatar_definition])).
% 26.23/14.03 cnf(ssp98, plain, (spl37 | spl39 | spl75), inference(avatar_split_clause, [status(thm)], [p1147, sdef37, sdef39, sdef75])).
% 26.23/14.03 cnf(p1149, plain, apart_point_and_line(sk1,line_connecting(X0,sk2)) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,line_connecting(X0,sk2)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p129, p537])).
% 26.23/14.03 fof(sdef76, definition, (spl76 <=> (apart_point_and_line(sk1,line_connecting(X0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,sk2)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl76])], [avatar_definition])).
% 26.23/14.03 cnf(ssp99, plain, (spl58 | spl76), inference(avatar_split_clause, [status(thm)], [p1149, sdef58, sdef76])).
% 26.23/14.03 cnf(p964, plain, distinct_lines(line_connecting(X0,sk2),line_connecting(sk2,sk1)) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p537, c1])).
% 26.23/14.03 cnf(p1151, plain, apart_point_and_line(sk1,line_connecting(X0,sk2)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(X0,sk2)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p129, p964])).
% 26.23/14.03 cnf(ssp100, plain, (spl37 | spl39 | spl76), inference(avatar_split_clause, [status(thm)], [p1151, sdef37, sdef39, sdef76])).
% 26.23/14.03 cnf(p539, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [p212, p306])).
% 26.23/14.03 cnf(p1152, plain, apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [p129, p539])).
% 26.23/14.03 fof(sdef77, definition, (spl77 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(sk0,X1))), introduced(definition, [new_symbols(naming, [spl77])], [avatar_definition])).
% 26.23/14.03 cnf(ssp101, plain, (spl37 | spl39 | spl77), inference(avatar_split_clause, [status(thm)], [p1152, sdef37, sdef39, sdef77])).
% 26.23/14.03 cnf(p1154, plain, apart_point_and_line(sk1,line_connecting(sk1,X0)) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p129, p539])).
% 26.23/14.03 fof(sdef78, definition, (spl78 <=> (apart_point_and_line(sk1,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl78])], [avatar_definition])).
% 26.23/14.03 cnf(ssp102, plain, (spl58 | spl78), inference(avatar_split_clause, [status(thm)], [p1154, sdef58, sdef78])).
% 26.23/14.03 cnf(p968, plain, distinct_lines(line_connecting(sk1,X0),line_connecting(sk2,sk1)) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p539, c1])).
% 26.23/14.03 cnf(p1156, plain, apart_point_and_line(sk1,line_connecting(sk1,X0)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p129, p968])).
% 26.23/14.03 cnf(ssp103, plain, (spl37 | spl39 | spl78), inference(avatar_split_clause, [status(thm)], [p1156, sdef37, sdef39, sdef78])).
% 26.23/14.03 cnf(p541, plain, distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(sk2,X1),X0) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [p212, p329])).
% 26.23/14.03 cnf(p1157, plain, apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,X1),X0) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [p129, p541])).
% 26.23/14.03 fof(sdef79, definition, (spl79 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,X1),X0) | distinct_points(sk0,X1))), introduced(definition, [new_symbols(naming, [spl79])], [avatar_definition])).
% 26.23/14.03 cnf(ssp104, plain, (spl37 | spl39 | spl79), inference(avatar_split_clause, [status(thm)], [p1157, sdef37, sdef39, sdef79])).
% 26.23/14.03 cnf(p1159, plain, apart_point_and_line(sk1,line_connecting(sk2,X0)) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,line_connecting(sk2,X0)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p129, p541])).
% 26.23/14.03 fof(sdef80, definition, (spl80 <=> (apart_point_and_line(sk1,line_connecting(sk2,X0)) | apart_point_and_line(sk2,line_connecting(sk2,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl80])], [avatar_definition])).
% 26.23/14.03 cnf(ssp105, plain, (spl58 | spl80), inference(avatar_split_clause, [status(thm)], [p1159, sdef58, sdef80])).
% 26.23/14.03 cnf(p972, plain, distinct_lines(line_connecting(sk2,X0),line_connecting(sk2,sk1)) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p541, c1])).
% 26.23/14.03 cnf(p1161, plain, apart_point_and_line(sk1,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk2,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p129, p972])).
% 26.23/14.03 cnf(ssp106, plain, (spl37 | spl39 | spl80), inference(avatar_split_clause, [status(thm)], [p1161, sdef37, sdef39, sdef80])).
% 26.23/14.03 cnf(p543, plain, (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(X1,sk0),X0) | distinct_points(sk1,X1) | ~spl22), inference(avatar_component_clause, [status(thm)], [sdef22])).
% 26.23/14.03 cnf(p1162, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(X1,sk0),X0) | distinct_points(sk1,X1) | ~spl22), inference(resolution, [status(thm)], [p129, p543])).
% 26.23/14.03 cnf(ssp107, plain, (~spl22 | spl37 | spl39 | spl65), inference(avatar_split_clause, [status(thm)], [p1162, sdef37, sdef39, sdef65])).
% 26.23/14.03 cnf(p1163, plain, (apart_point_and_line(sk1,line_connecting(X0,sk0)) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,line_connecting(X0,sk0)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_points(sk1,X0) | ~spl22), inference(resolution, [status(thm)], [p129, p543])).
% 26.23/14.03 cnf(ssp108, plain, (~spl22 | spl51 | spl58), inference(avatar_split_clause, [status(thm)], [p1163, sdef51, sdef58])).
% 26.23/14.03 cnf(p976, plain, (distinct_lines(line_connecting(X0,sk0),line_connecting(sk2,sk1)) | distinct_points(sk1,X0) | ~spl22), inference(resolution, [status(thm)], [p543, c1])).
% 26.23/14.03 cnf(p1164, plain, (apart_point_and_line(sk1,line_connecting(X0,sk0)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(X0,sk0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | distinct_points(sk1,X0) | ~spl22), inference(resolution, [status(thm)], [p129, p976])).
% 26.23/14.03 cnf(ssp109, plain, (~spl22 | spl37 | spl39 | spl51), inference(avatar_split_clause, [status(thm)], [p1164, sdef37, sdef39, sdef51])).
% 26.23/14.03 cnf(p547, plain, (distinct_lines(line_connecting(sk2,sk1),X0) | distinct_lines(line_connecting(X1,sk0),X0) | distinct_points(sk2,X1) | ~spl24), inference(avatar_component_clause, [status(thm)], [sdef24])).
% 26.23/14.03 cnf(p1165, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(X1,sk0),X0) | distinct_points(sk2,X1) | ~spl24), inference(resolution, [status(thm)], [p129, p547])).
% 26.23/14.03 cnf(ssp110, plain, (~spl24 | spl37 | spl39 | spl66), inference(avatar_split_clause, [status(thm)], [p1165, sdef37, sdef39, sdef66])).
% 26.23/14.03 cnf(p1166, plain, (apart_point_and_line(sk1,line_connecting(X0,sk0)) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,line_connecting(X0,sk0)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_points(sk2,X0) | ~spl24), inference(resolution, [status(thm)], [p129, p547])).
% 26.23/14.03 cnf(ssp111, plain, (~spl24 | spl52 | spl58), inference(avatar_split_clause, [status(thm)], [p1166, sdef52, sdef58])).
% 26.23/14.03 cnf(p980, plain, (distinct_lines(line_connecting(X0,sk0),line_connecting(sk2,sk1)) | distinct_points(sk2,X0) | ~spl24), inference(resolution, [status(thm)], [p547, c1])).
% 26.23/14.03 cnf(p1167, plain, (apart_point_and_line(sk1,line_connecting(X0,sk0)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(X0,sk0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | distinct_points(sk2,X0) | ~spl24), inference(resolution, [status(thm)], [p129, p980])).
% 26.23/14.04 cnf(ssp112, plain, (~spl24 | spl37 | spl39 | spl52), inference(avatar_split_clause, [status(thm)], [p1167, sdef37, sdef39, sdef52])).
% 26.23/14.04 cnf(p554, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl16), inference(resolution, [status(thm)], [p522, c4])).
% 26.23/14.04 cnf(p1168, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl16), inference(resolution, [status(thm)], [p129, p554])).
% 26.23/14.04 cnf(ssp113, plain, (~spl16 | spl41 | spl42 | spl67), inference(avatar_split_clause, [status(thm)], [p1168, sdef41, sdef42, sdef67])).
% 26.23/14.04 cnf(p1169, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X1,X0) | ~spl16), inference(resolution, [status(thm)], [p129, p554])).
% 26.23/14.04 cnf(ssp114, plain, (~spl16 | spl37 | spl39 | spl68), inference(avatar_split_clause, [status(thm)], [p1169, sdef37, sdef39, sdef68])).
% 26.23/14.04 cnf(p1170, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl16), inference(resolution, [status(thm)], [p129, p554])).
% 26.23/14.04 cnf(ssp115, plain, (~spl16 | spl53 | spl58), inference(avatar_split_clause, [status(thm)], [p1170, sdef53, sdef58])).
% 26.23/14.04 cnf(p984, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl16), inference(resolution, [status(thm)], [p554, c1])).
% 26.23/14.04 cnf(p1171, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl16), inference(resolution, [status(thm)], [p129, p984])).
% 26.23/14.04 cnf(ssp116, plain, (~spl16 | spl41 | spl42 | spl69), inference(avatar_split_clause, [status(thm)], [p1171, sdef41, sdef42, sdef69])).
% 26.23/14.04 cnf(p556, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl17), inference(resolution, [status(thm)], [p524, c4])).
% 26.23/14.04 cnf(p1172, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl17), inference(resolution, [status(thm)], [p129, p556])).
% 26.23/14.04 cnf(ssp117, plain, (~spl17 | spl43 | spl44 | spl67), inference(avatar_split_clause, [status(thm)], [p1172, sdef43, sdef44, sdef67])).
% 26.23/14.04 cnf(p1173, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl17), inference(resolution, [status(thm)], [p129, p556])).
% 26.23/14.04 cnf(ssp118, plain, (~spl17 | spl37 | spl39 | spl70), inference(avatar_split_clause, [status(thm)], [p1173, sdef37, sdef39, sdef70])).
% 26.23/14.04 cnf(p1174, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl17), inference(resolution, [status(thm)], [p129, p556])).
% 26.23/14.04 cnf(ssp119, plain, (~spl17 | spl54 | spl58), inference(avatar_split_clause, [status(thm)], [p1174, sdef54, sdef58])).
% 26.23/14.04 cnf(p990, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl17), inference(resolution, [status(thm)], [p556, c1])).
% 26.23/14.04 cnf(p1175, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl17), inference(resolution, [status(thm)], [p129, p990])).
% 26.23/14.04 cnf(ssp120, plain, (~spl17 | spl43 | spl44 | spl69), inference(avatar_split_clause, [status(thm)], [p1175, sdef43, sdef44, sdef69])).
% 26.23/14.04 cnf(p559, plain, (distinct_lines(line_connecting(sk1,sk0),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl18), inference(resolution, [status(thm)], [p526, c4])).
% 26.23/14.04 cnf(p1176, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl18), inference(resolution, [status(thm)], [p129, p559])).
% 26.23/14.04 cnf(ssp121, plain, (~spl18 | spl45 | spl46 | spl67), inference(avatar_split_clause, [status(thm)], [p1176, sdef45, sdef46, sdef67])).
% 26.23/14.04 cnf(p1177, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk0),X1) | distinct_lines(X1,X0) | ~spl18), inference(resolution, [status(thm)], [p129, p559])).
% 26.23/14.04 cnf(ssp122, plain, (~spl18 | spl37 | spl39 | spl71), inference(avatar_split_clause, [status(thm)], [p1177, sdef37, sdef39, sdef71])).
% 26.23/14.04 cnf(p1178, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk1,sk0),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl18), inference(resolution, [status(thm)], [p129, p559])).
% 26.23/14.04 cnf(ssp123, plain, (~spl18 | spl55 | spl58), inference(avatar_split_clause, [status(thm)], [p1178, sdef55, sdef58])).
% 26.23/14.04 cnf(p995, plain, (distinct_lines(line_connecting(sk1,sk0),X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl18), inference(resolution, [status(thm)], [p559, c1])).
% 26.23/14.04 cnf(p1179, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl18), inference(resolution, [status(thm)], [p129, p995])).
% 26.23/14.04 cnf(ssp124, plain, (~spl18 | spl45 | spl46 | spl69), inference(avatar_split_clause, [status(thm)], [p1179, sdef45, sdef46, sdef69])).
% 26.23/14.04 cnf(p561, plain, (distinct_lines(line_connecting(sk2,sk0),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl19), inference(resolution, [status(thm)], [p528, c4])).
% 26.23/14.04 cnf(p1180, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl19), inference(resolution, [status(thm)], [p129, p561])).
% 26.23/14.04 cnf(ssp125, plain, (~spl19 | spl47 | spl48 | spl67), inference(avatar_split_clause, [status(thm)], [p1180, sdef47, sdef48, sdef67])).
% 26.23/14.04 cnf(p1181, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk0),X1) | distinct_lines(X1,X0) | ~spl19), inference(resolution, [status(thm)], [p129, p561])).
% 26.23/14.04 cnf(ssp126, plain, (~spl19 | spl37 | spl39 | spl72), inference(avatar_split_clause, [status(thm)], [p1181, sdef37, sdef39, sdef72])).
% 26.23/14.04 cnf(p1182, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk2,sk0),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl19), inference(resolution, [status(thm)], [p129, p561])).
% 26.23/14.04 cnf(ssp127, plain, (~spl19 | spl56 | spl58), inference(avatar_split_clause, [status(thm)], [p1182, sdef56, sdef58])).
% 26.23/14.04 cnf(p1001, plain, (distinct_lines(line_connecting(sk2,sk0),X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl19), inference(resolution, [status(thm)], [p561, c1])).
% 26.23/14.04 cnf(p1183, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl19), inference(resolution, [status(thm)], [p129, p1001])).
% 26.23/14.04 cnf(ssp128, plain, (~spl19 | spl47 | spl48 | spl69), inference(avatar_split_clause, [status(thm)], [p1183, sdef47, sdef48, sdef69])).
% 26.23/14.04 cnf(p1184, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(X1,sk1) | distinct_points(X1,X0) | ~spl26), inference(resolution, [status(thm)], [p129, p563])).
% 26.23/14.04 fof(sdef81, definition, (spl81 <=> (apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(X1,sk1) | distinct_points(X1,X0))), introduced(definition, [new_symbols(naming, [spl81])], [avatar_definition])).
% 26.23/14.04 cnf(ssp129, plain, (~spl26 | spl37 | spl39 | spl81), inference(avatar_split_clause, [status(thm)], [p1184, sdef37, sdef39, sdef81])).
% 26.23/14.04 cnf(p1008, plain, (distinct_points(sk1,X0) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | ~spl26), inference(resolution, [status(thm)], [p563, c0])).
% 26.23/14.04 cnf(p1186, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(sk1,X0) | ~spl26), inference(resolution, [status(thm)], [p129, p1008])).
% 26.23/14.04 cnf(ssp130, plain, (~spl26 | spl37 | spl39 | spl60), inference(avatar_split_clause, [status(thm)], [p1186, sdef37, sdef39, sdef60])).
% 26.23/14.04 cnf(p1009, plain, (distinct_points(X0,sk1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(sk0,X0)) | ~spl26), inference(resolution, [status(thm)], [p563, c0])).
% 26.23/14.04 cnf(p1187, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,X0)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,X0)) | distinct_points(X0,sk1) | ~spl26), inference(resolution, [status(thm)], [p129, p1009])).
% 26.23/14.04 cnf(ssp131, plain, (~spl26 | spl37 | spl39 | spl49), inference(avatar_split_clause, [status(thm)], [p1187, sdef37, sdef39, sdef49])).
% 26.23/14.04 cnf(p567, plain, (distinct_points(sk0,X0) | distinct_points(sk1,X1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,X1)) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 26.23/14.04 cnf(p1188, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(X0,X1)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(X0,X1)) | distinct_points(sk0,X0) | distinct_points(sk1,X1) | ~spl28), inference(resolution, [status(thm)], [p129, p567])).
% 26.23/14.04 fof(sdef82, definition, (spl82 <=> (apart_point_and_line(sk1,line_connecting(X0,X1)) | apart_point_and_line(sk2,line_connecting(X0,X1)) | distinct_points(sk0,X0) | distinct_points(sk1,X1))), introduced(definition, [new_symbols(naming, [spl82])], [avatar_definition])).
% 26.23/14.04 cnf(ssp132, plain, (~spl28 | spl37 | spl39 | spl82), inference(avatar_split_clause, [status(thm)], [p1188, sdef37, sdef39, sdef82])).
% 26.23/14.04 cnf(p570, plain, (distinct_points(sk0,X0) | distinct_points(sk2,X1) | distinct_lines(line_connecting(sk2,sk1),line_connecting(X0,X1)) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 26.23/14.04 cnf(p1190, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(X0,X1)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(X0,X1)) | distinct_points(sk0,X0) | distinct_points(sk2,X1) | ~spl29), inference(resolution, [status(thm)], [p129, p570])).
% 26.23/14.04 fof(sdef83, definition, (spl83 <=> (apart_point_and_line(sk1,line_connecting(X0,X1)) | apart_point_and_line(sk2,line_connecting(X0,X1)) | distinct_points(sk0,X0) | distinct_points(sk2,X1))), introduced(definition, [new_symbols(naming, [spl83])], [avatar_definition])).
% 26.23/14.04 cnf(ssp133, plain, (~spl29 | spl37 | spl39 | spl83), inference(avatar_split_clause, [status(thm)], [p1190, sdef37, sdef39, sdef83])).
% 26.23/14.04 cnf(p130, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(sk0,X2), inference(resolution, [status(thm)], [c10, p19])).
% 26.23/14.04 cnf(p1200, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl0), inference(resolution, [status(thm)], [p130, p925])).
% 26.23/14.04 fof(sdef84, definition, (spl84 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl84])], [avatar_definition])).
% 26.23/14.04 cnf(ssp134, plain, (~spl0 | spl41 | spl84), inference(avatar_split_clause, [status(thm)], [p1200, sdef41, sdef84])).
% 26.23/14.04 cnf(p1202, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl2), inference(resolution, [status(thm)], [p130, p930])).
% 26.23/14.04 fof(sdef85, definition, (spl85 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl85])], [avatar_definition])).
% 26.23/14.04 cnf(ssp135, plain, (~spl2 | spl43 | spl85), inference(avatar_split_clause, [status(thm)], [p1202, sdef43, sdef85])).
% 26.23/14.04 cnf(p1204, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk1,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl3), inference(resolution, [status(thm)], [p130, p935])).
% 26.23/14.04 fof(sdef86, definition, (spl86 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk1,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl86])], [avatar_definition])).
% 26.23/14.04 cnf(ssp136, plain, (~spl3 | spl45 | spl86), inference(avatar_split_clause, [status(thm)], [p1204, sdef45, sdef86])).
% 26.23/14.04 cnf(p1206, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl4), inference(resolution, [status(thm)], [p130, p940])).
% 26.23/14.04 fof(sdef87, definition, (spl87 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl87])], [avatar_definition])).
% 26.23/14.04 cnf(ssp137, plain, (~spl4 | spl47 | spl87), inference(avatar_split_clause, [status(thm)], [p1206, sdef47, sdef87])).
% 26.23/14.04 cnf(p1208, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl16), inference(resolution, [status(thm)], [p130, p984])).
% 26.23/14.04 cnf(ssp138, plain, (~spl16 | spl41 | spl84), inference(avatar_split_clause, [status(thm)], [p1208, sdef41, sdef84])).
% 26.23/14.04 cnf(p1209, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl17), inference(resolution, [status(thm)], [p130, p990])).
% 26.23/14.04 cnf(ssp139, plain, (~spl17 | spl43 | spl85), inference(avatar_split_clause, [status(thm)], [p1209, sdef43, sdef85])).
% 26.23/14.04 cnf(p1210, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk1,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl18), inference(resolution, [status(thm)], [p130, p995])).
% 26.23/14.04 cnf(ssp140, plain, (~spl18 | spl45 | spl86), inference(avatar_split_clause, [status(thm)], [p1210, sdef45, sdef86])).
% 26.23/14.04 cnf(p1211, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl19), inference(resolution, [status(thm)], [p130, p1001])).
% 26.23/14.04 cnf(ssp141, plain, (~spl19 | spl47 | spl87), inference(avatar_split_clause, [status(thm)], [p1211, sdef47, sdef87])).
% 26.23/14.04 cnf(sat_ref, plain, $false, inference(avatar_sat_refutation, [status(thm)], [ssp0, ssp1, ssp2, ssp3, ssp4, ssp5, ssp6, ssp7, ssp8, ssp9, ssp10, ssp11, ssp12, ssp13, ssp14, ssp15, ssp16, ssp17, ssp18, ssp19, ssp20, ssp21, ssp22, ssp23, ssp24, ssp25, ssp26, ssp27, ssp28, ssp29, ssp30, ssp31, ssp32, ssp33, ssp34, ssp35, ssp36, ssp37, ssp38, ssp39, ssp40, ssp41, ssp42, ssp43, ssp44, ssp45, ssp46, ssp47, ssp48, ssp49, ssp50, ssp51, ssp52, ssp53, ssp54, ssp55, ssp56, ssp57, ssp58, ssp59, ssp60, ssp61, ssp62, ssp63, ssp64, ssp65, ssp66, ssp67, ssp68, ssp69, ssp70, ssp71, ssp72, ssp73, ssp74, ssp75, ssp76, ssp77, ssp78, ssp79, ssp80, ssp81, ssp82, ssp83, ssp84, ssp85, ssp86, ssp87, ssp88, ssp89, ssp90, ssp91, ssp92, ssp93, ssp94, ssp95, ssp96, ssp97, ssp98, ssp99, ssp100, ssp101, ssp102, ssp103, ssp104, ssp105, ssp106, ssp107, ssp108, ssp109, ssp110, ssp111, ssp112, ssp113, ssp114, ssp115, ssp116, ssp117, ssp118, ssp119, ssp120, ssp121, ssp122, ssp123, ssp124, ssp125, ssp126, ssp127, ssp128, ssp129, ssp130, ssp131, ssp132, ssp133, ssp134, ssp135, ssp136, ssp137, ssp138, ssp139, ssp140, ssp141, sct0, sct1, sct2, sct3, sct4, sct5, sct6, sct7, sct8])).
% 26.23/14.04 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------